%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SET011-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n003.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:41:27 PM UTC 2026
% Result : Unsatisfiable 11.78s 7.26s
% Output : Proof 11.78s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 14
% Syntax : Number of formulae : 90 ( 14 unt; 0 def)
% Number of atoms : 243 ( 0 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 241 ( 88 ~; 153 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 5 ( 4 usr; 1 prp; 0-3 aty)
% Number of functors : 7 ( 7 usr; 4 con; 0-3 aty)
% Number of variables : 191 ( 13 sgn 68 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f9,axiom,
( member(h(Set1,Set2,Intersection),Set1)
| intersection(Set1,Set2,Intersection)
| member(h(Set1,Set2,Intersection),Intersection) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intersection_axiom1) ).
fof(f9_nnf,plain,
! [Set1,Set2,Intersection] :
( member(h(Set1,Set2,Intersection),Set1)
| intersection(Set1,Set2,Intersection)
| member(h(Set1,Set2,Intersection),Intersection) ),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [Set1,Set2,Intersection] :
( member(h(Set1,Set2,Intersection),Set1)
| intersection(Set1,Set2,Intersection)
| member(h(Set1,Set2,Intersection),Intersection) ),
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c9,plain,
( member(h(X0,X1,X2),X0)
| intersection(X0,X1,X2)
| member(h(X0,X1,X2),X2) ),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(f12,axiom,
( member(Element,Set1)
| ~ member(Element,Difference)
| ~ difference(Set1,Set2,Difference) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',member_of_difference) ).
fof(f12_nnf,plain,
! [Set1,Set2,Difference,Element] :
( member(Element,Set1)
| ~ member(Element,Difference)
| ~ difference(Set1,Set2,Difference) ),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [Set1,Set2,Difference,Element] :
( member(Element,Set1)
| ~ member(Element,Difference)
| ~ difference(Set1,Set2,Difference) ),
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c12,plain,
( member(X3,X0)
| ~ member(X3,X2)
| ~ difference(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(f19,hypothesis,
difference(a,aDb,aD_aDb),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a_minus_aDb) ).
fof(f19_nnf,plain,
difference(a,aDb,aD_aDb),
inference(nnf_transformation,[status(thm)],[f19]) ).
cnf(c19,plain,
difference(a,aDb,aD_aDb),
inference(cnf_transformation,[status(esa)],[f19_nnf]) ).
cnf(p27,plain,
( member(X0,a)
| ~ member(X0,aD_aDb) ),
inference(resolution,[status(thm)],[c12,c19]) ).
cnf(p42,plain,
( member(h(X0,X1,aD_aDb),a)
| member(h(X0,X1,aD_aDb),X0)
| intersection(X0,X1,aD_aDb) ),
inference(resolution,[status(thm)],[c9,p27]) ).
cnf(p199,plain,
( member(h(a,X0,aD_aDb),a)
| intersection(a,X0,aD_aDb) ),
inference(factoring,[status(thm)],[p42]) ).
cnf(f14,axiom,
( member(Element,Set2)
| member(Element,Difference)
| ~ difference(Set1,Set2,Difference)
| ~ member(Element,Set1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',member_of_difference_or_set2) ).
fof(f14_nnf,plain,
! [Element,Set1,Set2,Difference] :
( member(Element,Set2)
| member(Element,Difference)
| ~ difference(Set1,Set2,Difference)
| ~ member(Element,Set1) ),
inference(nnf_transformation,[status(thm)],[f14]) ).
fof(f14_sk,plain,
! [Element,Set1,Set2,Difference] :
( member(Element,Set2)
| member(Element,Difference)
| ~ difference(Set1,Set2,Difference)
| ~ member(Element,Set1) ),
inference(skolemisation,[status(esa)],[f14_nnf]) ).
cnf(c14,plain,
( member(X0,X2)
| member(X0,X3)
| ~ difference(X1,X2,X3)
| ~ member(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(p213,plain,
( member(h(a,X0,aD_aDb),X1)
| member(h(a,X0,aD_aDb),X2)
| ~ difference(a,X1,X2)
| intersection(a,X0,aD_aDb) ),
inference(resolution,[status(thm)],[p199,c14]) ).
cnf(p735,plain,
( member(h(a,X0,aD_aDb),aDb)
| member(h(a,X0,aD_aDb),aD_aDb)
| intersection(a,X0,aD_aDb) ),
inference(resolution,[status(thm)],[p213,c19]) ).
cnf(f11,axiom,
( intersection(Set1,Set2,Intersection)
| ~ member(h(Set1,Set2,Intersection),Set1)
| ~ member(h(Set1,Set2,Intersection),Set2)
| ~ member(h(Set1,Set2,Intersection),Intersection) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intersection_axiom3) ).
fof(f11_nnf,plain,
! [Set1,Set2,Intersection] :
( intersection(Set1,Set2,Intersection)
| ~ member(h(Set1,Set2,Intersection),Set1)
| ~ member(h(Set1,Set2,Intersection),Set2)
| ~ member(h(Set1,Set2,Intersection),Intersection) ),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [Set1,Set2,Intersection] :
( intersection(Set1,Set2,Intersection)
| ~ member(h(Set1,Set2,Intersection),Set1)
| ~ member(h(Set1,Set2,Intersection),Set2)
| ~ member(h(Set1,Set2,Intersection),Intersection) ),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c11,plain,
( intersection(X0,X1,X2)
| ~ member(h(X0,X1,X2),X0)
| ~ member(h(X0,X1,X2),X1)
| ~ member(h(X0,X1,X2),X2) ),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(p1281,plain,
( intersection(a,X0,aD_aDb)
| ~ member(h(a,X0,aD_aDb),a)
| ~ member(h(a,X0,aD_aDb),X0)
| member(h(a,X0,aD_aDb),aDb)
| intersection(a,X0,aD_aDb) ),
inference(resolution,[status(thm)],[p735,c11]) ).
cnf(p2293,plain,
( ~ member(h(a,X0,aD_aDb),a)
| ~ member(h(a,X0,aD_aDb),X0)
| member(h(a,X0,aD_aDb),aDb)
| intersection(a,X0,aD_aDb) ),
inference(factoring,[status(thm)],[p1281]) ).
cnf(f1,axiom,
( member(member_of_1_not_of_2(Subset,Superset),Subset)
| subset(Subset,Superset) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',subsets_axiom1) ).
fof(f1_nnf,plain,
! [Subset,Superset] :
( member(member_of_1_not_of_2(Subset,Superset),Subset)
| subset(Subset,Superset) ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [Subset,Superset] :
( member(member_of_1_not_of_2(Subset,Superset),Subset)
| subset(Subset,Superset) ),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
( member(member_of_1_not_of_2(X0,X1),X0)
| subset(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p29,plain,
( subset(aD_aDb,X0)
| member(member_of_1_not_of_2(aD_aDb,X0),a) ),
inference(resolution,[status(thm)],[p27,c1]) ).
cnf(p96,plain,
( subset(aD_aDb,X2)
| member(member_of_1_not_of_2(aD_aDb,X2),X0)
| member(member_of_1_not_of_2(aD_aDb,X2),X1)
| ~ difference(a,X0,X1) ),
inference(resolution,[status(thm)],[c14,p29]) ).
cnf(f18,hypothesis,
difference(a,b,aDb),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a_minus_b) ).
fof(f18_nnf,plain,
difference(a,b,aDb),
inference(nnf_transformation,[status(thm)],[f18]) ).
cnf(c18,plain,
difference(a,b,aDb),
inference(cnf_transformation,[status(esa)],[f18_nnf]) ).
cnf(p377,plain,
( subset(aD_aDb,X0)
| member(member_of_1_not_of_2(aD_aDb,X0),b)
| member(member_of_1_not_of_2(aD_aDb,X0),aDb) ),
inference(resolution,[status(thm)],[p96,c18]) ).
cnf(f13,axiom,
( ~ difference(A_set,Set1,Set2)
| ~ member(Element,Set2)
| ~ member(Element,Set1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not_member_of_difference) ).
fof(f13_nnf,plain,
! [Element,Set1,Set2,A_set] :
( ~ difference(A_set,Set1,Set2)
| ~ member(Element,Set2)
| ~ member(Element,Set1) ),
inference(nnf_transformation,[status(thm)],[f13]) ).
fof(f13_sk,plain,
! [Element,Set1,Set2,A_set] :
( ~ difference(A_set,Set1,Set2)
| ~ member(Element,Set2)
| ~ member(Element,Set1) ),
inference(skolemisation,[status(esa)],[f13_nnf]) ).
cnf(c13,plain,
( ~ difference(X3,X1,X2)
| ~ member(X0,X2)
| ~ member(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(p67,plain,
( subset(X0,X1)
| ~ difference(X3,X0,X2)
| ~ member(member_of_1_not_of_2(X0,X1),X2) ),
inference(resolution,[status(thm)],[c13,c1]) ).
cnf(p423,plain,
( subset(aD_aDb,X0)
| ~ difference(X1,aD_aDb,aDb)
| subset(aD_aDb,X0)
| member(member_of_1_not_of_2(aD_aDb,X0),b) ),
inference(resolution,[status(thm)],[p377,p67]) ).
cnf(p799,plain,
( ~ difference(X1,aD_aDb,aDb)
| subset(aD_aDb,X0)
| member(member_of_1_not_of_2(aD_aDb,X0),b) ),
inference(factoring,[status(thm)],[p423]) ).
cnf(f17,axiom,
( difference(Set1,Set2,Difference)
| member(k(Set1,Set2,Difference),Set2)
| ~ member(k(Set1,Set2,Difference),Set1)
| ~ member(k(Set1,Set2,Difference),Difference) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',difference_axiom3) ).
fof(f17_nnf,plain,
! [Set1,Set2,Difference] :
( difference(Set1,Set2,Difference)
| member(k(Set1,Set2,Difference),Set2)
| ~ member(k(Set1,Set2,Difference),Set1)
| ~ member(k(Set1,Set2,Difference),Difference) ),
inference(nnf_transformation,[status(thm)],[f17]) ).
fof(f17_sk,plain,
! [Set1,Set2,Difference] :
( difference(Set1,Set2,Difference)
| member(k(Set1,Set2,Difference),Set2)
| ~ member(k(Set1,Set2,Difference),Set1)
| ~ member(k(Set1,Set2,Difference),Difference) ),
inference(skolemisation,[status(esa)],[f17_nnf]) ).
cnf(c17,plain,
( difference(X0,X1,X2)
| member(k(X0,X1,X2),X1)
| ~ member(k(X0,X1,X2),X0)
| ~ member(k(X0,X1,X2),X2) ),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(p131,plain,
( difference(X0,X1,X0)
| member(k(X0,X1,X0),X1)
| ~ member(k(X0,X1,X0),X0) ),
inference(factoring,[status(thm)],[c17]) ).
cnf(f15,axiom,
( member(k(Set1,Set2,Difference),Difference)
| member(k(Set1,Set2,Difference),Set1)
| difference(Set1,Set2,Difference) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',difference_axiom2) ).
fof(f15_nnf,plain,
! [Set1,Set2,Difference] :
( member(k(Set1,Set2,Difference),Difference)
| member(k(Set1,Set2,Difference),Set1)
| difference(Set1,Set2,Difference) ),
inference(nnf_transformation,[status(thm)],[f15]) ).
fof(f15_sk,plain,
! [Set1,Set2,Difference] :
( member(k(Set1,Set2,Difference),Difference)
| member(k(Set1,Set2,Difference),Set1)
| difference(Set1,Set2,Difference) ),
inference(skolemisation,[status(esa)],[f15_nnf]) ).
cnf(c15,plain,
( member(k(X0,X1,X2),X2)
| member(k(X0,X1,X2),X0)
| difference(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f15_sk]) ).
cnf(p107,plain,
( member(k(X0,X1,X0),X0)
| difference(X0,X1,X0) ),
inference(factoring,[status(thm)],[c15]) ).
cnf(p547,plain,
( difference(X0,X1,X0)
| difference(X0,X1,X0)
| member(k(X0,X1,X0),X1) ),
inference(resolution,[status(thm)],[p131,p107]) ).
cnf(p610,plain,
( difference(X0,X1,X0)
| member(k(X0,X1,X0),X1) ),
inference(factoring,[status(thm)],[p547]) ).
cnf(p124,plain,
( ~ difference(X3,X0,X2)
| ~ member(k(X0,X1,X0),X2)
| difference(X0,X1,X0) ),
inference(resolution,[status(thm)],[p107,c13]) ).
cnf(p618,plain,
( ~ difference(X2,X0,X1)
| difference(X0,X1,X0)
| difference(X0,X1,X0) ),
inference(resolution,[status(thm)],[p610,p124]) ).
cnf(p634,plain,
( ~ difference(X2,X0,X1)
| difference(X0,X1,X0) ),
inference(factoring,[status(thm)],[p618]) ).
cnf(p637,plain,
difference(aDb,aD_aDb,aDb),
inference(resolution,[status(thm)],[p634,c19]) ).
cnf(p802,plain,
( subset(aD_aDb,X0)
| member(member_of_1_not_of_2(aD_aDb,X0),b) ),
inference(resolution,[status(thm)],[p799,p637]) ).
cnf(f2,axiom,
( subset(Subset,Superset)
| ~ member(member_of_1_not_of_2(Subset,Superset),Superset) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',subsets_axiom2) ).
fof(f2_nnf,plain,
! [Subset,Superset] :
( subset(Subset,Superset)
| ~ member(member_of_1_not_of_2(Subset,Superset),Superset) ),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [Subset,Superset] :
( subset(Subset,Superset)
| ~ member(member_of_1_not_of_2(Subset,Superset),Superset) ),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
( subset(X0,X1)
| ~ member(member_of_1_not_of_2(X0,X1),X1) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p804,plain,
( subset(aD_aDb,b)
| subset(aD_aDb,b) ),
inference(resolution,[status(thm)],[p802,c2]) ).
cnf(p811,plain,
subset(aD_aDb,b),
inference(factoring,[status(thm)],[p804]) ).
cnf(f10,axiom,
( member(h(Set1,Set2,Intersection),Set2)
| intersection(Set1,Set2,Intersection)
| member(h(Set1,Set2,Intersection),Intersection) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intersection_axiom2) ).
fof(f10_nnf,plain,
! [Set1,Set2,Intersection] :
( member(h(Set1,Set2,Intersection),Set2)
| intersection(Set1,Set2,Intersection)
| member(h(Set1,Set2,Intersection),Intersection) ),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [Set1,Set2,Intersection] :
( member(h(Set1,Set2,Intersection),Set2)
| intersection(Set1,Set2,Intersection)
| member(h(Set1,Set2,Intersection),Intersection) ),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c10,plain,
( member(h(X0,X1,X2),X1)
| intersection(X0,X1,X2)
| member(h(X0,X1,X2),X2) ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(f0,axiom,
( member(Element,Superset)
| ~ subset(Subset,Superset)
| ~ member(Element,Subset) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',membership_in_subsets) ).
fof(f0_nnf,plain,
! [Element,Subset,Superset] :
( member(Element,Superset)
| ~ subset(Subset,Superset)
| ~ member(Element,Subset) ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [Element,Subset,Superset] :
( member(Element,Superset)
| ~ subset(Subset,Superset)
| ~ member(Element,Subset) ),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
( member(X0,X2)
| ~ subset(X1,X2)
| ~ member(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p50,plain,
( member(h(X0,X1,X2),X3)
| ~ subset(X2,X3)
| member(h(X0,X1,X2),X1)
| intersection(X0,X1,X2) ),
inference(resolution,[status(thm)],[c10,c0]) ).
cnf(p232,plain,
( ~ subset(X2,X1)
| member(h(X0,X1,X2),X1)
| intersection(X0,X1,X2) ),
inference(factoring,[status(thm)],[p50]) ).
cnf(p822,plain,
( member(h(X0,b,aD_aDb),b)
| intersection(X0,b,aD_aDb) ),
inference(resolution,[status(thm)],[p811,p232]) ).
cnf(p2974,plain,
( intersection(a,b,aD_aDb)
| ~ member(h(a,b,aD_aDb),a)
| member(h(a,b,aD_aDb),aDb)
| intersection(a,b,aD_aDb) ),
inference(resolution,[status(thm)],[p2293,p822]) ).
cnf(p2976,plain,
( ~ member(h(a,b,aD_aDb),a)
| member(h(a,b,aD_aDb),aDb)
| intersection(a,b,aD_aDb) ),
inference(factoring,[status(thm)],[p2974]) ).
cnf(p2977,plain,
( intersection(a,b,aD_aDb)
| member(h(a,b,aD_aDb),aDb)
| intersection(a,b,aD_aDb) ),
inference(resolution,[status(thm)],[p2976,p199]) ).
cnf(p2978,plain,
( member(h(a,b,aD_aDb),aDb)
| intersection(a,b,aD_aDb) ),
inference(factoring,[status(thm)],[p2977]) ).
cnf(p883,plain,
( ~ difference(X2,b,X1)
| ~ member(h(X0,b,aD_aDb),X1)
| intersection(X0,b,aD_aDb) ),
inference(resolution,[status(thm)],[p822,c13]) ).
cnf(p2987,plain,
( ~ difference(X0,b,aDb)
| intersection(a,b,aD_aDb)
| intersection(a,b,aD_aDb) ),
inference(resolution,[status(thm)],[p2978,p883]) ).
cnf(p2993,plain,
( ~ difference(X0,b,aDb)
| intersection(a,b,aD_aDb) ),
inference(factoring,[status(thm)],[p2987]) ).
cnf(p2998,plain,
intersection(a,b,aD_aDb),
inference(resolution,[status(thm)],[p2993,c18]) ).
cnf(f20,negated_conjecture,
~ intersection(a,b,aD_aDb),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_a_intersection_b_is_aD_aDb) ).
fof(f20_nnf,plain,
~ intersection(a,b,aD_aDb),
inference(nnf_transformation,[status(thm)],[f20]) ).
fof(f20_sk,plain,
~ intersection(a,b,aD_aDb),
inference(skolemisation,[status(esa)],[f20_nnf]) ).
cnf(c20,plain,
~ intersection(a,b,aD_aDb),
inference(cnf_transformation,[status(esa)],[f20_sk]) ).
cnf(p2999,plain,
$false,
inference(resolution,[status(thm)],[p2998,c20]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET011-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.11/5.38 % Computer : n003.cluster.edu
% 0.11/5.38 % Model : x86_64 x86_64
% 0.11/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.38 % Memory : 8046.5625MB
% 0.11/5.38 % OS : Linux 6.8.0-71-generic
% 0.11/5.38 % CPULimit : 300
% 0.11/5.38 % WCLimit : 300
% 0.11/5.38 % DateTime : Thu Sep 24 09:06:56 UTC 2026
% 0.11/5.38 % CPUTime :
% 0.11/5.38 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 11.78/7.26 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 11.78/7.26 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------