%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SET027-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 : n020.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:36 PM UTC 2026
% Result : Unsatisfiable 3.30s 0.89s
% Output : Proof 3.30s
% Verified :
% Comments :
%------------------------------------------------------------------------------
cnf(t92,axiom,
sF0 = subclass(x,y),
introduced(definition) ).
cnf(f91,negated_conjecture,
subclass(x,y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_transitivity_of_subclass_1) ).
fof(f91_nnf,plain,
subclass(x,y),
inference(nnf_transformation,[status(thm)],[f91]) ).
cnf(c91,plain,
subclass(x,y),
inference(cnf_transformation,[status(esa)],[f91_nnf]) ).
cnf(t11,plain,
subclass(x,y) = true,
inference(equality_encoding,[status(esa)],[c91]) ).
cnf(t107,plain,
subclass(x,y) = true,
inference(orient,[status(thm)],[t11]) ).
cnf(t1267,plain,
sF0 = true,
inference(step,[status(thm)],[t92,t107]) ).
cnf(t110,plain,
true = sF0,
inference(orient,[status(thm)],[t1267]) ).
cnf(t93,axiom,
sF1 = subclass(x,z),
introduced(definition) ).
cnf(f93,negated_conjecture,
~ subclass(x,z),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_transitivity_of_subclass_3) ).
fof(f93_nnf,plain,
~ subclass(x,z),
inference(nnf_transformation,[status(thm)],[f93]) ).
fof(f93_sk,plain,
~ subclass(x,z),
inference(skolemisation,[status(esa)],[f93_nnf]) ).
cnf(c93,plain,
~ subclass(x,z),
inference(cnf_transformation,[status(esa)],[f93_sk]) ).
cnf(t12,plain,
subclass(x,z) = false,
inference(equality_encoding,[status(esa)],[c93]) ).
cnf(t108,plain,
subclass(x,z) = false,
inference(orient,[status(thm)],[t12]) ).
cnf(t1285,plain,
sF1 = false,
inference(step,[status(thm)],[t93,t108]) ).
cnf(t131,plain,
false = sF1,
inference(orient,[status(thm)],[t1285]) ).
cnf(f2,axiom,
( subclass(X,Y)
| ~ member(not_subclass_element(X,Y),Y) ),
file('/export/starexec/sandbox/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(t45,plain,
ifeq(member(not_subclass_element(X1,X2),X2),true,subclass(X1,X2),true) = true,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t1388,plain,
ifeq(member(not_subclass_element(X1,X2),X2),sF0,subclass(X1,X2),true) = true,
inference(step,[status(thm)],[t45,t110]) ).
cnf(t1389,plain,
ifeq(member(not_subclass_element(X1,X2),X2),sF0,subclass(X1,X2),sF0) = true,
inference(step,[status(thm)],[t1388,t110]) ).
cnf(t1390,plain,
ifeq(member(not_subclass_element(X1,X2),X2),sF0,subclass(X1,X2),sF0) = sF0,
inference(step,[status(thm)],[t1389,t110]) ).
cnf(t326,plain,
ifeq(member(not_subclass_element(X1,X2),X2),sF0,subclass(X1,X2),sF0) = sF0,
inference(orient,[status(thm)],[t1390]) ).
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(t59,plain,
ifeq(subclass(X1,X2),true,ifeq(member(X3,X1),true,member(X3,X2),true),true) = true,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t1539,plain,
ifeq(subclass(X1,X2),sF0,ifeq(member(X3,X1),true,member(X3,X2),true),true) = true,
inference(step,[status(thm)],[t59,t110]) ).
cnf(t1540,plain,
ifeq(subclass(X1,X2),sF0,ifeq(member(X3,X1),sF0,member(X3,X2),true),true) = true,
inference(step,[status(thm)],[t1539,t110]) ).
cnf(t1541,plain,
ifeq(subclass(X1,X2),sF0,ifeq(member(X3,X1),sF0,member(X3,X2),sF0),true) = true,
inference(step,[status(thm)],[t1540,t110]) ).
cnf(t1542,plain,
ifeq(subclass(X1,X2),sF0,ifeq(member(X3,X1),sF0,member(X3,X2),sF0),sF0) = true,
inference(step,[status(thm)],[t1541,t110]) ).
cnf(t1543,plain,
ifeq(subclass(X1,X2),sF0,ifeq(member(X3,X1),sF0,member(X3,X2),sF0),sF0) = sF0,
inference(step,[status(thm)],[t1542,t110]) ).
cnf(t669,plain,
ifeq(subclass(X1,X2),sF0,ifeq(member(X3,X1),sF0,member(X3,X2),sF0),sF0) = sF0,
inference(orient,[status(thm)],[t1543]) ).
cnf(f92,negated_conjecture,
subclass(y,z),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_transitivity_of_subclass_2) ).
fof(f92_nnf,plain,
subclass(y,z),
inference(nnf_transformation,[status(thm)],[f92]) ).
cnf(c92,plain,
subclass(y,z),
inference(cnf_transformation,[status(esa)],[f92_nnf]) ).
cnf(t13,plain,
subclass(y,z) = true,
inference(equality_encoding,[status(esa)],[c92]) ).
cnf(t109,plain,
subclass(y,z) = true,
inference(orient,[status(thm)],[t13]) ).
cnf(t1283,plain,
subclass(y,z) = sF0,
inference(step,[status(thm)],[t109,t110]) ).
cnf(t128,plain,
subclass(y,z) = sF0,
inference(orient,[status(thm)],[t1283]) ).
cnf(t675,plain,
sF0 = ifeq(sF0,sF0,ifeq(member(X1,y),sF0,member(X1,z),sF0),sF0),
inference(cp,[status(thm)],[t669,t128]) ).
cnf(t14,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t143,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t14]) ).
cnf(t1636,plain,
sF0 = ifeq(member(X1,y),sF0,member(X1,z),sF0),
inference(step,[status(thm)],[t675,t143]) ).
cnf(t1167,plain,
ifeq(member(X1,y),sF0,member(X1,z),sF0) = sF0,
inference(orient,[status(thm)],[t1636]) ).
cnf(t1281,plain,
subclass(x,y) = sF0,
inference(step,[status(thm)],[t107,t110]) ).
cnf(t126,plain,
subclass(x,y) = sF0,
inference(orient,[status(thm)],[t1281]) ).
cnf(t673,plain,
sF0 = ifeq(sF0,sF0,ifeq(member(X1,x),sF0,member(X1,y),sF0),sF0),
inference(cp,[status(thm)],[t669,t126]) ).
cnf(t1628,plain,
sF0 = ifeq(member(X1,x),sF0,member(X1,y),sF0),
inference(step,[status(thm)],[t673,t143]) ).
cnf(t1139,plain,
ifeq(member(X1,x),sF0,member(X1,y),sF0) = sF0,
inference(orient,[status(thm)],[t1628]) ).
cnf(f1,axiom,
( subclass(X,Y)
| member(not_subclass_element(X,Y),X) ),
file('/export/starexec/sandbox/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(t36,plain,
or(member(not_subclass_element(X1,X2),X1),subclass(X1,X2)) = true,
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t1343,plain,
or(member(not_subclass_element(X1,X2),X1),subclass(X1,X2)) = sF0,
inference(step,[status(thm)],[t36,t110]) ).
cnf(t211,plain,
or(member(not_subclass_element(X1,X2),X1),subclass(X1,X2)) = sF0,
inference(orient,[status(thm)],[t1343]) ).
cnf(t1289,plain,
subclass(x,z) = sF1,
inference(step,[status(thm)],[t108,t131]) ).
cnf(t135,plain,
subclass(x,z) = sF1,
inference(orient,[status(thm)],[t1289]) ).
cnf(t212,plain,
sF0 = or(member(not_subclass_element(x,z),x),sF1),
inference(cp,[status(thm)],[t211,t135]) ).
cnf(t6,plain,
or(X1,false) = X1,
introduced(definition) ).
cnf(t102,plain,
or(X1,false) = X1,
inference(orient,[status(thm)],[t6]) ).
cnf(t1287,plain,
or(X1,sF1) = X1,
inference(step,[status(thm)],[t102,t131]) ).
cnf(t133,plain,
or(X1,sF1) = X1,
inference(rw,[status(thm)],[t1287]) ).
cnf(t144,plain,
or(X1,sF1) = X1,
inference(orient,[status(thm)],[t133]) ).
cnf(t1344,plain,
sF0 = member(not_subclass_element(x,z),x),
inference(step,[status(thm)],[t212,t144]) ).
cnf(t214,plain,
member(not_subclass_element(x,z),x) = sF0,
inference(orient,[status(thm)],[t1344]) ).
cnf(t1140,plain,
sF0 = ifeq(sF0,sF0,member(not_subclass_element(x,z),y),sF0),
inference(cp,[status(thm)],[t1139,t214]) ).
cnf(t1629,plain,
sF0 = member(not_subclass_element(x,z),y),
inference(step,[status(thm)],[t1140,t143]) ).
cnf(t1141,plain,
member(not_subclass_element(x,z),y) = sF0,
inference(orient,[status(thm)],[t1629]) ).
cnf(t1168,plain,
sF0 = ifeq(sF0,sF0,member(not_subclass_element(x,z),z),sF0),
inference(cp,[status(thm)],[t1167,t1141]) ).
cnf(t1637,plain,
sF0 = member(not_subclass_element(x,z),z),
inference(step,[status(thm)],[t1168,t143]) ).
cnf(t1169,plain,
member(not_subclass_element(x,z),z) = sF0,
inference(orient,[status(thm)],[t1637]) ).
cnf(t1172,plain,
sF0 = ifeq(sF0,sF0,subclass(x,z),sF0),
inference(cp,[status(thm)],[t326,t1169]) ).
cnf(t1638,plain,
sF0 = subclass(x,z),
inference(step,[status(thm)],[t1172,t143]) ).
cnf(t1639,plain,
sF0 = sF1,
inference(step,[status(thm)],[t1638,t135]) ).
cnf(t1184,plain,
sF1 = sF0,
inference(orient,[status(thm)],[t1639]) ).
cnf(t1644,plain,
false = sF0,
inference(step,[status(thm)],[t131,t1184]) ).
cnf(t1189,plain,
false = sF0,
inference(orient,[status(thm)],[t1644]) ).
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(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,c93]) ).
cnf(g0_0,plain,
sF0 != false,
inference(rw,[status(thm)],[goal_0,t110]) ).
cnf(g0_1,plain,
sF0 != sF0,
inference(rw,[status(thm)],[g0_0,t1189]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SET027-6 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.08/0.35 % Computer : n020.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 09:18:48 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.35 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 3.30/0.89 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.30/0.89 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------