%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : ALG385-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 : n008.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:26 PM UTC 2026
% Result : Unsatisfiable 65.18s 8.69s
% Output : Proof 65.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 39
% Syntax : Number of formulae : 203 ( 95 unt; 0 def)
% Number of atoms : 347 ( 97 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 402 ( 258 ~; 144 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 16 ( 14 usr; 1 prp; 0-3 aty)
% Number of functors : 21 ( 21 usr; 9 con; 0-4 aty)
% Number of variables : 348 ( 34 sgn 132 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f878,negated_conjecture,
~ c_lessequals(v_da____,c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(c_Polynomial_OpCons(v_aa____,c_Polynomial_OpCons(v_c____,v_cs____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_z____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f878_nnf,plain,
~ c_lessequals(v_da____,c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(c_Polynomial_OpCons(v_aa____,c_Polynomial_OpCons(v_c____,v_cs____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_z____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),
inference(nnf_transformation,[status(thm)],[f878]) ).
fof(f878_sk,plain,
~ c_lessequals(v_da____,c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(c_Polynomial_OpCons(v_aa____,c_Polynomial_OpCons(v_c____,v_cs____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_z____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),
inference(skolemisation,[status(esa)],[f878_nnf]) ).
cnf(c878,plain,
~ c_lessequals(v_da____,c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(c_Polynomial_OpCons(v_aa____,c_Polynomial_OpCons(v_c____,v_cs____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_z____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),
inference(cnf_transformation,[status(esa)],[f878_sk]) ).
cnf(t132,plain,
c_lessequals(v_da____,c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(c_Polynomial_OpCons(v_aa____,c_Polynomial_OpCons(v_c____,v_cs____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_z____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal) = false,
inference(equality_encoding,[status(esa)],[c878]) ).
cnf(t1256,plain,
c_lessequals(v_da____,c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(c_Polynomial_OpCons(v_aa____,c_Polynomial_OpCons(v_c____,v_cs____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_z____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal) = false,
inference(orient,[status(thm)],[t132]) ).
cnf(f843,axiom,
( c_Polynomial_Opoly(c_Polynomial_OpCons(V_a,V_p,T_a),V_x,T_a) = c_HOL_Oplus__class_Oplus(V_a,c_HOL_Otimes__class_Otimes(V_x,c_Polynomial_Opoly(V_p,V_x,T_a),T_a),T_a)
| ~ class_Ring__and__Field_Ocomm__semiring__0(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_poly__pCons_0) ).
fof(f843_nnf,plain,
! [T_a,V_a,V_p,V_x] :
( c_Polynomial_Opoly(c_Polynomial_OpCons(V_a,V_p,T_a),V_x,T_a) = c_HOL_Oplus__class_Oplus(V_a,c_HOL_Otimes__class_Otimes(V_x,c_Polynomial_Opoly(V_p,V_x,T_a),T_a),T_a)
| ~ class_Ring__and__Field_Ocomm__semiring__0(T_a) ),
inference(nnf_transformation,[status(thm)],[f843]) ).
fof(f843_sk,plain,
! [T_a,V_a,V_p,V_x] :
( c_Polynomial_Opoly(c_Polynomial_OpCons(V_a,V_p,T_a),V_x,T_a) = c_HOL_Oplus__class_Oplus(V_a,c_HOL_Otimes__class_Otimes(V_x,c_Polynomial_Opoly(V_p,V_x,T_a),T_a),T_a)
| ~ class_Ring__and__Field_Ocomm__semiring__0(T_a) ),
inference(skolemisation,[status(esa)],[f843_nnf]) ).
cnf(c843,plain,
( c_Polynomial_Opoly(c_Polynomial_OpCons(X1,X2,X0),X3,X0) = c_HOL_Oplus__class_Oplus(X1,c_HOL_Otimes__class_Otimes(X3,c_Polynomial_Opoly(X2,X3,X0),X0),X0)
| ~ class_Ring__and__Field_Ocomm__semiring__0(X0) ),
inference(cnf_transformation,[status(esa)],[f843_sk]) ).
cnf(hi818,axiom,
ifeq(class_Ring__and__Field_Ocomm__semiring__0(X0),true,c_Polynomial_Opoly(c_Polynomial_OpCons(X1,X2,X0),X3,X0),c_HOL_Oplus__class_Oplus(X1,c_HOL_Otimes__class_Otimes(X3,c_Polynomial_Opoly(X2,X3,X0),X0),X0)) = c_HOL_Oplus__class_Oplus(X1,c_HOL_Otimes__class_Otimes(X3,c_Polynomial_Opoly(X2,X3,X0),X0),X0),
inference(equality_encoding,[status(esa)],[c843]) ).
cnf(f961,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(f961_nnf,plain,
class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex),
inference(nnf_transformation,[status(thm)],[f961]) ).
cnf(c961,plain,
class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(esa)],[f961_nnf]) ).
cnf(hi933,axiom,
class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex) = true,
inference(equality_encoding,[status(esa)],[c961]) ).
cnf(t137,plain,
c_HOL_Oplus__class_Oplus(X1,c_HOL_Otimes__class_Otimes(X2,c_Polynomial_Opoly(X3,X2,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_Polynomial_Opoly(c_Polynomial_OpCons(X1,X3,tc_Complex_Ocomplex),X2,tc_Complex_Ocomplex),
inference(hyper_resolution,[status(thm)],[hi818,hi933]) ).
cnf(f450,axiom,
( c_Polynomial_Opoly(c_Polynomial_Osmult(V_a,V_p,T_a),V_x,T_a) = c_HOL_Otimes__class_Otimes(V_a,c_Polynomial_Opoly(V_p,V_x,T_a),T_a)
| ~ class_Ring__and__Field_Ocomm__semiring__0(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_poly__smult_0) ).
fof(f450_nnf,plain,
! [T_a,V_a,V_p,V_x] :
( c_Polynomial_Opoly(c_Polynomial_Osmult(V_a,V_p,T_a),V_x,T_a) = c_HOL_Otimes__class_Otimes(V_a,c_Polynomial_Opoly(V_p,V_x,T_a),T_a)
| ~ class_Ring__and__Field_Ocomm__semiring__0(T_a) ),
inference(nnf_transformation,[status(thm)],[f450]) ).
fof(f450_sk,plain,
! [T_a,V_a,V_p,V_x] :
( c_Polynomial_Opoly(c_Polynomial_Osmult(V_a,V_p,T_a),V_x,T_a) = c_HOL_Otimes__class_Otimes(V_a,c_Polynomial_Opoly(V_p,V_x,T_a),T_a)
| ~ class_Ring__and__Field_Ocomm__semiring__0(T_a) ),
inference(skolemisation,[status(esa)],[f450_nnf]) ).
cnf(c450,plain,
( c_Polynomial_Opoly(c_Polynomial_Osmult(X1,X2,X0),X3,X0) = c_HOL_Otimes__class_Otimes(X1,c_Polynomial_Opoly(X2,X3,X0),X0)
| ~ class_Ring__and__Field_Ocomm__semiring__0(X0) ),
inference(cnf_transformation,[status(esa)],[f450_sk]) ).
cnf(hi441,axiom,
ifeq(class_Ring__and__Field_Ocomm__semiring__0(X0),true,c_Polynomial_Opoly(c_Polynomial_Osmult(X1,X2,X0),X3,X0),c_HOL_Otimes__class_Otimes(X1,c_Polynomial_Opoly(X2,X3,X0),X0)) = c_HOL_Otimes__class_Otimes(X1,c_Polynomial_Opoly(X2,X3,X0),X0),
inference(equality_encoding,[status(esa)],[c450]) ).
cnf(t113,plain,
c_Polynomial_Opoly(c_Polynomial_Osmult(X1,X2,tc_Complex_Ocomplex),X3,tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(X1,c_Polynomial_Opoly(X2,X3,tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(hyper_resolution,[status(thm)],[hi441,hi933]) ).
cnf(t854,plain,
c_HOL_Otimes__class_Otimes(X1,c_Polynomial_Opoly(X2,X3,tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_Polynomial_Opoly(c_Polynomial_Osmult(X1,X2,tc_Complex_Ocomplex),X3,tc_Complex_Ocomplex),
inference(orient,[status(thm)],[t113]) ).
cnf(t7357,plain,
c_HOL_Oplus__class_Oplus(X1,c_Polynomial_Opoly(c_Polynomial_Osmult(X2,X3,tc_Complex_Ocomplex),X2,tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_Polynomial_Opoly(c_Polynomial_OpCons(X1,X3,tc_Complex_Ocomplex),X2,tc_Complex_Ocomplex),
inference(step,[status(thm)],[t137,t854]) ).
cnf(t1006,plain,
c_HOL_Oplus__class_Oplus(X1,c_Polynomial_Opoly(c_Polynomial_Osmult(X2,X3,tc_Complex_Ocomplex),X2,tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_Polynomial_Opoly(c_Polynomial_OpCons(X1,X3,tc_Complex_Ocomplex),X2,tc_Complex_Ocomplex),
inference(orient,[status(thm)],[t7357]) ).
cnf(f719,axiom,
( c_Polynomial_Osmult(V_a,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)),T_a) = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))
| ~ class_Ring__and__Field_Ocomm__semiring__0(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_smult__0__right_0) ).
fof(f719_nnf,plain,
! [T_a,V_a] :
( c_Polynomial_Osmult(V_a,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)),T_a) = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))
| ~ class_Ring__and__Field_Ocomm__semiring__0(T_a) ),
inference(nnf_transformation,[status(thm)],[f719]) ).
fof(f719_sk,plain,
! [T_a,V_a] :
( c_Polynomial_Osmult(V_a,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)),T_a) = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))
| ~ class_Ring__and__Field_Ocomm__semiring__0(T_a) ),
inference(skolemisation,[status(esa)],[f719_nnf]) ).
cnf(c719,plain,
( c_Polynomial_Osmult(X1,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)),X0) = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0))
| ~ class_Ring__and__Field_Ocomm__semiring__0(X0) ),
inference(cnf_transformation,[status(esa)],[f719_sk]) ).
cnf(t135,plain,
ifeq(class_Ring__and__Field_Ocomm__semiring__0(X1),true,c_Polynomial_Osmult(X2,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X1)),X1),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X1))) = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X1)),
inference(equality_encoding,[status(esa)],[c719]) ).
cnf(t596,plain,
ifeq(class_Ring__and__Field_Ocomm__semiring__0(X1),true,c_Polynomial_Osmult(X2,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X1)),X1),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X1))) = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X1)),
inference(orient,[status(thm)],[t135]) ).
cnf(f847,axiom,
v_cs____ = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_cs0_0) ).
fof(f847_nnf,plain,
v_cs____ = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(nnf_transformation,[status(thm)],[f847]) ).
cnf(c847,plain,
v_cs____ = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(cnf_transformation,[status(esa)],[f847_nnf]) ).
cnf(t3,plain,
c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = v_cs____,
inference(equality_encoding,[status(esa)],[c847]) ).
cnf(t619,plain,
c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = v_cs____,
inference(orient,[status(thm)],[t3]) ).
cnf(t623,plain,
c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = ifeq(class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex),true,c_Polynomial_Osmult(X1,v_cs____,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))),
inference(cp,[status(thm)],[t596,t619]) ).
cnf(t7373,plain,
v_cs____ = ifeq(class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex),true,c_Polynomial_Osmult(X1,v_cs____,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))),
inference(step,[status(thm)],[t623,t619]) ).
cnf(t0,plain,
class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex) = true,
inference(equality_encoding,[status(esa)],[c961]) ).
cnf(t508,plain,
class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex) = true,
inference(orient,[status(thm)],[t0]) ).
cnf(t7374,plain,
v_cs____ = ifeq(true,true,c_Polynomial_Osmult(X1,v_cs____,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))),
inference(step,[status(thm)],[t7373,t508]) ).
cnf(t29,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t220,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t29]) ).
cnf(t7375,plain,
v_cs____ = c_Polynomial_Osmult(X1,v_cs____,tc_Complex_Ocomplex),
inference(step,[status(thm)],[t7374,t220]) ).
cnf(t1562,plain,
c_Polynomial_Osmult(X1,v_cs____,tc_Complex_Ocomplex) = v_cs____,
inference(orient,[status(thm)],[t7375]) ).
cnf(t1568,plain,
c_Polynomial_Opoly(c_Polynomial_OpCons(X1,v_cs____,tc_Complex_Ocomplex),X2,tc_Complex_Ocomplex) = c_HOL_Oplus__class_Oplus(X1,c_Polynomial_Opoly(v_cs____,X2,tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(cp,[status(thm)],[t1006,t1562]) ).
cnf(f313,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(f313_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)],[f313]) ).
fof(f313_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)],[f313_nnf]) ).
cnf(c313,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)],[f313_sk]) ).
cnf(t118,plain,
ifeq(class_Ring__and__Field_Ocomm__semiring__0(X1),true,c_Polynomial_Opoly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X1)),X2,X1),c_HOL_Ozero__class_Ozero(X1)) = c_HOL_Ozero__class_Ozero(X1),
inference(equality_encoding,[status(esa)],[c313]) ).
cnf(t528,plain,
ifeq(class_Ring__and__Field_Ocomm__semiring__0(X1),true,c_Polynomial_Opoly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X1)),X2,X1),c_HOL_Ozero__class_Ozero(X1)) = c_HOL_Ozero__class_Ozero(X1),
inference(orient,[status(thm)],[t118]) ).
cnf(t630,plain,
c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = ifeq(class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex),true,c_Polynomial_Opoly(v_cs____,X1,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)),
inference(cp,[status(thm)],[t528,t619]) ).
cnf(t7376,plain,
c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = ifeq(true,true,c_Polynomial_Opoly(v_cs____,X1,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)),
inference(step,[status(thm)],[t630,t508]) ).
cnf(t7377,plain,
c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = c_Polynomial_Opoly(v_cs____,X1,tc_Complex_Ocomplex),
inference(step,[status(thm)],[t7376,t220]) ).
cnf(t1572,plain,
c_Polynomial_Opoly(v_cs____,X1,tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(orient,[status(thm)],[t7377]) ).
cnf(t7473,plain,
c_Polynomial_Opoly(c_Polynomial_OpCons(X1,v_cs____,tc_Complex_Ocomplex),X2,tc_Complex_Ocomplex) = c_HOL_Oplus__class_Oplus(X1,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(step,[status(thm)],[t1568,t1572]) ).
cnf(f598,axiom,
( c_HOL_Oplus__class_Oplus(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) = V_a
| ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_class__semiring_Osemiring__rules_I6_J_0) ).
fof(f598_nnf,plain,
! [T_a,V_a] :
( c_HOL_Oplus__class_Oplus(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) = V_a
| ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) ),
inference(nnf_transformation,[status(thm)],[f598]) ).
fof(f598_sk,plain,
! [T_a,V_a] :
( c_HOL_Oplus__class_Oplus(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) = V_a
| ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) ),
inference(skolemisation,[status(esa)],[f598_nnf]) ).
cnf(c598,plain,
( c_HOL_Oplus__class_Oplus(X1,c_HOL_Ozero__class_Ozero(X0),X0) = X1
| ~ class_Ring__and__Field_Ocomm__semiring__1(X0) ),
inference(cnf_transformation,[status(esa)],[f598_sk]) ).
cnf(hi584,axiom,
ifeq(class_Ring__and__Field_Ocomm__semiring__1(X0),true,c_HOL_Oplus__class_Oplus(X1,c_HOL_Ozero__class_Ozero(X0),X0),X1) = X1,
inference(equality_encoding,[status(esa)],[c598]) ).
cnf(f960,axiom,
class_Ring__and__Field_Ocomm__semiring__1(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_Complex__Ocomplex__Ring__and__Field_Ocomm__semiring__1) ).
fof(f960_nnf,plain,
class_Ring__and__Field_Ocomm__semiring__1(tc_Complex_Ocomplex),
inference(nnf_transformation,[status(thm)],[f960]) ).
cnf(c960,plain,
class_Ring__and__Field_Ocomm__semiring__1(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(esa)],[f960_nnf]) ).
cnf(hi932,axiom,
class_Ring__and__Field_Ocomm__semiring__1(tc_Complex_Ocomplex) = true,
inference(equality_encoding,[status(esa)],[c960]) ).
cnf(t21,plain,
c_HOL_Oplus__class_Oplus(X1,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex) = X1,
inference(hyper_resolution,[status(thm)],[hi584,hi932]) ).
cnf(t197,plain,
c_HOL_Oplus__class_Oplus(X1,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex) = X1,
inference(orient,[status(thm)],[t21]) ).
cnf(t7474,plain,
c_Polynomial_Opoly(c_Polynomial_OpCons(X1,v_cs____,tc_Complex_Ocomplex),X2,tc_Complex_Ocomplex) = X1,
inference(step,[status(thm)],[t7473,t197]) ).
cnf(t2268,plain,
c_Polynomial_Opoly(c_Polynomial_OpCons(X1,v_cs____,tc_Complex_Ocomplex),X2,tc_Complex_Ocomplex) = X1,
inference(orient,[status(thm)],[t7474]) ).
cnf(f110,axiom,
( c_Polynomial_Osmult(V_a,c_Polynomial_OpCons(V_b,V_p,T_a),T_a) = c_Polynomial_OpCons(c_HOL_Otimes__class_Otimes(V_a,V_b,T_a),c_Polynomial_Osmult(V_a,V_p,T_a),T_a)
| ~ class_Ring__and__Field_Ocomm__semiring__0(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_smult__pCons_0) ).
fof(f110_nnf,plain,
! [T_a,V_a,V_b,V_p] :
( c_Polynomial_Osmult(V_a,c_Polynomial_OpCons(V_b,V_p,T_a),T_a) = c_Polynomial_OpCons(c_HOL_Otimes__class_Otimes(V_a,V_b,T_a),c_Polynomial_Osmult(V_a,V_p,T_a),T_a)
| ~ class_Ring__and__Field_Ocomm__semiring__0(T_a) ),
inference(nnf_transformation,[status(thm)],[f110]) ).
fof(f110_sk,plain,
! [T_a,V_a,V_b,V_p] :
( c_Polynomial_Osmult(V_a,c_Polynomial_OpCons(V_b,V_p,T_a),T_a) = c_Polynomial_OpCons(c_HOL_Otimes__class_Otimes(V_a,V_b,T_a),c_Polynomial_Osmult(V_a,V_p,T_a),T_a)
| ~ class_Ring__and__Field_Ocomm__semiring__0(T_a) ),
inference(skolemisation,[status(esa)],[f110_nnf]) ).
cnf(c110,plain,
( c_Polynomial_Osmult(X1,c_Polynomial_OpCons(X2,X3,X0),X0) = c_Polynomial_OpCons(c_HOL_Otimes__class_Otimes(X1,X2,X0),c_Polynomial_Osmult(X1,X3,X0),X0)
| ~ class_Ring__and__Field_Ocomm__semiring__0(X0) ),
inference(cnf_transformation,[status(esa)],[f110_sk]) ).
cnf(hi105,axiom,
ifeq(class_Ring__and__Field_Ocomm__semiring__0(X0),true,c_Polynomial_Osmult(X1,c_Polynomial_OpCons(X2,X3,X0),X0),c_Polynomial_OpCons(c_HOL_Otimes__class_Otimes(X1,X2,X0),c_Polynomial_Osmult(X1,X3,X0),X0)) = c_Polynomial_OpCons(c_HOL_Otimes__class_Otimes(X1,X2,X0),c_Polynomial_Osmult(X1,X3,X0),X0),
inference(equality_encoding,[status(esa)],[c110]) ).
cnf(t142,plain,
c_Polynomial_OpCons(c_HOL_Otimes__class_Otimes(X1,X2,tc_Complex_Ocomplex),c_Polynomial_Osmult(X1,X3,tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_Polynomial_Osmult(X1,c_Polynomial_OpCons(X2,X3,tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(hyper_resolution,[status(thm)],[hi105,hi933]) ).
cnf(t1360,plain,
c_Polynomial_OpCons(c_HOL_Otimes__class_Otimes(X1,X2,tc_Complex_Ocomplex),c_Polynomial_Osmult(X1,X3,tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_Polynomial_Osmult(X1,c_Polynomial_OpCons(X2,X3,tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(orient,[status(thm)],[t142]) ).
cnf(t1563,plain,
c_Polynomial_Osmult(X1,c_Polynomial_OpCons(X2,v_cs____,tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_Polynomial_OpCons(c_HOL_Otimes__class_Otimes(X1,X2,tc_Complex_Ocomplex),v_cs____,tc_Complex_Ocomplex),
inference(cp,[status(thm)],[t1360,t1562]) ).
cnf(t2259,plain,
c_Polynomial_OpCons(c_HOL_Otimes__class_Otimes(X1,X2,tc_Complex_Ocomplex),v_cs____,tc_Complex_Ocomplex) = c_Polynomial_Osmult(X1,c_Polynomial_OpCons(X2,v_cs____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(orient,[status(thm)],[t1563]) ).
cnf(t2269,plain,
c_HOL_Otimes__class_Otimes(X1,X2,tc_Complex_Ocomplex) = c_Polynomial_Opoly(c_Polynomial_Osmult(X1,c_Polynomial_OpCons(X2,v_cs____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),X3,tc_Complex_Ocomplex),
inference(cp,[status(thm)],[t2268,t2259]) ).
cnf(t3148,plain,
c_Polynomial_Opoly(c_Polynomial_Osmult(X1,c_Polynomial_OpCons(X2,v_cs____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),X3,tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(X1,X2,tc_Complex_Ocomplex),
inference(orient,[status(thm)],[t2269]) ).
cnf(t3155,plain,
c_Polynomial_Opoly(c_Polynomial_OpCons(X1,c_Polynomial_OpCons(X2,v_cs____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),X3,tc_Complex_Ocomplex) = c_HOL_Oplus__class_Oplus(X1,c_HOL_Otimes__class_Otimes(X3,X2,tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(cp,[status(thm)],[t1006,t3148]) ).
cnf(t7304,plain,
c_Polynomial_Opoly(c_Polynomial_OpCons(X1,c_Polynomial_OpCons(X2,v_cs____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),X3,tc_Complex_Ocomplex) = c_HOL_Oplus__class_Oplus(X1,c_HOL_Otimes__class_Otimes(X3,X2,tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(orient,[status(thm)],[t3155]) ).
cnf(t7665,plain,
c_lessequals(v_da____,c_RealVector_Onorm__class_Onorm(c_HOL_Oplus__class_Oplus(v_aa____,c_HOL_Otimes__class_Otimes(v_z____,v_c____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal) = false,
inference(step,[status(thm)],[t1256,t7304]) ).
cnf(f877,axiom,
c_lessequals(v_da____,c_RealVector_Onorm__class_Onorm(c_HOL_Oplus__class_Oplus(v_aa____,c_HOL_Otimes__class_Otimes(v_z____,v_c____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_CHAINED_0_01) ).
fof(f877_nnf,plain,
c_lessequals(v_da____,c_RealVector_Onorm__class_Onorm(c_HOL_Oplus__class_Oplus(v_aa____,c_HOL_Otimes__class_Otimes(v_z____,v_c____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),
inference(nnf_transformation,[status(thm)],[f877]) ).
cnf(c877,plain,
c_lessequals(v_da____,c_RealVector_Onorm__class_Onorm(c_HOL_Oplus__class_Oplus(v_aa____,c_HOL_Otimes__class_Otimes(v_z____,v_c____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),
inference(cnf_transformation,[status(esa)],[f877_nnf]) ).
cnf(t99,plain,
c_lessequals(v_da____,c_RealVector_Onorm__class_Onorm(c_HOL_Oplus__class_Oplus(v_aa____,c_HOL_Otimes__class_Otimes(v_z____,v_c____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal) = true,
inference(equality_encoding,[status(esa)],[c877]) ).
cnf(t477,plain,
c_lessequals(v_da____,c_RealVector_Onorm__class_Onorm(c_HOL_Oplus__class_Oplus(v_aa____,c_HOL_Otimes__class_Otimes(v_z____,v_c____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal) = true,
inference(orient,[status(thm)],[t99]) ).
cnf(t7666,plain,
true = false,
inference(step,[status(thm)],[t7665,t477]) ).
cnf(t7314,plain,
true = false,
inference(rw,[status(thm)],[t7666]) ).
cnf(t7315,plain,
false = true,
inference(orient,[status(thm)],[t7314]) ).
cnf(f35,axiom,
( ~ 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',cls_real__sqrt__not__eq__zero_0) ).
fof(f35_nnf,plain,
! [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) ),
inference(nnf_transformation,[status(thm)],[f35]) ).
fof(f35_sk,plain,
! [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) ),
inference(skolemisation,[status(esa)],[f35_nnf]) ).
cnf(c35,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)
| c_NthRoot_Osqrt(X0) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
inference(cnf_transformation,[status(esa)],[f35_sk]) ).
cnf(f42,axiom,
~ c_HOL_Oord__class_Oless(c_Transcendental_Oexp(V_x,tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__exp__less__zero_0) ).
fof(f42_nnf,plain,
! [V_x] : ~ c_HOL_Oord__class_Oless(c_Transcendental_Oexp(V_x,tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(nnf_transformation,[status(thm)],[f42]) ).
fof(f42_sk,plain,
! [V_x] : ~ c_HOL_Oord__class_Oless(c_Transcendental_Oexp(V_x,tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(skolemisation,[status(esa)],[f42_nnf]) ).
cnf(c42,plain,
~ c_HOL_Oord__class_Oless(c_Transcendental_Oexp(X0,tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(cnf_transformation,[status(esa)],[f42_sk]) ).
cnf(f45,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(f45_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)],[f45]) ).
fof(f45_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)],[f45_nnf]) ).
cnf(c45,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)],[f45_sk]) ).
cnf(f58,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(f58_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)],[f58]) ).
fof(f58_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)],[f58_nnf]) ).
cnf(c58,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)],[f58_sk]) ).
cnf(f63,axiom,
( ~ c_Polynomial_Opos__poly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)),T_a)
| ~ class_Ring__and__Field_Oordered__idom(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__pos__poly__0_0) ).
fof(f63_nnf,plain,
! [T_a] :
( ~ c_Polynomial_Opos__poly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)),T_a)
| ~ class_Ring__and__Field_Oordered__idom(T_a) ),
inference(nnf_transformation,[status(thm)],[f63]) ).
fof(f63_sk,plain,
! [T_a] :
( ~ c_Polynomial_Opos__poly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)),T_a)
| ~ class_Ring__and__Field_Oordered__idom(T_a) ),
inference(skolemisation,[status(esa)],[f63_nnf]) ).
cnf(c63,plain,
( ~ c_Polynomial_Opos__poly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)),X0)
| ~ class_Ring__and__Field_Oordered__idom(X0) ),
inference(cnf_transformation,[status(esa)],[f63_sk]) ).
cnf(f169,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(f169_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)],[f169]) ).
fof(f169_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)],[f169_nnf]) ).
cnf(c169,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)],[f169_sk]) ).
cnf(f233,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(f233_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)],[f233]) ).
fof(f233_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)],[f233_nnf]) ).
cnf(c233,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)],[f233_sk]) ).
cnf(f261,axiom,
~ c_lessequals(c_Transcendental_Oexp(V_x,tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__exp__le__zero_0) ).
fof(f261_nnf,plain,
! [V_x] : ~ c_lessequals(c_Transcendental_Oexp(V_x,tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(nnf_transformation,[status(thm)],[f261]) ).
fof(f261_sk,plain,
! [V_x] : ~ c_lessequals(c_Transcendental_Oexp(V_x,tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(skolemisation,[status(esa)],[f261_nnf]) ).
cnf(c261,plain,
~ c_lessequals(c_Transcendental_Oexp(X0,tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(cnf_transformation,[status(esa)],[f261_sk]) ).
cnf(f338,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(f338_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)],[f338]) ).
fof(f338_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)],[f338_nnf]) ).
cnf(c338,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)],[f338_sk]) ).
cnf(f465,axiom,
( c_Transcendental_Oexp(V_x,T_a) != c_HOL_Ozero__class_Ozero(T_a)
| ~ class_RealVector_Oreal__normed__field(T_a)
| ~ class_SEQ_Obanach(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_exp__not__eq__zero_0) ).
fof(f465_nnf,plain,
! [T_a,V_x] :
( c_Transcendental_Oexp(V_x,T_a) != c_HOL_Ozero__class_Ozero(T_a)
| ~ class_RealVector_Oreal__normed__field(T_a)
| ~ class_SEQ_Obanach(T_a) ),
inference(nnf_transformation,[status(thm)],[f465]) ).
fof(f465_sk,plain,
! [T_a,V_x] :
( c_Transcendental_Oexp(V_x,T_a) != c_HOL_Ozero__class_Ozero(T_a)
| ~ class_RealVector_Oreal__normed__field(T_a)
| ~ class_SEQ_Obanach(T_a) ),
inference(skolemisation,[status(esa)],[f465_nnf]) ).
cnf(c465,plain,
( c_Transcendental_Oexp(X1,X0) != c_HOL_Ozero__class_Ozero(X0)
| ~ class_RealVector_Oreal__normed__field(X0)
| ~ class_SEQ_Obanach(X0) ),
inference(cnf_transformation,[status(esa)],[f465_sk]) ).
cnf(f513,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(f513_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)],[f513]) ).
fof(f513_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)],[f513_nnf]) ).
cnf(c513,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)],[f513_sk]) ).
cnf(f573,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(f573_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)],[f573]) ).
fof(f573_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)],[f573_nnf]) ).
cnf(c573,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f573_sk]) ).
cnf(f574,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(f574_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)],[f574]) ).
fof(f574_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)],[f574_nnf]) ).
cnf(c574,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(esa)],[f574_sk]) ).
cnf(f575,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(f575_nnf,plain,
! [V_x] : ~ c_HOL_Oord__class_Oless(V_x,V_x,tc_RealDef_Oreal),
inference(nnf_transformation,[status(thm)],[f575]) ).
fof(f575_sk,plain,
! [V_x] : ~ c_HOL_Oord__class_Oless(V_x,V_x,tc_RealDef_Oreal),
inference(skolemisation,[status(esa)],[f575_nnf]) ).
cnf(c575,plain,
~ c_HOL_Oord__class_Oless(X0,X0,tc_RealDef_Oreal),
inference(cnf_transformation,[status(esa)],[f575_sk]) ).
cnf(f676,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(f676_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)],[f676]) ).
fof(f676_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)],[f676_nnf]) ).
cnf(c676,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f676_sk]) ).
cnf(f698,axiom,
( ~ c_HOL_Oord__class_Oless(c_HOL_Oabs__class_Oabs(V_a,T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_OrderedGroup_Opordered__ab__group__add__abs(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_abs__not__less__zero_0) ).
fof(f698_nnf,plain,
! [T_a,V_a] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Oabs__class_Oabs(V_a,T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_OrderedGroup_Opordered__ab__group__add__abs(T_a) ),
inference(nnf_transformation,[status(thm)],[f698]) ).
fof(f698_sk,plain,
! [T_a,V_a] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Oabs__class_Oabs(V_a,T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_OrderedGroup_Opordered__ab__group__add__abs(T_a) ),
inference(skolemisation,[status(esa)],[f698_nnf]) ).
cnf(c698,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Oabs__class_Oabs(X1,X0),c_HOL_Ozero__class_Ozero(X0),X0)
| ~ class_OrderedGroup_Opordered__ab__group__add__abs(X0) ),
inference(cnf_transformation,[status(esa)],[f698_sk]) ).
cnf(f736,axiom,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Oabs__class_Oabs(c_HOL_Ozero__class_Ozero(T_a),T_a),T_a)
| ~ class_OrderedGroup_Opordered__ab__group__add__abs(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_zero__less__abs__iff_0) ).
fof(f736_nnf,plain,
! [T_a] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Oabs__class_Oabs(c_HOL_Ozero__class_Ozero(T_a),T_a),T_a)
| ~ class_OrderedGroup_Opordered__ab__group__add__abs(T_a) ),
inference(nnf_transformation,[status(thm)],[f736]) ).
fof(f736_sk,plain,
! [T_a] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Oabs__class_Oabs(c_HOL_Ozero__class_Ozero(T_a),T_a),T_a)
| ~ class_OrderedGroup_Opordered__ab__group__add__abs(T_a) ),
inference(skolemisation,[status(esa)],[f736_nnf]) ).
cnf(c736,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(X0),c_HOL_Oabs__class_Oabs(c_HOL_Ozero__class_Ozero(X0),X0),X0)
| ~ class_OrderedGroup_Opordered__ab__group__add__abs(X0) ),
inference(cnf_transformation,[status(esa)],[f736_sk]) ).
cnf(f772,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(f772_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)],[f772]) ).
fof(f772_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)],[f772_nnf]) ).
cnf(c772,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)],[f772_sk]) ).
cnf(f773,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(f773_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)],[f773]) ).
fof(f773_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)],[f773_nnf]) ).
cnf(c773,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)],[f773_sk]) ).
cnf(f774,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(f774_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)],[f774]) ).
fof(f774_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)],[f774_nnf]) ).
cnf(c774,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)],[f774_sk]) ).
cnf(f775,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(f775_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)],[f775]) ).
fof(f775_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)],[f775_nnf]) ).
cnf(c775,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)],[f775_sk]) ).
cnf(f800,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(f800_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)],[f800]) ).
fof(f800_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)],[f800_nnf]) ).
cnf(c800,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_lessequals(X1,X2,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f800_sk]) ).
cnf(f802,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(f802_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)],[f802]) ).
fof(f802_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)],[f802_nnf]) ).
cnf(c802,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ c_lessequals(X1,X1,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f802_sk]) ).
cnf(f804,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(f804_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)],[f804]) ).
fof(f804_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)],[f804_nnf]) ).
cnf(c804,plain,
( ~ c_lessequals(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f804_sk]) ).
cnf(f807,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(f807_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)],[f807]) ).
fof(f807_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)],[f807_nnf]) ).
cnf(c807,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_lessequals(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f807_sk]) ).
cnf(f848,axiom,
v_c____ != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_c0_0) ).
fof(f848_nnf,plain,
v_c____ != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(nnf_transformation,[status(thm)],[f848]) ).
fof(f848_sk,plain,
v_c____ != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(skolemisation,[status(esa)],[f848_nnf]) ).
cnf(c848,plain,
v_c____ != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(esa)],[f848_sk]) ).
cnf(f860,axiom,
c_Polynomial_OpCons(v_c____,v_cs____,tc_Complex_Ocomplex) != c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_pCons_Oprems_0) ).
fof(f860_nnf,plain,
c_Polynomial_OpCons(v_c____,v_cs____,tc_Complex_Ocomplex) != c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(nnf_transformation,[status(thm)],[f860]) ).
fof(f860_sk,plain,
c_Polynomial_OpCons(v_c____,v_cs____,tc_Complex_Ocomplex) != c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(skolemisation,[status(esa)],[f860_nnf]) ).
cnf(c860,plain,
c_Polynomial_OpCons(v_c____,v_cs____,tc_Complex_Ocomplex) != c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(cnf_transformation,[status(esa)],[f860_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c35,c42,c45,c58,c63,c169,c233,c261,c338,c465,c513,c573,c574,c575,c676,c698,c736,c772,c773,c774,c775,c800,c802,c804,c807,c848,c860,c878]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t7315]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG385-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.37 % Computer : n008.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Fri Sep 25 05:32:10 UTC 2026
% 0.09/0.38 % CPUTime :
% 0.09/0.38 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 65.18/8.69 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 65.18/8.69 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------