%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : SEU027+1 : TPTP v9.3.1. Released v3.2.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 : n015.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 08:37:28 AM UTC 2026
% Result : Theorem 91.75s 22.56s
% Output : Refutation 89.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 59
% Syntax : Number of formulae : 709 ( 126 unt; 0 typ; 22 def)
% Number of atoms : 2796 ( 817 equ; 0 cnn)
% Maximal formula atoms : 99 ( 3 avg)
% Number of connectives : 6951 (1311 ~;1300 |; 227 &;3997 @)
% ( 6 <=>; 110 =>; 0 <=; 0 <~>)
% Maximal formula depth : 30 ( 6 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 41 ( 38 usr; 13 con; 0-3 aty)
% Number of variables : 711 ( 22 ^; 626 !; 41 ?; 711 :)
% ( 0 !>; 0 ?*; 0 @-; 22 @+)
% Comments :
%------------------------------------------------------------------------------
thf(relation_decl,type,
relation: $i > $o ).
thf(function_decl,type,
function: $i > $o ).
thf(one_to_one_decl,type,
one_to_one: $i > $o ).
thf(relation_dom_decl,type,
relation_dom: $i > $i ).
thf(relation_rng_decl,type,
relation_rng: $i > $i ).
thf(in_decl,type,
in: $i > $i > $o ).
thf(apply_decl,type,
apply: $i > $i > $i ).
thf(function_inverse_decl,type,
function_inverse: $i > $i ).
thf(subset_decl,type,
subset: $i > $i > $o ).
thf(empty_decl,type,
empty: $i > $o ).
thf(empty_set_decl,type,
empty_set: $i ).
thf(element_decl,type,
element: $i > $i > $o ).
thf(powerset_decl,type,
powerset: $i > $i ).
thf(relation_empty_yielding_decl,type,
relation_empty_yielding: $i > $o ).
thf(sk1_decl,type,
sk1: $i ).
thf(sk2_decl,type,
sk2: $i ).
thf(sk3_decl,type,
sk3: $i ).
thf(sk4_decl,type,
sk4: $i ).
thf(sk5_decl,type,
sk5: $i > $i ).
thf(sk6_decl,type,
sk6: $i > $i ).
thf(sk7_decl,type,
sk7: $i > $i ).
thf(sk8_decl,type,
sk8: $i ).
thf(sk9_decl,type,
sk9: $i ).
thf(sk10_decl,type,
sk10: $i ).
thf(sk11_decl,type,
sk11: $i > $i > $i ).
thf(sk12_decl,type,
sk12: $i ).
thf(sk13_decl,type,
sk13: $i ).
thf(sk14_decl,type,
sk14: $i > $i > $i > $i ).
thf(sk15_decl,type,
sk15: $i > $i > $o ).
thf(sk16_decl,type,
sk16: $i > $i > $i ).
thf(sk17_decl,type,
sk17: $i > $i > $i ).
thf(sk18_decl,type,
sk18: $i > $i > $i ).
thf(sk19_decl,type,
sk19: $i > $i > $o ).
thf(sk20_decl,type,
sk20: $i > $i > $i ).
thf(sk21_decl,type,
sk21: $i > $i > $i ).
thf(sk22_decl,type,
sk22: $i > $i > $i ).
thf(sk23_decl,type,
sk23: $i > $i > $i ).
thf(sk24_decl,type,
sk24: $i ).
thf(sk1_def,definition,
( sk1
= ( @+[A: $i] :
~ ( ( ( A @ function )
& ( A @ relation ) )
=> ! [B: $i] :
( ( ( B @ function )
& ( B @ relation ) )
=> ( ( ! [C: $i,D: $i] :
( ( ( B @ relation_dom @ ( D @ in ) )
& ( A @ relation_dom @ ( C @ in ) ) )
=> ( ( ( ( D @ ( B @ apply ) )
= C )
=> ( ( C @ ( A @ apply ) )
= D ) )
& ( ( ( C @ ( A @ apply ) )
= D )
=> ( ( D @ ( B @ apply ) )
= C ) ) ) )
& ( ( A @ relation_rng )
= ( B @ relation_dom ) )
& ( ( A @ relation_dom )
= ( B @ relation_rng ) )
& ( A @ one_to_one ) )
=> ( B
= ( A @ function_inverse ) ) ) ) ) ) ) ).
thf(sk2_def,definition,
( sk2
= ( @+[A: $i] :
~ ( ( ( A @ function )
& ( A @ relation ) )
=> ( ( ! [B: $i,C: $i] :
( ( ( A @ relation_dom @ ( C @ in ) )
& ( sk1 @ relation_dom @ ( B @ in ) ) )
=> ( ( ( ( C @ ( A @ apply ) )
= B )
=> ( ( B @ ( sk1 @ apply ) )
= C ) )
& ( ( ( B @ ( sk1 @ apply ) )
= C )
=> ( ( C @ ( A @ apply ) )
= B ) ) ) )
& ( ( sk1 @ relation_rng )
= ( A @ relation_dom ) )
& ( ( sk1 @ relation_dom )
= ( A @ relation_rng ) )
& ( sk1 @ one_to_one ) )
=> ( A
= ( sk1 @ function_inverse ) ) ) ) ) ) ).
thf(sk3_def,definition,
( sk3
= ( @+[A: $i] : ( A @ empty ) ) ) ).
thf(sk4_def,definition,
( sk4
= ( @+[A: $i] :
~ ( A @ empty ) ) ) ).
thf(sk5_def,definition,
( sk5
= ( ^ [A: $i] :
@+[B: $i] :
( ~ ( B @ empty )
& ( A @ powerset @ ( B @ element ) ) ) ) ) ).
thf(sk6_def,definition,
( sk6
= ( ^ [A: $i] :
@+[B: $i] :
( ( B @ empty )
& ( A @ powerset @ ( B @ element ) ) ) ) ) ).
thf(sk7_def,definition,
( sk7
= ( ^ [A: $i] :
@+[B: $i] : ( A @ ( B @ element ) ) ) ) ).
thf(sk8_def,definition,
( sk8
= ( @+[A: $i] :
( ( A @ relation_empty_yielding )
& ( A @ relation ) ) ) ) ).
thf(sk9_def,definition,
( sk9
= ( @+[A: $i] :
( ( A @ relation )
& ( A @ empty ) ) ) ) ).
thf(sk10_def,definition,
( sk10
= ( @+[A: $i] :
( ( A @ one_to_one )
& ( A @ function )
& ( A @ relation ) ) ) ) ).
thf(sk11_def,definition,
( sk11
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
~ ( ( B @ relation_dom @ ( C @ in ) )
=> ( ( C @ ( B @ apply ) )
= ( C @ ( A @ apply ) ) ) ) ) ) ).
thf(sk12_def,definition,
( sk12
= ( @+[A: $i] :
( ( A @ function )
& ( A @ empty )
& ( A @ relation ) ) ) ) ).
thf(sk13_def,definition,
( sk13
= ( @+[A: $i] :
( ( A @ relation )
& ~ ( A @ empty ) ) ) ) ).
thf(sk14_def,definition,
( sk14
= ( ^ [A: $i,B: $i,C: $i] :
@+[D: $i] :
( ( A
= ( D @ ( C @ apply ) ) )
& ( C @ relation_dom @ ( D @ in ) ) ) ) ) ).
thf(sk16_def,definition,
( sk16
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
~ ( ( A @ ( C @ in ) )
=> ? [D: $i] :
( ( C
= ( D @ ( B @ apply ) ) )
& ( B @ relation_dom @ ( D @ in ) ) ) ) ) ) ).
thf(sk17_def,definition,
( sk17
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
~ ( ? [D: $i] :
( ( C
= ( D @ ( B @ apply ) ) )
& ( B @ relation_dom @ ( D @ in ) ) )
=> ( A @ ( C @ in ) ) ) ) ) ).
thf(sk18_def,definition,
( sk18
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
( ( ( B @ ( A @ sk17 ) )
= ( C @ ( B @ apply ) ) )
& ( B @ relation_dom @ ( C @ in ) ) ) ) ) ).
thf(sk20_def,definition,
( sk20
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
~ ! [D: $i] :
( ( ( D
= ( C @ ( A @ apply ) ) )
& ( B @ relation_rng @ ( C @ in ) ) )
=> ( ( C
= ( D @ ( B @ apply ) ) )
& ( B @ relation_dom @ ( D @ in ) ) ) ) ) ) ).
thf(sk21_def,definition,
( sk21
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
~ ( ( ( C
= ( B @ ( A @ sk20 ) @ ( A @ apply ) ) )
& ( B @ relation_rng @ ( B @ ( A @ sk20 ) @ in ) ) )
=> ( ( ( B @ ( A @ sk20 ) )
= ( C @ ( B @ apply ) ) )
& ( B @ relation_dom @ ( C @ in ) ) ) ) ) ) ).
thf(sk22_def,definition,
( sk22
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
~ ! [D: $i] :
( ( ( C
= ( D @ ( B @ apply ) ) )
& ( B @ relation_dom @ ( D @ in ) ) )
=> ( ( D
= ( C @ ( A @ apply ) ) )
& ( B @ relation_rng @ ( C @ in ) ) ) ) ) ) ).
thf(sk23_def,definition,
( sk23
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
~ ( ( ( ( B @ ( A @ sk22 ) )
= ( C @ ( B @ apply ) ) )
& ( B @ relation_dom @ ( C @ in ) ) )
=> ( ( C
= ( B @ ( A @ sk22 ) @ ( A @ apply ) ) )
& ( B @ relation_rng @ ( B @ ( A @ sk22 ) @ in ) ) ) ) ) ) ).
thf(sk24_def,definition,
( sk24
= ( @+[A: $i] :
( ( A @ function )
& ( A @ relation ) ) ) ) ).
thf(7,axiom,
empty_set @ empty,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_xboole_0) ).
thf(69,plain,
empty_set @ empty,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(12,axiom,
! [A: $i] :
? [B: $i] :
( ( B @ empty )
& ( A @ powerset @ ( B @ element ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc2_subset_1) ).
thf(86,plain,
! [A: $i] :
? [B: $i] :
( ( B @ empty )
& ( A @ powerset @ ( B @ element ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[12]) ).
thf(87,plain,
! [A: $i] :
( ( A @ sk6 @ empty )
& ( A @ powerset @ ( A @ sk6 @ element ) ) ),
inference(cnf,[status(esa)],[86]) ).
thf(88,plain,
! [A: $i] : ( A @ powerset @ ( A @ sk6 @ element ) ),
inference(cnfConj,[status(thm)],[87]) ).
thf(89,plain,
! [A: $i] : ( A @ sk6 @ empty ),
inference(cnfConj,[status(thm)],[87]) ).
thf(11,axiom,
! [A: $i] :
( ( A @ empty )
=> ( A = empty_set ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t6_boole) ).
thf(83,plain,
! [A: $i] :
( ( A @ empty )
=> ( A = empty_set ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[11]) ).
thf(84,plain,
! [A: $i] :
( ( A = empty_set )
| ~ ( A @ empty ) ),
inference(cnf,[status(esa)],[83]) ).
thf(85,plain,
! [A: $i] :
( ~ ( A @ empty )
| ( A = empty_set ) ),
inference(lifteq,[status(thm)],[84]) ).
thf(1694,plain,
! [B: $i,A: $i] :
( ( ( A @ sk6 @ empty )
!= ( B @ empty ) )
| ~ $true
| ( B = empty_set ) ),
inference(paramod_ordered,[status(thm)],[89,85]) ).
thf(1695,plain,
! [B: $i,A: $i] :
( ( ( A @ sk6 @ empty )
!= ( B @ empty ) )
| ( B = empty_set ) ),
inference(simp,[status(thm)],[1694]) ).
thf(1696,plain,
! [A: $i] :
( ( A @ sk6 )
= empty_set ),
inference(pattern_uni,[status(thm)],[1695:[bind(A,$thf( C )),bind(B,$thf( C @ sk6 ))]]) ).
thf(1964,plain,
! [A: $i] :
( ( A @ sk6 )
= empty_set ),
inference(simp,[status(thm)],[1696]) ).
thf(2048,plain,
! [A: $i] : ( A @ powerset @ ( empty_set @ element ) ),
inference(rewrite,[status(thm)],[88,1964]) ).
thf(24,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ element ) )
=> ( ( B @ ( A @ in ) )
| ( B @ empty ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2_subset) ).
thf(132,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ element ) )
=> ( ( B @ ( A @ in ) )
| ( B @ empty ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[24]) ).
thf(133,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ in ) )
| ( B @ empty )
| ~ ( B @ ( A @ element ) ) ),
inference(cnf,[status(esa)],[132]) ).
thf(2584,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ ( empty_set @ element ) )
!= ( C @ ( B @ element ) ) )
| ( C @ ( B @ in ) )
| ( C @ empty )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2048,133]) ).
thf(2585,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ ( empty_set @ element ) )
!= ( C @ ( B @ element ) ) )
| ( C @ ( B @ in ) )
| ( C @ empty ) ),
inference(simp,[status(thm)],[2584]) ).
thf(2586,plain,
! [A: $i] :
( ( A @ powerset @ ( empty_set @ in ) )
| ( A @ powerset @ empty ) ),
inference(pattern_uni,[status(thm)],[2585:[bind(A,$thf( D )),bind(B,$thf( empty_set )),bind(C,$thf( D @ powerset ))]]) ).
thf(2599,plain,
! [A: $i] :
( ( A @ powerset @ ( empty_set @ in ) )
| ( A @ powerset @ empty ) ),
inference(simp,[status(thm)],[2586]) ).
thf(10,axiom,
! [A: $i] :
~ ( A @ powerset @ empty ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_subset_1) ).
thf(80,plain,
! [A: $i] :
~ ( A @ powerset @ empty ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).
thf(81,plain,
~ ? [A: $i] : ( A @ powerset @ empty ),
inference(miniscope,[status(thm)],[80]) ).
thf(82,plain,
! [A: $i] :
~ ( A @ powerset @ empty ),
inference(cnf,[status(esa)],[81]) ).
thf(2821,plain,
! [A: $i] :
( ( A @ powerset @ ( empty_set @ in ) )
| $false ),
inference(rewrite,[status(thm)],[2599,82]) ).
thf(2822,plain,
! [A: $i] : ( A @ powerset @ ( empty_set @ in ) ),
inference(simp,[status(thm)],[2821]) ).
thf(26,axiom,
! [A: $i] :
( ( ( A @ function )
& ( A @ relation ) )
=> ( ( A @ function_inverse @ function )
& ( A @ function_inverse @ relation ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k2_funct_1) ).
thf(136,plain,
! [A: $i] :
( ( ( A @ function )
& ( A @ relation ) )
=> ( ( A @ function_inverse @ function )
& ( A @ function_inverse @ relation ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[26]) ).
thf(137,plain,
! [A: $i] :
( ( ( A @ function_inverse @ function )
| ~ ( A @ function )
| ~ ( A @ relation ) )
& ( ( A @ function_inverse @ relation )
| ~ ( A @ function )
| ~ ( A @ relation ) ) ),
inference(cnf,[status(esa)],[136]) ).
thf(138,plain,
! [A: $i] :
( ( A @ function_inverse @ relation )
| ~ ( A @ function )
| ~ ( A @ relation ) ),
inference(cnfConj,[status(thm)],[137]) ).
thf(16,axiom,
? [A: $i] :
( ( A @ relation_empty_yielding )
& ( A @ relation ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc3_relat_1) ).
thf(101,plain,
? [A: $i] :
( ( A @ relation_empty_yielding )
& ( A @ relation ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[16]) ).
thf(1,conjecture,
! [A: $i] :
( ( ( A @ function )
& ( A @ relation ) )
=> ! [B: $i] :
( ( ( B @ function )
& ( B @ relation ) )
=> ( ( ! [C: $i,D: $i] :
( ( ( B @ relation_dom @ ( D @ in ) )
& ( A @ relation_dom @ ( C @ in ) ) )
=> ( ( ( C @ ( A @ apply ) )
= D )
<=> ( ( D @ ( B @ apply ) )
= C ) ) )
& ( ( A @ relation_rng )
= ( B @ relation_dom ) )
& ( ( A @ relation_dom )
= ( B @ relation_rng ) )
& ( A @ one_to_one ) )
=> ( B
= ( A @ function_inverse ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t60_funct_1) ).
thf(2,negated_conjecture,
~ ! [A: $i] :
( ( ( A @ function )
& ( A @ relation ) )
=> ! [B: $i] :
( ( ( B @ function )
& ( B @ relation ) )
=> ( ( ! [C: $i,D: $i] :
( ( ( B @ relation_dom @ ( D @ in ) )
& ( A @ relation_dom @ ( C @ in ) ) )
=> ( ( ( C @ ( A @ apply ) )
= D )
<=> ( ( D @ ( B @ apply ) )
= C ) ) )
& ( ( A @ relation_rng )
= ( B @ relation_dom ) )
& ( ( A @ relation_dom )
= ( B @ relation_rng ) )
& ( A @ one_to_one ) )
=> ( B
= ( A @ function_inverse ) ) ) ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(39,plain,
~ ! [A: $i] :
( ( ( A @ function )
& ( A @ relation ) )
=> ! [B: $i] :
( ( ( B @ function )
& ( B @ relation ) )
=> ( ( ! [C: $i,D: $i] :
( ( ( B @ relation_dom @ ( D @ in ) )
& ( A @ relation_dom @ ( C @ in ) ) )
=> ( ( ( ( D @ ( B @ apply ) )
= C )
=> ( ( C @ ( A @ apply ) )
= D ) )
& ( ( ( C @ ( A @ apply ) )
= D )
=> ( ( D @ ( B @ apply ) )
= C ) ) ) )
& ( ( A @ relation_rng )
= ( B @ relation_dom ) )
& ( ( A @ relation_dom )
= ( B @ relation_rng ) )
& ( A @ one_to_one ) )
=> ( B
= ( A @ function_inverse ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(40,plain,
! [B: $i,A: $i] :
( ( sk2
!= ( sk1 @ function_inverse ) )
& ( ( ( A @ ( sk1 @ apply ) )
= B )
| ( ( B @ ( sk2 @ apply ) )
!= A )
| ~ ( sk2 @ relation_dom @ ( B @ in ) )
| ~ ( sk1 @ relation_dom @ ( A @ in ) ) )
& ( ( ( B @ ( sk2 @ apply ) )
= A )
| ( ( A @ ( sk1 @ apply ) )
!= B )
| ~ ( sk2 @ relation_dom @ ( B @ in ) )
| ~ ( sk1 @ relation_dom @ ( A @ in ) ) )
& ( ( sk1 @ relation_rng )
= ( sk2 @ relation_dom ) )
& ( ( sk1 @ relation_dom )
= ( sk2 @ relation_rng ) )
& ( sk1 @ one_to_one )
& ( sk2 @ function )
& ( sk2 @ relation )
& ( sk1 @ function )
& ( sk1 @ relation ) ),
inference(cnf,[status(esa)],[39]) ).
thf(46,plain,
( ( sk1 @ relation_dom )
= ( sk2 @ relation_rng ) ),
inference(cnfConj,[status(thm)],[40]) ).
thf(51,plain,
( ( sk2 @ relation_rng )
= ( sk1 @ relation_dom ) ),
inference(lifteq,[status(thm)],[46]) ).
thf(17,axiom,
! [A: $i] :
( ( A @ empty )
=> ( ( A @ relation_rng @ relation )
& ( A @ relation_rng @ empty ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc8_relat_1) ).
thf(105,plain,
! [A: $i] :
( ( A @ empty )
=> ( ( A @ relation_rng @ relation )
& ( A @ relation_rng @ empty ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[17]) ).
thf(106,plain,
! [A: $i] :
( ( ( A @ relation_rng @ relation )
| ~ ( A @ empty ) )
& ( ( A @ relation_rng @ empty )
| ~ ( A @ empty ) ) ),
inference(cnf,[status(esa)],[105]) ).
thf(107,plain,
! [A: $i] :
( ( A @ relation_rng @ empty )
| ~ ( A @ empty ) ),
inference(cnfConj,[status(thm)],[106]) ).
thf(2163,plain,
! [A: $i] :
( ( ( empty_set @ empty )
!= ( A @ empty ) )
| ( A @ relation_rng @ empty )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[69,107]) ).
thf(2164,plain,
! [A: $i] :
( ( ( empty_set @ empty )
!= ( A @ empty ) )
| ( A @ relation_rng @ empty ) ),
inference(simp,[status(thm)],[2163]) ).
thf(2165,plain,
empty_set @ relation_rng @ empty,
inference(pattern_uni,[status(thm)],[2164:[bind(A,$thf( empty_set ))]]) ).
thf(2265,plain,
( ( ( sk2 @ relation_rng )
!= ( empty_set @ relation_rng ) )
| ( sk1 @ relation_dom @ empty ) ),
inference(paramod_ordered,[status(thm)],[51,2165]) ).
thf(2280,plain,
( ( sk2 != empty_set )
| ( sk1 @ relation_dom @ empty ) ),
inference(simp,[status(thm)],[2265]) ).
thf(41,plain,
sk1 @ relation,
inference(cnfConj,[status(thm)],[40]) ).
thf(27,axiom,
! [A: $i] :
( ( ( A @ relation )
& ~ ( A @ empty ) )
=> ~ ( A @ relation_dom @ empty ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc5_relat_1) ).
thf(140,plain,
! [A: $i] :
( ( ( A @ relation )
& ~ ( A @ empty ) )
=> ~ ( A @ relation_dom @ empty ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[27]) ).
thf(141,plain,
! [A: $i] :
( ~ ( A @ relation_dom @ empty )
| ~ ( A @ relation )
| ( A @ empty ) ),
inference(cnf,[status(esa)],[140]) ).
thf(4063,plain,
! [A: $i] :
( ( ( sk1 @ relation )
!= ( A @ relation ) )
| ~ ( A @ relation_dom @ empty )
| ~ $true
| ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[41,141]) ).
thf(4064,plain,
! [A: $i] :
( ( ( sk1 @ relation )
!= ( A @ relation ) )
| ~ ( A @ relation_dom @ empty )
| ( A @ empty ) ),
inference(simp,[status(thm)],[4063]) ).
thf(4065,plain,
( ~ ( sk1 @ relation_dom @ empty )
| ( sk1 @ empty ) ),
inference(pattern_uni,[status(thm)],[4064:[bind(A,$thf( sk1 ))]]) ).
thf(13758,plain,
( ( ( sk1 @ relation_dom @ empty )
!= ( sk1 @ relation_dom @ empty ) )
| ~ $true
| ( sk1 @ empty )
| ( sk2 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[2280,4065]) ).
thf(13759,plain,
( ( ( sk1 @ relation_dom @ empty )
!= ( sk1 @ relation_dom @ empty ) )
| ( sk1 @ empty )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[13758]) ).
thf(13760,plain,
( ( sk1 @ empty )
| ( sk2 != empty_set ) ),
inference(pattern_uni,[status(thm)],[13759:[]]) ).
thf(50,plain,
sk1 @ one_to_one,
inference(cnfConj,[status(thm)],[40]) ).
thf(1608,plain,
! [A: $i] :
( ( A != sk1 )
| ( empty_set @ one_to_one )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[85,50]) ).
thf(1609,plain,
( ( empty_set @ one_to_one )
| ~ ( sk1 @ empty ) ),
inference(pattern_uni,[status(thm)],[1608:[bind(A,$thf( sk1 ))]]) ).
thf(14461,plain,
( ( ( sk1 @ empty )
!= ( sk1 @ empty ) )
| ( empty_set @ one_to_one )
| ~ $true
| ( sk2 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[13760,1609]) ).
thf(14462,plain,
( ( ( sk1 @ empty )
!= ( sk1 @ empty ) )
| ( empty_set @ one_to_one )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[14461]) ).
thf(14463,plain,
( ( empty_set @ one_to_one )
| ( sk2 != empty_set ) ),
inference(pattern_uni,[status(thm)],[14462:[]]) ).
thf(4,axiom,
! [A: $i,B: $i] :
~ ( ( B @ empty )
& ( A != B )
& ( A @ empty ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t8_boole) ).
thf(60,plain,
! [A: $i,B: $i] :
~ ( ( B @ empty )
& ( A != B )
& ( A @ empty ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(61,plain,
~ ? [A: $i] :
( ? [B: $i] :
( ( B @ empty )
& ( A != B ) )
& ( A @ empty ) ),
inference(miniscope,[status(thm)],[60]) ).
thf(62,plain,
! [B: $i,A: $i] :
( ~ ( B @ empty )
| ( A = B )
| ~ ( A @ empty ) ),
inference(cnf,[status(esa)],[61]) ).
thf(63,plain,
! [B: $i,A: $i] :
( ~ ( B @ empty )
| ~ ( A @ empty )
| ( A = B ) ),
inference(lifteq,[status(thm)],[62]) ).
thf(48,plain,
( sk2
!= ( sk1 @ function_inverse ) ),
inference(cnfConj,[status(thm)],[40]) ).
thf(55,plain,
( ( sk1 @ function_inverse )
!= sk2 ),
inference(lifteq,[status(thm)],[48]) ).
thf(601,plain,
! [B: $i,A: $i] :
( ( A
!= ( sk1 @ function_inverse ) )
| ( B != sk2 )
| ~ ( B @ empty )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[63,55]) ).
thf(602,plain,
! [A: $i] :
( ( A != sk2 )
| ~ ( A @ empty )
| ~ ( sk1 @ function_inverse @ empty ) ),
inference(pattern_uni,[status(thm)],[601:[bind(A,$thf( sk1 @ function_inverse )),bind(B,$thf( B ))]]) ).
thf(962,plain,
( ~ ( sk2 @ empty )
| ~ ( sk1 @ function_inverse @ empty ) ),
inference(simp,[status(thm)],[602]) ).
thf(45,plain,
! [B: $i,A: $i] :
( ( ( A @ ( sk1 @ apply ) )
= B )
| ( ( B @ ( sk2 @ apply ) )
!= A )
| ~ ( sk2 @ relation_dom @ ( B @ in ) )
| ~ ( sk1 @ relation_dom @ ( A @ in ) ) ),
inference(cnfConj,[status(thm)],[40]) ).
thf(52,plain,
! [B: $i,A: $i] :
( ~ ( sk2 @ relation_dom @ ( B @ in ) )
| ~ ( sk1 @ relation_dom @ ( A @ in ) )
| ( ( A @ ( sk1 @ apply ) )
= B )
| ( ( B @ ( sk2 @ apply ) )
!= A ) ),
inference(lifteq,[status(thm)],[45]) ).
thf(53,plain,
! [A: $i] :
( ~ ( sk2 @ relation_dom @ ( A @ in ) )
| ~ ( sk1 @ relation_dom @ ( A @ ( sk2 @ apply ) @ in ) )
| ( ( A @ ( sk2 @ apply ) @ ( sk1 @ apply ) )
= A ) ),
inference(simp,[status(thm)],[52]) ).
thf(230,plain,
! [B: $i,A: $i] :
( ( ( A @ ( sk2 @ apply ) @ ( sk1 @ apply ) )
!= ( B @ ( sk2 @ apply ) ) )
| ~ ( sk2 @ relation_dom @ ( B @ in ) )
| ~ ( sk1 @ relation_dom @ ( A @ in ) )
| ( ( B @ ( sk2 @ apply ) @ ( sk1 @ apply ) )
= B )
| ~ ( sk2 @ relation_dom @ ( A @ in ) )
| ~ ( sk1 @ relation_dom @ ( A @ ( sk2 @ apply ) @ in ) ) ),
inference(paramod_ordered,[status(thm)],[53,53]) ).
thf(232,plain,
! [B: $i,A: $i] :
( ( ( A @ ( sk2 @ apply ) )
!= B )
| ( sk2 != sk1 )
| ~ ( sk2 @ relation_dom @ ( B @ in ) )
| ~ ( sk1 @ relation_dom @ ( A @ in ) )
| ~ ( sk2 @ relation_dom @ ( A @ in ) )
| ~ ( sk1 @ relation_dom @ ( A @ ( sk2 @ apply ) @ in ) )
| ( ( B @ ( sk2 @ apply ) @ ( sk1 @ apply ) )
= B ) ),
inference(simp,[status(thm)],[230]) ).
thf(234,plain,
! [A: $i] :
( ( sk2 != sk1 )
| ~ ( sk2 @ relation_dom @ ( A @ ( sk2 @ apply ) @ in ) )
| ~ ( sk1 @ relation_dom @ ( A @ in ) )
| ~ ( sk2 @ relation_dom @ ( A @ in ) )
| ~ ( sk1 @ relation_dom @ ( A @ ( sk2 @ apply ) @ in ) )
| ( ( A @ ( sk2 @ apply ) @ ( sk2 @ apply ) @ ( sk1 @ apply ) )
= ( A @ ( sk2 @ apply ) ) ) ),
inference(simp,[status(thm)],[232]) ).
thf(2232,plain,
! [A: $i] :
( ( ( empty_set @ relation_rng @ empty )
!= ( A @ empty ) )
| ~ $true
| ( A = empty_set ) ),
inference(paramod_ordered,[status(thm)],[2165,85]) ).
thf(2233,plain,
! [A: $i] :
( ( ( empty_set @ relation_rng @ empty )
!= ( A @ empty ) )
| ( A = empty_set ) ),
inference(simp,[status(thm)],[2232]) ).
thf(2234,plain,
( ( empty_set @ relation_rng )
= empty_set ),
inference(pattern_uni,[status(thm)],[2233:[bind(A,$thf( empty_set @ relation_rng ))]]) ).
thf(44,plain,
( ( sk1 @ relation_rng )
= ( sk2 @ relation_dom ) ),
inference(cnfConj,[status(thm)],[40]) ).
thf(54,plain,
( ( sk1 @ relation_rng )
= ( sk2 @ relation_dom ) ),
inference(lifteq,[status(thm)],[44]) ).
thf(2292,plain,
( ( ( sk1 @ relation_rng )
!= ( empty_set @ relation_rng ) )
| ( ( sk2 @ relation_dom )
= empty_set ) ),
inference(paramod_ordered,[status(thm)],[2234,54]) ).
thf(2306,plain,
( ( sk1 != empty_set )
| ( ( sk2 @ relation_dom )
= empty_set ) ),
inference(simp,[status(thm)],[2292]) ).
thf(34,axiom,
! [A: $i] :
( ( ( A @ function )
& ( A @ relation ) )
=> ! [B: $i] :
( ( B
= ( A @ relation_rng ) )
<=> ! [C: $i] :
( ( B @ ( C @ in ) )
<=> ? [D: $i] :
( ( C
= ( D @ ( A @ apply ) ) )
& ( A @ relation_dom @ ( D @ in ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d5_funct_1) ).
thf(161,plain,
! [A: $i] :
( ( ( A @ function )
& ( A @ relation ) )
=> ! [B: $i] :
( ( ! [C: $i] :
( ( ? [D: $i] :
( ( C
= ( D @ ( A @ apply ) ) )
& ( A @ relation_dom @ ( D @ in ) ) )
=> ( B @ ( C @ in ) ) )
& ( ( B @ ( C @ in ) )
=> ? [D: $i] :
( ( C
= ( D @ ( A @ apply ) ) )
& ( A @ relation_dom @ ( D @ in ) ) ) ) )
=> ( B
= ( A @ relation_rng ) ) )
& ( ( B
= ( A @ relation_rng ) )
=> ! [C: $i] :
( ( ? [D: $i] :
( ( C
= ( D @ ( A @ apply ) ) )
& ( A @ relation_dom @ ( D @ in ) ) )
=> ( B @ ( C @ in ) ) )
& ( ( B @ ( C @ in ) )
=> ? [D: $i] :
( ( C
= ( D @ ( A @ apply ) ) )
& ( A @ relation_dom @ ( D @ in ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[34]) ).
thf(162,plain,
! [A: $i] :
( ( ( A @ function )
& ( A @ relation ) )
=> ( ! [B: $i] :
( ( ! [C: $i] :
( ? [D: $i] :
( ( C
= ( D @ ( A @ apply ) ) )
& ( A @ relation_dom @ ( D @ in ) ) )
=> ( B @ ( C @ in ) ) )
& ! [C: $i] :
( ( B @ ( C @ in ) )
=> ? [D: $i] :
( ( C
= ( D @ ( A @ apply ) ) )
& ( A @ relation_dom @ ( D @ in ) ) ) ) )
=> ( B
= ( A @ relation_rng ) ) )
& ! [B: $i] :
( ( B
= ( A @ relation_rng ) )
=> ( ! [C: $i] :
( ? [D: $i] :
( ( C
= ( D @ ( A @ apply ) ) )
& ( A @ relation_dom @ ( D @ in ) ) )
=> ( B @ ( C @ in ) ) )
& ! [C: $i] :
( ( B @ ( C @ in ) )
=> ? [D: $i] :
( ( C
= ( D @ ( A @ apply ) ) )
& ( A @ relation_dom @ ( D @ in ) ) ) ) ) ) ) ),
inference(miniscope,[status(thm)],[161]) ).
thf(163,plain,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( F
= ( A @ relation_rng ) )
| ~ ( F @ ( A @ ( F @ sk17 ) @ in ) )
| ( F @ ( A @ sk15 ) )
| ~ ( A @ function )
| ~ ( A @ relation ) )
& ( ( F
= ( A @ relation_rng ) )
| ( ( A @ ( F @ sk17 ) )
= ( A @ ( F @ sk18 ) @ ( A @ apply ) ) )
| ( F @ ( A @ sk15 ) )
| ~ ( A @ function )
| ~ ( A @ relation ) )
& ( ( F
= ( A @ relation_rng ) )
| ( A @ relation_dom @ ( A @ ( F @ sk18 ) @ in ) )
| ( F @ ( A @ sk15 ) )
| ~ ( A @ function )
| ~ ( A @ relation ) )
& ( ( F
= ( A @ relation_rng ) )
| ~ ( F @ ( A @ sk15 ) )
| ( ( A @ ( F @ sk16 ) )
!= ( G @ ( A @ apply ) ) )
| ~ ( A @ relation_dom @ ( G @ in ) )
| ~ ( A @ function )
| ~ ( A @ relation ) )
& ( ( F
= ( A @ relation_rng ) )
| ~ ( F @ ( A @ sk15 ) )
| ( F @ ( A @ ( F @ sk16 ) @ in ) )
| ~ ( A @ function )
| ~ ( A @ relation ) )
& ( ( B @ ( D @ in ) )
| ( D
!= ( E @ ( A @ apply ) ) )
| ~ ( A @ relation_dom @ ( E @ in ) )
| ( B
!= ( A @ relation_rng ) )
| ~ ( A @ function )
| ~ ( A @ relation ) )
& ( ( C
= ( A @ ( B @ ( C @ sk14 ) ) @ ( A @ apply ) ) )
| ~ ( B @ ( C @ in ) )
| ( B
!= ( A @ relation_rng ) )
| ~ ( A @ function )
| ~ ( A @ relation ) )
& ( ( A @ relation_dom @ ( A @ ( B @ ( C @ sk14 ) ) @ in ) )
| ~ ( B @ ( C @ in ) )
| ( B
!= ( A @ relation_rng ) )
| ~ ( A @ function )
| ~ ( A @ relation ) ) ),
inference(cnf,[status(esa)],[162]) ).
thf(165,plain,
! [B: $i,A: $i] :
( ( B
= ( A @ relation_rng ) )
| ( A @ relation_dom @ ( A @ ( B @ sk18 ) @ in ) )
| ( B @ ( A @ sk15 ) )
| ~ ( A @ function )
| ~ ( A @ relation ) ),
inference(cnfConj,[status(thm)],[163]) ).
thf(176,plain,
! [B: $i,A: $i] :
( ( A @ relation_dom @ ( A @ ( B @ sk18 ) @ in ) )
| ( B @ ( A @ sk15 ) )
| ~ ( A @ function )
| ~ ( A @ relation )
| ( B
= ( A @ relation_rng ) ) ),
inference(lifteq,[status(thm)],[165]) ).
thf(177,plain,
! [B: $i,A: $i] :
( ( A @ relation_dom @ ( A @ ( B @ sk18 ) @ in ) )
| ( B @ ( A @ sk15 ) )
| ~ ( A @ function )
| ~ ( A @ relation )
| ( B
= ( A @ relation_rng ) ) ),
inference(simp,[status(thm)],[176]) ).
thf(6921,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ relation )
!= ( A @ relation ) )
| ( A @ relation_dom @ ( A @ ( B @ sk18 ) @ in ) )
| ( B @ ( A @ sk15 ) )
| ~ ( A @ function )
| ~ $true
| ( B
= ( A @ relation_rng ) ) ),
inference(paramod_ordered,[status(thm)],[41,177]) ).
thf(6922,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ relation )
!= ( A @ relation ) )
| ( A @ relation_dom @ ( A @ ( B @ sk18 ) @ in ) )
| ( B @ ( A @ sk15 ) )
| ~ ( A @ function )
| ( B
= ( A @ relation_rng ) ) ),
inference(simp,[status(thm)],[6921]) ).
thf(6923,plain,
! [A: $i] :
( ( sk1 @ relation_dom @ ( sk1 @ ( A @ sk18 ) @ in ) )
| ( A @ ( sk1 @ sk15 ) )
| ~ ( sk1 @ function )
| ( A
= ( sk1 @ relation_rng ) ) ),
inference(pattern_uni,[status(thm)],[6922:[bind(A,$thf( sk1 ))]]) ).
thf(7227,plain,
! [A: $i] :
( ( sk1 @ relation_dom @ ( sk1 @ ( A @ sk18 ) @ in ) )
| ( A @ ( sk1 @ sk15 ) )
| ~ ( sk1 @ function )
| ( A
= ( sk1 @ relation_rng ) ) ),
inference(simp,[status(thm)],[6923]) ).
thf(49,plain,
sk1 @ function,
inference(cnfConj,[status(thm)],[40]) ).
thf(7411,plain,
! [A: $i] :
( ( sk1 @ relation_dom @ ( sk1 @ ( A @ sk18 ) @ in ) )
| ( A @ ( sk1 @ sk15 ) )
| ~ $true
| ( A
= ( sk2 @ relation_dom ) ) ),
inference(rewrite,[status(thm)],[7227,49,54]) ).
thf(7412,plain,
! [A: $i] :
( ( sk1 @ relation_dom @ ( sk1 @ ( A @ sk18 ) @ in ) )
| ( A @ ( sk1 @ sk15 ) )
| ( A
= ( sk2 @ relation_dom ) ) ),
inference(simp,[status(thm)],[7411]) ).
thf(38,axiom,
? [A: $i] :
( ( A @ function )
& ( A @ relation ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc1_funct_1) ).
thf(225,plain,
? [A: $i] :
( ( A @ function )
& ( A @ relation ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[38]) ).
thf(226,plain,
( ( sk24 @ function )
& ( sk24 @ relation ) ),
inference(cnf,[status(esa)],[225]) ).
thf(228,plain,
sk24 @ function,
inference(cnfConj,[status(thm)],[226]) ).
thf(3275,plain,
! [A: $i] :
( ( ( sk24 @ function )
!= ( A @ function ) )
| ( A @ function_inverse @ relation )
| ~ $true
| ~ ( A @ relation ) ),
inference(paramod_ordered,[status(thm)],[228,138]) ).
thf(3276,plain,
! [A: $i] :
( ( ( sk24 @ function )
!= ( A @ function ) )
| ( A @ function_inverse @ relation )
| ~ ( A @ relation ) ),
inference(simp,[status(thm)],[3275]) ).
thf(3277,plain,
( ( sk24 @ function_inverse @ relation )
| ~ ( sk24 @ relation ) ),
inference(pattern_uni,[status(thm)],[3276:[bind(A,$thf( sk24 ))]]) ).
thf(227,plain,
sk24 @ relation,
inference(cnfConj,[status(thm)],[226]) ).
thf(9735,plain,
( ( sk24 @ function_inverse @ relation )
| ~ $true ),
inference(rewrite,[status(thm)],[3277,227]) ).
thf(9736,plain,
sk24 @ function_inverse @ relation,
inference(simp,[status(thm)],[9735]) ).
thf(9785,plain,
! [A: $i] :
( ( A
!= ( sk24 @ function_inverse ) )
| ( sk2 @ relation_dom @ relation )
| ( sk1 @ relation_dom @ ( sk1 @ ( A @ sk18 ) @ in ) )
| ( A @ ( sk1 @ sk15 ) ) ),
inference(paramod_ordered,[status(thm)],[7412,9736]) ).
thf(9786,plain,
( ( sk2 @ relation_dom @ relation )
| ( sk1 @ relation_dom @ ( sk1 @ ( sk24 @ function_inverse @ sk18 ) @ in ) )
| ( sk24 @ function_inverse @ ( sk1 @ sk15 ) ) ),
inference(pattern_uni,[status(thm)],[9785:[bind(A,$thf( sk24 @ function_inverse ))]]) ).
thf(1077,plain,
( ( ( sk1 @ function_inverse @ empty )
!= ( empty_set @ empty ) )
| ~ ( sk2 @ empty )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[69,962]) ).
thf(1078,plain,
( ( ( sk1 @ function_inverse @ empty )
!= ( empty_set @ empty ) )
| ~ ( sk2 @ empty ) ),
inference(simp,[status(thm)],[1077]) ).
thf(1110,plain,
( ( ( sk1 @ function_inverse )
!= empty_set )
| ~ ( sk2 @ empty ) ),
inference(simp,[status(thm)],[1078]) ).
thf(20,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ in ) )
=> ( B @ ( A @ element ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t1_subset) ).
thf(115,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ in ) )
=> ( B @ ( A @ element ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[20]) ).
thf(36,axiom,
! [A: $i] :
( ( ( A @ function )
& ( A @ relation ) )
=> ( ( A @ one_to_one )
=> ! [B: $i] :
( ( ( B @ function )
& ( B @ relation ) )
=> ( ( B
= ( A @ function_inverse ) )
<=> ( ! [C: $i,D: $i] :
( ( ( ( C
= ( D @ ( A @ apply ) ) )
& ( A @ relation_dom @ ( D @ in ) ) )
=> ( ( D
= ( C @ ( B @ apply ) ) )
& ( A @ relation_rng @ ( C @ in ) ) ) )
& ( ( ( D
= ( C @ ( B @ apply ) ) )
& ( A @ relation_rng @ ( C @ in ) ) )
=> ( ( C
= ( D @ ( A @ apply ) ) )
& ( A @ relation_dom @ ( D @ in ) ) ) ) )
& ( ( B @ relation_dom )
= ( A @ relation_rng ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t54_funct_1) ).
thf(190,plain,
! [A: $i] :
( ( ( A @ function )
& ( A @ relation ) )
=> ( ( A @ one_to_one )
=> ! [B: $i] :
( ( ( B @ function )
& ( B @ relation ) )
=> ( ( ( ! [C: $i,D: $i] :
( ( ( ( C
= ( D @ ( A @ apply ) ) )
& ( A @ relation_dom @ ( D @ in ) ) )
=> ( ( D
= ( C @ ( B @ apply ) ) )
& ( A @ relation_rng @ ( C @ in ) ) ) )
& ( ( ( D
= ( C @ ( B @ apply ) ) )
& ( A @ relation_rng @ ( C @ in ) ) )
=> ( ( C
= ( D @ ( A @ apply ) ) )
& ( A @ relation_dom @ ( D @ in ) ) ) ) )
& ( ( B @ relation_dom )
= ( A @ relation_rng ) ) )
=> ( B
= ( A @ function_inverse ) ) )
& ( ( B
= ( A @ function_inverse ) )
=> ( ! [C: $i,D: $i] :
( ( ( ( C
= ( D @ ( A @ apply ) ) )
& ( A @ relation_dom @ ( D @ in ) ) )
=> ( ( D
= ( C @ ( B @ apply ) ) )
& ( A @ relation_rng @ ( C @ in ) ) ) )
& ( ( ( D
= ( C @ ( B @ apply ) ) )
& ( A @ relation_rng @ ( C @ in ) ) )
=> ( ( C
= ( D @ ( A @ apply ) ) )
& ( A @ relation_dom @ ( D @ in ) ) ) ) )
& ( ( B @ relation_dom )
= ( A @ relation_rng ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[36]) ).
thf(191,plain,
! [A: $i] :
( ( ( A @ function )
& ( A @ relation ) )
=> ( ( A @ one_to_one )
=> ! [B: $i] :
( ( ( B @ function )
& ( B @ relation ) )
=> ( ( ( ! [C: $i,D: $i] :
( ( ( C
= ( D @ ( A @ apply ) ) )
& ( A @ relation_dom @ ( D @ in ) ) )
=> ( ( D
= ( C @ ( B @ apply ) ) )
& ( A @ relation_rng @ ( C @ in ) ) ) )
& ! [C: $i,D: $i] :
( ( ( D
= ( C @ ( B @ apply ) ) )
& ( A @ relation_rng @ ( C @ in ) ) )
=> ( ( C
= ( D @ ( A @ apply ) ) )
& ( A @ relation_dom @ ( D @ in ) ) ) )
& ( ( B @ relation_dom )
= ( A @ relation_rng ) ) )
=> ( B
= ( A @ function_inverse ) ) )
& ( ( B
= ( A @ function_inverse ) )
=> ( ! [C: $i,D: $i] :
( ( ( C
= ( D @ ( A @ apply ) ) )
& ( A @ relation_dom @ ( D @ in ) ) )
=> ( ( D
= ( C @ ( B @ apply ) ) )
& ( A @ relation_rng @ ( C @ in ) ) ) )
& ! [C: $i,D: $i] :
( ( ( D
= ( C @ ( B @ apply ) ) )
& ( A @ relation_rng @ ( C @ in ) ) )
=> ( ( C
= ( D @ ( A @ apply ) ) )
& ( A @ relation_dom @ ( D @ in ) ) ) )
& ( ( B @ relation_dom )
= ( A @ relation_rng ) ) ) ) ) ) ) ),
inference(miniscope,[status(thm)],[190]) ).
thf(192,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B
= ( A @ function_inverse ) )
| ( ( A @ ( B @ sk23 ) )
!= ( A @ ( B @ sk22 ) @ ( B @ apply ) ) )
| ~ ( A @ relation_rng @ ( A @ ( B @ sk22 ) @ in ) )
| ( B @ ( A @ sk19 ) )
| ( ( B @ relation_dom )
!= ( A @ relation_rng ) )
| ~ ( B @ function )
| ~ ( B @ relation )
| ~ ( A @ one_to_one )
| ~ ( A @ function )
| ~ ( A @ relation ) )
& ( ( B
= ( A @ function_inverse ) )
| ( ( A @ ( B @ sk22 ) )
= ( A @ ( B @ sk23 ) @ ( A @ apply ) ) )
| ( B @ ( A @ sk19 ) )
| ( ( B @ relation_dom )
!= ( A @ relation_rng ) )
| ~ ( B @ function )
| ~ ( B @ relation )
| ~ ( A @ one_to_one )
| ~ ( A @ function )
| ~ ( A @ relation ) )
& ( ( B
= ( A @ function_inverse ) )
| ( A @ relation_dom @ ( A @ ( B @ sk23 ) @ in ) )
| ( B @ ( A @ sk19 ) )
| ( ( B @ relation_dom )
!= ( A @ relation_rng ) )
| ~ ( B @ function )
| ~ ( B @ relation )
| ~ ( A @ one_to_one )
| ~ ( A @ function )
| ~ ( A @ relation ) )
& ( ( B
= ( A @ function_inverse ) )
| ~ ( B @ ( A @ sk19 ) )
| ( ( A @ ( B @ sk20 ) )
!= ( A @ ( B @ sk21 ) @ ( A @ apply ) ) )
| ~ ( A @ relation_dom @ ( A @ ( B @ sk21 ) @ in ) )
| ( ( B @ relation_dom )
!= ( A @ relation_rng ) )
| ~ ( B @ function )
| ~ ( B @ relation )
| ~ ( A @ one_to_one )
| ~ ( A @ function )
| ~ ( A @ relation ) )
& ( ( B
= ( A @ function_inverse ) )
| ~ ( B @ ( A @ sk19 ) )
| ( ( A @ ( B @ sk21 ) )
= ( A @ ( B @ sk20 ) @ ( B @ apply ) ) )
| ( ( B @ relation_dom )
!= ( A @ relation_rng ) )
| ~ ( B @ function )
| ~ ( B @ relation )
| ~ ( A @ one_to_one )
| ~ ( A @ function )
| ~ ( A @ relation ) )
& ( ( B
= ( A @ function_inverse ) )
| ~ ( B @ ( A @ sk19 ) )
| ( A @ relation_rng @ ( A @ ( B @ sk20 ) @ in ) )
| ( ( B @ relation_dom )
!= ( A @ relation_rng ) )
| ~ ( B @ function )
| ~ ( B @ relation )
| ~ ( A @ one_to_one )
| ~ ( A @ function )
| ~ ( A @ relation ) )
& ( ( F
= ( E @ ( B @ apply ) ) )
| ( E
!= ( F @ ( A @ apply ) ) )
| ~ ( A @ relation_dom @ ( F @ in ) )
| ( B
!= ( A @ function_inverse ) )
| ~ ( B @ function )
| ~ ( B @ relation )
| ~ ( A @ one_to_one )
| ~ ( A @ function )
| ~ ( A @ relation ) )
& ( ( A @ relation_rng @ ( E @ in ) )
| ( E
!= ( F @ ( A @ apply ) ) )
| ~ ( A @ relation_dom @ ( F @ in ) )
| ( B
!= ( A @ function_inverse ) )
| ~ ( B @ function )
| ~ ( B @ relation )
| ~ ( A @ one_to_one )
| ~ ( A @ function )
| ~ ( A @ relation ) )
& ( ( C
= ( D @ ( A @ apply ) ) )
| ( D
!= ( C @ ( B @ apply ) ) )
| ~ ( A @ relation_rng @ ( C @ in ) )
| ( B
!= ( A @ function_inverse ) )
| ~ ( B @ function )
| ~ ( B @ relation )
| ~ ( A @ one_to_one )
| ~ ( A @ function )
| ~ ( A @ relation ) )
& ( ( A @ relation_dom @ ( D @ in ) )
| ( D
!= ( C @ ( B @ apply ) ) )
| ~ ( A @ relation_rng @ ( C @ in ) )
| ( B
!= ( A @ function_inverse ) )
| ~ ( B @ function )
| ~ ( B @ relation )
| ~ ( A @ one_to_one )
| ~ ( A @ function )
| ~ ( A @ relation ) )
& ( ( ( B @ relation_dom )
= ( A @ relation_rng ) )
| ( B
!= ( A @ function_inverse ) )
| ~ ( B @ function )
| ~ ( B @ relation )
| ~ ( A @ one_to_one )
| ~ ( A @ function )
| ~ ( A @ relation ) ) ),
inference(cnf,[status(esa)],[191]) ).
thf(203,plain,
! [B: $i,A: $i] :
( ( B
= ( A @ function_inverse ) )
| ~ ( B @ ( A @ sk19 ) )
| ( ( A @ ( B @ sk21 ) )
= ( A @ ( B @ sk20 ) @ ( B @ apply ) ) )
| ( ( B @ relation_dom )
!= ( A @ relation_rng ) )
| ~ ( B @ function )
| ~ ( B @ relation )
| ~ ( A @ one_to_one )
| ~ ( A @ function )
| ~ ( A @ relation ) ),
inference(cnfConj,[status(thm)],[192]) ).
thf(217,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ sk19 ) )
| ~ ( B @ function )
| ~ ( B @ relation )
| ~ ( A @ one_to_one )
| ~ ( A @ function )
| ~ ( A @ relation )
| ( B
= ( A @ function_inverse ) )
| ( ( A @ ( B @ sk21 ) )
= ( A @ ( B @ sk20 ) @ ( B @ apply ) ) )
| ( ( B @ relation_dom )
!= ( A @ relation_rng ) ) ),
inference(lifteq,[status(thm)],[203]) ).
thf(2266,plain,
! [A: $i] :
( ( ( empty_set @ relation_rng @ empty )
!= ( A @ empty ) )
| ( A @ relation_rng @ empty )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2165,107]) ).
thf(2267,plain,
! [A: $i] :
( ( ( empty_set @ relation_rng @ empty )
!= ( A @ empty ) )
| ( A @ relation_rng @ empty ) ),
inference(simp,[status(thm)],[2266]) ).
thf(2268,plain,
empty_set @ relation_rng @ relation_rng @ empty,
inference(pattern_uni,[status(thm)],[2267:[bind(A,$thf( empty_set @ relation_rng ))]]) ).
thf(2318,plain,
empty_set @ relation_rng @ empty,
inference(rewrite,[status(thm)],[2268,2234]) ).
thf(108,plain,
! [A: $i] :
( ( A @ relation_rng @ relation )
| ~ ( A @ empty ) ),
inference(cnfConj,[status(thm)],[106]) ).
thf(2405,plain,
! [A: $i] :
( ( ( empty_set @ relation_rng @ empty )
!= ( A @ empty ) )
| ( A @ relation_rng @ relation )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2318,108]) ).
thf(2406,plain,
! [A: $i] :
( ( ( empty_set @ relation_rng @ empty )
!= ( A @ empty ) )
| ( A @ relation_rng @ relation ) ),
inference(simp,[status(thm)],[2405]) ).
thf(2407,plain,
empty_set @ relation_rng @ relation_rng @ relation,
inference(pattern_uni,[status(thm)],[2406:[bind(A,$thf( empty_set @ relation_rng ))]]) ).
thf(2419,plain,
empty_set @ relation_rng @ relation,
inference(rewrite,[status(thm)],[2407,2234]) ).
thf(7587,plain,
! [A: $i] :
( ( A
!= ( empty_set @ relation_rng ) )
| ( sk2 @ relation_dom @ relation )
| ( sk1 @ relation_dom @ ( sk1 @ ( A @ sk18 ) @ in ) )
| ( A @ ( sk1 @ sk15 ) ) ),
inference(paramod_ordered,[status(thm)],[7412,2419]) ).
thf(7588,plain,
( ( sk2 @ relation_dom @ relation )
| ( sk1 @ relation_dom @ ( sk1 @ ( empty_set @ relation_rng @ sk18 ) @ in ) )
| ( empty_set @ relation_rng @ ( sk1 @ sk15 ) ) ),
inference(pattern_uni,[status(thm)],[7587:[bind(A,$thf( empty_set @ relation_rng ))]]) ).
thf(9887,plain,
( ( sk2 @ relation_dom @ relation )
| ( sk1 @ relation_dom @ ( sk1 @ ( empty_set @ sk18 ) @ in ) )
| ( empty_set @ ( sk1 @ sk15 ) ) ),
inference(rewrite,[status(thm)],[7588,2234]) ).
thf(116,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ element ) )
| ~ ( B @ ( A @ in ) ) ),
inference(cnf,[status(esa)],[115]) ).
thf(9899,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ relation_dom @ ( sk1 @ ( empty_set @ sk18 ) @ in ) )
!= ( B @ ( A @ in ) ) )
| ( B @ ( A @ element ) )
| ~ $true
| ( sk2 @ relation_dom @ relation )
| ( empty_set @ ( sk1 @ sk15 ) ) ),
inference(paramod_ordered,[status(thm)],[9887,116]) ).
thf(9900,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ relation_dom @ ( sk1 @ ( empty_set @ sk18 ) @ in ) )
!= ( B @ ( A @ in ) ) )
| ( B @ ( A @ element ) )
| ( sk2 @ relation_dom @ relation )
| ( empty_set @ ( sk1 @ sk15 ) ) ),
inference(simp,[status(thm)],[9899]) ).
thf(9901,plain,
( ( sk1 @ relation_dom @ ( sk1 @ ( empty_set @ sk18 ) @ element ) )
| ( sk2 @ relation_dom @ relation )
| ( empty_set @ ( sk1 @ sk15 ) ) ),
inference(pattern_uni,[status(thm)],[9900:[bind(A,$thf( sk1 @ ( empty_set @ sk18 ) )),bind(B,$thf( sk1 @ relation_dom ))]]) ).
thf(29,axiom,
? [A: $i] :
( ( A @ relation )
& ~ ( A @ empty ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc2_relat_1) ).
thf(147,plain,
? [A: $i] :
( ( A @ relation )
& ~ ( A @ empty ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[29]) ).
thf(148,plain,
( ( sk13 @ relation )
& ~ ( sk13 @ empty ) ),
inference(cnf,[status(esa)],[147]) ).
thf(149,plain,
~ ( sk13 @ empty ),
inference(cnfConj,[status(thm)],[148]) ).
thf(14493,plain,
( ( ( sk13 @ empty )
!= ( sk1 @ empty ) )
| ~ $true
| ( sk2 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[13760,149]) ).
thf(14494,plain,
( ( ( sk13 @ empty )
!= ( sk1 @ empty ) )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[14493]) ).
thf(14565,plain,
( ( sk13 != sk1 )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[14494]) ).
thf(14660,plain,
! [A: $i] :
( ( A != sk2 )
| ( sk13 != sk1 )
| ( empty_set != empty_set )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[85,14565]) ).
thf(14661,plain,
! [A: $i] :
( ( A != sk2 )
| ( sk13 != sk1 )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[14660]) ).
thf(14662,plain,
( ( sk13 != sk1 )
| ~ ( sk2 @ empty ) ),
inference(pattern_uni,[status(thm)],[14661:[bind(A,$thf( sk2 ))]]) ).
thf(28,axiom,
? [A: $i] :
( ( A @ function )
& ( A @ empty )
& ( A @ relation ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc2_funct_1) ).
thf(142,plain,
? [A: $i] :
( ( A @ function )
& ( A @ empty )
& ( A @ relation ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[28]) ).
thf(143,plain,
( ( sk12 @ function )
& ( sk12 @ empty )
& ( sk12 @ relation ) ),
inference(cnf,[status(esa)],[142]) ).
thf(146,plain,
sk12 @ function,
inference(cnfConj,[status(thm)],[143]) ).
thf(145,plain,
sk12 @ empty,
inference(cnfConj,[status(thm)],[143]) ).
thf(1814,plain,
! [A: $i] :
( ( ( sk12 @ empty )
!= ( A @ empty ) )
| ~ $true
| ( A = empty_set ) ),
inference(paramod_ordered,[status(thm)],[145,85]) ).
thf(1815,plain,
! [A: $i] :
( ( ( sk12 @ empty )
!= ( A @ empty ) )
| ( A = empty_set ) ),
inference(simp,[status(thm)],[1814]) ).
thf(1816,plain,
sk12 = empty_set,
inference(pattern_uni,[status(thm)],[1815:[bind(A,$thf( sk12 ))]]) ).
thf(2014,plain,
empty_set @ function,
inference(rewrite,[status(thm)],[146,1816]) ).
thf(2184,plain,
! [A: $i] :
( ( ( sk1 @ relation_rng )
!= ( A @ relation_rng ) )
| ( sk2 @ relation_dom @ empty )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[54,107]) ).
thf(2185,plain,
( ( sk2 @ relation_dom @ empty )
| ~ ( sk1 @ empty ) ),
inference(pattern_uni,[status(thm)],[2184:[bind(A,$thf( sk1 ))]]) ).
thf(43,plain,
sk2 @ relation,
inference(cnfConj,[status(thm)],[40]) ).
thf(4104,plain,
! [A: $i] :
( ( ( sk2 @ relation )
!= ( A @ relation ) )
| ~ ( A @ relation_dom @ empty )
| ~ $true
| ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[43,141]) ).
thf(4105,plain,
! [A: $i] :
( ( ( sk2 @ relation )
!= ( A @ relation ) )
| ~ ( A @ relation_dom @ empty )
| ( A @ empty ) ),
inference(simp,[status(thm)],[4104]) ).
thf(4106,plain,
( ~ ( sk2 @ relation_dom @ empty )
| ( sk2 @ empty ) ),
inference(pattern_uni,[status(thm)],[4105:[bind(A,$thf( sk2 ))]]) ).
thf(17562,plain,
( ( ( sk2 @ relation_dom @ empty )
!= ( sk2 @ relation_dom @ empty ) )
| ~ $true
| ( sk2 @ empty )
| ~ ( sk1 @ empty ) ),
inference(paramod_ordered,[status(thm)],[2185,4106]) ).
thf(17563,plain,
( ( ( sk2 @ relation_dom @ empty )
!= ( sk2 @ relation_dom @ empty ) )
| ( sk2 @ empty )
| ~ ( sk1 @ empty ) ),
inference(simp,[status(thm)],[17562]) ).
thf(17564,plain,
( ( sk2 @ empty )
| ~ ( sk1 @ empty ) ),
inference(pattern_uni,[status(thm)],[17563:[]]) ).
thf(6,axiom,
? [A: $i] :
~ ( A @ empty ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc2_xboole_0) ).
thf(66,plain,
? [A: $i] :
~ ( A @ empty ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(67,plain,
~ ! [A: $i] : ( A @ empty ),
inference(miniscope,[status(thm)],[66]) ).
thf(68,plain,
~ ( sk4 @ empty ),
inference(cnf,[status(esa)],[67]) ).
thf(14553,plain,
( ( ( sk4 @ empty )
!= ( sk1 @ empty ) )
| ~ $true
| ( sk2 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[13760,68]) ).
thf(14554,plain,
( ( ( sk4 @ empty )
!= ( sk1 @ empty ) )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[14553]) ).
thf(14573,plain,
( ( sk4 != sk1 )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[14554]) ).
thf(14685,plain,
! [A: $i] :
( ( A != sk2 )
| ( sk4 != sk1 )
| ( empty_set != empty_set )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[85,14573]) ).
thf(14686,plain,
! [A: $i] :
( ( A != sk2 )
| ( sk4 != sk1 )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[14685]) ).
thf(14687,plain,
( ( sk4 != sk1 )
| ~ ( sk2 @ empty ) ),
inference(pattern_uni,[status(thm)],[14686:[bind(A,$thf( sk2 ))]]) ).
thf(17686,plain,
( ( ( sk2 @ empty )
!= ( sk2 @ empty ) )
| ( sk4 != sk1 )
| ~ $true
| ~ ( sk1 @ empty ) ),
inference(paramod_ordered,[status(thm)],[17564,14687]) ).
thf(17687,plain,
( ( ( sk2 @ empty )
!= ( sk2 @ empty ) )
| ( sk4 != sk1 )
| ~ ( sk1 @ empty ) ),
inference(simp,[status(thm)],[17686]) ).
thf(17688,plain,
( ( sk4 != sk1 )
| ~ ( sk1 @ empty ) ),
inference(pattern_uni,[status(thm)],[17687:[]]) ).
thf(150,plain,
sk13 @ relation,
inference(cnfConj,[status(thm)],[148]) ).
thf(139,plain,
! [A: $i] :
( ( A @ function_inverse @ function )
| ~ ( A @ function )
| ~ ( A @ relation ) ),
inference(cnfConj,[status(thm)],[137]) ).
thf(3691,plain,
! [A: $i] :
( ( ( sk13 @ relation )
!= ( A @ relation ) )
| ( A @ function_inverse @ function )
| ~ ( A @ function )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[150,139]) ).
thf(3692,plain,
! [A: $i] :
( ( ( sk13 @ relation )
!= ( A @ relation ) )
| ( A @ function_inverse @ function )
| ~ ( A @ function ) ),
inference(simp,[status(thm)],[3691]) ).
thf(3693,plain,
( ( sk13 @ function_inverse @ function )
| ~ ( sk13 @ function ) ),
inference(pattern_uni,[status(thm)],[3692:[bind(A,$thf( sk13 ))]]) ).
thf(31,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ in ) )
=> ~ ( A @ ( B @ in ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',antisymmetry_r2_hidden) ).
thf(153,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ in ) )
=> ~ ( A @ ( B @ in ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[31]) ).
thf(2246,plain,
( ( ( sk1 @ relation_rng )
!= ( empty_set @ relation_rng ) )
| ( sk2 @ relation_dom @ empty ) ),
inference(paramod_ordered,[status(thm)],[54,2165]) ).
thf(2279,plain,
( ( sk1 != empty_set )
| ( sk2 @ relation_dom @ empty ) ),
inference(simp,[status(thm)],[2246]) ).
thf(17598,plain,
( ( ( sk2 @ relation_dom @ empty )
!= ( sk2 @ relation_dom @ empty ) )
| ~ $true
| ( sk2 @ empty )
| ( sk1 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[2279,4106]) ).
thf(17599,plain,
( ( ( sk2 @ relation_dom @ empty )
!= ( sk2 @ relation_dom @ empty ) )
| ( sk2 @ empty )
| ( sk1 != empty_set ) ),
inference(simp,[status(thm)],[17598]) ).
thf(17600,plain,
( ( sk2 @ empty )
| ( sk1 != empty_set ) ),
inference(pattern_uni,[status(thm)],[17599:[]]) ).
thf(17893,plain,
( ( ( sk13 @ empty )
!= ( sk2 @ empty ) )
| ~ $true
| ( sk1 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[17600,149]) ).
thf(17894,plain,
( ( ( sk13 @ empty )
!= ( sk2 @ empty ) )
| ( sk1 != empty_set ) ),
inference(simp,[status(thm)],[17893]) ).
thf(17976,plain,
( ( sk13 != sk2 )
| ( sk1 != empty_set ) ),
inference(simp,[status(thm)],[17894]) ).
thf(5,axiom,
? [A: $i] : ( A @ empty ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc1_xboole_0) ).
thf(64,plain,
? [A: $i] : ( A @ empty ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(65,plain,
sk3 @ empty,
inference(cnf,[status(esa)],[64]) ).
thf(1703,plain,
! [A: $i] :
( ( ( sk3 @ empty )
!= ( A @ empty ) )
| ~ $true
| ( A = empty_set ) ),
inference(paramod_ordered,[status(thm)],[65,85]) ).
thf(1704,plain,
! [A: $i] :
( ( ( sk3 @ empty )
!= ( A @ empty ) )
| ( A = empty_set ) ),
inference(simp,[status(thm)],[1703]) ).
thf(1705,plain,
sk3 = empty_set,
inference(pattern_uni,[status(thm)],[1704:[bind(A,$thf( sk3 ))]]) ).
thf(3516,plain,
( ( ( sk2 @ relation_dom @ empty )
!= ( sk4 @ empty ) )
| ~ $true
| ~ ( sk1 @ empty ) ),
inference(paramod_ordered,[status(thm)],[2185,68]) ).
thf(3517,plain,
( ( ( sk2 @ relation_dom @ empty )
!= ( sk4 @ empty ) )
| ~ ( sk1 @ empty ) ),
inference(simp,[status(thm)],[3516]) ).
thf(3522,plain,
( ( ( sk2 @ relation_dom )
!= sk4 )
| ~ ( sk1 @ empty ) ),
inference(simp,[status(thm)],[3517]) ).
thf(14504,plain,
( ( ( sk1 @ empty )
!= ( sk1 @ empty ) )
| ( ( sk2 @ relation_dom )
!= sk4 )
| ~ $true
| ( sk2 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[13760,3522]) ).
thf(14505,plain,
( ( ( sk1 @ empty )
!= ( sk1 @ empty ) )
| ( ( sk2 @ relation_dom )
!= sk4 )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[14504]) ).
thf(14506,plain,
( ( ( sk2 @ relation_dom )
!= sk4 )
| ( sk2 != empty_set ) ),
inference(pattern_uni,[status(thm)],[14505:[]]) ).
thf(171,plain,
! [B: $i,A: $i] :
( ( B
= ( A @ relation_rng ) )
| ~ ( B @ ( A @ ( B @ sk17 ) @ in ) )
| ( B @ ( A @ sk15 ) )
| ~ ( A @ function )
| ~ ( A @ relation ) ),
inference(cnfConj,[status(thm)],[163]) ).
thf(184,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ ( B @ sk17 ) @ in ) )
| ( B @ ( A @ sk15 ) )
| ~ ( A @ function )
| ~ ( A @ relation )
| ( B
= ( A @ relation_rng ) ) ),
inference(lifteq,[status(thm)],[171]) ).
thf(185,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ ( B @ sk17 ) @ in ) )
| ( B @ ( A @ sk15 ) )
| ~ ( A @ function )
| ~ ( A @ relation )
| ( B
= ( A @ relation_rng ) ) ),
inference(simp,[status(thm)],[184]) ).
thf(42,plain,
sk2 @ function,
inference(cnfConj,[status(thm)],[40]) ).
thf(1612,plain,
! [A: $i] :
( ( A != sk1 )
| ( ( empty_set @ function_inverse )
!= sk2 )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[85,55]) ).
thf(1613,plain,
( ( ( empty_set @ function_inverse )
!= sk2 )
| ~ ( sk1 @ empty ) ),
inference(pattern_uni,[status(thm)],[1612:[bind(A,$thf( sk1 ))]]) ).
thf(17787,plain,
( ( ( sk1 @ empty )
!= ( sk1 @ empty ) )
| ( sk2 @ empty )
| ~ $true
| ( sk2 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[13760,17564]) ).
thf(17788,plain,
( ( ( sk1 @ empty )
!= ( sk1 @ empty ) )
| ( sk2 @ empty )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[17787]) ).
thf(17789,plain,
( ( sk2 @ empty )
| ( sk2 != empty_set ) ),
inference(pattern_uni,[status(thm)],[17788:[]]) ).
thf(20394,plain,
( ( ( sk13 @ empty )
!= ( sk2 @ empty ) )
| ~ $true
| ( sk2 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[17789,149]) ).
thf(20395,plain,
( ( ( sk13 @ empty )
!= ( sk2 @ empty ) )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[20394]) ).
thf(20488,plain,
( ( sk13 != sk2 )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[20395]) ).
thf(14628,plain,
! [A: $i] :
( ( A != sk2 )
| ( empty_set @ one_to_one )
| ( empty_set != empty_set )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[85,14463]) ).
thf(14629,plain,
! [A: $i] :
( ( A != sk2 )
| ( empty_set @ one_to_one )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[14628]) ).
thf(14630,plain,
( ( empty_set @ one_to_one )
| ~ ( sk2 @ empty ) ),
inference(pattern_uni,[status(thm)],[14629:[bind(A,$thf( sk2 ))]]) ).
thf(2200,plain,
! [A: $i] :
( ( ( sk2 @ relation_rng )
!= ( A @ relation_rng ) )
| ( sk1 @ relation_dom @ empty )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[51,107]) ).
thf(2201,plain,
( ( sk1 @ relation_dom @ empty )
| ~ ( sk2 @ empty ) ),
inference(pattern_uni,[status(thm)],[2200:[bind(A,$thf( sk2 ))]]) ).
thf(25,axiom,
! [A: $i] :
( ( A @ empty )
=> ( A @ function ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc1_funct_1) ).
thf(134,plain,
! [A: $i] :
( ( A @ empty )
=> ( A @ function ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[25]) ).
thf(135,plain,
! [A: $i] :
( ( A @ function )
| ~ ( A @ empty ) ),
inference(cnf,[status(esa)],[134]) ).
thf(3572,plain,
! [A: $i] :
( ( ( sk1 @ relation_dom @ empty )
!= ( A @ empty ) )
| ( A @ function )
| ~ $true
| ~ ( sk2 @ empty ) ),
inference(paramod_ordered,[status(thm)],[2201,135]) ).
thf(3573,plain,
! [A: $i] :
( ( ( sk1 @ relation_dom @ empty )
!= ( A @ empty ) )
| ( A @ function )
| ~ ( sk2 @ empty ) ),
inference(simp,[status(thm)],[3572]) ).
thf(3574,plain,
( ( sk1 @ relation_dom @ function )
| ~ ( sk2 @ empty ) ),
inference(pattern_uni,[status(thm)],[3573:[bind(A,$thf( sk1 @ relation_dom ))]]) ).
thf(22,axiom,
? [A: $i] :
( ( A @ one_to_one )
& ( A @ function )
& ( A @ relation ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc3_funct_1) ).
thf(121,plain,
? [A: $i] :
( ( A @ one_to_one )
& ( A @ function )
& ( A @ relation ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[22]) ).
thf(122,plain,
( ( sk10 @ one_to_one )
& ( sk10 @ function )
& ( sk10 @ relation ) ),
inference(cnf,[status(esa)],[121]) ).
thf(125,plain,
sk10 @ one_to_one,
inference(cnfConj,[status(thm)],[122]) ).
thf(32,axiom,
! [A: $i] :
( ( A @ empty )
=> ( ( A @ relation_dom @ relation )
& ( A @ relation_dom @ empty ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc7_relat_1) ).
thf(155,plain,
! [A: $i] :
( ( A @ empty )
=> ( ( A @ relation_dom @ relation )
& ( A @ relation_dom @ empty ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[32]) ).
thf(156,plain,
! [A: $i] :
( ( ( A @ relation_dom @ relation )
| ~ ( A @ empty ) )
& ( ( A @ relation_dom @ empty )
| ~ ( A @ empty ) ) ),
inference(cnf,[status(esa)],[155]) ).
thf(157,plain,
! [A: $i] :
( ( A @ relation_dom @ empty )
| ~ ( A @ empty ) ),
inference(cnfConj,[status(thm)],[156]) ).
thf(4117,plain,
! [A: $i] :
( ( ( sk24 @ relation )
!= ( A @ relation ) )
| ~ ( A @ relation_dom @ empty )
| ~ $true
| ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[227,141]) ).
thf(4118,plain,
! [A: $i] :
( ( ( sk24 @ relation )
!= ( A @ relation ) )
| ~ ( A @ relation_dom @ empty )
| ( A @ empty ) ),
inference(simp,[status(thm)],[4117]) ).
thf(4119,plain,
( ~ ( sk24 @ relation_dom @ empty )
| ( sk24 @ empty ) ),
inference(pattern_uni,[status(thm)],[4118:[bind(A,$thf( sk24 ))]]) ).
thf(35,axiom,
! [A: $i] :
( ( ( A @ relation )
& ~ ( A @ empty ) )
=> ~ ( A @ relation_rng @ empty ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc6_relat_1) ).
thf(188,plain,
! [A: $i] :
( ( ( A @ relation )
& ~ ( A @ empty ) )
=> ~ ( A @ relation_rng @ empty ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[35]) ).
thf(189,plain,
! [A: $i] :
( ~ ( A @ relation_rng @ empty )
| ~ ( A @ relation )
| ( A @ empty ) ),
inference(cnf,[status(esa)],[188]) ).
thf(3,axiom,
! [A: $i,B: $i] : ( A @ ( A @ subset ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',reflexivity_r1_tarski) ).
thf(58,plain,
! [A: $i] : ( A @ ( A @ subset ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(59,plain,
! [A: $i] : ( A @ ( A @ subset ) ),
inference(cnf,[status(esa)],[58]) ).
thf(8,axiom,
! [A: $i,B: $i] :
( ( B @ powerset @ ( A @ element ) )
<=> ( B @ ( A @ subset ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t3_subset) ).
thf(70,plain,
! [A: $i,B: $i] :
( ( ( B @ ( A @ subset ) )
=> ( B @ powerset @ ( A @ element ) ) )
& ( ( B @ powerset @ ( A @ element ) )
=> ( B @ ( A @ subset ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(71,plain,
( ! [A: $i,B: $i] :
( ( B @ ( A @ subset ) )
=> ( B @ powerset @ ( A @ element ) ) )
& ! [A: $i,B: $i] :
( ( B @ powerset @ ( A @ element ) )
=> ( B @ ( A @ subset ) ) ) ),
inference(miniscope,[status(thm)],[70]) ).
thf(72,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ powerset @ ( C @ element ) )
| ~ ( D @ ( C @ subset ) ) )
& ( ( B @ ( A @ subset ) )
| ~ ( B @ powerset @ ( A @ element ) ) ) ),
inference(cnf,[status(esa)],[71]) ).
thf(74,plain,
! [B: $i,A: $i] :
( ( B @ powerset @ ( A @ element ) )
| ~ ( B @ ( A @ subset ) ) ),
inference(cnfConj,[status(thm)],[72]) ).
thf(75,plain,
! [B: $i,A: $i] :
( ( B @ powerset @ ( A @ element ) )
| ~ ( B @ ( A @ subset ) ) ),
inference(simp,[status(thm)],[74]) ).
thf(1238,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ subset ) )
!= ( C @ ( B @ subset ) ) )
| ( C @ powerset @ ( B @ element ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[59,75]) ).
thf(1239,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ subset ) )
!= ( C @ ( B @ subset ) ) )
| ( C @ powerset @ ( B @ element ) ) ),
inference(simp,[status(thm)],[1238]) ).
thf(1240,plain,
! [A: $i] : ( A @ powerset @ ( A @ element ) ),
inference(pattern_uni,[status(thm)],[1239:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( A ))]]) ).
thf(2590,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ element ) )
!= ( C @ ( B @ element ) ) )
| ( C @ ( B @ in ) )
| ( C @ empty )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1240,133]) ).
thf(2591,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ element ) )
!= ( C @ ( B @ element ) ) )
| ( C @ ( B @ in ) )
| ( C @ empty ) ),
inference(simp,[status(thm)],[2590]) ).
thf(2592,plain,
! [A: $i] :
( ( A @ powerset @ ( A @ in ) )
| ( A @ powerset @ empty ) ),
inference(pattern_uni,[status(thm)],[2591:[bind(A,$thf( D )),bind(B,$thf( D )),bind(C,$thf( D @ powerset ))]]) ).
thf(2596,plain,
! [A: $i] :
( ( A @ powerset @ ( A @ in ) )
| ( A @ powerset @ empty ) ),
inference(simp,[status(thm)],[2592]) ).
thf(3375,plain,
! [A: $i] :
( ( A @ powerset @ ( A @ in ) )
| $false ),
inference(rewrite,[status(thm)],[2596,82]) ).
thf(3376,plain,
! [A: $i] : ( A @ powerset @ ( A @ in ) ),
inference(simp,[status(thm)],[3375]) ).
thf(154,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ in ) )
| ~ ( B @ ( A @ in ) ) ),
inference(cnf,[status(esa)],[153]) ).
thf(4623,plain,
! [B: $i,A: $i] :
( ~ $true
| ( ( A @ ( B @ in ) )
!= ( B @ ( A @ in ) ) )
| ~ ( B @ ( A @ in ) ) ),
inference(eqfactor_ordered,[status(thm)],[154]) ).
thf(4624,plain,
! [A: $i] :
~ ( A @ ( A @ in ) ),
inference(pattern_uni,[status(thm)],[4623:[bind(A,$thf( B ))]]) ).
thf(4630,plain,
! [A: $i] :
~ ( A @ ( A @ in ) ),
inference(simp,[status(thm)],[4624]) ).
thf(4644,plain,
! [B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ in ) )
!= ( B @ ( B @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[3376,4630]) ).
thf(4645,plain,
! [B: $i,A: $i] :
( ( A @ powerset @ ( A @ in ) )
!= ( B @ ( B @ in ) ) ),
inference(simp,[status(thm)],[4644]) ).
thf(4655,plain,
! [B: $i,A: $i] :
( ( ( A @ powerset )
!= B )
| ( A != B ) ),
inference(simp,[status(thm)],[4645]) ).
thf(4664,plain,
! [A: $i] :
( ( A @ powerset )
!= A ),
inference(simp,[status(thm)],[4655]) ).
thf(30,axiom,
! [A: $i] :
( ( A @ empty )
=> ( A @ relation ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc1_relat_1) ).
thf(151,plain,
! [A: $i] :
( ( A @ empty )
=> ( A @ relation ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[30]) ).
thf(152,plain,
! [A: $i] :
( ( A @ relation )
| ~ ( A @ empty ) ),
inference(cnf,[status(esa)],[151]) ).
thf(47,plain,
! [B: $i,A: $i] :
( ( ( B @ ( sk2 @ apply ) )
= A )
| ( ( A @ ( sk1 @ apply ) )
!= B )
| ~ ( sk2 @ relation_dom @ ( B @ in ) )
| ~ ( sk1 @ relation_dom @ ( A @ in ) ) ),
inference(cnfConj,[status(thm)],[40]) ).
thf(56,plain,
! [B: $i,A: $i] :
( ~ ( sk2 @ relation_dom @ ( B @ in ) )
| ~ ( sk1 @ relation_dom @ ( A @ in ) )
| ( ( B @ ( sk2 @ apply ) )
= A )
| ( ( A @ ( sk1 @ apply ) )
!= B ) ),
inference(lifteq,[status(thm)],[47]) ).
thf(57,plain,
! [A: $i] :
( ~ ( sk2 @ relation_dom @ ( A @ ( sk1 @ apply ) @ in ) )
| ~ ( sk1 @ relation_dom @ ( A @ in ) )
| ( ( A @ ( sk1 @ apply ) @ ( sk2 @ apply ) )
= A ) ),
inference(simp,[status(thm)],[56]) ).
thf(9,axiom,
! [A: $i] :
( ~ ( A @ empty )
=> ? [B: $i] :
( ~ ( B @ empty )
& ( A @ powerset @ ( B @ element ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc1_subset_1) ).
thf(76,plain,
! [A: $i] :
( ~ ( A @ empty )
=> ? [B: $i] :
( ~ ( B @ empty )
& ( A @ powerset @ ( B @ element ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).
thf(77,plain,
! [A: $i] :
( ( ~ ( A @ sk5 @ empty )
| ( A @ empty ) )
& ( ( A @ powerset @ ( A @ sk5 @ element ) )
| ( A @ empty ) ) ),
inference(cnf,[status(esa)],[76]) ).
thf(78,plain,
! [A: $i] :
( ( A @ powerset @ ( A @ sk5 @ element ) )
| ( A @ empty ) ),
inference(cnfConj,[status(thm)],[77]) ).
thf(73,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ subset ) )
| ~ ( B @ powerset @ ( A @ element ) ) ),
inference(cnfConj,[status(thm)],[72]) ).
thf(1350,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ sk5 @ element ) )
!= ( C @ powerset @ ( B @ element ) ) )
| ( C @ ( B @ subset ) )
| ~ $true
| ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[78,73]) ).
thf(1351,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ sk5 @ element ) )
!= ( C @ powerset @ ( B @ element ) ) )
| ( C @ ( B @ subset ) )
| ( A @ empty ) ),
inference(simp,[status(thm)],[1350]) ).
thf(1352,plain,
! [A: $i] :
( ( A @ ( A @ sk5 @ subset ) )
| ( A @ empty ) ),
inference(pattern_uni,[status(thm)],[1351:[bind(A,$thf( D )),bind(B,$thf( D @ sk5 )),bind(C,$thf( D ))]]) ).
thf(1362,plain,
! [A: $i] :
( ( A @ ( A @ sk5 @ subset ) )
| ( A @ empty ) ),
inference(simp,[status(thm)],[1352]) ).
thf(3555,plain,
! [A: $i] :
( ( ( sk1 @ relation_dom @ empty )
!= ( A @ empty ) )
| ~ $true
| ( A = empty_set )
| ~ ( sk2 @ empty ) ),
inference(paramod_ordered,[status(thm)],[2201,85]) ).
thf(3556,plain,
! [A: $i] :
( ( ( sk1 @ relation_dom @ empty )
!= ( A @ empty ) )
| ( A = empty_set )
| ~ ( sk2 @ empty ) ),
inference(simp,[status(thm)],[3555]) ).
thf(3557,plain,
( ( ( sk1 @ relation_dom )
= empty_set )
| ~ ( sk2 @ empty ) ),
inference(pattern_uni,[status(thm)],[3556:[bind(A,$thf( sk1 @ relation_dom ))]]) ).
thf(199,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( C
= ( D @ ( A @ apply ) ) )
| ( D
!= ( C @ ( B @ apply ) ) )
| ~ ( A @ relation_rng @ ( C @ in ) )
| ( B
!= ( A @ function_inverse ) )
| ~ ( B @ function )
| ~ ( B @ relation )
| ~ ( A @ one_to_one )
| ~ ( A @ function )
| ~ ( A @ relation ) ),
inference(cnfConj,[status(thm)],[192]) ).
thf(215,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( A @ relation_rng @ ( C @ in ) )
| ~ ( B @ function )
| ~ ( B @ relation )
| ~ ( A @ one_to_one )
| ~ ( A @ function )
| ~ ( A @ relation )
| ( C
= ( D @ ( A @ apply ) ) )
| ( D
!= ( C @ ( B @ apply ) ) )
| ( B
!= ( A @ function_inverse ) ) ),
inference(lifteq,[status(thm)],[199]) ).
thf(216,plain,
! [B: $i,A: $i] :
( ~ ( A @ relation_rng @ ( B @ in ) )
| ~ ( A @ function_inverse @ function )
| ~ ( A @ function_inverse @ relation )
| ~ ( A @ one_to_one )
| ~ ( A @ function )
| ~ ( A @ relation )
| ( ( B @ ( A @ function_inverse @ apply ) @ ( A @ apply ) )
= B ) ),
inference(simp,[status(thm)],[215]) ).
thf(13,axiom,
! [A: $i] :
? [B: $i] : ( A @ ( B @ element ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',existence_m1_subset_1) ).
thf(90,plain,
! [A: $i] :
? [B: $i] : ( A @ ( B @ element ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[13]) ).
thf(91,plain,
! [A: $i] : ( A @ ( A @ sk7 @ element ) ),
inference(cnf,[status(esa)],[90]) ).
thf(2587,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ sk7 @ element ) )
!= ( C @ ( B @ element ) ) )
| ( C @ ( B @ in ) )
| ( C @ empty )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[91,133]) ).
thf(2588,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ sk7 @ element ) )
!= ( C @ ( B @ element ) ) )
| ( C @ ( B @ in ) )
| ( C @ empty ) ),
inference(simp,[status(thm)],[2587]) ).
thf(2589,plain,
! [A: $i] :
( ( A @ ( A @ sk7 @ in ) )
| ( A @ empty ) ),
inference(pattern_uni,[status(thm)],[2588:[bind(A,$thf( D )),bind(B,$thf( D @ sk7 )),bind(C,$thf( D ))]]) ).
thf(2600,plain,
! [A: $i] :
( ( A @ ( A @ sk7 @ in ) )
| ( A @ empty ) ),
inference(simp,[status(thm)],[2589]) ).
thf(3157,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ sk7 @ in ) )
!= ( C @ ( B @ in ) ) )
| ( C @ ( B @ element ) )
| ~ $true
| ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[2600,116]) ).
thf(3158,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ sk7 @ in ) )
!= ( C @ ( B @ in ) ) )
| ( C @ ( B @ element ) )
| ( A @ empty ) ),
inference(simp,[status(thm)],[3157]) ).
thf(3159,plain,
! [A: $i] :
( ( A @ ( A @ sk7 @ element ) )
| ( A @ empty ) ),
inference(pattern_uni,[status(thm)],[3158:[bind(A,$thf( D )),bind(B,$thf( D @ sk7 )),bind(C,$thf( D ))]]) ).
thf(3199,plain,
! [A: $i] :
( ( A @ ( A @ sk7 @ element ) )
| ( A @ empty ) ),
inference(simp,[status(thm)],[3159]) ).
thf(169,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( C @ in ) )
| ( C
!= ( D @ ( A @ apply ) ) )
| ~ ( A @ relation_dom @ ( D @ in ) )
| ( B
!= ( A @ relation_rng ) )
| ~ ( A @ function )
| ~ ( A @ relation ) ),
inference(cnfConj,[status(thm)],[163]) ).
thf(178,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( C @ in ) )
| ~ ( A @ relation_dom @ ( D @ in ) )
| ~ ( A @ function )
| ~ ( A @ relation )
| ( C
!= ( D @ ( A @ apply ) ) )
| ( B
!= ( A @ relation_rng ) ) ),
inference(lifteq,[status(thm)],[169]) ).
thf(179,plain,
! [B: $i,A: $i] :
( ( A @ relation_rng @ ( B @ ( A @ apply ) @ in ) )
| ~ ( A @ relation_dom @ ( B @ in ) )
| ~ ( A @ function )
| ~ ( A @ relation ) ),
inference(simp,[status(thm)],[178]) ).
thf(17877,plain,
( ( ( sk2 @ empty )
!= ( sk2 @ empty ) )
| ( sk4 != sk1 )
| ~ $true
| ( sk1 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[17600,14687]) ).
thf(17878,plain,
( ( ( sk2 @ empty )
!= ( sk2 @ empty ) )
| ( sk4 != sk1 )
| ( sk1 != empty_set ) ),
inference(simp,[status(thm)],[17877]) ).
thf(17879,plain,
( ( sk4 != sk1 )
| ( sk1 != empty_set ) ),
inference(pattern_uni,[status(thm)],[17878:[]]) ).
thf(124,plain,
sk10 @ function,
inference(cnfConj,[status(thm)],[122]) ).
thf(3286,plain,
! [A: $i] :
( ( ( sk10 @ function )
!= ( A @ function ) )
| ( A @ function_inverse @ relation )
| ~ $true
| ~ ( A @ relation ) ),
inference(paramod_ordered,[status(thm)],[124,138]) ).
thf(3287,plain,
! [A: $i] :
( ( ( sk10 @ function )
!= ( A @ function ) )
| ( A @ function_inverse @ relation )
| ~ ( A @ relation ) ),
inference(simp,[status(thm)],[3286]) ).
thf(3288,plain,
( ( sk10 @ function_inverse @ relation )
| ~ ( sk10 @ relation ) ),
inference(pattern_uni,[status(thm)],[3287:[bind(A,$thf( sk10 ))]]) ).
thf(123,plain,
sk10 @ relation,
inference(cnfConj,[status(thm)],[122]) ).
thf(9810,plain,
( ( sk10 @ function_inverse @ relation )
| ~ $true ),
inference(rewrite,[status(thm)],[3288,123]) ).
thf(9811,plain,
sk10 @ function_inverse @ relation,
inference(simp,[status(thm)],[9810]) ).
thf(14471,plain,
! [A: $i] :
( ( ( sk1 @ empty )
!= ( A @ empty ) )
| ~ $true
| ( A = empty_set )
| ( sk2 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[13760,85]) ).
thf(14472,plain,
! [A: $i] :
( ( ( sk1 @ empty )
!= ( A @ empty ) )
| ( A = empty_set )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[14471]) ).
thf(14473,plain,
( ( sk1 = empty_set )
| ( sk2 != empty_set ) ),
inference(pattern_uni,[status(thm)],[14472:[bind(A,$thf( sk1 ))]]) ).
thf(15092,plain,
! [A: $i] :
( ( A != sk2 )
| ( sk1 = empty_set )
| ( empty_set != empty_set )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[85,14473]) ).
thf(15093,plain,
! [A: $i] :
( ( A != sk2 )
| ( sk1 = empty_set )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[15092]) ).
thf(15094,plain,
( ( sk1 = empty_set )
| ~ ( sk2 @ empty ) ),
inference(pattern_uni,[status(thm)],[15093:[bind(A,$thf( sk2 ))]]) ).
thf(20653,plain,
( ( sk1 != sk1 )
| ( sk13 != sk2 )
| ( empty_set != empty_set )
| ~ ( sk2 @ empty ) ),
inference(paramod_ordered,[status(thm)],[15094,17976]) ).
thf(20654,plain,
( ( sk1 != sk1 )
| ( sk13 != sk2 )
| ~ ( sk2 @ empty ) ),
inference(simp,[status(thm)],[20653]) ).
thf(20655,plain,
( ( sk13 != sk2 )
| ~ ( sk2 @ empty ) ),
inference(pattern_uni,[status(thm)],[20654:[]]) ).
thf(3921,plain,
! [A: $i] :
( ( ( sk1 @ relation_dom @ empty )
!= ( A @ empty ) )
| ( A @ function )
| ~ $true
| ( sk2 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[2280,135]) ).
thf(3922,plain,
! [A: $i] :
( ( ( sk1 @ relation_dom @ empty )
!= ( A @ empty ) )
| ( A @ function )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[3921]) ).
thf(3923,plain,
( ( sk1 @ relation_dom @ function )
| ( sk2 != empty_set ) ),
inference(pattern_uni,[status(thm)],[3922:[bind(A,$thf( sk1 @ relation_dom ))]]) ).
thf(17860,plain,
! [A: $i] :
( ( ( sk2 @ empty )
!= ( A @ empty ) )
| ~ $true
| ( A = empty_set )
| ( sk1 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[17600,85]) ).
thf(17861,plain,
! [A: $i] :
( ( ( sk2 @ empty )
!= ( A @ empty ) )
| ( A = empty_set )
| ( sk1 != empty_set ) ),
inference(simp,[status(thm)],[17860]) ).
thf(17862,plain,
( ( sk2 = empty_set )
| ( sk1 != empty_set ) ),
inference(pattern_uni,[status(thm)],[17861:[bind(A,$thf( sk2 ))]]) ).
thf(196,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( A @ relation_dom @ ( D @ in ) )
| ( D
!= ( C @ ( B @ apply ) ) )
| ~ ( A @ relation_rng @ ( C @ in ) )
| ( B
!= ( A @ function_inverse ) )
| ~ ( B @ function )
| ~ ( B @ relation )
| ~ ( A @ one_to_one )
| ~ ( A @ function )
| ~ ( A @ relation ) ),
inference(cnfConj,[status(thm)],[192]) ).
thf(205,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( A @ relation_dom @ ( D @ in ) )
| ~ ( A @ relation_rng @ ( C @ in ) )
| ~ ( B @ function )
| ~ ( B @ relation )
| ~ ( A @ one_to_one )
| ~ ( A @ function )
| ~ ( A @ relation )
| ( D
!= ( C @ ( B @ apply ) ) )
| ( B
!= ( A @ function_inverse ) ) ),
inference(lifteq,[status(thm)],[196]) ).
thf(206,plain,
! [B: $i,A: $i] :
( ( A @ relation_dom @ ( B @ ( A @ function_inverse @ apply ) @ in ) )
| ~ ( A @ relation_rng @ ( B @ in ) )
| ~ ( A @ function_inverse @ function )
| ~ ( A @ function_inverse @ relation )
| ~ ( A @ one_to_one )
| ~ ( A @ function )
| ~ ( A @ relation ) ),
inference(simp,[status(thm)],[205]) ).
thf(229,plain,
! [B: $i,A: $i] :
( ( ( A @ ( sk2 @ apply ) @ ( sk1 @ apply ) )
!= ( B @ ( sk2 @ apply ) ) )
| ~ ( sk2 @ relation_dom @ ( B @ in ) )
| ~ ( sk1 @ relation_dom @ ( B @ ( sk2 @ apply ) @ in ) )
| ( ( A @ ( sk1 @ apply ) )
= B )
| ~ ( sk2 @ relation_dom @ ( A @ in ) )
| ~ ( sk1 @ relation_dom @ ( A @ ( sk2 @ apply ) @ in ) ) ),
inference(paramod_ordered,[status(thm)],[53,53]) ).
thf(231,plain,
! [B: $i,A: $i] :
( ( ( A @ ( sk2 @ apply ) )
!= B )
| ( sk2 != sk1 )
| ~ ( sk2 @ relation_dom @ ( B @ in ) )
| ~ ( sk1 @ relation_dom @ ( B @ ( sk2 @ apply ) @ in ) )
| ~ ( sk2 @ relation_dom @ ( A @ in ) )
| ~ ( sk1 @ relation_dom @ ( A @ ( sk2 @ apply ) @ in ) )
| ( ( A @ ( sk1 @ apply ) )
= B ) ),
inference(simp,[status(thm)],[229]) ).
thf(233,plain,
! [A: $i] :
( ( sk2 != sk1 )
| ~ ( sk2 @ relation_dom @ ( A @ ( sk2 @ apply ) @ in ) )
| ~ ( sk1 @ relation_dom @ ( A @ ( sk2 @ apply ) @ ( sk2 @ apply ) @ in ) )
| ~ ( sk2 @ relation_dom @ ( A @ in ) )
| ~ ( sk1 @ relation_dom @ ( A @ ( sk2 @ apply ) @ in ) )
| ( ( A @ ( sk2 @ apply ) )
= ( A @ ( sk1 @ apply ) ) ) ),
inference(simp,[status(thm)],[231]) ).
thf(1192,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ sk7 @ element ) )
!= ( C @ powerset @ ( B @ element ) ) )
| ( C @ ( B @ subset ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[91,73]) ).
thf(1193,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ sk7 @ element ) )
!= ( C @ powerset @ ( B @ element ) ) )
| ( C @ ( B @ subset ) ) ),
inference(simp,[status(thm)],[1192]) ).
thf(1194,plain,
! [A: $i] : ( A @ ( A @ powerset @ sk7 @ subset ) ),
inference(pattern_uni,[status(thm)],[1193:[bind(A,$thf( E @ powerset )),bind(B,$thf( E @ powerset @ sk7 )),bind(C,$thf( E ))]]) ).
thf(1199,plain,
! [A: $i] : ( A @ ( A @ powerset @ sk7 @ subset ) ),
inference(simp,[status(thm)],[1194]) ).
thf(37,axiom,
( ( empty_set @ relation_empty_yielding )
& ( empty_set @ relation )
& ( empty_set @ empty ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc12_relat_1) ).
thf(220,plain,
( ( empty_set @ relation_empty_yielding )
& ( empty_set @ relation )
& ( empty_set @ empty ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[37]) ).
thf(21,axiom,
? [A: $i] :
( ( A @ relation )
& ( A @ empty ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc1_relat_1) ).
thf(117,plain,
? [A: $i] :
( ( A @ relation )
& ( A @ empty ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[21]) ).
thf(3655,plain,
! [A: $i] :
( ( ( sk2 @ function )
!= ( A @ function ) )
| ( A @ function_inverse @ function )
| ~ $true
| ~ ( A @ relation ) ),
inference(paramod_ordered,[status(thm)],[42,139]) ).
thf(3656,plain,
! [A: $i] :
( ( ( sk2 @ function )
!= ( A @ function ) )
| ( A @ function_inverse @ function )
| ~ ( A @ relation ) ),
inference(simp,[status(thm)],[3655]) ).
thf(3657,plain,
( ( sk2 @ function_inverse @ function )
| ~ ( sk2 @ relation ) ),
inference(pattern_uni,[status(thm)],[3656:[bind(A,$thf( sk2 ))]]) ).
thf(10138,plain,
( ( sk2 @ function_inverse @ function )
| ~ $true ),
inference(rewrite,[status(thm)],[3657,43]) ).
thf(10139,plain,
sk2 @ function_inverse @ function,
inference(simp,[status(thm)],[10138]) ).
thf(2429,plain,
( ( ( sk1 @ relation_rng )
!= ( empty_set @ relation_rng ) )
| ( sk2 @ relation_dom @ relation ) ),
inference(paramod_ordered,[status(thm)],[54,2419]) ).
thf(2441,plain,
( ( sk1 != empty_set )
| ( sk2 @ relation_dom @ relation ) ),
inference(simp,[status(thm)],[2429]) ).
thf(9860,plain,
! [A: $i] :
( ( A
!= ( sk10 @ function_inverse ) )
| ( sk2 @ relation_dom @ relation )
| ( sk1 @ relation_dom @ ( sk1 @ ( A @ sk18 ) @ in ) )
| ( A @ ( sk1 @ sk15 ) ) ),
inference(paramod_ordered,[status(thm)],[7412,9811]) ).
thf(9861,plain,
( ( sk2 @ relation_dom @ relation )
| ( sk1 @ relation_dom @ ( sk1 @ ( sk10 @ function_inverse @ sk18 ) @ in ) )
| ( sk10 @ function_inverse @ ( sk1 @ sk15 ) ) ),
inference(pattern_uni,[status(thm)],[9860:[bind(A,$thf( sk10 @ function_inverse ))]]) ).
thf(33,axiom,
! [A: $i,B: $i,C: $i] :
( ( ( C @ powerset @ ( B @ element ) )
& ( B @ ( A @ in ) ) )
=> ( C @ ( A @ element ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t4_subset) ).
thf(159,plain,
! [A: $i,B: $i,C: $i] :
( ( ( C @ powerset @ ( B @ element ) )
& ( B @ ( A @ in ) ) )
=> ( C @ ( A @ element ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[33]) ).
thf(160,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ element ) )
| ~ ( C @ powerset @ ( B @ element ) )
| ~ ( B @ ( A @ in ) ) ),
inference(cnf,[status(esa)],[159]) ).
thf(4089,plain,
! [A: $i] :
( ( ( sk10 @ relation )
!= ( A @ relation ) )
| ~ ( A @ relation_dom @ empty )
| ~ $true
| ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[123,141]) ).
thf(4090,plain,
! [A: $i] :
( ( ( sk10 @ relation )
!= ( A @ relation ) )
| ~ ( A @ relation_dom @ empty )
| ( A @ empty ) ),
inference(simp,[status(thm)],[4089]) ).
thf(4091,plain,
( ~ ( sk10 @ relation_dom @ empty )
| ( sk10 @ empty ) ),
inference(pattern_uni,[status(thm)],[4090:[bind(A,$thf( sk10 ))]]) ).
thf(14,axiom,
! [A: $i] :
( ( ( A @ function )
& ( A @ empty )
& ( A @ relation ) )
=> ( ( A @ one_to_one )
& ( A @ function )
& ( A @ relation ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc2_funct_1) ).
thf(92,plain,
! [A: $i] :
( ( ( A @ function )
& ( A @ empty )
& ( A @ relation ) )
=> ( ( A @ one_to_one )
& ( A @ function )
& ( A @ relation ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[14]) ).
thf(15,axiom,
( ( empty_set @ relation )
& ( empty_set @ empty ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc4_relat_1) ).
thf(97,plain,
( ( empty_set @ relation )
& ( empty_set @ empty ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[15]) ).
thf(3646,plain,
! [A: $i] :
( ( ( sk1 @ relation )
!= ( A @ relation ) )
| ( A @ function_inverse @ function )
| ~ ( A @ function )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[41,139]) ).
thf(3647,plain,
! [A: $i] :
( ( ( sk1 @ relation )
!= ( A @ relation ) )
| ( A @ function_inverse @ function )
| ~ ( A @ function ) ),
inference(simp,[status(thm)],[3646]) ).
thf(3648,plain,
( ( sk1 @ function_inverse @ function )
| ~ ( sk1 @ function ) ),
inference(pattern_uni,[status(thm)],[3647:[bind(A,$thf( sk1 ))]]) ).
thf(10066,plain,
( ( sk1 @ function_inverse @ function )
| ~ $true ),
inference(rewrite,[status(thm)],[3648,49]) ).
thf(10067,plain,
sk1 @ function_inverse @ function,
inference(simp,[status(thm)],[10066]) ).
thf(3468,plain,
( ( ( sk2 @ relation_dom @ empty )
!= ( sk13 @ empty ) )
| ~ $true
| ~ ( sk1 @ empty ) ),
inference(paramod_ordered,[status(thm)],[2185,149]) ).
thf(3469,plain,
( ( ( sk2 @ relation_dom @ empty )
!= ( sk13 @ empty ) )
| ~ ( sk1 @ empty ) ),
inference(simp,[status(thm)],[3468]) ).
thf(3535,plain,
( ( ( sk2 @ relation_dom )
!= sk13 )
| ~ ( sk1 @ empty ) ),
inference(simp,[status(thm)],[3469]) ).
thf(7715,plain,
! [A: $i] :
( ( A
!= ( empty_set @ relation_rng ) )
| ( sk2 @ relation_dom @ empty )
| ( sk1 @ relation_dom @ ( sk1 @ ( A @ sk18 ) @ in ) )
| ( A @ ( sk1 @ sk15 ) ) ),
inference(paramod_ordered,[status(thm)],[7412,2318]) ).
thf(7716,plain,
( ( sk2 @ relation_dom @ empty )
| ( sk1 @ relation_dom @ ( sk1 @ ( empty_set @ relation_rng @ sk18 ) @ in ) )
| ( empty_set @ relation_rng @ ( sk1 @ sk15 ) ) ),
inference(pattern_uni,[status(thm)],[7715:[bind(A,$thf( empty_set @ relation_rng ))]]) ).
thf(12685,plain,
( ( sk2 @ relation_dom @ empty )
| ( sk1 @ relation_dom @ ( sk1 @ ( empty_set @ sk18 ) @ in ) )
| ( empty_set @ ( sk1 @ sk15 ) ) ),
inference(rewrite,[status(thm)],[7716,2234]) ).
thf(12707,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ relation_dom @ ( sk1 @ ( empty_set @ sk18 ) @ in ) )
!= ( B @ ( A @ in ) ) )
| ( B @ ( A @ element ) )
| ~ $true
| ( sk2 @ relation_dom @ empty )
| ( empty_set @ ( sk1 @ sk15 ) ) ),
inference(paramod_ordered,[status(thm)],[12685,116]) ).
thf(12708,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ relation_dom @ ( sk1 @ ( empty_set @ sk18 ) @ in ) )
!= ( B @ ( A @ in ) ) )
| ( B @ ( A @ element ) )
| ( sk2 @ relation_dom @ empty )
| ( empty_set @ ( sk1 @ sk15 ) ) ),
inference(simp,[status(thm)],[12707]) ).
thf(12709,plain,
( ( sk1 @ relation_dom @ ( sk1 @ ( empty_set @ sk18 ) @ element ) )
| ( sk2 @ relation_dom @ empty )
| ( empty_set @ ( sk1 @ sk15 ) ) ),
inference(pattern_uni,[status(thm)],[12708:[bind(A,$thf( sk1 @ ( empty_set @ sk18 ) )),bind(B,$thf( sk1 @ relation_dom ))]]) ).
thf(17636,plain,
( ( ( sk2 @ empty )
!= ( sk2 @ empty ) )
| ( sk13 != sk1 )
| ~ $true
| ~ ( sk1 @ empty ) ),
inference(paramod_ordered,[status(thm)],[17564,14662]) ).
thf(17637,plain,
( ( ( sk2 @ empty )
!= ( sk2 @ empty ) )
| ( sk13 != sk1 )
| ~ ( sk1 @ empty ) ),
inference(simp,[status(thm)],[17636]) ).
thf(17638,plain,
( ( sk13 != sk1 )
| ~ ( sk1 @ empty ) ),
inference(pattern_uni,[status(thm)],[17637:[]]) ).
thf(221,plain,
( ( empty_set @ relation_empty_yielding )
& ( empty_set @ relation )
& ( empty_set @ empty ) ),
inference(cnf,[status(esa)],[220]) ).
thf(224,plain,
empty_set @ relation_empty_yielding,
inference(cnfConj,[status(thm)],[221]) ).
thf(3961,plain,
( ( ( sk1 @ relation_dom @ empty )
!= ( sk4 @ empty ) )
| ~ $true
| ( sk2 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[2280,68]) ).
thf(3962,plain,
( ( ( sk1 @ relation_dom @ empty )
!= ( sk4 @ empty ) )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[3961]) ).
thf(3968,plain,
( ( ( sk1 @ relation_dom )
!= sk4 )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[3962]) ).
thf(7460,plain,
! [B: $i,A: $i] :
( ( A
!= ( B @ powerset ) )
| ( ( sk2 @ relation_dom )
!= B )
| ( sk1 @ relation_dom @ ( sk1 @ ( A @ sk18 ) @ in ) )
| ( A @ ( sk1 @ sk15 ) ) ),
inference(paramod_ordered,[status(thm)],[7412,4664]) ).
thf(7461,plain,
! [A: $i] :
( ( ( sk2 @ relation_dom )
!= A )
| ( sk1 @ relation_dom @ ( sk1 @ ( A @ powerset @ sk18 ) @ in ) )
| ( A @ powerset @ ( sk1 @ sk15 ) ) ),
inference(pattern_uni,[status(thm)],[7460:[bind(A,$thf( C @ powerset )),bind(B,$thf( C ))]]) ).
thf(8068,plain,
( ( sk1 @ relation_dom @ ( sk1 @ ( sk2 @ relation_dom @ powerset @ sk18 ) @ in ) )
| ( sk2 @ relation_dom @ powerset @ ( sk1 @ sk15 ) ) ),
inference(simp,[status(thm)],[7461]) ).
thf(17782,plain,
( ( ( sk4 @ empty )
!= ( sk2 @ empty ) )
| ~ $true
| ~ ( sk1 @ empty ) ),
inference(paramod_ordered,[status(thm)],[17564,68]) ).
thf(17783,plain,
( ( ( sk4 @ empty )
!= ( sk2 @ empty ) )
| ~ ( sk1 @ empty ) ),
inference(simp,[status(thm)],[17782]) ).
thf(17797,plain,
( ( sk4 != sk2 )
| ~ ( sk1 @ empty ) ),
inference(simp,[status(thm)],[17783]) ).
thf(18400,plain,
( ( ( sk1 @ empty )
!= ( sk1 @ empty ) )
| ( sk4 != sk2 )
| ~ $true
| ( sk2 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[13760,17797]) ).
thf(18401,plain,
( ( ( sk1 @ empty )
!= ( sk1 @ empty ) )
| ( sk4 != sk2 )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[18400]) ).
thf(18402,plain,
( ( sk4 != sk2 )
| ( sk2 != empty_set ) ),
inference(pattern_uni,[status(thm)],[18401:[]]) ).
thf(3567,plain,
( ( ( sk1 @ relation_dom @ empty )
!= ( sk13 @ empty ) )
| ~ $true
| ~ ( sk2 @ empty ) ),
inference(paramod_ordered,[status(thm)],[2201,149]) ).
thf(3568,plain,
( ( ( sk1 @ relation_dom @ empty )
!= ( sk13 @ empty ) )
| ~ ( sk2 @ empty ) ),
inference(simp,[status(thm)],[3567]) ).
thf(3632,plain,
( ( ( sk1 @ relation_dom )
!= sk13 )
| ~ ( sk2 @ empty ) ),
inference(simp,[status(thm)],[3568]) ).
thf(2578,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ sk5 @ element ) )
!= ( C @ ( B @ element ) ) )
| ( C @ ( B @ in ) )
| ( C @ empty )
| ~ $true
| ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[78,133]) ).
thf(2579,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ sk5 @ element ) )
!= ( C @ ( B @ element ) ) )
| ( C @ ( B @ in ) )
| ( C @ empty )
| ( A @ empty ) ),
inference(simp,[status(thm)],[2578]) ).
thf(2580,plain,
! [A: $i] :
( ( A @ powerset @ ( A @ sk5 @ in ) )
| ( A @ powerset @ empty )
| ( A @ empty ) ),
inference(pattern_uni,[status(thm)],[2579:[bind(A,$thf( E )),bind(B,$thf( E @ sk5 )),bind(C,$thf( E @ powerset ))]]) ).
thf(2598,plain,
! [A: $i] :
( ( A @ powerset @ ( A @ sk5 @ in ) )
| ( A @ powerset @ empty )
| ( A @ empty ) ),
inference(simp,[status(thm)],[2580]) ).
thf(4314,plain,
! [A: $i] :
( ( A @ powerset @ ( A @ sk5 @ in ) )
| $false
| ( A @ empty ) ),
inference(rewrite,[status(thm)],[2598,82]) ).
thf(4315,plain,
! [A: $i] :
( ( A @ powerset @ ( A @ sk5 @ in ) )
| ( A @ empty ) ),
inference(simp,[status(thm)],[4314]) ).
thf(1378,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ sk6 @ element ) )
!= ( C @ powerset @ ( B @ element ) ) )
| ( C @ ( B @ subset ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[88,73]) ).
thf(1379,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ sk6 @ element ) )
!= ( C @ powerset @ ( B @ element ) ) )
| ( C @ ( B @ subset ) ) ),
inference(simp,[status(thm)],[1378]) ).
thf(1380,plain,
! [A: $i] : ( A @ ( A @ sk6 @ subset ) ),
inference(pattern_uni,[status(thm)],[1379:[bind(A,$thf( D )),bind(B,$thf( D @ sk6 )),bind(C,$thf( D ))]]) ).
thf(1389,plain,
! [A: $i] : ( A @ ( A @ sk6 @ subset ) ),
inference(simp,[status(thm)],[1380]) ).
thf(2053,plain,
! [A: $i] : ( A @ ( empty_set @ subset ) ),
inference(rewrite,[status(thm)],[1389,1964]) ).
thf(102,plain,
( ( sk8 @ relation_empty_yielding )
& ( sk8 @ relation ) ),
inference(cnf,[status(esa)],[101]) ).
thf(103,plain,
sk8 @ relation,
inference(cnfConj,[status(thm)],[102]) ).
thf(3292,plain,
! [A: $i] :
( ( ( sk8 @ relation )
!= ( A @ relation ) )
| ( A @ function_inverse @ relation )
| ~ ( A @ function )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[103,138]) ).
thf(3293,plain,
! [A: $i] :
( ( ( sk8 @ relation )
!= ( A @ relation ) )
| ( A @ function_inverse @ relation )
| ~ ( A @ function ) ),
inference(simp,[status(thm)],[3292]) ).
thf(3294,plain,
( ( sk8 @ function_inverse @ relation )
| ~ ( sk8 @ function ) ),
inference(pattern_uni,[status(thm)],[3293:[bind(A,$thf( sk8 ))]]) ).
thf(198,plain,
! [B: $i,A: $i] :
( ( B
= ( A @ function_inverse ) )
| ~ ( B @ ( A @ sk19 ) )
| ( A @ relation_rng @ ( A @ ( B @ sk20 ) @ in ) )
| ( ( B @ relation_dom )
!= ( A @ relation_rng ) )
| ~ ( B @ function )
| ~ ( B @ relation )
| ~ ( A @ one_to_one )
| ~ ( A @ function )
| ~ ( A @ relation ) ),
inference(cnfConj,[status(thm)],[192]) ).
thf(212,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ sk19 ) )
| ( A @ relation_rng @ ( A @ ( B @ sk20 ) @ in ) )
| ~ ( B @ function )
| ~ ( B @ relation )
| ~ ( A @ one_to_one )
| ~ ( A @ function )
| ~ ( A @ relation )
| ( B
= ( A @ function_inverse ) )
| ( ( B @ relation_dom )
!= ( A @ relation_rng ) ) ),
inference(lifteq,[status(thm)],[198]) ).
thf(93,plain,
! [A: $i] :
( ( ( A @ one_to_one )
| ~ ( A @ function )
| ~ ( A @ empty )
| ~ ( A @ relation ) )
& ( ( A @ function )
| ~ ( A @ function )
| ~ ( A @ empty )
| ~ ( A @ relation ) )
& ( ( A @ relation )
| ~ ( A @ function )
| ~ ( A @ empty )
| ~ ( A @ relation ) ) ),
inference(cnf,[status(esa)],[92]) ).
thf(96,plain,
! [A: $i] :
( ( A @ one_to_one )
| ~ ( A @ function )
| ~ ( A @ empty )
| ~ ( A @ relation ) ),
inference(cnfConj,[status(thm)],[93]) ).
thf(18,axiom,
! [A: $i,B: $i,C: $i] :
~ ( ( C @ empty )
& ( C @ powerset @ ( B @ element ) )
& ( B @ ( A @ in ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_subset) ).
thf(109,plain,
! [A: $i,B: $i,C: $i] :
~ ( ( C @ empty )
& ( C @ powerset @ ( B @ element ) )
& ( B @ ( A @ in ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[18]) ).
thf(248,plain,
( ( ( sk2 @ relation_rng )
!= ( sk1 @ relation_rng ) )
| ( ( sk2 @ relation_dom )
= ( sk1 @ relation_dom ) ) ),
inference(paramod_ordered,[status(thm)],[54,51]) ).
thf(250,plain,
( ( sk2 != sk1 )
| ( ( sk2 @ relation_dom )
= ( sk1 @ relation_dom ) ) ),
inference(simp,[status(thm)],[248]) ).
thf(252,plain,
! [A: $i] :
( ( ( sk2 @ relation_dom )
!= ( sk1 @ relation_dom ) )
| ~ ( sk2 @ relation_dom @ ( A @ in ) )
| ~ ( sk1 @ relation_dom @ ( A @ ( sk2 @ apply ) @ in ) )
| ( ( A @ ( sk2 @ apply ) @ ( sk1 @ apply ) )
= A )
| ( sk2 != sk1 ) ),
inference(paramod_ordered,[status(thm)],[250,53]) ).
thf(255,plain,
! [A: $i] :
( ( sk2 != sk1 )
| ~ ( sk2 @ relation_dom @ ( A @ in ) )
| ~ ( sk1 @ relation_dom @ ( A @ ( sk2 @ apply ) @ in ) )
| ( sk2 != sk1 )
| ( ( A @ ( sk2 @ apply ) @ ( sk1 @ apply ) )
= A ) ),
inference(simp,[status(thm)],[252]) ).
thf(256,plain,
! [A: $i] :
( ~ ( sk2 @ relation_dom @ ( A @ in ) )
| ~ ( sk1 @ relation_dom @ ( A @ ( sk2 @ apply ) @ in ) )
| ( sk2 != sk1 )
| ( ( A @ ( sk2 @ apply ) @ ( sk1 @ apply ) )
= A ) ),
inference(simp,[status(thm)],[255]) ).
thf(3658,plain,
! [A: $i] :
( ( ( sk24 @ function )
!= ( A @ function ) )
| ( A @ function_inverse @ function )
| ~ $true
| ~ ( A @ relation ) ),
inference(paramod_ordered,[status(thm)],[228,139]) ).
thf(3659,plain,
! [A: $i] :
( ( ( sk24 @ function )
!= ( A @ function ) )
| ( A @ function_inverse @ function )
| ~ ( A @ relation ) ),
inference(simp,[status(thm)],[3658]) ).
thf(3660,plain,
( ( sk24 @ function_inverse @ function )
| ~ ( sk24 @ relation ) ),
inference(pattern_uni,[status(thm)],[3659:[bind(A,$thf( sk24 ))]]) ).
thf(11800,plain,
( ( sk24 @ function_inverse @ function )
| ~ $true ),
inference(rewrite,[status(thm)],[3660,227]) ).
thf(11801,plain,
sk24 @ function_inverse @ function,
inference(simp,[status(thm)],[11800]) ).
thf(3266,plain,
! [A: $i] :
( ( ( sk2 @ function )
!= ( A @ function ) )
| ( A @ function_inverse @ relation )
| ~ $true
| ~ ( A @ relation ) ),
inference(paramod_ordered,[status(thm)],[42,138]) ).
thf(3267,plain,
! [A: $i] :
( ( ( sk2 @ function )
!= ( A @ function ) )
| ( A @ function_inverse @ relation )
| ~ ( A @ relation ) ),
inference(simp,[status(thm)],[3266]) ).
thf(3268,plain,
( ( sk2 @ function_inverse @ relation )
| ~ ( sk2 @ relation ) ),
inference(pattern_uni,[status(thm)],[3267:[bind(A,$thf( sk2 ))]]) ).
thf(5575,plain,
( ( sk2 @ function_inverse @ relation )
| ~ $true ),
inference(rewrite,[status(thm)],[3268,43]) ).
thf(5576,plain,
sk2 @ function_inverse @ relation,
inference(simp,[status(thm)],[5575]) ).
thf(13803,plain,
( ( ( sk1 @ relation_dom @ empty )
!= ( sk1 @ relation_dom @ empty ) )
| ~ $true
| ( sk1 @ empty )
| ~ ( sk2 @ empty ) ),
inference(paramod_ordered,[status(thm)],[2201,4065]) ).
thf(13804,plain,
( ( ( sk1 @ relation_dom @ empty )
!= ( sk1 @ relation_dom @ empty ) )
| ( sk1 @ empty )
| ~ ( sk2 @ empty ) ),
inference(simp,[status(thm)],[13803]) ).
thf(13805,plain,
( ( sk1 @ empty )
| ~ ( sk2 @ empty ) ),
inference(pattern_uni,[status(thm)],[13804:[]]) ).
thf(4098,plain,
! [A: $i] :
( ( ( sk13 @ relation )
!= ( A @ relation ) )
| ~ ( A @ relation_dom @ empty )
| ~ $true
| ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[150,141]) ).
thf(4099,plain,
! [A: $i] :
( ( ( sk13 @ relation )
!= ( A @ relation ) )
| ~ ( A @ relation_dom @ empty )
| ( A @ empty ) ),
inference(simp,[status(thm)],[4098]) ).
thf(4100,plain,
( ~ ( sk13 @ relation_dom @ empty )
| ( sk13 @ empty ) ),
inference(pattern_uni,[status(thm)],[4099:[bind(A,$thf( sk13 ))]]) ).
thf(28370,plain,
( ~ ( sk13 @ relation_dom @ empty )
| $false ),
inference(rewrite,[status(thm)],[4100,149]) ).
thf(28371,plain,
~ ( sk13 @ relation_dom @ empty ),
inference(simp,[status(thm)],[28370]) ).
thf(28372,plain,
( ( ( sk13 @ relation_dom @ empty )
!= ( empty_set @ empty ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[69,28371]) ).
thf(28373,plain,
( ( sk13 @ relation_dom @ empty )
!= ( empty_set @ empty ) ),
inference(simp,[status(thm)],[28372]) ).
thf(28450,plain,
( ( sk13 @ relation_dom )
!= empty_set ),
inference(simp,[status(thm)],[28373]) ).
thf(170,plain,
! [B: $i,A: $i] :
( ( B
= ( A @ relation_rng ) )
| ~ ( B @ ( A @ sk15 ) )
| ( B @ ( A @ ( B @ sk16 ) @ in ) )
| ~ ( A @ function )
| ~ ( A @ relation ) ),
inference(cnfConj,[status(thm)],[163]) ).
thf(172,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ sk15 ) )
| ( B @ ( A @ ( B @ sk16 ) @ in ) )
| ~ ( A @ function )
| ~ ( A @ relation )
| ( B
= ( A @ relation_rng ) ) ),
inference(lifteq,[status(thm)],[170]) ).
thf(173,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ sk15 ) )
| ( B @ ( A @ ( B @ sk16 ) @ in ) )
| ~ ( A @ function )
| ~ ( A @ relation )
| ( B
= ( A @ relation_rng ) ) ),
inference(simp,[status(thm)],[172]) ).
thf(3758,plain,
! [A: $i] :
( ( ( sk2 @ relation_dom @ empty )
!= ( A @ empty ) )
| ( A @ function )
| ~ $true
| ( sk1 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[2279,135]) ).
thf(3759,plain,
! [A: $i] :
( ( ( sk2 @ relation_dom @ empty )
!= ( A @ empty ) )
| ( A @ function )
| ( sk1 != empty_set ) ),
inference(simp,[status(thm)],[3758]) ).
thf(3760,plain,
( ( sk2 @ relation_dom @ function )
| ( sk1 != empty_set ) ),
inference(pattern_uni,[status(thm)],[3759:[bind(A,$thf( sk2 @ relation_dom ))]]) ).
thf(7718,plain,
! [A: $i] :
( ( A
!= ( empty_set @ relation_rng ) )
| ( ( sk2 @ relation_dom )
= empty_set )
| ( sk1 @ relation_dom @ ( sk1 @ ( A @ sk18 ) @ in ) )
| ( A @ ( sk1 @ sk15 ) ) ),
inference(paramod_ordered,[status(thm)],[7412,2234]) ).
thf(7719,plain,
( ( ( sk2 @ relation_dom )
= empty_set )
| ( sk1 @ relation_dom @ ( sk1 @ ( empty_set @ relation_rng @ sk18 ) @ in ) )
| ( empty_set @ relation_rng @ ( sk1 @ sk15 ) ) ),
inference(pattern_uni,[status(thm)],[7718:[bind(A,$thf( empty_set @ relation_rng ))]]) ).
thf(14708,plain,
( ( ( sk2 @ relation_dom )
= empty_set )
| ( sk1 @ relation_dom @ ( sk1 @ ( empty_set @ sk18 ) @ in ) )
| ( empty_set @ ( sk1 @ sk15 ) ) ),
inference(rewrite,[status(thm)],[7719,2234]) ).
thf(14755,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ relation_dom @ ( sk1 @ ( empty_set @ sk18 ) @ in ) )
!= ( B @ ( A @ in ) ) )
| ( B @ ( A @ element ) )
| ~ $true
| ( ( sk2 @ relation_dom )
= empty_set )
| ( empty_set @ ( sk1 @ sk15 ) ) ),
inference(paramod_ordered,[status(thm)],[14708,116]) ).
thf(14756,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ relation_dom @ ( sk1 @ ( empty_set @ sk18 ) @ in ) )
!= ( B @ ( A @ in ) ) )
| ( B @ ( A @ element ) )
| ( ( sk2 @ relation_dom )
= empty_set )
| ( empty_set @ ( sk1 @ sk15 ) ) ),
inference(simp,[status(thm)],[14755]) ).
thf(14757,plain,
( ( sk1 @ relation_dom @ ( sk1 @ ( empty_set @ sk18 ) @ element ) )
| ( ( sk2 @ relation_dom )
= empty_set )
| ( empty_set @ ( sk1 @ sk15 ) ) ),
inference(pattern_uni,[status(thm)],[14756:[bind(A,$thf( sk1 @ ( empty_set @ sk18 ) )),bind(B,$thf( sk1 @ relation_dom ))]]) ).
thf(4084,plain,
! [A: $i] :
( ( ( sk8 @ relation )
!= ( A @ relation ) )
| ~ ( A @ relation_dom @ empty )
| ~ $true
| ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[103,141]) ).
thf(4085,plain,
! [A: $i] :
( ( ( sk8 @ relation )
!= ( A @ relation ) )
| ~ ( A @ relation_dom @ empty )
| ( A @ empty ) ),
inference(simp,[status(thm)],[4084]) ).
thf(4086,plain,
( ~ ( sk8 @ relation_dom @ empty )
| ( sk8 @ empty ) ),
inference(pattern_uni,[status(thm)],[4085:[bind(A,$thf( sk8 ))]]) ).
thf(3797,plain,
( ( ( sk2 @ relation_dom @ empty )
!= ( sk4 @ empty ) )
| ~ $true
| ( sk1 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[2279,68]) ).
thf(3798,plain,
( ( ( sk2 @ relation_dom @ empty )
!= ( sk4 @ empty ) )
| ( sk1 != empty_set ) ),
inference(simp,[status(thm)],[3797]) ).
thf(3802,plain,
( ( ( sk2 @ relation_dom )
!= sk4 )
| ( sk1 != empty_set ) ),
inference(simp,[status(thm)],[3798]) ).
thf(8480,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ relation_dom @ ( sk1 @ ( sk2 @ relation_dom @ powerset @ sk18 ) @ in ) )
!= ( B @ ( A @ in ) ) )
| ( B @ ( A @ element ) )
| ~ $true
| ( sk2 @ relation_dom @ powerset @ ( sk1 @ sk15 ) ) ),
inference(paramod_ordered,[status(thm)],[8068,116]) ).
thf(8481,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ relation_dom @ ( sk1 @ ( sk2 @ relation_dom @ powerset @ sk18 ) @ in ) )
!= ( B @ ( A @ in ) ) )
| ( B @ ( A @ element ) )
| ( sk2 @ relation_dom @ powerset @ ( sk1 @ sk15 ) ) ),
inference(simp,[status(thm)],[8480]) ).
thf(8482,plain,
( ( sk1 @ relation_dom @ ( sk1 @ ( sk2 @ relation_dom @ powerset @ sk18 ) @ element ) )
| ( sk2 @ relation_dom @ powerset @ ( sk1 @ sk15 ) ) ),
inference(pattern_uni,[status(thm)],[8481:[bind(A,$thf( sk1 @ ( sk2 @ relation_dom @ powerset @ sk18 ) )),bind(B,$thf( sk1 @ relation_dom ))]]) ).
thf(3616,plain,
( ( ( sk1 @ relation_dom @ empty )
!= ( sk4 @ empty ) )
| ~ $true
| ~ ( sk2 @ empty ) ),
inference(paramod_ordered,[status(thm)],[2201,68]) ).
thf(3617,plain,
( ( ( sk1 @ relation_dom @ empty )
!= ( sk4 @ empty ) )
| ~ ( sk2 @ empty ) ),
inference(simp,[status(thm)],[3616]) ).
thf(3624,plain,
( ( ( sk1 @ relation_dom )
!= sk4 )
| ~ ( sk2 @ empty ) ),
inference(simp,[status(thm)],[3617]) ).
thf(4608,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ in ) )
!= ( B @ ( C @ in ) ) )
| ~ $true
| ~ ( C @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[3376,154]) ).
thf(4609,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ in ) )
!= ( B @ ( C @ in ) ) )
| ~ ( C @ ( B @ in ) ) ),
inference(simp,[status(thm)],[4608]) ).
thf(4610,plain,
! [A: $i] :
~ ( A @ ( A @ powerset @ in ) ),
inference(pattern_uni,[status(thm)],[4609:[bind(A,$thf( D )),bind(B,$thf( D @ powerset )),bind(C,$thf( D ))]]) ).
thf(4625,plain,
! [A: $i] :
~ ( A @ ( A @ powerset @ in ) ),
inference(simp,[status(thm)],[4610]) ).
thf(1129,plain,
! [A: $i] :
( ( ( A @ powerset @ empty )
!= ( empty_set @ empty ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[69,82]) ).
thf(1130,plain,
! [A: $i] :
( ( A @ powerset @ empty )
!= ( empty_set @ empty ) ),
inference(simp,[status(thm)],[1129]) ).
thf(1146,plain,
! [A: $i] :
( ( A @ powerset )
!= empty_set ),
inference(simp,[status(thm)],[1130]) ).
thf(3643,plain,
! [A: $i] :
( ( ( empty_set @ function )
!= ( A @ function ) )
| ( A @ function_inverse @ function )
| ~ $true
| ~ ( A @ relation ) ),
inference(paramod_ordered,[status(thm)],[2014,139]) ).
thf(3644,plain,
! [A: $i] :
( ( ( empty_set @ function )
!= ( A @ function ) )
| ( A @ function_inverse @ function )
| ~ ( A @ relation ) ),
inference(simp,[status(thm)],[3643]) ).
thf(3645,plain,
( ( empty_set @ function_inverse @ function )
| ~ ( empty_set @ relation ) ),
inference(pattern_uni,[status(thm)],[3644:[bind(A,$thf( empty_set ))]]) ).
thf(98,plain,
( ( empty_set @ relation )
& ( empty_set @ empty ) ),
inference(cnf,[status(esa)],[97]) ).
thf(100,plain,
empty_set @ relation,
inference(cnfConj,[status(thm)],[98]) ).
thf(11709,plain,
( ( empty_set @ function_inverse @ function )
| ~ $true ),
inference(rewrite,[status(thm)],[3645,100]) ).
thf(11710,plain,
empty_set @ function_inverse @ function,
inference(simp,[status(thm)],[11709]) ).
thf(7598,plain,
! [A: $i] :
( ( A
!= ( sk2 @ function_inverse ) )
| ( sk2 @ relation_dom @ relation )
| ( sk1 @ relation_dom @ ( sk1 @ ( A @ sk18 ) @ in ) )
| ( A @ ( sk1 @ sk15 ) ) ),
inference(paramod_ordered,[status(thm)],[7412,5576]) ).
thf(7599,plain,
( ( sk2 @ relation_dom @ relation )
| ( sk1 @ relation_dom @ ( sk1 @ ( sk2 @ function_inverse @ sk18 ) @ in ) )
| ( sk2 @ function_inverse @ ( sk1 @ sk15 ) ) ),
inference(pattern_uni,[status(thm)],[7598:[bind(A,$thf( sk2 @ function_inverse ))]]) ).
thf(1648,plain,
! [A: $i] :
( ( A != sk10 )
| ( empty_set @ one_to_one )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[85,125]) ).
thf(1649,plain,
( ( empty_set @ one_to_one )
| ~ ( sk10 @ empty ) ),
inference(pattern_uni,[status(thm)],[1648:[bind(A,$thf( sk10 ))]]) ).
thf(2509,plain,
( ( ( sk10 @ empty )
!= ( empty_set @ empty ) )
| ( empty_set @ one_to_one )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[69,1649]) ).
thf(2510,plain,
( ( ( sk10 @ empty )
!= ( empty_set @ empty ) )
| ( empty_set @ one_to_one ) ),
inference(simp,[status(thm)],[2509]) ).
thf(2524,plain,
( ( sk10 != empty_set )
| ( empty_set @ one_to_one ) ),
inference(simp,[status(thm)],[2510]) ).
thf(3753,plain,
( ( ( sk2 @ relation_dom @ empty )
!= ( sk13 @ empty ) )
| ~ $true
| ( sk1 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[2279,149]) ).
thf(3754,plain,
( ( ( sk2 @ relation_dom @ empty )
!= ( sk13 @ empty ) )
| ( sk1 != empty_set ) ),
inference(simp,[status(thm)],[3753]) ).
thf(3811,plain,
( ( ( sk2 @ relation_dom )
!= sk13 )
| ( sk1 != empty_set ) ),
inference(simp,[status(thm)],[3754]) ).
thf(14479,plain,
( ( ( sk1 @ empty )
!= ( sk1 @ empty ) )
| ( ( sk2 @ relation_dom )
!= sk13 )
| ~ $true
| ( sk2 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[13760,3535]) ).
thf(14480,plain,
( ( ( sk1 @ empty )
!= ( sk1 @ empty ) )
| ( ( sk2 @ relation_dom )
!= sk13 )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[14479]) ).
thf(14481,plain,
( ( ( sk2 @ relation_dom )
!= sk13 )
| ( sk2 != empty_set ) ),
inference(pattern_uni,[status(thm)],[14480:[]]) ).
thf(1079,plain,
( ( ( sk2 @ empty )
!= ( empty_set @ empty ) )
| ~ $true
| ~ ( sk1 @ function_inverse @ empty ) ),
inference(paramod_ordered,[status(thm)],[69,962]) ).
thf(1080,plain,
( ( ( sk2 @ empty )
!= ( empty_set @ empty ) )
| ~ ( sk1 @ function_inverse @ empty ) ),
inference(simp,[status(thm)],[1079]) ).
thf(1116,plain,
( ( sk2 != empty_set )
| ~ ( sk1 @ function_inverse @ empty ) ),
inference(simp,[status(thm)],[1080]) ).
thf(14544,plain,
( ( ( sk1 @ function_inverse @ empty )
!= ( sk1 @ empty ) )
| ( sk2 != empty_set )
| ~ $true
| ( sk2 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[13760,1116]) ).
thf(14545,plain,
( ( ( sk1 @ function_inverse @ empty )
!= ( sk1 @ empty ) )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[14544]) ).
thf(14572,plain,
( ( ( sk1 @ function_inverse )
!= sk1 )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[14545]) ).
thf(11860,plain,
! [A: $i] :
( ( A
!= ( sk24 @ function_inverse ) )
| ( sk2 @ relation_dom @ function )
| ( sk1 @ relation_dom @ ( sk1 @ ( A @ sk18 ) @ in ) )
| ( A @ ( sk1 @ sk15 ) ) ),
inference(paramod_ordered,[status(thm)],[7412,11801]) ).
thf(11861,plain,
( ( sk2 @ relation_dom @ function )
| ( sk1 @ relation_dom @ ( sk1 @ ( sk24 @ function_inverse @ sk18 ) @ in ) )
| ( sk24 @ function_inverse @ ( sk1 @ sk15 ) ) ),
inference(pattern_uni,[status(thm)],[11860:[bind(A,$thf( sk24 @ function_inverse ))]]) ).
thf(202,plain,
! [B: $i,A: $i] :
( ( B
= ( A @ function_inverse ) )
| ( ( A @ ( B @ sk22 ) )
= ( A @ ( B @ sk23 ) @ ( A @ apply ) ) )
| ( B @ ( A @ sk19 ) )
| ( ( B @ relation_dom )
!= ( A @ relation_rng ) )
| ~ ( B @ function )
| ~ ( B @ relation )
| ~ ( A @ one_to_one )
| ~ ( A @ function )
| ~ ( A @ relation ) ),
inference(cnfConj,[status(thm)],[192]) ).
thf(204,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ sk19 ) )
| ~ ( B @ function )
| ~ ( B @ relation )
| ~ ( A @ one_to_one )
| ~ ( A @ function )
| ~ ( A @ relation )
| ( B
= ( A @ function_inverse ) )
| ( ( A @ ( B @ sk22 ) )
= ( A @ ( B @ sk23 ) @ ( A @ apply ) ) )
| ( ( B @ relation_dom )
!= ( A @ relation_rng ) ) ),
inference(lifteq,[status(thm)],[202]) ).
thf(1204,plain,
( ( ( sk2 @ empty )
!= ( empty_set @ empty ) )
| ( ( sk1 @ function_inverse )
!= empty_set )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[69,1110]) ).
thf(1205,plain,
( ( ( sk2 @ empty )
!= ( empty_set @ empty ) )
| ( ( sk1 @ function_inverse )
!= empty_set ) ),
inference(simp,[status(thm)],[1204]) ).
thf(1226,plain,
( ( sk2 != empty_set )
| ( ( sk1 @ function_inverse )
!= empty_set ) ),
inference(simp,[status(thm)],[1205]) ).
thf(3456,plain,
! [A: $i] :
( ( ( sk2 @ relation_dom @ empty )
!= ( A @ empty ) )
| ~ $true
| ( A = empty_set )
| ~ ( sk1 @ empty ) ),
inference(paramod_ordered,[status(thm)],[2185,85]) ).
thf(3457,plain,
! [A: $i] :
( ( ( sk2 @ relation_dom @ empty )
!= ( A @ empty ) )
| ( A = empty_set )
| ~ ( sk1 @ empty ) ),
inference(simp,[status(thm)],[3456]) ).
thf(3458,plain,
( ( ( sk2 @ relation_dom )
= empty_set )
| ~ ( sk1 @ empty ) ),
inference(pattern_uni,[status(thm)],[3457:[bind(A,$thf( sk2 @ relation_dom ))]]) ).
thf(3263,plain,
! [A: $i] :
( ( ( empty_set @ function )
!= ( A @ function ) )
| ( A @ function_inverse @ relation )
| ~ $true
| ~ ( A @ relation ) ),
inference(paramod_ordered,[status(thm)],[2014,138]) ).
thf(3264,plain,
! [A: $i] :
( ( ( empty_set @ function )
!= ( A @ function ) )
| ( A @ function_inverse @ relation )
| ~ ( A @ relation ) ),
inference(simp,[status(thm)],[3263]) ).
thf(3265,plain,
( ( empty_set @ function_inverse @ relation )
| ~ ( empty_set @ relation ) ),
inference(pattern_uni,[status(thm)],[3264:[bind(A,$thf( empty_set ))]]) ).
thf(9658,plain,
( ( empty_set @ function_inverse @ relation )
| ~ $true ),
inference(rewrite,[status(thm)],[3265,100]) ).
thf(9659,plain,
empty_set @ function_inverse @ relation,
inference(simp,[status(thm)],[9658]) ).
thf(2303,plain,
( ( ( sk2 @ relation_rng )
!= ( empty_set @ relation_rng ) )
| ( ( sk1 @ relation_dom )
= empty_set ) ),
inference(paramod_ordered,[status(thm)],[51,2234]) ).
thf(2308,plain,
( ( sk2 != empty_set )
| ( ( sk1 @ relation_dom )
= empty_set ) ),
inference(simp,[status(thm)],[2303]) ).
thf(166,plain,
! [B: $i,A: $i] :
( ( B
= ( A @ relation_rng ) )
| ( ( A @ ( B @ sk17 ) )
= ( A @ ( B @ sk18 ) @ ( A @ apply ) ) )
| ( B @ ( A @ sk15 ) )
| ~ ( A @ function )
| ~ ( A @ relation ) ),
inference(cnfConj,[status(thm)],[163]) ).
thf(180,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ sk15 ) )
| ~ ( A @ function )
| ~ ( A @ relation )
| ( B
= ( A @ relation_rng ) )
| ( ( A @ ( B @ sk17 ) )
= ( A @ ( B @ sk18 ) @ ( A @ apply ) ) ) ),
inference(lifteq,[status(thm)],[166]) ).
thf(181,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ sk15 ) )
| ~ ( A @ function )
| ~ ( A @ relation )
| ( B
= ( A @ relation_rng ) )
| ( ( A @ ( B @ sk17 ) )
= ( A @ ( B @ sk18 ) @ ( A @ apply ) ) ) ),
inference(simp,[status(thm)],[180]) ).
thf(2440,plain,
( ( ( sk2 @ relation_rng )
!= ( empty_set @ relation_rng ) )
| ( sk1 @ relation_dom @ relation ) ),
inference(paramod_ordered,[status(thm)],[51,2419]) ).
thf(2442,plain,
( ( sk2 != empty_set )
| ( sk1 @ relation_dom @ relation ) ),
inference(simp,[status(thm)],[2440]) ).
thf(6435,plain,
! [B: $i,A: $i] :
( ( ( A @ powerset @ ( empty_set @ in ) )
!= ( B @ ( B @ powerset @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2822,4625]) ).
thf(6436,plain,
! [B: $i,A: $i] :
( ( A @ powerset @ ( empty_set @ in ) )
!= ( B @ ( B @ powerset @ in ) ) ),
inference(simp,[status(thm)],[6435]) ).
thf(6463,plain,
! [B: $i,A: $i] :
( ( ( A @ powerset )
!= B )
| ( ( B @ powerset )
!= empty_set ) ),
inference(simp,[status(thm)],[6436]) ).
thf(6478,plain,
! [A: $i] :
( ( A @ powerset @ powerset )
!= empty_set ),
inference(simp,[status(thm)],[6463]) ).
thf(168,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ relation_dom @ ( A @ ( B @ ( C @ sk14 ) ) @ in ) )
| ~ ( B @ ( C @ in ) )
| ( B
!= ( A @ relation_rng ) )
| ~ ( A @ function )
| ~ ( A @ relation ) ),
inference(cnfConj,[status(thm)],[163]) ).
thf(186,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ relation_dom @ ( A @ ( B @ ( C @ sk14 ) ) @ in ) )
| ~ ( B @ ( C @ in ) )
| ~ ( A @ function )
| ~ ( A @ relation )
| ( B
!= ( A @ relation_rng ) ) ),
inference(lifteq,[status(thm)],[168]) ).
thf(187,plain,
! [B: $i,A: $i] :
( ( A @ relation_dom @ ( A @ ( A @ relation_rng @ ( B @ sk14 ) ) @ in ) )
| ~ ( A @ relation_rng @ ( B @ in ) )
| ~ ( A @ function )
| ~ ( A @ relation ) ),
inference(simp,[status(thm)],[186]) ).
thf(4875,plain,
! [A: $i] :
( ( ( empty_set @ relation_rng @ empty )
!= ( A @ empty ) )
| ( A @ relation_dom @ empty )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2318,157]) ).
thf(4876,plain,
! [A: $i] :
( ( ( empty_set @ relation_rng @ empty )
!= ( A @ empty ) )
| ( A @ relation_dom @ empty ) ),
inference(simp,[status(thm)],[4875]) ).
thf(4877,plain,
empty_set @ relation_rng @ relation_dom @ empty,
inference(pattern_uni,[status(thm)],[4876:[bind(A,$thf( empty_set @ relation_rng ))]]) ).
thf(5212,plain,
empty_set @ relation_dom @ empty,
inference(rewrite,[status(thm)],[4877,2234]) ).
thf(200,plain,
! [B: $i,A: $i] :
( ( B
= ( A @ function_inverse ) )
| ( ( A @ ( B @ sk23 ) )
!= ( A @ ( B @ sk22 ) @ ( B @ apply ) ) )
| ~ ( A @ relation_rng @ ( A @ ( B @ sk22 ) @ in ) )
| ( B @ ( A @ sk19 ) )
| ( ( B @ relation_dom )
!= ( A @ relation_rng ) )
| ~ ( B @ function )
| ~ ( B @ relation )
| ~ ( A @ one_to_one )
| ~ ( A @ function )
| ~ ( A @ relation ) ),
inference(cnfConj,[status(thm)],[192]) ).
thf(219,plain,
! [B: $i,A: $i] :
( ~ ( A @ relation_rng @ ( A @ ( B @ sk22 ) @ in ) )
| ( B @ ( A @ sk19 ) )
| ~ ( B @ function )
| ~ ( B @ relation )
| ~ ( A @ one_to_one )
| ~ ( A @ function )
| ~ ( A @ relation )
| ( B
= ( A @ function_inverse ) )
| ( ( A @ ( B @ sk23 ) )
!= ( A @ ( B @ sk22 ) @ ( B @ apply ) ) )
| ( ( B @ relation_dom )
!= ( A @ relation_rng ) ) ),
inference(lifteq,[status(thm)],[200]) ).
thf(241,plain,
( ( ( sk13 @ empty )
!= ( empty_set @ empty ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[69,149]) ).
thf(242,plain,
( ( sk13 @ empty )
!= ( empty_set @ empty ) ),
inference(simp,[status(thm)],[241]) ).
thf(245,plain,
sk13 != empty_set,
inference(simp,[status(thm)],[242]) ).
thf(3916,plain,
( ( ( sk1 @ relation_dom @ empty )
!= ( sk13 @ empty ) )
| ~ $true
| ( sk2 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[2280,149]) ).
thf(3917,plain,
( ( ( sk1 @ relation_dom @ empty )
!= ( sk13 @ empty ) )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[3916]) ).
thf(3977,plain,
( ( ( sk1 @ relation_dom )
!= sk13 )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[3917]) ).
thf(3308,plain,
! [A: $i] :
( ( ( sk13 @ relation )
!= ( A @ relation ) )
| ( A @ function_inverse @ relation )
| ~ ( A @ function )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[150,138]) ).
thf(3309,plain,
! [A: $i] :
( ( ( sk13 @ relation )
!= ( A @ relation ) )
| ( A @ function_inverse @ relation )
| ~ ( A @ function ) ),
inference(simp,[status(thm)],[3308]) ).
thf(3310,plain,
( ( sk13 @ function_inverse @ relation )
| ~ ( sk13 @ function ) ),
inference(pattern_uni,[status(thm)],[3309:[bind(A,$thf( sk13 ))]]) ).
thf(19,axiom,
! [A: $i,B: $i] :
~ ( ( B @ empty )
& ( B @ ( A @ in ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t7_boole) ).
thf(112,plain,
! [A: $i,B: $i] :
~ ( ( B @ empty )
& ( B @ ( A @ in ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[19]) ).
thf(113,plain,
~ ? [A: $i,B: $i] :
( ( B @ empty )
& ( B @ ( A @ in ) ) ),
inference(miniscope,[status(thm)],[112]) ).
thf(114,plain,
! [B: $i,A: $i] :
( ~ ( B @ empty )
| ~ ( B @ ( A @ in ) ) ),
inference(cnf,[status(esa)],[113]) ).
thf(2533,plain,
! [B: $i,A: $i] :
( ( ( empty_set @ empty )
!= ( B @ empty ) )
| ~ $true
| ~ ( B @ ( A @ in ) ) ),
inference(paramod_ordered,[status(thm)],[69,114]) ).
thf(2534,plain,
! [B: $i,A: $i] :
( ( ( empty_set @ empty )
!= ( B @ empty ) )
| ~ ( B @ ( A @ in ) ) ),
inference(simp,[status(thm)],[2533]) ).
thf(2535,plain,
! [A: $i] :
~ ( empty_set @ ( A @ in ) ),
inference(pattern_uni,[status(thm)],[2534:[bind(A,$thf( A )),bind(B,$thf( empty_set ))]]) ).
thf(10185,plain,
! [A: $i] :
( ( A
!= ( sk2 @ function_inverse ) )
| ( sk2 @ relation_dom @ function )
| ( sk1 @ relation_dom @ ( sk1 @ ( A @ sk18 ) @ in ) )
| ( A @ ( sk1 @ sk15 ) ) ),
inference(paramod_ordered,[status(thm)],[7412,10139]) ).
thf(10186,plain,
( ( sk2 @ relation_dom @ function )
| ( sk1 @ relation_dom @ ( sk1 @ ( sk2 @ function_inverse @ sk18 ) @ in ) )
| ( sk2 @ function_inverse @ ( sk1 @ sk15 ) ) ),
inference(pattern_uni,[status(thm)],[10185:[bind(A,$thf( sk2 @ function_inverse ))]]) ).
thf(17711,plain,
( ( ( sk2 @ empty )
!= ( sk2 @ empty ) )
| ( sk1 = empty_set )
| ~ $true
| ~ ( sk1 @ empty ) ),
inference(paramod_ordered,[status(thm)],[17564,15094]) ).
thf(17712,plain,
( ( ( sk2 @ empty )
!= ( sk2 @ empty ) )
| ( sk1 = empty_set )
| ~ ( sk1 @ empty ) ),
inference(simp,[status(thm)],[17711]) ).
thf(17713,plain,
( ( sk1 = empty_set )
| ~ ( sk1 @ empty ) ),
inference(pattern_uni,[status(thm)],[17712:[]]) ).
thf(23,axiom,
! [A: $i] :
( ( ( A @ function )
& ( A @ relation ) )
=> ! [B: $i] :
( ( ( B @ function )
& ( B @ relation ) )
=> ( ( ! [C: $i] :
( ( A @ relation_dom @ ( C @ in ) )
=> ( ( C @ ( A @ apply ) )
= ( C @ ( B @ apply ) ) ) )
& ( ( A @ relation_dom )
= ( B @ relation_dom ) ) )
=> ( A = B ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t9_funct_1) ).
thf(126,plain,
! [A: $i] :
( ( ( A @ function )
& ( A @ relation ) )
=> ! [B: $i] :
( ( ( B @ function )
& ( B @ relation ) )
=> ( ( ! [C: $i] :
( ( A @ relation_dom @ ( C @ in ) )
=> ( ( C @ ( A @ apply ) )
= ( C @ ( B @ apply ) ) ) )
& ( ( A @ relation_dom )
= ( B @ relation_dom ) ) )
=> ( A = B ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[23]) ).
thf(127,plain,
! [B: $i,A: $i] :
( ( ( A = B )
| ( ( A @ ( B @ sk11 ) @ ( A @ apply ) )
!= ( A @ ( B @ sk11 ) @ ( B @ apply ) ) )
| ( ( A @ relation_dom )
!= ( B @ relation_dom ) )
| ~ ( B @ function )
| ~ ( B @ relation )
| ~ ( A @ function )
| ~ ( A @ relation ) )
& ( ( A = B )
| ( A @ relation_dom @ ( A @ ( B @ sk11 ) @ in ) )
| ( ( A @ relation_dom )
!= ( B @ relation_dom ) )
| ~ ( B @ function )
| ~ ( B @ relation )
| ~ ( A @ function )
| ~ ( A @ relation ) ) ),
inference(cnf,[status(esa)],[126]) ).
thf(128,plain,
! [B: $i,A: $i] :
( ( A = B )
| ( A @ relation_dom @ ( A @ ( B @ sk11 ) @ in ) )
| ( ( A @ relation_dom )
!= ( B @ relation_dom ) )
| ~ ( B @ function )
| ~ ( B @ relation )
| ~ ( A @ function )
| ~ ( A @ relation ) ),
inference(cnfConj,[status(thm)],[127]) ).
thf(130,plain,
! [B: $i,A: $i] :
( ( A @ relation_dom @ ( A @ ( B @ sk11 ) @ in ) )
| ~ ( B @ function )
| ~ ( B @ relation )
| ~ ( A @ function )
| ~ ( A @ relation )
| ( A = B )
| ( ( A @ relation_dom )
!= ( B @ relation_dom ) ) ),
inference(lifteq,[status(thm)],[128]) ).
thf(118,plain,
( ( sk9 @ relation )
& ( sk9 @ empty ) ),
inference(cnf,[status(esa)],[117]) ).
thf(119,plain,
sk9 @ empty,
inference(cnfConj,[status(thm)],[118]) ).
thf(1839,plain,
! [A: $i] :
( ( ( sk9 @ empty )
!= ( A @ empty ) )
| ~ $true
| ( A = empty_set ) ),
inference(paramod_ordered,[status(thm)],[119,85]) ).
thf(1840,plain,
! [A: $i] :
( ( ( sk9 @ empty )
!= ( A @ empty ) )
| ( A = empty_set ) ),
inference(simp,[status(thm)],[1839]) ).
thf(1841,plain,
sk9 = empty_set,
inference(pattern_uni,[status(thm)],[1840:[bind(A,$thf( sk9 ))]]) ).
thf(197,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D
= ( C @ ( B @ apply ) ) )
| ( C
!= ( D @ ( A @ apply ) ) )
| ~ ( A @ relation_dom @ ( D @ in ) )
| ( B
!= ( A @ function_inverse ) )
| ~ ( B @ function )
| ~ ( B @ relation )
| ~ ( A @ one_to_one )
| ~ ( A @ function )
| ~ ( A @ relation ) ),
inference(cnfConj,[status(thm)],[192]) ).
thf(208,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( A @ relation_dom @ ( D @ in ) )
| ~ ( B @ function )
| ~ ( B @ relation )
| ~ ( A @ one_to_one )
| ~ ( A @ function )
| ~ ( A @ relation )
| ( D
= ( C @ ( B @ apply ) ) )
| ( C
!= ( D @ ( A @ apply ) ) )
| ( B
!= ( A @ function_inverse ) ) ),
inference(lifteq,[status(thm)],[197]) ).
thf(209,plain,
! [B: $i,A: $i] :
( ~ ( A @ relation_dom @ ( B @ in ) )
| ~ ( A @ function_inverse @ function )
| ~ ( A @ function_inverse @ relation )
| ~ ( A @ one_to_one )
| ~ ( A @ function )
| ~ ( A @ relation )
| ( ( B @ ( A @ apply ) @ ( A @ function_inverse @ apply ) )
= B ) ),
inference(simp,[status(thm)],[208]) ).
thf(6447,plain,
! [B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ in ) )
!= ( B @ ( B @ powerset @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[3376,4625]) ).
thf(6448,plain,
! [B: $i,A: $i] :
( ( A @ powerset @ ( A @ in ) )
!= ( B @ ( B @ powerset @ in ) ) ),
inference(simp,[status(thm)],[6447]) ).
thf(6457,plain,
! [B: $i,A: $i] :
( ( ( A @ powerset )
!= B )
| ( A
!= ( B @ powerset ) ) ),
inference(simp,[status(thm)],[6448]) ).
thf(6472,plain,
! [A: $i] :
( ( A @ powerset @ powerset )
!= A ),
inference(simp,[status(thm)],[6457]) ).
thf(3246,plain,
! [B: $i,A: $i] :
( ( A
!= ( B @ sk7 ) )
| ( B @ ( empty_set @ element ) )
| ( B @ empty )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[85,3199]) ).
thf(3247,plain,
! [A: $i] :
( ( A @ ( empty_set @ element ) )
| ( A @ empty )
| ~ ( A @ sk7 @ empty ) ),
inference(pattern_uni,[status(thm)],[3246:[bind(A,$thf( C @ sk7 )),bind(B,$thf( C ))]]) ).
thf(3260,plain,
! [A: $i] :
( ( A @ ( empty_set @ element ) )
| ( A @ empty )
| ~ ( A @ sk7 @ empty ) ),
inference(simp,[status(thm)],[3247]) ).
thf(3160,plain,
! [B: $i,A: $i] :
( ( A
!= ( B @ sk7 ) )
| ( B @ ( empty_set @ in ) )
| ( B @ empty )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[85,2600]) ).
thf(3161,plain,
! [A: $i] :
( ( A @ ( empty_set @ in ) )
| ( A @ empty )
| ~ ( A @ sk7 @ empty ) ),
inference(pattern_uni,[status(thm)],[3160:[bind(A,$thf( C @ sk7 )),bind(B,$thf( C ))]]) ).
thf(3202,plain,
! [A: $i] :
( ( A @ ( empty_set @ in ) )
| ( A @ empty )
| ~ ( A @ sk7 @ empty ) ),
inference(simp,[status(thm)],[3161]) ).
thf(3473,plain,
! [A: $i] :
( ( ( sk2 @ relation_dom @ empty )
!= ( A @ empty ) )
| ( A @ function )
| ~ $true
| ~ ( sk1 @ empty ) ),
inference(paramod_ordered,[status(thm)],[2185,135]) ).
thf(3474,plain,
! [A: $i] :
( ( ( sk2 @ relation_dom @ empty )
!= ( A @ empty ) )
| ( A @ function )
| ~ ( sk1 @ empty ) ),
inference(simp,[status(thm)],[3473]) ).
thf(3475,plain,
( ( sk2 @ relation_dom @ function )
| ~ ( sk1 @ empty ) ),
inference(pattern_uni,[status(thm)],[3474:[bind(A,$thf( sk2 @ relation_dom ))]]) ).
thf(17830,plain,
( ( ( sk2 @ empty )
!= ( sk2 @ empty ) )
| ( sk13 != sk1 )
| ~ $true
| ( sk1 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[17600,14662]) ).
thf(17831,plain,
( ( ( sk2 @ empty )
!= ( sk2 @ empty ) )
| ( sk13 != sk1 )
| ( sk1 != empty_set ) ),
inference(simp,[status(thm)],[17830]) ).
thf(17832,plain,
( ( sk13 != sk1 )
| ( sk1 != empty_set ) ),
inference(pattern_uni,[status(thm)],[17831:[]]) ).
thf(164,plain,
! [C: $i,B: $i,A: $i] :
( ( B
= ( A @ relation_rng ) )
| ~ ( B @ ( A @ sk15 ) )
| ( ( A @ ( B @ sk16 ) )
!= ( C @ ( A @ apply ) ) )
| ~ ( A @ relation_dom @ ( C @ in ) )
| ~ ( A @ function )
| ~ ( A @ relation ) ),
inference(cnfConj,[status(thm)],[163]) ).
thf(174,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( B @ ( A @ sk15 ) )
| ~ ( A @ relation_dom @ ( C @ in ) )
| ~ ( A @ function )
| ~ ( A @ relation )
| ( B
= ( A @ relation_rng ) )
| ( ( A @ ( B @ sk16 ) )
!= ( C @ ( A @ apply ) ) ) ),
inference(lifteq,[status(thm)],[164]) ).
thf(175,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( B @ ( A @ sk15 ) )
| ~ ( A @ relation_dom @ ( C @ in ) )
| ~ ( A @ function )
| ~ ( A @ relation )
| ( B
= ( A @ relation_rng ) )
| ( ( A @ ( B @ sk16 ) )
!= ( C @ ( A @ apply ) ) ) ),
inference(simp,[status(thm)],[174]) ).
thf(21086,plain,
( ( sk1 != sk1 )
| ( sk2 = empty_set )
| ( empty_set != empty_set )
| ~ ( sk2 @ empty ) ),
inference(paramod_ordered,[status(thm)],[15094,17862]) ).
thf(21087,plain,
( ( sk1 != sk1 )
| ( sk2 = empty_set )
| ~ ( sk2 @ empty ) ),
inference(simp,[status(thm)],[21086]) ).
thf(21088,plain,
( ( sk2 = empty_set )
| ~ ( sk2 @ empty ) ),
inference(pattern_uni,[status(thm)],[21087:[]]) ).
thf(10113,plain,
! [A: $i] :
( ( A
!= ( sk1 @ function_inverse ) )
| ( sk2 @ relation_dom @ function )
| ( sk1 @ relation_dom @ ( sk1 @ ( A @ sk18 ) @ in ) )
| ( A @ ( sk1 @ sk15 ) ) ),
inference(paramod_ordered,[status(thm)],[7412,10067]) ).
thf(10114,plain,
( ( sk2 @ relation_dom @ function )
| ( sk1 @ relation_dom @ ( sk1 @ ( sk1 @ function_inverse @ sk18 ) @ in ) )
| ( sk1 @ function_inverse @ ( sk1 @ sk15 ) ) ),
inference(pattern_uni,[status(thm)],[10113:[bind(A,$thf( sk1 @ function_inverse ))]]) ).
thf(104,plain,
sk8 @ relation_empty_yielding,
inference(cnfConj,[status(thm)],[102]) ).
thf(3541,plain,
( ( ( sk1 @ function_inverse @ empty )
!= ( sk1 @ relation_dom @ empty ) )
| ~ ( sk2 @ empty )
| ~ $true
| ~ ( sk2 @ empty ) ),
inference(paramod_ordered,[status(thm)],[2201,962]) ).
thf(3542,plain,
( ( ( sk1 @ function_inverse @ empty )
!= ( sk1 @ relation_dom @ empty ) )
| ~ ( sk2 @ empty ) ),
inference(simp,[status(thm)],[3541]) ).
thf(3625,plain,
( ( ( sk1 @ function_inverse )
!= ( sk1 @ relation_dom ) )
| ~ ( sk2 @ empty ) ),
inference(simp,[status(thm)],[3542]) ).
thf(195,plain,
! [B: $i,A: $i] :
( ( B
= ( A @ function_inverse ) )
| ( A @ relation_dom @ ( A @ ( B @ sk23 ) @ in ) )
| ( B @ ( A @ sk19 ) )
| ( ( B @ relation_dom )
!= ( A @ relation_rng ) )
| ~ ( B @ function )
| ~ ( B @ relation )
| ~ ( A @ one_to_one )
| ~ ( A @ function )
| ~ ( A @ relation ) ),
inference(cnfConj,[status(thm)],[192]) ).
thf(218,plain,
! [B: $i,A: $i] :
( ( A @ relation_dom @ ( A @ ( B @ sk23 ) @ in ) )
| ( B @ ( A @ sk19 ) )
| ~ ( B @ function )
| ~ ( B @ relation )
| ~ ( A @ one_to_one )
| ~ ( A @ function )
| ~ ( A @ relation )
| ( B
= ( A @ function_inverse ) )
| ( ( B @ relation_dom )
!= ( A @ relation_rng ) ) ),
inference(lifteq,[status(thm)],[195]) ).
thf(158,plain,
! [A: $i] :
( ( A @ relation_dom @ relation )
| ~ ( A @ empty ) ),
inference(cnfConj,[status(thm)],[156]) ).
thf(3340,plain,
( ( ( sk1 @ empty )
!= ( empty_set @ empty ) )
| ( ( empty_set @ function_inverse )
!= sk2 )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[69,1613]) ).
thf(3341,plain,
( ( ( sk1 @ empty )
!= ( empty_set @ empty ) )
| ( ( empty_set @ function_inverse )
!= sk2 ) ),
inference(simp,[status(thm)],[3340]) ).
thf(3369,plain,
( ( sk1 != empty_set )
| ( ( empty_set @ function_inverse )
!= sk2 ) ),
inference(simp,[status(thm)],[3341]) ).
thf(17670,plain,
! [A: $i] :
( ( ( sk2 @ empty )
!= ( A @ empty ) )
| ~ $true
| ( A = empty_set )
| ~ ( sk1 @ empty ) ),
inference(paramod_ordered,[status(thm)],[17564,85]) ).
thf(17671,plain,
! [A: $i] :
( ( ( sk2 @ empty )
!= ( A @ empty ) )
| ( A = empty_set )
| ~ ( sk1 @ empty ) ),
inference(simp,[status(thm)],[17670]) ).
thf(17672,plain,
( ( sk2 = empty_set )
| ~ ( sk1 @ empty ) ),
inference(pattern_uni,[status(thm)],[17671:[bind(A,$thf( sk2 ))]]) ).
thf(17702,plain,
( ( ( sk13 @ empty )
!= ( sk2 @ empty ) )
| ~ $true
| ~ ( sk1 @ empty ) ),
inference(paramod_ordered,[status(thm)],[17564,149]) ).
thf(17703,plain,
( ( ( sk13 @ empty )
!= ( sk2 @ empty ) )
| ~ ( sk1 @ empty ) ),
inference(simp,[status(thm)],[17702]) ).
thf(17804,plain,
( ( sk13 != sk2 )
| ~ ( sk1 @ empty ) ),
inference(simp,[status(thm)],[17703]) ).
thf(3952,plain,
( ( ( sk1 @ function_inverse @ empty )
!= ( sk1 @ relation_dom @ empty ) )
| ( sk2 != empty_set )
| ~ $true
| ( sk2 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[2280,1116]) ).
thf(3953,plain,
( ( ( sk1 @ function_inverse @ empty )
!= ( sk1 @ relation_dom @ empty ) )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[3952]) ).
thf(3978,plain,
( ( ( sk1 @ function_inverse )
!= ( sk1 @ relation_dom ) )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[3953]) ).
thf(243,plain,
( ( ( sk4 @ empty )
!= ( empty_set @ empty ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[69,68]) ).
thf(244,plain,
( ( sk4 @ empty )
!= ( empty_set @ empty ) ),
inference(simp,[status(thm)],[243]) ).
thf(246,plain,
sk4 != empty_set,
inference(simp,[status(thm)],[244]) ).
thf(17883,plain,
( ( ( sk2 @ empty )
!= ( sk2 @ empty ) )
| ( sk1 @ empty )
| ~ $true
| ( sk1 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[17600,13805]) ).
thf(17884,plain,
( ( ( sk2 @ empty )
!= ( sk2 @ empty ) )
| ( sk1 @ empty )
| ( sk1 != empty_set ) ),
inference(simp,[status(thm)],[17883]) ).
thf(17885,plain,
( ( sk1 @ empty )
| ( sk1 != empty_set ) ),
inference(pattern_uni,[status(thm)],[17884:[]]) ).
thf(201,plain,
! [B: $i,A: $i] :
( ( B
= ( A @ function_inverse ) )
| ~ ( B @ ( A @ sk19 ) )
| ( ( A @ ( B @ sk20 ) )
!= ( A @ ( B @ sk21 ) @ ( A @ apply ) ) )
| ~ ( A @ relation_dom @ ( A @ ( B @ sk21 ) @ in ) )
| ( ( B @ relation_dom )
!= ( A @ relation_rng ) )
| ~ ( B @ function )
| ~ ( B @ relation )
| ~ ( A @ one_to_one )
| ~ ( A @ function )
| ~ ( A @ relation ) ),
inference(cnfConj,[status(thm)],[192]) ).
thf(207,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ sk19 ) )
| ~ ( A @ relation_dom @ ( A @ ( B @ sk21 ) @ in ) )
| ~ ( B @ function )
| ~ ( B @ relation )
| ~ ( A @ one_to_one )
| ~ ( A @ function )
| ~ ( A @ relation )
| ( B
= ( A @ function_inverse ) )
| ( ( A @ ( B @ sk20 ) )
!= ( A @ ( B @ sk21 ) @ ( A @ apply ) ) )
| ( ( B @ relation_dom )
!= ( A @ relation_rng ) ) ),
inference(lifteq,[status(thm)],[201]) ).
thf(3675,plain,
! [A: $i] :
( ( ( sk8 @ relation )
!= ( A @ relation ) )
| ( A @ function_inverse @ function )
| ~ ( A @ function )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[103,139]) ).
thf(3676,plain,
! [A: $i] :
( ( ( sk8 @ relation )
!= ( A @ relation ) )
| ( A @ function_inverse @ function )
| ~ ( A @ function ) ),
inference(simp,[status(thm)],[3675]) ).
thf(3677,plain,
( ( sk8 @ function_inverse @ function )
| ~ ( sk8 @ function ) ),
inference(pattern_uni,[status(thm)],[3676:[bind(A,$thf( sk8 ))]]) ).
thf(194,plain,
! [B: $i,A: $i] :
( ( ( B @ relation_dom )
= ( A @ relation_rng ) )
| ( B
!= ( A @ function_inverse ) )
| ~ ( B @ function )
| ~ ( B @ relation )
| ~ ( A @ one_to_one )
| ~ ( A @ function )
| ~ ( A @ relation ) ),
inference(cnfConj,[status(thm)],[192]) ).
thf(213,plain,
! [B: $i,A: $i] :
( ~ ( B @ function )
| ~ ( B @ relation )
| ~ ( A @ one_to_one )
| ~ ( A @ function )
| ~ ( A @ relation )
| ( ( B @ relation_dom )
= ( A @ relation_rng ) )
| ( B
!= ( A @ function_inverse ) ) ),
inference(lifteq,[status(thm)],[194]) ).
thf(214,plain,
! [A: $i] :
( ~ ( A @ function_inverse @ function )
| ~ ( A @ function_inverse @ relation )
| ~ ( A @ one_to_one )
| ~ ( A @ function )
| ~ ( A @ relation )
| ( ( A @ function_inverse @ relation_dom )
= ( A @ relation_rng ) ) ),
inference(simp,[status(thm)],[213]) ).
thf(11771,plain,
! [A: $i] :
( ( A
!= ( empty_set @ function_inverse ) )
| ( sk2 @ relation_dom @ function )
| ( sk1 @ relation_dom @ ( sk1 @ ( A @ sk18 ) @ in ) )
| ( A @ ( sk1 @ sk15 ) ) ),
inference(paramod_ordered,[status(thm)],[7412,11710]) ).
thf(11772,plain,
( ( sk2 @ relation_dom @ function )
| ( sk1 @ relation_dom @ ( sk1 @ ( empty_set @ function_inverse @ sk18 ) @ in ) )
| ( empty_set @ function_inverse @ ( sk1 @ sk15 ) ) ),
inference(pattern_uni,[status(thm)],[11771:[bind(A,$thf( empty_set @ function_inverse ))]]) ).
thf(5402,plain,
! [A: $i] :
( ( ( empty_set @ relation_dom @ empty )
!= ( A @ empty ) )
| ( A @ relation_dom @ relation )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[5212,158]) ).
thf(5403,plain,
! [A: $i] :
( ( ( empty_set @ relation_dom @ empty )
!= ( A @ empty ) )
| ( A @ relation_dom @ relation ) ),
inference(simp,[status(thm)],[5402]) ).
thf(5404,plain,
empty_set @ relation_dom @ relation_dom @ relation,
inference(pattern_uni,[status(thm)],[5403:[bind(A,$thf( empty_set @ relation_dom ))]]) ).
thf(4817,plain,
! [A: $i] :
( ( ( empty_set @ empty )
!= ( A @ empty ) )
| ( A @ relation_dom @ empty )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[69,157]) ).
thf(4818,plain,
! [A: $i] :
( ( ( empty_set @ empty )
!= ( A @ empty ) )
| ( A @ relation_dom @ empty ) ),
inference(simp,[status(thm)],[4817]) ).
thf(4819,plain,
empty_set @ relation_dom @ empty,
inference(pattern_uni,[status(thm)],[4818:[bind(A,$thf( empty_set ))]]) ).
thf(4975,plain,
! [A: $i] :
( ( ( empty_set @ relation_dom @ empty )
!= ( A @ empty ) )
| ~ $true
| ( A = empty_set ) ),
inference(paramod_ordered,[status(thm)],[4819,85]) ).
thf(4976,plain,
! [A: $i] :
( ( ( empty_set @ relation_dom @ empty )
!= ( A @ empty ) )
| ( A = empty_set ) ),
inference(simp,[status(thm)],[4975]) ).
thf(4977,plain,
( ( empty_set @ relation_dom )
= empty_set ),
inference(pattern_uni,[status(thm)],[4976:[bind(A,$thf( empty_set @ relation_dom ))]]) ).
thf(6198,plain,
empty_set @ relation_dom @ relation,
inference(rewrite,[status(thm)],[5404,4977]) ).
thf(9710,plain,
! [A: $i] :
( ( A
!= ( empty_set @ function_inverse ) )
| ( sk2 @ relation_dom @ relation )
| ( sk1 @ relation_dom @ ( sk1 @ ( A @ sk18 ) @ in ) )
| ( A @ ( sk1 @ sk15 ) ) ),
inference(paramod_ordered,[status(thm)],[7412,9659]) ).
thf(9711,plain,
( ( sk2 @ relation_dom @ relation )
| ( sk1 @ relation_dom @ ( sk1 @ ( empty_set @ function_inverse @ sk18 ) @ in ) )
| ( empty_set @ function_inverse @ ( sk1 @ sk15 ) ) ),
inference(pattern_uni,[status(thm)],[9710:[bind(A,$thf( empty_set @ function_inverse ))]]) ).
thf(167,plain,
! [C: $i,B: $i,A: $i] :
( ( C
= ( A @ ( B @ ( C @ sk14 ) ) @ ( A @ apply ) ) )
| ~ ( B @ ( C @ in ) )
| ( B
!= ( A @ relation_rng ) )
| ~ ( A @ function )
| ~ ( A @ relation ) ),
inference(cnfConj,[status(thm)],[163]) ).
thf(182,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( B @ ( C @ in ) )
| ~ ( A @ function )
| ~ ( A @ relation )
| ( ( A @ ( B @ ( C @ sk14 ) ) @ ( A @ apply ) )
= C )
| ( B
!= ( A @ relation_rng ) ) ),
inference(lifteq,[status(thm)],[167]) ).
thf(183,plain,
! [B: $i,A: $i] :
( ~ ( A @ relation_rng @ ( B @ in ) )
| ~ ( A @ function )
| ~ ( A @ relation )
| ( ( A @ ( A @ relation_rng @ ( B @ sk14 ) ) @ ( A @ apply ) )
= B ) ),
inference(simp,[status(thm)],[182]) ).
thf(272,plain,
! [A: $i] :
( ( ( sk2 @ relation_dom )
!= ( sk2 @ relation_dom ) )
| ~ ( sk1 @ relation_dom @ ( A @ ( sk1 @ apply ) @ in ) )
| ~ ( sk1 @ relation_dom @ ( A @ in ) )
| ( ( A @ ( sk1 @ apply ) @ ( sk2 @ apply ) )
= A )
| ( sk2 != sk1 ) ),
inference(paramod_ordered,[status(thm)],[250,57]) ).
thf(273,plain,
! [A: $i] :
( ~ ( sk1 @ relation_dom @ ( A @ ( sk1 @ apply ) @ in ) )
| ~ ( sk1 @ relation_dom @ ( A @ in ) )
| ( ( A @ ( sk1 @ apply ) @ ( sk2 @ apply ) )
= A )
| ( sk2 != sk1 ) ),
inference(pattern_uni,[status(thm)],[272:[]]) ).
thf(79,plain,
! [A: $i] :
( ~ ( A @ sk5 @ empty )
| ( A @ empty ) ),
inference(cnfConj,[status(thm)],[77]) ).
thf(3669,plain,
! [A: $i] :
( ( ( sk10 @ function )
!= ( A @ function ) )
| ( A @ function_inverse @ function )
| ~ $true
| ~ ( A @ relation ) ),
inference(paramod_ordered,[status(thm)],[124,139]) ).
thf(3670,plain,
! [A: $i] :
( ( ( sk10 @ function )
!= ( A @ function ) )
| ( A @ function_inverse @ function )
| ~ ( A @ relation ) ),
inference(simp,[status(thm)],[3669]) ).
thf(3671,plain,
( ( sk10 @ function_inverse @ function )
| ~ ( sk10 @ relation ) ),
inference(pattern_uni,[status(thm)],[3670:[bind(A,$thf( sk10 ))]]) ).
thf(11889,plain,
( ( sk10 @ function_inverse @ function )
| ~ $true ),
inference(rewrite,[status(thm)],[3671,123]) ).
thf(11890,plain,
sk10 @ function_inverse @ function,
inference(simp,[status(thm)],[11889]) ).
thf(11949,plain,
! [A: $i] :
( ( A
!= ( sk10 @ function_inverse ) )
| ( sk2 @ relation_dom @ function )
| ( sk1 @ relation_dom @ ( sk1 @ ( A @ sk18 ) @ in ) )
| ( A @ ( sk1 @ sk15 ) ) ),
inference(paramod_ordered,[status(thm)],[7412,11890]) ).
thf(11950,plain,
( ( sk2 @ relation_dom @ function )
| ( sk1 @ relation_dom @ ( sk1 @ ( sk10 @ function_inverse @ sk18 ) @ in ) )
| ( sk10 @ function_inverse @ ( sk1 @ sk15 ) ) ),
inference(pattern_uni,[status(thm)],[11949:[bind(A,$thf( sk10 @ function_inverse ))]]) ).
thf(4496,plain,
! [A: $i] :
( ( ( A @ sk7 @ empty )
!= ( empty_set @ empty ) )
| ( A @ ( empty_set @ in ) )
| ( A @ empty )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[69,3202]) ).
thf(4497,plain,
! [A: $i] :
( ( ( A @ sk7 @ empty )
!= ( empty_set @ empty ) )
| ( A @ ( empty_set @ in ) )
| ( A @ empty ) ),
inference(simp,[status(thm)],[4496]) ).
thf(4565,plain,
! [A: $i] :
( ( ( A @ sk7 )
!= empty_set )
| ( A @ ( empty_set @ in ) )
| ( A @ empty ) ),
inference(simp,[status(thm)],[4497]) ).
thf(3269,plain,
! [A: $i] :
( ( ( sk1 @ relation )
!= ( A @ relation ) )
| ( A @ function_inverse @ relation )
| ~ ( A @ function )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[41,138]) ).
thf(3270,plain,
! [A: $i] :
( ( ( sk1 @ relation )
!= ( A @ relation ) )
| ( A @ function_inverse @ relation )
| ~ ( A @ function ) ),
inference(simp,[status(thm)],[3269]) ).
thf(3271,plain,
( ( sk1 @ function_inverse @ relation )
| ~ ( sk1 @ function ) ),
inference(pattern_uni,[status(thm)],[3270:[bind(A,$thf( sk1 ))]]) ).
thf(5617,plain,
( ( sk1 @ function_inverse @ relation )
| ~ $true ),
inference(rewrite,[status(thm)],[3271,49]) ).
thf(5618,plain,
sk1 @ function_inverse @ relation,
inference(simp,[status(thm)],[5617]) ).
thf(7914,plain,
! [A: $i] :
( ( A
!= ( sk1 @ function_inverse ) )
| ( sk2 @ relation_dom @ relation )
| ( sk1 @ relation_dom @ ( sk1 @ ( A @ sk18 ) @ in ) )
| ( A @ ( sk1 @ sk15 ) ) ),
inference(paramod_ordered,[status(thm)],[7412,5618]) ).
thf(7915,plain,
( ( sk2 @ relation_dom @ relation )
| ( sk1 @ relation_dom @ ( sk1 @ ( sk1 @ function_inverse @ sk18 ) @ in ) )
| ( sk1 @ function_inverse @ ( sk1 @ sk15 ) ) ),
inference(pattern_uni,[status(thm)],[7914:[bind(A,$thf( sk1 @ function_inverse ))]]) ).
thf(129,plain,
! [B: $i,A: $i] :
( ( A = B )
| ( ( A @ ( B @ sk11 ) @ ( A @ apply ) )
!= ( A @ ( B @ sk11 ) @ ( B @ apply ) ) )
| ( ( A @ relation_dom )
!= ( B @ relation_dom ) )
| ~ ( B @ function )
| ~ ( B @ relation )
| ~ ( A @ function )
| ~ ( A @ relation ) ),
inference(cnfConj,[status(thm)],[127]) ).
thf(131,plain,
! [B: $i,A: $i] :
( ~ ( B @ function )
| ~ ( B @ relation )
| ~ ( A @ function )
| ~ ( A @ relation )
| ( A = B )
| ( ( A @ ( B @ sk11 ) @ ( A @ apply ) )
!= ( A @ ( B @ sk11 ) @ ( B @ apply ) ) )
| ( ( A @ relation_dom )
!= ( B @ relation_dom ) ) ),
inference(lifteq,[status(thm)],[129]) ).
thf(17962,plain,
( ( ( sk4 @ empty )
!= ( sk2 @ empty ) )
| ~ $true
| ( sk1 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[17600,68]) ).
thf(17963,plain,
( ( ( sk4 @ empty )
!= ( sk2 @ empty ) )
| ( sk1 != empty_set ) ),
inference(simp,[status(thm)],[17962]) ).
thf(17982,plain,
( ( sk4 != sk2 )
| ( sk1 != empty_set ) ),
inference(simp,[status(thm)],[17963]) ).
thf(21986,plain,
( ( sk1 != sk1 )
| ( sk4 != sk2 )
| ( empty_set != empty_set )
| ~ ( sk2 @ empty ) ),
inference(paramod_ordered,[status(thm)],[15094,17982]) ).
thf(21987,plain,
( ( sk1 != sk1 )
| ( sk4 != sk2 )
| ~ ( sk2 @ empty ) ),
inference(simp,[status(thm)],[21986]) ).
thf(21988,plain,
( ( sk4 != sk2 )
| ~ ( sk2 @ empty ) ),
inference(pattern_uni,[status(thm)],[21987:[]]) ).
thf(14448,plain,
( ( ( sk1 @ empty )
!= ( sk1 @ empty ) )
| ( ( empty_set @ function_inverse )
!= sk2 )
| ~ $true
| ( sk2 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[13760,1613]) ).
thf(14449,plain,
( ( ( sk1 @ empty )
!= ( sk1 @ empty ) )
| ( ( empty_set @ function_inverse )
!= sk2 )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[14448]) ).
thf(14450,plain,
( ( ( empty_set @ function_inverse )
!= sk2 )
| ( sk2 != empty_set ) ),
inference(pattern_uni,[status(thm)],[14449:[]]) ).
thf(110,plain,
~ ? [A: $i,B: $i] :
( ? [C: $i] :
( ( C @ empty )
& ( C @ powerset @ ( B @ element ) ) )
& ( B @ ( A @ in ) ) ),
inference(miniscope,[status(thm)],[109]) ).
thf(111,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ empty )
| ~ ( C @ powerset @ ( B @ element ) )
| ~ ( B @ ( A @ in ) ) ),
inference(cnf,[status(esa)],[110]) ).
thf(253,plain,
! [A: $i] :
( ( ( sk2 @ relation_dom )
!= ( sk2 @ relation_dom ) )
| ~ ( sk1 @ relation_dom @ ( A @ in ) )
| ~ ( sk1 @ relation_dom @ ( A @ ( sk2 @ apply ) @ in ) )
| ( ( A @ ( sk2 @ apply ) @ ( sk1 @ apply ) )
= A )
| ( sk2 != sk1 ) ),
inference(paramod_ordered,[status(thm)],[250,53]) ).
thf(254,plain,
! [A: $i] :
( ~ ( sk1 @ relation_dom @ ( A @ in ) )
| ~ ( sk1 @ relation_dom @ ( A @ ( sk2 @ apply ) @ in ) )
| ( ( A @ ( sk2 @ apply ) @ ( sk1 @ apply ) )
= A )
| ( sk2 != sk1 ) ),
inference(pattern_uni,[status(thm)],[253:[]]) ).
thf(2064,plain,
( ( ( sk1 @ empty )
!= ( empty_set @ empty ) )
| ( empty_set @ one_to_one )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[69,1609]) ).
thf(2065,plain,
( ( ( sk1 @ empty )
!= ( empty_set @ empty ) )
| ( empty_set @ one_to_one ) ),
inference(simp,[status(thm)],[2064]) ).
thf(2074,plain,
( ( sk1 != empty_set )
| ( empty_set @ one_to_one ) ),
inference(simp,[status(thm)],[2065]) ).
thf(41451,plain,
$false,
inference(e,[status(thm)],[69,2822,138,101,14463,962,234,2306,9786,2280,1110,115,217,9901,14662,2014,17688,142,3693,153,17976,1705,14506,185,42,1613,20488,14630,3574,125,2185,157,4119,189,4664,1609,152,228,57,1362,3557,78,216,3199,179,17879,9811,20655,121,3923,17862,147,132,133,116,206,4065,233,1199,220,60,117,85,10139,2441,9861,160,70,4091,92,97,10067,3535,14565,12709,17638,224,3968,8068,188,18402,53,3632,141,14473,14687,2419,4315,2053,3294,212,96,109,256,11801,225,124,1964,5576,13805,28450,173,3760,14757,41,4086,134,73,14708,14573,3802,105,8482,3624,4625,64,1146,11710,161,7599,2524,149,2048,3811,14481,14572,11861,204,1226,59,3458,54,9659,2308,17789,181,49,2442,86,159,6478,187,5212,219,76,245,39,103,140,91,66,3977,155,108,15094,135,3310,2535,10186,17713,80,130,1841,3522,2318,2234,209,112,123,3376,17564,63,6472,150,3260,4630,50,28371,177,17600,3202,3475,17832,154,2279,4106,175,43,1240,250,1649,21088,10114,7412,104,3625,218,158,12685,3369,17672,17804,139,17797,9736,55,114,75,3978,58,246,17885,207,3677,214,11772,9887,6198,82,1116,151,9711,51,190,183,273,107,1816,79,11950,11890,2201,126,4565,136,2600,7915,131,68,21988,83,5618,4977,14450,100,17982,90,111,254,227,13760,2074]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU027+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.07 % 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.13/0.40 % Computer : n015.cluster.edu
% 0.13/0.40 % Model : x86_64 x86_64
% 0.13/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.40 % Memory : 8046.5625MB
% 0.13/0.40 % OS : Linux 6.8.0-71-generic
% 0.13/0.40 % CPULimit : 300
% 0.13/0.40 % WCLimit : 300
% 0.13/0.40 % DateTime : Sat Sep 26 08:34:58 UTC 2026
% 0.13/0.40 % CPUTime :
% 0.13/0.40 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 0.89/1.00 % [INFO] Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ...
% 1.43/1.21 % [INFO] Parsing done (215ms).
% 1.43/1.23 % [INFO] Running in sequential loop mode.
% 2.11/1.64 % [INFO] eprover registered as external prover.
% 2.11/1.65 % [INFO] Scanning for conjecture ...
% 2.33/1.78 % [INFO] Found a conjecture (or negated_conjecture) and 36 axioms. Running axiom selection ...
% 2.51/1.87 % [INFO] Axiom selection finished. Selected 36 axioms (removed 0 axioms).
% 2.71/1.92 % [INFO] Problem is first-order (TPTP FOF).
% 2.71/1.93 % [INFO] Type checking passed.
% 2.71/1.94 % [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 ...
% 91.75/22.55 % External prover 'e' found a proof!
% 91.75/22.55 % [INFO] Killing All external provers ...
% 91.75/22.56 % Time passed: 22007ms (effective reasoning time: 21318ms)
% 91.75/22.56 % 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)>
% 91.75/22.56 % Axioms used in derivation (36): rc3_funct_1, cc1_relat_1, rc1_funct_1, t5_subset, fc5_relat_1, rc2_relat_1, fc6_relat_1, d5_funct_1, rc2_xboole_0, antisymmetry_r2_hidden, fc1_xboole_0, fc4_relat_1, t1_subset, rc3_relat_1, t6_boole, rc2_subset_1, t4_subset, dt_k2_funct_1, t7_boole, cc1_funct_1, fc1_subset_1, rc2_funct_1, rc1_subset_1, cc2_funct_1, t3_subset, existence_m1_subset_1, rc1_relat_1, t54_funct_1, reflexivity_r1_tarski, t9_funct_1, t8_boole, rc1_xboole_0, t2_subset, fc7_relat_1, fc12_relat_1, fc8_relat_1
% 91.75/22.56 % No. of inferences in proof: 687
% 91.75/22.56 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : 22007 ms resp. 21318 ms w/o parsing
% 89.21/22.80 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 89.21/22.80 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------