%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SEU374+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n001.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:53 PM UTC 2026
% Result : Theorem 80.06s 10.52s
% Output : Proof 80.06s
% Verified :
% SZS Type : Refutation
% Derivation depth : 53
% Number of leaves : 79
% Syntax : Number of formulae : 485 ( 241 unt; 0 def)
% Number of atoms : 1720 ( 329 equ)
% Maximal formula atoms : 49 ( 3 avg)
% Number of connectives : 1856 ( 621 ~; 349 |; 793 &)
% ( 17 <=>; 76 =>; 0 <=; 0 <~>)
% Maximal formula depth : 27 ( 4 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 73 ( 71 usr; 1 prp; 0-3 aty)
% Number of functors : 72 ( 72 usr; 34 con; 0-4 aty)
% Number of variables : 715 ( 50 sgn 404 !; 70 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f181,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/sandbox2/benchmark/theBenchmark.p',d9_orders_2) ).
fof(f181_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)],[f181]) ).
fof(f181_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)],[f181_nnf]) ).
cnf(c742,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)],[f181_sk]) ).
cnf(t179,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)],[c742]) ).
cnf(t275,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)],[t179]) ).
fof(f404,lemma,
! [A,B] :
( subset(singleton(A),B)
<=> in(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l2_zfmisc_1) ).
fof(f404_nnf,plain,
! [A,B] :
( ( ~ in(A,B)
| subset(singleton(A),B) )
& ( in(A,B)
| ~ subset(singleton(A),B) ) ),
inference(nnf_transformation,[status(thm)],[f404]) ).
fof(f404_sk,plain,
! [A,B] :
( ( ~ in(A,B)
| subset(singleton(A),B) )
& ( in(A,B)
| ~ subset(singleton(A),B) ) ),
inference(skolemisation,[status(esa)],[f404_nnf]) ).
cnf(c1222,plain,
( in(X0,X1)
| ~ subset(singleton(X0),X1) ),
inference(cnf_transformation,[status(esa)],[f404_sk]) ).
cnf(t107,plain,
ifeq(subset(singleton(X1),X2),true,in(X1,X2),true) = true,
inference(equality_encoding,[status(esa)],[c1222]) ).
cnf(t254,plain,
ifeq(subset(singleton(X1),X2),true,in(X1,X2),true) = true,
inference(orient,[status(thm)],[t107]) ).
fof(f406,lemma,
! [A,B] :
( set_difference(A,B) = empty_set
<=> subset(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l32_xboole_1) ).
fof(f406_nnf,plain,
! [A,B] :
( ( ~ subset(A,B)
| set_difference(A,B) = empty_set )
& ( subset(A,B)
| set_difference(A,B) != empty_set ) ),
inference(nnf_transformation,[status(thm)],[f406]) ).
fof(f406_sk,plain,
! [A,B] :
( ( ~ subset(A,B)
| set_difference(A,B) = empty_set )
& ( subset(A,B)
| set_difference(A,B) != empty_set ) ),
inference(skolemisation,[status(esa)],[f406_nnf]) ).
cnf(c1226,plain,
( subset(X0,X1)
| set_difference(X0,X1) != empty_set ),
inference(cnf_transformation,[status(esa)],[f406_sk]) ).
cnf(t99,plain,
ifeq(set_difference(X1,X2),empty_set,subset(X1,X2),true) = true,
inference(equality_encoding,[status(esa)],[c1226]) ).
cnf(t272,plain,
ifeq(set_difference(X1,X2),empty_set,subset(X1,X2),true) = true,
inference(orient,[status(thm)],[t99]) ).
cnf(c1227,plain,
( ~ subset(X0,X1)
| set_difference(X0,X1) = empty_set ),
inference(cnf_transformation,[status(esa)],[f406_sk]) ).
cnf(t101,plain,
ifeq(subset(X1,X2),true,set_difference(X1,X2),empty_set) = empty_set,
inference(equality_encoding,[status(esa)],[c1227]) ).
cnf(t762,plain,
ifeq(subset(X1,X2),true,set_difference(X1,X2),empty_set) = empty_set,
inference(orient,[status(thm)],[t101]) ).
fof(f654,lemma,
! [A,B,C] :
( subset(A,B)
=> subset(set_difference(A,C),set_difference(B,C)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t33_xboole_1) ).
fof(f654_nnf,plain,
! [A,B,C] :
( subset(set_difference(A,C),set_difference(B,C))
| ~ subset(A,B) ),
inference(nnf_transformation,[status(thm)],[f654]) ).
fof(f654_sk,plain,
! [A,B,C] :
( subset(set_difference(A,C),set_difference(B,C))
| ~ subset(A,B) ),
inference(skolemisation,[status(esa)],[f654_nnf]) ).
cnf(c3431,plain,
( subset(set_difference(X0,X2),set_difference(X1,X2))
| ~ subset(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f654_sk]) ).
cnf(t137,plain,
ifeq(subset(X1,X2),true,subset(set_difference(X1,X3),set_difference(X2,X3)),true) = true,
inference(equality_encoding,[status(esa)],[c3431]) ).
cnf(t249,plain,
ifeq(subset(X1,X2),true,subset(set_difference(X1,X3),set_difference(X2,X3)),true) = true,
inference(orient,[status(thm)],[t137]) ).
fof(f659,lemma,
! [A,B] : subset(set_difference(A,B),A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t36_xboole_1) ).
fof(f659_nnf,plain,
! [A,B] : subset(set_difference(A,B),A),
inference(nnf_transformation,[status(thm)],[f659]) ).
fof(f659_sk,plain,
! [A,B] : subset(set_difference(A,B),A),
inference(skolemisation,[status(esa)],[f659_nnf]) ).
cnf(c3444,plain,
subset(set_difference(X0,X1),X0),
inference(cnf_transformation,[status(esa)],[f659_sk]) ).
cnf(t61,plain,
subset(set_difference(X1,X2),X1) = true,
inference(equality_encoding,[status(esa)],[c3444]) ).
cnf(t486,plain,
subset(set_difference(X1,X2),X1) = true,
inference(orient,[status(thm)],[t61]) ).
cnf(t490,plain,
true = ifeq(true,true,subset(set_difference(set_difference(X1,X2),X3),set_difference(X1,X3)),true),
inference(cp,[status(thm)],[t249,t486]) ).
cnf(t56,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t182,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t56]) ).
cnf(t8415,plain,
true = subset(set_difference(set_difference(X1,X2),X3),set_difference(X1,X3)),
inference(step,[status(thm)],[t490,t182]) ).
cnf(t2140,plain,
subset(set_difference(set_difference(X1,X2),X3),set_difference(X1,X3)) = true,
inference(orient,[status(thm)],[t8415]) ).
cnf(t2162,plain,
empty_set = ifeq(true,true,set_difference(set_difference(set_difference(X1,X2),X3),set_difference(X1,X3)),empty_set),
inference(cp,[status(thm)],[t762,t2140]) ).
cnf(t8440,plain,
empty_set = set_difference(set_difference(set_difference(X1,X2),X3),set_difference(X1,X3)),
inference(step,[status(thm)],[t2162,t182]) ).
cnf(t2370,plain,
set_difference(set_difference(set_difference(X1,X2),X3),set_difference(X1,X3)) = empty_set,
inference(orient,[status(thm)],[t8440]) ).
fof(f79,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/sandbox2/benchmark/theBenchmark.p',d13_yellow_0) ).
fof(f79_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)],[f79]) ).
fof(f79_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)],[f79_nnf]) ).
cnf(c261,plain,
( subset(the_InternalRel(X1),the_InternalRel(X0))
| ~ subrelstr(X1,X0)
| ~ rel_str(X1)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(esa)],[f79_sk]) ).
cnf(t170,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)],[c261]) ).
cnf(t287,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)],[t170]) ).
fof(f178,axiom,
! [A] :
( one_sorted_str(A)
=> ! [B] :
( net_str(B,A)
=> ! [C] :
( net_str(C,A)
=> ( subnetstr(C,A,B)
<=> ( the_mapping(A,C) = relation_dom_restr_as_relation_of(the_carrier(B),the_carrier(A),the_mapping(A,B),the_carrier(C))
& subrelstr(C,B) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d8_yellow_6) ).
fof(f178_nnf,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( ( the_mapping(A,C) != relation_dom_restr_as_relation_of(the_carrier(B),the_carrier(A),the_mapping(A,B),the_carrier(C))
| ~ subrelstr(C,B)
| subnetstr(C,A,B) )
& ( ( the_mapping(A,C) = relation_dom_restr_as_relation_of(the_carrier(B),the_carrier(A),the_mapping(A,B),the_carrier(C))
& subrelstr(C,B) )
| ~ subnetstr(C,A,B) ) )
| ~ net_str(C,A) )
| ~ net_str(B,A) )
| ~ one_sorted_str(A) ),
inference(nnf_transformation,[status(thm)],[f178]) ).
fof(f178_sk,plain,
! [A,B,C] :
( ( ( the_mapping(A,C) != relation_dom_restr_as_relation_of(the_carrier(B),the_carrier(A),the_mapping(A,B),the_carrier(C))
| ~ subrelstr(C,B)
| subnetstr(C,A,B) )
& ( ( the_mapping(A,C) = relation_dom_restr_as_relation_of(the_carrier(B),the_carrier(A),the_mapping(A,B),the_carrier(C))
& subrelstr(C,B) )
| ~ subnetstr(C,A,B) ) )
| ~ net_str(C,A)
| ~ net_str(B,A)
| ~ one_sorted_str(A) ),
inference(skolemisation,[status(esa)],[f178_nnf]) ).
cnf(c733,plain,
( subrelstr(X2,X1)
| ~ subnetstr(X2,X0,X1)
| ~ net_str(X2,X0)
| ~ net_str(X1,X0)
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[status(esa)],[f178_sk]) ).
cnf(t174,plain,
ifeq(one_sorted_str(X1),true,ifeq(net_str(X2,X1),true,ifeq(net_str(X3,X1),true,ifeq(subnetstr(X3,X1,X2),true,subrelstr(X3,X2),true),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c733]) ).
cnf(t308,plain,
ifeq(one_sorted_str(X1),true,ifeq(net_str(X2,X1),true,ifeq(net_str(X3,X1),true,ifeq(subnetstr(X3,X1,X2),true,subrelstr(X3,X2),true),true),true),true) = true,
inference(orient,[status(thm)],[t174]) ).
fof(f604,conjecture,
! [A] :
( one_sorted_str(A)
=> ! [B] :
( net_str(B,A)
=> ! [C] :
( subnetstr(C,A,B)
=> ! [D] :
( element(D,the_carrier(B))
=> ! [E] :
( element(E,the_carrier(B))
=> ! [F] :
( element(F,the_carrier(C))
=> ! [G] :
( element(G,the_carrier(C))
=> ( ( related(C,F,G)
& E = G
& D = F )
=> related(B,D,E) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t20_yellow_6) ).
fof(f604_neg,negated_conjecture,
~ ! [A] :
( one_sorted_str(A)
=> ! [B] :
( net_str(B,A)
=> ! [C] :
( subnetstr(C,A,B)
=> ! [D] :
( element(D,the_carrier(B))
=> ! [E] :
( element(E,the_carrier(B))
=> ! [F] :
( element(F,the_carrier(C))
=> ! [G] :
( element(G,the_carrier(C))
=> ( ( related(C,F,G)
& E = G
& D = F )
=> related(B,D,E) ) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f604]) ).
fof(f604_nnf,plain,
? [A] :
( ? [B] :
( ? [C] :
( ? [D] :
( ? [E] :
( ? [F] :
( ? [G] :
( ~ related(B,D,E)
& related(C,F,G)
& E = G
& D = F
& element(G,the_carrier(C)) )
& element(F,the_carrier(C)) )
& element(E,the_carrier(B)) )
& element(D,the_carrier(B)) )
& subnetstr(C,A,B) )
& net_str(B,A) )
& one_sorted_str(A) ),
inference(nnf_transformation,[status(thm)],[f604_neg]) ).
fof(f604_sk,plain,
( ~ related(sk478,sk480,sk481)
& related(sk479,sk482,sk483)
& sk481 = sk483
& sk480 = sk482
& element(sk483,the_carrier(sk479))
& element(sk482,the_carrier(sk479))
& element(sk481,the_carrier(sk478))
& element(sk480,the_carrier(sk478))
& subnetstr(sk479,sk477,sk478)
& net_str(sk478,sk477)
& one_sorted_str(sk477) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk477,sk478,sk479,sk480,sk481,sk482,sk483])],[f604_nnf]) ).
cnf(c3332,plain,
subnetstr(sk479,sk477,sk478),
inference(cnf_transformation,[status(esa)],[f604_sk]) ).
cnf(t54,plain,
subnetstr(sk479,sk477,sk478) = true,
inference(equality_encoding,[status(esa)],[c3332]) ).
cnf(t758,plain,
subnetstr(sk479,sk477,sk478) = true,
inference(orient,[status(thm)],[t54]) ).
cnf(t761,plain,
true = ifeq(one_sorted_str(sk477),true,ifeq(net_str(sk478,sk477),true,ifeq(net_str(sk479,sk477),true,ifeq(true,true,subrelstr(sk479,sk478),true),true),true),true),
inference(cp,[status(thm)],[t308,t758]) ).
cnf(c3330,plain,
one_sorted_str(sk477),
inference(cnf_transformation,[status(esa)],[f604_sk]) ).
cnf(t9,plain,
one_sorted_str(sk477) = true,
inference(equality_encoding,[status(esa)],[c3330]) ).
cnf(t730,plain,
one_sorted_str(sk477) = true,
inference(orient,[status(thm)],[t9]) ).
cnf(t8417,plain,
true = ifeq(true,true,ifeq(net_str(sk478,sk477),true,ifeq(net_str(sk479,sk477),true,ifeq(true,true,subrelstr(sk479,sk478),true),true),true),true),
inference(step,[status(thm)],[t761,t730]) ).
cnf(t8418,plain,
true = ifeq(net_str(sk478,sk477),true,ifeq(net_str(sk479,sk477),true,ifeq(true,true,subrelstr(sk479,sk478),true),true),true),
inference(step,[status(thm)],[t8417,t182]) ).
cnf(c3331,plain,
net_str(sk478,sk477),
inference(cnf_transformation,[status(esa)],[f604_sk]) ).
cnf(t25,plain,
net_str(sk478,sk477) = true,
inference(equality_encoding,[status(esa)],[c3331]) ).
cnf(t743,plain,
net_str(sk478,sk477) = true,
inference(orient,[status(thm)],[t25]) ).
cnf(t8419,plain,
true = ifeq(true,true,ifeq(net_str(sk479,sk477),true,ifeq(true,true,subrelstr(sk479,sk478),true),true),true),
inference(step,[status(thm)],[t8418,t743]) ).
cnf(t8420,plain,
true = ifeq(net_str(sk479,sk477),true,ifeq(true,true,subrelstr(sk479,sk478),true),true),
inference(step,[status(thm)],[t8419,t182]) ).
fof(f275,axiom,
! [A,B] :
( ( net_str(B,A)
& one_sorted_str(A) )
=> ! [C] :
( subnetstr(C,A,B)
=> net_str(C,A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m1_yellow_6) ).
fof(f275_nnf,plain,
! [A,B] :
( ! [C] :
( net_str(C,A)
| ~ subnetstr(C,A,B) )
| ~ net_str(B,A)
| ~ one_sorted_str(A) ),
inference(nnf_transformation,[status(thm)],[f275]) ).
fof(f275_sk,plain,
! [A,B,C] :
( net_str(C,A)
| ~ subnetstr(C,A,B)
| ~ net_str(B,A)
| ~ one_sorted_str(A) ),
inference(skolemisation,[status(esa)],[f275_nnf]) ).
cnf(c864,plain,
( net_str(X2,X0)
| ~ subnetstr(X2,X0,X1)
| ~ net_str(X1,X0)
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[status(esa)],[f275_sk]) ).
cnf(t169,plain,
ifeq(one_sorted_str(X1),true,ifeq(net_str(X2,X1),true,ifeq(subnetstr(X3,X1,X2),true,net_str(X3,X1),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c864]) ).
cnf(t312,plain,
ifeq(one_sorted_str(X1),true,ifeq(net_str(X2,X1),true,ifeq(subnetstr(X3,X1,X2),true,net_str(X3,X1),true),true),true) = true,
inference(orient,[status(thm)],[t169]) ).
cnf(t759,plain,
true = ifeq(one_sorted_str(sk477),true,ifeq(net_str(sk478,sk477),true,ifeq(true,true,net_str(sk479,sk477),true),true),true),
inference(cp,[status(thm)],[t312,t758]) ).
cnf(t8270,plain,
true = ifeq(true,true,ifeq(net_str(sk478,sk477),true,ifeq(true,true,net_str(sk479,sk477),true),true),true),
inference(step,[status(thm)],[t759,t730]) ).
cnf(t8271,plain,
true = ifeq(net_str(sk478,sk477),true,ifeq(true,true,net_str(sk479,sk477),true),true),
inference(step,[status(thm)],[t8270,t182]) ).
cnf(t8272,plain,
true = ifeq(true,true,ifeq(true,true,net_str(sk479,sk477),true),true),
inference(step,[status(thm)],[t8271,t743]) ).
cnf(t8273,plain,
true = ifeq(true,true,net_str(sk479,sk477),true),
inference(step,[status(thm)],[t8272,t182]) ).
cnf(t8274,plain,
true = net_str(sk479,sk477),
inference(step,[status(thm)],[t8273,t182]) ).
cnf(t948,plain,
net_str(sk479,sk477) = true,
inference(orient,[status(thm)],[t8274]) ).
cnf(t8421,plain,
true = ifeq(true,true,ifeq(true,true,subrelstr(sk479,sk478),true),true),
inference(step,[status(thm)],[t8420,t948]) ).
cnf(t8422,plain,
true = ifeq(true,true,subrelstr(sk479,sk478),true),
inference(step,[status(thm)],[t8421,t182]) ).
cnf(t8423,plain,
true = subrelstr(sk479,sk478),
inference(step,[status(thm)],[t8422,t182]) ).
cnf(t2171,plain,
subrelstr(sk479,sk478) = true,
inference(orient,[status(thm)],[t8423]) ).
cnf(t2172,plain,
true = ifeq(rel_str(sk478),true,ifeq(rel_str(sk479),true,ifeq(true,true,subset(the_InternalRel(sk479),the_InternalRel(sk478)),true),true),true),
inference(cp,[status(thm)],[t287,t2171]) ).
fof(f268,axiom,
! [A] :
( one_sorted_str(A)
=> ! [B] :
( net_str(B,A)
=> rel_str(B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l1_waybel_0) ).
fof(f268_nnf,plain,
! [A] :
( ! [B] :
( rel_str(B)
| ~ net_str(B,A) )
| ~ one_sorted_str(A) ),
inference(nnf_transformation,[status(thm)],[f268]) ).
fof(f268_sk,plain,
! [A,B] :
( rel_str(B)
| ~ net_str(B,A)
| ~ one_sorted_str(A) ),
inference(skolemisation,[status(esa)],[f268_nnf]) ).
cnf(c856,plain,
( rel_str(X1)
| ~ net_str(X1,X0)
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[status(esa)],[f268_sk]) ).
cnf(t134,plain,
ifeq(one_sorted_str(X1),true,ifeq(net_str(X2,X1),true,rel_str(X2),true),true) = true,
inference(equality_encoding,[status(esa)],[c856]) ).
cnf(t313,plain,
ifeq(one_sorted_str(X1),true,ifeq(net_str(X2,X1),true,rel_str(X2),true),true) = true,
inference(orient,[status(thm)],[t134]) ).
cnf(t744,plain,
true = ifeq(one_sorted_str(sk477),true,ifeq(true,true,rel_str(sk478),true),true),
inference(cp,[status(thm)],[t313,t743]) ).
cnf(t8265,plain,
true = ifeq(true,true,ifeq(true,true,rel_str(sk478),true),true),
inference(step,[status(thm)],[t744,t730]) ).
cnf(t8266,plain,
true = ifeq(true,true,rel_str(sk478),true),
inference(step,[status(thm)],[t8265,t182]) ).
cnf(t8267,plain,
true = rel_str(sk478),
inference(step,[status(thm)],[t8266,t182]) ).
cnf(t918,plain,
rel_str(sk478) = true,
inference(orient,[status(thm)],[t8267]) ).
cnf(t8424,plain,
true = ifeq(true,true,ifeq(rel_str(sk479),true,ifeq(true,true,subset(the_InternalRel(sk479),the_InternalRel(sk478)),true),true),true),
inference(step,[status(thm)],[t2172,t918]) ).
cnf(t8425,plain,
true = ifeq(rel_str(sk479),true,ifeq(true,true,subset(the_InternalRel(sk479),the_InternalRel(sk478)),true),true),
inference(step,[status(thm)],[t8424,t182]) ).
cnf(t949,plain,
true = ifeq(one_sorted_str(sk477),true,ifeq(true,true,rel_str(sk479),true),true),
inference(cp,[status(thm)],[t313,t948]) ).
cnf(t8275,plain,
true = ifeq(true,true,ifeq(true,true,rel_str(sk479),true),true),
inference(step,[status(thm)],[t949,t730]) ).
cnf(t8276,plain,
true = ifeq(true,true,rel_str(sk479),true),
inference(step,[status(thm)],[t8275,t182]) ).
cnf(t8277,plain,
true = rel_str(sk479),
inference(step,[status(thm)],[t8276,t182]) ).
cnf(t963,plain,
rel_str(sk479) = true,
inference(orient,[status(thm)],[t8277]) ).
cnf(t8426,plain,
true = ifeq(true,true,ifeq(true,true,subset(the_InternalRel(sk479),the_InternalRel(sk478)),true),true),
inference(step,[status(thm)],[t8425,t963]) ).
cnf(t8427,plain,
true = ifeq(true,true,subset(the_InternalRel(sk479),the_InternalRel(sk478)),true),
inference(step,[status(thm)],[t8426,t182]) ).
cnf(t8428,plain,
true = subset(the_InternalRel(sk479),the_InternalRel(sk478)),
inference(step,[status(thm)],[t8427,t182]) ).
cnf(t2174,plain,
subset(the_InternalRel(sk479),the_InternalRel(sk478)) = true,
inference(orient,[status(thm)],[t8428]) ).
cnf(t2175,plain,
empty_set = ifeq(true,true,set_difference(the_InternalRel(sk479),the_InternalRel(sk478)),empty_set),
inference(cp,[status(thm)],[t762,t2174]) ).
cnf(t8429,plain,
empty_set = set_difference(the_InternalRel(sk479),the_InternalRel(sk478)),
inference(step,[status(thm)],[t2175,t182]) ).
cnf(t2183,plain,
set_difference(the_InternalRel(sk479),the_InternalRel(sk478)) = empty_set,
inference(orient,[status(thm)],[t8429]) ).
cnf(t2380,plain,
empty_set = set_difference(set_difference(set_difference(the_InternalRel(sk479),X1),the_InternalRel(sk478)),empty_set),
inference(cp,[status(thm)],[t2370,t2183]) ).
fof(f667,axiom,
! [A] : set_difference(A,empty_set) = A,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t3_boole) ).
fof(f667_nnf,plain,
! [A] : set_difference(A,empty_set) = A,
inference(nnf_transformation,[status(thm)],[f667]) ).
fof(f667_sk,plain,
! [A] : set_difference(A,empty_set) = A,
inference(skolemisation,[status(esa)],[f667_nnf]) ).
cnf(c3459,plain,
set_difference(X0,empty_set) = X0,
inference(cnf_transformation,[status(esa)],[f667_sk]) ).
cnf(t31,plain,
set_difference(X1,empty_set) = X1,
inference(equality_encoding,[status(esa)],[c3459]) ).
cnf(t201,plain,
set_difference(X1,empty_set) = X1,
inference(orient,[status(thm)],[t31]) ).
cnf(t8441,plain,
empty_set = set_difference(set_difference(the_InternalRel(sk479),X1),the_InternalRel(sk478)),
inference(step,[status(thm)],[t2380,t201]) ).
cnf(t2401,plain,
set_difference(set_difference(the_InternalRel(sk479),X1),the_InternalRel(sk478)) = empty_set,
inference(orient,[status(thm)],[t8441]) ).
cnf(t2404,plain,
true = ifeq(empty_set,empty_set,subset(set_difference(the_InternalRel(sk479),X1),the_InternalRel(sk478)),true),
inference(cp,[status(thm)],[t272,t2401]) ).
cnf(t8442,plain,
true = subset(set_difference(the_InternalRel(sk479),X1),the_InternalRel(sk478)),
inference(step,[status(thm)],[t2404,t182]) ).
cnf(t2413,plain,
subset(set_difference(the_InternalRel(sk479),X1),the_InternalRel(sk478)) = true,
inference(orient,[status(thm)],[t8442]) ).
fof(f655,lemma,
! [A,B,C,D] :
( ordered_pair(A,B) = ordered_pair(C,D)
=> ( B = D
& A = C ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t33_zfmisc_1) ).
fof(f655_nnf,plain,
! [A,B,C,D] :
( ( B = D
& A = C )
| ordered_pair(A,B) != ordered_pair(C,D) ),
inference(nnf_transformation,[status(thm)],[f655]) ).
fof(f655_sk,plain,
! [A,B,C,D] :
( ( B = D
& A = C )
| ordered_pair(A,B) != ordered_pair(C,D) ),
inference(skolemisation,[status(esa)],[f655_nnf]) ).
cnf(c3433,plain,
( X1 = X3
| ordered_pair(X0,X1) != ordered_pair(X2,X3) ),
inference(cnf_transformation,[status(esa)],[f655_sk]) ).
cnf(hi3256,axiom,
ifeq(ordered_pair(X0,X1),ordered_pair(X2,X3),X1,X3) = X3,
inference(equality_encoding,[status(esa)],[c3433]) ).
fof(f56,axiom,
! [A,B] : unordered_pair(A,B) = unordered_pair(B,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_k2_tarski) ).
fof(f56_nnf,plain,
! [A,B] : unordered_pair(A,B) = unordered_pair(B,A),
inference(nnf_transformation,[status(thm)],[f56]) ).
fof(f56_sk,plain,
! [A,B] : unordered_pair(A,B) = unordered_pair(B,A),
inference(skolemisation,[status(esa)],[f56_nnf]) ).
cnf(c152,plain,
unordered_pair(X0,X1) = unordered_pair(X1,X0),
inference(cnf_transformation,[status(esa)],[f56_sk]) ).
cnf(hi120,axiom,
unordered_pair(X0,X1) = unordered_pair(X1,X0),
inference(equality_encoding,[status(esa)],[c152]) ).
fof(f59,axiom,
! [A,B] : set_intersection2(A,B) = set_intersection2(B,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_k3_xboole_0) ).
fof(f59_nnf,plain,
! [A,B] : set_intersection2(A,B) = set_intersection2(B,A),
inference(nnf_transformation,[status(thm)],[f59]) ).
fof(f59_sk,plain,
! [A,B] : set_intersection2(A,B) = set_intersection2(B,A),
inference(skolemisation,[status(esa)],[f59_nnf]) ).
cnf(c155,plain,
set_intersection2(X0,X1) = set_intersection2(X1,X0),
inference(cnf_transformation,[status(esa)],[f59_sk]) ).
cnf(hi123,axiom,
set_intersection2(X0,X1) = set_intersection2(X1,X0),
inference(equality_encoding,[status(esa)],[c155]) ).
fof(f695,lemma,
! [A,B] : set_difference(A,set_difference(A,B)) = set_intersection2(A,B),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t48_xboole_1) ).
fof(f695_nnf,plain,
! [A,B] : set_difference(A,set_difference(A,B)) = set_intersection2(A,B),
inference(nnf_transformation,[status(thm)],[f695]) ).
fof(f695_sk,plain,
! [A,B] : set_difference(A,set_difference(A,B)) = set_intersection2(A,B),
inference(skolemisation,[status(esa)],[f695_nnf]) ).
cnf(c3510,plain,
set_difference(X0,set_difference(X0,X1)) = set_intersection2(X0,X1),
inference(cnf_transformation,[status(esa)],[f695_sk]) ).
cnf(hi124,axiom,
set_difference(X0,set_difference(X0,X1)) = set_intersection2(X0,X1),
inference(equality_encoding,[status(esa)],[c3510]) ).
cnf(t104,plain,
set_difference(X1,set_difference(X1,X2)) = set_difference(X2,set_difference(X2,X1)),
inference(hyper_resolution,[status(thm)],[hi3256,hi120,hi123,hi124]) ).
cnf(t880,plain,
set_difference(X1,set_difference(X1,X2)) = set_difference(X2,set_difference(X2,X1)),
inference(orient,[status(thm)],[t104]) ).
cnf(t2414,plain,
true = subset(set_difference(X1,set_difference(X1,the_InternalRel(sk479))),the_InternalRel(sk478)),
inference(cp,[status(thm)],[t2413,t880]) ).
cnf(t2907,plain,
subset(set_difference(X1,set_difference(X1,the_InternalRel(sk479))),the_InternalRel(sk478)) = true,
inference(orient,[status(thm)],[t2414]) ).
cnf(c1223,plain,
( ~ in(X0,X1)
| subset(singleton(X0),X1) ),
inference(cnf_transformation,[status(esa)],[f404_sk]) ).
cnf(t105,plain,
ifeq(in(X1,X2),true,subset(singleton(X1),X2),true) = true,
inference(equality_encoding,[status(esa)],[c1223]) ).
cnf(t242,plain,
ifeq(in(X1,X2),true,subset(singleton(X1),X2),true) = true,
inference(orient,[status(thm)],[t105]) ).
cnf(c741,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)],[f181_sk]) ).
cnf(t180,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)],[c741]) ).
cnf(t278,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)],[t180]) ).
cnf(c3339,plain,
related(sk479,sk482,sk483),
inference(cnf_transformation,[status(esa)],[f604_sk]) ).
cnf(t52,plain,
related(sk479,sk482,sk483) = true,
inference(equality_encoding,[status(esa)],[c3339]) ).
cnf(t753,plain,
related(sk479,sk482,sk483) = true,
inference(orient,[status(thm)],[t52]) ).
cnf(t755,plain,
true = ifeq(rel_str(sk479),true,ifeq(element(sk482,the_carrier(sk479)),true,ifeq(element(sk483,the_carrier(sk479)),true,ifeq(true,true,in(ordered_pair(sk482,sk483),the_InternalRel(sk479)),true),true),true),true),
inference(cp,[status(thm)],[t278,t753]) ).
cnf(t8636,plain,
true = ifeq(true,true,ifeq(element(sk482,the_carrier(sk479)),true,ifeq(element(sk483,the_carrier(sk479)),true,ifeq(true,true,in(ordered_pair(sk482,sk483),the_InternalRel(sk479)),true),true),true),true),
inference(step,[status(thm)],[t755,t963]) ).
cnf(t8637,plain,
true = ifeq(element(sk482,the_carrier(sk479)),true,ifeq(element(sk483,the_carrier(sk479)),true,ifeq(true,true,in(ordered_pair(sk482,sk483),the_InternalRel(sk479)),true),true),true),
inference(step,[status(thm)],[t8636,t182]) ).
cnf(c3335,plain,
element(sk482,the_carrier(sk479)),
inference(cnf_transformation,[status(esa)],[f604_sk]) ).
cnf(t44,plain,
element(sk482,the_carrier(sk479)) = true,
inference(equality_encoding,[status(esa)],[c3335]) ).
cnf(t661,plain,
element(sk482,the_carrier(sk479)) = true,
inference(orient,[status(thm)],[t44]) ).
cnf(t8638,plain,
true = ifeq(true,true,ifeq(element(sk483,the_carrier(sk479)),true,ifeq(true,true,in(ordered_pair(sk482,sk483),the_InternalRel(sk479)),true),true),true),
inference(step,[status(thm)],[t8637,t661]) ).
cnf(t8639,plain,
true = ifeq(element(sk483,the_carrier(sk479)),true,ifeq(true,true,in(ordered_pair(sk482,sk483),the_InternalRel(sk479)),true),true),
inference(step,[status(thm)],[t8638,t182]) ).
cnf(c3336,plain,
element(sk483,the_carrier(sk479)),
inference(cnf_transformation,[status(esa)],[f604_sk]) ).
cnf(t45,plain,
element(sk483,the_carrier(sk479)) = true,
inference(equality_encoding,[status(esa)],[c3336]) ).
cnf(t675,plain,
element(sk483,the_carrier(sk479)) = true,
inference(orient,[status(thm)],[t45]) ).
cnf(t8640,plain,
true = ifeq(true,true,ifeq(true,true,in(ordered_pair(sk482,sk483),the_InternalRel(sk479)),true),true),
inference(step,[status(thm)],[t8639,t675]) ).
cnf(t8641,plain,
true = ifeq(true,true,in(ordered_pair(sk482,sk483),the_InternalRel(sk479)),true),
inference(step,[status(thm)],[t8640,t182]) ).
cnf(t8642,plain,
true = in(ordered_pair(sk482,sk483),the_InternalRel(sk479)),
inference(step,[status(thm)],[t8641,t182]) ).
cnf(t7931,plain,
in(ordered_pair(sk482,sk483),the_InternalRel(sk479)) = true,
inference(orient,[status(thm)],[t8642]) ).
cnf(t7941,plain,
true = ifeq(true,true,subset(singleton(ordered_pair(sk482,sk483)),the_InternalRel(sk479)),true),
inference(cp,[status(thm)],[t242,t7931]) ).
cnf(t8648,plain,
true = subset(singleton(ordered_pair(sk482,sk483)),the_InternalRel(sk479)),
inference(step,[status(thm)],[t7941,t182]) ).
cnf(t7997,plain,
subset(singleton(ordered_pair(sk482,sk483)),the_InternalRel(sk479)) = true,
inference(orient,[status(thm)],[t8648]) ).
cnf(t7998,plain,
empty_set = ifeq(true,true,set_difference(singleton(ordered_pair(sk482,sk483)),the_InternalRel(sk479)),empty_set),
inference(cp,[status(thm)],[t762,t7997]) ).
cnf(t8649,plain,
empty_set = set_difference(singleton(ordered_pair(sk482,sk483)),the_InternalRel(sk479)),
inference(step,[status(thm)],[t7998,t182]) ).
cnf(t8007,plain,
set_difference(singleton(ordered_pair(sk482,sk483)),the_InternalRel(sk479)) = empty_set,
inference(orient,[status(thm)],[t8649]) ).
cnf(t8013,plain,
true = subset(set_difference(singleton(ordered_pair(sk482,sk483)),empty_set),the_InternalRel(sk478)),
inference(cp,[status(thm)],[t2907,t8007]) ).
cnf(t8650,plain,
true = subset(singleton(ordered_pair(sk482,sk483)),the_InternalRel(sk478)),
inference(step,[status(thm)],[t8013,t201]) ).
cnf(t8021,plain,
subset(singleton(ordered_pair(sk482,sk483)),the_InternalRel(sk478)) = true,
inference(orient,[status(thm)],[t8650]) ).
cnf(t8024,plain,
true = ifeq(true,true,in(ordered_pair(sk482,sk483),the_InternalRel(sk478)),true),
inference(cp,[status(thm)],[t254,t8021]) ).
cnf(t8651,plain,
true = in(ordered_pair(sk482,sk483),the_InternalRel(sk478)),
inference(step,[status(thm)],[t8024,t182]) ).
cnf(t8032,plain,
in(ordered_pair(sk482,sk483),the_InternalRel(sk478)) = true,
inference(orient,[status(thm)],[t8651]) ).
cnf(t8069,plain,
true = ifeq(rel_str(sk478),true,ifeq(element(sk482,the_carrier(sk478)),true,ifeq(element(sk483,the_carrier(sk478)),true,ifeq(true,true,related(sk478,sk482,sk483),true),true),true),true),
inference(cp,[status(thm)],[t275,t8032]) ).
cnf(t8652,plain,
true = ifeq(true,true,ifeq(element(sk482,the_carrier(sk478)),true,ifeq(element(sk483,the_carrier(sk478)),true,ifeq(true,true,related(sk478,sk482,sk483),true),true),true),true),
inference(step,[status(thm)],[t8069,t918]) ).
cnf(t8653,plain,
true = ifeq(element(sk482,the_carrier(sk478)),true,ifeq(element(sk483,the_carrier(sk478)),true,ifeq(true,true,related(sk478,sk482,sk483),true),true),true),
inference(step,[status(thm)],[t8652,t182]) ).
cnf(c3333,plain,
element(sk480,the_carrier(sk478)),
inference(cnf_transformation,[status(esa)],[f604_sk]) ).
cnf(t42,plain,
element(sk480,the_carrier(sk478)) = true,
inference(equality_encoding,[status(esa)],[c3333]) ).
cnf(t633,plain,
element(sk480,the_carrier(sk478)) = true,
inference(orient,[status(thm)],[t42]) ).
cnf(c3337,plain,
sk480 = sk482,
inference(cnf_transformation,[status(esa)],[f604_sk]) ).
cnf(t0,plain,
sk482 = sk480,
inference(equality_encoding,[status(esa)],[c3337]) ).
cnf(t913,plain,
sk480 = sk482,
inference(orient,[status(thm)],[t0]) ).
cnf(t8263,plain,
element(sk482,the_carrier(sk478)) = true,
inference(step,[status(thm)],[t633,t913]) ).
cnf(t915,plain,
element(sk482,the_carrier(sk478)) = true,
inference(rw,[status(thm)],[t8263]) ).
cnf(t1087,plain,
element(sk482,the_carrier(sk478)) = true,
inference(orient,[status(thm)],[t915]) ).
cnf(t8654,plain,
true = ifeq(true,true,ifeq(element(sk483,the_carrier(sk478)),true,ifeq(true,true,related(sk478,sk482,sk483),true),true),true),
inference(step,[status(thm)],[t8653,t1087]) ).
cnf(t8655,plain,
true = ifeq(element(sk483,the_carrier(sk478)),true,ifeq(true,true,related(sk478,sk482,sk483),true),true),
inference(step,[status(thm)],[t8654,t182]) ).
cnf(c3334,plain,
element(sk481,the_carrier(sk478)),
inference(cnf_transformation,[status(esa)],[f604_sk]) ).
cnf(t43,plain,
element(sk481,the_carrier(sk478)) = true,
inference(equality_encoding,[status(esa)],[c3334]) ).
cnf(t647,plain,
element(sk481,the_carrier(sk478)) = true,
inference(orient,[status(thm)],[t43]) ).
cnf(c3338,plain,
sk481 = sk483,
inference(cnf_transformation,[status(esa)],[f604_sk]) ).
cnf(t1,plain,
sk483 = sk481,
inference(equality_encoding,[status(esa)],[c3338]) ).
cnf(t916,plain,
sk481 = sk483,
inference(orient,[status(thm)],[t1]) ).
cnf(t8264,plain,
element(sk483,the_carrier(sk478)) = true,
inference(step,[status(thm)],[t647,t916]) ).
cnf(t917,plain,
element(sk483,the_carrier(sk478)) = true,
inference(rw,[status(thm)],[t8264]) ).
cnf(t1101,plain,
element(sk483,the_carrier(sk478)) = true,
inference(orient,[status(thm)],[t917]) ).
cnf(t8656,plain,
true = ifeq(true,true,ifeq(true,true,related(sk478,sk482,sk483),true),true),
inference(step,[status(thm)],[t8655,t1101]) ).
cnf(t8657,plain,
true = ifeq(true,true,related(sk478,sk482,sk483),true),
inference(step,[status(thm)],[t8656,t182]) ).
cnf(t8658,plain,
true = related(sk478,sk482,sk483),
inference(step,[status(thm)],[t8657,t182]) ).
cnf(c3340,plain,
~ related(sk478,sk480,sk481),
inference(cnf_transformation,[status(esa)],[f604_sk]) ).
cnf(t51,plain,
related(sk478,sk480,sk481) = false,
inference(equality_encoding,[status(esa)],[c3340]) ).
cnf(t845,plain,
related(sk478,sk480,sk481) = false,
inference(orient,[status(thm)],[t51]) ).
cnf(t8262,plain,
related(sk478,sk482,sk481) = false,
inference(step,[status(thm)],[t845,t913]) ).
cnf(t914,plain,
related(sk478,sk482,sk481) = false,
inference(rw,[status(thm)],[t8262]) ).
cnf(t8286,plain,
related(sk478,sk482,sk483) = false,
inference(step,[status(thm)],[t914,t916]) ).
cnf(t1082,plain,
related(sk478,sk482,sk483) = false,
inference(orient,[status(thm)],[t8286]) ).
cnf(t8659,plain,
true = false,
inference(step,[status(thm)],[t8658,t1082]) ).
cnf(t8070,plain,
false = true,
inference(orient,[status(thm)],[t8659]) ).
fof(f2,axiom,
! [A,B] :
( in(A,B)
=> ~ in(B,A) ),
file('/export/starexec/sandbox2/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/sandbox2/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(f20,axiom,
! [A] :
( rel_str(A)
=> ( with_suprema_relstr(A)
=> ~ empty_carrier(A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc1_lattice3) ).
fof(f20_nnf,plain,
! [A] :
( ~ empty_carrier(A)
| ~ with_suprema_relstr(A)
| ~ rel_str(A) ),
inference(nnf_transformation,[status(thm)],[f20]) ).
fof(f20_sk,plain,
! [A] :
( ~ empty_carrier(A)
| ~ with_suprema_relstr(A)
| ~ rel_str(A) ),
inference(skolemisation,[status(esa)],[f20_nnf]) ).
cnf(c54,plain,
( ~ empty_carrier(X0)
| ~ with_suprema_relstr(X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(esa)],[f20_sk]) ).
fof(f34,axiom,
! [A] :
( rel_str(A)
=> ( with_infima_relstr(A)
=> ~ empty_carrier(A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc2_lattice3) ).
fof(f34_nnf,plain,
! [A] :
( ~ empty_carrier(A)
| ~ with_infima_relstr(A)
| ~ rel_str(A) ),
inference(nnf_transformation,[status(thm)],[f34]) ).
fof(f34_sk,plain,
! [A] :
( ~ empty_carrier(A)
| ~ with_infima_relstr(A)
| ~ rel_str(A) ),
inference(skolemisation,[status(esa)],[f34_nnf]) ).
cnf(c90,plain,
( ~ empty_carrier(X0)
| ~ with_infima_relstr(X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(esa)],[f34_sk]) ).
fof(f77,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/sandbox2/benchmark/theBenchmark.p',d13_pre_topc) ).
fof(f77_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)],[f77]) ).
fof(f77_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])],[f77_nnf]) ).
cnf(c235,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)],[f77_sk]) ).
fof(f107,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/sandbox2/benchmark/theBenchmark.p',d1_wellord1) ).
fof(f107_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)],[f107]) ).
fof(f107_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])],[f107_nnf]) ).
cnf(c390,plain,
( X3 != X1
| ~ in(X3,X2)
| X2 != fiber(X0,X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(esa)],[f107_sk]) ).
fof(f109,axiom,
! [A] :
( A = empty_set
<=> ! [B] : ~ in(B,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_xboole_0) ).
fof(f109_nnf,plain,
! [A] :
( ( ? [B] : in(B,A)
| A = empty_set )
& ( ! [B] : ~ in(B,A)
| A != empty_set ) ),
inference(nnf_transformation,[status(thm)],[f109]) ).
fof(f109_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])],[f109_nnf]) ).
cnf(c408,plain,
( ~ in(X1,X0)
| X0 != empty_set ),
inference(cnf_transformation,[status(esa)],[f109_sk]) ).
fof(f114,axiom,
! [A] :
( centered(A)
<=> ( ! [B] :
~ ( set_meet(B) = empty_set
& finite(B)
& subset(B,A)
& B != empty_set )
& A != empty_set ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d2_compts_1) ).
fof(f114_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)],[f114]) ).
fof(f114_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])],[f114_nnf]) ).
cnf(c423,plain,
( X0 != empty_set
| ~ centered(X0) ),
inference(cnf_transformation,[status(esa)],[f114_sk]) ).
fof(f123,axiom,
! [A,B] :
( element(B,A)
=> ( proper_element(B,A)
<=> B != union(A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d2_tex_2) ).
fof(f123_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)],[f123]) ).
fof(f123_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)],[f123_nnf]) ).
cnf(c457,plain,
( X1 != union(X0)
| ~ proper_element(X1,X0)
| ~ element(X1,X0) ),
inference(cnf_transformation,[status(esa)],[f123_sk]) ).
fof(f147,axiom,
! [A,B,C] :
( C = set_difference(A,B)
<=> ! [D] :
( in(D,C)
<=> ( ~ in(D,B)
& in(D,A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d4_xboole_0) ).
fof(f147_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)],[f147]) ).
fof(f147_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])],[f147_nnf]) ).
cnf(c571,plain,
( ~ in(X3,X1)
| ~ in(X3,X2)
| X2 != set_difference(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f147_sk]) ).
fof(f176,axiom,
! [A,B] :
( proper_subset(A,B)
<=> ( A != B
& subset(A,B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d8_xboole_0) ).
fof(f176_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)],[f176]) ).
fof(f176_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)],[f176_nnf]) ).
cnf(c713,plain,
( X0 != X1
| ~ proper_subset(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f176_sk]) ).
fof(f305,axiom,
! [A] :
( finite(singleton(A))
& ~ empty(singleton(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_finset_1) ).
fof(f305_nnf,plain,
! [A] :
( finite(singleton(A))
& ~ empty(singleton(A)) ),
inference(nnf_transformation,[status(thm)],[f305]) ).
fof(f305_sk,plain,
! [A] :
( finite(singleton(A))
& ~ empty(singleton(A)) ),
inference(skolemisation,[status(esa)],[f305_nnf]) ).
cnf(c905,plain,
~ empty(singleton(X0)),
inference(cnf_transformation,[status(esa)],[f305_sk]) ).
fof(f306,axiom,
! [A] :
( preboolean(powerset(A))
& diff_closed(powerset(A))
& cup_closed(powerset(A))
& ~ empty(powerset(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_finsub_1) ).
fof(f306_nnf,plain,
! [A] :
( preboolean(powerset(A))
& diff_closed(powerset(A))
& cup_closed(powerset(A))
& ~ empty(powerset(A)) ),
inference(nnf_transformation,[status(thm)],[f306]) ).
fof(f306_sk,plain,
! [A] :
( preboolean(powerset(A))
& diff_closed(powerset(A))
& cup_closed(powerset(A))
& ~ empty(powerset(A)) ),
inference(skolemisation,[status(esa)],[f306_nnf]) ).
cnf(c907,plain,
~ empty(powerset(X0)),
inference(cnf_transformation,[status(esa)],[f306_sk]) ).
fof(f308,axiom,
! [A] :
( complete_latt_str(boole_lattice(A))
& boolean_lattstr(boole_lattice(A))
& complemented_lattstr(boole_lattice(A))
& bounded_lattstr(boole_lattice(A))
& upper_bounded_semilattstr(boole_lattice(A))
& lower_bounded_semilattstr(boole_lattice(A))
& modular_lattstr(boole_lattice(A))
& distributive_lattstr(boole_lattice(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/sandbox2/benchmark/theBenchmark.p',fc1_knaster) ).
fof(f308_nnf,plain,
! [A] :
( complete_latt_str(boole_lattice(A))
& boolean_lattstr(boole_lattice(A))
& complemented_lattstr(boole_lattice(A))
& bounded_lattstr(boole_lattice(A))
& upper_bounded_semilattstr(boole_lattice(A))
& lower_bounded_semilattstr(boole_lattice(A))
& modular_lattstr(boole_lattice(A))
& distributive_lattstr(boole_lattice(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)],[f308]) ).
fof(f308_sk,plain,
! [A] :
( complete_latt_str(boole_lattice(A))
& boolean_lattstr(boole_lattice(A))
& complemented_lattstr(boole_lattice(A))
& bounded_lattstr(boole_lattice(A))
& upper_bounded_semilattstr(boole_lattice(A))
& lower_bounded_semilattstr(boole_lattice(A))
& modular_lattstr(boole_lattice(A))
& distributive_lattstr(boole_lattice(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)],[f308_nnf]) ).
cnf(c913,plain,
~ empty_carrier(boole_lattice(X0)),
inference(cnf_transformation,[status(esa)],[f308_sk]) ).
fof(f309,axiom,
! [A] :
( strict_latt_str(boole_lattice(A))
& ~ empty_carrier(boole_lattice(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_lattice3) ).
fof(f309_nnf,plain,
! [A] :
( strict_latt_str(boole_lattice(A))
& ~ empty_carrier(boole_lattice(A)) ),
inference(nnf_transformation,[status(thm)],[f309]) ).
fof(f309_sk,plain,
! [A] :
( strict_latt_str(boole_lattice(A))
& ~ empty_carrier(boole_lattice(A)) ),
inference(skolemisation,[status(esa)],[f309_nnf]) ).
cnf(c930,plain,
~ empty_carrier(boole_lattice(X0)),
inference(cnf_transformation,[status(esa)],[f309_sk]) ).
fof(f311,axiom,
! [A] : ~ empty(succ(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_ordinal1) ).
fof(f311_nnf,plain,
! [A] : ~ empty(succ(A)),
inference(nnf_transformation,[status(thm)],[f311]) ).
fof(f311_sk,plain,
! [A] : ~ empty(succ(A)),
inference(skolemisation,[status(esa)],[f311_nnf]) ).
cnf(c934,plain,
~ empty(succ(X0)),
inference(cnf_transformation,[status(esa)],[f311_sk]) ).
fof(f312,axiom,
( ~ empty(omega)
& ordinal(omega)
& epsilon_connected(omega)
& epsilon_transitive(omega) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_ordinal2) ).
fof(f312_nnf,plain,
( ~ empty(omega)
& ordinal(omega)
& epsilon_connected(omega)
& epsilon_transitive(omega) ),
inference(nnf_transformation,[status(thm)],[f312]) ).
fof(f312_sk,plain,
( ~ empty(omega)
& ordinal(omega)
& epsilon_connected(omega)
& epsilon_transitive(omega) ),
inference(skolemisation,[status(esa)],[f312_nnf]) ).
cnf(c938,plain,
~ empty(omega),
inference(cnf_transformation,[status(esa)],[f312_sk]) ).
fof(f316,axiom,
! [A] : ~ empty(powerset(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_subset_1) ).
fof(f316_nnf,plain,
! [A] : ~ empty(powerset(A)),
inference(nnf_transformation,[status(thm)],[f316]) ).
fof(f316_sk,plain,
! [A] : ~ empty(powerset(A)),
inference(skolemisation,[status(esa)],[f316_nnf]) ).
cnf(c947,plain,
~ empty(powerset(X0)),
inference(cnf_transformation,[status(esa)],[f316_sk]) ).
fof(f318,axiom,
! [A,B] :
( relation_of2(B,singleton(A),singleton(A))
=> ( trivial_carrier(rel_str_of(singleton(A),B))
& strict_rel_str(rel_str_of(singleton(A),B))
& ~ empty_carrier(rel_str_of(singleton(A),B)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_yellow_0) ).
fof(f318_nnf,plain,
! [A,B] :
( ( trivial_carrier(rel_str_of(singleton(A),B))
& strict_rel_str(rel_str_of(singleton(A),B))
& ~ empty_carrier(rel_str_of(singleton(A),B)) )
| ~ relation_of2(B,singleton(A),singleton(A)) ),
inference(nnf_transformation,[status(thm)],[f318]) ).
fof(f318_sk,plain,
! [B,A] :
( ( trivial_carrier(rel_str_of(singleton(A),B))
& strict_rel_str(rel_str_of(singleton(A),B))
& ~ empty_carrier(rel_str_of(singleton(A),B)) )
| ~ relation_of2(B,singleton(A),singleton(A)) ),
inference(skolemisation,[status(esa)],[f318_nnf]) ).
cnf(c949,plain,
( ~ empty_carrier(rel_str_of(singleton(X0),X1))
| ~ relation_of2(X1,singleton(X0),singleton(X0)) ),
inference(cnf_transformation,[status(esa)],[f318_sk]) ).
fof(f320,axiom,
! [A,B] : ~ empty(ordered_pair(A,B)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_zfmisc_1) ).
fof(f320_nnf,plain,
! [A,B] : ~ empty(ordered_pair(A,B)),
inference(nnf_transformation,[status(thm)],[f320]) ).
fof(f320_sk,plain,
! [A,B] : ~ empty(ordered_pair(A,B)),
inference(skolemisation,[status(esa)],[f320_nnf]) ).
cnf(c959,plain,
~ empty(ordered_pair(X0,X1)),
inference(cnf_transformation,[status(esa)],[f320_sk]) ).
fof(f324,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/sandbox2/benchmark/theBenchmark.p',fc2_arytm_3) ).
fof(f324_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)],[f324]) ).
fof(f324_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)],[f324_nnf]) ).
cnf(c964,plain,
( ~ empty(succ(X0))
| ~ natural(X0)
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(esa)],[f324_sk]) ).
fof(f325,axiom,
! [A,B] :
( finite(unordered_pair(A,B))
& ~ empty(unordered_pair(A,B)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc2_finset_1) ).
fof(f325_nnf,plain,
! [A,B] :
( finite(unordered_pair(A,B))
& ~ empty(unordered_pair(A,B)) ),
inference(nnf_transformation,[status(thm)],[f325]) ).
fof(f325_sk,plain,
! [A,B] :
( finite(unordered_pair(A,B))
& ~ empty(unordered_pair(A,B)) ),
inference(skolemisation,[status(esa)],[f325_nnf]) ).
cnf(c969,plain,
~ empty(unordered_pair(X0,X1)),
inference(cnf_transformation,[status(esa)],[f325_sk]) ).
fof(f328,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/sandbox2/benchmark/theBenchmark.p',fc2_lattice3) ).
fof(f328_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)],[f328]) ).
fof(f328_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)],[f328_nnf]) ).
cnf(c978,plain,
~ empty_carrier(boole_lattice(X0)),
inference(cnf_transformation,[status(esa)],[f328_sk]) ).
fof(f334,axiom,
! [A] : ~ empty(singleton(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc2_subset_1) ).
fof(f334_nnf,plain,
! [A] : ~ empty(singleton(A)),
inference(nnf_transformation,[status(thm)],[f334]) ).
fof(f334_sk,plain,
! [A] : ~ empty(singleton(A)),
inference(skolemisation,[status(esa)],[f334_nnf]) ).
cnf(c1008,plain,
~ empty(singleton(X0)),
inference(cnf_transformation,[status(esa)],[f334_sk]) ).
fof(f350,axiom,
! [A] :
( boolean_lattstr(boole_lattice(A))
& complemented_lattstr(boole_lattice(A))
& bounded_lattstr(boole_lattice(A))
& upper_bounded_semilattstr(boole_lattice(A))
& lower_bounded_semilattstr(boole_lattice(A))
& modular_lattstr(boole_lattice(A))
& distributive_lattstr(boole_lattice(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/sandbox2/benchmark/theBenchmark.p',fc3_lattice3) ).
fof(f350_nnf,plain,
! [A] :
( boolean_lattstr(boole_lattice(A))
& complemented_lattstr(boole_lattice(A))
& bounded_lattstr(boole_lattice(A))
& upper_bounded_semilattstr(boole_lattice(A))
& lower_bounded_semilattstr(boole_lattice(A))
& modular_lattstr(boole_lattice(A))
& distributive_lattstr(boole_lattice(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)],[f350]) ).
fof(f350_sk,plain,
! [A] :
( boolean_lattstr(boole_lattice(A))
& complemented_lattstr(boole_lattice(A))
& bounded_lattstr(boole_lattice(A))
& upper_bounded_semilattstr(boole_lattice(A))
& lower_bounded_semilattstr(boole_lattice(A))
& modular_lattstr(boole_lattice(A))
& distributive_lattstr(boole_lattice(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)],[f350_nnf]) ).
cnf(c1058,plain,
~ empty_carrier(boole_lattice(X0)),
inference(cnf_transformation,[status(esa)],[f350_sk]) ).
fof(f353,axiom,
! [A] :
( ordinal(A)
=> ( ordinal(succ(A))
& epsilon_connected(succ(A))
& epsilon_transitive(succ(A))
& ~ empty(succ(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc3_ordinal1) ).
fof(f353_nnf,plain,
! [A] :
( ( ordinal(succ(A))
& epsilon_connected(succ(A))
& epsilon_transitive(succ(A))
& ~ empty(succ(A)) )
| ~ ordinal(A) ),
inference(nnf_transformation,[status(thm)],[f353]) ).
fof(f353_sk,plain,
! [A] :
( ( ordinal(succ(A))
& epsilon_connected(succ(A))
& epsilon_transitive(succ(A))
& ~ empty(succ(A)) )
| ~ ordinal(A) ),
inference(skolemisation,[status(esa)],[f353_nnf]) ).
cnf(c1080,plain,
( ~ empty(succ(X0))
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(esa)],[f353_sk]) ).
fof(f355,axiom,
! [A,B] : ~ empty(unordered_pair(A,B)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc3_subset_1) ).
fof(f355_nnf,plain,
! [A,B] : ~ empty(unordered_pair(A,B)),
inference(nnf_transformation,[status(thm)],[f355]) ).
fof(f355_sk,plain,
! [A,B] : ~ empty(unordered_pair(A,B)),
inference(skolemisation,[status(esa)],[f355_nnf]) ).
cnf(c1085,plain,
~ empty(unordered_pair(X0,X1)),
inference(cnf_transformation,[status(esa)],[f355_sk]) ).
fof(f379,axiom,
! [A] :
( antisymmetric_relstr(boole_POSet(A))
& transitive_relstr(boole_POSet(A))
& reflexive_relstr(boole_POSet(A))
& strict_rel_str(boole_POSet(A))
& ~ empty_carrier(boole_POSet(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc7_yellow_1) ).
fof(f379_nnf,plain,
! [A] :
( antisymmetric_relstr(boole_POSet(A))
& transitive_relstr(boole_POSet(A))
& reflexive_relstr(boole_POSet(A))
& strict_rel_str(boole_POSet(A))
& ~ empty_carrier(boole_POSet(A)) ),
inference(nnf_transformation,[status(thm)],[f379]) ).
fof(f379_sk,plain,
! [A] :
( antisymmetric_relstr(boole_POSet(A))
& transitive_relstr(boole_POSet(A))
& reflexive_relstr(boole_POSet(A))
& strict_rel_str(boole_POSet(A))
& ~ empty_carrier(boole_POSet(A)) ),
inference(skolemisation,[status(esa)],[f379_nnf]) ).
cnf(c1163,plain,
~ empty_carrier(boole_POSet(X0)),
inference(cnf_transformation,[status(esa)],[f379_sk]) ).
fof(f381,axiom,
! [A] :
( complete_relstr(boole_POSet(A))
& with_infima_relstr(boole_POSet(A))
& with_suprema_relstr(boole_POSet(A))
& bounded_relstr(boole_POSet(A))
& upper_bounded_relstr(boole_POSet(A))
& lower_bounded_relstr(boole_POSet(A))
& antisymmetric_relstr(boole_POSet(A))
& transitive_relstr(boole_POSet(A))
& reflexive_relstr(boole_POSet(A))
& strict_rel_str(boole_POSet(A))
& ~ empty_carrier(boole_POSet(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc8_yellow_1) ).
fof(f381_nnf,plain,
! [A] :
( complete_relstr(boole_POSet(A))
& with_infima_relstr(boole_POSet(A))
& with_suprema_relstr(boole_POSet(A))
& bounded_relstr(boole_POSet(A))
& upper_bounded_relstr(boole_POSet(A))
& lower_bounded_relstr(boole_POSet(A))
& antisymmetric_relstr(boole_POSet(A))
& transitive_relstr(boole_POSet(A))
& reflexive_relstr(boole_POSet(A))
& strict_rel_str(boole_POSet(A))
& ~ empty_carrier(boole_POSet(A)) ),
inference(nnf_transformation,[status(thm)],[f381]) ).
fof(f381_sk,plain,
! [A] :
( complete_relstr(boole_POSet(A))
& with_infima_relstr(boole_POSet(A))
& with_suprema_relstr(boole_POSet(A))
& bounded_relstr(boole_POSet(A))
& upper_bounded_relstr(boole_POSet(A))
& lower_bounded_relstr(boole_POSet(A))
& antisymmetric_relstr(boole_POSet(A))
& transitive_relstr(boole_POSet(A))
& reflexive_relstr(boole_POSet(A))
& strict_rel_str(boole_POSet(A))
& ~ empty_carrier(boole_POSet(A)) ),
inference(skolemisation,[status(esa)],[f381_nnf]) ).
cnf(c1170,plain,
~ empty_carrier(boole_POSet(X0)),
inference(cnf_transformation,[status(esa)],[f381_sk]) ).
fof(f396,axiom,
! [A,B] : ~ proper_subset(A,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',irreflexivity_r2_xboole_0) ).
fof(f396_nnf,plain,
! [A,B] : ~ proper_subset(A,A),
inference(nnf_transformation,[status(thm)],[f396]) ).
fof(f396_sk,plain,
! [A] : ~ proper_subset(A,A),
inference(skolemisation,[status(esa)],[f396_nnf]) ).
cnf(c1209,plain,
~ proper_subset(X0,X0),
inference(cnf_transformation,[status(esa)],[f396_sk]) ).
fof(f398,lemma,
! [A] : singleton(A) != empty_set,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l1_zfmisc_1) ).
fof(f398_nnf,plain,
! [A] : singleton(A) != empty_set,
inference(nnf_transformation,[status(thm)],[f398]) ).
fof(f398_sk,plain,
! [A] : singleton(A) != empty_set,
inference(skolemisation,[status(esa)],[f398_nnf]) ).
cnf(c1213,plain,
singleton(X0) != empty_set,
inference(cnf_transformation,[status(esa)],[f398_sk]) ).
fof(f400,lemma,
! [A,B] :
~ ( in(A,B)
& disjoint(singleton(A),B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l25_zfmisc_1) ).
fof(f400_nnf,plain,
! [A,B] :
( ~ in(A,B)
| ~ disjoint(singleton(A),B) ),
inference(nnf_transformation,[status(thm)],[f400]) ).
fof(f400_sk,plain,
! [A,B] :
( ~ in(A,B)
| ~ disjoint(singleton(A),B) ),
inference(skolemisation,[status(esa)],[f400_nnf]) ).
cnf(c1215,plain,
( ~ in(X0,X1)
| ~ disjoint(singleton(X0),X1) ),
inference(cnf_transformation,[status(esa)],[f400_sk]) ).
fof(f417,axiom,
? [A] :
( upper_bounded_semilattstr(A)
& lower_bounded_semilattstr(A)
& modular_lattstr(A)
& distributive_lattstr(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/sandbox2/benchmark/theBenchmark.p',rc10_lattices) ).
fof(f417_nnf,plain,
? [A] :
( upper_bounded_semilattstr(A)
& lower_bounded_semilattstr(A)
& modular_lattstr(A)
& distributive_lattstr(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)],[f417]) ).
fof(f417_sk,plain,
( upper_bounded_semilattstr(sk159)
& lower_bounded_semilattstr(sk159)
& modular_lattstr(sk159)
& distributive_lattstr(sk159)
& lattice(sk159)
& join_absorbing(sk159)
& meet_absorbing(sk159)
& meet_associative(sk159)
& meet_commutative(sk159)
& join_associative(sk159)
& join_commutative(sk159)
& strict_latt_str(sk159)
& ~ empty_carrier(sk159)
& latt_str(sk159) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk159])],[f417_nnf]) ).
cnf(c1255,plain,
~ empty_carrier(sk159),
inference(cnf_transformation,[status(esa)],[f417_sk]) ).
fof(f418,axiom,
? [A] :
( bounded_lattstr(A)
& upper_bounded_semilattstr(A)
& lower_bounded_semilattstr(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/sandbox2/benchmark/theBenchmark.p',rc11_lattices) ).
fof(f418_nnf,plain,
? [A] :
( bounded_lattstr(A)
& upper_bounded_semilattstr(A)
& lower_bounded_semilattstr(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)],[f418]) ).
fof(f418_sk,plain,
( bounded_lattstr(sk160)
& upper_bounded_semilattstr(sk160)
& lower_bounded_semilattstr(sk160)
& lattice(sk160)
& join_absorbing(sk160)
& meet_absorbing(sk160)
& meet_associative(sk160)
& meet_commutative(sk160)
& join_associative(sk160)
& join_commutative(sk160)
& strict_latt_str(sk160)
& ~ empty_carrier(sk160)
& latt_str(sk160) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk160])],[f418_nnf]) ).
cnf(c1269,plain,
~ empty_carrier(sk160),
inference(cnf_transformation,[status(esa)],[f418_sk]) ).
fof(f419,axiom,
? [A] :
( complemented_lattstr(A)
& bounded_lattstr(A)
& upper_bounded_semilattstr(A)
& lower_bounded_semilattstr(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/sandbox2/benchmark/theBenchmark.p',rc12_lattices) ).
fof(f419_nnf,plain,
? [A] :
( complemented_lattstr(A)
& bounded_lattstr(A)
& upper_bounded_semilattstr(A)
& lower_bounded_semilattstr(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)],[f419]) ).
fof(f419_sk,plain,
( complemented_lattstr(sk161)
& bounded_lattstr(sk161)
& upper_bounded_semilattstr(sk161)
& lower_bounded_semilattstr(sk161)
& lattice(sk161)
& join_absorbing(sk161)
& meet_absorbing(sk161)
& meet_associative(sk161)
& meet_commutative(sk161)
& join_associative(sk161)
& join_commutative(sk161)
& strict_latt_str(sk161)
& ~ empty_carrier(sk161)
& latt_str(sk161) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk161])],[f419_nnf]) ).
cnf(c1282,plain,
~ empty_carrier(sk161),
inference(cnf_transformation,[status(esa)],[f419_sk]) ).
fof(f420,axiom,
? [A] :
( boolean_lattstr(A)
& complemented_lattstr(A)
& bounded_lattstr(A)
& upper_bounded_semilattstr(A)
& lower_bounded_semilattstr(A)
& distributive_lattstr(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/sandbox2/benchmark/theBenchmark.p',rc13_lattices) ).
fof(f420_nnf,plain,
? [A] :
( boolean_lattstr(A)
& complemented_lattstr(A)
& bounded_lattstr(A)
& upper_bounded_semilattstr(A)
& lower_bounded_semilattstr(A)
& distributive_lattstr(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)],[f420]) ).
fof(f420_sk,plain,
( boolean_lattstr(sk162)
& complemented_lattstr(sk162)
& bounded_lattstr(sk162)
& upper_bounded_semilattstr(sk162)
& lower_bounded_semilattstr(sk162)
& distributive_lattstr(sk162)
& lattice(sk162)
& join_absorbing(sk162)
& meet_absorbing(sk162)
& meet_associative(sk162)
& meet_commutative(sk162)
& join_associative(sk162)
& join_commutative(sk162)
& strict_latt_str(sk162)
& ~ empty_carrier(sk162)
& latt_str(sk162) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk162])],[f420_nnf]) ).
cnf(c1296,plain,
~ empty_carrier(sk162),
inference(cnf_transformation,[status(esa)],[f420_sk]) ).
fof(f421,axiom,
? [A] :
( natural(A)
& ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A)
& ~ empty(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc1_arytm_3) ).
fof(f421_nnf,plain,
? [A] :
( natural(A)
& ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A)
& ~ empty(A) ),
inference(nnf_transformation,[status(thm)],[f421]) ).
fof(f421_sk,plain,
( natural(sk163)
& ordinal(sk163)
& epsilon_connected(sk163)
& epsilon_transitive(sk163)
& ~ empty(sk163) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk163])],[f421_nnf]) ).
cnf(c1311,plain,
~ empty(sk163),
inference(cnf_transformation,[status(esa)],[f421_sk]) ).
fof(f422,axiom,
? [A] :
( finite(A)
& ~ empty(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc1_finset_1) ).
fof(f422_nnf,plain,
? [A] :
( finite(A)
& ~ empty(A) ),
inference(nnf_transformation,[status(thm)],[f422]) ).
fof(f422_sk,plain,
( finite(sk164)
& ~ empty(sk164) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk164])],[f422_nnf]) ).
cnf(c1316,plain,
~ empty(sk164),
inference(cnf_transformation,[status(esa)],[f422_sk]) ).
fof(f425,axiom,
? [A] :
( complete_relstr(A)
& antisymmetric_relstr(A)
& transitive_relstr(A)
& reflexive_relstr(A)
& strict_rel_str(A)
& ~ empty_carrier(A)
& rel_str(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc1_lattice3) ).
fof(f425_nnf,plain,
? [A] :
( complete_relstr(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)],[f425]) ).
fof(f425_sk,plain,
( complete_relstr(sk167)
& antisymmetric_relstr(sk167)
& transitive_relstr(sk167)
& reflexive_relstr(sk167)
& strict_rel_str(sk167)
& ~ empty_carrier(sk167)
& rel_str(sk167) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk167])],[f425_nnf]) ).
cnf(c1325,plain,
~ empty_carrier(sk167),
inference(cnf_transformation,[status(esa)],[f425_sk]) ).
fof(f426,axiom,
? [A] :
( v5_membered(A)
& v4_membered(A)
& v3_membered(A)
& v2_membered(A)
& v1_membered(A)
& ~ empty(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc1_membered) ).
fof(f426_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)],[f426]) ).
fof(f426_sk,plain,
( v5_membered(sk168)
& v4_membered(sk168)
& v3_membered(sk168)
& v2_membered(sk168)
& v1_membered(sk168)
& ~ empty(sk168) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk168])],[f426_nnf]) ).
cnf(c1331,plain,
~ empty(sk168),
inference(cnf_transformation,[status(esa)],[f426_sk]) ).
fof(f436,axiom,
? [A] :
( trivial_carrier(A)
& complete_relstr(A)
& with_infima_relstr(A)
& with_suprema_relstr(A)
& antisymmetric_relstr(A)
& transitive_relstr(A)
& reflexive_relstr(A)
& strict_rel_str(A)
& ~ empty_carrier(A)
& rel_str(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc1_yellow_0) ).
fof(f436_nnf,plain,
? [A] :
( trivial_carrier(A)
& complete_relstr(A)
& with_infima_relstr(A)
& with_suprema_relstr(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)],[f436]) ).
fof(f436_sk,plain,
( trivial_carrier(sk178)
& complete_relstr(sk178)
& with_infima_relstr(sk178)
& with_suprema_relstr(sk178)
& antisymmetric_relstr(sk178)
& transitive_relstr(sk178)
& reflexive_relstr(sk178)
& strict_rel_str(sk178)
& ~ empty_carrier(sk178)
& rel_str(sk178) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk178])],[f436_nnf]) ).
cnf(c1361,plain,
~ empty_carrier(sk178),
inference(cnf_transformation,[status(esa)],[f436_sk]) ).
fof(f440,axiom,
? [A] :
( complete_relstr(A)
& with_infima_relstr(A)
& with_suprema_relstr(A)
& antisymmetric_relstr(A)
& transitive_relstr(A)
& reflexive_relstr(A)
& strict_rel_str(A)
& ~ empty_carrier(A)
& rel_str(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc2_lattice3) ).
fof(f440_nnf,plain,
? [A] :
( complete_relstr(A)
& with_infima_relstr(A)
& with_suprema_relstr(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)],[f440]) ).
fof(f440_sk,plain,
( complete_relstr(sk182)
& with_infima_relstr(sk182)
& with_suprema_relstr(sk182)
& antisymmetric_relstr(sk182)
& transitive_relstr(sk182)
& reflexive_relstr(sk182)
& strict_rel_str(sk182)
& ~ empty_carrier(sk182)
& rel_str(sk182) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk182])],[f440_nnf]) ).
cnf(c1391,plain,
~ empty_carrier(sk182),
inference(cnf_transformation,[status(esa)],[f440_sk]) ).
fof(f441,axiom,
? [A] :
( antisymmetric_relstr(A)
& transitive_relstr(A)
& reflexive_relstr(A)
& strict_rel_str(A)
& ~ empty_carrier(A)
& rel_str(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc2_orders_2) ).
fof(f441_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)],[f441]) ).
fof(f441_sk,plain,
( antisymmetric_relstr(sk183)
& transitive_relstr(sk183)
& reflexive_relstr(sk183)
& strict_rel_str(sk183)
& ~ empty_carrier(sk183)
& rel_str(sk183) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk183])],[f441_nnf]) ).
cnf(c1400,plain,
~ empty_carrier(sk183),
inference(cnf_transformation,[status(esa)],[f441_sk]) ).
fof(f444,axiom,
? [A] :
( relation(A)
& ~ empty(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc2_relat_1) ).
fof(f444_nnf,plain,
? [A] :
( relation(A)
& ~ empty(A) ),
inference(nnf_transformation,[status(thm)],[f444]) ).
fof(f444_sk,plain,
( relation(sk186)
& ~ empty(sk186) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk186])],[f444_nnf]) ).
cnf(c1415,plain,
~ empty(sk186),
inference(cnf_transformation,[status(esa)],[f444_sk]) ).
fof(f446,axiom,
! [A] :
? [B] :
( ~ proper_element(B,powerset(A))
& element(B,powerset(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc2_tex_2) ).
fof(f446_nnf,plain,
! [A] :
? [B] :
( ~ proper_element(B,powerset(A))
& element(B,powerset(A)) ),
inference(nnf_transformation,[status(thm)],[f446]) ).
fof(f446_sk,plain,
! [A] :
( ~ proper_element(sk188(A),powerset(A))
& element(sk188(A),powerset(A)) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk188])],[f446_nnf]) ).
cnf(c1420,plain,
~ proper_element(sk188(X0),powerset(X0)),
inference(cnf_transformation,[status(esa)],[f446_sk]) ).
fof(f448,axiom,
? [A] : ~ empty(A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc2_xboole_0) ).
fof(f448_nnf,plain,
? [A] : ~ empty(A),
inference(nnf_transformation,[status(thm)],[f448]) ).
fof(f448_sk,plain,
~ empty(sk190),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk190])],[f448_nnf]) ).
cnf(c1424,plain,
~ empty(sk190),
inference(cnf_transformation,[status(esa)],[f448_sk]) ).
fof(f449,axiom,
? [A] :
( bounded_relstr(A)
& upper_bounded_relstr(A)
& lower_bounded_relstr(A)
& complete_relstr(A)
& with_infima_relstr(A)
& with_suprema_relstr(A)
& antisymmetric_relstr(A)
& transitive_relstr(A)
& reflexive_relstr(A)
& ~ empty_carrier(A)
& rel_str(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc2_yellow_0) ).
fof(f449_nnf,plain,
? [A] :
( bounded_relstr(A)
& upper_bounded_relstr(A)
& lower_bounded_relstr(A)
& complete_relstr(A)
& with_infima_relstr(A)
& with_suprema_relstr(A)
& antisymmetric_relstr(A)
& transitive_relstr(A)
& reflexive_relstr(A)
& ~ empty_carrier(A)
& rel_str(A) ),
inference(nnf_transformation,[status(thm)],[f449]) ).
fof(f449_sk,plain,
( bounded_relstr(sk191)
& upper_bounded_relstr(sk191)
& lower_bounded_relstr(sk191)
& complete_relstr(sk191)
& with_infima_relstr(sk191)
& with_suprema_relstr(sk191)
& antisymmetric_relstr(sk191)
& transitive_relstr(sk191)
& reflexive_relstr(sk191)
& ~ empty_carrier(sk191)
& rel_str(sk191) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk191])],[f449_nnf]) ).
cnf(c1426,plain,
~ empty_carrier(sk191),
inference(cnf_transformation,[status(esa)],[f449_sk]) ).
fof(f453,axiom,
? [A] :
( ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A)
& ~ empty(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc3_ordinal1) ).
fof(f453_nnf,plain,
? [A] :
( ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A)
& ~ empty(A) ),
inference(nnf_transformation,[status(thm)],[f453]) ).
fof(f453_sk,plain,
( ordinal(sk195)
& epsilon_connected(sk195)
& epsilon_transitive(sk195)
& ~ empty(sk195) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk195])],[f453_nnf]) ).
cnf(c1444,plain,
~ empty(sk195),
inference(cnf_transformation,[status(esa)],[f453_sk]) ).
fof(f456,axiom,
? [A] :
( ~ empty_carrier(A)
& one_sorted_str(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc3_struct_0) ).
fof(f456_nnf,plain,
? [A] :
( ~ empty_carrier(A)
& one_sorted_str(A) ),
inference(nnf_transformation,[status(thm)],[f456]) ).
fof(f456_sk,plain,
( ~ empty_carrier(sk198)
& one_sorted_str(sk198) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk198])],[f456_nnf]) ).
cnf(c1458,plain,
~ empty_carrier(sk198),
inference(cnf_transformation,[status(esa)],[f456_sk]) ).
fof(f460,axiom,
? [A] :
( strict_latt_str(A)
& ~ empty_carrier(A)
& latt_str(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc6_lattices) ).
fof(f460_nnf,plain,
? [A] :
( strict_latt_str(A)
& ~ empty_carrier(A)
& latt_str(A) ),
inference(nnf_transformation,[status(thm)],[f460]) ).
fof(f460_sk,plain,
( strict_latt_str(sk202)
& ~ empty_carrier(sk202)
& latt_str(sk202) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk202])],[f460_nnf]) ).
cnf(c1468,plain,
~ empty_carrier(sk202),
inference(cnf_transformation,[status(esa)],[f460_sk]) ).
fof(f463,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/sandbox2/benchmark/theBenchmark.p',rc9_lattices) ).
fof(f463_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)],[f463]) ).
fof(f463_sk,plain,
( lattice(sk205)
& join_absorbing(sk205)
& meet_absorbing(sk205)
& meet_associative(sk205)
& meet_commutative(sk205)
& join_associative(sk205)
& join_commutative(sk205)
& strict_latt_str(sk205)
& ~ empty_carrier(sk205)
& latt_str(sk205) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk205])],[f463_nnf]) ).
cnf(c1476,plain,
~ empty_carrier(sk205),
inference(cnf_transformation,[status(esa)],[f463_sk]) ).
fof(f500,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/sandbox2/benchmark/theBenchmark.p',s1_ordinal2__e18_27__finset_1) ).
fof(f500_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)],[f500]) ).
fof(f500_sk,plain,
! [B,E,G,I,K,L,N,P,D,R,T] :
( ( ( T = sk239(D,R)
| ~ subset(sk239(D,R),T)
| ~ in(T,R) )
& in(sk239(D,R),R) )
| R = empty_set
| ~ element(R,powerset(powerset(D)))
| ~ in(D,omega)
| ~ ordinal(D)
| ( ( ( sk238(P) != P
& subset(P,sk238(P))
& in(sk238(P),sk237) )
| ~ in(P,sk237) )
& sk237 != empty_set
& element(sk237,powerset(powerset(sk235)))
& in(sk235,omega)
& sk235 != empty_set
& ( ( ( N = sk236(K,L)
| ~ subset(sk236(K,L),N)
| ~ in(N,L) )
& in(sk236(K,L),L) )
| L = empty_set
| ~ element(L,powerset(powerset(K)))
| ~ in(K,omega)
| ~ in(K,sk235)
| ~ ordinal(K) )
& being_limit_ordinal(sk235)
& ordinal(sk235) )
| ( ( ( sk234(I) != I
& subset(I,sk234(I))
& in(sk234(I),sk233) )
| ~ in(I,sk233) )
& sk233 != empty_set
& element(sk233,powerset(powerset(succ(sk231))))
& in(succ(sk231),omega)
& ( ( ( G = sk232(E)
| ~ subset(sk232(E),G)
| ~ in(G,E) )
& in(sk232(E),E) )
| E = empty_set
| ~ element(E,powerset(powerset(sk231)))
| ~ in(sk231,omega) )
& ordinal(sk231) )
| ( ( ( sk230(B) != B
& subset(B,sk230(B))
& in(sk230(B),sk229) )
| ~ in(B,sk229) )
& sk229 != empty_set
& element(sk229,powerset(powerset(empty_set)))
& in(empty_set,omega) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk229,sk230,sk231,sk232,sk233,sk234,sk235,sk236,sk237,sk238,sk239])],[f500_nnf]) ).
cnf(c1719,plain,
( sk230(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])],[f500_sk]) ).
cnf(c1724,plain,
( sk229 != 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])],[f500_sk]) ).
cnf(c1733,plain,
( ~ subset(sk232(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])],[f500_sk]) ).
cnf(c1755,plain,
( sk234(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])],[f500_sk]) ).
cnf(c1760,plain,
( sk233 != 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])],[f500_sk]) ).
cnf(c1778,plain,
( ~ subset(sk236(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])],[f500_sk]) ).
cnf(c1809,plain,
( sk238(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])],[f500_sk]) ).
cnf(c1814,plain,
( sk237 != 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])],[f500_sk]) ).
cnf(c1823,plain,
( sk235 != 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])],[f500_sk]) ).
cnf(c1835,plain,
( ~ subset(sk239(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])],[f500_sk]) ).
fof(f669,lemma,
! [A,B,C] :
~ ( in(C,A)
& in(B,C)
& in(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t3_ordinal1) ).
fof(f669_nnf,plain,
! [A,B,C] :
( ~ in(C,A)
| ~ in(B,C)
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f669]) ).
fof(f669_sk,plain,
! [A,B,C] :
( ~ in(C,A)
| ~ in(B,C)
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f669_nnf]) ).
cnf(c3462,plain,
( ~ in(X2,X0)
| ~ in(X1,X2)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f669_sk]) ).
fof(f672,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/sandbox2/benchmark/theBenchmark.p',t3_xboole_0) ).
fof(f672_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)],[f672]) ).
fof(f672_sk,plain,
! [A,B,C] :
( ( ~ disjoint(A,B)
| ~ in(C,B)
| ~ in(C,A) )
& ( ( in(sk497(A,B),B)
& in(sk497(A,B),A) )
| disjoint(A,B) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk497])],[f672_nnf]) ).
cnf(c3468,plain,
( ~ disjoint(X0,X1)
| ~ in(X2,X1)
| ~ in(X2,X0) ),
inference(cnf_transformation,[status(esa)],[f672_sk]) ).
fof(f676,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/sandbox2/benchmark/theBenchmark.p',t42_ordinal1) ).
fof(f676_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)],[f676]) ).
fof(f676_sk,plain,
! [A,B] :
( ( ( ~ being_limit_ordinal(A)
| A != succ(B)
| ~ ordinal(B) )
& ( ( A = succ(sk499(A))
& ordinal(sk499(A)) )
| being_limit_ordinal(A) ) )
| ~ ordinal(A) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk499])],[f676_nnf]) ).
cnf(c3477,plain,
( ~ being_limit_ordinal(X0)
| X0 != succ(X1)
| ~ ordinal(X1)
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(esa)],[f676_sk]) ).
fof(f700,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/sandbox2/benchmark/theBenchmark.p',t4_xboole_0) ).
fof(f700_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)],[f700]) ).
fof(f700_sk,plain,
! [A,B,C] :
( ( ~ disjoint(A,B)
| ~ in(C,set_intersection2(A,B)) )
& ( in(sk503(A,B),set_intersection2(A,B))
| disjoint(A,B) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk503])],[f700_nnf]) ).
cnf(c3516,plain,
( ~ disjoint(X0,X1)
| ~ in(X2,set_intersection2(X0,X1)) ),
inference(cnf_transformation,[status(esa)],[f700_sk]) ).
fof(f708,lemma,
! [A,B,C] :
( element(C,powerset(A))
=> ~ ( in(B,C)
& in(B,subset_complement(A,C)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t54_subset_1) ).
fof(f708_nnf,plain,
! [A,B,C] :
( ~ in(B,C)
| ~ in(B,subset_complement(A,C))
| ~ element(C,powerset(A)) ),
inference(nnf_transformation,[status(thm)],[f708]) ).
fof(f708_sk,plain,
! [C,A,B] :
( ~ in(B,C)
| ~ in(B,subset_complement(A,C))
| ~ element(C,powerset(A)) ),
inference(skolemisation,[status(esa)],[f708_nnf]) ).
cnf(c3546,plain,
( ~ in(X1,X2)
| ~ in(X1,subset_complement(X0,X2))
| ~ element(X2,powerset(X0)) ),
inference(cnf_transformation,[status(esa)],[f708_sk]) ).
fof(f715,axiom,
! [A,B,C] :
~ ( empty(C)
& element(B,powerset(C))
& in(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_subset) ).
fof(f715_nnf,plain,
! [A,B,C] :
( ~ empty(C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f715]) ).
fof(f715_sk,plain,
! [A,B,C] :
( ~ empty(C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f715_nnf]) ).
cnf(c3556,plain,
( ~ empty(X2)
| ~ element(X1,powerset(X2))
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f715_sk]) ).
fof(f716,lemma,
! [A,B] :
( element(B,powerset(A))
=> ( proper_element(B,powerset(A))
<=> B != A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_tex_2) ).
fof(f716_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)],[f716]) ).
fof(f716_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)],[f716_nnf]) ).
cnf(c3557,plain,
( X1 != X0
| ~ proper_element(X1,powerset(X0))
| ~ element(X1,powerset(X0)) ),
inference(cnf_transformation,[status(esa)],[f716_sk]) ).
fof(f721,lemma,
! [A,B] :
~ ( proper_subset(B,A)
& subset(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t60_xboole_1) ).
fof(f721_nnf,plain,
! [A,B] :
( ~ proper_subset(B,A)
| ~ subset(A,B) ),
inference(nnf_transformation,[status(thm)],[f721]) ).
fof(f721_sk,plain,
! [A,B] :
( ~ proper_subset(B,A)
| ~ subset(A,B) ),
inference(skolemisation,[status(esa)],[f721_nnf]) ).
cnf(c3565,plain,
( ~ proper_subset(X1,X0)
| ~ subset(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f721_sk]) ).
fof(f728,lemma,
! [A,B] :
( set_difference(A,singleton(B)) = A
<=> ~ in(B,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t65_zfmisc_1) ).
fof(f728_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)],[f728]) ).
fof(f728_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)],[f728_nnf]) ).
cnf(c3574,plain,
( ~ in(X1,X0)
| set_difference(X0,singleton(X1)) != X0 ),
inference(cnf_transformation,[status(esa)],[f728_sk]) ).
fof(f741,axiom,
! [A,B] :
~ ( empty(B)
& in(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t7_boole) ).
fof(f741_nnf,plain,
! [A,B] :
( ~ empty(B)
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f741]) ).
fof(f741_sk,plain,
! [A,B] :
( ~ empty(B)
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f741_nnf]) ).
cnf(c3597,plain,
( ~ empty(X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f741_sk]) ).
fof(f744,axiom,
! [A,B] :
~ ( ! [C] :
~ ( ! [D] :
~ ( in(D,C)
& in(D,B) )
& in(C,B) )
& in(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t7_tarski) ).
fof(f744_nnf,plain,
! [A,B] :
( ? [C] :
( ! [D] :
( ~ in(D,C)
| ~ in(D,B) )
& in(C,B) )
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f744]) ).
fof(f744_sk,plain,
! [A,B,D] :
( ( ( ~ in(D,sk510(A,B))
| ~ in(D,B) )
& in(sk510(A,B),B) )
| ~ in(A,B) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk510])],[f744_nnf]) ).
cnf(c3603,plain,
( ~ in(X3,sk510(X0,X1))
| ~ in(X3,X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f744_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c2,c3,c54,c90,c235,c390,c408,c423,c457,c571,c713,c905,c907,c913,c930,c934,c938,c947,c949,c959,c964,c969,c978,c1008,c1058,c1080,c1085,c1163,c1170,c1209,c1213,c1215,c1255,c1269,c1282,c1296,c1311,c1316,c1325,c1331,c1361,c1391,c1400,c1415,c1420,c1424,c1426,c1444,c1458,c1468,c1476,c1719,c1724,c1733,c1755,c1760,c1778,c1809,c1814,c1823,c1835,c3340,c3462,c3468,c3477,c3516,c3546,c3556,c3557,c3565,c3574,c3597,c3603]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t8070]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU374+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.36 % Computer : n001.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Thu Sep 24 13:59:22 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 80.06/10.52 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 80.06/10.52 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------