Vampire---5.0.1.UNS-Ref.s

%------------------------------------------------------------------------------
% File     : Vampire---5.0.1
% Problem  : SWV602-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM

% 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 : Tue Sep 29 01:19:04 PM UTC 2026

% Result   : Unsatisfiable 14.61s 3.64s
% Output   : Refutation 0.31s
% Verified : 
% SZS Type : Refutation
%            Derivation depth      :   25
%            Number of leaves      :   35
% Syntax   : Number of formulae    :  203 ( 203 unt;  11 def)
%            Number of atoms       :  203 ( 202 equ)
%            Maximal formula atoms :    1 (   1 avg)
%            Number of connectives :    2 (   2   ~;   0   |;   0   &)
%                                         (   0 <=>;   0  =>;   0  <=;   0 <~>)
%            Maximal formula depth :    4 (   2 avg)
%            Maximal term depth    :    9 (   2 avg)
%            Number of predicates  :    2 (   0 usr;   1 prp; 0-2 aty)
%            Number of functors    :   29 (  29 usr;  16 con; 0-3 aty)
%            Number of variables   :  167 ( 167   !;   0   ?)

% 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/sandbox/benchmark/theBenchmark.p',cls_real__diff__def_0) ).

fof(f195,axiom,
    ! [X0,X1] : c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(X0,X1,tc_RealDef_Oreal)) = c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(X0),c_Transcendental_Ocos(X1),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(X0),c_Transcendental_Osin(X1),tc_RealDef_Oreal),tc_RealDef_Oreal),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_cos__add_0) ).

fof(f198,axiom,
    ! [X0,X1] : c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal)) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(X1),c_Transcendental_Ocos(X0),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(X1),c_Transcendental_Osin(X0),tc_RealDef_Oreal),tc_RealDef_Oreal),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_cos__diff2_0) ).

fof(f199,axiom,
    ! [X0,X1] : c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal)) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(X0),c_Transcendental_Ocos(X1),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(X0),c_Transcendental_Osin(X1),tc_RealDef_Oreal),tc_RealDef_Oreal),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_cos__diff_0) ).

fof(f468,axiom,
    ! [X0] : c_HOL_Oplus__class_Oplus(X0,c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_real__add__eq__0__iff_1) ).

fof(f469,plain,
    ! [X0] : c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(X0,c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(reorient_equations,[],[f468]) ).

fof(f610,axiom,
    c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_real__two__squares__add__zero__iff_2) ).

fof(f611,plain,
    c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(reorient_equations,[],[f610]) ).

fof(f632,axiom,
    c_Transcendental_Ocos(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)) = c_HOL_Oone__class_Oone(tc_RealDef_Oreal),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_cos__zero_0) ).

fof(f633,plain,
    c_HOL_Oone__class_Oone(tc_RealDef_Oreal) = c_Transcendental_Ocos(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)),
    inference(reorient_equations,[],[f632]) ).

fof(f783,axiom,
    c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) != c_HOL_Oone__class_Oone(tc_RealDef_Oreal),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_real__zero__not__eq__one_0) ).

fof(f806,axiom,
    ! [X2,X0,X1] : c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(X0,X1,tc_RealDef_Oreal),X2,tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(X0,X2,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X1,X2,tc_RealDef_Oreal),tc_RealDef_Oreal),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_real__add__mult__distrib_0) ).

fof(f820,axiom,
    ! [X0] : c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(X0,c_Transcendental_Opi,tc_RealDef_Oreal)) = c_HOL_Ouminus__class_Ouminus(c_Transcendental_Ocos(X0),tc_RealDef_Oreal),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_cos__periodic__pi_0) ).

fof(f821,axiom,
    ! [X0] : c_Transcendental_Ocos(c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal)) = c_Transcendental_Ocos(X0),
    file('/export/starexec/sandbox/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(f823,axiom,
    ! [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),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_sin__periodic__pi__diff_0) ).

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/sandbox/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(f836,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_Ocos(X1),c_Transcendental_Osin(X0),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(X1),c_Transcendental_Ocos(X0),tc_RealDef_Oreal),tc_RealDef_Oreal),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_sin__diff2_0) ).

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/sandbox/benchmark/theBenchmark.p',cls_sin__diff_0) ).

fof(f896,axiom,
    ! [X0] : c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(X0),tc_RealDef_Oreal) = c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(X0,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),tc_RealDef_Oreal)),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_minus__sin__cos__eq_0) ).

fof(f948,axiom,
    ! [X0] : c_Transcendental_Osin(X0) = c_Transcendental_Ocos(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/sandbox/benchmark/theBenchmark.p',cls_sin__cos__eq_0) ).

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/sandbox/benchmark/theBenchmark.p',cls_cos__sin__eq_0) ).

fof(f1039,axiom,
    c_Transcendental_Osin(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_sin__zero_0) ).

fof(f1040,plain,
    c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_Transcendental_Osin(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)),
    inference(reorient_equations,[],[f1039]) ).

fof(f1084,axiom,
    c_Transcendental_Ocos(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_Ozero__class_Ozero(tc_RealDef_Oreal),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_cos__pi__half_0) ).

fof(f1085,plain,
    c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_Transcendental_Ocos(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)),
    inference(reorient_equations,[],[f1084]) ).

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/sandbox/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/sandbox/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(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/sandbox/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/sandbox/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(f1289,plain,
    ! [X0] : c_Transcendental_Ocos(X0) = c_Transcendental_Ocos(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_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),tc_RealDef_Oreal)),
    inference(definition_unfolding,[],[f949,f948]) ).

fof(f1295,plain,
    ! [X0,X1] : c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(X0,X1,tc_RealDef_Oreal)) = c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(X0),c_Transcendental_Ocos(X1),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(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_Ocos(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),tc_RealDef_Oreal),
    inference(definition_unfolding,[],[f195,f948,f948]) ).

fof(f1297,plain,
    ! [X0,X1] : c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal)) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(X1),c_Transcendental_Ocos(X0),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(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)),c_Transcendental_Ocos(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)),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(definition_unfolding,[],[f198,f948,f948]) ).

fof(f1298,plain,
    ! [X0,X1] : c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal)) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(X0),c_Transcendental_Ocos(X1),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(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_Ocos(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),tc_RealDef_Oreal),
    inference(definition_unfolding,[],[f199,f948,f948]) ).

fof(f1321,plain,
    ! [X0] : c_Transcendental_Ocos(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_Ominus__class_Ominus(X0,c_Transcendental_Opi,tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_HOL_Ouminus__class_Ouminus(c_Transcendental_Ocos(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)),tc_RealDef_Oreal),
    inference(definition_unfolding,[],[f823,f948,f948]) ).

fof(f1324,plain,
    ! [X0] : c_Transcendental_Ocos(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_HOL_Ouminus__class_Ouminus(c_Transcendental_Ocos(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)),tc_RealDef_Oreal),
    inference(definition_unfolding,[],[f829,f948,f948]) ).

fof(f1327,plain,
    ! [X0,X1] : c_Transcendental_Ocos(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_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(X1),c_Transcendental_Ocos(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)),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(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)),c_Transcendental_Ocos(X0),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(definition_unfolding,[],[f836,f948,f948,f948]) ).

fof(f1328,plain,
    ! [X0,X1] : c_Transcendental_Ocos(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_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(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_Ocos(X1),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(X0),c_Transcendental_Ocos(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),tc_RealDef_Oreal),
    inference(definition_unfolding,[],[f837,f948,f948,f948]) ).

fof(f1335,plain,
    ! [X0] : c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(X0,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),tc_RealDef_Oreal)) = c_HOL_Ouminus__class_Ouminus(c_Transcendental_Ocos(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)),tc_RealDef_Oreal),
    inference(definition_unfolding,[],[f896,f948]) ).

fof(f1349,plain,
    c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_Transcendental_Ocos(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_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)),
    inference(definition_unfolding,[],[f1040,f948]) ).

fof(f1352,plain,
    c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_Transcendental_Ocos(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_Transcendental_Opi,tc_RealDef_Oreal)),
    inference(definition_unfolding,[],[f1115,f948]) ).

fof(f1355,plain,
    c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_Transcendental_Ocos(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,[],[f1138,f948]) ).

fof(f1356,definition,
    sF0 = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
    introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).

fof(f1357,plain,
    c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = sF0,
    inference(reorient_equations,[],[f1356]) ).

fof(f1358,definition,
    sF1 = c_Int_OBit1(c_Int_OPls),
    introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).

fof(f1359,plain,
    c_Int_OBit1(c_Int_OPls) = sF1,
    inference(reorient_equations,[],[f1358]) ).

fof(f1360,definition,
    sF2 = c_Int_OBit0(sF1),
    introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).

fof(f1361,plain,
    c_Int_OBit0(sF1) = sF2,
    inference(reorient_equations,[],[f1360]) ).

fof(f1362,definition,
    sF3 = c_Int_Onumber__class_Onumber__of(sF2,tc_RealDef_Oreal),
    introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).

fof(f1363,plain,
    c_Int_Onumber__class_Onumber__of(sF2,tc_RealDef_Oreal) = sF3,
    inference(reorient_equations,[],[f1362]) ).

fof(f1364,definition,
    sF4 = c_HOL_Otimes__class_Otimes(sF3,c_Transcendental_Opi,tc_RealDef_Oreal),
    introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).

fof(f1365,plain,
    c_HOL_Otimes__class_Otimes(sF3,c_Transcendental_Opi,tc_RealDef_Oreal) = sF4,
    inference(reorient_equations,[],[f1364]) ).

fof(f1366,definition,
    sF5 = c_RealDef_Oreal(v_n,tc_nat),
    introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).

fof(f1367,plain,
    c_RealDef_Oreal(v_n,tc_nat) = sF5,
    inference(reorient_equations,[],[f1366]) ).

fof(f1368,definition,
    sF6 = c_HOL_Oinverse__class_Odivide(sF4,sF5,tc_RealDef_Oreal),
    introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).

fof(f1369,plain,
    c_HOL_Oinverse__class_Odivide(sF4,sF5,tc_RealDef_Oreal) = sF6,
    inference(reorient_equations,[],[f1368]) ).

fof(f1370,definition,
    sF7 = c_Transcendental_Ocos(sF6),
    introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).

fof(f1371,plain,
    c_Transcendental_Ocos(sF6) = sF7,
    inference(reorient_equations,[],[f1370]) ).

fof(f1372,plain,
    sF0 = sF7,
    inference(definition_folding,[],[f1136,f1371,f1369,f1367,f1365,f1363,f1361,f1359,f1357]) ).

fof(f1373,definition,
    sF8 = c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,sF3,tc_RealDef_Oreal),
    introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).

fof(f1374,plain,
    c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,sF3,tc_RealDef_Oreal) = sF8,
    inference(reorient_equations,[],[f1373]) ).

fof(f1375,definition,
    sF9 = c_HOL_Ominus__class_Ominus(sF8,sF6,tc_RealDef_Oreal),
    introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).

fof(f1376,plain,
    c_HOL_Ominus__class_Ominus(sF8,sF6,tc_RealDef_Oreal) = sF9,
    inference(reorient_equations,[],[f1375]) ).

fof(f1377,definition,
    sF10 = c_Transcendental_Ocos(sF9),
    introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).

fof(f1378,plain,
    c_Transcendental_Ocos(sF9) = sF10,
    inference(reorient_equations,[],[f1377]) ).

fof(f1379,plain,
    sF0 = sF10,
    inference(definition_folding,[],[f1355,f1378,f1376,f1369,f1367,f1365,f1363,f1361,f1359,f1374,f1363,f1361,f1359,f1357]) ).

fof(f1381,plain,
    sF7 = sF10,
    inference(backward_demodulation,[],[f1379,f1372]) ).

fof(f1396,plain,
    ! [X0] : c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(X0,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),tc_RealDef_Oreal)) = c_Transcendental_Ocos(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(forward_demodulation,[],[f1324,f1335]) ).

fof(f1399,plain,
    ! [X0] : c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(X0,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),tc_RealDef_Oreal)) = c_Transcendental_Ocos(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_Ominus__class_Ominus(X0,c_Transcendental_Opi,tc_RealDef_Oreal),tc_RealDef_Oreal)),
    inference(forward_demodulation,[],[f1321,f1335]) ).

fof(f1408,plain,
    c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(forward_demodulation,[],[f611,f806]) ).

fof(f1414,plain,
    ! [X0] : c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_HOL_Ominus__class_Ominus(X0,X0,tc_RealDef_Oreal),
    inference(backward_demodulation,[],[f469,f96]) ).

fof(f1420,plain,
    c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = sF7,
    inference(forward_demodulation,[],[f1357,f1372]) ).

fof(f1471,plain,
    c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_Transcendental_Ocos(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF1),tc_RealDef_Oreal),tc_RealDef_Oreal)),
    inference(backward_demodulation,[],[f1085,f1359]) ).

fof(f1475,plain,
    ! [X0] : c_Transcendental_Ocos(X0) = c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF1),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF1),tc_RealDef_Oreal),tc_RealDef_Oreal),X0,tc_RealDef_Oreal),tc_RealDef_Oreal)),
    inference(backward_demodulation,[],[f1289,f1359]) ).

fof(f1476,plain,
    ! [X0,X1] : c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(X0,X1,tc_RealDef_Oreal)) = c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(X0),c_Transcendental_Ocos(X1),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF1),tc_RealDef_Oreal),tc_RealDef_Oreal),X0,tc_RealDef_Oreal)),c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF1),tc_RealDef_Oreal),tc_RealDef_Oreal),X1,tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(backward_demodulation,[],[f1295,f1359]) ).

fof(f1477,plain,
    ! [X0,X1] : c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal)) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(X1),c_Transcendental_Ocos(X0),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF1),tc_RealDef_Oreal),tc_RealDef_Oreal),X1,tc_RealDef_Oreal)),c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF1),tc_RealDef_Oreal),tc_RealDef_Oreal),X0,tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(backward_demodulation,[],[f1297,f1359]) ).

fof(f1478,plain,
    ! [X0,X1] : c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal)) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(X0),c_Transcendental_Ocos(X1),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF1),tc_RealDef_Oreal),tc_RealDef_Oreal),X0,tc_RealDef_Oreal)),c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF1),tc_RealDef_Oreal),tc_RealDef_Oreal),X1,tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(backward_demodulation,[],[f1298,f1359]) ).

fof(f1498,plain,
    ! [X0,X1] : c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF1),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(X1),c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF1),tc_RealDef_Oreal),tc_RealDef_Oreal),X0,tc_RealDef_Oreal)),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF1),tc_RealDef_Oreal),tc_RealDef_Oreal),X1,tc_RealDef_Oreal)),c_Transcendental_Ocos(X0),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(backward_demodulation,[],[f1327,f1359]) ).

fof(f1499,plain,
    ! [X0,X1] : c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF1),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF1),tc_RealDef_Oreal),tc_RealDef_Oreal),X0,tc_RealDef_Oreal)),c_Transcendental_Ocos(X1),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(X0),c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF1),tc_RealDef_Oreal),tc_RealDef_Oreal),X1,tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(backward_demodulation,[],[f1328,f1359]) ).

fof(f1512,plain,
    c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF1),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)),
    inference(backward_demodulation,[],[f1349,f1359]) ).

fof(f1514,plain,
    c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF1),tc_RealDef_Oreal),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal)),
    inference(backward_demodulation,[],[f1352,f1359]) ).

fof(f1517,plain,
    sF7 = c_Transcendental_Ocos(sF9),
    inference(backward_demodulation,[],[f1378,f1381]) ).

fof(f1532,plain,
    ! [X0] : c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(X0,c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF1),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF1),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal),tc_RealDef_Oreal)),
    inference(forward_demodulation,[],[f1396,f1359]) ).

fof(f1535,plain,
    ! [X0] : c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(X0,c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF1),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF1),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Ominus__class_Ominus(X0,c_Transcendental_Opi,tc_RealDef_Oreal),tc_RealDef_Oreal)),
    inference(forward_demodulation,[],[f1399,f1359]) ).

fof(f1542,plain,
    c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(forward_demodulation,[],[f1408,f1111]) ).

fof(f1595,plain,
    c_HOL_Oone__class_Oone(tc_RealDef_Oreal) = c_Transcendental_Ocos(sF7),
    inference(backward_demodulation,[],[f633,f1420]) ).

fof(f1598,plain,
    c_HOL_Oone__class_Oone(tc_RealDef_Oreal) != sF7,
    inference(backward_demodulation,[],[f783,f1420]) ).

fof(f1613,plain,
    ! [X0] : sF7 = c_HOL_Ominus__class_Ominus(X0,X0,tc_RealDef_Oreal),
    inference(backward_demodulation,[],[f1414,f1420]) ).

fof(f1618,plain,
    c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(sF2,tc_RealDef_Oreal),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal)),
    inference(forward_demodulation,[],[f1514,f1361]) ).

fof(f1620,plain,
    sF7 = c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF1),tc_RealDef_Oreal),tc_RealDef_Oreal),sF7,tc_RealDef_Oreal)),
    inference(forward_demodulation,[],[f1512,f1420]) ).

fof(f1632,plain,
    ! [X0,X1] : c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(sF2,tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(sF2,tc_RealDef_Oreal),tc_RealDef_Oreal),X0,tc_RealDef_Oreal)),c_Transcendental_Ocos(X1),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(X0),c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(sF2,tc_RealDef_Oreal),tc_RealDef_Oreal),X1,tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(forward_demodulation,[],[f1499,f1361]) ).

fof(f1633,plain,
    ! [X0,X1] : c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(sF2,tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(X1),c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(sF2,tc_RealDef_Oreal),tc_RealDef_Oreal),X0,tc_RealDef_Oreal)),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(sF2,tc_RealDef_Oreal),tc_RealDef_Oreal),X1,tc_RealDef_Oreal)),c_Transcendental_Ocos(X0),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(forward_demodulation,[],[f1498,f1361]) ).

fof(f1653,plain,
    ! [X0,X1] : c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal)) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(X0),c_Transcendental_Ocos(X1),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(sF2,tc_RealDef_Oreal),tc_RealDef_Oreal),X0,tc_RealDef_Oreal)),c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(sF2,tc_RealDef_Oreal),tc_RealDef_Oreal),X1,tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(forward_demodulation,[],[f1478,f1361]) ).

fof(f1654,plain,
    ! [X0,X1] : c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal)) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(X1),c_Transcendental_Ocos(X0),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(sF2,tc_RealDef_Oreal),tc_RealDef_Oreal),X1,tc_RealDef_Oreal)),c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(sF2,tc_RealDef_Oreal),tc_RealDef_Oreal),X0,tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(forward_demodulation,[],[f1477,f1361]) ).

fof(f1655,plain,
    ! [X0,X1] : c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(X0,X1,tc_RealDef_Oreal)) = c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(X0),c_Transcendental_Ocos(X1),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(sF2,tc_RealDef_Oreal),tc_RealDef_Oreal),X0,tc_RealDef_Oreal)),c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(sF2,tc_RealDef_Oreal),tc_RealDef_Oreal),X1,tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(forward_demodulation,[],[f1476,f1361]) ).

fof(f1656,plain,
    ! [X0] : c_Transcendental_Ocos(X0) = c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(sF2,tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(sF2,tc_RealDef_Oreal),tc_RealDef_Oreal),X0,tc_RealDef_Oreal),tc_RealDef_Oreal)),
    inference(forward_demodulation,[],[f1475,f1361]) ).

fof(f1658,plain,
    c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_Transcendental_Ocos(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(sF2,tc_RealDef_Oreal),tc_RealDef_Oreal)),
    inference(forward_demodulation,[],[f1471,f1361]) ).

fof(f1721,plain,
    ! [X0] : c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(X0,c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(sF2,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(sF2,tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal),tc_RealDef_Oreal)),
    inference(forward_demodulation,[],[f1532,f1361]) ).

fof(f1724,plain,
    ! [X0] : c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(X0,c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(sF2,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(sF2,tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Ominus__class_Ominus(X0,c_Transcendental_Opi,tc_RealDef_Oreal),tc_RealDef_Oreal)),
    inference(forward_demodulation,[],[f1535,f1361]) ).

fof(f1729,plain,
    sF7 = c_HOL_Otimes__class_Otimes(sF7,c_HOL_Oplus__class_Oplus(sF7,sF7,tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(forward_demodulation,[],[f1542,f1420]) ).

fof(f1761,plain,
    c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,sF3,tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal)),
    inference(forward_demodulation,[],[f1618,f1363]) ).

fof(f1763,plain,
    sF7 = c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(sF2,tc_RealDef_Oreal),tc_RealDef_Oreal),sF7,tc_RealDef_Oreal)),
    inference(forward_demodulation,[],[f1620,f1361]) ).

fof(f1775,plain,
    ! [X0,X1] : c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,sF3,tc_RealDef_Oreal),c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,sF3,tc_RealDef_Oreal),X0,tc_RealDef_Oreal)),c_Transcendental_Ocos(X1),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(X0),c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,sF3,tc_RealDef_Oreal),X1,tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(forward_demodulation,[],[f1632,f1363]) ).

fof(f1776,plain,
    ! [X0,X1] : c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,sF3,tc_RealDef_Oreal),c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(X1),c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,sF3,tc_RealDef_Oreal),X0,tc_RealDef_Oreal)),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,sF3,tc_RealDef_Oreal),X1,tc_RealDef_Oreal)),c_Transcendental_Ocos(X0),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(forward_demodulation,[],[f1633,f1363]) ).

fof(f1796,plain,
    ! [X0,X1] : c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal)) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(X0),c_Transcendental_Ocos(X1),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,sF3,tc_RealDef_Oreal),X0,tc_RealDef_Oreal)),c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,sF3,tc_RealDef_Oreal),X1,tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(forward_demodulation,[],[f1653,f1363]) ).

fof(f1797,plain,
    ! [X0,X1] : c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal)) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(X1),c_Transcendental_Ocos(X0),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,sF3,tc_RealDef_Oreal),X1,tc_RealDef_Oreal)),c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,sF3,tc_RealDef_Oreal),X0,tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(forward_demodulation,[],[f1654,f1363]) ).

fof(f1798,plain,
    ! [X0,X1] : c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(X0,X1,tc_RealDef_Oreal)) = c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(X0),c_Transcendental_Ocos(X1),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,sF3,tc_RealDef_Oreal),X0,tc_RealDef_Oreal)),c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,sF3,tc_RealDef_Oreal),X1,tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(forward_demodulation,[],[f1655,f1363]) ).

fof(f1799,plain,
    ! [X0] : c_Transcendental_Ocos(X0) = c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,sF3,tc_RealDef_Oreal),c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,sF3,tc_RealDef_Oreal),X0,tc_RealDef_Oreal),tc_RealDef_Oreal)),
    inference(forward_demodulation,[],[f1656,f1363]) ).

fof(f1801,plain,
    c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_Transcendental_Ocos(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,sF3,tc_RealDef_Oreal)),
    inference(forward_demodulation,[],[f1658,f1363]) ).

fof(f1854,plain,
    ! [X0] : c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(X0,c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,sF3,tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,sF3,tc_RealDef_Oreal),c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal),tc_RealDef_Oreal)),
    inference(forward_demodulation,[],[f1721,f1363]) ).

fof(f1857,plain,
    ! [X0] : c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(X0,c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,sF3,tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,sF3,tc_RealDef_Oreal),c_HOL_Ominus__class_Ominus(X0,c_Transcendental_Opi,tc_RealDef_Oreal),tc_RealDef_Oreal)),
    inference(forward_demodulation,[],[f1724,f1363]) ).

fof(f1874,plain,
    c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,c_Transcendental_Opi,tc_RealDef_Oreal)),
    inference(forward_demodulation,[],[f1761,f1374]) ).

fof(f1876,plain,
    sF7 = c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,sF3,tc_RealDef_Oreal),sF7,tc_RealDef_Oreal)),
    inference(forward_demodulation,[],[f1763,f1363]) ).

fof(f1888,plain,
    ! [X0,X1] : c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,X0,tc_RealDef_Oreal)),c_Transcendental_Ocos(X1),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(X0),c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,X1,tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(forward_demodulation,[],[f1775,f1374]) ).

fof(f1889,plain,
    ! [X0,X1] : c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(X1),c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,X0,tc_RealDef_Oreal)),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,X1,tc_RealDef_Oreal)),c_Transcendental_Ocos(X0),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(forward_demodulation,[],[f1776,f1374]) ).

fof(f1909,plain,
    ! [X0,X1] : c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal)) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(X0),c_Transcendental_Ocos(X1),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,X0,tc_RealDef_Oreal)),c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,X1,tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(forward_demodulation,[],[f1796,f1374]) ).

fof(f1910,plain,
    ! [X0,X1] : c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal)) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(X1),c_Transcendental_Ocos(X0),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,X1,tc_RealDef_Oreal)),c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,X0,tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(forward_demodulation,[],[f1797,f1374]) ).

fof(f1911,plain,
    ! [X0,X1] : c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(X0,X1,tc_RealDef_Oreal)) = c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(X0),c_Transcendental_Ocos(X1),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,X0,tc_RealDef_Oreal)),c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,X1,tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(forward_demodulation,[],[f1798,f1374]) ).

fof(f1912,plain,
    ! [X0] : c_Transcendental_Ocos(X0) = c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,c_HOL_Ominus__class_Ominus(sF8,X0,tc_RealDef_Oreal),tc_RealDef_Oreal)),
    inference(forward_demodulation,[],[f1799,f1374]) ).

fof(f1914,plain,
    c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_Transcendental_Ocos(sF8),
    inference(forward_demodulation,[],[f1801,f1374]) ).

fof(f1954,plain,
    ! [X0] : c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(X0,sF8,tc_RealDef_Oreal)) = c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal),tc_RealDef_Oreal)),
    inference(forward_demodulation,[],[f1854,f1374]) ).

fof(f1957,plain,
    ! [X0] : c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(X0,sF8,tc_RealDef_Oreal)) = c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,c_HOL_Ominus__class_Ominus(X0,c_Transcendental_Opi,tc_RealDef_Oreal),tc_RealDef_Oreal)),
    inference(forward_demodulation,[],[f1857,f1374]) ).

fof(f1967,plain,
    sF7 = c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,c_Transcendental_Opi,tc_RealDef_Oreal)),
    inference(forward_demodulation,[],[f1874,f1420]) ).

fof(f1969,plain,
    sF7 = c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,sF7,tc_RealDef_Oreal)),
    inference(forward_demodulation,[],[f1876,f1374]) ).

fof(f1998,plain,
    sF7 = c_Transcendental_Ocos(sF8),
    inference(forward_demodulation,[],[f1914,f1420]) ).

fof(f2643,plain,
    c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,sF7,tc_RealDef_Oreal)) = c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(c_Transcendental_Opi,sF8,tc_RealDef_Oreal)),
    inference(superposition,[],[f1957,f1613]) ).

fof(f2655,plain,
    sF7 = c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(c_Transcendental_Opi,sF8,tc_RealDef_Oreal)),
    inference(forward_demodulation,[],[f2643,f1969]) ).

fof(f2668,plain,
    c_Transcendental_Ocos(sF6) = c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,sF9,tc_RealDef_Oreal)),
    inference(superposition,[],[f1912,f1376]) ).

fof(f2686,plain,
    sF7 = c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,sF9,tc_RealDef_Oreal)),
    inference(forward_demodulation,[],[f2668,f1371]) ).

fof(f2810,plain,
    ! [X0] : c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(X0,sF6,tc_RealDef_Oreal)) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(sF6),c_Transcendental_Ocos(X0),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(sF9),c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,X0,tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(superposition,[],[f1910,f1376]) ).

fof(f2829,plain,
    ! [X0] : c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(X0,sF9,tc_RealDef_Oreal)) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(sF9),c_Transcendental_Ocos(X0),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(sF7,c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,X0,tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(superposition,[],[f1910,f2686]) ).

fof(f2868,plain,
    ! [X0] : c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(X0,sF9,tc_RealDef_Oreal)) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(sF7,c_Transcendental_Ocos(X0),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(sF7,c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,X0,tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(forward_demodulation,[],[f2829,f1517]) ).

fof(f2877,plain,
    ! [X0] : c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(X0,sF6,tc_RealDef_Oreal)) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(sF6),c_Transcendental_Ocos(X0),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(sF7,c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,X0,tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(forward_demodulation,[],[f2810,f1517]) ).

fof(f2955,plain,
    ! [X0] : c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(X0,sF6,tc_RealDef_Oreal)) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(sF7,c_Transcendental_Ocos(X0),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(sF7,c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,X0,tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(forward_demodulation,[],[f2877,f1371]) ).

fof(f2998,plain,
    ! [X0] : c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(X0,sF6,tc_RealDef_Oreal)) = c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(X0,sF9,tc_RealDef_Oreal)),
    inference(forward_demodulation,[],[f2955,f2868]) ).

fof(f3177,plain,
    ! [X0] : c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(X0,sF9,tc_RealDef_Oreal)) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(X0),sF7,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,X0,tc_RealDef_Oreal)),c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,sF9,tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(superposition,[],[f1909,f1517]) ).

fof(f3239,plain,
    ! [X0] : c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(X0,sF9,tc_RealDef_Oreal)) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(X0),sF7,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,X0,tc_RealDef_Oreal)),sF7,tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(forward_demodulation,[],[f3177,f2686]) ).

fof(f3296,plain,
    ! [X0] : c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(X0,sF9,tc_RealDef_Oreal)) = c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(c_Transcendental_Ocos(X0),c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,X0,tc_RealDef_Oreal)),tc_RealDef_Oreal),sF7,tc_RealDef_Oreal),
    inference(forward_demodulation,[],[f3239,f806]) ).

fof(f3329,plain,
    ! [X0] : c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(X0,sF9,tc_RealDef_Oreal)) = c_HOL_Otimes__class_Otimes(sF7,c_HOL_Oplus__class_Oplus(c_Transcendental_Ocos(X0),c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,X0,tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(forward_demodulation,[],[f3296,f1111]) ).

fof(f3630,plain,
    ! [X0,X1] : c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(X1,c_HOL_Ominus__class_Ominus(sF8,c_HOL_Ominus__class_Ominus(sF8,X0,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(X1),c_Transcendental_Ocos(X0),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,X1,tc_RealDef_Oreal)),c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,c_HOL_Ominus__class_Ominus(sF8,c_HOL_Ominus__class_Ominus(sF8,X0,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(superposition,[],[f1911,f1912]) ).

fof(f3660,plain,
    ! [X0,X1] : c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal),X1,tc_RealDef_Oreal)) = c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal)),c_Transcendental_Ocos(X1),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(X0,sF8,tc_RealDef_Oreal)),c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,X1,tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(superposition,[],[f1911,f1954]) ).

fof(f3661,plain,
    ! [X0] : c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(c_Transcendental_Opi,X0,tc_RealDef_Oreal)) = c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(c_Transcendental_Opi),c_Transcendental_Ocos(X0),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(sF7,c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,X0,tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(superposition,[],[f1911,f1967]) ).

fof(f3669,plain,
    ! [X0] : c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(sF9,X0,tc_RealDef_Oreal)) = c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(sF9),c_Transcendental_Ocos(X0),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(sF7,c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,X0,tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(superposition,[],[f1911,f2686]) ).

fof(f3671,plain,
    ! [X0] : c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(sF6,X0,tc_RealDef_Oreal)) = c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(sF6),c_Transcendental_Ocos(X0),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,sF9,tc_RealDef_Oreal)),c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,X0,tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(superposition,[],[f1911,f2998]) ).

fof(f3680,plain,
    ! [X0,X1] : c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(X1),c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,X0,tc_RealDef_Oreal)),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,X1,tc_RealDef_Oreal)),c_Transcendental_Ocos(X0),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(X1,c_HOL_Ominus__class_Ominus(sF8,X0,tc_RealDef_Oreal),tc_RealDef_Oreal)),
    inference(superposition,[],[f1911,f1912]) ).

fof(f3710,plain,
    ! [X0,X1] : c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(X1,c_HOL_Ominus__class_Ominus(sF8,X0,tc_RealDef_Oreal),tc_RealDef_Oreal)),
    inference(forward_demodulation,[],[f3680,f1889]) ).

fof(f3715,plain,
    ! [X0] : c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(sF6,X0,tc_RealDef_Oreal)) = c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(sF6),c_Transcendental_Ocos(X0),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(sF7,c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,X0,tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(forward_demodulation,[],[f3671,f2686]) ).

fof(f3717,plain,
    ! [X0] : c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(sF9,X0,tc_RealDef_Oreal)) = c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(sF7,c_Transcendental_Ocos(X0),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(sF7,c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,X0,tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(forward_demodulation,[],[f3669,f1517]) ).

fof(f3720,plain,
    ! [X0,X1] : c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal),X1,tc_RealDef_Oreal)) = c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(X0),c_Transcendental_Ocos(X1),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(X0,sF8,tc_RealDef_Oreal)),c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,X1,tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(forward_demodulation,[],[f3660,f822]) ).

fof(f3744,plain,
    ! [X0,X1] : c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(X1,c_HOL_Ominus__class_Ominus(sF8,c_HOL_Ominus__class_Ominus(sF8,X0,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(X1),c_Transcendental_Ocos(X0),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,X1,tc_RealDef_Oreal)),c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,X0,tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(forward_demodulation,[],[f3630,f1912]) ).

fof(f3780,plain,
    ! [X0] : c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(sF6,X0,tc_RealDef_Oreal)) = c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(sF7,c_Transcendental_Ocos(X0),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(sF7,c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,X0,tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(forward_demodulation,[],[f3715,f1371]) ).

fof(f3806,plain,
    ! [X0,X1] : c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(X1,X0,tc_RealDef_Oreal)) = c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(X1,c_HOL_Ominus__class_Ominus(sF8,c_HOL_Ominus__class_Ominus(sF8,X0,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)),
    inference(forward_demodulation,[],[f3744,f1911]) ).

fof(f3836,plain,
    ! [X0] : c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(sF6,X0,tc_RealDef_Oreal)) = c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(sF9,X0,tc_RealDef_Oreal)),
    inference(forward_demodulation,[],[f3780,f3717]) ).

fof(f3851,plain,
    ! [X0,X1] : c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(X1,X0,tc_RealDef_Oreal)) = c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(sF8,X0,tc_RealDef_Oreal),X1,tc_RealDef_Oreal),tc_RealDef_Oreal)),
    inference(forward_demodulation,[],[f3806,f3710]) ).

fof(f4452,plain,
    ! [X0,X1] : c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(sF8,c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal),tc_RealDef_Oreal),X1,tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,c_HOL_Ominus__class_Ominus(sF8,c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)),c_Transcendental_Ocos(X1),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(X0,sF8,tc_RealDef_Oreal)),c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,X1,tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(superposition,[],[f1888,f1954]) ).

fof(f4453,plain,
    ! [X0] : c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(sF8,c_Transcendental_Opi,tc_RealDef_Oreal),X0,tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,c_HOL_Ominus__class_Ominus(sF8,c_Transcendental_Opi,tc_RealDef_Oreal),tc_RealDef_Oreal)),c_Transcendental_Ocos(X0),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(sF7,c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,X0,tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(superposition,[],[f1888,f1967]) ).

fof(f4471,plain,
    ! [X0] : c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,c_HOL_Ominus__class_Ominus(sF6,X0,tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,sF6,tc_RealDef_Oreal)),c_Transcendental_Ocos(X0),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(sF7,c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,X0,tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(superposition,[],[f1888,f1371]) ).

fof(f4482,plain,
    ! [X0] : c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,c_HOL_Ominus__class_Ominus(X0,c_Transcendental_Opi,tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,X0,tc_RealDef_Oreal)),c_Transcendental_Ocos(c_Transcendental_Opi),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(X0),sF7,tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(superposition,[],[f1888,f1967]) ).

fof(f4512,plain,
    ! [X0] : c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,c_HOL_Ominus__class_Ominus(X0,c_Transcendental_Opi,tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(c_Transcendental_Opi),c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,X0,tc_RealDef_Oreal)),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(X0),sF7,tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(forward_demodulation,[],[f4482,f1111]) ).

fof(f4519,plain,
    ! [X0] : c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,c_HOL_Ominus__class_Ominus(sF6,X0,tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,sF9,tc_RealDef_Oreal)),c_Transcendental_Ocos(X0),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(sF7,c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,X0,tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(forward_demodulation,[],[f4471,f2998]) ).

fof(f4536,plain,
    ! [X0] : c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(c_Transcendental_Opi),c_Transcendental_Ocos(X0),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(sF7,c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,X0,tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(sF8,c_Transcendental_Opi,tc_RealDef_Oreal),X0,tc_RealDef_Oreal),tc_RealDef_Oreal)),
    inference(forward_demodulation,[],[f4453,f1912]) ).

fof(f4537,plain,
    ! [X0,X1] : c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal)),c_Transcendental_Ocos(X1),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(X0,sF8,tc_RealDef_Oreal)),c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,X1,tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(sF8,c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal),tc_RealDef_Oreal),X1,tc_RealDef_Oreal),tc_RealDef_Oreal)),
    inference(forward_demodulation,[],[f4452,f1912]) ).

fof(f4589,plain,
    ! [X0] : c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(X0,sF8,tc_RealDef_Oreal)) = c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(c_Transcendental_Opi),c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,X0,tc_RealDef_Oreal)),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(X0),sF7,tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(forward_demodulation,[],[f4512,f1957]) ).

fof(f4595,plain,
    ! [X0] : c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,c_HOL_Ominus__class_Ominus(sF6,X0,tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(sF7,c_Transcendental_Ocos(X0),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(sF7,c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,X0,tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(forward_demodulation,[],[f4519,f2686]) ).

fof(f4610,plain,
    ! [X0] : c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(X0,c_Transcendental_Opi,tc_RealDef_Oreal)) = c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(c_Transcendental_Opi),c_Transcendental_Ocos(X0),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(sF7,c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,X0,tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(forward_demodulation,[],[f4536,f3851]) ).

fof(f4611,plain,
    ! [X0,X1] : c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(X1,c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal)),c_Transcendental_Ocos(X1),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(X0,sF8,tc_RealDef_Oreal)),c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,X1,tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(forward_demodulation,[],[f4537,f3851]) ).

fof(f4653,plain,
    ! [X0] : c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,c_HOL_Ominus__class_Ominus(sF6,X0,tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(sF9,X0,tc_RealDef_Oreal)),
    inference(forward_demodulation,[],[f4595,f3717]) ).

fof(f4662,plain,
    ! [X0] : c_HOL_Ouminus__class_Ouminus(c_Transcendental_Ocos(X0),tc_RealDef_Oreal) = c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(c_Transcendental_Opi),c_Transcendental_Ocos(X0),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(sF7,c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,X0,tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(forward_demodulation,[],[f4610,f820]) ).

fof(f4663,plain,
    ! [X0,X1] : c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(X1,c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(X0),c_Transcendental_Ocos(X1),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(X0,sF8,tc_RealDef_Oreal)),c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,X1,tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(forward_demodulation,[],[f4611,f822]) ).

fof(f4711,plain,
    ! [X0] : c_HOL_Ouminus__class_Ouminus(c_Transcendental_Ocos(X0),tc_RealDef_Oreal) = c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(c_Transcendental_Opi,X0,tc_RealDef_Oreal)),
    inference(backward_demodulation,[],[f3661,f4662]) ).

fof(f4712,plain,
    ! [X0,X1] : c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(X1,X0,tc_RealDef_Oreal)) = c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(X0),c_Transcendental_Ocos(X1),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(X0,sF8,tc_RealDef_Oreal)),c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,X1,tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(forward_demodulation,[],[f4663,f96]) ).

fof(f4761,plain,
    sF7 = c_HOL_Ouminus__class_Ouminus(c_Transcendental_Ocos(sF8),tc_RealDef_Oreal),
    inference(backward_demodulation,[],[f2655,f4711]) ).

fof(f4762,plain,
    ! [X0,X1] : c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(X1,X0,tc_RealDef_Oreal)) = c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal),X1,tc_RealDef_Oreal)),
    inference(backward_demodulation,[],[f3720,f4712]) ).

fof(f4810,plain,
    sF7 = c_HOL_Ouminus__class_Ouminus(sF7,tc_RealDef_Oreal),
    inference(forward_demodulation,[],[f4761,f1998]) ).

fof(f5019,plain,
    ! [X0] : c_HOL_Ominus__class_Ominus(X0,sF7,tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(X0,sF7,tc_RealDef_Oreal),
    inference(superposition,[],[f96,f4810]) ).

fof(f5034,plain,
    sF7 = c_HOL_Otimes__class_Otimes(sF7,c_HOL_Ominus__class_Ominus(sF7,sF7,tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(backward_demodulation,[],[f1729,f5019]) ).

fof(f5035,plain,
    sF7 = c_HOL_Otimes__class_Otimes(sF7,sF7,tc_RealDef_Oreal),
    inference(forward_demodulation,[],[f5034,f1613]) ).

fof(f5464,plain,
    c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(sF6,sF8,tc_RealDef_Oreal)) = c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(sF9,c_Transcendental_Opi,tc_RealDef_Oreal)),
    inference(superposition,[],[f1957,f4653]) ).

fof(f5510,plain,
    c_HOL_Ouminus__class_Ouminus(c_Transcendental_Ocos(sF9),tc_RealDef_Oreal) = c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(sF6,sF8,tc_RealDef_Oreal)),
    inference(forward_demodulation,[],[f5464,f820]) ).

fof(f5525,plain,
    c_HOL_Ouminus__class_Ouminus(c_Transcendental_Ocos(sF9),tc_RealDef_Oreal) = c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(sF9,sF8,tc_RealDef_Oreal)),
    inference(forward_demodulation,[],[f5510,f3836]) ).

fof(f5532,plain,
    c_HOL_Ouminus__class_Ouminus(sF7,tc_RealDef_Oreal) = c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(sF9,sF8,tc_RealDef_Oreal)),
    inference(forward_demodulation,[],[f5525,f1517]) ).

fof(f5538,plain,
    sF7 = c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(sF9,sF8,tc_RealDef_Oreal)),
    inference(forward_demodulation,[],[f5532,f4810]) ).

fof(f5769,plain,
    ! [X0] : c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal),sF8,tc_RealDef_Oreal)) = c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(c_Transcendental_Opi),c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(X0,sF8,tc_RealDef_Oreal)),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal)),sF7,tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(superposition,[],[f4589,f1954]) ).

fof(f5884,plain,
    ! [X0] : c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal),sF8,tc_RealDef_Oreal)) = c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(c_Transcendental_Opi),c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(X0,sF8,tc_RealDef_Oreal)),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(sF7,c_Transcendental_Ocos(c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(forward_demodulation,[],[f5769,f1111]) ).

fof(f5938,plain,
    ! [X0] : c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal),sF8,tc_RealDef_Oreal)) = c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(c_Transcendental_Opi),c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(X0,sF8,tc_RealDef_Oreal)),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(sF7,c_Transcendental_Ocos(X0),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(forward_demodulation,[],[f5884,f822]) ).

fof(f5981,plain,
    ! [X0] : c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,X0,tc_RealDef_Oreal)) = c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(c_Transcendental_Opi),c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(X0,sF8,tc_RealDef_Oreal)),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(sF7,c_Transcendental_Ocos(X0),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(forward_demodulation,[],[f5938,f4762]) ).

fof(f6608,plain,
    ! [X0] : c_HOL_Ouminus__class_Ouminus(c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(X0,sF8,tc_RealDef_Oreal)),tc_RealDef_Oreal) = c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(c_Transcendental_Opi),c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(X0,sF8,tc_RealDef_Oreal)),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(sF7,c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,c_HOL_Ominus__class_Ominus(sF8,c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(superposition,[],[f4662,f1954]) ).

fof(f6708,plain,
    ! [X0] : c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(c_Transcendental_Opi),c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(X0,sF8,tc_RealDef_Oreal)),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(sF7,c_Transcendental_Ocos(c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Ouminus__class_Ouminus(c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(X0,sF8,tc_RealDef_Oreal)),tc_RealDef_Oreal),
    inference(forward_demodulation,[],[f6608,f1912]) ).

fof(f6754,plain,
    ! [X0] : c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(c_Transcendental_Opi),c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(X0,sF8,tc_RealDef_Oreal)),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(sF7,c_Transcendental_Ocos(X0),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Ouminus__class_Ouminus(c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(X0,sF8,tc_RealDef_Oreal)),tc_RealDef_Oreal),
    inference(forward_demodulation,[],[f6708,f822]) ).

fof(f6783,plain,
    ! [X0] : c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,X0,tc_RealDef_Oreal)) = c_HOL_Ouminus__class_Ouminus(c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(X0,sF8,tc_RealDef_Oreal)),tc_RealDef_Oreal),
    inference(forward_demodulation,[],[f6754,f5981]) ).

fof(f6829,plain,
    ! [X0,X1] : c_HOL_Ominus__class_Ominus(X1,c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(X0,sF8,tc_RealDef_Oreal)),tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(X1,c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF8,X0,tc_RealDef_Oreal)),tc_RealDef_Oreal),
    inference(superposition,[],[f96,f6783]) ).

fof(f6836,plain,
    ! [X0] : c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(X0,sF9,tc_RealDef_Oreal)) = c_HOL_Otimes__class_Otimes(sF7,c_HOL_Ominus__class_Ominus(c_Transcendental_Ocos(X0),c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(X0,sF8,tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(backward_demodulation,[],[f3329,f6829]) ).

fof(f6902,plain,
    c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF9,sF9,tc_RealDef_Oreal)) = c_HOL_Otimes__class_Otimes(sF7,c_HOL_Ominus__class_Ominus(c_Transcendental_Ocos(sF9),sF7,tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(superposition,[],[f6836,f5538]) ).

fof(f6903,plain,
    c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF9,sF9,tc_RealDef_Oreal)) = c_HOL_Otimes__class_Otimes(sF7,c_HOL_Ominus__class_Ominus(sF7,sF7,tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(forward_demodulation,[],[f6902,f1517]) ).

fof(f6951,plain,
    c_HOL_Otimes__class_Otimes(sF7,sF7,tc_RealDef_Oreal) = c_Transcendental_Ocos(c_HOL_Ominus__class_Ominus(sF9,sF9,tc_RealDef_Oreal)),
    inference(forward_demodulation,[],[f6903,f1613]) ).

fof(f6995,plain,
    c_HOL_Otimes__class_Otimes(sF7,sF7,tc_RealDef_Oreal) = c_Transcendental_Ocos(sF7),
    inference(forward_demodulation,[],[f6951,f1613]) ).

fof(f7025,plain,
    c_HOL_Oone__class_Oone(tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(sF7,sF7,tc_RealDef_Oreal),
    inference(forward_demodulation,[],[f6995,f1595]) ).

fof(f7041,plain,
    c_HOL_Oone__class_Oone(tc_RealDef_Oreal) = sF7,
    inference(forward_demodulation,[],[f7025,f5035]) ).

fof(f7055,plain,
    $false,
    inference(forward_subsumption_resolution,[],[f7041,f1598]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04  % Problem  : SWV602-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.07  % Command  : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.27  % Computer : n003.cluster.edu
% 0.10/0.27  % Model    : x86_64 x86_64
% 0.10/0.27  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.27  % Memory   : 8046.5625MB
% 0.10/0.27  % OS       : Linux 6.8.0-71-generic
% 0.10/0.27  % CPULimit : 300
% 0.10/0.27  % WCLimit  : 300
% 0.10/0.27  % DateTime : Mon Sep 28 12:02:42 UTC 2026
% 0.10/0.28  % CPUTime  : 
% 0.10/0.28  Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.27/0.33  Running first-order theorem proving
% 0.27/0.33  Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 17.06/3.12  % (1537343)Input is clausal, will run a generic CNF schedule.
% 17.06/3.12  % (1537366)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=2320841383:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 17.06/3.12  % (1537370)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2480068809:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 17.06/3.12  % (1537372)dis-21_1_sil=8000:lcm=predicate:random_seed=82480084:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 17.06/3.12  % (1537369)lrs+10_1_sil=8000:sp=occurrence:random_seed=1751251381:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 17.06/3.12  % (1537367)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1883035886:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 17.06/3.12  % (1537371)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3758240170:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 17.06/3.12  % (1537368)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=365405009:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 17.06/3.12  % (1537370)Instruction limit reached! 
% 17.06/3.12  % (1537370)------------------------------
% 17.06/3.12  % (1537370)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.06/3.12  % (1537370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.06/3.12  % (1537370)CaDiCaL version: 2.1.3
% 17.06/3.12  % (1537370)Termination reason: Instruction limit
% 17.06/3.12  % (1537370)Termination phase: Saturation
% 17.06/3.12  % (1537370)Time elapsed: 0.079 s
% 17.06/3.12  % (1537370)Peak memory usage: 90 MB
% 17.06/3.12  % (1537370)Instructions burned: 114 (million)
% 17.06/3.12  % (1537372)Instruction limit reached! 
% 17.06/3.12  % (1537372)------------------------------
% 17.06/3.12  % (1537372)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.06/3.12  % (1537372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.06/3.12  % (1537372)CaDiCaL version: 2.1.3
% 17.06/3.12  % (1537372)Termination reason: Instruction limit
% 17.06/3.12  % (1537372)Termination phase: Saturation
% 17.06/3.12  % (1537372)Time elapsed: 0.111 s
% 17.06/3.12  % (1537372)Peak memory usage: 89 MB
% 17.06/3.12  % (1537372)Instructions burned: 117 (million)
% 17.06/3.12  % (1537369)Instruction limit reached! 
% 17.06/3.12  % (1537369)------------------------------
% 17.06/3.12  % (1537369)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.06/3.12  % (1537369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.06/3.12  % (1537369)CaDiCaL version: 2.1.3
% 17.06/3.12  % (1537369)Termination reason: Instruction limit
% 17.06/3.12  % (1537369)Termination phase: Saturation
% 17.06/3.12  % (1537369)Time elapsed: 0.115 s
% 17.06/3.12  % (1537369)Peak memory usage: 90 MB
% 17.06/3.12  % (1537369)Instructions burned: 107 (million)
% 17.06/3.12  % (1537371)Instruction limit reached! 
% 17.06/3.12  % (1537371)------------------------------
% 17.06/3.12  % (1537371)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.06/3.12  % (1537371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.06/3.12  % (1537371)CaDiCaL version: 2.1.3
% 17.06/3.12  % (1537371)Termination reason: Instruction limit
% 17.06/3.12  % (1537371)Termination phase: Saturation
% 17.06/3.12  % (1537371)Time elapsed: 0.172 s
% 17.06/3.12  % (1537371)Peak memory usage: 90 MB
% 17.06/3.12  % (1537371)Instructions burned: 180 (million)
% 17.06/3.12  % (1537384)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=1517768913:i=143:sd=2:aac=none:ss=axioms:sgt=16_2996 on theBenchmark for (2996ds/143Mi)
% 17.06/3.12  % (1537385)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3360279954:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2996 on theBenchmark for (2996ds/189Mi)
% 17.06/3.12  % (1537386)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3201981465:st=4:i=219:sd=3:ss=axioms_2996 on theBenchmark for (2996ds/219Mi)
% 17.06/3.12  % (1537387)lrs+10_64_to=lpo:sil=8000:random_seed=3740624842:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 17.06/3.12  % (1537384)Instruction limit reached! 
% 14.61/3.64  % (1537384)------------------------------
% 14.61/3.64  % (1537384)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.61/3.64  % (1537384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.61/3.64  % (1537384)CaDiCaL version: 2.1.3
% 14.61/3.64  % (1537384)Termination reason: Instruction limit
% 14.61/3.64  % (1537384)Termination phase: Saturation
% 14.61/3.64  % (1537384)Time elapsed: 0.137 s
% 14.61/3.64  % (1537384)Peak memory usage: 90 MB
% 14.61/3.64  % (1537384)Instructions burned: 145 (million)
% 14.61/3.64  % (1537385)Instruction limit reached! 
% 14.61/3.64  % (1537385)------------------------------
% 14.61/3.64  % (1537385)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.61/3.64  % (1537385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.61/3.64  % (1537385)CaDiCaL version: 2.1.3
% 14.61/3.64  % (1537385)Termination reason: Instruction limit
% 14.61/3.64  % (1537385)Termination phase: Saturation
% 14.61/3.64  % (1537385)Time elapsed: 0.180 s
% 14.61/3.64  % (1537385)Peak memory usage: 91 MB
% 14.61/3.64  % (1537385)Instructions burned: 189 (million)
% 14.61/3.64  % (1537387)Instruction limit reached! 
% 14.61/3.64  % (1537387)------------------------------
% 14.61/3.64  % (1537387)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.61/3.64  % (1537387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.61/3.64  % (1537387)CaDiCaL version: 2.1.3
% 14.61/3.64  % (1537387)Termination reason: Instruction limit
% 14.61/3.64  % (1537387)Termination phase: Saturation
% 14.61/3.64  % (1537387)Time elapsed: 0.127 s
% 14.61/3.64  % (1537387)Peak memory usage: 90 MB
% 14.61/3.64  % (1537387)Instructions burned: 126 (million)
% 14.61/3.64  % (1537386)Instruction limit reached! 
% 14.61/3.64  % (1537386)------------------------------
% 14.61/3.64  % (1537386)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.61/3.64  % (1537386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.61/3.64  % (1537386)CaDiCaL version: 2.1.3
% 14.61/3.64  % (1537386)Termination reason: Instruction limit
% 14.61/3.64  % (1537386)Termination phase: Saturation
% 14.61/3.64  % (1537386)Time elapsed: 0.198 s
% 14.61/3.64  % (1537386)Peak memory usage: 91 MB
% 14.61/3.64  % (1537386)Instructions burned: 219 (million)
% 14.61/3.64  % (1537394)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=4040456158:avsq=on:i=194:fgj=on:bd=preordered_2993 on theBenchmark for (2993ds/194Mi)
% 14.61/3.64  % (1537395)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=4251061597:i=157:gtg=all_2992 on theBenchmark for (2992ds/157Mi)
% 14.61/3.64  % (1537396)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1741553454:i=3394:sd=4:ss=included:sgt=64_2992 on theBenchmark for (2992ds/3394Mi)
% 14.61/3.64  % (1537397)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=4223150858:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2992 on theBenchmark for (2992ds/106Mi)
% 14.61/3.64  % (1537394)Instruction limit reached! 
% 14.61/3.64  % (1537394)------------------------------
% 14.61/3.64  % (1537394)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.61/3.64  % (1537394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.61/3.64  % (1537394)CaDiCaL version: 2.1.3
% 14.61/3.64  % (1537394)Termination reason: Instruction limit
% 14.61/3.64  % (1537394)Termination phase: Saturation
% 14.61/3.64  % (1537394)Time elapsed: 0.185 s
% 14.61/3.64  % (1537394)Peak memory usage: 91 MB
% 14.61/3.64  % (1537394)Instructions burned: 194 (million)
% 14.61/3.64  % (1537395)Instruction limit reached! 
% 14.61/3.64  % (1537395)------------------------------
% 14.61/3.64  % (1537395)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.61/3.64  % (1537395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.61/3.64  % (1537395)CaDiCaL version: 2.1.3
% 14.61/3.64  % (1537395)Termination reason: Instruction limit
% 14.61/3.64  % (1537395)Termination phase: Saturation
% 14.61/3.64  % (1537395)Time elapsed: 0.166 s
% 14.61/3.64  % (1537395)Peak memory usage: 91 MB
% 14.61/3.64  % (1537395)Instructions burned: 157 (million)
% 14.61/3.64  % (1537397)Instruction limit reached! 
% 14.61/3.64  % (1537397)------------------------------
% 14.61/3.64  % (1537397)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.61/3.64  % (1537397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.61/3.64  % (1537397)CaDiCaL version: 2.1.3
% 14.61/3.64  % (1537397)Termination reason: Instruction limit
% 14.61/3.64  % (1537397)Termination phase: Saturation
% 14.61/3.64  % (1537397)Time elapsed: 0.089 s
% 14.61/3.64  % (1537397)Peak memory usage: 89 MB
% 14.61/3.64  % (1537397)Instructions burned: 107 (million)
% 14.61/3.64  % (1537403)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3801225392:i=107_2989 on theBenchmark for (2989ds/107Mi)
% 14.61/3.64  % (1537405)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3226456186:cond=fast:i=5208:av=off_2989 on theBenchmark for (2989ds/5208Mi)
% 14.61/3.64  % (1537404)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1467790278:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2989 on theBenchmark for (2989ds/242Mi)
% 14.61/3.64  % (1537403)Instruction limit reached! 
% 14.61/3.64  % (1537403)------------------------------
% 14.61/3.64  % (1537403)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.61/3.64  % (1537403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.61/3.64  % (1537403)CaDiCaL version: 2.1.3
% 14.61/3.64  % (1537403)Termination reason: Instruction limit
% 14.61/3.64  % (1537403)Termination phase: Saturation
% 14.61/3.64  % (1537403)Time elapsed: 0.104 s
% 14.61/3.64  % (1537403)Peak memory usage: 90 MB
% 14.61/3.64  % (1537403)Instructions burned: 108 (million)
% 14.61/3.64  % (1537404)Instruction limit reached! 
% 14.61/3.64  % (1537404)------------------------------
% 14.61/3.64  % (1537404)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.61/3.64  % (1537404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.61/3.64  % (1537404)CaDiCaL version: 2.1.3
% 14.61/3.64  % (1537404)Termination reason: Instruction limit
% 14.61/3.64  % (1537404)Termination phase: Saturation
% 14.61/3.64  % (1537404)Time elapsed: 0.243 s
% 14.61/3.64  % (1537404)Peak memory usage: 90 MB
% 14.61/3.64  % (1537404)Instructions burned: 242 (million)
% 14.61/3.64  % (1537410)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=788906491:i=134:sd=2:doe=on:ss=axioms:sgt=14_2986 on theBenchmark for (2986ds/134Mi)
% 14.61/3.64  % (1537410)Instruction limit reached! 
% 14.61/3.64  % (1537410)------------------------------
% 14.61/3.64  % (1537410)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.61/3.64  % (1537410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.61/3.64  % (1537410)CaDiCaL version: 2.1.3
% 14.61/3.64  % (1537410)Termination reason: Instruction limit
% 14.61/3.64  % (1537410)Termination phase: Saturation
% 14.61/3.64  % (1537410)Time elapsed: 0.115 s
% 14.61/3.64  % (1537410)Peak memory usage: 90 MB
% 14.61/3.64  % (1537410)Instructions burned: 134 (million)
% 14.61/3.64  % (1537411)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=3153666582:i=499:bd=all_2984 on theBenchmark for (2984ds/499Mi)
% 14.61/3.64  % (1537413)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1702583012:i=191:fgj=on:bd=all_2982 on theBenchmark for (2982ds/191Mi)
% 14.61/3.64  % (1537413)Instruction limit reached! 
% 14.61/3.64  % (1537413)------------------------------
% 14.61/3.64  % (1537413)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.61/3.64  % (1537413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.61/3.64  % (1537413)CaDiCaL version: 2.1.3
% 14.61/3.64  % (1537413)Termination reason: Instruction limit
% 14.61/3.64  % (1537413)Termination phase: Saturation
% 14.61/3.64  % (1537413)Time elapsed: 0.204 s
% 14.61/3.64  % (1537413)Peak memory usage: 91 MB
% 14.61/3.64  % (1537413)Instructions burned: 191 (million)
% 14.61/3.64  % (1537411)Instruction limit reached! 
% 14.61/3.64  % (1537411)------------------------------
% 14.61/3.64  % (1537411)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.61/3.64  % (1537411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.61/3.64  % (1537411)CaDiCaL version: 2.1.3
% 14.61/3.64  % (1537411)Termination reason: Instruction limit
% 14.61/3.64  % (1537411)Termination phase: Saturation
% 14.61/3.64  % (1537411)Time elapsed: 0.488 s
% 14.61/3.64  % (1537411)Peak memory usage: 95 MB
% 14.61/3.64  % (1537411)Instructions burned: 499 (million)
% 14.61/3.64  % (1537420)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3705044266:i=264:kws=precedence:fsr=off_2978 on theBenchmark for (2978ds/264Mi)
% 14.61/3.64  % (1537421)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=1443066304:cond=on:i=156:bs=on:gtg=exists_all:er=known_2977 on theBenchmark for (2977ds/156Mi)
% 14.61/3.64  % (1537368)First to succeed.
% 14.61/3.64  % (1537368)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1537343"
% 14.61/3.64  % (1537420)Instruction limit reached! 
% 14.61/3.64  % (1537420)------------------------------
% 14.61/3.64  % (1537420)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.61/3.64  % (1537420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.61/3.64  % (1537420)CaDiCaL version: 2.1.3
% 14.61/3.64  % (1537420)Termination reason: Instruction limit
% 14.61/3.64  % (1537420)Termination phase: Saturation
% 14.61/3.64  % (1537420)Time elapsed: 0.275 s
% 14.61/3.64  % (1537420)Peak memory usage: 92 MB
% 14.61/3.64  % (1537420)Instructions burned: 264 (million)
% 14.61/3.64  % (1537421)Instruction limit reached! 
% 14.61/3.64  % (1537421)------------------------------
% 14.61/3.64  % (1537421)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.61/3.64  % (1537421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.61/3.64  % (1537421)CaDiCaL version: 2.1.3
% 14.61/3.64  % (1537421)Termination reason: Instruction limit
% 14.61/3.64  % (1537421)Termination phase: Saturation
% 14.61/3.64  % (1537421)Time elapsed: 0.157 s
% 14.61/3.64  % (1537421)Peak memory usage: 90 MB
% 14.61/3.64  % (1537421)Instructions burned: 156 (million)
% 14.61/3.64  % (1537366)Also succeeded, but the first one will report.
% 14.61/3.64  % (1537424)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=4231097287:i=3256:kws=precedence:bd=preordered:av=off_2973 on theBenchmark for (2973ds/3256Mi)
% 14.61/3.64  % (1537425)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=758017718:i=537:av=off:ss=included_2973 on theBenchmark for (2973ds/537Mi)
% 14.61/3.64  % (1537368)Refutation found. Thanks to Tanya!
% 14.61/3.64  % SZS status Unsatisfiable for theBenchmark
% 14.61/3.64  % SZS output start Proof for theBenchmark
% See solution above
% 0.31/3.91  % (1537368)------------------------------
% 0.31/3.91  % (1537368)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.31/3.91  % (1537368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.31/3.91  % (1537368)CaDiCaL version: 2.1.3
% 0.31/3.91  % (1537368)Termination reason: Refutation
% 0.31/3.91  % (1537368)Time elapsed: 2.341 s
% 0.31/3.91  % (1537368)Peak memory usage: 143 MB
% 0.31/3.91  % (1537368)Instructions burned: 2338 (million)
% 0.31/3.91  % (1537368)------------------------------
% 0.31/3.91  % (1537368)------------------------------
% 0.31/3.91  % (1537343)Success in time 2.997 s
% 0.31/3.91  % Vampire exiting
%------------------------------------------------------------------------------