%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : SEU356+1 : TPTP v5.0.0. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : Source/sine.py -e eprover -t %d %s
% Computer : art03.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
% Memory : 2018MB
% OS : Linux 2.6.26.8-57.fc8
% CPULimit : 300s
% DateTime : Sun Dec 26 07:43:17 EST 2010
% Result : Theorem 0.19s
% Output : CNFRefutation 0.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 52
% Number of leaves : 3
% Syntax : Number of formulae : 155 ( 10 unt; 0 def)
% Number of atoms : 1084 ( 83 equ)
% Maximal formula atoms : 107 ( 6 avg)
% Number of connectives : 1535 ( 606 ~; 801 |; 108 &)
% ( 3 <=>; 17 =>; 0 <=; 0 <~>)
% Maximal formula depth : 28 ( 7 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-3 aty)
% Number of functors : 9 ( 9 usr; 3 con; 0-3 aty)
% Number of variables : 208 ( 0 sgn 63 !; 19 ?)
% Comments :
%------------------------------------------------------------------------------
fof(3,axiom,
! [X1] :
( ( antisymmetric_relstr(X1)
& rel_str(X1) )
=> ! [X2] :
( element(X2,the_carrier(X1))
=> ! [X3] :
( element(X3,the_carrier(X1))
=> ( ( related(X1,X2,X3)
& related(X1,X3,X2) )
=> X2 = X3 ) ) ) ),
file('/tmp/tmp3i-K86/sel_SEU356+1.p_1',t25_orders_2) ).
fof(6,conjecture,
! [X1] :
( ( antisymmetric_relstr(X1)
& rel_str(X1) )
=> ! [X2] :
( ex_sup_of_relstr_set(X1,X2)
<=> ? [X3] :
( element(X3,the_carrier(X1))
& relstr_set_smaller(X1,X2,X3)
& ! [X4] :
( element(X4,the_carrier(X1))
=> ( relstr_set_smaller(X1,X2,X4)
=> related(X1,X3,X4) ) ) ) ) ),
file('/tmp/tmp3i-K86/sel_SEU356+1.p_1',t15_yellow_0) ).
fof(8,axiom,
! [X1] :
( rel_str(X1)
=> ! [X2] :
( ex_sup_of_relstr_set(X1,X2)
<=> ? [X3] :
( element(X3,the_carrier(X1))
& relstr_set_smaller(X1,X2,X3)
& ! [X4] :
( element(X4,the_carrier(X1))
=> ( relstr_set_smaller(X1,X2,X4)
=> related(X1,X3,X4) ) )
& ! [X4] :
( element(X4,the_carrier(X1))
=> ( ( relstr_set_smaller(X1,X2,X4)
& ! [X5] :
( element(X5,the_carrier(X1))
=> ( relstr_set_smaller(X1,X2,X5)
=> related(X1,X4,X5) ) ) )
=> X4 = X3 ) ) ) ) ),
file('/tmp/tmp3i-K86/sel_SEU356+1.p_1',d7_yellow_0) ).
fof(11,negated_conjecture,
~ ! [X1] :
( ( antisymmetric_relstr(X1)
& rel_str(X1) )
=> ! [X2] :
( ex_sup_of_relstr_set(X1,X2)
<=> ? [X3] :
( element(X3,the_carrier(X1))
& relstr_set_smaller(X1,X2,X3)
& ! [X4] :
( element(X4,the_carrier(X1))
=> ( relstr_set_smaller(X1,X2,X4)
=> related(X1,X3,X4) ) ) ) ) ),
inference(assume_negation,[status(cth)],[6]) ).
fof(16,plain,
! [X1] :
( ~ antisymmetric_relstr(X1)
| ~ rel_str(X1)
| ! [X2] :
( ~ element(X2,the_carrier(X1))
| ! [X3] :
( ~ element(X3,the_carrier(X1))
| ~ related(X1,X2,X3)
| ~ related(X1,X3,X2)
| X2 = X3 ) ) ),
inference(fof_nnf,[status(thm)],[3]) ).
fof(17,plain,
! [X4] :
( ~ antisymmetric_relstr(X4)
| ~ rel_str(X4)
| ! [X5] :
( ~ element(X5,the_carrier(X4))
| ! [X6] :
( ~ element(X6,the_carrier(X4))
| ~ related(X4,X5,X6)
| ~ related(X4,X6,X5)
| X5 = X6 ) ) ),
inference(variable_rename,[status(thm)],[16]) ).
fof(18,plain,
! [X4,X5,X6] :
( ~ element(X6,the_carrier(X4))
| ~ related(X4,X5,X6)
| ~ related(X4,X6,X5)
| X5 = X6
| ~ element(X5,the_carrier(X4))
| ~ antisymmetric_relstr(X4)
| ~ rel_str(X4) ),
inference(shift_quantors,[status(thm)],[17]) ).
cnf(19,plain,
( X2 = X3
| ~ rel_str(X1)
| ~ antisymmetric_relstr(X1)
| ~ element(X2,the_carrier(X1))
| ~ related(X1,X3,X2)
| ~ related(X1,X2,X3)
| ~ element(X3,the_carrier(X1)) ),
inference(split_conjunct,[status(thm)],[18]) ).
fof(26,negated_conjecture,
? [X1] :
( antisymmetric_relstr(X1)
& rel_str(X1)
& ? [X2] :
( ( ~ ex_sup_of_relstr_set(X1,X2)
| ! [X3] :
( ~ element(X3,the_carrier(X1))
| ~ relstr_set_smaller(X1,X2,X3)
| ? [X4] :
( element(X4,the_carrier(X1))
& relstr_set_smaller(X1,X2,X4)
& ~ related(X1,X3,X4) ) ) )
& ( ex_sup_of_relstr_set(X1,X2)
| ? [X3] :
( element(X3,the_carrier(X1))
& relstr_set_smaller(X1,X2,X3)
& ! [X4] :
( ~ element(X4,the_carrier(X1))
| ~ relstr_set_smaller(X1,X2,X4)
| related(X1,X3,X4) ) ) ) ) ),
inference(fof_nnf,[status(thm)],[11]) ).
fof(27,negated_conjecture,
? [X5] :
( antisymmetric_relstr(X5)
& rel_str(X5)
& ? [X6] :
( ( ~ ex_sup_of_relstr_set(X5,X6)
| ! [X7] :
( ~ element(X7,the_carrier(X5))
| ~ relstr_set_smaller(X5,X6,X7)
| ? [X8] :
( element(X8,the_carrier(X5))
& relstr_set_smaller(X5,X6,X8)
& ~ related(X5,X7,X8) ) ) )
& ( ex_sup_of_relstr_set(X5,X6)
| ? [X9] :
( element(X9,the_carrier(X5))
& relstr_set_smaller(X5,X6,X9)
& ! [X10] :
( ~ element(X10,the_carrier(X5))
| ~ relstr_set_smaller(X5,X6,X10)
| related(X5,X9,X10) ) ) ) ) ),
inference(variable_rename,[status(thm)],[26]) ).
fof(28,negated_conjecture,
( antisymmetric_relstr(esk3_0)
& rel_str(esk3_0)
& ( ~ ex_sup_of_relstr_set(esk3_0,esk4_0)
| ! [X7] :
( ~ element(X7,the_carrier(esk3_0))
| ~ relstr_set_smaller(esk3_0,esk4_0,X7)
| ( element(esk5_1(X7),the_carrier(esk3_0))
& relstr_set_smaller(esk3_0,esk4_0,esk5_1(X7))
& ~ related(esk3_0,X7,esk5_1(X7)) ) ) )
& ( ex_sup_of_relstr_set(esk3_0,esk4_0)
| ( element(esk6_0,the_carrier(esk3_0))
& relstr_set_smaller(esk3_0,esk4_0,esk6_0)
& ! [X10] :
( ~ element(X10,the_carrier(esk3_0))
| ~ relstr_set_smaller(esk3_0,esk4_0,X10)
| related(esk3_0,esk6_0,X10) ) ) ) ),
inference(skolemize,[status(esa)],[27]) ).
fof(29,negated_conjecture,
! [X7,X10] :
( ( ( ( ~ element(X10,the_carrier(esk3_0))
| ~ relstr_set_smaller(esk3_0,esk4_0,X10)
| related(esk3_0,esk6_0,X10) )
& element(esk6_0,the_carrier(esk3_0))
& relstr_set_smaller(esk3_0,esk4_0,esk6_0) )
| ex_sup_of_relstr_set(esk3_0,esk4_0) )
& ( ~ element(X7,the_carrier(esk3_0))
| ~ relstr_set_smaller(esk3_0,esk4_0,X7)
| ( element(esk5_1(X7),the_carrier(esk3_0))
& relstr_set_smaller(esk3_0,esk4_0,esk5_1(X7))
& ~ related(esk3_0,X7,esk5_1(X7)) )
| ~ ex_sup_of_relstr_set(esk3_0,esk4_0) )
& antisymmetric_relstr(esk3_0)
& rel_str(esk3_0) ),
inference(shift_quantors,[status(thm)],[28]) ).
fof(30,negated_conjecture,
! [X7,X10] :
( ( ~ element(X10,the_carrier(esk3_0))
| ~ relstr_set_smaller(esk3_0,esk4_0,X10)
| related(esk3_0,esk6_0,X10)
| ex_sup_of_relstr_set(esk3_0,esk4_0) )
& ( element(esk6_0,the_carrier(esk3_0))
| ex_sup_of_relstr_set(esk3_0,esk4_0) )
& ( relstr_set_smaller(esk3_0,esk4_0,esk6_0)
| ex_sup_of_relstr_set(esk3_0,esk4_0) )
& ( element(esk5_1(X7),the_carrier(esk3_0))
| ~ element(X7,the_carrier(esk3_0))
| ~ relstr_set_smaller(esk3_0,esk4_0,X7)
| ~ ex_sup_of_relstr_set(esk3_0,esk4_0) )
& ( relstr_set_smaller(esk3_0,esk4_0,esk5_1(X7))
| ~ element(X7,the_carrier(esk3_0))
| ~ relstr_set_smaller(esk3_0,esk4_0,X7)
| ~ ex_sup_of_relstr_set(esk3_0,esk4_0) )
& ( ~ related(esk3_0,X7,esk5_1(X7))
| ~ element(X7,the_carrier(esk3_0))
| ~ relstr_set_smaller(esk3_0,esk4_0,X7)
| ~ ex_sup_of_relstr_set(esk3_0,esk4_0) )
& antisymmetric_relstr(esk3_0)
& rel_str(esk3_0) ),
inference(distribute,[status(thm)],[29]) ).
cnf(31,negated_conjecture,
rel_str(esk3_0),
inference(split_conjunct,[status(thm)],[30]) ).
cnf(32,negated_conjecture,
antisymmetric_relstr(esk3_0),
inference(split_conjunct,[status(thm)],[30]) ).
cnf(33,negated_conjecture,
( ~ ex_sup_of_relstr_set(esk3_0,esk4_0)
| ~ relstr_set_smaller(esk3_0,esk4_0,X1)
| ~ element(X1,the_carrier(esk3_0))
| ~ related(esk3_0,X1,esk5_1(X1)) ),
inference(split_conjunct,[status(thm)],[30]) ).
cnf(34,negated_conjecture,
( relstr_set_smaller(esk3_0,esk4_0,esk5_1(X1))
| ~ ex_sup_of_relstr_set(esk3_0,esk4_0)
| ~ relstr_set_smaller(esk3_0,esk4_0,X1)
| ~ element(X1,the_carrier(esk3_0)) ),
inference(split_conjunct,[status(thm)],[30]) ).
cnf(35,negated_conjecture,
( element(esk5_1(X1),the_carrier(esk3_0))
| ~ ex_sup_of_relstr_set(esk3_0,esk4_0)
| ~ relstr_set_smaller(esk3_0,esk4_0,X1)
| ~ element(X1,the_carrier(esk3_0)) ),
inference(split_conjunct,[status(thm)],[30]) ).
cnf(36,negated_conjecture,
( ex_sup_of_relstr_set(esk3_0,esk4_0)
| relstr_set_smaller(esk3_0,esk4_0,esk6_0) ),
inference(split_conjunct,[status(thm)],[30]) ).
cnf(37,negated_conjecture,
( ex_sup_of_relstr_set(esk3_0,esk4_0)
| element(esk6_0,the_carrier(esk3_0)) ),
inference(split_conjunct,[status(thm)],[30]) ).
cnf(38,negated_conjecture,
( ex_sup_of_relstr_set(esk3_0,esk4_0)
| related(esk3_0,esk6_0,X1)
| ~ relstr_set_smaller(esk3_0,esk4_0,X1)
| ~ element(X1,the_carrier(esk3_0)) ),
inference(split_conjunct,[status(thm)],[30]) ).
fof(40,plain,
! [X1] :
( ~ rel_str(X1)
| ! [X2] :
( ( ~ ex_sup_of_relstr_set(X1,X2)
| ? [X3] :
( element(X3,the_carrier(X1))
& relstr_set_smaller(X1,X2,X3)
& ! [X4] :
( ~ element(X4,the_carrier(X1))
| ~ relstr_set_smaller(X1,X2,X4)
| related(X1,X3,X4) )
& ! [X4] :
( ~ element(X4,the_carrier(X1))
| ~ relstr_set_smaller(X1,X2,X4)
| ? [X5] :
( element(X5,the_carrier(X1))
& relstr_set_smaller(X1,X2,X5)
& ~ related(X1,X4,X5) )
| X4 = X3 ) ) )
& ( ! [X3] :
( ~ element(X3,the_carrier(X1))
| ~ relstr_set_smaller(X1,X2,X3)
| ? [X4] :
( element(X4,the_carrier(X1))
& relstr_set_smaller(X1,X2,X4)
& ~ related(X1,X3,X4) )
| ? [X4] :
( element(X4,the_carrier(X1))
& relstr_set_smaller(X1,X2,X4)
& ! [X5] :
( ~ element(X5,the_carrier(X1))
| ~ relstr_set_smaller(X1,X2,X5)
| related(X1,X4,X5) )
& X4 != X3 ) )
| ex_sup_of_relstr_set(X1,X2) ) ) ),
inference(fof_nnf,[status(thm)],[8]) ).
fof(41,plain,
! [X6] :
( ~ rel_str(X6)
| ! [X7] :
( ( ~ ex_sup_of_relstr_set(X6,X7)
| ? [X8] :
( element(X8,the_carrier(X6))
& relstr_set_smaller(X6,X7,X8)
& ! [X9] :
( ~ element(X9,the_carrier(X6))
| ~ relstr_set_smaller(X6,X7,X9)
| related(X6,X8,X9) )
& ! [X10] :
( ~ element(X10,the_carrier(X6))
| ~ relstr_set_smaller(X6,X7,X10)
| ? [X11] :
( element(X11,the_carrier(X6))
& relstr_set_smaller(X6,X7,X11)
& ~ related(X6,X10,X11) )
| X10 = X8 ) ) )
& ( ! [X12] :
( ~ element(X12,the_carrier(X6))
| ~ relstr_set_smaller(X6,X7,X12)
| ? [X13] :
( element(X13,the_carrier(X6))
& relstr_set_smaller(X6,X7,X13)
& ~ related(X6,X12,X13) )
| ? [X14] :
( element(X14,the_carrier(X6))
& relstr_set_smaller(X6,X7,X14)
& ! [X15] :
( ~ element(X15,the_carrier(X6))
| ~ relstr_set_smaller(X6,X7,X15)
| related(X6,X14,X15) )
& X14 != X12 ) )
| ex_sup_of_relstr_set(X6,X7) ) ) ),
inference(variable_rename,[status(thm)],[40]) ).
fof(42,plain,
! [X6] :
( ~ rel_str(X6)
| ! [X7] :
( ( ~ ex_sup_of_relstr_set(X6,X7)
| ( element(esk7_2(X6,X7),the_carrier(X6))
& relstr_set_smaller(X6,X7,esk7_2(X6,X7))
& ! [X9] :
( ~ element(X9,the_carrier(X6))
| ~ relstr_set_smaller(X6,X7,X9)
| related(X6,esk7_2(X6,X7),X9) )
& ! [X10] :
( ~ element(X10,the_carrier(X6))
| ~ relstr_set_smaller(X6,X7,X10)
| ( element(esk8_3(X6,X7,X10),the_carrier(X6))
& relstr_set_smaller(X6,X7,esk8_3(X6,X7,X10))
& ~ related(X6,X10,esk8_3(X6,X7,X10)) )
| X10 = esk7_2(X6,X7) ) ) )
& ( ! [X12] :
( ~ element(X12,the_carrier(X6))
| ~ relstr_set_smaller(X6,X7,X12)
| ( element(esk9_3(X6,X7,X12),the_carrier(X6))
& relstr_set_smaller(X6,X7,esk9_3(X6,X7,X12))
& ~ related(X6,X12,esk9_3(X6,X7,X12)) )
| ( element(esk10_3(X6,X7,X12),the_carrier(X6))
& relstr_set_smaller(X6,X7,esk10_3(X6,X7,X12))
& ! [X15] :
( ~ element(X15,the_carrier(X6))
| ~ relstr_set_smaller(X6,X7,X15)
| related(X6,esk10_3(X6,X7,X12),X15) )
& esk10_3(X6,X7,X12) != X12 ) )
| ex_sup_of_relstr_set(X6,X7) ) ) ),
inference(skolemize,[status(esa)],[41]) ).
fof(43,plain,
! [X6,X7,X9,X10,X12,X15] :
( ( ( ( ( ~ element(X15,the_carrier(X6))
| ~ relstr_set_smaller(X6,X7,X15)
| related(X6,esk10_3(X6,X7,X12),X15) )
& relstr_set_smaller(X6,X7,esk10_3(X6,X7,X12))
& esk10_3(X6,X7,X12) != X12
& element(esk10_3(X6,X7,X12),the_carrier(X6)) )
| ~ element(X12,the_carrier(X6))
| ~ relstr_set_smaller(X6,X7,X12)
| ( element(esk9_3(X6,X7,X12),the_carrier(X6))
& relstr_set_smaller(X6,X7,esk9_3(X6,X7,X12))
& ~ related(X6,X12,esk9_3(X6,X7,X12)) )
| ex_sup_of_relstr_set(X6,X7) )
& ( ( ( ~ element(X10,the_carrier(X6))
| ~ relstr_set_smaller(X6,X7,X10)
| ( element(esk8_3(X6,X7,X10),the_carrier(X6))
& relstr_set_smaller(X6,X7,esk8_3(X6,X7,X10))
& ~ related(X6,X10,esk8_3(X6,X7,X10)) )
| X10 = esk7_2(X6,X7) )
& ( ~ element(X9,the_carrier(X6))
| ~ relstr_set_smaller(X6,X7,X9)
| related(X6,esk7_2(X6,X7),X9) )
& element(esk7_2(X6,X7),the_carrier(X6))
& relstr_set_smaller(X6,X7,esk7_2(X6,X7)) )
| ~ ex_sup_of_relstr_set(X6,X7) ) )
| ~ rel_str(X6) ),
inference(shift_quantors,[status(thm)],[42]) ).
fof(44,plain,
! [X6,X7,X9,X10,X12,X15] :
( ( element(esk9_3(X6,X7,X12),the_carrier(X6))
| ~ element(X12,the_carrier(X6))
| ~ relstr_set_smaller(X6,X7,X12)
| ~ element(X15,the_carrier(X6))
| ~ relstr_set_smaller(X6,X7,X15)
| related(X6,esk10_3(X6,X7,X12),X15)
| ex_sup_of_relstr_set(X6,X7)
| ~ rel_str(X6) )
& ( relstr_set_smaller(X6,X7,esk9_3(X6,X7,X12))
| ~ element(X12,the_carrier(X6))
| ~ relstr_set_smaller(X6,X7,X12)
| ~ element(X15,the_carrier(X6))
| ~ relstr_set_smaller(X6,X7,X15)
| related(X6,esk10_3(X6,X7,X12),X15)
| ex_sup_of_relstr_set(X6,X7)
| ~ rel_str(X6) )
& ( ~ related(X6,X12,esk9_3(X6,X7,X12))
| ~ element(X12,the_carrier(X6))
| ~ relstr_set_smaller(X6,X7,X12)
| ~ element(X15,the_carrier(X6))
| ~ relstr_set_smaller(X6,X7,X15)
| related(X6,esk10_3(X6,X7,X12),X15)
| ex_sup_of_relstr_set(X6,X7)
| ~ rel_str(X6) )
& ( element(esk9_3(X6,X7,X12),the_carrier(X6))
| ~ element(X12,the_carrier(X6))
| ~ relstr_set_smaller(X6,X7,X12)
| relstr_set_smaller(X6,X7,esk10_3(X6,X7,X12))
| ex_sup_of_relstr_set(X6,X7)
| ~ rel_str(X6) )
& ( relstr_set_smaller(X6,X7,esk9_3(X6,X7,X12))
| ~ element(X12,the_carrier(X6))
| ~ relstr_set_smaller(X6,X7,X12)
| relstr_set_smaller(X6,X7,esk10_3(X6,X7,X12))
| ex_sup_of_relstr_set(X6,X7)
| ~ rel_str(X6) )
& ( ~ related(X6,X12,esk9_3(X6,X7,X12))
| ~ element(X12,the_carrier(X6))
| ~ relstr_set_smaller(X6,X7,X12)
| relstr_set_smaller(X6,X7,esk10_3(X6,X7,X12))
| ex_sup_of_relstr_set(X6,X7)
| ~ rel_str(X6) )
& ( element(esk9_3(X6,X7,X12),the_carrier(X6))
| ~ element(X12,the_carrier(X6))
| ~ relstr_set_smaller(X6,X7,X12)
| esk10_3(X6,X7,X12) != X12
| ex_sup_of_relstr_set(X6,X7)
| ~ rel_str(X6) )
& ( relstr_set_smaller(X6,X7,esk9_3(X6,X7,X12))
| ~ element(X12,the_carrier(X6))
| ~ relstr_set_smaller(X6,X7,X12)
| esk10_3(X6,X7,X12) != X12
| ex_sup_of_relstr_set(X6,X7)
| ~ rel_str(X6) )
& ( ~ related(X6,X12,esk9_3(X6,X7,X12))
| ~ element(X12,the_carrier(X6))
| ~ relstr_set_smaller(X6,X7,X12)
| esk10_3(X6,X7,X12) != X12
| ex_sup_of_relstr_set(X6,X7)
| ~ rel_str(X6) )
& ( element(esk9_3(X6,X7,X12),the_carrier(X6))
| ~ element(X12,the_carrier(X6))
| ~ relstr_set_smaller(X6,X7,X12)
| element(esk10_3(X6,X7,X12),the_carrier(X6))
| ex_sup_of_relstr_set(X6,X7)
| ~ rel_str(X6) )
& ( relstr_set_smaller(X6,X7,esk9_3(X6,X7,X12))
| ~ element(X12,the_carrier(X6))
| ~ relstr_set_smaller(X6,X7,X12)
| element(esk10_3(X6,X7,X12),the_carrier(X6))
| ex_sup_of_relstr_set(X6,X7)
| ~ rel_str(X6) )
& ( ~ related(X6,X12,esk9_3(X6,X7,X12))
| ~ element(X12,the_carrier(X6))
| ~ relstr_set_smaller(X6,X7,X12)
| element(esk10_3(X6,X7,X12),the_carrier(X6))
| ex_sup_of_relstr_set(X6,X7)
| ~ rel_str(X6) )
& ( element(esk8_3(X6,X7,X10),the_carrier(X6))
| ~ relstr_set_smaller(X6,X7,X10)
| X10 = esk7_2(X6,X7)
| ~ element(X10,the_carrier(X6))
| ~ ex_sup_of_relstr_set(X6,X7)
| ~ rel_str(X6) )
& ( relstr_set_smaller(X6,X7,esk8_3(X6,X7,X10))
| ~ relstr_set_smaller(X6,X7,X10)
| X10 = esk7_2(X6,X7)
| ~ element(X10,the_carrier(X6))
| ~ ex_sup_of_relstr_set(X6,X7)
| ~ rel_str(X6) )
& ( ~ related(X6,X10,esk8_3(X6,X7,X10))
| ~ relstr_set_smaller(X6,X7,X10)
| X10 = esk7_2(X6,X7)
| ~ element(X10,the_carrier(X6))
| ~ ex_sup_of_relstr_set(X6,X7)
| ~ rel_str(X6) )
& ( ~ element(X9,the_carrier(X6))
| ~ relstr_set_smaller(X6,X7,X9)
| related(X6,esk7_2(X6,X7),X9)
| ~ ex_sup_of_relstr_set(X6,X7)
| ~ rel_str(X6) )
& ( element(esk7_2(X6,X7),the_carrier(X6))
| ~ ex_sup_of_relstr_set(X6,X7)
| ~ rel_str(X6) )
& ( relstr_set_smaller(X6,X7,esk7_2(X6,X7))
| ~ ex_sup_of_relstr_set(X6,X7)
| ~ rel_str(X6) ) ),
inference(distribute,[status(thm)],[43]) ).
cnf(45,plain,
( relstr_set_smaller(X1,X2,esk7_2(X1,X2))
| ~ rel_str(X1)
| ~ ex_sup_of_relstr_set(X1,X2) ),
inference(split_conjunct,[status(thm)],[44]) ).
cnf(46,plain,
( element(esk7_2(X1,X2),the_carrier(X1))
| ~ rel_str(X1)
| ~ ex_sup_of_relstr_set(X1,X2) ),
inference(split_conjunct,[status(thm)],[44]) ).
cnf(47,plain,
( related(X1,esk7_2(X1,X2),X3)
| ~ rel_str(X1)
| ~ ex_sup_of_relstr_set(X1,X2)
| ~ relstr_set_smaller(X1,X2,X3)
| ~ element(X3,the_carrier(X1)) ),
inference(split_conjunct,[status(thm)],[44]) ).
cnf(51,plain,
( ex_sup_of_relstr_set(X1,X2)
| element(esk10_3(X1,X2,X3),the_carrier(X1))
| ~ rel_str(X1)
| ~ relstr_set_smaller(X1,X2,X3)
| ~ element(X3,the_carrier(X1))
| ~ related(X1,X3,esk9_3(X1,X2,X3)) ),
inference(split_conjunct,[status(thm)],[44]) ).
cnf(52,plain,
( ex_sup_of_relstr_set(X1,X2)
| element(esk10_3(X1,X2,X3),the_carrier(X1))
| relstr_set_smaller(X1,X2,esk9_3(X1,X2,X3))
| ~ rel_str(X1)
| ~ relstr_set_smaller(X1,X2,X3)
| ~ element(X3,the_carrier(X1)) ),
inference(split_conjunct,[status(thm)],[44]) ).
cnf(53,plain,
( ex_sup_of_relstr_set(X1,X2)
| element(esk10_3(X1,X2,X3),the_carrier(X1))
| element(esk9_3(X1,X2,X3),the_carrier(X1))
| ~ rel_str(X1)
| ~ relstr_set_smaller(X1,X2,X3)
| ~ element(X3,the_carrier(X1)) ),
inference(split_conjunct,[status(thm)],[44]) ).
cnf(54,plain,
( ex_sup_of_relstr_set(X1,X2)
| ~ rel_str(X1)
| esk10_3(X1,X2,X3) != X3
| ~ relstr_set_smaller(X1,X2,X3)
| ~ element(X3,the_carrier(X1))
| ~ related(X1,X3,esk9_3(X1,X2,X3)) ),
inference(split_conjunct,[status(thm)],[44]) ).
cnf(55,plain,
( ex_sup_of_relstr_set(X1,X2)
| relstr_set_smaller(X1,X2,esk9_3(X1,X2,X3))
| ~ rel_str(X1)
| esk10_3(X1,X2,X3) != X3
| ~ relstr_set_smaller(X1,X2,X3)
| ~ element(X3,the_carrier(X1)) ),
inference(split_conjunct,[status(thm)],[44]) ).
cnf(56,plain,
( ex_sup_of_relstr_set(X1,X2)
| element(esk9_3(X1,X2,X3),the_carrier(X1))
| ~ rel_str(X1)
| esk10_3(X1,X2,X3) != X3
| ~ relstr_set_smaller(X1,X2,X3)
| ~ element(X3,the_carrier(X1)) ),
inference(split_conjunct,[status(thm)],[44]) ).
cnf(57,plain,
( ex_sup_of_relstr_set(X1,X2)
| relstr_set_smaller(X1,X2,esk10_3(X1,X2,X3))
| ~ rel_str(X1)
| ~ relstr_set_smaller(X1,X2,X3)
| ~ element(X3,the_carrier(X1))
| ~ related(X1,X3,esk9_3(X1,X2,X3)) ),
inference(split_conjunct,[status(thm)],[44]) ).
cnf(58,plain,
( ex_sup_of_relstr_set(X1,X2)
| relstr_set_smaller(X1,X2,esk10_3(X1,X2,X3))
| relstr_set_smaller(X1,X2,esk9_3(X1,X2,X3))
| ~ rel_str(X1)
| ~ relstr_set_smaller(X1,X2,X3)
| ~ element(X3,the_carrier(X1)) ),
inference(split_conjunct,[status(thm)],[44]) ).
cnf(59,plain,
( ex_sup_of_relstr_set(X1,X2)
| relstr_set_smaller(X1,X2,esk10_3(X1,X2,X3))
| element(esk9_3(X1,X2,X3),the_carrier(X1))
| ~ rel_str(X1)
| ~ relstr_set_smaller(X1,X2,X3)
| ~ element(X3,the_carrier(X1)) ),
inference(split_conjunct,[status(thm)],[44]) ).
cnf(60,plain,
( ex_sup_of_relstr_set(X1,X2)
| related(X1,esk10_3(X1,X2,X3),X4)
| ~ rel_str(X1)
| ~ relstr_set_smaller(X1,X2,X4)
| ~ element(X4,the_carrier(X1))
| ~ relstr_set_smaller(X1,X2,X3)
| ~ element(X3,the_carrier(X1))
| ~ related(X1,X3,esk9_3(X1,X2,X3)) ),
inference(split_conjunct,[status(thm)],[44]) ).
cnf(61,plain,
( ex_sup_of_relstr_set(X1,X2)
| related(X1,esk10_3(X1,X2,X3),X4)
| relstr_set_smaller(X1,X2,esk9_3(X1,X2,X3))
| ~ rel_str(X1)
| ~ relstr_set_smaller(X1,X2,X4)
| ~ element(X4,the_carrier(X1))
| ~ relstr_set_smaller(X1,X2,X3)
| ~ element(X3,the_carrier(X1)) ),
inference(split_conjunct,[status(thm)],[44]) ).
cnf(62,plain,
( ex_sup_of_relstr_set(X1,X2)
| related(X1,esk10_3(X1,X2,X3),X4)
| element(esk9_3(X1,X2,X3),the_carrier(X1))
| ~ rel_str(X1)
| ~ relstr_set_smaller(X1,X2,X4)
| ~ element(X4,the_carrier(X1))
| ~ relstr_set_smaller(X1,X2,X3)
| ~ element(X3,the_carrier(X1)) ),
inference(split_conjunct,[status(thm)],[44]) ).
cnf(67,negated_conjecture,
( X1 = esk6_0
| ex_sup_of_relstr_set(esk3_0,esk4_0)
| ~ related(esk3_0,X1,esk6_0)
| ~ element(esk6_0,the_carrier(esk3_0))
| ~ element(X1,the_carrier(esk3_0))
| ~ rel_str(esk3_0)
| ~ antisymmetric_relstr(esk3_0)
| ~ relstr_set_smaller(esk3_0,esk4_0,X1) ),
inference(spm,[status(thm)],[19,38,theory(equality)]) ).
cnf(69,negated_conjecture,
( X1 = esk6_0
| ex_sup_of_relstr_set(esk3_0,esk4_0)
| ~ related(esk3_0,X1,esk6_0)
| ~ element(esk6_0,the_carrier(esk3_0))
| ~ element(X1,the_carrier(esk3_0))
| $false
| ~ antisymmetric_relstr(esk3_0)
| ~ relstr_set_smaller(esk3_0,esk4_0,X1) ),
inference(rw,[status(thm)],[67,31,theory(equality)]) ).
cnf(70,negated_conjecture,
( X1 = esk6_0
| ex_sup_of_relstr_set(esk3_0,esk4_0)
| ~ related(esk3_0,X1,esk6_0)
| ~ element(esk6_0,the_carrier(esk3_0))
| ~ element(X1,the_carrier(esk3_0))
| $false
| $false
| ~ relstr_set_smaller(esk3_0,esk4_0,X1) ),
inference(rw,[status(thm)],[69,32,theory(equality)]) ).
cnf(71,negated_conjecture,
( X1 = esk6_0
| ex_sup_of_relstr_set(esk3_0,esk4_0)
| ~ related(esk3_0,X1,esk6_0)
| ~ element(esk6_0,the_carrier(esk3_0))
| ~ element(X1,the_carrier(esk3_0))
| ~ relstr_set_smaller(esk3_0,esk4_0,X1) ),
inference(cn,[status(thm)],[70,theory(equality)]) ).
cnf(73,negated_conjecture,
( ~ relstr_set_smaller(esk3_0,esk4_0,esk7_2(esk3_0,X1))
| ~ ex_sup_of_relstr_set(esk3_0,esk4_0)
| ~ element(esk7_2(esk3_0,X1),the_carrier(esk3_0))
| ~ relstr_set_smaller(esk3_0,X1,esk5_1(esk7_2(esk3_0,X1)))
| ~ ex_sup_of_relstr_set(esk3_0,X1)
| ~ element(esk5_1(esk7_2(esk3_0,X1)),the_carrier(esk3_0))
| ~ rel_str(esk3_0) ),
inference(spm,[status(thm)],[33,47,theory(equality)]) ).
cnf(74,negated_conjecture,
( ~ relstr_set_smaller(esk3_0,esk4_0,esk7_2(esk3_0,X1))
| ~ ex_sup_of_relstr_set(esk3_0,esk4_0)
| ~ element(esk7_2(esk3_0,X1),the_carrier(esk3_0))
| ~ relstr_set_smaller(esk3_0,X1,esk5_1(esk7_2(esk3_0,X1)))
| ~ ex_sup_of_relstr_set(esk3_0,X1)
| ~ element(esk5_1(esk7_2(esk3_0,X1)),the_carrier(esk3_0))
| $false ),
inference(rw,[status(thm)],[73,31,theory(equality)]) ).
cnf(75,negated_conjecture,
( ~ relstr_set_smaller(esk3_0,esk4_0,esk7_2(esk3_0,X1))
| ~ ex_sup_of_relstr_set(esk3_0,esk4_0)
| ~ element(esk7_2(esk3_0,X1),the_carrier(esk3_0))
| ~ relstr_set_smaller(esk3_0,X1,esk5_1(esk7_2(esk3_0,X1)))
| ~ ex_sup_of_relstr_set(esk3_0,X1)
| ~ element(esk5_1(esk7_2(esk3_0,X1)),the_carrier(esk3_0)) ),
inference(cn,[status(thm)],[74,theory(equality)]) ).
cnf(80,negated_conjecture,
( ex_sup_of_relstr_set(esk3_0,X1)
| ex_sup_of_relstr_set(esk3_0,esk4_0)
| esk10_3(esk3_0,X1,esk6_0) != esk6_0
| ~ relstr_set_smaller(esk3_0,X1,esk6_0)
| ~ element(esk6_0,the_carrier(esk3_0))
| ~ rel_str(esk3_0)
| ~ relstr_set_smaller(esk3_0,esk4_0,esk9_3(esk3_0,X1,esk6_0))
| ~ element(esk9_3(esk3_0,X1,esk6_0),the_carrier(esk3_0)) ),
inference(spm,[status(thm)],[54,38,theory(equality)]) ).
cnf(82,negated_conjecture,
( ex_sup_of_relstr_set(esk3_0,X1)
| ex_sup_of_relstr_set(esk3_0,esk4_0)
| esk10_3(esk3_0,X1,esk6_0) != esk6_0
| ~ relstr_set_smaller(esk3_0,X1,esk6_0)
| ~ element(esk6_0,the_carrier(esk3_0))
| $false
| ~ relstr_set_smaller(esk3_0,esk4_0,esk9_3(esk3_0,X1,esk6_0))
| ~ element(esk9_3(esk3_0,X1,esk6_0),the_carrier(esk3_0)) ),
inference(rw,[status(thm)],[80,31,theory(equality)]) ).
cnf(83,negated_conjecture,
( ex_sup_of_relstr_set(esk3_0,X1)
| ex_sup_of_relstr_set(esk3_0,esk4_0)
| esk10_3(esk3_0,X1,esk6_0) != esk6_0
| ~ relstr_set_smaller(esk3_0,X1,esk6_0)
| ~ element(esk6_0,the_carrier(esk3_0))
| ~ relstr_set_smaller(esk3_0,esk4_0,esk9_3(esk3_0,X1,esk6_0))
| ~ element(esk9_3(esk3_0,X1,esk6_0),the_carrier(esk3_0)) ),
inference(cn,[status(thm)],[82,theory(equality)]) ).
cnf(84,negated_conjecture,
( ex_sup_of_relstr_set(esk3_0,X1)
| element(esk10_3(esk3_0,X1,esk6_0),the_carrier(esk3_0))
| ex_sup_of_relstr_set(esk3_0,esk4_0)
| ~ relstr_set_smaller(esk3_0,X1,esk6_0)
| ~ element(esk6_0,the_carrier(esk3_0))
| ~ rel_str(esk3_0)
| ~ relstr_set_smaller(esk3_0,esk4_0,esk9_3(esk3_0,X1,esk6_0))
| ~ element(esk9_3(esk3_0,X1,esk6_0),the_carrier(esk3_0)) ),
inference(spm,[status(thm)],[51,38,theory(equality)]) ).
cnf(86,negated_conjecture,
( ex_sup_of_relstr_set(esk3_0,X1)
| element(esk10_3(esk3_0,X1,esk6_0),the_carrier(esk3_0))
| ex_sup_of_relstr_set(esk3_0,esk4_0)
| ~ relstr_set_smaller(esk3_0,X1,esk6_0)
| ~ element(esk6_0,the_carrier(esk3_0))
| $false
| ~ relstr_set_smaller(esk3_0,esk4_0,esk9_3(esk3_0,X1,esk6_0))
| ~ element(esk9_3(esk3_0,X1,esk6_0),the_carrier(esk3_0)) ),
inference(rw,[status(thm)],[84,31,theory(equality)]) ).
cnf(87,negated_conjecture,
( ex_sup_of_relstr_set(esk3_0,X1)
| element(esk10_3(esk3_0,X1,esk6_0),the_carrier(esk3_0))
| ex_sup_of_relstr_set(esk3_0,esk4_0)
| ~ relstr_set_smaller(esk3_0,X1,esk6_0)
| ~ element(esk6_0,the_carrier(esk3_0))
| ~ relstr_set_smaller(esk3_0,esk4_0,esk9_3(esk3_0,X1,esk6_0))
| ~ element(esk9_3(esk3_0,X1,esk6_0),the_carrier(esk3_0)) ),
inference(cn,[status(thm)],[86,theory(equality)]) ).
cnf(88,negated_conjecture,
( relstr_set_smaller(esk3_0,X1,esk10_3(esk3_0,X1,esk6_0))
| ex_sup_of_relstr_set(esk3_0,X1)
| ex_sup_of_relstr_set(esk3_0,esk4_0)
| ~ relstr_set_smaller(esk3_0,X1,esk6_0)
| ~ element(esk6_0,the_carrier(esk3_0))
| ~ rel_str(esk3_0)
| ~ relstr_set_smaller(esk3_0,esk4_0,esk9_3(esk3_0,X1,esk6_0))
| ~ element(esk9_3(esk3_0,X1,esk6_0),the_carrier(esk3_0)) ),
inference(spm,[status(thm)],[57,38,theory(equality)]) ).
cnf(90,negated_conjecture,
( relstr_set_smaller(esk3_0,X1,esk10_3(esk3_0,X1,esk6_0))
| ex_sup_of_relstr_set(esk3_0,X1)
| ex_sup_of_relstr_set(esk3_0,esk4_0)
| ~ relstr_set_smaller(esk3_0,X1,esk6_0)
| ~ element(esk6_0,the_carrier(esk3_0))
| $false
| ~ relstr_set_smaller(esk3_0,esk4_0,esk9_3(esk3_0,X1,esk6_0))
| ~ element(esk9_3(esk3_0,X1,esk6_0),the_carrier(esk3_0)) ),
inference(rw,[status(thm)],[88,31,theory(equality)]) ).
cnf(91,negated_conjecture,
( relstr_set_smaller(esk3_0,X1,esk10_3(esk3_0,X1,esk6_0))
| ex_sup_of_relstr_set(esk3_0,X1)
| ex_sup_of_relstr_set(esk3_0,esk4_0)
| ~ relstr_set_smaller(esk3_0,X1,esk6_0)
| ~ element(esk6_0,the_carrier(esk3_0))
| ~ relstr_set_smaller(esk3_0,esk4_0,esk9_3(esk3_0,X1,esk6_0))
| ~ element(esk9_3(esk3_0,X1,esk6_0),the_carrier(esk3_0)) ),
inference(cn,[status(thm)],[90,theory(equality)]) ).
cnf(108,negated_conjecture,
( ex_sup_of_relstr_set(esk3_0,X1)
| related(esk3_0,esk10_3(esk3_0,X1,esk6_0),X2)
| ex_sup_of_relstr_set(esk3_0,esk4_0)
| ~ relstr_set_smaller(esk3_0,X1,X2)
| ~ relstr_set_smaller(esk3_0,X1,esk6_0)
| ~ element(X2,the_carrier(esk3_0))
| ~ element(esk6_0,the_carrier(esk3_0))
| ~ rel_str(esk3_0)
| ~ relstr_set_smaller(esk3_0,esk4_0,esk9_3(esk3_0,X1,esk6_0))
| ~ element(esk9_3(esk3_0,X1,esk6_0),the_carrier(esk3_0)) ),
inference(spm,[status(thm)],[60,38,theory(equality)]) ).
cnf(111,negated_conjecture,
( ex_sup_of_relstr_set(esk3_0,X1)
| related(esk3_0,esk10_3(esk3_0,X1,esk6_0),X2)
| ex_sup_of_relstr_set(esk3_0,esk4_0)
| ~ relstr_set_smaller(esk3_0,X1,X2)
| ~ relstr_set_smaller(esk3_0,X1,esk6_0)
| ~ element(X2,the_carrier(esk3_0))
| ~ element(esk6_0,the_carrier(esk3_0))
| $false
| ~ relstr_set_smaller(esk3_0,esk4_0,esk9_3(esk3_0,X1,esk6_0))
| ~ element(esk9_3(esk3_0,X1,esk6_0),the_carrier(esk3_0)) ),
inference(rw,[status(thm)],[108,31,theory(equality)]) ).
cnf(112,negated_conjecture,
( ex_sup_of_relstr_set(esk3_0,X1)
| related(esk3_0,esk10_3(esk3_0,X1,esk6_0),X2)
| ex_sup_of_relstr_set(esk3_0,esk4_0)
| ~ relstr_set_smaller(esk3_0,X1,X2)
| ~ relstr_set_smaller(esk3_0,X1,esk6_0)
| ~ element(X2,the_carrier(esk3_0))
| ~ element(esk6_0,the_carrier(esk3_0))
| ~ relstr_set_smaller(esk3_0,esk4_0,esk9_3(esk3_0,X1,esk6_0))
| ~ element(esk9_3(esk3_0,X1,esk6_0),the_carrier(esk3_0)) ),
inference(cn,[status(thm)],[111,theory(equality)]) ).
cnf(113,negated_conjecture,
( X1 = esk6_0
| ex_sup_of_relstr_set(esk3_0,esk4_0)
| ~ relstr_set_smaller(esk3_0,esk4_0,X1)
| ~ related(esk3_0,X1,esk6_0)
| ~ element(X1,the_carrier(esk3_0)) ),
inference(csr,[status(thm)],[71,37]) ).
cnf(115,negated_conjecture,
( esk10_3(esk3_0,X1,X2) = esk6_0
| ex_sup_of_relstr_set(esk3_0,esk4_0)
| ex_sup_of_relstr_set(esk3_0,X1)
| element(esk9_3(esk3_0,X1,X2),the_carrier(esk3_0))
| ~ relstr_set_smaller(esk3_0,esk4_0,esk10_3(esk3_0,X1,X2))
| ~ element(esk10_3(esk3_0,X1,X2),the_carrier(esk3_0))
| ~ relstr_set_smaller(esk3_0,X1,esk6_0)
| ~ relstr_set_smaller(esk3_0,X1,X2)
| ~ element(esk6_0,the_carrier(esk3_0))
| ~ element(X2,the_carrier(esk3_0))
| ~ rel_str(esk3_0) ),
inference(spm,[status(thm)],[113,62,theory(equality)]) ).
cnf(118,negated_conjecture,
( esk10_3(esk3_0,X1,X2) = esk6_0
| ex_sup_of_relstr_set(esk3_0,esk4_0)
| ex_sup_of_relstr_set(esk3_0,X1)
| element(esk9_3(esk3_0,X1,X2),the_carrier(esk3_0))
| ~ relstr_set_smaller(esk3_0,esk4_0,esk10_3(esk3_0,X1,X2))
| ~ element(esk10_3(esk3_0,X1,X2),the_carrier(esk3_0))
| ~ relstr_set_smaller(esk3_0,X1,esk6_0)
| ~ relstr_set_smaller(esk3_0,X1,X2)
| ~ element(esk6_0,the_carrier(esk3_0))
| ~ element(X2,the_carrier(esk3_0))
| $false ),
inference(rw,[status(thm)],[115,31,theory(equality)]) ).
cnf(119,negated_conjecture,
( esk10_3(esk3_0,X1,X2) = esk6_0
| ex_sup_of_relstr_set(esk3_0,esk4_0)
| ex_sup_of_relstr_set(esk3_0,X1)
| element(esk9_3(esk3_0,X1,X2),the_carrier(esk3_0))
| ~ relstr_set_smaller(esk3_0,esk4_0,esk10_3(esk3_0,X1,X2))
| ~ element(esk10_3(esk3_0,X1,X2),the_carrier(esk3_0))
| ~ relstr_set_smaller(esk3_0,X1,esk6_0)
| ~ relstr_set_smaller(esk3_0,X1,X2)
| ~ element(esk6_0,the_carrier(esk3_0))
| ~ element(X2,the_carrier(esk3_0)) ),
inference(cn,[status(thm)],[118,theory(equality)]) ).
cnf(135,negated_conjecture,
( ~ relstr_set_smaller(esk3_0,X1,esk5_1(esk7_2(esk3_0,X1)))
| ~ relstr_set_smaller(esk3_0,esk4_0,esk7_2(esk3_0,X1))
| ~ ex_sup_of_relstr_set(esk3_0,esk4_0)
| ~ ex_sup_of_relstr_set(esk3_0,X1)
| ~ element(esk7_2(esk3_0,X1),the_carrier(esk3_0)) ),
inference(csr,[status(thm)],[75,35]) ).
cnf(136,negated_conjecture,
( ~ relstr_set_smaller(esk3_0,esk4_0,esk7_2(esk3_0,esk4_0))
| ~ ex_sup_of_relstr_set(esk3_0,esk4_0)
| ~ element(esk7_2(esk3_0,esk4_0),the_carrier(esk3_0)) ),
inference(spm,[status(thm)],[135,34,theory(equality)]) ).
cnf(137,negated_conjecture,
( ~ ex_sup_of_relstr_set(esk3_0,esk4_0)
| ~ element(esk7_2(esk3_0,esk4_0),the_carrier(esk3_0))
| ~ rel_str(esk3_0) ),
inference(spm,[status(thm)],[136,45,theory(equality)]) ).
cnf(138,negated_conjecture,
( ~ ex_sup_of_relstr_set(esk3_0,esk4_0)
| ~ element(esk7_2(esk3_0,esk4_0),the_carrier(esk3_0))
| $false ),
inference(rw,[status(thm)],[137,31,theory(equality)]) ).
cnf(139,negated_conjecture,
( ~ ex_sup_of_relstr_set(esk3_0,esk4_0)
| ~ element(esk7_2(esk3_0,esk4_0),the_carrier(esk3_0)) ),
inference(cn,[status(thm)],[138,theory(equality)]) ).
cnf(140,negated_conjecture,
( ~ ex_sup_of_relstr_set(esk3_0,esk4_0)
| ~ rel_str(esk3_0) ),
inference(spm,[status(thm)],[139,46,theory(equality)]) ).
cnf(141,negated_conjecture,
( ~ ex_sup_of_relstr_set(esk3_0,esk4_0)
| $false ),
inference(rw,[status(thm)],[140,31,theory(equality)]) ).
cnf(142,negated_conjecture,
~ ex_sup_of_relstr_set(esk3_0,esk4_0),
inference(cn,[status(thm)],[141,theory(equality)]) ).
cnf(143,negated_conjecture,
element(esk6_0,the_carrier(esk3_0)),
inference(sr,[status(thm)],[37,142,theory(equality)]) ).
cnf(144,negated_conjecture,
relstr_set_smaller(esk3_0,esk4_0,esk6_0),
inference(sr,[status(thm)],[36,142,theory(equality)]) ).
cnf(145,negated_conjecture,
( relstr_set_smaller(esk3_0,X1,esk9_3(esk3_0,X1,X2))
| ex_sup_of_relstr_set(esk3_0,X1)
| related(esk3_0,esk10_3(esk3_0,X1,X2),esk6_0)
| ~ relstr_set_smaller(esk3_0,X1,esk6_0)
| ~ relstr_set_smaller(esk3_0,X1,X2)
| ~ element(X2,the_carrier(esk3_0))
| ~ rel_str(esk3_0) ),
inference(spm,[status(thm)],[61,143,theory(equality)]) ).
cnf(146,negated_conjecture,
( relstr_set_smaller(esk3_0,X1,esk9_3(esk3_0,X1,X2))
| ex_sup_of_relstr_set(esk3_0,X1)
| related(esk3_0,esk10_3(esk3_0,X1,X2),esk6_0)
| ~ relstr_set_smaller(esk3_0,X1,esk6_0)
| ~ relstr_set_smaller(esk3_0,X1,X2)
| ~ element(X2,the_carrier(esk3_0))
| $false ),
inference(rw,[status(thm)],[145,31,theory(equality)]) ).
cnf(147,negated_conjecture,
( relstr_set_smaller(esk3_0,X1,esk9_3(esk3_0,X1,X2))
| ex_sup_of_relstr_set(esk3_0,X1)
| related(esk3_0,esk10_3(esk3_0,X1,X2),esk6_0)
| ~ relstr_set_smaller(esk3_0,X1,esk6_0)
| ~ relstr_set_smaller(esk3_0,X1,X2)
| ~ element(X2,the_carrier(esk3_0)) ),
inference(cn,[status(thm)],[146,theory(equality)]) ).
cnf(157,negated_conjecture,
( relstr_set_smaller(esk3_0,X1,esk9_3(esk3_0,X1,esk6_0))
| ex_sup_of_relstr_set(esk3_0,X1)
| related(esk3_0,esk10_3(esk3_0,X1,esk6_0),esk6_0)
| ~ relstr_set_smaller(esk3_0,X1,esk6_0) ),
inference(spm,[status(thm)],[147,143,theory(equality)]) ).
cnf(173,negated_conjecture,
( relstr_set_smaller(esk3_0,esk4_0,esk9_3(esk3_0,esk4_0,esk6_0))
| ex_sup_of_relstr_set(esk3_0,esk4_0)
| related(esk3_0,esk10_3(esk3_0,esk4_0,esk6_0),esk6_0) ),
inference(spm,[status(thm)],[157,144,theory(equality)]) ).
cnf(174,negated_conjecture,
( relstr_set_smaller(esk3_0,esk4_0,esk9_3(esk3_0,esk4_0,esk6_0))
| related(esk3_0,esk10_3(esk3_0,esk4_0,esk6_0),esk6_0) ),
inference(sr,[status(thm)],[173,142,theory(equality)]) ).
cnf(176,negated_conjecture,
( esk10_3(esk3_0,esk4_0,esk6_0) = esk6_0
| ex_sup_of_relstr_set(esk3_0,esk4_0)
| relstr_set_smaller(esk3_0,esk4_0,esk9_3(esk3_0,esk4_0,esk6_0))
| ~ relstr_set_smaller(esk3_0,esk4_0,esk10_3(esk3_0,esk4_0,esk6_0))
| ~ element(esk10_3(esk3_0,esk4_0,esk6_0),the_carrier(esk3_0)) ),
inference(spm,[status(thm)],[113,174,theory(equality)]) ).
cnf(181,negated_conjecture,
( esk10_3(esk3_0,esk4_0,esk6_0) = esk6_0
| relstr_set_smaller(esk3_0,esk4_0,esk9_3(esk3_0,esk4_0,esk6_0))
| ~ relstr_set_smaller(esk3_0,esk4_0,esk10_3(esk3_0,esk4_0,esk6_0))
| ~ element(esk10_3(esk3_0,esk4_0,esk6_0),the_carrier(esk3_0)) ),
inference(sr,[status(thm)],[176,142,theory(equality)]) ).
cnf(185,negated_conjecture,
( esk10_3(esk3_0,esk4_0,esk6_0) = esk6_0
| relstr_set_smaller(esk3_0,esk4_0,esk9_3(esk3_0,esk4_0,esk6_0))
| ex_sup_of_relstr_set(esk3_0,esk4_0)
| ~ element(esk10_3(esk3_0,esk4_0,esk6_0),the_carrier(esk3_0))
| ~ relstr_set_smaller(esk3_0,esk4_0,esk6_0)
| ~ element(esk6_0,the_carrier(esk3_0))
| ~ rel_str(esk3_0) ),
inference(spm,[status(thm)],[181,58,theory(equality)]) ).
cnf(191,negated_conjecture,
( esk10_3(esk3_0,esk4_0,esk6_0) = esk6_0
| relstr_set_smaller(esk3_0,esk4_0,esk9_3(esk3_0,esk4_0,esk6_0))
| ex_sup_of_relstr_set(esk3_0,esk4_0)
| ~ element(esk10_3(esk3_0,esk4_0,esk6_0),the_carrier(esk3_0))
| $false
| ~ element(esk6_0,the_carrier(esk3_0))
| ~ rel_str(esk3_0) ),
inference(rw,[status(thm)],[185,144,theory(equality)]) ).
cnf(192,negated_conjecture,
( esk10_3(esk3_0,esk4_0,esk6_0) = esk6_0
| relstr_set_smaller(esk3_0,esk4_0,esk9_3(esk3_0,esk4_0,esk6_0))
| ex_sup_of_relstr_set(esk3_0,esk4_0)
| ~ element(esk10_3(esk3_0,esk4_0,esk6_0),the_carrier(esk3_0))
| $false
| $false
| ~ rel_str(esk3_0) ),
inference(rw,[status(thm)],[191,143,theory(equality)]) ).
cnf(193,negated_conjecture,
( esk10_3(esk3_0,esk4_0,esk6_0) = esk6_0
| relstr_set_smaller(esk3_0,esk4_0,esk9_3(esk3_0,esk4_0,esk6_0))
| ex_sup_of_relstr_set(esk3_0,esk4_0)
| ~ element(esk10_3(esk3_0,esk4_0,esk6_0),the_carrier(esk3_0))
| $false
| $false
| $false ),
inference(rw,[status(thm)],[192,31,theory(equality)]) ).
cnf(194,negated_conjecture,
( esk10_3(esk3_0,esk4_0,esk6_0) = esk6_0
| relstr_set_smaller(esk3_0,esk4_0,esk9_3(esk3_0,esk4_0,esk6_0))
| ex_sup_of_relstr_set(esk3_0,esk4_0)
| ~ element(esk10_3(esk3_0,esk4_0,esk6_0),the_carrier(esk3_0)) ),
inference(cn,[status(thm)],[193,theory(equality)]) ).
cnf(195,negated_conjecture,
( esk10_3(esk3_0,esk4_0,esk6_0) = esk6_0
| relstr_set_smaller(esk3_0,esk4_0,esk9_3(esk3_0,esk4_0,esk6_0))
| ~ element(esk10_3(esk3_0,esk4_0,esk6_0),the_carrier(esk3_0)) ),
inference(sr,[status(thm)],[194,142,theory(equality)]) ).
cnf(196,negated_conjecture,
( ex_sup_of_relstr_set(esk3_0,X1)
| ex_sup_of_relstr_set(esk3_0,esk4_0)
| esk10_3(esk3_0,X1,esk6_0) != esk6_0
| ~ relstr_set_smaller(esk3_0,X1,esk6_0)
| $false
| ~ relstr_set_smaller(esk3_0,esk4_0,esk9_3(esk3_0,X1,esk6_0))
| ~ element(esk9_3(esk3_0,X1,esk6_0),the_carrier(esk3_0)) ),
inference(rw,[status(thm)],[83,143,theory(equality)]) ).
cnf(197,negated_conjecture,
( ex_sup_of_relstr_set(esk3_0,X1)
| ex_sup_of_relstr_set(esk3_0,esk4_0)
| esk10_3(esk3_0,X1,esk6_0) != esk6_0
| ~ relstr_set_smaller(esk3_0,X1,esk6_0)
| ~ relstr_set_smaller(esk3_0,esk4_0,esk9_3(esk3_0,X1,esk6_0))
| ~ element(esk9_3(esk3_0,X1,esk6_0),the_carrier(esk3_0)) ),
inference(cn,[status(thm)],[196,theory(equality)]) ).
cnf(198,negated_conjecture,
( ex_sup_of_relstr_set(esk3_0,X1)
| esk10_3(esk3_0,X1,esk6_0) != esk6_0
| ~ relstr_set_smaller(esk3_0,X1,esk6_0)
| ~ relstr_set_smaller(esk3_0,esk4_0,esk9_3(esk3_0,X1,esk6_0))
| ~ element(esk9_3(esk3_0,X1,esk6_0),the_carrier(esk3_0)) ),
inference(sr,[status(thm)],[197,142,theory(equality)]) ).
cnf(199,negated_conjecture,
( ex_sup_of_relstr_set(esk3_0,esk4_0)
| esk10_3(esk3_0,esk4_0,esk6_0) != esk6_0
| ~ relstr_set_smaller(esk3_0,esk4_0,esk6_0)
| ~ element(esk9_3(esk3_0,esk4_0,esk6_0),the_carrier(esk3_0))
| ~ element(esk6_0,the_carrier(esk3_0))
| ~ rel_str(esk3_0) ),
inference(spm,[status(thm)],[198,55,theory(equality)]) ).
cnf(202,negated_conjecture,
( ex_sup_of_relstr_set(esk3_0,esk4_0)
| esk10_3(esk3_0,esk4_0,esk6_0) != esk6_0
| $false
| ~ element(esk9_3(esk3_0,esk4_0,esk6_0),the_carrier(esk3_0))
| ~ element(esk6_0,the_carrier(esk3_0))
| ~ rel_str(esk3_0) ),
inference(rw,[status(thm)],[199,144,theory(equality)]) ).
cnf(203,negated_conjecture,
( ex_sup_of_relstr_set(esk3_0,esk4_0)
| esk10_3(esk3_0,esk4_0,esk6_0) != esk6_0
| $false
| ~ element(esk9_3(esk3_0,esk4_0,esk6_0),the_carrier(esk3_0))
| $false
| ~ rel_str(esk3_0) ),
inference(rw,[status(thm)],[202,143,theory(equality)]) ).
cnf(204,negated_conjecture,
( ex_sup_of_relstr_set(esk3_0,esk4_0)
| esk10_3(esk3_0,esk4_0,esk6_0) != esk6_0
| $false
| ~ element(esk9_3(esk3_0,esk4_0,esk6_0),the_carrier(esk3_0))
| $false
| $false ),
inference(rw,[status(thm)],[203,31,theory(equality)]) ).
cnf(205,negated_conjecture,
( ex_sup_of_relstr_set(esk3_0,esk4_0)
| esk10_3(esk3_0,esk4_0,esk6_0) != esk6_0
| ~ element(esk9_3(esk3_0,esk4_0,esk6_0),the_carrier(esk3_0)) ),
inference(cn,[status(thm)],[204,theory(equality)]) ).
cnf(206,negated_conjecture,
( esk10_3(esk3_0,esk4_0,esk6_0) != esk6_0
| ~ element(esk9_3(esk3_0,esk4_0,esk6_0),the_carrier(esk3_0)) ),
inference(sr,[status(thm)],[205,142,theory(equality)]) ).
cnf(218,negated_conjecture,
( ex_sup_of_relstr_set(esk3_0,esk4_0)
| esk10_3(esk3_0,esk4_0,esk6_0) != esk6_0
| ~ relstr_set_smaller(esk3_0,esk4_0,esk6_0)
| ~ element(esk6_0,the_carrier(esk3_0))
| ~ rel_str(esk3_0) ),
inference(spm,[status(thm)],[206,56,theory(equality)]) ).
cnf(219,negated_conjecture,
( ex_sup_of_relstr_set(esk3_0,esk4_0)
| esk10_3(esk3_0,esk4_0,esk6_0) != esk6_0
| $false
| ~ element(esk6_0,the_carrier(esk3_0))
| ~ rel_str(esk3_0) ),
inference(rw,[status(thm)],[218,144,theory(equality)]) ).
cnf(220,negated_conjecture,
( ex_sup_of_relstr_set(esk3_0,esk4_0)
| esk10_3(esk3_0,esk4_0,esk6_0) != esk6_0
| $false
| $false
| ~ rel_str(esk3_0) ),
inference(rw,[status(thm)],[219,143,theory(equality)]) ).
cnf(221,negated_conjecture,
( ex_sup_of_relstr_set(esk3_0,esk4_0)
| esk10_3(esk3_0,esk4_0,esk6_0) != esk6_0
| $false
| $false
| $false ),
inference(rw,[status(thm)],[220,31,theory(equality)]) ).
cnf(222,negated_conjecture,
( ex_sup_of_relstr_set(esk3_0,esk4_0)
| esk10_3(esk3_0,esk4_0,esk6_0) != esk6_0 ),
inference(cn,[status(thm)],[221,theory(equality)]) ).
cnf(223,negated_conjecture,
esk10_3(esk3_0,esk4_0,esk6_0) != esk6_0,
inference(sr,[status(thm)],[222,142,theory(equality)]) ).
cnf(231,negated_conjecture,
( ex_sup_of_relstr_set(esk3_0,X1)
| element(esk10_3(esk3_0,X1,esk6_0),the_carrier(esk3_0))
| ex_sup_of_relstr_set(esk3_0,esk4_0)
| ~ relstr_set_smaller(esk3_0,X1,esk6_0)
| $false
| ~ relstr_set_smaller(esk3_0,esk4_0,esk9_3(esk3_0,X1,esk6_0))
| ~ element(esk9_3(esk3_0,X1,esk6_0),the_carrier(esk3_0)) ),
inference(rw,[status(thm)],[87,143,theory(equality)]) ).
cnf(232,negated_conjecture,
( ex_sup_of_relstr_set(esk3_0,X1)
| element(esk10_3(esk3_0,X1,esk6_0),the_carrier(esk3_0))
| ex_sup_of_relstr_set(esk3_0,esk4_0)
| ~ relstr_set_smaller(esk3_0,X1,esk6_0)
| ~ relstr_set_smaller(esk3_0,esk4_0,esk9_3(esk3_0,X1,esk6_0))
| ~ element(esk9_3(esk3_0,X1,esk6_0),the_carrier(esk3_0)) ),
inference(cn,[status(thm)],[231,theory(equality)]) ).
cnf(233,negated_conjecture,
( ex_sup_of_relstr_set(esk3_0,X1)
| element(esk10_3(esk3_0,X1,esk6_0),the_carrier(esk3_0))
| ~ relstr_set_smaller(esk3_0,X1,esk6_0)
| ~ relstr_set_smaller(esk3_0,esk4_0,esk9_3(esk3_0,X1,esk6_0))
| ~ element(esk9_3(esk3_0,X1,esk6_0),the_carrier(esk3_0)) ),
inference(sr,[status(thm)],[232,142,theory(equality)]) ).
cnf(235,negated_conjecture,
( ex_sup_of_relstr_set(esk3_0,esk4_0)
| element(esk10_3(esk3_0,esk4_0,esk6_0),the_carrier(esk3_0))
| ~ relstr_set_smaller(esk3_0,esk4_0,esk6_0)
| ~ element(esk9_3(esk3_0,esk4_0,esk6_0),the_carrier(esk3_0))
| ~ element(esk6_0,the_carrier(esk3_0))
| ~ rel_str(esk3_0) ),
inference(spm,[status(thm)],[233,52,theory(equality)]) ).
cnf(242,negated_conjecture,
( ex_sup_of_relstr_set(esk3_0,esk4_0)
| element(esk10_3(esk3_0,esk4_0,esk6_0),the_carrier(esk3_0))
| $false
| ~ element(esk9_3(esk3_0,esk4_0,esk6_0),the_carrier(esk3_0))
| ~ element(esk6_0,the_carrier(esk3_0))
| ~ rel_str(esk3_0) ),
inference(rw,[status(thm)],[235,144,theory(equality)]) ).
cnf(243,negated_conjecture,
( ex_sup_of_relstr_set(esk3_0,esk4_0)
| element(esk10_3(esk3_0,esk4_0,esk6_0),the_carrier(esk3_0))
| $false
| ~ element(esk9_3(esk3_0,esk4_0,esk6_0),the_carrier(esk3_0))
| $false
| ~ rel_str(esk3_0) ),
inference(rw,[status(thm)],[242,143,theory(equality)]) ).
cnf(244,negated_conjecture,
( ex_sup_of_relstr_set(esk3_0,esk4_0)
| element(esk10_3(esk3_0,esk4_0,esk6_0),the_carrier(esk3_0))
| $false
| ~ element(esk9_3(esk3_0,esk4_0,esk6_0),the_carrier(esk3_0))
| $false
| $false ),
inference(rw,[status(thm)],[243,31,theory(equality)]) ).
cnf(245,negated_conjecture,
( ex_sup_of_relstr_set(esk3_0,esk4_0)
| element(esk10_3(esk3_0,esk4_0,esk6_0),the_carrier(esk3_0))
| ~ element(esk9_3(esk3_0,esk4_0,esk6_0),the_carrier(esk3_0)) ),
inference(cn,[status(thm)],[244,theory(equality)]) ).
cnf(246,negated_conjecture,
( element(esk10_3(esk3_0,esk4_0,esk6_0),the_carrier(esk3_0))
| ~ element(esk9_3(esk3_0,esk4_0,esk6_0),the_carrier(esk3_0)) ),
inference(sr,[status(thm)],[245,142,theory(equality)]) ).
cnf(254,negated_conjecture,
( relstr_set_smaller(esk3_0,X1,esk10_3(esk3_0,X1,esk6_0))
| ex_sup_of_relstr_set(esk3_0,X1)
| ex_sup_of_relstr_set(esk3_0,esk4_0)
| ~ relstr_set_smaller(esk3_0,X1,esk6_0)
| $false
| ~ relstr_set_smaller(esk3_0,esk4_0,esk9_3(esk3_0,X1,esk6_0))
| ~ element(esk9_3(esk3_0,X1,esk6_0),the_carrier(esk3_0)) ),
inference(rw,[status(thm)],[91,143,theory(equality)]) ).
cnf(255,negated_conjecture,
( relstr_set_smaller(esk3_0,X1,esk10_3(esk3_0,X1,esk6_0))
| ex_sup_of_relstr_set(esk3_0,X1)
| ex_sup_of_relstr_set(esk3_0,esk4_0)
| ~ relstr_set_smaller(esk3_0,X1,esk6_0)
| ~ relstr_set_smaller(esk3_0,esk4_0,esk9_3(esk3_0,X1,esk6_0))
| ~ element(esk9_3(esk3_0,X1,esk6_0),the_carrier(esk3_0)) ),
inference(cn,[status(thm)],[254,theory(equality)]) ).
cnf(256,negated_conjecture,
( relstr_set_smaller(esk3_0,X1,esk10_3(esk3_0,X1,esk6_0))
| ex_sup_of_relstr_set(esk3_0,X1)
| ~ relstr_set_smaller(esk3_0,X1,esk6_0)
| ~ relstr_set_smaller(esk3_0,esk4_0,esk9_3(esk3_0,X1,esk6_0))
| ~ element(esk9_3(esk3_0,X1,esk6_0),the_carrier(esk3_0)) ),
inference(sr,[status(thm)],[255,142,theory(equality)]) ).
cnf(259,negated_conjecture,
( relstr_set_smaller(esk3_0,esk4_0,esk10_3(esk3_0,esk4_0,esk6_0))
| ex_sup_of_relstr_set(esk3_0,esk4_0)
| esk10_3(esk3_0,esk4_0,esk6_0) = esk6_0
| ~ relstr_set_smaller(esk3_0,esk4_0,esk6_0)
| ~ element(esk9_3(esk3_0,esk4_0,esk6_0),the_carrier(esk3_0))
| ~ element(esk10_3(esk3_0,esk4_0,esk6_0),the_carrier(esk3_0)) ),
inference(spm,[status(thm)],[256,195,theory(equality)]) ).
cnf(270,negated_conjecture,
( relstr_set_smaller(esk3_0,esk4_0,esk10_3(esk3_0,esk4_0,esk6_0))
| ex_sup_of_relstr_set(esk3_0,esk4_0)
| esk10_3(esk3_0,esk4_0,esk6_0) = esk6_0
| $false
| ~ element(esk9_3(esk3_0,esk4_0,esk6_0),the_carrier(esk3_0))
| ~ element(esk10_3(esk3_0,esk4_0,esk6_0),the_carrier(esk3_0)) ),
inference(rw,[status(thm)],[259,144,theory(equality)]) ).
cnf(271,negated_conjecture,
( relstr_set_smaller(esk3_0,esk4_0,esk10_3(esk3_0,esk4_0,esk6_0))
| ex_sup_of_relstr_set(esk3_0,esk4_0)
| esk10_3(esk3_0,esk4_0,esk6_0) = esk6_0
| ~ element(esk9_3(esk3_0,esk4_0,esk6_0),the_carrier(esk3_0))
| ~ element(esk10_3(esk3_0,esk4_0,esk6_0),the_carrier(esk3_0)) ),
inference(cn,[status(thm)],[270,theory(equality)]) ).
cnf(272,negated_conjecture,
( relstr_set_smaller(esk3_0,esk4_0,esk10_3(esk3_0,esk4_0,esk6_0))
| esk10_3(esk3_0,esk4_0,esk6_0) = esk6_0
| ~ element(esk9_3(esk3_0,esk4_0,esk6_0),the_carrier(esk3_0))
| ~ element(esk10_3(esk3_0,esk4_0,esk6_0),the_carrier(esk3_0)) ),
inference(sr,[status(thm)],[271,142,theory(equality)]) ).
cnf(273,negated_conjecture,
( relstr_set_smaller(esk3_0,esk4_0,esk10_3(esk3_0,esk4_0,esk6_0))
| ~ element(esk9_3(esk3_0,esk4_0,esk6_0),the_carrier(esk3_0))
| ~ element(esk10_3(esk3_0,esk4_0,esk6_0),the_carrier(esk3_0)) ),
inference(sr,[status(thm)],[272,223,theory(equality)]) ).
cnf(280,negated_conjecture,
( relstr_set_smaller(esk3_0,esk4_0,esk10_3(esk3_0,esk4_0,esk6_0))
| ~ element(esk9_3(esk3_0,esk4_0,esk6_0),the_carrier(esk3_0)) ),
inference(csr,[status(thm)],[273,246]) ).
cnf(287,negated_conjecture,
( ex_sup_of_relstr_set(esk3_0,X1)
| related(esk3_0,esk10_3(esk3_0,X1,esk6_0),X2)
| ex_sup_of_relstr_set(esk3_0,esk4_0)
| ~ relstr_set_smaller(esk3_0,X1,X2)
| ~ relstr_set_smaller(esk3_0,X1,esk6_0)
| ~ element(X2,the_carrier(esk3_0))
| $false
| ~ relstr_set_smaller(esk3_0,esk4_0,esk9_3(esk3_0,X1,esk6_0))
| ~ element(esk9_3(esk3_0,X1,esk6_0),the_carrier(esk3_0)) ),
inference(rw,[status(thm)],[112,143,theory(equality)]) ).
cnf(288,negated_conjecture,
( ex_sup_of_relstr_set(esk3_0,X1)
| related(esk3_0,esk10_3(esk3_0,X1,esk6_0),X2)
| ex_sup_of_relstr_set(esk3_0,esk4_0)
| ~ relstr_set_smaller(esk3_0,X1,X2)
| ~ relstr_set_smaller(esk3_0,X1,esk6_0)
| ~ element(X2,the_carrier(esk3_0))
| ~ relstr_set_smaller(esk3_0,esk4_0,esk9_3(esk3_0,X1,esk6_0))
| ~ element(esk9_3(esk3_0,X1,esk6_0),the_carrier(esk3_0)) ),
inference(cn,[status(thm)],[287,theory(equality)]) ).
cnf(289,negated_conjecture,
( ex_sup_of_relstr_set(esk3_0,X1)
| related(esk3_0,esk10_3(esk3_0,X1,esk6_0),X2)
| ~ relstr_set_smaller(esk3_0,X1,X2)
| ~ relstr_set_smaller(esk3_0,X1,esk6_0)
| ~ element(X2,the_carrier(esk3_0))
| ~ relstr_set_smaller(esk3_0,esk4_0,esk9_3(esk3_0,X1,esk6_0))
| ~ element(esk9_3(esk3_0,X1,esk6_0),the_carrier(esk3_0)) ),
inference(sr,[status(thm)],[288,142,theory(equality)]) ).
cnf(297,negated_conjecture,
( esk10_3(esk3_0,X1,esk6_0) = esk6_0
| ex_sup_of_relstr_set(esk3_0,esk4_0)
| ex_sup_of_relstr_set(esk3_0,X1)
| ~ relstr_set_smaller(esk3_0,esk4_0,esk10_3(esk3_0,X1,esk6_0))
| ~ element(esk10_3(esk3_0,X1,esk6_0),the_carrier(esk3_0))
| ~ relstr_set_smaller(esk3_0,esk4_0,esk9_3(esk3_0,X1,esk6_0))
| ~ relstr_set_smaller(esk3_0,X1,esk6_0)
| ~ element(esk9_3(esk3_0,X1,esk6_0),the_carrier(esk3_0))
| ~ element(esk6_0,the_carrier(esk3_0)) ),
inference(spm,[status(thm)],[113,289,theory(equality)]) ).
cnf(312,negated_conjecture,
( esk10_3(esk3_0,X1,esk6_0) = esk6_0
| ex_sup_of_relstr_set(esk3_0,esk4_0)
| ex_sup_of_relstr_set(esk3_0,X1)
| ~ relstr_set_smaller(esk3_0,esk4_0,esk10_3(esk3_0,X1,esk6_0))
| ~ element(esk10_3(esk3_0,X1,esk6_0),the_carrier(esk3_0))
| ~ relstr_set_smaller(esk3_0,esk4_0,esk9_3(esk3_0,X1,esk6_0))
| ~ relstr_set_smaller(esk3_0,X1,esk6_0)
| ~ element(esk9_3(esk3_0,X1,esk6_0),the_carrier(esk3_0))
| $false ),
inference(rw,[status(thm)],[297,143,theory(equality)]) ).
cnf(313,negated_conjecture,
( esk10_3(esk3_0,X1,esk6_0) = esk6_0
| ex_sup_of_relstr_set(esk3_0,esk4_0)
| ex_sup_of_relstr_set(esk3_0,X1)
| ~ relstr_set_smaller(esk3_0,esk4_0,esk10_3(esk3_0,X1,esk6_0))
| ~ element(esk10_3(esk3_0,X1,esk6_0),the_carrier(esk3_0))
| ~ relstr_set_smaller(esk3_0,esk4_0,esk9_3(esk3_0,X1,esk6_0))
| ~ relstr_set_smaller(esk3_0,X1,esk6_0)
| ~ element(esk9_3(esk3_0,X1,esk6_0),the_carrier(esk3_0)) ),
inference(cn,[status(thm)],[312,theory(equality)]) ).
cnf(314,negated_conjecture,
( esk10_3(esk3_0,X1,esk6_0) = esk6_0
| ex_sup_of_relstr_set(esk3_0,X1)
| ~ relstr_set_smaller(esk3_0,esk4_0,esk10_3(esk3_0,X1,esk6_0))
| ~ element(esk10_3(esk3_0,X1,esk6_0),the_carrier(esk3_0))
| ~ relstr_set_smaller(esk3_0,esk4_0,esk9_3(esk3_0,X1,esk6_0))
| ~ relstr_set_smaller(esk3_0,X1,esk6_0)
| ~ element(esk9_3(esk3_0,X1,esk6_0),the_carrier(esk3_0)) ),
inference(sr,[status(thm)],[313,142,theory(equality)]) ).
cnf(318,negated_conjecture,
( esk10_3(esk3_0,X1,esk6_0) = esk6_0
| ex_sup_of_relstr_set(esk3_0,X1)
| ~ relstr_set_smaller(esk3_0,esk4_0,esk9_3(esk3_0,X1,esk6_0))
| ~ relstr_set_smaller(esk3_0,esk4_0,esk10_3(esk3_0,X1,esk6_0))
| ~ relstr_set_smaller(esk3_0,X1,esk6_0)
| ~ element(esk9_3(esk3_0,X1,esk6_0),the_carrier(esk3_0)) ),
inference(csr,[status(thm)],[314,233]) ).
cnf(319,negated_conjecture,
( ex_sup_of_relstr_set(esk3_0,X1)
| ~ relstr_set_smaller(esk3_0,esk4_0,esk10_3(esk3_0,X1,esk6_0))
| ~ relstr_set_smaller(esk3_0,esk4_0,esk9_3(esk3_0,X1,esk6_0))
| ~ relstr_set_smaller(esk3_0,X1,esk6_0)
| ~ element(esk9_3(esk3_0,X1,esk6_0),the_carrier(esk3_0)) ),
inference(csr,[status(thm)],[318,198]) ).
cnf(322,negated_conjecture,
( ex_sup_of_relstr_set(esk3_0,esk4_0)
| ~ relstr_set_smaller(esk3_0,esk4_0,esk9_3(esk3_0,esk4_0,esk6_0))
| ~ relstr_set_smaller(esk3_0,esk4_0,esk6_0)
| ~ element(esk9_3(esk3_0,esk4_0,esk6_0),the_carrier(esk3_0)) ),
inference(spm,[status(thm)],[319,280,theory(equality)]) ).
cnf(331,negated_conjecture,
( ex_sup_of_relstr_set(esk3_0,esk4_0)
| ~ relstr_set_smaller(esk3_0,esk4_0,esk9_3(esk3_0,esk4_0,esk6_0))
| $false
| ~ element(esk9_3(esk3_0,esk4_0,esk6_0),the_carrier(esk3_0)) ),
inference(rw,[status(thm)],[322,144,theory(equality)]) ).
cnf(332,negated_conjecture,
( ex_sup_of_relstr_set(esk3_0,esk4_0)
| ~ relstr_set_smaller(esk3_0,esk4_0,esk9_3(esk3_0,esk4_0,esk6_0))
| ~ element(esk9_3(esk3_0,esk4_0,esk6_0),the_carrier(esk3_0)) ),
inference(cn,[status(thm)],[331,theory(equality)]) ).
cnf(333,negated_conjecture,
( ~ relstr_set_smaller(esk3_0,esk4_0,esk9_3(esk3_0,esk4_0,esk6_0))
| ~ element(esk9_3(esk3_0,esk4_0,esk6_0),the_carrier(esk3_0)) ),
inference(sr,[status(thm)],[332,142,theory(equality)]) ).
cnf(336,negated_conjecture,
( esk10_3(esk3_0,esk4_0,esk6_0) = esk6_0
| ~ element(esk9_3(esk3_0,esk4_0,esk6_0),the_carrier(esk3_0))
| ~ element(esk10_3(esk3_0,esk4_0,esk6_0),the_carrier(esk3_0)) ),
inference(spm,[status(thm)],[333,195,theory(equality)]) ).
cnf(347,negated_conjecture,
( ~ element(esk9_3(esk3_0,esk4_0,esk6_0),the_carrier(esk3_0))
| ~ element(esk10_3(esk3_0,esk4_0,esk6_0),the_carrier(esk3_0)) ),
inference(sr,[status(thm)],[336,223,theory(equality)]) ).
cnf(352,negated_conjecture,
~ element(esk9_3(esk3_0,esk4_0,esk6_0),the_carrier(esk3_0)),
inference(csr,[status(thm)],[347,246]) ).
cnf(359,negated_conjecture,
( esk10_3(esk3_0,X1,X2) = esk6_0
| ex_sup_of_relstr_set(esk3_0,esk4_0)
| ex_sup_of_relstr_set(esk3_0,X1)
| element(esk9_3(esk3_0,X1,X2),the_carrier(esk3_0))
| ~ relstr_set_smaller(esk3_0,esk4_0,esk10_3(esk3_0,X1,X2))
| ~ element(esk10_3(esk3_0,X1,X2),the_carrier(esk3_0))
| ~ relstr_set_smaller(esk3_0,X1,esk6_0)
| ~ relstr_set_smaller(esk3_0,X1,X2)
| $false
| ~ element(X2,the_carrier(esk3_0)) ),
inference(rw,[status(thm)],[119,143,theory(equality)]) ).
cnf(360,negated_conjecture,
( esk10_3(esk3_0,X1,X2) = esk6_0
| ex_sup_of_relstr_set(esk3_0,esk4_0)
| ex_sup_of_relstr_set(esk3_0,X1)
| element(esk9_3(esk3_0,X1,X2),the_carrier(esk3_0))
| ~ relstr_set_smaller(esk3_0,esk4_0,esk10_3(esk3_0,X1,X2))
| ~ element(esk10_3(esk3_0,X1,X2),the_carrier(esk3_0))
| ~ relstr_set_smaller(esk3_0,X1,esk6_0)
| ~ relstr_set_smaller(esk3_0,X1,X2)
| ~ element(X2,the_carrier(esk3_0)) ),
inference(cn,[status(thm)],[359,theory(equality)]) ).
cnf(361,negated_conjecture,
( esk10_3(esk3_0,X1,X2) = esk6_0
| ex_sup_of_relstr_set(esk3_0,X1)
| element(esk9_3(esk3_0,X1,X2),the_carrier(esk3_0))
| ~ relstr_set_smaller(esk3_0,esk4_0,esk10_3(esk3_0,X1,X2))
| ~ element(esk10_3(esk3_0,X1,X2),the_carrier(esk3_0))
| ~ relstr_set_smaller(esk3_0,X1,esk6_0)
| ~ relstr_set_smaller(esk3_0,X1,X2)
| ~ element(X2,the_carrier(esk3_0)) ),
inference(sr,[status(thm)],[360,142,theory(equality)]) ).
cnf(362,negated_conjecture,
( esk10_3(esk3_0,esk4_0,X1) = esk6_0
| ex_sup_of_relstr_set(esk3_0,esk4_0)
| element(esk9_3(esk3_0,esk4_0,X1),the_carrier(esk3_0))
| ~ relstr_set_smaller(esk3_0,esk4_0,esk6_0)
| ~ relstr_set_smaller(esk3_0,esk4_0,X1)
| ~ element(esk10_3(esk3_0,esk4_0,X1),the_carrier(esk3_0))
| ~ element(X1,the_carrier(esk3_0))
| ~ rel_str(esk3_0) ),
inference(spm,[status(thm)],[361,59,theory(equality)]) ).
cnf(365,negated_conjecture,
( esk10_3(esk3_0,esk4_0,X1) = esk6_0
| ex_sup_of_relstr_set(esk3_0,esk4_0)
| element(esk9_3(esk3_0,esk4_0,X1),the_carrier(esk3_0))
| $false
| ~ relstr_set_smaller(esk3_0,esk4_0,X1)
| ~ element(esk10_3(esk3_0,esk4_0,X1),the_carrier(esk3_0))
| ~ element(X1,the_carrier(esk3_0))
| ~ rel_str(esk3_0) ),
inference(rw,[status(thm)],[362,144,theory(equality)]) ).
cnf(366,negated_conjecture,
( esk10_3(esk3_0,esk4_0,X1) = esk6_0
| ex_sup_of_relstr_set(esk3_0,esk4_0)
| element(esk9_3(esk3_0,esk4_0,X1),the_carrier(esk3_0))
| $false
| ~ relstr_set_smaller(esk3_0,esk4_0,X1)
| ~ element(esk10_3(esk3_0,esk4_0,X1),the_carrier(esk3_0))
| ~ element(X1,the_carrier(esk3_0))
| $false ),
inference(rw,[status(thm)],[365,31,theory(equality)]) ).
cnf(367,negated_conjecture,
( esk10_3(esk3_0,esk4_0,X1) = esk6_0
| ex_sup_of_relstr_set(esk3_0,esk4_0)
| element(esk9_3(esk3_0,esk4_0,X1),the_carrier(esk3_0))
| ~ relstr_set_smaller(esk3_0,esk4_0,X1)
| ~ element(esk10_3(esk3_0,esk4_0,X1),the_carrier(esk3_0))
| ~ element(X1,the_carrier(esk3_0)) ),
inference(cn,[status(thm)],[366,theory(equality)]) ).
cnf(368,negated_conjecture,
( esk10_3(esk3_0,esk4_0,X1) = esk6_0
| element(esk9_3(esk3_0,esk4_0,X1),the_carrier(esk3_0))
| ~ relstr_set_smaller(esk3_0,esk4_0,X1)
| ~ element(esk10_3(esk3_0,esk4_0,X1),the_carrier(esk3_0))
| ~ element(X1,the_carrier(esk3_0)) ),
inference(sr,[status(thm)],[367,142,theory(equality)]) ).
cnf(376,negated_conjecture,
( esk10_3(esk3_0,esk4_0,X1) = esk6_0
| element(esk9_3(esk3_0,esk4_0,X1),the_carrier(esk3_0))
| ex_sup_of_relstr_set(esk3_0,esk4_0)
| ~ relstr_set_smaller(esk3_0,esk4_0,X1)
| ~ element(X1,the_carrier(esk3_0))
| ~ rel_str(esk3_0) ),
inference(spm,[status(thm)],[368,53,theory(equality)]) ).
cnf(378,negated_conjecture,
( esk10_3(esk3_0,esk4_0,X1) = esk6_0
| element(esk9_3(esk3_0,esk4_0,X1),the_carrier(esk3_0))
| ex_sup_of_relstr_set(esk3_0,esk4_0)
| ~ relstr_set_smaller(esk3_0,esk4_0,X1)
| ~ element(X1,the_carrier(esk3_0))
| $false ),
inference(rw,[status(thm)],[376,31,theory(equality)]) ).
cnf(379,negated_conjecture,
( esk10_3(esk3_0,esk4_0,X1) = esk6_0
| element(esk9_3(esk3_0,esk4_0,X1),the_carrier(esk3_0))
| ex_sup_of_relstr_set(esk3_0,esk4_0)
| ~ relstr_set_smaller(esk3_0,esk4_0,X1)
| ~ element(X1,the_carrier(esk3_0)) ),
inference(cn,[status(thm)],[378,theory(equality)]) ).
cnf(380,negated_conjecture,
( esk10_3(esk3_0,esk4_0,X1) = esk6_0
| element(esk9_3(esk3_0,esk4_0,X1),the_carrier(esk3_0))
| ~ relstr_set_smaller(esk3_0,esk4_0,X1)
| ~ element(X1,the_carrier(esk3_0)) ),
inference(sr,[status(thm)],[379,142,theory(equality)]) ).
cnf(384,negated_conjecture,
( esk10_3(esk3_0,esk4_0,esk6_0) = esk6_0
| ~ relstr_set_smaller(esk3_0,esk4_0,esk6_0)
| ~ element(esk6_0,the_carrier(esk3_0)) ),
inference(spm,[status(thm)],[352,380,theory(equality)]) ).
cnf(389,negated_conjecture,
( esk10_3(esk3_0,esk4_0,esk6_0) = esk6_0
| $false
| ~ element(esk6_0,the_carrier(esk3_0)) ),
inference(rw,[status(thm)],[384,144,theory(equality)]) ).
cnf(390,negated_conjecture,
( esk10_3(esk3_0,esk4_0,esk6_0) = esk6_0
| $false
| $false ),
inference(rw,[status(thm)],[389,143,theory(equality)]) ).
cnf(391,negated_conjecture,
esk10_3(esk3_0,esk4_0,esk6_0) = esk6_0,
inference(cn,[status(thm)],[390,theory(equality)]) ).
cnf(392,negated_conjecture,
$false,
inference(sr,[status(thm)],[391,223,theory(equality)]) ).
cnf(393,negated_conjecture,
$false,
392,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% % SZS status Started for /home/graph/tptp/TPTP/Problems/SEU/SEU356+1.p
% --creating new selector for []
% -running prover on /tmp/tmp3i-K86/sel_SEU356+1.p_1 with time limit 29
% -prover status Theorem
% Problem SEU356+1.p solved in phase 0.
% % SZS status Theorem for /home/graph/tptp/TPTP/Problems/SEU/SEU356+1.p
% % SZS status Ended for /home/graph/tptp/TPTP/Problems/SEU/SEU356+1.p
% Solved 1 out of 1.
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% See solution above
% # SZS output end CNFRefutation
%
%------------------------------------------------------------------------------