%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : ALG385-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n019.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:19 AM UTC 2026
% Result : Unsatisfiable 247.45s 31.83s
% Output : CNFRefutation 247.45s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 19
% Syntax : Number of formulae : 74 ( 31 unt; 4 def)
% Number of atoms : 129 ( 41 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 106 ( 51 ~; 51 |; 0 &)
% ( 4 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 10 ( 8 usr; 5 prp; 0-3 aty)
% Number of functors : 14 ( 14 usr; 7 con; 0-3 aty)
% Number of variables : 83 ( 83 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f255,axiom,
! [T_a,V_x,V_y] :
( c_HOL_Otimes__class_Otimes(V_x,V_y,T_a) = c_HOL_Otimes__class_Otimes(V_y,V_x,T_a)
| ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f314,axiom,
! [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) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f560,axiom,
! [T_a,V_a] :
( c_HOL_Otimes__class_Otimes(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) = c_HOL_Ozero__class_Ozero(T_a)
| ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f593,axiom,
! [T_a,V_a] :
( c_HOL_Oplus__class_Oplus(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) = V_a
| ~ class_OrderedGroup_Omonoid__add(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f844,axiom,
! [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) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f848,axiom,
v_cs____ = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f863,axiom,
! [V_w,V_z] :
( c_lessequals(V_z,V_w,tc_RealDef_Oreal)
| c_lessequals(V_w,V_z,tc_RealDef_Oreal) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f867,axiom,
! [V_w] : c_lessequals(V_w,V_w,tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f868,axiom,
! [V_i,V_k,V_j] :
( ~ c_lessequals(V_i,V_j,tc_RealDef_Oreal)
| ~ c_lessequals(V_j,V_k,tc_RealDef_Oreal)
| c_lessequals(V_i,V_k,tc_RealDef_Oreal) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f876,axiom,
! [V_z,V_w] :
( ~ c_lessequals(V_z,V_w,tc_RealDef_Oreal)
| ~ c_lessequals(V_w,V_z,tc_RealDef_Oreal)
| V_z = V_w ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f878,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/sandbox2/benchmark/theBenchmark.p') ).
fof(f879,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/sandbox2/benchmark/theBenchmark.p') ).
fof(f961,axiom,
class_Ring__and__Field_Ocomm__semiring__1(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f962,axiom,
class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f976,axiom,
class_OrderedGroup_Omonoid__add(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1452,plain,
! [T_a] :
( ! [V_x,V_y] : c_HOL_Otimes__class_Otimes(V_x,V_y,T_a) = c_HOL_Otimes__class_Otimes(V_y,V_x,T_a)
| ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) ),
inference(miniscoping,[status(thm)],[f255]) ).
fof(f1453,plain,
! [X0,X1,X2] :
( c_HOL_Otimes__class_Otimes(X1,X2,X0) = c_HOL_Otimes__class_Otimes(X2,X1,X0)
| ~ class_Ring__and__Field_Ocomm__semiring__1(X0) ),
inference(cnf_transformation,[status(thm)],[f1452]) ).
fof(f1557,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(miniscoping,[status(thm)],[f314]) ).
fof(f1558,plain,
! [X0,X1] :
( 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(thm)],[f1557]) ).
fof(f1962,plain,
! [T_a] :
( ! [V_a] : c_HOL_Otimes__class_Otimes(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) = c_HOL_Ozero__class_Ozero(T_a)
| ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) ),
inference(miniscoping,[status(thm)],[f560]) ).
fof(f1963,plain,
! [X0,X1] :
( c_HOL_Otimes__class_Otimes(X1,c_HOL_Ozero__class_Ozero(X0),X0) = c_HOL_Ozero__class_Ozero(X0)
| ~ class_Ring__and__Field_Ocomm__semiring__1(X0) ),
inference(cnf_transformation,[status(thm)],[f1962]) ).
fof(f2024,plain,
! [T_a] :
( ! [V_a] : c_HOL_Oplus__class_Oplus(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) = V_a
| ~ class_OrderedGroup_Omonoid__add(T_a) ),
inference(miniscoping,[status(thm)],[f593]) ).
fof(f2025,plain,
! [X0,X1] :
( c_HOL_Oplus__class_Oplus(X1,c_HOL_Ozero__class_Ozero(X0),X0) = X1
| ~ class_OrderedGroup_Omonoid__add(X0) ),
inference(cnf_transformation,[status(thm)],[f2024]) ).
fof(f2423,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(miniscoping,[status(thm)],[f844]) ).
fof(f2424,plain,
! [X0,X1,X2,X3] :
( 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(thm)],[f2423]) ).
fof(f2430,plain,
v_cs____ = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(cnf_transformation,[status(thm)],[f848]) ).
fof(f2452,plain,
! [X0,X1] :
( c_lessequals(X1,X0,tc_RealDef_Oreal)
| c_lessequals(X0,X1,tc_RealDef_Oreal) ),
inference(cnf_transformation,[status(thm)],[f863]) ).
fof(f2458,plain,
! [X0] : c_lessequals(X0,X0,tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f867]) ).
fof(f2459,plain,
! [V_i,V_j] :
( ~ c_lessequals(V_i,V_j,tc_RealDef_Oreal)
| ! [V_k] :
( ~ c_lessequals(V_j,V_k,tc_RealDef_Oreal)
| c_lessequals(V_i,V_k,tc_RealDef_Oreal) ) ),
inference(miniscoping,[status(thm)],[f868]) ).
fof(f2460,plain,
! [X0,X1,X2] :
( ~ c_lessequals(X0,X2,tc_RealDef_Oreal)
| ~ c_lessequals(X2,X1,tc_RealDef_Oreal)
| c_lessequals(X0,X1,tc_RealDef_Oreal) ),
inference(cnf_transformation,[status(thm)],[f2459]) ).
fof(f2472,plain,
! [X0,X1] :
( ~ c_lessequals(X0,X1,tc_RealDef_Oreal)
| ~ c_lessequals(X1,X0,tc_RealDef_Oreal)
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f876]) ).
fof(f2474,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(thm)],[f878]) ).
fof(f2475,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(thm)],[f879]) ).
fof(f2557,plain,
class_Ring__and__Field_Ocomm__semiring__1(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f961]) ).
fof(f2558,plain,
class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f962]) ).
fof(f2572,plain,
class_OrderedGroup_Omonoid__add(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f976]) ).
fof(f2661,plain,
c_lessequals(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),v_da____,tc_RealDef_Oreal),
inference(resolution,[status(thm)],[f2452,f2475]) ).
fof(f2670,definition,
( sQ4_spl
<=> 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) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f2671,plain,
( ~ sQ4_spl
| 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) ),
inference(component_clause,[status(thm)],[f2670]) ).
fof(f2672,plain,
( sQ4_spl
| 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) ),
inference(component_clause,[status(thm)],[f2670]) ).
fof(f2678,plain,
( ~ sQ4_spl
| ~ c_lessequals(v_da____,v_da____,tc_RealDef_Oreal) ),
inference(backward_demodulation,[status(thm)],[f2671,f2475]) ).
fof(f2679,plain,
( ~ sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2678,f2458]) ).
fof(f2680,plain,
~ sQ4_spl,
inference(contradiction_clause,[status(thm)],[f2679]) ).
fof(f2684,plain,
! [X0,X1,X2] :
( ~ c_lessequals(X1,X2,tc_RealDef_Oreal)
| X1 = X2
| ~ c_lessequals(X2,X0,tc_RealDef_Oreal)
| ~ c_lessequals(X0,X1,tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f2460,f2472]) ).
fof(f2688,plain,
! [X0,X1,X2,X3] :
( ~ c_lessequals(X2,X3,tc_RealDef_Oreal)
| ~ c_lessequals(X3,X0,tc_RealDef_Oreal)
| ~ c_lessequals(X1,X2,tc_RealDef_Oreal)
| X1 = X2
| ~ c_lessequals(X0,X1,tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f2684,f2460]) ).
fof(f2714,definition,
( sQ8_spl
<=> 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) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f2716,plain,
( sQ8_spl
| 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) ),
inference(component_clause,[status(thm)],[f2714]) ).
fof(f5009,plain,
! [X0,X1,X2] : c_Polynomial_Opoly(c_Polynomial_OpCons(X0,X1,tc_Complex_Ocomplex),X2,tc_Complex_Ocomplex) = c_HOL_Oplus__class_Oplus(X0,c_HOL_Otimes__class_Otimes(X2,c_Polynomial_Opoly(X1,X2,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(resolution,[status(thm)],[f2558,f2424]) ).
fof(f5012,plain,
! [X0] : c_Polynomial_Opoly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X0,tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(resolution,[status(thm)],[f2558,f1558]) ).
fof(f5013,plain,
! [X0] : c_Polynomial_Opoly(v_cs____,X0,tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(forward_demodulation,[status(thm)],[f2430,f5012]) ).
fof(f6963,plain,
! [X0,X1] : c_Polynomial_Opoly(c_Polynomial_OpCons(X0,v_cs____,tc_Complex_Ocomplex),X1,tc_Complex_Ocomplex) = c_HOL_Oplus__class_Oplus(X0,c_HOL_Otimes__class_Otimes(X1,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(paramodulation,[status(thm)],[f5013,f5009]) ).
fof(f10502,plain,
! [X0] : c_HOL_Oplus__class_Oplus(X0,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex) = X0,
inference(resolution,[status(thm)],[f2025,f2572]) ).
fof(f17084,plain,
! [X0,X1] : c_HOL_Otimes__class_Otimes(X0,X1,tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(X1,X0,tc_Complex_Ocomplex),
inference(resolution,[status(thm)],[f1453,f2557]) ).
fof(f17090,plain,
c_lessequals(v_da____,c_RealVector_Onorm__class_Onorm(c_HOL_Oplus__class_Oplus(v_aa____,c_HOL_Otimes__class_Otimes(v_c____,v_z____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),
inference(backward_demodulation,[status(thm)],[f17084,f2474]) ).
fof(f17114,plain,
( sQ8_spl
| v_da____ != c_RealVector_Onorm__class_Onorm(c_HOL_Oplus__class_Oplus(v_aa____,c_HOL_Otimes__class_Otimes(v_c____,v_z____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex) ),
inference(backward_demodulation,[status(thm)],[f17084,f2716]) ).
fof(f17460,plain,
( ~ c_lessequals(c_RealVector_Onorm__class_Onorm(c_HOL_Oplus__class_Oplus(v_aa____,c_HOL_Otimes__class_Otimes(v_c____,v_z____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_da____,tc_RealDef_Oreal)
| v_da____ = c_RealVector_Onorm__class_Onorm(c_HOL_Oplus__class_Oplus(v_aa____,c_HOL_Otimes__class_Otimes(v_c____,v_z____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex)
| ~ c_lessequals(c_RealVector_Onorm__class_Onorm(c_HOL_Oplus__class_Oplus(v_aa____,c_HOL_Otimes__class_Otimes(v_c____,v_z____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_da____,tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f17090,f2688]) ).
fof(f17467,definition,
( sQ572_spl
<=> c_lessequals(c_RealVector_Onorm__class_Onorm(c_HOL_Oplus__class_Oplus(v_aa____,c_HOL_Otimes__class_Otimes(v_c____,v_z____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_da____,tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ572_spl])],[split_symbol_definition]) ).
fof(f17469,plain,
( sQ572_spl
| ~ c_lessequals(c_RealVector_Onorm__class_Onorm(c_HOL_Oplus__class_Oplus(v_aa____,c_HOL_Otimes__class_Otimes(v_c____,v_z____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_da____,tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f17467]) ).
fof(f17470,definition,
( sQ573_spl
<=> v_da____ = c_RealVector_Onorm__class_Onorm(c_HOL_Oplus__class_Oplus(v_aa____,c_HOL_Otimes__class_Otimes(v_c____,v_z____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex) ),
introduced(definition,[new_symbols(definition,[sQ573_spl])],[split_symbol_definition]) ).
fof(f17471,plain,
( ~ sQ573_spl
| v_da____ = c_RealVector_Onorm__class_Onorm(c_HOL_Oplus__class_Oplus(v_aa____,c_HOL_Otimes__class_Otimes(v_c____,v_z____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex) ),
inference(component_clause,[status(thm)],[f17470]) ).
fof(f17488,plain,
( sQ573_spl
| ~ sQ572_spl ),
inference(split_clause,[status(thm)],[f17460,f17467,f17470]) ).
fof(f17499,plain,
( ~ sQ573_spl
| sQ8_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f17471,f17114]) ).
fof(f17500,plain,
( ~ sQ573_spl
| sQ8_spl ),
inference(contradiction_clause,[status(thm)],[f17499]) ).
fof(f20096,plain,
! [X0] : c_HOL_Otimes__class_Otimes(X0,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(resolution,[status(thm)],[f1963,f2557]) ).
fof(f20098,plain,
! [X0,X1] : c_Polynomial_Opoly(c_Polynomial_OpCons(X0,v_cs____,tc_Complex_Ocomplex),X1,tc_Complex_Ocomplex) = c_HOL_Oplus__class_Oplus(X0,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(backward_demodulation,[status(thm)],[f20096,f6963]) ).
fof(f20099,plain,
! [X0,X1] : c_Polynomial_Opoly(c_Polynomial_OpCons(X0,v_cs____,tc_Complex_Ocomplex),X1,tc_Complex_Ocomplex) = X0,
inference(forward_demodulation,[status(thm)],[f10502,f20098]) ).
fof(f20158,plain,
! [X0,X1,X2] : c_Polynomial_Opoly(c_Polynomial_OpCons(X0,c_Polynomial_OpCons(X1,v_cs____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),X2,tc_Complex_Ocomplex) = c_HOL_Oplus__class_Oplus(X0,c_HOL_Otimes__class_Otimes(X2,X1,tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(paramodulation,[status(thm)],[f20099,f5009]) ).
fof(f20174,plain,
( sQ4_spl
| 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) ),
inference(backward_demodulation,[status(thm)],[f20158,f2672]) ).
fof(f20176,plain,
c_lessequals(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),v_da____,tc_RealDef_Oreal),
inference(backward_demodulation,[status(thm)],[f20158,f2661]) ).
fof(f20226,plain,
( sQ4_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f20174,f2714,f2670]) ).
fof(f20228,plain,
c_lessequals(c_RealVector_Onorm__class_Onorm(c_HOL_Oplus__class_Oplus(v_aa____,c_HOL_Otimes__class_Otimes(v_c____,v_z____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_da____,tc_RealDef_Oreal),
inference(forward_demodulation,[status(thm)],[f17084,f20176]) ).
fof(f20229,plain,
( sQ572_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20228,f17469]) ).
fof(f20230,plain,
sQ572_spl,
inference(contradiction_clause,[status(thm)],[f20229]) ).
fof(f20231,plain,
$false,
inference(sat_refutation,[status(thm)],[f2680,f17488,f17500,f20226,f20230]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : ALG385-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.42 % Computer : n019.cluster.edu
% 0.16/0.42 % Model : x86_64 x86_64
% 0.16/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.42 % Memory : 8046.5625MB
% 0.16/0.42 % OS : Linux 6.8.0-71-generic
% 0.16/0.42 % CPULimit : 300
% 0.16/0.42 % WCLimit : 300
% 0.16/0.42 % DateTime : Mon Sep 21 13:18:35 UTC 2026
% 0.16/0.42 % CPUTime :
% 0.26/0.53 % Drodi V4.1.1
% 247.45/31.83 % Refutation found
% 247.45/31.83 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 247.45/31.83 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 144.96/33.05 % Elapsed time: 32.402674 seconds
% 144.96/33.05 % CPU time: 239.799827 seconds
% 144.96/33.05 % Total memory used: 681.270 MB
% 144.96/33.05 % Net memory used: 622.818 MB
%------------------------------------------------------------------------------