%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : CAT004-1 : TPTP v9.3.1. Released v1.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 : n019.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 06:55:18 AM UTC 2026
% Result : Unsatisfiable 78.75s 18.83s
% Output : Refutation 79.95s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 19
% Syntax : Number of formulae : 820 ( 62 unt; 0 typ; 0 def)
% Number of atoms : 3254 (1017 equ; 0 cnn)
% Maximal formula atoms : 12 ( 3 avg)
% Number of connectives : 10488 (1996 ~;1672 |; 0 &;6820 @)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 31 ( 8 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 14 ( 11 usr; 8 con; 0-3 aty)
% Number of variables : 1491 ( 0 ^;1491 !; 0 ?;1491 :)
% Comments :
%------------------------------------------------------------------------------
thf(h_decl,type,
h: $i ).
thf(g_decl,type,
g: $i ).
thf(defined_decl,type,
defined: $i > $i > $o ).
thf(domain_decl,type,
domain: $i > $i ).
thf(codomain_decl,type,
codomain: $i > $i ).
thf(product_decl,type,
product: $i > $i > $i > $o ).
thf(a_decl,type,
a: $i ).
thf(compose_decl,type,
compose: $i > $i > $i ).
thf(b_decl,type,
b: $i ).
thf(c_decl,type,
c: $i ).
thf(d_decl,type,
d: $i ).
thf(19,axiom,
d @ ( c @ ( h @ product ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hc_equals_d) ).
thf(54,plain,
d @ ( c @ ( h @ product ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[19]) ).
thf(8,axiom,
! [C: $i,B: $i,A: $i] :
( ( B @ ( A @ defined ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associative_property1) ).
thf(33,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( A @ defined ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(34,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( A @ defined ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(cnf,[status(esa)],[33]) ).
thf(1264,plain,
! [C: $i,B: $i,A: $i] :
( ( ( d @ ( c @ ( h @ product ) ) )
!= ( C @ ( B @ ( A @ product ) ) ) )
| ( B @ ( A @ defined ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[54,34]) ).
thf(1265,plain,
! [C: $i,B: $i,A: $i] :
( ( ( d @ ( c @ ( h @ product ) ) )
!= ( C @ ( B @ ( A @ product ) ) ) )
| ( B @ ( A @ defined ) ) ),
inference(simp,[status(thm)],[1264]) ).
thf(1266,plain,
c @ ( h @ defined ),
inference(pattern_uni,[status(thm)],[1265:[bind(A,$thf( h )),bind(B,$thf( c )),bind(C,$thf( d ))]]) ).
thf(6,axiom,
! [B: $i,A: $i] :
( ( B @ ( A @ compose ) @ ( B @ ( A @ product ) ) )
| ~ ( B @ ( A @ defined ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',closure_of_composition) ).
thf(30,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ compose ) @ ( B @ ( A @ product ) ) )
| ~ ( B @ ( A @ defined ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(31,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ compose ) @ ( B @ ( A @ product ) ) )
| ~ ( B @ ( A @ defined ) ) ),
inference(cnf,[status(esa)],[30]) ).
thf(1320,plain,
! [B: $i,A: $i] :
( ( ( c @ ( h @ defined ) )
!= ( B @ ( A @ defined ) ) )
| ( B @ ( A @ compose ) @ ( B @ ( A @ product ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1266,31]) ).
thf(1321,plain,
! [B: $i,A: $i] :
( ( ( c @ ( h @ defined ) )
!= ( B @ ( A @ defined ) ) )
| ( B @ ( A @ compose ) @ ( B @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[1320]) ).
thf(1322,plain,
c @ ( h @ compose ) @ ( c @ ( h @ product ) ),
inference(pattern_uni,[status(thm)],[1321:[bind(A,$thf( h )),bind(B,$thf( c ))]]) ).
thf(7,axiom,
c @ ( b @ ( a @ product ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ab_equals_c) ).
thf(32,plain,
c @ ( b @ ( a @ product ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(1279,plain,
! [C: $i,B: $i,A: $i] :
( ( ( c @ ( b @ ( a @ product ) ) )
!= ( C @ ( B @ ( A @ product ) ) ) )
| ( B @ ( A @ defined ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[32,34]) ).
thf(1280,plain,
! [C: $i,B: $i,A: $i] :
( ( ( c @ ( b @ ( a @ product ) ) )
!= ( C @ ( B @ ( A @ product ) ) ) )
| ( B @ ( A @ defined ) ) ),
inference(simp,[status(thm)],[1279]) ).
thf(1281,plain,
b @ ( a @ defined ),
inference(pattern_uni,[status(thm)],[1280:[bind(A,$thf( a )),bind(B,$thf( b )),bind(C,$thf( c ))]]) ).
thf(18,axiom,
d @ ( c @ ( g @ product ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gc_equals_d) ).
thf(53,plain,
d @ ( c @ ( g @ product ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[18]) ).
thf(11,axiom,
! [D: $i,C: $i,B: $i,A: $i] :
( ( A @ ( D @ defined ) )
| ~ ( C @ ( D @ defined ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',category_theory_axiom3) ).
thf(38,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( A @ ( D @ defined ) )
| ~ ( C @ ( D @ defined ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[11]) ).
thf(39,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( A @ ( D @ defined ) )
| ~ ( C @ ( D @ defined ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(cnf,[status(esa)],[38]) ).
thf(2140,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( d @ ( c @ ( g @ product ) ) )
!= ( C @ ( B @ ( A @ product ) ) ) )
| ( A @ ( D @ defined ) )
| ~ ( C @ ( D @ defined ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[53,39]) ).
thf(2141,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( d @ ( c @ ( g @ product ) ) )
!= ( C @ ( B @ ( A @ product ) ) ) )
| ( A @ ( D @ defined ) )
| ~ ( C @ ( D @ defined ) ) ),
inference(simp,[status(thm)],[2140]) ).
thf(2142,plain,
! [A: $i] :
( ( g @ ( A @ defined ) )
| ~ ( d @ ( A @ defined ) ) ),
inference(pattern_uni,[status(thm)],[2141:[bind(A,$thf( g )),bind(B,$thf( c )),bind(C,$thf( d ))]]) ).
thf(2221,plain,
! [A: $i] :
( ( g @ ( A @ defined ) )
| ~ ( d @ ( A @ defined ) ) ),
inference(simp,[status(thm)],[2142]) ).
thf(29262,plain,
! [A: $i] :
( ( ( b @ ( a @ defined ) )
!= ( d @ ( A @ defined ) ) )
| ( g @ ( A @ defined ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1281,2221]) ).
thf(29263,plain,
! [A: $i] :
( ( ( b @ ( a @ defined ) )
!= ( d @ ( A @ defined ) ) )
| ( g @ ( A @ defined ) ) ),
inference(simp,[status(thm)],[29262]) ).
thf(29340,plain,
! [A: $i] :
( ( d != b )
| ( a != A )
| ( g @ ( A @ defined ) ) ),
inference(simp,[status(thm)],[29263]) ).
thf(29375,plain,
( ( d != b )
| ( g @ ( a @ defined ) ) ),
inference(simp,[status(thm)],[29340]) ).
thf(15,axiom,
! [A: $i] : ( A @ ( A @ domain @ ( A @ product ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_on_domain) ).
thf(48,plain,
! [A: $i] : ( A @ ( A @ domain @ ( A @ product ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[15]) ).
thf(10,axiom,
! [A: $i] : ( A @ ( A @ ( A @ codomain @ product ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_on_codomain) ).
thf(37,plain,
! [A: $i] : ( A @ ( A @ ( A @ codomain @ product ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).
thf(5,axiom,
! [C: $i,B: $i,A: $i] :
( ( A = C )
| ~ ( B @ ( a @ ( C @ product ) ) )
| ~ ( B @ ( a @ ( A @ product ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cancellation_for_product1) ).
thf(27,plain,
! [C: $i,B: $i,A: $i] :
( ( A = C )
| ~ ( B @ ( a @ ( C @ product ) ) )
| ~ ( B @ ( a @ ( A @ product ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(28,plain,
! [C: $i,B: $i,A: $i] :
( ( A = C )
| ~ ( B @ ( a @ ( C @ product ) ) )
| ~ ( B @ ( a @ ( A @ product ) ) ) ),
inference(cnf,[status(esa)],[27]) ).
thf(29,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( B @ ( a @ ( C @ product ) ) )
| ~ ( B @ ( a @ ( A @ product ) ) )
| ( A = C ) ),
inference(lifteq,[status(thm)],[28]) ).
thf(272,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( A @ codomain @ product ) ) )
!= ( C @ ( a @ ( B @ product ) ) ) )
| ~ ( C @ ( a @ ( D @ product ) ) )
| ~ $true
| ( B = D ) ),
inference(paramod_ordered,[status(thm)],[37,29]) ).
thf(273,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( A @ codomain @ product ) ) )
!= ( C @ ( a @ ( B @ product ) ) ) )
| ~ ( C @ ( a @ ( D @ product ) ) )
| ( B = D ) ),
inference(simp,[status(thm)],[272]) ).
thf(274,plain,
! [A: $i] :
( ~ ( a @ ( a @ ( A @ product ) ) )
| ( ( a @ codomain )
= A ) ),
inference(pattern_uni,[status(thm)],[273:[bind(A,$thf( a )),bind(B,$thf( a @ codomain )),bind(C,$thf( a )),bind(D,$thf( D ))]]) ).
thf(297,plain,
! [A: $i] :
( ~ ( a @ ( a @ ( A @ product ) ) )
| ( ( a @ codomain )
= A ) ),
inference(simp,[status(thm)],[274]) ).
thf(397,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ domain @ ( A @ product ) ) )
!= ( a @ ( a @ ( B @ product ) ) ) )
| ~ $true
| ( ( a @ codomain )
= B ) ),
inference(paramod_ordered,[status(thm)],[48,297]) ).
thf(398,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ domain @ ( A @ product ) ) )
!= ( a @ ( a @ ( B @ product ) ) ) )
| ( ( a @ codomain )
= B ) ),
inference(simp,[status(thm)],[397]) ).
thf(413,plain,
! [B: $i,A: $i] :
( ( A != a )
| ( ( A @ domain )
!= a )
| ( A != B )
| ( ( a @ codomain )
= B ) ),
inference(simp,[status(thm)],[398]) ).
thf(429,plain,
( ( ( a @ domain )
!= a )
| ( ( a @ codomain )
= a ) ),
inference(simp,[status(thm)],[413]) ).
thf(3,axiom,
! [A: $i] : ( A @ ( A @ codomain @ defined ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mapping_from_codomain_of_x_to_x) ).
thf(24,plain,
! [A: $i] : ( A @ ( A @ codomain @ defined ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(448,plain,
! [A: $i] :
( ( ( a @ codomain )
!= ( A @ codomain ) )
| ( A @ ( a @ defined ) )
| ( ( a @ domain )
!= a ) ),
inference(paramod_ordered,[status(thm)],[429,24]) ).
thf(449,plain,
( ( a @ ( a @ defined ) )
| ( ( a @ domain )
!= a ) ),
inference(pattern_uni,[status(thm)],[448:[bind(A,$thf( a ))]]) ).
thf(699,plain,
! [B: $i,A: $i] :
( ( ( a @ ( a @ defined ) )
!= ( B @ ( A @ defined ) ) )
| ( B @ ( A @ compose ) @ ( B @ ( A @ product ) ) )
| ~ $true
| ( ( a @ domain )
!= a ) ),
inference(paramod_ordered,[status(thm)],[449,31]) ).
thf(700,plain,
! [B: $i,A: $i] :
( ( ( a @ ( a @ defined ) )
!= ( B @ ( A @ defined ) ) )
| ( B @ ( A @ compose ) @ ( B @ ( A @ product ) ) )
| ( ( a @ domain )
!= a ) ),
inference(simp,[status(thm)],[699]) ).
thf(701,plain,
( ( a @ ( a @ compose ) @ ( a @ ( a @ product ) ) )
| ( ( a @ domain )
!= a ) ),
inference(pattern_uni,[status(thm)],[700:[bind(A,$thf( a )),bind(B,$thf( a ))]]) ).
thf(1,negated_conjecture,
h != g,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_h_equals_g) ).
thf(20,plain,
h != g,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[1]) ).
thf(21,plain,
h != g,
inference(polarity_switch,[status(thm)],[20]) ).
thf(22,plain,
g != h,
inference(lifteq,[status(thm)],[21]) ).
thf(244,plain,
! [C: $i,B: $i,A: $i] :
( ( A != g )
| ( C != h )
| ~ ( B @ ( a @ ( C @ product ) ) )
| ~ ( B @ ( a @ ( A @ product ) ) ) ),
inference(paramod_ordered,[status(thm)],[29,22]) ).
thf(245,plain,
! [B: $i,A: $i] :
( ( B != h )
| ~ ( A @ ( a @ ( B @ product ) ) )
| ~ ( A @ ( a @ ( g @ product ) ) ) ),
inference(pattern_uni,[status(thm)],[244:[bind(A,$thf( g ))]]) ).
thf(315,plain,
! [A: $i] :
( ~ ( A @ ( a @ ( h @ product ) ) )
| ~ ( A @ ( a @ ( g @ product ) ) ) ),
inference(simp,[status(thm)],[245]) ).
thf(515,plain,
! [A: $i] :
( ( ( d @ ( c @ ( g @ product ) ) )
!= ( A @ ( a @ ( g @ product ) ) ) )
| ~ ( A @ ( a @ ( h @ product ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[53,315]) ).
thf(516,plain,
! [A: $i] :
( ( ( d @ ( c @ ( g @ product ) ) )
!= ( A @ ( a @ ( g @ product ) ) ) )
| ~ ( A @ ( a @ ( h @ product ) ) ) ),
inference(simp,[status(thm)],[515]) ).
thf(544,plain,
! [A: $i] :
( ( d != A )
| ( c != a )
| ( g != g )
| ~ ( A @ ( a @ ( h @ product ) ) ) ),
inference(simp,[status(thm)],[516]) ).
thf(553,plain,
( ( c != a )
| ~ ( d @ ( a @ ( h @ product ) ) ) ),
inference(simp,[status(thm)],[544]) ).
thf(591,plain,
( ( ( d @ ( c @ ( h @ product ) ) )
!= ( d @ ( a @ ( h @ product ) ) ) )
| ( c != a )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[54,553]) ).
thf(592,plain,
( ( ( d @ ( c @ ( h @ product ) ) )
!= ( d @ ( a @ ( h @ product ) ) ) )
| ( c != a ) ),
inference(simp,[status(thm)],[591]) ).
thf(605,plain,
( ( d != d )
| ( c != a )
| ( h != h )
| ( c != a ) ),
inference(simp,[status(thm)],[592]) ).
thf(613,plain,
c != a,
inference(simp,[status(thm)],[605]) ).
thf(692,plain,
! [C: $i,B: $i,A: $i] :
( ( A != c )
| ( C != a )
| ~ ( B @ ( a @ ( C @ product ) ) )
| ~ ( B @ ( a @ ( A @ product ) ) ) ),
inference(paramod_ordered,[status(thm)],[29,613]) ).
thf(693,plain,
! [B: $i,A: $i] :
( ( B != a )
| ~ ( A @ ( a @ ( B @ product ) ) )
| ~ ( A @ ( a @ ( c @ product ) ) ) ),
inference(pattern_uni,[status(thm)],[692:[bind(A,$thf( c ))]]) ).
thf(697,plain,
! [A: $i] :
( ~ ( A @ ( a @ ( a @ product ) ) )
| ~ ( A @ ( a @ ( c @ product ) ) ) ),
inference(simp,[status(thm)],[693]) ).
thf(43964,plain,
! [A: $i] :
( ( ( a @ ( a @ compose ) @ ( a @ ( a @ product ) ) )
!= ( A @ ( a @ ( a @ product ) ) ) )
| ~ $true
| ~ ( A @ ( a @ ( c @ product ) ) )
| ( ( a @ domain )
!= a ) ),
inference(paramod_ordered,[status(thm)],[701,697]) ).
thf(43965,plain,
! [A: $i] :
( ( ( a @ ( a @ compose ) @ ( a @ ( a @ product ) ) )
!= ( A @ ( a @ ( a @ product ) ) ) )
| ~ ( A @ ( a @ ( c @ product ) ) )
| ( ( a @ domain )
!= a ) ),
inference(simp,[status(thm)],[43964]) ).
thf(43966,plain,
( ~ ( a @ ( a @ compose ) @ ( a @ ( c @ product ) ) )
| ( ( a @ domain )
!= a ) ),
inference(pattern_uni,[status(thm)],[43965:[bind(A,$thf( a @ ( a @ compose ) ))]]) ).
thf(29269,plain,
! [A: $i] :
( ( ( c @ ( h @ defined ) )
!= ( d @ ( A @ defined ) ) )
| ( g @ ( A @ defined ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1266,2221]) ).
thf(29270,plain,
! [A: $i] :
( ( ( c @ ( h @ defined ) )
!= ( d @ ( A @ defined ) ) )
| ( g @ ( A @ defined ) ) ),
inference(simp,[status(thm)],[29269]) ).
thf(29346,plain,
! [A: $i] :
( ( d != c )
| ( h != A )
| ( g @ ( A @ defined ) ) ),
inference(simp,[status(thm)],[29270]) ).
thf(29380,plain,
( ( d != c )
| ( g @ ( h @ defined ) ) ),
inference(simp,[status(thm)],[29346]) ).
thf(32768,plain,
! [B: $i,A: $i] :
( ( ( g @ ( h @ defined ) )
!= ( B @ ( A @ defined ) ) )
| ( B @ ( A @ compose ) @ ( B @ ( A @ product ) ) )
| ~ $true
| ( d != c ) ),
inference(paramod_ordered,[status(thm)],[29380,31]) ).
thf(32769,plain,
! [B: $i,A: $i] :
( ( ( g @ ( h @ defined ) )
!= ( B @ ( A @ defined ) ) )
| ( B @ ( A @ compose ) @ ( B @ ( A @ product ) ) )
| ( d != c ) ),
inference(simp,[status(thm)],[32768]) ).
thf(32770,plain,
( ( g @ ( h @ compose ) @ ( g @ ( h @ product ) ) )
| ( d != c ) ),
inference(pattern_uni,[status(thm)],[32769:[bind(A,$thf( h )),bind(B,$thf( g ))]]) ).
thf(2,axiom,
! [A: $i] : ( A @ domain @ ( A @ defined ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mapping_from_x_to_its_domain) ).
thf(23,plain,
! [A: $i] : ( A @ domain @ ( A @ defined ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(749,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ domain @ ( A @ defined ) )
!= ( C @ ( B @ defined ) ) )
| ( C @ ( B @ compose ) @ ( C @ ( B @ product ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[23,31]) ).
thf(750,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ domain @ ( A @ defined ) )
!= ( C @ ( B @ defined ) ) )
| ( C @ ( B @ compose ) @ ( C @ ( B @ product ) ) ) ),
inference(simp,[status(thm)],[749]) ).
thf(751,plain,
! [A: $i] : ( A @ domain @ ( A @ compose ) @ ( A @ domain @ ( A @ product ) ) ),
inference(pattern_uni,[status(thm)],[750:[bind(A,$thf( D )),bind(B,$thf( D )),bind(C,$thf( D @ domain ))]]) ).
thf(762,plain,
! [A: $i] : ( A @ domain @ ( A @ compose ) @ ( A @ domain @ ( A @ product ) ) ),
inference(simp,[status(thm)],[751]) ).
thf(29248,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ codomain @ defined ) )
!= ( d @ ( B @ defined ) ) )
| ( g @ ( B @ defined ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[24,2221]) ).
thf(29249,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ codomain @ defined ) )
!= ( d @ ( B @ defined ) ) )
| ( g @ ( B @ defined ) ) ),
inference(simp,[status(thm)],[29248]) ).
thf(29250,plain,
g @ ( d @ codomain @ defined ),
inference(pattern_uni,[status(thm)],[29249:[bind(A,$thf( d )),bind(B,$thf( d @ codomain ))]]) ).
thf(4,axiom,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( A @ defined ) )
| ~ ( D @ ( C @ defined ) )
| ~ ( E @ ( D @ ( B @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',category_theory_axiom1) ).
thf(25,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( A @ defined ) )
| ~ ( D @ ( C @ defined ) )
| ~ ( E @ ( D @ ( B @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(26,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( A @ defined ) )
| ~ ( D @ ( C @ defined ) )
| ~ ( E @ ( D @ ( B @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(cnf,[status(esa)],[25]) ).
thf(76,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ $true
| ( ( E @ ( D @ ( B @ product ) ) )
!= ( C @ ( B @ ( A @ product ) ) ) )
| ( E @ ( A @ defined ) )
| ~ ( D @ ( C @ defined ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(eqfactor_ordered,[status(thm)],[26]) ).
thf(77,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ defined ) )
| ~ ( A @ ( B @ defined ) )
| ~ ( B @ ( A @ ( A @ product ) ) ) ),
inference(pattern_uni,[status(thm)],[76:[bind(A,$thf( D )),bind(B,$thf( D )),bind(C,$thf( E ))]]) ).
thf(84,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ defined ) )
| ~ ( A @ ( B @ defined ) )
| ~ ( B @ ( A @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[77]) ).
thf(29433,plain,
! [B: $i,A: $i] :
( ( ( g @ ( d @ codomain @ defined ) )
!= ( A @ ( B @ defined ) ) )
| ( B @ ( A @ defined ) )
| ~ $true
| ~ ( B @ ( A @ ( A @ product ) ) ) ),
inference(paramod_ordered,[status(thm)],[29250,84]) ).
thf(29434,plain,
! [B: $i,A: $i] :
( ( ( g @ ( d @ codomain @ defined ) )
!= ( A @ ( B @ defined ) ) )
| ( B @ ( A @ defined ) )
| ~ ( B @ ( A @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[29433]) ).
thf(29435,plain,
( ( d @ codomain @ ( g @ defined ) )
| ~ ( d @ codomain @ ( g @ ( g @ product ) ) ) ),
inference(pattern_uni,[status(thm)],[29434:[bind(A,$thf( g )),bind(B,$thf( d @ codomain ))]]) ).
thf(450,plain,
! [A: $i] :
( ( ( a @ codomain )
!= ( A @ codomain ) )
| ( A @ ( A @ ( a @ product ) ) )
| ( ( a @ domain )
!= a ) ),
inference(paramod_ordered,[status(thm)],[429,37]) ).
thf(451,plain,
( ( a @ ( a @ ( a @ product ) ) )
| ( ( a @ domain )
!= a ) ),
inference(pattern_uni,[status(thm)],[450:[bind(A,$thf( a ))]]) ).
thf(655,plain,
! [A: $i] :
( ( ( a @ ( a @ ( a @ product ) ) )
!= ( A @ ( a @ ( g @ product ) ) ) )
| ~ ( A @ ( a @ ( h @ product ) ) )
| ~ $true
| ( ( a @ domain )
!= a ) ),
inference(paramod_ordered,[status(thm)],[451,315]) ).
thf(656,plain,
! [A: $i] :
( ( ( a @ ( a @ ( a @ product ) ) )
!= ( A @ ( a @ ( g @ product ) ) ) )
| ~ ( A @ ( a @ ( h @ product ) ) )
| ( ( a @ domain )
!= a ) ),
inference(simp,[status(thm)],[655]) ).
thf(673,plain,
! [A: $i] :
( ( a != A )
| ( a != a )
| ( a != g )
| ~ ( A @ ( a @ ( h @ product ) ) )
| ( ( a @ domain )
!= a ) ),
inference(simp,[status(thm)],[656]) ).
thf(677,plain,
( ( a != g )
| ~ ( a @ ( a @ ( h @ product ) ) )
| ( ( a @ domain )
!= a ) ),
inference(simp,[status(thm)],[673]) ).
thf(1258,plain,
! [C: $i,B: $i,A: $i] :
( ( ( d @ ( c @ ( g @ product ) ) )
!= ( C @ ( B @ ( A @ product ) ) ) )
| ( B @ ( A @ defined ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[53,34]) ).
thf(1259,plain,
! [C: $i,B: $i,A: $i] :
( ( ( d @ ( c @ ( g @ product ) ) )
!= ( C @ ( B @ ( A @ product ) ) ) )
| ( B @ ( A @ defined ) ) ),
inference(simp,[status(thm)],[1258]) ).
thf(1260,plain,
c @ ( g @ defined ),
inference(pattern_uni,[status(thm)],[1259:[bind(A,$thf( g )),bind(B,$thf( c )),bind(C,$thf( d ))]]) ).
thf(2188,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( c @ ( b @ ( a @ product ) ) )
!= ( C @ ( B @ ( A @ product ) ) ) )
| ( A @ ( D @ defined ) )
| ~ ( C @ ( D @ defined ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[32,39]) ).
thf(2189,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( c @ ( b @ ( a @ product ) ) )
!= ( C @ ( B @ ( A @ product ) ) ) )
| ( A @ ( D @ defined ) )
| ~ ( C @ ( D @ defined ) ) ),
inference(simp,[status(thm)],[2188]) ).
thf(2190,plain,
! [A: $i] :
( ( a @ ( A @ defined ) )
| ~ ( c @ ( A @ defined ) ) ),
inference(pattern_uni,[status(thm)],[2189:[bind(A,$thf( a )),bind(B,$thf( b )),bind(C,$thf( c ))]]) ).
thf(2218,plain,
! [A: $i] :
( ( a @ ( A @ defined ) )
| ~ ( c @ ( A @ defined ) ) ),
inference(simp,[status(thm)],[2190]) ).
thf(8853,plain,
! [A: $i] :
( ( ( c @ ( g @ defined ) )
!= ( c @ ( A @ defined ) ) )
| ( a @ ( A @ defined ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1260,2218]) ).
thf(8854,plain,
! [A: $i] :
( ( ( c @ ( g @ defined ) )
!= ( c @ ( A @ defined ) ) )
| ( a @ ( A @ defined ) ) ),
inference(simp,[status(thm)],[8853]) ).
thf(8855,plain,
a @ ( g @ defined ),
inference(pattern_uni,[status(thm)],[8854:[bind(A,$thf( g ))]]) ).
thf(73,plain,
! [J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( E @ ( A @ defined ) )
!= ( I @ ( H @ defined ) ) )
| ( J @ ( F @ defined ) )
| ~ $true
| ~ ( J @ ( I @ ( G @ product ) ) )
| ~ ( H @ ( G @ ( F @ product ) ) )
| ~ ( D @ ( C @ defined ) )
| ~ ( E @ ( D @ ( B @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(paramod_ordered,[status(thm)],[26,26]) ).
thf(74,plain,
! [J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( E @ ( A @ defined ) )
!= ( I @ ( H @ defined ) ) )
| ( J @ ( F @ defined ) )
| ~ ( J @ ( I @ ( G @ product ) ) )
| ~ ( H @ ( G @ ( F @ product ) ) )
| ~ ( D @ ( C @ defined ) )
| ~ ( E @ ( D @ ( B @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[73]) ).
thf(75,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( H @ ( F @ defined ) )
| ~ ( H @ ( E @ ( G @ product ) ) )
| ~ ( A @ ( G @ ( F @ product ) ) )
| ~ ( D @ ( C @ defined ) )
| ~ ( E @ ( D @ ( B @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(pattern_uni,[status(thm)],[74:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( E )),bind(F,$thf( F )),bind(G,$thf( G )),bind(H,$thf( A )),bind(I,$thf( E ))]]) ).
thf(82,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( H @ ( F @ defined ) )
| ~ ( H @ ( E @ ( G @ product ) ) )
| ~ ( A @ ( G @ ( F @ product ) ) )
| ~ ( D @ ( C @ defined ) )
| ~ ( E @ ( D @ ( B @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[75]) ).
thf(164,plain,
! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ domain @ ( A @ defined ) )
!= ( E @ ( D @ defined ) ) )
| ( I @ ( G @ defined ) )
| ~ ( I @ ( F @ ( H @ product ) ) )
| ~ ( B @ ( H @ ( G @ product ) ) )
| ~ $true
| ~ ( F @ ( E @ ( C @ product ) ) )
| ~ ( D @ ( C @ ( B @ product ) ) ) ),
inference(paramod_ordered,[status(thm)],[23,82]) ).
thf(165,plain,
! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ domain @ ( A @ defined ) )
!= ( E @ ( D @ defined ) ) )
| ( I @ ( G @ defined ) )
| ~ ( I @ ( F @ ( H @ product ) ) )
| ~ ( B @ ( H @ ( G @ product ) ) )
| ~ ( F @ ( E @ ( C @ product ) ) )
| ~ ( D @ ( C @ ( B @ product ) ) ) ),
inference(simp,[status(thm)],[164]) ).
thf(166,plain,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( F @ ( D @ defined ) )
| ~ ( F @ ( C @ ( E @ product ) ) )
| ~ ( A @ ( E @ ( D @ product ) ) )
| ~ ( C @ ( G @ domain @ ( B @ product ) ) )
| ~ ( G @ ( B @ ( A @ product ) ) ) ),
inference(pattern_uni,[status(thm)],[165:[bind(A,$thf( J )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( J )),bind(E,$thf( J @ domain ))]]) ).
thf(170,plain,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( F @ ( D @ defined ) )
| ~ ( F @ ( C @ ( E @ product ) ) )
| ~ ( A @ ( E @ ( D @ product ) ) )
| ~ ( C @ ( G @ domain @ ( B @ product ) ) )
| ~ ( G @ ( B @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[166]) ).
thf(64,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( c @ ( b @ ( a @ product ) ) )
!= ( E @ ( D @ ( B @ product ) ) ) )
| ( E @ ( A @ defined ) )
| ~ ( D @ ( C @ defined ) )
| ~ $true
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(paramod_ordered,[status(thm)],[32,26]) ).
thf(65,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( c @ ( b @ ( a @ product ) ) )
!= ( E @ ( D @ ( B @ product ) ) ) )
| ( E @ ( A @ defined ) )
| ~ ( D @ ( C @ defined ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[64]) ).
thf(66,plain,
! [B: $i,A: $i] :
( ( c @ ( A @ defined ) )
| ~ ( b @ ( B @ defined ) )
| ~ ( B @ ( a @ ( A @ product ) ) ) ),
inference(pattern_uni,[status(thm)],[65:[bind(A,$thf( A )),bind(B,$thf( a )),bind(C,$thf( C )),bind(D,$thf( b )),bind(E,$thf( c ))]]) ).
thf(78,plain,
! [B: $i,A: $i] :
( ( c @ ( A @ defined ) )
| ~ ( b @ ( B @ defined ) )
| ~ ( B @ ( a @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[66]) ).
thf(9684,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( A @ codomain @ product ) ) )
!= ( C @ ( a @ ( B @ product ) ) ) )
| ( c @ ( B @ defined ) )
| ~ ( b @ ( C @ defined ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[37,78]) ).
thf(9685,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( A @ codomain @ product ) ) )
!= ( C @ ( a @ ( B @ product ) ) ) )
| ( c @ ( B @ defined ) )
| ~ ( b @ ( C @ defined ) ) ),
inference(simp,[status(thm)],[9684]) ).
thf(9686,plain,
( ( c @ ( a @ codomain @ defined ) )
| ~ ( b @ ( a @ defined ) ) ),
inference(pattern_uni,[status(thm)],[9685:[bind(A,$thf( a )),bind(B,$thf( a @ codomain )),bind(C,$thf( a ))]]) ).
thf(11251,plain,
( ( c @ ( a @ codomain @ defined ) )
| ~ $true ),
inference(rewrite,[status(thm)],[9686,1281]) ).
thf(11252,plain,
c @ ( a @ codomain @ defined ),
inference(simp,[status(thm)],[11251]) ).
thf(11298,plain,
! [B: $i,A: $i] :
( ( ( c @ ( a @ codomain @ defined ) )
!= ( B @ ( A @ defined ) ) )
| ( B @ ( A @ compose ) @ ( B @ ( A @ product ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[11252,31]) ).
thf(11299,plain,
! [B: $i,A: $i] :
( ( ( c @ ( a @ codomain @ defined ) )
!= ( B @ ( A @ defined ) ) )
| ( B @ ( A @ compose ) @ ( B @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[11298]) ).
thf(11300,plain,
c @ ( a @ codomain @ compose ) @ ( c @ ( a @ codomain @ product ) ),
inference(pattern_uni,[status(thm)],[11299:[bind(A,$thf( a @ codomain )),bind(B,$thf( c ))]]) ).
thf(11439,plain,
( ( ( a @ codomain )
!= ( a @ codomain ) )
| ( c @ ( a @ codomain @ compose ) @ ( c @ ( a @ product ) ) )
| ( ( a @ domain )
!= a ) ),
inference(paramod_ordered,[status(thm)],[429,11300]) ).
thf(11440,plain,
( ( c @ ( a @ codomain @ compose ) @ ( c @ ( a @ product ) ) )
| ( ( a @ domain )
!= a ) ),
inference(pattern_uni,[status(thm)],[11439:[]]) ).
thf(55,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( d @ ( c @ ( g @ product ) ) )
!= ( C @ ( B @ ( A @ product ) ) ) )
| ( E @ ( A @ defined ) )
| ~ ( D @ ( C @ defined ) )
| ~ ( E @ ( D @ ( B @ product ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[53,26]) ).
thf(56,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( d @ ( c @ ( g @ product ) ) )
!= ( C @ ( B @ ( A @ product ) ) ) )
| ( E @ ( A @ defined ) )
| ~ ( D @ ( C @ defined ) )
| ~ ( E @ ( D @ ( B @ product ) ) ) ),
inference(simp,[status(thm)],[55]) ).
thf(57,plain,
! [B: $i,A: $i] :
( ( B @ ( g @ defined ) )
| ~ ( A @ ( d @ defined ) )
| ~ ( B @ ( A @ ( c @ product ) ) ) ),
inference(pattern_uni,[status(thm)],[56:[bind(A,$thf( g )),bind(B,$thf( c )),bind(C,$thf( d ))]]) ).
thf(81,plain,
! [B: $i,A: $i] :
( ( B @ ( g @ defined ) )
| ~ ( A @ ( d @ defined ) )
| ~ ( B @ ( A @ ( c @ product ) ) ) ),
inference(simp,[status(thm)],[57]) ).
thf(11974,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ domain @ ( A @ compose ) @ ( A @ domain @ ( A @ product ) ) )
!= ( C @ ( B @ ( c @ product ) ) ) )
| ( C @ ( g @ defined ) )
| ~ ( B @ ( d @ defined ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[762,81]) ).
thf(11975,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ domain @ ( A @ compose ) @ ( A @ domain @ ( A @ product ) ) )
!= ( C @ ( B @ ( c @ product ) ) ) )
| ( C @ ( g @ defined ) )
| ~ ( B @ ( d @ defined ) ) ),
inference(simp,[status(thm)],[11974]) ).
thf(11976,plain,
( ( c @ domain @ ( c @ compose ) @ ( g @ defined ) )
| ~ ( c @ domain @ ( d @ defined ) ) ),
inference(pattern_uni,[status(thm)],[11975:[bind(A,$thf( c )),bind(B,$thf( c @ domain )),bind(C,$thf( c @ domain @ ( c @ compose ) ))]]) ).
thf(23823,plain,
! [A: $i] :
( ( ( A @ ( A @ codomain @ defined ) )
!= ( c @ domain @ ( d @ defined ) ) )
| ( c @ domain @ ( c @ compose ) @ ( g @ defined ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[24,11976]) ).
thf(23824,plain,
! [A: $i] :
( ( ( A @ ( A @ codomain @ defined ) )
!= ( c @ domain @ ( d @ defined ) ) )
| ( c @ domain @ ( c @ compose ) @ ( g @ defined ) ) ),
inference(simp,[status(thm)],[23823]) ).
thf(24021,plain,
! [A: $i] :
( ( A
!= ( c @ domain ) )
| ( ( A @ codomain )
!= d )
| ( c @ domain @ ( c @ compose ) @ ( g @ defined ) ) ),
inference(simp,[status(thm)],[23824]) ).
thf(24056,plain,
( ( ( c @ domain @ codomain )
!= d )
| ( c @ domain @ ( c @ compose ) @ ( g @ defined ) ) ),
inference(simp,[status(thm)],[24021]) ).
thf(727,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ compose ) @ ( B @ ( A @ product ) ) )
!= ( C @ ( a @ ( g @ product ) ) ) )
| ~ ( C @ ( a @ ( h @ product ) ) )
| ~ $true
| ~ ( B @ ( A @ defined ) ) ),
inference(paramod_ordered,[status(thm)],[31,315]) ).
thf(728,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ compose ) @ ( B @ ( A @ product ) ) )
!= ( C @ ( a @ ( g @ product ) ) ) )
| ~ ( C @ ( a @ ( h @ product ) ) )
| ~ ( B @ ( A @ defined ) ) ),
inference(simp,[status(thm)],[727]) ).
thf(729,plain,
( ~ ( a @ ( g @ compose ) @ ( a @ ( h @ product ) ) )
| ~ ( a @ ( g @ defined ) ) ),
inference(pattern_uni,[status(thm)],[728:[bind(A,$thf( g )),bind(B,$thf( a )),bind(C,$thf( a @ ( g @ compose ) ))]]) ).
thf(8905,plain,
( ~ ( a @ ( g @ compose ) @ ( a @ ( h @ product ) ) )
| ~ $true ),
inference(rewrite,[status(thm)],[729,8855]) ).
thf(8906,plain,
~ ( a @ ( g @ compose ) @ ( a @ ( h @ product ) ) ),
inference(simp,[status(thm)],[8905]) ).
thf(9178,plain,
( ( ( a @ ( a @ ( a @ product ) ) )
!= ( a @ ( g @ compose ) @ ( a @ ( h @ product ) ) ) )
| ~ $true
| ( ( a @ domain )
!= a ) ),
inference(paramod_ordered,[status(thm)],[451,8906]) ).
thf(9179,plain,
( ( ( a @ ( a @ ( a @ product ) ) )
!= ( a @ ( g @ compose ) @ ( a @ ( h @ product ) ) ) )
| ( ( a @ domain )
!= a ) ),
inference(simp,[status(thm)],[9178]) ).
thf(9222,plain,
( ( ( a @ ( g @ compose ) )
!= a )
| ( a != a )
| ( a != h )
| ( ( a @ domain )
!= a ) ),
inference(simp,[status(thm)],[9179]) ).
thf(9233,plain,
( ( ( a @ ( g @ compose ) )
!= a )
| ( a != h )
| ( ( a @ domain )
!= a ) ),
inference(simp,[status(thm)],[9222]) ).
thf(13777,plain,
! [B: $i,A: $i] :
( ( ( b @ ( a @ defined ) )
!= ( A @ ( B @ defined ) ) )
| ( B @ ( A @ defined ) )
| ~ $true
| ~ ( B @ ( A @ ( A @ product ) ) ) ),
inference(paramod_ordered,[status(thm)],[1281,84]) ).
thf(13778,plain,
! [B: $i,A: $i] :
( ( ( b @ ( a @ defined ) )
!= ( A @ ( B @ defined ) ) )
| ( B @ ( A @ defined ) )
| ~ ( B @ ( A @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[13777]) ).
thf(13779,plain,
( ( a @ ( b @ defined ) )
| ~ ( a @ ( b @ ( b @ product ) ) ) ),
inference(pattern_uni,[status(thm)],[13778:[bind(A,$thf( b )),bind(B,$thf( a ))]]) ).
thf(43890,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ ( A @ codomain @ product ) ) )
!= ( B @ ( a @ ( c @ product ) ) ) )
| ~ ( B @ ( a @ ( a @ product ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[37,697]) ).
thf(43891,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ ( A @ codomain @ product ) ) )
!= ( B @ ( a @ ( c @ product ) ) ) )
| ~ ( B @ ( a @ ( a @ product ) ) ) ),
inference(simp,[status(thm)],[43890]) ).
thf(44115,plain,
! [B: $i,A: $i] :
( ( A != B )
| ( A != a )
| ( ( A @ codomain )
!= c )
| ~ ( B @ ( a @ ( a @ product ) ) ) ),
inference(simp,[status(thm)],[43891]) ).
thf(44202,plain,
( ( ( a @ codomain )
!= c )
| ~ ( a @ ( a @ ( a @ product ) ) ) ),
inference(simp,[status(thm)],[44115]) ).
thf(47436,plain,
! [A: $i] :
( ( ( A @ ( A @ ( A @ codomain @ product ) ) )
!= ( a @ ( a @ ( a @ product ) ) ) )
| ( ( a @ codomain )
!= c )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[37,44202]) ).
thf(47437,plain,
! [A: $i] :
( ( ( A @ ( A @ ( A @ codomain @ product ) ) )
!= ( a @ ( a @ ( a @ product ) ) ) )
| ( ( a @ codomain )
!= c ) ),
inference(simp,[status(thm)],[47436]) ).
thf(47567,plain,
! [A: $i] :
( ( A != a )
| ( A != a )
| ( ( A @ codomain )
!= a )
| ( ( a @ codomain )
!= c ) ),
inference(simp,[status(thm)],[47437]) ).
thf(47622,plain,
( ( ( a @ codomain )
!= a )
| ( ( a @ codomain )
!= c ) ),
inference(simp,[status(thm)],[47567]) ).
thf(135,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ $true
| ( ( H @ ( E @ ( G @ product ) ) )
!= ( E @ ( D @ ( B @ product ) ) ) )
| ( H @ ( F @ defined ) )
| ~ ( A @ ( G @ ( F @ product ) ) )
| ~ ( D @ ( C @ defined ) )
| ~ ( E @ ( D @ ( B @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(eqfactor_ordered,[status(thm)],[82]) ).
thf(141,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( C @ defined ) )
| ~ ( A @ ( D @ ( C @ product ) ) )
| ~ ( E @ ( B @ defined ) )
| ~ ( E @ ( E @ ( D @ product ) ) )
| ~ ( B @ ( D @ ( A @ product ) ) ) ),
inference(pattern_uni,[status(thm)],[135:[bind(A,$thf( A )),bind(B,$thf( G )),bind(C,$thf( C )),bind(D,$thf( H )),bind(E,$thf( H ))]]) ).
thf(153,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( C @ defined ) )
| ~ ( A @ ( D @ ( C @ product ) ) )
| ~ ( E @ ( B @ defined ) )
| ~ ( E @ ( E @ ( D @ product ) ) )
| ~ ( B @ ( D @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[141]) ).
thf(29236,plain,
! [A: $i] :
( ( ( a @ ( g @ defined ) )
!= ( d @ ( A @ defined ) ) )
| ( g @ ( A @ defined ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[8855,2221]) ).
thf(29237,plain,
! [A: $i] :
( ( ( a @ ( g @ defined ) )
!= ( d @ ( A @ defined ) ) )
| ( g @ ( A @ defined ) ) ),
inference(simp,[status(thm)],[29236]) ).
thf(29336,plain,
! [A: $i] :
( ( d != a )
| ( g != A )
| ( g @ ( A @ defined ) ) ),
inference(simp,[status(thm)],[29237]) ).
thf(29371,plain,
( ( d != a )
| ( g @ ( g @ defined ) ) ),
inference(simp,[status(thm)],[29336]) ).
thf(12,axiom,
! [C: $i,B: $i,A: $i] :
( ( A = C )
| ~ ( B @ ( b @ ( C @ product ) ) )
| ~ ( B @ ( b @ ( A @ product ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cancellation_for_product2) ).
thf(40,plain,
! [C: $i,B: $i,A: $i] :
( ( A = C )
| ~ ( B @ ( b @ ( C @ product ) ) )
| ~ ( B @ ( b @ ( A @ product ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[12]) ).
thf(41,plain,
! [C: $i,B: $i,A: $i] :
( ( A = C )
| ~ ( B @ ( b @ ( C @ product ) ) )
| ~ ( B @ ( b @ ( A @ product ) ) ) ),
inference(cnf,[status(esa)],[40]) ).
thf(42,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( B @ ( b @ ( C @ product ) ) )
| ~ ( B @ ( b @ ( A @ product ) ) )
| ( A = C ) ),
inference(lifteq,[status(thm)],[41]) ).
thf(29442,plain,
! [A: $i] :
( ( A
!= ( d @ codomain ) )
| ( g @ ( a @ codomain @ defined ) )
| ~ ( a @ ( a @ ( A @ product ) ) ) ),
inference(paramod_ordered,[status(thm)],[297,29250]) ).
thf(29443,plain,
( ( g @ ( a @ codomain @ defined ) )
| ~ ( a @ ( a @ ( d @ codomain @ product ) ) ) ),
inference(pattern_uni,[status(thm)],[29442:[bind(A,$thf( d @ codomain ))]]) ).
thf(38205,plain,
! [A: $i] :
( ( ( A @ ( A @ ( A @ codomain @ product ) ) )
!= ( a @ ( a @ ( d @ codomain @ product ) ) ) )
| ( g @ ( a @ codomain @ defined ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[37,29443]) ).
thf(38206,plain,
! [A: $i] :
( ( ( A @ ( A @ ( A @ codomain @ product ) ) )
!= ( a @ ( a @ ( d @ codomain @ product ) ) ) )
| ( g @ ( a @ codomain @ defined ) ) ),
inference(simp,[status(thm)],[38205]) ).
thf(38343,plain,
! [A: $i] :
( ( A != a )
| ( A != a )
| ( ( A @ codomain )
!= ( d @ codomain ) )
| ( g @ ( a @ codomain @ defined ) ) ),
inference(simp,[status(thm)],[38206]) ).
thf(38373,plain,
( ( ( d @ codomain )
!= ( a @ codomain ) )
| ( g @ ( a @ codomain @ defined ) ) ),
inference(simp,[status(thm)],[38343]) ).
thf(38486,plain,
! [B: $i,A: $i] :
( ( ( g @ ( a @ codomain @ defined ) )
!= ( B @ ( A @ defined ) ) )
| ( B @ ( A @ compose ) @ ( B @ ( A @ product ) ) )
| ~ $true
| ( ( d @ codomain )
!= ( a @ codomain ) ) ),
inference(paramod_ordered,[status(thm)],[38373,31]) ).
thf(38487,plain,
! [B: $i,A: $i] :
( ( ( g @ ( a @ codomain @ defined ) )
!= ( B @ ( A @ defined ) ) )
| ( B @ ( A @ compose ) @ ( B @ ( A @ product ) ) )
| ( ( d @ codomain )
!= ( a @ codomain ) ) ),
inference(simp,[status(thm)],[38486]) ).
thf(38488,plain,
( ( g @ ( a @ codomain @ compose ) @ ( g @ ( a @ codomain @ product ) ) )
| ( ( d @ codomain )
!= ( a @ codomain ) ) ),
inference(pattern_uni,[status(thm)],[38487:[bind(A,$thf( a @ codomain )),bind(B,$thf( g ))]]) ).
thf(47474,plain,
! [A: $i] :
( ( ( a @ codomain )
!= ( a @ codomain ) )
| ( A != c )
| ~ ( a @ ( a @ ( a @ product ) ) )
| ~ ( a @ ( a @ ( A @ product ) ) ) ),
inference(paramod_ordered,[status(thm)],[297,44202]) ).
thf(47475,plain,
! [A: $i] :
( ( A != c )
| ~ ( a @ ( a @ ( a @ product ) ) )
| ~ ( a @ ( a @ ( A @ product ) ) ) ),
inference(pattern_uni,[status(thm)],[47474:[]]) ).
thf(47650,plain,
( ~ ( a @ ( a @ ( a @ product ) ) )
| ~ ( a @ ( a @ ( c @ product ) ) ) ),
inference(simp,[status(thm)],[47475]) ).
thf(733,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ codomain @ defined ) )
!= ( C @ ( B @ defined ) ) )
| ( C @ ( B @ compose ) @ ( C @ ( B @ product ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[24,31]) ).
thf(734,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ codomain @ defined ) )
!= ( C @ ( B @ defined ) ) )
| ( C @ ( B @ compose ) @ ( C @ ( B @ product ) ) ) ),
inference(simp,[status(thm)],[733]) ).
thf(735,plain,
! [A: $i] : ( A @ ( A @ codomain @ compose ) @ ( A @ ( A @ codomain @ product ) ) ),
inference(pattern_uni,[status(thm)],[734:[bind(A,$thf( D )),bind(B,$thf( D @ codomain )),bind(C,$thf( D ))]]) ).
thf(766,plain,
! [A: $i] : ( A @ ( A @ codomain @ compose ) @ ( A @ ( A @ codomain @ product ) ) ),
inference(simp,[status(thm)],[735]) ).
thf(884,plain,
! [A: $i] :
( ( ( a @ codomain )
!= ( A @ codomain ) )
| ( A @ ( A @ codomain @ compose ) @ ( A @ ( a @ product ) ) )
| ( ( a @ domain )
!= a ) ),
inference(paramod_ordered,[status(thm)],[429,766]) ).
thf(885,plain,
( ( a @ ( a @ codomain @ compose ) @ ( a @ ( a @ product ) ) )
| ( ( a @ domain )
!= a ) ),
inference(pattern_uni,[status(thm)],[884:[bind(A,$thf( a ))]]) ).
thf(533,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ ( A @ codomain @ product ) ) )
!= ( B @ ( a @ ( h @ product ) ) ) )
| ~ $true
| ~ ( B @ ( a @ ( g @ product ) ) ) ),
inference(paramod_ordered,[status(thm)],[37,315]) ).
thf(534,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ ( A @ codomain @ product ) ) )
!= ( B @ ( a @ ( h @ product ) ) ) )
| ~ ( B @ ( a @ ( g @ product ) ) ) ),
inference(simp,[status(thm)],[533]) ).
thf(546,plain,
! [B: $i,A: $i] :
( ( A != B )
| ( A != a )
| ( ( A @ codomain )
!= h )
| ~ ( B @ ( a @ ( g @ product ) ) ) ),
inference(simp,[status(thm)],[534]) ).
thf(556,plain,
( ( ( a @ codomain )
!= h )
| ~ ( a @ ( a @ ( g @ product ) ) ) ),
inference(simp,[status(thm)],[546]) ).
thf(1018,plain,
! [A: $i] :
( ( ( A @ ( A @ ( A @ codomain @ product ) ) )
!= ( a @ ( a @ ( g @ product ) ) ) )
| ( ( a @ codomain )
!= h )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[37,556]) ).
thf(1019,plain,
! [A: $i] :
( ( ( A @ ( A @ ( A @ codomain @ product ) ) )
!= ( a @ ( a @ ( g @ product ) ) ) )
| ( ( a @ codomain )
!= h ) ),
inference(simp,[status(thm)],[1018]) ).
thf(1038,plain,
! [A: $i] :
( ( A != a )
| ( A != a )
| ( ( A @ codomain )
!= g )
| ( ( a @ codomain )
!= h ) ),
inference(simp,[status(thm)],[1019]) ).
thf(1046,plain,
( ( ( a @ codomain )
!= g )
| ( ( a @ codomain )
!= h ) ),
inference(simp,[status(thm)],[1038]) ).
thf(58,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( d @ ( c @ ( g @ product ) ) )
!= ( E @ ( D @ ( B @ product ) ) ) )
| ( E @ ( A @ defined ) )
| ~ ( D @ ( C @ defined ) )
| ~ $true
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(paramod_ordered,[status(thm)],[53,26]) ).
thf(59,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( d @ ( c @ ( g @ product ) ) )
!= ( E @ ( D @ ( B @ product ) ) ) )
| ( E @ ( A @ defined ) )
| ~ ( D @ ( C @ defined ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[58]) ).
thf(60,plain,
! [B: $i,A: $i] :
( ( d @ ( A @ defined ) )
| ~ ( c @ ( B @ defined ) )
| ~ ( B @ ( g @ ( A @ product ) ) ) ),
inference(pattern_uni,[status(thm)],[59:[bind(A,$thf( A )),bind(B,$thf( g )),bind(C,$thf( C )),bind(D,$thf( c )),bind(E,$thf( d ))]]) ).
thf(83,plain,
! [B: $i,A: $i] :
( ( d @ ( A @ defined ) )
| ~ ( c @ ( B @ defined ) )
| ~ ( B @ ( g @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[60]) ).
thf(12863,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( A @ codomain @ product ) ) )
!= ( C @ ( g @ ( B @ product ) ) ) )
| ( d @ ( B @ defined ) )
| ~ ( c @ ( C @ defined ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[37,83]) ).
thf(12864,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( A @ codomain @ product ) ) )
!= ( C @ ( g @ ( B @ product ) ) ) )
| ( d @ ( B @ defined ) )
| ~ ( c @ ( C @ defined ) ) ),
inference(simp,[status(thm)],[12863]) ).
thf(12865,plain,
( ( d @ ( g @ codomain @ defined ) )
| ~ ( c @ ( g @ defined ) ) ),
inference(pattern_uni,[status(thm)],[12864:[bind(A,$thf( g )),bind(B,$thf( g @ codomain )),bind(C,$thf( g ))]]) ).
thf(13030,plain,
( ( d @ ( g @ codomain @ defined ) )
| ~ $true ),
inference(rewrite,[status(thm)],[12865,1260]) ).
thf(13031,plain,
d @ ( g @ codomain @ defined ),
inference(simp,[status(thm)],[13030]) ).
thf(13798,plain,
! [B: $i,A: $i] :
( ( ( d @ ( g @ codomain @ defined ) )
!= ( A @ ( B @ defined ) ) )
| ( B @ ( A @ defined ) )
| ~ $true
| ~ ( B @ ( A @ ( A @ product ) ) ) ),
inference(paramod_ordered,[status(thm)],[13031,84]) ).
thf(13799,plain,
! [B: $i,A: $i] :
( ( ( d @ ( g @ codomain @ defined ) )
!= ( A @ ( B @ defined ) ) )
| ( B @ ( A @ defined ) )
| ~ ( B @ ( A @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[13798]) ).
thf(13800,plain,
( ( g @ codomain @ ( d @ defined ) )
| ~ ( g @ codomain @ ( d @ ( d @ product ) ) ) ),
inference(pattern_uni,[status(thm)],[13799:[bind(A,$thf( d )),bind(B,$thf( g @ codomain ))]]) ).
thf(8874,plain,
! [A: $i] :
( ( ( c @ ( h @ defined ) )
!= ( c @ ( A @ defined ) ) )
| ( a @ ( A @ defined ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1266,2218]) ).
thf(8875,plain,
! [A: $i] :
( ( ( c @ ( h @ defined ) )
!= ( c @ ( A @ defined ) ) )
| ( a @ ( A @ defined ) ) ),
inference(simp,[status(thm)],[8874]) ).
thf(8876,plain,
a @ ( h @ defined ),
inference(pattern_uni,[status(thm)],[8875:[bind(A,$thf( h ))]]) ).
thf(8994,plain,
! [B: $i,A: $i] :
( ( ( a @ ( h @ defined ) )
!= ( B @ ( A @ defined ) ) )
| ( B @ ( A @ compose ) @ ( B @ ( A @ product ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[8876,31]) ).
thf(8995,plain,
! [B: $i,A: $i] :
( ( ( a @ ( h @ defined ) )
!= ( B @ ( A @ defined ) ) )
| ( B @ ( A @ compose ) @ ( B @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[8994]) ).
thf(8996,plain,
a @ ( h @ compose ) @ ( a @ ( h @ product ) ),
inference(pattern_uni,[status(thm)],[8995:[bind(A,$thf( h )),bind(B,$thf( a ))]]) ).
thf(70,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( d @ ( c @ ( h @ product ) ) )
!= ( E @ ( D @ ( B @ product ) ) ) )
| ( E @ ( A @ defined ) )
| ~ ( D @ ( C @ defined ) )
| ~ $true
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(paramod_ordered,[status(thm)],[54,26]) ).
thf(71,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( d @ ( c @ ( h @ product ) ) )
!= ( E @ ( D @ ( B @ product ) ) ) )
| ( E @ ( A @ defined ) )
| ~ ( D @ ( C @ defined ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[70]) ).
thf(72,plain,
! [B: $i,A: $i] :
( ( d @ ( A @ defined ) )
| ~ ( c @ ( B @ defined ) )
| ~ ( B @ ( h @ ( A @ product ) ) ) ),
inference(pattern_uni,[status(thm)],[71:[bind(A,$thf( A )),bind(B,$thf( h )),bind(C,$thf( C )),bind(D,$thf( c )),bind(E,$thf( d ))]]) ).
thf(80,plain,
! [B: $i,A: $i] :
( ( d @ ( A @ defined ) )
| ~ ( c @ ( B @ defined ) )
| ~ ( B @ ( h @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[72]) ).
thf(11106,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( A @ codomain @ product ) ) )
!= ( C @ ( h @ ( B @ product ) ) ) )
| ( d @ ( B @ defined ) )
| ~ ( c @ ( C @ defined ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[37,80]) ).
thf(11107,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( A @ codomain @ product ) ) )
!= ( C @ ( h @ ( B @ product ) ) ) )
| ( d @ ( B @ defined ) )
| ~ ( c @ ( C @ defined ) ) ),
inference(simp,[status(thm)],[11106]) ).
thf(11108,plain,
( ( d @ ( h @ codomain @ defined ) )
| ~ ( c @ ( h @ defined ) ) ),
inference(pattern_uni,[status(thm)],[11107:[bind(A,$thf( h )),bind(B,$thf( h @ codomain )),bind(C,$thf( h ))]]) ).
thf(12150,plain,
( ( d @ ( h @ codomain @ defined ) )
| ~ $true ),
inference(rewrite,[status(thm)],[11108,1266]) ).
thf(12151,plain,
d @ ( h @ codomain @ defined ),
inference(simp,[status(thm)],[12150]) ).
thf(29264,plain,
! [A: $i] :
( ( ( d @ ( h @ codomain @ defined ) )
!= ( d @ ( A @ defined ) ) )
| ( g @ ( A @ defined ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[12151,2221]) ).
thf(29265,plain,
! [A: $i] :
( ( ( d @ ( h @ codomain @ defined ) )
!= ( d @ ( A @ defined ) ) )
| ( g @ ( A @ defined ) ) ),
inference(simp,[status(thm)],[29264]) ).
thf(29266,plain,
g @ ( h @ codomain @ defined ),
inference(pattern_uni,[status(thm)],[29265:[bind(A,$thf( h @ codomain ))]]) ).
thf(29629,plain,
! [B: $i,A: $i] :
( ( ( g @ ( h @ codomain @ defined ) )
!= ( B @ ( A @ defined ) ) )
| ( B @ ( A @ compose ) @ ( B @ ( A @ product ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[29266,31]) ).
thf(29630,plain,
! [B: $i,A: $i] :
( ( ( g @ ( h @ codomain @ defined ) )
!= ( B @ ( A @ defined ) ) )
| ( B @ ( A @ compose ) @ ( B @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[29629]) ).
thf(29631,plain,
g @ ( h @ codomain @ compose ) @ ( g @ ( h @ codomain @ product ) ),
inference(pattern_uni,[status(thm)],[29630:[bind(A,$thf( h @ codomain )),bind(B,$thf( g ))]]) ).
thf(8866,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ codomain @ defined ) )
!= ( c @ ( B @ defined ) ) )
| ( a @ ( B @ defined ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[24,2218]) ).
thf(8867,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ codomain @ defined ) )
!= ( c @ ( B @ defined ) ) )
| ( a @ ( B @ defined ) ) ),
inference(simp,[status(thm)],[8866]) ).
thf(8868,plain,
a @ ( c @ codomain @ defined ),
inference(pattern_uni,[status(thm)],[8867:[bind(A,$thf( c )),bind(B,$thf( c @ codomain ))]]) ).
thf(9063,plain,
! [B: $i,A: $i] :
( ( ( a @ ( c @ codomain @ defined ) )
!= ( B @ ( A @ defined ) ) )
| ( B @ ( A @ compose ) @ ( B @ ( A @ product ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[8868,31]) ).
thf(9064,plain,
! [B: $i,A: $i] :
( ( ( a @ ( c @ codomain @ defined ) )
!= ( B @ ( A @ defined ) ) )
| ( B @ ( A @ compose ) @ ( B @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[9063]) ).
thf(9065,plain,
a @ ( c @ codomain @ compose ) @ ( a @ ( c @ codomain @ product ) ),
inference(pattern_uni,[status(thm)],[9064:[bind(A,$thf( c @ codomain )),bind(B,$thf( a ))]]) ).
thf(730,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ compose ) @ ( B @ ( A @ product ) ) )
!= ( C @ ( a @ ( h @ product ) ) ) )
| ~ $true
| ~ ( C @ ( a @ ( g @ product ) ) )
| ~ ( B @ ( A @ defined ) ) ),
inference(paramod_ordered,[status(thm)],[31,315]) ).
thf(731,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ compose ) @ ( B @ ( A @ product ) ) )
!= ( C @ ( a @ ( h @ product ) ) ) )
| ~ ( C @ ( a @ ( g @ product ) ) )
| ~ ( B @ ( A @ defined ) ) ),
inference(simp,[status(thm)],[730]) ).
thf(732,plain,
( ~ ( a @ ( h @ compose ) @ ( a @ ( g @ product ) ) )
| ~ ( a @ ( h @ defined ) ) ),
inference(pattern_uni,[status(thm)],[731:[bind(A,$thf( h )),bind(B,$thf( a )),bind(C,$thf( a @ ( h @ compose ) ))]]) ).
thf(8968,plain,
( ~ ( a @ ( h @ compose ) @ ( a @ ( g @ product ) ) )
| ~ $true ),
inference(rewrite,[status(thm)],[732,8876]) ).
thf(8969,plain,
~ ( a @ ( h @ compose ) @ ( a @ ( g @ product ) ) ),
inference(simp,[status(thm)],[8968]) ).
thf(10271,plain,
( ( ( a @ ( c @ codomain @ compose ) @ ( a @ ( c @ codomain @ product ) ) )
!= ( a @ ( h @ compose ) @ ( a @ ( g @ product ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[9065,8969]) ).
thf(10272,plain,
( ( a @ ( c @ codomain @ compose ) @ ( a @ ( c @ codomain @ product ) ) )
!= ( a @ ( h @ compose ) @ ( a @ ( g @ product ) ) ) ),
inference(simp,[status(thm)],[10271]) ).
thf(10321,plain,
( ( ( a @ ( c @ codomain @ compose ) )
!= ( a @ ( h @ compose ) ) )
| ( a != a )
| ( ( c @ codomain )
!= g ) ),
inference(simp,[status(thm)],[10272]) ).
thf(10382,plain,
( ( ( a @ ( c @ codomain @ compose ) )
!= ( a @ ( h @ compose ) ) )
| ( ( c @ codomain )
!= g ) ),
inference(simp,[status(thm)],[10321]) ).
thf(43894,plain,
! [A: $i] :
( ( ( A @ ( a @ ( c @ product ) ) )
!= ( a @ ( h @ compose ) @ ( a @ ( h @ product ) ) ) )
| ~ ( A @ ( a @ ( a @ product ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[8996,697]) ).
thf(43895,plain,
! [A: $i] :
( ( ( A @ ( a @ ( c @ product ) ) )
!= ( a @ ( h @ compose ) @ ( a @ ( h @ product ) ) ) )
| ~ ( A @ ( a @ ( a @ product ) ) ) ),
inference(simp,[status(thm)],[43894]) ).
thf(44097,plain,
! [A: $i] :
( ( A
!= ( a @ ( h @ compose ) ) )
| ( a != a )
| ( c != h )
| ~ ( A @ ( a @ ( a @ product ) ) ) ),
inference(simp,[status(thm)],[43895]) ).
thf(44184,plain,
( ( c != h )
| ~ ( a @ ( h @ compose ) @ ( a @ ( a @ product ) ) ) ),
inference(simp,[status(thm)],[44097]) ).
thf(49716,plain,
( ( ( a @ ( h @ compose ) @ ( a @ ( a @ product ) ) )
!= ( a @ ( h @ compose ) @ ( a @ ( h @ product ) ) ) )
| ( c != h )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[8996,44184]) ).
thf(49717,plain,
( ( ( a @ ( h @ compose ) @ ( a @ ( a @ product ) ) )
!= ( a @ ( h @ compose ) @ ( a @ ( h @ product ) ) ) )
| ( c != h ) ),
inference(simp,[status(thm)],[49716]) ).
thf(49884,plain,
( ( ( a @ ( h @ compose ) )
!= ( a @ ( h @ compose ) ) )
| ( a != a )
| ( a != h )
| ( c != h ) ),
inference(simp,[status(thm)],[49717]) ).
thf(49934,plain,
( ( a != h )
| ( c != h ) ),
inference(simp,[status(thm)],[49884]) ).
thf(31699,plain,
! [B: $i,A: $i] :
( ( ( g @ ( a @ defined ) )
!= ( B @ ( A @ defined ) ) )
| ( B @ ( A @ compose ) @ ( B @ ( A @ product ) ) )
| ~ $true
| ( d != b ) ),
inference(paramod_ordered,[status(thm)],[29375,31]) ).
thf(31700,plain,
! [B: $i,A: $i] :
( ( ( g @ ( a @ defined ) )
!= ( B @ ( A @ defined ) ) )
| ( B @ ( A @ compose ) @ ( B @ ( A @ product ) ) )
| ( d != b ) ),
inference(simp,[status(thm)],[31699]) ).
thf(31701,plain,
( ( g @ ( a @ compose ) @ ( g @ ( a @ product ) ) )
| ( d != b ) ),
inference(pattern_uni,[status(thm)],[31700:[bind(A,$thf( a )),bind(B,$thf( g ))]]) ).
thf(116,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( d @ ( c @ ( h @ product ) ) )
!= ( A @ ( G @ ( F @ product ) ) ) )
| ( H @ ( F @ defined ) )
| ~ ( H @ ( E @ ( G @ product ) ) )
| ~ $true
| ~ ( D @ ( C @ defined ) )
| ~ ( E @ ( D @ ( B @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(paramod_ordered,[status(thm)],[54,82]) ).
thf(117,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( d @ ( c @ ( h @ product ) ) )
!= ( A @ ( G @ ( F @ product ) ) ) )
| ( H @ ( F @ defined ) )
| ~ ( H @ ( E @ ( G @ product ) ) )
| ~ ( D @ ( C @ defined ) )
| ~ ( E @ ( D @ ( B @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[116]) ).
thf(118,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( h @ defined ) )
| ~ ( E @ ( D @ ( c @ product ) ) )
| ~ ( C @ ( B @ defined ) )
| ~ ( D @ ( C @ ( A @ product ) ) )
| ~ ( B @ ( A @ ( d @ product ) ) ) ),
inference(pattern_uni,[status(thm)],[117:[bind(A,$thf( d )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( E )),bind(F,$thf( h )),bind(G,$thf( c ))]]) ).
thf(157,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( h @ defined ) )
| ~ ( E @ ( D @ ( c @ product ) ) )
| ~ ( C @ ( B @ defined ) )
| ~ ( D @ ( C @ ( A @ product ) ) )
| ~ ( B @ ( A @ ( d @ product ) ) ) ),
inference(simp,[status(thm)],[118]) ).
thf(17,axiom,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( B @ defined ) )
| ~ ( D @ ( C @ defined ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associative_property2) ).
thf(51,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( B @ defined ) )
| ~ ( D @ ( C @ defined ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[17]) ).
thf(52,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( B @ defined ) )
| ~ ( D @ ( C @ defined ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(cnf,[status(esa)],[51]) ).
thf(1297,plain,
! [B: $i,A: $i] :
( ( ( c @ ( g @ defined ) )
!= ( B @ ( A @ defined ) ) )
| ( B @ ( A @ compose ) @ ( B @ ( A @ product ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1260,31]) ).
thf(1298,plain,
! [B: $i,A: $i] :
( ( ( c @ ( g @ defined ) )
!= ( B @ ( A @ defined ) ) )
| ( B @ ( A @ compose ) @ ( B @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[1297]) ).
thf(1299,plain,
c @ ( g @ compose ) @ ( c @ ( g @ product ) ),
inference(pattern_uni,[status(thm)],[1298:[bind(A,$thf( g )),bind(B,$thf( c ))]]) ).
thf(1408,plain,
! [A: $i] :
( ( A
!= ( c @ ( g @ compose ) ) )
| ( a @ codomain @ ( c @ ( g @ product ) ) )
| ~ ( a @ ( a @ ( A @ product ) ) ) ),
inference(paramod_ordered,[status(thm)],[297,1299]) ).
thf(1409,plain,
( ( a @ codomain @ ( c @ ( g @ product ) ) )
| ~ ( a @ ( a @ ( c @ ( g @ compose ) @ product ) ) ) ),
inference(pattern_uni,[status(thm)],[1408:[bind(A,$thf( c @ ( g @ compose ) ))]]) ).
thf(12195,plain,
! [B: $i,A: $i] :
( ( ( d @ ( h @ codomain @ defined ) )
!= ( B @ ( A @ defined ) ) )
| ( B @ ( A @ compose ) @ ( B @ ( A @ product ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[12151,31]) ).
thf(12196,plain,
! [B: $i,A: $i] :
( ( ( d @ ( h @ codomain @ defined ) )
!= ( B @ ( A @ defined ) ) )
| ( B @ ( A @ compose ) @ ( B @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[12195]) ).
thf(12197,plain,
d @ ( h @ codomain @ compose ) @ ( d @ ( h @ codomain @ product ) ),
inference(pattern_uni,[status(thm)],[12196:[bind(A,$thf( h @ codomain )),bind(B,$thf( d ))]]) ).
thf(519,plain,
! [A: $i] :
( ( ( c @ ( b @ ( a @ product ) ) )
!= ( A @ ( a @ ( g @ product ) ) ) )
| ~ ( A @ ( a @ ( h @ product ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[32,315]) ).
thf(520,plain,
! [A: $i] :
( ( ( c @ ( b @ ( a @ product ) ) )
!= ( A @ ( a @ ( g @ product ) ) ) )
| ~ ( A @ ( a @ ( h @ product ) ) ) ),
inference(simp,[status(thm)],[519]) ).
thf(543,plain,
! [A: $i] :
( ( c != A )
| ( b != a )
| ( a != g )
| ~ ( A @ ( a @ ( h @ product ) ) ) ),
inference(simp,[status(thm)],[520]) ).
thf(570,plain,
( ( b != a )
| ( a != g )
| ~ ( c @ ( a @ ( h @ product ) ) ) ),
inference(simp,[status(thm)],[543]) ).
thf(9180,plain,
! [A: $i] :
( ( ( A @ ( A @ domain @ ( A @ product ) ) )
!= ( a @ ( g @ compose ) @ ( a @ ( h @ product ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[48,8906]) ).
thf(9181,plain,
! [A: $i] :
( ( A @ ( A @ domain @ ( A @ product ) ) )
!= ( a @ ( g @ compose ) @ ( a @ ( h @ product ) ) ) ),
inference(simp,[status(thm)],[9180]) ).
thf(9219,plain,
! [A: $i] :
( ( A
!= ( a @ ( g @ compose ) ) )
| ( ( A @ domain )
!= a )
| ( A != h ) ),
inference(simp,[status(thm)],[9181]) ).
thf(9230,plain,
( ( ( a @ ( g @ compose ) )
!= h )
| ( ( h @ domain )
!= a ) ),
inference(simp,[status(thm)],[9219]) ).
thf(1020,plain,
! [A: $i] :
( ( ( a @ codomain )
!= ( a @ codomain ) )
| ( A != h )
| ~ ( a @ ( a @ ( g @ product ) ) )
| ~ ( a @ ( a @ ( A @ product ) ) ) ),
inference(paramod_ordered,[status(thm)],[297,556]) ).
thf(1021,plain,
! [A: $i] :
( ( A != h )
| ~ ( a @ ( a @ ( g @ product ) ) )
| ~ ( a @ ( a @ ( A @ product ) ) ) ),
inference(pattern_uni,[status(thm)],[1020:[]]) ).
thf(1051,plain,
( ~ ( a @ ( a @ ( g @ product ) ) )
| ~ ( a @ ( a @ ( h @ product ) ) ) ),
inference(simp,[status(thm)],[1021]) ).
thf(1939,plain,
! [A: $i] :
( ( ( A @ ( A @ domain @ ( A @ product ) ) )
!= ( a @ ( a @ ( h @ product ) ) ) )
| ~ ( a @ ( a @ ( g @ product ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[48,1051]) ).
thf(1940,plain,
! [A: $i] :
( ( ( A @ ( A @ domain @ ( A @ product ) ) )
!= ( a @ ( a @ ( h @ product ) ) ) )
| ~ ( a @ ( a @ ( g @ product ) ) ) ),
inference(simp,[status(thm)],[1939]) ).
thf(1967,plain,
! [A: $i] :
( ( A != a )
| ( ( A @ domain )
!= a )
| ( A != h )
| ~ ( a @ ( a @ ( g @ product ) ) ) ),
inference(simp,[status(thm)],[1940]) ).
thf(1992,plain,
( ( a != h )
| ( ( h @ domain )
!= a )
| ~ ( a @ ( a @ ( g @ product ) ) ) ),
inference(simp,[status(thm)],[1967]) ).
thf(107,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( c @ ( b @ ( a @ product ) ) )
!= ( H @ ( E @ ( G @ product ) ) ) )
| ( H @ ( F @ defined ) )
| ~ $true
| ~ ( A @ ( G @ ( F @ product ) ) )
| ~ ( D @ ( C @ defined ) )
| ~ ( E @ ( D @ ( B @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(paramod_ordered,[status(thm)],[32,82]) ).
thf(108,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( c @ ( b @ ( a @ product ) ) )
!= ( H @ ( E @ ( G @ product ) ) ) )
| ( H @ ( F @ defined ) )
| ~ ( A @ ( G @ ( F @ product ) ) )
| ~ ( D @ ( C @ defined ) )
| ~ ( E @ ( D @ ( B @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[107]) ).
thf(109,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( c @ ( E @ defined ) )
| ~ ( A @ ( a @ ( E @ product ) ) )
| ~ ( D @ ( C @ defined ) )
| ~ ( b @ ( D @ ( B @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(pattern_uni,[status(thm)],[108:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( b )),bind(F,$thf( F )),bind(G,$thf( a )),bind(H,$thf( c ))]]) ).
thf(152,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( c @ ( E @ defined ) )
| ~ ( A @ ( a @ ( E @ product ) ) )
| ~ ( D @ ( C @ defined ) )
| ~ ( b @ ( D @ ( B @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[109]) ).
thf(44041,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ compose ) @ ( B @ ( A @ product ) ) )
!= ( C @ ( a @ ( c @ product ) ) ) )
| ~ ( C @ ( a @ ( a @ product ) ) )
| ~ $true
| ~ ( B @ ( A @ defined ) ) ),
inference(paramod_ordered,[status(thm)],[31,697]) ).
thf(44042,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ compose ) @ ( B @ ( A @ product ) ) )
!= ( C @ ( a @ ( c @ product ) ) ) )
| ~ ( C @ ( a @ ( a @ product ) ) )
| ~ ( B @ ( A @ defined ) ) ),
inference(simp,[status(thm)],[44041]) ).
thf(44043,plain,
( ~ ( a @ ( c @ compose ) @ ( a @ ( a @ product ) ) )
| ~ ( a @ ( c @ defined ) ) ),
inference(pattern_uni,[status(thm)],[44042:[bind(A,$thf( c )),bind(B,$thf( a )),bind(C,$thf( a @ ( c @ compose ) ))]]) ).
thf(29329,plain,
! [A: $i] :
( ( ( a @ ( h @ defined ) )
!= ( d @ ( A @ defined ) ) )
| ( g @ ( A @ defined ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[8876,2221]) ).
thf(29330,plain,
! [A: $i] :
( ( ( a @ ( h @ defined ) )
!= ( d @ ( A @ defined ) ) )
| ( g @ ( A @ defined ) ) ),
inference(simp,[status(thm)],[29329]) ).
thf(29344,plain,
! [A: $i] :
( ( d != a )
| ( h != A )
| ( g @ ( A @ defined ) ) ),
inference(simp,[status(thm)],[29330]) ).
thf(29378,plain,
( ( d != a )
| ( g @ ( h @ defined ) ) ),
inference(simp,[status(thm)],[29344]) ).
thf(13786,plain,
! [B: $i,A: $i] :
( ( ( c @ ( h @ defined ) )
!= ( A @ ( B @ defined ) ) )
| ( B @ ( A @ defined ) )
| ~ $true
| ~ ( B @ ( A @ ( A @ product ) ) ) ),
inference(paramod_ordered,[status(thm)],[1266,84]) ).
thf(13787,plain,
! [B: $i,A: $i] :
( ( ( c @ ( h @ defined ) )
!= ( A @ ( B @ defined ) ) )
| ( B @ ( A @ defined ) )
| ~ ( B @ ( A @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[13786]) ).
thf(13788,plain,
( ( h @ ( c @ defined ) )
| ~ ( h @ ( c @ ( c @ product ) ) ) ),
inference(pattern_uni,[status(thm)],[13787:[bind(A,$thf( c )),bind(B,$thf( h ))]]) ).
thf(8933,plain,
! [B: $i,A: $i] :
( ( ( a @ ( g @ defined ) )
!= ( B @ ( A @ defined ) ) )
| ( B @ ( A @ compose ) @ ( B @ ( A @ product ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[8855,31]) ).
thf(8934,plain,
! [B: $i,A: $i] :
( ( ( a @ ( g @ defined ) )
!= ( B @ ( A @ defined ) ) )
| ( B @ ( A @ compose ) @ ( B @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[8933]) ).
thf(8935,plain,
a @ ( g @ compose ) @ ( a @ ( g @ product ) ),
inference(pattern_uni,[status(thm)],[8934:[bind(A,$thf( g )),bind(B,$thf( a ))]]) ).
thf(9437,plain,
( ( ( a @ ( g @ compose ) @ ( a @ ( g @ product ) ) )
!= ( a @ ( a @ ( g @ product ) ) ) )
| ~ $true
| ~ ( a @ ( a @ ( h @ product ) ) ) ),
inference(paramod_ordered,[status(thm)],[8935,1051]) ).
thf(9438,plain,
( ( ( a @ ( g @ compose ) @ ( a @ ( g @ product ) ) )
!= ( a @ ( a @ ( g @ product ) ) ) )
| ~ ( a @ ( a @ ( h @ product ) ) ) ),
inference(simp,[status(thm)],[9437]) ).
thf(9582,plain,
( ( ( a @ ( g @ compose ) )
!= a )
| ( a != a )
| ( g != g )
| ~ ( a @ ( a @ ( h @ product ) ) ) ),
inference(simp,[status(thm)],[9438]) ).
thf(9636,plain,
( ( ( a @ ( g @ compose ) )
!= a )
| ~ ( a @ ( a @ ( h @ product ) ) ) ),
inference(simp,[status(thm)],[9582]) ).
thf(172,plain,
! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ codomain @ defined ) )
!= ( E @ ( D @ defined ) ) )
| ( I @ ( G @ defined ) )
| ~ ( I @ ( F @ ( H @ product ) ) )
| ~ ( B @ ( H @ ( G @ product ) ) )
| ~ $true
| ~ ( F @ ( E @ ( C @ product ) ) )
| ~ ( D @ ( C @ ( B @ product ) ) ) ),
inference(paramod_ordered,[status(thm)],[24,82]) ).
thf(173,plain,
! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ codomain @ defined ) )
!= ( E @ ( D @ defined ) ) )
| ( I @ ( G @ defined ) )
| ~ ( I @ ( F @ ( H @ product ) ) )
| ~ ( B @ ( H @ ( G @ product ) ) )
| ~ ( F @ ( E @ ( C @ product ) ) )
| ~ ( D @ ( C @ ( B @ product ) ) ) ),
inference(simp,[status(thm)],[172]) ).
thf(174,plain,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( F @ ( D @ defined ) )
| ~ ( F @ ( C @ ( E @ product ) ) )
| ~ ( A @ ( E @ ( D @ product ) ) )
| ~ ( C @ ( G @ ( B @ product ) ) )
| ~ ( G @ codomain @ ( B @ ( A @ product ) ) ) ),
inference(pattern_uni,[status(thm)],[173:[bind(A,$thf( J )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( J @ codomain )),bind(E,$thf( J ))]]) ).
thf(179,plain,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( F @ ( D @ defined ) )
| ~ ( F @ ( C @ ( E @ product ) ) )
| ~ ( A @ ( E @ ( D @ product ) ) )
| ~ ( C @ ( G @ ( B @ product ) ) )
| ~ ( G @ codomain @ ( B @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[174]) ).
thf(12684,plain,
( ( ( a @ ( h @ compose ) @ ( a @ ( h @ product ) ) )
!= ( a @ ( a @ ( h @ product ) ) ) )
| ( ( a @ ( g @ compose ) )
!= a )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[8996,9636]) ).
thf(12685,plain,
( ( ( a @ ( h @ compose ) @ ( a @ ( h @ product ) ) )
!= ( a @ ( a @ ( h @ product ) ) ) )
| ( ( a @ ( g @ compose ) )
!= a ) ),
inference(simp,[status(thm)],[12684]) ).
thf(12792,plain,
( ( ( a @ ( h @ compose ) )
!= a )
| ( a != a )
| ( h != h )
| ( ( a @ ( g @ compose ) )
!= a ) ),
inference(simp,[status(thm)],[12685]) ).
thf(12828,plain,
( ( ( a @ ( h @ compose ) )
!= a )
| ( ( a @ ( g @ compose ) )
!= a ) ),
inference(simp,[status(thm)],[12792]) ).
thf(134,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ $true
| ( ( H @ ( E @ ( G @ product ) ) )
!= ( C @ ( B @ ( A @ product ) ) ) )
| ( H @ ( F @ defined ) )
| ~ ( A @ ( G @ ( F @ product ) ) )
| ~ ( D @ ( C @ defined ) )
| ~ ( E @ ( D @ ( B @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(eqfactor_ordered,[status(thm)],[82]) ).
thf(137,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( C @ defined ) )
| ~ ( D @ ( D @ ( C @ product ) ) )
| ~ ( A @ ( E @ defined ) )
| ~ ( B @ ( A @ ( B @ product ) ) )
| ~ ( E @ ( B @ ( D @ product ) ) ) ),
inference(pattern_uni,[status(thm)],[134:[bind(A,$thf( G )),bind(B,$thf( E )),bind(C,$thf( H ))]]) ).
thf(147,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( C @ defined ) )
| ~ ( D @ ( D @ ( C @ product ) ) )
| ~ ( A @ ( E @ defined ) )
| ~ ( B @ ( A @ ( B @ product ) ) )
| ~ ( E @ ( B @ ( D @ product ) ) ) ),
inference(simp,[status(thm)],[137]) ).
thf(13075,plain,
! [B: $i,A: $i] :
( ( ( d @ ( g @ codomain @ defined ) )
!= ( B @ ( A @ defined ) ) )
| ( B @ ( A @ compose ) @ ( B @ ( A @ product ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[13031,31]) ).
thf(13076,plain,
! [B: $i,A: $i] :
( ( ( d @ ( g @ codomain @ defined ) )
!= ( B @ ( A @ defined ) ) )
| ( B @ ( A @ compose ) @ ( B @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[13075]) ).
thf(13077,plain,
d @ ( g @ codomain @ compose ) @ ( d @ ( g @ codomain @ product ) ),
inference(pattern_uni,[status(thm)],[13076:[bind(A,$thf( g @ codomain )),bind(B,$thf( d ))]]) ).
thf(1343,plain,
! [B: $i,A: $i] :
( ( ( b @ ( a @ defined ) )
!= ( B @ ( A @ defined ) ) )
| ( B @ ( A @ compose ) @ ( B @ ( A @ product ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1281,31]) ).
thf(1344,plain,
! [B: $i,A: $i] :
( ( ( b @ ( a @ defined ) )
!= ( B @ ( A @ defined ) ) )
| ( B @ ( A @ compose ) @ ( B @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[1343]) ).
thf(1345,plain,
b @ ( a @ compose ) @ ( b @ ( a @ product ) ),
inference(pattern_uni,[status(thm)],[1344:[bind(A,$thf( a )),bind(B,$thf( b ))]]) ).
thf(9155,plain,
! [A: $i] :
( ( ( A @ ( A @ ( A @ codomain @ product ) ) )
!= ( a @ ( g @ compose ) @ ( a @ ( h @ product ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[37,8906]) ).
thf(9156,plain,
! [A: $i] :
( ( A @ ( A @ ( A @ codomain @ product ) ) )
!= ( a @ ( g @ compose ) @ ( a @ ( h @ product ) ) ) ),
inference(simp,[status(thm)],[9155]) ).
thf(9227,plain,
! [A: $i] :
( ( A
!= ( a @ ( g @ compose ) ) )
| ( A != a )
| ( ( A @ codomain )
!= h ) ),
inference(simp,[status(thm)],[9156]) ).
thf(9236,plain,
( ( ( a @ ( g @ compose ) )
!= a )
| ( ( a @ codomain )
!= h ) ),
inference(simp,[status(thm)],[9227]) ).
thf(61,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( c @ ( b @ ( a @ product ) ) )
!= ( C @ ( B @ ( A @ product ) ) ) )
| ( E @ ( A @ defined ) )
| ~ ( D @ ( C @ defined ) )
| ~ ( E @ ( D @ ( B @ product ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[32,26]) ).
thf(62,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( c @ ( b @ ( a @ product ) ) )
!= ( C @ ( B @ ( A @ product ) ) ) )
| ( E @ ( A @ defined ) )
| ~ ( D @ ( C @ defined ) )
| ~ ( E @ ( D @ ( B @ product ) ) ) ),
inference(simp,[status(thm)],[61]) ).
thf(63,plain,
! [B: $i,A: $i] :
( ( B @ ( a @ defined ) )
| ~ ( A @ ( c @ defined ) )
| ~ ( B @ ( A @ ( b @ product ) ) ) ),
inference(pattern_uni,[status(thm)],[62:[bind(A,$thf( a )),bind(B,$thf( b )),bind(C,$thf( c ))]]) ).
thf(85,plain,
! [B: $i,A: $i] :
( ( B @ ( a @ defined ) )
| ~ ( A @ ( c @ defined ) )
| ~ ( B @ ( A @ ( b @ product ) ) ) ),
inference(simp,[status(thm)],[63]) ).
thf(1577,plain,
! [A: $i] :
( ( A
!= ( c @ ( h @ compose ) ) )
| ( a @ codomain @ ( c @ ( h @ product ) ) )
| ~ ( a @ ( a @ ( A @ product ) ) ) ),
inference(paramod_ordered,[status(thm)],[297,1322]) ).
thf(1578,plain,
( ( a @ codomain @ ( c @ ( h @ product ) ) )
| ~ ( a @ ( a @ ( c @ ( h @ compose ) @ product ) ) ) ),
inference(pattern_uni,[status(thm)],[1577:[bind(A,$thf( c @ ( h @ compose ) ))]]) ).
thf(7189,plain,
! [A: $i] :
( ( ( A @ ( A @ ( A @ codomain @ product ) ) )
!= ( a @ ( a @ ( c @ ( h @ compose ) @ product ) ) ) )
| ( a @ codomain @ ( c @ ( h @ product ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[37,1578]) ).
thf(7190,plain,
! [A: $i] :
( ( ( A @ ( A @ ( A @ codomain @ product ) ) )
!= ( a @ ( a @ ( c @ ( h @ compose ) @ product ) ) ) )
| ( a @ codomain @ ( c @ ( h @ product ) ) ) ),
inference(simp,[status(thm)],[7189]) ).
thf(7243,plain,
! [A: $i] :
( ( A != a )
| ( A != a )
| ( ( A @ codomain )
!= ( c @ ( h @ compose ) ) )
| ( a @ codomain @ ( c @ ( h @ product ) ) ) ),
inference(simp,[status(thm)],[7190]) ).
thf(7269,plain,
( ( ( c @ ( h @ compose ) )
!= ( a @ codomain ) )
| ( a @ codomain @ ( c @ ( h @ product ) ) ) ),
inference(simp,[status(thm)],[7243]) ).
thf(9332,plain,
! [A: $i] :
( ( ( A @ ( A @ domain @ ( A @ product ) ) )
!= ( a @ ( h @ compose ) @ ( a @ ( g @ product ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[48,8969]) ).
thf(9333,plain,
! [A: $i] :
( ( A @ ( A @ domain @ ( A @ product ) ) )
!= ( a @ ( h @ compose ) @ ( a @ ( g @ product ) ) ) ),
inference(simp,[status(thm)],[9332]) ).
thf(9363,plain,
! [A: $i] :
( ( A
!= ( a @ ( h @ compose ) ) )
| ( ( A @ domain )
!= a )
| ( A != g ) ),
inference(simp,[status(thm)],[9333]) ).
thf(9384,plain,
( ( ( a @ ( h @ compose ) )
!= g )
| ( ( g @ domain )
!= a ) ),
inference(simp,[status(thm)],[9363]) ).
thf(521,plain,
! [A: $i] :
( ( ( c @ ( b @ ( a @ product ) ) )
!= ( A @ ( a @ ( h @ product ) ) ) )
| ~ $true
| ~ ( A @ ( a @ ( g @ product ) ) ) ),
inference(paramod_ordered,[status(thm)],[32,315]) ).
thf(522,plain,
! [A: $i] :
( ( ( c @ ( b @ ( a @ product ) ) )
!= ( A @ ( a @ ( h @ product ) ) ) )
| ~ ( A @ ( a @ ( g @ product ) ) ) ),
inference(simp,[status(thm)],[521]) ).
thf(541,plain,
! [A: $i] :
( ( c != A )
| ( b != a )
| ( a != h )
| ~ ( A @ ( a @ ( g @ product ) ) ) ),
inference(simp,[status(thm)],[522]) ).
thf(567,plain,
( ( b != a )
| ( a != h )
| ~ ( c @ ( a @ ( g @ product ) ) ) ),
inference(simp,[status(thm)],[541]) ).
thf(2404,plain,
( ( ( c @ ( b @ ( a @ product ) ) )
!= ( c @ ( a @ ( g @ product ) ) ) )
| ( b != a )
| ( a != h )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[32,567]) ).
thf(2405,plain,
( ( ( c @ ( b @ ( a @ product ) ) )
!= ( c @ ( a @ ( g @ product ) ) ) )
| ( b != a )
| ( a != h ) ),
inference(simp,[status(thm)],[2404]) ).
thf(2411,plain,
( ( c != c )
| ( b != a )
| ( a != g )
| ( b != a )
| ( a != h ) ),
inference(simp,[status(thm)],[2405]) ).
thf(2428,plain,
( ( a != g )
| ( b != a )
| ( a != h ) ),
inference(simp,[status(thm)],[2411]) ).
thf(89,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( d @ ( c @ ( g @ product ) ) )
!= ( E @ ( D @ ( B @ product ) ) ) )
| ( H @ ( F @ defined ) )
| ~ ( H @ ( E @ ( G @ product ) ) )
| ~ ( A @ ( G @ ( F @ product ) ) )
| ~ ( D @ ( C @ defined ) )
| ~ $true
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(paramod_ordered,[status(thm)],[53,82]) ).
thf(90,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( d @ ( c @ ( g @ product ) ) )
!= ( E @ ( D @ ( B @ product ) ) ) )
| ( H @ ( F @ defined ) )
| ~ ( H @ ( E @ ( G @ product ) ) )
| ~ ( A @ ( G @ ( F @ product ) ) )
| ~ ( D @ ( C @ defined ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[89]) ).
thf(91,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( C @ defined ) )
| ~ ( E @ ( d @ ( D @ product ) ) )
| ~ ( A @ ( D @ ( C @ product ) ) )
| ~ ( c @ ( B @ defined ) )
| ~ ( B @ ( g @ ( A @ product ) ) ) ),
inference(pattern_uni,[status(thm)],[90:[bind(A,$thf( A )),bind(B,$thf( g )),bind(C,$thf( C )),bind(D,$thf( c )),bind(E,$thf( d ))]]) ).
thf(160,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( C @ defined ) )
| ~ ( E @ ( d @ ( D @ product ) ) )
| ~ ( A @ ( D @ ( C @ product ) ) )
| ~ ( c @ ( B @ defined ) )
| ~ ( B @ ( g @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[91]) ).
thf(54616,plain,
! [A: $i] :
( ( ( A @ domain @ ( A @ defined ) )
!= ( a @ ( c @ defined ) ) )
| ~ ( a @ ( c @ compose ) @ ( a @ ( a @ product ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[23,44043]) ).
thf(54617,plain,
! [A: $i] :
( ( ( A @ domain @ ( A @ defined ) )
!= ( a @ ( c @ defined ) ) )
| ~ ( a @ ( c @ compose ) @ ( a @ ( a @ product ) ) ) ),
inference(simp,[status(thm)],[54616]) ).
thf(54769,plain,
! [A: $i] :
( ( ( A @ domain )
!= a )
| ( A != c )
| ~ ( a @ ( c @ compose ) @ ( a @ ( a @ product ) ) ) ),
inference(simp,[status(thm)],[54617]) ).
thf(54831,plain,
( ( ( c @ domain )
!= a )
| ~ ( a @ ( c @ compose ) @ ( a @ ( a @ product ) ) ) ),
inference(simp,[status(thm)],[54769]) ).
thf(44000,plain,
! [A: $i] :
( ( ( a @ ( a @ ( a @ product ) ) )
!= ( A @ ( a @ ( a @ product ) ) ) )
| ~ $true
| ~ ( A @ ( a @ ( c @ product ) ) )
| ( ( a @ domain )
!= a ) ),
inference(paramod_ordered,[status(thm)],[451,697]) ).
thf(44001,plain,
! [A: $i] :
( ( ( a @ ( a @ ( a @ product ) ) )
!= ( A @ ( a @ ( a @ product ) ) ) )
| ~ ( A @ ( a @ ( c @ product ) ) )
| ( ( a @ domain )
!= a ) ),
inference(simp,[status(thm)],[44000]) ).
thf(44002,plain,
( ~ ( a @ ( a @ ( c @ product ) ) )
| ( ( a @ domain )
!= a ) ),
inference(pattern_uni,[status(thm)],[44001:[bind(A,$thf( a ))]]) ).
thf(45365,plain,
! [A: $i] :
( ( ( A @ ( A @ ( A @ codomain @ product ) ) )
!= ( a @ ( a @ ( c @ product ) ) ) )
| ~ $true
| ( ( a @ domain )
!= a ) ),
inference(paramod_ordered,[status(thm)],[37,44002]) ).
thf(45366,plain,
! [A: $i] :
( ( ( A @ ( A @ ( A @ codomain @ product ) ) )
!= ( a @ ( a @ ( c @ product ) ) ) )
| ( ( a @ domain )
!= a ) ),
inference(simp,[status(thm)],[45365]) ).
thf(45493,plain,
! [A: $i] :
( ( A != a )
| ( A != a )
| ( ( A @ codomain )
!= c )
| ( ( a @ domain )
!= a ) ),
inference(simp,[status(thm)],[45366]) ).
thf(45543,plain,
( ( ( a @ codomain )
!= c )
| ( ( a @ domain )
!= a ) ),
inference(simp,[status(thm)],[45493]) ).
thf(13848,plain,
! [B: $i,A: $i] :
( ( ( a @ ( h @ defined ) )
!= ( A @ ( B @ defined ) ) )
| ( B @ ( A @ defined ) )
| ~ $true
| ~ ( B @ ( A @ ( A @ product ) ) ) ),
inference(paramod_ordered,[status(thm)],[8876,84]) ).
thf(13849,plain,
! [B: $i,A: $i] :
( ( ( a @ ( h @ defined ) )
!= ( A @ ( B @ defined ) ) )
| ( B @ ( A @ defined ) )
| ~ ( B @ ( A @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[13848]) ).
thf(13850,plain,
( ( h @ ( a @ defined ) )
| ~ ( h @ ( a @ ( a @ product ) ) ) ),
inference(pattern_uni,[status(thm)],[13849:[bind(A,$thf( a )),bind(B,$thf( h ))]]) ).
thf(1010,plain,
( ( ( a @ ( a @ ( a @ product ) ) )
!= ( a @ ( a @ ( g @ product ) ) ) )
| ( ( a @ codomain )
!= h )
| ~ $true
| ( ( a @ domain )
!= a ) ),
inference(paramod_ordered,[status(thm)],[451,556]) ).
thf(1011,plain,
( ( ( a @ ( a @ ( a @ product ) ) )
!= ( a @ ( a @ ( g @ product ) ) ) )
| ( ( a @ codomain )
!= h )
| ( ( a @ domain )
!= a ) ),
inference(simp,[status(thm)],[1010]) ).
thf(1033,plain,
( ( a != a )
| ( a != a )
| ( a != g )
| ( ( a @ codomain )
!= h )
| ( ( a @ domain )
!= a ) ),
inference(simp,[status(thm)],[1011]) ).
thf(1042,plain,
( ( a != g )
| ( ( a @ codomain )
!= h )
| ( ( a @ domain )
!= a ) ),
inference(simp,[status(thm)],[1033]) ).
thf(870,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ codomain @ compose ) @ ( A @ ( A @ codomain @ product ) ) )
!= ( B @ ( a @ ( h @ product ) ) ) )
| ~ $true
| ~ ( B @ ( a @ ( g @ product ) ) ) ),
inference(paramod_ordered,[status(thm)],[766,315]) ).
thf(871,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ codomain @ compose ) @ ( A @ ( A @ codomain @ product ) ) )
!= ( B @ ( a @ ( h @ product ) ) ) )
| ~ ( B @ ( a @ ( g @ product ) ) ) ),
inference(simp,[status(thm)],[870]) ).
thf(895,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ codomain @ compose ) )
!= B )
| ( A != a )
| ( ( A @ codomain )
!= h )
| ~ ( B @ ( a @ ( g @ product ) ) ) ),
inference(simp,[status(thm)],[871]) ).
thf(916,plain,
( ( ( a @ codomain )
!= h )
| ~ ( a @ ( a @ codomain @ compose ) @ ( a @ ( g @ product ) ) ) ),
inference(simp,[status(thm)],[895]) ).
thf(29591,plain,
! [B: $i,A: $i] :
( ( ( g @ ( h @ codomain @ defined ) )
!= ( A @ ( B @ defined ) ) )
| ( B @ ( A @ defined ) )
| ~ $true
| ~ ( B @ ( A @ ( A @ product ) ) ) ),
inference(paramod_ordered,[status(thm)],[29266,84]) ).
thf(29592,plain,
! [B: $i,A: $i] :
( ( ( g @ ( h @ codomain @ defined ) )
!= ( A @ ( B @ defined ) ) )
| ( B @ ( A @ defined ) )
| ~ ( B @ ( A @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[29591]) ).
thf(29593,plain,
( ( h @ codomain @ ( g @ defined ) )
| ~ ( h @ codomain @ ( g @ ( g @ product ) ) ) ),
inference(pattern_uni,[status(thm)],[29592:[bind(A,$thf( g )),bind(B,$thf( h @ codomain ))]]) ).
thf(797,plain,
! [B: $i,A: $i] :
( ( ( A @ domain @ ( A @ compose ) @ ( A @ domain @ ( A @ product ) ) )
!= ( B @ ( a @ ( h @ product ) ) ) )
| ~ $true
| ~ ( B @ ( a @ ( g @ product ) ) ) ),
inference(paramod_ordered,[status(thm)],[762,315]) ).
thf(798,plain,
! [B: $i,A: $i] :
( ( ( A @ domain @ ( A @ compose ) @ ( A @ domain @ ( A @ product ) ) )
!= ( B @ ( a @ ( h @ product ) ) ) )
| ~ ( B @ ( a @ ( g @ product ) ) ) ),
inference(simp,[status(thm)],[797]) ).
thf(814,plain,
! [B: $i,A: $i] :
( ( ( A @ domain @ ( A @ compose ) )
!= B )
| ( ( A @ domain )
!= a )
| ( A != h )
| ~ ( B @ ( a @ ( g @ product ) ) ) ),
inference(simp,[status(thm)],[798]) ).
thf(830,plain,
( ( ( h @ domain )
!= a )
| ~ ( h @ domain @ ( h @ compose ) @ ( a @ ( g @ product ) ) ) ),
inference(simp,[status(thm)],[814]) ).
thf(54388,plain,
( ( ( a @ ( c @ defined ) )
!= ( a @ ( g @ defined ) ) )
| ~ ( a @ ( c @ compose ) @ ( a @ ( a @ product ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[8855,44043]) ).
thf(54389,plain,
( ( ( a @ ( c @ defined ) )
!= ( a @ ( g @ defined ) ) )
| ~ ( a @ ( c @ compose ) @ ( a @ ( a @ product ) ) ) ),
inference(simp,[status(thm)],[54388]) ).
thf(54710,plain,
( ( a != a )
| ( c != g )
| ~ ( a @ ( c @ compose ) @ ( a @ ( a @ product ) ) ) ),
inference(simp,[status(thm)],[54389]) ).
thf(54801,plain,
( ( c != g )
| ~ ( a @ ( c @ compose ) @ ( a @ ( a @ product ) ) ) ),
inference(simp,[status(thm)],[54710]) ).
thf(29290,plain,
! [A: $i] :
( ( ( a @ ( c @ codomain @ defined ) )
!= ( d @ ( A @ defined ) ) )
| ( g @ ( A @ defined ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[8868,2221]) ).
thf(29291,plain,
! [A: $i] :
( ( ( a @ ( c @ codomain @ defined ) )
!= ( d @ ( A @ defined ) ) )
| ( g @ ( A @ defined ) ) ),
inference(simp,[status(thm)],[29290]) ).
thf(29361,plain,
! [A: $i] :
( ( d != a )
| ( ( c @ codomain )
!= A )
| ( g @ ( A @ defined ) ) ),
inference(simp,[status(thm)],[29291]) ).
thf(29394,plain,
( ( d != a )
| ( g @ ( c @ codomain @ defined ) ) ),
inference(simp,[status(thm)],[29361]) ).
thf(32944,plain,
! [B: $i,A: $i] :
( ( ( g @ ( c @ codomain @ defined ) )
!= ( B @ ( A @ defined ) ) )
| ( B @ ( A @ compose ) @ ( B @ ( A @ product ) ) )
| ~ $true
| ( d != a ) ),
inference(paramod_ordered,[status(thm)],[29394,31]) ).
thf(32945,plain,
! [B: $i,A: $i] :
( ( ( g @ ( c @ codomain @ defined ) )
!= ( B @ ( A @ defined ) ) )
| ( B @ ( A @ compose ) @ ( B @ ( A @ product ) ) )
| ( d != a ) ),
inference(simp,[status(thm)],[32944]) ).
thf(32946,plain,
( ( g @ ( c @ codomain @ compose ) @ ( g @ ( c @ codomain @ product ) ) )
| ( d != a ) ),
inference(pattern_uni,[status(thm)],[32945:[bind(A,$thf( c @ codomain )),bind(B,$thf( g ))]]) ).
thf(9884,plain,
! [A: $i] :
( ( A
!= ( a @ ( h @ compose ) ) )
| ( a @ codomain @ ( a @ ( h @ product ) ) )
| ~ ( a @ ( a @ ( A @ product ) ) ) ),
inference(paramod_ordered,[status(thm)],[297,8996]) ).
thf(9885,plain,
( ( a @ codomain @ ( a @ ( h @ product ) ) )
| ~ ( a @ ( a @ ( a @ ( h @ compose ) @ product ) ) ) ),
inference(pattern_uni,[status(thm)],[9884:[bind(A,$thf( a @ ( h @ compose ) ))]]) ).
thf(113,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( d @ ( c @ ( h @ product ) ) )
!= ( E @ ( D @ ( B @ product ) ) ) )
| ( H @ ( F @ defined ) )
| ~ ( H @ ( E @ ( G @ product ) ) )
| ~ ( A @ ( G @ ( F @ product ) ) )
| ~ ( D @ ( C @ defined ) )
| ~ $true
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(paramod_ordered,[status(thm)],[54,82]) ).
thf(114,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( d @ ( c @ ( h @ product ) ) )
!= ( E @ ( D @ ( B @ product ) ) ) )
| ( H @ ( F @ defined ) )
| ~ ( H @ ( E @ ( G @ product ) ) )
| ~ ( A @ ( G @ ( F @ product ) ) )
| ~ ( D @ ( C @ defined ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[113]) ).
thf(115,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( C @ defined ) )
| ~ ( E @ ( d @ ( D @ product ) ) )
| ~ ( A @ ( D @ ( C @ product ) ) )
| ~ ( c @ ( B @ defined ) )
| ~ ( B @ ( h @ ( A @ product ) ) ) ),
inference(pattern_uni,[status(thm)],[114:[bind(A,$thf( A )),bind(B,$thf( h )),bind(C,$thf( C )),bind(D,$thf( c )),bind(E,$thf( d ))]]) ).
thf(156,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( C @ defined ) )
| ~ ( E @ ( d @ ( D @ product ) ) )
| ~ ( A @ ( D @ ( C @ product ) ) )
| ~ ( c @ ( B @ defined ) )
| ~ ( B @ ( h @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[115]) ).
thf(44044,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ compose ) @ ( B @ ( A @ product ) ) )
!= ( C @ ( a @ ( a @ product ) ) ) )
| ~ $true
| ~ ( C @ ( a @ ( c @ product ) ) )
| ~ ( B @ ( A @ defined ) ) ),
inference(paramod_ordered,[status(thm)],[31,697]) ).
thf(44045,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ compose ) @ ( B @ ( A @ product ) ) )
!= ( C @ ( a @ ( a @ product ) ) ) )
| ~ ( C @ ( a @ ( c @ product ) ) )
| ~ ( B @ ( A @ defined ) ) ),
inference(simp,[status(thm)],[44044]) ).
thf(44046,plain,
( ~ ( a @ ( a @ compose ) @ ( a @ ( c @ product ) ) )
| ~ ( a @ ( a @ defined ) ) ),
inference(pattern_uni,[status(thm)],[44045:[bind(A,$thf( a )),bind(B,$thf( a )),bind(C,$thf( a @ ( a @ compose ) ))]]) ).
thf(56287,plain,
( ( ( a @ ( a @ defined ) )
!= ( a @ ( g @ defined ) ) )
| ~ ( a @ ( a @ compose ) @ ( a @ ( c @ product ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[8855,44046]) ).
thf(56288,plain,
( ( ( a @ ( a @ defined ) )
!= ( a @ ( g @ defined ) ) )
| ~ ( a @ ( a @ compose ) @ ( a @ ( c @ product ) ) ) ),
inference(simp,[status(thm)],[56287]) ).
thf(56632,plain,
( ( a != a )
| ( a != g )
| ~ ( a @ ( a @ compose ) @ ( a @ ( c @ product ) ) ) ),
inference(simp,[status(thm)],[56288]) ).
thf(56698,plain,
( ( a != g )
| ~ ( a @ ( a @ compose ) @ ( a @ ( c @ product ) ) ) ),
inference(simp,[status(thm)],[56632]) ).
thf(10219,plain,
( ( ( a @ ( c @ codomain @ compose ) @ ( a @ ( c @ codomain @ product ) ) )
!= ( a @ ( g @ compose ) @ ( a @ ( h @ product ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[9065,8906]) ).
thf(10220,plain,
( ( a @ ( c @ codomain @ compose ) @ ( a @ ( c @ codomain @ product ) ) )
!= ( a @ ( g @ compose ) @ ( a @ ( h @ product ) ) ) ),
inference(simp,[status(thm)],[10219]) ).
thf(10341,plain,
( ( ( a @ ( c @ codomain @ compose ) )
!= ( a @ ( g @ compose ) ) )
| ( a != a )
| ( ( c @ codomain )
!= h ) ),
inference(simp,[status(thm)],[10220]) ).
thf(10398,plain,
( ( ( a @ ( c @ codomain @ compose ) )
!= ( a @ ( g @ compose ) ) )
| ( ( c @ codomain )
!= h ) ),
inference(simp,[status(thm)],[10341]) ).
thf(529,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ domain @ ( A @ product ) ) )
!= ( B @ ( a @ ( h @ product ) ) ) )
| ~ $true
| ~ ( B @ ( a @ ( g @ product ) ) ) ),
inference(paramod_ordered,[status(thm)],[48,315]) ).
thf(530,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ domain @ ( A @ product ) ) )
!= ( B @ ( a @ ( h @ product ) ) ) )
| ~ ( B @ ( a @ ( g @ product ) ) ) ),
inference(simp,[status(thm)],[529]) ).
thf(547,plain,
! [B: $i,A: $i] :
( ( A != B )
| ( ( A @ domain )
!= a )
| ( A != h )
| ~ ( B @ ( a @ ( g @ product ) ) ) ),
inference(simp,[status(thm)],[530]) ).
thf(557,plain,
( ( ( h @ domain )
!= a )
| ~ ( h @ ( a @ ( g @ product ) ) ) ),
inference(simp,[status(thm)],[547]) ).
thf(1212,plain,
( ( ( c @ ( b @ ( a @ product ) ) )
!= ( h @ ( a @ ( g @ product ) ) ) )
| ( ( h @ domain )
!= a )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[32,557]) ).
thf(1213,plain,
( ( ( c @ ( b @ ( a @ product ) ) )
!= ( h @ ( a @ ( g @ product ) ) ) )
| ( ( h @ domain )
!= a ) ),
inference(simp,[status(thm)],[1212]) ).
thf(1234,plain,
( ( c != h )
| ( b != a )
| ( a != g )
| ( ( h @ domain )
!= a ) ),
inference(simp,[status(thm)],[1213]) ).
thf(13780,plain,
! [B: $i,A: $i] :
( ( ( d @ ( h @ codomain @ defined ) )
!= ( A @ ( B @ defined ) ) )
| ( B @ ( A @ defined ) )
| ~ $true
| ~ ( B @ ( A @ ( A @ product ) ) ) ),
inference(paramod_ordered,[status(thm)],[12151,84]) ).
thf(13781,plain,
! [B: $i,A: $i] :
( ( ( d @ ( h @ codomain @ defined ) )
!= ( A @ ( B @ defined ) ) )
| ( B @ ( A @ defined ) )
| ~ ( B @ ( A @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[13780]) ).
thf(13782,plain,
( ( h @ codomain @ ( d @ defined ) )
| ~ ( h @ codomain @ ( d @ ( d @ product ) ) ) ),
inference(pattern_uni,[status(thm)],[13781:[bind(A,$thf( d )),bind(B,$thf( h @ codomain ))]]) ).
thf(4858,plain,
( ( ( a @ codomain )
!= ( a @ codomain ) )
| ( a != g )
| ( a != h )
| ( ( a @ domain )
!= a )
| ( ( a @ domain )
!= a ) ),
inference(paramod_ordered,[status(thm)],[429,1042]) ).
thf(4859,plain,
( ( ( a @ codomain )
!= ( a @ codomain ) )
| ( a != g )
| ( a != h )
| ( ( a @ domain )
!= a ) ),
inference(simp,[status(thm)],[4858]) ).
thf(4860,plain,
( ( a != g )
| ( a != h )
| ( ( a @ domain )
!= a ) ),
inference(pattern_uni,[status(thm)],[4859:[]]) ).
thf(527,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ domain @ ( A @ product ) ) )
!= ( B @ ( a @ ( g @ product ) ) ) )
| ~ ( B @ ( a @ ( h @ product ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[48,315]) ).
thf(528,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ domain @ ( A @ product ) ) )
!= ( B @ ( a @ ( g @ product ) ) ) )
| ~ ( B @ ( a @ ( h @ product ) ) ) ),
inference(simp,[status(thm)],[527]) ).
thf(545,plain,
! [B: $i,A: $i] :
( ( A != B )
| ( ( A @ domain )
!= a )
| ( A != g )
| ~ ( B @ ( a @ ( h @ product ) ) ) ),
inference(simp,[status(thm)],[528]) ).
thf(554,plain,
( ( ( g @ domain )
!= a )
| ~ ( g @ ( a @ ( h @ product ) ) ) ),
inference(simp,[status(thm)],[545]) ).
thf(29643,plain,
! [A: $i] :
( ( ( g @ ( h @ codomain @ defined ) )
!= ( c @ ( A @ defined ) ) )
| ( a @ ( A @ defined ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[29266,2218]) ).
thf(29644,plain,
! [A: $i] :
( ( ( g @ ( h @ codomain @ defined ) )
!= ( c @ ( A @ defined ) ) )
| ( a @ ( A @ defined ) ) ),
inference(simp,[status(thm)],[29643]) ).
thf(29671,plain,
! [A: $i] :
( ( c != g )
| ( ( h @ codomain )
!= A )
| ( a @ ( A @ defined ) ) ),
inference(simp,[status(thm)],[29644]) ).
thf(29702,plain,
( ( c != g )
| ( a @ ( h @ codomain @ defined ) ) ),
inference(simp,[status(thm)],[29671]) ).
thf(34455,plain,
! [B: $i,A: $i] :
( ( ( a @ ( h @ codomain @ defined ) )
!= ( B @ ( A @ defined ) ) )
| ( B @ ( A @ compose ) @ ( B @ ( A @ product ) ) )
| ~ $true
| ( c != g ) ),
inference(paramod_ordered,[status(thm)],[29702,31]) ).
thf(34456,plain,
! [B: $i,A: $i] :
( ( ( a @ ( h @ codomain @ defined ) )
!= ( B @ ( A @ defined ) ) )
| ( B @ ( A @ compose ) @ ( B @ ( A @ product ) ) )
| ( c != g ) ),
inference(simp,[status(thm)],[34455]) ).
thf(34457,plain,
( ( a @ ( h @ codomain @ compose ) @ ( a @ ( h @ codomain @ product ) ) )
| ( c != g ) ),
inference(pattern_uni,[status(thm)],[34456:[bind(A,$thf( h @ codomain )),bind(B,$thf( a ))]]) ).
thf(11441,plain,
( ( ( a @ codomain )
!= ( a @ codomain ) )
| ( c @ ( a @ compose ) @ ( c @ ( a @ codomain @ product ) ) )
| ( ( a @ domain )
!= a ) ),
inference(paramod_ordered,[status(thm)],[429,11300]) ).
thf(11442,plain,
( ( c @ ( a @ compose ) @ ( c @ ( a @ codomain @ product ) ) )
| ( ( a @ domain )
!= a ) ),
inference(pattern_uni,[status(thm)],[11441:[]]) ).
thf(67,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( d @ ( c @ ( h @ product ) ) )
!= ( C @ ( B @ ( A @ product ) ) ) )
| ( E @ ( A @ defined ) )
| ~ ( D @ ( C @ defined ) )
| ~ ( E @ ( D @ ( B @ product ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[54,26]) ).
thf(68,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( d @ ( c @ ( h @ product ) ) )
!= ( C @ ( B @ ( A @ product ) ) ) )
| ( E @ ( A @ defined ) )
| ~ ( D @ ( C @ defined ) )
| ~ ( E @ ( D @ ( B @ product ) ) ) ),
inference(simp,[status(thm)],[67]) ).
thf(69,plain,
! [B: $i,A: $i] :
( ( B @ ( h @ defined ) )
| ~ ( A @ ( d @ defined ) )
| ~ ( B @ ( A @ ( c @ product ) ) ) ),
inference(pattern_uni,[status(thm)],[68:[bind(A,$thf( h )),bind(B,$thf( c )),bind(C,$thf( d ))]]) ).
thf(79,plain,
! [B: $i,A: $i] :
( ( B @ ( h @ defined ) )
| ~ ( A @ ( d @ defined ) )
| ~ ( B @ ( A @ ( c @ product ) ) ) ),
inference(simp,[status(thm)],[69]) ).
thf(10859,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ domain @ ( A @ compose ) @ ( A @ domain @ ( A @ product ) ) )
!= ( C @ ( B @ ( c @ product ) ) ) )
| ( C @ ( h @ defined ) )
| ~ ( B @ ( d @ defined ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[762,79]) ).
thf(10860,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ domain @ ( A @ compose ) @ ( A @ domain @ ( A @ product ) ) )
!= ( C @ ( B @ ( c @ product ) ) ) )
| ( C @ ( h @ defined ) )
| ~ ( B @ ( d @ defined ) ) ),
inference(simp,[status(thm)],[10859]) ).
thf(10861,plain,
( ( c @ domain @ ( c @ compose ) @ ( h @ defined ) )
| ~ ( c @ domain @ ( d @ defined ) ) ),
inference(pattern_uni,[status(thm)],[10860:[bind(A,$thf( c )),bind(B,$thf( c @ domain )),bind(C,$thf( c @ domain @ ( c @ compose ) ))]]) ).
thf(20004,plain,
! [A: $i] :
( ( ( A @ domain @ ( A @ defined ) )
!= ( c @ domain @ ( d @ defined ) ) )
| ( c @ domain @ ( c @ compose ) @ ( h @ defined ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[23,10861]) ).
thf(20005,plain,
! [A: $i] :
( ( ( A @ domain @ ( A @ defined ) )
!= ( c @ domain @ ( d @ defined ) ) )
| ( c @ domain @ ( c @ compose ) @ ( h @ defined ) ) ),
inference(simp,[status(thm)],[20004]) ).
thf(20085,plain,
! [A: $i] :
( ( ( A @ domain )
!= ( c @ domain ) )
| ( A != d )
| ( c @ domain @ ( c @ compose ) @ ( h @ defined ) ) ),
inference(simp,[status(thm)],[20005]) ).
thf(20129,plain,
( ( ( d @ domain )
!= ( c @ domain ) )
| ( c @ domain @ ( c @ compose ) @ ( h @ defined ) ) ),
inference(simp,[status(thm)],[20085]) ).
thf(9330,plain,
( ( ( a @ ( a @ ( a @ product ) ) )
!= ( a @ ( h @ compose ) @ ( a @ ( g @ product ) ) ) )
| ~ $true
| ( ( a @ domain )
!= a ) ),
inference(paramod_ordered,[status(thm)],[451,8969]) ).
thf(9331,plain,
( ( ( a @ ( a @ ( a @ product ) ) )
!= ( a @ ( h @ compose ) @ ( a @ ( g @ product ) ) ) )
| ( ( a @ domain )
!= a ) ),
inference(simp,[status(thm)],[9330]) ).
thf(9375,plain,
( ( ( a @ ( h @ compose ) )
!= a )
| ( a != a )
| ( a != g )
| ( ( a @ domain )
!= a ) ),
inference(simp,[status(thm)],[9331]) ).
thf(9392,plain,
( ( ( a @ ( h @ compose ) )
!= a )
| ( a != g )
| ( ( a @ domain )
!= a ) ),
inference(simp,[status(thm)],[9375]) ).
thf(657,plain,
! [A: $i] :
( ( ( a @ ( a @ ( a @ product ) ) )
!= ( A @ ( a @ ( h @ product ) ) ) )
| ~ $true
| ~ ( A @ ( a @ ( g @ product ) ) )
| ( ( a @ domain )
!= a ) ),
inference(paramod_ordered,[status(thm)],[451,315]) ).
thf(658,plain,
! [A: $i] :
( ( ( a @ ( a @ ( a @ product ) ) )
!= ( A @ ( a @ ( h @ product ) ) ) )
| ~ ( A @ ( a @ ( g @ product ) ) )
| ( ( a @ domain )
!= a ) ),
inference(simp,[status(thm)],[657]) ).
thf(675,plain,
! [A: $i] :
( ( a != A )
| ( a != a )
| ( a != h )
| ~ ( A @ ( a @ ( g @ product ) ) )
| ( ( a @ domain )
!= a ) ),
inference(simp,[status(thm)],[658]) ).
thf(679,plain,
( ( a != h )
| ~ ( a @ ( a @ ( g @ product ) ) )
| ( ( a @ domain )
!= a ) ),
inference(simp,[status(thm)],[675]) ).
thf(43896,plain,
! [A: $i] :
( ( ( A @ ( a @ ( a @ product ) ) )
!= ( a @ ( h @ compose ) @ ( a @ ( h @ product ) ) ) )
| ~ $true
| ~ ( A @ ( a @ ( c @ product ) ) ) ),
inference(paramod_ordered,[status(thm)],[8996,697]) ).
thf(43897,plain,
! [A: $i] :
( ( ( A @ ( a @ ( a @ product ) ) )
!= ( a @ ( h @ compose ) @ ( a @ ( h @ product ) ) ) )
| ~ ( A @ ( a @ ( c @ product ) ) ) ),
inference(simp,[status(thm)],[43896]) ).
thf(44162,plain,
! [A: $i] :
( ( A
!= ( a @ ( h @ compose ) ) )
| ( a != a )
| ( a != h )
| ~ ( A @ ( a @ ( c @ product ) ) ) ),
inference(simp,[status(thm)],[43897]) ).
thf(44257,plain,
( ( a != h )
| ~ ( a @ ( h @ compose ) @ ( a @ ( c @ product ) ) ) ),
inference(simp,[status(thm)],[44162]) ).
thf(38381,plain,
( ( d != a )
| ( g @ ( a @ codomain @ defined ) ) ),
inference(simp,[status(thm)],[38373]) ).
thf(1941,plain,
! [A: $i] :
( ( ( A @ ( A @ domain @ ( A @ product ) ) )
!= ( a @ ( a @ ( g @ product ) ) ) )
| ~ $true
| ~ ( a @ ( a @ ( h @ product ) ) ) ),
inference(paramod_ordered,[status(thm)],[48,1051]) ).
thf(1942,plain,
! [A: $i] :
( ( ( A @ ( A @ domain @ ( A @ product ) ) )
!= ( a @ ( a @ ( g @ product ) ) ) )
| ~ ( a @ ( a @ ( h @ product ) ) ) ),
inference(simp,[status(thm)],[1941]) ).
thf(1946,plain,
! [A: $i] :
( ( A != a )
| ( ( A @ domain )
!= a )
| ( A != g )
| ~ ( a @ ( a @ ( h @ product ) ) ) ),
inference(simp,[status(thm)],[1942]) ).
thf(1979,plain,
( ( a != g )
| ( ( g @ domain )
!= a )
| ~ ( a @ ( a @ ( h @ product ) ) ) ),
inference(simp,[status(thm)],[1946]) ).
thf(12738,plain,
! [A: $i] :
( ( ( A @ ( A @ domain @ ( A @ product ) ) )
!= ( a @ ( a @ ( h @ product ) ) ) )
| ( ( a @ ( g @ compose ) )
!= a )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[48,9636]) ).
thf(12739,plain,
! [A: $i] :
( ( ( A @ ( A @ domain @ ( A @ product ) ) )
!= ( a @ ( a @ ( h @ product ) ) ) )
| ( ( a @ ( g @ compose ) )
!= a ) ),
inference(simp,[status(thm)],[12738]) ).
thf(12794,plain,
! [A: $i] :
( ( A != a )
| ( ( A @ domain )
!= a )
| ( A != h )
| ( ( a @ ( g @ compose ) )
!= a ) ),
inference(simp,[status(thm)],[12739]) ).
thf(12831,plain,
( ( a != h )
| ( ( h @ domain )
!= a )
| ( ( a @ ( g @ compose ) )
!= a ) ),
inference(simp,[status(thm)],[12794]) ).
thf(8872,plain,
! [A: $i] :
( ( ( b @ ( a @ defined ) )
!= ( c @ ( A @ defined ) ) )
| ( a @ ( A @ defined ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1281,2218]) ).
thf(8873,plain,
! [A: $i] :
( ( ( b @ ( a @ defined ) )
!= ( c @ ( A @ defined ) ) )
| ( a @ ( A @ defined ) ) ),
inference(simp,[status(thm)],[8872]) ).
thf(8892,plain,
! [A: $i] :
( ( c != b )
| ( a != A )
| ( a @ ( A @ defined ) ) ),
inference(simp,[status(thm)],[8873]) ).
thf(8901,plain,
( ( c != b )
| ( a @ ( a @ defined ) ) ),
inference(simp,[status(thm)],[8892]) ).
thf(10622,plain,
! [B: $i,A: $i] :
( ( ( a @ ( a @ defined ) )
!= ( B @ ( A @ defined ) ) )
| ( B @ ( A @ compose ) @ ( B @ ( A @ product ) ) )
| ~ $true
| ( c != b ) ),
inference(paramod_ordered,[status(thm)],[8901,31]) ).
thf(10623,plain,
! [B: $i,A: $i] :
( ( ( a @ ( a @ defined ) )
!= ( B @ ( A @ defined ) ) )
| ( B @ ( A @ compose ) @ ( B @ ( A @ product ) ) )
| ( c != b ) ),
inference(simp,[status(thm)],[10622]) ).
thf(10624,plain,
( ( a @ ( a @ compose ) @ ( a @ ( a @ product ) ) )
| ( c != b ) ),
inference(pattern_uni,[status(thm)],[10623:[bind(A,$thf( a )),bind(B,$thf( a ))]]) ).
thf(3801,plain,
! [A: $i] :
( ( ( A @ ( A @ ( A @ codomain @ product ) ) )
!= ( a @ ( a @ ( c @ ( g @ compose ) @ product ) ) ) )
| ( a @ codomain @ ( c @ ( g @ product ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[37,1409]) ).
thf(3802,plain,
! [A: $i] :
( ( ( A @ ( A @ ( A @ codomain @ product ) ) )
!= ( a @ ( a @ ( c @ ( g @ compose ) @ product ) ) ) )
| ( a @ codomain @ ( c @ ( g @ product ) ) ) ),
inference(simp,[status(thm)],[3801]) ).
thf(3835,plain,
! [A: $i] :
( ( A != a )
| ( A != a )
| ( ( A @ codomain )
!= ( c @ ( g @ compose ) ) )
| ( a @ codomain @ ( c @ ( g @ product ) ) ) ),
inference(simp,[status(thm)],[3802]) ).
thf(3856,plain,
( ( ( c @ ( g @ compose ) )
!= ( a @ codomain ) )
| ( a @ codomain @ ( c @ ( g @ product ) ) ) ),
inference(simp,[status(thm)],[3835]) ).
thf(19904,plain,
! [A: $i] :
( ( ( A @ ( A @ codomain @ defined ) )
!= ( c @ domain @ ( d @ defined ) ) )
| ( c @ domain @ ( c @ compose ) @ ( h @ defined ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[24,10861]) ).
thf(19905,plain,
! [A: $i] :
( ( ( A @ ( A @ codomain @ defined ) )
!= ( c @ domain @ ( d @ defined ) ) )
| ( c @ domain @ ( c @ compose ) @ ( h @ defined ) ) ),
inference(simp,[status(thm)],[19904]) ).
thf(20075,plain,
! [A: $i] :
( ( A
!= ( c @ domain ) )
| ( ( A @ codomain )
!= d )
| ( c @ domain @ ( c @ compose ) @ ( h @ defined ) ) ),
inference(simp,[status(thm)],[19905]) ).
thf(20125,plain,
( ( ( c @ domain @ codomain )
!= d )
| ( c @ domain @ ( c @ compose ) @ ( h @ defined ) ) ),
inference(simp,[status(thm)],[20075]) ).
thf(13084,plain,
! [A: $i] :
( ( ( d @ ( g @ codomain @ defined ) )
!= ( c @ ( A @ defined ) ) )
| ( a @ ( A @ defined ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[13031,2218]) ).
thf(13085,plain,
! [A: $i] :
( ( ( d @ ( g @ codomain @ defined ) )
!= ( c @ ( A @ defined ) ) )
| ( a @ ( A @ defined ) ) ),
inference(simp,[status(thm)],[13084]) ).
thf(13104,plain,
! [A: $i] :
( ( d != c )
| ( ( g @ codomain )
!= A )
| ( a @ ( A @ defined ) ) ),
inference(simp,[status(thm)],[13085]) ).
thf(13122,plain,
( ( d != c )
| ( a @ ( g @ codomain @ defined ) ) ),
inference(simp,[status(thm)],[13104]) ).
thf(104,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( c @ ( b @ ( a @ product ) ) )
!= ( A @ ( G @ ( F @ product ) ) ) )
| ( H @ ( F @ defined ) )
| ~ ( H @ ( E @ ( G @ product ) ) )
| ~ $true
| ~ ( D @ ( C @ defined ) )
| ~ ( E @ ( D @ ( B @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(paramod_ordered,[status(thm)],[32,82]) ).
thf(105,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( c @ ( b @ ( a @ product ) ) )
!= ( A @ ( G @ ( F @ product ) ) ) )
| ( H @ ( F @ defined ) )
| ~ ( H @ ( E @ ( G @ product ) ) )
| ~ ( D @ ( C @ defined ) )
| ~ ( E @ ( D @ ( B @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[104]) ).
thf(106,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( a @ defined ) )
| ~ ( E @ ( D @ ( b @ product ) ) )
| ~ ( C @ ( B @ defined ) )
| ~ ( D @ ( C @ ( A @ product ) ) )
| ~ ( B @ ( A @ ( c @ product ) ) ) ),
inference(pattern_uni,[status(thm)],[105:[bind(A,$thf( c )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( E )),bind(F,$thf( a )),bind(G,$thf( b ))]]) ).
thf(148,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( a @ defined ) )
| ~ ( E @ ( D @ ( b @ product ) ) )
| ~ ( C @ ( B @ defined ) )
| ~ ( D @ ( C @ ( A @ product ) ) )
| ~ ( B @ ( A @ ( c @ product ) ) ) ),
inference(simp,[status(thm)],[106]) ).
thf(14,axiom,
! [D: $i,C: $i,B: $i,A: $i] :
( ( C = D )
| ~ ( D @ ( B @ ( A @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',composition_is_well_defined) ).
thf(45,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( C = D )
| ~ ( D @ ( B @ ( A @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[14]) ).
thf(122,plain,
! [M: $i,L: $i,K: $i,J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( H @ ( F @ defined ) )
!= ( L @ ( K @ defined ) ) )
| ( M @ ( I @ defined ) )
| ~ $true
| ~ ( M @ ( L @ ( J @ product ) ) )
| ~ ( K @ ( J @ ( I @ product ) ) )
| ~ ( H @ ( E @ ( G @ product ) ) )
| ~ ( A @ ( G @ ( F @ product ) ) )
| ~ ( D @ ( C @ defined ) )
| ~ ( E @ ( D @ ( B @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(paramod_ordered,[status(thm)],[82,26]) ).
thf(123,plain,
! [M: $i,L: $i,K: $i,J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( H @ ( F @ defined ) )
!= ( L @ ( K @ defined ) ) )
| ( M @ ( I @ defined ) )
| ~ ( M @ ( L @ ( J @ product ) ) )
| ~ ( K @ ( J @ ( I @ product ) ) )
| ~ ( H @ ( E @ ( G @ product ) ) )
| ~ ( A @ ( G @ ( F @ product ) ) )
| ~ ( D @ ( C @ defined ) )
| ~ ( E @ ( D @ ( B @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[122]) ).
thf(124,plain,
! [K: $i,J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( K @ ( I @ defined ) )
| ~ ( K @ ( H @ ( J @ product ) ) )
| ~ ( F @ ( J @ ( I @ product ) ) )
| ~ ( H @ ( E @ ( G @ product ) ) )
| ~ ( A @ ( G @ ( F @ product ) ) )
| ~ ( D @ ( C @ defined ) )
| ~ ( E @ ( D @ ( B @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(pattern_uni,[status(thm)],[123:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( E )),bind(F,$thf( F )),bind(G,$thf( G )),bind(H,$thf( H )),bind(I,$thf( I )),bind(J,$thf( J )),bind(K,$thf( F )),bind(L,$thf( H ))]]) ).
thf(161,plain,
! [K: $i,J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( K @ ( I @ defined ) )
| ~ ( K @ ( H @ ( J @ product ) ) )
| ~ ( F @ ( J @ ( I @ product ) ) )
| ~ ( H @ ( E @ ( G @ product ) ) )
| ~ ( A @ ( G @ ( F @ product ) ) )
| ~ ( D @ ( C @ defined ) )
| ~ ( E @ ( D @ ( B @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[124]) ).
thf(14601,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ domain @ ( A @ compose ) @ ( A @ domain @ ( A @ product ) ) )
!= ( C @ ( B @ ( b @ product ) ) ) )
| ( C @ ( a @ defined ) )
| ~ ( B @ ( c @ defined ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[762,85]) ).
thf(14602,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ domain @ ( A @ compose ) @ ( A @ domain @ ( A @ product ) ) )
!= ( C @ ( B @ ( b @ product ) ) ) )
| ( C @ ( a @ defined ) )
| ~ ( B @ ( c @ defined ) ) ),
inference(simp,[status(thm)],[14601]) ).
thf(14603,plain,
( ( b @ domain @ ( b @ compose ) @ ( a @ defined ) )
| ~ ( b @ domain @ ( c @ defined ) ) ),
inference(pattern_uni,[status(thm)],[14602:[bind(A,$thf( b )),bind(B,$thf( b @ domain )),bind(C,$thf( b @ domain @ ( b @ compose ) ))]]) ).
thf(25110,plain,
! [A: $i] :
( ( ( A @ ( A @ codomain @ defined ) )
!= ( b @ domain @ ( c @ defined ) ) )
| ( b @ domain @ ( b @ compose ) @ ( a @ defined ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[24,14603]) ).
thf(25111,plain,
! [A: $i] :
( ( ( A @ ( A @ codomain @ defined ) )
!= ( b @ domain @ ( c @ defined ) ) )
| ( b @ domain @ ( b @ compose ) @ ( a @ defined ) ) ),
inference(simp,[status(thm)],[25110]) ).
thf(25312,plain,
! [A: $i] :
( ( A
!= ( b @ domain ) )
| ( ( A @ codomain )
!= c )
| ( b @ domain @ ( b @ compose ) @ ( a @ defined ) ) ),
inference(simp,[status(thm)],[25111]) ).
thf(25356,plain,
( ( ( b @ domain @ codomain )
!= c )
| ( b @ domain @ ( b @ compose ) @ ( a @ defined ) ) ),
inference(simp,[status(thm)],[25312]) ).
thf(20621,plain,
( ( a != a )
| ( ( c @ codomain )
!= h )
| ( ( c @ codomain )
!= g ) ),
inference(simp,[status(thm)],[10382]) ).
thf(20720,plain,
( ( ( c @ codomain )
!= h )
| ( ( c @ codomain )
!= g ) ),
inference(simp,[status(thm)],[20621]) ).
thf(131,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ $true
| ( ( E @ ( D @ ( B @ product ) ) )
!= ( C @ ( B @ ( A @ product ) ) ) )
| ( H @ ( F @ defined ) )
| ~ ( H @ ( E @ ( G @ product ) ) )
| ~ ( A @ ( G @ ( F @ product ) ) )
| ~ ( D @ ( C @ defined ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(eqfactor_ordered,[status(thm)],[82]) ).
thf(138,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( C @ defined ) )
| ~ ( E @ ( B @ ( D @ product ) ) )
| ~ ( A @ ( D @ ( C @ product ) ) )
| ~ ( A @ ( B @ defined ) )
| ~ ( B @ ( A @ ( A @ product ) ) ) ),
inference(pattern_uni,[status(thm)],[131:[bind(A,$thf( D )),bind(B,$thf( D )),bind(C,$thf( E ))]]) ).
thf(149,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( C @ defined ) )
| ~ ( E @ ( B @ ( D @ product ) ) )
| ~ ( A @ ( D @ ( C @ product ) ) )
| ~ ( A @ ( B @ defined ) )
| ~ ( B @ ( A @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[138]) ).
thf(9472,plain,
! [A: $i] :
( ( ( a @ ( g @ compose ) @ ( a @ ( g @ product ) ) )
!= ( a @ ( a @ ( A @ product ) ) ) )
| ~ $true
| ( ( a @ codomain )
= A ) ),
inference(paramod_ordered,[status(thm)],[8935,297]) ).
thf(9473,plain,
! [A: $i] :
( ( ( a @ ( g @ compose ) @ ( a @ ( g @ product ) ) )
!= ( a @ ( a @ ( A @ product ) ) ) )
| ( ( a @ codomain )
= A ) ),
inference(simp,[status(thm)],[9472]) ).
thf(9597,plain,
! [A: $i] :
( ( ( a @ ( g @ compose ) )
!= a )
| ( a != a )
| ( g != A )
| ( ( a @ codomain )
= A ) ),
inference(simp,[status(thm)],[9473]) ).
thf(9652,plain,
( ( ( a @ ( g @ compose ) )
!= a )
| ( ( a @ codomain )
= g ) ),
inference(simp,[status(thm)],[9597]) ).
thf(29303,plain,
! [A: $i] :
( ( ( c @ ( a @ codomain @ defined ) )
!= ( d @ ( A @ defined ) ) )
| ( g @ ( A @ defined ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[11252,2221]) ).
thf(29304,plain,
! [A: $i] :
( ( ( c @ ( a @ codomain @ defined ) )
!= ( d @ ( A @ defined ) ) )
| ( g @ ( A @ defined ) ) ),
inference(simp,[status(thm)],[29303]) ).
thf(29363,plain,
! [A: $i] :
( ( d != c )
| ( ( a @ codomain )
!= A )
| ( g @ ( A @ defined ) ) ),
inference(simp,[status(thm)],[29304]) ).
thf(29396,plain,
( ( d != c )
| ( g @ ( a @ codomain @ defined ) ) ),
inference(simp,[status(thm)],[29363]) ).
thf(13,axiom,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( B @ ( F @ product ) ) )
| ~ ( F @ ( A @ ( D @ product ) ) )
| ~ ( E @ ( C @ ( D @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',category_theory_axiom5) ).
thf(43,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( B @ ( F @ product ) ) )
| ~ ( F @ ( A @ ( D @ product ) ) )
| ~ ( E @ ( C @ ( D @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[13]) ).
thf(44,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( B @ ( F @ product ) ) )
| ~ ( F @ ( A @ ( D @ product ) ) )
| ~ ( E @ ( C @ ( D @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(cnf,[status(esa)],[43]) ).
thf(25229,plain,
! [A: $i] :
( ( ( A @ domain @ ( A @ defined ) )
!= ( b @ domain @ ( c @ defined ) ) )
| ( b @ domain @ ( b @ compose ) @ ( a @ defined ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[23,14603]) ).
thf(25230,plain,
! [A: $i] :
( ( ( A @ domain @ ( A @ defined ) )
!= ( b @ domain @ ( c @ defined ) ) )
| ( b @ domain @ ( b @ compose ) @ ( a @ defined ) ) ),
inference(simp,[status(thm)],[25229]) ).
thf(25316,plain,
! [A: $i] :
( ( ( A @ domain )
!= ( b @ domain ) )
| ( A != c )
| ( b @ domain @ ( b @ compose ) @ ( a @ defined ) ) ),
inference(simp,[status(thm)],[25230]) ).
thf(25357,plain,
( ( ( c @ domain )
!= ( b @ domain ) )
| ( b @ domain @ ( b @ compose ) @ ( a @ defined ) ) ),
inference(simp,[status(thm)],[25316]) ).
thf(43973,plain,
! [A: $i] :
( ( ( A @ ( a @ ( a @ product ) ) )
!= ( a @ ( g @ compose ) @ ( a @ ( g @ product ) ) ) )
| ~ $true
| ~ ( A @ ( a @ ( c @ product ) ) ) ),
inference(paramod_ordered,[status(thm)],[8935,697]) ).
thf(43974,plain,
! [A: $i] :
( ( ( A @ ( a @ ( a @ product ) ) )
!= ( a @ ( g @ compose ) @ ( a @ ( g @ product ) ) ) )
| ~ ( A @ ( a @ ( c @ product ) ) ) ),
inference(simp,[status(thm)],[43973]) ).
thf(44164,plain,
! [A: $i] :
( ( A
!= ( a @ ( g @ compose ) ) )
| ( a != a )
| ( a != g )
| ~ ( A @ ( a @ ( c @ product ) ) ) ),
inference(simp,[status(thm)],[43974]) ).
thf(44259,plain,
( ( a != g )
| ~ ( a @ ( g @ compose ) @ ( a @ ( c @ product ) ) ) ),
inference(simp,[status(thm)],[44164]) ).
thf(23940,plain,
! [A: $i] :
( ( ( A @ domain @ ( A @ defined ) )
!= ( c @ domain @ ( d @ defined ) ) )
| ( c @ domain @ ( c @ compose ) @ ( g @ defined ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[23,11976]) ).
thf(23941,plain,
! [A: $i] :
( ( ( A @ domain @ ( A @ defined ) )
!= ( c @ domain @ ( d @ defined ) ) )
| ( c @ domain @ ( c @ compose ) @ ( g @ defined ) ) ),
inference(simp,[status(thm)],[23940]) ).
thf(24005,plain,
! [A: $i] :
( ( ( A @ domain )
!= ( c @ domain ) )
| ( A != d )
| ( c @ domain @ ( c @ compose ) @ ( g @ defined ) ) ),
inference(simp,[status(thm)],[23941]) ).
thf(24050,plain,
( ( ( d @ domain )
!= ( c @ domain ) )
| ( c @ domain @ ( c @ compose ) @ ( g @ defined ) ) ),
inference(simp,[status(thm)],[24005]) ).
thf(26604,plain,
( ( d != c )
| ( c @ domain @ ( c @ compose ) @ ( g @ defined ) ) ),
inference(simp,[status(thm)],[24050]) ).
thf(128,plain,
! [P: $i,O: $i,N: $i,M: $i,L: $i,K: $i,J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( H @ ( F @ defined ) )
!= ( L @ ( K @ defined ) ) )
| ( P @ ( N @ defined ) )
| ~ ( P @ ( M @ ( O @ product ) ) )
| ~ ( I @ ( O @ ( N @ product ) ) )
| ~ $true
| ~ ( M @ ( L @ ( J @ product ) ) )
| ~ ( K @ ( J @ ( I @ product ) ) )
| ~ ( H @ ( E @ ( G @ product ) ) )
| ~ ( A @ ( G @ ( F @ product ) ) )
| ~ ( D @ ( C @ defined ) )
| ~ ( E @ ( D @ ( B @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(paramod_ordered,[status(thm)],[82,82]) ).
thf(129,plain,
! [P: $i,O: $i,N: $i,M: $i,L: $i,K: $i,J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( H @ ( F @ defined ) )
!= ( L @ ( K @ defined ) ) )
| ( P @ ( N @ defined ) )
| ~ ( P @ ( M @ ( O @ product ) ) )
| ~ ( I @ ( O @ ( N @ product ) ) )
| ~ ( M @ ( L @ ( J @ product ) ) )
| ~ ( K @ ( J @ ( I @ product ) ) )
| ~ ( H @ ( E @ ( G @ product ) ) )
| ~ ( A @ ( G @ ( F @ product ) ) )
| ~ ( D @ ( C @ defined ) )
| ~ ( E @ ( D @ ( B @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[128]) ).
thf(130,plain,
! [N: $i,M: $i,L: $i,K: $i,J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( N @ ( L @ defined ) )
| ~ ( N @ ( K @ ( M @ product ) ) )
| ~ ( I @ ( M @ ( L @ product ) ) )
| ~ ( K @ ( H @ ( J @ product ) ) )
| ~ ( F @ ( J @ ( I @ product ) ) )
| ~ ( H @ ( E @ ( G @ product ) ) )
| ~ ( A @ ( G @ ( F @ product ) ) )
| ~ ( D @ ( C @ defined ) )
| ~ ( E @ ( D @ ( B @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(pattern_uni,[status(thm)],[129:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( E )),bind(F,$thf( F )),bind(G,$thf( G )),bind(H,$thf( H )),bind(I,$thf( I )),bind(J,$thf( J )),bind(K,$thf( F )),bind(L,$thf( H ))]]) ).
thf(144,plain,
! [N: $i,M: $i,L: $i,K: $i,J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( N @ ( L @ defined ) )
| ~ ( N @ ( K @ ( M @ product ) ) )
| ~ ( I @ ( M @ ( L @ product ) ) )
| ~ ( K @ ( H @ ( J @ product ) ) )
| ~ ( F @ ( J @ ( I @ product ) ) )
| ~ ( H @ ( E @ ( G @ product ) ) )
| ~ ( A @ ( G @ ( F @ product ) ) )
| ~ ( D @ ( C @ defined ) )
| ~ ( E @ ( D @ ( B @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[130]) ).
thf(16,axiom,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( F @ ( A @ product ) ) )
| ~ ( F @ ( D @ ( B @ product ) ) )
| ~ ( E @ ( D @ ( C @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',category_theory_axiom2) ).
thf(49,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( F @ ( A @ product ) ) )
| ~ ( F @ ( D @ ( B @ product ) ) )
| ~ ( E @ ( D @ ( C @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[16]) ).
thf(28107,plain,
( ( c != b )
| ( b @ domain @ ( b @ compose ) @ ( a @ defined ) ) ),
inference(simp,[status(thm)],[25357]) ).
thf(43971,plain,
! [A: $i] :
( ( ( A @ ( a @ ( c @ product ) ) )
!= ( a @ ( g @ compose ) @ ( a @ ( g @ product ) ) ) )
| ~ ( A @ ( a @ ( a @ product ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[8935,697]) ).
thf(43972,plain,
! [A: $i] :
( ( ( A @ ( a @ ( c @ product ) ) )
!= ( a @ ( g @ compose ) @ ( a @ ( g @ product ) ) ) )
| ~ ( A @ ( a @ ( a @ product ) ) ) ),
inference(simp,[status(thm)],[43971]) ).
thf(44122,plain,
! [A: $i] :
( ( A
!= ( a @ ( g @ compose ) ) )
| ( a != a )
| ( c != g )
| ~ ( A @ ( a @ ( a @ product ) ) ) ),
inference(simp,[status(thm)],[43972]) ).
thf(44209,plain,
( ( c != g )
| ~ ( a @ ( g @ compose ) @ ( a @ ( a @ product ) ) ) ),
inference(simp,[status(thm)],[44122]) ).
thf(9812,plain,
( ( ( a @ ( h @ compose ) @ ( a @ ( h @ product ) ) )
!= ( a @ ( a @ ( h @ product ) ) ) )
| ~ ( a @ ( a @ ( g @ product ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[8996,1051]) ).
thf(9813,plain,
( ( ( a @ ( h @ compose ) @ ( a @ ( h @ product ) ) )
!= ( a @ ( a @ ( h @ product ) ) ) )
| ~ ( a @ ( a @ ( g @ product ) ) ) ),
inference(simp,[status(thm)],[9812]) ).
thf(9988,plain,
( ( ( a @ ( h @ compose ) )
!= a )
| ( a != a )
| ( h != h )
| ~ ( a @ ( a @ ( g @ product ) ) ) ),
inference(simp,[status(thm)],[9813]) ).
thf(10009,plain,
( ( ( a @ ( h @ compose ) )
!= a )
| ~ ( a @ ( a @ ( g @ product ) ) ) ),
inference(simp,[status(thm)],[9988]) ).
thf(13636,plain,
! [A: $i] :
( ( ( A @ ( A @ domain @ ( A @ product ) ) )
!= ( a @ ( a @ ( g @ product ) ) ) )
| ( ( a @ ( h @ compose ) )
!= a )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[48,10009]) ).
thf(13637,plain,
! [A: $i] :
( ( ( A @ ( A @ domain @ ( A @ product ) ) )
!= ( a @ ( a @ ( g @ product ) ) ) )
| ( ( a @ ( h @ compose ) )
!= a ) ),
inference(simp,[status(thm)],[13636]) ).
thf(13692,plain,
! [A: $i] :
( ( A != a )
| ( ( A @ domain )
!= a )
| ( A != g )
| ( ( a @ ( h @ compose ) )
!= a ) ),
inference(simp,[status(thm)],[13637]) ).
thf(13730,plain,
( ( a != g )
| ( ( g @ domain )
!= a )
| ( ( a @ ( h @ compose ) )
!= a ) ),
inference(simp,[status(thm)],[13692]) ).
thf(9287,plain,
! [A: $i] :
( ( ( A @ domain @ ( A @ compose ) @ ( A @ domain @ ( A @ product ) ) )
!= ( a @ ( h @ compose ) @ ( a @ ( g @ product ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[762,8969]) ).
thf(9288,plain,
! [A: $i] :
( ( A @ domain @ ( A @ compose ) @ ( A @ domain @ ( A @ product ) ) )
!= ( a @ ( h @ compose ) @ ( a @ ( g @ product ) ) ) ),
inference(simp,[status(thm)],[9287]) ).
thf(9369,plain,
! [A: $i] :
( ( ( A @ domain @ ( A @ compose ) )
!= ( a @ ( h @ compose ) ) )
| ( ( A @ domain )
!= a )
| ( A != g ) ),
inference(simp,[status(thm)],[9288]) ).
thf(9390,plain,
( ( ( g @ domain @ ( g @ compose ) )
!= ( a @ ( h @ compose ) ) )
| ( ( g @ domain )
!= a ) ),
inference(simp,[status(thm)],[9369]) ).
thf(119,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( d @ ( c @ ( h @ product ) ) )
!= ( H @ ( E @ ( G @ product ) ) ) )
| ( H @ ( F @ defined ) )
| ~ $true
| ~ ( A @ ( G @ ( F @ product ) ) )
| ~ ( D @ ( C @ defined ) )
| ~ ( E @ ( D @ ( B @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(paramod_ordered,[status(thm)],[54,82]) ).
thf(120,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( d @ ( c @ ( h @ product ) ) )
!= ( H @ ( E @ ( G @ product ) ) ) )
| ( H @ ( F @ defined ) )
| ~ ( A @ ( G @ ( F @ product ) ) )
| ~ ( D @ ( C @ defined ) )
| ~ ( E @ ( D @ ( B @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[119]) ).
thf(121,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( d @ ( E @ defined ) )
| ~ ( A @ ( h @ ( E @ product ) ) )
| ~ ( D @ ( C @ defined ) )
| ~ ( c @ ( D @ ( B @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(pattern_uni,[status(thm)],[120:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( c )),bind(F,$thf( F )),bind(G,$thf( h )),bind(H,$thf( d ))]]) ).
thf(159,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( d @ ( E @ defined ) )
| ~ ( A @ ( h @ ( E @ product ) ) )
| ~ ( D @ ( C @ defined ) )
| ~ ( c @ ( D @ ( B @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[121]) ).
thf(43986,plain,
! [A: $i] :
( ( ( c @ ( b @ ( a @ product ) ) )
!= ( A @ ( a @ ( a @ product ) ) ) )
| ~ $true
| ~ ( A @ ( a @ ( c @ product ) ) ) ),
inference(paramod_ordered,[status(thm)],[32,697]) ).
thf(43987,plain,
! [A: $i] :
( ( ( c @ ( b @ ( a @ product ) ) )
!= ( A @ ( a @ ( a @ product ) ) ) )
| ~ ( A @ ( a @ ( c @ product ) ) ) ),
inference(simp,[status(thm)],[43986]) ).
thf(44117,plain,
! [A: $i] :
( ( c != A )
| ( b != a )
| ( a != a )
| ~ ( A @ ( a @ ( c @ product ) ) ) ),
inference(simp,[status(thm)],[43987]) ).
thf(44204,plain,
( ( b != a )
| ~ ( c @ ( a @ ( c @ product ) ) ) ),
inference(simp,[status(thm)],[44117]) ).
thf(1079,plain,
( ( ( a @ codomain )
!= ( a @ codomain ) )
| ( ( a @ codomain )
!= g )
| ( a != h )
| ( ( a @ domain )
!= a ) ),
inference(paramod_ordered,[status(thm)],[429,1046]) ).
thf(1080,plain,
( ( ( a @ codomain )
!= g )
| ( a != h )
| ( ( a @ domain )
!= a ) ),
inference(pattern_uni,[status(thm)],[1079:[]]) ).
thf(31539,plain,
! [B: $i,A: $i] :
( ( ( g @ ( g @ defined ) )
!= ( B @ ( A @ defined ) ) )
| ( B @ ( A @ compose ) @ ( B @ ( A @ product ) ) )
| ~ $true
| ( d != a ) ),
inference(paramod_ordered,[status(thm)],[29371,31]) ).
thf(31540,plain,
! [B: $i,A: $i] :
( ( ( g @ ( g @ defined ) )
!= ( B @ ( A @ defined ) ) )
| ( B @ ( A @ compose ) @ ( B @ ( A @ product ) ) )
| ( d != a ) ),
inference(simp,[status(thm)],[31539]) ).
thf(31541,plain,
( ( g @ ( g @ compose ) @ ( g @ ( g @ product ) ) )
| ( d != a ) ),
inference(pattern_uni,[status(thm)],[31540:[bind(A,$thf( g )),bind(B,$thf( g ))]]) ).
thf(45161,plain,
! [A: $i] :
( ( ( A @ ( A @ domain @ ( A @ product ) ) )
!= ( c @ ( a @ ( c @ product ) ) ) )
| ( b != a )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[48,44204]) ).
thf(45162,plain,
! [A: $i] :
( ( ( A @ ( A @ domain @ ( A @ product ) ) )
!= ( c @ ( a @ ( c @ product ) ) ) )
| ( b != a ) ),
inference(simp,[status(thm)],[45161]) ).
thf(45233,plain,
! [A: $i] :
( ( A != c )
| ( ( A @ domain )
!= a )
| ( A != c )
| ( b != a ) ),
inference(simp,[status(thm)],[45162]) ).
thf(45275,plain,
( ( ( c @ domain )
!= a )
| ( b != a ) ),
inference(simp,[status(thm)],[45233]) ).
thf(868,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ codomain @ compose ) @ ( A @ ( A @ codomain @ product ) ) )
!= ( B @ ( a @ ( g @ product ) ) ) )
| ~ ( B @ ( a @ ( h @ product ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[766,315]) ).
thf(869,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ codomain @ compose ) @ ( A @ ( A @ codomain @ product ) ) )
!= ( B @ ( a @ ( g @ product ) ) ) )
| ~ ( B @ ( a @ ( h @ product ) ) ) ),
inference(simp,[status(thm)],[868]) ).
thf(894,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ codomain @ compose ) )
!= B )
| ( A != a )
| ( ( A @ codomain )
!= g )
| ~ ( B @ ( a @ ( h @ product ) ) ) ),
inference(simp,[status(thm)],[869]) ).
thf(915,plain,
( ( ( a @ codomain )
!= g )
| ~ ( a @ ( a @ codomain @ compose ) @ ( a @ ( h @ product ) ) ) ),
inference(simp,[status(thm)],[894]) ).
thf(110,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( d @ ( c @ ( h @ product ) ) )
!= ( C @ ( B @ ( A @ product ) ) ) )
| ( H @ ( F @ defined ) )
| ~ ( H @ ( E @ ( G @ product ) ) )
| ~ ( A @ ( G @ ( F @ product ) ) )
| ~ ( D @ ( C @ defined ) )
| ~ ( E @ ( D @ ( B @ product ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[54,82]) ).
thf(111,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( d @ ( c @ ( h @ product ) ) )
!= ( C @ ( B @ ( A @ product ) ) ) )
| ( H @ ( F @ defined ) )
| ~ ( H @ ( E @ ( G @ product ) ) )
| ~ ( A @ ( G @ ( F @ product ) ) )
| ~ ( D @ ( C @ defined ) )
| ~ ( E @ ( D @ ( B @ product ) ) ) ),
inference(simp,[status(thm)],[110]) ).
thf(112,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( C @ defined ) )
| ~ ( E @ ( B @ ( D @ product ) ) )
| ~ ( h @ ( D @ ( C @ product ) ) )
| ~ ( A @ ( d @ defined ) )
| ~ ( B @ ( A @ ( c @ product ) ) ) ),
inference(pattern_uni,[status(thm)],[111:[bind(A,$thf( h )),bind(B,$thf( c )),bind(C,$thf( d ))]]) ).
thf(155,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( C @ defined ) )
| ~ ( E @ ( B @ ( D @ product ) ) )
| ~ ( h @ ( D @ ( C @ product ) ) )
| ~ ( A @ ( d @ defined ) )
| ~ ( B @ ( A @ ( c @ product ) ) ) ),
inference(simp,[status(thm)],[112]) ).
thf(12204,plain,
! [A: $i] :
( ( ( d @ ( h @ codomain @ defined ) )
!= ( c @ ( A @ defined ) ) )
| ( a @ ( A @ defined ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[12151,2218]) ).
thf(12205,plain,
! [A: $i] :
( ( ( d @ ( h @ codomain @ defined ) )
!= ( c @ ( A @ defined ) ) )
| ( a @ ( A @ defined ) ) ),
inference(simp,[status(thm)],[12204]) ).
thf(12225,plain,
! [A: $i] :
( ( d != c )
| ( ( h @ codomain )
!= A )
| ( a @ ( A @ defined ) ) ),
inference(simp,[status(thm)],[12205]) ).
thf(12230,plain,
( ( d != c )
| ( a @ ( h @ codomain @ defined ) ) ),
inference(simp,[status(thm)],[12225]) ).
thf(12585,plain,
! [B: $i,A: $i] :
( ( ( a @ ( h @ codomain @ defined ) )
!= ( B @ ( A @ defined ) ) )
| ( B @ ( A @ compose ) @ ( B @ ( A @ product ) ) )
| ~ $true
| ( d != c ) ),
inference(paramod_ordered,[status(thm)],[12230,31]) ).
thf(12586,plain,
! [B: $i,A: $i] :
( ( ( a @ ( h @ codomain @ defined ) )
!= ( B @ ( A @ defined ) ) )
| ( B @ ( A @ compose ) @ ( B @ ( A @ product ) ) )
| ( d != c ) ),
inference(simp,[status(thm)],[12585]) ).
thf(12587,plain,
( ( a @ ( h @ codomain @ compose ) @ ( a @ ( h @ codomain @ product ) ) )
| ( d != c ) ),
inference(pattern_uni,[status(thm)],[12586:[bind(A,$thf( h @ codomain )),bind(B,$thf( a ))]]) ).
thf(33131,plain,
! [B: $i,A: $i] :
( ( ( g @ ( a @ codomain @ defined ) )
!= ( B @ ( A @ defined ) ) )
| ( B @ ( A @ compose ) @ ( B @ ( A @ product ) ) )
| ~ $true
| ( d != c ) ),
inference(paramod_ordered,[status(thm)],[29396,31]) ).
thf(33132,plain,
! [B: $i,A: $i] :
( ( ( g @ ( a @ codomain @ defined ) )
!= ( B @ ( A @ defined ) ) )
| ( B @ ( A @ compose ) @ ( B @ ( A @ product ) ) )
| ( d != c ) ),
inference(simp,[status(thm)],[33131]) ).
thf(33133,plain,
( ( g @ ( a @ codomain @ compose ) @ ( g @ ( a @ codomain @ product ) ) )
| ( d != c ) ),
inference(pattern_uni,[status(thm)],[33132:[bind(A,$thf( a @ codomain )),bind(B,$thf( g ))]]) ).
thf(43892,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ ( A @ codomain @ product ) ) )
!= ( B @ ( a @ ( a @ product ) ) ) )
| ~ $true
| ~ ( B @ ( a @ ( c @ product ) ) ) ),
inference(paramod_ordered,[status(thm)],[37,697]) ).
thf(43893,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ ( A @ codomain @ product ) ) )
!= ( B @ ( a @ ( a @ product ) ) ) )
| ~ ( B @ ( a @ ( c @ product ) ) ) ),
inference(simp,[status(thm)],[43892]) ).
thf(44158,plain,
! [B: $i,A: $i] :
( ( A != B )
| ( A != a )
| ( ( A @ codomain )
!= a )
| ~ ( B @ ( a @ ( c @ product ) ) ) ),
inference(simp,[status(thm)],[43893]) ).
thf(44253,plain,
( ( ( a @ codomain )
!= a )
| ~ ( a @ ( a @ ( c @ product ) ) ) ),
inference(simp,[status(thm)],[44158]) ).
thf(45090,plain,
( ( ( c @ ( a @ ( c @ product ) ) )
!= ( a @ ( h @ compose ) @ ( a @ ( h @ product ) ) ) )
| ( b != a )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[8996,44204]) ).
thf(45091,plain,
( ( ( c @ ( a @ ( c @ product ) ) )
!= ( a @ ( h @ compose ) @ ( a @ ( h @ product ) ) ) )
| ( b != a ) ),
inference(simp,[status(thm)],[45090]) ).
thf(45204,plain,
( ( ( a @ ( h @ compose ) )
!= c )
| ( a != a )
| ( c != h )
| ( b != a ) ),
inference(simp,[status(thm)],[45091]) ).
thf(45249,plain,
( ( ( a @ ( h @ compose ) )
!= c )
| ( c != h )
| ( b != a ) ),
inference(simp,[status(thm)],[45204]) ).
thf(9,axiom,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( E @ defined ) )
| ~ ( C @ ( D @ defined ) )
| ~ ( E @ ( A @ ( D @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',category_theory_axiom4) ).
thf(35,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( E @ defined ) )
| ~ ( C @ ( D @ defined ) )
| ~ ( E @ ( A @ ( D @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).
thf(13804,plain,
! [B: $i,A: $i] :
( ( ( a @ ( c @ codomain @ defined ) )
!= ( A @ ( B @ defined ) ) )
| ( B @ ( A @ defined ) )
| ~ $true
| ~ ( B @ ( A @ ( A @ product ) ) ) ),
inference(paramod_ordered,[status(thm)],[8868,84]) ).
thf(13805,plain,
! [B: $i,A: $i] :
( ( ( a @ ( c @ codomain @ defined ) )
!= ( A @ ( B @ defined ) ) )
| ( B @ ( A @ defined ) )
| ~ ( B @ ( A @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[13804]) ).
thf(13806,plain,
( ( c @ codomain @ ( a @ defined ) )
| ~ ( c @ codomain @ ( a @ ( a @ product ) ) ) ),
inference(pattern_uni,[status(thm)],[13805:[bind(A,$thf( a )),bind(B,$thf( c @ codomain ))]]) ).
thf(92,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( d @ ( c @ ( g @ product ) ) )
!= ( A @ ( G @ ( F @ product ) ) ) )
| ( H @ ( F @ defined ) )
| ~ ( H @ ( E @ ( G @ product ) ) )
| ~ $true
| ~ ( D @ ( C @ defined ) )
| ~ ( E @ ( D @ ( B @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(paramod_ordered,[status(thm)],[53,82]) ).
thf(93,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( d @ ( c @ ( g @ product ) ) )
!= ( A @ ( G @ ( F @ product ) ) ) )
| ( H @ ( F @ defined ) )
| ~ ( H @ ( E @ ( G @ product ) ) )
| ~ ( D @ ( C @ defined ) )
| ~ ( E @ ( D @ ( B @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[92]) ).
thf(94,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( g @ defined ) )
| ~ ( E @ ( D @ ( c @ product ) ) )
| ~ ( C @ ( B @ defined ) )
| ~ ( D @ ( C @ ( A @ product ) ) )
| ~ ( B @ ( A @ ( d @ product ) ) ) ),
inference(pattern_uni,[status(thm)],[93:[bind(A,$thf( d )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( E )),bind(F,$thf( g )),bind(G,$thf( c ))]]) ).
thf(162,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( g @ defined ) )
| ~ ( E @ ( D @ ( c @ product ) ) )
| ~ ( C @ ( B @ defined ) )
| ~ ( D @ ( C @ ( A @ product ) ) )
| ~ ( B @ ( A @ ( d @ product ) ) ) ),
inference(simp,[status(thm)],[94]) ).
thf(51372,plain,
( ( ( a @ ( g @ compose ) @ ( a @ ( a @ product ) ) )
!= ( a @ ( g @ compose ) @ ( a @ ( g @ product ) ) ) )
| ( c != g )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[8935,44209]) ).
thf(51373,plain,
( ( ( a @ ( g @ compose ) @ ( a @ ( a @ product ) ) )
!= ( a @ ( g @ compose ) @ ( a @ ( g @ product ) ) ) )
| ( c != g ) ),
inference(simp,[status(thm)],[51372]) ).
thf(51450,plain,
( ( ( a @ ( g @ compose ) )
!= ( a @ ( g @ compose ) ) )
| ( a != a )
| ( a != g )
| ( c != g ) ),
inference(simp,[status(thm)],[51373]) ).
thf(51532,plain,
( ( a != g )
| ( c != g ) ),
inference(simp,[status(thm)],[51450]) ).
thf(44019,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ domain @ ( A @ product ) ) )
!= ( B @ ( a @ ( c @ product ) ) ) )
| ~ ( B @ ( a @ ( a @ product ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[48,697]) ).
thf(44020,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ domain @ ( A @ product ) ) )
!= ( B @ ( a @ ( c @ product ) ) ) )
| ~ ( B @ ( a @ ( a @ product ) ) ) ),
inference(simp,[status(thm)],[44019]) ).
thf(44098,plain,
! [B: $i,A: $i] :
( ( A != B )
| ( ( A @ domain )
!= a )
| ( A != c )
| ~ ( B @ ( a @ ( a @ product ) ) ) ),
inference(simp,[status(thm)],[44020]) ).
thf(44185,plain,
( ( ( c @ domain )
!= a )
| ~ ( c @ ( a @ ( a @ product ) ) ) ),
inference(simp,[status(thm)],[44098]) ).
thf(11293,plain,
( ( ( a @ codomain )
!= ( a @ codomain ) )
| ( c @ ( a @ defined ) )
| ( ( a @ domain )
!= a ) ),
inference(paramod_ordered,[status(thm)],[429,11252]) ).
thf(11294,plain,
( ( c @ ( a @ defined ) )
| ( ( a @ domain )
!= a ) ),
inference(pattern_uni,[status(thm)],[11293:[]]) ).
thf(11677,plain,
! [B: $i,A: $i] :
( ( ( c @ ( a @ defined ) )
!= ( B @ ( A @ defined ) ) )
| ( B @ ( A @ compose ) @ ( B @ ( A @ product ) ) )
| ~ $true
| ( ( a @ domain )
!= a ) ),
inference(paramod_ordered,[status(thm)],[11294,31]) ).
thf(11678,plain,
! [B: $i,A: $i] :
( ( ( c @ ( a @ defined ) )
!= ( B @ ( A @ defined ) ) )
| ( B @ ( A @ compose ) @ ( B @ ( A @ product ) ) )
| ( ( a @ domain )
!= a ) ),
inference(simp,[status(thm)],[11677]) ).
thf(11679,plain,
( ( c @ ( a @ compose ) @ ( c @ ( a @ product ) ) )
| ( ( a @ domain )
!= a ) ),
inference(pattern_uni,[status(thm)],[11678:[bind(A,$thf( a )),bind(B,$thf( c ))]]) ).
thf(98,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( c @ ( b @ ( a @ product ) ) )
!= ( C @ ( B @ ( A @ product ) ) ) )
| ( H @ ( F @ defined ) )
| ~ ( H @ ( E @ ( G @ product ) ) )
| ~ ( A @ ( G @ ( F @ product ) ) )
| ~ ( D @ ( C @ defined ) )
| ~ ( E @ ( D @ ( B @ product ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[32,82]) ).
thf(99,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( c @ ( b @ ( a @ product ) ) )
!= ( C @ ( B @ ( A @ product ) ) ) )
| ( H @ ( F @ defined ) )
| ~ ( H @ ( E @ ( G @ product ) ) )
| ~ ( A @ ( G @ ( F @ product ) ) )
| ~ ( D @ ( C @ defined ) )
| ~ ( E @ ( D @ ( B @ product ) ) ) ),
inference(simp,[status(thm)],[98]) ).
thf(100,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( C @ defined ) )
| ~ ( E @ ( B @ ( D @ product ) ) )
| ~ ( a @ ( D @ ( C @ product ) ) )
| ~ ( A @ ( c @ defined ) )
| ~ ( B @ ( A @ ( b @ product ) ) ) ),
inference(pattern_uni,[status(thm)],[99:[bind(A,$thf( a )),bind(B,$thf( b )),bind(C,$thf( c ))]]) ).
thf(145,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( C @ defined ) )
| ~ ( E @ ( B @ ( D @ product ) ) )
| ~ ( a @ ( D @ ( C @ product ) ) )
| ~ ( A @ ( c @ defined ) )
| ~ ( B @ ( A @ ( b @ product ) ) ) ),
inference(simp,[status(thm)],[100]) ).
thf(56546,plain,
( ( ( a @ ( a @ defined ) )
!= ( a @ ( h @ defined ) ) )
| ~ ( a @ ( a @ compose ) @ ( a @ ( c @ product ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[8876,44046]) ).
thf(56547,plain,
( ( ( a @ ( a @ defined ) )
!= ( a @ ( h @ defined ) ) )
| ~ ( a @ ( a @ compose ) @ ( a @ ( c @ product ) ) ) ),
inference(simp,[status(thm)],[56546]) ).
thf(56603,plain,
( ( a != a )
| ( a != h )
| ~ ( a @ ( a @ compose ) @ ( a @ ( c @ product ) ) ) ),
inference(simp,[status(thm)],[56547]) ).
thf(56681,plain,
( ( a != h )
| ~ ( a @ ( a @ compose ) @ ( a @ ( c @ product ) ) ) ),
inference(simp,[status(thm)],[56603]) ).
thf(54955,plain,
! [A: $i] :
( ( ( A @ ( A @ ( A @ codomain @ product ) ) )
!= ( a @ ( a @ ( a @ ( h @ compose ) @ product ) ) ) )
| ( a @ codomain @ ( a @ ( h @ product ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[37,9885]) ).
thf(54956,plain,
! [A: $i] :
( ( ( A @ ( A @ ( A @ codomain @ product ) ) )
!= ( a @ ( a @ ( a @ ( h @ compose ) @ product ) ) ) )
| ( a @ codomain @ ( a @ ( h @ product ) ) ) ),
inference(simp,[status(thm)],[54955]) ).
thf(55099,plain,
! [A: $i] :
( ( A != a )
| ( A != a )
| ( ( A @ codomain )
!= ( a @ ( h @ compose ) ) )
| ( a @ codomain @ ( a @ ( h @ product ) ) ) ),
inference(simp,[status(thm)],[54956]) ).
thf(55146,plain,
( ( ( a @ ( h @ compose ) )
!= ( a @ codomain ) )
| ( a @ codomain @ ( a @ ( h @ product ) ) ) ),
inference(simp,[status(thm)],[55099]) ).
thf(29486,plain,
! [A: $i] :
( ( ( g @ ( d @ codomain @ defined ) )
!= ( c @ ( A @ defined ) ) )
| ( a @ ( A @ defined ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[29250,2218]) ).
thf(29487,plain,
! [A: $i] :
( ( ( g @ ( d @ codomain @ defined ) )
!= ( c @ ( A @ defined ) ) )
| ( a @ ( A @ defined ) ) ),
inference(simp,[status(thm)],[29486]) ).
thf(29524,plain,
! [A: $i] :
( ( c != g )
| ( ( d @ codomain )
!= A )
| ( a @ ( A @ defined ) ) ),
inference(simp,[status(thm)],[29487]) ).
thf(29546,plain,
( ( c != g )
| ( a @ ( d @ codomain @ defined ) ) ),
inference(simp,[status(thm)],[29524]) ).
thf(33421,plain,
! [B: $i,A: $i] :
( ( ( a @ ( d @ codomain @ defined ) )
!= ( B @ ( A @ defined ) ) )
| ( B @ ( A @ compose ) @ ( B @ ( A @ product ) ) )
| ~ $true
| ( c != g ) ),
inference(paramod_ordered,[status(thm)],[29546,31]) ).
thf(33422,plain,
! [B: $i,A: $i] :
( ( ( a @ ( d @ codomain @ defined ) )
!= ( B @ ( A @ defined ) ) )
| ( B @ ( A @ compose ) @ ( B @ ( A @ product ) ) )
| ( c != g ) ),
inference(simp,[status(thm)],[33421]) ).
thf(33423,plain,
( ( a @ ( d @ codomain @ compose ) @ ( a @ ( d @ codomain @ product ) ) )
| ( c != g ) ),
inference(pattern_uni,[status(thm)],[33422:[bind(A,$thf( d @ codomain )),bind(B,$thf( a ))]]) ).
thf(132,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ $true
| ( ( A @ ( G @ ( F @ product ) ) )
!= ( C @ ( B @ ( A @ product ) ) ) )
| ( H @ ( F @ defined ) )
| ~ ( H @ ( E @ ( G @ product ) ) )
| ~ ( D @ ( C @ defined ) )
| ~ ( E @ ( D @ ( B @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(eqfactor_ordered,[status(thm)],[82]) ).
thf(139,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( C @ defined ) )
| ~ ( E @ ( B @ ( D @ product ) ) )
| ~ ( A @ ( C @ defined ) )
| ~ ( B @ ( A @ ( D @ product ) ) )
| ~ ( C @ ( D @ ( C @ product ) ) ) ),
inference(pattern_uni,[status(thm)],[132:[bind(A,$thf( F )),bind(B,$thf( G )),bind(C,$thf( F ))]]) ).
thf(150,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( C @ defined ) )
| ~ ( E @ ( B @ ( D @ product ) ) )
| ~ ( A @ ( C @ defined ) )
| ~ ( B @ ( A @ ( D @ product ) ) )
| ~ ( C @ ( D @ ( C @ product ) ) ) ),
inference(simp,[status(thm)],[139]) ).
thf(886,plain,
! [A: $i] :
( ( ( a @ codomain )
!= ( A @ codomain ) )
| ( A @ ( a @ compose ) @ ( A @ ( A @ codomain @ product ) ) )
| ( ( a @ domain )
!= a ) ),
inference(paramod_ordered,[status(thm)],[429,766]) ).
thf(887,plain,
( ( a @ ( a @ compose ) @ ( a @ ( a @ codomain @ product ) ) )
| ( ( a @ domain )
!= a ) ),
inference(pattern_uni,[status(thm)],[886:[bind(A,$thf( a ))]]) ).
thf(26168,plain,
( ( d != c )
| ( c @ domain @ ( c @ compose ) @ ( h @ defined ) ) ),
inference(simp,[status(thm)],[20129]) ).
thf(10273,plain,
! [A: $i] :
( ( ( a @ ( c @ codomain @ compose ) @ ( a @ ( c @ codomain @ product ) ) )
!= ( A @ ( a @ ( g @ product ) ) ) )
| ~ ( A @ ( a @ ( h @ product ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[9065,315]) ).
thf(10274,plain,
! [A: $i] :
( ( ( a @ ( c @ codomain @ compose ) @ ( a @ ( c @ codomain @ product ) ) )
!= ( A @ ( a @ ( g @ product ) ) ) )
| ~ ( A @ ( a @ ( h @ product ) ) ) ),
inference(simp,[status(thm)],[10273]) ).
thf(10332,plain,
! [A: $i] :
( ( ( a @ ( c @ codomain @ compose ) )
!= A )
| ( a != a )
| ( ( c @ codomain )
!= g )
| ~ ( A @ ( a @ ( h @ product ) ) ) ),
inference(simp,[status(thm)],[10274]) ).
thf(10392,plain,
( ( ( c @ codomain )
!= g )
| ~ ( a @ ( c @ codomain @ compose ) @ ( a @ ( h @ product ) ) ) ),
inference(simp,[status(thm)],[10332]) ).
thf(50,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( F @ ( A @ product ) ) )
| ~ ( F @ ( D @ ( B @ product ) ) )
| ~ ( E @ ( D @ ( C @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(cnf,[status(esa)],[49]) ).
thf(43977,plain,
! [A: $i] :
( ( ( a @ ( a @ compose ) @ ( a @ ( a @ product ) ) )
!= ( A @ ( a @ ( a @ product ) ) ) )
| ~ $true
| ~ ( A @ ( a @ ( c @ product ) ) )
| ( c != b ) ),
inference(paramod_ordered,[status(thm)],[10624,697]) ).
thf(43978,plain,
! [A: $i] :
( ( ( a @ ( a @ compose ) @ ( a @ ( a @ product ) ) )
!= ( A @ ( a @ ( a @ product ) ) ) )
| ~ ( A @ ( a @ ( c @ product ) ) )
| ( c != b ) ),
inference(simp,[status(thm)],[43977]) ).
thf(43979,plain,
( ~ ( a @ ( a @ compose ) @ ( a @ ( c @ product ) ) )
| ( c != b ) ),
inference(pattern_uni,[status(thm)],[43978:[bind(A,$thf( a @ ( a @ compose ) ))]]) ).
thf(9171,plain,
( ( ( c @ ( b @ ( a @ product ) ) )
!= ( a @ ( g @ compose ) @ ( a @ ( h @ product ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[32,8906]) ).
thf(9172,plain,
( ( c @ ( b @ ( a @ product ) ) )
!= ( a @ ( g @ compose ) @ ( a @ ( h @ product ) ) ) ),
inference(simp,[status(thm)],[9171]) ).
thf(9214,plain,
( ( ( a @ ( g @ compose ) )
!= c )
| ( b != a )
| ( a != h ) ),
inference(simp,[status(thm)],[9172]) ).
thf(9538,plain,
( ( ( a @ ( g @ compose ) @ ( a @ ( g @ product ) ) )
!= ( a @ ( h @ compose ) @ ( a @ ( g @ product ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[8935,8969]) ).
thf(9539,plain,
( ( a @ ( g @ compose ) @ ( a @ ( g @ product ) ) )
!= ( a @ ( h @ compose ) @ ( a @ ( g @ product ) ) ) ),
inference(simp,[status(thm)],[9538]) ).
thf(9581,plain,
( ( ( a @ ( g @ compose ) )
!= ( a @ ( h @ compose ) ) )
| ( a != a )
| ( g != g ) ),
inference(simp,[status(thm)],[9539]) ).
thf(9634,plain,
( ( a @ ( g @ compose ) )
!= ( a @ ( h @ compose ) ) ),
inference(simp,[status(thm)],[9581]) ).
thf(56329,plain,
! [A: $i] :
( ( ( A @ ( A @ codomain @ defined ) )
!= ( a @ ( a @ defined ) ) )
| ~ ( a @ ( a @ compose ) @ ( a @ ( c @ product ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[24,44046]) ).
thf(56330,plain,
! [A: $i] :
( ( ( A @ ( A @ codomain @ defined ) )
!= ( a @ ( a @ defined ) ) )
| ~ ( a @ ( a @ compose ) @ ( a @ ( c @ product ) ) ) ),
inference(simp,[status(thm)],[56329]) ).
thf(56656,plain,
! [A: $i] :
( ( A != a )
| ( ( A @ codomain )
!= a )
| ~ ( a @ ( a @ compose ) @ ( a @ ( c @ product ) ) ) ),
inference(simp,[status(thm)],[56330]) ).
thf(56709,plain,
( ( ( a @ codomain )
!= a )
| ~ ( a @ ( a @ compose ) @ ( a @ ( c @ product ) ) ) ),
inference(simp,[status(thm)],[56656]) ).
thf(45138,plain,
( ( ( c @ ( a @ ( c @ product ) ) )
!= ( a @ ( g @ compose ) @ ( a @ ( g @ product ) ) ) )
| ( b != a )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[8935,44204]) ).
thf(45139,plain,
( ( ( c @ ( a @ ( c @ product ) ) )
!= ( a @ ( g @ compose ) @ ( a @ ( g @ product ) ) ) )
| ( b != a ) ),
inference(simp,[status(thm)],[45138]) ).
thf(45223,plain,
( ( ( a @ ( g @ compose ) )
!= c )
| ( a != a )
| ( c != g )
| ( b != a ) ),
inference(simp,[status(thm)],[45139]) ).
thf(45262,plain,
( ( ( a @ ( g @ compose ) )
!= c )
| ( c != g )
| ( b != a ) ),
inference(simp,[status(thm)],[45223]) ).
thf(9878,plain,
! [A: $i] :
( ( ( a @ ( h @ compose ) @ ( a @ ( h @ product ) ) )
!= ( a @ ( a @ ( A @ product ) ) ) )
| ~ $true
| ( ( a @ codomain )
= A ) ),
inference(paramod_ordered,[status(thm)],[8996,297]) ).
thf(9879,plain,
! [A: $i] :
( ( ( a @ ( h @ compose ) @ ( a @ ( h @ product ) ) )
!= ( a @ ( a @ ( A @ product ) ) ) )
| ( ( a @ codomain )
= A ) ),
inference(simp,[status(thm)],[9878]) ).
thf(9998,plain,
! [A: $i] :
( ( ( a @ ( h @ compose ) )
!= a )
| ( a != a )
| ( h != A )
| ( ( a @ codomain )
= A ) ),
inference(simp,[status(thm)],[9879]) ).
thf(10023,plain,
( ( ( a @ ( h @ compose ) )
!= a )
| ( ( a @ codomain )
= h ) ),
inference(simp,[status(thm)],[9998]) ).
thf(54430,plain,
! [A: $i] :
( ( ( A @ ( A @ codomain @ defined ) )
!= ( a @ ( c @ defined ) ) )
| ~ ( a @ ( c @ compose ) @ ( a @ ( a @ product ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[24,44043]) ).
thf(54431,plain,
! [A: $i] :
( ( ( A @ ( A @ codomain @ defined ) )
!= ( a @ ( c @ defined ) ) )
| ~ ( a @ ( c @ compose ) @ ( a @ ( a @ product ) ) ) ),
inference(simp,[status(thm)],[54430]) ).
thf(54755,plain,
! [A: $i] :
( ( A != a )
| ( ( A @ codomain )
!= c )
| ~ ( a @ ( c @ compose ) @ ( a @ ( a @ product ) ) ) ),
inference(simp,[status(thm)],[54431]) ).
thf(54824,plain,
( ( ( a @ codomain )
!= c )
| ~ ( a @ ( c @ compose ) @ ( a @ ( a @ product ) ) ) ),
inference(simp,[status(thm)],[54755]) ).
thf(136,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ $true
| ( ( H @ ( E @ ( G @ product ) ) )
!= ( A @ ( G @ ( F @ product ) ) ) )
| ( H @ ( F @ defined ) )
| ~ ( A @ ( G @ ( F @ product ) ) )
| ~ ( D @ ( C @ defined ) )
| ~ ( E @ ( D @ ( B @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(eqfactor_ordered,[status(thm)],[82]) ).
thf(142,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( D @ defined ) )
| ~ ( E @ ( D @ ( D @ product ) ) )
| ~ ( C @ ( B @ defined ) )
| ~ ( D @ ( C @ ( A @ product ) ) )
| ~ ( B @ ( A @ ( E @ product ) ) ) ),
inference(pattern_uni,[status(thm)],[136:[bind(A,$thf( H )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( E )),bind(F,$thf( E )),bind(G,$thf( E ))]]) ).
thf(154,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( D @ defined ) )
| ~ ( E @ ( D @ ( D @ product ) ) )
| ~ ( C @ ( B @ defined ) )
| ~ ( D @ ( C @ ( A @ product ) ) )
| ~ ( B @ ( A @ ( E @ product ) ) ) ),
inference(simp,[status(thm)],[142]) ).
thf(29472,plain,
! [B: $i,A: $i] :
( ( ( g @ ( d @ codomain @ defined ) )
!= ( B @ ( A @ defined ) ) )
| ( B @ ( A @ compose ) @ ( B @ ( A @ product ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[29250,31]) ).
thf(29473,plain,
! [B: $i,A: $i] :
( ( ( g @ ( d @ codomain @ defined ) )
!= ( B @ ( A @ defined ) ) )
| ( B @ ( A @ compose ) @ ( B @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[29472]) ).
thf(29474,plain,
g @ ( d @ codomain @ compose ) @ ( g @ ( d @ codomain @ product ) ),
inference(pattern_uni,[status(thm)],[29473:[bind(A,$thf( d @ codomain )),bind(B,$thf( g ))]]) ).
thf(9325,plain,
( ( ( c @ ( b @ ( a @ product ) ) )
!= ( a @ ( h @ compose ) @ ( a @ ( g @ product ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[32,8969]) ).
thf(9326,plain,
( ( c @ ( b @ ( a @ product ) ) )
!= ( a @ ( h @ compose ) @ ( a @ ( g @ product ) ) ) ),
inference(simp,[status(thm)],[9325]) ).
thf(9374,plain,
( ( ( a @ ( h @ compose ) )
!= c )
| ( b != a )
| ( a != g ) ),
inference(simp,[status(thm)],[9326]) ).
thf(95,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( d @ ( c @ ( g @ product ) ) )
!= ( H @ ( E @ ( G @ product ) ) ) )
| ( H @ ( F @ defined ) )
| ~ $true
| ~ ( A @ ( G @ ( F @ product ) ) )
| ~ ( D @ ( C @ defined ) )
| ~ ( E @ ( D @ ( B @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(paramod_ordered,[status(thm)],[53,82]) ).
thf(96,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( d @ ( c @ ( g @ product ) ) )
!= ( H @ ( E @ ( G @ product ) ) ) )
| ( H @ ( F @ defined ) )
| ~ ( A @ ( G @ ( F @ product ) ) )
| ~ ( D @ ( C @ defined ) )
| ~ ( E @ ( D @ ( B @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[95]) ).
thf(97,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( d @ ( E @ defined ) )
| ~ ( A @ ( g @ ( E @ product ) ) )
| ~ ( D @ ( C @ defined ) )
| ~ ( c @ ( D @ ( B @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(pattern_uni,[status(thm)],[96:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( c )),bind(F,$thf( F )),bind(G,$thf( g )),bind(H,$thf( d ))]]) ).
thf(143,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( d @ ( E @ defined ) )
| ~ ( A @ ( g @ ( E @ product ) ) )
| ~ ( D @ ( C @ defined ) )
| ~ ( c @ ( D @ ( B @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[97]) ).
thf(9309,plain,
! [A: $i] :
( ( ( A @ ( A @ ( A @ codomain @ product ) ) )
!= ( a @ ( h @ compose ) @ ( a @ ( g @ product ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[37,8969]) ).
thf(9310,plain,
! [A: $i] :
( ( A @ ( A @ ( A @ codomain @ product ) ) )
!= ( a @ ( h @ compose ) @ ( a @ ( g @ product ) ) ) ),
inference(simp,[status(thm)],[9309]) ).
thf(9378,plain,
! [A: $i] :
( ( A
!= ( a @ ( h @ compose ) ) )
| ( A != a )
| ( ( A @ codomain )
!= g ) ),
inference(simp,[status(thm)],[9310]) ).
thf(9395,plain,
( ( ( a @ ( h @ compose ) )
!= a )
| ( ( a @ codomain )
!= g ) ),
inference(simp,[status(thm)],[9378]) ).
thf(13737,plain,
! [B: $i,A: $i] :
( ( ( c @ ( g @ defined ) )
!= ( A @ ( B @ defined ) ) )
| ( B @ ( A @ defined ) )
| ~ $true
| ~ ( B @ ( A @ ( A @ product ) ) ) ),
inference(paramod_ordered,[status(thm)],[1260,84]) ).
thf(13738,plain,
! [B: $i,A: $i] :
( ( ( c @ ( g @ defined ) )
!= ( A @ ( B @ defined ) ) )
| ( B @ ( A @ defined ) )
| ~ ( B @ ( A @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[13737]) ).
thf(13739,plain,
( ( g @ ( c @ defined ) )
| ~ ( g @ ( c @ ( c @ product ) ) ) ),
inference(pattern_uni,[status(thm)],[13738:[bind(A,$thf( c )),bind(B,$thf( g ))]]) ).
thf(1222,plain,
! [A: $i] :
( ( ( A @ ( A @ ( A @ codomain @ product ) ) )
!= ( h @ ( a @ ( g @ product ) ) ) )
| ( ( h @ domain )
!= a )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[37,557]) ).
thf(1223,plain,
! [A: $i] :
( ( ( A @ ( A @ ( A @ codomain @ product ) ) )
!= ( h @ ( a @ ( g @ product ) ) ) )
| ( ( h @ domain )
!= a ) ),
inference(simp,[status(thm)],[1222]) ).
thf(1239,plain,
! [A: $i] :
( ( A != h )
| ( A != a )
| ( ( A @ codomain )
!= g )
| ( ( h @ domain )
!= a ) ),
inference(simp,[status(thm)],[1223]) ).
thf(1253,plain,
( ( a != h )
| ( ( a @ codomain )
!= g )
| ( ( h @ domain )
!= a ) ),
inference(simp,[status(thm)],[1239]) ).
thf(9159,plain,
! [A: $i] :
( ( ( A @ ( A @ codomain @ compose ) @ ( A @ ( A @ codomain @ product ) ) )
!= ( a @ ( g @ compose ) @ ( a @ ( h @ product ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[766,8906]) ).
thf(9160,plain,
! [A: $i] :
( ( A @ ( A @ codomain @ compose ) @ ( A @ ( A @ codomain @ product ) ) )
!= ( a @ ( g @ compose ) @ ( a @ ( h @ product ) ) ) ),
inference(simp,[status(thm)],[9159]) ).
thf(9223,plain,
! [A: $i] :
( ( ( A @ ( A @ codomain @ compose ) )
!= ( a @ ( g @ compose ) ) )
| ( A != a )
| ( ( A @ codomain )
!= h ) ),
inference(simp,[status(thm)],[9160]) ).
thf(9234,plain,
( ( ( a @ ( a @ codomain @ compose ) )
!= ( a @ ( g @ compose ) ) )
| ( ( a @ codomain )
!= h ) ),
inference(simp,[status(thm)],[9223]) ).
thf(86,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( d @ ( c @ ( g @ product ) ) )
!= ( C @ ( B @ ( A @ product ) ) ) )
| ( H @ ( F @ defined ) )
| ~ ( H @ ( E @ ( G @ product ) ) )
| ~ ( A @ ( G @ ( F @ product ) ) )
| ~ ( D @ ( C @ defined ) )
| ~ ( E @ ( D @ ( B @ product ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[53,82]) ).
thf(87,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( d @ ( c @ ( g @ product ) ) )
!= ( C @ ( B @ ( A @ product ) ) ) )
| ( H @ ( F @ defined ) )
| ~ ( H @ ( E @ ( G @ product ) ) )
| ~ ( A @ ( G @ ( F @ product ) ) )
| ~ ( D @ ( C @ defined ) )
| ~ ( E @ ( D @ ( B @ product ) ) ) ),
inference(simp,[status(thm)],[86]) ).
thf(88,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( C @ defined ) )
| ~ ( E @ ( B @ ( D @ product ) ) )
| ~ ( g @ ( D @ ( C @ product ) ) )
| ~ ( A @ ( d @ defined ) )
| ~ ( B @ ( A @ ( c @ product ) ) ) ),
inference(pattern_uni,[status(thm)],[87:[bind(A,$thf( g )),bind(B,$thf( c )),bind(C,$thf( d ))]]) ).
thf(158,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( C @ defined ) )
| ~ ( E @ ( B @ ( D @ product ) ) )
| ~ ( g @ ( D @ ( C @ product ) ) )
| ~ ( A @ ( d @ defined ) )
| ~ ( B @ ( A @ ( c @ product ) ) ) ),
inference(simp,[status(thm)],[88]) ).
thf(54567,plain,
( ( ( a @ ( c @ codomain @ defined ) )
!= ( a @ ( c @ defined ) ) )
| ~ ( a @ ( c @ compose ) @ ( a @ ( a @ product ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[8868,44043]) ).
thf(54568,plain,
( ( ( a @ ( c @ codomain @ defined ) )
!= ( a @ ( c @ defined ) ) )
| ~ ( a @ ( c @ compose ) @ ( a @ ( a @ product ) ) ) ),
inference(simp,[status(thm)],[54567]) ).
thf(54763,plain,
( ( a != a )
| ( ( c @ codomain )
!= c )
| ~ ( a @ ( c @ compose ) @ ( a @ ( a @ product ) ) ) ),
inference(simp,[status(thm)],[54568]) ).
thf(54829,plain,
( ( ( c @ codomain )
!= c )
| ~ ( a @ ( c @ compose ) @ ( a @ ( a @ product ) ) ) ),
inference(simp,[status(thm)],[54763]) ).
thf(167,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ domain @ ( A @ defined ) )
!= ( E @ ( D @ defined ) ) )
| ( F @ ( B @ defined ) )
| ~ $true
| ~ ( F @ ( E @ ( C @ product ) ) )
| ~ ( D @ ( C @ ( B @ product ) ) ) ),
inference(paramod_ordered,[status(thm)],[23,26]) ).
thf(168,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ domain @ ( A @ defined ) )
!= ( E @ ( D @ defined ) ) )
| ( F @ ( B @ defined ) )
| ~ ( F @ ( E @ ( C @ product ) ) )
| ~ ( D @ ( C @ ( B @ product ) ) ) ),
inference(simp,[status(thm)],[167]) ).
thf(169,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( C @ ( A @ defined ) )
| ~ ( C @ ( D @ domain @ ( B @ product ) ) )
| ~ ( D @ ( B @ ( A @ product ) ) ) ),
inference(pattern_uni,[status(thm)],[168:[bind(A,$thf( G )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( G )),bind(E,$thf( G @ domain ))]]) ).
thf(171,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( C @ ( A @ defined ) )
| ~ ( C @ ( D @ domain @ ( B @ product ) ) )
| ~ ( D @ ( B @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[169]) ).
thf(29242,plain,
! [A: $i] :
( ( ( c @ ( g @ defined ) )
!= ( d @ ( A @ defined ) ) )
| ( g @ ( A @ defined ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1260,2221]) ).
thf(29243,plain,
! [A: $i] :
( ( ( c @ ( g @ defined ) )
!= ( d @ ( A @ defined ) ) )
| ( g @ ( A @ defined ) ) ),
inference(simp,[status(thm)],[29242]) ).
thf(29345,plain,
! [A: $i] :
( ( d != c )
| ( g != A )
| ( g @ ( A @ defined ) ) ),
inference(simp,[status(thm)],[29243]) ).
thf(29379,plain,
( ( d != c )
| ( g @ ( g @ defined ) ) ),
inference(simp,[status(thm)],[29345]) ).
thf(32019,plain,
! [B: $i,A: $i] :
( ( ( g @ ( g @ defined ) )
!= ( B @ ( A @ defined ) ) )
| ( B @ ( A @ compose ) @ ( B @ ( A @ product ) ) )
| ~ $true
| ( d != c ) ),
inference(paramod_ordered,[status(thm)],[29379,31]) ).
thf(32020,plain,
! [B: $i,A: $i] :
( ( ( g @ ( g @ defined ) )
!= ( B @ ( A @ defined ) ) )
| ( B @ ( A @ compose ) @ ( B @ ( A @ product ) ) )
| ( d != c ) ),
inference(simp,[status(thm)],[32019]) ).
thf(32021,plain,
( ( g @ ( g @ compose ) @ ( g @ ( g @ product ) ) )
| ( d != c ) ),
inference(pattern_uni,[status(thm)],[32020:[bind(A,$thf( g )),bind(B,$thf( g ))]]) ).
thf(10275,plain,
! [A: $i] :
( ( ( a @ ( c @ codomain @ compose ) @ ( a @ ( c @ codomain @ product ) ) )
!= ( A @ ( a @ ( h @ product ) ) ) )
| ~ $true
| ~ ( A @ ( a @ ( g @ product ) ) ) ),
inference(paramod_ordered,[status(thm)],[9065,315]) ).
thf(10276,plain,
! [A: $i] :
( ( ( a @ ( c @ codomain @ compose ) @ ( a @ ( c @ codomain @ product ) ) )
!= ( A @ ( a @ ( h @ product ) ) ) )
| ~ ( A @ ( a @ ( g @ product ) ) ) ),
inference(simp,[status(thm)],[10275]) ).
thf(10343,plain,
! [A: $i] :
( ( ( a @ ( c @ codomain @ compose ) )
!= A )
| ( a != a )
| ( ( c @ codomain )
!= h )
| ~ ( A @ ( a @ ( g @ product ) ) ) ),
inference(simp,[status(thm)],[10276]) ).
thf(10400,plain,
( ( ( c @ codomain )
!= h )
| ~ ( a @ ( c @ codomain @ compose ) @ ( a @ ( g @ product ) ) ) ),
inference(simp,[status(thm)],[10343]) ).
thf(9313,plain,
! [A: $i] :
( ( ( A @ ( A @ codomain @ compose ) @ ( A @ ( A @ codomain @ product ) ) )
!= ( a @ ( h @ compose ) @ ( a @ ( g @ product ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[766,8969]) ).
thf(9314,plain,
! [A: $i] :
( ( A @ ( A @ codomain @ compose ) @ ( A @ ( A @ codomain @ product ) ) )
!= ( a @ ( h @ compose ) @ ( a @ ( g @ product ) ) ) ),
inference(simp,[status(thm)],[9313]) ).
thf(9376,plain,
! [A: $i] :
( ( ( A @ ( A @ codomain @ compose ) )
!= ( a @ ( h @ compose ) ) )
| ( A != a )
| ( ( A @ codomain )
!= g ) ),
inference(simp,[status(thm)],[9314]) ).
thf(9393,plain,
( ( ( a @ ( a @ codomain @ compose ) )
!= ( a @ ( h @ compose ) ) )
| ( ( a @ codomain )
!= g ) ),
inference(simp,[status(thm)],[9376]) ).
thf(795,plain,
! [B: $i,A: $i] :
( ( ( A @ domain @ ( A @ compose ) @ ( A @ domain @ ( A @ product ) ) )
!= ( B @ ( a @ ( g @ product ) ) ) )
| ~ ( B @ ( a @ ( h @ product ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[762,315]) ).
thf(796,plain,
! [B: $i,A: $i] :
( ( ( A @ domain @ ( A @ compose ) @ ( A @ domain @ ( A @ product ) ) )
!= ( B @ ( a @ ( g @ product ) ) ) )
| ~ ( B @ ( a @ ( h @ product ) ) ) ),
inference(simp,[status(thm)],[795]) ).
thf(816,plain,
! [B: $i,A: $i] :
( ( ( A @ domain @ ( A @ compose ) )
!= B )
| ( ( A @ domain )
!= a )
| ( A != g )
| ~ ( B @ ( a @ ( h @ product ) ) ) ),
inference(simp,[status(thm)],[796]) ).
thf(832,plain,
( ( ( g @ domain )
!= a )
| ~ ( g @ domain @ ( g @ compose ) @ ( a @ ( h @ product ) ) ) ),
inference(simp,[status(thm)],[816]) ).
thf(1811,plain,
! [A: $i] :
( ( A
!= ( b @ ( a @ compose ) ) )
| ( a @ codomain @ ( b @ ( a @ product ) ) )
| ~ ( a @ ( a @ ( A @ product ) ) ) ),
inference(paramod_ordered,[status(thm)],[297,1345]) ).
thf(1812,plain,
( ( a @ codomain @ ( b @ ( a @ product ) ) )
| ~ ( a @ ( a @ ( b @ ( a @ compose ) @ product ) ) ) ),
inference(pattern_uni,[status(thm)],[1811:[bind(A,$thf( b @ ( a @ compose ) ))]]) ).
thf(43653,plain,
! [A: $i] :
( ( ( A @ ( A @ ( A @ codomain @ product ) ) )
!= ( a @ ( a @ ( b @ ( a @ compose ) @ product ) ) ) )
| ( a @ codomain @ ( b @ ( a @ product ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[37,1812]) ).
thf(43654,plain,
! [A: $i] :
( ( ( A @ ( A @ ( A @ codomain @ product ) ) )
!= ( a @ ( a @ ( b @ ( a @ compose ) @ product ) ) ) )
| ( a @ codomain @ ( b @ ( a @ product ) ) ) ),
inference(simp,[status(thm)],[43653]) ).
thf(43802,plain,
! [A: $i] :
( ( A != a )
| ( A != a )
| ( ( A @ codomain )
!= ( b @ ( a @ compose ) ) )
| ( a @ codomain @ ( b @ ( a @ product ) ) ) ),
inference(simp,[status(thm)],[43654]) ).
thf(43836,plain,
( ( ( b @ ( a @ compose ) )
!= ( a @ codomain ) )
| ( a @ codomain @ ( b @ ( a @ product ) ) ) ),
inference(simp,[status(thm)],[43802]) ).
thf(39458,plain,
! [B: $i,A: $i] :
( ( ( g @ ( a @ codomain @ defined ) )
!= ( B @ ( A @ defined ) ) )
| ( B @ ( A @ compose ) @ ( B @ ( A @ product ) ) )
| ~ $true
| ( d != a ) ),
inference(paramod_ordered,[status(thm)],[38381,31]) ).
thf(39459,plain,
! [B: $i,A: $i] :
( ( ( g @ ( a @ codomain @ defined ) )
!= ( B @ ( A @ defined ) ) )
| ( B @ ( A @ compose ) @ ( B @ ( A @ product ) ) )
| ( d != a ) ),
inference(simp,[status(thm)],[39458]) ).
thf(39460,plain,
( ( g @ ( a @ codomain @ compose ) @ ( g @ ( a @ codomain @ product ) ) )
| ( d != a ) ),
inference(pattern_uni,[status(thm)],[39459:[bind(A,$thf( a @ codomain )),bind(B,$thf( g ))]]) ).
thf(101,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( c @ ( b @ ( a @ product ) ) )
!= ( E @ ( D @ ( B @ product ) ) ) )
| ( H @ ( F @ defined ) )
| ~ ( H @ ( E @ ( G @ product ) ) )
| ~ ( A @ ( G @ ( F @ product ) ) )
| ~ ( D @ ( C @ defined ) )
| ~ $true
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(paramod_ordered,[status(thm)],[32,82]) ).
thf(102,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( c @ ( b @ ( a @ product ) ) )
!= ( E @ ( D @ ( B @ product ) ) ) )
| ( H @ ( F @ defined ) )
| ~ ( H @ ( E @ ( G @ product ) ) )
| ~ ( A @ ( G @ ( F @ product ) ) )
| ~ ( D @ ( C @ defined ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[101]) ).
thf(103,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( C @ defined ) )
| ~ ( E @ ( c @ ( D @ product ) ) )
| ~ ( A @ ( D @ ( C @ product ) ) )
| ~ ( b @ ( B @ defined ) )
| ~ ( B @ ( a @ ( A @ product ) ) ) ),
inference(pattern_uni,[status(thm)],[102:[bind(A,$thf( A )),bind(B,$thf( a )),bind(C,$thf( C )),bind(D,$thf( b )),bind(E,$thf( c ))]]) ).
thf(146,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( C @ defined ) )
| ~ ( E @ ( c @ ( D @ product ) ) )
| ~ ( A @ ( D @ ( C @ product ) ) )
| ~ ( b @ ( B @ defined ) )
| ~ ( B @ ( a @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[103]) ).
thf(13746,plain,
! [B: $i,A: $i] :
( ( ( a @ ( g @ defined ) )
!= ( A @ ( B @ defined ) ) )
| ( B @ ( A @ defined ) )
| ~ $true
| ~ ( B @ ( A @ ( A @ product ) ) ) ),
inference(paramod_ordered,[status(thm)],[8855,84]) ).
thf(13747,plain,
! [B: $i,A: $i] :
( ( ( a @ ( g @ defined ) )
!= ( A @ ( B @ defined ) ) )
| ( B @ ( A @ defined ) )
| ~ ( B @ ( A @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[13746]) ).
thf(13748,plain,
( ( g @ ( a @ defined ) )
| ~ ( g @ ( a @ ( a @ product ) ) ) ),
inference(pattern_uni,[status(thm)],[13747:[bind(A,$thf( a )),bind(B,$thf( g ))]]) ).
thf(133,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ $true
| ( ( A @ ( G @ ( F @ product ) ) )
!= ( E @ ( D @ ( B @ product ) ) ) )
| ( H @ ( F @ defined ) )
| ~ ( H @ ( E @ ( G @ product ) ) )
| ~ ( D @ ( C @ defined ) )
| ~ ( E @ ( D @ ( B @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(eqfactor_ordered,[status(thm)],[82]) ).
thf(140,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( C @ defined ) )
| ~ ( E @ ( A @ ( D @ product ) ) )
| ~ ( D @ ( B @ defined ) )
| ~ ( A @ ( D @ ( C @ product ) ) )
| ~ ( B @ ( C @ ( A @ product ) ) ) ),
inference(pattern_uni,[status(thm)],[133:[bind(A,$thf( A )),bind(B,$thf( F )),bind(C,$thf( C )),bind(D,$thf( G )),bind(E,$thf( A ))]]) ).
thf(151,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( C @ defined ) )
| ~ ( E @ ( A @ ( D @ product ) ) )
| ~ ( D @ ( B @ defined ) )
| ~ ( A @ ( D @ ( C @ product ) ) )
| ~ ( B @ ( C @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[140]) ).
thf(36,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( E @ defined ) )
| ~ ( C @ ( D @ defined ) )
| ~ ( E @ ( A @ ( D @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(cnf,[status(esa)],[35]) ).
thf(941,plain,
( ( ( c @ ( b @ ( a @ product ) ) )
!= ( g @ ( a @ ( h @ product ) ) ) )
| ( ( g @ domain )
!= a )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[32,554]) ).
thf(942,plain,
( ( ( c @ ( b @ ( a @ product ) ) )
!= ( g @ ( a @ ( h @ product ) ) ) )
| ( ( g @ domain )
!= a ) ),
inference(simp,[status(thm)],[941]) ).
thf(967,plain,
( ( c != g )
| ( b != a )
| ( a != h )
| ( ( g @ domain )
!= a ) ),
inference(simp,[status(thm)],[942]) ).
thf(13817,plain,
! [B: $i,A: $i] :
( ( ( c @ ( a @ codomain @ defined ) )
!= ( A @ ( B @ defined ) ) )
| ( B @ ( A @ defined ) )
| ~ $true
| ~ ( B @ ( A @ ( A @ product ) ) ) ),
inference(paramod_ordered,[status(thm)],[11252,84]) ).
thf(13818,plain,
! [B: $i,A: $i] :
( ( ( c @ ( a @ codomain @ defined ) )
!= ( A @ ( B @ defined ) ) )
| ( B @ ( A @ defined ) )
| ~ ( B @ ( A @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[13817]) ).
thf(13819,plain,
( ( a @ codomain @ ( c @ defined ) )
| ~ ( a @ codomain @ ( c @ ( c @ product ) ) ) ),
inference(pattern_uni,[status(thm)],[13818:[bind(A,$thf( c )),bind(B,$thf( a @ codomain ))]]) ).
thf(56405,plain,
( ( ( b @ ( a @ defined ) )
!= ( a @ ( a @ defined ) ) )
| ~ ( a @ ( a @ compose ) @ ( a @ ( c @ product ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1281,44046]) ).
thf(56406,plain,
( ( ( b @ ( a @ defined ) )
!= ( a @ ( a @ defined ) ) )
| ~ ( a @ ( a @ compose ) @ ( a @ ( c @ product ) ) ) ),
inference(simp,[status(thm)],[56405]) ).
thf(56666,plain,
( ( b != a )
| ( a != a )
| ~ ( a @ ( a @ compose ) @ ( a @ ( c @ product ) ) ) ),
inference(simp,[status(thm)],[56406]) ).
thf(56716,plain,
( ( b != a )
| ~ ( a @ ( a @ compose ) @ ( a @ ( c @ product ) ) ) ),
inference(simp,[status(thm)],[56666]) ).
thf(9478,plain,
! [A: $i] :
( ( A
!= ( a @ ( g @ compose ) ) )
| ( a @ codomain @ ( a @ ( g @ product ) ) )
| ~ ( a @ ( a @ ( A @ product ) ) ) ),
inference(paramod_ordered,[status(thm)],[297,8935]) ).
thf(9479,plain,
( ( a @ codomain @ ( a @ ( g @ product ) ) )
| ~ ( a @ ( a @ ( a @ ( g @ compose ) @ product ) ) ) ),
inference(pattern_uni,[status(thm)],[9478:[bind(A,$thf( a @ ( g @ compose ) ))]]) ).
thf(50007,plain,
! [A: $i] :
( ( ( A @ ( A @ ( A @ codomain @ product ) ) )
!= ( a @ ( a @ ( a @ ( g @ compose ) @ product ) ) ) )
| ( a @ codomain @ ( a @ ( g @ product ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[37,9479]) ).
thf(50008,plain,
! [A: $i] :
( ( ( A @ ( A @ ( A @ codomain @ product ) ) )
!= ( a @ ( a @ ( a @ ( g @ compose ) @ product ) ) ) )
| ( a @ codomain @ ( a @ ( g @ product ) ) ) ),
inference(simp,[status(thm)],[50007]) ).
thf(50149,plain,
! [A: $i] :
( ( A != a )
| ( A != a )
| ( ( A @ codomain )
!= ( a @ ( g @ compose ) ) )
| ( a @ codomain @ ( a @ ( g @ product ) ) ) ),
inference(simp,[status(thm)],[50008]) ).
thf(50194,plain,
( ( ( a @ ( g @ compose ) )
!= ( a @ codomain ) )
| ( a @ codomain @ ( a @ ( g @ product ) ) ) ),
inference(simp,[status(thm)],[50149]) ).
thf(46,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( C = D )
| ~ ( D @ ( B @ ( A @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(cnf,[status(esa)],[45]) ).
thf(47,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( D @ ( B @ ( A @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) )
| ( C = D ) ),
inference(lifteq,[status(thm)],[46]) ).
thf(175,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ codomain @ defined ) )
!= ( E @ ( D @ defined ) ) )
| ( F @ ( B @ defined ) )
| ~ $true
| ~ ( F @ ( E @ ( C @ product ) ) )
| ~ ( D @ ( C @ ( B @ product ) ) ) ),
inference(paramod_ordered,[status(thm)],[24,26]) ).
thf(176,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ codomain @ defined ) )
!= ( E @ ( D @ defined ) ) )
| ( F @ ( B @ defined ) )
| ~ ( F @ ( E @ ( C @ product ) ) )
| ~ ( D @ ( C @ ( B @ product ) ) ) ),
inference(simp,[status(thm)],[175]) ).
thf(177,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( C @ ( A @ defined ) )
| ~ ( C @ ( D @ ( B @ product ) ) )
| ~ ( D @ codomain @ ( B @ ( A @ product ) ) ) ),
inference(pattern_uni,[status(thm)],[176:[bind(A,$thf( G )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( G @ codomain )),bind(E,$thf( G ))]]) ).
thf(178,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( C @ ( A @ defined ) )
| ~ ( C @ ( D @ ( B @ product ) ) )
| ~ ( D @ codomain @ ( B @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[177]) ).
thf(10197,plain,
! [A: $i] :
( ( ( a @ ( c @ codomain @ compose ) @ ( a @ ( c @ codomain @ product ) ) )
!= ( a @ ( a @ ( A @ product ) ) ) )
| ~ $true
| ( ( a @ codomain )
= A ) ),
inference(paramod_ordered,[status(thm)],[9065,297]) ).
thf(10198,plain,
! [A: $i] :
( ( ( a @ ( c @ codomain @ compose ) @ ( a @ ( c @ codomain @ product ) ) )
!= ( a @ ( a @ ( A @ product ) ) ) )
| ( ( a @ codomain )
= A ) ),
inference(simp,[status(thm)],[10197]) ).
thf(10322,plain,
! [A: $i] :
( ( ( a @ ( c @ codomain @ compose ) )
!= a )
| ( a != a )
| ( ( c @ codomain )
!= A )
| ( ( a @ codomain )
= A ) ),
inference(simp,[status(thm)],[10198]) ).
thf(10383,plain,
( ( ( a @ ( c @ codomain @ compose ) )
!= a )
| ( ( c @ codomain )
= ( a @ codomain ) ) ),
inference(simp,[status(thm)],[10322]) ).
thf(531,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ ( A @ codomain @ product ) ) )
!= ( B @ ( a @ ( g @ product ) ) ) )
| ~ ( B @ ( a @ ( h @ product ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[37,315]) ).
thf(532,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ ( A @ codomain @ product ) ) )
!= ( B @ ( a @ ( g @ product ) ) ) )
| ~ ( B @ ( a @ ( h @ product ) ) ) ),
inference(simp,[status(thm)],[531]) ).
thf(551,plain,
! [B: $i,A: $i] :
( ( A != B )
| ( A != a )
| ( ( A @ codomain )
!= g )
| ~ ( B @ ( a @ ( h @ product ) ) ) ),
inference(simp,[status(thm)],[532]) ).
thf(560,plain,
( ( ( a @ codomain )
!= g )
| ~ ( a @ ( a @ ( h @ product ) ) ) ),
inference(simp,[status(thm)],[551]) ).
thf(9133,plain,
! [A: $i] :
( ( ( A @ domain @ ( A @ compose ) @ ( A @ domain @ ( A @ product ) ) )
!= ( a @ ( g @ compose ) @ ( a @ ( h @ product ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[762,8906]) ).
thf(9134,plain,
! [A: $i] :
( ( A @ domain @ ( A @ compose ) @ ( A @ domain @ ( A @ product ) ) )
!= ( a @ ( g @ compose ) @ ( a @ ( h @ product ) ) ) ),
inference(simp,[status(thm)],[9133]) ).
thf(9212,plain,
! [A: $i] :
( ( ( A @ domain @ ( A @ compose ) )
!= ( a @ ( g @ compose ) ) )
| ( ( A @ domain )
!= a )
| ( A != h ) ),
inference(simp,[status(thm)],[9134]) ).
thf(9254,plain,
( ( ( a @ ( g @ compose ) )
!= ( h @ domain @ ( h @ compose ) ) )
| ( ( h @ domain )
!= a ) ),
inference(simp,[status(thm)],[9212]) ).
thf(31859,plain,
! [B: $i,A: $i] :
( ( ( g @ ( h @ defined ) )
!= ( B @ ( A @ defined ) ) )
| ( B @ ( A @ compose ) @ ( B @ ( A @ product ) ) )
| ~ $true
| ( d != a ) ),
inference(paramod_ordered,[status(thm)],[29378,31]) ).
thf(31860,plain,
! [B: $i,A: $i] :
( ( ( g @ ( h @ defined ) )
!= ( B @ ( A @ defined ) ) )
| ( B @ ( A @ compose ) @ ( B @ ( A @ product ) ) )
| ( d != a ) ),
inference(simp,[status(thm)],[31859]) ).
thf(31861,plain,
( ( g @ ( h @ compose ) @ ( g @ ( h @ product ) ) )
| ( d != a ) ),
inference(pattern_uni,[status(thm)],[31860:[bind(A,$thf( h )),bind(B,$thf( g ))]]) ).
thf(953,plain,
! [A: $i] :
( ( ( A @ ( A @ ( A @ codomain @ product ) ) )
!= ( g @ ( a @ ( h @ product ) ) ) )
| ( ( g @ domain )
!= a )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[37,554]) ).
thf(954,plain,
! [A: $i] :
( ( ( A @ ( A @ ( A @ codomain @ product ) ) )
!= ( g @ ( a @ ( h @ product ) ) ) )
| ( ( g @ domain )
!= a ) ),
inference(simp,[status(thm)],[953]) ).
thf(963,plain,
! [A: $i] :
( ( A != g )
| ( A != a )
| ( ( A @ codomain )
!= h )
| ( ( g @ domain )
!= a ) ),
inference(simp,[status(thm)],[954]) ).
thf(972,plain,
( ( a != g )
| ( ( a @ codomain )
!= h )
| ( ( g @ domain )
!= a ) ),
inference(simp,[status(thm)],[963]) ).
thf(43936,plain,
! [A: $i] :
( ( ( b @ ( a @ compose ) @ ( b @ ( a @ product ) ) )
!= ( A @ ( a @ ( a @ product ) ) ) )
| ~ $true
| ~ ( A @ ( a @ ( c @ product ) ) ) ),
inference(paramod_ordered,[status(thm)],[1345,697]) ).
thf(43937,plain,
! [A: $i] :
( ( ( b @ ( a @ compose ) @ ( b @ ( a @ product ) ) )
!= ( A @ ( a @ ( a @ product ) ) ) )
| ~ ( A @ ( a @ ( c @ product ) ) ) ),
inference(simp,[status(thm)],[43936]) ).
thf(44105,plain,
! [A: $i] :
( ( ( b @ ( a @ compose ) )
!= A )
| ( b != a )
| ( a != a )
| ~ ( A @ ( a @ ( c @ product ) ) ) ),
inference(simp,[status(thm)],[43937]) ).
thf(44192,plain,
( ( b != a )
| ~ ( b @ ( a @ compose ) @ ( a @ ( c @ product ) ) ) ),
inference(simp,[status(thm)],[44105]) ).
thf(13476,plain,
! [B: $i,A: $i] :
( ( ( a @ ( g @ codomain @ defined ) )
!= ( B @ ( A @ defined ) ) )
| ( B @ ( A @ compose ) @ ( B @ ( A @ product ) ) )
| ~ $true
| ( d != c ) ),
inference(paramod_ordered,[status(thm)],[13122,31]) ).
thf(13477,plain,
! [B: $i,A: $i] :
( ( ( a @ ( g @ codomain @ defined ) )
!= ( B @ ( A @ defined ) ) )
| ( B @ ( A @ compose ) @ ( B @ ( A @ product ) ) )
| ( d != c ) ),
inference(simp,[status(thm)],[13476]) ).
thf(13478,plain,
( ( a @ ( g @ codomain @ compose ) @ ( a @ ( g @ codomain @ product ) ) )
| ( d != c ) ),
inference(pattern_uni,[status(thm)],[13477:[bind(A,$thf( g @ codomain )),bind(B,$thf( a ))]]) ).
thf(54644,plain,
( ( ( a @ ( c @ defined ) )
!= ( a @ ( h @ defined ) ) )
| ~ ( a @ ( c @ compose ) @ ( a @ ( a @ product ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[8876,44043]) ).
thf(54645,plain,
( ( ( a @ ( c @ defined ) )
!= ( a @ ( h @ defined ) ) )
| ~ ( a @ ( c @ compose ) @ ( a @ ( a @ product ) ) ) ),
inference(simp,[status(thm)],[54644]) ).
thf(54770,plain,
( ( a != a )
| ( c != h )
| ~ ( a @ ( c @ compose ) @ ( a @ ( a @ product ) ) ) ),
inference(simp,[status(thm)],[54645]) ).
thf(54832,plain,
( ( c != h )
| ~ ( a @ ( c @ compose ) @ ( a @ ( a @ product ) ) ) ),
inference(simp,[status(thm)],[54770]) ).
thf(67977,plain,
$false,
inference(e,[status(thm)],[1322,29375,43966,32770,762,29435,449,677,8855,170,11440,24056,9233,13779,47622,1260,153,29371,42,24,38488,47650,25,885,1046,37,29250,13800,11976,8996,29631,10382,49934,31701,157,52,1409,12197,570,9230,1992,20,152,44202,78,44043,29,29378,13788,9636,179,12828,84,1051,766,147,13077,1345,9236,85,38373,7269,29380,9384,2428,38,160,297,54831,45543,429,33,13850,1042,916,29593,830,54801,32946,1281,9885,29266,156,56698,53,10398,697,1234,13782,12151,4860,554,34457,11442,20129,9392,679,701,44257,38381,11300,1979,12831,8935,1266,29394,2221,10624,3856,20125,13122,148,8906,45,161,25356,20720,32,34,13031,149,9652,29396,22,44,25357,44259,26604,27,144,49,28107,29443,54,44209,13730,9390,159,81,8868,44204,39,29702,451,567,1080,31541,44184,45275,915,155,12587,33133,24050,44253,45249,80,35,13806,162,51532,44185,11679,145,56681,55146,48,557,33423,150,887,26168,11252,10392,50,43979,9214,9634,9065,56709,10861,45262,31,10023,54824,613,154,29474,9374,143,43,9395,556,13739,1253,9234,44046,40,26,158,54829,171,23,32021,10400,9393,832,43836,12230,29546,82,8969,39460,315,1578,146,30,51,8901,13748,2218,151,36,967,13819,56716,50194,79,10009,14603,8876,44002,47,178,1299,10383,29379,560,9479,1812,9254,11294,31861,972,44192,83,13478,54832]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CAT004-1 : TPTP v9.3.1. Released v1.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.14/0.39 % Computer : n019.cluster.edu
% 0.14/0.39 % Model : x86_64 x86_64
% 0.14/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.39 % Memory : 8046.5625MB
% 0.14/0.39 % OS : Linux 6.8.0-71-generic
% 0.14/0.39 % CPULimit : 300
% 0.14/0.39 % WCLimit : 300
% 0.14/0.39 % DateTime : Sat Sep 26 22:48:18 UTC 2026
% 0.14/0.39 % CPUTime :
% 0.14/0.39 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
% 0.94/1.01 % [INFO] Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ...
% 1.47/1.23 % [INFO] Parsing done (217ms).
% 1.47/1.24 % [INFO] Running in sequential loop mode.
% 2.21/1.64 % [INFO] eprover registered as external prover.
% 2.21/1.65 % [INFO] Scanning for conjecture ...
% 2.43/1.74 % [INFO] Found a conjecture (or negated_conjecture) and 23 axioms. Running axiom selection ...
% 2.43/1.80 % [INFO] Axiom selection finished. Selected 18 axioms (removed 5 axioms).
% 2.63/1.83 % [INFO] Problem is propositional (TPTP CNF).
% 2.63/1.84 % [INFO] Type checking passed.
% 2.63/1.85 % [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 ...
% 78.75/18.83 % External prover 'e' found a proof!
% 78.75/18.83 % [INFO] Killing All external provers ...
% 78.75/18.83 % Time passed: 18275ms (effective reasoning time: 17582ms)
% 78.75/18.83 % Axioms used in derivation (18): category_theory_axiom5, category_theory_axiom1, hc_equals_d, category_theory_axiom4, closure_of_composition, mapping_from_x_to_its_domain, mapping_from_codomain_of_x_to_x, associative_property1, cancellation_for_product1, product_on_codomain, category_theory_axiom3, gc_equals_d, associative_property2, cancellation_for_product2, product_on_domain, composition_is_well_defined, category_theory_axiom2, ab_equals_c
% 78.75/18.83 % No. of inferences in proof: 820
% 78.75/18.83 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p : 18275 ms resp. 17582 ms w/o parsing
% 79.95/19.10 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 79.95/19.11 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------