%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV596-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n012.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.09s 0.48s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV596-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n012.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 09:12:53 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.45 % Drodi V4.1.1
% 0.09/0.48 % Refutation found
% 0.09/0.48 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.09/0.48 % SZS output start CNFRefutation for theBenchmark
% 0.09/0.48 fof(f370,axiom,(
% 0.09/0.48 (![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.09/0.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.48 fof(f820,axiom,(
% 0.09/0.48 (![V_x]: (~ c_HOL_Oord__class_Oless(V_x,V_x,tc_RealDef_Oreal) ))),
% 0.09/0.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.48 fof(f1089,axiom,(
% 0.09/0.48 (![V_x]: (c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(c_Transcendental_Opi,V_x,tc_RealDef_Oreal)) = c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(V_x),tc_RealDef_Oreal) ))),
% 0.09/0.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.48 fof(f1090,axiom,(
% 0.09/0.48 (![V_x]: (c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(V_x,c_Transcendental_Opi,tc_RealDef_Oreal)) = c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(V_x),tc_RealDef_Oreal) ))),
% 0.09/0.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.48 fof(f1092,axiom,(
% 0.09/0.48 (![V_y,V_z]: (V_y = c_HOL_Oplus__class_Oplus(c_HOL_Ominus__class_Ominus(V_y,V_z,tc_RealDef_Oreal),V_z,tc_RealDef_Oreal) ))),
% 0.09/0.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.48 fof(f1096,axiom,(
% 0.09/0.48 (![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.09/0.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.48 fof(f1113,axiom,(
% 0.09/0.48 c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal) ),
% 0.09/0.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.48 fof(f1128,axiom,(
% 0.09/0.48 (![V_x]: (( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Transcendental_Osin(V_x),tc_RealDef_Oreal)| ~ c_HOL_Oord__class_Oless(V_x,c_Transcendental_Opi,tc_RealDef_Oreal)| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_x,tc_RealDef_Oreal) ) ))),
% 0.09/0.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.48 fof(f1130,axiom,(
% 0.09/0.48 (![V_x]: (c_Transcendental_Osin(c_HOL_Ominus__class_Ominus(V_x,c_Transcendental_Opi,tc_RealDef_Oreal)) = c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(V_x),tc_RealDef_Oreal) ))),
% 0.09/0.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.48 fof(f1133,axiom,(
% 0.09/0.48 c_Transcendental_Osin(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
% 0.09/0.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.48 fof(f1139,axiom,(
% 0.09/0.48 c_Transcendental_Osin(c_Transcendental_Opi) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
% 0.09/0.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.48 fof(f1145,axiom,(
% 0.09/0.48 c_HOL_Oord__class_Oless(c_HOL_Ominus__class_Ominus(v_x,c_Transcendental_Opi,tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal) ),
% 0.09/0.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.48 fof(f1146,axiom,(
% 0.09/0.48 c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ominus__class_Ominus(v_x,c_Transcendental_Opi,tc_RealDef_Oreal),tc_RealDef_Oreal) ),
% 0.09/0.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.48 fof(f1147,negated_conjecture,(
% 0.09/0.48 c_Transcendental_Osin(c_HOL_Ominus__class_Ominus(v_x,c_Transcendental_Opi,tc_RealDef_Oreal)) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
% 0.09/0.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.48 fof(f1867,plain,(
% 0.09/0.48 ![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.09/0.48 inference(cnf_transformation,[status(thm)],[f370])).
% 0.09/0.48 fof(f2598,plain,(
% 0.09/0.48 ![X0]: (~c_HOL_Oord__class_Oless(X0,X0,tc_RealDef_Oreal))),
% 0.09/0.48 inference(cnf_transformation,[status(thm)],[f820])).
% 0.09/0.48 fof(f3021,plain,(
% 0.09/0.48 ![X0]: (c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(c_Transcendental_Opi,X0,tc_RealDef_Oreal))=c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(X0),tc_RealDef_Oreal))),
% 0.09/0.48 inference(cnf_transformation,[status(thm)],[f1089])).
% 0.09/0.48 fof(f3022,plain,(
% 0.09/0.48 ![X0]: (c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(X0,c_Transcendental_Opi,tc_RealDef_Oreal))=c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(X0),tc_RealDef_Oreal))),
% 0.09/0.48 inference(cnf_transformation,[status(thm)],[f1090])).
% 0.09/0.48 fof(f3024,plain,(
% 0.09/0.48 ![X0,X1]: (X0=c_HOL_Oplus__class_Oplus(c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal),X1,tc_RealDef_Oreal))),
% 0.09/0.48 inference(cnf_transformation,[status(thm)],[f1092])).
% 0.09/0.48 fof(f3028,plain,(
% 0.09/0.48 ![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.09/0.48 inference(cnf_transformation,[status(thm)],[f1096])).
% 0.09/0.48 fof(f3050,plain,(
% 0.09/0.48 c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal)),
% 0.09/0.48 inference(cnf_transformation,[status(thm)],[f1113])).
% 0.09/0.48 fof(f3070,plain,(
% 0.09/0.48 ![X0]: (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Transcendental_Osin(X0),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X0,c_Transcendental_Opi,tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal))),
% 0.09/0.48 inference(cnf_transformation,[status(thm)],[f1128])).
% 0.09/0.48 fof(f3072,plain,(
% 0.09/0.48 ![X0]: (c_Transcendental_Osin(c_HOL_Ominus__class_Ominus(X0,c_Transcendental_Opi,tc_RealDef_Oreal))=c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(X0),tc_RealDef_Oreal))),
% 0.09/0.48 inference(cnf_transformation,[status(thm)],[f1130])).
% 0.09/0.48 fof(f3075,plain,(
% 0.09/0.48 c_Transcendental_Osin(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal))=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)),
% 0.09/0.48 inference(cnf_transformation,[status(thm)],[f1133])).
% 0.09/0.48 fof(f3086,plain,(
% 0.09/0.48 c_Transcendental_Osin(c_Transcendental_Opi)=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)),
% 0.09/0.48 inference(cnf_transformation,[status(thm)],[f1139])).
% 0.09/0.48 fof(f3097,plain,(
% 0.09/0.48 c_HOL_Oord__class_Oless(c_HOL_Ominus__class_Ominus(v_x,c_Transcendental_Opi,tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal)),
% 0.09/0.48 inference(cnf_transformation,[status(thm)],[f1145])).
% 0.09/0.48 fof(f3098,plain,(
% 0.09/0.48 c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ominus__class_Ominus(v_x,c_Transcendental_Opi,tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 0.09/0.49 inference(cnf_transformation,[status(thm)],[f1146])).
% 0.09/0.49 fof(f3099,plain,(
% 0.09/0.49 c_Transcendental_Osin(c_HOL_Ominus__class_Ominus(v_x,c_Transcendental_Opi,tc_RealDef_Oreal))=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)),
% 0.09/0.49 inference(cnf_transformation,[status(thm)],[f1147])).
% 0.09/0.49 fof(f3238,plain,(
% 0.09/0.49 c_Transcendental_Osin(c_HOL_Ominus__class_Ominus(v_x,c_Transcendental_Opi,tc_RealDef_Oreal))=c_Transcendental_Osin(c_Transcendental_Opi)),
% 0.09/0.49 inference(backward_demodulation,[status(thm)],[f3086,f3099])).
% 0.09/0.49 fof(f3240,plain,(
% 0.09/0.49 c_HOL_Oord__class_Oless(c_Transcendental_Osin(c_Transcendental_Opi),c_Transcendental_Opi,tc_RealDef_Oreal)),
% 0.09/0.49 inference(forward_demodulation,[status(thm)],[f3086,f3050])).
% 0.09/0.49 fof(f3244,plain,(
% 0.09/0.49 c_Transcendental_Osin(c_Transcendental_Osin(c_Transcendental_Opi))=c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)),
% 0.09/0.49 inference(forward_demodulation,[status(thm)],[f3086,f3075])).
% 0.09/0.49 fof(f3245,plain,(
% 0.09/0.49 c_Transcendental_Osin(c_Transcendental_Osin(c_Transcendental_Opi))=c_Transcendental_Osin(c_Transcendental_Opi)),
% 0.09/0.49 inference(forward_demodulation,[status(thm)],[f3086,f3244])).
% 0.09/0.49 fof(f3262,plain,(
% 0.09/0.49 ![X0,X1]: (X0=c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(X0,c_HOL_Ouminus__class_Ouminus(X1,tc_RealDef_Oreal),tc_RealDef_Oreal),X1,tc_RealDef_Oreal))),
% 0.09/0.49 inference(paramodulation,[status(thm)],[f1867,f3024])).
% 0.09/0.49 fof(f3267,plain,(
% 0.09/0.49 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.09/0.49 inference(paramodulation,[status(thm)],[f3245,f3028])).
% 0.09/0.49 fof(f3268,plain,(
% 0.09/0.49 c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(c_HOL_Ominus__class_Ominus(v_x,c_Transcendental_Opi,tc_RealDef_Oreal),tc_RealDef_Oreal))=c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(c_Transcendental_Opi),tc_RealDef_Oreal)),
% 0.09/0.49 inference(paramodulation,[status(thm)],[f3238,f3028])).
% 0.09/0.49 fof(f3270,plain,(
% 0.09/0.49 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.09/0.49 inference(forward_demodulation,[status(thm)],[f3028,f3267])).
% 0.09/0.49 fof(f3271,plain,(
% 0.09/0.49 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.09/0.49 inference(forward_demodulation,[status(thm)],[f3028,f3270])).
% 0.09/0.49 fof(f3272,plain,(
% 0.09/0.49 c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(c_HOL_Ominus__class_Ominus(v_x,c_Transcendental_Opi,tc_RealDef_Oreal),tc_RealDef_Oreal))=c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(c_Transcendental_Opi,tc_RealDef_Oreal))),
% 0.09/0.49 inference(forward_demodulation,[status(thm)],[f3028,f3268])).
% 0.09/0.49 fof(f3280,plain,(
% 0.09/0.49 ![X0]: (c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(c_Transcendental_Opi,X0,tc_RealDef_Oreal))=c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal)))),
% 0.09/0.49 inference(forward_demodulation,[status(thm)],[f3028,f3021])).
% 0.09/0.49 fof(f3281,plain,(
% 0.09/0.49 ![X0]: (c_Transcendental_Osin(c_HOL_Ominus__class_Ominus(c_Transcendental_Opi,X0,tc_RealDef_Oreal))=c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal),tc_RealDef_Oreal)))),
% 0.09/0.49 inference(paramodulation,[status(thm)],[f1867,f3280])).
% 0.09/0.49 fof(f3285,plain,(
% 0.09/0.49 ![X0]: (c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(X0,c_Transcendental_Opi,tc_RealDef_Oreal))=c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal)))),
% 0.09/0.49 inference(forward_demodulation,[status(thm)],[f3028,f3022])).
% 0.09/0.49 fof(f3287,plain,(
% 0.09/0.49 ![X0]: (c_Transcendental_Osin(X0)=c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(c_HOL_Ominus__class_Ominus(X0,c_Transcendental_Opi,tc_RealDef_Oreal),tc_RealDef_Oreal)))),
% 0.09/0.49 inference(paramodulation,[status(thm)],[f3024,f3285])).
% 0.09/0.49 fof(f3292,plain,(
% 0.09/0.49 c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(v_x,tc_RealDef_Oreal))=c_Transcendental_Osin(c_Transcendental_Opi)),
% 0.09/0.49 inference(backward_demodulation,[status(thm)],[f3293,f3238])).
% 0.09/0.49 fof(f3293,plain,(
% 0.09/0.49 ![X0]: (c_Transcendental_Osin(c_HOL_Ominus__class_Ominus(X0,c_Transcendental_Opi,tc_RealDef_Oreal))=c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal)))),
% 0.09/0.49 inference(forward_demodulation,[status(thm)],[f3028,f3072])).
% 0.09/0.49 fof(f3298,plain,(
% 0.09/0.49 c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(v_x,tc_RealDef_Oreal),tc_RealDef_Oreal))=c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(c_Transcendental_Opi),tc_RealDef_Oreal)),
% 0.09/0.49 inference(paramodulation,[status(thm)],[f3292,f3028])).
% 0.09/0.49 fof(f3300,plain,(
% 0.09/0.49 c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(v_x,tc_RealDef_Oreal),tc_RealDef_Oreal))=c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(c_Transcendental_Opi,tc_RealDef_Oreal))),
% 0.09/0.49 inference(forward_demodulation,[status(thm)],[f3028,f3298])).
% 0.09/0.49 fof(f3301,plain,(
% 0.09/0.49 c_HOL_Oord__class_Oless(c_Transcendental_Osin(c_Transcendental_Opi),c_HOL_Ominus__class_Ominus(v_x,c_Transcendental_Opi,tc_RealDef_Oreal),tc_RealDef_Oreal)),
% 0.09/0.49 inference(forward_demodulation,[status(thm)],[f3086,f3098])).
% 0.09/0.49 fof(f3306,plain,(
% 0.09/0.49 ![X0,X1]: (c_HOL_Ominus__class_Ominus(X0,c_HOL_Ouminus__class_Ouminus(X1,tc_RealDef_Oreal),tc_RealDef_Oreal)=c_HOL_Oplus__class_Oplus(X0,X1,tc_RealDef_Oreal))),
% 0.09/0.49 inference(paramodulation,[status(thm)],[f3262,f3024])).
% 0.09/0.49 fof(f3332,plain,(
% 0.09/0.49 c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(v_x,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal))=c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(c_Transcendental_Opi,tc_RealDef_Oreal)),tc_RealDef_Oreal)),
% 0.09/0.49 inference(paramodulation,[status(thm)],[f3300,f3028])).
% 0.09/0.49 fof(f3334,plain,(
% 0.09/0.49 c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(v_x,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal))=c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(c_Transcendental_Opi,tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 0.09/0.49 inference(forward_demodulation,[status(thm)],[f3028,f3332])).
% 0.09/0.49 fof(f3335,plain,(
% 0.09/0.49 c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(v_x,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal))=c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(c_Transcendental_Opi,tc_RealDef_Oreal),tc_RealDef_Oreal)),tc_RealDef_Oreal)),
% 0.09/0.49 inference(paramodulation,[status(thm)],[f3334,f3028])).
% 0.09/0.49 fof(f3337,plain,(
% 0.09/0.49 c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(v_x,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal))=c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(c_Transcendental_Opi,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 0.09/0.49 inference(forward_demodulation,[status(thm)],[f3028,f3335])).
% 0.09/0.49 fof(f3338,plain,(
% 0.09/0.49 c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(v_x,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal))=c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(c_Transcendental_Opi,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)),tc_RealDef_Oreal)),
% 0.09/0.49 inference(paramodulation,[status(thm)],[f3337,f3028])).
% 0.09/0.49 fof(f3340,plain,(
% 0.09/0.49 c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(v_x,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal))=c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(c_Transcendental_Opi,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 0.09/0.49 inference(forward_demodulation,[status(thm)],[f3028,f3338])).
% 0.09/0.49 fof(f3355,plain,(
% 0.09/0.49 c_Transcendental_Osin(v_x)=c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(c_Transcendental_Opi,tc_RealDef_Oreal))),
% 0.09/0.49 inference(backward_demodulation,[status(thm)],[f3287,f3272])).
% 0.09/0.49 fof(f3390,plain,(
% 0.09/0.49 c_Transcendental_Osin(c_Transcendental_Osin(v_x))=c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(c_Transcendental_Opi,tc_RealDef_Oreal))),
% 0.09/0.49 inference(forward_demodulation,[status(thm)],[f3355,f3271])).
% 0.09/0.49 fof(f3391,plain,(
% 0.09/0.49 c_Transcendental_Osin(c_Transcendental_Osin(v_x))=c_Transcendental_Osin(v_x)),
% 0.09/0.49 inference(forward_demodulation,[status(thm)],[f3355,f3390])).
% 0.09/0.49 fof(f3404,plain,(
% 0.09/0.49 ![X0]: (c_HOL_Oord__class_Oless(c_Transcendental_Osin(c_Transcendental_Opi),c_Transcendental_Osin(X0),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X0,c_Transcendental_Opi,tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal))),
% 0.09/0.49 inference(forward_demodulation,[status(thm)],[f3086,f3070])).
% 0.09/0.49 fof(f3405,plain,(
% 0.09/0.49 ![X0]: (c_HOL_Oord__class_Oless(c_Transcendental_Osin(c_Transcendental_Opi),c_Transcendental_Osin(X0),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X0,c_Transcendental_Opi,tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_Transcendental_Osin(c_Transcendental_Opi),X0,tc_RealDef_Oreal))),
% 0.09/0.49 inference(forward_demodulation,[status(thm)],[f3086,f3404])).
% 0.09/0.49 fof(f3406,plain,(
% 0.09/0.49 c_HOL_Oord__class_Oless(c_Transcendental_Osin(c_Transcendental_Opi),c_Transcendental_Osin(c_HOL_Ominus__class_Ominus(v_x,c_Transcendental_Opi,tc_RealDef_Oreal)),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_HOL_Ominus__class_Ominus(v_x,c_Transcendental_Opi,tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal)),
% 0.09/0.49 inference(resolution,[status(thm)],[f3405,f3301])).
% 0.09/0.49 fof(f3409,definition,(
% 0.09/0.49 sQ13_spl <=> (c_HOL_Oord__class_Oless(c_Transcendental_Osin(c_Transcendental_Opi),c_Transcendental_Osin(c_HOL_Ominus__class_Ominus(v_x,c_Transcendental_Opi,tc_RealDef_Oreal)),tc_RealDef_Oreal))),
% 0.09/0.49 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.09/0.49 fof(f3410,plain,(
% 0.09/0.49 c_HOL_Oord__class_Oless(c_Transcendental_Osin(c_Transcendental_Opi),c_Transcendental_Osin(c_HOL_Ominus__class_Ominus(v_x,c_Transcendental_Opi,tc_RealDef_Oreal)),tc_RealDef_Oreal)|~sQ13_spl),
% 0.09/0.49 inference(component_clause,[status(thm)],[f3409])).
% 0.09/0.49 fof(f3412,definition,(
% 0.09/0.49 sQ14_spl <=> (c_HOL_Oord__class_Oless(c_HOL_Ominus__class_Ominus(v_x,c_Transcendental_Opi,tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal))),
% 0.09/0.49 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.09/0.49 fof(f3414,plain,(
% 0.09/0.49 ~c_HOL_Oord__class_Oless(c_HOL_Ominus__class_Ominus(v_x,c_Transcendental_Opi,tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal)|sQ14_spl),
% 0.09/0.49 inference(component_clause,[status(thm)],[f3412])).
% 0.09/0.49 fof(f3415,plain,(
% 0.09/0.49 sQ13_spl|~sQ14_spl),
% 0.09/0.49 inference(split_clause,[status(thm)],[f3406,f3409,f3412])).
% 0.09/0.49 fof(f3427,plain,(
% 0.09/0.49 c_HOL_Oord__class_Oless(c_Transcendental_Osin(c_Transcendental_Opi),c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(v_x,tc_RealDef_Oreal)),tc_RealDef_Oreal)|~sQ13_spl),
% 0.09/0.49 inference(forward_demodulation,[status(thm)],[f3293,f3410])).
% 0.09/0.49 fof(f3428,plain,(
% 0.09/0.49 c_HOL_Oord__class_Oless(c_Transcendental_Osin(c_Transcendental_Opi),c_Transcendental_Osin(c_Transcendental_Opi),tc_RealDef_Oreal)|~sQ13_spl),
% 0.09/0.49 inference(forward_demodulation,[status(thm)],[f3292,f3427])).
% 0.09/0.49 fof(f3455,plain,(
% 0.09/0.49 c_HOL_Oord__class_Oless(c_Transcendental_Osin(c_Transcendental_Opi),c_Transcendental_Osin(c_Transcendental_Osin(c_Transcendental_Opi)),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_Transcendental_Osin(c_Transcendental_Opi),c_Transcendental_Opi,tc_RealDef_Oreal)|~sQ13_spl),
% 0.09/0.49 inference(resolution,[status(thm)],[f3428,f3405])).
% 0.09/0.49 fof(f3456,definition,(
% 0.09/0.49 sQ24_spl <=> (c_HOL_Oord__class_Oless(c_Transcendental_Osin(c_Transcendental_Opi),c_Transcendental_Osin(c_Transcendental_Osin(c_Transcendental_Opi)),tc_RealDef_Oreal))),
% 0.09/0.49 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.09/0.49 fof(f3457,plain,(
% 0.09/0.49 c_HOL_Oord__class_Oless(c_Transcendental_Osin(c_Transcendental_Opi),c_Transcendental_Osin(c_Transcendental_Osin(c_Transcendental_Opi)),tc_RealDef_Oreal)|~sQ24_spl),
% 0.09/0.49 inference(component_clause,[status(thm)],[f3456])).
% 0.09/0.49 fof(f3459,definition,(
% 0.09/0.49 sQ25_spl <=> (c_HOL_Oord__class_Oless(c_Transcendental_Osin(c_Transcendental_Opi),c_Transcendental_Opi,tc_RealDef_Oreal))),
% 0.09/0.49 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.09/0.49 fof(f3461,plain,(
% 0.09/0.49 ~c_HOL_Oord__class_Oless(c_Transcendental_Osin(c_Transcendental_Opi),c_Transcendental_Opi,tc_RealDef_Oreal)|sQ25_spl),
% 0.09/0.49 inference(component_clause,[status(thm)],[f3459])).
% 0.09/0.49 fof(f3462,plain,(
% 0.09/0.49 sQ24_spl|~sQ25_spl|~sQ13_spl),
% 0.09/0.49 inference(split_clause,[status(thm)],[f3455,f3456,f3459,f3409])).
% 0.09/0.49 fof(f3463,plain,(
% 0.09/0.49 $false|sQ14_spl),
% 0.09/0.49 inference(forward_subsumption_resolution,[status(thm)],[f3414,f3097])).
% 0.09/0.49 fof(f3464,plain,(
% 0.09/0.49 sQ14_spl),
% 0.09/0.49 inference(contradiction_clause,[status(thm)],[f3463])).
% 0.09/0.49 fof(f3465,plain,(
% 0.09/0.49 c_HOL_Oord__class_Oless(c_Transcendental_Osin(c_Transcendental_Opi),c_Transcendental_Osin(c_Transcendental_Opi),tc_RealDef_Oreal)|~sQ24_spl),
% 0.09/0.49 inference(forward_demodulation,[status(thm)],[f3245,f3457])).
% 0.09/0.49 fof(f3560,plain,(
% 0.09/0.49 c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(v_x,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal))=c_Transcendental_Osin(c_HOL_Ominus__class_Ominus(c_Transcendental_Opi,c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(c_Transcendental_Opi,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 0.09/0.49 inference(backward_demodulation,[status(thm)],[f3281,f3340])).
% 0.09/0.49 fof(f3592,plain,(
% 0.09/0.49 c_Transcendental_Osin(c_HOL_Ominus__class_Ominus(c_Transcendental_Opi,c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(v_x,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal))=c_Transcendental_Osin(c_HOL_Ominus__class_Ominus(c_Transcendental_Opi,c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(c_Transcendental_Opi,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 0.09/0.49 inference(forward_demodulation,[status(thm)],[f3281,f3560])).
% 0.09/0.49 fof(f3593,plain,(
% 0.09/0.49 c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(c_Transcendental_Opi,c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(v_x,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal))=c_Transcendental_Osin(c_HOL_Ominus__class_Ominus(c_Transcendental_Opi,c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(c_Transcendental_Opi,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 0.09/0.49 inference(forward_demodulation,[status(thm)],[f3306,f3592])).
% 0.09/0.49 fof(f3594,plain,(
% 0.09/0.49 c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(v_x,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal))=c_Transcendental_Osin(c_HOL_Ominus__class_Ominus(c_Transcendental_Opi,c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(c_Transcendental_Opi,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 0.09/0.49 inference(forward_demodulation,[status(thm)],[f3280,f3593])).
% 0.09/0.49 fof(f3595,plain,(
% 0.09/0.49 c_Transcendental_Osin(c_HOL_Ominus__class_Ominus(c_Transcendental_Opi,c_HOL_Ouminus__class_Ouminus(v_x,tc_RealDef_Oreal),tc_RealDef_Oreal))=c_Transcendental_Osin(c_HOL_Ominus__class_Ominus(c_Transcendental_Opi,c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(c_Transcendental_Opi,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 0.09/0.49 inference(forward_demodulation,[status(thm)],[f3281,f3594])).
% 0.09/0.49 fof(f3596,plain,(
% 0.09/0.49 c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(c_Transcendental_Opi,v_x,tc_RealDef_Oreal))=c_Transcendental_Osin(c_HOL_Ominus__class_Ominus(c_Transcendental_Opi,c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(c_Transcendental_Opi,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 0.09/0.49 inference(forward_demodulation,[status(thm)],[f3306,f3595])).
% 0.09/0.49 fof(f3597,plain,(
% 0.09/0.49 c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(v_x,tc_RealDef_Oreal))=c_Transcendental_Osin(c_HOL_Ominus__class_Ominus(c_Transcendental_Opi,c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(c_Transcendental_Opi,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 0.09/0.49 inference(forward_demodulation,[status(thm)],[f3280,f3596])).
% 0.09/0.49 fof(f3598,plain,(
% 0.09/0.49 c_Transcendental_Osin(c_Transcendental_Opi)=c_Transcendental_Osin(c_HOL_Ominus__class_Ominus(c_Transcendental_Opi,c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(c_Transcendental_Opi,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 0.09/0.49 inference(forward_demodulation,[status(thm)],[f3292,f3597])).
% 0.09/0.49 fof(f3599,plain,(
% 0.09/0.49 c_Transcendental_Osin(c_Transcendental_Opi)=c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(c_Transcendental_Opi,c_HOL_Ouminus__class_Ouminus(c_Transcendental_Opi,tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 0.09/0.49 inference(forward_demodulation,[status(thm)],[f3306,f3598])).
% 0.09/0.49 fof(f3600,plain,(
% 0.09/0.49 c_Transcendental_Osin(c_Transcendental_Opi)=c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(c_Transcendental_Opi,tc_RealDef_Oreal),tc_RealDef_Oreal))),
% 0.09/0.49 inference(forward_demodulation,[status(thm)],[f3280,f3599])).
% 0.09/0.49 fof(f3601,plain,(
% 0.09/0.49 c_Transcendental_Osin(c_Transcendental_Opi)=c_Transcendental_Osin(c_HOL_Ominus__class_Ominus(c_Transcendental_Opi,c_Transcendental_Opi,tc_RealDef_Oreal))),
% 0.09/0.49 inference(forward_demodulation,[status(thm)],[f3281,f3600])).
% 0.09/0.49 fof(f3602,plain,(
% 0.09/0.49 c_Transcendental_Osin(c_Transcendental_Opi)=c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(c_Transcendental_Opi,tc_RealDef_Oreal))),
% 0.09/0.49 inference(forward_demodulation,[status(thm)],[f3293,f3601])).
% 0.09/0.49 fof(f3603,plain,(
% 0.09/0.49 c_Transcendental_Osin(c_Transcendental_Opi)=c_Transcendental_Osin(v_x)),
% 0.09/0.49 inference(forward_demodulation,[status(thm)],[f3355,f3602])).
% 0.09/0.49 fof(f3625,plain,(
% 0.09/0.49 c_HOL_Oord__class_Oless(c_Transcendental_Osin(c_Transcendental_Opi),c_Transcendental_Osin(v_x),tc_RealDef_Oreal)|~sQ24_spl),
% 0.09/0.50 inference(backward_demodulation,[status(thm)],[f3603,f3465])).
% 0.09/0.50 fof(f3626,plain,(
% 0.09/0.50 ![X0]: (c_HOL_Oord__class_Oless(c_Transcendental_Osin(c_Transcendental_Opi),c_Transcendental_Osin(X0),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X0,c_Transcendental_Opi,tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_Transcendental_Osin(v_x),X0,tc_RealDef_Oreal))),
% 0.09/0.50 inference(backward_demodulation,[status(thm)],[f3603,f3405])).
% 0.09/0.50 fof(f3638,plain,(
% 0.09/0.50 c_HOL_Oord__class_Oless(c_Transcendental_Osin(v_x),c_Transcendental_Opi,tc_RealDef_Oreal)),
% 0.09/0.50 inference(backward_demodulation,[status(thm)],[f3603,f3240])).
% 0.09/0.50 fof(f3646,plain,(
% 0.09/0.50 c_HOL_Oord__class_Oless(c_Transcendental_Osin(v_x),c_Transcendental_Osin(v_x),tc_RealDef_Oreal)|~sQ24_spl),
% 0.09/0.50 inference(forward_demodulation,[status(thm)],[f3603,f3625])).
% 0.09/0.50 fof(f3647,plain,(
% 0.09/0.50 ![X0]: (c_HOL_Oord__class_Oless(c_Transcendental_Osin(v_x),c_Transcendental_Osin(X0),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(X0,c_Transcendental_Opi,tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_Transcendental_Osin(v_x),X0,tc_RealDef_Oreal))),
% 0.09/0.50 inference(forward_demodulation,[status(thm)],[f3603,f3626])).
% 0.09/0.50 fof(f3722,plain,(
% 0.09/0.50 c_HOL_Oord__class_Oless(c_Transcendental_Osin(v_x),c_Transcendental_Osin(c_Transcendental_Osin(v_x)),tc_RealDef_Oreal)|~c_HOL_Oord__class_Oless(c_Transcendental_Osin(v_x),c_Transcendental_Opi,tc_RealDef_Oreal)|~sQ24_spl),
% 0.09/0.50 inference(resolution,[status(thm)],[f3647,f3646])).
% 0.09/0.50 fof(f3725,definition,(
% 0.09/0.50 sQ42_spl <=> (c_HOL_Oord__class_Oless(c_Transcendental_Osin(v_x),c_Transcendental_Osin(c_Transcendental_Osin(v_x)),tc_RealDef_Oreal))),
% 0.09/0.50 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 0.09/0.50 fof(f3726,plain,(
% 0.09/0.50 c_HOL_Oord__class_Oless(c_Transcendental_Osin(v_x),c_Transcendental_Osin(c_Transcendental_Osin(v_x)),tc_RealDef_Oreal)|~sQ42_spl),
% 0.09/0.50 inference(component_clause,[status(thm)],[f3725])).
% 0.09/0.50 fof(f3728,definition,(
% 0.09/0.50 sQ43_spl <=> (c_HOL_Oord__class_Oless(c_Transcendental_Osin(v_x),c_Transcendental_Opi,tc_RealDef_Oreal))),
% 0.09/0.50 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 0.09/0.50 fof(f3730,plain,(
% 0.09/0.50 ~c_HOL_Oord__class_Oless(c_Transcendental_Osin(v_x),c_Transcendental_Opi,tc_RealDef_Oreal)|sQ43_spl),
% 0.09/0.50 inference(component_clause,[status(thm)],[f3728])).
% 0.09/0.50 fof(f3731,plain,(
% 0.09/0.50 sQ42_spl|~sQ43_spl|~sQ24_spl),
% 0.09/0.50 inference(split_clause,[status(thm)],[f3722,f3725,f3728,f3456])).
% 0.09/0.50 fof(f3740,plain,(
% 0.09/0.50 ~c_HOL_Oord__class_Oless(c_Transcendental_Osin(v_x),c_Transcendental_Opi,tc_RealDef_Oreal)|sQ25_spl),
% 0.09/0.50 inference(forward_demodulation,[status(thm)],[f3603,f3461])).
% 0.09/0.50 fof(f3741,plain,(
% 0.09/0.50 $false|sQ25_spl),
% 0.09/0.50 inference(forward_subsumption_resolution,[status(thm)],[f3740,f3638])).
% 0.09/0.50 fof(f3742,plain,(
% 0.09/0.50 sQ25_spl),
% 0.09/0.50 inference(contradiction_clause,[status(thm)],[f3741])).
% 0.09/0.50 fof(f3744,plain,(
% 0.09/0.50 $false|sQ43_spl),
% 0.09/0.50 inference(forward_subsumption_resolution,[status(thm)],[f3730,f3638])).
% 0.09/0.50 fof(f3745,plain,(
% 0.09/0.50 sQ43_spl),
% 0.09/0.50 inference(contradiction_clause,[status(thm)],[f3744])).
% 0.09/0.50 fof(f3746,plain,(
% 0.09/0.50 c_HOL_Oord__class_Oless(c_Transcendental_Osin(v_x),c_Transcendental_Osin(v_x),tc_RealDef_Oreal)|~sQ42_spl),
% 0.09/0.50 inference(forward_demodulation,[status(thm)],[f3391,f3726])).
% 0.09/0.50 fof(f3947,plain,(
% 0.09/0.50 $false|~sQ42_spl),
% 0.09/0.50 inference(backward_subsumption_resolution,[status(thm)],[f3746,f2598])).
% 0.09/0.50 fof(f3948,plain,(
% 0.09/0.50 ~sQ42_spl),
% 0.09/0.50 inference(contradiction_clause,[status(thm)],[f3947])).
% 0.09/0.50 fof(f3949,plain,(
% 0.09/0.50 $false),
% 0.09/0.50 inference(sat_refutation,[status(thm)],[f3415,f3462,f3464,f3731,f3742,f3745,f3948])).
% 0.09/0.50 % SZS output end CNFRefutation for theBenchmark.p
% 0.20/0.53 % Elapsed time: 0.154600 seconds
% 0.20/0.53 % CPU time: 0.339580 seconds
% 0.20/0.53 % Total memory used: 96.082 MB
% 0.20/0.53 % Net memory used: 95.607 MB
%------------------------------------------------------------------------------