%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV608-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:19:05 PM UTC 2026
% Result : Unsatisfiable 28.22s 7.21s
% Output : Refutation 0.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 37
% Number of leaves : 98
% Syntax : Number of formulae : 555 ( 202 unt; 42 def)
% Number of atoms : 1080 ( 405 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 903 ( 378 ~; 498 |; 0 &)
% ( 27 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 40 ( 38 usr; 28 prp; 0-3 aty)
% Number of functors : 34 ( 34 usr; 23 con; 0-3 aty)
% Number of variables : 448 ( 0 sgn 448 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f117,axiom,
! [X0,X1] :
( ~ class_Ring__and__Field_Ocomm__semiring__1(X0)
| c_HOL_Otimes__class_Otimes(c_HOL_Oone__class_Oone(X0),X1,X0) = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_class__semiring_Osemiring__rules_I11_J_0) ).
fof(f150,axiom,
c_Transcendental_Opi != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_pi__neq__zero_0) ).
fof(f151,plain,
c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) != c_Transcendental_Opi,
inference(reorient_equations,[],[f150]) ).
fof(f216,axiom,
! [X0] : ~ c_HOL_Oord__class_Oless(c_RealDef_Oreal(X0,tc_nat),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__real__of__nat__less__zero_0) ).
fof(f231,axiom,
! [X0,X1] :
( ~ c_lessequals(X1,X0,tc_RealDef_Oreal)
| X0 = X1
| ~ c_lessequals(X0,X1,tc_RealDef_Oreal) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_real__le__antisym_0) ).
fof(f273,axiom,
! [X0] : ~ c_HOL_Oord__class_Oless(X0,X0,tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_real__less__def_1) ).
fof(f299,axiom,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_pi__gt__zero_0) ).
fof(f356,axiom,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),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/sandbox2/benchmark/theBenchmark.p',cls_pi__half__gt__zero_0) ).
fof(f422,axiom,
! [X0] :
( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealDef_Oreal(X0,tc_nat),tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_real__of__nat__gt__zero__cancel__iff_1) ).
fof(f434,axiom,
! [X2,X3,X0,X1] :
( c_HOL_Oord__class_Oless(X1,c_HOL_Oplus__class_Oplus(X2,X3,X0),X0)
| ~ class_Ring__and__Field_Oordered__semidom(X0)
| ~ c_HOL_Oord__class_Oless(X1,X3,X0)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(X0),X2,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_pos__add__strict_0) ).
fof(f501,axiom,
! [X0,X1] :
( ~ class_Ring__and__Field_Ofield(X0)
| X1 = c_HOL_Ozero__class_Ozero(X0)
| c_HOL_Oinverse__class_Odivide(X1,X1,X0) = c_HOL_Oone__class_Oone(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_right__inverse__eq_1) ).
fof(f502,plain,
! [X0,X1] :
( ~ class_Ring__and__Field_Ofield(X0)
| c_HOL_Ozero__class_Ozero(X0) = X1
| c_HOL_Oone__class_Oone(X0) = c_HOL_Oinverse__class_Odivide(X1,X1,X0) ),
inference(reorient_equations,[],[f501]) ).
fof(f528,axiom,
! [X0,X1] :
( ~ class_Ring__and__Field_Ocomm__semiring__1(X0)
| c_Power_Opower__class_Opower(X1,c_HOL_Ozero__class_Ozero(tc_nat),X0) = c_HOL_Oone__class_Oone(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_class__semiring_Opwr__0_0) ).
fof(f529,plain,
! [X0,X1] :
( ~ class_Ring__and__Field_Ocomm__semiring__1(X0)
| c_HOL_Oone__class_Oone(X0) = c_Power_Opower__class_Opower(X1,c_HOL_Ozero__class_Ozero(tc_nat),X0) ),
inference(reorient_equations,[],[f528]) ).
fof(f531,axiom,
! [X0] :
( c_RealDef_Oreal(X0,tc_nat) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)
| X0 = c_HOL_Ozero__class_Ozero(tc_nat) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_real__of__nat__zero__iff_0) ).
fof(f532,plain,
! [X0] :
( c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) != c_RealDef_Oreal(X0,tc_nat)
| c_HOL_Ozero__class_Ozero(tc_nat) = X0 ),
inference(reorient_equations,[],[f531]) ).
fof(f533,axiom,
c_RealDef_Oreal(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_real__of__nat__zero_0) ).
fof(f534,plain,
c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_RealDef_Oreal(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(reorient_equations,[],[f533]) ).
fof(f557,axiom,
! [X0,X1] :
( ~ class_Ring__and__Field_Ocomm__semiring__1(X0)
| c_HOL_Otimes__class_Otimes(X1,X1,X0) = c_Power_Opower__class_Opower(X1,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_class__semiring_Osemiring__rules_I29_J_0) ).
fof(f564,axiom,
! [X0] : 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,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_real__sum__of__halves_0) ).
fof(f566,axiom,
c_lessequals(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_pi__ge__two_0) ).
fof(f576,axiom,
c_lessequals(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),tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_pi__half__le__two_0) ).
fof(f583,axiom,
! [X0,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_HOL_Oinverse__class_Odivide(X0,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),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Oinverse__class_Odivide(X0,X1,tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_eq__divide__2__times__iff_0) ).
fof(f584,plain,
! [X0,X1] : c_HOL_Oinverse__class_Odivide(X0,X1,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(X0,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),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(reorient_equations,[],[f583]) ).
fof(f585,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/sandbox2/benchmark/theBenchmark.p',cls_pi__half__neq__two_0) ).
fof(f586,plain,
c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal) != c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(reorient_equations,[],[f585]) ).
fof(f598,axiom,
! [X2,X0,X1] :
( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(X0),c_HOL_Oinverse__class_Odivide(X1,X2,X0),X0)
| ~ class_Ring__and__Field_Oordered__field(X0)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(X0),X2,X0)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(X0),X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_divide__pos__pos_0) ).
fof(f623,axiom,
! [X2,X0,X1] : c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(X0,X1,tc_nat),X2,tc_nat) = c_HOL_Otimes__class_Otimes(X0,c_HOL_Otimes__class_Otimes(X1,X2,tc_nat),tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_nat__mult__assoc_0) ).
fof(f624,axiom,
! [X2,X0,X1] : c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(X0,X1,tc_RealDef_Oreal),X2,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(X0,c_HOL_Otimes__class_Otimes(X1,X2,tc_RealDef_Oreal),tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_real__mult__assoc_0) ).
fof(f641,axiom,
! [X2,X3,X0,X1] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(X1,X3,X0),X2,X0)
| c_HOL_Oord__class_Oless(X1,c_HOL_Oinverse__class_Odivide(X2,X3,X0),X0)
| ~ class_Ring__and__Field_Oordered__field(X0)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(X0),X3,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_mult__imp__less__div__pos_0) ).
fof(f670,axiom,
! [X0] : ~ c_HOL_Oord__class_Oless(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__less0_0) ).
fof(f679,axiom,
! [X0,X1] : c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(X0,X1,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X0,X0,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Oinverse__class_Odivide(X1,X0,tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_real__divide__square__eq_0) ).
fof(f680,plain,
! [X0,X1] : c_HOL_Oinverse__class_Odivide(X1,X0,tc_RealDef_Oreal) = c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(X0,X1,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X0,X0,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(reorient_equations,[],[f679]) ).
fof(f729,axiom,
! [X0,X1] :
( ~ class_Ring__and__Field_Ocomm__semiring__1(X0)
| c_HOL_Otimes__class_Otimes(X1,c_HOL_Ozero__class_Ozero(X0),X0) = c_HOL_Ozero__class_Ozero(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_class__semiring_Osemiring__rules_I10_J_0) ).
fof(f730,plain,
! [X0,X1] :
( ~ class_Ring__and__Field_Ocomm__semiring__1(X0)
| c_HOL_Ozero__class_Ozero(X0) = c_HOL_Otimes__class_Otimes(X1,c_HOL_Ozero__class_Ozero(X0),X0) ),
inference(reorient_equations,[],[f729]) ).
fof(f735,axiom,
! [X0] : c_HOL_Otimes__class_Otimes(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) = c_HOL_Ozero__class_Ozero(tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_mult__is__0_2) ).
fof(f736,plain,
! [X0] : c_HOL_Ozero__class_Ozero(tc_nat) = c_HOL_Otimes__class_Otimes(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(reorient_equations,[],[f735]) ).
fof(f743,axiom,
! [X0,X1] :
( ~ class_Ring__and__Field_Ocomm__semiring__1(X0)
| c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(X0),X1,X0) = c_HOL_Ozero__class_Ozero(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_class__semiring_Omul__0_0) ).
fof(f744,plain,
! [X0,X1] :
( ~ class_Ring__and__Field_Ocomm__semiring__1(X0)
| c_HOL_Ozero__class_Ozero(X0) = c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(X0),X1,X0) ),
inference(reorient_equations,[],[f743]) ).
fof(f758,axiom,
! [X0,X1] : c_RealDef_Oreal(c_HOL_Otimes__class_Otimes(X0,X1,tc_nat),tc_nat) = c_HOL_Otimes__class_Otimes(c_RealDef_Oreal(X0,tc_nat),c_RealDef_Oreal(X1,tc_nat),tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_real__of__nat__mult_0) ).
fof(f769,axiom,
! [X0] :
( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat)
| X0 = c_HOL_Ozero__class_Ozero(tc_nat) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_gr0I_0) ).
fof(f770,plain,
! [X0] :
( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat)
| c_HOL_Ozero__class_Ozero(tc_nat) = X0 ),
inference(reorient_equations,[],[f769]) ).
fof(f783,axiom,
! [X0,X1] : c_Power_Opower__class_Opower(c_Complex_Ocis(X0),X1,tc_Complex_Ocomplex) = c_Complex_Ocis(c_HOL_Otimes__class_Otimes(c_RealDef_Oreal(X1,tc_nat),X0,tc_RealDef_Oreal)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_DeMoivre_0) ).
fof(f806,axiom,
! [X2,X3,X0,X1,X4] :
( ~ class_Ring__and__Field_Ofield(X0)
| ~ class_Ring__and__Field_Odivision__by__zero(X0)
| c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X1,X2,X0),c_HOL_Oinverse__class_Odivide(X3,X4,X0),X0) = c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(X1,X3,X0),c_HOL_Otimes__class_Otimes(X2,X4,X0),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_mult__frac__frac_0) ).
fof(f807,axiom,
! [X2,X0,X1] :
( ~ class_Ring__and__Field_Oordered__idom(X0)
| c_HOL_Oord__class_Oless(X1,X2,X0)
| c_HOL_Oord__class_Oless(X2,X1,X0)
| X2 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_linorder__neqE__ordered__idom_0) ).
fof(f808,plain,
! [X2,X0,X1] :
( c_HOL_Oord__class_Oless(X2,X1,X0)
| c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Ring__and__Field_Oordered__idom(X0)
| X1 = X2 ),
inference(reorient_equations,[],[f807]) ).
fof(f817,axiom,
! [X2,X0,X1] :
( ~ class_Orderings_Olinorder(X0)
| c_HOL_Oord__class_Oless(X1,X2,X0)
| c_HOL_Oord__class_Oless(X2,X1,X0)
| X2 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_linorder__neqE_0) ).
fof(f818,plain,
! [X2,X0,X1] :
( c_HOL_Oord__class_Oless(X2,X1,X0)
| c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0)
| X1 = X2 ),
inference(reorient_equations,[],[f817]) ).
fof(f819,axiom,
! [X2,X3,X0,X1] :
( ~ class_Ring__and__Field_Ofield(X0)
| ~ class_Ring__and__Field_Odivision__by__zero(X0)
| c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Odivide(X1,X2,X0),X3,X0) = c_HOL_Oinverse__class_Odivide(c_Power_Opower__class_Opower(X1,X3,X0),c_Power_Opower__class_Opower(X2,X3,X0),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_power__divide_0) ).
fof(f826,axiom,
! [X2,X0,X1] :
( ~ class_Ring__and__Field_Ofield(X0)
| ~ class_Ring__and__Field_Odivision__by__zero(X0)
| c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(X1,X2,X0),X2,X0) = X1
| X2 = c_HOL_Ozero__class_Ozero(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_divide__eq__eq_3) ).
fof(f827,plain,
! [X2,X0,X1] :
( ~ class_Ring__and__Field_Ofield(X0)
| ~ class_Ring__and__Field_Odivision__by__zero(X0)
| c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(X1,X2,X0),X2,X0) = X1
| c_HOL_Ozero__class_Ozero(X0) = X2 ),
inference(reorient_equations,[],[f826]) ).
fof(f838,axiom,
! [X2,X0,X1] :
( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(X0),c_HOL_Otimes__class_Otimes(X1,X2,X0),X0)
| ~ class_Ring__and__Field_Oordered__semiring__strict(X0)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(X0),X2,X0)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(X0),X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_mult__pos__pos_0) ).
fof(f847,axiom,
! [X0,X1] :
( c_HOL_Otimes__class_Otimes(X0,X1,tc_nat) != c_HOL_Ozero__class_Ozero(tc_nat)
| X1 = c_HOL_Ozero__class_Ozero(tc_nat)
| X0 = c_HOL_Ozero__class_Ozero(tc_nat) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_mult__is__0_0) ).
fof(f848,plain,
! [X0,X1] :
( c_HOL_Ozero__class_Ozero(tc_nat) != c_HOL_Otimes__class_Otimes(X0,X1,tc_nat)
| c_HOL_Ozero__class_Ozero(tc_nat) = X1
| c_HOL_Ozero__class_Ozero(tc_nat) = X0 ),
inference(reorient_equations,[],[f847]) ).
fof(f870,axiom,
! [X2,X3,X0,X1] :
( ~ class_Ring__and__Field_Ocomm__semiring__1(X0)
| c_Power_Opower__class_Opower(c_Power_Opower__class_Opower(X1,X2,X0),X3,X0) = c_Power_Opower__class_Opower(X1,c_HOL_Otimes__class_Otimes(X2,X3,tc_nat),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_class__semiring_Opwr__pwr_0) ).
fof(f871,plain,
! [X2,X3,X0,X1] :
( ~ class_Ring__and__Field_Ocomm__semiring__1(X0)
| c_Power_Opower__class_Opower(X1,c_HOL_Otimes__class_Otimes(X2,X3,tc_nat),X0) = c_Power_Opower__class_Opower(c_Power_Opower__class_Opower(X1,X2,X0),X3,X0) ),
inference(reorient_equations,[],[f870]) ).
fof(f873,axiom,
! [X0,X1] : c_HOL_Otimes__class_Otimes(X0,X1,tc_nat) = c_HOL_Otimes__class_Otimes(X1,X0,tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_nat__mult__commute_0) ).
fof(f874,axiom,
! [X0,X1] : c_HOL_Otimes__class_Otimes(X0,X1,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(X1,X0,tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_real__mult__commute_0) ).
fof(f879,axiom,
! [X2,X3,X0,X1] :
( ~ c_HOL_Oord__class_Oless(X3,X2,X0)
| c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Opreorder(X0)
| ~ c_HOL_Oord__class_Oless(X1,X3,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_order__less__trans_0) ).
fof(f889,axiom,
! [X0,X1] :
( ~ class_Ring__and__Field_Ofield(X0)
| c_HOL_Oinverse__class_Odivide(c_HOL_Ozero__class_Ozero(X0),X1,X0) = c_HOL_Ozero__class_Ozero(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_divide__zero__left_0) ).
fof(f890,plain,
! [X0,X1] :
( ~ class_Ring__and__Field_Ofield(X0)
| c_HOL_Ozero__class_Ozero(X0) = c_HOL_Oinverse__class_Odivide(c_HOL_Ozero__class_Ozero(X0),X1,X0) ),
inference(reorient_equations,[],[f889]) ).
fof(f911,axiom,
! [X2,X3,X0,X1] :
( ~ class_Ring__and__Field_Ofield(X0)
| ~ class_Ring__and__Field_Odivision__by__zero(X0)
| c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X1,X2,X0),X3,X0) = c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(X1,X3,X0),X2,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_mult__frac__num_0) ).
fof(f931,negated_conjecture,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),v_d,tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f932,negated_conjecture,
c_Power_Opower__class_Opower(c_Complex_Ocis(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(c_HOL_Otimes__class_Otimes(v_d,v_n,tc_nat),tc_nat),tc_RealDef_Oreal)),c_HOL_Otimes__class_Otimes(v_d,v_k,tc_nat),tc_Complex_Ocomplex) != c_Power_Opower__class_Opower(c_Complex_Ocis(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)),v_k,tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_1) ).
fof(f1017,axiom,
class_Ring__and__Field_Oordered__semiring__strict(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_RealDef__Oreal__Ring__and__Field_Oordered__semiring__strict) ).
fof(f1029,axiom,
class_Ring__and__Field_Odivision__by__zero(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_RealDef__Oreal__Ring__and__Field_Odivision__by__zero) ).
fof(f1030,axiom,
class_Ring__and__Field_Oordered__semidom(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_RealDef__Oreal__Ring__and__Field_Oordered__semidom) ).
fof(f1031,axiom,
class_Ring__and__Field_Ocomm__semiring__1(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_RealDef__Oreal__Ring__and__Field_Ocomm__semiring__1) ).
fof(f1037,axiom,
class_Ring__and__Field_Oordered__field(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_RealDef__Oreal__Ring__and__Field_Oordered__field) ).
fof(f1042,axiom,
class_Ring__and__Field_Oordered__idom(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_RealDef__Oreal__Ring__and__Field_Oordered__idom) ).
fof(f1054,axiom,
class_Ring__and__Field_Ofield(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_RealDef__Oreal__Ring__and__Field_Ofield) ).
fof(f1057,axiom,
class_Orderings_Opreorder(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_RealDef__Oreal__Orderings_Opreorder) ).
fof(f1058,axiom,
class_Orderings_Olinorder(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_RealDef__Oreal__Orderings_Olinorder) ).
fof(f1070,axiom,
class_Ring__and__Field_Ocomm__semiring__1(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_Complex__Ocomplex__Ring__and__Field_Ocomm__semiring__1) ).
fof(f1095,definition,
sF0 = c_HOL_Ozero__class_Ozero(tc_nat),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f1096,plain,
c_HOL_Ozero__class_Ozero(tc_nat) = sF0,
inference(reorient_equations,[],[f1095]) ).
fof(f1097,plain,
c_HOL_Oord__class_Oless(sF0,v_d,tc_nat),
inference(definition_folding,[],[f931,f1096]) ).
fof(f1098,definition,
sF1 = c_Int_OBit1(c_Int_OPls),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f1099,plain,
c_Int_OBit1(c_Int_OPls) = sF1,
inference(reorient_equations,[],[f1098]) ).
fof(f1100,definition,
sF2 = c_Int_OBit0(sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f1101,plain,
c_Int_OBit0(sF1) = sF2,
inference(reorient_equations,[],[f1100]) ).
fof(f1102,definition,
sF3 = c_Int_Onumber__class_Onumber__of(sF2,tc_RealDef_Oreal),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f1103,plain,
c_Int_Onumber__class_Onumber__of(sF2,tc_RealDef_Oreal) = sF3,
inference(reorient_equations,[],[f1102]) ).
fof(f1104,definition,
sF4 = c_HOL_Otimes__class_Otimes(sF3,c_Transcendental_Opi,tc_RealDef_Oreal),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f1105,plain,
c_HOL_Otimes__class_Otimes(sF3,c_Transcendental_Opi,tc_RealDef_Oreal) = sF4,
inference(reorient_equations,[],[f1104]) ).
fof(f1106,definition,
sF5 = c_HOL_Otimes__class_Otimes(v_d,v_n,tc_nat),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f1107,plain,
c_HOL_Otimes__class_Otimes(v_d,v_n,tc_nat) = sF5,
inference(reorient_equations,[],[f1106]) ).
fof(f1108,definition,
sF6 = c_RealDef_Oreal(sF5,tc_nat),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f1109,plain,
c_RealDef_Oreal(sF5,tc_nat) = sF6,
inference(reorient_equations,[],[f1108]) ).
fof(f1110,definition,
sF7 = c_HOL_Oinverse__class_Odivide(sF4,sF6,tc_RealDef_Oreal),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f1111,plain,
c_HOL_Oinverse__class_Odivide(sF4,sF6,tc_RealDef_Oreal) = sF7,
inference(reorient_equations,[],[f1110]) ).
fof(f1112,definition,
sF8 = c_Complex_Ocis(sF7),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f1113,plain,
c_Complex_Ocis(sF7) = sF8,
inference(reorient_equations,[],[f1112]) ).
fof(f1114,definition,
sF9 = c_HOL_Otimes__class_Otimes(v_d,v_k,tc_nat),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f1115,plain,
c_HOL_Otimes__class_Otimes(v_d,v_k,tc_nat) = sF9,
inference(reorient_equations,[],[f1114]) ).
fof(f1116,definition,
sF10 = c_Power_Opower__class_Opower(sF8,sF9,tc_Complex_Ocomplex),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f1117,plain,
c_Power_Opower__class_Opower(sF8,sF9,tc_Complex_Ocomplex) = sF10,
inference(reorient_equations,[],[f1116]) ).
fof(f1118,definition,
sF11 = c_RealDef_Oreal(v_n,tc_nat),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f1119,plain,
c_RealDef_Oreal(v_n,tc_nat) = sF11,
inference(reorient_equations,[],[f1118]) ).
fof(f1120,definition,
sF12 = c_HOL_Oinverse__class_Odivide(sF4,sF11,tc_RealDef_Oreal),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f1121,plain,
c_HOL_Oinverse__class_Odivide(sF4,sF11,tc_RealDef_Oreal) = sF12,
inference(reorient_equations,[],[f1120]) ).
fof(f1122,definition,
sF13 = c_Complex_Ocis(sF12),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
fof(f1123,plain,
c_Complex_Ocis(sF12) = sF13,
inference(reorient_equations,[],[f1122]) ).
fof(f1124,definition,
sF14 = c_Power_Opower__class_Opower(sF13,v_k,tc_Complex_Ocomplex),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
fof(f1125,plain,
c_Power_Opower__class_Opower(sF13,v_k,tc_Complex_Ocomplex) = sF14,
inference(reorient_equations,[],[f1124]) ).
fof(f1126,plain,
sF10 != sF14,
inference(definition_folding,[],[f932,f1125,f1123,f1121,f1119,f1105,f1103,f1101,f1099,f1117,f1115,f1113,f1111,f1109,f1107,f1105,f1103,f1101,f1099]) ).
fof(f1132,plain,
! [X0] : c_Power_Opower__class_Opower(c_Complex_Ocis(X0),sF5,tc_Complex_Ocomplex) = c_Complex_Ocis(c_HOL_Otimes__class_Otimes(sF6,X0,tc_RealDef_Oreal)),
inference(superposition,[],[f783,f1109]) ).
fof(f1134,plain,
! [X0,X1] : c_Power_Opower__class_Opower(c_Complex_Ocis(X0),X1,tc_Complex_Ocomplex) = c_Complex_Ocis(c_HOL_Otimes__class_Otimes(X0,c_RealDef_Oreal(X1,tc_nat),tc_RealDef_Oreal)),
inference(superposition,[],[f783,f874]) ).
fof(f1135,plain,
c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_RealDef_Oreal(sF0,tc_nat),
inference(superposition,[],[f534,f1096]) ).
fof(f1142,plain,
! [X0] : c_HOL_Otimes__class_Otimes(v_d,c_HOL_Otimes__class_Otimes(v_k,X0,tc_nat),tc_nat) = c_HOL_Otimes__class_Otimes(sF9,X0,tc_nat),
inference(superposition,[],[f623,f1115]) ).
fof(f1143,plain,
! [X0] : c_HOL_Otimes__class_Otimes(v_d,c_HOL_Otimes__class_Otimes(v_n,X0,tc_nat),tc_nat) = c_HOL_Otimes__class_Otimes(sF5,X0,tc_nat),
inference(superposition,[],[f623,f1107]) ).
fof(f1153,plain,
! [X2,X0,X1] : c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(X0,X1,tc_RealDef_Oreal),X2,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(X1,c_HOL_Otimes__class_Otimes(X0,X2,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(superposition,[],[f624,f874]) ).
fof(f1159,plain,
! [X2,X0,X1] : c_HOL_Otimes__class_Otimes(X0,c_HOL_Otimes__class_Otimes(X1,X2,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(X2,c_HOL_Otimes__class_Otimes(X0,X1,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(superposition,[],[f874,f624]) ).
fof(f1161,plain,
! [X2,X0,X1] : c_HOL_Otimes__class_Otimes(X0,c_HOL_Otimes__class_Otimes(X1,X2,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(X1,c_HOL_Otimes__class_Otimes(X0,X2,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f1153,f624]) ).
fof(f1180,plain,
! [X0] :
( c_HOL_Oord__class_Oless(sF0,X0,tc_nat)
| sF0 = X0 ),
inference(superposition,[],[f770,f1096]) ).
fof(f1189,plain,
! [X0] : ~ c_HOL_Oord__class_Oless(X0,sF0,tc_nat),
inference(superposition,[],[f670,f1096]) ).
fof(f1199,plain,
! [X0] : sF0 = c_HOL_Otimes__class_Otimes(X0,sF0,tc_nat),
inference(superposition,[],[f736,f1096]) ).
fof(f1223,plain,
! [X0] : c_RealDef_Oreal(c_HOL_Otimes__class_Otimes(X0,v_n,tc_nat),tc_nat) = c_HOL_Otimes__class_Otimes(c_RealDef_Oreal(X0,tc_nat),sF11,tc_RealDef_Oreal),
inference(superposition,[],[f758,f1119]) ).
fof(f1228,plain,
! [X0,X1] : c_Power_Opower__class_Opower(c_Complex_Ocis(c_RealDef_Oreal(X1,tc_nat)),X0,tc_Complex_Ocomplex) = c_Complex_Ocis(c_RealDef_Oreal(c_HOL_Otimes__class_Otimes(X0,X1,tc_nat),tc_nat)),
inference(superposition,[],[f783,f758]) ).
fof(f1273,plain,
! [X0,X1] : c_HOL_Oinverse__class_Odivide(X0,X1,tc_RealDef_Oreal) = c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(X0,X1,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X1,X1,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(superposition,[],[f680,f874]) ).
fof(f1284,plain,
! [X0] : c_HOL_Otimes__class_Otimes(sF5,X0,tc_nat) = c_HOL_Otimes__class_Otimes(v_d,c_HOL_Otimes__class_Otimes(X0,v_n,tc_nat),tc_nat),
inference(superposition,[],[f1143,f873]) ).
fof(f1290,plain,
! [X0,X1] : c_HOL_Oinverse__class_Odivide(X0,X1,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF1),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(X0,c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF1),tc_RealDef_Oreal),X1,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(superposition,[],[f584,f1099]) ).
fof(f1293,plain,
! [X0,X1] : c_HOL_Oinverse__class_Odivide(X1,X0,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(X1,c_HOL_Otimes__class_Otimes(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(superposition,[],[f584,f874]) ).
fof(f1294,plain,
! [X0] : 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),X0,tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(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),
inference(superposition,[],[f584,f680]) ).
fof(f1295,plain,
! [X0,X1] : c_HOL_Oinverse__class_Odivide(c_HOL_Oinverse__class_Odivide(X0,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),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Oinverse__class_Odivide(c_HOL_Oinverse__class_Odivide(X0,X1,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(superposition,[],[f680,f584]) ).
fof(f1296,plain,
! [X2,X0,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_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X0,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),tc_RealDef_Oreal),X2,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X0,X1,tc_RealDef_Oreal),X2,tc_RealDef_Oreal),
inference(superposition,[],[f624,f584]) ).
fof(f1297,plain,
! [X2,X0,X1] : c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X0,X1,tc_RealDef_Oreal),X2,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF1),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X0,c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF1),tc_RealDef_Oreal),X1,tc_RealDef_Oreal),tc_RealDef_Oreal),X2,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f1296,f1099]) ).
fof(f1298,plain,
! [X0,X1] : c_HOL_Oinverse__class_Odivide(c_HOL_Oinverse__class_Odivide(X0,c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF1),tc_RealDef_Oreal),X1,tc_RealDef_Oreal),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF1),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Oinverse__class_Odivide(c_HOL_Oinverse__class_Odivide(X0,X1,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF1),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF1),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f1295,f1099]) ).
fof(f1299,plain,
! [X0] : c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF1),tc_RealDef_Oreal),X0,tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF1),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF1),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF1),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f1294,f1099]) ).
fof(f1300,plain,
! [X0,X1] : c_HOL_Oinverse__class_Odivide(X1,X0,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF1),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(X1,c_HOL_Otimes__class_Otimes(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF1),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f1293,f1099]) ).
fof(f1303,plain,
! [X0,X1] : c_HOL_Oinverse__class_Odivide(X0,X1,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(sF2,tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(X0,c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(sF2,tc_RealDef_Oreal),X1,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f1290,f1101]) ).
fof(f1304,plain,
! [X2,X0,X1] : c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X0,X1,tc_RealDef_Oreal),X2,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(sF2,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X0,c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(sF2,tc_RealDef_Oreal),X1,tc_RealDef_Oreal),tc_RealDef_Oreal),X2,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f1297,f1101]) ).
fof(f1305,plain,
! [X0,X1] : c_HOL_Oinverse__class_Odivide(c_HOL_Oinverse__class_Odivide(X0,c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(sF2,tc_RealDef_Oreal),X1,tc_RealDef_Oreal),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(sF2,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Oinverse__class_Odivide(c_HOL_Oinverse__class_Odivide(X0,X1,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(sF2,tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(sF2,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f1298,f1101]) ).
fof(f1306,plain,
! [X0] : c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(sF2,tc_RealDef_Oreal),X0,tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(sF2,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(sF2,tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(X0,c_Int_Onumber__class_Onumber__of(sF2,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f1299,f1101]) ).
fof(f1307,plain,
! [X0,X1] : c_HOL_Oinverse__class_Odivide(X1,X0,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(sF2,tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(X1,c_HOL_Otimes__class_Otimes(X0,c_Int_Onumber__class_Onumber__of(sF2,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f1300,f1101]) ).
fof(f1310,plain,
! [X0,X1] : c_HOL_Oinverse__class_Odivide(X0,X1,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(sF3,c_HOL_Oinverse__class_Odivide(X0,c_HOL_Otimes__class_Otimes(sF3,X1,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f1303,f1103]) ).
fof(f1311,plain,
! [X2,X0,X1] : c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X0,X1,tc_RealDef_Oreal),X2,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(sF3,c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X0,c_HOL_Otimes__class_Otimes(sF3,X1,tc_RealDef_Oreal),tc_RealDef_Oreal),X2,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f1304,f1103]) ).
fof(f1312,plain,
! [X0,X1] : c_HOL_Oinverse__class_Odivide(c_HOL_Oinverse__class_Odivide(X0,c_HOL_Otimes__class_Otimes(sF3,X1,tc_RealDef_Oreal),tc_RealDef_Oreal),sF3,tc_RealDef_Oreal) = c_HOL_Oinverse__class_Odivide(c_HOL_Oinverse__class_Odivide(X0,X1,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(sF3,sF3,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f1305,f1103]) ).
fof(f1313,plain,
! [X0] : c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(sF3,X0,tc_RealDef_Oreal),sF3,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(sF3,c_HOL_Oinverse__class_Odivide(X0,sF3,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f1306,f1103]) ).
fof(f1314,plain,
! [X0,X1] : c_HOL_Oinverse__class_Odivide(X1,X0,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(sF3,c_HOL_Oinverse__class_Odivide(X1,c_HOL_Otimes__class_Otimes(X0,sF3,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f1307,f1103]) ).
fof(f1317,plain,
! [X0] : c_HOL_Oinverse__class_Odivide(X0,c_Transcendental_Opi,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(sF3,c_HOL_Oinverse__class_Odivide(X0,sF4,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(superposition,[],[f1310,f1105]) ).
fof(f1516,plain,
( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF11,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),v_n,tc_nat) ),
inference(superposition,[],[f422,f1119]) ).
fof(f1518,plain,
( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF6,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),sF5,tc_nat) ),
inference(superposition,[],[f422,f1109]) ).
fof(f1519,plain,
( ~ c_HOL_Oord__class_Oless(sF0,sF5,tc_nat)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF6,tc_RealDef_Oreal) ),
inference(forward_demodulation,[],[f1518,f1096]) ).
fof(f1520,plain,
( ~ c_HOL_Oord__class_Oless(sF0,v_n,tc_nat)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF11,tc_RealDef_Oreal) ),
inference(forward_demodulation,[],[f1516,f1096]) ).
fof(f1526,definition,
( spl15_1
<=> c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF6,tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[spl15_1])],[avatar_definition]) ).
fof(f1527,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF6,tc_RealDef_Oreal)
| spl15_1 ),
inference(avatar_component_clause,[],[f1526]) ).
fof(f1528,plain,
( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF6,tc_RealDef_Oreal)
| ~ spl15_1 ),
inference(avatar_component_clause,[],[f1526]) ).
fof(f1530,definition,
( spl15_2
<=> c_HOL_Oord__class_Oless(sF0,sF5,tc_nat) ),
introduced(definition,[new_symbols(definition,[spl15_2])],[avatar_definition]) ).
fof(f1532,plain,
( ~ c_HOL_Oord__class_Oless(sF0,sF5,tc_nat)
| spl15_2 ),
inference(avatar_component_clause,[],[f1530]) ).
fof(f1533,plain,
( spl15_1
| ~ spl15_2 ),
inference(avatar_split_clause,[],[f1519,f1530,f1526]) ).
fof(f1535,definition,
( spl15_3
<=> c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF11,tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[spl15_3])],[avatar_definition]) ).
fof(f1536,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF11,tc_RealDef_Oreal)
| spl15_3 ),
inference(avatar_component_clause,[],[f1535]) ).
fof(f1537,plain,
( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF11,tc_RealDef_Oreal)
| ~ spl15_3 ),
inference(avatar_component_clause,[],[f1535]) ).
fof(f1539,definition,
( spl15_4
<=> c_HOL_Oord__class_Oless(sF0,v_n,tc_nat) ),
introduced(definition,[new_symbols(definition,[spl15_4])],[avatar_definition]) ).
fof(f1541,plain,
( ~ c_HOL_Oord__class_Oless(sF0,v_n,tc_nat)
| spl15_4 ),
inference(avatar_component_clause,[],[f1539]) ).
fof(f1542,plain,
( spl15_3
| ~ spl15_4 ),
inference(avatar_split_clause,[],[f1520,f1539,f1535]) ).
fof(f1578,plain,
! [X2,X0,X1] : c_Power_Opower__class_Opower(X0,c_HOL_Otimes__class_Otimes(X1,X2,tc_nat),tc_Complex_Ocomplex) = c_Power_Opower__class_Opower(c_Power_Opower__class_Opower(X0,X1,tc_Complex_Ocomplex),X2,tc_Complex_Ocomplex),
inference(resolution,[],[f1070,f871]) ).
fof(f1628,plain,
~ c_HOL_Oord__class_Oless(sF11,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(superposition,[],[f216,f1119]) ).
fof(f1630,plain,
~ c_HOL_Oord__class_Oless(sF6,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(superposition,[],[f216,f1109]) ).
fof(f1659,plain,
! [X0] :
( ~ c_HOL_Oord__class_Oless(sF4,X0,tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(sF3,c_HOL_Oinverse__class_Odivide(X0,c_Transcendental_Opi,tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ class_Ring__and__Field_Oordered__field(tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal) ),
inference(superposition,[],[f641,f1105]) ).
fof(f1670,plain,
! [X0] :
( ~ c_HOL_Oord__class_Oless(sF4,X0,tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(sF3,c_HOL_Oinverse__class_Odivide(X0,c_Transcendental_Opi,tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal) ),
inference(forward_subsumption_resolution,[],[f1659,f1037]) ).
fof(f1697,plain,
! [X0] :
( c_HOL_Oord__class_Oless(sF3,c_HOL_Oinverse__class_Odivide(X0,c_Transcendental_Opi,tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(sF4,X0,tc_RealDef_Oreal) ),
inference(forward_subsumption_resolution,[],[f1670,f299]) ).
fof(f1740,plain,
( c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal) = c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_lessequals(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(resolution,[],[f576,f231]) ).
fof(f1743,plain,
~ c_lessequals(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_subsumption_resolution,[],[f1740,f586]) ).
fof(f1745,plain,
~ c_lessequals(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF1),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF1),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f1743,f1099]) ).
fof(f1746,plain,
~ c_lessequals(c_Int_Onumber__class_Onumber__of(sF2,tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(sF2,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f1745,f1101]) ).
fof(f1747,plain,
~ c_lessequals(sF3,c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,sF3,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f1746,f1103]) ).
fof(f1963,plain,
! [X0] : c_Power_Opower__class_Opower(c_Complex_Ocis(c_RealDef_Oreal(X0,tc_nat)),sF5,tc_Complex_Ocomplex) = c_Power_Opower__class_Opower(c_Complex_Ocis(sF6),X0,tc_Complex_Ocomplex),
inference(superposition,[],[f1132,f1134]) ).
fof(f2045,plain,
! [X2,X3,X0,X1] : c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X1,X2,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X0,X3,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(sF3,c_HOL_Otimes__class_Otimes(X0,c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X1,c_HOL_Otimes__class_Otimes(sF3,X2,tc_RealDef_Oreal),tc_RealDef_Oreal),X3,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(superposition,[],[f1311,f1161]) ).
fof(f2229,plain,
! [X2,X0,X1] :
( ~ class_Ring__and__Field_Odivision__by__zero(tc_RealDef_Oreal)
| c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Odivide(X0,X1,tc_RealDef_Oreal),X2,tc_RealDef_Oreal) = c_HOL_Oinverse__class_Odivide(c_Power_Opower__class_Opower(X0,X2,tc_RealDef_Oreal),c_Power_Opower__class_Opower(X1,X2,tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(resolution,[],[f1054,f819]) ).
fof(f2230,plain,
! [X2,X0,X1] : c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Odivide(X0,X1,tc_RealDef_Oreal),X2,tc_RealDef_Oreal) = c_HOL_Oinverse__class_Odivide(c_Power_Opower__class_Opower(X0,X2,tc_RealDef_Oreal),c_Power_Opower__class_Opower(X1,X2,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_subsumption_resolution,[],[f2229,f1029]) ).
fof(f2297,plain,
( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF12,tc_RealDef_Oreal)
| ~ class_Ring__and__Field_Oordered__field(tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF11,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF4,tc_RealDef_Oreal) ),
inference(superposition,[],[f598,f1121]) ).
fof(f2299,plain,
( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF12,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF11,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF4,tc_RealDef_Oreal) ),
inference(forward_subsumption_resolution,[],[f2297,f1037]) ).
fof(f2307,definition,
( spl15_18
<=> c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF4,tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[spl15_18])],[avatar_definition]) ).
fof(f2308,plain,
( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF4,tc_RealDef_Oreal)
| ~ spl15_18 ),
inference(avatar_component_clause,[],[f2307]) ).
fof(f2309,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF4,tc_RealDef_Oreal)
| spl15_18 ),
inference(avatar_component_clause,[],[f2307]) ).
fof(f2311,definition,
( spl15_19
<=> c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF12,tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[spl15_19])],[avatar_definition]) ).
fof(f2313,plain,
( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF12,tc_RealDef_Oreal)
| ~ spl15_19 ),
inference(avatar_component_clause,[],[f2311]) ).
fof(f2314,plain,
( ~ spl15_18
| ~ spl15_3
| spl15_19 ),
inference(avatar_split_clause,[],[f2299,f2311,f1535,f2307]) ).
fof(f2321,definition,
( spl15_21
<=> c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF3,tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[spl15_21])],[avatar_definition]) ).
fof(f2322,plain,
( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF3,tc_RealDef_Oreal)
| ~ spl15_21 ),
inference(avatar_component_clause,[],[f2321]) ).
fof(f2323,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF3,tc_RealDef_Oreal)
| spl15_21 ),
inference(avatar_component_clause,[],[f2321]) ).
fof(f2334,plain,
! [X0] : c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal),
inference(resolution,[],[f744,f1031]) ).
fof(f2367,plain,
! [X0] : c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_HOL_Oinverse__class_Odivide(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal),
inference(resolution,[],[f890,f1054]) ).
fof(f2501,plain,
! [X0] : c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(resolution,[],[f730,f1031]) ).
fof(f2511,plain,
! [X0] : c_HOL_Oinverse__class_Odivide(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(superposition,[],[f680,f2501]) ).
fof(f2542,plain,
! [X0] : c_HOL_Oinverse__class_Odivide(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Oinverse__class_Odivide(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f2511,f2334]) ).
fof(f2545,plain,
! [X0] : c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_HOL_Oinverse__class_Odivide(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f2542,f2367]) ).
fof(f2557,plain,
( c_HOL_Ozero__class_Ozero(tc_nat) != sF5
| c_HOL_Ozero__class_Ozero(tc_nat) = v_n
| c_HOL_Ozero__class_Ozero(tc_nat) = v_d ),
inference(superposition,[],[f848,f1107]) ).
fof(f2564,plain,
( sF0 != sF5
| c_HOL_Ozero__class_Ozero(tc_nat) = v_n
| c_HOL_Ozero__class_Ozero(tc_nat) = v_d ),
inference(forward_demodulation,[],[f2557,f1096]) ).
fof(f2572,plain,
( v_n = sF0
| sF0 != sF5
| c_HOL_Ozero__class_Ozero(tc_nat) = v_d ),
inference(forward_demodulation,[],[f2564,f1096]) ).
fof(f2580,plain,
( v_d = sF0
| v_n = sF0
| sF0 != sF5 ),
inference(forward_demodulation,[],[f2572,f1096]) ).
fof(f2589,definition,
( spl15_28
<=> v_d = sF0 ),
introduced(definition,[new_symbols(definition,[spl15_28])],[avatar_definition]) ).
fof(f2591,plain,
( v_d = sF0
| ~ spl15_28 ),
inference(avatar_component_clause,[],[f2589]) ).
fof(f2598,definition,
( spl15_30
<=> sF0 = sF5 ),
introduced(definition,[new_symbols(definition,[spl15_30])],[avatar_definition]) ).
fof(f2602,definition,
( spl15_31
<=> v_n = sF0 ),
introduced(definition,[new_symbols(definition,[spl15_31])],[avatar_definition]) ).
fof(f2603,plain,
( v_n != sF0
| spl15_31 ),
inference(avatar_component_clause,[],[f2602]) ).
fof(f2604,plain,
( v_n = sF0
| ~ spl15_31 ),
inference(avatar_component_clause,[],[f2602]) ).
fof(f2605,plain,
( ~ spl15_30
| spl15_31
| spl15_28 ),
inference(avatar_split_clause,[],[f2580,f2589,f2602,f2598]) ).
fof(f2615,plain,
( c_HOL_Oord__class_Oless(v_d,v_d,tc_nat)
| ~ spl15_28 ),
inference(superposition,[],[f1097,f2591]) ).
fof(f2618,plain,
( ! [X0] : ~ c_HOL_Oord__class_Oless(X0,v_d,tc_nat)
| ~ spl15_28 ),
inference(superposition,[],[f1189,f2591]) ).
fof(f2627,plain,
( $false
| ~ spl15_28 ),
inference(forward_subsumption_resolution,[],[f2615,f2618]) ).
fof(f2628,plain,
~ spl15_28,
inference(avatar_contradiction_clause,[],[f2627]) ).
fof(f2812,plain,
( c_HOL_Oord__class_Oless(sF6,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ class_Ring__and__Field_Oordered__idom(tc_RealDef_Oreal)
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = sF6
| spl15_1 ),
inference(resolution,[],[f1527,f808]) ).
fof(f2813,plain,
( ~ class_Ring__and__Field_Oordered__idom(tc_RealDef_Oreal)
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = sF6
| spl15_1 ),
inference(forward_subsumption_resolution,[],[f2812,f1630]) ).
fof(f2815,plain,
( c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = sF6
| spl15_1 ),
inference(forward_subsumption_resolution,[],[f2813,f1042]) ).
fof(f2832,plain,
( ! [X0] : sF6 = c_HOL_Oinverse__class_Odivide(X0,sF6,tc_RealDef_Oreal)
| spl15_1 ),
inference(superposition,[],[f2545,f2815]) ).
fof(f2887,plain,
( c_HOL_Oord__class_Oless(sF11,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ class_Ring__and__Field_Oordered__idom(tc_RealDef_Oreal)
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = sF11
| spl15_3 ),
inference(resolution,[],[f1536,f808]) ).
fof(f2889,plain,
( ~ class_Ring__and__Field_Oordered__idom(tc_RealDef_Oreal)
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = sF11
| spl15_3 ),
inference(forward_subsumption_resolution,[],[f2887,f1628]) ).
fof(f2891,plain,
( c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = sF11
| spl15_3 ),
inference(forward_subsumption_resolution,[],[f2889,f1042]) ).
fof(f2893,plain,
( sF6 = sF11
| spl15_1
| spl15_3 ),
inference(forward_demodulation,[],[f2891,f2815]) ).
fof(f3063,plain,
( sF6 = sF7
| spl15_1 ),
inference(superposition,[],[f1111,f2832]) ).
fof(f3066,plain,
( sF8 = c_Complex_Ocis(sF6)
| spl15_1 ),
inference(superposition,[],[f1113,f3063]) ).
fof(f3563,plain,
! [X2,X0,X1] :
( ~ class_Ring__and__Field_Odivision__by__zero(tc_RealDef_Oreal)
| c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X0,X1,tc_RealDef_Oreal),X2,tc_RealDef_Oreal) = c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(X0,X2,tc_RealDef_Oreal),X1,tc_RealDef_Oreal) ),
inference(resolution,[],[f911,f1054]) ).
fof(f3564,plain,
! [X2,X0,X1] : c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X0,X1,tc_RealDef_Oreal),X2,tc_RealDef_Oreal) = c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(X0,X2,tc_RealDef_Oreal),X1,tc_RealDef_Oreal),
inference(forward_subsumption_resolution,[],[f3563,f1029]) ).
fof(f3597,plain,
! [X0] : c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(sF3,X0,tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal) = c_HOL_Oinverse__class_Odivide(sF4,X0,tc_RealDef_Oreal),
inference(superposition,[],[f3564,f1105]) ).
fof(f3611,plain,
! [X0] : c_HOL_Otimes__class_Otimes(sF3,c_HOL_Oinverse__class_Odivide(X0,sF3,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(sF3,sF3,tc_RealDef_Oreal),X0,tc_RealDef_Oreal),
inference(superposition,[],[f1313,f3564]) ).
fof(f3819,definition,
( spl15_48
<=> v_n = sF5 ),
introduced(definition,[new_symbols(definition,[spl15_48])],[avatar_definition]) ).
fof(f3821,plain,
( v_n = sF5
| ~ spl15_48 ),
inference(avatar_component_clause,[],[f3819]) ).
fof(f3858,definition,
( spl15_52
<=> c_HOL_Oord__class_Oless(sF11,sF6,tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[spl15_52])],[avatar_definition]) ).
fof(f3860,plain,
( c_HOL_Oord__class_Oless(sF11,sF6,tc_RealDef_Oreal)
| ~ spl15_52 ),
inference(avatar_component_clause,[],[f3858]) ).
fof(f3898,definition,
( spl15_58
<=> sF8 = sF13 ),
introduced(definition,[new_symbols(definition,[spl15_58])],[avatar_definition]) ).
fof(f3900,plain,
( sF8 = sF13
| ~ spl15_58 ),
inference(avatar_component_clause,[],[f3898]) ).
fof(f4033,definition,
( spl15_67
<=> c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = sF12 ),
introduced(definition,[new_symbols(definition,[spl15_67])],[avatar_definition]) ).
fof(f4035,plain,
( c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = sF12
| ~ spl15_67 ),
inference(avatar_component_clause,[],[f4033]) ).
fof(f4985,plain,
c_lessequals(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF1),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),
inference(superposition,[],[f566,f1099]) ).
fof(f4986,plain,
c_lessequals(c_Int_Onumber__class_Onumber__of(sF2,tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),
inference(forward_demodulation,[],[f4985,f1101]) ).
fof(f4989,plain,
c_lessequals(sF3,c_Transcendental_Opi,tc_RealDef_Oreal),
inference(forward_demodulation,[],[f4986,f1103]) ).
fof(f5164,definition,
( spl15_73
<=> c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = sF3 ),
introduced(definition,[new_symbols(definition,[spl15_73])],[avatar_definition]) ).
fof(f5165,plain,
( c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) != sF3
| spl15_73 ),
inference(avatar_component_clause,[],[f5164]) ).
fof(f5166,plain,
( c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = sF3
| ~ spl15_73 ),
inference(avatar_component_clause,[],[f5164]) ).
fof(f5168,plain,
( sF0 = sF5
| spl15_2 ),
inference(resolution,[],[f1532,f1180]) ).
fof(f5752,plain,
! [X0] : c_HOL_Oone__class_Oone(tc_RealDef_Oreal) = c_Power_Opower__class_Opower(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_RealDef_Oreal),
inference(resolution,[],[f529,f1031]) ).
fof(f5753,plain,
! [X0] : c_HOL_Oone__class_Oone(tc_RealDef_Oreal) = c_Power_Opower__class_Opower(X0,sF0,tc_RealDef_Oreal),
inference(forward_demodulation,[],[f5752,f1096]) ).
fof(f5976,plain,
! [X0,X1] : c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Odivide(X0,X1,tc_RealDef_Oreal),sF0,tc_RealDef_Oreal) = c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_Power_Opower__class_Opower(X1,sF0,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(superposition,[],[f2230,f5753]) ).
fof(f5980,plain,
! [X0,X1] : c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal) = c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Odivide(X0,X1,tc_RealDef_Oreal),sF0,tc_RealDef_Oreal),
inference(forward_demodulation,[],[f5976,f5753]) ).
fof(f5987,plain,
c_HOL_Oone__class_Oone(tc_RealDef_Oreal) = c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f5980,f5753]) ).
fof(f6129,plain,
c_RealDef_Oreal(sF5,tc_nat) = c_HOL_Otimes__class_Otimes(c_RealDef_Oreal(v_d,tc_nat),sF11,tc_RealDef_Oreal),
inference(superposition,[],[f1223,f1107]) ).
fof(f6170,plain,
sF6 = c_HOL_Otimes__class_Otimes(c_RealDef_Oreal(v_d,tc_nat),sF11,tc_RealDef_Oreal),
inference(forward_demodulation,[],[f6129,f1109]) ).
fof(f6197,plain,
! [X0] : c_HOL_Otimes__class_Otimes(sF6,X0,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_RealDef_Oreal(v_d,tc_nat),c_HOL_Otimes__class_Otimes(sF11,X0,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(superposition,[],[f624,f6170]) ).
fof(f6494,plain,
( c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_RealDef_Oreal(v_n,tc_nat)
| ~ spl15_31 ),
inference(superposition,[],[f1135,f2604]) ).
fof(f6497,plain,
( ! [X0] : v_n = c_HOL_Otimes__class_Otimes(X0,v_n,tc_nat)
| ~ spl15_31 ),
inference(superposition,[],[f1199,f2604]) ).
fof(f6529,plain,
( c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = sF11
| ~ spl15_31 ),
inference(forward_demodulation,[],[f6494,f1119]) ).
fof(f6550,plain,
( c_HOL_Oord__class_Oless(sF11,sF6,tc_RealDef_Oreal)
| ~ spl15_1
| ~ spl15_31 ),
inference(superposition,[],[f1528,f6529]) ).
fof(f6551,plain,
( c_HOL_Oord__class_Oless(sF11,sF11,tc_RealDef_Oreal)
| ~ spl15_3
| ~ spl15_31 ),
inference(superposition,[],[f1537,f6529]) ).
fof(f6574,plain,
( $false
| ~ spl15_3
| ~ spl15_31 ),
inference(forward_subsumption_resolution,[],[f6551,f273]) ).
fof(f6575,plain,
( ~ spl15_3
| ~ spl15_31 ),
inference(avatar_contradiction_clause,[],[f6574]) ).
fof(f6576,plain,
( spl15_52
| ~ spl15_1
| ~ spl15_31 ),
inference(avatar_split_clause,[],[f6550,f2602,f1526,f3858]) ).
fof(f6654,plain,
( c_RealDef_Oreal(sF5,tc_nat) = sF11
| ~ spl15_48 ),
inference(superposition,[],[f1119,f3821]) ).
fof(f6664,plain,
( sF6 = sF11
| ~ spl15_48 ),
inference(forward_demodulation,[],[f6654,f1109]) ).
fof(f6670,plain,
( c_HOL_Oinverse__class_Odivide(sF4,sF6,tc_RealDef_Oreal) = sF12
| ~ spl15_48 ),
inference(superposition,[],[f1121,f6664]) ).
fof(f6681,plain,
( sF7 = sF12
| ~ spl15_48 ),
inference(forward_demodulation,[],[f6670,f1111]) ).
fof(f6685,plain,
( c_Complex_Ocis(sF7) = sF13
| ~ spl15_48 ),
inference(superposition,[],[f1123,f6681]) ).
fof(f6686,plain,
( sF8 = sF13
| ~ spl15_48 ),
inference(forward_demodulation,[],[f6685,f1113]) ).
fof(f6687,plain,
( spl15_58
| ~ spl15_48 ),
inference(avatar_split_clause,[],[f6686,f3819,f3898]) ).
fof(f6741,plain,
( v_n = sF5
| ~ spl15_31 ),
inference(superposition,[],[f1107,f6497]) ).
fof(f7100,plain,
( c_HOL_Oord__class_Oless(sF6,sF6,tc_RealDef_Oreal)
| ~ spl15_48
| ~ spl15_52 ),
inference(forward_demodulation,[],[f3860,f6664]) ).
fof(f7119,plain,
( $false
| ~ spl15_48
| ~ spl15_52 ),
inference(forward_subsumption_resolution,[],[f7100,f273]) ).
fof(f7120,plain,
( ~ spl15_48
| ~ spl15_52 ),
inference(avatar_contradiction_clause,[],[f7119]) ).
fof(f7380,plain,
( v_n = sF0
| spl15_4 ),
inference(resolution,[],[f1541,f1180]) ).
fof(f7711,plain,
! [X0] :
( c_HOL_Oinverse__class_Odivide(X0,X0,tc_RealDef_Oreal) = c_HOL_Oone__class_Oone(tc_RealDef_Oreal)
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = X0 ),
inference(resolution,[],[f502,f1054]) ).
fof(f7722,plain,
( c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal) ),
inference(superposition,[],[f564,f7711]) ).
fof(f7725,plain,
( c_HOL_Oord__class_Oless(sF3,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(sF4,c_Transcendental_Opi,tc_RealDef_Oreal)
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_Transcendental_Opi ),
inference(superposition,[],[f1697,f7711]) ).
fof(f7758,definition,
( spl15_94
<=> c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[spl15_94])],[avatar_definition]) ).
fof(f7759,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal)
| spl15_94 ),
inference(avatar_component_clause,[],[f7758]) ).
fof(f7760,plain,
( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ spl15_94 ),
inference(avatar_component_clause,[],[f7758]) ).
fof(f7787,definition,
( spl15_100
<=> sF3 = c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[spl15_100])],[avatar_definition]) ).
fof(f7789,plain,
( sF3 = c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ spl15_100 ),
inference(avatar_component_clause,[],[f7787]) ).
fof(f7793,plain,
( c_HOL_Oord__class_Oless(sF3,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(sF4,c_Transcendental_Opi,tc_RealDef_Oreal) ),
inference(forward_subsumption_resolution,[],[f7725,f151]) ).
fof(f7795,plain,
( c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF1),tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal) ),
inference(forward_demodulation,[],[f7722,f1099]) ).
fof(f7825,plain,
( c_Int_Onumber__class_Onumber__of(sF2,tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal) ),
inference(forward_demodulation,[],[f7795,f1101]) ).
fof(f7840,definition,
( spl15_107
<=> c_HOL_Oord__class_Oless(sF3,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[spl15_107])],[avatar_definition]) ).
fof(f7842,plain,
( c_HOL_Oord__class_Oless(sF3,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ spl15_107 ),
inference(avatar_component_clause,[],[f7840]) ).
fof(f7849,plain,
( sF3 = c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal) ),
inference(forward_demodulation,[],[f7825,f1103]) ).
fof(f7852,plain,
( c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF1),tc_RealDef_Oreal)
| sF3 = c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(forward_demodulation,[],[f7849,f1099]) ).
fof(f7854,plain,
( c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_Int_Onumber__class_Onumber__of(sF2,tc_RealDef_Oreal)
| sF3 = c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(forward_demodulation,[],[f7852,f1101]) ).
fof(f7856,plain,
( c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = sF3
| sF3 = c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(forward_demodulation,[],[f7854,f1103]) ).
fof(f7858,plain,
( spl15_100
| spl15_73 ),
inference(avatar_split_clause,[],[f7856,f5164,f7787]) ).
fof(f7869,definition,
( spl15_109
<=> c_HOL_Oord__class_Oless(c_Transcendental_Opi,sF4,tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[spl15_109])],[avatar_definition]) ).
fof(f7870,plain,
( c_HOL_Oord__class_Oless(c_Transcendental_Opi,sF4,tc_RealDef_Oreal)
| ~ spl15_109 ),
inference(avatar_component_clause,[],[f7869]) ).
fof(f7871,plain,
( ~ c_HOL_Oord__class_Oless(c_Transcendental_Opi,sF4,tc_RealDef_Oreal)
| spl15_109 ),
inference(avatar_component_clause,[],[f7869]) ).
fof(f7874,definition,
( spl15_110
<=> c_HOL_Oord__class_Oless(sF4,c_Transcendental_Opi,tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[spl15_110])],[avatar_definition]) ).
fof(f7877,plain,
( ~ spl15_110
| spl15_107 ),
inference(avatar_split_clause,[],[f7793,f7840,f7874]) ).
fof(f7898,plain,
( c_HOL_Oord__class_Oless(sF3,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)
| ~ spl15_73 ),
inference(superposition,[],[f356,f5166]) ).
fof(f7913,plain,
( ! [X0] : sF3 = c_HOL_Oinverse__class_Odivide(X0,sF3,tc_RealDef_Oreal)
| ~ spl15_73 ),
inference(superposition,[],[f2545,f5166]) ).
fof(f7931,plain,
( c_HOL_Oord__class_Oless(sF3,c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF1),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ spl15_73 ),
inference(forward_demodulation,[],[f7898,f1099]) ).
fof(f7932,plain,
( c_HOL_Oord__class_Oless(sF3,c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(sF2,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ spl15_73 ),
inference(forward_demodulation,[],[f7931,f1101]) ).
fof(f7933,plain,
( c_HOL_Oord__class_Oless(sF3,c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,sF3,tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ spl15_73 ),
inference(forward_demodulation,[],[f7932,f1103]) ).
fof(f7934,plain,
( c_HOL_Oord__class_Oless(sF3,sF3,tc_RealDef_Oreal)
| ~ spl15_73 ),
inference(forward_demodulation,[],[f7933,f7913]) ).
fof(f7935,plain,
( $false
| ~ spl15_73 ),
inference(forward_subsumption_resolution,[],[f7934,f273]) ).
fof(f7936,plain,
~ spl15_73,
inference(avatar_contradiction_clause,[],[f7935]) ).
fof(f8155,plain,
( c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) != sF11
| c_HOL_Ozero__class_Ozero(tc_nat) = v_n ),
inference(superposition,[],[f532,f1119]) ).
fof(f8591,plain,
c_HOL_Otimes__class_Otimes(sF5,v_k,tc_nat) = c_HOL_Otimes__class_Otimes(sF9,v_n,tc_nat),
inference(superposition,[],[f1142,f1284]) ).
fof(f11951,plain,
( c_HOL_Oord__class_Oless(sF4,c_Transcendental_Opi,tc_RealDef_Oreal)
| ~ class_Orderings_Olinorder(tc_RealDef_Oreal)
| c_Transcendental_Opi = sF4
| spl15_109 ),
inference(resolution,[],[f7871,f818]) ).
fof(f11958,plain,
( c_HOL_Oord__class_Oless(sF4,c_Transcendental_Opi,tc_RealDef_Oreal)
| c_Transcendental_Opi = sF4
| spl15_109 ),
inference(forward_subsumption_resolution,[],[f11951,f1058]) ).
fof(f11960,definition,
( spl15_128
<=> c_Transcendental_Opi = sF4 ),
introduced(definition,[new_symbols(definition,[spl15_128])],[avatar_definition]) ).
fof(f11962,plain,
( c_Transcendental_Opi = sF4
| ~ spl15_128 ),
inference(avatar_component_clause,[],[f11960]) ).
fof(f11966,plain,
( spl15_128
| spl15_110
| spl15_109 ),
inference(avatar_split_clause,[],[f11958,f7869,f7874,f11960]) ).
fof(f11975,plain,
( sF4 = c_HOL_Otimes__class_Otimes(sF3,sF4,tc_RealDef_Oreal)
| ~ spl15_128 ),
inference(superposition,[],[f1105,f11962]) ).
fof(f11989,plain,
( c_lessequals(sF3,sF4,tc_RealDef_Oreal)
| ~ spl15_128 ),
inference(superposition,[],[f4989,f11962]) ).
fof(f12135,plain,
( sF4 = c_HOL_Otimes__class_Otimes(sF4,sF3,tc_RealDef_Oreal)
| ~ spl15_128 ),
inference(superposition,[],[f874,f11975]) ).
fof(f12644,plain,
! [X0,X1] :
( ~ class_Ring__and__Field_Odivision__by__zero(tc_RealDef_Oreal)
| c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(X0,X1,tc_RealDef_Oreal),X1,tc_RealDef_Oreal) = X0
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = X1 ),
inference(resolution,[],[f827,f1054]) ).
fof(f12645,plain,
! [X0,X1] :
( c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(X0,X1,tc_RealDef_Oreal),X1,tc_RealDef_Oreal) = X0
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = X1 ),
inference(forward_subsumption_resolution,[],[f12644,f1029]) ).
fof(f12647,plain,
! [X0,X1] :
( c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X0,X1,tc_RealDef_Oreal),X1,tc_RealDef_Oreal) = X0
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = X1 ),
inference(forward_demodulation,[],[f12645,f3564]) ).
fof(f12654,plain,
! [X0] :
( c_HOL_Otimes__class_Otimes(sF3,X0,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(sF3,c_HOL_Oinverse__class_Odivide(X0,sF3,tc_RealDef_Oreal),tc_RealDef_Oreal),sF3,tc_RealDef_Oreal)
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = sF3 ),
inference(superposition,[],[f12647,f1313]) ).
fof(f12655,plain,
! [X2,X0,X1] :
( c_HOL_Otimes__class_Otimes(X0,X2,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X0,X1,tc_RealDef_Oreal),X2,tc_RealDef_Oreal),X1,tc_RealDef_Oreal)
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = X1 ),
inference(superposition,[],[f12647,f3564]) ).
fof(f12668,plain,
( sF3 = c_HOL_Oinverse__class_Odivide(sF4,c_Transcendental_Opi,tc_RealDef_Oreal)
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_Transcendental_Opi ),
inference(superposition,[],[f3597,f12647]) ).
fof(f12679,plain,
! [X0,X1] :
( c_HOL_Otimes__class_Otimes(X1,c_HOL_Oinverse__class_Odivide(X0,X1,tc_RealDef_Oreal),tc_RealDef_Oreal) = X0
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = X1 ),
inference(superposition,[],[f874,f12647]) ).
fof(f12682,plain,
! [X2,X0,X1] :
( c_HOL_Oinverse__class_Odivide(X0,X2,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(c_HOL_Oinverse__class_Odivide(X0,X1,tc_RealDef_Oreal),X2,tc_RealDef_Oreal),X1,tc_RealDef_Oreal)
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = X1 ),
inference(superposition,[],[f3564,f12647]) ).
fof(f12689,plain,
! [X0,X1] :
( c_HOL_Oinverse__class_Odivide(X1,c_HOL_Oinverse__class_Odivide(X0,sF3,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(sF3,c_HOL_Oinverse__class_Odivide(X1,X0,tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = sF3 ),
inference(superposition,[],[f1314,f12647]) ).
fof(f12695,plain,
( ! [X0,X1] : c_HOL_Oinverse__class_Odivide(X1,c_HOL_Oinverse__class_Odivide(X0,sF3,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(sF3,c_HOL_Oinverse__class_Odivide(X1,X0,tc_RealDef_Oreal),tc_RealDef_Oreal)
| spl15_73 ),
inference(forward_subsumption_resolution,[],[f12689,f5165]) ).
fof(f12704,plain,
sF3 = c_HOL_Oinverse__class_Odivide(sF4,c_Transcendental_Opi,tc_RealDef_Oreal),
inference(forward_subsumption_resolution,[],[f12668,f151]) ).
fof(f12712,plain,
! [X2,X0,X1] :
( c_HOL_Otimes__class_Otimes(X0,X2,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X0,X1,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X2,X1,tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = X1 ),
inference(forward_demodulation,[],[f12655,f624]) ).
fof(f12713,plain,
( ! [X0] : c_HOL_Otimes__class_Otimes(sF3,X0,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(sF3,c_HOL_Oinverse__class_Odivide(X0,sF3,tc_RealDef_Oreal),tc_RealDef_Oreal),sF3,tc_RealDef_Oreal)
| spl15_73 ),
inference(forward_subsumption_resolution,[],[f12654,f5165]) ).
fof(f12718,plain,
( sF3 = c_HOL_Oinverse__class_Odivide(sF4,sF4,tc_RealDef_Oreal)
| ~ spl15_128 ),
inference(forward_demodulation,[],[f12704,f11962]) ).
fof(f12724,plain,
( ! [X0] : c_HOL_Otimes__class_Otimes(sF3,X0,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(sF3,c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X0,sF3,tc_RealDef_Oreal),sF3,tc_RealDef_Oreal),tc_RealDef_Oreal)
| spl15_73 ),
inference(forward_demodulation,[],[f12713,f624]) ).
fof(f12817,plain,
( c_HOL_Otimes__class_Otimes(sF3,sF3,tc_RealDef_Oreal) = c_HOL_Oinverse__class_Odivide(sF4,c_Transcendental_Opi,tc_RealDef_Oreal)
| ~ spl15_128 ),
inference(superposition,[],[f1317,f12718]) ).
fof(f12829,plain,
( c_HOL_Otimes__class_Otimes(sF3,sF3,tc_RealDef_Oreal) = c_HOL_Oinverse__class_Odivide(sF4,sF4,tc_RealDef_Oreal)
| ~ spl15_128 ),
inference(forward_demodulation,[],[f12817,f11962]) ).
fof(f12831,plain,
( sF3 = c_HOL_Otimes__class_Otimes(sF3,sF3,tc_RealDef_Oreal)
| ~ spl15_128 ),
inference(forward_demodulation,[],[f12829,f12718]) ).
fof(f12993,plain,
! [X0,X1] :
( c_HOL_Oinverse__class_Odivide(X0,c_HOL_Otimes__class_Otimes(sF3,X1,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(sF3,c_HOL_Oinverse__class_Odivide(c_HOL_Oinverse__class_Odivide(X0,X1,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(sF3,sF3,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = sF3 ),
inference(superposition,[],[f12679,f1312]) ).
fof(f12995,plain,
( sF4 = c_HOL_Otimes__class_Otimes(sF11,sF12,tc_RealDef_Oreal)
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = sF11 ),
inference(superposition,[],[f12679,f1121]) ).
fof(f13024,plain,
! [X0,X1] :
( c_HOL_Oinverse__class_Odivide(c_HOL_Oinverse__class_Odivide(X1,X0,tc_RealDef_Oreal),sF3,tc_RealDef_Oreal) = c_HOL_Oinverse__class_Odivide(c_HOL_Oinverse__class_Odivide(X1,c_HOL_Oinverse__class_Odivide(X0,sF3,tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(sF3,sF3,tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = sF3 ),
inference(superposition,[],[f1312,f12679]) ).
fof(f13027,plain,
! [X0] :
( c_HOL_Otimes__class_Otimes(c_RealDef_Oreal(v_d,tc_nat),X0,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(sF6,c_HOL_Oinverse__class_Odivide(X0,sF11,tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = sF11 ),
inference(superposition,[],[f6197,f12679]) ).
fof(f13034,plain,
( ! [X0,X1] : c_HOL_Oinverse__class_Odivide(c_HOL_Oinverse__class_Odivide(X1,X0,tc_RealDef_Oreal),sF3,tc_RealDef_Oreal) = c_HOL_Oinverse__class_Odivide(c_HOL_Oinverse__class_Odivide(X1,c_HOL_Oinverse__class_Odivide(X0,sF3,tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(sF3,sF3,tc_RealDef_Oreal),tc_RealDef_Oreal)
| spl15_73 ),
inference(forward_subsumption_resolution,[],[f13024,f5165]) ).
fof(f13045,plain,
( ! [X0,X1] : c_HOL_Oinverse__class_Odivide(X0,c_HOL_Otimes__class_Otimes(sF3,X1,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(sF3,c_HOL_Oinverse__class_Odivide(c_HOL_Oinverse__class_Odivide(X0,X1,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(sF3,sF3,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)
| spl15_73 ),
inference(forward_subsumption_resolution,[],[f12993,f5165]) ).
fof(f13051,plain,
( ! [X0,X1] : c_HOL_Oinverse__class_Odivide(c_HOL_Oinverse__class_Odivide(X1,X0,tc_RealDef_Oreal),sF3,tc_RealDef_Oreal) = c_HOL_Oinverse__class_Odivide(c_HOL_Oinverse__class_Odivide(X1,c_HOL_Oinverse__class_Odivide(X0,sF3,tc_RealDef_Oreal),tc_RealDef_Oreal),sF3,tc_RealDef_Oreal)
| spl15_73
| ~ spl15_128 ),
inference(forward_demodulation,[],[f13034,f12831]) ).
fof(f13059,plain,
( ! [X0,X1] : c_HOL_Oinverse__class_Odivide(X0,c_HOL_Otimes__class_Otimes(sF3,X1,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Oinverse__class_Odivide(c_HOL_Oinverse__class_Odivide(X0,X1,tc_RealDef_Oreal),sF3,tc_RealDef_Oreal)
| spl15_73 ),
inference(forward_demodulation,[],[f13045,f1310]) ).
fof(f13061,plain,
( ! [X0,X1] : c_HOL_Oinverse__class_Odivide(c_HOL_Oinverse__class_Odivide(X1,X0,tc_RealDef_Oreal),sF3,tc_RealDef_Oreal) = c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(sF3,c_HOL_Oinverse__class_Odivide(X1,X0,tc_RealDef_Oreal),tc_RealDef_Oreal),sF3,tc_RealDef_Oreal)
| spl15_73
| ~ spl15_128 ),
inference(forward_demodulation,[],[f13051,f12695]) ).
fof(f13065,plain,
( ! [X0,X1] : c_HOL_Oinverse__class_Odivide(c_HOL_Oinverse__class_Odivide(X1,X0,tc_RealDef_Oreal),sF3,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(sF3,sF3,tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(X1,X0,tc_RealDef_Oreal),tc_RealDef_Oreal)
| spl15_73
| ~ spl15_128 ),
inference(forward_demodulation,[],[f13061,f3564]) ).
fof(f13068,plain,
( ! [X0,X1] : c_HOL_Oinverse__class_Odivide(c_HOL_Oinverse__class_Odivide(X1,X0,tc_RealDef_Oreal),sF3,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(sF3,c_HOL_Oinverse__class_Odivide(c_HOL_Oinverse__class_Odivide(X1,X0,tc_RealDef_Oreal),sF3,tc_RealDef_Oreal),tc_RealDef_Oreal)
| spl15_73
| ~ spl15_128 ),
inference(forward_demodulation,[],[f13065,f3611]) ).
fof(f13073,plain,
( ! [X0,X1] : c_HOL_Oinverse__class_Odivide(X1,c_HOL_Otimes__class_Otimes(sF3,X0,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(sF3,c_HOL_Oinverse__class_Odivide(X1,c_HOL_Otimes__class_Otimes(sF3,X0,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)
| spl15_73
| ~ spl15_128 ),
inference(forward_demodulation,[],[f13068,f13059]) ).
fof(f13074,plain,
( ! [X0,X1] : c_HOL_Oinverse__class_Odivide(X1,X0,tc_RealDef_Oreal) = c_HOL_Oinverse__class_Odivide(X1,c_HOL_Otimes__class_Otimes(sF3,X0,tc_RealDef_Oreal),tc_RealDef_Oreal)
| spl15_73
| ~ spl15_128 ),
inference(forward_demodulation,[],[f13073,f1310]) ).
fof(f13098,plain,
( ! [X2,X0,X1] : c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X0,X1,tc_RealDef_Oreal),X2,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(sF3,c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X0,X1,tc_RealDef_Oreal),X2,tc_RealDef_Oreal),tc_RealDef_Oreal)
| spl15_73
| ~ spl15_128 ),
inference(superposition,[],[f1311,f13074]) ).
fof(f13153,plain,
! [X0,X1] :
( c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(sF3,X0,tc_RealDef_Oreal),X1,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(sF3,c_HOL_Oinverse__class_Odivide(X0,sF3,tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X1,sF3,tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = sF3 ),
inference(superposition,[],[f12712,f1313]) ).
fof(f13156,plain,
! [X2,X0,X1] :
( c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X0,c_HOL_Otimes__class_Otimes(sF3,X1,tc_RealDef_Oreal),tc_RealDef_Oreal),X2,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(c_HOL_Oinverse__class_Odivide(X0,X1,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(sF3,sF3,tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X2,sF3,tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = sF3 ),
inference(superposition,[],[f12712,f1312]) ).
fof(f13254,plain,
( ! [X2,X0,X1] : c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X0,c_HOL_Otimes__class_Otimes(sF3,X1,tc_RealDef_Oreal),tc_RealDef_Oreal),X2,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(c_HOL_Oinverse__class_Odivide(X0,X1,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(sF3,sF3,tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X2,sF3,tc_RealDef_Oreal),tc_RealDef_Oreal)
| spl15_73 ),
inference(forward_subsumption_resolution,[],[f13156,f5165]) ).
fof(f13257,plain,
( ! [X0,X1] : c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(sF3,X0,tc_RealDef_Oreal),X1,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(sF3,c_HOL_Oinverse__class_Odivide(X0,sF3,tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X1,sF3,tc_RealDef_Oreal),tc_RealDef_Oreal)
| spl15_73 ),
inference(forward_subsumption_resolution,[],[f13153,f5165]) ).
fof(f13282,plain,
( ! [X2,X0,X1] : c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X0,c_HOL_Otimes__class_Otimes(sF3,X1,tc_RealDef_Oreal),tc_RealDef_Oreal),X2,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(c_HOL_Oinverse__class_Odivide(X0,X1,tc_RealDef_Oreal),sF3,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X2,sF3,tc_RealDef_Oreal),tc_RealDef_Oreal)
| spl15_73
| ~ spl15_128 ),
inference(forward_demodulation,[],[f13254,f13074]) ).
fof(f13284,plain,
( ! [X0,X1] : c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(sF3,X0,tc_RealDef_Oreal),X1,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(sF3,c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X0,sF3,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X1,sF3,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)
| spl15_73 ),
inference(forward_demodulation,[],[f13257,f624]) ).
fof(f13294,plain,
( ! [X2,X0,X1] : c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X0,c_HOL_Otimes__class_Otimes(sF3,X1,tc_RealDef_Oreal),tc_RealDef_Oreal),X2,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X0,c_HOL_Otimes__class_Otimes(sF3,X1,tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X2,sF3,tc_RealDef_Oreal),tc_RealDef_Oreal)
| spl15_73
| ~ spl15_128 ),
inference(forward_demodulation,[],[f13282,f13059]) ).
fof(f13295,plain,
( ! [X0,X1] : c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(sF3,X0,tc_RealDef_Oreal),X1,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X0,sF3,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X1,sF3,tc_RealDef_Oreal),tc_RealDef_Oreal)
| spl15_73
| ~ spl15_128 ),
inference(forward_demodulation,[],[f13284,f13098]) ).
fof(f13303,plain,
( ! [X2,X0,X1] : c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X0,X1,tc_RealDef_Oreal),X2,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X0,X1,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X2,sF3,tc_RealDef_Oreal),tc_RealDef_Oreal)
| spl15_73
| ~ spl15_128 ),
inference(forward_demodulation,[],[f13294,f13074]) ).
fof(f13304,plain,
( ! [X0,X1] : c_HOL_Otimes__class_Otimes(sF3,c_HOL_Otimes__class_Otimes(X0,X1,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X0,sF3,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X1,sF3,tc_RealDef_Oreal),tc_RealDef_Oreal)
| spl15_73
| ~ spl15_128 ),
inference(forward_demodulation,[],[f13295,f624]) ).
fof(f13308,plain,
( ! [X0,X1] : c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X0,sF3,tc_RealDef_Oreal),X1,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(sF3,c_HOL_Otimes__class_Otimes(X0,X1,tc_RealDef_Oreal),tc_RealDef_Oreal)
| spl15_73
| ~ spl15_128 ),
inference(forward_demodulation,[],[f13304,f13303]) ).
fof(f13780,plain,
( ! [X0] : c_HOL_Otimes__class_Otimes(X0,sF3,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(sF3,c_HOL_Otimes__class_Otimes(X0,sF3,tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ spl15_128 ),
inference(superposition,[],[f1161,f12831]) ).
fof(f14059,plain,
! [X0,X1] : c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(X0,c_HOL_Otimes__class_Otimes(sF3,X1,tc_RealDef_Oreal),tc_RealDef_Oreal),sF3,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(sF3,c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(X1,X0,tc_RealDef_Oreal),sF3,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(superposition,[],[f1313,f1159]) ).
fof(f14472,plain,
! [X2,X3,X0,X1] :
( ~ class_Ring__and__Field_Odivision__by__zero(tc_RealDef_Oreal)
| c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X0,X1,tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(X2,X3,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(X0,X2,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X1,X3,tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(resolution,[],[f806,f1054]) ).
fof(f14473,plain,
! [X2,X3,X0,X1] : c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X0,X1,tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(X2,X3,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(X0,X2,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X1,X3,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_subsumption_resolution,[],[f14472,f1029]) ).
fof(f14475,plain,
! [X2,X3,X0,X1] : c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X0,X1,tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(X2,X3,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X0,c_HOL_Otimes__class_Otimes(X1,X3,tc_RealDef_Oreal),tc_RealDef_Oreal),X2,tc_RealDef_Oreal),
inference(forward_demodulation,[],[f14473,f3564]) ).
fof(f14619,plain,
! [X0,X1] : c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X0,sF4,tc_RealDef_Oreal),X1,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X0,sF3,tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(X1,c_Transcendental_Opi,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(superposition,[],[f14475,f1105]) ).
fof(f14631,plain,
! [X2,X0,X1] : c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X0,X1,tc_RealDef_Oreal),X2,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(X1,X0,tc_RealDef_Oreal),X1,tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(X2,X1,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(superposition,[],[f14475,f680]) ).
fof(f14720,plain,
! [X2,X0,X1] : c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X0,X1,tc_RealDef_Oreal),X2,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X1,X1,tc_RealDef_Oreal),X0,tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(X2,X1,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f14631,f3564]) ).
fof(f14774,plain,
! [X2,X0,X1] : c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X0,X1,tc_RealDef_Oreal),X2,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X1,X1,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X0,c_HOL_Oinverse__class_Odivide(X2,X1,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f14720,f624]) ).
fof(f14894,plain,
! [X0,X1] : c_HOL_Oinverse__class_Odivide(X0,X1,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X0,c_HOL_Otimes__class_Otimes(X1,X1,tc_RealDef_Oreal),tc_RealDef_Oreal),X1,tc_RealDef_Oreal),
inference(superposition,[],[f3564,f1273]) ).
fof(f14896,plain,
( ! [X0] : c_HOL_Oinverse__class_Odivide(X0,sF3,tc_RealDef_Oreal) = c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(X0,sF3,tc_RealDef_Oreal),sF3,tc_RealDef_Oreal)
| spl15_73
| ~ spl15_128 ),
inference(superposition,[],[f13074,f1273]) ).
fof(f14930,plain,
( ! [X0] : c_HOL_Oinverse__class_Odivide(X0,sF3,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X0,sF3,tc_RealDef_Oreal),sF3,tc_RealDef_Oreal)
| spl15_73
| ~ spl15_128 ),
inference(forward_demodulation,[],[f14896,f3564]) ).
fof(f14932,plain,
! [X0,X1] : c_HOL_Oinverse__class_Odivide(X0,X1,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X0,X1,tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(X1,X1,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f14894,f14475]) ).
fof(f14982,plain,
( ! [X0] : c_HOL_Oinverse__class_Odivide(X0,sF3,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(sF3,c_HOL_Otimes__class_Otimes(X0,sF3,tc_RealDef_Oreal),tc_RealDef_Oreal)
| spl15_73
| ~ spl15_128 ),
inference(forward_demodulation,[],[f14930,f13308]) ).
fof(f15017,plain,
( ! [X0] : c_HOL_Oinverse__class_Odivide(X0,sF3,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(X0,sF3,tc_RealDef_Oreal)
| spl15_73
| ~ spl15_128 ),
inference(forward_demodulation,[],[f14982,f13780]) ).
fof(f15133,plain,
( ~ c_lessequals(sF3,c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,sF3,tc_RealDef_Oreal),tc_RealDef_Oreal)
| spl15_73
| ~ spl15_128 ),
inference(superposition,[],[f1747,f15017]) ).
fof(f15157,plain,
( ~ c_lessequals(sF3,c_HOL_Otimes__class_Otimes(sF4,sF3,tc_RealDef_Oreal),tc_RealDef_Oreal)
| spl15_73
| ~ spl15_128 ),
inference(forward_demodulation,[],[f15133,f11962]) ).
fof(f15180,plain,
( ~ c_lessequals(sF3,sF4,tc_RealDef_Oreal)
| spl15_73
| ~ spl15_128 ),
inference(forward_demodulation,[],[f15157,f12135]) ).
fof(f15198,plain,
( $false
| spl15_73
| ~ spl15_128 ),
inference(forward_subsumption_resolution,[],[f15180,f11989]) ).
fof(f15199,plain,
( spl15_73
| ~ spl15_128 ),
inference(avatar_contradiction_clause,[],[f15198]) ).
fof(f15283,plain,
! [X0,X1] : c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(X0,c_HOL_Otimes__class_Otimes(sF3,X1,tc_RealDef_Oreal),tc_RealDef_Oreal),sF3,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(sF3,c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X1,sF3,tc_RealDef_Oreal),X0,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f14059,f3564]) ).
fof(f15321,plain,
! [X0,X1] : c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X0,sF3,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(sF3,X1,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(sF3,c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X1,sF3,tc_RealDef_Oreal),X0,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f15283,f3564]) ).
fof(f15380,plain,
( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF3,tc_RealDef_Oreal)
| ~ class_Ring__and__Field_Oordered__field(tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF4,tc_RealDef_Oreal) ),
inference(superposition,[],[f598,f12704]) ).
fof(f15468,plain,
( ~ class_Ring__and__Field_Oordered__field(tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF4,tc_RealDef_Oreal)
| spl15_21 ),
inference(forward_subsumption_resolution,[],[f15380,f2323]) ).
fof(f15472,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF4,tc_RealDef_Oreal)
| spl15_21 ),
inference(forward_subsumption_resolution,[],[f15468,f1037]) ).
fof(f15474,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF4,tc_RealDef_Oreal)
| spl15_21 ),
inference(forward_subsumption_resolution,[],[f15472,f299]) ).
fof(f15475,plain,
( $false
| ~ spl15_18
| spl15_21 ),
inference(forward_subsumption_resolution,[],[f15474,f2308]) ).
fof(f15476,plain,
( ~ spl15_18
| spl15_21 ),
inference(avatar_contradiction_clause,[],[f15475]) ).
fof(f17537,plain,
! [X0] : c_HOL_Otimes__class_Otimes(X0,X0,tc_RealDef_Oreal) = c_Power_Opower__class_Opower(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),tc_RealDef_Oreal),
inference(resolution,[],[f557,f1031]) ).
fof(f17538,plain,
! [X0] : c_HOL_Otimes__class_Otimes(X0,X0,tc_RealDef_Oreal) = c_Power_Opower__class_Opower(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF1),tc_nat),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f17537,f1099]) ).
fof(f17541,plain,
! [X0] : c_HOL_Otimes__class_Otimes(X0,X0,tc_RealDef_Oreal) = c_Power_Opower__class_Opower(X0,c_Int_Onumber__class_Onumber__of(sF2,tc_nat),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f17538,f1101]) ).
fof(f17585,plain,
! [X0] : 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_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(X0,c_Power_Opower__class_Opower(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(sF2,tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(superposition,[],[f584,f17541]) ).
fof(f17613,plain,
! [X0] : c_HOL_Oinverse__class_Odivide(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF1),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF1),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(X0,c_Power_Opower__class_Opower(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF1),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(sF2,tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f17585,f1099]) ).
fof(f17630,plain,
! [X0] : c_HOL_Oinverse__class_Odivide(X0,c_Int_Onumber__class_Onumber__of(sF2,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(sF2,tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(X0,c_Power_Opower__class_Opower(c_Int_Onumber__class_Onumber__of(sF2,tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(sF2,tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f17613,f1101]) ).
fof(f17633,plain,
! [X0] : c_HOL_Oinverse__class_Odivide(X0,sF3,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(sF3,c_HOL_Oinverse__class_Odivide(X0,c_Power_Opower__class_Opower(sF3,c_Int_Onumber__class_Onumber__of(sF2,tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f17630,f1103]) ).
fof(f17839,plain,
! [X0,X1] : c_HOL_Oinverse__class_Odivide(X1,c_HOL_Oinverse__class_Odivide(X0,c_Power_Opower__class_Opower(sF3,c_Int_Onumber__class_Onumber__of(sF2,tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(sF3,c_HOL_Oinverse__class_Odivide(X1,c_HOL_Oinverse__class_Odivide(X0,sF3,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(superposition,[],[f1310,f17633]) ).
fof(f17856,plain,
! [X2,X0,X1] : c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X1,c_HOL_Oinverse__class_Odivide(X0,sF3,tc_RealDef_Oreal),tc_RealDef_Oreal),X2,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X1,sF3,tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(X2,c_HOL_Oinverse__class_Odivide(X0,c_Power_Opower__class_Opower(sF3,c_Int_Onumber__class_Onumber__of(sF2,tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(superposition,[],[f14475,f17633]) ).
fof(f17861,plain,
( ! [X2,X0,X1] : c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(sF3,c_HOL_Oinverse__class_Odivide(X1,X0,tc_RealDef_Oreal),tc_RealDef_Oreal),X2,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X1,sF3,tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(X2,c_HOL_Oinverse__class_Odivide(X0,c_Power_Opower__class_Opower(sF3,c_Int_Onumber__class_Onumber__of(sF2,tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)
| spl15_73 ),
inference(forward_demodulation,[],[f17856,f12695]) ).
fof(f17868,plain,
( ! [X0,X1] : c_HOL_Oinverse__class_Odivide(X1,c_HOL_Oinverse__class_Odivide(X0,c_Power_Opower__class_Opower(sF3,c_Int_Onumber__class_Onumber__of(sF2,tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(sF3,c_HOL_Otimes__class_Otimes(sF3,c_HOL_Oinverse__class_Odivide(X1,X0,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)
| spl15_73 ),
inference(forward_demodulation,[],[f17839,f12695]) ).
fof(f17876,plain,
( ! [X2,X0,X1] : c_HOL_Otimes__class_Otimes(sF3,c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X1,X0,tc_RealDef_Oreal),X2,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X1,sF3,tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(X2,c_HOL_Oinverse__class_Odivide(X0,c_Power_Opower__class_Opower(sF3,c_Int_Onumber__class_Onumber__of(sF2,tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)
| spl15_73 ),
inference(forward_demodulation,[],[f17861,f624]) ).
fof(f17884,plain,
( ! [X2,X0,X1] : c_HOL_Otimes__class_Otimes(sF3,c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X1,X0,tc_RealDef_Oreal),X2,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X1,sF3,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(sF3,c_HOL_Otimes__class_Otimes(sF3,c_HOL_Oinverse__class_Odivide(X2,X0,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)
| spl15_73 ),
inference(forward_demodulation,[],[f17876,f17868]) ).
fof(f17898,plain,
( ! [X2,X0,X1] : c_HOL_Otimes__class_Otimes(sF3,c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X1,X0,tc_RealDef_Oreal),X2,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(sF3,c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(sF3,c_HOL_Oinverse__class_Odivide(X2,X0,tc_RealDef_Oreal),tc_RealDef_Oreal),sF3,tc_RealDef_Oreal),X1,tc_RealDef_Oreal),tc_RealDef_Oreal)
| spl15_73 ),
inference(forward_demodulation,[],[f17884,f15321]) ).
fof(f17901,plain,
( ! [X2,X0,X1] : c_HOL_Otimes__class_Otimes(sF3,c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X1,X0,tc_RealDef_Oreal),X2,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(sF3,c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(sF3,sF3,tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(X2,X0,tc_RealDef_Oreal),tc_RealDef_Oreal),X1,tc_RealDef_Oreal),tc_RealDef_Oreal)
| spl15_73 ),
inference(forward_demodulation,[],[f17898,f3564]) ).
fof(f17903,plain,
( ! [X2,X0,X1] : c_HOL_Otimes__class_Otimes(sF3,c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X1,X0,tc_RealDef_Oreal),X2,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(sF3,c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(sF3,sF3,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X2,X0,tc_RealDef_Oreal),X1,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)
| spl15_73 ),
inference(forward_demodulation,[],[f17901,f624]) ).
fof(f17905,plain,
( ! [X2,X0,X1] : c_HOL_Otimes__class_Otimes(sF3,c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X1,X0,tc_RealDef_Oreal),X2,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(sF3,c_HOL_Otimes__class_Otimes(sF3,c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X2,X0,tc_RealDef_Oreal),X1,tc_RealDef_Oreal),sF3,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)
| spl15_73 ),
inference(forward_demodulation,[],[f17903,f3611]) ).
fof(f17907,plain,
( ! [X2,X0,X1] : c_HOL_Otimes__class_Otimes(sF3,c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X1,X0,tc_RealDef_Oreal),X2,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(sF3,c_HOL_Otimes__class_Otimes(sF3,c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(c_HOL_Oinverse__class_Odivide(X2,X0,tc_RealDef_Oreal),sF3,tc_RealDef_Oreal),X1,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)
| spl15_73 ),
inference(forward_demodulation,[],[f17905,f3564]) ).
fof(f17908,plain,
( ! [X2,X0,X1] : c_HOL_Otimes__class_Otimes(sF3,c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X1,X0,tc_RealDef_Oreal),X2,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(sF3,c_HOL_Otimes__class_Otimes(sF3,c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X2,c_HOL_Otimes__class_Otimes(sF3,X0,tc_RealDef_Oreal),tc_RealDef_Oreal),X1,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)
| spl15_73 ),
inference(forward_demodulation,[],[f17907,f13059]) ).
fof(f17909,plain,
( ! [X2,X0,X1] : c_HOL_Otimes__class_Otimes(sF3,c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X1,X0,tc_RealDef_Oreal),X2,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X2,X0,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(sF3,X1,tc_RealDef_Oreal),tc_RealDef_Oreal)
| spl15_73 ),
inference(forward_demodulation,[],[f17908,f2045]) ).
fof(f22803,plain,
! [X2,X0,X1] : c_HOL_Otimes__class_Otimes(X2,c_HOL_Oinverse__class_Odivide(X0,X1,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X1,X1,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X2,c_HOL_Oinverse__class_Odivide(X0,X1,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(superposition,[],[f1159,f14932]) ).
fof(f22821,plain,
! [X2,X0,X1] : c_HOL_Otimes__class_Otimes(X2,c_HOL_Oinverse__class_Odivide(X0,X1,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X2,X1,tc_RealDef_Oreal),X0,tc_RealDef_Oreal),
inference(forward_demodulation,[],[f22803,f14774]) ).
fof(f23333,plain,
! [X0] : c_HOL_Otimes__class_Otimes(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),X0,tc_RealDef_Oreal) = X0,
inference(resolution,[],[f117,f1031]) ).
fof(f23532,plain,
( v_n = sF0
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) != sF11 ),
inference(forward_demodulation,[],[f8155,f1096]) ).
fof(f23553,definition,
( spl15_210
<=> c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = sF11 ),
introduced(definition,[new_symbols(definition,[spl15_210])],[avatar_definition]) ).
fof(f23592,definition,
( spl15_215
<=> ! [X0] : c_HOL_Otimes__class_Otimes(c_RealDef_Oreal(v_d,tc_nat),X0,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(sF6,c_HOL_Oinverse__class_Odivide(X0,sF11,tc_RealDef_Oreal),tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[spl15_215])],[avatar_definition]) ).
fof(f23593,plain,
( ! [X0] : c_HOL_Otimes__class_Otimes(c_RealDef_Oreal(v_d,tc_nat),X0,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(sF6,c_HOL_Oinverse__class_Odivide(X0,sF11,tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ spl15_215 ),
inference(avatar_component_clause,[],[f23592]) ).
fof(f23594,plain,
( spl15_210
| spl15_215 ),
inference(avatar_split_clause,[],[f13027,f23592,f23553]) ).
fof(f23597,definition,
( spl15_216
<=> sF4 = c_HOL_Otimes__class_Otimes(sF11,sF12,tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[spl15_216])],[avatar_definition]) ).
fof(f23599,plain,
( sF4 = c_HOL_Otimes__class_Otimes(sF11,sF12,tc_RealDef_Oreal)
| ~ spl15_216 ),
inference(avatar_component_clause,[],[f23597]) ).
fof(f23600,plain,
( spl15_210
| spl15_216 ),
inference(avatar_split_clause,[],[f12995,f23597,f23553]) ).
fof(f23750,plain,
( c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) != sF11
| spl15_31 ),
inference(forward_subsumption_resolution,[],[f23532,f2603]) ).
fof(f23800,plain,
( ~ spl15_210
| spl15_31 ),
inference(avatar_split_clause,[],[f23750,f2602,f23553]) ).
fof(f24816,plain,
( ! [X0] :
( c_HOL_Otimes__class_Otimes(X0,sF11,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X0,sF12,tc_RealDef_Oreal),sF4,tc_RealDef_Oreal)
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = sF12 )
| ~ spl15_216 ),
inference(superposition,[],[f12712,f23599]) ).
fof(f24825,plain,
( ! [X0] :
( c_HOL_Otimes__class_Otimes(X0,sF11,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(X0,c_HOL_Oinverse__class_Odivide(sF4,sF12,tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = sF12 )
| ~ spl15_216 ),
inference(forward_demodulation,[],[f24816,f22821]) ).
fof(f24845,definition,
( spl15_252
<=> ! [X0] : c_HOL_Otimes__class_Otimes(X0,sF11,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(X0,c_HOL_Oinverse__class_Odivide(sF4,sF12,tc_RealDef_Oreal),tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[spl15_252])],[avatar_definition]) ).
fof(f24846,plain,
( ! [X0] : c_HOL_Otimes__class_Otimes(X0,sF11,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(X0,c_HOL_Oinverse__class_Odivide(sF4,sF12,tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ spl15_252 ),
inference(avatar_component_clause,[],[f24845]) ).
fof(f24847,plain,
( spl15_67
| spl15_252
| ~ spl15_216 ),
inference(avatar_split_clause,[],[f24825,f23597,f24845,f4033]) ).
fof(f25065,plain,
! [X0] : c_HOL_Otimes__class_Otimes(X0,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal) = X0,
inference(superposition,[],[f874,f23333]) ).
fof(f25072,plain,
! [X0,X1] :
( c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X1,X0,tc_RealDef_Oreal),X0,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(X1,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = X0 ),
inference(superposition,[],[f12712,f23333]) ).
fof(f25098,plain,
! [X0] : c_HOL_Otimes__class_Otimes(sF3,c_HOL_Oinverse__class_Odivide(X0,sF3,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Oinverse__class_Odivide(X0,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(superposition,[],[f1314,f23333]) ).
fof(f25117,plain,
! [X0,X1] :
( c_HOL_Otimes__class_Otimes(X1,c_HOL_Oinverse__class_Odivide(X0,X0,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(X1,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = X0 ),
inference(forward_demodulation,[],[f25072,f22821]) ).
fof(f25137,plain,
! [X0,X1] :
( c_HOL_Otimes__class_Otimes(X1,c_HOL_Oinverse__class_Odivide(X0,X0,tc_RealDef_Oreal),tc_RealDef_Oreal) = X1
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = X0 ),
inference(forward_demodulation,[],[f25117,f25065]) ).
fof(f27240,plain,
( ! [X0,X1] : c_HOL_Otimes__class_Otimes(sF3,c_HOL_Oinverse__class_Odivide(X1,c_HOL_Otimes__class_Otimes(sF3,X0,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Oinverse__class_Odivide(X1,c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X0,sF3,tc_RealDef_Oreal),sF3,tc_RealDef_Oreal),tc_RealDef_Oreal)
| spl15_73 ),
inference(superposition,[],[f1310,f12724]) ).
fof(f27308,plain,
( ! [X0,X1] : c_HOL_Otimes__class_Otimes(sF3,c_HOL_Oinverse__class_Odivide(X1,c_HOL_Otimes__class_Otimes(sF3,X0,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Oinverse__class_Odivide(X1,c_HOL_Otimes__class_Otimes(X0,c_HOL_Oinverse__class_Odivide(sF3,sF3,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)
| spl15_73 ),
inference(forward_demodulation,[],[f27240,f22821]) ).
fof(f27343,plain,
( ! [X0,X1] : c_HOL_Oinverse__class_Odivide(X1,X0,tc_RealDef_Oreal) = c_HOL_Oinverse__class_Odivide(X1,c_HOL_Otimes__class_Otimes(X0,c_HOL_Oinverse__class_Odivide(sF3,sF3,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)
| spl15_73 ),
inference(forward_demodulation,[],[f27308,f1310]) ).
fof(f27422,plain,
( ! [X0,X1] : c_HOL_Otimes__class_Otimes(sF3,c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X0,sF3,tc_RealDef_Oreal),X1,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X0,c_HOL_Oinverse__class_Odivide(sF3,sF3,tc_RealDef_Oreal),tc_RealDef_Oreal),X1,tc_RealDef_Oreal)
| spl15_73 ),
inference(superposition,[],[f1311,f27343]) ).
fof(f27483,plain,
( ! [X0,X1] : c_HOL_Otimes__class_Otimes(sF3,c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X0,sF3,tc_RealDef_Oreal),X1,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(X0,c_HOL_Oinverse__class_Odivide(X1,c_HOL_Oinverse__class_Odivide(sF3,sF3,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)
| spl15_73 ),
inference(forward_demodulation,[],[f27422,f22821]) ).
fof(f27514,plain,
( ! [X0,X1] : c_HOL_Otimes__class_Otimes(sF3,c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X0,sF3,tc_RealDef_Oreal),X1,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(X0,c_HOL_Otimes__class_Otimes(sF3,c_HOL_Oinverse__class_Odivide(X1,sF3,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)
| spl15_73 ),
inference(forward_demodulation,[],[f27483,f12695]) ).
fof(f27530,plain,
( ! [X0,X1] : c_HOL_Otimes__class_Otimes(sF3,c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X0,sF3,tc_RealDef_Oreal),X1,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(X0,c_HOL_Oinverse__class_Odivide(X1,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)
| spl15_73 ),
inference(forward_demodulation,[],[f27514,f25098]) ).
fof(f27863,plain,
! [X2,X0,X1] : c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X1,X0,tc_RealDef_Oreal),X2,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X1,X0,tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(X2,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(superposition,[],[f14475,f25065]) ).
fof(f27884,plain,
c_HOL_Oinverse__class_Odivide(sF3,sF3,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(sF3,c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),sF3,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(superposition,[],[f1313,f25065]) ).
fof(f27894,plain,
c_HOL_Oinverse__class_Odivide(sF3,sF3,tc_RealDef_Oreal) = c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f27884,f25098]) ).
fof(f27907,plain,
! [X2,X0,X1] : c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X1,X0,tc_RealDef_Oreal),X2,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(X1,c_HOL_Oinverse__class_Odivide(c_HOL_Oinverse__class_Odivide(X2,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),X0,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f27863,f22821]) ).
fof(f27924,plain,
c_HOL_Oinverse__class_Odivide(sF3,sF3,tc_RealDef_Oreal) = c_HOL_Oone__class_Oone(tc_RealDef_Oreal),
inference(forward_demodulation,[],[f27894,f5987]) ).
fof(f29129,plain,
( ! [X0,X1] : c_HOL_Otimes__class_Otimes(sF3,c_HOL_Otimes__class_Otimes(X0,c_HOL_Oinverse__class_Odivide(X1,sF3,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(X0,c_HOL_Oinverse__class_Odivide(X1,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)
| spl15_73 ),
inference(forward_demodulation,[],[f27530,f22821]) ).
fof(f29155,plain,
! [X2,X0,X1] : c_HOL_Otimes__class_Otimes(X1,c_HOL_Oinverse__class_Odivide(X2,X0,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(X1,c_HOL_Oinverse__class_Odivide(c_HOL_Oinverse__class_Odivide(X2,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),X0,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f27907,f22821]) ).
fof(f35171,plain,
! [X0] :
( c_HOL_Oinverse__class_Odivide(X0,sF3,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X0,sF4,tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal)
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_Transcendental_Opi ),
inference(superposition,[],[f25137,f14619]) ).
fof(f35256,plain,
! [X0] : c_HOL_Oinverse__class_Odivide(X0,sF3,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X0,sF4,tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),
inference(forward_subsumption_resolution,[],[f35171,f151]) ).
fof(f35302,plain,
! [X0] : c_HOL_Oinverse__class_Odivide(X0,sF3,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(X0,c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,sF4,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f35256,f22821]) ).
fof(f35478,plain,
c_HOL_Oinverse__class_Odivide(sF3,sF3,tc_RealDef_Oreal) = c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Transcendental_Opi,tc_RealDef_Oreal),
inference(superposition,[],[f1317,f35302]) ).
fof(f35501,plain,
c_HOL_Oone__class_Oone(tc_RealDef_Oreal) = c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Transcendental_Opi,tc_RealDef_Oreal),
inference(forward_demodulation,[],[f35478,f27924]) ).
fof(f35723,plain,
( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ class_Ring__and__Field_Oordered__field(tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal) ),
inference(superposition,[],[f598,f35501]) ).
fof(f35730,plain,
( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ class_Ring__and__Field_Oordered__field(tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal) ),
inference(duplicate_literal_removal,[],[f35723]) ).
fof(f37024,plain,
( ! [X0] :
( c_HOL_Oord__class_Oless(X0,sF3,tc_RealDef_Oreal)
| ~ class_Ring__and__Field_Oordered__semidom(tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(X0,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal) )
| ~ spl15_100 ),
inference(superposition,[],[f434,f7789]) ).
fof(f37035,plain,
( ! [X0] :
( c_HOL_Oord__class_Oless(X0,sF3,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(X0,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal) )
| ~ spl15_100 ),
inference(forward_subsumption_resolution,[],[f37024,f1030]) ).
fof(f37049,plain,
( ! [X0] :
( ~ c_HOL_Oord__class_Oless(X0,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(X0,sF3,tc_RealDef_Oreal) )
| ~ spl15_94
| ~ spl15_100 ),
inference(forward_subsumption_resolution,[],[f37035,f7760]) ).
fof(f37064,plain,
( c_HOL_Oord__class_Oless(sF3,sF3,tc_RealDef_Oreal)
| ~ spl15_94
| ~ spl15_100
| ~ spl15_107 ),
inference(resolution,[],[f37049,f7842]) ).
fof(f37073,plain,
( $false
| ~ spl15_94
| ~ spl15_100
| ~ spl15_107 ),
inference(forward_subsumption_resolution,[],[f37064,f273]) ).
fof(f37074,plain,
( ~ spl15_94
| ~ spl15_100
| ~ spl15_107 ),
inference(avatar_contradiction_clause,[],[f37073]) ).
fof(f37083,plain,
( ~ class_Ring__and__Field_Oordered__field(tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal)
| spl15_94 ),
inference(forward_subsumption_resolution,[],[f35730,f7759]) ).
fof(f37089,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal)
| spl15_94 ),
inference(forward_subsumption_resolution,[],[f37083,f1037]) ).
fof(f37095,plain,
( $false
| spl15_94 ),
inference(forward_subsumption_resolution,[],[f37089,f299]) ).
fof(f37096,plain,
spl15_94,
inference(avatar_contradiction_clause,[],[f37095]) ).
fof(f40098,plain,
( ! [X0] :
( c_HOL_Oord__class_Oless(X0,sF4,tc_RealDef_Oreal)
| ~ class_Orderings_Opreorder(tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(X0,c_Transcendental_Opi,tc_RealDef_Oreal) )
| ~ spl15_109 ),
inference(resolution,[],[f879,f7870]) ).
fof(f40193,plain,
( ! [X0] :
( ~ c_HOL_Oord__class_Oless(X0,c_Transcendental_Opi,tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(X0,sF4,tc_RealDef_Oreal) )
| ~ spl15_109 ),
inference(forward_subsumption_resolution,[],[f40098,f1057]) ).
fof(f40592,plain,
( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF4,tc_RealDef_Oreal)
| ~ spl15_109 ),
inference(resolution,[],[f40193,f299]) ).
fof(f42172,plain,
c_Power_Opower__class_Opower(c_Complex_Ocis(c_RealDef_Oreal(v_n,tc_nat)),sF9,tc_Complex_Ocomplex) = c_Complex_Ocis(c_RealDef_Oreal(c_HOL_Otimes__class_Otimes(sF5,v_k,tc_nat),tc_nat)),
inference(superposition,[],[f1228,f8591]) ).
fof(f42221,plain,
c_Power_Opower__class_Opower(c_Complex_Ocis(c_RealDef_Oreal(v_n,tc_nat)),sF9,tc_Complex_Ocomplex) = c_Power_Opower__class_Opower(c_Complex_Ocis(c_RealDef_Oreal(v_k,tc_nat)),sF5,tc_Complex_Ocomplex),
inference(forward_demodulation,[],[f42172,f1228]) ).
fof(f42253,plain,
c_Power_Opower__class_Opower(c_Complex_Ocis(c_RealDef_Oreal(v_n,tc_nat)),sF9,tc_Complex_Ocomplex) = c_Power_Opower__class_Opower(c_Complex_Ocis(sF6),v_k,tc_Complex_Ocomplex),
inference(forward_demodulation,[],[f42221,f1963]) ).
fof(f42280,plain,
c_Power_Opower__class_Opower(c_Complex_Ocis(sF6),v_k,tc_Complex_Ocomplex) = c_Power_Opower__class_Opower(c_Complex_Ocis(sF11),sF9,tc_Complex_Ocomplex),
inference(forward_demodulation,[],[f42253,f1119]) ).
fof(f50365,plain,
( c_HOL_Oord__class_Oless(sF12,sF12,tc_RealDef_Oreal)
| ~ spl15_19
| ~ spl15_67 ),
inference(superposition,[],[f2313,f4035]) ).
fof(f50430,plain,
( $false
| ~ spl15_19
| ~ spl15_67 ),
inference(forward_subsumption_resolution,[],[f50365,f273]) ).
fof(f50431,plain,
( ~ spl15_19
| ~ spl15_67 ),
inference(avatar_contradiction_clause,[],[f50430]) ).
fof(f61769,plain,
( ! [X0] : c_HOL_Otimes__class_Otimes(sF3,c_HOL_Oinverse__class_Odivide(X0,c_HOL_Otimes__class_Otimes(sF3,sF11,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Oinverse__class_Odivide(X0,c_HOL_Oinverse__class_Odivide(sF4,sF12,tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ spl15_252 ),
inference(superposition,[],[f1310,f24846]) ).
fof(f61812,plain,
( ! [X0] : c_HOL_Oinverse__class_Odivide(X0,sF11,tc_RealDef_Oreal) = c_HOL_Oinverse__class_Odivide(X0,c_HOL_Oinverse__class_Odivide(sF4,sF12,tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ spl15_252 ),
inference(forward_demodulation,[],[f61769,f1310]) ).
fof(f75396,plain,
( c_HOL_Oinverse__class_Odivide(sF4,c_HOL_Otimes__class_Otimes(sF3,sF6,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Oinverse__class_Odivide(sF7,sF3,tc_RealDef_Oreal)
| spl15_73 ),
inference(superposition,[],[f13059,f1111]) ).
fof(f75699,plain,
( ! [X0] :
( c_HOL_Oinverse__class_Odivide(sF4,X0,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(c_HOL_Oinverse__class_Odivide(sF7,sF3,tc_RealDef_Oreal),X0,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(sF3,sF6,tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(sF3,sF6,tc_RealDef_Oreal) )
| spl15_73 ),
inference(superposition,[],[f12682,f75396]) ).
fof(f75737,plain,
( ! [X0] :
( c_HOL_Oinverse__class_Odivide(sF4,X0,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(sF3,c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(sF6,X0,tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(sF7,sF3,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(sF3,sF6,tc_RealDef_Oreal) )
| spl15_73 ),
inference(forward_demodulation,[],[f75699,f17909]) ).
fof(f75801,definition,
( spl15_590
<=> c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(sF3,sF6,tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[spl15_590])],[avatar_definition]) ).
fof(f75803,plain,
( c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(sF3,sF6,tc_RealDef_Oreal)
| ~ spl15_590 ),
inference(avatar_component_clause,[],[f75801]) ).
fof(f75815,plain,
( ! [X0] :
( c_HOL_Oinverse__class_Odivide(sF4,X0,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(sF6,X0,tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(sF7,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(sF3,sF6,tc_RealDef_Oreal) )
| spl15_73 ),
inference(forward_demodulation,[],[f75737,f29129]) ).
fof(f75847,plain,
( ! [X0] :
( c_HOL_Oinverse__class_Odivide(sF4,X0,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(sF6,c_HOL_Oinverse__class_Odivide(c_HOL_Oinverse__class_Odivide(sF7,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),X0,tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(sF3,sF6,tc_RealDef_Oreal) )
| spl15_73 ),
inference(forward_demodulation,[],[f75815,f22821]) ).
fof(f75866,plain,
( ! [X0] :
( c_HOL_Oinverse__class_Odivide(sF4,X0,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(sF6,c_HOL_Oinverse__class_Odivide(sF7,X0,tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(sF3,sF6,tc_RealDef_Oreal) )
| spl15_73 ),
inference(forward_demodulation,[],[f75847,f29155]) ).
fof(f75874,definition,
( spl15_596
<=> ! [X0] : c_HOL_Oinverse__class_Odivide(sF4,X0,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(sF6,c_HOL_Oinverse__class_Odivide(sF7,X0,tc_RealDef_Oreal),tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[spl15_596])],[avatar_definition]) ).
fof(f75875,plain,
( ! [X0] : c_HOL_Oinverse__class_Odivide(sF4,X0,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(sF6,c_HOL_Oinverse__class_Odivide(sF7,X0,tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ spl15_596 ),
inference(avatar_component_clause,[],[f75874]) ).
fof(f75876,plain,
( spl15_590
| spl15_596
| spl15_73 ),
inference(avatar_split_clause,[],[f75866,f5164,f75874,f75801]) ).
fof(f76050,plain,
( c_HOL_Oinverse__class_Odivide(sF4,c_HOL_Oinverse__class_Odivide(sF4,sF12,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(sF6,c_HOL_Oinverse__class_Odivide(sF7,sF11,tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ spl15_252
| ~ spl15_596 ),
inference(superposition,[],[f75875,f61812]) ).
fof(f76146,plain,
( c_HOL_Oinverse__class_Odivide(sF4,c_HOL_Oinverse__class_Odivide(sF4,sF12,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_RealDef_Oreal(v_d,tc_nat),sF7,tc_RealDef_Oreal)
| ~ spl15_215
| ~ spl15_252
| ~ spl15_596 ),
inference(forward_demodulation,[],[f76050,f23593]) ).
fof(f76175,plain,
( c_HOL_Oinverse__class_Odivide(sF4,sF11,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_RealDef_Oreal(v_d,tc_nat),sF7,tc_RealDef_Oreal)
| ~ spl15_215
| ~ spl15_252
| ~ spl15_596 ),
inference(forward_demodulation,[],[f76146,f61812]) ).
fof(f76186,plain,
( sF12 = c_HOL_Otimes__class_Otimes(c_RealDef_Oreal(v_d,tc_nat),sF7,tc_RealDef_Oreal)
| ~ spl15_215
| ~ spl15_252
| ~ spl15_596 ),
inference(forward_demodulation,[],[f76175,f1121]) ).
fof(f76361,plain,
( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ class_Ring__and__Field_Oordered__semiring__strict(tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF6,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF3,tc_RealDef_Oreal)
| ~ spl15_590 ),
inference(superposition,[],[f838,f75803]) ).
fof(f76373,plain,
( ~ class_Ring__and__Field_Oordered__semiring__strict(tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF6,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF3,tc_RealDef_Oreal)
| ~ spl15_590 ),
inference(forward_subsumption_resolution,[],[f76361,f273]) ).
fof(f76418,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF6,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF3,tc_RealDef_Oreal)
| ~ spl15_590 ),
inference(forward_subsumption_resolution,[],[f76373,f1017]) ).
fof(f76438,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF3,tc_RealDef_Oreal)
| ~ spl15_1
| ~ spl15_590 ),
inference(forward_subsumption_resolution,[],[f76418,f1528]) ).
fof(f76448,plain,
( $false
| ~ spl15_1
| ~ spl15_21
| ~ spl15_590 ),
inference(forward_subsumption_resolution,[],[f76438,f2322]) ).
fof(f76449,plain,
( ~ spl15_1
| ~ spl15_21
| ~ spl15_590 ),
inference(avatar_contradiction_clause,[],[f76448]) ).
fof(f76506,plain,
( c_Complex_Ocis(sF12) = c_Power_Opower__class_Opower(c_Complex_Ocis(sF7),v_d,tc_Complex_Ocomplex)
| ~ spl15_215
| ~ spl15_252
| ~ spl15_596 ),
inference(superposition,[],[f783,f76186]) ).
fof(f76581,plain,
( c_Complex_Ocis(sF12) = c_Power_Opower__class_Opower(sF8,v_d,tc_Complex_Ocomplex)
| ~ spl15_215
| ~ spl15_252
| ~ spl15_596 ),
inference(forward_demodulation,[],[f76506,f1113]) ).
fof(f76600,plain,
( sF13 = c_Power_Opower__class_Opower(sF8,v_d,tc_Complex_Ocomplex)
| ~ spl15_215
| ~ spl15_252
| ~ spl15_596 ),
inference(forward_demodulation,[],[f76581,f1123]) ).
fof(f76743,plain,
( ! [X0] : c_Power_Opower__class_Opower(sF13,X0,tc_Complex_Ocomplex) = c_Power_Opower__class_Opower(sF8,c_HOL_Otimes__class_Otimes(v_d,X0,tc_nat),tc_Complex_Ocomplex)
| ~ spl15_215
| ~ spl15_252
| ~ spl15_596 ),
inference(superposition,[],[f1578,f76600]) ).
fof(f76891,plain,
( c_Power_Opower__class_Opower(sF8,sF9,tc_Complex_Ocomplex) = c_Power_Opower__class_Opower(sF13,v_k,tc_Complex_Ocomplex)
| ~ spl15_215
| ~ spl15_252
| ~ spl15_596 ),
inference(superposition,[],[f76743,f1115]) ).
fof(f76945,plain,
( c_Power_Opower__class_Opower(sF8,sF9,tc_Complex_Ocomplex) = sF14
| ~ spl15_215
| ~ spl15_252
| ~ spl15_596 ),
inference(forward_demodulation,[],[f76891,f1125]) ).
fof(f76956,plain,
( sF10 = sF14
| ~ spl15_215
| ~ spl15_252
| ~ spl15_596 ),
inference(forward_demodulation,[],[f76945,f1117]) ).
fof(f76959,plain,
( $false
| ~ spl15_215
| ~ spl15_252
| ~ spl15_596 ),
inference(forward_subsumption_resolution,[],[f76956,f1126]) ).
fof(f76960,plain,
( ~ spl15_215
| ~ spl15_252
| ~ spl15_596 ),
inference(avatar_contradiction_clause,[],[f76959]) ).
fof(f77034,plain,
( $false
| spl15_18
| ~ spl15_109 ),
inference(forward_subsumption_resolution,[],[f40592,f2309]) ).
fof(f77035,plain,
( spl15_18
| ~ spl15_109 ),
inference(avatar_contradiction_clause,[],[f77034]) ).
fof(f77167,plain,
( spl15_30
| spl15_2 ),
inference(avatar_split_clause,[],[f5168,f1530,f2598]) ).
fof(f77183,plain,
( spl15_31
| spl15_4 ),
inference(avatar_split_clause,[],[f7380,f1539,f2602]) ).
fof(f77194,plain,
( spl15_48
| ~ spl15_31 ),
inference(avatar_split_clause,[],[f6741,f2602,f3819]) ).
fof(f80294,plain,
( c_Power_Opower__class_Opower(c_Complex_Ocis(sF6),v_k,tc_Complex_Ocomplex) = c_Power_Opower__class_Opower(c_Complex_Ocis(sF6),sF9,tc_Complex_Ocomplex)
| spl15_1
| spl15_3 ),
inference(superposition,[],[f42280,f2893]) ).
fof(f80355,plain,
( sF14 = c_Power_Opower__class_Opower(sF8,v_k,tc_Complex_Ocomplex)
| ~ spl15_58 ),
inference(superposition,[],[f1125,f3900]) ).
fof(f81866,plain,
( c_Power_Opower__class_Opower(sF8,sF9,tc_Complex_Ocomplex) = c_Power_Opower__class_Opower(sF8,v_k,tc_Complex_Ocomplex)
| spl15_1
| spl15_3 ),
inference(forward_demodulation,[],[f80294,f3066]) ).
fof(f81892,plain,
( c_Power_Opower__class_Opower(sF8,sF9,tc_Complex_Ocomplex) = sF14
| spl15_1
| spl15_3
| ~ spl15_58 ),
inference(forward_demodulation,[],[f81866,f80355]) ).
fof(f81909,plain,
( sF10 = sF14
| spl15_1
| spl15_3
| ~ spl15_58 ),
inference(forward_demodulation,[],[f81892,f1117]) ).
fof(f81919,plain,
( $false
| spl15_1
| spl15_3
| ~ spl15_58 ),
inference(forward_subsumption_resolution,[],[f81909,f1126]) ).
fof(f81920,plain,
( spl15_1
| spl15_3
| ~ spl15_58 ),
inference(avatar_contradiction_clause,[],[f81919]) ).
cnf(s1,plain,
( spl15_1
| ~ spl15_2 ),
inference(sat_conversion,[],[f1533]) ).
cnf(s2,plain,
( spl15_3
| ~ spl15_4 ),
inference(sat_conversion,[],[f1542]) ).
cnf(s15,plain,
( ~ spl15_3
| ~ spl15_18
| spl15_19 ),
inference(sat_conversion,[],[f2314]) ).
cnf(s23,plain,
( spl15_28
| ~ spl15_30
| spl15_31 ),
inference(sat_conversion,[],[f2605]) ).
cnf(s25,plain,
~ spl15_28,
inference(sat_conversion,[],[f2628]) ).
cnf(s108,plain,
( ~ spl15_3
| ~ spl15_31 ),
inference(sat_conversion,[],[f6575]) ).
cnf(s109,plain,
( ~ spl15_1
| ~ spl15_31
| spl15_52 ),
inference(sat_conversion,[],[f6576]) ).
cnf(s112,plain,
( ~ spl15_48
| spl15_58 ),
inference(sat_conversion,[],[f6687]) ).
cnf(s128,plain,
( ~ spl15_48
| ~ spl15_52 ),
inference(sat_conversion,[],[f7120]) ).
cnf(s153,plain,
( spl15_73
| spl15_100 ),
inference(sat_conversion,[],[f7858]) ).
cnf(s155,plain,
( spl15_107
| ~ spl15_110 ),
inference(sat_conversion,[],[f7877]) ).
cnf(s162,plain,
~ spl15_73,
inference(sat_conversion,[],[f7936]) ).
cnf(s273,plain,
( spl15_109
| spl15_110
| spl15_128 ),
inference(sat_conversion,[],[f11966]) ).
cnf(s316,plain,
( spl15_73
| ~ spl15_128 ),
inference(sat_conversion,[],[f15199]) ).
cnf(s328,plain,
( ~ spl15_18
| spl15_21 ),
inference(sat_conversion,[],[f15476]) ).
cnf(s447,plain,
( spl15_210
| spl15_215 ),
inference(sat_conversion,[],[f23594]) ).
cnf(s448,plain,
( spl15_210
| spl15_216 ),
inference(sat_conversion,[],[f23600]) ).
cnf(s461,plain,
( spl15_31
| ~ spl15_210 ),
inference(sat_conversion,[],[f23800]) ).
cnf(s486,plain,
( spl15_67
| ~ spl15_216
| spl15_252 ),
inference(sat_conversion,[],[f24847]) ).
cnf(s612,plain,
( ~ spl15_94
| ~ spl15_100
| ~ spl15_107 ),
inference(sat_conversion,[],[f37074]) ).
cnf(s615,plain,
spl15_94,
inference(sat_conversion,[],[f37096]) ).
cnf(s790,plain,
( ~ spl15_19
| ~ spl15_67 ),
inference(sat_conversion,[],[f50431]) ).
cnf(s1071,plain,
( spl15_73
| spl15_590
| spl15_596 ),
inference(sat_conversion,[],[f75876]) ).
cnf(s1090,plain,
( ~ spl15_1
| ~ spl15_21
| ~ spl15_590 ),
inference(sat_conversion,[],[f76449]) ).
cnf(s1104,plain,
( ~ spl15_215
| ~ spl15_252
| ~ spl15_596 ),
inference(sat_conversion,[],[f76960]) ).
cnf(s1108,plain,
( spl15_18
| ~ spl15_109 ),
inference(sat_conversion,[],[f77035]) ).
cnf(s1130,plain,
( spl15_2
| spl15_30 ),
inference(sat_conversion,[],[f77167]) ).
cnf(s1151,plain,
( spl15_4
| spl15_31 ),
inference(sat_conversion,[],[f77183]) ).
cnf(s1165,plain,
( ~ spl15_31
| spl15_48 ),
inference(sat_conversion,[],[f77194]) ).
cnf(s1252,plain,
( spl15_1
| spl15_3
| ~ spl15_58 ),
inference(sat_conversion,[],[f81920]) ).
cnf(s1257,plain,
( ~ spl15_100
| ~ spl15_107 ),
inference(rat,[],[s612,s615]) ).
cnf(s1286,plain,
~ spl15_128,
inference(rat,[],[s316,s162]) ).
cnf(s1294,plain,
spl15_100,
inference(rat,[],[s153,s162]) ).
cnf(s1295,plain,
~ spl15_107,
inference(rat,[],[s1257,s1294]) ).
cnf(s1296,plain,
~ spl15_110,
inference(rat,[],[s155,s1295]) ).
cnf(s1297,plain,
spl15_109,
inference(rat,[],[s273,s1286,s1296]) ).
cnf(s1298,plain,
spl15_18,
inference(rat,[],[s1108,s1297]) ).
cnf(s1301,plain,
spl15_21,
inference(rat,[],[s328,s1298]) ).
cnf(s1330,plain,
( ~ spl15_30
| spl15_31 ),
inference(rat,[],[s23,s25]) ).
cnf(s1336,plain,
( ~ spl15_3
| spl15_19 ),
inference(rat,[],[s15,s1298]) ).
cnf(s1340,plain,
spl15_1,
inference(rat,[],[s1252,s112,s108,s1165,s1330,s1130,s1]) ).
cnf(s1341,plain,
~ spl15_590,
inference(rat,[],[s1090,s1301,s1340]) ).
cnf(s1344,plain,
spl15_596,
inference(rat,[],[s1071,s162,s1341]) ).
cnf(s1350,plain,
~ spl15_31,
inference(rat,[],[s128,s109,s1165,s1340]) ).
cnf(s1351,plain,
spl15_4,
inference(rat,[],[s1151,s1350]) ).
cnf(s1352,plain,
~ spl15_210,
inference(rat,[],[s461,s1350]) ).
cnf(s1358,plain,
spl15_3,
inference(rat,[],[s2,s1351]) ).
cnf(s1363,plain,
spl15_216,
inference(rat,[],[s448,s1352]) ).
cnf(s1364,plain,
spl15_215,
inference(rat,[],[s447,s1352]) ).
cnf(s1374,plain,
spl15_19,
inference(rat,[],[s1336,s1358]) ).
cnf(s1375,plain,
~ spl15_252,
inference(rat,[],[s1104,s1344,s1364]) ).
cnf(s1380,plain,
~ spl15_67,
inference(rat,[],[s790,s1374]) ).
cnf(s1382,plain,
$false,
inference(rat,[],[s486,s1363,s1380,s1375]) ).
fof(f81933,plain,
$false,
inference(avatar_sat_refutation,[],[s1382]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV608-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.19 % Computer : n002.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Mon Sep 28 12:03:37 UTC 2026
% 0.08/0.20 % CPUTime :
% 0.08/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.23 Running first-order theorem proving
% 0.08/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 11.61/2.38 % (313454)Input is clausal, will run a generic CNF schedule.
% 11.61/2.38 % (313460)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3913610367:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 11.61/2.38 % (313463)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=559061486:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 11.61/2.38 % (313464)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3358777092:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 11.61/2.38 % (313459)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=2541469124:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 11.61/2.38 % (313465)dis-21_1_sil=8000:lcm=predicate:random_seed=4240283440:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 11.61/2.38 % (313462)lrs+10_1_sil=8000:sp=occurrence:random_seed=93532881:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 11.61/2.38 % (313461)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2563368986:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 11.61/2.38 % (313465)Instruction limit reached!
% 11.61/2.38 % (313465)------------------------------
% 11.61/2.38 % (313465)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.61/2.38 % (313465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.61/2.38 % (313465)CaDiCaL version: 2.1.3
% 11.61/2.38 % (313465)Termination reason: Instruction limit
% 11.61/2.38 % (313465)Termination phase: Saturation
% 11.61/2.38 % (313465)Time elapsed: 0.062 s
% 11.61/2.38 % (313465)Peak memory usage: 89 MB
% 11.61/2.38 % (313465)Instructions burned: 118 (million)
% 11.61/2.38 % (313462)Instruction limit reached!
% 11.61/2.38 % (313462)------------------------------
% 11.61/2.38 % (313462)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.61/2.38 % (313462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.61/2.38 % (313462)CaDiCaL version: 2.1.3
% 11.61/2.38 % (313462)Termination reason: Instruction limit
% 11.61/2.38 % (313462)Termination phase: Saturation
% 11.61/2.38 % (313462)Time elapsed: 0.067 s
% 11.61/2.38 % (313462)Peak memory usage: 89 MB
% 11.61/2.38 % (313462)Instructions burned: 107 (million)
% 11.61/2.38 % (313463)Instruction limit reached!
% 11.61/2.38 % (313463)------------------------------
% 11.61/2.38 % (313463)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.61/2.38 % (313463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.61/2.38 % (313463)CaDiCaL version: 2.1.3
% 11.61/2.38 % (313463)Termination reason: Instruction limit
% 11.61/2.38 % (313463)Termination phase: Saturation
% 11.61/2.38 % (313463)Time elapsed: 0.070 s
% 11.61/2.38 % (313463)Peak memory usage: 89 MB
% 11.61/2.38 % (313463)Instructions burned: 114 (million)
% 11.61/2.38 % (313464)Instruction limit reached!
% 11.61/2.38 % (313464)------------------------------
% 11.61/2.38 % (313464)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.61/2.38 % (313464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.61/2.38 % (313464)CaDiCaL version: 2.1.3
% 11.61/2.38 % (313464)Termination reason: Instruction limit
% 11.61/2.38 % (313464)Termination phase: Saturation
% 11.61/2.38 % (313464)Time elapsed: 0.111 s
% 11.61/2.38 % (313464)Peak memory usage: 90 MB
% 11.61/2.38 % (313464)Instructions burned: 181 (million)
% 11.61/2.38 % (313473)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=3722606868:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 11.61/2.38 % (313473)Refutation not found, incomplete strategy
% 11.61/2.38 % (313473)------------------------------
% 11.61/2.38 % (313473)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.61/2.38 % (313473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.61/2.38 % (313473)CaDiCaL version: 2.1.3
% 11.61/2.38 % (313473)Termination reason: Refutation not found, incomplete strategy
% 11.61/2.38 % (313473)Time elapsed: 0.018 s
% 11.61/2.38 % (313473)Peak memory usage: 89 MB
% 11.61/2.38 % (313473)Instructions burned: 29 (million)
% 11.61/2.38 % (313475)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=975259575:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 22.41/4.00 % (313474)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2107551949:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 22.41/4.00 % (313476)lrs+10_64_to=lpo:sil=8000:random_seed=368099068:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 22.41/4.00 % (313474)Instruction limit reached!
% 22.41/4.00 % (313474)------------------------------
% 22.41/4.00 % (313474)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.41/4.00 % (313474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.41/4.00 % (313474)CaDiCaL version: 2.1.3
% 22.41/4.00 % (313474)Termination reason: Instruction limit
% 22.41/4.00 % (313474)Termination phase: Saturation
% 22.41/4.00 % (313474)Time elapsed: 0.098 s
% 22.41/4.00 % (313474)Peak memory usage: 90 MB
% 22.41/4.00 % (313474)Instructions burned: 190 (million)
% 22.41/4.00 % (313475)Instruction limit reached!
% 22.41/4.00 % (313475)------------------------------
% 22.41/4.00 % (313475)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.41/4.00 % (313475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.41/4.00 % (313475)CaDiCaL version: 2.1.3
% 22.41/4.00 % (313475)Termination reason: Instruction limit
% 22.41/4.00 % (313475)Termination phase: Saturation
% 22.41/4.00 % (313475)Time elapsed: 0.113 s
% 22.41/4.00 % (313475)Peak memory usage: 90 MB
% 22.41/4.00 % (313475)Instructions burned: 219 (million)
% 22.41/4.00 % (313476)Instruction limit reached!
% 22.41/4.00 % (313476)------------------------------
% 22.41/4.00 % (313476)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.41/4.00 % (313476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.41/4.00 % (313476)CaDiCaL version: 2.1.3
% 22.41/4.00 % (313476)Termination reason: Instruction limit
% 22.41/4.00 % (313476)Termination phase: Saturation
% 22.41/4.00 % (313476)Time elapsed: 0.077 s
% 22.41/4.00 % (313476)Peak memory usage: 90 MB
% 22.41/4.00 % (313476)Instructions burned: 128 (million)
% 22.41/4.00 % (313473)------------------------------
% 22.41/4.00 % (313473)------------------------------
% 22.41/4.00 % (313482)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=988777942:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 22.41/4.00 % (313481)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1198547923:avsq=on:i=194:fgj=on:bd=preordered_2994 on theBenchmark for (2994ds/194Mi)
% 22.41/4.00 % (313483)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2742942679:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 22.41/4.00 % (313482)Instruction limit reached!
% 22.41/4.00 % (313482)------------------------------
% 22.41/4.00 % (313482)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.41/4.00 % (313482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.41/4.00 % (313482)CaDiCaL version: 2.1.3
% 22.41/4.00 % (313482)Termination reason: Instruction limit
% 22.41/4.00 % (313482)Termination phase: Saturation
% 22.41/4.00 % (313482)Time elapsed: 0.095 s
% 22.41/4.00 % (313482)Peak memory usage: 91 MB
% 22.41/4.00 % (313482)Instructions burned: 158 (million)
% 22.41/4.00 % (313481)Instruction limit reached!
% 22.41/4.00 % (313481)------------------------------
% 22.41/4.00 % (313481)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.41/4.00 % (313481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.41/4.00 % (313481)CaDiCaL version: 2.1.3
% 22.41/4.00 % (313481)Termination reason: Instruction limit
% 22.41/4.00 % (313481)Termination phase: Saturation
% 22.41/4.00 % (313481)Time elapsed: 0.127 s
% 22.41/4.00 % (313481)Peak memory usage: 90 MB
% 22.41/4.00 % (313481)Instructions burned: 194 (million)
% 22.41/4.00 % (313484)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=2679328311:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 22.41/4.00 % (313484)Instruction limit reached!
% 22.41/4.00 % (313484)------------------------------
% 22.41/4.00 % (313484)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.41/4.00 % (313484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.41/4.00 % (313484)CaDiCaL version: 2.1.3
% 22.41/4.00 % (313484)Termination reason: Instruction limit
% 43.61/6.86 % (313484)Termination phase: Saturation
% 43.61/6.86 % (313484)Time elapsed: 0.055 s
% 43.61/6.86 % (313484)Peak memory usage: 89 MB
% 43.61/6.86 % (313484)Instructions burned: 107 (million)
% 43.61/6.86 % (313488)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=895212561:i=107_2992 on theBenchmark for (2992ds/107Mi)
% 43.61/6.86 % (313489)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1388604350:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2991 on theBenchmark for (2991ds/242Mi)
% 43.61/6.86 % (313488)Instruction limit reached!
% 43.61/6.86 % (313488)------------------------------
% 43.61/6.86 % (313488)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.61/6.86 % (313488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.61/6.86 % (313488)CaDiCaL version: 2.1.3
% 43.61/6.86 % (313488)Termination reason: Instruction limit
% 43.61/6.86 % (313488)Termination phase: Saturation
% 43.61/6.86 % (313488)Time elapsed: 0.063 s
% 43.61/6.86 % (313488)Peak memory usage: 90 MB
% 43.61/6.86 % (313488)Instructions burned: 108 (million)
% 43.61/6.86 % (313491)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3329807277:cond=fast:i=5208:av=off_2990 on theBenchmark for (2990ds/5208Mi)
% 43.61/6.86 % (313489)Instruction limit reached!
% 43.61/6.86 % (313489)------------------------------
% 43.61/6.86 % (313489)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.61/6.86 % (313489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.61/6.86 % (313489)CaDiCaL version: 2.1.3
% 43.61/6.86 % (313489)Termination reason: Instruction limit
% 43.61/6.86 % (313489)Termination phase: Saturation
% 43.61/6.86 % (313489)Time elapsed: 0.150 s
% 43.61/6.86 % (313489)Peak memory usage: 90 MB
% 43.61/6.86 % (313489)Instructions burned: 243 (million)
% 43.61/6.86 % (313494)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=460851683:i=134:sd=2:doe=on:ss=axioms:sgt=14_2989 on theBenchmark for (2989ds/134Mi)
% 43.61/6.86 % (313494)Instruction limit reached!
% 43.61/6.86 % (313494)------------------------------
% 43.61/6.86 % (313494)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.61/6.86 % (313494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.61/6.86 % (313494)CaDiCaL version: 2.1.3
% 43.61/6.86 % (313494)Termination reason: Instruction limit
% 43.61/6.86 % (313494)Termination phase: Saturation
% 43.61/6.86 % (313494)Time elapsed: 0.084 s
% 43.61/6.86 % (313494)Peak memory usage: 90 MB
% 43.61/6.86 % (313494)Instructions burned: 134 (million)
% 43.61/6.86 % (313496)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2836693203:i=499:bd=all_2988 on theBenchmark for (2988ds/499Mi)
% 43.61/6.86 % (313498)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1813663294:i=191:fgj=on:bd=all_2987 on theBenchmark for (2987ds/191Mi)
% 43.61/6.86 % (313496)Instruction limit reached!
% 43.61/6.86 % (313496)------------------------------
% 43.61/6.86 % (313496)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.61/6.86 % (313496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.61/6.86 % (313496)CaDiCaL version: 2.1.3
% 43.61/6.86 % (313496)Termination reason: Instruction limit
% 43.61/6.86 % (313496)Termination phase: Saturation
% 43.61/6.86 % (313496)Time elapsed: 0.256 s
% 43.61/6.86 % (313496)Peak memory usage: 93 MB
% 43.61/6.86 % (313496)Instructions burned: 502 (million)
% 43.61/6.86 % (313498)Instruction limit reached!
% 43.61/6.86 % (313498)------------------------------
% 43.61/6.86 % (313498)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.61/6.86 % (313498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.61/6.86 % (313498)CaDiCaL version: 2.1.3
% 43.61/6.86 % (313498)Termination reason: Instruction limit
% 43.61/6.86 % (313498)Termination phase: Saturation
% 43.61/6.86 % (313498)Time elapsed: 0.123 s
% 43.61/6.86 % (313498)Peak memory usage: 91 MB
% 43.61/6.86 % (313498)Instructions burned: 191 (million)
% 43.61/6.86 % (313501)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1035472077:i=264:kws=precedence:fsr=off_2984 on theBenchmark for (2984ds/264Mi)
% 43.61/6.86 % (313502)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=2735182473:cond=on:i=156:bs=on:gtg=exists_all:er=known_2984 on theBenchmark for (2984ds/156Mi)
% 28.22/7.21 % (313502)Instruction limit reached!
% 28.22/7.21 % (313502)------------------------------
% 28.22/7.21 % (313502)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.22/7.21 % (313502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.22/7.21 % (313502)CaDiCaL version: 2.1.3
% 28.22/7.21 % (313502)Termination reason: Instruction limit
% 28.22/7.21 % (313502)Termination phase: Saturation
% 28.22/7.21 % (313502)Time elapsed: 0.093 s
% 28.22/7.21 % (313502)Peak memory usage: 90 MB
% 28.22/7.21 % (313502)Instructions burned: 156 (million)
% 28.22/7.21 % (313501)Instruction limit reached!
% 28.22/7.21 % (313501)------------------------------
% 28.22/7.21 % (313501)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.22/7.21 % (313501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.22/7.21 % (313501)CaDiCaL version: 2.1.3
% 28.22/7.21 % (313501)Termination reason: Instruction limit
% 28.22/7.21 % (313501)Termination phase: Saturation
% 28.22/7.21 % (313501)Time elapsed: 0.160 s
% 28.22/7.21 % (313501)Peak memory usage: 92 MB
% 28.22/7.21 % (313501)Instructions burned: 264 (million)
% 28.22/7.21 % (313505)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=4004378943:i=3256:kws=precedence:bd=preordered:av=off_2981 on theBenchmark for (2981ds/3256Mi)
% 28.22/7.21 % (313506)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=4035192185:i=537:av=off:ss=included_2981 on theBenchmark for (2981ds/537Mi)
% 28.22/7.21 % (313506)Instruction limit reached!
% 28.22/7.21 % (313506)------------------------------
% 28.22/7.21 % (313506)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.22/7.21 % (313506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.22/7.21 % (313506)CaDiCaL version: 2.1.3
% 28.22/7.21 % (313506)Termination reason: Instruction limit
% 28.22/7.21 % (313506)Termination phase: Saturation
% 28.22/7.21 % (313506)Time elapsed: 0.315 s
% 28.22/7.21 % (313506)Peak memory usage: 92 MB
% 28.22/7.21 % (313506)Instructions burned: 538 (million)
% 28.22/7.21 % (313509)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=1653879063:i=180:bd=preordered:av=off_2976 on theBenchmark for (2976ds/180Mi)
% 28.22/7.21 % (313509)Instruction limit reached!
% 28.22/7.21 % (313509)------------------------------
% 28.22/7.21 % (313509)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.22/7.21 % (313509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.22/7.21 % (313509)CaDiCaL version: 2.1.3
% 28.22/7.21 % (313509)Termination reason: Instruction limit
% 28.22/7.21 % (313509)Termination phase: Saturation
% 28.22/7.21 % (313509)Time elapsed: 0.105 s
% 28.22/7.21 % (313509)Peak memory usage: 90 MB
% 28.22/7.21 % (313509)Instructions burned: 182 (million)
% 28.22/7.21 % (313483)Instruction limit reached!
% 28.22/7.21 % (313483)------------------------------
% 28.22/7.21 % (313483)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.22/7.21 % (313483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.22/7.21 % (313483)CaDiCaL version: 2.1.3
% 28.22/7.21 % (313483)Termination reason: Instruction limit
% 28.22/7.21 % (313483)Termination phase: Saturation
% 28.22/7.21 % (313483)Time elapsed: 2.032 s
% 28.22/7.21 % (313483)Peak memory usage: 150 MB
% 28.22/7.21 % (313483)Instructions burned: 3394 (million)
% 28.22/7.21 % (313511)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=1671158772:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2973 on theBenchmark for (2973ds/10307Mi)
% 28.22/7.21 % (313512)lrs-1010_1024_to=lpo:sil=8000:tgt=ground:plsq=on:plsqc=1:sas=cadical:plsqr=1,32:sp=arity:lma=off:spb=goal:acc=on:bce=on:nwc=1.2:alpa=false:random_seed=1871357778:i=412:gtgl=4:gtg=exists_all_2972 on theBenchmark for (2972ds/412Mi)
% 28.22/7.21 % (313512)Instruction limit reached!
% 28.22/7.21 % (313512)------------------------------
% 28.22/7.21 % (313512)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.22/7.21 % (313512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.22/7.21 % (313512)CaDiCaL version: 2.1.3
% 28.22/7.21 % (313512)Termination reason: Instruction limit
% 28.22/7.21 % (313512)Termination phase: Saturation
% 28.22/7.21 % (313512)Time elapsed: 0.231 s
% 28.22/7.21 % (313512)Peak memory usage: 91 MB
% 28.22/7.21 % (313512)Instructions burned: 414 (million)
% 28.22/7.21 % (313515)ott+1002_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:etr=on:spb=units:urr=on:bsr=unit_only:gs=on:s2agt=16:br=off:random_seed=2017184451:s2pl=no:i=8478:s2at=4:nm=6_2968 on theBenchmark for (2968ds/8478Mi)
% 28.22/7.21 % (313505)Instruction limit reached!
% 28.22/7.21 % (313505)------------------------------
% 28.22/7.21 % (313505)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.22/7.21 % (313505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.22/7.21 % (313505)CaDiCaL version: 2.1.3
% 28.22/7.21 % (313505)Termination reason: Instruction limit
% 28.22/7.21 % (313505)Termination phase: Saturation
% 28.22/7.21 % (313505)Time elapsed: 1.979 s
% 28.22/7.21 % (313505)Peak memory usage: 148 MB
% 28.22/7.21 % (313505)Instructions burned: 3256 (million)
% 28.22/7.21 % (313517)ott-1011_2_sil=32000:bsd=on:sp=reverse_frequency:erd=off:urr=on:rnwc=on:gs=on:s2agt=70:updr=off:lftc=20:random_seed=623622894:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2960 on theBenchmark for (2960ds/303Mi)
% 28.22/7.21 % (313491)Instruction limit reached!
% 28.22/7.21 % (313491)------------------------------
% 28.22/7.21 % (313491)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.22/7.21 % (313491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.22/7.21 % (313491)CaDiCaL version: 2.1.3
% 28.22/7.21 % (313491)Termination reason: Instruction limit
% 28.22/7.21 % (313491)Termination phase: Saturation
% 28.22/7.21 % (313491)Time elapsed: 3.167 s
% 28.22/7.21 % (313491)Peak memory usage: 161 MB
% 28.22/7.21 % (313491)Instructions burned: 5209 (million)
% 28.22/7.21 % (313517)Instruction limit reached!
% 28.22/7.21 % (313517)------------------------------
% 28.22/7.21 % (313517)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.22/7.21 % (313517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.22/7.21 % (313517)CaDiCaL version: 2.1.3
% 28.22/7.21 % (313517)Termination reason: Instruction limit
% 28.22/7.21 % (313517)Termination phase: Saturation
% 28.22/7.21 % (313517)Time elapsed: 0.166 s
% 28.22/7.21 % (313517)Peak memory usage: 91 MB
% 28.22/7.21 % (313517)Instructions burned: 305 (million)
% 28.22/7.21 % (313519)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=2382053454:st=4:i=720:sd=3:fsr=off:ss=axioms_2957 on theBenchmark for (2957ds/720Mi)
% 28.22/7.21 % (313520)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=2583337247:i=598:bs=on:bd=preordered:av=off:ss=axioms_2957 on theBenchmark for (2957ds/598Mi)
% 28.22/7.21 % (313519)Instruction limit reached!
% 28.22/7.21 % (313519)------------------------------
% 28.22/7.21 % (313519)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.22/7.21 % (313519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.22/7.21 % (313519)CaDiCaL version: 2.1.3
% 28.22/7.21 % (313519)Termination reason: Instruction limit
% 28.22/7.21 % (313519)Termination phase: Saturation
% 28.22/7.21 % (313519)Time elapsed: 0.364 s
% 28.22/7.21 % (313519)Peak memory usage: 95 MB
% 28.22/7.21 % (313519)Instructions burned: 721 (million)
% 28.22/7.21 % (313520)Instruction limit reached!
% 28.22/7.21 % (313520)------------------------------
% 28.22/7.21 % (313520)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.22/7.21 % (313520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.22/7.21 % (313520)CaDiCaL version: 2.1.3
% 28.22/7.21 % (313520)Termination reason: Instruction limit
% 28.22/7.21 % (313520)Termination phase: Saturation
% 28.22/7.21 % (313520)Time elapsed: 0.350 s
% 28.22/7.21 % (313520)Peak memory usage: 94 MB
% 28.22/7.21 % (313520)Instructions burned: 600 (million)
% 28.22/7.21 % (313523)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=1321827442:i=2989:sd=3:ss=axioms:sgt=60_2952 on theBenchmark for (2952ds/2989Mi)
% 28.22/7.21 % (313524)dis+1011_1_ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:bsd=on:sp=const_min:spb=goal_then_units:lcm=predicate:urr=ec_only:s2agt=16:random_seed=1670465694:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2952 on theBenchmark for (2952ds/1997Mi)
% 28.22/7.21 % (313524)Instruction limit reached!
% 28.22/7.21 % (313524)------------------------------
% 28.22/7.21 % (313524)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.22/7.21 % (313524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.22/7.21 % (313524)CaDiCaL version: 2.1.3
% 28.22/7.21 % (313524)Termination reason: Instruction limit
% 28.22/7.21 % (313524)Termination phase: Saturation
% 28.22/7.21 % (313524)Time elapsed: 1.250 s
% 28.22/7.21 % (313524)Peak memory usage: 139 MB
% 28.22/7.21 % (313524)Instructions burned: 1998 (million)
% 28.22/7.21 % (313459)First to succeed.
% 28.22/7.21 % (313459)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-313454"
% 28.22/7.21 % (313527)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:drc=off:sp=unary_frequency:urr=ec_only:fd=preordered:random_seed=3694231091:i=2088:bd=preordered:av=off_2938 on theBenchmark for (2938ds/2088Mi)
% 28.22/7.21 % (313459)Refutation found. Thanks to Tanya!
% 28.22/7.21 % SZS status Unsatisfiable for theBenchmark
% 28.22/7.21 % SZS output start Proof for theBenchmark
% See solution above
% 0.19/7.30 % (313459)------------------------------
% 0.19/7.30 % (313459)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.19/7.30 % (313459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/7.30 % (313459)CaDiCaL version: 2.1.3
% 0.19/7.30 % (313459)Termination reason: Refutation
% 0.19/7.30 % (313459)Time elapsed: 6.038 s
% 0.19/7.30 % (313459)Peak memory usage: 195 MB
% 0.19/7.30 % (313459)Instructions burned: 9575 (million)
% 0.19/7.30 % (313459)------------------------------
% 0.19/7.30 % (313459)------------------------------
% 0.19/7.30 % (313454)Success in time 6.533 s
% 0.19/7.30 % Vampire exiting
%------------------------------------------------------------------------------