%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : ALG339-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 : n003.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:13 AM UTC 2026
% Result : Unsatisfiable 126.67s 16.62s
% Output : CNFRefutation 126.67s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 124
% Syntax : Number of formulae : 475 ( 177 unt; 70 def)
% Number of atoms : 831 ( 114 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 690 ( 334 ~; 286 |; 0 &)
% ( 70 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 88 ( 86 usr; 71 prp; 0-3 aty)
% Number of functors : 19 ( 19 usr; 8 con; 0-3 aty)
% Number of variables : 211 ( 211 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f31,axiom,
! [T_a,V_x] :
( V_x = c_HOL_Ozero__class_Ozero(T_a)
| c_HOL_Osgn__class_Osgn(V_x,T_a) != c_HOL_Ozero__class_Ozero(T_a)
| ~ class_RealVector_Oreal__normed__vector(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f67,axiom,
! [T_a,V_b] :
( c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(T_a),V_b,T_a) = c_HOL_Ozero__class_Ozero(T_a)
| ~ class_Ring__and__Field_Oring__no__zero__divisors(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f118,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(f129,axiom,
! [T_a,V_x] :
( c_HOL_Otimes__class_Otimes(c_HOL_Osgn__class_Osgn(V_x,T_a),c_HOL_Oabs__class_Oabs(V_x,T_a),T_a) = V_x
| ~ class_Ring__and__Field_Oordered__idom(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f191,axiom,
c_Transcendental_Opi != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f192,axiom,
c_NthRoot_Osqrt(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f196,axiom,
! [V_x] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_x,tc_RealDef_Oreal)
| c_Transcendental_Oexp(c_Transcendental_Oln(V_x),tc_RealDef_Oreal) = V_x ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f273,axiom,
! [V_z1,V_z2,V_z3] : c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(V_z1,V_z2,tc_RealDef_Oreal),V_z3,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(V_z1,c_HOL_Otimes__class_Otimes(V_z2,V_z3,tc_RealDef_Oreal),tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f307,axiom,
! [V_y] : c_Transcendental_Oln(c_Transcendental_Oexp(V_y,tc_RealDef_Oreal)) = V_y,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f352,axiom,
! [V_x] : c_NthRoot_Osqrt(c_HOL_Otimes__class_Otimes(V_x,V_x,tc_RealDef_Oreal)) = c_HOL_Oabs__class_Oabs(V_x,tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f400,axiom,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f401,axiom,
! [V_x] :
( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(V_x,V_x,tc_RealDef_Oreal),tc_RealDef_Oreal)
| V_x = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f402,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/sandbox/benchmark/theBenchmark.p') ).
fof(f404,axiom,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Complex_Osko__Complex__XRe__Xpos__bounded__1__1,tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f405,axiom,
! [T_a,V_y] :
( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Osko__RealVector__Xmult__left__Xpos__bounded__1__1(V_y,T_a),tc_RealDef_Oreal)
| ~ class_RealVector_Oreal__normed__algebra(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f406,axiom,
~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(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),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f408,axiom,
! [V_m] : c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealDef_Oreal__of__preal(V_m),tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f412,axiom,
! [V_d1,V_d2] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_d1,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_d2,tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealDef_Osko__RealDef__Xreal__lbound__gt__zero__1__1(V_d1,V_d2),tc_RealDef_Oreal) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f421,axiom,
! [V_x] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_x,tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(c_Transcendental_Oln(V_x),V_x,tc_RealDef_Oreal) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f428,axiom,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Complex_Osko__Complex__XIm__Xpos__bounded__1__1,tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f429,axiom,
! [V_x] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_x,tc_RealDef_Oreal)
| c_NthRoot_Osqrt(V_x) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f431,axiom,
! [V_x,V_y] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_x,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_y,tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(V_x,V_y,tc_RealDef_Oreal),tc_RealDef_Oreal) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f432,axiom,
! [V_d1,V_d2] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_d1,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_d2,tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(c_RealDef_Osko__RealDef__Xreal__lbound__gt__zero__1__1(V_d1,V_d2),V_d2,tc_RealDef_Oreal) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f433,axiom,
! [V_d1,V_d2] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_d1,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_d2,tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(c_RealDef_Osko__RealDef__Xreal__lbound__gt__zero__1__1(V_d1,V_d2),V_d1,tc_RealDef_Oreal) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f439,axiom,
~ c_HOL_Oord__class_Oless(c_Transcendental_Opi,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f440,axiom,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Complex_Osko__Complex__Xcnj__Xpos__bounded__1__1,tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f442,axiom,
! [V_z,V_x,V_y] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_z,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(V_x,V_y,tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(V_z,V_x,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(V_z,V_y,tc_RealDef_Oreal),tc_RealDef_Oreal) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f445,axiom,
! [V_x] : c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Transcendental_Oexp(V_x,tc_RealDef_Oreal),tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f446,axiom,
! [T_a,V_x] :
( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Osko__RealVector__XscaleR__left__Xpos__bounded__1__1(V_x,T_a),tc_RealDef_Oreal)
| ~ class_RealVector_Oreal__normed__vector(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f450,axiom,
! [T_a,V_x,V_y] :
( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f454,axiom,
! [V_x] : ~ c_HOL_Oord__class_Oless(V_x,V_x,tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f464,negated_conjecture,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_d1,tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f465,negated_conjecture,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_d2,tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f466,negated_conjecture,
! [V_x] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_x,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(V_x,v_d1,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(V_x,v_d2,tc_RealDef_Oreal) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f474,axiom,
class_Ring__and__Field_Ono__zero__divisors(tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f475,axiom,
class_Ring__and__Field_Oordered__semidom(tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f482,axiom,
class_Ring__and__Field_Ozero__neq__one(tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f483,axiom,
class_Ring__and__Field_Omult__zero(tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f491,axiom,
class_Power_Opower(tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f496,axiom,
class_Ring__and__Field_Oordered__semiring__strict(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f500,axiom,
class_Ring__and__Field_Oring__no__zero__divisors(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f509,axiom,
class_Ring__and__Field_Ono__zero__divisors(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f511,axiom,
class_Ring__and__Field_Oordered__semidom(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f513,axiom,
class_RealVector_Oreal__normed__algebra(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f515,axiom,
class_RealVector_Oreal__normed__vector(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f518,axiom,
class_Ring__and__Field_Oordered__field(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f519,axiom,
class_Ring__and__Field_Odivision__ring(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f523,axiom,
class_Ring__and__Field_Ozero__neq__one(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f524,axiom,
class_Ring__and__Field_Oordered__idom(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f525,axiom,
class_RealVector_Oreal__algebra__1(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f527,axiom,
class_Ring__and__Field_Omult__zero(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f540,axiom,
class_Nat_Osemiring__char__0(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f542,axiom,
class_Orderings_Olinorder(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f545,axiom,
class_Power_Opower(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f596,plain,
! [X0,X1] :
( ~ class_RealVector_Oreal__normed__vector(X1)
| c_HOL_Ozero__class_Ozero(X1) != c_HOL_Osgn__class_Osgn(X0,X1)
| X0 = c_HOL_Ozero__class_Ozero(X1) ),
inference(cnf_transformation,[status(thm)],[f31]) ).
fof(f654,plain,
! [T_a] :
( ! [V_b] : c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(T_a),V_b,T_a) = c_HOL_Ozero__class_Ozero(T_a)
| ~ class_Ring__and__Field_Oring__no__zero__divisors(T_a) ),
inference(miniscoping,[status(thm)],[f67]) ).
fof(f655,plain,
! [X0,X1] :
( c_HOL_Ozero__class_Ozero(X0) = c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(X0),X1,X0)
| ~ class_Ring__and__Field_Oring__no__zero__divisors(X0) ),
inference(cnf_transformation,[status(thm)],[f654]) ).
fof(f746,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)],[f118]) ).
fof(f767,plain,
! [T_a] :
( ! [V_x] : c_HOL_Otimes__class_Otimes(c_HOL_Osgn__class_Osgn(V_x,T_a),c_HOL_Oabs__class_Oabs(V_x,T_a),T_a) = V_x
| ~ class_Ring__and__Field_Oordered__idom(T_a) ),
inference(miniscoping,[status(thm)],[f129]) ).
fof(f768,plain,
! [X0,X1] :
( ~ class_Ring__and__Field_Oordered__idom(X1)
| X0 = c_HOL_Otimes__class_Otimes(c_HOL_Osgn__class_Osgn(X0,X1),c_HOL_Oabs__class_Oabs(X0,X1),X1) ),
inference(cnf_transformation,[status(thm)],[f767]) ).
fof(f873,plain,
c_Transcendental_Opi != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f874,plain,
c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_NthRoot_Osqrt(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)),
inference(cnf_transformation,[status(thm)],[f192]) ).
fof(f880,plain,
! [X0] :
( X0 = c_Transcendental_Oexp(c_Transcendental_Oln(X0),tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal) ),
inference(cnf_transformation,[status(thm)],[f196]) ).
fof(f994,plain,
! [X0,X1,X2] : c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(X0,X1,tc_RealDef_Oreal),X2,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(X0,c_HOL_Otimes__class_Otimes(X1,X2,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f273]) ).
fof(f1061,plain,
! [X0] : c_Transcendental_Oln(c_Transcendental_Oexp(X0,tc_RealDef_Oreal)) = X0,
inference(cnf_transformation,[status(thm)],[f307]) ).
fof(f1143,plain,
! [X0] : c_HOL_Oabs__class_Oabs(X0,tc_RealDef_Oreal) = c_NthRoot_Osqrt(c_HOL_Otimes__class_Otimes(X0,X0,tc_RealDef_Oreal)),
inference(cnf_transformation,[status(thm)],[f352]) ).
fof(f1222,plain,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f400]) ).
fof(f1223,plain,
! [X0] :
( X0 = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X0,X0,tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(cnf_transformation,[status(thm)],[f401]) ).
fof(f1224,plain,
! [X0] :
( c_HOL_Oabs__class_Oabs(X0,tc_RealDef_Oreal) = X0
| c_HOL_Oord__class_Oless(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(cnf_transformation,[status(thm)],[f402]) ).
fof(f1227,plain,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Complex_Osko__Complex__XRe__Xpos__bounded__1__1,tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f404]) ).
fof(f1228,plain,
! [T_a] :
( ! [V_y] : c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Osko__RealVector__Xmult__left__Xpos__bounded__1__1(V_y,T_a),tc_RealDef_Oreal)
| ~ class_RealVector_Oreal__normed__algebra(T_a) ),
inference(miniscoping,[status(thm)],[f405]) ).
fof(f1229,plain,
! [X0,X1] :
( ~ class_RealVector_Oreal__normed__algebra(X1)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Osko__RealVector__Xmult__left__Xpos__bounded__1__1(X0,X1),tc_RealDef_Oreal) ),
inference(cnf_transformation,[status(thm)],[f1228]) ).
fof(f1230,plain,
~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(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),
inference(cnf_transformation,[status(thm)],[f406]) ).
fof(f1233,plain,
! [X0] : c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealDef_Oreal__of__preal(X0),tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f408]) ).
fof(f1238,plain,
! [V_d1] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_d1,tc_RealDef_Oreal)
| ! [V_d2] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_d2,tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealDef_Osko__RealDef__Xreal__lbound__gt__zero__1__1(V_d1,V_d2),tc_RealDef_Oreal) ) ),
inference(miniscoping,[status(thm)],[f412]) ).
fof(f1239,plain,
! [X0,X1] :
( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealDef_Osko__RealDef__Xreal__lbound__gt__zero__1__1(X1,X0),tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X1,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal) ),
inference(cnf_transformation,[status(thm)],[f1238]) ).
fof(f1252,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_Transcendental_Oln(X0),X0,tc_RealDef_Oreal) ),
inference(cnf_transformation,[status(thm)],[f421]) ).
fof(f1265,plain,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Complex_Osko__Complex__XIm__Xpos__bounded__1__1,tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f428]) ).
fof(f1266,plain,
! [X0] :
( c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) != c_NthRoot_Osqrt(X0)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal) ),
inference(cnf_transformation,[status(thm)],[f429]) ).
fof(f1268,plain,
! [V_x] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_x,tc_RealDef_Oreal)
| ! [V_y] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_y,tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(V_x,V_y,tc_RealDef_Oreal),tc_RealDef_Oreal) ) ),
inference(miniscoping,[status(thm)],[f431]) ).
fof(f1269,plain,
! [X0,X1] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X1,tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X1,X0,tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal) ),
inference(cnf_transformation,[status(thm)],[f1268]) ).
fof(f1270,plain,
! [V_d1] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_d1,tc_RealDef_Oreal)
| ! [V_d2] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_d2,tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(c_RealDef_Osko__RealDef__Xreal__lbound__gt__zero__1__1(V_d1,V_d2),V_d2,tc_RealDef_Oreal) ) ),
inference(miniscoping,[status(thm)],[f432]) ).
fof(f1271,plain,
! [X0,X1] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X1,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(c_RealDef_Osko__RealDef__Xreal__lbound__gt__zero__1__1(X0,X1),X1,tc_RealDef_Oreal) ),
inference(cnf_transformation,[status(thm)],[f1270]) ).
fof(f1272,plain,
! [V_d1] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_d1,tc_RealDef_Oreal)
| ! [V_d2] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_d2,tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(c_RealDef_Osko__RealDef__Xreal__lbound__gt__zero__1__1(V_d1,V_d2),V_d1,tc_RealDef_Oreal) ) ),
inference(miniscoping,[status(thm)],[f433]) ).
fof(f1273,plain,
! [X0,X1] :
( c_HOL_Oord__class_Oless(c_RealDef_Osko__RealDef__Xreal__lbound__gt__zero__1__1(X1,X0),X1,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X1,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal) ),
inference(cnf_transformation,[status(thm)],[f1272]) ).
fof(f1281,plain,
~ c_HOL_Oord__class_Oless(c_Transcendental_Opi,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f439]) ).
fof(f1282,plain,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Complex_Osko__Complex__Xcnj__Xpos__bounded__1__1,tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f440]) ).
fof(f1285,plain,
! [V_z] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_z,tc_RealDef_Oreal)
| ! [V_x,V_y] :
( ~ c_HOL_Oord__class_Oless(V_x,V_y,tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(V_z,V_x,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(V_z,V_y,tc_RealDef_Oreal),tc_RealDef_Oreal) ) ),
inference(miniscoping,[status(thm)],[f442]) ).
fof(f1286,plain,
! [X0,X1,X2] :
( ~ c_HOL_Oord__class_Oless(X1,X2,tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(X0,X1,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X0,X2,tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal) ),
inference(cnf_transformation,[status(thm)],[f1285]) ).
fof(f1291,plain,
! [X0] : c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Transcendental_Oexp(X0,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f445]) ).
fof(f1292,plain,
! [T_a] :
( ! [V_x] : c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Osko__RealVector__XscaleR__left__Xpos__bounded__1__1(V_x,T_a),tc_RealDef_Oreal)
| ~ class_RealVector_Oreal__normed__vector(T_a) ),
inference(miniscoping,[status(thm)],[f446]) ).
fof(f1293,plain,
! [X0,X1] :
( ~ class_RealVector_Oreal__normed__vector(X1)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Osko__RealVector__XscaleR__left__Xpos__bounded__1__1(X0,X1),tc_RealDef_Oreal) ),
inference(cnf_transformation,[status(thm)],[f1292]) ).
fof(f1297,plain,
! [X0,X1,X2] :
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(thm)],[f450]) ).
fof(f1302,plain,
! [X0] : ~ c_HOL_Oord__class_Oless(X0,X0,tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f454]) ).
fof(f1318,plain,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_d1,tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f464]) ).
fof(f1319,plain,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_d2,tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f465]) ).
fof(f1320,plain,
! [X0] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(X0,v_d2,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(X0,v_d1,tc_RealDef_Oreal) ),
inference(cnf_transformation,[status(thm)],[f466]) ).
fof(f1328,plain,
class_Ring__and__Field_Ono__zero__divisors(tc_nat),
inference(cnf_transformation,[status(thm)],[f474]) ).
fof(f1329,plain,
class_Ring__and__Field_Oordered__semidom(tc_nat),
inference(cnf_transformation,[status(thm)],[f475]) ).
fof(f1336,plain,
class_Ring__and__Field_Ozero__neq__one(tc_nat),
inference(cnf_transformation,[status(thm)],[f482]) ).
fof(f1337,plain,
class_Ring__and__Field_Omult__zero(tc_nat),
inference(cnf_transformation,[status(thm)],[f483]) ).
fof(f1345,plain,
class_Power_Opower(tc_nat),
inference(cnf_transformation,[status(thm)],[f491]) ).
fof(f1350,plain,
class_Ring__and__Field_Oordered__semiring__strict(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f496]) ).
fof(f1354,plain,
class_Ring__and__Field_Oring__no__zero__divisors(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f500]) ).
fof(f1363,plain,
class_Ring__and__Field_Ono__zero__divisors(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f509]) ).
fof(f1365,plain,
class_Ring__and__Field_Oordered__semidom(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f511]) ).
fof(f1367,plain,
class_RealVector_Oreal__normed__algebra(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f513]) ).
fof(f1369,plain,
class_RealVector_Oreal__normed__vector(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f515]) ).
fof(f1372,plain,
class_Ring__and__Field_Oordered__field(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f518]) ).
fof(f1373,plain,
class_Ring__and__Field_Odivision__ring(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f519]) ).
fof(f1377,plain,
class_Ring__and__Field_Ozero__neq__one(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f523]) ).
fof(f1378,plain,
class_Ring__and__Field_Oordered__idom(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f524]) ).
fof(f1379,plain,
class_RealVector_Oreal__algebra__1(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f525]) ).
fof(f1381,plain,
class_Ring__and__Field_Omult__zero(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f527]) ).
fof(f1394,plain,
class_Nat_Osemiring__char__0(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f540]) ).
fof(f1396,plain,
class_Orderings_Olinorder(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f542]) ).
fof(f1399,plain,
class_Power_Opower(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f545]) ).
fof(f1402,definition,
( sQ0_spl
<=> c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_d2,tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f1404,plain,
( sQ0_spl
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_d2,tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f1402]) ).
fof(f1405,definition,
( sQ1_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) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f1409,plain,
( sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1404,f1319]) ).
fof(f1410,plain,
sQ0_spl,
inference(contradiction_clause,[status(thm)],[f1409]) ).
fof(f1512,definition,
( sQ9_spl
<=> c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_d1,tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f1514,plain,
( sQ9_spl
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_d1,tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f1512]) ).
fof(f1554,plain,
! [X0] : c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal),
inference(resolution,[status(thm)],[f655,f1354]) ).
fof(f1564,plain,
! [X0,X1,X2] : c_HOL_Otimes__class_Otimes(X0,c_HOL_Otimes__class_Otimes(X1,X2,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(X1,X0,tc_RealDef_Oreal),X2,tc_RealDef_Oreal),
inference(paramodulation,[status(thm)],[f746,f994]) ).
fof(f1575,plain,
! [X0,X1,X2] : c_HOL_Otimes__class_Otimes(X0,c_HOL_Otimes__class_Otimes(X1,X2,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(X1,c_HOL_Otimes__class_Otimes(X0,X2,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[status(thm)],[f994,f1564]) ).
fof(f1582,plain,
! [X0,X1] :
( ~ c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(v_d1,X0,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_d1,X1,tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f1286,f1318]) ).
fof(f1590,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_HOL_Otimes__class_Otimes(X0,v_d1,tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f1269,f1318]) ).
fof(f1591,plain,
! [X0] :
( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X0,v_d2,tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f1269,f1319]) ).
fof(f1960,plain,
c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(v_d1,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_d1,v_d1,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(resolution,[status(thm)],[f1582,f1318]) ).
fof(f2113,plain,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_d2,v_d2,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(resolution,[status(thm)],[f1591,f1319]) ).
fof(f2166,plain,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_d1,v_d1,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(resolution,[status(thm)],[f1590,f1318]) ).
fof(f2540,plain,
! [X0] :
( c_HOL_Osgn__class_Osgn(X0,tc_RealDef_Oreal) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = X0 ),
inference(resolution,[status(thm)],[f596,f1369]) ).
fof(f2655,plain,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Complex_Osko__Complex__XRe__Xpos__bounded__1__1,v_d2,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(resolution,[status(thm)],[f1227,f1591]) ).
fof(f2715,plain,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Complex_Osko__Complex__XIm__Xpos__bounded__1__1,v_d2,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(resolution,[status(thm)],[f1265,f1591]) ).
fof(f2794,plain,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_d2,c_Complex_Osko__Complex__XRe__Xpos__bounded__1__1,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(paramodulation,[status(thm)],[f746,f2655]) ).
fof(f2958,plain,
( sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1514,f1318]) ).
fof(f2959,plain,
sQ9_spl,
inference(contradiction_clause,[status(thm)],[f2958]) ).
fof(f3136,plain,
! [X0] : c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Osko__RealVector__Xmult__left__Xpos__bounded__1__1(X0,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(resolution,[status(thm)],[f1229,f1367]) ).
fof(f3220,definition,
( sQ47_spl
<=> c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_d1,tc_RealDef_Oreal),tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f3221,plain,
( ~ sQ47_spl
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_d1,tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f3220]) ).
fof(f3229,definition,
! [X1,X2] :
( sQ49_spl
<=> ( c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X1,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X2,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(X1,X2,tc_RealDef_Oreal) ) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f3230,plain,
! [X0,X1] :
( ~ sQ49_spl
| c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X1,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f3229]) ).
fof(f3233,definition,
! [X1,X2] :
( sQ50_spl
<=> ( ~ c_HOL_Oord__class_Oless(X1,X2,tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(X1,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X2,tc_RealDef_Oreal),tc_RealDef_Oreal) ) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f3234,plain,
! [X0,X1] :
( ~ sQ50_spl
| ~ c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X1,tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f3233]) ).
fof(f3237,definition,
! [X1,X2] :
( sQ51_spl
<=> ( ~ c_HOL_Oord__class_Oless(X1,X2,tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X1,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X2,tc_RealDef_Oreal),tc_RealDef_Oreal) ) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f3238,plain,
! [X0,X1] :
( ~ sQ51_spl
| ~ c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X1,tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f3237]) ).
fof(f3241,definition,
( sQ52_spl
<=> c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_d2,tc_RealDef_Oreal),tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f3242,plain,
( ~ sQ52_spl
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_d2,tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f3241]) ).
fof(f3249,definition,
! [X1,X2] :
( sQ54_spl
<=> ( ~ c_HOL_Oord__class_Oless(X1,X2,tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(X1,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X2,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) ) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f3250,plain,
! [X0,X1] :
( ~ sQ54_spl
| c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X1,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f3249]) ).
fof(f3315,definition,
! [X0,X1] :
( sQ55_spl
<=> c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(X0,X1,tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f3316,plain,
! [X0,X1] :
( ~ sQ55_spl
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(X0,X1,tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f3315]) ).
fof(f3413,plain,
! [X0] : X0 = c_HOL_Otimes__class_Otimes(c_HOL_Osgn__class_Osgn(X0,tc_RealDef_Oreal),c_HOL_Oabs__class_Oabs(X0,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(resolution,[status(thm)],[f768,f1378]) ).
fof(f3476,definition,
( sQ59_spl
<=> class_Ring__and__Field_Odivision__ring(tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f3478,plain,
( sQ59_spl
| ~ class_Ring__and__Field_Odivision__ring(tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f3476]) ).
fof(f3486,plain,
! [X0] :
( ~ c_HOL_Oord__class_Oless(c_RealDef_Osko__RealDef__Xreal__lbound__gt__zero__1__1(v_d1,X0),v_d2,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealDef_Osko__RealDef__Xreal__lbound__gt__zero__1__1(v_d1,X0),tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_d1,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f1273,f1320]) ).
fof(f3489,definition,
! [X0] :
( sQ61_spl
<=> ( ~ c_HOL_Oord__class_Oless(c_RealDef_Osko__RealDef__Xreal__lbound__gt__zero__1__1(v_d1,X0),v_d2,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealDef_Osko__RealDef__Xreal__lbound__gt__zero__1__1(v_d1,X0),tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal) ) ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f3490,plain,
! [X0] :
( ~ sQ61_spl
| ~ c_HOL_Oord__class_Oless(c_RealDef_Osko__RealDef__Xreal__lbound__gt__zero__1__1(v_d1,X0),v_d2,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealDef_Osko__RealDef__Xreal__lbound__gt__zero__1__1(v_d1,X0),tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f3489]) ).
fof(f3492,plain,
( ~ sQ9_spl
| sQ61_spl ),
inference(split_clause,[status(thm)],[f3486,f3489,f1512]) ).
fof(f3685,plain,
! [X0,X1] :
( ~ c_HOL_Oord__class_Oless(X1,X0,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f1297,f1396]) ).
fof(f3809,plain,
~ c_HOL_Oord__class_Oless(v_d1,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(resolution,[status(thm)],[f3685,f1318]) ).
fof(f3810,plain,
~ c_HOL_Oord__class_Oless(v_d2,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(resolution,[status(thm)],[f3685,f1319]) ).
fof(f3831,plain,
c_Transcendental_Opi = c_HOL_Oabs__class_Oabs(c_Transcendental_Opi,tc_RealDef_Oreal),
inference(resolution,[status(thm)],[f1224,f1281]) ).
fof(f3841,plain,
! [X0] :
( X0 = c_HOL_Oabs__class_Oabs(X0,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f1224,f3685]) ).
fof(f3845,definition,
( sQ64_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,[sQ64_spl])],[split_symbol_definition]) ).
fof(f3976,definition,
( sQ66_spl
<=> v_d1 = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f3977,plain,
( ~ sQ66_spl
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = v_d1 ),
inference(component_clause,[status(thm)],[f3976]) ).
fof(f4074,plain,
( ~ sQ66_spl
| c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(v_d1,v_d1,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_d1,v_d1,tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(backward_demodulation,[status(thm)],[f3977,f1960]) ).
fof(f4095,plain,
( ~ sQ66_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4074,f1302]) ).
fof(f4096,plain,
~ sQ66_spl,
inference(contradiction_clause,[status(thm)],[f4095]) ).
fof(f4483,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ 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(resolution,[status(thm)],[f1269,f1230]) ).
fof(f4503,plain,
~ sQ1_spl,
inference(split_clause,[status(thm)],[f4483,f1405]) ).
fof(f4774,definition,
! [X0] :
( sQ68_spl
<=> ~ class_Nat_Osemiring__char__0(X0) ),
introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition]) ).
fof(f4775,plain,
! [X0] :
( ~ sQ68_spl
| ~ class_Nat_Osemiring__char__0(X0) ),
inference(component_clause,[status(thm)],[f4774]) ).
fof(f4778,plain,
( ~ sQ68_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f1394,f4775]) ).
fof(f4780,plain,
~ sQ68_spl,
inference(contradiction_clause,[status(thm)],[f4778]) ).
fof(f4785,definition,
! [X1] :
( sQ69_spl
<=> ~ class_RealVector_Oreal__algebra__1(X1) ),
introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition]) ).
fof(f4786,plain,
! [X0] :
( ~ sQ69_spl
| ~ class_RealVector_Oreal__algebra__1(X0) ),
inference(component_clause,[status(thm)],[f4785]) ).
fof(f4789,plain,
( ~ sQ69_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f1379,f4786]) ).
fof(f4790,plain,
~ sQ69_spl,
inference(contradiction_clause,[status(thm)],[f4789]) ).
fof(f4946,definition,
( sQ72_spl
<=> class_RealVector_Oreal__normed__vector(tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition]) ).
fof(f4948,plain,
( sQ72_spl
| ~ class_RealVector_Oreal__normed__vector(tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f4946]) ).
fof(f4950,plain,
( sQ72_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4948,f1369]) ).
fof(f4951,plain,
sQ72_spl,
inference(contradiction_clause,[status(thm)],[f4950]) ).
fof(f5134,plain,
! [X0,X1] : c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(X0,c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X1,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(paramodulation,[status(thm)],[f1554,f1575]) ).
fof(f5170,plain,
! [X0] : c_HOL_Otimes__class_Otimes(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(forward_demodulation,[status(thm)],[f1554,f5134]) ).
fof(f6046,plain,
( sQ59_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3478,f1373]) ).
fof(f6047,plain,
sQ59_spl,
inference(contradiction_clause,[status(thm)],[f6046]) ).
fof(f6085,definition,
( sQ93_spl
<=> c_HOL_Oord__class_Oless(c_Complex_Osko__Complex__XRe__Xpos__bounded__1__1,c_Complex_Osko__Complex__XRe__Xpos__bounded__1__1,tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition]) ).
fof(f6086,plain,
( ~ sQ93_spl
| c_HOL_Oord__class_Oless(c_Complex_Osko__Complex__XRe__Xpos__bounded__1__1,c_Complex_Osko__Complex__XRe__Xpos__bounded__1__1,tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f6085]) ).
fof(f6095,plain,
( ~ sQ93_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6086,f1302]) ).
fof(f6096,plain,
~ sQ93_spl,
inference(contradiction_clause,[status(thm)],[f6095]) ).
fof(f6241,definition,
( sQ96_spl
<=> c_HOL_Otimes__class_Otimes(v_d2,v_d2,tc_RealDef_Oreal) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition]) ).
fof(f6242,plain,
( ~ sQ96_spl
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(v_d2,v_d2,tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f6241]) ).
fof(f6249,definition,
( sQ97_spl
<=> c_HOL_Otimes__class_Otimes(v_d1,v_d1,tc_RealDef_Oreal) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition]) ).
fof(f6250,plain,
( ~ sQ97_spl
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(v_d1,v_d1,tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f6249]) ).
fof(f6457,definition,
( sQ105_spl
<=> c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,c_Transcendental_Opi,tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition]) ).
fof(f6458,plain,
( ~ sQ105_spl
| c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,c_Transcendental_Opi,tc_RealDef_Oreal) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f6457]) ).
fof(f6642,definition,
( sQ106_spl
<=> c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Complex_Osko__Complex__XRe__Xpos__bounded__1__1,tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition]) ).
fof(f6644,plain,
( sQ106_spl
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Complex_Osko__Complex__XRe__Xpos__bounded__1__1,tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f6642]) ).
fof(f6688,definition,
( sQ119_spl
<=> class_Ring__and__Field_Oordered__semidom(tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition]) ).
fof(f6690,plain,
( sQ119_spl
| ~ class_Ring__and__Field_Oordered__semidom(tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f6688]) ).
fof(f6715,definition,
( sQ126_spl
<=> c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Complex_Osko__Complex__Xcnj__Xpos__bounded__1__1,tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ126_spl])],[split_symbol_definition]) ).
fof(f6717,plain,
( sQ126_spl
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Complex_Osko__Complex__Xcnj__Xpos__bounded__1__1,tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f6715]) ).
fof(f6722,definition,
( sQ128_spl
<=> class_Ring__and__Field_Oordered__field(tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ128_spl])],[split_symbol_definition]) ).
fof(f6724,plain,
( sQ128_spl
| ~ class_Ring__and__Field_Oordered__field(tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f6722]) ).
fof(f6758,definition,
( sQ138_spl
<=> c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Complex_Osko__Complex__XIm__Xpos__bounded__1__1,tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ138_spl])],[split_symbol_definition]) ).
fof(f6760,plain,
( sQ138_spl
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Complex_Osko__Complex__XIm__Xpos__bounded__1__1,tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f6758]) ).
fof(f6781,plain,
( ~ sQ96_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(backward_demodulation,[status(thm)],[f6242,f2113]) ).
fof(f6834,plain,
( ~ sQ96_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6781,f1302]) ).
fof(f6835,plain,
~ sQ96_spl,
inference(contradiction_clause,[status(thm)],[f6834]) ).
fof(f6905,plain,
( sQ126_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6717,f1282]) ).
fof(f6906,plain,
sQ126_spl,
inference(contradiction_clause,[status(thm)],[f6905]) ).
fof(f6908,plain,
( ~ sQ97_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(backward_demodulation,[status(thm)],[f6250,f2166]) ).
fof(f6959,plain,
( ~ sQ97_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6908,f1302]) ).
fof(f6960,plain,
~ sQ97_spl,
inference(contradiction_clause,[status(thm)],[f6959]) ).
fof(f7033,plain,
( sQ106_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6644,f1227]) ).
fof(f7034,plain,
sQ106_spl,
inference(contradiction_clause,[status(thm)],[f7033]) ).
fof(f7044,plain,
( ~ sQ105_spl
| c_HOL_Oabs__class_Oabs(c_Transcendental_Opi,tc_RealDef_Oreal) = c_NthRoot_Osqrt(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)) ),
inference(paramodulation,[status(thm)],[f6458,f1143]) ).
fof(f7083,plain,
( ~ sQ105_spl
| c_Transcendental_Opi = c_NthRoot_Osqrt(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)) ),
inference(forward_demodulation,[status(thm)],[f3831,f7044]) ).
fof(f7084,plain,
( ~ sQ105_spl
| c_Transcendental_Opi = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
inference(forward_demodulation,[status(thm)],[f874,f7083]) ).
fof(f7085,plain,
( ~ sQ105_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7084,f873]) ).
fof(f7086,plain,
~ sQ105_spl,
inference(contradiction_clause,[status(thm)],[f7085]) ).
fof(f7148,plain,
( sQ138_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6760,f1265]) ).
fof(f7149,plain,
sQ138_spl,
inference(contradiction_clause,[status(thm)],[f7148]) ).
fof(f7172,definition,
( sQ174_spl
<=> class_Ring__and__Field_Oordered__semidom(tc_nat) ),
introduced(definition,[new_symbols(definition,[sQ174_spl])],[split_symbol_definition]) ).
fof(f7174,plain,
( sQ174_spl
| ~ class_Ring__and__Field_Oordered__semidom(tc_nat) ),
inference(component_clause,[status(thm)],[f7172]) ).
fof(f7176,plain,
! [X0,X1] :
( ~ sQ50_spl
| ~ c_HOL_Oord__class_Oless(X1,X0,tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(forward_demodulation,[status(thm)],[f5170,f3234]) ).
fof(f7177,plain,
! [X0,X1] :
( ~ sQ50_spl
| ~ c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal)
| 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)],[f1554,f7176]) ).
fof(f7178,plain,
! [X0,X1] :
( ~ sQ50_spl
| ~ c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal) ),
inference(forward_subsumption_resolution,[status(thm)],[f7177,f1302]) ).
fof(f7181,plain,
( sQ174_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7174,f1329]) ).
fof(f7182,plain,
sQ174_spl,
inference(contradiction_clause,[status(thm)],[f7181]) ).
fof(f7185,plain,
! [X0,X1] :
( ~ sQ49_spl
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X1,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal) ),
inference(forward_demodulation,[status(thm)],[f1554,f3230]) ).
fof(f7186,plain,
! [X0,X1] :
( ~ sQ49_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)
| ~ c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal) ),
inference(forward_demodulation,[status(thm)],[f5170,f7185]) ).
fof(f7187,plain,
! [X0,X1] :
( ~ sQ49_spl
| ~ c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal) ),
inference(forward_subsumption_resolution,[status(thm)],[f7186,f1302]) ).
fof(f7188,plain,
( ~ sQ52_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)],[f1554,f3242]) ).
fof(f7189,plain,
( ~ sQ52_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7188,f1302]) ).
fof(f7190,plain,
~ sQ52_spl,
inference(contradiction_clause,[status(thm)],[f7189]) ).
fof(f7192,plain,
! [X0,X1] :
( ~ sQ51_spl
| ~ c_HOL_Oord__class_Oless(X1,X0,tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(forward_demodulation,[status(thm)],[f1554,f3238]) ).
fof(f7193,plain,
! [X0,X1] :
( ~ sQ51_spl
| ~ c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal)
| 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)],[f1554,f7192]) ).
fof(f7194,plain,
! [X0,X1] :
( ~ sQ51_spl
| ~ c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal) ),
inference(forward_subsumption_resolution,[status(thm)],[f7193,f1302]) ).
fof(f7195,plain,
( ~ sQ47_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)],[f1554,f3221]) ).
fof(f7196,plain,
( ~ sQ47_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7195,f1302]) ).
fof(f7197,plain,
~ sQ47_spl,
inference(contradiction_clause,[status(thm)],[f7196]) ).
fof(f7199,plain,
! [X0,X1] :
( ~ sQ54_spl
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X1,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal) ),
inference(forward_demodulation,[status(thm)],[f5170,f3250]) ).
fof(f7200,plain,
! [X0,X1] :
( ~ sQ54_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)
| ~ c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal) ),
inference(forward_demodulation,[status(thm)],[f5170,f7199]) ).
fof(f7201,plain,
! [X0,X1] :
( ~ sQ54_spl
| ~ c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal) ),
inference(forward_subsumption_resolution,[status(thm)],[f7200,f1302]) ).
fof(f7222,plain,
( ~ sQ50_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f3136,f7178]) ).
fof(f7265,plain,
~ sQ50_spl,
inference(contradiction_clause,[status(thm)],[f7222]) ).
fof(f7266,plain,
( ~ sQ49_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1318,f7187]) ).
fof(f7267,plain,
~ sQ49_spl,
inference(contradiction_clause,[status(thm)],[f7266]) ).
fof(f7268,plain,
( ~ sQ51_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1319,f7194]) ).
fof(f7269,plain,
~ sQ51_spl,
inference(contradiction_clause,[status(thm)],[f7268]) ).
fof(f7271,plain,
( ~ sQ54_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f1318,f7201]) ).
fof(f7272,plain,
~ sQ54_spl,
inference(contradiction_clause,[status(thm)],[f7271]) ).
fof(f7374,definition,
! [X0] :
( sQ176_spl
<=> X0 != X0 ),
introduced(definition,[new_symbols(definition,[sQ176_spl])],[split_symbol_definition]) ).
fof(f7375,plain,
! [X0] :
( ~ sQ176_spl
| X0 != X0 ),
inference(component_clause,[status(thm)],[f7374]) ).
fof(f7378,plain,
( ~ sQ176_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f7375]) ).
fof(f7379,plain,
~ sQ176_spl,
inference(contradiction_clause,[status(thm)],[f7378]) ).
fof(f8109,definition,
( sQ190_spl
<=> c_HOL_Oord__class_Oless(c_Complex_Osko__Complex__XIm__Xpos__bounded__1__1,c_Complex_Osko__Complex__XIm__Xpos__bounded__1__1,tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ190_spl])],[split_symbol_definition]) ).
fof(f8110,plain,
( ~ sQ190_spl
| c_HOL_Oord__class_Oless(c_Complex_Osko__Complex__XIm__Xpos__bounded__1__1,c_Complex_Osko__Complex__XIm__Xpos__bounded__1__1,tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f8109]) ).
fof(f8129,plain,
( ~ sQ190_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8110,f1302]) ).
fof(f8130,plain,
~ sQ190_spl,
inference(contradiction_clause,[status(thm)],[f8129]) ).
fof(f8293,definition,
( sQ195_spl
<=> class_Orderings_Olinorder(tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ195_spl])],[split_symbol_definition]) ).
fof(f8295,plain,
( sQ195_spl
| ~ class_Orderings_Olinorder(tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f8293]) ).
fof(f8300,plain,
( sQ195_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8295,f1396]) ).
fof(f8301,plain,
sQ195_spl,
inference(contradiction_clause,[status(thm)],[f8300]) ).
fof(f8434,definition,
! [X0] :
( sQ200_spl
<=> ( c_HOL_Oord__class_Oless(c_NthRoot_Osqrt(X0),c_NthRoot_Osqrt(X0),tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal) ) ),
introduced(definition,[new_symbols(definition,[sQ200_spl])],[split_symbol_definition]) ).
fof(f8435,plain,
! [X0] :
( ~ sQ200_spl
| c_HOL_Oord__class_Oless(c_NthRoot_Osqrt(X0),c_NthRoot_Osqrt(X0),tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f8434]) ).
fof(f8452,plain,
! [X0] :
( ~ sQ200_spl
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal) ),
inference(forward_subsumption_resolution,[status(thm)],[f8435,f1302]) ).
fof(f8476,plain,
( ~ sQ200_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f2715,f8452]) ).
fof(f8495,plain,
~ sQ200_spl,
inference(contradiction_clause,[status(thm)],[f8476]) ).
fof(f8733,plain,
! [X0] : c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Osko__RealVector__XscaleR__left__Xpos__bounded__1__1(X0,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(resolution,[status(thm)],[f1293,f1369]) ).
fof(f8760,plain,
c_HOL_Otimes__class_Otimes(c_HOL_Osgn__class_Osgn(c_Transcendental_Opi,tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal) = c_Transcendental_Opi,
inference(paramodulation,[status(thm)],[f3831,f3413]) ).
fof(f8906,plain,
c_Transcendental_Opi = c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,c_HOL_Osgn__class_Osgn(c_Transcendental_Opi,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(paramodulation,[status(thm)],[f746,f8760]) ).
fof(f8939,definition,
( sQ212_spl
<=> c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_HOL_Osgn__class_Osgn(c_Transcendental_Opi,tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ212_spl])],[split_symbol_definition]) ).
fof(f8940,plain,
( ~ sQ212_spl
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_HOL_Osgn__class_Osgn(c_Transcendental_Opi,tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f8939]) ).
fof(f8958,plain,
( ~ sQ212_spl
| c_Transcendental_Opi = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f8940,f2540]) ).
fof(f8963,plain,
( ~ sQ212_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8958,f873]) ).
fof(f8964,plain,
~ sQ212_spl,
inference(contradiction_clause,[status(thm)],[f8963]) ).
fof(f9156,definition,
( sQ234_spl
<=> class_RealVector_Oreal__algebra__1(tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ234_spl])],[split_symbol_definition]) ).
fof(f9158,plain,
( sQ234_spl
| ~ class_RealVector_Oreal__algebra__1(tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f9156]) ).
fof(f9163,plain,
( sQ234_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9158,f1379]) ).
fof(f9164,plain,
sQ234_spl,
inference(contradiction_clause,[status(thm)],[f9163]) ).
fof(f9477,definition,
( sQ245_spl
<=> v_d1 = v_d1 ),
introduced(definition,[new_symbols(definition,[sQ245_spl])],[split_symbol_definition]) ).
fof(f9479,plain,
( sQ245_spl
| v_d1 != v_d1 ),
inference(component_clause,[status(thm)],[f9477]) ).
fof(f9597,plain,
( sQ245_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f9479]) ).
fof(f9598,plain,
sQ245_spl,
inference(contradiction_clause,[status(thm)],[f9597]) ).
fof(f9730,definition,
! [X0] :
( sQ246_spl
<=> c_HOL_Oord__class_Oless(c_RealDef_Oreal__of__preal(X0),c_RealDef_Oreal__of__preal(X0),tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ246_spl])],[split_symbol_definition]) ).
fof(f9731,plain,
! [X0] :
( ~ sQ246_spl
| c_HOL_Oord__class_Oless(c_RealDef_Oreal__of__preal(X0),c_RealDef_Oreal__of__preal(X0),tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f9730]) ).
fof(f9738,plain,
( ~ sQ246_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9731,f1302]) ).
fof(f9739,plain,
~ sQ246_spl,
inference(contradiction_clause,[status(thm)],[f9738]) ).
fof(f9778,definition,
( sQ249_spl
<=> c_Transcendental_Opi = c_Transcendental_Opi ),
introduced(definition,[new_symbols(definition,[sQ249_spl])],[split_symbol_definition]) ).
fof(f9780,plain,
( sQ249_spl
| c_Transcendental_Opi != c_Transcendental_Opi ),
inference(component_clause,[status(thm)],[f9778]) ).
fof(f9798,definition,
( sQ251_spl
<=> v_d2 = v_d2 ),
introduced(definition,[new_symbols(definition,[sQ251_spl])],[split_symbol_definition]) ).
fof(f9800,plain,
( sQ251_spl
| v_d2 != v_d2 ),
inference(component_clause,[status(thm)],[f9798]) ).
fof(f9816,plain,
( sQ249_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f9780]) ).
fof(f9817,plain,
sQ249_spl,
inference(contradiction_clause,[status(thm)],[f9816]) ).
fof(f9866,plain,
( sQ251_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f9800]) ).
fof(f9867,plain,
sQ251_spl,
inference(contradiction_clause,[status(thm)],[f9866]) ).
fof(f9920,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)
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_HOL_Oabs__class_Oabs(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f1224,f3841]) ).
fof(f9973,plain,
sQ64_spl,
inference(split_clause,[status(thm)],[f9920,f3845]) ).
fof(f9979,plain,
( sQ119_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6690,f1365]) ).
fof(f9980,plain,
sQ119_spl,
inference(contradiction_clause,[status(thm)],[f9979]) ).
fof(f9981,plain,
( sQ128_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6724,f1372]) ).
fof(f9982,plain,
sQ128_spl,
inference(contradiction_clause,[status(thm)],[f9981]) ).
fof(f10014,definition,
( sQ258_spl
<=> c_Complex_Osko__Complex__XRe__Xpos__bounded__1__1 = c_Complex_Osko__Complex__XRe__Xpos__bounded__1__1 ),
introduced(definition,[new_symbols(definition,[sQ258_spl])],[split_symbol_definition]) ).
fof(f10016,plain,
( sQ258_spl
| c_Complex_Osko__Complex__XRe__Xpos__bounded__1__1 != c_Complex_Osko__Complex__XRe__Xpos__bounded__1__1 ),
inference(component_clause,[status(thm)],[f10014]) ).
fof(f10026,plain,
( sQ258_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f10016]) ).
fof(f10027,plain,
sQ258_spl,
inference(contradiction_clause,[status(thm)],[f10026]) ).
fof(f10060,definition,
( sQ260_spl
<=> c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_NthRoot_Osqrt(c_Complex_Osko__Complex__Xcnj__Xpos__bounded__1__1) ),
introduced(definition,[new_symbols(definition,[sQ260_spl])],[split_symbol_definition]) ).
fof(f10061,plain,
( ~ sQ260_spl
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_NthRoot_Osqrt(c_Complex_Osko__Complex__Xcnj__Xpos__bounded__1__1) ),
inference(component_clause,[status(thm)],[f10060]) ).
fof(f10081,definition,
( sQ264_spl
<=> c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_NthRoot_Osqrt(v_d1) ),
introduced(definition,[new_symbols(definition,[sQ264_spl])],[split_symbol_definition]) ).
fof(f10082,plain,
( ~ sQ264_spl
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_NthRoot_Osqrt(v_d1) ),
inference(component_clause,[status(thm)],[f10081]) ).
fof(f10175,definition,
( sQ266_spl
<=> c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_NthRoot_Osqrt(c_Complex_Osko__Complex__XRe__Xpos__bounded__1__1) ),
introduced(definition,[new_symbols(definition,[sQ266_spl])],[split_symbol_definition]) ).
fof(f10176,plain,
( ~ sQ266_spl
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_NthRoot_Osqrt(c_Complex_Osko__Complex__XRe__Xpos__bounded__1__1) ),
inference(component_clause,[status(thm)],[f10175]) ).
fof(f10194,definition,
( sQ268_spl
<=> c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_NthRoot_Osqrt(c_Complex_Osko__Complex__XIm__Xpos__bounded__1__1) ),
introduced(definition,[new_symbols(definition,[sQ268_spl])],[split_symbol_definition]) ).
fof(f10195,plain,
( ~ sQ268_spl
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_NthRoot_Osqrt(c_Complex_Osko__Complex__XIm__Xpos__bounded__1__1) ),
inference(component_clause,[status(thm)],[f10194]) ).
fof(f10205,definition,
( sQ270_spl
<=> c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_NthRoot_Osqrt(c_Transcendental_Opi) ),
introduced(definition,[new_symbols(definition,[sQ270_spl])],[split_symbol_definition]) ).
fof(f10206,plain,
( ~ sQ270_spl
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_NthRoot_Osqrt(c_Transcendental_Opi) ),
inference(component_clause,[status(thm)],[f10205]) ).
fof(f10270,definition,
( sQ271_spl
<=> c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_HOL_Osgn__class_Osgn(c_Transcendental_Opi,tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ271_spl])],[split_symbol_definition]) ).
fof(f10271,plain,
( ~ sQ271_spl
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_HOL_Osgn__class_Osgn(c_Transcendental_Opi,tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f10270]) ).
fof(f10294,definition,
( sQ277_spl
<=> c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,c_HOL_Osgn__class_Osgn(c_Transcendental_Opi,tc_RealDef_Oreal),tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ277_spl])],[split_symbol_definition]) ).
fof(f10295,plain,
( ~ sQ277_spl
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,c_HOL_Osgn__class_Osgn(c_Transcendental_Opi,tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f10294]) ).
fof(f10386,plain,
( ~ sQ271_spl
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_Transcendental_Opi ),
inference(forward_demodulation,[status(thm)],[f8760,f10271]) ).
fof(f10387,plain,
( ~ sQ271_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10386,f873]) ).
fof(f10388,plain,
~ sQ271_spl,
inference(contradiction_clause,[status(thm)],[f10387]) ).
fof(f10412,plain,
( ~ sQ277_spl
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_Transcendental_Opi ),
inference(forward_demodulation,[status(thm)],[f8906,f10295]) ).
fof(f10413,plain,
( ~ sQ277_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10412,f873]) ).
fof(f10414,plain,
~ sQ277_spl,
inference(contradiction_clause,[status(thm)],[f10413]) ).
fof(f10482,definition,
( sQ296_spl
<=> c_Complex_Osko__Complex__Xcnj__Xpos__bounded__1__1 = c_Complex_Osko__Complex__Xcnj__Xpos__bounded__1__1 ),
introduced(definition,[new_symbols(definition,[sQ296_spl])],[split_symbol_definition]) ).
fof(f10484,plain,
( sQ296_spl
| c_Complex_Osko__Complex__Xcnj__Xpos__bounded__1__1 != c_Complex_Osko__Complex__Xcnj__Xpos__bounded__1__1 ),
inference(component_clause,[status(thm)],[f10482]) ).
fof(f10490,plain,
( sQ296_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f10484]) ).
fof(f10491,plain,
sQ296_spl,
inference(contradiction_clause,[status(thm)],[f10490]) ).
fof(f10546,definition,
( sQ299_spl
<=> c_Complex_Osko__Complex__XIm__Xpos__bounded__1__1 = c_Complex_Osko__Complex__XIm__Xpos__bounded__1__1 ),
introduced(definition,[new_symbols(definition,[sQ299_spl])],[split_symbol_definition]) ).
fof(f10548,plain,
( sQ299_spl
| c_Complex_Osko__Complex__XIm__Xpos__bounded__1__1 != c_Complex_Osko__Complex__XIm__Xpos__bounded__1__1 ),
inference(component_clause,[status(thm)],[f10546]) ).
fof(f10553,plain,
( sQ299_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f10548]) ).
fof(f10554,plain,
sQ299_spl,
inference(contradiction_clause,[status(thm)],[f10553]) ).
fof(f11725,definition,
( sQ387_spl
<=> c_HOL_Oord__class_Oless(v_d1,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ387_spl])],[split_symbol_definition]) ).
fof(f11726,plain,
( ~ sQ387_spl
| c_HOL_Oord__class_Oless(v_d1,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f11725]) ).
fof(f12700,plain,
! [X0] : c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) != c_NthRoot_Osqrt(c_RealVector_Osko__RealVector__XscaleR__left__Xpos__bounded__1__1(X0,tc_RealDef_Oreal)),
inference(resolution,[status(thm)],[f1266,f8733]) ).
fof(f12704,plain,
! [X0] : c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) != c_NthRoot_Osqrt(c_Transcendental_Oexp(X0,tc_RealDef_Oreal)),
inference(resolution,[status(thm)],[f1266,f1291]) ).
fof(f12709,plain,
c_NthRoot_Osqrt(c_Complex_Osko__Complex__XRe__Xpos__bounded__1__1) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(resolution,[status(thm)],[f1266,f1227]) ).
fof(f12710,plain,
c_NthRoot_Osqrt(c_Transcendental_Opi) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(resolution,[status(thm)],[f1266,f1222]) ).
fof(f12731,plain,
c_NthRoot_Osqrt(c_Complex_Osko__Complex__Xcnj__Xpos__bounded__1__1) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(resolution,[status(thm)],[f1266,f1282]) ).
fof(f12732,plain,
c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) != c_NthRoot_Osqrt(c_Complex_Osko__Complex__XIm__Xpos__bounded__1__1),
inference(resolution,[status(thm)],[f1266,f1265]) ).
fof(f12740,definition,
( sQ405_spl
<=> c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_NthRoot_Osqrt(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)) ),
introduced(definition,[new_symbols(definition,[sQ405_spl])],[split_symbol_definition]) ).
fof(f12742,plain,
( sQ405_spl
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) != c_NthRoot_Osqrt(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)) ),
inference(component_clause,[status(thm)],[f12740]) ).
fof(f13212,plain,
( sQ405_spl
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
inference(forward_demodulation,[status(thm)],[f874,f12742]) ).
fof(f13213,plain,
( sQ405_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f13212]) ).
fof(f13214,plain,
sQ405_spl,
inference(contradiction_clause,[status(thm)],[f13213]) ).
fof(f13476,definition,
( sQ416_spl
<=> class_Ring__and__Field_Omult__zero(tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ416_spl])],[split_symbol_definition]) ).
fof(f13478,plain,
( sQ416_spl
| ~ class_Ring__and__Field_Omult__zero(tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f13476]) ).
fof(f13479,definition,
( sQ417_spl
<=> class_Power_Opower(tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ417_spl])],[split_symbol_definition]) ).
fof(f13481,plain,
( sQ417_spl
| ~ class_Power_Opower(tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f13479]) ).
fof(f13482,definition,
( sQ418_spl
<=> class_Ring__and__Field_Ozero__neq__one(tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ418_spl])],[split_symbol_definition]) ).
fof(f13484,plain,
( sQ418_spl
| ~ class_Ring__and__Field_Ozero__neq__one(tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f13482]) ).
fof(f13489,definition,
( sQ420_spl
<=> class_Ring__and__Field_Omult__zero(tc_nat) ),
introduced(definition,[new_symbols(definition,[sQ420_spl])],[split_symbol_definition]) ).
fof(f13491,plain,
( sQ420_spl
| ~ class_Ring__and__Field_Omult__zero(tc_nat) ),
inference(component_clause,[status(thm)],[f13489]) ).
fof(f13492,definition,
( sQ421_spl
<=> class_Power_Opower(tc_nat) ),
introduced(definition,[new_symbols(definition,[sQ421_spl])],[split_symbol_definition]) ).
fof(f13494,plain,
( sQ421_spl
| ~ class_Power_Opower(tc_nat) ),
inference(component_clause,[status(thm)],[f13492]) ).
fof(f13495,definition,
( sQ422_spl
<=> class_Ring__and__Field_Ozero__neq__one(tc_nat) ),
introduced(definition,[new_symbols(definition,[sQ422_spl])],[split_symbol_definition]) ).
fof(f13497,plain,
( sQ422_spl
| ~ class_Ring__and__Field_Ozero__neq__one(tc_nat) ),
inference(component_clause,[status(thm)],[f13495]) ).
fof(f13499,definition,
( sQ423_spl
<=> class_Ring__and__Field_Ono__zero__divisors(tc_nat) ),
introduced(definition,[new_symbols(definition,[sQ423_spl])],[split_symbol_definition]) ).
fof(f13501,plain,
( sQ423_spl
| ~ class_Ring__and__Field_Ono__zero__divisors(tc_nat) ),
inference(component_clause,[status(thm)],[f13499]) ).
fof(f13504,definition,
( sQ424_spl
<=> class_Ring__and__Field_Ono__zero__divisors(tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ424_spl])],[split_symbol_definition]) ).
fof(f13506,plain,
( sQ424_spl
| ~ class_Ring__and__Field_Ono__zero__divisors(tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f13504]) ).
fof(f13509,plain,
( sQ416_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f13478,f1381]) ).
fof(f13510,plain,
sQ416_spl,
inference(contradiction_clause,[status(thm)],[f13509]) ).
fof(f13511,plain,
( sQ417_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f13481,f1399]) ).
fof(f13512,plain,
sQ417_spl,
inference(contradiction_clause,[status(thm)],[f13511]) ).
fof(f13513,plain,
( sQ424_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f13506,f1363]) ).
fof(f13514,plain,
sQ424_spl,
inference(contradiction_clause,[status(thm)],[f13513]) ).
fof(f13515,plain,
( sQ421_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f13494,f1345]) ).
fof(f13516,plain,
sQ421_spl,
inference(contradiction_clause,[status(thm)],[f13515]) ).
fof(f13517,plain,
( sQ418_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f13484,f1377]) ).
fof(f13518,plain,
sQ418_spl,
inference(contradiction_clause,[status(thm)],[f13517]) ).
fof(f13519,plain,
( sQ420_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f13491,f1337]) ).
fof(f13520,plain,
sQ420_spl,
inference(contradiction_clause,[status(thm)],[f13519]) ).
fof(f13521,plain,
( sQ422_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f13497,f1336]) ).
fof(f13522,plain,
sQ422_spl,
inference(contradiction_clause,[status(thm)],[f13521]) ).
fof(f13523,plain,
( sQ423_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f13501,f1328]) ).
fof(f13524,plain,
sQ423_spl,
inference(contradiction_clause,[status(thm)],[f13523]) ).
fof(f14464,plain,
c_Transcendental_Oexp(c_Transcendental_Oln(v_d1),tc_RealDef_Oreal) = v_d1,
inference(resolution,[status(thm)],[f880,f1318]) ).
fof(f14480,plain,
! [X0] : c_RealDef_Oreal__of__preal(X0) = c_Transcendental_Oexp(c_Transcendental_Oln(c_RealDef_Oreal__of__preal(X0)),tc_RealDef_Oreal),
inference(resolution,[status(thm)],[f880,f1233]) ).
fof(f14482,plain,
c_Transcendental_Opi = c_Transcendental_Oexp(c_Transcendental_Oln(c_Transcendental_Opi),tc_RealDef_Oreal),
inference(resolution,[status(thm)],[f880,f1222]) ).
fof(f14949,plain,
( ~ sQ387_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11726,f3809]) ).
fof(f14950,plain,
~ sQ387_spl,
inference(contradiction_clause,[status(thm)],[f14949]) ).
fof(f15071,definition,
( sQ498_spl
<=> c_HOL_Oord__class_Oless(v_d2,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ498_spl])],[split_symbol_definition]) ).
fof(f15072,plain,
( ~ sQ498_spl
| c_HOL_Oord__class_Oless(v_d2,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f15071]) ).
fof(f15782,plain,
! [X0] :
( c_HOL_Oord__class_Oless(X0,c_Transcendental_Oexp(X0,tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Transcendental_Oexp(X0,tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(paramodulation,[status(thm)],[f1061,f1252]) ).
fof(f15792,plain,
! [X0] : c_HOL_Oord__class_Oless(X0,c_Transcendental_Oexp(X0,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_subsumption_resolution,[status(thm)],[f15782,f1291]) ).
fof(f15805,plain,
! [X0] : c_HOL_Oord__class_Oless(c_Transcendental_Oln(c_RealDef_Oreal__of__preal(X0)),c_RealDef_Oreal__of__preal(X0),tc_RealDef_Oreal),
inference(paramodulation,[status(thm)],[f14480,f15792]) ).
fof(f15809,plain,
c_HOL_Oord__class_Oless(c_Transcendental_Oln(c_Transcendental_Opi),c_Transcendental_Opi,tc_RealDef_Oreal),
inference(paramodulation,[status(thm)],[f14482,f15792]) ).
fof(f15918,plain,
( ~ sQ498_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f15072,f3810]) ).
fof(f15919,plain,
~ sQ498_spl,
inference(contradiction_clause,[status(thm)],[f15918]) ).
fof(f16357,plain,
c_HOL_Oord__class_Oless(c_Transcendental_Oln(v_d1),v_d1,tc_RealDef_Oreal),
inference(paramodulation,[status(thm)],[f14464,f15792]) ).
fof(f16361,plain,
c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) != c_NthRoot_Osqrt(v_d1),
inference(paramodulation,[status(thm)],[f14464,f12704]) ).
fof(f16715,definition,
( sQ582_spl
<=> c_Transcendental_Oln(v_d1) = v_d1 ),
introduced(definition,[new_symbols(definition,[sQ582_spl])],[split_symbol_definition]) ).
fof(f16716,plain,
( ~ sQ582_spl
| v_d1 = c_Transcendental_Oln(v_d1) ),
inference(component_clause,[status(thm)],[f16715]) ).
fof(f16720,plain,
( ~ sQ582_spl
| c_HOL_Oord__class_Oless(v_d1,v_d1,tc_RealDef_Oreal) ),
inference(backward_demodulation,[status(thm)],[f16716,f16357]) ).
fof(f16734,plain,
( ~ sQ582_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16720,f1302]) ).
fof(f16735,plain,
~ sQ582_spl,
inference(contradiction_clause,[status(thm)],[f16734]) ).
fof(f16802,definition,
( sQ592_spl
<=> c_Transcendental_Oln(c_Transcendental_Opi) = c_Transcendental_Opi ),
introduced(definition,[new_symbols(definition,[sQ592_spl])],[split_symbol_definition]) ).
fof(f16803,plain,
( ~ sQ592_spl
| c_Transcendental_Oln(c_Transcendental_Opi) = c_Transcendental_Opi ),
inference(component_clause,[status(thm)],[f16802]) ).
fof(f16808,plain,
( ~ sQ592_spl
| c_HOL_Oord__class_Oless(c_Transcendental_Opi,c_Transcendental_Opi,tc_RealDef_Oreal) ),
inference(backward_demodulation,[status(thm)],[f16803,f15809]) ).
fof(f16836,plain,
( ~ sQ592_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16808,f1302]) ).
fof(f16837,plain,
~ sQ592_spl,
inference(contradiction_clause,[status(thm)],[f16836]) ).
fof(f17522,definition,
! [X0] :
( sQ627_spl
<=> c_HOL_Oord__class_Oless(c_Transcendental_Oexp(X0,tc_RealDef_Oreal),c_Transcendental_Oexp(X0,tc_RealDef_Oreal),tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ627_spl])],[split_symbol_definition]) ).
fof(f17523,plain,
! [X0] :
( ~ sQ627_spl
| c_HOL_Oord__class_Oless(c_Transcendental_Oexp(X0,tc_RealDef_Oreal),c_Transcendental_Oexp(X0,tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f17522]) ).
fof(f17549,plain,
( ~ sQ627_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f17523,f1302]) ).
fof(f17550,plain,
~ sQ627_spl,
inference(contradiction_clause,[status(thm)],[f17549]) ).
fof(f18137,definition,
! [X1] :
( sQ664_spl
<=> c_NthRoot_Osqrt(X1) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ664_spl])],[split_symbol_definition]) ).
fof(f18138,plain,
! [X0] :
( ~ sQ664_spl
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_NthRoot_Osqrt(X0) ),
inference(component_clause,[status(thm)],[f18137]) ).
fof(f18174,plain,
( ~ sQ270_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10206,f12710]) ).
fof(f18175,plain,
~ sQ270_spl,
inference(contradiction_clause,[status(thm)],[f18174]) ).
fof(f18481,plain,
( ~ sQ260_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10061,f12731]) ).
fof(f18482,plain,
~ sQ260_spl,
inference(contradiction_clause,[status(thm)],[f18481]) ).
fof(f18483,plain,
( ~ sQ266_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10176,f12709]) ).
fof(f18484,plain,
~ sQ266_spl,
inference(contradiction_clause,[status(thm)],[f18483]) ).
fof(f18485,plain,
( ~ sQ268_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10195,f12732]) ).
fof(f18486,plain,
~ sQ268_spl,
inference(contradiction_clause,[status(thm)],[f18485]) ).
fof(f19744,plain,
( ~ sQ664_spl
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
inference(backward_demodulation,[status(thm)],[f18138,f12700]) ).
fof(f19793,plain,
( ~ sQ664_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f19744]) ).
fof(f19794,plain,
~ sQ664_spl,
inference(contradiction_clause,[status(thm)],[f19793]) ).
fof(f19900,definition,
( sQ703_spl
<=> class_Ring__and__Field_Oordered__idom(tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ703_spl])],[split_symbol_definition]) ).
fof(f19902,plain,
( sQ703_spl
| ~ class_Ring__and__Field_Oordered__idom(tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f19900]) ).
fof(f20054,plain,
( ~ sQ55_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(backward_demodulation,[status(thm)],[f3316,f2794]) ).
fof(f20135,plain,
( ~ sQ55_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20054,f1302]) ).
fof(f20136,plain,
~ sQ55_spl,
inference(contradiction_clause,[status(thm)],[f20135]) ).
fof(f20413,plain,
! [X0] : c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(paramodulation,[status(thm)],[f5170,f746]) ).
fof(f20442,definition,
! [X0,X1] :
( sQ728_spl
<=> ( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X1,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal) ) ),
introduced(definition,[new_symbols(definition,[sQ728_spl])],[split_symbol_definition]) ).
fof(f20443,plain,
! [X0,X1] :
( ~ sQ728_spl
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X1,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f20442]) ).
fof(f20553,definition,
! [X0,X1] :
( sQ733_spl
<=> ( ~ c_HOL_Oord__class_Oless(X1,X0,tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal),tc_RealDef_Oreal) ) ),
introduced(definition,[new_symbols(definition,[sQ733_spl])],[split_symbol_definition]) ).
fof(f20554,plain,
! [X0,X1] :
( ~ sQ733_spl
| ~ c_HOL_Oord__class_Oless(X1,X0,tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f20553]) ).
fof(f20906,definition,
! [X0,X1] :
( sQ746_spl
<=> ~ c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ746_spl])],[split_symbol_definition]) ).
fof(f20907,plain,
! [X0,X1] :
( ~ sQ746_spl
| ~ c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f20906]) ).
fof(f21053,plain,
! [X0,X1] :
( ~ sQ728_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)
| ~ c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal) ),
inference(forward_demodulation,[status(thm)],[f5170,f20443]) ).
fof(f21054,plain,
! [X0,X1] :
( ~ sQ728_spl
| ~ c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal) ),
inference(forward_subsumption_resolution,[status(thm)],[f21053,f1302]) ).
fof(f21115,plain,
! [X0,X1] :
( ~ sQ733_spl
| ~ c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal)
| 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)],[f20413,f20554]) ).
fof(f21116,plain,
! [X0,X1] :
( ~ sQ733_spl
| ~ c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal) ),
inference(forward_subsumption_resolution,[status(thm)],[f21115,f1302]) ).
fof(f21245,plain,
( sQ703_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19902,f1378]) ).
fof(f21246,plain,
sQ703_spl,
inference(contradiction_clause,[status(thm)],[f21245]) ).
fof(f21429,plain,
( ~ sQ728_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f15805,f21054]) ).
fof(f21448,plain,
~ sQ728_spl,
inference(contradiction_clause,[status(thm)],[f21429]) ).
fof(f21473,plain,
( ~ sQ733_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f873,f21476]) ).
fof(f21476,plain,
! [X0] :
( ~ sQ733_spl
| X0 = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
inference(forward_subsumption_resolution,[status(thm)],[f1223,f21116]) ).
fof(f21480,plain,
~ sQ733_spl,
inference(contradiction_clause,[status(thm)],[f21473]) ).
fof(f21496,definition,
( sQ749_spl
<=> class_RealVector_Oreal__normed__algebra(tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ749_spl])],[split_symbol_definition]) ).
fof(f21498,plain,
( sQ749_spl
| ~ class_RealVector_Oreal__normed__algebra(tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f21496]) ).
fof(f21510,plain,
( sQ749_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f21498,f1367]) ).
fof(f21511,plain,
sQ749_spl,
inference(contradiction_clause,[status(thm)],[f21510]) ).
fof(f21685,plain,
( ~ sQ746_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f12710,f21693]) ).
fof(f21693,plain,
! [X0] :
( ~ sQ746_spl
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = X0 ),
inference(forward_subsumption_resolution,[status(thm)],[f1223,f20907]) ).
fof(f21701,plain,
~ sQ746_spl,
inference(contradiction_clause,[status(thm)],[f21685]) ).
fof(f21753,definition,
( sQ761_spl
<=> class_Ring__and__Field_Oordered__semiring__strict(tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ761_spl])],[split_symbol_definition]) ).
fof(f21755,plain,
( sQ761_spl
| ~ class_Ring__and__Field_Oordered__semiring__strict(tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f21753]) ).
fof(f21757,plain,
( sQ761_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f21755,f1350]) ).
fof(f21758,plain,
sQ761_spl,
inference(contradiction_clause,[status(thm)],[f21757]) ).
fof(f21898,plain,
( ~ sQ264_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10082,f16361]) ).
fof(f21899,plain,
~ sQ264_spl,
inference(contradiction_clause,[status(thm)],[f21898]) ).
fof(f22521,plain,
( ~ sQ61_spl
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_d2,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_d1,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_d2,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealDef_Osko__RealDef__Xreal__lbound__gt__zero__1__1(v_d1,v_d2),tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f3490,f1271]) ).
fof(f22522,definition,
( sQ800_spl
<=> c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealDef_Osko__RealDef__Xreal__lbound__gt__zero__1__1(v_d1,v_d2),tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ800_spl])],[split_symbol_definition]) ).
fof(f22524,plain,
( sQ800_spl
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealDef_Osko__RealDef__Xreal__lbound__gt__zero__1__1(v_d1,v_d2),tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f22522]) ).
fof(f22525,plain,
( ~ sQ61_spl
| ~ sQ9_spl
| ~ sQ0_spl
| ~ sQ800_spl ),
inference(split_clause,[status(thm)],[f22521,f22522,f1402,f1512,f3489]) ).
fof(f25245,definition,
( sQ897_spl
<=> c_HOL_Oord__class_Oless(c_NthRoot_Osqrt(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ897_spl])],[split_symbol_definition]) ).
fof(f25246,plain,
( ~ sQ897_spl
| c_HOL_Oord__class_Oless(c_NthRoot_Osqrt(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f25245]) ).
fof(f25249,plain,
( ~ sQ897_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)],[f874,f25246]) ).
fof(f25250,plain,
( ~ sQ897_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f25249,f1302]) ).
fof(f25251,plain,
~ sQ897_spl,
inference(contradiction_clause,[status(thm)],[f25250]) ).
fof(f25306,plain,
( sQ800_spl
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_d1,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_d2,tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f22524,f1239]) ).
fof(f25308,plain,
( sQ800_spl
| ~ sQ9_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f25306,f1402,f1512,f22522]) ).
fof(f25309,plain,
$false,
inference(sat_refutation,[status(thm)],[f1410,f2959,f3492,f4096,f4503,f4780,f4790,f4951,f6047,f6096,f6835,f6906,f6960,f7034,f7086,f7149,f7182,f7190,f7197,f7265,f7267,f7269,f7272,f7379,f8130,f8301,f8495,f8964,f9164,f9598,f9739,f9817,f9867,f9973,f9980,f9982,f10027,f10388,f10414,f10491,f10554,f13214,f13510,f13512,f13514,f13516,f13518,f13520,f13522,f13524,f14950,f15919,f16735,f16837,f17550,f18175,f18482,f18484,f18486,f19794,f20136,f21246,f21448,f21480,f21511,f21701,f21758,f21899,f22525,f25251,f25308]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG339-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/0.42 % Computer : n003.cluster.edu
% 0.15/0.42 % Model : x86_64 x86_64
% 0.15/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.42 % Memory : 8046.5625MB
% 0.15/0.42 % OS : Linux 6.8.0-71-generic
% 0.15/0.42 % CPULimit : 300
% 0.15/0.42 % WCLimit : 300
% 0.15/0.42 % DateTime : Mon Sep 21 13:18:31 UTC 2026
% 0.15/0.42 % CPUTime :
% 0.15/0.51 % Drodi V4.1.1
% 126.67/16.62 % Refutation found
% 126.67/16.62 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 126.67/16.62 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 8.88/17.47 % Elapsed time: 17.029145 seconds
% 8.88/17.47 % CPU time: 128.686869 seconds
% 8.88/17.47 % Total memory used: 526.745 MB
% 8.88/17.47 % Net memory used: 498.866 MB
%------------------------------------------------------------------------------