%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW186+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 : n008.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:47 PM UTC 2026
% Result : Theorem 2.52s 0.81s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW186+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.33 % Computer : n008.cluster.edu
% 0.08/0.33 % Model : x86_64 x86_64
% 0.08/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.33 % Memory : 8046.5625MB
% 0.08/0.33 % OS : Linux 6.8.0-71-generic
% 0.08/0.33 % CPULimit : 300
% 0.08/0.33 % WCLimit : 300
% 0.08/0.33 % DateTime : Mon Sep 21 09:40:53 UTC 2026
% 0.08/0.33 % CPUTime :
% 0.11/0.42 % Drodi V4.1.1
% 2.52/0.81 % Refutation found
% 2.52/0.81 % SZS status Theorem for theBenchmark: Theorem is valid
% 2.52/0.81 % SZS output start CNFRefutation for theBenchmark
% 2.52/0.81 fof(f2,axiom,(
% 2.52/0.81 (! [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)) ) )),
% 2.52/0.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.52/0.81 fof(f3,axiom,(
% 2.52/0.81 (! [V_h,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,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))) ) )),
% 2.52/0.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.52/0.81 fof(f4,axiom,(
% 2.52/0.81 (! [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))) ) )),
% 2.52/0.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.52/0.81 fof(f5,axiom,(
% 2.52/0.81 (! [V_a,V_p,V_c,T_a] :( class_Rings_Ocomm__semiring__0(T_a)=> ( c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(T_a),c_Polynomial_Osmult(T_a,V_c,V_p),c_Polynomial_OpCons(T_a,V_a,V_p)) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))=> V_p = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)) ) ) )),
% 2.52/0.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.52/0.81 fof(f12,axiom,(
% 2.52/0.81 (! [V_pa_2,V_a_2,T_b] :( class_Groups_Ozero(T_b)=> ( c_Polynomial_OpCons(T_b,V_a_2,V_pa_2) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_b))<=> ( V_a_2 = c_Groups_Ozero__class_Ozero(T_b)& V_pa_2 = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_b)) ) ) ) )),
% 2.52/0.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.52/0.81 fof(f1003,axiom,(
% 2.52/0.81 (! [T] :( class_Rings_Ocomm__semiring__0(T)=> class_Groups_Ozero(T) ) )),
% 2.52/0.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.52/0.81 fof(f1179,hypothesis,(
% 2.52/0.81 ( c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,v_p,v_h) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))=> v_p = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)) ) ),
% 2.52/0.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.52/0.81 fof(f1180,hypothesis,(
% 2.52/0.81 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))) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)) ),
% 2.52/0.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.52/0.81 fof(f1181,conjecture,(
% 2.52/0.81 ( v_a = c_Groups_Ozero__class_Ozero(t_a)& v_p = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)) ) ),
% 2.52/0.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.52/0.81 fof(f1182,negated_conjecture,(
% 2.52/0.81 ~(( v_a = c_Groups_Ozero__class_Ozero(t_a)& v_p = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)) ) )),
% 2.52/0.81 inference(negated_conjecture,[status(cth)],[f1181])).
% 2.52/0.81 fof(f1183,hypothesis,(
% 2.52/0.81 class_Rings_Ocomm__semiring__0(t_a) ),
% 2.52/0.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.52/0.81 fof(f1187,plain,(
% 2.52/0.81 ![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)))),
% 2.52/0.81 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 2.52/0.81 fof(f1188,plain,(
% 2.52/0.81 ![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))))),
% 2.52/0.81 inference(miniscoping,[status(thm)],[f1187])).
% 2.52/0.81 fof(f1189,plain,(
% 2.52/0.81 ![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)))),
% 2.52/0.82 inference(cnf_transformation,[status(thm)],[f1188])).
% 2.52/0.82 fof(f1190,plain,(
% 2.52/0.82 ![V_h,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,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))))),
% 2.52/0.82 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 2.52/0.82 fof(f1191,plain,(
% 2.52/0.82 ![T_a]: (~class_Rings_Ocomm__semiring__0(T_a)|(![V_h,V_a]: 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)))))),
% 2.52/0.82 inference(miniscoping,[status(thm)],[f1190])).
% 2.52/0.82 fof(f1192,plain,(
% 2.52/0.82 ![X0,X1,X2]: (~class_Rings_Ocomm__semiring__0(X0)|c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(X0,c_Polynomial_OpCons(X0,X1,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X0))),X2)=c_Polynomial_OpCons(X0,X1,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X0))))),
% 2.52/0.82 inference(cnf_transformation,[status(thm)],[f1191])).
% 2.52/0.82 fof(f1193,plain,(
% 2.52/0.82 ![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))))),
% 2.52/0.82 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 2.52/0.82 fof(f1194,plain,(
% 2.52/0.82 ![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)))))),
% 2.52/0.82 inference(miniscoping,[status(thm)],[f1193])).
% 2.52/0.82 fof(f1195,plain,(
% 2.52/0.82 ![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))))),
% 2.52/0.82 inference(cnf_transformation,[status(thm)],[f1194])).
% 2.52/0.82 fof(f1196,plain,(
% 2.52/0.82 ![V_a,V_p,V_c,T_a]: (~class_Rings_Ocomm__semiring__0(T_a)|(~c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(T_a),c_Polynomial_Osmult(T_a,V_c,V_p),c_Polynomial_OpCons(T_a,V_a,V_p))=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))|V_p=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))))),
% 2.52/0.82 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 2.52/0.82 fof(f1197,plain,(
% 2.52/0.82 ![T_a]: (~class_Rings_Ocomm__semiring__0(T_a)|(![V_p]: ((![V_a,V_c]: ~c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(T_a),c_Polynomial_Osmult(T_a,V_c,V_p),c_Polynomial_OpCons(T_a,V_a,V_p))=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)))|V_p=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)))))),
% 2.52/0.82 inference(miniscoping,[status(thm)],[f1196])).
% 2.52/0.82 fof(f1198,plain,(
% 2.52/0.82 ![X0,X1,X2,X3]: (~class_Rings_Ocomm__semiring__0(X0)|~c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(X0),c_Polynomial_Osmult(X0,X1,X2),c_Polynomial_OpCons(X0,X3,X2))=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X0))|X2=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)))),
% 2.52/0.82 inference(cnf_transformation,[status(thm)],[f1197])).
% 2.52/0.82 fof(f1219,plain,(
% 2.52/0.82 ![V_pa_2,V_a_2,T_b]: (~class_Groups_Ozero(T_b)|(c_Polynomial_OpCons(T_b,V_a_2,V_pa_2)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_b))<=>(V_a_2=c_Groups_Ozero__class_Ozero(T_b)&V_pa_2=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_b)))))),
% 2.52/0.82 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 2.52/0.82 fof(f1220,plain,(
% 2.52/0.82 ![V_pa_2,V_a_2,T_b]: (~class_Groups_Ozero(T_b)|((~c_Polynomial_OpCons(T_b,V_a_2,V_pa_2)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_b))|(V_a_2=c_Groups_Ozero__class_Ozero(T_b)&V_pa_2=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_b))))&(c_Polynomial_OpCons(T_b,V_a_2,V_pa_2)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_b))|(~V_a_2=c_Groups_Ozero__class_Ozero(T_b)|~V_pa_2=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_b))))))),
% 2.52/0.82 inference(NNF_transformation,[status(thm)],[f1219])).
% 2.52/0.82 fof(f1221,plain,(
% 2.52/0.82 ![T_b]: (~class_Groups_Ozero(T_b)|((![V_pa_2,V_a_2]: (~c_Polynomial_OpCons(T_b,V_a_2,V_pa_2)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_b))|(V_a_2=c_Groups_Ozero__class_Ozero(T_b)&V_pa_2=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_b)))))&(![V_pa_2,V_a_2]: (c_Polynomial_OpCons(T_b,V_a_2,V_pa_2)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_b))|(~V_a_2=c_Groups_Ozero__class_Ozero(T_b)|~V_pa_2=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_b)))))))),
% 2.52/0.82 inference(miniscoping,[status(thm)],[f1220])).
% 2.52/0.82 fof(f1222,plain,(
% 2.52/0.82 ![X0,X1,X2]: (~class_Groups_Ozero(X0)|~c_Polynomial_OpCons(X0,X1,X2)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X0))|X1=c_Groups_Ozero__class_Ozero(X0))),
% 2.52/0.82 inference(cnf_transformation,[status(thm)],[f1221])).
% 2.52/0.82 fof(f4394,plain,(
% 2.52/0.82 ![T]: (~class_Rings_Ocomm__semiring__0(T)|class_Groups_Ozero(T))),
% 2.52/0.82 inference(pre_NNF_transformation,[status(thm)],[f1003])).
% 2.52/0.82 fof(f4395,plain,(
% 2.52/0.82 ![X0]: (~class_Rings_Ocomm__semiring__0(X0)|class_Groups_Ozero(X0))),
% 2.52/0.82 inference(cnf_transformation,[status(thm)],[f4394])).
% 2.52/0.82 fof(f4644,plain,(
% 2.52/0.82 ~c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,v_p,v_h)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))|v_p=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),
% 2.52/0.82 inference(pre_NNF_transformation,[status(thm)],[f1179])).
% 2.52/0.82 fof(f4645,plain,(
% 2.52/0.82 ~c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,v_p,v_h)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))|v_p=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),
% 2.52/0.82 inference(cnf_transformation,[status(thm)],[f4644])).
% 2.52/0.82 fof(f4646,plain,(
% 2.52/0.82 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)))=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),
% 2.52/0.82 inference(cnf_transformation,[status(thm)],[f1180])).
% 2.52/0.82 fof(f4647,plain,(
% 2.52/0.82 (~v_a=c_Groups_Ozero__class_Ozero(t_a)|~v_p=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))),
% 2.52/0.82 inference(pre_NNF_transformation,[status(thm)],[f1182])).
% 2.52/0.82 fof(f4648,plain,(
% 2.52/0.82 ~v_a=c_Groups_Ozero__class_Ozero(t_a)|~v_p=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),
% 2.52/0.82 inference(cnf_transformation,[status(thm)],[f4647])).
% 2.52/0.82 fof(f4649,plain,(
% 2.52/0.82 class_Rings_Ocomm__semiring__0(t_a)),
% 2.52/0.82 inference(cnf_transformation,[status(thm)],[f1183])).
% 2.52/0.82 fof(f4672,definition,(
% 2.52/0.82 sQ0_spl <=> (c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,v_p,v_h)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))),
% 2.52/0.82 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 2.52/0.82 fof(f4675,definition,(
% 2.52/0.82 sQ1_spl <=> (v_p=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))),
% 2.52/0.82 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 2.52/0.82 fof(f4678,plain,(
% 2.52/0.82 ~sQ0_spl|sQ1_spl),
% 2.52/0.82 inference(split_clause,[status(thm)],[f4645,f4672,f4675])).
% 2.52/0.82 fof(f4679,definition,(
% 2.52/0.82 sQ2_spl <=> (v_a=c_Groups_Ozero__class_Ozero(t_a))),
% 2.52/0.82 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 2.52/0.82 fof(f4682,plain,(
% 2.52/0.82 ~sQ2_spl|~sQ1_spl),
% 2.52/0.82 inference(split_clause,[status(thm)],[f4648,f4679,f4675])).
% 2.52/0.82 fof(f4824,plain,(
% 2.52/0.82 ![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)))),
% 2.52/0.82 inference(resolution,[status(thm)],[f1189,f4649])).
% 2.52/0.82 fof(f4825,plain,(
% 2.52/0.82 ![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_Polynomial_OpCons(t_a,X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))))),
% 2.52/0.82 inference(resolution,[status(thm)],[f1192,f4649])).
% 2.52/0.82 fof(f4826,plain,(
% 2.52/0.82 ![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))))),
% 2.52/0.82 inference(resolution,[status(thm)],[f1195,f4649])).
% 2.52/0.82 fof(f4827,plain,(
% 2.52/0.82 ~class_Rings_Ocomm__semiring__0(t_a)|c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,v_p,v_h)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),
% 2.52/0.82 inference(resolution,[status(thm)],[f1198,f4646])).
% 2.52/0.82 fof(f4829,definition,(
% 2.52/0.82 sQ3_spl <=> (class_Rings_Ocomm__semiring__0(t_a))),
% 2.52/0.82 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 2.52/0.82 fof(f4831,plain,(
% 2.52/0.82 ~class_Rings_Ocomm__semiring__0(t_a)|sQ3_spl),
% 2.52/0.82 inference(component_clause,[status(thm)],[f4829])).
% 2.52/0.82 fof(f4832,plain,(
% 2.52/0.82 ~sQ3_spl|sQ0_spl),
% 2.52/0.82 inference(split_clause,[status(thm)],[f4827,f4829,f4672])).
% 2.52/0.82 fof(f4837,plain,(
% 2.52/0.82 $false|sQ3_spl),
% 2.52/0.82 inference(forward_subsumption_resolution,[status(thm)],[f4831,f4649])).
% 2.52/0.82 fof(f4838,plain,(
% 2.52/0.82 sQ3_spl),
% 2.52/0.82 inference(contradiction_clause,[status(thm)],[f4837])).
% 2.52/0.82 fof(f4839,plain,(
% 2.52/0.82 c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,c_Polynomial_OpCons(t_a,v_a,v_p),v_h)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),
% 2.52/0.82 inference(backward_demodulation,[status(thm)],[f4826,f4646])).
% 2.52/0.82 fof(f4841,plain,(
% 2.52/0.82 ![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))))),
% 2.52/0.82 inference(paramodulation,[status(thm)],[f4824,f4826])).
% 2.52/0.82 fof(f4844,plain,(
% 2.52/0.82 ![X0,X1,X2]: (~class_Rings_Ocomm__semiring__0(t_a)|~c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,c_Polynomial_OpCons(t_a,X0,X1),X2)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))|c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,X1,X2)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))),
% 2.52/0.82 inference(paramodulation,[status(thm)],[f4826,f1198])).
% 2.52/0.82 fof(f4846,plain,(
% 2.52/0.82 ![X0,X1]: (c_Polynomial_OpCons(t_a,X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))=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))))),
% 2.52/0.82 inference(forward_demodulation,[status(thm)],[f4825,f4841])).
% 2.52/0.82 fof(f4847,plain,(
% 2.52/0.82 ![X0,X1]: (c_Polynomial_OpCons(t_a,X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))=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)))))),
% 2.52/0.82 inference(forward_demodulation,[status(thm)],[f4824,f4846])).
% 2.52/0.82 fof(f4851,definition,(
% 2.52/0.82 ![X0,X1,X2]: (sQ5_spl <=> (~c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,c_Polynomial_OpCons(t_a,X0,X1),X2)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))|c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,X1,X2)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))))),
% 2.52/0.82 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 2.52/0.82 fof(f4852,plain,(
% 2.52/0.82 ![X0,X1,X2]: (~c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,c_Polynomial_OpCons(t_a,X0,X1),X2)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))|c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,X1,X2)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))|~sQ5_spl)),
% 2.52/0.83 inference(component_clause,[status(thm)],[f4851])).
% 2.52/0.83 fof(f4854,plain,(
% 2.52/0.83 ~sQ3_spl|sQ5_spl),
% 2.52/0.83 inference(split_clause,[status(thm)],[f4844,f4829,f4851])).
% 2.52/0.83 fof(f4859,plain,(
% 2.52/0.83 c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,v_p,v_h)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))|~sQ5_spl),
% 2.52/0.83 inference(resolution,[status(thm)],[f4852,f4839])).
% 2.52/0.83 fof(f4870,plain,(
% 2.52/0.83 ![X0]: (c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,c_Polynomial_OpCons(t_a,X0,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,X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))))|~sQ5_spl)),
% 2.52/0.83 inference(paramodulation,[status(thm)],[f4859,f4826])).
% 2.52/0.83 fof(f4872,plain,(
% 2.52/0.83 ![X0]: (c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,c_Polynomial_OpCons(t_a,X0,v_p),v_h)=c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(t_a),c_Polynomial_Osmult(t_a,v_h,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))))|~sQ5_spl)),
% 2.52/0.83 inference(forward_demodulation,[status(thm)],[f4859,f4870])).
% 2.52/0.83 fof(f4881,plain,(
% 2.52/0.83 c_Polynomial_OpCons(t_a,v_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))|~sQ5_spl),
% 2.52/0.83 inference(backward_demodulation,[status(thm)],[f4882,f4839])).
% 2.52/0.83 fof(f4882,plain,(
% 2.52/0.83 ![X0]: (c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,c_Polynomial_OpCons(t_a,X0,v_p),v_h)=c_Polynomial_OpCons(t_a,X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))|~sQ5_spl)),
% 2.52/0.83 inference(forward_demodulation,[status(thm)],[f4847,f4872])).
% 2.52/0.83 fof(f5191,plain,(
% 2.52/0.83 ~class_Groups_Ozero(t_a)|v_a=c_Groups_Ozero__class_Ozero(t_a)|~sQ5_spl),
% 2.52/0.83 inference(resolution,[status(thm)],[f1222,f4881])).
% 2.52/0.83 fof(f5193,definition,(
% 2.52/0.83 sQ22_spl <=> (class_Groups_Ozero(t_a))),
% 2.52/0.83 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 2.52/0.83 fof(f5195,plain,(
% 2.52/0.83 ~class_Groups_Ozero(t_a)|sQ22_spl),
% 2.52/0.83 inference(component_clause,[status(thm)],[f5193])).
% 2.52/0.83 fof(f5196,plain,(
% 2.52/0.83 ~sQ22_spl|sQ2_spl|~sQ5_spl),
% 2.52/0.83 inference(split_clause,[status(thm)],[f5191,f5193,f4679,f4851])).
% 2.52/0.83 fof(f9253,plain,(
% 2.52/0.83 class_Groups_Ozero(t_a)),
% 2.52/0.83 inference(resolution,[status(thm)],[f4395,f4649])).
% 2.52/0.83 fof(f9254,plain,(
% 2.52/0.83 $false|sQ22_spl),
% 2.52/0.83 inference(forward_subsumption_resolution,[status(thm)],[f9253,f5195])).
% 2.52/0.83 fof(f9255,plain,(
% 2.52/0.83 sQ22_spl),
% 2.52/0.83 inference(contradiction_clause,[status(thm)],[f9254])).
% 2.52/0.83 fof(f9256,plain,(
% 2.52/0.83 $false),
% 2.52/0.83 inference(sat_refutation,[status(thm)],[f4678,f4682,f4832,f4838,f4854,f5196,f9255])).
% 2.52/0.83 % SZS output end CNFRefutation for theBenchmark.p
% 2.76/0.89 % Elapsed time: 0.552847 seconds
% 2.76/0.89 % CPU time: 3.213492 seconds
% 2.76/0.89 % Total memory used: 238.661 MB
% 2.76/0.89 % Net memory used: 236.594 MB
%------------------------------------------------------------------------------