%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW222+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 : n011.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:50 PM UTC 2026
% Result : Theorem 56.13s 7.73s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWW222+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.42 % Computer : n011.cluster.edu
% 0.16/0.42 % Model : x86_64 x86_64
% 0.16/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.42 % Memory : 8046.5625MB
% 0.16/0.42 % 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:42:11 UTC 2026
% 0.16/0.43 % CPUTime :
% 0.26/0.58 % Drodi V4.1.1
% 56.13/7.73 % Refutation found
% 56.13/7.73 % SZS status Theorem for theBenchmark: Theorem is valid
% 56.13/7.73 % SZS output start CNFRefutation for theBenchmark
% 56.13/7.73 fof(f3,axiom,(
% 56.13/7.73 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_wa____,v_z____)),v_d____) ),
% 56.13/7.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 56.13/7.73 fof(f5,axiom,(
% 56.13/7.73 ( ( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_wa____,v_z____)))& c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_wa____,v_z____)),v_d____) )=> c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_wa____),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))) ) ),
% 56.13/7.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 56.13/7.73 fof(f7,axiom,(
% 56.13/7.73 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))) ),
% 56.13/7.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 56.13/7.73 fof(f15,axiom,(
% 56.13/7.73 (! [V_a,T_a] :( class_RealVector_Oreal__normed__vector(T_a)=> c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(T_a,V_a)) = c_RealVector_Onorm__class_Onorm(T_a,V_a) ) )),
% 56.13/7.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 56.13/7.73 fof(f19,axiom,(
% 56.13/7.73 (! [T_a] :( class_RealVector_Oreal__normed__vector(T_a)=> c_RealVector_Onorm__class_Onorm(T_a,c_Groups_Ozero__class_Ozero(T_a)) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) ) )),
% 56.13/7.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 56.13/7.73 fof(f21,axiom,(
% 56.13/7.73 (! [V_x_2,T_a] :( class_RealVector_Oreal__normed__vector(T_a)=> ( c_RealVector_Onorm__class_Onorm(T_a,V_x_2) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)<=> V_x_2 = c_Groups_Ozero__class_Ozero(T_a) ) ) )),
% 56.13/7.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 56.13/7.73 fof(f31,axiom,(
% 56.13/7.73 (! [V_r] : c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,V_r) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,V_r) )),
% 56.13/7.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 56.13/7.73 fof(f79,axiom,(
% 56.13/7.73 (! [V_r] :( ( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_r,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))=> c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,V_r) = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,V_r) )& ( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_r,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))=> c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,V_r) = V_r ) ) )),
% 56.13/7.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 56.13/7.73 fof(f120,axiom,(
% 56.13/7.73 (! [V_a,T_a] :( class_Groups_Ogroup__add(T_a)=> c_Groups_Ominus__class_Ominus(T_a,V_a,V_a) = c_Groups_Ozero__class_Ozero(T_a) ) )),
% 56.13/7.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 56.13/7.73 fof(f121,axiom,(
% 56.13/7.73 (! [V_b_2,V_a_2,T_a] :( class_Groups_Oab__group__add(T_a)=> ( V_a_2 = V_b_2<=> c_Groups_Ominus__class_Ominus(T_a,V_a_2,V_b_2) = c_Groups_Ozero__class_Ozero(T_a) ) ) )),
% 56.13/7.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 56.13/7.73 fof(f126,axiom,(
% 56.13/7.73 (! [V_a_2,T_a] :( class_Groups_Olinordered__ab__group__add(T_a)=> ( V_a_2 = c_Groups_Ouminus__class_Ouminus(T_a,V_a_2)<=> V_a_2 = c_Groups_Ozero__class_Ozero(T_a) ) ) )),
% 56.13/7.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 56.13/7.73 fof(f138,axiom,(
% 56.13/7.73 (! [V_a,T_a] :( class_Groups_Oordered__ab__group__add__abs(T_a)=> c_Groups_Oabs__class_Oabs(T_a,c_Groups_Ouminus__class_Ouminus(T_a,V_a)) = c_Groups_Oabs__class_Oabs(T_a,V_a) ) )),
% 56.13/7.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 56.13/7.73 fof(f221,axiom,(
% 56.13/7.73 (! [V_a,T_a] :( class_Groups_Omonoid__add(T_a)=> c_Groups_Oplus__class_Oplus(T_a,V_a,c_Groups_Ozero__class_Ozero(T_a)) = V_a ) )),
% 56.13/7.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 56.13/7.73 fof(f307,axiom,(
% 56.13/7.73 (! [V_y,V_x] : c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,V_x,V_y) = c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,V_x,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,V_y)) )),
% 56.13/7.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 56.13/7.73 fof(f309,axiom,(
% 56.13/7.73 (! [V_y,V_x] : c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,V_x,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,V_y))) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,V_y,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,V_x))) )),
% 56.13/7.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 56.13/7.73 fof(f323,axiom,(
% 56.13/7.73 (! [V_y_2,V_x_2] :( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,V_x_2,V_y_2))<=> c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,V_x_2),V_y_2) ) )),
% 56.13/7.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 56.13/7.73 fof(f1099,axiom,(
% 56.13/7.73 class_Groups_Oordered__ab__group__add__abs(tc_RealDef_Oreal) ),
% 56.13/7.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 56.13/7.73 fof(f1102,axiom,(
% 56.13/7.73 class_Groups_Olinordered__ab__group__add(tc_RealDef_Oreal) ),
% 56.13/7.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 56.13/7.73 fof(f1138,axiom,(
% 56.13/7.73 class_Groups_Omonoid__add(tc_RealDef_Oreal) ),
% 56.13/7.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 56.13/7.73 fof(f1162,axiom,(
% 56.13/7.73 class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex) ),
% 56.13/7.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 56.13/7.73 fof(f1177,axiom,(
% 56.13/7.73 class_Groups_Oab__group__add(tc_Complex_Ocomplex) ),
% 56.13/7.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 56.13/7.73 fof(f1183,axiom,(
% 56.13/7.73 class_Groups_Ogroup__add(tc_Complex_Ocomplex) ),
% 56.13/7.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 56.13/7.73 fof(f1251,conjecture,(
% 56.13/7.73 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_wa____),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))) ),
% 56.13/7.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 56.13/7.73 fof(f1252,negated_conjecture,(
% 56.13/7.73 ~(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_wa____),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))) )),
% 56.13/7.73 inference(negated_conjecture,[status(cth)],[f1251])).
% 56.13/7.73 fof(f1257,plain,(
% 56.13/7.73 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_wa____,v_z____)),v_d____)),
% 56.13/7.73 inference(cnf_transformation,[status(thm)],[f3])).
% 56.13/7.73 fof(f1259,plain,(
% 56.13/7.73 (~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_wa____,v_z____)))|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_wa____,v_z____)),v_d____))|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_wa____),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))),
% 56.13/7.73 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 56.13/7.73 fof(f1260,plain,(
% 56.13/7.73 ~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_wa____,v_z____)))|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_wa____,v_z____)),v_d____)|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_wa____),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))),
% 56.13/7.73 inference(cnf_transformation,[status(thm)],[f1259])).
% 56.13/7.73 fof(f1263,plain,(
% 56.13/7.73 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))),
% 56.13/7.73 inference(cnf_transformation,[status(thm)],[f7])).
% 56.13/7.73 fof(f1290,plain,(
% 56.13/7.73 ![V_a,T_a]: (~class_RealVector_Oreal__normed__vector(T_a)|c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(T_a,V_a))=c_RealVector_Onorm__class_Onorm(T_a,V_a))),
% 56.13/7.73 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 56.13/7.73 fof(f1291,plain,(
% 56.13/7.73 ![T_a]: (~class_RealVector_Oreal__normed__vector(T_a)|(![V_a]: c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(T_a,V_a))=c_RealVector_Onorm__class_Onorm(T_a,V_a)))),
% 56.13/7.73 inference(miniscoping,[status(thm)],[f1290])).
% 56.13/7.73 fof(f1292,plain,(
% 56.13/7.73 ![X0,X1]: (~class_RealVector_Oreal__normed__vector(X0)|c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(X0,X1))=c_RealVector_Onorm__class_Onorm(X0,X1))),
% 56.13/7.73 inference(cnf_transformation,[status(thm)],[f1291])).
% 56.13/7.73 fof(f1300,plain,(
% 56.13/7.73 ![T_a]: (~class_RealVector_Oreal__normed__vector(T_a)|c_RealVector_Onorm__class_Onorm(T_a,c_Groups_Ozero__class_Ozero(T_a))=c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))),
% 56.13/7.73 inference(pre_NNF_transformation,[status(thm)],[f19])).
% 56.13/7.73 fof(f1301,plain,(
% 56.13/7.73 ![X0]: (~class_RealVector_Oreal__normed__vector(X0)|c_RealVector_Onorm__class_Onorm(X0,c_Groups_Ozero__class_Ozero(X0))=c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))),
% 56.13/7.73 inference(cnf_transformation,[status(thm)],[f1300])).
% 56.13/7.73 fof(f1305,plain,(
% 56.13/7.73 ![V_x_2,T_a]: (~class_RealVector_Oreal__normed__vector(T_a)|(c_RealVector_Onorm__class_Onorm(T_a,V_x_2)=c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)<=>V_x_2=c_Groups_Ozero__class_Ozero(T_a)))),
% 56.13/7.73 inference(pre_NNF_transformation,[status(thm)],[f21])).
% 56.13/7.73 fof(f1306,plain,(
% 56.13/7.73 ![V_x_2,T_a]: (~class_RealVector_Oreal__normed__vector(T_a)|((~c_RealVector_Onorm__class_Onorm(T_a,V_x_2)=c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)|V_x_2=c_Groups_Ozero__class_Ozero(T_a))&(c_RealVector_Onorm__class_Onorm(T_a,V_x_2)=c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)|~V_x_2=c_Groups_Ozero__class_Ozero(T_a))))),
% 56.13/7.73 inference(NNF_transformation,[status(thm)],[f1305])).
% 56.13/7.73 fof(f1307,plain,(
% 56.13/7.73 ![T_a]: (~class_RealVector_Oreal__normed__vector(T_a)|((![V_x_2]: (~c_RealVector_Onorm__class_Onorm(T_a,V_x_2)=c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)|V_x_2=c_Groups_Ozero__class_Ozero(T_a)))&(![V_x_2]: (c_RealVector_Onorm__class_Onorm(T_a,V_x_2)=c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)|~V_x_2=c_Groups_Ozero__class_Ozero(T_a)))))),
% 56.13/7.73 inference(miniscoping,[status(thm)],[f1306])).
% 56.13/7.73 fof(f1308,plain,(
% 56.13/7.73 ![X0,X1]: (~class_RealVector_Oreal__normed__vector(X0)|~c_RealVector_Onorm__class_Onorm(X0,X1)=c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)|X1=c_Groups_Ozero__class_Ozero(X0))),
% 56.13/7.73 inference(cnf_transformation,[status(thm)],[f1307])).
% 56.13/7.73 fof(f1331,plain,(
% 56.13/7.73 ![X0]: (c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X0)=c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0))),
% 56.13/7.73 inference(cnf_transformation,[status(thm)],[f31])).
% 56.13/7.73 fof(f1484,plain,(
% 56.13/7.73 ![V_r]: ((~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_r,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))|c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,V_r)=c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,V_r))&(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_r,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))|c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,V_r)=V_r))),
% 56.13/7.73 inference(pre_NNF_transformation,[status(thm)],[f79])).
% 56.13/7.73 fof(f1485,plain,(
% 56.13/7.73 (![V_r]: (~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_r,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))|c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,V_r)=c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,V_r)))&(![V_r]: (c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_r,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))|c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,V_r)=V_r))),
% 56.13/7.73 inference(miniscoping,[status(thm)],[f1484])).
% 56.13/7.73 fof(f1487,plain,(
% 56.13/7.73 ![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)),
% 56.13/7.73 inference(cnf_transformation,[status(thm)],[f1485])).
% 56.13/7.73 fof(f1615,plain,(
% 56.13/7.73 ![V_a,T_a]: (~class_Groups_Ogroup__add(T_a)|c_Groups_Ominus__class_Ominus(T_a,V_a,V_a)=c_Groups_Ozero__class_Ozero(T_a))),
% 56.13/7.73 inference(pre_NNF_transformation,[status(thm)],[f120])).
% 56.13/7.73 fof(f1616,plain,(
% 56.13/7.73 ![T_a]: (~class_Groups_Ogroup__add(T_a)|(![V_a]: c_Groups_Ominus__class_Ominus(T_a,V_a,V_a)=c_Groups_Ozero__class_Ozero(T_a)))),
% 56.13/7.73 inference(miniscoping,[status(thm)],[f1615])).
% 56.13/7.73 fof(f1617,plain,(
% 56.13/7.73 ![X0,X1]: (~class_Groups_Ogroup__add(X0)|c_Groups_Ominus__class_Ominus(X0,X1,X1)=c_Groups_Ozero__class_Ozero(X0))),
% 56.13/7.73 inference(cnf_transformation,[status(thm)],[f1616])).
% 56.13/7.73 fof(f1618,plain,(
% 56.13/7.73 ![V_b_2,V_a_2,T_a]: (~class_Groups_Oab__group__add(T_a)|(V_a_2=V_b_2<=>c_Groups_Ominus__class_Ominus(T_a,V_a_2,V_b_2)=c_Groups_Ozero__class_Ozero(T_a)))),
% 56.13/7.73 inference(pre_NNF_transformation,[status(thm)],[f121])).
% 56.13/7.73 fof(f1619,plain,(
% 56.13/7.73 ![V_b_2,V_a_2,T_a]: (~class_Groups_Oab__group__add(T_a)|((~V_a_2=V_b_2|c_Groups_Ominus__class_Ominus(T_a,V_a_2,V_b_2)=c_Groups_Ozero__class_Ozero(T_a))&(V_a_2=V_b_2|~c_Groups_Ominus__class_Ominus(T_a,V_a_2,V_b_2)=c_Groups_Ozero__class_Ozero(T_a))))),
% 56.13/7.73 inference(NNF_transformation,[status(thm)],[f1618])).
% 56.13/7.73 fof(f1620,plain,(
% 56.13/7.73 ![T_a]: (~class_Groups_Oab__group__add(T_a)|((![V_b_2,V_a_2]: (~V_a_2=V_b_2|c_Groups_Ominus__class_Ominus(T_a,V_a_2,V_b_2)=c_Groups_Ozero__class_Ozero(T_a)))&(![V_b_2,V_a_2]: (V_a_2=V_b_2|~c_Groups_Ominus__class_Ominus(T_a,V_a_2,V_b_2)=c_Groups_Ozero__class_Ozero(T_a)))))),
% 56.13/7.73 inference(miniscoping,[status(thm)],[f1619])).
% 56.13/7.73 fof(f1622,plain,(
% 56.13/7.73 ![X0,X1,X2]: (~class_Groups_Oab__group__add(X0)|X1=X2|~c_Groups_Ominus__class_Ominus(X0,X1,X2)=c_Groups_Ozero__class_Ozero(X0))),
% 56.13/7.73 inference(cnf_transformation,[status(thm)],[f1620])).
% 56.13/7.73 fof(f1640,plain,(
% 56.13/7.73 ![V_a_2,T_a]: (~class_Groups_Olinordered__ab__group__add(T_a)|(V_a_2=c_Groups_Ouminus__class_Ouminus(T_a,V_a_2)<=>V_a_2=c_Groups_Ozero__class_Ozero(T_a)))),
% 56.13/7.73 inference(pre_NNF_transformation,[status(thm)],[f126])).
% 56.13/7.73 fof(f1641,plain,(
% 56.13/7.73 ![V_a_2,T_a]: (~class_Groups_Olinordered__ab__group__add(T_a)|((~V_a_2=c_Groups_Ouminus__class_Ouminus(T_a,V_a_2)|V_a_2=c_Groups_Ozero__class_Ozero(T_a))&(V_a_2=c_Groups_Ouminus__class_Ouminus(T_a,V_a_2)|~V_a_2=c_Groups_Ozero__class_Ozero(T_a))))),
% 56.13/7.73 inference(NNF_transformation,[status(thm)],[f1640])).
% 56.13/7.73 fof(f1642,plain,(
% 56.13/7.73 ![T_a]: (~class_Groups_Olinordered__ab__group__add(T_a)|((![V_a_2]: (~V_a_2=c_Groups_Ouminus__class_Ouminus(T_a,V_a_2)|V_a_2=c_Groups_Ozero__class_Ozero(T_a)))&(![V_a_2]: (V_a_2=c_Groups_Ouminus__class_Ouminus(T_a,V_a_2)|~V_a_2=c_Groups_Ozero__class_Ozero(T_a)))))),
% 56.13/7.73 inference(miniscoping,[status(thm)],[f1641])).
% 56.13/7.73 fof(f1643,plain,(
% 56.13/7.73 ![X0,X1]: (~class_Groups_Olinordered__ab__group__add(X0)|~X1=c_Groups_Ouminus__class_Ouminus(X0,X1)|X1=c_Groups_Ozero__class_Ozero(X0))),
% 56.13/7.73 inference(cnf_transformation,[status(thm)],[f1642])).
% 56.13/7.73 fof(f1689,plain,(
% 56.13/7.73 ![V_a,T_a]: (~class_Groups_Oordered__ab__group__add__abs(T_a)|c_Groups_Oabs__class_Oabs(T_a,c_Groups_Ouminus__class_Ouminus(T_a,V_a))=c_Groups_Oabs__class_Oabs(T_a,V_a))),
% 56.13/7.73 inference(pre_NNF_transformation,[status(thm)],[f138])).
% 56.13/7.73 fof(f1690,plain,(
% 56.13/7.73 ![T_a]: (~class_Groups_Oordered__ab__group__add__abs(T_a)|(![V_a]: c_Groups_Oabs__class_Oabs(T_a,c_Groups_Ouminus__class_Ouminus(T_a,V_a))=c_Groups_Oabs__class_Oabs(T_a,V_a)))),
% 56.13/7.73 inference(miniscoping,[status(thm)],[f1689])).
% 56.13/7.73 fof(f1691,plain,(
% 56.13/7.73 ![X0,X1]: (~class_Groups_Oordered__ab__group__add__abs(X0)|c_Groups_Oabs__class_Oabs(X0,c_Groups_Ouminus__class_Ouminus(X0,X1))=c_Groups_Oabs__class_Oabs(X0,X1))),
% 56.13/7.73 inference(cnf_transformation,[status(thm)],[f1690])).
% 56.13/7.73 fof(f1973,plain,(
% 56.13/7.73 ![V_a,T_a]: (~class_Groups_Omonoid__add(T_a)|c_Groups_Oplus__class_Oplus(T_a,V_a,c_Groups_Ozero__class_Ozero(T_a))=V_a)),
% 56.13/7.73 inference(pre_NNF_transformation,[status(thm)],[f221])).
% 56.13/7.73 fof(f1974,plain,(
% 56.13/7.73 ![T_a]: (~class_Groups_Omonoid__add(T_a)|(![V_a]: c_Groups_Oplus__class_Oplus(T_a,V_a,c_Groups_Ozero__class_Ozero(T_a))=V_a))),
% 56.13/7.73 inference(miniscoping,[status(thm)],[f1973])).
% 56.13/7.73 fof(f1975,plain,(
% 56.13/7.73 ![X0,X1]: (~class_Groups_Omonoid__add(X0)|c_Groups_Oplus__class_Oplus(X0,X1,c_Groups_Ozero__class_Ozero(X0))=X1)),
% 56.13/7.73 inference(cnf_transformation,[status(thm)],[f1974])).
% 56.13/7.73 fof(f2270,plain,(
% 56.13/7.73 ![X0,X1]: (c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X0,X1)=c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X1)))),
% 56.13/7.73 inference(cnf_transformation,[status(thm)],[f307])).
% 56.13/7.73 fof(f2272,plain,(
% 56.13/7.73 ![X0,X1]: (c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X1)))=c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0))))),
% 56.13/7.73 inference(cnf_transformation,[status(thm)],[f309])).
% 56.13/7.73 fof(f2311,plain,(
% 56.13/7.73 ![V_y_2,V_x_2]: ((~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,V_x_2,V_y_2))|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,V_x_2),V_y_2))&(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,V_x_2,V_y_2))|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,V_x_2),V_y_2)))),
% 56.13/7.73 inference(NNF_transformation,[status(thm)],[f323])).
% 56.13/7.73 fof(f2312,plain,(
% 56.13/7.73 (![V_y_2,V_x_2]: (~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,V_x_2,V_y_2))|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,V_x_2),V_y_2)))&(![V_y_2,V_x_2]: (c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,V_x_2,V_y_2))|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,V_x_2),V_y_2)))),
% 56.13/7.73 inference(miniscoping,[status(thm)],[f2311])).
% 56.13/7.73 fof(f2314,plain,(
% 56.13/7.73 ![X0,X1]: (c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X1))|~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0),X1))),
% 56.13/7.73 inference(cnf_transformation,[status(thm)],[f2312])).
% 56.13/7.73 fof(f4492,plain,(
% 56.13/7.73 class_Groups_Oordered__ab__group__add__abs(tc_RealDef_Oreal)),
% 56.13/7.73 inference(cnf_transformation,[status(thm)],[f1099])).
% 56.13/7.73 fof(f4495,plain,(
% 56.13/7.73 class_Groups_Olinordered__ab__group__add(tc_RealDef_Oreal)),
% 56.13/7.73 inference(cnf_transformation,[status(thm)],[f1102])).
% 56.13/7.73 fof(f4531,plain,(
% 56.13/7.73 class_Groups_Omonoid__add(tc_RealDef_Oreal)),
% 56.13/7.73 inference(cnf_transformation,[status(thm)],[f1138])).
% 56.13/7.73 fof(f4555,plain,(
% 56.13/7.73 class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex)),
% 56.13/7.73 inference(cnf_transformation,[status(thm)],[f1162])).
% 56.13/7.73 fof(f4570,plain,(
% 56.13/7.73 class_Groups_Oab__group__add(tc_Complex_Ocomplex)),
% 56.13/7.73 inference(cnf_transformation,[status(thm)],[f1177])).
% 56.13/7.73 fof(f4576,plain,(
% 56.13/7.73 class_Groups_Ogroup__add(tc_Complex_Ocomplex)),
% 56.13/7.73 inference(cnf_transformation,[status(thm)],[f1183])).
% 56.13/7.73 fof(f4699,plain,(
% 56.13/7.73 ~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_wa____),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))),
% 56.13/7.73 inference(cnf_transformation,[status(thm)],[f1252])).
% 56.13/7.73 fof(f4858,plain,(
% 56.13/7.73 ~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_wa____,v_z____)))|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_wa____),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))),
% 56.13/7.73 inference(forward_subsumption_resolution,[status(thm)],[f1260,f1257])).
% 56.13/7.73 fof(f4874,plain,(
% 56.13/7.73 ~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_wa____,v_z____)))|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_wa____),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))),
% 56.13/7.73 inference(backward_demodulation,[status(thm)],[f1331,f4858])).
% 56.13/7.73 fof(f4875,plain,(
% 56.13/7.73 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))),
% 56.13/7.73 inference(backward_demodulation,[status(thm)],[f1331,f1263])).
% 56.13/7.73 fof(f4877,plain,(
% 56.13/7.73 ~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_wa____),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))),
% 56.13/7.73 inference(backward_demodulation,[status(thm)],[f1331,f4699])).
% 56.13/7.73 fof(f4944,plain,(
% 56.13/7.73 ![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)),
% 56.13/7.73 inference(forward_demodulation,[status(thm)],[f1331,f1487])).
% 56.13/7.73 fof(f5171,plain,(
% 56.13/7.73 ![X0,X1]: (~class_RealVector_Oreal__normed__vector(X0)|c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(X0,X1))=c_RealVector_Onorm__class_Onorm(X0,X1))),
% 56.13/7.73 inference(forward_demodulation,[status(thm)],[f1331,f1292])).
% 56.13/7.73 fof(f5639,plain,(
% 56.13/7.73 ![X0]: (~c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,X0)=c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)|X0=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex))),
% 56.13/7.73 inference(resolution,[status(thm)],[f4555,f1308])).
% 56.13/7.73 fof(f5640,plain,(
% 56.13/7.73 c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex))=c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),
% 56.13/7.73 inference(resolution,[status(thm)],[f4555,f1301])).
% 56.13/7.73 fof(f5641,plain,(
% 56.13/7.73 ![X0]: (c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,X0))=c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,X0))),
% 56.13/7.73 inference(resolution,[status(thm)],[f4555,f5171])).
% 56.13/7.73 fof(f6012,plain,(
% 56.13/7.73 ![X0,X1]: (c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X1)))=c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0))))),
% 56.13/7.73 inference(forward_demodulation,[status(thm)],[f1331,f2272])).
% 56.13/7.73 fof(f6013,plain,(
% 56.13/7.73 ![X0,X1]: (c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X0,X1))=c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0))))),
% 56.13/7.73 inference(forward_demodulation,[status(thm)],[f2270,f6012])).
% 56.13/7.73 fof(f6014,plain,(
% 56.13/7.73 ![X0,X1]: (c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X0,X1))=c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0))))),
% 56.13/7.73 inference(forward_demodulation,[status(thm)],[f1331,f6013])).
% 56.13/7.73 fof(f6017,plain,(
% 56.13/7.73 ~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_wa____),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))),
% 56.13/7.73 inference(backward_demodulation,[status(thm)],[f6020,f4877])).
% 56.13/7.73 fof(f6020,plain,(
% 56.13/7.73 ![X0,X1]: (c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X0,X1))=c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X1,X0)))),
% 56.13/7.73 inference(forward_demodulation,[status(thm)],[f2270,f6014])).
% 56.13/7.73 fof(f6177,plain,(
% 56.13/7.73 ![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,X0,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)))|c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0))=c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0))),
% 56.13/7.73 inference(resolution,[status(thm)],[f2314,f4944])).
% 56.13/7.73 fof(f10726,plain,(
% 56.13/7.73 ![X0]: (c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,X0,X0)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex))),
% 56.13/7.73 inference(resolution,[status(thm)],[f1617,f4576])).
% 56.13/7.73 fof(f10981,plain,(
% 56.13/7.73 ![X0,X1]: (X0=X1|~c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,X0,X1)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex))),
% 56.13/7.73 inference(resolution,[status(thm)],[f1622,f4570])).
% 56.13/7.73 fof(f12164,plain,(
% 56.13/7.73 ![X0]: (~X0=c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0)|X0=c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))),
% 56.13/7.73 inference(resolution,[status(thm)],[f1643,f4495])).
% 56.13/7.73 fof(f15121,plain,(
% 56.13/7.73 ![X0]: (c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0))=c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0))),
% 56.13/7.73 inference(resolution,[status(thm)],[f1691,f4492])).
% 56.13/7.73 fof(f15123,plain,(
% 56.13/7.73 ![X0]: (c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0))=c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0))),
% 56.13/7.73 inference(forward_demodulation,[status(thm)],[f1331,f15121])).
% 56.13/7.73 fof(f15124,plain,(
% 56.13/7.73 ![X0]: (c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0))=c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X0))),
% 56.13/7.73 inference(forward_demodulation,[status(thm)],[f1331,f15123])).
% 56.13/7.73 fof(f17830,plain,(
% 56.13/7.73 ~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_wa____,v_z____)))|c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_wa____),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))),
% 56.13/7.73 inference(forward_demodulation,[status(thm)],[f6020,f4874])).
% 56.13/7.73 fof(f17831,plain,(
% 56.13/7.73 ~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_wa____,v_z____)))),
% 56.13/7.73 inference(forward_subsumption_resolution,[status(thm)],[f17830,f6017])).
% 56.13/7.73 fof(f17832,plain,(
% 56.13/7.73 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____)))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))),
% 56.13/7.73 inference(forward_demodulation,[status(thm)],[f6020,f4875])).
% 56.13/7.73 fof(f18716,plain,(
% 56.13/7.73 ![X0]: (c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))=X0)),
% 56.13/7.73 inference(resolution,[status(thm)],[f1975,f4531])).
% 56.13/7.73 fof(f33602,plain,(
% 56.13/7.73 ![X0]: (c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),X0)|c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0))=c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0))),
% 56.13/7.74 inference(forward_demodulation,[status(thm)],[f18716,f6177])).
% 56.13/7.74 fof(f33603,plain,(
% 56.13/7.74 ![X0]: (c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),X0)|c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X0)=c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0))),
% 56.13/7.74 inference(forward_demodulation,[status(thm)],[f15124,f33602])).
% 56.13/7.74 fof(f33607,plain,(
% 56.13/7.74 c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_wa____,v_z____)))=c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_wa____,v_z____)))),
% 56.13/7.74 inference(resolution,[status(thm)],[f33603,f17831])).
% 56.13/7.74 fof(f33653,plain,(
% 56.13/7.74 c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_wa____,v_z____))=c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_wa____,v_z____)))),
% 56.13/7.74 inference(forward_demodulation,[status(thm)],[f5641,f33607])).
% 56.13/7.74 fof(f33988,plain,(
% 56.13/7.74 c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_wa____,v_z____))=c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),
% 56.13/7.74 inference(resolution,[status(thm)],[f33653,f12164])).
% 56.13/7.74 fof(f57753,plain,(
% 56.13/7.74 c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_wa____,v_z____)=c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)),
% 56.13/7.74 inference(resolution,[status(thm)],[f5639,f33988])).
% 56.13/7.74 fof(f58493,plain,(
% 56.13/7.74 v_wa____=v_z____),
% 56.13/7.74 inference(resolution,[status(thm)],[f57753,f10981])).
% 56.13/7.74 fof(f58544,plain,(
% 56.13/7.74 c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_wa____)))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))),
% 56.13/7.74 inference(backward_demodulation,[status(thm)],[f58493,f17832])).
% 56.13/7.74 fof(f58546,plain,(
% 56.13/7.74 ~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_wa____),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_z____))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_wa____)))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))),
% 23.45/7.85 inference(backward_demodulation,[status(thm)],[f58493,f6017])).
% 23.45/7.85 fof(f58559,plain,(
% 23.45/7.85 ~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_wa____),hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_wa____))),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_wa____)))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))),
% 23.45/7.85 inference(forward_demodulation,[status(thm)],[f58493,f58546])).
% 23.45/7.85 fof(f58560,plain,(
% 23.45/7.85 ~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_wa____)))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))),
% 23.45/7.85 inference(forward_demodulation,[status(thm)],[f10726,f58559])).
% 23.45/7.85 fof(f58561,plain,(
% 23.45/7.85 ~c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),v_wa____)))),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))),
% 23.45/7.85 inference(forward_demodulation,[status(thm)],[f5640,f58560])).
% 23.45/7.85 fof(f61644,plain,(
% 23.45/7.85 $false),
% 23.45/7.85 inference(forward_subsumption_resolution,[status(thm)],[f58561,f58544])).
% 23.45/7.85 % SZS output end CNFRefutation for theBenchmark.p
% 23.45/7.90 % Elapsed time: 7.447745 seconds
% 23.45/7.90 % CPU time: 57.331259 seconds
% 23.45/7.90 % Total memory used: 660.069 MB
% 23.45/7.90 % Net memory used: 635.315 MB
%------------------------------------------------------------------------------