%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWW227+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:39:40 PM UTC 2026
% Result : Theorem 23.58s 3.60s
% Output : Refutation 23.58s
% Verified :
% SZS Type : Refutation
% Derivation depth : 35
% Number of leaves : 27
% Syntax : Number of formulae : 120 ( 65 unt; 1 def)
% Number of atoms : 213 ( 30 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 198 ( 105 ~; 75 |; 2 &)
% ( 10 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 8 ( 6 usr; 2 prp; 0-3 aty)
% Number of functors : 26 ( 26 usr; 10 con; 0-3 aty)
% Number of variables : 102 ( 0 sgn 102 !; 0 ?)
% 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,c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact__0962_A_P_Aabs_A_Icmod_A_Ipoly_Ap_Az_J_A_N_A_N_As_J_A_060_Areal_A_ISuc_A_IN1_A_L_AN2_J_J_096) ).
fof(f4,axiom,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_e) ).
fof(f20,axiom,
! [X0] : c_Int_OBit1(X0) = c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),X0),X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_Bit1__def) ).
fof(f24,axiom,
! [X0,X1] :
( c_Orderings_Oord__class_Oless(tc_Int_Oint,X1,c_Groups_Oplus__class_Oplus(tc_Int_Oint,X0,c_Groups_Oone__class_Oone(tc_Int_Oint)))
<=> ( c_Orderings_Oord__class_Oless(tc_Int_Oint,X1,X0)
| X1 = X0 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_zless__add1__eq) ).
fof(f25,axiom,
! [X0,X1,X2] : c_Groups_Oplus__class_Oplus(tc_Int_Oint,X2,c_Groups_Oplus__class_Oplus(tc_Int_Oint,X1,X0)) = c_Groups_Oplus__class_Oplus(tc_Int_Oint,X1,c_Groups_Oplus__class_Oplus(tc_Int_Oint,X2,X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_zadd__left__commute) ).
fof(f29,axiom,
! [X0,X1,X2] : c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,X2,X1),X0) = c_Groups_Oplus__class_Oplus(tc_Int_Oint,X2,c_Groups_Oplus__class_Oplus(tc_Int_Oint,X1,X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_zadd__assoc) ).
fof(f32,axiom,
! [X0] : c_Groups_Oplus__class_Oplus(tc_Int_Oint,X0,c_Int_OPls) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_add__Pls__right) ).
fof(f33,axiom,
! [X0] : c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OPls,X0) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_add__Pls) ).
fof(f35,axiom,
! [X0] : c_Int_OBit0(X0) = c_Groups_Oplus__class_Oplus(tc_Int_Oint,X0,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_Bit0__def) ).
fof(f42,axiom,
! [X0] : c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X0) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_real__norm__def) ).
fof(f59,axiom,
! [X0,X1] :
( ( class_Int_Onumber__ring(X1)
& class_Rings_Olinordered__idom(X1) )
=> ( c_Orderings_Oord__class_Oless(X1,c_Groups_Ozero__class_Ozero(X1),c_Int_Onumber__class_Onumber__of(X1,X0))
<=> c_Orderings_Oord__class_Oless(tc_Int_Oint,c_Int_OPls,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_less__special_I1_J) ).
fof(f149,axiom,
c_Int_OPls = c_Groups_Ozero__class_Ozero(tc_Int_Oint),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_Pls__def) ).
fof(f207,axiom,
! [X0] : c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealDef_Oreal(tc_Nat_Onat,c_Nat_OSuc(X0))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_real__of__nat__Suc__gt__zero) ).
fof(f210,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/sandbox/benchmark/theBenchmark.p',fact_real__of__nat__Suc) ).
fof(f232,axiom,
! [X0,X1] : c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X1,X0) = c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X0,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_real__mult__commute) ).
fof(f265,axiom,
! [X0,X1] :
( c_Orderings_Oord__class_Oless(tc_Int_Oint,X1,X0)
<=> ( c_Orderings_Oord__class_Oless__eq(tc_Int_Oint,X1,X0)
& X1 != X0 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_zless__le) ).
fof(f267,axiom,
! [X0] : c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),X0) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_real__mult__1) ).
fof(f287,axiom,
! [X0] :
( c_Orderings_Oord__class_Oless__eq(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),X0)
<=> c_Orderings_Oord__class_Oless(tc_Int_Oint,c_Groups_Ozero__class_Ozero(tc_Int_Oint),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_int__one__le__iff__zero__less) ).
fof(f291,axiom,
! [X0,X1] : c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X1,X0) = c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X1,c_Rings_Oinverse__class_Oinverse(tc_RealDef_Oreal,X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_real__divide__def) ).
fof(f579,axiom,
! [X0] : c_Nat_OSuc(X0) = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Groups_Oone__class_Oone(tc_Nat_Onat),X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_Suc__eq__plus1__left) ).
fof(f593,axiom,
! [X0,X1,X2,X3] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),X3)
=> ( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),X2)
=> ( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X2,X1),c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X3,X0))
=> c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X1,c_Rings_Oinverse__class_Oinverse(tc_RealDef_Oreal,X3)),c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X0,c_Rings_Oinverse__class_Oinverse(tc_RealDef_Oreal,X2))) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_real__mult__inverse__cancel2) ).
fof(f810,axiom,
! [X0,X1,X2,X3] :
( class_Fields_Olinordered__field(X3)
=> ( c_Orderings_Oord__class_Oless(X3,c_Groups_Ozero__class_Ozero(X3),X2)
=> ( c_Orderings_Oord__class_Oless(X3,c_Rings_Oinverse__class_Odivide(X3,X1,X2),X0)
<=> c_Orderings_Oord__class_Oless(X3,X1,c_Groups_Otimes__class_Otimes(X3,X0,X2)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_pos__divide__less__eq) ).
fof(f1105,axiom,
class_Fields_Olinordered__field(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_RealDef__Oreal__Fields_Olinordered__field) ).
fof(f1111,axiom,
class_Rings_Olinordered__idom(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_RealDef__Oreal__Rings_Olinordered__idom) ).
fof(f1125,axiom,
class_Int_Onumber__ring(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_RealDef__Oreal__Int_Onumber__ring) ).
fof(f1171,conjecture,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,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(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
fof(f1172,negated_conjecture,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,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(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))),
inference(negated_conjecture,[status(cth)],[f1171]) ).
fof(f1175,plain,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,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(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))),
inference(flattening,[],[f1172]) ).
fof(f1210,plain,
! [X0,X1] :
( ( c_Orderings_Oord__class_Oless(X1,c_Groups_Ozero__class_Ozero(X1),c_Int_Onumber__class_Onumber__of(X1,X0))
<=> c_Orderings_Oord__class_Oless(tc_Int_Oint,c_Int_OPls,X0) )
| ~ class_Int_Onumber__ring(X1)
| ~ class_Rings_Olinordered__idom(X1) ),
inference(ennf_transformation,[],[f59]) ).
fof(f1211,plain,
! [X0,X1] :
( ( c_Orderings_Oord__class_Oless(X1,c_Groups_Ozero__class_Ozero(X1),c_Int_Onumber__class_Onumber__of(X1,X0))
<=> c_Orderings_Oord__class_Oless(tc_Int_Oint,c_Int_OPls,X0) )
| ~ class_Int_Onumber__ring(X1)
| ~ class_Rings_Olinordered__idom(X1) ),
inference(flattening,[],[f1210]) ).
fof(f1555,plain,
! [X0,X1,X2,X3] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X1,c_Rings_Oinverse__class_Oinverse(tc_RealDef_Oreal,X3)),c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X0,c_Rings_Oinverse__class_Oinverse(tc_RealDef_Oreal,X2)))
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X2,X1),c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X3,X0))
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),X2)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),X3) ),
inference(ennf_transformation,[],[f593]) ).
fof(f1556,plain,
! [X0,X1,X2,X3] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X1,c_Rings_Oinverse__class_Oinverse(tc_RealDef_Oreal,X3)),c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X0,c_Rings_Oinverse__class_Oinverse(tc_RealDef_Oreal,X2)))
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X2,X1),c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X3,X0))
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),X2)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),X3) ),
inference(flattening,[],[f1555]) ).
fof(f1869,plain,
! [X0,X1,X2,X3] :
( ( c_Orderings_Oord__class_Oless(X3,c_Rings_Oinverse__class_Odivide(X3,X1,X2),X0)
<=> c_Orderings_Oord__class_Oless(X3,X1,c_Groups_Otimes__class_Otimes(X3,X0,X2)) )
| ~ c_Orderings_Oord__class_Oless(X3,c_Groups_Ozero__class_Ozero(X3),X2)
| ~ class_Fields_Olinordered__field(X3) ),
inference(ennf_transformation,[],[f810]) ).
fof(f1870,plain,
! [X0,X1,X2,X3] :
( ( c_Orderings_Oord__class_Oless(X3,c_Rings_Oinverse__class_Odivide(X3,X1,X2),X0)
<=> c_Orderings_Oord__class_Oless(X3,X1,c_Groups_Otimes__class_Otimes(X3,X0,X2)) )
| ~ c_Orderings_Oord__class_Oless(X3,c_Groups_Ozero__class_Ozero(X3),X2)
| ~ class_Fields_Olinordered__field(X3) ),
inference(flattening,[],[f1869]) ).
fof(f2125,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,[],[f1]) ).
fof(f2128,plain,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____)))),
inference(cnf_transformation,[],[f4]) ).
fof(f2146,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,[],[f20]) ).
fof(f2151,plain,
! [X0,X1] :
( X0 != X1
| c_Orderings_Oord__class_Oless(tc_Int_Oint,X1,c_Groups_Oplus__class_Oplus(tc_Int_Oint,X0,c_Groups_Oone__class_Oone(tc_Int_Oint))) ),
inference(cnf_transformation,[],[f24]) ).
fof(f2153,plain,
! [X2,X0,X1] : c_Groups_Oplus__class_Oplus(tc_Int_Oint,X2,c_Groups_Oplus__class_Oplus(tc_Int_Oint,X1,X0)) = c_Groups_Oplus__class_Oplus(tc_Int_Oint,X1,c_Groups_Oplus__class_Oplus(tc_Int_Oint,X2,X0)),
inference(cnf_transformation,[],[f25]) ).
fof(f2159,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,[],[f29]) ).
fof(f2162,plain,
! [X0] : c_Groups_Oplus__class_Oplus(tc_Int_Oint,X0,c_Int_OPls) = X0,
inference(cnf_transformation,[],[f32]) ).
fof(f2163,plain,
! [X0] : c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OPls,X0) = X0,
inference(cnf_transformation,[],[f33]) ).
fof(f2165,plain,
! [X0] : c_Int_OBit0(X0) = c_Groups_Oplus__class_Oplus(tc_Int_Oint,X0,X0),
inference(cnf_transformation,[],[f35]) ).
fof(f2177,plain,
! [X0] : c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X0) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0),
inference(cnf_transformation,[],[f42]) ).
fof(f2202,plain,
! [X0,X1] :
( c_Orderings_Oord__class_Oless(X1,c_Groups_Ozero__class_Ozero(X1),c_Int_Onumber__class_Onumber__of(X1,X0))
| ~ class_Int_Onumber__ring(X1)
| ~ c_Orderings_Oord__class_Oless(tc_Int_Oint,c_Int_OPls,X0)
| ~ class_Rings_Olinordered__idom(X1) ),
inference(cnf_transformation,[],[f1211]) ).
fof(f2310,plain,
c_Int_OPls = c_Groups_Ozero__class_Ozero(tc_Int_Oint),
inference(cnf_transformation,[],[f149]) ).
fof(f2397,plain,
! [X0] : c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealDef_Oreal(tc_Nat_Onat,c_Nat_OSuc(X0))),
inference(cnf_transformation,[],[f207]) ).
fof(f2402,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,[],[f210]) ).
fof(f2435,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,[],[f232]) ).
fof(f2479,plain,
! [X0,X1] :
( c_Orderings_Oord__class_Oless__eq(tc_Int_Oint,X1,X0)
| ~ c_Orderings_Oord__class_Oless(tc_Int_Oint,X1,X0) ),
inference(cnf_transformation,[],[f265]) ).
fof(f2482,plain,
! [X0] : c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),X0) = X0,
inference(cnf_transformation,[],[f267]) ).
fof(f2513,plain,
! [X0] :
( c_Orderings_Oord__class_Oless(tc_Int_Oint,c_Groups_Ozero__class_Ozero(tc_Int_Oint),X0)
| ~ c_Orderings_Oord__class_Oless__eq(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),X0) ),
inference(cnf_transformation,[],[f287]) ).
fof(f2517,plain,
! [X0,X1] : c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X1,X0) = c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X1,c_Rings_Oinverse__class_Oinverse(tc_RealDef_Oreal,X0)),
inference(cnf_transformation,[],[f291]) ).
fof(f3021,plain,
! [X0] : c_Nat_OSuc(X0) = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Groups_Oone__class_Oone(tc_Nat_Onat),X0),
inference(cnf_transformation,[],[f579]) ).
fof(f3042,plain,
! [X2,X3,X0,X1] :
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),X3)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),X2)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X2,X1),c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X3,X0))
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X1,c_Rings_Oinverse__class_Oinverse(tc_RealDef_Oreal,X3)),c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X0,c_Rings_Oinverse__class_Oinverse(tc_RealDef_Oreal,X2))) ),
inference(cnf_transformation,[],[f1556]) ).
fof(f3383,plain,
! [X2,X3,X0,X1] :
( c_Orderings_Oord__class_Oless(X3,X1,c_Groups_Otimes__class_Otimes(X3,X0,X2))
| ~ c_Orderings_Oord__class_Oless(X3,c_Groups_Ozero__class_Ozero(X3),X2)
| ~ class_Fields_Olinordered__field(X3)
| ~ c_Orderings_Oord__class_Oless(X3,c_Rings_Oinverse__class_Odivide(X3,X1,X2),X0) ),
inference(cnf_transformation,[],[f1870]) ).
fof(f3751,plain,
class_Fields_Olinordered__field(tc_RealDef_Oreal),
inference(cnf_transformation,[],[f1105]) ).
fof(f3757,plain,
class_Rings_Olinordered__idom(tc_RealDef_Oreal),
inference(cnf_transformation,[],[f1111]) ).
fof(f3771,plain,
class_Int_Onumber__ring(tc_RealDef_Oreal),
inference(cnf_transformation,[],[f1125]) ).
fof(f3817,plain,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,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(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))),
inference(cnf_transformation,[],[f1175]) ).
fof(f3818,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_Oone__class_Oone(tc_Nat_Onat),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))),
inference(definition_unfolding,[],[f2125,f2165,f2146,f3021]) ).
fof(f3907,plain,
! [X0] : c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealDef_Oreal(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Groups_Oone__class_Oone(tc_Nat_Onat),X0))),
inference(definition_unfolding,[],[f2397,f3021]) ).
fof(f3908,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,c_Groups_Oone__class_Oone(tc_Nat_Onat),X0)),
inference(definition_unfolding,[],[f2402,f3021]) ).
fof(f4096,plain,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,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,c_Groups_Oone__class_Oone(tc_Nat_Onat),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls))))),
inference(definition_unfolding,[],[f3817,f3021,f2165,f2146]) ).
fof(f4097,plain,
! [X1] : c_Orderings_Oord__class_Oless(tc_Int_Oint,X1,c_Groups_Oplus__class_Oplus(tc_Int_Oint,X1,c_Groups_Oone__class_Oone(tc_Int_Oint))),
inference(equality_resolution,[],[f2151]) ).
fof(f4693,plain,
! [X0] :
( ~ c_Orderings_Oord__class_Oless__eq(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),X0)
| c_Orderings_Oord__class_Oless(tc_Int_Oint,c_Int_OPls,X0) ),
inference(forward_demodulation,[],[f2513,f2310]) ).
fof(f4696,plain,
! [X0] :
( ~ c_Orderings_Oord__class_Oless(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),X0)
| c_Orderings_Oord__class_Oless(tc_Int_Oint,c_Int_OPls,X0) ),
inference(resolution,[],[f4693,f2479]) ).
fof(f4707,plain,
c_Orderings_Oord__class_Oless(tc_Int_Oint,c_Int_OPls,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oone__class_Oone(tc_Int_Oint))),
inference(resolution,[],[f4696,f4097]) ).
fof(f16582,plain,
! [X0] : c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(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,[],[f3907,f3908]) ).
fof(f20327,plain,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____)))),
inference(forward_demodulation,[],[f2128,f2177]) ).
fof(f77979,plain,
! [X2,X3,X0,X1] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X1,c_Rings_Oinverse__class_Oinverse(tc_RealDef_Oreal,X3)),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X0,X2))
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),X3)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),X2)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X2,X1),c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X3,X0)) ),
inference(forward_demodulation,[],[f3042,f2517]) ).
fof(f77980,plain,
! [X2,X3,X0,X1] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X1,X3),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,X0,X2))
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),X3)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),X2)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X2,X1),c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X3,X0)) ),
inference(forward_demodulation,[],[f77979,f2517]) ).
fof(f77989,plain,
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealDef_Oreal(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Groups_Oone__class_Oone(tc_Nat_Onat),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))))
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(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_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls))),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Groups_Oone__class_Oone(tc_Nat_Onat),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))),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____))))) ),
inference(resolution,[],[f77980,f4096]) ).
fof(f78014,plain,
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)))
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(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_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls))),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Groups_Oone__class_Oone(tc_Nat_Onat),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))),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____))))) ),
inference(forward_demodulation,[],[f77989,f3908]) ).
fof(f78019,plain,
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(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_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls))),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Groups_Oone__class_Oone(tc_Nat_Onat),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))),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____))))) ),
inference(forward_subsumption_resolution,[],[f78014,f16582]) ).
fof(f78022,plain,
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls),c_Int_OPls))))
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls))),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Groups_Oone__class_Oone(tc_Nat_Onat),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))),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____))))) ),
inference(forward_demodulation,[],[f78019,f2153]) ).
fof(f78025,plain,
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OPls,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls),c_Int_OPls)))))
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls))),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Groups_Oone__class_Oone(tc_Nat_Onat),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))),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____))))) ),
inference(forward_demodulation,[],[f78022,f2159]) ).
fof(f78028,plain,
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OPls,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls),c_Int_OPls)))))
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls))),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Groups_Oone__class_Oone(tc_Nat_Onat),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))),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____))))) ),
inference(forward_demodulation,[],[f78025,f2153]) ).
fof(f78030,plain,
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls),c_Int_OPls))))
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls))),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Groups_Oone__class_Oone(tc_Nat_Onat),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))),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____))))) ),
inference(forward_demodulation,[],[f78028,f2163]) ).
fof(f78031,plain,
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls))))
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls))),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Groups_Oone__class_Oone(tc_Nat_Onat),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))),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____))))) ),
inference(forward_demodulation,[],[f78030,f2162]) ).
fof(f78032,plain,
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls))))
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls))),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Groups_Oone__class_Oone(tc_Nat_Onat),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))),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____))))) ),
inference(forward_demodulation,[],[f78031,f2162]) ).
fof(f78033,plain,
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oone__class_Oone(tc_Int_Oint))))
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls))),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Groups_Oone__class_Oone(tc_Nat_Onat),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))),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____))))) ),
inference(forward_demodulation,[],[f78032,f2162]) ).
fof(f78034,plain,
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls))),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Groups_Oone__class_Oone(tc_Nat_Onat),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))),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_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(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)))) ),
inference(forward_demodulation,[],[f78033,f2177]) ).
fof(f78035,plain,
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls))),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____)))))
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(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)))) ),
inference(forward_demodulation,[],[f78034,f3908]) ).
fof(f78036,plain,
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_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_Otimes__class_Otimes(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____)))))
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(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)))) ),
inference(forward_demodulation,[],[f78035,f2435]) ).
fof(f78037,plain,
( ~ c_Orderings_Oord__class_Oless(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_Otimes__class_Otimes(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____)))))
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(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)))) ),
inference(forward_demodulation,[],[f78036,f2482]) ).
fof(f78038,plain,
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls),c_Int_OPls))),c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____)))))
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(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)))) ),
inference(forward_demodulation,[],[f78037,f2153]) ).
fof(f78039,plain,
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OPls,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls),c_Int_OPls)))),c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____)))))
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(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)))) ),
inference(forward_demodulation,[],[f78038,f2159]) ).
fof(f78040,plain,
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OPls,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls),c_Int_OPls)))),c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____)))))
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(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)))) ),
inference(forward_demodulation,[],[f78039,f2153]) ).
fof(f78041,plain,
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls),c_Int_OPls))),c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____)))))
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(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)))) ),
inference(forward_demodulation,[],[f78040,f2163]) ).
fof(f78042,plain,
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls))),c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____)))))
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(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)))) ),
inference(forward_demodulation,[],[f78041,f2162]) ).
fof(f78043,plain,
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls))),c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____)))))
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(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)))) ),
inference(forward_demodulation,[],[f78042,f2162]) ).
fof(f78044,plain,
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oone__class_Oone(tc_Int_Oint))),c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____)))))
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(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)))) ),
inference(forward_demodulation,[],[f78043,f2162]) ).
fof(f81565,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_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))),
inference(forward_demodulation,[],[f3818,f3908]) ).
fof(f81566,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_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))),
inference(forward_demodulation,[],[f81565,f2177]) ).
fof(f81567,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_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls),c_Int_OPls))),c_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_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))),
inference(forward_demodulation,[],[f81566,f2153]) ).
fof(f81568,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_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),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_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))),
inference(forward_demodulation,[],[f81567,f2159]) ).
fof(f81569,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_Int_OPls,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls),c_Int_OPls)))),c_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_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))),
inference(forward_demodulation,[],[f81568,f2153]) ).
fof(f81570,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_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),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_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))),
inference(forward_demodulation,[],[f81569,f2163]) ).
fof(f81571,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))),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_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))),
inference(forward_demodulation,[],[f81570,f2162]) ).
fof(f81572,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))),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_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))),
inference(forward_demodulation,[],[f81571,f2162]) ).
fof(f81573,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))),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_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))),
inference(forward_demodulation,[],[f81572,f2162]) ).
fof(f84320,definition,
( spl35_66
<=> c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(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)))) ),
introduced(definition,[new_symbols(definition,[spl35_66])],[avatar_definition]) ).
fof(f84321,plain,
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(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))))
| ~ spl35_66 ),
inference(avatar_component_clause,[],[f84320]) ).
fof(f84322,plain,
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(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))))
| spl35_66 ),
inference(avatar_component_clause,[],[f84320]) ).
fof(f84328,plain,
( ~ class_Int_Onumber__ring(tc_RealDef_Oreal)
| ~ c_Orderings_Oord__class_Oless(tc_Int_Oint,c_Int_OPls,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oone__class_Oone(tc_Int_Oint)))
| ~ class_Rings_Olinordered__idom(tc_RealDef_Oreal)
| spl35_66 ),
inference(resolution,[],[f84322,f2202]) ).
fof(f84369,plain,
( ~ c_Orderings_Oord__class_Oless(tc_Int_Oint,c_Int_OPls,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oone__class_Oone(tc_Int_Oint)))
| ~ class_Rings_Olinordered__idom(tc_RealDef_Oreal)
| spl35_66 ),
inference(forward_subsumption_resolution,[],[f84328,f3771]) ).
fof(f84370,plain,
( ~ class_Rings_Olinordered__idom(tc_RealDef_Oreal)
| spl35_66 ),
inference(forward_subsumption_resolution,[],[f84369,f4707]) ).
fof(f84371,plain,
( $false
| spl35_66 ),
inference(forward_subsumption_resolution,[],[f84370,f3757]) ).
fof(f84372,plain,
spl35_66,
inference(avatar_contradiction_clause,[],[f84371]) ).
fof(f84425,plain,
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oone__class_Oone(tc_Int_Oint))),c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____)))))
| ~ spl35_66 ),
inference(forward_subsumption_resolution,[],[f78044,f84321]) ).
fof(f84427,plain,
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p,v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))))
| ~ class_Fields_Olinordered__field(tc_RealDef_Oreal)
| ~ 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))),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_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)))
| ~ spl35_66 ),
inference(resolution,[],[f84425,f3383]) ).
fof(f84432,plain,
( ~ class_Fields_Olinordered__field(tc_RealDef_Oreal)
| ~ 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))),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_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)))
| ~ spl35_66 ),
inference(forward_subsumption_resolution,[],[f84427,f20327]) ).
fof(f84434,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))),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_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)))
| ~ spl35_66 ),
inference(forward_subsumption_resolution,[],[f84432,f3751]) ).
fof(f84437,plain,
( $false
| ~ spl35_66 ),
inference(forward_subsumption_resolution,[],[f84434,f81573]) ).
fof(f84438,plain,
~ spl35_66,
inference(avatar_contradiction_clause,[],[f84437]) ).
cnf(s45,plain,
spl35_66,
inference(sat_conversion,[],[f84372]) ).
cnf(s48,plain,
~ spl35_66,
inference(sat_conversion,[],[f84438]) ).
cnf(s49,plain,
$false,
inference(rat,[],[s45,s48]) ).
fof(f84439,plain,
$false,
inference(avatar_sat_refutation,[],[s49]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW227+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.18 % Computer : n006.cluster.edu
% 0.09/0.18 % Model : x86_64 x86_64
% 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.18 % Memory : 8046.5625MB
% 0.09/0.18 % OS : Linux 6.8.0-71-generic
% 0.09/0.18 % CPULimit : 300
% 0.09/0.18 % WCLimit : 300
% 0.09/0.18 % DateTime : Mon Sep 28 13:19:25 UTC 2026
% 0.09/0.18 % CPUTime :
% 0.09/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.21 Running first-order model finding
% 0.09/0.21 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 10.65/2.02 % (3961580)Will run a generic schedule for satisfiability detection.
% 10.65/2.02 % (3961591)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3679824513:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 10.65/2.02 % (3961586)% WARNING: option uhcvi not known.
% 10.65/2.02 % (3961586)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2317772401:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 10.65/2.02 % (3961585)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=593305310_2999 on theBenchmark for (2999ds/0Mi)
% 10.65/2.02 % (3961588)dis+10_1_sil=32000:sp=arity:random_seed=2264324158:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 10.65/2.02 % (3961587)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=821766168:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 10.65/2.02 % (3961589)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3491607172:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 10.65/2.02 % (3961590)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1596072691:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 10.65/2.02 % (3961591)Instruction limit reached!
% 10.65/2.02 % (3961591)------------------------------
% 10.65/2.02 % (3961591)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.65/2.02 % (3961591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.65/2.02 % (3961591)CaDiCaL version: 2.1.3
% 10.65/2.02 % (3961591)Termination reason: Instruction limit
% 10.65/2.02 % (3961591)Termination phase: Saturation
% 10.65/2.02 % (3961591)Time elapsed: 0.048 s
% 10.65/2.02 % (3961591)Peak memory usage: 15 MB
% 10.65/2.02 % (3961591)Instructions burned: 162 (million)
% 10.65/2.02 % (3961588)Instruction limit reached!
% 10.65/2.02 % (3961588)------------------------------
% 10.65/2.02 % (3961588)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.65/2.02 % (3961588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.65/2.02 % (3961588)CaDiCaL version: 2.1.3
% 10.65/2.02 % (3961588)Termination reason: Instruction limit
% 10.65/2.02 % (3961588)Termination phase: Saturation
% 10.65/2.02 % (3961588)Time elapsed: 0.050 s
% 10.65/2.02 % (3961588)Peak memory usage: 14 MB
% 10.65/2.02 % (3961588)Instructions burned: 103 (million)
% 10.65/2.02 % (3961589)Instruction limit reached!
% 10.65/2.02 % (3961589)------------------------------
% 10.65/2.02 % (3961589)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.65/2.02 % (3961589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.65/2.02 % (3961589)CaDiCaL version: 2.1.3
% 10.65/2.02 % (3961589)Termination reason: Instruction limit
% 10.65/2.02 % (3961589)Termination phase: Saturation
% 10.65/2.02 % (3961589)Time elapsed: 0.054 s
% 10.65/2.02 % (3961589)Peak memory usage: 14 MB
% 10.65/2.02 % (3961589)Instructions burned: 117 (million)
% 10.65/2.02 % (3961599)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1122663924:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 10.65/2.02 % (3961590)Instruction limit reached!
% 10.65/2.02 % (3961590)------------------------------
% 10.65/2.02 % (3961590)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.65/2.02 % (3961590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.65/2.02 % (3961590)CaDiCaL version: 2.1.3
% 10.65/2.02 % (3961590)Termination reason: Instruction limit
% 10.65/2.02 % (3961590)Termination phase: Saturation
% 10.65/2.02 % (3961590)Time elapsed: 0.067 s
% 10.65/2.02 % (3961590)Peak memory usage: 14 MB
% 10.65/2.02 % (3961590)Instructions burned: 132 (million)
% 10.65/2.02 % (3961600)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3535327039:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 10.65/2.02 % (3961601)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=4033980118:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 10.65/2.02 % (3961603)ott-21_1_sil=16000:fs=off:random_seed=1444308033:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 10.65/2.02 % (3961600)Instruction limit reached!
% 10.65/2.02 % (3961600)------------------------------
% 10.65/2.02 % (3961600)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.65/2.02 % (3961600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.65/2.02 % (3961600)CaDiCaL version: 2.1.3
% 22.75/3.60 % (3961600)Termination reason: Instruction limit
% 22.75/3.60 % (3961600)Termination phase: Property scanning
% 22.75/3.60 % (3961600)Time elapsed: 0.060 s
% 22.75/3.60 % (3961600)Peak memory usage: 13 MB
% 22.75/3.60 % (3961600)Instructions burned: 131 (million)
% 22.75/3.60 % (3961607)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1126186381:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 22.75/3.60 % (3961603)Instruction limit reached!
% 22.75/3.60 % (3961603)------------------------------
% 22.75/3.60 % (3961603)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.75/3.60 % (3961603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.75/3.60 % (3961603)CaDiCaL version: 2.1.3
% 22.75/3.60 % (3961603)Termination reason: Instruction limit
% 22.75/3.60 % (3961603)Termination phase: Saturation
% 22.75/3.60 % (3961603)Time elapsed: 0.085 s
% 22.75/3.60 % (3961603)Peak memory usage: 14 MB
% 22.75/3.60 % (3961603)Instructions burned: 181 (million)
% 22.75/3.60 % (3961609)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=692977625:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 22.75/3.60 % TRYING [1]
% 22.75/3.60 % TRYING [2]
% 22.75/3.60 % (3961599)Instruction limit reached!
% 22.75/3.60 % (3961599)------------------------------
% 22.75/3.60 % (3961599)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.75/3.60 % (3961599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.75/3.60 % (3961599)CaDiCaL version: 2.1.3
% 22.75/3.60 % (3961599)Termination reason: Instruction limit
% 22.75/3.60 % (3961599)Termination phase: Finite model building constraint generation
% 22.75/3.60 % (3961599)Time elapsed: 0.180 s
% 22.75/3.60 % (3961599)Peak memory usage: 24 MB
% 22.75/3.60 % (3961599)Instructions burned: 720 (million)
% 22.75/3.60 % (3961611)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1056433718:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 22.75/3.60 % TRYING [1]
% 22.75/3.60 % TRYING [2]
% 22.75/3.60 % (3961607)Instruction limit reached!
% 22.75/3.60 % (3961607)------------------------------
% 22.75/3.60 % (3961607)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.75/3.60 % (3961607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.75/3.60 % (3961607)CaDiCaL version: 2.1.3
% 22.75/3.60 % (3961607)Termination reason: Instruction limit
% 22.75/3.60 % (3961607)Termination phase: Saturation
% 22.75/3.60 % (3961607)Time elapsed: 0.297 s
% 22.75/3.60 % (3961607)Peak memory usage: 16 MB
% 22.75/3.60 % (3961607)Instructions burned: 478 (million)
% 22.75/3.60 % (3961613)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=36103278:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 22.75/3.60 % (3961601)Instruction limit reached!
% 22.75/3.60 % (3961601)------------------------------
% 22.75/3.60 % (3961601)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.75/3.60 % (3961601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.75/3.60 % (3961601)CaDiCaL version: 2.1.3
% 22.75/3.60 % (3961601)Termination reason: Instruction limit
% 22.75/3.60 % (3961601)Termination phase: Saturation
% 22.75/3.60 % (3961601)Time elapsed: 0.409 s
% 22.75/3.60 % (3961601)Peak memory usage: 20 MB
% 22.75/3.60 % (3961601)Instructions burned: 684 (million)
% 22.75/3.60 % TRYING [1]
% 22.75/3.60 % (3961615)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=38894525:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 22.75/3.60 % TRYING [3]
% 22.75/3.60 % TRYING [2]
% 22.75/3.60 % (3961609)Instruction limit reached!
% 22.75/3.60 % (3961609)------------------------------
% 22.75/3.60 % (3961609)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.75/3.60 % (3961609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.75/3.60 % (3961609)CaDiCaL version: 2.1.3
% 22.75/3.60 % (3961609)Termination reason: Instruction limit
% 22.75/3.60 % (3961609)Termination phase: Finite model building constraint generation
% 22.75/3.60 % (3961609)Time elapsed: 0.401 s
% 22.75/3.60 % (3961609)Peak memory usage: 33 MB
% 22.75/3.60 % (3961609)Instructions burned: 866 (million)
% 22.75/3.60 % (3961617)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=258802602:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 22.75/3.60 % (3961611)Instruction limit reached!
% 22.75/3.60 % (3961611)------------------------------
% 22.75/3.60 % (3961611)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.75/3.60 % (3961611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.75/3.60 % (3961611)CaDiCaL version: 2.1.3
% 22.75/3.60 % (3961611)Termination reason: Instruction limit
% 22.75/3.60 % (3961611)Termination phase: Saturation
% 22.75/3.60 % (3961611)Time elapsed: 0.378 s
% 22.75/3.60 % (3961611)Peak memory usage: 22 MB
% 22.75/3.60 % (3961611)Instructions burned: 1179 (million)
% 22.75/3.60 % (3961619)fmb+10_1_sil=64000:random_seed=3729857502:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 22.75/3.60 % TRYING [1]
% 22.75/3.60 % TRYING [2]
% 22.75/3.60 % (3961613)Instruction limit reached!
% 22.75/3.60 % (3961613)------------------------------
% 22.75/3.60 % (3961613)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.75/3.60 % (3961613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.75/3.60 % (3961613)CaDiCaL version: 2.1.3
% 22.75/3.60 % (3961613)Termination reason: Instruction limit
% 22.75/3.60 % (3961613)Termination phase: Finite model building constraint generation
% 22.75/3.60 % (3961613)Time elapsed: 0.433 s
% 22.75/3.60 % (3961613)Peak memory usage: 53 MB
% 22.75/3.60 % (3961613)Instructions burned: 890 (million)
% 22.75/3.60 % (3961621)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=927631190:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 22.75/3.60 % (3961615)Instruction limit reached!
% 22.75/3.60 % (3961615)------------------------------
% 22.75/3.60 % (3961615)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.75/3.60 % (3961615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.75/3.60 % (3961615)CaDiCaL version: 2.1.3
% 22.75/3.60 % (3961615)Termination reason: Instruction limit
% 22.75/3.60 % (3961615)Termination phase: Saturation
% 22.75/3.60 % (3961615)Time elapsed: 0.454 s
% 22.75/3.60 % (3961615)Peak memory usage: 21 MB
% 22.75/3.60 % (3961615)Instructions burned: 692 (million)
% 22.75/3.60 % (3961623)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1525021473:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 22.75/3.60 % (3961617)Instruction limit reached!
% 22.75/3.60 % (3961617)------------------------------
% 22.75/3.60 % (3961617)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.75/3.60 % (3961617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.75/3.60 % (3961617)CaDiCaL version: 2.1.3
% 22.75/3.60 % (3961617)Termination reason: Instruction limit
% 22.75/3.60 % (3961617)Termination phase: Saturation
% 22.75/3.60 % (3961617)Time elapsed: 0.450 s
% 22.75/3.60 % (3961617)Peak memory usage: 20 MB
% 22.75/3.60 % (3961617)Instructions burned: 880 (million)
% 22.75/3.60 % (3961625)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=30179063:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 22.75/3.60 % (3961621)Cannot represent all propositional literals internally
% 22.75/3.60 % (3961621)Refutation not found, incomplete strategy
% 22.75/3.60 % (3961621)------------------------------
% 22.75/3.60 % (3961621)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.75/3.60 % (3961621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.75/3.60 % (3961621)CaDiCaL version: 2.1.3
% 22.75/3.60 % (3961621)Termination reason: Refutation not found, incomplete strategy
% 22.75/3.60 % (3961621)Time elapsed: 0.315 s
% 22.75/3.60 % (3961621)Peak memory usage: 22 MB
% 22.75/3.60 % (3961621)Instructions burned: 645 (million)
% 22.75/3.60 % (3961621)------------------------------
% 22.75/3.60 % (3961621)------------------------------
% 22.75/3.60 % (3961627)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1078902957:i=1472:ins=7:fdi=8:gsp=on_2986 on theBenchmark for (2986ds/1472Mi)
% 22.75/3.60 % TRYING [8]
% 22.75/3.60 % TRYING [3]
% 22.75/3.60 % (3961623)Instruction limit reached!
% 22.75/3.60 % (3961623)------------------------------
% 22.75/3.60 % (3961623)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.75/3.60 % (3961623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.75/3.60 % (3961623)CaDiCaL version: 2.1.3
% 22.75/3.60 % (3961623)Termination reason: Instruction limit
% 22.75/3.60 % (3961623)Termination phase: Finite model building constraint generation
% 22.75/3.60 % (3961623)Time elapsed: 0.409 s
% 22.75/3.60 % (3961623)Peak memory usage: 40 MB
% 22.75/3.60 % (3961623)Instructions burned: 921 (million)
% 22.75/3.60 % (3961629)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2132521157:i=6324_2985 on theBenchmark for (2985ds/6324Mi)
% 22.75/3.60 % TRYING [4]
% 22.75/3.60 % (3961629)Cannot represent all propositional literals internally
% 22.75/3.60 % (3961629)Refutation not found, incomplete strategy
% 22.75/3.60 % (3961629)------------------------------
% 22.75/3.60 % (3961629)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.75/3.60 % (3961629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.75/3.60 % (3961629)CaDiCaL version: 2.1.3
% 22.75/3.60 % (3961629)Termination reason: Refutation not found, incomplete strategy
% 22.75/3.60 % (3961629)Time elapsed: 0.334 s
% 22.75/3.60 % (3961629)Peak memory usage: 23 MB
% 22.75/3.60 % (3961629)Instructions burned: 690 (million)
% 22.75/3.60 % (3961629)------------------------------
% 22.75/3.60 % (3961629)------------------------------
% 22.75/3.60 % (3961631)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=886467588:fmbsr=2.30978:i=2174_2981 on theBenchmark for (2981ds/2174Mi)
% 22.75/3.60 % (3961627)Instruction limit reached!
% 22.75/3.60 % (3961627)------------------------------
% 22.75/3.60 % (3961627)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.75/3.60 % (3961627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.58/3.60 % (3961627)CaDiCaL version: 2.1.3
% 23.58/3.60 % (3961627)Termination reason: Instruction limit
% 23.58/3.60 % (3961627)Termination phase: Saturation
% 23.58/3.60 % (3961627)Time elapsed: 0.762 s
% 23.58/3.60 % (3961627)Peak memory usage: 27 MB
% 23.58/3.60 % (3961627)Instructions burned: 1473 (million)
% 23.58/3.60 % (3961633)ott-2_1_sil=16000:newcnf=on:random_seed=1641821340:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2979 on theBenchmark for (2979ds/869Mi)
% 23.58/3.60 % (3961633)Instruction limit reached!
% 23.58/3.60 % (3961633)------------------------------
% 23.58/3.60 % (3961633)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.58/3.60 % (3961633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.58/3.60 % (3961633)CaDiCaL version: 2.1.3
% 23.58/3.60 % (3961633)Termination reason: Instruction limit
% 23.58/3.60 % (3961633)Termination phase: Saturation
% 23.58/3.60 % (3961633)Time elapsed: 0.508 s
% 23.58/3.60 % (3961633)Peak memory usage: 20 MB
% 23.58/3.60 % (3961633)Instructions burned: 870 (million)
% 23.58/3.60 % (3961635)ott+10_1_sil=32000:tgt=ground:random_seed=1009613153:i=5114:av=off_2973 on theBenchmark for (2973ds/5114Mi)
% 23.58/3.60 % (3961631)Instruction limit reached!
% 23.58/3.60 % (3961631)------------------------------
% 23.58/3.60 % (3961631)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.58/3.60 % (3961631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.58/3.60 % (3961631)CaDiCaL version: 2.1.3
% 23.58/3.60 % (3961631)Termination reason: Instruction limit
% 23.58/3.60 % (3961631)Termination phase: Finite model building preprocessing
% 23.58/3.60 % (3961631)Time elapsed: 1.077 s
% 23.58/3.60 % (3961631)Peak memory usage: 37 MB
% 23.58/3.60 % (3961631)Instructions burned: 2175 (million)
% 23.58/3.60 % (3961637)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3812647543:i=54282_2970 on theBenchmark for (2970ds/54282Mi)
% 23.58/3.60 % TRYING [1]
% 23.58/3.60 % TRYING [2]
% 23.58/3.60 % (3961625) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3961580-3961625"...
% 23.58/3.60 % (3961625)...printing done.
% 23.58/3.60 % (3961625)Refutation found. Thanks to Tanya!
% 23.58/3.60 % SZS status Theorem for theBenchmark
% 23.58/3.60 % SZS output start Proof for theBenchmark
% See solution above
% 23.58/3.60 % (3961625)------------------------------
% 23.58/3.60 % (3961625)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.58/3.60 % (3961625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.58/3.60 % (3961625)CaDiCaL version: 2.1.3
% 23.58/3.60 % (3961625)Termination reason: Refutation
% 23.58/3.60 % (3961625)Time elapsed: 2.173 s
% 23.58/3.60 % (3961625)Peak memory usage: 33 MB
% 23.58/3.60 % (3961625)Instructions burned: 3588 (million)
% 23.58/3.60 % (3961580)Success in time 3.38 s
% 23.58/3.60 % Vampire exiting
%------------------------------------------------------------------------------