%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : SET802+4 : 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 : n008.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 08:30:56 AM UTC 2026
% Result : Theorem 18.25s 4.36s
% Output : Refutation 16.88s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 37
% Syntax : Number of formulae : 168 ( 37 unt; 0 typ; 15 def)
% Number of atoms : 906 ( 140 equ; 0 cnn)
% Maximal formula atoms : 142 ( 5 avg)
% Number of connectives : 2994 ( 223 ~; 284 |; 205 &;2104 @)
% ( 22 <=>; 156 =>; 0 <=; 0 <~>)
% Maximal formula depth : 53 ( 8 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 43 ( 40 usr; 9 con; 0-4 aty)
% Number of variables : 453 ( 20 ^; 414 !; 4 ?; 453 :)
% ( 0 !>; 0 ?*; 0 @-; 15 @+)
% Comments :
%------------------------------------------------------------------------------
thf(order_decl,type,
order: $i > $i > $o ).
thf(subset_decl,type,
subset: $i > $i > $o ).
thf(least_decl,type,
least: $i > $i > $i > $o ).
thf(member_decl,type,
member: $i > $i > $o ).
thf(greatest_lower_bound_decl,type,
greatest_lower_bound: $i > $i > $i > $i > $o ).
thf(apply_decl,type,
apply: $i > $i > $i > $o ).
thf(total_order_decl,type,
total_order: $i > $i > $o ).
thf(min_decl,type,
min: $i > $i > $i > $o ).
thf(power_set_decl,type,
power_set: $i > $i ).
thf(least_upper_bound_decl,type,
least_upper_bound: $i > $i > $i > $i > $o ).
thf(upper_bound_decl,type,
upper_bound: $i > $i > $i > $o ).
thf(singleton_decl,type,
singleton: $i > $i ).
thf(product_decl,type,
product: $i > $i ).
thf(lower_bound_decl,type,
lower_bound: $i > $i > $i > $o ).
thf(greatest_decl,type,
greatest: $i > $i > $i > $o ).
thf(empty_set_decl,type,
empty_set: $i ).
thf(difference_decl,type,
difference: $i > $i > $i ).
thf(intersection_decl,type,
intersection: $i > $i > $i ).
thf(max_decl,type,
max: $i > $i > $i > $o ).
thf(union_decl,type,
union: $i > $i > $i ).
thf(unordered_pair_decl,type,
unordered_pair: $i > $i > $i ).
thf(equal_set_decl,type,
equal_set: $i > $i > $o ).
thf(sum_decl,type,
sum: $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: $o ).
thf(sk5_decl,type,
sk5: $i ).
thf(sk6_decl,type,
sk6: $i ).
thf(sk7_decl,type,
sk7: $i > $i > $o ).
thf(sk8_decl,type,
sk8: $i > $i > $i ).
thf(sk9_decl,type,
sk9: $i > $i > $i ).
thf(sk10_decl,type,
sk10: $i > $i > $i ).
thf(sk11_decl,type,
sk11: $i > $i > $i ).
thf(sk12_decl,type,
sk12: $i > $i > $i ).
thf(sk13_decl,type,
sk13: $i > $i > $i ).
thf(sk14_decl,type,
sk14: $i > $i > $i ).
thf(sk15_decl,type,
sk15: $i > $i > $i ).
thf(sk19_decl,type,
sk19: $i > $i > $i ).
thf(sk24_decl,type,
sk24: $i > $i > $i ).
thf(sk1_def,definition,
( sk1
= ( @+[A: $i] :
~ ! [B: $i] :
( ( B @ ( A @ order ) )
=> ! [C: $i] :
( ( B @ ( C @ subset ) )
=> ( ! [D: $i] :
( ( ( B @ ( A @ ( C @ ( D @ greatest_lower_bound ) ) ) )
& ( C @ ( D @ member ) ) )
=> ( C @ ( A @ ( D @ least ) ) ) )
& ! [D: $i] :
( ( C @ ( A @ ( D @ least ) ) )
=> ( ( B @ ( A @ ( C @ ( D @ greatest_lower_bound ) ) ) )
& ( C @ ( D @ member ) ) ) ) ) ) ) ) ) ).
thf(sk2_def,definition,
( sk2
= ( @+[A: $i] :
~ ( ( A @ ( sk1 @ order ) )
=> ! [B: $i] :
( ( A @ ( B @ subset ) )
=> ( ! [C: $i] :
( ( ( A @ ( sk1 @ ( B @ ( C @ greatest_lower_bound ) ) ) )
& ( B @ ( C @ member ) ) )
=> ( B @ ( sk1 @ ( C @ least ) ) ) )
& ! [C: $i] :
( ( B @ ( sk1 @ ( C @ least ) ) )
=> ( ( A @ ( sk1 @ ( B @ ( C @ greatest_lower_bound ) ) ) )
& ( B @ ( C @ member ) ) ) ) ) ) ) ) ) ).
thf(sk3_def,definition,
( sk3
= ( @+[A: $i] :
~ ( ( sk2 @ ( A @ subset ) )
=> ( ! [B: $i] :
( ( ( sk2 @ ( sk1 @ ( A @ ( B @ greatest_lower_bound ) ) ) )
& ( A @ ( B @ member ) ) )
=> ( A @ ( sk1 @ ( B @ least ) ) ) )
& ! [B: $i] :
( ( A @ ( sk1 @ ( B @ least ) ) )
=> ( ( sk2 @ ( sk1 @ ( A @ ( B @ greatest_lower_bound ) ) ) )
& ( A @ ( B @ member ) ) ) ) ) ) ) ) ).
thf(sk5_def,definition,
( sk5
= ( @+[A: $i] :
~ ( ( sk3 @ ( sk1 @ ( A @ least ) ) )
=> ( ( sk2 @ ( sk1 @ ( sk3 @ ( A @ greatest_lower_bound ) ) ) )
& ( sk3 @ ( A @ member ) ) ) ) ) ) ).
thf(sk6_def,definition,
( sk6
= ( @+[A: $i] :
~ ( ( ( sk2 @ ( sk1 @ ( sk3 @ ( A @ greatest_lower_bound ) ) ) )
& ( sk3 @ ( A @ member ) ) )
=> ( sk3 @ ( sk1 @ ( A @ least ) ) ) ) ) ) ).
thf(sk8_def,definition,
( sk8
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
~ ( ( A @ ( C @ member ) )
=> ( C @ ( C @ ( B @ apply ) ) ) ) ) ) ).
thf(sk9_def,definition,
( sk9
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
~ ! [D: $i] :
( ( ( A @ ( D @ member ) )
& ( A @ ( C @ member ) ) )
=> ( ( ( C @ ( D @ ( B @ apply ) ) )
& ( D @ ( C @ ( B @ apply ) ) ) )
=> ( C = D ) ) ) ) ) ).
thf(sk10_def,definition,
( sk10
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
~ ( ( ( A @ ( C @ member ) )
& ( A @ ( B @ ( A @ sk9 ) @ member ) ) )
=> ( ( ( B @ ( A @ sk9 ) @ ( C @ ( B @ apply ) ) )
& ( C @ ( B @ ( A @ sk9 ) @ ( B @ apply ) ) ) )
=> ( ( B @ ( A @ sk9 ) )
= C ) ) ) ) ) ).
thf(sk11_def,definition,
( sk11
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
~ ! [D: $i,E: $i] :
( ( ( A @ ( E @ member ) )
& ( A @ ( D @ member ) )
& ( A @ ( C @ member ) ) )
=> ( ( ( E @ ( D @ ( B @ apply ) ) )
& ( D @ ( C @ ( B @ apply ) ) ) )
=> ( E @ ( C @ ( B @ apply ) ) ) ) ) ) ) ).
thf(sk12_def,definition,
( sk12
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
~ ! [D: $i] :
( ( ( A @ ( D @ member ) )
& ( A @ ( C @ member ) )
& ( A @ ( B @ ( A @ sk11 ) @ member ) ) )
=> ( ( ( D @ ( C @ ( B @ apply ) ) )
& ( C @ ( B @ ( A @ sk11 ) @ ( B @ apply ) ) ) )
=> ( D @ ( B @ ( A @ sk11 ) @ ( B @ apply ) ) ) ) ) ) ) ).
thf(sk13_def,definition,
( sk13
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
~ ( ( ( A @ ( C @ member ) )
& ( A @ ( B @ ( A @ sk12 ) @ member ) )
& ( A @ ( B @ ( A @ sk11 ) @ member ) ) )
=> ( ( ( C @ ( B @ ( A @ sk12 ) @ ( B @ apply ) ) )
& ( B @ ( A @ sk12 ) @ ( B @ ( A @ sk11 ) @ ( B @ apply ) ) ) )
=> ( C @ ( B @ ( A @ sk11 ) @ ( B @ apply ) ) ) ) ) ) ) ).
thf(sk14_def,definition,
( sk14
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
~ ! [D: $i] :
( ( ( A @ ( D @ member ) )
& ( A @ ( C @ member ) ) )
=> ( ( C @ ( D @ ( B @ apply ) ) )
| ( D @ ( C @ ( B @ apply ) ) ) ) ) ) ) ).
thf(sk15_def,definition,
( sk15
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
~ ( ( ( A @ ( C @ member ) )
& ( A @ ( B @ ( A @ sk14 ) @ member ) ) )
=> ( ( B @ ( A @ sk14 ) @ ( C @ ( B @ apply ) ) )
| ( C @ ( B @ ( A @ sk14 ) @ ( B @ apply ) ) ) ) ) ) ) ).
thf(sk19_def,definition,
( sk19
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
~ ( ( A @ ( C @ member ) )
=> ( C @ ( B @ member ) ) ) ) ) ).
thf(sk24_def,definition,
( sk24
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
~ ( ( B @ ( C @ member ) )
=> ( A @ ( C @ member ) ) ) ) ) ).
thf(1,conjecture,
! [A: $i,B: $i] :
( ( B @ ( A @ order ) )
=> ! [C: $i] :
( ( B @ ( C @ subset ) )
=> ! [D: $i] :
( ( C @ ( A @ ( D @ least ) ) )
<=> ( ( B @ ( A @ ( C @ ( D @ greatest_lower_bound ) ) ) )
& ( C @ ( D @ member ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thIV14) ).
thf(2,negated_conjecture,
~ ! [A: $i,B: $i] :
( ( B @ ( A @ order ) )
=> ! [C: $i] :
( ( B @ ( C @ subset ) )
=> ! [D: $i] :
( ( C @ ( A @ ( D @ least ) ) )
<=> ( ( B @ ( A @ ( C @ ( D @ greatest_lower_bound ) ) ) )
& ( C @ ( D @ member ) ) ) ) ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(24,plain,
~ ! [A: $i,B: $i] :
( ( B @ ( A @ order ) )
=> ! [C: $i] :
( ( B @ ( C @ subset ) )
=> ! [D: $i] :
( ( ( ( B @ ( A @ ( C @ ( D @ greatest_lower_bound ) ) ) )
& ( C @ ( D @ member ) ) )
=> ( C @ ( A @ ( D @ least ) ) ) )
& ( ( C @ ( A @ ( D @ least ) ) )
=> ( ( B @ ( A @ ( C @ ( D @ greatest_lower_bound ) ) ) )
& ( C @ ( D @ member ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(25,plain,
~ ! [A: $i,B: $i] :
( ( B @ ( A @ order ) )
=> ! [C: $i] :
( ( B @ ( C @ subset ) )
=> ( ! [D: $i] :
( ( ( B @ ( A @ ( C @ ( D @ greatest_lower_bound ) ) ) )
& ( C @ ( D @ member ) ) )
=> ( C @ ( A @ ( D @ least ) ) ) )
& ! [D: $i] :
( ( C @ ( A @ ( D @ least ) ) )
=> ( ( B @ ( A @ ( C @ ( D @ greatest_lower_bound ) ) ) )
& ( C @ ( D @ member ) ) ) ) ) ) ),
inference(miniscope,[status(thm)],[24]) ).
thf(26,plain,
( ( ~ ( sk3 @ ( sk1 @ ( sk6 @ least ) ) )
| sk4 )
& ( ( sk2 @ ( sk1 @ ( sk3 @ ( sk6 @ greatest_lower_bound ) ) ) )
| sk4 )
& ( ( sk3 @ ( sk6 @ member ) )
| sk4 )
& ( ~ sk4
| ~ ( sk2 @ ( sk1 @ ( sk3 @ ( sk5 @ greatest_lower_bound ) ) ) )
| ~ ( sk3 @ ( sk5 @ member ) ) )
& ( ~ sk4
| ( sk3 @ ( sk1 @ ( sk5 @ least ) ) ) )
& ( sk2 @ ( sk3 @ subset ) )
& ( sk2 @ ( sk1 @ order ) ) ),
inference(cnf,[status(esa)],[25]) ).
thf(33,plain,
sk2 @ ( sk1 @ order ),
inference(cnfConj,[status(thm)],[26]) ).
thf(3,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ order ) )
<=> ( ! [C: $i,D: $i,E: $i] :
( ( ( B @ ( E @ member ) )
& ( B @ ( D @ member ) )
& ( B @ ( C @ member ) ) )
=> ( ( ( E @ ( D @ ( A @ apply ) ) )
& ( D @ ( C @ ( A @ apply ) ) ) )
=> ( E @ ( C @ ( A @ apply ) ) ) ) )
& ! [C: $i,D: $i] :
( ( ( B @ ( D @ member ) )
& ( B @ ( C @ member ) ) )
=> ( ( ( C @ ( D @ ( A @ apply ) ) )
& ( D @ ( C @ ( A @ apply ) ) ) )
=> ( C = D ) ) )
& ! [C: $i] :
( ( B @ ( C @ member ) )
=> ( C @ ( C @ ( A @ apply ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',order) ).
thf(34,plain,
! [A: $i,B: $i] :
( ( ( ! [C: $i,D: $i,E: $i] :
( ( ( B @ ( E @ member ) )
& ( B @ ( D @ member ) )
& ( B @ ( C @ member ) ) )
=> ( ( ( E @ ( D @ ( A @ apply ) ) )
& ( D @ ( C @ ( A @ apply ) ) ) )
=> ( E @ ( C @ ( A @ apply ) ) ) ) )
& ! [C: $i,D: $i] :
( ( ( B @ ( D @ member ) )
& ( B @ ( C @ member ) ) )
=> ( ( ( C @ ( D @ ( A @ apply ) ) )
& ( D @ ( C @ ( A @ apply ) ) ) )
=> ( C = D ) ) )
& ! [C: $i] :
( ( B @ ( C @ member ) )
=> ( C @ ( C @ ( A @ apply ) ) ) ) )
=> ( B @ ( A @ order ) ) )
& ( ( B @ ( A @ order ) )
=> ( ! [C: $i,D: $i,E: $i] :
( ( ( B @ ( E @ member ) )
& ( B @ ( D @ member ) )
& ( B @ ( C @ member ) ) )
=> ( ( ( E @ ( D @ ( A @ apply ) ) )
& ( D @ ( C @ ( A @ apply ) ) ) )
=> ( E @ ( C @ ( A @ apply ) ) ) ) )
& ! [C: $i,D: $i] :
( ( ( B @ ( D @ member ) )
& ( B @ ( C @ member ) ) )
=> ( ( ( C @ ( D @ ( A @ apply ) ) )
& ( D @ ( C @ ( A @ apply ) ) ) )
=> ( C = D ) ) )
& ! [C: $i] :
( ( B @ ( C @ member ) )
=> ( C @ ( C @ ( A @ apply ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(35,plain,
( ! [A: $i,B: $i] :
( ( ! [C: $i,D: $i,E: $i] :
( ( ( B @ ( E @ member ) )
& ( B @ ( D @ member ) )
& ( B @ ( C @ member ) ) )
=> ( ( ( E @ ( D @ ( A @ apply ) ) )
& ( D @ ( C @ ( A @ apply ) ) ) )
=> ( E @ ( C @ ( A @ apply ) ) ) ) )
& ! [C: $i,D: $i] :
( ( ( B @ ( D @ member ) )
& ( B @ ( C @ member ) ) )
=> ( ( ( C @ ( D @ ( A @ apply ) ) )
& ( D @ ( C @ ( A @ apply ) ) ) )
=> ( C = D ) ) )
& ! [C: $i] :
( ( B @ ( C @ member ) )
=> ( C @ ( C @ ( A @ apply ) ) ) ) )
=> ( B @ ( A @ order ) ) )
& ! [A: $i,B: $i] :
( ( B @ ( A @ order ) )
=> ( ! [C: $i,D: $i,E: $i] :
( ( ( B @ ( E @ member ) )
& ( B @ ( D @ member ) )
& ( B @ ( C @ member ) ) )
=> ( ( ( E @ ( D @ ( A @ apply ) ) )
& ( D @ ( C @ ( A @ apply ) ) ) )
=> ( E @ ( C @ ( A @ apply ) ) ) ) )
& ! [C: $i,D: $i] :
( ( ( B @ ( D @ member ) )
& ( B @ ( C @ member ) ) )
=> ( ( ( C @ ( D @ ( A @ apply ) ) )
& ( D @ ( C @ ( A @ apply ) ) ) )
=> ( C = D ) ) )
& ! [C: $i] :
( ( B @ ( C @ member ) )
=> ( C @ ( C @ ( A @ apply ) ) ) ) ) ) ),
inference(miniscope,[status(thm)],[34]) ).
thf(36,plain,
! [J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( J @ ( I @ order ) )
| ~ ( I @ ( J @ sk13 ) @ ( I @ ( J @ sk11 ) @ ( I @ apply ) ) )
| ( ( I @ ( J @ sk9 ) )
!= ( I @ ( J @ sk10 ) ) )
| ( I @ ( J @ sk7 ) ) )
& ( ( J @ ( I @ order ) )
| ( I @ ( J @ sk13 ) @ ( I @ ( J @ sk12 ) @ ( I @ apply ) ) )
| ( ( I @ ( J @ sk9 ) )
!= ( I @ ( J @ sk10 ) ) )
| ( I @ ( J @ sk7 ) ) )
& ( ( J @ ( I @ order ) )
| ( I @ ( J @ sk12 ) @ ( I @ ( J @ sk11 ) @ ( I @ apply ) ) )
| ( ( I @ ( J @ sk9 ) )
!= ( I @ ( J @ sk10 ) ) )
| ( I @ ( J @ sk7 ) ) )
& ( ( J @ ( I @ order ) )
| ( J @ ( I @ ( J @ sk13 ) @ member ) )
| ( ( I @ ( J @ sk9 ) )
!= ( I @ ( J @ sk10 ) ) )
| ( I @ ( J @ sk7 ) ) )
& ( ( J @ ( I @ order ) )
| ( J @ ( I @ ( J @ sk12 ) @ member ) )
| ( ( I @ ( J @ sk9 ) )
!= ( I @ ( J @ sk10 ) ) )
| ( I @ ( J @ sk7 ) ) )
& ( ( J @ ( I @ order ) )
| ( J @ ( I @ ( J @ sk11 ) @ member ) )
| ( ( I @ ( J @ sk9 ) )
!= ( I @ ( J @ sk10 ) ) )
| ( I @ ( J @ sk7 ) ) )
& ( ( J @ ( I @ order ) )
| ~ ( I @ ( J @ sk13 ) @ ( I @ ( J @ sk11 ) @ ( I @ apply ) ) )
| ( I @ ( J @ sk9 ) @ ( I @ ( J @ sk10 ) @ ( I @ apply ) ) )
| ( I @ ( J @ sk7 ) ) )
& ( ( J @ ( I @ order ) )
| ( I @ ( J @ sk13 ) @ ( I @ ( J @ sk12 ) @ ( I @ apply ) ) )
| ( I @ ( J @ sk9 ) @ ( I @ ( J @ sk10 ) @ ( I @ apply ) ) )
| ( I @ ( J @ sk7 ) ) )
& ( ( J @ ( I @ order ) )
| ( I @ ( J @ sk12 ) @ ( I @ ( J @ sk11 ) @ ( I @ apply ) ) )
| ( I @ ( J @ sk9 ) @ ( I @ ( J @ sk10 ) @ ( I @ apply ) ) )
| ( I @ ( J @ sk7 ) ) )
& ( ( J @ ( I @ order ) )
| ( J @ ( I @ ( J @ sk13 ) @ member ) )
| ( I @ ( J @ sk9 ) @ ( I @ ( J @ sk10 ) @ ( I @ apply ) ) )
| ( I @ ( J @ sk7 ) ) )
& ( ( J @ ( I @ order ) )
| ( J @ ( I @ ( J @ sk12 ) @ member ) )
| ( I @ ( J @ sk9 ) @ ( I @ ( J @ sk10 ) @ ( I @ apply ) ) )
| ( I @ ( J @ sk7 ) ) )
& ( ( J @ ( I @ order ) )
| ( J @ ( I @ ( J @ sk11 ) @ member ) )
| ( I @ ( J @ sk9 ) @ ( I @ ( J @ sk10 ) @ ( I @ apply ) ) )
| ( I @ ( J @ sk7 ) ) )
& ( ( J @ ( I @ order ) )
| ~ ( I @ ( J @ sk13 ) @ ( I @ ( J @ sk11 ) @ ( I @ apply ) ) )
| ( I @ ( J @ sk10 ) @ ( I @ ( J @ sk9 ) @ ( I @ apply ) ) )
| ( I @ ( J @ sk7 ) ) )
& ( ( J @ ( I @ order ) )
| ( I @ ( J @ sk13 ) @ ( I @ ( J @ sk12 ) @ ( I @ apply ) ) )
| ( I @ ( J @ sk10 ) @ ( I @ ( J @ sk9 ) @ ( I @ apply ) ) )
| ( I @ ( J @ sk7 ) ) )
& ( ( J @ ( I @ order ) )
| ( I @ ( J @ sk12 ) @ ( I @ ( J @ sk11 ) @ ( I @ apply ) ) )
| ( I @ ( J @ sk10 ) @ ( I @ ( J @ sk9 ) @ ( I @ apply ) ) )
| ( I @ ( J @ sk7 ) ) )
& ( ( J @ ( I @ order ) )
| ( J @ ( I @ ( J @ sk13 ) @ member ) )
| ( I @ ( J @ sk10 ) @ ( I @ ( J @ sk9 ) @ ( I @ apply ) ) )
| ( I @ ( J @ sk7 ) ) )
& ( ( J @ ( I @ order ) )
| ( J @ ( I @ ( J @ sk12 ) @ member ) )
| ( I @ ( J @ sk10 ) @ ( I @ ( J @ sk9 ) @ ( I @ apply ) ) )
| ( I @ ( J @ sk7 ) ) )
& ( ( J @ ( I @ order ) )
| ( J @ ( I @ ( J @ sk11 ) @ member ) )
| ( I @ ( J @ sk10 ) @ ( I @ ( J @ sk9 ) @ ( I @ apply ) ) )
| ( I @ ( J @ sk7 ) ) )
& ( ( J @ ( I @ order ) )
| ~ ( I @ ( J @ sk13 ) @ ( I @ ( J @ sk11 ) @ ( I @ apply ) ) )
| ( J @ ( I @ ( J @ sk10 ) @ member ) )
| ( I @ ( J @ sk7 ) ) )
& ( ( J @ ( I @ order ) )
| ( I @ ( J @ sk13 ) @ ( I @ ( J @ sk12 ) @ ( I @ apply ) ) )
| ( J @ ( I @ ( J @ sk10 ) @ member ) )
| ( I @ ( J @ sk7 ) ) )
& ( ( J @ ( I @ order ) )
| ( I @ ( J @ sk12 ) @ ( I @ ( J @ sk11 ) @ ( I @ apply ) ) )
| ( J @ ( I @ ( J @ sk10 ) @ member ) )
| ( I @ ( J @ sk7 ) ) )
& ( ( J @ ( I @ order ) )
| ( J @ ( I @ ( J @ sk13 ) @ member ) )
| ( J @ ( I @ ( J @ sk10 ) @ member ) )
| ( I @ ( J @ sk7 ) ) )
& ( ( J @ ( I @ order ) )
| ( J @ ( I @ ( J @ sk12 ) @ member ) )
| ( J @ ( I @ ( J @ sk10 ) @ member ) )
| ( I @ ( J @ sk7 ) ) )
& ( ( J @ ( I @ order ) )
| ( J @ ( I @ ( J @ sk11 ) @ member ) )
| ( J @ ( I @ ( J @ sk10 ) @ member ) )
| ( I @ ( J @ sk7 ) ) )
& ( ( J @ ( I @ order ) )
| ~ ( I @ ( J @ sk13 ) @ ( I @ ( J @ sk11 ) @ ( I @ apply ) ) )
| ( J @ ( I @ ( J @ sk9 ) @ member ) )
| ( I @ ( J @ sk7 ) ) )
& ( ( J @ ( I @ order ) )
| ( I @ ( J @ sk13 ) @ ( I @ ( J @ sk12 ) @ ( I @ apply ) ) )
| ( J @ ( I @ ( J @ sk9 ) @ member ) )
| ( I @ ( J @ sk7 ) ) )
& ( ( J @ ( I @ order ) )
| ( I @ ( J @ sk12 ) @ ( I @ ( J @ sk11 ) @ ( I @ apply ) ) )
| ( J @ ( I @ ( J @ sk9 ) @ member ) )
| ( I @ ( J @ sk7 ) ) )
& ( ( J @ ( I @ order ) )
| ( J @ ( I @ ( J @ sk13 ) @ member ) )
| ( J @ ( I @ ( J @ sk9 ) @ member ) )
| ( I @ ( J @ sk7 ) ) )
& ( ( J @ ( I @ order ) )
| ( J @ ( I @ ( J @ sk12 ) @ member ) )
| ( J @ ( I @ ( J @ sk9 ) @ member ) )
| ( I @ ( J @ sk7 ) ) )
& ( ( J @ ( I @ order ) )
| ( J @ ( I @ ( J @ sk11 ) @ member ) )
| ( J @ ( I @ ( J @ sk9 ) @ member ) )
| ( I @ ( J @ sk7 ) ) )
& ( ( J @ ( I @ order ) )
| ~ ( I @ ( J @ sk7 ) )
| ~ ( I @ ( J @ sk8 ) @ ( I @ ( J @ sk8 ) @ ( I @ apply ) ) ) )
& ( ( J @ ( I @ order ) )
| ~ ( I @ ( J @ sk7 ) )
| ( J @ ( I @ ( J @ sk8 ) @ member ) ) )
& ( ( H @ ( F @ ( A @ apply ) ) )
| ~ ( H @ ( G @ ( A @ apply ) ) )
| ~ ( G @ ( F @ ( A @ apply ) ) )
| ~ ( B @ ( H @ member ) )
| ~ ( B @ ( G @ member ) )
| ~ ( B @ ( F @ member ) )
| ~ ( B @ ( A @ order ) ) )
& ( ( D = E )
| ~ ( D @ ( E @ ( A @ apply ) ) )
| ~ ( E @ ( D @ ( A @ apply ) ) )
| ~ ( B @ ( E @ member ) )
| ~ ( B @ ( D @ member ) )
| ~ ( B @ ( A @ order ) ) )
& ( ( C @ ( C @ ( A @ apply ) ) )
| ~ ( B @ ( C @ member ) )
| ~ ( B @ ( A @ order ) ) ) ),
inference(cnf,[status(esa)],[35]) ).
thf(47,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( C @ ( A @ apply ) ) )
| ~ ( B @ ( C @ member ) )
| ~ ( B @ ( A @ order ) ) ),
inference(cnfConj,[status(thm)],[36]) ).
thf(383,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( sk1 @ order ) )
!= ( B @ ( A @ order ) ) )
| ( C @ ( C @ ( A @ apply ) ) )
| ~ ( B @ ( C @ member ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[33,47]) ).
thf(384,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( sk1 @ order ) )
!= ( B @ ( A @ order ) ) )
| ( C @ ( C @ ( A @ apply ) ) )
| ~ ( B @ ( C @ member ) ) ),
inference(simp,[status(thm)],[383]) ).
thf(385,plain,
! [A: $i] :
( ( A @ ( A @ ( sk1 @ apply ) ) )
| ~ ( sk2 @ ( A @ member ) ) ),
inference(pattern_uni,[status(thm)],[384:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 ))]]) ).
thf(389,plain,
! [A: $i] :
( ( A @ ( A @ ( sk1 @ apply ) ) )
| ~ ( sk2 @ ( A @ member ) ) ),
inference(simp,[status(thm)],[385]) ).
thf(29,plain,
( ~ ( sk3 @ ( sk1 @ ( sk6 @ least ) ) )
| sk4 ),
inference(cnfConj,[status(thm)],[26]) ).
thf(4,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ total_order ) )
<=> ( ! [C: $i,D: $i] :
( ( ( B @ ( D @ member ) )
& ( B @ ( C @ member ) ) )
=> ( ( C @ ( D @ ( A @ apply ) ) )
| ( D @ ( C @ ( A @ apply ) ) ) ) )
& ( B @ ( A @ order ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',total_order) ).
thf(113,plain,
! [A: $i,B: $i] :
( ( ( ! [C: $i,D: $i] :
( ( ( B @ ( D @ member ) )
& ( B @ ( C @ member ) ) )
=> ( ( C @ ( D @ ( A @ apply ) ) )
| ( D @ ( C @ ( A @ apply ) ) ) ) )
& ( B @ ( A @ order ) ) )
=> ( B @ ( A @ total_order ) ) )
& ( ( B @ ( A @ total_order ) )
=> ( ! [C: $i,D: $i] :
( ( ( B @ ( D @ member ) )
& ( B @ ( C @ member ) ) )
=> ( ( C @ ( D @ ( A @ apply ) ) )
| ( D @ ( C @ ( A @ apply ) ) ) ) )
& ( B @ ( A @ order ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(114,plain,
( ! [A: $i,B: $i] :
( ( ! [C: $i,D: $i] :
( ( ( B @ ( D @ member ) )
& ( B @ ( C @ member ) ) )
=> ( ( C @ ( D @ ( A @ apply ) ) )
| ( D @ ( C @ ( A @ apply ) ) ) ) )
& ( B @ ( A @ order ) ) )
=> ( B @ ( A @ total_order ) ) )
& ! [A: $i,B: $i] :
( ( B @ ( A @ total_order ) )
=> ( ! [C: $i,D: $i] :
( ( ( B @ ( D @ member ) )
& ( B @ ( C @ member ) ) )
=> ( ( C @ ( D @ ( A @ apply ) ) )
| ( D @ ( C @ ( A @ apply ) ) ) ) )
& ( B @ ( A @ order ) ) ) ) ),
inference(miniscope,[status(thm)],[113]) ).
thf(115,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( F @ ( E @ total_order ) )
| ~ ( E @ ( F @ sk14 ) @ ( E @ ( F @ sk15 ) @ ( E @ apply ) ) )
| ~ ( F @ ( E @ order ) ) )
& ( ( F @ ( E @ total_order ) )
| ~ ( E @ ( F @ sk15 ) @ ( E @ ( F @ sk14 ) @ ( E @ apply ) ) )
| ~ ( F @ ( E @ order ) ) )
& ( ( F @ ( E @ total_order ) )
| ( F @ ( E @ ( F @ sk15 ) @ member ) )
| ~ ( F @ ( E @ order ) ) )
& ( ( F @ ( E @ total_order ) )
| ( F @ ( E @ ( F @ sk14 ) @ member ) )
| ~ ( F @ ( E @ order ) ) )
& ( ( C @ ( D @ ( A @ apply ) ) )
| ( D @ ( C @ ( A @ apply ) ) )
| ~ ( B @ ( D @ member ) )
| ~ ( B @ ( C @ member ) )
| ~ ( B @ ( A @ total_order ) ) )
& ( ( B @ ( A @ order ) )
| ~ ( B @ ( A @ total_order ) ) ) ),
inference(cnf,[status(esa)],[114]) ).
thf(121,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ order ) )
| ~ ( B @ ( A @ total_order ) ) ),
inference(cnfConj,[status(thm)],[115]) ).
thf(16,axiom,
! [A: $i] :
~ ( empty_set @ ( A @ member ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',empty_set) ).
thf(227,plain,
! [A: $i] :
~ ( empty_set @ ( A @ member ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[16]) ).
thf(228,plain,
~ ? [A: $i] : ( empty_set @ ( A @ member ) ),
inference(miniscope,[status(thm)],[227]) ).
thf(229,plain,
! [A: $i] :
~ ( empty_set @ ( A @ member ) ),
inference(cnf,[status(esa)],[228]) ).
thf(15,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ subset ) )
<=> ! [C: $i] :
( ( A @ ( C @ member ) )
=> ( B @ ( C @ member ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',subset) ).
thf(219,plain,
! [A: $i,B: $i] :
( ( ! [C: $i] :
( ( A @ ( C @ member ) )
=> ( B @ ( C @ member ) ) )
=> ( B @ ( A @ subset ) ) )
& ( ( B @ ( A @ subset ) )
=> ! [C: $i] :
( ( A @ ( C @ member ) )
=> ( B @ ( C @ member ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[15]) ).
thf(220,plain,
( ! [A: $i,B: $i] :
( ! [C: $i] :
( ( A @ ( C @ member ) )
=> ( B @ ( C @ member ) ) )
=> ( B @ ( A @ subset ) ) )
& ! [A: $i,B: $i] :
( ( B @ ( A @ subset ) )
=> ! [C: $i] :
( ( A @ ( C @ member ) )
=> ( B @ ( C @ member ) ) ) ) ),
inference(miniscope,[status(thm)],[219]) ).
thf(221,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( E @ ( D @ subset ) )
| ~ ( E @ ( D @ ( E @ sk24 ) @ member ) ) )
& ( ( E @ ( D @ subset ) )
| ( D @ ( D @ ( E @ sk24 ) @ member ) ) )
& ( ( B @ ( C @ member ) )
| ~ ( A @ ( C @ member ) )
| ~ ( B @ ( A @ subset ) ) ) ),
inference(cnf,[status(esa)],[220]) ).
thf(223,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ subset ) )
| ( A @ ( A @ ( B @ sk24 ) @ member ) ) ),
inference(cnfConj,[status(thm)],[221]) ).
thf(225,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ subset ) )
| ( A @ ( A @ ( B @ sk24 ) @ member ) ) ),
inference(simp,[status(thm)],[223]) ).
thf(9,axiom,
! [A: $i,B: $i] :
( ( B @ singleton @ ( A @ member ) )
<=> ( A = B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',singleton) ).
thf(166,plain,
! [A: $i,B: $i] :
( ( ( A = B )
=> ( B @ singleton @ ( A @ member ) ) )
& ( ( B @ singleton @ ( A @ member ) )
=> ( A = B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).
thf(167,plain,
( ! [A: $i,B: $i] :
( ( A = B )
=> ( B @ singleton @ ( A @ member ) ) )
& ! [A: $i,B: $i] :
( ( B @ singleton @ ( A @ member ) )
=> ( A = B ) ) ),
inference(miniscope,[status(thm)],[166]) ).
thf(168,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ singleton @ ( C @ member ) )
| ( C != D ) )
& ( ( A = B )
| ~ ( B @ singleton @ ( A @ member ) ) ) ),
inference(cnf,[status(esa)],[167]) ).
thf(170,plain,
! [B: $i,A: $i] :
( ( B @ singleton @ ( A @ member ) )
| ( A != B ) ),
inference(cnfConj,[status(thm)],[168]) ).
thf(172,plain,
! [B: $i,A: $i] :
( ( B @ singleton @ ( A @ member ) )
| ( A != B ) ),
inference(lifteq,[status(thm)],[170]) ).
thf(173,plain,
! [A: $i] : ( A @ singleton @ ( A @ member ) ),
inference(simp,[status(thm)],[172]) ).
thf(21,axiom,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ unordered_pair ) @ ( A @ member ) )
<=> ( ( A = C )
| ( A = B ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unordered_pair) ).
thf(265,plain,
! [A: $i,B: $i,C: $i] :
( ( ( ( A = C )
| ( A = B ) )
=> ( C @ ( B @ unordered_pair ) @ ( A @ member ) ) )
& ( ( C @ ( B @ unordered_pair ) @ ( A @ member ) )
=> ( ( A = C )
| ( A = B ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[21]) ).
thf(266,plain,
( ! [A: $i,B: $i,C: $i] :
( ( ( A = C )
| ( A = B ) )
=> ( C @ ( B @ unordered_pair ) @ ( A @ member ) ) )
& ! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ unordered_pair ) @ ( A @ member ) )
=> ( ( A = C )
| ( A = B ) ) ) ),
inference(miniscope,[status(thm)],[265]) ).
thf(267,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( F @ ( E @ unordered_pair ) @ ( D @ member ) )
| ( D != F ) )
& ( ( F @ ( E @ unordered_pair ) @ ( D @ member ) )
| ( D != E ) )
& ( ( A = C )
| ( A = B )
| ~ ( C @ ( B @ unordered_pair ) @ ( A @ member ) ) ) ),
inference(cnf,[status(esa)],[266]) ).
thf(270,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ unordered_pair ) @ ( A @ member ) )
| ( A != C ) ),
inference(cnfConj,[status(thm)],[267]) ).
thf(274,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ unordered_pair ) @ ( A @ member ) )
| ( A != C ) ),
inference(lifteq,[status(thm)],[270]) ).
thf(275,plain,
! [B: $i,A: $i] : ( B @ ( A @ unordered_pair ) @ ( B @ member ) ),
inference(simp,[status(thm)],[274]) ).
thf(317,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ unordered_pair ) @ ( B @ member ) )
!= ( empty_set @ ( C @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[275,229]) ).
thf(318,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( A @ unordered_pair ) @ ( B @ member ) )
!= ( empty_set @ ( C @ member ) ) ),
inference(simp,[status(thm)],[317]) ).
thf(321,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ unordered_pair ) )
!= empty_set )
| ( B != C ) ),
inference(simp,[status(thm)],[318]) ).
thf(323,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ unordered_pair ) )
!= empty_set ),
inference(simp,[status(thm)],[321]) ).
thf(12,axiom,
! [A: $i,B: $i,C: $i] :
( ( B @ ( A @ ( C @ upper_bound ) ) )
<=> ! [D: $i] :
( ( B @ ( D @ member ) )
=> ( C @ ( D @ ( A @ apply ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',upper_bound) ).
thf(194,plain,
! [A: $i,B: $i,C: $i] :
( ( ! [D: $i] :
( ( B @ ( D @ member ) )
=> ( C @ ( D @ ( A @ apply ) ) ) )
=> ( B @ ( A @ ( C @ upper_bound ) ) ) )
& ( ( B @ ( A @ ( C @ upper_bound ) ) )
=> ! [D: $i] :
( ( B @ ( D @ member ) )
=> ( C @ ( D @ ( A @ apply ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[12]) ).
thf(22,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ equal_set ) )
<=> ( ( A @ ( B @ subset ) )
& ( B @ ( A @ subset ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',equal_set) ).
thf(276,plain,
! [A: $i,B: $i] :
( ( ( ( A @ ( B @ subset ) )
& ( B @ ( A @ subset ) ) )
=> ( B @ ( A @ equal_set ) ) )
& ( ( B @ ( A @ equal_set ) )
=> ( ( A @ ( B @ subset ) )
& ( B @ ( A @ subset ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[22]) ).
thf(13,axiom,
! [A: $i,B: $i,C: $i] :
( ( B @ ( A @ ( C @ lower_bound ) ) )
<=> ! [D: $i] :
( ( B @ ( D @ member ) )
=> ( D @ ( C @ ( A @ apply ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',lower_bound) ).
thf(202,plain,
! [A: $i,B: $i,C: $i] :
( ( ! [D: $i] :
( ( B @ ( D @ member ) )
=> ( D @ ( C @ ( A @ apply ) ) ) )
=> ( B @ ( A @ ( C @ lower_bound ) ) ) )
& ( ( B @ ( A @ ( C @ lower_bound ) ) )
=> ! [D: $i] :
( ( B @ ( D @ member ) )
=> ( D @ ( C @ ( A @ apply ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[13]) ).
thf(10,axiom,
! [A: $i,B: $i] :
( ( B @ product @ ( A @ member ) )
<=> ! [C: $i] :
( ( B @ ( C @ member ) )
=> ( C @ ( A @ member ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product) ).
thf(174,plain,
! [A: $i,B: $i] :
( ( ! [C: $i] :
( ( B @ ( C @ member ) )
=> ( C @ ( A @ member ) ) )
=> ( B @ product @ ( A @ member ) ) )
& ( ( B @ product @ ( A @ member ) )
=> ! [C: $i] :
( ( B @ ( C @ member ) )
=> ( C @ ( A @ member ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).
thf(20,axiom,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ union ) @ ( A @ member ) )
<=> ( ( C @ ( A @ member ) )
| ( B @ ( A @ member ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',union) ).
thf(257,plain,
! [A: $i,B: $i,C: $i] :
( ( ( ( C @ ( A @ member ) )
| ( B @ ( A @ member ) ) )
=> ( C @ ( B @ union ) @ ( A @ member ) ) )
& ( ( C @ ( B @ union ) @ ( A @ member ) )
=> ( ( C @ ( A @ member ) )
| ( B @ ( A @ member ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[20]) ).
thf(290,plain,
! [B: $i,A: $i] :
( ( ( A @ singleton @ ( A @ member ) )
!= ( empty_set @ ( B @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[173,229]) ).
thf(291,plain,
! [B: $i,A: $i] :
( ( A @ singleton @ ( A @ member ) )
!= ( empty_set @ ( B @ member ) ) ),
inference(simp,[status(thm)],[290]) ).
thf(292,plain,
! [B: $i,A: $i] :
( ( ( A @ singleton )
!= empty_set )
| ( A != B ) ),
inference(simp,[status(thm)],[291]) ).
thf(293,plain,
! [A: $i] :
( ( A @ singleton )
!= empty_set ),
inference(simp,[status(thm)],[292]) ).
thf(169,plain,
! [B: $i,A: $i] :
( ( A = B )
| ~ ( B @ singleton @ ( A @ member ) ) ),
inference(cnfConj,[status(thm)],[168]) ).
thf(171,plain,
! [B: $i,A: $i] :
( ~ ( B @ singleton @ ( A @ member ) )
| ( A = B ) ),
inference(lifteq,[status(thm)],[169]) ).
thf(440,plain,
! [C: $i,B: $i,A: $i] :
( ( B
!= ( C @ singleton ) )
| ( A != empty_set )
| ~ ( B @ singleton @ ( A @ member ) ) ),
inference(paramod_ordered,[status(thm)],[171,293]) ).
thf(441,plain,
! [B: $i,A: $i] :
( ( A != empty_set )
| ~ ( B @ singleton @ singleton @ ( A @ member ) ) ),
inference(pattern_uni,[status(thm)],[440:[bind(A,$thf( A )),bind(B,$thf( D @ singleton )),bind(C,$thf( D ))]]) ).
thf(793,plain,
! [A: $i] :
~ ( A @ singleton @ singleton @ ( empty_set @ member ) ),
inference(simp,[status(thm)],[441]) ).
thf(27,plain,
( ( sk3 @ ( sk6 @ member ) )
| sk4 ),
inference(cnfConj,[status(thm)],[26]) ).
thf(298,plain,
! [A: $i] :
( ( ( sk3 @ ( sk6 @ member ) )
!= ( empty_set @ ( A @ member ) ) )
| ~ $true
| sk4 ),
inference(paramod_ordered,[status(thm)],[27,229]) ).
thf(299,plain,
! [A: $i] :
( ( ( sk3 @ ( sk6 @ member ) )
!= ( empty_set @ ( A @ member ) ) )
| sk4 ),
inference(simp,[status(thm)],[298]) ).
thf(302,plain,
! [A: $i] :
( ( sk3 != empty_set )
| ( sk6 != A )
| sk4 ),
inference(simp,[status(thm)],[299]) ).
thf(303,plain,
( ( sk3 != empty_set )
| sk4 ),
inference(simp,[status(thm)],[302]) ).
thf(32,plain,
( ~ sk4
| ( sk3 @ ( sk1 @ ( sk5 @ least ) ) ) ),
inference(cnfConj,[status(thm)],[26]) ).
thf(364,plain,
( ( sk4 != sk4 )
| ~ $true
| ( sk3 @ ( sk1 @ ( sk5 @ least ) ) )
| ( sk3 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[303,32]) ).
thf(365,plain,
( ( sk4 != sk4 )
| ( sk3 @ ( sk1 @ ( sk5 @ least ) ) )
| ( sk3 != empty_set ) ),
inference(simp,[status(thm)],[364]) ).
thf(366,plain,
( ( sk3 @ ( sk1 @ ( sk5 @ least ) ) )
| ( sk3 != empty_set ) ),
inference(pattern_uni,[status(thm)],[365:[]]) ).
thf(28,plain,
( ( sk2 @ ( sk1 @ ( sk3 @ ( sk6 @ greatest_lower_bound ) ) ) )
| sk4 ),
inference(cnfConj,[status(thm)],[26]) ).
thf(30,plain,
( ~ sk4
| ~ ( sk2 @ ( sk1 @ ( sk3 @ ( sk5 @ greatest_lower_bound ) ) ) )
| ~ ( sk3 @ ( sk5 @ member ) ) ),
inference(cnfConj,[status(thm)],[26]) ).
thf(294,plain,
! [A: $i] :
( ( ( A @ singleton @ ( A @ member ) )
!= ( sk3 @ ( sk5 @ member ) ) )
| ~ sk4
| ~ ( sk2 @ ( sk1 @ ( sk3 @ ( sk5 @ greatest_lower_bound ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[173,30]) ).
thf(295,plain,
! [A: $i] :
( ( ( A @ singleton @ ( A @ member ) )
!= ( sk3 @ ( sk5 @ member ) ) )
| ~ sk4
| ~ ( sk2 @ ( sk1 @ ( sk3 @ ( sk5 @ greatest_lower_bound ) ) ) ) ),
inference(simp,[status(thm)],[294]) ).
thf(296,plain,
! [A: $i] :
( ( ( A @ singleton )
!= sk3 )
| ( A != sk5 )
| ~ sk4
| ~ ( sk2 @ ( sk1 @ ( sk3 @ ( sk5 @ greatest_lower_bound ) ) ) ) ),
inference(simp,[status(thm)],[295]) ).
thf(297,plain,
( ( ( sk5 @ singleton )
!= sk3 )
| ~ sk4
| ~ ( sk2 @ ( sk1 @ ( sk3 @ ( sk5 @ greatest_lower_bound ) ) ) ) ),
inference(simp,[status(thm)],[296]) ).
thf(18,axiom,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ intersection ) @ ( A @ member ) )
<=> ( ( C @ ( A @ member ) )
& ( B @ ( A @ member ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intersection) ).
thf(237,plain,
! [A: $i,B: $i,C: $i] :
( ( ( ( C @ ( A @ member ) )
& ( B @ ( A @ member ) ) )
=> ( C @ ( B @ intersection ) @ ( A @ member ) ) )
& ( ( C @ ( B @ intersection ) @ ( A @ member ) )
=> ( ( C @ ( A @ member ) )
& ( B @ ( A @ member ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[18]) ).
thf(19,axiom,
! [A: $i,B: $i,C: $i] :
( ( B @ ( A @ ( C @ max ) ) )
<=> ( ! [D: $i] :
( ( ( D @ ( C @ ( A @ apply ) ) )
& ( B @ ( D @ member ) ) )
=> ( C = D ) )
& ( B @ ( C @ member ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',max) ).
thf(244,plain,
! [A: $i,B: $i,C: $i] :
( ( ( ! [D: $i] :
( ( ( D @ ( C @ ( A @ apply ) ) )
& ( B @ ( D @ member ) ) )
=> ( C = D ) )
& ( B @ ( C @ member ) ) )
=> ( B @ ( A @ ( C @ max ) ) ) )
& ( ( B @ ( A @ ( C @ max ) ) )
=> ( ! [D: $i] :
( ( ( D @ ( C @ ( A @ apply ) ) )
& ( B @ ( D @ member ) ) )
=> ( C = D ) )
& ( B @ ( C @ member ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[19]) ).
thf(399,plain,
! [A: $i] :
( ( ( sk3 @ ( sk6 @ member ) )
!= ( sk2 @ ( A @ member ) ) )
| ( A @ ( A @ ( sk1 @ apply ) ) )
| ~ $true
| sk4 ),
inference(paramod_ordered,[status(thm)],[27,389]) ).
thf(400,plain,
! [A: $i] :
( ( ( sk3 @ ( sk6 @ member ) )
!= ( sk2 @ ( A @ member ) ) )
| ( A @ ( A @ ( sk1 @ apply ) ) )
| sk4 ),
inference(simp,[status(thm)],[399]) ).
thf(408,plain,
! [A: $i] :
( ( sk3 != sk2 )
| ( sk6 != A )
| ( A @ ( A @ ( sk1 @ apply ) ) )
| sk4 ),
inference(simp,[status(thm)],[400]) ).
thf(412,plain,
( ( sk3 != sk2 )
| ( sk6 @ ( sk6 @ ( sk1 @ apply ) ) )
| sk4 ),
inference(simp,[status(thm)],[408]) ).
thf(7,axiom,
! [A: $i,B: $i] :
( ( B @ power_set @ ( A @ member ) )
<=> ( B @ ( A @ subset ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',power_set) ).
thf(148,plain,
! [A: $i,B: $i] :
( ( ( B @ ( A @ subset ) )
=> ( B @ power_set @ ( A @ member ) ) )
& ( ( B @ power_set @ ( A @ member ) )
=> ( B @ ( A @ subset ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(175,plain,
( ! [A: $i,B: $i] :
( ! [C: $i] :
( ( B @ ( C @ member ) )
=> ( C @ ( A @ member ) ) )
=> ( B @ product @ ( A @ member ) ) )
& ! [A: $i,B: $i] :
( ( B @ product @ ( A @ member ) )
=> ! [C: $i] :
( ( B @ ( C @ member ) )
=> ( C @ ( A @ member ) ) ) ) ),
inference(miniscope,[status(thm)],[174]) ).
thf(176,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( E @ product @ ( D @ member ) )
| ~ ( D @ ( E @ sk19 ) @ ( D @ member ) ) )
& ( ( E @ product @ ( D @ member ) )
| ( E @ ( D @ ( E @ sk19 ) @ member ) ) )
& ( ( C @ ( A @ member ) )
| ~ ( B @ ( C @ member ) )
| ~ ( B @ product @ ( A @ member ) ) ) ),
inference(cnf,[status(esa)],[175]) ).
thf(178,plain,
! [B: $i,A: $i] :
( ( B @ product @ ( A @ member ) )
| ( B @ ( A @ ( B @ sk19 ) @ member ) ) ),
inference(cnfConj,[status(thm)],[176]) ).
thf(180,plain,
! [B: $i,A: $i] :
( ( B @ product @ ( A @ member ) )
| ( B @ ( A @ ( B @ sk19 ) @ member ) ) ),
inference(simp,[status(thm)],[178]) ).
thf(394,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( B @ sk24 ) @ member ) )
!= ( sk2 @ ( C @ member ) ) )
| ( C @ ( C @ ( sk1 @ apply ) ) )
| ~ $true
| ( B @ ( A @ subset ) ) ),
inference(paramod_ordered,[status(thm)],[225,389]) ).
thf(395,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( B @ sk24 ) @ member ) )
!= ( sk2 @ ( C @ member ) ) )
| ( C @ ( C @ ( sk1 @ apply ) ) )
| ( B @ ( A @ subset ) ) ),
inference(simp,[status(thm)],[394]) ).
thf(396,plain,
! [A: $i] :
( ( sk2 @ ( A @ sk24 ) @ ( sk2 @ ( A @ sk24 ) @ ( sk1 @ apply ) ) )
| ( A @ ( sk2 @ subset ) ) ),
inference(pattern_uni,[status(thm)],[395:[bind(A,$thf( sk2 )),bind(B,$thf( D )),bind(C,$thf( sk2 @ ( D @ sk24 ) ))]]) ).
thf(413,plain,
! [A: $i] :
( ( sk2 @ ( A @ sk24 ) @ ( sk2 @ ( A @ sk24 ) @ ( sk1 @ apply ) ) )
| ( A @ ( sk2 @ subset ) ) ),
inference(simp,[status(thm)],[396]) ).
thf(17,axiom,
! [A: $i,B: $i,C: $i] :
( ( B @ ( C @ difference ) @ ( A @ member ) )
<=> ( ~ ( B @ ( A @ member ) )
& ( C @ ( A @ member ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',difference) ).
thf(230,plain,
! [A: $i,B: $i,C: $i] :
( ( ( ~ ( B @ ( A @ member ) )
& ( C @ ( A @ member ) ) )
=> ( B @ ( C @ difference ) @ ( A @ member ) ) )
& ( ( B @ ( C @ difference ) @ ( A @ member ) )
=> ( ~ ( B @ ( A @ member ) )
& ( C @ ( A @ member ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[17]) ).
thf(304,plain,
( ( sk4 != sk4 )
| ~ $true
| ~ ( sk2 @ ( sk1 @ ( sk3 @ ( sk5 @ greatest_lower_bound ) ) ) )
| ~ ( sk3 @ ( sk5 @ member ) )
| ( sk3 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[303,30]) ).
thf(305,plain,
( ( sk4 != sk4 )
| ~ ( sk2 @ ( sk1 @ ( sk3 @ ( sk5 @ greatest_lower_bound ) ) ) )
| ~ ( sk3 @ ( sk5 @ member ) )
| ( sk3 != empty_set ) ),
inference(simp,[status(thm)],[304]) ).
thf(306,plain,
( ~ ( sk2 @ ( sk1 @ ( sk3 @ ( sk5 @ greatest_lower_bound ) ) ) )
| ~ ( sk3 @ ( sk5 @ member ) )
| ( sk3 != empty_set ) ),
inference(pattern_uni,[status(thm)],[305:[]]) ).
thf(6,axiom,
! [A: $i,B: $i,C: $i] :
( ( B @ ( A @ ( C @ min ) ) )
<=> ( ! [D: $i] :
( ( ( C @ ( D @ ( A @ apply ) ) )
& ( B @ ( D @ member ) ) )
=> ( C = D ) )
& ( B @ ( C @ member ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',min) ).
thf(135,plain,
! [A: $i,B: $i,C: $i] :
( ( ( ! [D: $i] :
( ( ( C @ ( D @ ( A @ apply ) ) )
& ( B @ ( D @ member ) ) )
=> ( C = D ) )
& ( B @ ( C @ member ) ) )
=> ( B @ ( A @ ( C @ min ) ) ) )
& ( ( B @ ( A @ ( C @ min ) ) )
=> ( ! [D: $i] :
( ( ( C @ ( D @ ( A @ apply ) ) )
& ( B @ ( D @ member ) ) )
=> ( C = D ) )
& ( B @ ( C @ member ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(438,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( C @ singleton ) )
| ( B != empty_set )
| ~ ( B @ singleton @ ( A @ member ) ) ),
inference(paramod_ordered,[status(thm)],[171,293]) ).
thf(439,plain,
! [B: $i,A: $i] :
( ( A != empty_set )
| ~ ( A @ singleton @ ( B @ singleton @ member ) ) ),
inference(pattern_uni,[status(thm)],[438:[bind(A,$thf( D @ singleton )),bind(B,$thf( B )),bind(C,$thf( D ))]]) ).
thf(791,plain,
! [A: $i] :
~ ( empty_set @ singleton @ ( A @ singleton @ member ) ),
inference(simp,[status(thm)],[439]) ).
thf(827,plain,
! [B: $i,A: $i] :
( ( ( A @ singleton @ ( A @ member ) )
!= ( empty_set @ singleton @ ( B @ singleton @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[173,791]) ).
thf(828,plain,
! [B: $i,A: $i] :
( ( A @ singleton @ ( A @ member ) )
!= ( empty_set @ singleton @ ( B @ singleton @ member ) ) ),
inference(simp,[status(thm)],[827]) ).
thf(850,plain,
! [B: $i,A: $i] :
( ( ( A @ singleton )
!= ( empty_set @ singleton ) )
| ( A
!= ( B @ singleton ) ) ),
inference(simp,[status(thm)],[828]) ).
thf(855,plain,
! [A: $i] :
( ( A @ singleton @ singleton )
!= ( empty_set @ singleton ) ),
inference(simp,[status(thm)],[850]) ).
thf(325,plain,
( ( sk4 != sk4 )
| ( ( sk5 @ singleton )
!= sk3 )
| ~ $true
| ~ ( sk2 @ ( sk1 @ ( sk3 @ ( sk5 @ greatest_lower_bound ) ) ) )
| ( sk3 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[303,297]) ).
thf(326,plain,
( ( sk4 != sk4 )
| ( ( sk5 @ singleton )
!= sk3 )
| ~ ( sk2 @ ( sk1 @ ( sk3 @ ( sk5 @ greatest_lower_bound ) ) ) )
| ( sk3 != empty_set ) ),
inference(simp,[status(thm)],[325]) ).
thf(327,plain,
( ( ( sk5 @ singleton )
!= sk3 )
| ~ ( sk2 @ ( sk1 @ ( sk3 @ ( sk5 @ greatest_lower_bound ) ) ) )
| ( sk3 != empty_set ) ),
inference(pattern_uni,[status(thm)],[326:[]]) ).
thf(350,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( B @ sk24 ) @ member ) )
!= ( empty_set @ ( C @ member ) ) )
| ~ $true
| ( B @ ( A @ subset ) ) ),
inference(paramod_ordered,[status(thm)],[225,229]) ).
thf(351,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( B @ sk24 ) @ member ) )
!= ( empty_set @ ( C @ member ) ) )
| ( B @ ( A @ subset ) ) ),
inference(simp,[status(thm)],[350]) ).
thf(352,plain,
! [A: $i] : ( A @ ( empty_set @ subset ) ),
inference(pattern_uni,[status(thm)],[351:[bind(A,$thf( empty_set )),bind(B,$thf( D )),bind(C,$thf( empty_set @ ( D @ sk24 ) ))]]) ).
thf(359,plain,
! [A: $i] : ( A @ ( empty_set @ subset ) ),
inference(simp,[status(thm)],[352]) ).
thf(31,plain,
sk2 @ ( sk3 @ subset ),
inference(cnfConj,[status(thm)],[26]) ).
thf(11,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
( ( D @ ( C @ ( B @ ( A @ greatest_lower_bound ) ) ) )
<=> ( ! [E: $i] :
( ( ( B @ ( C @ ( E @ lower_bound ) ) )
& ( D @ ( E @ member ) ) )
=> ( A @ ( E @ ( C @ apply ) ) ) )
& ( B @ ( C @ ( A @ lower_bound ) ) )
& ( B @ ( A @ member ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',greatest_lower_bound) ).
thf(182,plain,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ( ! [E: $i] :
( ( ( B @ ( C @ ( E @ lower_bound ) ) )
& ( D @ ( E @ member ) ) )
=> ( A @ ( E @ ( C @ apply ) ) ) )
& ( B @ ( C @ ( A @ lower_bound ) ) )
& ( B @ ( A @ member ) ) )
=> ( D @ ( C @ ( B @ ( A @ greatest_lower_bound ) ) ) ) )
& ( ( D @ ( C @ ( B @ ( A @ greatest_lower_bound ) ) ) )
=> ( ! [E: $i] :
( ( ( B @ ( C @ ( E @ lower_bound ) ) )
& ( D @ ( E @ member ) ) )
=> ( A @ ( E @ ( C @ apply ) ) ) )
& ( B @ ( C @ ( A @ lower_bound ) ) )
& ( B @ ( A @ member ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[11]) ).
thf(576,plain,
! [B: $i,A: $i] :
( ( A
!= ( sk5 @ singleton ) )
| ( B != sk3 )
| ~ sk4
| ~ ( sk2 @ ( sk1 @ ( sk3 @ ( sk5 @ greatest_lower_bound ) ) ) )
| ~ ( B @ singleton @ ( A @ member ) ) ),
inference(paramod_ordered,[status(thm)],[171,297]) ).
thf(577,plain,
! [A: $i] :
( ( A != sk3 )
| ~ sk4
| ~ ( sk2 @ ( sk1 @ ( sk3 @ ( sk5 @ greatest_lower_bound ) ) ) )
| ~ ( A @ singleton @ ( sk5 @ singleton @ member ) ) ),
inference(pattern_uni,[status(thm)],[576:[bind(A,$thf( sk5 @ singleton )),bind(B,$thf( B ))]]) ).
thf(744,plain,
( ~ sk4
| ~ ( sk2 @ ( sk1 @ ( sk3 @ ( sk5 @ greatest_lower_bound ) ) ) )
| ~ ( sk3 @ singleton @ ( sk5 @ singleton @ member ) ) ),
inference(simp,[status(thm)],[577]) ).
thf(8,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
( ( D @ ( C @ ( B @ ( A @ least_upper_bound ) ) ) )
<=> ( ! [E: $i] :
( ( ( B @ ( C @ ( E @ upper_bound ) ) )
& ( D @ ( E @ member ) ) )
=> ( E @ ( A @ ( C @ apply ) ) ) )
& ( B @ ( C @ ( A @ upper_bound ) ) )
& ( B @ ( A @ member ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',least_upper_bound) ).
thf(154,plain,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ( ! [E: $i] :
( ( ( B @ ( C @ ( E @ upper_bound ) ) )
& ( D @ ( E @ member ) ) )
=> ( E @ ( A @ ( C @ apply ) ) ) )
& ( B @ ( C @ ( A @ upper_bound ) ) )
& ( B @ ( A @ member ) ) )
=> ( D @ ( C @ ( B @ ( A @ least_upper_bound ) ) ) ) )
& ( ( D @ ( C @ ( B @ ( A @ least_upper_bound ) ) ) )
=> ( ! [E: $i] :
( ( ( B @ ( C @ ( E @ upper_bound ) ) )
& ( D @ ( E @ member ) ) )
=> ( E @ ( A @ ( C @ apply ) ) ) )
& ( B @ ( C @ ( A @ upper_bound ) ) )
& ( B @ ( A @ member ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(69,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ order ) )
| ( A @ ( B @ sk13 ) @ ( A @ ( B @ sk12 ) @ ( A @ apply ) ) )
| ( B @ ( A @ ( B @ sk10 ) @ member ) )
| ( A @ ( B @ sk7 ) ) ),
inference(cnfConj,[status(thm)],[36]) ).
thf(72,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ order ) )
| ( A @ ( B @ sk13 ) @ ( A @ ( B @ sk12 ) @ ( A @ apply ) ) )
| ( B @ ( A @ ( B @ sk10 ) @ member ) )
| ( A @ ( B @ sk7 ) ) ),
inference(simp,[status(thm)],[69]) ).
thf(476,plain,
! [B: $i,A: $i] :
( ( A != sk3 )
| ( B != empty_set )
| sk4
| ~ ( B @ singleton @ ( A @ member ) ) ),
inference(paramod_ordered,[status(thm)],[171,303]) ).
thf(477,plain,
! [A: $i] :
( ( A != empty_set )
| sk4
| ~ ( A @ singleton @ ( sk3 @ member ) ) ),
inference(pattern_uni,[status(thm)],[476:[bind(A,$thf( sk3 ))]]) ).
thf(813,plain,
( sk4
| ~ ( empty_set @ singleton @ ( sk3 @ member ) ) ),
inference(simp,[status(thm)],[477]) ).
thf(269,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ unordered_pair ) @ ( A @ member ) )
| ( A != B ) ),
inference(cnfConj,[status(thm)],[267]) ).
thf(272,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ unordered_pair ) @ ( A @ member ) )
| ( A != B ) ),
inference(lifteq,[status(thm)],[269]) ).
thf(273,plain,
! [B: $i,A: $i] : ( B @ ( A @ unordered_pair ) @ ( A @ member ) ),
inference(simp,[status(thm)],[272]) ).
thf(309,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ unordered_pair ) @ ( A @ member ) )
!= ( empty_set @ ( C @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[273,229]) ).
thf(310,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( A @ unordered_pair ) @ ( A @ member ) )
!= ( empty_set @ ( C @ member ) ) ),
inference(simp,[status(thm)],[309]) ).
thf(313,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ unordered_pair ) )
!= empty_set )
| ( A != C ) ),
inference(simp,[status(thm)],[310]) ).
thf(315,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ unordered_pair ) )
!= empty_set ),
inference(simp,[status(thm)],[313]) ).
thf(397,plain,
! [B: $i,A: $i] :
( ( ( A @ singleton @ ( A @ member ) )
!= ( sk2 @ ( B @ member ) ) )
| ( B @ ( B @ ( sk1 @ apply ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[173,389]) ).
thf(398,plain,
! [B: $i,A: $i] :
( ( ( A @ singleton @ ( A @ member ) )
!= ( sk2 @ ( B @ member ) ) )
| ( B @ ( B @ ( sk1 @ apply ) ) ) ),
inference(simp,[status(thm)],[397]) ).
thf(406,plain,
! [B: $i,A: $i] :
( ( ( A @ singleton )
!= sk2 )
| ( A != B )
| ( B @ ( B @ ( sk1 @ apply ) ) ) ),
inference(simp,[status(thm)],[398]) ).
thf(410,plain,
! [A: $i] :
( ( ( A @ singleton )
!= sk2 )
| ( A @ ( A @ ( sk1 @ apply ) ) ) ),
inference(simp,[status(thm)],[406]) ).
thf(14,axiom,
! [A: $i,B: $i,C: $i] :
( ( B @ ( A @ ( C @ greatest ) ) )
<=> ( ! [D: $i] :
( ( B @ ( D @ member ) )
=> ( C @ ( D @ ( A @ apply ) ) ) )
& ( B @ ( C @ member ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',greatest) ).
thf(210,plain,
! [A: $i,B: $i,C: $i] :
( ( ( ! [D: $i] :
( ( B @ ( D @ member ) )
=> ( C @ ( D @ ( A @ apply ) ) ) )
& ( B @ ( C @ member ) ) )
=> ( B @ ( A @ ( C @ greatest ) ) ) )
& ( ( B @ ( A @ ( C @ greatest ) ) )
=> ( ! [D: $i] :
( ( B @ ( D @ member ) )
=> ( C @ ( D @ ( A @ apply ) ) ) )
& ( B @ ( C @ member ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[14]) ).
thf(5,axiom,
! [A: $i,B: $i,C: $i] :
( ( B @ ( A @ ( C @ least ) ) )
<=> ( ! [D: $i] :
( ( B @ ( D @ member ) )
=> ( D @ ( C @ ( A @ apply ) ) ) )
& ( B @ ( C @ member ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',least) ).
thf(126,plain,
! [A: $i,B: $i,C: $i] :
( ( ( ! [D: $i] :
( ( B @ ( D @ member ) )
=> ( D @ ( C @ ( A @ apply ) ) ) )
& ( B @ ( C @ member ) ) )
=> ( B @ ( A @ ( C @ least ) ) ) )
& ( ( B @ ( A @ ( C @ least ) ) )
=> ( ! [D: $i] :
( ( B @ ( D @ member ) )
=> ( D @ ( C @ ( A @ apply ) ) ) )
& ( B @ ( C @ member ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(23,axiom,
! [A: $i,B: $i] :
( ( B @ sum @ ( A @ member ) )
<=> ? [C: $i] :
( ( C @ ( A @ member ) )
& ( B @ ( C @ member ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sum) ).
thf(283,plain,
! [A: $i,B: $i] :
( ( ? [C: $i] :
( ( C @ ( A @ member ) )
& ( B @ ( C @ member ) ) )
=> ( B @ sum @ ( A @ member ) ) )
& ( ( B @ sum @ ( A @ member ) )
=> ? [C: $i] :
( ( C @ ( A @ member ) )
& ( B @ ( C @ member ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[23]) ).
thf(2857,plain,
$false,
inference(e,[status(thm)],[389,29,121,229,225,173,323,194,47,227,276,202,174,24,257,293,265,793,366,28,297,275,33,237,244,412,166,148,180,32,34,27,413,113,219,230,303,306,135,855,327,359,31,791,182,744,154,72,813,171,315,410,30,273,210,126,283]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SET802+4 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.07 % 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.13/0.38 % Computer : n008.cluster.edu
% 0.13/0.38 % Model : x86_64 x86_64
% 0.13/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.38 % Memory : 8046.5625MB
% 0.13/0.38 % OS : Linux 6.8.0-71-generic
% 0.13/0.38 % CPULimit : 300
% 0.13/0.38 % WCLimit : 300
% 0.13/0.38 % DateTime : Sat Sep 26 08:17:39 UTC 2026
% 0.13/0.38 % CPUTime :
% 0.13/0.38 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.63/0.69 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.02/0.81 % [INFO] Parsing done (122ms).
% 1.02/0.82 % [INFO] Running in sequential loop mode.
% 1.35/1.02 % [INFO] eprover registered as external prover.
% 1.35/1.03 % [INFO] Scanning for conjecture ...
% 1.66/1.08 % [INFO] Found a conjecture (or negated_conjecture) and 21 axioms. Running axiom selection ...
% 1.66/1.12 % [INFO] Axiom selection finished. Selected 21 axioms (removed 0 axioms).
% 1.91/1.16 % [INFO] Problem is first-order (TPTP FOF).
% 1.91/1.16 % [INFO] Type checking passed.
% 1.91/1.17 % [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 ...
% 18.25/4.35 % External prover 'e' found a proof!
% 18.25/4.35 % [INFO] Killing All external provers ...
% 18.25/4.36 % Time passed: 3887ms (effective reasoning time: 3536ms)
% 18.25/4.36 % 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)>
% 18.25/4.36 % Axioms used in derivation (21): power_set, unordered_pair, union, intersection, empty_set, upper_bound, min, least, max, total_order, singleton, difference, product, least_upper_bound, greatest_lower_bound, greatest, subset, order, equal_set, lower_bound, sum
% 18.25/4.36 % No. of inferences in proof: 153
% 18.25/4.36 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 3887 ms resp. 3536 ms w/o parsing
% 16.88/4.52 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 16.88/4.52 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------