%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV596-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:49:12 PM UTC 2026
% Result : Unsatisfiable 0.27s 0.60s
% Output : CNFRefutation 0.27s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 20
% Syntax : Number of formulae : 109 ( 74 unt; 6 def)
% Number of atoms : 154 ( 58 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 84 ( 39 ~; 39 |; 0 &)
% ( 6 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 2 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 9 ( 7 usr; 7 prp; 0-3 aty)
% Number of functors : 8 ( 8 usr; 3 con; 0-3 aty)
% Number of variables : 33 ( 33 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f370,axiom,
! [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),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f820,axiom,
! [V_x] : ~ c_HOL_Oord__class_Oless(V_x,V_x,tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1089,axiom,
! [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),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1090,axiom,
! [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),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1092,axiom,
! [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),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1096,axiom,
! [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),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1113,axiom,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1128,axiom,
! [V_x] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),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),c_Transcendental_Osin(V_x),tc_RealDef_Oreal) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1130,axiom,
! [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),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1133,axiom,
c_Transcendental_Osin(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1139,axiom,
c_Transcendental_Osin(c_Transcendental_Opi) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1145,axiom,
c_HOL_Oord__class_Oless(c_HOL_Ominus__class_Ominus(v_x,c_Transcendental_Opi,tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1146,axiom,
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),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1147,negated_conjecture,
c_Transcendental_Osin(c_HOL_Ominus__class_Ominus(v_x,c_Transcendental_Opi,tc_RealDef_Oreal)) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1867,plain,
! [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),
inference(cnf_transformation,[status(thm)],[f370]) ).
fof(f2598,plain,
! [X0] : ~ c_HOL_Oord__class_Oless(X0,X0,tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f820]) ).
fof(f3021,plain,
! [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),
inference(cnf_transformation,[status(thm)],[f1089]) ).
fof(f3022,plain,
! [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),
inference(cnf_transformation,[status(thm)],[f1090]) ).
fof(f3024,plain,
! [X0,X1] : X0 = c_HOL_Oplus__class_Oplus(c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal),X1,tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f1092]) ).
fof(f3028,plain,
! [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),
inference(cnf_transformation,[status(thm)],[f1096]) ).
fof(f3050,plain,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f1113]) ).
fof(f3070,plain,
! [X0] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),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),c_Transcendental_Osin(X0),tc_RealDef_Oreal) ),
inference(cnf_transformation,[status(thm)],[f1128]) ).
fof(f3072,plain,
! [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),
inference(cnf_transformation,[status(thm)],[f1130]) ).
fof(f3075,plain,
c_Transcendental_Osin(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f1133]) ).
fof(f3086,plain,
c_Transcendental_Osin(c_Transcendental_Opi) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f1139]) ).
fof(f3097,plain,
c_HOL_Oord__class_Oless(c_HOL_Ominus__class_Ominus(v_x,c_Transcendental_Opi,tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f1145]) ).
fof(f3098,plain,
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),
inference(cnf_transformation,[status(thm)],[f1146]) ).
fof(f3099,plain,
c_Transcendental_Osin(c_HOL_Ominus__class_Ominus(v_x,c_Transcendental_Opi,tc_RealDef_Oreal)) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f1147]) ).
fof(f3238,plain,
c_Transcendental_Osin(c_HOL_Ominus__class_Ominus(v_x,c_Transcendental_Opi,tc_RealDef_Oreal)) = c_Transcendental_Osin(c_Transcendental_Opi),
inference(backward_demodulation,[status(thm)],[f3086,f3099]) ).
fof(f3240,plain,
c_HOL_Oord__class_Oless(c_Transcendental_Osin(c_Transcendental_Opi),c_Transcendental_Opi,tc_RealDef_Oreal),
inference(forward_demodulation,[status(thm)],[f3086,f3050]) ).
fof(f3244,plain,
c_Transcendental_Osin(c_Transcendental_Osin(c_Transcendental_Opi)) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(forward_demodulation,[status(thm)],[f3086,f3075]) ).
fof(f3245,plain,
c_Transcendental_Osin(c_Transcendental_Osin(c_Transcendental_Opi)) = c_Transcendental_Osin(c_Transcendental_Opi),
inference(forward_demodulation,[status(thm)],[f3086,f3244]) ).
fof(f3262,plain,
! [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),
inference(paramodulation,[status(thm)],[f1867,f3024]) ).
fof(f3267,plain,
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),
inference(paramodulation,[status(thm)],[f3245,f3028]) ).
fof(f3268,plain,
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),
inference(paramodulation,[status(thm)],[f3238,f3028]) ).
fof(f3270,plain,
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),
inference(forward_demodulation,[status(thm)],[f3028,f3267]) ).
fof(f3271,plain,
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)),
inference(forward_demodulation,[status(thm)],[f3028,f3270]) ).
fof(f3272,plain,
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)),
inference(forward_demodulation,[status(thm)],[f3028,f3268]) ).
fof(f3280,plain,
! [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)),
inference(forward_demodulation,[status(thm)],[f3028,f3021]) ).
fof(f3281,plain,
! [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)),
inference(paramodulation,[status(thm)],[f1867,f3280]) ).
fof(f3285,plain,
! [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)),
inference(forward_demodulation,[status(thm)],[f3028,f3022]) ).
fof(f3287,plain,
! [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)),
inference(paramodulation,[status(thm)],[f3024,f3285]) ).
fof(f3292,plain,
c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(v_x,tc_RealDef_Oreal)) = c_Transcendental_Osin(c_Transcendental_Opi),
inference(backward_demodulation,[status(thm)],[f3293,f3238]) ).
fof(f3293,plain,
! [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)),
inference(forward_demodulation,[status(thm)],[f3028,f3072]) ).
fof(f3298,plain,
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),
inference(paramodulation,[status(thm)],[f3292,f3028]) ).
fof(f3300,plain,
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)),
inference(forward_demodulation,[status(thm)],[f3028,f3298]) ).
fof(f3301,plain,
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),
inference(forward_demodulation,[status(thm)],[f3086,f3098]) ).
fof(f3306,plain,
! [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),
inference(paramodulation,[status(thm)],[f3262,f3024]) ).
fof(f3332,plain,
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),
inference(paramodulation,[status(thm)],[f3300,f3028]) ).
fof(f3334,plain,
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)),
inference(forward_demodulation,[status(thm)],[f3028,f3332]) ).
fof(f3335,plain,
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),
inference(paramodulation,[status(thm)],[f3334,f3028]) ).
fof(f3337,plain,
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)),
inference(forward_demodulation,[status(thm)],[f3028,f3335]) ).
fof(f3338,plain,
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),
inference(paramodulation,[status(thm)],[f3337,f3028]) ).
fof(f3340,plain,
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)),
inference(forward_demodulation,[status(thm)],[f3028,f3338]) ).
fof(f3355,plain,
c_Transcendental_Osin(v_x) = c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(c_Transcendental_Opi,tc_RealDef_Oreal)),
inference(backward_demodulation,[status(thm)],[f3287,f3272]) ).
fof(f3390,plain,
c_Transcendental_Osin(c_Transcendental_Osin(v_x)) = c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(c_Transcendental_Opi,tc_RealDef_Oreal)),
inference(forward_demodulation,[status(thm)],[f3355,f3271]) ).
fof(f3391,plain,
c_Transcendental_Osin(c_Transcendental_Osin(v_x)) = c_Transcendental_Osin(v_x),
inference(forward_demodulation,[status(thm)],[f3355,f3390]) ).
fof(f3404,plain,
! [X0] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),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),c_Transcendental_Osin(X0),tc_RealDef_Oreal) ),
inference(forward_demodulation,[status(thm)],[f3086,f3070]) ).
fof(f3405,plain,
! [X0] :
( ~ c_HOL_Oord__class_Oless(c_Transcendental_Osin(c_Transcendental_Opi),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),c_Transcendental_Osin(X0),tc_RealDef_Oreal) ),
inference(forward_demodulation,[status(thm)],[f3086,f3404]) ).
fof(f3406,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ominus__class_Ominus(v_x,c_Transcendental_Opi,tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal)
| 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) ),
inference(resolution,[status(thm)],[f3405,f3301]) ).
fof(f3409,definition,
( 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) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f3410,plain,
( ~ 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) ),
inference(component_clause,[status(thm)],[f3409]) ).
fof(f3412,definition,
( 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) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f3414,plain,
( 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) ),
inference(component_clause,[status(thm)],[f3412]) ).
fof(f3415,plain,
( ~ sQ14_spl
| sQ13_spl ),
inference(split_clause,[status(thm)],[f3406,f3409,f3412]) ).
fof(f3427,plain,
( ~ sQ13_spl
| 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) ),
inference(forward_demodulation,[status(thm)],[f3293,f3410]) ).
fof(f3428,plain,
( ~ sQ13_spl
| c_HOL_Oord__class_Oless(c_Transcendental_Osin(c_Transcendental_Opi),c_Transcendental_Osin(c_Transcendental_Opi),tc_RealDef_Oreal) ),
inference(forward_demodulation,[status(thm)],[f3292,f3427]) ).
fof(f3455,plain,
( ~ sQ13_spl
| ~ c_HOL_Oord__class_Oless(c_Transcendental_Osin(c_Transcendental_Opi),c_Transcendental_Opi,tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(c_Transcendental_Osin(c_Transcendental_Opi),c_Transcendental_Osin(c_Transcendental_Osin(c_Transcendental_Opi)),tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f3428,f3405]) ).
fof(f3456,definition,
( 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) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f3457,plain,
( ~ 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) ),
inference(component_clause,[status(thm)],[f3456]) ).
fof(f3459,definition,
( sQ25_spl
<=> c_HOL_Oord__class_Oless(c_Transcendental_Osin(c_Transcendental_Opi),c_Transcendental_Opi,tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f3461,plain,
( sQ25_spl
| ~ c_HOL_Oord__class_Oless(c_Transcendental_Osin(c_Transcendental_Opi),c_Transcendental_Opi,tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f3459]) ).
fof(f3462,plain,
( ~ sQ13_spl
| ~ sQ25_spl
| sQ24_spl ),
inference(split_clause,[status(thm)],[f3455,f3456,f3459,f3409]) ).
fof(f3463,plain,
( sQ14_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3414,f3097]) ).
fof(f3464,plain,
sQ14_spl,
inference(contradiction_clause,[status(thm)],[f3463]) ).
fof(f3465,plain,
( ~ sQ24_spl
| c_HOL_Oord__class_Oless(c_Transcendental_Osin(c_Transcendental_Opi),c_Transcendental_Osin(c_Transcendental_Opi),tc_RealDef_Oreal) ),
inference(forward_demodulation,[status(thm)],[f3245,f3457]) ).
fof(f3560,plain,
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)),
inference(backward_demodulation,[status(thm)],[f3281,f3340]) ).
fof(f3592,plain,
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)),
inference(forward_demodulation,[status(thm)],[f3281,f3560]) ).
fof(f3593,plain,
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)),
inference(forward_demodulation,[status(thm)],[f3306,f3592]) ).
fof(f3594,plain,
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)),
inference(forward_demodulation,[status(thm)],[f3280,f3593]) ).
fof(f3595,plain,
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)),
inference(forward_demodulation,[status(thm)],[f3281,f3594]) ).
fof(f3596,plain,
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)),
inference(forward_demodulation,[status(thm)],[f3306,f3595]) ).
fof(f3597,plain,
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)),
inference(forward_demodulation,[status(thm)],[f3280,f3596]) ).
fof(f3598,plain,
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)),
inference(forward_demodulation,[status(thm)],[f3292,f3597]) ).
fof(f3599,plain,
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)),
inference(forward_demodulation,[status(thm)],[f3306,f3598]) ).
fof(f3600,plain,
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)),
inference(forward_demodulation,[status(thm)],[f3280,f3599]) ).
fof(f3601,plain,
c_Transcendental_Osin(c_Transcendental_Opi) = c_Transcendental_Osin(c_HOL_Ominus__class_Ominus(c_Transcendental_Opi,c_Transcendental_Opi,tc_RealDef_Oreal)),
inference(forward_demodulation,[status(thm)],[f3281,f3600]) ).
fof(f3602,plain,
c_Transcendental_Osin(c_Transcendental_Opi) = c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(c_Transcendental_Opi,tc_RealDef_Oreal)),
inference(forward_demodulation,[status(thm)],[f3293,f3601]) ).
fof(f3603,plain,
c_Transcendental_Osin(c_Transcendental_Opi) = c_Transcendental_Osin(v_x),
inference(forward_demodulation,[status(thm)],[f3355,f3602]) ).
fof(f3625,plain,
( ~ sQ24_spl
| c_HOL_Oord__class_Oless(c_Transcendental_Osin(c_Transcendental_Opi),c_Transcendental_Osin(v_x),tc_RealDef_Oreal) ),
inference(backward_demodulation,[status(thm)],[f3603,f3465]) ).
fof(f3626,plain,
! [X0] :
( ~ c_HOL_Oord__class_Oless(c_Transcendental_Osin(v_x),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),c_Transcendental_Osin(X0),tc_RealDef_Oreal) ),
inference(backward_demodulation,[status(thm)],[f3603,f3405]) ).
fof(f3638,plain,
c_HOL_Oord__class_Oless(c_Transcendental_Osin(v_x),c_Transcendental_Opi,tc_RealDef_Oreal),
inference(backward_demodulation,[status(thm)],[f3603,f3240]) ).
fof(f3646,plain,
( ~ sQ24_spl
| c_HOL_Oord__class_Oless(c_Transcendental_Osin(v_x),c_Transcendental_Osin(v_x),tc_RealDef_Oreal) ),
inference(forward_demodulation,[status(thm)],[f3603,f3625]) ).
fof(f3647,plain,
! [X0] :
( ~ c_HOL_Oord__class_Oless(c_Transcendental_Osin(v_x),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),c_Transcendental_Osin(X0),tc_RealDef_Oreal) ),
inference(forward_demodulation,[status(thm)],[f3603,f3626]) ).
fof(f3722,plain,
( ~ sQ24_spl
| ~ c_HOL_Oord__class_Oless(c_Transcendental_Osin(v_x),c_Transcendental_Opi,tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(c_Transcendental_Osin(v_x),c_Transcendental_Osin(c_Transcendental_Osin(v_x)),tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f3647,f3646]) ).
fof(f3725,definition,
( sQ42_spl
<=> c_HOL_Oord__class_Oless(c_Transcendental_Osin(v_x),c_Transcendental_Osin(c_Transcendental_Osin(v_x)),tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f3726,plain,
( ~ sQ42_spl
| c_HOL_Oord__class_Oless(c_Transcendental_Osin(v_x),c_Transcendental_Osin(c_Transcendental_Osin(v_x)),tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f3725]) ).
fof(f3728,definition,
( sQ43_spl
<=> c_HOL_Oord__class_Oless(c_Transcendental_Osin(v_x),c_Transcendental_Opi,tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f3730,plain,
( sQ43_spl
| ~ c_HOL_Oord__class_Oless(c_Transcendental_Osin(v_x),c_Transcendental_Opi,tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f3728]) ).
fof(f3731,plain,
( ~ sQ24_spl
| ~ sQ43_spl
| sQ42_spl ),
inference(split_clause,[status(thm)],[f3722,f3725,f3728,f3456]) ).
fof(f3740,plain,
( sQ25_spl
| ~ c_HOL_Oord__class_Oless(c_Transcendental_Osin(v_x),c_Transcendental_Opi,tc_RealDef_Oreal) ),
inference(forward_demodulation,[status(thm)],[f3603,f3461]) ).
fof(f3741,plain,
( sQ25_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3740,f3638]) ).
fof(f3742,plain,
sQ25_spl,
inference(contradiction_clause,[status(thm)],[f3741]) ).
fof(f3744,plain,
( sQ43_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3730,f3638]) ).
fof(f3745,plain,
sQ43_spl,
inference(contradiction_clause,[status(thm)],[f3744]) ).
fof(f3746,plain,
( ~ sQ42_spl
| c_HOL_Oord__class_Oless(c_Transcendental_Osin(v_x),c_Transcendental_Osin(v_x),tc_RealDef_Oreal) ),
inference(forward_demodulation,[status(thm)],[f3391,f3726]) ).
fof(f3947,plain,
( ~ sQ42_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f3746,f2598]) ).
fof(f3948,plain,
~ sQ42_spl,
inference(contradiction_clause,[status(thm)],[f3947]) ).
fof(f3949,plain,
$false,
inference(sat_refutation,[status(thm)],[f3415,f3462,f3464,f3731,f3742,f3745,f3948]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV596-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n011.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:13:11 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.14/0.50 % Drodi V4.1.1
% 0.27/0.60 % Refutation found
% 0.27/0.60 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.27/0.60 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.27/0.64 % Elapsed time: 0.272629 seconds
% 0.27/0.64 % CPU time: 0.982236 seconds
% 0.27/0.64 % Total memory used: 173.166 MB
% 0.27/0.64 % Net memory used: 172.559 MB
%------------------------------------------------------------------------------