%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SET644+3 : TPTP v9.3.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n018.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 : Fri Sep 25 02:43:42 PM UTC 2026
% Result : Theorem 26.37s 4.24s
% Output : Proof 26.37s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 12
% Syntax : Number of formulae : 106 ( 20 unt; 0 def)
% Number of atoms : 419 ( 30 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 533 ( 220 ~; 215 |; 56 &)
% ( 6 <=>; 36 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 6 con; 0-2 aty)
% Number of variables : 220 ( 17 sgn 87 !; 13 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f18,axiom,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ( member(B,power_set(C))
<=> ! [D] :
( ilf_type(D,set_type)
=> ( member(D,B)
=> member(D,C) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p19) ).
fof(f18_nnf,plain,
! [B] :
( ! [C] :
( ( ( ? [D] :
( ~ member(D,C)
& member(D,B)
& ilf_type(D,set_type) )
| member(B,power_set(C)) )
& ( ! [D] :
( member(D,C)
| ~ member(D,B)
| ~ ilf_type(D,set_type) )
| ~ member(B,power_set(C)) ) )
| ~ ilf_type(C,set_type) )
| ~ ilf_type(B,set_type) ),
inference(nnf_transformation,[status(thm)],[f18]) ).
fof(f18_sk,plain,
! [B,C,D] :
( ( ( ( ~ member(sk7(B,C),C)
& member(sk7(B,C),B)
& ilf_type(sk7(B,C),set_type) )
| member(B,power_set(C)) )
& ( member(D,C)
| ~ member(D,B)
| ~ ilf_type(D,set_type)
| ~ member(B,power_set(C)) ) )
| ~ ilf_type(C,set_type)
| ~ ilf_type(B,set_type) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk7])],[f18_nnf]) ).
cnf(c38,plain,
( member(X2,X1)
| ~ member(X2,X0)
| ~ ilf_type(X2,set_type)
| ~ member(X0,power_set(X1))
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
fof(f26,axiom,
! [B] : ilf_type(B,set_type),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p27) ).
fof(f26_nnf,plain,
! [B] : ilf_type(B,set_type),
inference(nnf_transformation,[status(thm)],[f26]) ).
fof(f26_sk,plain,
! [B] : ilf_type(B,set_type),
inference(skolemisation,[status(esa)],[f26_nnf]) ).
cnf(c58,plain,
ilf_type(X0,set_type),
inference(cnf_transformation,[status(esa)],[f26_sk]) ).
cnf(p187,plain,
( member(X2,X0)
| ~ member(X2,X1)
| ~ ilf_type(X2,set_type)
| ~ member(X1,power_set(X0))
| ~ ilf_type(X0,set_type) ),
inference(resolution,[status(thm)],[c38,c58]) ).
cnf(p501,plain,
( member(X2,X1)
| ~ member(X2,X0)
| ~ ilf_type(X2,set_type)
| ~ member(X0,power_set(X1)) ),
inference(resolution,[status(thm)],[p187,c58]) ).
fof(f20,axiom,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ( ilf_type(C,set_type)
& ~ empty(C) )
=> ( ilf_type(B,member_type(C))
<=> member(B,C) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p21) ).
fof(f20_nnf,plain,
! [B] :
( ! [C] :
( ( ( ~ member(B,C)
| ilf_type(B,member_type(C)) )
& ( member(B,C)
| ~ ilf_type(B,member_type(C)) ) )
| ~ ilf_type(C,set_type)
| empty(C) )
| ~ ilf_type(B,set_type) ),
inference(nnf_transformation,[status(thm)],[f20]) ).
fof(f20_sk,plain,
! [B,C] :
( ( ( ~ member(B,C)
| ilf_type(B,member_type(C)) )
& ( member(B,C)
| ~ ilf_type(B,member_type(C)) ) )
| ~ ilf_type(C,set_type)
| empty(C)
| ~ ilf_type(B,set_type) ),
inference(skolemisation,[status(esa)],[f20_nnf]) ).
cnf(c44,plain,
( member(X0,X1)
| ~ ilf_type(X0,member_type(X1))
| ~ ilf_type(X1,set_type)
| empty(X1)
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(esa)],[f20_sk]) ).
cnf(p205,plain,
( member(X1,X0)
| ~ ilf_type(X1,member_type(X0))
| ~ ilf_type(X0,set_type)
| empty(X0) ),
inference(resolution,[status(thm)],[c44,c58]) ).
cnf(p211,plain,
( member(X1,X0)
| ~ ilf_type(X1,member_type(X0))
| empty(X0) ),
inference(resolution,[status(thm)],[p205,c58]) ).
fof(f4,axiom,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ( ! [E] :
( ilf_type(E,relation_type(B,C))
=> ilf_type(E,subset_type(cross_product(B,C))) )
& ! [D] :
( ilf_type(D,subset_type(cross_product(B,C)))
=> ilf_type(D,relation_type(B,C)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p5) ).
fof(f4_nnf,plain,
! [B] :
( ! [C] :
( ( ! [E] :
( ilf_type(E,subset_type(cross_product(B,C)))
| ~ ilf_type(E,relation_type(B,C)) )
& ! [D] :
( ilf_type(D,relation_type(B,C))
| ~ ilf_type(D,subset_type(cross_product(B,C))) ) )
| ~ ilf_type(C,set_type) )
| ~ ilf_type(B,set_type) ),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [B,C,D,E] :
( ( ( ilf_type(E,subset_type(cross_product(B,C)))
| ~ ilf_type(E,relation_type(B,C)) )
& ( ilf_type(D,relation_type(B,C))
| ~ ilf_type(D,subset_type(cross_product(B,C))) ) )
| ~ ilf_type(C,set_type)
| ~ ilf_type(B,set_type) ),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c10,plain,
( ilf_type(X3,subset_type(cross_product(X0,X1)))
| ~ ilf_type(X3,relation_type(X0,X1))
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p115,plain,
( ilf_type(X1,subset_type(cross_product(X2,X0)))
| ~ ilf_type(X1,relation_type(X2,X0))
| ~ ilf_type(X0,set_type) ),
inference(resolution,[status(thm)],[c10,c58]) ).
cnf(p149,plain,
( ilf_type(X0,subset_type(cross_product(X1,X2)))
| ~ ilf_type(X0,relation_type(X1,X2)) ),
inference(resolution,[status(thm)],[p115,c58]) ).
fof(f27,conjecture,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ! [D] :
( ilf_type(D,set_type)
=> ! [E] :
( ilf_type(E,relation_type(B,C))
=> ( member(D,E)
=> ? [F] :
( ? [G] :
( member(G,C)
& member(F,B)
& D = ordered_pair(F,G)
& ilf_type(G,set_type) )
& ilf_type(F,set_type) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_relset_1_6) ).
fof(f27_neg,negated_conjecture,
~ ! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ! [D] :
( ilf_type(D,set_type)
=> ! [E] :
( ilf_type(E,relation_type(B,C))
=> ( member(D,E)
=> ? [F] :
( ? [G] :
( member(G,C)
& member(F,B)
& D = ordered_pair(F,G)
& ilf_type(G,set_type) )
& ilf_type(F,set_type) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f27]) ).
fof(f27_nnf,plain,
? [B] :
( ? [C] :
( ? [D] :
( ? [E] :
( ! [F] :
( ! [G] :
( ~ member(G,C)
| ~ member(F,B)
| D != ordered_pair(F,G)
| ~ ilf_type(G,set_type) )
| ~ ilf_type(F,set_type) )
& member(D,E)
& ilf_type(E,relation_type(B,C)) )
& ilf_type(D,set_type) )
& ilf_type(C,set_type) )
& ilf_type(B,set_type) ),
inference(nnf_transformation,[status(thm)],[f27_neg]) ).
fof(f27_sk,plain,
! [F,G] :
( ( ~ member(G,sk14)
| ~ member(F,sk13)
| sk15 != ordered_pair(F,G)
| ~ ilf_type(G,set_type)
| ~ ilf_type(F,set_type) )
& member(sk15,sk16)
& ilf_type(sk16,relation_type(sk13,sk14))
& ilf_type(sk15,set_type)
& ilf_type(sk14,set_type)
& ilf_type(sk13,set_type) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk13,sk14,sk15,sk16])],[f27_nnf]) ).
cnf(c62,plain,
ilf_type(sk16,relation_type(sk13,sk14)),
inference(cnf_transformation,[status(esa)],[f27_sk]) ).
cnf(p150,plain,
ilf_type(sk16,subset_type(cross_product(sk13,sk14))),
inference(resolution,[status(thm)],[p149,c62]) ).
fof(f13,axiom,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ( ilf_type(C,subset_type(B))
<=> ilf_type(C,member_type(power_set(B))) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p14) ).
fof(f13_nnf,plain,
! [B] :
( ! [C] :
( ( ( ~ ilf_type(C,member_type(power_set(B)))
| ilf_type(C,subset_type(B)) )
& ( ilf_type(C,member_type(power_set(B)))
| ~ ilf_type(C,subset_type(B)) ) )
| ~ ilf_type(C,set_type) )
| ~ ilf_type(B,set_type) ),
inference(nnf_transformation,[status(thm)],[f13]) ).
fof(f13_sk,plain,
! [B,C] :
( ( ( ~ ilf_type(C,member_type(power_set(B)))
| ilf_type(C,subset_type(B)) )
& ( ilf_type(C,member_type(power_set(B)))
| ~ ilf_type(C,subset_type(B)) ) )
| ~ ilf_type(C,set_type)
| ~ ilf_type(B,set_type) ),
inference(skolemisation,[status(esa)],[f13_nnf]) ).
cnf(c23,plain,
( ilf_type(X1,member_type(power_set(X0)))
| ~ ilf_type(X1,subset_type(X0))
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(p132,plain,
( ilf_type(X0,member_type(power_set(X1)))
| ~ ilf_type(X0,subset_type(X1))
| ~ ilf_type(X0,set_type) ),
inference(resolution,[status(thm)],[c23,c58]) ).
cnf(p133,plain,
( ilf_type(X0,member_type(power_set(X1)))
| ~ ilf_type(X0,subset_type(X1)) ),
inference(resolution,[status(thm)],[p132,c58]) ).
cnf(p152,plain,
ilf_type(sk16,member_type(power_set(cross_product(sk13,sk14)))),
inference(resolution,[status(thm)],[p150,p133]) ).
cnf(p214,plain,
( member(sk16,power_set(cross_product(sk13,sk14)))
| empty(power_set(cross_product(sk13,sk14))) ),
inference(resolution,[status(thm)],[p211,p152]) ).
cnf(p511,plain,
( empty(power_set(cross_product(sk13,sk14)))
| member(X0,cross_product(sk13,sk14))
| ~ member(X0,sk16)
| ~ ilf_type(X0,set_type) ),
inference(resolution,[status(thm)],[p501,p214]) ).
cnf(p1293,plain,
( empty(power_set(cross_product(sk13,sk14)))
| member(X0,cross_product(sk13,sk14))
| ~ member(X0,sk16) ),
inference(resolution,[status(thm)],[p511,c58]) ).
cnf(c63,plain,
member(sk15,sk16),
inference(cnf_transformation,[status(esa)],[f27_sk]) ).
cnf(p1294,plain,
( empty(power_set(cross_product(sk13,sk14)))
| member(sk15,cross_product(sk13,sk14)) ),
inference(resolution,[status(thm)],[p1293,c63]) ).
fof(f19,axiom,
! [B] :
( ilf_type(B,set_type)
=> ( ilf_type(power_set(B),set_type)
& ~ empty(power_set(B)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p20) ).
fof(f19_nnf,plain,
! [B] :
( ( ilf_type(power_set(B),set_type)
& ~ empty(power_set(B)) )
| ~ ilf_type(B,set_type) ),
inference(nnf_transformation,[status(thm)],[f19]) ).
fof(f19_sk,plain,
! [B] :
( ( ilf_type(power_set(B),set_type)
& ~ empty(power_set(B)) )
| ~ ilf_type(B,set_type) ),
inference(skolemisation,[status(esa)],[f19_nnf]) ).
cnf(c42,plain,
( ~ empty(power_set(X0))
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(p66,plain,
~ empty(power_set(X0)),
inference(resolution,[status(thm)],[c42,c58]) ).
cnf(p1327,plain,
member(sk15,cross_product(sk13,sk14)),
inference(resolution,[status(thm)],[p1294,p66]) ).
fof(f0,axiom,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,binary_relation_type)
=> ( member(B,C)
=> ? [D] :
( ? [E] :
( B = ordered_pair(D,E)
& ilf_type(E,set_type) )
& ilf_type(D,set_type) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p1) ).
fof(f0_nnf,plain,
! [B] :
( ! [C] :
( ? [D] :
( ? [E] :
( B = ordered_pair(D,E)
& ilf_type(E,set_type) )
& ilf_type(D,set_type) )
| ~ member(B,C)
| ~ ilf_type(C,binary_relation_type) )
| ~ ilf_type(B,set_type) ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [B,C] :
( ( B = ordered_pair(sk0(B,C),sk1(B,C))
& ilf_type(sk1(B,C),set_type)
& ilf_type(sk0(B,C),set_type) )
| ~ member(B,C)
| ~ ilf_type(C,binary_relation_type)
| ~ ilf_type(B,set_type) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0,sk1])],[f0_nnf]) ).
cnf(c2,plain,
( X0 = ordered_pair(sk0(X0,X1),sk1(X0,X1))
| ~ member(X0,X1)
| ~ ilf_type(X1,binary_relation_type)
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p67,plain,
( X1 = ordered_pair(sk0(X1,X0),sk1(X1,X0))
| ~ member(X1,X0)
| ~ ilf_type(X0,binary_relation_type) ),
inference(resolution,[status(thm)],[c2,c58]) ).
fof(f23,axiom,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ! [D] :
( ilf_type(D,subset_type(cross_product(B,C)))
=> relation_like(D) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p24) ).
fof(f23_nnf,plain,
! [B] :
( ! [C] :
( ! [D] :
( relation_like(D)
| ~ ilf_type(D,subset_type(cross_product(B,C))) )
| ~ ilf_type(C,set_type) )
| ~ ilf_type(B,set_type) ),
inference(nnf_transformation,[status(thm)],[f23]) ).
fof(f23_sk,plain,
! [B,C,D] :
( relation_like(D)
| ~ ilf_type(D,subset_type(cross_product(B,C)))
| ~ ilf_type(C,set_type)
| ~ ilf_type(B,set_type) ),
inference(skolemisation,[status(esa)],[f23_nnf]) ).
cnf(c53,plain,
( relation_like(X2)
| ~ ilf_type(X2,subset_type(cross_product(X0,X1)))
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(esa)],[f23_sk]) ).
cnf(p160,plain,
( relation_like(X1)
| ~ ilf_type(X1,subset_type(cross_product(X2,X0)))
| ~ ilf_type(X0,set_type) ),
inference(resolution,[status(thm)],[c53,c58]) ).
cnf(p161,plain,
( relation_like(X0)
| ~ ilf_type(X0,subset_type(cross_product(X1,X2))) ),
inference(resolution,[status(thm)],[p160,c58]) ).
cnf(p165,plain,
relation_like(sk16),
inference(resolution,[status(thm)],[p161,p150]) ).
fof(f11,axiom,
! [B] :
( ilf_type(B,set_type)
=> ( ilf_type(B,binary_relation_type)
<=> ( ilf_type(B,set_type)
& relation_like(B) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p12) ).
fof(f11_nnf,plain,
! [B] :
( ( ( ~ ilf_type(B,set_type)
| ~ relation_like(B)
| ilf_type(B,binary_relation_type) )
& ( ( ilf_type(B,set_type)
& relation_like(B) )
| ~ ilf_type(B,binary_relation_type) ) )
| ~ ilf_type(B,set_type) ),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [B] :
( ( ( ~ ilf_type(B,set_type)
| ~ relation_like(B)
| ilf_type(B,binary_relation_type) )
& ( ( ilf_type(B,set_type)
& relation_like(B) )
| ~ ilf_type(B,binary_relation_type) ) )
| ~ ilf_type(B,set_type) ),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c21,plain,
( ~ ilf_type(X0,set_type)
| ~ relation_like(X0)
| ilf_type(X0,binary_relation_type)
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(p100,plain,
( ~ relation_like(X0)
| ilf_type(X0,binary_relation_type)
| ~ ilf_type(X0,set_type) ),
inference(factoring,[status(thm)],[c21]) ).
cnf(p105,plain,
( ~ relation_like(X0)
| ilf_type(X0,binary_relation_type) ),
inference(resolution,[status(thm)],[p100,c58]) ).
cnf(p167,plain,
ilf_type(sk16,binary_relation_type),
inference(resolution,[status(thm)],[p165,p105]) ).
cnf(p175,plain,
( X0 = ordered_pair(sk0(X0,sk16),sk1(X0,sk16))
| ~ member(X0,sk16) ),
inference(resolution,[status(thm)],[p67,p167]) ).
cnf(p181,plain,
sk15 = ordered_pair(sk0(sk15,sk16),sk1(sk15,sk16)),
inference(resolution,[status(thm)],[p175,c63]) ).
fof(f6,axiom,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ( B = C
<=> ( subset(C,B)
& subset(B,C) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p7) ).
fof(f6_nnf,plain,
! [B] :
( ! [C] :
( ( ( ~ subset(C,B)
| ~ subset(B,C)
| B = C )
& ( ( subset(C,B)
& subset(B,C) )
| B != C ) )
| ~ ilf_type(C,set_type) )
| ~ ilf_type(B,set_type) ),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [B,C] :
( ( ( ~ subset(C,B)
| ~ subset(B,C)
| B = C )
& ( ( subset(C,B)
& subset(B,C) )
| B != C ) )
| ~ ilf_type(C,set_type)
| ~ ilf_type(B,set_type) ),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c13,plain,
( subset(X1,X0)
| X0 != X1
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(p117,plain,
( subset(X0,X1)
| X1 != X0
| ~ ilf_type(X0,set_type) ),
inference(resolution,[status(thm)],[c13,c58]) ).
cnf(p118,plain,
( subset(X1,X0)
| X0 != X1 ),
inference(resolution,[status(thm)],[p117,c58]) ).
cnf(p189,plain,
subset(ordered_pair(sk0(sk15,sk16),sk1(sk15,sk16)),sk15),
inference(resolution,[status(thm)],[p181,p118]) ).
cnf(c14,plain,
( ~ subset(X1,X0)
| ~ subset(X0,X1)
| X0 = X1
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(p119,plain,
( ~ subset(X0,X1)
| ~ subset(X1,X0)
| X1 = X0
| ~ ilf_type(X0,set_type) ),
inference(resolution,[status(thm)],[c14,c58]) ).
cnf(p139,plain,
( ~ subset(X1,X0)
| ~ subset(X0,X1)
| X0 = X1 ),
inference(resolution,[status(thm)],[p119,c58]) ).
cnf(p190,plain,
( ~ subset(sk15,ordered_pair(sk0(sk15,sk16),sk1(sk15,sk16)))
| ordered_pair(sk0(sk15,sk16),sk1(sk15,sk16)) = sk15 ),
inference(resolution,[status(thm)],[p189,p139]) ).
cnf(c12,plain,
( subset(X0,X1)
| X0 != X1
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(p113,plain,
( subset(X1,X0)
| X1 != X0
| ~ ilf_type(X0,set_type) ),
inference(resolution,[status(thm)],[c12,c58]) ).
cnf(p116,plain,
( subset(X0,X1)
| X0 != X1 ),
inference(resolution,[status(thm)],[p113,c58]) ).
cnf(p188,plain,
subset(sk15,ordered_pair(sk0(sk15,sk16),sk1(sk15,sk16))),
inference(resolution,[status(thm)],[p181,p116]) ).
cnf(p456,plain,
ordered_pair(sk0(sk15,sk16),sk1(sk15,sk16)) = sk15,
inference(resolution,[status(thm)],[p190,p188]) ).
fof(f1,axiom,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ! [D] :
( ilf_type(D,set_type)
=> ! [E] :
( ilf_type(E,set_type)
=> ( member(ordered_pair(B,C),cross_product(D,E))
<=> ( member(C,E)
& member(B,D) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p2) ).
fof(f1_nnf,plain,
! [B] :
( ! [C] :
( ! [D] :
( ! [E] :
( ( ( ~ member(C,E)
| ~ member(B,D)
| member(ordered_pair(B,C),cross_product(D,E)) )
& ( ( member(C,E)
& member(B,D) )
| ~ member(ordered_pair(B,C),cross_product(D,E)) ) )
| ~ ilf_type(E,set_type) )
| ~ ilf_type(D,set_type) )
| ~ ilf_type(C,set_type) )
| ~ ilf_type(B,set_type) ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [B,C,D,E] :
( ( ( ~ member(C,E)
| ~ member(B,D)
| member(ordered_pair(B,C),cross_product(D,E)) )
& ( ( member(C,E)
& member(B,D) )
| ~ member(ordered_pair(B,C),cross_product(D,E)) ) )
| ~ ilf_type(E,set_type)
| ~ ilf_type(D,set_type)
| ~ ilf_type(C,set_type)
| ~ ilf_type(B,set_type) ),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c3,plain,
( member(X0,X2)
| ~ member(ordered_pair(X0,X1),cross_product(X2,X3))
| ~ ilf_type(X3,set_type)
| ~ ilf_type(X2,set_type)
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p75,plain,
( member(X3,X1)
| ~ member(ordered_pair(X3,X0),cross_product(X1,X2))
| ~ ilf_type(X2,set_type)
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X0,set_type) ),
inference(resolution,[status(thm)],[c3,c58]) ).
cnf(p272,plain,
( member(X2,X0)
| ~ member(ordered_pair(X2,X3),cross_product(X0,X1))
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X0,set_type) ),
inference(resolution,[status(thm)],[p75,c58]) ).
cnf(p841,plain,
( member(X1,X3)
| ~ member(ordered_pair(X1,X2),cross_product(X3,X0))
| ~ ilf_type(X0,set_type) ),
inference(resolution,[status(thm)],[p272,c58]) ).
cnf(p842,plain,
( member(X0,X2)
| ~ member(ordered_pair(X0,X1),cross_product(X2,X3)) ),
inference(resolution,[status(thm)],[p841,c58]) ).
cnf(p849,plain,
( member(sk0(sk15,sk16),X0)
| ~ member(sk15,cross_product(X0,X1)) ),
inference(superposition,[status(thm)],[p456,p842]) ).
cnf(p1330,plain,
member(sk0(sk15,sk16),sk13),
inference(resolution,[status(thm)],[p1327,p849]) ).
cnf(c64,plain,
( ~ member(X5,sk14)
| ~ member(X4,sk13)
| sk15 != ordered_pair(X4,X5)
| ~ ilf_type(X5,set_type)
| ~ ilf_type(X4,set_type) ),
inference(cnf_transformation,[status(esa)],[f27_sk]) ).
cnf(p245,plain,
( ~ member(X0,sk14)
| ~ member(X1,sk13)
| sk15 != ordered_pair(X1,X0)
| ~ ilf_type(X0,set_type) ),
inference(resolution,[status(thm)],[c64,c58]) ).
cnf(p287,plain,
( ~ member(X1,sk14)
| ~ member(X0,sk13)
| sk15 != ordered_pair(X0,X1) ),
inference(resolution,[status(thm)],[p245,c58]) ).
cnf(p288,plain,
( ~ member(sk1(sk15,sk16),sk14)
| ~ member(sk0(sk15,sk16),sk13) ),
inference(resolution,[status(thm)],[p287,p181]) ).
cnf(p1335,plain,
~ member(sk1(sk15,sk16),sk14),
inference(resolution,[status(thm)],[p1330,p288]) ).
cnf(c4,plain,
( member(X1,X3)
| ~ member(ordered_pair(X0,X1),cross_product(X2,X3))
| ~ ilf_type(X3,set_type)
| ~ ilf_type(X2,set_type)
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X0,set_type) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p84,plain,
( member(X0,X2)
| ~ member(ordered_pair(X3,X0),cross_product(X1,X2))
| ~ ilf_type(X2,set_type)
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X0,set_type) ),
inference(resolution,[status(thm)],[c4,c58]) ).
cnf(p306,plain,
( member(X3,X1)
| ~ member(ordered_pair(X2,X3),cross_product(X0,X1))
| ~ ilf_type(X1,set_type)
| ~ ilf_type(X0,set_type) ),
inference(resolution,[status(thm)],[p84,c58]) ).
cnf(p1033,plain,
( member(X2,X0)
| ~ member(ordered_pair(X1,X2),cross_product(X3,X0))
| ~ ilf_type(X0,set_type) ),
inference(resolution,[status(thm)],[p306,c58]) ).
cnf(p1035,plain,
( member(X1,X3)
| ~ member(ordered_pair(X0,X1),cross_product(X2,X3)) ),
inference(resolution,[status(thm)],[p1033,c58]) ).
cnf(p1042,plain,
( member(sk1(sk15,sk16),X1)
| ~ member(sk15,cross_product(X0,X1)) ),
inference(superposition,[status(thm)],[p456,p1035]) ).
cnf(p1332,plain,
member(sk1(sk15,sk16),sk14),
inference(resolution,[status(thm)],[p1327,p1042]) ).
cnf(p1341,plain,
$false,
inference(resolution,[status(thm)],[p1335,p1332]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SET644+3 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.08/0.35 % Computer : n018.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Thu Sep 24 11:35:18 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.35 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 26.37/4.24 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 26.37/4.24 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------