%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : ALG431-1 : TPTP v9.3.1. Released v4.1.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 11:50:10 AM UTC 2026
% Result : Unsatisfiable 31.21s 4.64s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : ALG431-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.07 % 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 13:23:06 UTC 2026
% 0.17/0.44 % CPUTime :
% 0.27/0.57 % Drodi V4.1.1
% 31.21/4.64 % Refutation found
% 31.21/4.64 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 31.21/4.64 % SZS output start CNFRefutation for theBenchmark
% 31.21/4.64 fof(f149,axiom,(
% 31.21/4.64 (![T_a,V_a,V_b,V_n]: (( ~ class_Ring__and__Field_Ocomm__semiring__0(T_a)| c_Polynomial_Osmult(V_a,c_Polynomial_Omonom(V_b,V_n,T_a),T_a) = c_Polynomial_Omonom(c_HOL_Otimes__class_Otimes(V_a,V_b,T_a),V_n,T_a) ) ))),
% 31.21/4.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 31.21/4.64 fof(f432,axiom,(
% 31.21/4.64 (![T_a,V_p,V_c]: (( ~ class_Ring__and__Field_Ocomm__semiring__0(T_a)| c_HOL_Oplus__class_Oplus(V_p,c_Polynomial_Osmult(V_c,c_Polynomial_Osynthetic__div(V_p,V_c,T_a),T_a),tc_Polynomial_Opoly(T_a)) = c_Polynomial_OpCons(c_Polynomial_Opoly(V_p,V_c,T_a),c_Polynomial_Osynthetic__div(V_p,V_c,T_a),T_a) ) ))),
% 31.21/4.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 31.21/4.64 fof(f453,axiom,(
% 31.21/4.64 ( ~ class_Ring__and__Field_Oidom(t_a)| ~ class_Int_Oring__char__0(t_a)| c_Polynomial_Odegree(v_p,t_a) = c_HOL_Ozero__class_Ozero(tc_nat) ) ),
% 31.21/4.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 31.21/4.64 fof(f464,axiom,(
% 31.21/4.64 (![T_a,V_a]: (( ~ class_Ring__and__Field_Oring__no__zero__divisors(T_a)| c_HOL_Otimes__class_Otimes(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) = c_HOL_Ozero__class_Ozero(T_a) ) ))),
% 31.21/4.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 31.21/4.64 fof(f504,axiom,(
% 31.21/4.64 (![T_a,V_p,V_c]: (( ~ class_Ring__and__Field_Ocomm__semiring__0(T_a)| c_Polynomial_Odegree(V_p,T_a) != c_HOL_Ozero__class_Ozero(tc_nat)| c_Polynomial_Osynthetic__div(V_p,V_c,T_a) = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)) ) ))),
% 31.21/4.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 31.21/4.64 fof(f613,axiom,(
% 31.21/4.64 (![T_a,V_a]: (( ~ class_OrderedGroup_Omonoid__add(T_a)| c_HOL_Oplus__class_Oplus(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) = V_a ) ))),
% 31.21/4.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 31.21/4.64 fof(f672,axiom,(
% 31.21/4.64 (![T_a,V_n]: (( ~ class_HOL_Ozero(T_a)| c_Polynomial_Omonom(c_HOL_Ozero__class_Ozero(T_a),V_n,T_a) = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)) ) ))),
% 31.21/4.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 31.21/4.64 fof(f686,negated_conjecture,(
% 31.21/4.64 class_Int_Oring__char__0(t_a) ),
% 31.21/4.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 31.21/4.64 fof(f687,negated_conjecture,(
% 31.21/4.64 class_Ring__and__Field_Oidom(t_a) ),
% 31.21/4.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 31.21/4.64 fof(f688,negated_conjecture,(
% 31.21/4.64 ~ v_thesis____ ),
% 31.21/4.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 31.21/4.64 fof(f689,negated_conjecture,(
% 31.21/4.64 (![V_x]: (( v_p != c_Polynomial_OpCons(V_x,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)),t_a)| v_thesis____ ) ))),
% 31.21/4.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 31.21/4.64 fof(f690,axiom,(
% 31.21/4.64 (![T]: (( ~ class_Ring__and__Field_Oidom(T)| class_Ring__and__Field_Oring__no__zero__divisors(T) ) ))),
% 31.21/4.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 31.21/4.64 fof(f695,axiom,(
% 31.21/4.64 (![T]: (( ~ class_Ring__and__Field_Oidom(T)| class_Ring__and__Field_Ocomm__semiring__0(T) ) ))),
% 31.21/4.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 31.21/4.64 fof(f708,axiom,(
% 31.21/4.64 (![T]: (( ~ class_Ring__and__Field_Oidom(T)| class_OrderedGroup_Omonoid__add(T) ) ))),
% 31.21/4.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 31.21/4.64 fof(f726,axiom,(
% 31.21/4.64 (![T]: (( ~ class_Int_Oring__char__0(T)| class_HOL_Ozero(T) ) ))),
% 31.21/4.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 31.21/4.64 fof(f853,axiom,(
% 31.21/4.64 (![T_1]: (( class_Ring__and__Field_Oidom(tc_Polynomial_Opoly(T_1))| ~ class_Ring__and__Field_Oidom(T_1) ) ))),
% 31.21/4.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 31.21/4.64 fof(f1127,plain,(
% 31.21/4.64 ![T_a]: (~class_Ring__and__Field_Ocomm__semiring__0(T_a)|(![V_a,V_b,V_n]: c_Polynomial_Osmult(V_a,c_Polynomial_Omonom(V_b,V_n,T_a),T_a)=c_Polynomial_Omonom(c_HOL_Otimes__class_Otimes(V_a,V_b,T_a),V_n,T_a)))),
% 31.21/4.64 inference(miniscoping,[status(thm)],[f149])).
% 31.21/4.64 fof(f1128,plain,(
% 31.21/4.64 ![X0,X1,X2,X3]: (~class_Ring__and__Field_Ocomm__semiring__0(X0)|c_Polynomial_Osmult(X1,c_Polynomial_Omonom(X2,X3,X0),X0)=c_Polynomial_Omonom(c_HOL_Otimes__class_Otimes(X1,X2,X0),X3,X0))),
% 31.21/4.64 inference(cnf_transformation,[status(thm)],[f1127])).
% 31.21/4.64 fof(f1626,plain,(
% 31.21/4.64 ![T_a]: (~class_Ring__and__Field_Ocomm__semiring__0(T_a)|(![V_p,V_c]: c_HOL_Oplus__class_Oplus(V_p,c_Polynomial_Osmult(V_c,c_Polynomial_Osynthetic__div(V_p,V_c,T_a),T_a),tc_Polynomial_Opoly(T_a))=c_Polynomial_OpCons(c_Polynomial_Opoly(V_p,V_c,T_a),c_Polynomial_Osynthetic__div(V_p,V_c,T_a),T_a)))),
% 31.21/4.64 inference(miniscoping,[status(thm)],[f432])).
% 31.21/4.64 fof(f1627,plain,(
% 31.21/4.64 ![X0,X1,X2]: (~class_Ring__and__Field_Ocomm__semiring__0(X0)|c_HOL_Oplus__class_Oplus(X1,c_Polynomial_Osmult(X2,c_Polynomial_Osynthetic__div(X1,X2,X0),X0),tc_Polynomial_Opoly(X0))=c_Polynomial_OpCons(c_Polynomial_Opoly(X1,X2,X0),c_Polynomial_Osynthetic__div(X1,X2,X0),X0))),
% 31.21/4.64 inference(cnf_transformation,[status(thm)],[f1626])).
% 31.21/4.64 fof(f1659,plain,(
% 31.21/4.64 ~class_Ring__and__Field_Oidom(t_a)|~class_Int_Oring__char__0(t_a)|c_Polynomial_Odegree(v_p,t_a)=c_HOL_Ozero__class_Ozero(tc_nat)),
% 31.21/4.64 inference(cnf_transformation,[status(thm)],[f453])).
% 31.21/4.64 fof(f1673,plain,(
% 31.21/4.64 ![T_a]: (~class_Ring__and__Field_Oring__no__zero__divisors(T_a)|(![V_a]: c_HOL_Otimes__class_Otimes(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a)=c_HOL_Ozero__class_Ozero(T_a)))),
% 31.21/4.64 inference(miniscoping,[status(thm)],[f464])).
% 31.21/4.64 fof(f1674,plain,(
% 31.21/4.64 ![X0,X1]: (~class_Ring__and__Field_Oring__no__zero__divisors(X0)|c_HOL_Otimes__class_Otimes(X1,c_HOL_Ozero__class_Ozero(X0),X0)=c_HOL_Ozero__class_Ozero(X0))),
% 31.21/4.64 inference(cnf_transformation,[status(thm)],[f1673])).
% 31.21/4.64 fof(f1742,plain,(
% 31.21/4.64 ![T_a,V_p]: ((~class_Ring__and__Field_Ocomm__semiring__0(T_a)|~c_Polynomial_Odegree(V_p,T_a)=c_HOL_Ozero__class_Ozero(tc_nat))|(![V_c]: c_Polynomial_Osynthetic__div(V_p,V_c,T_a)=c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))))),
% 31.21/4.64 inference(miniscoping,[status(thm)],[f504])).
% 31.21/4.64 fof(f1743,plain,(
% 31.21/4.64 ![X0,X1,X2]: (~class_Ring__and__Field_Ocomm__semiring__0(X0)|~c_Polynomial_Odegree(X1,X0)=c_HOL_Ozero__class_Ozero(tc_nat)|c_Polynomial_Osynthetic__div(X1,X2,X0)=c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)))),
% 31.21/4.64 inference(cnf_transformation,[status(thm)],[f1742])).
% 31.21/4.64 fof(f1917,plain,(
% 31.21/4.64 ![T_a]: (~class_OrderedGroup_Omonoid__add(T_a)|(![V_a]: c_HOL_Oplus__class_Oplus(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a)=V_a))),
% 31.21/4.64 inference(miniscoping,[status(thm)],[f613])).
% 31.21/4.64 fof(f1918,plain,(
% 31.21/4.64 ![X0,X1]: (~class_OrderedGroup_Omonoid__add(X0)|c_HOL_Oplus__class_Oplus(X1,c_HOL_Ozero__class_Ozero(X0),X0)=X1)),
% 31.21/4.64 inference(cnf_transformation,[status(thm)],[f1917])).
% 31.21/4.64 fof(f2025,plain,(
% 31.21/4.64 ![T_a]: (~class_HOL_Ozero(T_a)|(![V_n]: c_Polynomial_Omonom(c_HOL_Ozero__class_Ozero(T_a),V_n,T_a)=c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))))),
% 31.21/4.64 inference(miniscoping,[status(thm)],[f672])).
% 31.21/4.64 fof(f2026,plain,(
% 31.21/4.64 ![X0,X1]: (~class_HOL_Ozero(X0)|c_Polynomial_Omonom(c_HOL_Ozero__class_Ozero(X0),X1,X0)=c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)))),
% 31.21/4.64 inference(cnf_transformation,[status(thm)],[f2025])).
% 31.21/4.64 fof(f2051,plain,(
% 31.21/4.64 class_Int_Oring__char__0(t_a)),
% 31.21/4.64 inference(cnf_transformation,[status(thm)],[f686])).
% 31.21/4.64 fof(f2052,plain,(
% 31.21/4.64 class_Ring__and__Field_Oidom(t_a)),
% 31.21/4.64 inference(cnf_transformation,[status(thm)],[f687])).
% 31.21/4.64 fof(f2053,plain,(
% 31.21/4.64 ~v_thesis____),
% 31.21/4.64 inference(cnf_transformation,[status(thm)],[f688])).
% 31.21/4.64 fof(f2054,plain,(
% 31.21/4.64 (![V_x]: ~v_p=c_Polynomial_OpCons(V_x,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)),t_a))|v_thesis____),
% 31.21/4.64 inference(miniscoping,[status(thm)],[f689])).
% 31.21/4.64 fof(f2055,plain,(
% 31.21/4.64 ![X0]: (~v_p=c_Polynomial_OpCons(X0,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)),t_a)|v_thesis____)),
% 31.21/4.64 inference(cnf_transformation,[status(thm)],[f2054])).
% 31.21/4.64 fof(f2056,plain,(
% 31.21/4.64 ![X0]: (~class_Ring__and__Field_Oidom(X0)|class_Ring__and__Field_Oring__no__zero__divisors(X0))),
% 31.21/4.64 inference(cnf_transformation,[status(thm)],[f690])).
% 31.21/4.64 fof(f2061,plain,(
% 31.21/4.64 ![X0]: (~class_Ring__and__Field_Oidom(X0)|class_Ring__and__Field_Ocomm__semiring__0(X0))),
% 31.21/4.64 inference(cnf_transformation,[status(thm)],[f695])).
% 31.21/4.64 fof(f2074,plain,(
% 31.21/4.64 ![X0]: (~class_Ring__and__Field_Oidom(X0)|class_OrderedGroup_Omonoid__add(X0))),
% 31.21/4.64 inference(cnf_transformation,[status(thm)],[f708])).
% 31.21/4.64 fof(f2092,plain,(
% 31.21/4.64 ![X0]: (~class_Int_Oring__char__0(X0)|class_HOL_Ozero(X0))),
% 31.21/4.64 inference(cnf_transformation,[status(thm)],[f726])).
% 31.21/4.64 fof(f2219,plain,(
% 31.21/4.64 ![X0]: (class_Ring__and__Field_Oidom(tc_Polynomial_Opoly(X0))|~class_Ring__and__Field_Oidom(X0))),
% 31.21/4.64 inference(cnf_transformation,[status(thm)],[f853])).
% 31.21/4.64 fof(f2228,plain,(
% 31.21/4.64 ![X0]: (~v_p=c_Polynomial_OpCons(X0,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)),t_a))),
% 31.21/4.64 inference(forward_subsumption_resolution,[status(thm)],[f2055,f2053])).
% 31.21/4.64 fof(f2233,plain,(
% 31.21/4.64 class_HOL_Ozero(t_a)),
% 31.21/4.64 inference(resolution,[status(thm)],[f2092,f2051])).
% 31.21/4.64 fof(f2234,plain,(
% 31.21/4.64 class_Ring__and__Field_Oidom(tc_Polynomial_Opoly(t_a))),
% 31.21/4.64 inference(resolution,[status(thm)],[f2219,f2052])).
% 31.21/4.64 fof(f2269,plain,(
% 31.21/4.64 ~class_Int_Oring__char__0(t_a)|c_Polynomial_Odegree(v_p,t_a)=c_HOL_Ozero__class_Ozero(tc_nat)),
% 31.21/4.64 inference(forward_subsumption_resolution,[status(thm)],[f1659,f2052])).
% 31.21/4.64 fof(f2270,plain,(
% 31.21/4.64 c_Polynomial_Odegree(v_p,t_a)=c_HOL_Ozero__class_Ozero(tc_nat)),
% 31.21/4.64 inference(resolution,[status(thm)],[f2269,f2051])).
% 31.21/4.64 fof(f2698,plain,(
% 31.21/4.64 class_Ring__and__Field_Oring__no__zero__divisors(t_a)),
% 31.21/4.64 inference(resolution,[status(thm)],[f2056,f2052])).
% 31.21/4.64 fof(f2840,plain,(
% 31.21/4.64 class_Ring__and__Field_Ocomm__semiring__0(t_a)),
% 31.21/4.64 inference(resolution,[status(thm)],[f2061,f2052])).
% 31.21/4.64 fof(f3162,plain,(
% 31.21/4.64 class_OrderedGroup_Omonoid__add(tc_Polynomial_Opoly(t_a))),
% 31.21/4.64 inference(resolution,[status(thm)],[f2074,f2234])).
% 31.21/4.64 fof(f5542,plain,(
% 31.21/4.64 ![X0]: (c_HOL_Oplus__class_Oplus(X0,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)),tc_Polynomial_Opoly(t_a))=X0)),
% 31.21/4.64 inference(resolution,[status(thm)],[f1918,f3162])).
% 31.21/4.64 fof(f8559,plain,(
% 31.21/4.64 ![X0]: (c_HOL_Otimes__class_Otimes(X0,c_HOL_Ozero__class_Ozero(t_a),t_a)=c_HOL_Ozero__class_Ozero(t_a))),
% 31.21/4.64 inference(resolution,[status(thm)],[f1674,f2698])).
% 31.21/4.64 fof(f13950,plain,(
% 31.21/4.64 ![X0,X1,X2]: (c_Polynomial_Osmult(X0,c_Polynomial_Omonom(X1,X2,t_a),t_a)=c_Polynomial_Omonom(c_HOL_Otimes__class_Otimes(X0,X1,t_a),X2,t_a))),
% 31.21/4.64 inference(resolution,[status(thm)],[f1128,f2840])).
% 31.21/4.64 fof(f16007,plain,(
% 31.21/4.64 ![X0]: (c_Polynomial_Omonom(c_HOL_Ozero__class_Ozero(t_a),X0,t_a)=c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))),
% 31.21/4.64 inference(resolution,[status(thm)],[f2026,f2233])).
% 31.21/4.64 fof(f18249,plain,(
% 31.21/4.64 ![X0,X1]: (c_Polynomial_Osmult(X0,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)),t_a)=c_Polynomial_Omonom(c_HOL_Otimes__class_Otimes(X0,c_HOL_Ozero__class_Ozero(t_a),t_a),X1,t_a))),
% 31.21/4.64 inference(paramodulation,[status(thm)],[f16007,f13950])).
% 31.21/4.64 fof(f18257,plain,(
% 31.21/4.64 ![X0,X1]: (c_Polynomial_Osmult(X0,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)),t_a)=c_Polynomial_Omonom(c_HOL_Ozero__class_Ozero(t_a),X1,t_a))),
% 31.21/4.64 inference(forward_demodulation,[status(thm)],[f8559,f18249])).
% 31.21/4.64 fof(f18258,plain,(
% 31.21/4.64 ![X0]: (c_Polynomial_Osmult(X0,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)),t_a)=c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))),
% 31.21/4.64 inference(forward_demodulation,[status(thm)],[f16007,f18257])).
% 31.21/4.64 fof(f59807,plain,(
% 31.21/4.64 ![X0,X1]: (c_HOL_Oplus__class_Oplus(X0,c_Polynomial_Osmult(X1,c_Polynomial_Osynthetic__div(X0,X1,t_a),t_a),tc_Polynomial_Opoly(t_a))=c_Polynomial_OpCons(c_Polynomial_Opoly(X0,X1,t_a),c_Polynomial_Osynthetic__div(X0,X1,t_a),t_a))),
% 31.21/4.64 inference(resolution,[status(thm)],[f1627,f2840])).
% 31.21/4.64 fof(f69615,plain,(
% 31.21/4.64 ![X0,X1]: (~c_Polynomial_Odegree(X0,t_a)=c_HOL_Ozero__class_Ozero(tc_nat)|c_Polynomial_Osynthetic__div(X0,X1,t_a)=c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))),
% 31.21/4.64 inference(resolution,[status(thm)],[f1743,f2840])).
% 31.21/4.64 fof(f71474,plain,(
% 31.21/4.64 ![X0]: (c_Polynomial_Osynthetic__div(v_p,X0,t_a)=c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))),
% 31.21/4.64 inference(resolution,[status(thm)],[f69615,f2270])).
% 31.21/4.64 fof(f71493,plain,(
% 31.21/4.64 ![X0]: (c_HOL_Oplus__class_Oplus(v_p,c_Polynomial_Osmult(X0,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)),t_a),tc_Polynomial_Opoly(t_a))=c_Polynomial_OpCons(c_Polynomial_Opoly(v_p,X0,t_a),c_Polynomial_Osynthetic__div(v_p,X0,t_a),t_a))),
% 31.21/4.64 inference(paramodulation,[status(thm)],[f71474,f59807])).
% 31.21/4.64 fof(f71497,plain,(
% 31.21/4.64 ![X0]: (c_HOL_Oplus__class_Oplus(v_p,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)),tc_Polynomial_Opoly(t_a))=c_Polynomial_OpCons(c_Polynomial_Opoly(v_p,X0,t_a),c_Polynomial_Osynthetic__div(v_p,X0,t_a),t_a))),
% 31.21/4.70 inference(forward_demodulation,[status(thm)],[f18258,f71493])).
% 31.21/4.70 fof(f71498,plain,(
% 31.21/4.70 ![X0]: (v_p=c_Polynomial_OpCons(c_Polynomial_Opoly(v_p,X0,t_a),c_Polynomial_Osynthetic__div(v_p,X0,t_a),t_a))),
% 31.21/4.70 inference(forward_demodulation,[status(thm)],[f5542,f71497])).
% 31.21/4.70 fof(f71499,plain,(
% 31.21/4.70 ![X0]: (v_p=c_Polynomial_OpCons(c_Polynomial_Opoly(v_p,X0,t_a),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)),t_a))),
% 31.21/4.70 inference(forward_demodulation,[status(thm)],[f71474,f71498])).
% 31.21/4.70 fof(f71500,plain,(
% 31.21/4.70 $false),
% 31.21/4.70 inference(forward_subsumption_resolution,[status(thm)],[f71499,f2228])).
% 31.21/4.70 % SZS output end CNFRefutation for theBenchmark.p
% 6.89/4.75 % Elapsed time: 4.295932 seconds
% 6.89/4.75 % CPU time: 32.376553 seconds
% 6.89/4.75 % Total memory used: 370.639 MB
% 6.89/4.75 % Net memory used: 358.721 MB
%------------------------------------------------------------------------------