FindProof---0.1.UNS-Prf.s

%------------------------------------------------------------------------------
% File     : FindProof---0.1
% Problem  : SWV601-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300

% Computer : n009.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8046.5625MB
% OS       : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Fri Sep 25 03:13:46 PM UTC 2026

% Result   : Unsatisfiable 69.61s 19.45s
% Output   : Proof 69.61s
% Verified : 
% SZS Type : Refutation
%            Derivation depth      :   60
%            Number of leaves      :   68
% Syntax   : Number of formulae    :  543 ( 451 unt;   0 def)
%            Number of atoms       :  683 ( 470 equ)
%            Maximal formula atoms :    4 (   1 avg)
%            Number of connectives :  422 ( 282   ~; 140   |;   0   &)
%                                         (   0 <=>;   0  =>;   0  <=;   0 <~>)
%            Maximal formula depth :    8 (   2 avg)
%            Maximal term depth    :    8 (   2 avg)
%            Number of predicates  :   11 (   9 usr;   1 prp; 0-3 aty)
%            Number of functors    :   31 (  31 usr;  14 con; 0-4 aty)
%            Number of variables   :  462 (  32 sgn 154   !;   0   ?)

% Comments : 
%------------------------------------------------------------------------------
cnf(f717,axiom,
    c_Transcendental_Ocos(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal)) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_cos__two__neq__zero_0) ).

fof(f717_nnf,plain,
    c_Transcendental_Ocos(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal)) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
    inference(nnf_transformation,[status(thm)],[f717]) ).

fof(f717_sk,plain,
    c_Transcendental_Ocos(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal)) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
    inference(skolemisation,[status(esa)],[f717_nnf]) ).

cnf(c717,plain,
    c_Transcendental_Ocos(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal)) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
    inference(cnf_transformation,[status(esa)],[f717_sk]) ).

cnf(t65,plain,
    eq(c_Transcendental_Ocos(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal)),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)) = false,
    inference(equality_encoding,[status(esa)],[c717]) ).

cnf(t238,axiom,
    sF0 = c_Int_OBit1(c_Int_OPls),
    introduced(definition) ).

cnf(t262,plain,
    c_Int_OBit1(c_Int_OPls) = sF0,
    inference(orient,[status(thm)],[t238]) ).

cnf(t15602,plain,
    eq(c_Transcendental_Ocos(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF0),tc_RealDef_Oreal)),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)) = false,
    inference(step,[status(thm)],[t65,t262]) ).

cnf(t239,axiom,
    sF1 = c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),
    introduced(definition) ).

cnf(t15560,plain,
    sF1 = c_Int_OBit0(sF0),
    inference(step,[status(thm)],[t239,t262]) ).

cnf(t270,plain,
    c_Int_OBit0(sF0) = sF1,
    inference(orient,[status(thm)],[t15560]) ).

cnf(t15603,plain,
    eq(c_Transcendental_Ocos(c_Int_Onumber__class_Onumber__of(sF1,tc_RealDef_Oreal)),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)) = false,
    inference(step,[status(thm)],[t15602,t270]) ).

cnf(t240,axiom,
    sF2 = c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),
    introduced(definition) ).

cnf(t15569,plain,
    sF2 = c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF0),tc_RealDef_Oreal),
    inference(step,[status(thm)],[t240,t262]) ).

cnf(t15570,plain,
    sF2 = c_Int_Onumber__class_Onumber__of(sF1,tc_RealDef_Oreal),
    inference(step,[status(thm)],[t15569,t270]) ).

cnf(t306,plain,
    c_Int_Onumber__class_Onumber__of(sF1,tc_RealDef_Oreal) = sF2,
    inference(orient,[status(thm)],[t15570]) ).

cnf(t15604,plain,
    eq(c_Transcendental_Ocos(sF2),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)) = false,
    inference(step,[status(thm)],[t15603,t306]) ).

cnf(f730,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(f730_nnf,plain,
    c_Transcendental_Osin(c_Transcendental_Opi) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
    inference(nnf_transformation,[status(thm)],[f730]) ).

cnf(c730,plain,
    c_Transcendental_Osin(c_Transcendental_Opi) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
    inference(cnf_transformation,[status(esa)],[f730_nnf]) ).

cnf(t14,plain,
    c_Transcendental_Osin(c_Transcendental_Opi) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
    inference(equality_encoding,[status(esa)],[c730]) ).

cnf(t261,plain,
    c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_Transcendental_Osin(c_Transcendental_Opi),
    inference(orient,[status(thm)],[t14]) ).

cnf(t15605,plain,
    eq(c_Transcendental_Ocos(sF2),c_Transcendental_Osin(c_Transcendental_Opi)) = false,
    inference(step,[status(thm)],[t15604,t261]) ).

cnf(t430,plain,
    eq(c_Transcendental_Ocos(sF2),c_Transcendental_Osin(c_Transcendental_Opi)) = false,
    inference(orient,[status(thm)],[t15605]) ).

cnf(f714,axiom,
    c_Transcendental_Osin(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal)) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_sin__two__pi_0) ).

fof(f714_nnf,plain,
    c_Transcendental_Osin(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal)) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
    inference(nnf_transformation,[status(thm)],[f714]) ).

cnf(c714,plain,
    c_Transcendental_Osin(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal)) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
    inference(cnf_transformation,[status(esa)],[f714_nnf]) ).

cnf(t75,plain,
    c_Transcendental_Osin(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal)) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
    inference(equality_encoding,[status(esa)],[c714]) ).

cnf(f867,axiom,
    c_HOL_Otimes__class_Otimes(V_z,V_w,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(V_w,V_z,tc_RealDef_Oreal),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_real__mult__commute_0) ).

fof(f867_nnf,plain,
    ! [V_z,V_w] : c_HOL_Otimes__class_Otimes(V_z,V_w,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(V_w,V_z,tc_RealDef_Oreal),
    inference(nnf_transformation,[status(thm)],[f867]) ).

fof(f867_sk,plain,
    ! [V_z,V_w] : c_HOL_Otimes__class_Otimes(V_z,V_w,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(V_w,V_z,tc_RealDef_Oreal),
    inference(skolemisation,[status(esa)],[f867_nnf]) ).

cnf(c867,plain,
    c_HOL_Otimes__class_Otimes(X0,X1,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(X1,X0,tc_RealDef_Oreal),
    inference(cnf_transformation,[status(esa)],[f867_sk]) ).

cnf(t46,plain,
    c_HOL_Otimes__class_Otimes(X1,X2,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(X2,X1,tc_RealDef_Oreal),
    inference(equality_encoding,[status(esa)],[c867]) ).

cnf(t341,plain,
    c_HOL_Otimes__class_Otimes(X1,X2,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(X2,X1,tc_RealDef_Oreal),
    inference(orient,[status(thm)],[t46]) ).

cnf(t15641,plain,
    c_Transcendental_Osin(c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
    inference(step,[status(thm)],[t75,t341]) ).

cnf(t15642,plain,
    c_Transcendental_Osin(c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF0),tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
    inference(step,[status(thm)],[t15641,t262]) ).

cnf(t15643,plain,
    c_Transcendental_Osin(c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(sF1,tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
    inference(step,[status(thm)],[t15642,t270]) ).

cnf(t15644,plain,
    c_Transcendental_Osin(c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,sF2,tc_RealDef_Oreal)) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
    inference(step,[status(thm)],[t15643,t306]) ).

cnf(t15645,plain,
    c_Transcendental_Osin(c_HOL_Otimes__class_Otimes(sF2,c_Transcendental_Opi,tc_RealDef_Oreal)) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
    inference(step,[status(thm)],[t15644,t341]) ).

cnf(t241,axiom,
    sF3 = 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),
    introduced(definition) ).

cnf(t15591,plain,
    sF3 = c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(step,[status(thm)],[t241,t341]) ).

cnf(t15592,plain,
    sF3 = c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF0),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(step,[status(thm)],[t15591,t262]) ).

cnf(t15593,plain,
    sF3 = c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(sF1,tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(step,[status(thm)],[t15592,t270]) ).

cnf(t15594,plain,
    sF3 = c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,sF2,tc_RealDef_Oreal),
    inference(step,[status(thm)],[t15593,t306]) ).

cnf(t15595,plain,
    sF3 = c_HOL_Otimes__class_Otimes(sF2,c_Transcendental_Opi,tc_RealDef_Oreal),
    inference(step,[status(thm)],[t15594,t341]) ).

cnf(t403,plain,
    c_HOL_Otimes__class_Otimes(sF2,c_Transcendental_Opi,tc_RealDef_Oreal) = sF3,
    inference(orient,[status(thm)],[t15595]) ).

cnf(t15646,plain,
    c_Transcendental_Osin(sF3) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
    inference(step,[status(thm)],[t15645,t403]) ).

cnf(t15647,plain,
    c_Transcendental_Osin(sF3) = c_Transcendental_Osin(c_Transcendental_Opi),
    inference(step,[status(thm)],[t15646,t261]) ).

cnf(t481,plain,
    c_Transcendental_Osin(c_Transcendental_Opi) = c_Transcendental_Osin(sF3),
    inference(orient,[status(thm)],[t15647]) ).

cnf(t15668,plain,
    eq(c_Transcendental_Ocos(sF2),c_Transcendental_Osin(sF3)) = false,
    inference(step,[status(thm)],[t430,t481]) ).

cnf(t506,plain,
    eq(c_Transcendental_Ocos(sF2),c_Transcendental_Osin(sF3)) = false,
    inference(rw,[status(thm)],[t15668]) ).

cnf(t533,plain,
    eq(c_Transcendental_Ocos(sF2),c_Transcendental_Osin(sF3)) = false,
    inference(orient,[status(thm)],[t506]) ).

cnf(f673,axiom,
    c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(V_z1,V_z2,tc_RealDef_Oreal),V_w,tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_z1,V_w,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(V_z2,V_w,tc_RealDef_Oreal),tc_RealDef_Oreal),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_real__add__mult__distrib_0) ).

fof(f673_nnf,plain,
    ! [V_z1,V_z2,V_w] : c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(V_z1,V_z2,tc_RealDef_Oreal),V_w,tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_z1,V_w,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(V_z2,V_w,tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(nnf_transformation,[status(thm)],[f673]) ).

fof(f673_sk,plain,
    ! [V_z1,V_z2,V_w] : c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(V_z1,V_z2,tc_RealDef_Oreal),V_w,tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_z1,V_w,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(V_z2,V_w,tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(skolemisation,[status(esa)],[f673_nnf]) ).

cnf(c673,plain,
    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),
    inference(cnf_transformation,[status(esa)],[f673_sk]) ).

cnf(t110,plain,
    c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(X1,X2,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X3,X2,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(X1,X3,tc_RealDef_Oreal),X2,tc_RealDef_Oreal),
    inference(equality_encoding,[status(esa)],[c673]) ).

cnf(t583,plain,
    c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(X1,X2,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X3,X2,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(X1,X3,tc_RealDef_Oreal),X2,tc_RealDef_Oreal),
    inference(orient,[status(thm)],[t110]) ).

cnf(f309,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(f309_nnf,plain,
    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),
    inference(nnf_transformation,[status(thm)],[f309]) ).

cnf(c309,plain,
    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),
    inference(cnf_transformation,[status(esa)],[f309_nnf]) ).

cnf(t100,plain,
    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),
    inference(equality_encoding,[status(esa)],[c309]) ).

cnf(t15836,plain,
    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) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
    inference(step,[status(thm)],[t100,t583]) ).

cnf(t15837,plain,
    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) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
    inference(step,[status(thm)],[t15836,t341]) ).

cnf(t15648,plain,
    c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_Transcendental_Osin(sF3),
    inference(step,[status(thm)],[t261,t481]) ).

cnf(t482,plain,
    c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_Transcendental_Osin(sF3),
    inference(orient,[status(thm)],[t15648]) ).

cnf(t15838,plain,
    c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(sF3),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) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
    inference(step,[status(thm)],[t15837,t482]) ).

cnf(t15839,plain,
    c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(sF3),c_HOL_Oplus__class_Oplus(c_Transcendental_Osin(sF3),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
    inference(step,[status(thm)],[t15838,t482]) ).

cnf(t15840,plain,
    c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(sF3),c_HOL_Oplus__class_Oplus(c_Transcendental_Osin(sF3),c_Transcendental_Osin(sF3),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
    inference(step,[status(thm)],[t15839,t482]) ).

cnf(f461,axiom,
    c_HOL_Oplus__class_Oplus(V_x,c_HOL_Ouminus__class_Ouminus(V_x,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(f461_nnf,plain,
    ! [V_x] : c_HOL_Oplus__class_Oplus(V_x,c_HOL_Ouminus__class_Ouminus(V_x,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
    inference(nnf_transformation,[status(thm)],[f461]) ).

fof(f461_sk,plain,
    ! [V_x] : c_HOL_Oplus__class_Oplus(V_x,c_HOL_Ouminus__class_Ouminus(V_x,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
    inference(skolemisation,[status(esa)],[f461_nnf]) ).

cnf(c461,plain,
    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),
    inference(cnf_transformation,[status(esa)],[f461_sk]) ).

cnf(t45,plain,
    c_HOL_Oplus__class_Oplus(X1,c_HOL_Ouminus__class_Ouminus(X1,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
    inference(equality_encoding,[status(esa)],[c461]) ).

cnf(t15574,plain,
    c_HOL_Oplus__class_Oplus(X1,c_HOL_Ouminus__class_Ouminus(X1,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_Transcendental_Osin(c_Transcendental_Opi),
    inference(step,[status(thm)],[t45,t261]) ).

cnf(t328,plain,
    c_HOL_Oplus__class_Oplus(X1,c_HOL_Ouminus__class_Ouminus(X1,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_Transcendental_Osin(c_Transcendental_Opi),
    inference(orient,[status(thm)],[t15574]) ).

cnf(f676,axiom,
    c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(c_Transcendental_Opi,V_x,tc_RealDef_Oreal)) = c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(V_x),tc_RealDef_Oreal),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_sin__periodic__pi2_0) ).

fof(f676_nnf,plain,
    ! [V_x] : c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(c_Transcendental_Opi,V_x,tc_RealDef_Oreal)) = c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(V_x),tc_RealDef_Oreal),
    inference(nnf_transformation,[status(thm)],[f676]) ).

fof(f676_sk,plain,
    ! [V_x] : c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(c_Transcendental_Opi,V_x,tc_RealDef_Oreal)) = c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(V_x),tc_RealDef_Oreal),
    inference(skolemisation,[status(esa)],[f676_nnf]) ).

cnf(c676,plain,
    c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(c_Transcendental_Opi,X0,tc_RealDef_Oreal)) = c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(X0),tc_RealDef_Oreal),
    inference(cnf_transformation,[status(esa)],[f676_sk]) ).

cnf(t58,plain,
    c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(c_Transcendental_Opi,X1,tc_RealDef_Oreal)) = c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(X1),tc_RealDef_Oreal),
    inference(equality_encoding,[status(esa)],[c676]) ).

cnf(t305,plain,
    c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(c_Transcendental_Opi,X1,tc_RealDef_Oreal)) = c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(X1),tc_RealDef_Oreal),
    inference(orient,[status(thm)],[t58]) ).

cnf(t329,plain,
    c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(c_Transcendental_Opi,tc_RealDef_Oreal)),tc_RealDef_Oreal) = c_Transcendental_Osin(c_Transcendental_Osin(c_Transcendental_Opi)),
    inference(cp,[status(thm)],[t305,t328]) ).

cnf(f678,axiom,
    c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(V_x,tc_RealDef_Oreal)) = c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(V_x),tc_RealDef_Oreal),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_sin__minus_0) ).

fof(f678_nnf,plain,
    ! [V_x] : c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(V_x,tc_RealDef_Oreal)) = c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(V_x),tc_RealDef_Oreal),
    inference(nnf_transformation,[status(thm)],[f678]) ).

fof(f678_sk,plain,
    ! [V_x] : c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(V_x,tc_RealDef_Oreal)) = c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(V_x),tc_RealDef_Oreal),
    inference(skolemisation,[status(esa)],[f678_nnf]) ).

cnf(c678,plain,
    c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal)) = c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(X0),tc_RealDef_Oreal),
    inference(cnf_transformation,[status(esa)],[f678_sk]) ).

cnf(t48,plain,
    c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(X1,tc_RealDef_Oreal)) = c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(X1),tc_RealDef_Oreal),
    inference(equality_encoding,[status(esa)],[c678]) ).

cnf(t282,plain,
    c_Transcendental_Osin(c_HOL_Ouminus__class_Ouminus(X1,tc_RealDef_Oreal)) = c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(X1),tc_RealDef_Oreal),
    inference(orient,[status(thm)],[t48]) ).

cnf(t15575,plain,
    c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(c_Transcendental_Opi),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_Transcendental_Osin(c_Transcendental_Osin(c_Transcendental_Opi)),
    inference(step,[status(thm)],[t329,t282]) ).

cnf(f738,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(f738_nnf,plain,
    c_Transcendental_Osin(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
    inference(nnf_transformation,[status(thm)],[f738]) ).

cnf(c738,plain,
    c_Transcendental_Osin(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
    inference(cnf_transformation,[status(esa)],[f738_nnf]) ).

cnf(t20,plain,
    c_Transcendental_Osin(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
    inference(equality_encoding,[status(esa)],[c738]) ).

cnf(t15558,plain,
    c_Transcendental_Osin(c_Transcendental_Osin(c_Transcendental_Opi)) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
    inference(step,[status(thm)],[t20,t261]) ).

cnf(t15559,plain,
    c_Transcendental_Osin(c_Transcendental_Osin(c_Transcendental_Opi)) = c_Transcendental_Osin(c_Transcendental_Opi),
    inference(step,[status(thm)],[t15558,t261]) ).

cnf(t269,plain,
    c_Transcendental_Osin(c_Transcendental_Osin(c_Transcendental_Opi)) = c_Transcendental_Osin(c_Transcendental_Opi),
    inference(orient,[status(thm)],[t15559]) ).

cnf(t15576,plain,
    c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(c_Transcendental_Opi),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_Transcendental_Osin(c_Transcendental_Opi),
    inference(step,[status(thm)],[t15575,t269]) ).

cnf(t330,plain,
    c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(c_Transcendental_Opi),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_Transcendental_Osin(c_Transcendental_Opi),
    inference(orient,[status(thm)],[t15576]) ).

cnf(t331,plain,
    c_Transcendental_Osin(c_Transcendental_Opi) = c_HOL_Oplus__class_Oplus(c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(c_Transcendental_Opi),tc_RealDef_Oreal),c_Transcendental_Osin(c_Transcendental_Opi),tc_RealDef_Oreal),
    inference(cp,[status(thm)],[t328,t330]) ).

cnf(t428,plain,
    c_HOL_Oplus__class_Oplus(c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(c_Transcendental_Opi),tc_RealDef_Oreal),c_Transcendental_Osin(c_Transcendental_Opi),tc_RealDef_Oreal) = c_Transcendental_Osin(c_Transcendental_Opi),
    inference(orient,[status(thm)],[t331]) ).

cnf(t505,plain,
    c_HOL_Oplus__class_Oplus(c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(sF3),tc_RealDef_Oreal),c_Transcendental_Osin(sF3),tc_RealDef_Oreal) = c_Transcendental_Osin(c_Transcendental_Opi),
    inference(rw,[status(thm)],[t428]) ).

cnf(t15696,plain,
    c_HOL_Oplus__class_Oplus(c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(sF3),tc_RealDef_Oreal),c_Transcendental_Osin(sF3),tc_RealDef_Oreal) = c_Transcendental_Osin(sF3),
    inference(step,[status(thm)],[t505,t481]) ).

cnf(t550,plain,
    c_HOL_Oplus__class_Oplus(c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(sF3),tc_RealDef_Oreal),c_Transcendental_Osin(sF3),tc_RealDef_Oreal) = c_Transcendental_Osin(sF3),
    inference(orient,[status(thm)],[t15696]) ).

cnf(f697,axiom,
    c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(V_x,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),tc_RealDef_Oreal)) = c_Transcendental_Osin(V_x),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_sin__periodic_0) ).

fof(f697_nnf,plain,
    ! [V_x] : c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(V_x,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),tc_RealDef_Oreal)) = c_Transcendental_Osin(V_x),
    inference(nnf_transformation,[status(thm)],[f697]) ).

fof(f697_sk,plain,
    ! [V_x] : c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(V_x,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),tc_RealDef_Oreal)) = c_Transcendental_Osin(V_x),
    inference(skolemisation,[status(esa)],[f697_nnf]) ).

cnf(c697,plain,
    c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(X0,c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_Transcendental_Osin(X0),
    inference(cnf_transformation,[status(esa)],[f697_sk]) ).

cnf(t92,plain,
    c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(X1,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),tc_RealDef_Oreal)) = c_Transcendental_Osin(X1),
    inference(equality_encoding,[status(esa)],[c697]) ).

cnf(t15760,plain,
    c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(X1,c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_Transcendental_Osin(X1),
    inference(step,[status(thm)],[t92,t341]) ).

cnf(t15761,plain,
    c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(X1,c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF0),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_Transcendental_Osin(X1),
    inference(step,[status(thm)],[t15760,t262]) ).

cnf(t15762,plain,
    c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(X1,c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(sF1,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_Transcendental_Osin(X1),
    inference(step,[status(thm)],[t15761,t270]) ).

cnf(t15763,plain,
    c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(X1,c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,sF2,tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_Transcendental_Osin(X1),
    inference(step,[status(thm)],[t15762,t306]) ).

cnf(t15764,plain,
    c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(X1,c_HOL_Otimes__class_Otimes(sF2,c_Transcendental_Opi,tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_Transcendental_Osin(X1),
    inference(step,[status(thm)],[t15763,t341]) ).

cnf(t15765,plain,
    c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(X1,sF3,tc_RealDef_Oreal)) = c_Transcendental_Osin(X1),
    inference(step,[status(thm)],[t15764,t403]) ).

cnf(t1118,plain,
    c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(X1,sF3,tc_RealDef_Oreal)) = c_Transcendental_Osin(X1),
    inference(orient,[status(thm)],[t15765]) ).

cnf(t1119,plain,
    c_Transcendental_Osin(c_Transcendental_Opi) = c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(sF3),tc_RealDef_Oreal),
    inference(cp,[status(thm)],[t1118,t305]) ).

cnf(t15766,plain,
    c_Transcendental_Osin(sF3) = c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(sF3),tc_RealDef_Oreal),
    inference(step,[status(thm)],[t1119,t481]) ).

cnf(t1125,plain,
    c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(sF3),tc_RealDef_Oreal) = c_Transcendental_Osin(sF3),
    inference(orient,[status(thm)],[t15766]) ).

cnf(t15769,plain,
    c_HOL_Oplus__class_Oplus(c_Transcendental_Osin(sF3),c_Transcendental_Osin(sF3),tc_RealDef_Oreal) = c_Transcendental_Osin(sF3),
    inference(step,[status(thm)],[t550,t1125]) ).

cnf(t1127,plain,
    c_HOL_Oplus__class_Oplus(c_Transcendental_Osin(sF3),c_Transcendental_Osin(sF3),tc_RealDef_Oreal) = c_Transcendental_Osin(sF3),
    inference(rw,[status(thm)],[t15769]) ).

cnf(t1131,plain,
    c_HOL_Oplus__class_Oplus(c_Transcendental_Osin(sF3),c_Transcendental_Osin(sF3),tc_RealDef_Oreal) = c_Transcendental_Osin(sF3),
    inference(orient,[status(thm)],[t1127]) ).

cnf(t15841,plain,
    c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(sF3),c_Transcendental_Osin(sF3),tc_RealDef_Oreal) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
    inference(step,[status(thm)],[t15840,t1131]) ).

cnf(t15842,plain,
    c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(sF3),c_Transcendental_Osin(sF3),tc_RealDef_Oreal) = c_Transcendental_Osin(sF3),
    inference(step,[status(thm)],[t15841,t482]) ).

cnf(t1857,plain,
    c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(sF3),c_Transcendental_Osin(sF3),tc_RealDef_Oreal) = c_Transcendental_Osin(sF3),
    inference(orient,[status(thm)],[t15842]) ).

cnf(t1862,plain,
    c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(c_Transcendental_Osin(sF3),X1,tc_RealDef_Oreal),c_Transcendental_Osin(sF3),tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(c_Transcendental_Osin(sF3),c_HOL_Otimes__class_Otimes(X1,c_Transcendental_Osin(sF3),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(cp,[status(thm)],[t583,t1857]) ).

cnf(t15850,plain,
    c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(sF3),c_HOL_Oplus__class_Oplus(c_Transcendental_Osin(sF3),X1,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(c_Transcendental_Osin(sF3),c_HOL_Otimes__class_Otimes(X1,c_Transcendental_Osin(sF3),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(step,[status(thm)],[t1862,t341]) ).

cnf(t1902,plain,
    c_HOL_Oplus__class_Oplus(c_Transcendental_Osin(sF3),c_HOL_Otimes__class_Otimes(X1,c_Transcendental_Osin(sF3),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(sF3),c_HOL_Oplus__class_Oplus(c_Transcendental_Osin(sF3),X1,tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(orient,[status(thm)],[t15850]) ).

cnf(f878,axiom,
    c_Transcendental_Osin(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),V_x,tc_RealDef_Oreal)) = c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Osin(V_x),tc_RealDef_Oreal),c_Transcendental_Ocos(V_x),tc_RealDef_Oreal),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_sin__double_0) ).

fof(f878_nnf,plain,
    ! [V_x] : c_Transcendental_Osin(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),V_x,tc_RealDef_Oreal)) = c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Osin(V_x),tc_RealDef_Oreal),c_Transcendental_Ocos(V_x),tc_RealDef_Oreal),
    inference(nnf_transformation,[status(thm)],[f878]) ).

fof(f878_sk,plain,
    ! [V_x] : c_Transcendental_Osin(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),V_x,tc_RealDef_Oreal)) = c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Osin(V_x),tc_RealDef_Oreal),c_Transcendental_Ocos(V_x),tc_RealDef_Oreal),
    inference(skolemisation,[status(esa)],[f878_nnf]) ).

cnf(c878,plain,
    c_Transcendental_Osin(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),X0,tc_RealDef_Oreal)) = c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Osin(X0),tc_RealDef_Oreal),c_Transcendental_Ocos(X0),tc_RealDef_Oreal),
    inference(cnf_transformation,[status(esa)],[f878_sk]) ).

cnf(t136,plain,
    c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Osin(X1),tc_RealDef_Oreal),c_Transcendental_Ocos(X1),tc_RealDef_Oreal) = c_Transcendental_Osin(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),X1,tc_RealDef_Oreal)),
    inference(equality_encoding,[status(esa)],[c878]) ).

cnf(f832,axiom,
    c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(V_z1,V_z2,tc_RealDef_Oreal),V_z3,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(V_z1,c_HOL_Otimes__class_Otimes(V_z2,V_z3,tc_RealDef_Oreal),tc_RealDef_Oreal),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_real__mult__assoc_0) ).

fof(f832_nnf,plain,
    ! [V_z1,V_z2,V_z3] : c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(V_z1,V_z2,tc_RealDef_Oreal),V_z3,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(V_z1,c_HOL_Otimes__class_Otimes(V_z2,V_z3,tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(nnf_transformation,[status(thm)],[f832]) ).

fof(f832_sk,plain,
    ! [V_z1,V_z2,V_z3] : c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(V_z1,V_z2,tc_RealDef_Oreal),V_z3,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(V_z1,c_HOL_Otimes__class_Otimes(V_z2,V_z3,tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(skolemisation,[status(esa)],[f832_nnf]) ).

cnf(c832,plain,
    c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(X0,X1,tc_RealDef_Oreal),X2,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(X0,c_HOL_Otimes__class_Otimes(X1,X2,tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(cnf_transformation,[status(esa)],[f832_sk]) ).

cnf(t90,plain,
    c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(X1,X2,tc_RealDef_Oreal),X3,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(X1,c_HOL_Otimes__class_Otimes(X2,X3,tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(equality_encoding,[status(esa)],[c832]) ).

cnf(t394,plain,
    c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(X1,X2,tc_RealDef_Oreal),X3,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(X1,c_HOL_Otimes__class_Otimes(X2,X3,tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(orient,[status(thm)],[t90]) ).

cnf(t16090,plain,
    c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(X1),c_Transcendental_Ocos(X1),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_Transcendental_Osin(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),X1,tc_RealDef_Oreal)),
    inference(step,[status(thm)],[t136,t394]) ).

cnf(t16091,plain,
    c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF0),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(X1),c_Transcendental_Ocos(X1),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_Transcendental_Osin(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),X1,tc_RealDef_Oreal)),
    inference(step,[status(thm)],[t16090,t262]) ).

cnf(t16092,plain,
    c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(sF1,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(X1),c_Transcendental_Ocos(X1),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_Transcendental_Osin(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),X1,tc_RealDef_Oreal)),
    inference(step,[status(thm)],[t16091,t270]) ).

cnf(t16093,plain,
    c_HOL_Otimes__class_Otimes(sF2,c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(X1),c_Transcendental_Ocos(X1),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_Transcendental_Osin(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),X1,tc_RealDef_Oreal)),
    inference(step,[status(thm)],[t16092,t306]) ).

cnf(t16094,plain,
    c_HOL_Otimes__class_Otimes(sF2,c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(X1),c_Transcendental_Ocos(X1),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_Transcendental_Osin(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF0),tc_RealDef_Oreal),X1,tc_RealDef_Oreal)),
    inference(step,[status(thm)],[t16093,t262]) ).

cnf(t16095,plain,
    c_HOL_Otimes__class_Otimes(sF2,c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(X1),c_Transcendental_Ocos(X1),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_Transcendental_Osin(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(sF1,tc_RealDef_Oreal),X1,tc_RealDef_Oreal)),
    inference(step,[status(thm)],[t16094,t270]) ).

cnf(t16096,plain,
    c_HOL_Otimes__class_Otimes(sF2,c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(X1),c_Transcendental_Ocos(X1),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_Transcendental_Osin(c_HOL_Otimes__class_Otimes(sF2,X1,tc_RealDef_Oreal)),
    inference(step,[status(thm)],[t16095,t306]) ).

cnf(t6170,plain,
    c_HOL_Otimes__class_Otimes(sF2,c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(X1),c_Transcendental_Ocos(X1),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_Transcendental_Osin(c_HOL_Otimes__class_Otimes(sF2,X1,tc_RealDef_Oreal)),
    inference(orient,[status(thm)],[t16096]) ).

cnf(t6180,plain,
    c_Transcendental_Osin(c_HOL_Otimes__class_Otimes(sF2,c_Transcendental_Opi,tc_RealDef_Oreal)) = c_HOL_Otimes__class_Otimes(sF2,c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(sF3),c_Transcendental_Ocos(c_Transcendental_Opi),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(cp,[status(thm)],[t6170,t481]) ).

cnf(t16144,plain,
    c_Transcendental_Osin(sF3) = c_HOL_Otimes__class_Otimes(sF2,c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(sF3),c_Transcendental_Ocos(c_Transcendental_Opi),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(step,[status(thm)],[t6180,t403]) ).

cnf(t7270,plain,
    c_HOL_Otimes__class_Otimes(sF2,c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(sF3),c_Transcendental_Ocos(c_Transcendental_Opi),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_Transcendental_Osin(sF3),
    inference(orient,[status(thm)],[t16144]) ).

cnf(f517,axiom,
    c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(V_x,V_y,tc_RealDef_Oreal)) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(V_x),c_Transcendental_Ocos(V_y),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(V_x),c_Transcendental_Osin(V_y),tc_RealDef_Oreal),tc_RealDef_Oreal),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_sin__add_0) ).

fof(f517_nnf,plain,
    ! [V_x,V_y] : c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(V_x,V_y,tc_RealDef_Oreal)) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(V_x),c_Transcendental_Ocos(V_y),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(V_x),c_Transcendental_Osin(V_y),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(nnf_transformation,[status(thm)],[f517]) ).

fof(f517_sk,plain,
    ! [V_x,V_y] : c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(V_x,V_y,tc_RealDef_Oreal)) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(V_x),c_Transcendental_Ocos(V_y),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(V_x),c_Transcendental_Osin(V_y),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(skolemisation,[status(esa)],[f517_nnf]) ).

cnf(c517,plain,
    c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(X0,X1,tc_RealDef_Oreal)) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(X0),c_Transcendental_Ocos(X1),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(X0),c_Transcendental_Osin(X1),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(cnf_transformation,[status(esa)],[f517_sk]) ).

cnf(t132,plain,
    c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(X1),c_Transcendental_Ocos(X2),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(X1),c_Transcendental_Osin(X2),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(X1,X2,tc_RealDef_Oreal)),
    inference(equality_encoding,[status(esa)],[c517]) ).

cnf(t5658,plain,
    c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(X1),c_Transcendental_Ocos(X2),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(X1),c_Transcendental_Osin(X2),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(X1,X2,tc_RealDef_Oreal)),
    inference(orient,[status(thm)],[t132]) ).

cnf(f744,axiom,
    c_HOL_Otimes__class_Otimes(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),V_z,tc_RealDef_Oreal) = V_z,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_real__mult__1_0) ).

fof(f744_nnf,plain,
    ! [V_z] : c_HOL_Otimes__class_Otimes(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),V_z,tc_RealDef_Oreal) = V_z,
    inference(nnf_transformation,[status(thm)],[f744]) ).

fof(f744_sk,plain,
    ! [V_z] : c_HOL_Otimes__class_Otimes(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),V_z,tc_RealDef_Oreal) = V_z,
    inference(skolemisation,[status(esa)],[f744_nnf]) ).

cnf(c744,plain,
    c_HOL_Otimes__class_Otimes(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),X0,tc_RealDef_Oreal) = X0,
    inference(cnf_transformation,[status(esa)],[f744_sk]) ).

cnf(t27,plain,
    c_HOL_Otimes__class_Otimes(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),X1,tc_RealDef_Oreal) = X1,
    inference(equality_encoding,[status(esa)],[c744]) ).

cnf(t284,plain,
    c_HOL_Otimes__class_Otimes(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),X1,tc_RealDef_Oreal) = X1,
    inference(orient,[status(thm)],[t27]) ).

cnf(f715,axiom,
    c_Transcendental_Ocos(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal)) = c_HOL_Oone__class_Oone(tc_RealDef_Oreal),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_cos__two__pi_0) ).

fof(f715_nnf,plain,
    c_Transcendental_Ocos(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal)) = c_HOL_Oone__class_Oone(tc_RealDef_Oreal),
    inference(nnf_transformation,[status(thm)],[f715]) ).

cnf(c715,plain,
    c_Transcendental_Ocos(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal)) = c_HOL_Oone__class_Oone(tc_RealDef_Oreal),
    inference(cnf_transformation,[status(esa)],[f715_nnf]) ).

cnf(t73,plain,
    c_Transcendental_Ocos(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal)) = c_HOL_Oone__class_Oone(tc_RealDef_Oreal),
    inference(equality_encoding,[status(esa)],[c715]) ).

cnf(t15610,plain,
    c_Transcendental_Ocos(c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_HOL_Oone__class_Oone(tc_RealDef_Oreal),
    inference(step,[status(thm)],[t73,t341]) ).

cnf(t15611,plain,
    c_Transcendental_Ocos(c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF0),tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_HOL_Oone__class_Oone(tc_RealDef_Oreal),
    inference(step,[status(thm)],[t15610,t262]) ).

cnf(t15612,plain,
    c_Transcendental_Ocos(c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(sF1,tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_HOL_Oone__class_Oone(tc_RealDef_Oreal),
    inference(step,[status(thm)],[t15611,t270]) ).

cnf(t15613,plain,
    c_Transcendental_Ocos(c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,sF2,tc_RealDef_Oreal)) = c_HOL_Oone__class_Oone(tc_RealDef_Oreal),
    inference(step,[status(thm)],[t15612,t306]) ).

cnf(t15614,plain,
    c_Transcendental_Ocos(c_HOL_Otimes__class_Otimes(sF2,c_Transcendental_Opi,tc_RealDef_Oreal)) = c_HOL_Oone__class_Oone(tc_RealDef_Oreal),
    inference(step,[status(thm)],[t15613,t341]) ).

cnf(t15615,plain,
    c_Transcendental_Ocos(sF3) = c_HOL_Oone__class_Oone(tc_RealDef_Oreal),
    inference(step,[status(thm)],[t15614,t403]) ).

cnf(t449,plain,
    c_HOL_Oone__class_Oone(tc_RealDef_Oreal) = c_Transcendental_Ocos(sF3),
    inference(orient,[status(thm)],[t15615]) ).

cnf(t15618,plain,
    c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(sF3),X1,tc_RealDef_Oreal) = X1,
    inference(step,[status(thm)],[t284,t449]) ).

cnf(t452,plain,
    c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(sF3),X1,tc_RealDef_Oreal) = X1,
    inference(rw,[status(thm)],[t15618]) ).

cnf(t464,plain,
    c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(sF3),X1,tc_RealDef_Oreal) = X1,
    inference(orient,[status(thm)],[t452]) ).

cnf(t5673,plain,
    c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(sF3,X1,tc_RealDef_Oreal)) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(sF3),c_Transcendental_Ocos(X1),tc_RealDef_Oreal),c_Transcendental_Osin(X1),tc_RealDef_Oreal),
    inference(cp,[status(thm)],[t5658,t464]) ).

cnf(t11093,plain,
    c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(sF3),c_Transcendental_Ocos(X1),tc_RealDef_Oreal),c_Transcendental_Osin(X1),tc_RealDef_Oreal) = c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(sF3,X1,tc_RealDef_Oreal)),
    inference(orient,[status(thm)],[t5673]) ).

cnf(t11099,plain,
    c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(sF3,c_Transcendental_Opi,tc_RealDef_Oreal)) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(sF3),c_Transcendental_Ocos(c_Transcendental_Opi),tc_RealDef_Oreal),c_Transcendental_Osin(sF3),tc_RealDef_Oreal),
    inference(cp,[status(thm)],[t11093,t481]) ).

cnf(f677,axiom,
    c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(V_x,c_Transcendental_Opi,tc_RealDef_Oreal)) = c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(V_x),tc_RealDef_Oreal),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_sin__periodic__pi_0) ).

fof(f677_nnf,plain,
    ! [V_x] : c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(V_x,c_Transcendental_Opi,tc_RealDef_Oreal)) = c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(V_x),tc_RealDef_Oreal),
    inference(nnf_transformation,[status(thm)],[f677]) ).

fof(f677_sk,plain,
    ! [V_x] : c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(V_x,c_Transcendental_Opi,tc_RealDef_Oreal)) = c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(V_x),tc_RealDef_Oreal),
    inference(skolemisation,[status(esa)],[f677_nnf]) ).

cnf(c677,plain,
    c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(X0,c_Transcendental_Opi,tc_RealDef_Oreal)) = c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(X0),tc_RealDef_Oreal),
    inference(cnf_transformation,[status(esa)],[f677_sk]) ).

cnf(t57,plain,
    c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(X1,c_Transcendental_Opi,tc_RealDef_Oreal)) = c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(X1),tc_RealDef_Oreal),
    inference(equality_encoding,[status(esa)],[c677]) ).

cnf(t304,plain,
    c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(X1,c_Transcendental_Opi,tc_RealDef_Oreal)) = c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(X1),tc_RealDef_Oreal),
    inference(orient,[status(thm)],[t57]) ).

cnf(t16249,plain,
    c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(sF3),tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(sF3),c_Transcendental_Ocos(c_Transcendental_Opi),tc_RealDef_Oreal),c_Transcendental_Osin(sF3),tc_RealDef_Oreal),
    inference(step,[status(thm)],[t11099,t304]) ).

cnf(t16250,plain,
    c_Transcendental_Osin(sF3) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(sF3),c_Transcendental_Ocos(c_Transcendental_Opi),tc_RealDef_Oreal),c_Transcendental_Osin(sF3),tc_RealDef_Oreal),
    inference(step,[status(thm)],[t16249,t1125]) ).

cnf(t584,plain,
    c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(X1,X2,tc_RealDef_Oreal),X3,tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(X3,X1,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X2,X3,tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(cp,[status(thm)],[t583,t341]) ).

cnf(t855,plain,
    c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(X1,X2,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X3,X1,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(X2,X3,tc_RealDef_Oreal),X1,tc_RealDef_Oreal),
    inference(orient,[status(thm)],[t584]) ).

cnf(t1867,plain,
    c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(X1,c_Transcendental_Osin(sF3),tc_RealDef_Oreal),c_Transcendental_Osin(sF3),tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(sF3),X1,tc_RealDef_Oreal),c_Transcendental_Osin(sF3),tc_RealDef_Oreal),
    inference(cp,[status(thm)],[t855,t1857]) ).

cnf(t15859,plain,
    c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(sF3),c_HOL_Oplus__class_Oplus(X1,c_Transcendental_Osin(sF3),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(sF3),X1,tc_RealDef_Oreal),c_Transcendental_Osin(sF3),tc_RealDef_Oreal),
    inference(step,[status(thm)],[t1867,t341]) ).

cnf(t1941,plain,
    c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(sF3),X1,tc_RealDef_Oreal),c_Transcendental_Osin(sF3),tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(sF3),c_HOL_Oplus__class_Oplus(X1,c_Transcendental_Osin(sF3),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(orient,[status(thm)],[t15859]) ).

cnf(t16251,plain,
    c_Transcendental_Osin(sF3) = c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(sF3),c_HOL_Oplus__class_Oplus(c_Transcendental_Ocos(c_Transcendental_Opi),c_Transcendental_Osin(sF3),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(step,[status(thm)],[t16250,t1941]) ).

cnf(f710,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(f710_nnf,plain,
    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),
    inference(nnf_transformation,[status(thm)],[f710]) ).

cnf(c710,plain,
    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),
    inference(cnf_transformation,[status(esa)],[f710_nnf]) ).

cnf(t72,plain,
    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),
    inference(equality_encoding,[status(esa)],[c710]) ).

cnf(t15606,plain,
    c_Transcendental_Ocos(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF0),tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
    inference(step,[status(thm)],[t72,t262]) ).

cnf(t15607,plain,
    c_Transcendental_Ocos(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(sF1,tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
    inference(step,[status(thm)],[t15606,t270]) ).

cnf(t15608,plain,
    c_Transcendental_Ocos(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,sF2,tc_RealDef_Oreal)) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
    inference(step,[status(thm)],[t15607,t306]) ).

cnf(t15609,plain,
    c_Transcendental_Ocos(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,sF2,tc_RealDef_Oreal)) = c_Transcendental_Osin(c_Transcendental_Opi),
    inference(step,[status(thm)],[t15608,t261]) ).

cnf(t448,plain,
    c_Transcendental_Ocos(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,sF2,tc_RealDef_Oreal)) = c_Transcendental_Osin(c_Transcendental_Opi),
    inference(orient,[status(thm)],[t15609]) ).

cnf(t15671,plain,
    c_Transcendental_Ocos(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,sF2,tc_RealDef_Oreal)) = c_Transcendental_Osin(sF3),
    inference(step,[status(thm)],[t448,t481]) ).

cnf(t512,plain,
    c_Transcendental_Ocos(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,sF2,tc_RealDef_Oreal)) = c_Transcendental_Osin(sF3),
    inference(orient,[status(thm)],[t15671]) ).

cnf(t5672,plain,
    c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,sF2,tc_RealDef_Oreal),X1,tc_RealDef_Oreal)) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,sF2,tc_RealDef_Oreal)),c_Transcendental_Ocos(X1),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(sF3),c_Transcendental_Osin(X1),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(cp,[status(thm)],[t5658,t512]) ).

cnf(f708,axiom,
    c_Transcendental_Osin(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_Oone__class_Oone(tc_RealDef_Oreal),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_sin__pi__half_0) ).

fof(f708_nnf,plain,
    c_Transcendental_Osin(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_Oone__class_Oone(tc_RealDef_Oreal),
    inference(nnf_transformation,[status(thm)],[f708]) ).

cnf(c708,plain,
    c_Transcendental_Osin(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_Oone__class_Oone(tc_RealDef_Oreal),
    inference(cnf_transformation,[status(esa)],[f708_nnf]) ).

cnf(t74,plain,
    c_Transcendental_Osin(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_Oone__class_Oone(tc_RealDef_Oreal),
    inference(equality_encoding,[status(esa)],[c708]) ).

cnf(t15637,plain,
    c_Transcendental_Osin(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF0),tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_HOL_Oone__class_Oone(tc_RealDef_Oreal),
    inference(step,[status(thm)],[t74,t262]) ).

cnf(t15638,plain,
    c_Transcendental_Osin(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(sF1,tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_HOL_Oone__class_Oone(tc_RealDef_Oreal),
    inference(step,[status(thm)],[t15637,t270]) ).

cnf(t15639,plain,
    c_Transcendental_Osin(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,sF2,tc_RealDef_Oreal)) = c_HOL_Oone__class_Oone(tc_RealDef_Oreal),
    inference(step,[status(thm)],[t15638,t306]) ).

cnf(t15640,plain,
    c_Transcendental_Osin(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,sF2,tc_RealDef_Oreal)) = c_Transcendental_Ocos(sF3),
    inference(step,[status(thm)],[t15639,t449]) ).

cnf(t480,plain,
    c_Transcendental_Osin(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,sF2,tc_RealDef_Oreal)) = c_Transcendental_Ocos(sF3),
    inference(orient,[status(thm)],[t15640]) ).

cnf(t16241,plain,
    c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,sF2,tc_RealDef_Oreal),X1,tc_RealDef_Oreal)) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(sF3),c_Transcendental_Ocos(X1),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(sF3),c_Transcendental_Osin(X1),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(step,[status(thm)],[t5672,t480]) ).

cnf(t16242,plain,
    c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,sF2,tc_RealDef_Oreal),X1,tc_RealDef_Oreal)) = c_HOL_Oplus__class_Oplus(c_Transcendental_Ocos(X1),c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(sF3),c_Transcendental_Osin(X1),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(step,[status(thm)],[t16241,t464]) ).

cnf(t10994,plain,
    c_HOL_Oplus__class_Oplus(c_Transcendental_Ocos(X1),c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(sF3),c_Transcendental_Osin(X1),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,sF2,tc_RealDef_Oreal),X1,tc_RealDef_Oreal)),
    inference(orient,[status(thm)],[t16242]) ).

cnf(t11001,plain,
    c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,sF2,tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal)) = c_HOL_Oplus__class_Oplus(c_Transcendental_Ocos(c_Transcendental_Opi),c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(sF3),c_Transcendental_Osin(sF3),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(cp,[status(thm)],[t10994,t481]) ).

cnf(t16243,plain,
    c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,sF2,tc_RealDef_Oreal)),tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(c_Transcendental_Ocos(c_Transcendental_Opi),c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(sF3),c_Transcendental_Osin(sF3),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(step,[status(thm)],[t11001,t304]) ).

cnf(t16244,plain,
    c_HOL_Ouminus__class_Ouminus(c_Transcendental_Ocos(sF3),tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(c_Transcendental_Ocos(c_Transcendental_Opi),c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(sF3),c_Transcendental_Osin(sF3),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(step,[status(thm)],[t16243,t480]) ).

cnf(f563,axiom,
    c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(V_x),tc_RealDef_Oreal) = c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(V_x,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(f563_nnf,plain,
    ! [V_x] : c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(V_x),tc_RealDef_Oreal) = c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(V_x,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)),
    inference(nnf_transformation,[status(thm)],[f563]) ).

fof(f563_sk,plain,
    ! [V_x] : c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(V_x),tc_RealDef_Oreal) = c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(V_x,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)),
    inference(skolemisation,[status(esa)],[f563_nnf]) ).

cnf(c563,plain,
    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)),
    inference(cnf_transformation,[status(esa)],[f563_sk]) ).

cnf(t102,plain,
    c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(X1,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_Osin(X1),tc_RealDef_Oreal),
    inference(equality_encoding,[status(esa)],[c563]) ).

cnf(t15863,plain,
    c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(X1,c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF0),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(X1),tc_RealDef_Oreal),
    inference(step,[status(thm)],[t102,t262]) ).

cnf(t15864,plain,
    c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(X1,c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(sF1,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(X1),tc_RealDef_Oreal),
    inference(step,[status(thm)],[t15863,t270]) ).

cnf(t15865,plain,
    c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(X1,c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,sF2,tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(X1),tc_RealDef_Oreal),
    inference(step,[status(thm)],[t15864,t306]) ).

cnf(t1959,plain,
    c_Transcendental_Ocos(c_HOL_Oplus__class_Oplus(X1,c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,sF2,tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(X1),tc_RealDef_Oreal),
    inference(orient,[status(thm)],[t15865]) ).

cnf(f572,axiom,
    c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(V_x,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(V_x,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) = V_x,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_real__sum__of__halves_0) ).

fof(f572_nnf,plain,
    ! [V_x] : c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(V_x,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(V_x,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) = V_x,
    inference(nnf_transformation,[status(thm)],[f572]) ).

fof(f572_sk,plain,
    ! [V_x] : c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(V_x,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(V_x,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) = V_x,
    inference(skolemisation,[status(esa)],[f572_nnf]) ).

cnf(c572,plain,
    c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(X0,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(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) = X0,
    inference(cnf_transformation,[status(esa)],[f572_sk]) ).

cnf(t131,plain,
    c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(X1,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(X1,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) = X1,
    inference(equality_encoding,[status(esa)],[c572]) ).

cnf(t16050,plain,
    c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(X1,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF0),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(X1,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) = X1,
    inference(step,[status(thm)],[t131,t262]) ).

cnf(t16051,plain,
    c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(X1,c_Int_Onumber__class_Onumber__of(sF1,tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(X1,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) = X1,
    inference(step,[status(thm)],[t16050,t270]) ).

cnf(t16052,plain,
    c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(X1,sF2,tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(X1,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) = X1,
    inference(step,[status(thm)],[t16051,t306]) ).

cnf(t16053,plain,
    c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(X1,sF2,tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(X1,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF0),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) = X1,
    inference(step,[status(thm)],[t16052,t262]) ).

cnf(t16054,plain,
    c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(X1,sF2,tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(X1,c_Int_Onumber__class_Onumber__of(sF1,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) = X1,
    inference(step,[status(thm)],[t16053,t270]) ).

cnf(t16055,plain,
    c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(X1,sF2,tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(X1,sF2,tc_RealDef_Oreal),tc_RealDef_Oreal) = X1,
    inference(step,[status(thm)],[t16054,t306]) ).

cnf(t5553,plain,
    c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(X1,sF2,tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(X1,sF2,tc_RealDef_Oreal),tc_RealDef_Oreal) = X1,
    inference(orient,[status(thm)],[t16055]) ).

cnf(t5557,plain,
    c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,sF2,tc_RealDef_Oreal)),tc_RealDef_Oreal) = c_Transcendental_Ocos(c_Transcendental_Opi),
    inference(cp,[status(thm)],[t1959,t5553]) ).

cnf(t16056,plain,
    c_HOL_Ouminus__class_Ouminus(c_Transcendental_Ocos(sF3),tc_RealDef_Oreal) = c_Transcendental_Ocos(c_Transcendental_Opi),
    inference(step,[status(thm)],[t5557,t480]) ).

cnf(t5568,plain,
    c_HOL_Ouminus__class_Ouminus(c_Transcendental_Ocos(sF3),tc_RealDef_Oreal) = c_Transcendental_Ocos(c_Transcendental_Opi),
    inference(orient,[status(thm)],[t16056]) ).

cnf(t16245,plain,
    c_Transcendental_Ocos(c_Transcendental_Opi) = c_HOL_Oplus__class_Oplus(c_Transcendental_Ocos(c_Transcendental_Opi),c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(sF3),c_Transcendental_Osin(sF3),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(step,[status(thm)],[t16244,t5568]) ).

cnf(t16246,plain,
    c_Transcendental_Ocos(c_Transcendental_Opi) = c_HOL_Oplus__class_Oplus(c_Transcendental_Ocos(c_Transcendental_Opi),c_Transcendental_Osin(sF3),tc_RealDef_Oreal),
    inference(step,[status(thm)],[t16245,t1857]) ).

cnf(t11064,plain,
    c_HOL_Oplus__class_Oplus(c_Transcendental_Ocos(c_Transcendental_Opi),c_Transcendental_Osin(sF3),tc_RealDef_Oreal) = c_Transcendental_Ocos(c_Transcendental_Opi),
    inference(orient,[status(thm)],[t16246]) ).

cnf(t16252,plain,
    c_Transcendental_Osin(sF3) = c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(sF3),c_Transcendental_Ocos(c_Transcendental_Opi),tc_RealDef_Oreal),
    inference(step,[status(thm)],[t16251,t11064]) ).

cnf(t11161,plain,
    c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(sF3),c_Transcendental_Ocos(c_Transcendental_Opi),tc_RealDef_Oreal) = c_Transcendental_Osin(sF3),
    inference(orient,[status(thm)],[t16252]) ).

cnf(t16253,plain,
    c_HOL_Otimes__class_Otimes(sF2,c_Transcendental_Osin(sF3),tc_RealDef_Oreal) = c_Transcendental_Osin(sF3),
    inference(step,[status(thm)],[t7270,t11161]) ).

cnf(t11162,plain,
    c_HOL_Otimes__class_Otimes(sF2,c_Transcendental_Osin(sF3),tc_RealDef_Oreal) = c_Transcendental_Osin(sF3),
    inference(rw,[status(thm)],[t16253]) ).

cnf(t11198,plain,
    c_HOL_Otimes__class_Otimes(sF2,c_Transcendental_Osin(sF3),tc_RealDef_Oreal) = c_Transcendental_Osin(sF3),
    inference(orient,[status(thm)],[t11162]) ).

cnf(t11209,plain,
    c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(sF2,X1,tc_RealDef_Oreal),c_Transcendental_Osin(sF3),tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(c_Transcendental_Osin(sF3),c_HOL_Otimes__class_Otimes(X1,c_Transcendental_Osin(sF3),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(cp,[status(thm)],[t583,t11198]) ).

cnf(t16378,plain,
    c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(sF3),c_HOL_Oplus__class_Oplus(sF2,X1,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(c_Transcendental_Osin(sF3),c_HOL_Otimes__class_Otimes(X1,c_Transcendental_Osin(sF3),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(step,[status(thm)],[t11209,t341]) ).

cnf(t16379,plain,
    c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(sF3),c_HOL_Oplus__class_Oplus(sF2,X1,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(sF3),c_HOL_Oplus__class_Oplus(c_Transcendental_Osin(sF3),X1,tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(step,[status(thm)],[t16378,t1902]) ).

cnf(t13186,plain,
    c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(sF3),c_HOL_Oplus__class_Oplus(c_Transcendental_Osin(sF3),X1,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(sF3),c_HOL_Oplus__class_Oplus(sF2,X1,tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(orient,[status(thm)],[t16379]) ).

cnf(t16380,plain,
    c_HOL_Oplus__class_Oplus(c_Transcendental_Osin(sF3),c_HOL_Otimes__class_Otimes(X1,c_Transcendental_Osin(sF3),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(sF3),c_HOL_Oplus__class_Oplus(sF2,X1,tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(step,[status(thm)],[t1902,t13186]) ).

cnf(t13187,plain,
    c_HOL_Oplus__class_Oplus(c_Transcendental_Osin(sF3),c_HOL_Otimes__class_Otimes(X1,c_Transcendental_Osin(sF3),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(sF3),c_HOL_Oplus__class_Oplus(sF2,X1,tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(orient,[status(thm)],[t16380]) ).

cnf(f565,axiom,
    c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(V_x),c_Transcendental_Ocos(V_x),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(V_x),c_Transcendental_Osin(V_x),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Oone__class_Oone(tc_RealDef_Oreal),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_sin__cos__squared__add3_0) ).

fof(f565_nnf,plain,
    ! [V_x] : c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(V_x),c_Transcendental_Ocos(V_x),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(V_x),c_Transcendental_Osin(V_x),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Oone__class_Oone(tc_RealDef_Oreal),
    inference(nnf_transformation,[status(thm)],[f565]) ).

fof(f565_sk,plain,
    ! [V_x] : c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(V_x),c_Transcendental_Ocos(V_x),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(V_x),c_Transcendental_Osin(V_x),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Oone__class_Oone(tc_RealDef_Oreal),
    inference(skolemisation,[status(esa)],[f565_nnf]) ).

cnf(c565,plain,
    c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(X0),c_Transcendental_Ocos(X0),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(X0),c_Transcendental_Osin(X0),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Oone__class_Oone(tc_RealDef_Oreal),
    inference(cnf_transformation,[status(esa)],[f565_sk]) ).

cnf(t101,plain,
    c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(X1),c_Transcendental_Ocos(X1),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(X1),c_Transcendental_Osin(X1),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Oone__class_Oone(tc_RealDef_Oreal),
    inference(equality_encoding,[status(esa)],[c565]) ).

cnf(t15851,plain,
    c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(X1),c_Transcendental_Ocos(X1),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(X1),c_Transcendental_Osin(X1),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_Transcendental_Ocos(sF3),
    inference(step,[status(thm)],[t101,t449]) ).

cnf(t1907,plain,
    c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(X1),c_Transcendental_Ocos(X1),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(X1),c_Transcendental_Osin(X1),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_Transcendental_Ocos(sF3),
    inference(orient,[status(thm)],[t15851]) ).

cnf(f728,axiom,
    ( V_b = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)
    | c_Complex_Ocomplex_OComplex(V_a,V_b) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Complex__eq__0_1) ).

fof(f728_nnf,plain,
    ! [V_a,V_b] :
      ( V_b = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)
      | c_Complex_Ocomplex_OComplex(V_a,V_b) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
    inference(nnf_transformation,[status(thm)],[f728]) ).

fof(f728_sk,plain,
    ! [V_a,V_b] :
      ( V_b = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)
      | c_Complex_Ocomplex_OComplex(V_a,V_b) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
    inference(skolemisation,[status(esa)],[f728_nnf]) ).

cnf(c728,plain,
    ( X1 = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)
    | c_Complex_Ocomplex_OComplex(X0,X1) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
    inference(cnf_transformation,[status(esa)],[f728_sk]) ).

cnf(t78,plain,
    ifeq(c_Complex_Ocomplex_OComplex(X1,X2),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),X2,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
    inference(equality_encoding,[status(esa)],[c728]) ).

cnf(t247,axiom,
    sF9 = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
    introduced(definition) ).

cnf(t263,plain,
    c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = sF9,
    inference(orient,[status(thm)],[t247]) ).

cnf(t15693,plain,
    ifeq(c_Complex_Ocomplex_OComplex(X1,X2),sF9,X2,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
    inference(step,[status(thm)],[t78,t263]) ).

cnf(t15694,plain,
    ifeq(c_Complex_Ocomplex_OComplex(X1,X2),sF9,X2,c_Transcendental_Osin(sF3)) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
    inference(step,[status(thm)],[t15693,t482]) ).

cnf(t15695,plain,
    ifeq(c_Complex_Ocomplex_OComplex(X1,X2),sF9,X2,c_Transcendental_Osin(sF3)) = c_Transcendental_Osin(sF3),
    inference(step,[status(thm)],[t15694,t482]) ).

cnf(t549,plain,
    ifeq(c_Complex_Ocomplex_OComplex(X1,X2),sF9,X2,c_Transcendental_Osin(sF3)) = c_Transcendental_Osin(sF3),
    inference(orient,[status(thm)],[t15695]) ).

cnf(f879,negated_conjecture,
    c_Complex_Ocomplex_OComplex(c_Transcendental_Ocos(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal)),c_Transcendental_Osin(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal))) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_0) ).

fof(f879_nnf,plain,
    c_Complex_Ocomplex_OComplex(c_Transcendental_Ocos(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal)),c_Transcendental_Osin(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal))) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
    inference(nnf_transformation,[status(thm)],[f879]) ).

cnf(c879,plain,
    c_Complex_Ocomplex_OComplex(c_Transcendental_Ocos(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal)),c_Transcendental_Osin(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal))) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
    inference(cnf_transformation,[status(esa)],[f879_nnf]) ).

cnf(t182,plain,
    c_Complex_Ocomplex_OComplex(c_Transcendental_Ocos(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal)),c_Transcendental_Osin(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal))) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
    inference(equality_encoding,[status(esa)],[c879]) ).

cnf(t16493,plain,
    c_Complex_Ocomplex_OComplex(c_Transcendental_Ocos(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal)),c_Transcendental_Osin(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal))) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
    inference(step,[status(thm)],[t182,t341]) ).

cnf(t16494,plain,
    c_Complex_Ocomplex_OComplex(c_Transcendental_Ocos(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF0),tc_RealDef_Oreal),tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal)),c_Transcendental_Osin(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal))) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
    inference(step,[status(thm)],[t16493,t262]) ).

cnf(t16495,plain,
    c_Complex_Ocomplex_OComplex(c_Transcendental_Ocos(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(sF1,tc_RealDef_Oreal),tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal)),c_Transcendental_Osin(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal))) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
    inference(step,[status(thm)],[t16494,t270]) ).

cnf(t16496,plain,
    c_Complex_Ocomplex_OComplex(c_Transcendental_Ocos(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,sF2,tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal)),c_Transcendental_Osin(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal))) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
    inference(step,[status(thm)],[t16495,t306]) ).

cnf(t16497,plain,
    c_Complex_Ocomplex_OComplex(c_Transcendental_Ocos(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(sF2,c_Transcendental_Opi,tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal)),c_Transcendental_Osin(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal))) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
    inference(step,[status(thm)],[t16496,t341]) ).

cnf(t16498,plain,
    c_Complex_Ocomplex_OComplex(c_Transcendental_Ocos(c_HOL_Oinverse__class_Odivide(sF3,c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal)),c_Transcendental_Osin(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal))) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
    inference(step,[status(thm)],[t16497,t403]) ).

cnf(t242,axiom,
    sF4 = c_RealDef_Oreal(v_n,tc_nat),
    introduced(definition) ).

cnf(t271,plain,
    c_RealDef_Oreal(v_n,tc_nat) = sF4,
    inference(orient,[status(thm)],[t242]) ).

cnf(t16499,plain,
    c_Complex_Ocomplex_OComplex(c_Transcendental_Ocos(c_HOL_Oinverse__class_Odivide(sF3,sF4,tc_RealDef_Oreal)),c_Transcendental_Osin(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal))) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
    inference(step,[status(thm)],[t16498,t271]) ).

cnf(t16500,plain,
    c_Complex_Ocomplex_OComplex(c_Transcendental_Ocos(c_HOL_Oinverse__class_Odivide(sF3,sF4,tc_RealDef_Oreal)),c_Transcendental_Osin(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal))) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
    inference(step,[status(thm)],[t16499,t341]) ).

cnf(t16501,plain,
    c_Complex_Ocomplex_OComplex(c_Transcendental_Ocos(c_HOL_Oinverse__class_Odivide(sF3,sF4,tc_RealDef_Oreal)),c_Transcendental_Osin(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF0),tc_RealDef_Oreal),tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal))) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
    inference(step,[status(thm)],[t16500,t262]) ).

cnf(t16502,plain,
    c_Complex_Ocomplex_OComplex(c_Transcendental_Ocos(c_HOL_Oinverse__class_Odivide(sF3,sF4,tc_RealDef_Oreal)),c_Transcendental_Osin(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(sF1,tc_RealDef_Oreal),tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal))) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
    inference(step,[status(thm)],[t16501,t270]) ).

cnf(t16503,plain,
    c_Complex_Ocomplex_OComplex(c_Transcendental_Ocos(c_HOL_Oinverse__class_Odivide(sF3,sF4,tc_RealDef_Oreal)),c_Transcendental_Osin(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,sF2,tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal))) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
    inference(step,[status(thm)],[t16502,t306]) ).

cnf(t16504,plain,
    c_Complex_Ocomplex_OComplex(c_Transcendental_Ocos(c_HOL_Oinverse__class_Odivide(sF3,sF4,tc_RealDef_Oreal)),c_Transcendental_Osin(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(sF2,c_Transcendental_Opi,tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal))) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
    inference(step,[status(thm)],[t16503,t341]) ).

cnf(t16505,plain,
    c_Complex_Ocomplex_OComplex(c_Transcendental_Ocos(c_HOL_Oinverse__class_Odivide(sF3,sF4,tc_RealDef_Oreal)),c_Transcendental_Osin(c_HOL_Oinverse__class_Odivide(sF3,c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal))) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
    inference(step,[status(thm)],[t16504,t403]) ).

cnf(t16506,plain,
    c_Complex_Ocomplex_OComplex(c_Transcendental_Ocos(c_HOL_Oinverse__class_Odivide(sF3,sF4,tc_RealDef_Oreal)),c_Transcendental_Osin(c_HOL_Oinverse__class_Odivide(sF3,sF4,tc_RealDef_Oreal))) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
    inference(step,[status(thm)],[t16505,t271]) ).

cnf(t16507,plain,
    c_Complex_Ocomplex_OComplex(c_Transcendental_Ocos(c_HOL_Oinverse__class_Odivide(sF3,sF4,tc_RealDef_Oreal)),c_Transcendental_Osin(c_HOL_Oinverse__class_Odivide(sF3,sF4,tc_RealDef_Oreal))) = sF9,
    inference(step,[status(thm)],[t16506,t263]) ).

cnf(t14727,plain,
    c_Complex_Ocomplex_OComplex(c_Transcendental_Ocos(c_HOL_Oinverse__class_Odivide(sF3,sF4,tc_RealDef_Oreal)),c_Transcendental_Osin(c_HOL_Oinverse__class_Odivide(sF3,sF4,tc_RealDef_Oreal))) = sF9,
    inference(orient,[status(thm)],[t16507]) ).

cnf(f729,axiom,
    ( V_a = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)
    | c_Complex_Ocomplex_OComplex(V_a,V_b) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Complex__eq__0_0) ).

fof(f729_nnf,plain,
    ! [V_a,V_b] :
      ( V_a = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)
      | c_Complex_Ocomplex_OComplex(V_a,V_b) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
    inference(nnf_transformation,[status(thm)],[f729]) ).

fof(f729_sk,plain,
    ! [V_a,V_b] :
      ( V_a = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)
      | c_Complex_Ocomplex_OComplex(V_a,V_b) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
    inference(skolemisation,[status(esa)],[f729_nnf]) ).

cnf(c729,plain,
    ( X0 = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)
    | c_Complex_Ocomplex_OComplex(X0,X1) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
    inference(cnf_transformation,[status(esa)],[f729_sk]) ).

cnf(t77,plain,
    ifeq(c_Complex_Ocomplex_OComplex(X1,X2),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),X1,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
    inference(equality_encoding,[status(esa)],[c729]) ).

cnf(t15687,plain,
    ifeq(c_Complex_Ocomplex_OComplex(X1,X2),sF9,X1,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
    inference(step,[status(thm)],[t77,t263]) ).

cnf(t15688,plain,
    ifeq(c_Complex_Ocomplex_OComplex(X1,X2),sF9,X1,c_Transcendental_Osin(sF3)) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
    inference(step,[status(thm)],[t15687,t482]) ).

cnf(t15689,plain,
    ifeq(c_Complex_Ocomplex_OComplex(X1,X2),sF9,X1,c_Transcendental_Osin(sF3)) = c_Transcendental_Osin(sF3),
    inference(step,[status(thm)],[t15688,t482]) ).

cnf(t540,plain,
    ifeq(c_Complex_Ocomplex_OComplex(X1,X2),sF9,X1,c_Transcendental_Osin(sF3)) = c_Transcendental_Osin(sF3),
    inference(orient,[status(thm)],[t15689]) ).

cnf(t14732,plain,
    c_Transcendental_Osin(sF3) = ifeq(sF9,sF9,c_Transcendental_Ocos(c_HOL_Oinverse__class_Odivide(sF3,sF4,tc_RealDef_Oreal)),c_Transcendental_Osin(sF3)),
    inference(cp,[status(thm)],[t540,t14727]) ).

cnf(t33,plain,
    ifeq(X1,X1,X2,X3) = X2,
    introduced(definition) ).

cnf(t297,plain,
    ifeq(X1,X1,X2,X3) = X2,
    inference(orient,[status(thm)],[t33]) ).

cnf(t16508,plain,
    c_Transcendental_Osin(sF3) = c_Transcendental_Ocos(c_HOL_Oinverse__class_Odivide(sF3,sF4,tc_RealDef_Oreal)),
    inference(step,[status(thm)],[t14732,t297]) ).

cnf(t14734,plain,
    c_Transcendental_Ocos(c_HOL_Oinverse__class_Odivide(sF3,sF4,tc_RealDef_Oreal)) = c_Transcendental_Osin(sF3),
    inference(orient,[status(thm)],[t16508]) ).

cnf(t16509,plain,
    c_Complex_Ocomplex_OComplex(c_Transcendental_Osin(sF3),c_Transcendental_Osin(c_HOL_Oinverse__class_Odivide(sF3,sF4,tc_RealDef_Oreal))) = sF9,
    inference(step,[status(thm)],[t14727,t14734]) ).

cnf(t14735,plain,
    c_Complex_Ocomplex_OComplex(c_Transcendental_Osin(sF3),c_Transcendental_Osin(c_HOL_Oinverse__class_Odivide(sF3,sF4,tc_RealDef_Oreal))) = sF9,
    inference(rw,[status(thm)],[t16509]) ).

cnf(t14756,plain,
    c_Complex_Ocomplex_OComplex(c_Transcendental_Osin(sF3),c_Transcendental_Osin(c_HOL_Oinverse__class_Odivide(sF3,sF4,tc_RealDef_Oreal))) = sF9,
    inference(orient,[status(thm)],[t14735]) ).

cnf(t14759,plain,
    c_Transcendental_Osin(sF3) = ifeq(sF9,sF9,c_Transcendental_Osin(c_HOL_Oinverse__class_Odivide(sF3,sF4,tc_RealDef_Oreal)),c_Transcendental_Osin(sF3)),
    inference(cp,[status(thm)],[t549,t14756]) ).

cnf(t16510,plain,
    c_Transcendental_Osin(sF3) = c_Transcendental_Osin(c_HOL_Oinverse__class_Odivide(sF3,sF4,tc_RealDef_Oreal)),
    inference(step,[status(thm)],[t14759,t297]) ).

cnf(t14760,plain,
    c_Transcendental_Osin(c_HOL_Oinverse__class_Odivide(sF3,sF4,tc_RealDef_Oreal)) = c_Transcendental_Osin(sF3),
    inference(orient,[status(thm)],[t16510]) ).

cnf(t14763,plain,
    c_Transcendental_Ocos(sF3) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(c_HOL_Oinverse__class_Odivide(sF3,sF4,tc_RealDef_Oreal)),c_Transcendental_Ocos(c_HOL_Oinverse__class_Odivide(sF3,sF4,tc_RealDef_Oreal)),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(sF3),c_Transcendental_Osin(c_HOL_Oinverse__class_Odivide(sF3,sF4,tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(cp,[status(thm)],[t1907,t14760]) ).

cnf(t16511,plain,
    c_Transcendental_Ocos(sF3) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(sF3),c_Transcendental_Ocos(c_HOL_Oinverse__class_Odivide(sF3,sF4,tc_RealDef_Oreal)),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(sF3),c_Transcendental_Osin(c_HOL_Oinverse__class_Odivide(sF3,sF4,tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(step,[status(thm)],[t14763,t14734]) ).

cnf(t856,plain,
    c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(X1,X2,tc_RealDef_Oreal),X3,tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(X3,X1,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X3,X2,tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(cp,[status(thm)],[t855,t341]) ).

cnf(t1687,plain,
    c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(X1,X2,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X1,X3,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(X2,X3,tc_RealDef_Oreal),X1,tc_RealDef_Oreal),
    inference(orient,[status(thm)],[t856]) ).

cnf(t16512,plain,
    c_Transcendental_Ocos(sF3) = c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(c_Transcendental_Ocos(c_HOL_Oinverse__class_Odivide(sF3,sF4,tc_RealDef_Oreal)),c_Transcendental_Osin(c_HOL_Oinverse__class_Odivide(sF3,sF4,tc_RealDef_Oreal)),tc_RealDef_Oreal),c_Transcendental_Osin(sF3),tc_RealDef_Oreal),
    inference(step,[status(thm)],[t16511,t1687]) ).

cnf(t16513,plain,
    c_Transcendental_Ocos(sF3) = c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(sF3),c_HOL_Oplus__class_Oplus(c_Transcendental_Ocos(c_HOL_Oinverse__class_Odivide(sF3,sF4,tc_RealDef_Oreal)),c_Transcendental_Osin(c_HOL_Oinverse__class_Odivide(sF3,sF4,tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(step,[status(thm)],[t16512,t341]) ).

cnf(t16514,plain,
    c_Transcendental_Ocos(sF3) = c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(sF3),c_HOL_Oplus__class_Oplus(c_Transcendental_Osin(sF3),c_Transcendental_Osin(c_HOL_Oinverse__class_Odivide(sF3,sF4,tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(step,[status(thm)],[t16513,t14734]) ).

cnf(t16515,plain,
    c_Transcendental_Ocos(sF3) = c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(sF3),c_HOL_Oplus__class_Oplus(sF2,c_Transcendental_Osin(c_HOL_Oinverse__class_Odivide(sF3,sF4,tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(step,[status(thm)],[t16514,t13186]) ).

cnf(t16516,plain,
    c_Transcendental_Ocos(sF3) = c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(sF3),c_HOL_Oplus__class_Oplus(sF2,c_Transcendental_Osin(sF3),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(step,[status(thm)],[t16515,t14760]) ).

cnf(t11210,plain,
    c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(X1,sF2,tc_RealDef_Oreal),c_Transcendental_Osin(sF3),tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(X1,c_Transcendental_Osin(sF3),tc_RealDef_Oreal),c_Transcendental_Osin(sF3),tc_RealDef_Oreal),
    inference(cp,[status(thm)],[t583,t11198]) ).

cnf(t16400,plain,
    c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(sF3),c_HOL_Oplus__class_Oplus(X1,sF2,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(X1,c_Transcendental_Osin(sF3),tc_RealDef_Oreal),c_Transcendental_Osin(sF3),tc_RealDef_Oreal),
    inference(step,[status(thm)],[t11210,t341]) ).

cnf(t1863,plain,
    c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(X1,c_Transcendental_Osin(sF3),tc_RealDef_Oreal),c_Transcendental_Osin(sF3),tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(X1,c_Transcendental_Osin(sF3),tc_RealDef_Oreal),c_Transcendental_Osin(sF3),tc_RealDef_Oreal),
    inference(cp,[status(thm)],[t583,t1857]) ).

cnf(t15858,plain,
    c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(sF3),c_HOL_Oplus__class_Oplus(X1,c_Transcendental_Osin(sF3),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(X1,c_Transcendental_Osin(sF3),tc_RealDef_Oreal),c_Transcendental_Osin(sF3),tc_RealDef_Oreal),
    inference(step,[status(thm)],[t1863,t341]) ).

cnf(t1935,plain,
    c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(X1,c_Transcendental_Osin(sF3),tc_RealDef_Oreal),c_Transcendental_Osin(sF3),tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(sF3),c_HOL_Oplus__class_Oplus(X1,c_Transcendental_Osin(sF3),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(orient,[status(thm)],[t15858]) ).

cnf(t16401,plain,
    c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(sF3),c_HOL_Oplus__class_Oplus(X1,sF2,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(sF3),c_HOL_Oplus__class_Oplus(X1,c_Transcendental_Osin(sF3),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(step,[status(thm)],[t16400,t1935]) ).

cnf(t13368,plain,
    c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(sF3),c_HOL_Oplus__class_Oplus(X1,c_Transcendental_Osin(sF3),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(sF3),c_HOL_Oplus__class_Oplus(X1,sF2,tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(orient,[status(thm)],[t16401]) ).

cnf(t16517,plain,
    c_Transcendental_Ocos(sF3) = c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(sF3),c_HOL_Oplus__class_Oplus(sF2,sF2,tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(step,[status(thm)],[t16516,t13368]) ).

cnf(t11214,plain,
    c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(c_Transcendental_Osin(sF3),X1,tc_RealDef_Oreal),sF2,tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(c_Transcendental_Osin(sF3),c_HOL_Otimes__class_Otimes(X1,sF2,tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(cp,[status(thm)],[t855,t11198]) ).

cnf(t16284,plain,
    c_HOL_Otimes__class_Otimes(sF2,c_HOL_Oplus__class_Oplus(c_Transcendental_Osin(sF3),X1,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(c_Transcendental_Osin(sF3),c_HOL_Otimes__class_Otimes(X1,sF2,tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(step,[status(thm)],[t11214,t341]) ).

cnf(t11586,plain,
    c_HOL_Oplus__class_Oplus(c_Transcendental_Osin(sF3),c_HOL_Otimes__class_Otimes(X1,sF2,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(sF2,c_HOL_Oplus__class_Oplus(c_Transcendental_Osin(sF3),X1,tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(orient,[status(thm)],[t16284]) ).

cnf(t11589,plain,
    c_HOL_Otimes__class_Otimes(sF2,c_HOL_Oplus__class_Oplus(c_Transcendental_Osin(sF3),c_Transcendental_Ocos(sF3),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(c_Transcendental_Osin(sF3),sF2,tc_RealDef_Oreal),
    inference(cp,[status(thm)],[t11586,t464]) ).

cnf(t1913,plain,
    c_Transcendental_Ocos(sF3) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(sF3),c_Transcendental_Ocos(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,sF2,tc_RealDef_Oreal)),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,sF2,tc_RealDef_Oreal)),c_Transcendental_Osin(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,sF2,tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(cp,[status(thm)],[t1907,t512]) ).

cnf(t15852,plain,
    c_Transcendental_Ocos(sF3) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(sF3),c_Transcendental_Osin(sF3),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,sF2,tc_RealDef_Oreal)),c_Transcendental_Osin(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,sF2,tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(step,[status(thm)],[t1913,t512]) ).

cnf(t15853,plain,
    c_Transcendental_Ocos(sF3) = c_HOL_Oplus__class_Oplus(c_Transcendental_Osin(sF3),c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,sF2,tc_RealDef_Oreal)),c_Transcendental_Osin(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,sF2,tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(step,[status(thm)],[t15852,t1857]) ).

cnf(t15854,plain,
    c_Transcendental_Ocos(sF3) = c_HOL_Oplus__class_Oplus(c_Transcendental_Osin(sF3),c_HOL_Otimes__class_Otimes(c_Transcendental_Ocos(sF3),c_Transcendental_Osin(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,sF2,tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(step,[status(thm)],[t15853,t480]) ).

cnf(t15855,plain,
    c_Transcendental_Ocos(sF3) = c_HOL_Oplus__class_Oplus(c_Transcendental_Osin(sF3),c_Transcendental_Osin(c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,sF2,tc_RealDef_Oreal)),tc_RealDef_Oreal),
    inference(step,[status(thm)],[t15854,t464]) ).

cnf(t15856,plain,
    c_Transcendental_Ocos(sF3) = c_HOL_Oplus__class_Oplus(c_Transcendental_Osin(sF3),c_Transcendental_Ocos(sF3),tc_RealDef_Oreal),
    inference(step,[status(thm)],[t15855,t480]) ).

cnf(t1931,plain,
    c_HOL_Oplus__class_Oplus(c_Transcendental_Osin(sF3),c_Transcendental_Ocos(sF3),tc_RealDef_Oreal) = c_Transcendental_Ocos(sF3),
    inference(orient,[status(thm)],[t15856]) ).

cnf(t16285,plain,
    c_HOL_Otimes__class_Otimes(sF2,c_Transcendental_Ocos(sF3),tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(c_Transcendental_Osin(sF3),sF2,tc_RealDef_Oreal),
    inference(step,[status(thm)],[t11589,t1931]) ).

cnf(t342,plain,
    c_HOL_Otimes__class_Otimes(X1,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal) = X1,
    inference(cp,[status(thm)],[t341,t284]) ).

cnf(t343,plain,
    c_HOL_Otimes__class_Otimes(X1,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal) = X1,
    inference(orient,[status(thm)],[t342]) ).

cnf(t15623,plain,
    c_HOL_Otimes__class_Otimes(X1,c_Transcendental_Ocos(sF3),tc_RealDef_Oreal) = X1,
    inference(step,[status(thm)],[t343,t449]) ).

cnf(t457,plain,
    c_HOL_Otimes__class_Otimes(X1,c_Transcendental_Ocos(sF3),tc_RealDef_Oreal) = X1,
    inference(rw,[status(thm)],[t15623]) ).

cnf(t468,plain,
    c_HOL_Otimes__class_Otimes(X1,c_Transcendental_Ocos(sF3),tc_RealDef_Oreal) = X1,
    inference(orient,[status(thm)],[t457]) ).

cnf(t16286,plain,
    sF2 = c_HOL_Oplus__class_Oplus(c_Transcendental_Osin(sF3),sF2,tc_RealDef_Oreal),
    inference(step,[status(thm)],[t16285,t468]) ).

cnf(t11609,plain,
    c_HOL_Oplus__class_Oplus(c_Transcendental_Osin(sF3),sF2,tc_RealDef_Oreal) = sF2,
    inference(orient,[status(thm)],[t16286]) ).

cnf(t13199,plain,
    c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(sF3),c_HOL_Oplus__class_Oplus(sF2,sF2,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(sF3),sF2,tc_RealDef_Oreal),
    inference(cp,[status(thm)],[t13186,t11609]) ).

cnf(t16393,plain,
    c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(sF3),c_HOL_Oplus__class_Oplus(sF2,sF2,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(sF2,c_Transcendental_Osin(sF3),tc_RealDef_Oreal),
    inference(step,[status(thm)],[t13199,t341]) ).

cnf(t16394,plain,
    c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(sF3),c_HOL_Oplus__class_Oplus(sF2,sF2,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_Transcendental_Osin(sF3),
    inference(step,[status(thm)],[t16393,t11198]) ).

cnf(t13333,plain,
    c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(sF3),c_HOL_Oplus__class_Oplus(sF2,sF2,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_Transcendental_Osin(sF3),
    inference(orient,[status(thm)],[t16394]) ).

cnf(t16518,plain,
    c_Transcendental_Ocos(sF3) = c_Transcendental_Osin(sF3),
    inference(step,[status(thm)],[t16517,t13333]) ).

cnf(t14773,plain,
    c_Transcendental_Ocos(sF3) = c_Transcendental_Osin(sF3),
    inference(orient,[status(thm)],[t16518]) ).

cnf(t16521,plain,
    c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(sF3),X1,tc_RealDef_Oreal) = X1,
    inference(step,[status(thm)],[t464,t14773]) ).

cnf(t14776,plain,
    c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(sF3),X1,tc_RealDef_Oreal) = X1,
    inference(rw,[status(thm)],[t16521]) ).

cnf(t14960,plain,
    c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(sF3),X1,tc_RealDef_Oreal) = X1,
    inference(orient,[status(thm)],[t14776]) ).

cnf(t16584,plain,
    c_HOL_Oplus__class_Oplus(c_Transcendental_Osin(sF3),c_HOL_Otimes__class_Otimes(X1,c_Transcendental_Osin(sF3),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(sF2,X1,tc_RealDef_Oreal),
    inference(step,[status(thm)],[t13187,t14960]) ).

cnf(t14964,plain,
    c_HOL_Oplus__class_Oplus(c_Transcendental_Osin(sF3),c_HOL_Otimes__class_Otimes(X1,c_Transcendental_Osin(sF3),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(sF2,X1,tc_RealDef_Oreal),
    inference(orient,[status(thm)],[t16584]) ).

cnf(t15030,plain,
    c_HOL_Oplus__class_Oplus(sF2,c_Transcendental_Osin(sF3),tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(c_Transcendental_Osin(sF3),c_Transcendental_Osin(sF3),tc_RealDef_Oreal),
    inference(cp,[status(thm)],[t14964,t14960]) ).

cnf(t585,plain,
    c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(X1,X2,tc_RealDef_Oreal),X3,tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(X1,X3,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X3,X2,tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(cp,[status(thm)],[t583,t341]) ).

cnf(t951,plain,
    c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(X1,X2,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X2,X3,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(X1,X3,tc_RealDef_Oreal),X2,tc_RealDef_Oreal),
    inference(orient,[status(thm)],[t585]) ).

cnf(t11216,plain,
    c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(X1,c_Transcendental_Osin(sF3),tc_RealDef_Oreal),sF2,tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(X1,sF2,tc_RealDef_Oreal),c_Transcendental_Osin(sF3),tc_RealDef_Oreal),
    inference(cp,[status(thm)],[t951,t11198]) ).

cnf(t16297,plain,
    c_HOL_Otimes__class_Otimes(sF2,c_HOL_Oplus__class_Oplus(X1,c_Transcendental_Osin(sF3),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(X1,sF2,tc_RealDef_Oreal),c_Transcendental_Osin(sF3),tc_RealDef_Oreal),
    inference(step,[status(thm)],[t11216,t341]) ).

cnf(t11736,plain,
    c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(X1,sF2,tc_RealDef_Oreal),c_Transcendental_Osin(sF3),tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(sF2,c_HOL_Oplus__class_Oplus(X1,c_Transcendental_Osin(sF3),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(orient,[status(thm)],[t16297]) ).

cnf(t11739,plain,
    c_HOL_Otimes__class_Otimes(sF2,c_HOL_Oplus__class_Oplus(c_Transcendental_Ocos(sF3),c_Transcendental_Osin(sF3),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(sF2,c_Transcendental_Osin(sF3),tc_RealDef_Oreal),
    inference(cp,[status(thm)],[t11736,t464]) ).

cnf(t1914,plain,
    c_Transcendental_Ocos(sF3) = c_HOL_Oplus__class_Oplus(c_Transcendental_Ocos(sF3),c_HOL_Otimes__class_Otimes(c_Transcendental_Osin(sF3),c_Transcendental_Osin(sF3),tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(cp,[status(thm)],[t1907,t464]) ).

cnf(t15857,plain,
    c_Transcendental_Ocos(sF3) = c_HOL_Oplus__class_Oplus(c_Transcendental_Ocos(sF3),c_Transcendental_Osin(sF3),tc_RealDef_Oreal),
    inference(step,[status(thm)],[t1914,t1857]) ).

cnf(t1933,plain,
    c_HOL_Oplus__class_Oplus(c_Transcendental_Ocos(sF3),c_Transcendental_Osin(sF3),tc_RealDef_Oreal) = c_Transcendental_Ocos(sF3),
    inference(orient,[status(thm)],[t15857]) ).

cnf(t16298,plain,
    c_HOL_Otimes__class_Otimes(sF2,c_Transcendental_Ocos(sF3),tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(sF2,c_Transcendental_Osin(sF3),tc_RealDef_Oreal),
    inference(step,[status(thm)],[t11739,t1933]) ).

cnf(t16299,plain,
    sF2 = c_HOL_Oplus__class_Oplus(sF2,c_Transcendental_Osin(sF3),tc_RealDef_Oreal),
    inference(step,[status(thm)],[t16298,t468]) ).

cnf(t11758,plain,
    c_HOL_Oplus__class_Oplus(sF2,c_Transcendental_Osin(sF3),tc_RealDef_Oreal) = sF2,
    inference(orient,[status(thm)],[t16299]) ).

cnf(t16604,plain,
    sF2 = c_HOL_Oplus__class_Oplus(c_Transcendental_Osin(sF3),c_Transcendental_Osin(sF3),tc_RealDef_Oreal),
    inference(step,[status(thm)],[t15030,t11758]) ).

cnf(t16605,plain,
    sF2 = c_Transcendental_Osin(sF3),
    inference(step,[status(thm)],[t16604,t1131]) ).

cnf(t15082,plain,
    c_Transcendental_Osin(sF3) = sF2,
    inference(orient,[status(thm)],[t16605]) ).

cnf(t16630,plain,
    eq(c_Transcendental_Ocos(sF2),sF2) = false,
    inference(step,[status(thm)],[t533,t15082]) ).

cnf(t15109,plain,
    eq(c_Transcendental_Ocos(sF2),sF2) = false,
    inference(rw,[status(thm)],[t16630]) ).

cnf(f775,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(f775_nnf,plain,
    c_Transcendental_Ocos(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)) = c_HOL_Oone__class_Oone(tc_RealDef_Oreal),
    inference(nnf_transformation,[status(thm)],[f775]) ).

cnf(c775,plain,
    c_Transcendental_Ocos(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)) = c_HOL_Oone__class_Oone(tc_RealDef_Oreal),
    inference(cnf_transformation,[status(esa)],[f775_nnf]) ).

cnf(t19,plain,
    c_Transcendental_Ocos(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)) = c_HOL_Oone__class_Oone(tc_RealDef_Oreal),
    inference(equality_encoding,[status(esa)],[c775]) ).

cnf(t15557,plain,
    c_Transcendental_Ocos(c_Transcendental_Osin(c_Transcendental_Opi)) = c_HOL_Oone__class_Oone(tc_RealDef_Oreal),
    inference(step,[status(thm)],[t19,t261]) ).

cnf(t267,plain,
    c_Transcendental_Ocos(c_Transcendental_Osin(c_Transcendental_Opi)) = c_HOL_Oone__class_Oone(tc_RealDef_Oreal),
    inference(orient,[status(thm)],[t15557]) ).

cnf(t15616,plain,
    c_Transcendental_Ocos(c_Transcendental_Osin(c_Transcendental_Opi)) = c_Transcendental_Ocos(sF3),
    inference(step,[status(thm)],[t267,t449]) ).

cnf(t450,plain,
    c_Transcendental_Ocos(c_Transcendental_Osin(c_Transcendental_Opi)) = c_Transcendental_Ocos(sF3),
    inference(orient,[status(thm)],[t15616]) ).

cnf(t15650,plain,
    c_Transcendental_Ocos(c_Transcendental_Osin(sF3)) = c_Transcendental_Ocos(sF3),
    inference(step,[status(thm)],[t450,t481]) ).

cnf(t484,plain,
    c_Transcendental_Ocos(c_Transcendental_Osin(sF3)) = c_Transcendental_Ocos(sF3),
    inference(rw,[status(thm)],[t15650]) ).

cnf(t520,plain,
    c_Transcendental_Ocos(c_Transcendental_Osin(sF3)) = c_Transcendental_Ocos(sF3),
    inference(orient,[status(thm)],[t484]) ).

cnf(t16529,plain,
    c_Transcendental_Ocos(c_Transcendental_Osin(sF3)) = c_Transcendental_Osin(sF3),
    inference(step,[status(thm)],[t520,t14773]) ).

cnf(t14784,plain,
    c_Transcendental_Ocos(c_Transcendental_Osin(sF3)) = c_Transcendental_Osin(sF3),
    inference(orient,[status(thm)],[t16529]) ).

cnf(t15099,plain,
    c_Transcendental_Ocos(sF2) = c_Transcendental_Osin(sF3),
    inference(rw,[status(thm)],[t14784]) ).

cnf(t16781,plain,
    c_Transcendental_Ocos(sF2) = sF2,
    inference(step,[status(thm)],[t15099,t15082]) ).

cnf(t15316,plain,
    c_Transcendental_Ocos(sF2) = sF2,
    inference(orient,[status(thm)],[t16781]) ).

cnf(t16819,plain,
    eq(sF2,sF2) = false,
    inference(step,[status(thm)],[t15109,t15316]) ).

cnf(t15,plain,
    eq(X1,X1) = true,
    introduced(definition) ).

cnf(t264,plain,
    eq(X1,X1) = true,
    inference(orient,[status(thm)],[t15]) ).

cnf(t16820,plain,
    true = false,
    inference(step,[status(thm)],[t16819,t264]) ).

cnf(t15489,plain,
    false = true,
    inference(orient,[status(thm)],[t16820]) ).

cnf(f60,axiom,
    ( ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
    | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
    | ~ class_Orderings_Oorder(T_a) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_xt1_I9_J_0) ).

fof(f60_nnf,plain,
    ! [T_a,V_a,V_b] :
      ( ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
      | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
      | ~ class_Orderings_Oorder(T_a) ),
    inference(nnf_transformation,[status(thm)],[f60]) ).

fof(f60_sk,plain,
    ! [T_a,V_a,V_b] :
      ( ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
      | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
      | ~ class_Orderings_Oorder(T_a) ),
    inference(skolemisation,[status(esa)],[f60_nnf]) ).

cnf(c60,plain,
    ( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
    | ~ c_HOL_Oord__class_Oless(X1,X2,X0)
    | ~ class_Orderings_Oorder(X0) ),
    inference(cnf_transformation,[status(esa)],[f60_sk]) ).

cnf(f61,axiom,
    ( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
    | ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
    | ~ class_Orderings_Olinorder(T_a) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__less__iff__gr__or__eq_1) ).

fof(f61_nnf,plain,
    ! [T_a,V_x,V_y] :
      ( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
      | ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
      | ~ class_Orderings_Olinorder(T_a) ),
    inference(nnf_transformation,[status(thm)],[f61]) ).

fof(f61_sk,plain,
    ! [T_a,V_x,V_y] :
      ( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
      | ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
      | ~ class_Orderings_Olinorder(T_a) ),
    inference(skolemisation,[status(esa)],[f61_nnf]) ).

cnf(c61,plain,
    ( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
    | ~ c_HOL_Oord__class_Oless(X1,X2,X0)
    | ~ class_Orderings_Olinorder(X0) ),
    inference(cnf_transformation,[status(esa)],[f61_sk]) ).

cnf(f64,axiom,
    ( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
    | ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
    | ~ class_Orderings_Opreorder(T_a) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_order__less__asym_0) ).

fof(f64_nnf,plain,
    ! [T_a,V_y,V_x] :
      ( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
      | ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
      | ~ class_Orderings_Opreorder(T_a) ),
    inference(nnf_transformation,[status(thm)],[f64]) ).

fof(f64_sk,plain,
    ! [T_a,V_y,V_x] :
      ( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
      | ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
      | ~ class_Orderings_Opreorder(T_a) ),
    inference(skolemisation,[status(esa)],[f64_nnf]) ).

cnf(c64,plain,
    ( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
    | ~ c_HOL_Oord__class_Oless(X1,X2,X0)
    | ~ class_Orderings_Opreorder(X0) ),
    inference(cnf_transformation,[status(esa)],[f64_sk]) ).

cnf(f65,axiom,
    ( ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
    | ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
    | ~ class_Orderings_Opreorder(T_a) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_order__less__asym_H_0) ).

fof(f65_nnf,plain,
    ! [T_a,V_b,V_a] :
      ( ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
      | ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
      | ~ class_Orderings_Opreorder(T_a) ),
    inference(nnf_transformation,[status(thm)],[f65]) ).

fof(f65_sk,plain,
    ! [T_a,V_b,V_a] :
      ( ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
      | ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
      | ~ class_Orderings_Opreorder(T_a) ),
    inference(skolemisation,[status(esa)],[f65_nnf]) ).

cnf(c65,plain,
    ( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
    | ~ c_HOL_Oord__class_Oless(X1,X2,X0)
    | ~ class_Orderings_Opreorder(X0) ),
    inference(cnf_transformation,[status(esa)],[f65_sk]) ).

cnf(f98,axiom,
    ( ~ c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(V_a,V_a,T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
    | ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__square__less__zero_0) ).

fof(f98_nnf,plain,
    ! [T_a,V_a] :
      ( ~ c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(V_a,V_a,T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
      | ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
    inference(nnf_transformation,[status(thm)],[f98]) ).

fof(f98_sk,plain,
    ! [T_a,V_a] :
      ( ~ c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(V_a,V_a,T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
      | ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
    inference(skolemisation,[status(esa)],[f98_nnf]) ).

cnf(c98,plain,
    ( ~ c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(X1,X1,X0),c_HOL_Ozero__class_Ozero(X0),X0)
    | ~ class_Ring__and__Field_Oordered__ring__strict(X0) ),
    inference(cnf_transformation,[status(esa)],[f98_sk]) ).

cnf(f111,axiom,
    ( ~ c_HOL_Oord__class_Oless(c_HOL_Oone__class_Oone(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
    | ~ class_Ring__and__Field_Oordered__semidom(T_a) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__one__less__zero_0) ).

fof(f111_nnf,plain,
    ! [T_a] :
      ( ~ c_HOL_Oord__class_Oless(c_HOL_Oone__class_Oone(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
      | ~ class_Ring__and__Field_Oordered__semidom(T_a) ),
    inference(nnf_transformation,[status(thm)],[f111]) ).

fof(f111_sk,plain,
    ! [T_a] :
      ( ~ c_HOL_Oord__class_Oless(c_HOL_Oone__class_Oone(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
      | ~ class_Ring__and__Field_Oordered__semidom(T_a) ),
    inference(skolemisation,[status(esa)],[f111_nnf]) ).

cnf(c111,plain,
    ( ~ c_HOL_Oord__class_Oless(c_HOL_Oone__class_Oone(X0),c_HOL_Ozero__class_Ozero(X0),X0)
    | ~ class_Ring__and__Field_Oordered__semidom(X0) ),
    inference(cnf_transformation,[status(esa)],[f111_sk]) ).

cnf(f113,axiom,
    ( ~ c_lessequals(c_HOL_Oone__class_Oone(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
    | ~ class_Ring__and__Field_Oordered__semidom(T_a) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__one__le__zero_0) ).

fof(f113_nnf,plain,
    ! [T_a] :
      ( ~ c_lessequals(c_HOL_Oone__class_Oone(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
      | ~ class_Ring__and__Field_Oordered__semidom(T_a) ),
    inference(nnf_transformation,[status(thm)],[f113]) ).

fof(f113_sk,plain,
    ! [T_a] :
      ( ~ c_lessequals(c_HOL_Oone__class_Oone(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
      | ~ class_Ring__and__Field_Oordered__semidom(T_a) ),
    inference(skolemisation,[status(esa)],[f113_nnf]) ).

cnf(c113,plain,
    ( ~ c_lessequals(c_HOL_Oone__class_Oone(X0),c_HOL_Ozero__class_Ozero(X0),X0)
    | ~ class_Ring__and__Field_Oordered__semidom(X0) ),
    inference(cnf_transformation,[status(esa)],[f113_sk]) ).

cnf(f194,axiom,
    ( ~ c_lessequals(c_Int_Onumber__class_Onumber__of(V_v,T_a),c_Int_Onumber__class_Onumber__of(V_w,T_a),T_a)
    | ~ c_HOL_Oord__class_Oless(c_Int_Onumber__class_Onumber__of(V_w,T_a),c_Int_Onumber__class_Onumber__of(V_v,T_a),T_a)
    | ~ class_Int_Onumber(T_a)
    | ~ class_Orderings_Olinorder(T_a) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_le__number__of__eq__not__less_0) ).

fof(f194_nnf,plain,
    ! [T_a,V_w,V_v] :
      ( ~ c_lessequals(c_Int_Onumber__class_Onumber__of(V_v,T_a),c_Int_Onumber__class_Onumber__of(V_w,T_a),T_a)
      | ~ c_HOL_Oord__class_Oless(c_Int_Onumber__class_Onumber__of(V_w,T_a),c_Int_Onumber__class_Onumber__of(V_v,T_a),T_a)
      | ~ class_Int_Onumber(T_a)
      | ~ class_Orderings_Olinorder(T_a) ),
    inference(nnf_transformation,[status(thm)],[f194]) ).

fof(f194_sk,plain,
    ! [T_a,V_w,V_v] :
      ( ~ c_lessequals(c_Int_Onumber__class_Onumber__of(V_v,T_a),c_Int_Onumber__class_Onumber__of(V_w,T_a),T_a)
      | ~ c_HOL_Oord__class_Oless(c_Int_Onumber__class_Onumber__of(V_w,T_a),c_Int_Onumber__class_Onumber__of(V_v,T_a),T_a)
      | ~ class_Int_Onumber(T_a)
      | ~ class_Orderings_Olinorder(T_a) ),
    inference(skolemisation,[status(esa)],[f194_nnf]) ).

cnf(c194,plain,
    ( ~ c_lessequals(c_Int_Onumber__class_Onumber__of(X2,X0),c_Int_Onumber__class_Onumber__of(X1,X0),X0)
    | ~ c_HOL_Oord__class_Oless(c_Int_Onumber__class_Onumber__of(X1,X0),c_Int_Onumber__class_Onumber__of(X2,X0),X0)
    | ~ class_Int_Onumber(X0)
    | ~ class_Orderings_Olinorder(X0) ),
    inference(cnf_transformation,[status(esa)],[f194_sk]) ).

cnf(f204,axiom,
    ( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
    | ~ class_Orderings_Opreorder(T_a) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_order__less__irrefl_0) ).

fof(f204_nnf,plain,
    ! [T_a,V_x] :
      ( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
      | ~ class_Orderings_Opreorder(T_a) ),
    inference(nnf_transformation,[status(thm)],[f204]) ).

fof(f204_sk,plain,
    ! [T_a,V_x] :
      ( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
      | ~ class_Orderings_Opreorder(T_a) ),
    inference(skolemisation,[status(esa)],[f204_nnf]) ).

cnf(c204,plain,
    ( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
    | ~ class_Orderings_Opreorder(X0) ),
    inference(cnf_transformation,[status(esa)],[f204_sk]) ).

cnf(f205,axiom,
    ~ c_HOL_Oord__class_Oless(V_x,V_x,tc_RealDef_Oreal),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_real__less__def_1) ).

fof(f205_nnf,plain,
    ! [V_x] : ~ c_HOL_Oord__class_Oless(V_x,V_x,tc_RealDef_Oreal),
    inference(nnf_transformation,[status(thm)],[f205]) ).

fof(f205_sk,plain,
    ! [V_x] : ~ c_HOL_Oord__class_Oless(V_x,V_x,tc_RealDef_Oreal),
    inference(skolemisation,[status(esa)],[f205_nnf]) ).

cnf(c205,plain,
    ~ c_HOL_Oord__class_Oless(X0,X0,tc_RealDef_Oreal),
    inference(cnf_transformation,[status(esa)],[f205_sk]) ).

cnf(f206,axiom,
    ( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
    | ~ class_Orderings_Oorder(T_a) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_order__less__le_1) ).

fof(f206_nnf,plain,
    ! [T_a,V_x] :
      ( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
      | ~ class_Orderings_Oorder(T_a) ),
    inference(nnf_transformation,[status(thm)],[f206]) ).

fof(f206_sk,plain,
    ! [T_a,V_x] :
      ( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
      | ~ class_Orderings_Oorder(T_a) ),
    inference(skolemisation,[status(esa)],[f206_nnf]) ).

cnf(c206,plain,
    ( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
    | ~ class_Orderings_Oorder(X0) ),
    inference(cnf_transformation,[status(esa)],[f206_sk]) ).

cnf(f207,axiom,
    ( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
    | ~ class_Orderings_Olinorder(T_a) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_linorder__neq__iff_1) ).

fof(f207_nnf,plain,
    ! [T_a,V_x] :
      ( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
      | ~ class_Orderings_Olinorder(T_a) ),
    inference(nnf_transformation,[status(thm)],[f207]) ).

fof(f207_sk,plain,
    ! [T_a,V_x] :
      ( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
      | ~ class_Orderings_Olinorder(T_a) ),
    inference(skolemisation,[status(esa)],[f207_nnf]) ).

cnf(c207,plain,
    ( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
    | ~ class_Orderings_Olinorder(X0) ),
    inference(cnf_transformation,[status(esa)],[f207_sk]) ).

cnf(f308,axiom,
    ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(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),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__real__square__gt__zero_1) ).

fof(f308_nnf,plain,
    ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(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(nnf_transformation,[status(thm)],[f308]) ).

fof(f308_sk,plain,
    ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(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(skolemisation,[status(esa)],[f308_nnf]) ).

cnf(c308,plain,
    ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(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(cnf_transformation,[status(esa)],[f308_sk]) ).

cnf(f324,axiom,
    ~ c_HOL_Oord__class_Oless(c_RealDef_Oreal(V_n,tc_nat),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__real__of__nat__less__zero_0) ).

fof(f324_nnf,plain,
    ! [V_n] : ~ c_HOL_Oord__class_Oless(c_RealDef_Oreal(V_n,tc_nat),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(nnf_transformation,[status(thm)],[f324]) ).

fof(f324_sk,plain,
    ! [V_n] : ~ c_HOL_Oord__class_Oless(c_RealDef_Oreal(V_n,tc_nat),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(skolemisation,[status(esa)],[f324_nnf]) ).

cnf(c324,plain,
    ~ c_HOL_Oord__class_Oless(c_RealDef_Oreal(X0,tc_nat),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(cnf_transformation,[status(esa)],[f324_sk]) ).

cnf(f325,axiom,
    ~ c_HOL_Oord__class_Oless(c_Transcendental_Opi,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_pi__not__less__zero_0) ).

fof(f325_nnf,plain,
    ~ c_HOL_Oord__class_Oless(c_Transcendental_Opi,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(nnf_transformation,[status(thm)],[f325]) ).

fof(f325_sk,plain,
    ~ c_HOL_Oord__class_Oless(c_Transcendental_Opi,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(skolemisation,[status(esa)],[f325_nnf]) ).

cnf(c325,plain,
    ~ c_HOL_Oord__class_Oless(c_Transcendental_Opi,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
    inference(cnf_transformation,[status(esa)],[f325_sk]) ).

cnf(f329,axiom,
    c_Transcendental_Ocos(c_Transcendental_Oarctan(V_x)) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_cos__arctan__not__zero_0) ).

fof(f329_nnf,plain,
    ! [V_x] : c_Transcendental_Ocos(c_Transcendental_Oarctan(V_x)) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
    inference(nnf_transformation,[status(thm)],[f329]) ).

fof(f329_sk,plain,
    ! [V_x] : c_Transcendental_Ocos(c_Transcendental_Oarctan(V_x)) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
    inference(skolemisation,[status(esa)],[f329_nnf]) ).

cnf(c329,plain,
    c_Transcendental_Ocos(c_Transcendental_Oarctan(X0)) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
    inference(cnf_transformation,[status(esa)],[f329_sk]) ).

cnf(f336,axiom,
    ( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_x,tc_RealDef_Oreal)
    | c_NthRoot_Osqrt(V_x) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_real__sqrt__not__eq__zero_0) ).

fof(f336_nnf,plain,
    ! [V_x] :
      ( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_x,tc_RealDef_Oreal)
      | c_NthRoot_Osqrt(V_x) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
    inference(nnf_transformation,[status(thm)],[f336]) ).

fof(f336_sk,plain,
    ! [V_x] :
      ( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_x,tc_RealDef_Oreal)
      | c_NthRoot_Osqrt(V_x) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
    inference(skolemisation,[status(esa)],[f336_nnf]) ).

cnf(c336,plain,
    ( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)
    | c_NthRoot_Osqrt(X0) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
    inference(cnf_transformation,[status(esa)],[f336_sk]) ).

cnf(f444,axiom,
    ( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
    | ~ c_lessequals(V_y,V_x,T_a)
    | ~ class_Orderings_Opreorder(T_a) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_less__le__not__le_1) ).

fof(f444_nnf,plain,
    ! [T_a,V_y,V_x] :
      ( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
      | ~ c_lessequals(V_y,V_x,T_a)
      | ~ class_Orderings_Opreorder(T_a) ),
    inference(nnf_transformation,[status(thm)],[f444]) ).

fof(f444_sk,plain,
    ! [T_a,V_y,V_x] :
      ( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
      | ~ c_lessequals(V_y,V_x,T_a)
      | ~ class_Orderings_Opreorder(T_a) ),
    inference(skolemisation,[status(esa)],[f444_nnf]) ).

cnf(c444,plain,
    ( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
    | ~ c_lessequals(X1,X2,X0)
    | ~ class_Orderings_Opreorder(X0) ),
    inference(cnf_transformation,[status(esa)],[f444_sk]) ).

cnf(f446,axiom,
    ( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
    | ~ c_lessequals(V_x,V_x,T_a)
    | ~ class_Orderings_Olinorder(T_a) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_linorder__antisym__conv2_1) ).

fof(f446_nnf,plain,
    ! [T_a,V_x] :
      ( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
      | ~ c_lessequals(V_x,V_x,T_a)
      | ~ class_Orderings_Olinorder(T_a) ),
    inference(nnf_transformation,[status(thm)],[f446]) ).

fof(f446_sk,plain,
    ! [T_a,V_x] :
      ( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
      | ~ c_lessequals(V_x,V_x,T_a)
      | ~ class_Orderings_Olinorder(T_a) ),
    inference(skolemisation,[status(esa)],[f446_nnf]) ).

cnf(c446,plain,
    ( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
    | ~ c_lessequals(X1,X1,X0)
    | ~ class_Orderings_Olinorder(X0) ),
    inference(cnf_transformation,[status(esa)],[f446_sk]) ).

cnf(f448,axiom,
    ( ~ c_lessequals(V_y,V_x,T_a)
    | ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
    | ~ class_Orderings_Olinorder(T_a) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_linorder__not__less_1) ).

fof(f448_nnf,plain,
    ! [T_a,V_x,V_y] :
      ( ~ c_lessequals(V_y,V_x,T_a)
      | ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
      | ~ class_Orderings_Olinorder(T_a) ),
    inference(nnf_transformation,[status(thm)],[f448]) ).

fof(f448_sk,plain,
    ! [T_a,V_x,V_y] :
      ( ~ c_lessequals(V_y,V_x,T_a)
      | ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
      | ~ class_Orderings_Olinorder(T_a) ),
    inference(skolemisation,[status(esa)],[f448_nnf]) ).

cnf(c448,plain,
    ( ~ c_lessequals(X2,X1,X0)
    | ~ c_HOL_Oord__class_Oless(X1,X2,X0)
    | ~ class_Orderings_Olinorder(X0) ),
    inference(cnf_transformation,[status(esa)],[f448_sk]) ).

cnf(f451,axiom,
    ( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
    | ~ c_lessequals(V_x,V_y,T_a)
    | ~ class_Orderings_Olinorder(T_a) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_linorder__not__le_1) ).

fof(f451_nnf,plain,
    ! [T_a,V_x,V_y] :
      ( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
      | ~ c_lessequals(V_x,V_y,T_a)
      | ~ class_Orderings_Olinorder(T_a) ),
    inference(nnf_transformation,[status(thm)],[f451]) ).

fof(f451_sk,plain,
    ! [T_a,V_x,V_y] :
      ( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
      | ~ c_lessequals(V_x,V_y,T_a)
      | ~ class_Orderings_Olinorder(T_a) ),
    inference(skolemisation,[status(esa)],[f451_nnf]) ).

cnf(c451,plain,
    ( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
    | ~ c_lessequals(X1,X2,X0)
    | ~ class_Orderings_Olinorder(X0) ),
    inference(cnf_transformation,[status(esa)],[f451_sk]) ).

cnf(f611,axiom,
    ( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a),T_a),T_a)
    | ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_sum__squares__gt__zero__iff_0) ).

fof(f611_nnf,plain,
    ! [T_a] :
      ( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a),T_a),T_a)
      | ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
    inference(nnf_transformation,[status(thm)],[f611]) ).

fof(f611_sk,plain,
    ! [T_a] :
      ( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a),T_a),T_a)
      | ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
    inference(skolemisation,[status(esa)],[f611_nnf]) ).

cnf(c611,plain,
    ( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(X0),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(X0),c_HOL_Ozero__class_Ozero(X0),X0),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(X0),c_HOL_Ozero__class_Ozero(X0),X0),X0),X0)
    | ~ class_Ring__and__Field_Oordered__ring__strict(X0) ),
    inference(cnf_transformation,[status(esa)],[f611_sk]) ).

cnf(f614,axiom,
    ( ~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_x,V_x,T_a),c_HOL_Otimes__class_Otimes(V_y,V_y,T_a),T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
    | ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__sum__squares__lt__zero_0) ).

fof(f614_nnf,plain,
    ! [T_a,V_x,V_y] :
      ( ~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_x,V_x,T_a),c_HOL_Otimes__class_Otimes(V_y,V_y,T_a),T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
      | ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
    inference(nnf_transformation,[status(thm)],[f614]) ).

fof(f614_sk,plain,
    ! [T_a,V_x,V_y] :
      ( ~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_x,V_x,T_a),c_HOL_Otimes__class_Otimes(V_y,V_y,T_a),T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
      | ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
    inference(skolemisation,[status(esa)],[f614_nnf]) ).

cnf(c614,plain,
    ( ~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(X1,X1,X0),c_HOL_Otimes__class_Otimes(X2,X2,X0),X0),c_HOL_Ozero__class_Ozero(X0),X0)
    | ~ class_Ring__and__Field_Oordered__ring__strict(X0) ),
    inference(cnf_transformation,[status(esa)],[f614_sk]) ).

cnf(f706,axiom,
    ( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_x,tc_RealDef_Oreal)
    | ~ c_HOL_Oord__class_Oless(V_x,c_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),tc_RealDef_Oreal)
    | c_Transcendental_Osin(V_x) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)
    | c_Transcendental_Ocos(V_x) != c_HOL_Oone__class_Oone(tc_RealDef_Oreal) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_sin__cos__between__zero__two__pi_0) ).

fof(f706_nnf,plain,
    ! [V_x] :
      ( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_x,tc_RealDef_Oreal)
      | ~ c_HOL_Oord__class_Oless(V_x,c_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),tc_RealDef_Oreal)
      | c_Transcendental_Osin(V_x) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)
      | c_Transcendental_Ocos(V_x) != c_HOL_Oone__class_Oone(tc_RealDef_Oreal) ),
    inference(nnf_transformation,[status(thm)],[f706]) ).

fof(f706_sk,plain,
    ! [V_x] :
      ( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_x,tc_RealDef_Oreal)
      | ~ c_HOL_Oord__class_Oless(V_x,c_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),tc_RealDef_Oreal)
      | c_Transcendental_Osin(V_x) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)
      | c_Transcendental_Ocos(V_x) != c_HOL_Oone__class_Oone(tc_RealDef_Oreal) ),
    inference(skolemisation,[status(esa)],[f706_nnf]) ).

cnf(c706,plain,
    ( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)
    | ~ c_HOL_Oord__class_Oless(X0,c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),tc_RealDef_Oreal)
    | c_Transcendental_Osin(X0) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)
    | c_Transcendental_Ocos(X0) != c_HOL_Oone__class_Oone(tc_RealDef_Oreal) ),
    inference(cnf_transformation,[status(esa)],[f706_sk]) ).

cnf(f716,axiom,
    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_pi__half__neq__zero_0) ).

fof(f716_nnf,plain,
    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),
    inference(nnf_transformation,[status(thm)],[f716]) ).

fof(f716_sk,plain,
    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),
    inference(skolemisation,[status(esa)],[f716_nnf]) ).

cnf(c716,plain,
    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),
    inference(cnf_transformation,[status(esa)],[f716_sk]) ).

cnf(f740,axiom,
    c_Transcendental_Opi != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_pi__neq__zero_0) ).

fof(f740_nnf,plain,
    c_Transcendental_Opi != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
    inference(nnf_transformation,[status(thm)],[f740]) ).

fof(f740_sk,plain,
    c_Transcendental_Opi != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
    inference(skolemisation,[status(esa)],[f740_nnf]) ).

cnf(c740,plain,
    c_Transcendental_Opi != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
    inference(cnf_transformation,[status(esa)],[f740_sk]) ).

cnf(f768,axiom,
    ( c_HOL_Oone__class_Oone(T_a) != c_HOL_Ozero__class_Ozero(T_a)
    | ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_one__neq__zero_0) ).

fof(f768_nnf,plain,
    ! [T_a] :
      ( c_HOL_Oone__class_Oone(T_a) != c_HOL_Ozero__class_Ozero(T_a)
      | ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
    inference(nnf_transformation,[status(thm)],[f768]) ).

fof(f768_sk,plain,
    ! [T_a] :
      ( c_HOL_Oone__class_Oone(T_a) != c_HOL_Ozero__class_Ozero(T_a)
      | ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
    inference(skolemisation,[status(esa)],[f768_nnf]) ).

cnf(c768,plain,
    ( c_HOL_Oone__class_Oone(X0) != c_HOL_Ozero__class_Ozero(X0)
    | ~ class_Ring__and__Field_Ozero__neq__one(X0) ),
    inference(cnf_transformation,[status(esa)],[f768_sk]) ).

cnf(f769,axiom,
    ( c_HOL_Ozero__class_Ozero(T_a) != c_HOL_Oone__class_Oone(T_a)
    | ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_zero__neq__one_0) ).

fof(f769_nnf,plain,
    ! [T_a] :
      ( c_HOL_Ozero__class_Ozero(T_a) != c_HOL_Oone__class_Oone(T_a)
      | ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
    inference(nnf_transformation,[status(thm)],[f769]) ).

fof(f769_sk,plain,
    ! [T_a] :
      ( c_HOL_Ozero__class_Ozero(T_a) != c_HOL_Oone__class_Oone(T_a)
      | ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
    inference(skolemisation,[status(esa)],[f769_nnf]) ).

cnf(c769,plain,
    ( c_HOL_Ozero__class_Ozero(X0) != c_HOL_Oone__class_Oone(X0)
    | ~ class_Ring__and__Field_Ozero__neq__one(X0) ),
    inference(cnf_transformation,[status(esa)],[f769_sk]) ).

cnf(f776,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(f776_nnf,plain,
    c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) != c_HOL_Oone__class_Oone(tc_RealDef_Oreal),
    inference(nnf_transformation,[status(thm)],[f776]) ).

fof(f776_sk,plain,
    c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) != c_HOL_Oone__class_Oone(tc_RealDef_Oreal),
    inference(skolemisation,[status(esa)],[f776_nnf]) ).

cnf(c776,plain,
    c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) != c_HOL_Oone__class_Oone(tc_RealDef_Oreal),
    inference(cnf_transformation,[status(esa)],[f776_sk]) ).

cnf(f815,axiom,
    c_Int_OPls != c_Int_OBit1(V_l),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_rel__simps_I39_J_0) ).

fof(f815_nnf,plain,
    ! [V_l] : c_Int_OPls != c_Int_OBit1(V_l),
    inference(nnf_transformation,[status(thm)],[f815]) ).

fof(f815_sk,plain,
    ! [V_l] : c_Int_OPls != c_Int_OBit1(V_l),
    inference(skolemisation,[status(esa)],[f815_nnf]) ).

cnf(c815,plain,
    c_Int_OPls != c_Int_OBit1(X0),
    inference(cnf_transformation,[status(esa)],[f815_sk]) ).

cnf(f817,axiom,
    c_Int_OBit1(V_k) != c_Int_OPls,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_rel__simps_I46_J_0) ).

fof(f817_nnf,plain,
    ! [V_k] : c_Int_OBit1(V_k) != c_Int_OPls,
    inference(nnf_transformation,[status(thm)],[f817]) ).

fof(f817_sk,plain,
    ! [V_k] : c_Int_OBit1(V_k) != c_Int_OPls,
    inference(skolemisation,[status(esa)],[f817_nnf]) ).

cnf(c817,plain,
    c_Int_OBit1(X0) != c_Int_OPls,
    inference(cnf_transformation,[status(esa)],[f817_sk]) ).

cnf(f824,axiom,
    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_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_pi__half__neq__two_0) ).

fof(f824_nnf,plain,
    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_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),
    inference(nnf_transformation,[status(thm)],[f824]) ).

fof(f824_sk,plain,
    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_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),
    inference(skolemisation,[status(esa)],[f824_nnf]) ).

cnf(c824,plain,
    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_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),
    inference(cnf_transformation,[status(esa)],[f824_sk]) ).

cnf(f827,axiom,
    c_Int_OBit1(V_k) != c_Int_OBit0(V_l),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_rel__simps_I50_J_0) ).

fof(f827_nnf,plain,
    ! [V_k,V_l] : c_Int_OBit1(V_k) != c_Int_OBit0(V_l),
    inference(nnf_transformation,[status(thm)],[f827]) ).

fof(f827_sk,plain,
    ! [V_k,V_l] : c_Int_OBit1(V_k) != c_Int_OBit0(V_l),
    inference(skolemisation,[status(esa)],[f827_nnf]) ).

cnf(c827,plain,
    c_Int_OBit1(X0) != c_Int_OBit0(X1),
    inference(cnf_transformation,[status(esa)],[f827_sk]) ).

cnf(f876,axiom,
    c_Int_OBit0(V_k) != c_Int_OBit1(V_l),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_rel__simps_I49_J_0) ).

fof(f876_nnf,plain,
    ! [V_k,V_l] : c_Int_OBit0(V_k) != c_Int_OBit1(V_l),
    inference(nnf_transformation,[status(thm)],[f876]) ).

fof(f876_sk,plain,
    ! [V_k,V_l] : c_Int_OBit0(V_k) != c_Int_OBit1(V_l),
    inference(skolemisation,[status(esa)],[f876_nnf]) ).

cnf(c876,plain,
    c_Int_OBit0(X0) != c_Int_OBit1(X1),
    inference(cnf_transformation,[status(esa)],[f876_sk]) ).

cnf(goal_0,negated_conjecture,
    true != false,
    inference(equality_encoding,[status(esa)],[c60,c61,c64,c65,c98,c111,c113,c194,c204,c205,c206,c207,c308,c324,c325,c329,c336,c444,c446,c448,c451,c611,c614,c706,c716,c717,c740,c768,c769,c776,c815,c817,c824,c827,c876]) ).

cnf(g0_0,plain,
    true != true,
    inference(rw,[status(thm)],[goal_0,t15489]) ).

cnf(contradiction_0,plain,
    $false,
    inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : SWV601-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04  % Command  : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/10.59  % Computer : n009.cluster.edu
% 0.09/10.59  % Model    : x86_64 x86_64
% 0.09/10.59  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/10.59  % Memory   : 8046.5625MB
% 0.09/10.59  % OS       : Linux 6.8.0-71-generic
% 0.09/10.59  % CPULimit : 300
% 0.09/10.59  % WCLimit  : 300
% 0.09/10.59  % DateTime : Thu Sep 24 20:41:25 UTC 2026
% 0.09/10.59  % CPUTime  : 
% 0.09/10.59  Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 69.61/19.45  % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 69.61/19.45  % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------