%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW213+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 : n011.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 72.25s 9.62s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW213+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n011.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 09:40:57 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.12/0.44 % Drodi V4.1.1
% 72.25/9.62 % Refutation found
% 72.25/9.62 % SZS status Theorem for theBenchmark: Theorem is valid
% 72.25/9.62 % SZS output start CNFRefutation for theBenchmark
% 72.25/9.62 fof(f3,axiom,(
% 72.25/9.62 (! [V_x,V_h,V_p,T_a] :( class_Rings_Ocomm__semiring__0(T_a)=> hAPP(c_Polynomial_Opoly(T_a,c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(T_a,V_p,V_h)),V_x) = hAPP(c_Polynomial_Opoly(T_a,V_p),c_Groups_Oplus__class_Oplus(T_a,V_h,V_x)) ) )),
% 72.25/9.62 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 72.25/9.62 fof(f14,axiom,(
% 72.25/9.62 (! [V_h,V_p,T_a] :( class_Rings_Ocomm__semiring__0(T_a)=> c_Polynomial_Odegree(T_a,c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(T_a,V_p,V_h)) = c_Polynomial_Odegree(T_a,V_p) ) )),
% 72.25/9.62 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 72.25/9.62 fof(f20,axiom,(
% 72.25/9.62 (! [V_a,V_p] :(? [B_q] :( c_Fundamental__Theorem__Algebra__Mirabelle_Opsize(tc_Complex_Ocomplex,B_q) = c_Fundamental__Theorem__Algebra__Mirabelle_Opsize(tc_Complex_Ocomplex,V_p)& (! [B_x] : hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,B_q),B_x) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,V_p),c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,V_a,B_x)) )) ))),
% 72.25/9.62 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 72.25/9.62 fof(f1181,axiom,(
% 72.25/9.62 class_Rings_Ocomm__semiring__0(tc_Complex_Ocomplex) ),
% 72.25/9.62 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 72.25/9.62 fof(f1263,hypothesis,(
% 72.25/9.62 (! [B_q] :( c_Polynomial_Odegree(tc_Complex_Ocomplex,B_q) = c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p)=> ( (! [B_x] : hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,B_q),B_x) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,v_z,B_x)))=> v_thesis____ ) ) )),
% 72.25/9.62 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 72.25/9.62 fof(f1264,conjecture,(
% 72.25/9.62 v_thesis____ ),
% 72.25/9.62 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 72.25/9.62 fof(f1265,negated_conjecture,(
% 72.25/9.62 ~(v_thesis____ )),
% 72.25/9.62 inference(negated_conjecture,[status(cth)],[f1264])).
% 72.25/9.62 fof(f1272,plain,(
% 72.25/9.62 ![V_x,V_h,V_p,T_a]: (~class_Rings_Ocomm__semiring__0(T_a)|hAPP(c_Polynomial_Opoly(T_a,c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(T_a,V_p,V_h)),V_x)=hAPP(c_Polynomial_Opoly(T_a,V_p),c_Groups_Oplus__class_Oplus(T_a,V_h,V_x)))),
% 72.25/9.62 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 72.25/9.62 fof(f1273,plain,(
% 72.25/9.62 ![T_a]: (~class_Rings_Ocomm__semiring__0(T_a)|(![V_x,V_h,V_p]: hAPP(c_Polynomial_Opoly(T_a,c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(T_a,V_p,V_h)),V_x)=hAPP(c_Polynomial_Opoly(T_a,V_p),c_Groups_Oplus__class_Oplus(T_a,V_h,V_x))))),
% 72.25/9.62 inference(miniscoping,[status(thm)],[f1272])).
% 72.25/9.62 fof(f1274,plain,(
% 72.25/9.62 ![X0,X1,X2,X3]: (~class_Rings_Ocomm__semiring__0(X0)|hAPP(c_Polynomial_Opoly(X0,c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(X0,X1,X2)),X3)=hAPP(c_Polynomial_Opoly(X0,X1),c_Groups_Oplus__class_Oplus(X0,X2,X3)))),
% 72.25/9.62 inference(cnf_transformation,[status(thm)],[f1273])).
% 72.25/9.62 fof(f1311,plain,(
% 72.25/9.62 ![V_h,V_p,T_a]: (~class_Rings_Ocomm__semiring__0(T_a)|c_Polynomial_Odegree(T_a,c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(T_a,V_p,V_h))=c_Polynomial_Odegree(T_a,V_p))),
% 72.25/9.62 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 72.25/9.62 fof(f1312,plain,(
% 72.25/9.62 ![T_a]: (~class_Rings_Ocomm__semiring__0(T_a)|(![V_h,V_p]: c_Polynomial_Odegree(T_a,c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(T_a,V_p,V_h))=c_Polynomial_Odegree(T_a,V_p)))),
% 72.25/9.62 inference(miniscoping,[status(thm)],[f1311])).
% 72.25/9.62 fof(f1313,plain,(
% 72.25/9.62 ![X0,X1,X2]: (~class_Rings_Ocomm__semiring__0(X0)|c_Polynomial_Odegree(X0,c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(X0,X1,X2))=c_Polynomial_Odegree(X0,X1))),
% 72.25/9.62 inference(cnf_transformation,[status(thm)],[f1312])).
% 72.25/9.62 fof(f1329,plain,(
% 72.25/9.62 ![V_a,V_p]: (c_Fundamental__Theorem__Algebra__Mirabelle_Opsize(tc_Complex_Ocomplex,sK1_skl(V_p,V_a))=c_Fundamental__Theorem__Algebra__Mirabelle_Opsize(tc_Complex_Ocomplex,V_p)&(![B_x]: hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,sK1_skl(V_p,V_a)),B_x)=hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,V_p),c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,V_a,B_x))))),
% 72.25/9.62 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(B_q,sK1_skl(V_p,V_a))],[f20])).
% 72.25/9.70 fof(f1331,plain,(
% 72.25/9.70 ![X0,X1,X2]: (hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,sK1_skl(X0,X1)),X2)=hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,X0),c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,X1,X2)))),
% 72.25/9.70 inference(cnf_transformation,[status(thm)],[f1329])).
% 72.25/9.70 fof(f4681,plain,(
% 72.25/9.70 class_Rings_Ocomm__semiring__0(tc_Complex_Ocomplex)),
% 72.25/9.70 inference(cnf_transformation,[status(thm)],[f1181])).
% 72.25/9.70 fof(f4820,plain,(
% 72.25/9.70 ![B_q]: (~c_Polynomial_Odegree(tc_Complex_Ocomplex,B_q)=c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p)|((?[B_x]: ~hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,B_q),B_x)=hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,v_z,B_x)))|v_thesis____))),
% 72.25/9.70 inference(pre_NNF_transformation,[status(thm)],[f1263])).
% 72.25/9.70 fof(f4821,plain,(
% 72.25/9.70 ![B_q]: (~c_Polynomial_Odegree(tc_Complex_Ocomplex,B_q)=c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p)|(~hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,B_q),sK23_skl(B_q))=hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,v_z,sK23_skl(B_q)))|v_thesis____))),
% 72.25/9.70 inference(skolemize,[status(esa),new_symbols(skolem,[sK23_skl]),skolemize(B_x,sK23_skl(B_q))],[f4820])).
% 72.25/9.70 fof(f4822,plain,(
% 72.25/9.70 ![X0]: (~c_Polynomial_Odegree(tc_Complex_Ocomplex,X0)=c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p)|~hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,X0),sK23_skl(X0))=hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,v_z,sK23_skl(X0)))|v_thesis____)),
% 72.25/9.70 inference(cnf_transformation,[status(thm)],[f4821])).
% 72.25/9.70 fof(f4823,plain,(
% 72.25/9.70 ~v_thesis____),
% 72.25/9.70 inference(cnf_transformation,[status(thm)],[f1265])).
% 72.25/9.70 fof(f5061,plain,(
% 72.25/9.70 ![X0,X1]: (c_Polynomial_Odegree(tc_Complex_Ocomplex,c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(tc_Complex_Ocomplex,X0,X1))=c_Polynomial_Odegree(tc_Complex_Ocomplex,X0))),
% 72.25/9.70 inference(resolution,[status(thm)],[f4681,f1313])).
% 72.25/9.70 fof(f5062,plain,(
% 72.25/9.70 ![X0,X1,X2]: (hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(tc_Complex_Ocomplex,X0,X1)),X2)=hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,X0),c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex,X1,X2)))),
% 72.25/9.70 inference(resolution,[status(thm)],[f4681,f1274])).
% 72.25/9.70 fof(f5064,plain,(
% 72.25/9.70 ![X0,X1,X2]: (hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(tc_Complex_Ocomplex,X0,X1)),X2)=hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,sK1_skl(X0,X1)),X2))),
% 72.25/9.70 inference(forward_demodulation,[status(thm)],[f1331,f5062])).
% 72.25/9.70 fof(f85297,plain,(
% 72.25/9.70 ![X0]: (~c_Polynomial_Odegree(tc_Complex_Ocomplex,X0)=c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p)|~hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,X0),sK23_skl(X0))=hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,sK1_skl(v_p,v_z)),sK23_skl(X0))|v_thesis____)),
% 72.25/9.70 inference(forward_demodulation,[status(thm)],[f1331,f4822])).
% 72.25/9.70 fof(f85298,plain,(
% 72.25/9.70 ![X0]: (~c_Polynomial_Odegree(tc_Complex_Ocomplex,X0)=c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p)|~hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,X0),sK23_skl(X0))=hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,sK1_skl(v_p,v_z)),sK23_skl(X0)))),
% 72.25/9.70 inference(forward_subsumption_resolution,[status(thm)],[f85297,f4823])).
% 72.25/9.70 fof(f110780,plain,(
% 72.25/9.70 ~c_Polynomial_Odegree(tc_Complex_Ocomplex,c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(tc_Complex_Ocomplex,v_p,v_z))=c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p)),
% 72.25/9.70 inference(resolution,[status(thm)],[f5064,f85298])).
% 72.25/9.70 fof(f110807,plain,(
% 72.25/9.70 ~c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p)=c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p)),
% 72.25/9.70 inference(forward_demodulation,[status(thm)],[f5061,f110780])).
% 72.25/9.70 fof(f110808,plain,(
% 72.25/9.70 $false),
% 72.25/9.70 inference(trivial_equality_resolution,[status(thm)],[f110807])).
% 72.25/9.70 % SZS output end CNFRefutation for theBenchmark.p
% 3.18/9.83 % Elapsed time: 9.458704 seconds
% 3.18/9.83 % CPU time: 73.330920 seconds
% 3.18/9.83 % Total memory used: 650.756 MB
% 3.18/9.83 % Net memory used: 622.892 MB
%------------------------------------------------------------------------------