%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : SEU401+1 : TPTP v5.0.0. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : Source/sine.py -e eprover -t %d %s
% Computer : art05.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 08:21:50 EST 2010
% Result : Theorem 3.35s
% Output : CNFRefutation 3.35s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 3
% Syntax : Number of formulae : 71 ( 6 unt; 0 def)
% Number of atoms : 498 ( 137 equ)
% Maximal formula atoms : 52 ( 7 avg)
% Number of connectives : 684 ( 257 ~; 247 |; 161 &)
% ( 9 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 28 ( 7 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 12 ( 10 usr; 1 prp; 0-5 aty)
% Number of functors : 15 ( 15 usr; 5 con; 0-6 aty)
% Number of variables : 372 ( 38 sgn 103 !; 38 ?)
% Comments :
%------------------------------------------------------------------------------
fof(25,axiom,
! [X1,X2] :
( ! [X3] :
( in(X3,X1)
<=> in(X3,X2) )
=> X1 = X2 ),
file('/tmp/tmpE_tkZN/sel_SEU401+1.p_1',t2_tarski) ).
fof(38,conjecture,
! [X1,X2,X3] :
( ( ~ empty_carrier(X1)
& topological_space(X1)
& top_str(X1)
& ~ empty_carrier(X2)
& transitive_relstr(X2)
& directed_relstr(X2)
& net_str(X2,X1) )
=> ! [X4,X5,X6] :
( ( ! [X7] :
( in(X7,X5)
<=> ( in(X7,the_carrier(X2))
& ? [X8] :
( netstr_induced_subset(X8,X1,X2)
& ? [X9] :
( element(X9,the_carrier(X2))
& X4 = topstr_closure(X1,X8)
& X7 = X9
& X8 = relation_rng_as_subset(the_carrier(subnetstr_of_element(X1,X2,X9)),the_carrier(X1),the_mapping(X1,subnetstr_of_element(X1,X2,X9))) ) ) ) )
& ! [X7] :
( in(X7,X6)
<=> ( in(X7,the_carrier(X2))
& ? [X10] :
( netstr_induced_subset(X10,X1,X2)
& ? [X11] :
( element(X11,the_carrier(X2))
& X4 = topstr_closure(X1,X10)
& X7 = X11
& X10 = relation_rng_as_subset(the_carrier(subnetstr_of_element(X1,X2,X11)),the_carrier(X1),the_mapping(X1,subnetstr_of_element(X1,X2,X11))) ) ) ) ) )
=> X5 = X6 ) ),
file('/tmp/tmpE_tkZN/sel_SEU401+1.p_1',s2_xboole_0__e6_39_3__yellow19__1) ).
fof(70,negated_conjecture,
~ ! [X1,X2,X3] :
( ( ~ empty_carrier(X1)
& topological_space(X1)
& top_str(X1)
& ~ empty_carrier(X2)
& transitive_relstr(X2)
& directed_relstr(X2)
& net_str(X2,X1) )
=> ! [X4,X5,X6] :
( ( ! [X7] :
( in(X7,X5)
<=> ( in(X7,the_carrier(X2))
& ? [X8] :
( netstr_induced_subset(X8,X1,X2)
& ? [X9] :
( element(X9,the_carrier(X2))
& X4 = topstr_closure(X1,X8)
& X7 = X9
& X8 = relation_rng_as_subset(the_carrier(subnetstr_of_element(X1,X2,X9)),the_carrier(X1),the_mapping(X1,subnetstr_of_element(X1,X2,X9))) ) ) ) )
& ! [X7] :
( in(X7,X6)
<=> ( in(X7,the_carrier(X2))
& ? [X10] :
( netstr_induced_subset(X10,X1,X2)
& ? [X11] :
( element(X11,the_carrier(X2))
& X4 = topstr_closure(X1,X10)
& X7 = X11
& X10 = relation_rng_as_subset(the_carrier(subnetstr_of_element(X1,X2,X11)),the_carrier(X1),the_mapping(X1,subnetstr_of_element(X1,X2,X11))) ) ) ) ) )
=> X5 = X6 ) ),
inference(assume_negation,[status(cth)],[38]) ).
fof(87,negated_conjecture,
~ ! [X1,X2,X3] :
( ( ~ empty_carrier(X1)
& topological_space(X1)
& top_str(X1)
& ~ empty_carrier(X2)
& transitive_relstr(X2)
& directed_relstr(X2)
& net_str(X2,X1) )
=> ! [X4,X5,X6] :
( ( ! [X7] :
( in(X7,X5)
<=> ( in(X7,the_carrier(X2))
& ? [X8] :
( netstr_induced_subset(X8,X1,X2)
& ? [X9] :
( element(X9,the_carrier(X2))
& X4 = topstr_closure(X1,X8)
& X7 = X9
& X8 = relation_rng_as_subset(the_carrier(subnetstr_of_element(X1,X2,X9)),the_carrier(X1),the_mapping(X1,subnetstr_of_element(X1,X2,X9))) ) ) ) )
& ! [X7] :
( in(X7,X6)
<=> ( in(X7,the_carrier(X2))
& ? [X10] :
( netstr_induced_subset(X10,X1,X2)
& ? [X11] :
( element(X11,the_carrier(X2))
& X4 = topstr_closure(X1,X10)
& X7 = X11
& X10 = relation_rng_as_subset(the_carrier(subnetstr_of_element(X1,X2,X11)),the_carrier(X1),the_mapping(X1,subnetstr_of_element(X1,X2,X11))) ) ) ) ) )
=> X5 = X6 ) ),
inference(fof_simplification,[status(thm)],[70,theory(equality)]) ).
fof(98,plain,
! [X6,X5,X4,X2,X1] :
( epred1_5(X1,X2,X4,X5,X6)
=> ( ! [X7] :
( in(X7,X5)
<=> ( in(X7,the_carrier(X2))
& ? [X8] :
( netstr_induced_subset(X8,X1,X2)
& ? [X9] :
( element(X9,the_carrier(X2))
& X4 = topstr_closure(X1,X8)
& X7 = X9
& X8 = relation_rng_as_subset(the_carrier(subnetstr_of_element(X1,X2,X9)),the_carrier(X1),the_mapping(X1,subnetstr_of_element(X1,X2,X9))) ) ) ) )
& ! [X7] :
( in(X7,X6)
<=> ( in(X7,the_carrier(X2))
& ? [X10] :
( netstr_induced_subset(X10,X1,X2)
& ? [X11] :
( element(X11,the_carrier(X2))
& X4 = topstr_closure(X1,X10)
& X7 = X11
& X10 = relation_rng_as_subset(the_carrier(subnetstr_of_element(X1,X2,X11)),the_carrier(X1),the_mapping(X1,subnetstr_of_element(X1,X2,X11))) ) ) ) ) ) ),
introduced(definition) ).
fof(99,negated_conjecture,
~ ! [X1,X2,X3] :
( ( ~ empty_carrier(X1)
& topological_space(X1)
& top_str(X1)
& ~ empty_carrier(X2)
& transitive_relstr(X2)
& directed_relstr(X2)
& net_str(X2,X1) )
=> ! [X4,X5,X6] :
( epred1_5(X1,X2,X4,X5,X6)
=> X5 = X6 ) ),
inference(apply_def,[status(esa)],[87,98,theory(equality)]) ).
fof(217,plain,
! [X1,X2] :
( ? [X3] :
( ( ~ in(X3,X1)
| ~ in(X3,X2) )
& ( in(X3,X1)
| in(X3,X2) ) )
| X1 = X2 ),
inference(fof_nnf,[status(thm)],[25]) ).
fof(218,plain,
! [X4,X5] :
( ? [X6] :
( ( ~ in(X6,X4)
| ~ in(X6,X5) )
& ( in(X6,X4)
| in(X6,X5) ) )
| X4 = X5 ),
inference(variable_rename,[status(thm)],[217]) ).
fof(219,plain,
! [X4,X5] :
( ( ( ~ in(esk9_2(X4,X5),X4)
| ~ in(esk9_2(X4,X5),X5) )
& ( in(esk9_2(X4,X5),X4)
| in(esk9_2(X4,X5),X5) ) )
| X4 = X5 ),
inference(skolemize,[status(esa)],[218]) ).
fof(220,plain,
! [X4,X5] :
( ( ~ in(esk9_2(X4,X5),X4)
| ~ in(esk9_2(X4,X5),X5)
| X4 = X5 )
& ( in(esk9_2(X4,X5),X4)
| in(esk9_2(X4,X5),X5)
| X4 = X5 ) ),
inference(distribute,[status(thm)],[219]) ).
cnf(221,plain,
( X1 = X2
| in(esk9_2(X1,X2),X2)
| in(esk9_2(X1,X2),X1) ),
inference(split_conjunct,[status(thm)],[220]) ).
cnf(222,plain,
( X1 = X2
| ~ in(esk9_2(X1,X2),X2)
| ~ in(esk9_2(X1,X2),X1) ),
inference(split_conjunct,[status(thm)],[220]) ).
fof(267,negated_conjecture,
? [X1,X2,X3] :
( ~ empty_carrier(X1)
& topological_space(X1)
& top_str(X1)
& ~ empty_carrier(X2)
& transitive_relstr(X2)
& directed_relstr(X2)
& net_str(X2,X1)
& ? [X4,X5,X6] :
( epred1_5(X1,X2,X4,X5,X6)
& X5 != X6 ) ),
inference(fof_nnf,[status(thm)],[99]) ).
fof(268,negated_conjecture,
? [X7,X8,X9] :
( ~ empty_carrier(X7)
& topological_space(X7)
& top_str(X7)
& ~ empty_carrier(X8)
& transitive_relstr(X8)
& directed_relstr(X8)
& net_str(X8,X7)
& ? [X10,X11,X12] :
( epred1_5(X7,X8,X10,X11,X12)
& X11 != X12 ) ),
inference(variable_rename,[status(thm)],[267]) ).
fof(269,negated_conjecture,
( ~ empty_carrier(esk14_0)
& topological_space(esk14_0)
& top_str(esk14_0)
& ~ empty_carrier(esk15_0)
& transitive_relstr(esk15_0)
& directed_relstr(esk15_0)
& net_str(esk15_0,esk14_0)
& epred1_5(esk14_0,esk15_0,esk17_0,esk18_0,esk19_0)
& esk18_0 != esk19_0 ),
inference(skolemize,[status(esa)],[268]) ).
cnf(270,negated_conjecture,
esk18_0 != esk19_0,
inference(split_conjunct,[status(thm)],[269]) ).
cnf(271,negated_conjecture,
epred1_5(esk14_0,esk15_0,esk17_0,esk18_0,esk19_0),
inference(split_conjunct,[status(thm)],[269]) ).
fof(435,plain,
! [X6,X5,X4,X2,X1] :
( ~ epred1_5(X1,X2,X4,X5,X6)
| ( ! [X7] :
( ( ~ in(X7,X5)
| ( in(X7,the_carrier(X2))
& ? [X8] :
( netstr_induced_subset(X8,X1,X2)
& ? [X9] :
( element(X9,the_carrier(X2))
& X4 = topstr_closure(X1,X8)
& X7 = X9
& X8 = relation_rng_as_subset(the_carrier(subnetstr_of_element(X1,X2,X9)),the_carrier(X1),the_mapping(X1,subnetstr_of_element(X1,X2,X9))) ) ) ) )
& ( ~ in(X7,the_carrier(X2))
| ! [X8] :
( ~ netstr_induced_subset(X8,X1,X2)
| ! [X9] :
( ~ element(X9,the_carrier(X2))
| X4 != topstr_closure(X1,X8)
| X7 != X9
| X8 != relation_rng_as_subset(the_carrier(subnetstr_of_element(X1,X2,X9)),the_carrier(X1),the_mapping(X1,subnetstr_of_element(X1,X2,X9))) ) )
| in(X7,X5) ) )
& ! [X7] :
( ( ~ in(X7,X6)
| ( in(X7,the_carrier(X2))
& ? [X10] :
( netstr_induced_subset(X10,X1,X2)
& ? [X11] :
( element(X11,the_carrier(X2))
& X4 = topstr_closure(X1,X10)
& X7 = X11
& X10 = relation_rng_as_subset(the_carrier(subnetstr_of_element(X1,X2,X11)),the_carrier(X1),the_mapping(X1,subnetstr_of_element(X1,X2,X11))) ) ) ) )
& ( ~ in(X7,the_carrier(X2))
| ! [X10] :
( ~ netstr_induced_subset(X10,X1,X2)
| ! [X11] :
( ~ element(X11,the_carrier(X2))
| X4 != topstr_closure(X1,X10)
| X7 != X11
| X10 != relation_rng_as_subset(the_carrier(subnetstr_of_element(X1,X2,X11)),the_carrier(X1),the_mapping(X1,subnetstr_of_element(X1,X2,X11))) ) )
| in(X7,X6) ) ) ) ),
inference(fof_nnf,[status(thm)],[98]) ).
fof(436,plain,
! [X12,X13,X14,X15,X16] :
( ~ epred1_5(X16,X15,X14,X13,X12)
| ( ! [X17] :
( ( ~ in(X17,X13)
| ( in(X17,the_carrier(X15))
& ? [X18] :
( netstr_induced_subset(X18,X16,X15)
& ? [X19] :
( element(X19,the_carrier(X15))
& X14 = topstr_closure(X16,X18)
& X17 = X19
& X18 = relation_rng_as_subset(the_carrier(subnetstr_of_element(X16,X15,X19)),the_carrier(X16),the_mapping(X16,subnetstr_of_element(X16,X15,X19))) ) ) ) )
& ( ~ in(X17,the_carrier(X15))
| ! [X20] :
( ~ netstr_induced_subset(X20,X16,X15)
| ! [X21] :
( ~ element(X21,the_carrier(X15))
| X14 != topstr_closure(X16,X20)
| X17 != X21
| X20 != relation_rng_as_subset(the_carrier(subnetstr_of_element(X16,X15,X21)),the_carrier(X16),the_mapping(X16,subnetstr_of_element(X16,X15,X21))) ) )
| in(X17,X13) ) )
& ! [X22] :
( ( ~ in(X22,X12)
| ( in(X22,the_carrier(X15))
& ? [X23] :
( netstr_induced_subset(X23,X16,X15)
& ? [X24] :
( element(X24,the_carrier(X15))
& X14 = topstr_closure(X16,X23)
& X22 = X24
& X23 = relation_rng_as_subset(the_carrier(subnetstr_of_element(X16,X15,X24)),the_carrier(X16),the_mapping(X16,subnetstr_of_element(X16,X15,X24))) ) ) ) )
& ( ~ in(X22,the_carrier(X15))
| ! [X25] :
( ~ netstr_induced_subset(X25,X16,X15)
| ! [X26] :
( ~ element(X26,the_carrier(X15))
| X14 != topstr_closure(X16,X25)
| X22 != X26
| X25 != relation_rng_as_subset(the_carrier(subnetstr_of_element(X16,X15,X26)),the_carrier(X16),the_mapping(X16,subnetstr_of_element(X16,X15,X26))) ) )
| in(X22,X12) ) ) ) ),
inference(variable_rename,[status(thm)],[435]) ).
fof(437,plain,
! [X12,X13,X14,X15,X16] :
( ~ epred1_5(X16,X15,X14,X13,X12)
| ( ! [X17] :
( ( ~ in(X17,X13)
| ( in(X17,the_carrier(X15))
& netstr_induced_subset(esk28_6(X12,X13,X14,X15,X16,X17),X16,X15)
& element(esk29_6(X12,X13,X14,X15,X16,X17),the_carrier(X15))
& X14 = topstr_closure(X16,esk28_6(X12,X13,X14,X15,X16,X17))
& X17 = esk29_6(X12,X13,X14,X15,X16,X17)
& esk28_6(X12,X13,X14,X15,X16,X17) = relation_rng_as_subset(the_carrier(subnetstr_of_element(X16,X15,esk29_6(X12,X13,X14,X15,X16,X17))),the_carrier(X16),the_mapping(X16,subnetstr_of_element(X16,X15,esk29_6(X12,X13,X14,X15,X16,X17)))) ) )
& ( ~ in(X17,the_carrier(X15))
| ! [X20] :
( ~ netstr_induced_subset(X20,X16,X15)
| ! [X21] :
( ~ element(X21,the_carrier(X15))
| X14 != topstr_closure(X16,X20)
| X17 != X21
| X20 != relation_rng_as_subset(the_carrier(subnetstr_of_element(X16,X15,X21)),the_carrier(X16),the_mapping(X16,subnetstr_of_element(X16,X15,X21))) ) )
| in(X17,X13) ) )
& ! [X22] :
( ( ~ in(X22,X12)
| ( in(X22,the_carrier(X15))
& netstr_induced_subset(esk30_6(X12,X13,X14,X15,X16,X22),X16,X15)
& element(esk31_6(X12,X13,X14,X15,X16,X22),the_carrier(X15))
& X14 = topstr_closure(X16,esk30_6(X12,X13,X14,X15,X16,X22))
& X22 = esk31_6(X12,X13,X14,X15,X16,X22)
& esk30_6(X12,X13,X14,X15,X16,X22) = relation_rng_as_subset(the_carrier(subnetstr_of_element(X16,X15,esk31_6(X12,X13,X14,X15,X16,X22))),the_carrier(X16),the_mapping(X16,subnetstr_of_element(X16,X15,esk31_6(X12,X13,X14,X15,X16,X22)))) ) )
& ( ~ in(X22,the_carrier(X15))
| ! [X25] :
( ~ netstr_induced_subset(X25,X16,X15)
| ! [X26] :
( ~ element(X26,the_carrier(X15))
| X14 != topstr_closure(X16,X25)
| X22 != X26
| X25 != relation_rng_as_subset(the_carrier(subnetstr_of_element(X16,X15,X26)),the_carrier(X16),the_mapping(X16,subnetstr_of_element(X16,X15,X26))) ) )
| in(X22,X12) ) ) ) ),
inference(skolemize,[status(esa)],[436]) ).
fof(438,plain,
! [X12,X13,X14,X15,X16,X17,X20,X21,X22,X25,X26] :
( ( ( ~ element(X26,the_carrier(X15))
| X14 != topstr_closure(X16,X25)
| X22 != X26
| X25 != relation_rng_as_subset(the_carrier(subnetstr_of_element(X16,X15,X26)),the_carrier(X16),the_mapping(X16,subnetstr_of_element(X16,X15,X26)))
| ~ netstr_induced_subset(X25,X16,X15)
| ~ in(X22,the_carrier(X15))
| in(X22,X12) )
& ( ~ in(X22,X12)
| ( in(X22,the_carrier(X15))
& netstr_induced_subset(esk30_6(X12,X13,X14,X15,X16,X22),X16,X15)
& element(esk31_6(X12,X13,X14,X15,X16,X22),the_carrier(X15))
& X14 = topstr_closure(X16,esk30_6(X12,X13,X14,X15,X16,X22))
& X22 = esk31_6(X12,X13,X14,X15,X16,X22)
& esk30_6(X12,X13,X14,X15,X16,X22) = relation_rng_as_subset(the_carrier(subnetstr_of_element(X16,X15,esk31_6(X12,X13,X14,X15,X16,X22))),the_carrier(X16),the_mapping(X16,subnetstr_of_element(X16,X15,esk31_6(X12,X13,X14,X15,X16,X22)))) ) )
& ( ~ element(X21,the_carrier(X15))
| X14 != topstr_closure(X16,X20)
| X17 != X21
| X20 != relation_rng_as_subset(the_carrier(subnetstr_of_element(X16,X15,X21)),the_carrier(X16),the_mapping(X16,subnetstr_of_element(X16,X15,X21)))
| ~ netstr_induced_subset(X20,X16,X15)
| ~ in(X17,the_carrier(X15))
| in(X17,X13) )
& ( ~ in(X17,X13)
| ( in(X17,the_carrier(X15))
& netstr_induced_subset(esk28_6(X12,X13,X14,X15,X16,X17),X16,X15)
& element(esk29_6(X12,X13,X14,X15,X16,X17),the_carrier(X15))
& X14 = topstr_closure(X16,esk28_6(X12,X13,X14,X15,X16,X17))
& X17 = esk29_6(X12,X13,X14,X15,X16,X17)
& esk28_6(X12,X13,X14,X15,X16,X17) = relation_rng_as_subset(the_carrier(subnetstr_of_element(X16,X15,esk29_6(X12,X13,X14,X15,X16,X17))),the_carrier(X16),the_mapping(X16,subnetstr_of_element(X16,X15,esk29_6(X12,X13,X14,X15,X16,X17)))) ) ) )
| ~ epred1_5(X16,X15,X14,X13,X12) ),
inference(shift_quantors,[status(thm)],[437]) ).
fof(439,plain,
! [X12,X13,X14,X15,X16,X17,X20,X21,X22,X25,X26] :
( ( ~ element(X26,the_carrier(X15))
| X14 != topstr_closure(X16,X25)
| X22 != X26
| X25 != relation_rng_as_subset(the_carrier(subnetstr_of_element(X16,X15,X26)),the_carrier(X16),the_mapping(X16,subnetstr_of_element(X16,X15,X26)))
| ~ netstr_induced_subset(X25,X16,X15)
| ~ in(X22,the_carrier(X15))
| in(X22,X12)
| ~ epred1_5(X16,X15,X14,X13,X12) )
& ( in(X22,the_carrier(X15))
| ~ in(X22,X12)
| ~ epred1_5(X16,X15,X14,X13,X12) )
& ( netstr_induced_subset(esk30_6(X12,X13,X14,X15,X16,X22),X16,X15)
| ~ in(X22,X12)
| ~ epred1_5(X16,X15,X14,X13,X12) )
& ( element(esk31_6(X12,X13,X14,X15,X16,X22),the_carrier(X15))
| ~ in(X22,X12)
| ~ epred1_5(X16,X15,X14,X13,X12) )
& ( X14 = topstr_closure(X16,esk30_6(X12,X13,X14,X15,X16,X22))
| ~ in(X22,X12)
| ~ epred1_5(X16,X15,X14,X13,X12) )
& ( X22 = esk31_6(X12,X13,X14,X15,X16,X22)
| ~ in(X22,X12)
| ~ epred1_5(X16,X15,X14,X13,X12) )
& ( esk30_6(X12,X13,X14,X15,X16,X22) = relation_rng_as_subset(the_carrier(subnetstr_of_element(X16,X15,esk31_6(X12,X13,X14,X15,X16,X22))),the_carrier(X16),the_mapping(X16,subnetstr_of_element(X16,X15,esk31_6(X12,X13,X14,X15,X16,X22))))
| ~ in(X22,X12)
| ~ epred1_5(X16,X15,X14,X13,X12) )
& ( ~ element(X21,the_carrier(X15))
| X14 != topstr_closure(X16,X20)
| X17 != X21
| X20 != relation_rng_as_subset(the_carrier(subnetstr_of_element(X16,X15,X21)),the_carrier(X16),the_mapping(X16,subnetstr_of_element(X16,X15,X21)))
| ~ netstr_induced_subset(X20,X16,X15)
| ~ in(X17,the_carrier(X15))
| in(X17,X13)
| ~ epred1_5(X16,X15,X14,X13,X12) )
& ( in(X17,the_carrier(X15))
| ~ in(X17,X13)
| ~ epred1_5(X16,X15,X14,X13,X12) )
& ( netstr_induced_subset(esk28_6(X12,X13,X14,X15,X16,X17),X16,X15)
| ~ in(X17,X13)
| ~ epred1_5(X16,X15,X14,X13,X12) )
& ( element(esk29_6(X12,X13,X14,X15,X16,X17),the_carrier(X15))
| ~ in(X17,X13)
| ~ epred1_5(X16,X15,X14,X13,X12) )
& ( X14 = topstr_closure(X16,esk28_6(X12,X13,X14,X15,X16,X17))
| ~ in(X17,X13)
| ~ epred1_5(X16,X15,X14,X13,X12) )
& ( X17 = esk29_6(X12,X13,X14,X15,X16,X17)
| ~ in(X17,X13)
| ~ epred1_5(X16,X15,X14,X13,X12) )
& ( esk28_6(X12,X13,X14,X15,X16,X17) = relation_rng_as_subset(the_carrier(subnetstr_of_element(X16,X15,esk29_6(X12,X13,X14,X15,X16,X17))),the_carrier(X16),the_mapping(X16,subnetstr_of_element(X16,X15,esk29_6(X12,X13,X14,X15,X16,X17))))
| ~ in(X17,X13)
| ~ epred1_5(X16,X15,X14,X13,X12) ) ),
inference(distribute,[status(thm)],[438]) ).
cnf(440,plain,
( esk28_6(X5,X4,X3,X2,X1,X6) = relation_rng_as_subset(the_carrier(subnetstr_of_element(X1,X2,esk29_6(X5,X4,X3,X2,X1,X6))),the_carrier(X1),the_mapping(X1,subnetstr_of_element(X1,X2,esk29_6(X5,X4,X3,X2,X1,X6))))
| ~ epred1_5(X1,X2,X3,X4,X5)
| ~ in(X6,X4) ),
inference(split_conjunct,[status(thm)],[439]) ).
cnf(441,plain,
( X6 = esk29_6(X5,X4,X3,X2,X1,X6)
| ~ epred1_5(X1,X2,X3,X4,X5)
| ~ in(X6,X4) ),
inference(split_conjunct,[status(thm)],[439]) ).
cnf(442,plain,
( X3 = topstr_closure(X1,esk28_6(X5,X4,X3,X2,X1,X6))
| ~ epred1_5(X1,X2,X3,X4,X5)
| ~ in(X6,X4) ),
inference(split_conjunct,[status(thm)],[439]) ).
cnf(443,plain,
( element(esk29_6(X5,X4,X3,X2,X1,X6),the_carrier(X2))
| ~ epred1_5(X1,X2,X3,X4,X5)
| ~ in(X6,X4) ),
inference(split_conjunct,[status(thm)],[439]) ).
cnf(444,plain,
( netstr_induced_subset(esk28_6(X5,X4,X3,X2,X1,X6),X1,X2)
| ~ epred1_5(X1,X2,X3,X4,X5)
| ~ in(X6,X4) ),
inference(split_conjunct,[status(thm)],[439]) ).
cnf(445,plain,
( in(X6,the_carrier(X2))
| ~ epred1_5(X1,X2,X3,X4,X5)
| ~ in(X6,X4) ),
inference(split_conjunct,[status(thm)],[439]) ).
cnf(446,plain,
( in(X6,X4)
| ~ epred1_5(X1,X2,X3,X4,X5)
| ~ in(X6,the_carrier(X2))
| ~ netstr_induced_subset(X7,X1,X2)
| X7 != relation_rng_as_subset(the_carrier(subnetstr_of_element(X1,X2,X8)),the_carrier(X1),the_mapping(X1,subnetstr_of_element(X1,X2,X8)))
| X6 != X8
| X3 != topstr_closure(X1,X7)
| ~ element(X8,the_carrier(X2)) ),
inference(split_conjunct,[status(thm)],[439]) ).
cnf(447,plain,
( esk30_6(X5,X4,X3,X2,X1,X6) = relation_rng_as_subset(the_carrier(subnetstr_of_element(X1,X2,esk31_6(X5,X4,X3,X2,X1,X6))),the_carrier(X1),the_mapping(X1,subnetstr_of_element(X1,X2,esk31_6(X5,X4,X3,X2,X1,X6))))
| ~ epred1_5(X1,X2,X3,X4,X5)
| ~ in(X6,X5) ),
inference(split_conjunct,[status(thm)],[439]) ).
cnf(448,plain,
( X6 = esk31_6(X5,X4,X3,X2,X1,X6)
| ~ epred1_5(X1,X2,X3,X4,X5)
| ~ in(X6,X5) ),
inference(split_conjunct,[status(thm)],[439]) ).
cnf(449,plain,
( X3 = topstr_closure(X1,esk30_6(X5,X4,X3,X2,X1,X6))
| ~ epred1_5(X1,X2,X3,X4,X5)
| ~ in(X6,X5) ),
inference(split_conjunct,[status(thm)],[439]) ).
cnf(450,plain,
( element(esk31_6(X5,X4,X3,X2,X1,X6),the_carrier(X2))
| ~ epred1_5(X1,X2,X3,X4,X5)
| ~ in(X6,X5) ),
inference(split_conjunct,[status(thm)],[439]) ).
cnf(451,plain,
( netstr_induced_subset(esk30_6(X5,X4,X3,X2,X1,X6),X1,X2)
| ~ epred1_5(X1,X2,X3,X4,X5)
| ~ in(X6,X5) ),
inference(split_conjunct,[status(thm)],[439]) ).
cnf(452,plain,
( in(X6,the_carrier(X2))
| ~ epred1_5(X1,X2,X3,X4,X5)
| ~ in(X6,X5) ),
inference(split_conjunct,[status(thm)],[439]) ).
cnf(453,plain,
( in(X6,X5)
| ~ epred1_5(X1,X2,X3,X4,X5)
| ~ in(X6,the_carrier(X2))
| ~ netstr_induced_subset(X7,X1,X2)
| X7 != relation_rng_as_subset(the_carrier(subnetstr_of_element(X1,X2,X8)),the_carrier(X1),the_mapping(X1,subnetstr_of_element(X1,X2,X8)))
| X6 != X8
| X3 != topstr_closure(X1,X7)
| ~ element(X8,the_carrier(X2)) ),
inference(split_conjunct,[status(thm)],[439]) ).
cnf(490,negated_conjecture,
( in(X1,the_carrier(esk15_0))
| ~ in(X1,esk18_0) ),
inference(spm,[status(thm)],[445,271,theory(equality)]) ).
cnf(524,plain,
( element(X6,the_carrier(X4))
| ~ epred1_5(X5,X4,X3,X2,X1)
| ~ in(X6,X2) ),
inference(spm,[status(thm)],[443,441,theory(equality)]) ).
cnf(551,plain,
( relation_rng_as_subset(the_carrier(subnetstr_of_element(X1,X2,X6)),the_carrier(X1),the_mapping(X1,subnetstr_of_element(X1,X2,X6))) = esk28_6(X3,X4,X5,X2,X1,X6)
| ~ epred1_5(X1,X2,X5,X4,X3)
| ~ in(X6,X4) ),
inference(spm,[status(thm)],[440,441,theory(equality)]) ).
cnf(555,plain,
( in(X1,X2)
| relation_rng_as_subset(the_carrier(subnetstr_of_element(X3,X4,X1)),the_carrier(X3),the_mapping(X3,subnetstr_of_element(X3,X4,X1))) != X5
| topstr_closure(X3,X5) != X6
| ~ epred1_5(X3,X4,X6,X7,X2)
| ~ in(X1,the_carrier(X4))
| ~ netstr_induced_subset(X5,X3,X4)
| ~ element(X1,the_carrier(X4)) ),
inference(er,[status(thm)],[453,theory(equality)]) ).
cnf(556,plain,
( in(X1,X2)
| relation_rng_as_subset(the_carrier(subnetstr_of_element(X3,X4,X1)),the_carrier(X3),the_mapping(X3,subnetstr_of_element(X3,X4,X1))) != X5
| topstr_closure(X3,X5) != X6
| ~ epred1_5(X3,X4,X6,X2,X7)
| ~ in(X1,the_carrier(X4))
| ~ netstr_induced_subset(X5,X3,X4)
| ~ element(X1,the_carrier(X4)) ),
inference(er,[status(thm)],[446,theory(equality)]) ).
cnf(608,negated_conjecture,
( element(X1,the_carrier(esk15_0))
| ~ in(X1,esk18_0) ),
inference(spm,[status(thm)],[524,271,theory(equality)]) ).
cnf(1149,plain,
( topstr_closure(X1,relation_rng_as_subset(the_carrier(subnetstr_of_element(X1,X5,X6)),the_carrier(X1),the_mapping(X1,subnetstr_of_element(X1,X5,X6)))) = X4
| ~ epred1_5(X1,X5,X4,X3,X2)
| ~ in(X6,X3) ),
inference(spm,[status(thm)],[442,551,theory(equality)]) ).
cnf(1150,plain,
( netstr_induced_subset(relation_rng_as_subset(the_carrier(subnetstr_of_element(X5,X4,X6)),the_carrier(X5),the_mapping(X5,subnetstr_of_element(X5,X4,X6))),X5,X4)
| ~ epred1_5(X5,X4,X3,X2,X1)
| ~ in(X6,X2) ),
inference(spm,[status(thm)],[444,551,theory(equality)]) ).
cnf(1257,plain,
( in(X1,X2)
| topstr_closure(X3,relation_rng_as_subset(the_carrier(subnetstr_of_element(X3,X4,X1)),the_carrier(X3),the_mapping(X3,subnetstr_of_element(X3,X4,X1)))) != X5
| ~ epred1_5(X3,X4,X5,X6,X2)
| ~ in(X1,the_carrier(X4))
| ~ netstr_induced_subset(relation_rng_as_subset(the_carrier(subnetstr_of_element(X3,X4,X1)),the_carrier(X3),the_mapping(X3,subnetstr_of_element(X3,X4,X1))),X3,X4)
| ~ element(X1,the_carrier(X4)) ),
inference(er,[status(thm)],[555,theory(equality)]) ).
cnf(1270,plain,
( in(X1,X2)
| topstr_closure(X3,relation_rng_as_subset(the_carrier(subnetstr_of_element(X3,X4,X1)),the_carrier(X3),the_mapping(X3,subnetstr_of_element(X3,X4,X1)))) != X5
| ~ epred1_5(X3,X4,X5,X2,X6)
| ~ in(X1,the_carrier(X4))
| ~ netstr_induced_subset(relation_rng_as_subset(the_carrier(subnetstr_of_element(X3,X4,X1)),the_carrier(X3),the_mapping(X3,subnetstr_of_element(X3,X4,X1))),X3,X4)
| ~ element(X1,the_carrier(X4)) ),
inference(er,[status(thm)],[556,theory(equality)]) ).
cnf(1452,negated_conjecture,
( netstr_induced_subset(relation_rng_as_subset(the_carrier(subnetstr_of_element(esk14_0,esk15_0,X1)),the_carrier(esk14_0),the_mapping(esk14_0,subnetstr_of_element(esk14_0,esk15_0,X1))),esk14_0,esk15_0)
| ~ in(X1,esk18_0) ),
inference(spm,[status(thm)],[1150,271,theory(equality)]) ).
cnf(2254,negated_conjecture,
( topstr_closure(esk14_0,relation_rng_as_subset(the_carrier(subnetstr_of_element(esk14_0,esk15_0,X1)),the_carrier(esk14_0),the_mapping(esk14_0,subnetstr_of_element(esk14_0,esk15_0,X1)))) = esk17_0
| ~ in(X1,esk18_0) ),
inference(spm,[status(thm)],[1149,271,theory(equality)]) ).
cnf(4630,negated_conjecture,
( in(X1,X2)
| topstr_closure(esk14_0,relation_rng_as_subset(the_carrier(subnetstr_of_element(esk14_0,esk15_0,X1)),the_carrier(esk14_0),the_mapping(esk14_0,subnetstr_of_element(esk14_0,esk15_0,X1)))) != X3
| ~ epred1_5(esk14_0,esk15_0,X3,X4,X2)
| ~ in(X1,the_carrier(esk15_0))
| ~ element(X1,the_carrier(esk15_0))
| ~ in(X1,esk18_0) ),
inference(spm,[status(thm)],[1257,1452,theory(equality)]) ).
cnf(4777,plain,
( in(esk31_6(X1,X2,X3,X4,X5,X6),X7)
| topstr_closure(X5,esk30_6(X1,X2,X3,X4,X5,X6)) != X8
| ~ epred1_5(X5,X4,X8,X7,X9)
| ~ in(esk31_6(X1,X2,X3,X4,X5,X6),the_carrier(X4))
| ~ netstr_induced_subset(esk30_6(X1,X2,X3,X4,X5,X6),X5,X4)
| ~ element(esk31_6(X1,X2,X3,X4,X5,X6),the_carrier(X4))
| ~ epred1_5(X5,X4,X3,X2,X1)
| ~ in(X6,X1) ),
inference(spm,[status(thm)],[1270,447,theory(equality)]) ).
cnf(10678,negated_conjecture,
( in(X1,X2)
| topstr_closure(esk14_0,relation_rng_as_subset(the_carrier(subnetstr_of_element(esk14_0,esk15_0,X1)),the_carrier(esk14_0),the_mapping(esk14_0,subnetstr_of_element(esk14_0,esk15_0,X1)))) != X3
| ~ epred1_5(esk14_0,esk15_0,X3,X4,X2)
| ~ in(X1,the_carrier(esk15_0))
| ~ in(X1,esk18_0) ),
inference(csr,[status(thm)],[4630,608]) ).
cnf(10679,negated_conjecture,
( in(X1,X2)
| topstr_closure(esk14_0,relation_rng_as_subset(the_carrier(subnetstr_of_element(esk14_0,esk15_0,X1)),the_carrier(esk14_0),the_mapping(esk14_0,subnetstr_of_element(esk14_0,esk15_0,X1)))) != X3
| ~ epred1_5(esk14_0,esk15_0,X3,X4,X2)
| ~ in(X1,esk18_0) ),
inference(csr,[status(thm)],[10678,490]) ).
cnf(10688,negated_conjecture,
( in(X1,X2)
| esk17_0 != X3
| ~ epred1_5(esk14_0,esk15_0,X3,X4,X2)
| ~ in(X1,esk18_0) ),
inference(spm,[status(thm)],[10679,2254,theory(equality)]) ).
cnf(10701,negated_conjecture,
( in(X1,esk19_0)
| ~ in(X1,esk18_0) ),
inference(spm,[status(thm)],[10688,271,theory(equality)]) ).
cnf(10704,negated_conjecture,
( X1 = esk19_0
| ~ in(esk9_2(X1,esk19_0),X1)
| ~ in(esk9_2(X1,esk19_0),esk18_0) ),
inference(spm,[status(thm)],[222,10701,theory(equality)]) ).
cnf(14442,plain,
( in(esk31_6(X1,X2,X3,X4,X5,X6),X7)
| topstr_closure(X5,esk30_6(X1,X2,X3,X4,X5,X6)) != X8
| ~ epred1_5(X5,X4,X3,X2,X1)
| ~ epred1_5(X5,X4,X8,X7,X9)
| ~ in(esk31_6(X1,X2,X3,X4,X5,X6),the_carrier(X4))
| ~ in(X6,X1)
| ~ netstr_induced_subset(esk30_6(X1,X2,X3,X4,X5,X6),X5,X4) ),
inference(csr,[status(thm)],[4777,450]) ).
cnf(14443,plain,
( in(esk31_6(X1,X2,X3,X4,X5,X6),X7)
| topstr_closure(X5,esk30_6(X1,X2,X3,X4,X5,X6)) != X8
| ~ epred1_5(X5,X4,X3,X2,X1)
| ~ epred1_5(X5,X4,X8,X7,X9)
| ~ in(esk31_6(X1,X2,X3,X4,X5,X6),the_carrier(X4))
| ~ in(X6,X1) ),
inference(csr,[status(thm)],[14442,451]) ).
cnf(14444,plain,
( in(X6,X7)
| topstr_closure(X5,esk30_6(X1,X2,X3,X4,X5,X6)) != X8
| ~ epred1_5(X5,X4,X8,X7,X9)
| ~ epred1_5(X5,X4,X3,X2,X1)
| ~ in(X6,the_carrier(X4))
| ~ in(X6,X1) ),
inference(spm,[status(thm)],[14443,448,theory(equality)]) ).
cnf(14465,plain,
( in(X6,X7)
| topstr_closure(X5,esk30_6(X1,X2,X3,X4,X5,X6)) != X8
| ~ epred1_5(X5,X4,X8,X7,X9)
| ~ epred1_5(X5,X4,X3,X2,X1)
| ~ in(X6,X1) ),
inference(csr,[status(thm)],[14444,452]) ).
cnf(14467,plain,
( in(X1,X2)
| X6 != X8
| ~ epred1_5(X3,X7,X8,X2,X9)
| ~ epred1_5(X3,X7,X6,X5,X4)
| ~ in(X1,X4) ),
inference(spm,[status(thm)],[14465,449,theory(equality)]) ).
cnf(14480,plain,
( in(X1,X2)
| ~ epred1_5(X3,X4,X5,X2,X6)
| ~ epred1_5(X3,X4,X5,X7,X8)
| ~ in(X1,X8) ),
inference(er,[status(thm)],[14467,theory(equality)]) ).
cnf(14481,negated_conjecture,
( in(X1,esk18_0)
| ~ epred1_5(esk14_0,esk15_0,esk17_0,X2,X3)
| ~ in(X1,X3) ),
inference(spm,[status(thm)],[14480,271,theory(equality)]) ).
cnf(14482,negated_conjecture,
( in(X1,esk18_0)
| ~ in(X1,esk19_0) ),
inference(spm,[status(thm)],[14481,271,theory(equality)]) ).
cnf(14484,negated_conjecture,
( in(esk9_2(X1,esk19_0),esk18_0)
| X1 = esk19_0
| in(esk9_2(X1,esk19_0),X1) ),
inference(spm,[status(thm)],[14482,221,theory(equality)]) ).
cnf(14509,negated_conjecture,
( esk18_0 = esk19_0
| in(esk9_2(esk18_0,esk19_0),esk18_0) ),
inference(ef,[status(thm)],[14484,theory(equality)]) ).
cnf(14517,negated_conjecture,
in(esk9_2(esk18_0,esk19_0),esk18_0),
inference(sr,[status(thm)],[14509,270,theory(equality)]) ).
cnf(14521,negated_conjecture,
( esk18_0 = esk19_0
| ~ in(esk9_2(esk18_0,esk19_0),esk18_0) ),
inference(spm,[status(thm)],[10704,14517,theory(equality)]) ).
cnf(14523,negated_conjecture,
( esk18_0 = esk19_0
| $false ),
inference(rw,[status(thm)],[14521,14517,theory(equality)]) ).
cnf(14524,negated_conjecture,
esk18_0 = esk19_0,
inference(cn,[status(thm)],[14523,theory(equality)]) ).
cnf(14525,negated_conjecture,
$false,
inference(sr,[status(thm)],[14524,270,theory(equality)]) ).
cnf(14526,negated_conjecture,
$false,
14525,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% % SZS status Started for /home/graph/tptp/TPTP/Problems/SEU/SEU401+1.p
% --creating new selector for []
% -running prover on /tmp/tmpE_tkZN/sel_SEU401+1.p_1 with time limit 29
% -prover status Theorem
% Problem SEU401+1.p solved in phase 0.
% % SZS status Theorem for /home/graph/tptp/TPTP/Problems/SEU/SEU401+1.p
% % SZS status Ended for /home/graph/tptp/TPTP/Problems/SEU/SEU401+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
%
%------------------------------------------------------------------------------