%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW218+1 : TPTP v9.3.1. Released v5.2.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 03:08:49 PM UTC 2026
% Result : Theorem 9.69s 1.84s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWW218+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.44 % Computer : n007.cluster.edu
% 0.17/0.44 % Model : x86_64 x86_64
% 0.17/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.44 % Memory : 8046.5625MB
% 0.17/0.44 % OS : Linux 6.8.0-71-generic
% 0.17/0.44 % CPULimit : 300
% 0.17/0.44 % WCLimit : 300
% 0.17/0.44 % DateTime : Mon Sep 21 09:39:50 UTC 2026
% 0.17/0.44 % CPUTime :
% 0.28/0.59 % Drodi V4.1.1
% 9.69/1.84 % Refutation found
% 9.69/1.84 % SZS status Theorem for theBenchmark: Theorem is valid
% 9.69/1.84 % SZS output start CNFRefutation for theBenchmark
% 9.69/1.84 fof(f3,axiom,(
% 9.69/1.84 (? [B_s] :(! [B_y] :( (? [B_x] :( (? [B_z] :( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,B_z),v_r)& c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),B_z)) = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,B_x) ))& c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B_y,B_x) ))<=> c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B_y,B_s) ) ))),
% 9.69/1.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.69/1.84 fof(f1259,hypothesis,(
% 9.69/1.84 ( (? [B_s] :(! [B_y] :( (? [B_x] :( (? [B_z] :( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,B_z),v_r)& c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),B_z)) = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,B_x) ))& c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B_y,B_x) ))<=> c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B_y,B_s) )))=> v_thesis____ ) ),
% 9.69/1.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.69/1.84 fof(f1260,conjecture,(
% 9.69/1.84 v_thesis____ ),
% 9.69/1.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.69/1.84 fof(f1261,negated_conjecture,(
% 9.69/1.84 ~(v_thesis____ )),
% 9.69/1.84 inference(negated_conjecture,[status(cth)],[f1260])).
% 9.69/1.84 fof(f1266,plain,(
% 9.69/1.84 ?[B_s]: ![B_y]: (((![B_x]: ((![B_z]: (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,B_z),v_r)|~c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),B_z))=c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,B_x)))|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B_y,B_x)))|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B_y,B_s))&((?[B_x]: ((?[B_z]: (c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,B_z),v_r)&c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),B_z))=c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,B_x)))&c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B_y,B_x)))|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B_y,B_s)))),
% 9.69/1.84 inference(NNF_transformation,[status(thm)],[f3])).
% 9.69/1.84 fof(f1267,plain,(
% 9.69/1.84 ?[B_s]: ((![B_y]: ((![B_x]: ((![B_z]: (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,B_z),v_r)|~c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),B_z))=c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,B_x)))|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B_y,B_x)))|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B_y,B_s)))&(![B_y]: ((?[B_x]: ((?[B_z]: (c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,B_z),v_r)&c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),B_z))=c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,B_x)))&c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B_y,B_x)))|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B_y,B_s))))),
% 9.69/1.84 inference(miniscoping,[status(thm)],[f1266])).
% 9.69/1.84 fof(f1268,plain,(
% 9.69/1.84 ((![B_y]: ((![B_x]: ((![B_z]: (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,B_z),v_r)|~c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),B_z))=c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,B_x)))|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B_y,B_x)))|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B_y,sK1_skl)))&(![B_y]: (((c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,sK3_skl(B_y)),v_r)&c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),sK3_skl(B_y)))=c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,sK2_skl(B_y)))&c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B_y,sK2_skl(B_y)))|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B_y,sK1_skl))))),
% 9.69/1.85 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl,sK2_skl,sK3_skl]),skolemize(B_s,sK1_skl),skolemize(B_x,sK2_skl(B_y)),skolemize(B_z,sK3_skl(B_y))],[f1267])).
% 9.69/1.85 fof(f1269,plain,(
% 9.69/1.85 ![X0,X1,X2]: (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,X0),v_r)|~c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),X0))=c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X1)|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X2,X1)|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X2,sK1_skl))),
% 9.69/1.85 inference(cnf_transformation,[status(thm)],[f1268])).
% 9.69/1.85 fof(f1270,plain,(
% 9.69/1.85 ![X0]: (c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,sK3_skl(X0)),v_r)|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,sK1_skl))),
% 9.69/1.85 inference(cnf_transformation,[status(thm)],[f1268])).
% 9.69/1.85 fof(f1271,plain,(
% 9.69/1.85 ![X0]: (c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),sK3_skl(X0)))=c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,sK2_skl(X0))|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,sK1_skl))),
% 9.69/1.85 inference(cnf_transformation,[status(thm)],[f1268])).
% 9.69/1.85 fof(f1272,plain,(
% 9.69/1.85 ![X0]: (c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,sK2_skl(X0))|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,sK1_skl))),
% 9.69/1.85 inference(cnf_transformation,[status(thm)],[f1268])).
% 9.69/1.85 fof(f4845,plain,(
% 9.69/1.85 (![B_s]: ?[B_y]: ((?[B_x]: ((?[B_z]: (c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,B_z),v_r)&c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),B_z))=c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,B_x)))&c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B_y,B_x)))<~>c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B_y,B_s)))|v_thesis____),
% 9.69/1.85 inference(pre_NNF_transformation,[status(thm)],[f1259])).
% 9.69/1.85 fof(f4846,plain,(
% 9.69/1.85 (![B_s]: ?[B_y]: (((?[B_x]: ((?[B_z]: (c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,B_z),v_r)&c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),B_z))=c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,B_x)))&c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B_y,B_x)))|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B_y,B_s))&((![B_x]: ((![B_z]: (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,B_z),v_r)|~c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),B_z))=c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,B_x)))|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B_y,B_x)))|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B_y,B_s))))|v_thesis____),
% 9.69/1.85 inference(NNF_transformation,[status(thm)],[f4845])).
% 9.69/1.85 fof(f4847,plain,(
% 9.69/1.85 (![B_s]: ((((c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,sK73_skl(B_s)),v_r)&c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),sK73_skl(B_s)))=c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,sK72_skl(B_s)))&c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(B_s),sK72_skl(B_s)))|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(B_s),B_s))&((![B_x]: ((![B_z]: (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,B_z),v_r)|~c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),B_z))=c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,B_x)))|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(B_s),B_x)))|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(B_s),B_s))))|v_thesis____),
% 9.69/1.85 inference(skolemize,[status(esa),new_symbols(skolem,[sK71_skl,sK72_skl,sK73_skl]),skolemize(B_y,sK71_skl(B_s)),skolemize(B_x,sK72_skl(B_s)),skolemize(B_z,sK73_skl(B_s))],[f4846])).
% 9.69/1.85 fof(f4848,plain,(
% 9.69/1.85 ![X0]: (c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,sK73_skl(X0)),v_r)|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(X0),X0)|v_thesis____)),
% 9.69/1.85 inference(cnf_transformation,[status(thm)],[f4847])).
% 9.69/1.85 fof(f4849,plain,(
% 9.69/1.85 ![X0]: (c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),sK73_skl(X0)))=c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,sK72_skl(X0))|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(X0),X0)|v_thesis____)),
% 9.69/1.85 inference(cnf_transformation,[status(thm)],[f4847])).
% 9.69/1.85 fof(f4850,plain,(
% 9.69/1.85 ![X0]: (c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(X0),sK72_skl(X0))|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(X0),X0)|v_thesis____)),
% 9.69/1.85 inference(cnf_transformation,[status(thm)],[f4847])).
% 9.69/1.85 fof(f4851,plain,(
% 9.69/1.85 ![X0,X1,X2]: (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,X0),v_r)|~c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),X0))=c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X1)|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(X2),X1)|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(X2),X2)|v_thesis____)),
% 9.69/1.85 inference(cnf_transformation,[status(thm)],[f4847])).
% 9.69/1.85 fof(f4852,plain,(
% 9.69/1.85 ~v_thesis____),
% 9.69/1.85 inference(cnf_transformation,[status(thm)],[f1261])).
% 9.69/1.85 fof(f5127,plain,(
% 9.69/1.85 ![X0,X1,X2]: (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,X0),v_r)|~c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),X0))=c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X1)|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(X2),X1)|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(X2),X2))),
% 9.69/1.85 inference(backward_subsumption_resolution,[status(thm)],[f4851,f4852])).
% 9.69/1.85 fof(f5128,plain,(
% 9.69/1.85 ![X0]: (c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(X0),sK72_skl(X0))|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(X0),X0))),
% 9.69/1.85 inference(backward_subsumption_resolution,[status(thm)],[f4850,f4852])).
% 9.69/1.85 fof(f5129,plain,(
% 9.69/1.85 ![X0]: (c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),sK73_skl(X0)))=c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,sK72_skl(X0))|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(X0),X0))),
% 9.69/1.85 inference(backward_subsumption_resolution,[status(thm)],[f4849,f4852])).
% 9.69/1.85 fof(f5130,plain,(
% 9.69/1.85 ![X0]: (c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,sK73_skl(X0)),v_r)|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(X0),X0))),
% 9.69/1.85 inference(backward_subsumption_resolution,[status(thm)],[f4848,f4852])).
% 9.69/1.85 fof(f5135,plain,(
% 9.69/1.85 ![X0,X1,X2]: (~c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),sK73_skl(X0)))=c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X1)|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X2,X1)|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X2,sK1_skl)|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(X0),X0))),
% 9.69/1.85 inference(resolution,[status(thm)],[f1269,f5130])).
% 9.69/1.85 fof(f5140,plain,(
% 9.69/1.85 c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),sK3_skl(sK71_skl(sK1_skl))))=c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,sK2_skl(sK71_skl(sK1_skl)))|c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),sK73_skl(sK1_skl)))=c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,sK72_skl(sK1_skl))),
% 9.69/1.85 inference(resolution,[status(thm)],[f1271,f5129])).
% 9.69/1.85 fof(f5144,plain,(
% 9.69/1.85 ![X0]: (c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),sK73_skl(sK1_skl)))=c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,sK72_skl(sK1_skl))|~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,sK3_skl(sK71_skl(sK1_skl))),v_r)|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(X0),sK2_skl(sK71_skl(sK1_skl)))|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(X0),X0))),
% 9.69/1.85 inference(resolution,[status(thm)],[f5140,f5127])).
% 9.69/1.85 fof(f5147,plain,(
% 9.69/1.85 ![X0]: (c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),sK73_skl(sK1_skl)))=c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,sK72_skl(sK1_skl))|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(X0),sK2_skl(sK71_skl(sK1_skl)))|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(X0),X0)|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(sK1_skl),sK1_skl))),
% 9.69/1.85 inference(resolution,[status(thm)],[f5144,f1270])).
% 9.69/1.85 fof(f5148,plain,(
% 9.69/1.85 ![X0]: (c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),sK73_skl(sK1_skl)))=c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,sK72_skl(sK1_skl))|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(X0),sK2_skl(sK71_skl(sK1_skl)))|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(X0),X0))),
% 9.69/1.85 inference(forward_subsumption_resolution,[status(thm)],[f5147,f5129])).
% 9.69/1.85 fof(f5153,plain,(
% 9.69/1.85 c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),sK73_skl(sK1_skl)))=c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,sK72_skl(sK1_skl))|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(sK1_skl),sK1_skl)|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(sK1_skl),sK1_skl)),
% 9.69/1.85 inference(resolution,[status(thm)],[f5148,f1272])).
% 9.69/1.85 fof(f5156,plain,(
% 9.69/1.85 c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),sK73_skl(sK1_skl)))=c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,sK72_skl(sK1_skl))|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(sK1_skl),sK1_skl)),
% 9.69/1.85 inference(duplicate_literals_removal,[status(thm)],[f5153])).
% 9.69/1.85 fof(f5166,plain,(
% 9.69/1.85 c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),sK73_skl(sK1_skl)))=c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,sK72_skl(sK1_skl))),
% 9.69/1.85 inference(forward_subsumption_resolution,[status(thm)],[f5156,f5129])).
% 9.69/1.85 fof(f5167,plain,(
% 9.69/1.85 ![X0]: (~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,sK72_skl(sK1_skl))|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,sK1_skl)|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(sK1_skl),sK1_skl))),
% 9.69/1.85 inference(resolution,[status(thm)],[f5166,f5135])).
% 9.69/1.85 fof(f5169,plain,(
% 9.69/1.85 ![X0,X1]: (~c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,sK72_skl(sK1_skl))=c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0)|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X1,X0)|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X1,sK1_skl)|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(sK1_skl),sK1_skl))),
% 9.69/1.85 inference(paramodulation,[status(thm)],[f5166,f5135])).
% 9.69/1.85 fof(f5172,plain,(
% 9.69/1.85 ![X0]: (~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,sK72_skl(sK1_skl))|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,sK1_skl)|c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),sK3_skl(sK71_skl(sK1_skl))))=c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,sK2_skl(sK71_skl(sK1_skl))))),
% 9.69/1.85 inference(resolution,[status(thm)],[f5167,f1271])).
% 9.69/1.85 fof(f5187,plain,(
% 9.69/1.85 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(sK1_skl),sK1_skl)|c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),sK3_skl(sK71_skl(sK1_skl))))=c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,sK2_skl(sK71_skl(sK1_skl)))|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(sK1_skl),sK1_skl)),
% 9.69/1.85 inference(resolution,[status(thm)],[f5172,f5128])).
% 9.69/1.85 fof(f5190,plain,(
% 9.69/1.85 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(sK1_skl),sK1_skl)|c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),sK3_skl(sK71_skl(sK1_skl))))=c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,sK2_skl(sK71_skl(sK1_skl)))),
% 9.69/1.90 inference(duplicate_literals_removal,[status(thm)],[f5187])).
% 9.69/1.90 fof(f5200,plain,(
% 9.69/1.90 c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),sK3_skl(sK71_skl(sK1_skl))))=c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,sK2_skl(sK71_skl(sK1_skl)))),
% 9.69/1.90 inference(forward_subsumption_resolution,[status(thm)],[f5190,f1271])).
% 9.69/1.90 fof(f5201,plain,(
% 9.69/1.90 ![X0]: (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,sK3_skl(sK71_skl(sK1_skl))),v_r)|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(X0),sK2_skl(sK71_skl(sK1_skl)))|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(X0),X0))),
% 9.69/1.90 inference(resolution,[status(thm)],[f5200,f5127])).
% 9.69/1.90 fof(f5208,plain,(
% 9.69/1.90 ![X0]: (~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(X0),sK2_skl(sK71_skl(sK1_skl)))|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(X0),X0)|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(sK1_skl),sK1_skl))),
% 9.69/1.90 inference(resolution,[status(thm)],[f5201,f1270])).
% 9.69/1.90 fof(f5211,plain,(
% 9.69/1.90 ~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(sK1_skl),sK1_skl)|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(sK1_skl),sK1_skl)|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(sK1_skl),sK1_skl)),
% 9.69/1.90 inference(resolution,[status(thm)],[f5208,f1272])).
% 9.69/1.90 fof(f5215,plain,(
% 9.69/1.90 ![X0,X1]: (~c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,sK72_skl(sK1_skl))=c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0)|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X1,X0)|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X1,sK1_skl))),
% 9.69/1.90 inference(backward_subsumption_resolution,[status(thm)],[f5169,f5222])).
% 9.69/1.90 fof(f5222,plain,(
% 9.69/1.90 ~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(sK1_skl),sK1_skl)),
% 9.69/1.90 inference(duplicate_literals_removal,[status(thm)],[f5211])).
% 9.69/1.90 fof(f5235,plain,(
% 9.69/1.90 ![X0]: (~c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,sK72_skl(sK1_skl))=c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0)|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(sK1_skl),X0))),
% 9.69/1.90 inference(resolution,[status(thm)],[f5215,f5222])).
% 9.69/1.90 fof(f5243,plain,(
% 9.69/1.90 ~c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,sK72_skl(sK1_skl))=c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,sK72_skl(sK1_skl))|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(sK1_skl),sK1_skl)),
% 9.69/1.90 inference(resolution,[status(thm)],[f5235,f5128])).
% 9.69/1.90 fof(f5251,plain,(
% 9.69/1.90 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(sK1_skl),sK1_skl)),
% 9.69/1.90 inference(trivial_equality_resolution,[status(thm)],[f5243])).
% 9.69/1.90 fof(f5252,plain,(
% 9.69/1.90 $false),
% 9.69/1.90 inference(forward_subsumption_resolution,[status(thm)],[f5251,f5222])).
% 9.69/1.90 % SZS output end CNFRefutation for theBenchmark.p
% 9.69/1.90 % Elapsed time: 1.454175 seconds
% 9.69/1.90 % CPU time: 10.197973 seconds
% 9.69/1.90 % Total memory used: 284.466 MB
% 9.69/1.90 % Net memory used: 279.122 MB
%------------------------------------------------------------------------------