%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV617-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 : n008.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 0.15s 5.83s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV617-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/5.39 % Computer : n008.cluster.edu
% 0.10/5.39 % Model : x86_64 x86_64
% 0.10/5.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.39 % Memory : 8046.5625MB
% 0.10/5.39 % OS : Linux 6.8.0-71-generic
% 0.10/5.39 % CPULimit : 300
% 0.10/5.39 % WCLimit : 300
% 0.10/5.39 % DateTime : Mon Sep 21 09:15:15 UTC 2026
% 0.10/5.39 % CPUTime :
% 0.15/5.49 % Drodi V4.1.1
% 0.15/5.83 % Refutation found
% 0.15/5.83 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.15/5.83 % SZS output start CNFRefutation for theBenchmark
% 0.15/5.83 fof(f644,axiom,(
% 0.15/5.83 (![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) ) ))),
% 0.15/5.83 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.83 fof(f652,axiom,(
% 0.15/5.83 (![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) ))),
% 0.15/5.83 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.83 fof(f656,axiom,(
% 0.15/5.83 (![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) ) ))),
% 0.15/5.83 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.83 fof(f670,axiom,(
% 0.15/5.83 (![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) ) ))),
% 0.15/5.83 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.83 fof(f674,negated_conjecture,(
% 0.15/5.83 c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(c_Power_Opower__class_Opower(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(v_n),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_FFT__Mirabelle_Oroot(v_n),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) ),
% 0.15/5.83 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.83 fof(f753,axiom,(
% 0.15/5.83 class_OrderedGroup_Oab__group__add(tc_Complex_Ocomplex) ),
% 0.15/5.83 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.83 fof(f755,axiom,(
% 0.15/5.83 class_OrderedGroup_Omonoid__mult(tc_Complex_Ocomplex) ),
% 0.15/5.83 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.83 fof(f758,axiom,(
% 0.15/5.83 class_Ring__and__Field_Ofield(tc_Complex_Ocomplex) ),
% 0.15/5.83 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.83 fof(f1775,plain,(
% 0.15/5.83 ![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)))),
% 0.15/5.83 inference(miniscoping,[status(thm)],[f644])).
% 0.15/5.83 fof(f1776,plain,(
% 0.15/5.83 ![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))),
% 0.15/5.83 inference(cnf_transformation,[status(thm)],[f1775])).
% 0.15/5.83 fof(f1789,plain,(
% 0.15/5.83 ![X0]: (c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(X0),X0,tc_Complex_Ocomplex)=c_HOL_Oone__class_Oone(tc_Complex_Ocomplex))),
% 0.15/5.83 inference(cnf_transformation,[status(thm)],[f652])).
% 0.15/5.83 fof(f1795,plain,(
% 0.15/5.83 ![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)))),
% 0.15/5.83 inference(miniscoping,[status(thm)],[f656])).
% 0.15/5.83 fof(f1796,plain,(
% 0.15/5.83 ![X0,X1]: (~class_OrderedGroup_Oab__group__add(X0)|c_HOL_Ominus__class_Ominus(X1,X1,X0)=c_HOL_Ozero__class_Ozero(X0))),
% 0.15/5.83 inference(cnf_transformation,[status(thm)],[f1795])).
% 0.15/5.83 fof(f1820,plain,(
% 0.15/5.83 ![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)))),
% 0.15/5.83 inference(miniscoping,[status(thm)],[f670])).
% 0.15/5.83 fof(f1821,plain,(
% 0.15/5.83 ![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))),
% 0.15/5.83 inference(cnf_transformation,[status(thm)],[f1820])).
% 0.15/5.83 fof(f1828,plain,(
% 0.15/5.83 ~c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(c_Power_Opower__class_Opower(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(v_n),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_FFT__Mirabelle_Oroot(v_n),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)),
% 0.15/5.86 inference(cnf_transformation,[status(thm)],[f674])).
% 0.15/5.86 fof(f1907,plain,(
% 0.15/5.86 class_OrderedGroup_Oab__group__add(tc_Complex_Ocomplex)),
% 0.15/5.86 inference(cnf_transformation,[status(thm)],[f753])).
% 0.15/5.86 fof(f1909,plain,(
% 0.15/5.86 class_OrderedGroup_Omonoid__mult(tc_Complex_Ocomplex)),
% 0.15/5.86 inference(cnf_transformation,[status(thm)],[f755])).
% 0.15/5.86 fof(f1912,plain,(
% 0.15/5.86 class_Ring__and__Field_Ofield(tc_Complex_Ocomplex)),
% 0.15/5.86 inference(cnf_transformation,[status(thm)],[f758])).
% 0.15/5.86 fof(f1921,plain,(
% 0.15/5.86 ~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_FFT__Mirabelle_Oroot(v_n),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)),
% 0.15/5.86 inference(backward_demodulation,[status(thm)],[f1789,f1828])).
% 0.15/5.86 fof(f2416,plain,(
% 0.15/5.86 ![X0]: (c_HOL_Ominus__class_Ominus(X0,X0,tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))),
% 0.15/5.86 inference(resolution,[status(thm)],[f1796,f1907])).
% 0.15/5.86 fof(f4346,plain,(
% 0.15/5.86 ![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))),
% 0.15/5.86 inference(resolution,[status(thm)],[f1776,f1909])).
% 0.15/5.86 fof(f4397,plain,(
% 0.15/5.86 ![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))),
% 0.15/5.86 inference(resolution,[status(thm)],[f1821,f1912])).
% 0.15/5.86 fof(f5404,plain,(
% 0.15/5.86 ~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_FFT__Mirabelle_Oroot(v_n),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)),
% 0.15/5.86 inference(backward_demodulation,[status(thm)],[f4346,f1921])).
% 0.15/5.86 fof(f5405,plain,(
% 0.15/5.86 ~c_HOL_Oinverse__class_Odivide(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),c_HOL_Ominus__class_Ominus(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(v_n),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)),
% 0.15/5.86 inference(forward_demodulation,[status(thm)],[f2416,f5404])).
% 0.15/5.86 fof(f5406,plain,(
% 0.15/5.86 ~c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)),
% 0.15/5.86 inference(forward_demodulation,[status(thm)],[f4397,f5405])).
% 0.15/5.86 fof(f5407,plain,(
% 0.15/5.86 $false),
% 0.15/5.86 inference(trivial_equality_resolution,[status(thm)],[f5406])).
% 0.15/5.86 % SZS output end CNFRefutation for theBenchmark.p
% 0.15/5.90 % Elapsed time: 0.484325 seconds
% 0.15/5.90 % CPU time: 2.729492 seconds
% 0.15/5.90 % Total memory used: 165.395 MB
% 0.15/5.90 % Net memory used: 163.582 MB
%------------------------------------------------------------------------------