%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SEU387+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n008.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:55 PM UTC 2026
% Result : Theorem 84.72s 11.38s
% Output : Proof 84.72s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 32
% Syntax : Number of formulae : 203 ( 109 unt; 0 def)
% Number of atoms : 723 ( 74 equ)
% Maximal formula atoms : 18 ( 3 avg)
% Number of connectives : 727 ( 207 ~; 80 |; 425 &)
% ( 1 <=>; 14 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 4 avg)
% Maximal term depth : 13 ( 2 avg)
% Number of predicates : 33 ( 31 usr; 1 prp; 0-2 aty)
% Number of functors : 25 ( 25 usr; 17 con; 0-4 aty)
% Number of variables : 190 ( 33 sgn 75 !; 29 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f84,axiom,
! [A] :
( ( rel_str(A)
& lower_bounded_relstr(A)
& antisymmetric_relstr(A)
& transitive_relstr(A)
& reflexive_relstr(A)
& ~ empty_carrier(A) )
=> ! [B] :
( ( element(B,powerset(the_carrier(A)))
& upper_relstr_subset(B,A)
& filtered_subset(B,A)
& ~ empty(B) )
=> ( proper_element(B,powerset(the_carrier(A)))
<=> ~ in(bottom_of_relstr(A),B) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t8_waybel_7) ).
fof(f84_nnf,plain,
! [A] :
( ! [B] :
( ( ( in(bottom_of_relstr(A),B)
| proper_element(B,powerset(the_carrier(A))) )
& ( ~ in(bottom_of_relstr(A),B)
| ~ proper_element(B,powerset(the_carrier(A))) ) )
| ~ element(B,powerset(the_carrier(A)))
| ~ upper_relstr_subset(B,A)
| ~ filtered_subset(B,A)
| empty(B) )
| ~ rel_str(A)
| ~ lower_bounded_relstr(A)
| ~ antisymmetric_relstr(A)
| ~ transitive_relstr(A)
| ~ reflexive_relstr(A)
| empty_carrier(A) ),
inference(nnf_transformation,[status(thm)],[f84]) ).
fof(f84_sk,plain,
! [A,B] :
( ( ( in(bottom_of_relstr(A),B)
| proper_element(B,powerset(the_carrier(A))) )
& ( ~ in(bottom_of_relstr(A),B)
| ~ proper_element(B,powerset(the_carrier(A))) ) )
| ~ element(B,powerset(the_carrier(A)))
| ~ upper_relstr_subset(B,A)
| ~ filtered_subset(B,A)
| empty(B)
| ~ rel_str(A)
| ~ lower_bounded_relstr(A)
| ~ antisymmetric_relstr(A)
| ~ transitive_relstr(A)
| ~ reflexive_relstr(A)
| empty_carrier(A) ),
inference(skolemisation,[status(esa)],[f84_nnf]) ).
cnf(c290,plain,
( ~ in(bottom_of_relstr(X0),X1)
| ~ proper_element(X1,powerset(the_carrier(X0)))
| ~ element(X1,powerset(the_carrier(X0)))
| ~ upper_relstr_subset(X1,X0)
| ~ filtered_subset(X1,X0)
| empty(X1)
| ~ rel_str(X0)
| ~ lower_bounded_relstr(X0)
| ~ antisymmetric_relstr(X0)
| ~ transitive_relstr(X0)
| ~ reflexive_relstr(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(esa)],[f84_sk]) ).
cnf(t228,plain,
ifeq(reflexive_relstr(X1),true,ifeq(transitive_relstr(X1),true,ifeq(antisymmetric_relstr(X1),true,ifeq(lower_bounded_relstr(X1),true,ifeq(rel_str(X1),true,ifeq(filtered_subset(X2,X1),true,ifeq(upper_relstr_subset(X2,X1),true,ifeq(element(X2,powerset(the_carrier(X1))),true,ifeq(proper_element(X2,powerset(the_carrier(X1))),true,ifeq(in(bottom_of_relstr(X1),X2),true,or(empty_carrier(X1),empty(X2)),true),true),true),true),true),true),true),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c290]) ).
cnf(t289,plain,
ifeq(reflexive_relstr(X1),true,ifeq(transitive_relstr(X1),true,ifeq(antisymmetric_relstr(X1),true,ifeq(lower_bounded_relstr(X1),true,ifeq(rel_str(X1),true,ifeq(filtered_subset(X2,X1),true,ifeq(upper_relstr_subset(X2,X1),true,ifeq(element(X2,powerset(the_carrier(X1))),true,ifeq(proper_element(X2,powerset(the_carrier(X1))),true,ifeq(in(bottom_of_relstr(X1),X2),true,or(empty_carrier(X1),empty(X2)),true),true),true),true),true),true),true),true),true),true) = true,
inference(orient,[status(thm)],[t228]) ).
fof(f25,axiom,
! [A] :
( rel_str(boole_POSet(A))
& strict_rel_str(boole_POSet(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k3_yellow_1) ).
fof(f25_nnf,plain,
! [A] :
( rel_str(boole_POSet(A))
& strict_rel_str(boole_POSet(A)) ),
inference(nnf_transformation,[status(thm)],[f25]) ).
fof(f25_sk,plain,
! [A] :
( rel_str(boole_POSet(A))
& strict_rel_str(boole_POSet(A)) ),
inference(skolemisation,[status(esa)],[f25_nnf]) ).
cnf(c61,plain,
rel_str(boole_POSet(X0)),
inference(cnf_transformation,[status(esa)],[f25_sk]) ).
cnf(t76,plain,
rel_str(boole_POSet(X1)) = true,
inference(equality_encoding,[status(esa)],[c61]) ).
cnf(t336,plain,
rel_str(boole_POSet(X1)) = true,
inference(orient,[status(thm)],[t76]) ).
cnf(t356,plain,
true = ifeq(reflexive_relstr(boole_POSet(X1)),true,ifeq(transitive_relstr(boole_POSet(X1)),true,ifeq(antisymmetric_relstr(boole_POSet(X1)),true,ifeq(lower_bounded_relstr(boole_POSet(X1)),true,ifeq(true,true,ifeq(filtered_subset(X2,boole_POSet(X1)),true,ifeq(upper_relstr_subset(X2,boole_POSet(X1)),true,ifeq(element(X2,powerset(the_carrier(boole_POSet(X1)))),true,ifeq(proper_element(X2,powerset(the_carrier(boole_POSet(X1)))),true,ifeq(in(bottom_of_relstr(boole_POSet(X1)),X2),true,or(empty_carrier(boole_POSet(X1)),empty(X2)),true),true),true),true),true),true),true),true),true),true),
inference(cp,[status(thm)],[t289,t336]) ).
fof(f42,axiom,
! [A] :
( complete_relstr(boole_POSet(A))
& with_infima_relstr(boole_POSet(A))
& with_suprema_relstr(boole_POSet(A))
& boolean_relstr(boole_POSet(A))
& complemented_relstr(boole_POSet(A))
& heyting_relstr(boole_POSet(A))
& distributive_relstr(boole_POSet(A))
& ~ v1_yellow_3(boole_POSet(A))
& join_complete_relstr(boole_POSet(A))
& up_complete_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',fc1_waybel_7) ).
fof(f42_nnf,plain,
! [A] :
( complete_relstr(boole_POSet(A))
& with_infima_relstr(boole_POSet(A))
& with_suprema_relstr(boole_POSet(A))
& boolean_relstr(boole_POSet(A))
& complemented_relstr(boole_POSet(A))
& heyting_relstr(boole_POSet(A))
& distributive_relstr(boole_POSet(A))
& ~ v1_yellow_3(boole_POSet(A))
& join_complete_relstr(boole_POSet(A))
& up_complete_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)],[f42]) ).
fof(f42_sk,plain,
! [A] :
( complete_relstr(boole_POSet(A))
& with_infima_relstr(boole_POSet(A))
& with_suprema_relstr(boole_POSet(A))
& boolean_relstr(boole_POSet(A))
& complemented_relstr(boole_POSet(A))
& heyting_relstr(boole_POSet(A))
& distributive_relstr(boole_POSet(A))
& ~ v1_yellow_3(boole_POSet(A))
& join_complete_relstr(boole_POSet(A))
& up_complete_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)],[f42_nnf]) ).
cnf(c82,plain,
reflexive_relstr(boole_POSet(X0)),
inference(cnf_transformation,[status(esa)],[f42_sk]) ).
cnf(t72,plain,
reflexive_relstr(boole_POSet(X1)) = true,
inference(equality_encoding,[status(esa)],[c82]) ).
cnf(t489,plain,
reflexive_relstr(boole_POSet(X1)) = true,
inference(orient,[status(thm)],[t72]) ).
cnf(t1558,plain,
true = ifeq(true,true,ifeq(transitive_relstr(boole_POSet(X1)),true,ifeq(antisymmetric_relstr(boole_POSet(X1)),true,ifeq(lower_bounded_relstr(boole_POSet(X1)),true,ifeq(true,true,ifeq(filtered_subset(X2,boole_POSet(X1)),true,ifeq(upper_relstr_subset(X2,boole_POSet(X1)),true,ifeq(element(X2,powerset(the_carrier(boole_POSet(X1)))),true,ifeq(proper_element(X2,powerset(the_carrier(boole_POSet(X1)))),true,ifeq(in(bottom_of_relstr(boole_POSet(X1)),X2),true,or(empty_carrier(boole_POSet(X1)),empty(X2)),true),true),true),true),true),true),true),true),true),true),
inference(step,[status(thm)],[t356,t489]) ).
cnf(t96,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t231,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t96]) ).
cnf(t1559,plain,
true = ifeq(transitive_relstr(boole_POSet(X1)),true,ifeq(antisymmetric_relstr(boole_POSet(X1)),true,ifeq(lower_bounded_relstr(boole_POSet(X1)),true,ifeq(true,true,ifeq(filtered_subset(X2,boole_POSet(X1)),true,ifeq(upper_relstr_subset(X2,boole_POSet(X1)),true,ifeq(element(X2,powerset(the_carrier(boole_POSet(X1)))),true,ifeq(proper_element(X2,powerset(the_carrier(boole_POSet(X1)))),true,ifeq(in(bottom_of_relstr(boole_POSet(X1)),X2),true,or(empty_carrier(boole_POSet(X1)),empty(X2)),true),true),true),true),true),true),true),true),true),
inference(step,[status(thm)],[t1558,t231]) ).
cnf(c83,plain,
transitive_relstr(boole_POSet(X0)),
inference(cnf_transformation,[status(esa)],[f42_sk]) ).
cnf(t78,plain,
transitive_relstr(boole_POSet(X1)) = true,
inference(equality_encoding,[status(esa)],[c83]) ).
cnf(t550,plain,
transitive_relstr(boole_POSet(X1)) = true,
inference(orient,[status(thm)],[t78]) ).
cnf(t1560,plain,
true = ifeq(true,true,ifeq(antisymmetric_relstr(boole_POSet(X1)),true,ifeq(lower_bounded_relstr(boole_POSet(X1)),true,ifeq(true,true,ifeq(filtered_subset(X2,boole_POSet(X1)),true,ifeq(upper_relstr_subset(X2,boole_POSet(X1)),true,ifeq(element(X2,powerset(the_carrier(boole_POSet(X1)))),true,ifeq(proper_element(X2,powerset(the_carrier(boole_POSet(X1)))),true,ifeq(in(bottom_of_relstr(boole_POSet(X1)),X2),true,or(empty_carrier(boole_POSet(X1)),empty(X2)),true),true),true),true),true),true),true),true),true),
inference(step,[status(thm)],[t1559,t550]) ).
cnf(t1561,plain,
true = ifeq(antisymmetric_relstr(boole_POSet(X1)),true,ifeq(lower_bounded_relstr(boole_POSet(X1)),true,ifeq(true,true,ifeq(filtered_subset(X2,boole_POSet(X1)),true,ifeq(upper_relstr_subset(X2,boole_POSet(X1)),true,ifeq(element(X2,powerset(the_carrier(boole_POSet(X1)))),true,ifeq(proper_element(X2,powerset(the_carrier(boole_POSet(X1)))),true,ifeq(in(bottom_of_relstr(boole_POSet(X1)),X2),true,or(empty_carrier(boole_POSet(X1)),empty(X2)),true),true),true),true),true),true),true),true),
inference(step,[status(thm)],[t1560,t231]) ).
cnf(c84,plain,
antisymmetric_relstr(boole_POSet(X0)),
inference(cnf_transformation,[status(esa)],[f42_sk]) ).
cnf(t38,plain,
antisymmetric_relstr(boole_POSet(X1)) = true,
inference(equality_encoding,[status(esa)],[c84]) ).
cnf(t571,plain,
antisymmetric_relstr(boole_POSet(X1)) = true,
inference(orient,[status(thm)],[t38]) ).
cnf(t1562,plain,
true = ifeq(true,true,ifeq(lower_bounded_relstr(boole_POSet(X1)),true,ifeq(true,true,ifeq(filtered_subset(X2,boole_POSet(X1)),true,ifeq(upper_relstr_subset(X2,boole_POSet(X1)),true,ifeq(element(X2,powerset(the_carrier(boole_POSet(X1)))),true,ifeq(proper_element(X2,powerset(the_carrier(boole_POSet(X1)))),true,ifeq(in(bottom_of_relstr(boole_POSet(X1)),X2),true,or(empty_carrier(boole_POSet(X1)),empty(X2)),true),true),true),true),true),true),true),true),
inference(step,[status(thm)],[t1561,t571]) ).
cnf(t1563,plain,
true = ifeq(lower_bounded_relstr(boole_POSet(X1)),true,ifeq(true,true,ifeq(filtered_subset(X2,boole_POSet(X1)),true,ifeq(upper_relstr_subset(X2,boole_POSet(X1)),true,ifeq(element(X2,powerset(the_carrier(boole_POSet(X1)))),true,ifeq(proper_element(X2,powerset(the_carrier(boole_POSet(X1)))),true,ifeq(in(bottom_of_relstr(boole_POSet(X1)),X2),true,or(empty_carrier(boole_POSet(X1)),empty(X2)),true),true),true),true),true),true),true),
inference(step,[status(thm)],[t1562,t231]) ).
cnf(c85,plain,
lower_bounded_relstr(boole_POSet(X0)),
inference(cnf_transformation,[status(esa)],[f42_sk]) ).
cnf(t56,plain,
lower_bounded_relstr(boole_POSet(X1)) = true,
inference(equality_encoding,[status(esa)],[c85]) ).
cnf(t402,plain,
lower_bounded_relstr(boole_POSet(X1)) = true,
inference(orient,[status(thm)],[t56]) ).
cnf(t1564,plain,
true = ifeq(true,true,ifeq(true,true,ifeq(filtered_subset(X2,boole_POSet(X1)),true,ifeq(upper_relstr_subset(X2,boole_POSet(X1)),true,ifeq(element(X2,powerset(the_carrier(boole_POSet(X1)))),true,ifeq(proper_element(X2,powerset(the_carrier(boole_POSet(X1)))),true,ifeq(in(bottom_of_relstr(boole_POSet(X1)),X2),true,or(empty_carrier(boole_POSet(X1)),empty(X2)),true),true),true),true),true),true),true),
inference(step,[status(thm)],[t1563,t402]) ).
cnf(t1565,plain,
true = ifeq(true,true,ifeq(filtered_subset(X2,boole_POSet(X1)),true,ifeq(upper_relstr_subset(X2,boole_POSet(X1)),true,ifeq(element(X2,powerset(the_carrier(boole_POSet(X1)))),true,ifeq(proper_element(X2,powerset(the_carrier(boole_POSet(X1)))),true,ifeq(in(bottom_of_relstr(boole_POSet(X1)),X2),true,or(empty_carrier(boole_POSet(X1)),empty(X2)),true),true),true),true),true),true),
inference(step,[status(thm)],[t1564,t231]) ).
cnf(t1566,plain,
true = ifeq(filtered_subset(X2,boole_POSet(X1)),true,ifeq(upper_relstr_subset(X2,boole_POSet(X1)),true,ifeq(element(X2,powerset(the_carrier(boole_POSet(X1)))),true,ifeq(proper_element(X2,powerset(the_carrier(boole_POSet(X1)))),true,ifeq(in(bottom_of_relstr(boole_POSet(X1)),X2),true,or(empty_carrier(boole_POSet(X1)),empty(X2)),true),true),true),true),true),
inference(step,[status(thm)],[t1565,t231]) ).
fof(f74,axiom,
! [A] : bottom_of_relstr(boole_POSet(A)) = empty_set,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t18_yellow_1) ).
fof(f74_nnf,plain,
! [A] : bottom_of_relstr(boole_POSet(A)) = empty_set,
inference(nnf_transformation,[status(thm)],[f74]) ).
fof(f74_sk,plain,
! [A] : bottom_of_relstr(boole_POSet(A)) = empty_set,
inference(skolemisation,[status(esa)],[f74_nnf]) ).
cnf(c272,plain,
bottom_of_relstr(boole_POSet(X0)) = empty_set,
inference(cnf_transformation,[status(esa)],[f74_sk]) ).
cnf(t42,plain,
bottom_of_relstr(boole_POSet(X1)) = empty_set,
inference(equality_encoding,[status(esa)],[c272]) ).
fof(f83,axiom,
! [A,B] :
~ ( empty(B)
& A != B
& empty(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t8_boole) ).
fof(f83_nnf,plain,
! [A,B] :
( ~ empty(B)
| A = B
| ~ empty(A) ),
inference(nnf_transformation,[status(thm)],[f83]) ).
fof(f83_sk,plain,
! [A,B] :
( ~ empty(B)
| A = B
| ~ empty(A) ),
inference(skolemisation,[status(esa)],[f83_nnf]) ).
cnf(c289,plain,
( ~ empty(X1)
| X0 = X1
| ~ empty(X0) ),
inference(cnf_transformation,[status(esa)],[f83_sk]) ).
cnf(hi227,axiom,
ifeq(empty(X0),true,ifeq(empty(X1),true,X0,X1),X1) = X1,
inference(equality_encoding,[status(esa)],[c289]) ).
fof(f44,axiom,
( relation(empty_set)
& empty(empty_set) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc4_relat_1) ).
fof(f44_nnf,plain,
( relation(empty_set)
& empty(empty_set) ),
inference(nnf_transformation,[status(thm)],[f44]) ).
fof(f44_sk,plain,
( relation(empty_set)
& empty(empty_set) ),
inference(skolemisation,[status(esa)],[f44_nnf]) ).
cnf(c117,plain,
empty(empty_set),
inference(cnf_transformation,[status(esa)],[f44_sk]) ).
cnf(hi78,axiom,
empty(empty_set) = true,
inference(equality_encoding,[status(esa)],[c117]) ).
fof(f77,conjecture,
! [A] :
( ~ empty(A)
=> ! [B] :
( ( element(B,powerset(the_carrier(boole_POSet(A))))
& proper_element(B,powerset(the_carrier(boole_POSet(A))))
& upper_relstr_subset(B,boole_POSet(A))
& filtered_subset(B,boole_POSet(A))
& ~ empty(B) )
=> ! [C] :
~ ( empty(C)
& in(C,B) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2_yellow19) ).
fof(f77_neg,negated_conjecture,
~ ! [A] :
( ~ empty(A)
=> ! [B] :
( ( element(B,powerset(the_carrier(boole_POSet(A))))
& proper_element(B,powerset(the_carrier(boole_POSet(A))))
& upper_relstr_subset(B,boole_POSet(A))
& filtered_subset(B,boole_POSet(A))
& ~ empty(B) )
=> ! [C] :
~ ( empty(C)
& in(C,B) ) ) ),
inference(negated_conjecture,[status(cth)],[f77]) ).
fof(f77_nnf,plain,
? [A] :
( ? [B] :
( ? [C] :
( empty(C)
& in(C,B) )
& element(B,powerset(the_carrier(boole_POSet(A))))
& proper_element(B,powerset(the_carrier(boole_POSet(A))))
& upper_relstr_subset(B,boole_POSet(A))
& filtered_subset(B,boole_POSet(A))
& ~ empty(B) )
& ~ empty(A) ),
inference(nnf_transformation,[status(thm)],[f77_neg]) ).
fof(f77_sk,plain,
( empty(sk29)
& in(sk29,sk28)
& element(sk28,powerset(the_carrier(boole_POSet(sk27))))
& proper_element(sk28,powerset(the_carrier(boole_POSet(sk27))))
& upper_relstr_subset(sk28,boole_POSet(sk27))
& filtered_subset(sk28,boole_POSet(sk27))
& ~ empty(sk28)
& ~ empty(sk27) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk27,sk28,sk29])],[f77_nnf]) ).
cnf(c282,plain,
empty(sk29),
inference(cnf_transformation,[status(esa)],[f77_sk]) ).
cnf(hi222,negated_conjecture,
empty(sk29) = true,
inference(equality_encoding,[status(esa)],[c282]) ).
cnf(t0,plain,
sk29 = empty_set,
inference(hyper_resolution,[status(thm)],[hi227,hi78,hi222]) ).
cnf(t732,plain,
empty_set = sk29,
inference(orient,[status(thm)],[t0]) ).
cnf(t1305,plain,
bottom_of_relstr(boole_POSet(X1)) = sk29,
inference(step,[status(thm)],[t42,t732]) ).
cnf(t734,plain,
bottom_of_relstr(boole_POSet(X1)) = sk29,
inference(orient,[status(thm)],[t1305]) ).
cnf(t1567,plain,
true = ifeq(filtered_subset(X2,boole_POSet(X1)),true,ifeq(upper_relstr_subset(X2,boole_POSet(X1)),true,ifeq(element(X2,powerset(the_carrier(boole_POSet(X1)))),true,ifeq(proper_element(X2,powerset(the_carrier(boole_POSet(X1)))),true,ifeq(in(sk29,X2),true,or(empty_carrier(boole_POSet(X1)),empty(X2)),true),true),true),true),true),
inference(step,[status(thm)],[t1566,t734]) ).
cnf(c80,plain,
~ empty_carrier(boole_POSet(X0)),
inference(cnf_transformation,[status(esa)],[f42_sk]) ).
cnf(t51,plain,
empty_carrier(boole_POSet(X1)) = false,
inference(equality_encoding,[status(esa)],[c80]) ).
cnf(t650,plain,
empty_carrier(boole_POSet(X1)) = false,
inference(orient,[status(thm)],[t51]) ).
cnf(t1568,plain,
true = ifeq(filtered_subset(X2,boole_POSet(X1)),true,ifeq(upper_relstr_subset(X2,boole_POSet(X1)),true,ifeq(element(X2,powerset(the_carrier(boole_POSet(X1)))),true,ifeq(proper_element(X2,powerset(the_carrier(boole_POSet(X1)))),true,ifeq(in(sk29,X2),true,or(false,empty(X2)),true),true),true),true),true),
inference(step,[status(thm)],[t1567,t650]) ).
cnf(t62,plain,
or(false,X1) = X1,
introduced(definition) ).
cnf(t230,plain,
or(false,X1) = X1,
inference(orient,[status(thm)],[t62]) ).
cnf(t1569,plain,
true = ifeq(filtered_subset(X2,boole_POSet(X1)),true,ifeq(upper_relstr_subset(X2,boole_POSet(X1)),true,ifeq(element(X2,powerset(the_carrier(boole_POSet(X1)))),true,ifeq(proper_element(X2,powerset(the_carrier(boole_POSet(X1)))),true,ifeq(in(sk29,X2),true,empty(X2),true),true),true),true),true),
inference(step,[status(thm)],[t1568,t230]) ).
cnf(t1197,plain,
ifeq(filtered_subset(X1,boole_POSet(X2)),true,ifeq(upper_relstr_subset(X1,boole_POSet(X2)),true,ifeq(element(X1,powerset(the_carrier(boole_POSet(X2)))),true,ifeq(proper_element(X1,powerset(the_carrier(boole_POSet(X2)))),true,ifeq(in(sk29,X1),true,empty(X1),true),true),true),true),true) = true,
inference(orient,[status(thm)],[t1569]) ).
cnf(c277,plain,
filtered_subset(sk28,boole_POSet(sk27)),
inference(cnf_transformation,[status(esa)],[f77_sk]) ).
cnf(t93,plain,
filtered_subset(sk28,boole_POSet(sk27)) = true,
inference(equality_encoding,[status(esa)],[c277]) ).
cnf(t643,plain,
filtered_subset(sk28,boole_POSet(sk27)) = true,
inference(orient,[status(thm)],[t93]) ).
cnf(t1198,plain,
true = ifeq(true,true,ifeq(upper_relstr_subset(sk28,boole_POSet(sk27)),true,ifeq(element(sk28,powerset(the_carrier(boole_POSet(sk27)))),true,ifeq(proper_element(sk28,powerset(the_carrier(boole_POSet(sk27)))),true,ifeq(in(sk29,sk28),true,empty(sk28),true),true),true),true),true),
inference(cp,[status(thm)],[t1197,t643]) ).
cnf(t1570,plain,
true = ifeq(upper_relstr_subset(sk28,boole_POSet(sk27)),true,ifeq(element(sk28,powerset(the_carrier(boole_POSet(sk27)))),true,ifeq(proper_element(sk28,powerset(the_carrier(boole_POSet(sk27)))),true,ifeq(in(sk29,sk28),true,empty(sk28),true),true),true),true),
inference(step,[status(thm)],[t1198,t231]) ).
cnf(c278,plain,
upper_relstr_subset(sk28,boole_POSet(sk27)),
inference(cnf_transformation,[status(esa)],[f77_sk]) ).
cnf(t94,plain,
upper_relstr_subset(sk28,boole_POSet(sk27)) = true,
inference(equality_encoding,[status(esa)],[c278]) ).
cnf(t640,plain,
upper_relstr_subset(sk28,boole_POSet(sk27)) = true,
inference(orient,[status(thm)],[t94]) ).
cnf(t1571,plain,
true = ifeq(true,true,ifeq(element(sk28,powerset(the_carrier(boole_POSet(sk27)))),true,ifeq(proper_element(sk28,powerset(the_carrier(boole_POSet(sk27)))),true,ifeq(in(sk29,sk28),true,empty(sk28),true),true),true),true),
inference(step,[status(thm)],[t1570,t640]) ).
cnf(t1572,plain,
true = ifeq(element(sk28,powerset(the_carrier(boole_POSet(sk27)))),true,ifeq(proper_element(sk28,powerset(the_carrier(boole_POSet(sk27)))),true,ifeq(in(sk29,sk28),true,empty(sk28),true),true),true),
inference(step,[status(thm)],[t1571,t231]) ).
cnf(c280,plain,
element(sk28,powerset(the_carrier(boole_POSet(sk27)))),
inference(cnf_transformation,[status(esa)],[f77_sk]) ).
cnf(t153,plain,
element(sk28,powerset(the_carrier(boole_POSet(sk27)))) = true,
inference(equality_encoding,[status(esa)],[c280]) ).
cnf(t622,plain,
element(sk28,powerset(the_carrier(boole_POSet(sk27)))) = true,
inference(orient,[status(thm)],[t153]) ).
cnf(t1573,plain,
true = ifeq(true,true,ifeq(proper_element(sk28,powerset(the_carrier(boole_POSet(sk27)))),true,ifeq(in(sk29,sk28),true,empty(sk28),true),true),true),
inference(step,[status(thm)],[t1572,t622]) ).
cnf(t1574,plain,
true = ifeq(proper_element(sk28,powerset(the_carrier(boole_POSet(sk27)))),true,ifeq(in(sk29,sk28),true,empty(sk28),true),true),
inference(step,[status(thm)],[t1573,t231]) ).
cnf(c279,plain,
proper_element(sk28,powerset(the_carrier(boole_POSet(sk27)))),
inference(cnf_transformation,[status(esa)],[f77_sk]) ).
cnf(t171,plain,
proper_element(sk28,powerset(the_carrier(boole_POSet(sk27)))) = true,
inference(equality_encoding,[status(esa)],[c279]) ).
cnf(t646,plain,
proper_element(sk28,powerset(the_carrier(boole_POSet(sk27)))) = true,
inference(orient,[status(thm)],[t171]) ).
cnf(t1575,plain,
true = ifeq(true,true,ifeq(in(sk29,sk28),true,empty(sk28),true),true),
inference(step,[status(thm)],[t1574,t646]) ).
cnf(t1576,plain,
true = ifeq(in(sk29,sk28),true,empty(sk28),true),
inference(step,[status(thm)],[t1575,t231]) ).
cnf(c281,plain,
in(sk29,sk28),
inference(cnf_transformation,[status(esa)],[f77_sk]) ).
cnf(t55,plain,
in(sk29,sk28) = true,
inference(equality_encoding,[status(esa)],[c281]) ).
cnf(t603,plain,
in(sk29,sk28) = true,
inference(orient,[status(thm)],[t55]) ).
cnf(t1577,plain,
true = ifeq(true,true,empty(sk28),true),
inference(step,[status(thm)],[t1576,t603]) ).
cnf(t1578,plain,
true = empty(sk28),
inference(step,[status(thm)],[t1577,t231]) ).
cnf(c276,plain,
~ empty(sk28),
inference(cnf_transformation,[status(esa)],[f77_sk]) ).
cnf(t11,plain,
empty(sk28) = false,
inference(equality_encoding,[status(esa)],[c276]) ).
cnf(t695,plain,
empty(sk28) = false,
inference(orient,[status(thm)],[t11]) ).
cnf(t1579,plain,
true = false,
inference(step,[status(thm)],[t1578,t695]) ).
cnf(t1209,plain,
false = true,
inference(orient,[status(thm)],[t1579]) ).
fof(f1,axiom,
! [A,B] :
( in(A,B)
=> ~ in(B,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',antisymmetry_r2_hidden) ).
fof(f1_nnf,plain,
! [A,B] :
( ~ in(B,A)
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [A,B] :
( ~ in(B,A)
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
( ~ in(X1,X0)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
fof(f8,axiom,
! [A] :
( rel_str(A)
=> ( with_suprema_relstr(A)
=> ~ empty_carrier(A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc1_lattice3) ).
fof(f8_nnf,plain,
! [A] :
( ~ empty_carrier(A)
| ~ with_suprema_relstr(A)
| ~ rel_str(A) ),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [A] :
( ~ empty_carrier(A)
| ~ with_suprema_relstr(A)
| ~ rel_str(A) ),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c29,plain,
( ~ empty_carrier(X0)
| ~ with_suprema_relstr(X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
fof(f13,axiom,
! [A] :
( rel_str(A)
=> ( with_infima_relstr(A)
=> ~ empty_carrier(A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc2_lattice3) ).
fof(f13_nnf,plain,
! [A] :
( ~ empty_carrier(A)
| ~ with_infima_relstr(A)
| ~ rel_str(A) ),
inference(nnf_transformation,[status(thm)],[f13]) ).
fof(f13_sk,plain,
! [A] :
( ~ empty_carrier(A)
| ~ with_infima_relstr(A)
| ~ rel_str(A) ),
inference(skolemisation,[status(esa)],[f13_nnf]) ).
cnf(c36,plain,
( ~ empty_carrier(X0)
| ~ with_infima_relstr(X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
fof(f19,axiom,
! [A] :
( rel_str(A)
=> ( ( up_complete_relstr(A)
& with_suprema_relstr(A)
& reflexive_relstr(A) )
=> ( upper_bounded_relstr(A)
& with_suprema_relstr(A)
& reflexive_relstr(A)
& ~ empty_carrier(A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc9_waybel_0) ).
fof(f19_nnf,plain,
! [A] :
( ( upper_bounded_relstr(A)
& with_suprema_relstr(A)
& reflexive_relstr(A)
& ~ empty_carrier(A) )
| ~ up_complete_relstr(A)
| ~ with_suprema_relstr(A)
| ~ reflexive_relstr(A)
| ~ rel_str(A) ),
inference(nnf_transformation,[status(thm)],[f19]) ).
fof(f19_sk,plain,
! [A] :
( ( upper_bounded_relstr(A)
& with_suprema_relstr(A)
& reflexive_relstr(A)
& ~ empty_carrier(A) )
| ~ up_complete_relstr(A)
| ~ with_suprema_relstr(A)
| ~ reflexive_relstr(A)
| ~ rel_str(A) ),
inference(skolemisation,[status(esa)],[f19_nnf]) ).
cnf(c50,plain,
( ~ empty_carrier(X0)
| ~ up_complete_relstr(X0)
| ~ with_suprema_relstr(X0)
| ~ reflexive_relstr(X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
fof(f41,axiom,
! [A] : ~ empty(powerset(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_subset_1) ).
fof(f41_nnf,plain,
! [A] : ~ empty(powerset(A)),
inference(nnf_transformation,[status(thm)],[f41]) ).
fof(f41_sk,plain,
! [A] : ~ empty(powerset(A)),
inference(skolemisation,[status(esa)],[f41_nnf]) ).
cnf(c79,plain,
~ empty(powerset(X0)),
inference(cnf_transformation,[status(esa)],[f41_sk]) ).
cnf(c90,plain,
~ v1_yellow_3(boole_POSet(X0)),
inference(cnf_transformation,[status(esa)],[f42_sk]) ).
fof(f46,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(f46_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)],[f46]) ).
fof(f46_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)],[f46_nnf]) ).
cnf(c120,plain,
~ empty_carrier(boole_POSet(X0)),
inference(cnf_transformation,[status(esa)],[f46_sk]) ).
fof(f47,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(f47_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)],[f47]) ).
fof(f47_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)],[f47_nnf]) ).
cnf(c125,plain,
~ empty_carrier(boole_POSet(X0)),
inference(cnf_transformation,[status(esa)],[f47_sk]) ).
fof(f48,axiom,
! [A] :
( complete_relstr(boole_POSet(A))
& with_infima_relstr(boole_POSet(A))
& with_suprema_relstr(boole_POSet(A))
& ~ v1_yellow_3(boole_POSet(A))
& join_complete_relstr(boole_POSet(A))
& up_complete_relstr(boole_POSet(A))
& directed_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_6) ).
fof(f48_nnf,plain,
! [A] :
( complete_relstr(boole_POSet(A))
& with_infima_relstr(boole_POSet(A))
& with_suprema_relstr(boole_POSet(A))
& ~ v1_yellow_3(boole_POSet(A))
& join_complete_relstr(boole_POSet(A))
& up_complete_relstr(boole_POSet(A))
& directed_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)],[f48]) ).
fof(f48_sk,plain,
! [A] :
( complete_relstr(boole_POSet(A))
& with_infima_relstr(boole_POSet(A))
& with_suprema_relstr(boole_POSet(A))
& ~ v1_yellow_3(boole_POSet(A))
& join_complete_relstr(boole_POSet(A))
& up_complete_relstr(boole_POSet(A))
& directed_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)],[f48_nnf]) ).
cnf(c136,plain,
~ empty_carrier(boole_POSet(X0)),
inference(cnf_transformation,[status(esa)],[f48_sk]) ).
cnf(c147,plain,
~ v1_yellow_3(boole_POSet(X0)),
inference(cnf_transformation,[status(esa)],[f48_sk]) ).
fof(f51,axiom,
? [A] :
( connected_relstr(A)
& antisymmetric_relstr(A)
& transitive_relstr(A)
& reflexive_relstr(A)
& ~ empty_carrier(A)
& rel_str(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc12_waybel_0) ).
fof(f51_nnf,plain,
? [A] :
( connected_relstr(A)
& antisymmetric_relstr(A)
& transitive_relstr(A)
& reflexive_relstr(A)
& ~ empty_carrier(A)
& rel_str(A) ),
inference(nnf_transformation,[status(thm)],[f51]) ).
fof(f51_sk,plain,
( connected_relstr(sk6)
& antisymmetric_relstr(sk6)
& transitive_relstr(sk6)
& reflexive_relstr(sk6)
& ~ empty_carrier(sk6)
& rel_str(sk6) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk6])],[f51_nnf]) ).
cnf(c158,plain,
~ empty_carrier(sk6),
inference(cnf_transformation,[status(esa)],[f51_sk]) ).
fof(f52,axiom,
? [A] :
( join_complete_relstr(A)
& up_complete_relstr(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)
& strict_rel_str(A)
& ~ empty_carrier(A)
& rel_str(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc13_waybel_0) ).
fof(f52_nnf,plain,
? [A] :
( join_complete_relstr(A)
& up_complete_relstr(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)
& strict_rel_str(A)
& ~ empty_carrier(A)
& rel_str(A) ),
inference(nnf_transformation,[status(thm)],[f52]) ).
fof(f52_sk,plain,
( join_complete_relstr(sk7)
& up_complete_relstr(sk7)
& bounded_relstr(sk7)
& upper_bounded_relstr(sk7)
& lower_bounded_relstr(sk7)
& complete_relstr(sk7)
& with_infima_relstr(sk7)
& with_suprema_relstr(sk7)
& antisymmetric_relstr(sk7)
& transitive_relstr(sk7)
& reflexive_relstr(sk7)
& strict_rel_str(sk7)
& ~ empty_carrier(sk7)
& rel_str(sk7) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk7])],[f52_nnf]) ).
cnf(c164,plain,
~ empty_carrier(sk7),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
fof(f53,axiom,
? [A] :
( finite(A)
& ~ empty(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc1_finset_1) ).
fof(f53_nnf,plain,
? [A] :
( finite(A)
& ~ empty(A) ),
inference(nnf_transformation,[status(thm)],[f53]) ).
fof(f53_sk,plain,
( finite(sk8)
& ~ empty(sk8) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk8])],[f53_nnf]) ).
cnf(c177,plain,
~ empty(sk8),
inference(cnf_transformation,[status(esa)],[f53_sk]) ).
fof(f54,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(f54_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)],[f54]) ).
fof(f54_sk,plain,
( complete_relstr(sk9)
& antisymmetric_relstr(sk9)
& transitive_relstr(sk9)
& reflexive_relstr(sk9)
& strict_rel_str(sk9)
& ~ empty_carrier(sk9)
& rel_str(sk9) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk9])],[f54_nnf]) ).
cnf(c180,plain,
~ empty_carrier(sk9),
inference(cnf_transformation,[status(esa)],[f54_sk]) ).
fof(f57,axiom,
? [A] :
( with_infima_relstr(A)
& with_suprema_relstr(A)
& boolean_relstr(A)
& complemented_relstr(A)
& heyting_relstr(A)
& distributive_relstr(A)
& ~ v1_yellow_3(A)
& bounded_relstr(A)
& upper_bounded_relstr(A)
& lower_bounded_relstr(A)
& antisymmetric_relstr(A)
& transitive_relstr(A)
& reflexive_relstr(A)
& strict_rel_str(A)
& ~ trivial_carrier(A)
& ~ empty_carrier(A)
& rel_str(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc1_waybel_7) ).
fof(f57_nnf,plain,
? [A] :
( with_infima_relstr(A)
& with_suprema_relstr(A)
& boolean_relstr(A)
& complemented_relstr(A)
& heyting_relstr(A)
& distributive_relstr(A)
& ~ v1_yellow_3(A)
& bounded_relstr(A)
& upper_bounded_relstr(A)
& lower_bounded_relstr(A)
& antisymmetric_relstr(A)
& transitive_relstr(A)
& reflexive_relstr(A)
& strict_rel_str(A)
& ~ trivial_carrier(A)
& ~ empty_carrier(A)
& rel_str(A) ),
inference(nnf_transformation,[status(thm)],[f57]) ).
fof(f57_sk,plain,
( with_infima_relstr(sk12)
& with_suprema_relstr(sk12)
& boolean_relstr(sk12)
& complemented_relstr(sk12)
& heyting_relstr(sk12)
& distributive_relstr(sk12)
& ~ v1_yellow_3(sk12)
& bounded_relstr(sk12)
& upper_bounded_relstr(sk12)
& lower_bounded_relstr(sk12)
& antisymmetric_relstr(sk12)
& transitive_relstr(sk12)
& reflexive_relstr(sk12)
& strict_rel_str(sk12)
& ~ trivial_carrier(sk12)
& ~ empty_carrier(sk12)
& rel_str(sk12) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk12])],[f57_nnf]) ).
cnf(c191,plain,
~ empty_carrier(sk12),
inference(cnf_transformation,[status(esa)],[f57_sk]) ).
cnf(c192,plain,
~ trivial_carrier(sk12),
inference(cnf_transformation,[status(esa)],[f57_sk]) ).
cnf(c200,plain,
~ v1_yellow_3(sk12),
inference(cnf_transformation,[status(esa)],[f57_sk]) ).
fof(f58,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(f58_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)],[f58]) ).
fof(f58_sk,plain,
( trivial_carrier(sk13)
& complete_relstr(sk13)
& with_infima_relstr(sk13)
& with_suprema_relstr(sk13)
& antisymmetric_relstr(sk13)
& transitive_relstr(sk13)
& reflexive_relstr(sk13)
& strict_rel_str(sk13)
& ~ empty_carrier(sk13)
& rel_str(sk13) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk13])],[f58_nnf]) ).
cnf(c208,plain,
~ empty_carrier(sk13),
inference(cnf_transformation,[status(esa)],[f58_sk]) ).
fof(f59,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(f59_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)],[f59]) ).
fof(f59_sk,plain,
( complete_relstr(sk14)
& with_infima_relstr(sk14)
& with_suprema_relstr(sk14)
& antisymmetric_relstr(sk14)
& transitive_relstr(sk14)
& reflexive_relstr(sk14)
& strict_rel_str(sk14)
& ~ empty_carrier(sk14)
& rel_str(sk14) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk14])],[f59_nnf]) ).
cnf(c218,plain,
~ empty_carrier(sk14),
inference(cnf_transformation,[status(esa)],[f59_sk]) ).
fof(f60,axiom,
? [A] :
( relation(A)
& ~ empty(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc2_relat_1) ).
fof(f60_nnf,plain,
? [A] :
( relation(A)
& ~ empty(A) ),
inference(nnf_transformation,[status(thm)],[f60]) ).
fof(f60_sk,plain,
( relation(sk15)
& ~ empty(sk15) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk15])],[f60_nnf]) ).
cnf(c226,plain,
~ empty(sk15),
inference(cnf_transformation,[status(esa)],[f60_sk]) ).
fof(f62,axiom,
! [A] :
? [B] :
( finite(B)
& ~ empty(B)
& element(B,powerset(powerset(A))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc2_waybel_7) ).
fof(f62_nnf,plain,
! [A] :
? [B] :
( finite(B)
& ~ empty(B)
& element(B,powerset(powerset(A))) ),
inference(nnf_transformation,[status(thm)],[f62]) ).
fof(f62_sk,plain,
! [A] :
( finite(sk17(A))
& ~ empty(sk17(A))
& element(sk17(A),powerset(powerset(A))) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk17])],[f62_nnf]) ).
cnf(c231,plain,
~ empty(sk17(X0)),
inference(cnf_transformation,[status(esa)],[f62_sk]) ).
fof(f63,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(f63_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)],[f63]) ).
fof(f63_sk,plain,
( bounded_relstr(sk18)
& upper_bounded_relstr(sk18)
& lower_bounded_relstr(sk18)
& complete_relstr(sk18)
& with_infima_relstr(sk18)
& with_suprema_relstr(sk18)
& antisymmetric_relstr(sk18)
& transitive_relstr(sk18)
& reflexive_relstr(sk18)
& ~ empty_carrier(sk18)
& rel_str(sk18) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk18])],[f63_nnf]) ).
cnf(c234,plain,
~ empty_carrier(sk18),
inference(cnf_transformation,[status(esa)],[f63_sk]) ).
fof(f66,axiom,
? [A] :
( ~ empty_carrier(A)
& one_sorted_str(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc3_struct_0) ).
fof(f66_nnf,plain,
? [A] :
( ~ empty_carrier(A)
& one_sorted_str(A) ),
inference(nnf_transformation,[status(thm)],[f66]) ).
fof(f66_sk,plain,
( ~ empty_carrier(sk21)
& one_sorted_str(sk21) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk21])],[f66_nnf]) ).
cnf(c250,plain,
~ empty_carrier(sk21),
inference(cnf_transformation,[status(esa)],[f66_sk]) ).
fof(f67,axiom,
! [A] :
( one_sorted_str(A)
=> ? [B] :
( finite(B)
& ~ empty(B)
& element(B,powerset(powerset(the_carrier(A)))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc3_waybel_7) ).
fof(f67_nnf,plain,
! [A] :
( ? [B] :
( finite(B)
& ~ empty(B)
& element(B,powerset(powerset(the_carrier(A)))) )
| ~ one_sorted_str(A) ),
inference(nnf_transformation,[status(thm)],[f67]) ).
fof(f67_sk,plain,
! [A] :
( ( finite(sk22(A))
& ~ empty(sk22(A))
& element(sk22(A),powerset(powerset(the_carrier(A)))) )
| ~ one_sorted_str(A) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk22])],[f67_nnf]) ).
cnf(c252,plain,
( ~ empty(sk22(X0))
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[status(esa)],[f67_sk]) ).
fof(f70,axiom,
? [A] :
( directed_relstr(A)
& transitive_relstr(A)
& strict_rel_str(A)
& ~ empty_carrier(A)
& rel_str(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc4_yellow_6) ).
fof(f70_nnf,plain,
? [A] :
( directed_relstr(A)
& transitive_relstr(A)
& strict_rel_str(A)
& ~ empty_carrier(A)
& rel_str(A) ),
inference(nnf_transformation,[status(thm)],[f70]) ).
fof(f70_sk,plain,
( directed_relstr(sk25)
& transitive_relstr(sk25)
& strict_rel_str(sk25)
& ~ empty_carrier(sk25)
& rel_str(sk25) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk25])],[f70_nnf]) ).
cnf(c263,plain,
~ empty_carrier(sk25),
inference(cnf_transformation,[status(esa)],[f70_sk]) ).
cnf(c275,plain,
~ empty(sk27),
inference(cnf_transformation,[status(esa)],[f77_sk]) ).
fof(f80,axiom,
! [A,B,C] :
~ ( empty(C)
& element(B,powerset(C))
& in(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_subset) ).
fof(f80_nnf,plain,
! [A,B,C] :
( ~ empty(C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f80]) ).
fof(f80_sk,plain,
! [A,B,C] :
( ~ empty(C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f80_nnf]) ).
cnf(c286,plain,
( ~ empty(X2)
| ~ element(X1,powerset(X2))
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f80_sk]) ).
fof(f82,axiom,
! [A,B] :
~ ( empty(B)
& in(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t7_boole) ).
fof(f82_nnf,plain,
! [A,B] :
( ~ empty(B)
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f82]) ).
fof(f82_sk,plain,
! [A,B] :
( ~ empty(B)
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f82_nnf]) ).
cnf(c288,plain,
( ~ empty(X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f82_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c1,c29,c36,c50,c79,c80,c90,c120,c125,c136,c147,c158,c164,c177,c180,c191,c192,c200,c208,c218,c226,c231,c234,c250,c252,c263,c275,c276,c286,c288]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t1209]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU387+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.07/0.35 % Computer : n008.cluster.edu
% 0.07/0.35 % Model : x86_64 x86_64
% 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.35 % Memory : 8046.5625MB
% 0.07/0.35 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Thu Sep 24 13:57:09 UTC 2026
% 0.07/0.36 % CPUTime :
% 0.07/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 84.72/11.38 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 84.72/11.38 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------