%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : ALG368-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 : n002.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:05 AM UTC 2026
% Result : Unsatisfiable 21.14s 3.31s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : ALG368-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.44 % Computer : n002.cluster.edu
% 0.18/0.44 % Model : x86_64 x86_64
% 0.18/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.44 % Memory : 8046.5625MB
% 0.18/0.44 % OS : Linux 6.8.0-71-generic
% 0.18/0.44 % CPULimit : 300
% 0.18/0.44 % WCLimit : 300
% 0.18/0.44 % DateTime : Mon Sep 21 13:20:32 UTC 2026
% 0.18/0.44 % CPUTime :
% 0.27/0.55 % Drodi V4.1.1
% 21.14/3.31 % Refutation found
% 21.14/3.31 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 21.14/3.31 % SZS output start CNFRefutation for theBenchmark
% 21.14/3.31 fof(f801,axiom,(
% 21.14/3.31 (![V_x]: (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Transcendental_Oexp(V_x,tc_RealDef_Oreal),tc_RealDef_Oreal) ))),
% 21.14/3.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 21.14/3.31 fof(f821,axiom,(
% 21.14/3.31 (![T_a]: (( ~ class_RealVector_Oreal__normed__vector(T_a)| c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(T_a),T_a) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ) ))),
% 21.14/3.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 21.14/3.31 fof(f822,axiom,(
% 21.14/3.31 (![T_a,V_x]: (( ~ class_Ring__and__Field_Ocomm__semiring__0(T_a)| c_Polynomial_Opoly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)),V_x,T_a) = c_HOL_Ozero__class_Ozero(T_a) ) ))),
% 21.14/3.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 21.14/3.31 fof(f824,axiom,(
% 21.14/3.31 c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_e,tc_RealDef_Oreal) ),
% 21.14/3.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 21.14/3.31 fof(f834,axiom,(
% 21.14/3.31 (![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) ) ))),
% 21.14/3.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 21.14/3.31 fof(f852,negated_conjecture,(
% 21.14/3.31 (![V_xa]: (( ~ c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(c_HOL_Ominus__class_Ominus(c_Polynomial_Opoly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),c_HOL_Ominus__class_Ominus(hAPP(v_x,V_xa),v_z,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_Polynomial_Opoly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),c_HOL_Ominus__class_Ominus(v_z,v_z,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_e,tc_RealDef_Oreal)| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_xa,tc_RealDef_Oreal) ) ))),
% 21.14/3.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 21.14/3.31 fof(f967,axiom,(
% 21.14/3.31 class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex) ),
% 21.14/3.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 21.14/3.31 fof(f970,axiom,(
% 21.14/3.31 class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex) ),
% 21.14/3.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 21.14/3.31 fof(f978,axiom,(
% 21.14/3.31 class_OrderedGroup_Oab__group__add(tc_Complex_Ocomplex) ),
% 21.14/3.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 21.14/3.31 fof(f2335,plain,(
% 21.14/3.31 ![X0]: (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Transcendental_Oexp(X0,tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 21.14/3.31 inference(cnf_transformation,[status(thm)],[f801])).
% 21.14/3.31 fof(f2362,plain,(
% 21.14/3.31 ![X0]: (~class_RealVector_Oreal__normed__vector(X0)|c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(X0),X0)=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal))),
% 21.14/3.31 inference(cnf_transformation,[status(thm)],[f821])).
% 21.14/3.31 fof(f2363,plain,(
% 21.14/3.31 ![T_a]: (~class_Ring__and__Field_Ocomm__semiring__0(T_a)|(![V_x]: c_Polynomial_Opoly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)),V_x,T_a)=c_HOL_Ozero__class_Ozero(T_a)))),
% 21.14/3.31 inference(miniscoping,[status(thm)],[f822])).
% 21.14/3.31 fof(f2364,plain,(
% 21.14/3.31 ![X0,X1]: (~class_Ring__and__Field_Ocomm__semiring__0(X0)|c_Polynomial_Opoly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)),X1,X0)=c_HOL_Ozero__class_Ozero(X0))),
% 21.14/3.31 inference(cnf_transformation,[status(thm)],[f2363])).
% 21.14/3.31 fof(f2367,plain,(
% 21.14/3.31 c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_e,tc_RealDef_Oreal)),
% 21.14/3.31 inference(cnf_transformation,[status(thm)],[f824])).
% 21.14/3.31 fof(f2381,plain,(
% 21.14/3.31 ![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)))),
% 21.14/3.31 inference(miniscoping,[status(thm)],[f834])).
% 21.14/3.31 fof(f2382,plain,(
% 21.14/3.31 ![X0,X1]: (~class_OrderedGroup_Oab__group__add(X0)|c_HOL_Ominus__class_Ominus(X1,X1,X0)=c_HOL_Ozero__class_Ozero(X0))),
% 21.14/3.31 inference(cnf_transformation,[status(thm)],[f2381])).
% 21.14/3.31 fof(f2413,plain,(
% 21.14/3.31 ![X0]: (~c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(c_HOL_Ominus__class_Ominus(c_Polynomial_Opoly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),c_HOL_Ominus__class_Ominus(hAPP(v_x,X0),v_z,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_Polynomial_Opoly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),c_HOL_Ominus__class_Ominus(v_z,v_z,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_e,tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal))),
% 21.14/3.31 inference(cnf_transformation,[status(thm)],[f852])).
% 21.14/3.31 fof(f2528,plain,(
% 21.14/3.31 class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex)),
% 21.14/3.31 inference(cnf_transformation,[status(thm)],[f967])).
% 21.14/3.31 fof(f2531,plain,(
% 21.14/3.31 class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex)),
% 21.14/3.31 inference(cnf_transformation,[status(thm)],[f970])).
% 21.14/3.31 fof(f2539,plain,(
% 21.14/3.31 class_OrderedGroup_Oab__group__add(tc_Complex_Ocomplex)),
% 21.14/3.31 inference(cnf_transformation,[status(thm)],[f978])).
% 21.14/3.31 fof(f2623,plain,(
% 21.14/3.31 ![X0]: (c_Polynomial_Opoly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),X0,tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))),
% 21.14/3.31 inference(resolution,[status(thm)],[f2528,f2364])).
% 21.14/3.31 fof(f2630,plain,(
% 21.14/3.31 ![X0]: (~c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(c_HOL_Ominus__class_Ominus(c_Polynomial_Opoly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),c_HOL_Ominus__class_Ominus(hAPP(v_x,X0),v_z,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_e,tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal))),
% 21.14/3.31 inference(backward_demodulation,[status(thm)],[f2623,f2413])).
% 21.14/3.31 fof(f2631,plain,(
% 21.14/3.31 ![X0]: (~c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(c_HOL_Ominus__class_Ominus(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_e,tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal))),
% 21.14/3.31 inference(forward_demodulation,[status(thm)],[f2623,f2630])).
% 21.14/3.31 fof(f5181,plain,(
% 21.14/3.31 ![X0]: (c_HOL_Ominus__class_Ominus(X0,X0,tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))),
% 21.14/3.31 inference(resolution,[status(thm)],[f2539,f2382])).
% 21.14/3.31 fof(f5182,plain,(
% 21.14/3.31 ![X0]: (~c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_e,tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal))),
% 21.14/3.31 inference(backward_demodulation,[status(thm)],[f5181,f2631])).
% 21.14/3.31 fof(f5183,definition,(
% 21.14/3.31 sQ17_spl <=> (c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_e,tc_RealDef_Oreal))),
% 21.14/3.31 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 21.14/3.31 fof(f5185,plain,(
% 21.14/3.31 ~c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_e,tc_RealDef_Oreal)|sQ17_spl),
% 21.14/3.31 inference(component_clause,[status(thm)],[f5183])).
% 21.14/3.31 fof(f5186,definition,(
% 21.14/3.31 ![X0]: (sQ18_spl <=> (~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)))),
% 21.14/3.31 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 21.14/3.31 fof(f5187,plain,(
% 21.14/3.31 ![X0]: (~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)|~sQ18_spl)),
% 21.14/3.31 inference(component_clause,[status(thm)],[f5186])).
% 21.14/3.31 fof(f5189,plain,(
% 21.14/3.31 ~sQ17_spl|sQ18_spl),
% 21.14/3.31 inference(split_clause,[status(thm)],[f5182,f5183,f5186])).
% 21.14/3.31 fof(f13905,plain,(
% 21.14/3.31 c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex)=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)),
% 21.14/3.31 inference(resolution,[status(thm)],[f2362,f2531])).
% 21.14/3.31 fof(f13919,plain,(
% 21.14/3.31 ~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_e,tc_RealDef_Oreal)|sQ17_spl),
% 21.14/3.31 inference(backward_demodulation,[status(thm)],[f13905,f5185])).
% 21.14/3.31 fof(f14015,plain,(
% 21.14/3.31 $false|sQ17_spl),
% 21.14/3.31 inference(forward_subsumption_resolution,[status(thm)],[f13919,f2367])).
% 21.15/3.35 fof(f14016,plain,(
% 21.15/3.35 sQ17_spl),
% 21.15/3.35 inference(contradiction_clause,[status(thm)],[f14015])).
% 21.15/3.35 fof(f14179,plain,(
% 21.15/3.35 $false|~sQ18_spl),
% 21.15/3.35 inference(backward_subsumption_resolution,[status(thm)],[f2335,f5187])).
% 21.15/3.35 fof(f14193,plain,(
% 21.15/3.35 ~sQ18_spl),
% 21.15/3.35 inference(contradiction_clause,[status(thm)],[f14179])).
% 21.15/3.35 fof(f14194,plain,(
% 21.15/3.35 $false),
% 21.15/3.35 inference(sat_refutation,[status(thm)],[f5189,f14016,f14193])).
% 21.15/3.35 % SZS output end CNFRefutation for theBenchmark.p
% 13.90/3.42 % Elapsed time: 2.962613 seconds
% 13.90/3.42 % CPU time: 22.365488 seconds
% 13.90/3.42 % Total memory used: 492.868 MB
% 13.90/3.42 % Net memory used: 484.993 MB
%------------------------------------------------------------------------------