%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SET152-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 : n008.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:37 PM UTC 2026
% Result : Unsatisfiable 7.78s 6.42s
% Output : Proof 7.78s
% Verified :
% SZS Type : Refutation
% Derivation depth : 36
% Number of leaves : 13
% Syntax : Number of formulae : 107 ( 91 unt; 0 def)
% Number of atoms : 127 ( 94 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 51 ( 31 ~; 20 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 7 con; 0-4 aty)
% Number of variables : 94 ( 11 sgn 18 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(t110,axiom,
sF2 = ifeq(complement(universal_class),null_class,false,true),
introduced(definition) ).
cnf(t108,axiom,
sF0 = complement(universal_class),
introduced(definition) ).
cnf(t115,plain,
complement(universal_class) = sF0,
inference(orient,[status(thm)],[t108]) ).
cnf(t1210,plain,
sF2 = ifeq(sF0,null_class,false,true),
inference(step,[status(thm)],[t110,t115]) ).
cnf(t109,axiom,
sF1 = eq(complement(universal_class),null_class),
introduced(definition) ).
cnf(t1197,plain,
sF1 = eq(sF0,null_class),
inference(step,[status(thm)],[t109,t115]) ).
cnf(f112,negated_conjecture,
complement(universal_class) != null_class,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_complement_of_universal_class_1) ).
fof(f112_nnf,plain,
complement(universal_class) != null_class,
inference(nnf_transformation,[status(thm)],[f112]) ).
fof(f112_sk,plain,
complement(universal_class) != null_class,
inference(skolemisation,[status(esa)],[f112_nnf]) ).
cnf(c112,plain,
complement(universal_class) != null_class,
inference(cnf_transformation,[status(esa)],[f112_sk]) ).
cnf(t11,plain,
eq(complement(universal_class),null_class) = false,
inference(equality_encoding,[status(esa)],[c112]) ).
cnf(t1196,plain,
eq(sF0,null_class) = false,
inference(step,[status(thm)],[t11,t115]) ).
cnf(t123,plain,
eq(sF0,null_class) = false,
inference(orient,[status(thm)],[t1196]) ).
cnf(t1198,plain,
sF1 = false,
inference(step,[status(thm)],[t1197,t123]) ).
cnf(t124,plain,
false = sF1,
inference(orient,[status(thm)],[t1198]) ).
cnf(t1211,plain,
sF2 = ifeq(sF0,null_class,sF1,true),
inference(step,[status(thm)],[t1210,t124]) ).
cnf(t17,plain,
ifeq(complement(universal_class),null_class,false,true) = true,
inference(equality_encoding,[status(esa)],[c112]) ).
cnf(t1206,plain,
ifeq(sF0,null_class,false,true) = true,
inference(step,[status(thm)],[t17,t115]) ).
cnf(t1207,plain,
ifeq(sF0,null_class,sF1,true) = true,
inference(step,[status(thm)],[t1206,t124]) ).
cnf(t140,plain,
ifeq(sF0,null_class,sF1,true) = true,
inference(orient,[status(thm)],[t1207]) ).
cnf(t1212,plain,
sF2 = true,
inference(step,[status(thm)],[t1211,t140]) ).
cnf(t145,plain,
true = sF2,
inference(orient,[status(thm)],[t1212]) ).
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(t1502,plain,
ifeq(subclass(X1,X2),sF2,ifeq(member(X3,X1),true,member(X3,X2),true),true) = true,
inference(step,[status(thm)],[t65,t145]) ).
cnf(t1503,plain,
ifeq(subclass(X1,X2),sF2,ifeq(member(X3,X1),sF2,member(X3,X2),true),true) = true,
inference(step,[status(thm)],[t1502,t145]) ).
cnf(t1504,plain,
ifeq(subclass(X1,X2),sF2,ifeq(member(X3,X1),sF2,member(X3,X2),sF2),true) = true,
inference(step,[status(thm)],[t1503,t145]) ).
cnf(t1505,plain,
ifeq(subclass(X1,X2),sF2,ifeq(member(X3,X1),sF2,member(X3,X2),sF2),sF2) = true,
inference(step,[status(thm)],[t1504,t145]) ).
cnf(t1506,plain,
ifeq(subclass(X1,X2),sF2,ifeq(member(X3,X1),sF2,member(X3,X2),sF2),sF2) = sF2,
inference(step,[status(thm)],[t1505,t145]) ).
cnf(t800,plain,
ifeq(subclass(X1,X2),sF2,ifeq(member(X3,X1),sF2,member(X3,X2),sF2),sF2) = sF2,
inference(orient,[status(thm)],[t1506]) ).
cnf(t18,plain,
ifeq(not(X1),true,X1,false) = false,
introduced(definition) ).
cnf(t1208,plain,
ifeq(not(X1),true,X1,sF1) = false,
inference(step,[status(thm)],[t18,t124]) ).
cnf(t1209,plain,
ifeq(not(X1),true,X1,sF1) = sF1,
inference(step,[status(thm)],[t1208,t124]) ).
cnf(t141,plain,
ifeq(not(X1),true,X1,sF1) = sF1,
inference(orient,[status(thm)],[t1209]) ).
cnf(t1234,plain,
ifeq(not(X1),sF2,X1,sF1) = sF1,
inference(step,[status(thm)],[t141,t145]) ).
cnf(t170,plain,
ifeq(not(X1),sF2,X1,sF1) = sF1,
inference(rw,[status(thm)],[t1234]) ).
cnf(t188,plain,
ifeq(not(X1),sF2,X1,sF1) = sF1,
inference(orient,[status(thm)],[t170]) ).
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(t44,plain,
or(not(member(X1,complement(X2))),not(member(X1,X2))) = true,
inference(equality_encoding,[status(esa)],[c23]) ).
cnf(t1288,plain,
or(not(member(X1,complement(X2))),not(member(X1,X2))) = sF2,
inference(step,[status(thm)],[t44,t145]) ).
cnf(t282,plain,
or(not(member(X1,complement(X2))),not(member(X1,X2))) = sF2,
inference(orient,[status(thm)],[t1288]) ).
cnf(t283,plain,
sF2 = or(not(member(X1,sF0)),not(member(X1,universal_class))),
inference(cp,[status(thm)],[t282,t115]) ).
cnf(t320,plain,
or(not(member(X1,sF0)),not(member(X1,universal_class))) = sF2,
inference(orient,[status(thm)],[t283]) ).
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(t32,plain,
or(eq(X1,null_class),member(regular(X1),X1)) = true,
inference(equality_encoding,[status(esa)],[c65]) ).
cnf(t1263,plain,
or(eq(X1,null_class),member(regular(X1),X1)) = sF2,
inference(step,[status(thm)],[t32,t145]) ).
cnf(t228,plain,
or(eq(X1,null_class),member(regular(X1),X1)) = sF2,
inference(orient,[status(thm)],[t1263]) ).
cnf(t1204,plain,
eq(sF0,null_class) = sF1,
inference(step,[status(thm)],[t123,t124]) ).
cnf(t130,plain,
eq(sF0,null_class) = sF1,
inference(orient,[status(thm)],[t1204]) ).
cnf(t229,plain,
sF2 = or(sF1,member(regular(sF0),sF0)),
inference(cp,[status(thm)],[t228,t130]) ).
cnf(t8,plain,
or(false,X1) = X1,
introduced(definition) ).
cnf(t120,plain,
or(false,X1) = X1,
inference(orient,[status(thm)],[t8]) ).
cnf(t1203,plain,
or(sF1,X1) = X1,
inference(step,[status(thm)],[t120,t124]) ).
cnf(t129,plain,
or(sF1,X1) = X1,
inference(rw,[status(thm)],[t1203]) ).
cnf(t134,plain,
or(sF1,X1) = X1,
inference(orient,[status(thm)],[t129]) ).
cnf(t1264,plain,
sF2 = member(regular(sF0),sF0),
inference(step,[status(thm)],[t229,t134]) ).
cnf(t230,plain,
member(regular(sF0),sF0) = sF2,
inference(orient,[status(thm)],[t1264]) ).
cnf(t321,plain,
sF2 = or(not(sF2),not(member(regular(sF0),universal_class))),
inference(cp,[status(thm)],[t320,t230]) ).
cnf(t3,plain,
not(true) = false,
introduced(definition) ).
cnf(t114,plain,
not(true) = false,
inference(orient,[status(thm)],[t3]) ).
cnf(t1200,plain,
not(true) = sF1,
inference(step,[status(thm)],[t114,t124]) ).
cnf(t126,plain,
not(true) = sF1,
inference(orient,[status(thm)],[t1200]) ).
cnf(t1217,plain,
not(sF2) = sF1,
inference(step,[status(thm)],[t126,t145]) ).
cnf(t150,plain,
not(sF2) = sF1,
inference(rw,[status(thm)],[t1217]) ).
cnf(t174,plain,
not(sF2) = sF1,
inference(orient,[status(thm)],[t150]) ).
cnf(t1309,plain,
sF2 = or(sF1,not(member(regular(sF0),universal_class))),
inference(step,[status(thm)],[t321,t174]) ).
cnf(t1310,plain,
sF2 = not(member(regular(sF0),universal_class)),
inference(step,[status(thm)],[t1309,t134]) ).
cnf(t322,plain,
not(member(regular(sF0),universal_class)) = sF2,
inference(orient,[status(thm)],[t1310]) ).
cnf(t323,plain,
sF1 = ifeq(sF2,sF2,member(regular(sF0),universal_class),sF1),
inference(cp,[status(thm)],[t188,t322]) ).
cnf(t12,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t135,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t12]) ).
cnf(t1311,plain,
sF1 = member(regular(sF0),universal_class),
inference(step,[status(thm)],[t323,t135]) ).
cnf(t324,plain,
member(regular(sF0),universal_class) = sF1,
inference(orient,[status(thm)],[t1311]) ).
cnf(t831,plain,
sF2 = ifeq(subclass(X1,universal_class),sF2,ifeq(member(regular(sF0),X1),sF2,sF1,sF2),sF2),
inference(cp,[status(thm)],[t800,t324]) ).
cnf(f3,axiom,
subclass(X,universal_class),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',class_elements_are_sets) ).
fof(f3_nnf,plain,
! [X] : subclass(X,universal_class),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [X] : subclass(X,universal_class),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
subclass(X0,universal_class),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(t10,plain,
subclass(X1,universal_class) = true,
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t122,plain,
subclass(X1,universal_class) = true,
inference(orient,[status(thm)],[t10]) ).
cnf(t1222,plain,
subclass(X1,universal_class) = sF2,
inference(step,[status(thm)],[t122,t145]) ).
cnf(t157,plain,
subclass(X1,universal_class) = sF2,
inference(orient,[status(thm)],[t1222]) ).
cnf(t1525,plain,
sF2 = ifeq(sF2,sF2,ifeq(member(regular(sF0),X1),sF2,sF1,sF2),sF2),
inference(step,[status(thm)],[t831,t157]) ).
cnf(t1526,plain,
sF2 = ifeq(member(regular(sF0),X1),sF2,sF1,sF2),
inference(step,[status(thm)],[t1525,t135]) ).
cnf(t937,plain,
ifeq(member(regular(sF0),X1),sF2,sF1,sF2) = sF2,
inference(orient,[status(thm)],[t1526]) ).
cnf(t942,plain,
sF2 = ifeq(sF2,sF2,sF1,sF2),
inference(cp,[status(thm)],[t937,t230]) ).
cnf(t1531,plain,
sF2 = sF1,
inference(step,[status(thm)],[t942,t135]) ).
cnf(t944,plain,
sF2 = sF1,
inference(orient,[status(thm)],[t1531]) ).
cnf(t1554,plain,
true = sF1,
inference(step,[status(thm)],[t145,t944]) ).
cnf(t967,plain,
true = sF1,
inference(orient,[status(thm)],[t1554]) ).
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,c112]) ).
cnf(g0_0,plain,
sF1 != false,
inference(rw,[status(thm)],[goal_0,t967]) ).
cnf(g0_1,plain,
sF1 != sF1,
inference(rw,[status(thm)],[g0_0,t124]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET152-6 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/5.37 % Computer : n008.cluster.edu
% 0.10/5.37 % Model : x86_64 x86_64
% 0.10/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.37 % Memory : 8046.5625MB
% 0.10/5.37 % OS : Linux 6.8.0-71-generic
% 0.10/5.37 % CPULimit : 300
% 0.10/5.37 % WCLimit : 300
% 0.10/5.37 % DateTime : Thu Sep 24 10:04:14 UTC 2026
% 0.10/5.37 % CPUTime :
% 0.10/5.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 7.78/6.42 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 7.78/6.42 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------