%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV602-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 : n016.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:52:53 PM UTC 2026
% Result : Unsatisfiable 0.25s 0.58s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV602-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.12/0.37 % Computer : n016.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Mon Sep 21 09:18:22 UTC 2026
% 0.12/0.37 % CPUTime :
% 0.16/0.45 % Drodi V4.1.1
% 0.25/0.58 % Refutation found
% 0.25/0.58 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.25/0.58 % SZS output start CNFRefutation for theBenchmark
% 0.25/0.58 fof(f91,axiom,(
% 0.25/0.58 (![V_r,V_s]: (c_HOL_Ominus__class_Ominus(V_r,V_s,tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(V_r,c_HOL_Ouminus__class_Ouminus(V_s,tc_RealDef_Oreal),tc_RealDef_Oreal) ))),
% 0.25/0.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.25/0.58 fof(f104,axiom,(
% 0.25/0.58 (![V_x]: (c_Transcendental_Otan(c_HOL_Ouminus__class_Ouminus(V_x,tc_RealDef_Oreal)) = c_HOL_Ouminus__class_Ouminus(c_Transcendental_Otan(V_x),tc_RealDef_Oreal) ))),
% 0.25/0.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.25/0.58 fof(f183,axiom,(
% 0.25/0.58 (![V_x,V_y]: (c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(V_x,V_y,tc_RealDef_Oreal)) = c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(V_x),c_Transcendental_Ocos(V_y),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(V_x),c_Transcendental_Osin(V_y),tc_RealDef_Oreal),tc_RealDef_Oreal) ))),
% 0.25/0.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.25/0.58 fof(f422,axiom,(
% 0.25/0.58 (![V_x]: (c_HOL_Oplus__class_Oplus(V_x,c_HOL_Ouminus__class_Ouminus(V_x,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ))),
% 0.25/0.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.25/0.58 fof(f550,axiom,(
% 0.25/0.58 c_Transcendental_Otan(c_Transcendental_Opi) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
% 0.25/0.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.25/0.58 fof(f553,axiom,(
% 0.25/0.58 c_Transcendental_Ocos(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)) = c_HOL_Oone__class_Oone(tc_RealDef_Oreal) ),
% 0.25/0.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.25/0.58 fof(f679,axiom,(
% 0.25/0.58 c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) != c_HOL_Oone__class_Oone(tc_RealDef_Oreal) ),
% 0.25/0.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.25/0.58 fof(f709,axiom,(
% 0.25/0.58 (![V_x]: (c_Transcendental_Ocos(c_HOL_Ouminus__class_Ouminus(V_x,tc_RealDef_Oreal)) = c_Transcendental_Ocos(V_x) ))),
% 0.25/0.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.25/0.58 fof(f713,axiom,(
% 0.25/0.58 (![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.25/0.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.25/0.58 fof(f715,axiom,(
% 0.25/0.58 (![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.25/0.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.25/0.58 fof(f857,axiom,(
% 0.25/0.58 c_Transcendental_Osin(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
% 0.25/0.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.25/0.58 fof(f915,negated_conjecture,(
% 0.25/0.58 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_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
% 0.25/0.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.25/0.58 fof(f916,negated_conjecture,(
% 0.25/0.58 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_RealDef_Oreal) ),
% 0.25/0.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.25/0.58 fof(f1186,plain,(
% 0.25/0.58 ![X0,X1]: (c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal)=c_HOL_Oplus__class_Oplus(X0,c_HOL_Ouminus__class_Ouminus(X1,tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 0.25/0.58 inference(cnf_transformation,[status(thm)],[f91])).
% 0.25/0.58 fof(f1201,plain,(
% 0.25/0.58 ![X0]: (c_Transcendental_Otan(c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal))=c_HOL_Ouminus__class_Ouminus(c_Transcendental_Otan(X0),tc_RealDef_Oreal))),
% 0.25/0.58 inference(cnf_transformation,[status(thm)],[f104])).
% 0.25/0.58 fof(f1323,plain,(
% 0.25/0.58 ![X0,X1]: (c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(X0,X1,tc_RealDef_Oreal))=c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(X0),c_Transcendental_Ocos(X1),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(X0),c_Transcendental_Osin(X1),tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 0.25/0.58 inference(cnf_transformation,[status(thm)],[f183])).
% 0.25/0.58 fof(f1693,plain,(
% 0.25/0.58 ![X0]: (c_HOL_Oplus__class_Oplus(X0,c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal),tc_RealDef_Oreal)=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal))),
% 0.25/0.58 inference(cnf_transformation,[status(thm)],[f422])).
% 0.25/0.58 fof(f1898,plain,(
% 0.25/0.58 c_Transcendental_Otan(c_Transcendental_Opi)=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)),
% 0.25/0.58 inference(cnf_transformation,[status(thm)],[f550])).
% 0.25/0.58 fof(f1901,plain,(
% 0.25/0.58 c_Transcendental_Ocos(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal))=c_HOL_Oone__class_Oone(tc_RealDef_Oreal)),
% 0.25/0.58 inference(cnf_transformation,[status(thm)],[f553])).
% 0.25/0.58 fof(f2095,plain,(
% 0.25/0.58 ~c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)=c_HOL_Oone__class_Oone(tc_RealDef_Oreal)),
% 0.25/0.58 inference(cnf_transformation,[status(thm)],[f679])).
% 0.25/0.58 fof(f2143,plain,(
% 0.25/0.58 ![X0]: (c_Transcendental_Ocos(c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal))=c_Transcendental_Ocos(X0))),
% 0.25/0.58 inference(cnf_transformation,[status(thm)],[f709])).
% 0.25/0.58 fof(f2147,plain,(
% 0.25/0.58 ![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.25/0.58 inference(cnf_transformation,[status(thm)],[f713])).
% 0.25/0.58 fof(f2149,plain,(
% 0.25/0.58 ![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.25/0.58 inference(cnf_transformation,[status(thm)],[f715])).
% 0.25/0.58 fof(f2331,plain,(
% 0.25/0.58 c_Transcendental_Osin(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal))=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)),
% 0.25/0.58 inference(cnf_transformation,[status(thm)],[f857])).
% 0.25/0.58 fof(f2430,plain,(
% 0.25/0.58 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_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)),
% 0.25/0.58 inference(cnf_transformation,[status(thm)],[f915])).
% 0.25/0.58 fof(f2431,plain,(
% 0.25/0.58 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_RealDef_Oreal)),
% 0.25/0.58 inference(cnf_transformation,[status(thm)],[f916])).
% 0.25/0.58 fof(f2586,plain,(
% 0.25/0.58 ![X0]: (c_HOL_Ominus__class_Ominus(X0,X0,tc_RealDef_Oreal)=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal))),
% 0.25/0.58 inference(forward_demodulation,[status(thm)],[f1186,f1693])).
% 0.25/0.58 fof(f2613,plain,(
% 0.25/0.58 ![X0]: (c_HOL_Ominus__class_Ominus(X0,X0,tc_RealDef_Oreal)=c_Transcendental_Otan(c_Transcendental_Opi))),
% 0.25/0.58 inference(backward_demodulation,[status(thm)],[f1898,f2586])).
% 0.25/0.58 fof(f2641,plain,(
% 0.25/0.58 c_Transcendental_Ocos(c_Transcendental_Otan(c_Transcendental_Opi))=c_HOL_Oone__class_Oone(tc_RealDef_Oreal)),
% 0.25/0.58 inference(forward_demodulation,[status(thm)],[f1898,f1901])).
% 0.25/0.58 fof(f2660,plain,(
% 0.25/0.58 ~c_Transcendental_Otan(c_Transcendental_Opi)=c_HOL_Oone__class_Oone(tc_RealDef_Oreal)),
% 0.25/0.58 inference(forward_demodulation,[status(thm)],[f1898,f2095])).
% 0.25/0.58 fof(f2682,plain,(
% 0.25/0.58 ![X0]: (~c_Transcendental_Ocos(X0)=c_HOL_Oone__class_Oone(tc_RealDef_Oreal)|c_Transcendental_Osin(X0)=c_Transcendental_Otan(c_Transcendental_Opi))),
% 0.25/0.58 inference(forward_demodulation,[status(thm)],[f1898,f2149])).
% 0.25/0.58 fof(f2731,plain,(
% 0.25/0.58 c_Transcendental_Osin(c_Transcendental_Otan(c_Transcendental_Opi))=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)),
% 0.25/0.58 inference(forward_demodulation,[status(thm)],[f1898,f2331])).
% 0.25/0.58 fof(f2732,plain,(
% 0.25/0.58 c_Transcendental_Osin(c_Transcendental_Otan(c_Transcendental_Opi))=c_Transcendental_Otan(c_Transcendental_Opi)),
% 0.25/0.58 inference(forward_demodulation,[status(thm)],[f1898,f2731])).
% 0.25/0.58 fof(f2743,plain,(
% 0.25/0.58 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_Otan(c_Transcendental_Opi)),
% 0.25/0.58 inference(forward_demodulation,[status(thm)],[f1898,f2430])).
% 0.25/0.58 fof(f2744,plain,(
% 0.25/0.58 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.25/0.58 inference(forward_demodulation,[status(thm)],[f1898,f2431])).
% 0.25/0.58 fof(f2804,plain,(
% 0.25/0.58 ![X0]: (c_Transcendental_Ocos(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_Ominus__class_Ominus(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_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(X0),tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 0.25/0.58 inference(paramodulation,[status(thm)],[f2743,f1323])).
% 0.25/0.58 fof(f2816,plain,(
% 0.25/0.58 ![X0]: (c_Transcendental_Ocos(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_Ominus__class_Ominus(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.25/0.58 inference(forward_demodulation,[status(thm)],[f2744,f2804])).
% 0.25/0.58 fof(f2854,plain,(
% 0.25/0.58 c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(c_Transcendental_Otan(c_Transcendental_Opi),tc_RealDef_Oreal))=c_HOL_Ouminus__class_Ouminus(c_Transcendental_Otan(c_Transcendental_Opi),tc_RealDef_Oreal)),
% 0.25/0.58 inference(paramodulation,[status(thm)],[f2732,f2147])).
% 0.25/0.58 fof(f2856,plain,(
% 0.25/0.58 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_Otan(c_Transcendental_Opi),tc_RealDef_Oreal)),
% 0.25/0.58 inference(paramodulation,[status(thm)],[f2744,f2147])).
% 0.25/0.58 fof(f2857,plain,(
% 0.25/0.58 ![X0]: (c_Transcendental_Ocos(c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal)))=c_Transcendental_Ocos(c_Transcendental_Osin(X0)))),
% 0.25/0.58 inference(paramodulation,[status(thm)],[f2147,f2143])).
% 0.25/0.58 fof(f2858,plain,(
% 0.25/0.58 c_Transcendental_Osin(c_Transcendental_Otan(c_HOL_Ouminus__class_Ouminus(c_Transcendental_Opi,tc_RealDef_Oreal)))=c_HOL_Ouminus__class_Ouminus(c_Transcendental_Otan(c_Transcendental_Opi),tc_RealDef_Oreal)),
% 0.25/0.58 inference(forward_demodulation,[status(thm)],[f1201,f2854])).
% 0.25/0.58 fof(f2859,plain,(
% 0.25/0.58 c_Transcendental_Osin(c_Transcendental_Otan(c_HOL_Ouminus__class_Ouminus(c_Transcendental_Opi,tc_RealDef_Oreal)))=c_Transcendental_Otan(c_HOL_Ouminus__class_Ouminus(c_Transcendental_Opi,tc_RealDef_Oreal))),
% 0.25/0.58 inference(forward_demodulation,[status(thm)],[f1201,f2858])).
% 0.25/0.58 fof(f2861,plain,(
% 0.25/0.58 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_Otan(c_HOL_Ouminus__class_Ouminus(c_Transcendental_Opi,tc_RealDef_Oreal))),
% 0.25/0.58 inference(forward_demodulation,[status(thm)],[f1201,f2856])).
% 0.25/0.58 fof(f3015,plain,(
% 0.25/0.58 c_Transcendental_Ocos(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),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),tc_RealDef_Oreal))=c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(c_Transcendental_Otan(c_Transcendental_Opi),c_Transcendental_Ocos(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)),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Otan(c_Transcendental_Opi),c_Transcendental_Otan(c_HOL_Ouminus__class_Ouminus(c_Transcendental_Opi,tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 0.25/0.58 inference(paramodulation,[status(thm)],[f2861,f2816])).
% 0.25/0.58 fof(f3030,plain,(
% 0.25/0.58 c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(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_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_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(c_Transcendental_Otan(c_Transcendental_Opi),c_Transcendental_Ocos(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)),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Otan(c_Transcendental_Opi),c_Transcendental_Otan(c_HOL_Ouminus__class_Ouminus(c_Transcendental_Opi,tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 0.25/0.58 inference(forward_demodulation,[status(thm)],[f1186,f3015])).
% 0.25/0.58 fof(f3031,plain,(
% 0.25/0.58 c_Transcendental_Ocos(c_Transcendental_Otan(c_Transcendental_Opi))=c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(c_Transcendental_Otan(c_Transcendental_Opi),c_Transcendental_Ocos(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)),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Otan(c_Transcendental_Opi),c_Transcendental_Otan(c_HOL_Ouminus__class_Ouminus(c_Transcendental_Opi,tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 0.25/0.58 inference(forward_demodulation,[status(thm)],[f2613,f3030])).
% 0.25/0.58 fof(f3032,plain,(
% 0.25/0.58 c_HOL_Oone__class_Oone(tc_RealDef_Oreal)=c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(c_Transcendental_Otan(c_Transcendental_Opi),c_Transcendental_Ocos(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)),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Otan(c_Transcendental_Opi),c_Transcendental_Otan(c_HOL_Ouminus__class_Ouminus(c_Transcendental_Opi,tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 0.25/0.58 inference(forward_demodulation,[status(thm)],[f2641,f3031])).
% 0.25/0.58 fof(f3033,plain,(
% 0.25/0.58 c_HOL_Oone__class_Oone(tc_RealDef_Oreal)=c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(c_Transcendental_Otan(c_Transcendental_Opi),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)),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Otan(c_Transcendental_Opi),c_Transcendental_Otan(c_HOL_Ouminus__class_Ouminus(c_Transcendental_Opi,tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 0.25/0.58 inference(forward_demodulation,[status(thm)],[f2143,f3032])).
% 0.25/0.58 fof(f3034,plain,(
% 0.25/0.58 c_HOL_Oone__class_Oone(tc_RealDef_Oreal)=c_HOL_Ominus__class_Ominus(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_HOL_Ouminus__class_Ouminus(c_Transcendental_Opi,tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 0.25/0.58 inference(forward_demodulation,[status(thm)],[f2743,f3033])).
% 0.25/0.58 fof(f3065,plain,(
% 0.25/0.58 c_Transcendental_Ocos(c_Transcendental_Otan(c_HOL_Ouminus__class_Ouminus(c_Transcendental_Opi,tc_RealDef_Oreal)))=c_Transcendental_Ocos(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)))),
% 0.25/0.58 inference(paramodulation,[status(thm)],[f2861,f2857])).
% 0.25/0.58 fof(f3076,plain,(
% 0.25/0.58 c_Transcendental_Ocos(c_Transcendental_Otan(c_HOL_Ouminus__class_Ouminus(c_Transcendental_Opi,tc_RealDef_Oreal)))=c_Transcendental_Ocos(c_Transcendental_Otan(c_Transcendental_Opi))),
% 0.25/0.58 inference(forward_demodulation,[status(thm)],[f2744,f3065])).
% 0.25/0.58 fof(f3077,plain,(
% 0.25/0.58 c_Transcendental_Ocos(c_Transcendental_Otan(c_HOL_Ouminus__class_Ouminus(c_Transcendental_Opi,tc_RealDef_Oreal)))=c_HOL_Oone__class_Oone(tc_RealDef_Oreal)),
% 0.25/0.58 inference(forward_demodulation,[status(thm)],[f2641,f3076])).
% 0.25/0.58 fof(f3078,plain,(
% 0.25/0.58 c_Transcendental_Osin(c_Transcendental_Otan(c_HOL_Ouminus__class_Ouminus(c_Transcendental_Opi,tc_RealDef_Oreal)))=c_Transcendental_Otan(c_Transcendental_Opi)),
% 0.25/0.58 inference(resolution,[status(thm)],[f3077,f2682])).
% 0.25/0.58 fof(f3088,plain,(
% 0.25/0.58 c_Transcendental_Otan(c_Transcendental_Opi)=c_Transcendental_Otan(c_HOL_Ouminus__class_Ouminus(c_Transcendental_Opi,tc_RealDef_Oreal))),
% 0.25/0.58 inference(backward_demodulation,[status(thm)],[f3078,f2859])).
% 0.25/0.58 fof(f3118,plain,(
% 0.25/0.58 c_HOL_Oone__class_Oone(tc_RealDef_Oreal)=c_HOL_Ominus__class_Ominus(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)),
% 0.25/0.58 inference(backward_demodulation,[status(thm)],[f3088,f3034])).
% 0.25/0.58 fof(f3127,plain,(
% 0.25/0.58 c_HOL_Oone__class_Oone(tc_RealDef_Oreal)=c_Transcendental_Otan(c_Transcendental_Opi)),
% 0.25/0.58 inference(forward_demodulation,[status(thm)],[f2613,f3118])).
% 0.25/0.58 fof(f3128,plain,(
% 0.25/0.58 $false),
% 0.25/0.58 inference(forward_subsumption_resolution,[status(thm)],[f3127,f2660])).
% 0.25/0.58 % SZS output end CNFRefutation for theBenchmark.p
% 0.25/0.62 % Elapsed time: 0.240949 seconds
% 0.25/0.62 % CPU time: 1.055160 seconds
% 0.25/0.62 % Total memory used: 173.425 MB
% 0.25/0.62 % Net memory used: 172.420 MB
%------------------------------------------------------------------------------