%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : ALG367-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 : n009.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:05 AM UTC 2026
% Result : Unsatisfiable 248.06s 36.83s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG367-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.13/5.38 % Computer : n009.cluster.edu
% 0.13/5.38 % Model : x86_64 x86_64
% 0.13/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/5.38 % Memory : 8046.5625MB
% 0.13/5.38 % OS : Linux 6.8.0-71-generic
% 0.13/5.38 % CPULimit : 300
% 0.13/5.38 % WCLimit : 300
% 0.13/5.38 % DateTime : Mon Sep 21 13:18:03 UTC 2026
% 0.13/5.38 % CPUTime :
% 0.16/5.45 % Drodi V4.1.1
% 248.06/36.83 % Refutation found
% 248.06/36.83 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 248.06/36.83 % SZS output start CNFRefutation for theBenchmark
% 248.06/36.83 fof(f698,axiom,(
% 248.06/36.83 (![V_a,V_p,V_q]: (c_Polynomial_Opoly(v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xpoly__offset__1(V_a,V_p),V_q,tc_Complex_Ocomplex) = c_Polynomial_Opoly(V_p,c_HOL_Oplus__class_Oplus(V_a,V_q,tc_Complex_Ocomplex),tc_Complex_Ocomplex) ))),
% 248.06/36.83 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 248.06/36.83 fof(f706,axiom,(
% 248.06/36.83 (![T_a,V_x,V_y]: (( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a)| c_HOL_Oplus__class_Oplus(V_x,V_y,T_a) = c_HOL_Oplus__class_Oplus(V_y,V_x,T_a) ) ))),
% 248.06/36.83 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 248.06/36.83 fof(f747,axiom,(
% 248.06/36.83 (![T_a,V_p,V_h,V_x]: (( ~ class_Ring__and__Field_Ocomm__semiring__0(T_a)| c_Polynomial_Opoly(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(V_p,V_h,T_a),V_x,T_a) = c_Polynomial_Opoly(V_p,c_HOL_Oplus__class_Oplus(V_h,V_x,T_a),T_a) ) ))),
% 248.06/36.83 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 248.06/36.83 fof(f748,axiom,(
% 248.06/36.83 (![T_a,V_p,V_h]: (( ~ class_Ring__and__Field_Ocomm__semiring__0(T_a)| c_Polynomial_Odegree(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(V_p,V_h,T_a),T_a) = c_Polynomial_Odegree(V_p,T_a) ) ))),
% 248.06/36.83 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 248.06/36.83 fof(f786,negated_conjecture,(
% 248.06/36.83 ~ v_thesis____ ),
% 248.06/36.83 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 248.06/36.83 fof(f787,negated_conjecture,(
% 248.06/36.83 (![V_qa]: (( c_Polynomial_Opoly(V_qa,v_q(V_qa),tc_Complex_Ocomplex) != c_Polynomial_Opoly(v_p,c_HOL_Oplus__class_Oplus(v_z,v_q(V_qa),tc_Complex_Ocomplex),tc_Complex_Ocomplex)| c_Polynomial_Odegree(V_qa,tc_Complex_Ocomplex) != c_Polynomial_Odegree(v_p,tc_Complex_Ocomplex)| v_thesis____ ) ))),
% 248.06/36.83 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 248.06/36.83 fof(f894,axiom,(
% 248.06/36.83 class_Ring__and__Field_Ocomm__semiring__1(tc_Complex_Ocomplex) ),
% 248.06/36.83 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 248.06/36.83 fof(f895,axiom,(
% 248.06/36.83 class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex) ),
% 248.06/36.83 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 248.06/36.83 fof(f2148,plain,(
% 248.06/36.83 ![X0,X1,X2]: (c_Polynomial_Opoly(v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xpoly__offset__1(X0,X1),X2,tc_Complex_Ocomplex)=c_Polynomial_Opoly(X1,c_HOL_Oplus__class_Oplus(X0,X2,tc_Complex_Ocomplex),tc_Complex_Ocomplex))),
% 248.06/36.83 inference(cnf_transformation,[status(thm)],[f698])).
% 248.06/36.83 fof(f2162,plain,(
% 248.06/36.83 ![T_a]: (~class_Ring__and__Field_Ocomm__semiring__1(T_a)|(![V_x,V_y]: c_HOL_Oplus__class_Oplus(V_x,V_y,T_a)=c_HOL_Oplus__class_Oplus(V_y,V_x,T_a)))),
% 248.06/36.83 inference(miniscoping,[status(thm)],[f706])).
% 248.06/36.83 fof(f2163,plain,(
% 248.06/36.83 ![X0,X1,X2]: (~class_Ring__and__Field_Ocomm__semiring__1(X0)|c_HOL_Oplus__class_Oplus(X1,X2,X0)=c_HOL_Oplus__class_Oplus(X2,X1,X0))),
% 248.06/36.83 inference(cnf_transformation,[status(thm)],[f2162])).
% 248.06/36.83 fof(f2242,plain,(
% 248.06/36.83 ![T_a]: (~class_Ring__and__Field_Ocomm__semiring__0(T_a)|(![V_p,V_h,V_x]: c_Polynomial_Opoly(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(V_p,V_h,T_a),V_x,T_a)=c_Polynomial_Opoly(V_p,c_HOL_Oplus__class_Oplus(V_h,V_x,T_a),T_a)))),
% 248.06/36.83 inference(miniscoping,[status(thm)],[f747])).
% 248.06/36.83 fof(f2243,plain,(
% 248.06/36.83 ![X0,X1,X2,X3]: (~class_Ring__and__Field_Ocomm__semiring__0(X0)|c_Polynomial_Opoly(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(X1,X2,X0),X3,X0)=c_Polynomial_Opoly(X1,c_HOL_Oplus__class_Oplus(X2,X3,X0),X0))),
% 248.06/36.83 inference(cnf_transformation,[status(thm)],[f2242])).
% 248.06/36.83 fof(f2244,plain,(
% 248.06/36.83 ![T_a]: (~class_Ring__and__Field_Ocomm__semiring__0(T_a)|(![V_p,V_h]: c_Polynomial_Odegree(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(V_p,V_h,T_a),T_a)=c_Polynomial_Odegree(V_p,T_a)))),
% 248.06/36.83 inference(miniscoping,[status(thm)],[f748])).
% 248.06/36.83 fof(f2245,plain,(
% 248.06/36.83 ![X0,X1,X2]: (~class_Ring__and__Field_Ocomm__semiring__0(X0)|c_Polynomial_Odegree(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(X1,X2,X0),X0)=c_Polynomial_Odegree(X1,X0))),
% 248.06/36.83 inference(cnf_transformation,[status(thm)],[f2244])).
% 248.06/36.83 fof(f2319,plain,(
% 248.06/36.83 ~v_thesis____),
% 248.06/36.83 inference(cnf_transformation,[status(thm)],[f786])).
% 248.06/36.83 fof(f2320,plain,(
% 248.06/36.83 (![V_qa]: (~c_Polynomial_Opoly(V_qa,v_q(V_qa),tc_Complex_Ocomplex)=c_Polynomial_Opoly(v_p,c_HOL_Oplus__class_Oplus(v_z,v_q(V_qa),tc_Complex_Ocomplex),tc_Complex_Ocomplex)|~c_Polynomial_Odegree(V_qa,tc_Complex_Ocomplex)=c_Polynomial_Odegree(v_p,tc_Complex_Ocomplex)))|v_thesis____),
% 248.06/36.83 inference(miniscoping,[status(thm)],[f787])).
% 248.06/36.83 fof(f2321,plain,(
% 248.06/36.83 ![X0]: (~c_Polynomial_Opoly(X0,v_q(X0),tc_Complex_Ocomplex)=c_Polynomial_Opoly(v_p,c_HOL_Oplus__class_Oplus(v_z,v_q(X0),tc_Complex_Ocomplex),tc_Complex_Ocomplex)|~c_Polynomial_Odegree(X0,tc_Complex_Ocomplex)=c_Polynomial_Odegree(v_p,tc_Complex_Ocomplex)|v_thesis____)),
% 248.06/36.83 inference(cnf_transformation,[status(thm)],[f2320])).
% 248.06/36.83 fof(f2428,plain,(
% 248.06/36.83 class_Ring__and__Field_Ocomm__semiring__1(tc_Complex_Ocomplex)),
% 248.06/36.83 inference(cnf_transformation,[status(thm)],[f894])).
% 248.06/36.83 fof(f2429,plain,(
% 248.06/36.83 class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex)),
% 248.06/36.83 inference(cnf_transformation,[status(thm)],[f895])).
% 248.06/36.83 fof(f2503,definition,(
% 248.06/36.83 sQ1_spl <=> (v_thesis____)),
% 248.06/36.83 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 248.06/36.83 fof(f2504,plain,(
% 248.06/36.83 v_thesis____|~sQ1_spl),
% 248.06/36.83 inference(component_clause,[status(thm)],[f2503])).
% 248.06/36.83 fof(f2507,definition,(
% 248.06/36.83 ![X0]: (sQ2_spl <=> (~c_Polynomial_Opoly(X0,v_q(X0),tc_Complex_Ocomplex)=c_Polynomial_Opoly(v_p,c_HOL_Oplus__class_Oplus(v_z,v_q(X0),tc_Complex_Ocomplex),tc_Complex_Ocomplex)|~c_Polynomial_Odegree(X0,tc_Complex_Ocomplex)=c_Polynomial_Odegree(v_p,tc_Complex_Ocomplex)))),
% 248.06/36.83 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 248.06/36.83 fof(f2508,plain,(
% 248.06/36.83 ![X0]: (~c_Polynomial_Opoly(X0,v_q(X0),tc_Complex_Ocomplex)=c_Polynomial_Opoly(v_p,c_HOL_Oplus__class_Oplus(v_z,v_q(X0),tc_Complex_Ocomplex),tc_Complex_Ocomplex)|~c_Polynomial_Odegree(X0,tc_Complex_Ocomplex)=c_Polynomial_Odegree(v_p,tc_Complex_Ocomplex)|~sQ2_spl)),
% 248.06/36.83 inference(component_clause,[status(thm)],[f2507])).
% 248.06/36.83 fof(f2510,plain,(
% 248.06/36.83 sQ2_spl|sQ1_spl),
% 248.06/36.83 inference(split_clause,[status(thm)],[f2321,f2507,f2503])).
% 248.06/36.83 fof(f2512,plain,(
% 248.06/36.83 $false|~sQ1_spl),
% 248.06/36.83 inference(forward_subsumption_resolution,[status(thm)],[f2504,f2319])).
% 248.06/36.83 fof(f2513,plain,(
% 248.06/36.83 ~sQ1_spl),
% 248.06/36.83 inference(contradiction_clause,[status(thm)],[f2512])).
% 248.06/36.83 fof(f2592,plain,(
% 248.06/36.83 ![X0]: (~c_Polynomial_Opoly(X0,v_q(X0),tc_Complex_Ocomplex)=c_Polynomial_Opoly(v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xpoly__offset__1(v_z,v_p),v_q(X0),tc_Complex_Ocomplex)|~c_Polynomial_Odegree(X0,tc_Complex_Ocomplex)=c_Polynomial_Odegree(v_p,tc_Complex_Ocomplex)|~sQ2_spl)),
% 248.06/36.83 inference(backward_demodulation,[status(thm)],[f2148,f2508])).
% 248.06/36.83 fof(f3772,plain,(
% 248.06/36.83 ![X0,X1]: (c_HOL_Oplus__class_Oplus(X0,X1,tc_Complex_Ocomplex)=c_HOL_Oplus__class_Oplus(X1,X0,tc_Complex_Ocomplex))),
% 248.06/36.83 inference(resolution,[status(thm)],[f2428,f2163])).
% 248.06/36.83 fof(f3852,plain,(
% 248.06/36.83 ![X0,X1,X2]: (c_Polynomial_Opoly(v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xpoly__offset__1(X0,X1),X2,tc_Complex_Ocomplex)=c_Polynomial_Opoly(X1,c_HOL_Oplus__class_Oplus(X2,X0,tc_Complex_Ocomplex),tc_Complex_Ocomplex))),
% 248.06/36.83 inference(paramodulation,[status(thm)],[f3772,f2148])).
% 248.06/36.83 fof(f4062,plain,(
% 248.06/36.83 ![X0,X1,X2]: (c_Polynomial_Opoly(v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xpoly__offset__1(X0,X1),X2,tc_Complex_Ocomplex)=c_Polynomial_Opoly(v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xpoly__offset__1(X2,X1),X0,tc_Complex_Ocomplex))),
% 248.06/36.83 inference(paramodulation,[status(thm)],[f2148,f3852])).
% 248.06/36.83 fof(f120777,plain,(
% 248.06/36.83 ![X0,X1]: (c_Polynomial_Odegree(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(X0,X1,tc_Complex_Ocomplex),tc_Complex_Ocomplex)=c_Polynomial_Odegree(X0,tc_Complex_Ocomplex))),
% 248.06/36.83 inference(resolution,[status(thm)],[f2429,f2245])).
% 248.06/36.83 fof(f120778,plain,(
% 248.06/36.83 ![X0,X1,X2]: (c_Polynomial_Opoly(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(X0,X1,tc_Complex_Ocomplex),X2,tc_Complex_Ocomplex)=c_Polynomial_Opoly(X0,c_HOL_Oplus__class_Oplus(X1,X2,tc_Complex_Ocomplex),tc_Complex_Ocomplex))),
% 248.06/36.83 inference(resolution,[status(thm)],[f2429,f2243])).
% 248.06/36.83 fof(f120782,plain,(
% 248.06/36.83 ![X0,X1,X2]: (c_Polynomial_Opoly(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(X0,X1,tc_Complex_Ocomplex),X2,tc_Complex_Ocomplex)=c_Polynomial_Opoly(v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xpoly__offset__1(X2,X0),X1,tc_Complex_Ocomplex))),
% 179.13/37.01 inference(forward_demodulation,[status(thm)],[f3852,f120778])).
% 179.13/37.01 fof(f120938,plain,(
% 179.13/37.01 ![X0,X1]: (~c_Polynomial_Opoly(v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xpoly__offset__1(v_q(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(X0,X1,tc_Complex_Ocomplex)),X0),X1,tc_Complex_Ocomplex)=c_Polynomial_Opoly(v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xpoly__offset__1(v_z,v_p),v_q(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(X0,X1,tc_Complex_Ocomplex)),tc_Complex_Ocomplex)|~c_Polynomial_Odegree(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(X0,X1,tc_Complex_Ocomplex),tc_Complex_Ocomplex)=c_Polynomial_Odegree(v_p,tc_Complex_Ocomplex)|~sQ2_spl)),
% 179.13/37.01 inference(paramodulation,[status(thm)],[f120782,f2592])).
% 179.13/37.01 fof(f120943,plain,(
% 179.13/37.01 ![X0,X1]: (~c_Polynomial_Opoly(v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xpoly__offset__1(v_q(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(X0,X1,tc_Complex_Ocomplex)),X0),X1,tc_Complex_Ocomplex)=c_Polynomial_Opoly(v_sko__Fundamental__Theorem__Algebra__Mirabelle__Xpoly__offset__1(v_z,v_p),v_q(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(X0,X1,tc_Complex_Ocomplex)),tc_Complex_Ocomplex)|~c_Polynomial_Odegree(X0,tc_Complex_Ocomplex)=c_Polynomial_Odegree(v_p,tc_Complex_Ocomplex)|~sQ2_spl)),
% 179.13/37.01 inference(forward_demodulation,[status(thm)],[f120777,f120938])).
% 179.13/37.01 fof(f123794,plain,(
% 179.13/37.01 ~c_Polynomial_Odegree(v_p,tc_Complex_Ocomplex)=c_Polynomial_Odegree(v_p,tc_Complex_Ocomplex)|~sQ2_spl),
% 179.13/37.01 inference(resolution,[status(thm)],[f120943,f4062])).
% 179.13/37.01 fof(f123842,plain,(
% 179.13/37.01 $false|~sQ2_spl),
% 179.13/37.01 inference(trivial_equality_resolution,[status(thm)],[f123794])).
% 179.13/37.01 fof(f123843,plain,(
% 179.13/37.01 ~sQ2_spl),
% 179.13/37.01 inference(contradiction_clause,[status(thm)],[f123842])).
% 179.13/37.01 fof(f123844,plain,(
% 179.13/37.01 $false),
% 179.13/37.01 inference(sat_refutation,[status(thm)],[f2510,f2513,f123843])).
% 179.13/37.01 % SZS output end CNFRefutation for theBenchmark.p
% 46.78/37.10 % Elapsed time: 31.692896 seconds
% 46.78/37.10 % CPU time: 250.387044 seconds
% 46.78/37.10 % Total memory used: 2.854 GB
% 46.78/37.10 % Net memory used: 2.699 GB
%------------------------------------------------------------------------------