Vampire-SAT---5.0.1.THM-Ref.s

%------------------------------------------------------------------------------
% File     : Vampire-SAT---5.0.1
% Problem  : SWW230+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT

% Computer : n005.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 : Tue Sep 29 01:39:40 PM UTC 2026

% Result   : Theorem 227.92s 41.99s
% Output   : Refutation 227.92s
% Verified : 
% SZS Type : Refutation
%            Derivation depth      :   27
%            Number of leaves      :   29
% Syntax   : Number of formulae    :  151 ( 124 unt;   0 def)
%            Number of atoms       :  180 ( 104 equ)
%            Maximal formula atoms :    4 (   1 avg)
%            Number of connectives :   75 (  46   ~;  20   |;   1   &)
%                                         (   1 <=>;   7  =>;   0  <=;   0 <~>)
%            Maximal formula depth :    7 (   3 avg)
%            Maximal term depth    :   11 (   2 avg)
%            Number of predicates  :    8 (   6 usr;   1 prp; 0-3 aty)
%            Number of functors    :   26 (  26 usr;  11 con; 0-3 aty)
%            Number of variables   :  170 ( 170   !;   0   ?)

% Comments : 
%------------------------------------------------------------------------------
fof(f3,axiom,
    c_Orderings_Oord__class_Oless__eq(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,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Groups_Oplus__class_Oplus(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,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))))),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))),c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____))))),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact__096abs_A_Icmod_A_Ipoly_Ap_Az_J_A_N_A_N_As_J_060_061_Aabs_A_Icmod_A_Ipoly_Ap_A_Ig_A_If_A_IN1_A_L_AN2_J_J_J_J_A_N_A_N_As_J_A_L_Acmod_A_Ipoly_Ap_A_Ig_A_If_A_IN1_A_L_AN2_J_J_J_A_N_Apoly_Ap_Az_J_096) ).

fof(f14,axiom,
    ! [X0,X1,X2] :
      ( X2 = c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X1,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),X0))
    <=> c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),X2) = c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X1,X0) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_eq__divide__2__times__iff) ).

fof(f25,axiom,
    ! [X0] : c_Groups_Oplus__class_Oplus(tc_Int_Oint,X0,c_Int_OPls) = X0,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_add__Pls__right) ).

fof(f26,axiom,
    ! [X0] : c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OPls,X0) = X0,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_add__Pls) ).

fof(f28,axiom,
    ! [X0] : c_Int_OBit0(X0) = c_Groups_Oplus__class_Oplus(tc_Int_Oint,X0,X0),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_Bit0__def) ).

fof(f95,axiom,
    ! [X0,X1] : c_Groups_Oplus__class_Oplus(tc_Int_Oint,X1,X0) = c_Groups_Oplus__class_Oplus(tc_Int_Oint,X0,X1),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_zadd__commute) ).

fof(f102,axiom,
    ! [X0,X1,X2] : c_Groups_Oplus__class_Oplus(tc_Int_Oint,X2,c_Groups_Oplus__class_Oplus(tc_Int_Oint,X1,X0)) = c_Groups_Oplus__class_Oplus(tc_Int_Oint,X1,c_Groups_Oplus__class_Oplus(tc_Int_Oint,X2,X0)),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_zadd__left__commute) ).

fof(f111,axiom,
    ! [X0,X1,X2] : c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,X2,X1),X0) = c_Groups_Oplus__class_Oplus(tc_Int_Oint,X2,c_Groups_Oplus__class_Oplus(tc_Int_Oint,X1,X0)),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_zadd__assoc) ).

fof(f196,axiom,
    ! [X0,X1] : c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X1,X0) = c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X0,X1),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_real__mult__commute) ).

fof(f197,axiom,
    ! [X0,X1,X2] : c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X2,X1),X0) = c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X2,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X1,X0)),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_real__mult__assoc) ).

fof(f221,axiom,
    ! [X0,X1] : c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X1,X0) = c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0)),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_minus__real__def) ).

fof(f245,axiom,
    ! [X0] : c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),X0) = X0,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_real__mult__1) ).

fof(f252,axiom,
    ! [X0,X1] : c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X1,X0) = c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X1,c_Rings_Oinverse__class_Oinverse(tc_RealDef_Oreal,X0)),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_real__divide__def) ).

fof(f273,axiom,
    ! [X0,X1] :
      ( class_Int_Onumber__ring(X1)
     => c_Groups_Otimes__class_Otimes(X1,c_Groups_Oplus__class_Oplus(X1,c_Groups_Oone__class_Oone(X1),c_Groups_Oone__class_Oone(X1)),c_Int_Onumber__class_Onumber__of(X1,X0)) = c_Int_Onumber__class_Onumber__of(X1,c_Int_OBit0(X0)) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_double__number__of__Bit0) ).

fof(f278,axiom,
    ! [X0] :
      ( class_Int_Onumber__ring(X0)
     => c_Groups_Oplus__class_Oplus(X0,c_Groups_Oone__class_Oone(X0),c_Groups_Oone__class_Oone(X0)) = c_Int_Onumber__class_Onumber__of(X0,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_one__add__one__is__two) ).

fof(f299,axiom,
    ! [X0] : c_Int_OBit1(X0) = c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),X0),X0),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_Bit1__def) ).

fof(f569,axiom,
    ! [X0] : c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X0) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_real__norm__def) ).

fof(f608,axiom,
    ! [X0,X1] :
      ( class_Rings_Odivision__ring(X1)
     => c_Rings_Oinverse__class_Odivide(X1,X0,c_Groups_Oone__class_Oone(X1)) = X0 ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_divide__1) ).

fof(f617,axiom,
    ! [X0,X1,X2] :
      ( class_RealVector_Oreal__normed__vector(X2)
     => c_RealVector_Onorm__class_Onorm(X2,c_Groups_Ominus__class_Ominus(X2,X1,X0)) = c_RealVector_Onorm__class_Onorm(X2,c_Groups_Ominus__class_Ominus(X2,X0,X1)) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_norm__minus__commute) ).

fof(f622,axiom,
    ! [X0,X1] :
      ( class_RealVector_Oreal__normed__vector(X1)
     => c_RealVector_Onorm__class_Onorm(X1,c_Groups_Ouminus__class_Ouminus(X1,X0)) = c_RealVector_Onorm__class_Onorm(X1,X0) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_norm__minus__cancel) ).

fof(f915,axiom,
    ! [X0,X1,X2] :
      ( class_Groups_Ogroup__add(X2)
     => c_Groups_Ouminus__class_Ouminus(X2,c_Groups_Oplus__class_Oplus(X2,X1,X0)) = c_Groups_Oplus__class_Oplus(X2,c_Groups_Ouminus__class_Ouminus(X2,X0),c_Groups_Ouminus__class_Ouminus(X2,X1)) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_minus__add) ).

fof(f993,axiom,
    ! [X0,X1,X2] :
      ( class_Rings_Ocomm__semiring__1(X2)
     => c_Groups_Oplus__class_Oplus(X2,X1,X0) = c_Groups_Oplus__class_Oplus(X2,X0,X1) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_comm__semiring__1__class_Onormalizing__semiring__rules_I24_J) ).

fof(f1091,axiom,
    class_RealVector_Oreal__normed__vector(tc_RealDef_Oreal),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_RealDef__Oreal__RealVector_Oreal__normed__vector) ).

fof(f1112,axiom,
    class_Rings_Ocomm__semiring__1(tc_RealDef_Oreal),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_RealDef__Oreal__Rings_Ocomm__semiring__1) ).

fof(f1114,axiom,
    class_Rings_Odivision__ring(tc_RealDef_Oreal),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_RealDef__Oreal__Rings_Odivision__ring) ).

fof(f1122,axiom,
    class_Groups_Ogroup__add(tc_RealDef_Oreal),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_RealDef__Oreal__Groups_Ogroup__add) ).

fof(f1125,axiom,
    class_Int_Onumber__ring(tc_RealDef_Oreal),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_RealDef__Oreal__Int_Onumber__ring) ).

fof(f1141,axiom,
    class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_Complex__Ocomplex__RealVector_Oreal__normed__vector) ).

fof(f1171,conjecture,
    c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),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,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_Oplus__class_Oplus(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,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))))),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))),c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____))))),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).

fof(f1172,negated_conjecture,
    ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),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,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_Oplus__class_Oplus(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,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))))),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))),c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____))))),
    inference(negated_conjecture,[status(cth)],[f1171]) ).

fof(f1175,plain,
    ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),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,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_Oplus__class_Oplus(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,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))))),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))),c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____))))),
    inference(flattening,[],[f1172]) ).

fof(f1326,plain,
    ! [X0,X1] :
      ( c_Groups_Otimes__class_Otimes(X1,c_Groups_Oplus__class_Oplus(X1,c_Groups_Oone__class_Oone(X1),c_Groups_Oone__class_Oone(X1)),c_Int_Onumber__class_Onumber__of(X1,X0)) = c_Int_Onumber__class_Onumber__of(X1,c_Int_OBit0(X0))
      | ~ class_Int_Onumber__ring(X1) ),
    inference(ennf_transformation,[],[f273]) ).

fof(f1333,plain,
    ! [X0] :
      ( c_Groups_Oplus__class_Oplus(X0,c_Groups_Oone__class_Oone(X0),c_Groups_Oone__class_Oone(X0)) = c_Int_Onumber__class_Onumber__of(X0,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))
      | ~ class_Int_Onumber__ring(X0) ),
    inference(ennf_transformation,[],[f278]) ).

fof(f1555,plain,
    ! [X0,X1] :
      ( c_Rings_Oinverse__class_Odivide(X1,X0,c_Groups_Oone__class_Oone(X1)) = X0
      | ~ class_Rings_Odivision__ring(X1) ),
    inference(ennf_transformation,[],[f608]) ).

fof(f1568,plain,
    ! [X0,X1,X2] :
      ( c_RealVector_Onorm__class_Onorm(X2,c_Groups_Ominus__class_Ominus(X2,X1,X0)) = c_RealVector_Onorm__class_Onorm(X2,c_Groups_Ominus__class_Ominus(X2,X0,X1))
      | ~ class_RealVector_Oreal__normed__vector(X2) ),
    inference(ennf_transformation,[],[f617]) ).

fof(f1572,plain,
    ! [X0,X1] :
      ( c_RealVector_Onorm__class_Onorm(X1,c_Groups_Ouminus__class_Ouminus(X1,X0)) = c_RealVector_Onorm__class_Onorm(X1,X0)
      | ~ class_RealVector_Oreal__normed__vector(X1) ),
    inference(ennf_transformation,[],[f622]) ).

fof(f2018,plain,
    ! [X0,X1,X2] :
      ( c_Groups_Ouminus__class_Ouminus(X2,c_Groups_Oplus__class_Oplus(X2,X1,X0)) = c_Groups_Oplus__class_Oplus(X2,c_Groups_Ouminus__class_Ouminus(X2,X0),c_Groups_Ouminus__class_Ouminus(X2,X1))
      | ~ class_Groups_Ogroup__add(X2) ),
    inference(ennf_transformation,[],[f915]) ).

fof(f2117,plain,
    ! [X0,X1,X2] :
      ( c_Groups_Oplus__class_Oplus(X2,X1,X0) = c_Groups_Oplus__class_Oplus(X2,X0,X1)
      | ~ class_Rings_Ocomm__semiring__1(X2) ),
    inference(ennf_transformation,[],[f993]) ).

fof(f2144,plain,
    ! [X0,X1,X2] :
      ( ( X2 = c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X1,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),X0))
        | c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),X2) != c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X1,X0) )
      & ( c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),X2) = c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X1,X0)
        | c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X1,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),X0)) != X2 ) ),
    inference(nnf_transformation,[],[f14]) ).

fof(f2582,plain,
    c_Orderings_Oord__class_Oless__eq(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,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Groups_Oplus__class_Oplus(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,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))))),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))),c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____))))),
    inference(cnf_transformation,[],[f3]) ).

fof(f2593,plain,
    ! [X2,X0,X1] :
      ( c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),X2) = c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X1,X0)
      | c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X1,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),X0)) != X2 ),
    inference(cnf_transformation,[],[f2144]) ).

fof(f2609,plain,
    ! [X0] : c_Groups_Oplus__class_Oplus(tc_Int_Oint,X0,c_Int_OPls) = X0,
    inference(cnf_transformation,[],[f25]) ).

fof(f2610,plain,
    ! [X0] : c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OPls,X0) = X0,
    inference(cnf_transformation,[],[f26]) ).

fof(f2612,plain,
    ! [X0] : c_Int_OBit0(X0) = c_Groups_Oplus__class_Oplus(tc_Int_Oint,X0,X0),
    inference(cnf_transformation,[],[f28]) ).

fof(f2695,plain,
    ! [X0,X1] : c_Groups_Oplus__class_Oplus(tc_Int_Oint,X1,X0) = c_Groups_Oplus__class_Oplus(tc_Int_Oint,X0,X1),
    inference(cnf_transformation,[],[f95]) ).

fof(f2704,plain,
    ! [X2,X0,X1] : c_Groups_Oplus__class_Oplus(tc_Int_Oint,X2,c_Groups_Oplus__class_Oplus(tc_Int_Oint,X1,X0)) = c_Groups_Oplus__class_Oplus(tc_Int_Oint,X1,c_Groups_Oplus__class_Oplus(tc_Int_Oint,X2,X0)),
    inference(cnf_transformation,[],[f102]) ).

fof(f2715,plain,
    ! [X2,X0,X1] : c_Groups_Oplus__class_Oplus(tc_Int_Oint,X2,c_Groups_Oplus__class_Oplus(tc_Int_Oint,X1,X0)) = c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,X2,X1),X0),
    inference(cnf_transformation,[],[f111]) ).

fof(f2874,plain,
    ! [X0,X1] : c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X1,X0) = c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X0,X1),
    inference(cnf_transformation,[],[f196]) ).

fof(f2875,plain,
    ! [X2,X0,X1] : c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X2,X1),X0) = c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X2,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X1,X0)),
    inference(cnf_transformation,[],[f197]) ).

fof(f2988,plain,
    ! [X0,X1] : c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X1,X0) = c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0)),
    inference(cnf_transformation,[],[f221]) ).

fof(f3014,plain,
    ! [X0] : c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),X0) = X0,
    inference(cnf_transformation,[],[f245]) ).

fof(f3021,plain,
    ! [X0,X1] : c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X1,X0) = c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X1,c_Rings_Oinverse__class_Oinverse(tc_RealDef_Oreal,X0)),
    inference(cnf_transformation,[],[f252]) ).

fof(f3051,plain,
    ! [X0,X1] :
      ( c_Int_Onumber__class_Onumber__of(X1,c_Int_OBit0(X0)) = c_Groups_Otimes__class_Otimes(X1,c_Groups_Oplus__class_Oplus(X1,c_Groups_Oone__class_Oone(X1),c_Groups_Oone__class_Oone(X1)),c_Int_Onumber__class_Onumber__of(X1,X0))
      | ~ class_Int_Onumber__ring(X1) ),
    inference(cnf_transformation,[],[f1326]) ).

fof(f3058,plain,
    ! [X0] :
      ( c_Groups_Oplus__class_Oplus(X0,c_Groups_Oone__class_Oone(X0),c_Groups_Oone__class_Oone(X0)) = c_Int_Onumber__class_Onumber__of(X0,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))
      | ~ class_Int_Onumber__ring(X0) ),
    inference(cnf_transformation,[],[f1333]) ).

fof(f3087,plain,
    ! [X0] : c_Int_OBit1(X0) = c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),X0),X0),
    inference(cnf_transformation,[],[f299]) ).

fof(f3496,plain,
    ! [X0] : c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0) = c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X0),
    inference(cnf_transformation,[],[f569]) ).

fof(f3539,plain,
    ! [X0,X1] :
      ( ~ class_Rings_Odivision__ring(X1)
      | c_Rings_Oinverse__class_Odivide(X1,X0,c_Groups_Oone__class_Oone(X1)) = X0 ),
    inference(cnf_transformation,[],[f1555]) ).

fof(f3549,plain,
    ! [X2,X0,X1] :
      ( ~ class_RealVector_Oreal__normed__vector(X2)
      | c_RealVector_Onorm__class_Onorm(X2,c_Groups_Ominus__class_Ominus(X2,X1,X0)) = c_RealVector_Onorm__class_Onorm(X2,c_Groups_Ominus__class_Ominus(X2,X0,X1)) ),
    inference(cnf_transformation,[],[f1568]) ).

fof(f3554,plain,
    ! [X0,X1] :
      ( ~ class_RealVector_Oreal__normed__vector(X1)
      | c_RealVector_Onorm__class_Onorm(X1,c_Groups_Ouminus__class_Ouminus(X1,X0)) = c_RealVector_Onorm__class_Onorm(X1,X0) ),
    inference(cnf_transformation,[],[f1572]) ).

fof(f4026,plain,
    ! [X2,X0,X1] :
      ( ~ class_Groups_Ogroup__add(X2)
      | c_Groups_Ouminus__class_Ouminus(X2,c_Groups_Oplus__class_Oplus(X2,X1,X0)) = c_Groups_Oplus__class_Oplus(X2,c_Groups_Ouminus__class_Ouminus(X2,X0),c_Groups_Ouminus__class_Ouminus(X2,X1)) ),
    inference(cnf_transformation,[],[f2018]) ).

fof(f4126,plain,
    ! [X2,X0,X1] :
      ( ~ class_Rings_Ocomm__semiring__1(X2)
      | c_Groups_Oplus__class_Oplus(X2,X1,X0) = c_Groups_Oplus__class_Oplus(X2,X0,X1) ),
    inference(cnf_transformation,[],[f2117]) ).

fof(f4224,plain,
    class_RealVector_Oreal__normed__vector(tc_RealDef_Oreal),
    inference(cnf_transformation,[],[f1091]) ).

fof(f4245,plain,
    class_Rings_Ocomm__semiring__1(tc_RealDef_Oreal),
    inference(cnf_transformation,[],[f1112]) ).

fof(f4247,plain,
    class_Rings_Odivision__ring(tc_RealDef_Oreal),
    inference(cnf_transformation,[],[f1114]) ).

fof(f4255,plain,
    class_Groups_Ogroup__add(tc_RealDef_Oreal),
    inference(cnf_transformation,[],[f1122]) ).

fof(f4258,plain,
    class_Int_Onumber__ring(tc_RealDef_Oreal),
    inference(cnf_transformation,[],[f1125]) ).

fof(f4274,plain,
    class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex),
    inference(cnf_transformation,[],[f1141]) ).

fof(f4304,plain,
    ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),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,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_Oplus__class_Oplus(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,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))))),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))),c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____))))),
    inference(cnf_transformation,[],[f1175]) ).

fof(f4312,plain,
    ! [X2,X0,X1] :
      ( c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X1,X0) = c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls))),X2)
      | c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X1,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls))),X0)) != X2 ),
    inference(definition_unfolding,[],[f2593,f2612,f3087,f2612,f3087]) ).

fof(f4423,plain,
    ! [X0,X1] :
      ( ~ class_Int_Onumber__ring(X1)
      | c_Groups_Otimes__class_Otimes(X1,c_Groups_Oplus__class_Oplus(X1,c_Groups_Oone__class_Oone(X1),c_Groups_Oone__class_Oone(X1)),c_Int_Onumber__class_Onumber__of(X1,X0)) = c_Int_Onumber__class_Onumber__of(X1,c_Groups_Oplus__class_Oplus(tc_Int_Oint,X0,X0)) ),
    inference(definition_unfolding,[],[f3051,f2612]) ).

fof(f4428,plain,
    ! [X0] :
      ( ~ class_Int_Onumber__ring(X0)
      | c_Groups_Oplus__class_Oplus(X0,c_Groups_Oone__class_Oone(X0),c_Groups_Oone__class_Oone(X0)) = c_Int_Onumber__class_Onumber__of(X0,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls))) ),
    inference(definition_unfolding,[],[f3058,f2612,f3087]) ).

fof(f4586,plain,
    ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls))),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,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_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls))))),c_Groups_Oplus__class_Oplus(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,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))))),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))),c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____))))),
    inference(definition_unfolding,[],[f4304,f2612,f3087,f2612,f3087]) ).

fof(f4587,plain,
    ! [X0,X1] : c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X1,X0) = c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X1,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls))),X0))),
    inference(equality_resolution,[],[f4312]) ).

fof(f4877,plain,
    ! [X0,X1] : c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X1,X0) = c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls),c_Int_OPls))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X1,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls),c_Int_OPls))),X0))),
    inference(forward_demodulation,[],[f4587,f2704]) ).

fof(f4937,plain,
    ! [X0,X1] : c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X1,X0) = c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OPls,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls),c_Int_OPls)))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X1,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OPls,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls),c_Int_OPls)))),X0))),
    inference(forward_demodulation,[],[f4877,f2715]) ).

fof(f4976,plain,
    ! [X0,X1] : c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X1,X0) = c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OPls,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls),c_Int_OPls)))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X1,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OPls,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls),c_Int_OPls)))),X0))),
    inference(forward_demodulation,[],[f4937,f2704]) ).

fof(f5006,plain,
    ! [X0,X1] : c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X1,X0) = c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls),c_Int_OPls))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X1,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls),c_Int_OPls))),X0))),
    inference(forward_demodulation,[],[f4976,f2610]) ).

fof(f5028,plain,
    ! [X0,X1] : c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X1,X0) = c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OPls,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls)))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X1,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OPls,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls)))),X0))),
    inference(forward_demodulation,[],[f5006,f2695]) ).

fof(f5048,plain,
    ! [X0,X1] : c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X1,X0) = c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OPls,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls)))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X1,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OPls,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls)))),X0))),
    inference(forward_demodulation,[],[f5028,f2704]) ).

fof(f5068,plain,
    ! [X0,X1] : c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X1,X0) = c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X1,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls))),X0))),
    inference(forward_demodulation,[],[f5048,f2610]) ).

fof(f5088,plain,
    ! [X0,X1] : c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X1,X0) = c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OPls,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls)))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X1,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OPls,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls)))),X0))),
    inference(forward_demodulation,[],[f5068,f2695]) ).

fof(f5108,plain,
    ! [X0,X1] : c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X1,X0) = c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OPls,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls)))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X1,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OPls,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls)))),X0))),
    inference(forward_demodulation,[],[f5088,f2704]) ).

fof(f5128,plain,
    ! [X0,X1] : c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X1,X0) = c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X1,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls))),X0))),
    inference(forward_demodulation,[],[f5108,f2610]) ).

fof(f5148,plain,
    ! [X0,X1] : c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X1,X0) = c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OPls,c_Groups_Oone__class_Oone(tc_Int_Oint)))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X1,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OPls,c_Groups_Oone__class_Oone(tc_Int_Oint)))),X0))),
    inference(forward_demodulation,[],[f5128,f2695]) ).

fof(f5168,plain,
    ! [X0,X1] : c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X1,X0) = c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OPls,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oone__class_Oone(tc_Int_Oint)))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X1,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OPls,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oone__class_Oone(tc_Int_Oint)))),X0))),
    inference(forward_demodulation,[],[f5148,f2704]) ).

fof(f5188,plain,
    ! [X0,X1] : c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X1,X0) = c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oone__class_Oone(tc_Int_Oint))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X1,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oone__class_Oone(tc_Int_Oint))),X0))),
    inference(forward_demodulation,[],[f5168,f2610]) ).

fof(f5369,plain,
    ! [X0] : c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X0,c_Groups_Oone__class_Oone(tc_RealDef_Oreal)) = X0,
    inference(superposition,[],[f3014,f2874]) ).

fof(f5465,plain,
    ! [X0] : c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X0,c_Groups_Oone__class_Oone(tc_RealDef_Oreal)) = X0,
    inference(resolution,[],[f3539,f4247]) ).

fof(f5566,plain,
    ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls))),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,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_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls))))),c_Groups_Oplus__class_Oplus(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,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))))),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))),c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____))))),
    inference(superposition,[],[f4586,f2609]) ).

fof(f5571,plain,
    ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls))),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,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_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls))))),c_Groups_Oplus__class_Oplus(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,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))))),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))),c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____))))),
    inference(forward_demodulation,[],[f5566,f2704]) ).

fof(f5579,plain,
    ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OPls,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls)))),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,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_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OPls,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls)))))),c_Groups_Oplus__class_Oplus(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,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))))),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))),c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____))))),
    inference(forward_demodulation,[],[f5571,f2695]) ).

fof(f5587,plain,
    ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OPls,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls)))),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,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_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OPls,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls)))))),c_Groups_Oplus__class_Oplus(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,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))))),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))),c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____))))),
    inference(forward_demodulation,[],[f5579,f2704]) ).

fof(f5595,plain,
    ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls))),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,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_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls))))),c_Groups_Oplus__class_Oplus(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,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))))),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))),c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____))))),
    inference(forward_demodulation,[],[f5587,f2610]) ).

fof(f5603,plain,
    ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OPls,c_Groups_Oone__class_Oone(tc_Int_Oint)))),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,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_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OPls,c_Groups_Oone__class_Oone(tc_Int_Oint)))))),c_Groups_Oplus__class_Oplus(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,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))))),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))),c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____))))),
    inference(forward_demodulation,[],[f5595,f2695]) ).

fof(f5611,plain,
    ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OPls,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oone__class_Oone(tc_Int_Oint)))),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,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_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OPls,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oone__class_Oone(tc_Int_Oint)))))),c_Groups_Oplus__class_Oplus(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,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))))),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))),c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____))))),
    inference(forward_demodulation,[],[f5603,f2704]) ).

fof(f5619,plain,
    ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oone__class_Oone(tc_Int_Oint))),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,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_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oone__class_Oone(tc_Int_Oint))))),c_Groups_Oplus__class_Oplus(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,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))))),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))),c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____))))),
    inference(forward_demodulation,[],[f5611,f2610]) ).

fof(f6637,plain,
    ! [X0] : c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X0) = c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0)),
    inference(resolution,[],[f3554,f4224]) ).

fof(f6639,plain,
    ! [X0] : c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X0) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0)),
    inference(forward_demodulation,[],[f6637,f3496]) ).

fof(f6640,plain,
    ! [X0] : c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0)),
    inference(forward_demodulation,[],[f6639,f3496]) ).

fof(f6716,plain,
    ! [X0,X1] : c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,X0) = c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X1),
    inference(resolution,[],[f4126,f4245]) ).

fof(f11878,plain,
    ! [X2,X0,X1] : c_Groups_Oplus__class_Oplus(tc_Int_Oint,X1,c_Groups_Oplus__class_Oplus(tc_Int_Oint,X2,X0)) = c_Groups_Oplus__class_Oplus(tc_Int_Oint,X2,c_Groups_Oplus__class_Oplus(tc_Int_Oint,X0,X1)),
    inference(superposition,[],[f2704,f2695]) ).

fof(f12848,plain,
    ! [X2,X0,X1] : c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X0,X1),X2) = c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X0,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X1,c_Rings_Oinverse__class_Oinverse(tc_RealDef_Oreal,X2))),
    inference(superposition,[],[f3021,f2875]) ).

fof(f12849,plain,
    ! [X2,X0,X1] : c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X0,X1),X2) = c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X0,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X1,X2)),
    inference(forward_demodulation,[],[f12848,f3021]) ).

fof(f13693,plain,
    ! [X0,X1] : c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X0,X1)) = c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X1,X0)),
    inference(resolution,[],[f3549,f4224]) ).

fof(f13694,plain,
    ! [X0,X1] : c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,X0,X1)) = c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,X1,X0)),
    inference(resolution,[],[f3549,f4274]) ).

fof(f13695,plain,
    ! [X0,X1] : c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X1,X0)) = c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X0,X1)),
    inference(forward_demodulation,[],[f13693,f3496]) ).

fof(f13696,plain,
    ! [X0,X1] : c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X1,X0)) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X0,X1)),
    inference(forward_demodulation,[],[f13695,f3496]) ).

fof(f20424,plain,
    ! [X0,X1] : c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X1),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0)) = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X1)),
    inference(resolution,[],[f4026,f4255]) ).

fof(f20427,plain,
    ! [X0,X1] : c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X1)) = c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X1),X0),
    inference(forward_demodulation,[],[f20424,f2988]) ).

fof(f36712,plain,
    ! [X0] : c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,X0)) = c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,X0,X0)),
    inference(resolution,[],[f4423,f4258]) ).

fof(f62692,plain,
    c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls))) = c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),
    inference(resolution,[],[f4428,f4258]) ).

fof(f62695,plain,
    c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)) = c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls))),
    inference(forward_demodulation,[],[f62692,f36712]) ).

fof(f62698,plain,
    c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)) = c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OPls,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls)))),
    inference(forward_demodulation,[],[f62695,f2695]) ).

fof(f62701,plain,
    c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)) = c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OPls,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OPls,c_Groups_Oone__class_Oone(tc_Int_Oint))))),
    inference(forward_demodulation,[],[f62698,f11878]) ).

fof(f62704,plain,
    c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)) = c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OPls,c_Groups_Oone__class_Oone(tc_Int_Oint)))),
    inference(forward_demodulation,[],[f62701,f2610]) ).

fof(f62707,plain,
    c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)) = c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OPls,c_Groups_Oone__class_Oone(tc_Int_Oint)),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OPls,c_Groups_Oone__class_Oone(tc_Int_Oint)))),
    inference(forward_demodulation,[],[f62704,f36712]) ).

fof(f62710,plain,
    c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)) = c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OPls,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OPls,c_Groups_Oone__class_Oone(tc_Int_Oint)),c_Groups_Oone__class_Oone(tc_Int_Oint)))),
    inference(forward_demodulation,[],[f62707,f2704]) ).

fof(f62713,plain,
    c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)) = c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OPls,c_Groups_Oone__class_Oone(tc_Int_Oint)),c_Groups_Oone__class_Oone(tc_Int_Oint))),
    inference(forward_demodulation,[],[f62710,f2610]) ).

fof(f62716,plain,
    c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OPls,c_Groups_Oone__class_Oone(tc_Int_Oint)))) = c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),
    inference(forward_demodulation,[],[f62713,f2695]) ).

fof(f62719,plain,
    c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OPls,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oone__class_Oone(tc_Int_Oint)))) = c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),
    inference(forward_demodulation,[],[f62716,f2704]) ).

fof(f62722,plain,
    c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oone__class_Oone(tc_Int_Oint))) = c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),
    inference(forward_demodulation,[],[f62719,f2610]) ).

fof(f98039,plain,
    ! [X0] : c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X0,c_Groups_Oone__class_Oone(tc_RealDef_Oreal)) = c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oone__class_Oone(tc_Int_Oint))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X0,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oone__class_Oone(tc_Int_Oint))))),
    inference(superposition,[],[f5188,f5369]) ).

fof(f98393,plain,
    ! [X0] : c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X0,c_Groups_Oone__class_Oone(tc_RealDef_Oreal)) = c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oone__class_Oone(tc_Int_Oint))),X0),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oone__class_Oone(tc_Int_Oint)))),
    inference(forward_demodulation,[],[f98039,f12849]) ).

fof(f98542,plain,
    ! [X0] : c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X0,c_Groups_Oone__class_Oone(tc_RealDef_Oreal)) = c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),X0),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))),
    inference(forward_demodulation,[],[f98393,f62722]) ).

fof(f98626,plain,
    ! [X0] : c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),X0),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))) = X0,
    inference(forward_demodulation,[],[f98542,f5465]) ).

fof(f116038,plain,
    ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oone__class_Oone(tc_Int_Oint))),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,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_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oone__class_Oone(tc_Int_Oint))))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))),c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____))),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))))),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))))),
    inference(superposition,[],[f5619,f6716]) ).

fof(f116039,plain,
    c_Orderings_Oord__class_Oless__eq(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,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))),c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____))),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))))),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))))),
    inference(superposition,[],[f2582,f6716]) ).

fof(f116224,plain,
    c_Orderings_Oord__class_Oless__eq(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,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))),c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____))),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))))))))),
    inference(forward_demodulation,[],[f116039,f13696]) ).

fof(f116225,plain,
    ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oone__class_Oone(tc_Int_Oint))),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,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_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oone__class_Oone(tc_Int_Oint))))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))),c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____))),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))))))))),
    inference(forward_demodulation,[],[f116038,f13696]) ).

fof(f116320,plain,
    c_Orderings_Oord__class_Oless__eq(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,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))),c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____))),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))))),v_s____))))),
    inference(forward_demodulation,[],[f116224,f20427]) ).

fof(f116321,plain,
    ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oone__class_Oone(tc_Int_Oint))),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,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_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oone__class_Oone(tc_Int_Oint))))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))),c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____))),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))))),v_s____))))),
    inference(forward_demodulation,[],[f116225,f20427]) ).

fof(f116354,plain,
    c_Orderings_Oord__class_Oless__eq(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,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))),c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____))),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))))),v_s____)))),
    inference(forward_demodulation,[],[f116320,f6640]) ).

fof(f116355,plain,
    ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oone__class_Oone(tc_Int_Oint))),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,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_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oone__class_Oone(tc_Int_Oint))))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))),c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____))),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))))),v_s____)))),
    inference(forward_demodulation,[],[f116321,f6640]) ).

fof(f116384,plain,
    c_Orderings_Oord__class_Oless__eq(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,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))))),v_s____)),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))),c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____))))),
    inference(forward_demodulation,[],[f116354,f6716]) ).

fof(f116385,plain,
    ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oone__class_Oone(tc_Int_Oint))),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,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_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oone__class_Oone(tc_Int_Oint))))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))))),v_s____)),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))),c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____))))),
    inference(forward_demodulation,[],[f116355,f6716]) ).

fof(f116409,plain,
    c_Orderings_Oord__class_Oless__eq(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,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))))),v_s____)),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____),c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))))))),
    inference(forward_demodulation,[],[f116384,f13694]) ).

fof(f116410,plain,
    ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oone__class_Oone(tc_Int_Oint))),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,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_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oone__class_Oone(tc_Int_Oint))))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))))),v_s____)),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____),c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))))))),
    inference(forward_demodulation,[],[f116385,f13694]) ).

fof(f116430,plain,
    c_Orderings_Oord__class_Oless__eq(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,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,v_s____,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))))))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____),c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))))))),
    inference(forward_demodulation,[],[f116409,f6716]) ).

fof(f116431,plain,
    ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oone__class_Oone(tc_Int_Oint))),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,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_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oone__class_Oone(tc_Int_Oint))))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,v_s____,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))))))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____),c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))))))),
    inference(forward_demodulation,[],[f116410,f6716]) ).

fof(f116554,plain,
    c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____)))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,v_s____,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))))))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____),c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))))))),
    inference(forward_demodulation,[],[f116430,f13696]) ).

fof(f116555,plain,
    ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oone__class_Oone(tc_Int_Oint))),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,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_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oone__class_Oone(tc_Int_Oint)))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,v_s____,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))))))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____),c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))))))),
    inference(forward_demodulation,[],[f116431,f12849]) ).

fof(f116567,plain,
    c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____)),v_s____))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,v_s____,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))))))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____),c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))))))),
    inference(forward_demodulation,[],[f116554,f20427]) ).

fof(f116568,plain,
    ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(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,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____)))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,v_s____,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))))))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____),c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))))))),
    inference(forward_demodulation,[],[f116555,f62722]) ).

fof(f116576,plain,
    c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____)),v_s____)),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,v_s____,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))))))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____),c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))))))),
    inference(forward_demodulation,[],[f116567,f6640]) ).

fof(f116577,plain,
    ~ c_Orderings_Oord__class_Oless__eq(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,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,v_s____,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))))))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____),c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))))))),
    inference(forward_demodulation,[],[f116568,f98626]) ).

fof(f116585,plain,
    c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,v_s____,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____)))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,v_s____,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))))))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____),c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))))))),
    inference(forward_demodulation,[],[f116576,f6716]) ).

fof(f116586,plain,
    ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____)))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,v_s____,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))))))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____),c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))))))),
    inference(forward_demodulation,[],[f116577,f13696]) ).

fof(f116594,plain,
    ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____)),v_s____))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,v_s____,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))))))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____),c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))))))),
    inference(forward_demodulation,[],[f116586,f20427]) ).

fof(f116599,plain,
    ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____)),v_s____)),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,v_s____,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))))))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____),c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))))))),
    inference(forward_demodulation,[],[f116594,f6640]) ).

fof(f116604,plain,
    ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,v_s____,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____)))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,v_s____,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))))))),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____),c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))))))),
    inference(forward_demodulation,[],[f116599,f6716]) ).

fof(f116609,plain,
    $false,
    inference(forward_subsumption_resolution,[],[f116604,f116585]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : SWW230+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.06  % Command  : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.20  % Computer : n005.cluster.edu
% 0.08/0.20  % Model    : x86_64 x86_64
% 0.08/0.20  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.20  % Memory   : 8046.5625MB
% 0.08/0.20  % OS       : Linux 6.8.0-71-generic
% 0.08/0.20  % CPULimit : 300
% 0.08/0.20  % WCLimit  : 300
% 0.08/0.20  % DateTime : Mon Sep 28 13:20:01 UTC 2026
% 0.08/0.20  % CPUTime  : 
% 0.08/0.20  Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.23  Running first-order model finding
% 0.08/0.23  Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 13.58/2.20  % (779266)Will run a generic schedule for satisfiability detection.
% 13.58/2.20  % (779271)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3902421033_2999 on theBenchmark for (2999ds/0Mi)
% 13.58/2.20  % (779272)% WARNING: option uhcvi not known.
% 13.58/2.20  % (779272)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3933927662:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 13.58/2.20  % (779273)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1470608047:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 13.58/2.20  % (779274)dis+10_1_sil=32000:sp=arity:random_seed=1044861173:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 13.58/2.20  % (779275)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3648839271:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 13.58/2.20  % (779276)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=341092611:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 13.58/2.20  % (779277)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2353058849:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 13.58/2.20  % (779274)Instruction limit reached! 
% 13.58/2.20  % (779274)------------------------------
% 13.58/2.20  % (779274)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.58/2.20  % (779274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.58/2.20  % (779274)CaDiCaL version: 2.1.3
% 13.58/2.20  % (779274)Termination reason: Instruction limit
% 13.58/2.20  % (779274)Termination phase: Saturation
% 13.58/2.20  % (779274)Time elapsed: 0.050 s
% 13.58/2.20  % (779274)Peak memory usage: 14 MB
% 13.58/2.20  % (779274)Instructions burned: 103 (million)
% 13.58/2.20  % (779275)Instruction limit reached! 
% 13.58/2.20  % (779275)------------------------------
% 13.58/2.20  % (779275)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.58/2.20  % (779275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.58/2.20  % (779275)CaDiCaL version: 2.1.3
% 13.58/2.20  % (779275)Termination reason: Instruction limit
% 13.58/2.20  % (779275)Termination phase: Property scanning
% 13.58/2.20  % (779275)Time elapsed: 0.054 s
% 13.58/2.20  % (779275)Peak memory usage: 13 MB
% 13.58/2.20  % (779275)Instructions burned: 117 (million)
% 13.58/2.20  % (779276)Instruction limit reached! 
% 13.58/2.20  % (779276)------------------------------
% 13.58/2.20  % (779276)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.58/2.20  % (779276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.58/2.20  % (779276)CaDiCaL version: 2.1.3
% 13.58/2.20  % (779276)Termination reason: Instruction limit
% 13.58/2.20  % (779276)Termination phase: Saturation
% 13.58/2.20  % (779276)Time elapsed: 0.067 s
% 13.58/2.20  % (779276)Peak memory usage: 14 MB
% 13.58/2.20  % (779276)Instructions burned: 132 (million)
% 13.58/2.20  % (779285)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1626779376:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 13.58/2.20  % (779286)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3891626205:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 13.58/2.20  % (779277)Instruction limit reached! 
% 13.58/2.20  % (779277)------------------------------
% 13.58/2.20  % (779277)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.58/2.20  % (779277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.58/2.20  % (779277)CaDiCaL version: 2.1.3
% 13.58/2.20  % (779277)Termination reason: Instruction limit
% 13.58/2.20  % (779277)Termination phase: Saturation
% 13.58/2.20  % (779277)Time elapsed: 0.086 s
% 13.58/2.20  % (779277)Peak memory usage: 15 MB
% 13.58/2.20  % (779277)Instructions burned: 159 (million)
% 13.58/2.20  % (779287)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=1984444091:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 13.58/2.20  % (779291)ott-21_1_sil=16000:fs=off:random_seed=2770170805:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 13.58/2.20  % (779286)Instruction limit reached! 
% 13.58/2.20  % (779286)------------------------------
% 13.58/2.20  % (779286)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.58/2.20  % (779286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.58/2.20  % (779286)CaDiCaL version: 2.1.3
% 13.58/2.20  % (779286)Termination reason: Instruction limit
% 44.54/6.69  % (779286)Termination phase: Property scanning
% 44.54/6.69  % (779286)Time elapsed: 0.060 s
% 44.54/6.69  % (779286)Peak memory usage: 13 MB
% 44.54/6.69  % (779286)Instructions burned: 134 (million)
% 44.54/6.69  % (779293)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2206222614:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 44.54/6.69  % TRYING [1]
% 44.54/6.69  % TRYING [2]
% 44.54/6.69  % (779291)Instruction limit reached! 
% 44.54/6.69  % (779291)------------------------------
% 44.54/6.69  % (779291)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.54/6.69  % (779291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.54/6.69  % (779291)CaDiCaL version: 2.1.3
% 44.54/6.69  % (779291)Termination reason: Instruction limit
% 44.54/6.69  % (779291)Termination phase: Saturation
% 44.54/6.69  % (779291)Time elapsed: 0.085 s
% 44.54/6.69  % (779291)Peak memory usage: 14 MB
% 44.54/6.69  % (779291)Instructions burned: 180 (million)
% 44.54/6.69  % (779295)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=979444259:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 44.54/6.69  % TRYING [3]
% 44.54/6.69  % TRYING [1]
% 44.54/6.69  % TRYING [2]
% 44.54/6.69  % (779285)Instruction limit reached! 
% 44.54/6.69  % (779285)------------------------------
% 44.54/6.69  % (779285)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.54/6.69  % (779285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.54/6.69  % (779285)CaDiCaL version: 2.1.3
% 44.54/6.69  % (779285)Termination reason: Instruction limit
% 44.54/6.69  % (779285)Termination phase: Finite model building constraint generation
% 44.54/6.69  % (779285)Time elapsed: 0.334 s
% 44.54/6.69  % (779285)Peak memory usage: 24 MB
% 44.54/6.69  % (779285)Instructions burned: 714 (million)
% 44.54/6.69  % (779297)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=440925680:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 44.54/6.69  % (779293)Instruction limit reached! 
% 44.54/6.69  % (779293)------------------------------
% 44.54/6.69  % (779293)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.54/6.69  % (779293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.54/6.69  % (779293)CaDiCaL version: 2.1.3
% 44.54/6.69  % (779293)Termination reason: Instruction limit
% 44.54/6.69  % (779293)Termination phase: Saturation
% 44.54/6.69  % (779293)Time elapsed: 0.300 s
% 44.54/6.69  % (779293)Peak memory usage: 16 MB
% 44.54/6.69  % (779293)Instructions burned: 478 (million)
% 44.54/6.69  % (779299)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2482841434:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 44.54/6.69  % (779287)Instruction limit reached! 
% 44.54/6.69  % (779287)------------------------------
% 44.54/6.69  % (779287)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.54/6.69  % (779287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.54/6.69  % (779287)CaDiCaL version: 2.1.3
% 44.54/6.69  % (779287)Termination reason: Instruction limit
% 44.54/6.69  % (779287)Termination phase: Saturation
% 44.54/6.69  % (779287)Time elapsed: 0.428 s
% 44.54/6.69  % (779287)Peak memory usage: 20 MB
% 44.54/6.69  % (779287)Instructions burned: 685 (million)
% 44.54/6.69  % TRYING [1]
% 44.54/6.69  % (779301)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=4268257087:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 44.54/6.69  % TRYING [2]
% 44.54/6.69  % (779295)Instruction limit reached! 
% 44.54/6.69  % (779295)------------------------------
% 44.54/6.69  % (779295)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.54/6.69  % (779295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.54/6.69  % (779295)CaDiCaL version: 2.1.3
% 44.54/6.69  % (779295)Termination reason: Instruction limit
% 44.54/6.69  % (779295)Termination phase: Finite model building constraint generation
% 44.54/6.69  % (779295)Time elapsed: 0.406 s
% 44.54/6.69  % (779295)Peak memory usage: 33 MB
% 44.54/6.69  % (779295)Instructions burned: 866 (million)
% 44.54/6.69  % (779303)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2873168383:i=879:kws=inv_precedence:fsr=off_2992 on theBenchmark for (2992ds/879Mi)
% 44.54/6.69  % TRYING [4]
% 44.54/6.69  % (779299)Instruction limit reached! 
% 44.54/6.69  % (779299)------------------------------
% 44.54/6.69  % (779299)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.54/6.69  % (779299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.92/15.51  % (779299)CaDiCaL version: 2.1.3
% 107.92/15.51  % (779299)Termination reason: Instruction limit
% 107.92/15.51  % (779299)Termination phase: Finite model building constraint generation
% 107.92/15.51  % (779299)Time elapsed: 0.438 s
% 107.92/15.51  % (779299)Peak memory usage: 53 MB
% 107.92/15.51  % (779299)Instructions burned: 891 (million)
% 107.92/15.51  % (779305)fmb+10_1_sil=64000:random_seed=2636588664:i=22061:nm=2:gsp=on_2989 on theBenchmark for (2989ds/22061Mi)
% 107.92/15.51  % (779301)Instruction limit reached! 
% 107.92/15.51  % (779301)------------------------------
% 107.92/15.51  % (779301)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 107.92/15.51  % (779301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.92/15.51  % (779301)CaDiCaL version: 2.1.3
% 107.92/15.51  % (779301)Termination reason: Instruction limit
% 107.92/15.51  % (779301)Termination phase: Saturation
% 107.92/15.51  % (779301)Time elapsed: 0.453 s
% 107.92/15.51  % (779301)Peak memory usage: 21 MB
% 107.92/15.51  % (779301)Instructions burned: 692 (million)
% 107.92/15.51  % (779307)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2304923498:i=9515:nm=5_2989 on theBenchmark for (2989ds/9515Mi)
% 107.92/15.51  % (779303)Instruction limit reached! 
% 107.92/15.51  % (779303)------------------------------
% 107.92/15.51  % (779303)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 107.92/15.51  % (779303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.92/15.51  % (779303)CaDiCaL version: 2.1.3
% 107.92/15.51  % (779303)Termination reason: Instruction limit
% 107.92/15.51  % (779303)Termination phase: Saturation
% 107.92/15.51  % (779303)Time elapsed: 0.445 s
% 107.92/15.51  % (779303)Peak memory usage: 20 MB
% 107.92/15.51  % (779303)Instructions burned: 880 (million)
% 107.92/15.51  % (779309)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2383174721:fmbsr=1.7:i=920_2988 on theBenchmark for (2988ds/920Mi)
% 107.92/15.51  % (779297)Instruction limit reached! 
% 107.92/15.51  % (779297)------------------------------
% 107.92/15.51  % (779297)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 107.92/15.51  % (779297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.92/15.51  % (779297)CaDiCaL version: 2.1.3
% 107.92/15.51  % (779297)Termination reason: Instruction limit
% 107.92/15.51  % (779297)Termination phase: Saturation
% 107.92/15.51  % (779297)Time elapsed: 0.736 s
% 107.92/15.51  % (779297)Peak memory usage: 23 MB
% 107.92/15.51  % (779297)Instructions burned: 1180 (million)
% 107.92/15.51  % (779311)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3346432320:i=5131_2987 on theBenchmark for (2987ds/5131Mi)
% 107.92/15.51  % TRYING [1]
% 107.92/15.51  % TRYING [2]
% 107.92/15.51  % (779307)Cannot represent all propositional literals internally
% 107.92/15.51  % (779307)Refutation not found, incomplete strategy
% 107.92/15.51  % (779307)------------------------------
% 107.92/15.51  % (779307)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 107.92/15.51  % (779307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.92/15.51  % (779307)CaDiCaL version: 2.1.3
% 107.92/15.51  % (779307)Termination reason: Refutation not found, incomplete strategy
% 107.92/15.51  % (779307)Time elapsed: 0.311 s
% 107.92/15.51  % (779307)Peak memory usage: 22 MB
% 107.92/15.51  % (779307)Instructions burned: 647 (million)
% 107.92/15.51  % (779307)------------------------------
% 107.92/15.51  % (779307)------------------------------
% 107.92/15.51  % (779313)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3508293738:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi)
% 107.92/15.51  % TRYING [8]
% 107.92/15.51  % (779309)Instruction limit reached! 
% 107.92/15.51  % (779309)------------------------------
% 107.92/15.51  % (779309)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 107.92/15.51  % (779309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.92/15.51  % (779309)CaDiCaL version: 2.1.3
% 107.92/15.51  % (779309)Termination reason: Instruction limit
% 107.92/15.51  % (779309)Termination phase: Finite model building constraint generation
% 107.92/15.51  % (779309)Time elapsed: 0.408 s
% 107.92/15.51  % (779309)Peak memory usage: 39 MB
% 107.92/15.51  % (779309)Instructions burned: 921 (million)
% 107.92/15.51  % (779315)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1985487002:i=6324_2983 on theBenchmark for (2983ds/6324Mi)
% 107.92/15.51  % (779315)Cannot represent all propositional literals internally
% 107.92/15.51  % (779315)Refutation not found, incomplete strategy
% 107.92/15.51  % (779315)------------------------------
% 107.92/15.51  % (779315)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 244.80/34.81  % (779315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 244.80/34.81  % (779315)CaDiCaL version: 2.1.3
% 244.80/34.81  % (779315)Termination reason: Refutation not found, incomplete strategy
% 244.80/34.81  % (779315)Time elapsed: 0.334 s
% 244.80/34.81  % (779315)Peak memory usage: 23 MB
% 244.80/34.81  % (779315)Instructions burned: 694 (million)
% 244.80/34.81  % (779315)------------------------------
% 244.80/34.81  % (779315)------------------------------
% 244.80/34.81  % (779317)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=4140974876:fmbsr=2.30978:i=2174_2980 on theBenchmark for (2980ds/2174Mi)
% 244.80/34.81  % (779313)Instruction limit reached! 
% 244.80/34.81  % (779313)------------------------------
% 244.80/34.81  % (779313)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 244.80/34.81  % (779313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 244.80/34.81  % (779313)CaDiCaL version: 2.1.3
% 244.80/34.81  % (779313)Termination reason: Instruction limit
% 244.80/34.81  % (779313)Termination phase: Saturation
% 244.80/34.81  % (779313)Time elapsed: 0.765 s
% 244.80/34.81  % (779313)Peak memory usage: 28 MB
% 244.80/34.81  % (779313)Instructions burned: 1474 (million)
% 244.80/34.81  % (779319)ott-2_1_sil=16000:newcnf=on:random_seed=1570357368:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2978 on theBenchmark for (2978ds/869Mi)
% 244.80/34.81  % TRYING [3]
% 244.80/34.81  % (779319)Instruction limit reached! 
% 244.80/34.81  % (779319)------------------------------
% 244.80/34.81  % (779319)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 244.80/34.81  % (779319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 244.80/34.81  % (779319)CaDiCaL version: 2.1.3
% 244.80/34.81  % (779319)Termination reason: Instruction limit
% 244.80/34.81  % (779319)Termination phase: Saturation
% 244.80/34.81  % (779319)Time elapsed: 0.504 s
% 244.80/34.81  % (779319)Peak memory usage: 18 MB
% 244.80/34.81  % (779319)Instructions burned: 870 (million)
% 244.80/34.81  % (779321)ott+10_1_sil=32000:tgt=ground:random_seed=3021136863:i=5114:av=off_2972 on theBenchmark for (2972ds/5114Mi)
% 244.80/34.81  % (779317)Instruction limit reached! 
% 244.80/34.81  % (779317)------------------------------
% 244.80/34.81  % (779317)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 244.80/34.81  % (779317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 244.80/34.81  % (779317)CaDiCaL version: 2.1.3
% 244.80/34.81  % (779317)Termination reason: Instruction limit
% 244.80/34.81  % (779317)Termination phase: Finite model building preprocessing
% 244.80/34.81  % (779317)Time elapsed: 1.087 s
% 244.80/34.81  % (779317)Peak memory usage: 37 MB
% 244.80/34.81  % (779317)Instructions burned: 2175 (million)
% 244.80/34.81  % (779323)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=968153783:i=54282_2969 on theBenchmark for (2969ds/54282Mi)
% 244.80/34.81  % TRYING [5]
% 244.80/34.81  % TRYING [1]
% 244.80/34.81  % TRYING [2]
% 244.80/34.81  % TRYING [3]
% 244.80/34.81  % (779311)Instruction limit reached! 
% 244.80/34.81  % (779311)------------------------------
% 244.80/34.81  % (779311)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 244.80/34.81  % (779311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 244.80/34.81  % (779311)CaDiCaL version: 2.1.3
% 244.80/34.81  % (779311)Termination reason: Instruction limit
% 244.80/34.81  % (779311)Termination phase: Saturation
% 244.80/34.81  % (779311)Time elapsed: 3.051 s
% 244.80/34.81  % (779311)Peak memory usage: 36 MB
% 244.80/34.81  % (779311)Instructions burned: 5132 (million)
% 244.80/34.81  % (779325)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=695609031:i=3512:aac=none_2956 on theBenchmark for (2956ds/3512Mi)
% 244.80/34.81  % TRYING [4]
% 244.80/34.81  % TRYING [4]
% 244.80/34.81  % (779321)Instruction limit reached! 
% 244.80/34.81  % (779321)------------------------------
% 244.80/34.81  % (779321)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 244.80/34.81  % (779321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 244.80/34.81  % (779321)CaDiCaL version: 2.1.3
% 244.80/34.81  % (779321)Termination reason: Instruction limit
% 244.80/34.81  % (779321)Termination phase: Saturation
% 244.80/34.81  % (779321)Time elapsed: 3.345 s
% 244.80/34.81  % (779321)Peak memory usage: 39 MB
% 244.80/34.81  % (779321)Instructions burned: 5114 (million)
% 244.80/34.81  % (779327)dis+21_1_sil=32000:sas=cadical:random_seed=2060257637:i=3773:amm=off_2939 on theBenchmark for (2939ds/3773Mi)
% 244.80/34.81  % (779325)Instruction limit reached! 
% 244.80/34.81  % (779325)------------------------------
% 244.80/34.81  % (779325)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 244.80/34.81  % (779325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 227.92/41.99  % (779325)CaDiCaL version: 2.1.3
% 227.92/41.99  % (779325)Termination reason: Instruction limit
% 227.92/41.99  % (779325)Termination phase: Saturation
% 227.92/41.99  % (779325)Time elapsed: 2.108 s
% 227.92/41.99  % (779325)Peak memory usage: 36 MB
% 227.92/41.99  % (779325)Instructions burned: 3513 (million)
% 227.92/41.99  % (779329)ott+11_1_sil=16000:gs=on:random_seed=2259069344:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2935 on theBenchmark for (2935ds/2251Mi)
% 227.92/41.99  % (779329)Instruction limit reached! 
% 227.92/41.99  % (779329)------------------------------
% 227.92/41.99  % (779329)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 227.92/41.99  % (779329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 227.92/41.99  % (779329)CaDiCaL version: 2.1.3
% 227.92/41.99  % (779329)Termination reason: Instruction limit
% 227.92/41.99  % (779329)Termination phase: Saturation
% 227.92/41.99  % (779329)Time elapsed: 1.358 s
% 227.92/41.99  % (779329)Peak memory usage: 31 MB
% 227.92/41.99  % (779329)Instructions burned: 2251 (million)
% 227.92/41.99  % (779331)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3363255471:fmbsr=1.6:i=67534_2921 on theBenchmark for (2921ds/67534Mi)
% 227.92/41.99  % (779327)Instruction limit reached! 
% 227.92/41.99  % (779327)------------------------------
% 227.92/41.99  % (779327)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 227.92/41.99  % (779327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 227.92/41.99  % (779327)CaDiCaL version: 2.1.3
% 227.92/41.99  % (779327)Termination reason: Instruction limit
% 227.92/41.99  % (779327)Termination phase: Saturation
% 227.92/41.99  % (779327)Time elapsed: 2.219 s
% 227.92/41.99  % (779327)Peak memory usage: 37 MB
% 227.92/41.99  % (779327)Instructions burned: 3773 (million)
% 227.92/41.99  % (779333)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2809741769:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2916 on theBenchmark for (2916ds/4591Mi)
% 227.92/41.99  % TRYING [5]
% 227.92/41.99  % (779333)Instruction limit reached! 
% 227.92/41.99  % (779333)------------------------------
% 227.92/41.99  % (779333)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 227.92/41.99  % (779333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 227.92/41.99  % (779333)CaDiCaL version: 2.1.3
% 227.92/41.99  % (779333)Termination reason: Instruction limit
% 227.92/41.99  % (779333)Termination phase: Saturation
% 227.92/41.99  % (779333)Time elapsed: 1.847 s
% 227.92/41.99  % (779333)Peak memory usage: 33 MB
% 227.92/41.99  % (779333)Instructions burned: 4592 (million)
% 227.92/41.99  % (779335)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2221268638:i=29340_2897 on theBenchmark for (2897ds/29340Mi)
% 227.92/41.99  % (779305)Instruction limit reached! 
% 227.92/41.99  % (779305)------------------------------
% 227.92/41.99  % (779305)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 227.92/41.99  % (779305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 227.92/41.99  % (779305)CaDiCaL version: 2.1.3
% 227.92/41.99  % (779305)Termination reason: Instruction limit
% 227.92/41.99  % (779305)Termination phase: Finite model building SAT solving
% 227.92/41.99  % (779305)Time elapsed: 9.407 s
% 227.92/41.99  % (779305)Peak memory usage: 508 MB
% 227.92/41.99  % (779305)Instructions burned: 22062 (million)
% 227.92/41.99  % (779337)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1621807769:i=5211_2895 on theBenchmark for (2895ds/5211Mi)
% 227.92/41.99  % TRYING [7]
% 227.92/41.99  % TRYING [6]
% 227.92/41.99  % (779337)Instruction limit reached! 
% 227.92/41.99  % (779337)------------------------------
% 227.92/41.99  % (779337)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 227.92/41.99  % (779337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 227.92/41.99  % (779337)CaDiCaL version: 2.1.3
% 227.92/41.99  % (779337)Termination reason: Instruction limit
% 227.92/41.99  % (779337)Termination phase: Saturation
% 227.92/41.99  % (779337)Time elapsed: 2.639 s
% 227.92/41.99  % (779337)Peak memory usage: 43 MB
% 227.92/41.99  % (779337)Instructions burned: 5214 (million)
% 227.92/41.99  % (779339)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1877367474:i=5497:nm=2_2868 on theBenchmark for (2868ds/5497Mi)
% 227.92/41.99  % TRYING [17]
% 227.92/41.99  % (779339)Instruction limit reached! 
% 227.92/41.99  % (779339)------------------------------
% 227.92/41.99  % (779339)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 227.92/41.99  % (779339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 227.92/41.99  % (779339)CaDiCaL version: 2.1.3
% 227.92/41.99  % (779339)Termination reason: Instruction limit
% 227.92/41.99  % (779339)Termination phase: Finite model building constraint generation
% 227.92/41.99  % (779339)Time elapsed: 2.081 s
% 227.92/41.99  % (779339)Peak memory usage: 335 MB
% 227.92/41.99  % (779339)Instructions burned: 5499 (million)
% 227.92/41.99  % (779341)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=573914878:fmbsr=2:i=46332_2846 on theBenchmark for (2846ds/46332Mi)
% 227.92/41.99  % TRYING [15]
% 227.92/41.99  % TRYING [6]
% 227.92/41.99  % (779335)Instruction limit reached! 
% 227.92/41.99  % (779335)------------------------------
% 227.92/41.99  % (779335)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 227.92/41.99  % (779335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 227.92/41.99  % (779335)CaDiCaL version: 2.1.3
% 227.92/41.99  % (779335)Termination reason: Instruction limit
% 227.92/41.99  % (779335)Termination phase: Saturation
% 227.92/41.99  % (779335)Time elapsed: 14.515 s
% 227.92/41.99  % (779335)Peak memory usage: 191 MB
% 227.92/41.99  % (779335)Instructions burned: 29342 (million)
% 227.92/41.99  % (779323)Instruction limit reached! 
% 227.92/41.99  % (779323)------------------------------
% 227.92/41.99  % (779323)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 227.92/41.99  % (779323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 227.92/41.99  % (779323)CaDiCaL version: 2.1.3
% 227.92/41.99  % (779323)Termination reason: Instruction limit
% 227.92/41.99  % (779323)Termination phase: Finite model building constraint generation
% 227.92/41.99  % (779323)Time elapsed: 21.679 s
% 227.92/41.99  % (779323)Peak memory usage: 1854 MB
% 227.92/41.99  % (779323)Instructions burned: 54283 (million)
% 227.92/41.99  % (779343)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3985395699:i=14071_2752 on theBenchmark for (2752ds/14071Mi)
% 227.92/41.99  % (779345)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=380651124:i=22565:add=on:rawr=on_2749 on theBenchmark for (2749ds/22565Mi)
% 227.92/41.99  % TRYING [12]
% 227.92/41.99  % TRYING [7]
% 227.92/41.99  % (779343)Instruction limit reached! 
% 227.92/41.99  % (779343)------------------------------
% 227.92/41.99  % (779343)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 227.92/41.99  % (779343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 227.92/41.99  % (779343)CaDiCaL version: 2.1.3
% 227.92/41.99  % (779343)Termination reason: Instruction limit
% 227.92/41.99  % (779343)Termination phase: Finite model building constraint generation
% 227.92/41.99  % (779343)Time elapsed: 5.032 s
% 227.92/41.99  % (779343)Peak memory usage: 808 MB
% 227.92/41.99  % (779343)Instructions burned: 14074 (million)
% 227.92/41.99  % (779347)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3583050182:i=8173:av=off_2700 on theBenchmark for (2700ds/8173Mi)
% 227.92/41.99  % (779331)Instruction limit reached! 
% 227.92/41.99  % (779331)------------------------------
% 227.92/41.99  % (779331)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 227.92/41.99  % (779331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 227.92/41.99  % (779331)CaDiCaL version: 2.1.3
% 227.92/41.99  % (779331)Termination reason: Instruction limit
% 227.92/41.99  % (779331)Termination phase: Finite model building constraint generation
% 227.92/41.99  % (779331)Time elapsed: 22.795 s
% 227.92/41.99  % (779331)Peak memory usage: 3573 MB
% 227.92/41.99  % (779331)Instructions burned: 67536 (million)
% 227.92/41.99  % (779341)Instruction limit reached! 
% 227.92/41.99  % (779341)------------------------------
% 227.92/41.99  % (779341)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 227.92/41.99  % (779341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 227.92/41.99  % (779341)CaDiCaL version: 2.1.3
% 227.92/41.99  % (779341)Termination reason: Instruction limit
% 227.92/41.99  % (779341)Termination phase: Finite model building constraint generation
% 227.92/41.99  % (779341)Time elapsed: 15.632 s
% 227.92/41.99  % (779341)Peak memory usage: 2357 MB
% 227.92/41.99  % (779341)Instructions burned: 46333 (million)
% 227.92/41.99  % (779349)dis+10_16:1_sil=16000:random_seed=4274946276:i=9155:fsr=off_2688 on theBenchmark for (2688ds/9155Mi)
% 227.92/41.99  % (779351)ott-3_8_sil=64000:random_seed=3586634132:i=20139:bs=on_2687 on theBenchmark for (2687ds/20139Mi)
% 227.92/41.99  % (779347)Instruction limit reached! 
% 227.92/41.99  % (779347)------------------------------
% 227.92/41.99  % (779347)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 227.92/41.99  % (779347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 227.92/41.99  % (779347)CaDiCaL version: 2.1.3
% 227.92/41.99  % (779347)Termination reason: Instruction limit
% 227.92/41.99  % (779347)Termination phase: Saturation
% 227.92/41.99  % (779347)Time elapsed: 4.626 s
% 227.92/41.99  % (779347)Peak memory usage: 33 MB
% 227.92/41.99  % (779347)Instructions burned: 8173 (million)
% 227.92/41.99  % (779353)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1031571425:fmbsr=2:i=32576_2654 on theBenchmark for (2654ds/32576Mi)
% 227.92/41.99  % TRYING [9]
% 227.92/41.99  % (779345)Instruction limit reached! 
% 227.92/41.99  % (779345)------------------------------
% 227.92/41.99  % (779345)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 227.92/41.99  % (779345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 227.92/41.99  % (779345)CaDiCaL version: 2.1.3
% 227.92/41.99  % (779345)Termination reason: Instruction limit
% 227.92/41.99  % (779345)Termination phase: Saturation
% 227.92/41.99  % (779345)Time elapsed: 10.352 s
% 227.92/41.99  % (779345)Peak memory usage: 123 MB
% 227.92/41.99  % (779345)Instructions burned: 22565 (million)
% 227.92/41.99  % (779355)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=50192285:i=11404_2646 on theBenchmark for (2646ds/11404Mi)
% 227.92/41.99  % (779349)Instruction limit reached! 
% 227.92/41.99  % (779349)------------------------------
% 227.92/41.99  % (779349)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 227.92/41.99  % (779349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 227.92/41.99  % (779349)CaDiCaL version: 2.1.3
% 227.92/41.99  % (779349)Termination reason: Instruction limit
% 227.92/41.99  % (779349)Termination phase: Saturation
% 227.92/41.99  % (779349)Time elapsed: 4.732 s
% 227.92/41.99  % (779349)Peak memory usage: 75 MB
% 227.92/41.99  % (779349)Instructions burned: 9156 (million)
% 227.92/41.99  % (779357)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3191420048:i=14134_2640 on theBenchmark for (2640ds/14134Mi)
% 227.92/41.99  % (779273)Instruction limit reached! 
% 227.92/41.99  % (779273)------------------------------
% 227.92/41.99  % (779273)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 227.92/41.99  % (779273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 227.92/41.99  % (779273)CaDiCaL version: 2.1.3
% 227.92/41.99  % (779273)Termination reason: Instruction limit
% 227.92/41.99  % (779273)Termination phase: Saturation
% 227.92/41.99  % (779273)Time elapsed: 38.914 s
% 227.92/41.99  % (779273)Peak memory usage: 345 MB
% 227.92/41.99  % (779273)Instructions burned: 88025 (million)
% 227.92/41.99  % (779359)dis+33_16_sil=32000:sac=on:random_seed=1167730868:i=15851:nm=0_2609 on theBenchmark for (2609ds/15851Mi)
% 227.92/41.99  % (779355) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-779266-779355"...
% 227.92/41.99  % (779355)...printing done.
% 227.92/41.99  % (779355)Refutation found. Thanks to Tanya!
% 227.92/41.99  % SZS status Theorem for theBenchmark
% 227.92/41.99  % SZS output start Proof for theBenchmark
% See solution above
% 227.92/42.00  % (779355)------------------------------
% 227.92/42.00  % (779355)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 227.92/42.00  % (779355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 227.92/42.00  % (779355)CaDiCaL version: 2.1.3
% 227.92/42.00  % (779355)Termination reason: Refutation
% 227.92/42.00  % (779355)Time elapsed: 5.610 s
% 227.92/42.00  % (779355)Peak memory usage: 69 MB
% 227.92/42.00  % (779355)Instructions burned: 8256 (million)
% 227.92/42.00  % (779266)Success in time 41.75 s
% 227.92/42.00  % Vampire exiting
%------------------------------------------------------------------------------