%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWV620-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:26:08 PM UTC 2026
% Result : Unsatisfiable 6.75s 1.27s
% Output : Refutation 6.75s
% Verified :
% SZS Type : Refutation
% Derivation depth : 38
% Number of leaves : 83
% Syntax : Number of formulae : 368 ( 96 unt; 26 def)
% Number of atoms : 898 ( 89 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 1053 ( 523 ~; 512 |; 0 &)
% ( 18 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 7 ( 1 avg)
% Number of predicates : 37 ( 35 usr; 19 prp; 0-3 aty)
% Number of functors : 23 ( 23 usr; 14 con; 0-3 aty)
% Number of variables : 102 ( 0 sgn 102 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f75,axiom,
! [X2,X0,X1] :
( ~ class_Ring__and__Field_Oring__no__zero__divisors(X0)
| c_HOL_Otimes__class_Otimes(X1,X2,X0) != c_HOL_Ozero__class_Ozero(X0)
| X2 = c_HOL_Ozero__class_Ozero(X0)
| X1 = c_HOL_Ozero__class_Ozero(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_mult__eq__0__iff_0) ).
fof(f76,plain,
! [X2,X0,X1] :
( c_HOL_Ozero__class_Ozero(X0) != c_HOL_Otimes__class_Otimes(X1,X2,X0)
| ~ class_Ring__and__Field_Oring__no__zero__divisors(X0)
| c_HOL_Ozero__class_Ozero(X0) = X2
| c_HOL_Ozero__class_Ozero(X0) = X1 ),
inference(reorient_equations,[],[f75]) ).
fof(f137,axiom,
! [X0,X1] :
( ~ c_lessequals(X0,X1,tc_RealDef_Oreal)
| X0 = X1
| c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_real__less__def_2) ).
fof(f151,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(f152,plain,
c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) != c_Transcendental_Opi,
inference(reorient_equations,[],[f151]) ).
fof(f160,axiom,
! [X2,X0,X1] :
( ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0)
| ~ c_lessequals(X2,X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_linorder__not__less_1) ).
fof(f163,axiom,
! [X2,X0,X1] :
( c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0)
| c_lessequals(X2,X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__leE_0) ).
fof(f164,axiom,
! [X2,X0,X1] :
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_lessequals(X1,X2,X0)
| ~ class_Orderings_Opreorder(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_less__le__not__le_1) ).
fof(f174,axiom,
! [X2,X0,X1] :
( ~ c_lessequals(X1,X2,X0)
| X1 = X2
| c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_linorder__antisym__conv2_0) ).
fof(f177,axiom,
! [X2,X0,X1] :
( ~ class_Orderings_Oorder(X0)
| c_HOL_Oord__class_Oless(X1,X2,X0)
| X2 = X1
| ~ c_lessequals(X1,X2,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_xt1_I11_J_0) ).
fof(f178,plain,
! [X2,X0,X1] :
( ~ c_lessequals(X1,X2,X0)
| c_HOL_Oord__class_Oless(X1,X2,X0)
| X1 = X2
| ~ class_Orderings_Oorder(X0) ),
inference(reorient_equations,[],[f177]) ).
fof(f189,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_lessequals(X1,X3,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_order__le__less__trans_0) ).
fof(f206,axiom,
! [X0,X1] :
( ~ class_OrderedGroup_Ogroup__add(X0)
| c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(X1,X0),X0) = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_minus__equation__iff_1) ).
fof(f238,axiom,
! [X0] : c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealDef_Oreal(X0,tc_nat),tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_real__of__nat__ge__zero_0) ).
fof(f258,axiom,
! [X0,X1] :
( ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(X1,X0,tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_lessequals(X1,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_real__0__le__divide__iff_0) ).
fof(f318,axiom,
! [X2,X0,X1] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(X0),c_HOL_Otimes__class_Otimes(X2,X1,X0),X0)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(X0),X1,X0)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(X0),X2,X0)
| ~ class_Ring__and__Field_Oordered__semiring__strict(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_zero__less__mult__pos_0) ).
fof(f371,axiom,
! [X2,X0,X1] :
( c_HOL_Oord__class_Oless(c_HOL_Oinverse__class_Odivide(X1,X2,X0),c_HOL_Ozero__class_Ozero(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(X1,c_HOL_Ozero__class_Ozero(X0),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_divide__neg__pos_0) ).
fof(f376,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(f389,axiom,
! [X2,X0,X1] :
( ~ c_lessequals(X2,X1,X0)
| c_lessequals(c_HOL_Ouminus__class_Ouminus(X1,X0),c_HOL_Ouminus__class_Ouminus(X2,X0),X0)
| ~ class_OrderedGroup_Opordered__ab__group__add(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_le__imp__neg__le_0) ).
fof(f395,axiom,
! [X2,X0,X1] :
( c_lessequals(c_HOL_Oinverse__class_Odivide(X1,X2,X0),c_HOL_Ozero__class_Ozero(X0),X0)
| ~ class_Ring__and__Field_Odivision__by__zero(X0)
| ~ class_Ring__and__Field_Oordered__field(X0)
| ~ c_lessequals(X2,c_HOL_Ozero__class_Ozero(X0),X0)
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(X0),X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_divide__le__0__iff_4) ).
fof(f425,axiom,
! [X0,X1] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(X1,X1,X0),c_HOL_Ozero__class_Ozero(X0),X0)
| c_HOL_Oord__class_Oless(X1,c_HOL_Ozero__class_Ozero(X0),X0)
| ~ class_OrderedGroup_Olordered__ab__group__add(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_double__add__less__zero__iff__single__less__zero_0) ).
fof(f440,axiom,
! [X2,X0,X1] :
( ~ c_lessequals(X2,X1,X0)
| X1 = X2
| ~ c_lessequals(X1,X2,X0)
| ~ class_Orderings_Oorder(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_order__antisym__conv_0) ).
fof(f459,axiom,
! [X0,X1] :
( c_lessequals(c_HOL_Ouminus__class_Ouminus(X1,X0),c_HOL_Ozero__class_Ozero(X0),X0)
| ~ class_OrderedGroup_Opordered__ab__group__add(X0)
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(X0),X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_neg__le__0__iff__le_1) ).
fof(f485,axiom,
! [X2,X0,X1] :
( c_lessequals(c_HOL_Ozero__class_Ozero(X0),c_HOL_Otimes__class_Otimes(X1,X2,X0),X0)
| ~ class_Ring__and__Field_Opordered__ring(X0)
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(X0),X2,X0)
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(X0),X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_split__mult__pos__le_0) ).
fof(f491,axiom,
! [X2,X0,X1] :
( c_lessequals(c_HOL_Ozero__class_Ozero(X0),c_HOL_Otimes__class_Otimes(X1,X2,X0),X0)
| ~ class_Ring__and__Field_Opordered__cancel__semiring(X0)
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(X0),X2,X0)
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(X0),X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_mult__nonneg__nonneg_0) ).
fof(f494,axiom,
! [X0,X1] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(X0),c_HOL_Oplus__class_Oplus(X1,X1,X0),X0)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(X0),X1,X0)
| ~ class_OrderedGroup_Olordered__ab__group__add(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_zero__less__double__add__iff__zero__less__single__add_0) ).
fof(f558,axiom,
! [X0,X1] :
( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(X0,X1,tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X1,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_real__mult__order_0) ).
fof(f562,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(f564,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(f623,axiom,
c_lessequals(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__ge__zero_0) ).
fof(f668,axiom,
! [X0,X1] :
( ~ c_lessequals(X1,c_HOL_Ozero__class_Ozero(X0),X0)
| c_lessequals(c_HOL_Ozero__class_Ozero(X0),c_HOL_Ouminus__class_Ouminus(X1,X0),X0)
| ~ class_OrderedGroup_Opordered__ab__group__add(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_neg__0__le__iff__le_1) ).
fof(f684,axiom,
! [X0,X1] :
( c_lessequals(c_HOL_Ouminus__class_Ouminus(X1,X0),X1,X0)
| ~ class_OrderedGroup_Oordered__ab__group__add(X0)
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(X0),X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_neg__less__eq__nonneg_1) ).
fof(f714,axiom,
! [X0,X1] :
( c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(X0,X1,tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X1,tc_RealDef_Oreal) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_real__0__le__divide__iff_4) ).
fof(f731,axiom,
c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_pi__ge__zero_0) ).
fof(f735,axiom,
! [X0] : c_lessequals(X0,X0,tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_real__le__refl_0) ).
fof(f751,axiom,
! [X0,X1] :
( c_lessequals(X0,X1,tc_RealDef_Oreal)
| c_lessequals(X1,X0,tc_RealDef_Oreal) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_real__le__linear_0) ).
fof(f780,axiom,
! [X0,X1] :
( ~ class_Int_Onumber__ring(X0)
| c_HOL_Otimes__class_Otimes(X1,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),X0),X0) = c_HOL_Oplus__class_Oplus(X1,X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_mult__2__right_0) ).
fof(f781,plain,
! [X0,X1] :
( ~ class_Int_Onumber__ring(X0)
| c_HOL_Oplus__class_Oplus(X1,X1,X0) = c_HOL_Otimes__class_Otimes(X1,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),X0),X0) ),
inference(reorient_equations,[],[f780]) ).
fof(f799,axiom,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_RealDef_Oreal(v_k,tc_nat),c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_real0_0) ).
fof(f803,axiom,
! [X2,X0,X1] :
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Opreorder(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_order__less__asym_0) ).
fof(f809,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(f846,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(f847,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,[],[f846]) ).
fof(f864,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(f871,axiom,
( c_HOL_Oord__class_Oless(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_RealDef_Oreal(v_k,tc_nat),c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),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_Transcendental_Opi,tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(v_k,v_n,tc_nat) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_CHAINED_0) ).
fof(f872,axiom,
c_HOL_Oord__class_Oless(v_k,v_n,tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_CHAINED_0_01) ).
fof(f874,negated_conjecture,
~ c_HOL_Oord__class_Oless(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_RealDef_Oreal(v_k,tc_nat),c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),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_Transcendental_Opi,tc_RealDef_Oreal),tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f954,axiom,
class_Ring__and__Field_Opordered__cancel__semiring(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_RealDef__Oreal__Ring__and__Field_Opordered__cancel__semiring) ).
fof(f956,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(f959,axiom,
class_Ring__and__Field_Oring__no__zero__divisors(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_RealDef__Oreal__Ring__and__Field_Oring__no__zero__divisors) ).
fof(f962,axiom,
class_OrderedGroup_Opordered__ab__group__add(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_RealDef__Oreal__OrderedGroup_Opordered__ab__group__add) ).
fof(f963,axiom,
class_OrderedGroup_Olordered__ab__group__add(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_RealDef__Oreal__OrderedGroup_Olordered__ab__group__add) ).
fof(f964,axiom,
class_OrderedGroup_Oordered__ab__group__add(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_RealDef__Oreal__OrderedGroup_Oordered__ab__group__add) ).
fof(f969,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(f976,axiom,
class_Ring__and__Field_Opordered__ring(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_RealDef__Oreal__Ring__and__Field_Opordered__ring) ).
fof(f977,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(f982,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(f990,axiom,
class_OrderedGroup_Ogroup__add(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_RealDef__Oreal__OrderedGroup_Ogroup__add) ).
fof(f995,axiom,
class_Orderings_Opreorder(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_RealDef__Oreal__Orderings_Opreorder) ).
fof(f996,axiom,
class_Orderings_Olinorder(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_RealDef__Oreal__Orderings_Olinorder) ).
fof(f997,axiom,
class_Orderings_Oorder(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_RealDef__Oreal__Orderings_Oorder) ).
fof(f999,axiom,
class_Int_Onumber__ring(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_RealDef__Oreal__Int_Onumber__ring) ).
fof(f1031,definition,
sF0 = c_RealDef_Oreal(v_k,tc_nat),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f1032,plain,
c_RealDef_Oreal(v_k,tc_nat) = sF0,
inference(reorient_equations,[],[f1031]) ).
fof(f1033,definition,
sF1 = c_Int_OBit1(c_Int_OPls),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f1034,plain,
c_Int_OBit1(c_Int_OPls) = sF1,
inference(reorient_equations,[],[f1033]) ).
fof(f1035,definition,
sF2 = c_Int_OBit0(sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f1036,plain,
c_Int_OBit0(sF1) = sF2,
inference(reorient_equations,[],[f1035]) ).
fof(f1037,definition,
sF3 = c_Int_Onumber__class_Onumber__of(sF2,tc_RealDef_Oreal),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f1038,plain,
c_Int_Onumber__class_Onumber__of(sF2,tc_RealDef_Oreal) = sF3,
inference(reorient_equations,[],[f1037]) ).
fof(f1039,definition,
sF4 = c_HOL_Otimes__class_Otimes(sF3,c_Transcendental_Opi,tc_RealDef_Oreal),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f1040,plain,
c_HOL_Otimes__class_Otimes(sF3,c_Transcendental_Opi,tc_RealDef_Oreal) = sF4,
inference(reorient_equations,[],[f1039]) ).
fof(f1041,definition,
sF5 = c_HOL_Otimes__class_Otimes(sF0,sF4,tc_RealDef_Oreal),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f1042,plain,
c_HOL_Otimes__class_Otimes(sF0,sF4,tc_RealDef_Oreal) = sF5,
inference(reorient_equations,[],[f1041]) ).
fof(f1043,definition,
sF6 = c_RealDef_Oreal(v_n,tc_nat),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f1044,plain,
c_RealDef_Oreal(v_n,tc_nat) = sF6,
inference(reorient_equations,[],[f1043]) ).
fof(f1045,definition,
sF7 = c_HOL_Oinverse__class_Odivide(sF5,sF6,tc_RealDef_Oreal),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f1046,plain,
c_HOL_Oinverse__class_Odivide(sF5,sF6,tc_RealDef_Oreal) = sF7,
inference(reorient_equations,[],[f1045]) ).
fof(f1047,plain,
~ c_HOL_Oord__class_Oless(sF7,sF4,tc_RealDef_Oreal),
inference(definition_folding,[],[f874,f1040,f1038,f1036,f1034,f1046,f1044,f1042,f1040,f1038,f1036,f1034,f1032]) ).
fof(f1049,plain,
( c_HOL_Oord__class_Oless(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_RealDef_Oreal(v_k,tc_nat),c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),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_Transcendental_Opi,tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(forward_subsumption_resolution,[],[f871,f872]) ).
fof(f1050,plain,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_RealDef_Oreal(v_k,tc_nat),c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f799,f864]) ).
fof(f1057,plain,
( c_HOL_Oord__class_Oless(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_RealDef_Oreal(v_k,tc_nat),c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(forward_demodulation,[],[f1049,f864]) ).
fof(f1058,plain,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_RealDef_Oreal(v_k,tc_nat),c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),sF6,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f1050,f1044]) ).
fof(f1063,plain,
( c_HOL_Oord__class_Oless(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_RealDef_Oreal(v_k,tc_nat),c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF1),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF1),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(forward_demodulation,[],[f1057,f1034]) ).
fof(f1064,plain,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_RealDef_Oreal(v_k,tc_nat),c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF1),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),sF6,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f1058,f1034]) ).
fof(f1069,plain,
( c_HOL_Oord__class_Oless(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_RealDef_Oreal(v_k,tc_nat),c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(sF2,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(sF2,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(forward_demodulation,[],[f1063,f1036]) ).
fof(f1070,plain,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_RealDef_Oreal(v_k,tc_nat),c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(sF2,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),sF6,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f1064,f1036]) ).
fof(f1075,plain,
( c_HOL_Oord__class_Oless(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_RealDef_Oreal(v_k,tc_nat),c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,sF3,tc_RealDef_Oreal),tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,sF3,tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(forward_demodulation,[],[f1069,f1038]) ).
fof(f1076,plain,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_RealDef_Oreal(v_k,tc_nat),c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,sF3,tc_RealDef_Oreal),tc_RealDef_Oreal),sF6,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f1070,f1038]) ).
fof(f1081,plain,
( c_HOL_Oord__class_Oless(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_RealDef_Oreal(v_k,tc_nat),c_HOL_Otimes__class_Otimes(sF3,c_Transcendental_Opi,tc_RealDef_Oreal),tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(sF3,c_Transcendental_Opi,tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(forward_demodulation,[],[f1075,f864]) ).
fof(f1082,plain,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_RealDef_Oreal(v_k,tc_nat),c_HOL_Otimes__class_Otimes(sF3,c_Transcendental_Opi,tc_RealDef_Oreal),tc_RealDef_Oreal),sF6,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f1076,f864]) ).
fof(f1085,plain,
( c_HOL_Oord__class_Oless(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_RealDef_Oreal(v_k,tc_nat),sF4,tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal),sF4,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(forward_demodulation,[],[f1081,f1040]) ).
fof(f1086,plain,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_RealDef_Oreal(v_k,tc_nat),sF4,tc_RealDef_Oreal),sF6,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f1082,f1040]) ).
fof(f1087,plain,
( c_HOL_Oord__class_Oless(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_RealDef_Oreal(v_k,tc_nat),sF4,tc_RealDef_Oreal),sF6,tc_RealDef_Oreal),sF4,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(forward_demodulation,[],[f1085,f1044]) ).
fof(f1088,plain,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(sF4,c_RealDef_Oreal(v_k,tc_nat),tc_RealDef_Oreal),sF6,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f1086,f864]) ).
fof(f1089,plain,
( c_HOL_Oord__class_Oless(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(sF4,c_RealDef_Oreal(v_k,tc_nat),tc_RealDef_Oreal),sF6,tc_RealDef_Oreal),sF4,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(forward_demodulation,[],[f1087,f864]) ).
fof(f1090,plain,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(sF4,sF0,tc_RealDef_Oreal),sF6,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f1088,f1032]) ).
fof(f1091,plain,
( c_HOL_Oord__class_Oless(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(sF4,sF0,tc_RealDef_Oreal),sF6,tc_RealDef_Oreal),sF4,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(forward_demodulation,[],[f1089,f1032]) ).
fof(f1092,plain,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(sF0,sF4,tc_RealDef_Oreal),sF6,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f1090,f864]) ).
fof(f1093,plain,
( c_HOL_Oord__class_Oless(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(sF0,sF4,tc_RealDef_Oreal),sF6,tc_RealDef_Oreal),sF4,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(forward_demodulation,[],[f1091,f864]) ).
fof(f1094,plain,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(sF5,sF6,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f1092,f1042]) ).
fof(f1095,plain,
( c_HOL_Oord__class_Oless(c_HOL_Oinverse__class_Odivide(sF5,sF6,tc_RealDef_Oreal),sF4,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(forward_demodulation,[],[f1093,f1042]) ).
fof(f1096,plain,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF7,tc_RealDef_Oreal),
inference(forward_demodulation,[],[f1094,f1046]) ).
fof(f1097,plain,
( c_HOL_Oord__class_Oless(sF7,sF4,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(forward_demodulation,[],[f1095,f1046]) ).
fof(f1098,plain,
~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_subsumption_resolution,[],[f1097,f1047]) ).
fof(f1099,plain,
~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),sF6,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f1098,f1044]) ).
fof(f1100,plain,
~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),sF6,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f1099,f864]) ).
fof(f1101,plain,
~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF1),tc_RealDef_Oreal),tc_RealDef_Oreal),sF6,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f1100,f1034]) ).
fof(f1102,plain,
~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(sF2,tc_RealDef_Oreal),tc_RealDef_Oreal),sF6,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f1101,f1036]) ).
fof(f1103,plain,
~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,sF3,tc_RealDef_Oreal),sF6,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f1102,f1038]) ).
fof(f1104,plain,
~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(sF3,c_Transcendental_Opi,tc_RealDef_Oreal),sF6,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f1103,f864]) ).
fof(f1105,plain,
~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(sF4,sF6,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f1104,f1040]) ).
fof(f1110,plain,
c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF0,tc_RealDef_Oreal),
inference(superposition,[],[f238,f1032]) ).
fof(f1111,plain,
c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF6,tc_RealDef_Oreal),
inference(superposition,[],[f238,f1044]) ).
fof(f1112,plain,
~ c_HOL_Oord__class_Oless(sF0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(superposition,[],[f562,f1032]) ).
fof(f1135,plain,
! [X0] : c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal),tc_RealDef_Oreal) = X0,
inference(resolution,[],[f206,f990]) ).
fof(f1237,plain,
( ~ class_Orderings_Olinorder(tc_RealDef_Oreal)
| ~ c_lessequals(c_Transcendental_Opi,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(resolution,[],[f160,f564]) ).
fof(f1239,plain,
( ~ class_Orderings_Olinorder(tc_RealDef_Oreal)
| ~ c_lessequals(sF7,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(resolution,[],[f160,f1096]) ).
fof(f1250,plain,
~ c_lessequals(sF7,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_subsumption_resolution,[],[f1239,f996]) ).
fof(f1252,plain,
~ c_lessequals(c_Transcendental_Opi,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_subsumption_resolution,[],[f1237,f996]) ).
fof(f1257,plain,
( ~ class_Orderings_Olinorder(tc_RealDef_Oreal)
| c_lessequals(c_HOL_Oinverse__class_Odivide(sF4,sF6,tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(resolution,[],[f163,f1105]) ).
fof(f1270,plain,
c_lessequals(c_HOL_Oinverse__class_Odivide(sF4,sF6,tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_subsumption_resolution,[],[f1257,f996]) ).
fof(f1406,plain,
( c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = sF6
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF6,tc_RealDef_Oreal) ),
inference(resolution,[],[f137,f1111]) ).
fof(f1409,plain,
( c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_HOL_Oinverse__class_Odivide(sF4,sF6,tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(c_HOL_Oinverse__class_Odivide(sF4,sF6,tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(resolution,[],[f137,f1270]) ).
fof(f1442,definition,
( spl8_5
<=> c_HOL_Oord__class_Oless(c_HOL_Oinverse__class_Odivide(sF4,sF6,tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[spl8_5])],[avatar_definition]) ).
fof(f1444,plain,
( c_HOL_Oord__class_Oless(c_HOL_Oinverse__class_Odivide(sF4,sF6,tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ spl8_5 ),
inference(avatar_component_clause,[],[f1442]) ).
fof(f1446,definition,
( spl8_6
<=> c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_HOL_Oinverse__class_Odivide(sF4,sF6,tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[spl8_6])],[avatar_definition]) ).
fof(f1448,plain,
( c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_HOL_Oinverse__class_Odivide(sF4,sF6,tc_RealDef_Oreal)
| ~ spl8_6 ),
inference(avatar_component_clause,[],[f1446]) ).
fof(f1449,plain,
( spl8_5
| spl8_6 ),
inference(avatar_split_clause,[],[f1409,f1446,f1442]) ).
fof(f1451,definition,
( spl8_7
<=> c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF6,tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[spl8_7])],[avatar_definition]) ).
fof(f1453,plain,
( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF6,tc_RealDef_Oreal)
| ~ spl8_7 ),
inference(avatar_component_clause,[],[f1451]) ).
fof(f1455,definition,
( spl8_8
<=> c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = sF6 ),
introduced(definition,[new_symbols(definition,[spl8_8])],[avatar_definition]) ).
fof(f1457,plain,
( c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = sF6
| ~ spl8_8 ),
inference(avatar_component_clause,[],[f1455]) ).
fof(f1458,plain,
( spl8_7
| spl8_8 ),
inference(avatar_split_clause,[],[f1406,f1455,f1451]) ).
fof(f1460,definition,
( spl8_9
<=> c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF0,tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[spl8_9])],[avatar_definition]) ).
fof(f1461,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF0,tc_RealDef_Oreal)
| spl8_9 ),
inference(avatar_component_clause,[],[f1460]) ).
fof(f1462,plain,
( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF0,tc_RealDef_Oreal)
| ~ spl8_9 ),
inference(avatar_component_clause,[],[f1460]) ).
fof(f1512,plain,
( ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(sF4,sF6,tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ class_Orderings_Opreorder(tc_RealDef_Oreal)
| ~ spl8_5 ),
inference(resolution,[],[f1444,f164]) ).
fof(f1518,plain,
( ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(sF4,sF6,tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ spl8_5 ),
inference(forward_subsumption_resolution,[],[f1512,f995]) ).
fof(f2330,definition,
( spl8_29
<=> c_lessequals(sF4,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[spl8_29])],[avatar_definition]) ).
fof(f2331,plain,
( ~ c_lessequals(sF4,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| spl8_29 ),
inference(avatar_component_clause,[],[f2330]) ).
fof(f2332,plain,
( c_lessequals(sF4,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ spl8_29 ),
inference(avatar_component_clause,[],[f2330]) ).
fof(f2375,plain,
( c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = sF4
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF4,tc_RealDef_Oreal)
| ~ class_Orderings_Oorder(tc_RealDef_Oreal)
| ~ spl8_29 ),
inference(resolution,[],[f2332,f440]) ).
fof(f2376,plain,
( c_HOL_Oord__class_Oless(sF4,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = sF4
| ~ class_Orderings_Oorder(tc_RealDef_Oreal)
| ~ spl8_29 ),
inference(resolution,[],[f2332,f178]) ).
fof(f2379,plain,
( c_HOL_Oord__class_Oless(sF4,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = sF4
| ~ spl8_29 ),
inference(forward_subsumption_resolution,[],[f2376,f997]) ).
fof(f2380,plain,
( c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = sF4
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF4,tc_RealDef_Oreal)
| ~ spl8_29 ),
inference(forward_subsumption_resolution,[],[f2375,f997]) ).
fof(f2382,definition,
( spl8_33
<=> c_HOL_Oord__class_Oless(sF4,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[spl8_33])],[avatar_definition]) ).
fof(f2384,plain,
( c_HOL_Oord__class_Oless(sF4,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ spl8_33 ),
inference(avatar_component_clause,[],[f2382]) ).
fof(f2386,definition,
( spl8_34
<=> c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = sF4 ),
introduced(definition,[new_symbols(definition,[spl8_34])],[avatar_definition]) ).
fof(f2387,plain,
( c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) != sF4
| spl8_34 ),
inference(avatar_component_clause,[],[f2386]) ).
fof(f2388,plain,
( c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = sF4
| ~ spl8_34 ),
inference(avatar_component_clause,[],[f2386]) ).
fof(f2391,definition,
( spl8_35
<=> c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF4,tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[spl8_35])],[avatar_definition]) ).
fof(f2392,plain,
( c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF4,tc_RealDef_Oreal)
| ~ spl8_35 ),
inference(avatar_component_clause,[],[f2391]) ).
fof(f2393,plain,
( ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF4,tc_RealDef_Oreal)
| spl8_35 ),
inference(avatar_component_clause,[],[f2391]) ).
fof(f2396,plain,
( spl8_34
| spl8_33
| ~ spl8_29 ),
inference(avatar_split_clause,[],[f2379,f2330,f2382,f2386]) ).
fof(f2397,plain,
( ~ spl8_35
| spl8_34
| ~ spl8_29 ),
inference(avatar_split_clause,[],[f2380,f2330,f2386,f2391]) ).
fof(f2418,plain,
( c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF4,tc_RealDef_Oreal)
| spl8_29 ),
inference(resolution,[],[f2331,f751]) ).
fof(f2423,plain,
( spl8_35
| spl8_29 ),
inference(avatar_split_clause,[],[f2418,f2330,f2391]) ).
fof(f2477,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF4,tc_RealDef_Oreal)
| ~ class_Orderings_Opreorder(tc_RealDef_Oreal)
| ~ spl8_33 ),
inference(resolution,[],[f2384,f803]) ).
fof(f2478,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF4,tc_RealDef_Oreal)
| ~ spl8_33 ),
inference(forward_subsumption_resolution,[],[f2477,f995]) ).
fof(f3019,definition,
( spl8_51
<=> sF3 = sF7 ),
introduced(definition,[new_symbols(definition,[spl8_51])],[avatar_definition]) ).
fof(f3020,plain,
( sF3 != sF7
| spl8_51 ),
inference(avatar_component_clause,[],[f3019]) ).
fof(f3021,plain,
( sF3 = sF7
| ~ spl8_51 ),
inference(avatar_component_clause,[],[f3019]) ).
fof(f3255,plain,
( ! [X0] :
( c_HOL_Oord__class_Oless(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ class_Orderings_Opreorder(tc_RealDef_Oreal)
| ~ c_lessequals(X0,sF4,tc_RealDef_Oreal) )
| ~ spl8_33 ),
inference(resolution,[],[f189,f2384]) ).
fof(f3260,plain,
( ! [X0] :
( c_HOL_Oord__class_Oless(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_lessequals(X0,sF4,tc_RealDef_Oreal) )
| ~ spl8_33 ),
inference(forward_subsumption_resolution,[],[f3255,f995]) ).
fof(f5195,definition,
( spl8_76
<=> c_lessequals(c_HOL_Ouminus__class_Ouminus(sF4,tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[spl8_76])],[avatar_definition]) ).
fof(f5196,plain,
( c_lessequals(c_HOL_Ouminus__class_Ouminus(sF4,tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ spl8_76 ),
inference(avatar_component_clause,[],[f5195]) ).
fof(f5197,plain,
( ~ c_lessequals(c_HOL_Ouminus__class_Ouminus(sF4,tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| spl8_76 ),
inference(avatar_component_clause,[],[f5195]) ).
fof(f5372,plain,
( ~ class_OrderedGroup_Opordered__ab__group__add(tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF4,tc_RealDef_Oreal)
| spl8_76 ),
inference(resolution,[],[f5197,f459]) ).
fof(f6811,plain,
! [X0] : c_HOL_Oplus__class_Oplus(X0,X0,tc_RealDef_Oreal) = 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),
inference(resolution,[],[f781,f999]) ).
fof(f6814,plain,
! [X0] : c_HOL_Oplus__class_Oplus(X0,X0,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF1),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f6811,f1034]) ).
fof(f6817,plain,
! [X0] : c_HOL_Oplus__class_Oplus(X0,X0,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(X0,c_Int_Onumber__class_Onumber__of(sF2,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f6814,f1036]) ).
fof(f6819,plain,
! [X0] : c_HOL_Oplus__class_Oplus(X0,X0,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(X0,sF3,tc_RealDef_Oreal),
inference(forward_demodulation,[],[f6817,f1038]) ).
fof(f7275,definition,
( spl8_103
<=> c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = sF3 ),
introduced(definition,[new_symbols(definition,[spl8_103])],[avatar_definition]) ).
fof(f7276,plain,
( c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) != sF3
| spl8_103 ),
inference(avatar_component_clause,[],[f7275]) ).
fof(f7277,plain,
( c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = sF3
| ~ spl8_103 ),
inference(avatar_component_clause,[],[f7275]) ).
fof(f8686,plain,
( c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) != sF4
| ~ class_Ring__and__Field_Oring__no__zero__divisors(tc_RealDef_Oreal)
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_Transcendental_Opi
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = sF3 ),
inference(superposition,[],[f76,f1040]) ).
fof(f8688,plain,
( c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) != sF4
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_Transcendental_Opi
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = sF3 ),
inference(forward_subsumption_resolution,[],[f8686,f959]) ).
fof(f8691,plain,
( c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) != sF4
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = sF3 ),
inference(forward_subsumption_resolution,[],[f8688,f152]) ).
fof(f8697,plain,
( c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) != sF4
| spl8_103 ),
inference(forward_subsumption_resolution,[],[f8691,f7276]) ).
fof(f8698,plain,
( ~ spl8_34
| spl8_103 ),
inference(avatar_split_clause,[],[f8697,f7275,f2386]) ).
fof(f9296,plain,
( ! [X0] : ~ c_lessequals(c_RealDef_Oreal(X0,tc_nat),sF4,tc_RealDef_Oreal)
| ~ spl8_33 ),
inference(resolution,[],[f3260,f562]) ).
fof(f9374,plain,
( ! [X0] : c_lessequals(sF4,c_RealDef_Oreal(X0,tc_nat),tc_RealDef_Oreal)
| ~ spl8_33 ),
inference(resolution,[],[f9296,f751]) ).
fof(f9397,plain,
( c_lessequals(sF4,sF6,tc_RealDef_Oreal)
| ~ spl8_33 ),
inference(superposition,[],[f9374,f1044]) ).
fof(f9442,plain,
( sF4 = sF6
| c_HOL_Oord__class_Oless(sF4,sF6,tc_RealDef_Oreal)
| ~ class_Orderings_Olinorder(tc_RealDef_Oreal)
| ~ spl8_33 ),
inference(resolution,[],[f9397,f174]) ).
fof(f9453,plain,
( sF4 = sF6
| c_HOL_Oord__class_Oless(sF4,sF6,tc_RealDef_Oreal)
| ~ spl8_33 ),
inference(forward_subsumption_resolution,[],[f9442,f996]) ).
fof(f9455,definition,
( spl8_133
<=> c_HOL_Oord__class_Oless(sF4,sF6,tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[spl8_133])],[avatar_definition]) ).
fof(f9457,plain,
( c_HOL_Oord__class_Oless(sF4,sF6,tc_RealDef_Oreal)
| ~ spl8_133 ),
inference(avatar_component_clause,[],[f9455]) ).
fof(f9459,definition,
( spl8_134
<=> sF4 = sF6 ),
introduced(definition,[new_symbols(definition,[spl8_134])],[avatar_definition]) ).
fof(f9464,plain,
( spl8_133
| spl8_134
| ~ spl8_33 ),
inference(avatar_split_clause,[],[f9453,f2382,f9459,f9455]) ).
fof(f9546,plain,
( ~ c_lessequals(sF6,sF4,tc_RealDef_Oreal)
| ~ class_Orderings_Opreorder(tc_RealDef_Oreal)
| ~ spl8_133 ),
inference(resolution,[],[f9457,f164]) ).
fof(f9706,plain,
( c_lessequals(c_Transcendental_Opi,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_lessequals(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),tc_RealDef_Oreal) ),
inference(resolution,[],[f258,f623]) ).
fof(f9710,plain,
c_lessequals(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),tc_RealDef_Oreal),
inference(forward_subsumption_resolution,[],[f9706,f1252]) ).
fof(f9711,plain,
c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF1),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f9710,f1034]) ).
fof(f9712,plain,
c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(sF2,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f9711,f1036]) ).
fof(f9713,plain,
c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF3,tc_RealDef_Oreal),
inference(forward_demodulation,[],[f9712,f1038]) ).
fof(f9860,plain,
( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF4,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),sF3,tc_RealDef_Oreal) ),
inference(superposition,[],[f558,f1040]) ).
fof(f9862,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),sF3,tc_RealDef_Oreal)
| ~ spl8_33 ),
inference(forward_subsumption_resolution,[],[f9860,f2478]) ).
fof(f9879,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF3,tc_RealDef_Oreal)
| ~ spl8_33 ),
inference(forward_subsumption_resolution,[],[f9862,f564]) ).
fof(f9885,plain,
( ~ class_Orderings_Olinorder(tc_RealDef_Oreal)
| c_lessequals(sF3,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ spl8_33 ),
inference(resolution,[],[f9879,f163]) ).
fof(f9886,plain,
( c_lessequals(sF3,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ spl8_33 ),
inference(forward_subsumption_resolution,[],[f9885,f996]) ).
fof(f9955,plain,
( c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ouminus__class_Ouminus(sF3,tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ class_OrderedGroup_Opordered__ab__group__add(tc_RealDef_Oreal)
| ~ spl8_33 ),
inference(resolution,[],[f9886,f668]) ).
fof(f9964,plain,
( c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = sF3
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF3,tc_RealDef_Oreal)
| ~ class_Orderings_Oorder(tc_RealDef_Oreal)
| ~ spl8_33 ),
inference(resolution,[],[f9886,f440]) ).
fof(f9969,plain,
( ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF3,tc_RealDef_Oreal)
| ~ class_Orderings_Oorder(tc_RealDef_Oreal)
| ~ spl8_33
| spl8_103 ),
inference(forward_subsumption_resolution,[],[f9964,f7276]) ).
fof(f9972,plain,
( c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ouminus__class_Ouminus(sF3,tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ spl8_33 ),
inference(forward_subsumption_resolution,[],[f9955,f962]) ).
fof(f9973,plain,
( ~ class_Orderings_Oorder(tc_RealDef_Oreal)
| ~ spl8_33
| spl8_103 ),
inference(forward_subsumption_resolution,[],[f9969,f9713]) ).
fof(f9977,plain,
( $false
| ~ spl8_33
| spl8_103 ),
inference(forward_subsumption_resolution,[],[f9973,f997]) ).
fof(f9978,plain,
( ~ spl8_33
| spl8_103 ),
inference(avatar_contradiction_clause,[],[f9977]) ).
fof(f10101,plain,
( ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF4,tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF6,tc_RealDef_Oreal)
| ~ spl8_5 ),
inference(resolution,[],[f714,f1518]) ).
fof(f10825,plain,
( c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_HOL_Ouminus__class_Ouminus(sF3,tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Ouminus__class_Ouminus(sF3,tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ class_Orderings_Oorder(tc_RealDef_Oreal)
| ~ spl8_33 ),
inference(resolution,[],[f9972,f440]) ).
fof(f10830,plain,
( c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_HOL_Ouminus__class_Ouminus(sF3,tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Ouminus__class_Ouminus(sF3,tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ spl8_33 ),
inference(forward_subsumption_resolution,[],[f10825,f997]) ).
fof(f10842,plain,
( sF3 = c_HOL_Ouminus__class_Ouminus(sF3,tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Ouminus__class_Ouminus(sF3,tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ spl8_33
| ~ spl8_103 ),
inference(forward_demodulation,[],[f10830,f7277]) ).
fof(f10851,plain,
( ~ c_lessequals(c_HOL_Ouminus__class_Ouminus(sF3,tc_RealDef_Oreal),sF3,tc_RealDef_Oreal)
| sF3 = c_HOL_Ouminus__class_Ouminus(sF3,tc_RealDef_Oreal)
| ~ spl8_33
| ~ spl8_103 ),
inference(forward_demodulation,[],[f10842,f7277]) ).
fof(f10856,definition,
( spl8_143
<=> sF3 = c_HOL_Ouminus__class_Ouminus(sF3,tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[spl8_143])],[avatar_definition]) ).
fof(f10858,plain,
( sF3 = c_HOL_Ouminus__class_Ouminus(sF3,tc_RealDef_Oreal)
| ~ spl8_143 ),
inference(avatar_component_clause,[],[f10856]) ).
fof(f10865,definition,
( spl8_145
<=> c_lessequals(c_HOL_Ouminus__class_Ouminus(sF3,tc_RealDef_Oreal),sF3,tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[spl8_145])],[avatar_definition]) ).
fof(f10867,plain,
( ~ c_lessequals(c_HOL_Ouminus__class_Ouminus(sF3,tc_RealDef_Oreal),sF3,tc_RealDef_Oreal)
| spl8_145 ),
inference(avatar_component_clause,[],[f10865]) ).
fof(f10871,plain,
( spl8_143
| ~ spl8_145
| ~ spl8_33
| ~ spl8_103 ),
inference(avatar_split_clause,[],[f10851,f7275,f2382,f10865,f10856]) ).
fof(f10892,plain,
( ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF4,tc_RealDef_Oreal)
| spl8_76 ),
inference(forward_subsumption_resolution,[],[f5372,f962]) ).
fof(f10893,plain,
( ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF4,tc_RealDef_Oreal)
| ~ spl8_5 ),
inference(forward_subsumption_resolution,[],[f10101,f1111]) ).
fof(f10901,plain,
( ~ c_lessequals(sF6,sF4,tc_RealDef_Oreal)
| ~ spl8_133 ),
inference(forward_subsumption_resolution,[],[f9546,f995]) ).
fof(f10935,plain,
( ~ c_lessequals(sF3,sF4,tc_RealDef_Oreal)
| spl8_76
| ~ spl8_103 ),
inference(forward_demodulation,[],[f10892,f7277]) ).
fof(f10936,plain,
( ~ c_lessequals(sF3,sF4,tc_RealDef_Oreal)
| ~ spl8_5
| ~ spl8_103 ),
inference(forward_demodulation,[],[f10893,f7277]) ).
fof(f10990,definition,
( spl8_153
<=> c_HOL_Oord__class_Oless(sF3,sF5,tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[spl8_153])],[avatar_definition]) ).
fof(f10991,plain,
( ~ c_HOL_Oord__class_Oless(sF3,sF5,tc_RealDef_Oreal)
| spl8_153 ),
inference(avatar_component_clause,[],[f10990]) ).
fof(f10992,plain,
( c_HOL_Oord__class_Oless(sF3,sF5,tc_RealDef_Oreal)
| ~ spl8_153 ),
inference(avatar_component_clause,[],[f10990]) ).
fof(f11008,plain,
( sF3 = sF4
| ~ spl8_34
| ~ spl8_103 ),
inference(forward_demodulation,[],[f2388,f7277]) ).
fof(f11017,plain,
( ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF3,tc_RealDef_Oreal)
| ~ spl8_34
| spl8_35
| ~ spl8_103 ),
inference(forward_demodulation,[],[f2393,f11008]) ).
fof(f11021,plain,
( ~ c_lessequals(sF3,sF3,tc_RealDef_Oreal)
| ~ spl8_5
| ~ spl8_34
| ~ spl8_103 ),
inference(forward_demodulation,[],[f10936,f11008]) ).
fof(f11022,plain,
( $false
| ~ spl8_34
| spl8_35
| ~ spl8_103 ),
inference(forward_subsumption_resolution,[],[f11017,f9713]) ).
fof(f11023,plain,
( ~ spl8_34
| spl8_35
| ~ spl8_103 ),
inference(avatar_contradiction_clause,[],[f11022]) ).
fof(f11030,plain,
( $false
| ~ spl8_5
| ~ spl8_34
| ~ spl8_103 ),
inference(forward_subsumption_resolution,[],[f11021,f735]) ).
fof(f11031,plain,
( ~ spl8_5
| ~ spl8_34
| ~ spl8_103 ),
inference(avatar_contradiction_clause,[],[f11030]) ).
fof(f11033,plain,
( sF3 = c_HOL_Oinverse__class_Odivide(sF4,sF6,tc_RealDef_Oreal)
| ~ spl8_6
| ~ spl8_103 ),
inference(forward_demodulation,[],[f1448,f7277]) ).
fof(f11041,plain,
( c_lessequals(c_HOL_Ouminus__class_Ouminus(sF4,tc_RealDef_Oreal),sF3,tc_RealDef_Oreal)
| ~ spl8_76
| ~ spl8_103 ),
inference(forward_demodulation,[],[f5196,f7277]) ).
fof(f11320,plain,
( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF3,tc_RealDef_Oreal)
| ~ spl8_51 ),
inference(superposition,[],[f1096,f3021]) ).
fof(f11430,plain,
( c_HOL_Oord__class_Oless(sF3,sF3,tc_RealDef_Oreal)
| ~ spl8_51
| ~ spl8_103 ),
inference(forward_demodulation,[],[f11320,f7277]) ).
fof(f11442,plain,
( $false
| ~ spl8_51
| ~ spl8_103 ),
inference(forward_subsumption_resolution,[],[f11430,f809]) ).
fof(f11443,plain,
( ~ spl8_51
| ~ spl8_103 ),
inference(avatar_contradiction_clause,[],[f11442]) ).
fof(f12533,plain,
( ~ class_OrderedGroup_Oordered__ab__group__add(tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF3,tc_RealDef_Oreal)
| spl8_145 ),
inference(resolution,[],[f10867,f684]) ).
fof(f12540,plain,
( ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF3,tc_RealDef_Oreal)
| spl8_145 ),
inference(forward_subsumption_resolution,[],[f12533,f964]) ).
fof(f12544,plain,
( $false
| spl8_145 ),
inference(forward_subsumption_resolution,[],[f12540,f9713]) ).
fof(f12545,plain,
spl8_145,
inference(avatar_contradiction_clause,[],[f12544]) ).
fof(f13039,plain,
( c_lessequals(c_HOL_Ouminus__class_Ouminus(sF3,tc_RealDef_Oreal),c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(sF4,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ class_OrderedGroup_Opordered__ab__group__add(tc_RealDef_Oreal)
| ~ spl8_76
| ~ spl8_103 ),
inference(resolution,[],[f11041,f389]) ).
fof(f13046,plain,
( c_lessequals(c_HOL_Ouminus__class_Ouminus(sF3,tc_RealDef_Oreal),c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(sF4,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ spl8_76
| ~ spl8_103 ),
inference(forward_subsumption_resolution,[],[f13039,f962]) ).
fof(f13066,plain,
( c_lessequals(c_HOL_Ouminus__class_Ouminus(sF3,tc_RealDef_Oreal),sF4,tc_RealDef_Oreal)
| ~ spl8_76
| ~ spl8_103 ),
inference(forward_demodulation,[],[f13046,f1135]) ).
fof(f13071,plain,
( c_lessequals(sF3,sF4,tc_RealDef_Oreal)
| ~ spl8_76
| ~ spl8_103
| ~ spl8_143 ),
inference(forward_demodulation,[],[f13066,f10858]) ).
fof(f14180,plain,
( sF5 = c_HOL_Otimes__class_Otimes(sF0,sF3,tc_RealDef_Oreal)
| ~ spl8_34
| ~ spl8_103 ),
inference(superposition,[],[f1042,f11008]) ).
fof(f14255,plain,
( sF3 = c_HOL_Oinverse__class_Odivide(sF3,sF6,tc_RealDef_Oreal)
| ~ spl8_6
| ~ spl8_34
| ~ spl8_103 ),
inference(superposition,[],[f11033,f11008]) ).
fof(f14297,plain,
( sF5 = c_HOL_Oplus__class_Oplus(sF0,sF0,tc_RealDef_Oreal)
| ~ spl8_34
| ~ spl8_103 ),
inference(forward_demodulation,[],[f14180,f6819]) ).
fof(f14382,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF5,tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF4,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF0,tc_RealDef_Oreal)
| ~ class_Ring__and__Field_Oordered__semiring__strict(tc_RealDef_Oreal) ),
inference(superposition,[],[f318,f1042]) ).
fof(f14396,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF5,tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF4,tc_RealDef_Oreal)
| ~ class_Ring__and__Field_Oordered__semiring__strict(tc_RealDef_Oreal)
| ~ spl8_9 ),
inference(forward_subsumption_resolution,[],[f14382,f1462]) ).
fof(f14399,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF5,tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF4,tc_RealDef_Oreal)
| ~ spl8_9 ),
inference(forward_subsumption_resolution,[],[f14396,f956]) ).
fof(f14402,plain,
( ~ c_HOL_Oord__class_Oless(sF3,sF5,tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF4,tc_RealDef_Oreal)
| ~ spl8_9
| ~ spl8_103 ),
inference(forward_demodulation,[],[f14399,f7277]) ).
fof(f14405,plain,
( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF4,tc_RealDef_Oreal)
| ~ spl8_9
| ~ spl8_103
| ~ spl8_153 ),
inference(forward_subsumption_resolution,[],[f14402,f10992]) ).
fof(f14408,plain,
( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF3,tc_RealDef_Oreal)
| ~ spl8_9
| ~ spl8_34
| ~ spl8_103
| ~ spl8_153 ),
inference(forward_demodulation,[],[f14405,f11008]) ).
fof(f14409,plain,
( c_HOL_Oord__class_Oless(sF3,sF3,tc_RealDef_Oreal)
| ~ spl8_9
| ~ spl8_34
| ~ spl8_103
| ~ spl8_153 ),
inference(forward_demodulation,[],[f14408,f7277]) ).
fof(f14410,plain,
( $false
| ~ spl8_9
| ~ spl8_34
| ~ spl8_103
| ~ spl8_153 ),
inference(forward_subsumption_resolution,[],[f14409,f809]) ).
fof(f14411,plain,
( ~ spl8_9
| ~ spl8_34
| ~ spl8_103
| ~ spl8_153 ),
inference(avatar_contradiction_clause,[],[f14410]) ).
fof(f14412,plain,
( ~ c_HOL_Oord__class_Oless(sF3,sF0,tc_RealDef_Oreal)
| spl8_9
| ~ spl8_103 ),
inference(forward_demodulation,[],[f1461,f7277]) ).
fof(f14706,plain,
( ~ c_HOL_Oord__class_Oless(sF5,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(sF0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ class_OrderedGroup_Olordered__ab__group__add(tc_RealDef_Oreal)
| ~ spl8_34
| ~ spl8_103 ),
inference(superposition,[],[f425,f14297]) ).
fof(f14708,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF5,tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF0,tc_RealDef_Oreal)
| ~ class_OrderedGroup_Olordered__ab__group__add(tc_RealDef_Oreal)
| ~ spl8_34
| ~ spl8_103 ),
inference(superposition,[],[f494,f14297]) ).
fof(f14805,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF5,tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF0,tc_RealDef_Oreal)
| ~ spl8_34
| ~ spl8_103 ),
inference(forward_subsumption_resolution,[],[f14708,f963]) ).
fof(f14806,plain,
( ~ c_HOL_Oord__class_Oless(sF5,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ class_OrderedGroup_Olordered__ab__group__add(tc_RealDef_Oreal)
| ~ spl8_34
| ~ spl8_103 ),
inference(forward_subsumption_resolution,[],[f14706,f1112]) ).
fof(f14819,plain,
( ~ c_HOL_Oord__class_Oless(sF3,sF5,tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF0,tc_RealDef_Oreal)
| ~ spl8_34
| ~ spl8_103 ),
inference(forward_demodulation,[],[f14805,f7277]) ).
fof(f14820,plain,
( ~ c_HOL_Oord__class_Oless(sF5,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ spl8_34
| ~ spl8_103 ),
inference(forward_subsumption_resolution,[],[f14806,f963]) ).
fof(f14827,definition,
( spl8_179
<=> c_HOL_Oord__class_Oless(sF5,sF3,tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[spl8_179])],[avatar_definition]) ).
fof(f14828,plain,
( ~ c_HOL_Oord__class_Oless(sF5,sF3,tc_RealDef_Oreal)
| spl8_179 ),
inference(avatar_component_clause,[],[f14827]) ).
fof(f14847,plain,
( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF0,tc_RealDef_Oreal)
| ~ spl8_34
| ~ spl8_103
| ~ spl8_153 ),
inference(forward_subsumption_resolution,[],[f14819,f10992]) ).
fof(f14848,plain,
( ~ c_HOL_Oord__class_Oless(sF5,sF3,tc_RealDef_Oreal)
| ~ spl8_34
| ~ spl8_103 ),
inference(forward_demodulation,[],[f14820,f7277]) ).
fof(f14851,plain,
( c_HOL_Oord__class_Oless(sF3,sF0,tc_RealDef_Oreal)
| ~ spl8_34
| ~ spl8_103
| ~ spl8_153 ),
inference(forward_demodulation,[],[f14847,f7277]) ).
fof(f14852,plain,
( ~ spl8_179
| ~ spl8_34
| ~ spl8_103 ),
inference(avatar_split_clause,[],[f14848,f7275,f2386,f14827]) ).
fof(f14853,plain,
( $false
| spl8_9
| ~ spl8_34
| ~ spl8_103
| ~ spl8_153 ),
inference(forward_subsumption_resolution,[],[f14851,f14412]) ).
fof(f14854,plain,
( spl8_9
| ~ spl8_34
| ~ spl8_103
| ~ spl8_153 ),
inference(avatar_contradiction_clause,[],[f14853]) ).
fof(f14886,plain,
( c_HOL_Oord__class_Oless(sF3,c_HOL_Ozero__class_Ozero(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),sF6,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(sF4,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ spl8_6
| ~ spl8_103 ),
inference(superposition,[],[f371,f11033]) ).
fof(f14892,plain,
( c_HOL_Oord__class_Oless(sF3,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),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(sF4,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ spl8_6
| ~ spl8_103 ),
inference(forward_subsumption_resolution,[],[f14886,f977]) ).
fof(f14897,plain,
( c_HOL_Oord__class_Oless(sF3,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(sF4,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ spl8_6
| ~ spl8_7
| ~ spl8_103 ),
inference(forward_subsumption_resolution,[],[f14892,f1453]) ).
fof(f14902,plain,
( c_HOL_Oord__class_Oless(sF3,sF3,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(sF4,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ spl8_6
| ~ spl8_7
| ~ spl8_103 ),
inference(forward_demodulation,[],[f14897,f7277]) ).
fof(f14907,plain,
( ~ c_HOL_Oord__class_Oless(sF4,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ spl8_6
| ~ spl8_7
| ~ spl8_103 ),
inference(forward_subsumption_resolution,[],[f14902,f809]) ).
fof(f14911,plain,
( ~ c_HOL_Oord__class_Oless(sF4,sF3,tc_RealDef_Oreal)
| ~ spl8_6
| ~ spl8_7
| ~ spl8_103 ),
inference(forward_demodulation,[],[f14907,f7277]) ).
fof(f14916,plain,
( c_HOL_Oord__class_Oless(sF3,sF5,tc_RealDef_Oreal)
| ~ class_Ring__and__Field_Oordered__idom(tc_RealDef_Oreal)
| sF3 = sF5
| spl8_179 ),
inference(resolution,[],[f14828,f847]) ).
fof(f14919,plain,
( ~ class_Ring__and__Field_Oordered__idom(tc_RealDef_Oreal)
| sF3 = sF5
| spl8_153
| spl8_179 ),
inference(forward_subsumption_resolution,[],[f14916,f10991]) ).
fof(f14923,plain,
( sF3 = sF5
| spl8_153
| spl8_179 ),
inference(forward_subsumption_resolution,[],[f14919,f982]) ).
fof(f14944,plain,
( ~ class_Ring__and__Field_Oordered__field(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),sF4,tc_RealDef_Oreal) ),
inference(resolution,[],[f376,f1105]) ).
fof(f14963,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),sF4,tc_RealDef_Oreal) ),
inference(forward_subsumption_resolution,[],[f14944,f977]) ).
fof(f14970,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF4,tc_RealDef_Oreal)
| ~ spl8_7 ),
inference(forward_subsumption_resolution,[],[f14963,f1453]) ).
fof(f14987,plain,
( sF7 = c_HOL_Oinverse__class_Odivide(sF3,sF6,tc_RealDef_Oreal)
| spl8_153
| spl8_179 ),
inference(superposition,[],[f1046,f14923]) ).
fof(f14988,plain,
( sF3 = sF7
| ~ spl8_6
| ~ spl8_34
| ~ spl8_103
| spl8_153
| spl8_179 ),
inference(forward_demodulation,[],[f14987,f14255]) ).
fof(f14989,plain,
( $false
| ~ spl8_6
| ~ spl8_34
| spl8_51
| ~ spl8_103
| spl8_153
| spl8_179 ),
inference(forward_subsumption_resolution,[],[f14988,f3020]) ).
fof(f14990,plain,
( ~ spl8_6
| ~ spl8_34
| spl8_51
| ~ spl8_103
| spl8_153
| spl8_179 ),
inference(avatar_contradiction_clause,[],[f14989]) ).
fof(f15067,plain,
( c_HOL_Oord__class_Oless(sF4,sF3,tc_RealDef_Oreal)
| ~ spl8_33
| ~ spl8_103 ),
inference(forward_demodulation,[],[f2384,f7277]) ).
fof(f15076,plain,
( ~ c_lessequals(sF3,sF4,tc_RealDef_Oreal)
| spl8_35
| ~ spl8_103 ),
inference(forward_demodulation,[],[f2393,f7277]) ).
fof(f15246,plain,
( $false
| ~ spl8_6
| ~ spl8_7
| ~ spl8_33
| ~ spl8_103 ),
inference(forward_subsumption_resolution,[],[f15067,f14911]) ).
fof(f15247,plain,
( ~ spl8_6
| ~ spl8_7
| ~ spl8_33
| ~ spl8_103 ),
inference(avatar_contradiction_clause,[],[f15246]) ).
fof(f15254,plain,
( $false
| spl8_35
| ~ spl8_76
| ~ spl8_103
| ~ spl8_143 ),
inference(forward_subsumption_resolution,[],[f15076,f13071]) ).
fof(f15255,plain,
( spl8_35
| ~ spl8_76
| ~ spl8_103
| ~ spl8_143 ),
inference(avatar_contradiction_clause,[],[f15254]) ).
fof(f15950,plain,
( c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF4,tc_RealDef_Oreal)
| ~ class_Ring__and__Field_Opordered__ring(tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF3,tc_RealDef_Oreal) ),
inference(superposition,[],[f485,f1040]) ).
fof(f15958,plain,
( c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF4,tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF3,tc_RealDef_Oreal) ),
inference(forward_subsumption_resolution,[],[f15950,f976]) ).
fof(f15967,plain,
( c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF4,tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF3,tc_RealDef_Oreal) ),
inference(forward_subsumption_resolution,[],[f15958,f731]) ).
fof(f15976,plain,
c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF4,tc_RealDef_Oreal),
inference(forward_subsumption_resolution,[],[f15967,f9713]) ).
fof(f15985,plain,
( c_lessequals(sF3,sF4,tc_RealDef_Oreal)
| ~ spl8_103 ),
inference(forward_demodulation,[],[f15976,f7277]) ).
fof(f15993,plain,
( $false
| spl8_76
| ~ spl8_103 ),
inference(forward_subsumption_resolution,[],[f15985,f10935]) ).
fof(f15994,plain,
( spl8_76
| ~ spl8_103 ),
inference(avatar_contradiction_clause,[],[f15993]) ).
fof(f17664,plain,
( sF4 != sF6
| ~ spl8_8
| spl8_34 ),
inference(forward_demodulation,[],[f2387,f1457]) ).
fof(f17674,plain,
( c_lessequals(sF6,sF4,tc_RealDef_Oreal)
| ~ spl8_8 ),
inference(forward_demodulation,[],[f15976,f1457]) ).
fof(f17719,plain,
( ~ spl8_134
| ~ spl8_8
| spl8_34 ),
inference(avatar_split_clause,[],[f17664,f2386,f1455,f9459]) ).
fof(f17721,plain,
( $false
| ~ spl8_8
| ~ spl8_133 ),
inference(forward_subsumption_resolution,[],[f17674,f10901]) ).
fof(f17722,plain,
( ~ spl8_8
| ~ spl8_133 ),
inference(avatar_contradiction_clause,[],[f17721]) ).
fof(f18128,plain,
( c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF5,tc_RealDef_Oreal)
| ~ class_Ring__and__Field_Opordered__cancel__semiring(tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF4,tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF0,tc_RealDef_Oreal) ),
inference(superposition,[],[f491,f1042]) ).
fof(f18137,plain,
( c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF5,tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF4,tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF0,tc_RealDef_Oreal) ),
inference(forward_subsumption_resolution,[],[f18128,f954]) ).
fof(f18139,plain,
( c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF5,tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF0,tc_RealDef_Oreal)
| ~ spl8_35 ),
inference(forward_subsumption_resolution,[],[f18137,f2392]) ).
fof(f18141,plain,
( c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF5,tc_RealDef_Oreal)
| ~ spl8_35 ),
inference(forward_subsumption_resolution,[],[f18139,f1110]) ).
fof(f18781,plain,
( ~ class_Orderings_Olinorder(tc_RealDef_Oreal)
| c_lessequals(sF4,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ spl8_7 ),
inference(resolution,[],[f14970,f163]) ).
fof(f18782,plain,
( c_lessequals(sF4,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ spl8_7 ),
inference(forward_subsumption_resolution,[],[f18781,f996]) ).
fof(f18783,plain,
( $false
| ~ spl8_7
| spl8_29 ),
inference(forward_subsumption_resolution,[],[f18782,f2331]) ).
fof(f18784,plain,
( ~ spl8_7
| spl8_29 ),
inference(avatar_contradiction_clause,[],[f18783]) ).
fof(f23851,plain,
( c_lessequals(sF7,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ class_Ring__and__Field_Odivision__by__zero(tc_RealDef_Oreal)
| ~ class_Ring__and__Field_Oordered__field(tc_RealDef_Oreal)
| ~ c_lessequals(sF6,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF5,tc_RealDef_Oreal) ),
inference(superposition,[],[f395,f1046]) ).
fof(f23853,plain,
( ~ class_Ring__and__Field_Odivision__by__zero(tc_RealDef_Oreal)
| ~ class_Ring__and__Field_Oordered__field(tc_RealDef_Oreal)
| ~ c_lessequals(sF6,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF5,tc_RealDef_Oreal) ),
inference(forward_subsumption_resolution,[],[f23851,f1250]) ).
fof(f23860,plain,
( ~ class_Ring__and__Field_Oordered__field(tc_RealDef_Oreal)
| ~ c_lessequals(sF6,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF5,tc_RealDef_Oreal) ),
inference(forward_subsumption_resolution,[],[f23853,f969]) ).
fof(f23867,plain,
( ~ c_lessequals(sF6,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF5,tc_RealDef_Oreal) ),
inference(forward_subsumption_resolution,[],[f23860,f977]) ).
fof(f23874,plain,
( ~ c_lessequals(sF6,sF6,tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF5,tc_RealDef_Oreal)
| ~ spl8_8 ),
inference(forward_demodulation,[],[f23867,f1457]) ).
fof(f23881,plain,
( ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF5,tc_RealDef_Oreal)
| ~ spl8_8 ),
inference(forward_subsumption_resolution,[],[f23874,f735]) ).
fof(f23911,plain,
( c_lessequals(sF6,sF5,tc_RealDef_Oreal)
| ~ spl8_8
| ~ spl8_35 ),
inference(forward_demodulation,[],[f18141,f1457]) ).
fof(f23926,plain,
( ~ c_lessequals(sF6,sF5,tc_RealDef_Oreal)
| ~ spl8_8 ),
inference(forward_demodulation,[],[f23881,f1457]) ).
fof(f23948,plain,
( $false
| ~ spl8_8
| ~ spl8_35 ),
inference(forward_subsumption_resolution,[],[f23926,f23911]) ).
fof(f23949,plain,
( ~ spl8_8
| ~ spl8_35 ),
inference(avatar_contradiction_clause,[],[f23948]) ).
cnf(s3,plain,
( spl8_5
| spl8_6 ),
inference(sat_conversion,[],[f1449]) ).
cnf(s4,plain,
( spl8_7
| spl8_8 ),
inference(sat_conversion,[],[f1458]) ).
cnf(s27,plain,
( ~ spl8_29
| spl8_33
| spl8_34 ),
inference(sat_conversion,[],[f2396]) ).
cnf(s28,plain,
( ~ spl8_29
| spl8_34
| ~ spl8_35 ),
inference(sat_conversion,[],[f2397]) ).
cnf(s30,plain,
( spl8_29
| spl8_35 ),
inference(sat_conversion,[],[f2423]) ).
cnf(s167,plain,
( ~ spl8_34
| spl8_103 ),
inference(sat_conversion,[],[f8698]) ).
cnf(s190,plain,
( ~ spl8_33
| spl8_133
| spl8_134 ),
inference(sat_conversion,[],[f9464]) ).
cnf(s197,plain,
( ~ spl8_33
| spl8_103 ),
inference(sat_conversion,[],[f9978]) ).
cnf(s206,plain,
( ~ spl8_33
| ~ spl8_103
| spl8_143
| ~ spl8_145 ),
inference(sat_conversion,[],[f10871]) ).
cnf(s235,plain,
( ~ spl8_34
| spl8_35
| ~ spl8_103 ),
inference(sat_conversion,[],[f11023]) ).
cnf(s239,plain,
( ~ spl8_5
| ~ spl8_34
| ~ spl8_103 ),
inference(sat_conversion,[],[f11031]) ).
cnf(s277,plain,
( ~ spl8_51
| ~ spl8_103 ),
inference(sat_conversion,[],[f11443]) ).
cnf(s305,plain,
spl8_145,
inference(sat_conversion,[],[f12545]) ).
cnf(s341,plain,
( ~ spl8_9
| ~ spl8_34
| ~ spl8_103
| ~ spl8_153 ),
inference(sat_conversion,[],[f14411]) ).
cnf(s351,plain,
( ~ spl8_34
| ~ spl8_103
| ~ spl8_179 ),
inference(sat_conversion,[],[f14852]) ).
cnf(s353,plain,
( spl8_9
| ~ spl8_34
| ~ spl8_103
| ~ spl8_153 ),
inference(sat_conversion,[],[f14854]) ).
cnf(s354,plain,
( ~ spl8_6
| ~ spl8_34
| spl8_51
| ~ spl8_103
| spl8_153
| spl8_179 ),
inference(sat_conversion,[],[f14990]) ).
cnf(s410,plain,
( ~ spl8_6
| ~ spl8_7
| ~ spl8_33
| ~ spl8_103 ),
inference(sat_conversion,[],[f15247]) ).
cnf(s414,plain,
( spl8_35
| ~ spl8_76
| ~ spl8_103
| ~ spl8_143 ),
inference(sat_conversion,[],[f15255]) ).
cnf(s429,plain,
( spl8_76
| ~ spl8_103 ),
inference(sat_conversion,[],[f15994]) ).
cnf(s494,plain,
( ~ spl8_8
| spl8_34
| ~ spl8_134 ),
inference(sat_conversion,[],[f17719]) ).
cnf(s495,plain,
( ~ spl8_8
| ~ spl8_133 ),
inference(sat_conversion,[],[f17722]) ).
cnf(s543,plain,
( ~ spl8_7
| spl8_29 ),
inference(sat_conversion,[],[f18784]) ).
cnf(s594,plain,
( ~ spl8_8
| ~ spl8_35 ),
inference(sat_conversion,[],[f23949]) ).
cnf(s606,plain,
( ~ spl8_33
| ~ spl8_103
| spl8_143 ),
inference(rat,[],[s206,s305]) ).
cnf(s608,plain,
( ~ spl8_34
| spl8_35 ),
inference(rat,[],[s167,s235]) ).
cnf(s609,plain,
~ spl8_8,
inference(rat,[],[s190,s27,s494,s608,s30,s495,s594]) ).
cnf(s611,plain,
spl8_7,
inference(rat,[],[s4,s609]) ).
cnf(s612,plain,
spl8_29,
inference(rat,[],[s543,s611]) ).
cnf(s615,plain,
( ~ spl8_153
| ~ spl8_34
| ~ spl8_103 ),
inference(rat,[],[s341,s353]) ).
cnf(s616,plain,
( spl8_51
| spl8_179
| ~ spl8_6
| ~ spl8_34
| ~ spl8_103 ),
inference(rat,[],[s615,s354]) ).
cnf(s617,plain,
( ~ spl8_34
| ~ spl8_6 ),
inference(rat,[],[s616,s277,s351,s167]) ).
cnf(s618,plain,
~ spl8_6,
inference(rat,[],[s410,s197,s27,s617,s611,s612]) ).
cnf(s619,plain,
spl8_5,
inference(rat,[],[s3,s618]) ).
cnf(s620,plain,
~ spl8_34,
inference(rat,[],[s239,s167,s619]) ).
cnf(s622,plain,
~ spl8_35,
inference(rat,[],[s28,s612,s620]) ).
cnf(s623,plain,
spl8_33,
inference(rat,[],[s27,s612,s620]) ).
cnf(s625,plain,
spl8_103,
inference(rat,[],[s197,s623]) ).
cnf(s628,plain,
spl8_143,
inference(rat,[],[s606,s625,s623]) ).
cnf(s629,plain,
spl8_76,
inference(rat,[],[s429,s625]) ).
cnf(s635,plain,
$false,
inference(rat,[],[s414,s628,s622,s625,s629]) ).
fof(f23955,plain,
$false,
inference(avatar_sat_refutation,[],[s635]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV620-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.18 % Computer : n009.cluster.edu
% 0.09/0.18 % Model : x86_64 x86_64
% 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.18 % Memory : 8046.5625MB
% 0.09/0.18 % OS : Linux 6.8.0-71-generic
% 0.09/0.18 % CPULimit : 300
% 0.09/0.18 % WCLimit : 300
% 0.09/0.18 % DateTime : Mon Sep 28 12:04:00 UTC 2026
% 0.09/0.18 % CPUTime :
% 0.09/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.21 Running first-order model finding
% 0.09/0.21 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 6.75/1.27 % (2991060)Will run a generic schedule for satisfiability detection.
% 6.75/1.27 % (2991070)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2158248315:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 6.75/1.27 % (2991066)% WARNING: option uhcvi not known.
% 6.75/1.27 % (2991065)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3643667942_2999 on theBenchmark for (2999ds/0Mi)
% 6.75/1.27 % (2991066)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2858395685:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 6.75/1.27 % (2991067)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2482525606:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 6.75/1.27 % (2991068)dis+10_1_sil=32000:sp=arity:random_seed=588144160:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 6.75/1.27 % (2991069)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=307948294:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 6.75/1.27 % (2991071)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1378022915:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 6.75/1.27 % (2991070)Instruction limit reached!
% 6.75/1.27 % (2991070)------------------------------
% 6.75/1.27 % (2991070)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.75/1.27 % (2991070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.75/1.27 % (2991070)CaDiCaL version: 2.1.3
% 6.75/1.27 % (2991070)Termination reason: Instruction limit
% 6.75/1.27 % (2991070)Termination phase: Saturation
% 6.75/1.27 % (2991070)Time elapsed: 0.043 s
% 6.75/1.27 % (2991070)Peak memory usage: 13 MB
% 6.75/1.27 % (2991070)Instructions burned: 134 (million)
% 6.75/1.27 % (2991079)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2217335924:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 6.75/1.27 % (2991068)Instruction limit reached!
% 6.75/1.27 % (2991068)------------------------------
% 6.75/1.27 % (2991068)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.75/1.27 % (2991068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.75/1.27 % (2991068)CaDiCaL version: 2.1.3
% 6.75/1.27 % (2991068)Termination reason: Instruction limit
% 6.75/1.27 % (2991068)Termination phase: Saturation
% 6.75/1.27 % (2991068)Time elapsed: 0.062 s
% 6.75/1.27 % (2991068)Peak memory usage: 13 MB
% 6.75/1.27 % (2991068)Instructions burned: 104 (million)
% 6.75/1.27 % (2991069)Instruction limit reached!
% 6.75/1.27 % (2991069)------------------------------
% 6.75/1.27 % (2991069)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.75/1.27 % (2991069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.75/1.27 % (2991069)CaDiCaL version: 2.1.3
% 6.75/1.27 % (2991069)Termination reason: Instruction limit
% 6.75/1.27 % (2991069)Termination phase: Saturation
% 6.75/1.27 % (2991069)Time elapsed: 0.071 s
% 6.75/1.27 % (2991069)Peak memory usage: 13 MB
% 6.75/1.27 % (2991069)Instructions burned: 116 (million)
% 6.75/1.27 % (2991081)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2186910286:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 6.75/1.27 % (2991082)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=402272691:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 6.75/1.27 % (2991071)Instruction limit reached!
% 6.75/1.27 % (2991071)------------------------------
% 6.75/1.27 % (2991071)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.75/1.27 % (2991071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.75/1.27 % (2991071)CaDiCaL version: 2.1.3
% 6.75/1.27 % (2991071)Termination reason: Instruction limit
% 6.75/1.27 % (2991071)Termination phase: Saturation
% 6.75/1.27 % (2991071)Time elapsed: 0.094 s
% 6.75/1.27 % (2991071)Peak memory usage: 14 MB
% 6.75/1.27 % (2991071)Instructions burned: 159 (million)
% 6.75/1.27 % TRYING [1]
% 6.75/1.27 % TRYING [2]
% 6.75/1.27 % TRYING [1]
% 6.75/1.27 % (2991085)ott-21_1_sil=16000:fs=off:random_seed=1763265629:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 6.75/1.27 % TRYING [2]
% 6.75/1.27 % TRYING [3]
% 6.75/1.27 % (2991081)Instruction limit reached!
% 6.75/1.27 % (2991081)------------------------------
% 6.75/1.27 % (2991081)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.75/1.27 % (2991081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.75/1.27 % (2991081)CaDiCaL version: 2.1.3
% 6.75/1.27 % (2991081)Termination reason: Instruction limit
% 6.75/1.27 % (2991081)Termination phase: Saturation
% 6.75/1.27 % (2991081)Time elapsed: 0.078 s
% 6.75/1.27 % (2991081)Peak memory usage: 14 MB
% 6.75/1.27 % (2991081)Instructions burned: 132 (million)
% 6.75/1.27 % (2991087)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1130640529:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 6.75/1.27 % (2991079)Instruction limit reached!
% 6.75/1.27 % (2991079)------------------------------
% 6.75/1.27 % (2991079)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.75/1.27 % (2991079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.75/1.27 % (2991079)CaDiCaL version: 2.1.3
% 6.75/1.27 % (2991079)Termination reason: Instruction limit
% 6.75/1.27 % (2991079)Termination phase: Finite model building constraint generation
% 6.75/1.27 % (2991079)Time elapsed: 0.145 s
% 6.75/1.27 % (2991079)Peak memory usage: 28 MB
% 6.75/1.27 % (2991079)Instructions burned: 715 (million)
% 6.75/1.27 % TRYING [3]
% 6.75/1.27 % (2991089)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=969049043:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 6.75/1.27 % (2991085)Instruction limit reached!
% 6.75/1.27 % (2991085)------------------------------
% 6.75/1.27 % (2991085)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.75/1.27 % (2991085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.75/1.27 % (2991085)CaDiCaL version: 2.1.3
% 6.75/1.27 % (2991085)Termination reason: Instruction limit
% 6.75/1.27 % (2991085)Termination phase: Saturation
% 6.75/1.27 % (2991085)Time elapsed: 0.089 s
% 6.75/1.27 % (2991085)Peak memory usage: 13 MB
% 6.75/1.27 % (2991085)Instructions burned: 180 (million)
% 6.75/1.27 % (2991091)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1469699326:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 6.75/1.27 % TRYING [1]
% 6.75/1.27 % TRYING [2]
% 6.75/1.27 % (2991089)Instruction limit reached!
% 6.75/1.27 % (2991089)------------------------------
% 6.75/1.27 % (2991089)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.75/1.27 % (2991089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.75/1.27 % (2991089)CaDiCaL version: 2.1.3
% 6.75/1.27 % (2991089)Termination reason: Instruction limit
% 6.75/1.27 % (2991089)Termination phase: Finite model building constraint generation
% 6.75/1.27 % (2991089)Time elapsed: 0.201 s
% 6.75/1.27 % (2991089)Peak memory usage: 28 MB
% 6.75/1.27 % (2991089)Instructions burned: 868 (million)
% 6.75/1.27 % (2991093)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3394230216:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 6.75/1.27 % (2991087)Instruction limit reached!
% 6.75/1.27 % (2991087)------------------------------
% 6.75/1.27 % (2991087)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.75/1.27 % (2991087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.75/1.27 % (2991087)CaDiCaL version: 2.1.3
% 6.75/1.27 % (2991087)Termination reason: Instruction limit
% 6.75/1.27 % (2991087)Termination phase: Saturation
% 6.75/1.27 % (2991087)Time elapsed: 0.295 s
% 6.75/1.27 % (2991087)Peak memory usage: 15 MB
% 6.75/1.27 % (2991087)Instructions burned: 477 (million)
% 6.75/1.27 % (2991082)Instruction limit reached!
% 6.75/1.27 % (2991082)------------------------------
% 6.75/1.27 % (2991082)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.75/1.27 % (2991082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.75/1.27 % (2991082)CaDiCaL version: 2.1.3
% 6.75/1.27 % (2991082)Termination reason: Instruction limit
% 6.75/1.27 % (2991082)Termination phase: Saturation
% 6.75/1.27 % (2991082)Time elapsed: 0.393 s
% 6.75/1.27 % (2991082)Peak memory usage: 17 MB
% 6.75/1.27 % (2991082)Instructions burned: 685 (million)
% 6.75/1.27 % (2991095)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=247485799:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 6.75/1.27 % (2991096)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1416374438:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 6.75/1.27 % (2991093)Instruction limit reached!
% 6.75/1.27 % (2991093)------------------------------
% 6.75/1.27 % (2991093)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.75/1.27 % (2991093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.75/1.27 % (2991093)CaDiCaL version: 2.1.3
% 6.75/1.27 % (2991093)Termination reason: Instruction limit
% 6.75/1.27 % (2991093)Termination phase: Finite model building constraint generation
% 6.75/1.27 % (2991093)Time elapsed: 0.244 s
% 6.75/1.27 % (2991093)Peak memory usage: 96 MB
% 6.75/1.27 % (2991093)Instructions burned: 894 (million)
% 6.75/1.27 % (2991099)fmb+10_1_sil=64000:random_seed=2342268896:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi)
% 6.75/1.27 % TRYING [1]
% 6.75/1.27 % TRYING [2]
% 6.75/1.27 % TRYING [4]
% 6.75/1.27 % TRYING [3]
% 6.75/1.27 % (2991095)Instruction limit reached!
% 6.75/1.27 % (2991095)------------------------------
% 6.75/1.27 % (2991095)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.75/1.27 % (2991095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.75/1.27 % (2991095)CaDiCaL version: 2.1.3
% 6.75/1.27 % (2991095)Termination reason: Instruction limit
% 6.75/1.27 % (2991095)Termination phase: Saturation
% 6.75/1.27 % (2991095)Time elapsed: 0.440 s
% 6.75/1.27 % (2991095)Peak memory usage: 17 MB
% 6.75/1.27 % (2991095)Instructions burned: 692 (million)
% 6.75/1.27 % (2991101)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=4099586976:i=9515:nm=5_2989 on theBenchmark for (2989ds/9515Mi)
% 6.75/1.27 % (2991091) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2991060-2991091"...
% 6.75/1.27 % (2991091)...printing done.
% 6.75/1.27 % (2991091)Refutation found. Thanks to Tanya!
% 6.75/1.27 % SZS status Unsatisfiable for theBenchmark
% 6.75/1.27 % SZS output start Proof for theBenchmark
% See solution above
% 6.75/1.27 % (2991091)------------------------------
% 6.75/1.27 % (2991091)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.75/1.27 % (2991091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.75/1.27 % (2991091)CaDiCaL version: 2.1.3
% 6.75/1.27 % (2991091)Termination reason: Refutation
% 6.75/1.27 % (2991091)Time elapsed: 0.740 s
% 6.75/1.27 % (2991091)Peak memory usage: 20 MB
% 6.75/1.27 % (2991091)Instructions burned: 1161 (million)
% 6.75/1.27 % (2991060)Success in time 1.047 s
% 6.75/1.27 % Vampire exiting
%------------------------------------------------------------------------------