%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW278+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 : n026.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:54 PM UTC 2026
% Result : Theorem 11.34s 2.08s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWW278+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.43 % Computer : n026.cluster.edu
% 0.17/0.43 % Model : x86_64 x86_64
% 0.17/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.43 % Memory : 8046.5625MB
% 0.17/0.43 % OS : Linux 6.8.0-71-generic
% 0.17/0.43 % CPULimit : 300
% 0.17/0.43 % WCLimit : 300
% 0.17/0.43 % DateTime : Mon Sep 21 09:48:23 UTC 2026
% 0.17/0.43 % CPUTime :
% 0.27/0.58 % Drodi V4.1.1
% 11.34/2.08 % Refutation found
% 11.34/2.08 % SZS status Theorem for theBenchmark: Theorem is valid
% 11.34/2.08 % SZS output start CNFRefutation for theBenchmark
% 11.34/2.08 fof(f3,axiom,(
% 11.34/2.08 hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_s____),v_x____) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
% 11.34/2.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.34/2.08 fof(f83,axiom,(
% 11.34/2.08 (! [V_a,T_a] :( class_Rings_Ocomm__semiring__1(T_a)=> hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(T_a),V_a),V_a)) ) )),
% 11.34/2.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.34/2.08 fof(f97,axiom,(
% 11.34/2.08 (! [V_a,T_a] :( class_Rings_Ocomm__semiring__1(T_a)=> ( hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(T_a),c_Groups_Ozero__class_Ozero(T_a)),V_a))=> V_a = c_Groups_Ozero__class_Ozero(T_a) ) ) )),
% 11.34/2.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.34/2.08 fof(f126,axiom,(
% 11.34/2.08 v_pa____ = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,v_a____),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Oone__class_Oone(tc_Complex_Ocomplex),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))),c_Polynomial_Oorder(tc_Complex_Ocomplex,v_a____,v_pa____))),v_s____) ),
% 11.34/2.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.34/2.08 fof(f301,axiom,(
% 11.34/2.08 (! [V_x,V_q,V_p,T_a] :( class_Rings_Ocomm__semiring__0(T_a)=> hAPP(c_Polynomial_Opoly(T_a,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(T_a)),V_p),V_q)),V_x) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),hAPP(c_Polynomial_Opoly(T_a,V_p),V_x)),hAPP(c_Polynomial_Opoly(T_a,V_q),V_x)) ) )),
% 11.34/2.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.34/2.08 fof(f358,axiom,(
% 11.34/2.08 (! [V_c,V_b,V_a,T_a] :( class_Rings_Ocomm__semiring__1(T_a)=> ( hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(T_a),hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_a),V_b)),V_c))=> hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(T_a),V_b),V_c)) ) ) )),
% 11.34/2.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.34/2.08 fof(f437,axiom,(
% 11.34/2.08 (! [V_x,V_p,V_a,T_a] :( class_Rings_Ocomm__semiring__0(T_a)=> hAPP(c_Polynomial_Opoly(T_a,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)) ) )),
% 11.34/2.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.34/2.08 fof(f1117,axiom,(
% 11.34/2.08 class_Rings_Ocomm__semiring__1(tc_Complex_Ocomplex) ),
% 11.34/2.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.34/2.08 fof(f1118,axiom,(
% 11.34/2.08 class_Rings_Ocomm__semiring__0(tc_Complex_Ocomplex) ),
% 11.34/2.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.34/2.08 fof(f1200,conjecture,(
% 11.34/2.08 hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_pa____),v_x____) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
% 11.34/2.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.34/2.08 fof(f1201,negated_conjecture,(
% 11.34/2.08 ~(hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_pa____),v_x____) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) )),
% 11.34/2.08 inference(negated_conjecture,[status(cth)],[f1200])).
% 11.34/2.08 fof(f1207,plain,(
% 11.34/2.08 hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_s____),v_x____)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)),
% 11.34/2.08 inference(cnf_transformation,[status(thm)],[f3])).
% 11.34/2.08 fof(f1455,plain,(
% 11.34/2.08 ![V_a,T_a]: (~class_Rings_Ocomm__semiring__1(T_a)|hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(T_a),V_a),V_a)))),
% 11.34/2.08 inference(pre_NNF_transformation,[status(thm)],[f83])).
% 11.34/2.08 fof(f1456,plain,(
% 11.34/2.08 ![T_a]: (~class_Rings_Ocomm__semiring__1(T_a)|(![V_a]: hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(T_a),V_a),V_a))))),
% 11.34/2.08 inference(miniscoping,[status(thm)],[f1455])).
% 11.34/2.08 fof(f1457,plain,(
% 11.34/2.08 ![X0,X1]: (~class_Rings_Ocomm__semiring__1(X0)|hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(X0),X1),X1)))),
% 11.34/2.08 inference(cnf_transformation,[status(thm)],[f1456])).
% 11.34/2.08 fof(f1490,plain,(
% 11.34/2.08 ![V_a,T_a]: (~class_Rings_Ocomm__semiring__1(T_a)|(~hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(T_a),c_Groups_Ozero__class_Ozero(T_a)),V_a))|V_a=c_Groups_Ozero__class_Ozero(T_a)))),
% 11.34/2.08 inference(pre_NNF_transformation,[status(thm)],[f97])).
% 11.34/2.08 fof(f1491,plain,(
% 11.34/2.08 ![T_a]: (~class_Rings_Ocomm__semiring__1(T_a)|(![V_a]: (~hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(T_a),c_Groups_Ozero__class_Ozero(T_a)),V_a))|V_a=c_Groups_Ozero__class_Ozero(T_a))))),
% 11.34/2.08 inference(miniscoping,[status(thm)],[f1490])).
% 11.34/2.08 fof(f1492,plain,(
% 11.34/2.08 ![X0,X1]: (~class_Rings_Ocomm__semiring__1(X0)|~hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(X0),c_Groups_Ozero__class_Ozero(X0)),X1))|X1=c_Groups_Ozero__class_Ozero(X0))),
% 11.34/2.08 inference(cnf_transformation,[status(thm)],[f1491])).
% 11.34/2.08 fof(f1579,plain,(
% 11.34/2.08 v_pa____=hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,v_a____),c_Polynomial_OpCons(tc_Complex_Ocomplex,c_Groups_Oone__class_Oone(tc_Complex_Ocomplex),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))),c_Polynomial_Oorder(tc_Complex_Ocomplex,v_a____,v_pa____))),v_s____)),
% 11.34/2.08 inference(cnf_transformation,[status(thm)],[f126])).
% 11.34/2.08 fof(f2179,plain,(
% 11.34/2.08 ![V_x,V_q,V_p,T_a]: (~class_Rings_Ocomm__semiring__0(T_a)|hAPP(c_Polynomial_Opoly(T_a,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(T_a)),V_p),V_q)),V_x)=hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),hAPP(c_Polynomial_Opoly(T_a,V_p),V_x)),hAPP(c_Polynomial_Opoly(T_a,V_q),V_x)))),
% 11.34/2.08 inference(pre_NNF_transformation,[status(thm)],[f301])).
% 11.34/2.08 fof(f2180,plain,(
% 11.34/2.08 ![T_a]: (~class_Rings_Ocomm__semiring__0(T_a)|(![V_x,V_q,V_p]: hAPP(c_Polynomial_Opoly(T_a,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(T_a)),V_p),V_q)),V_x)=hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),hAPP(c_Polynomial_Opoly(T_a,V_p),V_x)),hAPP(c_Polynomial_Opoly(T_a,V_q),V_x))))),
% 11.34/2.08 inference(miniscoping,[status(thm)],[f2179])).
% 11.34/2.08 fof(f2181,plain,(
% 11.34/2.08 ![X0,X1,X2,X3]: (~class_Rings_Ocomm__semiring__0(X0)|hAPP(c_Polynomial_Opoly(X0,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(X0)),X1),X2)),X3)=hAPP(hAPP(c_Groups_Otimes__class_Otimes(X0),hAPP(c_Polynomial_Opoly(X0,X1),X3)),hAPP(c_Polynomial_Opoly(X0,X2),X3)))),
% 11.34/2.08 inference(cnf_transformation,[status(thm)],[f2180])).
% 11.34/2.08 fof(f2339,plain,(
% 11.34/2.08 ![V_c,V_b,V_a,T_a]: (~class_Rings_Ocomm__semiring__1(T_a)|(~hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(T_a),hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_a),V_b)),V_c))|hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(T_a),V_b),V_c))))),
% 11.34/2.08 inference(pre_NNF_transformation,[status(thm)],[f358])).
% 11.34/2.08 fof(f2340,plain,(
% 11.34/2.08 ![T_a]: (~class_Rings_Ocomm__semiring__1(T_a)|(![V_c,V_b]: ((![V_a]: ~hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(T_a),hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_a),V_b)),V_c)))|hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(T_a),V_b),V_c)))))),
% 11.34/2.08 inference(miniscoping,[status(thm)],[f2339])).
% 11.34/2.08 fof(f2341,plain,(
% 11.34/2.08 ![X0,X1,X2,X3]: (~class_Rings_Ocomm__semiring__1(X0)|~hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(X0),hAPP(hAPP(c_Groups_Otimes__class_Otimes(X0),X1),X2)),X3))|hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(X0),X2),X3)))),
% 11.34/2.08 inference(cnf_transformation,[status(thm)],[f2340])).
% 11.34/2.08 fof(f2619,plain,(
% 11.34/2.08 ![V_x,V_p,V_a,T_a]: (~class_Rings_Ocomm__semiring__0(T_a)|hAPP(c_Polynomial_Opoly(T_a,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)))),
% 11.34/2.08 inference(pre_NNF_transformation,[status(thm)],[f437])).
% 11.34/2.08 fof(f2620,plain,(
% 11.34/2.08 ![T_a]: (~class_Rings_Ocomm__semiring__0(T_a)|(![V_x,V_p,V_a]: hAPP(c_Polynomial_Opoly(T_a,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))))),
% 11.34/2.08 inference(miniscoping,[status(thm)],[f2619])).
% 11.34/2.08 fof(f2621,plain,(
% 11.34/2.08 ![X0,X1,X2,X3]: (~class_Rings_Ocomm__semiring__0(X0)|hAPP(c_Polynomial_Opoly(X0,c_Polynomial_Osmult(X0,X1,X2)),X3)=hAPP(hAPP(c_Groups_Otimes__class_Otimes(X0),X1),hAPP(c_Polynomial_Opoly(X0,X2),X3)))),
% 11.34/2.08 inference(cnf_transformation,[status(thm)],[f2620])).
% 11.34/2.08 fof(f4504,plain,(
% 11.34/2.08 class_Rings_Ocomm__semiring__1(tc_Complex_Ocomplex)),
% 11.34/2.08 inference(cnf_transformation,[status(thm)],[f1117])).
% 11.34/2.08 fof(f4505,plain,(
% 11.34/2.08 class_Rings_Ocomm__semiring__0(tc_Complex_Ocomplex)),
% 11.34/2.08 inference(cnf_transformation,[status(thm)],[f1118])).
% 11.34/2.08 fof(f4644,plain,(
% 11.34/2.08 ~hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_pa____),v_x____)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)),
% 11.34/2.08 inference(cnf_transformation,[status(thm)],[f1201])).
% 11.34/2.08 fof(f4922,plain,(
% 11.34/2.08 ![X0,X1,X2]: (hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_Osmult(tc_Complex_Ocomplex,X0,X1)),X2)=hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),X0),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,X1),X2)))),
% 11.34/2.08 inference(resolution,[status(thm)],[f4505,f2621])).
% 11.34/2.08 fof(f4923,plain,(
% 11.34/2.08 ![X0,X1,X2]: (hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X0),X1)),X2)=hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,X0),X2)),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,X1),X2)))),
% 11.34/2.08 inference(resolution,[status(thm)],[f4505,f2181])).
% 11.34/2.08 fof(f4958,plain,(
% 11.34/2.08 ![X0,X1,X2,X3]: (~class_Rings_Ocomm__semiring__1(tc_Complex_Ocomplex)|~hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Complex_Ocomplex),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_Osmult(tc_Complex_Ocomplex,X0,X1)),X2)),X3))|hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Complex_Ocomplex),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,X1),X2)),X3)))),
% 11.34/2.08 inference(paramodulation,[status(thm)],[f4922,f2341])).
% 11.34/2.08 fof(f4979,definition,(
% 11.34/2.08 sQ23_spl <=> (class_Rings_Ocomm__semiring__1(tc_Complex_Ocomplex))),
% 11.34/2.08 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 11.34/2.08 fof(f4981,plain,(
% 11.34/2.08 ~class_Rings_Ocomm__semiring__1(tc_Complex_Ocomplex)|sQ23_spl),
% 11.34/2.08 inference(component_clause,[status(thm)],[f4979])).
% 11.34/2.08 fof(f4982,definition,(
% 11.34/2.08 ![X0,X1,X2,X3]: (sQ24_spl <=> (~hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Complex_Ocomplex),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_Osmult(tc_Complex_Ocomplex,X0,X1)),X2)),X3))|hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Complex_Ocomplex),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,X1),X2)),X3))))),
% 11.34/2.08 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 11.34/2.08 fof(f4983,plain,(
% 11.34/2.08 ![X0,X1,X2,X3]: (~hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Complex_Ocomplex),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_Osmult(tc_Complex_Ocomplex,X0,X1)),X2)),X3))|hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Complex_Ocomplex),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,X1),X2)),X3))|~sQ24_spl)),
% 11.34/2.08 inference(component_clause,[status(thm)],[f4982])).
% 11.34/2.08 fof(f4985,plain,(
% 11.34/2.08 ~sQ23_spl|sQ24_spl),
% 11.34/2.08 inference(split_clause,[status(thm)],[f4958,f4979,f4982])).
% 11.34/2.08 fof(f4990,plain,(
% 11.34/2.08 $false|sQ23_spl),
% 11.34/2.08 inference(forward_subsumption_resolution,[status(thm)],[f4981,f4504])).
% 11.34/2.08 fof(f4991,plain,(
% 11.34/2.08 sQ23_spl),
% 11.34/2.08 inference(contradiction_clause,[status(thm)],[f4990])).
% 11.34/2.08 fof(f4993,plain,(
% 11.34/2.08 ![X0,X1,X2]: (hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X0),X1)),X2)=hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_Osmult(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,X0),X2),X1)),X2))),
% 11.34/2.08 inference(forward_demodulation,[status(thm)],[f4922,f4923])).
% 11.34/2.08 fof(f5000,plain,(
% 11.34/2.08 ![X0,X1,X2,X3]: (~hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Complex_Ocomplex),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X0),X1)),X2)),X3))|hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Complex_Ocomplex),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,X1),X2)),X3))|~sQ24_spl)),
% 11.34/2.08 inference(paramodulation,[status(thm)],[f4993,f4983])).
% 11.34/2.08 fof(f5224,plain,(
% 11.34/2.08 ![X0]: (hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Complex_Ocomplex),X0),X0)))),
% 11.34/2.08 inference(resolution,[status(thm)],[f1457,f4504])).
% 11.34/2.08 fof(f7983,plain,(
% 11.34/2.08 ![X0,X1]: (~hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Complex_Ocomplex),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_pa____),X0)),X1))|hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Complex_Ocomplex),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_s____),X0)),X1))|~sQ24_spl)),
% 11.34/2.11 inference(paramodulation,[status(thm)],[f1579,f5000])).
% 11.34/2.11 fof(f8044,plain,(
% 11.34/2.11 ![X0]: (~hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Complex_Ocomplex),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_pa____),v_x____)),X0))|hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Complex_Ocomplex),c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)),X0))|~sQ24_spl)),
% 11.34/2.11 inference(paramodulation,[status(thm)],[f1207,f7983])).
% 11.34/2.11 fof(f8059,plain,(
% 11.34/2.11 hBOOL(hAPP(hAPP(c_Rings_Odvd__class_Odvd(tc_Complex_Ocomplex),c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_pa____),v_x____)))|~sQ24_spl),
% 11.34/2.11 inference(resolution,[status(thm)],[f8044,f5224])).
% 11.34/2.11 fof(f8161,plain,(
% 11.34/2.11 ~class_Rings_Ocomm__semiring__1(tc_Complex_Ocomplex)|hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_pa____),v_x____)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)|~sQ24_spl),
% 11.34/2.11 inference(resolution,[status(thm)],[f8059,f1492])).
% 11.34/2.11 fof(f8164,definition,(
% 11.34/2.11 sQ138_spl <=> (hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_pa____),v_x____)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex))),
% 11.34/2.11 introduced(definition,[new_symbols(definition,[sQ138_spl])],[split_symbol_definition])).
% 11.34/2.11 fof(f8165,plain,(
% 11.34/2.11 hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_pa____),v_x____)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)|~sQ138_spl),
% 11.34/2.11 inference(component_clause,[status(thm)],[f8164])).
% 11.34/2.11 fof(f8167,plain,(
% 11.34/2.11 ~sQ23_spl|sQ138_spl|~sQ24_spl),
% 11.34/2.11 inference(split_clause,[status(thm)],[f8161,f4979,f8164,f4982])).
% 11.34/2.11 fof(f8176,plain,(
% 11.34/2.11 $false|~sQ138_spl),
% 11.34/2.11 inference(forward_subsumption_resolution,[status(thm)],[f8165,f4644])).
% 11.34/2.11 fof(f8177,plain,(
% 11.34/2.11 ~sQ138_spl),
% 11.34/2.11 inference(contradiction_clause,[status(thm)],[f8176])).
% 11.34/2.11 fof(f8178,plain,(
% 11.34/2.11 $false),
% 11.34/2.11 inference(sat_refutation,[status(thm)],[f4985,f4991,f8167,f8177])).
% 11.34/2.11 % SZS output end CNFRefutation for theBenchmark.p
% 9.43/2.18 % Elapsed time: 1.726219 seconds
% 9.43/2.18 % CPU time: 12.255051 seconds
% 9.43/2.18 % Total memory used: 398.571 MB
% 9.43/2.18 % Net memory used: 394.191 MB
%------------------------------------------------------------------------------