%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : ALG375-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n007.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 11:49:18 AM UTC 2026
% Result : Unsatisfiable 11.81s 2.02s
% Output : CNFRefutation 8.87s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 47
% Syntax : Number of formulae : 161 ( 72 unt; 22 def)
% Number of atoms : 274 ( 41 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 210 ( 97 ~; 91 |; 0 &)
% ( 22 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 3 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 35 ( 33 usr; 24 prp; 0-3 aty)
% Number of functors : 20 ( 20 usr; 6 con; 0-3 aty)
% Number of variables : 65 ( 65 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,axiom,
! [V_w] : c_lessequals(V_w,V_w,tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f83,axiom,
! [V_z1,V_z2,V_w] : c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(V_z1,V_z2,tc_RealDef_Oreal),V_w,tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_z1,V_w,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(V_z2,V_w,tc_RealDef_Oreal),tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f270,axiom,
! [V_z,V_w] : c_HOL_Otimes__class_Otimes(V_z,V_w,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(V_w,V_z,tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f389,axiom,
! [V_x] : c_HOL_Oplus__class_Oplus(V_x,c_HOL_Ouminus__class_Ouminus(V_x,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f393,axiom,
! [V_x,V_y] :
( V_y = c_HOL_Ouminus__class_Ouminus(V_x,tc_RealDef_Oreal)
| c_HOL_Oplus__class_Oplus(V_x,V_y,tc_RealDef_Oreal) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f397,axiom,
! [V_r,V_s] : c_HOL_Ominus__class_Ominus(V_r,V_s,tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(V_r,c_HOL_Ouminus__class_Ouminus(V_s,tc_RealDef_Oreal),tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f399,axiom,
! [V_x,V_y] : c_HOL_Oabs__class_Oabs(c_HOL_Oplus__class_Oplus(V_x,c_HOL_Ouminus__class_Ouminus(V_y,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Oabs__class_Oabs(c_HOL_Oplus__class_Oplus(V_y,c_HOL_Ouminus__class_Ouminus(V_x,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f730,axiom,
! [V_x] : c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(V_x,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(V_x,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) = V_x,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f742,axiom,
! [V_a,V_b] : c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_HOL_Oplus__class_Oplus(V_a,V_b,tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),V_a,tc_RealDef_Oreal) = c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(V_b,V_a,tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f783,axiom,
! [V_x] : ~ c_HOL_Oord__class_Oless(V_x,V_x,tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f915,axiom,
! [V_w] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(c_HOL_Ominus__class_Ominus(V_w,v_z____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(c_HOL_Ominus__class_Ominus(V_w,v_z____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_sko__CHAINED__1(v_p,v_s____,v_z____),tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(c_HOL_Ominus__class_Ominus(c_Polynomial_Opoly(v_p,V_w,tc_Complex_Ocomplex),c_Polynomial_Opoly(v_p,v_z____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Oinverse__class_Odivide(c_HOL_Oabs__class_Oabs(c_HOL_Ominus__class_Ominus(c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_p,v_z____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Ouminus__class_Ouminus(v_s____,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f916,axiom,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_sko__CHAINED__1(v_p,v_s____,v_z____),tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f917,negated_conjecture,
~ v_thesis____,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f918,negated_conjecture,
! [V_da] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_da,tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(c_HOL_Ominus__class_Ominus(v_d(V_da),v_z____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal)
| v_thesis____ ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f919,negated_conjecture,
! [V_da] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_da,tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(c_HOL_Ominus__class_Ominus(v_d(V_da),v_z____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),V_da,tc_RealDef_Oreal)
| v_thesis____ ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f920,negated_conjecture,
! [V_da] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_da,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(c_HOL_Ominus__class_Ominus(c_Polynomial_Opoly(v_p,v_d(V_da),tc_Complex_Ocomplex),c_Polynomial_Opoly(v_p,v_z____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Oinverse__class_Odivide(c_HOL_Oabs__class_Oabs(c_HOL_Ominus__class_Ominus(c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_p,v_z____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Ouminus__class_Ouminus(v_s____,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)
| v_thesis____ ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f972,axiom,
class_Ring__and__Field_Opordered__cancel__semiring(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f974,axiom,
class_OrderedGroup_Opordered__ab__semigroup__add(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f977,axiom,
class_OrderedGroup_Opordered__comm__monoid__add(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f980,axiom,
class_Ring__and__Field_Oordered__ring__strict(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f983,axiom,
class_OrderedGroup_Olordered__ab__group__add(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f986,axiom,
class_Ring__and__Field_Opordered__semiring(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f991,axiom,
class_Ring__and__Field_Odivision__by__zero(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1006,axiom,
class_Ring__and__Field_Oordered__idom(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1056,plain,
c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f1079,plain,
! [X0] : c_lessequals(X0,X0,tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f1184,plain,
! [X0,X1,X2] : c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(X0,X1,tc_RealDef_Oreal),X2,tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(X0,X2,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X1,X2,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f83]) ).
fof(f1477,plain,
! [X0,X1] : c_HOL_Otimes__class_Otimes(X0,X1,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(X1,X0,tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f270]) ).
fof(f1672,plain,
! [X0] : c_HOL_Oplus__class_Oplus(X0,c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f389]) ).
fof(f1678,plain,
! [X0,X1] :
( X1 = c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal)
| c_HOL_Oplus__class_Oplus(X0,X1,tc_RealDef_Oreal) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
inference(cnf_transformation,[status(thm)],[f393]) ).
fof(f1682,plain,
! [X0,X1] : c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(X0,c_HOL_Ouminus__class_Ouminus(X1,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f397]) ).
fof(f1684,plain,
! [X0,X1] : c_HOL_Oabs__class_Oabs(c_HOL_Oplus__class_Oplus(X0,c_HOL_Ouminus__class_Ouminus(X1,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Oabs__class_Oabs(c_HOL_Oplus__class_Oplus(X1,c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f399]) ).
fof(f2187,plain,
! [X0] : c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) = X0,
inference(cnf_transformation,[status(thm)],[f730]) ).
fof(f2200,plain,
! [X0,X1] : c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_HOL_Oplus__class_Oplus(X0,X1,tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),X0,tc_RealDef_Oreal) = c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(X1,X0,tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f742]) ).
fof(f2264,plain,
! [X0] : ~ c_HOL_Oord__class_Oless(X0,X0,tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f783]) ).
fof(f2465,plain,
! [X0] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(c_HOL_Ominus__class_Ominus(X0,v_z____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(c_HOL_Ominus__class_Ominus(X0,v_z____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_sko__CHAINED__1(v_p,v_s____,v_z____),tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(c_HOL_Ominus__class_Ominus(c_Polynomial_Opoly(v_p,X0,tc_Complex_Ocomplex),c_Polynomial_Opoly(v_p,v_z____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Oinverse__class_Odivide(c_HOL_Oabs__class_Oabs(c_HOL_Ominus__class_Ominus(c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_p,v_z____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Ouminus__class_Ouminus(v_s____,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(cnf_transformation,[status(thm)],[f915]) ).
fof(f2466,plain,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_sko__CHAINED__1(v_p,v_s____,v_z____),tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f916]) ).
fof(f2467,plain,
~ v_thesis____,
inference(cnf_transformation,[status(thm)],[f917]) ).
fof(f2468,plain,
! [X0] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(c_HOL_Ominus__class_Ominus(v_d(X0),v_z____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal)
| v_thesis____ ),
inference(cnf_transformation,[status(thm)],[f918]) ).
fof(f2469,plain,
! [X0] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(c_HOL_Ominus__class_Ominus(v_d(X0),v_z____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),X0,tc_RealDef_Oreal)
| v_thesis____ ),
inference(cnf_transformation,[status(thm)],[f919]) ).
fof(f2470,plain,
! [X0] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(c_HOL_Ominus__class_Ominus(c_Polynomial_Opoly(v_p,v_d(X0),tc_Complex_Ocomplex),c_Polynomial_Opoly(v_p,v_z____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Oinverse__class_Odivide(c_HOL_Oabs__class_Oabs(c_HOL_Ominus__class_Ominus(c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_p,v_z____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Ouminus__class_Ouminus(v_s____,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)
| v_thesis____ ),
inference(cnf_transformation,[status(thm)],[f920]) ).
fof(f2522,plain,
class_Ring__and__Field_Opordered__cancel__semiring(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f972]) ).
fof(f2524,plain,
class_OrderedGroup_Opordered__ab__semigroup__add(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f974]) ).
fof(f2527,plain,
class_OrderedGroup_Opordered__comm__monoid__add(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f977]) ).
fof(f2530,plain,
class_Ring__and__Field_Oordered__ring__strict(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f980]) ).
fof(f2533,plain,
class_OrderedGroup_Olordered__ab__group__add(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f983]) ).
fof(f2536,plain,
class_Ring__and__Field_Opordered__semiring(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f986]) ).
fof(f2541,plain,
class_Ring__and__Field_Odivision__by__zero(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f991]) ).
fof(f2556,plain,
class_Ring__and__Field_Oordered__idom(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f1006]) ).
fof(f2606,definition,
( sQ0_spl
<=> v_thesis____ ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f2607,plain,
( ~ sQ0_spl
| v_thesis____ ),
inference(component_clause,[status(thm)],[f2606]) ).
fof(f2621,definition,
! [X0] :
( sQ4_spl
<=> ( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(c_HOL_Ominus__class_Ominus(v_d(X0),v_z____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal) ) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f2622,plain,
! [X0] :
( ~ sQ4_spl
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(c_HOL_Ominus__class_Ominus(v_d(X0),v_z____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f2621]) ).
fof(f2624,plain,
( sQ4_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f2468,f2606,f2621]) ).
fof(f2625,definition,
! [X0] :
( sQ5_spl
<=> ( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(c_HOL_Ominus__class_Ominus(v_d(X0),v_z____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),X0,tc_RealDef_Oreal) ) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f2626,plain,
! [X0] :
( ~ sQ5_spl
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(c_HOL_Ominus__class_Ominus(v_d(X0),v_z____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),X0,tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f2625]) ).
fof(f2628,plain,
( sQ5_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f2469,f2606,f2625]) ).
fof(f2629,definition,
! [X0] :
( sQ6_spl
<=> ( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(c_HOL_Ominus__class_Ominus(c_Polynomial_Opoly(v_p,v_d(X0),tc_Complex_Ocomplex),c_Polynomial_Opoly(v_p,v_z____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Oinverse__class_Odivide(c_HOL_Oabs__class_Oabs(c_HOL_Ominus__class_Ominus(c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_p,v_z____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Ouminus__class_Ouminus(v_s____,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) ) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f2630,plain,
! [X0] :
( ~ sQ6_spl
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(c_HOL_Ominus__class_Ominus(c_Polynomial_Opoly(v_p,v_d(X0),tc_Complex_Ocomplex),c_Polynomial_Opoly(v_p,v_z____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Oinverse__class_Odivide(c_HOL_Oabs__class_Oabs(c_HOL_Ominus__class_Ominus(c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_p,v_z____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Ouminus__class_Ouminus(v_s____,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f2629]) ).
fof(f2632,plain,
( sQ6_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f2470,f2606,f2629]) ).
fof(f2634,plain,
c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(backward_demodulation,[status(thm)],[f1184,f1056]) ).
fof(f2644,plain,
! [X0] : c_HOL_Ominus__class_Ominus(X0,X0,tc_RealDef_Oreal) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(backward_demodulation,[status(thm)],[f1682,f1672]) ).
fof(f2645,plain,
! [X0,X1] : c_HOL_Oabs__class_Oabs(c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Oabs__class_Oabs(c_HOL_Oplus__class_Oplus(X1,c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[status(thm)],[f1682,f1684]) ).
fof(f2646,plain,
! [X0,X1] : c_HOL_Oabs__class_Oabs(c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Oabs__class_Oabs(c_HOL_Ominus__class_Ominus(X1,X0,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[status(thm)],[f1682,f2645]) ).
fof(f2662,plain,
! [X0] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(c_HOL_Ominus__class_Ominus(X0,v_z____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(c_HOL_Ominus__class_Ominus(X0,v_z____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_sko__CHAINED__1(v_p,v_s____,v_z____),tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(c_HOL_Ominus__class_Ominus(c_Polynomial_Opoly(v_p,X0,tc_Complex_Ocomplex),c_Polynomial_Opoly(v_p,v_z____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Oinverse__class_Odivide(c_HOL_Oabs__class_Oabs(c_HOL_Ominus__class_Ominus(c_HOL_Ouminus__class_Ouminus(v_s____,tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_p,v_z____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(forward_demodulation,[status(thm)],[f2646,f2465]) ).
fof(f2663,plain,
( ~ sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2607,f2467]) ).
fof(f2664,plain,
~ sQ0_spl,
inference(contradiction_clause,[status(thm)],[f2663]) ).
fof(f2665,plain,
c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(forward_demodulation,[status(thm)],[f1477,f2634]) ).
fof(f2667,plain,
! [X0] :
( ~ sQ6_spl
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(c_HOL_Ominus__class_Ominus(c_Polynomial_Opoly(v_p,v_d(X0),tc_Complex_Ocomplex),c_Polynomial_Opoly(v_p,v_z____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Oinverse__class_Odivide(c_HOL_Oabs__class_Oabs(c_HOL_Ominus__class_Ominus(c_HOL_Ouminus__class_Ouminus(v_s____,tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_p,v_z____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(forward_demodulation,[status(thm)],[f2646,f2630]) ).
fof(f3163,definition,
( sQ54_spl
<=> c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(c_HOL_Ominus__class_Ominus(v_d(v_sko__CHAINED__1(v_p,v_s____,v_z____)),v_z____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f3165,plain,
( sQ54_spl
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(c_HOL_Ominus__class_Ominus(v_d(v_sko__CHAINED__1(v_p,v_s____,v_z____)),v_z____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f3163]) ).
fof(f3166,definition,
( sQ55_spl
<=> c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_sko__CHAINED__1(v_p,v_s____,v_z____),tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f3168,plain,
( sQ55_spl
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_sko__CHAINED__1(v_p,v_s____,v_z____),tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f3166]) ).
fof(f3170,plain,
( sQ55_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3168,f2466]) ).
fof(f3171,plain,
sQ55_spl,
inference(contradiction_clause,[status(thm)],[f3170]) ).
fof(f3187,plain,
( ~ sQ4_spl
| sQ54_spl
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_sko__CHAINED__1(v_p,v_s____,v_z____),tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f3165,f2622]) ).
fof(f3188,plain,
( ~ sQ4_spl
| sQ54_spl
| ~ sQ55_spl ),
inference(split_clause,[status(thm)],[f3187,f3166,f3163,f2621]) ).
fof(f3192,definition,
! [X0] :
( sQ56_spl
<=> c_HOL_Oord__class_Oless(X0,X0,tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f3193,plain,
! [X0] :
( ~ sQ56_spl
| c_HOL_Oord__class_Oless(X0,X0,tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f3192]) ).
fof(f3200,plain,
( ~ sQ56_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3193,f2264]) ).
fof(f3201,plain,
~ sQ56_spl,
inference(contradiction_clause,[status(thm)],[f3200]) ).
fof(f3241,definition,
( sQ58_spl
<=> class_OrderedGroup_Opordered__comm__monoid__add(tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f3243,plain,
( sQ58_spl
| ~ class_OrderedGroup_Opordered__comm__monoid__add(tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f3241]) ).
fof(f3248,definition,
( sQ60_spl
<=> class_OrderedGroup_Opordered__ab__semigroup__add(tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition]) ).
fof(f3250,plain,
( sQ60_spl
| ~ class_OrderedGroup_Opordered__ab__semigroup__add(tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f3248]) ).
fof(f3259,definition,
( sQ63_spl
<=> class_OrderedGroup_Olordered__ab__group__add(tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f3261,plain,
( sQ63_spl
| ~ class_OrderedGroup_Olordered__ab__group__add(tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f3259]) ).
fof(f3270,plain,
( sQ63_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3261,f2533]) ).
fof(f3271,plain,
sQ63_spl,
inference(contradiction_clause,[status(thm)],[f3270]) ).
fof(f3272,plain,
( sQ60_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3250,f2524]) ).
fof(f3273,plain,
sQ60_spl,
inference(contradiction_clause,[status(thm)],[f3272]) ).
fof(f3274,plain,
( sQ58_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3243,f2527]) ).
fof(f3275,plain,
sQ58_spl,
inference(contradiction_clause,[status(thm)],[f3274]) ).
fof(f3407,definition,
( sQ68_spl
<=> class_Ring__and__Field_Oordered__ring__strict(tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition]) ).
fof(f3409,plain,
( sQ68_spl
| ~ class_Ring__and__Field_Oordered__ring__strict(tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f3407]) ).
fof(f3426,definition,
( sQ73_spl
<=> class_Ring__and__Field_Opordered__semiring(tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition]) ).
fof(f3428,plain,
( sQ73_spl
| ~ class_Ring__and__Field_Opordered__semiring(tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f3426]) ).
fof(f3445,definition,
( sQ78_spl
<=> class_Ring__and__Field_Oordered__idom(tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition]) ).
fof(f3447,plain,
( sQ78_spl
| ~ class_Ring__and__Field_Oordered__idom(tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f3445]) ).
fof(f3467,definition,
( sQ84_spl
<=> class_Ring__and__Field_Opordered__cancel__semiring(tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition]) ).
fof(f3469,plain,
( sQ84_spl
| ~ class_Ring__and__Field_Opordered__cancel__semiring(tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f3467]) ).
fof(f3472,plain,
( sQ68_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3409,f2530]) ).
fof(f3473,plain,
sQ68_spl,
inference(contradiction_clause,[status(thm)],[f3472]) ).
fof(f3474,plain,
( sQ73_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3428,f2536]) ).
fof(f3475,plain,
sQ73_spl,
inference(contradiction_clause,[status(thm)],[f3474]) ).
fof(f3476,plain,
( sQ84_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3469,f2522]) ).
fof(f3477,plain,
sQ84_spl,
inference(contradiction_clause,[status(thm)],[f3476]) ).
fof(f3478,plain,
( sQ78_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3447,f2556]) ).
fof(f3479,plain,
sQ78_spl,
inference(contradiction_clause,[status(thm)],[f3478]) ).
fof(f3517,definition,
( sQ85_spl
<=> class_Ring__and__Field_Odivision__by__zero(tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition]) ).
fof(f3519,plain,
( sQ85_spl
| ~ class_Ring__and__Field_Odivision__by__zero(tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f3517]) ).
fof(f3528,plain,
( sQ85_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3519,f2541]) ).
fof(f3529,plain,
sQ85_spl,
inference(contradiction_clause,[status(thm)],[f3528]) ).
fof(f3538,plain,
c_HOL_Oinverse__class_Odivide(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Ouminus__class_Ouminus(c_HOL_Oinverse__class_Odivide(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(resolution,[status(thm)],[f2187,f1678]) ).
fof(f3539,plain,
! [X0] : c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(paramodulation,[status(thm)],[f2187,f2200]) ).
fof(f3554,plain,
! [X0] : c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[status(thm)],[f2644,f3539]) ).
fof(f3555,plain,
c_HOL_Oinverse__class_Odivide(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Ouminus__class_Ouminus(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(backward_demodulation,[status(thm)],[f3557,f3538]) ).
fof(f3557,plain,
c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_HOL_Oinverse__class_Odivide(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[status(thm)],[f2644,f3554]) ).
fof(f3585,plain,
c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_HOL_Ouminus__class_Ouminus(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[status(thm)],[f3557,f3555]) ).
fof(f3618,plain,
! [X0] : c_HOL_Ominus__class_Ominus(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(paramodulation,[status(thm)],[f3585,f1682]) ).
fof(f3680,definition,
( sQ99_spl
<=> c_lessequals(c_HOL_Oinverse__class_Odivide(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition]) ).
fof(f3682,plain,
( sQ99_spl
| ~ c_lessequals(c_HOL_Oinverse__class_Odivide(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f3680]) ).
fof(f3686,plain,
( sQ99_spl
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(forward_demodulation,[status(thm)],[f3557,f3682]) ).
fof(f3687,plain,
( sQ99_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3686,f1079]) ).
fof(f3688,plain,
sQ99_spl,
inference(contradiction_clause,[status(thm)],[f3687]) ).
fof(f3712,plain,
c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(paramodulation,[status(thm)],[f2644,f3618]) ).
fof(f3727,plain,
c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(backward_demodulation,[status(thm)],[f3712,f2665]) ).
fof(f3764,definition,
( sQ101_spl
<=> c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition]) ).
fof(f3765,plain,
( ~ sQ101_spl
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f3764]) ).
fof(f3768,definition,
( sQ102_spl
<=> c_HOL_Oord__class_Oless(c_HOL_Oinverse__class_Odivide(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition]) ).
fof(f3769,plain,
( ~ sQ102_spl
| c_HOL_Oord__class_Oless(c_HOL_Oinverse__class_Odivide(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f3768]) ).
fof(f3777,definition,
( sQ104_spl
<=> c_HOL_Oord__class_Oless(c_HOL_Ouminus__class_Ouminus(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition]) ).
fof(f3778,plain,
( ~ sQ104_spl
| c_HOL_Oord__class_Oless(c_HOL_Ouminus__class_Ouminus(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f3777]) ).
fof(f3793,plain,
( ~ sQ104_spl
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(forward_demodulation,[status(thm)],[f3585,f3778]) ).
fof(f3794,plain,
( ~ sQ104_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3793,f2264]) ).
fof(f3795,plain,
~ sQ104_spl,
inference(contradiction_clause,[status(thm)],[f3794]) ).
fof(f3796,plain,
( ~ sQ102_spl
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(forward_demodulation,[status(thm)],[f3557,f3769]) ).
fof(f3797,plain,
( ~ sQ102_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3796,f2264]) ).
fof(f3798,plain,
~ sQ102_spl,
inference(contradiction_clause,[status(thm)],[f3797]) ).
fof(f3799,plain,
( ~ sQ101_spl
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(forward_demodulation,[status(thm)],[f3557,f3765]) ).
fof(f3800,plain,
( ~ sQ101_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3799,f2264]) ).
fof(f3801,plain,
~ sQ101_spl,
inference(contradiction_clause,[status(thm)],[f3800]) ).
fof(f3950,definition,
! [X0] :
( sQ114_spl
<=> c_HOL_Otimes__class_Otimes(X0,X0,tc_RealDef_Oreal) != c_HOL_Ouminus__class_Ouminus(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ114_spl])],[split_symbol_definition]) ).
fof(f3951,plain,
! [X0] :
( ~ sQ114_spl
| c_HOL_Otimes__class_Otimes(X0,X0,tc_RealDef_Oreal) != c_HOL_Ouminus__class_Ouminus(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f3950]) ).
fof(f3954,plain,
( ~ sQ114_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f3727,f3955]) ).
fof(f3955,plain,
! [X0] :
( ~ sQ114_spl
| c_HOL_Otimes__class_Otimes(X0,X0,tc_RealDef_Oreal) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
inference(forward_demodulation,[status(thm)],[f3585,f3951]) ).
fof(f3956,plain,
~ sQ114_spl,
inference(contradiction_clause,[status(thm)],[f3954]) ).
fof(f3988,definition,
! [X0] :
( sQ115_spl
<=> c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) != c_HOL_Ouminus__class_Ouminus(c_HOL_Otimes__class_Otimes(X0,X0,tc_RealDef_Oreal),tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition]) ).
fof(f3989,plain,
! [X0] :
( ~ sQ115_spl
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) != c_HOL_Ouminus__class_Ouminus(c_HOL_Otimes__class_Otimes(X0,X0,tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f3988]) ).
fof(f4007,plain,
( ~ sQ115_spl
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) != c_HOL_Ouminus__class_Ouminus(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(paramodulation,[status(thm)],[f3727,f3989]) ).
fof(f4008,plain,
( ~ sQ115_spl
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
inference(forward_demodulation,[status(thm)],[f3585,f4007]) ).
fof(f4009,plain,
( ~ sQ115_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f4008]) ).
fof(f4010,plain,
~ sQ115_spl,
inference(contradiction_clause,[status(thm)],[f4009]) ).
fof(f4021,plain,
( ~ sQ5_spl
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_sko__CHAINED__1(v_p,v_s____,v_z____),tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(c_HOL_Ominus__class_Ominus(v_d(v_sko__CHAINED__1(v_p,v_s____,v_z____)),v_z____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(c_HOL_Ominus__class_Ominus(c_Polynomial_Opoly(v_p,v_d(v_sko__CHAINED__1(v_p,v_s____,v_z____)),tc_Complex_Ocomplex),c_Polynomial_Opoly(v_p,v_z____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Oinverse__class_Odivide(c_HOL_Oabs__class_Oabs(c_HOL_Ominus__class_Ominus(c_HOL_Ouminus__class_Ouminus(v_s____,tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_p,v_z____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f2662,f2626]) ).
fof(f4022,definition,
( sQ117_spl
<=> c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(c_HOL_Ominus__class_Ominus(c_Polynomial_Opoly(v_p,v_d(v_sko__CHAINED__1(v_p,v_s____,v_z____)),tc_Complex_Ocomplex),c_Polynomial_Opoly(v_p,v_z____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Oinverse__class_Odivide(c_HOL_Oabs__class_Oabs(c_HOL_Ominus__class_Ominus(c_HOL_Ouminus__class_Ouminus(v_s____,tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_p,v_z____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ117_spl])],[split_symbol_definition]) ).
fof(f4023,plain,
( ~ sQ117_spl
| c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(c_HOL_Ominus__class_Ominus(c_Polynomial_Opoly(v_p,v_d(v_sko__CHAINED__1(v_p,v_s____,v_z____)),tc_Complex_Ocomplex),c_Polynomial_Opoly(v_p,v_z____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Oinverse__class_Odivide(c_HOL_Oabs__class_Oabs(c_HOL_Ominus__class_Ominus(c_HOL_Ouminus__class_Ouminus(v_s____,tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_p,v_z____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f4022]) ).
fof(f4025,plain,
( ~ sQ5_spl
| ~ sQ55_spl
| ~ sQ54_spl
| sQ117_spl ),
inference(split_clause,[status(thm)],[f4021,f4022,f3163,f3166,f2625]) ).
fof(f4041,plain,
( ~ sQ6_spl
| ~ sQ117_spl
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_sko__CHAINED__1(v_p,v_s____,v_z____),tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f4023,f2667]) ).
fof(f4043,plain,
( ~ sQ6_spl
| ~ sQ117_spl
| ~ sQ55_spl ),
inference(split_clause,[status(thm)],[f4041,f3166,f4022,f2629]) ).
fof(f4048,plain,
$false,
inference(sat_refutation,[status(thm)],[f2624,f2628,f2632,f2664,f3171,f3188,f3201,f3271,f3273,f3275,f3473,f3475,f3477,f3479,f3529,f3688,f3795,f3798,f3801,f3956,f4010,f4025,f4043]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ALG375-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.07/0.35 % Computer : n007.cluster.edu
% 0.07/0.35 % Model : x86_64 x86_64
% 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.35 % Memory : 8046.5625MB
% 0.07/0.35 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Mon Sep 21 13:16:06 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.12/0.43 % Drodi V4.1.1
% 11.81/2.02 % Refutation found
% 11.81/2.02 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 11.81/2.02 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 8.87/2.09 % Elapsed time: 1.719817 seconds
% 8.87/2.09 % CPU time: 12.678280 seconds
% 8.87/2.09 % Total memory used: 287.679 MB
% 8.87/2.09 % Net memory used: 280.662 MB
%------------------------------------------------------------------------------