%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SET187-6 : TPTP v9.3.1. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n007.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:42:46 PM UTC 2026
% Result : Unsatisfiable 6.76s 6.49s
% Output : Proof 6.76s
% Verified :
% Comments :
%------------------------------------------------------------------------------
cnf(t109,axiom,
sF0 = subclass(x,y),
introduced(definition) ).
cnf(f112,negated_conjecture,
subclass(x,y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_subclass_property5_1) ).
fof(f112_nnf,plain,
subclass(x,y),
inference(nnf_transformation,[status(thm)],[f112]) ).
cnf(c112,plain,
subclass(x,y),
inference(cnf_transformation,[status(esa)],[f112_nnf]) ).
cnf(t11,plain,
subclass(x,y) = true,
inference(equality_encoding,[status(esa)],[c112]) ).
cnf(t126,plain,
subclass(x,y) = true,
inference(orient,[status(thm)],[t11]) ).
cnf(t1484,plain,
sF0 = true,
inference(step,[status(thm)],[t109,t126]) ).
cnf(t127,plain,
true = sF0,
inference(orient,[status(thm)],[t1484]) ).
cnf(t112,axiom,
sF3 = eq(intersection(complement(y),x),null_class),
introduced(definition) ).
cnf(t110,axiom,
sF1 = complement(y),
introduced(definition) ).
cnf(t118,plain,
complement(y) = sF1,
inference(orient,[status(thm)],[t110]) ).
cnf(t1511,plain,
sF3 = eq(intersection(sF1,x),null_class),
inference(step,[status(thm)],[t112,t118]) ).
cnf(t111,axiom,
sF2 = intersection(complement(y),x),
introduced(definition) ).
cnf(t1502,plain,
sF2 = intersection(sF1,x),
inference(step,[status(thm)],[t111,t118]) ).
cnf(t148,plain,
intersection(sF1,x) = sF2,
inference(orient,[status(thm)],[t1502]) ).
cnf(t1512,plain,
sF3 = eq(sF2,null_class),
inference(step,[status(thm)],[t1511,t148]) ).
cnf(f113,negated_conjecture,
intersection(complement(y),x) != null_class,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_subclass_property5_2) ).
fof(f113_nnf,plain,
intersection(complement(y),x) != null_class,
inference(nnf_transformation,[status(thm)],[f113]) ).
fof(f113_sk,plain,
intersection(complement(y),x) != null_class,
inference(skolemisation,[status(esa)],[f113_nnf]) ).
cnf(c113,plain,
intersection(complement(y),x) != null_class,
inference(cnf_transformation,[status(esa)],[f113_sk]) ).
cnf(t17,plain,
eq(intersection(complement(y),x),null_class) = false,
inference(equality_encoding,[status(esa)],[c113]) ).
cnf(t1507,plain,
eq(intersection(sF1,x),null_class) = false,
inference(step,[status(thm)],[t17,t118]) ).
cnf(t1508,plain,
eq(sF2,null_class) = false,
inference(step,[status(thm)],[t1507,t148]) ).
cnf(t154,plain,
eq(sF2,null_class) = false,
inference(orient,[status(thm)],[t1508]) ).
cnf(t1513,plain,
sF3 = false,
inference(step,[status(thm)],[t1512,t154]) ).
cnf(t159,plain,
false = sF3,
inference(orient,[status(thm)],[t1513]) ).
cnf(f0,axiom,
( member(U,Y)
| ~ member(U,X)
| ~ subclass(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',subclass_members) ).
fof(f0_nnf,plain,
! [X,Y,U] :
( member(U,Y)
| ~ member(U,X)
| ~ subclass(X,Y) ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [X,Y,U] :
( member(U,Y)
| ~ member(U,X)
| ~ subclass(X,Y) ),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
( member(X2,X1)
| ~ member(X2,X0)
| ~ subclass(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t66,plain,
ifeq(subclass(X1,X2),true,ifeq(member(X3,X1),true,member(X3,X2),true),true) = true,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t1786,plain,
ifeq(subclass(X1,X2),sF0,ifeq(member(X3,X1),true,member(X3,X2),true),true) = true,
inference(step,[status(thm)],[t66,t127]) ).
cnf(t1787,plain,
ifeq(subclass(X1,X2),sF0,ifeq(member(X3,X1),sF0,member(X3,X2),true),true) = true,
inference(step,[status(thm)],[t1786,t127]) ).
cnf(t1788,plain,
ifeq(subclass(X1,X2),sF0,ifeq(member(X3,X1),sF0,member(X3,X2),sF0),true) = true,
inference(step,[status(thm)],[t1787,t127]) ).
cnf(t1789,plain,
ifeq(subclass(X1,X2),sF0,ifeq(member(X3,X1),sF0,member(X3,X2),sF0),sF0) = true,
inference(step,[status(thm)],[t1788,t127]) ).
cnf(t1790,plain,
ifeq(subclass(X1,X2),sF0,ifeq(member(X3,X1),sF0,member(X3,X2),sF0),sF0) = sF0,
inference(step,[status(thm)],[t1789,t127]) ).
cnf(t813,plain,
ifeq(subclass(X1,X2),sF0,ifeq(member(X3,X1),sF0,member(X3,X2),sF0),sF0) = sF0,
inference(orient,[status(thm)],[t1790]) ).
cnf(t1498,plain,
subclass(x,y) = sF0,
inference(step,[status(thm)],[t126,t127]) ).
cnf(t143,plain,
subclass(x,y) = sF0,
inference(orient,[status(thm)],[t1498]) ).
cnf(t817,plain,
sF0 = ifeq(sF0,sF0,ifeq(member(X1,x),sF0,member(X1,y),sF0),sF0),
inference(cp,[status(thm)],[t813,t143]) ).
cnf(t12,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t149,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t12]) ).
cnf(t1905,plain,
sF0 = ifeq(member(X1,x),sF0,member(X1,y),sF0),
inference(step,[status(thm)],[t817,t149]) ).
cnf(t1384,plain,
ifeq(member(X1,x),sF0,member(X1,y),sF0) = sF0,
inference(orient,[status(thm)],[t1905]) ).
cnf(t18,plain,
ifeq(not(X1),true,X1,false) = false,
introduced(definition) ).
cnf(t1509,plain,
ifeq(not(X1),sF0,X1,false) = false,
inference(step,[status(thm)],[t18,t127]) ).
cnf(t155,plain,
ifeq(not(X1),sF0,X1,false) = false,
inference(orient,[status(thm)],[t1509]) ).
cnf(t167,plain,
ifeq(not(X1),sF0,X1,sF3) = false,
inference(rw,[status(thm)],[t155]) ).
cnf(t1524,plain,
ifeq(not(X1),sF0,X1,sF3) = sF3,
inference(step,[status(thm)],[t167,t159]) ).
cnf(t184,plain,
ifeq(not(X1),sF0,X1,sF3) = sF3,
inference(orient,[status(thm)],[t1524]) ).
cnf(f23,axiom,
( ~ member(Z,X)
| ~ member(Z,complement(X)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',complement1) ).
fof(f23_nnf,plain,
! [Z,X] :
( ~ member(Z,X)
| ~ member(Z,complement(X)) ),
inference(nnf_transformation,[status(thm)],[f23]) ).
fof(f23_sk,plain,
! [Z,X] :
( ~ member(Z,X)
| ~ member(Z,complement(X)) ),
inference(skolemisation,[status(esa)],[f23_nnf]) ).
cnf(c23,plain,
( ~ member(X0,X1)
| ~ member(X0,complement(X1)) ),
inference(cnf_transformation,[status(esa)],[f23_sk]) ).
cnf(t45,plain,
or(not(member(X1,complement(X2))),not(member(X1,X2))) = true,
inference(equality_encoding,[status(esa)],[c23]) ).
cnf(t1579,plain,
or(not(member(X1,complement(X2))),not(member(X1,X2))) = sF0,
inference(step,[status(thm)],[t45,t127]) ).
cnf(t282,plain,
or(not(member(X1,complement(X2))),not(member(X1,X2))) = sF0,
inference(orient,[status(thm)],[t1579]) ).
cnf(t283,plain,
sF0 = or(not(member(X1,sF1)),not(member(X1,y))),
inference(cp,[status(thm)],[t282,t118]) ).
cnf(t307,plain,
or(not(member(X1,sF1)),not(member(X1,y))) = sF0,
inference(orient,[status(thm)],[t283]) ).
cnf(f20,axiom,
( member(Z,X)
| ~ member(Z,intersection(X,Y)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intersection1) ).
fof(f20_nnf,plain,
! [Z,X,Y] :
( member(Z,X)
| ~ member(Z,intersection(X,Y)) ),
inference(nnf_transformation,[status(thm)],[f20]) ).
fof(f20_sk,plain,
! [Z,X,Y] :
( member(Z,X)
| ~ member(Z,intersection(X,Y)) ),
inference(skolemisation,[status(esa)],[f20_nnf]) ).
cnf(c20,plain,
( member(X0,X1)
| ~ member(X0,intersection(X1,X2)) ),
inference(cnf_transformation,[status(esa)],[f20_sk]) ).
cnf(t47,plain,
ifeq(member(X1,intersection(X2,X3)),true,member(X1,X2),true) = true,
inference(equality_encoding,[status(esa)],[c20]) ).
cnf(t1595,plain,
ifeq(member(X1,intersection(X2,X3)),sF0,member(X1,X2),true) = true,
inference(step,[status(thm)],[t47,t127]) ).
cnf(t1596,plain,
ifeq(member(X1,intersection(X2,X3)),sF0,member(X1,X2),sF0) = true,
inference(step,[status(thm)],[t1595,t127]) ).
cnf(t1597,plain,
ifeq(member(X1,intersection(X2,X3)),sF0,member(X1,X2),sF0) = sF0,
inference(step,[status(thm)],[t1596,t127]) ).
cnf(t312,plain,
ifeq(member(X1,intersection(X2,X3)),sF0,member(X1,X2),sF0) = sF0,
inference(orient,[status(thm)],[t1597]) ).
cnf(t314,plain,
sF0 = ifeq(member(X1,sF2),sF0,member(X1,sF1),sF0),
inference(cp,[status(thm)],[t312,t148]) ).
cnf(t340,plain,
ifeq(member(X1,sF2),sF0,member(X1,sF1),sF0) = sF0,
inference(orient,[status(thm)],[t314]) ).
cnf(f65,axiom,
( member(regular(X),X)
| X = null_class ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',regularity1) ).
fof(f65_nnf,plain,
! [X] :
( member(regular(X),X)
| X = null_class ),
inference(nnf_transformation,[status(thm)],[f65]) ).
fof(f65_sk,plain,
! [X] :
( member(regular(X),X)
| X = null_class ),
inference(skolemisation,[status(esa)],[f65_nnf]) ).
cnf(c65,plain,
( member(regular(X0),X0)
| X0 = null_class ),
inference(cnf_transformation,[status(esa)],[f65_sk]) ).
cnf(t33,plain,
or(eq(X1,null_class),member(regular(X1),X1)) = true,
inference(equality_encoding,[status(esa)],[c65]) ).
cnf(t1549,plain,
or(eq(X1,null_class),member(regular(X1),X1)) = sF0,
inference(step,[status(thm)],[t33,t127]) ).
cnf(t227,plain,
or(eq(X1,null_class),member(regular(X1),X1)) = sF0,
inference(orient,[status(thm)],[t1549]) ).
cnf(t1519,plain,
eq(sF2,null_class) = sF3,
inference(step,[status(thm)],[t154,t159]) ).
cnf(t165,plain,
eq(sF2,null_class) = sF3,
inference(orient,[status(thm)],[t1519]) ).
cnf(t228,plain,
sF0 = or(sF3,member(regular(sF2),sF2)),
inference(cp,[status(thm)],[t227,t165]) ).
cnf(t8,plain,
or(false,X1) = X1,
introduced(definition) ).
cnf(t123,plain,
or(false,X1) = X1,
inference(orient,[status(thm)],[t8]) ).
cnf(t1516,plain,
or(sF3,X1) = X1,
inference(step,[status(thm)],[t123,t159]) ).
cnf(t162,plain,
or(sF3,X1) = X1,
inference(rw,[status(thm)],[t1516]) ).
cnf(t171,plain,
or(sF3,X1) = X1,
inference(orient,[status(thm)],[t162]) ).
cnf(t1550,plain,
sF0 = member(regular(sF2),sF2),
inference(step,[status(thm)],[t228,t171]) ).
cnf(t229,plain,
member(regular(sF2),sF2) = sF0,
inference(orient,[status(thm)],[t1550]) ).
cnf(t341,plain,
sF0 = ifeq(sF0,sF0,member(regular(sF2),sF1),sF0),
inference(cp,[status(thm)],[t340,t229]) ).
cnf(t1601,plain,
sF0 = member(regular(sF2),sF1),
inference(step,[status(thm)],[t341,t149]) ).
cnf(t342,plain,
member(regular(sF2),sF1) = sF0,
inference(orient,[status(thm)],[t1601]) ).
cnf(t344,plain,
sF0 = or(not(sF0),not(member(regular(sF2),y))),
inference(cp,[status(thm)],[t307,t342]) ).
cnf(t3,plain,
not(true) = false,
introduced(definition) ).
cnf(t117,plain,
not(true) = false,
inference(orient,[status(thm)],[t3]) ).
cnf(t1491,plain,
not(sF0) = false,
inference(step,[status(thm)],[t117,t127]) ).
cnf(t134,plain,
not(sF0) = false,
inference(rw,[status(thm)],[t1491]) ).
cnf(t145,plain,
not(sF0) = false,
inference(orient,[status(thm)],[t134]) ).
cnf(t1517,plain,
not(sF0) = sF3,
inference(step,[status(thm)],[t145,t159]) ).
cnf(t163,plain,
not(sF0) = sF3,
inference(orient,[status(thm)],[t1517]) ).
cnf(t1602,plain,
sF0 = or(sF3,not(member(regular(sF2),y))),
inference(step,[status(thm)],[t344,t163]) ).
cnf(t1603,plain,
sF0 = not(member(regular(sF2),y)),
inference(step,[status(thm)],[t1602,t171]) ).
cnf(t347,plain,
not(member(regular(sF2),y)) = sF0,
inference(orient,[status(thm)],[t1603]) ).
cnf(t348,plain,
sF3 = ifeq(sF0,sF0,member(regular(sF2),y),sF3),
inference(cp,[status(thm)],[t184,t347]) ).
cnf(t1604,plain,
sF3 = member(regular(sF2),y),
inference(step,[status(thm)],[t348,t149]) ).
cnf(t349,plain,
member(regular(sF2),y) = sF3,
inference(orient,[status(thm)],[t1604]) ).
cnf(t1385,plain,
sF0 = ifeq(member(regular(sF2),x),sF0,sF3,sF0),
inference(cp,[status(thm)],[t1384,t349]) ).
cnf(f21,axiom,
( member(Z,Y)
| ~ member(Z,intersection(X,Y)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intersection2) ).
fof(f21_nnf,plain,
! [Z,X,Y] :
( member(Z,Y)
| ~ member(Z,intersection(X,Y)) ),
inference(nnf_transformation,[status(thm)],[f21]) ).
fof(f21_sk,plain,
! [Z,X,Y] :
( member(Z,Y)
| ~ member(Z,intersection(X,Y)) ),
inference(skolemisation,[status(esa)],[f21_nnf]) ).
cnf(c21,plain,
( member(X0,X2)
| ~ member(X0,intersection(X1,X2)) ),
inference(cnf_transformation,[status(esa)],[f21_sk]) ).
cnf(t48,plain,
ifeq(member(X1,intersection(X2,X3)),true,member(X1,X3),true) = true,
inference(equality_encoding,[status(esa)],[c21]) ).
cnf(t1598,plain,
ifeq(member(X1,intersection(X2,X3)),sF0,member(X1,X3),true) = true,
inference(step,[status(thm)],[t48,t127]) ).
cnf(t1599,plain,
ifeq(member(X1,intersection(X2,X3)),sF0,member(X1,X3),sF0) = true,
inference(step,[status(thm)],[t1598,t127]) ).
cnf(t1600,plain,
ifeq(member(X1,intersection(X2,X3)),sF0,member(X1,X3),sF0) = sF0,
inference(step,[status(thm)],[t1599,t127]) ).
cnf(t327,plain,
ifeq(member(X1,intersection(X2,X3)),sF0,member(X1,X3),sF0) = sF0,
inference(orient,[status(thm)],[t1600]) ).
cnf(t329,plain,
sF0 = ifeq(member(X1,sF2),sF0,member(X1,x),sF0),
inference(cp,[status(thm)],[t327,t148]) ).
cnf(t377,plain,
ifeq(member(X1,sF2),sF0,member(X1,x),sF0) = sF0,
inference(orient,[status(thm)],[t329]) ).
cnf(t378,plain,
sF0 = ifeq(sF0,sF0,member(regular(sF2),x),sF0),
inference(cp,[status(thm)],[t377,t229]) ).
cnf(t1615,plain,
sF0 = member(regular(sF2),x),
inference(step,[status(thm)],[t378,t149]) ).
cnf(t379,plain,
member(regular(sF2),x) = sF0,
inference(orient,[status(thm)],[t1615]) ).
cnf(t1906,plain,
sF0 = ifeq(sF0,sF0,sF3,sF0),
inference(step,[status(thm)],[t1385,t379]) ).
cnf(t1907,plain,
sF0 = sF3,
inference(step,[status(thm)],[t1906,t149]) ).
cnf(t1386,plain,
sF3 = sF0,
inference(orient,[status(thm)],[t1907]) ).
cnf(t1912,plain,
false = sF0,
inference(step,[status(thm)],[t159,t1386]) ).
cnf(t1391,plain,
false = sF0,
inference(orient,[status(thm)],[t1912]) ).
cnf(f29,axiom,
( ~ member(Z,domain_of(X))
| restrict(X,singleton(Z),universal_class) != null_class ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',domain1) ).
fof(f29_nnf,plain,
! [X,Z] :
( ~ member(Z,domain_of(X))
| restrict(X,singleton(Z),universal_class) != null_class ),
inference(nnf_transformation,[status(thm)],[f29]) ).
fof(f29_sk,plain,
! [X,Z] :
( ~ member(Z,domain_of(X))
| restrict(X,singleton(Z),universal_class) != null_class ),
inference(skolemisation,[status(esa)],[f29_nnf]) ).
cnf(c29,plain,
( ~ member(X1,domain_of(X0))
| restrict(X0,singleton(X1),universal_class) != null_class ),
inference(cnf_transformation,[status(esa)],[f29_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c23,c29,c113]) ).
cnf(g0_0,plain,
sF0 != false,
inference(rw,[status(thm)],[goal_0,t127]) ).
cnf(g0_1,plain,
sF0 != sF0,
inference(rw,[status(thm)],[g0_0,t1391]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET187-6 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.11/5.38 % Computer : n007.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 10:09:12 UTC 2026
% 0.11/5.38 % CPUTime :
% 0.11/5.38 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 6.76/6.49 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.76/6.49 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------