%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW226+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n016.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:29:53 PM UTC 2026
% Result : Theorem 84.65s 17.80s
% Output : Refutation 121.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 54
% Number of leaves : 65
% Syntax : Number of formulae : 300 ( 178 unt; 17 def)
% Number of atoms : 549 ( 219 equ)
% Maximal formula atoms : 11 ( 1 avg)
% Number of connectives : 460 ( 211 ~; 194 |; 25 &)
% ( 12 <=>; 18 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 3 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 13 ( 11 usr; 3 prp; 0-3 aty)
% Number of functors : 43 ( 43 usr; 25 con; 0-3 aty)
% Number of variables : 357 ( 0 sgn 351 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),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_RealDef_Oreal(tc_Nat_Onat,v_N2____)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_N2) ).
fof(f20,axiom,
! [X0] : c_Groups_Oplus__class_Oplus(tc_Int_Oint,X0,c_Int_OPls) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_add__Pls__right) ).
fof(f21,axiom,
! [X0] : c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OPls,X0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_add__Pls) ).
fof(f23,axiom,
! [X0] : c_Int_OBit0(X0) = c_Groups_Oplus__class_Oplus(tc_Int_Oint,X0,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_Bit0__def) ).
fof(f30,axiom,
! [X0] : c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X0) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_real__norm__def) ).
fof(f91,axiom,
! [X0] : c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(X0))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_RealDef_Oreal(tc_Nat_Onat,c_Nat_OSuc(X0))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_g_I2_J) ).
fof(f115,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/sandbox2/benchmark/theBenchmark.p',fact_zadd__assoc) ).
fof(f131,axiom,
c_RealDef_Oreal(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat)) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_real__of__nat__zero) ).
fof(f138,axiom,
! [X0] : c_RealDef_Oreal(tc_Nat_Onat,c_Nat_OSuc(X0)) = c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,X0),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_real__of__nat__Suc) ).
fof(f157,axiom,
! [X0,X1] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,X1),c_RealDef_Oreal(tc_Nat_Onat,X0))
<=> c_Orderings_Oord__class_Oless(tc_Nat_Onat,X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_real__of__nat__less__iff) ).
fof(f164,axiom,
! [X0,X1] :
( c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,X0) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)
<=> X0 = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_real__add__eq__0__iff) ).
fof(f167,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/sandbox2/benchmark/theBenchmark.p',fact_minus__real__def) ).
fof(f177,axiom,
! [X0] : c_Orderings_Oord__class_Oless__eq(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____(X0)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact__096_B_Bn_O_A_N_As_A_060_061_Acmod_A_Ipoly_Ap_A_Ig_An_J_J_096) ).
fof(f213,axiom,
! [X0,X1] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X1,X0)
<=> ( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X0)
& X1 != X0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_real__less__def) ).
fof(f228,axiom,
! [X0,X1,X2,X3,X4] :
( class_Groups_Oordered__cancel__ab__semigroup__add(X4)
=> ( c_Orderings_Oord__class_Oless(X4,X3,X2)
=> ( c_Orderings_Oord__class_Oless__eq(X4,X1,X0)
=> c_Orderings_Oord__class_Oless(X4,c_Groups_Oplus__class_Oplus(X4,X3,X1),c_Groups_Oplus__class_Oplus(X4,X2,X0)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_add__less__le__mono) ).
fof(f255,axiom,
! [X0,X1,X2,X3] :
( class_Groups_Oordered__comm__monoid__add(X3)
=> ( c_Orderings_Oord__class_Oless__eq(X3,c_Groups_Ozero__class_Ozero(X3),X2)
=> ( c_Orderings_Oord__class_Oless(X3,X1,X0)
=> c_Orderings_Oord__class_Oless(X3,X1,c_Groups_Oplus__class_Oplus(X3,X2,X0)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_add__strict__increasing2) ).
fof(f273,axiom,
! [X0] : c_Nat_OSuc(X0) = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X0,c_Groups_Oone__class_Oone(tc_Nat_Onat)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_Suc__eq__plus1) ).
fof(f280,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/sandbox2/benchmark/theBenchmark.p',fact_Bit1__def) ).
fof(f323,axiom,
! [X0,X1,X2,X3,X4] :
( class_Groups_Oordered__cancel__ab__semigroup__add(X4)
=> ( c_Orderings_Oord__class_Oless(X4,X3,X2)
=> ( c_Orderings_Oord__class_Oless(X4,X1,X0)
=> c_Orderings_Oord__class_Oless(X4,c_Groups_Oplus__class_Oplus(X4,X3,X1),c_Groups_Oplus__class_Oplus(X4,X2,X0)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_add__strict__mono) ).
fof(f327,axiom,
! [X0,X1,X2,X3] :
( class_Groups_Oordered__ab__semigroup__add__imp__le(X3)
=> ( c_Orderings_Oord__class_Oless(X3,c_Groups_Oplus__class_Oplus(X3,X2,X1),c_Groups_Oplus__class_Oplus(X3,X0,X1))
<=> c_Orderings_Oord__class_Oless(X3,X2,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_add__less__cancel__right) ).
fof(f339,axiom,
! [X0,X1,X2] :
( class_Groups_Ogroup__add(X2)
=> c_Groups_Oplus__class_Oplus(X2,c_Groups_Ominus__class_Ominus(X2,X1,X0),X0) = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_diff__add__cancel) ).
fof(f411,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/sandbox2/benchmark/theBenchmark.p',fact_real__mult__commute) ).
fof(f445,axiom,
! [X0] : c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),X0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_real__mult__1) ).
fof(f447,axiom,
! [X0,X1] : c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X1,X0),c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X1,X1)) = c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X0,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_real__divide__square__eq) ).
fof(f460,axiom,
! [X0,X1,X2,X3] :
( class_Fields_Ofield__inverse__zero(X3)
=> ( X2 = c_Rings_Oinverse__class_Odivide(X3,X1,X0)
<=> ( ( X0 != c_Groups_Ozero__class_Ozero(X3)
=> c_Groups_Otimes__class_Otimes(X3,X2,X0) = X1 )
& ( X0 = c_Groups_Ozero__class_Ozero(X3)
=> X2 = c_Groups_Ozero__class_Ozero(X3) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_eq__divide__eq) ).
fof(f534,axiom,
! [X0,X1] : c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X1,X0) = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X0,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_nat__add__commute) ).
fof(f536,axiom,
! [X0,X1,X2] : c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X2,X1),X0) = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X2,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X1,X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_nat__add__assoc) ).
fof(f565,axiom,
! [X0,X1] :
( class_Int_Onumber__ring(X1)
=> c_Groups_Otimes__class_Otimes(X1,X0,c_Int_Onumber__class_Onumber__of(X1,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))) = c_Groups_Oplus__class_Oplus(X1,X0,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_mult__2__right) ).
fof(f579,axiom,
! [X0] : ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,X0,c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_not__less0) ).
fof(f580,axiom,
! [X0,X1] :
( ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,X1,X0)
<=> c_Orderings_Oord__class_Oless(tc_Nat_Onat,X0,c_Nat_OSuc(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_not__less__eq) ).
fof(f594,axiom,
! [X0,X1] :
( c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X1,X0) = X1
=> X0 = c_Groups_Ozero__class_Ozero(tc_Nat_Onat) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_add__eq__self__zero) ).
fof(f596,axiom,
! [X0] : c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_less__eq__nat_Osimps_I1_J) ).
fof(f597,axiom,
! [X0,X1] : c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X1,c_Nat_OSuc(X0)) = c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X1,X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_add__Suc__right) ).
fof(f607,axiom,
! [X0,X1] : ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X1,X0),X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_not__add__less1) ).
fof(f608,axiom,
! [X0,X1] : ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X1,X0),X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_not__add__less2) ).
fof(f641,axiom,
! [X0,X1] : c_Groups_Ominus__class_Ominus(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X1,X0),X0) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_diff__add__inverse2) ).
fof(f657,axiom,
! [X0] :
( c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),X0)
<=> ? [X1] : X0 = c_Nat_OSuc(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_gr0__conv__Suc) ).
fof(f663,axiom,
! [X0,X1] :
( c_Orderings_Oord__class_Oless(tc_Nat_Onat,X1,X0)
<=> ? [X2] : X0 = c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X1,X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_less__iff__Suc__add) ).
fof(f678,axiom,
! [X0,X1] :
( ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,X1,X0)
=> c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X0,c_Groups_Ominus__class_Ominus(tc_Nat_Onat,X1,X0)) = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_add__diff__inverse) ).
fof(f926,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/sandbox2/benchmark/theBenchmark.p',fact_comm__semiring__1__class_Onormalizing__semiring__rules_I24_J) ).
fof(f1056,axiom,
class_Groups_Oordered__comm__monoid__add(tc_Nat_Onat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arity_Nat__Onat__Groups_Oordered__comm__monoid__add) ).
fof(f1083,axiom,
class_Groups_Oordered__cancel__ab__semigroup__add(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arity_RealDef__Oreal__Groups_Oordered__cancel__ab__semigroup__add) ).
fof(f1084,axiom,
class_Groups_Oordered__ab__semigroup__add__imp__le(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arity_RealDef__Oreal__Groups_Oordered__ab__semigroup__add__imp__le) ).
fof(f1109,axiom,
class_Fields_Ofield__inverse__zero(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arity_RealDef__Oreal__Fields_Ofield__inverse__zero) ).
fof(f1121,axiom,
class_Rings_Ocomm__semiring__1(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arity_RealDef__Oreal__Rings_Ocomm__semiring__1) ).
fof(f1133,axiom,
class_Groups_Ogroup__add(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arity_RealDef__Oreal__Groups_Ogroup__add) ).
fof(f1136,axiom,
class_Int_Onumber__ring(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arity_RealDef__Oreal__Int_Onumber__ring) ).
fof(f1185,conjecture,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),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_RealDef_Oreal(tc_Nat_Onat,c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0) ).
fof(f1186,negated_conjecture,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),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_RealDef_Oreal(tc_Nat_Onat,c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))),
inference(negated_conjecture,[status(cth)],[f1185]) ).
fof(f1189,plain,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),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_RealDef_Oreal(tc_Nat_Onat,c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))),
inference(flattening,[],[f1186]) ).
fof(f1334,plain,
! [X0,X1,X2,X3,X4] :
( c_Orderings_Oord__class_Oless(X4,c_Groups_Oplus__class_Oplus(X4,X3,X1),c_Groups_Oplus__class_Oplus(X4,X2,X0))
| ~ c_Orderings_Oord__class_Oless__eq(X4,X1,X0)
| ~ c_Orderings_Oord__class_Oless(X4,X3,X2)
| ~ class_Groups_Oordered__cancel__ab__semigroup__add(X4) ),
inference(ennf_transformation,[],[f228]) ).
fof(f1335,plain,
! [X0,X1,X2,X3,X4] :
( c_Orderings_Oord__class_Oless(X4,c_Groups_Oplus__class_Oplus(X4,X3,X1),c_Groups_Oplus__class_Oplus(X4,X2,X0))
| ~ c_Orderings_Oord__class_Oless__eq(X4,X1,X0)
| ~ c_Orderings_Oord__class_Oless(X4,X3,X2)
| ~ class_Groups_Oordered__cancel__ab__semigroup__add(X4) ),
inference(flattening,[],[f1334]) ).
fof(f1373,plain,
! [X0,X1,X2,X3] :
( c_Orderings_Oord__class_Oless(X3,X1,c_Groups_Oplus__class_Oplus(X3,X2,X0))
| ~ c_Orderings_Oord__class_Oless(X3,X1,X0)
| ~ c_Orderings_Oord__class_Oless__eq(X3,c_Groups_Ozero__class_Ozero(X3),X2)
| ~ class_Groups_Oordered__comm__monoid__add(X3) ),
inference(ennf_transformation,[],[f255]) ).
fof(f1374,plain,
! [X0,X1,X2,X3] :
( c_Orderings_Oord__class_Oless(X3,X1,c_Groups_Oplus__class_Oplus(X3,X2,X0))
| ~ c_Orderings_Oord__class_Oless(X3,X1,X0)
| ~ c_Orderings_Oord__class_Oless__eq(X3,c_Groups_Ozero__class_Ozero(X3),X2)
| ~ class_Groups_Oordered__comm__monoid__add(X3) ),
inference(flattening,[],[f1373]) ).
fof(f1440,plain,
! [X0,X1,X2,X3,X4] :
( c_Orderings_Oord__class_Oless(X4,c_Groups_Oplus__class_Oplus(X4,X3,X1),c_Groups_Oplus__class_Oplus(X4,X2,X0))
| ~ c_Orderings_Oord__class_Oless(X4,X1,X0)
| ~ c_Orderings_Oord__class_Oless(X4,X3,X2)
| ~ class_Groups_Oordered__cancel__ab__semigroup__add(X4) ),
inference(ennf_transformation,[],[f323]) ).
fof(f1441,plain,
! [X0,X1,X2,X3,X4] :
( c_Orderings_Oord__class_Oless(X4,c_Groups_Oplus__class_Oplus(X4,X3,X1),c_Groups_Oplus__class_Oplus(X4,X2,X0))
| ~ c_Orderings_Oord__class_Oless(X4,X1,X0)
| ~ c_Orderings_Oord__class_Oless(X4,X3,X2)
| ~ class_Groups_Oordered__cancel__ab__semigroup__add(X4) ),
inference(flattening,[],[f1440]) ).
fof(f1447,plain,
! [X0,X1,X2,X3] :
( ( c_Orderings_Oord__class_Oless(X3,c_Groups_Oplus__class_Oplus(X3,X2,X1),c_Groups_Oplus__class_Oplus(X3,X0,X1))
<=> c_Orderings_Oord__class_Oless(X3,X2,X0) )
| ~ class_Groups_Oordered__ab__semigroup__add__imp__le(X3) ),
inference(ennf_transformation,[],[f327]) ).
fof(f1460,plain,
! [X0,X1,X2] :
( c_Groups_Oplus__class_Oplus(X2,c_Groups_Ominus__class_Ominus(X2,X1,X0),X0) = X1
| ~ class_Groups_Ogroup__add(X2) ),
inference(ennf_transformation,[],[f339]) ).
fof(f1586,plain,
! [X0,X1,X2,X3] :
( ( X2 = c_Rings_Oinverse__class_Odivide(X3,X1,X0)
<=> ( ( c_Groups_Otimes__class_Otimes(X3,X2,X0) = X1
| c_Groups_Ozero__class_Ozero(X3) = X0 )
& ( X2 = c_Groups_Ozero__class_Ozero(X3)
| c_Groups_Ozero__class_Ozero(X3) != X0 ) ) )
| ~ class_Fields_Ofield__inverse__zero(X3) ),
inference(ennf_transformation,[],[f460]) ).
fof(f1701,plain,
! [X0,X1] :
( c_Groups_Otimes__class_Otimes(X1,X0,c_Int_Onumber__class_Onumber__of(X1,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))) = c_Groups_Oplus__class_Oplus(X1,X0,X0)
| ~ class_Int_Onumber__ring(X1) ),
inference(ennf_transformation,[],[f565]) ).
fof(f1717,plain,
! [X0,X1] :
( X0 = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
| c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X1,X0) != X1 ),
inference(ennf_transformation,[],[f594]) ).
fof(f1766,plain,
! [X0,X1] :
( c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X0,c_Groups_Ominus__class_Ominus(tc_Nat_Onat,X1,X0)) = X1
| c_Orderings_Oord__class_Oless(tc_Nat_Onat,X1,X0) ),
inference(ennf_transformation,[],[f678]) ).
fof(f2033,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,[],[f926]) ).
fof(f2167,plain,
! [X0,X1] :
( ( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,X1),c_RealDef_Oreal(tc_Nat_Onat,X0))
| ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,X1,X0) )
& ( c_Orderings_Oord__class_Oless(tc_Nat_Onat,X1,X0)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,X1),c_RealDef_Oreal(tc_Nat_Onat,X0)) ) ),
inference(nnf_transformation,[],[f157]) ).
fof(f2170,plain,
! [X0,X1] :
( ( c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,X0) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)
| c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X1) != X0 )
& ( X0 = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X1)
| c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) != c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,X0) ) ),
inference(nnf_transformation,[],[f164]) ).
fof(f2187,plain,
! [X0,X1] :
( ( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X1,X0)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X0)
| X0 = X1 )
& ( ( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X0)
& X1 != X0 )
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X1,X0) ) ),
inference(nnf_transformation,[],[f213]) ).
fof(f2188,plain,
! [X0,X1] :
( ( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X1,X0)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X0)
| X0 = X1 )
& ( ( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X0)
& X1 != X0 )
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X1,X0) ) ),
inference(flattening,[],[f2187]) ).
fof(f2235,plain,
! [X0,X1,X2,X3] :
( ( ( c_Orderings_Oord__class_Oless(X3,c_Groups_Oplus__class_Oplus(X3,X2,X1),c_Groups_Oplus__class_Oplus(X3,X0,X1))
| ~ c_Orderings_Oord__class_Oless(X3,X2,X0) )
& ( c_Orderings_Oord__class_Oless(X3,X2,X0)
| ~ c_Orderings_Oord__class_Oless(X3,c_Groups_Oplus__class_Oplus(X3,X2,X1),c_Groups_Oplus__class_Oplus(X3,X0,X1)) ) )
| ~ class_Groups_Oordered__ab__semigroup__add__imp__le(X3) ),
inference(nnf_transformation,[],[f1447]) ).
fof(f2283,plain,
! [X0,X1,X2,X3] :
( ( ( X2 = c_Rings_Oinverse__class_Odivide(X3,X1,X0)
| ( c_Groups_Otimes__class_Otimes(X3,X2,X0) != X1
& c_Groups_Ozero__class_Ozero(X3) != X0 )
| ( c_Groups_Ozero__class_Ozero(X3) != X2
& c_Groups_Ozero__class_Ozero(X3) = X0 ) )
& ( ( ( c_Groups_Otimes__class_Otimes(X3,X2,X0) = X1
| c_Groups_Ozero__class_Ozero(X3) = X0 )
& ( X2 = c_Groups_Ozero__class_Ozero(X3)
| c_Groups_Ozero__class_Ozero(X3) != X0 ) )
| c_Rings_Oinverse__class_Odivide(X3,X1,X0) != X2 ) )
| ~ class_Fields_Ofield__inverse__zero(X3) ),
inference(nnf_transformation,[],[f1586]) ).
fof(f2284,plain,
! [X0,X1,X2,X3] :
( ( ( X2 = c_Rings_Oinverse__class_Odivide(X3,X1,X0)
| ( c_Groups_Otimes__class_Otimes(X3,X2,X0) != X1
& c_Groups_Ozero__class_Ozero(X3) != X0 )
| ( c_Groups_Ozero__class_Ozero(X3) != X2
& c_Groups_Ozero__class_Ozero(X3) = X0 ) )
& ( ( ( c_Groups_Otimes__class_Otimes(X3,X2,X0) = X1
| c_Groups_Ozero__class_Ozero(X3) = X0 )
& ( X2 = c_Groups_Ozero__class_Ozero(X3)
| c_Groups_Ozero__class_Ozero(X3) != X0 ) )
| c_Rings_Oinverse__class_Odivide(X3,X1,X0) != X2 ) )
| ~ class_Fields_Ofield__inverse__zero(X3) ),
inference(flattening,[],[f2283]) ).
fof(f2397,plain,
! [X0,X1] :
( ( ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,X1,X0)
| ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,X0,c_Nat_OSuc(X1)) )
& ( c_Orderings_Oord__class_Oless(tc_Nat_Onat,X0,c_Nat_OSuc(X1))
| c_Orderings_Oord__class_Oless(tc_Nat_Onat,X1,X0) ) ),
inference(nnf_transformation,[],[f580]) ).
fof(f2428,plain,
! [X0] :
( ( c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),X0)
| ! [X1] : c_Nat_OSuc(X1) != X0 )
& ( ? [X1] : X0 = c_Nat_OSuc(X1)
| ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),X0) ) ),
inference(nnf_transformation,[],[f657]) ).
fof(f2429,plain,
! [X0] :
( ( c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),X0)
| ! [X1] : c_Nat_OSuc(X1) != X0 )
& ( ? [X2] : c_Nat_OSuc(X2) = X0
| ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),X0) ) ),
inference(rectify,[],[f2428]) ).
fof(f2430,plain,
! [X0] :
( ( c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),X0)
| ! [X1] : c_Nat_OSuc(X1) != X0 )
& ( c_Nat_OSuc(sK33(X0)) = X0
| ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK33]),skolemize(X2,sK33(X0))],[f2429]) ).
fof(f2437,plain,
! [X0,X1] :
( ( c_Orderings_Oord__class_Oless(tc_Nat_Onat,X1,X0)
| ! [X2] : c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X1,X2)) != X0 )
& ( ? [X2] : X0 = c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X1,X2))
| ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,X1,X0) ) ),
inference(nnf_transformation,[],[f663]) ).
fof(f2438,plain,
! [X0,X1] :
( ( c_Orderings_Oord__class_Oless(tc_Nat_Onat,X1,X0)
| ! [X2] : c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X1,X2)) != X0 )
& ( ? [X3] : c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X1,X3)) = X0
| ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,X1,X0) ) ),
inference(rectify,[],[f2437]) ).
fof(f2439,plain,
! [X0,X1] :
( ( c_Orderings_Oord__class_Oless(tc_Nat_Onat,X1,X0)
| ! [X2] : c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X1,X2)) != X0 )
& ( c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X1,sK34(X0,X1))) = X0
| ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,X1,X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK34]),skolemize(X3,sK34(X0,X1))],[f2438]) ).
fof(f2559,plain,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),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_RealDef_Oreal(tc_Nat_Onat,v_N2____)),
inference(cnf_transformation,[],[f1]) ).
fof(f2581,plain,
! [X0] : c_Groups_Oplus__class_Oplus(tc_Int_Oint,X0,c_Int_OPls) = X0,
inference(cnf_transformation,[],[f20]) ).
fof(f2582,plain,
! [X0] : c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OPls,X0) = X0,
inference(cnf_transformation,[],[f21]) ).
fof(f2584,plain,
! [X0] : c_Int_OBit0(X0) = c_Groups_Oplus__class_Oplus(tc_Int_Oint,X0,X0),
inference(cnf_transformation,[],[f23]) ).
fof(f2596,plain,
! [X0] : c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X0) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0),
inference(cnf_transformation,[],[f30]) ).
fof(f2677,plain,
! [X0] : c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(X0))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_RealDef_Oreal(tc_Nat_Onat,c_Nat_OSuc(X0))))),
inference(cnf_transformation,[],[f91]) ).
fof(f2706,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,[],[f115]) ).
fof(f2726,plain,
c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) = c_RealDef_Oreal(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
inference(cnf_transformation,[],[f131]) ).
fof(f2733,plain,
! [X0] : c_RealDef_Oreal(tc_Nat_Onat,c_Nat_OSuc(X0)) = c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,X0),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),
inference(cnf_transformation,[],[f138]) ).
fof(f2762,plain,
! [X0,X1] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,X1),c_RealDef_Oreal(tc_Nat_Onat,X0))
| ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,X1,X0) ),
inference(cnf_transformation,[],[f2167]) ).
fof(f2772,plain,
! [X0,X1] :
( c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) = c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,X0)
| c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X1) != X0 ),
inference(cnf_transformation,[],[f2170]) ).
fof(f2775,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,[],[f167]) ).
fof(f2787,plain,
! [X0] : c_Orderings_Oord__class_Oless__eq(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____(X0)))),
inference(cnf_transformation,[],[f177]) ).
fof(f2835,plain,
! [X0,X1] :
( X0 != X1
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X1,X0) ),
inference(cnf_transformation,[],[f2188]) ).
fof(f2857,plain,
! [X2,X3,X0,X1,X4] :
( c_Orderings_Oord__class_Oless(X4,c_Groups_Oplus__class_Oplus(X4,X3,X1),c_Groups_Oplus__class_Oplus(X4,X2,X0))
| ~ c_Orderings_Oord__class_Oless__eq(X4,X1,X0)
| ~ c_Orderings_Oord__class_Oless(X4,X3,X2)
| ~ class_Groups_Oordered__cancel__ab__semigroup__add(X4) ),
inference(cnf_transformation,[],[f1335]) ).
fof(f2906,plain,
! [X2,X3,X0,X1] :
( c_Orderings_Oord__class_Oless(X3,X1,c_Groups_Oplus__class_Oplus(X3,X2,X0))
| ~ c_Orderings_Oord__class_Oless(X3,X1,X0)
| ~ c_Orderings_Oord__class_Oless__eq(X3,c_Groups_Ozero__class_Ozero(X3),X2)
| ~ class_Groups_Oordered__comm__monoid__add(X3) ),
inference(cnf_transformation,[],[f1374]) ).
fof(f2925,plain,
! [X0] : c_Nat_OSuc(X0) = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X0,c_Groups_Oone__class_Oone(tc_Nat_Onat)),
inference(cnf_transformation,[],[f273]) ).
fof(f2940,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,[],[f280]) ).
fof(f3002,plain,
! [X2,X3,X0,X1,X4] :
( c_Orderings_Oord__class_Oless(X4,c_Groups_Oplus__class_Oplus(X4,X3,X1),c_Groups_Oplus__class_Oplus(X4,X2,X0))
| ~ c_Orderings_Oord__class_Oless(X4,X1,X0)
| ~ c_Orderings_Oord__class_Oless(X4,X3,X2)
| ~ class_Groups_Oordered__cancel__ab__semigroup__add(X4) ),
inference(cnf_transformation,[],[f1441]) ).
fof(f3007,plain,
! [X2,X3,X0,X1] :
( ~ c_Orderings_Oord__class_Oless(X3,c_Groups_Oplus__class_Oplus(X3,X2,X1),c_Groups_Oplus__class_Oplus(X3,X0,X1))
| c_Orderings_Oord__class_Oless(X3,X2,X0)
| ~ class_Groups_Oordered__ab__semigroup__add__imp__le(X3) ),
inference(cnf_transformation,[],[f2235]) ).
fof(f3027,plain,
! [X2,X0,X1] :
( ~ class_Groups_Ogroup__add(X2)
| c_Groups_Oplus__class_Oplus(X2,c_Groups_Ominus__class_Ominus(X2,X1,X0),X0) = X1 ),
inference(cnf_transformation,[],[f1460]) ).
fof(f3129,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,[],[f411]) ).
fof(f3171,plain,
! [X0] : c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),X0) = X0,
inference(cnf_transformation,[],[f445]) ).
fof(f3174,plain,
! [X0,X1] : c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X1,X0),c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X1,X1)) = c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X0,X1),
inference(cnf_transformation,[],[f447]) ).
fof(f3195,plain,
! [X2,X3,X0,X1] :
( c_Groups_Ozero__class_Ozero(X3) = X2
| c_Groups_Ozero__class_Ozero(X3) != X0
| c_Rings_Oinverse__class_Odivide(X3,X1,X0) != X2
| ~ class_Fields_Ofield__inverse__zero(X3) ),
inference(cnf_transformation,[],[f2284]) ).
fof(f3357,plain,
! [X0,X1] : c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X1,X0) = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X0,X1),
inference(cnf_transformation,[],[f534]) ).
fof(f3359,plain,
! [X2,X0,X1] : c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X2,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X1,X0)) = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X2,X1),X0),
inference(cnf_transformation,[],[f536]) ).
fof(f3494,plain,
! [X0,X1] :
( c_Groups_Oplus__class_Oplus(X1,X0,X0) = c_Groups_Otimes__class_Otimes(X1,X0,c_Int_Onumber__class_Onumber__of(X1,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))
| ~ class_Int_Onumber__ring(X1) ),
inference(cnf_transformation,[],[f1701]) ).
fof(f3510,plain,
! [X0] : ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,X0,c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
inference(cnf_transformation,[],[f579]) ).
fof(f3511,plain,
! [X0,X1] :
( c_Orderings_Oord__class_Oless(tc_Nat_Onat,X0,c_Nat_OSuc(X1))
| c_Orderings_Oord__class_Oless(tc_Nat_Onat,X1,X0) ),
inference(cnf_transformation,[],[f2397]) ).
fof(f3532,plain,
! [X0,X1] :
( c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X1,X0) != X1
| c_Groups_Ozero__class_Ozero(tc_Nat_Onat) = X0 ),
inference(cnf_transformation,[],[f1717]) ).
fof(f3535,plain,
! [X0] : c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),X0),
inference(cnf_transformation,[],[f596]) ).
fof(f3536,plain,
! [X0,X1] : c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X1,c_Nat_OSuc(X0)) = c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X1,X0)),
inference(cnf_transformation,[],[f597]) ).
fof(f3550,plain,
! [X0,X1] : ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X1,X0),X1),
inference(cnf_transformation,[],[f607]) ).
fof(f3551,plain,
! [X0,X1] : ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X1,X0),X0),
inference(cnf_transformation,[],[f608]) ).
fof(f3593,plain,
! [X0,X1] : c_Groups_Ominus__class_Ominus(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X1,X0),X0) = X1,
inference(cnf_transformation,[],[f641]) ).
fof(f3617,plain,
! [X0] :
( c_Nat_OSuc(sK33(X0)) = X0
| ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),X0) ),
inference(cnf_transformation,[],[f2430]) ).
fof(f3636,plain,
! [X0,X1] :
( c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X1,sK34(X0,X1))) = X0
| ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,X1,X0) ),
inference(cnf_transformation,[],[f2439]) ).
fof(f3658,plain,
! [X0,X1] :
( c_Orderings_Oord__class_Oless(tc_Nat_Onat,X1,X0)
| c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X0,c_Groups_Ominus__class_Ominus(tc_Nat_Onat,X1,X0)) = X1 ),
inference(cnf_transformation,[],[f1766]) ).
fof(f4023,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,[],[f2033]) ).
fof(f4166,plain,
class_Groups_Oordered__comm__monoid__add(tc_Nat_Onat),
inference(cnf_transformation,[],[f1056]) ).
fof(f4193,plain,
class_Groups_Oordered__cancel__ab__semigroup__add(tc_RealDef_Oreal),
inference(cnf_transformation,[],[f1083]) ).
fof(f4194,plain,
class_Groups_Oordered__ab__semigroup__add__imp__le(tc_RealDef_Oreal),
inference(cnf_transformation,[],[f1084]) ).
fof(f4219,plain,
class_Fields_Ofield__inverse__zero(tc_RealDef_Oreal),
inference(cnf_transformation,[],[f1109]) ).
fof(f4231,plain,
class_Rings_Ocomm__semiring__1(tc_RealDef_Oreal),
inference(cnf_transformation,[],[f1121]) ).
fof(f4243,plain,
class_Groups_Ogroup__add(tc_RealDef_Oreal),
inference(cnf_transformation,[],[f1133]) ).
fof(f4246,plain,
class_Int_Onumber__ring(tc_RealDef_Oreal),
inference(cnf_transformation,[],[f1136]) ).
fof(f4295,plain,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),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_RealDef_Oreal(tc_Nat_Onat,c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))),
inference(cnf_transformation,[],[f1189]) ).
fof(f4296,plain,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(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_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_RealDef_Oreal(tc_Nat_Onat,v_N2____)),
inference(definition_unfolding,[],[f2559,f2584,f2940]) ).
fof(f4357,plain,
! [X0] : c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(X0))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_RealDef_Oreal(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X0,c_Groups_Oone__class_Oone(tc_Nat_Onat)))))),
inference(definition_unfolding,[],[f2677,f2925]) ).
fof(f4371,plain,
! [X0] : c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,X0),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)) = c_RealDef_Oreal(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X0,c_Groups_Oone__class_Oone(tc_Nat_Onat))),
inference(definition_unfolding,[],[f2733,f2925]) ).
fof(f4452,plain,
! [X0,X1] :
( ~ class_Int_Onumber__ring(X1)
| c_Groups_Oplus__class_Oplus(X1,X0,X0) = c_Groups_Otimes__class_Otimes(X1,X0,c_Int_Onumber__class_Onumber__of(X1,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,[],[f3494,f2584,f2940]) ).
fof(f4464,plain,
! [X0,X1] :
( c_Orderings_Oord__class_Oless(tc_Nat_Onat,X0,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X1,c_Groups_Oone__class_Oone(tc_Nat_Onat)))
| c_Orderings_Oord__class_Oless(tc_Nat_Onat,X1,X0) ),
inference(definition_unfolding,[],[f3511,f2925]) ).
fof(f4479,plain,
! [X0,X1] : c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X1,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X0,c_Groups_Oone__class_Oone(tc_Nat_Onat))) = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X1,X0),c_Groups_Oone__class_Oone(tc_Nat_Onat)),
inference(definition_unfolding,[],[f3536,f2925,f2925]) ).
fof(f4503,plain,
! [X0] :
( ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),X0)
| c_Groups_Oplus__class_Oplus(tc_Nat_Onat,sK33(X0),c_Groups_Oone__class_Oone(tc_Nat_Onat)) = X0 ),
inference(definition_unfolding,[],[f3617,f2925]) ).
fof(f4519,plain,
! [X0,X1] :
( ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,X1,X0)
| c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X1,sK34(X0,X1)),c_Groups_Oone__class_Oone(tc_Nat_Onat)) = X0 ),
inference(definition_unfolding,[],[f3636,f2925]) ).
fof(f4582,plain,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(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_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_RealDef_Oreal(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____),c_Groups_Oone__class_Oone(tc_Nat_Onat)))),
inference(definition_unfolding,[],[f4295,f2584,f2940,f2925]) ).
fof(f4597,plain,
! [X1] : c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) = c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X1)),
inference(equality_resolution,[],[f2772]) ).
fof(f4600,plain,
! [X1] : ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X1,X1),
inference(equality_resolution,[],[f2835]) ).
fof(f4653,plain,
! [X2,X3,X1] :
( c_Groups_Ozero__class_Ozero(X3) = X2
| c_Rings_Oinverse__class_Odivide(X3,X1,c_Groups_Ozero__class_Ozero(X3)) != X2
| ~ class_Fields_Ofield__inverse__zero(X3) ),
inference(equality_resolution,[],[f3195]) ).
fof(f4654,plain,
! [X3,X1] :
( ~ class_Fields_Ofield__inverse__zero(X3)
| c_Groups_Ozero__class_Ozero(X3) = c_Rings_Oinverse__class_Odivide(X3,X1,c_Groups_Ozero__class_Ozero(X3)) ),
inference(equality_resolution,[],[f4653]) ).
fof(f4768,definition,
sF47 = c_Groups_Oone__class_Oone(tc_Int_Oint),
introduced(definition,[new_symbols(definition,[sF47])],[function_definition]) ).
fof(f4769,plain,
c_Groups_Oone__class_Oone(tc_Int_Oint) = sF47,
inference(reorient_equations,[],[f4768]) ).
fof(f4770,definition,
sF48 = c_Groups_Oplus__class_Oplus(tc_Int_Oint,sF47,c_Int_OPls),
introduced(definition,[new_symbols(definition,[sF48])],[function_definition]) ).
fof(f4771,plain,
c_Groups_Oplus__class_Oplus(tc_Int_Oint,sF47,c_Int_OPls) = sF48,
inference(reorient_equations,[],[f4770]) ).
fof(f4772,definition,
sF49 = c_Groups_Oplus__class_Oplus(tc_Int_Oint,sF48,c_Int_OPls),
introduced(definition,[new_symbols(definition,[sF49])],[function_definition]) ).
fof(f4773,plain,
c_Groups_Oplus__class_Oplus(tc_Int_Oint,sF48,c_Int_OPls) = sF49,
inference(reorient_equations,[],[f4772]) ).
fof(f4774,definition,
sF50 = c_Groups_Oplus__class_Oplus(tc_Int_Oint,sF49,sF49),
introduced(definition,[new_symbols(definition,[sF50])],[function_definition]) ).
fof(f4775,plain,
c_Groups_Oplus__class_Oplus(tc_Int_Oint,sF49,sF49) = sF50,
inference(reorient_equations,[],[f4774]) ).
fof(f4776,definition,
sF51 = c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,sF50),
introduced(definition,[new_symbols(definition,[sF51])],[function_definition]) ).
fof(f4777,plain,
c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,sF50) = sF51,
inference(reorient_equations,[],[f4776]) ).
fof(f4778,definition,
sF52 = c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____),
introduced(definition,[new_symbols(definition,[sF52])],[function_definition]) ).
fof(f4779,plain,
c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____) = sF52,
inference(reorient_equations,[],[f4778]) ).
fof(f4780,definition,
sF53 = c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,sF52),
introduced(definition,[new_symbols(definition,[sF53])],[function_definition]) ).
fof(f4781,plain,
c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,sF52) = sF53,
inference(reorient_equations,[],[f4780]) ).
fof(f4782,definition,
sF54 = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____),
introduced(definition,[new_symbols(definition,[sF54])],[function_definition]) ).
fof(f4783,plain,
c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____) = sF54,
inference(reorient_equations,[],[f4782]) ).
fof(f4784,definition,
sF55 = c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,sF53,sF54),
introduced(definition,[new_symbols(definition,[sF55])],[function_definition]) ).
fof(f4785,plain,
c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,sF53,sF54) = sF55,
inference(reorient_equations,[],[f4784]) ).
fof(f4786,definition,
sF56 = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,sF55),
introduced(definition,[new_symbols(definition,[sF56])],[function_definition]) ).
fof(f4787,plain,
c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,sF55) = sF56,
inference(reorient_equations,[],[f4786]) ).
fof(f4788,definition,
sF57 = c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,sF51,sF56),
introduced(definition,[new_symbols(definition,[sF57])],[function_definition]) ).
fof(f4789,plain,
c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,sF51,sF56) = sF57,
inference(reorient_equations,[],[f4788]) ).
fof(f4790,definition,
sF58 = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____),
introduced(definition,[new_symbols(definition,[sF58])],[function_definition]) ).
fof(f4791,plain,
c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____) = sF58,
inference(reorient_equations,[],[f4790]) ).
fof(f4792,definition,
sF59 = c_Groups_Oone__class_Oone(tc_Nat_Onat),
introduced(definition,[new_symbols(definition,[sF59])],[function_definition]) ).
fof(f4793,plain,
c_Groups_Oone__class_Oone(tc_Nat_Onat) = sF59,
inference(reorient_equations,[],[f4792]) ).
fof(f4794,definition,
sF60 = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,sF58,sF59),
introduced(definition,[new_symbols(definition,[sF60])],[function_definition]) ).
fof(f4795,plain,
c_Groups_Oplus__class_Oplus(tc_Nat_Onat,sF58,sF59) = sF60,
inference(reorient_equations,[],[f4794]) ).
fof(f4796,definition,
sF61 = c_RealDef_Oreal(tc_Nat_Onat,sF60),
introduced(definition,[new_symbols(definition,[sF61])],[function_definition]) ).
fof(f4797,plain,
c_RealDef_Oreal(tc_Nat_Onat,sF60) = sF61,
inference(reorient_equations,[],[f4796]) ).
fof(f4798,plain,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sF57,sF61),
inference(definition_folding,[],[f4582,f4797,f4795,f4793,f4791,f4789,f4787,f4785,f4783,f4781,f4779,f4777,f4775,f4773,f4771,f4769,f4773,f4771,f4769]) ).
fof(f4852,plain,
! [X1] : c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) = c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X1,X1),
inference(forward_demodulation,[],[f4597,f2775]) ).
fof(f4880,plain,
! [X0] : c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(X0))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,X0),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))))),
inference(forward_demodulation,[],[f4357,f4371]) ).
fof(f4923,plain,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(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_RealVector_Onorm__class_Onorm(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_RealDef_Oreal(tc_Nat_Onat,v_N2____)),
inference(forward_demodulation,[],[f4296,f2596]) ).
fof(f4924,plain,
sF47 = sF48,
inference(forward_demodulation,[],[f4771,f2581]) ).
fof(f4925,plain,
sF48 = sF49,
inference(forward_demodulation,[],[f4773,f2581]) ).
fof(f4926,plain,
sF56 = c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,sF55),
inference(forward_demodulation,[],[f4787,f2596]) ).
fof(f4946,plain,
! [X0] : c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(X0))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,sF54,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,X0),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))))),
inference(forward_demodulation,[],[f4880,f4783]) ).
fof(f4987,plain,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(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_RealVector_Onorm__class_Onorm(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____)),sF54))),c_RealDef_Oreal(tc_Nat_Onat,v_N2____)),
inference(forward_demodulation,[],[f4923,f4783]) ).
fof(f4988,plain,
sF47 = sF49,
inference(forward_demodulation,[],[f4925,f4924]) ).
fof(f5028,plain,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(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_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,sF52),sF54))),c_RealDef_Oreal(tc_Nat_Onat,v_N2____)),
inference(forward_demodulation,[],[f4987,f4779]) ).
fof(f5062,plain,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(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_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,sF53,sF54))),c_RealDef_Oreal(tc_Nat_Onat,v_N2____)),
inference(forward_demodulation,[],[f5028,f4781]) ).
fof(f5087,plain,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(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_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,sF55)),c_RealDef_Oreal(tc_Nat_Onat,v_N2____)),
inference(forward_demodulation,[],[f5062,f4785]) ).
fof(f5109,plain,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(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))),sF56),c_RealDef_Oreal(tc_Nat_Onat,v_N2____)),
inference(forward_demodulation,[],[f5087,f4926]) ).
fof(f5128,plain,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(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_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)))),sF56),c_RealDef_Oreal(tc_Nat_Onat,v_N2____)),
inference(forward_demodulation,[],[f5109,f2706]) ).
fof(f5147,plain,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(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_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))))),sF56),c_RealDef_Oreal(tc_Nat_Onat,v_N2____)),
inference(forward_demodulation,[],[f5128,f2706]) ).
fof(f5166,plain,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(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)))),sF56),c_RealDef_Oreal(tc_Nat_Onat,v_N2____)),
inference(forward_demodulation,[],[f5147,f2582]) ).
fof(f5185,plain,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(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))),sF56),c_RealDef_Oreal(tc_Nat_Onat,v_N2____)),
inference(forward_demodulation,[],[f5166,f2582]) ).
fof(f5201,plain,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(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_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OPls,c_Int_OPls)))),sF56),c_RealDef_Oreal(tc_Nat_Onat,v_N2____)),
inference(forward_demodulation,[],[f5185,f2706]) ).
fof(f5212,plain,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(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))),sF56),c_RealDef_Oreal(tc_Nat_Onat,v_N2____)),
inference(forward_demodulation,[],[f5201,f2581]) ).
fof(f5223,plain,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(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))),sF56),c_RealDef_Oreal(tc_Nat_Onat,v_N2____)),
inference(forward_demodulation,[],[f5212,f2581]) ).
fof(f5234,plain,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,sF47,sF47)),sF56),c_RealDef_Oreal(tc_Nat_Onat,v_N2____)),
inference(forward_demodulation,[],[f5223,f4769]) ).
fof(f5245,plain,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,sF49,sF49)),sF56),c_RealDef_Oreal(tc_Nat_Onat,v_N2____)),
inference(forward_demodulation,[],[f5234,f4988]) ).
fof(f5255,plain,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,sF50),sF56),c_RealDef_Oreal(tc_Nat_Onat,v_N2____)),
inference(forward_demodulation,[],[f5245,f4775]) ).
fof(f5264,plain,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,sF51,sF56),c_RealDef_Oreal(tc_Nat_Onat,v_N2____)),
inference(forward_demodulation,[],[f5255,f4777]) ).
fof(f5268,plain,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sF57,c_RealDef_Oreal(tc_Nat_Onat,v_N2____)),
inference(forward_demodulation,[],[f5264,f4789]) ).
fof(f5667,plain,
! [X0] : c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,X0),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)) = c_RealDef_Oreal(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X0,sF59)),
inference(superposition,[],[f4371,f4793]) ).
fof(f5759,definition,
( spl62_31
<=> ! [X0] :
( c_Orderings_Oord__class_Oless(tc_Nat_Onat,X0,sF60)
| ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,X0,sF59) ) ),
introduced(definition,[new_symbols(definition,[spl62_31])],[avatar_definition]) ).
fof(f5760,plain,
( ! [X0] :
( ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,X0,sF59)
| c_Orderings_Oord__class_Oless(tc_Nat_Onat,X0,sF60) )
| ~ spl62_31 ),
inference(avatar_component_clause,[],[f5759]) ).
fof(f5767,definition,
( spl62_33
<=> ! [X0] :
( c_Orderings_Oord__class_Oless(tc_Nat_Onat,X0,sF58)
| ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,X0,v_N2____) ) ),
introduced(definition,[new_symbols(definition,[spl62_33])],[avatar_definition]) ).
fof(f5768,plain,
( ! [X0] :
( ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,X0,v_N2____)
| c_Orderings_Oord__class_Oless(tc_Nat_Onat,X0,sF58) )
| ~ spl62_33 ),
inference(avatar_component_clause,[],[f5767]) ).
fof(f6059,plain,
! [X0,X1] : c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X0,X1),X1) = X0,
inference(resolution,[],[f4243,f3027]) ).
fof(f6077,plain,
! [X0] : c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),X0) = X0,
inference(superposition,[],[f6059,f4852]) ).
fof(f6091,plain,
! [X2,X0,X1] :
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X2,X1))
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X0,X1),X2)
| ~ class_Groups_Oordered__ab__semigroup__add__imp__le(tc_RealDef_Oreal) ),
inference(superposition,[],[f3007,f6059]) ).
fof(f6096,plain,
! [X2,X0,X1] :
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X2,X1))
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X0,X1),X2) ),
inference(forward_subsumption_resolution,[],[f6091,f4194]) ).
fof(f6669,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,[],[f4231,f4023]) ).
fof(f6725,plain,
! [X0] : c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)) = X0,
inference(superposition,[],[f6077,f6669]) ).
fof(f6784,plain,
! [X0] : c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X0,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)) = X0,
inference(superposition,[],[f6059,f6725]) ).
fof(f8374,plain,
! [X2,X3,X0,X1] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X2,X3),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X1))
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X3,X0)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X2,X1)
| ~ class_Groups_Oordered__cancel__ab__semigroup__add(tc_RealDef_Oreal) ),
inference(superposition,[],[f3002,f6669]) ).
fof(f8446,plain,
! [X2,X3,X0,X1] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X2,X3),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X1))
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X3,X0)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X2,X1) ),
inference(forward_subsumption_resolution,[],[f8374,f4193]) ).
fof(f11928,plain,
! [X0] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,X0),sF61)
| ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,X0,sF60) ),
inference(superposition,[],[f2762,f4797]) ).
fof(f13243,plain,
! [X0] : c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X0,c_Groups_Oone__class_Oone(tc_RealDef_Oreal)) = X0,
inference(superposition,[],[f3129,f3171]) ).
fof(f13259,plain,
! [X0] : c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),X0) = c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X0,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X0,X0)),
inference(superposition,[],[f3174,f13243]) ).
fof(f14577,plain,
! [X0] :
( c_Orderings_Oord__class_Oless(tc_Nat_Onat,X0,sF58)
| ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,X0,v_N2____)
| ~ c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),v_N1____)
| ~ class_Groups_Oordered__comm__monoid__add(tc_Nat_Onat) ),
inference(superposition,[],[f2906,f4791]) ).
fof(f14579,plain,
! [X0] :
( c_Orderings_Oord__class_Oless(tc_Nat_Onat,X0,sF60)
| ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,X0,sF59)
| ~ c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),sF58)
| ~ class_Groups_Oordered__comm__monoid__add(tc_Nat_Onat) ),
inference(superposition,[],[f2906,f4795]) ).
fof(f14592,plain,
! [X0] :
( c_Orderings_Oord__class_Oless(tc_Nat_Onat,X0,sF60)
| ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,X0,sF59)
| ~ class_Groups_Oordered__comm__monoid__add(tc_Nat_Onat) ),
inference(forward_subsumption_resolution,[],[f14579,f3535]) ).
fof(f14594,plain,
! [X0] :
( c_Orderings_Oord__class_Oless(tc_Nat_Onat,X0,sF58)
| ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,X0,v_N2____)
| ~ class_Groups_Oordered__comm__monoid__add(tc_Nat_Onat) ),
inference(forward_subsumption_resolution,[],[f14577,f3535]) ).
fof(f14638,plain,
! [X0] :
( c_Orderings_Oord__class_Oless(tc_Nat_Onat,X0,sF60)
| ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,X0,sF59) ),
inference(forward_subsumption_resolution,[],[f14592,f4166]) ).
fof(f14640,plain,
! [X0] :
( c_Orderings_Oord__class_Oless(tc_Nat_Onat,X0,sF58)
| ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,X0,v_N2____) ),
inference(forward_subsumption_resolution,[],[f14594,f4166]) ).
fof(f14687,plain,
spl62_31,
inference(avatar_split_clause,[],[f14638,f5759]) ).
fof(f14689,plain,
spl62_33,
inference(avatar_split_clause,[],[f14640,f5767]) ).
fof(f14727,plain,
( ! [X0] :
( c_Orderings_Oord__class_Oless(tc_Nat_Onat,X0,sF60)
| c_Groups_Oplus__class_Oplus(tc_Nat_Onat,sF59,c_Groups_Ominus__class_Ominus(tc_Nat_Onat,X0,sF59)) = X0 )
| ~ spl62_31 ),
inference(resolution,[],[f5760,f3658]) ).
fof(f14732,plain,
( ! [X0] :
( c_Orderings_Oord__class_Oless(tc_Nat_Onat,X0,sF58)
| c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N2____,c_Groups_Ominus__class_Ominus(tc_Nat_Onat,X0,v_N2____)) = X0 )
| ~ spl62_33 ),
inference(resolution,[],[f5768,f3658]) ).
fof(f15992,plain,
! [X2,X0,X1] :
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,X1)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X2,X0)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X2,X1)
| ~ class_Groups_Oordered__ab__semigroup__add__imp__le(tc_RealDef_Oreal) ),
inference(resolution,[],[f8446,f3007]) ).
fof(f16067,plain,
! [X2,X0,X1] :
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X2,X0)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,X1)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X2,X1) ),
inference(forward_subsumption_resolution,[],[f15992,f4194]) ).
fof(f16098,plain,
! [X0] :
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,v_N2____),X0)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sF57,X0) ),
inference(resolution,[],[f16067,f5268]) ).
fof(f16228,plain,
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sF57,sF61)
| ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,v_N2____,sF60) ),
inference(resolution,[],[f16098,f11928]) ).
fof(f16239,plain,
~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,v_N2____,sF60),
inference(forward_subsumption_resolution,[],[f16228,f4798]) ).
fof(f16309,plain,
v_N2____ = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,sF60,c_Groups_Ominus__class_Ominus(tc_Nat_Onat,v_N2____,sF60)),
inference(resolution,[],[f16239,f3658]) ).
fof(f16427,plain,
~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,v_N2____,c_Groups_Ominus__class_Ominus(tc_Nat_Onat,v_N2____,sF60)),
inference(superposition,[],[f3551,f16309]) ).
fof(f16429,plain,
sF60 = c_Groups_Ominus__class_Ominus(tc_Nat_Onat,v_N2____,c_Groups_Ominus__class_Ominus(tc_Nat_Onat,v_N2____,sF60)),
inference(superposition,[],[f3593,f16309]) ).
fof(f16471,plain,
v_N2____ = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Groups_Ominus__class_Ominus(tc_Nat_Onat,v_N2____,sF60),c_Groups_Ominus__class_Ominus(tc_Nat_Onat,v_N2____,c_Groups_Ominus__class_Ominus(tc_Nat_Onat,v_N2____,sF60))),
inference(resolution,[],[f16427,f3658]) ).
fof(f16472,plain,
v_N2____ = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Groups_Ominus__class_Ominus(tc_Nat_Onat,v_N2____,sF60),sF60),
inference(forward_demodulation,[],[f16471,f16429]) ).
fof(f21883,plain,
! [X0] : c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X0) = c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X0,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)))),
inference(resolution,[],[f4452,f4246]) ).
fof(f21886,plain,
! [X0] : c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X0) = c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X0,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_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(forward_demodulation,[],[f21883,f2706]) ).
fof(f21888,plain,
! [X0] : c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X0) = c_Groups_Otimes__class_Otimes(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_Oplus__class_Oplus(tc_Int_Oint,c_Int_OPls,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)))))),
inference(forward_demodulation,[],[f21886,f2706]) ).
fof(f21890,plain,
! [X0] : c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X0) = c_Groups_Otimes__class_Otimes(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_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))))),
inference(forward_demodulation,[],[f21888,f2582]) ).
fof(f21892,plain,
! [X0] : c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X0) = c_Groups_Otimes__class_Otimes(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_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,[],[f21890,f2582]) ).
fof(f21894,plain,
! [X0] : c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X0) = c_Groups_Otimes__class_Otimes(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_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_Int_OPls))))),
inference(forward_demodulation,[],[f21892,f2706]) ).
fof(f21896,plain,
! [X0] : c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X0) = c_Groups_Otimes__class_Otimes(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_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls)))),
inference(forward_demodulation,[],[f21894,f2581]) ).
fof(f21898,plain,
! [X0] : c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X0) = c_Groups_Otimes__class_Otimes(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(forward_demodulation,[],[f21896,f2581]) ).
fof(f21900,plain,
! [X0] : c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X0) = c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X0,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,sF47,sF47))),
inference(forward_demodulation,[],[f21898,f4769]) ).
fof(f21902,plain,
! [X0] : c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X0) = c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X0,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,sF49,sF49))),
inference(forward_demodulation,[],[f21900,f4988]) ).
fof(f21904,plain,
! [X0] : c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X0) = c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X0,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,sF50)),
inference(forward_demodulation,[],[f21902,f4775]) ).
fof(f21905,plain,
! [X0] : c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X0) = c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X0,sF51),
inference(forward_demodulation,[],[f21904,f4777]) ).
fof(f21976,plain,
c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) = c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),sF51),
inference(superposition,[],[f6077,f21905]) ).
fof(f22545,plain,
c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,sF51,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)) = c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))),
inference(superposition,[],[f3174,f21976]) ).
fof(f22552,plain,
c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,sF51,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)) = c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),
inference(forward_demodulation,[],[f22545,f13259]) ).
fof(f24627,plain,
( v_N2____ = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,sF59,c_Groups_Ominus__class_Ominus(tc_Nat_Onat,v_N2____,sF59))
| ~ spl62_31 ),
inference(resolution,[],[f14727,f16239]) ).
fof(f24893,plain,
( ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,v_N2____,c_Groups_Ominus__class_Ominus(tc_Nat_Onat,v_N2____,sF59))
| ~ spl62_31 ),
inference(superposition,[],[f3551,f24627]) ).
fof(f24895,plain,
( sF59 = c_Groups_Ominus__class_Ominus(tc_Nat_Onat,v_N2____,c_Groups_Ominus__class_Ominus(tc_Nat_Onat,v_N2____,sF59))
| ~ spl62_31 ),
inference(superposition,[],[f3593,f24627]) ).
fof(f24931,plain,
( v_N2____ = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Groups_Ominus__class_Ominus(tc_Nat_Onat,v_N2____,sF59),c_Groups_Ominus__class_Ominus(tc_Nat_Onat,v_N2____,c_Groups_Ominus__class_Ominus(tc_Nat_Onat,v_N2____,sF59)))
| ~ spl62_31 ),
inference(resolution,[],[f24893,f3658]) ).
fof(f24932,plain,
( v_N2____ = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Groups_Ominus__class_Ominus(tc_Nat_Onat,v_N2____,sF59),sF59)
| ~ spl62_31 ),
inference(forward_demodulation,[],[f24931,f24895]) ).
fof(f32466,plain,
! [X2,X3,X0,X1] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X2,X3),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X1))
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X3,X0)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X2,X1)
| ~ class_Groups_Oordered__cancel__ab__semigroup__add(tc_RealDef_Oreal) ),
inference(superposition,[],[f2857,f6669]) ).
fof(f32647,plain,
! [X2,X3,X0,X1] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X2,X3),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X1))
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X3,X0)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X2,X1) ),
inference(forward_subsumption_resolution,[],[f32466,f4193]) ).
fof(f35776,plain,
! [X0] : c_Groups_Oplus__class_Oplus(tc_Nat_Onat,sF58,X0) = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N2____,X0)),
inference(superposition,[],[f3359,f4791]) ).
fof(f35783,plain,
! [X0] : c_Groups_Oplus__class_Oplus(tc_Nat_Onat,sF60,X0) = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,sF58,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,sF59,X0)),
inference(superposition,[],[f3359,f4795]) ).
fof(f35806,plain,
! [X2,X0,X1] : c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X0,X1) = c_Groups_Ominus__class_Ominus(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X0,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X1,X2)),X2),
inference(superposition,[],[f3593,f3359]) ).
fof(f35990,plain,
! [X0] : c_Groups_Oplus__class_Oplus(tc_Nat_Onat,sF60,X0) = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,sF58,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X0,sF59)),
inference(superposition,[],[f35783,f3357]) ).
fof(f102222,plain,
! [X0,X1] :
( c_Orderings_Oord__class_Oless(tc_Nat_Onat,X0,X1)
| c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X0,c_Groups_Oone__class_Oone(tc_Nat_Onat)) = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X1,sK34(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X0,c_Groups_Oone__class_Oone(tc_Nat_Onat)),X1)),c_Groups_Oone__class_Oone(tc_Nat_Onat)) ),
inference(resolution,[],[f4464,f4519]) ).
fof(f102223,plain,
! [X0] :
( c_Orderings_Oord__class_Oless(tc_Nat_Onat,X0,c_Groups_Ozero__class_Ozero(tc_Nat_Onat))
| c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X0,c_Groups_Oone__class_Oone(tc_Nat_Onat)) = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,sK33(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X0,c_Groups_Oone__class_Oone(tc_Nat_Onat))),c_Groups_Oone__class_Oone(tc_Nat_Onat)) ),
inference(resolution,[],[f4464,f4503]) ).
fof(f102256,plain,
! [X0] : c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X0,c_Groups_Oone__class_Oone(tc_Nat_Onat)) = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,sK33(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X0,c_Groups_Oone__class_Oone(tc_Nat_Onat))),c_Groups_Oone__class_Oone(tc_Nat_Onat)),
inference(forward_subsumption_resolution,[],[f102223,f3510]) ).
fof(f102257,plain,
! [X0,X1] :
( c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X0,c_Groups_Oone__class_Oone(tc_Nat_Onat)) = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X1,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,sK34(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X0,c_Groups_Oone__class_Oone(tc_Nat_Onat)),X1),c_Groups_Oone__class_Oone(tc_Nat_Onat)))
| c_Orderings_Oord__class_Oless(tc_Nat_Onat,X0,X1) ),
inference(forward_demodulation,[],[f102222,f4479]) ).
fof(f102261,plain,
! [X0] : c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X0,sF59) = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,sK33(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X0,sF59)),sF59),
inference(forward_demodulation,[],[f102256,f4793]) ).
fof(f102262,plain,
! [X0,X1] :
( c_Orderings_Oord__class_Oless(tc_Nat_Onat,X0,X1)
| c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X0,sF59) = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X1,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,sK34(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X0,sF59),X1),sF59)) ),
inference(forward_demodulation,[],[f102257,f4793]) ).
fof(f102267,plain,
( v_N2____ = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,sK33(v_N2____),sF59)
| ~ spl62_31 ),
inference(superposition,[],[f102261,f24932]) ).
fof(f102547,plain,
( c_Groups_Ominus__class_Ominus(tc_Nat_Onat,v_N2____,sF59) = sK33(v_N2____)
| ~ spl62_31 ),
inference(superposition,[],[f3593,f102267]) ).
fof(f114436,plain,
! [X0] : c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) = c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X0,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),
inference(resolution,[],[f4654,f4219]) ).
fof(f137717,plain,
! [X0,X1] :
( ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X1)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X1,X0) ),
inference(resolution,[],[f32647,f4600]) ).
fof(f154457,plain,
! [X0] : c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,sF54,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(X0)))),
inference(superposition,[],[f2787,f4783]) ).
fof(f179977,plain,
! [X0] : c_Orderings_Oord__class_Oless(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____(X0))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,X0),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)))),sF54),
inference(resolution,[],[f6096,f4946]) ).
fof(f180265,plain,
! [X0] : c_Orderings_Oord__class_Oless(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____(X0))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_RealDef_Oreal(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X0,sF59)))),sF54),
inference(forward_demodulation,[],[f179977,f5667]) ).
fof(f198924,plain,
! [X0] : ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(X0))),sF54),
inference(resolution,[],[f137717,f154457]) ).
fof(f231134,plain,
! [X0] : c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X0,sF58) = c_Groups_Ominus__class_Ominus(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X0,sF60),sF59),
inference(superposition,[],[f35806,f4795]) ).
fof(f231302,plain,
c_Groups_Ominus__class_Ominus(tc_Nat_Onat,v_N2____,sF59) = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Groups_Ominus__class_Ominus(tc_Nat_Onat,v_N2____,sF60),sF58),
inference(superposition,[],[f231134,f16472]) ).
fof(f231340,plain,
( sK33(v_N2____) = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Groups_Ominus__class_Ominus(tc_Nat_Onat,v_N2____,sF60),sF58)
| ~ spl62_31 ),
inference(forward_demodulation,[],[f231302,f102547]) ).
fof(f231655,plain,
( ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,sK33(v_N2____),sF58)
| ~ spl62_31 ),
inference(superposition,[],[f3551,f231340]) ).
fof(f231750,plain,
( sK33(v_N2____) = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N2____,c_Groups_Ominus__class_Ominus(tc_Nat_Onat,sK33(v_N2____),v_N2____))
| ~ spl62_31
| ~ spl62_33 ),
inference(resolution,[],[f231655,f14732]) ).
fof(f231859,plain,
( ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,sK33(v_N2____),v_N2____)
| ~ spl62_31
| ~ spl62_33 ),
inference(superposition,[],[f3550,f231750]) ).
fof(f231937,plain,
( c_Groups_Oplus__class_Oplus(tc_Nat_Onat,sK33(v_N2____),sF59) = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N2____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,sK34(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,sK33(v_N2____),sF59),v_N2____),sF59))
| ~ spl62_31
| ~ spl62_33 ),
inference(resolution,[],[f231859,f102262]) ).
fof(f231941,plain,
( v_N2____ = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N2____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,sK34(v_N2____,v_N2____),sF59))
| ~ spl62_31
| ~ spl62_33 ),
inference(forward_demodulation,[],[f231937,f102267]) ).
fof(f231946,plain,
( c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____) = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,sF58,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,sK34(v_N2____,v_N2____),sF59))
| ~ spl62_31
| ~ spl62_33 ),
inference(superposition,[],[f35776,f231941]) ).
fof(f232027,plain,
( c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____) = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,sF60,sK34(v_N2____,v_N2____))
| ~ spl62_31
| ~ spl62_33 ),
inference(forward_demodulation,[],[f231946,f35990]) ).
fof(f232053,plain,
( sF58 = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,sF60,sK34(v_N2____,v_N2____))
| ~ spl62_31
| ~ spl62_33 ),
inference(forward_demodulation,[],[f232027,f4791]) ).
fof(f232072,plain,
( ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,sF58,sF60)
| ~ spl62_31
| ~ spl62_33 ),
inference(superposition,[],[f3550,f232053]) ).
fof(f232146,plain,
( c_Groups_Oplus__class_Oplus(tc_Nat_Onat,sF58,sF59) = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,sF60,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,sK34(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,sF58,sF59),sF60),sF59))
| ~ spl62_31
| ~ spl62_33 ),
inference(resolution,[],[f232072,f102262]) ).
fof(f232149,plain,
( sF60 = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,sF60,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,sK34(sF60,sF60),sF59))
| ~ spl62_31
| ~ spl62_33 ),
inference(forward_demodulation,[],[f232146,f4795]) ).
fof(f232161,plain,
( sF60 != sF60
| c_Groups_Ozero__class_Ozero(tc_Nat_Onat) = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,sK34(sF60,sF60),sF59)
| ~ spl62_31
| ~ spl62_33 ),
inference(superposition,[],[f3532,f232149]) ).
fof(f232204,plain,
( c_Groups_Ozero__class_Ozero(tc_Nat_Onat) = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,sK34(sF60,sF60),sF59)
| ~ spl62_31
| ~ spl62_33 ),
inference(trivial_inequality_removal,[],[f232161]) ).
fof(f232802,plain,
( c_Orderings_Oord__class_Oless(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____(sK34(sF60,sF60)))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_RealDef_Oreal(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))),sF54)
| ~ spl62_31
| ~ spl62_33 ),
inference(superposition,[],[f180265,f232204]) ).
fof(f232888,plain,
( c_Orderings_Oord__class_Oless(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____(sK34(sF60,sF60)))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))),sF54)
| ~ spl62_31
| ~ spl62_33 ),
inference(forward_demodulation,[],[f232802,f2726]) ).
fof(f232936,plain,
( c_Orderings_Oord__class_Oless(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____(sK34(sF60,sF60)))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,sF51,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))),sF54)
| ~ spl62_31
| ~ spl62_33 ),
inference(forward_demodulation,[],[f232888,f22552]) ).
fof(f232953,plain,
( c_Orderings_Oord__class_Oless(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____(sK34(sF60,sF60)))),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),sF54)
| ~ spl62_31
| ~ spl62_33 ),
inference(forward_demodulation,[],[f232936,f114436]) ).
fof(f232966,plain,
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_g____(sK34(sF60,sF60)))),sF54)
| ~ spl62_31
| ~ spl62_33 ),
inference(forward_demodulation,[],[f232953,f6784]) ).
fof(f232975,plain,
( $false
| ~ spl62_31
| ~ spl62_33 ),
inference(forward_subsumption_resolution,[],[f232966,f198924]) ).
fof(f232976,plain,
( ~ spl62_31
| ~ spl62_33 ),
inference(avatar_contradiction_clause,[],[f232975]) ).
cnf(s215,plain,
spl62_31,
inference(sat_conversion,[],[f14687]) ).
cnf(s216,plain,
spl62_33,
inference(sat_conversion,[],[f14689]) ).
cnf(s5158,plain,
( ~ spl62_31
| ~ spl62_33 ),
inference(sat_conversion,[],[f232976]) ).
cnf(s5211,plain,
~ spl62_31,
inference(rat,[],[s5158,s216]) ).
cnf(s5212,plain,
$false,
inference(rat,[],[s215,s5211]) ).
fof(f232982,plain,
$false,
inference(avatar_sat_refutation,[],[s5212]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW226+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.20 % Computer : n016.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:23:33 UTC 2026
% 0.08/0.20 % CPUTime :
% 0.08/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.24 Running first-order theorem proving
% 0.08/0.24 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 23.37/4.10 % (3619738)Detected formulas, will run a generic FOF schedule.
% 23.37/4.10 % (3619881)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=28173270:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 23.37/4.10 % (3619885)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1606706024:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 23.37/4.10 % (3619886)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3820169119:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 23.37/4.10 % (3619884)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3804699104:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 23.37/4.10 % (3619883)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=3053832554:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 23.37/4.10 % (3619887)dis-21_1_sil=8000:lcm=predicate:random_seed=1325898824:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 23.37/4.10 % (3619882)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=3506888273:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 23.37/4.10 % (3619884)Instruction limit reached!
% 23.37/4.10 % (3619884)------------------------------
% 23.37/4.10 % (3619884)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.37/4.10 % (3619884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.37/4.10 % (3619884)CaDiCaL version: 2.1.3
% 23.37/4.10 % (3619884)Termination reason: Instruction limit
% 23.37/4.10 % (3619884)Termination phase: Saturation
% 23.37/4.10 % (3619884)Time elapsed: 0.105 s
% 23.37/4.10 % (3619884)Peak memory usage: 90 MB
% 23.37/4.10 % (3619884)Instructions burned: 110 (million)
% 23.37/4.10 % (3619887)Instruction limit reached!
% 23.37/4.10 % (3619887)------------------------------
% 23.37/4.10 % (3619887)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.37/4.10 % (3619887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.37/4.10 % (3619887)CaDiCaL version: 2.1.3
% 23.37/4.10 % (3619887)Termination reason: Instruction limit
% 23.37/4.10 % (3619887)Termination phase: Saturation
% 23.37/4.10 % (3619887)Time elapsed: 0.111 s
% 23.37/4.10 % (3619887)Peak memory usage: 90 MB
% 23.37/4.10 % (3619887)Instructions burned: 130 (million)
% 23.37/4.10 % (3619885)Instruction limit reached!
% 23.37/4.10 % (3619885)------------------------------
% 23.37/4.10 % (3619885)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.37/4.10 % (3619885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.37/4.10 % (3619885)CaDiCaL version: 2.1.3
% 23.37/4.10 % (3619885)Termination reason: Instruction limit
% 23.37/4.10 % (3619885)Termination phase: Saturation
% 23.37/4.10 % (3619885)Time elapsed: 0.119 s
% 23.37/4.10 % (3619885)Peak memory usage: 90 MB
% 23.37/4.10 % (3619885)Instructions burned: 122 (million)
% 23.37/4.10 % (3619886)Instruction limit reached!
% 23.37/4.10 % (3619886)------------------------------
% 23.37/4.10 % (3619886)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.37/4.10 % (3619886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.37/4.10 % (3619886)CaDiCaL version: 2.1.3
% 23.37/4.10 % (3619886)Termination reason: Instruction limit
% 23.37/4.10 % (3619886)Termination phase: Saturation
% 23.37/4.10 % (3619886)Time elapsed: 0.136 s
% 23.37/4.10 % (3619886)Peak memory usage: 91 MB
% 23.37/4.10 % (3619886)Instructions burned: 139 (million)
% 23.37/4.10 % (3619903)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3183318097:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 23.37/4.10 % (3619901)lrs+10_1_sil=8000:sp=occurrence:random_seed=1004908473:i=285:sd=3:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/285Mi)
% 23.37/4.10 % (3619902)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3409461829:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/157Mi)
% 23.37/4.10 % (3619904)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=243371155:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 23.37/4.10 % (3619902)Instruction limit reached!
% 32.93/5.56 % (3619902)------------------------------
% 32.93/5.56 % (3619902)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.93/5.56 % (3619902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.93/5.56 % (3619902)CaDiCaL version: 2.1.3
% 32.93/5.56 % (3619902)Termination reason: Instruction limit
% 32.93/5.56 % (3619902)Termination phase: Saturation
% 32.93/5.56 % (3619902)Time elapsed: 0.155 s
% 32.93/5.56 % (3619902)Peak memory usage: 90 MB
% 32.93/5.56 % (3619902)Instructions burned: 157 (million)
% 32.93/5.56 % (3619903)Instruction limit reached!
% 32.93/5.56 % (3619903)------------------------------
% 32.93/5.56 % (3619903)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.93/5.56 % (3619903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.93/5.56 % (3619903)CaDiCaL version: 2.1.3
% 32.93/5.56 % (3619903)Termination reason: Instruction limit
% 32.93/5.56 % (3619903)Termination phase: Saturation
% 32.93/5.56 % (3619903)Time elapsed: 0.332 s
% 32.93/5.56 % (3619903)Peak memory usage: 92 MB
% 32.93/5.56 % (3619903)Instructions burned: 325 (million)
% 32.93/5.56 % (3619901)Instruction limit reached!
% 32.93/5.56 % (3619901)------------------------------
% 32.93/5.56 % (3619901)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.93/5.56 % (3619901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.93/5.56 % (3619901)CaDiCaL version: 2.1.3
% 32.93/5.56 % (3619901)Termination reason: Instruction limit
% 32.93/5.56 % (3619901)Termination phase: Saturation
% 32.93/5.56 % (3619901)Time elapsed: 0.283 s
% 32.93/5.56 % (3619901)Peak memory usage: 92 MB
% 32.93/5.56 % (3619901)Instructions burned: 285 (million)
% 32.93/5.56 % (3619904)Instruction limit reached!
% 32.93/5.56 % (3619904)------------------------------
% 32.93/5.56 % (3619904)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.93/5.56 % (3619904)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.93/5.56 % (3619904)CaDiCaL version: 2.1.3
% 32.93/5.56 % (3619904)Termination reason: Instruction limit
% 32.93/5.56 % (3619904)Termination phase: Saturation
% 32.93/5.56 % (3619904)Time elapsed: 0.248 s
% 32.93/5.56 % (3619904)Peak memory usage: 92 MB
% 32.93/5.56 % (3619904)Instructions burned: 248 (million)
% 32.93/5.56 % (3619915)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=783454878:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2991 on theBenchmark for (2991ds/294Mi)
% 32.93/5.56 % (3619918)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2742466569:i=2350_2990 on theBenchmark for (2990ds/2350Mi)
% 32.93/5.56 % (3619915)Instruction limit reached!
% 32.93/5.56 % (3619915)------------------------------
% 32.93/5.56 % (3619915)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.93/5.56 % (3619915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.93/5.56 % (3619915)CaDiCaL version: 2.1.3
% 32.93/5.56 % (3619915)Termination reason: Instruction limit
% 32.93/5.56 % (3619915)Termination phase: Saturation
% 32.93/5.56 % (3619915)Time elapsed: 0.180 s
% 32.93/5.56 % (3619915)Peak memory usage: 92 MB
% 32.93/5.56 % (3619915)Instructions burned: 294 (million)
% 32.93/5.56 % (3619919)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2720303781:cts=off:i=113:fsr=off:ss=included:sgt=4_2990 on theBenchmark for (2990ds/113Mi)
% 32.93/5.56 % (3619920)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=125959458:i=127:av=off:fsr=off:sup=off_2989 on theBenchmark for (2989ds/127Mi)
% 32.93/5.56 % (3619919)Instruction limit reached!
% 32.93/5.56 % (3619919)------------------------------
% 32.93/5.56 % (3619919)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.93/5.56 % (3619919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.93/5.56 % (3619919)CaDiCaL version: 2.1.3
% 32.93/5.56 % (3619919)Termination reason: Instruction limit
% 32.93/5.56 % (3619919)Termination phase: Saturation
% 32.93/5.56 % (3619919)Time elapsed: 0.102 s
% 32.93/5.56 % (3619919)Peak memory usage: 90 MB
% 32.93/5.56 % (3619919)Instructions burned: 114 (million)
% 32.93/5.56 % (3619920)Instruction limit reached!
% 32.93/5.56 % (3619920)------------------------------
% 32.93/5.56 % (3619920)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.93/5.56 % (3619920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.93/5.56 % (3619920)CaDiCaL version: 2.1.3
% 32.93/5.56 % (3619920)Termination reason: Instruction limit
% 32.93/5.56 % (3619920)Termination phase: Saturation
% 98.32/14.69 % (3619920)Time elapsed: 0.109 s
% 98.32/14.69 % (3619920)Peak memory usage: 90 MB
% 98.32/14.69 % (3619920)Instructions burned: 127 (million)
% 98.32/14.69 % (3619923)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2125291340:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2987 on theBenchmark for (2987ds/114Mi)
% 98.32/14.69 % (3619923)Instruction limit reached!
% 98.32/14.69 % (3619923)------------------------------
% 98.32/14.69 % (3619923)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 98.32/14.69 % (3619923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.32/14.69 % (3619923)CaDiCaL version: 2.1.3
% 98.32/14.69 % (3619923)Termination reason: Instruction limit
% 98.32/14.69 % (3619923)Termination phase: Saturation
% 98.32/14.69 % (3619923)Time elapsed: 0.100 s
% 98.32/14.69 % (3619923)Peak memory usage: 90 MB
% 98.32/14.69 % (3619923)Instructions burned: 114 (million)
% 98.32/14.69 % (3619928)lrs+10_1_sil=8000:sp=occurrence:random_seed=3926667704:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2986 on theBenchmark for (2986ds/907Mi)
% 98.32/14.69 % (3619930)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=680765358:i=437:sd=1:aac=none:ss=included_2985 on theBenchmark for (2985ds/437Mi)
% 98.32/14.69 % (3619935)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=219570857:i=5202:ss=axioms:sgt=16_2983 on theBenchmark for (2983ds/5202Mi)
% 98.32/14.69 % (3619930)Instruction limit reached!
% 98.32/14.69 % (3619930)------------------------------
% 98.32/14.69 % (3619930)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 98.32/14.69 % (3619930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.32/14.69 % (3619930)CaDiCaL version: 2.1.3
% 98.32/14.69 % (3619930)Termination reason: Instruction limit
% 98.32/14.69 % (3619930)Termination phase: Saturation
% 98.32/14.69 % (3619930)Time elapsed: 0.413 s
% 98.32/14.69 % (3619930)Peak memory usage: 94 MB
% 98.32/14.69 % (3619930)Instructions burned: 437 (million)
% 98.32/14.69 % (3619941)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3555134076:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2978 on theBenchmark for (2978ds/134Mi)
% 98.32/14.69 % (3619941)Instruction limit reached!
% 98.32/14.69 % (3619941)------------------------------
% 98.32/14.69 % (3619941)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 98.32/14.69 % (3619941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.32/14.69 % (3619941)CaDiCaL version: 2.1.3
% 98.32/14.69 % (3619941)Termination reason: Instruction limit
% 98.32/14.69 % (3619941)Termination phase: Saturation
% 98.32/14.69 % (3619941)Time elapsed: 0.074 s
% 98.32/14.69 % (3619941)Peak memory usage: 91 MB
% 98.32/14.69 % (3619941)Instructions burned: 135 (million)
% 98.32/14.69 % (3619928)Instruction limit reached!
% 98.32/14.69 % (3619928)------------------------------
% 98.32/14.69 % (3619928)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 98.32/14.69 % (3619928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.32/14.69 % (3619928)CaDiCaL version: 2.1.3
% 98.32/14.69 % (3619928)Termination reason: Instruction limit
% 98.32/14.69 % (3619928)Termination phase: Saturation
% 98.32/14.69 % (3619928)Time elapsed: 0.927 s
% 98.32/14.69 % (3619928)Peak memory usage: 98 MB
% 98.32/14.69 % (3619928)Instructions burned: 907 (million)
% 98.32/14.69 % (3619945)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3460960113:st=8:i=592:sd=3:ep=RST:ss=axioms_2976 on theBenchmark for (2976ds/592Mi)
% 98.32/14.69 % (3619946)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2769732017:st=3:i=13193:sd=3:ss=axioms_2974 on theBenchmark for (2974ds/13193Mi)
% 98.32/14.69 % (3619945)Instruction limit reached!
% 98.32/14.69 % (3619945)------------------------------
% 98.32/14.69 % (3619945)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 98.32/14.69 % (3619945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.32/14.69 % (3619945)CaDiCaL version: 2.1.3
% 98.32/14.69 % (3619945)Termination reason: Instruction limit
% 98.32/14.69 % (3619945)Termination phase: Saturation
% 98.32/14.69 % (3619945)Time elapsed: 0.517 s
% 98.32/14.69 % (3619945)Peak memory usage: 94 MB
% 98.32/14.69 % (3619945)Instructions burned: 592 (million)
% 98.32/14.69 % (3619951)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=4075152319:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2968 on theBenchmark for (2968ds/125Mi)
% 84.65/17.80 % (3619951)Instruction limit reached!
% 84.65/17.80 % (3619951)------------------------------
% 84.65/17.80 % (3619951)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.65/17.80 % (3619951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.65/17.80 % (3619951)CaDiCaL version: 2.1.3
% 84.65/17.80 % (3619951)Termination reason: Instruction limit
% 84.65/17.80 % (3619951)Termination phase: Saturation
% 84.65/17.80 % (3619951)Time elapsed: 0.131 s
% 84.65/17.80 % (3619951)Peak memory usage: 91 MB
% 84.65/17.80 % (3619951)Instructions burned: 126 (million)
% 84.65/17.80 % (3619918)Instruction limit reached!
% 84.65/17.80 % (3619918)------------------------------
% 84.65/17.80 % (3619918)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.65/17.80 % (3619918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.65/17.80 % (3619918)CaDiCaL version: 2.1.3
% 84.65/17.80 % (3619918)Termination reason: Instruction limit
% 84.65/17.80 % (3619918)Termination phase: Saturation
% 84.65/17.80 % (3619918)Time elapsed: 2.416 s
% 84.65/17.80 % (3619918)Peak memory usage: 147 MB
% 84.65/17.80 % (3619918)Instructions burned: 2350 (million)
% 84.65/17.80 % (3619955)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1272888136:i=134:gtgl=5:slsql=off:gtg=exists_sym_2964 on theBenchmark for (2964ds/134Mi)
% 84.65/17.80 % (3619955)Instruction limit reached!
% 84.65/17.80 % (3619955)------------------------------
% 84.65/17.80 % (3619955)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.65/17.80 % (3619955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.65/17.80 % (3619955)CaDiCaL version: 2.1.3
% 84.65/17.80 % (3619955)Termination reason: Instruction limit
% 84.65/17.80 % (3619955)Termination phase: Saturation
% 84.65/17.80 % (3619955)Time elapsed: 0.070 s
% 84.65/17.80 % (3619955)Peak memory usage: 90 MB
% 84.65/17.80 % (3619955)Instructions burned: 135 (million)
% 84.65/17.80 % (3619956)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=4182732240:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2963 on theBenchmark for (2963ds/141Mi)
% 84.65/17.80 % (3619956)Refutation not found, incomplete strategy
% 84.65/17.80 % (3619956)------------------------------
% 84.65/17.80 % (3619956)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.65/17.80 % (3619956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.65/17.80 % (3619956)CaDiCaL version: 2.1.3
% 84.65/17.80 % (3619956)Termination reason: Refutation not found, incomplete strategy
% 84.65/17.80 % (3619956)Time elapsed: 0.032 s
% 84.65/17.80 % (3619956)Peak memory usage: 89 MB
% 84.65/17.80 % (3619956)Instructions burned: 33 (million)
% 84.65/17.80 % (3619958)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1700076436:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2961 on theBenchmark for (2961ds/431Mi)
% 84.65/17.80 % (3619956)------------------------------
% 84.65/17.80 % (3619956)------------------------------
% 84.65/17.80 % (3619958)Instruction limit reached!
% 84.65/17.80 % (3619958)------------------------------
% 84.65/17.80 % (3619958)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.65/17.80 % (3619958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.65/17.80 % (3619958)CaDiCaL version: 2.1.3
% 84.65/17.80 % (3619958)Termination reason: Instruction limit
% 84.65/17.80 % (3619958)Termination phase: Saturation
% 84.65/17.80 % (3619958)Time elapsed: 0.374 s
% 84.65/17.80 % (3619958)Peak memory usage: 92 MB
% 84.65/17.80 % (3619958)Instructions burned: 432 (million)
% 84.65/17.80 % (3619963)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=2754045862:i=6060:aac=none:ins=25_2956 on theBenchmark for (2956ds/6060Mi)
% 84.65/17.80 % (3619964)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=4271772657:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2955 on theBenchmark for (2955ds/150Mi)
% 84.65/17.80 % (3619964)Instruction limit reached!
% 84.65/17.80 % (3619964)------------------------------
% 84.65/17.80 % (3619964)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.65/17.80 % (3619964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.65/17.80 % (3619964)CaDiCaL version: 2.1.3
% 84.65/17.80 % (3619964)Termination reason: Instruction limit
% 84.65/17.80 % (3619964)Termination phase: Saturation
% 84.65/17.80 % (3619964)Time elapsed: 0.142 s
% 84.65/17.80 % (3619964)Peak memory usage: 91 MB
% 84.65/17.80 % (3619964)Instructions burned: 151 (million)
% 84.65/17.80 % (3619969)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2299173873:i=14155:bd=all_2951 on theBenchmark for (2951ds/14155Mi)
% 84.65/17.80 % (3619935)Instruction limit reached!
% 84.65/17.80 % (3619935)------------------------------
% 84.65/17.80 % (3619935)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.65/17.80 % (3619935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.65/17.80 % (3619935)CaDiCaL version: 2.1.3
% 84.65/17.80 % (3619935)Termination reason: Instruction limit
% 84.65/17.80 % (3619935)Termination phase: Saturation
% 84.65/17.80 % (3619935)Time elapsed: 5.546 s
% 84.65/17.80 % (3619935)Peak memory usage: 167 MB
% 84.65/17.80 % (3619935)Instructions burned: 5202 (million)
% 84.65/17.80 % (3619973)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2203203324:i=667:av=off:fsr=off_2925 on theBenchmark for (2925ds/667Mi)
% 84.65/17.80 % (3619973)Instruction limit reached!
% 84.65/17.80 % (3619973)------------------------------
% 84.65/17.80 % (3619973)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.65/17.80 % (3619973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.65/17.80 % (3619973)CaDiCaL version: 2.1.3
% 84.65/17.80 % (3619973)Termination reason: Instruction limit
% 84.65/17.80 % (3619973)Termination phase: Saturation
% 84.65/17.80 % (3619973)Time elapsed: 0.540 s
% 84.65/17.80 % (3619973)Peak memory usage: 92 MB
% 84.65/17.80 % (3619973)Instructions burned: 668 (million)
% 84.65/17.80 % (3619975)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=3680274258:s2a=on:i=185:s2at=1.8:fdi=4_2916 on theBenchmark for (2916ds/185Mi)
% 84.65/17.80 % (3619975)Instruction limit reached!
% 84.65/17.80 % (3619975)------------------------------
% 84.65/17.80 % (3619975)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.65/17.80 % (3619975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.65/17.80 % (3619975)CaDiCaL version: 2.1.3
% 84.65/17.80 % (3619975)Termination reason: Instruction limit
% 84.65/17.80 % (3619975)Termination phase: Saturation
% 84.65/17.80 % (3619975)Time elapsed: 0.166 s
% 84.65/17.80 % (3619975)Peak memory usage: 92 MB
% 84.65/17.80 % (3619975)Instructions burned: 185 (million)
% 84.65/17.80 % (3619977)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=270287132:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2912 on theBenchmark for (2912ds/193Mi)
% 84.65/17.80 % (3619977)Instruction limit reached!
% 84.65/17.80 % (3619977)------------------------------
% 84.65/17.80 % (3619977)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.65/17.80 % (3619977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.65/17.80 % (3619977)CaDiCaL version: 2.1.3
% 84.65/17.80 % (3619977)Termination reason: Instruction limit
% 84.65/17.80 % (3619977)Termination phase: Saturation
% 84.65/17.80 % (3619977)Time elapsed: 0.169 s
% 84.65/17.80 % (3619977)Peak memory usage: 93 MB
% 84.65/17.80 % (3619977)Instructions burned: 193 (million)
% 84.65/17.80 % (3619979)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=1058168947:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2908 on theBenchmark for (2908ds/4850Mi)
% 84.65/17.80 % (3619963)Instruction limit reached!
% 84.65/17.80 % (3619963)------------------------------
% 84.65/17.80 % (3619963)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.65/17.80 % (3619963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.65/17.80 % (3619963)CaDiCaL version: 2.1.3
% 84.65/17.80 % (3619963)Termination reason: Instruction limit
% 84.65/17.80 % (3619963)Termination phase: Saturation
% 84.65/17.80 % (3619963)Time elapsed: 6.551 s
% 84.65/17.80 % (3619963)Peak memory usage: 178 MB
% 84.65/17.80 % (3619963)Instructions burned: 6061 (million)
% 84.65/17.80 % (3619987)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=697538860:i=12111:sd=1:ss=included_2887 on theBenchmark for (2887ds/12111Mi)
% 84.65/17.80 % (3619979)Instruction limit reached!
% 84.65/17.80 % (3619979)------------------------------
% 84.65/17.80 % (3619979)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.65/17.80 % (3619979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.65/17.80 % (3619979)CaDiCaL version: 2.1.3
% 84.65/17.80 % (3619979)Termination reason: Instruction limit
% 84.65/17.80 % (3619979)Termination phase: Saturation
% 84.65/17.80 % (3619979)Time elapsed: 4.543 s
% 84.65/17.80 % (3619979)Peak memory usage: 118 MB
% 84.65/17.80 % (3619979)Instructions burned: 4851 (million)
% 84.65/17.80 % (3619994)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=4204228456:i=319:kws=precedence:fsr=off_2860 on theBenchmark for (2860ds/319Mi)
% 84.65/17.80 % (3619994)Instruction limit reached!
% 84.65/17.80 % (3619994)------------------------------
% 84.65/17.80 % (3619994)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.65/17.80 % (3619994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.65/17.80 % (3619994)CaDiCaL version: 2.1.3
% 84.65/17.80 % (3619994)Termination reason: Instruction limit
% 84.65/17.80 % (3619994)Termination phase: Saturation
% 84.65/17.80 % (3619994)Time elapsed: 0.325 s
% 84.65/17.80 % (3619994)Peak memory usage: 94 MB
% 84.65/17.80 % (3619994)Instructions burned: 319 (million)
% 84.65/17.80 % (3619996)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=145070911:i=2064:ep=RST_2854 on theBenchmark for (2854ds/2064Mi)
% 84.65/17.80 % (3619996)Refutation not found, incomplete strategy
% 84.65/17.80 % (3619996)------------------------------
% 84.65/17.80 % (3619996)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.65/17.80 % (3619996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.65/17.80 % (3619996)CaDiCaL version: 2.1.3
% 84.65/17.80 % (3619996)Termination reason: Refutation not found, incomplete strategy
% 84.65/17.80 % (3619996)Time elapsed: 0.076 s
% 84.65/17.80 % (3619996)Peak memory usage: 91 MB
% 84.65/17.80 % (3619996)Instructions burned: 118 (million)
% 84.65/17.80 % (3619996)------------------------------
% 84.65/17.80 % (3619996)------------------------------
% 84.65/17.80 % (3619998)dis-1011_128_sil=32000:random_seed=865858538:i=3706:ep=RST:av=off_2848 on theBenchmark for (2848ds/3706Mi)
% 84.65/17.80 % (3619946)Instruction limit reached!
% 84.65/17.80 % (3619946)------------------------------
% 84.65/17.80 % (3619946)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.65/17.80 % (3619946)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.65/17.80 % (3619946)CaDiCaL version: 2.1.3
% 84.65/17.80 % (3619946)Termination reason: Instruction limit
% 84.65/17.80 % (3619946)Termination phase: Saturation
% 84.65/17.80 % (3619946)Time elapsed: 13.889 s
% 84.65/17.80 % (3619946)Peak memory usage: 222 MB
% 84.65/17.80 % (3619946)Instructions burned: 13193 (million)
% 84.65/17.80 % (3619881)First to succeed.
% 84.65/17.80 % (3619881)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3619738"
% 84.65/17.80 % (3619881)Refutation found. Thanks to Tanya!
% 84.65/17.80 % SZS status Theorem for theBenchmark
% 84.65/17.80 % SZS output start Proof for theBenchmark
% See solution above
% 121.19/18.10 % (3619881)------------------------------
% 121.19/18.10 % (3619881)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 121.19/18.10 % (3619881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.19/18.10 % (3619881)CaDiCaL version: 2.1.3
% 121.19/18.10 % (3619881)Termination reason: Refutation
% 121.19/18.10 % (3619881)Time elapsed: 16.437 s
% 121.19/18.10 % (3619881)Peak memory usage: 340 MB
% 121.19/18.10 % (3619881)Instructions burned: 27720 (million)
% 121.19/18.10 % (3619881)------------------------------
% 121.19/18.10 % (3619881)------------------------------
% 121.19/18.10 % (3619738)Success in time 17.077 s
% 121.19/18.10 % Vampire exiting
%------------------------------------------------------------------------------