%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW180+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n008.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:08:46 PM UTC 2026
% Result : Theorem 23.72s 3.69s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW180+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.05 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.42 % Computer : n008.cluster.edu
% 0.17/0.42 % Model : x86_64 x86_64
% 0.17/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.42 % Memory : 8046.5625MB
% 0.17/0.42 % OS : Linux 6.8.0-71-generic
% 0.17/0.42 % CPULimit : 300
% 0.17/0.42 % WCLimit : 300
% 0.17/0.42 % DateTime : Mon Sep 21 09:41:08 UTC 2026
% 0.17/0.43 % CPUTime :
% 0.28/0.62 % Drodi V4.1.1
% 23.72/3.69 % Refutation found
% 23.72/3.69 % SZS status Theorem for theBenchmark: Theorem is valid
% 23.72/3.69 % SZS output start CNFRefutation for theBenchmark
% 23.72/3.69 fof(f6,axiom,(
% 23.72/3.69 (! [T_a] :( class_RealVector_Oreal__normed__algebra__1(T_a)=> c_RealVector_Onorm__class_Onorm(T_a,c_Groups_Oone__class_Oone(T_a)) = c_Groups_Oone__class_Oone(tc_RealDef_Oreal) ) )),
% 23.72/3.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 23.72/3.69 fof(f19,axiom,(
% 23.72/3.69 (! [V_a,T_a] :( class_Groups_Oordered__ab__group__add__abs(T_a)=> ~ c_Orderings_Oord__class_Oless(T_a,c_Groups_Oabs__class_Oabs(T_a,V_a),c_Groups_Ozero__class_Ozero(T_a)) ) )),
% 23.72/3.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 23.72/3.69 fof(f54,axiom,(
% 23.72/3.69 (! [V_z,V_y,V_x,T_a] :( class_Orderings_Opreorder(T_a)=> ( c_Orderings_Oord__class_Oless(T_a,V_x,V_y)=> ( c_Orderings_Oord__class_Oless__eq(T_a,V_y,V_z)=> c_Orderings_Oord__class_Oless(T_a,V_x,V_z) ) ) ) )),
% 23.72/3.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 23.72/3.69 fof(f60,axiom,(
% 23.72/3.69 (! [V_x,V_y,T_a] :( class_Orderings_Olinorder(T_a)=> ( c_Orderings_Oord__class_Oless__eq(T_a,V_y,V_x)=> ~ c_Orderings_Oord__class_Oless(T_a,V_x,V_y) ) ) )),
% 23.72/3.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 23.72/3.69 fof(f67,axiom,(
% 23.72/3.69 (! [V_y_2,V_x_2,T_a] :( class_Orderings_Opreorder(T_a)=> ( c_Orderings_Oord__class_Oless(T_a,V_x_2,V_y_2)<=> ( c_Orderings_Oord__class_Oless__eq(T_a,V_x_2,V_y_2)& ~ c_Orderings_Oord__class_Oless__eq(T_a,V_y_2,V_x_2) ) ) ) )),
% 23.72/3.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 23.72/3.69 fof(f72,axiom,(
% 23.72/3.69 (! [V_b,V_a,V_c,T_a] :( class_Groups_Oordered__ab__semigroup__add__imp__le(T_a)=> ( c_Orderings_Oord__class_Oless(T_a,c_Groups_Oplus__class_Oplus(T_a,V_c,V_a),c_Groups_Oplus__class_Oplus(T_a,V_c,V_b))=> c_Orderings_Oord__class_Oless(T_a,V_a,V_b) ) ) )),
% 23.72/3.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 23.72/3.69 fof(f73,axiom,(
% 23.72/3.69 (! [V_b,V_c,V_a,T_a] :( class_Groups_Oordered__ab__semigroup__add__imp__le(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_c))=> c_Orderings_Oord__class_Oless(T_a,V_a,V_b) ) ) )),
% 23.72/3.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 23.72/3.69 fof(f90,axiom,(
% 23.72/3.69 (! [V_a,T_a] :( class_Groups_Ocomm__monoid__add(T_a)=> c_Groups_Oplus__class_Oplus(T_a,c_Groups_Ozero__class_Ozero(T_a),V_a) = V_a ) )),
% 23.72/3.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 23.72/3.69 fof(f93,axiom,(
% 23.72/3.69 (! [V_r] : c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,V_r) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,V_r) )),
% 23.72/3.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 23.72/3.69 fof(f200,axiom,(
% 23.72/3.69 (! [V_w,V_z] :( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_z,V_w)| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_w,V_z) ) )),
% 23.72/3.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 23.72/3.69 fof(f203,axiom,(
% 23.72/3.69 (! [V_w,V_z] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),V_z),V_w) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),V_w),V_z) )),
% 23.72/3.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 23.72/3.69 fof(f216,axiom,(
% 23.72/3.69 (! [V_y_2,V_x_2] :( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2,V_y_2)<=> ( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2,V_y_2)& V_x_2 != V_y_2 ) ) )),
% 23.72/3.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 23.72/3.69 fof(f534,axiom,(
% 23.72/3.69 (! [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,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,V_ra_2),V_x_2)& c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2,V_ra_2) ) ) )),
% 23.72/3.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 23.72/3.69 fof(f1112,axiom,(
% 23.72/3.69 class_Groups_Oordered__ab__semigroup__add__imp__le(tc_RealDef_Oreal) ),
% 23.72/3.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 23.72/3.69 fof(f1117,axiom,(
% 23.72/3.69 class_RealVector_Oreal__normed__algebra__1(tc_RealDef_Oreal) ),
% 23.72/3.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 23.72/3.69 fof(f1119,axiom,(
% 23.72/3.69 class_Groups_Oordered__ab__group__add__abs(tc_RealDef_Oreal) ),
% 23.72/3.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 23.72/3.69 fof(f1141,axiom,(
% 23.72/3.69 class_Groups_Ocomm__monoid__add(tc_RealDef_Oreal) ),
% 23.72/3.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 23.72/3.69 fof(f1150,axiom,(
% 23.72/3.69 class_Orderings_Opreorder(tc_RealDef_Oreal) ),
% 23.72/3.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 23.72/3.69 fof(f1151,axiom,(
% 23.72/3.69 class_Orderings_Olinorder(tc_RealDef_Oreal) ),
% 23.72/3.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 23.72/3.69 fof(f1275,conjecture,(
% 23.72/3.69 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____)))) ),
% 23.72/3.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 23.72/3.69 fof(f1276,negated_conjecture,(
% 23.72/3.69 ~(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____)))) )),
% 23.72/3.69 inference(negated_conjecture,[status(cth)],[f1275])).
% 23.72/3.69 fof(f1289,plain,(
% 23.72/3.69 ![T_a]: (~class_RealVector_Oreal__normed__algebra__1(T_a)|c_RealVector_Onorm__class_Onorm(T_a,c_Groups_Oone__class_Oone(T_a))=c_Groups_Oone__class_Oone(tc_RealDef_Oreal))),
% 23.72/3.69 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 23.72/3.69 fof(f1290,plain,(
% 23.72/3.69 ![X0]: (~class_RealVector_Oreal__normed__algebra__1(X0)|c_RealVector_Onorm__class_Onorm(X0,c_Groups_Oone__class_Oone(X0))=c_Groups_Oone__class_Oone(tc_RealDef_Oreal))),
% 23.72/3.69 inference(cnf_transformation,[status(thm)],[f1289])).
% 23.72/3.69 fof(f1320,plain,(
% 23.72/3.69 ![V_a,T_a]: (~class_Groups_Oordered__ab__group__add__abs(T_a)|~c_Orderings_Oord__class_Oless(T_a,c_Groups_Oabs__class_Oabs(T_a,V_a),c_Groups_Ozero__class_Ozero(T_a)))),
% 23.72/3.69 inference(pre_NNF_transformation,[status(thm)],[f19])).
% 23.72/3.69 fof(f1321,plain,(
% 23.72/3.69 ![T_a]: (~class_Groups_Oordered__ab__group__add__abs(T_a)|(![V_a]: ~c_Orderings_Oord__class_Oless(T_a,c_Groups_Oabs__class_Oabs(T_a,V_a),c_Groups_Ozero__class_Ozero(T_a))))),
% 23.72/3.69 inference(miniscoping,[status(thm)],[f1320])).
% 23.72/3.69 fof(f1322,plain,(
% 23.72/3.69 ![X0,X1]: (~class_Groups_Oordered__ab__group__add__abs(X0)|~c_Orderings_Oord__class_Oless(X0,c_Groups_Oabs__class_Oabs(X0,X1),c_Groups_Ozero__class_Ozero(X0)))),
% 23.72/3.69 inference(cnf_transformation,[status(thm)],[f1321])).
% 23.72/3.69 fof(f1444,plain,(
% 23.72/3.69 ![V_z,V_y,V_x,T_a]: (~class_Orderings_Opreorder(T_a)|(~c_Orderings_Oord__class_Oless(T_a,V_x,V_y)|(~c_Orderings_Oord__class_Oless__eq(T_a,V_y,V_z)|c_Orderings_Oord__class_Oless(T_a,V_x,V_z))))),
% 23.72/3.69 inference(pre_NNF_transformation,[status(thm)],[f54])).
% 23.72/3.69 fof(f1445,plain,(
% 23.72/3.69 ![T_a]: (~class_Orderings_Opreorder(T_a)|(![V_y,V_x]: (~c_Orderings_Oord__class_Oless(T_a,V_x,V_y)|(![V_z]: (~c_Orderings_Oord__class_Oless__eq(T_a,V_y,V_z)|c_Orderings_Oord__class_Oless(T_a,V_x,V_z))))))),
% 23.72/3.69 inference(miniscoping,[status(thm)],[f1444])).
% 23.72/3.69 fof(f1446,plain,(
% 23.72/3.69 ![X0,X1,X2,X3]: (~class_Orderings_Opreorder(X0)|~c_Orderings_Oord__class_Oless(X0,X1,X2)|~c_Orderings_Oord__class_Oless__eq(X0,X2,X3)|c_Orderings_Oord__class_Oless(X0,X1,X3))),
% 23.72/3.69 inference(cnf_transformation,[status(thm)],[f1445])).
% 23.72/3.69 fof(f1464,plain,(
% 23.72/3.69 ![V_x,V_y,T_a]: (~class_Orderings_Olinorder(T_a)|(~c_Orderings_Oord__class_Oless__eq(T_a,V_y,V_x)|~c_Orderings_Oord__class_Oless(T_a,V_x,V_y)))),
% 23.72/3.69 inference(pre_NNF_transformation,[status(thm)],[f60])).
% 23.72/3.69 fof(f1465,plain,(
% 23.72/3.69 ![T_a]: (~class_Orderings_Olinorder(T_a)|(![V_x,V_y]: (~c_Orderings_Oord__class_Oless__eq(T_a,V_y,V_x)|~c_Orderings_Oord__class_Oless(T_a,V_x,V_y))))),
% 23.72/3.69 inference(miniscoping,[status(thm)],[f1464])).
% 23.72/3.69 fof(f1466,plain,(
% 23.72/3.69 ![X0,X1,X2]: (~class_Orderings_Olinorder(X0)|~c_Orderings_Oord__class_Oless__eq(X0,X1,X2)|~c_Orderings_Oord__class_Oless(X0,X2,X1))),
% 23.72/3.69 inference(cnf_transformation,[status(thm)],[f1465])).
% 23.72/3.69 fof(f1490,plain,(
% 23.72/3.69 ![V_y_2,V_x_2,T_a]: (~class_Orderings_Opreorder(T_a)|(c_Orderings_Oord__class_Oless(T_a,V_x_2,V_y_2)<=>(c_Orderings_Oord__class_Oless__eq(T_a,V_x_2,V_y_2)&~c_Orderings_Oord__class_Oless__eq(T_a,V_y_2,V_x_2))))),
% 23.72/3.69 inference(pre_NNF_transformation,[status(thm)],[f67])).
% 23.72/3.69 fof(f1491,plain,(
% 23.72/3.69 ![V_y_2,V_x_2,T_a]: (~class_Orderings_Opreorder(T_a)|((~c_Orderings_Oord__class_Oless(T_a,V_x_2,V_y_2)|(c_Orderings_Oord__class_Oless__eq(T_a,V_x_2,V_y_2)&~c_Orderings_Oord__class_Oless__eq(T_a,V_y_2,V_x_2)))&(c_Orderings_Oord__class_Oless(T_a,V_x_2,V_y_2)|(~c_Orderings_Oord__class_Oless__eq(T_a,V_x_2,V_y_2)|c_Orderings_Oord__class_Oless__eq(T_a,V_y_2,V_x_2)))))),
% 23.72/3.69 inference(NNF_transformation,[status(thm)],[f1490])).
% 23.72/3.69 fof(f1492,plain,(
% 23.72/3.69 ![T_a]: (~class_Orderings_Opreorder(T_a)|((![V_y_2,V_x_2]: (~c_Orderings_Oord__class_Oless(T_a,V_x_2,V_y_2)|(c_Orderings_Oord__class_Oless__eq(T_a,V_x_2,V_y_2)&~c_Orderings_Oord__class_Oless__eq(T_a,V_y_2,V_x_2))))&(![V_y_2,V_x_2]: (c_Orderings_Oord__class_Oless(T_a,V_x_2,V_y_2)|(~c_Orderings_Oord__class_Oless__eq(T_a,V_x_2,V_y_2)|c_Orderings_Oord__class_Oless__eq(T_a,V_y_2,V_x_2))))))),
% 23.72/3.69 inference(miniscoping,[status(thm)],[f1491])).
% 23.72/3.69 fof(f1495,plain,(
% 23.72/3.69 ![X0,X1,X2]: (~class_Orderings_Opreorder(X0)|c_Orderings_Oord__class_Oless(X0,X1,X2)|~c_Orderings_Oord__class_Oless__eq(X0,X1,X2)|c_Orderings_Oord__class_Oless__eq(X0,X2,X1))),
% 23.72/3.69 inference(cnf_transformation,[status(thm)],[f1492])).
% 23.72/3.69 fof(f1515,plain,(
% 23.72/3.69 ![V_b,V_a,V_c,T_a]: (~class_Groups_Oordered__ab__semigroup__add__imp__le(T_a)|(~c_Orderings_Oord__class_Oless(T_a,c_Groups_Oplus__class_Oplus(T_a,V_c,V_a),c_Groups_Oplus__class_Oplus(T_a,V_c,V_b))|c_Orderings_Oord__class_Oless(T_a,V_a,V_b)))),
% 23.72/3.69 inference(pre_NNF_transformation,[status(thm)],[f72])).
% 23.72/3.69 fof(f1516,plain,(
% 23.72/3.69 ![T_a]: (~class_Groups_Oordered__ab__semigroup__add__imp__le(T_a)|(![V_b,V_a]: ((![V_c]: ~c_Orderings_Oord__class_Oless(T_a,c_Groups_Oplus__class_Oplus(T_a,V_c,V_a),c_Groups_Oplus__class_Oplus(T_a,V_c,V_b)))|c_Orderings_Oord__class_Oless(T_a,V_a,V_b))))),
% 23.72/3.69 inference(miniscoping,[status(thm)],[f1515])).
% 23.72/3.69 fof(f1517,plain,(
% 23.72/3.69 ![X0,X1,X2,X3]: (~class_Groups_Oordered__ab__semigroup__add__imp__le(X0)|~c_Orderings_Oord__class_Oless(X0,c_Groups_Oplus__class_Oplus(X0,X1,X2),c_Groups_Oplus__class_Oplus(X0,X1,X3))|c_Orderings_Oord__class_Oless(X0,X2,X3))),
% 23.72/3.69 inference(cnf_transformation,[status(thm)],[f1516])).
% 23.72/3.69 fof(f1518,plain,(
% 23.72/3.69 ![V_b,V_c,V_a,T_a]: (~class_Groups_Oordered__ab__semigroup__add__imp__le(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_c))|c_Orderings_Oord__class_Oless(T_a,V_a,V_b)))),
% 23.72/3.69 inference(pre_NNF_transformation,[status(thm)],[f73])).
% 23.72/3.69 fof(f1519,plain,(
% 23.72/3.69 ![T_a]: (~class_Groups_Oordered__ab__semigroup__add__imp__le(T_a)|(![V_b,V_a]: ((![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_c)))|c_Orderings_Oord__class_Oless(T_a,V_a,V_b))))),
% 23.72/3.69 inference(miniscoping,[status(thm)],[f1518])).
% 23.72/3.69 fof(f1520,plain,(
% 23.72/3.69 ![X0,X1,X2,X3]: (~class_Groups_Oordered__ab__semigroup__add__imp__le(X0)|~c_Orderings_Oord__class_Oless(X0,c_Groups_Oplus__class_Oplus(X0,X1,X2),c_Groups_Oplus__class_Oplus(X0,X3,X2))|c_Orderings_Oord__class_Oless(X0,X1,X3))),
% 23.72/3.69 inference(cnf_transformation,[status(thm)],[f1519])).
% 23.72/3.69 fof(f1577,plain,(
% 23.72/3.69 ![V_a,T_a]: (~class_Groups_Ocomm__monoid__add(T_a)|c_Groups_Oplus__class_Oplus(T_a,c_Groups_Ozero__class_Ozero(T_a),V_a)=V_a)),
% 23.72/3.69 inference(pre_NNF_transformation,[status(thm)],[f90])).
% 23.72/3.69 fof(f1578,plain,(
% 23.72/3.69 ![T_a]: (~class_Groups_Ocomm__monoid__add(T_a)|(![V_a]: c_Groups_Oplus__class_Oplus(T_a,c_Groups_Ozero__class_Ozero(T_a),V_a)=V_a))),
% 23.72/3.69 inference(miniscoping,[status(thm)],[f1577])).
% 23.72/3.69 fof(f1579,plain,(
% 23.72/3.69 ![X0,X1]: (~class_Groups_Ocomm__monoid__add(X0)|c_Groups_Oplus__class_Oplus(X0,c_Groups_Ozero__class_Ozero(X0),X1)=X1)),
% 23.72/3.69 inference(cnf_transformation,[status(thm)],[f1578])).
% 23.72/3.69 fof(f1586,plain,(
% 23.72/3.69 ![X0]: (c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X0)=c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0))),
% 23.72/3.69 inference(cnf_transformation,[status(thm)],[f93])).
% 23.72/3.69 fof(f1939,plain,(
% 23.72/3.69 ![X0,X1]: (c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X1)|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X0))),
% 23.72/3.69 inference(cnf_transformation,[status(thm)],[f200])).
% 23.72/3.69 fof(f1945,plain,(
% 23.72/3.69 ![X0,X1]: (hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X0),X1)=hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X1),X0))),
% 23.72/3.69 inference(cnf_transformation,[status(thm)],[f203])).
% 23.72/3.69 fof(f1981,plain,(
% 23.72/3.69 ![V_y_2,V_x_2]: ((~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2,V_y_2)|(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2,V_y_2)&~V_x_2=V_y_2))&(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2,V_y_2)|(~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2,V_y_2)|V_x_2=V_y_2)))),
% 23.72/3.69 inference(NNF_transformation,[status(thm)],[f216])).
% 23.72/3.69 fof(f1982,plain,(
% 23.72/3.69 (![V_y_2,V_x_2]: (~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2,V_y_2)|(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2,V_y_2)&~V_x_2=V_y_2)))&(![V_y_2,V_x_2]: (c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2,V_y_2)|(~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2,V_y_2)|V_x_2=V_y_2)))),
% 23.72/3.69 inference(miniscoping,[status(thm)],[f1981])).
% 23.72/3.69 fof(f1984,plain,(
% 23.72/3.69 ![X0,X1]: (~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,X1)|~X0=X1)),
% 23.72/3.69 inference(cnf_transformation,[status(thm)],[f1982])).
% 23.72/3.69 fof(f3050,plain,(
% 23.72/3.69 ![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,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,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_Oabs__class_Oabs(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,V_x_2,V_ra_2))))),
% 23.72/3.69 inference(NNF_transformation,[status(thm)],[f534])).
% 23.72/3.69 fof(f3051,plain,(
% 23.72/3.69 (![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,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,V_ra_2),V_x_2)&c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2,V_ra_2))))&(![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,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,V_ra_2),V_x_2)|~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2,V_ra_2))))),
% 23.72/3.69 inference(miniscoping,[status(thm)],[f3050])).
% 23.72/3.69 fof(f3053,plain,(
% 23.72/3.69 ![X0,X1]: (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0),X1)|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X1))),
% 23.72/3.69 inference(cnf_transformation,[status(thm)],[f3051])).
% 23.72/3.69 fof(f4589,plain,(
% 23.72/3.69 class_Groups_Oordered__ab__semigroup__add__imp__le(tc_RealDef_Oreal)),
% 23.72/3.69 inference(cnf_transformation,[status(thm)],[f1112])).
% 23.72/3.69 fof(f4594,plain,(
% 23.72/3.69 class_RealVector_Oreal__normed__algebra__1(tc_RealDef_Oreal)),
% 23.72/3.69 inference(cnf_transformation,[status(thm)],[f1117])).
% 23.72/3.69 fof(f4596,plain,(
% 23.72/3.69 class_Groups_Oordered__ab__group__add__abs(tc_RealDef_Oreal)),
% 23.72/3.69 inference(cnf_transformation,[status(thm)],[f1119])).
% 23.72/3.69 fof(f4618,plain,(
% 23.72/3.69 class_Groups_Ocomm__monoid__add(tc_RealDef_Oreal)),
% 23.72/3.69 inference(cnf_transformation,[status(thm)],[f1141])).
% 23.72/3.69 fof(f4627,plain,(
% 23.72/3.69 class_Orderings_Opreorder(tc_RealDef_Oreal)),
% 23.72/3.69 inference(cnf_transformation,[status(thm)],[f1150])).
% 23.72/3.69 fof(f4628,plain,(
% 23.72/3.69 class_Orderings_Olinorder(tc_RealDef_Oreal)),
% 23.72/3.69 inference(cnf_transformation,[status(thm)],[f1151])).
% 23.72/3.69 fof(f4812,plain,(
% 23.72/3.69 ~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____))))),
% 23.72/3.69 inference(cnf_transformation,[status(thm)],[f1276])).
% 23.72/3.69 fof(f4844,plain,(
% 23.72/3.69 ![X0]: (~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,X0))),
% 23.72/3.69 inference(destructive_equality_resolution,[status(thm)],[f1984])).
% 23.72/3.69 fof(f4886,plain,(
% 23.72/3.69 c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,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____))),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____)))),
% 23.72/3.69 inference(resolution,[status(thm)],[f1939,f4812])).
% 23.72/3.69 fof(f5278,plain,(
% 23.72/3.69 c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,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____))),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_m____),v_r)))),
% 23.72/3.69 inference(backward_demodulation,[status(thm)],[f1945,f4886])).
% 23.72/3.69 fof(f5281,plain,(
% 23.72/3.69 ~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_m____),v_r))))),
% 23.72/3.69 inference(backward_demodulation,[status(thm)],[f1945,f4812])).
% 23.72/3.69 fof(f5317,plain,(
% 23.72/3.69 c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,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_m____),v_r))),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_m____),v_r)))),
% 23.72/3.69 inference(forward_demodulation,[status(thm)],[f1945,f5278])).
% 23.72/3.69 fof(f5318,plain,(
% 23.72/3.69 ~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_m____),v_r)),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_m____),v_r))))),
% 23.72/3.69 inference(forward_demodulation,[status(thm)],[f1945,f5281])).
% 23.72/3.69 fof(f5815,plain,(
% 23.72/3.69 c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal))=c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),
% 23.72/3.69 inference(resolution,[status(thm)],[f4594,f1290])).
% 23.72/3.69 fof(f5816,plain,(
% 23.72/3.69 c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal))=c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),
% 23.72/3.69 inference(forward_demodulation,[status(thm)],[f1586,f5815])).
% 23.72/3.69 fof(f5872,plain,(
% 23.72/3.69 ~class_Groups_Oordered__ab__group__add__abs(tc_RealDef_Oreal)|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))),
% 23.72/3.69 inference(paramodulation,[status(thm)],[f5816,f1322])).
% 23.72/3.69 fof(f5875,plain,(
% 23.72/3.69 ~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))),
% 23.72/3.69 inference(forward_subsumption_resolution,[status(thm)],[f5872,f4596])).
% 23.72/3.69 fof(f6967,plain,(
% 23.72/3.69 ![X0]: (c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0)))),
% 23.72/3.69 inference(resolution,[status(thm)],[f3053,f1939])).
% 23.72/3.69 fof(f9188,plain,(
% 23.72/3.69 ![X0]: (~class_Orderings_Olinorder(tc_RealDef_Oreal)|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0),X0))),
% 23.72/3.69 inference(resolution,[status(thm)],[f1466,f6967])).
% 23.72/3.69 fof(f9235,plain,(
% 23.72/3.69 ![X0]: (~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0),X0))),
% 23.72/3.69 inference(forward_subsumption_resolution,[status(thm)],[f9188,f4628])).
% 23.72/3.69 fof(f9991,plain,(
% 23.72/3.69 ~class_Orderings_Opreorder(tc_RealDef_Oreal)|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,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_m____),v_r))),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_m____),v_r)))|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_m____),v_r)),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_m____),v_r))))),
% 23.72/3.69 inference(resolution,[status(thm)],[f1495,f5317])).
% 23.72/3.69 fof(f10023,plain,(
% 23.72/3.69 ![X0,X1]: (~class_Orderings_Opreorder(tc_RealDef_Oreal)|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,X1)|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X0)|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X0))),
% 23.72/3.69 inference(resolution,[status(thm)],[f1495,f1939])).
% 23.72/3.69 fof(f10052,plain,(
% 23.72/3.69 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,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_m____),v_r))),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_m____),v_r)))|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_m____),v_r)),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_m____),v_r))))),
% 23.72/3.69 inference(forward_subsumption_resolution,[status(thm)],[f9991,f4627])).
% 23.72/3.69 fof(f10076,plain,(
% 23.72/3.69 ![X0,X1]: (~class_Orderings_Opreorder(tc_RealDef_Oreal)|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,X1)|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X0))),
% 23.72/3.69 inference(duplicate_literals_removal,[status(thm)],[f10023])).
% 23.72/3.69 fof(f10077,plain,(
% 23.72/3.69 ![X0,X1]: (c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,X1)|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X0))),
% 23.72/3.69 inference(forward_subsumption_resolution,[status(thm)],[f10076,f4627])).
% 23.72/3.69 fof(f10123,plain,(
% 23.72/3.69 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,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_m____),v_r))),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_m____),v_r)))),
% 23.72/3.69 inference(forward_subsumption_resolution,[status(thm)],[f10052,f5318])).
% 23.72/3.69 fof(f10131,plain,(
% 23.72/3.69 ![X0]: (~class_Orderings_Opreorder(tc_RealDef_Oreal)|~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_m____),v_r)),X0)|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,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_m____),v_r))),X0))),
% 23.72/3.69 inference(resolution,[status(thm)],[f10123,f1446])).
% 23.72/3.69 fof(f10146,plain,(
% 23.72/3.69 ![X0]: (~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_m____),v_r)),X0)|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,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_m____),v_r))),X0))),
% 23.72/3.69 inference(forward_subsumption_resolution,[status(thm)],[f10131,f4627])).
% 23.72/3.69 fof(f10288,plain,(
% 23.72/3.69 ![X0]: (c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,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_m____),v_r))),X0)|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,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_m____),v_r))))),
% 23.72/3.69 inference(resolution,[status(thm)],[f10146,f10077])).
% 23.72/3.69 fof(f10890,plain,(
% 23.72/3.69 ![X0]: (~class_Groups_Oordered__ab__semigroup__add__imp__le(tc_RealDef_Oreal)|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_m____),v_r)),X0)|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,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____)),X0),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_m____),v_r))))),
% 23.72/3.69 inference(resolution,[status(thm)],[f1517,f10288])).
% 23.72/3.69 fof(f10917,plain,(
% 23.72/3.69 ![X0]: (c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_m____),v_r)),X0)|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,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____)),X0),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_m____),v_r))))),
% 23.72/3.69 inference(forward_subsumption_resolution,[status(thm)],[f10890,f4589])).
% 23.72/3.69 fof(f11427,plain,(
% 23.72/3.69 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_m____),v_r)),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_m____),v_r))|~class_Groups_Oordered__ab__semigroup__add__imp__le(tc_RealDef_Oreal)|c_Orderings_Oord__class_Oless(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_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____))),
% 23.72/3.69 inference(resolution,[status(thm)],[f10917,f1520])).
% 23.72/3.69 fof(f11450,plain,(
% 23.72/3.69 ~class_Groups_Oordered__ab__semigroup__add__imp__le(tc_RealDef_Oreal)|c_Orderings_Oord__class_Oless(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_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____))),
% 23.72/3.69 inference(forward_subsumption_resolution,[status(thm)],[f11427,f9235])).
% 23.72/3.69 fof(f11473,plain,(
% 23.72/3.69 c_Orderings_Oord__class_Oless(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_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____))),
% 23.72/3.69 inference(forward_subsumption_resolution,[status(thm)],[f11450,f4589])).
% 23.72/3.69 fof(f11487,plain,(
% 23.72/3.69 ![X0]: (~class_Orderings_Opreorder(tc_RealDef_Oreal)|~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____),X0)|c_Orderings_Oord__class_Oless(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____)),X0))),
% 23.72/3.69 inference(resolution,[status(thm)],[f11473,f1446])).
% 23.72/3.69 fof(f11509,plain,(
% 23.72/3.69 ![X0]: (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____),X0)|c_Orderings_Oord__class_Oless(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____)),X0))),
% 23.72/3.69 inference(forward_subsumption_resolution,[status(thm)],[f11487,f4627])).
% 23.72/3.69 fof(f12530,plain,(
% 23.72/3.69 ![X0]: (c_Orderings_Oord__class_Oless(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____)),X0)|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____)))),
% 23.72/3.69 inference(resolution,[status(thm)],[f11509,f10077])).
% 23.72/3.69 fof(f13161,plain,(
% 23.72/3.69 ![X0]: (c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),X0)=X0)),
% 23.72/3.69 inference(resolution,[status(thm)],[f1579,f4618])).
% 23.72/3.69 fof(f13598,plain,(
% 23.72/3.69 ![X0]: (c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____)),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____))|~class_Groups_Oordered__ab__semigroup__add__imp__le(tc_RealDef_Oreal)|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),X0))),
% 23.72/3.69 inference(resolution,[status(thm)],[f12530,f1520])).
% 23.72/3.69 fof(f13643,plain,(
% 23.72/3.69 ![X0]: (c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,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_Oone__class_Oone(tc_RealDef_Oreal),X0))),
% 23.72/3.73 inference(forward_subsumption_resolution,[status(thm)],[f13598,f4589])).
% 23.72/3.73 fof(f29754,plain,(
% 23.72/3.73 c_Orderings_Oord__class_Oless(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_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))),
% 23.72/3.73 inference(paramodulation,[status(thm)],[f13161,f13643])).
% 23.72/3.73 fof(f29841,plain,(
% 23.72/3.73 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))),
% 23.72/3.73 inference(forward_subsumption_resolution,[status(thm)],[f29754,f4844])).
% 23.72/3.73 fof(f29901,plain,(
% 23.72/3.73 $false),
% 23.72/3.73 inference(forward_subsumption_resolution,[status(thm)],[f29841,f5875])).
% 23.72/3.73 % SZS output end CNFRefutation for theBenchmark.p
% 1.75/3.79 % Elapsed time: 3.344956 seconds
% 1.75/3.79 % CPU time: 24.494724 seconds
% 1.75/3.79 % Total memory used: 374.697 MB
% 1.75/3.79 % Net memory used: 363.772 MB
%------------------------------------------------------------------------------