%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SWV602-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 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 : Fri Sep 25 03:23:52 PM UTC 2026
% Result : Unsatisfiable 39.68s 6.46s
% Output : CNFRefutation 39.68s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 27
% Syntax : Number of formulae : 129 ( 91 unt; 0 def)
% Number of atoms : 173 ( 134 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 92 ( 48 ~; 44 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 18 ( 18 usr; 5 con; 0-3 aty)
% Number of variables : 150 ( 0 sgn 150 !; 0 ?; 100 :)
% Comments :
%------------------------------------------------------------------------------
fof(f96,axiom,
! [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),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_real__diff__def_0) ).
fof(f491,axiom,
! [X0,X1] : X0 = c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(X0,X1,tc_RealDef_Oreal),X1,tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_eq__diff__eq_H_1) ).
fof(f492,plain,
! [X0,X1] : c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(X0,X1,tc_RealDef_Oreal),X1,tc_RealDef_Oreal) = X0,
inference(reorient_equations,[],[f491]) ).
fof(f595,axiom,
! [X0,X1] :
( c_HOL_Oplus__class_Oplus(c_Int_Onumber__class_Onumber__of(c_Int_OPls,X0),X1,X0) = X1
| ~ class_Int_Onumber__ring(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_add__numeral__0_0) ).
fof(f607,axiom,
! [X0,X1] :
( X1 = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)
| c_HOL_Otimes__class_Otimes(X0,X0,tc_RealDef_Oreal) != c_HOL_Ouminus__class_Ouminus(c_HOL_Otimes__class_Otimes(X1,X1,tc_RealDef_Oreal),tc_RealDef_Oreal) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_real__sum__squares__cancel__a_1) ).
fof(f608,plain,
! [X0,X1] :
( c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = X1
| c_HOL_Otimes__class_Otimes(X0,X0,tc_RealDef_Oreal) != c_HOL_Ouminus__class_Ouminus(c_HOL_Otimes__class_Otimes(X1,X1,tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(reorient_equations,[],[f607]) ).
fof(f693,axiom,
! [X0] :
( c_HOL_Oone__class_Oone(X0) = c_Int_Onumber__class_Onumber__of(c_Int_OBit1(c_Int_OPls),X0)
| ~ class_Int_Onumber__ring(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_comp__arith_I110_J_0) ).
fof(f783,axiom,
c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) != c_HOL_Oone__class_Oone(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_real__zero__not__eq__one_0) ).
fof(f821,axiom,
! [X0] : c_Transcendental_Ocos(c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal)) = c_Transcendental_Ocos(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_cos__minus_0) ).
fof(f822,plain,
! [X0] : c_Transcendental_Ocos(X0) = c_Transcendental_Ocos(c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal)),
inference(reorient_equations,[],[f821]) ).
fof(f824,axiom,
! [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),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_sin__periodic__pi2_0) ).
fof(f825,plain,
! [X0] : c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(X0),tc_RealDef_Oreal) = c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(c_Transcendental_Opi,X0,tc_RealDef_Oreal)),
inference(reorient_equations,[],[f824]) ).
fof(f828,axiom,
! [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),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_sin__minus_0) ).
fof(f829,plain,
! [X0] : c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(X0),tc_RealDef_Oreal) = c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal)),
inference(reorient_equations,[],[f828]) ).
fof(f837,axiom,
! [X0,X1] : c_Transcendental_Osin(c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal)) = c_HOL_Ominus__class_Ominus(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),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_sin__diff_0) ).
fof(f901,axiom,
! [X0,X1] :
( c_HOL_Otimes__class_Otimes(X1,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),X0),X0) = c_HOL_Oplus__class_Oplus(X1,X1,X0)
| ~ class_Int_Onumber__ring(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_mult__2__right_0) ).
fof(f902,plain,
! [X0,X1] :
( c_HOL_Oplus__class_Oplus(X1,X1,X0) = c_HOL_Otimes__class_Otimes(X1,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),X0),X0)
| ~ class_Int_Onumber__ring(X0) ),
inference(reorient_equations,[],[f901]) ).
fof(f946,axiom,
! [X0] : c_Transcendental_Ocos(c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_RealDef_Oreal(X0,tc_nat),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal)) = c_HOL_Oone__class_Oone(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_cos__2npi_0) ).
fof(f947,plain,
! [X0] : c_HOL_Oone__class_Oone(tc_RealDef_Oreal) = c_Transcendental_Ocos(c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_RealDef_Oreal(X0,tc_nat),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal)),
inference(reorient_equations,[],[f946]) ).
fof(f949,axiom,
! [X0] : c_Transcendental_Ocos(X0) = c_Transcendental_Osin(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),X0,tc_RealDef_Oreal)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_cos__sin__eq_0) ).
fof(f961,axiom,
! [X0] :
( c_HOL_Ozero__class_Ozero(X0) = c_Int_Onumber__class_Onumber__of(c_Int_OPls,X0)
| ~ class_Int_Onumber__ring(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_comp__arith_I112_J_0) ).
fof(f1004,axiom,
! [X0,X1] :
( c_HOL_Ozero__class_Ozero(X0) = c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(X0),X1,X0),X1,X0)
| ~ class_Ring__and__Field_Odivision__by__zero(X0)
| ~ class_Ring__and__Field_Ofield(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_eq__divide__eq_4) ).
fof(f1049,axiom,
! [X2,X0,X1] : c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(X0,X1,tc_RealDef_Oreal),X2,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(X0,c_HOL_Otimes__class_Otimes(X1,X2,tc_RealDef_Oreal),tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_real__mult__assoc_0) ).
fof(f1100,axiom,
c_Transcendental_Osin(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_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_sin__two__pi_0) ).
fof(f1101,plain,
c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_Transcendental_Osin(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)),
inference(reorient_equations,[],[f1100]) ).
fof(f1103,axiom,
! [X0,X1] :
( c_HOL_Otimes__class_Otimes(X1,c_Int_Onumber__class_Onumber__of(c_Int_OBit1(c_Int_OPls),X0),X0) = X1
| ~ class_Int_Onumber__ring(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_mult__numeral__1__right_0) ).
fof(f1111,axiom,
! [X0,X1] : c_HOL_Otimes__class_Otimes(X0,X1,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(X1,X0,tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_real__mult__commute_0) ).
fof(f1114,axiom,
c_Transcendental_Osin(c_Transcendental_Opi) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_sin__pi_0) ).
fof(f1115,plain,
c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_Transcendental_Osin(c_Transcendental_Opi),
inference(reorient_equations,[],[f1114]) ).
fof(f1117,axiom,
! [X0,X1] :
( c_HOL_Oinverse__class_Odivide(c_HOL_Ozero__class_Ozero(X0),X1,X0) = c_HOL_Ozero__class_Ozero(X0)
| ~ class_Ring__and__Field_Ofield(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_divide__zero__left_0) ).
fof(f1118,plain,
! [X0,X1] :
( c_HOL_Ozero__class_Ozero(X0) = c_HOL_Oinverse__class_Odivide(c_HOL_Ozero__class_Ozero(X0),X1,X0)
| ~ class_Ring__and__Field_Ofield(X0) ),
inference(reorient_equations,[],[f1117]) ).
fof(f1131,axiom,
! [X2,X3,X0,X1] :
( c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X1,X2,X0),X3,X0) = c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(X1,X3,X0),X2,X0)
| ~ class_Ring__and__Field_Odivision__by__zero(X0)
| ~ class_Ring__and__Field_Ofield(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_mult__frac__num_0) ).
fof(f1135,negated_conjecture,
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),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f1136,plain,
c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = 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)),
inference(reorient_equations,[],[f1135]) ).
fof(f1137,negated_conjecture,
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),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_1) ).
fof(f1138,plain,
c_HOL_Ozero__class_Ozero(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)),
inference(reorient_equations,[],[f1137]) ).
fof(f1229,axiom,
class_Ring__and__Field_Odivision__by__zero(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_RealDef__Oreal__Ring__and__Field_Odivision__by__zero) ).
fof(f1252,axiom,
class_Ring__and__Field_Ofield(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_RealDef__Oreal__Ring__and__Field_Ofield) ).
fof(f1259,axiom,
class_Int_Onumber__ring(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_RealDef__Oreal__Int_Onumber__ring) ).
fof(f1290,plain,
c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_Transcendental_Osin(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(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_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)),
inference(definition_unfolding,[],[f1136,f949]) ).
fof(f1291,plain,
! [X0] : c_HOL_Oone__class_Oone(tc_RealDef_Oreal) = c_Transcendental_Osin(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(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_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_RealDef_Oreal(X0,tc_nat),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),tc_RealDef_Oreal)),
inference(definition_unfolding,[],[f947,f949]) ).
fof(f1311,plain,
! [X0,X1] : c_Transcendental_Osin(c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal)) = c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(X0),c_Transcendental_Osin(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),X1,tc_RealDef_Oreal)),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),X0,tc_RealDef_Oreal)),c_Transcendental_Osin(X1),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(definition_unfolding,[],[f837,f949,f949]) ).
fof(f1315,plain,
! [X0] : c_Transcendental_Osin(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),X0,tc_RealDef_Oreal)) = c_Transcendental_Osin(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(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_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal),tc_RealDef_Oreal)),
inference(definition_unfolding,[],[f822,f949,f949]) ).
tcf(c_1115,negated_conjecture,
c_Transcendental_Osin(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(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_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_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(cnf_transformation,[],[f1290]) ).
tcf(c_1116,negated_conjecture,
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),
inference(cnf_transformation,[],[f1138]) ).
tcf(c_1117,plain,
! [X0: $i,X1: $i] : c_HOL_Otimes__class_Otimes(X0,X1,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(X1,X0,tc_RealDef_Oreal),
inference(cnf_transformation,[],[f1111]) ).
tcf(c_1118,plain,
! [X0: $i,X1: $i,X2: $i] : c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(X0,X1,tc_RealDef_Oreal),X2,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(X0,c_HOL_Otimes__class_Otimes(X1,X2,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(cnf_transformation,[],[f1049]) ).
tcf(c_1125,plain,
class_Ring__and__Field_Odivision__by__zero(tc_RealDef_Oreal),
inference(cnf_transformation,[],[f1229]) ).
tcf(c_1195,plain,
! [X0: $i] : c_Transcendental_Osin(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(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_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_RealDef_Oreal(X0,tc_nat),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_HOL_Oone__class_Oone(tc_RealDef_Oreal),
inference(cnf_transformation,[],[f1291]) ).
tcf(c_1219,plain,
! [X0: $i,X1: $i] : c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(X0),c_Transcendental_Osin(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),X1,tc_RealDef_Oreal)),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),X0,tc_RealDef_Oreal)),c_Transcendental_Osin(X1),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_Transcendental_Osin(c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal)),
inference(cnf_transformation,[],[f1311]) ).
tcf(c_1223,plain,
! [X0: $i] : c_Transcendental_Osin(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(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_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_Transcendental_Osin(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),X0,tc_RealDef_Oreal)),
inference(cnf_transformation,[],[f1315]) ).
tcf(c_1235,plain,
c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_Transcendental_Osin(c_Transcendental_Opi),
inference(cnf_transformation,[],[f1115]) ).
tcf(c_1236,plain,
c_Transcendental_Osin(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_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(cnf_transformation,[],[f1101]) ).
tcf(c_1248,plain,
! [X0: $i] : c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(X0),tc_RealDef_Oreal) = c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal)),
inference(cnf_transformation,[],[f829]) ).
tcf(c_1250,plain,
! [X0: $i] : 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,[],[f825]) ).
tcf(c_1322,plain,
! [X0: $i,X1: $i] :
( ( c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = X0 )
| ( c_HOL_Ouminus__class_Ouminus(c_HOL_Otimes__class_Otimes(X0,X0,tc_RealDef_Oreal),tc_RealDef_Oreal) != c_HOL_Otimes__class_Otimes(X1,X1,tc_RealDef_Oreal) ) ),
inference(cnf_transformation,[],[f608]) ).
tcf(c_1340,plain,
! [X0: $i,X1: $i] : c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(X0,X1,tc_RealDef_Oreal),X1,tc_RealDef_Oreal) = X0,
inference(cnf_transformation,[],[f492]) ).
tcf(c_1343,plain,
! [X0: $i,X1: $i] : c_HOL_Oplus__class_Oplus(X0,c_HOL_Ouminus__class_Ouminus(X1,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal),
inference(cnf_transformation,[],[f96]) ).
tcf(c_1430,plain,
c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) != c_HOL_Oone__class_Oone(tc_RealDef_Oreal),
inference(cnf_transformation,[],[f783]) ).
tcf(c_1526,plain,
class_Ring__and__Field_Ofield(tc_RealDef_Oreal),
inference(cnf_transformation,[],[f1252]) ).
tcf(c_1527,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X1,X2,X0),X3,X0) = c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(X1,X3,X0),X2,X0) )
| ~ class_Ring__and__Field_Odivision__by__zero(X0)
| ~ class_Ring__and__Field_Ofield(X0) ),
inference(cnf_transformation,[],[f1131]) ).
tcf(c_1532,plain,
! [X0: $i,X1: $i] :
( ( c_HOL_Oinverse__class_Odivide(c_HOL_Ozero__class_Ozero(X0),X1,X0) = c_HOL_Ozero__class_Ozero(X0) )
| ~ class_Ring__and__Field_Ofield(X0) ),
inference(cnf_transformation,[],[f1118]) ).
tcf(c_1556,plain,
! [X0: $i,X1: $i] :
( ( c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(X0),X1,X0),X1,X0) = c_HOL_Ozero__class_Ozero(X0) )
| ~ class_Ring__and__Field_Odivision__by__zero(X0)
| ~ class_Ring__and__Field_Ofield(X0) ),
inference(cnf_transformation,[],[f1004]) ).
tcf(c_1576,plain,
class_Int_Onumber__ring(tc_RealDef_Oreal),
inference(cnf_transformation,[],[f1259]) ).
tcf(c_1578,plain,
! [X0: $i,X1: $i] :
( ( c_HOL_Otimes__class_Otimes(X1,c_Int_Onumber__class_Onumber__of(c_Int_OBit1(c_Int_OPls),X0),X0) = X1 )
| ~ class_Int_Onumber__ring(X0) ),
inference(cnf_transformation,[],[f1103]) ).
tcf(c_1581,plain,
! [X0: $i] :
( ( c_Int_Onumber__class_Onumber__of(c_Int_OPls,X0) = c_HOL_Ozero__class_Ozero(X0) )
| ~ class_Int_Onumber__ring(X0) ),
inference(cnf_transformation,[],[f961]) ).
tcf(c_1585,plain,
! [X0: $i,X1: $i] :
( ( c_HOL_Otimes__class_Otimes(X1,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),X0),X0) = c_HOL_Oplus__class_Oplus(X1,X1,X0) )
| ~ class_Int_Onumber__ring(X0) ),
inference(cnf_transformation,[],[f902]) ).
tcf(c_1588,plain,
! [X0: $i] :
( ( c_Int_Onumber__class_Onumber__of(c_Int_OBit1(c_Int_OPls),X0) = c_HOL_Oone__class_Oone(X0) )
| ~ class_Int_Onumber__ring(X0) ),
inference(cnf_transformation,[],[f693]) ).
tcf(c_1592,plain,
! [X0: $i,X1: $i] :
( ( c_HOL_Oplus__class_Oplus(c_Int_Onumber__class_Onumber__of(c_Int_OPls,X0),X1,X0) = X1 )
| ~ class_Int_Onumber__ring(X0) ),
inference(cnf_transformation,[],[f595]) ).
tcf(c_2036,plain,
! [X0: $i,X1: $i] :
( ( c_HOL_Oplus__class_Oplus(c_Int_Onumber__class_Onumber__of(c_Int_OPls,X0),X1,X0) = X1 )
| ~ class_Int_Onumber__ring(X0) ),
inference(prop_impl_just,[status(thm)],[c_1592]) ).
tcf(c_2042,plain,
! [X0: $i] :
( ( c_Int_Onumber__class_Onumber__of(c_Int_OBit1(c_Int_OPls),X0) = c_HOL_Oone__class_Oone(X0) )
| ~ class_Int_Onumber__ring(X0) ),
inference(prop_impl_just,[status(thm)],[c_1588]) ).
tcf(c_2046,plain,
! [X0: $i,X1: $i] :
( ( c_HOL_Otimes__class_Otimes(X1,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),X0),X0) = c_HOL_Oplus__class_Oplus(X1,X1,X0) )
| ~ class_Int_Onumber__ring(X0) ),
inference(prop_impl_just,[status(thm)],[c_1585]) ).
tcf(c_2050,plain,
! [X0: $i] :
( ( c_Int_Onumber__class_Onumber__of(c_Int_OPls,X0) = c_HOL_Ozero__class_Ozero(X0) )
| ~ class_Int_Onumber__ring(X0) ),
inference(prop_impl_just,[status(thm)],[c_1581]) ).
tcf(c_2054,plain,
! [X0: $i,X1: $i] :
( ( c_HOL_Otimes__class_Otimes(X1,c_Int_Onumber__class_Onumber__of(c_Int_OBit1(c_Int_OPls),X0),X0) = X1 )
| ~ class_Int_Onumber__ring(X0) ),
inference(prop_impl_just,[status(thm)],[c_1578]) ).
tcf(c_2078,plain,
! [X0: $i,X1: $i] :
( ( c_HOL_Oinverse__class_Odivide(c_HOL_Ozero__class_Ozero(X0),X1,X0) = c_HOL_Ozero__class_Ozero(X0) )
| ~ class_Ring__and__Field_Ofield(X0) ),
inference(prop_impl_just,[status(thm)],[c_1532]) ).
tcf(c_4836,plain,
! [X0: $i] : 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(light_normalisation,[status(thm)],[c_1250,c_1248]) ).
tcf(c_4959,plain,
c_Transcendental_Osin(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_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(demodulation,[status(thm)],[c_1236,c_1117]) ).
tcf(c_5128,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_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(demodulation,[status(thm)],[c_1116,c_1117]) ).
tcf(c_5907,plain,
! [X0: $i] : c_Transcendental_Osin(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(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_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,c_RealDef_Oreal(X0,tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_HOL_Oone__class_Oone(tc_RealDef_Oreal),
inference(demodulation,[status(thm)],[c_1195,c_1117,c_1118]) ).
tcf(c_5908,plain,
c_Transcendental_Osin(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(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_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_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(demodulation,[status(thm)],[c_1115,c_1117]) ).
tcf(c_6804,plain,
! [X0: $i] :
( ( c_Int_Onumber__class_Onumber__of(c_Int_OPls,X0) = c_HOL_Ozero__class_Ozero(X0) )
| ( X0 != tc_RealDef_Oreal ) ),
inference(resolution_lifted,[status(thm)],[c_2050,c_1576]) ).
tcf(c_6805,plain,
c_Int_Onumber__class_Onumber__of(c_Int_OPls,tc_RealDef_Oreal) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(unflattening,[status(thm)],[c_6804]) ).
tcf(c_6815,plain,
! [X0: $i,X1: $i] :
( ( c_HOL_Otimes__class_Otimes(X1,c_Int_Onumber__class_Onumber__of(c_Int_OBit1(c_Int_OPls),X0),X0) = X1 )
| ( X0 != tc_RealDef_Oreal ) ),
inference(resolution_lifted,[status(thm)],[c_2054,c_1576]) ).
tcf(c_6816,plain,
! [X0: $i] : c_HOL_Otimes__class_Otimes(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit1(c_Int_OPls),tc_RealDef_Oreal),tc_RealDef_Oreal) = X0,
inference(unflattening,[status(thm)],[c_6815]) ).
tcf(c_6869,plain,
! [X0: $i,X1: $i] :
( ( c_HOL_Otimes__class_Otimes(X1,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),X0),X0) = c_HOL_Oplus__class_Oplus(X1,X1,X0) )
| ( X0 != tc_RealDef_Oreal ) ),
inference(resolution_lifted,[status(thm)],[c_2046,c_1576]) ).
tcf(c_6870,plain,
! [X0: $i] : c_HOL_Otimes__class_Otimes(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(X0,X0,tc_RealDef_Oreal),
inference(unflattening,[status(thm)],[c_6869]) ).
tcf(c_6881,plain,
! [X0: $i] :
( ( c_Int_Onumber__class_Onumber__of(c_Int_OBit1(c_Int_OPls),X0) = c_HOL_Oone__class_Oone(X0) )
| ( X0 != tc_RealDef_Oreal ) ),
inference(resolution_lifted,[status(thm)],[c_2042,c_1576]) ).
tcf(c_6882,plain,
c_Int_Onumber__class_Onumber__of(c_Int_OBit1(c_Int_OPls),tc_RealDef_Oreal) = c_HOL_Oone__class_Oone(tc_RealDef_Oreal),
inference(unflattening,[status(thm)],[c_6881]) ).
tcf(c_6904,plain,
! [X0: $i,X1: $i] :
( ( c_HOL_Oplus__class_Oplus(c_Int_Onumber__class_Onumber__of(c_Int_OPls,X0),X1,X0) = X1 )
| ( X0 != tc_RealDef_Oreal ) ),
inference(resolution_lifted,[status(thm)],[c_2036,c_1576]) ).
tcf(c_6905,plain,
! [X0: $i] : c_HOL_Oplus__class_Oplus(c_Int_Onumber__class_Onumber__of(c_Int_OPls,tc_RealDef_Oreal),X0,tc_RealDef_Oreal) = X0,
inference(unflattening,[status(thm)],[c_6904]) ).
tcf(c_7368,plain,
! [X0: $i,X1: $i] :
( ( c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(X0),X1,X0),X1,X0) = c_HOL_Ozero__class_Ozero(X0) )
| ~ class_Ring__and__Field_Odivision__by__zero(X0)
| ( X0 != tc_RealDef_Oreal ) ),
inference(resolution_lifted,[status(thm)],[c_1556,c_1526]) ).
tcf(c_7369,plain,
! [X0: $i] :
( ( c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal),X0,tc_RealDef_Oreal) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) )
| ~ class_Ring__and__Field_Odivision__by__zero(tc_RealDef_Oreal) ),
inference(unflattening,[status(thm)],[c_7368]) ).
tcf(c_7371,plain,
! [X0: $i] : c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal),X0,tc_RealDef_Oreal) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(global_subsumption_just,[status(thm)],[c_7369,c_1125,c_7369]) ).
tcf(c_7395,plain,
! [X0: $i,X1: $i] :
( ( c_HOL_Oinverse__class_Odivide(c_HOL_Ozero__class_Ozero(X0),X1,X0) = c_HOL_Ozero__class_Ozero(X0) )
| ( X0 != tc_RealDef_Oreal ) ),
inference(resolution_lifted,[status(thm)],[c_2078,c_1526]) ).
tcf(c_7396,plain,
! [X0: $i] : c_HOL_Oinverse__class_Odivide(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(unflattening,[status(thm)],[c_7395]) ).
tcf(c_7430,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X1,X2,X0),X3,X0) = c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(X1,X3,X0),X2,X0) )
| ~ class_Ring__and__Field_Odivision__by__zero(X0)
| ( X0 != tc_RealDef_Oreal ) ),
inference(resolution_lifted,[status(thm)],[c_1527,c_1526]) ).
tcf(c_7431,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X0,X1,tc_RealDef_Oreal),X2,tc_RealDef_Oreal) = c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(X0,X2,tc_RealDef_Oreal),X1,tc_RealDef_Oreal) )
| ~ class_Ring__and__Field_Odivision__by__zero(tc_RealDef_Oreal) ),
inference(unflattening,[status(thm)],[c_7430]) ).
tcf(c_7433,plain,
! [X0: $i,X1: $i,X2: $i] : c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X0,X1,tc_RealDef_Oreal),X2,tc_RealDef_Oreal) = c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(X0,X2,tc_RealDef_Oreal),X1,tc_RealDef_Oreal),
inference(global_subsumption_just,[status(thm)],[c_7431,c_1125,c_7431]) ).
tcf(c_12043,plain,
! [X0: $i] : c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal) = X0,
inference(light_normalisation,[status(thm)],[c_6905,c_6805]) ).
tcf(c_12052,plain,
! [X0: $i] : c_HOL_Otimes__class_Otimes(X0,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal) = X0,
inference(light_normalisation,[status(thm)],[c_6816,c_6882]) ).
tcf(c_12204,plain,
c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(c_Transcendental_Opi,c_Transcendental_Opi,tc_RealDef_Oreal)) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(demodulation,[status(thm)],[c_4959,c_6870]) ).
tcf(c_12206,plain,
c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(c_Transcendental_Opi,tc_RealDef_Oreal)) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(demodulation,[status(thm)],[c_12204,c_4836]) ).
tcf(c_12321,plain,
! [X0: $i] : c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal),X0,tc_RealDef_Oreal) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(demodulation,[status(thm)],[c_7371,c_7433]) ).
tcf(c_12322,plain,
! [X0: $i] : c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(light_normalisation,[status(thm)],[c_12321,c_7396]) ).
tcf(c_12366,plain,
c_Transcendental_Osin(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(demodulation,[status(thm)],[c_5128,c_1117,c_7433]) ).
tcf(c_13065,plain,
c_Transcendental_Osin(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(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_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(demodulation,[status(thm)],[c_5908,c_1117,c_7433]) ).
tcf(c_21812,plain,
c_HOL_Ouminus__class_Ouminus(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) = c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(c_Transcendental_Opi,tc_RealDef_Oreal)),
inference(superposition,[status(thm)],[c_1235,c_1248]) ).
tcf(c_21814,plain,
! [X0: $i] : c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(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_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,c_RealDef_Oreal(X0,tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_HOL_Ouminus__class_Ouminus(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(superposition,[status(thm)],[c_5907,c_1248]) ).
tcf(c_21818,plain,
c_HOL_Ouminus__class_Ouminus(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(light_normalisation,[status(thm)],[c_21812,c_12206]) ).
tcf(c_21822,plain,
! [X0: $i] : c_HOL_Otimes__class_Otimes(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(superposition,[status(thm)],[c_1117,c_12322]) ).
tcf(c_22147,plain,
! [X0: $i,X1: $i] : c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal),c_HOL_Ouminus__class_Ouminus(X1,tc_RealDef_Oreal),tc_RealDef_Oreal) = X0,
inference(superposition,[status(thm)],[c_1343,c_1340]) ).
tcf(c_22150,plain,
! [X0: $i] : c_HOL_Ominus__class_Ominus(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal) = c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal),
inference(superposition,[status(thm)],[c_1343,c_12043]) ).
tcf(c_22935,plain,
! [X0: $i,X1: $i] : 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(superposition,[status(thm)],[c_1340,c_22147]) ).
tcf(c_26844,plain,
! [X0: $i,X1: $i,X2: $i] : c_HOL_Otimes__class_Otimes(X0,c_HOL_Otimes__class_Otimes(X1,X2,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(X1,c_HOL_Otimes__class_Otimes(X2,X0,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(superposition,[status(thm)],[c_1118,c_1117]) ).
tcf(c_26851,plain,
! [X0: $i] : c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(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_HOL_Otimes__class_Otimes(c_Transcendental_Opi,c_HOL_Otimes__class_Otimes(c_RealDef_Oreal(X0,tc_nat),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_HOL_Ouminus__class_Ouminus(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(demodulation,[status(thm)],[c_21814,c_26844]) ).
tcf(c_28453,plain,
! [X0: $i] :
( ( c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_HOL_Oone__class_Oone(tc_RealDef_Oreal) )
| ( c_HOL_Otimes__class_Otimes(X0,X0,tc_RealDef_Oreal) != c_HOL_Ouminus__class_Ouminus(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal) ) ),
inference(superposition,[status(thm)],[c_12052,c_1322]) ).
tcf(c_28463,plain,
! [X0: $i] : c_HOL_Otimes__class_Otimes(X0,X0,tc_RealDef_Oreal) != c_HOL_Ouminus__class_Ouminus(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_subsumption_resolution,[status(thm)],[c_28453,c_1430]) ).
tcf(c_28582,plain,
c_HOL_Ouminus__class_Ouminus(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(superposition,[status(thm)],[c_12322,c_28463]) ).
tcf(c_28975,plain,
! [X0: $i] : c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(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_HOL_Otimes__class_Otimes(c_Transcendental_Opi,c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_RealDef_Oreal(X0,tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_HOL_Ouminus__class_Ouminus(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(superposition,[status(thm)],[c_1117,c_26851]) ).
tcf(c_44147,plain,
! [X0: $i] : c_Transcendental_Osin(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),X0,tc_RealDef_Oreal)) = c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),X0,tc_RealDef_Oreal)),
inference(demodulation,[status(thm)],[c_1223,c_22935]) ).
tcf(c_44159,plain,
c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(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_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(demodulation,[status(thm)],[c_13065,c_44147]) ).
tcf(c_47877,plain,
! [X0: $i,X1: $i] : c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(X0),c_Transcendental_Osin(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),X1,tc_RealDef_Oreal)),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),X0,tc_RealDef_Oreal)),c_Transcendental_Osin(X1),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_Transcendental_Osin(c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal)),
inference(light_normalisation,[status(thm)],[c_1219,c_44147]) ).
tcf(c_47878,plain,
! [X0: $i,X1: $i] : c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(X0),c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),X1,tc_RealDef_Oreal)),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),X0,tc_RealDef_Oreal)),c_Transcendental_Osin(X1),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_Transcendental_Osin(c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal)),
inference(demodulation,[status(thm)],[c_47877,c_44147]) ).
tcf(c_47921,plain,
! [X0: $i] : c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(X0),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),X0,tc_RealDef_Oreal)),c_Transcendental_Osin(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_Transcendental_Osin(c_HOL_Ominus__class_Ominus(X0,c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)),
inference(superposition,[status(thm)],[c_44159,c_47878]) ).
tcf(c_48026,plain,
! [X0: $i] : c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(X0),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),X0,tc_RealDef_Oreal)),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_Transcendental_Osin(c_HOL_Ominus__class_Ominus(X0,c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)),
inference(light_normalisation,[status(thm)],[c_47921,c_12366]) ).
tcf(c_50241,plain,
! [X0: $i] : c_Transcendental_Osin(c_HOL_Ominus__class_Ominus(X0,c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(demodulation,[status(thm)],[c_48026,c_21818,c_21822,c_22150]) ).
tcf(c_50244,plain,
! [X0: $i] : c_Transcendental_Osin(X0) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(superposition,[status(thm)],[c_1340,c_50241]) ).
tcf(c_50333,plain,
c_HOL_Ouminus__class_Ouminus(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(demodulation,[status(thm)],[c_28975,c_50244]) ).
tcf(c_50365,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_50333,c_28582]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWV602-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.07 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.18/0.45 % Computer : n016.cluster.edu
% 0.18/0.45 % Model : x86_64 x86_64
% 0.18/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.45 % Memory : 8046.5625MB
% 0.18/0.45 % OS : Linux 6.8.0-71-generic
% 0.18/0.45 % CPULimit : 300
% 0.18/0.45 % WCLimit : 300
% 0.18/0.46 % DateTime : Thu Sep 24 20:45:28 UTC 2026
% 0.18/0.46 % CPUTime :
% 0.18/0.46 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.24/0.52 Running first-order theorem proving
% 0.24/0.52 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.24/0.54
% 0.24/0.54 % ======== iProver multi-core TPTP/SMT =========
% 0.24/0.54
% 0.24/0.54 % Detected problem language: tptp
% 0.24/0.55 % Proving...
% 39.68/6.46 % SZS status Started for theBenchmark.p
% 39.68/6.46 % SZS status Unsatisfiable for theBenchmark.p
% 39.68/6.46
% 39.68/6.46 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 39.68/6.46
% 39.68/6.46 % ------ iProver source info
% 39.68/6.46
% 39.68/6.46 % git: date: 2026-07-19 20:42:38 +0200
% 39.68/6.46 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 39.68/6.46 % git: non_committed_changes: false
% 39.68/6.46
% 39.68/6.46 % ------ Parsing...% successful
% 39.68/6.46
% 39.68/6.46
% 39.68/6.46 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 39.68/6.46
% 39.68/6.46 % ------ Preprocessing... sup_sim: 41 sf_s rm: 1 0s sf_e pe_s pe:1:0s pe:2:0s pe:4:0s pe_e sup_sim: 64 sf_s rm: 6 0s sf_e pe_s pe_e sup_sim: 0 sf_s rm: 6 0s sf_e pe_s pe_e %
% 39.68/6.46
% 39.68/6.46 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 39.68/6.46
% 39.68/6.46 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 39.68/6.46 % ------ Proving...
% 39.68/6.46 % ------ Problem Properties
% 39.68/6.46
% 39.68/6.46 %
% 39.68/6.46 % clauses 357
% 39.68/6.46 % conjectures 0
% 39.68/6.46 % EPR 7
% 39.68/6.46 % Horn 291
% 39.68/6.46 % unary 140
% 39.68/6.46 % binary 81
% 39.68/6.46 % lits 766
% 39.68/6.46 % lits eq 260
% 39.68/6.46 % fd_pure 0
% 39.68/6.46 % fd_pseudo 0
% 39.68/6.46 % fd_cond 20
% 39.68/6.46 % fd_pseudo_cond 15
% 39.68/6.46 % AC symbols 0
% 39.68/6.46
% 39.68/6.46 % ------ Schedule dynamic 5 is on
% 39.68/6.46
% 39.68/6.46 % ------ no conjectures: strip conj schedule
% 39.68/6.46
% 39.68/6.46 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" stripped conjectures Time Limit: 10.
% 39.68/6.46
% 39.68/6.46
% 39.68/6.46 % ------
% 39.68/6.46 % Current options:
% 39.68/6.46 % ------
% 39.68/6.46
% 39.68/6.46
% 39.68/6.46 %
% 39.68/6.46
% 39.68/6.46 % ------ Proving...
% 39.68/6.46 %
% 39.68/6.46
% 39.68/6.46 % SZS status Unsatisfiable for theBenchmark.p
% 39.68/6.46
% 39.68/6.46 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 39.68/6.46
% 39.68/6.46
%------------------------------------------------------------------------------