%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW247+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:52 PM UTC 2026
% Result : Theorem 19.77s 3.20s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWW247+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.45 % Computer : n006.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:43:42 UTC 2026
% 0.19/0.46 % CPUTime :
% 0.37/0.64 % Drodi V4.1.1
% 19.77/3.20 % Refutation found
% 19.77/3.20 % SZS status Theorem for theBenchmark: Theorem is valid
% 19.77/3.20 % SZS output start CNFRefutation for theBenchmark
% 19.77/3.20 fof(f3,axiom,(
% 19.77/3.20 ( class_Rings_Oidom(t_a)=> (! [B_z] :( B_z != c_Groups_Ozero__class_Ozero(t_a)=> hAPP(c_Polynomial_Opoly(t_a,v_cs____),B_z) = c_Groups_Ozero__class_Ozero(t_a) ) )) ),
% 19.77/3.20 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 19.77/3.20 fof(f6,axiom,(
% 19.77/3.20 (! [V_q_2,V_b_2,V_pa_2,V_a_2,T_b] :( class_Groups_Ozero(T_b)=> ( hAPP(hAPP(c_Polynomial_OpCons(T_b),V_a_2),V_pa_2) = hAPP(hAPP(c_Polynomial_OpCons(T_b),V_b_2),V_q_2)<=> ( V_a_2 = V_b_2& V_pa_2 = V_q_2 ) ) ) )),
% 19.77/3.20 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 19.77/3.20 fof(f10,axiom,(
% 19.77/3.20 (! [V_p,T_a] :( class_Groups_Ozero(T_a)=> ~ (! [B_a,B_q] : V_p != hAPP(hAPP(c_Polynomial_OpCons(T_a),B_a),B_q) )) )),
% 19.77/3.20 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 19.77/3.20 fof(f12,axiom,(
% 19.77/3.20 (! [V_x,V_p,V_a,T_a] :( class_Rings_Ocomm__semiring__0(T_a)=> hAPP(c_Polynomial_Opoly(T_a,hAPP(hAPP(c_Polynomial_OpCons(T_a),V_a),V_p)),V_x) = hAPP(hAPP(c_Groups_Oplus__class_Oplus(T_a),V_a),hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_x),hAPP(c_Polynomial_Opoly(T_a,V_p),V_x))) ) )),
% 19.77/3.20 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 19.77/3.20 fof(f15,axiom,(
% 19.77/3.20 (! [V_c,V_p,T_a] :( class_Rings_Ocomm__semiring__0(T_a)=> hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(T_a)),V_p),hAPP(hAPP(c_Polynomial_Osmult(T_a),V_c),c_Polynomial_Osynthetic__div(T_a,V_p,V_c))) = hAPP(hAPP(c_Polynomial_OpCons(T_a),hAPP(c_Polynomial_Opoly(T_a,V_p),V_c)),c_Polynomial_Osynthetic__div(T_a,V_p,V_c)) ) )),
% 19.77/3.20 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 19.77/3.20 fof(f18,axiom,(
% 19.77/3.20 (! [V_p,T_a] :( class_Rings_Ocomm__semiring__0(T_a)=> hAPP(hAPP(c_Polynomial_Osmult(T_a),c_Groups_Ozero__class_Ozero(T_a)),V_p) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)) ) )),
% 19.77/3.20 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 19.77/3.20 fof(f24,axiom,(
% 19.77/3.20 (! [V_a,T_a] :( class_Rings_Ocomm__semiring__0(T_a)=> hAPP(hAPP(c_Polynomial_Osmult(T_a),V_a),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)) ) )),
% 19.77/3.20 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 19.77/3.20 fof(f26,axiom,(
% 19.77/3.20 (! [V_p,T_a] :( class_Groups_Ocomm__monoid__add(T_a)=> hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(T_a)),V_p),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))) = V_p ) )),
% 19.77/3.20 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 19.77/3.20 fof(f33,axiom,(
% 19.77/3.20 (! [V_pa_2,V_a_2,T_b] :( class_Groups_Ozero(T_b)=> ( hAPP(hAPP(c_Polynomial_OpCons(T_b),V_a_2),V_pa_2) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_b))<=> ( V_a_2 = c_Groups_Ozero__class_Ozero(T_b)& V_pa_2 = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_b)) ) ) ) )),
% 19.77/3.20 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 19.77/3.20 fof(f35,axiom,(
% 19.77/3.20 (! [V_x,V_p,V_a,T_a] :( class_Rings_Ocomm__semiring__0(T_a)=> hAPP(c_Polynomial_Opoly(T_a,hAPP(hAPP(c_Polynomial_Osmult(T_a),V_a),V_p)),V_x) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_a),hAPP(c_Polynomial_Opoly(T_a,V_p),V_x)) ) )),
% 19.77/3.20 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 19.77/3.20 fof(f53,axiom,(
% 19.77/3.20 (! [V_a_2,V_pa_2,T_b] :( class_Rings_Oidom(T_b)=> ( hAPP(c_Polynomial_Opoly(T_b,V_pa_2),V_a_2) = c_Groups_Ozero__class_Ozero(T_b)<=> ( V_pa_2 = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_b))| c_Polynomial_Oorder(T_b,V_a_2,V_pa_2) != c_Groups_Ozero__class_Ozero(tc_Nat_Onat) ) ) ) )),
% 19.77/3.20 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 19.77/3.20 fof(f1005,axiom,(
% 19.77/3.20 (! [T] :( class_Rings_Oidom(T)=> class_Groups_Ocomm__monoid__add(T) ) )),
% 19.77/3.20 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 19.77/3.20 fof(f1007,axiom,(
% 19.77/3.20 (! [T] :( class_Rings_Oidom(T)=> class_Rings_Ocomm__semiring__0(T) ) )),
% 19.77/3.20 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 19.77/3.20 fof(f1024,axiom,(
% 19.77/3.20 (! [T] :( class_Rings_Oidom(T)=> class_Groups_Ozero(T) ) )),
% 19.77/3.20 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 19.77/3.20 fof(f1213,conjecture,(
% 19.77/3.20 hAPP(c_Polynomial_Opoly(t_a,hAPP(hAPP(c_Polynomial_OpCons(t_a),v_c____),v_cs____)),v_x____) = hAPP(c_Polynomial_Opoly(t_a,hAPP(hAPP(c_Polynomial_OpCons(t_a),v_c____),v_cs____)),v_y____) ),
% 19.77/3.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 19.77/3.21 fof(f1214,negated_conjecture,(
% 19.77/3.21 ~(hAPP(c_Polynomial_Opoly(t_a,hAPP(hAPP(c_Polynomial_OpCons(t_a),v_c____),v_cs____)),v_x____) = hAPP(c_Polynomial_Opoly(t_a,hAPP(hAPP(c_Polynomial_OpCons(t_a),v_c____),v_cs____)),v_y____) )),
% 19.77/3.21 inference(negated_conjecture,[status(cth)],[f1213])).
% 19.77/3.21 fof(f1215,hypothesis,(
% 19.77/3.21 class_Rings_Oidom(t_a) ),
% 19.77/3.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 19.77/3.21 fof(f1221,plain,(
% 19.77/3.21 ~class_Rings_Oidom(t_a)|(![B_z]: (B_z=c_Groups_Ozero__class_Ozero(t_a)|hAPP(c_Polynomial_Opoly(t_a,v_cs____),B_z)=c_Groups_Ozero__class_Ozero(t_a)))),
% 19.77/3.21 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 19.77/3.21 fof(f1222,plain,(
% 19.77/3.21 ![X0]: (~class_Rings_Oidom(t_a)|X0=c_Groups_Ozero__class_Ozero(t_a)|hAPP(c_Polynomial_Opoly(t_a,v_cs____),X0)=c_Groups_Ozero__class_Ozero(t_a))),
% 19.77/3.21 inference(cnf_transformation,[status(thm)],[f1221])).
% 19.77/3.21 fof(f1230,plain,(
% 19.77/3.21 ![V_q_2,V_b_2,V_pa_2,V_a_2,T_b]: (~class_Groups_Ozero(T_b)|(hAPP(hAPP(c_Polynomial_OpCons(T_b),V_a_2),V_pa_2)=hAPP(hAPP(c_Polynomial_OpCons(T_b),V_b_2),V_q_2)<=>(V_a_2=V_b_2&V_pa_2=V_q_2)))),
% 19.77/3.21 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 19.77/3.21 fof(f1231,plain,(
% 19.77/3.21 ![V_q_2,V_b_2,V_pa_2,V_a_2,T_b]: (~class_Groups_Ozero(T_b)|((~hAPP(hAPP(c_Polynomial_OpCons(T_b),V_a_2),V_pa_2)=hAPP(hAPP(c_Polynomial_OpCons(T_b),V_b_2),V_q_2)|(V_a_2=V_b_2&V_pa_2=V_q_2))&(hAPP(hAPP(c_Polynomial_OpCons(T_b),V_a_2),V_pa_2)=hAPP(hAPP(c_Polynomial_OpCons(T_b),V_b_2),V_q_2)|(~V_a_2=V_b_2|~V_pa_2=V_q_2))))),
% 19.77/3.21 inference(NNF_transformation,[status(thm)],[f1230])).
% 19.77/3.21 fof(f1232,plain,(
% 19.77/3.21 ![T_b]: (~class_Groups_Ozero(T_b)|((![V_q_2,V_b_2,V_pa_2,V_a_2]: (~hAPP(hAPP(c_Polynomial_OpCons(T_b),V_a_2),V_pa_2)=hAPP(hAPP(c_Polynomial_OpCons(T_b),V_b_2),V_q_2)|(V_a_2=V_b_2&V_pa_2=V_q_2)))&(![V_q_2,V_b_2,V_pa_2,V_a_2]: (hAPP(hAPP(c_Polynomial_OpCons(T_b),V_a_2),V_pa_2)=hAPP(hAPP(c_Polynomial_OpCons(T_b),V_b_2),V_q_2)|(~V_a_2=V_b_2|~V_pa_2=V_q_2)))))),
% 19.77/3.21 inference(miniscoping,[status(thm)],[f1231])).
% 19.77/3.21 fof(f1233,plain,(
% 19.77/3.21 ![X0,X1,X2,X3,X4]: (~class_Groups_Ozero(X0)|~hAPP(hAPP(c_Polynomial_OpCons(X0),X1),X2)=hAPP(hAPP(c_Polynomial_OpCons(X0),X3),X4)|X1=X3)),
% 19.77/3.21 inference(cnf_transformation,[status(thm)],[f1232])).
% 19.77/3.21 fof(f1247,plain,(
% 19.77/3.21 ![V_p,T_a]: (~class_Groups_Ozero(T_a)|(?[B_a,B_q]: V_p=hAPP(hAPP(c_Polynomial_OpCons(T_a),B_a),B_q)))),
% 19.77/3.21 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 19.77/3.21 fof(f1248,plain,(
% 19.77/3.21 ![T_a]: (~class_Groups_Ozero(T_a)|(![V_p]: ?[B_a,B_q]: V_p=hAPP(hAPP(c_Polynomial_OpCons(T_a),B_a),B_q)))),
% 19.77/3.21 inference(miniscoping,[status(thm)],[f1247])).
% 19.77/3.21 fof(f1249,plain,(
% 19.77/3.21 ![T_a]: (~class_Groups_Ozero(T_a)|(![V_p]: V_p=hAPP(hAPP(c_Polynomial_OpCons(T_a),sK3_skl(V_p,T_a)),sK4_skl(V_p,T_a))))),
% 19.77/3.21 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl,sK4_skl]),skolemize(B_a,sK3_skl(V_p,T_a)),skolemize(B_q,sK4_skl(V_p,T_a))],[f1248])).
% 19.77/3.21 fof(f1250,plain,(
% 19.77/3.21 ![X0,X1]: (~class_Groups_Ozero(X0)|X1=hAPP(hAPP(c_Polynomial_OpCons(X0),sK3_skl(X1,X0)),sK4_skl(X1,X0)))),
% 19.77/3.21 inference(cnf_transformation,[status(thm)],[f1249])).
% 19.77/3.21 fof(f1254,plain,(
% 19.77/3.21 ![V_x,V_p,V_a,T_a]: (~class_Rings_Ocomm__semiring__0(T_a)|hAPP(c_Polynomial_Opoly(T_a,hAPP(hAPP(c_Polynomial_OpCons(T_a),V_a),V_p)),V_x)=hAPP(hAPP(c_Groups_Oplus__class_Oplus(T_a),V_a),hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_x),hAPP(c_Polynomial_Opoly(T_a,V_p),V_x))))),
% 19.77/3.21 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 19.77/3.21 fof(f1255,plain,(
% 19.77/3.21 ![T_a]: (~class_Rings_Ocomm__semiring__0(T_a)|(![V_x,V_p,V_a]: hAPP(c_Polynomial_Opoly(T_a,hAPP(hAPP(c_Polynomial_OpCons(T_a),V_a),V_p)),V_x)=hAPP(hAPP(c_Groups_Oplus__class_Oplus(T_a),V_a),hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_x),hAPP(c_Polynomial_Opoly(T_a,V_p),V_x)))))),
% 19.77/3.21 inference(miniscoping,[status(thm)],[f1254])).
% 19.77/3.21 fof(f1256,plain,(
% 19.77/3.21 ![X0,X1,X2,X3]: (~class_Rings_Ocomm__semiring__0(X0)|hAPP(c_Polynomial_Opoly(X0,hAPP(hAPP(c_Polynomial_OpCons(X0),X1),X2)),X3)=hAPP(hAPP(c_Groups_Oplus__class_Oplus(X0),X1),hAPP(hAPP(c_Groups_Otimes__class_Otimes(X0),X3),hAPP(c_Polynomial_Opoly(X0,X2),X3))))),
% 19.77/3.21 inference(cnf_transformation,[status(thm)],[f1255])).
% 19.77/3.21 fof(f1265,plain,(
% 19.77/3.21 ![V_c,V_p,T_a]: (~class_Rings_Ocomm__semiring__0(T_a)|hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(T_a)),V_p),hAPP(hAPP(c_Polynomial_Osmult(T_a),V_c),c_Polynomial_Osynthetic__div(T_a,V_p,V_c)))=hAPP(hAPP(c_Polynomial_OpCons(T_a),hAPP(c_Polynomial_Opoly(T_a,V_p),V_c)),c_Polynomial_Osynthetic__div(T_a,V_p,V_c)))),
% 19.77/3.21 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 19.77/3.21 fof(f1266,plain,(
% 19.77/3.21 ![T_a]: (~class_Rings_Ocomm__semiring__0(T_a)|(![V_c,V_p]: hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(T_a)),V_p),hAPP(hAPP(c_Polynomial_Osmult(T_a),V_c),c_Polynomial_Osynthetic__div(T_a,V_p,V_c)))=hAPP(hAPP(c_Polynomial_OpCons(T_a),hAPP(c_Polynomial_Opoly(T_a,V_p),V_c)),c_Polynomial_Osynthetic__div(T_a,V_p,V_c))))),
% 19.77/3.21 inference(miniscoping,[status(thm)],[f1265])).
% 19.77/3.21 fof(f1267,plain,(
% 19.77/3.21 ![X0,X1,X2]: (~class_Rings_Ocomm__semiring__0(X0)|hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(X0)),X1),hAPP(hAPP(c_Polynomial_Osmult(X0),X2),c_Polynomial_Osynthetic__div(X0,X1,X2)))=hAPP(hAPP(c_Polynomial_OpCons(X0),hAPP(c_Polynomial_Opoly(X0,X1),X2)),c_Polynomial_Osynthetic__div(X0,X1,X2)))),
% 19.77/3.21 inference(cnf_transformation,[status(thm)],[f1266])).
% 19.77/3.21 fof(f1273,plain,(
% 19.77/3.21 ![V_p,T_a]: (~class_Rings_Ocomm__semiring__0(T_a)|hAPP(hAPP(c_Polynomial_Osmult(T_a),c_Groups_Ozero__class_Ozero(T_a)),V_p)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)))),
% 19.77/3.21 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 19.77/3.21 fof(f1274,plain,(
% 19.77/3.21 ![T_a]: (~class_Rings_Ocomm__semiring__0(T_a)|(![V_p]: hAPP(hAPP(c_Polynomial_Osmult(T_a),c_Groups_Ozero__class_Ozero(T_a)),V_p)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))))),
% 19.77/3.21 inference(miniscoping,[status(thm)],[f1273])).
% 19.77/3.21 fof(f1275,plain,(
% 19.77/3.21 ![X0,X1]: (~class_Rings_Ocomm__semiring__0(X0)|hAPP(hAPP(c_Polynomial_Osmult(X0),c_Groups_Ozero__class_Ozero(X0)),X1)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)))),
% 19.77/3.21 inference(cnf_transformation,[status(thm)],[f1274])).
% 19.77/3.21 fof(f1291,plain,(
% 19.77/3.21 ![V_a,T_a]: (~class_Rings_Ocomm__semiring__0(T_a)|hAPP(hAPP(c_Polynomial_Osmult(T_a),V_a),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)))=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)))),
% 19.77/3.21 inference(pre_NNF_transformation,[status(thm)],[f24])).
% 19.77/3.21 fof(f1292,plain,(
% 19.77/3.21 ![T_a]: (~class_Rings_Ocomm__semiring__0(T_a)|(![V_a]: hAPP(hAPP(c_Polynomial_Osmult(T_a),V_a),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)))=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))))),
% 19.77/3.21 inference(miniscoping,[status(thm)],[f1291])).
% 19.77/3.21 fof(f1293,plain,(
% 19.77/3.21 ![X0,X1]: (~class_Rings_Ocomm__semiring__0(X0)|hAPP(hAPP(c_Polynomial_Osmult(X0),X1),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)))=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)))),
% 19.77/3.21 inference(cnf_transformation,[status(thm)],[f1292])).
% 19.77/3.21 fof(f1297,plain,(
% 19.77/3.21 ![V_p,T_a]: (~class_Groups_Ocomm__monoid__add(T_a)|hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(T_a)),V_p),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)))=V_p)),
% 19.77/3.21 inference(pre_NNF_transformation,[status(thm)],[f26])).
% 19.77/3.21 fof(f1298,plain,(
% 19.77/3.21 ![T_a]: (~class_Groups_Ocomm__monoid__add(T_a)|(![V_p]: hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(T_a)),V_p),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)))=V_p))),
% 19.77/3.21 inference(miniscoping,[status(thm)],[f1297])).
% 19.77/3.21 fof(f1299,plain,(
% 19.77/3.21 ![X0,X1]: (~class_Groups_Ocomm__monoid__add(X0)|hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(X0)),X1),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)))=X1)),
% 19.77/3.21 inference(cnf_transformation,[status(thm)],[f1298])).
% 19.77/3.21 fof(f1320,plain,(
% 19.77/3.21 ![V_pa_2,V_a_2,T_b]: (~class_Groups_Ozero(T_b)|(hAPP(hAPP(c_Polynomial_OpCons(T_b),V_a_2),V_pa_2)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_b))<=>(V_a_2=c_Groups_Ozero__class_Ozero(T_b)&V_pa_2=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_b)))))),
% 19.77/3.21 inference(pre_NNF_transformation,[status(thm)],[f33])).
% 19.77/3.21 fof(f1321,plain,(
% 19.77/3.21 ![V_pa_2,V_a_2,T_b]: (~class_Groups_Ozero(T_b)|((~hAPP(hAPP(c_Polynomial_OpCons(T_b),V_a_2),V_pa_2)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_b))|(V_a_2=c_Groups_Ozero__class_Ozero(T_b)&V_pa_2=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_b))))&(hAPP(hAPP(c_Polynomial_OpCons(T_b),V_a_2),V_pa_2)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_b))|(~V_a_2=c_Groups_Ozero__class_Ozero(T_b)|~V_pa_2=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_b))))))),
% 19.77/3.21 inference(NNF_transformation,[status(thm)],[f1320])).
% 19.77/3.21 fof(f1322,plain,(
% 19.77/3.21 ![T_b]: (~class_Groups_Ozero(T_b)|((![V_pa_2,V_a_2]: (~hAPP(hAPP(c_Polynomial_OpCons(T_b),V_a_2),V_pa_2)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_b))|(V_a_2=c_Groups_Ozero__class_Ozero(T_b)&V_pa_2=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_b)))))&(![V_pa_2,V_a_2]: (hAPP(hAPP(c_Polynomial_OpCons(T_b),V_a_2),V_pa_2)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_b))|(~V_a_2=c_Groups_Ozero__class_Ozero(T_b)|~V_pa_2=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_b)))))))),
% 19.77/3.21 inference(miniscoping,[status(thm)],[f1321])).
% 19.77/3.21 fof(f1323,plain,(
% 19.77/3.21 ![X0,X1,X2]: (~class_Groups_Ozero(X0)|~hAPP(hAPP(c_Polynomial_OpCons(X0),X1),X2)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X0))|X1=c_Groups_Ozero__class_Ozero(X0))),
% 19.77/3.21 inference(cnf_transformation,[status(thm)],[f1322])).
% 19.77/3.21 fof(f1332,plain,(
% 19.77/3.21 ![V_x,V_p,V_a,T_a]: (~class_Rings_Ocomm__semiring__0(T_a)|hAPP(c_Polynomial_Opoly(T_a,hAPP(hAPP(c_Polynomial_Osmult(T_a),V_a),V_p)),V_x)=hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_a),hAPP(c_Polynomial_Opoly(T_a,V_p),V_x)))),
% 19.77/3.21 inference(pre_NNF_transformation,[status(thm)],[f35])).
% 19.77/3.21 fof(f1333,plain,(
% 19.77/3.21 ![T_a]: (~class_Rings_Ocomm__semiring__0(T_a)|(![V_x,V_p,V_a]: hAPP(c_Polynomial_Opoly(T_a,hAPP(hAPP(c_Polynomial_Osmult(T_a),V_a),V_p)),V_x)=hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_a),hAPP(c_Polynomial_Opoly(T_a,V_p),V_x))))),
% 19.77/3.21 inference(miniscoping,[status(thm)],[f1332])).
% 19.77/3.21 fof(f1334,plain,(
% 19.77/3.21 ![X0,X1,X2,X3]: (~class_Rings_Ocomm__semiring__0(X0)|hAPP(c_Polynomial_Opoly(X0,hAPP(hAPP(c_Polynomial_Osmult(X0),X1),X2)),X3)=hAPP(hAPP(c_Groups_Otimes__class_Otimes(X0),X1),hAPP(c_Polynomial_Opoly(X0,X2),X3)))),
% 19.77/3.21 inference(cnf_transformation,[status(thm)],[f1333])).
% 19.77/3.21 fof(f1390,plain,(
% 19.77/3.21 ![V_a_2,V_pa_2,T_b]: (~class_Rings_Oidom(T_b)|(hAPP(c_Polynomial_Opoly(T_b,V_pa_2),V_a_2)=c_Groups_Ozero__class_Ozero(T_b)<=>(V_pa_2=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_b))|~c_Polynomial_Oorder(T_b,V_a_2,V_pa_2)=c_Groups_Ozero__class_Ozero(tc_Nat_Onat))))),
% 19.77/3.21 inference(pre_NNF_transformation,[status(thm)],[f53])).
% 19.77/3.21 fof(f1391,plain,(
% 19.77/3.21 ![V_a_2,V_pa_2,T_b]: (~class_Rings_Oidom(T_b)|((~hAPP(c_Polynomial_Opoly(T_b,V_pa_2),V_a_2)=c_Groups_Ozero__class_Ozero(T_b)|(V_pa_2=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_b))|~c_Polynomial_Oorder(T_b,V_a_2,V_pa_2)=c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))&(hAPP(c_Polynomial_Opoly(T_b,V_pa_2),V_a_2)=c_Groups_Ozero__class_Ozero(T_b)|(~V_pa_2=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_b))&c_Polynomial_Oorder(T_b,V_a_2,V_pa_2)=c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))))),
% 19.77/3.21 inference(NNF_transformation,[status(thm)],[f1390])).
% 19.77/3.21 fof(f1392,plain,(
% 19.77/3.21 ![T_b]: (~class_Rings_Oidom(T_b)|((![V_a_2,V_pa_2]: (~hAPP(c_Polynomial_Opoly(T_b,V_pa_2),V_a_2)=c_Groups_Ozero__class_Ozero(T_b)|(V_pa_2=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_b))|~c_Polynomial_Oorder(T_b,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_b,V_pa_2),V_a_2)=c_Groups_Ozero__class_Ozero(T_b)|(~V_pa_2=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_b))&c_Polynomial_Oorder(T_b,V_a_2,V_pa_2)=c_Groups_Ozero__class_Ozero(tc_Nat_Onat))))))),
% 19.77/3.21 inference(miniscoping,[status(thm)],[f1391])).
% 19.77/3.21 fof(f1394,plain,(
% 19.77/3.21 ![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)))),
% 19.77/3.21 inference(cnf_transformation,[status(thm)],[f1392])).
% 19.77/3.21 fof(f4457,plain,(
% 19.77/3.21 ![T]: (~class_Rings_Oidom(T)|class_Groups_Ocomm__monoid__add(T))),
% 19.77/3.21 inference(pre_NNF_transformation,[status(thm)],[f1005])).
% 19.77/3.21 fof(f4458,plain,(
% 19.77/3.21 ![X0]: (~class_Rings_Oidom(X0)|class_Groups_Ocomm__monoid__add(X0))),
% 19.77/3.21 inference(cnf_transformation,[status(thm)],[f4457])).
% 19.77/3.21 fof(f4461,plain,(
% 19.77/3.21 ![T]: (~class_Rings_Oidom(T)|class_Rings_Ocomm__semiring__0(T))),
% 19.77/3.21 inference(pre_NNF_transformation,[status(thm)],[f1007])).
% 19.77/3.21 fof(f4462,plain,(
% 19.77/3.21 ![X0]: (~class_Rings_Oidom(X0)|class_Rings_Ocomm__semiring__0(X0))),
% 19.77/3.21 inference(cnf_transformation,[status(thm)],[f4461])).
% 19.77/3.21 fof(f4495,plain,(
% 19.77/3.21 ![T]: (~class_Rings_Oidom(T)|class_Groups_Ozero(T))),
% 19.77/3.21 inference(pre_NNF_transformation,[status(thm)],[f1024])).
% 19.77/3.21 fof(f4496,plain,(
% 19.77/3.21 ![X0]: (~class_Rings_Oidom(X0)|class_Groups_Ozero(X0))),
% 19.77/3.21 inference(cnf_transformation,[status(thm)],[f4495])).
% 19.77/3.21 fof(f4762,plain,(
% 19.77/3.21 ~hAPP(c_Polynomial_Opoly(t_a,hAPP(hAPP(c_Polynomial_OpCons(t_a),v_c____),v_cs____)),v_x____)=hAPP(c_Polynomial_Opoly(t_a,hAPP(hAPP(c_Polynomial_OpCons(t_a),v_c____),v_cs____)),v_y____)),
% 19.77/3.21 inference(cnf_transformation,[status(thm)],[f1214])).
% 19.77/3.21 fof(f4763,plain,(
% 19.77/3.21 class_Rings_Oidom(t_a)),
% 19.77/3.21 inference(cnf_transformation,[status(thm)],[f1215])).
% 19.77/3.21 fof(f4785,plain,(
% 19.77/3.21 ![X0,X1]: (~class_Rings_Oidom(X0)|hAPP(c_Polynomial_Opoly(X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X0))),X1)=c_Groups_Ozero__class_Ozero(X0))),
% 19.77/3.21 inference(destructive_equality_resolution,[status(thm)],[f1394])).
% 19.77/3.21 fof(f5017,plain,(
% 19.77/3.21 ![X0]: (X0=c_Groups_Ozero__class_Ozero(t_a)|hAPP(c_Polynomial_Opoly(t_a,v_cs____),X0)=c_Groups_Ozero__class_Ozero(t_a))),
% 19.77/3.21 inference(backward_subsumption_resolution,[status(thm)],[f1222,f4763])).
% 19.77/3.21 fof(f5036,plain,(
% 19.77/3.21 ![X0]: (hAPP(c_Polynomial_Opoly(t_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),X0)=c_Groups_Ozero__class_Ozero(t_a))),
% 19.77/3.21 inference(resolution,[status(thm)],[f4785,f4763])).
% 19.77/3.21 fof(f8112,plain,(
% 19.77/3.21 class_Groups_Ocomm__monoid__add(t_a)),
% 19.77/3.21 inference(resolution,[status(thm)],[f4458,f4763])).
% 19.77/3.21 fof(f8113,plain,(
% 19.77/3.21 ![X0]: (hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(t_a)),X0),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))=X0)),
% 19.77/3.21 inference(resolution,[status(thm)],[f8112,f1299])).
% 19.77/3.21 fof(f8120,plain,(
% 19.77/3.21 class_Rings_Ocomm__semiring__0(t_a)),
% 19.77/3.21 inference(resolution,[status(thm)],[f4462,f4763])).
% 19.77/3.21 fof(f8128,plain,(
% 19.77/3.21 ![X0]: (hAPP(hAPP(c_Polynomial_Osmult(t_a),X0),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))),
% 19.77/3.21 inference(resolution,[status(thm)],[f8120,f1293])).
% 19.77/3.21 fof(f8133,plain,(
% 19.77/3.21 ![X0]: (hAPP(hAPP(c_Polynomial_Osmult(t_a),c_Groups_Ozero__class_Ozero(t_a)),X0)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))),
% 19.77/3.21 inference(resolution,[status(thm)],[f8120,f1275])).
% 19.77/3.21 fof(f8135,plain,(
% 19.77/3.21 ![X0,X1]: (hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(t_a)),X0),hAPP(hAPP(c_Polynomial_Osmult(t_a),X1),c_Polynomial_Osynthetic__div(t_a,X0,X1)))=hAPP(hAPP(c_Polynomial_OpCons(t_a),hAPP(c_Polynomial_Opoly(t_a,X0),X1)),c_Polynomial_Osynthetic__div(t_a,X0,X1)))),
% 19.77/3.21 inference(resolution,[status(thm)],[f8120,f1267])).
% 19.77/3.21 fof(f8137,plain,(
% 19.77/3.21 ![X0,X1,X2]: (hAPP(c_Polynomial_Opoly(t_a,hAPP(hAPP(c_Polynomial_OpCons(t_a),X0),X1)),X2)=hAPP(hAPP(c_Groups_Oplus__class_Oplus(t_a),X0),hAPP(hAPP(c_Groups_Otimes__class_Otimes(t_a),X2),hAPP(c_Polynomial_Opoly(t_a,X1),X2))))),
% 19.77/3.21 inference(resolution,[status(thm)],[f8120,f1256])).
% 19.77/3.21 fof(f8397,plain,(
% 19.77/3.21 ![X0,X1,X2]: (hAPP(c_Polynomial_Opoly(t_a,hAPP(hAPP(c_Polynomial_Osmult(t_a),X0),X1)),X2)=hAPP(hAPP(c_Groups_Otimes__class_Otimes(t_a),X0),hAPP(c_Polynomial_Opoly(t_a,X1),X2)))),
% 19.77/3.21 inference(resolution,[status(thm)],[f1334,f8120])).
% 19.77/3.21 fof(f9364,plain,(
% 19.77/3.21 ![X0]: (hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(t_a)),X0),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))=hAPP(hAPP(c_Polynomial_OpCons(t_a),hAPP(c_Polynomial_Opoly(t_a,X0),c_Groups_Ozero__class_Ozero(t_a))),c_Polynomial_Osynthetic__div(t_a,X0,c_Groups_Ozero__class_Ozero(t_a))))),
% 19.77/3.21 inference(paramodulation,[status(thm)],[f8133,f8135])).
% 19.77/3.21 fof(f9373,plain,(
% 19.77/3.21 ![X0]: (X0=hAPP(hAPP(c_Polynomial_OpCons(t_a),hAPP(c_Polynomial_Opoly(t_a,X0),c_Groups_Ozero__class_Ozero(t_a))),c_Polynomial_Osynthetic__div(t_a,X0,c_Groups_Ozero__class_Ozero(t_a))))),
% 19.77/3.21 inference(forward_demodulation,[status(thm)],[f8113,f9364])).
% 19.77/3.21 fof(f9417,plain,(
% 19.77/3.21 ![X0,X1]: (hAPP(c_Polynomial_Opoly(t_a,hAPP(hAPP(c_Polynomial_OpCons(t_a),X0),v_cs____)),X1)=hAPP(hAPP(c_Groups_Oplus__class_Oplus(t_a),X0),hAPP(hAPP(c_Groups_Otimes__class_Otimes(t_a),X1),c_Groups_Ozero__class_Ozero(t_a)))|X1=c_Groups_Ozero__class_Ozero(t_a))),
% 19.77/3.21 inference(paramodulation,[status(thm)],[f5017,f8137])).
% 19.77/3.21 fof(f9447,plain,(
% 19.77/3.21 class_Groups_Ozero(t_a)),
% 19.77/3.21 inference(resolution,[status(thm)],[f4496,f4763])).
% 19.77/3.21 fof(f9449,plain,(
% 19.77/3.21 ![X0,X1]: (~hAPP(hAPP(c_Polynomial_OpCons(t_a),X0),X1)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))|X0=c_Groups_Ozero__class_Ozero(t_a))),
% 19.77/3.21 inference(resolution,[status(thm)],[f9447,f1323])).
% 19.77/3.21 fof(f9451,plain,(
% 19.77/3.21 ![X0]: (X0=hAPP(hAPP(c_Polynomial_OpCons(t_a),sK3_skl(X0,t_a)),sK4_skl(X0,t_a)))),
% 19.77/3.21 inference(resolution,[status(thm)],[f9447,f1250])).
% 19.77/3.21 fof(f9453,plain,(
% 19.77/3.21 ![X0,X1,X2,X3]: (~hAPP(hAPP(c_Polynomial_OpCons(t_a),X0),X1)=hAPP(hAPP(c_Polynomial_OpCons(t_a),X2),X3)|X0=X2)),
% 19.77/3.21 inference(resolution,[status(thm)],[f9447,f1233])).
% 19.77/3.21 fof(f9467,plain,(
% 19.77/3.21 sK3_skl(c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)),t_a)=c_Groups_Ozero__class_Ozero(t_a)),
% 19.77/3.21 inference(resolution,[status(thm)],[f9449,f9451])).
% 19.77/3.21 fof(f9494,plain,(
% 19.77/3.21 ![X0,X1]: (X0=sK3_skl(hAPP(hAPP(c_Polynomial_OpCons(t_a),X0),X1),t_a))),
% 19.77/3.21 inference(resolution,[status(thm)],[f9453,f9451])).
% 19.77/3.21 fof(f9543,plain,(
% 19.77/3.21 ![X0]: (hAPP(c_Polynomial_Opoly(t_a,X0),c_Groups_Ozero__class_Ozero(t_a))=sK3_skl(X0,t_a))),
% 19.77/3.21 inference(paramodulation,[status(thm)],[f9373,f9494])).
% 19.77/3.21 fof(f9828,plain,(
% 19.77/3.21 ![X0,X1]: (hAPP(c_Polynomial_Opoly(t_a,hAPP(hAPP(c_Polynomial_OpCons(t_a),X0),X1)),c_Groups_Ozero__class_Ozero(t_a))=hAPP(hAPP(c_Groups_Oplus__class_Oplus(t_a),X0),hAPP(hAPP(c_Groups_Otimes__class_Otimes(t_a),c_Groups_Ozero__class_Ozero(t_a)),sK3_skl(X1,t_a))))),
% 19.77/3.21 inference(paramodulation,[status(thm)],[f9543,f8137])).
% 19.77/3.21 fof(f9840,plain,(
% 19.77/3.21 ![X0,X1]: (sK3_skl(hAPP(hAPP(c_Polynomial_OpCons(t_a),X0),X1),t_a)=hAPP(hAPP(c_Groups_Oplus__class_Oplus(t_a),X0),hAPP(hAPP(c_Groups_Otimes__class_Otimes(t_a),c_Groups_Ozero__class_Ozero(t_a)),sK3_skl(X1,t_a))))),
% 19.77/3.21 inference(forward_demodulation,[status(thm)],[f9543,f9828])).
% 19.77/3.21 fof(f9841,plain,(
% 19.77/3.21 ![X0,X1]: (X0=hAPP(hAPP(c_Groups_Oplus__class_Oplus(t_a),X0),hAPP(hAPP(c_Groups_Otimes__class_Otimes(t_a),c_Groups_Ozero__class_Ozero(t_a)),sK3_skl(X1,t_a))))),
% 19.77/3.21 inference(forward_demodulation,[status(thm)],[f9494,f9840])).
% 19.77/3.21 fof(f10326,plain,(
% 19.77/3.21 ![X0,X1]: (sK3_skl(hAPP(hAPP(c_Polynomial_Osmult(t_a),X0),X1),t_a)=hAPP(hAPP(c_Groups_Otimes__class_Otimes(t_a),X0),hAPP(c_Polynomial_Opoly(t_a,X1),c_Groups_Ozero__class_Ozero(t_a))))),
% 19.77/3.21 inference(paramodulation,[status(thm)],[f9543,f8397])).
% 19.77/3.21 fof(f10332,plain,(
% 19.77/3.21 ![X0,X1]: (hAPP(c_Polynomial_Opoly(t_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),X0)=hAPP(hAPP(c_Groups_Otimes__class_Otimes(t_a),X1),hAPP(c_Polynomial_Opoly(t_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),X0)))),
% 19.77/3.21 inference(paramodulation,[status(thm)],[f8128,f8397])).
% 19.77/3.21 fof(f10373,plain,(
% 19.77/3.21 ![X0,X1]: (X0=hAPP(hAPP(c_Groups_Oplus__class_Oplus(t_a),X0),sK3_skl(hAPP(hAPP(c_Polynomial_Osmult(t_a),c_Groups_Ozero__class_Ozero(t_a)),X1),t_a)))),
% 19.77/3.21 inference(backward_demodulation,[status(thm)],[f10377,f9841])).
% 19.77/3.21 fof(f10377,plain,(
% 19.77/3.21 ![X0,X1]: (sK3_skl(hAPP(hAPP(c_Polynomial_Osmult(t_a),X0),X1),t_a)=hAPP(hAPP(c_Groups_Otimes__class_Otimes(t_a),X0),sK3_skl(X1,t_a)))),
% 19.77/3.21 inference(forward_demodulation,[status(thm)],[f9543,f10326])).
% 19.77/3.21 fof(f10383,plain,(
% 19.77/3.21 ![X0,X1]: (c_Groups_Ozero__class_Ozero(t_a)=hAPP(hAPP(c_Groups_Otimes__class_Otimes(t_a),X0),hAPP(c_Polynomial_Opoly(t_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),X1)))),
% 19.77/3.21 inference(forward_demodulation,[status(thm)],[f5036,f10332])).
% 19.77/3.21 fof(f10407,plain,(
% 19.77/3.21 ![X0,X1]: (hAPP(c_Polynomial_Opoly(t_a,hAPP(hAPP(c_Polynomial_OpCons(t_a),X0),v_cs____)),X1)=hAPP(hAPP(c_Groups_Oplus__class_Oplus(t_a),X0),c_Groups_Ozero__class_Ozero(t_a))|X1=c_Groups_Ozero__class_Ozero(t_a))),
% 19.77/3.21 inference(backward_demodulation,[status(thm)],[f10411,f9417])).
% 19.77/3.21 fof(f10411,plain,(
% 19.77/3.21 ![X0]: (c_Groups_Ozero__class_Ozero(t_a)=hAPP(hAPP(c_Groups_Otimes__class_Otimes(t_a),X0),c_Groups_Ozero__class_Ozero(t_a)))),
% 19.77/3.25 inference(forward_demodulation,[status(thm)],[f5036,f10383])).
% 19.77/3.25 fof(f10426,plain,(
% 19.77/3.25 ![X0]: (X0=hAPP(hAPP(c_Groups_Oplus__class_Oplus(t_a),X0),sK3_skl(c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)),t_a)))),
% 19.77/3.25 inference(forward_demodulation,[status(thm)],[f8133,f10373])).
% 19.77/3.25 fof(f10427,plain,(
% 19.77/3.25 ![X0]: (X0=hAPP(hAPP(c_Groups_Oplus__class_Oplus(t_a),X0),c_Groups_Ozero__class_Ozero(t_a)))),
% 19.77/3.25 inference(forward_demodulation,[status(thm)],[f9467,f10426])).
% 19.77/3.25 fof(f10451,plain,(
% 19.77/3.25 ![X0,X1]: (hAPP(c_Polynomial_Opoly(t_a,hAPP(hAPP(c_Polynomial_OpCons(t_a),X0),v_cs____)),X1)=X0|X1=c_Groups_Ozero__class_Ozero(t_a))),
% 19.77/3.25 inference(forward_demodulation,[status(thm)],[f10427,f10407])).
% 19.77/3.25 fof(f10814,plain,(
% 19.77/3.25 ~v_c____=hAPP(c_Polynomial_Opoly(t_a,hAPP(hAPP(c_Polynomial_OpCons(t_a),v_c____),v_cs____)),v_y____)|v_x____=c_Groups_Ozero__class_Ozero(t_a)),
% 19.77/3.25 inference(paramodulation,[status(thm)],[f10451,f4762])).
% 19.77/3.25 fof(f11106,plain,(
% 19.77/3.25 v_x____=c_Groups_Ozero__class_Ozero(t_a)|v_y____=c_Groups_Ozero__class_Ozero(t_a)),
% 19.77/3.25 inference(resolution,[status(thm)],[f10814,f10451])).
% 19.77/3.25 fof(f11113,plain,(
% 19.77/3.25 ![X0]: (hAPP(c_Polynomial_Opoly(t_a,X0),v_x____)=sK3_skl(X0,t_a)|v_y____=c_Groups_Ozero__class_Ozero(t_a))),
% 19.77/3.25 inference(paramodulation,[status(thm)],[f11106,f9543])).
% 19.77/3.25 fof(f11212,plain,(
% 19.77/3.25 ~sK3_skl(hAPP(hAPP(c_Polynomial_OpCons(t_a),v_c____),v_cs____),t_a)=hAPP(c_Polynomial_Opoly(t_a,hAPP(hAPP(c_Polynomial_OpCons(t_a),v_c____),v_cs____)),v_y____)|v_y____=c_Groups_Ozero__class_Ozero(t_a)),
% 19.77/3.25 inference(paramodulation,[status(thm)],[f11113,f4762])).
% 19.77/3.25 fof(f11233,plain,(
% 19.77/3.25 ~v_c____=hAPP(c_Polynomial_Opoly(t_a,hAPP(hAPP(c_Polynomial_OpCons(t_a),v_c____),v_cs____)),v_y____)|v_y____=c_Groups_Ozero__class_Ozero(t_a)),
% 19.77/3.25 inference(forward_demodulation,[status(thm)],[f9494,f11212])).
% 19.77/3.25 fof(f11240,plain,(
% 19.77/3.25 ~v_c____=hAPP(c_Polynomial_Opoly(t_a,hAPP(hAPP(c_Polynomial_OpCons(t_a),v_c____),v_cs____)),v_y____)|v_x____=v_y____),
% 19.77/3.25 inference(backward_demodulation,[status(thm)],[f11856,f10814])).
% 19.77/3.25 fof(f11249,plain,(
% 19.77/3.25 ![X0]: (hAPP(c_Polynomial_Opoly(t_a,X0),v_y____)=sK3_skl(X0,t_a))),
% 19.77/3.25 inference(backward_demodulation,[status(thm)],[f11856,f9543])).
% 19.77/3.25 fof(f11856,plain,(
% 19.77/3.25 v_y____=c_Groups_Ozero__class_Ozero(t_a)),
% 19.77/3.25 inference(forward_subsumption_resolution,[status(thm)],[f11233,f10451])).
% 19.77/3.25 fof(f11873,plain,(
% 19.77/3.25 ~hAPP(c_Polynomial_Opoly(t_a,hAPP(hAPP(c_Polynomial_OpCons(t_a),v_c____),v_cs____)),v_x____)=sK3_skl(hAPP(hAPP(c_Polynomial_OpCons(t_a),v_c____),v_cs____),t_a)),
% 19.77/3.25 inference(backward_demodulation,[status(thm)],[f11249,f4762])).
% 19.77/3.25 fof(f11874,plain,(
% 19.77/3.25 ~v_c____=sK3_skl(hAPP(hAPP(c_Polynomial_OpCons(t_a),v_c____),v_cs____),t_a)|v_x____=v_y____),
% 19.77/3.25 inference(backward_demodulation,[status(thm)],[f11249,f11240])).
% 19.77/3.25 fof(f13037,plain,(
% 19.77/3.25 ~hAPP(c_Polynomial_Opoly(t_a,hAPP(hAPP(c_Polynomial_OpCons(t_a),v_c____),v_cs____)),v_x____)=v_c____),
% 19.77/3.25 inference(forward_demodulation,[status(thm)],[f9494,f11873])).
% 19.77/3.25 fof(f13038,plain,(
% 19.77/3.25 ~v_c____=v_c____|v_x____=v_y____),
% 19.77/3.25 inference(forward_demodulation,[status(thm)],[f9494,f11874])).
% 19.77/3.25 fof(f13039,plain,(
% 19.77/3.25 ~hAPP(c_Polynomial_Opoly(t_a,hAPP(hAPP(c_Polynomial_OpCons(t_a),v_c____),v_cs____)),v_y____)=v_c____),
% 19.77/3.25 inference(backward_demodulation,[status(thm)],[f13040,f13037])).
% 19.77/3.25 fof(f13040,plain,(
% 19.77/3.25 v_x____=v_y____),
% 19.77/3.25 inference(trivial_equality_resolution,[status(thm)],[f13038])).
% 19.77/3.25 fof(f13041,plain,(
% 19.77/3.25 ~sK3_skl(hAPP(hAPP(c_Polynomial_OpCons(t_a),v_c____),v_cs____),t_a)=v_c____),
% 19.77/3.25 inference(forward_demodulation,[status(thm)],[f11249,f13039])).
% 19.77/3.25 fof(f13042,plain,(
% 19.77/3.25 ~v_c____=v_c____),
% 19.77/3.25 inference(forward_demodulation,[status(thm)],[f9494,f13041])).
% 19.77/3.25 fof(f13043,plain,(
% 19.77/3.25 $false),
% 19.77/3.25 inference(trivial_equality_resolution,[status(thm)],[f13042])).
% 19.77/3.25 % SZS output end CNFRefutation for theBenchmark.p
% 12.20/3.32 % Elapsed time: 2.833073 seconds
% 12.20/3.32 % CPU time: 20.765524 seconds
% 12.20/3.32 % Total memory used: 394.401 MB
% 12.20/3.32 % Net memory used: 387.248 MB
%------------------------------------------------------------------------------