%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW208+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n016.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:48 PM UTC 2026
% Result : Theorem 6.42s 1.51s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWW208+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.43 % Computer : n016.cluster.edu
% 0.16/0.43 % Model : x86_64 x86_64
% 0.16/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.43 % Memory : 8046.5625MB
% 0.16/0.43 % OS : Linux 6.8.0-71-generic
% 0.16/0.43 % CPULimit : 300
% 0.16/0.43 % WCLimit : 300
% 0.16/0.43 % DateTime : Mon Sep 21 09:46:09 UTC 2026
% 0.16/0.44 % CPUTime :
% 0.26/0.60 % Drodi V4.1.1
% 6.42/1.51 % Refutation found
% 6.42/1.51 % SZS status Theorem for theBenchmark: Theorem is valid
% 6.42/1.51 % SZS output start CNFRefutation for theBenchmark
% 6.42/1.51 fof(f2,axiom,(
% 6.42/1.51 hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),v_r)) ),
% 6.42/1.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.42/1.51 fof(f4,axiom,(
% 6.42/1.51 (! [B_n] : hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,hAPP(c_Complex_OIm,hAPP(v_s,B_n)))),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),v_r),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)))) )),
% 6.42/1.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.42/1.51 fof(f17,axiom,(
% 6.42/1.51 (! [V_a,T_a] :( class_Groups_Oordered__ab__group__add__abs(T_a)=> ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless(T_a,c_Groups_Oabs__class_Oabs(T_a,V_a)),c_Groups_Ozero__class_Ozero(T_a))) ) )),
% 6.42/1.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.42/1.51 fof(f18,axiom,(
% 6.42/1.51 (! [V_a_2,T_a] :( class_Groups_Oordered__ab__group__add__abs(T_a)=> ( hBOOL(hAPP(c_Orderings_Oord__class_Oless(T_a,c_Groups_Ozero__class_Ozero(T_a)),c_Groups_Oabs__class_Oabs(T_a,V_a_2)))<=> V_a_2 != c_Groups_Ozero__class_Ozero(T_a) ) ) )),
% 6.42/1.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.42/1.51 fof(f25,axiom,(
% 6.42/1.51 (! [V_c,V_b,V_a,T_a] :( class_Groups_Ocancel__semigroup__add(T_a)=> ( hAPP(hAPP(c_Groups_Oplus__class_Oplus(T_a),V_a),V_b) = hAPP(hAPP(c_Groups_Oplus__class_Oplus(T_a),V_a),V_c)=> V_b = V_c ) ) )),
% 6.42/1.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.42/1.51 fof(f30,axiom,(
% 6.42/1.51 (! [V_w,V_z] :( hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_z),V_w))=> ( hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_w),V_z))=> V_z = V_w ) ) )),
% 6.42/1.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.42/1.51 fof(f31,axiom,(
% 6.42/1.51 (! [V_k,V_j,V_i] :( hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_i),V_j))=> ( hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_j),V_k))=> hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_i),V_k)) ) ) )),
% 6.42/1.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.42/1.51 fof(f32,axiom,(
% 6.42/1.51 (! [V_w,V_z] :( hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_z),V_w))| hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_w),V_z)) ) )),
% 6.42/1.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.42/1.51 fof(f33,axiom,(
% 6.42/1.51 (! [V_w] : hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_w),V_w)) )),
% 6.42/1.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.42/1.51 fof(f60,axiom,(
% 6.42/1.51 (! [V_y_2,V_x_2] :( hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2),V_y_2))<=> ( hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2),V_y_2))| V_x_2 = V_y_2 ) ) )),
% 6.42/1.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.42/1.51 fof(f63,axiom,(
% 6.42/1.51 (! [T_a] :( class_Rings_Olinordered__idom(T_a)=> c_Groups_Oabs__class_Oabs(T_a,c_Groups_Oone__class_Oone(T_a)) = c_Groups_Oone__class_Oone(T_a) ) )),
% 6.42/1.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.42/1.51 fof(f64,axiom,(
% 6.42/1.51 c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) != c_Groups_Oone__class_Oone(tc_RealDef_Oreal) ),
% 6.42/1.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.42/1.51 fof(f69,axiom,(
% 6.42/1.51 (! [V_y_2,V_x_2,T_a] :( class_Groups_Oordered__comm__monoid__add(T_a)=> ( hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(T_a,c_Groups_Ozero__class_Ozero(T_a)),V_x_2))=> ( hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(T_a,c_Groups_Ozero__class_Ozero(T_a)),V_y_2))=> ( hAPP(hAPP(c_Groups_Oplus__class_Oplus(T_a),V_x_2),V_y_2) = c_Groups_Ozero__class_Ozero(T_a)<=> ( V_x_2 = c_Groups_Ozero__class_Ozero(T_a)& V_y_2 = c_Groups_Ozero__class_Ozero(T_a) ) ) ) ) ) )),
% 6.42/1.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.42/1.51 fof(f101,axiom,(
% 6.42/1.51 (! [V_r] : c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,V_r) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,V_r) )),
% 6.42/1.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.42/1.51 fof(f1121,axiom,(
% 6.42/1.51 class_Groups_Oordered__ab__group__add__abs(tc_RealDef_Oreal) ),
% 6.42/1.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.42/1.51 fof(f1123,axiom,(
% 6.42/1.51 class_Groups_Oordered__comm__monoid__add(tc_RealDef_Oreal) ),
% 6.42/1.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.42/1.51 fof(f1135,axiom,(
% 6.42/1.51 class_Groups_Ocancel__semigroup__add(tc_RealDef_Oreal) ),
% 6.42/1.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.42/1.51 fof(f1149,axiom,(
% 6.42/1.51 class_Rings_Olinordered__idom(tc_RealDef_Oreal) ),
% 6.42/1.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.42/1.51 fof(f1269,conjecture,(
% 6.42/1.51 ( hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),v_r),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))))& (! [B_n] : hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,hAPP(c_Complex_OIm,hAPP(v_s,hAPP(v_f____,hAPP(v_ga____,B_n)))))),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),v_r),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)))) )) ),
% 6.42/1.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.42/1.51 fof(f1270,negated_conjecture,(
% 6.42/1.51 ~(( hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),v_r),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))))& (! [B_n] : hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,hAPP(c_Complex_OIm,hAPP(v_s,hAPP(v_f____,hAPP(v_ga____,B_n)))))),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),v_r),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)))) )) )),
% 6.42/1.51 inference(negated_conjecture,[status(cth)],[f1269])).
% 6.42/1.51 fof(f1274,plain,(
% 6.42/1.51 hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),v_r))),
% 6.42/1.51 inference(cnf_transformation,[status(thm)],[f2])).
% 6.42/1.51 fof(f1276,plain,(
% 6.42/1.51 ![X0]: (hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,hAPP(c_Complex_OIm,hAPP(v_s,X0)))),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),v_r),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)))))),
% 6.42/1.51 inference(cnf_transformation,[status(thm)],[f4])).
% 6.42/1.51 fof(f1304,plain,(
% 6.42/1.51 ![V_a,T_a]: (~class_Groups_Oordered__ab__group__add__abs(T_a)|~hBOOL(hAPP(c_Orderings_Oord__class_Oless(T_a,c_Groups_Oabs__class_Oabs(T_a,V_a)),c_Groups_Ozero__class_Ozero(T_a))))),
% 6.42/1.51 inference(pre_NNF_transformation,[status(thm)],[f17])).
% 6.42/1.51 fof(f1305,plain,(
% 6.42/1.51 ![T_a]: (~class_Groups_Oordered__ab__group__add__abs(T_a)|(![V_a]: ~hBOOL(hAPP(c_Orderings_Oord__class_Oless(T_a,c_Groups_Oabs__class_Oabs(T_a,V_a)),c_Groups_Ozero__class_Ozero(T_a)))))),
% 6.42/1.51 inference(miniscoping,[status(thm)],[f1304])).
% 6.42/1.51 fof(f1306,plain,(
% 6.42/1.51 ![X0,X1]: (~class_Groups_Oordered__ab__group__add__abs(X0)|~hBOOL(hAPP(c_Orderings_Oord__class_Oless(X0,c_Groups_Oabs__class_Oabs(X0,X1)),c_Groups_Ozero__class_Ozero(X0))))),
% 6.42/1.51 inference(cnf_transformation,[status(thm)],[f1305])).
% 6.42/1.51 fof(f1307,plain,(
% 6.42/1.51 ![V_a_2,T_a]: (~class_Groups_Oordered__ab__group__add__abs(T_a)|(hBOOL(hAPP(c_Orderings_Oord__class_Oless(T_a,c_Groups_Ozero__class_Ozero(T_a)),c_Groups_Oabs__class_Oabs(T_a,V_a_2)))<=>~V_a_2=c_Groups_Ozero__class_Ozero(T_a)))),
% 6.42/1.51 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 6.42/1.51 fof(f1308,plain,(
% 6.42/1.51 ![V_a_2,T_a]: (~class_Groups_Oordered__ab__group__add__abs(T_a)|((~hBOOL(hAPP(c_Orderings_Oord__class_Oless(T_a,c_Groups_Ozero__class_Ozero(T_a)),c_Groups_Oabs__class_Oabs(T_a,V_a_2)))|~V_a_2=c_Groups_Ozero__class_Ozero(T_a))&(hBOOL(hAPP(c_Orderings_Oord__class_Oless(T_a,c_Groups_Ozero__class_Ozero(T_a)),c_Groups_Oabs__class_Oabs(T_a,V_a_2)))|V_a_2=c_Groups_Ozero__class_Ozero(T_a))))),
% 6.42/1.51 inference(NNF_transformation,[status(thm)],[f1307])).
% 6.42/1.51 fof(f1309,plain,(
% 6.42/1.51 ![T_a]: (~class_Groups_Oordered__ab__group__add__abs(T_a)|((![V_a_2]: (~hBOOL(hAPP(c_Orderings_Oord__class_Oless(T_a,c_Groups_Ozero__class_Ozero(T_a)),c_Groups_Oabs__class_Oabs(T_a,V_a_2)))|~V_a_2=c_Groups_Ozero__class_Ozero(T_a)))&(![V_a_2]: (hBOOL(hAPP(c_Orderings_Oord__class_Oless(T_a,c_Groups_Ozero__class_Ozero(T_a)),c_Groups_Oabs__class_Oabs(T_a,V_a_2)))|V_a_2=c_Groups_Ozero__class_Ozero(T_a)))))),
% 6.42/1.51 inference(miniscoping,[status(thm)],[f1308])).
% 6.42/1.51 fof(f1310,plain,(
% 6.42/1.51 ![X0,X1]: (~class_Groups_Oordered__ab__group__add__abs(X0)|~hBOOL(hAPP(c_Orderings_Oord__class_Oless(X0,c_Groups_Ozero__class_Ozero(X0)),c_Groups_Oabs__class_Oabs(X0,X1)))|~X1=c_Groups_Ozero__class_Ozero(X0))),
% 6.42/1.51 inference(cnf_transformation,[status(thm)],[f1309])).
% 6.42/1.51 fof(f1311,plain,(
% 6.42/1.51 ![X0,X1]: (~class_Groups_Oordered__ab__group__add__abs(X0)|hBOOL(hAPP(c_Orderings_Oord__class_Oless(X0,c_Groups_Ozero__class_Ozero(X0)),c_Groups_Oabs__class_Oabs(X0,X1)))|X1=c_Groups_Ozero__class_Ozero(X0))),
% 6.42/1.51 inference(cnf_transformation,[status(thm)],[f1309])).
% 6.42/1.51 fof(f1328,plain,(
% 6.42/1.51 ![V_c,V_b,V_a,T_a]: (~class_Groups_Ocancel__semigroup__add(T_a)|(~hAPP(hAPP(c_Groups_Oplus__class_Oplus(T_a),V_a),V_b)=hAPP(hAPP(c_Groups_Oplus__class_Oplus(T_a),V_a),V_c)|V_b=V_c))),
% 6.42/1.51 inference(pre_NNF_transformation,[status(thm)],[f25])).
% 6.42/1.51 fof(f1329,plain,(
% 6.42/1.51 ![T_a]: (~class_Groups_Ocancel__semigroup__add(T_a)|(![V_c,V_b]: ((![V_a]: ~hAPP(hAPP(c_Groups_Oplus__class_Oplus(T_a),V_a),V_b)=hAPP(hAPP(c_Groups_Oplus__class_Oplus(T_a),V_a),V_c))|V_b=V_c)))),
% 6.42/1.51 inference(miniscoping,[status(thm)],[f1328])).
% 6.42/1.51 fof(f1330,plain,(
% 6.42/1.51 ![X0,X1,X2,X3]: (~class_Groups_Ocancel__semigroup__add(X0)|~hAPP(hAPP(c_Groups_Oplus__class_Oplus(X0),X1),X2)=hAPP(hAPP(c_Groups_Oplus__class_Oplus(X0),X1),X3)|X2=X3)),
% 6.42/1.51 inference(cnf_transformation,[status(thm)],[f1329])).
% 6.42/1.51 fof(f1349,plain,(
% 6.42/1.51 ![V_w,V_z]: (~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_z),V_w))|(~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_w),V_z))|V_z=V_w))),
% 6.42/1.51 inference(pre_NNF_transformation,[status(thm)],[f30])).
% 6.42/1.51 fof(f1350,plain,(
% 6.42/1.51 ![X0,X1]: (~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0),X1))|~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1),X0))|X0=X1)),
% 6.42/1.51 inference(cnf_transformation,[status(thm)],[f1349])).
% 6.42/1.51 fof(f1351,plain,(
% 6.42/1.51 ![V_k,V_j,V_i]: (~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_i),V_j))|(~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_j),V_k))|hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_i),V_k))))),
% 6.42/1.51 inference(pre_NNF_transformation,[status(thm)],[f31])).
% 6.42/1.51 fof(f1352,plain,(
% 6.42/1.51 ![V_j,V_i]: (~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_i),V_j))|(![V_k]: (~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_j),V_k))|hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_i),V_k)))))),
% 6.42/1.51 inference(miniscoping,[status(thm)],[f1351])).
% 6.42/1.51 fof(f1353,plain,(
% 6.42/1.51 ![X0,X1,X2]: (~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0),X1))|~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1),X2))|hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0),X2)))),
% 6.42/1.51 inference(cnf_transformation,[status(thm)],[f1352])).
% 6.42/1.51 fof(f1354,plain,(
% 6.42/1.51 ![X0,X1]: (hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0),X1))|hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1),X0)))),
% 6.42/1.51 inference(cnf_transformation,[status(thm)],[f32])).
% 6.42/1.51 fof(f1355,plain,(
% 6.42/1.51 ![X0]: (hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0),X0)))),
% 6.42/1.51 inference(cnf_transformation,[status(thm)],[f33])).
% 6.42/1.51 fof(f1443,plain,(
% 6.42/1.51 ![V_y_2,V_x_2]: ((~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2),V_y_2))|(hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2),V_y_2))|V_x_2=V_y_2))&(hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2),V_y_2))|(~hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2),V_y_2))&~V_x_2=V_y_2)))),
% 6.42/1.51 inference(NNF_transformation,[status(thm)],[f60])).
% 6.42/1.51 fof(f1444,plain,(
% 6.42/1.51 (![V_y_2,V_x_2]: (~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2),V_y_2))|(hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2),V_y_2))|V_x_2=V_y_2)))&(![V_y_2,V_x_2]: (hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2),V_y_2))|(~hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2),V_y_2))&~V_x_2=V_y_2)))),
% 6.42/1.51 inference(miniscoping,[status(thm)],[f1443])).
% 6.42/1.51 fof(f1445,plain,(
% 6.42/1.51 ![X0,X1]: (~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0),X1))|hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0),X1))|X0=X1)),
% 6.42/1.51 inference(cnf_transformation,[status(thm)],[f1444])).
% 6.42/1.51 fof(f1446,plain,(
% 6.42/1.51 ![X0,X1]: (hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0),X1))|~hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0),X1)))),
% 6.42/1.51 inference(cnf_transformation,[status(thm)],[f1444])).
% 6.42/1.51 fof(f1456,plain,(
% 6.42/1.51 ![T_a]: (~class_Rings_Olinordered__idom(T_a)|c_Groups_Oabs__class_Oabs(T_a,c_Groups_Oone__class_Oone(T_a))=c_Groups_Oone__class_Oone(T_a))),
% 6.42/1.51 inference(pre_NNF_transformation,[status(thm)],[f63])).
% 6.42/1.51 fof(f1457,plain,(
% 6.42/1.51 ![X0]: (~class_Rings_Olinordered__idom(X0)|c_Groups_Oabs__class_Oabs(X0,c_Groups_Oone__class_Oone(X0))=c_Groups_Oone__class_Oone(X0))),
% 6.42/1.51 inference(cnf_transformation,[status(thm)],[f1456])).
% 6.42/1.51 fof(f1458,plain,(
% 6.42/1.51 ~c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)=c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),
% 6.42/1.51 inference(cnf_transformation,[status(thm)],[f64])).
% 6.42/1.51 fof(f1471,plain,(
% 6.42/1.51 ![V_y_2,V_x_2,T_a]: (~class_Groups_Oordered__comm__monoid__add(T_a)|(~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(T_a,c_Groups_Ozero__class_Ozero(T_a)),V_x_2))|(~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(T_a,c_Groups_Ozero__class_Ozero(T_a)),V_y_2))|(hAPP(hAPP(c_Groups_Oplus__class_Oplus(T_a),V_x_2),V_y_2)=c_Groups_Ozero__class_Ozero(T_a)<=>(V_x_2=c_Groups_Ozero__class_Ozero(T_a)&V_y_2=c_Groups_Ozero__class_Ozero(T_a))))))),
% 6.42/1.51 inference(pre_NNF_transformation,[status(thm)],[f69])).
% 6.42/1.51 fof(f1472,plain,(
% 6.42/1.51 ![V_y_2,V_x_2,T_a]: (~class_Groups_Oordered__comm__monoid__add(T_a)|(~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(T_a,c_Groups_Ozero__class_Ozero(T_a)),V_x_2))|(~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(T_a,c_Groups_Ozero__class_Ozero(T_a)),V_y_2))|((~hAPP(hAPP(c_Groups_Oplus__class_Oplus(T_a),V_x_2),V_y_2)=c_Groups_Ozero__class_Ozero(T_a)|(V_x_2=c_Groups_Ozero__class_Ozero(T_a)&V_y_2=c_Groups_Ozero__class_Ozero(T_a)))&(hAPP(hAPP(c_Groups_Oplus__class_Oplus(T_a),V_x_2),V_y_2)=c_Groups_Ozero__class_Ozero(T_a)|(~V_x_2=c_Groups_Ozero__class_Ozero(T_a)|~V_y_2=c_Groups_Ozero__class_Ozero(T_a)))))))),
% 6.42/1.51 inference(NNF_transformation,[status(thm)],[f1471])).
% 6.42/1.51 fof(f1473,plain,(
% 6.42/1.51 ![T_a]: (~class_Groups_Oordered__comm__monoid__add(T_a)|(![V_x_2]: (~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(T_a,c_Groups_Ozero__class_Ozero(T_a)),V_x_2))|(![V_y_2]: (~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(T_a,c_Groups_Ozero__class_Ozero(T_a)),V_y_2))|((~hAPP(hAPP(c_Groups_Oplus__class_Oplus(T_a),V_x_2),V_y_2)=c_Groups_Ozero__class_Ozero(T_a)|(V_x_2=c_Groups_Ozero__class_Ozero(T_a)&V_y_2=c_Groups_Ozero__class_Ozero(T_a)))&(hAPP(hAPP(c_Groups_Oplus__class_Oplus(T_a),V_x_2),V_y_2)=c_Groups_Ozero__class_Ozero(T_a)|(~V_x_2=c_Groups_Ozero__class_Ozero(T_a)|~V_y_2=c_Groups_Ozero__class_Ozero(T_a)))))))))),
% 6.42/1.51 inference(miniscoping,[status(thm)],[f1472])).
% 6.42/1.51 fof(f1474,plain,(
% 6.42/1.51 ![X0,X1,X2]: (~class_Groups_Oordered__comm__monoid__add(X0)|~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(X0,c_Groups_Ozero__class_Ozero(X0)),X1))|~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(X0,c_Groups_Ozero__class_Ozero(X0)),X2))|~hAPP(hAPP(c_Groups_Oplus__class_Oplus(X0),X1),X2)=c_Groups_Ozero__class_Ozero(X0)|X1=c_Groups_Ozero__class_Ozero(X0))),
% 6.42/1.51 inference(cnf_transformation,[status(thm)],[f1473])).
% 6.42/1.51 fof(f1476,plain,(
% 6.42/1.51 ![X0,X1,X2]: (~class_Groups_Oordered__comm__monoid__add(X0)|~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(X0,c_Groups_Ozero__class_Ozero(X0)),X1))|~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(X0,c_Groups_Ozero__class_Ozero(X0)),X2))|hAPP(hAPP(c_Groups_Oplus__class_Oplus(X0),X1),X2)=c_Groups_Ozero__class_Ozero(X0)|~X1=c_Groups_Ozero__class_Ozero(X0)|~X2=c_Groups_Ozero__class_Ozero(X0))),
% 6.42/1.51 inference(cnf_transformation,[status(thm)],[f1473])).
% 6.42/1.51 fof(f1580,plain,(
% 6.42/1.51 ![X0]: (c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X0)=c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0))),
% 6.42/1.51 inference(cnf_transformation,[status(thm)],[f101])).
% 6.42/1.51 fof(f4406,plain,(
% 6.42/1.51 class_Groups_Oordered__ab__group__add__abs(tc_RealDef_Oreal)),
% 6.42/1.51 inference(cnf_transformation,[status(thm)],[f1121])).
% 6.42/1.51 fof(f4408,plain,(
% 6.42/1.51 class_Groups_Oordered__comm__monoid__add(tc_RealDef_Oreal)),
% 6.42/1.51 inference(cnf_transformation,[status(thm)],[f1123])).
% 6.42/1.51 fof(f4420,plain,(
% 6.42/1.51 class_Groups_Ocancel__semigroup__add(tc_RealDef_Oreal)),
% 6.42/1.51 inference(cnf_transformation,[status(thm)],[f1135])).
% 6.42/1.51 fof(f4434,plain,(
% 6.42/1.51 class_Rings_Olinordered__idom(tc_RealDef_Oreal)),
% 6.42/1.51 inference(cnf_transformation,[status(thm)],[f1149])).
% 6.42/1.51 fof(f4607,plain,(
% 6.42/1.51 (~hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),v_r),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))))|(?[B_n]: ~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,hAPP(c_Complex_OIm,hAPP(v_s,hAPP(v_f____,hAPP(v_ga____,B_n)))))),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),v_r),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))))))),
% 6.42/1.51 inference(pre_NNF_transformation,[status(thm)],[f1270])).
% 6.42/1.51 fof(f4608,plain,(
% 6.42/1.51 ~hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),v_r),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))))|~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,hAPP(c_Complex_OIm,hAPP(v_s,hAPP(v_f____,hAPP(v_ga____,sK73_skl)))))),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),v_r),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))))),
% 6.42/1.51 inference(skolemize,[status(esa),new_symbols(skolem,[sK73_skl]),skolemize(B_n,sK73_skl)],[f4607])).
% 6.42/1.51 fof(f4609,plain,(
% 6.42/1.51 ~hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),v_r),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))))|~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,hAPP(c_Complex_OIm,hAPP(v_s,hAPP(v_f____,hAPP(v_ga____,sK73_skl)))))),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),v_r),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))))),
% 6.42/1.51 inference(cnf_transformation,[status(thm)],[f4608])).
% 6.42/1.51 fof(f4655,plain,(
% 6.42/1.51 ![X0]: (~class_Groups_Oordered__ab__group__add__abs(X0)|~hBOOL(hAPP(c_Orderings_Oord__class_Oless(X0,c_Groups_Ozero__class_Ozero(X0)),c_Groups_Oabs__class_Oabs(X0,c_Groups_Ozero__class_Ozero(X0)))))),
% 6.42/1.51 inference(destructive_equality_resolution,[status(thm)],[f1310])).
% 6.42/1.51 fof(f4660,plain,(
% 6.42/1.51 ![X0]: (~class_Groups_Oordered__comm__monoid__add(X0)|~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(X0,c_Groups_Ozero__class_Ozero(X0)),c_Groups_Ozero__class_Ozero(X0)))|~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(X0,c_Groups_Ozero__class_Ozero(X0)),c_Groups_Ozero__class_Ozero(X0)))|hAPP(hAPP(c_Groups_Oplus__class_Oplus(X0),c_Groups_Ozero__class_Ozero(X0)),c_Groups_Ozero__class_Ozero(X0))=c_Groups_Ozero__class_Ozero(X0))),
% 6.42/1.51 inference(destructive_equality_resolution,[status(thm)],[f1476])).
% 6.42/1.51 fof(f4661,plain,(
% 6.42/1.51 ![X0]: (~class_Groups_Oordered__comm__monoid__add(X0)|~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(X0,c_Groups_Ozero__class_Ozero(X0)),c_Groups_Ozero__class_Ozero(X0)))|hAPP(hAPP(c_Groups_Oplus__class_Oplus(X0),c_Groups_Ozero__class_Ozero(X0)),c_Groups_Ozero__class_Ozero(X0))=c_Groups_Ozero__class_Ozero(X0))),
% 6.42/1.51 inference(duplicate_literals_removal,[status(thm)],[f4660])).
% 6.42/1.51 fof(f4789,plain,(
% 6.42/1.51 ~hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),v_r),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))))|~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,hAPP(c_Complex_OIm,hAPP(v_s,hAPP(v_f____,hAPP(v_ga____,sK73_skl)))))),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),v_r),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))))),
% 6.42/1.51 inference(backward_demodulation,[status(thm)],[f1580,f4609])).
% 6.42/1.51 fof(f4790,plain,(
% 6.42/1.51 ![X0]: (hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,hAPP(c_Complex_OIm,hAPP(v_s,X0)))),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),v_r),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)))))),
% 6.42/1.51 inference(forward_demodulation,[status(thm)],[f1580,f1276])).
% 6.42/1.51 fof(f4794,plain,(
% 6.42/1.51 ~hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),v_r),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))))),
% 6.42/1.51 inference(forward_subsumption_resolution,[status(thm)],[f4789,f4790])).
% 6.42/1.51 fof(f4841,plain,(
% 6.42/1.51 ![X0,X1]: (hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0),X1))|X0=X1|hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1),X0)))),
% 6.42/1.51 inference(resolution,[status(thm)],[f1445,f1354])).
% 6.42/1.51 fof(f4896,plain,(
% 6.42/1.51 ![X0]: (~class_Groups_Oordered__ab__group__add__abs(tc_RealDef_Oreal)|~hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X0)),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))))),
% 6.42/1.51 inference(paramodulation,[status(thm)],[f1580,f1306])).
% 6.42/1.51 fof(f5248,plain,(
% 6.42/1.51 c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)=hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),v_r),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))|hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),v_r),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)))),
% 6.42/1.51 inference(resolution,[status(thm)],[f4841,f4794])).
% 6.42/1.51 fof(f5258,plain,(
% 6.42/1.51 ![X0,X1]: (hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0),X1))|X0=X1|hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X1),X0))|X1=X0)),
% 6.42/1.51 inference(resolution,[status(thm)],[f4841,f1445])).
% 6.42/1.51 fof(f5268,plain,(
% 6.42/1.51 ![X0,X1]: (hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0),X1))|X0=X1|hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X1),X0)))),
% 6.42/1.51 inference(duplicate_literals_removal,[status(thm)],[f5258])).
% 6.42/1.51 fof(f5294,plain,(
% 6.42/1.51 c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)=hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),v_r),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))|~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),v_r),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))))|c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)=hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),v_r),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))),
% 6.42/1.51 inference(resolution,[status(thm)],[f5248,f1350])).
% 6.42/1.51 fof(f5297,plain,(
% 6.42/1.51 c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)=hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),v_r),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))|~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),v_r),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))))),
% 6.42/1.51 inference(duplicate_literals_removal,[status(thm)],[f5294])).
% 6.42/1.51 fof(f5303,plain,(
% 6.42/1.51 ![X0]: (c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)=hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),v_r),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))|~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),X0))|~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),v_r),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)))))),
% 6.42/1.51 inference(resolution,[status(thm)],[f5297,f1353])).
% 6.42/1.51 fof(f5410,plain,(
% 6.42/1.51 ![X0]: (~hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X0)),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))))),
% 6.42/1.51 inference(backward_subsumption_resolution,[status(thm)],[f4896,f4406])).
% 6.42/1.51 fof(f5412,plain,(
% 6.42/1.51 ![X0]: (hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0)))|X0=c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))),
% 6.42/1.51 inference(resolution,[status(thm)],[f4406,f1311])).
% 6.42/1.51 fof(f5417,plain,(
% 6.42/1.51 ![X0]: (hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X0)))|X0=c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))),
% 6.42/1.51 inference(forward_demodulation,[status(thm)],[f1580,f5412])).
% 6.42/1.51 fof(f5476,plain,(
% 6.42/1.51 ![X0]: (c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)=hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),v_r),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))|~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_RealDef_Oreal,hAPP(c_Complex_OIm,hAPP(v_s,X0))))))),
% 6.42/1.51 inference(resolution,[status(thm)],[f5303,f4790])).
% 6.42/1.51 fof(f5980,plain,(
% 6.42/1.51 c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)=c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))|hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)))|~class_Groups_Oordered__ab__group__add__abs(tc_RealDef_Oreal)),
% 6.42/1.51 inference(resolution,[status(thm)],[f5268,f4655])).
% 6.42/1.51 fof(f6000,plain,(
% 6.42/1.51 c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)=c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))|hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)))|~class_Groups_Oordered__ab__group__add__abs(tc_RealDef_Oreal)),
% 6.42/1.51 inference(forward_demodulation,[status(thm)],[f1580,f5980])).
% 6.42/1.51 fof(f6001,plain,(
% 6.42/1.51 c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)=c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))|hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)))|~class_Groups_Oordered__ab__group__add__abs(tc_RealDef_Oreal)),
% 6.42/1.51 inference(forward_demodulation,[status(thm)],[f1580,f6000])).
% 6.42/1.51 fof(f6002,plain,(
% 6.42/1.51 c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)=c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))|~class_Groups_Oordered__ab__group__add__abs(tc_RealDef_Oreal)),
% 6.42/1.51 inference(forward_subsumption_resolution,[status(thm)],[f6001,f5410])).
% 6.42/1.51 fof(f6013,plain,(
% 6.42/1.51 c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)=c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))),
% 6.42/1.51 inference(forward_subsumption_resolution,[status(thm)],[f6002,f4406])).
% 6.42/1.51 fof(f6228,plain,(
% 6.42/1.51 ![X0]: (X0=c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)|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_RealDef_Oreal,X0))))),
% 6.42/1.51 inference(resolution,[status(thm)],[f5417,f1446])).
% 6.42/1.51 fof(f6268,plain,(
% 6.42/1.51 ![X0]: (hAPP(c_Complex_OIm,hAPP(v_s,X0))=c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)|c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)=hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),v_r),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)))),
% 6.42/1.51 inference(resolution,[status(thm)],[f6228,f5476])).
% 6.42/1.51 fof(f6489,plain,(
% 6.42/1.51 c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)=hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),v_r),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))|~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_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))))|c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)=hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),v_r),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))),
% 6.42/1.51 inference(paramodulation,[status(thm)],[f6268,f5476])).
% 6.42/1.51 fof(f6505,plain,(
% 6.42/1.51 c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)=hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),v_r),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))|~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)))|c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)=hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),v_r),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))),
% 6.42/1.51 inference(forward_demodulation,[status(thm)],[f6013,f6489])).
% 6.42/1.51 fof(f6506,plain,(
% 6.42/1.51 c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)=hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),v_r),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))|~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)))),
% 6.42/1.51 inference(duplicate_literals_removal,[status(thm)],[f6505])).
% 6.42/1.51 fof(f6507,plain,(
% 6.42/1.51 c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)=hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),v_r),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))),
% 6.42/1.51 inference(forward_subsumption_resolution,[status(thm)],[f6506,f1355])).
% 6.42/1.51 fof(f7631,plain,(
% 6.42/1.51 c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal))=c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),
% 6.42/1.51 inference(resolution,[status(thm)],[f1457,f4434])).
% 6.42/1.51 fof(f7633,plain,(
% 6.42/1.51 c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal))=c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),
% 6.42/1.51 inference(forward_demodulation,[status(thm)],[f1580,f7631])).
% 6.42/1.51 fof(f7683,plain,(
% 6.42/1.51 c_Groups_Oone__class_Oone(tc_RealDef_Oreal)=c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)|hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)))),
% 6.42/1.51 inference(paramodulation,[status(thm)],[f7633,f6228])).
% 6.42/1.51 fof(f7690,plain,(
% 6.42/1.51 hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)))),
% 6.42/1.51 inference(forward_subsumption_resolution,[status(thm)],[f7683,f1458])).
% 6.42/1.51 fof(f8074,plain,(
% 6.42/1.51 ~class_Groups_Oordered__comm__monoid__add(tc_RealDef_Oreal)|~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),v_r))|~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)))|v_r=c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),
% 6.42/1.51 inference(resolution,[status(thm)],[f1474,f6507])).
% 6.42/1.51 fof(f8092,plain,(
% 6.42/1.51 ~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),v_r))|~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)))|v_r=c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),
% 6.42/1.51 inference(forward_subsumption_resolution,[status(thm)],[f8074,f4408])).
% 6.42/1.51 fof(f8346,plain,(
% 6.42/1.51 ~class_Groups_Oordered__comm__monoid__add(tc_RealDef_Oreal)|hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))=c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),
% 6.42/1.51 inference(resolution,[status(thm)],[f4661,f1354])).
% 6.42/1.51 fof(f8352,plain,(
% 6.42/1.51 hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))=c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),
% 6.42/1.51 inference(forward_subsumption_resolution,[status(thm)],[f8346,f4408])).
% 6.42/1.51 fof(f8433,plain,(
% 6.42/1.51 ![X0]: (~class_Groups_Ocancel__semigroup__add(tc_RealDef_Oreal)|~hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),X0)=c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)|X0=c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))),
% 6.42/1.51 inference(paramodulation,[status(thm)],[f8352,f1330])).
% 6.42/1.51 fof(f8447,plain,(
% 6.42/1.51 ![X0]: (~hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),X0)=c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)|X0=c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))),
% 6.84/1.55 inference(forward_subsumption_resolution,[status(thm)],[f8433,f4420])).
% 6.84/1.55 fof(f8939,plain,(
% 6.84/1.55 ~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)))|v_r=c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),
% 6.84/1.55 inference(forward_subsumption_resolution,[status(thm)],[f8092,f1274])).
% 6.84/1.55 fof(f8940,plain,(
% 6.84/1.55 v_r=c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),
% 6.84/1.55 inference(resolution,[status(thm)],[f8939,f7690])).
% 6.84/1.55 fof(f8960,plain,(
% 6.84/1.55 ![X0]: (~hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),X0)=c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)|X0=v_r)),
% 6.84/1.55 inference(backward_demodulation,[status(thm)],[f8940,f8447])).
% 6.84/1.55 fof(f9004,plain,(
% 6.84/1.55 v_r=hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),v_r),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))),
% 6.84/1.55 inference(backward_demodulation,[status(thm)],[f8940,f6507])).
% 6.84/1.55 fof(f9016,plain,(
% 6.84/1.55 ~v_r=c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),
% 6.84/1.55 inference(backward_demodulation,[status(thm)],[f8940,f1458])).
% 6.84/1.55 fof(f9039,plain,(
% 6.84/1.55 ![X0]: (~hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),v_r),X0)=c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)|X0=v_r)),
% 6.84/1.55 inference(forward_demodulation,[status(thm)],[f8940,f8960])).
% 6.84/1.55 fof(f9040,plain,(
% 6.84/1.55 ![X0]: (~hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),v_r),X0)=v_r|X0=v_r)),
% 6.84/1.55 inference(forward_demodulation,[status(thm)],[f8940,f9039])).
% 6.84/1.55 fof(f9850,plain,(
% 6.84/1.55 c_Groups_Oone__class_Oone(tc_RealDef_Oreal)=v_r),
% 6.84/1.55 inference(resolution,[status(thm)],[f9004,f9040])).
% 6.84/1.55 fof(f9870,plain,(
% 6.84/1.55 $false),
% 6.84/1.55 inference(forward_subsumption_resolution,[status(thm)],[f9850,f9016])).
% 6.84/1.55 % SZS output end CNFRefutation for theBenchmark.p
% 6.84/1.56 % Elapsed time: 1.106414 seconds
% 6.84/1.56 % CPU time: 7.356889 seconds
% 6.84/1.56 % Total memory used: 276.697 MB
% 6.84/1.56 % Net memory used: 273.584 MB
%------------------------------------------------------------------------------