%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW219+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 2.10s 0.92s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW219+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n007.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 09:39:36 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.26/0.52 % Drodi V4.1.1
% 2.10/0.92 % Refutation found
% 2.10/0.92 % SZS status Theorem for theBenchmark: Theorem is valid
% 2.10/0.92 % SZS output start CNFRefutation for theBenchmark
% 2.10/0.92 fof(f5,axiom,(
% 2.10/0.92 (? [B_f] :(! [B_x] :( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(B_f,B_x)),v_r)& c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),hAPP(B_f,B_x))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_RealDef_Oreal(tc_Nat_Onat,c_Nat_OSuc(B_x))))) ) ))),
% 2.10/0.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.10/0.92 fof(f1266,hypothesis,(
% 2.10/0.92 (! [B_g] :( (! [B_n] : c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(B_g,B_n)),v_r))=> ( (! [B_n] : c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),hAPP(B_g,B_n))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_RealDef_Oreal(tc_Nat_Onat,c_Nat_OSuc(B_n))))))=> v_thesis____ ) ) )),
% 2.10/0.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.10/0.92 fof(f1267,conjecture,(
% 2.10/0.92 v_thesis____ ),
% 2.10/0.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.10/0.92 fof(f1268,negated_conjecture,(
% 2.10/0.92 ~(v_thesis____ )),
% 2.10/0.92 inference(negated_conjecture,[status(cth)],[f1267])).
% 2.10/0.92 fof(f1278,plain,(
% 2.10/0.92 ?[B_f]: ((![B_x]: c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(B_f,B_x)),v_r))&(![B_x]: c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),hAPP(B_f,B_x))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_RealDef_Oreal(tc_Nat_Onat,c_Nat_OSuc(B_x)))))))),
% 2.10/0.92 inference(miniscoping,[status(thm)],[f5])).
% 2.10/0.92 fof(f1279,plain,(
% 2.10/0.92 ((![B_x]: c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(sK1_skl,B_x)),v_r))&(![B_x]: c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),hAPP(sK1_skl,B_x))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_RealDef_Oreal(tc_Nat_Onat,c_Nat_OSuc(B_x)))))))),
% 2.10/0.92 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(B_f,sK1_skl)],[f1278])).
% 2.10/0.92 fof(f1280,plain,(
% 2.10/0.92 ![X0]: (c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(sK1_skl,X0)),v_r))),
% 2.10/0.92 inference(cnf_transformation,[status(thm)],[f1279])).
% 2.10/0.92 fof(f1281,plain,(
% 2.10/0.92 ![X0]: (c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),hAPP(sK1_skl,X0))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_RealDef_Oreal(tc_Nat_Onat,c_Nat_OSuc(X0))))))),
% 2.10/0.92 inference(cnf_transformation,[status(thm)],[f1279])).
% 2.10/0.92 fof(f4864,plain,(
% 2.10/0.92 ![B_g]: ((?[B_n]: ~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(B_g,B_n)),v_r))|((?[B_n]: ~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),hAPP(B_g,B_n))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_RealDef_Oreal(tc_Nat_Onat,c_Nat_OSuc(B_n))))))|v_thesis____))),
% 2.53/0.95 inference(pre_NNF_transformation,[status(thm)],[f1266])).
% 2.53/0.95 fof(f4865,plain,(
% 2.53/0.95 ![B_g]: (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(B_g,sK79_skl(B_g))),v_r)|(~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),hAPP(B_g,sK80_skl(B_g)))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_RealDef_Oreal(tc_Nat_Onat,c_Nat_OSuc(sK80_skl(B_g))))))|v_thesis____))),
% 2.53/0.95 inference(skolemize,[status(esa),new_symbols(skolem,[sK79_skl,sK80_skl]),skolemize(B_n,sK79_skl(B_g)),skolemize(B_n,sK80_skl(B_g))],[f4864])).
% 2.53/0.95 fof(f4866,plain,(
% 2.53/0.95 ![X0]: (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(X0,sK79_skl(X0))),v_r)|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),hAPP(X0,sK80_skl(X0)))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_RealDef_Oreal(tc_Nat_Onat,c_Nat_OSuc(sK80_skl(X0))))))|v_thesis____)),
% 2.53/0.95 inference(cnf_transformation,[status(thm)],[f4865])).
% 2.53/0.95 fof(f4867,plain,(
% 2.53/0.95 ~v_thesis____),
% 2.53/0.95 inference(cnf_transformation,[status(thm)],[f1268])).
% 2.53/0.95 fof(f5196,plain,(
% 2.53/0.95 ![X0]: (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(X0,sK79_skl(X0))),v_r)|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),hAPP(X0,sK80_skl(X0)))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_RealDef_Oreal(tc_Nat_Onat,c_Nat_OSuc(sK80_skl(X0)))))))),
% 2.53/0.95 inference(backward_subsumption_resolution,[status(thm)],[f4866,f4867])).
% 2.53/0.95 fof(f5208,plain,(
% 2.53/0.95 ~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),hAPP(sK1_skl,sK80_skl(sK1_skl)))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_RealDef_Oreal(tc_Nat_Onat,c_Nat_OSuc(sK80_skl(sK1_skl))))))),
% 2.53/0.95 inference(resolution,[status(thm)],[f1280,f5196])).
% 2.53/0.95 fof(f5211,plain,(
% 2.53/0.95 $false),
% 2.53/0.95 inference(forward_subsumption_resolution,[status(thm)],[f5208,f1281])).
% 2.53/0.95 % SZS output end CNFRefutation for theBenchmark.p
% 2.53/0.97 % Elapsed time: 0.599278 seconds
% 2.53/0.97 % CPU time: 3.310166 seconds
% 2.53/0.97 % Total memory used: 235.815 MB
% 2.53/0.97 % Net memory used: 233.940 MB
%------------------------------------------------------------------------------