%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : SEU339+1 : TPTP v5.0.0. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : Source/sine.py -e eprover -t %d %s
% Computer : art09.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:29:51 EST 2010
% Result : Theorem 16.88s
% Output : CNFRefutation 16.88s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 18
% Syntax : Number of formulae : 147 ( 22 unt; 0 def)
% Number of atoms : 560 ( 47 equ)
% Maximal formula atoms : 22 ( 3 avg)
% Number of connectives : 691 ( 278 ~; 318 |; 70 &)
% ( 4 <=>; 21 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 11 ( 9 usr; 1 prp; 0-3 aty)
% Number of functors : 14 ( 14 usr; 4 con; 0-2 aty)
% Number of variables : 260 ( 18 sgn 138 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(2,axiom,
! [X1,X2,X3] :
( element(X3,powerset(cartesian_product2(X1,X2)))
=> relation(X3) ),
file('/tmp/tmpzA4N0U/sel_SEU339+1.p_1',cc1_relset_1) ).
fof(3,axiom,
! [X1] :
( rel_str(X1)
=> relation_of2_as_subset(the_InternalRel(X1),the_carrier(X1),the_carrier(X1)) ),
file('/tmp/tmpzA4N0U/sel_SEU339+1.p_1',dt_u1_orders_2) ).
fof(4,axiom,
! [X1,X2] :
( in(X1,X2)
=> element(X1,X2) ),
file('/tmp/tmpzA4N0U/sel_SEU339+1.p_1',t1_subset) ).
fof(8,axiom,
! [X1] :
( rel_str(X1)
=> ! [X2] :
( element(X2,the_carrier(X1))
=> ! [X3] :
( element(X3,the_carrier(X1))
=> ( related(X1,X2,X3)
<=> in(ordered_pair(X2,X3),the_InternalRel(X1)) ) ) ) ),
file('/tmp/tmpzA4N0U/sel_SEU339+1.p_1',d9_orders_2) ).
fof(12,axiom,
! [X1,X2,X3] :
( ( in(X1,X2)
& element(X2,powerset(X3)) )
=> element(X1,X3) ),
file('/tmp/tmpzA4N0U/sel_SEU339+1.p_1',t4_subset) ).
fof(13,axiom,
! [X1,X2] :
~ ( in(X1,X2)
& empty(X2) ),
file('/tmp/tmpzA4N0U/sel_SEU339+1.p_1',t7_boole) ).
fof(19,axiom,
empty(empty_set),
file('/tmp/tmpzA4N0U/sel_SEU339+1.p_1',fc1_xboole_0) ).
fof(20,axiom,
! [X1] :
( rel_str(X1)
=> ( antisymmetric_relstr(X1)
<=> is_antisymmetric_in(the_InternalRel(X1),the_carrier(X1)) ) ),
file('/tmp/tmpzA4N0U/sel_SEU339+1.p_1',d6_orders_2) ).
fof(22,axiom,
! [X1,X2,X3] :
~ ( in(X1,X2)
& element(X2,powerset(X3))
& empty(X3) ),
file('/tmp/tmpzA4N0U/sel_SEU339+1.p_1',t5_subset) ).
fof(23,conjecture,
! [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/tmpzA4N0U/sel_SEU339+1.p_1',t25_orders_2) ).
fof(29,axiom,
! [X1,X2,X3] :
( relation_of2_as_subset(X3,X1,X2)
=> element(X3,powerset(cartesian_product2(X1,X2))) ),
file('/tmp/tmpzA4N0U/sel_SEU339+1.p_1',dt_m2_relset_1) ).
fof(30,axiom,
! [X1] :
( relation(X1)
=> ! [X2] :
( is_antisymmetric_in(X1,X2)
<=> ! [X3,X4] :
( ( in(X3,X2)
& in(X4,X2)
& in(ordered_pair(X3,X4),X1)
& in(ordered_pair(X4,X3),X1) )
=> X3 = X4 ) ) ),
file('/tmp/tmpzA4N0U/sel_SEU339+1.p_1',d4_relat_2) ).
fof(34,axiom,
! [X1,X2,X3,X4] :
( in(ordered_pair(X1,X2),cartesian_product2(X3,X4))
<=> ( in(X1,X3)
& in(X2,X4) ) ),
file('/tmp/tmpzA4N0U/sel_SEU339+1.p_1',t106_zfmisc_1) ).
fof(39,axiom,
! [X1,X2] : ordered_pair(X1,X2) = unordered_pair(unordered_pair(X1,X2),singleton(X1)),
file('/tmp/tmpzA4N0U/sel_SEU339+1.p_1',d5_tarski) ).
fof(40,axiom,
! [X1] :
( empty(X1)
=> X1 = empty_set ),
file('/tmp/tmpzA4N0U/sel_SEU339+1.p_1',t6_boole) ).
fof(41,axiom,
! [X1] :
? [X2] : element(X2,X1),
file('/tmp/tmpzA4N0U/sel_SEU339+1.p_1',existence_m1_subset_1) ).
fof(42,axiom,
! [X1,X2] :
( element(X1,X2)
=> ( empty(X2)
| in(X1,X2) ) ),
file('/tmp/tmpzA4N0U/sel_SEU339+1.p_1',t2_subset) ).
fof(45,axiom,
! [X1,X2] :
~ ( empty(X1)
& X1 != X2
& empty(X2) ),
file('/tmp/tmpzA4N0U/sel_SEU339+1.p_1',t8_boole) ).
fof(47,negated_conjecture,
~ ! [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(assume_negation,[status(cth)],[23]) ).
fof(56,plain,
! [X1,X2,X3] :
( ~ element(X3,powerset(cartesian_product2(X1,X2)))
| relation(X3) ),
inference(fof_nnf,[status(thm)],[2]) ).
fof(57,plain,
! [X4,X5,X6] :
( ~ element(X6,powerset(cartesian_product2(X4,X5)))
| relation(X6) ),
inference(variable_rename,[status(thm)],[56]) ).
cnf(58,plain,
( relation(X1)
| ~ element(X1,powerset(cartesian_product2(X2,X3))) ),
inference(split_conjunct,[status(thm)],[57]) ).
fof(59,plain,
! [X1] :
( ~ rel_str(X1)
| relation_of2_as_subset(the_InternalRel(X1),the_carrier(X1),the_carrier(X1)) ),
inference(fof_nnf,[status(thm)],[3]) ).
fof(60,plain,
! [X2] :
( ~ rel_str(X2)
| relation_of2_as_subset(the_InternalRel(X2),the_carrier(X2),the_carrier(X2)) ),
inference(variable_rename,[status(thm)],[59]) ).
cnf(61,plain,
( relation_of2_as_subset(the_InternalRel(X1),the_carrier(X1),the_carrier(X1))
| ~ rel_str(X1) ),
inference(split_conjunct,[status(thm)],[60]) ).
fof(62,plain,
! [X1,X2] :
( ~ in(X1,X2)
| element(X1,X2) ),
inference(fof_nnf,[status(thm)],[4]) ).
fof(63,plain,
! [X3,X4] :
( ~ in(X3,X4)
| element(X3,X4) ),
inference(variable_rename,[status(thm)],[62]) ).
cnf(64,plain,
( element(X1,X2)
| ~ in(X1,X2) ),
inference(split_conjunct,[status(thm)],[63]) ).
fof(73,plain,
! [X1] :
( ~ rel_str(X1)
| ! [X2] :
( ~ element(X2,the_carrier(X1))
| ! [X3] :
( ~ element(X3,the_carrier(X1))
| ( ( ~ related(X1,X2,X3)
| in(ordered_pair(X2,X3),the_InternalRel(X1)) )
& ( ~ in(ordered_pair(X2,X3),the_InternalRel(X1))
| related(X1,X2,X3) ) ) ) ) ),
inference(fof_nnf,[status(thm)],[8]) ).
fof(74,plain,
! [X4] :
( ~ rel_str(X4)
| ! [X5] :
( ~ element(X5,the_carrier(X4))
| ! [X6] :
( ~ element(X6,the_carrier(X4))
| ( ( ~ related(X4,X5,X6)
| in(ordered_pair(X5,X6),the_InternalRel(X4)) )
& ( ~ in(ordered_pair(X5,X6),the_InternalRel(X4))
| related(X4,X5,X6) ) ) ) ) ),
inference(variable_rename,[status(thm)],[73]) ).
fof(75,plain,
! [X4,X5,X6] :
( ~ element(X6,the_carrier(X4))
| ( ( ~ related(X4,X5,X6)
| in(ordered_pair(X5,X6),the_InternalRel(X4)) )
& ( ~ in(ordered_pair(X5,X6),the_InternalRel(X4))
| related(X4,X5,X6) ) )
| ~ element(X5,the_carrier(X4))
| ~ rel_str(X4) ),
inference(shift_quantors,[status(thm)],[74]) ).
fof(76,plain,
! [X4,X5,X6] :
( ( ~ related(X4,X5,X6)
| in(ordered_pair(X5,X6),the_InternalRel(X4))
| ~ element(X6,the_carrier(X4))
| ~ element(X5,the_carrier(X4))
| ~ rel_str(X4) )
& ( ~ in(ordered_pair(X5,X6),the_InternalRel(X4))
| related(X4,X5,X6)
| ~ element(X6,the_carrier(X4))
| ~ element(X5,the_carrier(X4))
| ~ rel_str(X4) ) ),
inference(distribute,[status(thm)],[75]) ).
cnf(78,plain,
( in(ordered_pair(X2,X3),the_InternalRel(X1))
| ~ rel_str(X1)
| ~ element(X2,the_carrier(X1))
| ~ element(X3,the_carrier(X1))
| ~ related(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[76]) ).
fof(89,plain,
! [X1,X2,X3] :
( ~ in(X1,X2)
| ~ element(X2,powerset(X3))
| element(X1,X3) ),
inference(fof_nnf,[status(thm)],[12]) ).
fof(90,plain,
! [X4,X5,X6] :
( ~ in(X4,X5)
| ~ element(X5,powerset(X6))
| element(X4,X6) ),
inference(variable_rename,[status(thm)],[89]) ).
cnf(91,plain,
( element(X1,X2)
| ~ element(X3,powerset(X2))
| ~ in(X1,X3) ),
inference(split_conjunct,[status(thm)],[90]) ).
fof(92,plain,
! [X1,X2] :
( ~ in(X1,X2)
| ~ empty(X2) ),
inference(fof_nnf,[status(thm)],[13]) ).
fof(93,plain,
! [X3,X4] :
( ~ in(X3,X4)
| ~ empty(X4) ),
inference(variable_rename,[status(thm)],[92]) ).
cnf(94,plain,
( ~ empty(X1)
| ~ in(X2,X1) ),
inference(split_conjunct,[status(thm)],[93]) ).
cnf(106,plain,
empty(empty_set),
inference(split_conjunct,[status(thm)],[19]) ).
fof(107,plain,
! [X1] :
( ~ rel_str(X1)
| ( ( ~ antisymmetric_relstr(X1)
| is_antisymmetric_in(the_InternalRel(X1),the_carrier(X1)) )
& ( ~ is_antisymmetric_in(the_InternalRel(X1),the_carrier(X1))
| antisymmetric_relstr(X1) ) ) ),
inference(fof_nnf,[status(thm)],[20]) ).
fof(108,plain,
! [X2] :
( ~ rel_str(X2)
| ( ( ~ antisymmetric_relstr(X2)
| is_antisymmetric_in(the_InternalRel(X2),the_carrier(X2)) )
& ( ~ is_antisymmetric_in(the_InternalRel(X2),the_carrier(X2))
| antisymmetric_relstr(X2) ) ) ),
inference(variable_rename,[status(thm)],[107]) ).
fof(109,plain,
! [X2] :
( ( ~ antisymmetric_relstr(X2)
| is_antisymmetric_in(the_InternalRel(X2),the_carrier(X2))
| ~ rel_str(X2) )
& ( ~ is_antisymmetric_in(the_InternalRel(X2),the_carrier(X2))
| antisymmetric_relstr(X2)
| ~ rel_str(X2) ) ),
inference(distribute,[status(thm)],[108]) ).
cnf(111,plain,
( is_antisymmetric_in(the_InternalRel(X1),the_carrier(X1))
| ~ rel_str(X1)
| ~ antisymmetric_relstr(X1) ),
inference(split_conjunct,[status(thm)],[109]) ).
fof(115,plain,
! [X1,X2,X3] :
( ~ in(X1,X2)
| ~ element(X2,powerset(X3))
| ~ empty(X3) ),
inference(fof_nnf,[status(thm)],[22]) ).
fof(116,plain,
! [X4,X5,X6] :
( ~ in(X4,X5)
| ~ element(X5,powerset(X6))
| ~ empty(X6) ),
inference(variable_rename,[status(thm)],[115]) ).
cnf(117,plain,
( ~ empty(X1)
| ~ element(X2,powerset(X1))
| ~ in(X3,X2) ),
inference(split_conjunct,[status(thm)],[116]) ).
fof(118,negated_conjecture,
? [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)],[47]) ).
fof(119,negated_conjecture,
? [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)],[118]) ).
fof(120,negated_conjecture,
( antisymmetric_relstr(esk5_0)
& rel_str(esk5_0)
& element(esk6_0,the_carrier(esk5_0))
& element(esk7_0,the_carrier(esk5_0))
& related(esk5_0,esk6_0,esk7_0)
& related(esk5_0,esk7_0,esk6_0)
& esk6_0 != esk7_0 ),
inference(skolemize,[status(esa)],[119]) ).
cnf(121,negated_conjecture,
esk6_0 != esk7_0,
inference(split_conjunct,[status(thm)],[120]) ).
cnf(122,negated_conjecture,
related(esk5_0,esk7_0,esk6_0),
inference(split_conjunct,[status(thm)],[120]) ).
cnf(123,negated_conjecture,
related(esk5_0,esk6_0,esk7_0),
inference(split_conjunct,[status(thm)],[120]) ).
cnf(124,negated_conjecture,
element(esk7_0,the_carrier(esk5_0)),
inference(split_conjunct,[status(thm)],[120]) ).
cnf(125,negated_conjecture,
element(esk6_0,the_carrier(esk5_0)),
inference(split_conjunct,[status(thm)],[120]) ).
cnf(126,negated_conjecture,
rel_str(esk5_0),
inference(split_conjunct,[status(thm)],[120]) ).
cnf(127,negated_conjecture,
antisymmetric_relstr(esk5_0),
inference(split_conjunct,[status(thm)],[120]) ).
fof(138,plain,
! [X1,X2,X3] :
( ~ relation_of2_as_subset(X3,X1,X2)
| element(X3,powerset(cartesian_product2(X1,X2))) ),
inference(fof_nnf,[status(thm)],[29]) ).
fof(139,plain,
! [X4,X5,X6] :
( ~ relation_of2_as_subset(X6,X4,X5)
| element(X6,powerset(cartesian_product2(X4,X5))) ),
inference(variable_rename,[status(thm)],[138]) ).
cnf(140,plain,
( element(X1,powerset(cartesian_product2(X2,X3)))
| ~ relation_of2_as_subset(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[139]) ).
fof(141,plain,
! [X1] :
( ~ relation(X1)
| ! [X2] :
( ( ~ is_antisymmetric_in(X1,X2)
| ! [X3,X4] :
( ~ in(X3,X2)
| ~ in(X4,X2)
| ~ in(ordered_pair(X3,X4),X1)
| ~ in(ordered_pair(X4,X3),X1)
| X3 = X4 ) )
& ( ? [X3,X4] :
( in(X3,X2)
& in(X4,X2)
& in(ordered_pair(X3,X4),X1)
& in(ordered_pair(X4,X3),X1)
& X3 != X4 )
| is_antisymmetric_in(X1,X2) ) ) ),
inference(fof_nnf,[status(thm)],[30]) ).
fof(142,plain,
! [X5] :
( ~ relation(X5)
| ! [X6] :
( ( ~ is_antisymmetric_in(X5,X6)
| ! [X7,X8] :
( ~ in(X7,X6)
| ~ in(X8,X6)
| ~ in(ordered_pair(X7,X8),X5)
| ~ in(ordered_pair(X8,X7),X5)
| X7 = X8 ) )
& ( ? [X9,X10] :
( in(X9,X6)
& in(X10,X6)
& in(ordered_pair(X9,X10),X5)
& in(ordered_pair(X10,X9),X5)
& X9 != X10 )
| is_antisymmetric_in(X5,X6) ) ) ),
inference(variable_rename,[status(thm)],[141]) ).
fof(143,plain,
! [X5] :
( ~ relation(X5)
| ! [X6] :
( ( ~ is_antisymmetric_in(X5,X6)
| ! [X7,X8] :
( ~ in(X7,X6)
| ~ in(X8,X6)
| ~ in(ordered_pair(X7,X8),X5)
| ~ in(ordered_pair(X8,X7),X5)
| X7 = X8 ) )
& ( ( in(esk8_2(X5,X6),X6)
& in(esk9_2(X5,X6),X6)
& in(ordered_pair(esk8_2(X5,X6),esk9_2(X5,X6)),X5)
& in(ordered_pair(esk9_2(X5,X6),esk8_2(X5,X6)),X5)
& esk8_2(X5,X6) != esk9_2(X5,X6) )
| is_antisymmetric_in(X5,X6) ) ) ),
inference(skolemize,[status(esa)],[142]) ).
fof(144,plain,
! [X5,X6,X7,X8] :
( ( ( ~ in(X7,X6)
| ~ in(X8,X6)
| ~ in(ordered_pair(X7,X8),X5)
| ~ in(ordered_pair(X8,X7),X5)
| X7 = X8
| ~ is_antisymmetric_in(X5,X6) )
& ( ( in(esk8_2(X5,X6),X6)
& in(esk9_2(X5,X6),X6)
& in(ordered_pair(esk8_2(X5,X6),esk9_2(X5,X6)),X5)
& in(ordered_pair(esk9_2(X5,X6),esk8_2(X5,X6)),X5)
& esk8_2(X5,X6) != esk9_2(X5,X6) )
| is_antisymmetric_in(X5,X6) ) )
| ~ relation(X5) ),
inference(shift_quantors,[status(thm)],[143]) ).
fof(145,plain,
! [X5,X6,X7,X8] :
( ( ~ in(X7,X6)
| ~ in(X8,X6)
| ~ in(ordered_pair(X7,X8),X5)
| ~ in(ordered_pair(X8,X7),X5)
| X7 = X8
| ~ is_antisymmetric_in(X5,X6)
| ~ relation(X5) )
& ( in(esk8_2(X5,X6),X6)
| is_antisymmetric_in(X5,X6)
| ~ relation(X5) )
& ( in(esk9_2(X5,X6),X6)
| is_antisymmetric_in(X5,X6)
| ~ relation(X5) )
& ( in(ordered_pair(esk8_2(X5,X6),esk9_2(X5,X6)),X5)
| is_antisymmetric_in(X5,X6)
| ~ relation(X5) )
& ( in(ordered_pair(esk9_2(X5,X6),esk8_2(X5,X6)),X5)
| is_antisymmetric_in(X5,X6)
| ~ relation(X5) )
& ( esk8_2(X5,X6) != esk9_2(X5,X6)
| is_antisymmetric_in(X5,X6)
| ~ relation(X5) ) ),
inference(distribute,[status(thm)],[144]) ).
cnf(151,plain,
( X3 = X4
| ~ relation(X1)
| ~ is_antisymmetric_in(X1,X2)
| ~ in(ordered_pair(X4,X3),X1)
| ~ in(ordered_pair(X3,X4),X1)
| ~ in(X4,X2)
| ~ in(X3,X2) ),
inference(split_conjunct,[status(thm)],[145]) ).
fof(157,plain,
! [X1,X2,X3,X4] :
( ( ~ in(ordered_pair(X1,X2),cartesian_product2(X3,X4))
| ( in(X1,X3)
& in(X2,X4) ) )
& ( ~ in(X1,X3)
| ~ in(X2,X4)
| in(ordered_pair(X1,X2),cartesian_product2(X3,X4)) ) ),
inference(fof_nnf,[status(thm)],[34]) ).
fof(158,plain,
! [X5,X6,X7,X8] :
( ( ~ in(ordered_pair(X5,X6),cartesian_product2(X7,X8))
| ( in(X5,X7)
& in(X6,X8) ) )
& ( ~ in(X5,X7)
| ~ in(X6,X8)
| in(ordered_pair(X5,X6),cartesian_product2(X7,X8)) ) ),
inference(variable_rename,[status(thm)],[157]) ).
fof(159,plain,
! [X5,X6,X7,X8] :
( ( in(X5,X7)
| ~ in(ordered_pair(X5,X6),cartesian_product2(X7,X8)) )
& ( in(X6,X8)
| ~ in(ordered_pair(X5,X6),cartesian_product2(X7,X8)) )
& ( ~ in(X5,X7)
| ~ in(X6,X8)
| in(ordered_pair(X5,X6),cartesian_product2(X7,X8)) ) ),
inference(distribute,[status(thm)],[158]) ).
cnf(161,plain,
( in(X2,X4)
| ~ in(ordered_pair(X1,X2),cartesian_product2(X3,X4)) ),
inference(split_conjunct,[status(thm)],[159]) ).
fof(172,plain,
! [X3,X4] : ordered_pair(X3,X4) = unordered_pair(unordered_pair(X3,X4),singleton(X3)),
inference(variable_rename,[status(thm)],[39]) ).
cnf(173,plain,
ordered_pair(X1,X2) = unordered_pair(unordered_pair(X1,X2),singleton(X1)),
inference(split_conjunct,[status(thm)],[172]) ).
fof(174,plain,
! [X1] :
( ~ empty(X1)
| X1 = empty_set ),
inference(fof_nnf,[status(thm)],[40]) ).
fof(175,plain,
! [X2] :
( ~ empty(X2)
| X2 = empty_set ),
inference(variable_rename,[status(thm)],[174]) ).
cnf(176,plain,
( X1 = empty_set
| ~ empty(X1) ),
inference(split_conjunct,[status(thm)],[175]) ).
fof(177,plain,
! [X3] :
? [X4] : element(X4,X3),
inference(variable_rename,[status(thm)],[41]) ).
fof(178,plain,
! [X3] : element(esk12_1(X3),X3),
inference(skolemize,[status(esa)],[177]) ).
cnf(179,plain,
element(esk12_1(X1),X1),
inference(split_conjunct,[status(thm)],[178]) ).
fof(180,plain,
! [X1,X2] :
( ~ element(X1,X2)
| empty(X2)
| in(X1,X2) ),
inference(fof_nnf,[status(thm)],[42]) ).
fof(181,plain,
! [X3,X4] :
( ~ element(X3,X4)
| empty(X4)
| in(X3,X4) ),
inference(variable_rename,[status(thm)],[180]) ).
cnf(182,plain,
( in(X1,X2)
| empty(X2)
| ~ element(X1,X2) ),
inference(split_conjunct,[status(thm)],[181]) ).
fof(188,plain,
! [X1,X2] :
( ~ empty(X1)
| X1 = X2
| ~ empty(X2) ),
inference(fof_nnf,[status(thm)],[45]) ).
fof(189,plain,
! [X3,X4] :
( ~ empty(X3)
| X3 = X4
| ~ empty(X4) ),
inference(variable_rename,[status(thm)],[188]) ).
cnf(190,plain,
( X2 = X1
| ~ empty(X1)
| ~ empty(X2) ),
inference(split_conjunct,[status(thm)],[189]) ).
cnf(194,plain,
( in(X2,X4)
| ~ in(unordered_pair(unordered_pair(X1,X2),singleton(X1)),cartesian_product2(X3,X4)) ),
inference(rw,[status(thm)],[161,173,theory(equality)]),
[unfolding] ).
cnf(200,plain,
( in(unordered_pair(unordered_pair(X2,X3),singleton(X2)),the_InternalRel(X1))
| ~ rel_str(X1)
| ~ related(X1,X2,X3)
| ~ element(X3,the_carrier(X1))
| ~ element(X2,the_carrier(X1)) ),
inference(rw,[status(thm)],[78,173,theory(equality)]),
[unfolding] ).
cnf(201,plain,
( X3 = X4
| ~ relation(X1)
| ~ in(X4,X2)
| ~ in(X3,X2)
| ~ is_antisymmetric_in(X1,X2)
| ~ in(unordered_pair(unordered_pair(X4,X3),singleton(X4)),X1)
| ~ in(unordered_pair(unordered_pair(X3,X4),singleton(X3)),X1) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[151,173,theory(equality)]),173,theory(equality)]),
[unfolding] ).
cnf(212,negated_conjecture,
( empty(the_carrier(esk5_0))
| in(esk6_0,the_carrier(esk5_0)) ),
inference(spm,[status(thm)],[182,125,theory(equality)]) ).
cnf(214,plain,
( empty(X1)
| in(esk12_1(X1),X1) ),
inference(spm,[status(thm)],[182,179,theory(equality)]) ).
cnf(226,plain,
( element(X1,X2)
| ~ in(X1,esk12_1(powerset(X2))) ),
inference(spm,[status(thm)],[91,179,theory(equality)]) ).
cnf(231,plain,
( relation(X1)
| ~ relation_of2_as_subset(X1,X2,X3) ),
inference(spm,[status(thm)],[58,140,theory(equality)]) ).
cnf(232,plain,
( element(X1,cartesian_product2(X2,X3))
| ~ in(X1,X4)
| ~ relation_of2_as_subset(X4,X2,X3) ),
inference(spm,[status(thm)],[91,140,theory(equality)]) ).
cnf(236,plain,
( ~ empty(X1)
| ~ in(X2,esk12_1(powerset(X1))) ),
inference(spm,[status(thm)],[117,179,theory(equality)]) ).
cnf(263,plain,
( ~ empty(the_InternalRel(X1))
| ~ related(X1,X2,X3)
| ~ rel_str(X1)
| ~ element(X3,the_carrier(X1))
| ~ element(X2,the_carrier(X1)) ),
inference(spm,[status(thm)],[94,200,theory(equality)]) ).
cnf(281,plain,
( X1 = X2
| ~ is_antisymmetric_in(the_InternalRel(X3),X4)
| ~ in(unordered_pair(unordered_pair(X1,X2),singleton(X1)),the_InternalRel(X3))
| ~ in(X2,X4)
| ~ in(X1,X4)
| ~ relation(the_InternalRel(X3))
| ~ related(X3,X2,X1)
| ~ rel_str(X3)
| ~ element(X1,the_carrier(X3))
| ~ element(X2,the_carrier(X3)) ),
inference(spm,[status(thm)],[201,200,theory(equality)]) ).
cnf(306,negated_conjecture,
( X1 = the_carrier(esk5_0)
| in(esk6_0,the_carrier(esk5_0))
| ~ empty(X1) ),
inference(spm,[status(thm)],[190,212,theory(equality)]) ).
cnf(361,plain,
( relation(the_InternalRel(X1))
| ~ rel_str(X1) ),
inference(spm,[status(thm)],[231,61,theory(equality)]) ).
cnf(376,plain,
( empty(esk12_1(powerset(X1)))
| ~ empty(X1) ),
inference(spm,[status(thm)],[236,214,theory(equality)]) ).
cnf(381,plain,
( element(esk12_1(esk12_1(powerset(X1))),X1)
| empty(esk12_1(powerset(X1))) ),
inference(spm,[status(thm)],[226,214,theory(equality)]) ).
cnf(384,negated_conjecture,
( esk12_1(powerset(X1)) = the_carrier(esk5_0)
| in(esk6_0,the_carrier(esk5_0))
| ~ empty(X1) ),
inference(spm,[status(thm)],[306,376,theory(equality)]) ).
cnf(460,negated_conjecture,
( in(esk6_0,the_carrier(esk5_0))
| ~ empty(X1)
| ~ in(X2,the_carrier(esk5_0)) ),
inference(spm,[status(thm)],[236,384,theory(equality)]) ).
cnf(475,plain,
( element(X1,cartesian_product2(the_carrier(X2),the_carrier(X2)))
| ~ in(X1,the_InternalRel(X2))
| ~ rel_str(X2) ),
inference(spm,[status(thm)],[232,61,theory(equality)]) ).
cnf(538,plain,
( empty(X1)
| in(esk12_1(esk12_1(powerset(X1))),X1)
| empty(esk12_1(powerset(X1))) ),
inference(spm,[status(thm)],[182,381,theory(equality)]) ).
cnf(563,negated_conjecture,
( ~ empty(the_InternalRel(esk5_0))
| ~ rel_str(esk5_0)
| ~ element(esk7_0,the_carrier(esk5_0))
| ~ element(esk6_0,the_carrier(esk5_0)) ),
inference(spm,[status(thm)],[263,123,theory(equality)]) ).
cnf(565,negated_conjecture,
( ~ empty(the_InternalRel(esk5_0))
| $false
| ~ element(esk7_0,the_carrier(esk5_0))
| ~ element(esk6_0,the_carrier(esk5_0)) ),
inference(rw,[status(thm)],[563,126,theory(equality)]) ).
cnf(566,negated_conjecture,
( ~ empty(the_InternalRel(esk5_0))
| $false
| $false
| ~ element(esk6_0,the_carrier(esk5_0)) ),
inference(rw,[status(thm)],[565,124,theory(equality)]) ).
cnf(567,negated_conjecture,
( ~ empty(the_InternalRel(esk5_0))
| $false
| $false
| $false ),
inference(rw,[status(thm)],[566,125,theory(equality)]) ).
cnf(568,negated_conjecture,
~ empty(the_InternalRel(esk5_0)),
inference(cn,[status(thm)],[567,theory(equality)]) ).
cnf(701,plain,
( empty(cartesian_product2(the_carrier(X1),the_carrier(X1)))
| in(X2,cartesian_product2(the_carrier(X1),the_carrier(X1)))
| ~ in(X2,the_InternalRel(X1))
| ~ rel_str(X1) ),
inference(spm,[status(thm)],[182,475,theory(equality)]) ).
cnf(1190,plain,
( empty(esk12_1(powerset(X1)))
| in(esk12_1(esk12_1(powerset(X1))),X1) ),
inference(csr,[status(thm)],[538,376]) ).
cnf(1207,negated_conjecture,
( in(esk6_0,the_carrier(esk5_0))
| empty(esk12_1(powerset(the_carrier(esk5_0))))
| ~ empty(X1) ),
inference(spm,[status(thm)],[460,1190,theory(equality)]) ).
cnf(1435,plain,
( X1 = X2
| ~ is_antisymmetric_in(the_InternalRel(X3),X4)
| ~ related(X3,X2,X1)
| ~ in(unordered_pair(unordered_pair(X1,X2),singleton(X1)),the_InternalRel(X3))
| ~ in(X2,X4)
| ~ in(X1,X4)
| ~ rel_str(X3)
| ~ element(X1,the_carrier(X3))
| ~ element(X2,the_carrier(X3)) ),
inference(csr,[status(thm)],[281,361]) ).
cnf(1440,plain,
( X1 = X2
| ~ is_antisymmetric_in(the_InternalRel(X3),X4)
| ~ related(X3,X2,X1)
| ~ in(X2,X4)
| ~ in(X1,X4)
| ~ rel_str(X3)
| ~ element(X1,the_carrier(X3))
| ~ element(X2,the_carrier(X3))
| ~ related(X3,X1,X2) ),
inference(spm,[status(thm)],[1435,200,theory(equality)]) ).
cnf(1562,negated_conjecture,
( empty(esk12_1(powerset(the_carrier(esk5_0))))
| in(esk6_0,the_carrier(esk5_0)) ),
inference(spm,[status(thm)],[1207,106,theory(equality)]) ).
cnf(1573,negated_conjecture,
( esk12_1(powerset(the_carrier(esk5_0))) = the_carrier(esk5_0)
| in(esk6_0,the_carrier(esk5_0)) ),
inference(spm,[status(thm)],[306,1562,theory(equality)]) ).
cnf(1591,negated_conjecture,
( in(esk6_0,the_carrier(esk5_0))
| ~ empty(the_carrier(esk5_0))
| ~ in(X1,the_carrier(esk5_0)) ),
inference(spm,[status(thm)],[236,1573,theory(equality)]) ).
cnf(1639,negated_conjecture,
( in(esk6_0,the_carrier(esk5_0))
| ~ in(X1,the_carrier(esk5_0)) ),
inference(csr,[status(thm)],[1591,212]) ).
cnf(4440,plain,
( empty(cartesian_product2(the_carrier(X1),the_carrier(X1)))
| in(unordered_pair(unordered_pair(X2,X3),singleton(X2)),cartesian_product2(the_carrier(X1),the_carrier(X1)))
| ~ rel_str(X1)
| ~ related(X1,X2,X3)
| ~ element(X3,the_carrier(X1))
| ~ element(X2,the_carrier(X1)) ),
inference(spm,[status(thm)],[701,200,theory(equality)]) ).
cnf(12859,plain,
( X1 = X2
| ~ related(X3,X2,X1)
| ~ related(X3,X1,X2)
| ~ in(X2,the_carrier(X3))
| ~ in(X1,the_carrier(X3))
| ~ rel_str(X3)
| ~ element(X1,the_carrier(X3))
| ~ element(X2,the_carrier(X3))
| ~ antisymmetric_relstr(X3) ),
inference(spm,[status(thm)],[1440,111,theory(equality)]) ).
cnf(73316,plain,
( in(X1,the_carrier(X2))
| empty(cartesian_product2(the_carrier(X2),the_carrier(X2)))
| ~ related(X2,X3,X1)
| ~ rel_str(X2)
| ~ element(X1,the_carrier(X2))
| ~ element(X3,the_carrier(X2)) ),
inference(spm,[status(thm)],[194,4440,theory(equality)]) ).
cnf(228074,negated_conjecture,
( empty(cartesian_product2(the_carrier(esk5_0),the_carrier(esk5_0)))
| in(esk7_0,the_carrier(esk5_0))
| ~ rel_str(esk5_0)
| ~ element(esk7_0,the_carrier(esk5_0))
| ~ element(esk6_0,the_carrier(esk5_0)) ),
inference(spm,[status(thm)],[73316,123,theory(equality)]) ).
cnf(228078,negated_conjecture,
( empty(cartesian_product2(the_carrier(esk5_0),the_carrier(esk5_0)))
| in(esk7_0,the_carrier(esk5_0))
| $false
| ~ element(esk7_0,the_carrier(esk5_0))
| ~ element(esk6_0,the_carrier(esk5_0)) ),
inference(rw,[status(thm)],[228074,126,theory(equality)]) ).
cnf(228079,negated_conjecture,
( empty(cartesian_product2(the_carrier(esk5_0),the_carrier(esk5_0)))
| in(esk7_0,the_carrier(esk5_0))
| $false
| $false
| ~ element(esk6_0,the_carrier(esk5_0)) ),
inference(rw,[status(thm)],[228078,124,theory(equality)]) ).
cnf(228080,negated_conjecture,
( empty(cartesian_product2(the_carrier(esk5_0),the_carrier(esk5_0)))
| in(esk7_0,the_carrier(esk5_0))
| $false
| $false
| $false ),
inference(rw,[status(thm)],[228079,125,theory(equality)]) ).
cnf(228081,negated_conjecture,
( empty(cartesian_product2(the_carrier(esk5_0),the_carrier(esk5_0)))
| in(esk7_0,the_carrier(esk5_0)) ),
inference(cn,[status(thm)],[228080,theory(equality)]) ).
cnf(228086,negated_conjecture,
( empty_set = cartesian_product2(the_carrier(esk5_0),the_carrier(esk5_0))
| in(esk7_0,the_carrier(esk5_0)) ),
inference(spm,[status(thm)],[176,228081,theory(equality)]) ).
cnf(228206,negated_conjecture,
( element(X1,powerset(empty_set))
| in(esk7_0,the_carrier(esk5_0))
| ~ relation_of2_as_subset(X1,the_carrier(esk5_0),the_carrier(esk5_0)) ),
inference(spm,[status(thm)],[140,228086,theory(equality)]) ).
cnf(245917,negated_conjecture,
( in(esk7_0,the_carrier(esk5_0))
| element(the_InternalRel(esk5_0),powerset(empty_set))
| ~ rel_str(esk5_0) ),
inference(spm,[status(thm)],[228206,61,theory(equality)]) ).
cnf(245918,negated_conjecture,
( in(esk7_0,the_carrier(esk5_0))
| element(the_InternalRel(esk5_0),powerset(empty_set))
| $false ),
inference(rw,[status(thm)],[245917,126,theory(equality)]) ).
cnf(245919,negated_conjecture,
( in(esk7_0,the_carrier(esk5_0))
| element(the_InternalRel(esk5_0),powerset(empty_set)) ),
inference(cn,[status(thm)],[245918,theory(equality)]) ).
cnf(245922,negated_conjecture,
( in(esk7_0,the_carrier(esk5_0))
| ~ empty(empty_set)
| ~ in(X1,the_InternalRel(esk5_0)) ),
inference(spm,[status(thm)],[117,245919,theory(equality)]) ).
cnf(245926,negated_conjecture,
( in(esk7_0,the_carrier(esk5_0))
| $false
| ~ in(X1,the_InternalRel(esk5_0)) ),
inference(rw,[status(thm)],[245922,106,theory(equality)]) ).
cnf(245927,negated_conjecture,
( in(esk7_0,the_carrier(esk5_0))
| ~ in(X1,the_InternalRel(esk5_0)) ),
inference(cn,[status(thm)],[245926,theory(equality)]) ).
cnf(245942,negated_conjecture,
( in(esk7_0,the_carrier(esk5_0))
| empty(the_InternalRel(esk5_0)) ),
inference(spm,[status(thm)],[245927,214,theory(equality)]) ).
cnf(246021,negated_conjecture,
in(esk7_0,the_carrier(esk5_0)),
inference(sr,[status(thm)],[245942,568,theory(equality)]) ).
cnf(246051,negated_conjecture,
in(esk6_0,the_carrier(esk5_0)),
inference(spm,[status(thm)],[1639,246021,theory(equality)]) ).
cnf(247230,plain,
( X1 = X2
| ~ antisymmetric_relstr(X3)
| ~ related(X3,X2,X1)
| ~ related(X3,X1,X2)
| ~ in(X2,the_carrier(X3))
| ~ in(X1,the_carrier(X3))
| ~ rel_str(X3)
| ~ element(X1,the_carrier(X3)) ),
inference(csr,[status(thm)],[12859,64]) ).
cnf(247231,plain,
( X1 = X2
| ~ antisymmetric_relstr(X3)
| ~ related(X3,X2,X1)
| ~ related(X3,X1,X2)
| ~ in(X2,the_carrier(X3))
| ~ in(X1,the_carrier(X3))
| ~ rel_str(X3) ),
inference(csr,[status(thm)],[247230,64]) ).
cnf(247232,negated_conjecture,
( esk7_0 = esk6_0
| ~ antisymmetric_relstr(esk5_0)
| ~ related(esk5_0,esk7_0,esk6_0)
| ~ in(esk6_0,the_carrier(esk5_0))
| ~ in(esk7_0,the_carrier(esk5_0))
| ~ rel_str(esk5_0) ),
inference(spm,[status(thm)],[247231,123,theory(equality)]) ).
cnf(247236,negated_conjecture,
( esk7_0 = esk6_0
| $false
| ~ related(esk5_0,esk7_0,esk6_0)
| ~ in(esk6_0,the_carrier(esk5_0))
| ~ in(esk7_0,the_carrier(esk5_0))
| ~ rel_str(esk5_0) ),
inference(rw,[status(thm)],[247232,127,theory(equality)]) ).
cnf(247237,negated_conjecture,
( esk7_0 = esk6_0
| $false
| $false
| ~ in(esk6_0,the_carrier(esk5_0))
| ~ in(esk7_0,the_carrier(esk5_0))
| ~ rel_str(esk5_0) ),
inference(rw,[status(thm)],[247236,122,theory(equality)]) ).
cnf(247238,negated_conjecture,
( esk7_0 = esk6_0
| $false
| $false
| $false
| ~ in(esk7_0,the_carrier(esk5_0))
| ~ rel_str(esk5_0) ),
inference(rw,[status(thm)],[247237,246051,theory(equality)]) ).
cnf(247239,negated_conjecture,
( esk7_0 = esk6_0
| $false
| $false
| $false
| $false
| ~ rel_str(esk5_0) ),
inference(rw,[status(thm)],[247238,246021,theory(equality)]) ).
cnf(247240,negated_conjecture,
( esk7_0 = esk6_0
| $false
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[247239,126,theory(equality)]) ).
cnf(247241,negated_conjecture,
esk7_0 = esk6_0,
inference(cn,[status(thm)],[247240,theory(equality)]) ).
cnf(247242,negated_conjecture,
$false,
inference(sr,[status(thm)],[247241,121,theory(equality)]) ).
cnf(247243,negated_conjecture,
$false,
247242,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% % SZS status Started for /home/graph/tptp/TPTP/Problems/SEU/SEU339+1.p
% --creating new selector for []
% -running prover on /tmp/tmpzA4N0U/sel_SEU339+1.p_1 with time limit 29
% -prover status Theorem
% Problem SEU339+1.p solved in phase 0.
% % SZS status Theorem for /home/graph/tptp/TPTP/Problems/SEU/SEU339+1.p
% % SZS status Ended for /home/graph/tptp/TPTP/Problems/SEU/SEU339+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
%
%------------------------------------------------------------------------------