%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SET027-7 : TPTP v9.3.1. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n011.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:38 PM UTC 2026
% Result : Unsatisfiable 10.38s 1.89s
% Output : Proof 10.38s
% Verified :
% Comments :
%------------------------------------------------------------------------------
cnf(t97,axiom,
sF0 = subclass(x,y),
introduced(definition) ).
cnf(f96,negated_conjecture,
subclass(x,y),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_transitivity_of_subclass_1) ).
fof(f96_nnf,plain,
subclass(x,y),
inference(nnf_transformation,[status(thm)],[f96]) ).
cnf(c96,plain,
subclass(x,y),
inference(cnf_transformation,[status(esa)],[f96_nnf]) ).
cnf(t12,plain,
subclass(x,y) = true,
inference(equality_encoding,[status(esa)],[c96]) ).
cnf(t113,plain,
subclass(x,y) = true,
inference(orient,[status(thm)],[t12]) ).
cnf(t1274,plain,
sF0 = true,
inference(step,[status(thm)],[t97,t113]) ).
cnf(t116,plain,
true = sF0,
inference(orient,[status(thm)],[t1274]) ).
cnf(t98,axiom,
sF1 = subclass(x,z),
introduced(definition) ).
cnf(f98,negated_conjecture,
~ subclass(x,z),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_transitivity_of_subclass_3) ).
fof(f98_nnf,plain,
~ subclass(x,z),
inference(nnf_transformation,[status(thm)],[f98]) ).
fof(f98_sk,plain,
~ subclass(x,z),
inference(skolemisation,[status(esa)],[f98_nnf]) ).
cnf(c98,plain,
~ subclass(x,z),
inference(cnf_transformation,[status(esa)],[f98_sk]) ).
cnf(t13,plain,
subclass(x,z) = false,
inference(equality_encoding,[status(esa)],[c98]) ).
cnf(t114,plain,
subclass(x,z) = false,
inference(orient,[status(thm)],[t13]) ).
cnf(t1294,plain,
sF1 = false,
inference(step,[status(thm)],[t98,t114]) ).
cnf(t139,plain,
false = sF1,
inference(orient,[status(thm)],[t1294]) ).
cnf(f2,axiom,
( subclass(X,Y)
| ~ member(not_subclass_element(X,Y),Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_subclass_members2) ).
fof(f2_nnf,plain,
! [X,Y] :
( subclass(X,Y)
| ~ member(not_subclass_element(X,Y),Y) ),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [X,Y] :
( subclass(X,Y)
| ~ member(not_subclass_element(X,Y),Y) ),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
( subclass(X0,X1)
| ~ member(not_subclass_element(X0,X1),X1) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(t46,plain,
ifeq(member(not_subclass_element(X1,X2),X2),true,subclass(X1,X2),true) = true,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t1397,plain,
ifeq(member(not_subclass_element(X1,X2),X2),sF0,subclass(X1,X2),true) = true,
inference(step,[status(thm)],[t46,t116]) ).
cnf(t1398,plain,
ifeq(member(not_subclass_element(X1,X2),X2),sF0,subclass(X1,X2),sF0) = true,
inference(step,[status(thm)],[t1397,t116]) ).
cnf(t1399,plain,
ifeq(member(not_subclass_element(X1,X2),X2),sF0,subclass(X1,X2),sF0) = sF0,
inference(step,[status(thm)],[t1398,t116]) ).
cnf(t332,plain,
ifeq(member(not_subclass_element(X1,X2),X2),sF0,subclass(X1,X2),sF0) = sF0,
inference(orient,[status(thm)],[t1399]) ).
cnf(f0,axiom,
( member(U,Y)
| ~ member(U,X)
| ~ subclass(X,Y) ),
file('/export/starexec/sandbox2/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(t60,plain,
ifeq(subclass(X1,X2),true,ifeq(member(X3,X1),true,member(X3,X2),true),true) = true,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t1548,plain,
ifeq(subclass(X1,X2),sF0,ifeq(member(X3,X1),true,member(X3,X2),true),true) = true,
inference(step,[status(thm)],[t60,t116]) ).
cnf(t1549,plain,
ifeq(subclass(X1,X2),sF0,ifeq(member(X3,X1),sF0,member(X3,X2),true),true) = true,
inference(step,[status(thm)],[t1548,t116]) ).
cnf(t1550,plain,
ifeq(subclass(X1,X2),sF0,ifeq(member(X3,X1),sF0,member(X3,X2),sF0),true) = true,
inference(step,[status(thm)],[t1549,t116]) ).
cnf(t1551,plain,
ifeq(subclass(X1,X2),sF0,ifeq(member(X3,X1),sF0,member(X3,X2),sF0),sF0) = true,
inference(step,[status(thm)],[t1550,t116]) ).
cnf(t1552,plain,
ifeq(subclass(X1,X2),sF0,ifeq(member(X3,X1),sF0,member(X3,X2),sF0),sF0) = sF0,
inference(step,[status(thm)],[t1551,t116]) ).
cnf(t675,plain,
ifeq(subclass(X1,X2),sF0,ifeq(member(X3,X1),sF0,member(X3,X2),sF0),sF0) = sF0,
inference(orient,[status(thm)],[t1552]) ).
cnf(f97,negated_conjecture,
subclass(y,z),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_transitivity_of_subclass_2) ).
fof(f97_nnf,plain,
subclass(y,z),
inference(nnf_transformation,[status(thm)],[f97]) ).
cnf(c97,plain,
subclass(y,z),
inference(cnf_transformation,[status(esa)],[f97_nnf]) ).
cnf(t14,plain,
subclass(y,z) = true,
inference(equality_encoding,[status(esa)],[c97]) ).
cnf(t115,plain,
subclass(y,z) = true,
inference(orient,[status(thm)],[t14]) ).
cnf(t1292,plain,
subclass(y,z) = sF0,
inference(step,[status(thm)],[t115,t116]) ).
cnf(t136,plain,
subclass(y,z) = sF0,
inference(orient,[status(thm)],[t1292]) ).
cnf(t682,plain,
sF0 = ifeq(sF0,sF0,ifeq(member(X1,y),sF0,member(X1,z),sF0),sF0),
inference(cp,[status(thm)],[t675,t136]) ).
cnf(t15,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t150,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t15]) ).
cnf(t1646,plain,
sF0 = ifeq(member(X1,y),sF0,member(X1,z),sF0),
inference(step,[status(thm)],[t682,t150]) ).
cnf(t1174,plain,
ifeq(member(X1,y),sF0,member(X1,z),sF0) = sF0,
inference(orient,[status(thm)],[t1646]) ).
cnf(t1290,plain,
subclass(x,y) = sF0,
inference(step,[status(thm)],[t113,t116]) ).
cnf(t134,plain,
subclass(x,y) = sF0,
inference(orient,[status(thm)],[t1290]) ).
cnf(t680,plain,
sF0 = ifeq(sF0,sF0,ifeq(member(X1,x),sF0,member(X1,y),sF0),sF0),
inference(cp,[status(thm)],[t675,t134]) ).
cnf(t1638,plain,
sF0 = ifeq(member(X1,x),sF0,member(X1,y),sF0),
inference(step,[status(thm)],[t680,t150]) ).
cnf(t1146,plain,
ifeq(member(X1,x),sF0,member(X1,y),sF0) = sF0,
inference(orient,[status(thm)],[t1638]) ).
cnf(f1,axiom,
( subclass(X,Y)
| member(not_subclass_element(X,Y),X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_subclass_members1) ).
fof(f1_nnf,plain,
! [X,Y] :
( subclass(X,Y)
| member(not_subclass_element(X,Y),X) ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [X,Y] :
( subclass(X,Y)
| member(not_subclass_element(X,Y),X) ),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
( subclass(X0,X1)
| member(not_subclass_element(X0,X1),X0) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(t37,plain,
or(member(not_subclass_element(X1,X2),X1),subclass(X1,X2)) = true,
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t1352,plain,
or(member(not_subclass_element(X1,X2),X1),subclass(X1,X2)) = sF0,
inference(step,[status(thm)],[t37,t116]) ).
cnf(t217,plain,
or(member(not_subclass_element(X1,X2),X1),subclass(X1,X2)) = sF0,
inference(orient,[status(thm)],[t1352]) ).
cnf(t1298,plain,
subclass(x,z) = sF1,
inference(step,[status(thm)],[t114,t139]) ).
cnf(t143,plain,
subclass(x,z) = sF1,
inference(orient,[status(thm)],[t1298]) ).
cnf(t218,plain,
sF0 = or(member(not_subclass_element(x,z),x),sF1),
inference(cp,[status(thm)],[t217,t143]) ).
cnf(t6,plain,
or(X1,false) = X1,
introduced(definition) ).
cnf(t107,plain,
or(X1,false) = X1,
inference(orient,[status(thm)],[t6]) ).
cnf(t1296,plain,
or(X1,sF1) = X1,
inference(step,[status(thm)],[t107,t139]) ).
cnf(t141,plain,
or(X1,sF1) = X1,
inference(rw,[status(thm)],[t1296]) ).
cnf(t152,plain,
or(X1,sF1) = X1,
inference(orient,[status(thm)],[t141]) ).
cnf(t1353,plain,
sF0 = member(not_subclass_element(x,z),x),
inference(step,[status(thm)],[t218,t152]) ).
cnf(t220,plain,
member(not_subclass_element(x,z),x) = sF0,
inference(orient,[status(thm)],[t1353]) ).
cnf(t1147,plain,
sF0 = ifeq(sF0,sF0,member(not_subclass_element(x,z),y),sF0),
inference(cp,[status(thm)],[t1146,t220]) ).
cnf(t1639,plain,
sF0 = member(not_subclass_element(x,z),y),
inference(step,[status(thm)],[t1147,t150]) ).
cnf(t1148,plain,
member(not_subclass_element(x,z),y) = sF0,
inference(orient,[status(thm)],[t1639]) ).
cnf(t1175,plain,
sF0 = ifeq(sF0,sF0,member(not_subclass_element(x,z),z),sF0),
inference(cp,[status(thm)],[t1174,t1148]) ).
cnf(t1647,plain,
sF0 = member(not_subclass_element(x,z),z),
inference(step,[status(thm)],[t1175,t150]) ).
cnf(t1182,plain,
member(not_subclass_element(x,z),z) = sF0,
inference(orient,[status(thm)],[t1647]) ).
cnf(t1185,plain,
sF0 = ifeq(sF0,sF0,subclass(x,z),sF0),
inference(cp,[status(thm)],[t332,t1182]) ).
cnf(t1648,plain,
sF0 = subclass(x,z),
inference(step,[status(thm)],[t1185,t150]) ).
cnf(t1649,plain,
sF0 = sF1,
inference(step,[status(thm)],[t1648,t143]) ).
cnf(t1191,plain,
sF1 = sF0,
inference(orient,[status(thm)],[t1649]) ).
cnf(t1654,plain,
false = sF0,
inference(step,[status(thm)],[t139,t1191]) ).
cnf(t1196,plain,
false = sF0,
inference(orient,[status(thm)],[t1654]) ).
cnf(f23,axiom,
( ~ member(Z,X)
| ~ member(Z,complement(X)) ),
file('/export/starexec/sandbox2/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(f29,axiom,
( ~ member(Z,domain_of(X))
| restrict(X,singleton(Z),universal_class) != null_class ),
file('/export/starexec/sandbox2/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,c98]) ).
cnf(g0_0,plain,
sF0 != false,
inference(rw,[status(thm)],[goal_0,t116]) ).
cnf(g0_1,plain,
sF0 != sF0,
inference(rw,[status(thm)],[g0_0,t1196]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SET027-7 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.11/0.36 % Computer : n011.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Thu Sep 24 09:17:42 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.11/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 10.38/1.89 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 10.38/1.89 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------