%------------------------------------------------------------------------------
% File : Enigma---0.5.1
% Problem : SWW180+1 : TPTP v8.1.0. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : enigmatic-eprover.py %s %d 1
% Computer : n018.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 : 600s
% DateTime : Thu Jul 21 00:01:41 EDT 2022
% Result : Theorem 14.22s 3.55s
% Output : CNFRefutation 14.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 39
% Syntax : Number of clauses : 125 ( 60 unt; 18 nHn; 79 RR)
% Number of literals : 219 ( 74 equ; 88 neg)
% Maximal clause size : 4 ( 1 avg)
% Maximal term depth : 7 ( 1 avg)
% Number of predicates : 12 ( 10 usr; 1 prp; 0-3 aty)
% Number of functors : 17 ( 17 usr; 7 con; 0-3 aty)
% Number of variables : 150 ( 11 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(i_0_1363,plain,
( c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X2)) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)
| X1 != X2 ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-kmv3sf_4/lgb.p',i_0_1363) ).
cnf(i_0_353,plain,
( X1 = c_Groups_Ozero__class_Ozero(X2)
| c_Groups_Oplus__class_Oplus(X2,X3,X1) != X3
| ~ class_Semiring__Normalization_Ocomm__semiring__1__cancel__crossproduct(X2) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-kmv3sf_4/lgb.p',i_0_353) ).
cnf(i_0_277,plain,
class_Semiring__Normalization_Ocomm__semiring__1__cancel__crossproduct(tc_RealDef_Oreal),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-kmv3sf_4/lgb.p',i_0_277) ).
cnf(i_0_330,plain,
( ~ class_Groups_Oordered__ab__group__add__abs(X1)
| ~ c_Orderings_Oord__class_Oless(X1,c_Groups_Oabs__class_Oabs(X1,X2),c_Groups_Ozero__class_Ozero(X1)) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-kmv3sf_4/lgb.p',i_0_330) ).
cnf(i_0_831,plain,
( c_Orderings_Oord__class_Oless__eq(X1,X2,X3)
| c_Orderings_Oord__class_Oless(X1,X3,X2)
| ~ class_Orderings_Olinorder(X1) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-kmv3sf_4/lgb.p',i_0_831) ).
cnf(i_0_856,plain,
c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X2)) = c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X1,X2),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-kmv3sf_4/lgb.p',i_0_856) ).
cnf(i_0_500,plain,
( c_Groups_Ominus__class_Ominus(X1,X2,c_Groups_Ozero__class_Ozero(X1)) = X2
| ~ class_Groups_Ogroup__add(X1) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-kmv3sf_4/lgb.p',i_0_500) ).
cnf(i_0_222,plain,
class_Groups_Ogroup__add(tc_RealDef_Oreal),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-kmv3sf_4/lgb.p',i_0_222) ).
cnf(i_0_1182,plain,
( ~ class_Rings_Olinordered__semidom(X1)
| ~ c_Orderings_Oord__class_Oless(X1,c_Groups_Oone__class_Oone(X1),c_Groups_Ozero__class_Ozero(X1)) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-kmv3sf_4/lgb.p',i_0_1182) ).
cnf(i_0_460,plain,
( c_Groups_Oplus__class_Oplus(X1,X2,X3) = c_Groups_Oplus__class_Oplus(X1,X3,X2)
| ~ class_Rings_Ocomm__semiring__1(X1) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-kmv3sf_4/lgb.p',i_0_460) ).
cnf(i_0_250,plain,
class_Rings_Ocomm__semiring__1(tc_RealDef_Oreal),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-kmv3sf_4/lgb.p',i_0_250) ).
cnf(i_0_1360,plain,
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,X2),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,X3))
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X2,X3) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-kmv3sf_4/lgb.p',i_0_1360) ).
cnf(i_0_228,plain,
class_Groups_Oordered__ab__group__add__abs(tc_RealDef_Oreal),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-kmv3sf_4/lgb.p',i_0_228) ).
cnf(i_0_238,plain,
class_Orderings_Olinorder(tc_RealDef_Oreal),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-kmv3sf_4/lgb.p',i_0_238) ).
cnf(i_0_332,plain,
( c_Groups_Oabs__class_Oabs(X1,X2) = X2
| ~ class_Groups_Oordered__ab__group__add__abs(X1)
| ~ c_Orderings_Oord__class_Oless__eq(X1,c_Groups_Ozero__class_Ozero(X1),X2) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-kmv3sf_4/lgb.p',i_0_332) ).
cnf(i_0_278,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____)))),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-kmv3sf_4/lgb.p',i_0_278) ).
cnf(i_0_258,plain,
class_Rings_Olinordered__semidom(tc_RealDef_Oreal),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-kmv3sf_4/lgb.p',i_0_258) ).
cnf(i_0_1443,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),v_r),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-kmv3sf_4/lgb.p',i_0_1443) ).
cnf(i_0_458,plain,
( c_Groups_Oplus__class_Oplus(X1,X2,c_Groups_Oplus__class_Oplus(X1,X3,X4)) = c_Groups_Oplus__class_Oplus(X1,X3,c_Groups_Oplus__class_Oplus(X1,X2,X4))
| ~ class_Rings_Ocomm__semiring__1(X1) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-kmv3sf_4/lgb.p',i_0_458) ).
cnf(i_0_1370,plain,
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X2)
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X2,X1) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-kmv3sf_4/lgb.p',i_0_1370) ).
cnf(i_0_1375,plain,
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X2)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X3,X2)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X3) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-kmv3sf_4/lgb.p',i_0_1375) ).
cnf(i_0_885,plain,
( c_Orderings_Oord__class_Oless__eq(X1,X2,c_Groups_Ozero__class_Ozero(X1))
| c_Orderings_Oord__class_Oless__eq(X1,X3,c_Groups_Ozero__class_Ozero(X1))
| ~ class_Rings_Olinordered__ring__strict(X1)
| ~ c_Orderings_Oord__class_Oless__eq(X1,hAPP(hAPP(c_Groups_Otimes__class_Otimes(X1),X3),X2),c_Groups_Ozero__class_Ozero(X1)) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-kmv3sf_4/lgb.p',i_0_885) ).
cnf(i_0_257,plain,
class_Rings_Olinordered__ring__strict(tc_RealDef_Oreal),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-kmv3sf_4/lgb.p',i_0_257) ).
cnf(i_0_474,plain,
( c_Groups_Oplus__class_Oplus(X1,c_Groups_Ozero__class_Ozero(X1),X2) = X2
| ~ class_Rings_Ocomm__semiring__1(X1) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-kmv3sf_4/lgb.p',i_0_474) ).
cnf(i_0_1556,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_cs____),v_z____)),v_m____),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-kmv3sf_4/lgb.p',i_0_1556) ).
cnf(i_0_830,plain,
( ~ class_Orderings_Olinorder(X1)
| ~ c_Orderings_Oord__class_Oless__eq(X1,X2,X3)
| ~ c_Orderings_Oord__class_Oless(X1,X3,X2) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-kmv3sf_4/lgb.p',i_0_830) ).
cnf(i_0_1638,plain,
( X1 = c_Groups_Ozero__class_Ozero(X2)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(X2,X1))
| ~ class_RealVector_Oreal__normed__vector(X2) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-kmv3sf_4/lgb.p',i_0_1638) ).
cnf(i_0_1149,plain,
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(X1,X2))
| ~ class_RealVector_Oreal__normed__vector(X1) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-kmv3sf_4/lgb.p',i_0_1149) ).
cnf(i_0_22,plain,
class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-kmv3sf_4/lgb.p',i_0_22) ).
cnf(i_0_759,plain,
( X1 = X2
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X1,X2)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X2) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-kmv3sf_4/lgb.p',i_0_759) ).
cnf(i_0_1395,plain,
c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X1) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X1),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-kmv3sf_4/lgb.p',i_0_1395) ).
cnf(i_0_246,plain,
class_RealVector_Oreal__normed__vector(tc_RealDef_Oreal),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-kmv3sf_4/lgb.p',i_0_246) ).
cnf(i_0_478,plain,
( hAPP(hAPP(c_Groups_Otimes__class_Otimes(X1),c_Groups_Ozero__class_Ozero(X1)),X2) = c_Groups_Ozero__class_Ozero(X1)
| ~ class_Rings_Ocomm__semiring__1(X1) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-kmv3sf_4/lgb.p',i_0_478) ).
cnf(i_0_333,plain,
( c_Groups_Ouminus__class_Ouminus(X1,X2) = c_Groups_Oabs__class_Oabs(X1,X2)
| ~ class_Groups_Oordered__ab__group__add__abs(X1)
| ~ c_Orderings_Oord__class_Oless__eq(X1,X2,c_Groups_Ozero__class_Ozero(X1)) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-kmv3sf_4/lgb.p',i_0_333) ).
cnf(i_0_321,plain,
c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X2))) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X2,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X1))),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-kmv3sf_4/lgb.p',i_0_321) ).
cnf(i_0_1367,plain,
( X1 = X2
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X2,X1)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X2) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-kmv3sf_4/lgb.p',i_0_1367) ).
cnf(i_0_1440,plain,
( c_Groups_Oplus__class_Oplus(X1,X2,c_Groups_Ouminus__class_Ouminus(X1,X2)) = c_Groups_Ozero__class_Ozero(X1)
| ~ class_Groups_Ogroup__add(X1) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-kmv3sf_4/lgb.p',i_0_1440) ).
cnf(i_0_296,plain,
( X1 = c_Groups_Ozero__class_Ozero(X2)
| c_Groups_Oabs__class_Oabs(X2,X1) != c_Groups_Ozero__class_Ozero(X2)
| ~ class_Groups_Oordered__ab__group__add__abs(X2) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-kmv3sf_4/lgb.p',i_0_296) ).
cnf(i_0_1379,plain,
hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X1),X2) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X2),X1),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-kmv3sf_4/lgb.p',i_0_1379) ).
cnf(c_0_1678,plain,
( c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X2)) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)
| X1 != X2 ),
i_0_1363 ).
cnf(c_0_1679,plain,
( X1 = c_Groups_Ozero__class_Ozero(X2)
| c_Groups_Oplus__class_Oplus(X2,X3,X1) != X3
| ~ class_Semiring__Normalization_Ocomm__semiring__1__cancel__crossproduct(X2) ),
i_0_353 ).
cnf(c_0_1680,plain,
c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X1)) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(er,[status(thm)],[c_0_1678]) ).
cnf(c_0_1681,plain,
class_Semiring__Normalization_Ocomm__semiring__1__cancel__crossproduct(tc_RealDef_Oreal),
i_0_277 ).
cnf(c_0_1682,plain,
( ~ class_Groups_Oordered__ab__group__add__abs(X1)
| ~ c_Orderings_Oord__class_Oless(X1,c_Groups_Oabs__class_Oabs(X1,X2),c_Groups_Ozero__class_Ozero(X1)) ),
i_0_330 ).
cnf(c_0_1683,plain,
( c_Orderings_Oord__class_Oless__eq(X1,X2,X3)
| c_Orderings_Oord__class_Oless(X1,X3,X2)
| ~ class_Orderings_Olinorder(X1) ),
i_0_831 ).
cnf(c_0_1684,plain,
c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X2)) = c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X1,X2),
i_0_856 ).
cnf(c_0_1685,plain,
( c_Groups_Ominus__class_Ominus(X1,X2,c_Groups_Ozero__class_Ozero(X1)) = X2
| ~ class_Groups_Ogroup__add(X1) ),
i_0_500 ).
cnf(c_0_1686,plain,
c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(er,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1679,c_0_1680]),c_0_1681])])]) ).
cnf(c_0_1687,plain,
class_Groups_Ogroup__add(tc_RealDef_Oreal),
i_0_222 ).
cnf(c_0_1688,plain,
( ~ class_Rings_Olinordered__semidom(X1)
| ~ c_Orderings_Oord__class_Oless(X1,c_Groups_Oone__class_Oone(X1),c_Groups_Ozero__class_Ozero(X1)) ),
i_0_1182 ).
cnf(c_0_1689,plain,
( c_Groups_Oplus__class_Oplus(X1,X2,X3) = c_Groups_Oplus__class_Oplus(X1,X3,X2)
| ~ class_Rings_Ocomm__semiring__1(X1) ),
i_0_460 ).
cnf(c_0_1690,plain,
class_Rings_Ocomm__semiring__1(tc_RealDef_Oreal),
i_0_250 ).
cnf(c_0_1691,plain,
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,X2),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,X3))
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X2,X3) ),
i_0_1360 ).
cnf(c_0_1692,plain,
( 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)
| ~ class_Orderings_Olinorder(X1) ),
inference(spm,[status(thm)],[c_0_1682,c_0_1683]) ).
cnf(c_0_1693,plain,
c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)) = X1,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1684,c_0_1685]),c_0_1686]),c_0_1687])]) ).
cnf(c_0_1694,plain,
class_Groups_Oordered__ab__group__add__abs(tc_RealDef_Oreal),
i_0_228 ).
cnf(c_0_1695,plain,
class_Orderings_Olinorder(tc_RealDef_Oreal),
i_0_238 ).
cnf(c_0_1696,plain,
( c_Groups_Oabs__class_Oabs(X1,X2) = X2
| ~ class_Groups_Oordered__ab__group__add__abs(X1)
| ~ c_Orderings_Oord__class_Oless__eq(X1,c_Groups_Ozero__class_Ozero(X1),X2) ),
i_0_332 ).
cnf(c_0_1697,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)
| ~ class_Orderings_Olinorder(X1) ),
inference(spm,[status(thm)],[c_0_1688,c_0_1683]) ).
cnf(c_0_1698,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____)))),
i_0_278 ).
cnf(c_0_1699,plain,
c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,X2) = c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X2,X1),
inference(spm,[status(thm)],[c_0_1689,c_0_1690]) ).
cnf(c_0_1700,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X2))),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1691,c_0_1692]),c_0_1693]),c_0_1694]),c_0_1695])]) ).
cnf(c_0_1701,plain,
( c_Groups_Oabs__class_Oabs(X1,c_Groups_Oone__class_Oone(X1)) = c_Groups_Oone__class_Oone(X1)
| ~ class_Rings_Olinordered__semidom(X1)
| ~ class_Groups_Oordered__ab__group__add__abs(X1)
| ~ class_Orderings_Olinorder(X1) ),
inference(spm,[status(thm)],[c_0_1696,c_0_1697]) ).
cnf(c_0_1702,plain,
class_Rings_Olinordered__semidom(tc_RealDef_Oreal),
i_0_258 ).
cnf(c_0_1703,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),v_r),
i_0_1443 ).
cnf(c_0_1704,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_Oabs__class_Oabs(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_r),v_m____)),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(rw,[status(thm)],[c_0_1698,c_0_1699]) ).
cnf(c_0_1705,plain,
( c_Groups_Oplus__class_Oplus(X1,X2,c_Groups_Oplus__class_Oplus(X1,X3,X4)) = c_Groups_Oplus__class_Oplus(X1,X3,c_Groups_Oplus__class_Oplus(X1,X2,X4))
| ~ class_Rings_Ocomm__semiring__1(X1) ),
i_0_458 ).
cnf(c_0_1706,plain,
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X2)
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X2,X1) ),
i_0_1370 ).
cnf(c_0_1707,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,c_Groups_Oone__class_Oone(tc_RealDef_Oreal))),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1700,c_0_1701]),c_0_1702]),c_0_1694]),c_0_1695])]) ).
cnf(c_0_1708,plain,
c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,v_r) = v_r,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1696,c_0_1703]),c_0_1694])]) ).
cnf(c_0_1709,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_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Oplus__class_Oplus(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(rw,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1704,c_0_1705]),c_0_1690])]),c_0_1699]) ).
cnf(c_0_1710,plain,
( c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X1) = X1
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1696,c_0_1706]),c_0_1694])]) ).
cnf(c_0_1711,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),X1)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1707,c_0_1689]),c_0_1690])]) ).
cnf(c_0_1712,plain,
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X2)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X3,X2)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X3) ),
i_0_1375 ).
cnf(c_0_1713,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,v_r)),
inference(spm,[status(thm)],[c_0_1700,c_0_1708]) ).
cnf(c_0_1714,plain,
( c_Orderings_Oord__class_Oless__eq(X1,X2,c_Groups_Ozero__class_Ozero(X1))
| c_Orderings_Oord__class_Oless__eq(X1,X3,c_Groups_Ozero__class_Ozero(X1))
| ~ class_Rings_Olinordered__ring__strict(X1)
| ~ c_Orderings_Oord__class_Oless__eq(X1,hAPP(hAPP(c_Groups_Otimes__class_Otimes(X1),X3),X2),c_Groups_Ozero__class_Ozero(X1)) ),
i_0_885 ).
cnf(c_0_1715,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_Ozero__class_Ozero(tc_RealDef_Oreal)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1709,c_0_1710]),c_0_1711])]) ).
cnf(c_0_1716,plain,
class_Rings_Olinordered__ring__strict(tc_RealDef_Oreal),
i_0_257 ).
cnf(c_0_1717,plain,
( c_Groups_Oplus__class_Oplus(X1,c_Groups_Ozero__class_Ozero(X1),X2) = X2
| ~ class_Rings_Ocomm__semiring__1(X1) ),
i_0_474 ).
cnf(c_0_1718,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_cs____),v_z____)),v_m____),
i_0_1556 ).
cnf(c_0_1719,plain,
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X2,v_r))
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X2) ),
inference(spm,[status(thm)],[c_0_1712,c_0_1713]) ).
cnf(c_0_1720,plain,
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_m____,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_r,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1714,c_0_1715]),c_0_1716])]) ).
cnf(c_0_1721,plain,
c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),X1) = X1,
inference(spm,[status(thm)],[c_0_1717,c_0_1690]) ).
cnf(c_0_1722,plain,
( ~ class_Orderings_Olinorder(X1)
| ~ c_Orderings_Oord__class_Oless__eq(X1,X2,X3)
| ~ c_Orderings_Oord__class_Oless(X1,X3,X2) ),
i_0_830 ).
cnf(c_0_1723,plain,
( X1 = c_Groups_Ozero__class_Ozero(X2)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(X2,X1))
| ~ class_RealVector_Oreal__normed__vector(X2) ),
i_0_1638 ).
cnf(c_0_1724,plain,
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,v_m____)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_cs____),v_z____))) ),
inference(spm,[status(thm)],[c_0_1712,c_0_1718]) ).
cnf(c_0_1725,plain,
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(X1,X2))
| ~ class_RealVector_Oreal__normed__vector(X1) ),
i_0_1149 ).
cnf(c_0_1726,plain,
class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex),
i_0_22 ).
cnf(c_0_1727,plain,
( X1 = X2
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X1,X2)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X2) ),
i_0_759 ).
cnf(c_0_1728,plain,
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_r,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_m____,v_r) ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1719,c_0_1720]),c_0_1721]) ).
cnf(c_0_1729,plain,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,v_r,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1682,c_0_1708]),c_0_1694])]) ).
cnf(c_0_1730,plain,
( X1 = c_Groups_Ozero__class_Ozero(X2)
| ~ class_RealVector_Oreal__normed__vector(X2)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(X2,X1),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1722,c_0_1723]),c_0_1695])]) ).
cnf(c_0_1731,plain,
c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X1) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X1),
i_0_1395 ).
cnf(c_0_1732,plain,
class_RealVector_Oreal__normed__vector(tc_RealDef_Oreal),
i_0_246 ).
cnf(c_0_1733,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),v_m____),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1724,c_0_1725]),c_0_1726])]) ).
cnf(c_0_1734,plain,
( hAPP(hAPP(c_Groups_Otimes__class_Otimes(X1),c_Groups_Ozero__class_Ozero(X1)),X2) = c_Groups_Ozero__class_Ozero(X1)
| ~ class_Rings_Ocomm__semiring__1(X1) ),
i_0_478 ).
cnf(c_0_1735,plain,
( c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) = v_r
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_m____,v_r) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1727,c_0_1728]),c_0_1729]) ).
cnf(c_0_1736,plain,
( X1 = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X1),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1730,c_0_1731]),c_0_1732])]) ).
cnf(c_0_1737,plain,
c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,v_m____) = v_m____,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1696,c_0_1733]),c_0_1694])]) ).
cnf(c_0_1738,plain,
( hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_r),X1) = v_r
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_m____,v_r) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1734,c_0_1735]),c_0_1690])]) ).
cnf(c_0_1739,plain,
( c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) = v_m____
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_m____,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)) ),
inference(spm,[status(thm)],[c_0_1736,c_0_1737]) ).
cnf(c_0_1740,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_m____,v_r),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1709,c_0_1738]),c_0_1708]),c_0_1711])]) ).
cnf(c_0_1741,plain,
( c_Groups_Ouminus__class_Ouminus(X1,X2) = c_Groups_Oabs__class_Oabs(X1,X2)
| ~ class_Groups_Oordered__ab__group__add__abs(X1)
| ~ c_Orderings_Oord__class_Oless__eq(X1,X2,c_Groups_Ozero__class_Ozero(X1)) ),
i_0_333 ).
cnf(c_0_1742,plain,
( c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) = v_m____
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_r,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)) ),
inference(spm,[status(thm)],[c_0_1739,c_0_1720]) ).
cnf(c_0_1743,plain,
c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X2))) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X2,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X1))),
i_0_321 ).
cnf(c_0_1744,plain,
( X1 = X2
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X2,X1)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X2) ),
i_0_1367 ).
cnf(c_0_1745,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_m____,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,v_r,v_r)),
inference(spm,[status(thm)],[c_0_1719,c_0_1740]) ).
cnf(c_0_1746,plain,
( c_Groups_Oplus__class_Oplus(X1,X2,c_Groups_Ouminus__class_Ouminus(X1,X2)) = c_Groups_Ozero__class_Ozero(X1)
| ~ class_Groups_Ogroup__add(X1) ),
i_0_1440 ).
cnf(c_0_1747,plain,
( c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_r) = v_r
| c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) = v_m____ ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1741,c_0_1742]),c_0_1708]),c_0_1694])]) ).
cnf(c_0_1748,plain,
( X1 = c_Groups_Ozero__class_Ozero(X2)
| c_Groups_Oabs__class_Oabs(X2,X1) != c_Groups_Ozero__class_Ozero(X2)
| ~ class_Groups_Oordered__ab__group__add__abs(X2) ),
i_0_296 ).
cnf(c_0_1749,plain,
c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X1)) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1743,c_0_1717]),c_0_1686]),c_0_1693]),c_0_1690])]) ).
cnf(c_0_1750,plain,
hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X1),X2) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X2),X1),
i_0_1379 ).
cnf(c_0_1751,plain,
( c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,v_r,v_r) = v_m____
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,v_r,v_r),v_m____) ),
inference(spm,[status(thm)],[c_0_1744,c_0_1745]) ).
cnf(c_0_1752,plain,
( c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,v_r,v_r) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)
| c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) = v_m____ ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1746,c_0_1747]),c_0_1687])]) ).
cnf(c_0_1753,plain,
( c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X1) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)
| c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X1) != c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1748,c_0_1749]),c_0_1694])]) ).
cnf(c_0_1754,plain,
c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_r),v_m____)) = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_r),v_m____)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1741,c_0_1715]),c_0_1694])]) ).
cnf(c_0_1755,plain,
hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X1),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1750,c_0_1734]),c_0_1690])]) ).
cnf(c_0_1756,plain,
c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) = v_m____,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1751,c_0_1752]),c_0_1733])]) ).
cnf(c_0_1757,plain,
( c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_m____) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)
| c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) != v_m____ ),
inference(spm,[status(thm)],[c_0_1753,c_0_1737]) ).
cnf(c_0_1758,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_Ouminus__class_Ouminus(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_r),v_m____)),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(rw,[status(thm)],[c_0_1704,c_0_1754]) ).
cnf(c_0_1759,plain,
hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X1),v_m____) = v_m____,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_1755,c_0_1756]),c_0_1756]) ).
cnf(c_0_1760,plain,
c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,v_m____) = X1,
inference(rw,[status(thm)],[c_0_1693,c_0_1756]) ).
cnf(c_0_1761,plain,
c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_m____) = v_m____,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_1757,c_0_1756]),c_0_1756])]) ).
cnf(c_0_1762,plain,
c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,v_m____,X1) = X1,
inference(rw,[status(thm)],[c_0_1721,c_0_1756]) ).
cnf(c_0_1763,negated_conjecture,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_1758,c_0_1759]),c_0_1760]),c_0_1759]),c_0_1761]),c_0_1762]),c_0_1711])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SWW180+1 : TPTP v8.1.0. Released v5.2.0.
% 0.03/0.12 % Command : enigmatic-eprover.py %s %d 1
% 0.12/0.33 % Computer : n018.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 600
% 0.12/0.33 % DateTime : Sun Jun 5 15:19:50 EDT 2022
% 0.12/0.34 % CPUTime :
% 0.19/0.45 # ENIGMATIC: Selected SinE mode:
% 0.19/0.52 # Parsing /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.52 # Filter: axfilter_auto 0 goes into file theBenchmark_axfilter_auto 0.p
% 0.19/0.52 # Filter: axfilter_auto 1 goes into file theBenchmark_axfilter_auto 1.p
% 0.19/0.52 # Filter: axfilter_auto 2 goes into file theBenchmark_axfilter_auto 2.p
% 14.22/3.55 # ENIGMATIC: Solved by autoschedule-lgb:
% 14.22/3.55 # No SInE strategy applied
% 14.22/3.55 # Trying AutoSched0 for 150 seconds
% 14.22/3.55 # AutoSched0-Mode selected heuristic G_E___208_C18_F1_SE_CS_SP_PS_S5PRR_S4d
% 14.22/3.55 # and selection function SelectCQIPrecWNTNp.
% 14.22/3.55 #
% 14.22/3.55 # Preprocessing time : 0.032 s
% 14.22/3.55 # Presaturation interreduction done
% 14.22/3.55
% 14.22/3.55 # Proof found!
% 14.22/3.55 # SZS status Theorem
% 14.22/3.55 # SZS output start CNFRefutation
% See solution above
% 14.22/3.55 # Training examples: 0 positive, 0 negative
% 14.22/3.55
% 14.22/3.55 # -------------------------------------------------
% 14.22/3.55 # User time : 0.603 s
% 14.22/3.55 # System time : 0.021 s
% 14.22/3.55 # Total time : 0.624 s
% 14.22/3.55 # Maximum resident set size: 7388 pages
% 14.22/3.55
%------------------------------------------------------------------------------