%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : NUM183-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:47 PM UTC 2026
% Result : Unsatisfiable 26.69s 3.82s
% Output : Proof 26.69s
% Verified :
% Comments :
%------------------------------------------------------------------------------
cnf(t156,axiom,
sF2 = member(x,ordinal_numbers),
introduced(definition) ).
cnf(f158,negated_conjecture,
member(x,ordinal_numbers),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_ordinals_are_kind_1_or_limit_1) ).
fof(f158_nnf,plain,
member(x,ordinal_numbers),
inference(nnf_transformation,[status(thm)],[f158]) ).
cnf(c158,plain,
member(x,ordinal_numbers),
inference(cnf_transformation,[status(esa)],[f158_nnf]) ).
cnf(t8,plain,
member(x,ordinal_numbers) = true,
inference(equality_encoding,[status(esa)],[c158]) ).
cnf(t167,plain,
member(x,ordinal_numbers) = true,
inference(orient,[status(thm)],[t8]) ).
cnf(t6586,plain,
sF2 = true,
inference(step,[status(thm)],[t156,t167]) ).
cnf(t185,plain,
true = sF2,
inference(orient,[status(thm)],[t6586]) ).
cnf(f22,axiom,
( member(Z,intersection(X,Y))
| ~ member(Z,Y)
| ~ member(Z,X) ),
file('/export/starexec/sandbox2/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(t97,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(t7069,plain,
ifeq(member(X1,X2),sF2,ifeq(member(X1,X3),true,member(X1,intersection(X2,X3)),true),true) = true,
inference(step,[status(thm)],[t97,t185]) ).
cnf(t7070,plain,
ifeq(member(X1,X2),sF2,ifeq(member(X1,X3),sF2,member(X1,intersection(X2,X3)),true),true) = true,
inference(step,[status(thm)],[t7069,t185]) ).
cnf(t7071,plain,
ifeq(member(X1,X2),sF2,ifeq(member(X1,X3),sF2,member(X1,intersection(X2,X3)),sF2),true) = true,
inference(step,[status(thm)],[t7070,t185]) ).
cnf(t7072,plain,
ifeq(member(X1,X2),sF2,ifeq(member(X1,X3),sF2,member(X1,intersection(X2,X3)),sF2),sF2) = true,
inference(step,[status(thm)],[t7071,t185]) ).
cnf(t7073,plain,
ifeq(member(X1,X2),sF2,ifeq(member(X1,X3),sF2,member(X1,intersection(X2,X3)),sF2),sF2) = sF2,
inference(step,[status(thm)],[t7072,t185]) ).
cnf(t1411,plain,
ifeq(member(X1,X2),sF2,ifeq(member(X1,X3),sF2,member(X1,intersection(X2,X3)),sF2),sF2) = sF2,
inference(orient,[status(thm)],[t7073]) ).
cnf(t6596,plain,
member(x,ordinal_numbers) = sF2,
inference(step,[status(thm)],[t167,t185]) ).
cnf(t195,plain,
member(x,ordinal_numbers) = sF2,
inference(orient,[status(thm)],[t6596]) ).
cnf(t1419,plain,
sF2 = ifeq(member(x,X1),sF2,ifeq(sF2,sF2,member(x,intersection(X1,ordinal_numbers)),sF2),sF2),
inference(cp,[status(thm)],[t1411,t195]) ).
cnf(t15,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t209,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t15]) ).
cnf(t7639,plain,
sF2 = ifeq(member(x,X1),sF2,member(x,intersection(X1,ordinal_numbers)),sF2),
inference(step,[status(thm)],[t1419,t209]) ).
cnf(t5641,plain,
ifeq(member(x,X1),sF2,member(x,intersection(X1,ordinal_numbers)),sF2) = sF2,
inference(orient,[status(thm)],[t7639]) ).
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(t14,plain,
intersection(complement(kind_1_ordinals),ordinal_numbers) = limit_ordinals,
inference(equality_encoding,[status(esa)],[c138]) ).
cnf(t206,plain,
intersection(complement(kind_1_ordinals),ordinal_numbers) = limit_ordinals,
inference(orient,[status(thm)],[t14]) ).
cnf(t5644,plain,
sF2 = ifeq(member(x,complement(kind_1_ordinals)),sF2,member(x,limit_ordinals),sF2),
inference(cp,[status(thm)],[t5641,t206]) ).
cnf(f24,axiom,
( member(Z,X)
| member(Z,complement(X))
| ~ member(Z,universal_class) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',complement2) ).
fof(f24_nnf,plain,
! [Z,X] :
( member(Z,X)
| member(Z,complement(X))
| ~ member(Z,universal_class) ),
inference(nnf_transformation,[status(thm)],[f24]) ).
fof(f24_sk,plain,
! [Z,X] :
( member(Z,X)
| member(Z,complement(X))
| ~ member(Z,universal_class) ),
inference(skolemisation,[status(esa)],[f24_nnf]) ).
cnf(c24,plain,
( member(X0,X1)
| member(X0,complement(X1))
| ~ member(X0,universal_class) ),
inference(cnf_transformation,[status(esa)],[f24_sk]) ).
cnf(t75,plain,
ifeq(member(X1,universal_class),true,or(member(X1,complement(X2)),member(X1,X2)),true) = true,
inference(equality_encoding,[status(esa)],[c24]) ).
cnf(t6798,plain,
ifeq(member(X1,universal_class),sF2,or(member(X1,complement(X2)),member(X1,X2)),true) = true,
inference(step,[status(thm)],[t75,t185]) ).
cnf(t6799,plain,
ifeq(member(X1,universal_class),sF2,or(member(X1,complement(X2)),member(X1,X2)),sF2) = true,
inference(step,[status(thm)],[t6798,t185]) ).
cnf(t6800,plain,
ifeq(member(X1,universal_class),sF2,or(member(X1,complement(X2)),member(X1,X2)),sF2) = sF2,
inference(step,[status(thm)],[t6799,t185]) ).
cnf(t668,plain,
ifeq(member(X1,universal_class),sF2,or(member(X1,complement(X2)),member(X1,X2)),sF2) = sF2,
inference(orient,[status(thm)],[t6800]) ).
cnf(f159,negated_conjecture,
~ member(x,kind_1_ordinals),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_ordinals_are_kind_1_or_limit_2) ).
fof(f159_nnf,plain,
~ member(x,kind_1_ordinals),
inference(nnf_transformation,[status(thm)],[f159]) ).
fof(f159_sk,plain,
~ member(x,kind_1_ordinals),
inference(skolemisation,[status(esa)],[f159_nnf]) ).
cnf(c159,plain,
~ member(x,kind_1_ordinals),
inference(cnf_transformation,[status(esa)],[f159_sk]) ).
cnf(t6,plain,
member(x,kind_1_ordinals) = false,
inference(equality_encoding,[status(esa)],[c159]) ).
cnf(t165,plain,
member(x,kind_1_ordinals) = false,
inference(orient,[status(thm)],[t6]) ).
cnf(t154,axiom,
sF0 = member(x,kind_1_ordinals),
introduced(definition) ).
cnf(t6575,plain,
sF0 = false,
inference(step,[status(thm)],[t154,t165]) ).
cnf(t173,plain,
false = sF0,
inference(orient,[status(thm)],[t6575]) ).
cnf(t6579,plain,
member(x,kind_1_ordinals) = sF0,
inference(step,[status(thm)],[t165,t173]) ).
cnf(t177,plain,
member(x,kind_1_ordinals) = sF0,
inference(orient,[status(thm)],[t6579]) ).
cnf(t670,plain,
sF2 = ifeq(member(x,universal_class),sF2,or(member(x,complement(kind_1_ordinals)),sF0),sF2),
inference(cp,[status(thm)],[t668,t177]) ).
cnf(t9,plain,
or(X1,false) = X1,
introduced(definition) ).
cnf(t168,plain,
or(X1,false) = X1,
inference(orient,[status(thm)],[t9]) ).
cnf(t6583,plain,
or(X1,sF0) = X1,
inference(step,[status(thm)],[t168,t173]) ).
cnf(t181,plain,
or(X1,sF0) = X1,
inference(rw,[status(thm)],[t6583]) ).
cnf(t204,plain,
or(X1,sF0) = X1,
inference(orient,[status(thm)],[t181]) ).
cnf(t6854,plain,
sF2 = ifeq(member(x,universal_class),sF2,member(x,complement(kind_1_ordinals)),sF2),
inference(step,[status(thm)],[t670,t204]) ).
cnf(t786,plain,
ifeq(member(x,universal_class),sF2,member(x,complement(kind_1_ordinals)),sF2) = sF2,
inference(orient,[status(thm)],[t6854]) ).
cnf(t1154,plain,
ifeq(sF2,sF2,member(x,complement(kind_1_ordinals)),sF2) = sF2,
inference(rw,[status(thm)],[t786]) ).
cnf(t7016,plain,
member(x,complement(kind_1_ordinals)) = sF2,
inference(step,[status(thm)],[t1154,t209]) ).
cnf(t1267,plain,
member(x,complement(kind_1_ordinals)) = sF2,
inference(orient,[status(thm)],[t7016]) ).
cnf(t7640,plain,
sF2 = ifeq(sF2,sF2,member(x,limit_ordinals),sF2),
inference(step,[status(thm)],[t5644,t1267]) ).
cnf(t7641,plain,
sF2 = member(x,limit_ordinals),
inference(step,[status(thm)],[t7640,t209]) ).
cnf(f160,negated_conjecture,
~ member(x,limit_ordinals),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_ordinals_are_kind_1_or_limit_3) ).
fof(f160_nnf,plain,
~ member(x,limit_ordinals),
inference(nnf_transformation,[status(thm)],[f160]) ).
fof(f160_sk,plain,
~ member(x,limit_ordinals),
inference(skolemisation,[status(esa)],[f160_nnf]) ).
cnf(c160,plain,
~ member(x,limit_ordinals),
inference(cnf_transformation,[status(esa)],[f160_sk]) ).
cnf(t7,plain,
member(x,limit_ordinals) = false,
inference(equality_encoding,[status(esa)],[c160]) ).
cnf(t166,plain,
member(x,limit_ordinals) = false,
inference(orient,[status(thm)],[t7]) ).
cnf(t6581,plain,
member(x,limit_ordinals) = sF0,
inference(step,[status(thm)],[t166,t173]) ).
cnf(t179,plain,
member(x,limit_ordinals) = sF0,
inference(orient,[status(thm)],[t6581]) ).
cnf(t7642,plain,
sF2 = sF0,
inference(step,[status(thm)],[t7641,t179]) ).
cnf(t5752,plain,
sF2 = sF0,
inference(orient,[status(thm)],[t7642]) ).
cnf(t7657,plain,
true = sF0,
inference(step,[status(thm)],[t185,t5752]) ).
cnf(t5767,plain,
true = sF0,
inference(orient,[status(thm)],[t7657]) ).
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,c159,c160]) ).
cnf(g0_0,plain,
sF0 != false,
inference(rw,[status(thm)],[goal_0,t5767]) ).
cnf(g0_1,plain,
sF0 != sF0,
inference(rw,[status(thm)],[g0_0,t173]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM183-1 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.36 % Computer : n011.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Thu Sep 24 03:08:57 UTC 2026
% 0.13/0.36 % CPUTime :
% 0.13/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 26.69/3.82 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 26.69/3.82 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------