%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW182+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/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:46 PM UTC 2026
% Result : Theorem 0.43s 1.17s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWW182+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.43 % Computer : n011.cluster.edu
% 0.17/0.43 % Model : x86_64 x86_64
% 0.17/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.43 % Memory : 8046.5625MB
% 0.17/0.43 % OS : Linux 6.8.0-71-generic
% 0.17/0.43 % CPULimit : 300
% 0.17/0.43 % WCLimit : 300
% 0.17/0.43 % DateTime : Mon Sep 21 09:40:10 UTC 2026
% 0.17/0.43 % CPUTime :
% 0.26/0.58 % Drodi V4.1.1
% 0.43/1.17 % Refutation found
% 0.43/1.17 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.43/1.17 % SZS output start CNFRefutation for theBenchmark
% 0.43/1.17 fof(f2,axiom,(
% 0.43/1.17 (! [V_h,T_a] :( class_Rings_Ocomm__semiring__0(T_a)=> c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(T_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)),V_h) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)) ) )),
% 0.43/1.17 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.43/1.17 fof(f17,axiom,(
% 0.43/1.17 (! [V_a,T_a] :( class_Groups_Ozero(T_a)=> c_Polynomial_Omonom(T_a,V_a,c_Groups_Ozero__class_Ozero(tc_Nat_Onat)) = c_Polynomial_OpCons(T_a,V_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))) ) )),
% 0.43/1.17 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.43/1.17 fof(f38,axiom,(
% 0.43/1.17 (! [V_a,T_a] :( class_Rings_Ocomm__semiring__0(T_a)=> c_Polynomial_Osmult(T_a,V_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)) ) )),
% 0.43/1.17 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.43/1.17 fof(f68,axiom,(
% 0.43/1.17 (! [V_a,T_a] :( class_Groups_Ocomm__monoid__add(T_a)=> c_Groups_Oplus__class_Oplus(T_a,c_Groups_Ozero__class_Ozero(T_a),V_a) = V_a ) )),
% 0.43/1.17 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.43/1.17 fof(f77,axiom,(
% 0.43/1.17 (! [V_h,V_p,V_a,T_a] :( class_Rings_Ocomm__semiring__0(T_a)=> c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(T_a,c_Polynomial_OpCons(T_a,V_a,V_p),V_h) = c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(T_a),c_Polynomial_Osmult(T_a,V_h,c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(T_a,V_p,V_h)),c_Polynomial_OpCons(T_a,V_a,c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(T_a,V_p,V_h))) ) )),
% 0.43/1.17 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.43/1.17 fof(f378,axiom,(
% 0.43/1.17 c_HOL_Obool_Obool__size(c_fFalse) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat) ),
% 0.43/1.17 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.43/1.17 fof(f998,axiom,(
% 0.43/1.17 (! [T] :( class_Rings_Ocomm__semiring__0(T)=> class_Groups_Ocomm__monoid__add(T) ) )),
% 0.43/1.17 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.43/1.17 fof(f1004,axiom,(
% 0.43/1.17 (! [T] :( class_Rings_Ocomm__semiring__0(T)=> class_Groups_Ozero(T) ) )),
% 0.43/1.17 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.43/1.17 fof(f1147,axiom,(
% 0.43/1.17 (! [T_1] :( class_Rings_Ocomm__semiring__0(T_1)=> class_Rings_Ocomm__semiring__0(tc_Polynomial_Opoly(T_1)) ) )),
% 0.43/1.17 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.43/1.17 fof(f1180,conjecture,(
% 0.43/1.17 c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,c_Polynomial_OpCons(t_a,v_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),v_h) = c_Polynomial_OpCons(t_a,v_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))) ),
% 0.43/1.17 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.43/1.17 fof(f1181,negated_conjecture,(
% 0.43/1.17 ~(c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,c_Polynomial_OpCons(t_a,v_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),v_h) = c_Polynomial_OpCons(t_a,v_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))) )),
% 0.43/1.17 inference(negated_conjecture,[status(cth)],[f1180])).
% 0.43/1.17 fof(f1182,hypothesis,(
% 0.43/1.17 class_Rings_Ocomm__semiring__0(t_a) ),
% 0.43/1.17 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.43/1.17 fof(f1186,plain,(
% 0.43/1.17 ![V_h,T_a]: (~class_Rings_Ocomm__semiring__0(T_a)|c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(T_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)),V_h)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)))),
% 0.43/1.17 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.43/1.17 fof(f1187,plain,(
% 0.43/1.17 ![T_a]: (~class_Rings_Ocomm__semiring__0(T_a)|(![V_h]: c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(T_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)),V_h)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))))),
% 0.43/1.17 inference(miniscoping,[status(thm)],[f1186])).
% 0.43/1.17 fof(f1188,plain,(
% 0.43/1.17 ![X0,X1]: (~class_Rings_Ocomm__semiring__0(X0)|c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)),X1)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)))),
% 0.43/1.17 inference(cnf_transformation,[status(thm)],[f1187])).
% 0.43/1.17 fof(f1253,plain,(
% 0.43/1.17 ![V_a,T_a]: (~class_Groups_Ozero(T_a)|c_Polynomial_Omonom(T_a,V_a,c_Groups_Ozero__class_Ozero(tc_Nat_Onat))=c_Polynomial_OpCons(T_a,V_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))))),
% 0.43/1.17 inference(pre_NNF_transformation,[status(thm)],[f17])).
% 0.43/1.17 fof(f1254,plain,(
% 0.43/1.17 ![T_a]: (~class_Groups_Ozero(T_a)|(![V_a]: c_Polynomial_Omonom(T_a,V_a,c_Groups_Ozero__class_Ozero(tc_Nat_Onat))=c_Polynomial_OpCons(T_a,V_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)))))),
% 0.43/1.17 inference(miniscoping,[status(thm)],[f1253])).
% 0.43/1.17 fof(f1255,plain,(
% 0.43/1.17 ![X0,X1]: (~class_Groups_Ozero(X0)|c_Polynomial_Omonom(X0,X1,c_Groups_Ozero__class_Ozero(tc_Nat_Onat))=c_Polynomial_OpCons(X0,X1,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X0))))),
% 0.43/1.17 inference(cnf_transformation,[status(thm)],[f1254])).
% 0.43/1.17 fof(f1328,plain,(
% 0.43/1.17 ![V_a,T_a]: (~class_Rings_Ocomm__semiring__0(T_a)|c_Polynomial_Osmult(T_a,V_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)))=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)))),
% 0.43/1.17 inference(pre_NNF_transformation,[status(thm)],[f38])).
% 0.43/1.17 fof(f1329,plain,(
% 0.43/1.17 ![T_a]: (~class_Rings_Ocomm__semiring__0(T_a)|(![V_a]: c_Polynomial_Osmult(T_a,V_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)))=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))))),
% 0.43/1.17 inference(miniscoping,[status(thm)],[f1328])).
% 0.43/1.17 fof(f1330,plain,(
% 0.43/1.17 ![X0,X1]: (~class_Rings_Ocomm__semiring__0(X0)|c_Polynomial_Osmult(X0,X1,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)))=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)))),
% 0.43/1.17 inference(cnf_transformation,[status(thm)],[f1329])).
% 0.43/1.17 fof(f1414,plain,(
% 0.43/1.17 ![V_a,T_a]: (~class_Groups_Ocomm__monoid__add(T_a)|c_Groups_Oplus__class_Oplus(T_a,c_Groups_Ozero__class_Ozero(T_a),V_a)=V_a)),
% 0.43/1.17 inference(pre_NNF_transformation,[status(thm)],[f68])).
% 0.43/1.17 fof(f1415,plain,(
% 0.43/1.17 ![T_a]: (~class_Groups_Ocomm__monoid__add(T_a)|(![V_a]: c_Groups_Oplus__class_Oplus(T_a,c_Groups_Ozero__class_Ozero(T_a),V_a)=V_a))),
% 0.43/1.17 inference(miniscoping,[status(thm)],[f1414])).
% 0.43/1.17 fof(f1416,plain,(
% 0.43/1.17 ![X0,X1]: (~class_Groups_Ocomm__monoid__add(X0)|c_Groups_Oplus__class_Oplus(X0,c_Groups_Ozero__class_Ozero(X0),X1)=X1)),
% 0.43/1.17 inference(cnf_transformation,[status(thm)],[f1415])).
% 0.43/1.17 fof(f1437,plain,(
% 0.43/1.17 ![V_h,V_p,V_a,T_a]: (~class_Rings_Ocomm__semiring__0(T_a)|c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(T_a,c_Polynomial_OpCons(T_a,V_a,V_p),V_h)=c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(T_a),c_Polynomial_Osmult(T_a,V_h,c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(T_a,V_p,V_h)),c_Polynomial_OpCons(T_a,V_a,c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(T_a,V_p,V_h))))),
% 0.43/1.17 inference(pre_NNF_transformation,[status(thm)],[f77])).
% 0.43/1.17 fof(f1438,plain,(
% 0.43/1.17 ![T_a]: (~class_Rings_Ocomm__semiring__0(T_a)|(![V_h,V_p,V_a]: c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(T_a,c_Polynomial_OpCons(T_a,V_a,V_p),V_h)=c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(T_a),c_Polynomial_Osmult(T_a,V_h,c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(T_a,V_p,V_h)),c_Polynomial_OpCons(T_a,V_a,c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(T_a,V_p,V_h)))))),
% 0.43/1.17 inference(miniscoping,[status(thm)],[f1437])).
% 0.43/1.17 fof(f1439,plain,(
% 0.43/1.17 ![X0,X1,X2,X3]: (~class_Rings_Ocomm__semiring__0(X0)|c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(X0,c_Polynomial_OpCons(X0,X1,X2),X3)=c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(X0),c_Polynomial_Osmult(X0,X3,c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(X0,X2,X3)),c_Polynomial_OpCons(X0,X1,c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(X0,X2,X3))))),
% 0.43/1.17 inference(cnf_transformation,[status(thm)],[f1438])).
% 0.43/1.17 fof(f2406,plain,(
% 0.43/1.17 c_HOL_Obool_Obool__size(c_fFalse)=c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
% 0.43/1.17 inference(cnf_transformation,[status(thm)],[f378])).
% 0.43/1.17 fof(f4413,plain,(
% 0.43/1.17 ![T]: (~class_Rings_Ocomm__semiring__0(T)|class_Groups_Ocomm__monoid__add(T))),
% 0.43/1.17 inference(pre_NNF_transformation,[status(thm)],[f998])).
% 0.43/1.17 fof(f4414,plain,(
% 0.43/1.17 ![X0]: (~class_Rings_Ocomm__semiring__0(X0)|class_Groups_Ocomm__monoid__add(X0))),
% 0.43/1.17 inference(cnf_transformation,[status(thm)],[f4413])).
% 0.43/1.17 fof(f4425,plain,(
% 0.43/1.17 ![T]: (~class_Rings_Ocomm__semiring__0(T)|class_Groups_Ozero(T))),
% 0.43/1.17 inference(pre_NNF_transformation,[status(thm)],[f1004])).
% 0.43/1.17 fof(f4426,plain,(
% 0.43/1.17 ![X0]: (~class_Rings_Ocomm__semiring__0(X0)|class_Groups_Ozero(X0))),
% 0.43/1.17 inference(cnf_transformation,[status(thm)],[f4425])).
% 0.43/1.17 fof(f4611,plain,(
% 0.43/1.17 ![T_1]: (~class_Rings_Ocomm__semiring__0(T_1)|class_Rings_Ocomm__semiring__0(tc_Polynomial_Opoly(T_1)))),
% 0.43/1.17 inference(pre_NNF_transformation,[status(thm)],[f1147])).
% 0.43/1.17 fof(f4612,plain,(
% 0.43/1.17 ![X0]: (~class_Rings_Ocomm__semiring__0(X0)|class_Rings_Ocomm__semiring__0(tc_Polynomial_Opoly(X0)))),
% 0.43/1.17 inference(cnf_transformation,[status(thm)],[f4611])).
% 0.43/1.17 fof(f4673,plain,(
% 0.43/1.17 ~c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,c_Polynomial_OpCons(t_a,v_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),v_h)=c_Polynomial_OpCons(t_a,v_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))),
% 0.43/1.17 inference(cnf_transformation,[status(thm)],[f1181])).
% 0.43/1.17 fof(f4674,plain,(
% 0.43/1.17 class_Rings_Ocomm__semiring__0(t_a)),
% 0.43/1.17 inference(cnf_transformation,[status(thm)],[f1182])).
% 0.43/1.17 fof(f4867,plain,(
% 0.43/1.17 ![X0]: (c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)),X0)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))),
% 0.43/1.17 inference(resolution,[status(thm)],[f1188,f4674])).
% 0.43/1.17 fof(f4868,plain,(
% 0.43/1.17 ![X0,X1,X2]: (c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,c_Polynomial_OpCons(t_a,X0,X1),X2)=c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(t_a),c_Polynomial_Osmult(t_a,X2,c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,X1,X2)),c_Polynomial_OpCons(t_a,X0,c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,X1,X2))))),
% 0.43/1.17 inference(resolution,[status(thm)],[f1439,f4674])).
% 0.43/1.17 fof(f4869,plain,(
% 0.43/1.17 ![X0,X1]: (c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,c_Polynomial_OpCons(t_a,X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),X1)=c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(t_a),c_Polynomial_Osmult(t_a,X1,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Polynomial_OpCons(t_a,X0,c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)),X1))))),
% 0.43/1.17 inference(paramodulation,[status(thm)],[f4867,f4868])).
% 0.43/1.17 fof(f4871,plain,(
% 0.43/1.17 ![X0,X1]: (c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,c_Polynomial_OpCons(t_a,X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),X1)=c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(t_a),c_Polynomial_Osmult(t_a,X1,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Polynomial_OpCons(t_a,X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))))),
% 0.43/1.17 inference(forward_demodulation,[status(thm)],[f4867,f4869])).
% 0.43/1.17 fof(f5133,plain,(
% 0.43/1.17 class_Groups_Ozero(t_a)),
% 0.43/1.17 inference(resolution,[status(thm)],[f4426,f4674])).
% 0.43/1.17 fof(f5139,plain,(
% 0.43/1.17 ![X0]: (c_Polynomial_Osmult(t_a,X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))),
% 0.43/1.17 inference(resolution,[status(thm)],[f1330,f4674])).
% 0.43/1.17 fof(f5151,plain,(
% 0.43/1.17 ![X0]: (c_Polynomial_Omonom(t_a,X0,c_Groups_Ozero__class_Ozero(tc_Nat_Onat))=c_Polynomial_OpCons(t_a,X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))))),
% 0.43/1.17 inference(resolution,[status(thm)],[f5133,f1255])).
% 0.43/1.17 fof(f5197,plain,(
% 0.43/1.17 ![X0,X1]: (c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,c_Polynomial_OpCons(t_a,X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),X1)=c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(t_a),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)),c_Polynomial_OpCons(t_a,X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))))),
% 0.43/1.17 inference(backward_demodulation,[status(thm)],[f5139,f4871])).
% 0.43/1.17 fof(f5284,plain,(
% 0.43/1.17 ~c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,c_Polynomial_OpCons(t_a,v_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),v_h)=c_Polynomial_Omonom(t_a,v_a,c_Groups_Ozero__class_Ozero(tc_Nat_Onat))),
% 0.43/1.17 inference(backward_demodulation,[status(thm)],[f5151,f4673])).
% 0.43/1.17 fof(f5296,plain,(
% 0.43/1.17 ~c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,c_Polynomial_Omonom(t_a,v_a,c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),v_h)=c_Polynomial_Omonom(t_a,v_a,c_Groups_Ozero__class_Ozero(tc_Nat_Onat))),
% 0.43/1.20 inference(forward_demodulation,[status(thm)],[f5151,f5284])).
% 0.43/1.20 fof(f5507,plain,(
% 0.43/1.20 ~c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,c_Polynomial_Omonom(t_a,v_a,c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),v_h)=c_Polynomial_Omonom(t_a,v_a,c_HOL_Obool_Obool__size(c_fFalse))),
% 0.43/1.20 inference(backward_demodulation,[status(thm)],[f2406,f5296])).
% 0.43/1.20 fof(f5508,plain,(
% 0.43/1.20 ![X0]: (c_Polynomial_Omonom(t_a,X0,c_HOL_Obool_Obool__size(c_fFalse))=c_Polynomial_OpCons(t_a,X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))))),
% 0.43/1.20 inference(backward_demodulation,[status(thm)],[f2406,f5151])).
% 0.43/1.20 fof(f5514,plain,(
% 0.43/1.20 ~c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,c_Polynomial_Omonom(t_a,v_a,c_HOL_Obool_Obool__size(c_fFalse)),v_h)=c_Polynomial_Omonom(t_a,v_a,c_HOL_Obool_Obool__size(c_fFalse))),
% 0.43/1.20 inference(forward_demodulation,[status(thm)],[f2406,f5507])).
% 0.43/1.21 fof(f5821,plain,(
% 0.43/1.21 ![X0,X1]: (c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,c_Polynomial_Omonom(t_a,X0,c_HOL_Obool_Obool__size(c_fFalse)),X1)=c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(t_a),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)),c_Polynomial_OpCons(t_a,X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))))),
% 0.43/1.21 inference(forward_demodulation,[status(thm)],[f5508,f5197])).
% 0.43/1.21 fof(f5822,plain,(
% 0.43/1.21 ![X0,X1]: (c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,c_Polynomial_Omonom(t_a,X0,c_HOL_Obool_Obool__size(c_fFalse)),X1)=c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(t_a),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)),c_Polynomial_Omonom(t_a,X0,c_HOL_Obool_Obool__size(c_fFalse))))),
% 0.43/1.21 inference(forward_demodulation,[status(thm)],[f5508,f5821])).
% 0.43/1.21 fof(f5825,plain,(
% 0.43/1.21 ![X0,X1,X2]: (c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,c_Polynomial_Omonom(t_a,X0,c_HOL_Obool_Obool__size(c_fFalse)),X1)=c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,c_Polynomial_Omonom(t_a,X0,c_HOL_Obool_Obool__size(c_fFalse)),X2))),
% 0.43/1.21 inference(paramodulation,[status(thm)],[f5822,f5822])).
% 0.43/1.21 fof(f5844,plain,(
% 0.43/1.21 ![X0]: (~c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,c_Polynomial_Omonom(t_a,v_a,c_HOL_Obool_Obool__size(c_fFalse)),X0)=c_Polynomial_Omonom(t_a,v_a,c_HOL_Obool_Obool__size(c_fFalse)))),
% 0.43/1.21 inference(paramodulation,[status(thm)],[f5825,f5514])).
% 0.43/1.21 fof(f5860,plain,(
% 0.43/1.21 ~c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(t_a),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)),c_Polynomial_Omonom(t_a,v_a,c_HOL_Obool_Obool__size(c_fFalse)))=c_Polynomial_Omonom(t_a,v_a,c_HOL_Obool_Obool__size(c_fFalse))),
% 0.43/1.21 inference(paramodulation,[status(thm)],[f5822,f5844])).
% 0.43/1.21 fof(f6575,plain,(
% 0.43/1.21 class_Rings_Ocomm__semiring__0(tc_Polynomial_Opoly(t_a))),
% 0.43/1.21 inference(resolution,[status(thm)],[f4612,f4674])).
% 0.43/1.21 fof(f6641,plain,(
% 0.43/1.21 class_Groups_Ocomm__monoid__add(tc_Polynomial_Opoly(t_a))),
% 0.43/1.21 inference(resolution,[status(thm)],[f6575,f4414])).
% 0.43/1.21 fof(f6799,plain,(
% 0.43/1.21 ![X0]: (c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(t_a),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)),X0)=X0)),
% 0.43/1.21 inference(resolution,[status(thm)],[f1416,f6641])).
% 0.43/1.21 fof(f7289,plain,(
% 0.43/1.21 ~c_Polynomial_Omonom(t_a,v_a,c_HOL_Obool_Obool__size(c_fFalse))=c_Polynomial_Omonom(t_a,v_a,c_HOL_Obool_Obool__size(c_fFalse))),
% 0.43/1.21 inference(backward_demodulation,[status(thm)],[f6799,f5860])).
% 0.43/1.21 fof(f7300,plain,(
% 0.43/1.21 $false),
% 0.43/1.21 inference(trivial_equality_resolution,[status(thm)],[f7289])).
% 0.43/1.21 % SZS output end CNFRefutation for theBenchmark.p
% 1.17/1.21 % Elapsed time: 0.768758 seconds
% 1.17/1.21 % CPU time: 4.762467 seconds
% 1.17/1.21 % Total memory used: 246.841 MB
% 1.17/1.21 % Net memory used: 244.483 MB
%------------------------------------------------------------------------------