%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWW233+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n015.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 03:07:29 PM UTC 2026
% Result : Theorem 30.21s 4.49s
% Output : CNFRefutation 30.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 52
% Syntax : Number of formulae : 170 ( 68 unt; 24 def)
% Number of atoms : 296 ( 7 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 207 ( 81 ~; 93 |; 0 &)
% ( 24 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 2 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 42 ( 40 usr; 25 prp; 0-3 aty)
% Number of functors : 11 ( 11 usr; 6 con; 0-3 aty)
% Number of variables : 61 ( 61 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,v_r____)),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z____)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [V_w] : c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_w,V_w),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [V_w,V_z] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_w,V_z)
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_z,V_w) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [V_k,V_j,V_i] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_i,V_j)
=> ( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_j,V_k)
=> c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_i,V_k) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f33,axiom,
! [V_a,T_a] :
( class_Groups_Oordered__ab__group__add__abs(T_a)
=> ( c_Orderings_Oord__class_Oless__eq(T_a,c_Groups_Ozero__class_Ozero(T_a),V_a)
=> c_Groups_Oabs__class_Oabs(T_a,V_a) = V_a ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f34,axiom,
! [T_a] :
( class_Rings_Olinordered__semidom(T_a)
=> ~ c_Orderings_Oord__class_Oless__eq(T_a,c_Groups_Oone__class_Oone(T_a),c_Groups_Ozero__class_Ozero(T_a)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f41,axiom,
! [V_x,T_a] :
( class_RealVector_Oreal__normed__vector(T_a)
=> c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(T_a,V_x)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f77,axiom,
! [V_c,V_b,V_a,T_a] :
( class_Groups_Oordered__comm__monoid__add(T_a)
=> ( c_Orderings_Oord__class_Oless__eq(T_a,c_Groups_Ozero__class_Ozero(T_a),V_a)
=> ( c_Orderings_Oord__class_Oless__eq(T_a,V_b,V_c)
=> c_Orderings_Oord__class_Oless__eq(T_a,V_b,c_Groups_Oplus__class_Oplus(T_a,V_a,V_c)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1025,axiom,
class_Rings_Olinordered__semiring(tc_Int_Oint),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1034,axiom,
class_Rings_Olinordered__ring(tc_Int_Oint),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1075,axiom,
class_Rings_Olinordered__semiring(tc_Nat_Onat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1105,axiom,
class_Groups_Oordered__ab__semigroup__add__imp__le(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1110,axiom,
class_RealVector_Oreal__normed__algebra__1(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1112,axiom,
class_Groups_Oordered__ab__group__add__abs(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1113,axiom,
class_RealVector_Oreal__normed__algebra(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1114,axiom,
class_Groups_Oordered__comm__monoid__add(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1119,axiom,
class_RealVector_Oreal__normed__vector(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1126,axiom,
class_Rings_Olinordered__semiring(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1127,axiom,
class_Rings_Olinordered__semidom(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1135,axiom,
class_Rings_Olinordered__ring(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1171,axiom,
class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1173,axiom,
class_Groups_Ocancel__semigroup__add(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1176,axiom,
class_Groups_Oab__semigroup__add(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1178,axiom,
class_Groups_Ocomm__monoid__add(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1179,axiom,
class_Rings_Ocomm__semiring__1(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1184,axiom,
class_Rings_Ozero__neq__one(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1187,axiom,
class_Groups_Omonoid__add(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1261,conjecture,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_r____,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z____)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1262,negated_conjecture,
~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_r____,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z____)),
inference(negated_conjecture,[status(cth)],[f1261]) ).
fof(f1270,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,v_r____)),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z____)),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f1271,plain,
! [X0] : c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X0),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f1272,plain,
! [X0,X1] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X0)
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f1273,plain,
! [V_k,V_j,V_i] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_i,V_k)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_j,V_k)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_i,V_j) ),
inference(pre_NNF_transformation,[status(thm)],[f7]) ).
fof(f1274,plain,
! [V_j,V_i] :
( ! [V_k] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_i,V_k)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_j,V_k) )
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_i,V_j) ),
inference(miniscoping,[status(thm)],[f1273]) ).
fof(f1275,plain,
! [X0,X1,X2] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X2)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X2)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1274]) ).
fof(f1359,plain,
! [V_a,T_a] :
( c_Groups_Oabs__class_Oabs(T_a,V_a) = V_a
| ~ c_Orderings_Oord__class_Oless__eq(T_a,c_Groups_Ozero__class_Ozero(T_a),V_a)
| ~ class_Groups_Oordered__ab__group__add__abs(T_a) ),
inference(pre_NNF_transformation,[status(thm)],[f33]) ).
fof(f1360,plain,
! [T_a] :
( ! [V_a] :
( c_Groups_Oabs__class_Oabs(T_a,V_a) = V_a
| ~ c_Orderings_Oord__class_Oless__eq(T_a,c_Groups_Ozero__class_Ozero(T_a),V_a) )
| ~ class_Groups_Oordered__ab__group__add__abs(T_a) ),
inference(miniscoping,[status(thm)],[f1359]) ).
fof(f1361,plain,
! [X0,X1] :
( c_Groups_Oabs__class_Oabs(X0,X1) = X1
| ~ c_Orderings_Oord__class_Oless__eq(X0,c_Groups_Ozero__class_Ozero(X0),X1)
| ~ class_Groups_Oordered__ab__group__add__abs(X0) ),
inference(cnf_transformation,[status(thm)],[f1360]) ).
fof(f1362,plain,
! [T_a] :
( ~ c_Orderings_Oord__class_Oless__eq(T_a,c_Groups_Oone__class_Oone(T_a),c_Groups_Ozero__class_Ozero(T_a))
| ~ class_Rings_Olinordered__semidom(T_a) ),
inference(pre_NNF_transformation,[status(thm)],[f34]) ).
fof(f1363,plain,
! [X0] :
( ~ c_Orderings_Oord__class_Oless__eq(X0,c_Groups_Oone__class_Oone(X0),c_Groups_Ozero__class_Ozero(X0))
| ~ class_Rings_Olinordered__semidom(X0) ),
inference(cnf_transformation,[status(thm)],[f1362]) ).
fof(f1381,plain,
! [V_x,T_a] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(T_a,V_x))
| ~ class_RealVector_Oreal__normed__vector(T_a) ),
inference(pre_NNF_transformation,[status(thm)],[f41]) ).
fof(f1382,plain,
! [T_a] :
( ! [V_x] : c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(T_a,V_x))
| ~ class_RealVector_Oreal__normed__vector(T_a) ),
inference(miniscoping,[status(thm)],[f1381]) ).
fof(f1383,plain,
! [X0,X1] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(X0,X1))
| ~ class_RealVector_Oreal__normed__vector(X0) ),
inference(cnf_transformation,[status(thm)],[f1382]) ).
fof(f1500,plain,
! [V_c,V_b,V_a,T_a] :
( c_Orderings_Oord__class_Oless__eq(T_a,V_b,c_Groups_Oplus__class_Oplus(T_a,V_a,V_c))
| ~ c_Orderings_Oord__class_Oless__eq(T_a,V_b,V_c)
| ~ c_Orderings_Oord__class_Oless__eq(T_a,c_Groups_Ozero__class_Ozero(T_a),V_a)
| ~ class_Groups_Oordered__comm__monoid__add(T_a) ),
inference(pre_NNF_transformation,[status(thm)],[f77]) ).
fof(f1501,plain,
! [T_a] :
( ! [V_a] :
( ! [V_c,V_b] :
( c_Orderings_Oord__class_Oless__eq(T_a,V_b,c_Groups_Oplus__class_Oplus(T_a,V_a,V_c))
| ~ c_Orderings_Oord__class_Oless__eq(T_a,V_b,V_c) )
| ~ c_Orderings_Oord__class_Oless__eq(T_a,c_Groups_Ozero__class_Ozero(T_a),V_a) )
| ~ class_Groups_Oordered__comm__monoid__add(T_a) ),
inference(miniscoping,[status(thm)],[f1500]) ).
fof(f1502,plain,
! [X0,X1,X2,X3] :
( c_Orderings_Oord__class_Oless__eq(X0,X2,c_Groups_Oplus__class_Oplus(X0,X1,X3))
| ~ c_Orderings_Oord__class_Oless__eq(X0,X2,X3)
| ~ c_Orderings_Oord__class_Oless__eq(X0,c_Groups_Ozero__class_Ozero(X0),X1)
| ~ class_Groups_Oordered__comm__monoid__add(X0) ),
inference(cnf_transformation,[status(thm)],[f1501]) ).
fof(f4419,plain,
class_Rings_Olinordered__semiring(tc_Int_Oint),
inference(cnf_transformation,[status(thm)],[f1025]) ).
fof(f4428,plain,
class_Rings_Olinordered__ring(tc_Int_Oint),
inference(cnf_transformation,[status(thm)],[f1034]) ).
fof(f4469,plain,
class_Rings_Olinordered__semiring(tc_Nat_Onat),
inference(cnf_transformation,[status(thm)],[f1075]) ).
fof(f4499,plain,
class_Groups_Oordered__ab__semigroup__add__imp__le(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f1105]) ).
fof(f4504,plain,
class_RealVector_Oreal__normed__algebra__1(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f1110]) ).
fof(f4506,plain,
class_Groups_Oordered__ab__group__add__abs(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f1112]) ).
fof(f4507,plain,
class_RealVector_Oreal__normed__algebra(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f1113]) ).
fof(f4508,plain,
class_Groups_Oordered__comm__monoid__add(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f1114]) ).
fof(f4513,plain,
class_RealVector_Oreal__normed__vector(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f1119]) ).
fof(f4520,plain,
class_Rings_Olinordered__semiring(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f1126]) ).
fof(f4521,plain,
class_Rings_Olinordered__semidom(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f1127]) ).
fof(f4529,plain,
class_Rings_Olinordered__ring(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f1135]) ).
fof(f4565,plain,
class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f1171]) ).
fof(f4567,plain,
class_Groups_Ocancel__semigroup__add(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f1173]) ).
fof(f4570,plain,
class_Groups_Oab__semigroup__add(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f1176]) ).
fof(f4572,plain,
class_Groups_Ocomm__monoid__add(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f1178]) ).
fof(f4573,plain,
class_Rings_Ocomm__semiring__1(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f1179]) ).
fof(f4578,plain,
class_Rings_Ozero__neq__one(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f1184]) ).
fof(f4581,plain,
class_Groups_Omonoid__add(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f1187]) ).
fof(f4713,plain,
~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_r____,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z____)),
inference(cnf_transformation,[status(thm)],[f1262]) ).
fof(f4838,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z____),v_r____),
inference(resolution,[status(thm)],[f1272,f4713]) ).
fof(f4843,plain,
! [X0] :
( ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z____))
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_r____,X0) ),
inference(resolution,[status(thm)],[f1275,f4713]) ).
fof(f4854,plain,
! [X0] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,v_r____)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z____)) ),
inference(resolution,[status(thm)],[f4838,f1275]) ).
fof(f4855,plain,
~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_r____,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,v_r____))),
inference(resolution,[status(thm)],[f4843,f1270]) ).
fof(f5512,definition,
( sQ96_spl
<=> class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex) ),
introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition]) ).
fof(f5514,plain,
( sQ96_spl
| ~ class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex) ),
inference(component_clause,[status(thm)],[f5512]) ).
fof(f5518,definition,
( sQ98_spl
<=> c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),v_r____) ),
introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition]) ).
fof(f5519,plain,
( ~ sQ98_spl
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),v_r____) ),
inference(component_clause,[status(thm)],[f5518]) ).
fof(f5558,definition,
( sQ105_spl
<=> class_Groups_Oordered__ab__group__add__abs(tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition]) ).
fof(f5560,plain,
( sQ105_spl
| ~ class_Groups_Oordered__ab__group__add__abs(tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f5558]) ).
fof(f5721,plain,
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))
| ~ class_Rings_Olinordered__semidom(tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f1363,f1272]) ).
fof(f5725,definition,
( sQ129_spl
<=> class_Rings_Olinordered__semidom(tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ129_spl])],[split_symbol_definition]) ).
fof(f5727,plain,
( sQ129_spl
| ~ class_Rings_Olinordered__semidom(tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f5725]) ).
fof(f5732,definition,
( sQ131_spl
<=> c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)) ),
introduced(definition,[new_symbols(definition,[sQ131_spl])],[split_symbol_definition]) ).
fof(f5735,plain,
( sQ131_spl
| ~ sQ129_spl ),
inference(split_clause,[status(thm)],[f5721,f5725,f5732]) ).
fof(f5923,definition,
( sQ156_spl
<=> class_Groups_Oordered__comm__monoid__add(tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ156_spl])],[split_symbol_definition]) ).
fof(f5925,plain,
( sQ156_spl
| ~ class_Groups_Oordered__comm__monoid__add(tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f5923]) ).
fof(f5945,definition,
( sQ160_spl
<=> class_RealVector_Oreal__normed__algebra__1(tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ160_spl])],[split_symbol_definition]) ).
fof(f5947,plain,
( sQ160_spl
| ~ class_RealVector_Oreal__normed__algebra__1(tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f5945]) ).
fof(f5952,definition,
( sQ162_spl
<=> class_RealVector_Oreal__normed__vector(tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ162_spl])],[split_symbol_definition]) ).
fof(f5954,plain,
( sQ162_spl
| ~ class_RealVector_Oreal__normed__vector(tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f5952]) ).
fof(f5985,plain,
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),v_r____)
| ~ class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex) ),
inference(resolution,[status(thm)],[f1383,f4854]) ).
fof(f6007,plain,
( sQ98_spl
| ~ sQ96_spl ),
inference(split_clause,[status(thm)],[f5985,f5512,f5518]) ).
fof(f6077,plain,
( ~ sQ98_spl
| c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,v_r____) = v_r____
| ~ class_Groups_Oordered__ab__group__add__abs(tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f5519,f1361]) ).
fof(f6085,definition,
( sQ183_spl
<=> c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,v_r____) = v_r____ ),
introduced(definition,[new_symbols(definition,[sQ183_spl])],[split_symbol_definition]) ).
fof(f6086,plain,
( ~ sQ183_spl
| c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,v_r____) = v_r____ ),
inference(component_clause,[status(thm)],[f6085]) ).
fof(f6088,plain,
( ~ sQ98_spl
| sQ183_spl
| ~ sQ105_spl ),
inference(split_clause,[status(thm)],[f6077,f5558,f6085,f5518]) ).
fof(f6611,definition,
( sQ256_spl
<=> class_Groups_Oordered__ab__semigroup__add__imp__le(tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ256_spl])],[split_symbol_definition]) ).
fof(f6613,plain,
( sQ256_spl
| ~ class_Groups_Oordered__ab__semigroup__add__imp__le(tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f6611]) ).
fof(f7122,definition,
( sQ325_spl
<=> class_Groups_Omonoid__add(tc_Complex_Ocomplex) ),
introduced(definition,[new_symbols(definition,[sQ325_spl])],[split_symbol_definition]) ).
fof(f7124,plain,
( sQ325_spl
| ~ class_Groups_Omonoid__add(tc_Complex_Ocomplex) ),
inference(component_clause,[status(thm)],[f7122]) ).
fof(f7129,definition,
( sQ327_spl
<=> class_Groups_Ocomm__monoid__add(tc_Complex_Ocomplex) ),
introduced(definition,[new_symbols(definition,[sQ327_spl])],[split_symbol_definition]) ).
fof(f7131,plain,
( sQ327_spl
| ~ class_Groups_Ocomm__monoid__add(tc_Complex_Ocomplex) ),
inference(component_clause,[status(thm)],[f7129]) ).
fof(f7455,definition,
( sQ360_spl
<=> class_Groups_Ocancel__semigroup__add(tc_Complex_Ocomplex) ),
introduced(definition,[new_symbols(definition,[sQ360_spl])],[split_symbol_definition]) ).
fof(f7457,plain,
( sQ360_spl
| ~ class_Groups_Ocancel__semigroup__add(tc_Complex_Ocomplex) ),
inference(component_clause,[status(thm)],[f7455]) ).
fof(f7462,definition,
( sQ361_spl
<=> class_Groups_Oab__semigroup__add(tc_Complex_Ocomplex) ),
introduced(definition,[new_symbols(definition,[sQ361_spl])],[split_symbol_definition]) ).
fof(f7464,plain,
( sQ361_spl
| ~ class_Groups_Oab__semigroup__add(tc_Complex_Ocomplex) ),
inference(component_clause,[status(thm)],[f7462]) ).
fof(f7709,plain,
( ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_r____,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,v_r____))
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))
| ~ class_Groups_Oordered__comm__monoid__add(tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f1502,f4855]) ).
fof(f7736,definition,
( sQ401_spl
<=> c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_r____,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,v_r____)) ),
introduced(definition,[new_symbols(definition,[sQ401_spl])],[split_symbol_definition]) ).
fof(f7738,plain,
( sQ401_spl
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_r____,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,v_r____)) ),
inference(component_clause,[status(thm)],[f7736]) ).
fof(f7739,plain,
( ~ sQ401_spl
| ~ sQ131_spl
| ~ sQ156_spl ),
inference(split_clause,[status(thm)],[f7709,f5923,f5732,f7736]) ).
fof(f8629,definition,
( sQ519_spl
<=> class_Rings_Ozero__neq__one(tc_Complex_Ocomplex) ),
introduced(definition,[new_symbols(definition,[sQ519_spl])],[split_symbol_definition]) ).
fof(f8631,plain,
( sQ519_spl
| ~ class_Rings_Ozero__neq__one(tc_Complex_Ocomplex) ),
inference(component_clause,[status(thm)],[f8629]) ).
fof(f9295,definition,
( sQ607_spl
<=> class_Rings_Ocomm__semiring__1(tc_Complex_Ocomplex) ),
introduced(definition,[new_symbols(definition,[sQ607_spl])],[split_symbol_definition]) ).
fof(f9297,plain,
( sQ607_spl
| ~ class_Rings_Ocomm__semiring__1(tc_Complex_Ocomplex) ),
inference(component_clause,[status(thm)],[f9295]) ).
fof(f9649,definition,
( sQ636_spl
<=> class_RealVector_Oreal__normed__algebra(tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ636_spl])],[split_symbol_definition]) ).
fof(f9651,plain,
( sQ636_spl
| ~ class_RealVector_Oreal__normed__algebra(tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f9649]) ).
fof(f10667,plain,
( sQ105_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4506,f5560]) ).
fof(f10668,plain,
sQ105_spl,
inference(contradiction_clause,[status(thm)],[f10667]) ).
fof(f10874,plain,
( sQ156_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4508,f5925]) ).
fof(f10875,plain,
sQ156_spl,
inference(contradiction_clause,[status(thm)],[f10874]) ).
fof(f11567,plain,
( sQ129_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4521,f5727]) ).
fof(f11568,plain,
sQ129_spl,
inference(contradiction_clause,[status(thm)],[f11567]) ).
fof(f15068,plain,
( sQ96_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4565,f5514]) ).
fof(f15069,plain,
sQ96_spl,
inference(contradiction_clause,[status(thm)],[f15068]) ).
fof(f15204,plain,
( sQ360_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4567,f7457]) ).
fof(f15205,plain,
sQ360_spl,
inference(contradiction_clause,[status(thm)],[f15204]) ).
fof(f15277,plain,
( sQ361_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4570,f7464]) ).
fof(f15278,plain,
sQ361_spl,
inference(contradiction_clause,[status(thm)],[f15277]) ).
fof(f15279,plain,
( sQ327_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4572,f7131]) ).
fof(f15280,plain,
sQ327_spl,
inference(contradiction_clause,[status(thm)],[f15279]) ).
fof(f15391,plain,
( sQ607_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4573,f9297]) ).
fof(f15392,plain,
sQ607_spl,
inference(contradiction_clause,[status(thm)],[f15391]) ).
fof(f15529,definition,
( sQ1214_spl
<=> class_Rings_Olinordered__ring(tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ1214_spl])],[split_symbol_definition]) ).
fof(f15531,plain,
( sQ1214_spl
| ~ class_Rings_Olinordered__ring(tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f15529]) ).
fof(f15572,plain,
( sQ1214_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f15531,f4529]) ).
fof(f15573,plain,
sQ1214_spl,
inference(contradiction_clause,[status(thm)],[f15572]) ).
fof(f15589,plain,
( sQ519_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4578,f8631]) ).
fof(f15590,plain,
sQ519_spl,
inference(contradiction_clause,[status(thm)],[f15589]) ).
fof(f15641,plain,
( sQ325_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4581,f7124]) ).
fof(f15642,plain,
sQ325_spl,
inference(contradiction_clause,[status(thm)],[f15641]) ).
fof(f15911,definition,
( sQ1254_spl
<=> class_Rings_Olinordered__ring(tc_Int_Oint) ),
introduced(definition,[new_symbols(definition,[sQ1254_spl])],[split_symbol_definition]) ).
fof(f15913,plain,
( sQ1254_spl
| ~ class_Rings_Olinordered__ring(tc_Int_Oint) ),
inference(component_clause,[status(thm)],[f15911]) ).
fof(f15942,plain,
( sQ1254_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f15913,f4428]) ).
fof(f15943,plain,
sQ1254_spl,
inference(contradiction_clause,[status(thm)],[f15942]) ).
fof(f17384,definition,
! [X1,X2] :
( sQ1393_spl
<=> ( ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X2,X1)
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X2) ) ),
introduced(definition,[new_symbols(definition,[sQ1393_spl])],[split_symbol_definition]) ).
fof(f17385,plain,
! [X0,X1] :
( ~ sQ1393_spl
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X0)
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X1) ),
inference(component_clause,[status(thm)],[f17384]) ).
fof(f17435,plain,
! [X0,X1] :
( ~ sQ1393_spl
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f17385,f1272]) ).
fof(f17561,plain,
( ~ sQ1393_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f4713,f17435]) ).
fof(f17576,plain,
~ sQ1393_spl,
inference(contradiction_clause,[status(thm)],[f17561]) ).
fof(f17621,plain,
( sQ162_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5954,f4513]) ).
fof(f17622,plain,
sQ162_spl,
inference(contradiction_clause,[status(thm)],[f17621]) ).
fof(f17623,plain,
( sQ160_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5947,f4504]) ).
fof(f17624,plain,
sQ160_spl,
inference(contradiction_clause,[status(thm)],[f17623]) ).
fof(f17933,definition,
( sQ1450_spl
<=> class_Rings_Olinordered__semiring(tc_Nat_Onat) ),
introduced(definition,[new_symbols(definition,[sQ1450_spl])],[split_symbol_definition]) ).
fof(f17935,plain,
( sQ1450_spl
| ~ class_Rings_Olinordered__semiring(tc_Nat_Onat) ),
inference(component_clause,[status(thm)],[f17933]) ).
fof(f17940,definition,
( sQ1452_spl
<=> class_Rings_Olinordered__semiring(tc_Int_Oint) ),
introduced(definition,[new_symbols(definition,[sQ1452_spl])],[split_symbol_definition]) ).
fof(f17942,plain,
( sQ1452_spl
| ~ class_Rings_Olinordered__semiring(tc_Int_Oint) ),
inference(component_clause,[status(thm)],[f17940]) ).
fof(f17947,definition,
( sQ1454_spl
<=> class_Rings_Olinordered__semiring(tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ1454_spl])],[split_symbol_definition]) ).
fof(f17949,plain,
( sQ1454_spl
| ~ class_Rings_Olinordered__semiring(tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f17947]) ).
fof(f17974,plain,
( sQ1454_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f17949,f4520]) ).
fof(f17975,plain,
sQ1454_spl,
inference(contradiction_clause,[status(thm)],[f17974]) ).
fof(f17976,plain,
( sQ1452_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f17942,f4419]) ).
fof(f17977,plain,
sQ1452_spl,
inference(contradiction_clause,[status(thm)],[f17976]) ).
fof(f17978,plain,
( sQ1450_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f17935,f4469]) ).
fof(f17979,plain,
sQ1450_spl,
inference(contradiction_clause,[status(thm)],[f17978]) ).
fof(f18131,plain,
( sQ256_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6613,f4499]) ).
fof(f18132,plain,
sQ256_spl,
inference(contradiction_clause,[status(thm)],[f18131]) ).
fof(f18929,plain,
( sQ636_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9651,f4507]) ).
fof(f18930,plain,
sQ636_spl,
inference(contradiction_clause,[status(thm)],[f18929]) ).
fof(f19710,plain,
( sQ401_spl
| ~ sQ183_spl
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_r____,v_r____) ),
inference(forward_demodulation,[status(thm)],[f6086,f7738]) ).
fof(f19711,plain,
( sQ401_spl
| ~ sQ183_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19710,f1271]) ).
fof(f19712,plain,
( sQ401_spl
| ~ sQ183_spl ),
inference(contradiction_clause,[status(thm)],[f19711]) ).
fof(f19713,plain,
$false,
inference(sat_refutation,[status(thm)],[f5735,f6007,f6088,f7739,f10668,f10875,f11568,f15069,f15205,f15278,f15280,f15392,f15573,f15590,f15642,f15943,f17576,f17622,f17624,f17975,f17977,f17979,f18132,f18930,f19712]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWW233+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.44 % Computer : n015.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 09:46:06 UTC 2026
% 0.18/0.45 % CPUTime :
% 0.36/0.60 % Drodi V4.1.1
% 30.21/4.49 % Refutation found
% 30.21/4.49 % SZS status Theorem for theBenchmark: Theorem is valid
% 30.21/4.49 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 23.54/4.57 % Elapsed time: 4.099682 seconds
% 23.54/4.57 % CPU time: 31.120010 seconds
% 23.54/4.57 % Total memory used: 366.931 MB
% 23.54/4.57 % Net memory used: 349.955 MB
%------------------------------------------------------------------------------