%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW269+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 : n015.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:53 PM UTC 2026
% Result : Theorem 37.63s 5.24s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW269+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.34 % Computer : n015.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Mon Sep 21 09:47:50 UTC 2026
% 0.08/0.34 % CPUTime :
% 0.13/0.44 % Drodi V4.1.1
% 37.63/5.24 % Refutation found
% 37.63/5.24 % SZS status Theorem for theBenchmark: Theorem is valid
% 37.63/5.24 % SZS output start CNFRefutation for theBenchmark
% 37.63/5.24 fof(f1,axiom,(
% 37.63/5.24 (! [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 ) )),
% 37.63/5.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 37.63/5.24 fof(f2,axiom,(
% 37.63/5.24 v_d____ = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
% 37.63/5.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 37.63/5.24 fof(f3,axiom,(
% 37.63/5.24 (! [B_w] :( B_w != c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)=> hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____)),B_w) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) ) )),
% 37.63/5.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 37.63/5.24 fof(f15,axiom,(
% 37.63/5.24 (! [V_q_2,V_pa_2,T_a] :( ( class_Int_Oring__char__0(T_a)& class_Rings_Oidom(T_a) )=> ( c_Polynomial_Opoly(T_a,V_pa_2) = c_Polynomial_Opoly(T_a,V_q_2)<=> V_pa_2 = V_q_2 ) ) )),
% 37.63/5.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 37.63/5.24 fof(f17,axiom,(
% 37.63/5.24 (! [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) ) )),
% 37.63/5.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 37.63/5.24 fof(f21,axiom,(
% 37.63/5.24 (! [V_a_2,V_pa_2,T_a] :( class_Rings_Oidom(T_a)=> ( hAPP(c_Polynomial_Opoly(T_a,V_pa_2),V_a_2) = c_Groups_Ozero__class_Ozero(T_a)<=> ( V_pa_2 = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))| c_Polynomial_Oorder(T_a,V_a_2,V_pa_2) != c_Groups_Ozero__class_Ozero(tc_Nat_Onat) ) ) ) )),
% 37.63/5.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 37.63/5.24 fof(f29,axiom,(
% 37.63/5.24 (! [V_n_2,V_a_2,T_a] :( class_Groups_Ozero(T_a)=> ( c_Polynomial_Omonom(T_a,V_a_2,V_n_2) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))<=> V_a_2 = c_Groups_Ozero__class_Ozero(T_a) ) ) )),
% 37.63/5.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 37.63/5.24 fof(f43,axiom,(
% 37.63/5.24 (! [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) ) ) ) )),
% 37.63/5.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 37.63/5.24 fof(f68,axiom,(
% 37.63/5.24 (! [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 ) )),
% 37.63/5.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 37.63/5.24 fof(f81,axiom,(
% 37.63/5.24 (! [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) ) ) ) )),
% 37.63/5.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 37.63/5.24 fof(f85,axiom,(
% 37.63/5.24 (! [V_pa_2,V_a_2,T_a] :( class_Rings_Oidom(T_a)=> ( c_Polynomial_Osmult(T_a,V_a_2,V_pa_2) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))<=> ( V_a_2 = c_Groups_Ozero__class_Ozero(T_a)| V_pa_2 = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)) ) ) ) )),
% 37.63/5.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 37.63/5.24 fof(f118,axiom,(
% 37.63/5.24 (! [V_n] : c_Nat_OSuc(V_n) != V_n )),
% 37.63/5.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 37.63/5.24 fof(f296,axiom,(
% 37.63/5.24 c_HOL_Obool_Obool__size(c_fFalse) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat) ),
% 37.63/5.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 37.63/5.24 fof(f297,axiom,(
% 37.63/5.24 c_HOL_Obool_Obool__size(c_fTrue) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat) ),
% 37.63/5.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 37.63/5.24 fof(f1069,axiom,(
% 37.63/5.24 class_Groups_Ocomm__monoid__add(tc_Complex_Ocomplex) ),
% 37.63/5.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 37.63/5.24 fof(f1071,axiom,(
% 37.63/5.24 class_Rings_Ocomm__semiring__0(tc_Complex_Ocomplex) ),
% 37.63/5.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 37.63/5.24 fof(f1084,axiom,(
% 37.63/5.24 class_Int_Oring__char__0(tc_Complex_Ocomplex) ),
% 37.63/5.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 37.63/5.24 fof(f1090,axiom,(
% 37.63/5.24 class_Groups_Ozero(tc_Complex_Ocomplex) ),
% 37.63/5.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 37.63/5.24 fof(f1092,axiom,(
% 37.63/5.24 class_Rings_Oidom(tc_Complex_Ocomplex) ),
% 37.63/5.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 37.63/5.24 fof(f1121,axiom,(
% 37.63/5.24 (! [T_1] :( class_Groups_Ocomm__monoid__add(T_1)=> class_Groups_Ocomm__monoid__add(tc_Polynomial_Opoly(T_1)) ) )),
% 37.63/5.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 37.63/5.24 fof(f1159,conjecture,(
% 37.63/5.24 c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
% 37.63/5.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 37.63/5.24 fof(f1160,negated_conjecture,(
% 37.63/5.24 ~(c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) )),
% 37.63/5.24 inference(negated_conjecture,[status(cth)],[f1159])).
% 37.63/5.24 fof(f1161,plain,(
% 37.63/5.24 ![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)),
% 37.63/5.24 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 37.63/5.24 fof(f1162,plain,(
% 37.63/5.24 ![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)),
% 37.63/5.24 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(B_x,sK0_skl(V_f_2,V_g_2))],[f1161])).
% 37.63/5.24 fof(f1163,plain,(
% 37.63/5.24 ![X0,X1]: (~hAPP(X0,sK0_skl(X0,X1))=hAPP(X1,sK0_skl(X0,X1))|X0=X1)),
% 37.63/5.24 inference(cnf_transformation,[status(thm)],[f1162])).
% 37.63/5.24 fof(f1164,plain,(
% 37.63/5.24 v_d____=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)),
% 37.63/5.24 inference(cnf_transformation,[status(thm)],[f2])).
% 37.63/5.24 fof(f1165,plain,(
% 37.63/5.24 ![B_w]: (B_w=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)|hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____)),B_w)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex))),
% 37.63/5.24 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 37.63/5.24 fof(f1166,plain,(
% 37.63/5.24 ![X0]: (X0=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)|hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____)),X0)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex))),
% 37.63/5.24 inference(cnf_transformation,[status(thm)],[f1165])).
% 37.63/5.24 fof(f1205,plain,(
% 37.63/5.24 ![V_q_2,V_pa_2,T_a]: ((~class_Int_Oring__char__0(T_a)|~class_Rings_Oidom(T_a))|(c_Polynomial_Opoly(T_a,V_pa_2)=c_Polynomial_Opoly(T_a,V_q_2)<=>V_pa_2=V_q_2))),
% 37.63/5.24 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 37.63/5.24 fof(f1206,plain,(
% 37.63/5.24 ![V_q_2,V_pa_2,T_a]: ((~class_Int_Oring__char__0(T_a)|~class_Rings_Oidom(T_a))|((~c_Polynomial_Opoly(T_a,V_pa_2)=c_Polynomial_Opoly(T_a,V_q_2)|V_pa_2=V_q_2)&(c_Polynomial_Opoly(T_a,V_pa_2)=c_Polynomial_Opoly(T_a,V_q_2)|~V_pa_2=V_q_2)))),
% 37.63/5.24 inference(NNF_transformation,[status(thm)],[f1205])).
% 37.63/5.24 fof(f1207,plain,(
% 37.63/5.24 ![T_a]: ((~class_Int_Oring__char__0(T_a)|~class_Rings_Oidom(T_a))|((![V_q_2,V_pa_2]: (~c_Polynomial_Opoly(T_a,V_pa_2)=c_Polynomial_Opoly(T_a,V_q_2)|V_pa_2=V_q_2))&(![V_q_2,V_pa_2]: (c_Polynomial_Opoly(T_a,V_pa_2)=c_Polynomial_Opoly(T_a,V_q_2)|~V_pa_2=V_q_2))))),
% 37.63/5.24 inference(miniscoping,[status(thm)],[f1206])).
% 37.63/5.24 fof(f1208,plain,(
% 37.63/5.24 ![X0,X1,X2]: (~class_Int_Oring__char__0(X0)|~class_Rings_Oidom(X0)|~c_Polynomial_Opoly(X0,X1)=c_Polynomial_Opoly(X0,X2)|X1=X2)),
% 37.63/5.24 inference(cnf_transformation,[status(thm)],[f1207])).
% 37.63/5.24 fof(f1215,plain,(
% 37.63/5.24 ![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))),
% 37.63/5.24 inference(pre_NNF_transformation,[status(thm)],[f17])).
% 37.63/5.24 fof(f1216,plain,(
% 37.63/5.24 ![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)))),
% 37.63/5.24 inference(miniscoping,[status(thm)],[f1215])).
% 37.63/5.24 fof(f1217,plain,(
% 37.63/5.24 ![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))),
% 37.63/5.24 inference(cnf_transformation,[status(thm)],[f1216])).
% 37.63/5.24 fof(f1228,plain,(
% 37.63/5.24 ![V_a_2,V_pa_2,T_a]: (~class_Rings_Oidom(T_a)|(hAPP(c_Polynomial_Opoly(T_a,V_pa_2),V_a_2)=c_Groups_Ozero__class_Ozero(T_a)<=>(V_pa_2=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))|~c_Polynomial_Oorder(T_a,V_a_2,V_pa_2)=c_Groups_Ozero__class_Ozero(tc_Nat_Onat))))),
% 37.63/5.24 inference(pre_NNF_transformation,[status(thm)],[f21])).
% 37.63/5.24 fof(f1229,plain,(
% 37.63/5.24 ![V_a_2,V_pa_2,T_a]: (~class_Rings_Oidom(T_a)|((~hAPP(c_Polynomial_Opoly(T_a,V_pa_2),V_a_2)=c_Groups_Ozero__class_Ozero(T_a)|(V_pa_2=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))|~c_Polynomial_Oorder(T_a,V_a_2,V_pa_2)=c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))&(hAPP(c_Polynomial_Opoly(T_a,V_pa_2),V_a_2)=c_Groups_Ozero__class_Ozero(T_a)|(~V_pa_2=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))&c_Polynomial_Oorder(T_a,V_a_2,V_pa_2)=c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))))),
% 37.63/5.24 inference(NNF_transformation,[status(thm)],[f1228])).
% 37.63/5.24 fof(f1230,plain,(
% 37.63/5.24 ![T_a]: (~class_Rings_Oidom(T_a)|((![V_a_2,V_pa_2]: (~hAPP(c_Polynomial_Opoly(T_a,V_pa_2),V_a_2)=c_Groups_Ozero__class_Ozero(T_a)|(V_pa_2=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))|~c_Polynomial_Oorder(T_a,V_a_2,V_pa_2)=c_Groups_Ozero__class_Ozero(tc_Nat_Onat))))&(![V_a_2,V_pa_2]: (hAPP(c_Polynomial_Opoly(T_a,V_pa_2),V_a_2)=c_Groups_Ozero__class_Ozero(T_a)|(~V_pa_2=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))&c_Polynomial_Oorder(T_a,V_a_2,V_pa_2)=c_Groups_Ozero__class_Ozero(tc_Nat_Onat))))))),
% 37.63/5.24 inference(miniscoping,[status(thm)],[f1229])).
% 37.63/5.24 fof(f1231,plain,(
% 37.63/5.24 ![X0,X1,X2]: (~class_Rings_Oidom(X0)|~hAPP(c_Polynomial_Opoly(X0,X1),X2)=c_Groups_Ozero__class_Ozero(X0)|X1=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X0))|~c_Polynomial_Oorder(X0,X2,X1)=c_Groups_Ozero__class_Ozero(tc_Nat_Onat))),
% 37.63/5.24 inference(cnf_transformation,[status(thm)],[f1230])).
% 37.63/5.24 fof(f1233,plain,(
% 37.63/5.24 ![X0,X1,X2]: (~class_Rings_Oidom(X0)|hAPP(c_Polynomial_Opoly(X0,X1),X2)=c_Groups_Ozero__class_Ozero(X0)|c_Polynomial_Oorder(X0,X2,X1)=c_Groups_Ozero__class_Ozero(tc_Nat_Onat))),
% 37.63/5.24 inference(cnf_transformation,[status(thm)],[f1230])).
% 37.63/5.24 fof(f1253,plain,(
% 37.63/5.24 ![V_n_2,V_a_2,T_a]: (~class_Groups_Ozero(T_a)|(c_Polynomial_Omonom(T_a,V_a_2,V_n_2)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))<=>V_a_2=c_Groups_Ozero__class_Ozero(T_a)))),
% 37.63/5.24 inference(pre_NNF_transformation,[status(thm)],[f29])).
% 37.63/5.24 fof(f1254,plain,(
% 37.63/5.24 ![V_n_2,V_a_2,T_a]: (~class_Groups_Ozero(T_a)|((~c_Polynomial_Omonom(T_a,V_a_2,V_n_2)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))|V_a_2=c_Groups_Ozero__class_Ozero(T_a))&(c_Polynomial_Omonom(T_a,V_a_2,V_n_2)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))|~V_a_2=c_Groups_Ozero__class_Ozero(T_a))))),
% 37.63/5.24 inference(NNF_transformation,[status(thm)],[f1253])).
% 37.63/5.24 fof(f1255,plain,(
% 37.63/5.24 ![T_a]: (~class_Groups_Ozero(T_a)|((![V_a_2]: ((![V_n_2]: ~c_Polynomial_Omonom(T_a,V_a_2,V_n_2)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)))|V_a_2=c_Groups_Ozero__class_Ozero(T_a)))&(![V_a_2]: ((![V_n_2]: c_Polynomial_Omonom(T_a,V_a_2,V_n_2)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)))|~V_a_2=c_Groups_Ozero__class_Ozero(T_a)))))),
% 37.63/5.24 inference(miniscoping,[status(thm)],[f1254])).
% 37.63/5.24 fof(f1257,plain,(
% 37.63/5.24 ![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))),
% 37.63/5.24 inference(cnf_transformation,[status(thm)],[f1255])).
% 37.63/5.24 fof(f1311,plain,(
% 37.63/5.24 ![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))))),
% 37.63/5.24 inference(pre_NNF_transformation,[status(thm)],[f43])).
% 37.63/5.24 fof(f1312,plain,(
% 37.63/5.24 ![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))))))),
% 37.63/5.24 inference(miniscoping,[status(thm)],[f1311])).
% 37.63/5.24 fof(f1314,plain,(
% 37.63/5.24 ![X0,X1,X2,X3]: (~class_Groups_Ozero(X0)|X1=X2|hAPP(c_Polynomial_Ocoeff(X0,c_Polynomial_Omonom(X0,X3,X1)),X2)=c_Groups_Ozero__class_Ozero(X0))),
% 37.63/5.24 inference(cnf_transformation,[status(thm)],[f1312])).
% 37.63/5.24 fof(f1404,plain,(
% 37.63/5.24 ![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)),
% 37.63/5.24 inference(pre_NNF_transformation,[status(thm)],[f68])).
% 37.63/5.24 fof(f1405,plain,(
% 37.63/5.24 ![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))),
% 37.63/5.24 inference(miniscoping,[status(thm)],[f1404])).
% 37.63/5.24 fof(f1406,plain,(
% 37.63/5.24 ![X0,X1]: (~class_Groups_Ocomm__monoid__add(X0)|c_Groups_Oplus__class_Oplus(X0,X1,c_Groups_Ozero__class_Ozero(X0))=X1)),
% 37.63/5.24 inference(cnf_transformation,[status(thm)],[f1405])).
% 37.63/5.24 fof(f1447,plain,(
% 37.63/5.24 ![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))))),
% 37.63/5.24 inference(pre_NNF_transformation,[status(thm)],[f81])).
% 37.63/5.24 fof(f1448,plain,(
% 37.63/5.24 ![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)))))),
% 37.63/5.24 inference(miniscoping,[status(thm)],[f1447])).
% 37.63/5.24 fof(f1449,plain,(
% 37.63/5.24 ![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))),
% 37.63/5.24 inference(cnf_transformation,[status(thm)],[f1448])).
% 37.63/5.24 fof(f1458,plain,(
% 37.63/5.24 ![V_pa_2,V_a_2,T_a]: (~class_Rings_Oidom(T_a)|(c_Polynomial_Osmult(T_a,V_a_2,V_pa_2)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))<=>(V_a_2=c_Groups_Ozero__class_Ozero(T_a)|V_pa_2=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)))))),
% 37.63/5.24 inference(pre_NNF_transformation,[status(thm)],[f85])).
% 37.63/5.24 fof(f1459,plain,(
% 37.63/5.24 ![V_pa_2,V_a_2,T_a]: (~class_Rings_Oidom(T_a)|((~c_Polynomial_Osmult(T_a,V_a_2,V_pa_2)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))|(V_a_2=c_Groups_Ozero__class_Ozero(T_a)|V_pa_2=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))))&(c_Polynomial_Osmult(T_a,V_a_2,V_pa_2)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))|(~V_a_2=c_Groups_Ozero__class_Ozero(T_a)&~V_pa_2=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))))))),
% 37.63/5.24 inference(NNF_transformation,[status(thm)],[f1458])).
% 37.63/5.24 fof(f1460,plain,(
% 37.63/5.24 ![T_a]: (~class_Rings_Oidom(T_a)|((![V_pa_2,V_a_2]: (~c_Polynomial_Osmult(T_a,V_a_2,V_pa_2)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))|(V_a_2=c_Groups_Ozero__class_Ozero(T_a)|V_pa_2=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)))))&(![V_pa_2,V_a_2]: (c_Polynomial_Osmult(T_a,V_a_2,V_pa_2)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))|(~V_a_2=c_Groups_Ozero__class_Ozero(T_a)&~V_pa_2=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)))))))),
% 37.63/5.24 inference(miniscoping,[status(thm)],[f1459])).
% 37.63/5.24 fof(f1462,plain,(
% 37.63/5.24 ![X0,X1,X2]: (~class_Rings_Oidom(X0)|c_Polynomial_Osmult(X0,X1,X2)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X0))|~X1=c_Groups_Ozero__class_Ozero(X0))),
% 37.63/5.24 inference(cnf_transformation,[status(thm)],[f1460])).
% 37.63/5.24 fof(f1550,plain,(
% 37.63/5.24 ![X0]: (~c_Nat_OSuc(X0)=X0)),
% 37.63/5.24 inference(cnf_transformation,[status(thm)],[f118])).
% 37.63/5.24 fof(f2097,plain,(
% 37.63/5.24 c_HOL_Obool_Obool__size(c_fFalse)=c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
% 37.63/5.24 inference(cnf_transformation,[status(thm)],[f296])).
% 37.63/5.24 fof(f2098,plain,(
% 37.63/5.24 c_HOL_Obool_Obool__size(c_fTrue)=c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
% 37.63/5.24 inference(cnf_transformation,[status(thm)],[f297])).
% 37.63/5.24 fof(f4636,plain,(
% 37.63/5.24 class_Groups_Ocomm__monoid__add(tc_Complex_Ocomplex)),
% 37.63/5.24 inference(cnf_transformation,[status(thm)],[f1069])).
% 37.63/5.24 fof(f4638,plain,(
% 37.63/5.24 class_Rings_Ocomm__semiring__0(tc_Complex_Ocomplex)),
% 37.63/5.24 inference(cnf_transformation,[status(thm)],[f1071])).
% 37.63/5.24 fof(f4651,plain,(
% 37.63/5.24 class_Int_Oring__char__0(tc_Complex_Ocomplex)),
% 37.63/5.24 inference(cnf_transformation,[status(thm)],[f1084])).
% 37.63/5.24 fof(f4657,plain,(
% 37.63/5.24 class_Groups_Ozero(tc_Complex_Ocomplex)),
% 37.63/5.24 inference(cnf_transformation,[status(thm)],[f1090])).
% 37.63/5.24 fof(f4659,plain,(
% 37.63/5.24 class_Rings_Oidom(tc_Complex_Ocomplex)),
% 37.63/5.24 inference(cnf_transformation,[status(thm)],[f1092])).
% 37.63/5.24 fof(f4713,plain,(
% 37.63/5.24 ![T_1]: (~class_Groups_Ocomm__monoid__add(T_1)|class_Groups_Ocomm__monoid__add(tc_Polynomial_Opoly(T_1)))),
% 37.63/5.24 inference(pre_NNF_transformation,[status(thm)],[f1121])).
% 37.63/5.24 fof(f4714,plain,(
% 37.63/5.24 ![X0]: (~class_Groups_Ocomm__monoid__add(X0)|class_Groups_Ocomm__monoid__add(tc_Polynomial_Opoly(X0)))),
% 37.63/5.24 inference(cnf_transformation,[status(thm)],[f4713])).
% 37.63/5.24 fof(f4785,plain,(
% 37.63/5.24 ~c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))),
% 37.63/5.24 inference(cnf_transformation,[status(thm)],[f1160])).
% 37.63/5.24 fof(f4843,plain,(
% 37.63/5.24 ![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)))),
% 37.63/5.24 inference(destructive_equality_resolution,[status(thm)],[f1257])).
% 37.63/5.24 fof(f4852,plain,(
% 37.63/5.24 ![X0,X1]: (~class_Rings_Oidom(X0)|c_Polynomial_Osmult(X0,c_Groups_Ozero__class_Ozero(X0),X1)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)))),
% 37.63/5.24 inference(destructive_equality_resolution,[status(thm)],[f1462])).
% 37.63/5.24 fof(f5005,plain,(
% 37.63/5.24 ![X0]: (X0=v_d____|hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____)),X0)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex))),
% 37.63/5.24 inference(forward_demodulation,[status(thm)],[f1164,f1166])).
% 37.63/5.24 fof(f5006,plain,(
% 37.63/5.24 ![X0]: (X0=v_d____|hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____)),X0)=v_d____)),
% 37.63/5.24 inference(forward_demodulation,[status(thm)],[f1164,f5005])).
% 37.63/5.24 fof(f5008,plain,(
% 37.63/5.24 ![X0]: (~hAPP(X0,sK0_skl(X0,c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____))))=v_d____|X0=c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____))|sK0_skl(X0,c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____)))=v_d____)),
% 37.63/5.24 inference(paramodulation,[status(thm)],[f5006,f1163])).
% 37.63/5.24 fof(f5027,plain,(
% 37.63/5.24 ![X0]: (hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))),X0)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex))),
% 37.63/5.24 inference(resolution,[status(thm)],[f4638,f1217])).
% 37.63/5.24 fof(f5030,plain,(
% 37.63/5.24 ![X0]: (hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))),X0)=v_d____)),
% 37.63/5.24 inference(forward_demodulation,[status(thm)],[f1164,f5027])).
% 37.63/5.24 fof(f5035,plain,(
% 37.63/5.24 ![X0]: (~hAPP(X0,sK0_skl(X0,c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))))=v_d____|X0=c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))),
% 37.63/5.24 inference(paramodulation,[status(thm)],[f5030,f1163])).
% 37.63/5.24 fof(f5150,plain,(
% 37.63/5.24 ![X0]: (~class_Rings_Oidom(tc_Complex_Ocomplex)|~v_d____=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)|c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))|~c_Polynomial_Oorder(tc_Complex_Ocomplex,X0,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____))=c_Groups_Ozero__class_Ozero(tc_Nat_Onat)|X0=v_d____)),
% 37.63/5.24 inference(paramodulation,[status(thm)],[f5006,f1231])).
% 37.63/5.24 fof(f5154,plain,(
% 37.63/5.24 ![X0]: (~class_Rings_Oidom(tc_Complex_Ocomplex)|~v_d____=v_d____|c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))|~c_Polynomial_Oorder(tc_Complex_Ocomplex,X0,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____))=c_Groups_Ozero__class_Ozero(tc_Nat_Onat)|X0=v_d____)),
% 37.63/5.24 inference(forward_demodulation,[status(thm)],[f1164,f5150])).
% 37.63/5.24 fof(f5155,plain,(
% 37.63/5.24 ![X0]: (~class_Rings_Oidom(tc_Complex_Ocomplex)|c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))|~c_Polynomial_Oorder(tc_Complex_Ocomplex,X0,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____))=c_Groups_Ozero__class_Ozero(tc_Nat_Onat)|X0=v_d____)),
% 37.63/5.24 inference(trivial_equality_resolution,[status(thm)],[f5154])).
% 37.63/5.24 fof(f5156,plain,(
% 37.63/5.24 ![X0]: (c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))|~c_Polynomial_Oorder(tc_Complex_Ocomplex,X0,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____))=c_Groups_Ozero__class_Ozero(tc_Nat_Onat)|X0=v_d____)),
% 37.63/5.24 inference(forward_subsumption_resolution,[status(thm)],[f5155,f4659])).
% 37.63/5.24 fof(f5159,plain,(
% 37.63/5.24 ![X0,X1]: (hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,X0),X1)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)|c_Polynomial_Oorder(tc_Complex_Ocomplex,X1,X0)=c_Groups_Ozero__class_Ozero(tc_Nat_Onat))),
% 37.63/5.24 inference(resolution,[status(thm)],[f1233,f4659])).
% 37.63/5.24 fof(f5160,plain,(
% 37.63/5.24 ![X0,X1]: (hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,X0),X1)=v_d____|c_Polynomial_Oorder(tc_Complex_Ocomplex,X1,X0)=c_Groups_Ozero__class_Ozero(tc_Nat_Onat))),
% 37.63/5.24 inference(forward_demodulation,[status(thm)],[f1164,f5159])).
% 37.63/5.24 fof(f5200,plain,(
% 37.63/5.24 ![X0,X1]: (~hAPP(X0,sK0_skl(X0,c_Polynomial_Opoly(tc_Complex_Ocomplex,X1)))=v_d____|X0=c_Polynomial_Opoly(tc_Complex_Ocomplex,X1)|c_Polynomial_Oorder(tc_Complex_Ocomplex,sK0_skl(X0,c_Polynomial_Opoly(tc_Complex_Ocomplex,X1)),X1)=c_Groups_Ozero__class_Ozero(tc_Nat_Onat))),
% 37.63/5.24 inference(paramodulation,[status(thm)],[f5160,f1163])).
% 37.63/5.24 fof(f5272,plain,(
% 37.63/5.24 ![X0]: (~c_Polynomial_Oorder(tc_Complex_Ocomplex,X0,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____))=c_Groups_Ozero__class_Ozero(tc_Nat_Onat)|X0=v_d____)),
% 37.63/5.24 inference(forward_subsumption_resolution,[status(thm)],[f5156,f4785])).
% 37.63/5.24 fof(f5647,plain,(
% 37.63/5.24 ![X0,X1]: (~hAPP(X0,sK0_skl(X0,c_Polynomial_Opoly(tc_Complex_Ocomplex,X1)))=v_d____|X0=c_Polynomial_Opoly(tc_Complex_Ocomplex,X1)|c_Polynomial_Oorder(tc_Complex_Ocomplex,sK0_skl(X0,c_Polynomial_Opoly(tc_Complex_Ocomplex,X1)),X1)=c_HOL_Obool_Obool__size(c_fFalse))),
% 37.63/5.24 inference(backward_demodulation,[status(thm)],[f2097,f5200])).
% 37.63/5.24 fof(f5656,plain,(
% 37.63/5.24 ![X0]: (~c_Polynomial_Oorder(tc_Complex_Ocomplex,X0,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____))=c_HOL_Obool_Obool__size(c_fFalse)|X0=v_d____)),
% 37.63/5.24 inference(backward_demodulation,[status(thm)],[f2097,f5272])).
% 37.63/5.24 fof(f5667,plain,(
% 37.63/5.24 c_HOL_Obool_Obool__size(c_fFalse)=c_HOL_Obool_Obool__size(c_fTrue)),
% 37.63/5.24 inference(backward_demodulation,[status(thm)],[f2098,f2097])).
% 37.63/5.24 fof(f5670,plain,(
% 37.63/5.24 ![X0]: (c_Polynomial_Omonom(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex),X0)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))),
% 37.63/5.24 inference(resolution,[status(thm)],[f4843,f4657])).
% 37.63/5.24 fof(f5672,plain,(
% 37.63/5.24 ![X0]: (c_Polynomial_Omonom(tc_Complex_Ocomplex,v_d____,X0)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))),
% 37.63/5.24 inference(forward_demodulation,[status(thm)],[f1164,f5670])).
% 37.63/5.24 fof(f6369,plain,(
% 37.63/5.24 class_Groups_Ocomm__monoid__add(tc_Polynomial_Opoly(tc_Complex_Ocomplex))),
% 37.63/5.24 inference(resolution,[status(thm)],[f4714,f4636])).
% 37.63/5.24 fof(f6687,plain,(
% 37.63/5.24 ![X0,X1,X2]: (X0=X1|hAPP(c_Polynomial_Ocoeff(tc_Complex_Ocomplex,c_Polynomial_Omonom(tc_Complex_Ocomplex,X2,X0)),X1)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex))),
% 37.63/5.24 inference(resolution,[status(thm)],[f1314,f4657])).
% 37.63/5.24 fof(f6689,plain,(
% 37.63/5.24 ![X0,X1,X2]: (X0=X1|hAPP(c_Polynomial_Ocoeff(tc_Complex_Ocomplex,c_Polynomial_Omonom(tc_Complex_Ocomplex,X2,X0)),X1)=v_d____)),
% 37.63/5.24 inference(forward_demodulation,[status(thm)],[f1164,f6687])).
% 37.63/5.24 fof(f6697,plain,(
% 37.63/5.24 ![X0,X1]: (X0=sK0_skl(c_Polynomial_Ocoeff(tc_Complex_Ocomplex,c_Polynomial_Omonom(tc_Complex_Ocomplex,X1,X0)),c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____)))|c_Polynomial_Ocoeff(tc_Complex_Ocomplex,c_Polynomial_Omonom(tc_Complex_Ocomplex,X1,X0))=c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____))|sK0_skl(c_Polynomial_Ocoeff(tc_Complex_Ocomplex,c_Polynomial_Omonom(tc_Complex_Ocomplex,X1,X0)),c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____)))=v_d____)),
% 37.63/5.24 inference(resolution,[status(thm)],[f6689,f5008])).
% 37.63/5.24 fof(f6702,plain,(
% 37.63/5.24 ![X0,X1]: (X0=X1|hAPP(c_Polynomial_Ocoeff(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))),X1)=v_d____)),
% 37.63/5.24 inference(paramodulation,[status(thm)],[f5672,f6689])).
% 37.63/5.24 fof(f6747,plain,(
% 37.63/5.24 ![X0]: (hAPP(c_Polynomial_Ocoeff(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))),X0)=v_d____)),
% 37.63/5.24 inference(resolution,[status(thm)],[f6702,f1550])).
% 37.63/5.24 fof(f6859,plain,(
% 37.63/5.24 c_Polynomial_Ocoeff(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))=c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))),
% 37.63/5.24 inference(resolution,[status(thm)],[f6747,f5035])).
% 37.63/5.24 fof(f6882,plain,(
% 37.63/5.24 ![X0]: (~v_d____=hAPP(X0,sK0_skl(c_Polynomial_Ocoeff(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))),X0))|c_Polynomial_Ocoeff(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))=X0)),
% 37.63/5.24 inference(paramodulation,[status(thm)],[f6747,f1163])).
% 37.63/5.24 fof(f6989,plain,(
% 37.63/5.24 ![X0]: (~class_Int_Oring__char__0(tc_Complex_Ocomplex)|~class_Rings_Oidom(tc_Complex_Ocomplex)|~c_Polynomial_Opoly(tc_Complex_Ocomplex,X0)=c_Polynomial_Ocoeff(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))|X0=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))),
% 37.63/5.24 inference(paramodulation,[status(thm)],[f6859,f1208])).
% 37.63/5.24 fof(f7014,plain,(
% 37.63/5.24 ![X0]: (~class_Rings_Oidom(tc_Complex_Ocomplex)|~c_Polynomial_Opoly(tc_Complex_Ocomplex,X0)=c_Polynomial_Ocoeff(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))|X0=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))),
% 37.63/5.24 inference(forward_subsumption_resolution,[status(thm)],[f6989,f4651])).
% 37.63/5.24 fof(f7049,plain,(
% 37.63/5.24 ![X0]: (~c_Polynomial_Oorder(tc_Complex_Ocomplex,X0,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____))=c_HOL_Obool_Obool__size(c_fTrue)|X0=v_d____)),
% 37.63/5.24 inference(backward_demodulation,[status(thm)],[f5667,f5656])).
% 37.63/5.24 fof(f7356,plain,(
% 37.63/5.24 ![X0]: (~c_Polynomial_Opoly(tc_Complex_Ocomplex,X0)=c_Polynomial_Ocoeff(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))|X0=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))),
% 37.63/5.24 inference(forward_subsumption_resolution,[status(thm)],[f7014,f4659])).
% 37.63/5.24 fof(f8120,plain,(
% 37.63/5.24 ![X0]: (c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(tc_Complex_Ocomplex),X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))=X0)),
% 37.63/5.24 inference(resolution,[status(thm)],[f1406,f6369])).
% 37.63/5.24 fof(f8682,plain,(
% 37.63/5.24 ![X0,X1]: (~hAPP(X0,sK0_skl(X0,c_Polynomial_Opoly(tc_Complex_Ocomplex,X1)))=v_d____|X0=c_Polynomial_Opoly(tc_Complex_Ocomplex,X1)|c_Polynomial_Oorder(tc_Complex_Ocomplex,sK0_skl(X0,c_Polynomial_Opoly(tc_Complex_Ocomplex,X1)),X1)=c_HOL_Obool_Obool__size(c_fTrue))),
% 37.63/5.24 inference(forward_demodulation,[status(thm)],[f5667,f5647])).
% 37.63/5.24 fof(f9093,plain,(
% 37.63/5.24 ![X0]: (c_Polynomial_Osmult(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex),X0)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))),
% 37.63/5.24 inference(resolution,[status(thm)],[f4852,f4659])).
% 37.63/5.24 fof(f9094,plain,(
% 37.63/5.24 ![X0]: (c_Polynomial_Osmult(tc_Complex_Ocomplex,v_d____,X0)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))),
% 37.63/5.24 inference(forward_demodulation,[status(thm)],[f1164,f9093])).
% 37.63/5.24 fof(f9103,plain,(
% 37.63/5.24 ![X0,X1,X2]: (~class_Rings_Ocomm__semiring__0(tc_Complex_Ocomplex)|~c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(tc_Complex_Ocomplex),X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))=c_Polynomial_OpCons(tc_Complex_Ocomplex,X1,X2)|X1=hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,X0),v_d____))),
% 37.63/5.24 inference(paramodulation,[status(thm)],[f9094,f1449])).
% 37.63/5.24 fof(f9106,plain,(
% 37.63/5.24 ![X0,X1,X2]: (~c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(tc_Complex_Ocomplex),X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))=c_Polynomial_OpCons(tc_Complex_Ocomplex,X1,X2)|X1=hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,X0),v_d____))),
% 37.63/5.24 inference(forward_subsumption_resolution,[status(thm)],[f9103,f4638])).
% 37.63/5.24 fof(f15627,plain,(
% 37.63/5.24 ![X0,X1]: (~hAPP(c_Polynomial_Ocoeff(tc_Complex_Ocomplex,c_Polynomial_Omonom(tc_Complex_Ocomplex,X0,X1)),X1)=v_d____|c_Polynomial_Ocoeff(tc_Complex_Ocomplex,c_Polynomial_Omonom(tc_Complex_Ocomplex,X0,X1))=c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____))|c_Polynomial_Oorder(tc_Complex_Ocomplex,sK0_skl(c_Polynomial_Ocoeff(tc_Complex_Ocomplex,c_Polynomial_Omonom(tc_Complex_Ocomplex,X0,X1)),c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____))),c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____))=c_HOL_Obool_Obool__size(c_fTrue)|c_Polynomial_Ocoeff(tc_Complex_Ocomplex,c_Polynomial_Omonom(tc_Complex_Ocomplex,X0,X1))=c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____))|sK0_skl(c_Polynomial_Ocoeff(tc_Complex_Ocomplex,c_Polynomial_Omonom(tc_Complex_Ocomplex,X0,X1)),c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____)))=v_d____)),
% 37.63/5.24 inference(paramodulation,[status(thm)],[f6697,f8682])).
% 37.63/5.24 fof(f15636,plain,(
% 37.63/5.24 ![X0,X1]: (~hAPP(c_Polynomial_Ocoeff(tc_Complex_Ocomplex,c_Polynomial_Omonom(tc_Complex_Ocomplex,X0,X1)),X1)=v_d____|c_Polynomial_Ocoeff(tc_Complex_Ocomplex,c_Polynomial_Omonom(tc_Complex_Ocomplex,X0,X1))=c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____))|c_Polynomial_Oorder(tc_Complex_Ocomplex,sK0_skl(c_Polynomial_Ocoeff(tc_Complex_Ocomplex,c_Polynomial_Omonom(tc_Complex_Ocomplex,X0,X1)),c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____))),c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____))=c_HOL_Obool_Obool__size(c_fTrue)|sK0_skl(c_Polynomial_Ocoeff(tc_Complex_Ocomplex,c_Polynomial_Omonom(tc_Complex_Ocomplex,X0,X1)),c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____)))=v_d____)),
% 37.63/5.24 inference(duplicate_literals_removal,[status(thm)],[f15627])).
% 37.63/5.24 fof(f15637,plain,(
% 37.63/5.24 ![X0,X1]: (~hAPP(c_Polynomial_Ocoeff(tc_Complex_Ocomplex,c_Polynomial_Omonom(tc_Complex_Ocomplex,X0,X1)),X1)=v_d____|c_Polynomial_Ocoeff(tc_Complex_Ocomplex,c_Polynomial_Omonom(tc_Complex_Ocomplex,X0,X1))=c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____))|sK0_skl(c_Polynomial_Ocoeff(tc_Complex_Ocomplex,c_Polynomial_Omonom(tc_Complex_Ocomplex,X0,X1)),c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____)))=v_d____)),
% 37.63/5.24 inference(forward_subsumption_resolution,[status(thm)],[f15636,f7049])).
% 37.63/5.24 fof(f15753,plain,(
% 37.63/5.24 ![X0]: (~hAPP(c_Polynomial_Ocoeff(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))),X0)=v_d____|c_Polynomial_Ocoeff(tc_Complex_Ocomplex,c_Polynomial_Omonom(tc_Complex_Ocomplex,v_d____,X0))=c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____))|sK0_skl(c_Polynomial_Ocoeff(tc_Complex_Ocomplex,c_Polynomial_Omonom(tc_Complex_Ocomplex,v_d____,X0)),c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____)))=v_d____)),
% 37.63/5.24 inference(paramodulation,[status(thm)],[f5672,f15637])).
% 37.63/5.24 fof(f15754,plain,(
% 37.63/5.24 ![X0]: (~v_d____=v_d____|c_Polynomial_Ocoeff(tc_Complex_Ocomplex,c_Polynomial_Omonom(tc_Complex_Ocomplex,v_d____,X0))=c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____))|sK0_skl(c_Polynomial_Ocoeff(tc_Complex_Ocomplex,c_Polynomial_Omonom(tc_Complex_Ocomplex,v_d____,X0)),c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____)))=v_d____)),
% 37.63/5.24 inference(forward_demodulation,[status(thm)],[f6747,f15753])).
% 37.63/5.24 fof(f15755,plain,(
% 37.63/5.24 ![X0]: (~v_d____=v_d____|c_Polynomial_Ocoeff(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))=c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____))|sK0_skl(c_Polynomial_Ocoeff(tc_Complex_Ocomplex,c_Polynomial_Omonom(tc_Complex_Ocomplex,v_d____,X0)),c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____)))=v_d____)),
% 37.63/5.32 inference(forward_demodulation,[status(thm)],[f5672,f15754])).
% 37.63/5.32 fof(f15756,plain,(
% 37.63/5.32 ~v_d____=v_d____|c_Polynomial_Ocoeff(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))=c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____))|sK0_skl(c_Polynomial_Ocoeff(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))),c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____)))=v_d____),
% 37.63/5.32 inference(forward_demodulation,[status(thm)],[f5672,f15755])).
% 37.63/5.32 fof(f15757,plain,(
% 37.63/5.32 c_Polynomial_Ocoeff(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))=c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____))|sK0_skl(c_Polynomial_Ocoeff(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))),c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____)))=v_d____),
% 37.63/5.32 inference(trivial_equality_resolution,[status(thm)],[f15756])).
% 37.63/5.32 fof(f15760,plain,(
% 37.63/5.32 ~v_d____=hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____)),v_d____)|c_Polynomial_Ocoeff(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))=c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____))|c_Polynomial_Ocoeff(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))=c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____))),
% 37.63/5.32 inference(paramodulation,[status(thm)],[f15757,f6882])).
% 37.63/5.32 fof(f15766,plain,(
% 37.63/5.32 ~v_d____=hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____)),v_d____)|c_Polynomial_Ocoeff(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))=c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____))),
% 37.63/5.32 inference(duplicate_literals_removal,[status(thm)],[f15760])).
% 37.63/5.32 fof(f20403,plain,(
% 37.63/5.32 ![X0,X1,X2]: (~X0=c_Polynomial_OpCons(tc_Complex_Ocomplex,X1,X2)|X1=hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,X0),v_d____))),
% 37.63/5.32 inference(backward_demodulation,[status(thm)],[f8120,f9106])).
% 37.63/5.32 fof(f20433,plain,(
% 37.63/5.32 ![X0,X1]: (X0=hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,X0,X1)),v_d____))),
% 37.63/5.32 inference(destructive_equality_resolution,[status(thm)],[f20403])).
% 37.63/5.32 fof(f20803,plain,(
% 37.63/5.32 ~v_d____=v_d____|c_Polynomial_Ocoeff(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))=c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____))),
% 37.63/5.32 inference(backward_demodulation,[status(thm)],[f20433,f15766])).
% 37.63/5.32 fof(f20855,plain,(
% 37.63/5.32 c_Polynomial_Ocoeff(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))=c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____))),
% 37.63/5.32 inference(trivial_equality_resolution,[status(thm)],[f20803])).
% 37.63/5.32 fof(f21171,plain,(
% 37.63/5.32 c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))),
% 37.63/5.32 inference(resolution,[status(thm)],[f20855,f7356])).
% 37.63/5.32 fof(f21355,plain,(
% 37.63/5.32 $false),
% 37.63/5.32 inference(forward_subsumption_resolution,[status(thm)],[f21171,f4785])).
% 37.63/5.32 % SZS output end CNFRefutation for theBenchmark.p
% 9.87/5.34 % Elapsed time: 4.980859 seconds
% 9.87/5.34 % CPU time: 38.385926 seconds
% 9.87/5.34 % Total memory used: 492.245 MB
% 9.87/5.34 % Net memory used: 475.193 MB
%------------------------------------------------------------------------------