%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SEU381+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n001.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 02:57:17 PM UTC 2026
% Result : Theorem 26.86s 9.48s
% Output : CNFRefutation 26.86s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 11
% Syntax : Number of formulae : 135 ( 16 unt; 1 def)
% Number of atoms : 698 ( 16 equ)
% Maximal formula atoms : 20 ( 5 avg)
% Number of connectives : 935 ( 372 ~; 399 |; 137 &)
% ( 11 <=>; 14 =>; 0 <=; 2 <~>)
% Maximal formula depth : 23 ( 8 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 30 ( 28 usr; 1 prp; 0-3 aty)
% Number of functors : 9 ( 9 usr; 4 con; 0-2 aty)
% Number of variables : 284 ( 0 sgn 264 !; 20 ?; 116 :)
% Comments :
%------------------------------------------------------------------------------
fof(f36,axiom,
! [X0] :
( rel_str(X0)
=> ! [X1] :
( element(X1,powerset(the_carrier(X0)))
=> ( upper_relstr_subset(X1,X0)
<=> ! [X2] :
( element(X2,the_carrier(X0))
=> ! [X3] :
( element(X3,the_carrier(X0))
=> ( ( related(X0,X2,X3)
& in(X2,X1) )
=> in(X3,X1) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d20_waybel_0) ).
fof(f41,axiom,
! [X0] :
( rel_str(boole_POSet(X0))
& strict_rel_str(boole_POSet(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k3_yellow_1) ).
fof(f61,axiom,
! [X0] :
( ~ empty(X0)
=> ( complete_relstr(boole_POSet(X0))
& with_infima_relstr(boole_POSet(X0))
& with_suprema_relstr(boole_POSet(X0))
& boolean_relstr(boole_POSet(X0))
& complemented_relstr(boole_POSet(X0))
& heyting_relstr(boole_POSet(X0))
& distributive_relstr(boole_POSet(X0))
& ~ v1_yellow_3(boole_POSet(X0))
& join_complete_relstr(boole_POSet(X0))
& up_complete_relstr(boole_POSet(X0))
& bounded_relstr(boole_POSet(X0))
& upper_bounded_relstr(boole_POSet(X0))
& lower_bounded_relstr(boole_POSet(X0))
& antisymmetric_relstr(boole_POSet(X0))
& transitive_relstr(boole_POSet(X0))
& reflexive_relstr(boole_POSet(X0))
& strict_rel_str(boole_POSet(X0))
& ~ trivial_carrier(boole_POSet(X0))
& ~ empty_carrier(boole_POSet(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc2_waybel_7) ).
fof(f65,axiom,
! [X0] :
( complemented_relstr(boole_POSet(X0))
& distributive_relstr(boole_POSet(X0))
& join_complete_relstr(boole_POSet(X0))
& up_complete_relstr(boole_POSet(X0))
& bounded_relstr(boole_POSet(X0))
& upper_bounded_relstr(boole_POSet(X0))
& lower_bounded_relstr(boole_POSet(X0))
& complete_relstr(boole_POSet(X0))
& with_infima_relstr(boole_POSet(X0))
& with_suprema_relstr(boole_POSet(X0))
& antisymmetric_relstr(boole_POSet(X0))
& transitive_relstr(boole_POSet(X0))
& reflexive_relstr(boole_POSet(X0))
& strict_rel_str(boole_POSet(X0))
& ~ empty_carrier(boole_POSet(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc9_waybel_1) ).
fof(f95,axiom,
! [X0,X1,X2] :
( ( element(X2,the_carrier(X0))
& element(X1,the_carrier(X0))
& rel_str(X0)
& reflexive_relstr(X0)
& ~ empty_carrier(X0) )
=> ( related_reflexive(X0,X1,X2)
<=> related(X0,X1,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_r3_orders_2) ).
fof(f98,conjecture,
! [X0,X1] :
( element(X1,powerset(the_carrier(boole_POSet(X0))))
=> ( upper_relstr_subset(X1,boole_POSet(X0))
<=> ! [X2,X3] :
( ( in(X2,X1)
& subset(X3,X0)
& subset(X2,X3) )
=> in(X3,X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t11_waybel_7) ).
fof(f99,negated_conjecture,
~ ! [X0,X1] :
( element(X1,powerset(the_carrier(boole_POSet(X0))))
=> ( upper_relstr_subset(X1,boole_POSet(X0))
<=> ! [X2,X3] :
( ( in(X2,X1)
& subset(X3,X0)
& subset(X2,X3) )
=> in(X3,X1) ) ) ),
inference(negated_conjecture,[status(cth)],[f98]) ).
fof(f102,axiom,
! [X0,X1] :
( element(X1,the_carrier(boole_POSet(X0)))
=> ! [X2] :
( element(X2,the_carrier(boole_POSet(X0)))
=> ( related_reflexive(boole_POSet(X0),X1,X2)
<=> subset(X1,X2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2_yellow_1) ).
fof(f103,axiom,
! [X0,X1] :
( element(X0,powerset(X1))
<=> subset(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t3_subset) ).
fof(f104,axiom,
! [X0,X1,X2] :
( ( element(X1,powerset(X2))
& in(X0,X1) )
=> element(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t4_subset) ).
fof(f105,axiom,
! [X0] : the_carrier(boole_POSet(X0)) = powerset(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t4_waybel_7) ).
fof(f186,plain,
! [X0] :
( ~ rel_str(X0)
| ! [X1] :
( ~ element(X1,powerset(the_carrier(X0)))
| ( upper_relstr_subset(X1,X0)
<=> ! [X2] :
( ~ element(X2,the_carrier(X0))
| ! [X3] :
( ~ element(X3,the_carrier(X0))
| ~ related(X0,X2,X3)
| ~ in(X2,X1)
| in(X3,X1) ) ) ) ) ),
inference(ennf_transformation,[],[f36]) ).
fof(f187,plain,
! [X0] :
( ~ rel_str(X0)
| ! [X1] :
( ~ element(X1,powerset(the_carrier(X0)))
| ( upper_relstr_subset(X1,X0)
<=> ! [X2] :
( ~ element(X2,the_carrier(X0))
| ! [X3] :
( ~ element(X3,the_carrier(X0))
| ~ related(X0,X2,X3)
| ~ in(X2,X1)
| in(X3,X1) ) ) ) ) ),
inference(flattening,[],[f186]) ).
fof(f198,plain,
! [X0] :
( empty(X0)
| ( complete_relstr(boole_POSet(X0))
& with_infima_relstr(boole_POSet(X0))
& with_suprema_relstr(boole_POSet(X0))
& boolean_relstr(boole_POSet(X0))
& complemented_relstr(boole_POSet(X0))
& heyting_relstr(boole_POSet(X0))
& distributive_relstr(boole_POSet(X0))
& ~ v1_yellow_3(boole_POSet(X0))
& join_complete_relstr(boole_POSet(X0))
& up_complete_relstr(boole_POSet(X0))
& bounded_relstr(boole_POSet(X0))
& upper_bounded_relstr(boole_POSet(X0))
& lower_bounded_relstr(boole_POSet(X0))
& antisymmetric_relstr(boole_POSet(X0))
& transitive_relstr(boole_POSet(X0))
& reflexive_relstr(boole_POSet(X0))
& strict_rel_str(boole_POSet(X0))
& ~ trivial_carrier(boole_POSet(X0))
& ~ empty_carrier(boole_POSet(X0)) ) ),
inference(ennf_transformation,[],[f61]) ).
fof(f213,plain,
! [X0,X1,X2] :
( ~ element(X2,the_carrier(X0))
| ~ element(X1,the_carrier(X0))
| ~ rel_str(X0)
| ~ reflexive_relstr(X0)
| empty_carrier(X0)
| ( related_reflexive(X0,X1,X2)
<=> related(X0,X1,X2) ) ),
inference(ennf_transformation,[],[f95]) ).
fof(f214,plain,
! [X0,X1,X2] :
( ~ element(X2,the_carrier(X0))
| ~ element(X1,the_carrier(X0))
| ~ rel_str(X0)
| ~ reflexive_relstr(X0)
| empty_carrier(X0)
| ( related_reflexive(X0,X1,X2)
<=> related(X0,X1,X2) ) ),
inference(flattening,[],[f213]) ).
fof(f217,plain,
? [X0,X1] :
( element(X1,powerset(the_carrier(boole_POSet(X0))))
& ( upper_relstr_subset(X1,boole_POSet(X0))
<~> ! [X2,X3] :
( ~ in(X2,X1)
| ~ subset(X3,X0)
| ~ subset(X2,X3)
| in(X3,X1) ) ) ),
inference(ennf_transformation,[],[f99]) ).
fof(f218,plain,
? [X0,X1] :
( element(X1,powerset(the_carrier(boole_POSet(X0))))
& ( upper_relstr_subset(X1,boole_POSet(X0))
<~> ! [X2,X3] :
( ~ in(X2,X1)
| ~ subset(X3,X0)
| ~ subset(X2,X3)
| in(X3,X1) ) ) ),
inference(flattening,[],[f217]) ).
fof(f222,plain,
! [X0,X1] :
( ~ element(X1,the_carrier(boole_POSet(X0)))
| ! [X2] :
( ~ element(X2,the_carrier(boole_POSet(X0)))
| ( related_reflexive(boole_POSet(X0),X1,X2)
<=> subset(X1,X2) ) ) ),
inference(ennf_transformation,[],[f102]) ).
fof(f223,plain,
! [X0,X1,X2] :
( ~ element(X1,powerset(X2))
| ~ in(X0,X1)
| element(X0,X2) ),
inference(ennf_transformation,[],[f104]) ).
fof(f224,plain,
! [X0,X1,X2] :
( ~ element(X1,powerset(X2))
| ~ in(X0,X1)
| element(X0,X2) ),
inference(flattening,[],[f223]) ).
fof(f252,plain,
! [X0] :
( ~ rel_str(X0)
| ! [X1] :
( ~ element(X1,powerset(the_carrier(X0)))
| ( ( ~ upper_relstr_subset(X1,X0)
| ! [X2] :
( ~ element(X2,the_carrier(X0))
| ! [X3] :
( ~ element(X3,the_carrier(X0))
| ~ related(X0,X2,X3)
| ~ in(X2,X1)
| in(X3,X1) ) ) )
& ( ? [X2] :
( element(X2,the_carrier(X0))
& ? [X3] :
( element(X3,the_carrier(X0))
& related(X0,X2,X3)
& in(X2,X1)
& ~ in(X3,X1) ) )
| upper_relstr_subset(X1,X0) ) ) ) ),
inference(nnf_transformation,[],[f187]) ).
fof(f253,plain,
! [X0] :
( ~ rel_str(X0)
| ! [X1] :
( ~ element(X1,powerset(the_carrier(X0)))
| ( ( ~ upper_relstr_subset(X1,X0)
| ! [X4] :
( ~ element(X4,the_carrier(X0))
| ! [X5] :
( ~ element(X5,the_carrier(X0))
| ~ related(X0,X4,X5)
| ~ in(X4,X1)
| in(X5,X1) ) ) )
& ( ? [X2] :
( element(X2,the_carrier(X0))
& ? [X3] :
( element(X3,the_carrier(X0))
& related(X0,X2,X3)
& in(X2,X1)
& ~ in(X3,X1) ) )
| upper_relstr_subset(X1,X0) ) ) ) ),
inference(rectify,[],[f252]) ).
fof(f254,plain,
! [X0] :
( ~ rel_str(X0)
| ! [X1] :
( ~ element(X1,powerset(the_carrier(X0)))
| ( ( ~ upper_relstr_subset(X1,X0)
| ! [X4] :
( ~ element(X4,the_carrier(X0))
| ! [X5] :
( ~ element(X5,the_carrier(X0))
| ~ related(X0,X4,X5)
| ~ in(X4,X1)
| in(X5,X1) ) ) )
& ( ( element(sK8(X0,X1),the_carrier(X0))
& element(sK9(X0,X1),the_carrier(X0))
& related(X0,sK8(X0,X1),sK9(X0,X1))
& in(sK8(X0,X1),X1)
& ~ in(sK9(X0,X1),X1) )
| upper_relstr_subset(X1,X0) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8,sK9]),skolemize(X2,sK8(X0,X1)),skolemize(X3,sK9(X0,X1))],[f253]) ).
fof(f289,plain,
! [X0,X1,X2] :
( ~ element(X2,the_carrier(X0))
| ~ element(X1,the_carrier(X0))
| ~ rel_str(X0)
| ~ reflexive_relstr(X0)
| empty_carrier(X0)
| ( ( ~ related_reflexive(X0,X1,X2)
| related(X0,X1,X2) )
& ( ~ related(X0,X1,X2)
| related_reflexive(X0,X1,X2) ) ) ),
inference(nnf_transformation,[],[f214]) ).
fof(f290,plain,
? [X0,X1] :
( element(X1,powerset(the_carrier(boole_POSet(X0))))
& ( upper_relstr_subset(X1,boole_POSet(X0))
| ! [X2,X3] :
( ~ in(X2,X1)
| ~ subset(X3,X0)
| ~ subset(X2,X3)
| in(X3,X1) ) )
& ( ~ upper_relstr_subset(X1,boole_POSet(X0))
| ? [X2,X3] :
( in(X2,X1)
& subset(X3,X0)
& subset(X2,X3)
& ~ in(X3,X1) ) ) ),
inference(nnf_transformation,[],[f218]) ).
fof(f291,plain,
? [X0,X1] :
( element(X1,powerset(the_carrier(boole_POSet(X0))))
& ( upper_relstr_subset(X1,boole_POSet(X0))
| ! [X2,X3] :
( ~ in(X2,X1)
| ~ subset(X3,X0)
| ~ subset(X2,X3)
| in(X3,X1) ) )
& ( ~ upper_relstr_subset(X1,boole_POSet(X0))
| ? [X2,X3] :
( in(X2,X1)
& subset(X3,X0)
& subset(X2,X3)
& ~ in(X3,X1) ) ) ),
inference(flattening,[],[f290]) ).
fof(f292,plain,
? [X0,X1] :
( element(X1,powerset(the_carrier(boole_POSet(X0))))
& ( upper_relstr_subset(X1,boole_POSet(X0))
| ! [X4,X5] :
( ~ in(X4,X1)
| ~ subset(X5,X0)
| ~ subset(X4,X5)
| in(X5,X1) ) )
& ( ~ upper_relstr_subset(X1,boole_POSet(X0))
| ? [X2,X3] :
( in(X2,X1)
& subset(X3,X0)
& subset(X2,X3)
& ~ in(X3,X1) ) ) ),
inference(rectify,[],[f291]) ).
fof(f293,plain,
( element(sK43,powerset(the_carrier(boole_POSet(sK42))))
& ( upper_relstr_subset(sK43,boole_POSet(sK42))
| ! [X4,X5] :
( ~ in(X4,sK43)
| ~ subset(X5,sK42)
| ~ subset(X4,X5)
| in(X5,sK43) ) )
& ( ~ upper_relstr_subset(sK43,boole_POSet(sK42))
| ( in(sK44,sK43)
& subset(sK45,sK42)
& subset(sK44,sK45)
& ~ in(sK45,sK43) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK42,sK43,sK44,sK45]),skolemize(X0,sK42),skolemize(X1,sK43),skolemize(X2,sK44),skolemize(X3,sK45)],[f292]) ).
fof(f294,plain,
! [X0,X1] :
( ~ element(X1,the_carrier(boole_POSet(X0)))
| ! [X2] :
( ~ element(X2,the_carrier(boole_POSet(X0)))
| ( ( ~ related_reflexive(boole_POSet(X0),X1,X2)
| subset(X1,X2) )
& ( ~ subset(X1,X2)
| related_reflexive(boole_POSet(X0),X1,X2) ) ) ) ),
inference(nnf_transformation,[],[f222]) ).
fof(f295,plain,
! [X0,X1] :
( ( ~ element(X0,powerset(X1))
| subset(X0,X1) )
& ( ~ subset(X0,X1)
| element(X0,powerset(X1)) ) ),
inference(nnf_transformation,[],[f103]) ).
fof(f459,plain,
! [X0,X1,X4,X5] :
( ~ rel_str(X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ upper_relstr_subset(X1,X0)
| ~ element(X4,the_carrier(X0))
| ~ element(X5,the_carrier(X0))
| ~ related(X0,X4,X5)
| ~ in(X4,X1)
| in(X5,X1) ),
inference(cnf_transformation,[],[f254]) ).
fof(f460,plain,
! [X0,X1] :
( ~ rel_str(X0)
| ~ element(X1,powerset(the_carrier(X0)))
| element(sK8(X0,X1),the_carrier(X0))
| upper_relstr_subset(X1,X0) ),
inference(cnf_transformation,[],[f254]) ).
fof(f461,plain,
! [X0,X1] :
( ~ rel_str(X0)
| ~ element(X1,powerset(the_carrier(X0)))
| element(sK9(X0,X1),the_carrier(X0))
| upper_relstr_subset(X1,X0) ),
inference(cnf_transformation,[],[f254]) ).
fof(f462,plain,
! [X0,X1] :
( ~ rel_str(X0)
| ~ element(X1,powerset(the_carrier(X0)))
| related(X0,sK8(X0,X1),sK9(X0,X1))
| upper_relstr_subset(X1,X0) ),
inference(cnf_transformation,[],[f254]) ).
fof(f463,plain,
! [X0,X1] :
( ~ rel_str(X0)
| ~ element(X1,powerset(the_carrier(X0)))
| in(sK8(X0,X1),X1)
| upper_relstr_subset(X1,X0) ),
inference(cnf_transformation,[],[f254]) ).
fof(f464,plain,
! [X0,X1] :
( ~ rel_str(X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ in(sK9(X0,X1),X1)
| upper_relstr_subset(X1,X0) ),
inference(cnf_transformation,[],[f254]) ).
fof(f467,plain,
! [X0] : rel_str(boole_POSet(X0)),
inference(cnf_transformation,[],[f41]) ).
fof(f563,plain,
! [X0] : reflexive_relstr(boole_POSet(X0)),
inference(cnf_transformation,[],[f65]) ).
fof(f565,plain,
! [X0] : ~ empty_carrier(boole_POSet(X0)),
inference(cnf_transformation,[],[f65]) ).
fof(f755,plain,
! [X2,X0,X1] :
( ~ element(X2,the_carrier(X0))
| ~ element(X1,the_carrier(X0))
| ~ rel_str(X0)
| ~ reflexive_relstr(X0)
| empty_carrier(X0)
| ~ related_reflexive(X0,X1,X2)
| related(X0,X1,X2) ),
inference(cnf_transformation,[],[f289]) ).
fof(f756,plain,
! [X2,X0,X1] :
( ~ element(X2,the_carrier(X0))
| ~ element(X1,the_carrier(X0))
| ~ rel_str(X0)
| ~ reflexive_relstr(X0)
| empty_carrier(X0)
| ~ related(X0,X1,X2)
| related_reflexive(X0,X1,X2) ),
inference(cnf_transformation,[],[f289]) ).
fof(f759,plain,
element(sK43,powerset(the_carrier(boole_POSet(sK42)))),
inference(cnf_transformation,[],[f293]) ).
fof(f760,plain,
! [X4,X5] :
( upper_relstr_subset(sK43,boole_POSet(sK42))
| ~ in(X4,sK43)
| ~ subset(X5,sK42)
| ~ subset(X4,X5)
| in(X5,sK43) ),
inference(cnf_transformation,[],[f293]) ).
fof(f761,plain,
( ~ upper_relstr_subset(sK43,boole_POSet(sK42))
| in(sK44,sK43) ),
inference(cnf_transformation,[],[f293]) ).
fof(f762,plain,
( ~ upper_relstr_subset(sK43,boole_POSet(sK42))
| subset(sK45,sK42) ),
inference(cnf_transformation,[],[f293]) ).
fof(f763,plain,
( ~ upper_relstr_subset(sK43,boole_POSet(sK42))
| subset(sK44,sK45) ),
inference(cnf_transformation,[],[f293]) ).
fof(f764,plain,
( ~ upper_relstr_subset(sK43,boole_POSet(sK42))
| ~ in(sK45,sK43) ),
inference(cnf_transformation,[],[f293]) ).
fof(f767,plain,
! [X2,X0,X1] :
( ~ element(X1,the_carrier(boole_POSet(X0)))
| ~ element(X2,the_carrier(boole_POSet(X0)))
| ~ related_reflexive(boole_POSet(X0),X1,X2)
| subset(X1,X2) ),
inference(cnf_transformation,[],[f294]) ).
fof(f768,plain,
! [X2,X0,X1] :
( ~ element(X1,the_carrier(boole_POSet(X0)))
| ~ element(X2,the_carrier(boole_POSet(X0)))
| ~ subset(X1,X2)
| related_reflexive(boole_POSet(X0),X1,X2) ),
inference(cnf_transformation,[],[f294]) ).
fof(f769,plain,
! [X0,X1] :
( ~ element(X0,powerset(X1))
| subset(X0,X1) ),
inference(cnf_transformation,[],[f295]) ).
fof(f770,plain,
! [X0,X1] :
( ~ subset(X0,X1)
| element(X0,powerset(X1)) ),
inference(cnf_transformation,[],[f295]) ).
fof(f771,plain,
! [X2,X0,X1] :
( ~ element(X1,powerset(X2))
| ~ in(X0,X1)
| element(X0,X2) ),
inference(cnf_transformation,[],[f224]) ).
fof(f772,plain,
! [X0] : powerset(X0) = the_carrier(boole_POSet(X0)),
inference(cnf_transformation,[],[f105]) ).
fof(f778,plain,
! [X0,X1] :
( ~ rel_str(X0)
| ~ element(X1,the_carrier(boole_POSet(the_carrier(X0))))
| ~ in(sK9(X0,X1),X1)
| upper_relstr_subset(X1,X0) ),
inference(definition_unfolding,[],[f464,f772]) ).
fof(f779,plain,
! [X0,X1] :
( ~ rel_str(X0)
| ~ element(X1,the_carrier(boole_POSet(the_carrier(X0))))
| in(sK8(X0,X1),X1)
| upper_relstr_subset(X1,X0) ),
inference(definition_unfolding,[],[f463,f772]) ).
fof(f780,plain,
! [X0,X1] :
( ~ rel_str(X0)
| ~ element(X1,the_carrier(boole_POSet(the_carrier(X0))))
| related(X0,sK8(X0,X1),sK9(X0,X1))
| upper_relstr_subset(X1,X0) ),
inference(definition_unfolding,[],[f462,f772]) ).
fof(f781,plain,
! [X0,X1] :
( ~ rel_str(X0)
| ~ element(X1,the_carrier(boole_POSet(the_carrier(X0))))
| element(sK9(X0,X1),the_carrier(X0))
| upper_relstr_subset(X1,X0) ),
inference(definition_unfolding,[],[f461,f772]) ).
fof(f782,plain,
! [X0,X1] :
( ~ rel_str(X0)
| ~ element(X1,the_carrier(boole_POSet(the_carrier(X0))))
| element(sK8(X0,X1),the_carrier(X0))
| upper_relstr_subset(X1,X0) ),
inference(definition_unfolding,[],[f460,f772]) ).
fof(f783,plain,
! [X0,X1,X4,X5] :
( ~ rel_str(X0)
| ~ element(X1,the_carrier(boole_POSet(the_carrier(X0))))
| ~ upper_relstr_subset(X1,X0)
| ~ element(X4,the_carrier(X0))
| ~ element(X5,the_carrier(X0))
| ~ related(X0,X4,X5)
| ~ in(X4,X1)
| in(X5,X1) ),
inference(definition_unfolding,[],[f459,f772]) ).
fof(f796,plain,
element(sK43,the_carrier(boole_POSet(the_carrier(boole_POSet(sK42))))),
inference(definition_unfolding,[],[f759,f772]) ).
fof(f797,plain,
! [X0,X1] :
( ~ subset(X0,X1)
| element(X0,the_carrier(boole_POSet(X1))) ),
inference(definition_unfolding,[],[f770,f772]) ).
fof(f798,plain,
! [X0,X1] :
( ~ element(X0,the_carrier(boole_POSet(X1)))
| subset(X0,X1) ),
inference(definition_unfolding,[],[f769,f772]) ).
fof(f799,plain,
! [X2,X0,X1] :
( ~ element(X1,the_carrier(boole_POSet(X2)))
| ~ in(X0,X1)
| element(X0,X2) ),
inference(definition_unfolding,[],[f771,f772]) ).
tcf(c_175,plain,
! [X0: $i,X1: $i] :
( upper_relstr_subset(X0,X1)
| ~ rel_str(X1)
| ~ in(sK9(X1,X0),X0)
| ~ element(X0,the_carrier(boole_POSet(the_carrier(X1)))) ),
inference(cnf_transformation,[],[f778]) ).
tcf(c_176,plain,
! [X0: $i,X1: $i] :
( upper_relstr_subset(X0,X1)
| in(sK8(X1,X0),X0)
| ~ rel_str(X1)
| ~ element(X0,the_carrier(boole_POSet(the_carrier(X1)))) ),
inference(cnf_transformation,[],[f779]) ).
tcf(c_177,plain,
! [X0: $i,X1: $i] :
( upper_relstr_subset(X0,X1)
| related(X1,sK8(X1,X0),sK9(X1,X0))
| ~ rel_str(X1)
| ~ element(X0,the_carrier(boole_POSet(the_carrier(X1)))) ),
inference(cnf_transformation,[],[f780]) ).
tcf(c_178,plain,
! [X0: $i,X1: $i] :
( upper_relstr_subset(X0,X1)
| element(sK9(X1,X0),the_carrier(X1))
| ~ rel_str(X1)
| ~ element(X0,the_carrier(boole_POSet(the_carrier(X1)))) ),
inference(cnf_transformation,[],[f781]) ).
tcf(c_179,plain,
! [X0: $i,X1: $i] :
( upper_relstr_subset(X0,X1)
| element(sK8(X1,X0),the_carrier(X1))
| ~ rel_str(X1)
| ~ element(X0,the_carrier(boole_POSet(the_carrier(X1)))) ),
inference(cnf_transformation,[],[f782]) ).
tcf(c_180,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( in(X3,X0)
| ~ rel_str(X1)
| ~ upper_relstr_subset(X0,X1)
| ~ in(X2,X0)
| ~ element(X3,the_carrier(X1))
| ~ element(X2,the_carrier(X1))
| ~ related(X1,X2,X3)
| ~ element(X0,the_carrier(boole_POSet(the_carrier(X1)))) ),
inference(cnf_transformation,[],[f783]) ).
tcf(c_184,plain,
! [X0: $i] : rel_str(boole_POSet(X0)),
inference(cnf_transformation,[],[f467]) ).
tcf(c_267,plain,
! [X0: $i] : ~ empty_carrier(boole_POSet(X0)),
inference(cnf_transformation,[],[f565]) ).
tcf(c_269,plain,
! [X0: $i] : reflexive_relstr(boole_POSet(X0)),
inference(cnf_transformation,[],[f563]) ).
tcf(c_471,plain,
! [X0: $i,X1: $i,X2: $i] :
( empty_carrier(X0)
| related_reflexive(X0,X1,X2)
| ~ reflexive_relstr(X0)
| ~ rel_str(X0)
| ~ element(X2,the_carrier(X0))
| ~ element(X1,the_carrier(X0))
| ~ related(X0,X1,X2) ),
inference(cnf_transformation,[],[f756]) ).
tcf(c_472,plain,
! [X0: $i,X1: $i,X2: $i] :
( empty_carrier(X0)
| related(X0,X1,X2)
| ~ reflexive_relstr(X0)
| ~ rel_str(X0)
| ~ element(X2,the_carrier(X0))
| ~ element(X1,the_carrier(X0))
| ~ related_reflexive(X0,X1,X2) ),
inference(cnf_transformation,[],[f755]) ).
tcf(c_475,negated_conjecture,
( ~ in(sK45,sK43)
| ~ upper_relstr_subset(sK43,boole_POSet(sK42)) ),
inference(cnf_transformation,[],[f764]) ).
tcf(c_476,negated_conjecture,
( subset(sK44,sK45)
| ~ upper_relstr_subset(sK43,boole_POSet(sK42)) ),
inference(cnf_transformation,[],[f763]) ).
tcf(c_477,negated_conjecture,
( subset(sK45,sK42)
| ~ upper_relstr_subset(sK43,boole_POSet(sK42)) ),
inference(cnf_transformation,[],[f762]) ).
tcf(c_478,negated_conjecture,
( in(sK44,sK43)
| ~ upper_relstr_subset(sK43,boole_POSet(sK42)) ),
inference(cnf_transformation,[],[f761]) ).
tcf(c_479,negated_conjecture,
! [X0: $i,X1: $i] :
( in(X1,sK43)
| upper_relstr_subset(sK43,boole_POSet(sK42))
| ~ subset(X1,sK42)
| ~ in(X0,sK43)
| ~ subset(X0,X1) ),
inference(cnf_transformation,[],[f760]) ).
tcf(c_480,negated_conjecture,
element(sK43,the_carrier(boole_POSet(the_carrier(boole_POSet(sK42))))),
inference(cnf_transformation,[],[f796]) ).
tcf(c_483,plain,
! [X0: $i,X1: $i,X2: $i] :
( related_reflexive(boole_POSet(X1),X0,X2)
| ~ subset(X0,X2)
| ~ element(X2,the_carrier(boole_POSet(X1)))
| ~ element(X0,the_carrier(boole_POSet(X1))) ),
inference(cnf_transformation,[],[f768]) ).
tcf(c_484,plain,
! [X0: $i,X1: $i,X2: $i] :
( subset(X1,X2)
| ~ element(X2,the_carrier(boole_POSet(X0)))
| ~ element(X1,the_carrier(boole_POSet(X0)))
| ~ related_reflexive(boole_POSet(X0),X1,X2) ),
inference(cnf_transformation,[],[f767]) ).
tcf(c_485,plain,
! [X0: $i,X1: $i] :
( element(X0,the_carrier(boole_POSet(X1)))
| ~ subset(X0,X1) ),
inference(cnf_transformation,[],[f797]) ).
tcf(c_486,plain,
! [X0: $i,X1: $i] :
( subset(X0,X1)
| ~ element(X0,the_carrier(boole_POSet(X1))) ),
inference(cnf_transformation,[],[f798]) ).
tcf(c_487,plain,
! [X0: $i,X1: $i,X2: $i] :
( element(X2,X1)
| ~ in(X2,X0)
| ~ element(X0,the_carrier(boole_POSet(X1))) ),
inference(cnf_transformation,[],[f799]) ).
tcf(c_638,plain,
! [X0: $i,X1: $i] :
( element(X0,the_carrier(boole_POSet(X1)))
| ~ subset(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_485]) ).
tcf(c_1433,plain,
! [X0: $i,X1: $i,X2: $i] :
( related_reflexive(boole_POSet(X1),X2,X0)
| ~ subset(X2,X1)
| ~ subset(X2,X0)
| ~ element(X0,the_carrier(boole_POSet(X1))) ),
inference(bin_hyper_res,[status(thm)],[c_483,c_638]) ).
tcf(c_1434,plain,
! [X0: $i,X1: $i,X2: $i] :
( element(X0,X2)
| ~ subset(X1,X2)
| ~ in(X0,X1) ),
inference(bin_hyper_res,[status(thm)],[c_487,c_638]) ).
tcf(c_3639,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( empty_carrier(X4)
| upper_relstr_subset(X1,X0)
| related_reflexive(X4,X3,X2)
| ~ reflexive_relstr(X4)
| ~ rel_str(X4)
| ~ rel_str(X0)
| ~ element(X3,the_carrier(X4))
| ~ element(X2,the_carrier(X4))
| ~ element(X1,the_carrier(boole_POSet(the_carrier(X0))))
| ( X0 != X4 )
| ( sK8(X0,X1) != X3 )
| ( sK9(X0,X1) != X2 ) ),
inference(resolution_lifted,[status(thm)],[c_177,c_471]) ).
tcf(c_3640,plain,
! [X0: $i,X1: $i] :
( empty_carrier(X0)
| upper_relstr_subset(X1,X0)
| related_reflexive(X0,sK8(X0,X1),sK9(X0,X1))
| ~ reflexive_relstr(X0)
| ~ rel_str(X0)
| ~ element(X1,the_carrier(boole_POSet(the_carrier(X0))))
| ~ element(sK8(X0,X1),the_carrier(X0))
| ~ element(sK9(X0,X1),the_carrier(X0)) ),
inference(unflattening,[status(thm)],[c_3639]) ).
tcf(c_3658,plain,
! [X0: $i,X1: $i] :
( empty_carrier(X1)
| upper_relstr_subset(X0,X1)
| related_reflexive(X1,sK8(X1,X0),sK9(X1,X0))
| ~ reflexive_relstr(X1)
| ~ rel_str(X1)
| ~ element(X0,the_carrier(boole_POSet(the_carrier(X1)))) ),
inference(forward_subsumption_resolution,[status(thm)],[c_3640,c_179,c_178]) ).
tcf(c_3666,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] :
( empty_carrier(X1)
| in(X4,X6)
| ~ reflexive_relstr(X1)
| ~ rel_str(X1)
| ~ rel_str(X0)
| ~ upper_relstr_subset(X6,X0)
| ~ in(X2,X6)
| ~ element(X5,the_carrier(X1))
| ~ element(X4,the_carrier(X0))
| ~ element(X3,the_carrier(X1))
| ~ element(X2,the_carrier(X0))
| ~ related_reflexive(X1,X3,X5)
| ~ element(X6,the_carrier(boole_POSet(the_carrier(X0))))
| ( X4 != X5 )
| ( X2 != X3 )
| ( X0 != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_180,c_472]) ).
tcf(c_3667,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( empty_carrier(X1)
| in(X3,X0)
| ~ reflexive_relstr(X1)
| ~ rel_str(X1)
| ~ upper_relstr_subset(X0,X1)
| ~ in(X2,X0)
| ~ element(X3,the_carrier(X1))
| ~ element(X2,the_carrier(X1))
| ~ related_reflexive(X1,X2,X3)
| ~ element(X0,the_carrier(boole_POSet(the_carrier(X1)))) ),
inference(unflattening,[status(thm)],[c_3666]) ).
tcf(c_4200,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( empty_carrier(X1)
| subset(X3,X4)
| upper_relstr_subset(X2,X1)
| ~ reflexive_relstr(X1)
| ~ rel_str(X1)
| ~ element(X4,the_carrier(boole_POSet(X0)))
| ~ element(X3,the_carrier(boole_POSet(X0)))
| ~ element(X2,the_carrier(boole_POSet(the_carrier(X1))))
| ( boole_POSet(X0) != X1 )
| ( sK8(X1,X2) != X3 )
| ( sK9(X1,X2) != X4 ) ),
inference(resolution_lifted,[status(thm)],[c_484,c_3658]) ).
tcf(c_4201,plain,
! [X0: $i,X1: $i] :
( empty_carrier(boole_POSet(X0))
| upper_relstr_subset(X1,boole_POSet(X0))
| subset(sK8(boole_POSet(X0),X1),sK9(boole_POSet(X0),X1))
| ~ reflexive_relstr(boole_POSet(X0))
| ~ rel_str(boole_POSet(X0))
| ~ element(X1,the_carrier(boole_POSet(the_carrier(boole_POSet(X0)))))
| ~ element(sK8(boole_POSet(X0),X1),the_carrier(boole_POSet(X0)))
| ~ element(sK9(boole_POSet(X0),X1),the_carrier(boole_POSet(X0))) ),
inference(unflattening,[status(thm)],[c_4200]) ).
tcf(c_4203,plain,
! [X0: $i,X1: $i] :
( ~ element(sK9(boole_POSet(X0),X1),the_carrier(boole_POSet(X0)))
| ~ element(sK8(boole_POSet(X0),X1),the_carrier(boole_POSet(X0)))
| ~ element(X1,the_carrier(boole_POSet(the_carrier(boole_POSet(X0)))))
| subset(sK8(boole_POSet(X0),X1),sK9(boole_POSet(X0),X1))
| upper_relstr_subset(X1,boole_POSet(X0)) ),
inference(global_subsumption_just,[status(thm)],[c_4201,c_269,c_184,c_267,c_4201]) ).
tcf(c_4204,plain,
! [X0: $i,X1: $i] :
( upper_relstr_subset(X1,boole_POSet(X0))
| subset(sK8(boole_POSet(X0),X1),sK9(boole_POSet(X0),X1))
| ~ element(X1,the_carrier(boole_POSet(the_carrier(boole_POSet(X0)))))
| ~ element(sK8(boole_POSet(X0),X1),the_carrier(boole_POSet(X0)))
| ~ element(sK9(boole_POSet(X0),X1),the_carrier(boole_POSet(X0))) ),
inference(renaming,[status(thm)],[c_4203]) ).
tcf(c_4221,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] :
( empty_carrier(X1)
| in(X3,X6)
| ~ reflexive_relstr(X1)
| ~ rel_str(X1)
| ~ subset(X4,X2)
| ~ subset(X4,X0)
| ~ upper_relstr_subset(X6,X1)
| ~ in(X5,X6)
| ~ element(X5,the_carrier(X1))
| ~ element(X3,the_carrier(X1))
| ~ element(X2,the_carrier(boole_POSet(X0)))
| ~ element(X6,the_carrier(boole_POSet(the_carrier(X1))))
| ( X4 != X5 )
| ( X2 != X3 )
| ( boole_POSet(X0) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_1433,c_3667]) ).
tcf(c_4222,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( empty_carrier(boole_POSet(X1))
| in(X2,X0)
| ~ reflexive_relstr(boole_POSet(X1))
| ~ rel_str(boole_POSet(X1))
| ~ subset(X3,X2)
| ~ subset(X3,X1)
| ~ in(X3,X0)
| ~ upper_relstr_subset(X0,boole_POSet(X1))
| ~ element(X3,the_carrier(boole_POSet(X1)))
| ~ element(X2,the_carrier(boole_POSet(X1)))
| ~ element(X0,the_carrier(boole_POSet(the_carrier(boole_POSet(X1))))) ),
inference(unflattening,[status(thm)],[c_4221]) ).
tcf(c_7639,plain,
! [X0: $i,X1: $i,X2: $i] :
( upper_relstr_subset(X2,X1)
| element(sK8(X1,X2),the_carrier(X1))
| ~ element(X2,the_carrier(boole_POSet(the_carrier(X1))))
| ( boole_POSet(X0) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_179,c_184]) ).
tcf(c_7640,plain,
! [X0: $i,X1: $i] :
( upper_relstr_subset(X0,boole_POSet(X1))
| element(sK8(boole_POSet(X1),X0),the_carrier(boole_POSet(X1)))
| ~ element(X0,the_carrier(boole_POSet(the_carrier(boole_POSet(X1))))) ),
inference(unflattening,[status(thm)],[c_7639]) ).
tcf(c_7651,plain,
! [X0: $i,X1: $i,X2: $i] :
( upper_relstr_subset(X2,X1)
| element(sK9(X1,X2),the_carrier(X1))
| ~ element(X2,the_carrier(boole_POSet(the_carrier(X1))))
| ( boole_POSet(X0) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_178,c_184]) ).
tcf(c_7652,plain,
! [X0: $i,X1: $i] :
( upper_relstr_subset(X0,boole_POSet(X1))
| element(sK9(boole_POSet(X1),X0),the_carrier(boole_POSet(X1)))
| ~ element(X0,the_carrier(boole_POSet(the_carrier(boole_POSet(X1))))) ),
inference(unflattening,[status(thm)],[c_7651]) ).
tcf(c_8941,plain,
! [X0: $i,X1: $i] :
( upper_relstr_subset(X1,boole_POSet(X0))
| subset(sK8(boole_POSet(X0),X1),sK9(boole_POSet(X0),X1))
| ~ element(X1,the_carrier(boole_POSet(the_carrier(boole_POSet(X0)))))
| ~ element(sK9(boole_POSet(X0),X1),the_carrier(boole_POSet(X0))) ),
inference(backward_subsumption_resolution,[status(thm)],[c_4204,c_7640]) ).
tcf(c_8946,plain,
! [X0: $i,X1: $i] :
( upper_relstr_subset(X0,boole_POSet(X1))
| subset(sK8(boole_POSet(X1),X0),sK9(boole_POSet(X1),X0))
| ~ element(X0,the_carrier(boole_POSet(the_carrier(boole_POSet(X1))))) ),
inference(backward_subsumption_resolution,[status(thm)],[c_8941,c_7652]) ).
tcf(c_11131,plain,
( subset(sK43,the_carrier(boole_POSet(sK42)))
| ~ element(sK43,the_carrier(boole_POSet(the_carrier(boole_POSet(sK42))))) ),
inference(instantiation,[status(thm)],[c_486]) ).
tcf(c_11134,plain,
( upper_relstr_subset(sK43,boole_POSet(sK42))
| element(sK9(boole_POSet(sK42),sK43),the_carrier(boole_POSet(sK42)))
| ~ rel_str(boole_POSet(sK42))
| ~ element(sK43,the_carrier(boole_POSet(the_carrier(boole_POSet(sK42))))) ),
inference(instantiation,[status(thm)],[c_178]) ).
tcf(c_11136,plain,
( upper_relstr_subset(sK43,boole_POSet(sK42))
| in(sK8(boole_POSet(sK42),sK43),sK43)
| ~ rel_str(boole_POSet(sK42))
| ~ element(sK43,the_carrier(boole_POSet(the_carrier(boole_POSet(sK42))))) ),
inference(instantiation,[status(thm)],[c_176]) ).
tcf(c_11151,plain,
( upper_relstr_subset(sK43,boole_POSet(sK42))
| subset(sK8(boole_POSet(sK42),sK43),sK9(boole_POSet(sK42),sK43))
| ~ element(sK43,the_carrier(boole_POSet(the_carrier(boole_POSet(sK42))))) ),
inference(instantiation,[status(thm)],[c_8946]) ).
tcf(c_11165,plain,
( element(sK45,the_carrier(boole_POSet(sK42)))
| ~ subset(sK45,sK42) ),
inference(instantiation,[status(thm)],[c_485]) ).
tcf(c_11205,plain,
rel_str(boole_POSet(sK42)),
inference(instantiation,[status(thm)],[c_184]) ).
tcf(c_11252,plain,
! [X0: $i] :
( element(sK44,X0)
| ~ in(sK44,sK43)
| ~ subset(sK43,X0) ),
inference(instantiation,[status(thm)],[c_1434]) ).
tcf(c_11448,plain,
( element(sK44,the_carrier(boole_POSet(sK42)))
| ~ in(sK44,sK43)
| ~ subset(sK43,the_carrier(boole_POSet(sK42))) ),
inference(instantiation,[status(thm)],[c_11252]) ).
tcf(c_11566,plain,
( subset(sK9(boole_POSet(sK42),sK43),sK42)
| ~ element(sK9(boole_POSet(sK42),sK43),the_carrier(boole_POSet(sK42))) ),
inference(instantiation,[status(thm)],[c_486]) ).
tcf(c_11871,plain,
( subset(sK44,sK42)
| ~ element(sK44,the_carrier(boole_POSet(sK42))) ),
inference(instantiation,[status(thm)],[c_486]) ).
tcf(c_12176,plain,
! [X0: $i] :
( upper_relstr_subset(sK43,boole_POSet(sK42))
| in(sK9(boole_POSet(sK42),sK43),sK43)
| ~ in(X0,sK43)
| ~ subset(sK9(boole_POSet(sK42),sK43),sK42)
| ~ subset(X0,sK9(boole_POSet(sK42),sK43)) ),
inference(instantiation,[status(thm)],[c_479]) ).
tcf(c_12178,plain,
! [X0: $i] :
( upper_relstr_subset(sK43,boole_POSet(sK42))
| in(sK9(boole_POSet(sK42),sK43),sK43)
| ~ in(X0,sK43)
| ~ subset(X0,sK9(boole_POSet(sK42),sK43)) ),
inference(global_subsumption_just,[status(thm)],[c_12176,c_480,c_11134,c_11205,c_11566,c_12176]) ).
tcf(c_12629,plain,
( upper_relstr_subset(sK43,boole_POSet(sK42))
| in(sK9(boole_POSet(sK42),sK43),sK43)
| ~ in(sK8(boole_POSet(sK42),sK43),sK43)
| ~ subset(sK8(boole_POSet(sK42),sK43),sK9(boole_POSet(sK42),sK43)) ),
inference(instantiation,[status(thm)],[c_12178]) ).
tcf(c_13373,plain,
( upper_relstr_subset(sK43,boole_POSet(sK42))
| ~ rel_str(boole_POSet(sK42))
| ~ in(sK9(boole_POSet(sK42),sK43),sK43)
| ~ element(sK43,the_carrier(boole_POSet(the_carrier(boole_POSet(sK42))))) ),
inference(instantiation,[status(thm)],[c_175]) ).
fof(f243,definition,
! [X0] :
( ~ sP7(X0)
| ( complete_relstr(boole_POSet(X0))
& with_infima_relstr(boole_POSet(X0))
& with_suprema_relstr(boole_POSet(X0))
& boolean_relstr(boole_POSet(X0))
& complemented_relstr(boole_POSet(X0))
& heyting_relstr(boole_POSet(X0))
& distributive_relstr(boole_POSet(X0))
& ~ v1_yellow_3(boole_POSet(X0))
& join_complete_relstr(boole_POSet(X0))
& up_complete_relstr(boole_POSet(X0))
& bounded_relstr(boole_POSet(X0))
& upper_bounded_relstr(boole_POSet(X0))
& lower_bounded_relstr(boole_POSet(X0))
& antisymmetric_relstr(boole_POSet(X0))
& transitive_relstr(boole_POSet(X0))
& reflexive_relstr(boole_POSet(X0))
& strict_rel_str(boole_POSet(X0))
& ~ trivial_carrier(boole_POSet(X0))
& ~ empty_carrier(boole_POSet(X0)) ) ),
introduced(definition,[new_symbols(definition,[sP7])],[predicate_definition_introduction]) ).
fof(f244,plain,
! [X0] :
( empty(X0)
| sP7(X0) ),
inference(definition_folding,[],[f198,f243]) ).
fof(f260,plain,
! [X0] :
( ~ sP7(X0)
| ( complete_relstr(boole_POSet(X0))
& with_infima_relstr(boole_POSet(X0))
& with_suprema_relstr(boole_POSet(X0))
& boolean_relstr(boole_POSet(X0))
& complemented_relstr(boole_POSet(X0))
& heyting_relstr(boole_POSet(X0))
& distributive_relstr(boole_POSet(X0))
& ~ v1_yellow_3(boole_POSet(X0))
& join_complete_relstr(boole_POSet(X0))
& up_complete_relstr(boole_POSet(X0))
& bounded_relstr(boole_POSet(X0))
& upper_bounded_relstr(boole_POSet(X0))
& lower_bounded_relstr(boole_POSet(X0))
& antisymmetric_relstr(boole_POSet(X0))
& transitive_relstr(boole_POSet(X0))
& reflexive_relstr(boole_POSet(X0))
& strict_rel_str(boole_POSet(X0))
& ~ trivial_carrier(boole_POSet(X0))
& ~ empty_carrier(boole_POSet(X0)) ) ),
inference(nnf_transformation,[],[f243]) ).
fof(f529,plain,
! [X0] :
( ~ sP7(X0)
| reflexive_relstr(boole_POSet(X0)) ),
inference(cnf_transformation,[],[f260]) ).
fof(f532,plain,
! [X0] :
( ~ sP7(X0)
| ~ empty_carrier(boole_POSet(X0)) ),
inference(cnf_transformation,[],[f260]) ).
tcf(c_230,plain,
! [X0: $i] :
( ~ sP7(X0)
| ~ empty_carrier(boole_POSet(X0)) ),
inference(cnf_transformation,[],[f532]) ).
tcf(c_233,plain,
! [X0: $i] :
( reflexive_relstr(boole_POSet(X0))
| ~ sP7(X0) ),
inference(cnf_transformation,[],[f529]) ).
tcf(c_615,plain,
! [X0: $i] : reflexive_relstr(boole_POSet(X0)),
inference(global_subsumption_just,[status(thm)],[c_233,c_269]) ).
tcf(c_621,plain,
! [X0: $i] : ~ empty_carrier(boole_POSet(X0)),
inference(global_subsumption_just,[status(thm)],[c_230,c_267]) ).
tcf(c_4245,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( in(X2,X0)
| ~ subset(X3,X2)
| ~ subset(X3,X1)
| ~ in(X3,X0)
| ~ upper_relstr_subset(X0,boole_POSet(X1))
| ~ element(X2,the_carrier(boole_POSet(X1)))
| ~ element(X0,the_carrier(boole_POSet(the_carrier(boole_POSet(X1))))) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4222,c_621,c_615,c_184,c_638]) ).
tcf(c_11589,plain,
! [X0: $i,X1: $i] :
( in(X1,sK43)
| ~ in(sK44,sK43)
| ~ subset(sK44,X1)
| ~ subset(sK44,X0)
| ~ upper_relstr_subset(sK43,boole_POSet(X0))
| ~ element(X1,the_carrier(boole_POSet(X0)))
| ~ element(sK43,the_carrier(boole_POSet(the_carrier(boole_POSet(X0))))) ),
inference(instantiation,[status(thm)],[c_4245]) ).
tcf(c_11670,plain,
! [X0: $i] :
( in(sK45,sK43)
| ~ subset(sK44,sK45)
| ~ in(sK44,sK43)
| ~ subset(sK44,X0)
| ~ upper_relstr_subset(sK43,boole_POSet(X0))
| ~ element(sK45,the_carrier(boole_POSet(X0)))
| ~ element(sK43,the_carrier(boole_POSet(the_carrier(boole_POSet(X0))))) ),
inference(instantiation,[status(thm)],[c_11589]) ).
tcf(c_12584,plain,
( in(sK45,sK43)
| ~ subset(sK44,sK42)
| ~ subset(sK44,sK45)
| ~ in(sK44,sK43)
| ~ upper_relstr_subset(sK43,boole_POSet(sK42))
| ~ element(sK45,the_carrier(boole_POSet(sK42)))
| ~ element(sK43,the_carrier(boole_POSet(the_carrier(boole_POSet(sK42))))) ),
inference(instantiation,[status(thm)],[c_11670]) ).
tcf(c_12585,plain,
~ upper_relstr_subset(sK43,boole_POSet(sK42)),
inference(global_subsumption_just,[status(thm)],[c_12584,c_480,c_478,c_477,c_476,c_475,c_11131,c_11165,c_11448,c_11871,c_12584]) ).
tcf(c_13374,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_13373,c_12629,c_12585,c_11205,c_11151,c_11136,c_480]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SEU381+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.05 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.13/5.42 % Computer : n001.cluster.edu
% 0.13/5.42 % Model : x86_64 x86_64
% 0.13/5.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/5.42 % Memory : 8046.5625MB
% 0.13/5.42 % OS : Linux 6.8.0-71-generic
% 0.13/5.42 % CPULimit : 300
% 0.13/5.42 % WCLimit : 300
% 0.13/5.42 % DateTime : Thu Sep 24 14:00:29 UTC 2026
% 0.13/5.42 % CPUTime :
% 0.13/5.42 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.13/5.47 Running first-order theorem proving
% 0.13/5.47 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.13/5.48
% 0.13/5.48 % ======== iProver multi-core TPTP/SMT =========
% 0.13/5.48
% 0.13/5.49 % Detected problem language: tptp
% 0.17/5.50 % Proving...
% 26.86/9.48 % SZS status Started for theBenchmark.p
% 26.86/9.48 % SZS status Theorem for theBenchmark.p
% 26.86/9.48
% 26.86/9.48 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 26.86/9.48
% 26.86/9.48 % ------ iProver source info
% 26.86/9.48
% 26.86/9.48 % git: date: 2026-07-19 20:42:38 +0200
% 26.86/9.48 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 26.86/9.48 % git: non_committed_changes: false
% 26.86/9.48
% 26.86/9.48 % ------ Parsing...
% 26.86/9.48 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 26.86/9.48
% 26.86/9.48 % ------ Preprocessing... sup_sim: 0 sf_s rm: 11 0s sf_e pe_s pe:1:0s pe:2:0s pe:4:0s pe:8:0s pe:16:0s pe_e %
% 26.86/9.48
% 26.86/9.48 % ------ Preprocessing... gs_s sp: 1 0s gs_e snvd_s sp: 0 0s snvd_e %
% 26.86/9.48
% 26.86/9.48 % ------ Preprocessing... sf_s rm: 59 0s sf_e
% 26.86/9.48 % ------ Proving...
% 26.86/9.48 % ------ Problem Properties
% 26.86/9.48
% 26.86/9.48 %
% 26.86/9.48 % clauses 316
% 26.86/9.48 % conjectures 6
% 26.86/9.48 % EPR 90
% 26.86/9.48 % Horn 304
% 26.86/9.48 % unary 203
% 26.86/9.48 % binary 81
% 26.86/9.48 % lits 491
% 26.86/9.48 % lits eq 67
% 26.86/9.48 % fd_pure 0
% 26.86/9.48 % fd_pseudo 0
% 26.86/9.48 % fd_cond 1
% 26.86/9.48 % fd_pseudo_cond 3
% 26.86/9.48 % AC symbols 0
% 26.86/9.48
% 26.86/9.48 % ------ Input Options Time Limit: Unbounded
% 26.86/9.48
% 26.86/9.48
% 26.86/9.48 % ------
% 26.86/9.48 % Current options:
% 26.86/9.48 % ------
% 26.86/9.48
% 26.86/9.48
% 26.86/9.48 %
% 26.86/9.48
% 26.86/9.48 % ------ Proving...
% 26.86/9.48 %
% 26.86/9.48
% 26.86/9.48 % SZS status Theorem for theBenchmark.p
% 26.86/9.48
% 26.86/9.48 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 26.86/9.48
% 26.86/9.48
%------------------------------------------------------------------------------