%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SEU361+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 : n005.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:50 PM UTC 2026
% Result : Theorem 93.56s 12.75s
% Output : Proof 93.56s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 55
% Syntax : Number of formulae : 293 ( 119 unt; 0 def)
% Number of atoms : 1054 ( 207 equ)
% Maximal formula atoms : 49 ( 3 avg)
% Number of connectives : 1275 ( 514 ~; 303 |; 388 &)
% ( 12 <=>; 58 =>; 0 <=; 0 <~>)
% Maximal formula depth : 27 ( 5 avg)
% Maximal term depth : 8 ( 1 avg)
% Number of predicates : 59 ( 57 usr; 1 prp; 0-3 aty)
% Number of functors : 58 ( 58 usr; 21 con; 0-4 aty)
% Number of variables : 478 ( 31 sgn 296 !; 50 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f573,lemma,
! [A] :
( ( rel_str(A)
& antisymmetric_relstr(A) )
=> ! [B] :
( element(B,the_carrier(A))
=> ! [C] :
( ( ( ! [D] :
( element(D,the_carrier(A))
=> ( relstr_set_smaller(A,C,D)
=> related(A,B,D) ) )
& relstr_set_smaller(A,C,B) )
=> ( ex_sup_of_relstr_set(A,C)
& B = join_on_relstr(A,C) ) )
& ( ( ex_sup_of_relstr_set(A,C)
& B = join_on_relstr(A,C) )
=> ( ! [D] :
( element(D,the_carrier(A))
=> ( relstr_set_smaller(A,C,D)
=> related(A,B,D) ) )
& relstr_set_smaller(A,C,B) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t30_yellow_0) ).
fof(f573_nnf,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( ( ex_sup_of_relstr_set(A,C)
& B = join_on_relstr(A,C) )
| ? [D] :
( ~ related(A,B,D)
& relstr_set_smaller(A,C,D)
& element(D,the_carrier(A)) )
| ~ relstr_set_smaller(A,C,B) )
& ( ( ! [D] :
( related(A,B,D)
| ~ relstr_set_smaller(A,C,D)
| ~ element(D,the_carrier(A)) )
& relstr_set_smaller(A,C,B) )
| ~ ex_sup_of_relstr_set(A,C)
| B != join_on_relstr(A,C) ) )
| ~ element(B,the_carrier(A)) )
| ~ rel_str(A)
| ~ antisymmetric_relstr(A) ),
inference(nnf_transformation,[status(thm)],[f573]) ).
fof(f573_sk,plain,
! [A,B,C,D] :
( ( ( ( ex_sup_of_relstr_set(A,C)
& B = join_on_relstr(A,C) )
| ( ~ related(A,B,sk446(A,B,C))
& relstr_set_smaller(A,C,sk446(A,B,C))
& element(sk446(A,B,C),the_carrier(A)) )
| ~ relstr_set_smaller(A,C,B) )
& ( ( ( related(A,B,D)
| ~ relstr_set_smaller(A,C,D)
| ~ element(D,the_carrier(A)) )
& relstr_set_smaller(A,C,B) )
| ~ ex_sup_of_relstr_set(A,C)
| B != join_on_relstr(A,C) ) )
| ~ element(B,the_carrier(A))
| ~ rel_str(A)
| ~ antisymmetric_relstr(A) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk446])],[f573_nnf]) ).
cnf(c2983,plain,
( related(X0,X1,X3)
| ~ relstr_set_smaller(X0,X2,X3)
| ~ element(X3,the_carrier(X0))
| ~ ex_sup_of_relstr_set(X0,X2)
| X1 != join_on_relstr(X0,X2)
| ~ element(X1,the_carrier(X0))
| ~ rel_str(X0)
| ~ antisymmetric_relstr(X0) ),
inference(cnf_transformation,[status(esa)],[f573_sk]) ).
cnf(t99,plain,
ifeq(antisymmetric_relstr(X1),true,ifeq(rel_str(X1),true,ifeq(element(X2,the_carrier(X1)),true,ifeq(X2,join_on_relstr(X1,X3),ifeq(ex_sup_of_relstr_set(X1,X3),true,ifeq(element(X4,the_carrier(X1)),true,ifeq(relstr_set_smaller(X1,X3,X4),true,related(X1,X2,X4),true),true),true),true),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c2983]) ).
cnf(t152,plain,
ifeq(antisymmetric_relstr(X1),true,ifeq(rel_str(X1),true,ifeq(element(X2,the_carrier(X1)),true,ifeq(X2,join_on_relstr(X1,X3),ifeq(ex_sup_of_relstr_set(X1,X3),true,ifeq(element(X4,the_carrier(X1)),true,ifeq(relstr_set_smaller(X1,X3,X4),true,related(X1,X2,X4),true),true),true),true),true),true),true) = true,
inference(orient,[status(thm)],[t99]) ).
cnf(t35,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t100,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t35]) ).
cnf(t153,plain,
true = ifeq(antisymmetric_relstr(X1),true,ifeq(rel_str(X1),true,ifeq(element(join_on_relstr(X1,X2),the_carrier(X1)),true,ifeq(ex_sup_of_relstr_set(X1,X2),true,ifeq(element(X3,the_carrier(X1)),true,ifeq(relstr_set_smaller(X1,X2,X3),true,related(X1,join_on_relstr(X1,X2),X3),true),true),true),true),true),true),
inference(cp,[status(thm)],[t152,t100]) ).
cnf(t791,plain,
ifeq(antisymmetric_relstr(X1),true,ifeq(rel_str(X1),true,ifeq(element(join_on_relstr(X1,X2),the_carrier(X1)),true,ifeq(ex_sup_of_relstr_set(X1,X2),true,ifeq(element(X3,the_carrier(X1)),true,ifeq(relstr_set_smaller(X1,X2,X3),true,related(X1,join_on_relstr(X1,X2),X3),true),true),true),true),true),true) = true,
inference(orient,[status(thm)],[t153]) ).
fof(f658,lemma,
! [A] :
( rel_str(A)
=> ! [B] :
( element(B,the_carrier(A))
=> ( relstr_element_smaller(A,empty_set,B)
& relstr_set_smaller(A,empty_set,B) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t6_yellow_0) ).
fof(f658_nnf,plain,
! [A] :
( ! [B] :
( ( relstr_element_smaller(A,empty_set,B)
& relstr_set_smaller(A,empty_set,B) )
| ~ element(B,the_carrier(A)) )
| ~ rel_str(A) ),
inference(nnf_transformation,[status(thm)],[f658]) ).
fof(f658_sk,plain,
! [A,B] :
( ( relstr_element_smaller(A,empty_set,B)
& relstr_set_smaller(A,empty_set,B) )
| ~ element(B,the_carrier(A))
| ~ rel_str(A) ),
inference(skolemisation,[status(esa)],[f658_nnf]) ).
cnf(c3158,plain,
( relstr_set_smaller(X0,empty_set,X1)
| ~ element(X1,the_carrier(X0))
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(esa)],[f658_sk]) ).
cnf(t85,plain,
ifeq(rel_str(X1),true,ifeq(element(X2,the_carrier(X1)),true,relstr_set_smaller(X1,empty_set,X2),true),true) = true,
inference(equality_encoding,[status(esa)],[c3158]) ).
cnf(t140,plain,
ifeq(rel_str(X1),true,ifeq(element(X2,the_carrier(X1)),true,relstr_set_smaller(X1,empty_set,X2),true),true) = true,
inference(orient,[status(thm)],[t85]) ).
fof(f609,conjecture,
! [A] :
( ( rel_str(A)
& lower_bounded_relstr(A)
& antisymmetric_relstr(A)
& ~ empty_carrier(A) )
=> ! [B] :
( element(B,the_carrier(A))
=> related(A,bottom_of_relstr(A),B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t44_yellow_0) ).
fof(f609_neg,negated_conjecture,
~ ! [A] :
( ( rel_str(A)
& lower_bounded_relstr(A)
& antisymmetric_relstr(A)
& ~ empty_carrier(A) )
=> ! [B] :
( element(B,the_carrier(A))
=> related(A,bottom_of_relstr(A),B) ) ),
inference(negated_conjecture,[status(cth)],[f609]) ).
fof(f609_nnf,plain,
? [A] :
( ? [B] :
( ~ related(A,bottom_of_relstr(A),B)
& element(B,the_carrier(A)) )
& rel_str(A)
& lower_bounded_relstr(A)
& antisymmetric_relstr(A)
& ~ empty_carrier(A) ),
inference(nnf_transformation,[status(thm)],[f609_neg]) ).
fof(f609_sk,plain,
( ~ related(sk455,bottom_of_relstr(sk455),sk456)
& element(sk456,the_carrier(sk455))
& rel_str(sk455)
& lower_bounded_relstr(sk455)
& antisymmetric_relstr(sk455)
& ~ empty_carrier(sk455) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk455,sk456])],[f609_nnf]) ).
cnf(c3063,plain,
element(sk456,the_carrier(sk455)),
inference(cnf_transformation,[status(esa)],[f609_sk]) ).
cnf(t20,plain,
element(sk456,the_carrier(sk455)) = true,
inference(equality_encoding,[status(esa)],[c3063]) ).
cnf(t188,plain,
element(sk456,the_carrier(sk455)) = true,
inference(orient,[status(thm)],[t20]) ).
cnf(t194,plain,
true = ifeq(rel_str(sk455),true,ifeq(true,true,relstr_set_smaller(sk455,empty_set,sk456),true),true),
inference(cp,[status(thm)],[t140,t188]) ).
cnf(c3062,plain,
rel_str(sk455),
inference(cnf_transformation,[status(esa)],[f609_sk]) ).
cnf(t9,plain,
rel_str(sk455) = true,
inference(equality_encoding,[status(esa)],[c3062]) ).
cnf(t240,plain,
rel_str(sk455) = true,
inference(orient,[status(thm)],[t9]) ).
cnf(t933,plain,
true = ifeq(true,true,ifeq(true,true,relstr_set_smaller(sk455,empty_set,sk456),true),true),
inference(step,[status(thm)],[t194,t240]) ).
cnf(t934,plain,
true = ifeq(true,true,relstr_set_smaller(sk455,empty_set,sk456),true),
inference(step,[status(thm)],[t933,t100]) ).
cnf(t935,plain,
true = relstr_set_smaller(sk455,empty_set,sk456),
inference(step,[status(thm)],[t934,t100]) ).
cnf(t561,plain,
relstr_set_smaller(sk455,empty_set,sk456) = true,
inference(orient,[status(thm)],[t935]) ).
cnf(t803,plain,
true = ifeq(antisymmetric_relstr(sk455),true,ifeq(rel_str(sk455),true,ifeq(element(join_on_relstr(sk455,empty_set),the_carrier(sk455)),true,ifeq(ex_sup_of_relstr_set(sk455,empty_set),true,ifeq(element(sk456,the_carrier(sk455)),true,ifeq(true,true,related(sk455,join_on_relstr(sk455,empty_set),sk456),true),true),true),true),true),true),
inference(cp,[status(thm)],[t791,t561]) ).
cnf(c3060,plain,
antisymmetric_relstr(sk455),
inference(cnf_transformation,[status(esa)],[f609_sk]) ).
cnf(t0,plain,
antisymmetric_relstr(sk455) = true,
inference(equality_encoding,[status(esa)],[c3060]) ).
cnf(t267,plain,
antisymmetric_relstr(sk455) = true,
inference(orient,[status(thm)],[t0]) ).
cnf(t984,plain,
true = ifeq(true,true,ifeq(rel_str(sk455),true,ifeq(element(join_on_relstr(sk455,empty_set),the_carrier(sk455)),true,ifeq(ex_sup_of_relstr_set(sk455,empty_set),true,ifeq(element(sk456,the_carrier(sk455)),true,ifeq(true,true,related(sk455,join_on_relstr(sk455,empty_set),sk456),true),true),true),true),true),true),
inference(step,[status(thm)],[t803,t267]) ).
cnf(t985,plain,
true = ifeq(rel_str(sk455),true,ifeq(element(join_on_relstr(sk455,empty_set),the_carrier(sk455)),true,ifeq(ex_sup_of_relstr_set(sk455,empty_set),true,ifeq(element(sk456,the_carrier(sk455)),true,ifeq(true,true,related(sk455,join_on_relstr(sk455,empty_set),sk456),true),true),true),true),true),
inference(step,[status(thm)],[t984,t100]) ).
cnf(t986,plain,
true = ifeq(true,true,ifeq(element(join_on_relstr(sk455,empty_set),the_carrier(sk455)),true,ifeq(ex_sup_of_relstr_set(sk455,empty_set),true,ifeq(element(sk456,the_carrier(sk455)),true,ifeq(true,true,related(sk455,join_on_relstr(sk455,empty_set),sk456),true),true),true),true),true),
inference(step,[status(thm)],[t985,t240]) ).
cnf(t987,plain,
true = ifeq(element(join_on_relstr(sk455,empty_set),the_carrier(sk455)),true,ifeq(ex_sup_of_relstr_set(sk455,empty_set),true,ifeq(element(sk456,the_carrier(sk455)),true,ifeq(true,true,related(sk455,join_on_relstr(sk455,empty_set),sk456),true),true),true),true),
inference(step,[status(thm)],[t986,t100]) ).
fof(f184,axiom,
! [A,B] :
( rel_str(A)
=> element(join_on_relstr(A,B),the_carrier(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k1_yellow_0) ).
fof(f184_nnf,plain,
! [A,B] :
( element(join_on_relstr(A,B),the_carrier(A))
| ~ rel_str(A) ),
inference(nnf_transformation,[status(thm)],[f184]) ).
fof(f184_sk,plain,
! [A,B] :
( element(join_on_relstr(A,B),the_carrier(A))
| ~ rel_str(A) ),
inference(skolemisation,[status(esa)],[f184_nnf]) ).
cnf(c697,plain,
( element(join_on_relstr(X0,X1),the_carrier(X0))
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(esa)],[f184_sk]) ).
cnf(t73,plain,
ifeq(rel_str(X1),true,element(join_on_relstr(X1,X2),the_carrier(X1)),true) = true,
inference(equality_encoding,[status(esa)],[c697]) ).
cnf(t143,plain,
ifeq(rel_str(X1),true,element(join_on_relstr(X1,X2),the_carrier(X1)),true) = true,
inference(orient,[status(thm)],[t73]) ).
cnf(t242,plain,
true = ifeq(true,true,element(join_on_relstr(sk455,X1),the_carrier(sk455)),true),
inference(cp,[status(thm)],[t143,t240]) ).
cnf(t895,plain,
true = element(join_on_relstr(sk455,X1),the_carrier(sk455)),
inference(step,[status(thm)],[t242,t100]) ).
cnf(t459,plain,
element(join_on_relstr(sk455,X1),the_carrier(sk455)) = true,
inference(orient,[status(thm)],[t895]) ).
cnf(t988,plain,
true = ifeq(true,true,ifeq(ex_sup_of_relstr_set(sk455,empty_set),true,ifeq(element(sk456,the_carrier(sk455)),true,ifeq(true,true,related(sk455,join_on_relstr(sk455,empty_set),sk456),true),true),true),true),
inference(step,[status(thm)],[t987,t459]) ).
cnf(t989,plain,
true = ifeq(ex_sup_of_relstr_set(sk455,empty_set),true,ifeq(element(sk456,the_carrier(sk455)),true,ifeq(true,true,related(sk455,join_on_relstr(sk455,empty_set),sk456),true),true),true),
inference(step,[status(thm)],[t988,t100]) ).
fof(f604,lemma,
! [A] :
( ( rel_str(A)
& lower_bounded_relstr(A)
& antisymmetric_relstr(A)
& ~ empty_carrier(A) )
=> ( ex_inf_of_relstr_set(A,the_carrier(A))
& ex_sup_of_relstr_set(A,empty_set) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t42_yellow_0) ).
fof(f604_nnf,plain,
! [A] :
( ( ex_inf_of_relstr_set(A,the_carrier(A))
& ex_sup_of_relstr_set(A,empty_set) )
| ~ rel_str(A)
| ~ lower_bounded_relstr(A)
| ~ antisymmetric_relstr(A)
| empty_carrier(A) ),
inference(nnf_transformation,[status(thm)],[f604]) ).
fof(f604_sk,plain,
! [A] :
( ( ex_inf_of_relstr_set(A,the_carrier(A))
& ex_sup_of_relstr_set(A,empty_set) )
| ~ rel_str(A)
| ~ lower_bounded_relstr(A)
| ~ antisymmetric_relstr(A)
| empty_carrier(A) ),
inference(skolemisation,[status(esa)],[f604_nnf]) ).
cnf(c3050,plain,
( ex_sup_of_relstr_set(X0,empty_set)
| ~ rel_str(X0)
| ~ lower_bounded_relstr(X0)
| ~ antisymmetric_relstr(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(esa)],[f604_sk]) ).
cnf(t89,plain,
ifeq(antisymmetric_relstr(X1),true,ifeq(lower_bounded_relstr(X1),true,ifeq(rel_str(X1),true,or(empty_carrier(X1),ex_sup_of_relstr_set(X1,empty_set)),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c3050]) ).
cnf(t156,plain,
ifeq(antisymmetric_relstr(X1),true,ifeq(lower_bounded_relstr(X1),true,ifeq(rel_str(X1),true,or(empty_carrier(X1),ex_sup_of_relstr_set(X1,empty_set)),true),true),true) = true,
inference(orient,[status(thm)],[t89]) ).
cnf(c3059,plain,
~ empty_carrier(sk455),
inference(cnf_transformation,[status(esa)],[f609_sk]) ).
cnf(t6,plain,
empty_carrier(sk455) = false,
inference(equality_encoding,[status(esa)],[c3059]) ).
cnf(t352,plain,
empty_carrier(sk455) = false,
inference(orient,[status(thm)],[t6]) ).
cnf(t355,plain,
true = ifeq(antisymmetric_relstr(sk455),true,ifeq(lower_bounded_relstr(sk455),true,ifeq(rel_str(sk455),true,or(false,ex_sup_of_relstr_set(sk455,empty_set)),true),true),true),
inference(cp,[status(thm)],[t156,t352]) ).
cnf(t874,plain,
true = ifeq(true,true,ifeq(lower_bounded_relstr(sk455),true,ifeq(rel_str(sk455),true,or(false,ex_sup_of_relstr_set(sk455,empty_set)),true),true),true),
inference(step,[status(thm)],[t355,t267]) ).
cnf(t875,plain,
true = ifeq(lower_bounded_relstr(sk455),true,ifeq(rel_str(sk455),true,or(false,ex_sup_of_relstr_set(sk455,empty_set)),true),true),
inference(step,[status(thm)],[t874,t100]) ).
cnf(c3061,plain,
lower_bounded_relstr(sk455),
inference(cnf_transformation,[status(esa)],[f609_sk]) ).
cnf(t7,plain,
lower_bounded_relstr(sk455) = true,
inference(equality_encoding,[status(esa)],[c3061]) ).
cnf(t308,plain,
lower_bounded_relstr(sk455) = true,
inference(orient,[status(thm)],[t7]) ).
cnf(t876,plain,
true = ifeq(true,true,ifeq(rel_str(sk455),true,or(false,ex_sup_of_relstr_set(sk455,empty_set)),true),true),
inference(step,[status(thm)],[t875,t308]) ).
cnf(t877,plain,
true = ifeq(rel_str(sk455),true,or(false,ex_sup_of_relstr_set(sk455,empty_set)),true),
inference(step,[status(thm)],[t876,t100]) ).
cnf(t878,plain,
true = ifeq(true,true,or(false,ex_sup_of_relstr_set(sk455,empty_set)),true),
inference(step,[status(thm)],[t877,t240]) ).
cnf(t879,plain,
true = or(false,ex_sup_of_relstr_set(sk455,empty_set)),
inference(step,[status(thm)],[t878,t100]) ).
cnf(t18,plain,
or(false,X1) = X1,
introduced(definition) ).
cnf(t108,plain,
or(false,X1) = X1,
inference(orient,[status(thm)],[t18]) ).
cnf(t880,plain,
true = ex_sup_of_relstr_set(sk455,empty_set),
inference(step,[status(thm)],[t879,t108]) ).
cnf(t386,plain,
ex_sup_of_relstr_set(sk455,empty_set) = true,
inference(orient,[status(thm)],[t880]) ).
cnf(t990,plain,
true = ifeq(true,true,ifeq(element(sk456,the_carrier(sk455)),true,ifeq(true,true,related(sk455,join_on_relstr(sk455,empty_set),sk456),true),true),true),
inference(step,[status(thm)],[t989,t386]) ).
cnf(t991,plain,
true = ifeq(element(sk456,the_carrier(sk455)),true,ifeq(true,true,related(sk455,join_on_relstr(sk455,empty_set),sk456),true),true),
inference(step,[status(thm)],[t990,t100]) ).
cnf(t992,plain,
true = ifeq(true,true,ifeq(true,true,related(sk455,join_on_relstr(sk455,empty_set),sk456),true),true),
inference(step,[status(thm)],[t991,t188]) ).
cnf(t993,plain,
true = ifeq(true,true,related(sk455,join_on_relstr(sk455,empty_set),sk456),true),
inference(step,[status(thm)],[t992,t100]) ).
cnf(t994,plain,
true = related(sk455,join_on_relstr(sk455,empty_set),sk456),
inference(step,[status(thm)],[t993,t100]) ).
fof(f55,axiom,
! [A] :
( rel_str(A)
=> bottom_of_relstr(A) = join_on_relstr(A,empty_set) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d11_yellow_0) ).
fof(f55_nnf,plain,
! [A] :
( bottom_of_relstr(A) = join_on_relstr(A,empty_set)
| ~ rel_str(A) ),
inference(nnf_transformation,[status(thm)],[f55]) ).
fof(f55_sk,plain,
! [A] :
( bottom_of_relstr(A) = join_on_relstr(A,empty_set)
| ~ rel_str(A) ),
inference(skolemisation,[status(esa)],[f55_nnf]) ).
cnf(c138,plain,
( bottom_of_relstr(X0) = join_on_relstr(X0,empty_set)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(esa)],[f55_sk]) ).
cnf(t72,plain,
ifeq(rel_str(X1),true,bottom_of_relstr(X1),join_on_relstr(X1,empty_set)) = join_on_relstr(X1,empty_set),
inference(equality_encoding,[status(esa)],[c138]) ).
cnf(t313,plain,
ifeq(rel_str(X1),true,bottom_of_relstr(X1),join_on_relstr(X1,empty_set)) = join_on_relstr(X1,empty_set),
inference(orient,[status(thm)],[t72]) ).
cnf(t314,plain,
join_on_relstr(sk455,empty_set) = ifeq(true,true,bottom_of_relstr(sk455),join_on_relstr(sk455,empty_set)),
inference(cp,[status(thm)],[t313,t240]) ).
cnf(t881,plain,
join_on_relstr(sk455,empty_set) = bottom_of_relstr(sk455),
inference(step,[status(thm)],[t314,t100]) ).
cnf(t389,plain,
join_on_relstr(sk455,empty_set) = bottom_of_relstr(sk455),
inference(orient,[status(thm)],[t881]) ).
cnf(t995,plain,
true = related(sk455,bottom_of_relstr(sk455),sk456),
inference(step,[status(thm)],[t994,t389]) ).
cnf(c3064,plain,
~ related(sk455,bottom_of_relstr(sk455),sk456),
inference(cnf_transformation,[status(esa)],[f609_sk]) ).
cnf(t36,plain,
related(sk455,bottom_of_relstr(sk455),sk456) = false,
inference(equality_encoding,[status(esa)],[c3064]) ).
cnf(t359,plain,
related(sk455,bottom_of_relstr(sk455),sk456) = false,
inference(orient,[status(thm)],[t36]) ).
cnf(t996,plain,
true = false,
inference(step,[status(thm)],[t995,t359]) ).
cnf(t808,plain,
false = true,
inference(orient,[status(thm)],[t996]) ).
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(f61,axiom,
! [A] :
( top_str(A)
=> ! [B] :
( element(B,powerset(the_carrier(A)))
=> ! [C] :
( element(C,powerset(the_carrier(A)))
=> ( C = topstr_closure(A,B)
<=> ! [D] :
( in(D,the_carrier(A))
=> ( in(D,C)
<=> ! [E] :
( element(E,powerset(the_carrier(A)))
=> ~ ( disjoint(B,E)
& in(D,E)
& open_subset(E,A) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d13_pre_topc) ).
fof(f61_nnf,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( ( ? [D] :
( ( ( ! [E] :
( ~ disjoint(B,E)
| ~ in(D,E)
| ~ open_subset(E,A)
| ~ element(E,powerset(the_carrier(A))) )
& ~ in(D,C) )
| ( ? [E] :
( disjoint(B,E)
& in(D,E)
& open_subset(E,A)
& element(E,powerset(the_carrier(A))) )
& in(D,C) ) )
& in(D,the_carrier(A)) )
| C = topstr_closure(A,B) )
& ( ! [D] :
( ( ( ? [E] :
( disjoint(B,E)
& in(D,E)
& open_subset(E,A)
& element(E,powerset(the_carrier(A))) )
| in(D,C) )
& ( ! [E] :
( ~ disjoint(B,E)
| ~ in(D,E)
| ~ open_subset(E,A)
| ~ element(E,powerset(the_carrier(A))) )
| ~ in(D,C) ) )
| ~ in(D,the_carrier(A)) )
| C != topstr_closure(A,B) ) )
| ~ element(C,powerset(the_carrier(A))) )
| ~ element(B,powerset(the_carrier(A))) )
| ~ top_str(A) ),
inference(nnf_transformation,[status(thm)],[f61]) ).
fof(f61_sk,plain,
! [A,B,C,D,E] :
( ( ( ( ( ( ( ~ disjoint(B,E)
| ~ in(sk14(A,B,C),E)
| ~ open_subset(E,A)
| ~ element(E,powerset(the_carrier(A))) )
& ~ in(sk14(A,B,C),C) )
| ( disjoint(B,sk15(A,B,C))
& in(sk14(A,B,C),sk15(A,B,C))
& open_subset(sk15(A,B,C),A)
& element(sk15(A,B,C),powerset(the_carrier(A)))
& in(sk14(A,B,C),C) ) )
& in(sk14(A,B,C),the_carrier(A)) )
| C = topstr_closure(A,B) )
& ( ( ( ( disjoint(B,sk13(A,B,C,D))
& in(D,sk13(A,B,C,D))
& open_subset(sk13(A,B,C,D),A)
& element(sk13(A,B,C,D),powerset(the_carrier(A))) )
| in(D,C) )
& ( ~ disjoint(B,E)
| ~ in(D,E)
| ~ open_subset(E,A)
| ~ element(E,powerset(the_carrier(A)))
| ~ in(D,C) ) )
| ~ in(D,the_carrier(A))
| C != topstr_closure(A,B) ) )
| ~ element(C,powerset(the_carrier(A)))
| ~ element(B,powerset(the_carrier(A)))
| ~ top_str(A) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk13,sk14,sk15])],[f61_nnf]) ).
cnf(c176,plain,
( ~ disjoint(X1,X4)
| ~ in(X3,X4)
| ~ open_subset(X4,X0)
| ~ element(X4,powerset(the_carrier(X0)))
| ~ in(X3,X2)
| ~ in(X3,the_carrier(X0))
| X2 != topstr_closure(X0,X1)
| ~ element(X2,powerset(the_carrier(X0)))
| ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0) ),
inference(cnf_transformation,[status(esa)],[f61_sk]) ).
fof(f88,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(f88_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)],[f88]) ).
fof(f88_sk,plain,
! [A,C,B,D] :
( ( ( ( in(ordered_pair(sk46(A,B,C),B),A)
& sk46(A,B,C) != B
& ~ in(sk46(A,B,C),C) )
| ( ( ~ in(ordered_pair(sk46(A,B,C),B),A)
| sk46(A,B,C) = B )
& in(sk46(A,B,C),C) )
| C = fiber(A,B) )
& ( ( ( ~ in(ordered_pair(D,B),A)
| D = B
| in(D,C) )
& ( ( in(ordered_pair(D,B),A)
& D != B )
| ~ in(D,C) ) )
| C != fiber(A,B) ) )
| ~ relation(A) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk46])],[f88_nnf]) ).
cnf(c317,plain,
( X3 != X1
| ~ in(X3,X2)
| X2 != fiber(X0,X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(esa)],[f88_sk]) ).
fof(f90,axiom,
! [A] :
( A = empty_set
<=> ! [B] : ~ in(B,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_xboole_0) ).
fof(f90_nnf,plain,
! [A] :
( ( ? [B] : in(B,A)
| A = empty_set )
& ( ! [B] : ~ in(B,A)
| A != empty_set ) ),
inference(nnf_transformation,[status(thm)],[f90]) ).
fof(f90_sk,plain,
! [A,B] :
( ( in(sk49(A),A)
| A = empty_set )
& ( ~ in(B,A)
| A != empty_set ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk49])],[f90_nnf]) ).
cnf(c335,plain,
( ~ in(X1,X0)
| X0 != empty_set ),
inference(cnf_transformation,[status(esa)],[f90_sk]) ).
fof(f94,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(f94_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)],[f94]) ).
fof(f94_sk,plain,
! [A,B] :
( ( ( set_meet(sk52(A)) = empty_set
& finite(sk52(A))
& subset(sk52(A),A)
& sk52(A) != empty_set )
| A = empty_set
| centered(A) )
& ( ( ( set_meet(B) != empty_set
| ~ finite(B)
| ~ subset(B,A)
| B = empty_set )
& A != empty_set )
| ~ centered(A) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk52])],[f94_nnf]) ).
cnf(c349,plain,
( X0 != empty_set
| ~ centered(X0) ),
inference(cnf_transformation,[status(esa)],[f94_sk]) ).
fof(f103,axiom,
! [A,B] :
( element(B,A)
=> ( proper_element(B,A)
<=> B != union(A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d2_tex_2) ).
fof(f103_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)],[f103]) ).
fof(f103_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)],[f103_nnf]) ).
cnf(c383,plain,
( X1 != union(X0)
| ~ proper_element(X1,X0)
| ~ element(X1,X0) ),
inference(cnf_transformation,[status(esa)],[f103_sk]) ).
fof(f126,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(f126_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)],[f126]) ).
fof(f126_sk,plain,
! [C,A,B,D] :
( ( ( ~ in(sk87(A,B,C),B)
& in(sk87(A,B,C),A)
& ~ in(sk87(A,B,C),C) )
| ( ( in(sk87(A,B,C),B)
| ~ in(sk87(A,B,C),A) )
& in(sk87(A,B,C),C) )
| C = set_difference(A,B) )
& ( ( ( in(D,B)
| ~ in(D,A)
| in(D,C) )
& ( ( ~ in(D,B)
& in(D,A) )
| ~ in(D,C) ) )
| C != set_difference(A,B) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk87])],[f126_nnf]) ).
cnf(c496,plain,
( ~ in(X3,X1)
| ~ in(X3,X2)
| X2 != set_difference(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f126_sk]) ).
fof(f154,axiom,
! [A,B] :
( proper_subset(A,B)
<=> ( A != B
& subset(A,B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d8_xboole_0) ).
fof(f154_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)],[f154]) ).
fof(f154_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)],[f154_nnf]) ).
cnf(c637,plain,
( X0 != X1
| ~ proper_subset(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f154_sk]) ).
fof(f267,axiom,
! [A] :
( finite(singleton(A))
& ~ empty(singleton(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_finset_1) ).
fof(f267_nnf,plain,
! [A] :
( finite(singleton(A))
& ~ empty(singleton(A)) ),
inference(nnf_transformation,[status(thm)],[f267]) ).
fof(f267_sk,plain,
! [A] :
( finite(singleton(A))
& ~ empty(singleton(A)) ),
inference(skolemisation,[status(esa)],[f267_nnf]) ).
cnf(c803,plain,
~ empty(singleton(X0)),
inference(cnf_transformation,[status(esa)],[f267_sk]) ).
fof(f268,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(f268_nnf,plain,
! [A] :
( preboolean(powerset(A))
& diff_closed(powerset(A))
& cup_closed(powerset(A))
& ~ empty(powerset(A)) ),
inference(nnf_transformation,[status(thm)],[f268]) ).
fof(f268_sk,plain,
! [A] :
( preboolean(powerset(A))
& diff_closed(powerset(A))
& cup_closed(powerset(A))
& ~ empty(powerset(A)) ),
inference(skolemisation,[status(esa)],[f268_nnf]) ).
cnf(c805,plain,
~ empty(powerset(X0)),
inference(cnf_transformation,[status(esa)],[f268_sk]) ).
fof(f270,axiom,
! [A] :
( strict_latt_str(boole_lattice(A))
& ~ empty_carrier(boole_lattice(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_lattice3) ).
fof(f270_nnf,plain,
! [A] :
( strict_latt_str(boole_lattice(A))
& ~ empty_carrier(boole_lattice(A)) ),
inference(nnf_transformation,[status(thm)],[f270]) ).
fof(f270_sk,plain,
! [A] :
( strict_latt_str(boole_lattice(A))
& ~ empty_carrier(boole_lattice(A)) ),
inference(skolemisation,[status(esa)],[f270_nnf]) ).
cnf(c811,plain,
~ empty_carrier(boole_lattice(X0)),
inference(cnf_transformation,[status(esa)],[f270_sk]) ).
fof(f272,axiom,
! [A] : ~ empty(succ(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_ordinal1) ).
fof(f272_nnf,plain,
! [A] : ~ empty(succ(A)),
inference(nnf_transformation,[status(thm)],[f272]) ).
fof(f272_sk,plain,
! [A] : ~ empty(succ(A)),
inference(skolemisation,[status(esa)],[f272_nnf]) ).
cnf(c815,plain,
~ empty(succ(X0)),
inference(cnf_transformation,[status(esa)],[f272_sk]) ).
fof(f273,axiom,
( ~ empty(omega)
& ordinal(omega)
& epsilon_connected(omega)
& epsilon_transitive(omega) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_ordinal2) ).
fof(f273_nnf,plain,
( ~ empty(omega)
& ordinal(omega)
& epsilon_connected(omega)
& epsilon_transitive(omega) ),
inference(nnf_transformation,[status(thm)],[f273]) ).
fof(f273_sk,plain,
( ~ empty(omega)
& ordinal(omega)
& epsilon_connected(omega)
& epsilon_transitive(omega) ),
inference(skolemisation,[status(esa)],[f273_nnf]) ).
cnf(c819,plain,
~ empty(omega),
inference(cnf_transformation,[status(esa)],[f273_sk]) ).
fof(f277,axiom,
! [A] : ~ empty(powerset(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_subset_1) ).
fof(f277_nnf,plain,
! [A] : ~ empty(powerset(A)),
inference(nnf_transformation,[status(thm)],[f277]) ).
fof(f277_sk,plain,
! [A] : ~ empty(powerset(A)),
inference(skolemisation,[status(esa)],[f277_nnf]) ).
cnf(c828,plain,
~ empty(powerset(X0)),
inference(cnf_transformation,[status(esa)],[f277_sk]) ).
fof(f279,axiom,
! [A,B] : ~ empty(ordered_pair(A,B)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_zfmisc_1) ).
fof(f279_nnf,plain,
! [A,B] : ~ empty(ordered_pair(A,B)),
inference(nnf_transformation,[status(thm)],[f279]) ).
fof(f279_sk,plain,
! [A,B] : ~ empty(ordered_pair(A,B)),
inference(skolemisation,[status(esa)],[f279_nnf]) ).
cnf(c830,plain,
~ empty(ordered_pair(X0,X1)),
inference(cnf_transformation,[status(esa)],[f279_sk]) ).
fof(f283,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(f283_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)],[f283]) ).
fof(f283_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)],[f283_nnf]) ).
cnf(c835,plain,
( ~ empty(succ(X0))
| ~ natural(X0)
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(esa)],[f283_sk]) ).
fof(f286,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(f286_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)],[f286]) ).
fof(f286_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)],[f286_nnf]) ).
cnf(c847,plain,
~ empty_carrier(boole_lattice(X0)),
inference(cnf_transformation,[status(esa)],[f286_sk]) ).
fof(f292,axiom,
! [A] : ~ empty(singleton(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc2_subset_1) ).
fof(f292_nnf,plain,
! [A] : ~ empty(singleton(A)),
inference(nnf_transformation,[status(thm)],[f292]) ).
fof(f292_sk,plain,
! [A] : ~ empty(singleton(A)),
inference(skolemisation,[status(esa)],[f292_nnf]) ).
cnf(c877,plain,
~ empty(singleton(X0)),
inference(cnf_transformation,[status(esa)],[f292_sk]) ).
fof(f309,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(f309_nnf,plain,
! [A] :
( ( ordinal(succ(A))
& epsilon_connected(succ(A))
& epsilon_transitive(succ(A))
& ~ empty(succ(A)) )
| ~ ordinal(A) ),
inference(nnf_transformation,[status(thm)],[f309]) ).
fof(f309_sk,plain,
! [A] :
( ( ordinal(succ(A))
& epsilon_connected(succ(A))
& epsilon_transitive(succ(A))
& ~ empty(succ(A)) )
| ~ ordinal(A) ),
inference(skolemisation,[status(esa)],[f309_nnf]) ).
cnf(c925,plain,
( ~ empty(succ(X0))
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(esa)],[f309_sk]) ).
fof(f311,axiom,
! [A,B] : ~ empty(unordered_pair(A,B)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc3_subset_1) ).
fof(f311_nnf,plain,
! [A,B] : ~ empty(unordered_pair(A,B)),
inference(nnf_transformation,[status(thm)],[f311]) ).
fof(f311_sk,plain,
! [A,B] : ~ empty(unordered_pair(A,B)),
inference(skolemisation,[status(esa)],[f311_nnf]) ).
cnf(c930,plain,
~ empty(unordered_pair(X0,X1)),
inference(cnf_transformation,[status(esa)],[f311_sk]) ).
fof(f346,axiom,
! [A,B] : ~ proper_subset(A,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',irreflexivity_r2_xboole_0) ).
fof(f346_nnf,plain,
! [A,B] : ~ proper_subset(A,A),
inference(nnf_transformation,[status(thm)],[f346]) ).
fof(f346_sk,plain,
! [A] : ~ proper_subset(A,A),
inference(skolemisation,[status(esa)],[f346_nnf]) ).
cnf(c1010,plain,
~ proper_subset(X0,X0),
inference(cnf_transformation,[status(esa)],[f346_sk]) ).
fof(f348,lemma,
! [A] : singleton(A) != empty_set,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l1_zfmisc_1) ).
fof(f348_nnf,plain,
! [A] : singleton(A) != empty_set,
inference(nnf_transformation,[status(thm)],[f348]) ).
fof(f348_sk,plain,
! [A] : singleton(A) != empty_set,
inference(skolemisation,[status(esa)],[f348_nnf]) ).
cnf(c1014,plain,
singleton(X0) != empty_set,
inference(cnf_transformation,[status(esa)],[f348_sk]) ).
fof(f350,lemma,
! [A,B] :
~ ( in(A,B)
& disjoint(singleton(A),B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l25_zfmisc_1) ).
fof(f350_nnf,plain,
! [A,B] :
( ~ in(A,B)
| ~ disjoint(singleton(A),B) ),
inference(nnf_transformation,[status(thm)],[f350]) ).
fof(f350_sk,plain,
! [A,B] :
( ~ in(A,B)
| ~ disjoint(singleton(A),B) ),
inference(skolemisation,[status(esa)],[f350_nnf]) ).
cnf(c1016,plain,
( ~ in(X0,X1)
| ~ disjoint(singleton(X0),X1) ),
inference(cnf_transformation,[status(esa)],[f350_sk]) ).
fof(f367,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(f367_nnf,plain,
? [A] :
( natural(A)
& ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A)
& ~ empty(A) ),
inference(nnf_transformation,[status(thm)],[f367]) ).
fof(f367_sk,plain,
( natural(sk149)
& ordinal(sk149)
& epsilon_connected(sk149)
& epsilon_transitive(sk149)
& ~ empty(sk149) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk149])],[f367_nnf]) ).
cnf(c1055,plain,
~ empty(sk149),
inference(cnf_transformation,[status(esa)],[f367_sk]) ).
fof(f368,axiom,
? [A] :
( finite(A)
& ~ empty(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc1_finset_1) ).
fof(f368_nnf,plain,
? [A] :
( finite(A)
& ~ empty(A) ),
inference(nnf_transformation,[status(thm)],[f368]) ).
fof(f368_sk,plain,
( finite(sk150)
& ~ empty(sk150) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk150])],[f368_nnf]) ).
cnf(c1060,plain,
~ empty(sk150),
inference(cnf_transformation,[status(esa)],[f368_sk]) ).
fof(f371,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(f371_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)],[f371]) ).
fof(f371_sk,plain,
( v5_membered(sk153)
& v4_membered(sk153)
& v3_membered(sk153)
& v2_membered(sk153)
& v1_membered(sk153)
& ~ empty(sk153) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk153])],[f371_nnf]) ).
cnf(c1068,plain,
~ empty(sk153),
inference(cnf_transformation,[status(esa)],[f371_sk]) ).
fof(f383,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(f383_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)],[f383]) ).
fof(f383_sk,plain,
( antisymmetric_relstr(sk165)
& transitive_relstr(sk165)
& reflexive_relstr(sk165)
& strict_rel_str(sk165)
& ~ empty_carrier(sk165)
& rel_str(sk165) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk165])],[f383_nnf]) ).
cnf(c1115,plain,
~ empty_carrier(sk165),
inference(cnf_transformation,[status(esa)],[f383_sk]) ).
fof(f386,axiom,
? [A] :
( relation(A)
& ~ empty(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc2_relat_1) ).
fof(f386_nnf,plain,
? [A] :
( relation(A)
& ~ empty(A) ),
inference(nnf_transformation,[status(thm)],[f386]) ).
fof(f386_sk,plain,
( relation(sk168)
& ~ empty(sk168) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk168])],[f386_nnf]) ).
cnf(c1130,plain,
~ empty(sk168),
inference(cnf_transformation,[status(esa)],[f386_sk]) ).
fof(f388,axiom,
! [A] :
? [B] :
( ~ proper_element(B,powerset(A))
& element(B,powerset(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc2_tex_2) ).
fof(f388_nnf,plain,
! [A] :
? [B] :
( ~ proper_element(B,powerset(A))
& element(B,powerset(A)) ),
inference(nnf_transformation,[status(thm)],[f388]) ).
fof(f388_sk,plain,
! [A] :
( ~ proper_element(sk170(A),powerset(A))
& element(sk170(A),powerset(A)) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk170])],[f388_nnf]) ).
cnf(c1135,plain,
~ proper_element(sk170(X0),powerset(X0)),
inference(cnf_transformation,[status(esa)],[f388_sk]) ).
fof(f390,axiom,
? [A] : ~ empty(A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc2_xboole_0) ).
fof(f390_nnf,plain,
? [A] : ~ empty(A),
inference(nnf_transformation,[status(thm)],[f390]) ).
fof(f390_sk,plain,
~ empty(sk172),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk172])],[f390_nnf]) ).
cnf(c1139,plain,
~ empty(sk172),
inference(cnf_transformation,[status(esa)],[f390_sk]) ).
fof(f394,axiom,
? [A] :
( ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A)
& ~ empty(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc3_ordinal1) ).
fof(f394_nnf,plain,
? [A] :
( ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A)
& ~ empty(A) ),
inference(nnf_transformation,[status(thm)],[f394]) ).
fof(f394_sk,plain,
( ordinal(sk176)
& epsilon_connected(sk176)
& epsilon_transitive(sk176)
& ~ empty(sk176) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk176])],[f394_nnf]) ).
cnf(c1148,plain,
~ empty(sk176),
inference(cnf_transformation,[status(esa)],[f394_sk]) ).
fof(f397,axiom,
? [A] :
( ~ empty_carrier(A)
& one_sorted_str(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc3_struct_0) ).
fof(f397_nnf,plain,
? [A] :
( ~ empty_carrier(A)
& one_sorted_str(A) ),
inference(nnf_transformation,[status(thm)],[f397]) ).
fof(f397_sk,plain,
( ~ empty_carrier(sk179)
& one_sorted_str(sk179) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk179])],[f397_nnf]) ).
cnf(c1162,plain,
~ empty_carrier(sk179),
inference(cnf_transformation,[status(esa)],[f397_sk]) ).
fof(f401,axiom,
? [A] :
( strict_latt_str(A)
& ~ empty_carrier(A)
& latt_str(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc6_lattices) ).
fof(f401_nnf,plain,
? [A] :
( strict_latt_str(A)
& ~ empty_carrier(A)
& latt_str(A) ),
inference(nnf_transformation,[status(thm)],[f401]) ).
fof(f401_sk,plain,
( strict_latt_str(sk183)
& ~ empty_carrier(sk183)
& latt_str(sk183) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk183])],[f401_nnf]) ).
cnf(c1172,plain,
~ empty_carrier(sk183),
inference(cnf_transformation,[status(esa)],[f401_sk]) ).
fof(f404,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(f404_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)],[f404]) ).
fof(f404_sk,plain,
( lattice(sk186)
& join_absorbing(sk186)
& meet_absorbing(sk186)
& meet_associative(sk186)
& meet_commutative(sk186)
& join_associative(sk186)
& join_commutative(sk186)
& strict_latt_str(sk186)
& ~ empty_carrier(sk186)
& latt_str(sk186) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk186])],[f404_nnf]) ).
cnf(c1180,plain,
~ empty_carrier(sk186),
inference(cnf_transformation,[status(esa)],[f404_sk]) ).
fof(f436,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(f436_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)],[f436]) ).
fof(f436_sk,plain,
! [B,E,G,I,K,L,N,P,D,R,T] :
( ( ( T = sk220(D,R)
| ~ subset(sk220(D,R),T)
| ~ in(T,R) )
& in(sk220(D,R),R) )
| R = empty_set
| ~ element(R,powerset(powerset(D)))
| ~ in(D,omega)
| ~ ordinal(D)
| ( ( ( sk219(P) != P
& subset(P,sk219(P))
& in(sk219(P),sk218) )
| ~ in(P,sk218) )
& sk218 != empty_set
& element(sk218,powerset(powerset(sk216)))
& in(sk216,omega)
& sk216 != empty_set
& ( ( ( N = sk217(K,L)
| ~ subset(sk217(K,L),N)
| ~ in(N,L) )
& in(sk217(K,L),L) )
| L = empty_set
| ~ element(L,powerset(powerset(K)))
| ~ in(K,omega)
| ~ in(K,sk216)
| ~ ordinal(K) )
& being_limit_ordinal(sk216)
& ordinal(sk216) )
| ( ( ( sk215(I) != I
& subset(I,sk215(I))
& in(sk215(I),sk214) )
| ~ in(I,sk214) )
& sk214 != empty_set
& element(sk214,powerset(powerset(succ(sk212))))
& in(succ(sk212),omega)
& ( ( ( G = sk213(E)
| ~ subset(sk213(E),G)
| ~ in(G,E) )
& in(sk213(E),E) )
| E = empty_set
| ~ element(E,powerset(powerset(sk212)))
| ~ in(sk212,omega) )
& ordinal(sk212) )
| ( ( ( sk211(B) != B
& subset(B,sk211(B))
& in(sk211(B),sk210) )
| ~ in(B,sk210) )
& sk210 != empty_set
& element(sk210,powerset(powerset(empty_set)))
& in(empty_set,omega) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk210,sk211,sk212,sk213,sk214,sk215,sk216,sk217,sk218,sk219,sk220])],[f436_nnf]) ).
cnf(c1418,plain,
( sk211(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])],[f436_sk]) ).
cnf(c1423,plain,
( sk210 != 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])],[f436_sk]) ).
cnf(c1432,plain,
( ~ subset(sk213(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])],[f436_sk]) ).
cnf(c1454,plain,
( sk215(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])],[f436_sk]) ).
cnf(c1459,plain,
( sk214 != 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])],[f436_sk]) ).
cnf(c1477,plain,
( ~ subset(sk217(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])],[f436_sk]) ).
cnf(c1508,plain,
( sk219(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])],[f436_sk]) ).
cnf(c1513,plain,
( sk218 != 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])],[f436_sk]) ).
cnf(c1522,plain,
( sk216 != 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])],[f436_sk]) ).
cnf(c1534,plain,
( ~ subset(sk220(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])],[f436_sk]) ).
fof(f596,lemma,
! [A,B,C] :
~ ( in(C,A)
& in(B,C)
& in(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t3_ordinal1) ).
fof(f596_nnf,plain,
! [A,B,C] :
( ~ in(C,A)
| ~ in(B,C)
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f596]) ).
fof(f596_sk,plain,
! [A,B,C] :
( ~ in(C,A)
| ~ in(B,C)
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f596_nnf]) ).
cnf(c3034,plain,
( ~ in(X2,X0)
| ~ in(X1,X2)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f596_sk]) ).
fof(f599,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(f599_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)],[f599]) ).
fof(f599_sk,plain,
! [A,B,C] :
( ( ~ disjoint(A,B)
| ~ in(C,B)
| ~ in(C,A) )
& ( ( in(sk451(A,B),B)
& in(sk451(A,B),A) )
| disjoint(A,B) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk451])],[f599_nnf]) ).
cnf(c3040,plain,
( ~ disjoint(X0,X1)
| ~ in(X2,X1)
| ~ in(X2,X0) ),
inference(cnf_transformation,[status(esa)],[f599_sk]) ).
fof(f603,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(f603_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)],[f603]) ).
fof(f603_sk,plain,
! [A,B] :
( ( ( ~ being_limit_ordinal(A)
| A != succ(B)
| ~ ordinal(B) )
& ( ( A = succ(sk453(A))
& ordinal(sk453(A)) )
| being_limit_ordinal(A) ) )
| ~ ordinal(A) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk453])],[f603_nnf]) ).
cnf(c3049,plain,
( ~ being_limit_ordinal(X0)
| X0 != succ(X1)
| ~ ordinal(X1)
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(esa)],[f603_sk]) ).
fof(f627,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(f627_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)],[f627]) ).
fof(f627_sk,plain,
! [A,B,C] :
( ( ~ disjoint(A,B)
| ~ in(C,set_intersection2(A,B)) )
& ( in(sk459(A,B),set_intersection2(A,B))
| disjoint(A,B) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk459])],[f627_nnf]) ).
cnf(c3093,plain,
( ~ disjoint(X0,X1)
| ~ in(X2,set_intersection2(X0,X1)) ),
inference(cnf_transformation,[status(esa)],[f627_sk]) ).
fof(f634,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(f634_nnf,plain,
! [A,B,C] :
( ~ in(B,C)
| ~ in(B,subset_complement(A,C))
| ~ element(C,powerset(A)) ),
inference(nnf_transformation,[status(thm)],[f634]) ).
fof(f634_sk,plain,
! [C,A,B] :
( ~ in(B,C)
| ~ in(B,subset_complement(A,C))
| ~ element(C,powerset(A)) ),
inference(skolemisation,[status(esa)],[f634_nnf]) ).
cnf(c3122,plain,
( ~ in(X1,X2)
| ~ in(X1,subset_complement(X0,X2))
| ~ element(X2,powerset(X0)) ),
inference(cnf_transformation,[status(esa)],[f634_sk]) ).
fof(f641,axiom,
! [A,B,C] :
~ ( empty(C)
& element(B,powerset(C))
& in(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_subset) ).
fof(f641_nnf,plain,
! [A,B,C] :
( ~ empty(C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f641]) ).
fof(f641_sk,plain,
! [A,B,C] :
( ~ empty(C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f641_nnf]) ).
cnf(c3132,plain,
( ~ empty(X2)
| ~ element(X1,powerset(X2))
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f641_sk]) ).
fof(f642,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(f642_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)],[f642]) ).
fof(f642_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)],[f642_nnf]) ).
cnf(c3133,plain,
( X1 != X0
| ~ proper_element(X1,powerset(X0))
| ~ element(X1,powerset(X0)) ),
inference(cnf_transformation,[status(esa)],[f642_sk]) ).
fof(f647,lemma,
! [A,B] :
~ ( proper_subset(B,A)
& subset(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t60_xboole_1) ).
fof(f647_nnf,plain,
! [A,B] :
( ~ proper_subset(B,A)
| ~ subset(A,B) ),
inference(nnf_transformation,[status(thm)],[f647]) ).
fof(f647_sk,plain,
! [A,B] :
( ~ proper_subset(B,A)
| ~ subset(A,B) ),
inference(skolemisation,[status(esa)],[f647_nnf]) ).
cnf(c3141,plain,
( ~ proper_subset(X1,X0)
| ~ subset(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f647_sk]) ).
fof(f652,lemma,
! [A,B] :
( set_difference(A,singleton(B)) = A
<=> ~ in(B,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t65_zfmisc_1) ).
fof(f652_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)],[f652]) ).
fof(f652_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)],[f652_nnf]) ).
cnf(c3148,plain,
( ~ in(X1,X0)
| set_difference(X0,singleton(X1)) != X0 ),
inference(cnf_transformation,[status(esa)],[f652_sk]) ).
fof(f664,axiom,
! [A,B] :
~ ( empty(B)
& in(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t7_boole) ).
fof(f664_nnf,plain,
! [A,B] :
( ~ empty(B)
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f664]) ).
fof(f664_sk,plain,
! [A,B] :
( ~ empty(B)
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f664_nnf]) ).
cnf(c3168,plain,
( ~ empty(X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f664_sk]) ).
fof(f667,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(f667_nnf,plain,
! [A,B] :
( ? [C] :
( ! [D] :
( ~ in(D,C)
| ~ in(D,B) )
& in(C,B) )
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f667]) ).
fof(f667_sk,plain,
! [A,B,D] :
( ( ( ~ in(D,sk465(A,B))
| ~ in(D,B) )
& in(sk465(A,B),B) )
| ~ in(A,B) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk465])],[f667_nnf]) ).
cnf(c3174,plain,
( ~ in(X3,sk465(X0,X1))
| ~ in(X3,X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f667_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c2,c3,c176,c317,c335,c349,c383,c496,c637,c803,c805,c811,c815,c819,c828,c830,c835,c847,c877,c925,c930,c1010,c1014,c1016,c1055,c1060,c1068,c1115,c1130,c1135,c1139,c1148,c1162,c1172,c1180,c1418,c1423,c1432,c1454,c1459,c1477,c1508,c1513,c1522,c1534,c3034,c3040,c3049,c3059,c3064,c3093,c3122,c3132,c3133,c3141,c3148,c3168,c3174]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t808]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU361+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.11/0.42 % Computer : n005.cluster.edu
% 0.11/0.42 % Model : x86_64 x86_64
% 0.11/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.42 % Memory : 8046.5625MB
% 0.11/0.42 % OS : Linux 6.8.0-71-generic
% 0.11/0.42 % CPULimit : 300
% 0.11/0.42 % WCLimit : 300
% 0.11/0.42 % DateTime : Thu Sep 24 13:50:17 UTC 2026
% 0.11/0.43 % CPUTime :
% 0.11/0.43 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 93.56/12.75 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 93.56/12.75 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------