%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : SWW233+1 : TPTP v9.2.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n005.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 05:30:47 PM UTC 2026
% Result : Theorem 16.52s 10.62s
% Output : CNFRefutation 16.52s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 15
% Syntax : Number of formulae : 49 ( 25 unt; 0 def)
% Number of atoms : 105 ( 9 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 97 ( 41 ~; 37 |; 6 &)
% ( 3 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-3 aty)
% Number of functors : 9 ( 9 usr; 4 con; 0-3 aty)
% Number of variables : 62 ( 0 sgn 41 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(fact_less__le__not__le,axiom,
! [X13,X14,X5] :
( class_Orderings_Opreorder(X5)
=> ( c_Orderings_Oord__class_Oless(X5,X14,X13)
<=> ( c_Orderings_Oord__class_Oless__eq(X5,X14,X13)
& ~ c_Orderings_Oord__class_Oless__eq(X5,X13,X14) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_less__le__not__le) ).
fof(fact_real__norm__def,axiom,
! [X19] : c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X19) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X19),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_real__norm__def) ).
fof(fact_h,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',fact_h) ).
fof(arity_RealDef__Oreal__Orderings_Opreorder,axiom,
class_Orderings_Opreorder(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_RealDef__Oreal__Orderings_Opreorder) ).
fof(fact_add__strict__increasing,axiom,
! [X15,X17,X16,X5] :
( class_Groups_Oordered__comm__monoid__add(X5)
=> ( c_Orderings_Oord__class_Oless(X5,c_Groups_Ozero__class_Ozero(X5),X16)
=> ( c_Orderings_Oord__class_Oless__eq(X5,X17,X15)
=> c_Orderings_Oord__class_Oless(X5,X17,c_Groups_Oplus__class_Oplus(X5,X16,X15)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_add__strict__increasing) ).
fof(fact_less__eq__real__def,axiom,
! [X13,X14] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X14,X13)
<=> ( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X14,X13)
| X14 = X13 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_less__eq__real__def) ).
fof(fact_zero__le__one,axiom,
! [X5] :
( class_Rings_Olinordered__semidom(X5)
=> c_Orderings_Oord__class_Oless__eq(X5,c_Groups_Ozero__class_Ozero(X5),c_Groups_Oone__class_Oone(X5)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_zero__le__one) ).
fof(arity_RealDef__Oreal__Groups_Oordered__comm__monoid__add,axiom,
class_Groups_Oordered__comm__monoid__add(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_RealDef__Oreal__Groups_Oordered__comm__monoid__add) ).
fof(arity_RealDef__Oreal__Rings_Olinordered__semidom,axiom,
class_Rings_Olinordered__semidom(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_RealDef__Oreal__Rings_Olinordered__semidom) ).
fof(fact_real__zero__not__eq__one,axiom,
c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) != c_Groups_Oone__class_Oone(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_real__zero__not__eq__one) ).
fof(fact_real__le__linear,axiom,
! [X6,X7] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X7,X6)
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X6,X7) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_real__le__linear) ).
fof(fact_order__trans,axiom,
! [X7,X12,X4,X5] :
( class_Orderings_Opreorder(X5)
=> ( c_Orderings_Oord__class_Oless__eq(X5,X4,X12)
=> ( c_Orderings_Oord__class_Oless__eq(X5,X12,X7)
=> c_Orderings_Oord__class_Oless__eq(X5,X4,X7) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_order__trans) ).
fof(fact_abs__ge__self,axiom,
! [X16,X5] :
( class_Groups_Oordered__ab__group__add__abs(X5)
=> c_Orderings_Oord__class_Oless__eq(X5,X16,c_Groups_Oabs__class_Oabs(X5,X16)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_abs__ge__self) ).
fof(conj_0,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',conj_0) ).
fof(arity_RealDef__Oreal__Groups_Oordered__ab__group__add__abs,axiom,
class_Groups_Oordered__ab__group__add__abs(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_RealDef__Oreal__Groups_Oordered__ab__group__add__abs) ).
fof(c_0_15,plain,
! [X13,X14,X5] :
( class_Orderings_Opreorder(X5)
=> ( c_Orderings_Oord__class_Oless(X5,X14,X13)
<=> ( c_Orderings_Oord__class_Oless__eq(X5,X14,X13)
& ~ c_Orderings_Oord__class_Oless__eq(X5,X13,X14) ) ) ),
inference(fof_simplification,[status(thm)],[fact_less__le__not__le]) ).
fof(c_0_16,plain,
! [X3005] : c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X3005) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X3005),
inference(variable_rename,[status(thm)],[fact_real__norm__def]) ).
fof(c_0_17,plain,
! [X3595,X3596,X3597] :
( ( c_Orderings_Oord__class_Oless__eq(X3597,X3596,X3595)
| ~ c_Orderings_Oord__class_Oless(X3597,X3596,X3595)
| ~ class_Orderings_Opreorder(X3597) )
& ( ~ c_Orderings_Oord__class_Oless__eq(X3597,X3595,X3596)
| ~ c_Orderings_Oord__class_Oless(X3597,X3596,X3595)
| ~ class_Orderings_Opreorder(X3597) )
& ( ~ c_Orderings_Oord__class_Oless__eq(X3597,X3596,X3595)
| c_Orderings_Oord__class_Oless__eq(X3597,X3595,X3596)
| c_Orderings_Oord__class_Oless(X3597,X3596,X3595)
| ~ class_Orderings_Opreorder(X3597) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_15])])]) ).
cnf(c_0_18,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(split_conjunct,[status(thm)],[fact_h]) ).
cnf(c_0_19,plain,
c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X1) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X1),
inference(split_conjunct,[status(thm)],[c_0_16]) ).
cnf(c_0_20,plain,
( ~ c_Orderings_Oord__class_Oless__eq(X1,X2,X3)
| ~ c_Orderings_Oord__class_Oless(X1,X3,X2)
| ~ class_Orderings_Opreorder(X1) ),
inference(split_conjunct,[status(thm)],[c_0_17]) ).
cnf(c_0_21,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_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,v_r____)),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z____)),
inference(rw,[status(thm)],[c_0_18,c_0_19]) ).
cnf(c_0_22,plain,
class_Orderings_Opreorder(tc_RealDef_Oreal),
inference(split_conjunct,[status(thm)],[arity_RealDef__Oreal__Orderings_Opreorder]) ).
fof(c_0_23,plain,
! [X3875,X3876,X3877,X3878] :
( ~ class_Groups_Oordered__comm__monoid__add(X3878)
| ~ c_Orderings_Oord__class_Oless(X3878,c_Groups_Ozero__class_Ozero(X3878),X3877)
| ~ c_Orderings_Oord__class_Oless__eq(X3878,X3876,X3875)
| c_Orderings_Oord__class_Oless(X3878,X3876,c_Groups_Oplus__class_Oplus(X3878,X3877,X3875)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_add__strict__increasing])]) ).
fof(c_0_24,plain,
! [X3705,X3706] :
( ( ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X3706,X3705)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X3706,X3705)
| X3706 = X3705 )
& ( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X3706,X3705)
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X3706,X3705) )
& ( X3706 != X3705
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X3706,X3705) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_less__eq__real__def])])]) ).
fof(c_0_25,plain,
! [X2997] :
( ~ class_Rings_Olinordered__semidom(X2997)
| c_Orderings_Oord__class_Oless__eq(X2997,c_Groups_Ozero__class_Ozero(X2997),c_Groups_Oone__class_Oone(X2997)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_zero__le__one])]) ).
cnf(c_0_26,plain,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z____),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,v_r____))),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_20,c_0_21]),c_0_22])]) ).
cnf(c_0_27,plain,
( c_Orderings_Oord__class_Oless(X1,X3,c_Groups_Oplus__class_Oplus(X1,X2,X4))
| ~ class_Groups_Oordered__comm__monoid__add(X1)
| ~ c_Orderings_Oord__class_Oless(X1,c_Groups_Ozero__class_Ozero(X1),X2)
| ~ c_Orderings_Oord__class_Oless__eq(X1,X3,X4) ),
inference(split_conjunct,[status(thm)],[c_0_23]) ).
cnf(c_0_28,plain,
class_Groups_Oordered__comm__monoid__add(tc_RealDef_Oreal),
inference(split_conjunct,[status(thm)],[arity_RealDef__Oreal__Groups_Oordered__comm__monoid__add]) ).
cnf(c_0_29,plain,
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X1,X2)
| X1 = X2
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X2) ),
inference(split_conjunct,[status(thm)],[c_0_24]) ).
cnf(c_0_30,plain,
( c_Orderings_Oord__class_Oless__eq(X1,c_Groups_Ozero__class_Ozero(X1),c_Groups_Oone__class_Oone(X1))
| ~ class_Rings_Olinordered__semidom(X1) ),
inference(split_conjunct,[status(thm)],[c_0_25]) ).
cnf(c_0_31,plain,
class_Rings_Olinordered__semidom(tc_RealDef_Oreal),
inference(split_conjunct,[status(thm)],[arity_RealDef__Oreal__Rings_Olinordered__semidom]) ).
cnf(c_0_32,plain,
c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) != c_Groups_Oone__class_Oone(tc_RealDef_Oreal),
inference(split_conjunct,[status(thm)],[fact_real__zero__not__eq__one]) ).
cnf(c_0_33,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))
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z____),c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,v_r____)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_26,c_0_27]),c_0_28])]) ).
cnf(c_0_34,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(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_29,c_0_30]),c_0_31])]),c_0_32]) ).
fof(c_0_35,plain,
! [X2910,X2911] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X2911,X2910)
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X2910,X2911) ),
inference(variable_rename,[status(thm)],[fact_real__le__linear]) ).
fof(c_0_36,plain,
! [X2955,X2956,X2957,X2958] :
( ~ class_Orderings_Opreorder(X2958)
| ~ c_Orderings_Oord__class_Oless__eq(X2958,X2957,X2956)
| ~ c_Orderings_Oord__class_Oless__eq(X2958,X2956,X2955)
| c_Orderings_Oord__class_Oless__eq(X2958,X2957,X2955) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_order__trans])]) ).
cnf(c_0_37,plain,
~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z____),c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,v_r____)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_33,c_0_34])]) ).
cnf(c_0_38,plain,
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X2)
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X2,X1) ),
inference(split_conjunct,[status(thm)],[c_0_35]) ).
fof(c_0_39,plain,
! [X3087,X3088] :
( ~ class_Groups_Oordered__ab__group__add__abs(X3088)
| c_Orderings_Oord__class_Oless__eq(X3088,X3087,c_Groups_Oabs__class_Oabs(X3088,X3087)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_abs__ge__self])]) ).
fof(c_0_40,negated_conjecture,
~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_r____,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z____)),
inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[conj_0])]) ).
cnf(c_0_41,plain,
( c_Orderings_Oord__class_Oless__eq(X1,X2,X4)
| ~ class_Orderings_Opreorder(X1)
| ~ c_Orderings_Oord__class_Oless__eq(X1,X2,X3)
| ~ c_Orderings_Oord__class_Oless__eq(X1,X3,X4) ),
inference(split_conjunct,[status(thm)],[c_0_36]) ).
cnf(c_0_42,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,v_r____),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z____)),
inference(spm,[status(thm)],[c_0_37,c_0_38]) ).
cnf(c_0_43,plain,
( c_Orderings_Oord__class_Oless__eq(X1,X2,c_Groups_Oabs__class_Oabs(X1,X2))
| ~ class_Groups_Oordered__ab__group__add__abs(X1) ),
inference(split_conjunct,[status(thm)],[c_0_39]) ).
cnf(c_0_44,plain,
class_Groups_Oordered__ab__group__add__abs(tc_RealDef_Oreal),
inference(split_conjunct,[status(thm)],[arity_RealDef__Oreal__Groups_Oordered__ab__group__add__abs]) ).
cnf(c_0_45,negated_conjecture,
~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_r____,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z____)),
inference(split_conjunct,[status(thm)],[c_0_40]) ).
cnf(c_0_46,plain,
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_z____))
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,v_r____)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_41,c_0_42]),c_0_22])]) ).
cnf(c_0_47,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X1)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_43,c_0_19]),c_0_44])]) ).
cnf(c_0_48,negated_conjecture,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_45,c_0_46]),c_0_47])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWW233+1 : TPTP v9.2.1. Released v5.2.0.
% 0.00/0.12 % Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.15/0.33 % Computer : n005.cluster.edu
% 0.15/0.33 % Model : x86_64 x86_64
% 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33 % Memory : 8042.1875MB
% 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.34 % CPULimit : 300
% 0.15/0.34 % WCLimit : 300
% 0.15/0.34 % DateTime : Tue May 5 06:28:00 EDT 2026
% 0.15/0.34 % CPUTime :
% 0.15/0.35 % start to proof: theBenchmark
% 16.52/10.62 % Version : CSE_E---1.7
% 16.52/10.62 % Problem : theBenchmark.p
% 16.52/10.62 % SZS status Theorem for theBenchmark.p
% 16.52/10.62 % SZS output start CNFRefutation
% See solution above
% 16.52/10.69 % Total time : 7.622s
%------------------------------------------------------------------------------