%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SEU368+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 : n002.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:52 PM UTC 2026
% Result : Theorem 135.80s 18.71s
% Output : Proof 135.80s
% Verified :
% SZS Type : Refutation
% Derivation depth : 38
% Number of leaves : 58
% Syntax : Number of formulae : 320 ( 139 unt; 0 def)
% Number of atoms : 1030 ( 245 equ)
% Maximal formula atoms : 49 ( 3 avg)
% Number of connectives : 1201 ( 491 ~; 279 |; 372 &)
% ( 13 <=>; 46 =>; 0 <=; 0 <~>)
% Maximal formula depth : 27 ( 4 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 59 ( 57 usr; 1 prp; 0-3 aty)
% Number of functors : 58 ( 58 usr; 20 con; 0-4 aty)
% Number of variables : 571 ( 49 sgn 308 !; 48 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f560,conjecture,
! [A] :
( the_InternalRel(incl_POSet(A)) = inclusion_order(A)
& the_carrier(incl_POSet(A)) = A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_yellow_1) ).
fof(f560_neg,negated_conjecture,
~ ! [A] :
( the_InternalRel(incl_POSet(A)) = inclusion_order(A)
& the_carrier(incl_POSet(A)) = A ),
inference(negated_conjecture,[status(cth)],[f560]) ).
fof(f560_nnf,plain,
? [A] :
( the_InternalRel(incl_POSet(A)) != inclusion_order(A)
| the_carrier(incl_POSet(A)) != A ),
inference(nnf_transformation,[status(thm)],[f560_neg]) ).
fof(f560_sk,plain,
( the_InternalRel(incl_POSet(sk467)) != inclusion_order(sk467)
| the_carrier(incl_POSet(sk467)) != sk467 ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk467])],[f560_nnf]) ).
cnf(c3080,plain,
( the_InternalRel(incl_POSet(sk467)) != inclusion_order(sk467)
| the_carrier(incl_POSet(sk467)) != sk467 ),
inference(cnf_transformation,[status(esa)],[f560_sk]) ).
cnf(t103,plain,
ifeq(the_carrier(incl_POSet(sk467)),sk467,ifeq(the_InternalRel(incl_POSet(sk467)),inclusion_order(sk467),false,true),true) = true,
inference(equality_encoding,[status(esa)],[c3080]) ).
cnf(t188,plain,
ifeq(the_carrier(incl_POSet(sk467)),sk467,ifeq(the_InternalRel(incl_POSet(sk467)),inclusion_order(sk467),false,true),true) = true,
inference(orient,[status(thm)],[t103]) ).
fof(f432,axiom,
! [A] : inclusion_order(A) = inclusion_relation(A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k1_yellow_1) ).
fof(f432_nnf,plain,
! [A] : inclusion_order(A) = inclusion_relation(A),
inference(nnf_transformation,[status(thm)],[f432]) ).
fof(f432_sk,plain,
! [A] : inclusion_order(A) = inclusion_relation(A),
inference(skolemisation,[status(esa)],[f432_nnf]) ).
cnf(c1250,plain,
inclusion_order(X0) = inclusion_relation(X0),
inference(cnf_transformation,[status(esa)],[f432_sk]) ).
cnf(t20,plain,
inclusion_relation(X1) = inclusion_order(X1),
inference(equality_encoding,[status(esa)],[c1250]) ).
cnf(t618,plain,
inclusion_order(X1) = inclusion_relation(X1),
inference(orient,[status(thm)],[t20]) ).
cnf(t2782,plain,
ifeq(the_carrier(incl_POSet(sk467)),sk467,ifeq(the_InternalRel(incl_POSet(sk467)),inclusion_relation(sk467),false,true),true) = true,
inference(step,[status(thm)],[t188,t618]) ).
cnf(t623,plain,
ifeq(the_carrier(incl_POSet(sk467)),sk467,ifeq(the_InternalRel(incl_POSet(sk467)),inclusion_relation(sk467),false,true),true) = true,
inference(rw,[status(thm)],[t2782]) ).
fof(f359,axiom,
! [A,B] :
( relation_of2(B,A,A)
=> ! [C,D] :
( rel_str_of(A,B) = rel_str_of(C,D)
=> ( B = D
& A = C ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',free_g1_orders_2) ).
fof(f359_nnf,plain,
! [A,B] :
( ! [C,D] :
( ( B = D
& A = C )
| rel_str_of(A,B) != rel_str_of(C,D) )
| ~ relation_of2(B,A,A) ),
inference(nnf_transformation,[status(thm)],[f359]) ).
fof(f359_sk,plain,
! [B,A,C,D] :
( ( B = D
& A = C )
| rel_str_of(A,B) != rel_str_of(C,D)
| ~ relation_of2(B,A,A) ),
inference(skolemisation,[status(esa)],[f359_nnf]) ).
cnf(c1054,plain,
( X0 = X2
| rel_str_of(X0,X1) != rel_str_of(X2,X3)
| ~ relation_of2(X1,X0,X0) ),
inference(cnf_transformation,[status(esa)],[f359_sk]) ).
cnf(t111,plain,
ifeq(relation_of2(X1,X2,X2),true,ifeq(rel_str_of(X2,X1),rel_str_of(X3,X4),X2,X3),X3) = X3,
inference(equality_encoding,[status(esa)],[c1054]) ).
cnf(t156,plain,
ifeq(relation_of2(X1,X2,X2),true,ifeq(rel_str_of(X2,X1),rel_str_of(X3,X4),X2,X3),X3) = X3,
inference(orient,[status(thm)],[t111]) ).
fof(f447,axiom,
! [A,B,C] :
( relation_of2_as_subset(C,A,B)
<=> relation_of2(C,A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(f447_nnf,plain,
! [A,B,C] :
( ( ~ relation_of2(C,A,B)
| relation_of2_as_subset(C,A,B) )
& ( relation_of2(C,A,B)
| ~ relation_of2_as_subset(C,A,B) ) ),
inference(nnf_transformation,[status(thm)],[f447]) ).
fof(f447_sk,plain,
! [C,A,B] :
( ( ~ relation_of2(C,A,B)
| relation_of2_as_subset(C,A,B) )
& ( relation_of2(C,A,B)
| ~ relation_of2_as_subset(C,A,B) ) ),
inference(skolemisation,[status(esa)],[f447_nnf]) ).
cnf(c1265,plain,
( relation_of2(X2,X0,X1)
| ~ relation_of2_as_subset(X2,X0,X1) ),
inference(cnf_transformation,[status(esa)],[f447_sk]) ).
cnf(hi1128,axiom,
ifeq(relation_of2_as_subset(X0,X1,X2),true,relation_of2(X0,X1,X2),true) = true,
inference(equality_encoding,[status(esa)],[c1265]) ).
fof(f195,axiom,
! [A] :
( relation_of2_as_subset(inclusion_order(A),A,A)
& v1_partfun1(inclusion_order(A),A,A)
& transitive(inclusion_order(A))
& antisymmetric(inclusion_order(A))
& reflexive(inclusion_order(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k1_yellow_1) ).
fof(f195_nnf,plain,
! [A] :
( relation_of2_as_subset(inclusion_order(A),A,A)
& v1_partfun1(inclusion_order(A),A,A)
& transitive(inclusion_order(A))
& antisymmetric(inclusion_order(A))
& reflexive(inclusion_order(A)) ),
inference(nnf_transformation,[status(thm)],[f195]) ).
fof(f195_sk,plain,
! [A] :
( relation_of2_as_subset(inclusion_order(A),A,A)
& v1_partfun1(inclusion_order(A),A,A)
& transitive(inclusion_order(A))
& antisymmetric(inclusion_order(A))
& reflexive(inclusion_order(A)) ),
inference(skolemisation,[status(esa)],[f195_nnf]) ).
cnf(c731,plain,
relation_of2_as_subset(inclusion_order(X0),X0,X0),
inference(cnf_transformation,[status(esa)],[f195_sk]) ).
cnf(hi639,axiom,
relation_of2_as_subset(inclusion_order(X0),X0,X0) = true,
inference(equality_encoding,[status(esa)],[c731]) ).
cnf(hi309,axiom,
inclusion_order(X0) = inclusion_relation(X0),
inference(equality_encoding,[status(esa)],[c1250]) ).
cnf(t51,plain,
relation_of2(inclusion_order(X1),X1,X1) = true,
inference(hyper_resolution,[status(thm)],[hi1128,hi639,hi309]) ).
cnf(t409,plain,
relation_of2(inclusion_order(X1),X1,X1) = true,
inference(orient,[status(thm)],[t51]) ).
cnf(t2781,plain,
relation_of2(inclusion_relation(X1),X1,X1) = true,
inference(step,[status(thm)],[t409,t618]) ).
cnf(t622,plain,
relation_of2(inclusion_relation(X1),X1,X1) = true,
inference(rw,[status(thm)],[t2781]) ).
cnf(t692,plain,
relation_of2(inclusion_relation(X1),X1,X1) = true,
inference(orient,[status(thm)],[t622]) ).
cnf(t693,plain,
X1 = ifeq(true,true,ifeq(rel_str_of(X2,inclusion_relation(X2)),rel_str_of(X1,X3),X2,X1),X1),
inference(cp,[status(thm)],[t156,t692]) ).
cnf(t47,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t145,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t47]) ).
cnf(t2831,plain,
X1 = ifeq(rel_str_of(X2,inclusion_relation(X2)),rel_str_of(X1,X3),X2,X1),
inference(step,[status(thm)],[t693,t145]) ).
fof(f97,axiom,
! [A] : incl_POSet(A) = rel_str_of(A,inclusion_order(A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d1_yellow_1) ).
fof(f97_nnf,plain,
! [A] : incl_POSet(A) = rel_str_of(A,inclusion_order(A)),
inference(nnf_transformation,[status(thm)],[f97]) ).
fof(f97_sk,plain,
! [A] : incl_POSet(A) = rel_str_of(A,inclusion_order(A)),
inference(skolemisation,[status(esa)],[f97_nnf]) ).
cnf(c362,plain,
incl_POSet(X0) = rel_str_of(X0,inclusion_order(X0)),
inference(cnf_transformation,[status(esa)],[f97_sk]) ).
cnf(t49,plain,
rel_str_of(X1,inclusion_order(X1)) = incl_POSet(X1),
inference(equality_encoding,[status(esa)],[c362]) ).
cnf(t551,plain,
rel_str_of(X1,inclusion_order(X1)) = incl_POSet(X1),
inference(orient,[status(thm)],[t49]) ).
cnf(t2778,plain,
rel_str_of(X1,inclusion_relation(X1)) = incl_POSet(X1),
inference(step,[status(thm)],[t551,t618]) ).
cnf(t619,plain,
rel_str_of(X1,inclusion_relation(X1)) = incl_POSet(X1),
inference(rw,[status(thm)],[t2778]) ).
cnf(t665,plain,
rel_str_of(X1,inclusion_relation(X1)) = incl_POSet(X1),
inference(orient,[status(thm)],[t619]) ).
cnf(t2832,plain,
X1 = ifeq(incl_POSet(X2),rel_str_of(X1,X3),X2,X1),
inference(step,[status(thm)],[t2831,t665]) ).
cnf(t810,plain,
ifeq(incl_POSet(X1),rel_str_of(X2,X3),X1,X2) = X2,
inference(orient,[status(thm)],[t2832]) ).
fof(f0,axiom,
! [A] :
( rel_str(A)
=> ( strict_rel_str(A)
=> A = rel_str_of(the_carrier(A),the_InternalRel(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',abstractness_v1_orders_2) ).
fof(f0_nnf,plain,
! [A] :
( A = rel_str_of(the_carrier(A),the_InternalRel(A))
| ~ strict_rel_str(A)
| ~ rel_str(A) ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [A] :
( A = rel_str_of(the_carrier(A),the_InternalRel(A))
| ~ strict_rel_str(A)
| ~ rel_str(A) ),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
( X0 = rel_str_of(the_carrier(X0),the_InternalRel(X0))
| ~ strict_rel_str(X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(hi0,axiom,
ifeq(rel_str(X0),true,ifeq(strict_rel_str(X0),true,X0,rel_str_of(the_carrier(X0),the_InternalRel(X0))),rel_str_of(the_carrier(X0),the_InternalRel(X0))) = rel_str_of(the_carrier(X0),the_InternalRel(X0)),
inference(equality_encoding,[status(esa)],[c0]) ).
fof(f210,axiom,
! [A] :
( rel_str(incl_POSet(A))
& strict_rel_str(incl_POSet(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k2_yellow_1) ).
fof(f210_nnf,plain,
! [A] :
( rel_str(incl_POSet(A))
& strict_rel_str(incl_POSet(A)) ),
inference(nnf_transformation,[status(thm)],[f210]) ).
fof(f210_sk,plain,
! [A] :
( rel_str(incl_POSet(A))
& strict_rel_str(incl_POSet(A)) ),
inference(skolemisation,[status(esa)],[f210_nnf]) ).
cnf(c752,plain,
rel_str(incl_POSet(X0)),
inference(cnf_transformation,[status(esa)],[f210_sk]) ).
cnf(hi656,axiom,
rel_str(incl_POSet(X0)) = true,
inference(equality_encoding,[status(esa)],[c752]) ).
cnf(c751,plain,
strict_rel_str(incl_POSet(X0)),
inference(cnf_transformation,[status(esa)],[f210_sk]) ).
cnf(hi655,axiom,
strict_rel_str(incl_POSet(X0)) = true,
inference(equality_encoding,[status(esa)],[c751]) ).
cnf(hi317,axiom,
incl_POSet(X0) = rel_str_of(X0,inclusion_order(X0)),
inference(equality_encoding,[status(esa)],[c362]) ).
cnf(t67,plain,
rel_str_of(the_carrier(incl_POSet(X1)),the_InternalRel(incl_POSet(X1))) = incl_POSet(X1),
inference(hyper_resolution,[status(thm)],[hi0,hi656,hi655,hi317,hi309]) ).
cnf(t556,plain,
rel_str_of(the_carrier(incl_POSet(X1)),the_InternalRel(incl_POSet(X1))) = incl_POSet(X1),
inference(orient,[status(thm)],[t67]) ).
cnf(t812,plain,
the_carrier(incl_POSet(X1)) = ifeq(incl_POSet(X2),incl_POSet(X1),X2,the_carrier(incl_POSet(X1))),
inference(cp,[status(thm)],[t810,t556]) ).
cnf(t839,plain,
ifeq(incl_POSet(X1),incl_POSet(X2),X1,the_carrier(incl_POSet(X2))) = the_carrier(incl_POSet(X2)),
inference(orient,[status(thm)],[t812]) ).
cnf(t840,plain,
the_carrier(incl_POSet(X1)) = X1,
inference(cp,[status(thm)],[t839,t145]) ).
cnf(t841,plain,
the_carrier(incl_POSet(X1)) = X1,
inference(orient,[status(thm)],[t840]) ).
cnf(t3051,plain,
ifeq(sk467,sk467,ifeq(the_InternalRel(incl_POSet(sk467)),inclusion_relation(sk467),false,true),true) = true,
inference(step,[status(thm)],[t623,t841]) ).
cnf(t3052,plain,
ifeq(the_InternalRel(incl_POSet(sk467)),inclusion_relation(sk467),false,true) = true,
inference(step,[status(thm)],[t3051,t145]) ).
cnf(c1055,plain,
( X1 = X3
| rel_str_of(X0,X1) != rel_str_of(X2,X3)
| ~ relation_of2(X1,X0,X0) ),
inference(cnf_transformation,[status(esa)],[f359_sk]) ).
cnf(t110,plain,
ifeq(relation_of2(X1,X2,X2),true,ifeq(rel_str_of(X2,X1),rel_str_of(X3,X4),X1,X4),X4) = X4,
inference(equality_encoding,[status(esa)],[c1055]) ).
cnf(t154,plain,
ifeq(relation_of2(X1,X2,X2),true,ifeq(rel_str_of(X2,X1),rel_str_of(X3,X4),X1,X4),X4) = X4,
inference(orient,[status(thm)],[t110]) ).
cnf(t90,plain,
ifeq(relation_of2_as_subset(X1,X2,X3),true,relation_of2(X1,X2,X3),true) = true,
inference(equality_encoding,[status(esa)],[c1265]) ).
cnf(t207,plain,
ifeq(relation_of2_as_subset(X1,X2,X3),true,relation_of2(X1,X2,X3),true) = true,
inference(orient,[status(thm)],[t90]) ).
fof(f260,axiom,
! [A] :
( rel_str(A)
=> relation_of2_as_subset(the_InternalRel(A),the_carrier(A),the_carrier(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_u1_orders_2) ).
fof(f260_nnf,plain,
! [A] :
( relation_of2_as_subset(the_InternalRel(A),the_carrier(A),the_carrier(A))
| ~ rel_str(A) ),
inference(nnf_transformation,[status(thm)],[f260]) ).
fof(f260_sk,plain,
! [A] :
( relation_of2_as_subset(the_InternalRel(A),the_carrier(A),the_carrier(A))
| ~ rel_str(A) ),
inference(skolemisation,[status(esa)],[f260_nnf]) ).
cnf(c813,plain,
( relation_of2_as_subset(the_InternalRel(X0),the_carrier(X0),the_carrier(X0))
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(esa)],[f260_sk]) ).
cnf(t95,plain,
ifeq(rel_str(X1),true,relation_of2_as_subset(the_InternalRel(X1),the_carrier(X1),the_carrier(X1)),true) = true,
inference(equality_encoding,[status(esa)],[c813]) ).
cnf(t214,plain,
ifeq(rel_str(X1),true,relation_of2_as_subset(the_InternalRel(X1),the_carrier(X1),the_carrier(X1)),true) = true,
inference(orient,[status(thm)],[t95]) ).
cnf(t842,plain,
true = ifeq(rel_str(incl_POSet(X1)),true,relation_of2_as_subset(the_InternalRel(incl_POSet(X1)),X1,the_carrier(incl_POSet(X1))),true),
inference(cp,[status(thm)],[t214,t841]) ).
cnf(t29,plain,
rel_str(incl_POSet(X1)) = true,
inference(equality_encoding,[status(esa)],[c752]) ).
cnf(t470,plain,
rel_str(incl_POSet(X1)) = true,
inference(orient,[status(thm)],[t29]) ).
cnf(t2863,plain,
true = ifeq(true,true,relation_of2_as_subset(the_InternalRel(incl_POSet(X1)),X1,the_carrier(incl_POSet(X1))),true),
inference(step,[status(thm)],[t842,t470]) ).
cnf(t2864,plain,
true = relation_of2_as_subset(the_InternalRel(incl_POSet(X1)),X1,the_carrier(incl_POSet(X1))),
inference(step,[status(thm)],[t2863,t145]) ).
cnf(t2865,plain,
true = relation_of2_as_subset(the_InternalRel(incl_POSet(X1)),X1,X1),
inference(step,[status(thm)],[t2864,t841]) ).
cnf(t866,plain,
relation_of2_as_subset(the_InternalRel(incl_POSet(X1)),X1,X1) = true,
inference(orient,[status(thm)],[t2865]) ).
cnf(t867,plain,
true = ifeq(true,true,relation_of2(the_InternalRel(incl_POSet(X1)),X1,X1),true),
inference(cp,[status(thm)],[t207,t866]) ).
cnf(t2891,plain,
true = relation_of2(the_InternalRel(incl_POSet(X1)),X1,X1),
inference(step,[status(thm)],[t867,t145]) ).
cnf(t984,plain,
relation_of2(the_InternalRel(incl_POSet(X1)),X1,X1) = true,
inference(orient,[status(thm)],[t2891]) ).
cnf(t985,plain,
X1 = ifeq(true,true,ifeq(rel_str_of(X2,the_InternalRel(incl_POSet(X2))),rel_str_of(X3,X1),the_InternalRel(incl_POSet(X2)),X1),X1),
inference(cp,[status(thm)],[t154,t984]) ).
cnf(t2918,plain,
X1 = ifeq(rel_str_of(X2,the_InternalRel(incl_POSet(X2))),rel_str_of(X3,X1),the_InternalRel(incl_POSet(X2)),X1),
inference(step,[status(thm)],[t985,t145]) ).
cnf(t137,plain,
ifeq(rel_str(X1),true,ifeq(strict_rel_str(X1),true,X1,rel_str_of(the_carrier(X1),the_InternalRel(X1))),rel_str_of(the_carrier(X1),the_InternalRel(X1))) = rel_str_of(the_carrier(X1),the_InternalRel(X1)),
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t532,plain,
ifeq(rel_str(X1),true,ifeq(strict_rel_str(X1),true,X1,rel_str_of(the_carrier(X1),the_InternalRel(X1))),rel_str_of(the_carrier(X1),the_InternalRel(X1))) = rel_str_of(the_carrier(X1),the_InternalRel(X1)),
inference(orient,[status(thm)],[t137]) ).
cnf(t844,plain,
rel_str_of(the_carrier(incl_POSet(X1)),the_InternalRel(incl_POSet(X1))) = ifeq(rel_str(incl_POSet(X1)),true,ifeq(strict_rel_str(incl_POSet(X1)),true,incl_POSet(X1),rel_str_of(X1,the_InternalRel(incl_POSet(X1)))),rel_str_of(the_carrier(incl_POSet(X1)),the_InternalRel(incl_POSet(X1)))),
inference(cp,[status(thm)],[t532,t841]) ).
cnf(t2858,plain,
rel_str_of(X1,the_InternalRel(incl_POSet(X1))) = ifeq(rel_str(incl_POSet(X1)),true,ifeq(strict_rel_str(incl_POSet(X1)),true,incl_POSet(X1),rel_str_of(X1,the_InternalRel(incl_POSet(X1)))),rel_str_of(the_carrier(incl_POSet(X1)),the_InternalRel(incl_POSet(X1)))),
inference(step,[status(thm)],[t844,t841]) ).
cnf(t2859,plain,
rel_str_of(X1,the_InternalRel(incl_POSet(X1))) = ifeq(true,true,ifeq(strict_rel_str(incl_POSet(X1)),true,incl_POSet(X1),rel_str_of(X1,the_InternalRel(incl_POSet(X1)))),rel_str_of(the_carrier(incl_POSet(X1)),the_InternalRel(incl_POSet(X1)))),
inference(step,[status(thm)],[t2858,t470]) ).
cnf(t2860,plain,
rel_str_of(X1,the_InternalRel(incl_POSet(X1))) = ifeq(strict_rel_str(incl_POSet(X1)),true,incl_POSet(X1),rel_str_of(X1,the_InternalRel(incl_POSet(X1)))),
inference(step,[status(thm)],[t2859,t145]) ).
cnf(t34,plain,
strict_rel_str(incl_POSet(X1)) = true,
inference(equality_encoding,[status(esa)],[c751]) ).
cnf(t491,plain,
strict_rel_str(incl_POSet(X1)) = true,
inference(orient,[status(thm)],[t34]) ).
cnf(t2861,plain,
rel_str_of(X1,the_InternalRel(incl_POSet(X1))) = ifeq(true,true,incl_POSet(X1),rel_str_of(X1,the_InternalRel(incl_POSet(X1)))),
inference(step,[status(thm)],[t2860,t491]) ).
cnf(t2862,plain,
rel_str_of(X1,the_InternalRel(incl_POSet(X1))) = incl_POSet(X1),
inference(step,[status(thm)],[t2861,t145]) ).
cnf(t853,plain,
rel_str_of(X1,the_InternalRel(incl_POSet(X1))) = incl_POSet(X1),
inference(orient,[status(thm)],[t2862]) ).
cnf(t2919,plain,
X1 = ifeq(incl_POSet(X2),rel_str_of(X3,X1),the_InternalRel(incl_POSet(X2)),X1),
inference(step,[status(thm)],[t2918,t853]) ).
cnf(t1013,plain,
ifeq(incl_POSet(X1),rel_str_of(X2,X3),the_InternalRel(incl_POSet(X1)),X3) = X3,
inference(orient,[status(thm)],[t2919]) ).
cnf(t1014,plain,
inclusion_relation(X1) = ifeq(incl_POSet(X2),incl_POSet(X1),the_InternalRel(incl_POSet(X2)),inclusion_relation(X1)),
inference(cp,[status(thm)],[t1013,t665]) ).
cnf(t1018,plain,
ifeq(incl_POSet(X1),incl_POSet(X2),the_InternalRel(incl_POSet(X1)),inclusion_relation(X2)) = inclusion_relation(X2),
inference(orient,[status(thm)],[t1014]) ).
cnf(t1019,plain,
inclusion_relation(X1) = the_InternalRel(incl_POSet(X1)),
inference(cp,[status(thm)],[t1018,t145]) ).
cnf(t1020,plain,
the_InternalRel(incl_POSet(X1)) = inclusion_relation(X1),
inference(orient,[status(thm)],[t1019]) ).
cnf(t3053,plain,
ifeq(inclusion_relation(sk467),inclusion_relation(sk467),false,true) = true,
inference(step,[status(thm)],[t3052,t1020]) ).
cnf(t3054,plain,
false = true,
inference(step,[status(thm)],[t3053,t145]) ).
cnf(t2752,plain,
false = true,
inference(orient,[status(thm)],[t3054]) ).
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(f64,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(f64_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)],[f64]) ).
fof(f64_sk,plain,
! [A,B,C,D,E] :
( ( ( ( ( ( ( ~ disjoint(B,E)
| ~ in(sk18(A,B,C),E)
| ~ open_subset(E,A)
| ~ element(E,powerset(the_carrier(A))) )
& ~ in(sk18(A,B,C),C) )
| ( disjoint(B,sk19(A,B,C))
& in(sk18(A,B,C),sk19(A,B,C))
& open_subset(sk19(A,B,C),A)
& element(sk19(A,B,C),powerset(the_carrier(A)))
& in(sk18(A,B,C),C) ) )
& in(sk18(A,B,C),the_carrier(A)) )
| C = topstr_closure(A,B) )
& ( ( ( ( disjoint(B,sk17(A,B,C,D))
& in(D,sk17(A,B,C,D))
& open_subset(sk17(A,B,C,D),A)
& element(sk17(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,[sk17,sk18,sk19])],[f64_nnf]) ).
cnf(c187,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)],[f64_sk]) ).
fof(f94,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(f94_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)],[f94]) ).
fof(f94_sk,plain,
! [A,C,B,D] :
( ( ( ( in(ordered_pair(sk53(A,B,C),B),A)
& sk53(A,B,C) != B
& ~ in(sk53(A,B,C),C) )
| ( ( ~ in(ordered_pair(sk53(A,B,C),B),A)
| sk53(A,B,C) = B )
& in(sk53(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,[sk53])],[f94_nnf]) ).
cnf(c342,plain,
( X3 != X1
| ~ in(X3,X2)
| X2 != fiber(X0,X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(esa)],[f94_sk]) ).
fof(f96,axiom,
! [A] :
( A = empty_set
<=> ! [B] : ~ in(B,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d1_xboole_0) ).
fof(f96_nnf,plain,
! [A] :
( ( ? [B] : in(B,A)
| A = empty_set )
& ( ! [B] : ~ in(B,A)
| A != empty_set ) ),
inference(nnf_transformation,[status(thm)],[f96]) ).
fof(f96_sk,plain,
! [A,B] :
( ( in(sk56(A),A)
| A = empty_set )
& ( ~ in(B,A)
| A != empty_set ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk56])],[f96_nnf]) ).
cnf(c360,plain,
( ~ in(X1,X0)
| X0 != empty_set ),
inference(cnf_transformation,[status(esa)],[f96_sk]) ).
fof(f101,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(f101_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)],[f101]) ).
fof(f101_sk,plain,
! [A,B] :
( ( ( set_meet(sk59(A)) = empty_set
& finite(sk59(A))
& subset(sk59(A),A)
& sk59(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,[sk59])],[f101_nnf]) ).
cnf(c375,plain,
( X0 != empty_set
| ~ centered(X0) ),
inference(cnf_transformation,[status(esa)],[f101_sk]) ).
fof(f110,axiom,
! [A,B] :
( element(B,A)
=> ( proper_element(B,A)
<=> B != union(A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d2_tex_2) ).
fof(f110_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)],[f110]) ).
fof(f110_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)],[f110_nnf]) ).
cnf(c409,plain,
( X1 != union(X0)
| ~ proper_element(X1,X0)
| ~ element(X1,X0) ),
inference(cnf_transformation,[status(esa)],[f110_sk]) ).
fof(f133,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(f133_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)],[f133]) ).
fof(f133_sk,plain,
! [C,A,B,D] :
( ( ( ~ in(sk94(A,B,C),B)
& in(sk94(A,B,C),A)
& ~ in(sk94(A,B,C),C) )
| ( ( in(sk94(A,B,C),B)
| ~ in(sk94(A,B,C),A) )
& in(sk94(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,[sk94])],[f133_nnf]) ).
cnf(c522,plain,
( ~ in(X3,X1)
| ~ in(X3,X2)
| X2 != set_difference(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f133_sk]) ).
fof(f162,axiom,
! [A,B] :
( proper_subset(A,B)
<=> ( A != B
& subset(A,B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d8_xboole_0) ).
fof(f162_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)],[f162]) ).
fof(f162_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)],[f162_nnf]) ).
cnf(c664,plain,
( X0 != X1
| ~ proper_subset(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f162_sk]) ).
fof(f286,axiom,
! [A] :
( finite(singleton(A))
& ~ empty(singleton(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_finset_1) ).
fof(f286_nnf,plain,
! [A] :
( finite(singleton(A))
& ~ empty(singleton(A)) ),
inference(nnf_transformation,[status(thm)],[f286]) ).
fof(f286_sk,plain,
! [A] :
( finite(singleton(A))
& ~ empty(singleton(A)) ),
inference(skolemisation,[status(esa)],[f286_nnf]) ).
cnf(c848,plain,
~ empty(singleton(X0)),
inference(cnf_transformation,[status(esa)],[f286_sk]) ).
fof(f287,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(f287_nnf,plain,
! [A] :
( preboolean(powerset(A))
& diff_closed(powerset(A))
& cup_closed(powerset(A))
& ~ empty(powerset(A)) ),
inference(nnf_transformation,[status(thm)],[f287]) ).
fof(f287_sk,plain,
! [A] :
( preboolean(powerset(A))
& diff_closed(powerset(A))
& cup_closed(powerset(A))
& ~ empty(powerset(A)) ),
inference(skolemisation,[status(esa)],[f287_nnf]) ).
cnf(c850,plain,
~ empty(powerset(X0)),
inference(cnf_transformation,[status(esa)],[f287_sk]) ).
fof(f289,axiom,
! [A] :
( strict_latt_str(boole_lattice(A))
& ~ empty_carrier(boole_lattice(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_lattice3) ).
fof(f289_nnf,plain,
! [A] :
( strict_latt_str(boole_lattice(A))
& ~ empty_carrier(boole_lattice(A)) ),
inference(nnf_transformation,[status(thm)],[f289]) ).
fof(f289_sk,plain,
! [A] :
( strict_latt_str(boole_lattice(A))
& ~ empty_carrier(boole_lattice(A)) ),
inference(skolemisation,[status(esa)],[f289_nnf]) ).
cnf(c856,plain,
~ empty_carrier(boole_lattice(X0)),
inference(cnf_transformation,[status(esa)],[f289_sk]) ).
fof(f291,axiom,
! [A] : ~ empty(succ(A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_ordinal1) ).
fof(f291_nnf,plain,
! [A] : ~ empty(succ(A)),
inference(nnf_transformation,[status(thm)],[f291]) ).
fof(f291_sk,plain,
! [A] : ~ empty(succ(A)),
inference(skolemisation,[status(esa)],[f291_nnf]) ).
cnf(c860,plain,
~ empty(succ(X0)),
inference(cnf_transformation,[status(esa)],[f291_sk]) ).
fof(f292,axiom,
( ~ empty(omega)
& ordinal(omega)
& epsilon_connected(omega)
& epsilon_transitive(omega) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_ordinal2) ).
fof(f292_nnf,plain,
( ~ empty(omega)
& ordinal(omega)
& epsilon_connected(omega)
& epsilon_transitive(omega) ),
inference(nnf_transformation,[status(thm)],[f292]) ).
fof(f292_sk,plain,
( ~ empty(omega)
& ordinal(omega)
& epsilon_connected(omega)
& epsilon_transitive(omega) ),
inference(skolemisation,[status(esa)],[f292_nnf]) ).
cnf(c864,plain,
~ empty(omega),
inference(cnf_transformation,[status(esa)],[f292_sk]) ).
fof(f296,axiom,
! [A] : ~ empty(powerset(A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_subset_1) ).
fof(f296_nnf,plain,
! [A] : ~ empty(powerset(A)),
inference(nnf_transformation,[status(thm)],[f296]) ).
fof(f296_sk,plain,
! [A] : ~ empty(powerset(A)),
inference(skolemisation,[status(esa)],[f296_nnf]) ).
cnf(c873,plain,
~ empty(powerset(X0)),
inference(cnf_transformation,[status(esa)],[f296_sk]) ).
fof(f298,axiom,
! [A,B] : ~ empty(ordered_pair(A,B)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_zfmisc_1) ).
fof(f298_nnf,plain,
! [A,B] : ~ empty(ordered_pair(A,B)),
inference(nnf_transformation,[status(thm)],[f298]) ).
fof(f298_sk,plain,
! [A,B] : ~ empty(ordered_pair(A,B)),
inference(skolemisation,[status(esa)],[f298_nnf]) ).
cnf(c875,plain,
~ empty(ordered_pair(X0,X1)),
inference(cnf_transformation,[status(esa)],[f298_sk]) ).
fof(f302,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(f302_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)],[f302]) ).
fof(f302_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)],[f302_nnf]) ).
cnf(c880,plain,
( ~ empty(succ(X0))
| ~ natural(X0)
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(esa)],[f302_sk]) ).
fof(f303,axiom,
! [A,B] :
( finite(unordered_pair(A,B))
& ~ empty(unordered_pair(A,B)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc2_finset_1) ).
fof(f303_nnf,plain,
! [A,B] :
( finite(unordered_pair(A,B))
& ~ empty(unordered_pair(A,B)) ),
inference(nnf_transformation,[status(thm)],[f303]) ).
fof(f303_sk,plain,
! [A,B] :
( finite(unordered_pair(A,B))
& ~ empty(unordered_pair(A,B)) ),
inference(skolemisation,[status(esa)],[f303_nnf]) ).
cnf(c885,plain,
~ empty(unordered_pair(X0,X1)),
inference(cnf_transformation,[status(esa)],[f303_sk]) ).
fof(f306,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(f306_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)],[f306]) ).
fof(f306_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)],[f306_nnf]) ).
cnf(c894,plain,
~ empty_carrier(boole_lattice(X0)),
inference(cnf_transformation,[status(esa)],[f306_sk]) ).
fof(f312,axiom,
! [A] : ~ empty(singleton(A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc2_subset_1) ).
fof(f312_nnf,plain,
! [A] : ~ empty(singleton(A)),
inference(nnf_transformation,[status(thm)],[f312]) ).
fof(f312_sk,plain,
! [A] : ~ empty(singleton(A)),
inference(skolemisation,[status(esa)],[f312_nnf]) ).
cnf(c924,plain,
~ empty(singleton(X0)),
inference(cnf_transformation,[status(esa)],[f312_sk]) ).
fof(f329,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(f329_nnf,plain,
! [A] :
( ( ordinal(succ(A))
& epsilon_connected(succ(A))
& epsilon_transitive(succ(A))
& ~ empty(succ(A)) )
| ~ ordinal(A) ),
inference(nnf_transformation,[status(thm)],[f329]) ).
fof(f329_sk,plain,
! [A] :
( ( ordinal(succ(A))
& epsilon_connected(succ(A))
& epsilon_transitive(succ(A))
& ~ empty(succ(A)) )
| ~ ordinal(A) ),
inference(skolemisation,[status(esa)],[f329_nnf]) ).
cnf(c972,plain,
( ~ empty(succ(X0))
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(esa)],[f329_sk]) ).
fof(f331,axiom,
! [A,B] : ~ empty(unordered_pair(A,B)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc3_subset_1) ).
fof(f331_nnf,plain,
! [A,B] : ~ empty(unordered_pair(A,B)),
inference(nnf_transformation,[status(thm)],[f331]) ).
fof(f331_sk,plain,
! [A,B] : ~ empty(unordered_pair(A,B)),
inference(skolemisation,[status(esa)],[f331_nnf]) ).
cnf(c977,plain,
~ empty(unordered_pair(X0,X1)),
inference(cnf_transformation,[status(esa)],[f331_sk]) ).
fof(f368,axiom,
! [A,B] : ~ proper_subset(A,A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',irreflexivity_r2_xboole_0) ).
fof(f368_nnf,plain,
! [A,B] : ~ proper_subset(A,A),
inference(nnf_transformation,[status(thm)],[f368]) ).
fof(f368_sk,plain,
! [A] : ~ proper_subset(A,A),
inference(skolemisation,[status(esa)],[f368_nnf]) ).
cnf(c1066,plain,
~ proper_subset(X0,X0),
inference(cnf_transformation,[status(esa)],[f368_sk]) ).
fof(f370,lemma,
! [A] : singleton(A) != empty_set,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l1_zfmisc_1) ).
fof(f370_nnf,plain,
! [A] : singleton(A) != empty_set,
inference(nnf_transformation,[status(thm)],[f370]) ).
fof(f370_sk,plain,
! [A] : singleton(A) != empty_set,
inference(skolemisation,[status(esa)],[f370_nnf]) ).
cnf(c1070,plain,
singleton(X0) != empty_set,
inference(cnf_transformation,[status(esa)],[f370_sk]) ).
fof(f372,lemma,
! [A,B] :
~ ( in(A,B)
& disjoint(singleton(A),B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l25_zfmisc_1) ).
fof(f372_nnf,plain,
! [A,B] :
( ~ in(A,B)
| ~ disjoint(singleton(A),B) ),
inference(nnf_transformation,[status(thm)],[f372]) ).
fof(f372_sk,plain,
! [A,B] :
( ~ in(A,B)
| ~ disjoint(singleton(A),B) ),
inference(skolemisation,[status(esa)],[f372_nnf]) ).
cnf(c1072,plain,
( ~ in(X0,X1)
| ~ disjoint(singleton(X0),X1) ),
inference(cnf_transformation,[status(esa)],[f372_sk]) ).
fof(f389,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(f389_nnf,plain,
? [A] :
( natural(A)
& ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A)
& ~ empty(A) ),
inference(nnf_transformation,[status(thm)],[f389]) ).
fof(f389_sk,plain,
( natural(sk158)
& ordinal(sk158)
& epsilon_connected(sk158)
& epsilon_transitive(sk158)
& ~ empty(sk158) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk158])],[f389_nnf]) ).
cnf(c1111,plain,
~ empty(sk158),
inference(cnf_transformation,[status(esa)],[f389_sk]) ).
fof(f390,axiom,
? [A] :
( finite(A)
& ~ empty(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc1_finset_1) ).
fof(f390_nnf,plain,
? [A] :
( finite(A)
& ~ empty(A) ),
inference(nnf_transformation,[status(thm)],[f390]) ).
fof(f390_sk,plain,
( finite(sk159)
& ~ empty(sk159) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk159])],[f390_nnf]) ).
cnf(c1116,plain,
~ empty(sk159),
inference(cnf_transformation,[status(esa)],[f390_sk]) ).
fof(f393,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(f393_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)],[f393]) ).
fof(f393_sk,plain,
( v5_membered(sk162)
& v4_membered(sk162)
& v3_membered(sk162)
& v2_membered(sk162)
& v1_membered(sk162)
& ~ empty(sk162) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk162])],[f393_nnf]) ).
cnf(c1124,plain,
~ empty(sk162),
inference(cnf_transformation,[status(esa)],[f393_sk]) ).
fof(f405,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(f405_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)],[f405]) ).
fof(f405_sk,plain,
( antisymmetric_relstr(sk174)
& transitive_relstr(sk174)
& reflexive_relstr(sk174)
& strict_rel_str(sk174)
& ~ empty_carrier(sk174)
& rel_str(sk174) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk174])],[f405_nnf]) ).
cnf(c1171,plain,
~ empty_carrier(sk174),
inference(cnf_transformation,[status(esa)],[f405_sk]) ).
fof(f408,axiom,
? [A] :
( relation(A)
& ~ empty(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc2_relat_1) ).
fof(f408_nnf,plain,
? [A] :
( relation(A)
& ~ empty(A) ),
inference(nnf_transformation,[status(thm)],[f408]) ).
fof(f408_sk,plain,
( relation(sk177)
& ~ empty(sk177) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk177])],[f408_nnf]) ).
cnf(c1186,plain,
~ empty(sk177),
inference(cnf_transformation,[status(esa)],[f408_sk]) ).
fof(f410,axiom,
! [A] :
? [B] :
( ~ proper_element(B,powerset(A))
& element(B,powerset(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc2_tex_2) ).
fof(f410_nnf,plain,
! [A] :
? [B] :
( ~ proper_element(B,powerset(A))
& element(B,powerset(A)) ),
inference(nnf_transformation,[status(thm)],[f410]) ).
fof(f410_sk,plain,
! [A] :
( ~ proper_element(sk179(A),powerset(A))
& element(sk179(A),powerset(A)) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk179])],[f410_nnf]) ).
cnf(c1191,plain,
~ proper_element(sk179(X0),powerset(X0)),
inference(cnf_transformation,[status(esa)],[f410_sk]) ).
fof(f412,axiom,
? [A] : ~ empty(A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc2_xboole_0) ).
fof(f412_nnf,plain,
? [A] : ~ empty(A),
inference(nnf_transformation,[status(thm)],[f412]) ).
fof(f412_sk,plain,
~ empty(sk181),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk181])],[f412_nnf]) ).
cnf(c1195,plain,
~ empty(sk181),
inference(cnf_transformation,[status(esa)],[f412_sk]) ).
fof(f416,axiom,
? [A] :
( ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A)
& ~ empty(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc3_ordinal1) ).
fof(f416_nnf,plain,
? [A] :
( ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A)
& ~ empty(A) ),
inference(nnf_transformation,[status(thm)],[f416]) ).
fof(f416_sk,plain,
( ordinal(sk185)
& epsilon_connected(sk185)
& epsilon_transitive(sk185)
& ~ empty(sk185) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk185])],[f416_nnf]) ).
cnf(c1204,plain,
~ empty(sk185),
inference(cnf_transformation,[status(esa)],[f416_sk]) ).
fof(f419,axiom,
? [A] :
( ~ empty_carrier(A)
& one_sorted_str(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc3_struct_0) ).
fof(f419_nnf,plain,
? [A] :
( ~ empty_carrier(A)
& one_sorted_str(A) ),
inference(nnf_transformation,[status(thm)],[f419]) ).
fof(f419_sk,plain,
( ~ empty_carrier(sk188)
& one_sorted_str(sk188) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk188])],[f419_nnf]) ).
cnf(c1218,plain,
~ empty_carrier(sk188),
inference(cnf_transformation,[status(esa)],[f419_sk]) ).
fof(f423,axiom,
? [A] :
( strict_latt_str(A)
& ~ empty_carrier(A)
& latt_str(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc6_lattices) ).
fof(f423_nnf,plain,
? [A] :
( strict_latt_str(A)
& ~ empty_carrier(A)
& latt_str(A) ),
inference(nnf_transformation,[status(thm)],[f423]) ).
fof(f423_sk,plain,
( strict_latt_str(sk192)
& ~ empty_carrier(sk192)
& latt_str(sk192) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk192])],[f423_nnf]) ).
cnf(c1228,plain,
~ empty_carrier(sk192),
inference(cnf_transformation,[status(esa)],[f423_sk]) ).
fof(f426,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(f426_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)],[f426]) ).
fof(f426_sk,plain,
( lattice(sk195)
& join_absorbing(sk195)
& meet_absorbing(sk195)
& meet_associative(sk195)
& meet_commutative(sk195)
& join_associative(sk195)
& join_commutative(sk195)
& strict_latt_str(sk195)
& ~ empty_carrier(sk195)
& latt_str(sk195) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk195])],[f426_nnf]) ).
cnf(c1236,plain,
~ empty_carrier(sk195),
inference(cnf_transformation,[status(esa)],[f426_sk]) ).
fof(f462,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(f462_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)],[f462]) ).
fof(f462_sk,plain,
! [B,E,G,I,K,L,N,P,D,R,T] :
( ( ( T = sk229(D,R)
| ~ subset(sk229(D,R),T)
| ~ in(T,R) )
& in(sk229(D,R),R) )
| R = empty_set
| ~ element(R,powerset(powerset(D)))
| ~ in(D,omega)
| ~ ordinal(D)
| ( ( ( sk228(P) != P
& subset(P,sk228(P))
& in(sk228(P),sk227) )
| ~ in(P,sk227) )
& sk227 != empty_set
& element(sk227,powerset(powerset(sk225)))
& in(sk225,omega)
& sk225 != empty_set
& ( ( ( N = sk226(K,L)
| ~ subset(sk226(K,L),N)
| ~ in(N,L) )
& in(sk226(K,L),L) )
| L = empty_set
| ~ element(L,powerset(powerset(K)))
| ~ in(K,omega)
| ~ in(K,sk225)
| ~ ordinal(K) )
& being_limit_ordinal(sk225)
& ordinal(sk225) )
| ( ( ( sk224(I) != I
& subset(I,sk224(I))
& in(sk224(I),sk223) )
| ~ in(I,sk223) )
& sk223 != empty_set
& element(sk223,powerset(powerset(succ(sk221))))
& in(succ(sk221),omega)
& ( ( ( G = sk222(E)
| ~ subset(sk222(E),G)
| ~ in(G,E) )
& in(sk222(E),E) )
| E = empty_set
| ~ element(E,powerset(powerset(sk221)))
| ~ in(sk221,omega) )
& ordinal(sk221) )
| ( ( ( sk220(B) != B
& subset(B,sk220(B))
& in(sk220(B),sk219) )
| ~ in(B,sk219) )
& sk219 != empty_set
& element(sk219,powerset(powerset(empty_set)))
& in(empty_set,omega) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk219,sk220,sk221,sk222,sk223,sk224,sk225,sk226,sk227,sk228,sk229])],[f462_nnf]) ).
cnf(c1478,plain,
( sk220(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])],[f462_sk]) ).
cnf(c1483,plain,
( sk219 != 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])],[f462_sk]) ).
cnf(c1492,plain,
( ~ subset(sk222(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])],[f462_sk]) ).
cnf(c1514,plain,
( sk224(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])],[f462_sk]) ).
cnf(c1519,plain,
( sk223 != 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])],[f462_sk]) ).
cnf(c1537,plain,
( ~ subset(sk226(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])],[f462_sk]) ).
cnf(c1568,plain,
( sk228(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])],[f462_sk]) ).
cnf(c1573,plain,
( sk227 != 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])],[f462_sk]) ).
cnf(c1582,plain,
( sk225 != 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])],[f462_sk]) ).
cnf(c1594,plain,
( ~ subset(sk229(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])],[f462_sk]) ).
fof(f627,lemma,
! [A,B,C] :
~ ( in(C,A)
& in(B,C)
& in(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t3_ordinal1) ).
fof(f627_nnf,plain,
! [A,B,C] :
( ~ in(C,A)
| ~ in(B,C)
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f627]) ).
fof(f627_sk,plain,
! [A,B,C] :
( ~ in(C,A)
| ~ in(B,C)
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f627_nnf]) ).
cnf(c3205,plain,
( ~ in(X2,X0)
| ~ in(X1,X2)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f627_sk]) ).
fof(f630,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(f630_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)],[f630]) ).
fof(f630_sk,plain,
! [A,B,C] :
( ( ~ disjoint(A,B)
| ~ in(C,B)
| ~ in(C,A) )
& ( ( in(sk481(A,B),B)
& in(sk481(A,B),A) )
| disjoint(A,B) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk481])],[f630_nnf]) ).
cnf(c3211,plain,
( ~ disjoint(X0,X1)
| ~ in(X2,X1)
| ~ in(X2,X0) ),
inference(cnf_transformation,[status(esa)],[f630_sk]) ).
fof(f634,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(f634_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)],[f634]) ).
fof(f634_sk,plain,
! [A,B] :
( ( ( ~ being_limit_ordinal(A)
| A != succ(B)
| ~ ordinal(B) )
& ( ( A = succ(sk483(A))
& ordinal(sk483(A)) )
| being_limit_ordinal(A) ) )
| ~ ordinal(A) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk483])],[f634_nnf]) ).
cnf(c3220,plain,
( ~ being_limit_ordinal(X0)
| X0 != succ(X1)
| ~ ordinal(X1)
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(esa)],[f634_sk]) ).
fof(f658,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(f658_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)],[f658]) ).
fof(f658_sk,plain,
! [A,B,C] :
( ( ~ disjoint(A,B)
| ~ in(C,set_intersection2(A,B)) )
& ( in(sk487(A,B),set_intersection2(A,B))
| disjoint(A,B) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk487])],[f658_nnf]) ).
cnf(c3259,plain,
( ~ disjoint(X0,X1)
| ~ in(X2,set_intersection2(X0,X1)) ),
inference(cnf_transformation,[status(esa)],[f658_sk]) ).
fof(f665,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(f665_nnf,plain,
! [A,B,C] :
( ~ in(B,C)
| ~ in(B,subset_complement(A,C))
| ~ element(C,powerset(A)) ),
inference(nnf_transformation,[status(thm)],[f665]) ).
fof(f665_sk,plain,
! [C,A,B] :
( ~ in(B,C)
| ~ in(B,subset_complement(A,C))
| ~ element(C,powerset(A)) ),
inference(skolemisation,[status(esa)],[f665_nnf]) ).
cnf(c3288,plain,
( ~ in(X1,X2)
| ~ in(X1,subset_complement(X0,X2))
| ~ element(X2,powerset(X0)) ),
inference(cnf_transformation,[status(esa)],[f665_sk]) ).
fof(f672,axiom,
! [A,B,C] :
~ ( empty(C)
& element(B,powerset(C))
& in(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t5_subset) ).
fof(f672_nnf,plain,
! [A,B,C] :
( ~ empty(C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f672]) ).
fof(f672_sk,plain,
! [A,B,C] :
( ~ empty(C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f672_nnf]) ).
cnf(c3298,plain,
( ~ empty(X2)
| ~ element(X1,powerset(X2))
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f672_sk]) ).
fof(f673,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(f673_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)],[f673]) ).
fof(f673_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)],[f673_nnf]) ).
cnf(c3299,plain,
( X1 != X0
| ~ proper_element(X1,powerset(X0))
| ~ element(X1,powerset(X0)) ),
inference(cnf_transformation,[status(esa)],[f673_sk]) ).
fof(f678,lemma,
! [A,B] :
~ ( proper_subset(B,A)
& subset(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t60_xboole_1) ).
fof(f678_nnf,plain,
! [A,B] :
( ~ proper_subset(B,A)
| ~ subset(A,B) ),
inference(nnf_transformation,[status(thm)],[f678]) ).
fof(f678_sk,plain,
! [A,B] :
( ~ proper_subset(B,A)
| ~ subset(A,B) ),
inference(skolemisation,[status(esa)],[f678_nnf]) ).
cnf(c3307,plain,
( ~ proper_subset(X1,X0)
| ~ subset(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f678_sk]) ).
fof(f685,lemma,
! [A,B] :
( set_difference(A,singleton(B)) = A
<=> ~ in(B,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t65_zfmisc_1) ).
fof(f685_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)],[f685]) ).
fof(f685_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)],[f685_nnf]) ).
cnf(c3316,plain,
( ~ in(X1,X0)
| set_difference(X0,singleton(X1)) != X0 ),
inference(cnf_transformation,[status(esa)],[f685_sk]) ).
fof(f697,axiom,
! [A,B] :
~ ( empty(B)
& in(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t7_boole) ).
fof(f697_nnf,plain,
! [A,B] :
( ~ empty(B)
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f697]) ).
fof(f697_sk,plain,
! [A,B] :
( ~ empty(B)
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f697_nnf]) ).
cnf(c3336,plain,
( ~ empty(X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f697_sk]) ).
fof(f700,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(f700_nnf,plain,
! [A,B] :
( ? [C] :
( ! [D] :
( ~ in(D,C)
| ~ in(D,B) )
& in(C,B) )
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f700]) ).
fof(f700_sk,plain,
! [A,B,D] :
( ( ( ~ in(D,sk493(A,B))
| ~ in(D,B) )
& in(sk493(A,B),B) )
| ~ in(A,B) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk493])],[f700_nnf]) ).
cnf(c3342,plain,
( ~ in(X3,sk493(X0,X1))
| ~ in(X3,X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f700_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c2,c3,c187,c342,c360,c375,c409,c522,c664,c848,c850,c856,c860,c864,c873,c875,c880,c885,c894,c924,c972,c977,c1066,c1070,c1072,c1111,c1116,c1124,c1171,c1186,c1191,c1195,c1204,c1218,c1228,c1236,c1478,c1483,c1492,c1514,c1519,c1537,c1568,c1573,c1582,c1594,c3080,c3205,c3211,c3220,c3259,c3288,c3298,c3299,c3307,c3316,c3336,c3342]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t2752]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU368+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.07 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.18/0.44 % Computer : n002.cluster.edu
% 0.18/0.44 % Model : x86_64 x86_64
% 0.18/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.44 % Memory : 8046.5625MB
% 0.18/0.44 % OS : Linux 6.8.0-71-generic
% 0.18/0.44 % CPULimit : 300
% 0.18/0.44 % WCLimit : 300
% 0.18/0.44 % DateTime : Thu Sep 24 13:54:35 UTC 2026
% 0.18/0.44 % CPUTime :
% 0.18/0.44 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 135.80/18.71 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 135.80/18.71 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------