%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWW180+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 : n026.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:23 PM UTC 2026
% Result : Theorem 6.41s 1.57s
% Output : CNFRefutation 7.53s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 11
% Syntax : Number of formulae : 44 ( 19 unt; 0 def)
% Number of atoms : 109 ( 16 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 120 ( 55 ~; 44 |; 12 &)
% ( 3 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-3 aty)
% Number of functors : 13 ( 13 usr; 5 con; 0-3 aty)
% Number of variables : 66 ( 66 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f99,axiom,
! [V_c,V_b,V_a,T_a] :
( class_Groups_Oordered__comm__monoid__add(T_a)
=> ( c_Orderings_Oord__class_Oless(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(T_a,V_b,c_Groups_Oplus__class_Oplus(T_a,V_a,V_c)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f104,axiom,
! [V_d,V_c,V_b,V_a,T_a] :
( class_Groups_Oordered__cancel__ab__semigroup__add(T_a)
=> ( c_Orderings_Oord__class_Oless(T_a,V_a,V_b)
=> ( c_Orderings_Oord__class_Oless__eq(T_a,V_c,V_d)
=> c_Orderings_Oord__class_Oless(T_a,c_Groups_Oplus__class_Oplus(T_a,V_a,V_c),c_Groups_Oplus__class_Oplus(T_a,V_b,V_d)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f199,axiom,
! [V_w] : c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_w,V_w),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f216,axiom,
! [V_y_2,V_x_2] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2,V_y_2)
<=> ( V_x_2 != V_y_2
& c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2,V_y_2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f222,axiom,
c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) != c_Groups_Oone__class_Oone(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f223,axiom,
! [V_z] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),V_z) = V_z,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f291,axiom,
! [V_x_2] :
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),V_x_2),V_x_2))
<=> V_x_2 = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f534,axiom,
! [V_ra_2,V_x_2] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,V_x_2),V_ra_2)
<=> ( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2,V_ra_2)
& c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,V_ra_2),V_x_2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1111,axiom,
class_Groups_Oordered__cancel__ab__semigroup__add(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1121,axiom,
class_Groups_Oordered__comm__monoid__add(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1275,conjecture,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_r),v_m____)),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____)),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_r),v_m____)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1276,negated_conjecture,
~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_r),v_m____)),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____)),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_r),v_m____)))),
inference(negated_conjecture,[status(cth)],[f1275]) ).
fof(f1603,plain,
! [V_c,V_b,V_a,T_a] :
( c_Orderings_Oord__class_Oless(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(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)],[f99]) ).
fof(f1604,plain,
! [T_a] :
( ! [V_a] :
( ! [V_c,V_b] :
( c_Orderings_Oord__class_Oless(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(T_a,c_Groups_Ozero__class_Ozero(T_a),V_a) )
| ~ class_Groups_Oordered__comm__monoid__add(T_a) ),
inference(miniscoping,[status(thm)],[f1603]) ).
fof(f1605,plain,
! [X0,X1,X2,X3] :
( c_Orderings_Oord__class_Oless(X0,X2,c_Groups_Oplus__class_Oplus(X0,X1,X3))
| ~ c_Orderings_Oord__class_Oless__eq(X0,X2,X3)
| ~ c_Orderings_Oord__class_Oless(X0,c_Groups_Ozero__class_Ozero(X0),X1)
| ~ class_Groups_Oordered__comm__monoid__add(X0) ),
inference(cnf_transformation,[status(thm)],[f1604]) ).
fof(f1620,plain,
! [V_d,V_c,V_b,V_a,T_a] :
( c_Orderings_Oord__class_Oless(T_a,c_Groups_Oplus__class_Oplus(T_a,V_a,V_c),c_Groups_Oplus__class_Oplus(T_a,V_b,V_d))
| ~ c_Orderings_Oord__class_Oless__eq(T_a,V_c,V_d)
| ~ c_Orderings_Oord__class_Oless(T_a,V_a,V_b)
| ~ class_Groups_Oordered__cancel__ab__semigroup__add(T_a) ),
inference(pre_NNF_transformation,[status(thm)],[f104]) ).
fof(f1621,plain,
! [T_a] :
( ! [V_b,V_a] :
( ! [V_d,V_c] :
( c_Orderings_Oord__class_Oless(T_a,c_Groups_Oplus__class_Oplus(T_a,V_a,V_c),c_Groups_Oplus__class_Oplus(T_a,V_b,V_d))
| ~ c_Orderings_Oord__class_Oless__eq(T_a,V_c,V_d) )
| ~ c_Orderings_Oord__class_Oless(T_a,V_a,V_b) )
| ~ class_Groups_Oordered__cancel__ab__semigroup__add(T_a) ),
inference(miniscoping,[status(thm)],[f1620]) ).
fof(f1622,plain,
! [X0,X1,X2,X3,X4] :
( c_Orderings_Oord__class_Oless(X0,c_Groups_Oplus__class_Oplus(X0,X1,X3),c_Groups_Oplus__class_Oplus(X0,X2,X4))
| ~ c_Orderings_Oord__class_Oless__eq(X0,X3,X4)
| ~ c_Orderings_Oord__class_Oless(X0,X1,X2)
| ~ class_Groups_Oordered__cancel__ab__semigroup__add(X0) ),
inference(cnf_transformation,[status(thm)],[f1621]) ).
fof(f1938,plain,
! [X0] : c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X0),
inference(cnf_transformation,[status(thm)],[f199]) ).
fof(f1981,plain,
! [V_y_2,V_x_2] :
( ( V_x_2 = V_y_2
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2,V_y_2)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2,V_y_2) )
& ( ( V_x_2 != V_y_2
& c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2,V_y_2) )
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2,V_y_2) ) ),
inference(NNF_transformation,[status(thm)],[f216]) ).
fof(f1982,plain,
( ! [V_y_2,V_x_2] :
( V_x_2 = V_y_2
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2,V_y_2)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2,V_y_2) )
& ! [V_y_2,V_x_2] :
( ( V_x_2 != V_y_2
& c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2,V_y_2) )
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2,V_y_2) ) ),
inference(miniscoping,[status(thm)],[f1981]) ).
fof(f1983,plain,
! [X0,X1] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X1)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1982]) ).
fof(f2006,plain,
c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) != c_Groups_Oone__class_Oone(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f222]) ).
fof(f2007,plain,
! [X0] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),X0) = X0,
inference(cnf_transformation,[status(thm)],[f223]) ).
fof(f2246,plain,
! [V_x_2] :
( ( V_x_2 != c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),V_x_2),V_x_2)) )
& ( V_x_2 = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),V_x_2),V_x_2)) ) ),
inference(NNF_transformation,[status(thm)],[f291]) ).
fof(f2247,plain,
( ! [V_x_2] :
( V_x_2 != c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),V_x_2),V_x_2)) )
& ! [V_x_2] :
( V_x_2 = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),V_x_2),V_x_2)) ) ),
inference(miniscoping,[status(thm)],[f2246]) ).
fof(f2248,plain,
! [X0] :
( X0 = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X0),X0)) ),
inference(cnf_transformation,[status(thm)],[f2247]) ).
fof(f3050,plain,
! [V_ra_2,V_x_2] :
( ( ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2,V_ra_2)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,V_ra_2),V_x_2)
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,V_x_2),V_ra_2) )
& ( ( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2,V_ra_2)
& c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,V_ra_2),V_x_2) )
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,V_x_2),V_ra_2) ) ),
inference(NNF_transformation,[status(thm)],[f534]) ).
fof(f3051,plain,
( ! [V_ra_2,V_x_2] :
( ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2,V_ra_2)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,V_ra_2),V_x_2)
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,V_x_2),V_ra_2) )
& ! [V_ra_2,V_x_2] :
( ( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2,V_ra_2)
& c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,V_ra_2),V_x_2) )
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,V_x_2),V_ra_2) ) ),
inference(miniscoping,[status(thm)],[f3050]) ).
fof(f3053,plain,
! [X0,X1] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X1)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0),X1) ),
inference(cnf_transformation,[status(thm)],[f3051]) ).
fof(f4588,plain,
class_Groups_Oordered__cancel__ab__semigroup__add(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f1111]) ).
fof(f4598,plain,
class_Groups_Oordered__comm__monoid__add(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f1121]) ).
fof(f4812,plain,
~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_r),v_m____)),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____)),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_r),v_m____)))),
inference(cnf_transformation,[status(thm)],[f1276]) ).
fof(f5026,plain,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_r),v_m____)),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____)),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_r),v_m____)))),
inference(resolution,[status(thm)],[f1983,f4812]) ).
fof(f5819,plain,
( c_Groups_Oone__class_Oone(tc_RealDef_Oreal) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)) ),
inference(paramodulation,[status(thm)],[f2007,f2248]) ).
fof(f5821,plain,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),
inference(forward_subsumption_resolution,[status(thm)],[f5819,f2006]) ).
fof(f8152,plain,
! [X0] : c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0)),
inference(resolution,[status(thm)],[f3053,f1938]) ).
fof(f11798,plain,
( ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_r),v_m____),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_r),v_m____)))
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____)))
| ~ class_Groups_Oordered__cancel__ab__semigroup__add(tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f1622,f5026]) ).
fof(f11844,plain,
( ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_r),v_m____),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_r),v_m____)))
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____))) ),
inference(forward_subsumption_resolution,[status(thm)],[f11798,f4588]) ).
fof(f12562,plain,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____))),
inference(forward_subsumption_resolution,[status(thm)],[f11844,f8152]) ).
fof(f12564,plain,
( ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____))
| ~ c_Orderings_Oord__class_Oless(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)],[f12562,f1605]) ).
fof(f12571,plain,
( ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____))
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)) ),
inference(forward_subsumption_resolution,[status(thm)],[f12564,f4598]) ).
fof(f13256,plain,
~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____)),
inference(forward_subsumption_resolution,[status(thm)],[f12571,f5821]) ).
fof(f13261,plain,
$false,
inference(resolution,[status(thm)],[f13256,f1938]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWW180+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.07 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.20/0.46 % Computer : n026.cluster.edu
% 0.20/0.46 % Model : x86_64 x86_64
% 0.20/0.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/0.46 % Memory : 8046.5625MB
% 0.20/0.46 % OS : Linux 6.8.0-71-generic
% 0.20/0.46 % CPULimit : 300
% 0.20/0.46 % WCLimit : 300
% 0.20/0.46 % DateTime : Mon Sep 21 09:43:06 UTC 2026
% 0.20/0.46 % CPUTime :
% 0.24/0.60 % Drodi V4.1.1
% 6.41/1.57 % Refutation found
% 6.41/1.57 % SZS status Theorem for theBenchmark: Theorem is valid
% 6.41/1.57 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 1.24/1.64 % Elapsed time: 1.151021 seconds
% 1.24/1.64 % CPU time: 7.774562 seconds
% 1.24/1.64 % Total memory used: 270.459 MB
% 1.24/1.64 % Net memory used: 265.393 MB
%------------------------------------------------------------------------------