%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SEU362+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n007.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:51:51 PM UTC 2026
% Result : Theorem 157.92s 25.34s
% Output : Proof 157.92s
% Verified :
% SZS Type : Refutation
% Derivation depth : 40
% Number of leaves : 54
% Syntax : Number of formulae : 325 ( 149 unt; 0 def)
% Number of atoms : 1085 ( 232 equ)
% Maximal formula atoms : 49 ( 3 avg)
% Number of connectives : 1271 ( 511 ~; 303 |; 379 &)
% ( 15 <=>; 63 =>; 0 <=; 0 <~>)
% Maximal formula depth : 27 ( 4 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 55 ( 53 usr; 1 prp; 0-3 aty)
% Number of functors : 59 ( 59 usr; 25 con; 0-4 aty)
% Number of variables : 507 ( 25 sgn 309 !; 53 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f159,axiom,
! [A] :
( rel_str(A)
=> ! [B] :
( element(B,the_carrier(A))
=> ! [C] :
( element(C,the_carrier(A))
=> ( related(A,B,C)
<=> in(ordered_pair(B,C),the_InternalRel(A)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d9_orders_2) ).
fof(f159_nnf,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( ( ~ in(ordered_pair(B,C),the_InternalRel(A))
| related(A,B,C) )
& ( in(ordered_pair(B,C),the_InternalRel(A))
| ~ related(A,B,C) ) )
| ~ element(C,the_carrier(A)) )
| ~ element(B,the_carrier(A)) )
| ~ rel_str(A) ),
inference(nnf_transformation,[status(thm)],[f159]) ).
fof(f159_sk,plain,
! [A,B,C] :
( ( ( ~ in(ordered_pair(B,C),the_InternalRel(A))
| related(A,B,C) )
& ( in(ordered_pair(B,C),the_InternalRel(A))
| ~ related(A,B,C) ) )
| ~ element(C,the_carrier(A))
| ~ element(B,the_carrier(A))
| ~ rel_str(A) ),
inference(skolemisation,[status(esa)],[f159_nnf]) ).
cnf(c666,plain,
( ~ in(ordered_pair(X1,X2),the_InternalRel(X0))
| related(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ~ element(X1,the_carrier(X0))
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(esa)],[f159_sk]) ).
cnf(t189,plain,
ifeq(rel_str(X1),true,ifeq(element(X2,the_carrier(X1)),true,ifeq(element(X3,the_carrier(X1)),true,ifeq(in(ordered_pair(X2,X3),the_InternalRel(X1)),true,related(X1,X2,X3),true),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c666]) ).
cnf(t378,plain,
ifeq(rel_str(X1),true,ifeq(element(X2,the_carrier(X1)),true,ifeq(element(X3,the_carrier(X1)),true,ifeq(in(ordered_pair(X2,X3),the_InternalRel(X1)),true,related(X1,X2,X3),true),true),true),true) = true,
inference(orient,[status(thm)],[t189]) ).
fof(f357,lemma,
! [A,B] :
( subset(singleton(A),B)
<=> in(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l2_zfmisc_1) ).
fof(f357_nnf,plain,
! [A,B] :
( ( ~ in(A,B)
| subset(singleton(A),B) )
& ( in(A,B)
| ~ subset(singleton(A),B) ) ),
inference(nnf_transformation,[status(thm)],[f357]) ).
fof(f357_sk,plain,
! [A,B] :
( ( ~ in(A,B)
| subset(singleton(A),B) )
& ( in(A,B)
| ~ subset(singleton(A),B) ) ),
inference(skolemisation,[status(esa)],[f357_nnf]) ).
cnf(c1028,plain,
( in(X0,X1)
| ~ subset(singleton(X0),X1) ),
inference(cnf_transformation,[status(esa)],[f357_sk]) ).
cnf(t96,plain,
ifeq(subset(singleton(X1),X2),true,in(X1,X2),true) = true,
inference(equality_encoding,[status(esa)],[c1028]) ).
cnf(t331,plain,
ifeq(subset(singleton(X1),X2),true,in(X1,X2),true) = true,
inference(orient,[status(thm)],[t96]) ).
fof(f532,lemma,
! [A,B,C] :
( ( subset(B,C)
& subset(A,B) )
=> subset(A,C) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_xboole_1) ).
fof(f532_nnf,plain,
! [A,B,C] :
( subset(A,C)
| ~ subset(B,C)
| ~ subset(A,B) ),
inference(nnf_transformation,[status(thm)],[f532]) ).
fof(f532_sk,plain,
! [A,B,C] :
( subset(A,C)
| ~ subset(B,C)
| ~ subset(A,B) ),
inference(skolemisation,[status(esa)],[f532_nnf]) ).
cnf(c2914,plain,
( subset(X0,X2)
| ~ subset(X1,X2)
| ~ subset(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f532_sk]) ).
cnf(t145,plain,
ifeq(subset(X1,X2),true,ifeq(subset(X2,X3),true,subset(X1,X3),true),true) = true,
inference(equality_encoding,[status(esa)],[c2914]) ).
cnf(t322,plain,
ifeq(subset(X1,X2),true,ifeq(subset(X2,X3),true,subset(X1,X3),true),true) = true,
inference(orient,[status(thm)],[t145]) ).
fof(f63,axiom,
! [A] :
( rel_str(A)
=> ! [B] :
( rel_str(B)
=> ( subrelstr(B,A)
<=> ( subset(the_InternalRel(B),the_InternalRel(A))
& subset(the_carrier(B),the_carrier(A)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d13_yellow_0) ).
fof(f63_nnf,plain,
! [A] :
( ! [B] :
( ( ( ~ subset(the_InternalRel(B),the_InternalRel(A))
| ~ subset(the_carrier(B),the_carrier(A))
| subrelstr(B,A) )
& ( ( subset(the_InternalRel(B),the_InternalRel(A))
& subset(the_carrier(B),the_carrier(A)) )
| ~ subrelstr(B,A) ) )
| ~ rel_str(B) )
| ~ rel_str(A) ),
inference(nnf_transformation,[status(thm)],[f63]) ).
fof(f63_sk,plain,
! [A,B] :
( ( ( ~ subset(the_InternalRel(B),the_InternalRel(A))
| ~ subset(the_carrier(B),the_carrier(A))
| subrelstr(B,A) )
& ( ( subset(the_InternalRel(B),the_InternalRel(A))
& subset(the_carrier(B),the_carrier(A)) )
| ~ subrelstr(B,A) ) )
| ~ rel_str(B)
| ~ rel_str(A) ),
inference(skolemisation,[status(esa)],[f63_nnf]) ).
cnf(c202,plain,
( subset(the_InternalRel(X1),the_InternalRel(X0))
| ~ subrelstr(X1,X0)
| ~ rel_str(X1)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(esa)],[f63_sk]) ).
cnf(t166,plain,
ifeq(rel_str(X1),true,ifeq(rel_str(X2),true,ifeq(subrelstr(X2,X1),true,subset(the_InternalRel(X2),the_InternalRel(X1)),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c202]) ).
cnf(t382,plain,
ifeq(rel_str(X1),true,ifeq(rel_str(X2),true,ifeq(subrelstr(X2,X1),true,subset(the_InternalRel(X2),the_InternalRel(X1)),true),true),true) = true,
inference(orient,[status(thm)],[t166]) ).
fof(f651,conjecture,
! [A] :
( rel_str(A)
=> ! [B] :
( subrelstr(B,A)
=> ! [C] :
( element(C,the_carrier(A))
=> ! [D] :
( element(D,the_carrier(A))
=> ! [E] :
( element(E,the_carrier(B))
=> ! [F] :
( element(F,the_carrier(B))
=> ( ( related(B,E,F)
& F = D
& E = C )
=> related(A,C,D) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t60_yellow_0) ).
fof(f651_neg,negated_conjecture,
~ ! [A] :
( rel_str(A)
=> ! [B] :
( subrelstr(B,A)
=> ! [C] :
( element(C,the_carrier(A))
=> ! [D] :
( element(D,the_carrier(A))
=> ! [E] :
( element(E,the_carrier(B))
=> ! [F] :
( element(F,the_carrier(B))
=> ( ( related(B,E,F)
& F = D
& E = C )
=> related(A,C,D) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f651]) ).
fof(f651_nnf,plain,
? [A] :
( ? [B] :
( ? [C] :
( ? [D] :
( ? [E] :
( ? [F] :
( ~ related(A,C,D)
& related(B,E,F)
& F = D
& E = C
& element(F,the_carrier(B)) )
& element(E,the_carrier(B)) )
& element(D,the_carrier(A)) )
& element(C,the_carrier(A)) )
& subrelstr(B,A) )
& rel_str(A) ),
inference(nnf_transformation,[status(thm)],[f651_neg]) ).
fof(f651_sk,plain,
( ~ related(sk463,sk465,sk466)
& related(sk464,sk467,sk468)
& sk468 = sk466
& sk467 = sk465
& element(sk468,the_carrier(sk464))
& element(sk467,the_carrier(sk464))
& element(sk466,the_carrier(sk463))
& element(sk465,the_carrier(sk463))
& subrelstr(sk464,sk463)
& rel_str(sk463) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk463,sk464,sk465,sk466,sk467,sk468])],[f651_nnf]) ).
cnf(c3143,plain,
subrelstr(sk464,sk463),
inference(cnf_transformation,[status(esa)],[f651_sk]) ).
cnf(t29,plain,
subrelstr(sk464,sk463) = true,
inference(equality_encoding,[status(esa)],[c3143]) ).
cnf(t1068,plain,
subrelstr(sk464,sk463) = true,
inference(orient,[status(thm)],[t29]) ).
cnf(t1070,plain,
true = ifeq(rel_str(sk463),true,ifeq(rel_str(sk464),true,ifeq(true,true,subset(the_InternalRel(sk464),the_InternalRel(sk463)),true),true),true),
inference(cp,[status(thm)],[t382,t1068]) ).
cnf(c3142,plain,
rel_str(sk463),
inference(cnf_transformation,[status(esa)],[f651_sk]) ).
cnf(t8,plain,
rel_str(sk463) = true,
inference(equality_encoding,[status(esa)],[c3142]) ).
cnf(t1056,plain,
rel_str(sk463) = true,
inference(orient,[status(thm)],[t8]) ).
cnf(t24840,plain,
true = ifeq(true,true,ifeq(rel_str(sk464),true,ifeq(true,true,subset(the_InternalRel(sk464),the_InternalRel(sk463)),true),true),true),
inference(step,[status(thm)],[t1070,t1056]) ).
cnf(t48,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t194,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t48]) ).
cnf(t24841,plain,
true = ifeq(rel_str(sk464),true,ifeq(true,true,subset(the_InternalRel(sk464),the_InternalRel(sk463)),true),true),
inference(step,[status(thm)],[t24840,t194]) ).
fof(f243,axiom,
! [A] :
( rel_str(A)
=> ! [B] :
( subrelstr(B,A)
=> rel_str(B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m1_yellow_0) ).
fof(f243_nnf,plain,
! [A] :
( ! [B] :
( rel_str(B)
| ~ subrelstr(B,A) )
| ~ rel_str(A) ),
inference(nnf_transformation,[status(thm)],[f243]) ).
fof(f243_sk,plain,
! [A,B] :
( rel_str(B)
| ~ subrelstr(B,A)
| ~ rel_str(A) ),
inference(skolemisation,[status(esa)],[f243_nnf]) ).
cnf(c772,plain,
( rel_str(X1)
| ~ subrelstr(X1,X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(esa)],[f243_sk]) ).
cnf(t128,plain,
ifeq(rel_str(X1),true,ifeq(subrelstr(X2,X1),true,rel_str(X2),true),true) = true,
inference(equality_encoding,[status(esa)],[c772]) ).
cnf(t383,plain,
ifeq(rel_str(X1),true,ifeq(subrelstr(X2,X1),true,rel_str(X2),true),true) = true,
inference(orient,[status(thm)],[t128]) ).
cnf(t1069,plain,
true = ifeq(rel_str(sk463),true,ifeq(true,true,rel_str(sk464),true),true),
inference(cp,[status(thm)],[t383,t1068]) ).
cnf(t24471,plain,
true = ifeq(true,true,ifeq(true,true,rel_str(sk464),true),true),
inference(step,[status(thm)],[t1069,t1056]) ).
cnf(t24472,plain,
true = ifeq(true,true,rel_str(sk464),true),
inference(step,[status(thm)],[t24471,t194]) ).
cnf(t24473,plain,
true = rel_str(sk464),
inference(step,[status(thm)],[t24472,t194]) ).
cnf(t1304,plain,
rel_str(sk464) = true,
inference(orient,[status(thm)],[t24473]) ).
cnf(t24842,plain,
true = ifeq(true,true,ifeq(true,true,subset(the_InternalRel(sk464),the_InternalRel(sk463)),true),true),
inference(step,[status(thm)],[t24841,t1304]) ).
cnf(t24843,plain,
true = ifeq(true,true,subset(the_InternalRel(sk464),the_InternalRel(sk463)),true),
inference(step,[status(thm)],[t24842,t194]) ).
cnf(t24844,plain,
true = subset(the_InternalRel(sk464),the_InternalRel(sk463)),
inference(step,[status(thm)],[t24843,t194]) ).
cnf(t7645,plain,
subset(the_InternalRel(sk464),the_InternalRel(sk463)) = true,
inference(orient,[status(thm)],[t24844]) ).
cnf(t7652,plain,
true = ifeq(subset(X1,the_InternalRel(sk464)),true,ifeq(true,true,subset(X1,the_InternalRel(sk463)),true),true),
inference(cp,[status(thm)],[t322,t7645]) ).
cnf(t25530,plain,
true = ifeq(subset(X1,the_InternalRel(sk464)),true,subset(X1,the_InternalRel(sk463)),true),
inference(step,[status(thm)],[t7652,t194]) ).
cnf(t24322,plain,
ifeq(subset(X1,the_InternalRel(sk464)),true,subset(X1,the_InternalRel(sk463)),true) = true,
inference(orient,[status(thm)],[t25530]) ).
cnf(c1029,plain,
( ~ in(X0,X1)
| subset(singleton(X0),X1) ),
inference(cnf_transformation,[status(esa)],[f357_sk]) ).
cnf(t92,plain,
ifeq(in(X1,X2),true,subset(singleton(X1),X2),true) = true,
inference(equality_encoding,[status(esa)],[c1029]) ).
cnf(t260,plain,
ifeq(in(X1,X2),true,subset(singleton(X1),X2),true) = true,
inference(orient,[status(thm)],[t92]) ).
cnf(c665,plain,
( in(ordered_pair(X1,X2),the_InternalRel(X0))
| ~ related(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ~ element(X1,the_carrier(X0))
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(esa)],[f159_sk]) ).
cnf(t190,plain,
ifeq(rel_str(X1),true,ifeq(element(X2,the_carrier(X1)),true,ifeq(element(X3,the_carrier(X1)),true,ifeq(related(X1,X2,X3),true,in(ordered_pair(X2,X3),the_InternalRel(X1)),true),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c665]) ).
cnf(t379,plain,
ifeq(rel_str(X1),true,ifeq(element(X2,the_carrier(X1)),true,ifeq(element(X3,the_carrier(X1)),true,ifeq(related(X1,X2,X3),true,in(ordered_pair(X2,X3),the_InternalRel(X1)),true),true),true),true) = true,
inference(orient,[status(thm)],[t190]) ).
cnf(c3150,plain,
related(sk464,sk467,sk468),
inference(cnf_transformation,[status(esa)],[f651_sk]) ).
cnf(t46,plain,
related(sk464,sk467,sk468) = true,
inference(equality_encoding,[status(esa)],[c3150]) ).
cnf(t1073,plain,
related(sk464,sk467,sk468) = true,
inference(orient,[status(thm)],[t46]) ).
cnf(t1074,plain,
true = ifeq(rel_str(sk464),true,ifeq(element(sk467,the_carrier(sk464)),true,ifeq(element(sk468,the_carrier(sk464)),true,ifeq(true,true,in(ordered_pair(sk467,sk468),the_InternalRel(sk464)),true),true),true),true),
inference(cp,[status(thm)],[t379,t1073]) ).
cnf(t25262,plain,
true = ifeq(true,true,ifeq(element(sk467,the_carrier(sk464)),true,ifeq(element(sk468,the_carrier(sk464)),true,ifeq(true,true,in(ordered_pair(sk467,sk468),the_InternalRel(sk464)),true),true),true),true),
inference(step,[status(thm)],[t1074,t1304]) ).
cnf(t25263,plain,
true = ifeq(element(sk467,the_carrier(sk464)),true,ifeq(element(sk468,the_carrier(sk464)),true,ifeq(true,true,in(ordered_pair(sk467,sk468),the_InternalRel(sk464)),true),true),true),
inference(step,[status(thm)],[t25262,t194]) ).
cnf(c3146,plain,
element(sk467,the_carrier(sk464)),
inference(cnf_transformation,[status(esa)],[f651_sk]) ).
cnf(t38,plain,
element(sk467,the_carrier(sk464)) = true,
inference(equality_encoding,[status(esa)],[c3146]) ).
cnf(t975,plain,
element(sk467,the_carrier(sk464)) = true,
inference(orient,[status(thm)],[t38]) ).
cnf(t25264,plain,
true = ifeq(true,true,ifeq(element(sk468,the_carrier(sk464)),true,ifeq(true,true,in(ordered_pair(sk467,sk468),the_InternalRel(sk464)),true),true),true),
inference(step,[status(thm)],[t25263,t975]) ).
cnf(t25265,plain,
true = ifeq(element(sk468,the_carrier(sk464)),true,ifeq(true,true,in(ordered_pair(sk467,sk468),the_InternalRel(sk464)),true),true),
inference(step,[status(thm)],[t25264,t194]) ).
cnf(c3147,plain,
element(sk468,the_carrier(sk464)),
inference(cnf_transformation,[status(esa)],[f651_sk]) ).
cnf(t39,plain,
element(sk468,the_carrier(sk464)) = true,
inference(equality_encoding,[status(esa)],[c3147]) ).
cnf(t997,plain,
element(sk468,the_carrier(sk464)) = true,
inference(orient,[status(thm)],[t39]) ).
cnf(t25266,plain,
true = ifeq(true,true,ifeq(true,true,in(ordered_pair(sk467,sk468),the_InternalRel(sk464)),true),true),
inference(step,[status(thm)],[t25265,t997]) ).
cnf(t25267,plain,
true = ifeq(true,true,in(ordered_pair(sk467,sk468),the_InternalRel(sk464)),true),
inference(step,[status(thm)],[t25266,t194]) ).
cnf(t25268,plain,
true = in(ordered_pair(sk467,sk468),the_InternalRel(sk464)),
inference(step,[status(thm)],[t25267,t194]) ).
cnf(t19902,plain,
in(ordered_pair(sk467,sk468),the_InternalRel(sk464)) = true,
inference(orient,[status(thm)],[t25268]) ).
cnf(t19908,plain,
true = ifeq(true,true,subset(singleton(ordered_pair(sk467,sk468)),the_InternalRel(sk464)),true),
inference(cp,[status(thm)],[t260,t19902]) ).
cnf(t25281,plain,
true = subset(singleton(ordered_pair(sk467,sk468)),the_InternalRel(sk464)),
inference(step,[status(thm)],[t19908,t194]) ).
cnf(t20056,plain,
subset(singleton(ordered_pair(sk467,sk468)),the_InternalRel(sk464)) = true,
inference(orient,[status(thm)],[t25281]) ).
cnf(t24323,plain,
true = ifeq(true,true,subset(singleton(ordered_pair(sk467,sk468)),the_InternalRel(sk463)),true),
inference(cp,[status(thm)],[t24322,t20056]) ).
cnf(t25531,plain,
true = subset(singleton(ordered_pair(sk467,sk468)),the_InternalRel(sk463)),
inference(step,[status(thm)],[t24323,t194]) ).
cnf(t24325,plain,
subset(singleton(ordered_pair(sk467,sk468)),the_InternalRel(sk463)) = true,
inference(orient,[status(thm)],[t25531]) ).
cnf(t24328,plain,
true = ifeq(true,true,in(ordered_pair(sk467,sk468),the_InternalRel(sk463)),true),
inference(cp,[status(thm)],[t331,t24325]) ).
cnf(t25532,plain,
true = in(ordered_pair(sk467,sk468),the_InternalRel(sk463)),
inference(step,[status(thm)],[t24328,t194]) ).
cnf(t24342,plain,
in(ordered_pair(sk467,sk468),the_InternalRel(sk463)) = true,
inference(orient,[status(thm)],[t25532]) ).
cnf(t24379,plain,
true = ifeq(rel_str(sk463),true,ifeq(element(sk467,the_carrier(sk463)),true,ifeq(element(sk468,the_carrier(sk463)),true,ifeq(true,true,related(sk463,sk467,sk468),true),true),true),true),
inference(cp,[status(thm)],[t378,t24342]) ).
cnf(t25533,plain,
true = ifeq(true,true,ifeq(element(sk467,the_carrier(sk463)),true,ifeq(element(sk468,the_carrier(sk463)),true,ifeq(true,true,related(sk463,sk467,sk468),true),true),true),true),
inference(step,[status(thm)],[t24379,t1056]) ).
cnf(t25534,plain,
true = ifeq(element(sk467,the_carrier(sk463)),true,ifeq(element(sk468,the_carrier(sk463)),true,ifeq(true,true,related(sk463,sk467,sk468),true),true),true),
inference(step,[status(thm)],[t25533,t194]) ).
cnf(c3144,plain,
element(sk465,the_carrier(sk463)),
inference(cnf_transformation,[status(esa)],[f651_sk]) ).
cnf(t36,plain,
element(sk465,the_carrier(sk463)) = true,
inference(equality_encoding,[status(esa)],[c3144]) ).
cnf(t964,plain,
element(sk465,the_carrier(sk463)) = true,
inference(orient,[status(thm)],[t36]) ).
cnf(c3148,plain,
sk467 = sk465,
inference(cnf_transformation,[status(esa)],[f651_sk]) ).
cnf(t0,plain,
sk467 = sk465,
inference(equality_encoding,[status(esa)],[c3148]) ).
cnf(t1299,plain,
sk465 = sk467,
inference(orient,[status(thm)],[t0]) ).
cnf(t24469,plain,
element(sk467,the_carrier(sk463)) = true,
inference(step,[status(thm)],[t964,t1299]) ).
cnf(t1301,plain,
element(sk467,the_carrier(sk463)) = true,
inference(rw,[status(thm)],[t24469]) ).
cnf(t1483,plain,
element(sk467,the_carrier(sk463)) = true,
inference(orient,[status(thm)],[t1301]) ).
cnf(t25535,plain,
true = ifeq(true,true,ifeq(element(sk468,the_carrier(sk463)),true,ifeq(true,true,related(sk463,sk467,sk468),true),true),true),
inference(step,[status(thm)],[t25534,t1483]) ).
cnf(t25536,plain,
true = ifeq(element(sk468,the_carrier(sk463)),true,ifeq(true,true,related(sk463,sk467,sk468),true),true),
inference(step,[status(thm)],[t25535,t194]) ).
cnf(c3145,plain,
element(sk466,the_carrier(sk463)),
inference(cnf_transformation,[status(esa)],[f651_sk]) ).
cnf(t37,plain,
element(sk466,the_carrier(sk463)) = true,
inference(equality_encoding,[status(esa)],[c3145]) ).
cnf(t986,plain,
element(sk466,the_carrier(sk463)) = true,
inference(orient,[status(thm)],[t37]) ).
cnf(c3149,plain,
sk468 = sk466,
inference(cnf_transformation,[status(esa)],[f651_sk]) ).
cnf(t1,plain,
sk468 = sk466,
inference(equality_encoding,[status(esa)],[c3149]) ).
cnf(t1302,plain,
sk466 = sk468,
inference(orient,[status(thm)],[t1]) ).
cnf(t24470,plain,
element(sk468,the_carrier(sk463)) = true,
inference(step,[status(thm)],[t986,t1302]) ).
cnf(t1303,plain,
element(sk468,the_carrier(sk463)) = true,
inference(rw,[status(thm)],[t24470]) ).
cnf(t1494,plain,
element(sk468,the_carrier(sk463)) = true,
inference(orient,[status(thm)],[t1303]) ).
cnf(t25537,plain,
true = ifeq(true,true,ifeq(true,true,related(sk463,sk467,sk468),true),true),
inference(step,[status(thm)],[t25536,t1494]) ).
cnf(t25538,plain,
true = ifeq(true,true,related(sk463,sk467,sk468),true),
inference(step,[status(thm)],[t25537,t194]) ).
cnf(t25539,plain,
true = related(sk463,sk467,sk468),
inference(step,[status(thm)],[t25538,t194]) ).
cnf(c3151,plain,
~ related(sk463,sk465,sk466),
inference(cnf_transformation,[status(esa)],[f651_sk]) ).
cnf(t45,plain,
related(sk463,sk465,sk466) = false,
inference(equality_encoding,[status(esa)],[c3151]) ).
cnf(t1287,plain,
related(sk463,sk465,sk466) = false,
inference(orient,[status(thm)],[t45]) ).
cnf(t24468,plain,
related(sk463,sk467,sk466) = false,
inference(step,[status(thm)],[t1287,t1299]) ).
cnf(t1300,plain,
related(sk463,sk467,sk466) = false,
inference(rw,[status(thm)],[t24468]) ).
cnf(t24482,plain,
related(sk463,sk467,sk468) = false,
inference(step,[status(thm)],[t1300,t1302]) ).
cnf(t1480,plain,
related(sk463,sk467,sk468) = false,
inference(orient,[status(thm)],[t24482]) ).
cnf(t25540,plain,
true = false,
inference(step,[status(thm)],[t25539,t1480]) ).
cnf(t24391,plain,
false = true,
inference(orient,[status(thm)],[t25540]) ).
fof(f2,axiom,
! [A,B] :
( in(A,B)
=> ~ in(B,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',antisymmetry_r2_hidden) ).
fof(f2_nnf,plain,
! [A,B] :
( ~ in(B,A)
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [A,B] :
( ~ in(B,A)
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
( ~ in(X1,X0)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
fof(f3,axiom,
! [A,B] :
( proper_subset(A,B)
=> ~ proper_subset(B,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',antisymmetry_r2_xboole_0) ).
fof(f3_nnf,plain,
! [A,B] :
( ~ proper_subset(B,A)
| ~ proper_subset(A,B) ),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [A,B] :
( ~ proper_subset(B,A)
| ~ proper_subset(A,B) ),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
( ~ proper_subset(X1,X0)
| ~ proper_subset(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
fof(f61,axiom,
! [A] :
( top_str(A)
=> ! [B] :
( element(B,powerset(the_carrier(A)))
=> ! [C] :
( element(C,powerset(the_carrier(A)))
=> ( C = topstr_closure(A,B)
<=> ! [D] :
( in(D,the_carrier(A))
=> ( in(D,C)
<=> ! [E] :
( element(E,powerset(the_carrier(A)))
=> ~ ( disjoint(B,E)
& in(D,E)
& open_subset(E,A) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d13_pre_topc) ).
fof(f61_nnf,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( ( ? [D] :
( ( ( ! [E] :
( ~ disjoint(B,E)
| ~ in(D,E)
| ~ open_subset(E,A)
| ~ element(E,powerset(the_carrier(A))) )
& ~ in(D,C) )
| ( ? [E] :
( disjoint(B,E)
& in(D,E)
& open_subset(E,A)
& element(E,powerset(the_carrier(A))) )
& in(D,C) ) )
& in(D,the_carrier(A)) )
| C = topstr_closure(A,B) )
& ( ! [D] :
( ( ( ? [E] :
( disjoint(B,E)
& in(D,E)
& open_subset(E,A)
& element(E,powerset(the_carrier(A))) )
| in(D,C) )
& ( ! [E] :
( ~ disjoint(B,E)
| ~ in(D,E)
| ~ open_subset(E,A)
| ~ element(E,powerset(the_carrier(A))) )
| ~ in(D,C) ) )
| ~ in(D,the_carrier(A)) )
| C != topstr_closure(A,B) ) )
| ~ element(C,powerset(the_carrier(A))) )
| ~ element(B,powerset(the_carrier(A))) )
| ~ top_str(A) ),
inference(nnf_transformation,[status(thm)],[f61]) ).
fof(f61_sk,plain,
! [A,B,C,D,E] :
( ( ( ( ( ( ( ~ disjoint(B,E)
| ~ in(sk14(A,B,C),E)
| ~ open_subset(E,A)
| ~ element(E,powerset(the_carrier(A))) )
& ~ in(sk14(A,B,C),C) )
| ( disjoint(B,sk15(A,B,C))
& in(sk14(A,B,C),sk15(A,B,C))
& open_subset(sk15(A,B,C),A)
& element(sk15(A,B,C),powerset(the_carrier(A)))
& in(sk14(A,B,C),C) ) )
& in(sk14(A,B,C),the_carrier(A)) )
| C = topstr_closure(A,B) )
& ( ( ( ( disjoint(B,sk13(A,B,C,D))
& in(D,sk13(A,B,C,D))
& open_subset(sk13(A,B,C,D),A)
& element(sk13(A,B,C,D),powerset(the_carrier(A))) )
| in(D,C) )
& ( ~ disjoint(B,E)
| ~ in(D,E)
| ~ open_subset(E,A)
| ~ element(E,powerset(the_carrier(A)))
| ~ in(D,C) ) )
| ~ in(D,the_carrier(A))
| C != topstr_closure(A,B) ) )
| ~ element(C,powerset(the_carrier(A)))
| ~ element(B,powerset(the_carrier(A)))
| ~ top_str(A) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk13,sk14,sk15])],[f61_nnf]) ).
cnf(c176,plain,
( ~ disjoint(X1,X4)
| ~ in(X3,X4)
| ~ open_subset(X4,X0)
| ~ element(X4,powerset(the_carrier(X0)))
| ~ in(X3,X2)
| ~ in(X3,the_carrier(X0))
| X2 != topstr_closure(X0,X1)
| ~ element(X2,powerset(the_carrier(X0)))
| ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0) ),
inference(cnf_transformation,[status(esa)],[f61_sk]) ).
fof(f89,axiom,
! [A] :
( relation(A)
=> ! [B,C] :
( C = fiber(A,B)
<=> ! [D] :
( in(D,C)
<=> ( in(ordered_pair(D,B),A)
& D != B ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d1_wellord1) ).
fof(f89_nnf,plain,
! [A] :
( ! [B,C] :
( ( ? [D] :
( ( in(ordered_pair(D,B),A)
& D != B
& ~ in(D,C) )
| ( ( ~ in(ordered_pair(D,B),A)
| D = B )
& in(D,C) ) )
| C = fiber(A,B) )
& ( ! [D] :
( ( ~ in(ordered_pair(D,B),A)
| D = B
| in(D,C) )
& ( ( in(ordered_pair(D,B),A)
& D != B )
| ~ in(D,C) ) )
| C != fiber(A,B) ) )
| ~ relation(A) ),
inference(nnf_transformation,[status(thm)],[f89]) ).
fof(f89_sk,plain,
! [A,C,B,D] :
( ( ( ( in(ordered_pair(sk46(A,B,C),B),A)
& sk46(A,B,C) != B
& ~ in(sk46(A,B,C),C) )
| ( ( ~ in(ordered_pair(sk46(A,B,C),B),A)
| sk46(A,B,C) = B )
& in(sk46(A,B,C),C) )
| C = fiber(A,B) )
& ( ( ( ~ in(ordered_pair(D,B),A)
| D = B
| in(D,C) )
& ( ( in(ordered_pair(D,B),A)
& D != B )
| ~ in(D,C) ) )
| C != fiber(A,B) ) )
| ~ relation(A) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk46])],[f89_nnf]) ).
cnf(c320,plain,
( X3 != X1
| ~ in(X3,X2)
| X2 != fiber(X0,X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(esa)],[f89_sk]) ).
fof(f91,axiom,
! [A] :
( A = empty_set
<=> ! [B] : ~ in(B,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d1_xboole_0) ).
fof(f91_nnf,plain,
! [A] :
( ( ? [B] : in(B,A)
| A = empty_set )
& ( ! [B] : ~ in(B,A)
| A != empty_set ) ),
inference(nnf_transformation,[status(thm)],[f91]) ).
fof(f91_sk,plain,
! [A,B] :
( ( in(sk49(A),A)
| A = empty_set )
& ( ~ in(B,A)
| A != empty_set ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk49])],[f91_nnf]) ).
cnf(c338,plain,
( ~ in(X1,X0)
| X0 != empty_set ),
inference(cnf_transformation,[status(esa)],[f91_sk]) ).
fof(f95,axiom,
! [A] :
( centered(A)
<=> ( ! [B] :
~ ( set_meet(B) = empty_set
& finite(B)
& subset(B,A)
& B != empty_set )
& A != empty_set ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d2_compts_1) ).
fof(f95_nnf,plain,
! [A] :
( ( ? [B] :
( set_meet(B) = empty_set
& finite(B)
& subset(B,A)
& B != empty_set )
| A = empty_set
| centered(A) )
& ( ( ! [B] :
( set_meet(B) != empty_set
| ~ finite(B)
| ~ subset(B,A)
| B = empty_set )
& A != empty_set )
| ~ centered(A) ) ),
inference(nnf_transformation,[status(thm)],[f95]) ).
fof(f95_sk,plain,
! [A,B] :
( ( ( set_meet(sk52(A)) = empty_set
& finite(sk52(A))
& subset(sk52(A),A)
& sk52(A) != empty_set )
| A = empty_set
| centered(A) )
& ( ( ( set_meet(B) != empty_set
| ~ finite(B)
| ~ subset(B,A)
| B = empty_set )
& A != empty_set )
| ~ centered(A) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk52])],[f95_nnf]) ).
cnf(c352,plain,
( X0 != empty_set
| ~ centered(X0) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
fof(f104,axiom,
! [A,B] :
( element(B,A)
=> ( proper_element(B,A)
<=> B != union(A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d2_tex_2) ).
fof(f104_nnf,plain,
! [A,B] :
( ( ( B = union(A)
| proper_element(B,A) )
& ( B != union(A)
| ~ proper_element(B,A) ) )
| ~ element(B,A) ),
inference(nnf_transformation,[status(thm)],[f104]) ).
fof(f104_sk,plain,
! [B,A] :
( ( ( B = union(A)
| proper_element(B,A) )
& ( B != union(A)
| ~ proper_element(B,A) ) )
| ~ element(B,A) ),
inference(skolemisation,[status(esa)],[f104_nnf]) ).
cnf(c386,plain,
( X1 != union(X0)
| ~ proper_element(X1,X0)
| ~ element(X1,X0) ),
inference(cnf_transformation,[status(esa)],[f104_sk]) ).
fof(f127,axiom,
! [A,B,C] :
( C = set_difference(A,B)
<=> ! [D] :
( in(D,C)
<=> ( ~ in(D,B)
& in(D,A) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d4_xboole_0) ).
fof(f127_nnf,plain,
! [A,B,C] :
( ( ? [D] :
( ( ~ in(D,B)
& in(D,A)
& ~ in(D,C) )
| ( ( in(D,B)
| ~ in(D,A) )
& in(D,C) ) )
| C = set_difference(A,B) )
& ( ! [D] :
( ( in(D,B)
| ~ in(D,A)
| in(D,C) )
& ( ( ~ in(D,B)
& in(D,A) )
| ~ in(D,C) ) )
| C != set_difference(A,B) ) ),
inference(nnf_transformation,[status(thm)],[f127]) ).
fof(f127_sk,plain,
! [C,A,B,D] :
( ( ( ~ in(sk87(A,B,C),B)
& in(sk87(A,B,C),A)
& ~ in(sk87(A,B,C),C) )
| ( ( in(sk87(A,B,C),B)
| ~ in(sk87(A,B,C),A) )
& in(sk87(A,B,C),C) )
| C = set_difference(A,B) )
& ( ( ( in(D,B)
| ~ in(D,A)
| in(D,C) )
& ( ( ~ in(D,B)
& in(D,A) )
| ~ in(D,C) ) )
| C != set_difference(A,B) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk87])],[f127_nnf]) ).
cnf(c499,plain,
( ~ in(X3,X1)
| ~ in(X3,X2)
| X2 != set_difference(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f127_sk]) ).
fof(f155,axiom,
! [A,B] :
( proper_subset(A,B)
<=> ( A != B
& subset(A,B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d8_xboole_0) ).
fof(f155_nnf,plain,
! [A,B] :
( ( A = B
| ~ subset(A,B)
| proper_subset(A,B) )
& ( ( A != B
& subset(A,B) )
| ~ proper_subset(A,B) ) ),
inference(nnf_transformation,[status(thm)],[f155]) ).
fof(f155_sk,plain,
! [A,B] :
( ( A = B
| ~ subset(A,B)
| proper_subset(A,B) )
& ( ( A != B
& subset(A,B) )
| ~ proper_subset(A,B) ) ),
inference(skolemisation,[status(esa)],[f155_nnf]) ).
cnf(c640,plain,
( X0 != X1
| ~ proper_subset(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f155_sk]) ).
fof(f270,axiom,
! [A] :
( finite(singleton(A))
& ~ empty(singleton(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_finset_1) ).
fof(f270_nnf,plain,
! [A] :
( finite(singleton(A))
& ~ empty(singleton(A)) ),
inference(nnf_transformation,[status(thm)],[f270]) ).
fof(f270_sk,plain,
! [A] :
( finite(singleton(A))
& ~ empty(singleton(A)) ),
inference(skolemisation,[status(esa)],[f270_nnf]) ).
cnf(c808,plain,
~ empty(singleton(X0)),
inference(cnf_transformation,[status(esa)],[f270_sk]) ).
fof(f271,axiom,
! [A] :
( preboolean(powerset(A))
& diff_closed(powerset(A))
& cup_closed(powerset(A))
& ~ empty(powerset(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_finsub_1) ).
fof(f271_nnf,plain,
! [A] :
( preboolean(powerset(A))
& diff_closed(powerset(A))
& cup_closed(powerset(A))
& ~ empty(powerset(A)) ),
inference(nnf_transformation,[status(thm)],[f271]) ).
fof(f271_sk,plain,
! [A] :
( preboolean(powerset(A))
& diff_closed(powerset(A))
& cup_closed(powerset(A))
& ~ empty(powerset(A)) ),
inference(skolemisation,[status(esa)],[f271_nnf]) ).
cnf(c810,plain,
~ empty(powerset(X0)),
inference(cnf_transformation,[status(esa)],[f271_sk]) ).
fof(f273,axiom,
! [A] :
( strict_latt_str(boole_lattice(A))
& ~ empty_carrier(boole_lattice(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_lattice3) ).
fof(f273_nnf,plain,
! [A] :
( strict_latt_str(boole_lattice(A))
& ~ empty_carrier(boole_lattice(A)) ),
inference(nnf_transformation,[status(thm)],[f273]) ).
fof(f273_sk,plain,
! [A] :
( strict_latt_str(boole_lattice(A))
& ~ empty_carrier(boole_lattice(A)) ),
inference(skolemisation,[status(esa)],[f273_nnf]) ).
cnf(c816,plain,
~ empty_carrier(boole_lattice(X0)),
inference(cnf_transformation,[status(esa)],[f273_sk]) ).
fof(f275,axiom,
! [A] : ~ empty(succ(A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_ordinal1) ).
fof(f275_nnf,plain,
! [A] : ~ empty(succ(A)),
inference(nnf_transformation,[status(thm)],[f275]) ).
fof(f275_sk,plain,
! [A] : ~ empty(succ(A)),
inference(skolemisation,[status(esa)],[f275_nnf]) ).
cnf(c820,plain,
~ empty(succ(X0)),
inference(cnf_transformation,[status(esa)],[f275_sk]) ).
fof(f276,axiom,
( ~ empty(omega)
& ordinal(omega)
& epsilon_connected(omega)
& epsilon_transitive(omega) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_ordinal2) ).
fof(f276_nnf,plain,
( ~ empty(omega)
& ordinal(omega)
& epsilon_connected(omega)
& epsilon_transitive(omega) ),
inference(nnf_transformation,[status(thm)],[f276]) ).
fof(f276_sk,plain,
( ~ empty(omega)
& ordinal(omega)
& epsilon_connected(omega)
& epsilon_transitive(omega) ),
inference(skolemisation,[status(esa)],[f276_nnf]) ).
cnf(c824,plain,
~ empty(omega),
inference(cnf_transformation,[status(esa)],[f276_sk]) ).
fof(f280,axiom,
! [A] : ~ empty(powerset(A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_subset_1) ).
fof(f280_nnf,plain,
! [A] : ~ empty(powerset(A)),
inference(nnf_transformation,[status(thm)],[f280]) ).
fof(f280_sk,plain,
! [A] : ~ empty(powerset(A)),
inference(skolemisation,[status(esa)],[f280_nnf]) ).
cnf(c833,plain,
~ empty(powerset(X0)),
inference(cnf_transformation,[status(esa)],[f280_sk]) ).
fof(f282,axiom,
! [A,B] : ~ empty(ordered_pair(A,B)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_zfmisc_1) ).
fof(f282_nnf,plain,
! [A,B] : ~ empty(ordered_pair(A,B)),
inference(nnf_transformation,[status(thm)],[f282]) ).
fof(f282_sk,plain,
! [A,B] : ~ empty(ordered_pair(A,B)),
inference(skolemisation,[status(esa)],[f282_nnf]) ).
cnf(c835,plain,
~ empty(ordered_pair(X0,X1)),
inference(cnf_transformation,[status(esa)],[f282_sk]) ).
fof(f286,axiom,
! [A] :
( ( natural(A)
& ordinal(A) )
=> ( natural(succ(A))
& ordinal(succ(A))
& epsilon_connected(succ(A))
& epsilon_transitive(succ(A))
& ~ empty(succ(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc2_arytm_3) ).
fof(f286_nnf,plain,
! [A] :
( ( natural(succ(A))
& ordinal(succ(A))
& epsilon_connected(succ(A))
& epsilon_transitive(succ(A))
& ~ empty(succ(A)) )
| ~ natural(A)
| ~ ordinal(A) ),
inference(nnf_transformation,[status(thm)],[f286]) ).
fof(f286_sk,plain,
! [A] :
( ( natural(succ(A))
& ordinal(succ(A))
& epsilon_connected(succ(A))
& epsilon_transitive(succ(A))
& ~ empty(succ(A)) )
| ~ natural(A)
| ~ ordinal(A) ),
inference(skolemisation,[status(esa)],[f286_nnf]) ).
cnf(c840,plain,
( ~ empty(succ(X0))
| ~ natural(X0)
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(esa)],[f286_sk]) ).
fof(f289,axiom,
! [A] :
( lattice(boole_lattice(A))
& join_absorbing(boole_lattice(A))
& meet_absorbing(boole_lattice(A))
& meet_associative(boole_lattice(A))
& meet_commutative(boole_lattice(A))
& join_associative(boole_lattice(A))
& join_commutative(boole_lattice(A))
& strict_latt_str(boole_lattice(A))
& ~ empty_carrier(boole_lattice(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc2_lattice3) ).
fof(f289_nnf,plain,
! [A] :
( lattice(boole_lattice(A))
& join_absorbing(boole_lattice(A))
& meet_absorbing(boole_lattice(A))
& meet_associative(boole_lattice(A))
& meet_commutative(boole_lattice(A))
& join_associative(boole_lattice(A))
& join_commutative(boole_lattice(A))
& strict_latt_str(boole_lattice(A))
& ~ empty_carrier(boole_lattice(A)) ),
inference(nnf_transformation,[status(thm)],[f289]) ).
fof(f289_sk,plain,
! [A] :
( lattice(boole_lattice(A))
& join_absorbing(boole_lattice(A))
& meet_absorbing(boole_lattice(A))
& meet_associative(boole_lattice(A))
& meet_commutative(boole_lattice(A))
& join_associative(boole_lattice(A))
& join_commutative(boole_lattice(A))
& strict_latt_str(boole_lattice(A))
& ~ empty_carrier(boole_lattice(A)) ),
inference(skolemisation,[status(esa)],[f289_nnf]) ).
cnf(c852,plain,
~ empty_carrier(boole_lattice(X0)),
inference(cnf_transformation,[status(esa)],[f289_sk]) ).
fof(f295,axiom,
! [A] : ~ empty(singleton(A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc2_subset_1) ).
fof(f295_nnf,plain,
! [A] : ~ empty(singleton(A)),
inference(nnf_transformation,[status(thm)],[f295]) ).
fof(f295_sk,plain,
! [A] : ~ empty(singleton(A)),
inference(skolemisation,[status(esa)],[f295_nnf]) ).
cnf(c882,plain,
~ empty(singleton(X0)),
inference(cnf_transformation,[status(esa)],[f295_sk]) ).
fof(f312,axiom,
! [A] :
( ordinal(A)
=> ( ordinal(succ(A))
& epsilon_connected(succ(A))
& epsilon_transitive(succ(A))
& ~ empty(succ(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc3_ordinal1) ).
fof(f312_nnf,plain,
! [A] :
( ( ordinal(succ(A))
& epsilon_connected(succ(A))
& epsilon_transitive(succ(A))
& ~ empty(succ(A)) )
| ~ ordinal(A) ),
inference(nnf_transformation,[status(thm)],[f312]) ).
fof(f312_sk,plain,
! [A] :
( ( ordinal(succ(A))
& epsilon_connected(succ(A))
& epsilon_transitive(succ(A))
& ~ empty(succ(A)) )
| ~ ordinal(A) ),
inference(skolemisation,[status(esa)],[f312_nnf]) ).
cnf(c930,plain,
( ~ empty(succ(X0))
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(esa)],[f312_sk]) ).
fof(f314,axiom,
! [A,B] : ~ empty(unordered_pair(A,B)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc3_subset_1) ).
fof(f314_nnf,plain,
! [A,B] : ~ empty(unordered_pair(A,B)),
inference(nnf_transformation,[status(thm)],[f314]) ).
fof(f314_sk,plain,
! [A,B] : ~ empty(unordered_pair(A,B)),
inference(skolemisation,[status(esa)],[f314_nnf]) ).
cnf(c935,plain,
~ empty(unordered_pair(X0,X1)),
inference(cnf_transformation,[status(esa)],[f314_sk]) ).
fof(f349,axiom,
! [A,B] : ~ proper_subset(A,A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',irreflexivity_r2_xboole_0) ).
fof(f349_nnf,plain,
! [A,B] : ~ proper_subset(A,A),
inference(nnf_transformation,[status(thm)],[f349]) ).
fof(f349_sk,plain,
! [A] : ~ proper_subset(A,A),
inference(skolemisation,[status(esa)],[f349_nnf]) ).
cnf(c1015,plain,
~ proper_subset(X0,X0),
inference(cnf_transformation,[status(esa)],[f349_sk]) ).
fof(f351,lemma,
! [A] : singleton(A) != empty_set,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l1_zfmisc_1) ).
fof(f351_nnf,plain,
! [A] : singleton(A) != empty_set,
inference(nnf_transformation,[status(thm)],[f351]) ).
fof(f351_sk,plain,
! [A] : singleton(A) != empty_set,
inference(skolemisation,[status(esa)],[f351_nnf]) ).
cnf(c1019,plain,
singleton(X0) != empty_set,
inference(cnf_transformation,[status(esa)],[f351_sk]) ).
fof(f353,lemma,
! [A,B] :
~ ( in(A,B)
& disjoint(singleton(A),B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l25_zfmisc_1) ).
fof(f353_nnf,plain,
! [A,B] :
( ~ in(A,B)
| ~ disjoint(singleton(A),B) ),
inference(nnf_transformation,[status(thm)],[f353]) ).
fof(f353_sk,plain,
! [A,B] :
( ~ in(A,B)
| ~ disjoint(singleton(A),B) ),
inference(skolemisation,[status(esa)],[f353_nnf]) ).
cnf(c1021,plain,
( ~ in(X0,X1)
| ~ disjoint(singleton(X0),X1) ),
inference(cnf_transformation,[status(esa)],[f353_sk]) ).
fof(f370,axiom,
? [A] :
( natural(A)
& ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A)
& ~ empty(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc1_arytm_3) ).
fof(f370_nnf,plain,
? [A] :
( natural(A)
& ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A)
& ~ empty(A) ),
inference(nnf_transformation,[status(thm)],[f370]) ).
fof(f370_sk,plain,
( natural(sk150)
& ordinal(sk150)
& epsilon_connected(sk150)
& epsilon_transitive(sk150)
& ~ empty(sk150) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk150])],[f370_nnf]) ).
cnf(c1060,plain,
~ empty(sk150),
inference(cnf_transformation,[status(esa)],[f370_sk]) ).
fof(f371,axiom,
? [A] :
( finite(A)
& ~ empty(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc1_finset_1) ).
fof(f371_nnf,plain,
? [A] :
( finite(A)
& ~ empty(A) ),
inference(nnf_transformation,[status(thm)],[f371]) ).
fof(f371_sk,plain,
( finite(sk151)
& ~ empty(sk151) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk151])],[f371_nnf]) ).
cnf(c1065,plain,
~ empty(sk151),
inference(cnf_transformation,[status(esa)],[f371_sk]) ).
fof(f374,axiom,
? [A] :
( v5_membered(A)
& v4_membered(A)
& v3_membered(A)
& v2_membered(A)
& v1_membered(A)
& ~ empty(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc1_membered) ).
fof(f374_nnf,plain,
? [A] :
( v5_membered(A)
& v4_membered(A)
& v3_membered(A)
& v2_membered(A)
& v1_membered(A)
& ~ empty(A) ),
inference(nnf_transformation,[status(thm)],[f374]) ).
fof(f374_sk,plain,
( v5_membered(sk154)
& v4_membered(sk154)
& v3_membered(sk154)
& v2_membered(sk154)
& v1_membered(sk154)
& ~ empty(sk154) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk154])],[f374_nnf]) ).
cnf(c1073,plain,
~ empty(sk154),
inference(cnf_transformation,[status(esa)],[f374_sk]) ).
fof(f386,axiom,
? [A] :
( antisymmetric_relstr(A)
& transitive_relstr(A)
& reflexive_relstr(A)
& strict_rel_str(A)
& ~ empty_carrier(A)
& rel_str(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc2_orders_2) ).
fof(f386_nnf,plain,
? [A] :
( antisymmetric_relstr(A)
& transitive_relstr(A)
& reflexive_relstr(A)
& strict_rel_str(A)
& ~ empty_carrier(A)
& rel_str(A) ),
inference(nnf_transformation,[status(thm)],[f386]) ).
fof(f386_sk,plain,
( antisymmetric_relstr(sk166)
& transitive_relstr(sk166)
& reflexive_relstr(sk166)
& strict_rel_str(sk166)
& ~ empty_carrier(sk166)
& rel_str(sk166) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk166])],[f386_nnf]) ).
cnf(c1120,plain,
~ empty_carrier(sk166),
inference(cnf_transformation,[status(esa)],[f386_sk]) ).
fof(f389,axiom,
? [A] :
( relation(A)
& ~ empty(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc2_relat_1) ).
fof(f389_nnf,plain,
? [A] :
( relation(A)
& ~ empty(A) ),
inference(nnf_transformation,[status(thm)],[f389]) ).
fof(f389_sk,plain,
( relation(sk169)
& ~ empty(sk169) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk169])],[f389_nnf]) ).
cnf(c1135,plain,
~ empty(sk169),
inference(cnf_transformation,[status(esa)],[f389_sk]) ).
fof(f391,axiom,
! [A] :
? [B] :
( ~ proper_element(B,powerset(A))
& element(B,powerset(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc2_tex_2) ).
fof(f391_nnf,plain,
! [A] :
? [B] :
( ~ proper_element(B,powerset(A))
& element(B,powerset(A)) ),
inference(nnf_transformation,[status(thm)],[f391]) ).
fof(f391_sk,plain,
! [A] :
( ~ proper_element(sk171(A),powerset(A))
& element(sk171(A),powerset(A)) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk171])],[f391_nnf]) ).
cnf(c1140,plain,
~ proper_element(sk171(X0),powerset(X0)),
inference(cnf_transformation,[status(esa)],[f391_sk]) ).
fof(f393,axiom,
? [A] : ~ empty(A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc2_xboole_0) ).
fof(f393_nnf,plain,
? [A] : ~ empty(A),
inference(nnf_transformation,[status(thm)],[f393]) ).
fof(f393_sk,plain,
~ empty(sk173),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk173])],[f393_nnf]) ).
cnf(c1144,plain,
~ empty(sk173),
inference(cnf_transformation,[status(esa)],[f393_sk]) ).
fof(f397,axiom,
? [A] :
( ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A)
& ~ empty(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc3_ordinal1) ).
fof(f397_nnf,plain,
? [A] :
( ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A)
& ~ empty(A) ),
inference(nnf_transformation,[status(thm)],[f397]) ).
fof(f397_sk,plain,
( ordinal(sk177)
& epsilon_connected(sk177)
& epsilon_transitive(sk177)
& ~ empty(sk177) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk177])],[f397_nnf]) ).
cnf(c1153,plain,
~ empty(sk177),
inference(cnf_transformation,[status(esa)],[f397_sk]) ).
fof(f400,axiom,
? [A] :
( ~ empty_carrier(A)
& one_sorted_str(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc3_struct_0) ).
fof(f400_nnf,plain,
? [A] :
( ~ empty_carrier(A)
& one_sorted_str(A) ),
inference(nnf_transformation,[status(thm)],[f400]) ).
fof(f400_sk,plain,
( ~ empty_carrier(sk180)
& one_sorted_str(sk180) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk180])],[f400_nnf]) ).
cnf(c1167,plain,
~ empty_carrier(sk180),
inference(cnf_transformation,[status(esa)],[f400_sk]) ).
fof(f404,axiom,
? [A] :
( strict_latt_str(A)
& ~ empty_carrier(A)
& latt_str(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc6_lattices) ).
fof(f404_nnf,plain,
? [A] :
( strict_latt_str(A)
& ~ empty_carrier(A)
& latt_str(A) ),
inference(nnf_transformation,[status(thm)],[f404]) ).
fof(f404_sk,plain,
( strict_latt_str(sk184)
& ~ empty_carrier(sk184)
& latt_str(sk184) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk184])],[f404_nnf]) ).
cnf(c1177,plain,
~ empty_carrier(sk184),
inference(cnf_transformation,[status(esa)],[f404_sk]) ).
fof(f407,axiom,
? [A] :
( lattice(A)
& join_absorbing(A)
& meet_absorbing(A)
& meet_associative(A)
& meet_commutative(A)
& join_associative(A)
& join_commutative(A)
& strict_latt_str(A)
& ~ empty_carrier(A)
& latt_str(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc9_lattices) ).
fof(f407_nnf,plain,
? [A] :
( lattice(A)
& join_absorbing(A)
& meet_absorbing(A)
& meet_associative(A)
& meet_commutative(A)
& join_associative(A)
& join_commutative(A)
& strict_latt_str(A)
& ~ empty_carrier(A)
& latt_str(A) ),
inference(nnf_transformation,[status(thm)],[f407]) ).
fof(f407_sk,plain,
( lattice(sk187)
& join_absorbing(sk187)
& meet_absorbing(sk187)
& meet_associative(sk187)
& meet_commutative(sk187)
& join_associative(sk187)
& join_commutative(sk187)
& strict_latt_str(sk187)
& ~ empty_carrier(sk187)
& latt_str(sk187) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk187])],[f407_nnf]) ).
cnf(c1185,plain,
~ empty_carrier(sk187),
inference(cnf_transformation,[status(esa)],[f407_sk]) ).
fof(f439,lemma,
( ( ! [D] :
( ordinal(D)
=> ( ( ! [K] :
( ordinal(K)
=> ( in(K,D)
=> ( in(K,omega)
=> ! [L] :
( element(L,powerset(powerset(K)))
=> ~ ( ! [M] :
~ ( ! [N] :
( ( subset(M,N)
& in(N,L) )
=> N = M )
& in(M,L) )
& L != empty_set ) ) ) ) )
& being_limit_ordinal(D) )
=> ( ( in(D,omega)
=> ! [O] :
( element(O,powerset(powerset(D)))
=> ~ ( ! [P] :
~ ( ! [Q] :
( ( subset(P,Q)
& in(Q,O) )
=> Q = P )
& in(P,O) )
& O != empty_set ) ) )
| D = empty_set ) ) )
& ! [D] :
( ordinal(D)
=> ( ( in(D,omega)
=> ! [E] :
( element(E,powerset(powerset(D)))
=> ~ ( ! [F] :
~ ( ! [G] :
( ( subset(F,G)
& in(G,E) )
=> G = F )
& in(F,E) )
& E != empty_set ) ) )
=> ( in(succ(D),omega)
=> ! [H] :
( element(H,powerset(powerset(succ(D))))
=> ~ ( ! [I] :
~ ( ! [J] :
( ( subset(I,J)
& in(J,H) )
=> J = I )
& in(I,H) )
& H != empty_set ) ) ) ) )
& ( in(empty_set,omega)
=> ! [A] :
( element(A,powerset(powerset(empty_set)))
=> ~ ( ! [B] :
~ ( ! [C] :
( ( subset(B,C)
& in(C,A) )
=> C = B )
& in(B,A) )
& A != empty_set ) ) ) )
=> ! [D] :
( ordinal(D)
=> ( in(D,omega)
=> ! [R] :
( element(R,powerset(powerset(D)))
=> ~ ( ! [S] :
~ ( ! [T] :
( ( subset(S,T)
& in(T,R) )
=> T = S )
& in(S,R) )
& R != empty_set ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s1_ordinal2__e18_27__finset_1) ).
fof(f439_nnf,plain,
( ! [D] :
( ! [R] :
( ? [S] :
( ! [T] :
( T = S
| ~ subset(S,T)
| ~ in(T,R) )
& in(S,R) )
| R = empty_set
| ~ element(R,powerset(powerset(D))) )
| ~ in(D,omega)
| ~ ordinal(D) )
| ? [D] :
( ? [O] :
( ! [P] :
( ? [Q] :
( Q != P
& subset(P,Q)
& in(Q,O) )
| ~ in(P,O) )
& O != empty_set
& element(O,powerset(powerset(D))) )
& in(D,omega)
& D != empty_set
& ! [K] :
( ! [L] :
( ? [M] :
( ! [N] :
( N = M
| ~ subset(M,N)
| ~ in(N,L) )
& in(M,L) )
| L = empty_set
| ~ element(L,powerset(powerset(K))) )
| ~ in(K,omega)
| ~ in(K,D)
| ~ ordinal(K) )
& being_limit_ordinal(D)
& ordinal(D) )
| ? [D] :
( ? [H] :
( ! [I] :
( ? [J] :
( J != I
& subset(I,J)
& in(J,H) )
| ~ in(I,H) )
& H != empty_set
& element(H,powerset(powerset(succ(D)))) )
& in(succ(D),omega)
& ( ! [E] :
( ? [F] :
( ! [G] :
( G = F
| ~ subset(F,G)
| ~ in(G,E) )
& in(F,E) )
| E = empty_set
| ~ element(E,powerset(powerset(D))) )
| ~ in(D,omega) )
& ordinal(D) )
| ( ? [A] :
( ! [B] :
( ? [C] :
( C != B
& subset(B,C)
& in(C,A) )
| ~ in(B,A) )
& A != empty_set
& element(A,powerset(powerset(empty_set))) )
& in(empty_set,omega) ) ),
inference(nnf_transformation,[status(thm)],[f439]) ).
fof(f439_sk,plain,
! [B,E,G,I,K,L,N,P,D,R,T] :
( ( ( T = sk221(D,R)
| ~ subset(sk221(D,R),T)
| ~ in(T,R) )
& in(sk221(D,R),R) )
| R = empty_set
| ~ element(R,powerset(powerset(D)))
| ~ in(D,omega)
| ~ ordinal(D)
| ( ( ( sk220(P) != P
& subset(P,sk220(P))
& in(sk220(P),sk219) )
| ~ in(P,sk219) )
& sk219 != empty_set
& element(sk219,powerset(powerset(sk217)))
& in(sk217,omega)
& sk217 != empty_set
& ( ( ( N = sk218(K,L)
| ~ subset(sk218(K,L),N)
| ~ in(N,L) )
& in(sk218(K,L),L) )
| L = empty_set
| ~ element(L,powerset(powerset(K)))
| ~ in(K,omega)
| ~ in(K,sk217)
| ~ ordinal(K) )
& being_limit_ordinal(sk217)
& ordinal(sk217) )
| ( ( ( sk216(I) != I
& subset(I,sk216(I))
& in(sk216(I),sk215) )
| ~ in(I,sk215) )
& sk215 != empty_set
& element(sk215,powerset(powerset(succ(sk213))))
& in(succ(sk213),omega)
& ( ( ( G = sk214(E)
| ~ subset(sk214(E),G)
| ~ in(G,E) )
& in(sk214(E),E) )
| E = empty_set
| ~ element(E,powerset(powerset(sk213)))
| ~ in(sk213,omega) )
& ordinal(sk213) )
| ( ( ( sk212(B) != B
& subset(B,sk212(B))
& in(sk212(B),sk211) )
| ~ in(B,sk211) )
& sk211 != empty_set
& element(sk211,powerset(powerset(empty_set)))
& in(empty_set,omega) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk211,sk212,sk213,sk214,sk215,sk216,sk217,sk218,sk219,sk220,sk221])],[f439_nnf]) ).
cnf(c1423,plain,
( sk212(X1) != X1
| ~ def1(X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47])],[f439_sk]) ).
cnf(c1428,plain,
( sk211 != empty_set
| ~ def3(X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47])],[f439_sk]) ).
cnf(c1437,plain,
( ~ subset(sk214(X4),X6)
| ~ in(X6,X4)
| ~ def6(X6,X4) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47])],[f439_sk]) ).
cnf(c1459,plain,
( sk216(X8) != X8
| ~ def13(X8) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47])],[f439_sk]) ).
cnf(c1464,plain,
( sk215 != empty_set
| ~ def15(X8) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47])],[f439_sk]) ).
cnf(c1482,plain,
( ~ subset(sk218(X10,X11),X13)
| ~ in(X13,X11)
| ~ def21(X13,X11,X10) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47])],[f439_sk]) ).
cnf(c1513,plain,
( sk220(X15) != X15
| ~ def31(X15) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47])],[f439_sk]) ).
cnf(c1518,plain,
( sk219 != empty_set
| ~ def33(X15) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47])],[f439_sk]) ).
cnf(c1527,plain,
( sk217 != empty_set
| ~ def36(X15) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47])],[f439_sk]) ).
cnf(c1539,plain,
( ~ subset(sk221(X3,X17),X19)
| ~ in(X19,X17)
| ~ def40(X19,X17,X3) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47])],[f439_sk]) ).
fof(f599,lemma,
! [A,B,C] :
~ ( in(C,A)
& in(B,C)
& in(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t3_ordinal1) ).
fof(f599_nnf,plain,
! [A,B,C] :
( ~ in(C,A)
| ~ in(B,C)
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f599]) ).
fof(f599_sk,plain,
! [A,B,C] :
( ~ in(C,A)
| ~ in(B,C)
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f599_nnf]) ).
cnf(c3039,plain,
( ~ in(X2,X0)
| ~ in(X1,X2)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f599_sk]) ).
fof(f602,lemma,
! [A,B] :
( ~ ( disjoint(A,B)
& ? [C] :
( in(C,B)
& in(C,A) ) )
& ~ ( ! [C] :
~ ( in(C,B)
& in(C,A) )
& ~ disjoint(A,B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t3_xboole_0) ).
fof(f602_nnf,plain,
! [A,B] :
( ( ~ disjoint(A,B)
| ! [C] :
( ~ in(C,B)
| ~ in(C,A) ) )
& ( ? [C] :
( in(C,B)
& in(C,A) )
| disjoint(A,B) ) ),
inference(nnf_transformation,[status(thm)],[f602]) ).
fof(f602_sk,plain,
! [A,B,C] :
( ( ~ disjoint(A,B)
| ~ in(C,B)
| ~ in(C,A) )
& ( ( in(sk452(A,B),B)
& in(sk452(A,B),A) )
| disjoint(A,B) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk452])],[f602_nnf]) ).
cnf(c3045,plain,
( ~ disjoint(X0,X1)
| ~ in(X2,X1)
| ~ in(X2,X0) ),
inference(cnf_transformation,[status(esa)],[f602_sk]) ).
fof(f606,lemma,
! [A] :
( ordinal(A)
=> ( ~ ( being_limit_ordinal(A)
& ? [B] :
( A = succ(B)
& ordinal(B) ) )
& ~ ( ! [B] :
( ordinal(B)
=> A != succ(B) )
& ~ being_limit_ordinal(A) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t42_ordinal1) ).
fof(f606_nnf,plain,
! [A] :
( ( ( ~ being_limit_ordinal(A)
| ! [B] :
( A != succ(B)
| ~ ordinal(B) ) )
& ( ? [B] :
( A = succ(B)
& ordinal(B) )
| being_limit_ordinal(A) ) )
| ~ ordinal(A) ),
inference(nnf_transformation,[status(thm)],[f606]) ).
fof(f606_sk,plain,
! [A,B] :
( ( ( ~ being_limit_ordinal(A)
| A != succ(B)
| ~ ordinal(B) )
& ( ( A = succ(sk454(A))
& ordinal(sk454(A)) )
| being_limit_ordinal(A) ) )
| ~ ordinal(A) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk454])],[f606_nnf]) ).
cnf(c3054,plain,
( ~ being_limit_ordinal(X0)
| X0 != succ(X1)
| ~ ordinal(X1)
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(esa)],[f606_sk]) ).
fof(f630,lemma,
! [A,B] :
( ~ ( disjoint(A,B)
& ? [C] : in(C,set_intersection2(A,B)) )
& ~ ( ! [C] : ~ in(C,set_intersection2(A,B))
& ~ disjoint(A,B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t4_xboole_0) ).
fof(f630_nnf,plain,
! [A,B] :
( ( ~ disjoint(A,B)
| ! [C] : ~ in(C,set_intersection2(A,B)) )
& ( ? [C] : in(C,set_intersection2(A,B))
| disjoint(A,B) ) ),
inference(nnf_transformation,[status(thm)],[f630]) ).
fof(f630_sk,plain,
! [A,B,C] :
( ( ~ disjoint(A,B)
| ~ in(C,set_intersection2(A,B)) )
& ( in(sk458(A,B),set_intersection2(A,B))
| disjoint(A,B) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk458])],[f630_nnf]) ).
cnf(c3093,plain,
( ~ disjoint(X0,X1)
| ~ in(X2,set_intersection2(X0,X1)) ),
inference(cnf_transformation,[status(esa)],[f630_sk]) ).
fof(f637,lemma,
! [A,B,C] :
( element(C,powerset(A))
=> ~ ( in(B,C)
& in(B,subset_complement(A,C)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t54_subset_1) ).
fof(f637_nnf,plain,
! [A,B,C] :
( ~ in(B,C)
| ~ in(B,subset_complement(A,C))
| ~ element(C,powerset(A)) ),
inference(nnf_transformation,[status(thm)],[f637]) ).
fof(f637_sk,plain,
! [C,A,B] :
( ~ in(B,C)
| ~ in(B,subset_complement(A,C))
| ~ element(C,powerset(A)) ),
inference(skolemisation,[status(esa)],[f637_nnf]) ).
cnf(c3122,plain,
( ~ in(X1,X2)
| ~ in(X1,subset_complement(X0,X2))
| ~ element(X2,powerset(X0)) ),
inference(cnf_transformation,[status(esa)],[f637_sk]) ).
fof(f644,axiom,
! [A,B,C] :
~ ( empty(C)
& element(B,powerset(C))
& in(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t5_subset) ).
fof(f644_nnf,plain,
! [A,B,C] :
( ~ empty(C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f644]) ).
fof(f644_sk,plain,
! [A,B,C] :
( ~ empty(C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f644_nnf]) ).
cnf(c3132,plain,
( ~ empty(X2)
| ~ element(X1,powerset(X2))
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f644_sk]) ).
fof(f645,lemma,
! [A,B] :
( element(B,powerset(A))
=> ( proper_element(B,powerset(A))
<=> B != A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t5_tex_2) ).
fof(f645_nnf,plain,
! [A,B] :
( ( ( B = A
| proper_element(B,powerset(A)) )
& ( B != A
| ~ proper_element(B,powerset(A)) ) )
| ~ element(B,powerset(A)) ),
inference(nnf_transformation,[status(thm)],[f645]) ).
fof(f645_sk,plain,
! [B,A] :
( ( ( B = A
| proper_element(B,powerset(A)) )
& ( B != A
| ~ proper_element(B,powerset(A)) ) )
| ~ element(B,powerset(A)) ),
inference(skolemisation,[status(esa)],[f645_nnf]) ).
cnf(c3133,plain,
( X1 != X0
| ~ proper_element(X1,powerset(X0))
| ~ element(X1,powerset(X0)) ),
inference(cnf_transformation,[status(esa)],[f645_sk]) ).
fof(f650,lemma,
! [A,B] :
~ ( proper_subset(B,A)
& subset(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t60_xboole_1) ).
fof(f650_nnf,plain,
! [A,B] :
( ~ proper_subset(B,A)
| ~ subset(A,B) ),
inference(nnf_transformation,[status(thm)],[f650]) ).
fof(f650_sk,plain,
! [A,B] :
( ~ proper_subset(B,A)
| ~ subset(A,B) ),
inference(skolemisation,[status(esa)],[f650_nnf]) ).
cnf(c3141,plain,
( ~ proper_subset(X1,X0)
| ~ subset(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f650_sk]) ).
fof(f656,lemma,
! [A,B] :
( set_difference(A,singleton(B)) = A
<=> ~ in(B,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t65_zfmisc_1) ).
fof(f656_nnf,plain,
! [A,B] :
( ( in(B,A)
| set_difference(A,singleton(B)) = A )
& ( ~ in(B,A)
| set_difference(A,singleton(B)) != A ) ),
inference(nnf_transformation,[status(thm)],[f656]) ).
fof(f656_sk,plain,
! [A,B] :
( ( in(B,A)
| set_difference(A,singleton(B)) = A )
& ( ~ in(B,A)
| set_difference(A,singleton(B)) != A ) ),
inference(skolemisation,[status(esa)],[f656_nnf]) ).
cnf(c3158,plain,
( ~ in(X1,X0)
| set_difference(X0,singleton(X1)) != X0 ),
inference(cnf_transformation,[status(esa)],[f656_sk]) ).
fof(f668,axiom,
! [A,B] :
~ ( empty(B)
& in(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t7_boole) ).
fof(f668_nnf,plain,
! [A,B] :
( ~ empty(B)
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f668]) ).
fof(f668_sk,plain,
! [A,B] :
( ~ empty(B)
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f668_nnf]) ).
cnf(c3178,plain,
( ~ empty(X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f668_sk]) ).
fof(f671,axiom,
! [A,B] :
~ ( ! [C] :
~ ( ! [D] :
~ ( in(D,C)
& in(D,B) )
& in(C,B) )
& in(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t7_tarski) ).
fof(f671_nnf,plain,
! [A,B] :
( ? [C] :
( ! [D] :
( ~ in(D,C)
| ~ in(D,B) )
& in(C,B) )
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f671]) ).
fof(f671_sk,plain,
! [A,B,D] :
( ( ( ~ in(D,sk470(A,B))
| ~ in(D,B) )
& in(sk470(A,B),B) )
| ~ in(A,B) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk470])],[f671_nnf]) ).
cnf(c3184,plain,
( ~ in(X3,sk470(X0,X1))
| ~ in(X3,X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f671_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c2,c3,c176,c320,c338,c352,c386,c499,c640,c808,c810,c816,c820,c824,c833,c835,c840,c852,c882,c930,c935,c1015,c1019,c1021,c1060,c1065,c1073,c1120,c1135,c1140,c1144,c1153,c1167,c1177,c1185,c1423,c1428,c1437,c1459,c1464,c1482,c1513,c1518,c1527,c1539,c3039,c3045,c3054,c3093,c3122,c3132,c3133,c3141,c3151,c3158,c3178,c3184]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t24391]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU362+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/5.36 % Computer : n007.cluster.edu
% 0.10/5.36 % Model : x86_64 x86_64
% 0.10/5.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.36 % Memory : 8046.5625MB
% 0.10/5.36 % OS : Linux 6.8.0-71-generic
% 0.10/5.36 % CPULimit : 300
% 0.10/5.36 % WCLimit : 300
% 0.10/5.36 % DateTime : Thu Sep 24 13:48:44 UTC 2026
% 0.10/5.36 % CPUTime :
% 0.10/5.36 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 157.92/25.34 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 157.92/25.34 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------