%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV621-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n012.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 02:52:55 PM UTC 2026
% Result : Unsatisfiable 35.68s 4.93s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SWV621-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.02 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.03/0.29 % Computer : n012.cluster.edu
% 0.03/0.29 % Model : x86_64 x86_64
% 0.03/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.29 % Memory : 8046.5625MB
% 0.03/0.29 % OS : Linux 6.8.0-71-generic
% 0.03/0.29 % CPULimit : 300
% 0.03/0.29 % WCLimit : 300
% 0.03/0.29 % DateTime : Mon Sep 21 09:14:21 UTC 2026
% 0.03/0.30 % CPUTime :
% 0.10/0.36 % Drodi V4.1.1
% 35.68/4.93 % Refutation found
% 35.68/4.93 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 35.68/4.93 % SZS output start CNFRefutation for theBenchmark
% 35.68/4.93 fof(f16,axiom,(
% 35.68/4.93 (![V_k,V_m,V_n]: (( c_HOL_Otimes__class_Otimes(V_k,V_m,tc_nat) != c_HOL_Otimes__class_Otimes(V_k,V_n,tc_nat)| ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),V_k))| V_m = V_n ) ))),
% 35.68/4.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 35.68/4.93 fof(f179,axiom,(
% 35.68/4.93 (![T_a]: (( ~ class_Ring__and__Field_Odivision__by__zero(T_a)| c_HOL_Oinverse__class_Oinverse(c_HOL_Ozero__class_Ozero(T_a),T_a) = c_HOL_Ozero__class_Ozero(T_a) ) ))),
% 35.68/4.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 35.68/4.93 fof(f294,axiom,(
% 35.68/4.93 (![T_a,V_a]: (( ~ class_Ring__and__Field_Ofield(T_a)| c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Oinverse(V_a,T_a),V_a,T_a) = c_HOL_Oone__class_Oone(T_a)| V_a = c_HOL_Ozero__class_Ozero(T_a) ) ))),
% 35.68/4.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 35.68/4.93 fof(f372,axiom,(
% 35.68/4.93 (![T_a,V_a]: (( ~ class_OrderedGroup_Omonoid__mult(T_a)| c_HOL_Otimes__class_Otimes(V_a,c_HOL_Oone__class_Oone(T_a),T_a) = V_a ) ))),
% 35.68/4.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 35.68/4.93 fof(f381,axiom,(
% 35.68/4.93 (![V_n]: (( hBOOL(hAPP(c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),V_n))| V_n = c_HOL_Ozero__class_Ozero(tc_nat) ) ))),
% 35.68/4.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 35.68/4.93 fof(f385,axiom,(
% 35.68/4.93 (![V_m]: (c_HOL_Otimes__class_Otimes(V_m,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) = c_HOL_Ozero__class_Ozero(tc_nat) ))),
% 35.68/4.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 35.68/4.93 fof(f511,axiom,(
% 35.68/4.93 (![T_a,V_a,V_n]: (( ~ class_Ring__and__Field_Odivision__ring(T_a)| ~ class_Ring__and__Field_Odivision__by__zero(T_a)| c_HOL_Oinverse__class_Oinverse(hAPP(c_Power_Opower__class_Opower(V_a,T_a),V_n),T_a) = hAPP(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Oinverse(V_a,T_a),T_a),V_n) ) ))),
% 35.68/4.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 35.68/4.93 fof(f518,axiom,(
% 35.68/4.93 (![T_a,V_a,V_b]: (( ~ class_Ring__and__Field_Ofield(T_a)| ~ class_Ring__and__Field_Odivision__by__zero(T_a)| c_HOL_Oinverse__class_Oinverse(c_HOL_Oinverse__class_Odivide(V_a,V_b,T_a),T_a) = c_HOL_Oinverse__class_Odivide(V_b,V_a,T_a) ) ))),
% 35.68/4.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 35.68/4.93 fof(f726,axiom,(
% 35.68/4.93 (![V_n]: (c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat) = c_SetInterval_Oord__class_OlessThan(V_n,tc_nat) ))),
% 35.68/4.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 35.68/4.93 fof(f728,axiom,(
% 35.68/4.93 hBOOL(hAPP(c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),v_k)) ),
% 35.68/4.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 35.68/4.93 fof(f729,axiom,(
% 35.68/4.93 hBOOL(hAPP(c_HOL_Oord__class_Oless(v_k,tc_nat),v_n)) ),
% 35.68/4.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 35.68/4.93 fof(f748,axiom,(
% 35.68/4.93 (![V_n,V_k]: (( c_Finite__Set_Osetsum(c_Power_Opower__class_Opower(hAPP(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(V_n),tc_Complex_Ocomplex),V_k),tc_Complex_Ocomplex),c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat),tc_nat,tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)| ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_k,tc_nat),V_n))| ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),V_k)) ) ))),
% 35.68/4.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 35.68/4.93 fof(f754,axiom,(
% 35.68/4.93 (![T_a]: (( ~ class_Ring__and__Field_Ozero__neq__one(T_a)| c_HOL_Ozero__class_Ozero(T_a) != c_HOL_Oone__class_Oone(T_a) ) ))),
% 35.68/4.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 35.68/4.93 fof(f756,axiom,(
% 35.68/4.93 (![T_a,V_a]: (( ~ class_Ring__and__Field_Ofield(T_a)| c_HOL_Oinverse__class_Odivide(V_a,c_HOL_Oone__class_Oone(T_a),T_a) = V_a ) ))),
% 35.68/4.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 35.68/4.93 fof(f767,axiom,(
% 35.68/4.93 (![T_a,V_a,V_b,V_c]: (( ~ class_Ring__and__Field_Ofield(T_a)| c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(V_a,V_b,T_a),V_c,T_a) = c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(V_a,V_c,T_a),c_HOL_Oinverse__class_Odivide(V_b,V_c,T_a),T_a) ) ))),
% 35.68/4.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 35.68/4.93 fof(f769,axiom,(
% 35.68/4.93 (![T_a,V_x]: (( ~ class_OrderedGroup_Oab__group__add(T_a)| c_HOL_Ominus__class_Ominus(V_x,V_x,T_a) = c_HOL_Ozero__class_Ozero(T_a) ) ))),
% 35.68/4.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 35.68/4.93 fof(f788,axiom,(
% 35.68/4.93 (![T_a,V_x,V_n]: (( ~ class_Ring__and__Field_Ofield(T_a)| c_Finite__Set_Osetsum(c_Power_Opower__class_Opower(V_x,T_a),c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat),tc_nat,T_a) = c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(hAPP(c_Power_Opower__class_Opower(V_x,T_a),V_n),c_HOL_Oone__class_Oone(T_a),T_a),c_HOL_Ominus__class_Ominus(V_x,c_HOL_Oone__class_Oone(T_a),T_a),T_a)| V_x = c_HOL_Oone__class_Oone(T_a) ) ))),
% 35.68/4.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 35.68/4.93 fof(f789,negated_conjecture,(
% 35.68/4.93 c_Finite__Set_Osetsum(c_Power_Opower__class_Opower(hAPP(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_k),tc_Complex_Ocomplex),c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),v_n,tc_nat),tc_nat,tc_Complex_Ocomplex) != c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(hAPP(c_Power_Opower__class_Opower(hAPP(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_k),tc_Complex_Ocomplex),v_n),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Ominus__class_Ominus(hAPP(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_k),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex) ),
% 35.68/4.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 35.68/4.93 fof(f807,axiom,(
% 35.68/4.93 class_Ring__and__Field_Ozero__neq__one(tc_nat) ),
% 35.68/4.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 35.68/4.93 fof(f812,axiom,(
% 35.68/4.93 class_OrderedGroup_Omonoid__mult(tc_nat) ),
% 35.68/4.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 35.68/4.93 fof(f870,axiom,(
% 35.68/4.93 class_Ring__and__Field_Odivision__by__zero(tc_Complex_Ocomplex) ),
% 35.68/4.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 35.68/4.93 fof(f876,axiom,(
% 35.68/4.93 class_Ring__and__Field_Odivision__ring(tc_Complex_Ocomplex) ),
% 35.68/4.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 35.68/4.93 fof(f879,axiom,(
% 35.68/4.93 class_Ring__and__Field_Ozero__neq__one(tc_Complex_Ocomplex) ),
% 35.68/4.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 35.68/4.93 fof(f882,axiom,(
% 35.68/4.93 class_OrderedGroup_Oab__group__add(tc_Complex_Ocomplex) ),
% 35.68/4.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 35.68/4.93 fof(f884,axiom,(
% 35.68/4.93 class_OrderedGroup_Omonoid__mult(tc_Complex_Ocomplex) ),
% 35.68/4.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 35.68/4.93 fof(f887,axiom,(
% 35.68/4.93 class_Ring__and__Field_Ofield(tc_Complex_Ocomplex) ),
% 35.68/4.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 35.68/4.93 fof(f922,plain,(
% 35.68/4.93 ![V_m,V_n]: ((![V_k]: (~c_HOL_Otimes__class_Otimes(V_k,V_m,tc_nat)=c_HOL_Otimes__class_Otimes(V_k,V_n,tc_nat)|~hBOOL(hAPP(c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),V_k))))|V_m=V_n)),
% 35.68/4.93 inference(miniscoping,[status(thm)],[f16])).
% 35.68/4.93 fof(f923,plain,(
% 35.68/4.93 ![X0,X1,X2]: (~c_HOL_Otimes__class_Otimes(X0,X1,tc_nat)=c_HOL_Otimes__class_Otimes(X0,X2,tc_nat)|~hBOOL(hAPP(c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),X0))|X1=X2)),
% 35.68/4.93 inference(cnf_transformation,[status(thm)],[f922])).
% 35.68/4.93 fof(f1160,plain,(
% 35.68/4.93 ![X0]: (~class_Ring__and__Field_Odivision__by__zero(X0)|c_HOL_Oinverse__class_Oinverse(c_HOL_Ozero__class_Ozero(X0),X0)=c_HOL_Ozero__class_Ozero(X0))),
% 35.68/4.93 inference(cnf_transformation,[status(thm)],[f179])).
% 35.68/4.93 fof(f1339,plain,(
% 35.68/4.93 ![X0,X1]: (~class_Ring__and__Field_Ofield(X0)|c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Oinverse(X1,X0),X1,X0)=c_HOL_Oone__class_Oone(X0)|X1=c_HOL_Ozero__class_Ozero(X0))),
% 35.68/4.93 inference(cnf_transformation,[status(thm)],[f294])).
% 35.68/4.93 fof(f1475,plain,(
% 35.68/4.93 ![T_a]: (~class_OrderedGroup_Omonoid__mult(T_a)|(![V_a]: c_HOL_Otimes__class_Otimes(V_a,c_HOL_Oone__class_Oone(T_a),T_a)=V_a))),
% 35.68/4.93 inference(miniscoping,[status(thm)],[f372])).
% 35.68/4.93 fof(f1476,plain,(
% 35.68/4.93 ![X0,X1]: (~class_OrderedGroup_Omonoid__mult(X0)|c_HOL_Otimes__class_Otimes(X1,c_HOL_Oone__class_Oone(X0),X0)=X1)),
% 35.68/4.93 inference(cnf_transformation,[status(thm)],[f1475])).
% 35.68/4.93 fof(f1490,plain,(
% 35.68/4.93 ![X0]: (hBOOL(hAPP(c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),X0))|X0=c_HOL_Ozero__class_Ozero(tc_nat))),
% 35.68/4.93 inference(cnf_transformation,[status(thm)],[f381])).
% 35.68/4.93 fof(f1494,plain,(
% 35.68/4.93 ![X0]: (c_HOL_Otimes__class_Otimes(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat)=c_HOL_Ozero__class_Ozero(tc_nat))),
% 35.68/4.93 inference(cnf_transformation,[status(thm)],[f385])).
% 35.68/4.93 fof(f1688,plain,(
% 35.68/4.93 ![T_a]: ((~class_Ring__and__Field_Odivision__ring(T_a)|~class_Ring__and__Field_Odivision__by__zero(T_a))|(![V_a,V_n]: c_HOL_Oinverse__class_Oinverse(hAPP(c_Power_Opower__class_Opower(V_a,T_a),V_n),T_a)=hAPP(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Oinverse(V_a,T_a),T_a),V_n)))),
% 35.68/4.93 inference(miniscoping,[status(thm)],[f511])).
% 35.68/4.93 fof(f1689,plain,(
% 35.68/4.93 ![X0,X1,X2]: (~class_Ring__and__Field_Odivision__ring(X0)|~class_Ring__and__Field_Odivision__by__zero(X0)|c_HOL_Oinverse__class_Oinverse(hAPP(c_Power_Opower__class_Opower(X1,X0),X2),X0)=hAPP(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Oinverse(X1,X0),X0),X2))),
% 35.68/4.93 inference(cnf_transformation,[status(thm)],[f1688])).
% 35.68/4.93 fof(f1702,plain,(
% 35.68/4.93 ![T_a]: ((~class_Ring__and__Field_Ofield(T_a)|~class_Ring__and__Field_Odivision__by__zero(T_a))|(![V_a,V_b]: c_HOL_Oinverse__class_Oinverse(c_HOL_Oinverse__class_Odivide(V_a,V_b,T_a),T_a)=c_HOL_Oinverse__class_Odivide(V_b,V_a,T_a)))),
% 35.68/4.93 inference(miniscoping,[status(thm)],[f518])).
% 35.68/4.93 fof(f1703,plain,(
% 35.68/4.93 ![X0,X1,X2]: (~class_Ring__and__Field_Ofield(X0)|~class_Ring__and__Field_Odivision__by__zero(X0)|c_HOL_Oinverse__class_Oinverse(c_HOL_Oinverse__class_Odivide(X1,X2,X0),X0)=c_HOL_Oinverse__class_Odivide(X2,X1,X0))),
% 35.68/4.93 inference(cnf_transformation,[status(thm)],[f1702])).
% 35.68/4.93 fof(f2030,plain,(
% 35.68/4.93 ![X0]: (c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat)=c_SetInterval_Oord__class_OlessThan(X0,tc_nat))),
% 35.68/4.93 inference(cnf_transformation,[status(thm)],[f726])).
% 35.68/4.93 fof(f2032,plain,(
% 35.68/4.93 hBOOL(hAPP(c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),v_k))),
% 35.68/4.93 inference(cnf_transformation,[status(thm)],[f728])).
% 35.68/4.93 fof(f2033,plain,(
% 35.68/4.93 hBOOL(hAPP(c_HOL_Oord__class_Oless(v_k,tc_nat),v_n))),
% 35.68/4.93 inference(cnf_transformation,[status(thm)],[f729])).
% 35.68/4.93 fof(f2060,plain,(
% 35.68/4.93 ![V_k]: ((![V_n]: (c_Finite__Set_Osetsum(c_Power_Opower__class_Opower(hAPP(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(V_n),tc_Complex_Ocomplex),V_k),tc_Complex_Ocomplex),c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat),tc_nat,tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)|~hBOOL(hAPP(c_HOL_Oord__class_Oless(V_k,tc_nat),V_n))))|~hBOOL(hAPP(c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),V_k)))),
% 35.68/4.93 inference(miniscoping,[status(thm)],[f748])).
% 35.68/4.93 fof(f2061,plain,(
% 35.68/4.93 ![X0,X1]: (c_Finite__Set_Osetsum(c_Power_Opower__class_Opower(hAPP(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(X0),tc_Complex_Ocomplex),X1),tc_Complex_Ocomplex),c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat),tc_nat,tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)|~hBOOL(hAPP(c_HOL_Oord__class_Oless(X1,tc_nat),X0))|~hBOOL(hAPP(c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),X1)))),
% 35.68/4.93 inference(cnf_transformation,[status(thm)],[f2060])).
% 35.68/4.93 fof(f2071,plain,(
% 35.68/4.93 ![X0]: (~class_Ring__and__Field_Ozero__neq__one(X0)|~c_HOL_Ozero__class_Ozero(X0)=c_HOL_Oone__class_Oone(X0))),
% 35.68/4.93 inference(cnf_transformation,[status(thm)],[f754])).
% 35.68/4.93 fof(f2073,plain,(
% 35.68/4.93 ![T_a]: (~class_Ring__and__Field_Ofield(T_a)|(![V_a]: c_HOL_Oinverse__class_Odivide(V_a,c_HOL_Oone__class_Oone(T_a),T_a)=V_a))),
% 35.68/4.93 inference(miniscoping,[status(thm)],[f756])).
% 35.68/4.93 fof(f2074,plain,(
% 35.68/4.93 ![X0,X1]: (~class_Ring__and__Field_Ofield(X0)|c_HOL_Oinverse__class_Odivide(X1,c_HOL_Oone__class_Oone(X0),X0)=X1)),
% 35.68/4.93 inference(cnf_transformation,[status(thm)],[f2073])).
% 35.68/4.93 fof(f2093,plain,(
% 35.68/4.93 ![T_a]: (~class_Ring__and__Field_Ofield(T_a)|(![V_a,V_b,V_c]: c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(V_a,V_b,T_a),V_c,T_a)=c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(V_a,V_c,T_a),c_HOL_Oinverse__class_Odivide(V_b,V_c,T_a),T_a)))),
% 35.68/4.93 inference(miniscoping,[status(thm)],[f767])).
% 35.68/4.93 fof(f2094,plain,(
% 35.68/4.93 ![X0,X1,X2,X3]: (~class_Ring__and__Field_Ofield(X0)|c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(X1,X2,X0),X3,X0)=c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(X1,X3,X0),c_HOL_Oinverse__class_Odivide(X2,X3,X0),X0))),
% 35.68/4.93 inference(cnf_transformation,[status(thm)],[f2093])).
% 35.68/4.93 fof(f2097,plain,(
% 35.68/4.93 ![T_a]: (~class_OrderedGroup_Oab__group__add(T_a)|(![V_x]: c_HOL_Ominus__class_Ominus(V_x,V_x,T_a)=c_HOL_Ozero__class_Ozero(T_a)))),
% 35.68/4.93 inference(miniscoping,[status(thm)],[f769])).
% 35.68/4.93 fof(f2098,plain,(
% 35.68/4.93 ![X0,X1]: (~class_OrderedGroup_Oab__group__add(X0)|c_HOL_Ominus__class_Ominus(X1,X1,X0)=c_HOL_Ozero__class_Ozero(X0))),
% 35.68/4.93 inference(cnf_transformation,[status(thm)],[f2097])).
% 35.68/4.93 fof(f2132,plain,(
% 35.68/4.93 ![T_a,V_x]: ((~class_Ring__and__Field_Ofield(T_a)|(![V_n]: c_Finite__Set_Osetsum(c_Power_Opower__class_Opower(V_x,T_a),c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat),tc_nat,T_a)=c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(hAPP(c_Power_Opower__class_Opower(V_x,T_a),V_n),c_HOL_Oone__class_Oone(T_a),T_a),c_HOL_Ominus__class_Ominus(V_x,c_HOL_Oone__class_Oone(T_a),T_a),T_a)))|V_x=c_HOL_Oone__class_Oone(T_a))),
% 35.68/4.93 inference(miniscoping,[status(thm)],[f788])).
% 35.68/4.93 fof(f2133,plain,(
% 35.68/4.93 ![X0,X1,X2]: (~class_Ring__and__Field_Ofield(X0)|c_Finite__Set_Osetsum(c_Power_Opower__class_Opower(X1,X0),c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),X2,tc_nat),tc_nat,X0)=c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(hAPP(c_Power_Opower__class_Opower(X1,X0),X2),c_HOL_Oone__class_Oone(X0),X0),c_HOL_Ominus__class_Ominus(X1,c_HOL_Oone__class_Oone(X0),X0),X0)|X1=c_HOL_Oone__class_Oone(X0))),
% 35.68/4.93 inference(cnf_transformation,[status(thm)],[f2132])).
% 35.68/4.93 fof(f2134,plain,(
% 35.68/4.93 ~c_Finite__Set_Osetsum(c_Power_Opower__class_Opower(hAPP(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_k),tc_Complex_Ocomplex),c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),v_n,tc_nat),tc_nat,tc_Complex_Ocomplex)=c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(hAPP(c_Power_Opower__class_Opower(hAPP(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_k),tc_Complex_Ocomplex),v_n),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Ominus__class_Ominus(hAPP(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_k),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex)),
% 35.68/4.93 inference(cnf_transformation,[status(thm)],[f789])).
% 35.68/4.93 fof(f2158,plain,(
% 35.68/4.93 class_Ring__and__Field_Ozero__neq__one(tc_nat)),
% 35.68/4.93 inference(cnf_transformation,[status(thm)],[f807])).
% 35.68/4.93 fof(f2163,plain,(
% 35.68/4.93 class_OrderedGroup_Omonoid__mult(tc_nat)),
% 35.68/4.93 inference(cnf_transformation,[status(thm)],[f812])).
% 35.68/4.93 fof(f2221,plain,(
% 35.68/4.93 class_Ring__and__Field_Odivision__by__zero(tc_Complex_Ocomplex)),
% 35.68/4.93 inference(cnf_transformation,[status(thm)],[f870])).
% 35.68/4.93 fof(f2227,plain,(
% 35.68/4.93 class_Ring__and__Field_Odivision__ring(tc_Complex_Ocomplex)),
% 35.68/4.93 inference(cnf_transformation,[status(thm)],[f876])).
% 35.68/4.93 fof(f2230,plain,(
% 35.68/4.93 class_Ring__and__Field_Ozero__neq__one(tc_Complex_Ocomplex)),
% 35.68/4.93 inference(cnf_transformation,[status(thm)],[f879])).
% 35.68/4.93 fof(f2233,plain,(
% 35.68/4.93 class_OrderedGroup_Oab__group__add(tc_Complex_Ocomplex)),
% 35.68/4.93 inference(cnf_transformation,[status(thm)],[f882])).
% 35.68/4.93 fof(f2235,plain,(
% 35.68/4.93 class_OrderedGroup_Omonoid__mult(tc_Complex_Ocomplex)),
% 35.68/4.93 inference(cnf_transformation,[status(thm)],[f884])).
% 35.68/4.93 fof(f2238,plain,(
% 35.68/4.93 class_Ring__and__Field_Ofield(tc_Complex_Ocomplex)),
% 35.68/4.93 inference(cnf_transformation,[status(thm)],[f887])).
% 35.68/4.93 fof(f2500,plain,(
% 35.68/4.93 ![X0,X1]: (~c_HOL_Otimes__class_Otimes(v_k,X0,tc_nat)=c_HOL_Otimes__class_Otimes(v_k,X1,tc_nat)|X0=X1)),
% 35.68/4.93 inference(resolution,[status(thm)],[f2032,f923])).
% 35.68/4.93 fof(f2601,plain,(
% 35.68/4.93 ![X0]: (~c_HOL_Ozero__class_Ozero(tc_nat)=c_HOL_Otimes__class_Otimes(v_k,X0,tc_nat)|c_HOL_Ozero__class_Ozero(tc_nat)=X0)),
% 35.68/4.93 inference(paramodulation,[status(thm)],[f1494,f2500])).
% 35.68/4.93 fof(f2739,plain,(
% 35.68/4.93 ![X0,X1]: (c_Finite__Set_Osetsum(c_Power_Opower__class_Opower(hAPP(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(X0),tc_Complex_Ocomplex),X1),tc_Complex_Ocomplex),c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat),tc_nat,tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)|~hBOOL(hAPP(c_HOL_Oord__class_Oless(X1,tc_nat),X0))|X1=c_HOL_Ozero__class_Ozero(tc_nat))),
% 35.68/4.93 inference(resolution,[status(thm)],[f2061,f1490])).
% 35.68/4.93 fof(f2752,plain,(
% 35.68/4.93 ![X0,X1,X2]: (c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(X0,X1,tc_Complex_Ocomplex),X2,tc_Complex_Ocomplex)=c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(X0,X2,tc_Complex_Ocomplex),c_HOL_Oinverse__class_Odivide(X1,X2,tc_Complex_Ocomplex),tc_Complex_Ocomplex))),
% 35.68/4.93 inference(resolution,[status(thm)],[f2094,f2238])).
% 35.68/4.93 fof(f2753,plain,(
% 35.68/4.93 ![X0,X1]: (c_Finite__Set_Osetsum(c_Power_Opower__class_Opower(X0,tc_Complex_Ocomplex),c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),X1,tc_nat),tc_nat,tc_Complex_Ocomplex)=c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(hAPP(c_Power_Opower__class_Opower(X0,tc_Complex_Ocomplex),X1),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Ominus__class_Ominus(X0,c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex)|X0=c_HOL_Oone__class_Oone(tc_Complex_Ocomplex))),
% 35.68/4.93 inference(resolution,[status(thm)],[f2133,f2238])).
% 35.68/4.93 fof(f3962,plain,(
% 35.68/4.93 c_HOL_Oinverse__class_Oinverse(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)),
% 35.68/4.93 inference(resolution,[status(thm)],[f1160,f2221])).
% 35.68/4.93 fof(f6349,plain,(
% 35.68/4.93 ~c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)=c_HOL_Oone__class_Oone(tc_Complex_Ocomplex)),
% 35.68/4.93 inference(resolution,[status(thm)],[f2071,f2230])).
% 35.68/4.93 fof(f6351,plain,(
% 35.68/4.93 ~c_HOL_Ozero__class_Ozero(tc_nat)=c_HOL_Oone__class_Oone(tc_nat)),
% 35.68/4.93 inference(resolution,[status(thm)],[f2071,f2158])).
% 35.68/4.93 fof(f7623,plain,(
% 35.68/4.93 ![X0]: (c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Oinverse(X0,tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex)=c_HOL_Oone__class_Oone(tc_Complex_Ocomplex)|X0=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))),
% 35.68/4.93 inference(resolution,[status(thm)],[f1339,f2238])).
% 35.68/4.93 fof(f7738,plain,(
% 35.68/4.93 ![X0]: (c_HOL_Otimes__class_Otimes(X0,c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex)=X0)),
% 35.68/4.93 inference(resolution,[status(thm)],[f1476,f2235])).
% 35.68/4.93 fof(f7740,plain,(
% 35.68/4.93 ![X0]: (c_HOL_Otimes__class_Otimes(X0,c_HOL_Oone__class_Oone(tc_nat),tc_nat)=X0)),
% 35.68/4.93 inference(resolution,[status(thm)],[f1476,f2163])).
% 35.68/4.93 fof(f8008,plain,(
% 35.68/4.93 ~c_HOL_Ozero__class_Ozero(tc_nat)=v_k|c_HOL_Ozero__class_Ozero(tc_nat)=c_HOL_Oone__class_Oone(tc_nat)),
% 35.68/4.93 inference(paramodulation,[status(thm)],[f7740,f2601])).
% 35.68/4.93 fof(f8144,plain,(
% 35.68/4.93 ~c_HOL_Ozero__class_Ozero(tc_nat)=v_k),
% 35.68/4.93 inference(forward_subsumption_resolution,[status(thm)],[f8008,f6351])).
% 35.68/4.93 fof(f8633,plain,(
% 35.68/4.93 hAPP(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_k)=c_HOL_Oone__class_Oone(tc_Complex_Ocomplex)),
% 35.68/4.93 inference(resolution,[status(thm)],[f2753,f2134])).
% 35.68/4.93 fof(f8803,plain,(
% 35.68/4.93 ~c_Finite__Set_Osetsum(c_Power_Opower__class_Opower(hAPP(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_k),tc_Complex_Ocomplex),c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),v_n,tc_nat),tc_nat,tc_Complex_Ocomplex)=c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(hAPP(c_Power_Opower__class_Opower(hAPP(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_k),tc_Complex_Ocomplex),v_n),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Ominus__class_Ominus(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex)),
% 35.68/4.93 inference(backward_demodulation,[status(thm)],[f8633,f2134])).
% 35.68/4.93 fof(f8805,plain,(
% 35.68/4.93 ~c_Finite__Set_Osetsum(c_Power_Opower__class_Opower(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),v_n,tc_nat),tc_nat,tc_Complex_Ocomplex)=c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(hAPP(c_Power_Opower__class_Opower(hAPP(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_k),tc_Complex_Ocomplex),v_n),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Ominus__class_Ominus(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex)),
% 35.68/4.93 inference(forward_demodulation,[status(thm)],[f8633,f8803])).
% 35.68/4.93 fof(f8806,plain,(
% 35.68/4.93 ~c_Finite__Set_Osetsum(c_Power_Opower__class_Opower(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),v_n,tc_nat),tc_nat,tc_Complex_Ocomplex)=c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(hAPP(c_Power_Opower__class_Opower(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_n),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Ominus__class_Ominus(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex)),
% 35.68/4.93 inference(forward_demodulation,[status(thm)],[f8633,f8805])).
% 35.68/4.93 fof(f9607,plain,(
% 35.68/4.93 ![X0]: (c_HOL_Oinverse__class_Odivide(X0,c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex)=X0)),
% 35.68/4.93 inference(resolution,[status(thm)],[f2074,f2238])).
% 35.68/4.93 fof(f9791,plain,(
% 35.68/4.93 ![X0]: (c_HOL_Ominus__class_Ominus(X0,X0,tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))),
% 35.68/4.93 inference(resolution,[status(thm)],[f2098,f2233])).
% 35.68/4.93 fof(f9802,plain,(
% 35.68/4.93 ~c_Finite__Set_Osetsum(c_Power_Opower__class_Opower(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),v_n,tc_nat),tc_nat,tc_Complex_Ocomplex)=c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(hAPP(c_Power_Opower__class_Opower(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_n),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex)),
% 35.68/4.93 inference(backward_demodulation,[status(thm)],[f9791,f8806])).
% 35.68/4.93 fof(f9803,plain,(
% 35.68/4.93 ![X0,X1]: (c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(X0,X0,tc_Complex_Ocomplex),X1,tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))),
% 35.68/4.93 inference(paramodulation,[status(thm)],[f2752,f9791])).
% 35.68/4.93 fof(f9809,plain,(
% 35.68/4.93 ![X0]: (c_HOL_Oinverse__class_Odivide(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))),
% 35.68/4.93 inference(forward_demodulation,[status(thm)],[f9791,f9803])).
% 35.68/4.93 fof(f11740,plain,(
% 35.68/4.93 c_HOL_Oinverse__class_Oinverse(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex)=c_HOL_Oone__class_Oone(tc_Complex_Ocomplex)|c_HOL_Oone__class_Oone(tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)),
% 35.68/4.93 inference(paramodulation,[status(thm)],[f7738,f7623])).
% 35.68/4.93 fof(f11749,plain,(
% 35.68/4.93 c_HOL_Oinverse__class_Oinverse(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex)=c_HOL_Oone__class_Oone(tc_Complex_Ocomplex)),
% 35.68/4.93 inference(forward_subsumption_resolution,[status(thm)],[f11740,f6349])).
% 35.68/4.93 fof(f15964,plain,(
% 35.68/4.93 ![X0,X1]: (~class_Ring__and__Field_Odivision__by__zero(tc_Complex_Ocomplex)|c_HOL_Oinverse__class_Oinverse(hAPP(c_Power_Opower__class_Opower(X0,tc_Complex_Ocomplex),X1),tc_Complex_Ocomplex)=hAPP(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Oinverse(X0,tc_Complex_Ocomplex),tc_Complex_Ocomplex),X1))),
% 35.68/4.93 inference(resolution,[status(thm)],[f1689,f2227])).
% 35.68/4.93 fof(f15965,plain,(
% 35.68/4.93 ![X0,X1]: (c_HOL_Oinverse__class_Oinverse(hAPP(c_Power_Opower__class_Opower(X0,tc_Complex_Ocomplex),X1),tc_Complex_Ocomplex)=hAPP(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Oinverse(X0,tc_Complex_Ocomplex),tc_Complex_Ocomplex),X1))),
% 35.68/4.93 inference(forward_subsumption_resolution,[status(thm)],[f15964,f2221])).
% 35.68/4.93 fof(f16043,plain,(
% 35.68/4.93 c_HOL_Oinverse__class_Oinverse(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex)=hAPP(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Oinverse(c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_k)),
% 35.68/4.93 inference(paramodulation,[status(thm)],[f8633,f15965])).
% 35.68/4.93 fof(f16059,plain,(
% 35.68/4.93 c_HOL_Oone__class_Oone(tc_Complex_Ocomplex)=hAPP(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Oinverse(c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_k)),
% 35.68/4.93 inference(forward_demodulation,[status(thm)],[f11749,f16043])).
% 35.68/4.93 fof(f16207,plain,(
% 35.68/4.93 ![X0,X1]: (~class_Ring__and__Field_Odivision__by__zero(tc_Complex_Ocomplex)|c_HOL_Oinverse__class_Oinverse(c_HOL_Oinverse__class_Odivide(X0,X1,tc_Complex_Ocomplex),tc_Complex_Ocomplex)=c_HOL_Oinverse__class_Odivide(X1,X0,tc_Complex_Ocomplex))),
% 35.68/4.93 inference(resolution,[status(thm)],[f1703,f2238])).
% 35.68/4.93 fof(f16208,plain,(
% 35.68/4.93 ![X0,X1]: (c_HOL_Oinverse__class_Oinverse(c_HOL_Oinverse__class_Odivide(X0,X1,tc_Complex_Ocomplex),tc_Complex_Ocomplex)=c_HOL_Oinverse__class_Odivide(X1,X0,tc_Complex_Ocomplex))),
% 35.68/4.93 inference(forward_subsumption_resolution,[status(thm)],[f16207,f2221])).
% 35.68/4.93 fof(f16250,plain,(
% 35.68/4.93 c_HOL_Oone__class_Oone(tc_Complex_Ocomplex)=hAPP(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Odivide(c_FFT__Mirabelle_Oroot(v_n),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_k)),
% 35.68/4.93 inference(backward_demodulation,[status(thm)],[f16208,f16059])).
% 35.68/4.93 fof(f16258,plain,(
% 35.68/4.93 ![X0]: (c_HOL_Oinverse__class_Oinverse(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex)=c_HOL_Oinverse__class_Odivide(X0,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex))),
% 35.68/4.93 inference(paramodulation,[status(thm)],[f9809,f16208])).
% 35.68/4.93 fof(f16280,plain,(
% 35.68/4.93 c_HOL_Oone__class_Oone(tc_Complex_Ocomplex)=hAPP(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),v_k)),
% 35.68/4.93 inference(forward_demodulation,[status(thm)],[f9607,f16250])).
% 35.68/4.93 fof(f16284,plain,(
% 35.68/4.93 ![X0]: (c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)=c_HOL_Oinverse__class_Odivide(X0,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex))),
% 35.68/4.93 inference(forward_demodulation,[status(thm)],[f3962,f16258])).
% 35.68/4.93 fof(f16349,plain,(
% 35.68/4.93 ~c_Finite__Set_Osetsum(c_Power_Opower__class_Opower(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),v_n,tc_nat),tc_nat,tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)),
% 35.68/4.93 inference(backward_demodulation,[status(thm)],[f16284,f9802])).
% 35.68/4.93 fof(f17100,plain,(
% 35.68/4.93 ~c_Finite__Set_Osetsum(c_Power_Opower__class_Opower(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_SetInterval_Oord__class_OlessThan(v_n,tc_nat),tc_nat,tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)),
% 35.68/4.98 inference(backward_demodulation,[status(thm)],[f2030,f16349])).
% 35.68/4.98 fof(f17109,plain,(
% 35.68/4.98 ![X0,X1]: (c_Finite__Set_Osetsum(c_Power_Opower__class_Opower(hAPP(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(X0),tc_Complex_Ocomplex),X1),tc_Complex_Ocomplex),c_SetInterval_Oord__class_OlessThan(X0,tc_nat),tc_nat,tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)|~hBOOL(hAPP(c_HOL_Oord__class_Oless(X1,tc_nat),X0))|X1=c_HOL_Ozero__class_Ozero(tc_nat))),
% 35.68/4.98 inference(backward_demodulation,[status(thm)],[f2030,f2739])).
% 35.68/4.98 fof(f17256,plain,(
% 35.68/4.98 c_Finite__Set_Osetsum(c_Power_Opower__class_Opower(hAPP(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),v_k),tc_Complex_Ocomplex),c_SetInterval_Oord__class_OlessThan(v_n,tc_nat),tc_nat,tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)|v_k=c_HOL_Ozero__class_Ozero(tc_nat)),
% 35.68/4.98 inference(resolution,[status(thm)],[f17109,f2033])).
% 35.68/4.98 fof(f17304,plain,(
% 35.68/4.98 c_Finite__Set_Osetsum(c_Power_Opower__class_Opower(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_SetInterval_Oord__class_OlessThan(v_n,tc_nat),tc_nat,tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)|v_k=c_HOL_Ozero__class_Ozero(tc_nat)),
% 35.68/4.98 inference(forward_demodulation,[status(thm)],[f16280,f17256])).
% 35.68/4.98 fof(f17305,plain,(
% 35.68/4.98 v_k=c_HOL_Ozero__class_Ozero(tc_nat)),
% 35.68/4.98 inference(forward_subsumption_resolution,[status(thm)],[f17304,f17100])).
% 35.68/4.98 fof(f17306,plain,(
% 35.68/4.98 $false),
% 35.68/4.98 inference(forward_subsumption_resolution,[status(thm)],[f17305,f8144])).
% 35.68/4.98 % SZS output end CNFRefutation for theBenchmark.p
% 13.25/5.01 % Elapsed time: 4.692702 seconds
% 13.25/5.01 % CPU time: 36.372598 seconds
% 13.25/5.01 % Total memory used: 492.097 MB
% 13.25/5.01 % Net memory used: 471.426 MB
%------------------------------------------------------------------------------