%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW288+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 03:08:55 PM UTC 2026
% Result : Theorem 0.21s 0.51s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW288+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n009.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 09:45:58 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.21/0.47 % Drodi V4.1.1
% 0.21/0.51 % Refutation found
% 0.21/0.51 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.21/0.51 % SZS output start CNFRefutation for theBenchmark
% 0.21/0.51 fof(f5,axiom,(
% 0.21/0.51 (! [V_p,V_a,T_a] :( class_Rings_Oidom(T_a)=> ( ( V_a = c_Groups_Ozero__class_Ozero(T_a)=> c_Polynomial_Odegree(T_a,c_Polynomial_Osmult(T_a,V_a,V_p)) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat) )& ( V_a != c_Groups_Ozero__class_Ozero(T_a)=> c_Polynomial_Odegree(T_a,c_Polynomial_Osmult(T_a,V_a,V_p)) = c_Polynomial_Odegree(T_a,V_p) ) ) ) )),
% 0.21/0.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.21/0.51 fof(f7,axiom,(
% 0.21/0.51 (! [V_x] :( ( class_Int_Oring__char__0(t_a)& class_Rings_Oidom(t_a) )=> hAPP(c_Polynomial_Opoly(t_a,v_p),V_x) = hAPP(c_Polynomial_Opoly(t_a,v_p),c_Groups_Ozero__class_Ozero(t_a)) ) )),
% 0.21/0.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.21/0.51 fof(f9,axiom,(
% 0.21/0.51 c_HOL_Obool_Obool__size(c_fTrue) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat) ),
% 0.21/0.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.21/0.51 fof(f10,axiom,(
% 0.21/0.51 c_HOL_Obool_Obool__size(c_fFalse) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat) ),
% 0.21/0.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.21/0.51 fof(f14,axiom,(
% 0.21/0.51 ( ( class_Int_Oring__char__0(t_a)& class_Rings_Oidom(t_a) )=> v_p = c_Polynomial_OpCons(t_a,hAPP(c_Polynomial_Opoly(t_a,v_p),c_Groups_Ozero__class_Ozero(t_a)),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))) ) ),
% 0.21/0.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.21/0.51 fof(f25,axiom,(
% 0.21/0.51 (! [V_pa_2,V_a_2,T_b] :( class_Groups_Ozero(T_b)=> ( 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)) ) ) ) )),
% 0.21/0.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.21/0.51 fof(f27,axiom,(
% 0.21/0.51 (! [V_pa_2,V_a_2,T_b] :( class_Rings_Oidom(T_b)=> ( c_Polynomial_Osmult(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)) ) ) ) )),
% 0.21/0.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.21/0.51 fof(f32,axiom,(
% 0.21/0.51 (! [V_a,T_a] :( class_Groups_Ozero(T_a)=> c_Polynomial_Odegree(T_a,c_Polynomial_OpCons(T_a,V_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)))) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat) ) )),
% 0.21/0.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.21/0.51 fof(f1012,axiom,(
% 0.21/0.51 (! [T] :( class_Int_Oring__char__0(T)=> class_Groups_Ozero(T) ) )),
% 0.21/0.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.21/0.51 fof(f1216,conjecture,(
% 0.21/0.51 c_Polynomial_Odegree(t_a,v_p) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat) ),
% 0.21/0.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.21/0.51 fof(f1217,negated_conjecture,(
% 0.21/0.51 ~(c_Polynomial_Odegree(t_a,v_p) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat) )),
% 0.21/0.51 inference(negated_conjecture,[status(cth)],[f1216])).
% 0.21/0.51 fof(f1218,hypothesis,(
% 0.21/0.51 class_Int_Oring__char__0(t_a) ),
% 0.21/0.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.21/0.51 fof(f1219,hypothesis,(
% 0.21/0.51 class_Rings_Oidom(t_a) ),
% 0.21/0.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.21/0.51 fof(f1233,plain,(
% 0.21/0.51 ![V_p,V_a,T_a]: (~class_Rings_Oidom(T_a)|((~V_a=c_Groups_Ozero__class_Ozero(T_a)|c_Polynomial_Odegree(T_a,c_Polynomial_Osmult(T_a,V_a,V_p))=c_Groups_Ozero__class_Ozero(tc_Nat_Onat))&(V_a=c_Groups_Ozero__class_Ozero(T_a)|c_Polynomial_Odegree(T_a,c_Polynomial_Osmult(T_a,V_a,V_p))=c_Polynomial_Odegree(T_a,V_p))))),
% 0.21/0.51 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.21/0.51 fof(f1234,plain,(
% 0.21/0.51 ![T_a]: (~class_Rings_Oidom(T_a)|((![V_a]: (~V_a=c_Groups_Ozero__class_Ozero(T_a)|(![V_p]: c_Polynomial_Odegree(T_a,c_Polynomial_Osmult(T_a,V_a,V_p))=c_Groups_Ozero__class_Ozero(tc_Nat_Onat))))&(![V_a]: (V_a=c_Groups_Ozero__class_Ozero(T_a)|(![V_p]: c_Polynomial_Odegree(T_a,c_Polynomial_Osmult(T_a,V_a,V_p))=c_Polynomial_Odegree(T_a,V_p))))))),
% 0.21/0.51 inference(miniscoping,[status(thm)],[f1233])).
% 0.21/0.51 fof(f1235,plain,(
% 0.21/0.51 ![X0,X1,X2]: (~class_Rings_Oidom(X0)|~X1=c_Groups_Ozero__class_Ozero(X0)|c_Polynomial_Odegree(X0,c_Polynomial_Osmult(X0,X1,X2))=c_Groups_Ozero__class_Ozero(tc_Nat_Onat))),
% 0.21/0.51 inference(cnf_transformation,[status(thm)],[f1234])).
% 0.21/0.51 fof(f1239,plain,(
% 0.21/0.51 ![V_x]: ((~class_Int_Oring__char__0(t_a)|~class_Rings_Oidom(t_a))|hAPP(c_Polynomial_Opoly(t_a,v_p),V_x)=hAPP(c_Polynomial_Opoly(t_a,v_p),c_Groups_Ozero__class_Ozero(t_a)))),
% 0.21/0.51 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 0.21/0.51 fof(f1240,plain,(
% 0.21/0.51 (~class_Int_Oring__char__0(t_a)|~class_Rings_Oidom(t_a))|(![V_x]: hAPP(c_Polynomial_Opoly(t_a,v_p),V_x)=hAPP(c_Polynomial_Opoly(t_a,v_p),c_Groups_Ozero__class_Ozero(t_a)))),
% 0.21/0.51 inference(miniscoping,[status(thm)],[f1239])).
% 0.21/0.51 fof(f1241,plain,(
% 0.21/0.51 ![X0]: (~class_Int_Oring__char__0(t_a)|~class_Rings_Oidom(t_a)|hAPP(c_Polynomial_Opoly(t_a,v_p),X0)=hAPP(c_Polynomial_Opoly(t_a,v_p),c_Groups_Ozero__class_Ozero(t_a)))),
% 0.21/0.51 inference(cnf_transformation,[status(thm)],[f1240])).
% 0.21/0.51 fof(f1245,plain,(
% 0.21/0.51 c_HOL_Obool_Obool__size(c_fTrue)=c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
% 0.21/0.51 inference(cnf_transformation,[status(thm)],[f9])).
% 0.21/0.51 fof(f1246,plain,(
% 0.21/0.51 c_HOL_Obool_Obool__size(c_fFalse)=c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
% 0.21/0.51 inference(cnf_transformation,[status(thm)],[f10])).
% 0.21/0.51 fof(f1251,plain,(
% 0.21/0.51 (~class_Int_Oring__char__0(t_a)|~class_Rings_Oidom(t_a))|v_p=c_Polynomial_OpCons(t_a,hAPP(c_Polynomial_Opoly(t_a,v_p),c_Groups_Ozero__class_Ozero(t_a)),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))),
% 0.21/0.51 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 0.21/0.51 fof(f1252,plain,(
% 0.21/0.51 ~class_Int_Oring__char__0(t_a)|~class_Rings_Oidom(t_a)|v_p=c_Polynomial_OpCons(t_a,hAPP(c_Polynomial_Opoly(t_a,v_p),c_Groups_Ozero__class_Ozero(t_a)),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))),
% 0.21/0.51 inference(cnf_transformation,[status(thm)],[f1251])).
% 0.21/0.51 fof(f1294,plain,(
% 0.21/0.51 ![V_pa_2,V_a_2,T_b]: (~class_Groups_Ozero(T_b)|(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)))))),
% 0.21/0.51 inference(pre_NNF_transformation,[status(thm)],[f25])).
% 0.21/0.51 fof(f1295,plain,(
% 0.21/0.51 ![V_pa_2,V_a_2,T_b]: (~class_Groups_Ozero(T_b)|((~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))))&(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))))))),
% 0.21/0.51 inference(NNF_transformation,[status(thm)],[f1294])).
% 0.21/0.51 fof(f1296,plain,(
% 0.21/0.51 ![T_b]: (~class_Groups_Ozero(T_b)|((![V_pa_2,V_a_2]: (~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]: (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)))))))),
% 0.21/0.51 inference(miniscoping,[status(thm)],[f1295])).
% 0.21/0.51 fof(f1299,plain,(
% 0.21/0.51 ![X0,X1,X2]: (~class_Groups_Ozero(X0)|c_Polynomial_OpCons(X0,X1,X2)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X0))|~X1=c_Groups_Ozero__class_Ozero(X0)|~X2=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)))),
% 0.21/0.51 inference(cnf_transformation,[status(thm)],[f1296])).
% 0.21/0.51 fof(f1302,plain,(
% 0.21/0.51 ![V_pa_2,V_a_2,T_b]: (~class_Rings_Oidom(T_b)|(c_Polynomial_Osmult(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)))))),
% 0.21/0.51 inference(pre_NNF_transformation,[status(thm)],[f27])).
% 0.21/0.51 fof(f1303,plain,(
% 0.21/0.51 ![V_pa_2,V_a_2,T_b]: (~class_Rings_Oidom(T_b)|((~c_Polynomial_Osmult(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))))&(c_Polynomial_Osmult(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))))))),
% 0.21/0.51 inference(NNF_transformation,[status(thm)],[f1302])).
% 0.21/0.51 fof(f1304,plain,(
% 0.21/0.51 ![T_b]: (~class_Rings_Oidom(T_b)|((![V_pa_2,V_a_2]: (~c_Polynomial_Osmult(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]: (c_Polynomial_Osmult(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)))))))),
% 0.21/0.51 inference(miniscoping,[status(thm)],[f1303])).
% 0.21/0.51 fof(f1306,plain,(
% 0.21/0.51 ![X0,X1,X2]: (~class_Rings_Oidom(X0)|c_Polynomial_Osmult(X0,X1,X2)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X0))|~X1=c_Groups_Ozero__class_Ozero(X0))),
% 0.21/0.51 inference(cnf_transformation,[status(thm)],[f1304])).
% 0.21/0.51 fof(f1322,plain,(
% 0.21/0.51 ![V_a,T_a]: (~class_Groups_Ozero(T_a)|c_Polynomial_Odegree(T_a,c_Polynomial_OpCons(T_a,V_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))))=c_Groups_Ozero__class_Ozero(tc_Nat_Onat))),
% 0.21/0.51 inference(pre_NNF_transformation,[status(thm)],[f32])).
% 0.21/0.51 fof(f1323,plain,(
% 0.21/0.51 ![T_a]: (~class_Groups_Ozero(T_a)|(![V_a]: c_Polynomial_Odegree(T_a,c_Polynomial_OpCons(T_a,V_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))))=c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))),
% 0.21/0.51 inference(miniscoping,[status(thm)],[f1322])).
% 0.21/0.51 fof(f1324,plain,(
% 0.21/0.51 ![X0,X1]: (~class_Groups_Ozero(X0)|c_Polynomial_Odegree(X0,c_Polynomial_OpCons(X0,X1,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X0))))=c_Groups_Ozero__class_Ozero(tc_Nat_Onat))),
% 0.21/0.51 inference(cnf_transformation,[status(thm)],[f1323])).
% 0.21/0.51 fof(f4522,plain,(
% 0.21/0.51 ![T]: (~class_Int_Oring__char__0(T)|class_Groups_Ozero(T))),
% 0.21/0.51 inference(pre_NNF_transformation,[status(thm)],[f1012])).
% 0.21/0.51 fof(f4523,plain,(
% 0.21/0.51 ![X0]: (~class_Int_Oring__char__0(X0)|class_Groups_Ozero(X0))),
% 0.21/0.51 inference(cnf_transformation,[status(thm)],[f4522])).
% 0.21/0.51 fof(f4831,plain,(
% 0.21/0.51 ~c_Polynomial_Odegree(t_a,v_p)=c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
% 0.21/0.51 inference(cnf_transformation,[status(thm)],[f1217])).
% 0.21/0.51 fof(f4832,plain,(
% 0.21/0.51 class_Int_Oring__char__0(t_a)),
% 0.21/0.51 inference(cnf_transformation,[status(thm)],[f1218])).
% 0.21/0.51 fof(f4833,plain,(
% 0.21/0.51 class_Rings_Oidom(t_a)),
% 0.21/0.51 inference(cnf_transformation,[status(thm)],[f1219])).
% 0.21/0.51 fof(f4888,definition,(
% 0.21/0.51 sQ0_spl <=> (class_Int_Oring__char__0(t_a))),
% 0.21/0.51 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.21/0.51 fof(f4890,plain,(
% 0.21/0.51 ~class_Int_Oring__char__0(t_a)|sQ0_spl),
% 0.21/0.51 inference(component_clause,[status(thm)],[f4888])).
% 0.21/0.51 fof(f4891,definition,(
% 0.21/0.51 sQ1_spl <=> (class_Rings_Oidom(t_a))),
% 0.21/0.51 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.21/0.51 fof(f4893,plain,(
% 0.21/0.51 ~class_Rings_Oidom(t_a)|sQ1_spl),
% 0.21/0.51 inference(component_clause,[status(thm)],[f4891])).
% 0.21/0.51 fof(f4902,definition,(
% 0.21/0.51 ![X0]: (sQ4_spl <=> (hAPP(c_Polynomial_Opoly(t_a,v_p),X0)=hAPP(c_Polynomial_Opoly(t_a,v_p),c_Groups_Ozero__class_Ozero(t_a))))),
% 0.21/0.51 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.21/0.51 fof(f4903,plain,(
% 0.21/0.51 ![X0]: (hAPP(c_Polynomial_Opoly(t_a,v_p),X0)=hAPP(c_Polynomial_Opoly(t_a,v_p),c_Groups_Ozero__class_Ozero(t_a))|~sQ4_spl)),
% 0.21/0.51 inference(component_clause,[status(thm)],[f4902])).
% 0.21/0.51 fof(f4905,plain,(
% 0.21/0.51 ~sQ0_spl|~sQ1_spl|sQ4_spl),
% 0.21/0.51 inference(split_clause,[status(thm)],[f1241,f4888,f4891,f4902])).
% 0.21/0.51 fof(f4910,definition,(
% 0.21/0.51 sQ6_spl <=> (v_p=c_Polynomial_OpCons(t_a,hAPP(c_Polynomial_Opoly(t_a,v_p),c_Groups_Ozero__class_Ozero(t_a)),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))))),
% 0.21/0.51 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.21/0.51 fof(f4911,plain,(
% 0.21/0.51 v_p=c_Polynomial_OpCons(t_a,hAPP(c_Polynomial_Opoly(t_a,v_p),c_Groups_Ozero__class_Ozero(t_a)),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))|~sQ6_spl),
% 0.21/0.51 inference(component_clause,[status(thm)],[f4910])).
% 0.21/0.51 fof(f4913,plain,(
% 0.21/0.51 ~sQ0_spl|~sQ1_spl|sQ6_spl),
% 0.21/0.51 inference(split_clause,[status(thm)],[f1252,f4888,f4891,f4910])).
% 0.21/0.51 fof(f4914,plain,(
% 0.21/0.51 ![X0,X1]: (~class_Rings_Oidom(X0)|c_Polynomial_Odegree(X0,c_Polynomial_Osmult(X0,c_Groups_Ozero__class_Ozero(X0),X1))=c_Groups_Ozero__class_Ozero(tc_Nat_Onat))),
% 0.21/0.51 inference(destructive_equality_resolution,[status(thm)],[f1235])).
% 0.21/0.51 fof(f4916,plain,(
% 0.21/0.51 ![X0]: (~class_Groups_Ozero(X0)|c_Polynomial_OpCons(X0,c_Groups_Ozero__class_Ozero(X0),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)))=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)))),
% 0.21/0.51 inference(destructive_equality_resolution,[status(thm)],[f1299])).
% 0.21/0.51 fof(f4917,plain,(
% 0.21/0.51 ![X0,X1]: (~class_Rings_Oidom(X0)|c_Polynomial_Osmult(X0,c_Groups_Ozero__class_Ozero(X0),X1)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)))),
% 0.21/0.51 inference(destructive_equality_resolution,[status(thm)],[f1306])).
% 0.21/0.51 fof(f5079,plain,(
% 0.21/0.51 ![X0]: (c_Polynomial_Odegree(t_a,c_Polynomial_Osmult(t_a,c_Groups_Ozero__class_Ozero(t_a),X0))=c_Groups_Ozero__class_Ozero(tc_Nat_Onat))),
% 0.21/0.51 inference(resolution,[status(thm)],[f4914,f4833])).
% 0.21/0.51 fof(f5082,plain,(
% 0.21/0.51 ~c_Polynomial_Odegree(t_a,v_p)=c_HOL_Obool_Obool__size(c_fTrue)),
% 0.21/0.51 inference(backward_demodulation,[status(thm)],[f1245,f4831])).
% 0.21/0.51 fof(f5083,plain,(
% 0.21/0.51 ![X0]: (c_Polynomial_Odegree(t_a,c_Polynomial_Osmult(t_a,c_Groups_Ozero__class_Ozero(t_a),X0))=c_HOL_Obool_Obool__size(c_fTrue))),
% 0.21/0.51 inference(forward_demodulation,[status(thm)],[f1245,f5079])).
% 0.21/0.51 fof(f5132,plain,(
% 0.21/0.51 $false|sQ1_spl),
% 0.21/0.51 inference(forward_subsumption_resolution,[status(thm)],[f4893,f4833])).
% 0.21/0.51 fof(f5133,plain,(
% 0.21/0.51 sQ1_spl),
% 0.21/0.51 inference(contradiction_clause,[status(thm)],[f5132])).
% 0.21/0.51 fof(f5134,plain,(
% 0.21/0.51 $false|sQ0_spl),
% 0.21/0.51 inference(forward_subsumption_resolution,[status(thm)],[f4890,f4832])).
% 0.21/0.51 fof(f5135,plain,(
% 0.21/0.51 sQ0_spl),
% 0.21/0.51 inference(contradiction_clause,[status(thm)],[f5134])).
% 0.21/0.51 fof(f5139,plain,(
% 0.21/0.51 ![X0,X1]: (hAPP(c_Polynomial_Opoly(t_a,v_p),X0)=hAPP(c_Polynomial_Opoly(t_a,v_p),X1)|~sQ4_spl)),
% 0.21/0.51 inference(paramodulation,[status(thm)],[f4903,f4903])).
% 0.21/0.51 fof(f5152,plain,(
% 0.21/0.51 ![X0]: (v_p=c_Polynomial_OpCons(t_a,hAPP(c_Polynomial_Opoly(t_a,v_p),X0),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))|~sQ6_spl|~sQ4_spl)),
% 0.21/0.52 inference(paramodulation,[status(thm)],[f5139,f4911])).
% 0.21/0.52 fof(f5161,definition,(
% 0.21/0.52 sQ12_spl <=> (class_Groups_Ozero(t_a))),
% 0.21/0.52 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.21/0.52 fof(f5162,plain,(
% 0.21/0.52 class_Groups_Ozero(t_a)|~sQ12_spl),
% 0.21/0.52 inference(component_clause,[status(thm)],[f5161])).
% 0.21/0.52 fof(f5163,plain,(
% 0.21/0.52 ~class_Groups_Ozero(t_a)|sQ12_spl),
% 0.21/0.52 inference(component_clause,[status(thm)],[f5161])).
% 0.21/0.52 fof(f5248,plain,(
% 0.21/0.52 ![X0]: (c_Polynomial_Osmult(t_a,c_Groups_Ozero__class_Ozero(t_a),X0)=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))),
% 0.21/0.52 inference(resolution,[status(thm)],[f4917,f4833])).
% 0.21/0.52 fof(f5254,plain,(
% 0.21/0.52 c_Polynomial_Odegree(t_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))=c_HOL_Obool_Obool__size(c_fTrue)),
% 0.21/0.52 inference(backward_demodulation,[status(thm)],[f5248,f5083])).
% 0.21/0.52 fof(f5329,plain,(
% 0.21/0.52 ![X0,X1]: (~class_Groups_Ozero(X0)|c_Polynomial_Odegree(X0,c_Polynomial_OpCons(X0,X1,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X0))))=c_HOL_Obool_Obool__size(c_fFalse))),
% 0.21/0.52 inference(forward_demodulation,[status(thm)],[f1246,f1324])).
% 0.21/0.52 fof(f5334,plain,(
% 0.21/0.52 class_Groups_Ozero(t_a)),
% 0.21/0.52 inference(resolution,[status(thm)],[f4523,f4832])).
% 0.21/0.52 fof(f5336,plain,(
% 0.21/0.52 $false|sQ12_spl),
% 0.21/0.52 inference(forward_subsumption_resolution,[status(thm)],[f5334,f5163])).
% 0.21/0.52 fof(f5337,plain,(
% 0.21/0.52 sQ12_spl),
% 0.21/0.52 inference(contradiction_clause,[status(thm)],[f5336])).
% 0.21/0.52 fof(f5338,plain,(
% 0.21/0.52 ![X0]: (c_Polynomial_Odegree(t_a,c_Polynomial_OpCons(t_a,X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))))=c_HOL_Obool_Obool__size(c_fFalse)|~sQ12_spl)),
% 0.21/0.52 inference(resolution,[status(thm)],[f5162,f5329])).
% 0.21/0.52 fof(f5340,plain,(
% 0.21/0.52 c_Polynomial_OpCons(t_a,c_Groups_Ozero__class_Ozero(t_a),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))|~sQ12_spl),
% 0.21/0.52 inference(resolution,[status(thm)],[f5162,f4916])).
% 0.21/0.52 fof(f5345,definition,(
% 0.21/0.52 sQ30_spl <=> (v_p=v_p)),
% 0.21/0.52 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.21/0.52 fof(f5347,plain,(
% 0.21/0.52 ~v_p=v_p|sQ30_spl),
% 0.21/0.52 inference(component_clause,[status(thm)],[f5345])).
% 0.21/0.52 fof(f5374,plain,(
% 0.21/0.52 $false|sQ30_spl),
% 0.21/0.52 inference(trivial_equality_resolution,[status(thm)],[f5347])).
% 0.21/0.52 fof(f5375,plain,(
% 0.21/0.52 sQ30_spl),
% 0.21/0.52 inference(contradiction_clause,[status(thm)],[f5374])).
% 0.21/0.52 fof(f5376,plain,(
% 0.21/0.52 c_Polynomial_Odegree(t_a,v_p)=c_HOL_Obool_Obool__size(c_fFalse)|~sQ12_spl|~sQ6_spl|~sQ4_spl),
% 0.21/0.52 inference(paramodulation,[status(thm)],[f5152,f5338])).
% 0.21/0.52 fof(f5377,plain,(
% 0.21/0.52 ~c_HOL_Obool_Obool__size(c_fFalse)=c_HOL_Obool_Obool__size(c_fTrue)|~sQ12_spl|~sQ6_spl|~sQ4_spl),
% 0.21/0.52 inference(backward_demodulation,[status(thm)],[f5376,f5082])).
% 0.21/0.52 fof(f5380,plain,(
% 0.21/0.52 c_Polynomial_Odegree(t_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))=c_HOL_Obool_Obool__size(c_fFalse)|~sQ12_spl),
% 0.21/0.52 inference(paramodulation,[status(thm)],[f5340,f5338])).
% 0.21/0.52 fof(f5407,plain,(
% 0.21/0.52 c_HOL_Obool_Obool__size(c_fFalse)=c_HOL_Obool_Obool__size(c_fTrue)|~sQ12_spl),
% 0.21/0.52 inference(backward_demodulation,[status(thm)],[f5380,f5254])).
% 0.21/0.52 fof(f5408,plain,(
% 0.21/0.52 $false|~sQ6_spl|~sQ4_spl|~sQ12_spl),
% 0.21/0.52 inference(forward_subsumption_resolution,[status(thm)],[f5407,f5377])).
% 0.21/0.52 fof(f5409,plain,(
% 0.21/0.52 ~sQ6_spl|~sQ4_spl|~sQ12_spl),
% 0.21/0.52 inference(contradiction_clause,[status(thm)],[f5408])).
% 0.21/0.52 fof(f5410,plain,(
% 0.21/0.52 $false),
% 0.21/0.52 inference(sat_refutation,[status(thm)],[f4905,f4913,f5133,f5135,f5337,f5375,f5409])).
% 0.21/0.52 % SZS output end CNFRefutation for theBenchmark.p
% 0.21/0.56 % Elapsed time: 0.187682 seconds
% 0.21/0.56 % CPU time: 0.476037 seconds
% 0.21/0.56 % Total memory used: 155.188 MB
% 0.21/0.56 % Net memory used: 154.072 MB
%------------------------------------------------------------------------------