%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : ALG374-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 : n026.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:17 AM UTC 2026
% Result : Unsatisfiable 95.43s 12.58s
% Output : CNFRefutation 93.64s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 22
% Syntax : Number of formulae : 68 ( 36 unt; 0 def)
% Number of atoms : 113 ( 22 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 97 ( 52 ~; 45 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 7 ( 1 avg)
% Number of predicates : 9 ( 7 usr; 1 prp; 0-3 aty)
% Number of functors : 18 ( 18 usr; 7 con; 0-3 aty)
% Number of variables : 76 ( 76 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f39,axiom,
c_RealDef_Oreal(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f90,axiom,
! [V_n] : ~ c_HOL_Oord__class_Oless(V_n,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f236,axiom,
! [T_a,V_a,V_b] :
( ~ c_lessequals(c_HOL_Oinverse__class_Odivide(V_a,V_b,T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| c_lessequals(V_b,c_HOL_Ozero__class_Ozero(T_a),T_a)
| c_lessequals(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Odivision__by__zero(T_a)
| ~ class_Ring__and__Field_Oordered__field(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f271,axiom,
! [V_n] : ~ c_HOL_Oord__class_Oless(c_RealDef_Oreal(V_n,tc_nat),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f278,axiom,
! [V_r,V_s] : c_HOL_Ominus__class_Ominus(V_r,V_s,tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(V_r,c_HOL_Ouminus__class_Ouminus(V_s,tc_RealDef_Oreal),tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f289,axiom,
! [T_a,V_a,V_b] :
( c_HOL_Oplus__class_Oplus(c_HOL_Ominus__class_Ominus(V_a,V_b,T_a),V_b,T_a) = V_a
| ~ class_OrderedGroup_Ogroup__add(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f373,axiom,
c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) != c_HOL_Oone__class_Oone(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f418,axiom,
c_RealDef_Oreal(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat) = c_HOL_Oone__class_Oone(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f425,axiom,
! [V_x,V_y] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(V_x,V_y,tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(c_HOL_Ouminus__class_Ouminus(V_x,tc_RealDef_Oreal),V_y,tc_RealDef_Oreal) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f434,axiom,
! [V_n,V_m] :
( ~ c_lessequals(c_HOL_Oplus__class_Oplus(c_RealDef_Oreal(V_n,tc_nat),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),c_RealDef_Oreal(V_m,tc_nat),tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(V_n,V_m,tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f445,axiom,
! [V_y] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ouminus__class_Ouminus(v_s____,tc_RealDef_Oreal),V_y,tc_RealDef_Oreal)
| c_lessequals(c_RealVector_Onorm__class_Onorm(v_sko__local__Xs1__1(v_p,v_r,V_y),tc_Complex_Ocomplex),v_r,tc_RealDef_Oreal) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f446,axiom,
! [V_y] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ouminus__class_Ouminus(v_s____,tc_RealDef_Oreal),V_y,tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_p,v_sko__local__Xs1__1(v_p,v_r,V_y),tc_Complex_Ocomplex),tc_Complex_Ocomplex),V_y,tc_RealDef_Oreal) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f486,axiom,
! [T_a,V_a,V_b] :
( c_HOL_Oplus__class_Oplus(V_a,V_b,T_a) = c_HOL_Oplus__class_Oplus(V_b,V_a,T_a)
| ~ class_OrderedGroup_Ocomm__monoid__add(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f503,axiom,
! [V_n] : c_RealDef_Oreal(c_Suc(V_n),tc_nat) = c_HOL_Oplus__class_Oplus(c_RealDef_Oreal(V_n,tc_nat),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f512,axiom,
! [V_x,V_y] :
( ~ c_lessequals(V_x,V_y,tc_RealDef_Oreal)
| V_x = V_y
| c_HOL_Oord__class_Oless(V_x,V_y,tc_RealDef_Oreal) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f558,axiom,
! [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) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f588,negated_conjecture,
! [V_x] :
( ~ c_lessequals(c_RealVector_Onorm__class_Onorm(V_x,tc_Complex_Ocomplex),v_r,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_p,V_x,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(c_HOL_Ouminus__class_Ouminus(v_s____,tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_RealDef_Oreal(c_Suc(v_n____),tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f626,axiom,
class_Ring__and__Field_Odivision__by__zero(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f631,axiom,
class_Ring__and__Field_Oordered__field(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f633,axiom,
class_OrderedGroup_Ocomm__monoid__add(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f642,axiom,
class_OrderedGroup_Ogroup__add(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f648,axiom,
class_Orderings_Olinorder(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f727,plain,
c_RealDef_Oreal(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f794,plain,
! [X0] : ~ c_HOL_Oord__class_Oless(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(cnf_transformation,[status(thm)],[f90]) ).
fof(f1023,plain,
! [X0,X1,X2] :
( ~ c_lessequals(c_HOL_Oinverse__class_Odivide(X1,X2,X0),c_HOL_Ozero__class_Ozero(X0),X0)
| c_lessequals(X2,c_HOL_Ozero__class_Ozero(X0),X0)
| c_lessequals(X1,c_HOL_Ozero__class_Ozero(X0),X0)
| ~ class_Ring__and__Field_Odivision__by__zero(X0)
| ~ class_Ring__and__Field_Oordered__field(X0) ),
inference(cnf_transformation,[status(thm)],[f236]) ).
fof(f1080,plain,
! [X0] : ~ c_HOL_Oord__class_Oless(c_RealDef_Oreal(X0,tc_nat),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f271]) ).
fof(f1087,plain,
! [X0,X1] : c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(X0,c_HOL_Ouminus__class_Ouminus(X1,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f278]) ).
fof(f1105,plain,
! [T_a] :
( ! [V_a,V_b] : c_HOL_Oplus__class_Oplus(c_HOL_Ominus__class_Ominus(V_a,V_b,T_a),V_b,T_a) = V_a
| ~ class_OrderedGroup_Ogroup__add(T_a) ),
inference(miniscoping,[status(thm)],[f289]) ).
fof(f1106,plain,
! [X0,X1,X2] :
( c_HOL_Oplus__class_Oplus(c_HOL_Ominus__class_Ominus(X1,X2,X0),X2,X0) = X1
| ~ class_OrderedGroup_Ogroup__add(X0) ),
inference(cnf_transformation,[status(thm)],[f1105]) ).
fof(f1222,plain,
c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) != c_HOL_Oone__class_Oone(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f373]) ).
fof(f1292,plain,
c_RealDef_Oreal(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat) = c_HOL_Oone__class_Oone(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f418]) ).
fof(f1299,plain,
! [X0,X1] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(X0,X1,tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal),X1,tc_RealDef_Oreal) ),
inference(cnf_transformation,[status(thm)],[f425]) ).
fof(f1310,plain,
! [X0,X1] :
( ~ c_lessequals(c_HOL_Oplus__class_Oplus(c_RealDef_Oreal(X0,tc_nat),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),c_RealDef_Oreal(X1,tc_nat),tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(X0,X1,tc_nat) ),
inference(cnf_transformation,[status(thm)],[f434]) ).
fof(f1322,plain,
! [X0] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ouminus__class_Ouminus(v_s____,tc_RealDef_Oreal),X0,tc_RealDef_Oreal)
| c_lessequals(c_RealVector_Onorm__class_Onorm(v_sko__local__Xs1__1(v_p,v_r,X0),tc_Complex_Ocomplex),v_r,tc_RealDef_Oreal) ),
inference(cnf_transformation,[status(thm)],[f445]) ).
fof(f1323,plain,
! [X0] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ouminus__class_Ouminus(v_s____,tc_RealDef_Oreal),X0,tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_p,v_sko__local__Xs1__1(v_p,v_r,X0),tc_Complex_Ocomplex),tc_Complex_Ocomplex),X0,tc_RealDef_Oreal) ),
inference(cnf_transformation,[status(thm)],[f446]) ).
fof(f1388,plain,
! [T_a] :
( ! [V_a,V_b] : c_HOL_Oplus__class_Oplus(V_a,V_b,T_a) = c_HOL_Oplus__class_Oplus(V_b,V_a,T_a)
| ~ class_OrderedGroup_Ocomm__monoid__add(T_a) ),
inference(miniscoping,[status(thm)],[f486]) ).
fof(f1389,plain,
! [X0,X1,X2] :
( c_HOL_Oplus__class_Oplus(X1,X2,X0) = c_HOL_Oplus__class_Oplus(X2,X1,X0)
| ~ class_OrderedGroup_Ocomm__monoid__add(X0) ),
inference(cnf_transformation,[status(thm)],[f1388]) ).
fof(f1418,plain,
! [X0] : c_RealDef_Oreal(c_Suc(X0),tc_nat) = c_HOL_Oplus__class_Oplus(c_RealDef_Oreal(X0,tc_nat),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f503]) ).
fof(f1431,plain,
! [X0,X1] :
( ~ c_lessequals(X0,X1,tc_RealDef_Oreal)
| X0 = X1
| c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal) ),
inference(cnf_transformation,[status(thm)],[f512]) ).
fof(f1504,plain,
! [X0,X1,X2] :
( c_lessequals(X2,X1,X0)
| c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(thm)],[f558]) ).
fof(f1546,plain,
! [X0] :
( ~ c_lessequals(c_RealVector_Onorm__class_Onorm(X0,tc_Complex_Ocomplex),v_r,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_p,X0,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(c_HOL_Ouminus__class_Ouminus(v_s____,tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_RealDef_Oreal(c_Suc(v_n____),tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(cnf_transformation,[status(thm)],[f588]) ).
fof(f1584,plain,
class_Ring__and__Field_Odivision__by__zero(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f626]) ).
fof(f1589,plain,
class_Ring__and__Field_Oordered__field(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f631]) ).
fof(f1591,plain,
class_OrderedGroup_Ocomm__monoid__add(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f633]) ).
fof(f1600,plain,
class_OrderedGroup_Ogroup__add(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f642]) ).
fof(f1606,plain,
class_Orderings_Olinorder(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f648]) ).
fof(f1874,plain,
~ c_HOL_Oord__class_Oless(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(paramodulation,[status(thm)],[f1292,f1080]) ).
fof(f1896,plain,
( ~ c_lessequals(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_HOL_Oone__class_Oone(tc_RealDef_Oreal) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f1431,f1874]) ).
fof(f1902,plain,
~ c_lessequals(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_subsumption_resolution,[status(thm)],[f1896,f1222]) ).
fof(f2722,plain,
! [X0,X1] :
( ~ c_lessequals(c_RealDef_Oreal(c_Suc(X0),tc_nat),c_RealDef_Oreal(X1,tc_nat),tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(X0,X1,tc_nat) ),
inference(backward_demodulation,[status(thm)],[f1418,f1310]) ).
fof(f2871,plain,
! [X0] :
( ~ c_lessequals(c_RealDef_Oreal(c_Suc(X0),tc_nat),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) ),
inference(paramodulation,[status(thm)],[f727,f2722]) ).
fof(f2873,plain,
! [X0] : ~ c_lessequals(c_RealDef_Oreal(c_Suc(X0),tc_nat),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_subsumption_resolution,[status(thm)],[f2871,f794]) ).
fof(f2961,plain,
! [X0,X1] : c_HOL_Oplus__class_Oplus(c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal),X1,tc_RealDef_Oreal) = X0,
inference(resolution,[status(thm)],[f1106,f1600]) ).
fof(f3442,plain,
! [X0,X1] : c_HOL_Oplus__class_Oplus(X0,X1,tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(X1,X0,tc_RealDef_Oreal),
inference(resolution,[status(thm)],[f1389,f1591]) ).
fof(f3468,plain,
! [X0] :
( ~ c_lessequals(c_RealVector_Onorm__class_Onorm(X0,tc_Complex_Ocomplex),v_r,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_p,X0,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_RealDef_Oreal(c_Suc(v_n____),tc_nat),tc_RealDef_Oreal),c_HOL_Ouminus__class_Ouminus(v_s____,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(backward_demodulation,[status(thm)],[f3442,f1546]) ).
fof(f3469,plain,
! [X0,X1] : X0 = c_HOL_Oplus__class_Oplus(X1,c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(paramodulation,[status(thm)],[f2961,f3442]) ).
fof(f4126,plain,
! [X0,X1] :
( c_lessequals(X1,X0,tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f1504,f1606]) ).
fof(f6804,plain,
! [X0,X1] :
( ~ c_lessequals(c_HOL_Oinverse__class_Odivide(X0,X1,tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_lessequals(X1,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_lessequals(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ class_Ring__and__Field_Odivision__by__zero(tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f1023,f1589]) ).
fof(f6805,plain,
! [X0,X1] :
( ~ c_lessequals(c_HOL_Oinverse__class_Odivide(X0,X1,tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_lessequals(X1,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_lessequals(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(forward_subsumption_resolution,[status(thm)],[f6804,f1584]) ).
fof(f7876,plain,
! [X0] :
( ~ c_lessequals(c_RealVector_Onorm__class_Onorm(X0,tc_Complex_Ocomplex),v_r,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_p,X0,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_RealDef_Oreal(c_Suc(v_n____),tc_nat),tc_RealDef_Oreal),v_s____,tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(backward_demodulation,[status(thm)],[f1087,f3468]) ).
fof(f13023,plain,
( ~ c_lessequals(c_RealVector_Onorm__class_Onorm(v_sko__local__Xs1__1(v_p,v_r,c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_RealDef_Oreal(c_Suc(v_n____),tc_nat),tc_RealDef_Oreal),v_s____,tc_RealDef_Oreal)),tc_Complex_Ocomplex),v_r,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ouminus__class_Ouminus(v_s____,tc_RealDef_Oreal),c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_RealDef_Oreal(c_Suc(v_n____),tc_nat),tc_RealDef_Oreal),v_s____,tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f1323,f7876]) ).
fof(f13033,plain,
~ c_HOL_Oord__class_Oless(c_HOL_Ouminus__class_Ouminus(v_s____,tc_RealDef_Oreal),c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_RealDef_Oreal(c_Suc(v_n____),tc_nat),tc_RealDef_Oreal),v_s____,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_subsumption_resolution,[status(thm)],[f13023,f1322]) ).
fof(f13038,plain,
~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(v_s____,c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_RealDef_Oreal(c_Suc(v_n____),tc_nat),tc_RealDef_Oreal),v_s____,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(resolution,[status(thm)],[f13033,f1299]) ).
fof(f13043,plain,
~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_RealDef_Oreal(c_Suc(v_n____),tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[status(thm)],[f3469,f13038]) ).
fof(f13045,plain,
c_lessequals(c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_RealDef_Oreal(c_Suc(v_n____),tc_nat),tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(resolution,[status(thm)],[f13043,f4126]) ).
fof(f29177,plain,
( c_lessequals(c_RealDef_Oreal(c_Suc(v_n____),tc_nat),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_lessequals(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f6805,f13045]) ).
fof(f29207,plain,
c_lessequals(c_RealDef_Oreal(c_Suc(v_n____),tc_nat),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_subsumption_resolution,[status(thm)],[f29177,f1902]) ).
fof(f29241,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f29207,f2873]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG374-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n026.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 13:20:53 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.12/0.40 % Drodi V4.1.1
% 95.43/12.58 % Refutation found
% 95.43/12.58 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 95.43/12.58 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 6.53/13.25 % Elapsed time: 12.877714 seconds
% 6.53/13.25 % CPU time: 97.221134 seconds
% 6.53/13.25 % Total memory used: 501.313 MB
% 6.53/13.25 % Net memory used: 457.640 MB
%------------------------------------------------------------------------------