%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW245+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 : n006.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:51 PM UTC 2026
% Result : Theorem 171.89s 37.23s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW245+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.05 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.14/15.40 % Computer : n006.cluster.edu
% 0.14/15.40 % Model : x86_64 x86_64
% 0.14/15.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/15.40 % Memory : 8046.5625MB
% 0.14/15.40 % OS : Linux 6.8.0-71-generic
% 0.14/15.40 % CPULimit : 300
% 0.14/15.40 % WCLimit : 300
% 0.14/15.40 % DateTime : Mon Sep 21 09:43:12 UTC 2026
% 0.14/15.41 % CPUTime :
% 0.16/15.50 % Drodi V4.1.1
% 171.89/37.23 % Refutation found
% 171.89/37.23 % SZS status Theorem for theBenchmark: Theorem is valid
% 171.89/37.23 % SZS output start CNFRefutation for theBenchmark
% 171.89/37.23 fof(f4,axiom,(
% 171.89/37.23 ( class_Rings_Oidom(t_a)=> ( v_c____ != c_Groups_Ozero__class_Ozero(t_a)=> (? [B_k,B_a] :( B_a != c_Groups_Ozero__class_Ozero(t_a)& (? [B_q] :( ( c_Polynomial_OpCons(t_a,v_c____,v_cs____) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))=> c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(B_q,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,B_q))),B_k)) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat) )& ( c_Polynomial_OpCons(t_a,v_c____,v_cs____) != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))=> c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(B_q,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,B_q))),B_k)) = c_Nat_OSuc(c_Polynomial_Odegree(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____))) )& (! [B_z] : hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)),B_z) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(t_a),hAPP(hAPP(c_Power_Opower__class_Opower(t_a),B_z),B_k)),hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,B_a,B_q)),B_z)) )) )) )) ) ),
% 171.89/37.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 171.89/37.23 fof(f5,axiom,(
% 171.89/37.23 ( class_Rings_Oidom(t_a)=> ( v_c____ = c_Groups_Ozero__class_Ozero(t_a)=> (? [B_k,B_a] :( B_a != c_Groups_Ozero__class_Ozero(t_a)& (? [B_q] :( ( c_Polynomial_OpCons(t_a,v_c____,v_cs____) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))=> c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(B_q,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,B_q))),B_k)) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat) )& ( c_Polynomial_OpCons(t_a,v_c____,v_cs____) != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))=> c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(B_q,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,B_q))),B_k)) = c_Nat_OSuc(c_Polynomial_Odegree(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____))) )& (! [B_z] : hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)),B_z) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(t_a),hAPP(hAPP(c_Power_Opower__class_Opower(t_a),B_z),B_k)),hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,B_a,B_q)),B_z)) )) )) )) ) ),
% 171.89/37.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 171.89/37.23 fof(f70,axiom,(
% 171.89/37.23 (! [V_n,V_m] : c_Groups_Oplus__class_Oplus(tc_Nat_Onat,V_m,V_n) = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,V_n,V_m) )),
% 171.89/37.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 171.89/37.23 fof(f91,axiom,(
% 171.89/37.23 (! [V_m] : c_Groups_Ozero__class_Ozero(tc_Nat_Onat) != c_Nat_OSuc(V_m) )),
% 171.89/37.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 171.89/37.23 fof(f492,axiom,(
% 171.89/37.23 (! [V_n] : c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(V_n)) )),
% 171.89/37.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 171.89/37.23 fof(f535,axiom,(
% 171.89/37.23 (! [V_t,V_s] :( c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_s,V_t)=> V_s != V_t ) )),
% 171.89/37.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 171.89/37.23 fof(f1160,conjecture,(
% 171.89/37.23 (? [B_k,B_a] :( B_a != c_Groups_Ozero__class_Ozero(t_a)& (? [B_q] :( ( c_Polynomial_OpCons(t_a,v_c____,v_cs____) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))=> c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(B_q,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,B_q))),B_k)) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat) )& ( c_Polynomial_OpCons(t_a,v_c____,v_cs____) != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))=> c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(B_q,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,B_q))),B_k)) = c_Nat_OSuc(c_Polynomial_Odegree(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____))) )& (! [B_z] : hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)),B_z) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(t_a),hAPP(hAPP(c_Power_Opower__class_Opower(t_a),B_z),B_k)),hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,B_a,B_q)),B_z)) )) )) )),
% 171.89/37.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 171.89/37.23 fof(f1161,negated_conjecture,(
% 171.89/37.23 ~((? [B_k,B_a] :( B_a != c_Groups_Ozero__class_Ozero(t_a)& (? [B_q] :( ( c_Polynomial_OpCons(t_a,v_c____,v_cs____) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))=> c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(B_q,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,B_q))),B_k)) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat) )& ( c_Polynomial_OpCons(t_a,v_c____,v_cs____) != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))=> c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(B_q,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,B_q))),B_k)) = c_Nat_OSuc(c_Polynomial_Odegree(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____))) )& (! [B_z] : hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)),B_z) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(t_a),hAPP(hAPP(c_Power_Opower__class_Opower(t_a),B_z),B_k)),hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,B_a,B_q)),B_z)) )) )) ))),
% 171.89/37.23 inference(negated_conjecture,[status(cth)],[f1160])).
% 171.89/37.23 fof(f1162,hypothesis,(
% 171.89/37.23 class_Rings_Oidom(t_a) ),
% 171.89/37.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 171.89/37.23 fof(f1174,plain,(
% 171.89/37.23 ~class_Rings_Oidom(t_a)|(v_c____=c_Groups_Ozero__class_Ozero(t_a)|(?[B_k,B_a]: (~B_a=c_Groups_Ozero__class_Ozero(t_a)&(?[B_q]: (((~c_Polynomial_OpCons(t_a,v_c____,v_cs____)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))|c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(B_q,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,B_q))),B_k))=c_Groups_Ozero__class_Ozero(tc_Nat_Onat))&(c_Polynomial_OpCons(t_a,v_c____,v_cs____)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))|c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(B_q,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,B_q))),B_k))=c_Nat_OSuc(c_Polynomial_Odegree(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)))))&(![B_z]: hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)),B_z)=hAPP(hAPP(c_Groups_Otimes__class_Otimes(t_a),hAPP(hAPP(c_Power_Opower__class_Opower(t_a),B_z),B_k)),hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,B_a,B_q)),B_z))))))))),
% 171.89/37.23 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 171.89/37.23 fof(f1175,plain,(
% 171.89/37.23 ~class_Rings_Oidom(t_a)|(v_c____=c_Groups_Ozero__class_Ozero(t_a)|(?[B_a]: (~B_a=c_Groups_Ozero__class_Ozero(t_a)&(?[B_k,B_q]: (((~c_Polynomial_OpCons(t_a,v_c____,v_cs____)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))|c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(B_q,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,B_q))),B_k))=c_Groups_Ozero__class_Ozero(tc_Nat_Onat))&(c_Polynomial_OpCons(t_a,v_c____,v_cs____)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))|c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(B_q,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,B_q))),B_k))=c_Nat_OSuc(c_Polynomial_Odegree(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)))))&(![B_z]: hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)),B_z)=hAPP(hAPP(c_Groups_Otimes__class_Otimes(t_a),hAPP(hAPP(c_Power_Opower__class_Opower(t_a),B_z),B_k)),hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,B_a,B_q)),B_z))))))))),
% 171.89/37.23 inference(miniscoping,[status(thm)],[f1174])).
% 171.89/37.23 fof(f1176,plain,(
% 171.89/37.23 ~class_Rings_Oidom(t_a)|(v_c____=c_Groups_Ozero__class_Ozero(t_a)|(~sK3_skl=c_Groups_Ozero__class_Ozero(t_a)&(((~c_Polynomial_OpCons(t_a,v_c____,v_cs____)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))|c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(sK5_skl,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,sK5_skl))),sK4_skl))=c_Groups_Ozero__class_Ozero(tc_Nat_Onat))&(c_Polynomial_OpCons(t_a,v_c____,v_cs____)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))|c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(sK5_skl,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,sK5_skl))),sK4_skl))=c_Nat_OSuc(c_Polynomial_Odegree(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)))))&(![B_z]: hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)),B_z)=hAPP(hAPP(c_Groups_Otimes__class_Otimes(t_a),hAPP(hAPP(c_Power_Opower__class_Opower(t_a),B_z),sK4_skl)),hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,sK3_skl,sK5_skl)),B_z))))))),
% 171.89/37.23 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl,sK4_skl,sK5_skl]),skolemize(B_a,sK3_skl),skolemize(B_k,sK4_skl),skolemize(B_q,sK5_skl)],[f1175])).
% 171.89/37.23 fof(f1177,plain,(
% 171.89/37.23 ~class_Rings_Oidom(t_a)|v_c____=c_Groups_Ozero__class_Ozero(t_a)|~sK3_skl=c_Groups_Ozero__class_Ozero(t_a)),
% 171.89/37.23 inference(cnf_transformation,[status(thm)],[f1176])).
% 171.89/37.23 fof(f1178,plain,(
% 171.89/37.23 ~class_Rings_Oidom(t_a)|v_c____=c_Groups_Ozero__class_Ozero(t_a)|~c_Polynomial_OpCons(t_a,v_c____,v_cs____)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))|c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(sK5_skl,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,sK5_skl))),sK4_skl))=c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
% 171.89/37.23 inference(cnf_transformation,[status(thm)],[f1176])).
% 171.89/37.23 fof(f1179,plain,(
% 171.89/37.23 ~class_Rings_Oidom(t_a)|v_c____=c_Groups_Ozero__class_Ozero(t_a)|c_Polynomial_OpCons(t_a,v_c____,v_cs____)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))|c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(sK5_skl,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,sK5_skl))),sK4_skl))=c_Nat_OSuc(c_Polynomial_Odegree(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)))),
% 171.89/37.23 inference(cnf_transformation,[status(thm)],[f1176])).
% 171.89/37.23 fof(f1180,plain,(
% 171.89/37.23 ![X0]: (~class_Rings_Oidom(t_a)|v_c____=c_Groups_Ozero__class_Ozero(t_a)|hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)),X0)=hAPP(hAPP(c_Groups_Otimes__class_Otimes(t_a),hAPP(hAPP(c_Power_Opower__class_Opower(t_a),X0),sK4_skl)),hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,sK3_skl,sK5_skl)),X0)))),
% 171.89/37.23 inference(cnf_transformation,[status(thm)],[f1176])).
% 171.89/37.23 fof(f1181,plain,(
% 171.89/37.23 ~class_Rings_Oidom(t_a)|(~v_c____=c_Groups_Ozero__class_Ozero(t_a)|(?[B_k,B_a]: (~B_a=c_Groups_Ozero__class_Ozero(t_a)&(?[B_q]: (((~c_Polynomial_OpCons(t_a,v_c____,v_cs____)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))|c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(B_q,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,B_q))),B_k))=c_Groups_Ozero__class_Ozero(tc_Nat_Onat))&(c_Polynomial_OpCons(t_a,v_c____,v_cs____)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))|c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(B_q,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,B_q))),B_k))=c_Nat_OSuc(c_Polynomial_Odegree(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)))))&(![B_z]: hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)),B_z)=hAPP(hAPP(c_Groups_Otimes__class_Otimes(t_a),hAPP(hAPP(c_Power_Opower__class_Opower(t_a),B_z),B_k)),hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,B_a,B_q)),B_z))))))))),
% 171.89/37.23 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 171.89/37.23 fof(f1182,plain,(
% 171.89/37.23 ~class_Rings_Oidom(t_a)|(~v_c____=c_Groups_Ozero__class_Ozero(t_a)|(?[B_a]: (~B_a=c_Groups_Ozero__class_Ozero(t_a)&(?[B_k,B_q]: (((~c_Polynomial_OpCons(t_a,v_c____,v_cs____)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))|c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(B_q,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,B_q))),B_k))=c_Groups_Ozero__class_Ozero(tc_Nat_Onat))&(c_Polynomial_OpCons(t_a,v_c____,v_cs____)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))|c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(B_q,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,B_q))),B_k))=c_Nat_OSuc(c_Polynomial_Odegree(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)))))&(![B_z]: hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)),B_z)=hAPP(hAPP(c_Groups_Otimes__class_Otimes(t_a),hAPP(hAPP(c_Power_Opower__class_Opower(t_a),B_z),B_k)),hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,B_a,B_q)),B_z))))))))),
% 171.89/37.23 inference(miniscoping,[status(thm)],[f1181])).
% 171.89/37.23 fof(f1183,plain,(
% 171.89/37.23 ~class_Rings_Oidom(t_a)|(~v_c____=c_Groups_Ozero__class_Ozero(t_a)|(~sK6_skl=c_Groups_Ozero__class_Ozero(t_a)&(((~c_Polynomial_OpCons(t_a,v_c____,v_cs____)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))|c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(sK8_skl,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,sK8_skl))),sK7_skl))=c_Groups_Ozero__class_Ozero(tc_Nat_Onat))&(c_Polynomial_OpCons(t_a,v_c____,v_cs____)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))|c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(sK8_skl,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,sK8_skl))),sK7_skl))=c_Nat_OSuc(c_Polynomial_Odegree(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)))))&(![B_z]: hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)),B_z)=hAPP(hAPP(c_Groups_Otimes__class_Otimes(t_a),hAPP(hAPP(c_Power_Opower__class_Opower(t_a),B_z),sK7_skl)),hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,sK6_skl,sK8_skl)),B_z))))))),
% 171.89/37.23 inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl,sK7_skl,sK8_skl]),skolemize(B_a,sK6_skl),skolemize(B_k,sK7_skl),skolemize(B_q,sK8_skl)],[f1182])).
% 171.89/37.23 fof(f1184,plain,(
% 171.89/37.23 ~class_Rings_Oidom(t_a)|~v_c____=c_Groups_Ozero__class_Ozero(t_a)|~sK6_skl=c_Groups_Ozero__class_Ozero(t_a)),
% 171.89/37.23 inference(cnf_transformation,[status(thm)],[f1183])).
% 171.89/37.23 fof(f1185,plain,(
% 171.89/37.23 ~class_Rings_Oidom(t_a)|~v_c____=c_Groups_Ozero__class_Ozero(t_a)|~c_Polynomial_OpCons(t_a,v_c____,v_cs____)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))|c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(sK8_skl,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,sK8_skl))),sK7_skl))=c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
% 171.89/37.23 inference(cnf_transformation,[status(thm)],[f1183])).
% 171.89/37.23 fof(f1186,plain,(
% 171.89/37.23 ~class_Rings_Oidom(t_a)|~v_c____=c_Groups_Ozero__class_Ozero(t_a)|c_Polynomial_OpCons(t_a,v_c____,v_cs____)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))|c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(sK8_skl,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,sK8_skl))),sK7_skl))=c_Nat_OSuc(c_Polynomial_Odegree(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)))),
% 171.89/37.23 inference(cnf_transformation,[status(thm)],[f1183])).
% 171.89/37.23 fof(f1187,plain,(
% 171.89/37.23 ![X0]: (~class_Rings_Oidom(t_a)|~v_c____=c_Groups_Ozero__class_Ozero(t_a)|hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)),X0)=hAPP(hAPP(c_Groups_Otimes__class_Otimes(t_a),hAPP(hAPP(c_Power_Opower__class_Opower(t_a),X0),sK7_skl)),hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,sK6_skl,sK8_skl)),X0)))),
% 171.89/37.23 inference(cnf_transformation,[status(thm)],[f1183])).
% 171.89/37.23 fof(f1408,plain,(
% 171.89/37.23 ![X0,X1]: (c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X0,X1)=c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X1,X0))),
% 171.89/37.23 inference(cnf_transformation,[status(thm)],[f70])).
% 171.89/37.23 fof(f1471,plain,(
% 171.89/37.23 ![X0]: (~c_Groups_Ozero__class_Ozero(tc_Nat_Onat)=c_Nat_OSuc(X0))),
% 171.89/37.23 inference(cnf_transformation,[status(thm)],[f91])).
% 171.89/37.23 fof(f2665,plain,(
% 171.89/37.23 ![X0]: (c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(X0)))),
% 171.89/37.23 inference(cnf_transformation,[status(thm)],[f492])).
% 171.89/37.23 fof(f2800,plain,(
% 171.89/37.23 ![V_t,V_s]: (~c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_s,V_t)|~V_s=V_t)),
% 171.89/37.23 inference(pre_NNF_transformation,[status(thm)],[f535])).
% 171.89/37.23 fof(f2801,plain,(
% 171.89/37.23 ![X0,X1]: (~c_Orderings_Oord__class_Oless(tc_Nat_Onat,X0,X1)|~X0=X1)),
% 171.89/37.23 inference(cnf_transformation,[status(thm)],[f2800])).
% 171.89/37.23 fof(f4612,plain,(
% 171.89/37.23 (![B_k,B_a]: (B_a=c_Groups_Ozero__class_Ozero(t_a)|(![B_q]: (((c_Polynomial_OpCons(t_a,v_c____,v_cs____)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))&~c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(B_q,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,B_q))),B_k))=c_Groups_Ozero__class_Ozero(tc_Nat_Onat))|(~c_Polynomial_OpCons(t_a,v_c____,v_cs____)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))&~c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(B_q,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,B_q))),B_k))=c_Nat_OSuc(c_Polynomial_Odegree(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)))))|(?[B_z]: ~hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)),B_z)=hAPP(hAPP(c_Groups_Otimes__class_Otimes(t_a),hAPP(hAPP(c_Power_Opower__class_Opower(t_a),B_z),B_k)),hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,B_a,B_q)),B_z)))))))),
% 171.89/37.23 inference(pre_NNF_transformation,[status(thm)],[f1161])).
% 171.89/37.23 fof(f4613,definition,(
% 171.89/37.23 ![B_k,B_q]: (sP6_prd(B_q,B_k)<=>(c_Polynomial_OpCons(t_a,v_c____,v_cs____)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))&~c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(B_q,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,B_q))),B_k))=c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))),
% 171.89/37.23 introduced(definition,[new_symbols(definition,[sP6_prd])],[])).
% 171.89/37.23 fof(f4614,plain,(
% 171.89/37.23 ![B_k,B_a]: (B_a=c_Groups_Ozero__class_Ozero(t_a)|(![B_q]: ((sP6_prd(B_q,B_k)|(~c_Polynomial_OpCons(t_a,v_c____,v_cs____)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))&~c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(B_q,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,B_q))),B_k))=c_Nat_OSuc(c_Polynomial_Odegree(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)))))|(?[B_z]: ~hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)),B_z)=hAPP(hAPP(c_Groups_Otimes__class_Otimes(t_a),hAPP(hAPP(c_Power_Opower__class_Opower(t_a),B_z),B_k)),hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,B_a,B_q)),B_z))))))),
% 171.89/37.23 inference(formula_renaming,[status(thm)],[f4612,f4613])).
% 171.89/37.23 fof(f4615,plain,(
% 171.89/37.23 ![B_a]: (B_a=c_Groups_Ozero__class_Ozero(t_a)|(![B_k,B_q]: ((sP6_prd(B_q,B_k)|(~c_Polynomial_OpCons(t_a,v_c____,v_cs____)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))&~c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(B_q,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,B_q))),B_k))=c_Nat_OSuc(c_Polynomial_Odegree(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)))))|(?[B_z]: ~hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)),B_z)=hAPP(hAPP(c_Groups_Otimes__class_Otimes(t_a),hAPP(hAPP(c_Power_Opower__class_Opower(t_a),B_z),B_k)),hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,B_a,B_q)),B_z))))))),
% 171.89/37.23 inference(miniscoping,[status(thm)],[f4614])).
% 171.89/37.23 fof(f4616,plain,(
% 171.89/37.23 ![B_a]: (B_a=c_Groups_Ozero__class_Ozero(t_a)|(![B_k,B_q]: ((sP6_prd(B_q,B_k)|(~c_Polynomial_OpCons(t_a,v_c____,v_cs____)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))&~c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(B_q,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,B_q))),B_k))=c_Nat_OSuc(c_Polynomial_Odegree(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)))))|~hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)),sK31_skl(B_q,B_k,B_a))=hAPP(hAPP(c_Groups_Otimes__class_Otimes(t_a),hAPP(hAPP(c_Power_Opower__class_Opower(t_a),sK31_skl(B_q,B_k,B_a)),B_k)),hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,B_a,B_q)),sK31_skl(B_q,B_k,B_a))))))),
% 171.89/37.23 inference(skolemize,[status(esa),new_symbols(skolem,[sK31_skl]),skolemize(B_z,sK31_skl(B_q,B_k,B_a))],[f4615])).
% 171.89/37.23 fof(f4618,plain,(
% 171.89/37.23 ![X0,X1,X2]: (X0=c_Groups_Ozero__class_Ozero(t_a)|sP6_prd(X1,X2)|~c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(X1,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,X1))),X2))=c_Nat_OSuc(c_Polynomial_Odegree(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)))|~hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)),sK31_skl(X1,X2,X0))=hAPP(hAPP(c_Groups_Otimes__class_Otimes(t_a),hAPP(hAPP(c_Power_Opower__class_Opower(t_a),sK31_skl(X1,X2,X0)),X2)),hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,X0,X1)),sK31_skl(X1,X2,X0))))),
% 171.89/37.23 inference(cnf_transformation,[status(thm)],[f4616])).
% 171.89/37.23 fof(f4619,plain,(
% 171.89/37.23 class_Rings_Oidom(t_a)),
% 171.89/37.23 inference(cnf_transformation,[status(thm)],[f1162])).
% 171.89/37.23 fof(f4658,plain,(
% 171.89/37.23 ![B_k,B_q]: ((~sP6_prd(B_q,B_k)|(c_Polynomial_OpCons(t_a,v_c____,v_cs____)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))&~c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(B_q,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,B_q))),B_k))=c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))&(sP6_prd(B_q,B_k)|(~c_Polynomial_OpCons(t_a,v_c____,v_cs____)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))|c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(B_q,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,B_q))),B_k))=c_Groups_Ozero__class_Ozero(tc_Nat_Onat))))),
% 171.89/37.23 inference(NNF_transformation,[status(thm)],[f4613])).
% 171.89/37.23 fof(f4659,plain,(
% 171.89/37.23 (![B_k,B_q]: (~sP6_prd(B_q,B_k)|(c_Polynomial_OpCons(t_a,v_c____,v_cs____)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))&~c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(B_q,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,B_q))),B_k))=c_Groups_Ozero__class_Ozero(tc_Nat_Onat))))&(![B_k,B_q]: (sP6_prd(B_q,B_k)|(~c_Polynomial_OpCons(t_a,v_c____,v_cs____)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))|c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(B_q,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,B_q))),B_k))=c_Groups_Ozero__class_Ozero(tc_Nat_Onat))))),
% 171.89/37.23 inference(miniscoping,[status(thm)],[f4658])).
% 171.89/37.23 fof(f4660,plain,(
% 171.89/37.23 ![X0,X1]: (~sP6_prd(X0,X1)|c_Polynomial_OpCons(t_a,v_c____,v_cs____)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))),
% 171.89/37.23 inference(cnf_transformation,[status(thm)],[f4659])).
% 171.89/37.23 fof(f4677,plain,(
% 171.89/37.23 ![X0]: (~c_Orderings_Oord__class_Oless(tc_Nat_Onat,X0,X0))),
% 171.89/37.23 inference(destructive_equality_resolution,[status(thm)],[f2801])).
% 171.89/37.23 fof(f4693,plain,(
% 171.89/37.23 ![X0,X1,X2]: (X0=c_Groups_Ozero__class_Ozero(t_a)|~c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(X1,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,X1))),X2))=c_Nat_OSuc(c_Polynomial_Odegree(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)))|~hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)),sK31_skl(X1,X2,X0))=hAPP(hAPP(c_Groups_Otimes__class_Otimes(t_a),hAPP(hAPP(c_Power_Opower__class_Opower(t_a),sK31_skl(X1,X2,X0)),X2)),hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,X0,X1)),sK31_skl(X1,X2,X0)))|c_Polynomial_OpCons(t_a,v_c____,v_cs____)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))),
% 171.89/37.23 inference(resolution,[status(thm)],[f4618,f4660])).
% 171.89/37.23 fof(f4768,plain,(
% 171.89/37.23 v_c____=c_Groups_Ozero__class_Ozero(t_a)|~c_Polynomial_OpCons(t_a,v_c____,v_cs____)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))|c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(sK5_skl,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,sK5_skl))),sK4_skl))=c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
% 171.89/37.23 inference(forward_subsumption_resolution,[status(thm)],[f1178,f4619])).
% 171.89/37.23 fof(f4769,plain,(
% 171.89/37.23 v_c____=c_Groups_Ozero__class_Ozero(t_a)|c_Polynomial_OpCons(t_a,v_c____,v_cs____)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))|c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(sK5_skl,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,sK5_skl))),sK4_skl))=c_Nat_OSuc(c_Polynomial_Odegree(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)))),
% 171.89/37.23 inference(forward_subsumption_resolution,[status(thm)],[f1179,f4619])).
% 171.89/37.23 fof(f4778,plain,(
% 171.89/37.23 ![X0]: (v_c____=c_Groups_Ozero__class_Ozero(t_a)|hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)),X0)=hAPP(hAPP(c_Groups_Otimes__class_Otimes(t_a),hAPP(hAPP(c_Power_Opower__class_Opower(t_a),X0),sK4_skl)),hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,sK3_skl,sK5_skl)),X0)))),
% 171.89/37.23 inference(forward_subsumption_resolution,[status(thm)],[f1180,f4619])).
% 171.89/37.23 fof(f4779,plain,(
% 171.89/37.23 v_c____=c_Groups_Ozero__class_Ozero(t_a)|sK3_skl=c_Groups_Ozero__class_Ozero(t_a)|~c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(sK5_skl,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,sK5_skl))),sK4_skl))=c_Nat_OSuc(c_Polynomial_Odegree(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)))|c_Polynomial_OpCons(t_a,v_c____,v_cs____)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),
% 171.89/37.23 inference(resolution,[status(thm)],[f4778,f4693])).
% 171.89/37.23 fof(f4788,plain,(
% 171.89/37.23 v_c____=c_Groups_Ozero__class_Ozero(t_a)|sK3_skl=c_Groups_Ozero__class_Ozero(t_a)|c_Polynomial_OpCons(t_a,v_c____,v_cs____)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),
% 171.89/37.23 inference(forward_subsumption_resolution,[status(thm)],[f4779,f4769])).
% 171.89/37.23 fof(f4792,plain,(
% 171.89/37.23 ~v_c____=c_Groups_Ozero__class_Ozero(t_a)|c_Polynomial_OpCons(t_a,v_c____,v_cs____)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))|c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(sK8_skl,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,sK8_skl))),sK7_skl))=c_Nat_OSuc(c_Polynomial_Odegree(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)))),
% 171.89/37.23 inference(forward_subsumption_resolution,[status(thm)],[f1186,f4619])).
% 171.89/37.23 fof(f4858,plain,(
% 171.89/37.23 v_c____=c_Groups_Ozero__class_Ozero(t_a)|~sK3_skl=c_Groups_Ozero__class_Ozero(t_a)),
% 171.89/37.24 inference(forward_subsumption_resolution,[status(thm)],[f1177,f4619])).
% 171.89/37.24 fof(f4859,plain,(
% 171.89/37.24 c_Polynomial_OpCons(t_a,v_c____,v_cs____)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))|c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(sK8_skl,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,sK8_skl))),sK7_skl))=c_Nat_OSuc(c_Polynomial_Odegree(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)))),
% 171.89/37.24 inference(backward_subsumption_resolution,[status(thm)],[f4792,f4861])).
% 171.89/37.24 fof(f4860,plain,(
% 171.89/37.24 v_c____=c_Groups_Ozero__class_Ozero(t_a)|c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(sK5_skl,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,sK5_skl))),sK4_skl))=c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
% 171.89/37.24 inference(backward_subsumption_resolution,[status(thm)],[f4768,f4861])).
% 171.89/37.24 fof(f4861,plain,(
% 171.89/37.24 v_c____=c_Groups_Ozero__class_Ozero(t_a)|c_Polynomial_OpCons(t_a,v_c____,v_cs____)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),
% 171.89/37.24 inference(forward_subsumption_resolution,[status(thm)],[f4788,f4858])).
% 171.89/37.24 fof(f4872,plain,(
% 171.89/37.24 c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Groups_Ozero__class_Ozero(tc_Nat_Onat))|v_c____=c_Groups_Ozero__class_Ozero(t_a)),
% 171.89/37.24 inference(paramodulation,[status(thm)],[f4860,f2665])).
% 171.89/37.24 fof(f4881,plain,(
% 171.89/37.24 v_c____=c_Groups_Ozero__class_Ozero(t_a)),
% 171.89/37.24 inference(forward_subsumption_resolution,[status(thm)],[f4872,f4677])).
% 171.89/37.24 fof(f5082,plain,(
% 171.89/37.24 ![X0,X1,X2]: (X0=v_c____|sP6_prd(X1,X2)|~c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(X1,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,X1))),X2))=c_Nat_OSuc(c_Polynomial_Odegree(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)))|~hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)),sK31_skl(X1,X2,X0))=hAPP(hAPP(c_Groups_Otimes__class_Otimes(t_a),hAPP(hAPP(c_Power_Opower__class_Opower(t_a),sK31_skl(X1,X2,X0)),X2)),hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,X0,X1)),sK31_skl(X1,X2,X0))))),
% 171.89/37.24 inference(backward_demodulation,[status(thm)],[f4881,f4618])).
% 171.89/37.24 fof(f5095,plain,(
% 171.89/37.24 c_Polynomial_OpCons(t_a,v_c____,v_cs____)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))|c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,sK7_skl,c_If(tc_Nat_Onat,c_fequal(sK8_skl,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,sK8_skl)))))=c_Nat_OSuc(c_Polynomial_Odegree(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)))),
% 171.89/37.24 inference(backward_demodulation,[status(thm)],[f1408,f4859])).
% 171.89/37.24 fof(f5203,plain,(
% 171.89/37.24 ~class_Rings_Oidom(t_a)|~v_c____=v_c____|~sK6_skl=c_Groups_Ozero__class_Ozero(t_a)),
% 171.89/37.24 inference(forward_demodulation,[status(thm)],[f4881,f1184])).
% 171.89/37.24 fof(f5204,plain,(
% 171.89/37.24 ~class_Rings_Oidom(t_a)|~v_c____=v_c____|~sK6_skl=v_c____),
% 171.89/37.24 inference(forward_demodulation,[status(thm)],[f4881,f5203])).
% 171.89/37.24 fof(f5205,plain,(
% 171.89/37.24 ~class_Rings_Oidom(t_a)|~sK6_skl=v_c____),
% 171.89/37.24 inference(trivial_equality_resolution,[status(thm)],[f5204])).
% 171.89/37.24 fof(f5206,plain,(
% 171.89/37.24 ~sK6_skl=v_c____),
% 171.89/37.24 inference(forward_subsumption_resolution,[status(thm)],[f5205,f4619])).
% 171.89/37.24 fof(f5207,plain,(
% 171.89/37.24 ~class_Rings_Oidom(t_a)|~v_c____=v_c____|~c_Polynomial_OpCons(t_a,v_c____,v_cs____)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))|c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(sK8_skl,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,sK8_skl))),sK7_skl))=c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
% 171.89/37.24 inference(forward_demodulation,[status(thm)],[f4881,f1185])).
% 171.89/37.24 fof(f5208,plain,(
% 171.89/37.24 ~class_Rings_Oidom(t_a)|~v_c____=v_c____|~c_Polynomial_OpCons(t_a,v_c____,v_cs____)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))|c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,sK7_skl,c_If(tc_Nat_Onat,c_fequal(sK8_skl,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,sK8_skl)))))=c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
% 171.89/37.24 inference(forward_demodulation,[status(thm)],[f1408,f5207])).
% 171.89/37.24 fof(f5209,plain,(
% 171.89/37.24 ~class_Rings_Oidom(t_a)|~c_Polynomial_OpCons(t_a,v_c____,v_cs____)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))|c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,sK7_skl,c_If(tc_Nat_Onat,c_fequal(sK8_skl,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,sK8_skl)))))=c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
% 171.89/37.24 inference(trivial_equality_resolution,[status(thm)],[f5208])).
% 171.89/37.24 fof(f5210,plain,(
% 171.89/37.24 ~c_Polynomial_OpCons(t_a,v_c____,v_cs____)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))|c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,sK7_skl,c_If(tc_Nat_Onat,c_fequal(sK8_skl,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,sK8_skl)))))=c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
% 171.89/37.24 inference(forward_subsumption_resolution,[status(thm)],[f5209,f4619])).
% 171.89/37.24 fof(f5211,plain,(
% 171.89/37.24 ![X0]: (~class_Rings_Oidom(t_a)|~v_c____=v_c____|hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)),X0)=hAPP(hAPP(c_Groups_Otimes__class_Otimes(t_a),hAPP(hAPP(c_Power_Opower__class_Opower(t_a),X0),sK7_skl)),hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,sK6_skl,sK8_skl)),X0)))),
% 171.89/37.24 inference(forward_demodulation,[status(thm)],[f4881,f1187])).
% 171.89/37.24 fof(f5212,plain,(
% 171.89/37.24 ![X0]: (~class_Rings_Oidom(t_a)|hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)),X0)=hAPP(hAPP(c_Groups_Otimes__class_Otimes(t_a),hAPP(hAPP(c_Power_Opower__class_Opower(t_a),X0),sK7_skl)),hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,sK6_skl,sK8_skl)),X0)))),
% 171.89/37.24 inference(trivial_equality_resolution,[status(thm)],[f5211])).
% 171.89/37.24 fof(f5213,plain,(
% 171.89/37.24 ![X0]: (hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)),X0)=hAPP(hAPP(c_Groups_Otimes__class_Otimes(t_a),hAPP(hAPP(c_Power_Opower__class_Opower(t_a),X0),sK7_skl)),hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,sK6_skl,sK8_skl)),X0)))),
% 171.89/37.24 inference(forward_subsumption_resolution,[status(thm)],[f5212,f4619])).
% 171.89/37.24 fof(f20610,plain,(
% 171.89/37.24 ~c_Polynomial_OpCons(t_a,v_c____,v_cs____)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),
% 171.89/37.24 inference(backward_subsumption_resolution,[status(thm)],[f5210,f1471])).
% 171.89/37.24 fof(f22109,plain,(
% 171.89/37.24 c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,sK7_skl,c_If(tc_Nat_Onat,c_fequal(sK8_skl,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,sK8_skl)))))=c_Nat_OSuc(c_Polynomial_Odegree(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)))),
% 171.89/37.24 inference(backward_subsumption_resolution,[status(thm)],[f5095,f20610])).
% 171.89/37.24 fof(f22110,plain,(
% 171.89/37.24 ![X0,X1]: (~sP6_prd(X0,X1))),
% 171.89/37.24 inference(backward_subsumption_resolution,[status(thm)],[f4660,f20610])).
% 171.89/37.24 fof(f22116,plain,(
% 171.89/37.24 ![X0,X1,X2]: (X0=v_c____|~c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(X1,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,X1))),X2))=c_Nat_OSuc(c_Polynomial_Odegree(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)))|~hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)),sK31_skl(X1,X2,X0))=hAPP(hAPP(c_Groups_Otimes__class_Otimes(t_a),hAPP(hAPP(c_Power_Opower__class_Opower(t_a),sK31_skl(X1,X2,X0)),X2)),hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,X0,X1)),sK31_skl(X1,X2,X0))))),
% 171.89/37.24 inference(backward_subsumption_resolution,[status(thm)],[f5082,f22110])).
% 171.89/37.24 fof(f32750,plain,(
% 171.89/37.24 sK6_skl=v_c____|~c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(sK8_skl,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,sK8_skl))),sK7_skl))=c_Nat_OSuc(c_Polynomial_Odegree(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)))),
% 146.26/37.35 inference(resolution,[status(thm)],[f22116,f5213])).
% 146.26/37.35 fof(f32753,plain,(
% 146.26/37.35 sK6_skl=v_c____|~c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,sK7_skl,c_If(tc_Nat_Onat,c_fequal(sK8_skl,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,sK8_skl)))))=c_Nat_OSuc(c_Polynomial_Odegree(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)))),
% 146.26/37.35 inference(forward_demodulation,[status(thm)],[f1408,f32750])).
% 146.26/37.35 fof(f32754,plain,(
% 146.26/37.35 sK6_skl=v_c____|~c_Nat_OSuc(c_Polynomial_Odegree(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)))=c_Nat_OSuc(c_Polynomial_Odegree(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)))),
% 146.26/37.35 inference(forward_demodulation,[status(thm)],[f22109,f32753])).
% 146.26/37.35 fof(f32755,plain,(
% 146.26/37.35 sK6_skl=v_c____),
% 146.26/37.35 inference(trivial_equality_resolution,[status(thm)],[f32754])).
% 146.26/37.35 fof(f32756,plain,(
% 146.26/37.35 $false),
% 146.26/37.35 inference(forward_subsumption_resolution,[status(thm)],[f32755,f5206])).
% 146.26/37.35 % SZS output end CNFRefutation for theBenchmark.p
% 14.73/37.53 % Elapsed time: 22.106292 seconds
% 14.73/37.53 % CPU time: 173.510275 seconds
% 14.73/37.53 % Total memory used: 1.312 GB
% 14.73/37.53 % Net memory used: 1.276 GB
%------------------------------------------------------------------------------