%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : ALG371-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 : n005.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 3.12s 1.01s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : ALG371-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.42 % Computer : n005.cluster.edu
% 0.17/0.42 % Model : x86_64 x86_64
% 0.17/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.42 % Memory : 8046.5625MB
% 0.17/0.42 % OS : Linux 6.8.0-71-generic
% 0.17/0.42 % CPULimit : 300
% 0.17/0.42 % WCLimit : 300
% 0.17/0.42 % DateTime : Mon Sep 21 13:18:04 UTC 2026
% 0.17/0.43 % CPUTime :
% 0.17/0.49 % Drodi V4.1.1
% 3.12/1.01 % Refutation found
% 3.12/1.01 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 3.12/1.01 % SZS output start CNFRefutation for theBenchmark
% 3.12/1.01 fof(f213,axiom,(
% 3.12/1.01 (![V_m]: (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealDef_Oreal__of__preal(V_m),tc_RealDef_Oreal) ))),
% 3.12/1.01 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.12/1.01 fof(f217,axiom,(
% 3.12/1.01 (![V_p,V_r]: (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xpoly__bound__exists__1(V_p,V_r),tc_RealDef_Oreal) ))),
% 3.12/1.01 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.12/1.01 fof(f370,axiom,(
% 3.12/1.01 (![V_w,V_z]: (( c_lessequals(V_w,V_z,tc_RealDef_Oreal)| c_lessequals(V_z,V_w,tc_RealDef_Oreal) ) ))),
% 3.12/1.01 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.12/1.01 fof(f380,axiom,(
% 3.12/1.01 (![V_w]: (c_lessequals(V_w,V_w,tc_RealDef_Oreal) ))),
% 3.12/1.01 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.12/1.01 fof(f381,axiom,(
% 3.12/1.01 (![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) ) ))),
% 3.12/1.01 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.12/1.01 fof(f385,axiom,(
% 3.12/1.01 (![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) ) ))),
% 3.12/1.01 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.12/1.01 fof(f389,axiom,(
% 3.12/1.01 (![V_x]: (~ c_HOL_Oord__class_Oless(V_x,V_x,tc_RealDef_Oreal) ))),
% 3.12/1.01 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.12/1.01 fof(f393,axiom,(
% 3.12/1.01 (![T_a,V_x]: (( ~ class_RealVector_Oreal__normed__vector(T_a)| c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(V_x,T_a),tc_RealDef_Oreal) ) ))),
% 3.12/1.01 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.12/1.01 fof(f412,axiom,(
% 3.12/1.01 (![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) ) ))),
% 3.12/1.01 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.12/1.01 fof(f420,axiom,(
% 3.12/1.01 (![T_a,V_y,V_x]: (( ~ class_Orderings_Opreorder(T_a)| ~ c_lessequals(V_y,V_x,T_a)| ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a) ) ))),
% 3.12/1.01 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.12/1.01 fof(f428,negated_conjecture,(
% 3.12/1.01 c_HOL_Oord__class_Oless(v_r,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
% 3.12/1.01 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.12/1.01 fof(f429,negated_conjecture,(
% 3.12/1.01 c_lessequals(c_RealVector_Onorm__class_Onorm(v_x,tc_Complex_Ocomplex),v_r,tc_RealDef_Oreal) ),
% 3.12/1.01 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.12/1.01 fof(f430,negated_conjecture,(
% 3.12/1.01 ~ c_lessequals(c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_p,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_p,v_x,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal) ),
% 3.12/1.01 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.12/1.01 fof(f449,axiom,(
% 3.12/1.01 class_Ring__and__Field_Odivision__by__zero(tc_RealDef_Oreal) ),
% 3.12/1.01 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.12/1.01 fof(f473,axiom,(
% 3.12/1.01 class_Ring__and__Field_Oidom(tc_RealDef_Oreal) ),
% 3.12/1.01 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.12/1.01 fof(f474,axiom,(
% 3.12/1.01 class_Orderings_Opreorder(tc_RealDef_Oreal) ),
% 3.12/1.01 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.12/1.01 fof(f489,axiom,(
% 3.12/1.01 class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex) ),
% 3.12/1.01 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.12/1.01 fof(f502,axiom,(
% 3.12/1.01 class_Ring__and__Field_Oidom(tc_Complex_Ocomplex) ),
% 3.12/1.01 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.12/1.01 fof(f865,plain,(
% 3.12/1.01 ![X0]: (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealDef_Oreal__of__preal(X0),tc_RealDef_Oreal))),
% 3.12/1.01 inference(cnf_transformation,[status(thm)],[f213])).
% 3.12/1.01 fof(f871,plain,(
% 3.12/1.01 ![X0,X1]: (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xpoly__bound__exists__1(X0,X1),tc_RealDef_Oreal))),
% 3.12/1.01 inference(cnf_transformation,[status(thm)],[f217])).
% 3.12/1.01 fof(f1155,plain,(
% 3.12/1.01 ![X0,X1]: (c_lessequals(X0,X1,tc_RealDef_Oreal)|c_lessequals(X1,X0,tc_RealDef_Oreal))),
% 3.12/1.01 inference(cnf_transformation,[status(thm)],[f370])).
% 3.12/1.01 fof(f1171,plain,(
% 3.12/1.01 ![X0]: (c_lessequals(X0,X0,tc_RealDef_Oreal))),
% 3.12/1.01 inference(cnf_transformation,[status(thm)],[f380])).
% 3.12/1.01 fof(f1172,plain,(
% 3.12/1.01 ![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))),
% 3.12/1.01 inference(miniscoping,[status(thm)],[f381])).
% 3.12/1.01 fof(f1173,plain,(
% 3.12/1.01 ![X0,X1,X2]: (c_lessequals(X0,X1,tc_RealDef_Oreal)|~c_lessequals(X2,X1,tc_RealDef_Oreal)|~c_lessequals(X0,X2,tc_RealDef_Oreal))),
% 3.12/1.01 inference(cnf_transformation,[status(thm)],[f1172])).
% 3.12/1.01 fof(f1179,plain,(
% 3.12/1.01 ![X0,X1]: (c_lessequals(X0,X1,tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal))),
% 3.12/1.01 inference(cnf_transformation,[status(thm)],[f385])).
% 3.12/1.01 fof(f1184,plain,(
% 3.12/1.01 ![X0]: (~c_HOL_Oord__class_Oless(X0,X0,tc_RealDef_Oreal))),
% 3.12/1.01 inference(cnf_transformation,[status(thm)],[f389])).
% 3.12/1.01 fof(f1190,plain,(
% 3.12/1.01 ![T_a]: (~class_RealVector_Oreal__normed__vector(T_a)|(![V_x]: c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(V_x,T_a),tc_RealDef_Oreal)))),
% 3.12/1.01 inference(miniscoping,[status(thm)],[f393])).
% 3.12/1.01 fof(f1191,plain,(
% 3.12/1.01 ![X0,X1]: (~class_RealVector_Oreal__normed__vector(X0)|c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(X1,X0),tc_RealDef_Oreal))),
% 3.12/1.01 inference(cnf_transformation,[status(thm)],[f1190])).
% 3.12/1.01 fof(f1214,plain,(
% 3.12/1.01 ![X0,X1]: (X0=X1|~c_lessequals(X1,X0,tc_RealDef_Oreal)|~c_lessequals(X0,X1,tc_RealDef_Oreal))),
% 3.12/1.01 inference(cnf_transformation,[status(thm)],[f412])).
% 3.12/1.01 fof(f1225,plain,(
% 3.12/1.01 ![X0,X1,X2]: (~class_Orderings_Opreorder(X0)|~c_lessequals(X1,X2,X0)|~c_HOL_Oord__class_Oless(X2,X1,X0))),
% 3.12/1.01 inference(cnf_transformation,[status(thm)],[f420])).
% 3.12/1.01 fof(f1233,plain,(
% 3.12/1.01 c_HOL_Oord__class_Oless(v_r,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 3.12/1.01 inference(cnf_transformation,[status(thm)],[f428])).
% 3.12/1.01 fof(f1234,plain,(
% 3.12/1.01 c_lessequals(c_RealVector_Onorm__class_Onorm(v_x,tc_Complex_Ocomplex),v_r,tc_RealDef_Oreal)),
% 3.12/1.01 inference(cnf_transformation,[status(thm)],[f429])).
% 3.12/1.01 fof(f1235,plain,(
% 3.12/1.01 ~c_lessequals(c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_p,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_p,v_x,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal)),
% 3.12/1.01 inference(cnf_transformation,[status(thm)],[f430])).
% 3.12/1.01 fof(f1254,plain,(
% 3.12/1.01 class_Ring__and__Field_Odivision__by__zero(tc_RealDef_Oreal)),
% 3.12/1.01 inference(cnf_transformation,[status(thm)],[f449])).
% 3.12/1.01 fof(f1278,plain,(
% 3.12/1.01 class_Ring__and__Field_Oidom(tc_RealDef_Oreal)),
% 3.12/1.01 inference(cnf_transformation,[status(thm)],[f473])).
% 3.12/1.01 fof(f1279,plain,(
% 3.12/1.01 class_Orderings_Opreorder(tc_RealDef_Oreal)),
% 3.12/1.01 inference(cnf_transformation,[status(thm)],[f474])).
% 3.12/1.01 fof(f1294,plain,(
% 3.12/1.01 class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex)),
% 3.12/1.01 inference(cnf_transformation,[status(thm)],[f489])).
% 3.12/1.01 fof(f1307,plain,(
% 3.12/1.01 class_Ring__and__Field_Oidom(tc_Complex_Ocomplex)),
% 3.12/1.01 inference(cnf_transformation,[status(thm)],[f502])).
% 3.12/1.01 fof(f1345,plain,(
% 3.12/1.01 c_lessequals(v_r,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 3.12/1.01 inference(resolution,[status(thm)],[f1179,f1233])).
% 3.12/1.01 fof(f1358,plain,(
% 3.12/1.01 c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)=v_r|~c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_r,tc_RealDef_Oreal)),
% 3.12/1.01 inference(resolution,[status(thm)],[f1214,f1345])).
% 3.12/1.01 fof(f1360,plain,(
% 3.12/1.01 v_r=c_RealVector_Onorm__class_Onorm(v_x,tc_Complex_Ocomplex)|~c_lessequals(v_r,c_RealVector_Onorm__class_Onorm(v_x,tc_Complex_Ocomplex),tc_RealDef_Oreal)),
% 3.12/1.01 inference(resolution,[status(thm)],[f1214,f1234])).
% 3.12/1.01 fof(f1366,definition,(
% 3.12/1.01 sQ4_spl <=> (c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)=v_r)),
% 3.12/1.01 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 3.12/1.01 fof(f1367,plain,(
% 3.12/1.01 c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)=v_r|~sQ4_spl),
% 3.12/1.01 inference(component_clause,[status(thm)],[f1366])).
% 3.12/1.01 fof(f1369,definition,(
% 3.12/1.01 sQ5_spl <=> (c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_r,tc_RealDef_Oreal))),
% 3.12/1.01 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 3.12/1.01 fof(f1371,plain,(
% 3.12/1.01 ~c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_r,tc_RealDef_Oreal)|sQ5_spl),
% 3.12/1.01 inference(component_clause,[status(thm)],[f1369])).
% 3.12/1.01 fof(f1372,plain,(
% 3.12/1.01 sQ4_spl|~sQ5_spl),
% 3.12/1.01 inference(split_clause,[status(thm)],[f1358,f1366,f1369])).
% 3.12/1.01 fof(f1373,definition,(
% 3.12/1.01 sQ6_spl <=> (c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_p,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex)=c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_p,v_x,tc_Complex_Ocomplex),tc_Complex_Ocomplex))),
% 3.12/1.01 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 3.12/1.01 fof(f1374,plain,(
% 3.12/1.01 c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_p,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex)=c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_p,v_x,tc_Complex_Ocomplex),tc_Complex_Ocomplex)|~sQ6_spl),
% 3.12/1.01 inference(component_clause,[status(thm)],[f1373])).
% 3.12/1.01 fof(f1380,definition,(
% 3.12/1.01 sQ8_spl <=> (v_r=c_RealVector_Onorm__class_Onorm(v_x,tc_Complex_Ocomplex))),
% 3.12/1.01 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 3.12/1.01 fof(f1381,plain,(
% 3.12/1.01 v_r=c_RealVector_Onorm__class_Onorm(v_x,tc_Complex_Ocomplex)|~sQ8_spl),
% 3.12/1.01 inference(component_clause,[status(thm)],[f1380])).
% 3.12/1.01 fof(f1383,definition,(
% 3.12/1.01 sQ9_spl <=> (c_lessequals(v_r,c_RealVector_Onorm__class_Onorm(v_x,tc_Complex_Ocomplex),tc_RealDef_Oreal))),
% 3.12/1.01 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 3.12/1.01 fof(f1385,plain,(
% 3.12/1.01 ~c_lessequals(v_r,c_RealVector_Onorm__class_Onorm(v_x,tc_Complex_Ocomplex),tc_RealDef_Oreal)|sQ9_spl),
% 3.12/1.01 inference(component_clause,[status(thm)],[f1383])).
% 3.12/1.01 fof(f1386,plain,(
% 3.12/1.01 sQ8_spl|~sQ9_spl),
% 3.12/1.01 inference(split_clause,[status(thm)],[f1360,f1380,f1383])).
% 3.12/1.01 fof(f1391,plain,(
% 3.12/1.01 c_HOL_Oord__class_Oless(v_r,v_r,tc_RealDef_Oreal)|~sQ4_spl),
% 3.12/1.01 inference(backward_demodulation,[status(thm)],[f1367,f1233])).
% 3.12/1.01 fof(f1396,plain,(
% 3.12/1.01 $false|~sQ4_spl),
% 3.12/1.01 inference(forward_subsumption_resolution,[status(thm)],[f1391,f1184])).
% 3.12/1.01 fof(f1397,plain,(
% 3.12/1.01 ~sQ4_spl),
% 3.12/1.01 inference(contradiction_clause,[status(thm)],[f1396])).
% 3.12/1.01 fof(f1406,plain,(
% 3.12/1.01 ![X0]: (~c_lessequals(X0,v_r,tc_RealDef_Oreal)|~c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)|sQ5_spl)),
% 3.12/1.01 inference(resolution,[status(thm)],[f1173,f1371])).
% 3.12/1.01 fof(f1433,definition,(
% 3.12/1.01 sQ10_spl <=> (class_Ring__and__Field_Odivision__by__zero(tc_RealDef_Oreal))),
% 3.12/1.01 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 3.12/1.01 fof(f1435,plain,(
% 3.12/1.01 ~class_Ring__and__Field_Odivision__by__zero(tc_RealDef_Oreal)|sQ10_spl),
% 3.12/1.01 inference(component_clause,[status(thm)],[f1433])).
% 3.12/1.01 fof(f1448,plain,(
% 3.12/1.01 $false|sQ10_spl),
% 3.12/1.01 inference(forward_subsumption_resolution,[status(thm)],[f1435,f1254])).
% 3.12/1.01 fof(f1449,plain,(
% 3.12/1.01 sQ10_spl),
% 3.12/1.01 inference(contradiction_clause,[status(thm)],[f1448])).
% 3.12/1.01 fof(f1494,definition,(
% 3.12/1.01 sQ19_spl <=> (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 3.12/1.01 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 3.12/1.01 fof(f1495,plain,(
% 3.12/1.01 c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)|~sQ19_spl),
% 3.12/1.01 inference(component_clause,[status(thm)],[f1494])).
% 3.12/1.01 fof(f1498,plain,(
% 3.12/1.01 $false|~sQ19_spl),
% 3.12/1.01 inference(forward_subsumption_resolution,[status(thm)],[f1495,f1184])).
% 3.12/1.01 fof(f1499,plain,(
% 3.12/1.01 ~sQ19_spl),
% 3.12/1.01 inference(contradiction_clause,[status(thm)],[f1498])).
% 3.12/1.01 fof(f1562,plain,(
% 3.12/1.01 ~c_lessequals(c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_p,v_x,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_p,v_x,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal)|~sQ6_spl),
% 3.12/1.01 inference(backward_demodulation,[status(thm)],[f1374,f1235])).
% 3.12/1.01 fof(f1563,plain,(
% 3.12/1.01 $false|~sQ6_spl),
% 3.12/1.01 inference(forward_subsumption_resolution,[status(thm)],[f1562,f1171])).
% 3.12/1.01 fof(f1564,plain,(
% 3.12/1.01 ~sQ6_spl),
% 3.12/1.01 inference(contradiction_clause,[status(thm)],[f1563])).
% 3.12/1.01 fof(f1636,definition,(
% 3.12/1.01 sQ26_spl <=> (c_lessequals(v_r,v_r,tc_RealDef_Oreal))),
% 3.12/1.01 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 3.12/1.01 fof(f1638,plain,(
% 3.12/1.01 ~c_lessequals(v_r,v_r,tc_RealDef_Oreal)|sQ26_spl),
% 3.12/1.01 inference(component_clause,[status(thm)],[f1636])).
% 3.12/1.01 fof(f1648,definition,(
% 3.12/1.01 ![X0]: (sQ29_spl <=> (~c_lessequals(X0,c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_p,v_x,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal)|~c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)))),
% 3.12/1.01 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 3.12/1.01 fof(f1649,plain,(
% 3.12/1.01 ![X0]: (~c_lessequals(X0,c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_p,v_x,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal)|~c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)|~sQ29_spl)),
% 3.12/1.01 inference(component_clause,[status(thm)],[f1648])).
% 3.12/1.01 fof(f2566,plain,(
% 3.12/1.01 ~c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_p,v_x,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal)|~sQ29_spl),
% 3.12/1.01 inference(resolution,[status(thm)],[f1649,f1171])).
% 3.12/1.01 fof(f2577,plain,(
% 3.12/1.01 $false|sQ26_spl),
% 3.12/1.01 inference(forward_subsumption_resolution,[status(thm)],[f1638,f1171])).
% 3.12/1.01 fof(f2578,plain,(
% 3.12/1.01 sQ26_spl),
% 3.12/1.01 inference(contradiction_clause,[status(thm)],[f2577])).
% 3.12/1.01 fof(f3426,plain,(
% 3.12/1.01 ![X0,X1]: (~c_lessequals(X0,X1,tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X1,X0,tc_RealDef_Oreal))),
% 3.12/1.01 inference(resolution,[status(thm)],[f1225,f1279])).
% 3.12/1.01 fof(f3427,plain,(
% 3.12/1.01 ![X0,X1]: (~c_lessequals(v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xpoly__bound__exists__1(X0,X1),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 3.12/1.01 inference(resolution,[status(thm)],[f3426,f871])).
% 3.12/1.01 fof(f3428,plain,(
% 3.12/1.01 ![X0]: (~c_lessequals(c_RealDef_Oreal__of__preal(X0),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 3.12/1.01 inference(resolution,[status(thm)],[f3426,f865])).
% 3.12/1.01 fof(f3434,plain,(
% 3.12/1.01 ![X0,X1]: (~c_lessequals(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_lessequals(c_RealDef_Oreal__of__preal(X1),X0,tc_RealDef_Oreal))),
% 3.12/1.01 inference(resolution,[status(thm)],[f3428,f1173])).
% 3.12/1.01 fof(f3438,plain,(
% 3.12/1.01 ![X0,X1,X2]: (~c_lessequals(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_lessequals(v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xpoly__bound__exists__1(X1,X2),X0,tc_RealDef_Oreal))),
% 3.12/1.01 inference(resolution,[status(thm)],[f3427,f1173])).
% 3.12/1.01 fof(f3472,plain,(
% 3.12/1.01 ![X0,X1]: (~c_lessequals(c_RealDef_Oreal__of__preal(X0),X1,tc_RealDef_Oreal)|c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X1,tc_RealDef_Oreal))),
% 3.12/1.01 inference(resolution,[status(thm)],[f3434,f1155])).
% 3.12/1.01 fof(f3486,plain,(
% 3.12/1.01 ![X0,X1]: (c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)|c_lessequals(X0,c_RealDef_Oreal__of__preal(X1),tc_RealDef_Oreal))),
% 3.12/1.01 inference(resolution,[status(thm)],[f3472,f1155])).
% 3.12/1.01 fof(f3490,definition,(
% 3.12/1.01 ![X0,X1]: (sQ79_spl <=> (c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xpoly__bound__exists__1(X0,X1),tc_RealDef_Oreal)))),
% 3.12/1.01 introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition])).
% 3.12/1.01 fof(f3494,definition,(
% 3.12/1.01 ![X0]: (sQ80_spl <=> (c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealDef_Oreal__of__preal(X0),tc_RealDef_Oreal)))),
% 3.12/1.01 introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition])).
% 3.12/1.01 fof(f3522,plain,(
% 3.12/1.01 ![X0,X1]: (c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealDef_Oreal__of__preal(X0),tc_RealDef_Oreal)|c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealDef_Oreal__of__preal(X1),tc_RealDef_Oreal))),
% 3.12/1.01 inference(resolution,[status(thm)],[f3486,f3472])).
% 3.12/1.01 fof(f3553,plain,(
% 3.12/1.01 sQ80_spl),
% 3.12/1.01 inference(split_clause,[status(thm)],[f3522,f3494])).
% 3.12/1.01 fof(f3767,plain,(
% 3.12/1.01 ![X0,X1,X2]: (~c_lessequals(v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xpoly__bound__exists__1(X0,X1),X2,tc_RealDef_Oreal)|c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X2,tc_RealDef_Oreal))),
% 3.12/1.01 inference(resolution,[status(thm)],[f3438,f1155])).
% 3.12/1.01 fof(f3780,plain,(
% 3.12/1.01 ![X0,X1,X2]: (c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)|c_lessequals(X0,v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xpoly__bound__exists__1(X1,X2),tc_RealDef_Oreal))),
% 3.12/1.01 inference(resolution,[status(thm)],[f3767,f1155])).
% 3.12/1.01 fof(f3789,plain,(
% 3.12/1.01 ![X0,X1,X2,X3]: (c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xpoly__bound__exists__1(X0,X1),tc_RealDef_Oreal)|c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xpoly__bound__exists__1(X2,X3),tc_RealDef_Oreal))),
% 3.12/1.01 inference(resolution,[status(thm)],[f3780,f3767])).
% 3.12/1.01 fof(f3806,plain,(
% 3.12/1.01 sQ79_spl),
% 3.12/1.01 inference(split_clause,[status(thm)],[f3789,f3490])).
% 3.12/1.01 fof(f4205,definition,(
% 3.12/1.01 sQ117_spl <=> (class_Ring__and__Field_Oidom(tc_Complex_Ocomplex))),
% 3.12/1.01 introduced(definition,[new_symbols(definition,[sQ117_spl])],[split_symbol_definition])).
% 3.12/1.01 fof(f4207,plain,(
% 3.12/1.01 ~class_Ring__and__Field_Oidom(tc_Complex_Ocomplex)|sQ117_spl),
% 3.12/1.01 inference(component_clause,[status(thm)],[f4205])).
% 3.12/1.01 fof(f4212,definition,(
% 3.12/1.01 sQ119_spl <=> (class_Ring__and__Field_Oidom(tc_RealDef_Oreal))),
% 3.12/1.01 introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition])).
% 3.12/1.01 fof(f4214,plain,(
% 3.12/1.01 ~class_Ring__and__Field_Oidom(tc_RealDef_Oreal)|sQ119_spl),
% 3.12/1.01 inference(component_clause,[status(thm)],[f4212])).
% 3.12/1.01 fof(f4219,plain,(
% 3.12/1.01 $false|sQ119_spl),
% 3.12/1.01 inference(forward_subsumption_resolution,[status(thm)],[f4214,f1278])).
% 3.12/1.01 fof(f4220,plain,(
% 3.12/1.01 sQ119_spl),
% 3.12/1.01 inference(contradiction_clause,[status(thm)],[f4219])).
% 3.12/1.01 fof(f4221,plain,(
% 3.12/1.01 $false|sQ117_spl),
% 3.12/1.01 inference(forward_subsumption_resolution,[status(thm)],[f4207,f1307])).
% 3.12/1.01 fof(f4222,plain,(
% 3.12/1.01 sQ117_spl),
% 3.12/1.01 inference(contradiction_clause,[status(thm)],[f4221])).
% 3.12/1.01 fof(f4565,definition,(
% 3.12/1.01 ![X0]: (sQ129_spl <=> (~X0=X0))),
% 3.12/1.01 introduced(definition,[new_symbols(definition,[sQ129_spl])],[split_symbol_definition])).
% 3.12/1.01 fof(f4566,plain,(
% 3.12/1.01 ![X0]: (~X0=X0|~sQ129_spl)),
% 3.12/1.01 inference(component_clause,[status(thm)],[f4565])).
% 3.12/1.01 fof(f4569,plain,(
% 3.12/1.01 $false|~sQ129_spl),
% 3.12/1.01 inference(trivial_equality_resolution,[status(thm)],[f4566])).
% 3.12/1.01 fof(f4570,plain,(
% 3.12/1.01 ~sQ129_spl),
% 3.12/1.01 inference(contradiction_clause,[status(thm)],[f4569])).
% 3.12/1.01 fof(f4859,plain,(
% 3.12/1.01 ![X0]: (c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(X0,tc_Complex_Ocomplex),tc_RealDef_Oreal))),
% 3.12/1.01 inference(resolution,[status(thm)],[f1191,f1294])).
% 3.12/1.01 fof(f4861,plain,(
% 3.12/1.01 $false|~sQ29_spl),
% 3.12/1.01 inference(backward_subsumption_resolution,[status(thm)],[f2566,f4859])).
% 3.12/1.01 fof(f4867,plain,(
% 3.12/1.01 ![X0]: (~c_lessequals(c_RealVector_Onorm__class_Onorm(X0,tc_Complex_Ocomplex),v_r,tc_RealDef_Oreal)|sQ5_spl)),
% 3.12/1.01 inference(resolution,[status(thm)],[f4859,f1406])).
% 3.12/1.01 fof(f4875,plain,(
% 3.12/1.01 c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_r,tc_RealDef_Oreal)|~sQ8_spl),
% 3.12/1.01 inference(paramodulation,[status(thm)],[f1381,f4859])).
% 3.12/1.01 fof(f4876,plain,(
% 3.12/1.01 ~sQ29_spl),
% 3.12/1.01 inference(contradiction_clause,[status(thm)],[f4861])).
% 3.12/1.01 fof(f4880,plain,(
% 3.12/1.01 $false|sQ5_spl|~sQ8_spl),
% 3.12/1.01 inference(forward_subsumption_resolution,[status(thm)],[f4875,f1371])).
% 3.12/1.01 fof(f4881,plain,(
% 3.12/1.01 sQ5_spl|~sQ8_spl),
% 3.12/1.01 inference(contradiction_clause,[status(thm)],[f4880])).
% 3.12/1.01 fof(f4883,plain,(
% 3.12/1.01 ![X0]: (c_lessequals(v_r,c_RealVector_Onorm__class_Onorm(X0,tc_Complex_Ocomplex),tc_RealDef_Oreal)|sQ5_spl)),
% 3.12/1.01 inference(resolution,[status(thm)],[f4867,f1155])).
% 3.12/1.01 fof(f4896,plain,(
% 3.12/1.01 $false|sQ5_spl|sQ9_spl),
% 3.12/1.01 inference(forward_subsumption_resolution,[status(thm)],[f1385,f4883])).
% 3.12/1.01 fof(f4897,plain,(
% 3.12/1.01 sQ5_spl|sQ9_spl),
% 3.12/1.01 inference(contradiction_clause,[status(thm)],[f4896])).
% 3.12/1.01 fof(f4898,plain,(
% 3.12/1.01 $false),
% 3.12/1.01 inference(sat_refutation,[status(thm)],[f1372,f1386,f1397,f1449,f1499,f1564,f2578,f3553,f3806,f4220,f4222,f4570,f4876,f4881,f4897])).
% 1.97/1.03 % SZS output end CNFRefutation for theBenchmark.p
% 1.97/1.04 % Elapsed time: 0.595576 seconds
% 1.97/1.04 % CPU time: 3.983707 seconds
% 1.97/1.04 % Total memory used: 158.642 MB
% 1.97/1.04 % Net memory used: 155.846 MB
%------------------------------------------------------------------------------