%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : ALG370-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n015.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:50:05 AM UTC 2026
% Result : Unsatisfiable 35.29s 5.06s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG370-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n015.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Mon Sep 21 13:21:06 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.15/0.41 % Drodi V4.1.1
% 35.29/5.06 % Refutation found
% 35.29/5.06 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 35.29/5.06 % SZS output start CNFRefutation for theBenchmark
% 35.29/5.06 fof(f91,axiom,(
% 35.29/5.06 (![V_z,V_w]: (( V_z = V_w| ~ c_lessequals(V_w,V_z,tc_RealDef_Oreal)| ~ c_lessequals(V_z,V_w,tc_RealDef_Oreal) ) ))),
% 35.29/5.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 35.29/5.06 fof(f201,axiom,(
% 35.29/5.06 (![V_x,V_y]: (( c_lessequals(V_x,V_y,tc_RealDef_Oreal)| ~ c_HOL_Oord__class_Oless(V_x,V_y,tc_RealDef_Oreal) ) ))),
% 35.29/5.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 35.29/5.06 fof(f202,axiom,(
% 35.29/5.06 (![V_x,V_y]: (( c_HOL_Oord__class_Oless(V_x,V_y,tc_RealDef_Oreal)| V_x = V_y| ~ c_lessequals(V_x,V_y,tc_RealDef_Oreal) ) ))),
% 35.29/5.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 35.29/5.06 fof(f311,axiom,(
% 35.29/5.06 (![V_i,V_k,V_j]: (( c_lessequals(V_i,V_k,tc_RealDef_Oreal)| ~ c_lessequals(V_j,V_k,tc_RealDef_Oreal)| ~ c_lessequals(V_i,V_j,tc_RealDef_Oreal) ) ))),
% 35.29/5.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 35.29/5.06 fof(f312,axiom,(
% 35.29/5.06 (![V_w]: (c_lessequals(V_w,V_w,tc_RealDef_Oreal) ))),
% 35.29/5.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 35.29/5.06 fof(f321,axiom,(
% 35.29/5.06 (![V_w,V_z]: (( c_lessequals(V_w,V_z,tc_RealDef_Oreal)| c_lessequals(V_z,V_w,tc_RealDef_Oreal) ) ))),
% 35.29/5.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 35.29/5.06 fof(f364,axiom,(
% 35.29/5.06 (![V_x,V_y]: (c_RealVector_Odist__class_Odist(V_x,V_y,tc_Complex_Ocomplex) = c_RealVector_Onorm__class_Onorm(c_HOL_Ominus__class_Ominus(V_x,V_y,tc_Complex_Ocomplex),tc_Complex_Ocomplex) ))),
% 35.29/5.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 35.29/5.06 fof(f383,axiom,(
% 35.29/5.06 (![V_x]: (~ c_HOL_Oord__class_Oless(V_x,V_x,tc_RealDef_Oreal) ))),
% 35.29/5.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 35.29/5.06 fof(f422,axiom,(
% 35.29/5.06 c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(v_da____,v_m____,tc_RealDef_Oreal),v_e,tc_RealDef_Oreal) ),
% 35.29/5.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 35.29/5.06 fof(f423,axiom,(
% 35.29/5.06 c_lessequals(c_HOL_Otimes__class_Otimes(c_RealVector_Onorm__class_Onorm(c_HOL_Ominus__class_Ominus(v_w____,v_z,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_cs____,c_HOL_Ominus__class_Ominus(v_w____,v_z,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_da____,v_m____,tc_RealDef_Oreal),tc_RealDef_Oreal) ),
% 35.29/5.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 35.29/5.06 fof(f424,negated_conjecture,(
% 35.29/5.06 ~ c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(c_RealVector_Onorm__class_Onorm(c_HOL_Ominus__class_Ominus(v_w____,v_z,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_cs____,c_HOL_Ominus__class_Ominus(v_w____,v_z,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),v_e,tc_RealDef_Oreal) ),
% 35.29/5.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 35.29/5.06 fof(f461,axiom,(
% 35.29/5.06 class_OrderedGroup_Ocomm__monoid__add(tc_Int_Oint) ),
% 35.29/5.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 35.29/5.06 fof(f594,axiom,(
% 35.29/5.06 (![T_1]: (( class_OrderedGroup_Ocomm__monoid__add(tc_Polynomial_Opoly(T_1))| ~ class_OrderedGroup_Ocomm__monoid__add(T_1) ) ))),
% 35.29/5.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 35.29/5.06 fof(f761,plain,(
% 35.29/5.06 ![X0,X1]: (X0=X1|~c_lessequals(X1,X0,tc_RealDef_Oreal)|~c_lessequals(X0,X1,tc_RealDef_Oreal))),
% 35.29/5.06 inference(cnf_transformation,[status(thm)],[f91])).
% 35.29/5.06 fof(f956,plain,(
% 35.29/5.06 ![X0,X1]: (c_lessequals(X0,X1,tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal))),
% 35.29/5.06 inference(cnf_transformation,[status(thm)],[f201])).
% 35.29/5.06 fof(f957,plain,(
% 35.29/5.06 ![X0,X1]: (c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal)|X0=X1|~c_lessequals(X0,X1,tc_RealDef_Oreal))),
% 35.29/5.06 inference(cnf_transformation,[status(thm)],[f202])).
% 35.29/5.06 fof(f1133,plain,(
% 35.29/5.06 ![V_i,V_j]: ((![V_k]: (c_lessequals(V_i,V_k,tc_RealDef_Oreal)|~c_lessequals(V_j,V_k,tc_RealDef_Oreal)))|~c_lessequals(V_i,V_j,tc_RealDef_Oreal))),
% 35.29/5.06 inference(miniscoping,[status(thm)],[f311])).
% 35.29/5.06 fof(f1134,plain,(
% 35.29/5.06 ![X0,X1,X2]: (c_lessequals(X0,X1,tc_RealDef_Oreal)|~c_lessequals(X2,X1,tc_RealDef_Oreal)|~c_lessequals(X0,X2,tc_RealDef_Oreal))),
% 35.29/5.06 inference(cnf_transformation,[status(thm)],[f1133])).
% 35.29/5.06 fof(f1135,plain,(
% 35.29/5.06 ![X0]: (c_lessequals(X0,X0,tc_RealDef_Oreal))),
% 35.29/5.06 inference(cnf_transformation,[status(thm)],[f312])).
% 35.29/5.06 fof(f1150,plain,(
% 35.29/5.06 ![X0,X1]: (c_lessequals(X0,X1,tc_RealDef_Oreal)|c_lessequals(X1,X0,tc_RealDef_Oreal))),
% 35.29/5.06 inference(cnf_transformation,[status(thm)],[f321])).
% 35.29/5.06 fof(f1226,plain,(
% 35.29/5.06 ![X0,X1]: (c_RealVector_Odist__class_Odist(X0,X1,tc_Complex_Ocomplex)=c_RealVector_Onorm__class_Onorm(c_HOL_Ominus__class_Ominus(X0,X1,tc_Complex_Ocomplex),tc_Complex_Ocomplex))),
% 35.29/5.06 inference(cnf_transformation,[status(thm)],[f364])).
% 35.29/5.06 fof(f1247,plain,(
% 35.29/5.06 ![X0]: (~c_HOL_Oord__class_Oless(X0,X0,tc_RealDef_Oreal))),
% 35.29/5.06 inference(cnf_transformation,[status(thm)],[f383])).
% 35.29/5.06 fof(f1318,plain,(
% 35.29/5.06 c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(v_da____,v_m____,tc_RealDef_Oreal),v_e,tc_RealDef_Oreal)),
% 35.29/5.06 inference(cnf_transformation,[status(thm)],[f422])).
% 35.29/5.06 fof(f1319,plain,(
% 35.29/5.06 c_lessequals(c_HOL_Otimes__class_Otimes(c_RealVector_Onorm__class_Onorm(c_HOL_Ominus__class_Ominus(v_w____,v_z,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_cs____,c_HOL_Ominus__class_Ominus(v_w____,v_z,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_da____,v_m____,tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 35.29/5.06 inference(cnf_transformation,[status(thm)],[f423])).
% 35.29/5.06 fof(f1320,plain,(
% 35.29/5.06 ~c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(c_RealVector_Onorm__class_Onorm(c_HOL_Ominus__class_Ominus(v_w____,v_z,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_cs____,c_HOL_Ominus__class_Ominus(v_w____,v_z,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),v_e,tc_RealDef_Oreal)),
% 35.29/5.06 inference(cnf_transformation,[status(thm)],[f424])).
% 35.29/5.06 fof(f1357,plain,(
% 35.29/5.06 class_OrderedGroup_Ocomm__monoid__add(tc_Int_Oint)),
% 35.29/5.06 inference(cnf_transformation,[status(thm)],[f461])).
% 35.29/5.06 fof(f1490,plain,(
% 35.29/5.06 ![X0]: (class_OrderedGroup_Ocomm__monoid__add(tc_Polynomial_Opoly(X0))|~class_OrderedGroup_Ocomm__monoid__add(X0))),
% 35.29/5.06 inference(cnf_transformation,[status(thm)],[f594])).
% 35.29/5.06 fof(f1564,plain,(
% 35.29/5.06 ![X0,X1]: (c_lessequals(X0,X1,tc_RealDef_Oreal)|c_HOL_Oord__class_Oless(X1,X0,tc_RealDef_Oreal)|X1=X0)),
% 35.29/5.06 inference(resolution,[status(thm)],[f1150,f957])).
% 35.29/5.06 fof(f1582,plain,(
% 35.29/5.06 c_lessequals(v_e,c_HOL_Otimes__class_Otimes(c_RealVector_Onorm__class_Onorm(c_HOL_Ominus__class_Ominus(v_w____,v_z,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_cs____,c_HOL_Ominus__class_Ominus(v_w____,v_z,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal)|c_HOL_Otimes__class_Otimes(c_RealVector_Onorm__class_Onorm(c_HOL_Ominus__class_Ominus(v_w____,v_z,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_cs____,c_HOL_Ominus__class_Ominus(v_w____,v_z,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal)=v_e),
% 35.29/5.06 inference(resolution,[status(thm)],[f1564,f1320])).
% 35.29/5.06 fof(f1591,definition,(
% 35.29/5.06 sQ10_spl <=> (c_lessequals(v_e,c_HOL_Otimes__class_Otimes(c_RealVector_Onorm__class_Onorm(c_HOL_Ominus__class_Ominus(v_w____,v_z,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_cs____,c_HOL_Ominus__class_Ominus(v_w____,v_z,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 35.29/5.06 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 35.29/5.06 fof(f1592,plain,(
% 35.29/5.06 c_lessequals(v_e,c_HOL_Otimes__class_Otimes(c_RealVector_Onorm__class_Onorm(c_HOL_Ominus__class_Ominus(v_w____,v_z,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_cs____,c_HOL_Ominus__class_Ominus(v_w____,v_z,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal)|~sQ10_spl),
% 35.29/5.06 inference(component_clause,[status(thm)],[f1591])).
% 35.29/5.06 fof(f1593,plain,(
% 35.29/5.06 ~c_lessequals(v_e,c_HOL_Otimes__class_Otimes(c_RealVector_Onorm__class_Onorm(c_HOL_Ominus__class_Ominus(v_w____,v_z,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_cs____,c_HOL_Ominus__class_Ominus(v_w____,v_z,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal)|sQ10_spl),
% 35.29/5.06 inference(component_clause,[status(thm)],[f1591])).
% 35.29/5.06 fof(f1594,definition,(
% 35.29/5.06 sQ11_spl <=> (c_HOL_Otimes__class_Otimes(c_RealVector_Onorm__class_Onorm(c_HOL_Ominus__class_Ominus(v_w____,v_z,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_cs____,c_HOL_Ominus__class_Ominus(v_w____,v_z,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal)=v_e)),
% 35.29/5.06 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 35.29/5.06 fof(f1595,plain,(
% 35.29/5.06 c_HOL_Otimes__class_Otimes(c_RealVector_Onorm__class_Onorm(c_HOL_Ominus__class_Ominus(v_w____,v_z,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_cs____,c_HOL_Ominus__class_Ominus(v_w____,v_z,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal)=v_e|~sQ11_spl),
% 35.29/5.06 inference(component_clause,[status(thm)],[f1594])).
% 35.29/5.06 fof(f1597,plain,(
% 35.29/5.06 sQ10_spl|sQ11_spl),
% 35.29/5.06 inference(split_clause,[status(thm)],[f1582,f1591,f1594])).
% 35.29/5.06 fof(f1704,plain,(
% 35.29/5.06 ![X0]: (c_lessequals(v_e,X0,tc_RealDef_Oreal)|~c_lessequals(c_HOL_Otimes__class_Otimes(c_RealVector_Onorm__class_Onorm(c_HOL_Ominus__class_Ominus(v_w____,v_z,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_cs____,c_HOL_Ominus__class_Ominus(v_w____,v_z,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),X0,tc_RealDef_Oreal)|~sQ10_spl)),
% 35.29/5.06 inference(resolution,[status(thm)],[f1592,f1134])).
% 35.29/5.06 fof(f2417,plain,(
% 35.29/5.06 ~c_lessequals(v_e,v_e,tc_RealDef_Oreal)|~sQ11_spl|sQ10_spl),
% 35.29/5.06 inference(forward_demodulation,[status(thm)],[f1595,f1593])).
% 35.29/5.06 fof(f2418,plain,(
% 35.29/5.06 $false|~sQ11_spl|sQ10_spl),
% 35.29/5.06 inference(forward_subsumption_resolution,[status(thm)],[f2417,f1135])).
% 35.29/5.06 fof(f2419,plain,(
% 35.29/5.06 ~sQ11_spl|sQ10_spl),
% 35.29/5.06 inference(contradiction_clause,[status(thm)],[f2418])).
% 35.29/5.06 fof(f3410,plain,(
% 35.29/5.06 class_OrderedGroup_Ocomm__monoid__add(tc_Polynomial_Opoly(tc_Int_Oint))),
% 35.29/5.06 inference(resolution,[status(thm)],[f1490,f1357])).
% 35.29/5.06 fof(f3425,plain,(
% 35.29/5.06 class_OrderedGroup_Ocomm__monoid__add(tc_Polynomial_Opoly(tc_Polynomial_Opoly(tc_Int_Oint)))),
% 35.29/5.06 inference(resolution,[status(thm)],[f3410,f1490])).
% 35.29/5.06 fof(f3933,plain,(
% 35.29/5.06 class_OrderedGroup_Ocomm__monoid__add(tc_Polynomial_Opoly(tc_Polynomial_Opoly(tc_Polynomial_Opoly(tc_Int_Oint))))),
% 35.29/5.06 inference(resolution,[status(thm)],[f3425,f1490])).
% 35.29/5.06 fof(f5153,plain,(
% 35.29/5.06 class_OrderedGroup_Ocomm__monoid__add(tc_Polynomial_Opoly(tc_Polynomial_Opoly(tc_Polynomial_Opoly(tc_Polynomial_Opoly(tc_Int_Oint)))))),
% 35.29/5.06 inference(resolution,[status(thm)],[f3933,f1490])).
% 35.29/5.06 fof(f5778,definition,(
% 35.29/5.06 sQ291_spl <=> (c_HOL_Oord__class_Oless(v_e,v_e,tc_RealDef_Oreal))),
% 35.29/5.06 introduced(definition,[new_symbols(definition,[sQ291_spl])],[split_symbol_definition])).
% 35.29/5.06 fof(f5779,plain,(
% 35.29/5.06 c_HOL_Oord__class_Oless(v_e,v_e,tc_RealDef_Oreal)|~sQ291_spl),
% 35.29/5.06 inference(component_clause,[status(thm)],[f5778])).
% 35.29/5.06 fof(f8995,plain,(
% 35.29/5.06 class_OrderedGroup_Ocomm__monoid__add(tc_Polynomial_Opoly(tc_Polynomial_Opoly(tc_Polynomial_Opoly(tc_Polynomial_Opoly(tc_Polynomial_Opoly(tc_Int_Oint))))))),
% 35.29/5.06 inference(resolution,[status(thm)],[f5153,f1490])).
% 35.29/5.06 fof(f13636,plain,(
% 35.29/5.06 c_lessequals(c_HOL_Otimes__class_Otimes(v_da____,v_m____,tc_RealDef_Oreal),v_e,tc_RealDef_Oreal)),
% 35.29/5.06 inference(resolution,[status(thm)],[f1318,f956])).
% 35.29/5.06 fof(f16502,plain,(
% 35.29/5.06 v_e=c_HOL_Otimes__class_Otimes(v_da____,v_m____,tc_RealDef_Oreal)|~c_lessequals(v_e,c_HOL_Otimes__class_Otimes(v_da____,v_m____,tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 35.29/5.06 inference(resolution,[status(thm)],[f13636,f761])).
% 35.29/5.06 fof(f16505,definition,(
% 35.29/5.06 sQ760_spl <=> (v_e=c_HOL_Otimes__class_Otimes(v_da____,v_m____,tc_RealDef_Oreal))),
% 35.29/5.06 introduced(definition,[new_symbols(definition,[sQ760_spl])],[split_symbol_definition])).
% 35.29/5.06 fof(f16506,plain,(
% 36.36/5.08 v_e=c_HOL_Otimes__class_Otimes(v_da____,v_m____,tc_RealDef_Oreal)|~sQ760_spl),
% 36.36/5.08 inference(component_clause,[status(thm)],[f16505])).
% 36.36/5.08 fof(f16508,definition,(
% 36.36/5.08 sQ761_spl <=> (c_lessequals(v_e,c_HOL_Otimes__class_Otimes(v_da____,v_m____,tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 36.36/5.08 introduced(definition,[new_symbols(definition,[sQ761_spl])],[split_symbol_definition])).
% 36.36/5.08 fof(f16510,plain,(
% 36.36/5.08 ~c_lessequals(v_e,c_HOL_Otimes__class_Otimes(v_da____,v_m____,tc_RealDef_Oreal),tc_RealDef_Oreal)|sQ761_spl),
% 36.36/5.08 inference(component_clause,[status(thm)],[f16508])).
% 36.36/5.08 fof(f16511,plain,(
% 36.36/5.08 sQ760_spl|~sQ761_spl),
% 36.36/5.08 inference(split_clause,[status(thm)],[f16502,f16505,f16508])).
% 36.36/5.08 fof(f16513,plain,(
% 36.36/5.08 c_HOL_Oord__class_Oless(v_e,v_e,tc_RealDef_Oreal)|~sQ760_spl),
% 36.36/5.08 inference(backward_demodulation,[status(thm)],[f16506,f1318])).
% 36.36/5.08 fof(f16523,plain,(
% 36.36/5.08 $false|~sQ760_spl),
% 36.36/5.08 inference(forward_subsumption_resolution,[status(thm)],[f16513,f1247])).
% 36.36/5.08 fof(f16524,plain,(
% 36.36/5.08 ~sQ760_spl),
% 36.36/5.08 inference(contradiction_clause,[status(thm)],[f16523])).
% 36.36/5.08 fof(f18612,plain,(
% 36.36/5.08 $false|~sQ291_spl),
% 36.36/5.08 inference(forward_subsumption_resolution,[status(thm)],[f5779,f1247])).
% 36.36/5.08 fof(f18613,plain,(
% 36.36/5.08 ~sQ291_spl),
% 36.36/5.08 inference(contradiction_clause,[status(thm)],[f18612])).
% 36.36/5.08 fof(f20029,definition,(
% 36.36/5.08 sQ814_spl <=> (class_OrderedGroup_Ocomm__monoid__add(tc_Polynomial_Opoly(tc_Polynomial_Opoly(tc_Polynomial_Opoly(tc_Polynomial_Opoly(tc_Polynomial_Opoly(tc_Int_Oint)))))))),
% 36.36/5.08 introduced(definition,[new_symbols(definition,[sQ814_spl])],[split_symbol_definition])).
% 36.36/5.08 fof(f20031,plain,(
% 36.36/5.08 ~class_OrderedGroup_Ocomm__monoid__add(tc_Polynomial_Opoly(tc_Polynomial_Opoly(tc_Polynomial_Opoly(tc_Polynomial_Opoly(tc_Polynomial_Opoly(tc_Int_Oint))))))|sQ814_spl),
% 36.36/5.08 inference(component_clause,[status(thm)],[f20029])).
% 36.36/5.08 fof(f20044,plain,(
% 36.36/5.08 $false|sQ814_spl),
% 36.36/5.08 inference(forward_subsumption_resolution,[status(thm)],[f20031,f8995])).
% 36.36/5.08 fof(f20045,plain,(
% 36.36/5.08 sQ814_spl),
% 36.36/5.08 inference(contradiction_clause,[status(thm)],[f20044])).
% 36.36/5.08 fof(f21452,plain,(
% 36.36/5.08 c_lessequals(c_HOL_Otimes__class_Otimes(c_RealVector_Odist__class_Odist(v_w____,v_z,tc_Complex_Ocomplex),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_cs____,c_HOL_Ominus__class_Ominus(v_w____,v_z,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_da____,v_m____,tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 36.36/5.08 inference(forward_demodulation,[status(thm)],[f1226,f1319])).
% 36.36/5.08 fof(f23049,plain,(
% 36.36/5.08 ![X0]: (c_lessequals(v_e,X0,tc_RealDef_Oreal)|~c_lessequals(c_HOL_Otimes__class_Otimes(c_RealVector_Odist__class_Odist(v_w____,v_z,tc_Complex_Ocomplex),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_cs____,c_HOL_Ominus__class_Ominus(v_w____,v_z,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),X0,tc_RealDef_Oreal)|~sQ10_spl)),
% 36.36/5.08 inference(forward_demodulation,[status(thm)],[f1226,f1704])).
% 36.36/5.08 fof(f23050,plain,(
% 36.36/5.08 c_lessequals(v_e,c_HOL_Otimes__class_Otimes(v_da____,v_m____,tc_RealDef_Oreal),tc_RealDef_Oreal)|~sQ10_spl),
% 36.36/5.08 inference(resolution,[status(thm)],[f23049,f21452])).
% 36.36/5.08 fof(f23066,plain,(
% 36.36/5.08 $false|sQ761_spl|~sQ10_spl),
% 36.36/5.08 inference(forward_subsumption_resolution,[status(thm)],[f23050,f16510])).
% 36.36/5.08 fof(f23067,plain,(
% 36.36/5.08 sQ761_spl|~sQ10_spl),
% 36.36/5.08 inference(contradiction_clause,[status(thm)],[f23066])).
% 36.36/5.08 fof(f23068,plain,(
% 36.36/5.08 $false),
% 36.36/5.08 inference(sat_refutation,[status(thm)],[f1597,f2419,f16511,f16524,f18613,f20045,f23067])).
% 36.36/5.08 % SZS output end CNFRefutation for theBenchmark.p
% 15.29/5.12 % Elapsed time: 4.725174 seconds
% 15.29/5.12 % CPU time: 36.771138 seconds
% 15.29/5.12 % Total memory used: 342.470 MB
% 15.29/5.12 % Net memory used: 329.770 MB
%------------------------------------------------------------------------------