%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW287+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 : n016.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:55 PM UTC 2026
% Result : Theorem 0.28s 0.73s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWW287+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.45 % Computer : n016.cluster.edu
% 0.19/0.45 % Model : x86_64 x86_64
% 0.19/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.45 % Memory : 8046.5625MB
% 0.19/0.45 % OS : Linux 6.8.0-71-generic
% 0.19/0.45 % CPULimit : 300
% 0.19/0.45 % WCLimit : 300
% 0.19/0.45 % DateTime : Mon Sep 21 09:50:22 UTC 2026
% 0.19/0.45 % CPUTime :
% 0.28/0.62 % Drodi V4.1.1
% 0.28/0.73 % Refutation found
% 0.28/0.73 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.28/0.73 % SZS output start CNFRefutation for theBenchmark
% 0.28/0.73 fof(f2,axiom,(
% 0.28/0.73 v_p != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
% 0.28/0.73 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.28/0.73 fof(f3,axiom,(
% 0.28/0.73 c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p) != c_Groups_Ozero__class_Ozero(tc_Nat_Onat) ),
% 0.28/0.73 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.28/0.73 fof(f4,axiom,(
% 0.28/0.73 c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p) = c_Nat_OSuc(v_n____) ),
% 0.28/0.73 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.28/0.73 fof(f6,axiom,(
% 0.28/0.73 (! [V_x_3] :( hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Nat_OSuc(v_n____))))=> ( hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),V_x_3) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)=> hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q),V_x_3) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) ) ) )),
% 0.28/0.73 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.28/0.73 fof(f7,axiom,(
% 0.28/0.73 ( (! [B_x] :( hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),B_x) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)=> hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q),B_x) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) ))=> ( c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p) != c_Groups_Ozero__class_Ozero(tc_Nat_Onat)=> hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p)))) ) ) ),
% 0.28/0.73 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.28/0.73 fof(f1206,conjecture,(
% 0.28/0.73 ( (! [B_x] :( hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),B_x) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)=> hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q),B_x) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) ))<=> ( hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p))))| ( v_p = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))& v_q = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ) ) ) ),
% 0.28/0.73 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.28/0.73 fof(f1207,negated_conjecture,(
% 0.28/0.73 ~(( (! [B_x] :( hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),B_x) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)=> hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q),B_x) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) ))<=> ( hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p))))| ( v_p = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))& v_q = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ) ) ) )),
% 0.28/0.73 inference(negated_conjecture,[status(cth)],[f1206])).
% 0.28/0.73 fof(f1211,plain,(
% 0.28/0.73 ~v_p=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))),
% 0.28/0.73 inference(cnf_transformation,[status(thm)],[f2])).
% 0.28/0.73 fof(f1212,plain,(
% 0.28/0.73 ~c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p)=c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
% 0.28/0.73 inference(cnf_transformation,[status(thm)],[f3])).
% 0.28/0.73 fof(f1213,plain,(
% 0.28/0.73 c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p)=c_Nat_OSuc(v_n____)),
% 0.28/0.73 inference(cnf_transformation,[status(thm)],[f4])).
% 0.28/0.73 fof(f1223,plain,(
% 0.28/0.73 ![V_x_3]: (~hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Nat_OSuc(v_n____))))|(~hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),V_x_3)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)|hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q),V_x_3)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)))),
% 0.28/0.73 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 0.28/0.73 fof(f1224,plain,(
% 0.28/0.73 ~hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Nat_OSuc(v_n____))))|(![V_x_3]: (~hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),V_x_3)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)|hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q),V_x_3)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)))),
% 0.28/0.73 inference(miniscoping,[status(thm)],[f1223])).
% 0.28/0.73 fof(f1225,plain,(
% 0.28/0.73 ![X0]: (~hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Nat_OSuc(v_n____))))|~hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),X0)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)|hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q),X0)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex))),
% 0.28/0.73 inference(cnf_transformation,[status(thm)],[f1224])).
% 0.28/0.73 fof(f1226,plain,(
% 0.28/0.73 (?[B_x]: (hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),B_x)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)&~hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q),B_x)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)))|(c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p)=c_Groups_Ozero__class_Ozero(tc_Nat_Onat)|hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p)))))),
% 0.28/0.73 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 0.28/0.73 fof(f1227,plain,(
% 0.28/0.73 (hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),sK2_skl)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)&~hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q),sK2_skl)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex))|(c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p)=c_Groups_Ozero__class_Ozero(tc_Nat_Onat)|hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p)))))),
% 0.28/0.73 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(B_x,sK2_skl)],[f1226])).
% 0.28/0.73 fof(f1228,plain,(
% 0.28/0.73 hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),sK2_skl)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)|c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p)=c_Groups_Ozero__class_Ozero(tc_Nat_Onat)|hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p))))),
% 0.28/0.73 inference(cnf_transformation,[status(thm)],[f1227])).
% 0.28/0.73 fof(f1229,plain,(
% 0.28/0.73 ~hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q),sK2_skl)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)|c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p)=c_Groups_Ozero__class_Ozero(tc_Nat_Onat)|hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p))))),
% 0.28/0.73 inference(cnf_transformation,[status(thm)],[f1227])).
% 0.28/0.73 fof(f4801,plain,(
% 0.28/0.73 ((![B_x]: (~hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),B_x)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)|hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q),B_x)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)))<~>(hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p))))|(v_p=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))&v_q=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))))),
% 0.28/0.73 inference(pre_NNF_transformation,[status(thm)],[f1207])).
% 0.28/0.73 fof(f4802,plain,(
% 0.28/0.73 ((![B_x]: (~hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),B_x)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)|hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q),B_x)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)))|(hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p))))|(v_p=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))&v_q=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))))&((?[B_x]: (hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),B_x)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)&~hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q),B_x)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)))|(~hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p))))&(~v_p=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))|~v_q=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))))),
% 0.28/0.73 inference(NNF_transformation,[status(thm)],[f4801])).
% 0.28/0.73 fof(f4803,plain,(
% 0.28/0.73 ((![B_x]: (~hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),B_x)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)|hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q),B_x)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)))|(hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p))))|(v_p=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))&v_q=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))))&((hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),sK19_skl)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)&~hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q),sK19_skl)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex))|(~hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p))))&(~v_p=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))|~v_q=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))))),
% 0.28/0.73 inference(skolemize,[status(esa),new_symbols(skolem,[sK19_skl]),skolemize(B_x,sK19_skl)],[f4802])).
% 0.28/0.73 fof(f4804,plain,(
% 0.28/0.73 ![X0]: (~hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),X0)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)|hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q),X0)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)|hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p))))|v_p=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))),
% 0.28/0.73 inference(cnf_transformation,[status(thm)],[f4803])).
% 0.28/0.73 fof(f4806,plain,(
% 0.28/0.73 hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),sK19_skl)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)|~hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p))))),
% 0.28/0.73 inference(cnf_transformation,[status(thm)],[f4803])).
% 0.28/0.73 fof(f4808,plain,(
% 0.28/0.73 ~hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q),sK19_skl)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)|~hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p))))),
% 0.28/0.73 inference(cnf_transformation,[status(thm)],[f4803])).
% 0.28/0.73 fof(f4896,plain,(
% 0.28/0.73 ![X0]: (~hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),X0)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)|hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q),X0)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)|hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p)))))),
% 0.28/0.73 inference(backward_subsumption_resolution,[status(thm)],[f4804,f1211])).
% 0.28/0.73 fof(f4898,plain,(
% 0.28/0.73 ~c_Nat_OSuc(v_n____)=c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
% 0.28/0.73 inference(backward_demodulation,[status(thm)],[f1213,f1212])).
% 0.28/0.73 fof(f4902,plain,(
% 0.28/0.73 hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),sK2_skl)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)|c_Nat_OSuc(v_n____)=c_Groups_Ozero__class_Ozero(tc_Nat_Onat)|hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p))))),
% 0.28/0.73 inference(forward_demodulation,[status(thm)],[f1213,f1228])).
% 0.28/0.73 fof(f4903,plain,(
% 0.28/0.73 hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),sK2_skl)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)|c_Nat_OSuc(v_n____)=c_Groups_Ozero__class_Ozero(tc_Nat_Onat)|hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Nat_OSuc(v_n____))))),
% 0.28/0.73 inference(forward_demodulation,[status(thm)],[f1213,f4902])).
% 0.28/0.73 fof(f4905,plain,(
% 0.28/0.73 hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),sK19_skl)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)|~hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Nat_OSuc(v_n____))))),
% 0.28/0.73 inference(forward_demodulation,[status(thm)],[f1213,f4806])).
% 0.28/0.73 fof(f4906,plain,(
% 0.28/0.73 hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),sK19_skl)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)|hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),sK2_skl)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)|c_Nat_OSuc(v_n____)=c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
% 0.28/0.73 inference(resolution,[status(thm)],[f4905,f4903])).
% 0.28/0.73 fof(f4907,plain,(
% 0.28/0.73 ~hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q),sK19_skl)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)|~hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Nat_OSuc(v_n____))))),
% 0.28/0.73 inference(forward_demodulation,[status(thm)],[f1213,f4808])).
% 0.28/0.73 fof(f4908,plain,(
% 0.28/0.73 ~hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q),sK19_skl)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)|hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),sK2_skl)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)|c_Nat_OSuc(v_n____)=c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
% 0.28/0.73 inference(resolution,[status(thm)],[f4907,f4903])).
% 0.28/0.73 fof(f4915,plain,(
% 0.28/0.73 ~hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q),sK2_skl)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)|c_Nat_OSuc(v_n____)=c_Groups_Ozero__class_Ozero(tc_Nat_Onat)|hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p))))),
% 0.28/0.73 inference(forward_demodulation,[status(thm)],[f1213,f1229])).
% 0.28/0.73 fof(f4916,plain,(
% 0.28/0.73 ~hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q),sK2_skl)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)|c_Nat_OSuc(v_n____)=c_Groups_Ozero__class_Ozero(tc_Nat_Onat)|hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Nat_OSuc(v_n____))))),
% 0.28/0.73 inference(forward_demodulation,[status(thm)],[f1213,f4915])).
% 0.28/0.73 fof(f4917,plain,(
% 0.28/0.73 ~hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q),sK2_skl)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)|hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Nat_OSuc(v_n____))))),
% 0.28/0.77 inference(forward_subsumption_resolution,[status(thm)],[f4916,f4898])).
% 0.28/0.77 fof(f4926,plain,(
% 0.28/0.77 hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),sK19_skl)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)|hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),sK2_skl)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)),
% 0.28/0.77 inference(forward_subsumption_resolution,[status(thm)],[f4906,f4898])).
% 0.28/0.77 fof(f4927,plain,(
% 0.28/0.77 ![X0]: (~hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),X0)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)|hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q),X0)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)|hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Nat_OSuc(v_n____)))))),
% 0.28/0.77 inference(forward_demodulation,[status(thm)],[f1213,f4896])).
% 0.28/0.77 fof(f4928,plain,(
% 0.28/0.77 ![X0]: (~hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),X0)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)|hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q),X0)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex))),
% 0.28/0.77 inference(forward_subsumption_resolution,[status(thm)],[f4927,f1225])).
% 0.28/0.77 fof(f4929,plain,(
% 0.28/0.77 hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q),sK19_skl)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)|hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),sK2_skl)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)),
% 0.28/0.77 inference(resolution,[status(thm)],[f4928,f4926])).
% 0.28/0.77 fof(f4940,plain,(
% 0.28/0.77 hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),sK2_skl)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)|c_Nat_OSuc(v_n____)=c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
% 0.28/0.77 inference(forward_subsumption_resolution,[status(thm)],[f4908,f4929])).
% 0.28/0.77 fof(f4941,plain,(
% 0.28/0.77 c_Nat_OSuc(v_n____)=c_Groups_Ozero__class_Ozero(tc_Nat_Onat)|hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q),sK2_skl)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)),
% 0.28/0.77 inference(resolution,[status(thm)],[f4940,f4928])).
% 0.28/0.77 fof(f4943,plain,(
% 0.28/0.77 hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q),sK2_skl)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)),
% 0.28/0.77 inference(forward_subsumption_resolution,[status(thm)],[f4941,f4898])).
% 0.28/0.77 fof(f4946,plain,(
% 0.28/0.77 ~c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)|hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Nat_OSuc(v_n____))))),
% 0.28/0.77 inference(backward_demodulation,[status(thm)],[f4943,f4917])).
% 0.28/0.77 fof(f4947,plain,(
% 0.28/0.77 hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Nat_OSuc(v_n____))))),
% 0.28/0.77 inference(trivial_equality_resolution,[status(thm)],[f4946])).
% 0.28/0.77 fof(f4956,plain,(
% 0.28/0.77 ~hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q),sK19_skl)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)),
% 0.28/0.77 inference(backward_subsumption_resolution,[status(thm)],[f4907,f4947])).
% 0.28/0.77 fof(f4957,plain,(
% 0.28/0.77 hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),sK19_skl)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)),
% 0.28/0.77 inference(backward_subsumption_resolution,[status(thm)],[f4905,f4947])).
% 0.28/0.77 fof(f4961,plain,(
% 0.28/0.77 hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_q),sK19_skl)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)),
% 0.28/0.77 inference(resolution,[status(thm)],[f4957,f4928])).
% 0.28/0.77 fof(f4963,plain,(
% 0.28/0.77 $false),
% 0.28/0.77 inference(forward_subsumption_resolution,[status(thm)],[f4961,f4956])).
% 0.28/0.77 % SZS output end CNFRefutation for theBenchmark.p
% 0.28/0.81 % Elapsed time: 0.332337 seconds
% 0.28/0.81 % CPU time: 0.878986 seconds
% 0.28/0.81 % Total memory used: 209.923 MB
% 0.28/0.81 % Net memory used: 208.302 MB
%------------------------------------------------------------------------------