%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : ALG402-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 11:50:08 AM UTC 2026
% Result : Unsatisfiable 2.01s 1.36s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : ALG402-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.16/0.43 % Computer : n008.cluster.edu
% 0.16/0.43 % Model : x86_64 x86_64
% 0.16/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.43 % Memory : 8046.5625MB
% 0.16/0.43 % OS : Linux 6.8.0-71-generic
% 0.16/0.43 % CPULimit : 300
% 0.16/0.43 % WCLimit : 300
% 0.16/0.43 % DateTime : Mon Sep 21 13:20:08 UTC 2026
% 0.16/0.43 % CPUTime :
% 0.27/0.55 % Drodi V4.1.1
% 2.01/1.36 % Refutation found
% 2.01/1.36 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 2.01/1.36 % SZS output start CNFRefutation for theBenchmark
% 2.01/1.36 fof(f77,axiom,(
% 2.01/1.36 (![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) ) ))),
% 2.01/1.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.01/1.36 fof(f288,axiom,(
% 2.01/1.36 (![T_a,V_a]: (( ~ class_OrderedGroup_Omonoid__mult(T_a)| c_HOL_Otimes__class_Otimes(c_HOL_Oone__class_Oone(T_a),V_a,T_a) = V_a ) ))),
% 2.01/1.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.01/1.36 fof(f447,axiom,(
% 2.01/1.36 (![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) ) ))),
% 2.01/1.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.01/1.36 fof(f716,axiom,(
% 2.01/1.36 c_HOL_Oone__class_Oone(tc_nat) = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) ),
% 2.01/1.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.01/1.36 fof(f866,axiom,(
% 2.01/1.36 (![T_a,V_x]: (( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a)| c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(T_a),V_x,T_a) = c_HOL_Ozero__class_Ozero(T_a) ) ))),
% 2.01/1.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.01/1.37 fof(f931,negated_conjecture,(
% 2.01/1.37 (![V_x,V_xa]: (c_HOL_Otimes__class_Otimes(V_x,c_Power_Opower__class_Opower(V_x,c_HOL_Ominus__class_Ominus(v_k____,c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat),tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(V_xa,c_Power_Opower__class_Opower(V_xa,c_HOL_Ominus__class_Ominus(v_k____,c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat),tc_Complex_Ocomplex),tc_Complex_Ocomplex) ))),
% 2.01/1.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.01/1.37 fof(f1019,axiom,(
% 2.01/1.37 class_Ring__and__Field_Ocomm__semiring__1(tc_Complex_Ocomplex) ),
% 2.01/1.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.01/1.37 fof(f1028,axiom,(
% 2.01/1.37 class_Ring__and__Field_Ozero__neq__one(tc_Complex_Ocomplex) ),
% 2.01/1.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.01/1.37 fof(f1034,axiom,(
% 2.01/1.37 class_OrderedGroup_Omonoid__mult(tc_Complex_Ocomplex) ),
% 2.01/1.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.01/1.37 fof(f1160,plain,(
% 2.01/1.37 ![X0]: (~class_Ring__and__Field_Ozero__neq__one(X0)|~c_HOL_Ozero__class_Ozero(X0)=c_HOL_Oone__class_Oone(X0))),
% 2.01/1.37 inference(cnf_transformation,[status(thm)],[f77])).
% 2.01/1.37 fof(f1492,plain,(
% 2.01/1.37 ![T_a]: (~class_OrderedGroup_Omonoid__mult(T_a)|(![V_a]: c_HOL_Otimes__class_Otimes(c_HOL_Oone__class_Oone(T_a),V_a,T_a)=V_a))),
% 2.01/1.37 inference(miniscoping,[status(thm)],[f288])).
% 2.01/1.37 fof(f1493,plain,(
% 2.01/1.37 ![X0,X1]: (~class_OrderedGroup_Omonoid__mult(X0)|c_HOL_Otimes__class_Otimes(c_HOL_Oone__class_Oone(X0),X1,X0)=X1)),
% 2.01/1.37 inference(cnf_transformation,[status(thm)],[f1492])).
% 2.01/1.37 fof(f1751,plain,(
% 2.01/1.37 ![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)))),
% 2.01/1.37 inference(miniscoping,[status(thm)],[f447])).
% 2.01/1.37 fof(f1752,plain,(
% 2.01/1.37 ![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))),
% 2.01/1.37 inference(cnf_transformation,[status(thm)],[f1751])).
% 2.01/1.37 fof(f2173,plain,(
% 2.01/1.37 c_HOL_Oone__class_Oone(tc_nat)=c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))),
% 2.01/1.37 inference(cnf_transformation,[status(thm)],[f716])).
% 2.01/1.37 fof(f2403,plain,(
% 2.01/1.37 ![T_a]: (~class_Ring__and__Field_Ocomm__semiring__1(T_a)|(![V_x]: c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(T_a),V_x,T_a)=c_HOL_Ozero__class_Ozero(T_a)))),
% 2.01/1.37 inference(miniscoping,[status(thm)],[f866])).
% 2.01/1.37 fof(f2404,plain,(
% 2.01/1.37 ![X0,X1]: (~class_Ring__and__Field_Ocomm__semiring__1(X0)|c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(X0),X1,X0)=c_HOL_Ozero__class_Ozero(X0))),
% 2.01/1.37 inference(cnf_transformation,[status(thm)],[f2403])).
% 2.01/1.37 fof(f2518,plain,(
% 2.01/1.37 ![X0,X1]: (c_HOL_Otimes__class_Otimes(X0,c_Power_Opower__class_Opower(X0,c_HOL_Ominus__class_Ominus(v_k____,c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat),tc_Complex_Ocomplex),tc_Complex_Ocomplex)=c_HOL_Otimes__class_Otimes(X1,c_Power_Opower__class_Opower(X1,c_HOL_Ominus__class_Ominus(v_k____,c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat),tc_Complex_Ocomplex),tc_Complex_Ocomplex))),
% 2.01/1.37 inference(cnf_transformation,[status(thm)],[f931])).
% 2.01/1.37 fof(f2606,plain,(
% 2.01/1.37 class_Ring__and__Field_Ocomm__semiring__1(tc_Complex_Ocomplex)),
% 2.01/1.37 inference(cnf_transformation,[status(thm)],[f1019])).
% 2.01/1.37 fof(f2615,plain,(
% 2.01/1.37 class_Ring__and__Field_Ozero__neq__one(tc_Complex_Ocomplex)),
% 2.01/1.37 inference(cnf_transformation,[status(thm)],[f1028])).
% 2.01/1.37 fof(f2621,plain,(
% 2.01/1.37 class_OrderedGroup_Omonoid__mult(tc_Complex_Ocomplex)),
% 2.01/1.37 inference(cnf_transformation,[status(thm)],[f1034])).
% 2.01/1.37 fof(f4293,plain,(
% 2.01/1.37 ![X0,X1]: (c_HOL_Otimes__class_Otimes(X0,c_Power_Opower__class_Opower(X0,c_HOL_Ominus__class_Ominus(v_k____,c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat),tc_Complex_Ocomplex),tc_Complex_Ocomplex)=c_HOL_Otimes__class_Otimes(X1,c_Power_Opower__class_Opower(X1,c_HOL_Ominus__class_Ominus(v_k____,c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_Complex_Ocomplex),tc_Complex_Ocomplex))),
% 2.01/1.37 inference(backward_demodulation,[status(thm)],[f2173,f2518])).
% 2.01/1.37 fof(f4344,plain,(
% 2.01/1.37 ![X0,X1]: (c_HOL_Otimes__class_Otimes(X0,c_Power_Opower__class_Opower(X0,c_HOL_Ominus__class_Ominus(v_k____,c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_Complex_Ocomplex),tc_Complex_Ocomplex)=c_HOL_Otimes__class_Otimes(X1,c_Power_Opower__class_Opower(X1,c_HOL_Ominus__class_Ominus(v_k____,c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_Complex_Ocomplex),tc_Complex_Ocomplex))),
% 2.01/1.37 inference(forward_demodulation,[status(thm)],[f2173,f4293])).
% 2.01/1.37 fof(f4862,plain,(
% 2.01/1.37 ![X0]: (c_HOL_Otimes__class_Otimes(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex)=X0)),
% 2.01/1.37 inference(resolution,[status(thm)],[f1493,f2621])).
% 2.01/1.37 fof(f4866,plain,(
% 2.01/1.37 ![X0]: (c_HOL_Otimes__class_Otimes(X0,c_Power_Opower__class_Opower(X0,c_HOL_Ominus__class_Ominus(v_k____,c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_Complex_Ocomplex),tc_Complex_Ocomplex)=c_Power_Opower__class_Opower(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_HOL_Ominus__class_Ominus(v_k____,c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_Complex_Ocomplex))),
% 2.01/1.37 inference(paramodulation,[status(thm)],[f4344,f4862])).
% 2.01/1.37 fof(f5396,definition,(
% 2.01/1.37 sQ94_spl <=> (c_HOL_Oone__class_Oone(tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))),
% 2.01/1.37 introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition])).
% 2.01/1.37 fof(f5397,plain,(
% 2.01/1.37 c_HOL_Oone__class_Oone(tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)|~sQ94_spl),
% 2.01/1.37 inference(component_clause,[status(thm)],[f5396])).
% 2.01/1.37 fof(f5398,plain,(
% 2.01/1.37 ~c_HOL_Oone__class_Oone(tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)|sQ94_spl),
% 2.01/1.37 inference(component_clause,[status(thm)],[f5396])).
% 2.01/1.37 fof(f6875,plain,(
% 2.01/1.37 ~class_Ring__and__Field_Ozero__neq__one(tc_Complex_Ocomplex)|~sQ94_spl),
% 2.01/1.37 inference(resolution,[status(thm)],[f5397,f1160])).
% 2.01/1.37 fof(f6891,plain,(
% 2.01/1.37 $false|~sQ94_spl),
% 2.01/1.37 inference(forward_subsumption_resolution,[status(thm)],[f6875,f2615])).
% 2.01/1.37 fof(f6892,plain,(
% 2.01/1.37 ~sQ94_spl),
% 2.01/1.37 inference(contradiction_clause,[status(thm)],[f6891])).
% 2.01/1.37 fof(f7047,plain,(
% 2.01/1.37 ![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))),
% 2.01/1.37 inference(resolution,[status(thm)],[f1752,f2621])).
% 2.01/1.37 fof(f7880,plain,(
% 2.01/1.37 ![X0]: (c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))),
% 2.01/1.37 inference(resolution,[status(thm)],[f2404,f2606])).
% 2.01/1.37 fof(f8127,plain,(
% 2.01/1.37 c_Power_Opower__class_Opower(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_HOL_Ominus__class_Ominus(v_k____,c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)),
% 2.01/1.37 inference(paramodulation,[status(thm)],[f4866,f7880])).
% 2.01/1.37 fof(f9886,plain,(
% 2.01/1.37 c_HOL_Oone__class_Oone(tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)),
% 2.01/1.37 inference(backward_demodulation,[status(thm)],[f7047,f8127])).
% 2.01/1.37 fof(f9890,plain,(
% 2.01/1.37 $false|sQ94_spl),
% 2.01/1.37 inference(forward_subsumption_resolution,[status(thm)],[f9886,f5398])).
% 2.01/1.37 fof(f9891,plain,(
% 2.01/1.37 sQ94_spl),
% 2.01/1.37 inference(contradiction_clause,[status(thm)],[f9890])).
% 2.01/1.39 fof(f9892,plain,(
% 2.01/1.39 $false),
% 2.01/1.39 inference(sat_refutation,[status(thm)],[f6892,f9891])).
% 2.01/1.39 % SZS output end CNFRefutation for theBenchmark.p
% 2.01/1.41 % Elapsed time: 0.956169 seconds
% 2.01/1.41 % CPU time: 6.539233 seconds
% 2.01/1.41 % Total memory used: 211.141 MB
% 2.01/1.41 % Net memory used: 205.635 MB
%------------------------------------------------------------------------------