%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV601-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 : 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:49:12 PM UTC 2026
% Result : Unsatisfiable 1.46s 0.68s
% Output : CNFRefutation 1.46s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 18
% Syntax : Number of formulae : 81 ( 64 unt; 0 def)
% Number of atoms : 98 ( 84 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 39 ( 22 ~; 17 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 2 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 20 ( 20 usr; 6 con; 0-3 aty)
% Number of variables : 62 ( 62 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f330,axiom,
! [V_x] : c_Transcendental_Ocos(c_Transcendental_Oarctan(V_x)) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f394,axiom,
c_Transcendental_Oarctan(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f476,axiom,
! [V_x,V_z] : V_x = c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(V_x,V_z,tc_RealDef_Oreal),V_z,tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f518,axiom,
! [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),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f566,axiom,
! [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),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f602,axiom,
! [T_a,V_a] :
( c_HOL_Oplus__class_Oplus(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) = V_a
| ~ class_OrderedGroup_Omonoid__add(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f603,axiom,
! [T_a,V_a] :
( c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(T_a),V_a,T_a) = V_a
| ~ class_OrderedGroup_Omonoid__add(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f729,axiom,
! [V_a,V_b] :
( V_b = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)
| c_Complex_Ocomplex_OComplex(V_a,V_b) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f730,axiom,
! [V_a,V_b] :
( V_a = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)
| c_Complex_Ocomplex_OComplex(V_a,V_b) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f731,axiom,
c_Transcendental_Osin(c_Transcendental_Opi) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f739,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(f745,axiom,
! [V_z] : c_HOL_Otimes__class_Otimes(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),V_z,tc_RealDef_Oreal) = V_z,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f766,axiom,
! [T_a,V_a] :
( c_HOL_Ominus__class_Ominus(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) = V_a
| ~ class_OrderedGroup_Ogroup__add(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f776,axiom,
c_Transcendental_Ocos(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)) = c_HOL_Oone__class_Oone(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f868,axiom,
! [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),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f880,negated_conjecture,
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),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f991,axiom,
class_OrderedGroup_Omonoid__add(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f992,axiom,
class_OrderedGroup_Ogroup__add(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1546,plain,
! [X0] : c_Transcendental_Ocos(c_Transcendental_Oarctan(X0)) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f330]) ).
fof(f1626,plain,
c_Transcendental_Oarctan(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f394]) ).
fof(f1746,plain,
! [X0,X1] : X0 = c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(X0,X1,tc_RealDef_Oreal),X1,tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f476]) ).
fof(f1811,plain,
! [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),
inference(cnf_transformation,[status(thm)],[f518]) ).
fof(f1869,plain,
! [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),
inference(cnf_transformation,[status(thm)],[f566]) ).
fof(f1913,plain,
! [T_a] :
( ! [V_a] : c_HOL_Oplus__class_Oplus(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) = V_a
| ~ class_OrderedGroup_Omonoid__add(T_a) ),
inference(miniscoping,[status(thm)],[f602]) ).
fof(f1914,plain,
! [X0,X1] :
( c_HOL_Oplus__class_Oplus(X1,c_HOL_Ozero__class_Ozero(X0),X0) = X1
| ~ class_OrderedGroup_Omonoid__add(X0) ),
inference(cnf_transformation,[status(thm)],[f1913]) ).
fof(f1915,plain,
! [T_a] :
( ! [V_a] : c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(T_a),V_a,T_a) = V_a
| ~ class_OrderedGroup_Omonoid__add(T_a) ),
inference(miniscoping,[status(thm)],[f603]) ).
fof(f1916,plain,
! [X0,X1] :
( c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(X0),X1,X0) = X1
| ~ class_OrderedGroup_Omonoid__add(X0) ),
inference(cnf_transformation,[status(thm)],[f1915]) ).
fof(f2105,plain,
! [V_b] :
( V_b = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)
| ! [V_a] : c_Complex_Ocomplex_OComplex(V_a,V_b) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
inference(miniscoping,[status(thm)],[f729]) ).
fof(f2106,plain,
! [X0,X1] :
( X1 = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)
| c_Complex_Ocomplex_OComplex(X0,X1) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
inference(cnf_transformation,[status(thm)],[f2105]) ).
fof(f2107,plain,
! [V_a] :
( V_a = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)
| ! [V_b] : c_Complex_Ocomplex_OComplex(V_a,V_b) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
inference(miniscoping,[status(thm)],[f730]) ).
fof(f2108,plain,
! [X0,X1] :
( X0 = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)
| c_Complex_Ocomplex_OComplex(X0,X1) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
inference(cnf_transformation,[status(thm)],[f2107]) ).
fof(f2109,plain,
c_Transcendental_Osin(c_Transcendental_Opi) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f731]) ).
fof(f2120,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)],[f739]) ).
fof(f2126,plain,
! [X0] : c_HOL_Otimes__class_Otimes(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),X0,tc_RealDef_Oreal) = X0,
inference(cnf_transformation,[status(thm)],[f745]) ).
fof(f2167,plain,
! [T_a] :
( ! [V_a] : c_HOL_Ominus__class_Ominus(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) = V_a
| ~ class_OrderedGroup_Ogroup__add(T_a) ),
inference(miniscoping,[status(thm)],[f766]) ).
fof(f2168,plain,
! [X0,X1] :
( c_HOL_Ominus__class_Ominus(X1,c_HOL_Ozero__class_Ozero(X0),X0) = X1
| ~ class_OrderedGroup_Ogroup__add(X0) ),
inference(cnf_transformation,[status(thm)],[f2167]) ).
fof(f2182,plain,
c_Transcendental_Ocos(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)) = c_HOL_Oone__class_Oone(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f776]) ).
fof(f2335,plain,
! [X0,X1] : c_HOL_Otimes__class_Otimes(X0,X1,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(X1,X0,tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f868]) ).
fof(f2356,plain,
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),
inference(cnf_transformation,[status(thm)],[f880]) ).
fof(f2467,plain,
class_OrderedGroup_Omonoid__add(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f991]) ).
fof(f2468,plain,
class_OrderedGroup_Ogroup__add(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f992]) ).
fof(f2540,plain,
c_Transcendental_Osin(c_Transcendental_Osin(c_Transcendental_Opi)) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(forward_demodulation,[status(thm)],[f2109,f2120]) ).
fof(f2541,plain,
c_Transcendental_Osin(c_Transcendental_Osin(c_Transcendental_Opi)) = c_Transcendental_Osin(c_Transcendental_Opi),
inference(forward_demodulation,[status(thm)],[f2109,f2540]) ).
fof(f2542,plain,
c_Transcendental_Ocos(c_Transcendental_Osin(c_Transcendental_Opi)) = c_HOL_Oone__class_Oone(tc_RealDef_Oreal),
inference(forward_demodulation,[status(thm)],[f2109,f2182]) ).
fof(f2585,plain,
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),
inference(paramodulation,[status(thm)],[f2335,f2356]) ).
fof(f2586,plain,
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),
inference(paramodulation,[status(thm)],[f2335,f2356]) ).
fof(f2673,plain,
! [X0,X1] :
( X1 = c_Transcendental_Osin(c_Transcendental_Opi)
| c_Complex_Ocomplex_OComplex(X0,X1) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
inference(forward_demodulation,[status(thm)],[f2109,f2106]) ).
fof(f2674,plain,
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),
inference(resolution,[status(thm)],[f2673,f2586]) ).
fof(f2675,plain,
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_Transcendental_Osin(c_Transcendental_Opi),
inference(resolution,[status(thm)],[f2673,f2585]) ).
fof(f2689,plain,
! [X0,X1] :
( X0 = c_Transcendental_Osin(c_Transcendental_Opi)
| c_Complex_Ocomplex_OComplex(X0,X1) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
inference(forward_demodulation,[status(thm)],[f2109,f2108]) ).
fof(f2690,plain,
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),
inference(resolution,[status(thm)],[f2689,f2586]) ).
fof(f2691,plain,
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),
inference(resolution,[status(thm)],[f2689,f2585]) ).
fof(f3404,plain,
! [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_Transcendental_Opi),c_Transcendental_Ocos(X0),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(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(X0),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(paramodulation,[status(thm)],[f2674,f1811]) ).
fof(f3450,plain,
! [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_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),
inference(forward_demodulation,[status(thm)],[f2691,f3404]) ).
fof(f3799,plain,
! [X0] : c_Transcendental_Ocos(c_Transcendental_Oarctan(X0)) != c_Transcendental_Osin(c_Transcendental_Opi),
inference(forward_demodulation,[status(thm)],[f2109,f1546]) ).
fof(f3807,plain,
c_Transcendental_Oarctan(c_Transcendental_Osin(c_Transcendental_Opi)) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(forward_demodulation,[status(thm)],[f2109,f1626]) ).
fof(f3808,plain,
c_Transcendental_Oarctan(c_Transcendental_Osin(c_Transcendental_Opi)) = c_Transcendental_Osin(c_Transcendental_Opi),
inference(forward_demodulation,[status(thm)],[f2109,f3807]) ).
fof(f3809,plain,
c_Transcendental_Ocos(c_Transcendental_Osin(c_Transcendental_Opi)) != c_Transcendental_Osin(c_Transcendental_Opi),
inference(paramodulation,[status(thm)],[f3808,f3799]) ).
fof(f3811,plain,
c_HOL_Oone__class_Oone(tc_RealDef_Oreal) != c_Transcendental_Osin(c_Transcendental_Opi),
inference(forward_demodulation,[status(thm)],[f2542,f3809]) ).
fof(f3996,plain,
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_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_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_Oone__class_Oone(tc_RealDef_Oreal),
inference(paramodulation,[status(thm)],[f2690,f1869]) ).
fof(f4068,plain,
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_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_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_Oone__class_Oone(tc_RealDef_Oreal),
inference(forward_demodulation,[status(thm)],[f2690,f3996]) ).
fof(f4069,plain,
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_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_Oone__class_Oone(tc_RealDef_Oreal),
inference(forward_demodulation,[status(thm)],[f2675,f4068]) ).
fof(f4070,plain,
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),
inference(forward_demodulation,[status(thm)],[f2675,f4069]) ).
fof(f4320,plain,
! [X0] : c_HOL_Otimes__class_Otimes(X0,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal) = X0,
inference(paramodulation,[status(thm)],[f2335,f2126]) ).
fof(f4904,plain,
! [X0] : c_HOL_Oplus__class_Oplus(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) = X0,
inference(resolution,[status(thm)],[f1914,f2467]) ).
fof(f4907,plain,
! [X0] : c_HOL_Oplus__class_Oplus(X0,c_Transcendental_Osin(c_Transcendental_Opi),tc_RealDef_Oreal) = X0,
inference(forward_demodulation,[status(thm)],[f2109,f4904]) ).
fof(f5063,plain,
! [X0] : c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal) = X0,
inference(resolution,[status(thm)],[f1916,f2467]) ).
fof(f5066,plain,
! [X0] : c_HOL_Oplus__class_Oplus(c_Transcendental_Osin(c_Transcendental_Opi),X0,tc_RealDef_Oreal) = X0,
inference(forward_demodulation,[status(thm)],[f2109,f5063]) ).
fof(f5515,plain,
! [X0] : c_HOL_Ominus__class_Ominus(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) = X0,
inference(resolution,[status(thm)],[f2168,f2468]) ).
fof(f5517,plain,
! [X0] : c_HOL_Ominus__class_Ominus(X0,c_Transcendental_Osin(c_Transcendental_Opi),tc_RealDef_Oreal) = X0,
inference(forward_demodulation,[status(thm)],[f2109,f5515]) ).
fof(f5805,plain,
c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(c_Transcendental_Opi),c_Transcendental_Osin(c_Transcendental_Opi),tc_RealDef_Oreal) = c_HOL_Ominus__class_Ominus(c_HOL_Oone__class_Oone(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),
inference(paramodulation,[status(thm)],[f4070,f1746]) ).
fof(f6250,plain,
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_Osin(c_Transcendental_Opi),c_Transcendental_Ocos(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_Osin(c_Transcendental_Opi)),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(paramodulation,[status(thm)],[f4907,f3450]) ).
fof(f6302,plain,
c_Transcendental_Osin(c_Transcendental_Opi) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(c_Transcendental_Opi),c_Transcendental_Ocos(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_Osin(c_Transcendental_Opi)),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[status(thm)],[f2674,f6250]) ).
fof(f6303,plain,
c_Transcendental_Osin(c_Transcendental_Opi) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(c_Transcendental_Opi),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(c_Transcendental_Opi),c_Transcendental_Osin(c_Transcendental_Osin(c_Transcendental_Opi)),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[status(thm)],[f2542,f6302]) ).
fof(f6304,plain,
c_Transcendental_Osin(c_Transcendental_Opi) = c_HOL_Oplus__class_Oplus(c_Transcendental_Osin(c_Transcendental_Opi),c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(c_Transcendental_Opi),c_Transcendental_Osin(c_Transcendental_Osin(c_Transcendental_Opi)),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[status(thm)],[f4320,f6303]) ).
fof(f6305,plain,
c_Transcendental_Osin(c_Transcendental_Opi) = c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(c_Transcendental_Opi),c_Transcendental_Osin(c_Transcendental_Osin(c_Transcendental_Opi)),tc_RealDef_Oreal),
inference(forward_demodulation,[status(thm)],[f5066,f6304]) ).
fof(f6306,plain,
c_Transcendental_Osin(c_Transcendental_Opi) = c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(c_Transcendental_Opi),c_Transcendental_Osin(c_Transcendental_Opi),tc_RealDef_Oreal),
inference(forward_demodulation,[status(thm)],[f2541,f6305]) ).
fof(f6494,plain,
c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(c_Transcendental_Opi),c_Transcendental_Osin(c_Transcendental_Opi),tc_RealDef_Oreal) = c_HOL_Ominus__class_Ominus(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_Transcendental_Osin(c_Transcendental_Opi),tc_RealDef_Oreal),
inference(backward_demodulation,[status(thm)],[f6306,f5805]) ).
fof(f6506,plain,
c_Transcendental_Osin(c_Transcendental_Opi) = c_HOL_Ominus__class_Ominus(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_Transcendental_Osin(c_Transcendental_Opi),tc_RealDef_Oreal),
inference(forward_demodulation,[status(thm)],[f6306,f6494]) ).
fof(f6507,plain,
c_Transcendental_Osin(c_Transcendental_Opi) = c_HOL_Oone__class_Oone(tc_RealDef_Oreal),
inference(forward_demodulation,[status(thm)],[f5517,f6506]) ).
fof(f6508,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f6507,f3811]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV601-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.35 % Computer : n003.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 21 09:14:46 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.12/0.46 % Drodi V4.1.1
% 1.46/0.68 % Refutation found
% 1.46/0.68 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 1.46/0.68 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 1.46/0.71 % Elapsed time: 0.352285 seconds
% 1.46/0.71 % CPU time: 1.844255 seconds
% 1.46/0.71 % Total memory used: 190.054 MB
% 1.46/0.71 % Net memory used: 189.033 MB
%------------------------------------------------------------------------------