%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : ALG368-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n006.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:49:16 AM UTC 2026
% Result : Unsatisfiable 27.76s 4.19s
% Output : CNFRefutation 26.92s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 25
% Syntax : Number of formulae : 95 ( 39 unt; 4 def)
% Number of atoms : 164 ( 33 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 142 ( 73 ~; 65 |; 0 &)
% ( 4 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 15 ( 13 usr; 5 prp; 0-3 aty)
% Number of functors : 16 ( 16 usr; 6 con; 0-3 aty)
% Number of variables : 101 ( 101 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f18,axiom,
! [T_a,V_a,V_b,V_c] :
( ~ c_lessequals(c_HOL_Oplus__class_Oplus(V_a,V_c,T_a),c_HOL_Oplus__class_Oplus(V_b,V_c,T_a),T_a)
| c_lessequals(V_a,V_b,T_a)
| ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f194,axiom,
! [T_a,V_a] :
( c_HOL_Oplus__class_Oplus(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) = V_a
| ~ class_OrderedGroup_Omonoid__add(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f195,axiom,
! [T_a,V_a] :
( c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(T_a),V_a,T_a) = V_a
| ~ class_OrderedGroup_Omonoid__add(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f320,axiom,
! [V_x,V_y] :
( ~ c_lessequals(c_HOL_Ominus__class_Ominus(V_x,V_y,tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_lessequals(V_x,V_y,tc_RealDef_Oreal) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f325,axiom,
c_Transcendental_Osin(c_Transcendental_Opi) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f326,axiom,
c_Transcendental_Otan(c_Transcendental_Opi) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f526,axiom,
! [V_x] : ~ c_lessequals(c_Transcendental_Oexp(V_x,tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f562,axiom,
! [T_a,V_x,V_y] :
( c_lessequals(V_y,V_x,T_a)
| c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f821,axiom,
! [T_a] :
( c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(T_a),T_a) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)
| ~ class_RealVector_Oreal__normed__vector(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f822,axiom,
! [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)
| ~ class_Ring__and__Field_Ocomm__semiring__0(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f824,axiom,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_e,tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f834,axiom,
! [T_a,V_x] :
( c_HOL_Ominus__class_Ominus(V_x,V_x,T_a) = c_HOL_Ozero__class_Ozero(T_a)
| ~ class_OrderedGroup_Oab__group__add(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f836,axiom,
! [T_a,V_a] :
( c_HOL_Ominus__class_Ominus(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) = V_a
| ~ class_OrderedGroup_Ogroup__add(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f852,negated_conjecture,
! [V_xa] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_xa,tc_RealDef_Oreal)
| ~ 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) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f893,axiom,
class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f941,axiom,
class_OrderedGroup_Omonoid__add(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f943,axiom,
class_OrderedGroup_Ogroup__add(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f952,axiom,
class_Orderings_Olinorder(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f967,axiom,
class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f970,axiom,
class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f978,axiom,
class_OrderedGroup_Oab__group__add(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1075,plain,
! [T_a,V_a,V_b] :
( ! [V_c] : ~ c_lessequals(c_HOL_Oplus__class_Oplus(V_a,V_c,T_a),c_HOL_Oplus__class_Oplus(V_b,V_c,T_a),T_a)
| c_lessequals(V_a,V_b,T_a)
| ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(T_a) ),
inference(miniscoping,[status(thm)],[f18]) ).
fof(f1076,plain,
! [X0,X1,X2,X3] :
( ~ c_lessequals(c_HOL_Oplus__class_Oplus(X1,X3,X0),c_HOL_Oplus__class_Oplus(X2,X3,X0),X0)
| c_lessequals(X1,X2,X0)
| ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(X0) ),
inference(cnf_transformation,[status(thm)],[f1075]) ).
fof(f1372,plain,
! [T_a] :
( ! [V_a] : c_HOL_Oplus__class_Oplus(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) = V_a
| ~ class_OrderedGroup_Omonoid__add(T_a) ),
inference(miniscoping,[status(thm)],[f194]) ).
fof(f1373,plain,
! [X0,X1] :
( c_HOL_Oplus__class_Oplus(X1,c_HOL_Ozero__class_Ozero(X0),X0) = X1
| ~ class_OrderedGroup_Omonoid__add(X0) ),
inference(cnf_transformation,[status(thm)],[f1372]) ).
fof(f1374,plain,
! [T_a] :
( ! [V_a] : c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(T_a),V_a,T_a) = V_a
| ~ class_OrderedGroup_Omonoid__add(T_a) ),
inference(miniscoping,[status(thm)],[f195]) ).
fof(f1375,plain,
! [X0,X1] :
( c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(X0),X1,X0) = X1
| ~ class_OrderedGroup_Omonoid__add(X0) ),
inference(cnf_transformation,[status(thm)],[f1374]) ).
fof(f1594,plain,
! [X0,X1] :
( ~ c_lessequals(c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_lessequals(X0,X1,tc_RealDef_Oreal) ),
inference(cnf_transformation,[status(thm)],[f320]) ).
fof(f1601,plain,
c_Transcendental_Osin(c_Transcendental_Opi) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f325]) ).
fof(f1602,plain,
c_Transcendental_Otan(c_Transcendental_Opi) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f326]) ).
fof(f1892,plain,
! [X0] : ~ c_lessequals(c_Transcendental_Oexp(X0,tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f526]) ).
fof(f1946,plain,
! [X0,X1,X2] :
( c_lessequals(X2,X1,X0)
| c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(thm)],[f562]) ).
fof(f2362,plain,
! [X0] :
( c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(X0),X0) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)
| ~ class_RealVector_Oreal__normed__vector(X0) ),
inference(cnf_transformation,[status(thm)],[f821]) ).
fof(f2363,plain,
! [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)
| ~ class_Ring__and__Field_Ocomm__semiring__0(T_a) ),
inference(miniscoping,[status(thm)],[f822]) ).
fof(f2364,plain,
! [X0,X1] :
( c_Polynomial_Opoly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)),X1,X0) = c_HOL_Ozero__class_Ozero(X0)
| ~ class_Ring__and__Field_Ocomm__semiring__0(X0) ),
inference(cnf_transformation,[status(thm)],[f2363]) ).
fof(f2367,plain,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_e,tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f824]) ).
fof(f2381,plain,
! [T_a] :
( ! [V_x] : c_HOL_Ominus__class_Ominus(V_x,V_x,T_a) = c_HOL_Ozero__class_Ozero(T_a)
| ~ class_OrderedGroup_Oab__group__add(T_a) ),
inference(miniscoping,[status(thm)],[f834]) ).
fof(f2382,plain,
! [X0,X1] :
( c_HOL_Ominus__class_Ominus(X1,X1,X0) = c_HOL_Ozero__class_Ozero(X0)
| ~ class_OrderedGroup_Oab__group__add(X0) ),
inference(cnf_transformation,[status(thm)],[f2381]) ).
fof(f2385,plain,
! [T_a] :
( ! [V_a] : c_HOL_Ominus__class_Ominus(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) = V_a
| ~ class_OrderedGroup_Ogroup__add(T_a) ),
inference(miniscoping,[status(thm)],[f836]) ).
fof(f2386,plain,
! [X0,X1] :
( c_HOL_Ominus__class_Ominus(X1,c_HOL_Ozero__class_Ozero(X0),X0) = X1
| ~ class_OrderedGroup_Ogroup__add(X0) ),
inference(cnf_transformation,[status(thm)],[f2385]) ).
fof(f2413,plain,
! [X0] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)
| ~ 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) ),
inference(cnf_transformation,[status(thm)],[f852]) ).
fof(f2454,plain,
class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f893]) ).
fof(f2502,plain,
class_OrderedGroup_Omonoid__add(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f941]) ).
fof(f2504,plain,
class_OrderedGroup_Ogroup__add(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f943]) ).
fof(f2513,plain,
class_Orderings_Olinorder(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f952]) ).
fof(f2528,plain,
class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f967]) ).
fof(f2531,plain,
class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f970]) ).
fof(f2539,plain,
class_OrderedGroup_Oab__group__add(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f978]) ).
fof(f2731,plain,
! [X0,X1,X2] :
( c_lessequals(X0,X1,tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Oplus__class_Oplus(c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal),X2,tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X2,tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f1076,f1594]) ).
fof(f2732,definition,
( sQ2_spl
<=> class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f2734,plain,
( sQ2_spl
| ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f2732]) ).
fof(f2735,definition,
! [X0,X1,X2] :
( sQ3_spl
<=> ( c_lessequals(X0,X1,tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Oplus__class_Oplus(c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal),X2,tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X2,tc_RealDef_Oreal),tc_RealDef_Oreal) ) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f2736,plain,
! [X0,X1,X2] :
( ~ sQ3_spl
| c_lessequals(X0,X1,tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Oplus__class_Oplus(c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal),X2,tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X2,tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f2735]) ).
fof(f2738,plain,
( sQ3_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f2731,f2732,f2735]) ).
fof(f2739,plain,
( sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2734,f2454]) ).
fof(f2740,plain,
sQ2_spl,
inference(contradiction_clause,[status(thm)],[f2739]) ).
fof(f3230,plain,
! [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),
inference(resolution,[status(thm)],[f2528,f2364]) ).
fof(f3247,plain,
! [X0] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)
| ~ 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) ),
inference(backward_demodulation,[status(thm)],[f3230,f2413]) ).
fof(f3248,plain,
! [X0] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)
| ~ 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) ),
inference(forward_demodulation,[status(thm)],[f3230,f3247]) ).
fof(f3646,plain,
! [X0] :
( ~ c_HOL_Oord__class_Oless(c_Transcendental_Osin(c_Transcendental_Opi),X0,tc_RealDef_Oreal)
| ~ 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) ),
inference(backward_demodulation,[status(thm)],[f1601,f3248]) ).
fof(f3677,plain,
! [X0,X1,X2] :
( ~ sQ3_spl
| c_lessequals(X0,X1,tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Oplus__class_Oplus(c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal),X2,tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_Transcendental_Osin(c_Transcendental_Opi),X2,tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(backward_demodulation,[status(thm)],[f1601,f2736]) ).
fof(f3708,plain,
c_HOL_Oord__class_Oless(c_Transcendental_Osin(c_Transcendental_Opi),v_e,tc_RealDef_Oreal),
inference(backward_demodulation,[status(thm)],[f1601,f2367]) ).
fof(f3713,definition,
( sQ21_spl
<=> 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) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f3715,plain,
( sQ21_spl
| ~ 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) ),
inference(component_clause,[status(thm)],[f3713]) ).
fof(f3716,definition,
! [X0] :
( sQ22_spl
<=> ~ c_HOL_Oord__class_Oless(c_Transcendental_Osin(c_Transcendental_Opi),X0,tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f3717,plain,
! [X0] :
( ~ sQ22_spl
| ~ c_HOL_Oord__class_Oless(c_Transcendental_Osin(c_Transcendental_Opi),X0,tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f3716]) ).
fof(f3719,plain,
( sQ22_spl
| ~ sQ21_spl ),
inference(split_clause,[status(thm)],[f3646,f3713,f3716]) ).
fof(f3747,plain,
c_Transcendental_Otan(c_Transcendental_Opi) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(backward_demodulation,[status(thm)],[f3748,f1601]) ).
fof(f3748,plain,
c_Transcendental_Otan(c_Transcendental_Opi) = c_Transcendental_Osin(c_Transcendental_Opi),
inference(forward_demodulation,[status(thm)],[f1601,f1602]) ).
fof(f3779,plain,
c_HOL_Oord__class_Oless(c_Transcendental_Otan(c_Transcendental_Opi),v_e,tc_RealDef_Oreal),
inference(forward_demodulation,[status(thm)],[f3748,f3708]) ).
fof(f3858,plain,
! [X0,X1,X2] :
( ~ sQ3_spl
| c_lessequals(X0,X1,tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Oplus__class_Oplus(c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal),X2,tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_Transcendental_Otan(c_Transcendental_Opi),X2,tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(forward_demodulation,[status(thm)],[f3748,f3677]) ).
fof(f5706,plain,
! [X0] : c_HOL_Oplus__class_Oplus(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) = X0,
inference(resolution,[status(thm)],[f1373,f2502]) ).
fof(f5708,plain,
! [X0] : c_HOL_Oplus__class_Oplus(X0,c_Transcendental_Otan(c_Transcendental_Opi),tc_RealDef_Oreal) = X0,
inference(forward_demodulation,[status(thm)],[f3747,f5706]) ).
fof(f5804,plain,
! [X0] : c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal) = X0,
inference(resolution,[status(thm)],[f1375,f2502]) ).
fof(f5806,plain,
! [X0] : c_HOL_Oplus__class_Oplus(c_Transcendental_Otan(c_Transcendental_Opi),X0,tc_RealDef_Oreal) = X0,
inference(forward_demodulation,[status(thm)],[f3747,f5804]) ).
fof(f5829,plain,
! [X0,X1,X2] :
( ~ sQ3_spl
| c_lessequals(X0,X1,tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Oplus__class_Oplus(c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal),X2,tc_RealDef_Oreal),X2,tc_RealDef_Oreal) ),
inference(backward_demodulation,[status(thm)],[f5806,f3858]) ).
fof(f6163,plain,
! [X0] : c_HOL_Ominus__class_Ominus(X0,X0,tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(resolution,[status(thm)],[f2382,f2539]) ).
fof(f6166,plain,
( sQ21_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) ),
inference(backward_demodulation,[status(thm)],[f6163,f3715]) ).
fof(f6213,plain,
! [X0] : c_HOL_Ominus__class_Ominus(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) = X0,
inference(resolution,[status(thm)],[f2386,f2504]) ).
fof(f6214,plain,
! [X0] : c_HOL_Ominus__class_Ominus(X0,c_Transcendental_Otan(c_Transcendental_Opi),tc_RealDef_Oreal) = X0,
inference(forward_demodulation,[status(thm)],[f3747,f6213]) ).
fof(f6221,plain,
! [X0,X1] :
( ~ sQ3_spl
| c_lessequals(X0,c_Transcendental_Otan(c_Transcendental_Opi),tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Oplus__class_Oplus(X0,X1,tc_RealDef_Oreal),X1,tc_RealDef_Oreal) ),
inference(paramodulation,[status(thm)],[f6214,f5829]) ).
fof(f8707,plain,
! [X0] : ~ c_lessequals(c_Transcendental_Oexp(X0,tc_RealDef_Oreal),c_Transcendental_Otan(c_Transcendental_Opi),tc_RealDef_Oreal),
inference(forward_demodulation,[status(thm)],[f3747,f1892]) ).
fof(f8714,plain,
! [X0,X1] :
( ~ sQ3_spl
| ~ c_lessequals(c_HOL_Oplus__class_Oplus(c_Transcendental_Oexp(X0,tc_RealDef_Oreal),X1,tc_RealDef_Oreal),X1,tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f8707,f6221]) ).
fof(f9440,plain,
! [X0,X1] :
( c_lessequals(X1,X0,tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f1946,f2513]) ).
fof(f9445,plain,
! [X0,X1] :
( ~ sQ3_spl
| c_HOL_Oord__class_Oless(X0,c_HOL_Oplus__class_Oplus(c_Transcendental_Oexp(X1,tc_RealDef_Oreal),X0,tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f9440,f8714]) ).
fof(f9688,plain,
! [X0] :
( ~ sQ3_spl
| c_HOL_Oord__class_Oless(c_Transcendental_Otan(c_Transcendental_Opi),c_Transcendental_Oexp(X0,tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(paramodulation,[status(thm)],[f5708,f9445]) ).
fof(f9750,plain,
! [X0] :
( c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(X0),X0) = c_Transcendental_Otan(c_Transcendental_Opi)
| ~ class_RealVector_Oreal__normed__vector(X0) ),
inference(forward_demodulation,[status(thm)],[f3747,f2362]) ).
fof(f9751,plain,
c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_Transcendental_Otan(c_Transcendental_Opi),
inference(resolution,[status(thm)],[f9750,f2531]) ).
fof(f9760,plain,
( sQ21_spl
| ~ c_HOL_Oord__class_Oless(c_Transcendental_Otan(c_Transcendental_Opi),v_e,tc_RealDef_Oreal) ),
inference(backward_demodulation,[status(thm)],[f9751,f6166]) ).
fof(f9791,plain,
( sQ21_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9760,f3779]) ).
fof(f9792,plain,
sQ21_spl,
inference(contradiction_clause,[status(thm)],[f9791]) ).
fof(f9840,plain,
! [X0] :
( ~ sQ22_spl
| ~ c_HOL_Oord__class_Oless(c_Transcendental_Otan(c_Transcendental_Opi),X0,tc_RealDef_Oreal) ),
inference(forward_demodulation,[status(thm)],[f3748,f3717]) ).
fof(f9867,plain,
( ~ sQ3_spl
| ~ sQ22_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f9688,f9840]) ).
fof(f9927,plain,
( ~ sQ3_spl
| ~ sQ22_spl ),
inference(contradiction_clause,[status(thm)],[f9867]) ).
fof(f9928,plain,
$false,
inference(sat_refutation,[status(thm)],[f2738,f2740,f3719,f9792,f9927]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : ALG368-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.45 % Computer : n006.cluster.edu
% 0.17/0.45 % Model : x86_64 x86_64
% 0.17/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.45 % Memory : 8046.5625MB
% 0.17/0.45 % OS : Linux 6.8.0-71-generic
% 0.17/0.45 % CPULimit : 300
% 0.17/0.45 % WCLimit : 300
% 0.17/0.45 % DateTime : Mon Sep 21 13:17:42 UTC 2026
% 0.17/0.45 % CPUTime :
% 0.27/0.59 % Drodi V4.1.1
% 27.76/4.19 % Refutation found
% 27.76/4.19 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 27.76/4.19 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 1.08/4.33 % Elapsed time: 3.858404 seconds
% 1.08/4.33 % CPU time: 29.052056 seconds
% 1.08/4.33 % Total memory used: 630.593 MB
% 1.08/4.33 % Net memory used: 623.584 MB
%------------------------------------------------------------------------------