%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SET254-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 : n004.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:59 PM UTC 2026
% Result : Unsatisfiable 241.78s 35.91s
% Output : Proof 241.78s
% Verified :
% Comments :
%------------------------------------------------------------------------------
cnf(t109,axiom,
sF0 = subclass(x1,x2),
introduced(definition) ).
cnf(f112,negated_conjecture,
subclass(x1,x2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_monotonicity_of_restriction1_1) ).
fof(f112_nnf,plain,
subclass(x1,x2),
inference(nnf_transformation,[status(thm)],[f112]) ).
cnf(c112,plain,
subclass(x1,x2),
inference(cnf_transformation,[status(esa)],[f112_nnf]) ).
cnf(t11,plain,
subclass(x1,x2) = true,
inference(equality_encoding,[status(esa)],[c112]) ).
cnf(t126,plain,
subclass(x1,x2) = true,
inference(orient,[status(thm)],[t11]) ).
cnf(t51578,plain,
sF0 = true,
inference(step,[status(thm)],[t109,t126]) ).
cnf(t127,plain,
true = sF0,
inference(orient,[status(thm)],[t51578]) ).
cnf(t113,axiom,
sF4 = subclass(intersection(x1,cross_product(y,z)),intersection(x2,cross_product(y,z))),
introduced(definition) ).
cnf(t110,axiom,
sF1 = cross_product(y,z),
introduced(definition) ).
cnf(t146,plain,
cross_product(y,z) = sF1,
inference(orient,[status(thm)],[t110]) ).
cnf(t51722,plain,
sF4 = subclass(intersection(x1,sF1),intersection(x2,cross_product(y,z))),
inference(step,[status(thm)],[t113,t146]) ).
cnf(f28,axiom,
intersection(cross_product(X,Y),Xr) = restrict(Xr,X,Y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',restriction2) ).
fof(f28_nnf,plain,
! [X,Y,Xr] : intersection(cross_product(X,Y),Xr) = restrict(Xr,X,Y),
inference(nnf_transformation,[status(thm)],[f28]) ).
fof(f28_sk,plain,
! [X,Y,Xr] : intersection(cross_product(X,Y),Xr) = restrict(Xr,X,Y),
inference(skolemisation,[status(esa)],[f28_nnf]) ).
cnf(c28,plain,
intersection(cross_product(X0,X1),X2) = restrict(X2,X0,X1),
inference(cnf_transformation,[status(esa)],[f28_sk]) ).
cnf(u35,axiom,
intersection(cross_product(X0,X1),X2) = restrict(X2,X0,X1),
inference(equality_encoding,[status(esa)],[c28]) ).
cnf(f27,axiom,
intersection(Xr,cross_product(X,Y)) = restrict(Xr,X,Y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',restriction1) ).
fof(f27_nnf,plain,
! [Xr,X,Y] : intersection(Xr,cross_product(X,Y)) = restrict(Xr,X,Y),
inference(nnf_transformation,[status(thm)],[f27]) ).
fof(f27_sk,plain,
! [Xr,X,Y] : intersection(Xr,cross_product(X,Y)) = restrict(Xr,X,Y),
inference(skolemisation,[status(esa)],[f27_nnf]) ).
cnf(c27,plain,
intersection(X0,cross_product(X1,X2)) = restrict(X0,X1,X2),
inference(cnf_transformation,[status(esa)],[f27_sk]) ).
cnf(d4,axiom,
intersection(X0,cross_product(X1,X2)) = restrict(X0,X1,X2),
inference(equality_encoding,[status(esa)],[c27]) ).
cnf(t39,plain,
intersection(cross_product(X1,X2),X3) = intersection(X3,cross_product(X1,X2)),
inference(definition_unfolding,[status(thm)],[u35,d4]) ).
cnf(t227,plain,
intersection(cross_product(X1,X2),X3) = intersection(X3,cross_product(X1,X2)),
inference(orient,[status(thm)],[t39]) ).
cnf(t228,plain,
intersection(X1,cross_product(y,z)) = intersection(sF1,X1),
inference(cp,[status(thm)],[t227,t146]) ).
cnf(t51641,plain,
intersection(X1,sF1) = intersection(sF1,X1),
inference(step,[status(thm)],[t228,t146]) ).
cnf(t229,plain,
intersection(X1,sF1) = intersection(sF1,X1),
inference(orient,[status(thm)],[t51641]) ).
cnf(t51723,plain,
sF4 = subclass(intersection(sF1,x1),intersection(x2,cross_product(y,z))),
inference(step,[status(thm)],[t51722,t229]) ).
cnf(t111,axiom,
sF2 = intersection(x1,cross_product(y,z)),
introduced(definition) ).
cnf(t51600,plain,
sF2 = intersection(x1,sF1),
inference(step,[status(thm)],[t111,t146]) ).
cnf(t154,plain,
intersection(x1,sF1) = sF2,
inference(orient,[status(thm)],[t51600]) ).
cnf(t51642,plain,
intersection(sF1,x1) = sF2,
inference(step,[status(thm)],[t154,t229]) ).
cnf(t230,plain,
intersection(sF1,x1) = sF2,
inference(rw,[status(thm)],[t51642]) ).
cnf(t232,plain,
intersection(sF1,x1) = sF2,
inference(orient,[status(thm)],[t230]) ).
cnf(t51724,plain,
sF4 = subclass(sF2,intersection(x2,cross_product(y,z))),
inference(step,[status(thm)],[t51723,t232]) ).
cnf(t51725,plain,
sF4 = subclass(sF2,intersection(x2,sF1)),
inference(step,[status(thm)],[t51724,t146]) ).
cnf(t51726,plain,
sF4 = subclass(sF2,intersection(sF1,x2)),
inference(step,[status(thm)],[t51725,t229]) ).
cnf(t112,axiom,
sF3 = intersection(x2,cross_product(y,z)),
introduced(definition) ).
cnf(t51601,plain,
sF3 = intersection(x2,sF1),
inference(step,[status(thm)],[t112,t146]) ).
cnf(t155,plain,
intersection(x2,sF1) = sF3,
inference(orient,[status(thm)],[t51601]) ).
cnf(t51643,plain,
intersection(sF1,x2) = sF3,
inference(step,[status(thm)],[t155,t229]) ).
cnf(t231,plain,
intersection(sF1,x2) = sF3,
inference(rw,[status(thm)],[t51643]) ).
cnf(t233,plain,
intersection(sF1,x2) = sF3,
inference(orient,[status(thm)],[t231]) ).
cnf(t51727,plain,
sF4 = subclass(sF2,sF3),
inference(step,[status(thm)],[t51726,t233]) ).
cnf(f113,negated_conjecture,
~ subclass(restrict(x1,y,z),restrict(x2,y,z)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_monotonicity_of_restriction1_2) ).
fof(f113_nnf,plain,
~ subclass(restrict(x1,y,z),restrict(x2,y,z)),
inference(nnf_transformation,[status(thm)],[f113]) ).
fof(f113_sk,plain,
~ subclass(restrict(x1,y,z),restrict(x2,y,z)),
inference(skolemisation,[status(esa)],[f113_nnf]) ).
cnf(c113,plain,
~ subclass(restrict(x1,y,z),restrict(x2,y,z)),
inference(cnf_transformation,[status(esa)],[f113_sk]) ).
cnf(u39,axiom,
subclass(restrict(x1,y,z),restrict(x2,y,z)) = false,
inference(equality_encoding,[status(esa)],[c113]) ).
cnf(t51,plain,
subclass(intersection(x1,cross_product(y,z)),intersection(x2,cross_product(y,z))) = false,
inference(definition_unfolding,[status(thm)],[u39,d4]) ).
cnf(t51693,plain,
subclass(intersection(x1,sF1),intersection(x2,cross_product(y,z))) = false,
inference(step,[status(thm)],[t51,t146]) ).
cnf(t51694,plain,
subclass(intersection(sF1,x1),intersection(x2,cross_product(y,z))) = false,
inference(step,[status(thm)],[t51693,t229]) ).
cnf(t51695,plain,
subclass(sF2,intersection(x2,cross_product(y,z))) = false,
inference(step,[status(thm)],[t51694,t232]) ).
cnf(t51696,plain,
subclass(sF2,intersection(x2,sF1)) = false,
inference(step,[status(thm)],[t51695,t146]) ).
cnf(t51697,plain,
subclass(sF2,intersection(sF1,x2)) = false,
inference(step,[status(thm)],[t51696,t229]) ).
cnf(t51698,plain,
subclass(sF2,sF3) = false,
inference(step,[status(thm)],[t51697,t233]) ).
cnf(t382,plain,
subclass(sF2,sF3) = false,
inference(orient,[status(thm)],[t51698]) ).
cnf(t51728,plain,
sF4 = false,
inference(step,[status(thm)],[t51727,t382]) ).
cnf(t464,plain,
false = sF4,
inference(orient,[status(thm)],[t51728]) ).
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(t49,plain,
ifeq(member(not_subclass_element(X1,X2),X2),true,subclass(X1,X2),true) = true,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t51682,plain,
ifeq(member(not_subclass_element(X1,X2),X2),sF0,subclass(X1,X2),true) = true,
inference(step,[status(thm)],[t49,t127]) ).
cnf(t51683,plain,
ifeq(member(not_subclass_element(X1,X2),X2),sF0,subclass(X1,X2),sF0) = true,
inference(step,[status(thm)],[t51682,t127]) ).
cnf(t51684,plain,
ifeq(member(not_subclass_element(X1,X2),X2),sF0,subclass(X1,X2),sF0) = sF0,
inference(step,[status(thm)],[t51683,t127]) ).
cnf(t350,plain,
ifeq(member(not_subclass_element(X1,X2),X2),sF0,subclass(X1,X2),sF0) = sF0,
inference(orient,[status(thm)],[t51684]) ).
cnf(f22,axiom,
( member(Z,intersection(X,Y))
| ~ member(Z,Y)
| ~ member(Z,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intersection3) ).
fof(f22_nnf,plain,
! [Z,X,Y] :
( member(Z,intersection(X,Y))
| ~ member(Z,Y)
| ~ member(Z,X) ),
inference(nnf_transformation,[status(thm)],[f22]) ).
fof(f22_sk,plain,
! [Z,X,Y] :
( member(Z,intersection(X,Y))
| ~ member(Z,Y)
| ~ member(Z,X) ),
inference(skolemisation,[status(esa)],[f22_nnf]) ).
cnf(c22,plain,
( member(X0,intersection(X1,X2))
| ~ member(X0,X2)
| ~ member(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f22_sk]) ).
cnf(t72,plain,
ifeq(member(X1,X2),true,ifeq(member(X1,X3),true,member(X1,intersection(X2,X3)),true),true) = true,
inference(equality_encoding,[status(esa)],[c22]) ).
cnf(t51970,plain,
ifeq(member(X1,X2),sF0,ifeq(member(X1,X3),true,member(X1,intersection(X2,X3)),true),true) = true,
inference(step,[status(thm)],[t72,t127]) ).
cnf(t51971,plain,
ifeq(member(X1,X2),sF0,ifeq(member(X1,X3),sF0,member(X1,intersection(X2,X3)),true),true) = true,
inference(step,[status(thm)],[t51970,t127]) ).
cnf(t51972,plain,
ifeq(member(X1,X2),sF0,ifeq(member(X1,X3),sF0,member(X1,intersection(X2,X3)),sF0),true) = true,
inference(step,[status(thm)],[t51971,t127]) ).
cnf(t51973,plain,
ifeq(member(X1,X2),sF0,ifeq(member(X1,X3),sF0,member(X1,intersection(X2,X3)),sF0),sF0) = true,
inference(step,[status(thm)],[t51972,t127]) ).
cnf(t51974,plain,
ifeq(member(X1,X2),sF0,ifeq(member(X1,X3),sF0,member(X1,intersection(X2,X3)),sF0),sF0) = sF0,
inference(step,[status(thm)],[t51973,t127]) ).
cnf(t1115,plain,
ifeq(member(X1,X2),sF0,ifeq(member(X1,X3),sF0,member(X1,intersection(X2,X3)),sF0),sF0) = sF0,
inference(orient,[status(thm)],[t51974]) ).
cnf(t1125,plain,
sF0 = ifeq(member(X1,X2),sF0,ifeq(member(X1,sF1),sF0,member(X1,intersection(sF1,X2)),sF0),sF0),
inference(cp,[status(thm)],[t1115,t229]) ).
cnf(t50111,plain,
ifeq(member(X1,X2),sF0,ifeq(member(X1,sF1),sF0,member(X1,intersection(sF1,X2)),sF0),sF0) = sF0,
inference(orient,[status(thm)],[t1125]) ).
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(t65,plain,
ifeq(subclass(X1,X2),true,ifeq(member(X3,X1),true,member(X3,X2),true),true) = true,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t51884,plain,
ifeq(subclass(X1,X2),sF0,ifeq(member(X3,X1),true,member(X3,X2),true),true) = true,
inference(step,[status(thm)],[t65,t127]) ).
cnf(t51885,plain,
ifeq(subclass(X1,X2),sF0,ifeq(member(X3,X1),sF0,member(X3,X2),true),true) = true,
inference(step,[status(thm)],[t51884,t127]) ).
cnf(t51886,plain,
ifeq(subclass(X1,X2),sF0,ifeq(member(X3,X1),sF0,member(X3,X2),sF0),true) = true,
inference(step,[status(thm)],[t51885,t127]) ).
cnf(t51887,plain,
ifeq(subclass(X1,X2),sF0,ifeq(member(X3,X1),sF0,member(X3,X2),sF0),sF0) = true,
inference(step,[status(thm)],[t51886,t127]) ).
cnf(t51888,plain,
ifeq(subclass(X1,X2),sF0,ifeq(member(X3,X1),sF0,member(X3,X2),sF0),sF0) = sF0,
inference(step,[status(thm)],[t51887,t127]) ).
cnf(t773,plain,
ifeq(subclass(X1,X2),sF0,ifeq(member(X3,X1),sF0,member(X3,X2),sF0),sF0) = sF0,
inference(orient,[status(thm)],[t51888]) ).
cnf(t51592,plain,
subclass(x1,x2) = sF0,
inference(step,[status(thm)],[t126,t127]) ).
cnf(t143,plain,
subclass(x1,x2) = sF0,
inference(orient,[status(thm)],[t51592]) ).
cnf(t777,plain,
sF0 = ifeq(sF0,sF0,ifeq(member(X1,x1),sF0,member(X1,x2),sF0),sF0),
inference(cp,[status(thm)],[t773,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(t51965,plain,
sF0 = ifeq(member(X1,x1),sF0,member(X1,x2),sF0),
inference(step,[status(thm)],[t777,t149]) ).
cnf(t1099,plain,
ifeq(member(X1,x1),sF0,member(X1,x2),sF0) = sF0,
inference(orient,[status(thm)],[t51965]) ).
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(t46,plain,
ifeq(member(X1,intersection(X2,X3)),true,member(X1,X3),true) = true,
inference(equality_encoding,[status(esa)],[c21]) ).
cnf(t51666,plain,
ifeq(member(X1,intersection(X2,X3)),sF0,member(X1,X3),true) = true,
inference(step,[status(thm)],[t46,t127]) ).
cnf(t51667,plain,
ifeq(member(X1,intersection(X2,X3)),sF0,member(X1,X3),sF0) = true,
inference(step,[status(thm)],[t51666,t127]) ).
cnf(t51668,plain,
ifeq(member(X1,intersection(X2,X3)),sF0,member(X1,X3),sF0) = sF0,
inference(step,[status(thm)],[t51667,t127]) ).
cnf(t305,plain,
ifeq(member(X1,intersection(X2,X3)),sF0,member(X1,X3),sF0) = sF0,
inference(orient,[status(thm)],[t51668]) ).
cnf(t311,plain,
sF0 = ifeq(member(X1,sF2),sF0,member(X1,x1),sF0),
inference(cp,[status(thm)],[t305,t232]) ).
cnf(t324,plain,
ifeq(member(X1,sF2),sF0,member(X1,x1),sF0) = sF0,
inference(orient,[status(thm)],[t311]) ).
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(t40,plain,
or(member(not_subclass_element(X1,X2),X1),subclass(X1,X2)) = true,
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t51644,plain,
or(member(not_subclass_element(X1,X2),X1),subclass(X1,X2)) = sF0,
inference(step,[status(thm)],[t40,t127]) ).
cnf(t235,plain,
or(member(not_subclass_element(X1,X2),X1),subclass(X1,X2)) = sF0,
inference(orient,[status(thm)],[t51644]) ).
cnf(t385,plain,
sF0 = or(member(not_subclass_element(sF2,sF3),sF2),false),
inference(cp,[status(thm)],[t235,t382]) ).
cnf(t6,plain,
or(X1,false) = X1,
introduced(definition) ).
cnf(t121,plain,
or(X1,false) = X1,
inference(orient,[status(thm)],[t6]) ).
cnf(t51700,plain,
sF0 = member(not_subclass_element(sF2,sF3),sF2),
inference(step,[status(thm)],[t385,t121]) ).
cnf(t390,plain,
member(not_subclass_element(sF2,sF3),sF2) = sF0,
inference(orient,[status(thm)],[t51700]) ).
cnf(t395,plain,
sF0 = ifeq(sF0,sF0,member(not_subclass_element(sF2,sF3),x1),sF0),
inference(cp,[status(thm)],[t324,t390]) ).
cnf(t51702,plain,
sF0 = member(not_subclass_element(sF2,sF3),x1),
inference(step,[status(thm)],[t395,t149]) ).
cnf(t401,plain,
member(not_subclass_element(sF2,sF3),x1) = sF0,
inference(orient,[status(thm)],[t51702]) ).
cnf(t1100,plain,
sF0 = ifeq(sF0,sF0,member(not_subclass_element(sF2,sF3),x2),sF0),
inference(cp,[status(thm)],[t1099,t401]) ).
cnf(t51966,plain,
sF0 = member(not_subclass_element(sF2,sF3),x2),
inference(step,[status(thm)],[t1100,t149]) ).
cnf(t1101,plain,
member(not_subclass_element(sF2,sF3),x2) = sF0,
inference(orient,[status(thm)],[t51966]) ).
cnf(t50144,plain,
sF0 = ifeq(sF0,sF0,ifeq(member(not_subclass_element(sF2,sF3),sF1),sF0,member(not_subclass_element(sF2,sF3),intersection(sF1,x2)),sF0),sF0),
inference(cp,[status(thm)],[t50111,t1101]) ).
cnf(t55556,plain,
sF0 = ifeq(member(not_subclass_element(sF2,sF3),sF1),sF0,member(not_subclass_element(sF2,sF3),intersection(sF1,x2)),sF0),
inference(step,[status(thm)],[t50144,t149]) ).
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(t45,plain,
ifeq(member(X1,intersection(X2,X3)),true,member(X1,X2),true) = true,
inference(equality_encoding,[status(esa)],[c20]) ).
cnf(t51663,plain,
ifeq(member(X1,intersection(X2,X3)),sF0,member(X1,X2),true) = true,
inference(step,[status(thm)],[t45,t127]) ).
cnf(t51664,plain,
ifeq(member(X1,intersection(X2,X3)),sF0,member(X1,X2),sF0) = true,
inference(step,[status(thm)],[t51663,t127]) ).
cnf(t51665,plain,
ifeq(member(X1,intersection(X2,X3)),sF0,member(X1,X2),sF0) = sF0,
inference(step,[status(thm)],[t51664,t127]) ).
cnf(t286,plain,
ifeq(member(X1,intersection(X2,X3)),sF0,member(X1,X2),sF0) = sF0,
inference(orient,[status(thm)],[t51665]) ).
cnf(t294,plain,
sF0 = ifeq(member(X1,sF2),sF0,member(X1,sF1),sF0),
inference(cp,[status(thm)],[t286,t232]) ).
cnf(t303,plain,
ifeq(member(X1,sF2),sF0,member(X1,sF1),sF0) = sF0,
inference(orient,[status(thm)],[t294]) ).
cnf(t393,plain,
sF0 = ifeq(sF0,sF0,member(not_subclass_element(sF2,sF3),sF1),sF0),
inference(cp,[status(thm)],[t303,t390]) ).
cnf(t51701,plain,
sF0 = member(not_subclass_element(sF2,sF3),sF1),
inference(step,[status(thm)],[t393,t149]) ).
cnf(t396,plain,
member(not_subclass_element(sF2,sF3),sF1) = sF0,
inference(orient,[status(thm)],[t51701]) ).
cnf(t55557,plain,
sF0 = ifeq(sF0,sF0,member(not_subclass_element(sF2,sF3),intersection(sF1,x2)),sF0),
inference(step,[status(thm)],[t55556,t396]) ).
cnf(t55558,plain,
sF0 = member(not_subclass_element(sF2,sF3),intersection(sF1,x2)),
inference(step,[status(thm)],[t55557,t149]) ).
cnf(t55559,plain,
sF0 = member(not_subclass_element(sF2,sF3),sF3),
inference(step,[status(thm)],[t55558,t233]) ).
cnf(t50474,plain,
member(not_subclass_element(sF2,sF3),sF3) = sF0,
inference(orient,[status(thm)],[t55559]) ).
cnf(t50478,plain,
sF0 = ifeq(sF0,sF0,subclass(sF2,sF3),sF0),
inference(cp,[status(thm)],[t350,t50474]) ).
cnf(t55560,plain,
sF0 = subclass(sF2,sF3),
inference(step,[status(thm)],[t50478,t149]) ).
cnf(t51749,plain,
subclass(sF2,sF3) = sF4,
inference(step,[status(thm)],[t382,t464]) ).
cnf(t487,plain,
subclass(sF2,sF3) = sF4,
inference(orient,[status(thm)],[t51749]) ).
cnf(t55561,plain,
sF0 = sF4,
inference(step,[status(thm)],[t55560,t487]) ).
cnf(t50493,plain,
sF4 = sF0,
inference(orient,[status(thm)],[t55561]) ).
cnf(t55582,plain,
false = sF0,
inference(step,[status(thm)],[t464,t50493]) ).
cnf(t50514,plain,
false = sF0,
inference(orient,[status(thm)],[t55582]) ).
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,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,t50514]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET254-6 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.37 % Computer : n004.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Thu Sep 24 10:23:05 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 241.78/35.91 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 241.78/35.91 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------