%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW231+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 : n005.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 279.90s 41.12s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW231+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.13/5.41 % Computer : n005.cluster.edu
% 0.13/5.41 % Model : x86_64 x86_64
% 0.13/5.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/5.41 % Memory : 8046.5625MB
% 0.13/5.41 % OS : Linux 6.8.0-71-generic
% 0.13/5.41 % CPULimit : 300
% 0.13/5.41 % WCLimit : 300
% 0.13/5.41 % DateTime : Mon Sep 21 09:42:09 UTC 2026
% 0.13/5.41 % CPUTime :
% 0.17/5.55 % Drodi V4.1.1
% 279.90/41.12 % Refutation found
% 279.90/41.12 % SZS status Theorem for theBenchmark: Theorem is valid
% 279.90/41.12 % SZS output start CNFRefutation for theBenchmark
% 279.90/41.12 fof(f3,axiom,(
% 279.90/41.12 (! [V_x] : c_NthRoot_Osqrt(hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),V_x),V_x)) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,V_x) )),
% 279.90/41.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 279.90/41.12 fof(f5,axiom,(
% 279.90/41.12 (! [V_y,V_x] : c_NthRoot_Osqrt(hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),V_x),V_y)) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_NthRoot_Osqrt(V_x)),c_NthRoot_Osqrt(V_y)) )),
% 279.90/41.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 279.90/41.12 fof(f6,axiom,(
% 279.90/41.12 (! [V_w,V_z2,V_z1] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,V_z1,V_z2)),V_w) = c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),V_z1),V_w),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),V_z2),V_w)) )),
% 279.90/41.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 279.90/41.12 fof(f26,axiom,(
% 279.90/41.12 (! [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) )),
% 279.90/41.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 279.90/41.12 fof(f27,axiom,(
% 279.90/41.12 (! [V_a,T_a] :( class_Groups_Oordered__ab__group__add__abs(T_a)=> c_Groups_Oabs__class_Oabs(T_a,c_Groups_Oabs__class_Oabs(T_a,V_a)) = c_Groups_Oabs__class_Oabs(T_a,V_a) ) )),
% 279.90/41.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 279.90/41.12 fof(f37,axiom,(
% 279.90/41.12 (! [V_b,V_r2,V_a,V_r1] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),c_Complex_Orcis(V_r1,V_a)),c_Complex_Orcis(V_r2,V_b)) = c_Complex_Orcis(hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),V_r1),V_r2),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,V_a,V_b)) )),
% 279.90/41.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 279.90/41.12 fof(f38,axiom,(
% 279.90/41.12 (! [V_y,V_x,T_a] :( class_RealVector_Oreal__normed__algebra(T_a)=> hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),c_Groups_Ouminus__class_Ouminus(T_a,V_x)),V_y) = c_Groups_Ouminus__class_Ouminus(T_a,hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_x),V_y)) ) )),
% 279.90/41.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 279.90/41.12 fof(f114,axiom,(
% 279.90/41.12 (! [V_a,V_r] : c_Complex_Orcis(V_r,V_a) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),c_RealVector_Oof__real(tc_Complex_Ocomplex,V_r)),c_Complex_Ocis(V_a)) )),
% 279.90/41.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 279.90/41.12 fof(f130,axiom,(
% 279.90/41.12 (! [V_r] : c_Complex_Orcis(V_r,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)) = c_RealVector_Oof__real(tc_Complex_Ocomplex,V_r) )),
% 279.90/41.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 279.90/41.12 fof(f145,axiom,(
% 279.90/41.12 (! [V_a,T_a] :( class_Rings_Ocomm__semiring__1(T_a)=> c_Groups_Oplus__class_Oplus(T_a,c_Groups_Ozero__class_Ozero(T_a),V_a) = V_a ) )),
% 279.90/41.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 279.90/41.12 fof(f220,axiom,(
% 279.90/41.12 (! [V_y_2,V_x_2] :( c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,V_x_2,V_y_2) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)<=> V_y_2 = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,V_x_2) ) )),
% 279.90/41.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 279.90/41.12 fof(f249,axiom,(
% 279.90/41.12 (! [V_r] : c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,V_r) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,V_r) )),
% 279.90/41.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 279.90/41.12 fof(f313,axiom,(
% 279.90/41.12 (! [V_d,V_c,V_b,V_a] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),c_Complex_Ocomplex_OComplex(V_a,V_b)),c_Complex_Ocomplex_OComplex(V_c,V_d)) = c_Complex_Ocomplex_OComplex(c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),V_a),V_c),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),V_b),V_d)),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),V_a),V_d),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),V_b),V_c))) )),
% 279.90/41.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 279.90/41.12 fof(f338,axiom,(
% 279.90/41.12 (! [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)) )),
% 279.90/41.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 279.90/41.12 fof(f340,axiom,(
% 279.90/41.12 (! [V_xa_2,V_y_2,V_x_2] :( c_Complex_Ocomplex_OComplex(V_x_2,V_y_2) = c_RealVector_Oof__real(tc_Complex_Ocomplex,V_xa_2)<=> ( V_x_2 = V_xa_2& V_y_2 = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) ) ) )),
% 279.90/41.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 279.90/41.12 fof(f349,axiom,(
% 279.90/41.12 (! [V_a] : c_Complex_Ocis(V_a) = c_Complex_Orcis(c_Groups_Oone__class_Oone(tc_RealDef_Oreal),V_a) )),
% 279.90/41.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 279.90/41.12 fof(f360,axiom,(
% 279.90/41.12 (! [V_x] : c_Transcendental_Ocos(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,V_x,c_Transcendental_Opi)) = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Transcendental_Ocos(V_x)) )),
% 279.90/41.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 279.90/41.12 fof(f409,axiom,(
% 279.90/41.12 c_Transcendental_Osin(c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) ),
% 279.90/41.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 279.90/41.12 fof(f445,axiom,(
% 279.90/41.12 c_Transcendental_Osin(c_Transcendental_Opi) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) ),
% 279.90/41.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 279.90/41.12 fof(f475,axiom,(
% 279.90/41.12 (! [V_x] : c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_Transcendental_Ocos(V_x)),c_Transcendental_Ocos(V_x)),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_Transcendental_Osin(V_x)),c_Transcendental_Osin(V_x))) = c_Groups_Oone__class_Oone(tc_RealDef_Oreal) )),
% 279.90/41.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 279.90/41.12 fof(f478,axiom,(
% 279.90/41.12 (! [V_y,V_x] : c_Transcendental_Ocos(c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,V_x,V_y)) = c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_Transcendental_Ocos(V_x)),c_Transcendental_Ocos(V_y)),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_Transcendental_Osin(V_x)),c_Transcendental_Osin(V_y))) )),
% 279.90/41.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 279.90/41.12 fof(f484,axiom,(
% 279.90/41.12 (! [V_b,V_a] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),c_Complex_Oii),c_Complex_Ocomplex_OComplex(V_a,V_b)) = c_Complex_Ocomplex_OComplex(c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,V_b),V_a) )),
% 279.90/41.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 279.90/41.12 fof(f937,axiom,(
% 279.90/41.12 c_Complex_ORe(c_Complex_Oii) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) ),
% 279.90/41.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 279.90/41.12 fof(f938,axiom,(
% 279.90/41.12 (! [V_z] : c_Complex_OIm(c_RealVector_Oof__real(tc_Complex_Ocomplex,V_z)) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) )),
% 279.90/41.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 279.90/41.12 fof(f942,axiom,(
% 279.90/41.12 (! [V_y,V_x] : c_Complex_OIm(c_Complex_Ocomplex_OComplex(V_x,V_y)) = V_y )),
% 279.90/41.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 279.90/41.12 fof(f943,axiom,(
% 279.90/41.12 (! [V_z] : c_Complex_ORe(c_RealVector_Oof__real(tc_Complex_Ocomplex,V_z)) = V_z )),
% 279.90/41.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 279.90/41.12 fof(f946,axiom,(
% 279.90/41.12 (! [V_z] : c_Complex_Ocomplex_OComplex(c_Complex_ORe(V_z),c_Complex_OIm(V_z)) = V_z )),
% 279.90/41.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 279.90/41.12 fof(f950,axiom,(
% 279.90/41.12 c_Complex_OIm(c_Complex_Oii) = c_Groups_Oone__class_Oone(tc_RealDef_Oreal) ),
% 279.90/41.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 279.90/41.12 fof(f955,axiom,(
% 279.90/41.12 (! [V_x] : c_Complex_OIm(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,V_x)) = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Complex_OIm(V_x)) )),
% 279.90/41.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 279.90/41.12 fof(f956,axiom,(
% 279.90/41.12 (! [V_x] : c_Complex_ORe(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,V_x)) = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Complex_ORe(V_x)) )),
% 279.90/41.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 279.90/41.12 fof(f965,axiom,(
% 279.90/41.12 (! [V_a,V_r] : c_Complex_OIm(c_Complex_Orcis(V_r,V_a)) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),V_r),c_Transcendental_Osin(V_a)) )),
% 279.90/41.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 279.90/41.12 fof(f966,axiom,(
% 279.90/41.12 (! [V_a,V_r] : c_Complex_ORe(c_Complex_Orcis(V_r,V_a)) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),V_r),c_Transcendental_Ocos(V_a)) )),
% 279.90/41.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 279.90/41.12 fof(f1111,axiom,(
% 279.90/41.12 class_Groups_Oordered__ab__group__add__abs(tc_RealDef_Oreal) ),
% 279.90/41.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 279.90/41.12 fof(f1138,axiom,(
% 279.90/41.12 class_Rings_Ocomm__semiring__1(tc_RealDef_Oreal) ),
% 279.90/41.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 279.90/41.12 fof(f1168,axiom,(
% 279.90/41.12 class_RealVector_Oreal__normed__algebra(tc_Complex_Ocomplex) ),
% 279.90/41.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 279.90/41.12 fof(f1201,conjecture,(
% 279.90/41.12 c_Complex_Orcis(hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_NthRoot_Osqrt(c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,v_r))),c_NthRoot_Osqrt(c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,v_r))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Transcendental_Opi,v_a)) = c_Complex_Orcis(c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,v_r)),v_a) ),
% 279.90/41.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 279.90/41.12 fof(f1202,negated_conjecture,(
% 279.90/41.12 ~(c_Complex_Orcis(hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_NthRoot_Osqrt(c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,v_r))),c_NthRoot_Osqrt(c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,v_r))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Transcendental_Opi,v_a)) = c_Complex_Orcis(c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,v_r)),v_a) )),
% 279.90/41.12 inference(negated_conjecture,[status(cth)],[f1201])).
% 279.90/41.12 fof(f1207,plain,(
% 279.90/41.12 ![X0]: (c_NthRoot_Osqrt(hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X0),X0))=c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0))),
% 279.90/41.12 inference(cnf_transformation,[status(thm)],[f3])).
% 279.90/41.12 fof(f1209,plain,(
% 279.90/41.12 ![X0,X1]: (c_NthRoot_Osqrt(hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X0),X1))=hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_NthRoot_Osqrt(X0)),c_NthRoot_Osqrt(X1)))),
% 279.90/41.12 inference(cnf_transformation,[status(thm)],[f5])).
% 279.90/41.12 fof(f1210,plain,(
% 279.90/41.12 ![X0,X1,X2]: (hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X1)),X2)=c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X0),X2),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X1),X2)))),
% 279.90/41.12 inference(cnf_transformation,[status(thm)],[f6])).
% 279.90/41.12 fof(f1276,plain,(
% 279.90/41.12 ![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))),
% 279.90/41.12 inference(cnf_transformation,[status(thm)],[f26])).
% 279.90/41.12 fof(f1277,plain,(
% 279.90/41.12 ![V_a,T_a]: (~class_Groups_Oordered__ab__group__add__abs(T_a)|c_Groups_Oabs__class_Oabs(T_a,c_Groups_Oabs__class_Oabs(T_a,V_a))=c_Groups_Oabs__class_Oabs(T_a,V_a))),
% 279.90/41.12 inference(pre_NNF_transformation,[status(thm)],[f27])).
% 279.90/41.12 fof(f1278,plain,(
% 279.90/41.12 ![T_a]: (~class_Groups_Oordered__ab__group__add__abs(T_a)|(![V_a]: c_Groups_Oabs__class_Oabs(T_a,c_Groups_Oabs__class_Oabs(T_a,V_a))=c_Groups_Oabs__class_Oabs(T_a,V_a)))),
% 279.90/41.12 inference(miniscoping,[status(thm)],[f1277])).
% 279.90/41.12 fof(f1279,plain,(
% 279.90/41.12 ![X0,X1]: (~class_Groups_Oordered__ab__group__add__abs(X0)|c_Groups_Oabs__class_Oabs(X0,c_Groups_Oabs__class_Oabs(X0,X1))=c_Groups_Oabs__class_Oabs(X0,X1))),
% 279.90/41.12 inference(cnf_transformation,[status(thm)],[f1278])).
% 279.90/41.12 fof(f1311,plain,(
% 279.90/41.12 ![X0,X1,X2,X3]: (hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),c_Complex_Orcis(X0,X1)),c_Complex_Orcis(X2,X3))=c_Complex_Orcis(hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X0),X2),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,X3)))),
% 279.90/41.12 inference(cnf_transformation,[status(thm)],[f37])).
% 279.90/41.12 fof(f1312,plain,(
% 279.90/41.12 ![V_y,V_x,T_a]: (~class_RealVector_Oreal__normed__algebra(T_a)|hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),c_Groups_Ouminus__class_Ouminus(T_a,V_x)),V_y)=c_Groups_Ouminus__class_Ouminus(T_a,hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_x),V_y)))),
% 279.90/41.12 inference(pre_NNF_transformation,[status(thm)],[f38])).
% 279.90/41.12 fof(f1313,plain,(
% 279.90/41.12 ![T_a]: (~class_RealVector_Oreal__normed__algebra(T_a)|(![V_y,V_x]: hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),c_Groups_Ouminus__class_Ouminus(T_a,V_x)),V_y)=c_Groups_Ouminus__class_Ouminus(T_a,hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_x),V_y))))),
% 279.90/41.12 inference(miniscoping,[status(thm)],[f1312])).
% 279.90/41.12 fof(f1314,plain,(
% 279.90/41.12 ![X0,X1,X2]: (~class_RealVector_Oreal__normed__algebra(X0)|hAPP(hAPP(c_Groups_Otimes__class_Otimes(X0),c_Groups_Ouminus__class_Ouminus(X0,X1)),X2)=c_Groups_Ouminus__class_Ouminus(X0,hAPP(hAPP(c_Groups_Otimes__class_Otimes(X0),X1),X2)))),
% 279.90/41.12 inference(cnf_transformation,[status(thm)],[f1313])).
% 279.90/41.12 fof(f1550,plain,(
% 279.90/41.12 ![X0,X1]: (c_Complex_Orcis(X0,X1)=hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),c_RealVector_Oof__real(tc_Complex_Ocomplex,X0)),c_Complex_Ocis(X1)))),
% 279.90/41.12 inference(cnf_transformation,[status(thm)],[f114])).
% 279.90/41.12 fof(f1604,plain,(
% 279.90/41.12 ![X0]: (c_Complex_Orcis(X0,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))=c_RealVector_Oof__real(tc_Complex_Ocomplex,X0))),
% 279.90/41.12 inference(cnf_transformation,[status(thm)],[f130])).
% 279.90/41.12 fof(f1648,plain,(
% 279.90/41.12 ![V_a,T_a]: (~class_Rings_Ocomm__semiring__1(T_a)|c_Groups_Oplus__class_Oplus(T_a,c_Groups_Ozero__class_Ozero(T_a),V_a)=V_a)),
% 279.90/41.12 inference(pre_NNF_transformation,[status(thm)],[f145])).
% 279.90/41.12 fof(f1649,plain,(
% 279.90/41.12 ![T_a]: (~class_Rings_Ocomm__semiring__1(T_a)|(![V_a]: c_Groups_Oplus__class_Oplus(T_a,c_Groups_Ozero__class_Ozero(T_a),V_a)=V_a))),
% 279.90/41.12 inference(miniscoping,[status(thm)],[f1648])).
% 279.90/41.12 fof(f1650,plain,(
% 279.90/41.12 ![X0,X1]: (~class_Rings_Ocomm__semiring__1(X0)|c_Groups_Oplus__class_Oplus(X0,c_Groups_Ozero__class_Ozero(X0),X1)=X1)),
% 279.90/41.12 inference(cnf_transformation,[status(thm)],[f1649])).
% 279.90/41.12 fof(f1923,plain,(
% 279.90/41.12 ![V_y_2,V_x_2]: ((~c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,V_x_2,V_y_2)=c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)|V_y_2=c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,V_x_2))&(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,V_x_2,V_y_2)=c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)|~V_y_2=c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,V_x_2)))),
% 279.90/41.12 inference(NNF_transformation,[status(thm)],[f220])).
% 279.90/41.12 fof(f1924,plain,(
% 279.90/41.12 (![V_y_2,V_x_2]: (~c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,V_x_2,V_y_2)=c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)|V_y_2=c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,V_x_2)))&(![V_y_2,V_x_2]: (c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,V_x_2,V_y_2)=c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)|~V_y_2=c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,V_x_2)))),
% 279.90/41.12 inference(miniscoping,[status(thm)],[f1923])).
% 279.90/41.12 fof(f1925,plain,(
% 279.90/41.12 ![X0,X1]: (~c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X1)=c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)|X1=c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0))),
% 279.90/41.12 inference(cnf_transformation,[status(thm)],[f1924])).
% 279.90/41.12 fof(f1926,plain,(
% 279.90/41.12 ![X0,X1]: (c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X1)=c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)|~X1=c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0))),
% 279.90/41.12 inference(cnf_transformation,[status(thm)],[f1924])).
% 279.90/41.12 fof(f2025,plain,(
% 279.90/41.12 ![X0]: (c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X0)=c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0))),
% 279.90/41.12 inference(cnf_transformation,[status(thm)],[f249])).
% 279.90/41.12 fof(f2203,plain,(
% 279.90/41.12 ![X0,X1,X2,X3]: (hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),c_Complex_Ocomplex_OComplex(X0,X1)),c_Complex_Ocomplex_OComplex(X2,X3))=c_Complex_Ocomplex_OComplex(c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X0),X2),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X1),X3)),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X0),X3),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X1),X2))))),
% 279.90/41.12 inference(cnf_transformation,[status(thm)],[f313])).
% 279.90/41.12 fof(f2282,plain,(
% 279.90/41.12 ![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)))),
% 279.90/41.12 inference(cnf_transformation,[status(thm)],[f338])).
% 279.90/41.12 fof(f2284,plain,(
% 279.90/41.12 ![V_xa_2,V_y_2,V_x_2]: ((~c_Complex_Ocomplex_OComplex(V_x_2,V_y_2)=c_RealVector_Oof__real(tc_Complex_Ocomplex,V_xa_2)|(V_x_2=V_xa_2&V_y_2=c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)))&(c_Complex_Ocomplex_OComplex(V_x_2,V_y_2)=c_RealVector_Oof__real(tc_Complex_Ocomplex,V_xa_2)|(~V_x_2=V_xa_2|~V_y_2=c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))))),
% 279.90/41.12 inference(NNF_transformation,[status(thm)],[f340])).
% 279.90/41.12 fof(f2285,plain,(
% 279.90/41.12 (![V_xa_2,V_y_2,V_x_2]: (~c_Complex_Ocomplex_OComplex(V_x_2,V_y_2)=c_RealVector_Oof__real(tc_Complex_Ocomplex,V_xa_2)|(V_x_2=V_xa_2&V_y_2=c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))))&(![V_xa_2,V_y_2,V_x_2]: (c_Complex_Ocomplex_OComplex(V_x_2,V_y_2)=c_RealVector_Oof__real(tc_Complex_Ocomplex,V_xa_2)|(~V_x_2=V_xa_2|~V_y_2=c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))))),
% 279.90/41.12 inference(miniscoping,[status(thm)],[f2284])).
% 279.90/41.12 fof(f2288,plain,(
% 279.90/41.12 ![X0,X1,X2]: (c_Complex_Ocomplex_OComplex(X0,X1)=c_RealVector_Oof__real(tc_Complex_Ocomplex,X2)|~X0=X2|~X1=c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))),
% 279.90/41.12 inference(cnf_transformation,[status(thm)],[f2285])).
% 279.90/41.12 fof(f2308,plain,(
% 279.90/41.12 ![X0]: (c_Complex_Ocis(X0)=c_Complex_Orcis(c_Groups_Oone__class_Oone(tc_RealDef_Oreal),X0))),
% 279.90/41.12 inference(cnf_transformation,[status(thm)],[f349])).
% 279.90/41.12 fof(f2341,plain,(
% 279.90/41.12 ![X0]: (c_Transcendental_Ocos(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,c_Transcendental_Opi))=c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Transcendental_Ocos(X0)))),
% 279.90/41.12 inference(cnf_transformation,[status(thm)],[f360])).
% 279.90/41.12 fof(f2449,plain,(
% 279.90/41.12 c_Transcendental_Osin(c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))=c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),
% 279.90/41.12 inference(cnf_transformation,[status(thm)],[f409])).
% 279.90/41.12 fof(f2526,plain,(
% 279.90/41.12 c_Transcendental_Osin(c_Transcendental_Opi)=c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),
% 279.90/41.12 inference(cnf_transformation,[status(thm)],[f445])).
% 279.90/41.12 fof(f2585,plain,(
% 279.90/41.12 ![X0]: (c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_Transcendental_Ocos(X0)),c_Transcendental_Ocos(X0)),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_Transcendental_Osin(X0)),c_Transcendental_Osin(X0)))=c_Groups_Oone__class_Oone(tc_RealDef_Oreal))),
% 279.90/41.12 inference(cnf_transformation,[status(thm)],[f475])).
% 279.90/41.12 fof(f2589,plain,(
% 279.90/41.12 ![X0,X1]: (c_Transcendental_Ocos(c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X0,X1))=c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_Transcendental_Ocos(X0)),c_Transcendental_Ocos(X1)),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_Transcendental_Osin(X0)),c_Transcendental_Osin(X1))))),
% 279.90/41.12 inference(cnf_transformation,[status(thm)],[f478])).
% 279.90/41.12 fof(f2599,plain,(
% 279.90/41.12 ![X0,X1]: (hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),c_Complex_Oii),c_Complex_Ocomplex_OComplex(X0,X1))=c_Complex_Ocomplex_OComplex(c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X1),X0))),
% 279.90/41.12 inference(cnf_transformation,[status(thm)],[f484])).
% 279.90/41.12 fof(f4064,plain,(
% 279.90/41.12 c_Complex_ORe(c_Complex_Oii)=c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),
% 279.90/41.12 inference(cnf_transformation,[status(thm)],[f937])).
% 279.90/41.12 fof(f4065,plain,(
% 279.90/41.12 ![X0]: (c_Complex_OIm(c_RealVector_Oof__real(tc_Complex_Ocomplex,X0))=c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))),
% 279.90/41.12 inference(cnf_transformation,[status(thm)],[f938])).
% 279.90/41.12 fof(f4069,plain,(
% 279.90/41.12 ![X0,X1]: (c_Complex_OIm(c_Complex_Ocomplex_OComplex(X0,X1))=X1)),
% 279.90/41.12 inference(cnf_transformation,[status(thm)],[f942])).
% 279.90/41.12 fof(f4070,plain,(
% 279.90/41.12 ![X0]: (c_Complex_ORe(c_RealVector_Oof__real(tc_Complex_Ocomplex,X0))=X0)),
% 279.90/41.12 inference(cnf_transformation,[status(thm)],[f943])).
% 279.90/41.12 fof(f4078,plain,(
% 279.90/41.12 ![X0]: (c_Complex_Ocomplex_OComplex(c_Complex_ORe(X0),c_Complex_OIm(X0))=X0)),
% 279.90/41.12 inference(cnf_transformation,[status(thm)],[f946])).
% 279.90/41.12 fof(f4082,plain,(
% 279.90/41.12 c_Complex_OIm(c_Complex_Oii)=c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),
% 279.90/41.12 inference(cnf_transformation,[status(thm)],[f950])).
% 279.90/41.12 fof(f4087,plain,(
% 279.90/41.12 ![X0]: (c_Complex_OIm(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,X0))=c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Complex_OIm(X0)))),
% 279.90/41.12 inference(cnf_transformation,[status(thm)],[f955])).
% 279.90/41.12 fof(f4088,plain,(
% 279.90/41.12 ![X0]: (c_Complex_ORe(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,X0))=c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Complex_ORe(X0)))),
% 279.90/41.12 inference(cnf_transformation,[status(thm)],[f956])).
% 279.90/41.12 fof(f4097,plain,(
% 279.90/41.12 ![X0,X1]: (c_Complex_OIm(c_Complex_Orcis(X0,X1))=hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X0),c_Transcendental_Osin(X1)))),
% 279.90/41.12 inference(cnf_transformation,[status(thm)],[f965])).
% 279.90/41.12 fof(f4098,plain,(
% 279.90/41.12 ![X0,X1]: (c_Complex_ORe(c_Complex_Orcis(X0,X1))=hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X0),c_Transcendental_Ocos(X1)))),
% 279.90/41.12 inference(cnf_transformation,[status(thm)],[f966])).
% 279.90/41.12 fof(f4306,plain,(
% 279.90/41.12 class_Groups_Oordered__ab__group__add__abs(tc_RealDef_Oreal)),
% 279.90/41.12 inference(cnf_transformation,[status(thm)],[f1111])).
% 279.90/41.12 fof(f4333,plain,(
% 279.90/41.12 class_Rings_Ocomm__semiring__1(tc_RealDef_Oreal)),
% 279.90/41.12 inference(cnf_transformation,[status(thm)],[f1138])).
% 279.90/41.12 fof(f4363,plain,(
% 279.90/41.12 class_RealVector_Oreal__normed__algebra(tc_Complex_Ocomplex)),
% 279.90/41.12 inference(cnf_transformation,[status(thm)],[f1168])).
% 279.90/41.12 fof(f4396,plain,(
% 279.90/41.12 ~c_Complex_Orcis(hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_NthRoot_Osqrt(c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,v_r))),c_NthRoot_Osqrt(c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,v_r))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Transcendental_Opi,v_a))=c_Complex_Orcis(c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,v_r)),v_a)),
% 279.90/41.12 inference(cnf_transformation,[status(thm)],[f1202])).
% 279.90/41.12 fof(f4451,plain,(
% 279.90/41.12 ![X0]: (c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0))=c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))),
% 279.90/41.12 inference(destructive_equality_resolution,[status(thm)],[f1926])).
% 279.90/41.12 fof(f4468,plain,(
% 279.90/41.12 ![X0]: (c_NthRoot_Osqrt(hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X0),X0))=c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X0))),
% 279.90/41.12 inference(backward_demodulation,[status(thm)],[f2025,f1207])).
% 279.90/41.12 fof(f4485,plain,(
% 279.90/41.12 ![X0]: (c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X0,X0)=c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))),
% 279.90/41.12 inference(backward_demodulation,[status(thm)],[f2282,f4451])).
% 279.90/41.12 fof(f4487,plain,(
% 279.90/41.12 ![X0]: (c_Complex_Ocomplex_OComplex(X0,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))=c_RealVector_Oof__real(tc_Complex_Ocomplex,X0))),
% 279.90/41.12 inference(destructive_equality_resolution,[status(thm)],[f2288])).
% 279.90/41.12 fof(f4503,plain,(
% 279.90/41.12 c_Transcendental_Osin(c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))=c_Transcendental_Osin(c_Transcendental_Opi)),
% 279.90/41.12 inference(backward_demodulation,[status(thm)],[f2526,f2449])).
% 279.90/41.12 fof(f4515,plain,(
% 279.90/41.12 ![X0]: (c_Complex_Ocomplex_OComplex(X0,c_Transcendental_Osin(c_Transcendental_Opi))=c_RealVector_Oof__real(tc_Complex_Ocomplex,X0))),
% 279.90/41.12 inference(backward_demodulation,[status(thm)],[f2526,f4487])).
% 279.90/41.12 fof(f4533,plain,(
% 279.90/41.12 ![X0,X1]: (~c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X1)=c_Transcendental_Osin(c_Transcendental_Opi)|X1=c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0))),
% 279.90/41.12 inference(backward_demodulation,[status(thm)],[f2526,f1925])).
% 279.90/41.12 fof(f4546,plain,(
% 279.90/41.12 ![X0]: (c_Complex_Orcis(X0,c_Transcendental_Osin(c_Transcendental_Opi))=c_RealVector_Oof__real(tc_Complex_Ocomplex,X0))),
% 279.90/41.12 inference(backward_demodulation,[status(thm)],[f2526,f1604])).
% 279.90/41.12 fof(f4574,plain,(
% 279.90/41.12 ![X0]: (c_Transcendental_Ocos(c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X0,X0))=c_Groups_Oone__class_Oone(tc_RealDef_Oreal))),
% 279.90/41.12 inference(backward_demodulation,[status(thm)],[f2589,f2585])).
% 279.90/41.12 fof(f4812,plain,(
% 279.90/41.12 c_Transcendental_Osin(c_Transcendental_Opi)=c_Complex_ORe(c_Complex_Oii)),
% 279.90/41.12 inference(backward_demodulation,[status(thm)],[f4064,f2526])).
% 279.90/41.12 fof(f4813,plain,(
% 279.90/41.12 ![X0]: (c_Complex_OIm(c_RealVector_Oof__real(tc_Complex_Ocomplex,X0))=c_Complex_ORe(c_Complex_Oii))),
% 279.90/41.12 inference(forward_demodulation,[status(thm)],[f4064,f4065])).
% 279.90/41.12 fof(f4863,plain,(
% 279.90/41.12 ![X0]: (c_Complex_Ocis(X0)=c_Complex_Orcis(c_Complex_OIm(c_Complex_Oii),X0))),
% 279.90/41.12 inference(backward_demodulation,[status(thm)],[f4082,f2308])).
% 279.90/41.12 fof(f4932,plain,(
% 279.90/41.12 ~hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),c_Complex_Orcis(c_NthRoot_Osqrt(c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,v_r)),c_Transcendental_Opi)),c_Complex_Orcis(c_NthRoot_Osqrt(c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,v_r)),v_a))=c_Complex_Orcis(c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,v_r)),v_a)),
% 279.90/41.12 inference(forward_demodulation,[status(thm)],[f1311,f4396])).
% 279.90/41.12 fof(f4933,plain,(
% 279.90/41.12 ~hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),c_Complex_Orcis(c_NthRoot_Osqrt(c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,v_r)),c_Transcendental_Opi)),c_Complex_Orcis(c_NthRoot_Osqrt(c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,v_r)),v_a))=c_Complex_Orcis(c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,v_r)),v_a)),
% 279.90/41.12 inference(forward_demodulation,[status(thm)],[f2025,f4932])).
% 279.90/41.12 fof(f4934,plain,(
% 279.90/41.12 ~hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),c_Complex_Orcis(c_NthRoot_Osqrt(c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,v_r)),c_Transcendental_Opi)),c_Complex_Orcis(c_NthRoot_Osqrt(c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,v_r)),v_a))=c_Complex_Orcis(c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,v_r)),v_a)),
% 279.90/41.12 inference(forward_demodulation,[status(thm)],[f2025,f4933])).
% 279.90/41.12 fof(f4935,plain,(
% 279.90/41.12 ~hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),c_Complex_Orcis(c_NthRoot_Osqrt(c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,v_r)),c_Transcendental_Opi)),c_Complex_Orcis(c_NthRoot_Osqrt(c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,v_r)),v_a))=c_Complex_Orcis(c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,v_r)),v_a)),
% 279.90/41.12 inference(forward_demodulation,[status(thm)],[f2025,f4934])).
% 279.90/41.12 fof(f4951,plain,(
% 279.90/41.12 ![X0]: (c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X0,X0)=c_Complex_ORe(c_Complex_Oii))),
% 279.90/41.12 inference(forward_demodulation,[status(thm)],[f4064,f4485])).
% 279.90/41.12 fof(f4953,plain,(
% 279.90/41.12 c_Transcendental_Osin(c_Complex_ORe(c_Complex_Oii))=c_Transcendental_Osin(c_Transcendental_Opi)),
% 279.90/41.12 inference(forward_demodulation,[status(thm)],[f4064,f4503])).
% 279.90/41.12 fof(f4974,plain,(
% 279.90/41.12 c_Transcendental_Ocos(c_Complex_ORe(c_Complex_Oii))=c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),
% 279.90/41.12 inference(forward_demodulation,[status(thm)],[f4951,f4574])).
% 279.90/41.12 fof(f4975,plain,(
% 279.90/41.12 c_Transcendental_Ocos(c_Complex_ORe(c_Complex_Oii))=c_Complex_OIm(c_Complex_Oii)),
% 279.90/41.12 inference(forward_demodulation,[status(thm)],[f4082,f4974])).
% 279.90/41.12 fof(f4989,plain,(
% 279.90/41.12 ![X0]: (c_Complex_Orcis(X0,c_Complex_ORe(c_Complex_Oii))=c_RealVector_Oof__real(tc_Complex_Ocomplex,X0))),
% 279.90/41.12 inference(backward_demodulation,[status(thm)],[f4812,f4546])).
% 279.90/41.12 fof(f5002,plain,(
% 279.90/41.12 ![X0,X1]: (~c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X1)=c_Complex_ORe(c_Complex_Oii)|X1=c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0))),
% 279.90/41.12 inference(backward_demodulation,[status(thm)],[f4812,f4533])).
% 279.90/41.12 fof(f5020,plain,(
% 279.90/41.12 ![X0]: (c_Complex_Ocomplex_OComplex(X0,c_Complex_ORe(c_Complex_Oii))=c_RealVector_Oof__real(tc_Complex_Ocomplex,X0))),
% 279.90/41.12 inference(backward_demodulation,[status(thm)],[f4812,f4515])).
% 279.90/41.12 fof(f5031,plain,(
% 279.90/41.12 c_Transcendental_Osin(c_Complex_ORe(c_Complex_Oii))=c_Complex_ORe(c_Complex_Oii)),
% 279.90/41.12 inference(backward_demodulation,[status(thm)],[f4812,f4953])).
% 279.90/41.12 fof(f5248,plain,(
% 279.90/41.12 ![X0,X1,X2,X3]: (hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),c_Complex_Orcis(c_NthRoot_Osqrt(X0),X1)),c_Complex_Orcis(c_NthRoot_Osqrt(X2),X3))=c_Complex_Orcis(c_NthRoot_Osqrt(hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X0),X2)),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,X3)))),
% 279.90/41.12 inference(paramodulation,[status(thm)],[f1209,f1311])).
% 279.90/41.12 fof(f5253,plain,(
% 279.90/41.12 ~c_Complex_Orcis(c_NthRoot_Osqrt(hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,v_r)),c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,v_r))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Transcendental_Opi,v_a))=c_Complex_Orcis(c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,v_r)),v_a)),
% 279.90/41.12 inference(backward_demodulation,[status(thm)],[f5248,f4935])).
% 279.90/41.12 fof(f5254,plain,(
% 279.90/41.12 ~c_Complex_Orcis(c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,v_r)),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Transcendental_Opi,v_a))=c_Complex_Orcis(c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,v_r)),v_a)),
% 279.90/41.12 inference(forward_demodulation,[status(thm)],[f4468,f5253])).
% 279.90/41.12 fof(f5840,plain,(
% 279.90/41.12 ![X0]: (c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0))=c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0))),
% 279.90/41.12 inference(resolution,[status(thm)],[f4306,f1279])).
% 279.90/41.12 fof(f5843,plain,(
% 279.90/41.12 ![X0]: (c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0))=c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0))),
% 279.90/41.12 inference(forward_demodulation,[status(thm)],[f2025,f5840])).
% 279.90/41.12 fof(f5844,plain,(
% 279.90/41.12 ![X0]: (c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X0))=c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0))),
% 279.90/41.12 inference(forward_demodulation,[status(thm)],[f2025,f5843])).
% 279.90/41.12 fof(f5845,plain,(
% 279.90/41.12 ~c_Complex_Orcis(c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,v_r),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Transcendental_Opi,v_a))=c_Complex_Orcis(c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,v_r)),v_a)),
% 279.90/41.12 inference(backward_demodulation,[status(thm)],[f5846,f5254])).
% 279.90/41.12 fof(f5846,plain,(
% 279.90/41.12 ![X0]: (c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X0))=c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X0))),
% 279.90/41.12 inference(forward_demodulation,[status(thm)],[f2025,f5844])).
% 279.90/41.12 fof(f6310,plain,(
% 279.90/41.12 ![X0]: (c_Complex_OIm(c_Complex_Orcis(X0,c_Complex_ORe(c_Complex_Oii)))=hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X0),c_Complex_ORe(c_Complex_Oii)))),
% 279.90/41.12 inference(paramodulation,[status(thm)],[f5031,f4097])).
% 279.90/41.12 fof(f6311,plain,(
% 279.90/41.12 ![X0]: (c_Complex_OIm(c_Complex_Orcis(X0,c_Transcendental_Opi))=hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X0),c_Complex_ORe(c_Complex_Oii)))),
% 279.90/41.12 inference(paramodulation,[status(thm)],[f4812,f4097])).
% 279.90/41.12 fof(f6327,plain,(
% 279.90/41.12 ![X0]: (c_Complex_OIm(c_RealVector_Oof__real(tc_Complex_Ocomplex,X0))=hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X0),c_Complex_ORe(c_Complex_Oii)))),
% 279.90/41.12 inference(forward_demodulation,[status(thm)],[f4989,f6310])).
% 279.90/41.12 fof(f6330,plain,(
% 279.90/41.12 ![X0]: (c_Complex_ORe(c_Complex_Oii)=hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X0),c_Complex_ORe(c_Complex_Oii)))),
% 279.90/41.12 inference(forward_demodulation,[status(thm)],[f4813,f6327])).
% 279.90/41.12 fof(f6331,plain,(
% 279.90/41.12 ![X0]: (c_Complex_OIm(c_Complex_Orcis(X0,c_Transcendental_Opi))=c_Complex_ORe(c_Complex_Oii))),
% 279.90/41.12 inference(forward_demodulation,[status(thm)],[f6330,f6311])).
% 279.90/41.12 fof(f6629,plain,(
% 279.90/41.12 ![X0,X1]: (c_Complex_ORe(c_Complex_Orcis(X0,X1))=hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_Transcendental_Ocos(X1)),X0))),
% 279.90/41.12 inference(paramodulation,[status(thm)],[f1276,f4098])).
% 279.90/41.12 fof(f6632,plain,(
% 279.90/41.12 ![X0]: (c_Complex_ORe(c_Complex_Orcis(X0,c_Complex_ORe(c_Complex_Oii)))=hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X0),c_Complex_OIm(c_Complex_Oii)))),
% 279.90/41.12 inference(paramodulation,[status(thm)],[f4975,f4098])).
% 279.90/41.12 fof(f6651,plain,(
% 279.90/41.12 ![X0]: (c_Complex_ORe(c_RealVector_Oof__real(tc_Complex_Ocomplex,X0))=hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X0),c_Complex_OIm(c_Complex_Oii)))),
% 279.90/41.12 inference(forward_demodulation,[status(thm)],[f4989,f6632])).
% 279.90/41.12 fof(f6653,plain,(
% 279.90/41.12 ![X0]: (X0=hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X0),c_Complex_OIm(c_Complex_Oii)))),
% 279.90/41.12 inference(forward_demodulation,[status(thm)],[f4070,f6651])).
% 279.90/41.12 fof(f6788,plain,(
% 279.90/41.12 ![X0,X1,X2]: (hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),c_Complex_Orcis(X0,X1)),c_Complex_Orcis(c_Complex_OIm(c_Complex_Oii),X2))=c_Complex_Orcis(X0,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,X2)))),
% 279.90/41.12 inference(paramodulation,[status(thm)],[f6653,f1311])).
% 279.90/41.12 fof(f6796,plain,(
% 279.90/41.12 ![X0,X1,X2]: (hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),c_Complex_Orcis(X0,X1)),c_Complex_Ocis(X2))=c_Complex_Orcis(X0,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,X2)))),
% 279.90/41.12 inference(forward_demodulation,[status(thm)],[f4863,f6788])).
% 279.90/41.12 fof(f6867,plain,(
% 279.90/41.12 ![X0,X1]: (hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,X0)),X1)=c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),X0),X1)))),
% 279.90/41.12 inference(resolution,[status(thm)],[f4363,f1314])).
% 279.90/41.12 fof(f7664,plain,(
% 279.90/41.12 ![X0]: (c_Complex_Ocomplex_OComplex(c_Complex_ORe(c_Complex_Orcis(X0,c_Transcendental_Opi)),c_Complex_ORe(c_Complex_Oii))=c_Complex_Orcis(X0,c_Transcendental_Opi))),
% 279.90/41.12 inference(paramodulation,[status(thm)],[f6331,f4078])).
% 279.90/41.12 fof(f7677,plain,(
% 279.90/41.12 ![X0]: (c_RealVector_Oof__real(tc_Complex_Ocomplex,c_Complex_ORe(c_Complex_Orcis(X0,c_Transcendental_Opi)))=c_Complex_Orcis(X0,c_Transcendental_Opi))),
% 279.90/41.12 inference(forward_demodulation,[status(thm)],[f5020,f7664])).
% 279.90/41.12 fof(f7822,plain,(
% 279.90/41.12 ![X0,X1]: (c_Complex_Orcis(c_Complex_ORe(c_Complex_Orcis(X0,c_Transcendental_Opi)),X1)=hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),c_Complex_Orcis(X0,c_Transcendental_Opi)),c_Complex_Ocis(X1)))),
% 279.90/41.12 inference(paramodulation,[status(thm)],[f7677,f1550])).
% 279.90/41.12 fof(f7830,plain,(
% 279.90/41.12 ![X0,X1]: (c_Complex_Orcis(c_Complex_ORe(c_Complex_Orcis(X0,c_Transcendental_Opi)),X1)=c_Complex_Orcis(X0,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Transcendental_Opi,X1)))),
% 279.90/41.12 inference(forward_demodulation,[status(thm)],[f6796,f7822])).
% 279.90/41.12 fof(f8372,plain,(
% 279.90/41.12 ![X0]: (c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),X0)=X0)),
% 279.90/41.12 inference(resolution,[status(thm)],[f1650,f4333])).
% 279.90/41.12 fof(f8381,plain,(
% 279.90/41.12 ![X0]: (c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Oii),X0)=X0)),
% 279.90/41.12 inference(forward_demodulation,[status(thm)],[f4064,f8372])).
% 279.90/41.12 fof(f8384,plain,(
% 279.90/41.12 c_Complex_ORe(c_Complex_Oii)=c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Oii))),
% 279.90/41.12 inference(resolution,[status(thm)],[f8381,f5002])).
% 279.90/41.12 fof(f8387,plain,(
% 279.90/41.12 c_Transcendental_Ocos(c_Transcendental_Opi)=c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Transcendental_Ocos(c_Complex_ORe(c_Complex_Oii)))),
% 279.90/41.12 inference(paramodulation,[status(thm)],[f8381,f2341])).
% 279.90/41.12 fof(f8418,plain,(
% 279.90/41.12 c_Complex_ORe(c_Complex_Oii)=c_Complex_ORe(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Complex_Oii))),
% 279.90/41.12 inference(forward_demodulation,[status(thm)],[f4088,f8384])).
% 279.90/41.12 fof(f8422,plain,(
% 279.90/41.12 c_Transcendental_Ocos(c_Transcendental_Opi)=c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Complex_OIm(c_Complex_Oii))),
% 279.90/41.12 inference(forward_demodulation,[status(thm)],[f4975,f8387])).
% 279.90/41.12 fof(f8447,plain,(
% 279.90/41.12 c_Transcendental_Ocos(c_Transcendental_Opi)=c_Complex_OIm(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Complex_Oii))),
% 279.90/41.12 inference(forward_demodulation,[status(thm)],[f4087,f8422])).
% 279.90/41.12 fof(f8544,plain,(
% 279.90/41.12 c_Complex_Ocomplex_OComplex(c_Complex_ORe(c_Complex_Oii),c_Complex_OIm(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Complex_Oii)))=c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Complex_Oii)),
% 279.90/41.12 inference(paramodulation,[status(thm)],[f8418,f4078])).
% 279.90/41.12 fof(f8545,plain,(
% 279.90/41.12 c_Complex_Ocomplex_OComplex(c_Complex_ORe(c_Complex_Oii),c_Transcendental_Ocos(c_Transcendental_Opi))=c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Complex_Oii)),
% 279.90/41.12 inference(forward_demodulation,[status(thm)],[f8447,f8544])).
% 279.90/41.12 fof(f15222,plain,(
% 279.90/41.12 ![X0,X1]: (c_Complex_OIm(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Complex_Ocomplex_OComplex(X0,X1)))=c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X1))),
% 53.58/41.31 inference(paramodulation,[status(thm)],[f4069,f4087])).
% 53.58/41.31 fof(f26714,plain,(
% 53.58/41.31 ![X0,X1,X2,X3]: (c_Complex_OIm(hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),c_Complex_Ocomplex_OComplex(X0,X1)),c_Complex_Ocomplex_OComplex(X2,X3)))=c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X0),X3),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X1),X2)))),
% 53.58/41.31 inference(paramodulation,[status(thm)],[f2203,f4069])).
% 53.58/41.31 fof(f26779,plain,(
% 53.58/41.31 ![X0,X1,X2]: (hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X1)),X2)=c_Complex_OIm(hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),c_Complex_Ocomplex_OComplex(X0,X1)),c_Complex_Ocomplex_OComplex(X2,X2))))),
% 53.58/41.31 inference(backward_demodulation,[status(thm)],[f26714,f1210])).
% 53.58/41.31 fof(f41051,plain,(
% 53.58/41.31 ![X0]: (hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Oii),c_Transcendental_Ocos(c_Transcendental_Opi))),X0)=c_Complex_OIm(hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Complex_Oii)),c_Complex_Ocomplex_OComplex(X0,X0))))),
% 53.58/41.31 inference(paramodulation,[status(thm)],[f8545,f26779])).
% 53.58/41.31 fof(f41092,plain,(
% 53.58/41.31 ![X0]: (hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_Transcendental_Ocos(c_Transcendental_Opi)),X0)=c_Complex_OIm(hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Complex_Oii)),c_Complex_Ocomplex_OComplex(X0,X0))))),
% 53.58/41.31 inference(forward_demodulation,[status(thm)],[f8381,f41051])).
% 53.58/41.31 fof(f41093,plain,(
% 53.58/41.31 ![X0]: (c_Complex_ORe(c_Complex_Orcis(X0,c_Transcendental_Opi))=c_Complex_OIm(hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Complex_Oii)),c_Complex_Ocomplex_OComplex(X0,X0))))),
% 53.58/41.31 inference(forward_demodulation,[status(thm)],[f6629,f41092])).
% 53.58/41.31 fof(f41094,plain,(
% 53.58/41.31 ![X0]: (c_Complex_ORe(c_Complex_Orcis(X0,c_Transcendental_Opi))=c_Complex_OIm(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),c_Complex_Oii),c_Complex_Ocomplex_OComplex(X0,X0)))))),
% 53.58/41.31 inference(forward_demodulation,[status(thm)],[f6867,f41093])).
% 53.58/41.31 fof(f41095,plain,(
% 53.58/41.31 ![X0]: (c_Complex_ORe(c_Complex_Orcis(X0,c_Transcendental_Opi))=c_Complex_OIm(c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Complex_Ocomplex_OComplex(c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0),X0))))),
% 53.58/41.31 inference(forward_demodulation,[status(thm)],[f2599,f41094])).
% 53.58/41.31 fof(f41125,plain,(
% 53.58/41.31 ![X0,X1]: (c_Complex_Orcis(c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0),X1)=c_Complex_Orcis(X0,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Transcendental_Opi,X1)))),
% 53.58/41.31 inference(backward_demodulation,[status(thm)],[f41128,f7830])).
% 53.58/41.31 fof(f41128,plain,(
% 53.58/41.31 ![X0]: (c_Complex_ORe(c_Complex_Orcis(X0,c_Transcendental_Opi))=c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0))),
% 53.58/41.31 inference(forward_demodulation,[status(thm)],[f15222,f41095])).
% 53.58/41.31 fof(f41191,plain,(
% 53.58/41.31 ~c_Complex_Orcis(c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,v_r)),v_a)=c_Complex_Orcis(c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,v_r)),v_a)),
% 53.58/41.31 inference(backward_demodulation,[status(thm)],[f41125,f5845])).
% 53.58/41.31 fof(f42619,plain,(
% 53.58/41.31 $false),
% 53.58/41.31 inference(trivial_equality_resolution,[status(thm)],[f41191])).
% 53.58/41.31 % SZS output end CNFRefutation for theBenchmark.p
% 221.18/41.42 % Elapsed time: 35.966909 seconds
% 221.18/41.42 % CPU time: 282.956042 seconds
% 221.18/41.42 % Total memory used: 1.748 GB
% 221.18/41.42 % Net memory used: 1.685 GB
%------------------------------------------------------------------------------