%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : HAL004+1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% Computer : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 07:31:31 AM UTC 2026
% Result : Theorem 138.53s 40.30s
% Output : Refutation 138.91s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 38
% Syntax : Number of formulae : 318 ( 51 unt; 0 typ; 7 def)
% Number of atoms : 1470 ( 845 equ; 0 cnn)
% Maximal formula atoms : 24 ( 4 avg)
% Number of connectives : 4770 ( 889 ~; 839 |; 120 &;2856 @)
% ( 2 <=>; 64 =>; 0 <=; 0 <~>)
% Maximal formula depth : 25 ( 8 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 33 ( 30 usr; 17 con; 0-8 aty)
% Number of variables : 526 ( 25 ^; 462 !; 32 ?; 526 :)
% ( 0 !>; 0 ?*; 0 @-; 7 @+)
% Comments :
%------------------------------------------------------------------------------
thf(element_decl,type,
element: $i > $i > $o ).
thf(e_decl,type,
e: $i ).
thf(r_decl,type,
r: $i ).
thf(apply_decl,type,
apply: $i > $i > $i ).
thf(delta_decl,type,
delta: $i ).
thf(b_decl,type,
b: $i ).
thf(h_decl,type,
h: $i ).
thf(beta_decl,type,
beta: $i ).
thf(g_decl,type,
g: $i ).
thf(injection_decl,type,
injection: $i > $o ).
thf(gamma_decl,type,
gamma: $i ).
thf(alpha_decl,type,
alpha: $i ).
thf(surjection_decl,type,
surjection: $i > $o ).
thf(f_decl,type,
f: $i ).
thf(morphism_decl,type,
morphism: $i > $i > $i > $o ).
thf(a_decl,type,
a: $i ).
thf(d_decl,type,
d: $i ).
thf(c_decl,type,
c: $i ).
thf(commute_decl,type,
commute: $i > $i > $i > $i > $o ).
thf(subtract_decl,type,
subtract: $i > $i > $i > $i ).
thf(exact_decl,type,
exact: $i > $i > $o ).
thf(gammma_decl,type,
gammma: $i ).
thf(zero_decl,type,
zero: $i > $i ).
thf(sk1_decl,type,
sk1: $i ).
thf(sk2_decl,type,
sk2: $i > $i > $i > $i > $i > $i > $i > $i > $i ).
thf(sk3_decl,type,
sk3: $i > $i > $i > $i ).
thf(sk4_decl,type,
sk4: $i > $i > $i > $i > $i ).
thf(sk5_decl,type,
sk5: $i > $i > $i > $i > $i > $i > $i ).
thf(sk10_decl,type,
sk10: $i > $i > $i ).
thf(sk11_decl,type,
sk11: $i > $i > $i ).
thf(sk1_def,definition,
( sk1
= ( @+[A: $i] :
~ ( ( e @ ( A @ element ) )
=> ? [B: $i] :
( ? [C: $i] :
( ( ( C @ ( g @ apply ) @ ( delta @ apply ) )
= B )
& ( ( C @ ( beta @ apply ) @ ( h @ apply ) )
= B )
& ( b @ ( C @ element ) ) )
& ( ( A @ ( delta @ apply ) )
= B )
& ( r @ ( B @ element ) ) ) ) ) ) ).
thf(sk2_def,definition,
( sk2
= ( ^ [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i,G: $i,H: $i] :
@+[I: $i] :
~ ( ( D @ ( I @ element ) )
=> ( ( I @ ( H @ apply ) @ ( G @ apply ) )
= ( I @ ( F @ apply ) @ ( E @ apply ) ) ) ) ) ) ).
thf(sk3_def,definition,
( sk3
= ( ^ [A: $i,B: $i,C: $i] :
@+[D: $i] :
~ ( ( A @ ( D @ element ) )
=> ? [E: $i] :
( ( ( E @ ( C @ apply ) )
= D )
& ( B @ ( E @ element ) ) ) ) ) ) ).
thf(sk4_def,definition,
( sk4
= ( ^ [A: $i,B: $i,C: $i,D: $i] :
@+[E: $i] :
( ( ( E @ ( D @ apply ) )
= A )
& ( C @ ( E @ element ) ) ) ) ) ).
thf(sk5_def,definition,
( sk5
= ( ^ [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i] :
@+[G: $i] :
( ( ( G @ ( F @ apply ) )
= A )
& ( D @ ( G @ element ) ) ) ) ) ).
thf(sk10_def,definition,
( sk10
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
~ ! [D: $i] :
( ( ( ( C @ ( B @ apply ) )
= ( D @ ( B @ apply ) ) )
& ( A @ ( D @ element ) )
& ( A @ ( C @ element ) ) )
=> ( C = D ) ) ) ) ).
thf(sk11_def,definition,
( sk11
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
~ ( ( ( ( B @ ( A @ sk10 ) @ ( B @ apply ) )
= ( C @ ( B @ apply ) ) )
& ( A @ ( C @ element ) )
& ( A @ ( B @ ( A @ sk10 ) @ element ) ) )
=> ( ( B @ ( A @ sk10 ) )
= C ) ) ) ) ).
thf(17,axiom,
r @ ( e @ ( delta @ morphism ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',delta_morphism) ).
thf(82,plain,
r @ ( e @ ( delta @ morphism ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[17]) ).
thf(24,axiom,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ ( A @ morphism ) ) )
=> ( ( ( B @ zero @ ( A @ apply ) )
= ( C @ zero ) )
& ! [D: $i] :
( ( B @ ( D @ element ) )
=> ( C @ ( D @ ( A @ apply ) @ element ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',morphism) ).
thf(97,plain,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ ( A @ morphism ) ) )
=> ( ( ( B @ zero @ ( A @ apply ) )
= ( C @ zero ) )
& ! [D: $i] :
( ( B @ ( D @ element ) )
=> ( C @ ( D @ ( A @ apply ) @ element ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[24]) ).
thf(98,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( ( B @ zero @ ( A @ apply ) )
= ( C @ zero ) )
| ~ ( C @ ( B @ ( A @ morphism ) ) ) )
& ( ( C @ ( D @ ( A @ apply ) @ element ) )
| ~ ( B @ ( D @ element ) )
| ~ ( C @ ( B @ ( A @ morphism ) ) ) ) ),
inference(cnf,[status(esa)],[97]) ).
thf(100,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ zero @ ( A @ apply ) )
= ( C @ zero ) )
| ~ ( C @ ( B @ ( A @ morphism ) ) ) ),
inference(cnfConj,[status(thm)],[98]) ).
thf(101,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ ( B @ ( A @ morphism ) ) )
| ( ( B @ zero @ ( A @ apply ) )
= ( C @ zero ) ) ),
inference(lifteq,[status(thm)],[100]) ).
thf(606,plain,
! [C: $i,B: $i,A: $i] :
( ( ( r @ ( e @ ( delta @ morphism ) ) )
!= ( C @ ( B @ ( A @ morphism ) ) ) )
| ~ $true
| ( ( B @ zero @ ( A @ apply ) )
= ( C @ zero ) ) ),
inference(paramod_ordered,[status(thm)],[82,101]) ).
thf(607,plain,
! [C: $i,B: $i,A: $i] :
( ( ( r @ ( e @ ( delta @ morphism ) ) )
!= ( C @ ( B @ ( A @ morphism ) ) ) )
| ( ( B @ zero @ ( A @ apply ) )
= ( C @ zero ) ) ),
inference(simp,[status(thm)],[606]) ).
thf(608,plain,
( ( e @ zero @ ( delta @ apply ) )
= ( r @ zero ) ),
inference(pattern_uni,[status(thm)],[607:[bind(A,$thf( delta )),bind(B,$thf( e )),bind(C,$thf( r ))]]) ).
thf(16,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i] :
( ( ( E @ ( D @ ( B @ morphism ) ) )
& ( D @ ( C @ ( A @ morphism ) ) )
& ( B @ ( A @ exact ) ) )
=> ! [F: $i] :
( ( ( ( F @ ( B @ apply ) )
= ( E @ zero ) )
& ( D @ ( F @ element ) ) )
<=> ? [G: $i] :
( ( ( G @ ( A @ apply ) )
= F )
& ( C @ ( G @ element ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',exact_properties) ).
thf(69,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i] :
( ( ( E @ ( D @ ( B @ morphism ) ) )
& ( D @ ( C @ ( A @ morphism ) ) )
& ( B @ ( A @ exact ) ) )
=> ! [F: $i] :
( ( ? [G: $i] :
( ( ( G @ ( A @ apply ) )
= F )
& ( C @ ( G @ element ) ) )
=> ( ( ( F @ ( B @ apply ) )
= ( E @ zero ) )
& ( D @ ( F @ element ) ) ) )
& ( ( ( ( F @ ( B @ apply ) )
= ( E @ zero ) )
& ( D @ ( F @ element ) ) )
=> ? [G: $i] :
( ( ( G @ ( A @ apply ) )
= F )
& ( C @ ( G @ element ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[16]) ).
thf(10,axiom,
e @ ( b @ ( g @ morphism ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',g_morphism) ).
thf(57,plain,
e @ ( b @ ( g @ morphism ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).
thf(9,axiom,
! [A: $i,B: $i,C: $i] :
( ( ! [D: $i] :
( ( C @ ( D @ element ) )
=> ? [E: $i] :
( ( ( E @ ( A @ apply ) )
= D )
& ( B @ ( E @ element ) ) ) )
& ( C @ ( B @ ( A @ morphism ) ) ) )
=> ( A @ surjection ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',properties_for_surjection) ).
thf(51,plain,
! [A: $i,B: $i,C: $i] :
( ( ! [D: $i] :
( ( C @ ( D @ element ) )
=> ? [E: $i] :
( ( ( E @ ( A @ apply ) )
= D )
& ( B @ ( E @ element ) ) ) )
& ( C @ ( B @ ( A @ morphism ) ) ) )
=> ( A @ surjection ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).
thf(52,plain,
! [A: $i] :
( ? [B: $i,C: $i] :
( ! [D: $i] :
( ( C @ ( D @ element ) )
=> ? [E: $i] :
( ( ( E @ ( A @ apply ) )
= D )
& ( B @ ( E @ element ) ) ) )
& ( C @ ( B @ ( A @ morphism ) ) ) )
=> ( A @ surjection ) ),
inference(miniscope,[status(thm)],[51]) ).
thf(53,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ surjection )
| ( ( D @ ( A @ apply ) )
!= ( A @ ( B @ ( C @ sk3 ) ) ) )
| ~ ( B @ ( D @ element ) )
| ~ ( C @ ( B @ ( A @ morphism ) ) ) )
& ( ( A @ surjection )
| ( C @ ( A @ ( B @ ( C @ sk3 ) ) @ element ) )
| ~ ( C @ ( B @ ( A @ morphism ) ) ) ) ),
inference(cnf,[status(esa)],[52]) ).
thf(54,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ surjection )
| ( C @ ( A @ ( B @ ( C @ sk3 ) ) @ element ) )
| ~ ( C @ ( B @ ( A @ morphism ) ) ) ),
inference(cnfConj,[status(thm)],[53]) ).
thf(862,plain,
! [C: $i,B: $i,A: $i] :
( ( ( e @ ( b @ ( g @ morphism ) ) )
!= ( C @ ( B @ ( A @ morphism ) ) ) )
| ( A @ surjection )
| ( C @ ( A @ ( B @ ( C @ sk3 ) ) @ element ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[57,54]) ).
thf(863,plain,
! [C: $i,B: $i,A: $i] :
( ( ( e @ ( b @ ( g @ morphism ) ) )
!= ( C @ ( B @ ( A @ morphism ) ) ) )
| ( A @ surjection )
| ( C @ ( A @ ( B @ ( C @ sk3 ) ) @ element ) ) ),
inference(simp,[status(thm)],[862]) ).
thf(864,plain,
( ( g @ surjection )
| ( e @ ( g @ ( b @ ( e @ sk3 ) ) @ element ) ) ),
inference(pattern_uni,[status(thm)],[863:[bind(A,$thf( g )),bind(B,$thf( b )),bind(C,$thf( e ))]]) ).
thf(20,axiom,
! [A: $i,B: $i] :
( ( A @ ( B @ element ) )
=> ( ( B @ ( B @ ( A @ subtract ) ) )
= ( A @ zero ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',subtract_to_0) ).
thf(87,plain,
! [A: $i,B: $i] :
( ( A @ ( B @ element ) )
=> ( ( B @ ( B @ ( A @ subtract ) ) )
= ( A @ zero ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[20]) ).
thf(88,plain,
! [B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ subtract ) ) )
= ( A @ zero ) )
| ~ ( A @ ( B @ element ) ) ),
inference(cnf,[status(esa)],[87]) ).
thf(89,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ element ) )
| ( ( B @ ( B @ ( A @ subtract ) ) )
= ( A @ zero ) ) ),
inference(lifteq,[status(thm)],[88]) ).
thf(2070,plain,
! [B: $i,A: $i] :
( ( ( e @ ( g @ ( b @ ( e @ sk3 ) ) @ element ) )
!= ( A @ ( B @ element ) ) )
| ~ $true
| ( ( B @ ( B @ ( A @ subtract ) ) )
= ( A @ zero ) )
| ( g @ surjection ) ),
inference(paramod_ordered,[status(thm)],[864,89]) ).
thf(2071,plain,
! [B: $i,A: $i] :
( ( ( e @ ( g @ ( b @ ( e @ sk3 ) ) @ element ) )
!= ( A @ ( B @ element ) ) )
| ( ( B @ ( B @ ( A @ subtract ) ) )
= ( A @ zero ) )
| ( g @ surjection ) ),
inference(simp,[status(thm)],[2070]) ).
thf(2072,plain,
( ( ( g @ ( b @ ( e @ sk3 ) ) @ ( g @ ( b @ ( e @ sk3 ) ) @ ( e @ subtract ) ) )
= ( e @ zero ) )
| ( g @ surjection ) ),
inference(pattern_uni,[status(thm)],[2071:[bind(A,$thf( e )),bind(B,$thf( g @ ( b @ ( e @ sk3 ) ) ))]]) ).
thf(557,plain,
! [C: $i,B: $i,A: $i] :
( ( ( e @ ( b @ ( g @ morphism ) ) )
!= ( C @ ( B @ ( A @ morphism ) ) ) )
| ~ $true
| ( ( B @ zero @ ( A @ apply ) )
= ( C @ zero ) ) ),
inference(paramod_ordered,[status(thm)],[57,101]) ).
thf(558,plain,
! [C: $i,B: $i,A: $i] :
( ( ( e @ ( b @ ( g @ morphism ) ) )
!= ( C @ ( B @ ( A @ morphism ) ) ) )
| ( ( B @ zero @ ( A @ apply ) )
= ( C @ zero ) ) ),
inference(simp,[status(thm)],[557]) ).
thf(559,plain,
( ( b @ zero @ ( g @ apply ) )
= ( e @ zero ) ),
inference(pattern_uni,[status(thm)],[558:[bind(A,$thf( g )),bind(B,$thf( b )),bind(C,$thf( e ))]]) ).
thf(711,plain,
! [C: $i,B: $i,A: $i] :
( ( ( b @ zero @ ( g @ apply ) )
!= ( B @ zero @ ( A @ apply ) ) )
| ~ ( C @ ( B @ ( A @ morphism ) ) )
| ( ( e @ zero )
= ( C @ zero ) ) ),
inference(paramod_ordered,[status(thm)],[559,101]) ).
thf(712,plain,
! [A: $i] :
( ~ ( A @ ( b @ ( g @ morphism ) ) )
| ( ( e @ zero )
= ( A @ zero ) ) ),
inference(pattern_uni,[status(thm)],[711:[bind(A,$thf( g )),bind(B,$thf( b ))]]) ).
thf(826,plain,
! [A: $i] :
( ~ ( A @ ( b @ ( g @ morphism ) ) )
| ( ( e @ zero )
= ( A @ zero ) ) ),
inference(simp,[status(thm)],[712]) ).
thf(29,axiom,
c @ ( b @ ( beta @ morphism ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',beta_morphism) ).
thf(118,plain,
c @ ( b @ ( beta @ morphism ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[29]) ).
thf(578,plain,
! [C: $i,B: $i,A: $i] :
( ( ( c @ ( b @ ( beta @ morphism ) ) )
!= ( C @ ( B @ ( A @ morphism ) ) ) )
| ~ $true
| ( ( B @ zero @ ( A @ apply ) )
= ( C @ zero ) ) ),
inference(paramod_ordered,[status(thm)],[118,101]) ).
thf(579,plain,
! [C: $i,B: $i,A: $i] :
( ( ( c @ ( b @ ( beta @ morphism ) ) )
!= ( C @ ( B @ ( A @ morphism ) ) ) )
| ( ( B @ zero @ ( A @ apply ) )
= ( C @ zero ) ) ),
inference(simp,[status(thm)],[578]) ).
thf(580,plain,
( ( b @ zero @ ( beta @ apply ) )
= ( c @ zero ) ),
inference(pattern_uni,[status(thm)],[579:[bind(A,$thf( beta )),bind(B,$thf( b )),bind(C,$thf( c ))]]) ).
thf(3808,plain,
! [A: $i] :
( ( ( A @ zero )
!= ( b @ zero ) )
| ( ( e @ zero @ ( beta @ apply ) )
= ( c @ zero ) )
| ~ ( A @ ( b @ ( g @ morphism ) ) ) ),
inference(paramod_ordered,[status(thm)],[826,580]) ).
thf(3809,plain,
( ( ( e @ zero @ ( beta @ apply ) )
= ( c @ zero ) )
| ~ ( b @ ( b @ ( g @ morphism ) ) ) ),
inference(pattern_uni,[status(thm)],[3808:[bind(A,$thf( b ))]]) ).
thf(8879,plain,
( ( ( b @ ( b @ ( g @ morphism ) ) )
!= ( e @ ( b @ ( g @ morphism ) ) ) )
| ( ( e @ zero @ ( beta @ apply ) )
= ( c @ zero ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[57,3809]) ).
thf(8880,plain,
( ( ( b @ ( b @ ( g @ morphism ) ) )
!= ( e @ ( b @ ( g @ morphism ) ) ) )
| ( ( e @ zero @ ( beta @ apply ) )
= ( c @ zero ) ) ),
inference(simp,[status(thm)],[8879]) ).
thf(9008,plain,
( ( b != e )
| ( b != b )
| ( g != g )
| ( ( e @ zero @ ( beta @ apply ) )
= ( c @ zero ) ) ),
inference(simp,[status(thm)],[8880]) ).
thf(9111,plain,
( ( b != e )
| ( ( e @ zero @ ( beta @ apply ) )
= ( c @ zero ) ) ),
inference(simp,[status(thm)],[9008]) ).
thf(3713,plain,
! [A: $i] :
( ( ( A @ zero )
!= ( b @ zero ) )
| ( ( e @ zero @ ( g @ apply ) )
= ( e @ zero ) )
| ~ ( A @ ( b @ ( g @ morphism ) ) ) ),
inference(paramod_ordered,[status(thm)],[826,559]) ).
thf(3714,plain,
( ( ( e @ zero @ ( g @ apply ) )
= ( e @ zero ) )
| ~ ( b @ ( b @ ( g @ morphism ) ) ) ),
inference(pattern_uni,[status(thm)],[3713:[bind(A,$thf( b ))]]) ).
thf(3911,plain,
( ( ( b @ ( b @ ( g @ morphism ) ) )
!= ( e @ ( b @ ( g @ morphism ) ) ) )
| ( ( e @ zero @ ( g @ apply ) )
= ( e @ zero ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[57,3714]) ).
thf(3912,plain,
( ( ( b @ ( b @ ( g @ morphism ) ) )
!= ( e @ ( b @ ( g @ morphism ) ) ) )
| ( ( e @ zero @ ( g @ apply ) )
= ( e @ zero ) ) ),
inference(simp,[status(thm)],[3911]) ).
thf(3993,plain,
( ( b != e )
| ( b != b )
| ( g != g )
| ( ( e @ zero @ ( g @ apply ) )
= ( e @ zero ) ) ),
inference(simp,[status(thm)],[3912]) ).
thf(4072,plain,
( ( b != e )
| ( ( e @ zero @ ( g @ apply ) )
= ( e @ zero ) ) ),
inference(simp,[status(thm)],[3993]) ).
thf(1,conjecture,
! [A: $i] :
( ( e @ ( A @ element ) )
=> ? [B: $i,C: $i] :
( ( ( C @ ( g @ apply ) @ ( delta @ apply ) )
= B )
& ( ( C @ ( beta @ apply ) @ ( h @ apply ) )
= B )
& ( b @ ( C @ element ) )
& ( ( A @ ( delta @ apply ) )
= B )
& ( r @ ( B @ element ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',lemma3) ).
thf(2,negated_conjecture,
~ ! [A: $i] :
( ( e @ ( A @ element ) )
=> ? [B: $i,C: $i] :
( ( ( C @ ( g @ apply ) @ ( delta @ apply ) )
= B )
& ( ( C @ ( beta @ apply ) @ ( h @ apply ) )
= B )
& ( b @ ( C @ element ) )
& ( ( A @ ( delta @ apply ) )
= B )
& ( r @ ( B @ element ) ) ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(33,plain,
~ ! [A: $i] :
( ( e @ ( A @ element ) )
=> ? [B: $i,C: $i] :
( ( ( C @ ( g @ apply ) @ ( delta @ apply ) )
= B )
& ( ( C @ ( beta @ apply ) @ ( h @ apply ) )
= B )
& ( b @ ( C @ element ) )
& ( ( A @ ( delta @ apply ) )
= B )
& ( r @ ( B @ element ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(34,plain,
~ ! [A: $i] :
( ( e @ ( A @ element ) )
=> ? [B: $i] :
( ? [C: $i] :
( ( ( C @ ( g @ apply ) @ ( delta @ apply ) )
= B )
& ( ( C @ ( beta @ apply ) @ ( h @ apply ) )
= B )
& ( b @ ( C @ element ) ) )
& ( ( A @ ( delta @ apply ) )
= B )
& ( r @ ( B @ element ) ) ) ),
inference(miniscope,[status(thm)],[33]) ).
thf(35,plain,
! [B: $i,A: $i] :
( ( ( ( B @ ( g @ apply ) @ ( delta @ apply ) )
!= A )
| ( ( B @ ( beta @ apply ) @ ( h @ apply ) )
!= A )
| ~ ( b @ ( B @ element ) )
| ( ( sk1 @ ( delta @ apply ) )
!= A )
| ~ ( r @ ( A @ element ) ) )
& ( e @ ( sk1 @ element ) ) ),
inference(cnf,[status(esa)],[34]) ).
thf(36,plain,
e @ ( sk1 @ element ),
inference(cnfConj,[status(thm)],[35]) ).
thf(37,plain,
! [B: $i,A: $i] :
( ( ( B @ ( g @ apply ) @ ( delta @ apply ) )
!= A )
| ( ( B @ ( beta @ apply ) @ ( h @ apply ) )
!= A )
| ~ ( b @ ( B @ element ) )
| ( ( sk1 @ ( delta @ apply ) )
!= A )
| ~ ( r @ ( A @ element ) ) ),
inference(cnfConj,[status(thm)],[35]) ).
thf(38,plain,
! [B: $i,A: $i] :
( ~ ( b @ ( B @ element ) )
| ~ ( r @ ( A @ element ) )
| ( ( B @ ( g @ apply ) @ ( delta @ apply ) )
!= A )
| ( ( B @ ( beta @ apply ) @ ( h @ apply ) )
!= A )
| ( ( sk1 @ ( delta @ apply ) )
!= A ) ),
inference(lifteq,[status(thm)],[37]) ).
thf(39,plain,
! [A: $i] :
( ~ ( b @ ( A @ element ) )
| ~ ( r @ ( sk1 @ ( delta @ apply ) @ element ) )
| ( ( A @ ( g @ apply ) @ ( delta @ apply ) )
!= ( sk1 @ ( delta @ apply ) ) )
| ( ( A @ ( beta @ apply ) @ ( h @ apply ) )
!= ( sk1 @ ( delta @ apply ) ) ) ),
inference(simp,[status(thm)],[38]) ).
thf(163,plain,
! [A: $i] :
( ( ( e @ ( sk1 @ element ) )
!= ( b @ ( A @ element ) ) )
| ~ $true
| ~ ( r @ ( sk1 @ ( delta @ apply ) @ element ) )
| ( ( A @ ( g @ apply ) @ ( delta @ apply ) )
!= ( sk1 @ ( delta @ apply ) ) )
| ( ( A @ ( beta @ apply ) @ ( h @ apply ) )
!= ( sk1 @ ( delta @ apply ) ) ) ),
inference(paramod_ordered,[status(thm)],[36,39]) ).
thf(164,plain,
! [A: $i] :
( ( ( e @ ( sk1 @ element ) )
!= ( b @ ( A @ element ) ) )
| ~ ( r @ ( sk1 @ ( delta @ apply ) @ element ) )
| ( ( A @ ( g @ apply ) @ ( delta @ apply ) )
!= ( sk1 @ ( delta @ apply ) ) )
| ( ( A @ ( beta @ apply ) @ ( h @ apply ) )
!= ( sk1 @ ( delta @ apply ) ) ) ),
inference(simp,[status(thm)],[163]) ).
thf(182,plain,
! [A: $i] :
( ( b != e )
| ( sk1 != A )
| ~ ( r @ ( sk1 @ ( delta @ apply ) @ element ) )
| ( ( A @ ( g @ apply ) )
!= sk1 )
| ( delta != delta )
| ( ( A @ ( beta @ apply ) )
!= sk1 )
| ( h != delta ) ),
inference(simp,[status(thm)],[164]) ).
thf(194,plain,
( ( b != e )
| ~ ( r @ ( sk1 @ ( delta @ apply ) @ element ) )
| ( ( sk1 @ ( g @ apply ) )
!= sk1 )
| ( ( sk1 @ ( beta @ apply ) )
!= sk1 )
| ( h != delta ) ),
inference(simp,[status(thm)],[182]) ).
thf(196,plain,
( ( ( r @ ( sk1 @ ( delta @ apply ) @ element ) )
!= ( e @ ( sk1 @ element ) ) )
| ( b != e )
| ~ $true
| ( ( sk1 @ ( g @ apply ) )
!= sk1 )
| ( ( sk1 @ ( beta @ apply ) )
!= sk1 )
| ( h != delta ) ),
inference(paramod_ordered,[status(thm)],[36,194]) ).
thf(197,plain,
( ( ( r @ ( sk1 @ ( delta @ apply ) @ element ) )
!= ( e @ ( sk1 @ element ) ) )
| ( b != e )
| ( ( sk1 @ ( g @ apply ) )
!= sk1 )
| ( ( sk1 @ ( beta @ apply ) )
!= sk1 )
| ( h != delta ) ),
inference(simp,[status(thm)],[196]) ).
thf(199,plain,
( ( r != e )
| ( ( sk1 @ ( delta @ apply ) )
!= sk1 )
| ( b != e )
| ( ( sk1 @ ( g @ apply ) )
!= sk1 )
| ( ( sk1 @ ( beta @ apply ) )
!= sk1 )
| ( h != delta ) ),
inference(simp,[status(thm)],[197]) ).
thf(376,plain,
( ( sk1 != sk1 )
| ( ( sk1 @ ( g @ apply ) )
!= ( sk1 @ ( delta @ apply ) ) )
| ( r != e )
| ( ( sk1 @ ( delta @ apply ) )
!= sk1 )
| ( b != e )
| ( ( sk1 @ ( beta @ apply ) )
!= sk1 )
| ( h != delta ) ),
inference(eqfactor_ordered,[status(thm)],[199]) ).
thf(380,plain,
( ( sk1 != sk1 )
| ( g != delta )
| ( r != e )
| ( ( sk1 @ ( delta @ apply ) )
!= sk1 )
| ( b != e )
| ( ( sk1 @ ( beta @ apply ) )
!= sk1 )
| ( h != delta ) ),
inference(simp,[status(thm)],[376]) ).
thf(382,plain,
( ( g != delta )
| ( r != e )
| ( ( sk1 @ ( delta @ apply ) )
!= sk1 )
| ( b != e )
| ( ( sk1 @ ( beta @ apply ) )
!= sk1 )
| ( h != delta ) ),
inference(simp,[status(thm)],[380]) ).
thf(4185,plain,
( ( ( e @ zero @ ( g @ apply ) )
!= ( sk1 @ ( delta @ apply ) ) )
| ( g != delta )
| ( r != e )
| ( ( e @ zero )
!= sk1 )
| ( b != e )
| ( ( sk1 @ ( beta @ apply ) )
!= sk1 )
| ( h != delta )
| ( b != e ) ),
inference(paramod_ordered,[status(thm)],[4072,382]) ).
thf(4186,plain,
( ( ( e @ zero @ ( g @ apply ) )
!= ( sk1 @ ( delta @ apply ) ) )
| ( g != delta )
| ( r != e )
| ( ( e @ zero )
!= sk1 )
| ( ( sk1 @ ( beta @ apply ) )
!= sk1 )
| ( h != delta )
| ( b != e ) ),
inference(simp,[status(thm)],[4185]) ).
thf(4272,plain,
( ( ( e @ zero )
!= sk1 )
| ( g != delta )
| ( g != delta )
| ( r != e )
| ( ( e @ zero )
!= sk1 )
| ( ( sk1 @ ( beta @ apply ) )
!= sk1 )
| ( h != delta )
| ( b != e ) ),
inference(simp,[status(thm)],[4186]) ).
thf(4330,plain,
( ( g != delta )
| ( r != e )
| ( ( e @ zero )
!= sk1 )
| ( ( sk1 @ ( beta @ apply ) )
!= sk1 )
| ( h != delta )
| ( b != e ) ),
inference(simp,[status(thm)],[4272]) ).
thf(9312,plain,
( ( ( e @ zero @ ( beta @ apply ) )
!= ( sk1 @ ( beta @ apply ) ) )
| ( g != delta )
| ( r != e )
| ( ( e @ zero )
!= sk1 )
| ( ( c @ zero )
!= sk1 )
| ( h != delta )
| ( b != e )
| ( b != e ) ),
inference(paramod_ordered,[status(thm)],[9111,4330]) ).
thf(9313,plain,
( ( ( e @ zero @ ( beta @ apply ) )
!= ( sk1 @ ( beta @ apply ) ) )
| ( g != delta )
| ( r != e )
| ( ( e @ zero )
!= sk1 )
| ( ( c @ zero )
!= sk1 )
| ( h != delta )
| ( b != e ) ),
inference(simp,[status(thm)],[9312]) ).
thf(9388,plain,
( ( ( e @ zero )
!= sk1 )
| ( beta != beta )
| ( g != delta )
| ( r != e )
| ( ( e @ zero )
!= sk1 )
| ( ( c @ zero )
!= sk1 )
| ( h != delta )
| ( b != e ) ),
inference(simp,[status(thm)],[9313]) ).
thf(9469,plain,
( ( g != delta )
| ( r != e )
| ( ( e @ zero )
!= sk1 )
| ( ( c @ zero )
!= sk1 )
| ( h != delta )
| ( b != e ) ),
inference(simp,[status(thm)],[9388]) ).
thf(198,plain,
( ( sk1 != sk1 )
| ( ( sk1 @ ( g @ apply ) )
!= ( sk1 @ ( beta @ apply ) ) )
| ( b != e )
| ~ ( r @ ( sk1 @ ( delta @ apply ) @ element ) )
| ( ( sk1 @ ( beta @ apply ) )
!= sk1 )
| ( h != delta ) ),
inference(eqfactor_ordered,[status(thm)],[194]) ).
thf(201,plain,
( ( sk1 != sk1 )
| ( g != beta )
| ( b != e )
| ~ ( r @ ( sk1 @ ( delta @ apply ) @ element ) )
| ( ( sk1 @ ( beta @ apply ) )
!= sk1 )
| ( h != delta ) ),
inference(simp,[status(thm)],[198]) ).
thf(202,plain,
( ( g != beta )
| ( b != e )
| ~ ( r @ ( sk1 @ ( delta @ apply ) @ element ) )
| ( ( sk1 @ ( beta @ apply ) )
!= sk1 )
| ( h != delta ) ),
inference(simp,[status(thm)],[201]) ).
thf(7,axiom,
r @ ( c @ ( h @ morphism ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',h_morphism) ).
thf(44,plain,
r @ ( c @ ( h @ morphism ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(575,plain,
! [C: $i,B: $i,A: $i] :
( ( ( r @ ( c @ ( h @ morphism ) ) )
!= ( C @ ( B @ ( A @ morphism ) ) ) )
| ~ $true
| ( ( B @ zero @ ( A @ apply ) )
= ( C @ zero ) ) ),
inference(paramod_ordered,[status(thm)],[44,101]) ).
thf(576,plain,
! [C: $i,B: $i,A: $i] :
( ( ( r @ ( c @ ( h @ morphism ) ) )
!= ( C @ ( B @ ( A @ morphism ) ) ) )
| ( ( B @ zero @ ( A @ apply ) )
= ( C @ zero ) ) ),
inference(simp,[status(thm)],[575]) ).
thf(577,plain,
( ( c @ zero @ ( h @ apply ) )
= ( r @ zero ) ),
inference(pattern_uni,[status(thm)],[576:[bind(A,$thf( h )),bind(B,$thf( c )),bind(C,$thf( r ))]]) ).
thf(383,plain,
( ( sk1 != sk1 )
| ( ( sk1 @ ( beta @ apply ) )
!= ( sk1 @ ( delta @ apply ) ) )
| ( g != delta )
| ( r != e )
| ( ( sk1 @ ( delta @ apply ) )
!= sk1 )
| ( b != e )
| ( h != delta ) ),
inference(eqfactor_ordered,[status(thm)],[382]) ).
thf(385,plain,
( ( sk1 != sk1 )
| ( beta != delta )
| ( g != delta )
| ( r != e )
| ( ( sk1 @ ( delta @ apply ) )
!= sk1 )
| ( b != e )
| ( h != delta ) ),
inference(simp,[status(thm)],[383]) ).
thf(386,plain,
( ( beta != delta )
| ( g != delta )
| ( r != e )
| ( ( sk1 @ ( delta @ apply ) )
!= sk1 )
| ( b != e )
| ( h != delta ) ),
inference(simp,[status(thm)],[385]) ).
thf(1091,plain,
( ( ( c @ zero @ ( h @ apply ) )
!= ( sk1 @ ( delta @ apply ) ) )
| ( beta != delta )
| ( g != delta )
| ( r != e )
| ( ( r @ zero )
!= sk1 )
| ( b != e )
| ( h != delta ) ),
inference(paramod_ordered,[status(thm)],[577,386]) ).
thf(1100,plain,
( ( ( c @ zero )
!= sk1 )
| ( h != delta )
| ( beta != delta )
| ( g != delta )
| ( r != e )
| ( ( r @ zero )
!= sk1 )
| ( b != e )
| ( h != delta ) ),
inference(simp,[status(thm)],[1091]) ).
thf(1174,plain,
( ( ( c @ zero )
!= sk1 )
| ( beta != delta )
| ( g != delta )
| ( r != e )
| ( ( r @ zero )
!= sk1 )
| ( b != e )
| ( h != delta ) ),
inference(simp,[status(thm)],[1100]) ).
thf(1703,plain,
( ( sk1 != sk1 )
| ( ( c @ zero )
!= ( r @ zero ) )
| ( beta != delta )
| ( g != delta )
| ( r != e )
| ( ( r @ zero )
!= sk1 )
| ( b != e )
| ( h != delta ) ),
inference(eqfactor_ordered,[status(thm)],[1174]) ).
thf(1705,plain,
( ( c != r )
| ( beta != delta )
| ( g != delta )
| ( r != e )
| ( ( r @ zero )
!= sk1 )
| ( b != e )
| ( h != delta ) ),
inference(simp,[status(thm)],[1703]) ).
thf(6,axiom,
d @ ( a @ ( f @ morphism ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f_morphism) ).
thf(43,plain,
d @ ( a @ ( f @ morphism ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(600,plain,
! [C: $i,B: $i,A: $i] :
( ( ( d @ ( a @ ( f @ morphism ) ) )
!= ( C @ ( B @ ( A @ morphism ) ) ) )
| ~ $true
| ( ( B @ zero @ ( A @ apply ) )
= ( C @ zero ) ) ),
inference(paramod_ordered,[status(thm)],[43,101]) ).
thf(601,plain,
! [C: $i,B: $i,A: $i] :
( ( ( d @ ( a @ ( f @ morphism ) ) )
!= ( C @ ( B @ ( A @ morphism ) ) ) )
| ( ( B @ zero @ ( A @ apply ) )
= ( C @ zero ) ) ),
inference(simp,[status(thm)],[600]) ).
thf(602,plain,
( ( a @ zero @ ( f @ apply ) )
= ( d @ zero ) ),
inference(pattern_uni,[status(thm)],[601:[bind(A,$thf( f )),bind(B,$thf( a )),bind(C,$thf( d ))]]) ).
thf(11,axiom,
b @ ( a @ ( alpha @ morphism ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',alpha_morphism) ).
thf(58,plain,
b @ ( a @ ( alpha @ morphism ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[11]) ).
thf(603,plain,
! [C: $i,B: $i,A: $i] :
( ( ( b @ ( a @ ( alpha @ morphism ) ) )
!= ( C @ ( B @ ( A @ morphism ) ) ) )
| ~ $true
| ( ( B @ zero @ ( A @ apply ) )
= ( C @ zero ) ) ),
inference(paramod_ordered,[status(thm)],[58,101]) ).
thf(604,plain,
! [C: $i,B: $i,A: $i] :
( ( ( b @ ( a @ ( alpha @ morphism ) ) )
!= ( C @ ( B @ ( A @ morphism ) ) ) )
| ( ( B @ zero @ ( A @ apply ) )
= ( C @ zero ) ) ),
inference(simp,[status(thm)],[603]) ).
thf(605,plain,
( ( a @ zero @ ( alpha @ apply ) )
= ( b @ zero ) ),
inference(pattern_uni,[status(thm)],[604:[bind(A,$thf( alpha )),bind(B,$thf( a )),bind(C,$thf( b ))]]) ).
thf(1562,plain,
( ( ( a @ zero @ ( f @ apply ) )
!= ( a @ zero @ ( alpha @ apply ) ) )
| ( ( d @ zero )
= ( b @ zero ) ) ),
inference(paramod_ordered,[status(thm)],[602,605]) ).
thf(1598,plain,
( ( ( a @ zero )
!= ( a @ zero ) )
| ( f != alpha )
| ( ( d @ zero )
= ( b @ zero ) ) ),
inference(simp,[status(thm)],[1562]) ).
thf(1667,plain,
( ( f != alpha )
| ( ( d @ zero )
= ( b @ zero ) ) ),
inference(simp,[status(thm)],[1598]) ).
thf(25,axiom,
e @ ( d @ ( gamma @ morphism ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gamma_morphism) ).
thf(102,plain,
e @ ( d @ ( gamma @ morphism ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[25]) ).
thf(570,plain,
! [C: $i,B: $i,A: $i] :
( ( ( e @ ( d @ ( gamma @ morphism ) ) )
!= ( C @ ( B @ ( A @ morphism ) ) ) )
| ~ $true
| ( ( B @ zero @ ( A @ apply ) )
= ( C @ zero ) ) ),
inference(paramod_ordered,[status(thm)],[102,101]) ).
thf(571,plain,
! [C: $i,B: $i,A: $i] :
( ( ( e @ ( d @ ( gamma @ morphism ) ) )
!= ( C @ ( B @ ( A @ morphism ) ) ) )
| ( ( B @ zero @ ( A @ apply ) )
= ( C @ zero ) ) ),
inference(simp,[status(thm)],[570]) ).
thf(572,plain,
( ( d @ zero @ ( gamma @ apply ) )
= ( e @ zero ) ),
inference(pattern_uni,[status(thm)],[571:[bind(A,$thf( gamma )),bind(B,$thf( d )),bind(C,$thf( e ))]]) ).
thf(1998,plain,
( ( ( d @ zero )
!= ( d @ zero ) )
| ( ( b @ zero @ ( gamma @ apply ) )
= ( e @ zero ) )
| ( f != alpha ) ),
inference(paramod_ordered,[status(thm)],[1667,572]) ).
thf(1999,plain,
( ( ( b @ zero @ ( gamma @ apply ) )
= ( e @ zero ) )
| ( f != alpha ) ),
inference(pattern_uni,[status(thm)],[1998:[]]) ).
thf(203,plain,
( ( ( r @ ( sk1 @ ( delta @ apply ) @ element ) )
!= ( e @ ( sk1 @ element ) ) )
| ( g != beta )
| ( b != e )
| ~ $true
| ( ( sk1 @ ( beta @ apply ) )
!= sk1 )
| ( h != delta ) ),
inference(paramod_ordered,[status(thm)],[36,202]) ).
thf(204,plain,
( ( ( r @ ( sk1 @ ( delta @ apply ) @ element ) )
!= ( e @ ( sk1 @ element ) ) )
| ( g != beta )
| ( b != e )
| ( ( sk1 @ ( beta @ apply ) )
!= sk1 )
| ( h != delta ) ),
inference(simp,[status(thm)],[203]) ).
thf(205,plain,
( ( r != e )
| ( ( sk1 @ ( delta @ apply ) )
!= sk1 )
| ( g != beta )
| ( b != e )
| ( ( sk1 @ ( beta @ apply ) )
!= sk1 )
| ( h != delta ) ),
inference(simp,[status(thm)],[204]) ).
thf(206,plain,
( ( sk1 != sk1 )
| ( ( sk1 @ ( beta @ apply ) )
!= ( sk1 @ ( delta @ apply ) ) )
| ( r != e )
| ( ( sk1 @ ( delta @ apply ) )
!= sk1 )
| ( g != beta )
| ( b != e )
| ( h != delta ) ),
inference(eqfactor_ordered,[status(thm)],[205]) ).
thf(208,plain,
( ( sk1 != sk1 )
| ( beta != delta )
| ( r != e )
| ( ( sk1 @ ( delta @ apply ) )
!= sk1 )
| ( g != beta )
| ( b != e )
| ( h != delta ) ),
inference(simp,[status(thm)],[206]) ).
thf(209,plain,
( ( beta != delta )
| ( r != e )
| ( ( sk1 @ ( delta @ apply ) )
!= sk1 )
| ( g != beta )
| ( b != e )
| ( h != delta ) ),
inference(simp,[status(thm)],[208]) ).
thf(1077,plain,
( ( ( c @ zero @ ( h @ apply ) )
!= ( sk1 @ ( delta @ apply ) ) )
| ( beta != delta )
| ( r != e )
| ( ( r @ zero )
!= sk1 )
| ( g != beta )
| ( b != e )
| ( h != delta ) ),
inference(paramod_ordered,[status(thm)],[577,209]) ).
thf(1114,plain,
( ( ( c @ zero )
!= sk1 )
| ( h != delta )
| ( beta != delta )
| ( r != e )
| ( ( r @ zero )
!= sk1 )
| ( g != beta )
| ( b != e )
| ( h != delta ) ),
inference(simp,[status(thm)],[1077]) ).
thf(1184,plain,
( ( ( c @ zero )
!= sk1 )
| ( beta != delta )
| ( r != e )
| ( ( r @ zero )
!= sk1 )
| ( g != beta )
| ( b != e )
| ( h != delta ) ),
inference(simp,[status(thm)],[1114]) ).
thf(2137,plain,
( ( sk1 != sk1 )
| ( ( c @ zero )
!= ( r @ zero ) )
| ( beta != delta )
| ( r != e )
| ( ( r @ zero )
!= sk1 )
| ( g != beta )
| ( b != e )
| ( h != delta ) ),
inference(eqfactor_ordered,[status(thm)],[1184]) ).
thf(2141,plain,
( ( c != r )
| ( beta != delta )
| ( r != e )
| ( ( r @ zero )
!= sk1 )
| ( g != beta )
| ( b != e )
| ( h != delta ) ),
inference(simp,[status(thm)],[2137]) ).
thf(384,plain,
( ( ( sk1 @ ( beta @ apply ) )
!= ( sk1 @ ( delta @ apply ) ) )
| ( g != delta )
| ( r != e )
| ( ( sk1 @ ( delta @ apply ) )
!= sk1 )
| ( b != e )
| ( h != delta ) ),
inference(simp,[status(thm)],[383]) ).
thf(55,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( A @ surjection )
| ( ( D @ ( A @ apply ) )
!= ( A @ ( B @ ( C @ sk3 ) ) ) )
| ~ ( B @ ( D @ element ) )
| ~ ( C @ ( B @ ( A @ morphism ) ) ) ),
inference(cnfConj,[status(thm)],[53]) ).
thf(56,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( A @ surjection )
| ~ ( B @ ( D @ element ) )
| ~ ( C @ ( B @ ( A @ morphism ) ) )
| ( ( D @ ( A @ apply ) )
!= ( A @ ( B @ ( C @ sk3 ) ) ) ) ),
inference(lifteq,[status(thm)],[55]) ).
thf(5,axiom,
f @ surjection,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f_surjection) ).
thf(42,plain,
f @ surjection,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(3782,plain,
! [A: $i] :
( ( ( A @ zero )
!= ( d @ zero ) )
| ( ( e @ zero @ ( gamma @ apply ) )
= ( e @ zero ) )
| ~ ( A @ ( b @ ( g @ morphism ) ) ) ),
inference(paramod_ordered,[status(thm)],[826,572]) ).
thf(3783,plain,
( ( ( e @ zero @ ( gamma @ apply ) )
= ( e @ zero ) )
| ~ ( d @ ( b @ ( g @ morphism ) ) ) ),
inference(pattern_uni,[status(thm)],[3782:[bind(A,$thf( d ))]]) ).
thf(6867,plain,
( ( ( d @ ( b @ ( g @ morphism ) ) )
!= ( e @ ( b @ ( g @ morphism ) ) ) )
| ( ( e @ zero @ ( gamma @ apply ) )
= ( e @ zero ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[57,3783]) ).
thf(6868,plain,
( ( ( d @ ( b @ ( g @ morphism ) ) )
!= ( e @ ( b @ ( g @ morphism ) ) ) )
| ( ( e @ zero @ ( gamma @ apply ) )
= ( e @ zero ) ) ),
inference(simp,[status(thm)],[6867]) ).
thf(6975,plain,
( ( d != e )
| ( b != b )
| ( g != g )
| ( ( e @ zero @ ( gamma @ apply ) )
= ( e @ zero ) ) ),
inference(simp,[status(thm)],[6868]) ).
thf(7079,plain,
( ( d != e )
| ( ( e @ zero @ ( gamma @ apply ) )
= ( e @ zero ) ) ),
inference(simp,[status(thm)],[6975]) ).
thf(884,plain,
! [C: $i,B: $i,A: $i] :
( ( ( b @ ( a @ ( alpha @ morphism ) ) )
!= ( C @ ( B @ ( A @ morphism ) ) ) )
| ( A @ surjection )
| ( C @ ( A @ ( B @ ( C @ sk3 ) ) @ element ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[58,54]) ).
thf(885,plain,
! [C: $i,B: $i,A: $i] :
( ( ( b @ ( a @ ( alpha @ morphism ) ) )
!= ( C @ ( B @ ( A @ morphism ) ) ) )
| ( A @ surjection )
| ( C @ ( A @ ( B @ ( C @ sk3 ) ) @ element ) ) ),
inference(simp,[status(thm)],[884]) ).
thf(886,plain,
( ( alpha @ surjection )
| ( b @ ( alpha @ ( a @ ( b @ sk3 ) ) @ element ) ) ),
inference(pattern_uni,[status(thm)],[885:[bind(A,$thf( alpha )),bind(B,$thf( a )),bind(C,$thf( b ))]]) ).
thf(2855,plain,
! [B: $i,A: $i] :
( ( ( b @ ( alpha @ ( a @ ( b @ sk3 ) ) @ element ) )
!= ( A @ ( B @ element ) ) )
| ~ $true
| ( ( B @ ( B @ ( A @ subtract ) ) )
= ( A @ zero ) )
| ( alpha @ surjection ) ),
inference(paramod_ordered,[status(thm)],[886,89]) ).
thf(2856,plain,
! [B: $i,A: $i] :
( ( ( b @ ( alpha @ ( a @ ( b @ sk3 ) ) @ element ) )
!= ( A @ ( B @ element ) ) )
| ( ( B @ ( B @ ( A @ subtract ) ) )
= ( A @ zero ) )
| ( alpha @ surjection ) ),
inference(simp,[status(thm)],[2855]) ).
thf(2857,plain,
( ( ( alpha @ ( a @ ( b @ sk3 ) ) @ ( alpha @ ( a @ ( b @ sk3 ) ) @ ( b @ subtract ) ) )
= ( b @ zero ) )
| ( alpha @ surjection ) ),
inference(pattern_uni,[status(thm)],[2856:[bind(A,$thf( b )),bind(B,$thf( alpha @ ( a @ ( b @ sk3 ) ) ))]]) ).
thf(542,plain,
! [B: $i,A: $i] :
( ( ( e @ ( sk1 @ element ) )
!= ( A @ ( B @ element ) ) )
| ~ $true
| ( ( B @ ( B @ ( A @ subtract ) ) )
= ( A @ zero ) ) ),
inference(paramod_ordered,[status(thm)],[36,89]) ).
thf(543,plain,
! [B: $i,A: $i] :
( ( ( e @ ( sk1 @ element ) )
!= ( A @ ( B @ element ) ) )
| ( ( B @ ( B @ ( A @ subtract ) ) )
= ( A @ zero ) ) ),
inference(simp,[status(thm)],[542]) ).
thf(544,plain,
( ( sk1 @ ( sk1 @ ( e @ subtract ) ) )
= ( e @ zero ) ),
inference(pattern_uni,[status(thm)],[543:[bind(A,$thf( e )),bind(B,$thf( sk1 ))]]) ).
thf(5793,plain,
( ( ( alpha @ ( a @ ( b @ sk3 ) ) @ ( alpha @ ( a @ ( b @ sk3 ) ) @ ( b @ subtract ) ) )
!= ( sk1 @ ( sk1 @ ( e @ subtract ) ) ) )
| ( ( b @ zero )
= ( e @ zero ) )
| ( alpha @ surjection ) ),
inference(paramod_ordered,[status(thm)],[544,2857]) ).
thf(5794,plain,
( ( ( alpha @ ( a @ ( b @ sk3 ) ) )
!= sk1 )
| ( ( alpha @ ( a @ ( b @ sk3 ) ) )
!= sk1 )
| ( b != e )
| ( ( b @ zero )
= ( e @ zero ) )
| ( alpha @ surjection ) ),
inference(simp,[status(thm)],[5793]) ).
thf(5802,plain,
( ( ( alpha @ ( a @ ( b @ sk3 ) ) )
!= sk1 )
| ( b != e )
| ( ( b @ zero )
= ( e @ zero ) )
| ( alpha @ surjection ) ),
inference(simp,[status(thm)],[5794]) ).
thf(1228,plain,
( ( ( b @ zero @ ( g @ apply ) )
!= ( b @ zero @ ( beta @ apply ) ) )
| ( ( c @ zero )
= ( e @ zero ) ) ),
inference(paramod_ordered,[status(thm)],[559,580]) ).
thf(1270,plain,
( ( ( b @ zero )
!= ( b @ zero ) )
| ( g != beta )
| ( ( c @ zero )
= ( e @ zero ) ) ),
inference(simp,[status(thm)],[1228]) ).
thf(1345,plain,
( ( g != beta )
| ( ( c @ zero )
= ( e @ zero ) ) ),
inference(simp,[status(thm)],[1270]) ).
thf(1961,plain,
( ( ( c @ zero )
!= ( c @ zero ) )
| ( ( e @ zero @ ( h @ apply ) )
= ( r @ zero ) )
| ( g != beta ) ),
inference(paramod_ordered,[status(thm)],[1345,577]) ).
thf(1962,plain,
( ( ( e @ zero @ ( h @ apply ) )
= ( r @ zero ) )
| ( g != beta ) ),
inference(pattern_uni,[status(thm)],[1961:[]]) ).
thf(4118,plain,
( ( ( e @ zero @ ( g @ apply ) )
!= ( sk1 @ ( beta @ apply ) ) )
| ( g != beta )
| ( b != e )
| ~ ( r @ ( sk1 @ ( delta @ apply ) @ element ) )
| ( ( e @ zero )
!= sk1 )
| ( h != delta )
| ( b != e ) ),
inference(paramod_ordered,[status(thm)],[4072,202]) ).
thf(4119,plain,
( ( ( e @ zero @ ( g @ apply ) )
!= ( sk1 @ ( beta @ apply ) ) )
| ( g != beta )
| ~ ( r @ ( sk1 @ ( delta @ apply ) @ element ) )
| ( ( e @ zero )
!= sk1 )
| ( h != delta )
| ( b != e ) ),
inference(simp,[status(thm)],[4118]) ).
thf(4245,plain,
( ( ( e @ zero )
!= sk1 )
| ( g != beta )
| ( g != beta )
| ~ ( r @ ( sk1 @ ( delta @ apply ) @ element ) )
| ( ( e @ zero )
!= sk1 )
| ( h != delta )
| ( b != e ) ),
inference(simp,[status(thm)],[4119]) ).
thf(4310,plain,
( ( g != beta )
| ~ ( r @ ( sk1 @ ( delta @ apply ) @ element ) )
| ( ( e @ zero )
!= sk1 )
| ( h != delta )
| ( b != e ) ),
inference(simp,[status(thm)],[4245]) ).
thf(4388,plain,
( ( ( e @ zero @ ( h @ apply ) )
!= ( sk1 @ ( delta @ apply ) ) )
| ( g != beta )
| ~ ( r @ ( r @ zero @ element ) )
| ( ( e @ zero )
!= sk1 )
| ( h != delta )
| ( b != e )
| ( g != beta ) ),
inference(paramod_ordered,[status(thm)],[1962,4310]) ).
thf(4389,plain,
( ( ( e @ zero @ ( h @ apply ) )
!= ( sk1 @ ( delta @ apply ) ) )
| ~ ( r @ ( r @ zero @ element ) )
| ( ( e @ zero )
!= sk1 )
| ( h != delta )
| ( b != e )
| ( g != beta ) ),
inference(simp,[status(thm)],[4388]) ).
thf(4393,plain,
( ( ( e @ zero )
!= sk1 )
| ( h != delta )
| ~ ( r @ ( r @ zero @ element ) )
| ( ( e @ zero )
!= sk1 )
| ( h != delta )
| ( b != e )
| ( g != beta ) ),
inference(simp,[status(thm)],[4389]) ).
thf(4414,plain,
( ~ ( r @ ( r @ zero @ element ) )
| ( ( e @ zero )
!= sk1 )
| ( h != delta )
| ( b != e )
| ( g != beta ) ),
inference(simp,[status(thm)],[4393]) ).
thf(4449,plain,
( ( ( r @ ( r @ zero @ element ) )
!= ( e @ ( sk1 @ element ) ) )
| ~ $true
| ( ( e @ zero )
!= sk1 )
| ( h != delta )
| ( b != e )
| ( g != beta ) ),
inference(paramod_ordered,[status(thm)],[36,4414]) ).
thf(4450,plain,
( ( ( r @ ( r @ zero @ element ) )
!= ( e @ ( sk1 @ element ) ) )
| ( ( e @ zero )
!= sk1 )
| ( h != delta )
| ( b != e )
| ( g != beta ) ),
inference(simp,[status(thm)],[4449]) ).
thf(4453,plain,
( ( r != e )
| ( ( r @ zero )
!= sk1 )
| ( ( e @ zero )
!= sk1 )
| ( h != delta )
| ( b != e )
| ( g != beta ) ),
inference(simp,[status(thm)],[4450]) ).
thf(4505,plain,
( ( sk1 != sk1 )
| ( ( r @ zero )
!= ( e @ zero ) )
| ( r != e )
| ( ( e @ zero )
!= sk1 )
| ( h != delta )
| ( b != e )
| ( g != beta ) ),
inference(eqfactor_ordered,[status(thm)],[4453]) ).
thf(4511,plain,
( ( r != e )
| ( r != e )
| ( ( e @ zero )
!= sk1 )
| ( h != delta )
| ( b != e )
| ( g != beta ) ),
inference(simp,[status(thm)],[4505]) ).
thf(4514,plain,
( ( r != e )
| ( ( e @ zero )
!= sk1 )
| ( h != delta )
| ( b != e )
| ( g != beta ) ),
inference(simp,[status(thm)],[4511]) ).
thf(30,axiom,
! [A: $i,B: $i,C: $i] :
( ( ! [D: $i,E: $i] :
( ( ( ( D @ ( A @ apply ) )
= ( E @ ( A @ apply ) ) )
& ( B @ ( E @ element ) )
& ( B @ ( D @ element ) ) )
=> ( D = E ) )
& ( C @ ( B @ ( A @ morphism ) ) ) )
=> ( A @ injection ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',properties_for_injection) ).
thf(119,plain,
! [A: $i,B: $i,C: $i] :
( ( ! [D: $i,E: $i] :
( ( ( ( D @ ( A @ apply ) )
= ( E @ ( A @ apply ) ) )
& ( B @ ( E @ element ) )
& ( B @ ( D @ element ) ) )
=> ( D = E ) )
& ( C @ ( B @ ( A @ morphism ) ) ) )
=> ( A @ injection ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[30]) ).
thf(120,plain,
! [A: $i] :
( ? [B: $i] :
( ! [C: $i,D: $i] :
( ( ( ( C @ ( A @ apply ) )
= ( D @ ( A @ apply ) ) )
& ( B @ ( D @ element ) )
& ( B @ ( C @ element ) ) )
=> ( C = D ) )
& ? [C: $i] : ( C @ ( B @ ( A @ morphism ) ) ) )
=> ( A @ injection ) ),
inference(miniscope,[status(thm)],[119]) ).
thf(121,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ injection )
| ( ( A @ ( B @ sk10 ) )
!= ( A @ ( B @ sk11 ) ) )
| ~ ( C @ ( B @ ( A @ morphism ) ) ) )
& ( ( A @ injection )
| ( ( A @ ( B @ sk10 ) @ ( A @ apply ) )
= ( A @ ( B @ sk11 ) @ ( A @ apply ) ) )
| ~ ( C @ ( B @ ( A @ morphism ) ) ) )
& ( ( A @ injection )
| ( B @ ( A @ ( B @ sk11 ) @ element ) )
| ~ ( C @ ( B @ ( A @ morphism ) ) ) )
& ( ( A @ injection )
| ( B @ ( A @ ( B @ sk10 ) @ element ) )
| ~ ( C @ ( B @ ( A @ morphism ) ) ) ) ),
inference(cnf,[status(esa)],[120]) ).
thf(122,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ injection )
| ( B @ ( A @ ( B @ sk10 ) @ element ) )
| ~ ( C @ ( B @ ( A @ morphism ) ) ) ),
inference(cnfConj,[status(thm)],[121]) ).
thf(7439,plain,
! [C: $i,B: $i,A: $i] :
( ( ( r @ ( c @ ( h @ morphism ) ) )
!= ( C @ ( B @ ( A @ morphism ) ) ) )
| ( A @ injection )
| ( B @ ( A @ ( B @ sk10 ) @ element ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[44,122]) ).
thf(7440,plain,
! [C: $i,B: $i,A: $i] :
( ( ( r @ ( c @ ( h @ morphism ) ) )
!= ( C @ ( B @ ( A @ morphism ) ) ) )
| ( A @ injection )
| ( B @ ( A @ ( B @ sk10 ) @ element ) ) ),
inference(simp,[status(thm)],[7439]) ).
thf(7441,plain,
( ( h @ injection )
| ( c @ ( h @ ( c @ sk10 ) @ element ) ) ),
inference(pattern_uni,[status(thm)],[7440:[bind(A,$thf( h )),bind(B,$thf( c )),bind(C,$thf( r ))]]) ).
thf(135,plain,
! [A: $i] :
( ~ ( b @ ( A @ element ) )
| ~ ( r @ ( sk1 @ ( delta @ apply ) @ element ) )
| ( ( A @ ( g @ apply ) )
!= sk1 )
| ( delta != delta )
| ( ( A @ ( beta @ apply ) )
!= sk1 )
| ( h != delta ) ),
inference(simp,[status(thm)],[39]) ).
thf(150,plain,
! [A: $i] :
( ~ ( b @ ( A @ element ) )
| ~ ( r @ ( sk1 @ ( delta @ apply ) @ element ) )
| ( ( A @ ( g @ apply ) )
!= sk1 )
| ( ( A @ ( beta @ apply ) )
!= sk1 )
| ( h != delta ) ),
inference(simp,[status(thm)],[135]) ).
thf(157,plain,
! [A: $i] :
( ( sk1 != sk1 )
| ( ( A @ ( g @ apply ) )
!= ( A @ ( beta @ apply ) ) )
| ~ ( b @ ( A @ element ) )
| ~ ( r @ ( sk1 @ ( delta @ apply ) @ element ) )
| ( ( A @ ( beta @ apply ) )
!= sk1 )
| ( h != delta ) ),
inference(eqfactor_ordered,[status(thm)],[150]) ).
thf(159,plain,
! [A: $i] :
( ( A != A )
| ( g != beta )
| ~ ( b @ ( A @ element ) )
| ~ ( r @ ( sk1 @ ( delta @ apply ) @ element ) )
| ( ( A @ ( beta @ apply ) )
!= sk1 )
| ( h != delta ) ),
inference(simp,[status(thm)],[157]) ).
thf(160,plain,
! [A: $i] :
( ( g != beta )
| ~ ( b @ ( A @ element ) )
| ~ ( r @ ( sk1 @ ( delta @ apply ) @ element ) )
| ( ( A @ ( beta @ apply ) )
!= sk1 )
| ( h != delta ) ),
inference(simp,[status(thm)],[159]) ).
thf(1218,plain,
! [A: $i] :
( ( ( b @ zero @ ( beta @ apply ) )
!= ( A @ ( beta @ apply ) ) )
| ( g != beta )
| ~ ( b @ ( A @ element ) )
| ~ ( r @ ( sk1 @ ( delta @ apply ) @ element ) )
| ( ( c @ zero )
!= sk1 )
| ( h != delta ) ),
inference(paramod_ordered,[status(thm)],[580,160]) ).
thf(1219,plain,
( ( g != beta )
| ~ ( b @ ( b @ zero @ element ) )
| ~ ( r @ ( sk1 @ ( delta @ apply ) @ element ) )
| ( ( c @ zero )
!= sk1 )
| ( h != delta ) ),
inference(pattern_uni,[status(thm)],[1218:[bind(A,$thf( b @ zero ))]]) ).
thf(2566,plain,
( ( ( c @ zero @ ( h @ apply ) )
!= ( sk1 @ ( delta @ apply ) ) )
| ( g != beta )
| ~ ( b @ ( b @ zero @ element ) )
| ~ ( r @ ( r @ zero @ element ) )
| ( ( c @ zero )
!= sk1 )
| ( h != delta ) ),
inference(paramod_ordered,[status(thm)],[577,1219]) ).
thf(2597,plain,
( ( ( c @ zero )
!= sk1 )
| ( h != delta )
| ( g != beta )
| ~ ( b @ ( b @ zero @ element ) )
| ~ ( r @ ( r @ zero @ element ) )
| ( ( c @ zero )
!= sk1 )
| ( h != delta ) ),
inference(simp,[status(thm)],[2566]) ).
thf(2618,plain,
( ( g != beta )
| ~ ( b @ ( b @ zero @ element ) )
| ~ ( r @ ( r @ zero @ element ) )
| ( ( c @ zero )
!= sk1 )
| ( h != delta ) ),
inference(simp,[status(thm)],[2597]) ).
thf(12,axiom,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ ( A @ morphism ) ) )
=> ! [D: $i,E: $i] :
( ( ( B @ ( E @ element ) )
& ( B @ ( D @ element ) ) )
=> ( ( E @ ( D @ ( B @ subtract ) ) @ ( A @ apply ) )
= ( E @ ( A @ apply ) @ ( D @ ( A @ apply ) @ ( C @ subtract ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',subtract_distribution) ).
thf(59,plain,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ ( A @ morphism ) ) )
=> ! [D: $i,E: $i] :
( ( ( B @ ( E @ element ) )
& ( B @ ( D @ element ) ) )
=> ( ( E @ ( D @ ( B @ subtract ) ) @ ( A @ apply ) )
= ( E @ ( A @ apply ) @ ( D @ ( A @ apply ) @ ( C @ subtract ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[12]) ).
thf(60,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( E @ ( D @ ( B @ subtract ) ) @ ( A @ apply ) )
= ( E @ ( A @ apply ) @ ( D @ ( A @ apply ) @ ( C @ subtract ) ) ) )
| ~ ( B @ ( E @ element ) )
| ~ ( B @ ( D @ element ) )
| ~ ( C @ ( B @ ( A @ morphism ) ) ) ),
inference(cnf,[status(esa)],[59]) ).
thf(61,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ ( B @ ( E @ element ) )
| ~ ( B @ ( D @ element ) )
| ~ ( C @ ( B @ ( A @ morphism ) ) )
| ( ( E @ ( D @ ( B @ subtract ) ) @ ( A @ apply ) )
= ( E @ ( A @ apply ) @ ( D @ ( A @ apply ) @ ( C @ subtract ) ) ) ) ),
inference(lifteq,[status(thm)],[60]) ).
thf(28,axiom,
beta @ surjection,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',beta_surjection) ).
thf(117,plain,
beta @ surjection,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[28]) ).
thf(3719,plain,
! [A: $i] :
( ( ( A @ zero )
!= ( a @ zero ) )
| ( ( e @ zero @ ( f @ apply ) )
= ( d @ zero ) )
| ~ ( A @ ( b @ ( g @ morphism ) ) ) ),
inference(paramod_ordered,[status(thm)],[826,602]) ).
thf(3720,plain,
( ( ( e @ zero @ ( f @ apply ) )
= ( d @ zero ) )
| ~ ( a @ ( b @ ( g @ morphism ) ) ) ),
inference(pattern_uni,[status(thm)],[3719:[bind(A,$thf( a ))]]) ).
thf(18,axiom,
! [A: $i,B: $i,C: $i] :
( ( ( A @ ( C @ element ) )
& ( A @ ( B @ element ) ) )
=> ( ( C @ ( B @ ( A @ subtract ) ) @ ( B @ ( A @ subtract ) ) )
= C ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',subtract_cancellation) ).
thf(83,plain,
! [A: $i,B: $i,C: $i] :
( ( ( A @ ( C @ element ) )
& ( A @ ( B @ element ) ) )
=> ( ( C @ ( B @ ( A @ subtract ) ) @ ( B @ ( A @ subtract ) ) )
= C ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[18]) ).
thf(84,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ subtract ) ) @ ( B @ ( A @ subtract ) ) )
= C )
| ~ ( A @ ( C @ element ) )
| ~ ( A @ ( B @ element ) ) ),
inference(cnf,[status(esa)],[83]) ).
thf(85,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( A @ ( C @ element ) )
| ~ ( A @ ( B @ element ) )
| ( ( C @ ( B @ ( A @ subtract ) ) @ ( B @ ( A @ subtract ) ) )
= C ) ),
inference(lifteq,[status(thm)],[84]) ).
thf(3762,plain,
! [A: $i] :
( ( ( A @ zero )
!= ( a @ zero ) )
| ( ( e @ zero @ ( alpha @ apply ) )
= ( b @ zero ) )
| ~ ( A @ ( b @ ( g @ morphism ) ) ) ),
inference(paramod_ordered,[status(thm)],[826,605]) ).
thf(3763,plain,
( ( ( e @ zero @ ( alpha @ apply ) )
= ( b @ zero ) )
| ~ ( a @ ( b @ ( g @ morphism ) ) ) ),
inference(pattern_uni,[status(thm)],[3762:[bind(A,$thf( a ))]]) ).
thf(207,plain,
( ( ( sk1 @ ( beta @ apply ) )
!= ( sk1 @ ( delta @ apply ) ) )
| ( r != e )
| ( ( sk1 @ ( delta @ apply ) )
!= sk1 )
| ( g != beta )
| ( b != e )
| ( h != delta ) ),
inference(simp,[status(thm)],[206]) ).
thf(1253,plain,
( ( ( b @ zero @ ( beta @ apply ) )
!= ( sk1 @ ( delta @ apply ) ) )
| ( ( sk1 @ ( beta @ apply ) )
!= ( sk1 @ ( delta @ apply ) ) )
| ( r != e )
| ( ( c @ zero )
!= sk1 )
| ( g != beta )
| ( b != e )
| ( h != delta ) ),
inference(paramod_ordered,[status(thm)],[580,207]) ).
thf(1308,plain,
( ( ( b @ zero )
!= sk1 )
| ( beta != delta )
| ( sk1 != sk1 )
| ( beta != delta )
| ( r != e )
| ( ( c @ zero )
!= sk1 )
| ( g != beta )
| ( b != e )
| ( h != delta ) ),
inference(simp,[status(thm)],[1253]) ).
thf(1329,plain,
( ( ( b @ zero )
!= sk1 )
| ( beta != delta )
| ( r != e )
| ( ( c @ zero )
!= sk1 )
| ( g != beta )
| ( b != e )
| ( h != delta ) ),
inference(simp,[status(thm)],[1308]) ).
thf(7433,plain,
! [C: $i,B: $i,A: $i] :
( ( ( e @ ( b @ ( g @ morphism ) ) )
!= ( C @ ( B @ ( A @ morphism ) ) ) )
| ( A @ injection )
| ( B @ ( A @ ( B @ sk10 ) @ element ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[57,122]) ).
thf(7434,plain,
! [C: $i,B: $i,A: $i] :
( ( ( e @ ( b @ ( g @ morphism ) ) )
!= ( C @ ( B @ ( A @ morphism ) ) ) )
| ( A @ injection )
| ( B @ ( A @ ( B @ sk10 ) @ element ) ) ),
inference(simp,[status(thm)],[7433]) ).
thf(7435,plain,
( ( g @ injection )
| ( b @ ( g @ ( b @ sk10 ) @ element ) ) ),
inference(pattern_uni,[status(thm)],[7434:[bind(A,$thf( g )),bind(B,$thf( b )),bind(C,$thf( e ))]]) ).
thf(23,axiom,
delta @ ( g @ ( h @ ( beta @ commute ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',beta_h_g_delta_commute) ).
thf(96,plain,
delta @ ( g @ ( h @ ( beta @ commute ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[23]) ).
thf(70,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i] :
( ( ( E @ ( D @ ( B @ morphism ) ) )
& ( D @ ( C @ ( A @ morphism ) ) )
& ( B @ ( A @ exact ) ) )
=> ( ! [F: $i] :
( ? [G: $i] :
( ( ( G @ ( A @ apply ) )
= F )
& ( C @ ( G @ element ) ) )
=> ( ( ( F @ ( B @ apply ) )
= ( E @ zero ) )
& ( D @ ( F @ element ) ) ) )
& ! [F: $i] :
( ( ( ( F @ ( B @ apply ) )
= ( E @ zero ) )
& ( D @ ( F @ element ) ) )
=> ? [G: $i] :
( ( ( G @ ( A @ apply ) )
= F )
& ( C @ ( G @ element ) ) ) ) ) ),
inference(miniscope,[status(thm)],[69]) ).
thf(71,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( ( G @ ( B @ apply ) )
= ( E @ zero ) )
| ( ( H @ ( A @ apply ) )
!= G )
| ~ ( C @ ( H @ element ) )
| ~ ( E @ ( D @ ( B @ morphism ) ) )
| ~ ( D @ ( C @ ( A @ morphism ) ) )
| ~ ( B @ ( A @ exact ) ) )
& ( ( D @ ( G @ element ) )
| ( ( H @ ( A @ apply ) )
!= G )
| ~ ( C @ ( H @ element ) )
| ~ ( E @ ( D @ ( B @ morphism ) ) )
| ~ ( D @ ( C @ ( A @ morphism ) ) )
| ~ ( B @ ( A @ exact ) ) )
& ( ( ( A @ ( B @ ( C @ ( D @ ( E @ ( F @ sk5 ) ) ) ) ) @ ( A @ apply ) )
= F )
| ( ( F @ ( B @ apply ) )
!= ( E @ zero ) )
| ~ ( D @ ( F @ element ) )
| ~ ( E @ ( D @ ( B @ morphism ) ) )
| ~ ( D @ ( C @ ( A @ morphism ) ) )
| ~ ( B @ ( A @ exact ) ) )
& ( ( C @ ( A @ ( B @ ( C @ ( D @ ( E @ ( F @ sk5 ) ) ) ) ) @ element ) )
| ( ( F @ ( B @ apply ) )
!= ( E @ zero ) )
| ~ ( D @ ( F @ element ) )
| ~ ( E @ ( D @ ( B @ morphism ) ) )
| ~ ( D @ ( C @ ( A @ morphism ) ) )
| ~ ( B @ ( A @ exact ) ) ) ),
inference(cnf,[status(esa)],[70]) ).
thf(73,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( C @ ( D @ ( E @ ( F @ sk5 ) ) ) ) ) @ ( A @ apply ) )
= F )
| ( ( F @ ( B @ apply ) )
!= ( E @ zero ) )
| ~ ( D @ ( F @ element ) )
| ~ ( E @ ( D @ ( B @ morphism ) ) )
| ~ ( D @ ( C @ ( A @ morphism ) ) )
| ~ ( B @ ( A @ exact ) ) ),
inference(cnfConj,[status(thm)],[71]) ).
thf(77,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ ( D @ ( F @ element ) )
| ~ ( E @ ( D @ ( B @ morphism ) ) )
| ~ ( D @ ( C @ ( A @ morphism ) ) )
| ~ ( B @ ( A @ exact ) )
| ( ( A @ ( B @ ( C @ ( D @ ( E @ ( F @ sk5 ) ) ) ) ) @ ( A @ apply ) )
= F )
| ( ( F @ ( B @ apply ) )
!= ( E @ zero ) ) ),
inference(lifteq,[status(thm)],[73]) ).
thf(7451,plain,
! [C: $i,B: $i,A: $i] :
( ( ( r @ ( e @ ( delta @ morphism ) ) )
!= ( C @ ( B @ ( A @ morphism ) ) ) )
| ( A @ injection )
| ( B @ ( A @ ( B @ sk10 ) @ element ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[82,122]) ).
thf(7452,plain,
! [C: $i,B: $i,A: $i] :
( ( ( r @ ( e @ ( delta @ morphism ) ) )
!= ( C @ ( B @ ( A @ morphism ) ) ) )
| ( A @ injection )
| ( B @ ( A @ ( B @ sk10 ) @ element ) ) ),
inference(simp,[status(thm)],[7451]) ).
thf(7453,plain,
( ( delta @ injection )
| ( e @ ( delta @ ( e @ sk10 ) @ element ) ) ),
inference(pattern_uni,[status(thm)],[7452:[bind(A,$thf( delta )),bind(B,$thf( e )),bind(C,$thf( r ))]]) ).
thf(1252,plain,
( ( ( b @ zero @ ( beta @ apply ) )
!= ( sk1 @ ( delta @ apply ) ) )
| ( beta != delta )
| ( g != delta )
| ( r != e )
| ( ( c @ zero )
!= sk1 )
| ( b != e )
| ( h != delta ) ),
inference(paramod_ordered,[status(thm)],[580,386]) ).
thf(1298,plain,
( ( ( b @ zero )
!= sk1 )
| ( beta != delta )
| ( beta != delta )
| ( g != delta )
| ( r != e )
| ( ( c @ zero )
!= sk1 )
| ( b != e )
| ( h != delta ) ),
inference(simp,[status(thm)],[1252]) ).
thf(1324,plain,
( ( ( b @ zero )
!= sk1 )
| ( beta != delta )
| ( g != delta )
| ( r != e )
| ( ( c @ zero )
!= sk1 )
| ( b != e )
| ( h != delta ) ),
inference(simp,[status(thm)],[1298]) ).
thf(32,axiom,
! [A: $i,B: $i,C: $i] :
( ( ( C @ ( B @ ( A @ morphism ) ) )
& ( A @ injection ) )
=> ! [D: $i,E: $i] :
( ( ( ( D @ ( A @ apply ) )
= ( E @ ( A @ apply ) ) )
& ( B @ ( E @ element ) )
& ( B @ ( D @ element ) ) )
=> ( D = E ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',injection_properties) ).
thf(129,plain,
! [A: $i,B: $i,C: $i] :
( ( ( C @ ( B @ ( A @ morphism ) ) )
& ( A @ injection ) )
=> ! [D: $i,E: $i] :
( ( ( ( D @ ( A @ apply ) )
= ( E @ ( A @ apply ) ) )
& ( B @ ( E @ element ) )
& ( B @ ( D @ element ) ) )
=> ( D = E ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[32]) ).
thf(3329,plain,
( ( sk1 != sk1 )
| ( ( c @ zero )
!= ( b @ zero ) )
| ( ( b @ zero )
!= sk1 )
| ( beta != delta )
| ( g != delta )
| ( r != e )
| ( b != e )
| ( h != delta ) ),
inference(eqfactor_ordered,[status(thm)],[1324]) ).
thf(3333,plain,
( ( c != b )
| ( ( b @ zero )
!= sk1 )
| ( beta != delta )
| ( g != delta )
| ( r != e )
| ( b != e )
| ( h != delta ) ),
inference(simp,[status(thm)],[3329]) ).
thf(4,axiom,
alpha @ injection,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',alpha_injection) ).
thf(41,plain,
alpha @ injection,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(31,axiom,
delta @ surjection,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',delta_surjection) ).
thf(128,plain,
delta @ surjection,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[31]) ).
thf(7442,plain,
! [C: $i,B: $i,A: $i] :
( ( ( c @ ( b @ ( beta @ morphism ) ) )
!= ( C @ ( B @ ( A @ morphism ) ) ) )
| ( A @ injection )
| ( B @ ( A @ ( B @ sk10 ) @ element ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[118,122]) ).
thf(7443,plain,
! [C: $i,B: $i,A: $i] :
( ( ( c @ ( b @ ( beta @ morphism ) ) )
!= ( C @ ( B @ ( A @ morphism ) ) ) )
| ( A @ injection )
| ( B @ ( A @ ( B @ sk10 ) @ element ) ) ),
inference(simp,[status(thm)],[7442]) ).
thf(7444,plain,
( ( beta @ injection )
| ( b @ ( beta @ ( b @ sk10 ) @ element ) ) ),
inference(pattern_uni,[status(thm)],[7443:[bind(A,$thf( beta )),bind(B,$thf( b )),bind(C,$thf( c ))]]) ).
thf(5279,plain,
( ( ( a @ ( b @ ( g @ morphism ) ) )
!= ( e @ ( b @ ( g @ morphism ) ) ) )
| ( ( e @ zero @ ( alpha @ apply ) )
= ( b @ zero ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[57,3763]) ).
thf(5280,plain,
( ( ( a @ ( b @ ( g @ morphism ) ) )
!= ( e @ ( b @ ( g @ morphism ) ) ) )
| ( ( e @ zero @ ( alpha @ apply ) )
= ( b @ zero ) ) ),
inference(simp,[status(thm)],[5279]) ).
thf(5458,plain,
( ( a != e )
| ( b != b )
| ( g != g )
| ( ( e @ zero @ ( alpha @ apply ) )
= ( b @ zero ) ) ),
inference(simp,[status(thm)],[5280]) ).
thf(5508,plain,
( ( a != e )
| ( ( e @ zero @ ( alpha @ apply ) )
= ( b @ zero ) ) ),
inference(simp,[status(thm)],[5458]) ).
thf(8,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i,G: $i,H: $i] :
( ( ! [I: $i] :
( ( E @ ( I @ element ) )
=> ( ( I @ ( A @ apply ) @ ( B @ apply ) )
= ( I @ ( C @ apply ) @ ( D @ apply ) ) ) )
& ( H @ ( G @ ( D @ morphism ) ) )
& ( G @ ( E @ ( C @ morphism ) ) )
& ( H @ ( F @ ( B @ morphism ) ) )
& ( F @ ( E @ ( A @ morphism ) ) ) )
=> ( D @ ( C @ ( B @ ( A @ commute ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',properties_for_commute) ).
thf(45,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i,G: $i,H: $i] :
( ( ! [I: $i] :
( ( E @ ( I @ element ) )
=> ( ( I @ ( A @ apply ) @ ( B @ apply ) )
= ( I @ ( C @ apply ) @ ( D @ apply ) ) ) )
& ( H @ ( G @ ( D @ morphism ) ) )
& ( G @ ( E @ ( C @ morphism ) ) )
& ( H @ ( F @ ( B @ morphism ) ) )
& ( F @ ( E @ ( A @ morphism ) ) ) )
=> ( D @ ( C @ ( B @ ( A @ commute ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(13,axiom,
! [A: $i,B: $i,C: $i] :
( ( ( C @ ( B @ ( A @ morphism ) ) )
& ( A @ surjection ) )
=> ! [D: $i] :
( ( C @ ( D @ element ) )
=> ? [E: $i] :
( ( ( E @ ( A @ apply ) )
= D )
& ( B @ ( E @ element ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',surjection_properties) ).
thf(62,plain,
! [A: $i,B: $i,C: $i] :
( ( ( C @ ( B @ ( A @ morphism ) ) )
& ( A @ surjection ) )
=> ! [D: $i] :
( ( C @ ( D @ element ) )
=> ? [E: $i] :
( ( ( E @ ( A @ apply ) )
= D )
& ( B @ ( E @ element ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[13]) ).
thf(63,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( ( A @ ( B @ ( C @ ( D @ sk4 ) ) ) @ ( A @ apply ) )
= D )
| ~ ( C @ ( D @ element ) )
| ~ ( C @ ( B @ ( A @ morphism ) ) )
| ~ ( A @ surjection ) )
& ( ( B @ ( A @ ( B @ ( C @ ( D @ sk4 ) ) ) @ element ) )
| ~ ( C @ ( D @ element ) )
| ~ ( C @ ( B @ ( A @ morphism ) ) )
| ~ ( A @ surjection ) ) ),
inference(cnf,[status(esa)],[62]) ).
thf(64,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( A @ ( B @ ( C @ ( D @ sk4 ) ) ) @ element ) )
| ~ ( C @ ( D @ element ) )
| ~ ( C @ ( B @ ( A @ morphism ) ) )
| ~ ( A @ surjection ) ),
inference(cnfConj,[status(thm)],[63]) ).
thf(3779,plain,
! [A: $i] :
( ( ( A @ zero )
!= ( c @ zero ) )
| ( ( e @ zero @ ( h @ apply ) )
= ( r @ zero ) )
| ~ ( A @ ( b @ ( g @ morphism ) ) ) ),
inference(paramod_ordered,[status(thm)],[826,577]) ).
thf(3780,plain,
( ( ( e @ zero @ ( h @ apply ) )
= ( r @ zero ) )
| ~ ( c @ ( b @ ( g @ morphism ) ) ) ),
inference(pattern_uni,[status(thm)],[3779:[bind(A,$thf( c ))]]) ).
thf(6289,plain,
( ( ( c @ ( b @ ( g @ morphism ) ) )
!= ( e @ ( b @ ( g @ morphism ) ) ) )
| ( ( e @ zero @ ( h @ apply ) )
= ( r @ zero ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[57,3780]) ).
thf(6290,plain,
( ( ( c @ ( b @ ( g @ morphism ) ) )
!= ( e @ ( b @ ( g @ morphism ) ) ) )
| ( ( e @ zero @ ( h @ apply ) )
= ( r @ zero ) ) ),
inference(simp,[status(thm)],[6289]) ).
thf(6474,plain,
( ( c != e )
| ( b != b )
| ( g != g )
| ( ( e @ zero @ ( h @ apply ) )
= ( r @ zero ) ) ),
inference(simp,[status(thm)],[6290]) ).
thf(6532,plain,
( ( c != e )
| ( ( e @ zero @ ( h @ apply ) )
= ( r @ zero ) ) ),
inference(simp,[status(thm)],[6474]) ).
thf(720,plain,
! [A: $i] :
( ( ( b @ zero @ ( g @ apply ) )
!= ( A @ ( beta @ apply ) ) )
| ( g != beta )
| ~ ( b @ ( A @ element ) )
| ~ ( r @ ( sk1 @ ( delta @ apply ) @ element ) )
| ( ( e @ zero )
!= sk1 )
| ( h != delta ) ),
inference(paramod_ordered,[status(thm)],[559,160]) ).
thf(760,plain,
! [A: $i] :
( ( ( b @ zero )
!= A )
| ( g != beta )
| ( g != beta )
| ~ ( b @ ( A @ element ) )
| ~ ( r @ ( sk1 @ ( delta @ apply ) @ element ) )
| ( ( e @ zero )
!= sk1 )
| ( h != delta ) ),
inference(simp,[status(thm)],[720]) ).
thf(836,plain,
( ( g != beta )
| ~ ( b @ ( b @ zero @ element ) )
| ~ ( r @ ( sk1 @ ( delta @ apply ) @ element ) )
| ( ( e @ zero )
!= sk1 )
| ( h != delta ) ),
inference(simp,[status(thm)],[760]) ).
thf(1803,plain,
( ( ( e @ zero @ ( delta @ apply ) )
!= ( sk1 @ ( delta @ apply ) ) )
| ( g != beta )
| ~ ( b @ ( b @ zero @ element ) )
| ~ ( r @ ( r @ zero @ element ) )
| ( ( e @ zero )
!= sk1 )
| ( h != delta ) ),
inference(paramod_ordered,[status(thm)],[608,836]) ).
thf(1824,plain,
( ( ( e @ zero )
!= sk1 )
| ( delta != delta )
| ( g != beta )
| ~ ( b @ ( b @ zero @ element ) )
| ~ ( r @ ( r @ zero @ element ) )
| ( ( e @ zero )
!= sk1 )
| ( h != delta ) ),
inference(simp,[status(thm)],[1803]) ).
thf(1897,plain,
( ( g != beta )
| ~ ( b @ ( b @ zero @ element ) )
| ~ ( r @ ( r @ zero @ element ) )
| ( ( e @ zero )
!= sk1 )
| ( h != delta ) ),
inference(simp,[status(thm)],[1824]) ).
thf(19,axiom,
beta @ ( alpha @ exact ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',alpha_beta_exact) ).
thf(86,plain,
beta @ ( alpha @ exact ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[19]) ).
thf(75,plain,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( F @ ( B @ apply ) )
= ( E @ zero ) )
| ( ( G @ ( A @ apply ) )
!= F )
| ~ ( C @ ( G @ element ) )
| ~ ( E @ ( D @ ( B @ morphism ) ) )
| ~ ( D @ ( C @ ( A @ morphism ) ) )
| ~ ( B @ ( A @ exact ) ) ),
inference(cnfConj,[status(thm)],[71]) ).
thf(80,plain,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ ( C @ ( G @ element ) )
| ~ ( E @ ( D @ ( B @ morphism ) ) )
| ~ ( D @ ( C @ ( A @ morphism ) ) )
| ~ ( B @ ( A @ exact ) )
| ( ( F @ ( B @ apply ) )
= ( E @ zero ) )
| ( ( G @ ( A @ apply ) )
!= F ) ),
inference(lifteq,[status(thm)],[75]) ).
thf(81,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ ( C @ ( F @ element ) )
| ~ ( E @ ( D @ ( B @ morphism ) ) )
| ~ ( D @ ( C @ ( A @ morphism ) ) )
| ~ ( B @ ( A @ exact ) )
| ( ( F @ ( A @ apply ) @ ( B @ apply ) )
= ( E @ zero ) ) ),
inference(simp,[status(thm)],[80]) ).
thf(72,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( C @ ( A @ ( B @ ( C @ ( D @ ( E @ ( F @ sk5 ) ) ) ) ) @ element ) )
| ( ( F @ ( B @ apply ) )
!= ( E @ zero ) )
| ~ ( D @ ( F @ element ) )
| ~ ( E @ ( D @ ( B @ morphism ) ) )
| ~ ( D @ ( C @ ( A @ morphism ) ) )
| ~ ( B @ ( A @ exact ) ) ),
inference(cnfConj,[status(thm)],[71]) ).
thf(76,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( C @ ( A @ ( B @ ( C @ ( D @ ( E @ ( F @ sk5 ) ) ) ) ) @ element ) )
| ~ ( D @ ( F @ element ) )
| ~ ( E @ ( D @ ( B @ morphism ) ) )
| ~ ( D @ ( C @ ( A @ morphism ) ) )
| ~ ( B @ ( A @ exact ) )
| ( ( F @ ( B @ apply ) )
!= ( E @ zero ) ) ),
inference(lifteq,[status(thm)],[72]) ).
thf(26,axiom,
gamma @ ( f @ ( g @ ( alpha @ commute ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',alpha_g_f_gamma_commute) ).
thf(103,plain,
gamma @ ( f @ ( g @ ( alpha @ commute ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[26]) ).
thf(4797,plain,
( ( ( a @ ( b @ ( g @ morphism ) ) )
!= ( e @ ( b @ ( g @ morphism ) ) ) )
| ( ( e @ zero @ ( f @ apply ) )
= ( d @ zero ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[57,3720]) ).
thf(4798,plain,
( ( ( a @ ( b @ ( g @ morphism ) ) )
!= ( e @ ( b @ ( g @ morphism ) ) ) )
| ( ( e @ zero @ ( f @ apply ) )
= ( d @ zero ) ) ),
inference(simp,[status(thm)],[4797]) ).
thf(4900,plain,
( ( a != e )
| ( b != b )
| ( g != g )
| ( ( e @ zero @ ( f @ apply ) )
= ( d @ zero ) ) ),
inference(simp,[status(thm)],[4798]) ).
thf(4985,plain,
( ( a != e )
| ( ( e @ zero @ ( f @ apply ) )
= ( d @ zero ) ) ),
inference(simp,[status(thm)],[4900]) ).
thf(65,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( C @ ( D @ sk4 ) ) ) @ ( A @ apply ) )
= D )
| ~ ( C @ ( D @ element ) )
| ~ ( C @ ( B @ ( A @ morphism ) ) )
| ~ ( A @ surjection ) ),
inference(cnfConj,[status(thm)],[63]) ).
thf(66,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( C @ ( D @ element ) )
| ~ ( C @ ( B @ ( A @ morphism ) ) )
| ~ ( A @ surjection )
| ( ( A @ ( B @ ( C @ ( D @ sk4 ) ) ) @ ( A @ apply ) )
= D ) ),
inference(lifteq,[status(thm)],[65]) ).
thf(7445,plain,
! [C: $i,B: $i,A: $i] :
( ( ( d @ ( a @ ( f @ morphism ) ) )
!= ( C @ ( B @ ( A @ morphism ) ) ) )
| ( A @ injection )
| ( B @ ( A @ ( B @ sk10 ) @ element ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[43,122]) ).
thf(7446,plain,
! [C: $i,B: $i,A: $i] :
( ( ( d @ ( a @ ( f @ morphism ) ) )
!= ( C @ ( B @ ( A @ morphism ) ) ) )
| ( A @ injection )
| ( B @ ( A @ ( B @ sk10 ) @ element ) ) ),
inference(simp,[status(thm)],[7445]) ).
thf(7447,plain,
( ( f @ injection )
| ( a @ ( f @ ( a @ sk10 ) @ element ) ) ),
inference(pattern_uni,[status(thm)],[7446:[bind(A,$thf( f )),bind(B,$thf( a )),bind(C,$thf( d ))]]) ).
thf(46,plain,
! [A: $i,B: $i,C: $i,D: $i] :
( ? [E: $i,F: $i] :
( ? [G: $i,H: $i] :
( ! [I: $i] :
( ( E @ ( I @ element ) )
=> ( ( I @ ( A @ apply ) @ ( B @ apply ) )
= ( I @ ( C @ apply ) @ ( D @ apply ) ) ) )
& ( H @ ( G @ ( D @ morphism ) ) )
& ( G @ ( E @ ( C @ morphism ) ) )
& ( H @ ( F @ ( B @ morphism ) ) ) )
& ( F @ ( E @ ( A @ morphism ) ) ) )
=> ( D @ ( C @ ( B @ ( A @ commute ) ) ) ) ),
inference(miniscope,[status(thm)],[45]) ).
thf(47,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( B @ ( A @ commute ) ) ) )
| ( ( A @ ( B @ ( C @ ( D @ ( E @ ( F @ ( G @ ( H @ sk2 ) ) ) ) ) ) ) @ ( A @ apply ) @ ( B @ apply ) )
!= ( A @ ( B @ ( C @ ( D @ ( E @ ( F @ ( G @ ( H @ sk2 ) ) ) ) ) ) ) @ ( C @ apply ) @ ( D @ apply ) ) )
| ~ ( H @ ( G @ ( D @ morphism ) ) )
| ~ ( G @ ( E @ ( C @ morphism ) ) )
| ~ ( H @ ( F @ ( B @ morphism ) ) )
| ~ ( F @ ( E @ ( A @ morphism ) ) ) )
& ( ( D @ ( C @ ( B @ ( A @ commute ) ) ) )
| ( E @ ( A @ ( B @ ( C @ ( D @ ( E @ ( F @ ( G @ ( H @ sk2 ) ) ) ) ) ) ) @ element ) )
| ~ ( H @ ( G @ ( D @ morphism ) ) )
| ~ ( G @ ( E @ ( C @ morphism ) ) )
| ~ ( H @ ( F @ ( B @ morphism ) ) )
| ~ ( F @ ( E @ ( A @ morphism ) ) ) ) ),
inference(cnf,[status(esa)],[46]) ).
thf(48,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ ( B @ ( A @ commute ) ) ) )
| ( E @ ( A @ ( B @ ( C @ ( D @ ( E @ ( F @ ( G @ ( H @ sk2 ) ) ) ) ) ) ) @ element ) )
| ~ ( H @ ( G @ ( D @ morphism ) ) )
| ~ ( G @ ( E @ ( C @ morphism ) ) )
| ~ ( H @ ( F @ ( B @ morphism ) ) )
| ~ ( F @ ( E @ ( A @ morphism ) ) ) ),
inference(cnfConj,[status(thm)],[47]) ).
thf(49,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ ( B @ ( A @ commute ) ) ) )
| ( ( A @ ( B @ ( C @ ( D @ ( E @ ( F @ ( G @ ( H @ sk2 ) ) ) ) ) ) ) @ ( A @ apply ) @ ( B @ apply ) )
!= ( A @ ( B @ ( C @ ( D @ ( E @ ( F @ ( G @ ( H @ sk2 ) ) ) ) ) ) ) @ ( C @ apply ) @ ( D @ apply ) ) )
| ~ ( H @ ( G @ ( D @ morphism ) ) )
| ~ ( G @ ( E @ ( C @ morphism ) ) )
| ~ ( H @ ( F @ ( B @ morphism ) ) )
| ~ ( F @ ( E @ ( A @ morphism ) ) ) ),
inference(cnfConj,[status(thm)],[47]) ).
thf(50,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ ( B @ ( A @ commute ) ) ) )
| ~ ( H @ ( G @ ( D @ morphism ) ) )
| ~ ( G @ ( E @ ( C @ morphism ) ) )
| ~ ( H @ ( F @ ( B @ morphism ) ) )
| ~ ( F @ ( E @ ( A @ morphism ) ) )
| ( ( A @ ( B @ ( C @ ( D @ ( E @ ( F @ ( G @ ( H @ sk2 ) ) ) ) ) ) ) @ ( A @ apply ) @ ( B @ apply ) )
!= ( A @ ( B @ ( C @ ( D @ ( E @ ( F @ ( G @ ( H @ sk2 ) ) ) ) ) ) ) @ ( C @ apply ) @ ( D @ apply ) ) ) ),
inference(lifteq,[status(thm)],[49]) ).
thf(14,axiom,
delta @ ( gammma @ exact ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gamma_delta_exact) ).
thf(67,plain,
delta @ ( gammma @ exact ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[14]) ).
thf(7691,plain,
! [B: $i,A: $i] :
( ( ( b @ ( g @ ( b @ sk10 ) @ element ) )
!= ( A @ ( B @ element ) ) )
| ~ $true
| ( ( B @ ( B @ ( A @ subtract ) ) )
= ( A @ zero ) )
| ( g @ injection ) ),
inference(paramod_ordered,[status(thm)],[7435,89]) ).
thf(7692,plain,
! [B: $i,A: $i] :
( ( ( b @ ( g @ ( b @ sk10 ) @ element ) )
!= ( A @ ( B @ element ) ) )
| ( ( B @ ( B @ ( A @ subtract ) ) )
= ( A @ zero ) )
| ( g @ injection ) ),
inference(simp,[status(thm)],[7691]) ).
thf(7693,plain,
( ( ( g @ ( b @ sk10 ) @ ( g @ ( b @ sk10 ) @ ( b @ subtract ) ) )
= ( b @ zero ) )
| ( g @ injection ) ),
inference(pattern_uni,[status(thm)],[7692:[bind(A,$thf( b )),bind(B,$thf( g @ ( b @ sk10 ) ))]]) ).
thf(865,plain,
! [C: $i,B: $i,A: $i] :
( ( ( e @ ( d @ ( gamma @ morphism ) ) )
!= ( C @ ( B @ ( A @ morphism ) ) ) )
| ( A @ surjection )
| ( C @ ( A @ ( B @ ( C @ sk3 ) ) @ element ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[102,54]) ).
thf(866,plain,
! [C: $i,B: $i,A: $i] :
( ( ( e @ ( d @ ( gamma @ morphism ) ) )
!= ( C @ ( B @ ( A @ morphism ) ) ) )
| ( A @ surjection )
| ( C @ ( A @ ( B @ ( C @ sk3 ) ) @ element ) ) ),
inference(simp,[status(thm)],[865]) ).
thf(867,plain,
( ( gamma @ surjection )
| ( e @ ( gamma @ ( d @ ( e @ sk3 ) ) @ element ) ) ),
inference(pattern_uni,[status(thm)],[866:[bind(A,$thf( gamma )),bind(B,$thf( d )),bind(C,$thf( e ))]]) ).
thf(2484,plain,
! [B: $i,A: $i] :
( ( ( e @ ( gamma @ ( d @ ( e @ sk3 ) ) @ element ) )
!= ( A @ ( B @ element ) ) )
| ~ $true
| ( ( B @ ( B @ ( A @ subtract ) ) )
= ( A @ zero ) )
| ( gamma @ surjection ) ),
inference(paramod_ordered,[status(thm)],[867,89]) ).
thf(2485,plain,
! [B: $i,A: $i] :
( ( ( e @ ( gamma @ ( d @ ( e @ sk3 ) ) @ element ) )
!= ( A @ ( B @ element ) ) )
| ( ( B @ ( B @ ( A @ subtract ) ) )
= ( A @ zero ) )
| ( gamma @ surjection ) ),
inference(simp,[status(thm)],[2484]) ).
thf(2486,plain,
( ( ( gamma @ ( d @ ( e @ sk3 ) ) @ ( gamma @ ( d @ ( e @ sk3 ) ) @ ( e @ subtract ) ) )
= ( e @ zero ) )
| ( gamma @ surjection ) ),
inference(pattern_uni,[status(thm)],[2485:[bind(A,$thf( e )),bind(B,$thf( gamma @ ( d @ ( e @ sk3 ) ) ))]]) ).
thf(747,plain,
( ( ( b @ zero @ ( g @ apply ) )
!= ( sk1 @ ( delta @ apply ) ) )
| ( beta != delta )
| ( g != delta )
| ( r != e )
| ( ( e @ zero )
!= sk1 )
| ( b != e )
| ( h != delta ) ),
inference(paramod_ordered,[status(thm)],[559,386]) ).
thf(750,plain,
( ( ( b @ zero )
!= sk1 )
| ( g != delta )
| ( beta != delta )
| ( g != delta )
| ( r != e )
| ( ( e @ zero )
!= sk1 )
| ( b != e )
| ( h != delta ) ),
inference(simp,[status(thm)],[747]) ).
thf(828,plain,
( ( ( b @ zero )
!= sk1 )
| ( beta != delta )
| ( g != delta )
| ( r != e )
| ( ( e @ zero )
!= sk1 )
| ( b != e )
| ( h != delta ) ),
inference(simp,[status(thm)],[750]) ).
thf(842,plain,
( ( sk1 != sk1 )
| ( ( b @ zero )
!= ( e @ zero ) )
| ( beta != delta )
| ( g != delta )
| ( r != e )
| ( ( e @ zero )
!= sk1 )
| ( b != e )
| ( h != delta ) ),
inference(eqfactor_ordered,[status(thm)],[828]) ).
thf(844,plain,
( ( b != e )
| ( beta != delta )
| ( g != delta )
| ( r != e )
| ( ( e @ zero )
!= sk1 )
| ( b != e )
| ( h != delta ) ),
inference(simp,[status(thm)],[842]) ).
thf(845,plain,
( ( beta != delta )
| ( g != delta )
| ( r != e )
| ( ( e @ zero )
!= sk1 )
| ( b != e )
| ( h != delta ) ),
inference(simp,[status(thm)],[844]) ).
thf(27,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i] :
( ( ! [F: $i] :
( ( ( ( F @ ( B @ apply ) )
= ( E @ zero ) )
& ( D @ ( F @ element ) ) )
<=> ? [G: $i] :
( ( ( G @ ( A @ apply ) )
= F )
& ( C @ ( G @ element ) ) ) )
& ( E @ ( D @ ( B @ morphism ) ) )
& ( D @ ( C @ ( A @ morphism ) ) ) )
=> ( B @ ( A @ exact ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',properties_for_exact) ).
thf(104,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i] :
( ( ! [F: $i] :
( ( ? [G: $i] :
( ( ( G @ ( A @ apply ) )
= F )
& ( C @ ( G @ element ) ) )
=> ( ( ( F @ ( B @ apply ) )
= ( E @ zero ) )
& ( D @ ( F @ element ) ) ) )
& ( ( ( ( F @ ( B @ apply ) )
= ( E @ zero ) )
& ( D @ ( F @ element ) ) )
=> ? [G: $i] :
( ( ( G @ ( A @ apply ) )
= F )
& ( C @ ( G @ element ) ) ) ) )
& ( E @ ( D @ ( B @ morphism ) ) )
& ( D @ ( C @ ( A @ morphism ) ) ) )
=> ( B @ ( A @ exact ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[27]) ).
thf(3,axiom,
gamma @ injection,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gamma_injection) ).
thf(40,plain,
gamma @ injection,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(9538,plain,
( ( ( g @ ( b @ sk10 ) @ ( g @ ( b @ sk10 ) @ ( b @ subtract ) ) )
!= ( sk1 @ ( sk1 @ ( e @ subtract ) ) ) )
| ( ( b @ zero )
= ( e @ zero ) )
| ( g @ injection ) ),
inference(paramod_ordered,[status(thm)],[544,7693]) ).
thf(9543,plain,
( ( ( g @ ( b @ sk10 ) )
!= sk1 )
| ( ( g @ ( b @ sk10 ) )
!= sk1 )
| ( b != e )
| ( ( b @ zero )
= ( e @ zero ) )
| ( g @ injection ) ),
inference(simp,[status(thm)],[9538]) ).
thf(9551,plain,
( ( ( g @ ( b @ sk10 ) )
!= sk1 )
| ( b != e )
| ( ( b @ zero )
= ( e @ zero ) )
| ( g @ injection ) ),
inference(simp,[status(thm)],[9543]) ).
thf(3368,plain,
( ( sk1 != sk1 )
| ( ( c @ zero )
!= ( b @ zero ) )
| ( ( b @ zero )
!= sk1 )
| ( beta != delta )
| ( r != e )
| ( g != beta )
| ( b != e )
| ( h != delta ) ),
inference(eqfactor_ordered,[status(thm)],[1329]) ).
thf(3373,plain,
( ( c != b )
| ( ( b @ zero )
!= sk1 )
| ( beta != delta )
| ( r != e )
| ( g != beta )
| ( b != e )
| ( h != delta ) ),
inference(simp,[status(thm)],[3368]) ).
thf(74,plain,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( F @ element ) )
| ( ( G @ ( A @ apply ) )
!= F )
| ~ ( C @ ( G @ element ) )
| ~ ( E @ ( D @ ( B @ morphism ) ) )
| ~ ( D @ ( C @ ( A @ morphism ) ) )
| ~ ( B @ ( A @ exact ) ) ),
inference(cnfConj,[status(thm)],[71]) ).
thf(78,plain,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( F @ element ) )
| ~ ( C @ ( G @ element ) )
| ~ ( E @ ( D @ ( B @ morphism ) ) )
| ~ ( D @ ( C @ ( A @ morphism ) ) )
| ~ ( B @ ( A @ exact ) )
| ( ( G @ ( A @ apply ) )
!= F ) ),
inference(lifteq,[status(thm)],[74]) ).
thf(79,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( F @ ( A @ apply ) @ element ) )
| ~ ( C @ ( F @ element ) )
| ~ ( E @ ( D @ ( B @ morphism ) ) )
| ~ ( D @ ( C @ ( A @ morphism ) ) )
| ~ ( B @ ( A @ exact ) ) ),
inference(simp,[status(thm)],[78]) ).
thf(22,axiom,
! [A: $i,B: $i,C: $i] :
( ( ( A @ ( C @ element ) )
& ( A @ ( B @ element ) ) )
=> ( A @ ( C @ ( B @ ( A @ subtract ) ) @ element ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',subtract_in_domain) ).
thf(94,plain,
! [A: $i,B: $i,C: $i] :
( ( ( A @ ( C @ element ) )
& ( A @ ( B @ element ) ) )
=> ( A @ ( C @ ( B @ ( A @ subtract ) ) @ element ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[22]) ).
thf(15,axiom,
h @ surjection,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',h_surjection) ).
thf(68,plain,
h @ surjection,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[15]) ).
thf(21,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i,G: $i,H: $i] :
( ( ( H @ ( G @ ( D @ morphism ) ) )
& ( G @ ( E @ ( C @ morphism ) ) )
& ( H @ ( F @ ( B @ morphism ) ) )
& ( F @ ( E @ ( A @ morphism ) ) )
& ( D @ ( C @ ( B @ ( A @ commute ) ) ) ) )
=> ! [I: $i] :
( ( E @ ( I @ element ) )
=> ( ( I @ ( A @ apply ) @ ( B @ apply ) )
= ( I @ ( C @ apply ) @ ( D @ apply ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commute_properties) ).
thf(90,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i,G: $i,H: $i] :
( ( ( H @ ( G @ ( D @ morphism ) ) )
& ( G @ ( E @ ( C @ morphism ) ) )
& ( H @ ( F @ ( B @ morphism ) ) )
& ( F @ ( E @ ( A @ morphism ) ) )
& ( D @ ( C @ ( B @ ( A @ commute ) ) ) ) )
=> ! [I: $i] :
( ( E @ ( I @ element ) )
=> ( ( I @ ( A @ apply ) @ ( B @ apply ) )
= ( I @ ( C @ apply ) @ ( D @ apply ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[21]) ).
thf(107564,plain,
$false,
inference(e,[status(thm)],[608,69,101,2072,9469,202,1705,1999,2141,384,56,42,7079,3809,559,2857,5802,57,4514,4072,7441,602,2618,61,89,1345,117,3720,85,102,1174,160,33,97,3763,1329,7435,3714,96,77,7453,1324,129,3333,41,605,128,205,7444,1219,5508,45,64,44,826,577,59,118,572,6532,3783,1897,86,382,54,81,76,39,1667,103,4985,66,9111,7447,209,836,194,48,580,150,50,67,199,7693,2486,544,864,386,43,4414,845,87,104,4310,40,3780,207,82,119,58,9551,36,51,3373,867,79,94,886,62,4330,68,90,122,1962,83,1184]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HAL004+1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.08 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.14/0.41 % Computer : n004.cluster.edu
% 0.14/0.41 % Model : x86_64 x86_64
% 0.14/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.41 % Memory : 8046.5625MB
% 0.14/0.41 % OS : Linux 6.8.0-71-generic
% 0.14/0.41 % CPULimit : 300
% 0.14/0.41 % WCLimit : 300
% 0.14/0.41 % DateTime : Fri Sep 25 15:54:06 UTC 2026
% 0.14/0.41 % CPUTime :
% 0.14/0.41 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.88/0.97 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.28/1.19 % [INFO] Parsing done (214ms).
% 1.52/1.21 % [INFO] Running in sequential loop mode.
% 2.02/1.60 % [INFO] eprover registered as external prover.
% 2.23/1.60 % [INFO] Scanning for conjecture ...
% 2.43/1.72 % [INFO] Found a conjecture (or negated_conjecture) and 30 axioms. Running axiom selection ...
% 2.61/1.82 % [INFO] Axiom selection finished. Selected 30 axioms (removed 0 axioms).
% 2.61/1.89 % [INFO] Problem is first-order (TPTP FOF).
% 2.87/1.90 % [INFO] Type checking passed.
% 2.87/1.91 % [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 ...
% 144.33/40.29 % External prover 'e' found a proof!
% 144.33/40.29 % [INFO] Killing All external provers ...
% 144.33/40.29 % Time passed: 39743ms (effective reasoning time: 39082ms)
% 144.33/40.29 % Solved by strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>
% 138.53/40.30 % Axioms used in derivation (30): surjection_properties, beta_morphism, gamma_morphism, subtract_cancellation, alpha_g_f_gamma_commute, alpha_injection, properties_for_surjection, morphism, commute_properties, subtract_in_domain, subtract_to_0, beta_h_g_delta_commute, delta_morphism, h_morphism, alpha_morphism, injection_properties, properties_for_exact, subtract_distribution, h_surjection, f_morphism, f_surjection, properties_for_injection, delta_surjection, properties_for_commute, gamma_injection, exact_properties, gamma_delta_exact, beta_surjection, g_morphism, alpha_beta_exact
% 138.53/40.30 % No. of inferences in proof: 311
% 138.53/40.30 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 39743 ms resp. 39082 ms w/o parsing
% 138.91/40.45 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 138.91/40.45 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------