%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : SEU017+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% Computer : 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:27 AM UTC 2026
% Result : Theorem 102.03s 23.12s
% Output : Refutation 98.40s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 59
% Syntax : Number of formulae : 1113 ( 134 unt; 0 typ; 19 def)
% Number of atoms : 3913 (1407 equ; 0 cnn)
% Maximal formula atoms : 42 ( 3 avg)
% Number of connectives : 8329 (1876 ~;1799 |; 190 &;4366 @)
% ( 5 <=>; 93 =>; 0 <=; 0 <~>)
% Maximal formula depth : 24 ( 5 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 38 ( 35 usr; 12 con; 0-3 aty)
% Number of variables : 877 ( 16 ^; 805 !; 37 ?; 877 :)
% ( 0 !>; 0 ?*; 0 @-; 19 @+)
% Comments :
%------------------------------------------------------------------------------
thf(relation_decl,type,
relation: $i > $o ).
thf(function_decl,type,
function: $i > $o ).
thf(relation_dom_decl,type,
relation_dom: $i > $i ).
thf(subset_decl,type,
subset: $i > $i > $o ).
thf(relation_rng_decl,type,
relation_rng: $i > $i ).
thf(one_to_one_decl,type,
one_to_one: $i > $o ).
thf(relation_composition_decl,type,
relation_composition: $i > $i > $i ).
thf(identity_relation_decl,type,
identity_relation: $i > $i ).
thf(empty_decl,type,
empty: $i > $o ).
thf(in_decl,type,
in: $i > $i > $o ).
thf(element_decl,type,
element: $i > $i > $o ).
thf(powerset_decl,type,
powerset: $i > $i ).
thf(empty_set_decl,type,
empty_set: $i ).
thf(relation_empty_yielding_decl,type,
relation_empty_yielding: $i > $o ).
thf(apply_decl,type,
apply: $i > $i > $i ).
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 ).
thf(sk6_decl,type,
sk6: $i > $i ).
thf(sk7_decl,type,
sk7: $i > $i ).
thf(sk8_decl,type,
sk8: $i > $i ).
thf(sk9_decl,type,
sk9: $i ).
thf(sk10_decl,type,
sk10: $i ).
thf(sk11_decl,type,
sk11: $i ).
thf(sk12_decl,type,
sk12: $i > $i ).
thf(sk13_decl,type,
sk13: $i > $i ).
thf(sk14_decl,type,
sk14: $i ).
thf(sk15_decl,type,
sk15: $i > $i > $i ).
thf(sk16_decl,type,
sk16: $i > $i > $i > $i ).
thf(sk17_decl,type,
sk17: $i > $i > $o ).
thf(sk18_decl,type,
sk18: $i > $i > $i ).
thf(sk19_decl,type,
sk19: $i > $i > $i ).
thf(sk20_decl,type,
sk20: $i > $i > $i ).
thf(sk1_def,definition,
( sk1
= ( @+[A: $i] :
~ ! [B: $i] :
( ( ( B @ function )
& ( B @ relation ) )
=> ! [C: $i] :
( ( ( C @ function )
& ( C @ relation ) )
=> ( ( ( ( B @ ( C @ relation_composition ) )
= B )
& ( B @ one_to_one )
& ( A @ ( C @ relation_rng @ subset ) )
& ( ( C @ relation_dom )
= A )
& ( ( B @ relation_dom )
= A ) )
=> ( C
= ( A @ identity_relation ) ) ) ) ) ) ) ).
thf(sk2_def,definition,
( sk2
= ( @+[A: $i] :
~ ( ( ( A @ function )
& ( A @ relation ) )
=> ! [B: $i] :
( ( ( B @ function )
& ( B @ relation ) )
=> ( ( ( ( A @ ( B @ relation_composition ) )
= A )
& ( A @ one_to_one )
& ( sk1 @ ( B @ relation_rng @ subset ) )
& ( ( B @ relation_dom )
= sk1 )
& ( ( A @ relation_dom )
= sk1 ) )
=> ( B
= ( sk1 @ identity_relation ) ) ) ) ) ) ) ).
thf(sk3_def,definition,
( sk3
= ( @+[A: $i] :
~ ( ( ( A @ function )
& ( A @ relation ) )
=> ( ( ( ( sk2 @ ( A @ relation_composition ) )
= sk2 )
& ( sk2 @ one_to_one )
& ( sk1 @ ( A @ relation_rng @ subset ) )
& ( ( A @ relation_dom )
= sk1 )
& ( ( sk2 @ relation_dom )
= sk1 ) )
=> ( A
= ( sk1 @ identity_relation ) ) ) ) ) ) ).
thf(sk4_def,definition,
( sk4
= ( @+[A: $i] : ( A @ empty ) ) ) ).
thf(sk5_def,definition,
( sk5
= ( @+[A: $i] :
~ ( A @ empty ) ) ) ).
thf(sk6_def,definition,
( sk6
= ( ^ [A: $i] :
@+[B: $i] :
( ~ ( B @ empty )
& ( A @ powerset @ ( B @ element ) ) ) ) ) ).
thf(sk7_def,definition,
( sk7
= ( ^ [A: $i] :
@+[B: $i] :
( ( B @ empty )
& ( A @ powerset @ ( B @ element ) ) ) ) ) ).
thf(sk8_def,definition,
( sk8
= ( ^ [A: $i] :
@+[B: $i] : ( A @ ( B @ element ) ) ) ) ).
thf(sk9_def,definition,
( sk9
= ( @+[A: $i] :
( ( A @ relation_empty_yielding )
& ( A @ relation ) ) ) ) ).
thf(sk10_def,definition,
( sk10
= ( @+[A: $i] :
( ( A @ relation )
& ~ ( A @ empty ) ) ) ) ).
thf(sk11_def,definition,
( sk11
= ( @+[A: $i] :
( ( A @ function )
& ( A @ relation ) ) ) ) ).
thf(sk12_def,definition,
( sk12
= ( ^ [A: $i] :
@+[B: $i] :
~ ! [C: $i] :
( ( ( ( B @ ( A @ apply ) )
= ( C @ ( A @ apply ) ) )
& ( A @ relation_dom @ ( C @ in ) )
& ( A @ relation_dom @ ( B @ in ) ) )
=> ( B = C ) ) ) ) ).
thf(sk13_def,definition,
( sk13
= ( ^ [A: $i] :
@+[B: $i] :
~ ( ( ( ( A @ sk12 @ ( A @ apply ) )
= ( B @ ( A @ apply ) ) )
& ( A @ relation_dom @ ( B @ in ) )
& ( A @ relation_dom @ ( A @ sk12 @ in ) ) )
=> ( ( A @ sk12 )
= B ) ) ) ) ).
thf(sk14_def,definition,
( sk14
= ( @+[A: $i] :
( ( A @ relation )
& ( A @ empty ) ) ) ) ).
thf(sk15_def,definition,
( sk15
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
~ ( ( B @ ( C @ in ) )
=> ( ( C @ ( A @ apply ) )
= C ) ) ) ) ).
thf(sk16_def,definition,
( sk16
= ( ^ [A: $i,B: $i,C: $i] :
@+[D: $i] :
( ( A
= ( D @ ( C @ apply ) ) )
& ( C @ relation_dom @ ( D @ in ) ) ) ) ) ).
thf(sk18_def,definition,
( sk18
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
~ ( ( A @ ( C @ in ) )
=> ? [D: $i] :
( ( C
= ( D @ ( B @ apply ) ) )
& ( B @ relation_dom @ ( D @ in ) ) ) ) ) ) ).
thf(sk19_def,definition,
( sk19
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
~ ( ? [D: $i] :
( ( C
= ( D @ ( B @ apply ) ) )
& ( B @ relation_dom @ ( D @ in ) ) )
=> ( A @ ( C @ in ) ) ) ) ) ).
thf(sk20_def,definition,
( sk20
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
( ( ( B @ ( A @ sk19 ) )
= ( C @ ( B @ apply ) ) )
& ( B @ relation_dom @ ( C @ in ) ) ) ) ) ).
thf(6,axiom,
! [A: $i,B: $i] :
~ ( ( B @ empty )
& ( B @ ( A @ in ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t7_boole) ).
thf(67,plain,
! [A: $i,B: $i] :
~ ( ( B @ empty )
& ( B @ ( A @ in ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(68,plain,
~ ? [A: $i,B: $i] :
( ( B @ empty )
& ( B @ ( A @ in ) ) ),
inference(miniscope,[status(thm)],[67]) ).
thf(69,plain,
! [B: $i,A: $i] :
( ~ ( B @ empty )
| ~ ( B @ ( A @ in ) ) ),
inference(cnf,[status(esa)],[68]) ).
thf(14,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ in ) )
=> ~ ( A @ ( B @ in ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',antisymmetry_r2_hidden) ).
thf(87,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ in ) )
=> ~ ( A @ ( B @ in ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[14]) ).
thf(88,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ in ) )
| ~ ( B @ ( A @ in ) ) ),
inference(cnf,[status(esa)],[87]) ).
thf(1584,plain,
! [B: $i,A: $i] :
( ~ $true
| ( ( A @ ( B @ in ) )
!= ( B @ ( A @ in ) ) )
| ~ ( B @ ( A @ in ) ) ),
inference(eqfactor_ordered,[status(thm)],[88]) ).
thf(1585,plain,
! [A: $i] :
~ ( A @ ( A @ in ) ),
inference(pattern_uni,[status(thm)],[1584:[bind(A,$thf( B ))]]) ).
thf(1586,plain,
! [A: $i] :
~ ( A @ ( A @ in ) ),
inference(simp,[status(thm)],[1585]) ).
thf(12,axiom,
! [A: $i] :
( ( A @ empty )
=> ( A = empty_set ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t6_boole) ).
thf(82,plain,
! [A: $i] :
( ( A @ empty )
=> ( A = empty_set ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[12]) ).
thf(83,plain,
! [A: $i] :
( ( A = empty_set )
| ~ ( A @ empty ) ),
inference(cnf,[status(esa)],[82]) ).
thf(84,plain,
! [A: $i] :
( ~ ( A @ empty )
| ( A = empty_set ) ),
inference(lifteq,[status(thm)],[83]) ).
thf(9,axiom,
empty_set @ empty,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_xboole_0) ).
thf(75,plain,
empty_set @ empty,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).
thf(30,axiom,
? [A: $i] :
( ( A @ function )
& ( A @ relation ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc1_funct_1) ).
thf(136,plain,
? [A: $i] :
( ( A @ function )
& ( A @ relation ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[30]) ).
thf(137,plain,
( ( sk11 @ function )
& ( sk11 @ relation ) ),
inference(cnf,[status(esa)],[136]) ).
thf(138,plain,
sk11 @ relation,
inference(cnfConj,[status(thm)],[137]) ).
thf(22,axiom,
! [A: $i] :
( ( ( A @ relation )
& ~ ( A @ empty ) )
=> ~ ( A @ relation_rng @ empty ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc6_relat_1) ).
thf(112,plain,
! [A: $i] :
( ( ( A @ relation )
& ~ ( A @ empty ) )
=> ~ ( A @ relation_rng @ empty ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[22]) ).
thf(113,plain,
! [A: $i] :
( ~ ( A @ relation_rng @ empty )
| ~ ( A @ relation )
| ( A @ empty ) ),
inference(cnf,[status(esa)],[112]) ).
thf(2617,plain,
! [A: $i] :
( ( ( sk11 @ relation )
!= ( A @ relation ) )
| ~ ( A @ relation_rng @ empty )
| ~ $true
| ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[138,113]) ).
thf(2618,plain,
! [A: $i] :
( ( ( sk11 @ relation )
!= ( A @ relation ) )
| ~ ( A @ relation_rng @ empty )
| ( A @ empty ) ),
inference(simp,[status(thm)],[2617]) ).
thf(2619,plain,
( ~ ( sk11 @ relation_rng @ empty )
| ( sk11 @ empty ) ),
inference(pattern_uni,[status(thm)],[2618:[bind(A,$thf( sk11 ))]]) ).
thf(3153,plain,
( ( ( sk11 @ relation_rng @ empty )
!= ( empty_set @ empty ) )
| ~ $true
| ( sk11 @ empty ) ),
inference(paramod_ordered,[status(thm)],[75,2619]) ).
thf(3154,plain,
( ( ( sk11 @ relation_rng @ empty )
!= ( empty_set @ empty ) )
| ( sk11 @ empty ) ),
inference(simp,[status(thm)],[3153]) ).
thf(3160,plain,
( ( ( sk11 @ relation_rng )
!= empty_set )
| ( sk11 @ empty ) ),
inference(simp,[status(thm)],[3154]) ).
thf(8,axiom,
? [A: $i] :
~ ( A @ empty ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc2_xboole_0) ).
thf(72,plain,
? [A: $i] :
~ ( A @ empty ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(73,plain,
~ ! [A: $i] : ( A @ empty ),
inference(miniscope,[status(thm)],[72]) ).
thf(74,plain,
~ ( sk5 @ empty ),
inference(cnf,[status(esa)],[73]) ).
thf(5006,plain,
( ( ( sk11 @ empty )
!= ( sk5 @ empty ) )
| ~ $true
| ( ( sk11 @ relation_rng )
!= empty_set ) ),
inference(paramod_ordered,[status(thm)],[3160,74]) ).
thf(5007,plain,
( ( ( sk11 @ empty )
!= ( sk5 @ empty ) )
| ( ( sk11 @ relation_rng )
!= empty_set ) ),
inference(simp,[status(thm)],[5006]) ).
thf(5072,plain,
( ( sk11 != sk5 )
| ( ( sk11 @ relation_rng )
!= empty_set ) ),
inference(simp,[status(thm)],[5007]) ).
thf(16135,plain,
! [A: $i] :
( ( A
!= ( sk11 @ relation_rng ) )
| ( sk11 != sk5 )
| ( empty_set != empty_set )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[84,5072]) ).
thf(16136,plain,
! [A: $i] :
( ( A
!= ( sk11 @ relation_rng ) )
| ( sk11 != sk5 )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[16135]) ).
thf(16137,plain,
( ( sk11 != sk5 )
| ~ ( sk11 @ relation_rng @ empty ) ),
inference(pattern_uni,[status(thm)],[16136:[bind(A,$thf( sk11 @ relation_rng ))]]) ).
thf(18,axiom,
? [A: $i] :
( ( A @ relation_empty_yielding )
& ( A @ relation ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc3_relat_1) ).
thf(98,plain,
? [A: $i] :
( ( A @ relation_empty_yielding )
& ( A @ relation ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[18]) ).
thf(99,plain,
( ( sk9 @ relation_empty_yielding )
& ( sk9 @ relation ) ),
inference(cnf,[status(esa)],[98]) ).
thf(101,plain,
sk9 @ relation_empty_yielding,
inference(cnfConj,[status(thm)],[99]) ).
thf(19,axiom,
! [A: $i] :
( ( A @ empty )
=> ( ( A @ relation_rng @ relation )
& ( A @ relation_rng @ empty ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc8_relat_1) ).
thf(102,plain,
! [A: $i] :
( ( A @ empty )
=> ( ( A @ relation_rng @ relation )
& ( A @ relation_rng @ empty ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[19]) ).
thf(103,plain,
! [A: $i] :
( ( ( A @ relation_rng @ relation )
| ~ ( A @ empty ) )
& ( ( A @ relation_rng @ empty )
| ~ ( A @ empty ) ) ),
inference(cnf,[status(esa)],[102]) ).
thf(104,plain,
! [A: $i] :
( ( A @ relation_rng @ empty )
| ~ ( A @ empty ) ),
inference(cnfConj,[status(thm)],[103]) ).
thf(1734,plain,
! [A: $i] :
( ( ( empty_set @ empty )
!= ( A @ empty ) )
| ( A @ relation_rng @ empty )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[75,104]) ).
thf(1735,plain,
! [A: $i] :
( ( ( empty_set @ empty )
!= ( A @ empty ) )
| ( A @ relation_rng @ empty ) ),
inference(simp,[status(thm)],[1734]) ).
thf(1736,plain,
empty_set @ relation_rng @ empty,
inference(pattern_uni,[status(thm)],[1735:[bind(A,$thf( empty_set ))]]) ).
thf(1762,plain,
! [A: $i] :
( ( ( empty_set @ relation_rng @ empty )
!= ( A @ empty ) )
| ~ $true
| ( A = empty_set ) ),
inference(paramod_ordered,[status(thm)],[1736,84]) ).
thf(1763,plain,
! [A: $i] :
( ( ( empty_set @ relation_rng @ empty )
!= ( A @ empty ) )
| ( A = empty_set ) ),
inference(simp,[status(thm)],[1762]) ).
thf(1764,plain,
( ( empty_set @ relation_rng )
= empty_set ),
inference(pattern_uni,[status(thm)],[1763:[bind(A,$thf( empty_set @ relation_rng ))]]) ).
thf(100,plain,
sk9 @ relation,
inference(cnfConj,[status(thm)],[99]) ).
thf(2656,plain,
! [A: $i] :
( ( ( sk9 @ relation )
!= ( A @ relation ) )
| ~ ( A @ relation_rng @ empty )
| ~ $true
| ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[100,113]) ).
thf(2657,plain,
! [A: $i] :
( ( ( sk9 @ relation )
!= ( A @ relation ) )
| ~ ( A @ relation_rng @ empty )
| ( A @ empty ) ),
inference(simp,[status(thm)],[2656]) ).
thf(2658,plain,
( ~ ( sk9 @ relation_rng @ empty )
| ( sk9 @ empty ) ),
inference(pattern_uni,[status(thm)],[2657:[bind(A,$thf( sk9 ))]]) ).
thf(4100,plain,
( ( ( sk9 @ relation_rng @ empty )
!= ( empty_set @ empty ) )
| ~ $true
| ( sk9 @ empty ) ),
inference(paramod_ordered,[status(thm)],[75,2658]) ).
thf(4101,plain,
( ( ( sk9 @ relation_rng @ empty )
!= ( empty_set @ empty ) )
| ( sk9 @ empty ) ),
inference(simp,[status(thm)],[4100]) ).
thf(4104,plain,
( ( ( sk9 @ relation_rng )
!= empty_set )
| ( sk9 @ empty ) ),
inference(simp,[status(thm)],[4101]) ).
thf(7600,plain,
( ( ( sk9 @ relation_rng )
!= ( empty_set @ relation_rng ) )
| ( empty_set != empty_set )
| ( sk9 @ empty ) ),
inference(paramod_ordered,[status(thm)],[1764,4104]) ).
thf(7601,plain,
( ( ( sk9 @ relation_rng )
!= ( empty_set @ relation_rng ) )
| ( sk9 @ empty ) ),
inference(simp,[status(thm)],[7600]) ).
thf(7652,plain,
( ( sk9 != empty_set )
| ( sk9 @ empty ) ),
inference(simp,[status(thm)],[7601]) ).
thf(26,axiom,
? [A: $i] :
( ( A @ relation )
& ~ ( A @ empty ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc2_relat_1) ).
thf(122,plain,
? [A: $i] :
( ( A @ relation )
& ~ ( A @ empty ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[26]) ).
thf(123,plain,
( ( sk10 @ relation )
& ~ ( sk10 @ empty ) ),
inference(cnf,[status(esa)],[122]) ).
thf(124,plain,
~ ( sk10 @ empty ),
inference(cnfConj,[status(thm)],[123]) ).
thf(8223,plain,
( ( ( sk10 @ empty )
!= ( sk9 @ empty ) )
| ~ $true
| ( sk9 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[7652,124]) ).
thf(8224,plain,
( ( ( sk10 @ empty )
!= ( sk9 @ empty ) )
| ( sk9 != empty_set ) ),
inference(simp,[status(thm)],[8223]) ).
thf(8288,plain,
( ( sk10 != sk9 )
| ( sk9 != empty_set ) ),
inference(simp,[status(thm)],[8224]) ).
thf(231,plain,
( ( ( sk10 @ empty )
!= ( empty_set @ empty ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[75,124]) ).
thf(232,plain,
( ( sk10 @ empty )
!= ( empty_set @ empty ) ),
inference(simp,[status(thm)],[231]) ).
thf(234,plain,
sk10 != empty_set,
inference(simp,[status(thm)],[232]) ).
thf(1,conjecture,
! [A: $i,B: $i] :
( ( ( B @ function )
& ( B @ relation ) )
=> ! [C: $i] :
( ( ( C @ function )
& ( C @ relation ) )
=> ( ( ( ( B @ ( C @ relation_composition ) )
= B )
& ( B @ one_to_one )
& ( A @ ( C @ relation_rng @ subset ) )
& ( ( C @ relation_dom )
= A )
& ( ( B @ relation_dom )
= A ) )
=> ( C
= ( A @ identity_relation ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t50_funct_1) ).
thf(2,negated_conjecture,
~ ! [A: $i,B: $i] :
( ( ( B @ function )
& ( B @ relation ) )
=> ! [C: $i] :
( ( ( C @ function )
& ( C @ relation ) )
=> ( ( ( ( B @ ( C @ relation_composition ) )
= B )
& ( B @ one_to_one )
& ( A @ ( C @ relation_rng @ subset ) )
& ( ( C @ relation_dom )
= A )
& ( ( B @ relation_dom )
= A ) )
=> ( C
= ( A @ identity_relation ) ) ) ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(42,plain,
~ ! [A: $i,B: $i] :
( ( ( B @ function )
& ( B @ relation ) )
=> ! [C: $i] :
( ( ( C @ function )
& ( C @ relation ) )
=> ( ( ( ( B @ ( C @ relation_composition ) )
= B )
& ( B @ one_to_one )
& ( A @ ( C @ relation_rng @ subset ) )
& ( ( C @ relation_dom )
= A )
& ( ( B @ relation_dom )
= A ) )
=> ( C
= ( A @ identity_relation ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(43,plain,
( ( sk3
!= ( sk1 @ identity_relation ) )
& ( ( sk2 @ ( sk3 @ relation_composition ) )
= sk2 )
& ( sk2 @ one_to_one )
& ( sk1 @ ( sk3 @ relation_rng @ subset ) )
& ( ( sk3 @ relation_dom )
= sk1 )
& ( ( sk2 @ relation_dom )
= sk1 )
& ( sk3 @ function )
& ( sk3 @ relation )
& ( sk2 @ function )
& ( sk2 @ relation ) ),
inference(cnf,[status(esa)],[42]) ).
thf(49,plain,
sk2 @ relation,
inference(cnfConj,[status(thm)],[43]) ).
thf(2639,plain,
! [A: $i] :
( ( ( sk2 @ relation )
!= ( A @ relation ) )
| ~ ( A @ relation_rng @ empty )
| ~ $true
| ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[49,113]) ).
thf(2640,plain,
! [A: $i] :
( ( ( sk2 @ relation )
!= ( A @ relation ) )
| ~ ( A @ relation_rng @ empty )
| ( A @ empty ) ),
inference(simp,[status(thm)],[2639]) ).
thf(2641,plain,
( ~ ( sk2 @ relation_rng @ empty )
| ( sk2 @ empty ) ),
inference(pattern_uni,[status(thm)],[2640:[bind(A,$thf( sk2 ))]]) ).
thf(3185,plain,
( ( ( sk2 @ relation_rng @ empty )
!= ( empty_set @ empty ) )
| ~ $true
| ( sk2 @ empty ) ),
inference(paramod_ordered,[status(thm)],[75,2641]) ).
thf(3186,plain,
( ( ( sk2 @ relation_rng @ empty )
!= ( empty_set @ empty ) )
| ( sk2 @ empty ) ),
inference(simp,[status(thm)],[3185]) ).
thf(3190,plain,
( ( ( sk2 @ relation_rng )
!= empty_set )
| ( sk2 @ empty ) ),
inference(simp,[status(thm)],[3186]) ).
thf(3487,plain,
( ( ( sk2 @ relation_rng )
!= ( empty_set @ relation_rng ) )
| ( empty_set != empty_set )
| ( sk2 @ empty ) ),
inference(paramod_ordered,[status(thm)],[1764,3190]) ).
thf(3488,plain,
( ( ( sk2 @ relation_rng )
!= ( empty_set @ relation_rng ) )
| ( sk2 @ empty ) ),
inference(simp,[status(thm)],[3487]) ).
thf(3525,plain,
( ( sk2 != empty_set )
| ( sk2 @ empty ) ),
inference(simp,[status(thm)],[3488]) ).
thf(105,plain,
! [A: $i] :
( ( A @ relation_rng @ relation )
| ~ ( A @ empty ) ),
inference(cnfConj,[status(thm)],[103]) ).
thf(3785,plain,
! [A: $i] :
( ( ( sk2 @ empty )
!= ( A @ empty ) )
| ( A @ relation_rng @ relation )
| ~ $true
| ( sk2 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[3525,105]) ).
thf(3786,plain,
! [A: $i] :
( ( ( sk2 @ empty )
!= ( A @ empty ) )
| ( A @ relation_rng @ relation )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[3785]) ).
thf(3787,plain,
( ( sk2 @ relation_rng @ relation )
| ( sk2 != empty_set ) ),
inference(pattern_uni,[status(thm)],[3786:[bind(A,$thf( sk2 ))]]) ).
thf(5776,plain,
! [A: $i] :
( ( A != sk2 )
| ( sk2 @ relation_rng @ relation )
| ( empty_set != empty_set )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[84,3787]) ).
thf(5777,plain,
! [A: $i] :
( ( A != sk2 )
| ( sk2 @ relation_rng @ relation )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[5776]) ).
thf(5778,plain,
( ( sk2 @ relation_rng @ relation )
| ~ ( sk2 @ empty ) ),
inference(pattern_uni,[status(thm)],[5777:[bind(A,$thf( sk2 ))]]) ).
thf(44,plain,
( ( sk3 @ relation_dom )
= sk1 ),
inference(cnfConj,[status(thm)],[43]) ).
thf(56,plain,
( ( sk3 @ relation_dom )
= sk1 ),
inference(lifteq,[status(thm)],[44]) ).
thf(1128,plain,
! [A: $i] :
( ( A != sk3 )
| ( ( empty_set @ relation_dom )
= sk1 )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[84,56]) ).
thf(1129,plain,
( ( ( empty_set @ relation_dom )
= sk1 )
| ~ ( sk3 @ empty ) ),
inference(pattern_uni,[status(thm)],[1128:[bind(A,$thf( sk3 ))]]) ).
thf(2250,plain,
( ( ( sk3 @ empty )
!= ( empty_set @ empty ) )
| ( ( empty_set @ relation_dom )
= sk1 )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[75,1129]) ).
thf(2251,plain,
( ( ( sk3 @ empty )
!= ( empty_set @ empty ) )
| ( ( empty_set @ relation_dom )
= sk1 ) ),
inference(simp,[status(thm)],[2250]) ).
thf(2256,plain,
( ( sk3 != empty_set )
| ( ( empty_set @ relation_dom )
= sk1 ) ),
inference(simp,[status(thm)],[2251]) ).
thf(38,axiom,
! [A: $i] :
( ( A @ empty )
=> ( ( A @ relation_dom @ relation )
& ( A @ relation_dom @ empty ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc7_relat_1) ).
thf(188,plain,
! [A: $i] :
( ( A @ empty )
=> ( ( A @ relation_dom @ relation )
& ( A @ relation_dom @ empty ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[38]) ).
thf(189,plain,
! [A: $i] :
( ( ( A @ relation_dom @ relation )
| ~ ( A @ empty ) )
& ( ( A @ relation_dom @ empty )
| ~ ( A @ empty ) ) ),
inference(cnf,[status(esa)],[188]) ).
thf(190,plain,
! [A: $i] :
( ( A @ relation_dom @ empty )
| ~ ( A @ empty ) ),
inference(cnfConj,[status(thm)],[189]) ).
thf(9281,plain,
! [A: $i] :
( ( ( empty_set @ empty )
!= ( A @ empty ) )
| ( A @ relation_dom @ empty )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[75,190]) ).
thf(9282,plain,
! [A: $i] :
( ( ( empty_set @ empty )
!= ( A @ empty ) )
| ( A @ relation_dom @ empty ) ),
inference(simp,[status(thm)],[9281]) ).
thf(9283,plain,
empty_set @ relation_dom @ empty,
inference(pattern_uni,[status(thm)],[9282:[bind(A,$thf( empty_set ))]]) ).
thf(9375,plain,
! [A: $i] :
( ( ( empty_set @ relation_dom @ empty )
!= ( A @ empty ) )
| ~ $true
| ( A = empty_set ) ),
inference(paramod_ordered,[status(thm)],[9283,84]) ).
thf(9376,plain,
! [A: $i] :
( ( ( empty_set @ relation_dom @ empty )
!= ( A @ empty ) )
| ( A = empty_set ) ),
inference(simp,[status(thm)],[9375]) ).
thf(9377,plain,
( ( empty_set @ relation_dom )
= empty_set ),
inference(pattern_uni,[status(thm)],[9376:[bind(A,$thf( empty_set @ relation_dom ))]]) ).
thf(9621,plain,
( ( sk3 != empty_set )
| ( sk1 = empty_set ) ),
inference(rewrite,[status(thm)],[2256,9377]) ).
thf(3435,plain,
! [A: $i] :
( ( ( sk2 @ empty )
!= ( A @ empty ) )
| ~ $true
| ( A = empty_set )
| ( ( sk2 @ relation_rng )
!= empty_set ) ),
inference(paramod_ordered,[status(thm)],[3190,84]) ).
thf(3436,plain,
! [A: $i] :
( ( ( sk2 @ empty )
!= ( A @ empty ) )
| ( A = empty_set )
| ( ( sk2 @ relation_rng )
!= empty_set ) ),
inference(simp,[status(thm)],[3435]) ).
thf(3437,plain,
( ( sk2 = empty_set )
| ( ( sk2 @ relation_rng )
!= empty_set ) ),
inference(pattern_uni,[status(thm)],[3436:[bind(A,$thf( sk2 ))]]) ).
thf(5263,plain,
! [A: $i] :
( ( A
!= ( sk2 @ relation_rng ) )
| ( sk2 = empty_set )
| ( empty_set != empty_set )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[84,3437]) ).
thf(5264,plain,
! [A: $i] :
( ( A
!= ( sk2 @ relation_rng ) )
| ( sk2 = empty_set )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[5263]) ).
thf(5265,plain,
( ( sk2 = empty_set )
| ~ ( sk2 @ relation_rng @ empty ) ),
inference(pattern_uni,[status(thm)],[5264:[bind(A,$thf( sk2 @ relation_rng ))]]) ).
thf(51,plain,
( ( sk2 @ relation_dom )
= sk1 ),
inference(cnfConj,[status(thm)],[43]) ).
thf(57,plain,
( ( sk2 @ relation_dom )
= sk1 ),
inference(lifteq,[status(thm)],[51]) ).
thf(1155,plain,
! [A: $i] :
( ( A != sk2 )
| ( ( empty_set @ relation_dom )
= sk1 )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[84,57]) ).
thf(1156,plain,
( ( ( empty_set @ relation_dom )
= sk1 )
| ~ ( sk2 @ empty ) ),
inference(pattern_uni,[status(thm)],[1155:[bind(A,$thf( sk2 ))]]) ).
thf(2530,plain,
( ( ( sk2 @ empty )
!= ( empty_set @ empty ) )
| ( ( empty_set @ relation_dom )
= sk1 )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[75,1156]) ).
thf(2531,plain,
( ( ( sk2 @ empty )
!= ( empty_set @ empty ) )
| ( ( empty_set @ relation_dom )
= sk1 ) ),
inference(simp,[status(thm)],[2530]) ).
thf(2541,plain,
( ( sk2 != empty_set )
| ( ( empty_set @ relation_dom )
= sk1 ) ),
inference(simp,[status(thm)],[2531]) ).
thf(9417,plain,
( ( ( empty_set @ relation_dom )
!= ( empty_set @ relation_dom ) )
| ( sk1 @ empty )
| ( sk2 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[2541,9283]) ).
thf(9418,plain,
( ( sk1 @ empty )
| ( sk2 != empty_set ) ),
inference(pattern_uni,[status(thm)],[9417:[]]) ).
thf(10080,plain,
( ( ( sk5 @ empty )
!= ( sk1 @ empty ) )
| ~ $true
| ( sk2 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[9418,74]) ).
thf(10081,plain,
( ( ( sk5 @ empty )
!= ( sk1 @ empty ) )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[10080]) ).
thf(10173,plain,
( ( sk5 != sk1 )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[10081]) ).
thf(10444,plain,
( ( sk2 != sk2 )
| ( sk5 != sk1 )
| ( empty_set != empty_set )
| ~ ( sk2 @ relation_rng @ empty ) ),
inference(paramod_ordered,[status(thm)],[5265,10173]) ).
thf(10445,plain,
( ( sk2 != sk2 )
| ( sk5 != sk1 )
| ~ ( sk2 @ relation_rng @ empty ) ),
inference(simp,[status(thm)],[10444]) ).
thf(10446,plain,
( ( sk5 != sk1 )
| ~ ( sk2 @ relation_rng @ empty ) ),
inference(pattern_uni,[status(thm)],[10445:[]]) ).
thf(21,axiom,
! [A: $i] :
( ( A @ empty )
=> ( A @ function ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc1_funct_1) ).
thf(110,plain,
! [A: $i] :
( ( A @ empty )
=> ( A @ function ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[21]) ).
thf(111,plain,
! [A: $i] :
( ( A @ function )
| ~ ( A @ empty ) ),
inference(cnf,[status(esa)],[110]) ).
thf(2549,plain,
! [A: $i] :
( ( ( empty_set @ empty )
!= ( A @ empty ) )
| ( A @ function )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[75,111]) ).
thf(2550,plain,
! [A: $i] :
( ( ( empty_set @ empty )
!= ( A @ empty ) )
| ( A @ function ) ),
inference(simp,[status(thm)],[2549]) ).
thf(2551,plain,
empty_set @ function,
inference(pattern_uni,[status(thm)],[2550:[bind(A,$thf( empty_set ))]]) ).
thf(39,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/sandbox/benchmark/theBenchmark.p',d5_funct_1) ).
thf(192,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)],[39]) ).
thf(193,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)],[192]) ).
thf(194,plain,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( F
= ( A @ relation_rng ) )
| ~ ( F @ ( A @ ( F @ sk19 ) @ in ) )
| ( F @ ( A @ sk17 ) )
| ~ ( A @ function )
| ~ ( A @ relation ) )
& ( ( F
= ( A @ relation_rng ) )
| ( ( A @ ( F @ sk19 ) )
= ( A @ ( F @ sk20 ) @ ( A @ apply ) ) )
| ( F @ ( A @ sk17 ) )
| ~ ( A @ function )
| ~ ( A @ relation ) )
& ( ( F
= ( A @ relation_rng ) )
| ( A @ relation_dom @ ( A @ ( F @ sk20 ) @ in ) )
| ( F @ ( A @ sk17 ) )
| ~ ( A @ function )
| ~ ( A @ relation ) )
& ( ( F
= ( A @ relation_rng ) )
| ~ ( F @ ( A @ sk17 ) )
| ( ( A @ ( F @ sk18 ) )
!= ( G @ ( A @ apply ) ) )
| ~ ( A @ relation_dom @ ( G @ in ) )
| ~ ( A @ function )
| ~ ( A @ relation ) )
& ( ( F
= ( A @ relation_rng ) )
| ~ ( F @ ( A @ sk17 ) )
| ( F @ ( A @ ( F @ sk18 ) @ 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 @ sk16 ) ) @ ( A @ apply ) ) )
| ~ ( B @ ( C @ in ) )
| ( B
!= ( A @ relation_rng ) )
| ~ ( A @ function )
| ~ ( A @ relation ) )
& ( ( A @ relation_dom @ ( A @ ( B @ ( C @ sk16 ) ) @ in ) )
| ~ ( B @ ( C @ in ) )
| ( B
!= ( A @ relation_rng ) )
| ~ ( A @ function )
| ~ ( A @ relation ) ) ),
inference(cnf,[status(esa)],[193]) ).
thf(201,plain,
! [B: $i,A: $i] :
( ( B
= ( A @ relation_rng ) )
| ( A @ relation_dom @ ( A @ ( B @ sk20 ) @ in ) )
| ( B @ ( A @ sk17 ) )
| ~ ( A @ function )
| ~ ( A @ relation ) ),
inference(cnfConj,[status(thm)],[194]) ).
thf(207,plain,
! [B: $i,A: $i] :
( ( A @ relation_dom @ ( A @ ( B @ sk20 ) @ in ) )
| ( B @ ( A @ sk17 ) )
| ~ ( A @ function )
| ~ ( A @ relation )
| ( B
= ( A @ relation_rng ) ) ),
inference(lifteq,[status(thm)],[201]) ).
thf(208,plain,
! [B: $i,A: $i] :
( ( A @ relation_dom @ ( A @ ( B @ sk20 ) @ in ) )
| ( B @ ( A @ sk17 ) )
| ~ ( A @ function )
| ~ ( A @ relation )
| ( B
= ( A @ relation_rng ) ) ),
inference(simp,[status(thm)],[207]) ).
thf(11291,plain,
! [B: $i,A: $i] :
( ( ( empty_set @ function )
!= ( A @ function ) )
| ( A @ relation_dom @ ( A @ ( B @ sk20 ) @ in ) )
| ( B @ ( A @ sk17 ) )
| ~ $true
| ~ ( A @ relation )
| ( B
= ( A @ relation_rng ) ) ),
inference(paramod_ordered,[status(thm)],[2551,208]) ).
thf(11292,plain,
! [B: $i,A: $i] :
( ( ( empty_set @ function )
!= ( A @ function ) )
| ( A @ relation_dom @ ( A @ ( B @ sk20 ) @ in ) )
| ( B @ ( A @ sk17 ) )
| ~ ( A @ relation )
| ( B
= ( A @ relation_rng ) ) ),
inference(simp,[status(thm)],[11291]) ).
thf(11293,plain,
! [A: $i] :
( ( empty_set @ relation_dom @ ( empty_set @ ( A @ sk20 ) @ in ) )
| ( A @ ( empty_set @ sk17 ) )
| ~ ( empty_set @ relation )
| ( A
= ( empty_set @ relation_rng ) ) ),
inference(pattern_uni,[status(thm)],[11292:[bind(A,$thf( empty_set ))]]) ).
thf(11705,plain,
! [A: $i] :
( ( empty_set @ relation_dom @ ( empty_set @ ( A @ sk20 ) @ in ) )
| ( A @ ( empty_set @ sk17 ) )
| ~ ( empty_set @ relation )
| ( A
= ( empty_set @ relation_rng ) ) ),
inference(simp,[status(thm)],[11293]) ).
thf(27,axiom,
( ( empty_set @ relation_empty_yielding )
& ( empty_set @ relation )
& ( empty_set @ empty ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc12_relat_1) ).
thf(126,plain,
( ( empty_set @ relation_empty_yielding )
& ( empty_set @ relation )
& ( empty_set @ empty ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[27]) ).
thf(127,plain,
( ( empty_set @ relation_empty_yielding )
& ( empty_set @ relation )
& ( empty_set @ empty ) ),
inference(cnf,[status(esa)],[126]) ).
thf(129,plain,
empty_set @ relation,
inference(cnfConj,[status(thm)],[127]) ).
thf(11957,plain,
! [A: $i] :
( ( empty_set @ ( empty_set @ ( A @ sk20 ) @ in ) )
| ( A @ ( empty_set @ sk17 ) )
| ~ $true
| ( A = empty_set ) ),
inference(rewrite,[status(thm)],[11705,129,9377,1764]) ).
thf(11958,plain,
! [A: $i] :
( ( empty_set @ ( empty_set @ ( A @ sk20 ) @ in ) )
| ( A @ ( empty_set @ sk17 ) )
| ( A = empty_set ) ),
inference(simp,[status(thm)],[11957]) ).
thf(229,plain,
( ( ( sk5 @ empty )
!= ( empty_set @ empty ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[75,74]) ).
thf(230,plain,
( ( sk5 @ empty )
!= ( empty_set @ empty ) ),
inference(simp,[status(thm)],[229]) ).
thf(233,plain,
sk5 != empty_set,
inference(simp,[status(thm)],[230]) ).
thf(12235,plain,
! [A: $i] :
( ( A != sk5 )
| ( empty_set != empty_set )
| ( empty_set @ ( empty_set @ ( A @ sk20 ) @ in ) )
| ( A @ ( empty_set @ sk17 ) ) ),
inference(paramod_ordered,[status(thm)],[11958,233]) ).
thf(12236,plain,
! [A: $i] :
( ( A != sk5 )
| ( empty_set @ ( empty_set @ ( A @ sk20 ) @ in ) )
| ( A @ ( empty_set @ sk17 ) ) ),
inference(simp,[status(thm)],[12235]) ).
thf(12237,plain,
( ( empty_set @ ( empty_set @ ( sk5 @ sk20 ) @ in ) )
| ( sk5 @ ( empty_set @ sk17 ) ) ),
inference(pattern_uni,[status(thm)],[12236:[bind(A,$thf( sk5 ))]]) ).
thf(576,plain,
! [B: $i,A: $i] :
( ( ( empty_set @ empty )
!= ( B @ empty ) )
| ~ $true
| ~ ( B @ ( A @ in ) ) ),
inference(paramod_ordered,[status(thm)],[75,69]) ).
thf(577,plain,
! [B: $i,A: $i] :
( ( ( empty_set @ empty )
!= ( B @ empty ) )
| ~ ( B @ ( A @ in ) ) ),
inference(simp,[status(thm)],[576]) ).
thf(578,plain,
! [A: $i] :
~ ( empty_set @ ( A @ in ) ),
inference(pattern_uni,[status(thm)],[577:[bind(A,$thf( A )),bind(B,$thf( empty_set ))]]) ).
thf(15142,plain,
( $false
| ( sk5 @ ( empty_set @ sk17 ) ) ),
inference(rewrite,[status(thm)],[12237,578]) ).
thf(15143,plain,
sk5 @ ( empty_set @ sk17 ),
inference(simp,[status(thm)],[15142]) ).
thf(9151,plain,
! [A: $i] :
( ( ( sk2 @ relation_dom )
!= ( A @ relation_dom ) )
| ( sk1 @ empty )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[57,190]) ).
thf(9152,plain,
( ( sk1 @ empty )
| ~ ( sk2 @ empty ) ),
inference(pattern_uni,[status(thm)],[9151:[bind(A,$thf( sk2 ))]]) ).
thf(25,axiom,
! [A: $i] :
( ( A @ empty )
=> ( A @ relation ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc1_relat_1) ).
thf(120,plain,
! [A: $i] :
( ( A @ empty )
=> ( A @ relation ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[25]) ).
thf(12117,plain,
! [A: $i] :
( ( A != sk2 )
| ( empty_set != empty_set )
| ( sk2 @ empty )
| ( empty_set @ ( empty_set @ ( A @ sk20 ) @ in ) )
| ( A @ ( empty_set @ sk17 ) ) ),
inference(paramod_ordered,[status(thm)],[11958,3525]) ).
thf(12118,plain,
! [A: $i] :
( ( A != sk2 )
| ( sk2 @ empty )
| ( empty_set @ ( empty_set @ ( A @ sk20 ) @ in ) )
| ( A @ ( empty_set @ sk17 ) ) ),
inference(simp,[status(thm)],[12117]) ).
thf(12119,plain,
( ( sk2 @ empty )
| ( empty_set @ ( empty_set @ ( sk2 @ sk20 ) @ in ) )
| ( sk2 @ ( empty_set @ sk17 ) ) ),
inference(pattern_uni,[status(thm)],[12118:[bind(A,$thf( sk2 ))]]) ).
thf(21206,plain,
( ( sk2 @ empty )
| $false
| ( sk2 @ ( empty_set @ sk17 ) ) ),
inference(rewrite,[status(thm)],[12119,578]) ).
thf(21207,plain,
( ( sk2 @ empty )
| ( sk2 @ ( empty_set @ sk17 ) ) ),
inference(simp,[status(thm)],[21206]) ).
thf(3479,plain,
( ( ( sk10 @ empty )
!= ( sk2 @ empty ) )
| ~ $true
| ( ( sk2 @ relation_rng )
!= empty_set ) ),
inference(paramod_ordered,[status(thm)],[3190,124]) ).
thf(3480,plain,
( ( ( sk10 @ empty )
!= ( sk2 @ empty ) )
| ( ( sk2 @ relation_rng )
!= empty_set ) ),
inference(simp,[status(thm)],[3479]) ).
thf(3537,plain,
( ( sk10 != sk2 )
| ( ( sk2 @ relation_rng )
!= empty_set ) ),
inference(simp,[status(thm)],[3480]) ).
thf(5667,plain,
! [A: $i] :
( ( A
!= ( sk2 @ relation_rng ) )
| ( sk10 != sk2 )
| ( empty_set != empty_set )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[84,3537]) ).
thf(5668,plain,
! [A: $i] :
( ( A
!= ( sk2 @ relation_rng ) )
| ( sk10 != sk2 )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[5667]) ).
thf(5669,plain,
( ( sk10 != sk2 )
| ~ ( sk2 @ relation_rng @ empty ) ),
inference(pattern_uni,[status(thm)],[5668:[bind(A,$thf( sk2 @ relation_rng ))]]) ).
thf(40,axiom,
! [A: $i] :
( ( ( A @ relation )
& ~ ( A @ empty ) )
=> ~ ( A @ relation_dom @ empty ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc5_relat_1) ).
thf(219,plain,
! [A: $i] :
( ( ( A @ relation )
& ~ ( A @ empty ) )
=> ~ ( A @ relation_dom @ empty ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[40]) ).
thf(220,plain,
! [A: $i] :
( ~ ( A @ relation_dom @ empty )
| ~ ( A @ relation )
| ( A @ empty ) ),
inference(cnf,[status(esa)],[219]) ).
thf(17227,plain,
! [A: $i] :
( ( ( sk2 @ relation )
!= ( A @ relation ) )
| ~ ( A @ relation_dom @ empty )
| ~ $true
| ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[49,220]) ).
thf(17228,plain,
! [A: $i] :
( ( ( sk2 @ relation )
!= ( A @ relation ) )
| ~ ( A @ relation_dom @ empty )
| ( A @ empty ) ),
inference(simp,[status(thm)],[17227]) ).
thf(17229,plain,
( ~ ( sk2 @ relation_dom @ empty )
| ( sk2 @ empty ) ),
inference(pattern_uni,[status(thm)],[17228:[bind(A,$thf( sk2 ))]]) ).
thf(35289,plain,
( ~ ( sk1 @ empty )
| ( sk2 @ empty ) ),
inference(rewrite,[status(thm)],[17229,57]) ).
thf(10447,plain,
! [A: $i] :
( ( A != sk2 )
| ( sk5 != sk1 )
| ( empty_set != empty_set )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[84,10173]) ).
thf(10448,plain,
! [A: $i] :
( ( A != sk2 )
| ( sk5 != sk1 )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[10447]) ).
thf(10449,plain,
( ( sk5 != sk1 )
| ~ ( sk2 @ empty ) ),
inference(pattern_uni,[status(thm)],[10448:[bind(A,$thf( sk2 ))]]) ).
thf(35525,plain,
( ( ( sk2 @ empty )
!= ( sk2 @ empty ) )
| ( sk5 != sk1 )
| ~ $true
| ~ ( sk1 @ empty ) ),
inference(paramod_ordered,[status(thm)],[35289,10449]) ).
thf(35526,plain,
( ( ( sk2 @ empty )
!= ( sk2 @ empty ) )
| ( sk5 != sk1 )
| ~ ( sk1 @ empty ) ),
inference(simp,[status(thm)],[35525]) ).
thf(35527,plain,
( ( sk5 != sk1 )
| ~ ( sk1 @ empty ) ),
inference(pattern_uni,[status(thm)],[35526:[]]) ).
thf(9459,plain,
( ( ( empty_set @ relation_dom )
!= ( empty_set @ relation_dom ) )
| ( sk1 @ empty )
| ( sk3 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[2256,9283]) ).
thf(9460,plain,
( ( sk1 @ empty )
| ( sk3 != empty_set ) ),
inference(pattern_uni,[status(thm)],[9459:[]]) ).
thf(9620,plain,
( ( sk2 != empty_set )
| ( sk1 = empty_set ) ),
inference(rewrite,[status(thm)],[2541,9377]) ).
thf(13743,plain,
! [A: $i] :
( ( A != sk2 )
| ( empty_set != empty_set )
| ( sk1 = empty_set )
| ( empty_set @ ( empty_set @ ( A @ sk20 ) @ in ) )
| ( A @ ( empty_set @ sk17 ) ) ),
inference(paramod_ordered,[status(thm)],[11958,9620]) ).
thf(13744,plain,
! [A: $i] :
( ( A != sk2 )
| ( sk1 = empty_set )
| ( empty_set @ ( empty_set @ ( A @ sk20 ) @ in ) )
| ( A @ ( empty_set @ sk17 ) ) ),
inference(simp,[status(thm)],[13743]) ).
thf(13745,plain,
( ( sk1 = empty_set )
| ( empty_set @ ( empty_set @ ( sk2 @ sk20 ) @ in ) )
| ( sk2 @ ( empty_set @ sk17 ) ) ),
inference(pattern_uni,[status(thm)],[13744:[bind(A,$thf( sk2 ))]]) ).
thf(33939,plain,
( ( sk1 = empty_set )
| $false
| ( sk2 @ ( empty_set @ sk17 ) ) ),
inference(rewrite,[status(thm)],[13745,578]) ).
thf(33940,plain,
( ( sk1 = empty_set )
| ( sk2 @ ( empty_set @ sk17 ) ) ),
inference(simp,[status(thm)],[33939]) ).
thf(35344,plain,
! [A: $i] :
( ( ( sk2 @ empty )
!= ( A @ empty ) )
| ~ $true
| ( A = empty_set )
| ~ ( sk1 @ empty ) ),
inference(paramod_ordered,[status(thm)],[35289,84]) ).
thf(35345,plain,
! [A: $i] :
( ( ( sk2 @ empty )
!= ( A @ empty ) )
| ( A = empty_set )
| ~ ( sk1 @ empty ) ),
inference(simp,[status(thm)],[35344]) ).
thf(35346,plain,
( ( sk2 = empty_set )
| ~ ( sk1 @ empty ) ),
inference(pattern_uni,[status(thm)],[35345:[bind(A,$thf( sk2 ))]]) ).
thf(37085,plain,
( ( ( sk1 @ empty )
!= ( empty_set @ empty ) )
| ( sk2 = empty_set )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[75,35346]) ).
thf(37086,plain,
( ( ( sk1 @ empty )
!= ( empty_set @ empty ) )
| ( sk2 = empty_set ) ),
inference(simp,[status(thm)],[37085]) ).
thf(37145,plain,
( ( sk1 != empty_set )
| ( sk2 = empty_set ) ),
inference(simp,[status(thm)],[37086]) ).
thf(39323,plain,
( ( sk1 != sk1 )
| ( empty_set != empty_set )
| ( sk2 = empty_set )
| ( sk2 @ ( empty_set @ sk17 ) ) ),
inference(paramod_ordered,[status(thm)],[33940,37145]) ).
thf(39324,plain,
( ( sk1 != sk1 )
| ( sk2 = empty_set )
| ( sk2 @ ( empty_set @ sk17 ) ) ),
inference(simp,[status(thm)],[39323]) ).
thf(39325,plain,
( ( sk2 = empty_set )
| ( sk2 @ ( empty_set @ sk17 ) ) ),
inference(pattern_uni,[status(thm)],[39324:[]]) ).
thf(31,axiom,
! [A: $i] :
( ( ( A @ function )
& ( A @ relation ) )
=> ( ( A @ one_to_one )
<=> ! [B: $i,C: $i] :
( ( ( ( B @ ( A @ apply ) )
= ( C @ ( A @ apply ) ) )
& ( A @ relation_dom @ ( C @ in ) )
& ( A @ relation_dom @ ( B @ in ) ) )
=> ( B = C ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d8_funct_1) ).
thf(140,plain,
! [A: $i] :
( ( ( A @ function )
& ( A @ relation ) )
=> ( ( ! [B: $i,C: $i] :
( ( ( ( B @ ( A @ apply ) )
= ( C @ ( A @ apply ) ) )
& ( A @ relation_dom @ ( C @ in ) )
& ( A @ relation_dom @ ( B @ in ) ) )
=> ( B = C ) )
=> ( A @ one_to_one ) )
& ( ( A @ one_to_one )
=> ! [B: $i,C: $i] :
( ( ( ( B @ ( A @ apply ) )
= ( C @ ( A @ apply ) ) )
& ( A @ relation_dom @ ( C @ in ) )
& ( A @ relation_dom @ ( B @ in ) ) )
=> ( B = C ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[31]) ).
thf(141,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ one_to_one )
| ( ( A @ sk12 )
!= ( A @ sk13 ) )
| ~ ( A @ function )
| ~ ( A @ relation ) )
& ( ( A @ one_to_one )
| ( ( A @ sk12 @ ( A @ apply ) )
= ( A @ sk13 @ ( A @ apply ) ) )
| ~ ( A @ function )
| ~ ( A @ relation ) )
& ( ( A @ one_to_one )
| ( A @ relation_dom @ ( A @ sk13 @ in ) )
| ~ ( A @ function )
| ~ ( A @ relation ) )
& ( ( A @ one_to_one )
| ( A @ relation_dom @ ( A @ sk12 @ in ) )
| ~ ( A @ function )
| ~ ( A @ relation ) )
& ( ( B = C )
| ( ( B @ ( A @ apply ) )
!= ( C @ ( A @ apply ) ) )
| ~ ( A @ relation_dom @ ( C @ in ) )
| ~ ( A @ relation_dom @ ( B @ in ) )
| ~ ( A @ one_to_one )
| ~ ( A @ function )
| ~ ( A @ relation ) ) ),
inference(cnf,[status(esa)],[140]) ).
thf(142,plain,
! [A: $i] :
( ( A @ one_to_one )
| ( A @ relation_dom @ ( A @ sk13 @ in ) )
| ~ ( A @ function )
| ~ ( A @ relation ) ),
inference(cnfConj,[status(thm)],[141]) ).
thf(16,axiom,
! [A: $i] :
? [B: $i] :
( ( B @ empty )
& ( A @ powerset @ ( B @ element ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc2_subset_1) ).
thf(92,plain,
! [A: $i] :
? [B: $i] :
( ( B @ empty )
& ( A @ powerset @ ( B @ element ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[16]) ).
thf(93,plain,
! [A: $i] :
( ( A @ sk7 @ empty )
& ( A @ powerset @ ( A @ sk7 @ element ) ) ),
inference(cnf,[status(esa)],[92]) ).
thf(95,plain,
! [A: $i] : ( A @ sk7 @ empty ),
inference(cnfConj,[status(thm)],[93]) ).
thf(1286,plain,
! [B: $i,A: $i] :
( ( ( A @ sk7 @ empty )
!= ( B @ empty ) )
| ~ $true
| ( B = empty_set ) ),
inference(paramod_ordered,[status(thm)],[95,84]) ).
thf(1287,plain,
! [B: $i,A: $i] :
( ( ( A @ sk7 @ empty )
!= ( B @ empty ) )
| ( B = empty_set ) ),
inference(simp,[status(thm)],[1286]) ).
thf(1288,plain,
! [A: $i] :
( ( A @ sk7 )
= empty_set ),
inference(pattern_uni,[status(thm)],[1287:[bind(A,$thf( C )),bind(B,$thf( C @ sk7 ))]]) ).
thf(1342,plain,
! [A: $i] :
( ( A @ sk7 )
= empty_set ),
inference(simp,[status(thm)],[1288]) ).
thf(32,axiom,
! [A: $i,B: $i] :
( ( B @ powerset @ ( A @ element ) )
<=> ( B @ ( A @ subset ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t3_subset) ).
thf(150,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)],[32]) ).
thf(151,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)],[150]) ).
thf(152,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)],[151]) ).
thf(153,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ subset ) )
| ~ ( B @ powerset @ ( A @ element ) ) ),
inference(cnfConj,[status(thm)],[152]) ).
thf(3810,plain,
! [A: $i] :
( ( ( sk2 @ empty )
!= ( A @ empty ) )
| ( A @ relation_rng @ empty )
| ~ $true
| ( sk2 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[3525,104]) ).
thf(3811,plain,
! [A: $i] :
( ( ( sk2 @ empty )
!= ( A @ empty ) )
| ( A @ relation_rng @ empty )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[3810]) ).
thf(3812,plain,
( ( sk2 @ relation_rng @ empty )
| ( sk2 != empty_set ) ),
inference(pattern_uni,[status(thm)],[3811:[bind(A,$thf( sk2 ))]]) ).
thf(5978,plain,
( ( ( sk2 @ relation_rng @ empty )
!= ( sk10 @ empty ) )
| ~ $true
| ( sk2 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[3812,124]) ).
thf(5979,plain,
( ( ( sk2 @ relation_rng @ empty )
!= ( sk10 @ empty ) )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[5978]) ).
thf(6046,plain,
( ( ( sk2 @ relation_rng )
!= sk10 )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[5979]) ).
thf(48,plain,
sk3 @ relation,
inference(cnfConj,[status(thm)],[43]) ).
thf(2645,plain,
! [A: $i] :
( ( ( sk3 @ relation )
!= ( A @ relation ) )
| ~ ( A @ relation_rng @ empty )
| ~ $true
| ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[48,113]) ).
thf(2646,plain,
! [A: $i] :
( ( ( sk3 @ relation )
!= ( A @ relation ) )
| ~ ( A @ relation_rng @ empty )
| ( A @ empty ) ),
inference(simp,[status(thm)],[2645]) ).
thf(2647,plain,
( ~ ( sk3 @ relation_rng @ empty )
| ( sk3 @ empty ) ),
inference(pattern_uni,[status(thm)],[2646:[bind(A,$thf( sk3 ))]]) ).
thf(3214,plain,
( ( ( sk3 @ relation_rng @ empty )
!= ( empty_set @ empty ) )
| ~ $true
| ( sk3 @ empty ) ),
inference(paramod_ordered,[status(thm)],[75,2647]) ).
thf(3215,plain,
( ( ( sk3 @ relation_rng @ empty )
!= ( empty_set @ empty ) )
| ( sk3 @ empty ) ),
inference(simp,[status(thm)],[3214]) ).
thf(3220,plain,
( ( ( sk3 @ relation_rng )
!= empty_set )
| ( sk3 @ empty ) ),
inference(simp,[status(thm)],[3215]) ).
thf(4256,plain,
( ( ( sk3 @ relation_rng )
!= ( empty_set @ relation_rng ) )
| ( empty_set != empty_set )
| ( sk3 @ empty ) ),
inference(paramod_ordered,[status(thm)],[1764,3220]) ).
thf(4257,plain,
( ( ( sk3 @ relation_rng )
!= ( empty_set @ relation_rng ) )
| ( sk3 @ empty ) ),
inference(simp,[status(thm)],[4256]) ).
thf(4314,plain,
( ( sk3 != empty_set )
| ( sk3 @ empty ) ),
inference(simp,[status(thm)],[4257]) ).
thf(4405,plain,
! [A: $i] :
( ( ( sk3 @ empty )
!= ( A @ empty ) )
| ( A @ relation_rng @ empty )
| ~ $true
| ( sk3 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[4314,104]) ).
thf(4406,plain,
! [A: $i] :
( ( ( sk3 @ empty )
!= ( A @ empty ) )
| ( A @ relation_rng @ empty )
| ( sk3 != empty_set ) ),
inference(simp,[status(thm)],[4405]) ).
thf(4407,plain,
( ( sk3 @ relation_rng @ empty )
| ( sk3 != empty_set ) ),
inference(pattern_uni,[status(thm)],[4406:[bind(A,$thf( sk3 ))]]) ).
thf(7791,plain,
! [A: $i] :
( ( ( sk3 @ relation_rng @ empty )
!= ( A @ empty ) )
| ~ $true
| ( A = empty_set )
| ( sk3 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[4407,84]) ).
thf(7792,plain,
! [A: $i] :
( ( ( sk3 @ relation_rng @ empty )
!= ( A @ empty ) )
| ( A = empty_set )
| ( sk3 != empty_set ) ),
inference(simp,[status(thm)],[7791]) ).
thf(7793,plain,
( ( ( sk3 @ relation_rng )
= empty_set )
| ( sk3 != empty_set ) ),
inference(pattern_uni,[status(thm)],[7792:[bind(A,$thf( sk3 @ relation_rng ))]]) ).
thf(3780,plain,
( ( ( sk10 @ empty )
!= ( sk2 @ empty ) )
| ~ $true
| ( sk2 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[3525,124]) ).
thf(3781,plain,
( ( ( sk10 @ empty )
!= ( sk2 @ empty ) )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[3780]) ).
thf(3822,plain,
( ( sk10 != sk2 )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[3781]) ).
thf(3846,plain,
! [A: $i] :
( ( A != sk2 )
| ( sk10 != sk2 )
| ( empty_set != empty_set )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[84,3822]) ).
thf(3847,plain,
! [A: $i] :
( ( A != sk2 )
| ( sk10 != sk2 )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[3846]) ).
thf(3848,plain,
( ( sk10 != sk2 )
| ~ ( sk2 @ empty ) ),
inference(pattern_uni,[status(thm)],[3847:[bind(A,$thf( sk2 ))]]) ).
thf(37,axiom,
! [A: $i] :
( ( A @ identity_relation @ function )
& ( A @ identity_relation @ relation ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc2_funct_1) ).
thf(182,plain,
! [A: $i] :
( ( A @ identity_relation @ function )
& ( A @ identity_relation @ relation ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[37]) ).
thf(183,plain,
( ! [A: $i] : ( A @ identity_relation @ function )
& ! [A: $i] : ( A @ identity_relation @ relation ) ),
inference(miniscope,[status(thm)],[182]) ).
thf(184,plain,
! [B: $i,A: $i] :
( ( B @ identity_relation @ function )
& ( A @ identity_relation @ relation ) ),
inference(cnf,[status(esa)],[183]) ).
thf(185,plain,
! [A: $i] : ( A @ identity_relation @ relation ),
inference(cnfConj,[status(thm)],[184]) ).
thf(4204,plain,
! [A: $i] :
( ( ( sk3 @ empty )
!= ( A @ empty ) )
| ~ $true
| ( A = empty_set )
| ( ( sk3 @ relation_rng )
!= empty_set ) ),
inference(paramod_ordered,[status(thm)],[3220,84]) ).
thf(4205,plain,
! [A: $i] :
( ( ( sk3 @ empty )
!= ( A @ empty ) )
| ( A = empty_set )
| ( ( sk3 @ relation_rng )
!= empty_set ) ),
inference(simp,[status(thm)],[4204]) ).
thf(4206,plain,
( ( sk3 = empty_set )
| ( ( sk3 @ relation_rng )
!= empty_set ) ),
inference(pattern_uni,[status(thm)],[4205:[bind(A,$thf( sk3 ))]]) ).
thf(7016,plain,
! [A: $i] :
( ( A
!= ( sk3 @ relation_rng ) )
| ( sk3 = empty_set )
| ( empty_set != empty_set )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[84,4206]) ).
thf(7017,plain,
! [A: $i] :
( ( A
!= ( sk3 @ relation_rng ) )
| ( sk3 = empty_set )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[7016]) ).
thf(7018,plain,
( ( sk3 = empty_set )
| ~ ( sk3 @ relation_rng @ empty ) ),
inference(pattern_uni,[status(thm)],[7017:[bind(A,$thf( sk3 @ relation_rng ))]]) ).
thf(121,plain,
! [A: $i] :
( ( A @ relation )
| ~ ( A @ empty ) ),
inference(cnf,[status(esa)],[120]) ).
thf(9372,plain,
! [A: $i] :
( ( ( empty_set @ relation_dom @ empty )
!= ( A @ empty ) )
| ( A @ relation )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[9283,121]) ).
thf(9373,plain,
! [A: $i] :
( ( ( empty_set @ relation_dom @ empty )
!= ( A @ empty ) )
| ( A @ relation ) ),
inference(simp,[status(thm)],[9372]) ).
thf(9374,plain,
empty_set @ relation_dom @ relation,
inference(pattern_uni,[status(thm)],[9373:[bind(A,$thf( empty_set @ relation_dom ))]]) ).
thf(9608,plain,
( ( ( empty_set @ relation_dom )
!= ( empty_set @ relation_dom ) )
| ( sk1 @ relation )
| ~ ( sk3 @ empty ) ),
inference(paramod_ordered,[status(thm)],[1129,9374]) ).
thf(9609,plain,
( ( sk1 @ relation )
| ~ ( sk3 @ empty ) ),
inference(pattern_uni,[status(thm)],[9608:[]]) ).
thf(13624,plain,
( ( ( sk3 @ empty )
!= ( sk3 @ empty ) )
| ( sk1 @ relation )
| ~ $true
| ( ( sk3 @ relation_rng )
!= empty_set ) ),
inference(paramod_ordered,[status(thm)],[3220,9609]) ).
thf(13625,plain,
( ( ( sk3 @ empty )
!= ( sk3 @ empty ) )
| ( sk1 @ relation )
| ( ( sk3 @ relation_rng )
!= empty_set ) ),
inference(simp,[status(thm)],[13624]) ).
thf(13626,plain,
( ( sk1 @ relation )
| ( ( sk3 @ relation_rng )
!= empty_set ) ),
inference(pattern_uni,[status(thm)],[13625:[]]) ).
thf(5933,plain,
! [A: $i] :
( ( ( sk2 @ relation_rng @ empty )
!= ( A @ empty ) )
| ~ $true
| ( A = empty_set )
| ( sk2 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[3812,84]) ).
thf(5934,plain,
! [A: $i] :
( ( ( sk2 @ relation_rng @ empty )
!= ( A @ empty ) )
| ( A = empty_set )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[5933]) ).
thf(5935,plain,
( ( ( sk2 @ relation_rng )
= empty_set )
| ( sk2 != empty_set ) ),
inference(pattern_uni,[status(thm)],[5934:[bind(A,$thf( sk2 @ relation_rng ))]]) ).
thf(5936,plain,
! [A: $i] :
( ( A != sk2 )
| ( sk2 @ relation_rng @ empty )
| ( empty_set != empty_set )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[84,3812]) ).
thf(5937,plain,
! [A: $i] :
( ( A != sk2 )
| ( sk2 @ relation_rng @ empty )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[5936]) ).
thf(5938,plain,
( ( sk2 @ relation_rng @ empty )
| ~ ( sk2 @ empty ) ),
inference(pattern_uni,[status(thm)],[5937:[bind(A,$thf( sk2 ))]]) ).
thf(35312,plain,
( ( ( sk2 @ empty )
!= ( sk2 @ empty ) )
| ( sk10 != sk2 )
| ~ $true
| ~ ( sk1 @ empty ) ),
inference(paramod_ordered,[status(thm)],[35289,3848]) ).
thf(35313,plain,
( ( ( sk2 @ empty )
!= ( sk2 @ empty ) )
| ( sk10 != sk2 )
| ~ ( sk1 @ empty ) ),
inference(simp,[status(thm)],[35312]) ).
thf(35314,plain,
( ( sk10 != sk2 )
| ~ ( sk1 @ empty ) ),
inference(pattern_uni,[status(thm)],[35313:[]]) ).
thf(3962,plain,
! [A: $i] :
( ( ( sk11 @ relation )
!= ( A @ relation ) )
| ( A @ one_to_one )
| ( A @ relation_dom @ ( A @ sk13 @ in ) )
| ~ ( A @ function )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[138,142]) ).
thf(3963,plain,
! [A: $i] :
( ( ( sk11 @ relation )
!= ( A @ relation ) )
| ( A @ one_to_one )
| ( A @ relation_dom @ ( A @ sk13 @ in ) )
| ~ ( A @ function ) ),
inference(simp,[status(thm)],[3962]) ).
thf(3964,plain,
( ( sk11 @ one_to_one )
| ( sk11 @ relation_dom @ ( sk11 @ sk13 @ in ) )
| ~ ( sk11 @ function ) ),
inference(pattern_uni,[status(thm)],[3963:[bind(A,$thf( sk11 ))]]) ).
thf(139,plain,
sk11 @ function,
inference(cnfConj,[status(thm)],[137]) ).
thf(4116,plain,
( ( sk11 @ one_to_one )
| ( sk11 @ relation_dom @ ( sk11 @ sk13 @ in ) )
| ~ $true ),
inference(rewrite,[status(thm)],[3964,139]) ).
thf(4117,plain,
( ( sk11 @ one_to_one )
| ( sk11 @ relation_dom @ ( sk11 @ sk13 @ in ) ) ),
inference(simp,[status(thm)],[4116]) ).
thf(36,axiom,
! [A: $i,B: $i] :
( ( ( B @ function )
& ( B @ relation ) )
=> ( ( B
= ( A @ identity_relation ) )
<=> ( ! [C: $i] :
( ( A @ ( C @ in ) )
=> ( ( C @ ( B @ apply ) )
= C ) )
& ( ( B @ relation_dom )
= A ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t34_funct_1) ).
thf(168,plain,
! [A: $i,B: $i] :
( ( ( B @ function )
& ( B @ relation ) )
=> ( ( ( ! [C: $i] :
( ( A @ ( C @ in ) )
=> ( ( C @ ( B @ apply ) )
= C ) )
& ( ( B @ relation_dom )
= A ) )
=> ( B
= ( A @ identity_relation ) ) )
& ( ( B
= ( A @ identity_relation ) )
=> ( ! [C: $i] :
( ( A @ ( C @ in ) )
=> ( ( C @ ( B @ apply ) )
= C ) )
& ( ( B @ relation_dom )
= A ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[36]) ).
thf(169,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B
= ( A @ identity_relation ) )
| ( ( A @ ( B @ sk15 ) @ ( B @ apply ) )
!= ( A @ ( B @ sk15 ) ) )
| ( ( B @ relation_dom )
!= A )
| ~ ( B @ function )
| ~ ( B @ relation ) )
& ( ( B
= ( A @ identity_relation ) )
| ( A @ ( A @ ( B @ sk15 ) @ in ) )
| ( ( B @ relation_dom )
!= A )
| ~ ( B @ function )
| ~ ( B @ relation ) )
& ( ( ( C @ ( B @ apply ) )
= C )
| ~ ( A @ ( C @ in ) )
| ( B
!= ( A @ identity_relation ) )
| ~ ( B @ function )
| ~ ( B @ relation ) )
& ( ( ( B @ relation_dom )
= A )
| ( B
!= ( A @ identity_relation ) )
| ~ ( B @ function )
| ~ ( B @ relation ) ) ),
inference(cnf,[status(esa)],[168]) ).
thf(171,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ apply ) )
= C )
| ~ ( A @ ( C @ in ) )
| ( B
!= ( A @ identity_relation ) )
| ~ ( B @ function )
| ~ ( B @ relation ) ),
inference(cnfConj,[status(thm)],[169]) ).
thf(176,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( A @ ( C @ in ) )
| ~ ( B @ function )
| ~ ( B @ relation )
| ( ( C @ ( B @ apply ) )
= C )
| ( B
!= ( A @ identity_relation ) ) ),
inference(lifteq,[status(thm)],[171]) ).
thf(177,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ in ) )
| ~ ( A @ identity_relation @ function )
| ~ ( A @ identity_relation @ relation )
| ( ( B @ ( A @ identity_relation @ apply ) )
= B ) ),
inference(simp,[status(thm)],[176]) ).
thf(186,plain,
! [A: $i] : ( A @ identity_relation @ function ),
inference(cnfConj,[status(thm)],[184]) ).
thf(187,plain,
! [A: $i] : ( A @ identity_relation @ function ),
inference(simp,[status(thm)],[186]) ).
thf(7264,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ in ) )
| ~ $true
| ~ $true
| ( ( B @ ( A @ identity_relation @ apply ) )
= B ) ),
inference(rewrite,[status(thm)],[177,185,187]) ).
thf(7265,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ in ) )
| ( ( B @ ( A @ identity_relation @ apply ) )
= B ) ),
inference(simp,[status(thm)],[7264]) ).
thf(7309,plain,
! [B: $i,A: $i] :
( ( ( sk11 @ relation_dom @ ( sk11 @ sk13 @ in ) )
!= ( A @ ( B @ in ) ) )
| ~ $true
| ( ( B @ ( A @ identity_relation @ apply ) )
= B )
| ( sk11 @ one_to_one ) ),
inference(paramod_ordered,[status(thm)],[4117,7265]) ).
thf(7310,plain,
! [B: $i,A: $i] :
( ( ( sk11 @ relation_dom @ ( sk11 @ sk13 @ in ) )
!= ( A @ ( B @ in ) ) )
| ( ( B @ ( A @ identity_relation @ apply ) )
= B )
| ( sk11 @ one_to_one ) ),
inference(simp,[status(thm)],[7309]) ).
thf(7311,plain,
( ( ( sk11 @ sk13 @ ( sk11 @ relation_dom @ identity_relation @ apply ) )
= ( sk11 @ sk13 ) )
| ( sk11 @ one_to_one ) ),
inference(pattern_uni,[status(thm)],[7310:[bind(A,$thf( sk11 @ relation_dom )),bind(B,$thf( sk11 @ sk13 ))]]) ).
thf(52,plain,
sk1 @ ( sk3 @ relation_rng @ subset ),
inference(cnfConj,[status(thm)],[43]) ).
thf(154,plain,
! [B: $i,A: $i] :
( ( B @ powerset @ ( A @ element ) )
| ~ ( B @ ( A @ subset ) ) ),
inference(cnfConj,[status(thm)],[152]) ).
thf(155,plain,
! [B: $i,A: $i] :
( ( B @ powerset @ ( A @ element ) )
| ~ ( B @ ( A @ subset ) ) ),
inference(simp,[status(thm)],[154]) ).
thf(6103,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( sk3 @ relation_rng @ subset ) )
!= ( B @ ( A @ subset ) ) )
| ( B @ powerset @ ( A @ element ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[52,155]) ).
thf(6104,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( sk3 @ relation_rng @ subset ) )
!= ( B @ ( A @ subset ) ) )
| ( B @ powerset @ ( A @ element ) ) ),
inference(simp,[status(thm)],[6103]) ).
thf(6105,plain,
sk1 @ powerset @ ( sk3 @ relation_rng @ element ),
inference(pattern_uni,[status(thm)],[6104:[bind(A,$thf( sk3 @ relation_rng )),bind(B,$thf( sk1 ))]]) ).
thf(10,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ element ) )
=> ( ( B @ ( A @ in ) )
| ( B @ empty ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2_subset) ).
thf(76,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ element ) )
=> ( ( B @ ( A @ in ) )
| ( B @ empty ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).
thf(77,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ in ) )
| ( B @ empty )
| ~ ( B @ ( A @ element ) ) ),
inference(cnf,[status(esa)],[76]) ).
thf(6166,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk3 @ relation_rng @ element ) )
!= ( B @ ( A @ element ) ) )
| ( B @ ( A @ in ) )
| ( B @ empty )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[6105,77]) ).
thf(6167,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk3 @ relation_rng @ element ) )
!= ( B @ ( A @ element ) ) )
| ( B @ ( A @ in ) )
| ( B @ empty ) ),
inference(simp,[status(thm)],[6166]) ).
thf(6168,plain,
( ( sk1 @ powerset @ ( sk3 @ relation_rng @ in ) )
| ( sk1 @ powerset @ empty ) ),
inference(pattern_uni,[status(thm)],[6167:[bind(A,$thf( sk3 @ relation_rng )),bind(B,$thf( sk1 @ powerset ))]]) ).
thf(15,axiom,
! [A: $i] :
~ ( A @ powerset @ empty ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_subset_1) ).
thf(89,plain,
! [A: $i] :
~ ( A @ powerset @ empty ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[15]) ).
thf(90,plain,
~ ? [A: $i] : ( A @ powerset @ empty ),
inference(miniscope,[status(thm)],[89]) ).
thf(91,plain,
! [A: $i] :
~ ( A @ powerset @ empty ),
inference(cnf,[status(esa)],[90]) ).
thf(6234,plain,
( ( sk1 @ powerset @ ( sk3 @ relation_rng @ in ) )
| $false ),
inference(rewrite,[status(thm)],[6168,91]) ).
thf(6235,plain,
sk1 @ powerset @ ( sk3 @ relation_rng @ in ),
inference(simp,[status(thm)],[6234]) ).
thf(6275,plain,
! [A: $i] :
( ( ( sk1 @ powerset @ ( sk3 @ relation_rng @ in ) )
!= ( empty_set @ ( A @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[6235,578]) ).
thf(6276,plain,
! [A: $i] :
( ( sk1 @ powerset @ ( sk3 @ relation_rng @ in ) )
!= ( empty_set @ ( A @ in ) ) ),
inference(simp,[status(thm)],[6275]) ).
thf(6294,plain,
! [A: $i] :
( ( ( sk1 @ powerset )
!= empty_set )
| ( ( sk3 @ relation_rng )
!= A ) ),
inference(simp,[status(thm)],[6276]) ).
thf(6306,plain,
( ( sk1 @ powerset )
!= empty_set ),
inference(simp,[status(thm)],[6294]) ).
thf(9146,plain,
! [A: $i] :
( ( ( sk9 @ empty )
!= ( A @ empty ) )
| ( A @ relation_dom @ empty )
| ~ $true
| ( sk9 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[7652,190]) ).
thf(9147,plain,
! [A: $i] :
( ( ( sk9 @ empty )
!= ( A @ empty ) )
| ( A @ relation_dom @ empty )
| ( sk9 != empty_set ) ),
inference(simp,[status(thm)],[9146]) ).
thf(9148,plain,
( ( sk9 @ relation_dom @ empty )
| ( sk9 != empty_set ) ),
inference(pattern_uni,[status(thm)],[9147:[bind(A,$thf( sk9 ))]]) ).
thf(10953,plain,
( ( ( sk2 @ empty )
!= ( sk2 @ empty ) )
| ( sk5 != sk1 )
| ~ $true
| ( ( sk2 @ relation_rng )
!= empty_set ) ),
inference(paramod_ordered,[status(thm)],[3190,10449]) ).
thf(10954,plain,
( ( ( sk2 @ empty )
!= ( sk2 @ empty ) )
| ( sk5 != sk1 )
| ( ( sk2 @ relation_rng )
!= empty_set ) ),
inference(simp,[status(thm)],[10953]) ).
thf(10955,plain,
( ( sk5 != sk1 )
| ( ( sk2 @ relation_rng )
!= empty_set ) ),
inference(pattern_uni,[status(thm)],[10954:[]]) ).
thf(7835,plain,
( ( ( sk3 @ relation_rng @ empty )
!= ( sk10 @ empty ) )
| ~ $true
| ( sk3 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[4407,124]) ).
thf(7836,plain,
( ( ( sk3 @ relation_rng @ empty )
!= ( sk10 @ empty ) )
| ( sk3 != empty_set ) ),
inference(simp,[status(thm)],[7835]) ).
thf(7914,plain,
( ( ( sk3 @ relation_rng )
!= sk10 )
| ( sk3 != empty_set ) ),
inference(simp,[status(thm)],[7836]) ).
thf(36556,plain,
( ( ( sk1 @ empty )
!= ( empty_set @ empty ) )
| ( sk5 != sk1 )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[75,35527]) ).
thf(36557,plain,
( ( ( sk1 @ empty )
!= ( empty_set @ empty ) )
| ( sk5 != sk1 ) ),
inference(simp,[status(thm)],[36556]) ).
thf(36596,plain,
( ( sk1 != empty_set )
| ( sk5 != sk1 ) ),
inference(simp,[status(thm)],[36557]) ).
thf(11,axiom,
! [A: $i] :
( ~ ( A @ empty )
=> ? [B: $i] :
( ~ ( B @ empty )
& ( A @ powerset @ ( B @ element ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc1_subset_1) ).
thf(78,plain,
! [A: $i] :
( ~ ( A @ empty )
=> ? [B: $i] :
( ~ ( B @ empty )
& ( A @ powerset @ ( B @ element ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[11]) ).
thf(79,plain,
! [A: $i] :
( ( ~ ( A @ sk6 @ empty )
| ( A @ empty ) )
& ( ( A @ powerset @ ( A @ sk6 @ element ) )
| ( A @ empty ) ) ),
inference(cnf,[status(esa)],[78]) ).
thf(80,plain,
! [A: $i] :
( ( A @ powerset @ ( A @ sk6 @ element ) )
| ( A @ empty ) ),
inference(cnfConj,[status(thm)],[79]) ).
thf(5872,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ sk6 @ element ) )
!= ( C @ powerset @ ( B @ element ) ) )
| ( C @ ( B @ subset ) )
| ~ $true
| ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[80,153]) ).
thf(5873,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ sk6 @ element ) )
!= ( C @ powerset @ ( B @ element ) ) )
| ( C @ ( B @ subset ) )
| ( A @ empty ) ),
inference(simp,[status(thm)],[5872]) ).
thf(5874,plain,
! [A: $i] :
( ( A @ ( A @ sk6 @ subset ) )
| ( A @ empty ) ),
inference(pattern_uni,[status(thm)],[5873:[bind(A,$thf( D )),bind(B,$thf( D @ sk6 )),bind(C,$thf( D ))]]) ).
thf(5883,plain,
! [A: $i] :
( ( A @ ( A @ sk6 @ subset ) )
| ( A @ empty ) ),
inference(simp,[status(thm)],[5874]) ).
thf(46,plain,
sk2 @ one_to_one,
inference(cnfConj,[status(thm)],[43]) ).
thf(1149,plain,
! [A: $i] :
( ( A != sk2 )
| ( empty_set @ one_to_one )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[84,46]) ).
thf(1150,plain,
( ( empty_set @ one_to_one )
| ~ ( sk2 @ empty ) ),
inference(pattern_uni,[status(thm)],[1149:[bind(A,$thf( sk2 ))]]) ).
thf(35447,plain,
( ( ( sk2 @ empty )
!= ( sk2 @ empty ) )
| ( empty_set @ one_to_one )
| ~ $true
| ~ ( sk1 @ empty ) ),
inference(paramod_ordered,[status(thm)],[35289,1150]) ).
thf(35448,plain,
( ( ( sk2 @ empty )
!= ( sk2 @ empty ) )
| ( empty_set @ one_to_one )
| ~ ( sk1 @ empty ) ),
inference(simp,[status(thm)],[35447]) ).
thf(35449,plain,
( ( empty_set @ one_to_one )
| ~ ( sk1 @ empty ) ),
inference(pattern_uni,[status(thm)],[35448:[]]) ).
thf(37742,plain,
( ( ( sk1 @ empty )
!= ( empty_set @ empty ) )
| ( empty_set @ one_to_one )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[75,35449]) ).
thf(37743,plain,
( ( ( sk1 @ empty )
!= ( empty_set @ empty ) )
| ( empty_set @ one_to_one ) ),
inference(simp,[status(thm)],[37742]) ).
thf(37769,plain,
( ( sk1 != empty_set )
| ( empty_set @ one_to_one ) ),
inference(simp,[status(thm)],[37743]) ).
thf(125,plain,
sk10 @ relation,
inference(cnfConj,[status(thm)],[123]) ).
thf(4375,plain,
( ( ( sk10 @ empty )
!= ( sk3 @ empty ) )
| ~ $true
| ( sk3 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[4314,124]) ).
thf(4376,plain,
( ( ( sk10 @ empty )
!= ( sk3 @ empty ) )
| ( sk3 != empty_set ) ),
inference(simp,[status(thm)],[4375]) ).
thf(4428,plain,
( ( sk10 != sk3 )
| ( sk3 != empty_set ) ),
inference(simp,[status(thm)],[4376]) ).
thf(7593,plain,
( ( ( sk10 @ empty )
!= ( sk9 @ empty ) )
| ~ $true
| ( ( sk9 @ relation_rng )
!= empty_set ) ),
inference(paramod_ordered,[status(thm)],[4104,124]) ).
thf(7594,plain,
( ( ( sk10 @ empty )
!= ( sk9 @ empty ) )
| ( ( sk9 @ relation_rng )
!= empty_set ) ),
inference(simp,[status(thm)],[7593]) ).
thf(7665,plain,
( ( sk10 != sk9 )
| ( ( sk9 @ relation_rng )
!= empty_set ) ),
inference(simp,[status(thm)],[7594]) ).
thf(10096,plain,
( ( ( sk10 @ empty )
!= ( sk1 @ empty ) )
| ~ $true
| ( sk2 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[9418,124]) ).
thf(10097,plain,
( ( ( sk10 @ empty )
!= ( sk1 @ empty ) )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[10096]) ).
thf(10188,plain,
( ( sk10 != sk1 )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[10097]) ).
thf(10467,plain,
( ( sk2 != sk2 )
| ( sk10 != sk1 )
| ( empty_set != empty_set )
| ~ ( sk2 @ relation_rng @ empty ) ),
inference(paramod_ordered,[status(thm)],[5265,10188]) ).
thf(10468,plain,
( ( sk2 != sk2 )
| ( sk10 != sk1 )
| ~ ( sk2 @ relation_rng @ empty ) ),
inference(simp,[status(thm)],[10467]) ).
thf(10469,plain,
( ( sk10 != sk1 )
| ~ ( sk2 @ relation_rng @ empty ) ),
inference(pattern_uni,[status(thm)],[10468:[]]) ).
thf(4249,plain,
( ( ( sk10 @ empty )
!= ( sk3 @ empty ) )
| ~ $true
| ( ( sk3 @ relation_rng )
!= empty_set ) ),
inference(paramod_ordered,[status(thm)],[3220,124]) ).
thf(4250,plain,
( ( ( sk10 @ empty )
!= ( sk3 @ empty ) )
| ( ( sk3 @ relation_rng )
!= empty_set ) ),
inference(simp,[status(thm)],[4249]) ).
thf(4315,plain,
( ( sk10 != sk3 )
| ( ( sk3 @ relation_rng )
!= empty_set ) ),
inference(simp,[status(thm)],[4250]) ).
thf(6641,plain,
! [A: $i] :
( ( A
!= ( sk3 @ relation_rng ) )
| ( sk10 != sk3 )
| ( empty_set != empty_set )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[84,4315]) ).
thf(6642,plain,
! [A: $i] :
( ( A
!= ( sk3 @ relation_rng ) )
| ( sk10 != sk3 )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[6641]) ).
thf(6643,plain,
( ( sk10 != sk3 )
| ~ ( sk3 @ relation_rng @ empty ) ),
inference(pattern_uni,[status(thm)],[6642:[bind(A,$thf( sk3 @ relation_rng ))]]) ).
thf(11976,plain,
! [A: $i] :
( ( A != sk10 )
| ( empty_set != empty_set )
| ( empty_set @ ( empty_set @ ( A @ sk20 ) @ in ) )
| ( A @ ( empty_set @ sk17 ) ) ),
inference(paramod_ordered,[status(thm)],[11958,234]) ).
thf(11977,plain,
! [A: $i] :
( ( A != sk10 )
| ( empty_set @ ( empty_set @ ( A @ sk20 ) @ in ) )
| ( A @ ( empty_set @ sk17 ) ) ),
inference(simp,[status(thm)],[11976]) ).
thf(11978,plain,
( ( empty_set @ ( empty_set @ ( sk10 @ sk20 ) @ in ) )
| ( sk10 @ ( empty_set @ sk17 ) ) ),
inference(pattern_uni,[status(thm)],[11977:[bind(A,$thf( sk10 ))]]) ).
thf(13703,plain,
( $false
| ( sk10 @ ( empty_set @ sk17 ) ) ),
inference(rewrite,[status(thm)],[11978,578]) ).
thf(13704,plain,
sk10 @ ( empty_set @ sk17 ),
inference(simp,[status(thm)],[13703]) ).
thf(8209,plain,
( ( ( sk9 @ empty )
!= ( sk5 @ empty ) )
| ~ $true
| ( sk9 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[7652,74]) ).
thf(8210,plain,
( ( ( sk9 @ empty )
!= ( sk5 @ empty ) )
| ( sk9 != empty_set ) ),
inference(simp,[status(thm)],[8209]) ).
thf(8278,plain,
( ( sk9 != sk5 )
| ( sk9 != empty_set ) ),
inference(simp,[status(thm)],[8210]) ).
thf(6239,plain,
! [A: $i] :
( ( ( sk1 @ powerset @ ( sk3 @ relation_rng @ in ) )
!= ( A @ ( A @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[6235,1586]) ).
thf(6240,plain,
! [A: $i] :
( ( sk1 @ powerset @ ( sk3 @ relation_rng @ in ) )
!= ( A @ ( A @ in ) ) ),
inference(simp,[status(thm)],[6239]) ).
thf(6298,plain,
! [A: $i] :
( ( ( sk1 @ powerset )
!= A )
| ( ( sk3 @ relation_rng )
!= A ) ),
inference(simp,[status(thm)],[6240]) ).
thf(6310,plain,
( ( sk1 @ powerset )
!= ( sk3 @ relation_rng ) ),
inference(simp,[status(thm)],[6298]) ).
thf(17,axiom,
! [A: $i] :
? [B: $i] : ( A @ ( B @ element ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_m1_subset_1) ).
thf(96,plain,
! [A: $i] :
? [B: $i] : ( A @ ( B @ element ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[17]) ).
thf(97,plain,
! [A: $i] : ( A @ ( A @ sk8 @ element ) ),
inference(cnf,[status(esa)],[96]) ).
thf(785,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ sk8 @ element ) )
!= ( C @ ( B @ element ) ) )
| ( C @ ( B @ in ) )
| ( C @ empty )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[97,77]) ).
thf(786,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ sk8 @ element ) )
!= ( C @ ( B @ element ) ) )
| ( C @ ( B @ in ) )
| ( C @ empty ) ),
inference(simp,[status(thm)],[785]) ).
thf(787,plain,
! [A: $i] :
( ( A @ ( A @ sk8 @ in ) )
| ( A @ empty ) ),
inference(pattern_uni,[status(thm)],[786:[bind(A,$thf( D )),bind(B,$thf( D @ sk8 )),bind(C,$thf( D ))]]) ).
thf(791,plain,
! [A: $i] :
( ( A @ ( A @ sk8 @ in ) )
| ( A @ empty ) ),
inference(simp,[status(thm)],[787]) ).
thf(7,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ in ) )
=> ( B @ ( A @ element ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_subset) ).
thf(70,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ in ) )
=> ( B @ ( A @ element ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(71,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ element ) )
| ~ ( B @ ( A @ in ) ) ),
inference(cnf,[status(esa)],[70]) ).
thf(942,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ sk8 @ in ) )
!= ( C @ ( B @ in ) ) )
| ( C @ ( B @ element ) )
| ~ $true
| ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[791,71]) ).
thf(943,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ sk8 @ in ) )
!= ( C @ ( B @ in ) ) )
| ( C @ ( B @ element ) )
| ( A @ empty ) ),
inference(simp,[status(thm)],[942]) ).
thf(944,plain,
! [A: $i] :
( ( A @ ( A @ sk8 @ element ) )
| ( A @ empty ) ),
inference(pattern_uni,[status(thm)],[943:[bind(A,$thf( D )),bind(B,$thf( D @ sk8 )),bind(C,$thf( D ))]]) ).
thf(957,plain,
! [A: $i] :
( ( A @ ( A @ sk8 @ element ) )
| ( A @ empty ) ),
inference(simp,[status(thm)],[944]) ).
thf(1102,plain,
! [B: $i,A: $i] :
( ( A
!= ( B @ sk8 ) )
| ( B @ ( empty_set @ element ) )
| ( B @ empty )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[84,957]) ).
thf(1103,plain,
! [A: $i] :
( ( A @ ( empty_set @ element ) )
| ( A @ empty )
| ~ ( A @ sk8 @ empty ) ),
inference(pattern_uni,[status(thm)],[1102:[bind(A,$thf( C @ sk8 )),bind(B,$thf( C ))]]) ).
thf(1347,plain,
! [A: $i] :
( ( A @ ( empty_set @ element ) )
| ( A @ empty )
| ~ ( A @ sk8 @ empty ) ),
inference(simp,[status(thm)],[1103]) ).
thf(5027,plain,
( ( ( sk11 @ relation_rng )
!= ( empty_set @ relation_rng ) )
| ( empty_set != empty_set )
| ( sk11 @ empty ) ),
inference(paramod_ordered,[status(thm)],[1764,3160]) ).
thf(5028,plain,
( ( ( sk11 @ relation_rng )
!= ( empty_set @ relation_rng ) )
| ( sk11 @ empty ) ),
inference(simp,[status(thm)],[5027]) ).
thf(5068,plain,
( ( sk11 != empty_set )
| ( sk11 @ empty ) ),
inference(simp,[status(thm)],[5028]) ).
thf(12690,plain,
! [A: $i] :
( ( A != sk11 )
| ( empty_set != empty_set )
| ( sk11 @ empty )
| ( empty_set @ ( empty_set @ ( A @ sk20 ) @ in ) )
| ( A @ ( empty_set @ sk17 ) ) ),
inference(paramod_ordered,[status(thm)],[11958,5068]) ).
thf(12691,plain,
! [A: $i] :
( ( A != sk11 )
| ( sk11 @ empty )
| ( empty_set @ ( empty_set @ ( A @ sk20 ) @ in ) )
| ( A @ ( empty_set @ sk17 ) ) ),
inference(simp,[status(thm)],[12690]) ).
thf(12692,plain,
( ( sk11 @ empty )
| ( empty_set @ ( empty_set @ ( sk11 @ sk20 ) @ in ) )
| ( sk11 @ ( empty_set @ sk17 ) ) ),
inference(pattern_uni,[status(thm)],[12691:[bind(A,$thf( sk11 ))]]) ).
thf(26268,plain,
( ( sk11 @ empty )
| $false
| ( sk11 @ ( empty_set @ sk17 ) ) ),
inference(rewrite,[status(thm)],[12692,578]) ).
thf(26269,plain,
( ( sk11 @ empty )
| ( sk11 @ ( empty_set @ sk17 ) ) ),
inference(simp,[status(thm)],[26268]) ).
thf(2620,plain,
! [A: $i] :
( ( ( sk10 @ relation )
!= ( A @ relation ) )
| ~ ( A @ relation_rng @ empty )
| ~ $true
| ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[125,113]) ).
thf(2621,plain,
! [A: $i] :
( ( ( sk10 @ relation )
!= ( A @ relation ) )
| ~ ( A @ relation_rng @ empty )
| ( A @ empty ) ),
inference(simp,[status(thm)],[2620]) ).
thf(2622,plain,
( ~ ( sk10 @ relation_rng @ empty )
| ( sk10 @ empty ) ),
inference(pattern_uni,[status(thm)],[2621:[bind(A,$thf( sk10 ))]]) ).
thf(3327,plain,
( ~ ( sk10 @ relation_rng @ empty )
| $false ),
inference(rewrite,[status(thm)],[2622,124]) ).
thf(3328,plain,
~ ( sk10 @ relation_rng @ empty ),
inference(simp,[status(thm)],[3327]) ).
thf(3813,plain,
( ( ( sk10 @ relation_rng @ empty )
!= ( sk2 @ empty ) )
| ~ $true
| ( sk2 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[3525,3328]) ).
thf(3814,plain,
( ( ( sk10 @ relation_rng @ empty )
!= ( sk2 @ empty ) )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[3813]) ).
thf(3835,plain,
( ( ( sk10 @ relation_rng )
!= sk2 )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[3814]) ).
thf(3766,plain,
( ( ( sk5 @ empty )
!= ( sk2 @ empty ) )
| ~ $true
| ( sk2 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[3525,74]) ).
thf(3767,plain,
( ( ( sk5 @ empty )
!= ( sk2 @ empty ) )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[3766]) ).
thf(3832,plain,
( ( sk5 != sk2 )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[3767]) ).
thf(3864,plain,
! [A: $i] :
( ( A != sk2 )
| ( sk5 != sk2 )
| ( empty_set != empty_set )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[84,3832]) ).
thf(3865,plain,
! [A: $i] :
( ( A != sk2 )
| ( sk5 != sk2 )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[3864]) ).
thf(3866,plain,
( ( sk5 != sk2 )
| ~ ( sk2 @ empty ) ),
inference(pattern_uni,[status(thm)],[3865:[bind(A,$thf( sk2 ))]]) ).
thf(35596,plain,
( ( ( sk1 @ empty )
!= ( empty_set @ empty ) )
| ~ $true
| ( sk2 @ empty ) ),
inference(paramod_ordered,[status(thm)],[75,35289]) ).
thf(35597,plain,
( ( ( sk1 @ empty )
!= ( empty_set @ empty ) )
| ( sk2 @ empty ) ),
inference(simp,[status(thm)],[35596]) ).
thf(35742,plain,
( ( sk1 != empty_set )
| ( sk2 @ empty ) ),
inference(simp,[status(thm)],[35597]) ).
thf(6023,plain,
! [A: $i] :
( ( ( sk2 @ relation_rng @ empty )
!= ( A @ empty ) )
| ( A @ function )
| ~ $true
| ( sk2 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[3812,111]) ).
thf(6024,plain,
! [A: $i] :
( ( ( sk2 @ relation_rng @ empty )
!= ( A @ empty ) )
| ( A @ function )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[6023]) ).
thf(6025,plain,
( ( sk2 @ relation_rng @ function )
| ( sk2 != empty_set ) ),
inference(pattern_uni,[status(thm)],[6024:[bind(A,$thf( sk2 @ relation_rng ))]]) ).
thf(195,plain,
! [C: $i,B: $i,A: $i] :
( ( B
= ( A @ relation_rng ) )
| ~ ( B @ ( A @ sk17 ) )
| ( ( A @ ( B @ sk18 ) )
!= ( C @ ( A @ apply ) ) )
| ~ ( A @ relation_dom @ ( C @ in ) )
| ~ ( A @ function )
| ~ ( A @ relation ) ),
inference(cnfConj,[status(thm)],[194]) ).
thf(215,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( B @ ( A @ sk17 ) )
| ~ ( A @ relation_dom @ ( C @ in ) )
| ~ ( A @ function )
| ~ ( A @ relation )
| ( B
= ( A @ relation_rng ) )
| ( ( A @ ( B @ sk18 ) )
!= ( C @ ( A @ apply ) ) ) ),
inference(lifteq,[status(thm)],[195]) ).
thf(216,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( B @ ( A @ sk17 ) )
| ~ ( A @ relation_dom @ ( C @ in ) )
| ~ ( A @ function )
| ~ ( A @ relation )
| ( B
= ( A @ relation_rng ) )
| ( ( A @ ( B @ sk18 ) )
!= ( C @ ( A @ apply ) ) ) ),
inference(simp,[status(thm)],[215]) ).
thf(35,axiom,
! [A: $i,B: $i] :
( ( ( B @ relation )
& ( A @ empty ) )
=> ( ( A @ ( B @ relation_composition ) @ relation )
& ( A @ ( B @ relation_composition ) @ empty ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc10_relat_1) ).
thf(164,plain,
! [A: $i,B: $i] :
( ( ( B @ relation )
& ( A @ empty ) )
=> ( ( A @ ( B @ relation_composition ) @ relation )
& ( A @ ( B @ relation_composition ) @ empty ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[35]) ).
thf(4130,plain,
( ( ( sk11 @ relation_dom )
!= ( sk2 @ relation_dom ) )
| ( sk11 @ one_to_one )
| ( sk1 @ ( sk11 @ sk13 @ in ) ) ),
inference(paramod_ordered,[status(thm)],[57,4117]) ).
thf(4173,plain,
( ( sk11 != sk2 )
| ( sk11 @ one_to_one )
| ( sk1 @ ( sk11 @ sk13 @ in ) ) ),
inference(simp,[status(thm)],[4130]) ).
thf(4410,plain,
( ( ( sk10 @ relation_rng @ empty )
!= ( sk3 @ empty ) )
| ~ $true
| ( sk3 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[4314,3328]) ).
thf(4411,plain,
( ( ( sk10 @ relation_rng @ empty )
!= ( sk3 @ empty ) )
| ( sk3 != empty_set ) ),
inference(simp,[status(thm)],[4410]) ).
thf(4420,plain,
( ( ( sk10 @ relation_rng )
!= sk3 )
| ( sk3 != empty_set ) ),
inference(simp,[status(thm)],[4411]) ).
thf(6668,plain,
! [A: $i] :
( ( A != sk3 )
| ( ( sk10 @ relation_rng )
!= sk3 )
| ( empty_set != empty_set )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[84,4420]) ).
thf(6669,plain,
! [A: $i] :
( ( A != sk3 )
| ( ( sk10 @ relation_rng )
!= sk3 )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[6668]) ).
thf(6670,plain,
( ( ( sk10 @ relation_rng )
!= sk3 )
| ~ ( sk3 @ empty ) ),
inference(pattern_uni,[status(thm)],[6669:[bind(A,$thf( sk3 ))]]) ).
thf(9606,plain,
( ( ( empty_set @ relation_dom )
!= ( empty_set @ relation_dom ) )
| ( sk1 @ relation )
| ~ ( sk2 @ empty ) ),
inference(paramod_ordered,[status(thm)],[1156,9374]) ).
thf(9607,plain,
( ( sk1 @ relation )
| ~ ( sk2 @ empty ) ),
inference(pattern_uni,[status(thm)],[9606:[]]) ).
thf(13536,plain,
( ( ( sk2 @ empty )
!= ( sk2 @ empty ) )
| ( sk1 @ relation )
| ~ $true
| ( ( sk2 @ relation_rng )
!= empty_set ) ),
inference(paramod_ordered,[status(thm)],[3190,9607]) ).
thf(13537,plain,
( ( ( sk2 @ empty )
!= ( sk2 @ empty ) )
| ( sk1 @ relation )
| ( ( sk2 @ relation_rng )
!= empty_set ) ),
inference(simp,[status(thm)],[13536]) ).
thf(13538,plain,
( ( sk1 @ relation )
| ( ( sk2 @ relation_rng )
!= empty_set ) ),
inference(pattern_uni,[status(thm)],[13537:[]]) ).
thf(4,axiom,
? [A: $i] : ( A @ empty ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc1_xboole_0) ).
thf(62,plain,
? [A: $i] : ( A @ empty ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(63,plain,
sk4 @ empty,
inference(cnf,[status(esa)],[62]) ).
thf(1281,plain,
! [A: $i] :
( ( ( sk4 @ empty )
!= ( A @ empty ) )
| ~ $true
| ( A = empty_set ) ),
inference(paramod_ordered,[status(thm)],[63,84]) ).
thf(1282,plain,
! [A: $i] :
( ( ( sk4 @ empty )
!= ( A @ empty ) )
| ( A = empty_set ) ),
inference(simp,[status(thm)],[1281]) ).
thf(1283,plain,
sk4 = empty_set,
inference(pattern_uni,[status(thm)],[1282:[bind(A,$thf( sk4 ))]]) ).
thf(13756,plain,
! [A: $i] :
( ( A != sk3 )
| ( empty_set != empty_set )
| ( sk1 = empty_set )
| ( empty_set @ ( empty_set @ ( A @ sk20 ) @ in ) )
| ( A @ ( empty_set @ sk17 ) ) ),
inference(paramod_ordered,[status(thm)],[11958,9621]) ).
thf(13757,plain,
! [A: $i] :
( ( A != sk3 )
| ( sk1 = empty_set )
| ( empty_set @ ( empty_set @ ( A @ sk20 ) @ in ) )
| ( A @ ( empty_set @ sk17 ) ) ),
inference(simp,[status(thm)],[13756]) ).
thf(13758,plain,
( ( sk1 = empty_set )
| ( empty_set @ ( empty_set @ ( sk3 @ sk20 ) @ in ) )
| ( sk3 @ ( empty_set @ sk17 ) ) ),
inference(pattern_uni,[status(thm)],[13757:[bind(A,$thf( sk3 ))]]) ).
thf(38510,plain,
( ( sk1 = empty_set )
| $false
| ( sk3 @ ( empty_set @ sk17 ) ) ),
inference(rewrite,[status(thm)],[13758,578]) ).
thf(38511,plain,
( ( sk1 = empty_set )
| ( sk3 @ ( empty_set @ sk17 ) ) ),
inference(simp,[status(thm)],[38510]) ).
thf(39462,plain,
( ( sk1 != sk1 )
| ( empty_set != empty_set )
| ( sk2 = empty_set )
| ( sk3 @ ( empty_set @ sk17 ) ) ),
inference(paramod_ordered,[status(thm)],[38511,37145]) ).
thf(39463,plain,
( ( sk1 != sk1 )
| ( sk2 = empty_set )
| ( sk3 @ ( empty_set @ sk17 ) ) ),
inference(simp,[status(thm)],[39462]) ).
thf(39464,plain,
( ( sk2 = empty_set )
| ( sk3 @ ( empty_set @ sk17 ) ) ),
inference(pattern_uni,[status(thm)],[39463:[]]) ).
thf(45,plain,
( sk3
!= ( sk1 @ identity_relation ) ),
inference(cnfConj,[status(thm)],[43]) ).
thf(55,plain,
( ( sk1 @ identity_relation )
!= sk3 ),
inference(lifteq,[status(thm)],[45]) ).
thf(1301,plain,
! [A: $i] :
( ( A != sk1 )
| ( ( empty_set @ identity_relation )
!= sk3 )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[84,55]) ).
thf(1302,plain,
( ( ( empty_set @ identity_relation )
!= sk3 )
| ~ ( sk1 @ empty ) ),
inference(pattern_uni,[status(thm)],[1301:[bind(A,$thf( sk1 ))]]) ).
thf(172,plain,
! [B: $i,A: $i] :
( ( B
= ( A @ identity_relation ) )
| ( A @ ( A @ ( B @ sk15 ) @ in ) )
| ( ( B @ relation_dom )
!= A )
| ~ ( B @ function )
| ~ ( B @ relation ) ),
inference(cnfConj,[status(thm)],[169]) ).
thf(178,plain,
! [B: $i,A: $i] :
( ( A @ ( A @ ( B @ sk15 ) @ in ) )
| ~ ( B @ function )
| ~ ( B @ relation )
| ( B
= ( A @ identity_relation ) )
| ( ( B @ relation_dom )
!= A ) ),
inference(lifteq,[status(thm)],[172]) ).
thf(179,plain,
! [A: $i] :
( ( A @ relation_dom @ ( A @ relation_dom @ ( A @ sk15 ) @ in ) )
| ~ ( A @ function )
| ~ ( A @ relation )
| ( ( A @ relation_dom @ identity_relation )
= A ) ),
inference(simp,[status(thm)],[178]) ).
thf(8227,plain,
! [A: $i] :
( ( ( sk9 @ empty )
!= ( A @ empty ) )
| ( A @ relation_rng @ relation )
| ~ $true
| ( sk9 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[7652,105]) ).
thf(8228,plain,
! [A: $i] :
( ( ( sk9 @ empty )
!= ( A @ empty ) )
| ( A @ relation_rng @ relation )
| ( sk9 != empty_set ) ),
inference(simp,[status(thm)],[8227]) ).
thf(8229,plain,
( ( sk9 @ relation_rng @ relation )
| ( sk9 != empty_set ) ),
inference(pattern_uni,[status(thm)],[8228:[bind(A,$thf( sk9 ))]]) ).
thf(20,axiom,
! [A: $i,B: $i] :
( ( ( B @ function )
& ( B @ relation )
& ( A @ function )
& ( A @ relation ) )
=> ( ( B @ ( A @ relation_composition ) @ function )
& ( B @ ( A @ relation_composition ) @ relation ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_funct_1) ).
thf(106,plain,
! [A: $i,B: $i] :
( ( ( B @ function )
& ( B @ relation )
& ( A @ function )
& ( A @ relation ) )
=> ( ( B @ ( A @ relation_composition ) @ function )
& ( B @ ( A @ relation_composition ) @ relation ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[20]) ).
thf(144,plain,
! [C: $i,B: $i,A: $i] :
( ( B = C )
| ( ( B @ ( A @ apply ) )
!= ( C @ ( A @ apply ) ) )
| ~ ( A @ relation_dom @ ( C @ in ) )
| ~ ( A @ relation_dom @ ( B @ in ) )
| ~ ( A @ one_to_one )
| ~ ( A @ function )
| ~ ( A @ relation ) ),
inference(cnfConj,[status(thm)],[141]) ).
thf(147,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( A @ relation_dom @ ( C @ in ) )
| ~ ( A @ relation_dom @ ( B @ in ) )
| ~ ( A @ one_to_one )
| ~ ( A @ function )
| ~ ( A @ relation )
| ( B = C )
| ( ( B @ ( A @ apply ) )
!= ( C @ ( A @ apply ) ) ) ),
inference(lifteq,[status(thm)],[144]) ).
thf(8272,plain,
! [A: $i] :
( ( ( sk9 @ empty )
!= ( A @ empty ) )
| ( A @ function )
| ~ $true
| ( sk9 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[7652,111]) ).
thf(8273,plain,
! [A: $i] :
( ( ( sk9 @ empty )
!= ( A @ empty ) )
| ( A @ function )
| ( sk9 != empty_set ) ),
inference(simp,[status(thm)],[8272]) ).
thf(8274,plain,
( ( sk9 @ function )
| ( sk9 != empty_set ) ),
inference(pattern_uni,[status(thm)],[8273:[bind(A,$thf( sk9 ))]]) ).
thf(41,axiom,
! [A: $i] : ( A @ identity_relation @ relation ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k6_relat_1) ).
thf(221,plain,
! [A: $i] : ( A @ identity_relation @ relation ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[41]) ).
thf(3,axiom,
! [A: $i,B: $i] :
~ ( ( B @ empty )
& ( A != B )
& ( A @ empty ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t8_boole) ).
thf(58,plain,
! [A: $i,B: $i] :
~ ( ( B @ empty )
& ( A != B )
& ( A @ empty ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(59,plain,
~ ? [A: $i] :
( ? [B: $i] :
( ( B @ empty )
& ( A != B ) )
& ( A @ empty ) ),
inference(miniscope,[status(thm)],[58]) ).
thf(60,plain,
! [B: $i,A: $i] :
( ~ ( B @ empty )
| ( A = B )
| ~ ( A @ empty ) ),
inference(cnf,[status(esa)],[59]) ).
thf(61,plain,
! [B: $i,A: $i] :
( ~ ( B @ empty )
| ~ ( A @ empty )
| ( A = B ) ),
inference(lifteq,[status(thm)],[60]) ).
thf(261,plain,
! [B: $i,A: $i] :
( ( A
!= ( sk1 @ identity_relation ) )
| ( B != sk3 )
| ~ ( B @ empty )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[61,55]) ).
thf(262,plain,
! [A: $i] :
( ( A != sk3 )
| ~ ( A @ empty )
| ~ ( sk1 @ identity_relation @ empty ) ),
inference(pattern_uni,[status(thm)],[261:[bind(A,$thf( sk1 @ identity_relation )),bind(B,$thf( B ))]]) ).
thf(362,plain,
( ~ ( sk3 @ empty )
| ~ ( sk1 @ identity_relation @ empty ) ),
inference(simp,[status(thm)],[262]) ).
thf(424,plain,
( ( ( sk1 @ identity_relation @ empty )
!= ( empty_set @ empty ) )
| ~ ( sk3 @ empty )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[75,362]) ).
thf(425,plain,
( ( ( sk1 @ identity_relation @ empty )
!= ( empty_set @ empty ) )
| ~ ( sk3 @ empty ) ),
inference(simp,[status(thm)],[424]) ).
thf(453,plain,
( ( ( sk1 @ identity_relation )
!= empty_set )
| ~ ( sk3 @ empty ) ),
inference(simp,[status(thm)],[425]) ).
thf(196,plain,
! [B: $i,A: $i] :
( ( B
= ( A @ relation_rng ) )
| ( ( A @ ( B @ sk19 ) )
= ( A @ ( B @ sk20 ) @ ( A @ apply ) ) )
| ( B @ ( A @ sk17 ) )
| ~ ( A @ function )
| ~ ( A @ relation ) ),
inference(cnfConj,[status(thm)],[194]) ).
thf(205,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ sk17 ) )
| ~ ( A @ function )
| ~ ( A @ relation )
| ( B
= ( A @ relation_rng ) )
| ( ( A @ ( B @ sk19 ) )
= ( A @ ( B @ sk20 ) @ ( A @ apply ) ) ) ),
inference(lifteq,[status(thm)],[196]) ).
thf(206,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ sk17 ) )
| ~ ( A @ function )
| ~ ( A @ relation )
| ( B
= ( A @ relation_rng ) )
| ( ( A @ ( B @ sk19 ) )
= ( A @ ( B @ sk20 ) @ ( A @ apply ) ) ) ),
inference(simp,[status(thm)],[205]) ).
thf(8259,plain,
! [A: $i] :
( ( ( sk9 @ empty )
!= ( A @ empty ) )
| ( A @ relation_rng @ empty )
| ~ $true
| ( sk9 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[7652,104]) ).
thf(8260,plain,
! [A: $i] :
( ( ( sk9 @ empty )
!= ( A @ empty ) )
| ( A @ relation_rng @ empty )
| ( sk9 != empty_set ) ),
inference(simp,[status(thm)],[8259]) ).
thf(8261,plain,
( ( sk9 @ relation_rng @ empty )
| ( sk9 != empty_set ) ),
inference(pattern_uni,[status(thm)],[8260:[bind(A,$thf( sk9 ))]]) ).
thf(28,axiom,
! [A: $i,B: $i] :
( ( ( B @ relation )
& ( A @ relation ) )
=> ( B @ ( A @ relation_composition ) @ relation ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k5_relat_1) ).
thf(131,plain,
! [A: $i,B: $i] :
( ( ( B @ relation )
& ( A @ relation ) )
=> ( B @ ( A @ relation_composition ) @ relation ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[28]) ).
thf(132,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ relation_composition ) @ relation )
| ~ ( B @ relation )
| ~ ( A @ relation ) ),
inference(cnf,[status(esa)],[131]) ).
thf(24,axiom,
! [A: $i,B: $i] : ( A @ ( A @ subset ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reflexivity_r1_tarski) ).
thf(118,plain,
! [A: $i] : ( A @ ( A @ subset ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[24]) ).
thf(119,plain,
! [A: $i] : ( A @ ( A @ subset ) ),
inference(cnf,[status(esa)],[118]) ).
thf(6130,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ subset ) )
!= ( C @ ( B @ subset ) ) )
| ( C @ powerset @ ( B @ element ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[119,155]) ).
thf(6131,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ subset ) )
!= ( C @ ( B @ subset ) ) )
| ( C @ powerset @ ( B @ element ) ) ),
inference(simp,[status(thm)],[6130]) ).
thf(6132,plain,
! [A: $i] : ( A @ powerset @ ( A @ element ) ),
inference(pattern_uni,[status(thm)],[6131:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( A ))]]) ).
thf(6192,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)],[6132,77]) ).
thf(6193,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ element ) )
!= ( C @ ( B @ element ) ) )
| ( C @ ( B @ in ) )
| ( C @ empty ) ),
inference(simp,[status(thm)],[6192]) ).
thf(6194,plain,
! [A: $i] :
( ( A @ powerset @ ( A @ in ) )
| ( A @ powerset @ empty ) ),
inference(pattern_uni,[status(thm)],[6193:[bind(A,$thf( D )),bind(B,$thf( D )),bind(C,$thf( D @ powerset ))]]) ).
thf(6201,plain,
! [A: $i] :
( ( A @ powerset @ ( A @ in ) )
| ( A @ powerset @ empty ) ),
inference(simp,[status(thm)],[6194]) ).
thf(6696,plain,
! [A: $i] :
( ( A @ powerset @ ( A @ in ) )
| $false ),
inference(rewrite,[status(thm)],[6201,91]) ).
thf(6697,plain,
! [A: $i] : ( A @ powerset @ ( A @ in ) ),
inference(simp,[status(thm)],[6696]) ).
thf(6701,plain,
! [B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ in ) )
!= ( B @ ( B @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[6697,1586]) ).
thf(6702,plain,
! [B: $i,A: $i] :
( ( A @ powerset @ ( A @ in ) )
!= ( B @ ( B @ in ) ) ),
inference(simp,[status(thm)],[6701]) ).
thf(6741,plain,
! [B: $i,A: $i] :
( ( ( A @ powerset )
!= B )
| ( A != B ) ),
inference(simp,[status(thm)],[6702]) ).
thf(6757,plain,
! [A: $i] :
( ( A @ powerset )
!= A ),
inference(simp,[status(thm)],[6741]) ).
thf(12468,plain,
! [B: $i,A: $i] :
( ( A
!= ( B @ powerset ) )
| ( empty_set != B )
| ( empty_set @ ( empty_set @ ( A @ sk20 ) @ in ) )
| ( A @ ( empty_set @ sk17 ) ) ),
inference(paramod_ordered,[status(thm)],[11958,6757]) ).
thf(12469,plain,
! [A: $i] :
( ( empty_set != A )
| ( empty_set @ ( empty_set @ ( A @ powerset @ sk20 ) @ in ) )
| ( A @ powerset @ ( empty_set @ sk17 ) ) ),
inference(pattern_uni,[status(thm)],[12468:[bind(A,$thf( C @ powerset )),bind(B,$thf( C ))]]) ).
thf(12882,plain,
( ( empty_set @ ( empty_set @ ( empty_set @ powerset @ sk20 ) @ in ) )
| ( empty_set @ powerset @ ( empty_set @ sk17 ) ) ),
inference(simp,[status(thm)],[12469]) ).
thf(32359,plain,
( $false
| ( empty_set @ powerset @ ( empty_set @ sk17 ) ) ),
inference(rewrite,[status(thm)],[12882,578]) ).
thf(32360,plain,
empty_set @ powerset @ ( empty_set @ sk17 ),
inference(simp,[status(thm)],[32359]) ).
thf(29,axiom,
! [A: $i,B: $i] :
( ( ( B @ function )
& ( B @ relation ) )
=> ! [C: $i] :
( ( ( C @ function )
& ( C @ relation ) )
=> ( ( B @ relation_dom @ ( A @ in ) )
=> ( ( A @ ( C @ ( B @ relation_composition ) @ apply ) )
= ( A @ ( B @ apply ) @ ( C @ apply ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t23_funct_1) ).
thf(133,plain,
! [A: $i,B: $i] :
( ( ( B @ function )
& ( B @ relation ) )
=> ! [C: $i] :
( ( ( C @ function )
& ( C @ relation ) )
=> ( ( B @ relation_dom @ ( A @ in ) )
=> ( ( A @ ( C @ ( B @ relation_composition ) @ apply ) )
= ( A @ ( B @ apply ) @ ( C @ apply ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[29]) ).
thf(23,axiom,
! [A: $i,B: $i] :
( ( ( B @ relation )
& ( A @ empty ) )
=> ( ( B @ ( A @ relation_composition ) @ relation )
& ( B @ ( A @ relation_composition ) @ empty ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc9_relat_1) ).
thf(114,plain,
! [A: $i,B: $i] :
( ( ( B @ relation )
& ( A @ empty ) )
=> ( ( B @ ( A @ relation_composition ) @ relation )
& ( B @ ( A @ relation_composition ) @ empty ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[23]) ).
thf(115,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ relation_composition ) @ relation )
| ~ ( B @ relation )
| ~ ( A @ empty ) )
& ( ( B @ ( A @ relation_composition ) @ empty )
| ~ ( B @ relation )
| ~ ( A @ empty ) ) ),
inference(cnf,[status(esa)],[114]) ).
thf(116,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ relation_composition ) @ empty )
| ~ ( B @ relation )
| ~ ( A @ empty ) ),
inference(cnfConj,[status(thm)],[115]) ).
thf(94,plain,
! [A: $i] : ( A @ powerset @ ( A @ sk7 @ element ) ),
inference(cnfConj,[status(thm)],[93]) ).
thf(1405,plain,
! [A: $i] : ( A @ powerset @ ( empty_set @ element ) ),
inference(rewrite,[status(thm)],[94,1342]) ).
thf(7579,plain,
( ( ( sk9 @ empty )
!= ( sk5 @ empty ) )
| ~ $true
| ( ( sk9 @ relation_rng )
!= empty_set ) ),
inference(paramod_ordered,[status(thm)],[4104,74]) ).
thf(7580,plain,
( ( ( sk9 @ empty )
!= ( sk5 @ empty ) )
| ( ( sk9 @ relation_rng )
!= empty_set ) ),
inference(simp,[status(thm)],[7579]) ).
thf(7674,plain,
( ( sk9 != sk5 )
| ( ( sk9 @ relation_rng )
!= empty_set ) ),
inference(simp,[status(thm)],[7580]) ).
thf(291,plain,
! [B: $i,A: $i] :
( ( B != sk3 )
| ( sk1 @ ( A @ relation_rng @ subset ) )
| ~ ( B @ empty )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[61,52]) ).
thf(292,plain,
! [A: $i] :
( ( sk1 @ ( A @ relation_rng @ subset ) )
| ~ ( sk3 @ empty )
| ~ ( A @ empty ) ),
inference(pattern_uni,[status(thm)],[291:[bind(A,$thf( A )),bind(B,$thf( sk3 ))]]) ).
thf(35309,plain,
( ( ( sk1 @ empty )
!= ( sk1 @ empty ) )
| ~ $true
| ( sk2 @ empty )
| ( sk3 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[9460,35289]) ).
thf(35310,plain,
( ( ( sk1 @ empty )
!= ( sk1 @ empty ) )
| ( sk2 @ empty )
| ( sk3 != empty_set ) ),
inference(simp,[status(thm)],[35309]) ).
thf(35311,plain,
( ( sk2 @ empty )
| ( sk3 != empty_set ) ),
inference(pattern_uni,[status(thm)],[35310:[]]) ).
thf(35822,plain,
! [A: $i] :
( ( A != sk3 )
| ( sk2 @ empty )
| ( empty_set != empty_set )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[84,35311]) ).
thf(35823,plain,
! [A: $i] :
( ( A != sk3 )
| ( sk2 @ empty )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[35822]) ).
thf(35824,plain,
( ( sk2 @ empty )
| ~ ( sk3 @ empty ) ),
inference(pattern_uni,[status(thm)],[35823:[bind(A,$thf( sk3 ))]]) ).
thf(6062,plain,
! [A: $i] :
( ( A != sk2 )
| ( ( sk10 @ relation_rng )
!= sk2 )
| ( empty_set != empty_set )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[84,3835]) ).
thf(6063,plain,
! [A: $i] :
( ( A != sk2 )
| ( ( sk10 @ relation_rng )
!= sk2 )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[6062]) ).
thf(6064,plain,
( ( ( sk10 @ relation_rng )
!= sk2 )
| ~ ( sk2 @ empty ) ),
inference(pattern_uni,[status(thm)],[6063:[bind(A,$thf( sk2 ))]]) ).
thf(426,plain,
( ( ( sk3 @ empty )
!= ( empty_set @ empty ) )
| ~ $true
| ~ ( sk1 @ identity_relation @ empty ) ),
inference(paramod_ordered,[status(thm)],[75,362]) ).
thf(427,plain,
( ( ( sk3 @ empty )
!= ( empty_set @ empty ) )
| ~ ( sk1 @ identity_relation @ empty ) ),
inference(simp,[status(thm)],[426]) ).
thf(452,plain,
( ( sk3 != empty_set )
| ~ ( sk1 @ identity_relation @ empty ) ),
inference(simp,[status(thm)],[427]) ).
thf(6241,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk3 @ relation_rng @ in ) )
!= ( B @ ( A @ in ) ) )
| ~ ( A @ ( B @ in ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[6235,88]) ).
thf(6242,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk3 @ relation_rng @ in ) )
!= ( B @ ( A @ in ) ) )
| ~ ( A @ ( B @ in ) ) ),
inference(simp,[status(thm)],[6241]) ).
thf(6243,plain,
~ ( sk3 @ relation_rng @ ( sk1 @ powerset @ in ) ),
inference(pattern_uni,[status(thm)],[6242:[bind(A,$thf( sk3 @ relation_rng )),bind(B,$thf( sk1 @ powerset ))]]) ).
thf(6721,plain,
! [A: $i] :
( ( ( A @ powerset @ ( A @ in ) )
!= ( sk3 @ relation_rng @ ( sk1 @ powerset @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[6697,6243]) ).
thf(6722,plain,
! [A: $i] :
( ( A @ powerset @ ( A @ in ) )
!= ( sk3 @ relation_rng @ ( sk1 @ powerset @ in ) ) ),
inference(simp,[status(thm)],[6721]) ).
thf(6743,plain,
! [A: $i] :
( ( ( A @ powerset )
!= ( sk3 @ relation_rng ) )
| ( A
!= ( sk1 @ powerset ) ) ),
inference(simp,[status(thm)],[6722]) ).
thf(6760,plain,
( ( sk1 @ powerset @ powerset )
!= ( sk3 @ relation_rng ) ),
inference(simp,[status(thm)],[6743]) ).
thf(117,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ relation_composition ) @ relation )
| ~ ( B @ relation )
| ~ ( A @ empty ) ),
inference(cnfConj,[status(thm)],[115]) ).
thf(35444,plain,
( ( ( sk2 @ empty )
!= ( sk2 @ empty ) )
| ( sk1 @ relation )
| ~ $true
| ~ ( sk1 @ empty ) ),
inference(paramod_ordered,[status(thm)],[35289,9607]) ).
thf(35445,plain,
( ( ( sk2 @ empty )
!= ( sk2 @ empty ) )
| ( sk1 @ relation )
| ~ ( sk1 @ empty ) ),
inference(simp,[status(thm)],[35444]) ).
thf(35446,plain,
( ( sk1 @ relation )
| ~ ( sk1 @ empty ) ),
inference(pattern_uni,[status(thm)],[35445:[]]) ).
thf(37610,plain,
( ( ( sk1 @ empty )
!= ( empty_set @ empty ) )
| ( sk1 @ relation )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[75,35446]) ).
thf(37611,plain,
( ( ( sk1 @ empty )
!= ( empty_set @ empty ) )
| ( sk1 @ relation ) ),
inference(simp,[status(thm)],[37610]) ).
thf(37643,plain,
( ( sk1 != empty_set )
| ( sk1 @ relation ) ),
inference(simp,[status(thm)],[37611]) ).
thf(10504,plain,
( ( ( sk1 @ empty )
!= ( sk1 @ empty ) )
| ( ( empty_set @ identity_relation )
!= sk3 )
| ~ $true
| ( sk3 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[9460,1302]) ).
thf(10505,plain,
( ( ( sk1 @ empty )
!= ( sk1 @ empty ) )
| ( ( empty_set @ identity_relation )
!= sk3 )
| ( sk3 != empty_set ) ),
inference(simp,[status(thm)],[10504]) ).
thf(10506,plain,
( ( ( empty_set @ identity_relation )
!= sk3 )
| ( sk3 != empty_set ) ),
inference(pattern_uni,[status(thm)],[10505:[]]) ).
thf(13,axiom,
! [A: $i,B: $i,C: $i] :
( ( ( C @ powerset @ ( B @ element ) )
& ( B @ ( A @ in ) ) )
=> ( C @ ( A @ element ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t4_subset) ).
thf(85,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)],[13]) ).
thf(170,plain,
! [B: $i,A: $i] :
( ( ( B @ relation_dom )
= A )
| ( B
!= ( A @ identity_relation ) )
| ~ ( B @ function )
| ~ ( B @ relation ) ),
inference(cnfConj,[status(thm)],[169]) ).
thf(174,plain,
! [B: $i,A: $i] :
( ~ ( B @ function )
| ~ ( B @ relation )
| ( ( B @ relation_dom )
= A )
| ( B
!= ( A @ identity_relation ) ) ),
inference(lifteq,[status(thm)],[170]) ).
thf(175,plain,
! [A: $i] :
( ~ ( A @ identity_relation @ function )
| ~ ( A @ identity_relation @ relation )
| ( ( A @ identity_relation @ relation_dom )
= A ) ),
inference(simp,[status(thm)],[174]) ).
thf(7036,plain,
! [A: $i] :
( ~ $true
| ~ $true
| ( ( A @ identity_relation @ relation_dom )
= A ) ),
inference(rewrite,[status(thm)],[175,185,187]) ).
thf(7037,plain,
! [A: $i] :
( ( A @ identity_relation @ relation_dom )
= A ),
inference(simp,[status(thm)],[7036]) ).
thf(1806,plain,
! [A: $i] :
( ( ( empty_set @ relation_rng @ empty )
!= ( A @ empty ) )
| ( A @ relation_rng @ empty )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1736,104]) ).
thf(1807,plain,
! [A: $i] :
( ( ( empty_set @ relation_rng @ empty )
!= ( A @ empty ) )
| ( A @ relation_rng @ empty ) ),
inference(simp,[status(thm)],[1806]) ).
thf(1808,plain,
empty_set @ relation_rng @ relation_rng @ empty,
inference(pattern_uni,[status(thm)],[1807:[bind(A,$thf( empty_set @ relation_rng ))]]) ).
thf(1848,plain,
empty_set @ relation_rng @ empty,
inference(rewrite,[status(thm)],[1808,1764]) ).
thf(9305,plain,
! [A: $i] :
( ( ( empty_set @ relation_rng @ empty )
!= ( A @ empty ) )
| ( A @ relation_dom @ empty )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1848,190]) ).
thf(9306,plain,
! [A: $i] :
( ( ( empty_set @ relation_rng @ empty )
!= ( A @ empty ) )
| ( A @ relation_dom @ empty ) ),
inference(simp,[status(thm)],[9305]) ).
thf(9307,plain,
empty_set @ relation_rng @ relation_dom @ empty,
inference(pattern_uni,[status(thm)],[9306:[bind(A,$thf( empty_set @ relation_rng ))]]) ).
thf(9686,plain,
empty_set @ relation_dom @ empty,
inference(rewrite,[status(thm)],[9307,1764]) ).
thf(191,plain,
! [A: $i] :
( ( A @ relation_dom @ relation )
| ~ ( A @ empty ) ),
inference(cnfConj,[status(thm)],[189]) ).
thf(9935,plain,
! [A: $i] :
( ( ( empty_set @ relation_dom @ empty )
!= ( A @ empty ) )
| ( A @ relation_dom @ relation )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[9686,191]) ).
thf(9936,plain,
! [A: $i] :
( ( ( empty_set @ relation_dom @ empty )
!= ( A @ empty ) )
| ( A @ relation_dom @ relation ) ),
inference(simp,[status(thm)],[9935]) ).
thf(9937,plain,
empty_set @ relation_dom @ relation_dom @ relation,
inference(pattern_uni,[status(thm)],[9936:[bind(A,$thf( empty_set @ relation_dom ))]]) ).
thf(10831,plain,
empty_set @ relation_dom @ relation,
inference(rewrite,[status(thm)],[9937,9377]) ).
thf(1291,plain,
! [B: $i,A: $i] :
( ( A
!= ( B @ sk8 ) )
| ( B @ ( empty_set @ in ) )
| ( B @ empty )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[84,791]) ).
thf(1292,plain,
! [A: $i] :
( ( A @ ( empty_set @ in ) )
| ( A @ empty )
| ~ ( A @ sk8 @ empty ) ),
inference(pattern_uni,[status(thm)],[1291:[bind(A,$thf( C @ sk8 )),bind(B,$thf( C ))]]) ).
thf(1343,plain,
! [A: $i] :
( ( A @ ( empty_set @ in ) )
| ( A @ empty )
| ~ ( A @ sk8 @ empty ) ),
inference(simp,[status(thm)],[1292]) ).
thf(5963,plain,
( ( ( sk2 @ relation_rng @ empty )
!= ( sk5 @ empty ) )
| ~ $true
| ( sk2 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[3812,74]) ).
thf(5964,plain,
( ( ( sk2 @ relation_rng @ empty )
!= ( sk5 @ empty ) )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[5963]) ).
thf(6032,plain,
( ( ( sk2 @ relation_rng )
!= sk5 )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[5964]) ).
thf(301,plain,
! [B: $i,A: $i] :
( ( B != sk2 )
| ( A @ one_to_one )
| ~ ( B @ empty )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[61,46]) ).
thf(302,plain,
! [A: $i] :
( ( A @ one_to_one )
| ~ ( sk2 @ empty )
| ~ ( A @ empty ) ),
inference(pattern_uni,[status(thm)],[301:[bind(A,$thf( A )),bind(B,$thf( sk2 ))]]) ).
thf(12002,plain,
! [A: $i] :
( ( A != sk3 )
| ( sk1 @ empty )
| ( empty_set != empty_set )
| ( empty_set @ ( empty_set @ ( A @ sk20 ) @ in ) )
| ( A @ ( empty_set @ sk17 ) ) ),
inference(paramod_ordered,[status(thm)],[11958,9460]) ).
thf(12003,plain,
! [A: $i] :
( ( A != sk3 )
| ( sk1 @ empty )
| ( empty_set @ ( empty_set @ ( A @ sk20 ) @ in ) )
| ( A @ ( empty_set @ sk17 ) ) ),
inference(simp,[status(thm)],[12002]) ).
thf(12004,plain,
( ( sk1 @ empty )
| ( empty_set @ ( empty_set @ ( sk3 @ sk20 ) @ in ) )
| ( sk3 @ ( empty_set @ sk17 ) ) ),
inference(pattern_uni,[status(thm)],[12003:[bind(A,$thf( sk3 ))]]) ).
thf(17302,plain,
( ( sk1 @ empty )
| $false
| ( sk3 @ ( empty_set @ sk17 ) ) ),
inference(rewrite,[status(thm)],[12004,578]) ).
thf(17303,plain,
( ( sk1 @ empty )
| ( sk3 @ ( empty_set @ sk17 ) ) ),
inference(simp,[status(thm)],[17302]) ).
thf(34,axiom,
? [A: $i] :
( ( A @ relation )
& ( A @ empty ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc1_relat_1) ).
thf(160,plain,
? [A: $i] :
( ( A @ relation )
& ( A @ empty ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[34]) ).
thf(10470,plain,
! [A: $i] :
( ( A != sk2 )
| ( sk10 != sk1 )
| ( empty_set != empty_set )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[84,10188]) ).
thf(10471,plain,
! [A: $i] :
( ( A != sk2 )
| ( sk10 != sk1 )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[10470]) ).
thf(10472,plain,
( ( sk10 != sk1 )
| ~ ( sk2 @ empty ) ),
inference(pattern_uni,[status(thm)],[10471:[bind(A,$thf( sk2 ))]]) ).
thf(11906,plain,
( ( ( sk2 @ empty )
!= ( sk2 @ empty ) )
| ( sk10 != sk1 )
| ~ $true
| ( ( sk2 @ relation_rng )
!= empty_set ) ),
inference(paramod_ordered,[status(thm)],[3190,10472]) ).
thf(11907,plain,
( ( ( sk2 @ empty )
!= ( sk2 @ empty ) )
| ( sk10 != sk1 )
| ( ( sk2 @ relation_rng )
!= empty_set ) ),
inference(simp,[status(thm)],[11906]) ).
thf(11908,plain,
( ( sk10 != sk1 )
| ( ( sk2 @ relation_rng )
!= empty_set ) ),
inference(pattern_uni,[status(thm)],[11907:[]]) ).
thf(4158,plain,
! [B: $i,A: $i] :
( ( ( sk11 @ relation_dom @ ( sk11 @ sk13 @ in ) )
!= ( B @ ( A @ in ) ) )
| ( B @ ( A @ element ) )
| ~ $true
| ( sk11 @ one_to_one ) ),
inference(paramod_ordered,[status(thm)],[4117,71]) ).
thf(4159,plain,
! [B: $i,A: $i] :
( ( ( sk11 @ relation_dom @ ( sk11 @ sk13 @ in ) )
!= ( B @ ( A @ in ) ) )
| ( B @ ( A @ element ) )
| ( sk11 @ one_to_one ) ),
inference(simp,[status(thm)],[4158]) ).
thf(4160,plain,
( ( sk11 @ relation_dom @ ( sk11 @ sk13 @ element ) )
| ( sk11 @ one_to_one ) ),
inference(pattern_uni,[status(thm)],[4159:[bind(A,$thf( sk11 @ sk13 )),bind(B,$thf( sk11 @ relation_dom ))]]) ).
thf(10100,plain,
! [A: $i] :
( ( ( sk1 @ empty )
!= ( A @ empty ) )
| ( A @ relation_rng @ relation )
| ~ $true
| ( sk2 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[9418,105]) ).
thf(10101,plain,
! [A: $i] :
( ( ( sk1 @ empty )
!= ( A @ empty ) )
| ( A @ relation_rng @ relation )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[10100]) ).
thf(10102,plain,
( ( sk1 @ relation_rng @ relation )
| ( sk2 != empty_set ) ),
inference(pattern_uni,[status(thm)],[10101:[bind(A,$thf( sk1 ))]]) ).
thf(9991,plain,
( ( ( sk2 @ empty )
!= ( sk2 @ empty ) )
| ( sk1 @ empty )
| ~ $true
| ( ( sk2 @ relation_rng )
!= empty_set ) ),
inference(paramod_ordered,[status(thm)],[3190,9152]) ).
thf(9992,plain,
( ( ( sk2 @ empty )
!= ( sk2 @ empty ) )
| ( sk1 @ empty )
| ( ( sk2 @ relation_rng )
!= empty_set ) ),
inference(simp,[status(thm)],[9991]) ).
thf(9993,plain,
( ( sk1 @ empty )
| ( ( sk2 @ relation_rng )
!= empty_set ) ),
inference(pattern_uni,[status(thm)],[9992:[]]) ).
thf(35792,plain,
( ( ( sk2 @ empty )
!= ( sk2 @ empty ) )
| ( sk10 != sk2 )
| ~ $true
| ( sk3 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[35311,3848]) ).
thf(35793,plain,
( ( ( sk2 @ empty )
!= ( sk2 @ empty ) )
| ( sk10 != sk2 )
| ( sk3 != empty_set ) ),
inference(simp,[status(thm)],[35792]) ).
thf(35794,plain,
( ( sk10 != sk2 )
| ( sk3 != empty_set ) ),
inference(pattern_uni,[status(thm)],[35793:[]]) ).
thf(247,plain,
! [B: $i,A: $i] :
( ( B
!= ( sk3 @ relation_dom ) )
| ( A = sk1 )
| ~ ( B @ empty )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[61,56]) ).
thf(248,plain,
! [A: $i] :
( ( A = sk1 )
| ~ ( sk3 @ relation_dom @ empty )
| ~ ( A @ empty ) ),
inference(pattern_uni,[status(thm)],[247:[bind(A,$thf( A )),bind(B,$thf( sk3 @ relation_dom ))]]) ).
thf(18176,plain,
! [A: $i] :
( ( A = sk1 )
| ~ ( sk1 @ empty )
| ~ ( A @ empty ) ),
inference(rewrite,[status(thm)],[248,56]) ).
thf(35430,plain,
! [A: $i] :
( ( ( sk2 @ empty )
!= ( A @ empty ) )
| ( A = sk1 )
| ~ ( sk1 @ empty )
| ~ $true
| ~ ( sk1 @ empty ) ),
inference(paramod_ordered,[status(thm)],[35289,18176]) ).
thf(35431,plain,
! [A: $i] :
( ( ( sk2 @ empty )
!= ( A @ empty ) )
| ( A = sk1 )
| ~ ( sk1 @ empty ) ),
inference(simp,[status(thm)],[35430]) ).
thf(35432,plain,
( ( sk2 = sk1 )
| ~ ( sk1 @ empty ) ),
inference(pattern_uni,[status(thm)],[35431:[bind(A,$thf( sk2 ))]]) ).
thf(37353,plain,
( ( ( sk1 @ empty )
!= ( sk1 @ empty ) )
| ( sk2 = sk1 )
| ~ $true
| ( sk2 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[9418,35432]) ).
thf(37354,plain,
( ( ( sk1 @ empty )
!= ( sk1 @ empty ) )
| ( sk2 = sk1 )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[37353]) ).
thf(37355,plain,
( ( sk2 = sk1 )
| ( sk2 != empty_set ) ),
inference(pattern_uni,[status(thm)],[37354:[]]) ).
thf(10534,plain,
( ( ( sk5 @ empty )
!= ( sk1 @ empty ) )
| ~ $true
| ( sk3 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[9460,74]) ).
thf(10535,plain,
( ( ( sk5 @ empty )
!= ( sk1 @ empty ) )
| ( sk3 != empty_set ) ),
inference(simp,[status(thm)],[10534]) ).
thf(10646,plain,
( ( sk5 != sk1 )
| ( sk3 != empty_set ) ),
inference(simp,[status(thm)],[10535]) ).
thf(13679,plain,
! [A: $i] :
( ( A != sk3 )
| ( sk5 != sk1 )
| ( empty_set != empty_set )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[84,10646]) ).
thf(13680,plain,
! [A: $i] :
( ( A != sk3 )
| ( sk5 != sk1 )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[13679]) ).
thf(13681,plain,
( ( sk5 != sk1 )
| ~ ( sk3 @ empty ) ),
inference(pattern_uni,[status(thm)],[13680:[bind(A,$thf( sk3 ))]]) ).
thf(4643,plain,
( ( ( sk11 @ relation_dom )
!= ( sk2 @ relation_dom ) )
| ( sk1 @ ( sk11 @ sk13 @ element ) )
| ( sk11 @ one_to_one ) ),
inference(paramod_ordered,[status(thm)],[57,4160]) ).
thf(4680,plain,
( ( sk11 != sk2 )
| ( sk1 @ ( sk11 @ sk13 @ element ) )
| ( sk11 @ one_to_one ) ),
inference(simp,[status(thm)],[4643]) ).
thf(1435,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)],[1405,77]) ).
thf(1436,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ ( empty_set @ element ) )
!= ( C @ ( B @ element ) ) )
| ( C @ ( B @ in ) )
| ( C @ empty ) ),
inference(simp,[status(thm)],[1435]) ).
thf(1437,plain,
! [A: $i] :
( ( A @ powerset @ ( empty_set @ in ) )
| ( A @ powerset @ empty ) ),
inference(pattern_uni,[status(thm)],[1436:[bind(A,$thf( D )),bind(B,$thf( empty_set )),bind(C,$thf( D @ powerset ))]]) ).
thf(1446,plain,
! [A: $i] :
( ( A @ powerset @ ( empty_set @ in ) )
| ( A @ powerset @ empty ) ),
inference(simp,[status(thm)],[1437]) ).
thf(1452,plain,
! [A: $i] :
( ( A @ powerset @ ( empty_set @ in ) )
| $false ),
inference(rewrite,[status(thm)],[1446,91]) ).
thf(1453,plain,
! [A: $i] : ( A @ powerset @ ( empty_set @ in ) ),
inference(simp,[status(thm)],[1452]) ).
thf(7312,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ ( empty_set @ in ) )
!= ( B @ ( C @ in ) ) )
| ~ $true
| ( ( C @ ( B @ identity_relation @ apply ) )
= C ) ),
inference(paramod_ordered,[status(thm)],[1453,7265]) ).
thf(7313,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ ( empty_set @ in ) )
!= ( B @ ( C @ in ) ) )
| ( ( C @ ( B @ identity_relation @ apply ) )
= C ) ),
inference(simp,[status(thm)],[7312]) ).
thf(7314,plain,
! [A: $i] :
( ( empty_set @ ( A @ powerset @ identity_relation @ apply ) )
= empty_set ),
inference(pattern_uni,[status(thm)],[7313:[bind(A,$thf( D )),bind(B,$thf( D @ powerset )),bind(C,$thf( empty_set ))]]) ).
thf(7329,plain,
! [A: $i] :
( ( empty_set @ ( A @ powerset @ identity_relation @ apply ) )
= empty_set ),
inference(simp,[status(thm)],[7314]) ).
thf(9144,plain,
! [A: $i] :
( ( ( sk3 @ relation_dom )
!= ( A @ relation_dom ) )
| ( sk1 @ empty )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[56,190]) ).
thf(9145,plain,
( ( sk1 @ empty )
| ~ ( sk3 @ empty ) ),
inference(pattern_uni,[status(thm)],[9144:[bind(A,$thf( sk3 ))]]) ).
thf(33,axiom,
( ( empty_set @ relation )
& ( empty_set @ empty ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc4_relat_1) ).
thf(156,plain,
( ( empty_set @ relation )
& ( empty_set @ empty ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[33]) ).
thf(10152,plain,
! [A: $i] :
( ( ( sk1 @ empty )
!= ( A @ empty ) )
| ( A @ relation_dom @ empty )
| ~ $true
| ( sk2 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[9418,190]) ).
thf(10153,plain,
! [A: $i] :
( ( ( sk1 @ empty )
!= ( A @ empty ) )
| ( A @ relation_dom @ empty )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[10152]) ).
thf(10154,plain,
( ( sk1 @ relation_dom @ empty )
| ( sk2 != empty_set ) ),
inference(pattern_uni,[status(thm)],[10153:[bind(A,$thf( sk1 ))]]) ).
thf(1960,plain,
! [A: $i] :
( ( ( empty_set @ relation_rng @ empty )
!= ( A @ empty ) )
| ( A @ relation_rng @ relation )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1848,105]) ).
thf(1961,plain,
! [A: $i] :
( ( ( empty_set @ relation_rng @ empty )
!= ( A @ empty ) )
| ( A @ relation_rng @ relation ) ),
inference(simp,[status(thm)],[1960]) ).
thf(1962,plain,
empty_set @ relation_rng @ relation_rng @ relation,
inference(pattern_uni,[status(thm)],[1961:[bind(A,$thf( empty_set @ relation_rng ))]]) ).
thf(1970,plain,
empty_set @ relation_rng @ relation,
inference(rewrite,[status(thm)],[1962,1764]) ).
thf(10050,plain,
( ( ( sk1 @ empty )
!= ( sk1 @ empty ) )
| ( ( empty_set @ identity_relation )
!= sk3 )
| ~ $true
| ( sk2 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[9418,1302]) ).
thf(10051,plain,
( ( ( sk1 @ empty )
!= ( sk1 @ empty ) )
| ( ( empty_set @ identity_relation )
!= sk3 )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[10050]) ).
thf(10052,plain,
( ( ( empty_set @ identity_relation )
!= sk3 )
| ( sk2 != empty_set ) ),
inference(pattern_uni,[status(thm)],[10051:[]]) ).
thf(9624,plain,
( ( sk1 = empty_set )
| ~ ( sk3 @ empty ) ),
inference(rewrite,[status(thm)],[1129,9377]) ).
thf(107,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ relation_composition ) @ function )
| ~ ( B @ function )
| ~ ( B @ relation )
| ~ ( A @ function )
| ~ ( A @ relation ) )
& ( ( B @ ( A @ relation_composition ) @ relation )
| ~ ( B @ function )
| ~ ( B @ relation )
| ~ ( A @ function )
| ~ ( A @ relation ) ) ),
inference(cnf,[status(esa)],[106]) ).
thf(109,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ relation_composition ) @ function )
| ~ ( B @ function )
| ~ ( B @ relation )
| ~ ( A @ function )
| ~ ( A @ relation ) ),
inference(cnfConj,[status(thm)],[107]) ).
thf(9622,plain,
( ( sk1 = empty_set )
| ~ ( sk2 @ empty ) ),
inference(rewrite,[status(thm)],[1156,9377]) ).
thf(14750,plain,
( ( ( sk2 @ empty )
!= ( sk2 @ empty ) )
| ( sk1 = empty_set )
| ~ $true
| ( ( sk2 @ relation_rng )
!= empty_set ) ),
inference(paramod_ordered,[status(thm)],[3190,9622]) ).
thf(14751,plain,
( ( ( sk2 @ empty )
!= ( sk2 @ empty ) )
| ( sk1 = empty_set )
| ( ( sk2 @ relation_rng )
!= empty_set ) ),
inference(simp,[status(thm)],[14750]) ).
thf(14752,plain,
( ( sk1 = empty_set )
| ( ( sk2 @ relation_rng )
!= empty_set ) ),
inference(pattern_uni,[status(thm)],[14751:[]]) ).
thf(4361,plain,
( ( ( sk5 @ empty )
!= ( sk3 @ empty ) )
| ~ $true
| ( sk3 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[4314,74]) ).
thf(4362,plain,
( ( ( sk5 @ empty )
!= ( sk3 @ empty ) )
| ( sk3 != empty_set ) ),
inference(simp,[status(thm)],[4361]) ).
thf(4425,plain,
( ( sk5 != sk3 )
| ( sk3 != empty_set ) ),
inference(simp,[status(thm)],[4362]) ).
thf(33947,plain,
( ( sk1 != sk1 )
| ( empty_set @ ( sk3 @ relation_rng @ subset ) )
| ( sk2 @ ( empty_set @ sk17 ) ) ),
inference(paramod_ordered,[status(thm)],[33940,52]) ).
thf(33948,plain,
( ( empty_set @ ( sk3 @ relation_rng @ subset ) )
| ( sk2 @ ( empty_set @ sk17 ) ) ),
inference(pattern_uni,[status(thm)],[33947:[]]) ).
thf(35332,plain,
( ( ( sk2 @ empty )
!= ( sk2 @ empty ) )
| ( sk5 != sk2 )
| ~ $true
| ~ ( sk1 @ empty ) ),
inference(paramod_ordered,[status(thm)],[35289,3866]) ).
thf(35333,plain,
( ( ( sk2 @ empty )
!= ( sk2 @ empty ) )
| ( sk5 != sk2 )
| ~ ( sk1 @ empty ) ),
inference(simp,[status(thm)],[35332]) ).
thf(35334,plain,
( ( sk5 != sk2 )
| ~ ( sk1 @ empty ) ),
inference(pattern_uni,[status(thm)],[35333:[]]) ).
thf(9908,plain,
! [A: $i] :
( ( ( sk9 @ empty )
!= ( A @ empty ) )
| ( A @ relation_dom @ relation )
| ~ $true
| ( sk9 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[7652,191]) ).
thf(9909,plain,
! [A: $i] :
( ( ( sk9 @ empty )
!= ( A @ empty ) )
| ( A @ relation_dom @ relation )
| ( sk9 != empty_set ) ),
inference(simp,[status(thm)],[9908]) ).
thf(9910,plain,
( ( sk9 @ relation_dom @ relation )
| ( sk9 != empty_set ) ),
inference(pattern_uni,[status(thm)],[9909:[bind(A,$thf( sk9 ))]]) ).
thf(10161,plain,
! [A: $i] :
( ( ( sk1 @ empty )
!= ( A @ empty ) )
| ( A @ function )
| ~ $true
| ( sk2 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[9418,111]) ).
thf(10162,plain,
! [A: $i] :
( ( ( sk1 @ empty )
!= ( A @ empty ) )
| ( A @ function )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[10161]) ).
thf(10163,plain,
( ( sk1 @ function )
| ( sk2 != empty_set ) ),
inference(pattern_uni,[status(thm)],[10162:[bind(A,$thf( sk1 ))]]) ).
thf(34079,plain,
( ( sk1 != sk1 )
| ( empty_set @ powerset @ ( sk3 @ relation_rng @ element ) )
| ( sk2 @ ( empty_set @ sk17 ) ) ),
inference(paramod_ordered,[status(thm)],[33940,6105]) ).
thf(34080,plain,
( ( empty_set @ powerset @ ( sk3 @ relation_rng @ element ) )
| ( sk2 @ ( empty_set @ sk17 ) ) ),
inference(pattern_uni,[status(thm)],[34079:[]]) ).
thf(7291,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk3 @ relation_rng @ in ) )
!= ( A @ ( B @ in ) ) )
| ~ $true
| ( ( B @ ( A @ identity_relation @ apply ) )
= B ) ),
inference(paramod_ordered,[status(thm)],[6235,7265]) ).
thf(7292,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk3 @ relation_rng @ in ) )
!= ( A @ ( B @ in ) ) )
| ( ( B @ ( A @ identity_relation @ apply ) )
= B ) ),
inference(simp,[status(thm)],[7291]) ).
thf(7293,plain,
( ( sk3 @ relation_rng @ ( sk1 @ powerset @ identity_relation @ apply ) )
= ( sk3 @ relation_rng ) ),
inference(pattern_uni,[status(thm)],[7292:[bind(A,$thf( sk1 @ powerset )),bind(B,$thf( sk3 @ relation_rng ))]]) ).
thf(198,plain,
! [B: $i,A: $i] :
( ( B
= ( A @ relation_rng ) )
| ~ ( B @ ( A @ sk17 ) )
| ( B @ ( A @ ( B @ sk18 ) @ in ) )
| ~ ( A @ function )
| ~ ( A @ relation ) ),
inference(cnfConj,[status(thm)],[194]) ).
thf(211,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ sk17 ) )
| ( B @ ( A @ ( B @ sk18 ) @ in ) )
| ~ ( A @ function )
| ~ ( A @ relation )
| ( B
= ( A @ relation_rng ) ) ),
inference(lifteq,[status(thm)],[198]) ).
thf(212,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ sk17 ) )
| ( B @ ( A @ ( B @ sk18 ) @ in ) )
| ~ ( A @ function )
| ~ ( A @ relation )
| ( B
= ( A @ relation_rng ) ) ),
inference(simp,[status(thm)],[211]) ).
thf(10157,plain,
( ( ( sk10 @ relation_rng @ empty )
!= ( sk1 @ empty ) )
| ~ $true
| ( sk2 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[9418,3328]) ).
thf(10158,plain,
( ( ( sk10 @ relation_rng @ empty )
!= ( sk1 @ empty ) )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[10157]) ).
thf(10180,plain,
( ( ( sk10 @ relation_rng )
!= sk1 )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[10158]) ).
thf(12065,plain,
! [A: $i] :
( ( A != sk2 )
| ( empty_set @ one_to_one )
| ( empty_set @ ( empty_set @ ( A @ sk20 ) @ in ) )
| ( A @ ( empty_set @ sk17 ) ) ),
inference(paramod_ordered,[status(thm)],[11958,46]) ).
thf(12066,plain,
( ( empty_set @ one_to_one )
| ( empty_set @ ( empty_set @ ( sk2 @ sk20 ) @ in ) )
| ( sk2 @ ( empty_set @ sk17 ) ) ),
inference(pattern_uni,[status(thm)],[12065:[bind(A,$thf( sk2 ))]]) ).
thf(20391,plain,
( ( empty_set @ one_to_one )
| $false
| ( sk2 @ ( empty_set @ sk17 ) ) ),
inference(rewrite,[status(thm)],[12066,578]) ).
thf(20392,plain,
( ( empty_set @ one_to_one )
| ( sk2 @ ( empty_set @ sk17 ) ) ),
inference(simp,[status(thm)],[20391]) ).
thf(4118,plain,
! [B: $i,A: $i] :
( ( ( sk11 @ relation_dom @ ( sk11 @ sk13 @ in ) )
!= ( B @ ( A @ in ) ) )
| ~ ( B @ empty )
| ~ $true
| ( sk11 @ one_to_one ) ),
inference(paramod_ordered,[status(thm)],[4117,69]) ).
thf(4119,plain,
! [B: $i,A: $i] :
( ( ( sk11 @ relation_dom @ ( sk11 @ sk13 @ in ) )
!= ( B @ ( A @ in ) ) )
| ~ ( B @ empty )
| ( sk11 @ one_to_one ) ),
inference(simp,[status(thm)],[4118]) ).
thf(4120,plain,
( ~ ( sk11 @ relation_dom @ empty )
| ( sk11 @ one_to_one ) ),
inference(pattern_uni,[status(thm)],[4119:[bind(A,$thf( sk11 @ sk13 )),bind(B,$thf( sk11 @ relation_dom ))]]) ).
thf(10550,plain,
( ( ( sk10 @ empty )
!= ( sk1 @ empty ) )
| ~ $true
| ( sk3 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[9460,124]) ).
thf(10551,plain,
( ( ( sk10 @ empty )
!= ( sk1 @ empty ) )
| ( sk3 != empty_set ) ),
inference(simp,[status(thm)],[10550]) ).
thf(10629,plain,
( ( sk10 != sk1 )
| ( sk3 != empty_set ) ),
inference(simp,[status(thm)],[10551]) ).
thf(13729,plain,
( ( sk2 != sk2 )
| ( empty_set != empty_set )
| ( sk1 = empty_set )
| ~ ( sk2 @ relation_rng @ empty ) ),
inference(paramod_ordered,[status(thm)],[5265,9620]) ).
thf(13730,plain,
( ( sk2 != sk2 )
| ( sk1 = empty_set )
| ~ ( sk2 @ relation_rng @ empty ) ),
inference(simp,[status(thm)],[13729]) ).
thf(13731,plain,
( ( sk1 = empty_set )
| ~ ( sk2 @ relation_rng @ empty ) ),
inference(pattern_uni,[status(thm)],[13730:[]]) ).
thf(37213,plain,
( ( sk2 != sk2 )
| ( sk1 @ one_to_one )
| ~ ( sk1 @ empty ) ),
inference(paramod_ordered,[status(thm)],[35432,46]) ).
thf(37214,plain,
( ( sk1 @ one_to_one )
| ~ ( sk1 @ empty ) ),
inference(pattern_uni,[status(thm)],[37213:[]]) ).
thf(10612,plain,
! [A: $i] :
( ( ( sk1 @ empty )
!= ( A @ empty ) )
| ( A @ function )
| ~ $true
| ( sk3 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[9460,111]) ).
thf(10613,plain,
! [A: $i] :
( ( ( sk1 @ empty )
!= ( A @ empty ) )
| ( A @ function )
| ( sk3 != empty_set ) ),
inference(simp,[status(thm)],[10612]) ).
thf(10614,plain,
( ( sk1 @ function )
| ( sk3 != empty_set ) ),
inference(pattern_uni,[status(thm)],[10613:[bind(A,$thf( sk1 ))]]) ).
thf(8359,plain,
! [A: $i] :
( ( A != sk9 )
| ( sk9 != sk5 )
| ( empty_set != empty_set )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[84,8278]) ).
thf(8360,plain,
! [A: $i] :
( ( A != sk9 )
| ( sk9 != sk5 )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[8359]) ).
thf(8361,plain,
( ( sk9 != sk5 )
| ~ ( sk9 @ empty ) ),
inference(pattern_uni,[status(thm)],[8360:[bind(A,$thf( sk9 ))]]) ).
thf(16535,plain,
( ( sk2 != sk2 )
| ( sk1 @ function )
| ( empty_set != empty_set )
| ~ ( sk2 @ relation_rng @ empty ) ),
inference(paramod_ordered,[status(thm)],[5265,10163]) ).
thf(16536,plain,
( ( sk2 != sk2 )
| ( sk1 @ function )
| ~ ( sk2 @ relation_rng @ empty ) ),
inference(simp,[status(thm)],[16535]) ).
thf(16537,plain,
( ( sk1 @ function )
| ~ ( sk2 @ relation_rng @ empty ) ),
inference(pattern_uni,[status(thm)],[16536:[]]) ).
thf(8376,plain,
! [A: $i] :
( ( A != sk9 )
| ( sk10 != sk9 )
| ( empty_set != empty_set )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[84,8288]) ).
thf(8377,plain,
! [A: $i] :
( ( A != sk9 )
| ( sk10 != sk9 )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[8376]) ).
thf(8378,plain,
( ( sk10 != sk9 )
| ~ ( sk9 @ empty ) ),
inference(pattern_uni,[status(thm)],[8377:[bind(A,$thf( sk9 ))]]) ).
thf(7644,plain,
! [A: $i] :
( ( ( sk9 @ empty )
!= ( A @ empty ) )
| ( A @ function )
| ~ $true
| ( ( sk9 @ relation_rng )
!= empty_set ) ),
inference(paramod_ordered,[status(thm)],[4104,111]) ).
thf(7645,plain,
! [A: $i] :
( ( ( sk9 @ empty )
!= ( A @ empty ) )
| ( A @ function )
| ( ( sk9 @ relation_rng )
!= empty_set ) ),
inference(simp,[status(thm)],[7644]) ).
thf(7646,plain,
( ( sk9 @ function )
| ( ( sk9 @ relation_rng )
!= empty_set ) ),
inference(pattern_uni,[status(thm)],[7645:[bind(A,$thf( sk9 ))]]) ).
thf(10554,plain,
! [A: $i] :
( ( ( sk1 @ empty )
!= ( A @ empty ) )
| ( A @ relation_rng @ relation )
| ~ $true
| ( sk3 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[9460,105]) ).
thf(10555,plain,
! [A: $i] :
( ( ( sk1 @ empty )
!= ( A @ empty ) )
| ( A @ relation_rng @ relation )
| ( sk3 != empty_set ) ),
inference(simp,[status(thm)],[10554]) ).
thf(10556,plain,
( ( sk1 @ relation_rng @ relation )
| ( sk3 != empty_set ) ),
inference(pattern_uni,[status(thm)],[10555:[bind(A,$thf( sk1 ))]]) ).
thf(3481,plain,
( ( ( sk2 @ empty )
!= ( sk2 @ empty ) )
| ( empty_set @ one_to_one )
| ~ $true
| ( ( sk2 @ relation_rng )
!= empty_set ) ),
inference(paramod_ordered,[status(thm)],[3190,1150]) ).
thf(3482,plain,
( ( ( sk2 @ empty )
!= ( sk2 @ empty ) )
| ( empty_set @ one_to_one )
| ( ( sk2 @ relation_rng )
!= empty_set ) ),
inference(simp,[status(thm)],[3481]) ).
thf(3483,plain,
( ( empty_set @ one_to_one )
| ( ( sk2 @ relation_rng )
!= empty_set ) ),
inference(pattern_uni,[status(thm)],[3482:[]]) ).
thf(5522,plain,
! [A: $i] :
( ( A
!= ( sk2 @ relation_rng ) )
| ( empty_set @ one_to_one )
| ( empty_set != empty_set )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[84,3483]) ).
thf(5523,plain,
! [A: $i] :
( ( A
!= ( sk2 @ relation_rng ) )
| ( empty_set @ one_to_one )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[5522]) ).
thf(5524,plain,
( ( empty_set @ one_to_one )
| ~ ( sk2 @ relation_rng @ empty ) ),
inference(pattern_uni,[status(thm)],[5523:[bind(A,$thf( sk2 @ relation_rng ))]]) ).
thf(1126,plain,
! [A: $i] :
( ( A
!= ( sk3 @ relation_dom ) )
| ( sk1 = empty_set )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[84,56]) ).
thf(1127,plain,
( ( sk1 = empty_set )
| ~ ( sk3 @ relation_dom @ empty ) ),
inference(pattern_uni,[status(thm)],[1126:[bind(A,$thf( sk3 @ relation_dom ))]]) ).
thf(2176,plain,
( ( sk1 = empty_set )
| ~ ( sk1 @ empty ) ),
inference(rewrite,[status(thm)],[1127,56]) ).
thf(5,axiom,
! [A: $i,B: $i,C: $i] :
~ ( ( C @ empty )
& ( C @ powerset @ ( B @ element ) )
& ( B @ ( A @ in ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t5_subset) ).
thf(64,plain,
! [A: $i,B: $i,C: $i] :
~ ( ( C @ empty )
& ( C @ powerset @ ( B @ element ) )
& ( B @ ( A @ in ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(146,plain,
! [A: $i] :
( ( A @ one_to_one )
| ( ( A @ sk12 @ ( A @ apply ) )
= ( A @ sk13 @ ( A @ apply ) ) )
| ~ ( A @ function )
| ~ ( A @ relation ) ),
inference(cnfConj,[status(thm)],[141]) ).
thf(149,plain,
! [A: $i] :
( ( A @ one_to_one )
| ~ ( A @ function )
| ~ ( A @ relation )
| ( ( A @ sk13 @ ( A @ apply ) )
= ( A @ sk12 @ ( A @ apply ) ) ) ),
inference(lifteq,[status(thm)],[146]) ).
thf(6703,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ in ) )
!= ( C @ ( B @ in ) ) )
| ~ ( B @ ( C @ in ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[6697,88]) ).
thf(6704,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ in ) )
!= ( C @ ( B @ in ) ) )
| ~ ( B @ ( C @ in ) ) ),
inference(simp,[status(thm)],[6703]) ).
thf(6705,plain,
! [A: $i] :
~ ( A @ ( A @ powerset @ in ) ),
inference(pattern_uni,[status(thm)],[6704:[bind(A,$thf( D )),bind(B,$thf( D )),bind(C,$thf( D @ powerset ))]]) ).
thf(6751,plain,
! [A: $i] :
~ ( A @ ( A @ powerset @ in ) ),
inference(simp,[status(thm)],[6705]) ).
thf(6985,plain,
! [B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ in ) )
!= ( B @ ( B @ powerset @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[6697,6751]) ).
thf(6986,plain,
! [B: $i,A: $i] :
( ( A @ powerset @ ( A @ in ) )
!= ( B @ ( B @ powerset @ in ) ) ),
inference(simp,[status(thm)],[6985]) ).
thf(6996,plain,
! [B: $i,A: $i] :
( ( ( A @ powerset )
!= B )
| ( A
!= ( B @ powerset ) ) ),
inference(simp,[status(thm)],[6986]) ).
thf(7010,plain,
! [A: $i] :
( ( A @ powerset @ powerset )
!= A ),
inference(simp,[status(thm)],[6996]) ).
thf(165,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ relation_composition ) @ relation )
| ~ ( B @ relation )
| ~ ( A @ empty ) )
& ( ( A @ ( B @ relation_composition ) @ empty )
| ~ ( B @ relation )
| ~ ( A @ empty ) ) ),
inference(cnf,[status(esa)],[164]) ).
thf(166,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ relation_composition ) @ empty )
| ~ ( B @ relation )
| ~ ( A @ empty ) ),
inference(cnfConj,[status(thm)],[165]) ).
thf(143,plain,
! [A: $i] :
( ( A @ one_to_one )
| ( ( A @ sk12 )
!= ( A @ sk13 ) )
| ~ ( A @ function )
| ~ ( A @ relation ) ),
inference(cnfConj,[status(thm)],[141]) ).
thf(148,plain,
! [A: $i] :
( ( A @ one_to_one )
| ~ ( A @ function )
| ~ ( A @ relation )
| ( ( A @ sk13 )
!= ( A @ sk12 ) ) ),
inference(lifteq,[status(thm)],[143]) ).
thf(5152,plain,
( ( ( sk11 @ empty )
!= ( sk10 @ empty ) )
| ~ $true
| ( sk11 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[5068,124]) ).
thf(5153,plain,
( ( ( sk11 @ empty )
!= ( sk10 @ empty ) )
| ( sk11 != empty_set ) ),
inference(simp,[status(thm)],[5152]) ).
thf(5215,plain,
( ( sk11 != sk10 )
| ( sk11 != empty_set ) ),
inference(simp,[status(thm)],[5153]) ).
thf(5228,plain,
! [A: $i] :
( ( A != sk11 )
| ( sk11 != sk10 )
| ( empty_set != empty_set )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[84,5215]) ).
thf(5229,plain,
! [A: $i] :
( ( A != sk11 )
| ( sk11 != sk10 )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[5228]) ).
thf(5230,plain,
( ( sk11 != sk10 )
| ~ ( sk11 @ empty ) ),
inference(pattern_uni,[status(thm)],[5229:[bind(A,$thf( sk11 ))]]) ).
thf(9601,plain,
( ( ( empty_set @ relation_dom )
!= ( empty_set @ relation_dom ) )
| ( sk1 @ relation )
| ( sk3 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[2256,9374]) ).
thf(9602,plain,
( ( sk1 @ relation )
| ( sk3 != empty_set ) ),
inference(pattern_uni,[status(thm)],[9601:[]]) ).
thf(4235,plain,
( ( ( sk5 @ empty )
!= ( sk3 @ empty ) )
| ~ $true
| ( ( sk3 @ relation_rng )
!= empty_set ) ),
inference(paramod_ordered,[status(thm)],[3220,74]) ).
thf(4236,plain,
( ( ( sk5 @ empty )
!= ( sk3 @ empty ) )
| ( ( sk3 @ relation_rng )
!= empty_set ) ),
inference(simp,[status(thm)],[4235]) ).
thf(4309,plain,
( ( sk5 != sk3 )
| ( ( sk3 @ relation_rng )
!= empty_set ) ),
inference(simp,[status(thm)],[4236]) ).
thf(4379,plain,
! [A: $i] :
( ( ( sk3 @ empty )
!= ( A @ empty ) )
| ( A @ relation_rng @ relation )
| ~ $true
| ( sk3 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[4314,105]) ).
thf(4380,plain,
! [A: $i] :
( ( ( sk3 @ empty )
!= ( A @ empty ) )
| ( A @ relation_rng @ relation )
| ( sk3 != empty_set ) ),
inference(simp,[status(thm)],[4379]) ).
thf(4381,plain,
( ( sk3 @ relation_rng @ relation )
| ( sk3 != empty_set ) ),
inference(pattern_uni,[status(thm)],[4380:[bind(A,$thf( sk3 ))]]) ).
thf(202,plain,
! [C: $i,B: $i,A: $i] :
( ( C
= ( A @ ( B @ ( C @ sk16 ) ) @ ( A @ apply ) ) )
| ~ ( B @ ( C @ in ) )
| ( B
!= ( A @ relation_rng ) )
| ~ ( A @ function )
| ~ ( A @ relation ) ),
inference(cnfConj,[status(thm)],[194]) ).
thf(203,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( B @ ( C @ in ) )
| ~ ( A @ function )
| ~ ( A @ relation )
| ( ( A @ ( B @ ( C @ sk16 ) ) @ ( A @ apply ) )
= C )
| ( B
!= ( A @ relation_rng ) ) ),
inference(lifteq,[status(thm)],[202]) ).
thf(204,plain,
! [B: $i,A: $i] :
( ~ ( A @ relation_rng @ ( B @ in ) )
| ~ ( A @ function )
| ~ ( A @ relation )
| ( ( A @ ( A @ relation_rng @ ( B @ sk16 ) ) @ ( A @ apply ) )
= B ) ),
inference(simp,[status(thm)],[203]) ).
thf(14867,plain,
( ( sk1 != sk1 )
| ( ( empty_set @ identity_relation )
!= empty_set )
| ~ ( sk3 @ empty )
| ~ ( sk3 @ empty ) ),
inference(paramod_ordered,[status(thm)],[9624,453]) ).
thf(14868,plain,
( ( sk1 != sk1 )
| ( ( empty_set @ identity_relation )
!= empty_set )
| ~ ( sk3 @ empty ) ),
inference(simp,[status(thm)],[14867]) ).
thf(14869,plain,
( ( ( empty_set @ identity_relation )
!= empty_set )
| ~ ( sk3 @ empty ) ),
inference(pattern_uni,[status(thm)],[14868:[]]) ).
thf(4976,plain,
! [A: $i] :
( ( ( sk11 @ empty )
!= ( A @ empty ) )
| ~ $true
| ( A = empty_set )
| ( ( sk11 @ relation_rng )
!= empty_set ) ),
inference(paramod_ordered,[status(thm)],[3160,84]) ).
thf(4977,plain,
! [A: $i] :
( ( ( sk11 @ empty )
!= ( A @ empty ) )
| ( A = empty_set )
| ( ( sk11 @ relation_rng )
!= empty_set ) ),
inference(simp,[status(thm)],[4976]) ).
thf(4978,plain,
( ( sk11 = empty_set )
| ( ( sk11 @ relation_rng )
!= empty_set ) ),
inference(pattern_uni,[status(thm)],[4977:[bind(A,$thf( sk11 ))]]) ).
thf(53,plain,
( ( sk2 @ ( sk3 @ relation_composition ) )
= sk2 ),
inference(cnfConj,[status(thm)],[43]) ).
thf(54,plain,
( ( sk2 @ ( sk3 @ relation_composition ) )
= sk2 ),
inference(lifteq,[status(thm)],[53]) ).
thf(38526,plain,
( ( sk1 != sk1 )
| ( empty_set != empty_set )
| ( sk2 @ empty )
| ( sk3 @ ( empty_set @ sk17 ) ) ),
inference(paramod_ordered,[status(thm)],[38511,35742]) ).
thf(38527,plain,
( ( sk1 != sk1 )
| ( sk2 @ empty )
| ( sk3 @ ( empty_set @ sk17 ) ) ),
inference(simp,[status(thm)],[38526]) ).
thf(38528,plain,
( ( sk2 @ empty )
| ( sk3 @ ( empty_set @ sk17 ) ) ),
inference(pattern_uni,[status(thm)],[38527:[]]) ).
thf(173,plain,
! [B: $i,A: $i] :
( ( B
= ( A @ identity_relation ) )
| ( ( A @ ( B @ sk15 ) @ ( B @ apply ) )
!= ( A @ ( B @ sk15 ) ) )
| ( ( B @ relation_dom )
!= A )
| ~ ( B @ function )
| ~ ( B @ relation ) ),
inference(cnfConj,[status(thm)],[169]) ).
thf(180,plain,
! [B: $i,A: $i] :
( ~ ( B @ function )
| ~ ( B @ relation )
| ( B
= ( A @ identity_relation ) )
| ( ( A @ ( B @ sk15 ) @ ( B @ apply ) )
!= ( A @ ( B @ sk15 ) ) )
| ( ( B @ relation_dom )
!= A ) ),
inference(lifteq,[status(thm)],[173]) ).
thf(181,plain,
! [A: $i] :
( ~ ( A @ function )
| ~ ( A @ relation )
| ( ( A @ relation_dom @ identity_relation )
= A )
| ( ( A @ relation_dom @ ( A @ sk15 ) @ ( A @ apply ) )
!= ( A @ relation_dom @ ( A @ sk15 ) ) ) ),
inference(simp,[status(thm)],[180]) ).
thf(5156,plain,
! [A: $i] :
( ( ( sk11 @ empty )
!= ( A @ empty ) )
| ( A @ relation_rng @ relation )
| ~ $true
| ( sk11 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[5068,105]) ).
thf(5157,plain,
! [A: $i] :
( ( ( sk11 @ empty )
!= ( A @ empty ) )
| ( A @ relation_rng @ relation )
| ( sk11 != empty_set ) ),
inference(simp,[status(thm)],[5156]) ).
thf(5158,plain,
( ( sk11 @ relation_rng @ relation )
| ( sk11 != empty_set ) ),
inference(pattern_uni,[status(thm)],[5157:[bind(A,$thf( sk11 ))]]) ).
thf(14941,plain,
( ( sk1 != sk1 )
| ( ( empty_set @ identity_relation )
!= sk3 )
| ~ ( sk3 @ empty ) ),
inference(paramod_ordered,[status(thm)],[9624,55]) ).
thf(14942,plain,
( ( ( empty_set @ identity_relation )
!= sk3 )
| ~ ( sk3 @ empty ) ),
inference(pattern_uni,[status(thm)],[14941:[]]) ).
thf(86,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ element ) )
| ~ ( C @ powerset @ ( B @ element ) )
| ~ ( B @ ( A @ in ) ) ),
inference(cnf,[status(esa)],[85]) ).
thf(8316,plain,
! [A: $i] :
( ( A != sk9 )
| ( sk9 @ function )
| ( empty_set != empty_set )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[84,8274]) ).
thf(8317,plain,
! [A: $i] :
( ( A != sk9 )
| ( sk9 @ function )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[8316]) ).
thf(8318,plain,
( ( sk9 @ function )
| ~ ( sk9 @ empty ) ),
inference(pattern_uni,[status(thm)],[8317:[bind(A,$thf( sk9 ))]]) ).
thf(3349,plain,
( ( ( sk10 @ relation_rng @ empty )
!= ( empty_set @ empty ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[75,3328]) ).
thf(3350,plain,
( ( sk10 @ relation_rng @ empty )
!= ( empty_set @ empty ) ),
inference(simp,[status(thm)],[3349]) ).
thf(3356,plain,
( ( sk10 @ relation_rng )
!= empty_set ),
inference(simp,[status(thm)],[3350]) ).
thf(12665,plain,
! [A: $i] :
( ( A
!= ( sk10 @ relation_rng ) )
| ( empty_set != empty_set )
| ( empty_set @ ( empty_set @ ( A @ sk20 ) @ in ) )
| ( A @ ( empty_set @ sk17 ) ) ),
inference(paramod_ordered,[status(thm)],[11958,3356]) ).
thf(12666,plain,
! [A: $i] :
( ( A
!= ( sk10 @ relation_rng ) )
| ( empty_set @ ( empty_set @ ( A @ sk20 ) @ in ) )
| ( A @ ( empty_set @ sk17 ) ) ),
inference(simp,[status(thm)],[12665]) ).
thf(12667,plain,
( ( empty_set @ ( empty_set @ ( sk10 @ relation_rng @ sk20 ) @ in ) )
| ( sk10 @ relation_rng @ ( empty_set @ sk17 ) ) ),
inference(pattern_uni,[status(thm)],[12666:[bind(A,$thf( sk10 @ relation_rng ))]]) ).
thf(25897,plain,
( $false
| ( sk10 @ relation_rng @ ( empty_set @ sk17 ) ) ),
inference(rewrite,[status(thm)],[12667,578]) ).
thf(25898,plain,
sk10 @ relation_rng @ ( empty_set @ sk17 ),
inference(simp,[status(thm)],[25897]) ).
thf(12419,plain,
! [A: $i] :
( ( A != sk2 )
| ( sk1 @ empty )
| ( empty_set != empty_set )
| ( empty_set @ ( empty_set @ ( A @ sk20 ) @ in ) )
| ( A @ ( empty_set @ sk17 ) ) ),
inference(paramod_ordered,[status(thm)],[11958,9418]) ).
thf(12420,plain,
! [A: $i] :
( ( A != sk2 )
| ( sk1 @ empty )
| ( empty_set @ ( empty_set @ ( A @ sk20 ) @ in ) )
| ( A @ ( empty_set @ sk17 ) ) ),
inference(simp,[status(thm)],[12419]) ).
thf(12421,plain,
( ( sk1 @ empty )
| ( empty_set @ ( empty_set @ ( sk2 @ sk20 ) @ in ) )
| ( sk2 @ ( empty_set @ sk17 ) ) ),
inference(pattern_uni,[status(thm)],[12420:[bind(A,$thf( sk2 ))]]) ).
thf(23938,plain,
( ( sk1 @ empty )
| $false
| ( sk2 @ ( empty_set @ sk17 ) ) ),
inference(rewrite,[status(thm)],[12421,578]) ).
thf(23939,plain,
( ( sk1 @ empty )
| ( sk2 @ ( empty_set @ sk17 ) ) ),
inference(simp,[status(thm)],[23938]) ).
thf(12639,plain,
! [A: $i] :
( ( A != sk3 )
| ( empty_set != empty_set )
| ( sk3 @ empty )
| ( empty_set @ ( empty_set @ ( A @ sk20 ) @ in ) )
| ( A @ ( empty_set @ sk17 ) ) ),
inference(paramod_ordered,[status(thm)],[11958,4314]) ).
thf(12640,plain,
! [A: $i] :
( ( A != sk3 )
| ( sk3 @ empty )
| ( empty_set @ ( empty_set @ ( A @ sk20 ) @ in ) )
| ( A @ ( empty_set @ sk17 ) ) ),
inference(simp,[status(thm)],[12639]) ).
thf(12641,plain,
( ( sk3 @ empty )
| ( empty_set @ ( empty_set @ ( sk3 @ sk20 ) @ in ) )
| ( sk3 @ ( empty_set @ sk17 ) ) ),
inference(pattern_uni,[status(thm)],[12640:[bind(A,$thf( sk3 ))]]) ).
thf(25517,plain,
( ( sk3 @ empty )
| $false
| ( sk3 @ ( empty_set @ sk17 ) ) ),
inference(rewrite,[status(thm)],[12641,578]) ).
thf(25518,plain,
( ( sk3 @ empty )
| ( sk3 @ ( empty_set @ sk17 ) ) ),
inference(simp,[status(thm)],[25517]) ).
thf(81,plain,
! [A: $i] :
( ~ ( A @ sk6 @ empty )
| ( A @ empty ) ),
inference(cnfConj,[status(thm)],[79]) ).
thf(7306,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ sk8 @ in ) )
!= ( B @ ( C @ in ) ) )
| ~ $true
| ( ( C @ ( B @ identity_relation @ apply ) )
= C )
| ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[791,7265]) ).
thf(7307,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ sk8 @ in ) )
!= ( B @ ( C @ in ) ) )
| ( ( C @ ( B @ identity_relation @ apply ) )
= C )
| ( A @ empty ) ),
inference(simp,[status(thm)],[7306]) ).
thf(7308,plain,
! [A: $i] :
( ( ( A @ sk8 @ ( A @ identity_relation @ apply ) )
= ( A @ sk8 ) )
| ( A @ empty ) ),
inference(pattern_uni,[status(thm)],[7307:[bind(A,$thf( D )),bind(B,$thf( D )),bind(C,$thf( D @ sk8 ))]]) ).
thf(7328,plain,
! [A: $i] :
( ( ( A @ sk8 @ ( A @ identity_relation @ apply ) )
= ( A @ sk8 ) )
| ( A @ empty ) ),
inference(simp,[status(thm)],[7308]) ).
thf(895,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ sk6 @ element ) )
!= ( C @ ( B @ element ) ) )
| ( C @ ( B @ in ) )
| ( C @ empty )
| ~ $true
| ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[80,77]) ).
thf(896,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ sk6 @ element ) )
!= ( C @ ( B @ element ) ) )
| ( C @ ( B @ in ) )
| ( C @ empty )
| ( A @ empty ) ),
inference(simp,[status(thm)],[895]) ).
thf(897,plain,
! [A: $i] :
( ( A @ powerset @ ( A @ sk6 @ in ) )
| ( A @ powerset @ empty )
| ( A @ empty ) ),
inference(pattern_uni,[status(thm)],[896:[bind(A,$thf( E )),bind(B,$thf( E @ sk6 )),bind(C,$thf( E @ powerset ))]]) ).
thf(901,plain,
! [A: $i] :
( ( A @ powerset @ ( A @ sk6 @ in ) )
| ( A @ powerset @ empty )
| ( A @ empty ) ),
inference(simp,[status(thm)],[897]) ).
thf(1606,plain,
! [A: $i] :
( ( A @ powerset @ ( A @ sk6 @ in ) )
| $false
| ( A @ empty ) ),
inference(rewrite,[status(thm)],[901,91]) ).
thf(1607,plain,
! [A: $i] :
( ( A @ powerset @ ( A @ sk6 @ in ) )
| ( A @ empty ) ),
inference(simp,[status(thm)],[1606]) ).
thf(7318,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ sk6 @ in ) )
!= ( B @ ( C @ in ) ) )
| ~ $true
| ( ( C @ ( B @ identity_relation @ apply ) )
= C )
| ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[1607,7265]) ).
thf(7319,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ sk6 @ in ) )
!= ( B @ ( C @ in ) ) )
| ( ( C @ ( B @ identity_relation @ apply ) )
= C )
| ( A @ empty ) ),
inference(simp,[status(thm)],[7318]) ).
thf(7320,plain,
! [A: $i] :
( ( ( A @ sk6 @ ( A @ powerset @ identity_relation @ apply ) )
= ( A @ sk6 ) )
| ( A @ empty ) ),
inference(pattern_uni,[status(thm)],[7319:[bind(A,$thf( E )),bind(B,$thf( E @ powerset )),bind(C,$thf( E @ sk6 ))]]) ).
thf(7330,plain,
! [A: $i] :
( ( ( A @ sk6 @ ( A @ powerset @ identity_relation @ apply ) )
= ( A @ sk6 ) )
| ( A @ empty ) ),
inference(simp,[status(thm)],[7320]) ).
thf(9569,plain,
( ( ( empty_set @ relation_dom )
!= ( empty_set @ relation_dom ) )
| ( sk1 @ relation )
| ( sk2 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[2541,9374]) ).
thf(9570,plain,
( ( sk1 @ relation )
| ( sk2 != empty_set ) ),
inference(pattern_uni,[status(thm)],[9569:[]]) ).
thf(4129,plain,
( ( ( sk11 @ relation_dom )
!= ( sk3 @ relation_dom ) )
| ( sk11 @ one_to_one )
| ( sk1 @ ( sk11 @ sk13 @ in ) ) ),
inference(paramod_ordered,[status(thm)],[56,4117]) ).
thf(4176,plain,
( ( sk11 != sk3 )
| ( sk11 @ one_to_one )
| ( sk1 @ ( sk11 @ sk13 @ in ) ) ),
inference(simp,[status(thm)],[4129]) ).
thf(35628,plain,
( ( ( sk2 @ empty )
!= ( sk2 @ empty ) )
| ( sk10 != sk1 )
| ~ $true
| ~ ( sk1 @ empty ) ),
inference(paramod_ordered,[status(thm)],[35289,10472]) ).
thf(35629,plain,
( ( ( sk2 @ empty )
!= ( sk2 @ empty ) )
| ( sk10 != sk1 )
| ~ ( sk1 @ empty ) ),
inference(simp,[status(thm)],[35628]) ).
thf(35630,plain,
( ( sk10 != sk1 )
| ~ ( sk1 @ empty ) ),
inference(pattern_uni,[status(thm)],[35629:[]]) ).
thf(12045,plain,
! [A: $i] :
( ( A != sk9 )
| ( empty_set != empty_set )
| ( sk9 @ empty )
| ( empty_set @ ( empty_set @ ( A @ sk20 ) @ in ) )
| ( A @ ( empty_set @ sk17 ) ) ),
inference(paramod_ordered,[status(thm)],[11958,7652]) ).
thf(12046,plain,
! [A: $i] :
( ( A != sk9 )
| ( sk9 @ empty )
| ( empty_set @ ( empty_set @ ( A @ sk20 ) @ in ) )
| ( A @ ( empty_set @ sk17 ) ) ),
inference(simp,[status(thm)],[12045]) ).
thf(12047,plain,
( ( sk9 @ empty )
| ( empty_set @ ( empty_set @ ( sk9 @ sk20 ) @ in ) )
| ( sk9 @ ( empty_set @ sk17 ) ) ),
inference(pattern_uni,[status(thm)],[12046:[bind(A,$thf( sk9 ))]]) ).
thf(19598,plain,
( ( sk9 @ empty )
| $false
| ( sk9 @ ( empty_set @ sk17 ) ) ),
inference(rewrite,[status(thm)],[12047,578]) ).
thf(19599,plain,
( ( sk9 @ empty )
| ( sk9 @ ( empty_set @ sk17 ) ) ),
inference(simp,[status(thm)],[19598]) ).
thf(9273,plain,
! [A: $i] :
( ( ( sk11 @ empty )
!= ( A @ empty ) )
| ( A @ relation_dom @ empty )
| ~ $true
| ( sk11 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[5068,190]) ).
thf(9274,plain,
! [A: $i] :
( ( ( sk11 @ empty )
!= ( A @ empty ) )
| ( A @ relation_dom @ empty )
| ( sk11 != empty_set ) ),
inference(simp,[status(thm)],[9273]) ).
thf(9275,plain,
( ( sk11 @ relation_dom @ empty )
| ( sk11 != empty_set ) ),
inference(pattern_uni,[status(thm)],[9274:[bind(A,$thf( sk11 ))]]) ).
thf(7549,plain,
! [A: $i] :
( ( ( sk9 @ empty )
!= ( A @ empty ) )
| ~ $true
| ( A = empty_set )
| ( ( sk9 @ relation_rng )
!= empty_set ) ),
inference(paramod_ordered,[status(thm)],[4104,84]) ).
thf(7550,plain,
! [A: $i] :
( ( ( sk9 @ empty )
!= ( A @ empty ) )
| ( A = empty_set )
| ( ( sk9 @ relation_rng )
!= empty_set ) ),
inference(simp,[status(thm)],[7549]) ).
thf(7551,plain,
( ( sk9 = empty_set )
| ( ( sk9 @ relation_rng )
!= empty_set ) ),
inference(pattern_uni,[status(thm)],[7550:[bind(A,$thf( sk9 ))]]) ).
thf(329,plain,
! [B: $i,A: $i] :
( ( B != sk3 )
| ( ( sk2 @ ( A @ relation_composition ) )
= sk2 )
| ~ ( B @ empty )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[61,54]) ).
thf(330,plain,
! [A: $i] :
( ( ( sk2 @ ( A @ relation_composition ) )
= sk2 )
| ~ ( sk3 @ empty )
| ~ ( A @ empty ) ),
inference(pattern_uni,[status(thm)],[329:[bind(A,$thf( A )),bind(B,$thf( sk3 ))]]) ).
thf(14908,plain,
( ( sk1 != sk1 )
| ~ ( sk3 @ empty )
| ~ ( empty_set @ identity_relation @ empty )
| ~ ( sk3 @ empty ) ),
inference(paramod_ordered,[status(thm)],[9624,362]) ).
thf(14909,plain,
( ( sk1 != sk1 )
| ~ ( empty_set @ identity_relation @ empty )
| ~ ( sk3 @ empty ) ),
inference(simp,[status(thm)],[14908]) ).
thf(14910,plain,
( ~ ( empty_set @ identity_relation @ empty )
| ~ ( sk3 @ empty ) ),
inference(pattern_uni,[status(thm)],[14909:[]]) ).
thf(65,plain,
~ ? [A: $i,B: $i] :
( ? [C: $i] :
( ( C @ empty )
& ( C @ powerset @ ( B @ element ) ) )
& ( B @ ( A @ in ) ) ),
inference(miniscope,[status(thm)],[64]) ).
thf(66,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ empty )
| ~ ( C @ powerset @ ( B @ element ) )
| ~ ( B @ ( A @ in ) ) ),
inference(cnf,[status(esa)],[65]) ).
thf(130,plain,
empty_set @ relation_empty_yielding,
inference(cnfConj,[status(thm)],[127]) ).
thf(5138,plain,
( ( ( sk11 @ empty )
!= ( sk5 @ empty ) )
| ~ $true
| ( sk11 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[5068,74]) ).
thf(5139,plain,
( ( ( sk11 @ empty )
!= ( sk5 @ empty ) )
| ( sk11 != empty_set ) ),
inference(simp,[status(thm)],[5138]) ).
thf(5218,plain,
( ( sk11 != sk5 )
| ( sk11 != empty_set ) ),
inference(simp,[status(thm)],[5139]) ).
thf(134,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( C @ ( B @ relation_composition ) @ apply ) )
= ( A @ ( B @ apply ) @ ( C @ apply ) ) )
| ~ ( B @ relation_dom @ ( A @ in ) )
| ~ ( C @ function )
| ~ ( C @ relation )
| ~ ( B @ function )
| ~ ( B @ relation ) ),
inference(cnf,[status(esa)],[133]) ).
thf(135,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( B @ relation_dom @ ( A @ in ) )
| ~ ( C @ function )
| ~ ( C @ relation )
| ~ ( B @ function )
| ~ ( B @ relation )
| ( ( A @ ( C @ ( B @ relation_composition ) @ apply ) )
= ( A @ ( B @ apply ) @ ( C @ apply ) ) ) ),
inference(lifteq,[status(thm)],[134]) ).
thf(10117,plain,
! [A: $i] :
( ( ( sk1 @ empty )
!= ( A @ empty ) )
| ( A @ relation_dom @ relation )
| ~ $true
| ( sk2 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[9418,191]) ).
thf(10118,plain,
! [A: $i] :
( ( ( sk1 @ empty )
!= ( A @ empty ) )
| ( A @ relation_dom @ relation )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[10117]) ).
thf(10119,plain,
( ( sk1 @ relation_dom @ relation )
| ( sk2 != empty_set ) ),
inference(pattern_uni,[status(thm)],[10118:[bind(A,$thf( sk1 ))]]) ).
thf(167,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ relation_composition ) @ relation )
| ~ ( B @ relation )
| ~ ( A @ empty ) ),
inference(cnfConj,[status(thm)],[165]) ).
thf(10541,plain,
( ( ( sk1 @ identity_relation @ empty )
!= ( sk1 @ empty ) )
| ( sk3 != empty_set )
| ~ $true
| ( sk3 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[9460,452]) ).
thf(10542,plain,
( ( ( sk1 @ identity_relation @ empty )
!= ( sk1 @ empty ) )
| ( sk3 != empty_set ) ),
inference(simp,[status(thm)],[10541]) ).
thf(10617,plain,
( ( ( sk1 @ identity_relation )
!= sk1 )
| ( sk3 != empty_set ) ),
inference(simp,[status(thm)],[10542]) ).
thf(35819,plain,
! [A: $i] :
( ( ( sk2 @ empty )
!= ( A @ empty ) )
| ~ $true
| ( A = empty_set )
| ( sk3 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[35311,84]) ).
thf(35820,plain,
! [A: $i] :
( ( ( sk2 @ empty )
!= ( A @ empty ) )
| ( A = empty_set )
| ( sk3 != empty_set ) ),
inference(simp,[status(thm)],[35819]) ).
thf(35821,plain,
( ( sk2 = empty_set )
| ( sk3 != empty_set ) ),
inference(pattern_uni,[status(thm)],[35820:[bind(A,$thf( sk2 ))]]) ).
thf(5846,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ sk8 @ element ) )
!= ( C @ powerset @ ( B @ element ) ) )
| ( C @ ( B @ subset ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[97,153]) ).
thf(5847,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ sk8 @ element ) )
!= ( C @ powerset @ ( B @ element ) ) )
| ( C @ ( B @ subset ) ) ),
inference(simp,[status(thm)],[5846]) ).
thf(5848,plain,
! [A: $i] : ( A @ ( A @ powerset @ sk8 @ subset ) ),
inference(pattern_uni,[status(thm)],[5847:[bind(A,$thf( E @ powerset )),bind(B,$thf( E @ powerset @ sk8 )),bind(C,$thf( E ))]]) ).
thf(5886,plain,
! [A: $i] : ( A @ ( A @ powerset @ sk8 @ subset ) ),
inference(simp,[status(thm)],[5848]) ).
thf(16547,plain,
! [A: $i] :
( ( A != sk2 )
| ( sk1 @ function )
| ( empty_set != empty_set )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[84,10163]) ).
thf(16548,plain,
! [A: $i] :
( ( A != sk2 )
| ( sk1 @ function )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[16547]) ).
thf(16549,plain,
( ( sk1 @ function )
| ~ ( sk2 @ empty ) ),
inference(pattern_uni,[status(thm)],[16548:[bind(A,$thf( sk2 ))]]) ).
thf(35671,plain,
( ( ( sk2 @ empty )
!= ( sk2 @ empty ) )
| ( sk1 @ function )
| ~ $true
| ~ ( sk1 @ empty ) ),
inference(paramod_ordered,[status(thm)],[35289,16549]) ).
thf(35672,plain,
( ( ( sk2 @ empty )
!= ( sk2 @ empty ) )
| ( sk1 @ function )
| ~ ( sk1 @ empty ) ),
inference(simp,[status(thm)],[35671]) ).
thf(35673,plain,
( ( sk1 @ function )
| ~ ( sk1 @ empty ) ),
inference(pattern_uni,[status(thm)],[35672:[]]) ).
thf(37927,plain,
( ( ( sk1 @ empty )
!= ( empty_set @ empty ) )
| ( sk1 @ function )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[75,35673]) ).
thf(37928,plain,
( ( ( sk1 @ empty )
!= ( empty_set @ empty ) )
| ( sk1 @ function ) ),
inference(simp,[status(thm)],[37927]) ).
thf(37959,plain,
( ( sk1 != empty_set )
| ( sk1 @ function ) ),
inference(simp,[status(thm)],[37928]) ).
thf(643,plain,
( ( ( sk1 @ identity_relation @ empty )
!= ( empty_set @ empty ) )
| ( sk3 != empty_set )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[75,452]) ).
thf(644,plain,
( ( ( sk1 @ identity_relation @ empty )
!= ( empty_set @ empty ) )
| ( sk3 != empty_set ) ),
inference(simp,[status(thm)],[643]) ).
thf(648,plain,
( ( ( sk1 @ identity_relation )
!= empty_set )
| ( sk3 != empty_set ) ),
inference(simp,[status(thm)],[644]) ).
thf(7188,plain,
! [A: $i] :
( ( A != sk3 )
| ( sk3 @ relation_rng @ relation )
| ( empty_set != empty_set )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[84,4381]) ).
thf(7189,plain,
! [A: $i] :
( ( A != sk3 )
| ( sk3 @ relation_rng @ relation )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[7188]) ).
thf(7190,plain,
( ( sk3 @ relation_rng @ relation )
| ~ ( sk3 @ empty ) ),
inference(pattern_uni,[status(thm)],[7189:[bind(A,$thf( sk3 ))]]) ).
thf(4564,plain,
! [A: $i] :
( ( A != sk3 )
| ( sk5 != sk3 )
| ( empty_set != empty_set )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[84,4425]) ).
thf(4565,plain,
! [A: $i] :
( ( A != sk3 )
| ( sk5 != sk3 )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[4564]) ).
thf(4566,plain,
( ( sk5 != sk3 )
| ~ ( sk3 @ empty ) ),
inference(pattern_uni,[status(thm)],[4565:[bind(A,$thf( sk3 ))]]) ).
thf(6979,plain,
! [B: $i,A: $i] :
( ( ( A @ powerset @ ( empty_set @ in ) )
!= ( B @ ( B @ powerset @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1453,6751]) ).
thf(6980,plain,
! [B: $i,A: $i] :
( ( A @ powerset @ ( empty_set @ in ) )
!= ( B @ ( B @ powerset @ in ) ) ),
inference(simp,[status(thm)],[6979]) ).
thf(6998,plain,
! [B: $i,A: $i] :
( ( ( A @ powerset )
!= B )
| ( ( B @ powerset )
!= empty_set ) ),
inference(simp,[status(thm)],[6980]) ).
thf(7013,plain,
! [A: $i] :
( ( A @ powerset @ powerset )
!= empty_set ),
inference(simp,[status(thm)],[6998]) ).
thf(9941,plain,
! [A: $i] :
( ( ( sk11 @ empty )
!= ( A @ empty ) )
| ( A @ relation_dom @ relation )
| ~ $true
| ( sk11 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[5068,191]) ).
thf(9942,plain,
! [A: $i] :
( ( ( sk11 @ empty )
!= ( A @ empty ) )
| ( A @ relation_dom @ relation )
| ( sk11 != empty_set ) ),
inference(simp,[status(thm)],[9941]) ).
thf(9943,plain,
( ( sk11 @ relation_dom @ relation )
| ( sk11 != empty_set ) ),
inference(pattern_uni,[status(thm)],[9942:[bind(A,$thf( sk11 ))]]) ).
thf(14938,plain,
( ( ( sk3 @ empty )
!= ( sk3 @ empty ) )
| ( sk1 = empty_set )
| ~ $true
| ( ( sk3 @ relation_rng )
!= empty_set ) ),
inference(paramod_ordered,[status(thm)],[3220,9624]) ).
thf(14939,plain,
( ( ( sk3 @ empty )
!= ( sk3 @ empty ) )
| ( sk1 = empty_set )
| ( ( sk3 @ relation_rng )
!= empty_set ) ),
inference(simp,[status(thm)],[14938]) ).
thf(14940,plain,
( ( sk1 = empty_set )
| ( ( sk3 @ relation_rng )
!= empty_set ) ),
inference(pattern_uni,[status(thm)],[14939:[]]) ).
thf(145,plain,
! [A: $i] :
( ( A @ one_to_one )
| ( A @ relation_dom @ ( A @ sk12 @ in ) )
| ~ ( A @ function )
| ~ ( A @ relation ) ),
inference(cnfConj,[status(thm)],[141]) ).
thf(327,plain,
! [B: $i,A: $i] :
( ( B
!= ( sk2 @ ( sk3 @ relation_composition ) ) )
| ( A = sk2 )
| ~ ( B @ empty )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[61,54]) ).
thf(328,plain,
! [A: $i] :
( ( A = sk2 )
| ~ ( sk2 @ ( sk3 @ relation_composition ) @ empty )
| ~ ( A @ empty ) ),
inference(pattern_uni,[status(thm)],[327:[bind(A,$thf( A )),bind(B,$thf( sk2 @ ( sk3 @ relation_composition ) ))]]) ).
thf(26323,plain,
! [A: $i] :
( ( A = sk2 )
| ~ ( sk2 @ empty )
| ~ ( A @ empty ) ),
inference(rewrite,[status(thm)],[328,54]) ).
thf(36254,plain,
( ( ( sk1 @ empty )
!= ( empty_set @ empty ) )
| ( sk10 != sk2 )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[75,35314]) ).
thf(36255,plain,
( ( ( sk1 @ empty )
!= ( empty_set @ empty ) )
| ( sk10 != sk2 ) ),
inference(simp,[status(thm)],[36254]) ).
thf(36277,plain,
( ( sk1 != empty_set )
| ( sk10 != sk2 ) ),
inference(simp,[status(thm)],[36255]) ).
thf(5020,plain,
( ( ( sk11 @ empty )
!= ( sk10 @ empty ) )
| ~ $true
| ( ( sk11 @ relation_rng )
!= empty_set ) ),
inference(paramod_ordered,[status(thm)],[3160,124]) ).
thf(5021,plain,
( ( ( sk11 @ empty )
!= ( sk10 @ empty ) )
| ( ( sk11 @ relation_rng )
!= empty_set ) ),
inference(simp,[status(thm)],[5020]) ).
thf(5079,plain,
( ( sk11 != sk10 )
| ( ( sk11 @ relation_rng )
!= empty_set ) ),
inference(simp,[status(thm)],[5021]) ).
thf(12018,plain,
! [A: $i] :
( ( A
!= ( sk1 @ powerset ) )
| ( empty_set != empty_set )
| ( empty_set @ ( empty_set @ ( A @ sk20 ) @ in ) )
| ( A @ ( empty_set @ sk17 ) ) ),
inference(paramod_ordered,[status(thm)],[11958,6306]) ).
thf(12019,plain,
! [A: $i] :
( ( A
!= ( sk1 @ powerset ) )
| ( empty_set @ ( empty_set @ ( A @ sk20 ) @ in ) )
| ( A @ ( empty_set @ sk17 ) ) ),
inference(simp,[status(thm)],[12018]) ).
thf(12020,plain,
( ( empty_set @ ( empty_set @ ( sk1 @ powerset @ sk20 ) @ in ) )
| ( sk1 @ powerset @ ( empty_set @ sk17 ) ) ),
inference(pattern_uni,[status(thm)],[12019:[bind(A,$thf( sk1 @ powerset ))]]) ).
thf(17942,plain,
( $false
| ( sk1 @ powerset @ ( empty_set @ sk17 ) ) ),
inference(rewrite,[status(thm)],[12020,578]) ).
thf(17943,plain,
sk1 @ powerset @ ( empty_set @ sk17 ),
inference(simp,[status(thm)],[17942]) ).
thf(50,plain,
sk3 @ function,
inference(cnfConj,[status(thm)],[43]) ).
thf(2481,plain,
! [A: $i] :
( ( ( A @ sk8 @ empty )
!= ( empty_set @ empty ) )
| ( A @ ( empty_set @ element ) )
| ( A @ empty )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[75,1347]) ).
thf(2482,plain,
! [A: $i] :
( ( ( A @ sk8 @ empty )
!= ( empty_set @ empty ) )
| ( A @ ( empty_set @ element ) )
| ( A @ empty ) ),
inference(simp,[status(thm)],[2481]) ).
thf(2486,plain,
! [A: $i] :
( ( ( A @ sk8 )
!= empty_set )
| ( A @ ( empty_set @ element ) )
| ( A @ empty ) ),
inference(simp,[status(thm)],[2482]) ).
thf(37435,plain,
( ( ( sk1 @ empty )
!= ( empty_set @ empty ) )
| ( sk2 = sk1 )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[75,35432]) ).
thf(37436,plain,
( ( ( sk1 @ empty )
!= ( empty_set @ empty ) )
| ( sk2 = sk1 ) ),
inference(simp,[status(thm)],[37435]) ).
thf(37501,plain,
( ( sk1 != empty_set )
| ( sk2 = sk1 ) ),
inference(simp,[status(thm)],[37436]) ).
thf(38522,plain,
( ( sk1 != sk1 )
| ( empty_set @ ( sk3 @ relation_rng @ subset ) )
| ( sk3 @ ( empty_set @ sk17 ) ) ),
inference(paramod_ordered,[status(thm)],[38511,52]) ).
thf(38523,plain,
( ( empty_set @ ( sk3 @ relation_rng @ subset ) )
| ( sk3 @ ( empty_set @ sk17 ) ) ),
inference(pattern_uni,[status(thm)],[38522:[]]) ).
thf(13183,plain,
! [A: $i] :
( ( A != sk3 )
| ( sk1 @ relation )
| ( empty_set != empty_set )
| ( empty_set @ ( empty_set @ ( A @ sk20 ) @ in ) )
| ( A @ ( empty_set @ sk17 ) ) ),
inference(paramod_ordered,[status(thm)],[11958,9602]) ).
thf(13184,plain,
! [A: $i] :
( ( A != sk3 )
| ( sk1 @ relation )
| ( empty_set @ ( empty_set @ ( A @ sk20 ) @ in ) )
| ( A @ ( empty_set @ sk17 ) ) ),
inference(simp,[status(thm)],[13183]) ).
thf(13185,plain,
( ( sk1 @ relation )
| ( empty_set @ ( empty_set @ ( sk3 @ sk20 ) @ in ) )
| ( sk3 @ ( empty_set @ sk17 ) ) ),
inference(pattern_uni,[status(thm)],[13184:[bind(A,$thf( sk3 ))]]) ).
thf(33386,plain,
( ( sk1 @ relation )
| $false
| ( sk3 @ ( empty_set @ sk17 ) ) ),
inference(rewrite,[status(thm)],[13185,578]) ).
thf(33387,plain,
( ( sk1 @ relation )
| ( sk3 @ ( empty_set @ sk17 ) ) ),
inference(simp,[status(thm)],[33386]) ).
thf(13088,plain,
! [A: $i] :
( ( A != sk2 )
| ( sk1 @ relation )
| ( empty_set != empty_set )
| ( empty_set @ ( empty_set @ ( A @ sk20 ) @ in ) )
| ( A @ ( empty_set @ sk17 ) ) ),
inference(paramod_ordered,[status(thm)],[11958,9570]) ).
thf(13089,plain,
! [A: $i] :
( ( A != sk2 )
| ( sk1 @ relation )
| ( empty_set @ ( empty_set @ ( A @ sk20 ) @ in ) )
| ( A @ ( empty_set @ sk17 ) ) ),
inference(simp,[status(thm)],[13088]) ).
thf(13090,plain,
( ( sk1 @ relation )
| ( empty_set @ ( empty_set @ ( sk2 @ sk20 ) @ in ) )
| ( sk2 @ ( empty_set @ sk17 ) ) ),
inference(pattern_uni,[status(thm)],[13089:[bind(A,$thf( sk2 ))]]) ).
thf(32892,plain,
( ( sk1 @ relation )
| $false
| ( sk2 @ ( empty_set @ sk17 ) ) ),
inference(rewrite,[status(thm)],[13090,578]) ).
thf(32893,plain,
( ( sk1 @ relation )
| ( sk2 @ ( empty_set @ sk17 ) ) ),
inference(simp,[status(thm)],[32892]) ).
thf(7794,plain,
! [A: $i] :
( ( A != sk3 )
| ( sk3 @ relation_rng @ empty )
| ( empty_set != empty_set )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[84,4407]) ).
thf(7795,plain,
! [A: $i] :
( ( A != sk3 )
| ( sk3 @ relation_rng @ empty )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[7794]) ).
thf(7796,plain,
( ( sk3 @ relation_rng @ empty )
| ~ ( sk3 @ empty ) ),
inference(pattern_uni,[status(thm)],[7795:[bind(A,$thf( sk3 ))]]) ).
thf(10142,plain,
! [A: $i] :
( ( ( sk1 @ empty )
!= ( A @ empty ) )
| ( A @ relation_rng @ empty )
| ~ $true
| ( sk2 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[9418,104]) ).
thf(10143,plain,
! [A: $i] :
( ( ( sk1 @ empty )
!= ( A @ empty ) )
| ( A @ relation_rng @ empty )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[10142]) ).
thf(10144,plain,
( ( sk1 @ relation_rng @ empty )
| ( sk2 != empty_set ) ),
inference(pattern_uni,[status(thm)],[10143:[bind(A,$thf( sk1 ))]]) ).
thf(5187,plain,
( ( ( sk10 @ relation_rng @ empty )
!= ( sk11 @ empty ) )
| ~ $true
| ( sk11 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[5068,3328]) ).
thf(5188,plain,
( ( ( sk10 @ relation_rng @ empty )
!= ( sk11 @ empty ) )
| ( sk11 != empty_set ) ),
inference(simp,[status(thm)],[5187]) ).
thf(5208,plain,
( ( ( sk10 @ relation_rng )
!= sk11 )
| ( sk11 != empty_set ) ),
inference(simp,[status(thm)],[5188]) ).
thf(7321,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ in ) )
!= ( B @ ( C @ in ) ) )
| ~ $true
| ( ( C @ ( B @ identity_relation @ apply ) )
= C ) ),
inference(paramod_ordered,[status(thm)],[6697,7265]) ).
thf(7322,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ in ) )
!= ( B @ ( C @ in ) ) )
| ( ( C @ ( B @ identity_relation @ apply ) )
= C ) ),
inference(simp,[status(thm)],[7321]) ).
thf(7323,plain,
! [A: $i] :
( ( A @ ( A @ powerset @ identity_relation @ apply ) )
= A ),
inference(pattern_uni,[status(thm)],[7322:[bind(A,$thf( D )),bind(B,$thf( D @ powerset )),bind(C,$thf( D ))]]) ).
thf(7331,plain,
! [A: $i] :
( ( A @ ( A @ powerset @ identity_relation @ apply ) )
= A ),
inference(simp,[status(thm)],[7323]) ).
thf(34001,plain,
( ( sk1 != sk1 )
| ( empty_set @ powerset @ ( sk3 @ relation_rng @ in ) )
| ( sk2 @ ( empty_set @ sk17 ) ) ),
inference(paramod_ordered,[status(thm)],[33940,6235]) ).
thf(34002,plain,
( ( empty_set @ powerset @ ( sk3 @ relation_rng @ in ) )
| ( sk2 @ ( empty_set @ sk17 ) ) ),
inference(pattern_uni,[status(thm)],[34001:[]]) ).
thf(313,plain,
! [B: $i,A: $i] :
( ( B != sk2 )
| ( ( A @ relation_dom )
= sk1 )
| ~ ( B @ empty )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[61,57]) ).
thf(314,plain,
! [A: $i] :
( ( ( A @ relation_dom )
= sk1 )
| ~ ( sk2 @ empty )
| ~ ( A @ empty ) ),
inference(pattern_uni,[status(thm)],[313:[bind(A,$thf( A )),bind(B,$thf( sk2 ))]]) ).
thf(36405,plain,
( ( ( sk1 @ empty )
!= ( empty_set @ empty ) )
| ( sk5 != sk2 )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[75,35334]) ).
thf(36406,plain,
( ( ( sk1 @ empty )
!= ( empty_set @ empty ) )
| ( sk5 != sk2 ) ),
inference(simp,[status(thm)],[36405]) ).
thf(36440,plain,
( ( sk1 != empty_set )
| ( sk5 != sk2 ) ),
inference(simp,[status(thm)],[36406]) ).
thf(38401,plain,
! [A: $i] :
( ( A != sk3 )
| ( sk10 != sk2 )
| ( empty_set != empty_set )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[84,35794]) ).
thf(38402,plain,
! [A: $i] :
( ( A != sk3 )
| ( sk10 != sk2 )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[38401]) ).
thf(38403,plain,
( ( sk10 != sk2 )
| ~ ( sk3 @ empty ) ),
inference(pattern_uni,[status(thm)],[38402:[bind(A,$thf( sk3 ))]]) ).
thf(17065,plain,
! [A: $i] :
( ( A != sk3 )
| ( sk1 @ function )
| ( empty_set != empty_set )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[84,10614]) ).
thf(17066,plain,
! [A: $i] :
( ( A != sk3 )
| ( sk1 @ function )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[17065]) ).
thf(17067,plain,
( ( sk1 @ function )
| ~ ( sk3 @ empty ) ),
inference(pattern_uni,[status(thm)],[17066:[bind(A,$thf( sk3 ))]]) ).
thf(249,plain,
! [B: $i,A: $i] :
( ( B != sk3 )
| ( ( A @ relation_dom )
= sk1 )
| ~ ( B @ empty )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[61,56]) ).
thf(250,plain,
! [A: $i] :
( ( ( A @ relation_dom )
= sk1 )
| ~ ( sk3 @ empty )
| ~ ( A @ empty ) ),
inference(pattern_uni,[status(thm)],[249:[bind(A,$thf( A )),bind(B,$thf( sk3 ))]]) ).
thf(35809,plain,
( ( ( sk2 @ empty )
!= ( sk2 @ empty ) )
| ( sk5 != sk2 )
| ~ $true
| ( sk3 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[35311,3866]) ).
thf(35810,plain,
( ( ( sk2 @ empty )
!= ( sk2 @ empty ) )
| ( sk5 != sk2 )
| ( sk3 != empty_set ) ),
inference(simp,[status(thm)],[35809]) ).
thf(35811,plain,
( ( sk5 != sk2 )
| ( sk3 != empty_set ) ),
inference(pattern_uni,[status(thm)],[35810:[]]) ).
thf(7821,plain,
( ( ( sk3 @ relation_rng @ empty )
!= ( sk5 @ empty ) )
| ~ $true
| ( sk3 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[4407,74]) ).
thf(7822,plain,
( ( ( sk3 @ relation_rng @ empty )
!= ( sk5 @ empty ) )
| ( sk3 != empty_set ) ),
inference(simp,[status(thm)],[7821]) ).
thf(7904,plain,
( ( ( sk3 @ relation_rng )
!= sk5 )
| ( sk3 != empty_set ) ),
inference(simp,[status(thm)],[7822]) ).
thf(17679,plain,
! [A: $i] :
( ( ( A @ relation_dom @ empty )
!= ( sk11 @ relation_dom @ empty ) )
| ~ $true
| ( sk11 @ one_to_one )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[190,4120]) ).
thf(17680,plain,
! [A: $i] :
( ( ( A @ relation_dom @ empty )
!= ( sk11 @ relation_dom @ empty ) )
| ( sk11 @ one_to_one )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[17679]) ).
thf(17681,plain,
( ( sk11 @ one_to_one )
| ~ ( sk11 @ empty ) ),
inference(pattern_uni,[status(thm)],[17680:[bind(A,$thf( sk11 ))]]) ).
thf(19454,plain,
( ( ( sk11 @ empty )
!= ( sk11 @ empty ) )
| ( sk11 @ one_to_one )
| ~ $true
| ( sk11 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[5068,17681]) ).
thf(19455,plain,
( ( ( sk11 @ empty )
!= ( sk11 @ empty ) )
| ( sk11 @ one_to_one )
| ( sk11 != empty_set ) ),
inference(simp,[status(thm)],[19454]) ).
thf(19456,plain,
( ( sk11 @ one_to_one )
| ( sk11 != empty_set ) ),
inference(pattern_uni,[status(thm)],[19455:[]]) ).
thf(4156,plain,
! [A: $i] :
( ( ( sk11 @ relation_dom @ ( sk11 @ sk13 @ in ) )
!= ( empty_set @ ( A @ in ) ) )
| ~ $true
| ( sk11 @ one_to_one ) ),
inference(paramod_ordered,[status(thm)],[4117,578]) ).
thf(4157,plain,
! [A: $i] :
( ( ( sk11 @ relation_dom @ ( sk11 @ sk13 @ in ) )
!= ( empty_set @ ( A @ in ) ) )
| ( sk11 @ one_to_one ) ),
inference(simp,[status(thm)],[4156]) ).
thf(4180,plain,
! [A: $i] :
( ( ( sk11 @ relation_dom )
!= empty_set )
| ( ( sk11 @ sk13 )
!= A )
| ( sk11 @ one_to_one ) ),
inference(simp,[status(thm)],[4157]) ).
thf(4185,plain,
( ( ( sk11 @ relation_dom )
!= empty_set )
| ( sk11 @ one_to_one ) ),
inference(simp,[status(thm)],[4180]) ).
thf(200,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ relation_dom @ ( A @ ( B @ ( C @ sk16 ) ) @ in ) )
| ~ ( B @ ( C @ in ) )
| ( B
!= ( A @ relation_rng ) )
| ~ ( A @ function )
| ~ ( A @ relation ) ),
inference(cnfConj,[status(thm)],[194]) ).
thf(217,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ relation_dom @ ( A @ ( B @ ( C @ sk16 ) ) @ in ) )
| ~ ( B @ ( C @ in ) )
| ~ ( A @ function )
| ~ ( A @ relation )
| ( B
!= ( A @ relation_rng ) ) ),
inference(lifteq,[status(thm)],[200]) ).
thf(218,plain,
! [B: $i,A: $i] :
( ( A @ relation_dom @ ( A @ ( A @ relation_rng @ ( B @ sk16 ) ) @ in ) )
| ~ ( A @ relation_rng @ ( B @ in ) )
| ~ ( A @ function )
| ~ ( A @ relation ) ),
inference(simp,[status(thm)],[217]) ).
thf(7887,plain,
! [A: $i] :
( ( ( sk3 @ relation_rng @ empty )
!= ( A @ empty ) )
| ( A @ function )
| ~ $true
| ( sk3 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[4407,111]) ).
thf(7888,plain,
! [A: $i] :
( ( ( sk3 @ relation_rng @ empty )
!= ( A @ empty ) )
| ( A @ function )
| ( sk3 != empty_set ) ),
inference(simp,[status(thm)],[7887]) ).
thf(7889,plain,
( ( sk3 @ relation_rng @ function )
| ( sk3 != empty_set ) ),
inference(pattern_uni,[status(thm)],[7888:[bind(A,$thf( sk3 @ relation_rng ))]]) ).
thf(8266,plain,
( ( ( sk10 @ relation_rng @ empty )
!= ( sk9 @ empty ) )
| ~ $true
| ( sk9 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[7652,3328]) ).
thf(8267,plain,
( ( ( sk10 @ relation_rng @ empty )
!= ( sk9 @ empty ) )
| ( sk9 != empty_set ) ),
inference(simp,[status(thm)],[8266]) ).
thf(8285,plain,
( ( ( sk10 @ relation_rng )
!= sk9 )
| ( sk9 != empty_set ) ),
inference(simp,[status(thm)],[8267]) ).
thf(5858,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ ( empty_set @ element ) )
!= ( C @ powerset @ ( B @ element ) ) )
| ( C @ ( B @ subset ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1405,153]) ).
thf(5859,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ ( empty_set @ element ) )
!= ( C @ powerset @ ( B @ element ) ) )
| ( C @ ( B @ subset ) ) ),
inference(simp,[status(thm)],[5858]) ).
thf(5860,plain,
! [A: $i] : ( A @ ( empty_set @ subset ) ),
inference(pattern_uni,[status(thm)],[5859:[bind(A,$thf( A )),bind(B,$thf( empty_set )),bind(C,$thf( A ))]]) ).
thf(5182,plain,
! [A: $i] :
( ( ( sk11 @ empty )
!= ( A @ empty ) )
| ( A @ relation_rng @ empty )
| ~ $true
| ( sk11 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[5068,104]) ).
thf(5183,plain,
! [A: $i] :
( ( ( sk11 @ empty )
!= ( A @ empty ) )
| ( A @ relation_rng @ empty )
| ( sk11 != empty_set ) ),
inference(simp,[status(thm)],[5182]) ).
thf(5184,plain,
( ( sk11 @ relation_rng @ empty )
| ( sk11 != empty_set ) ),
inference(pattern_uni,[status(thm)],[5183:[bind(A,$thf( sk11 ))]]) ).
thf(2161,plain,
! [A: $i] :
( ( ( A @ sk8 @ empty )
!= ( empty_set @ empty ) )
| ( A @ ( empty_set @ in ) )
| ( A @ empty )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[75,1343]) ).
thf(2162,plain,
! [A: $i] :
( ( ( A @ sk8 @ empty )
!= ( empty_set @ empty ) )
| ( A @ ( empty_set @ in ) )
| ( A @ empty ) ),
inference(simp,[status(thm)],[2161]) ).
thf(2167,plain,
! [A: $i] :
( ( ( A @ sk8 )
!= empty_set )
| ( A @ ( empty_set @ in ) )
| ( A @ empty ) ),
inference(simp,[status(thm)],[2162]) ).
thf(10603,plain,
! [A: $i] :
( ( ( sk1 @ empty )
!= ( A @ empty ) )
| ( A @ relation_dom @ empty )
| ~ $true
| ( sk3 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[9460,190]) ).
thf(10604,plain,
! [A: $i] :
( ( ( sk1 @ empty )
!= ( A @ empty ) )
| ( A @ relation_dom @ empty )
| ( sk3 != empty_set ) ),
inference(simp,[status(thm)],[10603]) ).
thf(10605,plain,
( ( sk1 @ relation_dom @ empty )
| ( sk3 != empty_set ) ),
inference(pattern_uni,[status(thm)],[10604:[bind(A,$thf( sk1 ))]]) ).
thf(13002,plain,
( ( sk2 != sk2 )
| ( sk1 @ relation )
| ( empty_set != empty_set )
| ~ ( sk2 @ relation_rng @ empty ) ),
inference(paramod_ordered,[status(thm)],[5265,9570]) ).
thf(13003,plain,
( ( sk2 != sk2 )
| ( sk1 @ relation )
| ~ ( sk2 @ relation_rng @ empty ) ),
inference(simp,[status(thm)],[13002]) ).
thf(13004,plain,
( ( sk1 @ relation )
| ~ ( sk2 @ relation_rng @ empty ) ),
inference(pattern_uni,[status(thm)],[13003:[]]) ).
thf(36706,plain,
( ( ( sk1 @ empty )
!= ( empty_set @ empty ) )
| ( sk10 != sk1 )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[75,35630]) ).
thf(36707,plain,
( ( ( sk1 @ empty )
!= ( empty_set @ empty ) )
| ( sk10 != sk1 ) ),
inference(simp,[status(thm)],[36706]) ).
thf(36740,plain,
( ( sk1 != empty_set )
| ( sk10 != sk1 ) ),
inference(simp,[status(thm)],[36707]) ).
thf(8615,plain,
! [A: $i] :
( ( ( A @ relation_rng @ empty )
!= ( sk2 @ relation_rng @ empty ) )
| ( sk2 = empty_set )
| ~ $true
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[104,5265]) ).
thf(8616,plain,
! [A: $i] :
( ( ( A @ relation_rng @ empty )
!= ( sk2 @ relation_rng @ empty ) )
| ( sk2 = empty_set )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[8615]) ).
thf(8617,plain,
( ( sk2 = empty_set )
| ~ ( sk2 @ empty ) ),
inference(pattern_uni,[status(thm)],[8616:[bind(A,$thf( sk2 ))]]) ).
thf(2443,plain,
( ( ( sk1 @ empty )
!= ( empty_set @ empty ) )
| ( ( empty_set @ identity_relation )
!= sk3 )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[75,1302]) ).
thf(2444,plain,
( ( ( sk1 @ empty )
!= ( empty_set @ empty ) )
| ( ( empty_set @ identity_relation )
!= sk3 ) ),
inference(simp,[status(thm)],[2443]) ).
thf(2447,plain,
( ( sk1 != empty_set )
| ( ( empty_set @ identity_relation )
!= sk3 ) ),
inference(simp,[status(thm)],[2444]) ).
thf(3465,plain,
( ( ( sk5 @ empty )
!= ( sk2 @ empty ) )
| ~ $true
| ( ( sk2 @ relation_rng )
!= empty_set ) ),
inference(paramod_ordered,[status(thm)],[3190,74]) ).
thf(3466,plain,
( ( ( sk5 @ empty )
!= ( sk2 @ empty ) )
| ( ( sk2 @ relation_rng )
!= empty_set ) ),
inference(simp,[status(thm)],[3465]) ).
thf(3529,plain,
( ( sk5 != sk2 )
| ( ( sk2 @ relation_rng )
!= empty_set ) ),
inference(simp,[status(thm)],[3466]) ).
thf(10598,plain,
! [A: $i] :
( ( ( sk1 @ empty )
!= ( A @ empty ) )
| ( A @ relation_rng @ empty )
| ~ $true
| ( sk3 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[9460,104]) ).
thf(10599,plain,
! [A: $i] :
( ( ( sk1 @ empty )
!= ( A @ empty ) )
| ( A @ relation_rng @ empty )
| ( sk3 != empty_set ) ),
inference(simp,[status(thm)],[10598]) ).
thf(10600,plain,
( ( sk1 @ relation_rng @ empty )
| ( sk3 != empty_set ) ),
inference(pattern_uni,[status(thm)],[10599:[bind(A,$thf( sk1 ))]]) ).
thf(199,plain,
! [B: $i,A: $i] :
( ( B
= ( A @ relation_rng ) )
| ~ ( B @ ( A @ ( B @ sk19 ) @ in ) )
| ( B @ ( A @ sk17 ) )
| ~ ( A @ function )
| ~ ( A @ relation ) ),
inference(cnfConj,[status(thm)],[194]) ).
thf(213,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ ( B @ sk19 ) @ in ) )
| ( B @ ( A @ sk17 ) )
| ~ ( A @ function )
| ~ ( A @ relation )
| ( B
= ( A @ relation_rng ) ) ),
inference(lifteq,[status(thm)],[199]) ).
thf(214,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ ( B @ sk19 ) @ in ) )
| ( B @ ( A @ sk17 ) )
| ~ ( A @ function )
| ~ ( A @ relation )
| ( B
= ( A @ relation_rng ) ) ),
inference(simp,[status(thm)],[213]) ).
thf(289,plain,
! [B: $i,A: $i] :
( ( B
!= ( sk3 @ relation_rng ) )
| ( sk1 @ ( A @ subset ) )
| ~ ( B @ empty )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[61,52]) ).
thf(290,plain,
! [A: $i] :
( ( sk1 @ ( A @ subset ) )
| ~ ( sk3 @ relation_rng @ empty )
| ~ ( A @ empty ) ),
inference(pattern_uni,[status(thm)],[289:[bind(A,$thf( A )),bind(B,$thf( sk3 @ relation_rng ))]]) ).
thf(15107,plain,
( ( ( sk3 @ empty )
!= ( sk3 @ empty ) )
| ( sk5 != sk1 )
| ~ $true
| ( ( sk3 @ relation_rng )
!= empty_set ) ),
inference(paramod_ordered,[status(thm)],[3220,13681]) ).
thf(15108,plain,
( ( ( sk3 @ empty )
!= ( sk3 @ empty ) )
| ( sk5 != sk1 )
| ( ( sk3 @ relation_rng )
!= empty_set ) ),
inference(simp,[status(thm)],[15107]) ).
thf(15109,plain,
( ( sk5 != sk1 )
| ( ( sk3 @ relation_rng )
!= empty_set ) ),
inference(pattern_uni,[status(thm)],[15108:[]]) ).
thf(16190,plain,
! [A: $i] :
( ( A
!= ( sk11 @ relation_rng ) )
| ( sk11 != sk10 )
| ( empty_set != empty_set )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[84,5079]) ).
thf(16191,plain,
! [A: $i] :
( ( A
!= ( sk11 @ relation_rng ) )
| ( sk11 != sk10 )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[16190]) ).
thf(16192,plain,
( ( sk11 != sk10 )
| ~ ( sk11 @ relation_rng @ empty ) ),
inference(pattern_uni,[status(thm)],[16191:[bind(A,$thf( sk11 @ relation_rng ))]]) ).
thf(35899,plain,
( ( ( sk2 @ empty )
!= ( sk2 @ empty ) )
| ( empty_set @ one_to_one )
| ~ $true
| ( sk3 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[35311,1150]) ).
thf(35900,plain,
( ( ( sk2 @ empty )
!= ( sk2 @ empty ) )
| ( empty_set @ one_to_one )
| ( sk3 != empty_set ) ),
inference(simp,[status(thm)],[35899]) ).
thf(35901,plain,
( ( empty_set @ one_to_one )
| ( sk3 != empty_set ) ),
inference(pattern_uni,[status(thm)],[35900:[]]) ).
thf(10039,plain,
( ( sk2 != sk2 )
| ( sk1 @ empty )
| ( empty_set != empty_set )
| ~ ( sk2 @ relation_rng @ empty ) ),
inference(paramod_ordered,[status(thm)],[5265,9418]) ).
thf(10040,plain,
( ( sk2 != sk2 )
| ( sk1 @ empty )
| ~ ( sk2 @ relation_rng @ empty ) ),
inference(simp,[status(thm)],[10039]) ).
thf(10041,plain,
( ( sk1 @ empty )
| ~ ( sk2 @ relation_rng @ empty ) ),
inference(pattern_uni,[status(thm)],[10040:[]]) ).
thf(13655,plain,
! [A: $i] :
( ( A != sk3 )
| ( sk10 != sk1 )
| ( empty_set != empty_set )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[84,10629]) ).
thf(13656,plain,
! [A: $i] :
( ( A != sk3 )
| ( sk10 != sk1 )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[13655]) ).
thf(13657,plain,
( ( sk10 != sk1 )
| ~ ( sk3 @ empty ) ),
inference(pattern_uni,[status(thm)],[13656:[bind(A,$thf( sk3 ))]]) ).
thf(15025,plain,
( ( ( sk3 @ empty )
!= ( sk3 @ empty ) )
| ( sk10 != sk1 )
| ~ $true
| ( ( sk3 @ relation_rng )
!= empty_set ) ),
inference(paramod_ordered,[status(thm)],[3220,13657]) ).
thf(15026,plain,
( ( ( sk3 @ empty )
!= ( sk3 @ empty ) )
| ( sk10 != sk1 )
| ( ( sk3 @ relation_rng )
!= empty_set ) ),
inference(simp,[status(thm)],[15025]) ).
thf(15027,plain,
( ( sk10 != sk1 )
| ( ( sk3 @ relation_rng )
!= empty_set ) ),
inference(pattern_uni,[status(thm)],[15026:[]]) ).
thf(5245,plain,
! [A: $i] :
( ( A != sk11 )
| ( sk11 != sk5 )
| ( empty_set != empty_set )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[84,5218]) ).
thf(5246,plain,
! [A: $i] :
( ( A != sk11 )
| ( sk11 != sk5 )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[5245]) ).
thf(5247,plain,
( ( sk11 != sk5 )
| ~ ( sk11 @ empty ) ),
inference(pattern_uni,[status(thm)],[5246:[bind(A,$thf( sk11 ))]]) ).
thf(588,plain,
! [A: $i] :
( ( ( A @ powerset @ empty )
!= ( empty_set @ empty ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[75,91]) ).
thf(589,plain,
! [A: $i] :
( ( A @ powerset @ empty )
!= ( empty_set @ empty ) ),
inference(simp,[status(thm)],[588]) ).
thf(603,plain,
! [A: $i] :
( ( A @ powerset )
!= empty_set ),
inference(simp,[status(thm)],[589]) ).
thf(197,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)],[194]) ).
thf(209,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)],[197]) ).
thf(210,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)],[209]) ).
thf(267,plain,
! [B: $i,A: $i] :
( ( B != sk1 )
| ( ( A @ identity_relation )
!= sk3 )
| ~ ( B @ empty )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[61,55]) ).
thf(268,plain,
! [A: $i] :
( ( ( A @ identity_relation )
!= sk3 )
| ~ ( sk1 @ empty )
| ~ ( A @ empty ) ),
inference(pattern_uni,[status(thm)],[267:[bind(A,$thf( A )),bind(B,$thf( sk1 ))]]) ).
thf(10608,plain,
( ( ( sk10 @ relation_rng @ empty )
!= ( sk1 @ empty ) )
| ~ $true
| ( sk3 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[9460,3328]) ).
thf(10609,plain,
( ( ( sk10 @ relation_rng @ empty )
!= ( sk1 @ empty ) )
| ( sk3 != empty_set ) ),
inference(simp,[status(thm)],[10608]) ).
thf(10622,plain,
( ( ( sk10 @ relation_rng )
!= sk1 )
| ( sk3 != empty_set ) ),
inference(simp,[status(thm)],[10609]) ).
thf(12157,plain,
! [A: $i] :
( ( A != sk9 )
| ( sk9 @ function )
| ( empty_set != empty_set )
| ( empty_set @ ( empty_set @ ( A @ sk20 ) @ in ) )
| ( A @ ( empty_set @ sk17 ) ) ),
inference(paramod_ordered,[status(thm)],[11958,8274]) ).
thf(12158,plain,
! [A: $i] :
( ( A != sk9 )
| ( sk9 @ function )
| ( empty_set @ ( empty_set @ ( A @ sk20 ) @ in ) )
| ( A @ ( empty_set @ sk17 ) ) ),
inference(simp,[status(thm)],[12157]) ).
thf(12159,plain,
( ( sk9 @ function )
| ( empty_set @ ( empty_set @ ( sk9 @ sk20 ) @ in ) )
| ( sk9 @ ( empty_set @ sk17 ) ) ),
inference(pattern_uni,[status(thm)],[12158:[bind(A,$thf( sk9 ))]]) ).
thf(21980,plain,
( ( sk9 @ function )
| $false
| ( sk9 @ ( empty_set @ sk17 ) ) ),
inference(rewrite,[status(thm)],[12159,578]) ).
thf(21981,plain,
( ( sk9 @ function )
| ( sk9 @ ( empty_set @ sk17 ) ) ),
inference(simp,[status(thm)],[21980]) ).
thf(241,plain,
! [B: $i,A: $i] :
( ( B != sk9 )
| ( A @ relation_empty_yielding )
| ~ ( B @ empty )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[61,101]) ).
thf(242,plain,
! [A: $i] :
( ( A @ relation_empty_yielding )
| ~ ( sk9 @ empty )
| ~ ( A @ empty ) ),
inference(pattern_uni,[status(thm)],[241:[bind(A,$thf( A )),bind(B,$thf( sk9 ))]]) ).
thf(293,plain,
! [B: $i,A: $i] :
( ( B != sk1 )
| ( A @ ( sk3 @ relation_rng @ subset ) )
| ~ ( B @ empty )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[61,52]) ).
thf(294,plain,
! [A: $i] :
( ( A @ ( sk3 @ relation_rng @ subset ) )
| ~ ( sk1 @ empty )
| ~ ( A @ empty ) ),
inference(pattern_uni,[status(thm)],[293:[bind(A,$thf( A )),bind(B,$thf( sk1 ))]]) ).
thf(5640,plain,
! [A: $i] :
( ( A
!= ( sk2 @ relation_rng ) )
| ( sk5 != sk2 )
| ( empty_set != empty_set )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[84,3529]) ).
thf(5641,plain,
! [A: $i] :
( ( A
!= ( sk2 @ relation_rng ) )
| ( sk5 != sk2 )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[5640]) ).
thf(5642,plain,
( ( sk5 != sk2 )
| ~ ( sk2 @ relation_rng @ empty ) ),
inference(pattern_uni,[status(thm)],[5641:[bind(A,$thf( sk2 @ relation_rng ))]]) ).
thf(9881,plain,
( ( ( sk3 @ empty )
!= ( sk3 @ empty ) )
| ( sk1 @ empty )
| ~ $true
| ( ( sk3 @ relation_rng )
!= empty_set ) ),
inference(paramod_ordered,[status(thm)],[3220,9145]) ).
thf(9882,plain,
( ( ( sk3 @ empty )
!= ( sk3 @ empty ) )
| ( sk1 @ empty )
| ( ( sk3 @ relation_rng )
!= empty_set ) ),
inference(simp,[status(thm)],[9881]) ).
thf(9883,plain,
( ( sk1 @ empty )
| ( ( sk3 @ relation_rng )
!= empty_set ) ),
inference(pattern_uni,[status(thm)],[9882:[]]) ).
thf(331,plain,
! [B: $i,A: $i] :
( ( B != sk2 )
| ( ( A @ ( sk3 @ relation_composition ) )
= sk2 )
| ~ ( B @ empty )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[61,54]) ).
thf(332,plain,
! [A: $i] :
( ( ( A @ ( sk3 @ relation_composition ) )
= sk2 )
| ~ ( sk2 @ empty )
| ~ ( A @ empty ) ),
inference(pattern_uni,[status(thm)],[331:[bind(A,$thf( A )),bind(B,$thf( sk2 ))]]) ).
thf(161,plain,
( ( sk14 @ relation )
& ( sk14 @ empty ) ),
inference(cnf,[status(esa)],[160]) ).
thf(162,plain,
sk14 @ empty,
inference(cnfConj,[status(thm)],[161]) ).
thf(1266,plain,
! [A: $i] :
( ( ( sk14 @ empty )
!= ( A @ empty ) )
| ~ $true
| ( A = empty_set ) ),
inference(paramod_ordered,[status(thm)],[162,84]) ).
thf(1267,plain,
! [A: $i] :
( ( ( sk14 @ empty )
!= ( A @ empty ) )
| ( A = empty_set ) ),
inference(simp,[status(thm)],[1266]) ).
thf(1268,plain,
sk14 = empty_set,
inference(pattern_uni,[status(thm)],[1267:[bind(A,$thf( sk14 ))]]) ).
thf(10571,plain,
! [A: $i] :
( ( ( sk1 @ empty )
!= ( A @ empty ) )
| ( A @ relation_dom @ relation )
| ~ $true
| ( sk3 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[9460,191]) ).
thf(10572,plain,
! [A: $i] :
( ( ( sk1 @ empty )
!= ( A @ empty ) )
| ( A @ relation_dom @ relation )
| ( sk3 != empty_set ) ),
inference(simp,[status(thm)],[10571]) ).
thf(10573,plain,
( ( sk1 @ relation_dom @ relation )
| ( sk3 != empty_set ) ),
inference(pattern_uni,[status(thm)],[10572:[bind(A,$thf( sk1 ))]]) ).
thf(1498,plain,
( ( ( sk2 @ empty )
!= ( empty_set @ empty ) )
| ( empty_set @ one_to_one )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[75,1150]) ).
thf(1499,plain,
( ( ( sk2 @ empty )
!= ( empty_set @ empty ) )
| ( empty_set @ one_to_one ) ),
inference(simp,[status(thm)],[1498]) ).
thf(1500,plain,
( ( sk2 != empty_set )
| ( empty_set @ one_to_one ) ),
inference(simp,[status(thm)],[1499]) ).
thf(14795,plain,
( ( sk1 != sk1 )
| ( ( empty_set @ identity_relation )
!= sk3 )
| ~ ( sk2 @ empty ) ),
inference(paramod_ordered,[status(thm)],[9622,55]) ).
thf(14796,plain,
( ( ( empty_set @ identity_relation )
!= sk3 )
| ~ ( sk2 @ empty ) ),
inference(pattern_uni,[status(thm)],[14795:[]]) ).
thf(6207,plain,
! [A: $i] :
( ( A
!= ( sk3 @ relation_rng ) )
| ( sk5 != sk3 )
| ( empty_set != empty_set )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[84,4309]) ).
thf(6208,plain,
! [A: $i] :
( ( A
!= ( sk3 @ relation_rng ) )
| ( sk5 != sk3 )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[6207]) ).
thf(6209,plain,
( ( sk5 != sk3 )
| ~ ( sk3 @ relation_rng @ empty ) ),
inference(pattern_uni,[status(thm)],[6208:[bind(A,$thf( sk3 @ relation_rng ))]]) ).
thf(47,plain,
sk2 @ function,
inference(cnfConj,[status(thm)],[43]) ).
thf(4582,plain,
! [A: $i] :
( ( A != sk3 )
| ( sk10 != sk3 )
| ( empty_set != empty_set )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[84,4428]) ).
thf(4583,plain,
! [A: $i] :
( ( A != sk3 )
| ( sk10 != sk3 )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[4582]) ).
thf(4584,plain,
( ( sk10 != sk3 )
| ~ ( sk3 @ empty ) ),
inference(pattern_uni,[status(thm)],[4583:[bind(A,$thf( sk3 ))]]) ).
thf(37184,plain,
( ( ( sk1 @ empty )
!= ( sk1 @ empty ) )
| ( sk2 = sk1 )
| ~ $true
| ( sk3 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[9460,35432]) ).
thf(37185,plain,
( ( ( sk1 @ empty )
!= ( sk1 @ empty ) )
| ( sk2 = sk1 )
| ( sk3 != empty_set ) ),
inference(simp,[status(thm)],[37184]) ).
thf(37186,plain,
( ( sk2 = sk1 )
| ( sk3 != empty_set ) ),
inference(pattern_uni,[status(thm)],[37185:[]]) ).
thf(22187,plain,
! [A: $i] :
( ( ( A @ relation_rng @ empty )
!= ( sk3 @ relation_rng @ empty ) )
| ( sk3 = empty_set )
| ~ $true
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[104,7018]) ).
thf(22188,plain,
! [A: $i] :
( ( ( A @ relation_rng @ empty )
!= ( sk3 @ relation_rng @ empty ) )
| ( sk3 = empty_set )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[22187]) ).
thf(22189,plain,
( ( sk3 = empty_set )
| ~ ( sk3 @ empty ) ),
inference(pattern_uni,[status(thm)],[22188:[bind(A,$thf( sk3 ))]]) ).
thf(71177,plain,
$false,
inference(e,[status(thm)],[69,1586,16137,138,101,8288,234,5778,88,9621,10446,15143,5265,9152,120,21207,5669,35527,56,9460,39325,142,1342,153,6046,7793,3848,185,7018,13626,42,5935,5938,35314,7311,6306,9148,52,10955,7914,36596,5883,37769,110,7652,125,4428,7665,10469,6643,13704,8278,6310,46,1347,26269,3835,3866,35742,57,78,6025,216,164,4173,6670,13538,121,84,1283,39464,1302,179,8229,3525,106,147,8274,3537,221,453,35289,74,206,8261,61,132,32360,89,133,116,1405,7674,292,35824,4407,6064,233,452,6760,117,37643,10506,85,7037,10831,220,2641,102,957,1343,6032,302,17303,160,70,192,11908,4160,10102,35311,33940,9993,92,35794,97,37355,4104,13681,4680,578,7329,9145,156,10154,1970,37145,10052,10646,6235,188,9624,109,124,77,14752,4425,4315,9609,2551,33948,96,35334,9910,10163,34080,7293,212,3787,18176,9620,9607,10180,1150,20392,129,4120,10629,13731,37214,105,35432,10614,8361,16537,3190,8378,7646,10556,1764,5524,2176,6243,64,149,7010,166,148,5230,9418,191,9602,4309,118,4381,204,14869,4978,54,38528,49,3832,181,5158,6757,14942,86,71,8318,25898,23939,187,113,25518,9377,81,7328,7330,9570,7265,4176,98,208,3160,219,35630,362,76,19599,4420,9275,140,91,7551,3483,2647,155,330,14910,66,130,5218,135,10119,80,167,10617,35821,5886,37959,6751,10449,648,7190,4566,7013,112,9943,6132,14940,145,48,26323,150,36277,5079,17943,50,4314,67,2486,4117,37501,38523,33387,32893,791,182,7796,10144,5208,7331,3356,34002,72,9622,314,6105,36440,38403,17067,250,9686,35811,87,7904,19456,4185,2658,218,7889,8285,10188,104,1453,5860,5068,5184,2167,10605,13004,3220,36740,139,8617,17681,55,114,2447,35446,75,35673,3529,1607,5072,10600,82,214,290,119,58,15109,16192,10173,168,35901,10041,15027,190,5247,603,38511,210,268,35346,10472,13657,5215,10622,3822,21981,3328,242,294,126,136,5642,2619,9883,332,1268,10573,11958,1500,4206,35449,14796,62,3812,6209,6697,131,47,3437,122,4584,37186,100,22189,111,16549,1848]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU017+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.08 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.15/0.41 % Computer : n015.cluster.edu
% 0.15/0.41 % Model : x86_64 x86_64
% 0.15/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.41 % Memory : 8046.5625MB
% 0.15/0.41 % OS : Linux 6.8.0-71-generic
% 0.15/0.41 % CPULimit : 300
% 0.15/0.41 % WCLimit : 300
% 0.15/0.41 % DateTime : Sat Sep 26 08:34:13 UTC 2026
% 0.15/0.42 % CPUTime :
% 0.15/0.42 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.67/0.73 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 0.92/0.86 % [INFO] Parsing done (124ms).
% 0.92/0.87 % [INFO] Running in sequential loop mode.
% 1.54/1.10 % [INFO] eprover registered as external prover.
% 1.54/1.10 % [INFO] Scanning for conjecture ...
% 1.80/1.16 % [INFO] Found a conjecture (or negated_conjecture) and 39 axioms. Running axiom selection ...
% 1.96/1.21 % [INFO] Axiom selection finished. Selected 39 axioms (removed 0 axioms).
% 1.96/1.25 % [INFO] Problem is first-order (TPTP FOF).
% 1.96/1.25 % [INFO] Type checking passed.
% 1.96/1.25 % [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 ...
% 102.03/23.11 % External prover 'e' found a proof!
% 102.03/23.11 % [INFO] Killing All external provers ...
% 102.03/23.11 % Time passed: 22604ms (effective reasoning time: 22242ms)
% 102.03/23.11 % 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)>
% 102.03/23.11 % Axioms used in derivation (39): d8_funct_1, fc9_relat_1, fc1_funct_1, cc1_relat_1, rc1_funct_1, t23_funct_1, t5_subset, fc2_funct_1, t4_subset, fc5_relat_1, rc2_relat_1, d5_funct_1, rc2_xboole_0, antisymmetry_r2_hidden, fc1_xboole_0, fc4_relat_1, t1_subset, t34_funct_1, rc3_relat_1, t6_boole, rc2_subset_1, t7_boole, cc1_funct_1, fc1_subset_1, fc10_relat_1, rc1_subset_1, t3_subset, existence_m1_subset_1, rc1_relat_1, dt_k5_relat_1, reflexivity_r1_tarski, dt_k6_relat_1, fc6_relat_1, t8_boole, rc1_xboole_0, t2_subset, fc7_relat_1, fc12_relat_1, fc8_relat_1
% 102.03/23.11 % No. of inferences in proof: 1094
% 102.03/23.12 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 22604 ms resp. 22242 ms w/o parsing
% 98.40/23.41 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 98.40/23.42 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------