%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : SWW204+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:29:30 PM UTC 2026
% Result : Theorem 11.62s 7.73s
% Output : CNFRefutation 11.62s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 12
% Syntax : Number of formulae : 43 ( 24 unt; 0 def)
% Number of atoms : 84 ( 17 equ)
% Maximal formula atoms : 10 ( 1 avg)
% Number of connectives : 71 ( 30 ~; 30 |; 3 &)
% ( 1 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 7 con; 0-2 aty)
% Number of variables : 51 ( 4 sgn 30 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(conj_0,conjecture,
hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),v_r)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
fof(fact_complex__Re__i,axiom,
hAPP(c_Complex_ORe,c_Complex_Oii) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_complex__Re__i) ).
fof(fact_real__le__linear,axiom,
! [X7,X8] :
( hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X8),X7))
| hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X7),X8)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_real__le__linear) ).
fof(fact_xt1_I6_J,axiom,
! [X8,X4,X13,X5] :
( class_Orderings_Oorder(X5)
=> ( hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(X5,X13),X4))
=> ( hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(X5,X8),X13))
=> hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(X5,X8),X4)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_xt1_I6_J) ).
fof(fact_abs__ge__zero,axiom,
! [X17,X5] :
( class_Groups_Oordered__ab__group__add__abs(X5)
=> hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(X5,c_Groups_Ozero__class_Ozero(X5)),c_Groups_Oabs__class_Oabs(X5,X17))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_abs__ge__zero) ).
fof(fact_real__norm__def,axiom,
! [X45] : c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X45) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X45),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_real__norm__def) ).
fof(arity_RealDef__Oreal__Orderings_Oorder,axiom,
class_Orderings_Oorder(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_RealDef__Oreal__Orderings_Oorder) ).
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(fact_order__eq__iff,axiom,
! [X14,X15,X5] :
( class_Orderings_Oorder(X5)
=> ( X15 = X14
<=> ( hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(X5,X15),X14))
& hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(X5,X14),X15)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_order__eq__iff) ).
fof(fact_abs__of__nonneg,axiom,
! [X17,X5] :
( class_Groups_Oordered__ab__group__add__abs(X5)
=> ( hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(X5,c_Groups_Ozero__class_Ozero(X5)),X17))
=> c_Groups_Oabs__class_Oabs(X5,X17) = X17 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_abs__of__nonneg) ).
fof(fact__0960_A_060_061_Acmod_A_Is_A0_J_096,axiom,
hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(v_s,c_Groups_Ozero__class_Ozero(tc_Nat_Onat))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact__0960_A_060_061_Acmod_A_Is_A0_J_096) ).
fof(fact_assms,axiom,
! [X6] : hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(v_s,X6))),v_r)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_assms) ).
fof(c_0_12,negated_conjecture,
~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),v_r)),
inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[conj_0])]) ).
cnf(c_0_13,negated_conjecture,
~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),v_r)),
inference(split_conjunct,[status(thm)],[c_0_12]) ).
cnf(c_0_14,plain,
hAPP(c_Complex_ORe,c_Complex_Oii) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(split_conjunct,[status(thm)],[fact_complex__Re__i]) ).
fof(c_0_15,plain,
! [X2834,X2835] :
( hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X2835),X2834))
| hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X2834),X2835)) ),
inference(variable_rename,[status(thm)],[fact_real__le__linear]) ).
fof(c_0_16,plain,
! [X2864,X2865,X2866,X2867] :
( ~ class_Orderings_Oorder(X2867)
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(X2867,X2866),X2865))
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(X2867,X2864),X2866))
| hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(X2867,X2864),X2865)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_xt1_I6_J])]) ).
cnf(c_0_17,negated_conjecture,
~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(c_Complex_ORe,c_Complex_Oii)),v_r)),
inference(rw,[status(thm)],[c_0_13,c_0_14]) ).
cnf(c_0_18,plain,
( hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1),X2))
| hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X2),X1)) ),
inference(split_conjunct,[status(thm)],[c_0_15]) ).
fof(c_0_19,plain,
! [X5355,X5356] :
( ~ class_Groups_Oordered__ab__group__add__abs(X5356)
| hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(X5356,c_Groups_Ozero__class_Ozero(X5356)),c_Groups_Oabs__class_Oabs(X5356,X5355))) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_abs__ge__zero])]) ).
fof(c_0_20,plain,
! [X5334] : c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X5334) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X5334),
inference(variable_rename,[status(thm)],[fact_real__norm__def]) ).
cnf(c_0_21,plain,
( hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(X1,X4),X3))
| ~ class_Orderings_Oorder(X1)
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(X1,X2),X3))
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(X1,X4),X2)) ),
inference(split_conjunct,[status(thm)],[c_0_16]) ).
cnf(c_0_22,negated_conjecture,
hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_r),hAPP(c_Complex_ORe,c_Complex_Oii))),
inference(spm,[status(thm)],[c_0_17,c_0_18]) ).
cnf(c_0_23,plain,
class_Orderings_Oorder(tc_RealDef_Oreal),
inference(split_conjunct,[status(thm)],[arity_RealDef__Oreal__Orderings_Oorder]) ).
cnf(c_0_24,plain,
( hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(X1,c_Groups_Ozero__class_Ozero(X1)),c_Groups_Oabs__class_Oabs(X1,X2)))
| ~ class_Groups_Oordered__ab__group__add__abs(X1) ),
inference(split_conjunct,[status(thm)],[c_0_19]) ).
cnf(c_0_25,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_20]) ).
cnf(c_0_26,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]) ).
fof(c_0_27,plain,
! [X2850,X2851,X2852] :
( ( hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(X2852,X2851),X2850))
| X2851 != X2850
| ~ class_Orderings_Oorder(X2852) )
& ( hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(X2852,X2850),X2851))
| X2851 != X2850
| ~ class_Orderings_Oorder(X2852) )
& ( ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(X2852,X2851),X2850))
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(X2852,X2850),X2851))
| X2851 = X2850
| ~ class_Orderings_Oorder(X2852) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_order__eq__iff])])]) ).
cnf(c_0_28,negated_conjecture,
( hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_r),X1))
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(c_Complex_ORe,c_Complex_Oii)),X1)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_21,c_0_22]),c_0_23])]) ).
cnf(c_0_29,plain,
hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(c_Complex_ORe,c_Complex_Oii)),c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X1))),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_24,c_0_25]),c_0_14]),c_0_26])]) ).
fof(c_0_30,plain,
! [X5351,X5352] :
( ~ class_Groups_Oordered__ab__group__add__abs(X5352)
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(X5352,c_Groups_Ozero__class_Ozero(X5352)),X5351))
| c_Groups_Oabs__class_Oabs(X5352,X5351) = X5351 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_abs__of__nonneg])]) ).
cnf(c_0_31,plain,
( X2 = X3
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(X1,X2),X3))
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(X1,X3),X2))
| ~ class_Orderings_Oorder(X1) ),
inference(split_conjunct,[status(thm)],[c_0_27]) ).
cnf(c_0_32,negated_conjecture,
hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_r),c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X1))),
inference(spm,[status(thm)],[c_0_28,c_0_29]) ).
cnf(c_0_33,plain,
( c_Groups_Oabs__class_Oabs(X1,X2) = X2
| ~ class_Groups_Oordered__ab__group__add__abs(X1)
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(X1,c_Groups_Ozero__class_Ozero(X1)),X2)) ),
inference(split_conjunct,[status(thm)],[c_0_30]) ).
cnf(c_0_34,negated_conjecture,
( c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X1) = v_r
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X1)),v_r)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_31,c_0_32]),c_0_23])]) ).
cnf(c_0_35,plain,
( c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X1) = X1
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(c_Complex_ORe,c_Complex_Oii)),X1)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_33,c_0_14]),c_0_25]),c_0_26])]) ).
cnf(c_0_36,plain,
hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(v_s,c_Groups_Ozero__class_Ozero(tc_Nat_Onat))))),
inference(split_conjunct,[status(thm)],[fact__0960_A_060_061_Acmod_A_Is_A0_J_096]) ).
fof(c_0_37,plain,
! [X2832] : hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(v_s,X2832))),v_r)),
inference(variable_rename,[status(thm)],[fact_assms]) ).
cnf(c_0_38,negated_conjecture,
( X1 = v_r
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(c_Complex_ORe,c_Complex_Oii)),X1))
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1),v_r)) ),
inference(spm,[status(thm)],[c_0_34,c_0_35]) ).
cnf(c_0_39,plain,
hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(c_Complex_ORe,c_Complex_Oii)),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(v_s,c_Groups_Ozero__class_Ozero(tc_Nat_Onat))))),
inference(rw,[status(thm)],[c_0_36,c_0_14]) ).
cnf(c_0_40,plain,
hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(v_s,X1))),v_r)),
inference(split_conjunct,[status(thm)],[c_0_37]) ).
cnf(c_0_41,negated_conjecture,
c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(v_s,c_Groups_Ozero__class_Ozero(tc_Nat_Onat))) = v_r,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_38,c_0_39]),c_0_40])]) ).
cnf(c_0_42,plain,
$false,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_39,c_0_41]),c_0_17]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWW204+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.14/0.32 % Computer : n005.cluster.edu
% 0.14/0.32 % Model : x86_64 x86_64
% 0.14/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.32 % Memory : 8042.1875MB
% 0.14/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.32 % CPULimit : 300
% 0.14/0.32 % WCLimit : 300
% 0.14/0.32 % DateTime : Tue May 5 06:25:00 EDT 2026
% 0.14/0.33 % CPUTime :
% 0.14/0.34 % start to proof: theBenchmark
% 11.62/7.73 % Version : CSE_E---1.7
% 11.62/7.73 % Problem : theBenchmark.p
% 11.62/7.73 % SZS status Theorem for theBenchmark.p
% 11.62/7.73 % SZS output start CNFRefutation
% See solution above
% 11.62/7.77 % Total time : 5.597s
%------------------------------------------------------------------------------