%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV627-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 : n003.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:56 PM UTC 2026
% Result : Unsatisfiable 19.62s 3.08s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWV627-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.20/0.44 % Computer : n003.cluster.edu
% 0.20/0.44 % Model : x86_64 x86_64
% 0.20/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/0.44 % Memory : 8046.5625MB
% 0.20/0.44 % OS : Linux 6.8.0-71-generic
% 0.20/0.44 % CPULimit : 300
% 0.20/0.44 % WCLimit : 300
% 0.20/0.44 % DateTime : Mon Sep 21 09:16:15 UTC 2026
% 0.20/0.44 % CPUTime :
% 0.28/0.54 % Drodi V4.1.1
% 19.62/3.08 % Refutation found
% 19.62/3.08 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 19.62/3.08 % SZS output start CNFRefutation for theBenchmark
% 19.62/3.08 fof(f231,axiom,(
% 19.62/3.08 (![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) ) ))),
% 19.62/3.08 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 19.62/3.08 fof(f399,axiom,(
% 19.62/3.08 (![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 ) ))),
% 19.62/3.08 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 19.62/3.08 fof(f428,axiom,(
% 19.62/3.08 (![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(c_Power_Opower__class_Opower(V_a,V_n,T_a),T_a) = c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Oinverse(V_a,T_a),V_n,T_a) ) ))),
% 19.62/3.08 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 19.62/3.08 fof(f435,axiom,(
% 19.62/3.08 (![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) ) ))),
% 19.62/3.08 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 19.62/3.08 fof(f644,axiom,(
% 19.62/3.08 (![T_a,V_n]: (( ~ class_OrderedGroup_Omonoid__mult(T_a)| c_Power_Opower__class_Opower(c_HOL_Oone__class_Oone(T_a),V_n,T_a) = c_HOL_Oone__class_Oone(T_a) ) ))),
% 19.62/3.08 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 19.62/3.08 fof(f645,axiom,(
% 19.62/3.08 (![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) ) ))),
% 19.62/3.08 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 19.62/3.08 fof(f647,axiom,(
% 19.62/3.08 (![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 ) ))),
% 19.62/3.08 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 19.62/3.08 fof(f652,axiom,(
% 19.62/3.08 (![V_n]: (c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(V_n),V_n,tc_Complex_Ocomplex) = c_HOL_Oone__class_Oone(tc_Complex_Ocomplex) ))),
% 19.62/3.08 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 19.62/3.08 fof(f656,axiom,(
% 19.62/3.08 (![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) ) ))),
% 19.62/3.08 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 19.62/3.08 fof(f670,axiom,(
% 19.62/3.08 (![T_a,V_a]: (( ~ class_Ring__and__Field_Ofield(T_a)| c_HOL_Oinverse__class_Odivide(c_HOL_Ozero__class_Ozero(T_a),V_a,T_a) = c_HOL_Ozero__class_Ozero(T_a) ) ))),
% 19.62/3.08 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 19.62/3.08 fof(f674,negated_conjecture,(
% 19.62/3.08 c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(c_Power_Opower__class_Opower(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),v_n,tc_Complex_Ocomplex),v_k,tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Ominus__class_Ominus(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),v_k,tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
% 19.62/3.08 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 19.62/3.08 fof(f743,axiom,(
% 19.62/3.08 class_Ring__and__Field_Odivision__by__zero(tc_Complex_Ocomplex) ),
% 19.62/3.08 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 19.62/3.08 fof(f748,axiom,(
% 19.62/3.08 class_Ring__and__Field_Odivision__ring(tc_Complex_Ocomplex) ),
% 19.62/3.08 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 19.62/3.08 fof(f750,axiom,(
% 19.62/3.08 class_Ring__and__Field_Ozero__neq__one(tc_Complex_Ocomplex) ),
% 19.62/3.08 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 19.62/3.08 fof(f753,axiom,(
% 19.62/3.08 class_OrderedGroup_Oab__group__add(tc_Complex_Ocomplex) ),
% 19.62/3.08 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 19.62/3.08 fof(f755,axiom,(
% 19.62/3.08 class_OrderedGroup_Omonoid__mult(tc_Complex_Ocomplex) ),
% 19.62/3.08 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 19.62/3.08 fof(f758,axiom,(
% 19.62/3.08 class_Ring__and__Field_Ofield(tc_Complex_Ocomplex) ),
% 19.62/3.08 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 19.62/3.08 fof(f1110,plain,(
% 19.62/3.08 ![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))),
% 19.62/3.08 inference(cnf_transformation,[status(thm)],[f231])).
% 19.62/3.08 fof(f1377,plain,(
% 19.62/3.08 ![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))),
% 19.62/3.08 inference(miniscoping,[status(thm)],[f399])).
% 19.62/3.08 fof(f1378,plain,(
% 19.62/3.08 ![X0,X1]: (~class_OrderedGroup_Omonoid__mult(X0)|c_HOL_Otimes__class_Otimes(X1,c_HOL_Oone__class_Oone(X0),X0)=X1)),
% 19.62/3.08 inference(cnf_transformation,[status(thm)],[f1377])).
% 19.62/3.08 fof(f1434,plain,(
% 19.62/3.08 ![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(c_Power_Opower__class_Opower(V_a,V_n,T_a),T_a)=c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Oinverse(V_a,T_a),V_n,T_a)))),
% 19.62/3.08 inference(miniscoping,[status(thm)],[f428])).
% 19.62/3.08 fof(f1435,plain,(
% 19.62/3.08 ![X0,X1,X2]: (~class_Ring__and__Field_Odivision__ring(X0)|~class_Ring__and__Field_Odivision__by__zero(X0)|c_HOL_Oinverse__class_Oinverse(c_Power_Opower__class_Opower(X1,X2,X0),X0)=c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Oinverse(X1,X0),X2,X0))),
% 19.62/3.08 inference(cnf_transformation,[status(thm)],[f1434])).
% 19.62/3.08 fof(f1448,plain,(
% 19.62/3.08 ![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)))),
% 19.62/3.08 inference(miniscoping,[status(thm)],[f435])).
% 19.62/3.08 fof(f1449,plain,(
% 19.62/3.08 ![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))),
% 19.62/3.08 inference(cnf_transformation,[status(thm)],[f1448])).
% 19.62/3.08 fof(f1775,plain,(
% 19.62/3.08 ![T_a]: (~class_OrderedGroup_Omonoid__mult(T_a)|(![V_n]: c_Power_Opower__class_Opower(c_HOL_Oone__class_Oone(T_a),V_n,T_a)=c_HOL_Oone__class_Oone(T_a)))),
% 19.62/3.08 inference(miniscoping,[status(thm)],[f644])).
% 19.62/3.08 fof(f1776,plain,(
% 19.62/3.08 ![X0,X1]: (~class_OrderedGroup_Omonoid__mult(X0)|c_Power_Opower__class_Opower(c_HOL_Oone__class_Oone(X0),X1,X0)=c_HOL_Oone__class_Oone(X0))),
% 19.62/3.08 inference(cnf_transformation,[status(thm)],[f1775])).
% 19.62/3.08 fof(f1777,plain,(
% 19.62/3.08 ![X0]: (~class_Ring__and__Field_Ozero__neq__one(X0)|~c_HOL_Ozero__class_Ozero(X0)=c_HOL_Oone__class_Oone(X0))),
% 19.62/3.08 inference(cnf_transformation,[status(thm)],[f645])).
% 19.62/3.08 fof(f1779,plain,(
% 19.62/3.08 ![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))),
% 19.62/3.08 inference(miniscoping,[status(thm)],[f647])).
% 19.62/3.08 fof(f1780,plain,(
% 19.62/3.08 ![X0,X1]: (~class_Ring__and__Field_Ofield(X0)|c_HOL_Oinverse__class_Odivide(X1,c_HOL_Oone__class_Oone(X0),X0)=X1)),
% 19.62/3.08 inference(cnf_transformation,[status(thm)],[f1779])).
% 19.62/3.08 fof(f1789,plain,(
% 19.62/3.08 ![X0]: (c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(X0),X0,tc_Complex_Ocomplex)=c_HOL_Oone__class_Oone(tc_Complex_Ocomplex))),
% 19.62/3.08 inference(cnf_transformation,[status(thm)],[f652])).
% 19.62/3.08 fof(f1795,plain,(
% 19.62/3.08 ![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)))),
% 19.62/3.08 inference(miniscoping,[status(thm)],[f656])).
% 19.62/3.08 fof(f1796,plain,(
% 19.62/3.08 ![X0,X1]: (~class_OrderedGroup_Oab__group__add(X0)|c_HOL_Ominus__class_Ominus(X1,X1,X0)=c_HOL_Ozero__class_Ozero(X0))),
% 19.62/3.08 inference(cnf_transformation,[status(thm)],[f1795])).
% 19.62/3.08 fof(f1820,plain,(
% 19.62/3.08 ![T_a]: (~class_Ring__and__Field_Ofield(T_a)|(![V_a]: c_HOL_Oinverse__class_Odivide(c_HOL_Ozero__class_Ozero(T_a),V_a,T_a)=c_HOL_Ozero__class_Ozero(T_a)))),
% 19.62/3.08 inference(miniscoping,[status(thm)],[f670])).
% 19.62/3.08 fof(f1821,plain,(
% 19.62/3.08 ![X0,X1]: (~class_Ring__and__Field_Ofield(X0)|c_HOL_Oinverse__class_Odivide(c_HOL_Ozero__class_Ozero(X0),X1,X0)=c_HOL_Ozero__class_Ozero(X0))),
% 19.62/3.08 inference(cnf_transformation,[status(thm)],[f1820])).
% 19.62/3.08 fof(f1828,plain,(
% 19.62/3.08 ~c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(c_Power_Opower__class_Opower(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),v_n,tc_Complex_Ocomplex),v_k,tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Ominus__class_Ominus(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),v_k,tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)),
% 19.62/3.08 inference(cnf_transformation,[status(thm)],[f674])).
% 19.62/3.08 fof(f1897,plain,(
% 19.62/3.08 class_Ring__and__Field_Odivision__by__zero(tc_Complex_Ocomplex)),
% 19.62/3.08 inference(cnf_transformation,[status(thm)],[f743])).
% 19.62/3.08 fof(f1902,plain,(
% 19.62/3.08 class_Ring__and__Field_Odivision__ring(tc_Complex_Ocomplex)),
% 19.62/3.08 inference(cnf_transformation,[status(thm)],[f748])).
% 19.62/3.08 fof(f1904,plain,(
% 19.62/3.08 class_Ring__and__Field_Ozero__neq__one(tc_Complex_Ocomplex)),
% 19.62/3.08 inference(cnf_transformation,[status(thm)],[f750])).
% 19.62/3.08 fof(f1907,plain,(
% 19.62/3.08 class_OrderedGroup_Oab__group__add(tc_Complex_Ocomplex)),
% 19.62/3.08 inference(cnf_transformation,[status(thm)],[f753])).
% 19.62/3.08 fof(f1909,plain,(
% 19.62/3.08 class_OrderedGroup_Omonoid__mult(tc_Complex_Ocomplex)),
% 19.62/3.08 inference(cnf_transformation,[status(thm)],[f755])).
% 19.62/3.08 fof(f1912,plain,(
% 19.62/3.08 class_Ring__and__Field_Ofield(tc_Complex_Ocomplex)),
% 19.62/3.08 inference(cnf_transformation,[status(thm)],[f758])).
% 19.62/3.08 fof(f2195,plain,(
% 19.62/3.08 ~c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)=c_HOL_Oone__class_Oone(tc_Complex_Ocomplex)),
% 19.62/3.08 inference(resolution,[status(thm)],[f1777,f1904])).
% 19.62/3.08 fof(f2243,plain,(
% 19.62/3.08 ![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))),
% 19.62/3.08 inference(resolution,[status(thm)],[f1110,f1912])).
% 19.62/3.08 fof(f2281,plain,(
% 19.62/3.08 ![X0]: (c_HOL_Otimes__class_Otimes(X0,c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex)=X0)),
% 19.62/3.08 inference(resolution,[status(thm)],[f1378,f1909])).
% 19.62/3.08 fof(f2284,plain,(
% 19.62/3.08 c_HOL_Oone__class_Oone(tc_Complex_Ocomplex)=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_Ozero__class_Ozero(tc_Complex_Ocomplex)),
% 19.62/3.08 inference(paramodulation,[status(thm)],[f2243,f2281])).
% 19.62/3.08 fof(f2321,plain,(
% 19.62/3.08 c_HOL_Oone__class_Oone(tc_Complex_Ocomplex)=c_HOL_Oinverse__class_Oinverse(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex)),
% 19.62/3.08 inference(forward_subsumption_resolution,[status(thm)],[f2284,f2195])).
% 19.62/3.08 fof(f2751,plain,(
% 19.62/3.08 ![X0]: (c_HOL_Oinverse__class_Odivide(X0,c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex)=X0)),
% 19.62/3.08 inference(resolution,[status(thm)],[f1780,f1912])).
% 19.62/3.08 fof(f2766,plain,(
% 19.62/3.08 ![X0]: (c_HOL_Ominus__class_Ominus(X0,X0,tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))),
% 19.62/3.08 inference(resolution,[status(thm)],[f1796,f1907])).
% 19.62/3.08 fof(f6632,plain,(
% 19.62/3.08 ![X0]: (c_Power_Opower__class_Opower(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex)=c_HOL_Oone__class_Oone(tc_Complex_Ocomplex))),
% 19.62/3.08 inference(resolution,[status(thm)],[f1776,f1909])).
% 19.62/3.08 fof(f6735,plain,(
% 19.62/3.08 ![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))),
% 19.62/3.08 inference(resolution,[status(thm)],[f1821,f1912])).
% 19.62/3.08 fof(f6742,plain,(
% 19.62/3.08 ![X0,X1]: (~class_Ring__and__Field_Odivision__by__zero(tc_Complex_Ocomplex)|c_HOL_Oinverse__class_Oinverse(c_Power_Opower__class_Opower(X0,X1,tc_Complex_Ocomplex),tc_Complex_Ocomplex)=c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Oinverse(X0,tc_Complex_Ocomplex),X1,tc_Complex_Ocomplex))),
% 19.62/3.08 inference(resolution,[status(thm)],[f1435,f1902])).
% 19.62/3.08 fof(f6743,plain,(
% 19.62/3.08 ![X0,X1]: (c_HOL_Oinverse__class_Oinverse(c_Power_Opower__class_Opower(X0,X1,tc_Complex_Ocomplex),tc_Complex_Ocomplex)=c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Oinverse(X0,tc_Complex_Ocomplex),X1,tc_Complex_Ocomplex))),
% 19.62/3.08 inference(forward_subsumption_resolution,[status(thm)],[f6742,f1897])).
% 19.62/3.08 fof(f6760,plain,(
% 19.62/3.08 ![X0]: (c_HOL_Oinverse__class_Oinverse(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex)=c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Oinverse(c_FFT__Mirabelle_Oroot(X0),tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex))),
% 19.62/3.08 inference(paramodulation,[status(thm)],[f1789,f6743])).
% 19.62/3.08 fof(f6797,plain,(
% 19.62/3.08 ![X0]: (c_HOL_Oone__class_Oone(tc_Complex_Ocomplex)=c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Oinverse(c_FFT__Mirabelle_Oroot(X0),tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex))),
% 19.62/3.08 inference(forward_demodulation,[status(thm)],[f2321,f6760])).
% 19.62/3.08 fof(f7120,plain,(
% 19.62/3.08 ![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))),
% 19.62/3.08 inference(resolution,[status(thm)],[f1449,f1912])).
% 19.62/3.08 fof(f7121,plain,(
% 19.62/3.08 ![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))),
% 19.62/3.08 inference(forward_subsumption_resolution,[status(thm)],[f7120,f1897])).
% 19.62/3.08 fof(f7177,plain,(
% 19.62/3.08 ![X0]: (c_HOL_Oinverse__class_Oinverse(X0,tc_Complex_Ocomplex)=c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex))),
% 19.62/3.08 inference(paramodulation,[status(thm)],[f2751,f7121])).
% 19.62/3.08 fof(f7716,plain,(
% 19.62/3.08 ~c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(c_Power_Opower__class_Opower(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),v_n,tc_Complex_Ocomplex),v_k,tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Ominus__class_Ominus(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Oinverse(c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),v_k,tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)),
% 19.62/3.08 inference(backward_demodulation,[status(thm)],[f7177,f1828])).
% 19.62/3.08 fof(f7731,plain,(
% 19.62/3.08 ~c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(c_Power_Opower__class_Opower(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Oinverse(c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),v_n,tc_Complex_Ocomplex),v_k,tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Ominus__class_Ominus(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Oinverse(c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),v_k,tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)),
% 19.62/3.08 inference(forward_demodulation,[status(thm)],[f7177,f7716])).
% 19.62/3.08 fof(f7732,plain,(
% 19.62/3.08 ~c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(c_Power_Opower__class_Opower(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),v_k,tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Ominus__class_Ominus(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Oinverse(c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),v_k,tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)),
% 19.62/3.08 inference(forward_demodulation,[status(thm)],[f6797,f7731])).
% 19.62/3.08 fof(f9326,plain,(
% 19.62/3.08 ~c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Ominus__class_Ominus(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Oinverse(c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),v_k,tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)),
% 19.62/3.12 inference(backward_demodulation,[status(thm)],[f6632,f7732])).
% 19.62/3.12 fof(f9329,plain,(
% 19.62/3.12 ~c_HOL_Oinverse__class_Odivide(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),c_HOL_Ominus__class_Ominus(c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Oinverse(c_FFT__Mirabelle_Oroot(v_n),tc_Complex_Ocomplex),v_k,tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)),
% 19.62/3.12 inference(forward_demodulation,[status(thm)],[f2766,f9326])).
% 19.62/3.12 fof(f9330,plain,(
% 19.62/3.12 ~c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)),
% 19.62/3.12 inference(forward_demodulation,[status(thm)],[f6735,f9329])).
% 19.62/3.12 fof(f9331,plain,(
% 19.62/3.12 $false),
% 19.62/3.12 inference(trivial_equality_resolution,[status(thm)],[f9330])).
% 19.62/3.12 % SZS output end CNFRefutation for theBenchmark.p
% 5.29/3.15 % Elapsed time: 2.682478 seconds
% 5.29/3.15 % CPU time: 20.280970 seconds
% 5.29/3.15 % Total memory used: 325.238 MB
% 5.29/3.15 % Net memory used: 316.281 MB
%------------------------------------------------------------------------------