%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV601-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n003.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 02:52:53 PM UTC 2026
% Result : Unsatisfiable 0.24s 0.53s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV601-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n003.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Mon Sep 21 09:14:46 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.15/0.44 % Drodi V4.1.1
% 0.24/0.53 % Refutation found
% 0.24/0.53 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.24/0.53 % SZS output start CNFRefutation for theBenchmark
% 0.24/0.53 fof(f327,axiom,(
% 0.24/0.53 c_Transcendental_Otan(c_Transcendental_Opi) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
% 0.24/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.24/0.53 fof(f518,axiom,(
% 0.24/0.53 (![V_x,V_y]: (c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(V_x,V_y,tc_RealDef_Oreal)) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(V_x),c_Transcendental_Ocos(V_y),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(V_x),c_Transcendental_Osin(V_y),tc_RealDef_Oreal),tc_RealDef_Oreal) ))),
% 0.24/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.24/0.53 fof(f566,axiom,(
% 0.24/0.53 (![V_x]: (c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(V_x),c_Transcendental_Ocos(V_x),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(V_x),c_Transcendental_Osin(V_x),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Oone__class_Oone(tc_RealDef_Oreal) ))),
% 0.24/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.24/0.53 fof(f602,axiom,(
% 0.24/0.53 (![T_a,V_a]: (( ~ class_OrderedGroup_Omonoid__add(T_a)| c_HOL_Oplus__class_Oplus(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) = V_a ) ))),
% 0.24/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.24/0.53 fof(f603,axiom,(
% 0.24/0.53 (![T_a,V_a]: (( ~ class_OrderedGroup_Omonoid__add(T_a)| c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(T_a),V_a,T_a) = V_a ) ))),
% 0.24/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.24/0.53 fof(f676,axiom,(
% 0.24/0.53 (![V_x]: (c_Transcendental_Ocos(c_HOL_Ouminus__class_Ouminus(V_x,tc_RealDef_Oreal)) = c_Transcendental_Ocos(V_x) ))),
% 0.24/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.24/0.53 fof(f679,axiom,(
% 0.24/0.53 (![V_x]: (c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(V_x,tc_RealDef_Oreal)) = c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(V_x),tc_RealDef_Oreal) ))),
% 0.24/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.24/0.53 fof(f729,axiom,(
% 0.24/0.53 (![V_a,V_b]: (( c_Complex_Ocomplex_OComplex(V_a,V_b) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)| V_b = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ) ))),
% 0.24/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.24/0.53 fof(f730,axiom,(
% 0.24/0.53 (![V_a,V_b]: (( c_Complex_Ocomplex_OComplex(V_a,V_b) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)| V_a = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ) ))),
% 0.24/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.24/0.53 fof(f731,axiom,(
% 0.24/0.53 c_Transcendental_Osin(c_Transcendental_Opi) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
% 0.24/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.24/0.53 fof(f739,axiom,(
% 0.24/0.53 c_Transcendental_Osin(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
% 0.24/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.24/0.53 fof(f740,axiom,(
% 0.24/0.53 (![V_x]: (( c_Transcendental_Ocos(V_x) != c_HOL_Oone__class_Oone(tc_RealDef_Oreal)| c_Transcendental_Osin(V_x) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ) ))),
% 0.24/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.24/0.53 fof(f745,axiom,(
% 0.24/0.53 (![V_z]: (c_HOL_Otimes__class_Otimes(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),V_z,tc_RealDef_Oreal) = V_z ))),
% 0.24/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.24/0.53 fof(f776,axiom,(
% 0.24/0.53 c_Transcendental_Ocos(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)) = c_HOL_Oone__class_Oone(tc_RealDef_Oreal) ),
% 0.24/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.24/0.53 fof(f777,axiom,(
% 0.24/0.53 c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) != c_HOL_Oone__class_Oone(tc_RealDef_Oreal) ),
% 0.24/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.24/0.53 fof(f868,axiom,(
% 0.24/0.53 (![V_z,V_w]: (c_HOL_Otimes__class_Otimes(V_z,V_w,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(V_w,V_z,tc_RealDef_Oreal) ))),
% 0.24/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.24/0.53 fof(f880,negated_conjecture,(
% 0.24/0.53 c_Complex_Ocomplex_OComplex(c_Transcendental_Ocos(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal)),c_Transcendental_Osin(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal))) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
% 0.24/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.24/0.53 fof(f991,axiom,(
% 0.24/0.53 class_OrderedGroup_Omonoid__add(tc_RealDef_Oreal) ),
% 0.24/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.24/0.53 fof(f1543,plain,(
% 0.24/0.53 c_Transcendental_Otan(c_Transcendental_Opi)=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)),
% 0.24/0.53 inference(cnf_transformation,[status(thm)],[f327])).
% 0.24/0.53 fof(f1811,plain,(
% 0.24/0.53 ![X0,X1]: (c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(X0,X1,tc_RealDef_Oreal))=c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(X0),c_Transcendental_Ocos(X1),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(X0),c_Transcendental_Osin(X1),tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 0.24/0.53 inference(cnf_transformation,[status(thm)],[f518])).
% 0.24/0.53 fof(f1869,plain,(
% 0.24/0.53 ![X0]: (c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(X0),c_Transcendental_Ocos(X0),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(X0),c_Transcendental_Osin(X0),tc_RealDef_Oreal),tc_RealDef_Oreal)=c_HOL_Oone__class_Oone(tc_RealDef_Oreal))),
% 0.24/0.53 inference(cnf_transformation,[status(thm)],[f566])).
% 0.24/0.53 fof(f1913,plain,(
% 0.24/0.53 ![T_a]: (~class_OrderedGroup_Omonoid__add(T_a)|(![V_a]: c_HOL_Oplus__class_Oplus(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a)=V_a))),
% 0.24/0.53 inference(miniscoping,[status(thm)],[f602])).
% 0.24/0.53 fof(f1914,plain,(
% 0.24/0.53 ![X0,X1]: (~class_OrderedGroup_Omonoid__add(X0)|c_HOL_Oplus__class_Oplus(X1,c_HOL_Ozero__class_Ozero(X0),X0)=X1)),
% 0.24/0.53 inference(cnf_transformation,[status(thm)],[f1913])).
% 0.24/0.53 fof(f1915,plain,(
% 0.24/0.53 ![T_a]: (~class_OrderedGroup_Omonoid__add(T_a)|(![V_a]: c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(T_a),V_a,T_a)=V_a))),
% 0.24/0.53 inference(miniscoping,[status(thm)],[f603])).
% 0.24/0.53 fof(f1916,plain,(
% 0.24/0.53 ![X0,X1]: (~class_OrderedGroup_Omonoid__add(X0)|c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(X0),X1,X0)=X1)),
% 0.24/0.53 inference(cnf_transformation,[status(thm)],[f1915])).
% 0.24/0.53 fof(f2051,plain,(
% 0.24/0.53 ![X0]: (c_Transcendental_Ocos(c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal))=c_Transcendental_Ocos(X0))),
% 0.24/0.53 inference(cnf_transformation,[status(thm)],[f676])).
% 0.24/0.53 fof(f2054,plain,(
% 0.24/0.53 ![X0]: (c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal))=c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(X0),tc_RealDef_Oreal))),
% 0.24/0.53 inference(cnf_transformation,[status(thm)],[f679])).
% 0.24/0.53 fof(f2105,plain,(
% 0.24/0.53 ![V_b]: ((![V_a]: ~c_Complex_Ocomplex_OComplex(V_a,V_b)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))|V_b=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal))),
% 0.24/0.53 inference(miniscoping,[status(thm)],[f729])).
% 0.24/0.53 fof(f2106,plain,(
% 0.24/0.53 ![X0,X1]: (~c_Complex_Ocomplex_OComplex(X0,X1)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)|X1=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal))),
% 0.24/0.53 inference(cnf_transformation,[status(thm)],[f2105])).
% 0.24/0.53 fof(f2107,plain,(
% 0.24/0.53 ![V_a]: ((![V_b]: ~c_Complex_Ocomplex_OComplex(V_a,V_b)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))|V_a=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal))),
% 0.24/0.53 inference(miniscoping,[status(thm)],[f730])).
% 0.24/0.53 fof(f2108,plain,(
% 0.24/0.53 ![X0,X1]: (~c_Complex_Ocomplex_OComplex(X0,X1)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)|X0=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal))),
% 0.24/0.53 inference(cnf_transformation,[status(thm)],[f2107])).
% 0.24/0.53 fof(f2109,plain,(
% 0.24/0.53 c_Transcendental_Osin(c_Transcendental_Opi)=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)),
% 0.24/0.53 inference(cnf_transformation,[status(thm)],[f731])).
% 0.24/0.53 fof(f2120,plain,(
% 0.24/0.53 c_Transcendental_Osin(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal))=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)),
% 0.24/0.53 inference(cnf_transformation,[status(thm)],[f739])).
% 0.24/0.53 fof(f2121,plain,(
% 0.24/0.53 ![X0]: (~c_Transcendental_Ocos(X0)=c_HOL_Oone__class_Oone(tc_RealDef_Oreal)|c_Transcendental_Osin(X0)=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal))),
% 0.24/0.53 inference(cnf_transformation,[status(thm)],[f740])).
% 0.24/0.53 fof(f2126,plain,(
% 0.24/0.53 ![X0]: (c_HOL_Otimes__class_Otimes(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)=X0)),
% 0.24/0.53 inference(cnf_transformation,[status(thm)],[f745])).
% 0.24/0.53 fof(f2182,plain,(
% 0.24/0.53 c_Transcendental_Ocos(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal))=c_HOL_Oone__class_Oone(tc_RealDef_Oreal)),
% 0.24/0.53 inference(cnf_transformation,[status(thm)],[f776])).
% 0.24/0.53 fof(f2183,plain,(
% 0.24/0.53 ~c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)=c_HOL_Oone__class_Oone(tc_RealDef_Oreal)),
% 0.24/0.53 inference(cnf_transformation,[status(thm)],[f777])).
% 0.24/0.53 fof(f2335,plain,(
% 0.24/0.53 ![X0,X1]: (c_HOL_Otimes__class_Otimes(X0,X1,tc_RealDef_Oreal)=c_HOL_Otimes__class_Otimes(X1,X0,tc_RealDef_Oreal))),
% 0.24/0.53 inference(cnf_transformation,[status(thm)],[f868])).
% 0.24/0.53 fof(f2356,plain,(
% 0.24/0.53 c_Complex_Ocomplex_OComplex(c_Transcendental_Ocos(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal)),c_Transcendental_Osin(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal)))=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)),
% 0.24/0.53 inference(cnf_transformation,[status(thm)],[f880])).
% 0.24/0.53 fof(f2467,plain,(
% 0.24/0.53 class_OrderedGroup_Omonoid__add(tc_RealDef_Oreal)),
% 0.24/0.53 inference(cnf_transformation,[status(thm)],[f991])).
% 0.24/0.53 fof(f2531,plain,(
% 0.24/0.53 c_Transcendental_Osin(c_Transcendental_Osin(c_Transcendental_Opi))=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)),
% 0.24/0.53 inference(forward_demodulation,[status(thm)],[f2109,f2120])).
% 0.24/0.53 fof(f2532,plain,(
% 0.24/0.53 c_Transcendental_Osin(c_Transcendental_Osin(c_Transcendental_Opi))=c_Transcendental_Osin(c_Transcendental_Opi)),
% 0.24/0.53 inference(forward_demodulation,[status(thm)],[f2109,f2531])).
% 0.24/0.53 fof(f2533,plain,(
% 0.24/0.53 c_Transcendental_Ocos(c_Transcendental_Osin(c_Transcendental_Opi))=c_HOL_Oone__class_Oone(tc_RealDef_Oreal)),
% 0.24/0.53 inference(forward_demodulation,[status(thm)],[f2109,f2182])).
% 0.24/0.53 fof(f2576,plain,(
% 0.24/0.53 c_Complex_Ocomplex_OComplex(c_Transcendental_Ocos(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal)),c_Transcendental_Osin(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal)))=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)),
% 0.24/0.53 inference(paramodulation,[status(thm)],[f2335,f2356])).
% 0.24/0.53 fof(f2577,plain,(
% 0.24/0.53 c_Complex_Ocomplex_OComplex(c_Transcendental_Ocos(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal)),c_Transcendental_Osin(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal)))=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)),
% 0.24/0.53 inference(paramodulation,[status(thm)],[f2335,f2356])).
% 0.24/0.53 fof(f2648,plain,(
% 0.24/0.53 ![X0,X1]: (~c_Complex_Ocomplex_OComplex(X0,X1)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)|X1=c_Transcendental_Osin(c_Transcendental_Opi))),
% 0.24/0.53 inference(forward_demodulation,[status(thm)],[f2109,f2106])).
% 0.24/0.53 fof(f2649,plain,(
% 0.24/0.53 c_Transcendental_Osin(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal))=c_Transcendental_Osin(c_Transcendental_Opi)),
% 0.24/0.53 inference(resolution,[status(thm)],[f2648,f2577])).
% 0.24/0.53 fof(f2664,plain,(
% 0.24/0.53 ![X0,X1]: (~c_Complex_Ocomplex_OComplex(X0,X1)=c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)|X0=c_Transcendental_Osin(c_Transcendental_Opi))),
% 0.24/0.53 inference(forward_demodulation,[status(thm)],[f2109,f2108])).
% 0.24/0.53 fof(f2665,plain,(
% 0.24/0.53 c_Transcendental_Ocos(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal))=c_Transcendental_Osin(c_Transcendental_Opi)),
% 0.24/0.53 inference(resolution,[status(thm)],[f2664,f2577])).
% 0.24/0.53 fof(f2666,plain,(
% 0.24/0.53 c_Transcendental_Ocos(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal))=c_Transcendental_Osin(c_Transcendental_Opi)),
% 0.24/0.53 inference(resolution,[status(thm)],[f2664,f2576])).
% 0.24/0.53 fof(f2680,plain,(
% 0.24/0.53 c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(c_Transcendental_Opi),tc_RealDef_Oreal))=c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(c_Transcendental_Opi),tc_RealDef_Oreal)),
% 0.24/0.53 inference(paramodulation,[status(thm)],[f2532,f2054])).
% 0.24/0.53 fof(f2682,plain,(
% 0.24/0.53 c_Transcendental_Osin(c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(c_Transcendental_Opi,tc_RealDef_Oreal)))=c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(c_Transcendental_Opi),tc_RealDef_Oreal)),
% 0.24/0.53 inference(forward_demodulation,[status(thm)],[f2054,f2680])).
% 0.24/0.53 fof(f2683,plain,(
% 0.24/0.53 c_Transcendental_Osin(c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(c_Transcendental_Opi,tc_RealDef_Oreal)))=c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(c_Transcendental_Opi,tc_RealDef_Oreal))),
% 0.24/0.53 inference(forward_demodulation,[status(thm)],[f2054,f2682])).
% 0.24/0.53 fof(f2759,plain,(
% 0.24/0.53 ![X0]: (~c_Transcendental_Ocos(X0)=c_HOL_Oone__class_Oone(tc_RealDef_Oreal)|c_Transcendental_Osin(X0)=c_Transcendental_Osin(c_Transcendental_Opi))),
% 0.24/0.53 inference(forward_demodulation,[status(thm)],[f2109,f2121])).
% 0.24/0.53 fof(f2762,plain,(
% 0.24/0.53 ![X0]: (~c_Transcendental_Ocos(X0)=c_HOL_Oone__class_Oone(tc_RealDef_Oreal)|c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal))=c_Transcendental_Osin(c_Transcendental_Opi))),
% 0.24/0.53 inference(paramodulation,[status(thm)],[f2051,f2759])).
% 0.24/0.53 fof(f2884,plain,(
% 0.24/0.53 c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(c_Transcendental_Opi),tc_RealDef_Oreal))=c_Transcendental_Osin(c_Transcendental_Opi)),
% 0.24/0.53 inference(resolution,[status(thm)],[f2762,f2533])).
% 0.24/0.53 fof(f2891,plain,(
% 0.24/0.53 c_Transcendental_Osin(c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(c_Transcendental_Opi,tc_RealDef_Oreal)))=c_Transcendental_Osin(c_Transcendental_Opi)),
% 0.24/0.53 inference(forward_demodulation,[status(thm)],[f2054,f2884])).
% 0.24/0.53 fof(f2906,plain,(
% 0.24/0.53 c_Transcendental_Osin(c_Transcendental_Opi)=c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(c_Transcendental_Opi,tc_RealDef_Oreal))),
% 0.24/0.53 inference(backward_demodulation,[status(thm)],[f2891,f2683])).
% 0.24/0.53 fof(f3151,plain,(
% 0.24/0.53 ![X0]: (c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal),X0,tc_RealDef_Oreal))=c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal)),c_Transcendental_Ocos(X0),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(c_Transcendental_Opi),c_Transcendental_Osin(X0),tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 0.24/0.53 inference(paramodulation,[status(thm)],[f2666,f1811])).
% 0.24/0.53 fof(f3242,plain,(
% 0.24/0.53 c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal))=c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(c_Transcendental_Opi),tc_RealDef_Oreal)),
% 0.24/0.53 inference(paramodulation,[status(thm)],[f2649,f2054])).
% 0.24/0.53 fof(f3246,plain,(
% 0.24/0.53 c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal))=c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(c_Transcendental_Opi,tc_RealDef_Oreal))),
% 0.24/0.53 inference(forward_demodulation,[status(thm)],[f2054,f3242])).
% 0.24/0.53 fof(f3247,plain,(
% 0.24/0.53 c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal))=c_Transcendental_Osin(c_Transcendental_Opi)),
% 0.24/0.53 inference(forward_demodulation,[status(thm)],[f2906,f3246])).
% 0.24/0.53 fof(f3298,plain,(
% 0.24/0.53 c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal))=c_Transcendental_Osin(c_Transcendental_Opi)),
% 0.24/0.53 inference(paramodulation,[status(thm)],[f2335,f3247])).
% 0.24/0.53 fof(f3488,plain,(
% 0.24/0.53 c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(c_HOL_Ouminus__class_Ouminus(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal)),c_Transcendental_Ocos(c_HOL_Ouminus__class_Ouminus(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal)),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal)),c_Transcendental_Osin(c_Transcendental_Opi),tc_RealDef_Oreal),tc_RealDef_Oreal)=c_HOL_Oone__class_Oone(tc_RealDef_Oreal)),
% 0.24/0.53 inference(paramodulation,[status(thm)],[f3298,f1869])).
% 0.24/0.53 fof(f3568,plain,(
% 0.24/0.53 c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal)),c_Transcendental_Ocos(c_HOL_Ouminus__class_Ouminus(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal)),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal)),c_Transcendental_Osin(c_Transcendental_Opi),tc_RealDef_Oreal),tc_RealDef_Oreal)=c_HOL_Oone__class_Oone(tc_RealDef_Oreal)),
% 0.24/0.53 inference(forward_demodulation,[status(thm)],[f2051,f3488])).
% 0.24/0.53 fof(f3569,plain,(
% 0.24/0.53 c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(c_Transcendental_Opi),c_Transcendental_Ocos(c_HOL_Ouminus__class_Ouminus(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal)),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal)),c_Transcendental_Osin(c_Transcendental_Opi),tc_RealDef_Oreal),tc_RealDef_Oreal)=c_HOL_Oone__class_Oone(tc_RealDef_Oreal)),
% 0.24/0.53 inference(forward_demodulation,[status(thm)],[f2665,f3568])).
% 0.24/0.53 fof(f3570,plain,(
% 0.24/0.53 c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(c_Transcendental_Opi),c_Transcendental_Ocos(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal)),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal)),c_Transcendental_Osin(c_Transcendental_Opi),tc_RealDef_Oreal),tc_RealDef_Oreal)=c_HOL_Oone__class_Oone(tc_RealDef_Oreal)),
% 0.24/0.53 inference(forward_demodulation,[status(thm)],[f2051,f3569])).
% 0.24/0.53 fof(f3571,plain,(
% 0.24/0.53 c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(c_Transcendental_Opi),c_Transcendental_Osin(c_Transcendental_Opi),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal)),c_Transcendental_Osin(c_Transcendental_Opi),tc_RealDef_Oreal),tc_RealDef_Oreal)=c_HOL_Oone__class_Oone(tc_RealDef_Oreal)),
% 0.24/0.53 inference(forward_demodulation,[status(thm)],[f2665,f3570])).
% 0.24/0.53 fof(f3572,plain,(
% 0.24/0.53 c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(c_Transcendental_Opi),c_Transcendental_Osin(c_Transcendental_Opi),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(c_Transcendental_Opi),c_Transcendental_Osin(c_Transcendental_Opi),tc_RealDef_Oreal),tc_RealDef_Oreal)=c_HOL_Oone__class_Oone(tc_RealDef_Oreal)),
% 0.24/0.53 inference(forward_demodulation,[status(thm)],[f3298,f3571])).
% 0.24/0.53 fof(f4159,plain,(
% 0.24/0.53 c_Transcendental_Osin(c_Transcendental_Opi)=c_Transcendental_Otan(c_Transcendental_Opi)),
% 0.24/0.53 inference(backward_demodulation,[status(thm)],[f1543,f2109])).
% 0.24/0.53 fof(f4196,plain,(
% 0.24/0.53 ~c_Transcendental_Otan(c_Transcendental_Opi)=c_HOL_Oone__class_Oone(tc_RealDef_Oreal)),
% 0.24/0.53 inference(forward_demodulation,[status(thm)],[f1543,f2183])).
% 0.24/0.53 fof(f4225,plain,(
% 0.24/0.53 c_Transcendental_Osin(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal))=c_Transcendental_Otan(c_Transcendental_Opi)),
% 0.24/0.53 inference(backward_demodulation,[status(thm)],[f4159,f2649])).
% 0.24/0.53 fof(f4233,plain,(
% 0.24/0.53 c_Transcendental_Osin(c_Transcendental_Osin(c_Transcendental_Opi))=c_Transcendental_Otan(c_Transcendental_Opi)),
% 0.24/0.53 inference(backward_demodulation,[status(thm)],[f4159,f2532])).
% 0.24/0.53 fof(f4250,plain,(
% 0.24/0.53 c_Transcendental_Ocos(c_Transcendental_Otan(c_Transcendental_Opi))=c_HOL_Oone__class_Oone(tc_RealDef_Oreal)),
% 0.24/0.53 inference(backward_demodulation,[status(thm)],[f4159,f2533])).
% 0.24/0.53 fof(f4276,plain,(
% 0.24/0.53 c_Transcendental_Osin(c_Transcendental_Otan(c_Transcendental_Opi))=c_Transcendental_Otan(c_Transcendental_Opi)),
% 0.24/0.53 inference(forward_demodulation,[status(thm)],[f4159,f4233])).
% 0.24/0.53 fof(f4304,plain,(
% 0.24/0.53 c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Transcendental_Otan(c_Transcendental_Opi),c_Transcendental_Osin(c_Transcendental_Opi),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(c_Transcendental_Opi),c_Transcendental_Osin(c_Transcendental_Opi),tc_RealDef_Oreal),tc_RealDef_Oreal)=c_HOL_Oone__class_Oone(tc_RealDef_Oreal)),
% 0.24/0.53 inference(forward_demodulation,[status(thm)],[f4159,f3572])).
% 0.24/0.53 fof(f4305,plain,(
% 0.24/0.53 c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Transcendental_Otan(c_Transcendental_Opi),c_Transcendental_Otan(c_Transcendental_Opi),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(c_Transcendental_Opi),c_Transcendental_Osin(c_Transcendental_Opi),tc_RealDef_Oreal),tc_RealDef_Oreal)=c_HOL_Oone__class_Oone(tc_RealDef_Oreal)),
% 0.24/0.53 inference(forward_demodulation,[status(thm)],[f4159,f4304])).
% 0.24/0.53 fof(f4306,plain,(
% 0.24/0.53 c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Transcendental_Otan(c_Transcendental_Opi),c_Transcendental_Otan(c_Transcendental_Opi),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Otan(c_Transcendental_Opi),c_Transcendental_Osin(c_Transcendental_Opi),tc_RealDef_Oreal),tc_RealDef_Oreal)=c_HOL_Oone__class_Oone(tc_RealDef_Oreal)),
% 0.24/0.53 inference(forward_demodulation,[status(thm)],[f4159,f4305])).
% 0.24/0.53 fof(f4307,plain,(
% 0.24/0.53 c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Transcendental_Otan(c_Transcendental_Opi),c_Transcendental_Otan(c_Transcendental_Opi),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Otan(c_Transcendental_Opi),c_Transcendental_Otan(c_Transcendental_Opi),tc_RealDef_Oreal),tc_RealDef_Oreal)=c_HOL_Oone__class_Oone(tc_RealDef_Oreal)),
% 0.24/0.53 inference(forward_demodulation,[status(thm)],[f4159,f4306])).
% 0.24/0.53 fof(f4474,plain,(
% 0.24/0.53 ![X0]: (c_HOL_Otimes__class_Otimes(X0,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal)=X0)),
% 0.24/0.53 inference(paramodulation,[status(thm)],[f2335,f2126])).
% 0.24/0.53 fof(f4714,plain,(
% 0.24/0.53 ![X0]: (c_HOL_Oplus__class_Oplus(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)=X0)),
% 0.24/0.53 inference(resolution,[status(thm)],[f1914,f2467])).
% 0.24/0.53 fof(f4717,plain,(
% 0.24/0.53 ![X0]: (c_HOL_Oplus__class_Oplus(X0,c_Transcendental_Otan(c_Transcendental_Opi),tc_RealDef_Oreal)=X0)),
% 0.24/0.53 inference(forward_demodulation,[status(thm)],[f1543,f4714])).
% 0.24/0.53 fof(f4873,plain,(
% 0.24/0.53 ![X0]: (c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)=X0)),
% 0.24/0.53 inference(resolution,[status(thm)],[f1916,f2467])).
% 0.24/0.53 fof(f4876,plain,(
% 0.24/0.53 ![X0]: (c_HOL_Oplus__class_Oplus(c_Transcendental_Otan(c_Transcendental_Opi),X0,tc_RealDef_Oreal)=X0)),
% 0.24/0.53 inference(forward_demodulation,[status(thm)],[f1543,f4873])).
% 0.24/0.53 fof(f5412,plain,(
% 0.24/0.53 ![X0]: (c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal),X0,tc_RealDef_Oreal))=c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Transcendental_Otan(c_Transcendental_Opi),c_Transcendental_Ocos(X0),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(c_Transcendental_Opi),c_Transcendental_Osin(X0),tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 0.24/0.53 inference(forward_demodulation,[status(thm)],[f4225,f3151])).
% 0.24/0.53 fof(f5413,plain,(
% 0.24/0.53 ![X0]: (c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal),X0,tc_RealDef_Oreal))=c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Transcendental_Otan(c_Transcendental_Opi),c_Transcendental_Ocos(X0),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Otan(c_Transcendental_Opi),c_Transcendental_Osin(X0),tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 0.24/0.53 inference(forward_demodulation,[status(thm)],[f4159,f5412])).
% 0.24/0.53 fof(f5416,plain,(
% 0.24/0.53 c_Transcendental_Osin(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal))=c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Transcendental_Otan(c_Transcendental_Opi),c_Transcendental_Ocos(c_Transcendental_Otan(c_Transcendental_Opi)),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Otan(c_Transcendental_Opi),c_Transcendental_Osin(c_Transcendental_Otan(c_Transcendental_Opi)),tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 0.24/0.53 inference(paramodulation,[status(thm)],[f4717,f5413])).
% 0.24/0.53 fof(f5456,plain,(
% 0.24/0.53 c_Transcendental_Otan(c_Transcendental_Opi)=c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Transcendental_Otan(c_Transcendental_Opi),c_Transcendental_Ocos(c_Transcendental_Otan(c_Transcendental_Opi)),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Otan(c_Transcendental_Opi),c_Transcendental_Osin(c_Transcendental_Otan(c_Transcendental_Opi)),tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 0.24/0.53 inference(forward_demodulation,[status(thm)],[f4225,f5416])).
% 0.24/0.53 fof(f5457,plain,(
% 0.24/0.53 c_Transcendental_Otan(c_Transcendental_Opi)=c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Transcendental_Otan(c_Transcendental_Opi),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Otan(c_Transcendental_Opi),c_Transcendental_Osin(c_Transcendental_Otan(c_Transcendental_Opi)),tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 0.24/0.53 inference(forward_demodulation,[status(thm)],[f4250,f5456])).
% 0.24/0.53 fof(f5458,plain,(
% 0.24/0.53 c_Transcendental_Otan(c_Transcendental_Opi)=c_HOL_Oplus__class_Oplus(c_Transcendental_Otan(c_Transcendental_Opi),c_HOL_Otimes__class_Otimes(c_Transcendental_Otan(c_Transcendental_Opi),c_Transcendental_Osin(c_Transcendental_Otan(c_Transcendental_Opi)),tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 0.24/0.53 inference(forward_demodulation,[status(thm)],[f4474,f5457])).
% 0.24/0.53 fof(f5459,plain,(
% 0.24/0.53 c_Transcendental_Otan(c_Transcendental_Opi)=c_HOL_Otimes__class_Otimes(c_Transcendental_Otan(c_Transcendental_Opi),c_Transcendental_Osin(c_Transcendental_Otan(c_Transcendental_Opi)),tc_RealDef_Oreal)),
% 0.24/0.53 inference(forward_demodulation,[status(thm)],[f4876,f5458])).
% 0.24/0.53 fof(f5460,plain,(
% 0.24/0.53 c_Transcendental_Otan(c_Transcendental_Opi)=c_HOL_Otimes__class_Otimes(c_Transcendental_Otan(c_Transcendental_Opi),c_Transcendental_Otan(c_Transcendental_Opi),tc_RealDef_Oreal)),
% 0.24/0.53 inference(forward_demodulation,[status(thm)],[f4276,f5459])).
% 0.24/0.53 fof(f5506,plain,(
% 0.24/0.53 c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Transcendental_Otan(c_Transcendental_Opi),c_Transcendental_Otan(c_Transcendental_Opi),tc_RealDef_Oreal),c_Transcendental_Otan(c_Transcendental_Opi),tc_RealDef_Oreal)=c_HOL_Oone__class_Oone(tc_RealDef_Oreal)),
% 0.24/0.53 inference(backward_demodulation,[status(thm)],[f5460,f4307])).
% 0.24/0.53 fof(f5507,plain,(
% 0.24/0.53 c_HOL_Otimes__class_Otimes(c_Transcendental_Otan(c_Transcendental_Opi),c_Transcendental_Otan(c_Transcendental_Opi),tc_RealDef_Oreal)=c_HOL_Oone__class_Oone(tc_RealDef_Oreal)),
% 0.24/0.53 inference(forward_demodulation,[status(thm)],[f4717,f5506])).
% 0.24/0.53 fof(f5508,plain,(
% 0.24/0.53 c_Transcendental_Otan(c_Transcendental_Opi)=c_HOL_Oone__class_Oone(tc_RealDef_Oreal)),
% 0.24/0.53 inference(forward_demodulation,[status(thm)],[f5460,f5507])).
% 0.24/0.53 fof(f5509,plain,(
% 0.24/0.53 $false),
% 0.24/0.53 inference(forward_subsumption_resolution,[status(thm)],[f5508,f4196])).
% 0.24/0.53 % SZS output end CNFRefutation for theBenchmark.p
% 0.24/0.58 % Elapsed time: 0.195462 seconds
% 0.24/0.58 % CPU time: 0.744849 seconds
% 0.24/0.58 % Total memory used: 165.212 MB
% 0.24/0.58 % Net memory used: 164.423 MB
%------------------------------------------------------------------------------