%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : ALG401-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 : n014.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:08 AM UTC 2026
% Result : Unsatisfiable 159.47s 20.72s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ALG401-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.50 % Computer : n014.cluster.edu
% 0.08/0.50 % Model : x86_64 x86_64
% 0.08/0.50 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.50 % Memory : 8046.5625MB
% 0.08/0.50 % OS : Linux 6.8.0-71-generic
% 0.08/0.50 % CPULimit : 300
% 0.08/0.50 % WCLimit : 300
% 0.08/0.50 % DateTime : Mon Sep 21 13:19:19 UTC 2026
% 0.08/0.51 % CPUTime :
% 0.17/0.58 % Drodi V4.1.1
% 159.47/20.72 % Refutation found
% 159.47/20.72 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 159.47/20.72 % SZS output start CNFRefutation for theBenchmark
% 159.47/20.72 fof(f659,axiom,(
% 159.47/20.72 (![T_a,V_p,V_q]: (( ~ class_Ring__and__Field_Ofield(T_a)| ~ c_Ring__and__Field_Odvd__class_Odvd(c_Polynomial_Osmult(c_HOL_Ozero__class_Ozero(T_a),V_p,T_a),V_q,tc_Polynomial_Opoly(T_a))| V_q = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)) ) ))),
% 159.47/20.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 159.47/20.72 fof(f660,axiom,(
% 159.47/20.72 (![T_a,V_p]: (( ~ class_Ring__and__Field_Ofield(T_a)| c_Ring__and__Field_Odvd__class_Odvd(c_Polynomial_Osmult(c_HOL_Ozero__class_Ozero(T_a),V_p,T_a),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)),tc_Polynomial_Opoly(T_a)) ) ))),
% 159.47/20.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 159.47/20.72 fof(f666,axiom,(
% 159.47/20.72 (![T_a,V_p,V_c,V_q,V_r]: (( ~ class_Ring__and__Field_Ocomm__semiring__0(T_a)| c_HOL_Oplus__class_Oplus(V_p,c_Polynomial_Osmult(V_c,V_q,T_a),tc_Polynomial_Opoly(T_a)) != c_Polynomial_OpCons(V_r,V_q,T_a)| V_r = c_Polynomial_Opoly(V_p,V_c,T_a) ) ))),
% 159.47/20.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 159.47/20.72 fof(f673,axiom,(
% 159.47/20.72 (![T_a,V_p,V_q,V_a]: (( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a)| c_Ring__and__Field_Odvd__class_Odvd(V_p,V_q,tc_Polynomial_Opoly(T_a))| ~ c_Ring__and__Field_Odvd__class_Odvd(c_Polynomial_Osmult(V_a,V_p,T_a),V_q,tc_Polynomial_Opoly(T_a)) ) ))),
% 159.47/20.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 159.47/20.72 fof(f674,axiom,(
% 159.47/20.72 (![T_a,V_p,V_a,V_q]: (( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a)| c_Ring__and__Field_Odvd__class_Odvd(V_p,c_Polynomial_Osmult(V_a,V_q,T_a),tc_Polynomial_Opoly(T_a))| ~ c_Ring__and__Field_Odvd__class_Odvd(V_p,V_q,tc_Polynomial_Opoly(T_a)) ) ))),
% 159.47/20.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 159.47/20.72 fof(f758,axiom,(
% 159.47/20.72 (![V_z]: (c_Polynomial_Opoly(c_Polynomial_Osmult(c_HOL_Oinverse__class_Oinverse(c_Polynomial_Opoly(v_q____,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_q____,tc_Complex_Ocomplex),V_z,tc_Complex_Ocomplex) = c_HOL_Oplus__class_Oplus(c_Polynomial_Opoly(c_Polynomial_Osmult(c_HOL_Oinverse__class_Oinverse(c_Polynomial_Opoly(v_q____,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_q____,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(V_z,v_k____,tc_Complex_Ocomplex),c_Polynomial_Opoly(c_Polynomial_OpCons(v_a____,v_s____,tc_Complex_Ocomplex),V_z,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex) ))),
% 159.47/20.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 159.47/20.72 fof(f852,axiom,(
% 159.47/20.72 (![T_a,V_x,V_y]: (( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a)| c_HOL_Otimes__class_Otimes(V_x,V_y,T_a) = c_HOL_Otimes__class_Otimes(V_y,V_x,T_a) ) ))),
% 159.47/20.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 159.47/20.72 fof(f866,axiom,(
% 159.47/20.72 c_Polynomial_Opoly(c_Polynomial_Osmult(c_HOL_Oinverse__class_Oinverse(c_Polynomial_Opoly(v_q____,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_q____,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Oone__class_Oone(tc_Complex_Ocomplex) ),
% 159.47/20.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 159.47/20.72 fof(f869,axiom,(
% 159.47/20.72 (![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 ) ))),
% 159.47/20.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 159.47/20.72 fof(f878,axiom,(
% 159.47/20.72 v_s____ = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
% 159.47/20.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 159.47/20.72 fof(f880,negated_conjecture,(
% 159.47/20.72 c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(c_Polynomial_Osmult(c_HOL_Oinverse__class_Oinverse(c_Polynomial_Opoly(v_q____,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_q____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex) != c_RealVector_Onorm__class_Onorm(c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(v_a____,c_Power_Opower__class_Opower(v_w____,v_k____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex) ),
% 159.47/20.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 159.47/20.72 fof(f988,axiom,(
% 159.47/20.72 class_Ring__and__Field_Ocomm__semiring__1(tc_Complex_Ocomplex) ),
% 159.47/20.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 159.47/20.72 fof(f989,axiom,(
% 159.47/20.72 class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex) ),
% 159.47/20.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 159.47/20.72 fof(f998,axiom,(
% 159.47/20.72 class_OrderedGroup_Ocomm__monoid__add(tc_Complex_Ocomplex) ),
% 159.47/20.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 159.47/20.72 fof(f1011,axiom,(
% 159.47/20.72 class_Ring__and__Field_Ofield(tc_Complex_Ocomplex) ),
% 159.47/20.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 159.47/20.72 fof(f1055,axiom,(
% 159.47/20.72 (![T_1]: (( class_OrderedGroup_Omonoid__add(tc_Polynomial_Opoly(T_1))| ~ class_OrderedGroup_Ocomm__monoid__add(T_1) ) ))),
% 159.47/20.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 159.47/20.72 fof(f2146,plain,(
% 159.47/20.72 ![T_a,V_q]: ((~class_Ring__and__Field_Ofield(T_a)|(![V_p]: ~c_Ring__and__Field_Odvd__class_Odvd(c_Polynomial_Osmult(c_HOL_Ozero__class_Ozero(T_a),V_p,T_a),V_q,tc_Polynomial_Opoly(T_a))))|V_q=c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)))),
% 159.47/20.72 inference(miniscoping,[status(thm)],[f659])).
% 159.47/20.72 fof(f2147,plain,(
% 159.47/20.72 ![X0,X1,X2]: (~class_Ring__and__Field_Ofield(X0)|~c_Ring__and__Field_Odvd__class_Odvd(c_Polynomial_Osmult(c_HOL_Ozero__class_Ozero(X0),X1,X0),X2,tc_Polynomial_Opoly(X0))|X2=c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)))),
% 159.47/20.72 inference(cnf_transformation,[status(thm)],[f2146])).
% 159.47/20.72 fof(f2148,plain,(
% 159.47/20.72 ![T_a]: (~class_Ring__and__Field_Ofield(T_a)|(![V_p]: c_Ring__and__Field_Odvd__class_Odvd(c_Polynomial_Osmult(c_HOL_Ozero__class_Ozero(T_a),V_p,T_a),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)),tc_Polynomial_Opoly(T_a))))),
% 159.47/20.72 inference(miniscoping,[status(thm)],[f660])).
% 159.47/20.72 fof(f2149,plain,(
% 159.47/20.72 ![X0,X1]: (~class_Ring__and__Field_Ofield(X0)|c_Ring__and__Field_Odvd__class_Odvd(c_Polynomial_Osmult(c_HOL_Ozero__class_Ozero(X0),X1,X0),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)),tc_Polynomial_Opoly(X0)))),
% 159.47/20.72 inference(cnf_transformation,[status(thm)],[f2148])).
% 159.47/20.72 fof(f2160,plain,(
% 159.47/20.72 ![T_a,V_p,V_c,V_r]: ((~class_Ring__and__Field_Ocomm__semiring__0(T_a)|(![V_q]: ~c_HOL_Oplus__class_Oplus(V_p,c_Polynomial_Osmult(V_c,V_q,T_a),tc_Polynomial_Opoly(T_a))=c_Polynomial_OpCons(V_r,V_q,T_a)))|V_r=c_Polynomial_Opoly(V_p,V_c,T_a))),
% 159.47/20.72 inference(miniscoping,[status(thm)],[f666])).
% 159.47/20.72 fof(f2161,plain,(
% 159.47/20.72 ![X0,X1,X2,X3,X4]: (~class_Ring__and__Field_Ocomm__semiring__0(X0)|~c_HOL_Oplus__class_Oplus(X1,c_Polynomial_Osmult(X2,X3,X0),tc_Polynomial_Opoly(X0))=c_Polynomial_OpCons(X4,X3,X0)|X4=c_Polynomial_Opoly(X1,X2,X0))),
% 159.47/20.72 inference(cnf_transformation,[status(thm)],[f2160])).
% 159.47/20.72 fof(f2174,plain,(
% 159.47/20.72 ![T_a,V_p,V_q]: ((~class_Ring__and__Field_Ocomm__semiring__1(T_a)|c_Ring__and__Field_Odvd__class_Odvd(V_p,V_q,tc_Polynomial_Opoly(T_a)))|(![V_a]: ~c_Ring__and__Field_Odvd__class_Odvd(c_Polynomial_Osmult(V_a,V_p,T_a),V_q,tc_Polynomial_Opoly(T_a))))),
% 159.47/20.72 inference(miniscoping,[status(thm)],[f673])).
% 159.47/20.72 fof(f2175,plain,(
% 159.47/20.72 ![X0,X1,X2,X3]: (~class_Ring__and__Field_Ocomm__semiring__1(X0)|c_Ring__and__Field_Odvd__class_Odvd(X1,X2,tc_Polynomial_Opoly(X0))|~c_Ring__and__Field_Odvd__class_Odvd(c_Polynomial_Osmult(X3,X1,X0),X2,tc_Polynomial_Opoly(X0)))),
% 159.47/20.72 inference(cnf_transformation,[status(thm)],[f2174])).
% 159.47/20.72 fof(f2176,plain,(
% 159.47/20.72 ![T_a,V_p,V_q]: ((~class_Ring__and__Field_Ocomm__semiring__1(T_a)|(![V_a]: c_Ring__and__Field_Odvd__class_Odvd(V_p,c_Polynomial_Osmult(V_a,V_q,T_a),tc_Polynomial_Opoly(T_a))))|~c_Ring__and__Field_Odvd__class_Odvd(V_p,V_q,tc_Polynomial_Opoly(T_a)))),
% 159.47/20.72 inference(miniscoping,[status(thm)],[f674])).
% 159.47/20.72 fof(f2177,plain,(
% 159.47/20.72 ![X0,X1,X2,X3]: (~class_Ring__and__Field_Ocomm__semiring__1(X0)|c_Ring__and__Field_Odvd__class_Odvd(X1,c_Polynomial_Osmult(X2,X3,X0),tc_Polynomial_Opoly(X0))|~c_Ring__and__Field_Odvd__class_Odvd(X1,X3,tc_Polynomial_Opoly(X0)))),
% 159.47/20.72 inference(cnf_transformation,[status(thm)],[f2176])).
% 159.47/20.72 fof(f2316,plain,(
% 159.47/20.72 ![X0]: (c_Polynomial_Opoly(c_Polynomial_Osmult(c_HOL_Oinverse__class_Oinverse(c_Polynomial_Opoly(v_q____,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_q____,tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex)=c_HOL_Oplus__class_Oplus(c_Polynomial_Opoly(c_Polynomial_Osmult(c_HOL_Oinverse__class_Oinverse(c_Polynomial_Opoly(v_q____,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_q____,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(X0,v_k____,tc_Complex_Ocomplex),c_Polynomial_Opoly(c_Polynomial_OpCons(v_a____,v_s____,tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex))),
% 159.47/20.72 inference(cnf_transformation,[status(thm)],[f758])).
% 159.47/20.72 fof(f2485,plain,(
% 159.47/20.72 ![T_a]: (~class_Ring__and__Field_Ocomm__semiring__1(T_a)|(![V_x,V_y]: c_HOL_Otimes__class_Otimes(V_x,V_y,T_a)=c_HOL_Otimes__class_Otimes(V_y,V_x,T_a)))),
% 159.47/20.72 inference(miniscoping,[status(thm)],[f852])).
% 159.47/20.72 fof(f2486,plain,(
% 159.47/20.72 ![X0,X1,X2]: (~class_Ring__and__Field_Ocomm__semiring__1(X0)|c_HOL_Otimes__class_Otimes(X1,X2,X0)=c_HOL_Otimes__class_Otimes(X2,X1,X0))),
% 159.47/20.72 inference(cnf_transformation,[status(thm)],[f2485])).
% 159.47/20.72 fof(f2511,plain,(
% 159.47/20.72 c_Polynomial_Opoly(c_Polynomial_Osmult(c_HOL_Oinverse__class_Oinverse(c_Polynomial_Opoly(v_q____,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_q____,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex)=c_HOL_Oone__class_Oone(tc_Complex_Ocomplex)),
% 159.47/20.72 inference(cnf_transformation,[status(thm)],[f866])).
% 159.47/20.72 fof(f2516,plain,(
% 159.47/20.72 ![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))),
% 159.47/20.72 inference(miniscoping,[status(thm)],[f869])).
% 159.47/20.72 fof(f2517,plain,(
% 159.47/20.72 ![X0,X1]: (~class_OrderedGroup_Omonoid__add(X0)|c_HOL_Oplus__class_Oplus(X1,c_HOL_Ozero__class_Ozero(X0),X0)=X1)),
% 159.47/20.72 inference(cnf_transformation,[status(thm)],[f2516])).
% 159.47/20.72 fof(f2533,plain,(
% 159.47/20.72 v_s____=c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))),
% 159.47/20.72 inference(cnf_transformation,[status(thm)],[f878])).
% 159.47/20.72 fof(f2535,plain,(
% 159.47/20.72 ~c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(c_Polynomial_Osmult(c_HOL_Oinverse__class_Oinverse(c_Polynomial_Opoly(v_q____,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_q____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex)=c_RealVector_Onorm__class_Onorm(c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(v_a____,c_Power_Opower__class_Opower(v_w____,v_k____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex)),
% 159.47/20.72 inference(cnf_transformation,[status(thm)],[f880])).
% 159.47/20.72 fof(f2643,plain,(
% 159.47/20.72 class_Ring__and__Field_Ocomm__semiring__1(tc_Complex_Ocomplex)),
% 159.47/20.72 inference(cnf_transformation,[status(thm)],[f988])).
% 159.47/20.72 fof(f2644,plain,(
% 159.47/20.72 class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex)),
% 159.47/20.72 inference(cnf_transformation,[status(thm)],[f989])).
% 159.47/20.72 fof(f2653,plain,(
% 159.47/20.72 class_OrderedGroup_Ocomm__monoid__add(tc_Complex_Ocomplex)),
% 159.47/20.72 inference(cnf_transformation,[status(thm)],[f998])).
% 159.47/20.72 fof(f2666,plain,(
% 159.47/20.72 class_Ring__and__Field_Ofield(tc_Complex_Ocomplex)),
% 159.47/20.72 inference(cnf_transformation,[status(thm)],[f1011])).
% 159.47/20.72 fof(f2710,plain,(
% 159.47/20.72 ![X0]: (class_OrderedGroup_Omonoid__add(tc_Polynomial_Opoly(X0))|~class_OrderedGroup_Ocomm__monoid__add(X0))),
% 159.47/20.72 inference(cnf_transformation,[status(thm)],[f1055])).
% 159.47/20.72 fof(f2739,plain,(
% 159.47/20.72 ![X0]: (c_Polynomial_Opoly(c_Polynomial_Osmult(c_HOL_Oinverse__class_Oinverse(c_Polynomial_Opoly(v_q____,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_q____,tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex)=c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(X0,v_k____,tc_Complex_Ocomplex),c_Polynomial_Opoly(c_Polynomial_OpCons(v_a____,v_s____,tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex))),
% 159.47/20.72 inference(forward_demodulation,[status(thm)],[f2511,f2316])).
% 159.47/20.72 fof(f3044,plain,(
% 159.47/20.72 ![X0]: (c_Ring__and__Field_Odvd__class_Odvd(c_Polynomial_Osmult(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)))),
% 159.47/20.72 inference(resolution,[status(thm)],[f2666,f2149])).
% 159.47/20.72 fof(f3070,plain,(
% 159.47/20.72 ![X0]: (~class_Ring__and__Field_Ocomm__semiring__1(tc_Complex_Ocomplex)|c_Ring__and__Field_Odvd__class_Odvd(X0,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)))),
% 159.47/20.72 inference(resolution,[status(thm)],[f3044,f2175])).
% 159.47/20.72 fof(f3077,plain,(
% 159.47/20.72 ![X0]: (c_Ring__and__Field_Odvd__class_Odvd(X0,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)))),
% 159.47/20.72 inference(forward_subsumption_resolution,[status(thm)],[f3070,f2643])).
% 159.47/20.72 fof(f3096,plain,(
% 159.47/20.72 ![X0,X1]: (~class_Ring__and__Field_Ocomm__semiring__1(tc_Complex_Ocomplex)|c_Ring__and__Field_Odvd__class_Odvd(X0,c_Polynomial_Osmult(X1,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex)))),
% 159.47/20.72 inference(resolution,[status(thm)],[f3077,f2177])).
% 159.47/20.72 fof(f3100,plain,(
% 159.47/20.72 ![X0,X1]: (c_Ring__and__Field_Odvd__class_Odvd(X0,c_Polynomial_Osmult(X1,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex)))),
% 159.47/20.72 inference(forward_subsumption_resolution,[status(thm)],[f3096,f2643])).
% 159.47/20.72 fof(f3101,plain,(
% 159.47/20.72 ![X0]: (~class_Ring__and__Field_Ofield(tc_Complex_Ocomplex)|c_Polynomial_Osmult(X0,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))),
% 159.47/20.72 inference(resolution,[status(thm)],[f3100,f2147])).
% 159.47/20.72 fof(f3111,plain,(
% 159.47/20.72 ![X0]: (c_Polynomial_Osmult(X0,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))),
% 159.47/20.72 inference(forward_subsumption_resolution,[status(thm)],[f3101,f2666])).
% 159.47/20.72 fof(f3190,plain,(
% 159.47/20.72 ![X0]: (c_Polynomial_Osmult(X0,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex)=v_s____)),
% 159.47/20.72 inference(backward_demodulation,[status(thm)],[f2533,f3111])).
% 159.47/20.72 fof(f3226,plain,(
% 159.47/20.72 ![X0]: (c_Polynomial_Osmult(X0,v_s____,tc_Complex_Ocomplex)=v_s____)),
% 159.47/20.72 inference(forward_demodulation,[status(thm)],[f2533,f3190])).
% 159.47/20.72 fof(f4371,plain,(
% 159.47/20.72 class_OrderedGroup_Omonoid__add(tc_Polynomial_Opoly(tc_Complex_Ocomplex))),
% 159.47/20.72 inference(resolution,[status(thm)],[f2710,f2653])).
% 159.47/20.72 fof(f11224,plain,(
% 159.47/20.72 ![X0]: (c_HOL_Oplus__class_Oplus(X0,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex))=X0)),
% 159.47/20.72 inference(resolution,[status(thm)],[f2517,f4371])).
% 159.47/20.72 fof(f11228,plain,(
% 159.47/20.72 ![X0]: (c_HOL_Oplus__class_Oplus(X0,v_s____,tc_Polynomial_Opoly(tc_Complex_Ocomplex))=X0)),
% 159.47/20.72 inference(forward_demodulation,[status(thm)],[f2533,f11224])).
% 159.47/20.72 fof(f20972,plain,(
% 159.47/20.72 ![X0,X1]: (c_HOL_Otimes__class_Otimes(X0,X1,tc_Complex_Ocomplex)=c_HOL_Otimes__class_Otimes(X1,X0,tc_Complex_Ocomplex))),
% 159.47/20.72 inference(resolution,[status(thm)],[f2486,f2643])).
% 159.47/20.72 fof(f100926,plain,(
% 159.47/20.72 ![X0,X1,X2]: (~class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex)|~c_HOL_Oplus__class_Oplus(X0,v_s____,tc_Polynomial_Opoly(tc_Complex_Ocomplex))=c_Polynomial_OpCons(X1,v_s____,tc_Complex_Ocomplex)|X1=c_Polynomial_Opoly(X0,X2,tc_Complex_Ocomplex))),
% 159.47/20.72 inference(paramodulation,[status(thm)],[f3226,f2161])).
% 159.47/20.72 fof(f100972,plain,(
% 159.47/20.72 ![X0,X1,X2]: (~class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex)|~X0=c_Polynomial_OpCons(X1,v_s____,tc_Complex_Ocomplex)|X1=c_Polynomial_Opoly(X0,X2,tc_Complex_Ocomplex))),
% 159.47/20.72 inference(forward_demodulation,[status(thm)],[f11228,f100926])).
% 159.47/20.72 fof(f100973,plain,(
% 159.47/20.72 ![X1,X2]: (~class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex)|X1=c_Polynomial_Opoly(c_Polynomial_OpCons(X1,v_s____,tc_Complex_Ocomplex),X2,tc_Complex_Ocomplex))),
% 116.75/20.85 inference(destructive_equality_resolution,[status(thm)],[f100972])).
% 116.75/20.85 fof(f100974,plain,(
% 116.75/20.85 ![X0,X1]: (X0=c_Polynomial_Opoly(c_Polynomial_OpCons(X0,v_s____,tc_Complex_Ocomplex),X1,tc_Complex_Ocomplex))),
% 116.75/20.85 inference(forward_subsumption_resolution,[status(thm)],[f100973,f2644])).
% 116.75/20.85 fof(f101009,plain,(
% 116.75/20.85 ![X0]: (c_Polynomial_Opoly(c_Polynomial_Osmult(c_HOL_Oinverse__class_Oinverse(c_Polynomial_Opoly(v_q____,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_q____,tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex)=c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(X0,v_k____,tc_Complex_Ocomplex),v_a____,tc_Complex_Ocomplex),tc_Complex_Ocomplex))),
% 116.75/20.85 inference(backward_demodulation,[status(thm)],[f100974,f2739])).
% 116.75/20.85 fof(f101025,plain,(
% 116.75/20.85 ~c_RealVector_Onorm__class_Onorm(c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(v_w____,v_k____,tc_Complex_Ocomplex),v_a____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex)=c_RealVector_Onorm__class_Onorm(c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(v_a____,c_Power_Opower__class_Opower(v_w____,v_k____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex)),
% 116.75/20.85 inference(backward_demodulation,[status(thm)],[f101009,f2535])).
% 116.75/20.85 fof(f101371,plain,(
% 116.75/20.85 ~c_RealVector_Onorm__class_Onorm(c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(v_a____,c_Power_Opower__class_Opower(v_w____,v_k____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex)=c_RealVector_Onorm__class_Onorm(c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(v_a____,c_Power_Opower__class_Opower(v_w____,v_k____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex)),
% 116.75/20.85 inference(paramodulation,[status(thm)],[f20972,f101025])).
% 116.75/20.85 fof(f101373,plain,(
% 116.75/20.85 $false),
% 116.75/20.85 inference(trivial_equality_resolution,[status(thm)],[f101371])).
% 116.75/20.85 % SZS output end CNFRefutation for theBenchmark.p
% 116.75/20.90 % Elapsed time: 20.374481 seconds
% 116.75/20.90 % CPU time: 160.718452 seconds
% 116.75/20.90 % Total memory used: 1.347 GB
% 116.75/20.90 % Net memory used: 1.303 GB
%------------------------------------------------------------------------------