%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : NUM139-1 : TPTP v9.3.1. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/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:41 PM UTC 2026
% Result : Unsatisfiable 16.18s 2.56s
% Output : Proof 16.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 23
% Syntax : Number of formulae : 158 ( 138 unt; 0 def)
% Number of atoms : 186 ( 133 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 74 ( 46 ~; 28 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 2 avg)
% Maximal term depth : 11 ( 2 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 31 ( 31 usr; 15 con; 0-4 aty)
% Number of variables : 138 ( 6 sgn 48 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f158,negated_conjecture,
~ member(not_subclass_element(intersection(power_class(x),z),x),z),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_complete_induction3_1) ).
fof(f158_nnf,plain,
~ member(not_subclass_element(intersection(power_class(x),z),x),z),
inference(nnf_transformation,[status(thm)],[f158]) ).
fof(f158_sk,plain,
~ member(not_subclass_element(intersection(power_class(x),z),x),z),
inference(skolemisation,[status(esa)],[f158_nnf]) ).
cnf(c158,plain,
~ member(not_subclass_element(intersection(power_class(x),z),x),z),
inference(cnf_transformation,[status(esa)],[f158_sk]) ).
cnf(u89,axiom,
member(not_subclass_element(intersection(power_class(x),z),x),z) = false,
inference(equality_encoding,[status(esa)],[c158]) ).
cnf(f54,axiom,
complement(image(element_relation,complement(X))) = power_class(X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',power_class_definition) ).
fof(f54_nnf,plain,
! [X] : complement(image(element_relation,complement(X))) = power_class(X),
inference(nnf_transformation,[status(thm)],[f54]) ).
fof(f54_sk,plain,
! [X] : complement(image(element_relation,complement(X))) = power_class(X),
inference(skolemisation,[status(esa)],[f54_nnf]) ).
cnf(c54,plain,
complement(image(element_relation,complement(X0))) = power_class(X0),
inference(cnf_transformation,[status(esa)],[f54_sk]) ).
cnf(u80,axiom,
complement(image(element_relation,complement(X0))) = power_class(X0),
inference(equality_encoding,[status(esa)],[c54]) ).
cnf(f41,axiom,
range_of(restrict(Xr,X,universal_class)) = image(Xr,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',image) ).
fof(f41_nnf,plain,
! [Xr,X] : range_of(restrict(Xr,X,universal_class)) = image(Xr,X),
inference(nnf_transformation,[status(thm)],[f41]) ).
fof(f41_sk,plain,
! [Xr,X] : range_of(restrict(Xr,X,universal_class)) = image(Xr,X),
inference(skolemisation,[status(esa)],[f41_nnf]) ).
cnf(c41,plain,
range_of(restrict(X0,X1,universal_class)) = image(X0,X1),
inference(cnf_transformation,[status(esa)],[f41_sk]) ).
cnf(u50,axiom,
range_of(restrict(X0,X1,universal_class)) = image(X0,X1),
inference(equality_encoding,[status(esa)],[c41]) ).
cnf(f27,axiom,
intersection(Xr,cross_product(X,Y)) = restrict(Xr,X,Y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',restriction1) ).
fof(f27_nnf,plain,
! [Xr,X,Y] : intersection(Xr,cross_product(X,Y)) = restrict(Xr,X,Y),
inference(nnf_transformation,[status(thm)],[f27]) ).
fof(f27_sk,plain,
! [Xr,X,Y] : intersection(Xr,cross_product(X,Y)) = restrict(Xr,X,Y),
inference(skolemisation,[status(esa)],[f27_nnf]) ).
cnf(c27,plain,
intersection(X0,cross_product(X1,X2)) = restrict(X0,X1,X2),
inference(cnf_transformation,[status(esa)],[f27_sk]) ).
cnf(d4,axiom,
intersection(X0,cross_product(X1,X2)) = restrict(X0,X1,X2),
inference(equality_encoding,[status(esa)],[c27]) ).
cnf(f38,axiom,
domain_of(inverse(Z)) = range_of(Z),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',range_of) ).
fof(f38_nnf,plain,
! [Z] : domain_of(inverse(Z)) = range_of(Z),
inference(nnf_transformation,[status(thm)],[f38]) ).
fof(f38_sk,plain,
! [Z] : domain_of(inverse(Z)) = range_of(Z),
inference(skolemisation,[status(esa)],[f38_nnf]) ).
cnf(c38,plain,
domain_of(inverse(X0)) = range_of(X0),
inference(cnf_transformation,[status(esa)],[f38_sk]) ).
cnf(u60,axiom,
domain_of(inverse(X0)) = range_of(X0),
inference(equality_encoding,[status(esa)],[c38]) ).
cnf(f37,axiom,
domain_of(flip(cross_product(Y,universal_class))) = inverse(Y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',inverse) ).
fof(f37_nnf,plain,
! [Y] : domain_of(flip(cross_product(Y,universal_class))) = inverse(Y),
inference(nnf_transformation,[status(thm)],[f37]) ).
fof(f37_sk,plain,
! [Y] : domain_of(flip(cross_product(Y,universal_class))) = inverse(Y),
inference(skolemisation,[status(esa)],[f37_nnf]) ).
cnf(c37,plain,
domain_of(flip(cross_product(X0,universal_class))) = inverse(X0),
inference(cnf_transformation,[status(esa)],[f37_sk]) ).
cnf(d5,axiom,
domain_of(flip(cross_product(X0,universal_class))) = inverse(X0),
inference(equality_encoding,[status(esa)],[c37]) ).
cnf(d6,axiom,
domain_of(domain_of(flip(cross_product(X0,universal_class)))) = range_of(X0),
inference(definition_unfolding,[status(thm)],[u60,d5]) ).
cnf(d9,axiom,
domain_of(domain_of(flip(cross_product(intersection(X0,cross_product(X1,universal_class)),universal_class)))) = image(X0,X1),
inference(definition_unfolding,[status(thm)],[u50,d4,d6]) ).
cnf(d12,axiom,
complement(domain_of(domain_of(flip(cross_product(intersection(element_relation,cross_product(complement(X0),universal_class)),universal_class))))) = power_class(X0),
inference(definition_unfolding,[status(thm)],[u80,d9]) ).
cnf(t98,plain,
member(not_subclass_element(intersection(complement(domain_of(domain_of(flip(cross_product(intersection(element_relation,cross_product(complement(x),universal_class)),universal_class))))),z),x),z) = false,
inference(definition_unfolding,[status(thm)],[u89,d12]) ).
cnf(t153,axiom,
sF0 = complement(x),
introduced(definition) ).
cnf(t171,plain,
complement(x) = sF0,
inference(orient,[status(thm)],[t153]) ).
cnf(t2278,plain,
member(not_subclass_element(intersection(complement(domain_of(domain_of(flip(cross_product(intersection(element_relation,cross_product(sF0,universal_class)),universal_class))))),z),x),z) = false,
inference(step,[status(thm)],[t98,t171]) ).
cnf(t154,axiom,
sF1 = cross_product(complement(x),universal_class),
introduced(definition) ).
cnf(t1919,plain,
sF1 = cross_product(sF0,universal_class),
inference(step,[status(thm)],[t154,t171]) ).
cnf(t180,plain,
cross_product(sF0,universal_class) = sF1,
inference(orient,[status(thm)],[t1919]) ).
cnf(t2279,plain,
member(not_subclass_element(intersection(complement(domain_of(domain_of(flip(cross_product(intersection(element_relation,sF1),universal_class))))),z),x),z) = false,
inference(step,[status(thm)],[t2278,t180]) ).
cnf(f28,axiom,
intersection(cross_product(X,Y),Xr) = restrict(Xr,X,Y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',restriction2) ).
fof(f28_nnf,plain,
! [X,Y,Xr] : intersection(cross_product(X,Y),Xr) = restrict(Xr,X,Y),
inference(nnf_transformation,[status(thm)],[f28]) ).
fof(f28_sk,plain,
! [X,Y,Xr] : intersection(cross_product(X,Y),Xr) = restrict(Xr,X,Y),
inference(skolemisation,[status(esa)],[f28_nnf]) ).
cnf(c28,plain,
intersection(cross_product(X0,X1),X2) = restrict(X2,X0,X1),
inference(cnf_transformation,[status(esa)],[f28_sk]) ).
cnf(u49,axiom,
intersection(cross_product(X0,X1),X2) = restrict(X2,X0,X1),
inference(equality_encoding,[status(esa)],[c28]) ).
cnf(t48,plain,
intersection(cross_product(X1,X2),X3) = intersection(X3,cross_product(X1,X2)),
inference(definition_unfolding,[status(thm)],[u49,d4]) ).
cnf(t294,plain,
intersection(cross_product(X1,X2),X3) = intersection(X3,cross_product(X1,X2)),
inference(orient,[status(thm)],[t48]) ).
cnf(t295,plain,
intersection(X1,cross_product(sF0,universal_class)) = intersection(sF1,X1),
inference(cp,[status(thm)],[t294,t180]) ).
cnf(t1931,plain,
intersection(X1,sF1) = intersection(sF1,X1),
inference(step,[status(thm)],[t295,t180]) ).
cnf(t297,plain,
intersection(X1,sF1) = intersection(sF1,X1),
inference(orient,[status(thm)],[t1931]) ).
cnf(t2280,plain,
member(not_subclass_element(intersection(complement(domain_of(domain_of(flip(cross_product(intersection(sF1,element_relation),universal_class))))),z),x),z) = false,
inference(step,[status(thm)],[t2279,t297]) ).
cnf(t155,axiom,
sF2 = intersection(element_relation,cross_product(complement(x),universal_class)),
introduced(definition) ).
cnf(t1920,plain,
sF2 = intersection(element_relation,cross_product(sF0,universal_class)),
inference(step,[status(thm)],[t155,t171]) ).
cnf(t1921,plain,
sF2 = intersection(element_relation,sF1),
inference(step,[status(thm)],[t1920,t180]) ).
cnf(t193,plain,
intersection(element_relation,sF1) = sF2,
inference(orient,[status(thm)],[t1921]) ).
cnf(t1932,plain,
intersection(sF1,element_relation) = sF2,
inference(step,[status(thm)],[t193,t297]) ).
cnf(t298,plain,
intersection(sF1,element_relation) = sF2,
inference(rw,[status(thm)],[t1932]) ).
cnf(t299,plain,
intersection(sF1,element_relation) = sF2,
inference(orient,[status(thm)],[t298]) ).
cnf(t2281,plain,
member(not_subclass_element(intersection(complement(domain_of(domain_of(flip(cross_product(sF2,universal_class))))),z),x),z) = false,
inference(step,[status(thm)],[t2280,t299]) ).
cnf(t156,axiom,
sF3 = cross_product(intersection(element_relation,cross_product(complement(x),universal_class)),universal_class),
introduced(definition) ).
cnf(t1924,plain,
sF3 = cross_product(intersection(element_relation,cross_product(sF0,universal_class)),universal_class),
inference(step,[status(thm)],[t156,t171]) ).
cnf(t1925,plain,
sF3 = cross_product(intersection(element_relation,sF1),universal_class),
inference(step,[status(thm)],[t1924,t180]) ).
cnf(t1926,plain,
sF3 = cross_product(sF2,universal_class),
inference(step,[status(thm)],[t1925,t193]) ).
cnf(t261,plain,
cross_product(sF2,universal_class) = sF3,
inference(orient,[status(thm)],[t1926]) ).
cnf(t2282,plain,
member(not_subclass_element(intersection(complement(domain_of(domain_of(flip(sF3)))),z),x),z) = false,
inference(step,[status(thm)],[t2281,t261]) ).
cnf(t157,axiom,
sF4 = flip(cross_product(intersection(element_relation,cross_product(complement(x),universal_class)),universal_class)),
introduced(definition) ).
cnf(t1927,plain,
sF4 = flip(cross_product(intersection(element_relation,cross_product(sF0,universal_class)),universal_class)),
inference(step,[status(thm)],[t157,t171]) ).
cnf(t1928,plain,
sF4 = flip(cross_product(intersection(element_relation,sF1),universal_class)),
inference(step,[status(thm)],[t1927,t180]) ).
cnf(t1929,plain,
sF4 = flip(cross_product(sF2,universal_class)),
inference(step,[status(thm)],[t1928,t193]) ).
cnf(t1930,plain,
sF4 = flip(sF3),
inference(step,[status(thm)],[t1929,t261]) ).
cnf(t284,plain,
flip(sF3) = sF4,
inference(orient,[status(thm)],[t1930]) ).
cnf(t2283,plain,
member(not_subclass_element(intersection(complement(domain_of(domain_of(sF4))),z),x),z) = false,
inference(step,[status(thm)],[t2282,t284]) ).
cnf(t158,axiom,
sF5 = domain_of(flip(cross_product(intersection(element_relation,cross_product(complement(x),universal_class)),universal_class))),
introduced(definition) ).
cnf(t1944,plain,
sF5 = domain_of(flip(cross_product(intersection(element_relation,cross_product(sF0,universal_class)),universal_class))),
inference(step,[status(thm)],[t158,t171]) ).
cnf(t1945,plain,
sF5 = domain_of(flip(cross_product(intersection(element_relation,sF1),universal_class))),
inference(step,[status(thm)],[t1944,t180]) ).
cnf(t1946,plain,
sF5 = domain_of(flip(cross_product(intersection(sF1,element_relation),universal_class))),
inference(step,[status(thm)],[t1945,t297]) ).
cnf(t1947,plain,
sF5 = domain_of(flip(cross_product(sF2,universal_class))),
inference(step,[status(thm)],[t1946,t299]) ).
cnf(t1948,plain,
sF5 = domain_of(flip(sF3)),
inference(step,[status(thm)],[t1947,t261]) ).
cnf(t1949,plain,
sF5 = domain_of(sF4),
inference(step,[status(thm)],[t1948,t284]) ).
cnf(t371,plain,
domain_of(sF4) = sF5,
inference(orient,[status(thm)],[t1949]) ).
cnf(t2284,plain,
member(not_subclass_element(intersection(complement(domain_of(sF5)),z),x),z) = false,
inference(step,[status(thm)],[t2283,t371]) ).
cnf(t159,axiom,
sF6 = domain_of(domain_of(flip(cross_product(intersection(element_relation,cross_product(complement(x),universal_class)),universal_class)))),
introduced(definition) ).
cnf(t1968,plain,
sF6 = domain_of(domain_of(flip(cross_product(intersection(element_relation,cross_product(sF0,universal_class)),universal_class)))),
inference(step,[status(thm)],[t159,t171]) ).
cnf(t1969,plain,
sF6 = domain_of(domain_of(flip(cross_product(intersection(element_relation,sF1),universal_class)))),
inference(step,[status(thm)],[t1968,t180]) ).
cnf(t1970,plain,
sF6 = domain_of(domain_of(flip(cross_product(intersection(sF1,element_relation),universal_class)))),
inference(step,[status(thm)],[t1969,t297]) ).
cnf(t1971,plain,
sF6 = domain_of(domain_of(flip(cross_product(sF2,universal_class)))),
inference(step,[status(thm)],[t1970,t299]) ).
cnf(t1972,plain,
sF6 = domain_of(domain_of(flip(sF3))),
inference(step,[status(thm)],[t1971,t261]) ).
cnf(t1973,plain,
sF6 = domain_of(domain_of(sF4)),
inference(step,[status(thm)],[t1972,t284]) ).
cnf(t1974,plain,
sF6 = domain_of(sF5),
inference(step,[status(thm)],[t1973,t371]) ).
cnf(t501,plain,
domain_of(sF5) = sF6,
inference(orient,[status(thm)],[t1974]) ).
cnf(t2285,plain,
member(not_subclass_element(intersection(complement(sF6),z),x),z) = false,
inference(step,[status(thm)],[t2284,t501]) ).
cnf(t160,axiom,
sF7 = complement(domain_of(domain_of(flip(cross_product(intersection(element_relation,cross_product(complement(x),universal_class)),universal_class))))),
introduced(definition) ).
cnf(t2005,plain,
sF7 = complement(domain_of(domain_of(flip(cross_product(intersection(element_relation,cross_product(sF0,universal_class)),universal_class))))),
inference(step,[status(thm)],[t160,t171]) ).
cnf(t2006,plain,
sF7 = complement(domain_of(domain_of(flip(cross_product(intersection(element_relation,sF1),universal_class))))),
inference(step,[status(thm)],[t2005,t180]) ).
cnf(t2007,plain,
sF7 = complement(domain_of(domain_of(flip(cross_product(intersection(sF1,element_relation),universal_class))))),
inference(step,[status(thm)],[t2006,t297]) ).
cnf(t2008,plain,
sF7 = complement(domain_of(domain_of(flip(cross_product(sF2,universal_class))))),
inference(step,[status(thm)],[t2007,t299]) ).
cnf(t2009,plain,
sF7 = complement(domain_of(domain_of(flip(sF3)))),
inference(step,[status(thm)],[t2008,t261]) ).
cnf(t2010,plain,
sF7 = complement(domain_of(domain_of(sF4))),
inference(step,[status(thm)],[t2009,t284]) ).
cnf(t2011,plain,
sF7 = complement(domain_of(sF5)),
inference(step,[status(thm)],[t2010,t371]) ).
cnf(t2012,plain,
sF7 = complement(sF6),
inference(step,[status(thm)],[t2011,t501]) ).
cnf(t623,plain,
complement(sF6) = sF7,
inference(orient,[status(thm)],[t2012]) ).
cnf(t2286,plain,
member(not_subclass_element(intersection(sF7,z),x),z) = false,
inference(step,[status(thm)],[t2285,t623]) ).
cnf(f21,axiom,
( member(Z,Y)
| ~ member(Z,intersection(X,Y)) ),
file('/export/starexec/sandbox/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(t56,plain,
ifeq(member(X1,intersection(X2,X3)),true,member(X1,X3),true) = true,
inference(equality_encoding,[status(esa)],[c21]) ).
cnf(t404,plain,
ifeq(member(X1,intersection(X2,X3)),true,member(X1,X3),true) = true,
inference(orient,[status(thm)],[t56]) ).
cnf(f1,axiom,
( subclass(X,Y)
| member(not_subclass_element(X,Y),X) ),
file('/export/starexec/sandbox/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(t49,plain,
or(member(not_subclass_element(X1,X2),X1),subclass(X1,X2)) = true,
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t283,plain,
or(member(not_subclass_element(X1,X2),X1),subclass(X1,X2)) = true,
inference(orient,[status(thm)],[t49]) ).
cnf(f159,negated_conjecture,
~ subclass(intersection(power_class(x),z),x),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_complete_induction3_2) ).
fof(f159_nnf,plain,
~ subclass(intersection(power_class(x),z),x),
inference(nnf_transformation,[status(thm)],[f159]) ).
fof(f159_sk,plain,
~ subclass(intersection(power_class(x),z),x),
inference(skolemisation,[status(esa)],[f159_nnf]) ).
cnf(c159,plain,
~ subclass(intersection(power_class(x),z),x),
inference(cnf_transformation,[status(esa)],[f159_sk]) ).
cnf(u90,axiom,
subclass(intersection(power_class(x),z),x) = false,
inference(equality_encoding,[status(esa)],[c159]) ).
cnf(t87,plain,
subclass(intersection(complement(domain_of(domain_of(flip(cross_product(intersection(element_relation,cross_product(complement(x),universal_class)),universal_class))))),z),x) = false,
inference(definition_unfolding,[status(thm)],[u90,d12]) ).
cnf(t2181,plain,
subclass(intersection(complement(domain_of(domain_of(flip(cross_product(intersection(element_relation,cross_product(sF0,universal_class)),universal_class))))),z),x) = false,
inference(step,[status(thm)],[t87,t171]) ).
cnf(t2182,plain,
subclass(intersection(complement(domain_of(domain_of(flip(cross_product(intersection(element_relation,sF1),universal_class))))),z),x) = false,
inference(step,[status(thm)],[t2181,t180]) ).
cnf(t2183,plain,
subclass(intersection(complement(domain_of(domain_of(flip(cross_product(intersection(sF1,element_relation),universal_class))))),z),x) = false,
inference(step,[status(thm)],[t2182,t297]) ).
cnf(t2184,plain,
subclass(intersection(complement(domain_of(domain_of(flip(cross_product(sF2,universal_class))))),z),x) = false,
inference(step,[status(thm)],[t2183,t299]) ).
cnf(t2185,plain,
subclass(intersection(complement(domain_of(domain_of(flip(sF3)))),z),x) = false,
inference(step,[status(thm)],[t2184,t261]) ).
cnf(t2186,plain,
subclass(intersection(complement(domain_of(domain_of(sF4))),z),x) = false,
inference(step,[status(thm)],[t2185,t284]) ).
cnf(t2187,plain,
subclass(intersection(complement(domain_of(sF5)),z),x) = false,
inference(step,[status(thm)],[t2186,t371]) ).
cnf(t2188,plain,
subclass(intersection(complement(sF6),z),x) = false,
inference(step,[status(thm)],[t2187,t501]) ).
cnf(t2189,plain,
subclass(intersection(sF7,z),x) = false,
inference(step,[status(thm)],[t2188,t623]) ).
cnf(t1243,plain,
subclass(intersection(sF7,z),x) = false,
inference(orient,[status(thm)],[t2189]) ).
cnf(t1246,plain,
true = or(member(not_subclass_element(intersection(sF7,z),x),intersection(sF7,z)),false),
inference(cp,[status(thm)],[t283,t1243]) ).
cnf(t6,plain,
or(X1,false) = X1,
introduced(definition) ).
cnf(t174,plain,
or(X1,false) = X1,
inference(orient,[status(thm)],[t6]) ).
cnf(t2219,plain,
true = member(not_subclass_element(intersection(sF7,z),x),intersection(sF7,z)),
inference(step,[status(thm)],[t1246,t174]) ).
cnf(t1370,plain,
member(not_subclass_element(intersection(sF7,z),x),intersection(sF7,z)) = true,
inference(orient,[status(thm)],[t2219]) ).
cnf(t1374,plain,
true = ifeq(true,true,member(not_subclass_element(intersection(sF7,z),x),z),true),
inference(cp,[status(thm)],[t404,t1370]) ).
cnf(t12,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t181,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t12]) ).
cnf(t2221,plain,
true = member(not_subclass_element(intersection(sF7,z),x),z),
inference(step,[status(thm)],[t1374,t181]) ).
cnf(t1390,plain,
member(not_subclass_element(intersection(sF7,z),x),z) = true,
inference(orient,[status(thm)],[t2221]) ).
cnf(t2287,plain,
true = false,
inference(step,[status(thm)],[t2286,t1390]) ).
cnf(t1800,plain,
false = true,
inference(orient,[status(thm)],[t2287]) ).
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(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(f126,axiom,
( ~ member(ordered_pair(V,least(Xr,U)),Xr)
| ~ member(V,U)
| ~ subclass(U,Y)
| ~ well_ordering(Xr,Y) ),
file('/export/starexec/sandbox/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,c159]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t1800]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : NUM139-1 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.07 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.16/0.43 % Computer : n011.cluster.edu
% 0.16/0.43 % Model : x86_64 x86_64
% 0.16/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.43 % Memory : 8046.5625MB
% 0.16/0.43 % OS : Linux 6.8.0-71-generic
% 0.16/0.43 % CPULimit : 300
% 0.16/0.43 % WCLimit : 300
% 0.16/0.43 % DateTime : Thu Sep 24 03:01:12 UTC 2026
% 0.16/0.44 % CPUTime :
% 0.16/0.44 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 16.18/2.56 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 16.18/2.56 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------