%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : ALG363-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n004.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:16 AM UTC 2026
% Result : Unsatisfiable 0.13s 5.57s
% Output : CNFRefutation 0.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 80
% Syntax : Number of formulae : 257 ( 45 unt; 40 def)
% Number of atoms : 550 ( 101 equ)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 507 ( 214 ~; 253 |; 0 &)
% ( 40 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 51 ( 49 usr; 41 prp; 0-3 aty)
% Number of functors : 15 ( 15 usr; 3 con; 0-3 aty)
% Number of variables : 130 ( 130 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f17,axiom,
! [T_a,V_a] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(V_a,V_a,T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f23,axiom,
! [T_a,V_a] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Oinverse__class_Oinverse(V_a,T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| c_HOL_Oord__class_Oless(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Odivision__by__zero(T_a)
| ~ class_Ring__and__Field_Oordered__field(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f24,axiom,
! [T_a,V_a] :
( ~ c_HOL_Oord__class_Oless(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a)
| c_HOL_Oord__class_Oless(c_HOL_Oinverse__class_Oinverse(V_a,T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Odivision__by__zero(T_a)
| ~ class_Ring__and__Field_Oordered__field(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f34,axiom,
! [T_a,V_a] :
( ~ c_lessequals(c_HOL_Oinverse__class_Oinverse(V_a,T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| c_lessequals(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Odivision__by__zero(T_a)
| ~ class_Ring__and__Field_Oordered__field(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f35,axiom,
! [T_a,V_a] :
( ~ c_lessequals(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a)
| c_lessequals(c_HOL_Oinverse__class_Oinverse(V_a,T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Odivision__by__zero(T_a)
| ~ class_Ring__and__Field_Oordered__field(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f132,axiom,
c_HOL_Otimes__class_Otimes(c_HOL_Ouminus__class_Ouminus(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Ouminus__class_Ouminus(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Oone__class_Oone(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f172,axiom,
! [V_x] :
( V_x = c_HOL_Oone__class_Oone(tc_RealDef_Oreal)
| V_x = c_HOL_Ouminus__class_Ouminus(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_HOL_Otimes__class_Otimes(V_x,V_x,tc_RealDef_Oreal) != c_HOL_Oone__class_Oone(tc_RealDef_Oreal) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f228,axiom,
c_Transcendental_Ocos(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)) = c_HOL_Oone__class_Oone(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f234,axiom,
! [V_x,V_y] :
( V_x = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)
| c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_x,V_x,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(V_y,V_y,tc_RealDef_Oreal),tc_RealDef_Oreal) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f239,axiom,
! [V_r,V_x] :
( ~ c_lessequals(c_HOL_Oabs__class_Oabs(V_x,tc_RealDef_Oreal),V_r,tc_RealDef_Oreal)
| c_lessequals(c_HOL_Ouminus__class_Ouminus(V_r,tc_RealDef_Oreal),V_x,tc_RealDef_Oreal) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f320,axiom,
! [T_a,V_a] :
( V_a = c_HOL_Ozero__class_Ozero(T_a)
| c_HOL_Ouminus__class_Ouminus(V_a,T_a) != V_a
| ~ class_OrderedGroup_Oordered__ab__group__add(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f402,axiom,
! [V_z] : c_HOL_Otimes__class_Otimes(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),V_z,tc_RealDef_Oreal) = V_z,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f416,axiom,
( c_Transcendental_Oln(c_HOL_Oone__class_Oone(tc_RealDef_Oreal)) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f426,axiom,
! [V_x,V_y] :
( V_x = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_x,V_x,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(V_y,V_y,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f427,axiom,
! [V_x,V_y] :
( V_y = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_x,V_x,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(V_y,V_y,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f435,axiom,
! [V_r] :
( ~ c_HOL_Oord__class_Oless(V_r,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_HOL_Oabs__class_Oabs(V_r,tc_RealDef_Oreal) = c_HOL_Ouminus__class_Ouminus(V_r,tc_RealDef_Oreal) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f459,axiom,
! [T_a,V_a] :
( c_lessequals(V_a,c_HOL_Oabs__class_Oabs(V_a,T_a),T_a)
| ~ class_OrderedGroup_Opordered__ab__group__add__abs(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f462,axiom,
! [T_a] :
( c_lessequals(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Oone__class_Oone(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__semidom(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f463,axiom,
! [V_x] : ~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(c_HOL_Oabs__class_Oabs(V_x,tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),V_x,tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f466,axiom,
! [V_x] : ~ c_HOL_Oord__class_Oless(V_x,V_x,tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f473,axiom,
! [V_x,V_y] :
( ~ c_HOL_Oord__class_Oless(V_x,V_y,tc_RealDef_Oreal)
| c_lessequals(V_x,V_y,tc_RealDef_Oreal) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f476,axiom,
! [T_a] :
( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Oone__class_Oone(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__semidom(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f479,axiom,
! [V_r] :
( c_HOL_Oord__class_Oless(V_r,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_HOL_Oabs__class_Oabs(V_r,tc_RealDef_Oreal) = V_r ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f493,axiom,
! [V_i,V_k,V_j] :
( ~ c_lessequals(V_i,V_j,tc_RealDef_Oreal)
| ~ c_lessequals(V_j,V_k,tc_RealDef_Oreal)
| c_lessequals(V_i,V_k,tc_RealDef_Oreal) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f494,axiom,
! [V_w] : c_lessequals(V_w,V_w,tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f507,axiom,
! [V_w,V_z] :
( c_lessequals(V_z,V_w,tc_RealDef_Oreal)
| c_lessequals(V_w,V_z,tc_RealDef_Oreal) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f514,axiom,
c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) != c_HOL_Oone__class_Oone(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f533,axiom,
! [V_x,V_y] :
( ~ c_lessequals(V_x,V_y,tc_RealDef_Oreal)
| V_x = V_y
| c_HOL_Oord__class_Oless(V_x,V_y,tc_RealDef_Oreal) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f536,axiom,
c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_r,tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f537,axiom,
! [V_n] : c_lessequals(c_HOL_Oabs__class_Oabs(c_Complex_ORe(v_s(V_n)),tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(v_r,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f556,axiom,
! [V_z,V_w] :
( ~ c_lessequals(V_z,V_w,tc_RealDef_Oreal)
| ~ c_lessequals(V_w,V_z,tc_RealDef_Oreal)
| V_z = V_w ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f601,axiom,
! [T_a,V_a] :
( c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(T_a),V_a,T_a) = V_a
| ~ class_OrderedGroup_Omonoid__add(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f612,negated_conjecture,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(v_r,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Oabs__class_Oabs(c_Complex_ORe(v_s(v_f____(v_x))),tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(v_r,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f619,axiom,
class_OrderedGroup_Opordered__ab__group__add__abs(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f624,axiom,
class_Ring__and__Field_Oordered__ring__strict(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f628,axiom,
class_OrderedGroup_Oordered__ab__group__add(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f635,axiom,
class_Ring__and__Field_Odivision__by__zero(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f636,axiom,
class_Ring__and__Field_Oordered__semidom(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f644,axiom,
class_Ring__and__Field_Oordered__field(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f658,axiom,
class_OrderedGroup_Omonoid__add(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f722,plain,
! [T_a] :
( ! [V_a] : ~ c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(V_a,V_a,T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
inference(miniscoping,[status(thm)],[f17]) ).
fof(f723,plain,
! [X0,X1] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(X1,X1,X0),c_HOL_Ozero__class_Ozero(X0),X0)
| ~ class_Ring__and__Field_Oordered__ring__strict(X0) ),
inference(cnf_transformation,[status(thm)],[f722]) ).
fof(f729,plain,
! [X0,X1] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Oinverse__class_Oinverse(X1,X0),c_HOL_Ozero__class_Ozero(X0),X0)
| c_HOL_Oord__class_Oless(X1,c_HOL_Ozero__class_Ozero(X0),X0)
| ~ class_Ring__and__Field_Odivision__by__zero(X0)
| ~ class_Ring__and__Field_Oordered__field(X0) ),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f730,plain,
! [X0,X1] :
( ~ c_HOL_Oord__class_Oless(X1,c_HOL_Ozero__class_Ozero(X0),X0)
| c_HOL_Oord__class_Oless(c_HOL_Oinverse__class_Oinverse(X1,X0),c_HOL_Ozero__class_Ozero(X0),X0)
| ~ class_Ring__and__Field_Odivision__by__zero(X0)
| ~ class_Ring__and__Field_Oordered__field(X0) ),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f740,plain,
! [X0,X1] :
( ~ c_lessequals(c_HOL_Oinverse__class_Oinverse(X1,X0),c_HOL_Ozero__class_Ozero(X0),X0)
| c_lessequals(X1,c_HOL_Ozero__class_Ozero(X0),X0)
| ~ class_Ring__and__Field_Odivision__by__zero(X0)
| ~ class_Ring__and__Field_Oordered__field(X0) ),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f741,plain,
! [X0,X1] :
( ~ c_lessequals(X1,c_HOL_Ozero__class_Ozero(X0),X0)
| c_lessequals(c_HOL_Oinverse__class_Oinverse(X1,X0),c_HOL_Ozero__class_Ozero(X0),X0)
| ~ class_Ring__and__Field_Odivision__by__zero(X0)
| ~ class_Ring__and__Field_Oordered__field(X0) ),
inference(cnf_transformation,[status(thm)],[f35]) ).
fof(f894,plain,
c_HOL_Otimes__class_Otimes(c_HOL_Ouminus__class_Ouminus(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Ouminus__class_Ouminus(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Oone__class_Oone(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f132]) ).
fof(f962,plain,
! [X0] :
( X0 = c_HOL_Oone__class_Oone(tc_RealDef_Oreal)
| X0 = c_HOL_Ouminus__class_Ouminus(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_HOL_Otimes__class_Otimes(X0,X0,tc_RealDef_Oreal) != c_HOL_Oone__class_Oone(tc_RealDef_Oreal) ),
inference(cnf_transformation,[status(thm)],[f172]) ).
fof(f1050,plain,
c_Transcendental_Ocos(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)) = c_HOL_Oone__class_Oone(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f228]) ).
fof(f1056,plain,
! [V_x] :
( V_x = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)
| ! [V_y] : c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_x,V_x,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(V_y,V_y,tc_RealDef_Oreal),tc_RealDef_Oreal) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
inference(miniscoping,[status(thm)],[f234]) ).
fof(f1057,plain,
! [X0,X1] :
( X0 = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)
| c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(X0,X0,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X1,X1,tc_RealDef_Oreal),tc_RealDef_Oreal) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
inference(cnf_transformation,[status(thm)],[f1056]) ).
fof(f1063,plain,
! [X0,X1] :
( ~ c_lessequals(c_HOL_Oabs__class_Oabs(X1,tc_RealDef_Oreal),X0,tc_RealDef_Oreal)
| c_lessequals(c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal),X1,tc_RealDef_Oreal) ),
inference(cnf_transformation,[status(thm)],[f239]) ).
fof(f1183,plain,
! [X0,X1] :
( X1 = c_HOL_Ozero__class_Ozero(X0)
| c_HOL_Ouminus__class_Ouminus(X1,X0) != X1
| ~ class_OrderedGroup_Oordered__ab__group__add(X0) ),
inference(cnf_transformation,[status(thm)],[f320]) ).
fof(f1307,plain,
! [X0] : c_HOL_Otimes__class_Otimes(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),X0,tc_RealDef_Oreal) = X0,
inference(cnf_transformation,[status(thm)],[f402]) ).
fof(f1322,plain,
( c_Transcendental_Oln(c_HOL_Oone__class_Oone(tc_RealDef_Oreal)) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(cnf_transformation,[status(thm)],[f416]) ).
fof(f1332,plain,
! [V_x] :
( V_x = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)
| ! [V_y] : c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_x,V_x,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(V_y,V_y,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(miniscoping,[status(thm)],[f426]) ).
fof(f1333,plain,
! [X0,X1] :
( X0 = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(X0,X0,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X1,X1,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(cnf_transformation,[status(thm)],[f1332]) ).
fof(f1334,plain,
! [V_y] :
( V_y = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)
| ! [V_x] : c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_x,V_x,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(V_y,V_y,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(miniscoping,[status(thm)],[f427]) ).
fof(f1335,plain,
! [X0,X1] :
( X1 = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(X0,X0,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X1,X1,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(cnf_transformation,[status(thm)],[f1334]) ).
fof(f1344,plain,
! [X0] :
( ~ c_HOL_Oord__class_Oless(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_HOL_Oabs__class_Oabs(X0,tc_RealDef_Oreal) = c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal) ),
inference(cnf_transformation,[status(thm)],[f435]) ).
fof(f1373,plain,
! [T_a] :
( ! [V_a] : c_lessequals(V_a,c_HOL_Oabs__class_Oabs(V_a,T_a),T_a)
| ~ class_OrderedGroup_Opordered__ab__group__add__abs(T_a) ),
inference(miniscoping,[status(thm)],[f459]) ).
fof(f1374,plain,
! [X0,X1] :
( c_lessequals(X1,c_HOL_Oabs__class_Oabs(X1,X0),X0)
| ~ class_OrderedGroup_Opordered__ab__group__add__abs(X0) ),
inference(cnf_transformation,[status(thm)],[f1373]) ).
fof(f1377,plain,
! [X0] :
( c_lessequals(c_HOL_Ozero__class_Ozero(X0),c_HOL_Oone__class_Oone(X0),X0)
| ~ class_Ring__and__Field_Oordered__semidom(X0) ),
inference(cnf_transformation,[status(thm)],[f462]) ).
fof(f1378,plain,
! [X0] : ~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(c_HOL_Oabs__class_Oabs(X0,tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),X0,tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f463]) ).
fof(f1383,plain,
! [X0] : ~ c_HOL_Oord__class_Oless(X0,X0,tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f466]) ).
fof(f1393,plain,
! [X0,X1] :
( ~ c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal)
| c_lessequals(X0,X1,tc_RealDef_Oreal) ),
inference(cnf_transformation,[status(thm)],[f473]) ).
fof(f1397,plain,
! [X0] :
( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(X0),c_HOL_Oone__class_Oone(X0),X0)
| ~ class_Ring__and__Field_Oordered__semidom(X0) ),
inference(cnf_transformation,[status(thm)],[f476]) ).
fof(f1400,plain,
! [X0] :
( c_HOL_Oord__class_Oless(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_HOL_Oabs__class_Oabs(X0,tc_RealDef_Oreal) = X0 ),
inference(cnf_transformation,[status(thm)],[f479]) ).
fof(f1423,plain,
! [V_i,V_j] :
( ~ c_lessequals(V_i,V_j,tc_RealDef_Oreal)
| ! [V_k] :
( ~ c_lessequals(V_j,V_k,tc_RealDef_Oreal)
| c_lessequals(V_i,V_k,tc_RealDef_Oreal) ) ),
inference(miniscoping,[status(thm)],[f493]) ).
fof(f1424,plain,
! [X0,X1,X2] :
( ~ c_lessequals(X0,X2,tc_RealDef_Oreal)
| ~ c_lessequals(X2,X1,tc_RealDef_Oreal)
| c_lessequals(X0,X1,tc_RealDef_Oreal) ),
inference(cnf_transformation,[status(thm)],[f1423]) ).
fof(f1425,plain,
! [X0] : c_lessequals(X0,X0,tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f494]) ).
fof(f1447,plain,
! [X0,X1] :
( c_lessequals(X1,X0,tc_RealDef_Oreal)
| c_lessequals(X0,X1,tc_RealDef_Oreal) ),
inference(cnf_transformation,[status(thm)],[f507]) ).
fof(f1457,plain,
c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) != c_HOL_Oone__class_Oone(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f514]) ).
fof(f1485,plain,
! [X0,X1] :
( ~ c_lessequals(X0,X1,tc_RealDef_Oreal)
| X0 = X1
| c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal) ),
inference(cnf_transformation,[status(thm)],[f533]) ).
fof(f1488,plain,
c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_r,tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f536]) ).
fof(f1489,plain,
! [X0] : c_lessequals(c_HOL_Oabs__class_Oabs(c_Complex_ORe(v_s(X0)),tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(v_r,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f537]) ).
fof(f1519,plain,
! [X0,X1] :
( ~ c_lessequals(X0,X1,tc_RealDef_Oreal)
| ~ c_lessequals(X1,X0,tc_RealDef_Oreal)
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f556]) ).
fof(f1586,plain,
! [T_a] :
( ! [V_a] : c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(T_a),V_a,T_a) = V_a
| ~ class_OrderedGroup_Omonoid__add(T_a) ),
inference(miniscoping,[status(thm)],[f601]) ).
fof(f1587,plain,
! [X0,X1] :
( c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(X0),X1,X0) = X1
| ~ class_OrderedGroup_Omonoid__add(X0) ),
inference(cnf_transformation,[status(thm)],[f1586]) ).
fof(f1606,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(v_r,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Oabs__class_Oabs(c_Complex_ORe(v_s(v_f____(v_x))),tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(v_r,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(cnf_transformation,[status(thm)],[f612]) ).
fof(f1613,plain,
class_OrderedGroup_Opordered__ab__group__add__abs(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f619]) ).
fof(f1618,plain,
class_Ring__and__Field_Oordered__ring__strict(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f624]) ).
fof(f1622,plain,
class_OrderedGroup_Oordered__ab__group__add(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f628]) ).
fof(f1629,plain,
class_Ring__and__Field_Odivision__by__zero(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f635]) ).
fof(f1630,plain,
class_Ring__and__Field_Oordered__semidom(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f636]) ).
fof(f1638,plain,
class_Ring__and__Field_Oordered__field(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f644]) ).
fof(f1652,plain,
class_OrderedGroup_Omonoid__add(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f658]) ).
fof(f1693,definition,
( sQ0_spl
<=> c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f1695,plain,
( sQ0_spl
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f1693]) ).
fof(f1696,definition,
( sQ1_spl
<=> c_Transcendental_Oln(c_HOL_Oone__class_Oone(tc_RealDef_Oreal)) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f1699,plain,
( sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f1322,f1693,f1696]) ).
fof(f1700,definition,
( sQ2_spl
<=> c_lessequals(c_HOL_Oabs__class_Oabs(c_Complex_ORe(v_s(v_f____(v_x))),tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(v_r,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f1702,plain,
( sQ2_spl
| ~ c_lessequals(c_HOL_Oabs__class_Oabs(c_Complex_ORe(v_s(v_f____(v_x))),tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(v_r,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f1700]) ).
fof(f1703,definition,
( sQ3_spl
<=> c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(v_r,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f1705,plain,
( sQ3_spl
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(v_r,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f1703]) ).
fof(f1706,plain,
( ~ sQ3_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f1606,f1700,f1703]) ).
fof(f1711,plain,
( c_HOL_Oone__class_Oone(tc_RealDef_Oreal) = c_HOL_Oone__class_Oone(tc_RealDef_Oreal)
| c_HOL_Oone__class_Oone(tc_RealDef_Oreal) = c_HOL_Ouminus__class_Ouminus(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f962,f1307]) ).
fof(f1714,plain,
( c_HOL_Ouminus__class_Ouminus(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Oone__class_Oone(tc_RealDef_Oreal)
| c_HOL_Ouminus__class_Ouminus(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Ouminus__class_Ouminus(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_HOL_Oone__class_Oone(tc_RealDef_Oreal) != c_HOL_Oone__class_Oone(tc_RealDef_Oreal) ),
inference(paramodulation,[status(thm)],[f894,f962]) ).
fof(f1715,definition,
( sQ4_spl
<=> c_HOL_Oone__class_Oone(tc_RealDef_Oreal) = c_HOL_Ouminus__class_Ouminus(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f1716,plain,
( ~ sQ4_spl
| c_HOL_Oone__class_Oone(tc_RealDef_Oreal) = c_HOL_Ouminus__class_Ouminus(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f1715]) ).
fof(f1718,definition,
( sQ5_spl
<=> c_HOL_Oone__class_Oone(tc_RealDef_Oreal) = c_HOL_Oone__class_Oone(tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f1721,plain,
( sQ5_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f1711,f1715,f1718]) ).
fof(f1722,definition,
( sQ6_spl
<=> c_HOL_Ouminus__class_Ouminus(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Ouminus__class_Ouminus(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f1727,plain,
( sQ4_spl
| sQ6_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f1714,f1718,f1722,f1715]) ).
fof(f1728,plain,
! [X0] :
( c_HOL_Oone__class_Oone(tc_RealDef_Oreal) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)
| c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X0,X0,tc_RealDef_Oreal),tc_RealDef_Oreal) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
inference(paramodulation,[status(thm)],[f1307,f1057]) ).
fof(f1732,definition,
! [X0] :
( sQ7_spl
<=> c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X0,X0,tc_RealDef_Oreal),tc_RealDef_Oreal) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f1735,definition,
( sQ8_spl
<=> c_HOL_Oone__class_Oone(tc_RealDef_Oreal) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f1736,plain,
( ~ sQ8_spl
| c_HOL_Oone__class_Oone(tc_RealDef_Oreal) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f1735]) ).
fof(f1738,plain,
( sQ8_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f1728,f1732,f1735]) ).
fof(f1753,plain,
( ~ c_lessequals(v_r,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| v_r = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f1519,f1488]) ).
fof(f1760,definition,
( sQ11_spl
<=> v_r = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f1761,plain,
( ~ sQ11_spl
| v_r = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f1760]) ).
fof(f1763,definition,
( sQ12_spl
<=> c_lessequals(v_r,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f1765,plain,
( sQ12_spl
| ~ c_lessequals(v_r,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f1763]) ).
fof(f1766,plain,
( ~ sQ12_spl
| sQ11_spl ),
inference(split_clause,[status(thm)],[f1753,f1760,f1763]) ).
fof(f1769,plain,
( ~ sQ11_spl
| v_r != c_HOL_Oone__class_Oone(tc_RealDef_Oreal) ),
inference(backward_demodulation,[status(thm)],[f1761,f1457]) ).
fof(f1778,definition,
( sQ14_spl
<=> c_HOL_Oone__class_Oone(tc_RealDef_Oreal) = v_r ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f1779,plain,
( ~ sQ14_spl
| c_HOL_Oone__class_Oone(tc_RealDef_Oreal) = v_r ),
inference(component_clause,[status(thm)],[f1778]) ).
fof(f1791,plain,
! [X0] :
( c_lessequals(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_HOL_Oabs__class_Oabs(X0,tc_RealDef_Oreal) = X0 ),
inference(resolution,[status(thm)],[f1400,f1393]) ).
fof(f1792,plain,
c_HOL_Oabs__class_Oabs(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(resolution,[status(thm)],[f1400,f1383]) ).
fof(f1805,plain,
( sQ3_spl
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(v_r,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(v_r,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f1705,f1485]) ).
fof(f1806,definition,
( sQ17_spl
<=> c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(v_r,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f1807,plain,
( ~ sQ17_spl
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(v_r,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f1806]) ).
fof(f1809,definition,
( sQ18_spl
<=> c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(v_r,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f1811,plain,
( sQ18_spl
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(v_r,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f1809]) ).
fof(f1812,plain,
( sQ3_spl
| ~ sQ18_spl
| sQ17_spl ),
inference(split_clause,[status(thm)],[f1805,f1806,f1809,f1703]) ).
fof(f1813,plain,
( sQ18_spl
| ~ sQ17_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)],[f1807,f1811]) ).
fof(f1814,plain,
( sQ18_spl
| ~ sQ17_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1813,f1425]) ).
fof(f1815,plain,
( sQ18_spl
| ~ sQ17_spl ),
inference(contradiction_clause,[status(thm)],[f1814]) ).
fof(f1821,plain,
( sQ12_spl
| c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal) = v_r ),
inference(resolution,[status(thm)],[f1791,f1765]) ).
fof(f1830,definition,
( sQ20_spl
<=> c_lessequals(c_HOL_Ouminus__class_Ouminus(c_HOL_Oplus__class_Oplus(v_r,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),c_Complex_ORe(v_s(v_f____(v_x))),tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f1831,plain,
( ~ sQ20_spl
| c_lessequals(c_HOL_Ouminus__class_Ouminus(c_HOL_Oplus__class_Oplus(v_r,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),c_Complex_ORe(v_s(v_f____(v_x))),tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f1830]) ).
fof(f1832,plain,
( sQ20_spl
| ~ c_lessequals(c_HOL_Ouminus__class_Ouminus(c_HOL_Oplus__class_Oplus(v_r,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),c_Complex_ORe(v_s(v_f____(v_x))),tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f1830]) ).
fof(f1844,plain,
( sQ18_spl
| c_lessequals(c_HOL_Oplus__class_Oplus(v_r,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f1811,f1447]) ).
fof(f1867,plain,
( sQ12_spl
| ~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(v_r,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),v_r,tc_RealDef_Oreal) ),
inference(paramodulation,[status(thm)],[f1821,f1378]) ).
fof(f1871,plain,
( sQ12_spl
| ~ c_lessequals(c_HOL_Oplus__class_Oplus(v_r,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),v_r,tc_RealDef_Oreal)
| c_HOL_Oplus__class_Oplus(v_r,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal) = v_r ),
inference(resolution,[status(thm)],[f1867,f1485]) ).
fof(f1872,definition,
( sQ21_spl
<=> c_HOL_Oplus__class_Oplus(v_r,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal) = v_r ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f1873,plain,
( ~ sQ21_spl
| c_HOL_Oplus__class_Oplus(v_r,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal) = v_r ),
inference(component_clause,[status(thm)],[f1872]) ).
fof(f1875,definition,
( sQ22_spl
<=> c_lessequals(c_HOL_Oplus__class_Oplus(v_r,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),v_r,tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f1877,plain,
( sQ22_spl
| ~ c_lessequals(c_HOL_Oplus__class_Oplus(v_r,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),v_r,tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f1875]) ).
fof(f1878,plain,
( sQ12_spl
| ~ sQ22_spl
| sQ21_spl ),
inference(split_clause,[status(thm)],[f1871,f1872,f1875,f1763]) ).
fof(f1971,plain,
( ~ sQ14_spl
| ~ sQ11_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1779,f1769]) ).
fof(f1972,plain,
( ~ sQ14_spl
| ~ sQ11_spl ),
inference(contradiction_clause,[status(thm)],[f1971]) ).
fof(f2015,plain,
! [X0] : ~ c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(X0,X0,tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(resolution,[status(thm)],[f723,f1618]) ).
fof(f2016,plain,
! [X0] :
( ~ sQ11_spl
| ~ c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(X0,X0,tc_RealDef_Oreal),v_r,tc_RealDef_Oreal) ),
inference(forward_demodulation,[status(thm)],[f1761,f2015]) ).
fof(f2031,plain,
( ~ sQ11_spl
| ~ c_HOL_Oord__class_Oless(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),v_r,tc_RealDef_Oreal) ),
inference(paramodulation,[status(thm)],[f1307,f2016]) ).
fof(f2032,plain,
( ~ sQ11_spl
| ~ c_lessequals(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),v_r,tc_RealDef_Oreal)
| c_HOL_Oone__class_Oone(tc_RealDef_Oreal) = v_r ),
inference(resolution,[status(thm)],[f2031,f1485]) ).
fof(f2033,definition,
( sQ30_spl
<=> c_lessequals(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),v_r,tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f2035,plain,
( sQ30_spl
| ~ c_lessequals(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),v_r,tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f2033]) ).
fof(f2036,plain,
( ~ sQ11_spl
| ~ sQ30_spl
| sQ14_spl ),
inference(split_clause,[status(thm)],[f2032,f1778,f2033,f1760]) ).
fof(f2038,plain,
( sQ30_spl
| c_lessequals(v_r,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f2035,f1447]) ).
fof(f2082,plain,
( sQ20_spl
| ~ c_lessequals(c_HOL_Oabs__class_Oabs(c_Complex_ORe(v_s(v_f____(v_x))),tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(v_r,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f1832,f1063]) ).
fof(f2103,plain,
( sQ2_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f1702,f1489]) ).
fof(f2105,plain,
sQ2_spl,
inference(contradiction_clause,[status(thm)],[f2103]) ).
fof(f2106,plain,
( sQ20_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f2082,f1700,f1830]) ).
fof(f2113,plain,
! [X0] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Oinverse__class_Oinverse(X0,tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ class_Ring__and__Field_Odivision__by__zero(tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f729,f1638]) ).
fof(f2114,definition,
( sQ31_spl
<=> class_Ring__and__Field_Odivision__by__zero(tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f2116,plain,
( sQ31_spl
| ~ class_Ring__and__Field_Odivision__by__zero(tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f2114]) ).
fof(f2117,definition,
! [X0] :
( sQ32_spl
<=> ( ~ c_HOL_Oord__class_Oless(c_HOL_Oinverse__class_Oinverse(X0,tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) ) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f2120,plain,
( sQ32_spl
| ~ sQ31_spl ),
inference(split_clause,[status(thm)],[f2113,f2114,f2117]) ).
fof(f2121,plain,
( sQ31_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2116,f1629]) ).
fof(f2122,plain,
sQ31_spl,
inference(contradiction_clause,[status(thm)],[f2121]) ).
fof(f2123,plain,
! [X0] :
( ~ c_HOL_Oord__class_Oless(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(c_HOL_Oinverse__class_Oinverse(X0,tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ class_Ring__and__Field_Odivision__by__zero(tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f730,f1638]) ).
fof(f2124,definition,
! [X0] :
( sQ33_spl
<=> ( ~ c_HOL_Oord__class_Oless(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(c_HOL_Oinverse__class_Oinverse(X0,tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) ) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f2127,plain,
( sQ33_spl
| ~ sQ31_spl ),
inference(split_clause,[status(thm)],[f2123,f2114,f2124]) ).
fof(f2142,plain,
( sQ12_spl
| ~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(v_r,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),v_r,tc_RealDef_Oreal) ),
inference(paramodulation,[status(thm)],[f1821,f1378]) ).
fof(f2144,plain,
( sQ12_spl
| ~ sQ17_spl
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_r,tc_RealDef_Oreal) ),
inference(forward_demodulation,[status(thm)],[f1807,f2142]) ).
fof(f2147,plain,
! [X0] :
( sQ12_spl
| ~ c_lessequals(v_r,X0,tc_RealDef_Oreal)
| ~ c_lessequals(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f1765,f1424]) ).
fof(f2151,plain,
( sQ12_spl
| ~ sQ17_spl
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_r,tc_RealDef_Oreal)
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = v_r ),
inference(resolution,[status(thm)],[f2144,f1485]) ).
fof(f2152,definition,
( sQ35_spl
<=> c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_r,tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f2154,plain,
( sQ35_spl
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_r,tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f2152]) ).
fof(f2155,plain,
( sQ12_spl
| ~ sQ17_spl
| ~ sQ35_spl
| sQ11_spl ),
inference(split_clause,[status(thm)],[f2151,f1760,f2152,f1806,f1763]) ).
fof(f2156,plain,
( sQ35_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2154,f1488]) ).
fof(f2157,plain,
sQ35_spl,
inference(contradiction_clause,[status(thm)],[f2156]) ).
fof(f2184,plain,
( ~ sQ11_spl
| v_r != c_Transcendental_Ocos(v_r) ),
inference(backward_demodulation,[status(thm)],[f2193,f1769]) ).
fof(f2193,plain,
( ~ sQ11_spl
| c_Transcendental_Ocos(v_r) = c_HOL_Oone__class_Oone(tc_RealDef_Oreal) ),
inference(forward_demodulation,[status(thm)],[f1761,f1050]) ).
fof(f2214,definition,
( sQ36_spl
<=> c_Transcendental_Ocos(v_r) = v_r ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f2215,plain,
( ~ sQ36_spl
| c_Transcendental_Ocos(v_r) = v_r ),
inference(component_clause,[status(thm)],[f2214]) ).
fof(f2221,plain,
( ~ sQ36_spl
| ~ sQ11_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2215,f2184]) ).
fof(f2222,plain,
( ~ sQ36_spl
| ~ sQ11_spl ),
inference(contradiction_clause,[status(thm)],[f2221]) ).
fof(f2385,plain,
! [X0] : c_lessequals(X0,c_HOL_Oabs__class_Oabs(X0,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(resolution,[status(thm)],[f1374,f1613]) ).
fof(f2386,plain,
! [X0] :
( ~ c_lessequals(c_HOL_Oabs__class_Oabs(X0,tc_RealDef_Oreal),X0,tc_RealDef_Oreal)
| c_HOL_Oabs__class_Oabs(X0,tc_RealDef_Oreal) = X0 ),
inference(resolution,[status(thm)],[f2385,f1519]) ).
fof(f2398,plain,
! [X0] : c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal) = X0,
inference(resolution,[status(thm)],[f1587,f1652]) ).
fof(f2399,plain,
! [X0] :
( ~ sQ11_spl
| c_HOL_Oplus__class_Oplus(v_r,X0,tc_RealDef_Oreal) = X0 ),
inference(forward_demodulation,[status(thm)],[f1761,f2398]) ).
fof(f2558,plain,
! [X0] :
( ~ c_lessequals(c_HOL_Oinverse__class_Oinverse(X0,tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_lessequals(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ class_Ring__and__Field_Odivision__by__zero(tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f740,f1638]) ).
fof(f2559,definition,
! [X0] :
( sQ46_spl
<=> ( ~ c_lessequals(c_HOL_Oinverse__class_Oinverse(X0,tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_lessequals(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) ) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f2562,plain,
( sQ46_spl
| ~ sQ31_spl ),
inference(split_clause,[status(thm)],[f2558,f2114,f2559]) ).
fof(f2563,plain,
! [X0] :
( ~ c_lessequals(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_lessequals(c_HOL_Oinverse__class_Oinverse(X0,tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ class_Ring__and__Field_Odivision__by__zero(tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f741,f1638]) ).
fof(f2564,definition,
! [X0] :
( sQ47_spl
<=> ( ~ c_lessequals(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_lessequals(c_HOL_Oinverse__class_Oinverse(X0,tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) ) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f2567,plain,
( sQ47_spl
| ~ sQ31_spl ),
inference(split_clause,[status(thm)],[f2563,f2114,f2564]) ).
fof(f2575,plain,
( ~ sQ20_spl
| ~ c_lessequals(c_Complex_ORe(v_s(v_f____(v_x))),c_HOL_Ouminus__class_Ouminus(c_HOL_Oplus__class_Oplus(v_r,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_Complex_ORe(v_s(v_f____(v_x))) = c_HOL_Ouminus__class_Ouminus(c_HOL_Oplus__class_Oplus(v_r,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f1831,f1519]) ).
fof(f2576,definition,
( sQ48_spl
<=> c_Complex_ORe(v_s(v_f____(v_x))) = c_HOL_Ouminus__class_Ouminus(c_HOL_Oplus__class_Oplus(v_r,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f2579,definition,
( sQ49_spl
<=> c_lessequals(c_Complex_ORe(v_s(v_f____(v_x))),c_HOL_Ouminus__class_Ouminus(c_HOL_Oplus__class_Oplus(v_r,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f2582,plain,
( ~ sQ20_spl
| ~ sQ49_spl
| sQ48_spl ),
inference(split_clause,[status(thm)],[f2575,f2576,f2579,f1830]) ).
fof(f2584,plain,
( sQ18_spl
| ~ sQ21_spl
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_r,tc_RealDef_Oreal) ),
inference(backward_demodulation,[status(thm)],[f1873,f1811]) ).
fof(f2591,plain,
( sQ18_spl
| ~ sQ21_spl
| ~ sQ35_spl ),
inference(split_clause,[status(thm)],[f2584,f2152,f1872,f1809]) ).
fof(f2631,plain,
( sQ30_spl
| ~ sQ11_spl
| c_lessequals(v_r,c_Transcendental_Ocos(v_r),tc_RealDef_Oreal) ),
inference(forward_demodulation,[status(thm)],[f2193,f2038]) ).
fof(f2656,plain,
( sQ3_spl
| ~ sQ11_spl
| ~ c_HOL_Oord__class_Oless(v_r,c_HOL_Oplus__class_Oplus(v_r,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(forward_demodulation,[status(thm)],[f1761,f1705]) ).
fof(f2657,plain,
( sQ3_spl
| ~ sQ11_spl
| ~ c_HOL_Oord__class_Oless(v_r,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(forward_demodulation,[status(thm)],[f2399,f2656]) ).
fof(f2658,plain,
( sQ3_spl
| ~ sQ11_spl
| ~ c_HOL_Oord__class_Oless(v_r,c_Transcendental_Ocos(v_r),tc_RealDef_Oreal) ),
inference(forward_demodulation,[status(thm)],[f2193,f2657]) ).
fof(f2659,plain,
( sQ3_spl
| ~ sQ11_spl
| ~ c_lessequals(v_r,c_Transcendental_Ocos(v_r),tc_RealDef_Oreal)
| v_r = c_Transcendental_Ocos(v_r) ),
inference(resolution,[status(thm)],[f2658,f1485]) ).
fof(f2660,definition,
( sQ51_spl
<=> c_lessequals(v_r,c_Transcendental_Ocos(v_r),tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f2662,plain,
( sQ51_spl
| ~ c_lessequals(v_r,c_Transcendental_Ocos(v_r),tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f2660]) ).
fof(f2663,plain,
( sQ3_spl
| ~ sQ11_spl
| ~ sQ51_spl
| sQ36_spl ),
inference(split_clause,[status(thm)],[f2659,f2214,f2660,f1760,f1703]) ).
fof(f2664,plain,
( sQ51_spl
| sQ30_spl
| ~ sQ11_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2662,f2631]) ).
fof(f2665,plain,
( sQ51_spl
| sQ30_spl
| ~ sQ11_spl ),
inference(contradiction_clause,[status(thm)],[f2664]) ).
fof(f2755,plain,
! [X0] :
( c_HOL_Oabs__class_Oabs(X0,tc_RealDef_Oreal) = c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal)
| c_HOL_Oabs__class_Oabs(X0,tc_RealDef_Oreal) = X0 ),
inference(resolution,[status(thm)],[f1400,f1344]) ).
fof(f2769,plain,
( ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_HOL_Oabs__class_Oabs(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
inference(paramodulation,[status(thm)],[f1792,f2386]) ).
fof(f2774,definition,
( sQ52_spl
<=> c_HOL_Oabs__class_Oabs(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f2781,definition,
( sQ54_spl
<=> c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f2783,plain,
( sQ54_spl
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f2781]) ).
fof(f2784,plain,
( ~ sQ54_spl
| sQ52_spl ),
inference(split_clause,[status(thm)],[f2769,f2774,f2781]) ).
fof(f2788,definition,
( sQ56_spl
<=> c_lessequals(v_r,v_r,tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f2790,plain,
( sQ56_spl
| ~ c_lessequals(v_r,v_r,tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f2788]) ).
fof(f2834,plain,
! [X0] :
( X0 = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)
| c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal) != X0 ),
inference(resolution,[status(thm)],[f1183,f1622]) ).
fof(f2836,plain,
( ~ sQ4_spl
| c_HOL_Oone__class_Oone(tc_RealDef_Oreal) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f2834,f1716]) ).
fof(f2841,plain,
( ~ sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2836,f1457]) ).
fof(f2842,plain,
~ sQ4_spl,
inference(contradiction_clause,[status(thm)],[f2841]) ).
fof(f2843,plain,
( sQ56_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2790,f1425]) ).
fof(f2844,plain,
sQ56_spl,
inference(contradiction_clause,[status(thm)],[f2843]) ).
fof(f2845,plain,
( sQ54_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2783,f1425]) ).
fof(f2846,plain,
sQ54_spl,
inference(contradiction_clause,[status(thm)],[f2845]) ).
fof(f2863,plain,
! [X0] :
( sQ12_spl
| c_lessequals(X0,v_r,tc_RealDef_Oreal)
| ~ c_lessequals(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f2147,f1447]) ).
fof(f2873,plain,
( ~ sQ20_spl
| c_HOL_Oabs__class_Oabs(c_HOL_Oplus__class_Oplus(v_r,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(v_r,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_lessequals(c_HOL_Oabs__class_Oabs(c_HOL_Oplus__class_Oplus(v_r,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),c_Complex_ORe(v_s(v_f____(v_x))),tc_RealDef_Oreal) ),
inference(paramodulation,[status(thm)],[f2755,f1831]) ).
fof(f2888,definition,
( sQ57_spl
<=> c_HOL_Oone__class_Oone(tc_RealDef_Oreal) = c_HOL_Oabs__class_Oabs(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f2892,definition,
( sQ58_spl
<=> c_lessequals(c_HOL_Oabs__class_Oabs(c_HOL_Oplus__class_Oplus(v_r,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),c_Complex_ORe(v_s(v_f____(v_x))),tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f2895,definition,
( sQ59_spl
<=> c_HOL_Oabs__class_Oabs(c_HOL_Oplus__class_Oplus(v_r,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(v_r,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f2898,plain,
( ~ sQ20_spl
| sQ59_spl
| sQ58_spl ),
inference(split_clause,[status(thm)],[f2873,f2892,f2895,f1830]) ).
fof(f2924,plain,
! [X0] :
( c_HOL_Oone__class_Oone(tc_RealDef_Oreal) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X0,X0,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(paramodulation,[status(thm)],[f1307,f1333]) ).
fof(f2936,definition,
! [X0] :
( sQ65_spl
<=> c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X0,X0,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f2939,plain,
( sQ8_spl
| sQ65_spl ),
inference(split_clause,[status(thm)],[f2924,f2936,f1735]) ).
fof(f2949,plain,
! [X0] :
( c_HOL_Oone__class_Oone(tc_RealDef_Oreal) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(X0,X0,tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(paramodulation,[status(thm)],[f1307,f1335]) ).
fof(f2956,definition,
! [X0] :
( sQ67_spl
<=> c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(X0,X0,tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition]) ).
fof(f2959,plain,
( sQ8_spl
| sQ67_spl ),
inference(split_clause,[status(thm)],[f2949,f2956,f1735]) ).
fof(f2961,plain,
( ~ sQ8_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1736,f1457]) ).
fof(f2962,plain,
~ sQ8_spl,
inference(contradiction_clause,[status(thm)],[f2961]) ).
fof(f2970,plain,
( ~ c_lessequals(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_HOL_Oone__class_Oone(tc_RealDef_Oreal) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)
| ~ class_Ring__and__Field_Oordered__semidom(tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f1377,f1519]) ).
fof(f2971,definition,
( sQ68_spl
<=> class_Ring__and__Field_Oordered__semidom(tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition]) ).
fof(f2973,plain,
( sQ68_spl
| ~ class_Ring__and__Field_Oordered__semidom(tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f2971]) ).
fof(f2974,definition,
( sQ69_spl
<=> c_lessequals(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition]) ).
fof(f2976,plain,
( sQ69_spl
| ~ c_lessequals(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f2974]) ).
fof(f2977,plain,
( ~ sQ69_spl
| sQ8_spl
| ~ sQ68_spl ),
inference(split_clause,[status(thm)],[f2970,f2971,f1735,f2974]) ).
fof(f2978,plain,
( sQ68_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2973,f1630]) ).
fof(f2979,plain,
sQ68_spl,
inference(contradiction_clause,[status(thm)],[f2978]) ).
fof(f2981,plain,
( c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ class_Ring__and__Field_Oordered__semidom(tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f1397,f1393]) ).
fof(f2982,definition,
( sQ70_spl
<=> c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f2985,plain,
( sQ70_spl
| ~ sQ68_spl ),
inference(split_clause,[status(thm)],[f2981,f2971,f2982]) ).
fof(f2989,plain,
( sQ0_spl
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_HOL_Oone__class_Oone(tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f1695,f1485]) ).
fof(f2991,plain,
( sQ0_spl
| ~ sQ70_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f2989,f1735,f2982,f1693]) ).
fof(f3042,plain,
( sQ69_spl
| c_HOL_Oabs__class_Oabs(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Oone__class_Oone(tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f2976,f1791]) ).
fof(f3048,plain,
( sQ69_spl
| ~ c_lessequals(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_HOL_Oabs__class_Oabs(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Oone__class_Oone(tc_RealDef_Oreal) ),
inference(paramodulation,[status(thm)],[f3042,f2386]) ).
fof(f3051,definition,
( sQ75_spl
<=> c_lessequals(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).
fof(f3054,plain,
( sQ69_spl
| ~ sQ75_spl
| sQ57_spl ),
inference(split_clause,[status(thm)],[f3048,f2888,f3051,f2974]) ).
fof(f3056,plain,
( sQ22_spl
| sQ12_spl
| ~ c_lessequals(c_HOL_Oplus__class_Oplus(v_r,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f2863,f1877]) ).
fof(f3065,plain,
( sQ22_spl
| sQ12_spl
| sQ18_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3056,f1844]) ).
fof(f3066,plain,
( sQ22_spl
| sQ12_spl
| sQ18_spl ),
inference(contradiction_clause,[status(thm)],[f3065]) ).
fof(f3067,plain,
$false,
inference(sat_refutation,[status(thm)],[f1699,f1706,f1721,f1727,f1738,f1766,f1812,f1815,f1878,f1972,f2036,f2105,f2106,f2120,f2122,f2127,f2155,f2157,f2222,f2562,f2567,f2582,f2591,f2663,f2665,f2784,f2842,f2844,f2846,f2898,f2939,f2959,f2962,f2977,f2979,f2985,f2991,f3054,f3066]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG363-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/5.36 % Computer : n004.cluster.edu
% 0.08/5.36 % Model : x86_64 x86_64
% 0.08/5.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/5.36 % Memory : 8046.5625MB
% 0.08/5.36 % OS : Linux 6.8.0-71-generic
% 0.08/5.36 % CPULimit : 300
% 0.08/5.36 % WCLimit : 300
% 0.08/5.36 % DateTime : Mon Sep 21 13:17:40 UTC 2026
% 0.08/5.37 % CPUTime :
% 0.13/5.41 % Drodi V4.1.1
% 0.13/5.57 % Refutation found
% 0.13/5.57 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.13/5.57 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.13/5.59 % Elapsed time: 0.213750 seconds
% 0.13/5.59 % CPU time: 1.268009 seconds
% 0.13/5.59 % Total memory used: 155.489 MB
% 0.13/5.59 % Net memory used: 154.396 MB
%------------------------------------------------------------------------------