%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW179+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 : n014.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 12.03s 2.41s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWW179+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.18/0.44 % Computer : n014.cluster.edu
% 0.18/0.44 % Model : x86_64 x86_64
% 0.18/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.44 % Memory : 8046.5625MB
% 0.18/0.44 % OS : Linux 6.8.0-71-generic
% 0.18/0.44 % CPULimit : 300
% 0.18/0.44 % WCLimit : 300
% 0.18/0.44 % DateTime : Mon Sep 21 09:40:19 UTC 2026
% 0.18/0.44 % CPUTime :
% 0.27/0.59 % Drodi V4.1.1
% 12.03/2.41 % Refutation found
% 12.03/2.41 % SZS status Theorem for theBenchmark: Theorem is valid
% 12.03/2.41 % SZS output start CNFRefutation for theBenchmark
% 12.03/2.41 fof(f2,axiom,(
% 12.03/2.41 c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____)) ),
% 12.03/2.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 12.03/2.41 fof(f3,axiom,(
% 12.03/2.41 c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(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____))) ),
% 12.03/2.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 12.03/2.41 fof(f4,axiom,(
% 12.03/2.41 (! [V_x] : c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,V_x))) )),
% 12.03/2.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 12.03/2.41 fof(f15,axiom,(
% 12.03/2.41 (! [V_x_2] :( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),V_x_2),V_x_2))<=> V_x_2 = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) ) )),
% 12.03/2.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 12.03/2.41 fof(f16,axiom,(
% 12.03/2.41 (! [V_w] : c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_w,V_w) )),
% 12.03/2.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 12.03/2.41 fof(f17,axiom,(
% 12.03/2.41 (! [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) ) )),
% 12.03/2.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 12.03/2.41 fof(f18,axiom,(
% 12.03/2.41 (! [V_k,V_j,V_i] :( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_i,V_j)=> ( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_j,V_k)=> c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_i,V_k) ) ) )),
% 12.03/2.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 12.03/2.41 fof(f19,axiom,(
% 12.03/2.41 (! [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)=> V_z = V_w ) ) )),
% 12.03/2.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 12.03/2.41 fof(f20,axiom,(
% 12.03/2.41 (! [V_y_2,V_x_2] :( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2,V_y_2)<=> ( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2,V_y_2)| V_x_2 = V_y_2 ) ) )),
% 12.03/2.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 12.03/2.41 fof(f21,axiom,(
% 12.03/2.41 (! [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 ) ) )),
% 12.03/2.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 12.03/2.41 fof(f22,axiom,(
% 12.03/2.41 (! [V_r] : c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,V_r) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,V_r) )),
% 12.03/2.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 12.03/2.41 fof(f23,axiom,(
% 12.03/2.41 (! [V_z,V_y,V_x] :( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x,V_y)=> c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,V_z,V_x),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,V_z,V_y)) ) )),
% 12.03/2.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 12.03/2.41 fof(f66,axiom,(
% 12.03/2.41 (! [V_y_2,V_x_2,V_z_2] :( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),V_z_2)=> ( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),V_x_2),V_z_2),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),V_y_2),V_z_2))<=> c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2,V_y_2) ) ) )),
% 12.03/2.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 12.03/2.41 fof(f71,axiom,(
% 12.03/2.41 (! [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) )),
% 12.03/2.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 12.03/2.41 fof(f96,axiom,(
% 12.03/2.41 (! [V_z] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),V_z) = V_z )),
% 12.03/2.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 12.03/2.42 fof(f259,axiom,(
% 12.03/2.42 (! [V_c,V_a,T_a] :( class_Rings_Ocomm__semiring__1(T_a)=> c_Groups_Oplus__class_Oplus(T_a,V_a,V_c) = c_Groups_Oplus__class_Oplus(T_a,V_c,V_a) ) )),
% 12.03/2.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 12.03/2.42 fof(f283,axiom,(
% 12.03/2.42 (! [V_a,T_a] :( class_Rings_Ocomm__semiring__1(T_a)=> hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_a),c_Groups_Ozero__class_Ozero(T_a)) = c_Groups_Ozero__class_Ozero(T_a) ) )),
% 12.03/2.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 12.03/2.42 fof(f287,axiom,(
% 12.03/2.42 (! [V_a,T_a] :( class_Rings_Ocomm__semiring__1(T_a)=> c_Groups_Oplus__class_Oplus(T_a,V_a,c_Groups_Ozero__class_Ozero(T_a)) = V_a ) )),
% 12.03/2.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 12.03/2.42 fof(f539,axiom,(
% 12.03/2.42 (! [V_a] :( ( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_a,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))=> c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,V_a) = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,V_a) )& ( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_a,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))=> c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,V_a) = V_a ) ) )),
% 12.03/2.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 12.03/2.42 fof(f924,axiom,(
% 12.03/2.42 (! [V_n] : c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealDef_Oreal(tc_Nat_Onat,c_Nat_OSuc(V_n))) )),
% 12.03/2.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 12.03/2.42 fof(f1148,axiom,(
% 12.03/2.42 class_Rings_Ocomm__semiring__1(tc_RealDef_Oreal) ),
% 12.03/2.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 12.03/2.42 fof(f1275,conjecture,(
% 12.03/2.42 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(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____)))) ),
% 12.03/2.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 12.03/2.42 fof(f1276,negated_conjecture,(
% 12.03/2.42 ~(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(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____)))) )),
% 12.03/2.42 inference(negated_conjecture,[status(cth)],[f1275])).
% 12.03/2.42 fof(f1280,plain,(
% 12.03/2.42 c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____))),
% 12.03/2.42 inference(cnf_transformation,[status(thm)],[f2])).
% 12.03/2.42 fof(f1281,plain,(
% 12.03/2.42 c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(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____)))),
% 12.03/2.42 inference(cnf_transformation,[status(thm)],[f3])).
% 12.03/2.42 fof(f1282,plain,(
% 12.03/2.42 ![X0]: (c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0))))),
% 12.03/2.42 inference(cnf_transformation,[status(thm)],[f4])).
% 12.03/2.42 fof(f1316,plain,(
% 12.03/2.42 ![V_x_2]: ((c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),V_x_2),V_x_2))|V_x_2=c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))&(~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),V_x_2),V_x_2))|~V_x_2=c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)))),
% 12.03/2.42 inference(NNF_transformation,[status(thm)],[f15])).
% 12.03/2.42 fof(f1317,plain,(
% 12.03/2.42 (![V_x_2]: (c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),V_x_2),V_x_2))|V_x_2=c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)))&(![V_x_2]: (~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),V_x_2),V_x_2))|~V_x_2=c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)))),
% 12.03/2.42 inference(miniscoping,[status(thm)],[f1316])).
% 12.03/2.42 fof(f1319,plain,(
% 12.03/2.42 ![X0]: (~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X0),X0))|~X0=c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))),
% 12.03/2.42 inference(cnf_transformation,[status(thm)],[f1317])).
% 12.03/2.42 fof(f1320,plain,(
% 12.03/2.42 ![X0]: (c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X0))),
% 12.03/2.42 inference(cnf_transformation,[status(thm)],[f16])).
% 12.03/2.42 fof(f1321,plain,(
% 12.03/2.42 ![X0,X1]: (c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X1)|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X0))),
% 12.03/2.42 inference(cnf_transformation,[status(thm)],[f17])).
% 12.03/2.42 fof(f1322,plain,(
% 12.03/2.42 ![V_k,V_j,V_i]: (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_i,V_j)|(~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_j,V_k)|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_i,V_k)))),
% 12.03/2.42 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 12.03/2.42 fof(f1323,plain,(
% 12.03/2.42 ![V_j,V_i]: (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_i,V_j)|(![V_k]: (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_j,V_k)|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_i,V_k))))),
% 12.03/2.42 inference(miniscoping,[status(thm)],[f1322])).
% 12.03/2.42 fof(f1324,plain,(
% 12.03/2.42 ![X0,X1,X2]: (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X1)|~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X2)|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X2))),
% 12.03/2.42 inference(cnf_transformation,[status(thm)],[f1323])).
% 12.03/2.42 fof(f1325,plain,(
% 12.03/2.42 ![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)|V_z=V_w))),
% 12.03/2.42 inference(pre_NNF_transformation,[status(thm)],[f19])).
% 12.03/2.42 fof(f1326,plain,(
% 12.03/2.42 ![X0,X1]: (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X1)|~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X0)|X0=X1)),
% 12.03/2.42 inference(cnf_transformation,[status(thm)],[f1325])).
% 12.03/2.42 fof(f1327,plain,(
% 12.03/2.42 ![V_y_2,V_x_2]: ((~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2,V_y_2)|(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2,V_y_2)|V_x_2=V_y_2))&(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2,V_y_2)|(~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2,V_y_2)&~V_x_2=V_y_2)))),
% 12.03/2.42 inference(NNF_transformation,[status(thm)],[f20])).
% 12.03/2.42 fof(f1328,plain,(
% 12.03/2.42 (![V_y_2,V_x_2]: (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2,V_y_2)|(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]: (c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2,V_y_2)|(~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2,V_y_2)&~V_x_2=V_y_2)))),
% 12.03/2.42 inference(miniscoping,[status(thm)],[f1327])).
% 12.03/2.42 fof(f1329,plain,(
% 12.03/2.42 ![X0,X1]: (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X1)|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,X1)|X0=X1)),
% 12.03/2.42 inference(cnf_transformation,[status(thm)],[f1328])).
% 12.03/2.42 fof(f1330,plain,(
% 12.03/2.42 ![X0,X1]: (c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X1)|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,X1))),
% 12.03/2.42 inference(cnf_transformation,[status(thm)],[f1328])).
% 12.03/2.42 fof(f1332,plain,(
% 12.03/2.42 ![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)))),
% 12.03/2.42 inference(NNF_transformation,[status(thm)],[f21])).
% 12.03/2.42 fof(f1333,plain,(
% 12.03/2.42 (![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)))),
% 12.03/2.42 inference(miniscoping,[status(thm)],[f1332])).
% 12.03/2.42 fof(f1335,plain,(
% 12.03/2.42 ![X0,X1]: (~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,X1)|~X0=X1)),
% 12.03/2.42 inference(cnf_transformation,[status(thm)],[f1333])).
% 12.03/2.42 fof(f1337,plain,(
% 12.03/2.42 ![X0]: (c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X0)=c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0))),
% 12.03/2.42 inference(cnf_transformation,[status(thm)],[f22])).
% 12.03/2.42 fof(f1338,plain,(
% 12.03/2.42 ![V_z,V_y,V_x]: (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x,V_y)|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,V_z,V_x),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,V_z,V_y)))),
% 12.03/2.42 inference(pre_NNF_transformation,[status(thm)],[f23])).
% 12.03/2.42 fof(f1339,plain,(
% 12.03/2.42 ![V_y,V_x]: (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x,V_y)|(![V_z]: c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,V_z,V_x),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,V_z,V_y))))),
% 12.03/2.42 inference(miniscoping,[status(thm)],[f1338])).
% 12.03/2.42 fof(f1340,plain,(
% 12.03/2.42 ![X0,X1,X2]: (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X1)|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X2,X0),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X2,X1)))),
% 12.03/2.42 inference(cnf_transformation,[status(thm)],[f1339])).
% 12.03/2.42 fof(f1491,plain,(
% 12.03/2.42 ![V_y_2,V_x_2,V_z_2]: (~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),V_z_2)|(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),V_x_2),V_z_2),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),V_y_2),V_z_2))<=>c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2,V_y_2)))),
% 12.03/2.42 inference(pre_NNF_transformation,[status(thm)],[f66])).
% 12.03/2.42 fof(f1492,plain,(
% 12.03/2.42 ![V_y_2,V_x_2,V_z_2]: (~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),V_z_2)|((~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),V_x_2),V_z_2),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),V_y_2),V_z_2))|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2,V_y_2))&(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),V_x_2),V_z_2),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),V_y_2),V_z_2))|~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2,V_y_2))))),
% 12.03/2.42 inference(NNF_transformation,[status(thm)],[f1491])).
% 12.03/2.42 fof(f1493,plain,(
% 12.03/2.42 ![V_z_2]: (~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),V_z_2)|((![V_y_2,V_x_2]: (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),V_x_2),V_z_2),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),V_y_2),V_z_2))|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2,V_y_2)))&(![V_y_2,V_x_2]: (c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),V_x_2),V_z_2),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),V_y_2),V_z_2))|~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2,V_y_2)))))),
% 12.03/2.42 inference(miniscoping,[status(thm)],[f1492])).
% 12.03/2.42 fof(f1494,plain,(
% 12.03/2.42 ![X0,X1,X2]: (~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),X0)|~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X1),X0),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X2),X0))|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X2))),
% 12.03/2.42 inference(cnf_transformation,[status(thm)],[f1493])).
% 12.03/2.42 fof(f1506,plain,(
% 12.03/2.42 ![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))),
% 12.03/2.42 inference(cnf_transformation,[status(thm)],[f71])).
% 12.03/2.42 fof(f1581,plain,(
% 12.03/2.42 ![X0]: (hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),X0)=X0)),
% 12.03/2.42 inference(cnf_transformation,[status(thm)],[f96])).
% 12.03/2.42 fof(f2138,plain,(
% 12.03/2.42 ![V_c,V_a,T_a]: (~class_Rings_Ocomm__semiring__1(T_a)|c_Groups_Oplus__class_Oplus(T_a,V_a,V_c)=c_Groups_Oplus__class_Oplus(T_a,V_c,V_a))),
% 12.03/2.42 inference(pre_NNF_transformation,[status(thm)],[f259])).
% 12.03/2.42 fof(f2139,plain,(
% 12.03/2.42 ![T_a]: (~class_Rings_Ocomm__semiring__1(T_a)|(![V_c,V_a]: c_Groups_Oplus__class_Oplus(T_a,V_a,V_c)=c_Groups_Oplus__class_Oplus(T_a,V_c,V_a)))),
% 12.03/2.42 inference(miniscoping,[status(thm)],[f2138])).
% 12.03/2.42 fof(f2140,plain,(
% 12.03/2.42 ![X0,X1,X2]: (~class_Rings_Ocomm__semiring__1(X0)|c_Groups_Oplus__class_Oplus(X0,X1,X2)=c_Groups_Oplus__class_Oplus(X0,X2,X1))),
% 12.03/2.42 inference(cnf_transformation,[status(thm)],[f2139])).
% 12.03/2.42 fof(f2231,plain,(
% 12.03/2.42 ![V_a,T_a]: (~class_Rings_Ocomm__semiring__1(T_a)|hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_a),c_Groups_Ozero__class_Ozero(T_a))=c_Groups_Ozero__class_Ozero(T_a))),
% 12.03/2.42 inference(pre_NNF_transformation,[status(thm)],[f283])).
% 12.03/2.42 fof(f2232,plain,(
% 12.03/2.42 ![T_a]: (~class_Rings_Ocomm__semiring__1(T_a)|(![V_a]: hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_a),c_Groups_Ozero__class_Ozero(T_a))=c_Groups_Ozero__class_Ozero(T_a)))),
% 12.03/2.42 inference(miniscoping,[status(thm)],[f2231])).
% 12.03/2.42 fof(f2233,plain,(
% 12.03/2.42 ![X0,X1]: (~class_Rings_Ocomm__semiring__1(X0)|hAPP(hAPP(c_Groups_Otimes__class_Otimes(X0),X1),c_Groups_Ozero__class_Ozero(X0))=c_Groups_Ozero__class_Ozero(X0))),
% 12.03/2.42 inference(cnf_transformation,[status(thm)],[f2232])).
% 12.03/2.42 fof(f2247,plain,(
% 12.03/2.42 ![V_a,T_a]: (~class_Rings_Ocomm__semiring__1(T_a)|c_Groups_Oplus__class_Oplus(T_a,V_a,c_Groups_Ozero__class_Ozero(T_a))=V_a)),
% 12.03/2.42 inference(pre_NNF_transformation,[status(thm)],[f287])).
% 12.03/2.42 fof(f2248,plain,(
% 12.03/2.42 ![T_a]: (~class_Rings_Ocomm__semiring__1(T_a)|(![V_a]: c_Groups_Oplus__class_Oplus(T_a,V_a,c_Groups_Ozero__class_Ozero(T_a))=V_a))),
% 12.03/2.42 inference(miniscoping,[status(thm)],[f2247])).
% 12.03/2.42 fof(f2249,plain,(
% 12.03/2.42 ![X0,X1]: (~class_Rings_Ocomm__semiring__1(X0)|c_Groups_Oplus__class_Oplus(X0,X1,c_Groups_Ozero__class_Ozero(X0))=X1)),
% 12.03/2.42 inference(cnf_transformation,[status(thm)],[f2248])).
% 12.03/2.42 fof(f3134,plain,(
% 12.03/2.42 ![V_a]: ((~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_a,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))|c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,V_a)=c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,V_a))&(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_a,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))|c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,V_a)=V_a))),
% 12.03/2.42 inference(pre_NNF_transformation,[status(thm)],[f539])).
% 12.03/2.42 fof(f3135,plain,(
% 12.03/2.42 (![V_a]: (~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_a,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))|c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,V_a)=c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,V_a)))&(![V_a]: (c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_a,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))|c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,V_a)=V_a))),
% 12.03/2.42 inference(miniscoping,[status(thm)],[f3134])).
% 12.03/2.42 fof(f3137,plain,(
% 12.03/2.42 ![X0]: (c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))|c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0)=X0)),
% 12.03/2.42 inference(cnf_transformation,[status(thm)],[f3135])).
% 12.03/2.42 fof(f4250,plain,(
% 12.03/2.42 ![X0]: (c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealDef_Oreal(tc_Nat_Onat,c_Nat_OSuc(X0))))),
% 12.03/2.42 inference(cnf_transformation,[status(thm)],[f924])).
% 12.03/2.42 fof(f4669,plain,(
% 12.03/2.42 class_Rings_Ocomm__semiring__1(tc_RealDef_Oreal)),
% 12.03/2.42 inference(cnf_transformation,[status(thm)],[f1148])).
% 12.03/2.42 fof(f4856,plain,(
% 12.03/2.42 ~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(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____))))),
% 12.03/2.42 inference(cnf_transformation,[status(thm)],[f1276])).
% 12.03/2.42 fof(f4908,plain,(
% 12.03/2.42 ![X0]: (~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,X0))),
% 12.03/2.42 inference(destructive_equality_resolution,[status(thm)],[f1335])).
% 12.03/2.42 fof(f4945,plain,(
% 12.03/2.42 ~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(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_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_r),v_m____))))),
% 12.03/2.42 inference(backward_demodulation,[status(thm)],[f1337,f4856])).
% 12.03/2.42 fof(f4951,plain,(
% 12.03/2.42 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(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_r),v_m____)))),
% 12.03/2.42 inference(forward_demodulation,[status(thm)],[f1337,f1281])).
% 12.03/2.42 fof(f4952,plain,(
% 12.03/2.42 ![X0]: (c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X0))))),
% 12.03/2.42 inference(forward_demodulation,[status(thm)],[f1337,f1282])).
% 12.03/2.42 fof(f4962,plain,(
% 12.03/2.42 ![X0]: (c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))|c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X0)=X0)),
% 12.03/2.42 inference(forward_demodulation,[status(thm)],[f1337,f3137])).
% 12.03/2.42 fof(f4964,plain,(
% 12.03/2.42 ![X0]: (c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X0)=X0|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)))),
% 12.03/2.42 inference(resolution,[status(thm)],[f4962,f1330])).
% 12.03/2.42 fof(f4971,definition,(
% 12.03/2.42 sQ1_spl <=> (c_Groups_Oone__class_Oone(tc_RealDef_Oreal)=c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))),
% 12.03/2.42 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 12.03/2.42 fof(f4975,plain,(
% 12.03/2.42 ~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(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_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_m____),v_r))))),
% 12.03/2.42 inference(backward_demodulation,[status(thm)],[f1506,f4945])).
% 12.03/2.42 fof(f4976,plain,(
% 12.03/2.42 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(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_m____),v_r)))),
% 12.03/2.42 inference(backward_demodulation,[status(thm)],[f1506,f4951])).
% 12.03/2.42 fof(f4994,plain,(
% 12.03/2.42 c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))=c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),
% 12.03/2.42 inference(resolution,[status(thm)],[f4908,f4962])).
% 12.03/2.42 fof(f5031,plain,(
% 12.03/2.42 ![X0]: (c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))=X0)),
% 12.03/2.42 inference(resolution,[status(thm)],[f2249,f4669])).
% 12.03/2.42 fof(f5041,plain,(
% 12.03/2.42 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)))),
% 12.03/2.42 inference(paramodulation,[status(thm)],[f4994,f4952])).
% 12.03/2.42 fof(f5044,plain,(
% 12.03/2.42 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))),
% 12.03/2.42 inference(forward_demodulation,[status(thm)],[f5031,f5041])).
% 12.03/2.42 fof(f5057,plain,(
% 12.03/2.42 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))),
% 12.03/2.42 inference(resolution,[status(thm)],[f5044,f1330])).
% 12.03/2.42 fof(f5061,definition,(
% 12.03/2.42 sQ10_spl <=> (c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)))),
% 12.03/2.42 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 12.03/2.42 fof(f5063,plain,(
% 12.03/2.42 ~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))|sQ10_spl),
% 12.03/2.42 inference(component_clause,[status(thm)],[f5061])).
% 12.03/2.42 fof(f5087,plain,(
% 12.03/2.42 ~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))|~c_Groups_Oone__class_Oone(tc_RealDef_Oreal)=c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),
% 12.03/2.42 inference(paramodulation,[status(thm)],[f1581,f1319])).
% 12.03/2.42 fof(f5089,plain,(
% 12.03/2.42 ~sQ10_spl|~sQ1_spl),
% 12.03/2.42 inference(split_clause,[status(thm)],[f5087,f5061,f4971])).
% 12.03/2.42 fof(f5091,plain,(
% 12.03/2.42 $false|sQ10_spl),
% 12.03/2.42 inference(forward_subsumption_resolution,[status(thm)],[f5063,f5044])).
% 12.03/2.42 fof(f5092,plain,(
% 12.03/2.42 sQ10_spl),
% 12.03/2.42 inference(contradiction_clause,[status(thm)],[f5091])).
% 12.03/2.42 fof(f5127,plain,(
% 12.03/2.42 ~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))|c_Groups_Oone__class_Oone(tc_RealDef_Oreal)=c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),
% 12.03/2.42 inference(resolution,[status(thm)],[f1326,f5057])).
% 12.03/2.42 fof(f5129,plain,(
% 12.03/2.42 ~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_m____),v_r)),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))|c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_m____),v_r))=c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),
% 12.03/2.42 inference(resolution,[status(thm)],[f1326,f4976])).
% 12.03/2.42 fof(f5130,plain,(
% 12.03/2.42 ~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))|c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____)=c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),
% 12.03/2.42 inference(resolution,[status(thm)],[f1326,f1280])).
% 12.03/2.42 fof(f5138,definition,(
% 12.03/2.42 sQ11_spl <=> (c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)))),
% 12.03/2.42 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 12.03/2.42 fof(f5141,plain,(
% 12.03/2.42 ~sQ11_spl|sQ1_spl),
% 12.03/2.42 inference(split_clause,[status(thm)],[f5127,f5138,f4971])).
% 12.03/2.42 fof(f5149,definition,(
% 12.03/2.42 sQ14_spl <=> (c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_m____),v_r)),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)))),
% 12.03/2.42 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 12.03/2.42 fof(f5152,definition,(
% 12.03/2.42 sQ15_spl <=> (c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_m____),v_r))=c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))),
% 12.03/2.42 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 12.03/2.42 fof(f5153,plain,(
% 12.03/2.42 c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_m____),v_r))=c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)|~sQ15_spl),
% 12.03/2.42 inference(component_clause,[status(thm)],[f5152])).
% 12.03/2.42 fof(f5155,plain,(
% 12.03/2.42 ~sQ14_spl|sQ15_spl),
% 12.03/2.42 inference(split_clause,[status(thm)],[f5129,f5149,f5152])).
% 12.03/2.42 fof(f5156,definition,(
% 12.03/2.42 sQ16_spl <=> (c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)))),
% 12.03/2.42 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 12.03/2.42 fof(f5159,definition,(
% 12.03/2.42 sQ17_spl <=> (c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____)=c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))),
% 12.03/2.42 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 12.03/2.42 fof(f5160,plain,(
% 12.03/2.42 c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____)=c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)|~sQ17_spl),
% 12.03/2.42 inference(component_clause,[status(thm)],[f5159])).
% 12.03/2.42 fof(f5162,plain,(
% 12.03/2.42 ~sQ16_spl|sQ17_spl),
% 12.03/2.42 inference(split_clause,[status(thm)],[f5130,f5156,f5159])).
% 12.03/2.42 fof(f5182,plain,(
% 12.03/2.42 ~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(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_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_m____),v_r))))|c_Groups_Ozero__class_Ozero(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_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_m____),v_r)))),
% 12.03/2.42 inference(resolution,[status(thm)],[f1329,f4975])).
% 12.03/2.42 fof(f5187,definition,(
% 12.03/2.42 sQ19_spl <=> (c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(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_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_m____),v_r)))))),
% 12.03/2.42 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 12.03/2.42 fof(f5189,plain,(
% 12.03/2.42 ~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(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_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_m____),v_r))))|sQ19_spl),
% 12.03/2.42 inference(component_clause,[status(thm)],[f5187])).
% 12.03/2.42 fof(f5190,definition,(
% 12.03/2.42 sQ20_spl <=> (c_Groups_Ozero__class_Ozero(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_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_m____),v_r))))),
% 12.03/2.42 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 12.03/2.42 fof(f5191,plain,(
% 12.03/2.42 c_Groups_Ozero__class_Ozero(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_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_m____),v_r)))|~sQ20_spl),
% 12.03/2.42 inference(component_clause,[status(thm)],[f5190])).
% 12.03/2.42 fof(f5193,plain,(
% 12.03/2.42 ~sQ19_spl|sQ20_spl),
% 12.03/2.42 inference(split_clause,[status(thm)],[f5182,f5187,f5190])).
% 12.03/2.42 fof(f5195,plain,(
% 12.03/2.42 ![X0,X1]: (c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X1)=c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,X0))),
% 12.03/2.42 inference(resolution,[status(thm)],[f2140,f4669])).
% 12.03/2.42 fof(f5229,plain,(
% 12.03/2.42 ![X0]: (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),X0)|~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,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_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_m____),v_r))))|sQ19_spl)),
% 12.03/2.42 inference(resolution,[status(thm)],[f5189,f1324])).
% 12.03/2.42 fof(f5236,plain,(
% 12.03/2.42 ~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(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_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_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_m____),v_r))))|sQ19_spl),
% 12.03/2.42 inference(resolution,[status(thm)],[f5229,f4976])).
% 12.03/2.42 fof(f5291,plain,(
% 12.03/2.42 ![X0,X1]: (c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X1),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)))|c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X1)=X1)),
% 12.03/2.42 inference(resolution,[status(thm)],[f1340,f4964])).
% 12.03/2.42 fof(f5294,plain,(
% 12.03/2.42 ![X0,X1,X2]: (c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X1),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X2))|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X2,X1))),
% 12.03/2.42 inference(resolution,[status(thm)],[f1340,f1321])).
% 12.03/2.42 fof(f5303,plain,(
% 12.03/2.42 ![X0,X1]: (c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X1),X0)|c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X1)=X1)),
% 12.03/2.42 inference(forward_demodulation,[status(thm)],[f5031,f5291])).
% 12.03/2.42 fof(f5389,plain,(
% 12.03/2.42 ![X0,X1]: (c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X1),X1)|c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X0)=X0)),
% 12.03/2.42 inference(paramodulation,[status(thm)],[f5195,f5303])).
% 12.03/2.42 fof(f5391,definition,(
% 12.03/2.42 sQ25_spl <=> (c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(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____))))),
% 12.03/2.42 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 12.03/2.42 fof(f5392,plain,(
% 12.03/2.42 c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(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____)))|~sQ25_spl),
% 12.03/2.42 inference(component_clause,[status(thm)],[f5391])).
% 12.03/2.42 fof(f5418,plain,(
% 12.03/2.42 ![X0,X1]: (c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X1))|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)))),
% 12.03/2.42 inference(paramodulation,[status(thm)],[f5031,f5294])).
% 12.03/2.42 fof(f5433,plain,(
% 12.03/2.42 ![X0,X1]: (c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,X0))|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)))),
% 12.03/2.42 inference(paramodulation,[status(thm)],[f5195,f5418])).
% 12.03/2.42 fof(f5522,plain,(
% 12.03/2.42 ![X0]: (c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,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____))))|~sQ25_spl)),
% 12.03/2.42 inference(resolution,[status(thm)],[f5392,f1340])).
% 12.03/2.42 fof(f5523,plain,(
% 12.03/2.42 ~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____)),c_Groups_Ozero__class_Ozero(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_Ozero__class_Ozero(tc_RealDef_Oreal)|~sQ25_spl),
% 12.03/2.42 inference(resolution,[status(thm)],[f5392,f1326])).
% 12.03/2.42 fof(f5524,plain,(
% 12.03/2.42 ![X0]: (c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,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____))))|~sQ25_spl)),
% 12.03/2.42 inference(forward_demodulation,[status(thm)],[f5031,f5522])).
% 12.03/2.42 fof(f5525,definition,(
% 12.03/2.42 sQ32_spl <=> (c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____)),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)))),
% 12.03/2.42 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 12.03/2.42 fof(f5528,definition,(
% 12.03/2.42 sQ33_spl <=> (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_Ozero__class_Ozero(tc_RealDef_Oreal))),
% 12.03/2.42 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 12.03/2.42 fof(f5529,plain,(
% 12.03/2.42 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_Ozero__class_Ozero(tc_RealDef_Oreal)|~sQ33_spl),
% 12.03/2.42 inference(component_clause,[status(thm)],[f5528])).
% 12.03/2.42 fof(f5531,plain,(
% 12.03/2.42 ~sQ32_spl|sQ33_spl|~sQ25_spl),
% 12.03/2.42 inference(split_clause,[status(thm)],[f5523,f5525,f5528,f5391])).
% 12.03/2.42 fof(f5539,plain,(
% 12.03/2.42 c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))|~sQ33_spl),
% 12.03/2.42 inference(paramodulation,[status(thm)],[f5529,f5418])).
% 12.03/2.42 fof(f5547,definition,(
% 12.03/2.42 sQ35_spl <=> (c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____)))),
% 12.03/2.42 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 12.03/2.42 fof(f5549,plain,(
% 12.03/2.42 ~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____))|sQ35_spl),
% 12.03/2.42 inference(component_clause,[status(thm)],[f5547])).
% 12.03/2.42 fof(f5551,plain,(
% 12.03/2.42 sQ11_spl|sQ16_spl|~sQ33_spl),
% 12.03/2.42 inference(split_clause,[status(thm)],[f5539,f5138,f5156,f5528])).
% 12.03/2.42 fof(f5556,definition,(
% 12.03/2.42 sQ37_spl <=> (c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____))=c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____))),
% 12.03/2.42 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 12.03/2.42 fof(f5557,plain,(
% 12.03/2.42 c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____))=c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____)|~sQ37_spl),
% 12.03/2.42 inference(component_clause,[status(thm)],[f5556])).
% 12.03/2.42 fof(f5561,plain,(
% 12.03/2.42 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(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____)))|~sQ37_spl),
% 12.03/2.42 inference(paramodulation,[status(thm)],[f5557,f4952])).
% 12.03/2.42 fof(f5563,definition,(
% 12.03/2.42 sQ38_spl <=> (c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____)))),
% 12.03/2.42 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 12.03/2.42 fof(f5564,plain,(
% 12.03/2.42 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____))|~sQ38_spl),
% 12.03/2.42 inference(component_clause,[status(thm)],[f5563])).
% 12.03/2.42 fof(f5565,plain,(
% 12.03/2.42 ~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____))|sQ38_spl),
% 12.03/2.42 inference(component_clause,[status(thm)],[f5563])).
% 12.03/2.42 fof(f5569,plain,(
% 12.03/2.42 c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(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____)))|~sQ37_spl),
% 12.03/2.42 inference(resolution,[status(thm)],[f5561,f1330])).
% 12.03/2.42 fof(f5572,plain,(
% 12.03/2.42 ~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(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_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_m____),v_r))))|~sQ17_spl),
% 12.03/2.42 inference(backward_demodulation,[status(thm)],[f5160,f4975])).
% 12.03/2.42 fof(f5581,plain,(
% 12.03/2.42 ~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_m____),v_r))))|~sQ17_spl),
% 12.03/2.42 inference(forward_demodulation,[status(thm)],[f5031,f5572])).
% 12.03/2.42 fof(f5582,plain,(
% 12.03/2.42 $false|~sQ17_spl),
% 12.03/2.42 inference(forward_subsumption_resolution,[status(thm)],[f5581,f4952])).
% 12.03/2.42 fof(f5583,plain,(
% 12.03/2.42 ~sQ17_spl),
% 12.03/2.42 inference(contradiction_clause,[status(thm)],[f5582])).
% 12.03/2.42 fof(f5714,plain,(
% 12.03/2.42 ![X0]: (hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X0),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))=c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))),
% 12.03/2.42 inference(resolution,[status(thm)],[f2233,f4669])).
% 12.03/2.42 fof(f5719,plain,(
% 12.03/2.42 ![X0]: (c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,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))|~sQ25_spl)),
% 12.03/2.42 inference(paramodulation,[status(thm)],[f5195,f5524])).
% 12.03/2.42 fof(f5727,plain,(
% 12.03/2.42 ~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____))|c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)=c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____)|sQ38_spl),
% 12.03/2.42 inference(resolution,[status(thm)],[f5565,f1329])).
% 12.03/2.42 fof(f5728,plain,(
% 12.03/2.42 ~sQ35_spl|sQ17_spl|sQ38_spl),
% 12.03/2.42 inference(split_clause,[status(thm)],[f5727,f5547,f5159,f5563])).
% 12.03/2.42 fof(f5730,plain,(
% 12.03/2.42 c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))|sQ35_spl),
% 12.03/2.42 inference(resolution,[status(thm)],[f5549,f1321])).
% 12.03/2.42 fof(f5732,plain,(
% 12.03/2.42 sQ16_spl|sQ35_spl),
% 12.03/2.42 inference(split_clause,[status(thm)],[f5730,f5156,f5547])).
% 12.03/2.42 fof(f5738,plain,(
% 12.03/2.42 ![X0,X1]: (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X0),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____)),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X1),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____)))|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X1)|~sQ38_spl)),
% 12.03/2.42 inference(resolution,[status(thm)],[f5564,f1494])).
% 12.03/2.42 fof(f5905,plain,(
% 12.03/2.42 ![X0]: (hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),X0)=c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))),
% 12.03/2.42 inference(paramodulation,[status(thm)],[f1506,f5714])).
% 12.03/2.42 fof(f5935,definition,(
% 12.03/2.42 sQ47_spl <=> (c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____)))),
% 12.03/2.42 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 12.03/2.42 fof(f5937,plain,(
% 12.03/2.42 ~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____))|sQ47_spl),
% 12.03/2.42 inference(component_clause,[status(thm)],[f5935])).
% 12.03/2.42 fof(f5942,plain,(
% 12.03/2.42 $false|sQ47_spl),
% 12.03/2.42 inference(forward_subsumption_resolution,[status(thm)],[f5937,f1320])).
% 12.03/2.42 fof(f5943,plain,(
% 12.03/2.42 sQ47_spl),
% 12.03/2.42 inference(contradiction_clause,[status(thm)],[f5942])).
% 12.03/2.42 fof(f5961,plain,(
% 12.03/2.42 ![X0]: (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X0),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____)),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))|~sQ38_spl)),
% 12.03/2.42 inference(paramodulation,[status(thm)],[f5905,f5738])).
% 12.03/2.42 fof(f6184,plain,(
% 12.03/2.42 ![X0,X1]: (c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))|~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X0),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____)),X1)|~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))|~sQ38_spl)),
% 12.03/2.42 inference(resolution,[status(thm)],[f5961,f1324])).
% 12.03/2.43 fof(f6296,definition,(
% 12.03/2.43 ![X0]: (sQ69_spl <=> (X0=c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____))))),
% 12.03/2.43 introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition])).
% 12.03/2.43 fof(f6297,plain,(
% 12.03/2.43 ![X0]: (X0=c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____))|~sQ69_spl)),
% 12.03/2.43 inference(component_clause,[status(thm)],[f6296])).
% 12.03/2.43 fof(f6319,plain,(
% 12.03/2.43 sQ25_spl|~sQ37_spl),
% 12.03/2.43 inference(split_clause,[status(thm)],[f5569,f5391,f5556])).
% 12.03/2.43 fof(f6322,plain,(
% 12.03/2.43 ~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_m____),v_r))))|~sQ69_spl),
% 12.03/2.43 inference(backward_demodulation,[status(thm)],[f6297,f4975])).
% 12.03/2.43 fof(f6351,plain,(
% 12.03/2.43 $false|~sQ69_spl),
% 12.03/2.43 inference(forward_subsumption_resolution,[status(thm)],[f6322,f4952])).
% 12.03/2.43 fof(f6352,plain,(
% 12.03/2.43 ~sQ69_spl),
% 12.03/2.43 inference(contradiction_clause,[status(thm)],[f6351])).
% 12.03/2.43 fof(f7052,definition,(
% 12.03/2.43 sQ104_spl <=> (c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)=c_RealDef_Oreal(tc_Nat_Onat,c_Nat_OSuc(c_Groups_Oone__class_Oone(tc_Nat_Onat))))),
% 12.03/2.43 introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition])).
% 12.03/2.43 fof(f7053,plain,(
% 12.03/2.43 c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)=c_RealDef_Oreal(tc_Nat_Onat,c_Nat_OSuc(c_Groups_Oone__class_Oone(tc_Nat_Onat)))|~sQ104_spl),
% 12.03/2.43 inference(component_clause,[status(thm)],[f7052])).
% 12.03/2.43 fof(f7060,plain,(
% 12.03/2.43 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))|~sQ104_spl),
% 12.03/2.43 inference(paramodulation,[status(thm)],[f7053,f4250])).
% 12.03/2.43 fof(f7065,plain,(
% 12.03/2.43 $false|~sQ104_spl),
% 12.03/2.43 inference(forward_subsumption_resolution,[status(thm)],[f7060,f4908])).
% 12.03/2.43 fof(f7066,plain,(
% 12.03/2.43 ~sQ104_spl),
% 12.03/2.43 inference(contradiction_clause,[status(thm)],[f7065])).
% 12.03/2.43 fof(f7553,plain,(
% 12.03/2.43 $false|~sQ25_spl|sQ19_spl),
% 12.03/2.43 inference(forward_subsumption_resolution,[status(thm)],[f5236,f5719])).
% 12.03/2.43 fof(f7554,plain,(
% 12.03/2.43 ~sQ25_spl|sQ19_spl),
% 12.03/2.43 inference(contradiction_clause,[status(thm)],[f7553])).
% 12.03/2.43 fof(f7872,plain,(
% 12.03/2.43 ![X0,X1]: (c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))|~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X0),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____)),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)))|c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X1)=X1|~sQ38_spl)),
% 12.03/2.43 inference(resolution,[status(thm)],[f6184,f5389])).
% 12.03/2.43 fof(f7890,plain,(
% 12.03/2.43 ![X0,X1]: (c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))|~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X0),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____)),X1)|c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X1)=X1|~sQ38_spl)),
% 12.03/2.43 inference(forward_demodulation,[status(thm)],[f5031,f7872])).
% 12.03/2.43 fof(f7931,plain,(
% 12.03/2.43 ![X0]: (c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))|~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____),X0)|c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X0)=X0|~sQ38_spl)),
% 12.03/2.43 inference(paramodulation,[status(thm)],[f1581,f7890])).
% 12.03/2.43 fof(f7972,definition,(
% 12.03/2.43 ![X0]: (sQ129_spl <=> (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____),X0)|c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X0)=X0))),
% 12.03/2.43 introduced(definition,[new_symbols(definition,[sQ129_spl])],[split_symbol_definition])).
% 12.03/2.43 fof(f7973,plain,(
% 12.03/2.43 ![X0]: (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____),X0)|c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X0)=X0|~sQ129_spl)),
% 12.03/2.43 inference(component_clause,[status(thm)],[f7972])).
% 12.03/2.43 fof(f7975,plain,(
% 12.03/2.43 sQ11_spl|sQ129_spl|~sQ38_spl),
% 12.03/2.43 inference(split_clause,[status(thm)],[f7931,f5138,f7972,f5563])).
% 12.03/2.43 fof(f7998,plain,(
% 12.03/2.43 ![X0]: (c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X0)=X0|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____))|~sQ129_spl)),
% 12.03/2.43 inference(resolution,[status(thm)],[f7973,f1321])).
% 12.03/2.43 fof(f8024,plain,(
% 12.03/2.43 c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____))=c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____)|c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____))=c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____)|~sQ129_spl),
% 12.03/2.43 inference(resolution,[status(thm)],[f7998,f7973])).
% 12.03/2.43 fof(f8030,plain,(
% 12.03/2.43 sQ37_spl|~sQ129_spl),
% 12.03/2.43 inference(split_clause,[status(thm)],[f8024,f5556,f7972])).
% 12.03/2.43 fof(f8348,plain,(
% 12.03/2.43 c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),v_m____),v_r)),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))|c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_c____)),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))|~sQ20_spl),
% 12.03/2.43 inference(paramodulation,[status(thm)],[f5191,f5433])).
% 12.03/2.43 fof(f8403,plain,(
% 12.03/2.43 sQ14_spl|sQ32_spl|~sQ20_spl),
% 12.03/2.43 inference(split_clause,[status(thm)],[f8348,f5149,f5525,f5190])).
% 12.03/2.43 fof(f8408,plain,(
% 12.03/2.43 c_Groups_Ozero__class_Ozero(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_Ozero__class_Ozero(tc_RealDef_Oreal))|~sQ15_spl|~sQ20_spl),
% 12.03/2.43 inference(backward_demodulation,[status(thm)],[f5153,f5191])).
% 12.03/2.43 fof(f8416,plain,(
% 12.03/2.43 c_Groups_Ozero__class_Ozero(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____))|~sQ15_spl|~sQ20_spl),
% 12.03/2.43 inference(forward_demodulation,[status(thm)],[f5031,f8408])).
% 12.03/2.43 fof(f8428,plain,(
% 12.03/2.43 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))|~sQ15_spl|~sQ20_spl|~sQ37_spl),
% 12.03/2.43 inference(backward_demodulation,[status(thm)],[f8416,f5561])).
% 12.03/2.43 fof(f8469,plain,(
% 12.03/2.43 $false|~sQ15_spl|~sQ20_spl|~sQ37_spl),
% 12.03/2.43 inference(forward_subsumption_resolution,[status(thm)],[f8428,f4908])).
% 12.03/2.43 fof(f8470,plain,(
% 12.03/2.43 ~sQ15_spl|~sQ20_spl|~sQ37_spl),
% 12.03/2.43 inference(contradiction_clause,[status(thm)],[f8469])).
% 12.03/2.43 fof(f8471,plain,(
% 12.03/2.43 $false),
% 12.03/2.43 inference(sat_refutation,[status(thm)],[f5089,f5092,f5141,f5155,f5162,f5193,f5531,f5551,f5583,f5728,f5732,f5943,f6319,f6352,f7066,f7554,f7975,f8030,f8403,f8470])).
% 12.03/2.45 % SZS output end CNFRefutation for theBenchmark.p
% 8.53/2.49 % Elapsed time: 2.023705 seconds
% 8.53/2.49 % CPU time: 14.654518 seconds
% 8.53/2.49 % Total memory used: 319.937 MB
% 8.53/2.49 % Net memory used: 313.362 MB
%------------------------------------------------------------------------------