%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : ALG372-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n007.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:06 AM UTC 2026
% Result : Unsatisfiable 17.97s 3.02s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG372-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.58 % Computer : n007.cluster.edu
% 0.09/0.58 % Model : x86_64 x86_64
% 0.09/0.58 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.58 % Memory : 8046.5625MB
% 0.09/0.58 % OS : Linux 6.8.0-71-generic
% 0.09/0.58 % CPULimit : 300
% 0.09/0.58 % WCLimit : 300
% 0.09/0.58 % DateTime : Mon Sep 21 13:16:06 UTC 2026
% 0.09/0.58 % CPUTime :
% 0.14/0.68 % Drodi V4.1.1
% 17.97/3.02 % Refutation found
% 17.97/3.02 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 17.97/3.02 % SZS output start CNFRefutation for theBenchmark
% 17.97/3.02 fof(f684,axiom,(
% 17.97/3.02 (![T_a]: (( ~ class_RealVector_Oreal__normed__vector(T_a)| c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(T_a),T_a) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ) ))),
% 17.97/3.02 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.97/3.02 fof(f699,axiom,(
% 17.97/3.02 c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_r,tc_RealDef_Oreal) ),
% 17.97/3.02 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.97/3.02 fof(f708,axiom,(
% 17.97/3.02 (![V_w,V_z]: (( c_lessequals(V_w,V_z,tc_RealDef_Oreal)| c_lessequals(V_z,V_w,tc_RealDef_Oreal) ) ))),
% 17.97/3.02 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.97/3.02 fof(f712,axiom,(
% 17.97/3.02 (![V_w]: (c_lessequals(V_w,V_w,tc_RealDef_Oreal) ))),
% 17.97/3.02 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.97/3.02 fof(f713,axiom,(
% 17.97/3.02 (![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) ) ))),
% 17.97/3.02 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.97/3.02 fof(f737,axiom,(
% 17.97/3.02 (![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) ) ))),
% 17.97/3.02 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.97/3.02 fof(f744,axiom,(
% 17.97/3.02 (![T_a,V_b]: (( ~ class_OrderedGroup_Ogroup__add(T_a)| c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(V_b,T_a),T_a) = V_b ) ))),
% 17.97/3.02 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.97/3.02 fof(f754,negated_conjecture,(
% 17.97/3.02 ( 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_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_p,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal)| ~ c_lessequals(c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_r,tc_RealDef_Oreal) ) ),
% 17.97/3.02 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.97/3.02 fof(f855,axiom,(
% 17.97/3.02 class_OrderedGroup_Ogroup__add(tc_RealDef_Oreal) ),
% 17.97/3.02 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.97/3.02 fof(f880,axiom,(
% 17.97/3.02 class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex) ),
% 17.97/3.02 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.97/3.02 fof(f2131,plain,(
% 17.97/3.02 ![X0]: (~class_RealVector_Oreal__normed__vector(X0)|c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(X0),X0)=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal))),
% 17.97/3.02 inference(cnf_transformation,[status(thm)],[f684])).
% 17.97/3.02 fof(f2155,plain,(
% 17.97/3.02 c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_r,tc_RealDef_Oreal)),
% 17.97/3.02 inference(cnf_transformation,[status(thm)],[f699])).
% 17.97/3.02 fof(f2167,plain,(
% 17.97/3.02 ![X0,X1]: (c_lessequals(X0,X1,tc_RealDef_Oreal)|c_lessequals(X1,X0,tc_RealDef_Oreal))),
% 17.97/3.02 inference(cnf_transformation,[status(thm)],[f708])).
% 17.97/3.02 fof(f2173,plain,(
% 17.97/3.02 ![X0]: (c_lessequals(X0,X0,tc_RealDef_Oreal))),
% 17.97/3.02 inference(cnf_transformation,[status(thm)],[f712])).
% 17.97/3.02 fof(f2174,plain,(
% 17.97/3.02 ![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))),
% 17.97/3.02 inference(miniscoping,[status(thm)],[f713])).
% 17.97/3.02 fof(f2175,plain,(
% 17.97/3.02 ![X0,X1,X2]: (c_lessequals(X0,X1,tc_RealDef_Oreal)|~c_lessequals(X2,X1,tc_RealDef_Oreal)|~c_lessequals(X0,X2,tc_RealDef_Oreal))),
% 17.97/3.02 inference(cnf_transformation,[status(thm)],[f2174])).
% 17.97/3.02 fof(f2202,plain,(
% 17.97/3.02 ![X0,X1]: (X0=X1|~c_lessequals(X1,X0,tc_RealDef_Oreal)|~c_lessequals(X0,X1,tc_RealDef_Oreal))),
% 17.97/3.02 inference(cnf_transformation,[status(thm)],[f737])).
% 17.97/3.02 fof(f2211,plain,(
% 17.97/3.02 ![T_a]: (~class_OrderedGroup_Ogroup__add(T_a)|(![V_b]: c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(V_b,T_a),T_a)=V_b))),
% 17.97/3.02 inference(miniscoping,[status(thm)],[f744])).
% 17.97/3.02 fof(f2212,plain,(
% 17.97/3.02 ![X0,X1]: (~class_OrderedGroup_Ogroup__add(X0)|c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(X1,X0),X0)=X1)),
% 17.97/3.02 inference(cnf_transformation,[status(thm)],[f2211])).
% 17.97/3.02 fof(f2226,plain,(
% 17.97/3.02 ~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_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_p,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal)|~c_lessequals(c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_r,tc_RealDef_Oreal)),
% 17.97/3.02 inference(cnf_transformation,[status(thm)],[f754])).
% 17.97/3.02 fof(f2327,plain,(
% 17.97/3.02 class_OrderedGroup_Ogroup__add(tc_RealDef_Oreal)),
% 17.97/3.02 inference(cnf_transformation,[status(thm)],[f855])).
% 17.97/3.02 fof(f2352,plain,(
% 17.97/3.02 class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex)),
% 17.97/3.02 inference(cnf_transformation,[status(thm)],[f880])).
% 17.97/3.02 fof(f2432,definition,(
% 17.97/3.02 sQ2_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_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_p,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 17.97/3.02 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 17.97/3.02 fof(f2434,plain,(
% 17.97/3.02 ~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_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_p,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),tc_RealDef_Oreal)|sQ2_spl),
% 17.97/3.02 inference(component_clause,[status(thm)],[f2432])).
% 17.97/3.02 fof(f2435,definition,(
% 17.97/3.02 sQ3_spl <=> (c_lessequals(c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_r,tc_RealDef_Oreal))),
% 17.97/3.02 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 17.97/3.02 fof(f2437,plain,(
% 17.97/3.02 ~c_lessequals(c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_r,tc_RealDef_Oreal)|sQ3_spl),
% 17.97/3.02 inference(component_clause,[status(thm)],[f2435])).
% 17.97/3.02 fof(f2438,plain,(
% 17.97/3.02 ~sQ2_spl|~sQ3_spl),
% 17.97/3.02 inference(split_clause,[status(thm)],[f2226,f2432,f2435])).
% 17.97/3.02 fof(f2460,definition,(
% 17.97/3.02 sQ4_spl <=> (v_r=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal))),
% 17.97/3.02 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 17.97/3.02 fof(f2461,plain,(
% 17.97/3.02 v_r=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)|~sQ4_spl),
% 17.97/3.02 inference(component_clause,[status(thm)],[f2460])).
% 17.97/3.02 fof(f2468,plain,(
% 17.97/3.02 ![X0,X1,X2]: (~c_lessequals(X0,X1,tc_RealDef_Oreal)|~c_lessequals(X2,X0,tc_RealDef_Oreal)|X1=X2|~c_lessequals(X1,X2,tc_RealDef_Oreal))),
% 17.97/3.02 inference(resolution,[status(thm)],[f2175,f2202])).
% 17.97/3.02 fof(f2583,plain,(
% 17.97/3.02 ![X0]: (~c_lessequals(X0,v_r,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)|sQ3_spl)),
% 17.97/3.02 inference(resolution,[status(thm)],[f2437,f2175])).
% 17.97/3.02 fof(f2584,plain,(
% 17.97/3.02 c_lessequals(v_r,c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal)|sQ3_spl),
% 17.97/3.02 inference(resolution,[status(thm)],[f2437,f2167])).
% 17.97/3.02 fof(f2586,plain,(
% 17.97/3.02 ![X0,X1]: (~c_lessequals(X0,v_r,tc_RealDef_Oreal)|~c_lessequals(X1,X0,tc_RealDef_Oreal)|~c_lessequals(c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),X1,tc_RealDef_Oreal)|sQ3_spl)),
% 17.97/3.02 inference(resolution,[status(thm)],[f2583,f2175])).
% 17.97/3.02 fof(f2596,plain,(
% 17.97/3.02 ![X0,X1]: (~c_lessequals(X0,X1,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)|c_lessequals(v_r,X1,tc_RealDef_Oreal)|sQ3_spl)),
% 17.97/3.02 inference(resolution,[status(thm)],[f2586,f2167])).
% 17.97/3.02 fof(f2610,definition,(
% 17.97/3.02 sQ11_spl <=> (c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex)=v_r)),
% 17.97/3.02 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 17.97/3.02 fof(f2611,plain,(
% 17.97/3.02 c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex)=v_r|~sQ11_spl),
% 17.97/3.02 inference(component_clause,[status(thm)],[f2610])).
% 17.97/3.02 fof(f2628,plain,(
% 17.97/3.02 ![X0,X1]: (~c_lessequals(X0,v_r,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)|~c_lessequals(X1,v_r,tc_RealDef_Oreal)|~c_lessequals(c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),X1,tc_RealDef_Oreal)|sQ3_spl)),
% 17.97/3.02 inference(resolution,[status(thm)],[f2596,f2586])).
% 17.97/3.02 fof(f2630,definition,(
% 17.97/3.02 ![X0]: (sQ12_spl <=> (~c_lessequals(X0,v_r,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)))),
% 17.97/3.02 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 17.97/3.02 fof(f2631,plain,(
% 17.97/3.02 ![X0]: (~c_lessequals(X0,v_r,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)|~sQ12_spl)),
% 17.97/3.02 inference(component_clause,[status(thm)],[f2630])).
% 17.97/3.02 fof(f2633,plain,(
% 17.97/3.02 sQ12_spl|sQ3_spl),
% 17.97/3.02 inference(split_clause,[status(thm)],[f2628,f2630,f2435])).
% 17.97/3.02 fof(f2635,plain,(
% 17.97/3.02 ~c_lessequals(c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_r,tc_RealDef_Oreal)|~sQ12_spl),
% 17.97/3.02 inference(resolution,[status(thm)],[f2631,f2167])).
% 17.97/3.02 fof(f3094,plain,(
% 17.97/3.02 ~c_lessequals(v_r,v_r,tc_RealDef_Oreal)|~sQ11_spl|~sQ12_spl),
% 17.97/3.02 inference(forward_demodulation,[status(thm)],[f2611,f2635])).
% 17.97/3.02 fof(f3095,plain,(
% 17.97/3.02 $false|~sQ11_spl|~sQ12_spl),
% 17.97/3.02 inference(forward_subsumption_resolution,[status(thm)],[f3094,f2173])).
% 17.97/3.02 fof(f3096,plain,(
% 17.97/3.02 ~sQ11_spl|~sQ12_spl),
% 17.97/3.02 inference(contradiction_clause,[status(thm)],[f3095])).
% 17.97/3.02 fof(f3379,definition,(
% 17.97/3.02 sQ39_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))),
% 17.97/3.02 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 17.97/3.02 fof(f3380,plain,(
% 17.97/3.02 c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)=c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex)|~sQ39_spl),
% 17.97/3.02 inference(component_clause,[status(thm)],[f3379])).
% 17.97/3.02 fof(f3381,plain,(
% 17.97/3.02 ~c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)=c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex)|sQ39_spl),
% 17.97/3.02 inference(component_clause,[status(thm)],[f3379])).
% 17.97/3.02 fof(f3393,plain,(
% 17.97/3.02 c_lessequals(v_r,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)|~sQ39_spl|sQ3_spl),
% 17.97/3.02 inference(backward_demodulation,[status(thm)],[f3380,f2584])).
% 17.97/3.02 fof(f3430,plain,(
% 17.97/3.02 ![X0]: (~c_lessequals(X0,v_r,tc_RealDef_Oreal)|~c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)|v_r=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)|~sQ39_spl|sQ3_spl)),
% 17.97/3.02 inference(resolution,[status(thm)],[f3393,f2468])).
% 17.97/3.02 fof(f3433,definition,(
% 17.97/3.02 ![X0]: (sQ45_spl <=> (~c_lessequals(X0,v_r,tc_RealDef_Oreal)|~c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)))),
% 17.97/3.02 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 17.97/3.02 fof(f3434,plain,(
% 17.97/3.02 ![X0]: (~c_lessequals(X0,v_r,tc_RealDef_Oreal)|~c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)|~sQ45_spl)),
% 17.97/3.02 inference(component_clause,[status(thm)],[f3433])).
% 17.97/3.02 fof(f3436,plain,(
% 17.97/3.02 sQ45_spl|sQ4_spl|~sQ39_spl|sQ3_spl),
% 17.97/3.02 inference(split_clause,[status(thm)],[f3430,f3433,f2460,f3379,f2435])).
% 17.97/3.02 fof(f3893,plain,(
% 17.97/3.02 ~c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)|~sQ45_spl),
% 17.97/3.02 inference(resolution,[status(thm)],[f3434,f2155])).
% 17.97/3.02 fof(f3901,plain,(
% 17.97/3.02 $false|~sQ45_spl),
% 17.97/3.05 inference(forward_subsumption_resolution,[status(thm)],[f3893,f2173])).
% 17.97/3.05 fof(f3902,plain,(
% 17.97/3.05 ~sQ45_spl),
% 17.97/3.05 inference(contradiction_clause,[status(thm)],[f3901])).
% 17.97/3.05 fof(f4817,plain,(
% 17.97/3.05 ![X0]: (c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal),tc_RealDef_Oreal)=X0)),
% 17.97/3.05 inference(resolution,[status(thm)],[f2212,f2327])).
% 17.97/3.05 fof(f4819,plain,(
% 17.97/3.05 ~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,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex)|sQ2_spl),
% 17.97/3.05 inference(backward_demodulation,[status(thm)],[f4817,f2434])).
% 17.97/3.05 fof(f4822,plain,(
% 17.97/3.05 $false|sQ2_spl),
% 17.97/3.05 inference(trivial_equality_resolution,[status(thm)],[f4819])).
% 17.97/3.05 fof(f4823,plain,(
% 17.97/3.05 sQ2_spl),
% 17.97/3.05 inference(contradiction_clause,[status(thm)],[f4822])).
% 17.97/3.05 fof(f11392,plain,(
% 17.97/3.05 ![X0]: (~class_RealVector_Oreal__normed__vector(X0)|c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(X0),X0)=v_r|~sQ4_spl)),
% 17.97/3.05 inference(forward_demodulation,[status(thm)],[f2461,f2131])).
% 17.97/3.05 fof(f11393,plain,(
% 17.97/3.05 c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex)=v_r|~sQ4_spl),
% 17.97/3.05 inference(resolution,[status(thm)],[f11392,f2352])).
% 17.97/3.05 fof(f11395,plain,(
% 17.97/3.05 sQ11_spl|~sQ4_spl),
% 17.97/3.05 inference(split_clause,[status(thm)],[f11393,f2610,f2460])).
% 17.97/3.05 fof(f12772,plain,(
% 17.97/3.05 c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)),
% 17.97/3.05 inference(resolution,[status(thm)],[f2131,f2352])).
% 17.97/3.05 fof(f12774,plain,(
% 17.97/3.05 $false|sQ39_spl),
% 17.97/3.05 inference(forward_subsumption_resolution,[status(thm)],[f12772,f3381])).
% 17.97/3.05 fof(f12775,plain,(
% 17.97/3.05 sQ39_spl),
% 17.97/3.05 inference(contradiction_clause,[status(thm)],[f12774])).
% 17.97/3.05 fof(f12776,plain,(
% 17.97/3.05 $false),
% 17.97/3.05 inference(sat_refutation,[status(thm)],[f2438,f2633,f3096,f3436,f3902,f4823,f11395,f12775])).
% 17.97/3.05 % SZS output end CNFRefutation for theBenchmark.p
% 17.97/3.07 % Elapsed time: 2.466369 seconds
% 17.97/3.07 % CPU time: 18.381058 seconds
% 17.97/3.07 % Total memory used: 265.876 MB
% 17.97/3.07 % Net memory used: 259.084 MB
%------------------------------------------------------------------------------