%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : ALG340-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 : n002.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:03 AM UTC 2026
% Result : Unsatisfiable 1.68s 0.72s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG340-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.36 % Computer : n002.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 13:19:16 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.16/0.41 % Drodi V4.1.1
% 1.68/0.72 % Refutation found
% 1.68/0.72 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 1.68/0.72 % SZS output start CNFRefutation for theBenchmark
% 1.68/0.72 fof(f211,axiom,(
% 1.68/0.72 (![V_x]: (( V_x = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(V_x,V_x,tc_RealDef_Oreal),tc_RealDef_Oreal) ) ))),
% 1.68/0.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.68/0.72 fof(f213,axiom,(
% 1.68/0.72 (![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) ))),
% 1.68/0.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.68/0.72 fof(f368,axiom,(
% 1.68/0.72 (![V_w,V_z]: (( c_lessequals(V_w,V_z,tc_RealDef_Oreal)| c_lessequals(V_z,V_w,tc_RealDef_Oreal) ) ))),
% 1.68/0.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.68/0.72 fof(f378,axiom,(
% 1.68/0.72 (![V_w]: (c_lessequals(V_w,V_w,tc_RealDef_Oreal) ))),
% 1.68/0.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.68/0.72 fof(f379,axiom,(
% 1.68/0.72 (![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) ) ))),
% 1.68/0.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.68/0.72 fof(f383,axiom,(
% 1.68/0.72 (![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) ) ))),
% 1.68/0.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.68/0.72 fof(f392,axiom,(
% 1.68/0.72 (![T_a,V_a]: (( ~ class_Ring__and__Field_Oidom(T_a)| c_Polynomial_Opoly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)),V_a,T_a) = c_HOL_Ozero__class_Ozero(T_a) ) ))),
% 1.68/0.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.68/0.72 fof(f400,axiom,(
% 1.68/0.72 (![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) ) ))),
% 1.68/0.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.68/0.72 fof(f412,axiom,(
% 1.68/0.72 (![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) ) ))),
% 1.68/0.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.68/0.72 fof(f429,negated_conjecture,(
% 1.68/0.72 (![V_xa]: (( ~ c_lessequals(c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_x(V_xa),tc_Complex_Ocomplex),tc_Complex_Ocomplex),V_xa,tc_RealDef_Oreal)| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_xa,tc_RealDef_Oreal) ) ))),
% 1.68/0.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.68/0.72 fof(f454,axiom,(
% 1.68/0.72 class_Ring__and__Field_Odivision__by__zero(tc_RealDef_Oreal) ),
% 1.68/0.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.68/0.72 fof(f509,axiom,(
% 1.68/0.72 class_Ring__and__Field_Oidom(tc_Complex_Ocomplex) ),
% 1.68/0.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.68/0.72 fof(f911,plain,(
% 1.68/0.72 ![X0]: (X0=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)|c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X0,X0,tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 1.68/0.72 inference(cnf_transformation,[status(thm)],[f211])).
% 1.68/0.72 fof(f913,plain,(
% 1.68/0.72 ![X0]: (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealDef_Oreal__of__preal(X0),tc_RealDef_Oreal))),
% 1.68/0.72 inference(cnf_transformation,[status(thm)],[f213])).
% 1.68/0.72 fof(f1200,plain,(
% 1.68/0.72 ![X0,X1]: (c_lessequals(X0,X1,tc_RealDef_Oreal)|c_lessequals(X1,X0,tc_RealDef_Oreal))),
% 1.68/0.72 inference(cnf_transformation,[status(thm)],[f368])).
% 1.68/0.72 fof(f1216,plain,(
% 1.68/0.72 ![X0]: (c_lessequals(X0,X0,tc_RealDef_Oreal))),
% 1.68/0.72 inference(cnf_transformation,[status(thm)],[f378])).
% 1.68/0.72 fof(f1217,plain,(
% 1.68/0.72 ![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))),
% 1.68/0.72 inference(miniscoping,[status(thm)],[f379])).
% 1.68/0.72 fof(f1218,plain,(
% 1.68/0.72 ![X0,X1,X2]: (c_lessequals(X0,X1,tc_RealDef_Oreal)|~c_lessequals(X2,X1,tc_RealDef_Oreal)|~c_lessequals(X0,X2,tc_RealDef_Oreal))),
% 1.68/0.72 inference(cnf_transformation,[status(thm)],[f1217])).
% 1.68/0.72 fof(f1224,plain,(
% 1.68/0.72 ![X0,X1]: (c_lessequals(X0,X1,tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal))),
% 1.68/0.72 inference(cnf_transformation,[status(thm)],[f383])).
% 1.68/0.72 fof(f1237,plain,(
% 1.68/0.72 ![T_a]: (~class_Ring__and__Field_Oidom(T_a)|(![V_a]: c_Polynomial_Opoly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)),V_a,T_a)=c_HOL_Ozero__class_Ozero(T_a)))),
% 1.68/0.72 inference(miniscoping,[status(thm)],[f392])).
% 1.68/0.72 fof(f1238,plain,(
% 1.68/0.72 ![X0,X1]: (~class_Ring__and__Field_Oidom(X0)|c_Polynomial_Opoly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)),X1,X0)=c_HOL_Ozero__class_Ozero(X0))),
% 1.68/0.72 inference(cnf_transformation,[status(thm)],[f1237])).
% 1.68/0.72 fof(f1249,plain,(
% 1.68/0.72 ![X0,X1]: (c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal)|X0=X1|~c_lessequals(X0,X1,tc_RealDef_Oreal))),
% 1.68/0.72 inference(cnf_transformation,[status(thm)],[f400])).
% 1.68/0.72 fof(f1263,plain,(
% 1.68/0.72 ![X0,X1]: (X0=X1|~c_lessequals(X1,X0,tc_RealDef_Oreal)|~c_lessequals(X0,X1,tc_RealDef_Oreal))),
% 1.68/0.72 inference(cnf_transformation,[status(thm)],[f412])).
% 1.68/0.72 fof(f1283,plain,(
% 1.68/0.72 ![X0]: (~c_lessequals(c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_x(X0),tc_Complex_Ocomplex),tc_Complex_Ocomplex),X0,tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal))),
% 1.68/0.72 inference(cnf_transformation,[status(thm)],[f429])).
% 1.68/0.72 fof(f1308,plain,(
% 1.68/0.72 class_Ring__and__Field_Odivision__by__zero(tc_RealDef_Oreal)),
% 1.68/0.72 inference(cnf_transformation,[status(thm)],[f454])).
% 1.68/0.72 fof(f1363,plain,(
% 1.68/0.72 class_Ring__and__Field_Oidom(tc_Complex_Ocomplex)),
% 1.68/0.72 inference(cnf_transformation,[status(thm)],[f509])).
% 1.68/0.72 fof(f1677,plain,(
% 1.68/0.72 ![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))),
% 1.68/0.72 inference(resolution,[status(thm)],[f1238,f1363])).
% 1.68/0.72 fof(f1703,plain,(
% 1.68/0.72 ![X0]: (~c_lessequals(c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_x(X0),tc_Complex_Ocomplex),tc_Complex_Ocomplex),X0,tc_RealDef_Oreal)|c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)=X0|~c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal))),
% 1.68/0.72 inference(resolution,[status(thm)],[f1283,f1249])).
% 1.68/0.72 fof(f1704,plain,(
% 1.68/0.72 ![X0]: (~c_lessequals(c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),X0,tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal))),
% 1.68/0.72 inference(backward_demodulation,[status(thm)],[f1677,f1283])).
% 1.68/0.72 fof(f1743,plain,(
% 1.68/0.72 ![X0]: (~c_lessequals(c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),X0,tc_RealDef_Oreal)|c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)=X0|~c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal))),
% 1.68/0.72 inference(forward_demodulation,[status(thm)],[f1677,f1703])).
% 1.68/0.72 fof(f1755,definition,(
% 1.68/0.72 sQ10_spl <=> (c_lessequals(c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 1.68/0.72 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 1.68/0.72 fof(f1756,plain,(
% 1.68/0.72 c_lessequals(c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)|~sQ10_spl),
% 1.68/0.72 inference(component_clause,[status(thm)],[f1755])).
% 1.68/0.72 fof(f1757,plain,(
% 1.68/0.72 ~c_lessequals(c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)|sQ10_spl),
% 1.68/0.72 inference(component_clause,[status(thm)],[f1755])).
% 1.68/0.72 fof(f1767,plain,(
% 1.68/0.72 c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal)|sQ10_spl),
% 1.68/0.72 inference(resolution,[status(thm)],[f1757,f1200])).
% 1.68/0.72 fof(f1769,plain,(
% 1.68/0.72 ~c_lessequals(c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal)|c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)=c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex)|sQ10_spl),
% 1.68/0.72 inference(resolution,[status(thm)],[f1767,f1743])).
% 1.68/0.72 fof(f1774,definition,(
% 1.68/0.72 sQ11_spl <=> (c_lessequals(c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal))),
% 1.68/0.72 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 1.68/0.72 fof(f1776,plain,(
% 1.68/0.72 ~c_lessequals(c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal)|sQ11_spl),
% 1.68/0.72 inference(component_clause,[status(thm)],[f1774])).
% 1.68/0.72 fof(f1777,definition,(
% 1.68/0.72 sQ12_spl <=> (c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)=c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex))),
% 1.68/0.72 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 1.68/0.72 fof(f1778,plain,(
% 1.68/0.72 c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)=c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex)|~sQ12_spl),
% 1.68/0.72 inference(component_clause,[status(thm)],[f1777])).
% 1.68/0.72 fof(f1779,plain,(
% 1.68/0.72 ~c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)=c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex)|sQ12_spl),
% 1.68/0.72 inference(component_clause,[status(thm)],[f1777])).
% 1.68/0.72 fof(f1780,plain,(
% 1.68/0.72 ~sQ11_spl|sQ12_spl|sQ10_spl),
% 1.68/0.72 inference(split_clause,[status(thm)],[f1769,f1774,f1777,f1755])).
% 1.68/0.72 fof(f1782,plain,(
% 1.68/0.72 $false|sQ11_spl),
% 1.68/0.72 inference(forward_subsumption_resolution,[status(thm)],[f1776,f1216])).
% 1.68/0.72 fof(f1783,plain,(
% 1.68/0.72 sQ11_spl),
% 1.68/0.72 inference(contradiction_clause,[status(thm)],[f1782])).
% 1.68/0.72 fof(f1785,plain,(
% 1.68/0.72 ![X0]: (~c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)|~sQ12_spl)),
% 1.68/0.72 inference(backward_demodulation,[status(thm)],[f1778,f1704])).
% 1.68/0.72 fof(f1787,plain,(
% 1.68/0.72 ![X0]: (~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)|~sQ12_spl)),
% 1.68/0.72 inference(forward_subsumption_resolution,[status(thm)],[f1785,f1224])).
% 1.68/0.72 fof(f1861,plain,(
% 1.68/0.72 ![X0]: (X0=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)|~sQ12_spl)),
% 1.68/0.72 inference(forward_subsumption_resolution,[status(thm)],[f911,f1787])).
% 1.68/0.72 fof(f1862,plain,(
% 1.68/0.72 ![X0,X1]: (X0=X1|~sQ12_spl)),
% 1.68/0.72 inference(paramodulation,[status(thm)],[f1861,f1861])).
% 1.68/0.72 fof(f1863,plain,(
% 1.68/0.72 ![X0,X1]: (~c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal)|~sQ12_spl)),
% 1.68/0.72 inference(paramodulation,[status(thm)],[f1861,f1787])).
% 1.68/0.72 fof(f1864,plain,(
% 1.68/0.72 ![X0,X1,X2]: (~c_HOL_Oord__class_Oless(X0,X1,X2)|~sQ12_spl)),
% 1.68/0.72 inference(paramodulation,[status(thm)],[f1862,f1863])).
% 1.68/0.72 fof(f2227,plain,(
% 1.68/0.72 $false|~sQ12_spl),
% 1.68/0.72 inference(forward_subsumption_resolution,[status(thm)],[f913,f1864])).
% 1.68/0.72 fof(f2228,plain,(
% 1.68/0.72 ~sQ12_spl),
% 1.68/0.72 inference(contradiction_clause,[status(thm)],[f2227])).
% 1.68/0.72 fof(f2253,plain,(
% 1.68/0.72 c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)=c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex)|~c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal)|~sQ10_spl),
% 1.68/0.72 inference(resolution,[status(thm)],[f1263,f1756])).
% 1.68/0.72 fof(f2261,definition,(
% 1.68/0.72 sQ18_spl <=> (c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal))),
% 1.68/0.72 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 1.68/0.72 fof(f2263,plain,(
% 1.68/0.72 ~c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal)|sQ18_spl),
% 1.68/0.72 inference(component_clause,[status(thm)],[f2261])).
% 1.68/0.72 fof(f2264,plain,(
% 1.68/0.72 sQ12_spl|~sQ18_spl|~sQ10_spl),
% 1.68/0.72 inference(split_clause,[status(thm)],[f2253,f1777,f2261,f1755])).
% 1.68/0.72 fof(f2277,plain,(
% 1.68/0.72 ![X0]: (~c_lessequals(X0,c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal)|~c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)|sQ18_spl)),
% 1.68/0.72 inference(resolution,[status(thm)],[f2263,f1218])).
% 1.68/0.72 fof(f2282,plain,(
% 1.68/0.72 ![X0]: (~c_lessequals(X0,c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal)|c_lessequals(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)|sQ18_spl)),
% 1.68/0.72 inference(resolution,[status(thm)],[f2277,f1200])).
% 1.68/0.72 fof(f2288,plain,(
% 1.68/0.72 ![X0]: (c_lessequals(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)|c_lessequals(c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),X0,tc_RealDef_Oreal)|sQ18_spl)),
% 1.68/0.72 inference(resolution,[status(thm)],[f2282,f1200])).
% 1.68/0.72 fof(f2362,plain,(
% 1.68/0.72 ![X0]: (~c_lessequals(c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),X0,tc_RealDef_Oreal)|c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)=X0|c_lessequals(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 1.68/0.72 inference(resolution,[status(thm)],[f1743,f1200])).
% 1.68/0.72 fof(f2370,plain,(
% 1.68/0.72 ![X0]: (c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)=X0|c_lessequals(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)|sQ18_spl)),
% 1.68/0.72 inference(forward_subsumption_resolution,[status(thm)],[f2362,f2288])).
% 1.68/0.72 fof(f2377,plain,(
% 1.68/0.72 ![X0]: (c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)=X0|c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)=X0|~c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)|sQ18_spl)),
% 1.68/0.72 inference(resolution,[status(thm)],[f2370,f1263])).
% 1.68/0.72 fof(f2380,plain,(
% 1.68/0.72 ![X0]: (c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)=X0|~c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)|sQ18_spl)),
% 1.68/0.72 inference(duplicate_literals_removal,[status(thm)],[f2377])).
% 1.68/0.72 fof(f2475,plain,(
% 1.68/0.72 ![X0]: (X0=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)|~c_lessequals(c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(X0,X0,tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 1.68/0.72 inference(resolution,[status(thm)],[f911,f1704])).
% 1.68/0.72 fof(f2476,plain,(
% 1.68/0.72 ![X0]: (X0=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)|c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X0,X0,tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 1.68/0.72 inference(resolution,[status(thm)],[f911,f1224])).
% 1.68/0.72 fof(f2568,definition,(
% 1.68/0.72 sQ29_spl <=> (class_Ring__and__Field_Odivision__by__zero(tc_RealDef_Oreal))),
% 1.68/0.72 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 1.68/0.72 fof(f2570,plain,(
% 1.68/0.72 ~class_Ring__and__Field_Odivision__by__zero(tc_RealDef_Oreal)|sQ29_spl),
% 1.68/0.72 inference(component_clause,[status(thm)],[f2568])).
% 1.68/0.72 fof(f2587,plain,(
% 1.68/0.72 $false|sQ29_spl),
% 1.68/0.72 inference(forward_subsumption_resolution,[status(thm)],[f2570,f1308])).
% 1.68/0.72 fof(f2588,plain,(
% 1.68/0.72 sQ29_spl),
% 1.68/0.72 inference(contradiction_clause,[status(thm)],[f2587])).
% 1.68/0.72 fof(f2612,plain,(
% 1.68/0.72 ![X0]: (X0=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)|c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)=c_HOL_Otimes__class_Otimes(X0,X0,tc_RealDef_Oreal)|sQ18_spl)),
% 1.68/0.72 inference(resolution,[status(thm)],[f2476,f2380])).
% 1.68/0.72 fof(f2629,plain,(
% 1.68/0.72 ![X0]: (X0=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)|~c_lessequals(c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)|X0=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)|sQ18_spl)),
% 1.68/0.72 inference(paramodulation,[status(thm)],[f2612,f2475])).
% 1.68/0.72 fof(f2646,definition,(
% 1.68/0.72 ![X0]: (sQ36_spl <=> (X0=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)|X0=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)))),
% 1.68/0.72 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 1.68/0.72 fof(f2647,plain,(
% 1.68/0.73 ![X0]: (X0=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)|X0=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)|~sQ36_spl)),
% 1.68/0.73 inference(component_clause,[status(thm)],[f2646])).
% 1.68/0.73 fof(f2650,plain,(
% 1.68/0.73 sQ36_spl|~sQ10_spl|sQ18_spl),
% 1.68/0.73 inference(split_clause,[status(thm)],[f2629,f2646,f1755,f2261])).
% 1.68/0.73 fof(f2658,plain,(
% 1.68/0.73 ![X0]: (X0=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)|~sQ36_spl)),
% 1.68/0.73 inference(duplicate_literals_removal,[status(thm)],[f2647])).
% 1.68/0.73 fof(f2659,plain,(
% 1.68/0.73 $false|~sQ36_spl|sQ12_spl),
% 1.68/0.73 inference(backward_subsumption_resolution,[status(thm)],[f1779,f2658])).
% 1.68/0.73 fof(f2672,plain,(
% 1.68/0.73 ~sQ36_spl|sQ12_spl),
% 1.68/0.73 inference(contradiction_clause,[status(thm)],[f2659])).
% 1.68/0.73 fof(f2673,plain,(
% 1.68/0.73 $false),
% 1.68/0.73 inference(sat_refutation,[status(thm)],[f1780,f1783,f2228,f2264,f2588,f2650,f2672])).
% 1.68/0.73 % SZS output end CNFRefutation for theBenchmark.p
% 1.68/0.76 % Elapsed time: 0.383359 seconds
% 1.68/0.76 % CPU time: 2.551443 seconds
% 1.68/0.76 % Total memory used: 145.808 MB
% 1.68/0.76 % Net memory used: 143.410 MB
%------------------------------------------------------------------------------