%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SET081-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 : n003.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:03 PM UTC 2026
% Result : Unsatisfiable 11.46s 6.95s
% Output : Proof 11.46s
% Verified :
% SZS Type : Refutation
% Derivation depth : 36
% Number of leaves : 19
% Syntax : Number of formulae : 123 ( 91 unt; 0 def)
% Number of atoms : 163 ( 103 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 115 ( 75 ~; 40 |; 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 : 20 ( 20 usr; 9 con; 0-4 aty)
% Number of variables : 169 ( 30 sgn 50 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(t131,axiom,
sF1 = ifeq(y,x,false,true),
introduced(definition) ).
cnf(t130,axiom,
sF0 = eq(y,x),
introduced(definition) ).
cnf(f125,negated_conjecture,
y != x,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_only_member_in_singleton_2) ).
fof(f125_nnf,plain,
y != x,
inference(nnf_transformation,[status(thm)],[f125]) ).
fof(f125_sk,plain,
y != x,
inference(skolemisation,[status(esa)],[f125_nnf]) ).
cnf(c125,plain,
y != x,
inference(cnf_transformation,[status(esa)],[f125_sk]) ).
cnf(t5,plain,
eq(y,x) = false,
inference(equality_encoding,[status(esa)],[c125]) ).
cnf(t139,plain,
eq(y,x) = false,
inference(orient,[status(thm)],[t5]) ).
cnf(t3673,plain,
sF0 = false,
inference(step,[status(thm)],[t130,t139]) ).
cnf(t150,plain,
false = sF0,
inference(orient,[status(thm)],[t3673]) ).
cnf(t3686,plain,
sF1 = ifeq(y,x,sF0,true),
inference(step,[status(thm)],[t131,t150]) ).
cnf(t17,plain,
ifeq(y,x,false,true) = true,
inference(equality_encoding,[status(esa)],[c125]) ).
cnf(t3683,plain,
ifeq(y,x,sF0,true) = true,
inference(step,[status(thm)],[t17,t150]) ).
cnf(t165,plain,
ifeq(y,x,sF0,true) = true,
inference(orient,[status(thm)],[t3683]) ).
cnf(t3687,plain,
sF1 = true,
inference(step,[status(thm)],[t3686,t165]) ).
cnf(t175,plain,
true = sF1,
inference(orient,[status(thm)],[t3687]) ).
cnf(t3677,plain,
eq(y,x) = sF0,
inference(step,[status(thm)],[t139,t150]) ).
cnf(t154,plain,
eq(y,x) = sF0,
inference(orient,[status(thm)],[t3677]) ).
cnf(f7,axiom,
( U = Y
| U = X
| ~ member(U,unordered_pair(X,Y)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unordered_pair_member) ).
fof(f7_nnf,plain,
! [U,X,Y] :
( U = Y
| U = X
| ~ member(U,unordered_pair(X,Y)) ),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [U,X,Y] :
( U = Y
| U = X
| ~ member(U,unordered_pair(X,Y)) ),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c7,plain,
( X0 = X2
| X0 = X1
| ~ member(X0,unordered_pair(X1,X2)) ),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(t81,plain,
ifeq(member(X1,unordered_pair(X2,X3)),true,or(eq(X1,X2),eq(X1,X3)),true) = true,
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(t4046,plain,
ifeq(member(X1,unordered_pair(X2,X3)),sF1,or(eq(X1,X2),eq(X1,X3)),true) = true,
inference(step,[status(thm)],[t81,t175]) ).
cnf(t4047,plain,
ifeq(member(X1,unordered_pair(X2,X3)),sF1,or(eq(X1,X2),eq(X1,X3)),sF1) = true,
inference(step,[status(thm)],[t4046,t175]) ).
cnf(t4048,plain,
ifeq(member(X1,unordered_pair(X2,X3)),sF1,or(eq(X1,X2),eq(X1,X3)),sF1) = sF1,
inference(step,[status(thm)],[t4047,t175]) ).
cnf(t1246,plain,
ifeq(member(X1,unordered_pair(X2,X3)),sF1,or(eq(X1,X2),eq(X1,X3)),sF1) = sF1,
inference(orient,[status(thm)],[t4048]) ).
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(t83,plain,
ifeq(subclass(X1,X2),true,ifeq(member(X3,X1),true,member(X3,X2),true),true) = true,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t4074,plain,
ifeq(subclass(X1,X2),sF1,ifeq(member(X3,X1),true,member(X3,X2),true),true) = true,
inference(step,[status(thm)],[t83,t175]) ).
cnf(t4075,plain,
ifeq(subclass(X1,X2),sF1,ifeq(member(X3,X1),sF1,member(X3,X2),true),true) = true,
inference(step,[status(thm)],[t4074,t175]) ).
cnf(t4076,plain,
ifeq(subclass(X1,X2),sF1,ifeq(member(X3,X1),sF1,member(X3,X2),sF1),true) = true,
inference(step,[status(thm)],[t4075,t175]) ).
cnf(t4077,plain,
ifeq(subclass(X1,X2),sF1,ifeq(member(X3,X1),sF1,member(X3,X2),sF1),sF1) = true,
inference(step,[status(thm)],[t4076,t175]) ).
cnf(t4078,plain,
ifeq(subclass(X1,X2),sF1,ifeq(member(X3,X1),sF1,member(X3,X2),sF1),sF1) = sF1,
inference(step,[status(thm)],[t4077,t175]) ).
cnf(t1361,plain,
ifeq(subclass(X1,X2),sF1,ifeq(member(X3,X1),sF1,member(X3,X2),sF1),sF1) = sF1,
inference(orient,[status(thm)],[t4078]) ).
cnf(f124,negated_conjecture,
member(y,singleton(x)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_only_member_in_singleton_1) ).
fof(f124_nnf,plain,
member(y,singleton(x)),
inference(nnf_transformation,[status(thm)],[f124]) ).
cnf(c124,plain,
member(y,singleton(x)),
inference(cnf_transformation,[status(esa)],[f124_nnf]) ).
cnf(u16,axiom,
member(y,singleton(x)) = true,
inference(equality_encoding,[status(esa)],[c124]) ).
cnf(f11,axiom,
unordered_pair(X,X) = singleton(X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',singleton_set) ).
fof(f11_nnf,plain,
! [X] : unordered_pair(X,X) = singleton(X),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [X] : unordered_pair(X,X) = singleton(X),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c11,plain,
unordered_pair(X0,X0) = singleton(X0),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(d0,axiom,
unordered_pair(X0,X0) = singleton(X0),
inference(equality_encoding,[status(esa)],[c11]) ).
cnf(t21,plain,
member(y,unordered_pair(x,x)) = true,
inference(definition_unfolding,[status(thm)],[u16,d0]) ).
cnf(t132,axiom,
sF2 = unordered_pair(x,x),
introduced(definition) ).
cnf(t161,plain,
unordered_pair(x,x) = sF2,
inference(orient,[status(thm)],[t132]) ).
cnf(t3685,plain,
member(y,sF2) = true,
inference(step,[status(thm)],[t21,t161]) ).
cnf(t172,plain,
member(y,sF2) = true,
inference(orient,[status(thm)],[t3685]) ).
cnf(t3713,plain,
member(y,sF2) = sF1,
inference(step,[status(thm)],[t172,t175]) ).
cnf(t204,plain,
member(y,sF2) = sF1,
inference(orient,[status(thm)],[t3713]) ).
cnf(t1373,plain,
sF1 = ifeq(subclass(sF2,X1),sF1,ifeq(sF1,sF1,member(y,X1),sF1),sF1),
inference(cp,[status(thm)],[t1361,t204]) ).
cnf(t16,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t164,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t16]) ).
cnf(t4327,plain,
sF1 = ifeq(subclass(sF2,X1),sF1,member(y,X1),sF1),
inference(step,[status(thm)],[t1373,t164]) ).
cnf(t3162,plain,
ifeq(subclass(sF2,X1),sF1,member(y,X1),sF1) = sF1,
inference(orient,[status(thm)],[t4327]) ).
cnf(f108,axiom,
subclass(singleton(X),unordered_pair(X,Y)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',singleton_in_unordered_pair1) ).
fof(f108_nnf,plain,
! [X,Y] : subclass(singleton(X),unordered_pair(X,Y)),
inference(nnf_transformation,[status(thm)],[f108]) ).
fof(f108_sk,plain,
! [X,Y] : subclass(singleton(X),unordered_pair(X,Y)),
inference(skolemisation,[status(esa)],[f108_nnf]) ).
cnf(c108,plain,
subclass(singleton(X0),unordered_pair(X0,X1)),
inference(cnf_transformation,[status(esa)],[f108_sk]) ).
cnf(u8,axiom,
subclass(singleton(X0),unordered_pair(X0,X1)) = true,
inference(equality_encoding,[status(esa)],[c108]) ).
cnf(t36,plain,
subclass(unordered_pair(X1,X1),unordered_pair(X1,X2)) = true,
inference(definition_unfolding,[status(thm)],[u8,d0]) ).
cnf(t3746,plain,
subclass(unordered_pair(X1,X1),unordered_pair(X1,X2)) = sF1,
inference(step,[status(thm)],[t36,t175]) ).
cnf(t249,plain,
subclass(unordered_pair(X1,X1),unordered_pair(X1,X2)) = sF1,
inference(orient,[status(thm)],[t3746]) ).
cnf(t250,plain,
sF1 = subclass(sF2,unordered_pair(x,X1)),
inference(cp,[status(thm)],[t249,t161]) ).
cnf(t254,plain,
subclass(sF2,unordered_pair(x,X1)) = sF1,
inference(orient,[status(thm)],[t250]) ).
cnf(t3164,plain,
sF1 = ifeq(sF1,sF1,member(y,unordered_pair(x,X1)),sF1),
inference(cp,[status(thm)],[t3162,t254]) ).
cnf(t4328,plain,
sF1 = member(y,unordered_pair(x,X1)),
inference(step,[status(thm)],[t3164,t164]) ).
cnf(t3174,plain,
member(y,unordered_pair(x,X1)) = sF1,
inference(orient,[status(thm)],[t4328]) ).
cnf(t3177,plain,
sF1 = ifeq(sF1,sF1,or(eq(y,x),eq(y,X1)),sF1),
inference(cp,[status(thm)],[t1246,t3174]) ).
cnf(t4329,plain,
sF1 = or(eq(y,x),eq(y,X1)),
inference(step,[status(thm)],[t3177,t164]) ).
cnf(t4330,plain,
sF1 = or(sF0,eq(y,X1)),
inference(step,[status(thm)],[t4329,t154]) ).
cnf(t11,plain,
or(false,X1) = X1,
introduced(definition) ).
cnf(t145,plain,
or(false,X1) = X1,
inference(orient,[status(thm)],[t11]) ).
cnf(t3682,plain,
or(sF0,X1) = X1,
inference(step,[status(thm)],[t145,t150]) ).
cnf(t159,plain,
or(sF0,X1) = X1,
inference(rw,[status(thm)],[t3682]) ).
cnf(t163,plain,
or(sF0,X1) = X1,
inference(orient,[status(thm)],[t159]) ).
cnf(t4331,plain,
sF1 = eq(y,X1),
inference(step,[status(thm)],[t4330,t163]) ).
cnf(t3183,plain,
eq(y,X1) = sF1,
inference(orient,[status(thm)],[t4331]) ).
cnf(t4332,plain,
sF1 = sF0,
inference(step,[status(thm)],[t154,t3183]) ).
cnf(t3184,plain,
sF1 = sF0,
inference(rw,[status(thm)],[t4332]) ).
cnf(t3191,plain,
sF1 = sF0,
inference(orient,[status(thm)],[t3184]) ).
cnf(t4364,plain,
true = sF0,
inference(step,[status(thm)],[t175,t3191]) ).
cnf(t3220,plain,
true = sF0,
inference(orient,[status(thm)],[t4364]) ).
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(f101,axiom,
~ member(Y,intersection(complement(X),X)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',special_classes_lemma) ).
fof(f101_nnf,plain,
! [Y,X] : ~ member(Y,intersection(complement(X),X)),
inference(nnf_transformation,[status(thm)],[f101]) ).
fof(f101_sk,plain,
! [Y,X] : ~ member(Y,intersection(complement(X),X)),
inference(skolemisation,[status(esa)],[f101_nnf]) ).
cnf(c101,plain,
~ member(X0,intersection(complement(X1),X1)),
inference(cnf_transformation,[status(esa)],[f101_sk]) ).
cnf(f102,axiom,
~ member(Z,null_class),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',existence_of_null_class) ).
fof(f102_nnf,plain,
! [Z] : ~ member(Z,null_class),
inference(nnf_transformation,[status(thm)],[f102]) ).
fof(f102_sk,plain,
! [Z] : ~ member(Z,null_class),
inference(skolemisation,[status(esa)],[f102_nnf]) ).
cnf(c102,plain,
~ member(X0,null_class),
inference(cnf_transformation,[status(esa)],[f102_sk]) ).
cnf(f115,axiom,
( unordered_pair(X,Y) != null_class
| ~ member(X,universal_class) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',corollary_to_unordered_pair_axiom1) ).
fof(f115_nnf,plain,
! [X,Y] :
( unordered_pair(X,Y) != null_class
| ~ member(X,universal_class) ),
inference(nnf_transformation,[status(thm)],[f115]) ).
fof(f115_sk,plain,
! [X,Y] :
( unordered_pair(X,Y) != null_class
| ~ member(X,universal_class) ),
inference(skolemisation,[status(esa)],[f115_nnf]) ).
cnf(c115,plain,
( unordered_pair(X0,X1) != null_class
| ~ member(X0,universal_class) ),
inference(cnf_transformation,[status(esa)],[f115_sk]) ).
cnf(f116,axiom,
( unordered_pair(X,Y) != null_class
| ~ member(Y,universal_class) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',corollary_to_unordered_pair_axiom2) ).
fof(f116_nnf,plain,
! [Y,X] :
( unordered_pair(X,Y) != null_class
| ~ member(Y,universal_class) ),
inference(nnf_transformation,[status(thm)],[f116]) ).
fof(f116_sk,plain,
! [Y,X] :
( unordered_pair(X,Y) != null_class
| ~ member(Y,universal_class) ),
inference(skolemisation,[status(esa)],[f116_nnf]) ).
cnf(c116,plain,
( unordered_pair(X1,X0) != null_class
| ~ member(X0,universal_class) ),
inference(cnf_transformation,[status(esa)],[f116_sk]) ).
cnf(f117,axiom,
( unordered_pair(X,Y) != null_class
| ~ member(ordered_pair(X,Y),cross_product(U,V)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',corollary_to_unordered_pair_axiom3) ).
fof(f117_nnf,plain,
! [X,Y,U,V] :
( unordered_pair(X,Y) != null_class
| ~ member(ordered_pair(X,Y),cross_product(U,V)) ),
inference(nnf_transformation,[status(thm)],[f117]) ).
fof(f117_sk,plain,
! [X,Y,U,V] :
( unordered_pair(X,Y) != null_class
| ~ member(ordered_pair(X,Y),cross_product(U,V)) ),
inference(skolemisation,[status(esa)],[f117_nnf]) ).
cnf(c117,plain,
( unordered_pair(X0,X1) != null_class
| ~ member(ordered_pair(X0,X1),cross_product(X2,X3)) ),
inference(cnf_transformation,[status(esa)],[f117_sk]) ).
cnf(f122,axiom,
( singleton(X) != null_class
| ~ member(X,universal_class) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',corollary_to_set_in_its_singleton) ).
fof(f122_nnf,plain,
! [X] :
( singleton(X) != null_class
| ~ member(X,universal_class) ),
inference(nnf_transformation,[status(thm)],[f122]) ).
fof(f122_sk,plain,
! [X] :
( singleton(X) != null_class
| ~ member(X,universal_class) ),
inference(skolemisation,[status(esa)],[f122_nnf]) ).
cnf(c122,plain,
( singleton(X0) != null_class
| ~ member(X0,universal_class) ),
inference(cnf_transformation,[status(esa)],[f122_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c23,c29,c101,c102,c115,c116,c117,c122,c125]) ).
cnf(g0_0,plain,
sF0 != false,
inference(rw,[status(thm)],[goal_0,t3220]) ).
cnf(g0_1,plain,
sF0 != sF0,
inference(rw,[status(thm)],[g0_0,t150]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET081-7 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.08/5.36 % Computer : n003.cluster.edu
% 0.08/5.36 % Model : x86_64 x86_64
% 0.08/5.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/5.36 % Memory : 8046.5625MB
% 0.08/5.36 % OS : Linux 6.8.0-71-generic
% 0.08/5.37 % CPULimit : 300
% 0.08/5.37 % WCLimit : 300
% 0.08/5.37 % DateTime : Thu Sep 24 09:41:26 UTC 2026
% 0.08/5.37 % CPUTime :
% 0.08/5.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 11.46/6.95 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 11.46/6.95 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------