%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWW222+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n001.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 03:07:28 PM UTC 2026
% Result : Theorem 20.03s 3.30s
% Output : CNFRefutation 8.83s
% Verified :
% SZS Type : Refutation
% Derivation depth : 41
% Number of leaves : 32
% Syntax : Number of formulae : 174 ( 62 unt; 0 def)
% Number of atoms : 401 ( 152 equ)
% Maximal formula atoms : 11 ( 2 avg)
% Number of connectives : 377 ( 150 ~; 169 |; 29 &)
% ( 9 <=>; 20 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 14 ( 12 usr; 1 prp; 0-3 aty)
% Number of functors : 20 ( 20 usr; 8 con; 0-3 aty)
% Number of variables : 210 ( 210 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_wa____,v_z____)),v_d____),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
( ( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_wa____,v_z____)),v_d____)
& c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_wa____,v_z____))) )
=> c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_wa____),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [V_b,V_a,T_a] :
( ( class_RealVector_Oreal__normed__field(T_a)
& class_Fields_Ofield__inverse__zero(T_a) )
=> c_RealVector_Onorm__class_Onorm(T_a,c_Rings_Oinverse__class_Odivide(T_a,V_a,V_b)) = c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(T_a,V_a),c_RealVector_Onorm__class_Onorm(T_a,V_b)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f21,axiom,
! [V_x_2,T_a] :
( class_RealVector_Oreal__normed__vector(T_a)
=> ( c_RealVector_Onorm__class_Onorm(T_a,V_x_2) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)
<=> V_x_2 = c_Groups_Ozero__class_Ozero(T_a) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f31,axiom,
! [V_r] : c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,V_r) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,V_r),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f32,axiom,
! [V_a,T_a] :
( class_Rings_Odivision__ring__inverse__zero(T_a)
=> c_Rings_Oinverse__class_Odivide(T_a,V_a,c_Groups_Ozero__class_Ozero(T_a)) = c_Groups_Ozero__class_Ozero(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f35,axiom,
! [V_x_2,T_a] :
( class_RealVector_Oreal__normed__vector(T_a)
=> ( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(T_a,V_x_2))
<=> V_x_2 != c_Groups_Ozero__class_Ozero(T_a) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f48,axiom,
! [V_x,T_a] :
( class_RealVector_Oreal__normed__vector(T_a)
=> ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(T_a,V_x),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f54,axiom,
! [V_y,V_x,T_a] :
( class_Rings_Olinordered__idom(T_a)
=> ( V_x != V_y
=> ( ~ c_Orderings_Oord__class_Oless(T_a,V_x,V_y)
=> c_Orderings_Oord__class_Oless(T_a,V_y,V_x) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f60,axiom,
! [V_r,T_a] :
( ( class_Int_Onumber__ring(T_a)
& class_Fields_Olinordered__field__inverse__zero(T_a) )
=> ( c_Orderings_Oord__class_Oless(T_a,c_Groups_Ozero__class_Ozero(T_a),V_r)
=> c_Orderings_Oord__class_Oless(T_a,c_Groups_Ozero__class_Ozero(T_a),c_Rings_Oinverse__class_Odivide(T_a,V_r,c_Int_Onumber__class_Onumber__of(T_a,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f67,axiom,
! [V_c,V_b,V_a,T_a] :
( class_Rings_Odivision__ring(T_a)
=> c_Rings_Oinverse__class_Odivide(T_a,c_Groups_Ominus__class_Ominus(T_a,V_a,V_b),V_c) = c_Groups_Ominus__class_Ominus(T_a,c_Rings_Oinverse__class_Odivide(T_a,V_a,V_c),c_Rings_Oinverse__class_Odivide(T_a,V_b,V_c)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f75,axiom,
! [V_b,V_a,T_a] :
( class_RealVector_Oreal__normed__vector(T_a)
=> c_RealVector_Onorm__class_Onorm(T_a,c_Groups_Ominus__class_Ominus(T_a,V_a,V_b)) = c_RealVector_Onorm__class_Onorm(T_a,c_Groups_Ominus__class_Ominus(T_a,V_b,V_a)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f77,axiom,
! [V_b,V_a,T_a] :
( class_Rings_Odivision__ring(T_a)
=> c_Groups_Ouminus__class_Ouminus(T_a,c_Rings_Oinverse__class_Odivide(T_a,V_a,V_b)) = c_Rings_Oinverse__class_Odivide(T_a,c_Groups_Ouminus__class_Ouminus(T_a,V_a),V_b) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f79,axiom,
! [V_r] :
( ( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_r,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))
=> c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,V_r) = V_r )
& ( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_r,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))
=> c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,V_r) = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,V_r) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f112,axiom,
! [V_da_2,V_c_2,V_b_2,V_a_2,T_a] :
( class_Groups_Oab__group__add(T_a)
=> ( c_Groups_Ominus__class_Ominus(T_a,V_a_2,V_b_2) = c_Groups_Ominus__class_Ominus(T_a,V_c_2,V_da_2)
=> ( V_a_2 = V_b_2
<=> V_c_2 = V_da_2 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f119,axiom,
! [V_a,T_a] :
( class_Groups_Ogroup__add(T_a)
=> c_Groups_Ominus__class_Ominus(T_a,V_a,c_Groups_Ozero__class_Ozero(T_a)) = V_a ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f145,axiom,
! [V_b_2,V_a_2,T_a] :
( class_Fields_Olinordered__field__inverse__zero(T_a)
=> ( c_Orderings_Oord__class_Oless(T_a,c_Rings_Oinverse__class_Odivide(T_a,V_a_2,V_b_2),c_Groups_Ozero__class_Ozero(T_a))
<=> ( ( c_Orderings_Oord__class_Oless(T_a,c_Groups_Ozero__class_Ozero(T_a),V_b_2)
& c_Orderings_Oord__class_Oless(T_a,V_a_2,c_Groups_Ozero__class_Ozero(T_a)) )
| ( c_Orderings_Oord__class_Oless(T_a,V_b_2,c_Groups_Ozero__class_Ozero(T_a))
& c_Orderings_Oord__class_Oless(T_a,c_Groups_Ozero__class_Ozero(T_a),V_a_2) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f471,axiom,
! [V_y_2,V_x_2] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2,V_y_2)
<=> ( V_x_2 != V_y_2
& c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2,V_y_2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f656,axiom,
! [V_y,V_x] : c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,V_x,V_y) = c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,V_x,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,V_y)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1092,axiom,
class_Fields_Olinordered__field__inverse__zero(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1096,axiom,
class_Rings_Odivision__ring__inverse__zero(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1106,axiom,
class_RealVector_Oreal__normed__vector(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1126,axiom,
class_Rings_Olinordered__idom(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1144,axiom,
class_Int_Onumber__ring(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1162,axiom,
class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1163,axiom,
class_RealVector_Oreal__normed__field(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1166,axiom,
class_Fields_Ofield__inverse__zero(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1175,axiom,
class_Rings_Odivision__ring(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1177,axiom,
class_Groups_Oab__group__add(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1183,axiom,
class_Groups_Ogroup__add(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1251,conjecture,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_wa____),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1252,negated_conjecture,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_wa____),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))),
inference(negated_conjecture,[status(cth)],[f1251]) ).
fof(f1257,plain,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_wa____,v_z____)),v_d____),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f1259,plain,
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_wa____),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_wa____,v_z____)),v_d____)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_wa____,v_z____))) ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f1260,plain,
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_wa____),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_wa____,v_z____)),v_d____)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_wa____,v_z____))) ),
inference(cnf_transformation,[status(thm)],[f1259]) ).
fof(f1263,plain,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f1277,plain,
! [V_b,V_a,T_a] :
( c_RealVector_Onorm__class_Onorm(T_a,c_Rings_Oinverse__class_Odivide(T_a,V_a,V_b)) = c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(T_a,V_a),c_RealVector_Onorm__class_Onorm(T_a,V_b))
| ~ class_RealVector_Oreal__normed__field(T_a)
| ~ class_Fields_Ofield__inverse__zero(T_a) ),
inference(pre_NNF_transformation,[status(thm)],[f12]) ).
fof(f1278,plain,
! [T_a] :
( ! [V_b,V_a] : c_RealVector_Onorm__class_Onorm(T_a,c_Rings_Oinverse__class_Odivide(T_a,V_a,V_b)) = c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(T_a,V_a),c_RealVector_Onorm__class_Onorm(T_a,V_b))
| ~ class_RealVector_Oreal__normed__field(T_a)
| ~ class_Fields_Ofield__inverse__zero(T_a) ),
inference(miniscoping,[status(thm)],[f1277]) ).
fof(f1279,plain,
! [X0,X1,X2] :
( c_RealVector_Onorm__class_Onorm(X0,c_Rings_Oinverse__class_Odivide(X0,X1,X2)) = c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(X0,X1),c_RealVector_Onorm__class_Onorm(X0,X2))
| ~ class_RealVector_Oreal__normed__field(X0)
| ~ class_Fields_Ofield__inverse__zero(X0) ),
inference(cnf_transformation,[status(thm)],[f1278]) ).
fof(f1305,plain,
! [V_x_2,T_a] :
( ( c_RealVector_Onorm__class_Onorm(T_a,V_x_2) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)
<=> V_x_2 = c_Groups_Ozero__class_Ozero(T_a) )
| ~ class_RealVector_Oreal__normed__vector(T_a) ),
inference(pre_NNF_transformation,[status(thm)],[f21]) ).
fof(f1306,plain,
! [V_x_2,T_a] :
( ( ( V_x_2 != c_Groups_Ozero__class_Ozero(T_a)
| c_RealVector_Onorm__class_Onorm(T_a,V_x_2) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) )
& ( V_x_2 = c_Groups_Ozero__class_Ozero(T_a)
| c_RealVector_Onorm__class_Onorm(T_a,V_x_2) != c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) ) )
| ~ class_RealVector_Oreal__normed__vector(T_a) ),
inference(NNF_transformation,[status(thm)],[f1305]) ).
fof(f1307,plain,
! [T_a] :
( ( ! [V_x_2] :
( V_x_2 != c_Groups_Ozero__class_Ozero(T_a)
| c_RealVector_Onorm__class_Onorm(T_a,V_x_2) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) )
& ! [V_x_2] :
( V_x_2 = c_Groups_Ozero__class_Ozero(T_a)
| c_RealVector_Onorm__class_Onorm(T_a,V_x_2) != c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) ) )
| ~ class_RealVector_Oreal__normed__vector(T_a) ),
inference(miniscoping,[status(thm)],[f1306]) ).
fof(f1308,plain,
! [X0,X1] :
( X1 = c_Groups_Ozero__class_Ozero(X0)
| c_RealVector_Onorm__class_Onorm(X0,X1) != c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)
| ~ class_RealVector_Oreal__normed__vector(X0) ),
inference(cnf_transformation,[status(thm)],[f1307]) ).
fof(f1331,plain,
! [X0] : c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X0) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0),
inference(cnf_transformation,[status(thm)],[f31]) ).
fof(f1332,plain,
! [V_a,T_a] :
( c_Rings_Oinverse__class_Odivide(T_a,V_a,c_Groups_Ozero__class_Ozero(T_a)) = c_Groups_Ozero__class_Ozero(T_a)
| ~ class_Rings_Odivision__ring__inverse__zero(T_a) ),
inference(pre_NNF_transformation,[status(thm)],[f32]) ).
fof(f1333,plain,
! [T_a] :
( ! [V_a] : c_Rings_Oinverse__class_Odivide(T_a,V_a,c_Groups_Ozero__class_Ozero(T_a)) = c_Groups_Ozero__class_Ozero(T_a)
| ~ class_Rings_Odivision__ring__inverse__zero(T_a) ),
inference(miniscoping,[status(thm)],[f1332]) ).
fof(f1334,plain,
! [X0,X1] :
( c_Rings_Oinverse__class_Odivide(X0,X1,c_Groups_Ozero__class_Ozero(X0)) = c_Groups_Ozero__class_Ozero(X0)
| ~ class_Rings_Odivision__ring__inverse__zero(X0) ),
inference(cnf_transformation,[status(thm)],[f1333]) ).
fof(f1341,plain,
! [V_x_2,T_a] :
( ( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(T_a,V_x_2))
<=> V_x_2 != c_Groups_Ozero__class_Ozero(T_a) )
| ~ class_RealVector_Oreal__normed__vector(T_a) ),
inference(pre_NNF_transformation,[status(thm)],[f35]) ).
fof(f1342,plain,
! [V_x_2,T_a] :
( ( ( V_x_2 = c_Groups_Ozero__class_Ozero(T_a)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(T_a,V_x_2)) )
& ( V_x_2 != c_Groups_Ozero__class_Ozero(T_a)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(T_a,V_x_2)) ) )
| ~ class_RealVector_Oreal__normed__vector(T_a) ),
inference(NNF_transformation,[status(thm)],[f1341]) ).
fof(f1343,plain,
! [T_a] :
( ( ! [V_x_2] :
( V_x_2 = c_Groups_Ozero__class_Ozero(T_a)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(T_a,V_x_2)) )
& ! [V_x_2] :
( V_x_2 != c_Groups_Ozero__class_Ozero(T_a)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(T_a,V_x_2)) ) )
| ~ class_RealVector_Oreal__normed__vector(T_a) ),
inference(miniscoping,[status(thm)],[f1342]) ).
fof(f1345,plain,
! [X0,X1] :
( X1 = c_Groups_Ozero__class_Ozero(X0)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(X0,X1))
| ~ class_RealVector_Oreal__normed__vector(X0) ),
inference(cnf_transformation,[status(thm)],[f1343]) ).
fof(f1382,plain,
! [V_x,T_a] :
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(T_a,V_x),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))
| ~ class_RealVector_Oreal__normed__vector(T_a) ),
inference(pre_NNF_transformation,[status(thm)],[f48]) ).
fof(f1383,plain,
! [T_a] :
( ! [V_x] : ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(T_a,V_x),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))
| ~ class_RealVector_Oreal__normed__vector(T_a) ),
inference(miniscoping,[status(thm)],[f1382]) ).
fof(f1384,plain,
! [X0,X1] :
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(X0,X1),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))
| ~ class_RealVector_Oreal__normed__vector(X0) ),
inference(cnf_transformation,[status(thm)],[f1383]) ).
fof(f1405,plain,
! [V_y,V_x,T_a] :
( c_Orderings_Oord__class_Oless(T_a,V_y,V_x)
| c_Orderings_Oord__class_Oless(T_a,V_x,V_y)
| V_x = V_y
| ~ class_Rings_Olinordered__idom(T_a) ),
inference(pre_NNF_transformation,[status(thm)],[f54]) ).
fof(f1406,plain,
! [T_a] :
( ! [V_y,V_x] :
( c_Orderings_Oord__class_Oless(T_a,V_y,V_x)
| c_Orderings_Oord__class_Oless(T_a,V_x,V_y)
| V_x = V_y )
| ~ class_Rings_Olinordered__idom(T_a) ),
inference(miniscoping,[status(thm)],[f1405]) ).
fof(f1407,plain,
! [X0,X1,X2] :
( c_Orderings_Oord__class_Oless(X0,X2,X1)
| c_Orderings_Oord__class_Oless(X0,X1,X2)
| X1 = X2
| ~ class_Rings_Olinordered__idom(X0) ),
inference(cnf_transformation,[status(thm)],[f1406]) ).
fof(f1431,plain,
! [V_r,T_a] :
( c_Orderings_Oord__class_Oless(T_a,c_Groups_Ozero__class_Ozero(T_a),c_Rings_Oinverse__class_Odivide(T_a,V_r,c_Int_Onumber__class_Onumber__of(T_a,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))
| ~ c_Orderings_Oord__class_Oless(T_a,c_Groups_Ozero__class_Ozero(T_a),V_r)
| ~ class_Int_Onumber__ring(T_a)
| ~ class_Fields_Olinordered__field__inverse__zero(T_a) ),
inference(pre_NNF_transformation,[status(thm)],[f60]) ).
fof(f1432,plain,
! [T_a] :
( ! [V_r] :
( c_Orderings_Oord__class_Oless(T_a,c_Groups_Ozero__class_Ozero(T_a),c_Rings_Oinverse__class_Odivide(T_a,V_r,c_Int_Onumber__class_Onumber__of(T_a,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))
| ~ c_Orderings_Oord__class_Oless(T_a,c_Groups_Ozero__class_Ozero(T_a),V_r) )
| ~ class_Int_Onumber__ring(T_a)
| ~ class_Fields_Olinordered__field__inverse__zero(T_a) ),
inference(miniscoping,[status(thm)],[f1431]) ).
fof(f1433,plain,
! [X0,X1] :
( c_Orderings_Oord__class_Oless(X0,c_Groups_Ozero__class_Ozero(X0),c_Rings_Oinverse__class_Odivide(X0,X1,c_Int_Onumber__class_Onumber__of(X0,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))
| ~ c_Orderings_Oord__class_Oless(X0,c_Groups_Ozero__class_Ozero(X0),X1)
| ~ class_Int_Onumber__ring(X0)
| ~ class_Fields_Olinordered__field__inverse__zero(X0) ),
inference(cnf_transformation,[status(thm)],[f1432]) ).
fof(f1456,plain,
! [V_c,V_b,V_a,T_a] :
( c_Rings_Oinverse__class_Odivide(T_a,c_Groups_Ominus__class_Ominus(T_a,V_a,V_b),V_c) = c_Groups_Ominus__class_Ominus(T_a,c_Rings_Oinverse__class_Odivide(T_a,V_a,V_c),c_Rings_Oinverse__class_Odivide(T_a,V_b,V_c))
| ~ class_Rings_Odivision__ring(T_a) ),
inference(pre_NNF_transformation,[status(thm)],[f67]) ).
fof(f1457,plain,
! [T_a] :
( ! [V_c,V_b,V_a] : c_Rings_Oinverse__class_Odivide(T_a,c_Groups_Ominus__class_Ominus(T_a,V_a,V_b),V_c) = c_Groups_Ominus__class_Ominus(T_a,c_Rings_Oinverse__class_Odivide(T_a,V_a,V_c),c_Rings_Oinverse__class_Odivide(T_a,V_b,V_c))
| ~ class_Rings_Odivision__ring(T_a) ),
inference(miniscoping,[status(thm)],[f1456]) ).
fof(f1458,plain,
! [X0,X1,X2,X3] :
( c_Rings_Oinverse__class_Odivide(X0,c_Groups_Ominus__class_Ominus(X0,X1,X2),X3) = c_Groups_Ominus__class_Ominus(X0,c_Rings_Oinverse__class_Odivide(X0,X1,X3),c_Rings_Oinverse__class_Odivide(X0,X2,X3))
| ~ class_Rings_Odivision__ring(X0) ),
inference(cnf_transformation,[status(thm)],[f1457]) ).
fof(f1472,plain,
! [V_b,V_a,T_a] :
( c_RealVector_Onorm__class_Onorm(T_a,c_Groups_Ominus__class_Ominus(T_a,V_a,V_b)) = c_RealVector_Onorm__class_Onorm(T_a,c_Groups_Ominus__class_Ominus(T_a,V_b,V_a))
| ~ class_RealVector_Oreal__normed__vector(T_a) ),
inference(pre_NNF_transformation,[status(thm)],[f75]) ).
fof(f1473,plain,
! [T_a] :
( ! [V_b,V_a] : c_RealVector_Onorm__class_Onorm(T_a,c_Groups_Ominus__class_Ominus(T_a,V_a,V_b)) = c_RealVector_Onorm__class_Onorm(T_a,c_Groups_Ominus__class_Ominus(T_a,V_b,V_a))
| ~ class_RealVector_Oreal__normed__vector(T_a) ),
inference(miniscoping,[status(thm)],[f1472]) ).
fof(f1474,plain,
! [X0,X1,X2] :
( c_RealVector_Onorm__class_Onorm(X0,c_Groups_Ominus__class_Ominus(X0,X1,X2)) = c_RealVector_Onorm__class_Onorm(X0,c_Groups_Ominus__class_Ominus(X0,X2,X1))
| ~ class_RealVector_Oreal__normed__vector(X0) ),
inference(cnf_transformation,[status(thm)],[f1473]) ).
fof(f1478,plain,
! [V_b,V_a,T_a] :
( c_Groups_Ouminus__class_Ouminus(T_a,c_Rings_Oinverse__class_Odivide(T_a,V_a,V_b)) = c_Rings_Oinverse__class_Odivide(T_a,c_Groups_Ouminus__class_Ouminus(T_a,V_a),V_b)
| ~ class_Rings_Odivision__ring(T_a) ),
inference(pre_NNF_transformation,[status(thm)],[f77]) ).
fof(f1479,plain,
! [T_a] :
( ! [V_b,V_a] : c_Groups_Ouminus__class_Ouminus(T_a,c_Rings_Oinverse__class_Odivide(T_a,V_a,V_b)) = c_Rings_Oinverse__class_Odivide(T_a,c_Groups_Ouminus__class_Ouminus(T_a,V_a),V_b)
| ~ class_Rings_Odivision__ring(T_a) ),
inference(miniscoping,[status(thm)],[f1478]) ).
fof(f1480,plain,
! [X0,X1,X2] :
( c_Groups_Ouminus__class_Ouminus(X0,c_Rings_Oinverse__class_Odivide(X0,X1,X2)) = c_Rings_Oinverse__class_Odivide(X0,c_Groups_Ouminus__class_Ouminus(X0,X1),X2)
| ~ class_Rings_Odivision__ring(X0) ),
inference(cnf_transformation,[status(thm)],[f1479]) ).
fof(f1484,plain,
! [V_r] :
( ( c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,V_r) = V_r
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_r,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)) )
& ( c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,V_r) = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,V_r)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_r,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)) ) ),
inference(pre_NNF_transformation,[status(thm)],[f79]) ).
fof(f1485,plain,
( ! [V_r] :
( c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,V_r) = V_r
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_r,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)) )
& ! [V_r] :
( c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,V_r) = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,V_r)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_r,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)) ) ),
inference(miniscoping,[status(thm)],[f1484]) ).
fof(f1487,plain,
! [X0] :
( c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0) = X0
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)) ),
inference(cnf_transformation,[status(thm)],[f1485]) ).
fof(f1579,plain,
! [V_da_2,V_c_2,V_b_2,V_a_2,T_a] :
( ( V_a_2 = V_b_2
<=> V_c_2 = V_da_2 )
| c_Groups_Ominus__class_Ominus(T_a,V_a_2,V_b_2) != c_Groups_Ominus__class_Ominus(T_a,V_c_2,V_da_2)
| ~ class_Groups_Oab__group__add(T_a) ),
inference(pre_NNF_transformation,[status(thm)],[f112]) ).
fof(f1580,plain,
! [V_da_2,V_c_2,V_b_2,V_a_2,T_a] :
( ( ( V_c_2 != V_da_2
| V_a_2 = V_b_2 )
& ( V_c_2 = V_da_2
| V_a_2 != V_b_2 ) )
| c_Groups_Ominus__class_Ominus(T_a,V_a_2,V_b_2) != c_Groups_Ominus__class_Ominus(T_a,V_c_2,V_da_2)
| ~ class_Groups_Oab__group__add(T_a) ),
inference(NNF_transformation,[status(thm)],[f1579]) ).
fof(f1581,plain,
! [T_a] :
( ! [V_da_2,V_c_2,V_b_2,V_a_2] :
( ( ( V_c_2 != V_da_2
| V_a_2 = V_b_2 )
& ( V_c_2 = V_da_2
| V_a_2 != V_b_2 ) )
| c_Groups_Ominus__class_Ominus(T_a,V_a_2,V_b_2) != c_Groups_Ominus__class_Ominus(T_a,V_c_2,V_da_2) )
| ~ class_Groups_Oab__group__add(T_a) ),
inference(miniscoping,[status(thm)],[f1580]) ).
fof(f1582,plain,
! [X0,X1,X2,X3,X4] :
( X3 = X4
| X1 != X2
| c_Groups_Ominus__class_Ominus(X0,X1,X2) != c_Groups_Ominus__class_Ominus(X0,X3,X4)
| ~ class_Groups_Oab__group__add(X0) ),
inference(cnf_transformation,[status(thm)],[f1581]) ).
fof(f1612,plain,
! [V_a,T_a] :
( c_Groups_Ominus__class_Ominus(T_a,V_a,c_Groups_Ozero__class_Ozero(T_a)) = V_a
| ~ class_Groups_Ogroup__add(T_a) ),
inference(pre_NNF_transformation,[status(thm)],[f119]) ).
fof(f1613,plain,
! [T_a] :
( ! [V_a] : c_Groups_Ominus__class_Ominus(T_a,V_a,c_Groups_Ozero__class_Ozero(T_a)) = V_a
| ~ class_Groups_Ogroup__add(T_a) ),
inference(miniscoping,[status(thm)],[f1612]) ).
fof(f1614,plain,
! [X0,X1] :
( c_Groups_Ominus__class_Ominus(X0,X1,c_Groups_Ozero__class_Ozero(X0)) = X1
| ~ class_Groups_Ogroup__add(X0) ),
inference(cnf_transformation,[status(thm)],[f1613]) ).
fof(f1724,plain,
! [V_b_2,V_a_2,T_a] :
( ( c_Orderings_Oord__class_Oless(T_a,c_Rings_Oinverse__class_Odivide(T_a,V_a_2,V_b_2),c_Groups_Ozero__class_Ozero(T_a))
<=> ( ( c_Orderings_Oord__class_Oless(T_a,c_Groups_Ozero__class_Ozero(T_a),V_b_2)
& c_Orderings_Oord__class_Oless(T_a,V_a_2,c_Groups_Ozero__class_Ozero(T_a)) )
| ( c_Orderings_Oord__class_Oless(T_a,V_b_2,c_Groups_Ozero__class_Ozero(T_a))
& c_Orderings_Oord__class_Oless(T_a,c_Groups_Ozero__class_Ozero(T_a),V_a_2) ) ) )
| ~ class_Fields_Olinordered__field__inverse__zero(T_a) ),
inference(pre_NNF_transformation,[status(thm)],[f145]) ).
fof(f1725,plain,
! [V_b_2,V_a_2,T_a] :
( ( ( ( ( ~ c_Orderings_Oord__class_Oless(T_a,c_Groups_Ozero__class_Ozero(T_a),V_b_2)
| ~ c_Orderings_Oord__class_Oless(T_a,V_a_2,c_Groups_Ozero__class_Ozero(T_a)) )
& ( ~ c_Orderings_Oord__class_Oless(T_a,V_b_2,c_Groups_Ozero__class_Ozero(T_a))
| ~ c_Orderings_Oord__class_Oless(T_a,c_Groups_Ozero__class_Ozero(T_a),V_a_2) ) )
| c_Orderings_Oord__class_Oless(T_a,c_Rings_Oinverse__class_Odivide(T_a,V_a_2,V_b_2),c_Groups_Ozero__class_Ozero(T_a)) )
& ( ( c_Orderings_Oord__class_Oless(T_a,c_Groups_Ozero__class_Ozero(T_a),V_b_2)
& c_Orderings_Oord__class_Oless(T_a,V_a_2,c_Groups_Ozero__class_Ozero(T_a)) )
| ( c_Orderings_Oord__class_Oless(T_a,V_b_2,c_Groups_Ozero__class_Ozero(T_a))
& c_Orderings_Oord__class_Oless(T_a,c_Groups_Ozero__class_Ozero(T_a),V_a_2) )
| ~ c_Orderings_Oord__class_Oless(T_a,c_Rings_Oinverse__class_Odivide(T_a,V_a_2,V_b_2),c_Groups_Ozero__class_Ozero(T_a)) ) )
| ~ class_Fields_Olinordered__field__inverse__zero(T_a) ),
inference(NNF_transformation,[status(thm)],[f1724]) ).
fof(f1726,plain,
! [T_a] :
( ( ! [V_b_2,V_a_2] :
( ( ( ~ c_Orderings_Oord__class_Oless(T_a,c_Groups_Ozero__class_Ozero(T_a),V_b_2)
| ~ c_Orderings_Oord__class_Oless(T_a,V_a_2,c_Groups_Ozero__class_Ozero(T_a)) )
& ( ~ c_Orderings_Oord__class_Oless(T_a,V_b_2,c_Groups_Ozero__class_Ozero(T_a))
| ~ c_Orderings_Oord__class_Oless(T_a,c_Groups_Ozero__class_Ozero(T_a),V_a_2) ) )
| c_Orderings_Oord__class_Oless(T_a,c_Rings_Oinverse__class_Odivide(T_a,V_a_2,V_b_2),c_Groups_Ozero__class_Ozero(T_a)) )
& ! [V_b_2,V_a_2] :
( ( c_Orderings_Oord__class_Oless(T_a,c_Groups_Ozero__class_Ozero(T_a),V_b_2)
& c_Orderings_Oord__class_Oless(T_a,V_a_2,c_Groups_Ozero__class_Ozero(T_a)) )
| ( c_Orderings_Oord__class_Oless(T_a,V_b_2,c_Groups_Ozero__class_Ozero(T_a))
& c_Orderings_Oord__class_Oless(T_a,c_Groups_Ozero__class_Ozero(T_a),V_a_2) )
| ~ c_Orderings_Oord__class_Oless(T_a,c_Rings_Oinverse__class_Odivide(T_a,V_a_2,V_b_2),c_Groups_Ozero__class_Ozero(T_a)) ) )
| ~ class_Fields_Olinordered__field__inverse__zero(T_a) ),
inference(miniscoping,[status(thm)],[f1725]) ).
fof(f1727,plain,
! [X0,X1,X2] :
( c_Orderings_Oord__class_Oless(X0,X1,c_Groups_Ozero__class_Ozero(X0))
| c_Orderings_Oord__class_Oless(X0,c_Groups_Ozero__class_Ozero(X0),X1)
| ~ c_Orderings_Oord__class_Oless(X0,c_Rings_Oinverse__class_Odivide(X0,X1,X2),c_Groups_Ozero__class_Ozero(X0))
| ~ class_Fields_Olinordered__field__inverse__zero(X0) ),
inference(cnf_transformation,[status(thm)],[f1726]) ).
fof(f2662,plain,
! [V_y_2,V_x_2] :
( ( V_x_2 = V_y_2
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2,V_y_2)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2,V_y_2) )
& ( ( V_x_2 != V_y_2
& c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2,V_y_2) )
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2,V_y_2) ) ),
inference(NNF_transformation,[status(thm)],[f471]) ).
fof(f2663,plain,
( ! [V_y_2,V_x_2] :
( V_x_2 = V_y_2
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2,V_y_2)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2,V_y_2) )
& ! [V_y_2,V_x_2] :
( ( V_x_2 != V_y_2
& c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2,V_y_2) )
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2,V_y_2) ) ),
inference(miniscoping,[status(thm)],[f2662]) ).
fof(f2665,plain,
! [X0,X1] :
( X0 != X1
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f2663]) ).
fof(f3210,plain,
! [X0,X1] : c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,X0,X1) = c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,X0,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,X1)),
inference(cnf_transformation,[status(thm)],[f656]) ).
fof(f4485,plain,
class_Fields_Olinordered__field__inverse__zero(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f1092]) ).
fof(f4489,plain,
class_Rings_Odivision__ring__inverse__zero(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f1096]) ).
fof(f4499,plain,
class_RealVector_Oreal__normed__vector(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f1106]) ).
fof(f4519,plain,
class_Rings_Olinordered__idom(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f1126]) ).
fof(f4537,plain,
class_Int_Onumber__ring(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f1144]) ).
fof(f4555,plain,
class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f1162]) ).
fof(f4556,plain,
class_RealVector_Oreal__normed__field(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f1163]) ).
fof(f4559,plain,
class_Fields_Ofield__inverse__zero(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f1166]) ).
fof(f4568,plain,
class_Rings_Odivision__ring(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f1175]) ).
fof(f4570,plain,
class_Groups_Oab__group__add(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f1177]) ).
fof(f4576,plain,
class_Groups_Ogroup__add(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f1183]) ).
fof(f4699,plain,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_wa____),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))),
inference(cnf_transformation,[status(thm)],[f1252]) ).
fof(f4816,plain,
! [X0,X1,X2,X3] :
( X2 = X3
| c_Groups_Ominus__class_Ominus(X0,X1,X1) != c_Groups_Ominus__class_Ominus(X0,X2,X3)
| ~ class_Groups_Oab__group__add(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f1582]) ).
fof(f4859,plain,
! [X0] : ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,X0),
inference(destructive_equality_resolution,[status(thm)],[f2665]) ).
fof(f4947,plain,
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_wa____),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_wa____,v_z____))) ),
inference(forward_subsumption_resolution,[status(thm)],[f1260,f1257]) ).
fof(f4948,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,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_wa____,v_z____))),
inference(resolution,[status(thm)],[f4947,f4699]) ).
fof(f4978,plain,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))),
inference(backward_demodulation,[status(thm)],[f1331,f1263]) ).
fof(f4980,plain,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_wa____),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))),
inference(backward_demodulation,[status(thm)],[f1331,f4699]) ).
fof(f5078,plain,
! [X0] :
( c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X0) = X0
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)) ),
inference(forward_demodulation,[status(thm)],[f1331,f1487]) ).
fof(f5079,plain,
c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(resolution,[status(thm)],[f5078,f4859]) ).
fof(f5197,plain,
( c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_wa____,v_z____) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)
| ~ class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex) ),
inference(resolution,[status(thm)],[f1345,f4948]) ).
fof(f5537,plain,
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_wa____),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____))))
| c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))) = c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_wa____),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)))
| ~ class_Rings_Olinordered__idom(tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f1407,f4980]) ).
fof(f5539,plain,
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_wa____,v_z____)),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))
| c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_wa____,v_z____)) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)
| ~ class_Rings_Olinordered__idom(tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f1407,f4948]) ).
fof(f5558,plain,
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_wa____),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____))))
| c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))) = c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_wa____),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____))) ),
inference(forward_subsumption_resolution,[status(thm)],[f5537,f4519]) ).
fof(f5560,plain,
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_wa____,v_z____)),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))
| c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_wa____,v_z____)) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) ),
inference(forward_subsumption_resolution,[status(thm)],[f5539,f4519]) ).
fof(f5574,plain,
( ~ class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex)
| c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_wa____,v_z____)) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f5560,f1384]) ).
fof(f5796,plain,
c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_wa____,v_z____)) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(backward_subsumption_resolution,[status(thm)],[f5574,f4555]) ).
fof(f5797,plain,
c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_wa____,v_z____) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(backward_subsumption_resolution,[status(thm)],[f5197,f4555]) ).
fof(f5857,plain,
( c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_z____,v_wa____)) = c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex))
| ~ class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex) ),
inference(paramodulation,[status(thm)],[f5797,f1474]) ).
fof(f5860,plain,
c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_z____,v_wa____)) = c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)),
inference(forward_subsumption_resolution,[status(thm)],[f5857,f4555]) ).
fof(f5863,plain,
c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(forward_demodulation,[status(thm)],[f5797,f5796]) ).
fof(f5873,plain,
! [X0] :
( c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Rings_Oinverse__class_Odivide(tc_Complex_Ocomplex,X0,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex))) = c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,X0),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))
| ~ class_RealVector_Oreal__normed__field(tc_Complex_Ocomplex)
| ~ class_Fields_Ofield__inverse__zero(tc_Complex_Ocomplex) ),
inference(paramodulation,[status(thm)],[f5863,f1279]) ).
fof(f5877,plain,
! [X0] :
( c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Rings_Oinverse__class_Odivide(tc_Complex_Ocomplex,X0,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex))) = c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,X0),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))
| ~ class_Fields_Ofield__inverse__zero(tc_Complex_Ocomplex) ),
inference(forward_subsumption_resolution,[status(thm)],[f5873,f4556]) ).
fof(f5930,plain,
c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_z____,v_wa____)) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(forward_demodulation,[status(thm)],[f5863,f5860]) ).
fof(f5931,plain,
( c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_z____,v_wa____) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)
| ~ class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex) ),
inference(resolution,[status(thm)],[f5930,f1308]) ).
fof(f5940,plain,
c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_z____,v_wa____) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(forward_subsumption_resolution,[status(thm)],[f5931,f4555]) ).
fof(f6082,plain,
! [X0] : c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Rings_Oinverse__class_Odivide(tc_Complex_Ocomplex,X0,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex))) = c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,X0),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),
inference(forward_subsumption_resolution,[status(thm)],[f5877,f4559]) ).
fof(f6087,plain,
! [X0] :
( c_Rings_Oinverse__class_Odivide(tc_Complex_Ocomplex,X0,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)
| c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,X0),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)) != c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)
| ~ class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex) ),
inference(paramodulation,[status(thm)],[f6082,f1308]) ).
fof(f6095,plain,
! [X0] :
( c_Rings_Oinverse__class_Odivide(tc_Complex_Ocomplex,X0,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)
| c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,X0),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)) != c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) ),
inference(forward_subsumption_resolution,[status(thm)],[f6087,f4555]) ).
fof(f6865,plain,
! [X0] :
( ~ class_Rings_Odivision__ring__inverse__zero(tc_RealDef_Oreal)
| c_Rings_Oinverse__class_Odivide(tc_Complex_Ocomplex,X0,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
inference(resolution,[status(thm)],[f6095,f1334]) ).
fof(f6869,plain,
! [X0] : c_Rings_Oinverse__class_Odivide(tc_Complex_Ocomplex,X0,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(forward_subsumption_resolution,[status(thm)],[f6865,f4489]) ).
fof(f6894,plain,
! [X0] :
( c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)) = c_Rings_Oinverse__class_Odivide(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,X0),c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex))
| ~ class_Rings_Odivision__ring(tc_Complex_Ocomplex) ),
inference(paramodulation,[status(thm)],[f6869,f1480]) ).
fof(f6896,plain,
! [X0,X1] :
( c_Rings_Oinverse__class_Odivide(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,X0,X1),c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)) = c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,c_Rings_Oinverse__class_Odivide(tc_Complex_Ocomplex,X0,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)),c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex))
| ~ class_Rings_Odivision__ring(tc_Complex_Ocomplex) ),
inference(paramodulation,[status(thm)],[f6869,f1458]) ).
fof(f6905,plain,
( c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)
| ~ class_Rings_Odivision__ring(tc_Complex_Ocomplex) ),
inference(forward_demodulation,[status(thm)],[f6869,f6894]) ).
fof(f6906,plain,
c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(forward_subsumption_resolution,[status(thm)],[f6905,f4568]) ).
fof(f6909,plain,
! [X0] :
( c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,c_Rings_Oinverse__class_Odivide(tc_Complex_Ocomplex,X0,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)),c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex))
| ~ class_Rings_Odivision__ring(tc_Complex_Ocomplex) ),
inference(forward_demodulation,[status(thm)],[f6869,f6896]) ).
fof(f6910,plain,
( c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex),c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex))
| ~ class_Rings_Odivision__ring(tc_Complex_Ocomplex) ),
inference(forward_demodulation,[status(thm)],[f6869,f6909]) ).
fof(f6911,plain,
c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex),c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)),
inference(forward_subsumption_resolution,[status(thm)],[f6910,f4568]) ).
fof(f6921,plain,
! [X0] : c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,X0,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)) = c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,X0,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)),
inference(paramodulation,[status(thm)],[f6906,f3210]) ).
fof(f6964,plain,
! [X0] :
( v_z____ = v_wa____
| c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,X0,X0) != c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)
| ~ class_Groups_Oab__group__add(tc_Complex_Ocomplex) ),
inference(paramodulation,[status(thm)],[f5940,f4816]) ).
fof(f7000,plain,
! [X0] :
( v_z____ = v_wa____
| c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,X0,X0) != c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
inference(forward_subsumption_resolution,[status(thm)],[f6964,f4570]) ).
fof(f7110,plain,
v_z____ = v_wa____,
inference(resolution,[status(thm)],[f6911,f7000]) ).
fof(f7122,plain,
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____))))
| c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))) = c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_wa____),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____))) ),
inference(backward_demodulation,[status(thm)],[f7110,f5558]) ).
fof(f7124,plain,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))),
inference(backward_demodulation,[status(thm)],[f7110,f4980]) ).
fof(f7127,plain,
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____))))
| c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))) = c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____))) ),
inference(forward_demodulation,[status(thm)],[f7110,f7122]) ).
fof(f7708,plain,
! [X0] :
( c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,X0,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)) = X0
| ~ class_Groups_Ogroup__add(tc_Complex_Ocomplex) ),
inference(paramodulation,[status(thm)],[f6921,f1614]) ).
fof(f7715,plain,
! [X0,X1] :
( X1 = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)
| c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,X0,X0) != c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,X1,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex))
| ~ class_Groups_Oab__group__add(tc_Complex_Ocomplex) ),
inference(paramodulation,[status(thm)],[f6921,f4816]) ).
fof(f7721,plain,
! [X0] : c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,X0,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)) = X0,
inference(forward_subsumption_resolution,[status(thm)],[f7708,f4576]) ).
fof(f7726,plain,
! [X0,X1] :
( X1 = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)
| c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,X0,X0) != c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,X1,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)) ),
inference(forward_subsumption_resolution,[status(thm)],[f7715,f4570]) ).
fof(f7984,plain,
! [X0,X1] :
( X1 = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)
| c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,X0,X0) != X1 ),
inference(forward_demodulation,[status(thm)],[f7721,f7726]) ).
fof(f7988,plain,
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)))
| c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))) = c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____))) ),
inference(backward_demodulation,[status(thm)],[f7990,f7127]) ).
fof(f7989,plain,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))),
inference(backward_demodulation,[status(thm)],[f7990,f7124]) ).
fof(f7990,plain,
! [X0] : c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,X0,X0) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(destructive_equality_resolution,[status(thm)],[f7984]) ).
fof(f8017,plain,
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)))
| c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))) = c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)) ),
inference(forward_demodulation,[status(thm)],[f7990,f7988]) ).
fof(f8018,plain,
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)))
| c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) ),
inference(forward_demodulation,[status(thm)],[f5863,f8017]) ).
fof(f8019,plain,
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))
| c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) ),
inference(forward_demodulation,[status(thm)],[f5863,f8018]) ).
fof(f8020,plain,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))),
inference(forward_demodulation,[status(thm)],[f5863,f7989]) ).
fof(f8030,plain,
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))))
| ~ class_Int_Onumber__ring(tc_RealDef_Oreal)
| ~ class_Fields_Olinordered__field__inverse__zero(tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f8020,f1433]) ).
fof(f8034,plain,
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))))
| ~ class_Int_Onumber__ring(tc_RealDef_Oreal) ),
inference(forward_subsumption_resolution,[status(thm)],[f8030,f4485]) ).
fof(f8696,plain,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____)))),
inference(forward_subsumption_resolution,[status(thm)],[f8034,f4537]) ).
fof(f8697,plain,
( c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____)) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)
| ~ class_RealVector_Oreal__normed__vector(tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f8696,f1345]) ).
fof(f8701,plain,
c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____)) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(forward_subsumption_resolution,[status(thm)],[f8697,f4499]) ).
fof(f10013,plain,
( c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Groups_Ozero__class_Ozero(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_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))))
| ~ class_Fields_Olinordered__field__inverse__zero(tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f1727,f8019]) ).
fof(f10028,plain,
( c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Groups_Ozero__class_Ozero(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_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____)))) ),
inference(forward_subsumption_resolution,[status(thm)],[f10013,f4485]) ).
fof(f18869,plain,
( c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Groups_Ozero__class_Ozero(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_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))) ),
inference(forward_demodulation,[status(thm)],[f8701,f10028]) ).
fof(f18870,plain,
( c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)) ),
inference(forward_demodulation,[status(thm)],[f5079,f18869]) ).
fof(f18871,plain,
( c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)) ),
inference(forward_demodulation,[status(thm)],[f8701,f18870]) ).
fof(f18872,plain,
( c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)) ),
inference(forward_demodulation,[status(thm)],[f5079,f18871]) ).
fof(f18873,plain,
( c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)) ),
inference(forward_demodulation,[status(thm)],[f8701,f18872]) ).
fof(f18874,plain,
( c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)) ),
inference(forward_demodulation,[status(thm)],[f5079,f18873]) ).
fof(f18875,plain,
( c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)) ),
inference(duplicate_literals_removal,[status(thm)],[f18874]) ).
fof(f18879,plain,
c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(forward_subsumption_resolution,[status(thm)],[f18875,f4859]) ).
fof(f20208,plain,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))),
inference(forward_demodulation,[status(thm)],[f8701,f4978]) ).
fof(f20209,plain,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))),
inference(forward_demodulation,[status(thm)],[f5079,f20208]) ).
fof(f20210,plain,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),
inference(forward_demodulation,[status(thm)],[f18879,f20209]) ).
fof(f20211,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f20210,f4859]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWW222+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.07 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.20/0.49 % Computer : n001.cluster.edu
% 0.20/0.49 % Model : x86_64 x86_64
% 0.20/0.49 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/0.49 % Memory : 8046.5625MB
% 0.20/0.49 % OS : Linux 6.8.0-71-generic
% 0.20/0.49 % CPULimit : 300
% 0.20/0.49 % WCLimit : 300
% 0.20/0.49 % DateTime : Mon Sep 21 09:47:44 UTC 2026
% 0.20/0.50 % CPUTime :
% 0.37/0.70 % Drodi V4.1.1
% 20.03/3.30 % Refutation found
% 20.03/3.30 % SZS status Theorem for theBenchmark: Theorem is valid
% 20.03/3.30 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 8.83/3.40 % Elapsed time: 2.874819 seconds
% 8.83/3.40 % CPU time: 20.842473 seconds
% 8.83/3.40 % Total memory used: 386.897 MB
% 8.83/3.40 % Net memory used: 376.830 MB
%------------------------------------------------------------------------------