%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : SWW254+1 : TPTP v5.2.0. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : Source/sine.py -e eprover -t %d %s
% Computer : art07.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 Mar 6 15:25:43 EST 2011
% Result : Theorem 109.38s
% Output : CNFRefutation 109.38s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 14
% Syntax : Number of formulae : 66 ( 29 unt; 0 def)
% Number of atoms : 162 ( 20 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 167 ( 71 ~; 72 |; 10 &)
% ( 6 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-3 aty)
% Number of functors : 14 ( 14 usr; 6 con; 0-3 aty)
% Number of variables : 87 ( 11 sgn 57 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(69,conjecture,
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q____),v_w____)),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q____),c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)))),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))
<=> c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q____),v_w____)),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q____),c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)))) ),
file('/tmp/tmp0N6hNK/sel_SWW254+1.p_2',conj_0) ).
fof(100,axiom,
class_Fields_Olinordered__field(tc_RealDef_Oreal),
file('/tmp/tmp0N6hNK/sel_SWW254+1.p_2',arity_RealDef__Oreal__Fields_Olinordered__field) ).
fof(129,axiom,
hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_pa____),v_c____) != c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex),
file('/tmp/tmp0N6hNK/sel_SWW254+1.p_2',fact_pc0) ).
fof(144,axiom,
class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex),
file('/tmp/tmp0N6hNK/sel_SWW254+1.p_2',arity_Complex__Ocomplex__RealVector_Oreal__normed__vector) ).
fof(240,axiom,
! [X21] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),X21) = X21,
file('/tmp/tmp0N6hNK/sel_SWW254+1.p_2',fact_real__mult__1) ).
fof(254,axiom,
! [X2,X1,X15,X6] :
( class_Fields_Olinordered__field(X6)
=> ( c_Orderings_Oord__class_Oless(X6,c_Groups_Ozero__class_Ozero(X6),X15)
=> ( c_Orderings_Oord__class_Oless(X6,c_Rings_Oinverse__class_Odivide(X6,X1,X15),X2)
<=> c_Orderings_Oord__class_Oless(X6,X1,hAPP(hAPP(c_Groups_Otimes__class_Otimes(X6),X2),X15)) ) ) ),
file('/tmp/tmp0N6hNK/sel_SWW254+1.p_2',fact_pos__divide__less__eq) ).
fof(344,axiom,
! [X21,X5,X4,X6] :
( class_Orderings_Oorder(X6)
=> ( c_Orderings_Oord__class_Oless__eq(X6,X4,X5)
=> ( c_Orderings_Oord__class_Oless(X6,X21,X4)
=> c_Orderings_Oord__class_Oless(X6,X21,X5) ) ) ),
file('/tmp/tmp0N6hNK/sel_SWW254+1.p_2',fact_xt1_I8_J) ).
fof(588,axiom,
hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_pa____),v_c____) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q____),c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)),
file('/tmp/tmp0N6hNK/sel_SWW254+1.p_2',fact_pqc0) ).
fof(614,axiom,
! [X35] : hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q____),X35) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_pa____),c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,v_c____,X35)),
file('/tmp/tmp0N6hNK/sel_SWW254+1.p_2',fact_q_I2_J) ).
fof(760,axiom,
! [X10,X6] :
( class_RealVector_Oreal__normed__vector(X6)
=> ( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(X6,X10))
<=> X10 != c_Groups_Ozero__class_Ozero(X6) ) ),
file('/tmp/tmp0N6hNK/sel_SWW254+1.p_2',fact_zero__less__norm__iff) ).
fof(824,axiom,
! [X39] : c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q____),c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_pa____),X39))),
file('/tmp/tmp0N6hNK/sel_SWW254+1.p_2',fact_cq0) ).
fof(912,axiom,
! [X9,X10,X6] :
( class_Orderings_Olinorder(X6)
=> ( ~ c_Orderings_Oord__class_Oless__eq(X6,X10,X9)
<=> c_Orderings_Oord__class_Oless(X6,X9,X10) ) ),
file('/tmp/tmp0N6hNK/sel_SWW254+1.p_2',fact_linorder__not__le) ).
fof(1083,axiom,
class_Orderings_Oorder(tc_RealDef_Oreal),
file('/tmp/tmp0N6hNK/sel_SWW254+1.p_2',arity_RealDef__Oreal__Orderings_Oorder) ).
fof(1121,axiom,
class_Orderings_Olinorder(tc_RealDef_Oreal),
file('/tmp/tmp0N6hNK/sel_SWW254+1.p_2',arity_RealDef__Oreal__Orderings_Olinorder) ).
fof(1246,negated_conjecture,
~ ( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q____),v_w____)),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q____),c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)))),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))
<=> c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q____),v_w____)),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q____),c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)))) ),
inference(assume_negation,[status(cth)],[69]) ).
fof(1299,plain,
! [X9,X10,X6] :
( class_Orderings_Olinorder(X6)
=> ( ~ c_Orderings_Oord__class_Oless__eq(X6,X10,X9)
<=> c_Orderings_Oord__class_Oless(X6,X9,X10) ) ),
inference(fof_simplification,[status(thm)],[912,theory(equality)]) ).
fof(1525,negated_conjecture,
( ( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q____),v_w____)),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q____),c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)))),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q____),v_w____)),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q____),c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)))) )
& ( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q____),v_w____)),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q____),c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)))),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q____),v_w____)),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q____),c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)))) ) ),
inference(fof_nnf,[status(thm)],[1246]) ).
cnf(1526,negated_conjecture,
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q____),v_w____)),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q____),c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex))))
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q____),v_w____)),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q____),c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)))),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)) ),
inference(split_conjunct,[status(thm)],[1525]) ).
cnf(1630,plain,
class_Fields_Olinordered__field(tc_RealDef_Oreal),
inference(split_conjunct,[status(thm)],[100]) ).
cnf(1708,plain,
hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_pa____),v_c____) != c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(split_conjunct,[status(thm)],[129]) ).
cnf(1753,plain,
class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex),
inference(split_conjunct,[status(thm)],[144]) ).
fof(2079,plain,
! [X22] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),X22) = X22,
inference(variable_rename,[status(thm)],[240]) ).
cnf(2080,plain,
hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),X1) = X1,
inference(split_conjunct,[status(thm)],[2079]) ).
fof(2134,plain,
! [X2,X1,X15,X6] :
( ~ class_Fields_Olinordered__field(X6)
| ~ c_Orderings_Oord__class_Oless(X6,c_Groups_Ozero__class_Ozero(X6),X15)
| ( ( ~ c_Orderings_Oord__class_Oless(X6,c_Rings_Oinverse__class_Odivide(X6,X1,X15),X2)
| c_Orderings_Oord__class_Oless(X6,X1,hAPP(hAPP(c_Groups_Otimes__class_Otimes(X6),X2),X15)) )
& ( ~ c_Orderings_Oord__class_Oless(X6,X1,hAPP(hAPP(c_Groups_Otimes__class_Otimes(X6),X2),X15))
| c_Orderings_Oord__class_Oless(X6,c_Rings_Oinverse__class_Odivide(X6,X1,X15),X2) ) ) ),
inference(fof_nnf,[status(thm)],[254]) ).
fof(2135,plain,
! [X16,X17,X18,X19] :
( ~ class_Fields_Olinordered__field(X19)
| ~ c_Orderings_Oord__class_Oless(X19,c_Groups_Ozero__class_Ozero(X19),X18)
| ( ( ~ c_Orderings_Oord__class_Oless(X19,c_Rings_Oinverse__class_Odivide(X19,X17,X18),X16)
| c_Orderings_Oord__class_Oless(X19,X17,hAPP(hAPP(c_Groups_Otimes__class_Otimes(X19),X16),X18)) )
& ( ~ c_Orderings_Oord__class_Oless(X19,X17,hAPP(hAPP(c_Groups_Otimes__class_Otimes(X19),X16),X18))
| c_Orderings_Oord__class_Oless(X19,c_Rings_Oinverse__class_Odivide(X19,X17,X18),X16) ) ) ),
inference(variable_rename,[status(thm)],[2134]) ).
fof(2136,plain,
! [X16,X17,X18,X19] :
( ( ~ c_Orderings_Oord__class_Oless(X19,c_Rings_Oinverse__class_Odivide(X19,X17,X18),X16)
| c_Orderings_Oord__class_Oless(X19,X17,hAPP(hAPP(c_Groups_Otimes__class_Otimes(X19),X16),X18))
| ~ c_Orderings_Oord__class_Oless(X19,c_Groups_Ozero__class_Ozero(X19),X18)
| ~ class_Fields_Olinordered__field(X19) )
& ( ~ c_Orderings_Oord__class_Oless(X19,X17,hAPP(hAPP(c_Groups_Otimes__class_Otimes(X19),X16),X18))
| c_Orderings_Oord__class_Oless(X19,c_Rings_Oinverse__class_Odivide(X19,X17,X18),X16)
| ~ c_Orderings_Oord__class_Oless(X19,c_Groups_Ozero__class_Ozero(X19),X18)
| ~ class_Fields_Olinordered__field(X19) ) ),
inference(distribute,[status(thm)],[2135]) ).
cnf(2138,plain,
( c_Orderings_Oord__class_Oless(X1,X3,hAPP(hAPP(c_Groups_Otimes__class_Otimes(X1),X4),X2))
| ~ class_Fields_Olinordered__field(X1)
| ~ c_Orderings_Oord__class_Oless(X1,c_Groups_Ozero__class_Ozero(X1),X2)
| ~ c_Orderings_Oord__class_Oless(X1,c_Rings_Oinverse__class_Odivide(X1,X3,X2),X4) ),
inference(split_conjunct,[status(thm)],[2136]) ).
fof(2414,plain,
! [X21,X5,X4,X6] :
( ~ class_Orderings_Oorder(X6)
| ~ c_Orderings_Oord__class_Oless__eq(X6,X4,X5)
| ~ c_Orderings_Oord__class_Oless(X6,X21,X4)
| c_Orderings_Oord__class_Oless(X6,X21,X5) ),
inference(fof_nnf,[status(thm)],[344]) ).
fof(2415,plain,
! [X22,X23,X24,X25] :
( ~ class_Orderings_Oorder(X25)
| ~ c_Orderings_Oord__class_Oless__eq(X25,X24,X23)
| ~ c_Orderings_Oord__class_Oless(X25,X22,X24)
| c_Orderings_Oord__class_Oless(X25,X22,X23) ),
inference(variable_rename,[status(thm)],[2414]) ).
cnf(2416,plain,
( c_Orderings_Oord__class_Oless(X1,X2,X3)
| ~ c_Orderings_Oord__class_Oless(X1,X2,X4)
| ~ c_Orderings_Oord__class_Oless__eq(X1,X4,X3)
| ~ class_Orderings_Oorder(X1) ),
inference(split_conjunct,[status(thm)],[2415]) ).
cnf(3121,plain,
hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_pa____),v_c____) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q____),c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)),
inference(split_conjunct,[status(thm)],[588]) ).
fof(3193,plain,
! [X36] : hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q____),X36) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_pa____),c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,v_c____,X36)),
inference(variable_rename,[status(thm)],[614]) ).
cnf(3194,plain,
hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q____),X1) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_pa____),c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,v_c____,X1)),
inference(split_conjunct,[status(thm)],[3193]) ).
fof(3648,plain,
! [X10,X6] :
( ~ class_RealVector_Oreal__normed__vector(X6)
| ( ( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(X6,X10))
| X10 != c_Groups_Ozero__class_Ozero(X6) )
& ( X10 = c_Groups_Ozero__class_Ozero(X6)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(X6,X10)) ) ) ),
inference(fof_nnf,[status(thm)],[760]) ).
fof(3649,plain,
! [X11,X12] :
( ~ class_RealVector_Oreal__normed__vector(X12)
| ( ( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(X12,X11))
| X11 != c_Groups_Ozero__class_Ozero(X12) )
& ( X11 = c_Groups_Ozero__class_Ozero(X12)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(X12,X11)) ) ) ),
inference(variable_rename,[status(thm)],[3648]) ).
fof(3650,plain,
! [X11,X12] :
( ( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(X12,X11))
| X11 != c_Groups_Ozero__class_Ozero(X12)
| ~ class_RealVector_Oreal__normed__vector(X12) )
& ( X11 = c_Groups_Ozero__class_Ozero(X12)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(X12,X11))
| ~ class_RealVector_Oreal__normed__vector(X12) ) ),
inference(distribute,[status(thm)],[3649]) ).
cnf(3651,plain,
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(X1,X2))
| X2 = c_Groups_Ozero__class_Ozero(X1)
| ~ class_RealVector_Oreal__normed__vector(X1) ),
inference(split_conjunct,[status(thm)],[3650]) ).
fof(3850,plain,
! [X40] : c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q____),c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_pa____),X40))),
inference(variable_rename,[status(thm)],[824]) ).
cnf(3851,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q____),c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_pa____),X1))),
inference(split_conjunct,[status(thm)],[3850]) ).
fof(4124,plain,
! [X9,X10,X6] :
( ~ class_Orderings_Olinorder(X6)
| ( ( c_Orderings_Oord__class_Oless__eq(X6,X10,X9)
| c_Orderings_Oord__class_Oless(X6,X9,X10) )
& ( ~ c_Orderings_Oord__class_Oless(X6,X9,X10)
| ~ c_Orderings_Oord__class_Oless__eq(X6,X10,X9) ) ) ),
inference(fof_nnf,[status(thm)],[1299]) ).
fof(4125,plain,
! [X11,X12,X13] :
( ~ class_Orderings_Olinorder(X13)
| ( ( c_Orderings_Oord__class_Oless__eq(X13,X12,X11)
| c_Orderings_Oord__class_Oless(X13,X11,X12) )
& ( ~ c_Orderings_Oord__class_Oless(X13,X11,X12)
| ~ c_Orderings_Oord__class_Oless__eq(X13,X12,X11) ) ) ),
inference(variable_rename,[status(thm)],[4124]) ).
fof(4126,plain,
! [X11,X12,X13] :
( ( c_Orderings_Oord__class_Oless__eq(X13,X12,X11)
| c_Orderings_Oord__class_Oless(X13,X11,X12)
| ~ class_Orderings_Olinorder(X13) )
& ( ~ c_Orderings_Oord__class_Oless(X13,X11,X12)
| ~ c_Orderings_Oord__class_Oless__eq(X13,X12,X11)
| ~ class_Orderings_Olinorder(X13) ) ),
inference(distribute,[status(thm)],[4125]) ).
cnf(4127,plain,
( ~ class_Orderings_Olinorder(X1)
| ~ c_Orderings_Oord__class_Oless__eq(X1,X2,X3)
| ~ c_Orderings_Oord__class_Oless(X1,X3,X2) ),
inference(split_conjunct,[status(thm)],[4126]) ).
cnf(4707,plain,
class_Orderings_Oorder(tc_RealDef_Oreal),
inference(split_conjunct,[status(thm)],[1083]) ).
cnf(4821,plain,
class_Orderings_Olinorder(tc_RealDef_Oreal),
inference(split_conjunct,[status(thm)],[1121]) ).
cnf(5362,negated_conjecture,
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q____),v_w____)),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_pa____),v_c____))),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q____),v_w____)),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q____),c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)))) ),
inference(rw,[status(thm)],[1526,3121,theory(equality)]) ).
cnf(5363,negated_conjecture,
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q____),v_w____)),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_pa____),v_c____))),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q____),v_w____)),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_pa____),v_c____))) ),
inference(rw,[status(thm)],[5362,3121,theory(equality)]) ).
cnf(5399,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_pa____),v_c____)),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_pa____),X1))),
inference(rw,[status(thm)],[3851,3121,theory(equality)]) ).
cnf(5543,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_pa____),v_c____)),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q____),X1))),
inference(spm,[status(thm)],[5399,3194,theory(equality)]) ).
cnf(5799,plain,
( c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = X1
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,X1)) ),
inference(spm,[status(thm)],[3651,1753,theory(equality)]) ).
cnf(9820,plain,
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X1,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_pa____),X2)))
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X1,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_pa____),v_c____)))
| ~ class_Orderings_Oorder(tc_RealDef_Oreal) ),
inference(spm,[status(thm)],[2416,5399,theory(equality)]) ).
cnf(9871,plain,
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X1,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_pa____),X2)))
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X1,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_pa____),v_c____)))
| $false ),
inference(rw,[status(thm)],[9820,4707,theory(equality)]) ).
cnf(9872,plain,
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X1,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_pa____),X2)))
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X1,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_pa____),v_c____))) ),
inference(cn,[status(thm)],[9871,theory(equality)]) ).
cnf(89981,plain,
( ~ class_Orderings_Olinorder(tc_RealDef_Oreal)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q____),X1)),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_pa____),v_c____))) ),
inference(spm,[status(thm)],[4127,5543,theory(equality)]) ).
cnf(89998,plain,
( $false
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q____),X1)),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_pa____),v_c____))) ),
inference(rw,[status(thm)],[89981,4821,theory(equality)]) ).
cnf(89999,plain,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q____),X1)),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_pa____),v_c____))),
inference(cn,[status(thm)],[89998,theory(equality)]) ).
cnf(96859,negated_conjecture,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q____),v_w____)),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_pa____),v_c____))),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),
inference(sr,[status(thm)],[5363,89999,theory(equality)]) ).
cnf(253847,plain,
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_pa____),X1)))
| c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_pa____),v_c____) ),
inference(spm,[status(thm)],[9872,5799,theory(equality)]) ).
cnf(253867,plain,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_pa____),X1))),
inference(sr,[status(thm)],[253847,1708,theory(equality)]) ).
cnf(421001,negated_conjecture,
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q____),v_w____)),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_pa____),v_c____))))
| ~ class_Fields_Olinordered__field(tc_RealDef_Oreal)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_pa____),v_c____))) ),
inference(spm,[status(thm)],[2138,96859,theory(equality)]) ).
cnf(421051,negated_conjecture,
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q____),v_w____)),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_pa____),v_c____)))
| ~ class_Fields_Olinordered__field(tc_RealDef_Oreal)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_pa____),v_c____))) ),
inference(rw,[status(thm)],[421001,2080,theory(equality)]) ).
cnf(421052,negated_conjecture,
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q____),v_w____)),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_pa____),v_c____)))
| $false
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_pa____),v_c____))) ),
inference(rw,[status(thm)],[421051,1630,theory(equality)]) ).
cnf(421053,negated_conjecture,
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q____),v_w____)),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_pa____),v_c____)))
| $false
| $false ),
inference(rw,[status(thm)],[421052,253867,theory(equality)]) ).
cnf(421054,negated_conjecture,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q____),v_w____)),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_pa____),v_c____))),
inference(cn,[status(thm)],[421053,theory(equality)]) ).
cnf(421055,negated_conjecture,
$false,
inference(sr,[status(thm)],[421054,89999,theory(equality)]) ).
cnf(421056,negated_conjecture,
$false,
421055,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% % SZS status Started for /home/graph/tptp/TPTP/Problems/SWW/SWW254+1.p
% --creating new selector for []
% eprover: CPU time limit exceeded, terminating
% -running prover on /tmp/tmp0N6hNK/sel_SWW254+1.p_1 with time limit 29
% -prover status ResourceOut
% -running prover on /tmp/tmp0N6hNK/sel_SWW254+1.p_2 with time limit 80
% -prover status Theorem
% Problem SWW254+1.p solved in phase 1.
% % SZS status Theorem for /home/graph/tptp/TPTP/Problems/SWW/SWW254+1.p
% % SZS status Ended for /home/graph/tptp/TPTP/Problems/SWW/SWW254+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
%
%------------------------------------------------------------------------------