%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW185+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 : 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 03:08:46 PM UTC 2026
% Result : Theorem 8.92s 1.78s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWW185+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.20/0.44 % Computer : n009.cluster.edu
% 0.20/0.44 % Model : x86_64 x86_64
% 0.20/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/0.44 % Memory : 8046.5625MB
% 0.20/0.44 % OS : Linux 6.8.0-71-generic
% 0.20/0.45 % CPULimit : 300
% 0.20/0.45 % WCLimit : 300
% 0.20/0.45 % DateTime : Mon Sep 21 09:40:12 UTC 2026
% 0.20/0.45 % CPUTime :
% 0.23/0.60 % Drodi V4.1.1
% 8.92/1.78 % Refutation found
% 8.92/1.78 % SZS status Theorem for theBenchmark: Theorem is valid
% 8.92/1.78 % SZS output start CNFRefutation for theBenchmark
% 8.92/1.78 fof(f1,axiom,(
% 8.92/1.78 (! [V_g_2,V_f_2] :( (! [B_x] : hAPP(V_f_2,B_x) = hAPP(V_g_2,B_x))=> V_f_2 = V_g_2 ) )),
% 8.92/1.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 8.92/1.78 fof(f18,axiom,(
% 8.92/1.78 (! [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))) ) )),
% 8.92/1.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 8.92/1.78 fof(f20,axiom,(
% 8.92/1.78 (! [V_n_2,V_a_2,T_b] :( class_Groups_Ozero(T_b)=> ( c_Polynomial_Omonom(T_b,V_a_2,V_n_2) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_b))<=> V_a_2 = c_Groups_Ozero__class_Ozero(T_b) ) ) )),
% 8.92/1.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 8.92/1.78 fof(f27,axiom,(
% 8.92/1.78 (! [V_x,T_a] :( class_Rings_Ocomm__semiring__0(T_a)=> hAPP(c_Polynomial_Opoly(T_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))),V_x) = c_Groups_Ozero__class_Ozero(T_a) ) )),
% 8.92/1.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 8.92/1.78 fof(f28,axiom,(
% 8.92/1.78 (! [V_c,T_a] :( class_Rings_Ocomm__semiring__0(T_a)=> c_Polynomial_Osynthetic__div(T_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)),V_c) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)) ) )),
% 8.92/1.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 8.92/1.78 fof(f29,axiom,(
% 8.92/1.78 (! [V_a,V_n,V_m,T_a] :( class_Groups_Ozero(T_a)=> ( ( V_m = V_n=> hAPP(c_Polynomial_Ocoeff(T_a,c_Polynomial_Omonom(T_a,V_a,V_m)),V_n) = V_a )& ( V_m != V_n=> hAPP(c_Polynomial_Ocoeff(T_a,c_Polynomial_Omonom(T_a,V_a,V_m)),V_n) = c_Groups_Ozero__class_Ozero(T_a) ) ) ) )),
% 8.92/1.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 8.92/1.78 fof(f32,axiom,(
% 8.92/1.78 (! [V_p,T_a] :( class_Rings_Ocomm__semiring__0(T_a)=> c_Polynomial_Osmult(T_a,c_Groups_Ozero__class_Ozero(T_a),V_p) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)) ) )),
% 8.92/1.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 8.92/1.78 fof(f35,axiom,(
% 8.92/1.78 (! [V_y_2,V_x_2,T_b] :( class_Groups_Ozero(T_b)=> ( c_Polynomial_Ocoeff(T_b,V_x_2) = c_Polynomial_Ocoeff(T_b,V_y_2)<=> V_x_2 = V_y_2 ) ) )),
% 8.92/1.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 8.92/1.78 fof(f39,axiom,(
% 8.92/1.78 (! [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)) ) )),
% 8.92/1.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 8.92/1.78 fof(f50,axiom,(
% 8.92/1.78 (! [V_c,V_p,T_a] :( class_Rings_Ocomm__semiring__0(T_a)=> c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(T_a),V_p,c_Polynomial_Osmult(T_a,V_c,c_Polynomial_Osynthetic__div(T_a,V_p,V_c))) = c_Polynomial_OpCons(T_a,hAPP(c_Polynomial_Opoly(T_a,V_p),V_c),c_Polynomial_Osynthetic__div(T_a,V_p,V_c)) ) )),
% 8.92/1.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 8.92/1.78 fof(f51,axiom,(
% 8.92/1.78 (! [V_r,V_q,V_c,V_p,T_a] :( class_Rings_Ocomm__semiring__0(T_a)=> ( c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(T_a),V_p,c_Polynomial_Osmult(T_a,V_c,V_q)) = c_Polynomial_OpCons(T_a,V_r,V_q)=> ( V_r = hAPP(c_Polynomial_Opoly(T_a,V_p),V_c)& V_q = c_Polynomial_Osynthetic__div(T_a,V_p,V_c) ) ) ) )),
% 8.92/1.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 8.92/1.78 fof(f66,axiom,(
% 8.92/1.78 (! [V_a,T_a] :( class_Groups_Ocomm__monoid__add(T_a)=> c_Groups_Oplus__class_Oplus(T_a,V_a,c_Groups_Ozero__class_Ozero(T_a)) = V_a ) )),
% 8.92/1.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 8.92/1.78 fof(f69,axiom,(
% 8.92/1.78 (! [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 ) )),
% 8.92/1.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 8.92/1.78 fof(f73,axiom,(
% 8.92/1.78 (! [V_q,V_p,V_a,T_a] :( class_Rings_Ocomm__semiring__0(T_a)=> c_Polynomial_Osmult(T_a,V_a,c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(T_a),V_p,V_q)) = c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(T_a),c_Polynomial_Osmult(T_a,V_a,V_p),c_Polynomial_Osmult(T_a,V_a,V_q)) ) )),
% 8.92/1.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 8.92/1.78 fof(f74,axiom,(
% 8.92/1.78 (! [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)) ) )),
% 8.92/1.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 8.92/1.78 fof(f75,axiom,(
% 8.92/1.78 (! [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)) ) ) )),
% 8.92/1.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 8.92/1.78 fof(f80,axiom,(
% 8.92/1.78 (! [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))) ) )),
% 8.92/1.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 8.92/1.78 fof(f90,axiom,(
% 8.92/1.78 (! [V_x,V_p,V_a,T_a] :( class_Rings_Ocomm__semiring__0(T_a)=> hAPP(c_Polynomial_Opoly(T_a,c_Polynomial_OpCons(T_a,V_a,V_p)),V_x) = c_Groups_Oplus__class_Oplus(T_a,V_a,hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_x),hAPP(c_Polynomial_Opoly(T_a,V_p),V_x))) ) )),
% 8.92/1.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 8.92/1.78 fof(f381,axiom,(
% 8.92/1.78 c_HOL_Obool_Obool__size(c_fFalse) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat) ),
% 8.92/1.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 8.92/1.78 fof(f998,axiom,(
% 8.92/1.78 (! [T] :( class_Rings_Ocomm__semiring__0(T)=> class_Groups_Ocomm__monoid__add(T) ) )),
% 8.92/1.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 8.92/1.78 fof(f1004,axiom,(
% 8.92/1.78 (! [T] :( class_Rings_Ocomm__semiring__0(T)=> class_Groups_Ozero(T) ) )),
% 8.92/1.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 8.92/1.78 fof(f1147,axiom,(
% 8.92/1.78 (! [T_1] :( class_Rings_Ocomm__semiring__0(T_1)=> class_Rings_Ocomm__semiring__0(tc_Polynomial_Opoly(T_1)) ) )),
% 8.92/1.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 8.92/1.78 fof(f1180,hypothesis,(
% 8.92/1.78 ( 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)) ) ),
% 8.92/1.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 8.92/1.78 fof(f1181,hypothesis,(
% 8.92/1.78 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)) ),
% 8.92/1.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 8.92/1.78 fof(f1182,conjecture,(
% 8.92/1.78 c_Polynomial_OpCons(t_a,v_a,v_p) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)) ),
% 8.92/1.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 8.92/1.78 fof(f1183,negated_conjecture,(
% 8.92/1.78 ~(c_Polynomial_OpCons(t_a,v_a,v_p) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)) )),
% 8.92/1.78 inference(negated_conjecture,[status(cth)],[f1182])).
% 8.92/1.78 fof(f1184,hypothesis,(
% 8.92/1.78 class_Rings_Ocomm__semiring__0(t_a) ),
% 8.92/1.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 8.92/1.78 fof(f1185,plain,(
% 8.92/1.78 ![V_g_2,V_f_2]: ((?[B_x]: ~hAPP(V_f_2,B_x)=hAPP(V_g_2,B_x))|V_f_2=V_g_2)),
% 8.92/1.78 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 8.92/1.78 fof(f1186,plain,(
% 8.92/1.78 ![V_g_2,V_f_2]: (~hAPP(V_f_2,sK0_skl(V_f_2,V_g_2))=hAPP(V_g_2,sK0_skl(V_f_2,V_g_2))|V_f_2=V_g_2)),
% 8.92/1.78 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(B_x,sK0_skl(V_f_2,V_g_2))],[f1185])).
% 8.92/1.78 fof(f1187,plain,(
% 8.92/1.78 ![X0,X1]: (~hAPP(X0,sK0_skl(X0,X1))=hAPP(X1,sK0_skl(X0,X1))|X0=X1)),
% 8.92/1.78 inference(cnf_transformation,[status(thm)],[f1186])).
% 8.92/1.78 fof(f1258,plain,(
% 8.92/1.78 ![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))))),
% 8.92/1.78 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 8.92/1.78 fof(f1259,plain,(
% 8.92/1.78 ![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)))))),
% 8.92/1.78 inference(miniscoping,[status(thm)],[f1258])).
% 8.92/1.78 fof(f1260,plain,(
% 8.92/1.78 ![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))))),
% 8.92/1.78 inference(cnf_transformation,[status(thm)],[f1259])).
% 8.92/1.78 fof(f1263,plain,(
% 8.92/1.78 ![V_n_2,V_a_2,T_b]: (~class_Groups_Ozero(T_b)|(c_Polynomial_Omonom(T_b,V_a_2,V_n_2)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_b))<=>V_a_2=c_Groups_Ozero__class_Ozero(T_b)))),
% 8.92/1.78 inference(pre_NNF_transformation,[status(thm)],[f20])).
% 8.92/1.78 fof(f1264,plain,(
% 8.92/1.78 ![V_n_2,V_a_2,T_b]: (~class_Groups_Ozero(T_b)|((~c_Polynomial_Omonom(T_b,V_a_2,V_n_2)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_b))|V_a_2=c_Groups_Ozero__class_Ozero(T_b))&(c_Polynomial_Omonom(T_b,V_a_2,V_n_2)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_b))|~V_a_2=c_Groups_Ozero__class_Ozero(T_b))))),
% 8.92/1.78 inference(NNF_transformation,[status(thm)],[f1263])).
% 8.92/1.78 fof(f1265,plain,(
% 8.92/1.78 ![T_b]: (~class_Groups_Ozero(T_b)|((![V_a_2]: ((![V_n_2]: ~c_Polynomial_Omonom(T_b,V_a_2,V_n_2)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_b)))|V_a_2=c_Groups_Ozero__class_Ozero(T_b)))&(![V_a_2]: ((![V_n_2]: c_Polynomial_Omonom(T_b,V_a_2,V_n_2)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_b)))|~V_a_2=c_Groups_Ozero__class_Ozero(T_b)))))),
% 8.92/1.78 inference(miniscoping,[status(thm)],[f1264])).
% 8.92/1.78 fof(f1267,plain,(
% 8.92/1.78 ![X0,X1,X2]: (~class_Groups_Ozero(X0)|c_Polynomial_Omonom(X0,X1,X2)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X0))|~X1=c_Groups_Ozero__class_Ozero(X0))),
% 8.92/1.78 inference(cnf_transformation,[status(thm)],[f1265])).
% 8.92/1.78 fof(f1286,plain,(
% 8.92/1.78 ![V_x,T_a]: (~class_Rings_Ocomm__semiring__0(T_a)|hAPP(c_Polynomial_Opoly(T_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))),V_x)=c_Groups_Ozero__class_Ozero(T_a))),
% 8.92/1.78 inference(pre_NNF_transformation,[status(thm)],[f27])).
% 8.92/1.78 fof(f1287,plain,(
% 8.92/1.78 ![T_a]: (~class_Rings_Ocomm__semiring__0(T_a)|(![V_x]: hAPP(c_Polynomial_Opoly(T_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))),V_x)=c_Groups_Ozero__class_Ozero(T_a)))),
% 8.92/1.78 inference(miniscoping,[status(thm)],[f1286])).
% 8.92/1.78 fof(f1288,plain,(
% 8.92/1.78 ![X0,X1]: (~class_Rings_Ocomm__semiring__0(X0)|hAPP(c_Polynomial_Opoly(X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X0))),X1)=c_Groups_Ozero__class_Ozero(X0))),
% 8.92/1.78 inference(cnf_transformation,[status(thm)],[f1287])).
% 8.92/1.78 fof(f1289,plain,(
% 8.92/1.78 ![V_c,T_a]: (~class_Rings_Ocomm__semiring__0(T_a)|c_Polynomial_Osynthetic__div(T_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)),V_c)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)))),
% 8.92/1.78 inference(pre_NNF_transformation,[status(thm)],[f28])).
% 8.92/1.78 fof(f1290,plain,(
% 8.92/1.78 ![T_a]: (~class_Rings_Ocomm__semiring__0(T_a)|(![V_c]: c_Polynomial_Osynthetic__div(T_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)),V_c)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))))),
% 8.92/1.78 inference(miniscoping,[status(thm)],[f1289])).
% 8.92/1.78 fof(f1291,plain,(
% 8.92/1.78 ![X0,X1]: (~class_Rings_Ocomm__semiring__0(X0)|c_Polynomial_Osynthetic__div(X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)),X1)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)))),
% 8.92/1.78 inference(cnf_transformation,[status(thm)],[f1290])).
% 8.92/1.78 fof(f1292,plain,(
% 8.92/1.78 ![V_a,V_n,V_m,T_a]: (~class_Groups_Ozero(T_a)|((~V_m=V_n|hAPP(c_Polynomial_Ocoeff(T_a,c_Polynomial_Omonom(T_a,V_a,V_m)),V_n)=V_a)&(V_m=V_n|hAPP(c_Polynomial_Ocoeff(T_a,c_Polynomial_Omonom(T_a,V_a,V_m)),V_n)=c_Groups_Ozero__class_Ozero(T_a))))),
% 8.92/1.78 inference(pre_NNF_transformation,[status(thm)],[f29])).
% 8.92/1.78 fof(f1293,plain,(
% 8.92/1.78 ![T_a]: (~class_Groups_Ozero(T_a)|((![V_n,V_m]: (~V_m=V_n|(![V_a]: hAPP(c_Polynomial_Ocoeff(T_a,c_Polynomial_Omonom(T_a,V_a,V_m)),V_n)=V_a)))&(![V_n,V_m]: (V_m=V_n|(![V_a]: hAPP(c_Polynomial_Ocoeff(T_a,c_Polynomial_Omonom(T_a,V_a,V_m)),V_n)=c_Groups_Ozero__class_Ozero(T_a))))))),
% 8.92/1.78 inference(miniscoping,[status(thm)],[f1292])).
% 8.92/1.78 fof(f1294,plain,(
% 8.92/1.78 ![X0,X1,X2,X3]: (~class_Groups_Ozero(X0)|~X1=X2|hAPP(c_Polynomial_Ocoeff(X0,c_Polynomial_Omonom(X0,X3,X1)),X2)=X3)),
% 8.92/1.78 inference(cnf_transformation,[status(thm)],[f1293])).
% 8.92/1.78 fof(f1305,plain,(
% 8.92/1.78 ![V_p,T_a]: (~class_Rings_Ocomm__semiring__0(T_a)|c_Polynomial_Osmult(T_a,c_Groups_Ozero__class_Ozero(T_a),V_p)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)))),
% 8.92/1.78 inference(pre_NNF_transformation,[status(thm)],[f32])).
% 8.92/1.78 fof(f1306,plain,(
% 8.92/1.78 ![T_a]: (~class_Rings_Ocomm__semiring__0(T_a)|(![V_p]: c_Polynomial_Osmult(T_a,c_Groups_Ozero__class_Ozero(T_a),V_p)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))))),
% 8.92/1.78 inference(miniscoping,[status(thm)],[f1305])).
% 8.92/1.78 fof(f1307,plain,(
% 8.92/1.78 ![X0,X1]: (~class_Rings_Ocomm__semiring__0(X0)|c_Polynomial_Osmult(X0,c_Groups_Ozero__class_Ozero(X0),X1)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)))),
% 8.92/1.78 inference(cnf_transformation,[status(thm)],[f1306])).
% 8.92/1.78 fof(f1319,plain,(
% 8.92/1.78 ![V_y_2,V_x_2,T_b]: (~class_Groups_Ozero(T_b)|(c_Polynomial_Ocoeff(T_b,V_x_2)=c_Polynomial_Ocoeff(T_b,V_y_2)<=>V_x_2=V_y_2))),
% 8.92/1.78 inference(pre_NNF_transformation,[status(thm)],[f35])).
% 8.92/1.78 fof(f1320,plain,(
% 8.92/1.78 ![V_y_2,V_x_2,T_b]: (~class_Groups_Ozero(T_b)|((~c_Polynomial_Ocoeff(T_b,V_x_2)=c_Polynomial_Ocoeff(T_b,V_y_2)|V_x_2=V_y_2)&(c_Polynomial_Ocoeff(T_b,V_x_2)=c_Polynomial_Ocoeff(T_b,V_y_2)|~V_x_2=V_y_2)))),
% 8.92/1.78 inference(NNF_transformation,[status(thm)],[f1319])).
% 8.92/1.78 fof(f1321,plain,(
% 8.92/1.78 ![T_b]: (~class_Groups_Ozero(T_b)|((![V_y_2,V_x_2]: (~c_Polynomial_Ocoeff(T_b,V_x_2)=c_Polynomial_Ocoeff(T_b,V_y_2)|V_x_2=V_y_2))&(![V_y_2,V_x_2]: (c_Polynomial_Ocoeff(T_b,V_x_2)=c_Polynomial_Ocoeff(T_b,V_y_2)|~V_x_2=V_y_2))))),
% 8.92/1.78 inference(miniscoping,[status(thm)],[f1320])).
% 8.92/1.78 fof(f1322,plain,(
% 8.92/1.78 ![X0,X1,X2]: (~class_Groups_Ozero(X0)|~c_Polynomial_Ocoeff(X0,X1)=c_Polynomial_Ocoeff(X0,X2)|X1=X2)),
% 8.92/1.78 inference(cnf_transformation,[status(thm)],[f1321])).
% 8.92/1.78 fof(f1333,plain,(
% 8.92/1.78 ![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)))),
% 8.92/1.78 inference(pre_NNF_transformation,[status(thm)],[f39])).
% 8.92/1.78 fof(f1334,plain,(
% 8.92/1.78 ![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))))),
% 8.92/1.78 inference(miniscoping,[status(thm)],[f1333])).
% 8.92/1.78 fof(f1335,plain,(
% 8.92/1.78 ![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)))),
% 8.92/1.78 inference(cnf_transformation,[status(thm)],[f1334])).
% 8.92/1.78 fof(f1359,plain,(
% 8.92/1.78 ![V_c,V_p,T_a]: (~class_Rings_Ocomm__semiring__0(T_a)|c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(T_a),V_p,c_Polynomial_Osmult(T_a,V_c,c_Polynomial_Osynthetic__div(T_a,V_p,V_c)))=c_Polynomial_OpCons(T_a,hAPP(c_Polynomial_Opoly(T_a,V_p),V_c),c_Polynomial_Osynthetic__div(T_a,V_p,V_c)))),
% 8.92/1.78 inference(pre_NNF_transformation,[status(thm)],[f50])).
% 8.92/1.78 fof(f1360,plain,(
% 8.92/1.78 ![T_a]: (~class_Rings_Ocomm__semiring__0(T_a)|(![V_c,V_p]: c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(T_a),V_p,c_Polynomial_Osmult(T_a,V_c,c_Polynomial_Osynthetic__div(T_a,V_p,V_c)))=c_Polynomial_OpCons(T_a,hAPP(c_Polynomial_Opoly(T_a,V_p),V_c),c_Polynomial_Osynthetic__div(T_a,V_p,V_c))))),
% 8.92/1.78 inference(miniscoping,[status(thm)],[f1359])).
% 8.92/1.78 fof(f1361,plain,(
% 8.92/1.78 ![X0,X1,X2]: (~class_Rings_Ocomm__semiring__0(X0)|c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(X0),X1,c_Polynomial_Osmult(X0,X2,c_Polynomial_Osynthetic__div(X0,X1,X2)))=c_Polynomial_OpCons(X0,hAPP(c_Polynomial_Opoly(X0,X1),X2),c_Polynomial_Osynthetic__div(X0,X1,X2)))),
% 8.92/1.78 inference(cnf_transformation,[status(thm)],[f1360])).
% 8.92/1.78 fof(f1362,plain,(
% 8.92/1.78 ![V_r,V_q,V_c,V_p,T_a]: (~class_Rings_Ocomm__semiring__0(T_a)|(~c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(T_a),V_p,c_Polynomial_Osmult(T_a,V_c,V_q))=c_Polynomial_OpCons(T_a,V_r,V_q)|(V_r=hAPP(c_Polynomial_Opoly(T_a,V_p),V_c)&V_q=c_Polynomial_Osynthetic__div(T_a,V_p,V_c))))),
% 8.92/1.78 inference(pre_NNF_transformation,[status(thm)],[f51])).
% 8.92/1.78 fof(f1363,plain,(
% 8.92/1.78 ![T_a]: (~class_Rings_Ocomm__semiring__0(T_a)|(![V_r,V_q,V_c,V_p]: (~c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(T_a),V_p,c_Polynomial_Osmult(T_a,V_c,V_q))=c_Polynomial_OpCons(T_a,V_r,V_q)|(V_r=hAPP(c_Polynomial_Opoly(T_a,V_p),V_c)&V_q=c_Polynomial_Osynthetic__div(T_a,V_p,V_c)))))),
% 8.92/1.78 inference(miniscoping,[status(thm)],[f1362])).
% 8.92/1.78 fof(f1364,plain,(
% 8.92/1.78 ![X0,X1,X2,X3,X4]: (~class_Rings_Ocomm__semiring__0(X0)|~c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(X0),X1,c_Polynomial_Osmult(X0,X2,X3))=c_Polynomial_OpCons(X0,X4,X3)|X4=hAPP(c_Polynomial_Opoly(X0,X1),X2))),
% 8.92/1.78 inference(cnf_transformation,[status(thm)],[f1363])).
% 8.92/1.78 fof(f1408,plain,(
% 8.92/1.78 ![V_a,T_a]: (~class_Groups_Ocomm__monoid__add(T_a)|c_Groups_Oplus__class_Oplus(T_a,V_a,c_Groups_Ozero__class_Ozero(T_a))=V_a)),
% 8.92/1.78 inference(pre_NNF_transformation,[status(thm)],[f66])).
% 8.92/1.78 fof(f1409,plain,(
% 8.92/1.78 ![T_a]: (~class_Groups_Ocomm__monoid__add(T_a)|(![V_a]: c_Groups_Oplus__class_Oplus(T_a,V_a,c_Groups_Ozero__class_Ozero(T_a))=V_a))),
% 8.92/1.78 inference(miniscoping,[status(thm)],[f1408])).
% 8.92/1.78 fof(f1410,plain,(
% 8.92/1.78 ![X0,X1]: (~class_Groups_Ocomm__monoid__add(X0)|c_Groups_Oplus__class_Oplus(X0,X1,c_Groups_Ozero__class_Ozero(X0))=X1)),
% 8.92/1.78 inference(cnf_transformation,[status(thm)],[f1409])).
% 8.92/1.78 fof(f1419,plain,(
% 8.92/1.78 ![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)),
% 8.92/1.78 inference(pre_NNF_transformation,[status(thm)],[f69])).
% 8.92/1.78 fof(f1420,plain,(
% 8.92/1.78 ![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))),
% 8.92/1.78 inference(miniscoping,[status(thm)],[f1419])).
% 8.92/1.78 fof(f1421,plain,(
% 8.92/1.78 ![X0,X1]: (~class_Groups_Ocomm__monoid__add(X0)|c_Groups_Oplus__class_Oplus(X0,c_Groups_Ozero__class_Ozero(X0),X1)=X1)),
% 8.92/1.78 inference(cnf_transformation,[status(thm)],[f1420])).
% 8.92/1.78 fof(f1431,plain,(
% 8.92/1.78 ![V_q,V_p,V_a,T_a]: (~class_Rings_Ocomm__semiring__0(T_a)|c_Polynomial_Osmult(T_a,V_a,c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(T_a),V_p,V_q))=c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(T_a),c_Polynomial_Osmult(T_a,V_a,V_p),c_Polynomial_Osmult(T_a,V_a,V_q)))),
% 8.92/1.78 inference(pre_NNF_transformation,[status(thm)],[f73])).
% 8.92/1.78 fof(f1432,plain,(
% 8.92/1.78 ![T_a]: (~class_Rings_Ocomm__semiring__0(T_a)|(![V_q,V_p,V_a]: c_Polynomial_Osmult(T_a,V_a,c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(T_a),V_p,V_q))=c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(T_a),c_Polynomial_Osmult(T_a,V_a,V_p),c_Polynomial_Osmult(T_a,V_a,V_q))))),
% 8.92/1.78 inference(miniscoping,[status(thm)],[f1431])).
% 8.92/1.78 fof(f1433,plain,(
% 8.92/1.78 ![X0,X1,X2,X3]: (~class_Rings_Ocomm__semiring__0(X0)|c_Polynomial_Osmult(X0,X1,c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(X0),X2,X3))=c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(X0),c_Polynomial_Osmult(X0,X1,X2),c_Polynomial_Osmult(X0,X1,X3)))),
% 8.92/1.78 inference(cnf_transformation,[status(thm)],[f1432])).
% 8.92/1.78 fof(f1434,plain,(
% 8.92/1.78 ![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)))),
% 8.92/1.78 inference(pre_NNF_transformation,[status(thm)],[f74])).
% 8.92/1.78 fof(f1435,plain,(
% 8.92/1.78 ![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))))),
% 8.92/1.78 inference(miniscoping,[status(thm)],[f1434])).
% 8.92/1.78 fof(f1436,plain,(
% 8.92/1.78 ![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)))),
% 8.92/1.78 inference(cnf_transformation,[status(thm)],[f1435])).
% 8.92/1.78 fof(f1437,plain,(
% 8.92/1.78 ![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))))),
% 8.92/1.78 inference(pre_NNF_transformation,[status(thm)],[f75])).
% 8.92/1.78 fof(f1438,plain,(
% 8.92/1.78 ![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)))))),
% 8.92/1.78 inference(miniscoping,[status(thm)],[f1437])).
% 8.92/1.78 fof(f1439,plain,(
% 8.92/1.78 ![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)))),
% 8.92/1.78 inference(cnf_transformation,[status(thm)],[f1438])).
% 8.92/1.78 fof(f1448,plain,(
% 8.92/1.78 ![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))))),
% 8.92/1.78 inference(pre_NNF_transformation,[status(thm)],[f80])).
% 8.92/1.78 fof(f1449,plain,(
% 8.92/1.78 ![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)))))),
% 8.92/1.78 inference(miniscoping,[status(thm)],[f1448])).
% 8.92/1.78 fof(f1450,plain,(
% 8.92/1.78 ![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))))),
% 8.92/1.78 inference(cnf_transformation,[status(thm)],[f1449])).
% 8.92/1.78 fof(f1483,plain,(
% 8.92/1.78 ![V_x,V_p,V_a,T_a]: (~class_Rings_Ocomm__semiring__0(T_a)|hAPP(c_Polynomial_Opoly(T_a,c_Polynomial_OpCons(T_a,V_a,V_p)),V_x)=c_Groups_Oplus__class_Oplus(T_a,V_a,hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_x),hAPP(c_Polynomial_Opoly(T_a,V_p),V_x))))),
% 8.92/1.78 inference(pre_NNF_transformation,[status(thm)],[f90])).
% 8.92/1.78 fof(f1484,plain,(
% 8.92/1.78 ![T_a]: (~class_Rings_Ocomm__semiring__0(T_a)|(![V_x,V_p,V_a]: hAPP(c_Polynomial_Opoly(T_a,c_Polynomial_OpCons(T_a,V_a,V_p)),V_x)=c_Groups_Oplus__class_Oplus(T_a,V_a,hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_x),hAPP(c_Polynomial_Opoly(T_a,V_p),V_x)))))),
% 8.92/1.78 inference(miniscoping,[status(thm)],[f1483])).
% 8.92/1.78 fof(f1485,plain,(
% 8.92/1.78 ![X0,X1,X2,X3]: (~class_Rings_Ocomm__semiring__0(X0)|hAPP(c_Polynomial_Opoly(X0,c_Polynomial_OpCons(X0,X1,X2)),X3)=c_Groups_Oplus__class_Oplus(X0,X1,hAPP(hAPP(c_Groups_Otimes__class_Otimes(X0),X3),hAPP(c_Polynomial_Opoly(X0,X2),X3))))),
% 8.92/1.78 inference(cnf_transformation,[status(thm)],[f1484])).
% 8.92/1.78 fof(f2417,plain,(
% 8.92/1.78 c_HOL_Obool_Obool__size(c_fFalse)=c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
% 8.92/1.78 inference(cnf_transformation,[status(thm)],[f381])).
% 8.92/1.78 fof(f4412,plain,(
% 8.92/1.78 ![T]: (~class_Rings_Ocomm__semiring__0(T)|class_Groups_Ocomm__monoid__add(T))),
% 8.92/1.78 inference(pre_NNF_transformation,[status(thm)],[f998])).
% 8.92/1.78 fof(f4413,plain,(
% 8.92/1.78 ![X0]: (~class_Rings_Ocomm__semiring__0(X0)|class_Groups_Ocomm__monoid__add(X0))),
% 8.92/1.78 inference(cnf_transformation,[status(thm)],[f4412])).
% 8.92/1.78 fof(f4424,plain,(
% 8.92/1.78 ![T]: (~class_Rings_Ocomm__semiring__0(T)|class_Groups_Ozero(T))),
% 8.92/1.78 inference(pre_NNF_transformation,[status(thm)],[f1004])).
% 8.92/1.78 fof(f4425,plain,(
% 8.92/1.78 ![X0]: (~class_Rings_Ocomm__semiring__0(X0)|class_Groups_Ozero(X0))),
% 8.92/1.78 inference(cnf_transformation,[status(thm)],[f4424])).
% 8.92/1.78 fof(f4610,plain,(
% 8.92/1.78 ![T_1]: (~class_Rings_Ocomm__semiring__0(T_1)|class_Rings_Ocomm__semiring__0(tc_Polynomial_Opoly(T_1)))),
% 8.92/1.78 inference(pre_NNF_transformation,[status(thm)],[f1147])).
% 8.92/1.78 fof(f4611,plain,(
% 8.92/1.78 ![X0]: (~class_Rings_Ocomm__semiring__0(X0)|class_Rings_Ocomm__semiring__0(tc_Polynomial_Opoly(X0)))),
% 8.92/1.78 inference(cnf_transformation,[status(thm)],[f4610])).
% 8.92/1.78 fof(f4672,plain,(
% 8.92/1.78 ~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))),
% 8.92/1.78 inference(pre_NNF_transformation,[status(thm)],[f1180])).
% 8.92/1.78 fof(f4673,plain,(
% 8.92/1.78 ~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))),
% 8.92/1.78 inference(cnf_transformation,[status(thm)],[f4672])).
% 8.92/1.78 fof(f4674,plain,(
% 8.92/1.78 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))),
% 8.92/1.78 inference(cnf_transformation,[status(thm)],[f1181])).
% 8.92/1.78 fof(f4675,plain,(
% 8.92/1.78 ~c_Polynomial_OpCons(t_a,v_a,v_p)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),
% 8.92/1.78 inference(cnf_transformation,[status(thm)],[f1183])).
% 8.92/1.78 fof(f4676,plain,(
% 8.92/1.78 class_Rings_Ocomm__semiring__0(t_a)),
% 8.92/1.78 inference(cnf_transformation,[status(thm)],[f1184])).
% 8.92/1.78 fof(f4723,definition,(
% 8.92/1.78 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)))),
% 8.92/1.78 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 8.92/1.78 fof(f4726,definition,(
% 8.92/1.78 sQ1_spl <=> (v_p=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))),
% 8.92/1.78 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 8.92/1.78 fof(f4727,plain,(
% 8.92/1.78 v_p=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))|~sQ1_spl),
% 8.92/1.78 inference(component_clause,[status(thm)],[f4726])).
% 8.92/1.78 fof(f4729,plain,(
% 8.92/1.78 ~sQ0_spl|sQ1_spl),
% 8.92/1.78 inference(split_clause,[status(thm)],[f4673,f4723,f4726])).
% 8.92/1.78 fof(f4732,plain,(
% 8.92/1.78 ![X0,X1]: (~class_Groups_Ozero(X0)|c_Polynomial_Omonom(X0,c_Groups_Ozero__class_Ozero(X0),X1)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)))),
% 8.92/1.78 inference(destructive_equality_resolution,[status(thm)],[f1267])).
% 8.92/1.78 fof(f4734,plain,(
% 8.92/1.78 ![X0,X1,X2]: (~class_Groups_Ozero(X0)|hAPP(c_Polynomial_Ocoeff(X0,c_Polynomial_Omonom(X0,X1,X2)),X2)=X1)),
% 8.92/1.78 inference(destructive_equality_resolution,[status(thm)],[f1294])).
% 8.92/1.78 fof(f4948,plain,(
% 8.92/1.78 ![X0]: (hAPP(c_Polynomial_Opoly(t_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),X0)=c_Groups_Ozero__class_Ozero(t_a))),
% 8.92/1.78 inference(resolution,[status(thm)],[f1288,f4676])).
% 8.92/1.78 fof(f4951,plain,(
% 8.92/1.78 ![X0]: (c_Polynomial_Osynthetic__div(t_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)),X0)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))),
% 8.92/1.78 inference(resolution,[status(thm)],[f1291,f4676])).
% 8.92/1.78 fof(f4954,plain,(
% 8.92/1.78 ![X0]: (~hAPP(X0,sK0_skl(X0,c_Polynomial_Opoly(t_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))))=c_Groups_Ozero__class_Ozero(t_a)|X0=c_Polynomial_Opoly(t_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))))),
% 8.92/1.78 inference(paramodulation,[status(thm)],[f4948,f1187])).
% 8.92/1.78 fof(f4957,plain,(
% 8.92/1.78 ~c_Groups_Ozero__class_Ozero(t_a)=c_Groups_Ozero__class_Ozero(t_a)|c_Polynomial_Opoly(t_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))=c_Polynomial_Opoly(t_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))),
% 8.92/1.78 inference(paramodulation,[status(thm)],[f4948,f4954])).
% 8.92/1.78 fof(f4958,definition,(
% 8.92/1.78 sQ9_spl <=> (c_Groups_Ozero__class_Ozero(t_a)=c_Groups_Ozero__class_Ozero(t_a))),
% 8.92/1.78 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 8.92/1.78 fof(f4960,plain,(
% 8.92/1.78 ~c_Groups_Ozero__class_Ozero(t_a)=c_Groups_Ozero__class_Ozero(t_a)|sQ9_spl),
% 8.92/1.78 inference(component_clause,[status(thm)],[f4958])).
% 8.92/1.78 fof(f4961,definition,(
% 8.92/1.78 sQ10_spl <=> (c_Polynomial_Opoly(t_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))=c_Polynomial_Opoly(t_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))))),
% 8.92/1.78 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 8.92/1.78 fof(f4964,plain,(
% 8.92/1.78 ~sQ9_spl|sQ10_spl),
% 8.92/1.79 inference(split_clause,[status(thm)],[f4957,f4958,f4961])).
% 8.92/1.79 fof(f4965,plain,(
% 8.92/1.79 $false|sQ9_spl),
% 8.92/1.79 inference(trivial_equality_resolution,[status(thm)],[f4960])).
% 8.92/1.79 fof(f4966,plain,(
% 8.92/1.79 sQ9_spl),
% 8.92/1.79 inference(contradiction_clause,[status(thm)],[f4965])).
% 8.92/1.79 fof(f4983,plain,(
% 8.92/1.79 class_Groups_Ocomm__monoid__add(t_a)),
% 8.92/1.79 inference(resolution,[status(thm)],[f4413,f4676])).
% 8.92/1.79 fof(f5001,plain,(
% 8.92/1.79 ![X0]: (c_Polynomial_Osmult(t_a,c_Groups_Ozero__class_Ozero(t_a),X0)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))),
% 8.92/1.79 inference(resolution,[status(thm)],[f1307,f4676])).
% 8.92/1.79 fof(f5008,plain,(
% 8.92/1.79 class_Groups_Ozero(t_a)),
% 8.92/1.79 inference(resolution,[status(thm)],[f4425,f4676])).
% 8.92/1.79 fof(f5010,plain,(
% 8.92/1.79 ![X0,X1]: (hAPP(c_Polynomial_Ocoeff(t_a,c_Polynomial_Omonom(t_a,X0,X1)),X1)=X0)),
% 8.92/1.79 inference(resolution,[status(thm)],[f5008,f4734])).
% 8.92/1.79 fof(f5012,plain,(
% 8.92/1.79 ![X0]: (c_Polynomial_Omonom(t_a,c_Groups_Ozero__class_Ozero(t_a),X0)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))),
% 8.92/1.79 inference(resolution,[status(thm)],[f5008,f4732])).
% 8.92/1.79 fof(f5015,plain,(
% 8.92/1.79 ![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))))),
% 8.92/1.79 inference(resolution,[status(thm)],[f5008,f1260])).
% 8.92/1.79 fof(f5047,plain,(
% 8.92/1.79 ![X0,X1]: (~c_Polynomial_Ocoeff(t_a,X0)=c_Polynomial_Ocoeff(t_a,X1)|X0=X1)),
% 8.92/1.79 inference(resolution,[status(thm)],[f1322,f5008])).
% 8.92/1.79 fof(f5051,plain,(
% 8.92/1.79 ![X0]: (hAPP(c_Polynomial_Ocoeff(t_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),X0)=c_Groups_Ozero__class_Ozero(t_a))),
% 8.92/1.79 inference(paramodulation,[status(thm)],[f5012,f5010])).
% 8.92/1.79 fof(f5054,definition,(
% 8.92/1.79 sQ17_spl <=> (c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))),
% 8.92/1.79 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 8.92/1.79 fof(f5058,plain,(
% 8.92/1.79 c_Polynomial_Ocoeff(t_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))=c_Polynomial_Opoly(t_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))),
% 8.92/1.79 inference(resolution,[status(thm)],[f5051,f4954])).
% 8.92/1.79 fof(f5152,plain,(
% 8.92/1.79 ![X0]: (~c_Polynomial_Ocoeff(t_a,X0)=c_Polynomial_Opoly(t_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))|X0=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))),
% 8.92/1.79 inference(paramodulation,[status(thm)],[f5058,f5047])).
% 8.92/1.79 fof(f5204,plain,(
% 8.92/1.79 ~c_Polynomial_Opoly(t_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))=c_Polynomial_Opoly(t_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))|c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),
% 8.92/1.79 inference(paramodulation,[status(thm)],[f5058,f5152])).
% 8.92/1.79 fof(f5205,plain,(
% 8.92/1.79 ~sQ10_spl|sQ17_spl),
% 8.92/1.79 inference(split_clause,[status(thm)],[f5204,f4961,f5054])).
% 8.92/1.79 fof(f5307,plain,(
% 8.92/1.79 ![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))))),
% 8.92/1.79 inference(backward_demodulation,[status(thm)],[f2417,f5015])).
% 8.92/1.79 fof(f5313,plain,(
% 8.92/1.79 ![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)))),
% 8.92/1.79 inference(resolution,[status(thm)],[f1335,f4676])).
% 8.92/1.79 fof(f5730,plain,(
% 8.92/1.79 ![X0,X1]: (c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(t_a),X0,c_Polynomial_Osmult(t_a,X1,c_Polynomial_Osynthetic__div(t_a,X0,X1)))=c_Polynomial_OpCons(t_a,hAPP(c_Polynomial_Opoly(t_a,X0),X1),c_Polynomial_Osynthetic__div(t_a,X0,X1)))),
% 8.92/1.79 inference(resolution,[status(thm)],[f1361,f4676])).
% 8.92/1.79 fof(f5733,plain,(
% 8.92/1.79 ![X0,X1,X2,X3]: (~c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(t_a),X0,c_Polynomial_Osmult(t_a,X1,X2))=c_Polynomial_OpCons(t_a,X3,X2)|X3=hAPP(c_Polynomial_Opoly(t_a,X0),X1))),
% 8.92/1.79 inference(resolution,[status(thm)],[f1364,f4676])).
% 8.92/1.79 fof(f5737,plain,(
% 8.92/1.79 ![X0,X1,X2]: (~c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(t_a),X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))=c_Polynomial_OpCons(t_a,X1,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))|X1=hAPP(c_Polynomial_Opoly(t_a,X0),X2))),
% 8.92/1.79 inference(paramodulation,[status(thm)],[f5313,f5733])).
% 8.92/1.79 fof(f5742,plain,(
% 8.92/1.79 ![X0,X1,X2]: (~c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(t_a),X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))=c_Polynomial_Omonom(t_a,X1,c_HOL_Obool_Obool__size(c_fFalse))|X1=hAPP(c_Polynomial_Opoly(t_a,X0),X2))),
% 8.92/1.79 inference(forward_demodulation,[status(thm)],[f5307,f5737])).
% 8.92/1.79 fof(f6365,plain,(
% 8.92/1.79 class_Rings_Ocomm__semiring__0(tc_Polynomial_Opoly(t_a))),
% 8.92/1.79 inference(resolution,[status(thm)],[f4611,f4676])).
% 8.92/1.79 fof(f6426,plain,(
% 8.92/1.79 class_Groups_Ocomm__monoid__add(tc_Polynomial_Opoly(t_a))),
% 8.92/1.79 inference(resolution,[status(thm)],[f6365,f4413])).
% 8.92/1.79 fof(f6743,plain,(
% 8.92/1.79 ![X0]: (c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(t_a),X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))=X0)),
% 8.92/1.79 inference(resolution,[status(thm)],[f1410,f6426])).
% 8.92/1.79 fof(f6745,plain,(
% 8.92/1.79 ![X0]: (c_Groups_Oplus__class_Oplus(t_a,X0,c_Groups_Ozero__class_Ozero(t_a))=X0)),
% 8.92/1.79 inference(resolution,[status(thm)],[f1410,f4983])).
% 8.92/1.79 fof(f6821,plain,(
% 8.92/1.79 ![X0]: (c_Groups_Oplus__class_Oplus(t_a,c_Groups_Ozero__class_Ozero(t_a),X0)=X0)),
% 8.92/1.79 inference(resolution,[status(thm)],[f1421,f4983])).
% 8.92/1.79 fof(f6918,plain,(
% 8.92/1.79 ![X0,X1,X2]: (c_Polynomial_Osmult(t_a,X0,c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(t_a),X1,X2))=c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(t_a),c_Polynomial_Osmult(t_a,X0,X1),c_Polynomial_Osmult(t_a,X0,X2)))),
% 8.92/1.79 inference(resolution,[status(thm)],[f1433,f4676])).
% 8.92/1.79 fof(f6923,plain,(
% 8.92/1.79 ![X0,X1,X2]: (~X0=c_Polynomial_Omonom(t_a,X1,c_HOL_Obool_Obool__size(c_fFalse))|X1=hAPP(c_Polynomial_Opoly(t_a,X0),X2))),
% 8.92/1.79 inference(backward_demodulation,[status(thm)],[f6743,f5742])).
% 8.92/1.79 fof(f6927,plain,(
% 8.92/1.79 ![X0,X1]: (X0=hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_Omonom(t_a,X0,c_HOL_Obool_Obool__size(c_fFalse))),X1))),
% 8.92/1.79 inference(destructive_equality_resolution,[status(thm)],[f6923])).
% 8.92/1.79 fof(f6930,plain,(
% 8.92/1.79 ![X0,X1]: (c_Polynomial_Osmult(t_a,X0,c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(t_a),X1,c_Polynomial_Osynthetic__div(t_a,c_Polynomial_Osmult(t_a,X0,X1),X0)))=c_Polynomial_OpCons(t_a,hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_Osmult(t_a,X0,X1)),X0),c_Polynomial_Osynthetic__div(t_a,c_Polynomial_Osmult(t_a,X0,X1),X0)))),
% 8.92/1.79 inference(paramodulation,[status(thm)],[f5730,f6918])).
% 8.92/1.79 fof(f7147,plain,(
% 8.92/1.79 ![X0,X1,X2]: (hAPP(c_Polynomial_Opoly(t_a,c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,X0,X1)),X2)=hAPP(c_Polynomial_Opoly(t_a,X0),c_Groups_Oplus__class_Oplus(t_a,X1,X2)))),
% 8.92/1.79 inference(resolution,[status(thm)],[f1436,f4676])).
% 8.92/1.79 fof(f7159,plain,(
% 8.92/1.79 ![X0,X1,X2]: (~c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(t_a),c_Polynomial_Osmult(t_a,X0,X1),c_Polynomial_OpCons(t_a,X2,X1))=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))|X1=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))),
% 8.92/1.79 inference(resolution,[status(thm)],[f1439,f4676])).
% 8.92/1.79 fof(f7171,plain,(
% 8.92/1.79 ![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))))),
% 8.92/1.79 inference(resolution,[status(thm)],[f1450,f4676])).
% 8.92/1.79 fof(f7175,plain,(
% 8.92/1.79 ![X0]: (hAPP(c_Polynomial_Opoly(t_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),X0)=hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,v_a,v_p)),c_Groups_Oplus__class_Oplus(t_a,v_h,X0)))),
% 8.92/1.79 inference(paramodulation,[status(thm)],[f4674,f7147])).
% 8.92/1.79 fof(f7191,plain,(
% 8.92/1.79 ![X0]: (c_Groups_Ozero__class_Ozero(t_a)=hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,v_a,v_p)),c_Groups_Oplus__class_Oplus(t_a,v_h,X0)))),
% 8.92/1.79 inference(forward_demodulation,[status(thm)],[f4948,f7175])).
% 8.92/1.79 fof(f7230,plain,(
% 8.92/1.79 ![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)))),
% 8.92/1.79 inference(paramodulation,[status(thm)],[f7171,f7159])).
% 8.92/1.79 fof(f7817,plain,(
% 8.92/1.79 ![X0,X1,X2]: (hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,X0,X1)),X2)=c_Groups_Oplus__class_Oplus(t_a,X0,hAPP(hAPP(c_Groups_Otimes__class_Otimes(t_a),X2),hAPP(c_Polynomial_Opoly(t_a,X1),X2))))),
% 8.92/1.79 inference(resolution,[status(thm)],[f1485,f4676])).
% 8.92/1.79 fof(f7842,plain,(
% 8.92/1.79 ![X0,X1]: (hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))),X1)=c_Groups_Oplus__class_Oplus(t_a,X0,hAPP(hAPP(c_Groups_Otimes__class_Otimes(t_a),X1),c_Groups_Ozero__class_Ozero(t_a))))),
% 8.92/1.79 inference(paramodulation,[status(thm)],[f4948,f7817])).
% 8.92/1.79 fof(f7851,plain,(
% 8.92/1.79 ![X0,X1]: (hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_Omonom(t_a,X0,c_HOL_Obool_Obool__size(c_fFalse))),X1)=c_Groups_Oplus__class_Oplus(t_a,X0,hAPP(hAPP(c_Groups_Otimes__class_Otimes(t_a),X1),c_Groups_Ozero__class_Ozero(t_a))))),
% 8.92/1.79 inference(forward_demodulation,[status(thm)],[f5307,f7842])).
% 8.92/1.79 fof(f7852,plain,(
% 8.92/1.79 ![X0,X1]: (X0=c_Groups_Oplus__class_Oplus(t_a,X0,hAPP(hAPP(c_Groups_Otimes__class_Otimes(t_a),X1),c_Groups_Ozero__class_Ozero(t_a))))),
% 8.92/1.79 inference(forward_demodulation,[status(thm)],[f6927,f7851])).
% 8.92/1.79 fof(f8007,plain,(
% 8.92/1.79 ![X0]: (c_Groups_Ozero__class_Ozero(t_a)=hAPP(hAPP(c_Groups_Otimes__class_Otimes(t_a),X0),c_Groups_Ozero__class_Ozero(t_a)))),
% 8.92/1.79 inference(paramodulation,[status(thm)],[f6821,f7852])).
% 8.92/1.79 fof(f9392,plain,(
% 8.92/1.79 c_Groups_Ozero__class_Ozero(t_a)=hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,v_a,v_p)),v_h)),
% 8.92/1.79 inference(paramodulation,[status(thm)],[f6745,f7191])).
% 8.92/1.79 fof(f11024,plain,(
% 8.92/1.79 c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,v_p,v_h)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),
% 8.92/1.79 inference(resolution,[status(thm)],[f7230,f4674])).
% 8.92/1.79 fof(f11025,plain,(
% 8.92/1.79 ~c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(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))),
% 8.92/1.79 inference(paramodulation,[status(thm)],[f4674,f7230])).
% 8.92/1.79 fof(f11037,plain,(
% 8.92/1.79 ~sQ17_spl|sQ0_spl),
% 8.92/1.79 inference(split_clause,[status(thm)],[f11025,f5054,f4723])).
% 8.92/1.79 fof(f11052,plain,(
% 8.92/1.79 ![X0]: (hAPP(c_Polynomial_Opoly(t_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),X0)=hAPP(c_Polynomial_Opoly(t_a,v_p),c_Groups_Oplus__class_Oplus(t_a,v_h,X0)))),
% 8.92/1.79 inference(paramodulation,[status(thm)],[f11024,f7147])).
% 8.92/1.79 fof(f11080,plain,(
% 8.92/1.79 ![X0]: (c_Groups_Ozero__class_Ozero(t_a)=hAPP(c_Polynomial_Opoly(t_a,v_p),c_Groups_Oplus__class_Oplus(t_a,v_h,X0)))),
% 8.92/1.79 inference(forward_demodulation,[status(thm)],[f4948,f11052])).
% 8.92/1.79 fof(f11083,plain,(
% 8.92/1.79 c_Groups_Ozero__class_Ozero(t_a)=hAPP(c_Polynomial_Opoly(t_a,v_p),v_h)),
% 8.92/1.79 inference(paramodulation,[status(thm)],[f6745,f11080])).
% 8.92/1.79 fof(f11142,plain,(
% 8.92/1.79 ![X0]: (hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,X0,v_p)),v_h)=c_Groups_Oplus__class_Oplus(t_a,X0,hAPP(hAPP(c_Groups_Otimes__class_Otimes(t_a),v_h),c_Groups_Ozero__class_Ozero(t_a))))),
% 8.92/1.79 inference(paramodulation,[status(thm)],[f11083,f7817])).
% 8.92/1.79 fof(f11157,plain,(
% 8.92/1.79 ![X0]: (hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,X0,v_p)),v_h)=c_Groups_Oplus__class_Oplus(t_a,X0,c_Groups_Ozero__class_Ozero(t_a)))),
% 8.92/1.79 inference(forward_demodulation,[status(thm)],[f8007,f11142])).
% 8.92/1.79 fof(f11158,plain,(
% 8.92/1.79 ![X0]: (hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,X0,v_p)),v_h)=X0)),
% 8.92/1.79 inference(forward_demodulation,[status(thm)],[f6745,f11157])).
% 8.92/1.79 fof(f11165,plain,(
% 8.92/1.79 c_Groups_Ozero__class_Ozero(t_a)=v_a),
% 8.92/1.79 inference(backward_demodulation,[status(thm)],[f11158,f9392])).
% 8.92/1.79 fof(f11221,plain,(
% 8.92/1.79 ![X0]: (hAPP(c_Polynomial_Opoly(t_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),X0)=v_a)),
% 8.92/1.79 inference(backward_demodulation,[status(thm)],[f11165,f4948])).
% 8.92/1.79 fof(f11225,plain,(
% 8.92/1.79 ![X0]: (c_Polynomial_Osmult(t_a,v_a,X0)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))),
% 8.92/1.79 inference(backward_demodulation,[status(thm)],[f11165,f5001])).
% 8.92/1.79 fof(f11325,plain,(
% 8.92/1.79 ![X0]: (c_Polynomial_Osynthetic__div(t_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)),X0)=v_p|~sQ1_spl)),
% 4.98/1.83 inference(backward_demodulation,[status(thm)],[f4727,f4951])).
% 4.98/1.83 fof(f11329,plain,(
% 4.98/1.83 ~c_Polynomial_OpCons(t_a,v_a,v_p)=v_p|~sQ1_spl),
% 4.98/1.83 inference(backward_demodulation,[status(thm)],[f4727,f4675])).
% 4.98/1.83 fof(f11349,plain,(
% 4.98/1.83 ![X0]: (c_Polynomial_Osynthetic__div(t_a,v_p,X0)=v_p|~sQ1_spl)),
% 4.98/1.83 inference(forward_demodulation,[status(thm)],[f4727,f11325])).
% 4.98/1.83 fof(f11599,plain,(
% 4.98/1.83 ![X0]: (hAPP(c_Polynomial_Opoly(t_a,v_p),X0)=v_a|~sQ1_spl)),
% 4.98/1.83 inference(forward_demodulation,[status(thm)],[f4727,f11221])).
% 4.98/1.83 fof(f11760,plain,(
% 4.98/1.83 ![X0]: (c_Polynomial_Osmult(t_a,v_a,X0)=v_p|~sQ1_spl)),
% 4.98/1.83 inference(forward_demodulation,[status(thm)],[f4727,f11225])).
% 4.98/1.83 fof(f11775,plain,(
% 4.98/1.83 ![X0]: (c_Polynomial_Osmult(t_a,v_a,c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(t_a),X0,c_Polynomial_Osynthetic__div(t_a,c_Polynomial_Osmult(t_a,v_a,X0),v_a)))=c_Polynomial_OpCons(t_a,hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_Osmult(t_a,v_a,X0)),v_a),c_Polynomial_Osynthetic__div(t_a,v_p,v_a))|~sQ1_spl)),
% 4.98/1.83 inference(paramodulation,[status(thm)],[f11760,f6930])).
% 4.98/1.83 fof(f11799,plain,(
% 4.98/1.83 ![X0]: (v_p=c_Polynomial_OpCons(t_a,hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_Osmult(t_a,v_a,X0)),v_a),c_Polynomial_Osynthetic__div(t_a,v_p,v_a))|~sQ1_spl)),
% 4.98/1.83 inference(forward_demodulation,[status(thm)],[f11760,f11775])).
% 4.98/1.83 fof(f11800,plain,(
% 4.98/1.83 v_p=c_Polynomial_OpCons(t_a,hAPP(c_Polynomial_Opoly(t_a,v_p),v_a),c_Polynomial_Osynthetic__div(t_a,v_p,v_a))|~sQ1_spl),
% 4.98/1.83 inference(forward_demodulation,[status(thm)],[f11760,f11799])).
% 4.98/1.83 fof(f11801,plain,(
% 4.98/1.83 v_p=c_Polynomial_OpCons(t_a,v_a,c_Polynomial_Osynthetic__div(t_a,v_p,v_a))|~sQ1_spl),
% 4.98/1.83 inference(forward_demodulation,[status(thm)],[f11599,f11800])).
% 4.98/1.83 fof(f11802,plain,(
% 4.98/1.83 v_p=c_Polynomial_OpCons(t_a,v_a,v_p)|~sQ1_spl),
% 4.98/1.83 inference(forward_demodulation,[status(thm)],[f11349,f11801])).
% 4.98/1.83 fof(f11803,plain,(
% 4.98/1.83 $false|~sQ1_spl),
% 4.98/1.83 inference(forward_subsumption_resolution,[status(thm)],[f11802,f11329])).
% 4.98/1.83 fof(f11804,plain,(
% 4.98/1.83 ~sQ1_spl),
% 4.98/1.83 inference(contradiction_clause,[status(thm)],[f11803])).
% 4.98/1.83 fof(f11805,plain,(
% 4.98/1.83 $false),
% 4.98/1.83 inference(sat_refutation,[status(thm)],[f4729,f4964,f4966,f5205,f11037,f11804])).
% 4.98/1.83 % SZS output end CNFRefutation for theBenchmark.p
% 4.98/1.85 % Elapsed time: 1.375019 seconds
% 4.98/1.85 % CPU time: 9.600355 seconds
% 4.98/1.85 % Total memory used: 309.553 MB
% 4.98/1.85 % Net memory used: 305.418 MB
%------------------------------------------------------------------------------