%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWV611-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 : n026.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:07 PM UTC 2026
% Result : Unsatisfiable 6.18s 1.27s
% Output : Refutation 6.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 35
% Syntax : Number of formulae : 116 ( 48 unt; 7 def)
% Number of atoms : 224 ( 28 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 209 ( 101 ~; 101 |; 0 &)
% ( 7 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 18 ( 16 usr; 8 prp; 0-3 aty)
% Number of functors : 13 ( 13 usr; 6 con; 0-3 aty)
% Number of variables : 54 ( 0 sgn 54 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f28,axiom,
! [X0,X1] :
( ~ class_Ring__and__Field_Oring__no__zero__divisors(X0)
| c_HOL_Otimes__class_Otimes(X1,c_HOL_Ozero__class_Ozero(X0),X0) = c_HOL_Ozero__class_Ozero(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_mult__eq__0__iff_2) ).
fof(f29,plain,
! [X0,X1] :
( ~ class_Ring__and__Field_Oring__no__zero__divisors(X0)
| c_HOL_Ozero__class_Ozero(X0) = c_HOL_Otimes__class_Otimes(X1,c_HOL_Ozero__class_Ozero(X0),X0) ),
inference(reorient_equations,[],[f28]) ).
fof(f30,axiom,
! [X0,X1] :
( ~ class_Ring__and__Field_Oring__no__zero__divisors(X0)
| c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(X0),X1,X0) = c_HOL_Ozero__class_Ozero(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_mult__eq__0__iff_1) ).
fof(f31,plain,
! [X0,X1] :
( ~ class_Ring__and__Field_Oring__no__zero__divisors(X0)
| c_HOL_Ozero__class_Ozero(X0) = c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(X0),X1,X0) ),
inference(reorient_equations,[],[f30]) ).
fof(f113,axiom,
! [X0,X1] :
( ~ class_Ring__and__Field_Ofield(X0)
| ~ class_Ring__and__Field_Odivision__by__zero(X0)
| c_HOL_Ozero__class_Ozero(X0) = c_HOL_Oinverse__class_Odivide(X1,c_HOL_Ozero__class_Ozero(X0),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_eq__divide__eq_2) ).
fof(f131,axiom,
! [X0,X1] :
( ~ class_RealVector_Oreal__normed__field(X0)
| c_HOL_Oinverse__class_Odivide(c_HOL_Ozero__class_Ozero(X0),X1,X0) = c_HOL_Ozero__class_Ozero(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_divide_Ozero_0) ).
fof(f132,plain,
! [X0,X1] :
( ~ class_RealVector_Oreal__normed__field(X0)
| c_HOL_Ozero__class_Ozero(X0) = c_HOL_Oinverse__class_Odivide(c_HOL_Ozero__class_Ozero(X0),X1,X0) ),
inference(reorient_equations,[],[f131]) ).
fof(f137,axiom,
! [X0,X1] :
( c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal)
| X0 = X1
| ~ c_lessequals(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(f173,axiom,
! [X2,X0,X1] :
( ~ class_Orderings_Olinorder(X0)
| X1 = X2
| ~ c_lessequals(X1,X2,X0)
| c_HOL_Oord__class_Oless(X1,X2,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_linorder__antisym__conv1_0) ).
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(f319,axiom,
! [X2,X0,X1] :
( ~ class_Ring__and__Field_Oordered__semiring__strict(X0)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(X0),c_HOL_Otimes__class_Otimes(X1,X2,X0),X0)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(X0),X2,X0)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(X0),X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_mult__pos__pos_0) ).
fof(f437,axiom,
! [X0,X1] :
( ~ c_lessequals(X0,X1,tc_RealDef_Oreal)
| ~ c_lessequals(X1,X0,tc_RealDef_Oreal)
| X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_real__le__antisym_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(f584,axiom,
! [X2,X3,X0,X1] :
( ~ class_Ring__and__Field_Oordered__field(X0)
| c_HOL_Oord__class_Oless(X1,c_HOL_Oinverse__class_Odivide(X2,X3,X0),X0)
| ~ c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(X1,X3,X0),X2,X0)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(X0),X3,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_mult__imp__less__div__pos_0) ).
fof(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(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(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(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(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(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(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(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(f979,axiom,
class_RealVector_Oreal__normed__field(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_RealDef__Oreal__RealVector_Oreal__normed__field) ).
fof(f992,axiom,
class_Ring__and__Field_Ofield(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_RealDef__Oreal__Ring__and__Field_Ofield) ).
fof(f996,axiom,
class_Orderings_Olinorder(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_RealDef__Oreal__Orderings_Olinorder) ).
fof(f1082,plain,
! [X0,X1] :
( class_Ring__and__Field_Ofield(X0)
| class_Ring__and__Field_Odivision__by__zero(X0)
| c_HOL_Ozero__class_Ozero(X0) = c_HOL_Oinverse__class_Odivide(X1,c_HOL_Ozero__class_Ozero(X0),X0) ),
inference(consistent_polarity_flipping,[],[f113]) ).
fof(f1095,plain,
! [X0,X1] :
( ~ c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal)
| X0 = X1
| ~ c_lessequals(X0,X1,tc_RealDef_Oreal) ),
inference(consistent_polarity_flipping,[],[f137]) ).
fof(f1122,plain,
! [X2,X0,X1] :
( ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| X1 = X2
| ~ c_lessequals(X1,X2,X0)
| class_Orderings_Olinorder(X0) ),
inference(consistent_polarity_flipping,[],[f173]) ).
fof(f1204,plain,
! [X2,X0,X1] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(X0),c_HOL_Otimes__class_Otimes(X1,X2,X0),X0)
| class_Ring__and__Field_Oordered__semiring__strict(X0)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(X0),X2,X0)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(X0),X1,X0) ),
inference(consistent_polarity_flipping,[],[f319]) ).
fof(f1336,plain,
~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),
inference(consistent_polarity_flipping,[],[f564]) ).
fof(f1352,plain,
! [X2,X3,X0,X1] :
( ~ c_HOL_Oord__class_Oless(X1,c_HOL_Oinverse__class_Odivide(X2,X3,X0),X0)
| class_Ring__and__Field_Oordered__field(X0)
| c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(X1,X3,X0),X2,X0)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(X0),X3,X0) ),
inference(consistent_polarity_flipping,[],[f584]) ).
fof(f1473,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_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),
inference(consistent_polarity_flipping,[],[f799]) ).
fof(f1479,plain,
! [X0] : c_HOL_Oord__class_Oless(X0,X0,tc_RealDef_Oreal),
inference(consistent_polarity_flipping,[],[f809]) ).
fof(f1497,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)
| c_HOL_Oord__class_Oless(v_k,v_n,tc_nat) ),
inference(consistent_polarity_flipping,[],[f871]) ).
fof(f1498,plain,
~ c_HOL_Oord__class_Oless(v_k,v_n,tc_nat),
inference(consistent_polarity_flipping,[],[f872]) ).
fof(f1500,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),
inference(consistent_polarity_flipping,[],[f874]) ).
fof(f1535,plain,
~ class_Ring__and__Field_Oordered__semiring__strict(tc_RealDef_Oreal),
inference(consistent_polarity_flipping,[],[f956]) ).
fof(f1543,plain,
~ class_Ring__and__Field_Odivision__by__zero(tc_RealDef_Oreal),
inference(consistent_polarity_flipping,[],[f969]) ).
fof(f1546,plain,
~ class_Ring__and__Field_Oordered__field(tc_RealDef_Oreal),
inference(consistent_polarity_flipping,[],[f977]) ).
fof(f1551,plain,
~ class_Ring__and__Field_Ofield(tc_RealDef_Oreal),
inference(consistent_polarity_flipping,[],[f992]) ).
fof(f1553,plain,
~ class_Orderings_Olinorder(tc_RealDef_Oreal),
inference(consistent_polarity_flipping,[],[f996]) ).
fof(f1568,definition,
( spl0_1
<=> c_HOL_Oord__class_Oless(v_k,v_n,tc_nat) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f1572,definition,
( spl0_2
<=> 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) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f1574,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)
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f1572]) ).
fof(f1576,definition,
( spl0_3
<=> 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) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f1579,plain,
( spl0_1
| spl0_2
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f1497,f1576,f1572,f1568]) ).
fof(f1580,plain,
spl0_3,
inference(avatar_split_clause,[],[f1500,f1576]) ).
fof(f1581,plain,
~ spl0_1,
inference(avatar_split_clause,[],[f1498,f1568]) ).
fof(f1642,plain,
! [X0] : c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(resolution,[],[f29,f959]) ).
fof(f1645,plain,
! [X0] : c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal),
inference(resolution,[],[f31,f959]) ).
fof(f1671,plain,
! [X0] : c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_HOL_Oinverse__class_Odivide(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal),
inference(resolution,[],[f132,f979]) ).
fof(f1771,plain,
( ~ c_lessequals(c_Transcendental_Opi,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_Transcendental_Opi ),
inference(resolution,[],[f437,f731]) ).
fof(f1793,plain,
~ c_lessequals(c_Transcendental_Opi,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_subsumption_resolution,[],[f1771,f152]) ).
fof(f1943,plain,
! [X0] :
( class_Ring__and__Field_Odivision__by__zero(tc_RealDef_Oreal)
| c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_HOL_Oinverse__class_Odivide(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(resolution,[],[f1082,f1551]) ).
fof(f1946,plain,
! [X0] : c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_HOL_Oinverse__class_Odivide(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_subsumption_resolution,[],[f1943,f1543]) ).
fof(f4210,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),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ spl0_2 ),
inference(forward_demodulation,[],[f1574,f864]) ).
fof(f4299,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(f4310,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,[],[f4299,f1793]) ).
fof(f7557,definition,
( spl0_109
<=> c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(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) ),
introduced(definition,[new_symbols(definition,[spl0_109])],[avatar_definition]) ).
fof(f7559,plain,
( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(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)
| ~ spl0_109 ),
inference(avatar_component_clause,[],[f7557]) ).
fof(f7561,definition,
( spl0_110
<=> c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[spl0_110])],[avatar_definition]) ).
fof(f7563,plain,
( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal)
| ~ spl0_110 ),
inference(avatar_component_clause,[],[f7561]) ).
fof(f8832,plain,
( class_Ring__and__Field_Oordered__field(tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(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_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal)
| ~ spl0_2 ),
inference(resolution,[],[f1352,f4210]) ).
fof(f8846,plain,
( c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(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_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal)
| ~ spl0_2 ),
inference(forward_subsumption_resolution,[],[f8832,f1546]) ).
fof(f8850,plain,
( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(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_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal)
| ~ spl0_2 ),
inference(forward_demodulation,[],[f8846,f1645]) ).
fof(f8852,plain,
( spl0_110
| spl0_109
| ~ spl0_2 ),
inference(avatar_split_clause,[],[f8850,f1572,f7557,f7561]) ).
fof(f9178,definition,
( spl0_119
<=> 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) ),
introduced(definition,[new_symbols(definition,[spl0_119])],[avatar_definition]) ).
fof(f9179,plain,
( 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)
| spl0_119 ),
inference(avatar_component_clause,[],[f9178]) ).
fof(f9180,plain,
( 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)
| ~ spl0_119 ),
inference(avatar_component_clause,[],[f9178]) ).
fof(f9749,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,[],[f1473,f864]) ).
fof(f9818,definition,
( spl0_128
<=> c_HOL_Oord__class_Oless(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) ),
introduced(definition,[new_symbols(definition,[spl0_128])],[avatar_definition]) ).
fof(f9819,plain,
( ~ c_HOL_Oord__class_Oless(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)
| spl0_128 ),
inference(avatar_component_clause,[],[f9818]) ).
fof(f9820,plain,
( c_HOL_Oord__class_Oless(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)
| ~ spl0_128 ),
inference(avatar_component_clause,[],[f9818]) ).
fof(f9900,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_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ spl0_119 ),
inference(superposition,[],[f9749,f9180]) ).
fof(f9901,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_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ spl0_119 ),
inference(forward_demodulation,[],[f9900,f1642]) ).
fof(f9924,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_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealDef_Oreal(v_k,tc_nat),tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ spl0_119 ),
inference(forward_demodulation,[],[f9901,f864]) ).
fof(f9935,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ spl0_119 ),
inference(forward_demodulation,[],[f9924,f1645]) ).
fof(f9938,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ spl0_119 ),
inference(forward_demodulation,[],[f9935,f1671]) ).
fof(f9939,plain,
( $false
| ~ spl0_119 ),
inference(forward_subsumption_resolution,[],[f9938,f1479]) ).
fof(f9940,plain,
~ spl0_119,
inference(avatar_contradiction_clause,[],[f9939]) ).
fof(f10032,plain,
( 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)
| ~ 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)
| class_Orderings_Olinorder(tc_RealDef_Oreal)
| ~ spl0_128 ),
inference(resolution,[],[f9820,f1122]) ).
fof(f10037,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)
| class_Orderings_Olinorder(tc_RealDef_Oreal)
| spl0_119
| ~ spl0_128 ),
inference(forward_subsumption_resolution,[],[f10032,f9179]) ).
fof(f10058,plain,
( class_Orderings_Olinorder(tc_RealDef_Oreal)
| spl0_119
| ~ spl0_128 ),
inference(forward_subsumption_resolution,[],[f10037,f4310]) ).
fof(f10074,plain,
( $false
| spl0_119
| ~ spl0_128 ),
inference(forward_subsumption_resolution,[],[f10058,f1553]) ).
fof(f10075,plain,
( spl0_119
| ~ spl0_128 ),
inference(avatar_contradiction_clause,[],[f10074]) ).
fof(f12069,plain,
( c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_RealDef_Oreal(v_n,tc_nat)
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealDef_Oreal(v_n,tc_nat),tc_RealDef_Oreal)
| ~ spl0_110 ),
inference(resolution,[],[f7563,f1095]) ).
fof(f12086,plain,
( c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_RealDef_Oreal(v_n,tc_nat)
| ~ spl0_110 ),
inference(forward_subsumption_resolution,[],[f12069,f238]) ).
fof(f12202,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_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ spl0_110 ),
inference(superposition,[],[f9749,f12086]) ).
fof(f12212,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ spl0_110 ),
inference(forward_demodulation,[],[f12202,f1946]) ).
fof(f12214,plain,
( $false
| ~ spl0_110 ),
inference(forward_subsumption_resolution,[],[f12212,f1479]) ).
fof(f12215,plain,
~ spl0_110,
inference(avatar_contradiction_clause,[],[f12214]) ).
fof(f20207,plain,
( class_Ring__and__Field_Oordered__semiring__strict(tc_RealDef_Oreal)
| c_HOL_Oord__class_Oless(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)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal)
| ~ spl0_109 ),
inference(resolution,[],[f7559,f1204]) ).
fof(f20302,plain,
( c_HOL_Oord__class_Oless(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)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal)
| ~ spl0_109 ),
inference(forward_subsumption_resolution,[],[f20207,f1535]) ).
fof(f20345,plain,
( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal)
| ~ spl0_109
| spl0_128 ),
inference(forward_subsumption_resolution,[],[f20302,f9819]) ).
fof(f20430,plain,
( $false
| ~ spl0_109
| spl0_128 ),
inference(forward_subsumption_resolution,[],[f20345,f1336]) ).
fof(f20431,plain,
( ~ spl0_109
| spl0_128 ),
inference(avatar_contradiction_clause,[],[f20430]) ).
cnf(s1,plain,
( spl0_1
| spl0_2
| ~ spl0_3 ),
inference(sat_conversion,[],[f1579]) ).
cnf(s2,plain,
spl0_3,
inference(sat_conversion,[],[f1580]) ).
cnf(s3,plain,
~ spl0_1,
inference(sat_conversion,[],[f1581]) ).
cnf(s239,plain,
( ~ spl0_2
| spl0_109
| spl0_110 ),
inference(sat_conversion,[],[f8852]) ).
cnf(s268,plain,
~ spl0_119,
inference(sat_conversion,[],[f9940]) ).
cnf(s273,plain,
( spl0_119
| ~ spl0_128 ),
inference(sat_conversion,[],[f10075]) ).
cnf(s303,plain,
~ spl0_110,
inference(sat_conversion,[],[f12215]) ).
cnf(s379,plain,
( ~ spl0_109
| spl0_128 ),
inference(sat_conversion,[],[f20431]) ).
cnf(s381,plain,
~ spl0_128,
inference(rat,[],[s273,s268]) ).
cnf(s382,plain,
~ spl0_109,
inference(rat,[],[s379,s381]) ).
cnf(s392,plain,
~ spl0_2,
inference(rat,[],[s239,s303,s382]) ).
cnf(s403,plain,
$false,
inference(rat,[],[s1,s2,s392,s3]) ).
fof(f20432,plain,
$false,
inference(avatar_sat_refutation,[],[s403]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWV611-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.13/0.27 % Computer : n026.cluster.edu
% 0.13/0.27 % Model : x86_64 x86_64
% 0.13/0.27 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.27 % Memory : 8046.5625MB
% 0.13/0.27 % OS : Linux 6.8.0-71-generic
% 0.13/0.27 % CPULimit : 300
% 0.13/0.27 % WCLimit : 300
% 0.13/0.27 % DateTime : Mon Sep 28 12:05:27 UTC 2026
% 0.13/0.27 % CPUTime :
% 0.13/0.27 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.26/0.32 Running first-order model finding
% 0.26/0.32 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.18/1.27 % (3810869)Will run a generic schedule for satisfiability detection.
% 6.18/1.27 % (3810874)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=739429283_2999 on theBenchmark for (2999ds/0Mi)
% 6.18/1.27 % (3810875)% WARNING: option uhcvi not known.
% 6.18/1.27 % (3810878)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=248238503:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 6.18/1.27 % (3810877)dis+10_1_sil=32000:sp=arity:random_seed=917324619:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 6.18/1.27 % (3810880)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=514628334:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 6.18/1.27 % (3810876)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1604916082:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 6.18/1.27 % (3810879)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1969623694:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 6.18/1.27 % (3810875)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3925110575:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 6.18/1.27 % TRYING [1]
% 6.18/1.27 % TRYING [2]
% 6.18/1.27 % (3810877)Instruction limit reached!
% 6.18/1.27 % (3810877)------------------------------
% 6.18/1.27 % (3810877)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.18/1.27 % (3810877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.18/1.27 % (3810877)CaDiCaL version: 2.1.3
% 6.18/1.27 % (3810877)Termination reason: Instruction limit
% 6.18/1.27 % (3810877)Termination phase: Saturation
% 6.18/1.27 % (3810877)Time elapsed: 0.105 s
% 6.18/1.27 % (3810877)Peak memory usage: 13 MB
% 6.18/1.27 % (3810877)Instructions burned: 103 (million)
% 6.18/1.27 % (3810878)Instruction limit reached!
% 6.18/1.27 % (3810878)------------------------------
% 6.18/1.27 % (3810878)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.18/1.27 % (3810878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.18/1.27 % (3810878)CaDiCaL version: 2.1.3
% 6.18/1.27 % (3810878)Termination reason: Instruction limit
% 6.18/1.27 % (3810878)Termination phase: Saturation
% 6.18/1.27 % (3810878)Time elapsed: 0.112 s
% 6.18/1.27 % (3810878)Peak memory usage: 13 MB
% 6.18/1.27 % (3810878)Instructions burned: 118 (million)
% 6.18/1.27 % (3810880)Instruction limit reached!
% 6.18/1.27 % (3810880)------------------------------
% 6.18/1.27 % (3810880)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.18/1.27 % (3810880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.18/1.27 % (3810880)CaDiCaL version: 2.1.3
% 6.18/1.27 % (3810880)Termination reason: Instruction limit
% 6.18/1.27 % (3810880)Termination phase: Saturation
% 6.18/1.27 % (3810880)Time elapsed: 0.125 s
% 6.18/1.27 % (3810880)Peak memory usage: 14 MB
% 6.18/1.27 % (3810880)Instructions burned: 160 (million)
% 6.18/1.27 % (3810879)Instruction limit reached!
% 6.18/1.27 % (3810879)------------------------------
% 6.18/1.27 % (3810879)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.18/1.27 % (3810879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.18/1.27 % (3810879)CaDiCaL version: 2.1.3
% 6.18/1.27 % (3810879)Termination reason: Instruction limit
% 6.18/1.27 % (3810879)Termination phase: Saturation
% 6.18/1.27 % (3810879)Time elapsed: 0.130 s
% 6.18/1.27 % (3810879)Peak memory usage: 13 MB
% 6.18/1.27 % (3810879)Instructions burned: 131 (million)
% 6.18/1.27 % (3810890)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2851364432:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 6.18/1.27 % (3810891)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=4043519926:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 6.18/1.27 % (3810892)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=2886297157:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 6.18/1.27 % (3810893)ott-21_1_sil=16000:fs=off:random_seed=386444641:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 6.18/1.27 % TRYING [3]
% 6.18/1.27 % (3810891)Instruction limit reached!
% 6.18/1.27 % (3810891)------------------------------
% 6.18/1.27 % (3810891)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.18/1.27 % (3810891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.18/1.27 % (3810891)CaDiCaL version: 2.1.3
% 6.18/1.27 % (3810891)Termination reason: Instruction limit
% 6.18/1.27 % (3810891)Termination phase: Saturation
% 6.18/1.27 % (3810891)Time elapsed: 0.128 s
% 6.18/1.27 % (3810891)Peak memory usage: 14 MB
% 6.18/1.27 % (3810891)Instructions burned: 131 (million)
% 6.18/1.27 % (3810898)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=839341950:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 6.18/1.27 % (3810893)Instruction limit reached!
% 6.18/1.27 % (3810893)------------------------------
% 6.18/1.27 % (3810893)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.18/1.27 % (3810893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.18/1.27 % (3810893)CaDiCaL version: 2.1.3
% 6.18/1.27 % (3810893)Termination reason: Instruction limit
% 6.18/1.27 % (3810893)Termination phase: Saturation
% 6.18/1.27 % (3810893)Time elapsed: 0.170 s
% 6.18/1.27 % (3810893)Peak memory usage: 13 MB
% 6.18/1.27 % (3810893)Instructions burned: 180 (million)
% 6.18/1.27 % (3810900)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=4270006931:fmbsr=1.3:i=865:ins=25_2995 on theBenchmark for (2995ds/865Mi)
% 6.18/1.27 % TRYING [1]
% 6.18/1.27 % TRYING [2]
% 6.18/1.27 % TRYING [1]
% 6.18/1.27 % TRYING [3]
% 6.18/1.27 % TRYING [2]
% 6.18/1.27 % (3810892)Instruction limit reached!
% 6.18/1.27 % (3810892)------------------------------
% 6.18/1.27 % (3810892)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.18/1.27 % (3810892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.18/1.27 % (3810892)CaDiCaL version: 2.1.3
% 6.18/1.27 % (3810892)Termination reason: Instruction limit
% 6.18/1.27 % (3810892)Termination phase: Saturation
% 6.18/1.27 % (3810892)Time elapsed: 0.580 s
% 6.18/1.27 % (3810892)Peak memory usage: 17 MB
% 6.18/1.27 % (3810892)Instructions burned: 685 (million)
% 6.18/1.27 % (3810890)Instruction limit reached!
% 6.18/1.27 % (3810890)------------------------------
% 6.18/1.27 % (3810890)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.18/1.27 % (3810890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.18/1.27 % (3810890)CaDiCaL version: 2.1.3
% 6.18/1.27 % (3810890)Termination reason: Instruction limit
% 6.18/1.27 % (3810890)Termination phase: Finite model building constraint generation
% 6.18/1.27 % (3810890)Time elapsed: 0.593 s
% 6.18/1.27 % (3810890)Peak memory usage: 28 MB
% 6.18/1.27 % (3810890)Instructions burned: 714 (million)
% 6.18/1.27 % (3810906)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2653006782:i=1179_2991 on theBenchmark for (2991ds/1179Mi)
% 6.18/1.27 % (3810907)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3756619590:i=889:ins=1_2991 on theBenchmark for (2991ds/889Mi)
% 6.18/1.27 % (3810898)Instruction limit reached!
% 6.18/1.27 % (3810898)------------------------------
% 6.18/1.27 % (3810898)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.18/1.27 % (3810898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.18/1.27 % (3810898)CaDiCaL version: 2.1.3
% 6.18/1.27 % (3810898)Termination reason: Instruction limit
% 6.18/1.27 % (3810898)Termination phase: Saturation
% 6.18/1.27 % (3810898)Time elapsed: 0.500 s
% 6.18/1.27 % (3810898)Peak memory usage: 14 MB
% 6.18/1.27 % (3810898)Instructions burned: 477 (million)
% 6.18/1.27 % (3810911)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=3676509141:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2991 on theBenchmark for (2991ds/692Mi)
% 6.18/1.27 % TRYING [4]
% 6.18/1.27 % (3810875) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3810869-3810875"...
% 6.18/1.27 % (3810875)...printing done.
% 6.18/1.27 % (3810875)Refutation found. Thanks to Tanya!
% 6.18/1.27 % SZS status Unsatisfiable for theBenchmark
% 6.18/1.27 % SZS output start Proof for theBenchmark
% See solution above
% 6.18/1.28 % (3810875)------------------------------
% 6.18/1.28 % (3810875)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.18/1.28 % (3810875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.18/1.28 % (3810875)CaDiCaL version: 2.1.3
% 6.18/1.28 % (3810875)Termination reason: Refutation
% 6.18/1.28 % (3810875)Time elapsed: 0.849 s
% 6.18/1.28 % (3810875)Peak memory usage: 19 MB
% 6.18/1.28 % (3810875)Instructions burned: 830 (million)
% 6.18/1.28 % (3810869)Success in time 0.943 s
% 6.18/1.28 % Vampire exiting
%------------------------------------------------------------------------------