%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : NUM180-1 : TPTP v9.3.1. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n011.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:18:45 PM UTC 2026
% Result : Unsatisfiable 7.12s 1.49s
% Output : Proof 7.12s
% Verified :
% Comments :
%------------------------------------------------------------------------------
cnf(t152,axiom,
sF1 = ifeq(subclass(limit_ordinals,ordinal_numbers),true,false,true),
introduced(definition) ).
cnf(f158,negated_conjecture,
~ subclass(limit_ordinals,ordinal_numbers),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_limit_ordinals_are_ordinals_1) ).
fof(f158_nnf,plain,
~ subclass(limit_ordinals,ordinal_numbers),
inference(nnf_transformation,[status(thm)],[f158]) ).
fof(f158_sk,plain,
~ subclass(limit_ordinals,ordinal_numbers),
inference(skolemisation,[status(esa)],[f158_nnf]) ).
cnf(c158,plain,
~ subclass(limit_ordinals,ordinal_numbers),
inference(cnf_transformation,[status(esa)],[f158_sk]) ).
cnf(t11,plain,
subclass(limit_ordinals,ordinal_numbers) = false,
inference(equality_encoding,[status(esa)],[c158]) ).
cnf(t164,plain,
subclass(limit_ordinals,ordinal_numbers) = false,
inference(orient,[status(thm)],[t11]) ).
cnf(t151,axiom,
sF0 = subclass(limit_ordinals,ordinal_numbers),
introduced(definition) ).
cnf(t763,plain,
sF0 = false,
inference(step,[status(thm)],[t151,t164]) ).
cnf(t165,plain,
false = sF0,
inference(orient,[status(thm)],[t763]) ).
cnf(t769,plain,
subclass(limit_ordinals,ordinal_numbers) = sF0,
inference(step,[status(thm)],[t164,t165]) ).
cnf(t171,plain,
subclass(limit_ordinals,ordinal_numbers) = sF0,
inference(orient,[status(thm)],[t769]) ).
cnf(t775,plain,
sF1 = ifeq(sF0,true,false,true),
inference(step,[status(thm)],[t152,t171]) ).
cnf(t776,plain,
sF1 = ifeq(sF0,true,sF0,true),
inference(step,[status(thm)],[t775,t165]) ).
cnf(t28,plain,
ifeq(subclass(limit_ordinals,ordinal_numbers),true,false,true) = true,
inference(equality_encoding,[status(esa)],[c158]) ).
cnf(t773,plain,
ifeq(sF0,true,false,true) = true,
inference(step,[status(thm)],[t28,t171]) ).
cnf(t774,plain,
ifeq(sF0,true,sF0,true) = true,
inference(step,[status(thm)],[t773,t165]) ).
cnf(t222,plain,
ifeq(sF0,true,sF0,true) = true,
inference(orient,[status(thm)],[t774]) ).
cnf(t777,plain,
sF1 = true,
inference(step,[status(thm)],[t776,t222]) ).
cnf(t234,plain,
true = sF1,
inference(orient,[status(thm)],[t777]) ).
cnf(f2,axiom,
( subclass(X,Y)
| ~ member(not_subclass_element(X,Y),Y) ),
file('/export/starexec/sandbox2/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(t63,plain,
ifeq(member(not_subclass_element(X1,X2),X2),true,subclass(X1,X2),true) = true,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t935,plain,
ifeq(member(not_subclass_element(X1,X2),X2),sF1,subclass(X1,X2),true) = true,
inference(step,[status(thm)],[t63,t234]) ).
cnf(t936,plain,
ifeq(member(not_subclass_element(X1,X2),X2),sF1,subclass(X1,X2),sF1) = true,
inference(step,[status(thm)],[t935,t234]) ).
cnf(t937,plain,
ifeq(member(not_subclass_element(X1,X2),X2),sF1,subclass(X1,X2),sF1) = sF1,
inference(step,[status(thm)],[t936,t234]) ).
cnf(t570,plain,
ifeq(member(not_subclass_element(X1,X2),X2),sF1,subclass(X1,X2),sF1) = sF1,
inference(orient,[status(thm)],[t937]) ).
cnf(t572,plain,
sF1 = ifeq(member(not_subclass_element(limit_ordinals,ordinal_numbers),ordinal_numbers),sF1,sF0,sF1),
inference(cp,[status(thm)],[t570,t171]) ).
cnf(f21,axiom,
( member(Z,Y)
| ~ member(Z,intersection(X,Y)) ),
file('/export/starexec/sandbox2/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(t58,plain,
ifeq(member(X1,intersection(X2,X3)),true,member(X1,X3),true) = true,
inference(equality_encoding,[status(esa)],[c21]) ).
cnf(t899,plain,
ifeq(member(X1,intersection(X2,X3)),sF1,member(X1,X3),true) = true,
inference(step,[status(thm)],[t58,t234]) ).
cnf(t900,plain,
ifeq(member(X1,intersection(X2,X3)),sF1,member(X1,X3),sF1) = true,
inference(step,[status(thm)],[t899,t234]) ).
cnf(t901,plain,
ifeq(member(X1,intersection(X2,X3)),sF1,member(X1,X3),sF1) = sF1,
inference(step,[status(thm)],[t900,t234]) ).
cnf(t476,plain,
ifeq(member(X1,intersection(X2,X3)),sF1,member(X1,X3),sF1) = sF1,
inference(orient,[status(thm)],[t901]) ).
cnf(f138,axiom,
intersection(complement(kind_1_ordinals),ordinal_numbers) = limit_ordinals,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',limit_ordinals) ).
fof(f138_nnf,plain,
intersection(complement(kind_1_ordinals),ordinal_numbers) = limit_ordinals,
inference(nnf_transformation,[status(thm)],[f138]) ).
cnf(c138,plain,
intersection(complement(kind_1_ordinals),ordinal_numbers) = limit_ordinals,
inference(cnf_transformation,[status(esa)],[f138_nnf]) ).
cnf(t12,plain,
intersection(complement(kind_1_ordinals),ordinal_numbers) = limit_ordinals,
inference(equality_encoding,[status(esa)],[c138]) ).
cnf(t176,plain,
intersection(complement(kind_1_ordinals),ordinal_numbers) = limit_ordinals,
inference(orient,[status(thm)],[t12]) ).
cnf(t478,plain,
sF1 = ifeq(member(X1,limit_ordinals),sF1,member(X1,ordinal_numbers),sF1),
inference(cp,[status(thm)],[t476,t176]) ).
cnf(t489,plain,
ifeq(member(X1,limit_ordinals),sF1,member(X1,ordinal_numbers),sF1) = sF1,
inference(orient,[status(thm)],[t478]) ).
cnf(f1,axiom,
( subclass(X,Y)
| member(not_subclass_element(X,Y),X) ),
file('/export/starexec/sandbox2/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(t51,plain,
or(member(not_subclass_element(X1,X2),X1),subclass(X1,X2)) = true,
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t870,plain,
or(member(not_subclass_element(X1,X2),X1),subclass(X1,X2)) = sF1,
inference(step,[status(thm)],[t51,t234]) ).
cnf(t373,plain,
or(member(not_subclass_element(X1,X2),X1),subclass(X1,X2)) = sF1,
inference(orient,[status(thm)],[t870]) ).
cnf(t374,plain,
sF1 = or(member(not_subclass_element(limit_ordinals,ordinal_numbers),limit_ordinals),sF0),
inference(cp,[status(thm)],[t373,t171]) ).
cnf(t6,plain,
or(X1,false) = X1,
introduced(definition) ).
cnf(t159,plain,
or(X1,false) = X1,
inference(orient,[status(thm)],[t6]) ).
cnf(t767,plain,
or(X1,sF0) = X1,
inference(step,[status(thm)],[t159,t165]) ).
cnf(t169,plain,
or(X1,sF0) = X1,
inference(rw,[status(thm)],[t767]) ).
cnf(t174,plain,
or(X1,sF0) = X1,
inference(orient,[status(thm)],[t169]) ).
cnf(t871,plain,
sF1 = member(not_subclass_element(limit_ordinals,ordinal_numbers),limit_ordinals),
inference(step,[status(thm)],[t374,t174]) ).
cnf(t375,plain,
member(not_subclass_element(limit_ordinals,ordinal_numbers),limit_ordinals) = sF1,
inference(orient,[status(thm)],[t871]) ).
cnf(t490,plain,
sF1 = ifeq(sF1,sF1,member(not_subclass_element(limit_ordinals,ordinal_numbers),ordinal_numbers),sF1),
inference(cp,[status(thm)],[t489,t375]) ).
cnf(t13,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t177,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t13]) ).
cnf(t902,plain,
sF1 = member(not_subclass_element(limit_ordinals,ordinal_numbers),ordinal_numbers),
inference(step,[status(thm)],[t490,t177]) ).
cnf(t491,plain,
member(not_subclass_element(limit_ordinals,ordinal_numbers),ordinal_numbers) = sF1,
inference(orient,[status(thm)],[t902]) ).
cnf(t938,plain,
sF1 = ifeq(sF1,sF1,sF0,sF1),
inference(step,[status(thm)],[t572,t491]) ).
cnf(t939,plain,
sF1 = sF0,
inference(step,[status(thm)],[t938,t177]) ).
cnf(t587,plain,
sF1 = sF0,
inference(orient,[status(thm)],[t939]) ).
cnf(t976,plain,
true = sF0,
inference(step,[status(thm)],[t234,t587]) ).
cnf(t624,plain,
true = sF0,
inference(orient,[status(thm)],[t976]) ).
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(f126,axiom,
( ~ member(ordered_pair(V,least(Xr,U)),Xr)
| ~ member(V,U)
| ~ subclass(U,Y)
| ~ well_ordering(Xr,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',well_ordering5) ).
fof(f126_nnf,plain,
! [Xr,Y,U,V] :
( ~ member(ordered_pair(V,least(Xr,U)),Xr)
| ~ member(V,U)
| ~ subclass(U,Y)
| ~ well_ordering(Xr,Y) ),
inference(nnf_transformation,[status(thm)],[f126]) ).
fof(f126_sk,plain,
! [Xr,Y,U,V] :
( ~ member(ordered_pair(V,least(Xr,U)),Xr)
| ~ member(V,U)
| ~ subclass(U,Y)
| ~ well_ordering(Xr,Y) ),
inference(skolemisation,[status(esa)],[f126_nnf]) ).
cnf(c126,plain,
( ~ member(ordered_pair(X3,least(X0,X2)),X0)
| ~ member(X3,X2)
| ~ subclass(X2,X1)
| ~ well_ordering(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f126_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c23,c29,c126,c158]) ).
cnf(g0_0,plain,
sF0 != false,
inference(rw,[status(thm)],[goal_0,t624]) ).
cnf(g0_1,plain,
sF0 != sF0,
inference(rw,[status(thm)],[g0_0,t165]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM180-1 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.36 % Computer : n011.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Thu Sep 24 03:08:42 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 7.12/1.49 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.12/1.49 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------