%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : ALG340-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n011.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 : Fri Sep 25 12:52:20 PM UTC 2026
% Result : Unsatisfiable 23.64s 21.82s
% Output : Proof 23.64s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 32
% Syntax : Number of formulae : 154 ( 66 unt; 0 def)
% Number of atoms : 282 ( 49 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 334 ( 206 ~; 128 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 7 ( 1 avg)
% Number of predicates : 12 ( 10 usr; 1 prp; 0-3 aty)
% Number of functors : 16 ( 16 usr; 4 con; 0-4 aty)
% Number of variables : 237 ( 12 sgn 100 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f428,negated_conjecture,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_xa,tc_RealDef_Oreal)
| ~ c_lessequals(c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_x(V_xa),tc_Complex_Ocomplex),tc_Complex_Ocomplex),V_xa,tc_RealDef_Oreal) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_1) ).
fof(f428_nnf,plain,
! [V_xa] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_xa,tc_RealDef_Oreal)
| ~ c_lessequals(c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_x(V_xa),tc_Complex_Ocomplex),tc_Complex_Ocomplex),V_xa,tc_RealDef_Oreal) ),
inference(nnf_transformation,[status(thm)],[f428]) ).
fof(f428_sk,plain,
! [V_xa] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_xa,tc_RealDef_Oreal)
| ~ c_lessequals(c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_x(V_xa),tc_Complex_Ocomplex),tc_Complex_Ocomplex),V_xa,tc_RealDef_Oreal) ),
inference(skolemisation,[status(esa)],[f428_nnf]) ).
cnf(c428,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)
| ~ c_lessequals(c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_x(X0),tc_Complex_Ocomplex),tc_Complex_Ocomplex),X0,tc_RealDef_Oreal) ),
inference(cnf_transformation,[status(esa)],[f428_sk]) ).
cnf(t156,plain,
or(not(c_lessequals(c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_x(X1),tc_Complex_Ocomplex),tc_Complex_Ocomplex),X1,tc_RealDef_Oreal)),not(c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X1,tc_RealDef_Oreal))) = true,
inference(equality_encoding,[status(esa)],[c428]) ).
cnf(t373,plain,
or(not(c_lessequals(c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_x(X1),tc_Complex_Ocomplex),tc_Complex_Ocomplex),X1,tc_RealDef_Oreal)),not(c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X1,tc_RealDef_Oreal))) = true,
inference(orient,[status(thm)],[t156]) ).
cnf(f390,axiom,
( c_Polynomial_Opoly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)),V_x,T_a) = c_HOL_Ozero__class_Ozero(T_a)
| ~ class_Ring__and__Field_Ocomm__semiring__0(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_poly__0_0) ).
fof(f390_nnf,plain,
! [T_a,V_x] :
( c_Polynomial_Opoly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)),V_x,T_a) = c_HOL_Ozero__class_Ozero(T_a)
| ~ class_Ring__and__Field_Ocomm__semiring__0(T_a) ),
inference(nnf_transformation,[status(thm)],[f390]) ).
fof(f390_sk,plain,
! [T_a,V_x] :
( c_Polynomial_Opoly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)),V_x,T_a) = c_HOL_Ozero__class_Ozero(T_a)
| ~ class_Ring__and__Field_Ocomm__semiring__0(T_a) ),
inference(skolemisation,[status(esa)],[f390_nnf]) ).
cnf(c390,plain,
( c_Polynomial_Opoly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)),X1,X0) = c_HOL_Ozero__class_Ozero(X0)
| ~ class_Ring__and__Field_Ocomm__semiring__0(X0) ),
inference(cnf_transformation,[status(esa)],[f390_sk]) ).
cnf(hi378,axiom,
ifeq(class_Ring__and__Field_Ocomm__semiring__0(X0),true,c_Polynomial_Opoly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)),X1,X0),c_HOL_Ozero__class_Ozero(X0)) = c_HOL_Ozero__class_Ozero(X0),
inference(equality_encoding,[status(esa)],[c390]) ).
cnf(f492,axiom,
class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_Complex__Ocomplex__Ring__and__Field_Ocomm__semiring__0) ).
fof(f492_nnf,plain,
class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex),
inference(nnf_transformation,[status(thm)],[f492]) ).
cnf(c492,plain,
class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(esa)],[f492_nnf]) ).
cnf(hi473,axiom,
class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex) = true,
inference(equality_encoding,[status(esa)],[c492]) ).
cnf(t50,plain,
c_Polynomial_Opoly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X1,tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(hyper_resolution,[status(thm)],[hi378,hi473]) ).
cnf(t965,plain,
c_Polynomial_Opoly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X1,tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(orient,[status(thm)],[t50]) ).
cnf(t3071,plain,
or(not(c_lessequals(c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),X1,tc_RealDef_Oreal)),not(c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X1,tc_RealDef_Oreal))) = true,
inference(step,[status(thm)],[t373,t965]) ).
cnf(f389,axiom,
( c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(T_a),T_a) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)
| ~ class_RealVector_Oreal__normed__vector(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_norm__zero_0) ).
fof(f389_nnf,plain,
! [T_a] :
( c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(T_a),T_a) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)
| ~ class_RealVector_Oreal__normed__vector(T_a) ),
inference(nnf_transformation,[status(thm)],[f389]) ).
fof(f389_sk,plain,
! [T_a] :
( c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(T_a),T_a) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)
| ~ class_RealVector_Oreal__normed__vector(T_a) ),
inference(skolemisation,[status(esa)],[f389_nnf]) ).
cnf(c389,plain,
( c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(X0),X0) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)
| ~ class_RealVector_Oreal__normed__vector(X0) ),
inference(cnf_transformation,[status(esa)],[f389_sk]) ).
cnf(hi377,axiom,
ifeq(class_RealVector_Oreal__normed__vector(X0),true,c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(X0),X0),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(equality_encoding,[status(esa)],[c389]) ).
cnf(f495,axiom,
class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_Complex__Ocomplex__RealVector_Oreal__normed__vector) ).
fof(f495_nnf,plain,
class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex),
inference(nnf_transformation,[status(thm)],[f495]) ).
cnf(c495,plain,
class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(esa)],[f495_nnf]) ).
cnf(hi476,axiom,
class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex) = true,
inference(equality_encoding,[status(esa)],[c495]) ).
cnf(t33,plain,
c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(hyper_resolution,[status(thm)],[hi377,hi476]) ).
cnf(t939,plain,
c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(orient,[status(thm)],[t33]) ).
cnf(t3072,plain,
or(not(c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X1,tc_RealDef_Oreal)),not(c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X1,tc_RealDef_Oreal))) = true,
inference(step,[status(thm)],[t3071,t939]) ).
cnf(t967,plain,
or(not(c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X1,tc_RealDef_Oreal)),not(c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X1,tc_RealDef_Oreal))) = true,
inference(rw,[status(thm)],[t3072]) ).
cnf(t3014,plain,
or(not(c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X1,tc_RealDef_Oreal)),not(c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X1,tc_RealDef_Oreal))) = true,
inference(orient,[status(thm)],[t967]) ).
cnf(f382,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_y,tc_RealDef_Oreal)
| c_lessequals(V_x,V_y,tc_RealDef_Oreal) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_real__less__def_0) ).
fof(f382_nnf,plain,
! [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) ),
inference(nnf_transformation,[status(thm)],[f382]) ).
fof(f382_sk,plain,
! [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) ),
inference(skolemisation,[status(esa)],[f382_nnf]) ).
cnf(c382,plain,
( ~ c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal)
| c_lessequals(X0,X1,tc_RealDef_Oreal) ),
inference(cnf_transformation,[status(esa)],[f382_sk]) ).
cnf(t89,plain,
ifeq(c_HOL_Oord__class_Oless(X1,X2,tc_RealDef_Oreal),true,c_lessequals(X1,X2,tc_RealDef_Oreal),true) = true,
inference(equality_encoding,[status(esa)],[c382]) ).
cnf(t290,plain,
ifeq(c_HOL_Oord__class_Oless(X1,X2,tc_RealDef_Oreal),true,c_lessequals(X1,X2,tc_RealDef_Oreal),true) = true,
inference(orient,[status(thm)],[t89]) ).
cnf(f10,axiom,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),V_a,T_a)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Oplus__class_Oplus(V_a,V_a,T_a),T_a)
| ~ class_OrderedGroup_Olordered__ab__group__add(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_zero__less__double__add__iff__zero__less__single__add_1) ).
fof(f10_nnf,plain,
! [T_a,V_a] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),V_a,T_a)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Oplus__class_Oplus(V_a,V_a,T_a),T_a)
| ~ class_OrderedGroup_Olordered__ab__group__add(T_a) ),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [T_a,V_a] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),V_a,T_a)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Oplus__class_Oplus(V_a,V_a,T_a),T_a)
| ~ class_OrderedGroup_Olordered__ab__group__add(T_a) ),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c10,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(X0),X1,X0)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(X0),c_HOL_Oplus__class_Oplus(X1,X1,X0),X0)
| ~ class_OrderedGroup_Olordered__ab__group__add(X0) ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(hi10,axiom,
ifeq(class_OrderedGroup_Olordered__ab__group__add(X0),true,ifeq(c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(X0),X1,X0),true,c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(X0),c_HOL_Oplus__class_Oplus(X1,X1,X0),X0),true),true) = true,
inference(equality_encoding,[status(esa)],[c10]) ).
cnf(f448,axiom,
class_OrderedGroup_Olordered__ab__group__add(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_RealDef__Oreal__OrderedGroup_Olordered__ab__group__add) ).
fof(f448_nnf,plain,
class_OrderedGroup_Olordered__ab__group__add(tc_RealDef_Oreal),
inference(nnf_transformation,[status(thm)],[f448]) ).
cnf(c448,plain,
class_OrderedGroup_Olordered__ab__group__add(tc_RealDef_Oreal),
inference(cnf_transformation,[status(esa)],[f448_nnf]) ).
cnf(hi429,axiom,
class_OrderedGroup_Olordered__ab__group__add(tc_RealDef_Oreal) = true,
inference(equality_encoding,[status(esa)],[c448]) ).
cnf(f213,axiom,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealDef_Oreal__of__preal(V_xa),tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_real__gt__zero__preal__Ex_1) ).
fof(f213_nnf,plain,
! [V_xa] : c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealDef_Oreal__of__preal(V_xa),tc_RealDef_Oreal),
inference(nnf_transformation,[status(thm)],[f213]) ).
fof(f213_sk,plain,
! [V_xa] : c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealDef_Oreal__of__preal(V_xa),tc_RealDef_Oreal),
inference(skolemisation,[status(esa)],[f213_nnf]) ).
cnf(c213,plain,
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(esa)],[f213_sk]) ).
cnf(hi209,axiom,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealDef_Oreal__of__preal(X0),tc_RealDef_Oreal) = true,
inference(equality_encoding,[status(esa)],[c213]) ).
cnf(h46,plain,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_RealDef_Oreal__of__preal(V0),c_RealDef_Oreal__of__preal(V0),tc_RealDef_Oreal),tc_RealDef_Oreal) = true,
inference(hyper_resolution,[status(thm)],[hi10,hi429,hi209]) ).
cnf(f128,axiom,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),V_a,T_a)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Osgn__class_Osgn(V_a,T_a),T_a)
| ~ class_Ring__and__Field_Oordered__idom(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Rational_Oordered__idom__class_Osgn__greater_1) ).
fof(f128_nnf,plain,
! [T_a,V_a] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),V_a,T_a)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Osgn__class_Osgn(V_a,T_a),T_a)
| ~ class_Ring__and__Field_Oordered__idom(T_a) ),
inference(nnf_transformation,[status(thm)],[f128]) ).
fof(f128_sk,plain,
! [T_a,V_a] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),V_a,T_a)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Osgn__class_Osgn(V_a,T_a),T_a)
| ~ class_Ring__and__Field_Oordered__idom(T_a) ),
inference(skolemisation,[status(esa)],[f128_nnf]) ).
cnf(c128,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(X0),X1,X0)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(X0),c_HOL_Osgn__class_Osgn(X1,X0),X0)
| ~ class_Ring__and__Field_Oordered__idom(X0) ),
inference(cnf_transformation,[status(esa)],[f128_sk]) ).
cnf(hi125,axiom,
ifeq(class_Ring__and__Field_Oordered__idom(X0),true,ifeq(c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(X0),X1,X0),true,c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(X0),c_HOL_Osgn__class_Osgn(X1,X0),X0),true),true) = true,
inference(equality_encoding,[status(esa)],[c128]) ).
cnf(f468,axiom,
class_Ring__and__Field_Oordered__idom(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_RealDef__Oreal__Ring__and__Field_Oordered__idom) ).
fof(f468_nnf,plain,
class_Ring__and__Field_Oordered__idom(tc_RealDef_Oreal),
inference(nnf_transformation,[status(thm)],[f468]) ).
cnf(c468,plain,
class_Ring__and__Field_Oordered__idom(tc_RealDef_Oreal),
inference(cnf_transformation,[status(esa)],[f468_nnf]) ).
cnf(hi449,axiom,
class_Ring__and__Field_Oordered__idom(tc_RealDef_Oreal) = true,
inference(equality_encoding,[status(esa)],[c468]) ).
cnf(t96,plain,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Osgn__class_Osgn(c_HOL_Oplus__class_Oplus(c_RealDef_Oreal__of__preal(X1),c_RealDef_Oreal__of__preal(X1),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) = true,
inference(hyper_resolution,[status(thm)],[hi125,hi449,h46]) ).
cnf(t204,plain,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Osgn__class_Osgn(c_HOL_Oplus__class_Oplus(c_RealDef_Oreal__of__preal(X1),c_RealDef_Oreal__of__preal(X1),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) = true,
inference(orient,[status(thm)],[t96]) ).
cnf(t293,plain,
true = ifeq(true,true,c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Osgn__class_Osgn(c_HOL_Oplus__class_Oplus(c_RealDef_Oreal__of__preal(X1),c_RealDef_Oreal__of__preal(X1),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),true),
inference(cp,[status(thm)],[t290,t204]) ).
cnf(t36,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t171,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t36]) ).
cnf(t3178,plain,
true = c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Osgn__class_Osgn(c_HOL_Oplus__class_Oplus(c_RealDef_Oreal__of__preal(X1),c_RealDef_Oreal__of__preal(X1),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(step,[status(thm)],[t293,t171]) ).
cnf(t1961,plain,
c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Osgn__class_Osgn(c_HOL_Oplus__class_Oplus(c_RealDef_Oreal__of__preal(X1),c_RealDef_Oreal__of__preal(X1),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) = true,
inference(orient,[status(thm)],[t3178]) ).
cnf(t3023,plain,
true = or(not(true),not(c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Osgn__class_Osgn(c_HOL_Oplus__class_Oplus(c_RealDef_Oreal__of__preal(X1),c_RealDef_Oreal__of__preal(X1),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal))),
inference(cp,[status(thm)],[t3014,t1961]) ).
cnf(t6,plain,
not(true) = false,
introduced(definition) ).
cnf(t1039,plain,
not(true) = false,
inference(orient,[status(thm)],[t6]) ).
cnf(t3202,plain,
true = or(false,not(c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Osgn__class_Osgn(c_HOL_Oplus__class_Oplus(c_RealDef_Oreal__of__preal(X1),c_RealDef_Oreal__of__preal(X1),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal))),
inference(step,[status(thm)],[t3023,t1039]) ).
cnf(t19,plain,
or(false,X1) = X1,
introduced(definition) ).
cnf(t174,plain,
or(false,X1) = X1,
inference(orient,[status(thm)],[t19]) ).
cnf(t3203,plain,
true = not(c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Osgn__class_Osgn(c_HOL_Oplus__class_Oplus(c_RealDef_Oreal__of__preal(X1),c_RealDef_Oreal__of__preal(X1),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)),
inference(step,[status(thm)],[t3202,t174]) ).
cnf(t3204,plain,
true = not(true),
inference(step,[status(thm)],[t3203,t204]) ).
cnf(t3205,plain,
true = false,
inference(step,[status(thm)],[t3204,t1039]) ).
cnf(t3043,plain,
false = true,
inference(orient,[status(thm)],[t3205]) ).
cnf(f31,axiom,
( ~ 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/sandbox/benchmark/theBenchmark.p',cls_not__square__less__zero_0) ).
fof(f31_nnf,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(nnf_transformation,[status(thm)],[f31]) ).
fof(f31_sk,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(skolemisation,[status(esa)],[f31_nnf]) ).
cnf(c31,plain,
( ~ 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(esa)],[f31_sk]) ).
cnf(f89,axiom,
( ~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_x,V_x,T_a),c_HOL_Otimes__class_Otimes(V_y,V_y,T_a),T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__sum__squares__lt__zero_0) ).
fof(f89_nnf,plain,
! [T_a,V_x,V_y] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_x,V_x,T_a),c_HOL_Otimes__class_Otimes(V_y,V_y,T_a),T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
inference(nnf_transformation,[status(thm)],[f89]) ).
fof(f89_sk,plain,
! [T_a,V_x,V_y] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_x,V_x,T_a),c_HOL_Otimes__class_Otimes(V_y,V_y,T_a),T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
inference(skolemisation,[status(esa)],[f89_nnf]) ).
cnf(c89,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(X1,X1,X0),c_HOL_Otimes__class_Otimes(X2,X2,X0),X0),c_HOL_Ozero__class_Ozero(X0),X0)
| ~ class_Ring__and__Field_Oordered__ring__strict(X0) ),
inference(cnf_transformation,[status(esa)],[f89_sk]) ).
cnf(f96,axiom,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a),T_a),T_a)
| ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_sum__squares__gt__zero__iff_0) ).
fof(f96_nnf,plain,
! [T_a] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a),T_a),T_a)
| ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
inference(nnf_transformation,[status(thm)],[f96]) ).
fof(f96_sk,plain,
! [T_a] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a),T_a),T_a)
| ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
inference(skolemisation,[status(esa)],[f96_nnf]) ).
cnf(c96,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(X0),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(X0),c_HOL_Ozero__class_Ozero(X0),X0),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(X0),c_HOL_Ozero__class_Ozero(X0),X0),X0),X0)
| ~ class_Ring__and__Field_Oordered__ring__strict(X0) ),
inference(cnf_transformation,[status(esa)],[f96_sk]) ).
cnf(f211,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',cls_not__real__square__gt__zero_1) ).
fof(f211_nnf,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(nnf_transformation,[status(thm)],[f211]) ).
fof(f211_sk,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(skolemisation,[status(esa)],[f211_nnf]) ).
cnf(c211,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(esa)],[f211_sk]) ).
cnf(f365,axiom,
( ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
| ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| ~ class_Orderings_Oorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_xt1_I9_J_0) ).
fof(f365_nnf,plain,
! [T_a,V_a,V_b] :
( ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
| ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f365]) ).
fof(f365_sk,plain,
! [T_a,V_a,V_b] :
( ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
| ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(skolemisation,[status(esa)],[f365_nnf]) ).
cnf(c365,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(esa)],[f365_sk]) ).
cnf(f366,axiom,
( ~ 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',cls_not__less__iff__gr__or__eq_1) ).
fof(f366_nnf,plain,
! [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) ),
inference(nnf_transformation,[status(thm)],[f366]) ).
fof(f366_sk,plain,
! [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) ),
inference(skolemisation,[status(esa)],[f366_nnf]) ).
cnf(c366,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f366_sk]) ).
cnf(f369,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_order__less__asym_0) ).
fof(f369_nnf,plain,
! [T_a,V_y,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f369]) ).
fof(f369_sk,plain,
! [T_a,V_y,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(skolemisation,[status(esa)],[f369_nnf]) ).
cnf(c369,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f369_sk]) ).
cnf(f370,axiom,
( ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_order__less__asym_H_0) ).
fof(f370_nnf,plain,
! [T_a,V_b,V_a] :
( ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f370]) ).
fof(f370_sk,plain,
! [T_a,V_b,V_a] :
( ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(skolemisation,[status(esa)],[f370_nnf]) ).
cnf(c370,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f370_sk]) ).
cnf(f385,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_order__less__irrefl_0) ).
fof(f385_nnf,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f385]) ).
fof(f385_sk,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(skolemisation,[status(esa)],[f385_nnf]) ).
cnf(c385,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f385_sk]) ).
cnf(f386,axiom,
~ c_HOL_Oord__class_Oless(V_x,V_x,tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_real__less__def_1) ).
fof(f386_nnf,plain,
! [V_x] : ~ c_HOL_Oord__class_Oless(V_x,V_x,tc_RealDef_Oreal),
inference(nnf_transformation,[status(thm)],[f386]) ).
fof(f386_sk,plain,
! [V_x] : ~ c_HOL_Oord__class_Oless(V_x,V_x,tc_RealDef_Oreal),
inference(skolemisation,[status(esa)],[f386_nnf]) ).
cnf(c386,plain,
~ c_HOL_Oord__class_Oless(X0,X0,tc_RealDef_Oreal),
inference(cnf_transformation,[status(esa)],[f386_sk]) ).
cnf(f387,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Oorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_order__less__le_1) ).
fof(f387_nnf,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f387]) ).
fof(f387_sk,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(skolemisation,[status(esa)],[f387_nnf]) ).
cnf(c387,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(esa)],[f387_sk]) ).
cnf(f388,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_linorder__neq__iff_1) ).
fof(f388_nnf,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f388]) ).
fof(f388_sk,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f388_nnf]) ).
cnf(c388,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f388_sk]) ).
cnf(f412,axiom,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(T_a),T_a),tc_RealDef_Oreal)
| ~ class_RealVector_Oreal__normed__vector(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_zero__less__norm__iff_0) ).
fof(f412_nnf,plain,
! [T_a] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(T_a),T_a),tc_RealDef_Oreal)
| ~ class_RealVector_Oreal__normed__vector(T_a) ),
inference(nnf_transformation,[status(thm)],[f412]) ).
fof(f412_sk,plain,
! [T_a] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(T_a),T_a),tc_RealDef_Oreal)
| ~ class_RealVector_Oreal__normed__vector(T_a) ),
inference(skolemisation,[status(esa)],[f412_nnf]) ).
cnf(c412,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(X0),X0),tc_RealDef_Oreal)
| ~ class_RealVector_Oreal__normed__vector(X0) ),
inference(cnf_transformation,[status(esa)],[f412_sk]) ).
cnf(f416,axiom,
( ~ c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(V_x,T_a),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ class_RealVector_Oreal__normed__vector(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_norm__not__less__zero_0) ).
fof(f416_nnf,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(V_x,T_a),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ class_RealVector_Oreal__normed__vector(T_a) ),
inference(nnf_transformation,[status(thm)],[f416]) ).
fof(f416_sk,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(V_x,T_a),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ class_RealVector_Oreal__normed__vector(T_a) ),
inference(skolemisation,[status(esa)],[f416_nnf]) ).
cnf(c416,plain,
( ~ c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(X1,X0),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ class_RealVector_Oreal__normed__vector(X0) ),
inference(cnf_transformation,[status(esa)],[f416_sk]) ).
cnf(f419,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ c_lessequals(V_y,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_less__le__not__le_1) ).
fof(f419_nnf,plain,
! [T_a,V_y,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ c_lessequals(V_y,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f419]) ).
fof(f419_sk,plain,
! [T_a,V_y,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ c_lessequals(V_y,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(skolemisation,[status(esa)],[f419_nnf]) ).
cnf(c419,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_lessequals(X1,X2,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f419_sk]) ).
cnf(f421,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ c_lessequals(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_linorder__antisym__conv2_1) ).
fof(f421_nnf,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ c_lessequals(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f421]) ).
fof(f421_sk,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ c_lessequals(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f421_nnf]) ).
cnf(c421,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ c_lessequals(X1,X1,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f421_sk]) ).
cnf(f423,axiom,
( ~ c_lessequals(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',cls_linorder__not__less_1) ).
fof(f423_nnf,plain,
! [T_a,V_x,V_y] :
( ~ c_lessequals(V_y,V_x,T_a)
| ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f423]) ).
fof(f423_sk,plain,
! [T_a,V_x,V_y] :
( ~ c_lessequals(V_y,V_x,T_a)
| ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f423_nnf]) ).
cnf(c423,plain,
( ~ c_lessequals(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f423_sk]) ).
cnf(f426,axiom,
( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ c_lessequals(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_linorder__not__le_1) ).
fof(f426_nnf,plain,
! [T_a,V_x,V_y] :
( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ c_lessequals(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f426]) ).
fof(f426_sk,plain,
! [T_a,V_x,V_y] :
( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ c_lessequals(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f426_nnf]) ).
cnf(c426,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_lessequals(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f426_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c31,c89,c96,c211,c365,c366,c369,c370,c385,c386,c387,c388,c412,c416,c419,c421,c423,c426,c428]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t3043]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : ALG340-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.02 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.08/0.34 % Computer : n011.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.03/18.50 % CPULimit : 300
% 0.03/18.50 % WCLimit : 300
% 0.03/18.50 % DateTime : Fri Sep 25 05:26:04 UTC 2026
% 0.03/18.50 % CPUTime :
% 0.03/18.50 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 23.64/21.82 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 23.64/21.82 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------