%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SET090+1 : TPTP v9.3.1. Bugfixed v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n009.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:10 PM UTC 2026
% Result : Theorem 64.52s 9.22s
% Output : Proof 64.52s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 18
% Syntax : Number of formulae : 138 ( 100 unt; 0 def)
% Number of atoms : 235 ( 127 equ)
% Maximal formula atoms : 6 ( 1 avg)
% Number of connectives : 165 ( 68 ~; 52 |; 34 &)
% ( 5 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 2 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 20 ( 20 usr; 6 con; 0-4 aty)
% Number of variables : 137 ( 3 sgn 64 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f47,conjecture,
! [X,U] :
( ( X = singleton(U)
& member(U,universal_class) )
=> member_of(X) = U ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',member_of_singleton) ).
fof(f47_neg,negated_conjecture,
~ ! [X,U] :
( ( X = singleton(U)
& member(U,universal_class) )
=> member_of(X) = U ),
inference(negated_conjecture,[status(cth)],[f47]) ).
fof(f47_nnf,plain,
? [X,U] :
( member_of(X) != U
& X = singleton(U)
& member(U,universal_class) ),
inference(nnf_transformation,[status(thm)],[f47_neg]) ).
fof(f47_sk,plain,
( member_of(sk7) != sk8
& sk7 = singleton(sk8)
& member(sk8,universal_class) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk7,sk8])],[f47_nnf]) ).
cnf(c95,plain,
member_of(sk7) != sk8,
inference(cnf_transformation,[status(esa)],[f47_sk]) ).
cnf(t22,plain,
eq(member_of(sk7),sk8) = false,
inference(equality_encoding,[status(esa)],[c95]) ).
cnf(t1258,plain,
eq(member_of(sk7),sk8) = false,
inference(orient,[status(thm)],[t22]) ).
fof(f8,axiom,
! [X,Y] :
( ( member(Y,universal_class)
& member(X,universal_class) )
=> ( second(ordered_pair(X,Y)) = Y
& first(ordered_pair(X,Y)) = X ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',first_second) ).
fof(f8_nnf,plain,
! [X,Y] :
( ( second(ordered_pair(X,Y)) = Y
& first(ordered_pair(X,Y)) = X )
| ~ member(Y,universal_class)
| ~ member(X,universal_class) ),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [X,Y] :
( ( second(ordered_pair(X,Y)) = Y
& first(ordered_pair(X,Y)) = X )
| ~ member(Y,universal_class)
| ~ member(X,universal_class) ),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c18,plain,
( second(ordered_pair(X0,X1)) = X1
| ~ member(X1,universal_class)
| ~ member(X0,universal_class) ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(t211,plain,
ifeq(member(X1,universal_class),true,ifeq(member(X2,universal_class),true,second(ordered_pair(X1,X2)),X2),X2) = X2,
inference(equality_encoding,[status(esa)],[c18]) ).
cnf(t259,plain,
ifeq(member(X1,universal_class),true,ifeq(member(X2,universal_class),true,second(ordered_pair(X1,X2)),X2),X2) = X2,
inference(orient,[status(thm)],[t211]) ).
fof(f6,axiom,
! [X,Y] : ordered_pair(X,Y) = unordered_pair(singleton(X),unordered_pair(X,singleton(Y))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ordered_pair_defn) ).
fof(f6_nnf,plain,
! [X,Y] : ordered_pair(X,Y) = unordered_pair(singleton(X),unordered_pair(X,singleton(Y))),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [X,Y] : ordered_pair(X,Y) = unordered_pair(singleton(X),unordered_pair(X,singleton(Y))),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c13,plain,
ordered_pair(X0,X1) = unordered_pair(singleton(X0),unordered_pair(X0,singleton(X1))),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(t111,plain,
unordered_pair(singleton(X1),unordered_pair(X1,singleton(X2))) = ordered_pair(X1,X2),
inference(equality_encoding,[status(esa)],[c13]) ).
cnf(t293,plain,
unordered_pair(singleton(X1),unordered_pair(X1,singleton(X2))) = ordered_pair(X1,X2),
inference(orient,[status(thm)],[t111]) ).
fof(f2,axiom,
! [X,Y] :
( X = Y
<=> ( subclass(Y,X)
& subclass(X,Y) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',extensionality) ).
fof(f2_nnf,plain,
! [X,Y] :
( ( ~ subclass(Y,X)
| ~ subclass(X,Y)
| X = Y )
& ( ( subclass(Y,X)
& subclass(X,Y) )
| X != Y ) ),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [X,Y] :
( ( ~ subclass(Y,X)
| ~ subclass(X,Y)
| X = Y )
& ( ( subclass(Y,X)
& subclass(X,Y) )
| X != Y ) ),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c4,plain,
( subclass(X0,X1)
| X0 != X1 ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(hi4,axiom,
ifeq(X0,X1,subclass(X0,X1),true) = true,
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(c94,plain,
sk7 = singleton(sk8),
inference(cnf_transformation,[status(esa)],[f47_sk]) ).
cnf(hi90,negated_conjecture,
sk7 = singleton(sk8),
inference(equality_encoding,[status(esa)],[c94]) ).
fof(f5,axiom,
! [X] : singleton(X) = unordered_pair(X,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',singleton_set_defn) ).
fof(f5_nnf,plain,
! [X] : singleton(X) = unordered_pair(X,X),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [X] : singleton(X) = unordered_pair(X,X),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c12,plain,
singleton(X0) = unordered_pair(X0,X0),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(hi14,axiom,
singleton(X0) = unordered_pair(X0,X0),
inference(equality_encoding,[status(esa)],[c12]) ).
cnf(h109,plain,
subclass(sk7,unordered_pair(sk8,sk8)) = true,
inference(hyper_resolution,[status(thm)],[hi4,hi90,hi14]) ).
cnf(c5,plain,
( subclass(X1,X0)
| X0 != X1 ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(hi5,axiom,
ifeq(X0,X1,subclass(X1,X0),true) = true,
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(h108,plain,
subclass(unordered_pair(sk8,sk8),sk7) = true,
inference(hyper_resolution,[status(thm)],[hi5,hi90,hi14]) ).
cnf(c6,plain,
( ~ subclass(X1,X0)
| ~ subclass(X0,X1)
| X0 = X1 ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(hi6,axiom,
ifeq(subclass(X0,X1),true,ifeq(subclass(X1,X0),true,X0,X1),X1) = X1,
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t20,plain,
unordered_pair(sk8,sk8) = sk7,
inference(hyper_resolution,[status(thm)],[hi6,h108,h109]) ).
cnf(t27,plain,
unordered_pair(X1,X1) = singleton(X1),
inference(equality_encoding,[status(esa)],[c12]) ).
cnf(t264,plain,
unordered_pair(X1,X1) = singleton(X1),
inference(orient,[status(thm)],[t27]) ).
cnf(t9711,plain,
singleton(sk8) = sk7,
inference(step,[status(thm)],[t20,t264]) ).
cnf(t271,plain,
singleton(sk8) = sk7,
inference(orient,[status(thm)],[t9711]) ).
cnf(t314,plain,
ordered_pair(sk8,X1) = unordered_pair(sk7,unordered_pair(sk8,singleton(X1))),
inference(cp,[status(thm)],[t293,t271]) ).
cnf(t9487,plain,
unordered_pair(sk7,unordered_pair(sk8,singleton(X1))) = ordered_pair(sk8,X1),
inference(orient,[status(thm)],[t314]) ).
fof(f44,axiom,
! [Y] :
( member(Y,universal_class)
=> singleton(member_of(singleton(Y))) = singleton(Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',member_singleton_singleton) ).
fof(f44_nnf,plain,
! [Y] :
( singleton(member_of(singleton(Y))) = singleton(Y)
| ~ member(Y,universal_class) ),
inference(nnf_transformation,[status(thm)],[f44]) ).
fof(f44_sk,plain,
! [Y] :
( singleton(member_of(singleton(Y))) = singleton(Y)
| ~ member(Y,universal_class) ),
inference(skolemisation,[status(esa)],[f44_nnf]) ).
cnf(c90,plain,
( singleton(member_of(singleton(X0))) = singleton(X0)
| ~ member(X0,universal_class) ),
inference(cnf_transformation,[status(esa)],[f44_sk]) ).
cnf(hi86,axiom,
ifeq(member(X0,universal_class),true,singleton(member_of(singleton(X0))),singleton(X0)) = singleton(X0),
inference(equality_encoding,[status(esa)],[c90]) ).
cnf(c93,plain,
member(sk8,universal_class),
inference(cnf_transformation,[status(esa)],[f47_sk]) ).
cnf(hi89,negated_conjecture,
member(sk8,universal_class) = true,
inference(equality_encoding,[status(esa)],[c93]) ).
cnf(t154,plain,
unordered_pair(member_of(unordered_pair(sk8,sk8)),member_of(unordered_pair(sk8,sk8))) = unordered_pair(sk8,sk8),
inference(hyper_resolution,[status(thm)],[hi86,hi89,hi14]) ).
cnf(t9708,plain,
singleton(member_of(unordered_pair(sk8,sk8))) = unordered_pair(sk8,sk8),
inference(step,[status(thm)],[t154,t264]) ).
cnf(t9709,plain,
singleton(member_of(singleton(sk8))) = unordered_pair(sk8,sk8),
inference(step,[status(thm)],[t9708,t264]) ).
cnf(t9710,plain,
singleton(member_of(singleton(sk8))) = singleton(sk8),
inference(step,[status(thm)],[t9709,t264]) ).
cnf(t270,plain,
singleton(member_of(singleton(sk8))) = singleton(sk8),
inference(orient,[status(thm)],[t9710]) ).
cnf(t9712,plain,
singleton(member_of(sk7)) = singleton(sk8),
inference(step,[status(thm)],[t270,t271]) ).
cnf(t9713,plain,
singleton(member_of(sk7)) = sk7,
inference(step,[status(thm)],[t9712,t271]) ).
cnf(t272,plain,
singleton(member_of(sk7)) = sk7,
inference(rw,[status(thm)],[t9713]) ).
cnf(t1453,plain,
singleton(member_of(sk7)) = sk7,
inference(orient,[status(thm)],[t272]) ).
cnf(t9491,plain,
ordered_pair(sk8,member_of(sk7)) = unordered_pair(sk7,unordered_pair(sk8,sk7)),
inference(cp,[status(thm)],[t9487,t1453]) ).
cnf(t9510,plain,
ordered_pair(sk8,sk8) = unordered_pair(sk7,unordered_pair(sk8,sk7)),
inference(cp,[status(thm)],[t9487,t271]) ).
cnf(t9559,plain,
unordered_pair(sk7,unordered_pair(sk8,sk7)) = ordered_pair(sk8,sk8),
inference(orient,[status(thm)],[t9510]) ).
cnf(t10232,plain,
ordered_pair(sk8,member_of(sk7)) = ordered_pair(sk8,sk8),
inference(step,[status(thm)],[t9491,t9559]) ).
cnf(t9591,plain,
ordered_pair(sk8,member_of(sk7)) = ordered_pair(sk8,sk8),
inference(orient,[status(thm)],[t10232]) ).
cnf(t9597,plain,
member_of(sk7) = ifeq(member(sk8,universal_class),true,ifeq(member(member_of(sk7),universal_class),true,second(ordered_pair(sk8,sk8)),member_of(sk7)),member_of(sk7)),
inference(cp,[status(thm)],[t259,t9591]) ).
cnf(hi103,axiom,
or(false,X0) = X0,
introduced(definition) ).
cnf(h131,plain,
subclass(V0,or(false,V0)) = true,
inference(hyper_resolution,[status(thm)],[hi5,hi103]) ).
fof(f0,axiom,
! [X,Y] :
( subclass(X,Y)
<=> ! [U] :
( member(U,X)
=> member(U,Y) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',subclass_defn) ).
fof(f0_nnf,plain,
! [X,Y] :
( ( ? [U] :
( ~ member(U,Y)
& member(U,X) )
| subclass(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(sk0(X,Y),Y)
& member(sk0(X,Y),X) )
| subclass(X,Y) )
& ( member(U,Y)
| ~ member(U,X)
| ~ subclass(X,Y) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0])],[f0_nnf]) ).
cnf(c0,plain,
( member(X2,X1)
| ~ member(X2,X0)
| ~ subclass(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(hi0,axiom,
ifeq(subclass(X0,X1),true,ifeq(member(X2,X0),true,member(X2,X1),true),true) = true,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(h4084,plain,
member(sk8,or(false,universal_class)) = true,
inference(hyper_resolution,[status(thm)],[hi0,h131,hi89]) ).
cnf(hi104,axiom,
or(X0,false) = X0,
introduced(definition) ).
cnf(h142,plain,
subclass(V0,or(V0,false)) = true,
inference(hyper_resolution,[status(thm)],[hi5,hi104]) ).
cnf(t82,plain,
member(sk8,or(or(false,universal_class),false)) = true,
inference(hyper_resolution,[status(thm)],[hi0,h142,h4084]) ).
cnf(t10,plain,
or(X1,false) = X1,
introduced(definition) ).
cnf(t256,plain,
or(X1,false) = X1,
inference(orient,[status(thm)],[t10]) ).
cnf(t9787,plain,
member(sk8,or(false,universal_class)) = true,
inference(step,[status(thm)],[t82,t256]) ).
cnf(t12,plain,
or(false,X1) = X1,
introduced(definition) ).
cnf(t257,plain,
or(false,X1) = X1,
inference(orient,[status(thm)],[t12]) ).
cnf(t9788,plain,
member(sk8,universal_class) = true,
inference(step,[status(thm)],[t9787,t257]) ).
cnf(t347,plain,
member(sk8,universal_class) = true,
inference(orient,[status(thm)],[t9788]) ).
cnf(t10233,plain,
member_of(sk7) = ifeq(true,true,ifeq(member(member_of(sk7),universal_class),true,second(ordered_pair(sk8,sk8)),member_of(sk7)),member_of(sk7)),
inference(step,[status(thm)],[t9597,t347]) ).
cnf(t28,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t258,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t28]) ).
cnf(t10234,plain,
member_of(sk7) = ifeq(member(member_of(sk7),universal_class),true,second(ordered_pair(sk8,sk8)),member_of(sk7)),
inference(step,[status(thm)],[t10233,t258]) ).
fof(f43,axiom,
! [Y] :
( member(Y,universal_class)
=> member(member_of(singleton(Y)),universal_class) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',member_singleton_universal) ).
fof(f43_nnf,plain,
! [Y] :
( member(member_of(singleton(Y)),universal_class)
| ~ member(Y,universal_class) ),
inference(nnf_transformation,[status(thm)],[f43]) ).
fof(f43_sk,plain,
! [Y] :
( member(member_of(singleton(Y)),universal_class)
| ~ member(Y,universal_class) ),
inference(skolemisation,[status(esa)],[f43_nnf]) ).
cnf(c89,plain,
( member(member_of(singleton(X0)),universal_class)
| ~ member(X0,universal_class) ),
inference(cnf_transformation,[status(esa)],[f43_sk]) ).
cnf(t145,plain,
ifeq(member(X1,universal_class),true,member(member_of(singleton(X1)),universal_class),true) = true,
inference(equality_encoding,[status(esa)],[c89]) ).
cnf(t600,plain,
ifeq(member(X1,universal_class),true,member(member_of(singleton(X1)),universal_class),true) = true,
inference(orient,[status(thm)],[t145]) ).
cnf(t604,plain,
true = ifeq(true,true,member(member_of(singleton(sk8)),universal_class),true),
inference(cp,[status(thm)],[t600,t347]) ).
cnf(t9956,plain,
true = member(member_of(singleton(sk8)),universal_class),
inference(step,[status(thm)],[t604,t258]) ).
cnf(t9957,plain,
true = member(member_of(sk7),universal_class),
inference(step,[status(thm)],[t9956,t271]) ).
cnf(t1905,plain,
member(member_of(sk7),universal_class) = true,
inference(orient,[status(thm)],[t9957]) ).
cnf(t10235,plain,
member_of(sk7) = ifeq(true,true,second(ordered_pair(sk8,sk8)),member_of(sk7)),
inference(step,[status(thm)],[t10234,t1905]) ).
cnf(t10236,plain,
member_of(sk7) = second(ordered_pair(sk8,sk8)),
inference(step,[status(thm)],[t10235,t258]) ).
cnf(hi18,axiom,
ifeq(member(X0,universal_class),true,ifeq(member(X1,universal_class),true,second(ordered_pair(X0,X1)),X1),X1) = X1,
inference(equality_encoding,[status(esa)],[c18]) ).
cnf(hi13,axiom,
ordered_pair(X0,X1) = unordered_pair(singleton(X0),unordered_pair(X0,singleton(X1))),
inference(equality_encoding,[status(esa)],[c13]) ).
cnf(t139,plain,
second(unordered_pair(unordered_pair(sk8,sk8),unordered_pair(sk8,unordered_pair(sk8,sk8)))) = sk8,
inference(hyper_resolution,[status(thm)],[hi18,hi89,hi89,hi13,hi14]) ).
cnf(t9806,plain,
second(unordered_pair(singleton(sk8),unordered_pair(sk8,unordered_pair(sk8,sk8)))) = sk8,
inference(step,[status(thm)],[t139,t264]) ).
cnf(t9807,plain,
second(unordered_pair(sk7,unordered_pair(sk8,unordered_pair(sk8,sk8)))) = sk8,
inference(step,[status(thm)],[t9806,t271]) ).
cnf(t9808,plain,
second(unordered_pair(sk7,unordered_pair(sk8,singleton(sk8)))) = sk8,
inference(step,[status(thm)],[t9807,t264]) ).
cnf(t9809,plain,
second(unordered_pair(sk7,unordered_pair(sk8,sk7))) = sk8,
inference(step,[status(thm)],[t9808,t271]) ).
cnf(t1170,plain,
second(unordered_pair(sk7,unordered_pair(sk8,sk7))) = sk8,
inference(orient,[status(thm)],[t9809]) ).
cnf(t10228,plain,
second(ordered_pair(sk8,sk8)) = sk8,
inference(step,[status(thm)],[t1170,t9559]) ).
cnf(t9566,plain,
second(ordered_pair(sk8,sk8)) = sk8,
inference(rw,[status(thm)],[t10228]) ).
cnf(t9570,plain,
second(ordered_pair(sk8,sk8)) = sk8,
inference(orient,[status(thm)],[t9566]) ).
cnf(t10237,plain,
member_of(sk7) = sk8,
inference(step,[status(thm)],[t10236,t9570]) ).
cnf(t9613,plain,
member_of(sk7) = sk8,
inference(orient,[status(thm)],[t10237]) ).
cnf(t10240,plain,
eq(sk8,sk8) = false,
inference(step,[status(thm)],[t1258,t9613]) ).
cnf(t6,plain,
eq(X1,X1) = true,
introduced(definition) ).
cnf(t1157,plain,
eq(X1,X1) = true,
inference(orient,[status(thm)],[t6]) ).
cnf(t10241,plain,
true = false,
inference(step,[status(thm)],[t10240,t1157]) ).
cnf(t9616,plain,
true = false,
inference(rw,[status(thm)],[t10241]) ).
cnf(t9619,plain,
false = true,
inference(orient,[status(thm)],[t9616]) ).
fof(f13,axiom,
! [X,Z] :
( member(Z,complement(X))
<=> ( ~ member(Z,X)
& member(Z,universal_class) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',complement) ).
fof(f13_nnf,plain,
! [X,Z] :
( ( member(Z,X)
| ~ member(Z,universal_class)
| member(Z,complement(X)) )
& ( ( ~ member(Z,X)
& member(Z,universal_class) )
| ~ member(Z,complement(X)) ) ),
inference(nnf_transformation,[status(thm)],[f13]) ).
fof(f13_sk,plain,
! [Z,X] :
( ( member(Z,X)
| ~ member(Z,universal_class)
| member(Z,complement(X)) )
& ( ( ~ member(Z,X)
& member(Z,universal_class) )
| ~ member(Z,complement(X)) ) ),
inference(skolemisation,[status(esa)],[f13_nnf]) ).
cnf(c28,plain,
( ~ member(X1,X0)
| ~ member(X1,complement(X0)) ),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
fof(f15,axiom,
! [X] : ~ member(X,null_class),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',null_class_defn) ).
fof(f15_nnf,plain,
! [X] : ~ member(X,null_class),
inference(nnf_transformation,[status(thm)],[f15]) ).
fof(f15_sk,plain,
! [X] : ~ member(X,null_class),
inference(skolemisation,[status(esa)],[f15_nnf]) ).
cnf(c31,plain,
~ member(X0,null_class),
inference(cnf_transformation,[status(esa)],[f15_sk]) ).
fof(f16,axiom,
! [X,Z] :
( member(Z,domain_of(X))
<=> ( restrict(X,singleton(Z),universal_class) != null_class
& member(Z,universal_class) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',domain_of) ).
fof(f16_nnf,plain,
! [X,Z] :
( ( restrict(X,singleton(Z),universal_class) = null_class
| ~ member(Z,universal_class)
| member(Z,domain_of(X)) )
& ( ( restrict(X,singleton(Z),universal_class) != null_class
& member(Z,universal_class) )
| ~ member(Z,domain_of(X)) ) ),
inference(nnf_transformation,[status(thm)],[f16]) ).
fof(f16_sk,plain,
! [Z,X] :
( ( restrict(X,singleton(Z),universal_class) = null_class
| ~ member(Z,universal_class)
| member(Z,domain_of(X)) )
& ( ( restrict(X,singleton(Z),universal_class) != null_class
& member(Z,universal_class) )
| ~ member(Z,domain_of(X)) ) ),
inference(skolemisation,[status(esa)],[f16_nnf]) ).
cnf(c33,plain,
( restrict(X0,singleton(X1),universal_class) != null_class
| ~ member(X1,domain_of(X0)) ),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
fof(f39,axiom,
! [X,Y] :
( disjoint(X,Y)
<=> ! [U] :
~ ( member(U,Y)
& member(U,X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',disjoint_defn) ).
fof(f39_nnf,plain,
! [X,Y] :
( ( ? [U] :
( member(U,Y)
& member(U,X) )
| disjoint(X,Y) )
& ( ! [U] :
( ~ member(U,Y)
| ~ member(U,X) )
| ~ disjoint(X,Y) ) ),
inference(nnf_transformation,[status(thm)],[f39]) ).
fof(f39_sk,plain,
! [X,Y,U] :
( ( ( member(sk4(X,Y),Y)
& member(sk4(X,Y),X) )
| disjoint(X,Y) )
& ( ~ member(U,Y)
| ~ member(U,X)
| ~ disjoint(X,Y) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk4])],[f39_nnf]) ).
cnf(c80,plain,
( ~ member(X2,X1)
| ~ member(X2,X0)
| ~ disjoint(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f39_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c28,c31,c33,c80,c95]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t9619]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SET090+1 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.08/0.37 % Computer : n009.cluster.edu
% 0.08/0.37 % Model : x86_64 x86_64
% 0.08/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.37 % Memory : 8046.5625MB
% 0.08/0.37 % OS : Linux 6.8.0-71-generic
% 0.08/0.37 % CPULimit : 300
% 0.08/0.37 % WCLimit : 300
% 0.08/0.37 % DateTime : Thu Sep 24 09:43:14 UTC 2026
% 0.08/0.37 % CPUTime :
% 0.08/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 64.52/9.22 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 64.52/9.22 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------