%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ALG374-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n017.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 09:19:53 AM UTC 2026
% Result : Unsatisfiable 8.60s 2.04s
% Output : Refutation 10.24s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 36
% Syntax : Number of formulae : 139 ( 56 unt; 18 def)
% Number of atoms : 241 ( 44 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 199 ( 97 ~; 93 |; 0 &)
% ( 9 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 15 ( 13 usr; 10 prp; 0-3 aty)
% Number of functors : 27 ( 27 usr; 13 con; 0-4 aty)
% Number of variables : 40 ( 0 sgn 40 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f13,axiom,
! [X0] :
( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealDef_Oreal(X0,tc_nat),tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_real__of__nat__gt__zero__cancel__iff_1) ).
fof(f194,axiom,
! [X0] : c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Suc(X0),tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_zero__less__Suc_0) ).
fof(f248,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(f324,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(f335,axiom,
! [X0] : c_HOL_Oplus__class_Oplus(X0,c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_real__add__eq__0__iff_1) ).
fof(f336,plain,
! [X0] : c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(X0,c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(reorient_equations,[],[f335]) ).
fof(f340,axiom,
! [X0,X1] : c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(X0,c_HOL_Ouminus__class_Ouminus(X1,tc_RealDef_Oreal),tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_real__diff__def_0) ).
fof(f441,axiom,
! [X0] : c_HOL_Oord__class_Oless(X0,c_Suc(X0),tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_less__Suc__eq_2) ).
fof(f512,axiom,
c_RealDef_Oreal(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat) = c_HOL_Oone__class_Oone(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_real__of__nat__one_0) ).
fof(f513,plain,
c_HOL_Oone__class_Oone(tc_RealDef_Oreal) = c_RealDef_Oreal(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat),
inference(reorient_equations,[],[f512]) ).
fof(f547,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(f553,axiom,
! [X0,X1] :
( ~ c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal)
| c_lessequals(X0,X1,tc_RealDef_Oreal) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_real__less__def_0) ).
fof(f556,axiom,
! [X2,X0,X1] :
( ~ class_OrderedGroup_Ogroup__add(X0)
| c_HOL_Oplus__class_Oplus(c_HOL_Ouminus__class_Ouminus(X1,X0),c_HOL_Oplus__class_Oplus(X1,X2,X0),X0) = X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_minus__add__cancel_0) ).
fof(f616,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(f630,axiom,
! [X2,X0,X1] :
( c_lessequals(c_HOL_Oplus__class_Oplus(X0,X1,tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(X0,X2,tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_lessequals(X1,X2,tc_RealDef_Oreal) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_real__add__left__mono_0) ).
fof(f701,axiom,
( c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_p,v_sko__CHAINED__1(v_n____,v_p,v_r,v_s____),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(c_HOL_Ouminus__class_Ouminus(v_s____,tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_RealDef_Oreal(c_Suc(v_n____),tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ouminus__class_Ouminus(v_s____,tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_HOL_Ouminus__class_Ouminus(v_s____,tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_RealDef_Oreal(c_Suc(v_n____),tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_CHAINED_2) ).
fof(f702,axiom,
( c_lessequals(c_RealVector_Onorm__class_Onorm(v_sko__CHAINED__1(v_n____,v_p,v_r,v_s____),tc_Complex_Ocomplex),v_r,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ouminus__class_Ouminus(v_s____,tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_HOL_Ouminus__class_Ouminus(v_s____,tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_RealDef_Oreal(c_Suc(v_n____),tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_CHAINED_1) ).
fof(f704,negated_conjecture,
! [X0] :
( ~ c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_p,X0,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(c_HOL_Ouminus__class_Ouminus(v_s____,tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_RealDef_Oreal(c_Suc(v_n____),tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_lessequals(c_RealVector_Onorm__class_Onorm(X0,tc_Complex_Ocomplex),v_r,tc_RealDef_Oreal) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f747,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(f758,axiom,
class_OrderedGroup_Ogroup__add(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_RealDef__Oreal__OrderedGroup_Ogroup__add) ).
fof(f792,definition,
! [X0] : sF0(X0) = c_Polynomial_Opoly(v_p,X0,tc_Complex_Ocomplex),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f793,plain,
! [X0] : c_Polynomial_Opoly(v_p,X0,tc_Complex_Ocomplex) = sF0(X0),
inference(reorient_equations,[],[f792]) ).
fof(f794,definition,
! [X0] : sF1(X0) = c_RealVector_Onorm__class_Onorm(sF0(X0),tc_Complex_Ocomplex),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f795,plain,
! [X0] : c_RealVector_Onorm__class_Onorm(sF0(X0),tc_Complex_Ocomplex) = sF1(X0),
inference(reorient_equations,[],[f794]) ).
fof(f796,definition,
sF2 = c_HOL_Ouminus__class_Ouminus(v_s____,tc_RealDef_Oreal),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f797,plain,
c_HOL_Ouminus__class_Ouminus(v_s____,tc_RealDef_Oreal) = sF2,
inference(reorient_equations,[],[f796]) ).
fof(f798,definition,
sF3 = c_HOL_Oone__class_Oone(tc_RealDef_Oreal),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f799,plain,
c_HOL_Oone__class_Oone(tc_RealDef_Oreal) = sF3,
inference(reorient_equations,[],[f798]) ).
fof(f800,definition,
sF4 = c_Suc(v_n____),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f801,plain,
c_Suc(v_n____) = sF4,
inference(reorient_equations,[],[f800]) ).
fof(f802,definition,
sF5 = c_RealDef_Oreal(sF4,tc_nat),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f803,plain,
c_RealDef_Oreal(sF4,tc_nat) = sF5,
inference(reorient_equations,[],[f802]) ).
fof(f804,definition,
sF6 = c_HOL_Oinverse__class_Odivide(sF3,sF5,tc_RealDef_Oreal),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f805,plain,
c_HOL_Oinverse__class_Odivide(sF3,sF5,tc_RealDef_Oreal) = sF6,
inference(reorient_equations,[],[f804]) ).
fof(f806,definition,
sF7 = c_HOL_Oplus__class_Oplus(sF2,sF6,tc_RealDef_Oreal),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f807,plain,
c_HOL_Oplus__class_Oplus(sF2,sF6,tc_RealDef_Oreal) = sF7,
inference(reorient_equations,[],[f806]) ).
fof(f808,definition,
! [X0] : sF8(X0) = c_RealVector_Onorm__class_Onorm(X0,tc_Complex_Ocomplex),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f809,plain,
! [X0] : c_RealVector_Onorm__class_Onorm(X0,tc_Complex_Ocomplex) = sF8(X0),
inference(reorient_equations,[],[f808]) ).
fof(f810,plain,
! [X0] :
( ~ c_HOL_Oord__class_Oless(sF1(X0),sF7,tc_RealDef_Oreal)
| ~ c_lessequals(sF8(X0),v_r,tc_RealDef_Oreal) ),
inference(definition_folding,[],[f704,f809,f807,f805,f803,f801,f799,f797,f795,f793]) ).
fof(f816,definition,
( spl9_2
<=> c_HOL_Oord__class_Oless(c_HOL_Ouminus__class_Ouminus(v_s____,tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_HOL_Ouminus__class_Ouminus(v_s____,tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_RealDef_Oreal(c_Suc(v_n____),tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[spl9_2])],[avatar_definition]) ).
fof(f817,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ouminus__class_Ouminus(v_s____,tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_HOL_Ouminus__class_Ouminus(v_s____,tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_RealDef_Oreal(c_Suc(v_n____),tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)
| spl9_2 ),
inference(avatar_component_clause,[],[f816]) ).
fof(f821,definition,
( spl9_3
<=> c_lessequals(c_RealVector_Onorm__class_Onorm(v_sko__CHAINED__1(v_n____,v_p,v_r,v_s____),tc_Complex_Ocomplex),v_r,tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[spl9_3])],[avatar_definition]) ).
fof(f823,plain,
( c_lessequals(c_RealVector_Onorm__class_Onorm(v_sko__CHAINED__1(v_n____,v_p,v_r,v_s____),tc_Complex_Ocomplex),v_r,tc_RealDef_Oreal)
| ~ spl9_3 ),
inference(avatar_component_clause,[],[f821]) ).
fof(f824,plain,
( ~ spl9_2
| spl9_3 ),
inference(avatar_split_clause,[],[f702,f821,f816]) ).
fof(f826,definition,
( spl9_4
<=> c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_p,v_sko__CHAINED__1(v_n____,v_p,v_r,v_s____),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(c_HOL_Ouminus__class_Ouminus(v_s____,tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_RealDef_Oreal(c_Suc(v_n____),tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[spl9_4])],[avatar_definition]) ).
fof(f828,plain,
( c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_p,v_sko__CHAINED__1(v_n____,v_p,v_r,v_s____),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(c_HOL_Ouminus__class_Ouminus(v_s____,tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_RealDef_Oreal(c_Suc(v_n____),tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ spl9_4 ),
inference(avatar_component_clause,[],[f826]) ).
fof(f829,plain,
( ~ spl9_2
| spl9_4 ),
inference(avatar_split_clause,[],[f701,f826,f816]) ).
fof(f847,plain,
! [X0] : c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_HOL_Ominus__class_Ominus(X0,X0,tc_RealDef_Oreal),
inference(forward_demodulation,[],[f336,f340]) ).
fof(f850,plain,
( c_lessequals(sF8(v_sko__CHAINED__1(v_n____,v_p,v_r,v_s____)),v_r,tc_RealDef_Oreal)
| ~ spl9_3 ),
inference(forward_demodulation,[],[f823,f809]) ).
fof(f851,plain,
( c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_p,v_sko__CHAINED__1(v_n____,v_p,v_r,v_s____),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(c_HOL_Ouminus__class_Ouminus(v_s____,tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_RealDef_Oreal(sF4,tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ spl9_4 ),
inference(forward_demodulation,[],[f828,f801]) ).
fof(f853,plain,
( c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_p,v_sko__CHAINED__1(v_n____,v_p,v_r,v_s____),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(c_HOL_Ouminus__class_Ouminus(v_s____,tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),sF5,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ spl9_4 ),
inference(forward_demodulation,[],[f851,f803]) ).
fof(f855,plain,
( c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_p,v_sko__CHAINED__1(v_n____,v_p,v_r,v_s____),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(c_HOL_Ouminus__class_Ouminus(v_s____,tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(sF3,sF5,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ spl9_4 ),
inference(forward_demodulation,[],[f853,f799]) ).
fof(f857,plain,
( c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_p,v_sko__CHAINED__1(v_n____,v_p,v_r,v_s____),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(c_HOL_Ouminus__class_Ouminus(v_s____,tc_RealDef_Oreal),sF6,tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ spl9_4 ),
inference(forward_demodulation,[],[f855,f805]) ).
fof(f859,plain,
( c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_p,v_sko__CHAINED__1(v_n____,v_p,v_r,v_s____),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(sF2,sF6,tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ spl9_4 ),
inference(forward_demodulation,[],[f857,f797]) ).
fof(f861,plain,
( c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_p,v_sko__CHAINED__1(v_n____,v_p,v_r,v_s____),tc_Complex_Ocomplex),tc_Complex_Ocomplex),sF7,tc_RealDef_Oreal)
| ~ spl9_4 ),
inference(forward_demodulation,[],[f859,f807]) ).
fof(f862,plain,
( c_HOL_Oord__class_Oless(sF8(c_Polynomial_Opoly(v_p,v_sko__CHAINED__1(v_n____,v_p,v_r,v_s____),tc_Complex_Ocomplex)),sF7,tc_RealDef_Oreal)
| ~ spl9_4 ),
inference(forward_demodulation,[],[f861,f809]) ).
fof(f863,plain,
( c_HOL_Oord__class_Oless(sF8(sF0(v_sko__CHAINED__1(v_n____,v_p,v_r,v_s____))),sF7,tc_RealDef_Oreal)
| ~ spl9_4 ),
inference(forward_demodulation,[],[f862,f793]) ).
fof(f881,plain,
! [X0] : sF1(X0) = sF8(sF0(X0)),
inference(superposition,[],[f795,f809]) ).
fof(f883,plain,
( c_HOL_Oord__class_Oless(sF1(v_sko__CHAINED__1(v_n____,v_p,v_r,v_s____)),sF7,tc_RealDef_Oreal)
| ~ spl9_4 ),
inference(superposition,[],[f863,f881]) ).
fof(f884,plain,
( ~ c_lessequals(sF8(v_sko__CHAINED__1(v_n____,v_p,v_r,v_s____)),v_r,tc_RealDef_Oreal)
| ~ spl9_4 ),
inference(resolution,[],[f883,f810]) ).
fof(f886,plain,
( $false
| ~ spl9_3
| ~ spl9_4 ),
inference(forward_subsumption_resolution,[],[f884,f850]) ).
fof(f887,plain,
( ~ spl9_3
| ~ spl9_4 ),
inference(avatar_contradiction_clause,[],[f886]) ).
fof(f889,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ouminus__class_Ouminus(v_s____,tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_HOL_Ouminus__class_Ouminus(v_s____,tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_RealDef_Oreal(sF4,tc_nat),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)
| spl9_2 ),
inference(forward_demodulation,[],[f817,f801]) ).
fof(f892,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ouminus__class_Ouminus(v_s____,tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_HOL_Ouminus__class_Ouminus(v_s____,tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),sF5,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)
| spl9_2 ),
inference(forward_demodulation,[],[f889,f803]) ).
fof(f895,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ouminus__class_Ouminus(v_s____,tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_HOL_Ouminus__class_Ouminus(v_s____,tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(sF3,sF5,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)
| spl9_2 ),
inference(forward_demodulation,[],[f892,f799]) ).
fof(f898,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ouminus__class_Ouminus(v_s____,tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_HOL_Ouminus__class_Ouminus(v_s____,tc_RealDef_Oreal),sF6,tc_RealDef_Oreal),tc_RealDef_Oreal)
| spl9_2 ),
inference(forward_demodulation,[],[f895,f805]) ).
fof(f901,plain,
( ~ c_HOL_Oord__class_Oless(sF2,c_HOL_Oplus__class_Oplus(sF2,sF6,tc_RealDef_Oreal),tc_RealDef_Oreal)
| spl9_2 ),
inference(forward_demodulation,[],[f898,f797]) ).
fof(f904,plain,
( ~ c_HOL_Oord__class_Oless(sF2,sF7,tc_RealDef_Oreal)
| spl9_2 ),
inference(forward_demodulation,[],[f901,f807]) ).
fof(f948,plain,
! [X0] :
( c_lessequals(c_HOL_Oplus__class_Oplus(sF2,X0,tc_RealDef_Oreal),sF7,tc_RealDef_Oreal)
| ~ c_lessequals(X0,sF6,tc_RealDef_Oreal) ),
inference(superposition,[],[f630,f807]) ).
fof(f1045,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_nat),sF4,tc_nat) ),
inference(superposition,[],[f13,f803]) ).
fof(f1077,plain,
( c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF6,tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF3,tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF5,tc_RealDef_Oreal) ),
inference(superposition,[],[f324,f805]) ).
fof(f1198,plain,
! [X0] : c_HOL_Ominus__class_Ominus(X0,v_s____,tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(X0,sF2,tc_RealDef_Oreal),
inference(superposition,[],[f340,f797]) ).
fof(f1252,plain,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),sF4,tc_nat),
inference(superposition,[],[f194,f801]) ).
fof(f1352,plain,
( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat) ),
inference(superposition,[],[f13,f513]) ).
fof(f1355,plain,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_subsumption_resolution,[],[f1352,f441]) ).
fof(f1357,plain,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF3,tc_RealDef_Oreal),
inference(forward_demodulation,[],[f1355,f799]) ).
fof(f1382,definition,
( spl9_30
<=> c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF5,tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[spl9_30])],[avatar_definition]) ).
fof(f1384,plain,
( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF5,tc_RealDef_Oreal)
| ~ spl9_30 ),
inference(avatar_component_clause,[],[f1382]) ).
fof(f1393,plain,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF5,tc_RealDef_Oreal),
inference(forward_subsumption_resolution,[],[f1045,f1252]) ).
fof(f1396,definition,
( spl9_33
<=> c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF5,tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[spl9_33])],[avatar_definition]) ).
fof(f1398,plain,
( ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF5,tc_RealDef_Oreal)
| spl9_33 ),
inference(avatar_component_clause,[],[f1396]) ).
fof(f1400,definition,
( spl9_34
<=> c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF3,tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[spl9_34])],[avatar_definition]) ).
fof(f1402,plain,
( ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF3,tc_RealDef_Oreal)
| spl9_34 ),
inference(avatar_component_clause,[],[f1400]) ).
fof(f1404,definition,
( spl9_35
<=> c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF6,tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[spl9_35])],[avatar_definition]) ).
fof(f1406,plain,
( c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF6,tc_RealDef_Oreal)
| ~ spl9_35 ),
inference(avatar_component_clause,[],[f1404]) ).
fof(f1407,plain,
( ~ spl9_33
| ~ spl9_34
| spl9_35 ),
inference(avatar_split_clause,[],[f1077,f1404,f1400,f1396]) ).
fof(f1413,plain,
spl9_30,
inference(avatar_split_clause,[],[f1393,f1382]) ).
fof(f1415,plain,
( c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF5,tc_RealDef_Oreal)
| ~ spl9_30 ),
inference(resolution,[],[f1384,f553]) ).
fof(f1416,plain,
( $false
| ~ spl9_30
| spl9_33 ),
inference(forward_subsumption_resolution,[],[f1415,f1398]) ).
fof(f1417,plain,
( ~ spl9_30
| spl9_33 ),
inference(avatar_contradiction_clause,[],[f1416]) ).
fof(f1418,plain,
c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF3,tc_RealDef_Oreal),
inference(resolution,[],[f1357,f553]) ).
fof(f1419,plain,
( $false
| spl9_34 ),
inference(forward_subsumption_resolution,[],[f1418,f1402]) ).
fof(f1420,plain,
spl9_34,
inference(avatar_contradiction_clause,[],[f1419]) ).
fof(f1457,definition,
( spl9_42
<=> c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = sF6 ),
introduced(definition,[new_symbols(definition,[spl9_42])],[avatar_definition]) ).
fof(f1459,plain,
( c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = sF6
| ~ spl9_42 ),
inference(avatar_component_clause,[],[f1457]) ).
fof(f1682,plain,
( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF6,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),sF5,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF3,tc_RealDef_Oreal) ),
inference(superposition,[],[f248,f805]) ).
fof(f2694,plain,
! [X0,X1] : c_HOL_Oplus__class_Oplus(c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(X0,X1,tc_RealDef_Oreal),tc_RealDef_Oreal) = X1,
inference(resolution,[],[f556,f758]) ).
fof(f2695,plain,
! [X0] : c_HOL_Oplus__class_Oplus(sF2,c_HOL_Oplus__class_Oplus(v_s____,X0,tc_RealDef_Oreal),tc_RealDef_Oreal) = X0,
inference(superposition,[],[f2694,f797]) ).
fof(f2720,plain,
sF2 = c_HOL_Oplus__class_Oplus(sF2,c_HOL_Ominus__class_Ominus(v_s____,v_s____,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(superposition,[],[f2695,f1198]) ).
fof(f2729,plain,
! [X0] : c_HOL_Oplus__class_Oplus(v_s____,X0,tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(c_HOL_Ouminus__class_Ouminus(sF2,tc_RealDef_Oreal),X0,tc_RealDef_Oreal),
inference(superposition,[],[f2694,f2695]) ).
fof(f2737,plain,
sF2 = c_HOL_Oplus__class_Oplus(sF2,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f2720,f847]) ).
fof(f2740,plain,
( c_lessequals(sF2,sF7,tc_RealDef_Oreal)
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF6,tc_RealDef_Oreal) ),
inference(superposition,[],[f948,f2737]) ).
fof(f2783,plain,
( c_lessequals(sF2,sF7,tc_RealDef_Oreal)
| ~ spl9_35 ),
inference(forward_subsumption_resolution,[],[f2740,f1406]) ).
fof(f2787,plain,
( sF2 = sF7
| c_HOL_Oord__class_Oless(sF2,sF7,tc_RealDef_Oreal)
| ~ spl9_35 ),
inference(resolution,[],[f2783,f616]) ).
fof(f2796,plain,
( sF2 = sF7
| spl9_2
| ~ spl9_35 ),
inference(forward_subsumption_resolution,[],[f2787,f904]) ).
fof(f2802,definition,
( spl9_84
<=> sF2 = sF7 ),
introduced(definition,[new_symbols(definition,[spl9_84])],[avatar_definition]) ).
fof(f2804,plain,
( sF2 = sF7
| ~ spl9_84 ),
inference(avatar_component_clause,[],[f2802]) ).
fof(f2807,plain,
( spl9_84
| spl9_2
| ~ spl9_35 ),
inference(avatar_split_clause,[],[f2796,f1404,f816,f2802]) ).
fof(f2857,plain,
! [X0] : c_HOL_Oplus__class_Oplus(v_s____,c_HOL_Oplus__class_Oplus(sF2,X0,tc_RealDef_Oreal),tc_RealDef_Oreal) = X0,
inference(superposition,[],[f2694,f2729]) ).
fof(f2900,plain,
sF6 = c_HOL_Oplus__class_Oplus(v_s____,sF7,tc_RealDef_Oreal),
inference(superposition,[],[f2857,f807]) ).
fof(f2922,plain,
( sF6 = c_HOL_Oplus__class_Oplus(v_s____,sF2,tc_RealDef_Oreal)
| ~ spl9_84 ),
inference(forward_demodulation,[],[f2900,f2804]) ).
fof(f2932,plain,
( sF6 = c_HOL_Ominus__class_Ominus(v_s____,v_s____,tc_RealDef_Oreal)
| ~ spl9_84 ),
inference(forward_demodulation,[],[f2922,f1198]) ).
fof(f2933,plain,
( c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = sF6
| ~ spl9_84 ),
inference(forward_demodulation,[],[f2932,f847]) ).
fof(f2934,plain,
( spl9_42
| ~ spl9_84 ),
inference(avatar_split_clause,[],[f2933,f2802,f1457]) ).
fof(f2994,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),sF5,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF3,tc_RealDef_Oreal) ),
inference(forward_subsumption_resolution,[],[f1682,f747]) ).
fof(f2996,plain,
( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF6,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF3,tc_RealDef_Oreal)
| ~ spl9_30 ),
inference(forward_subsumption_resolution,[],[f2994,f1384]) ).
fof(f2998,plain,
( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),sF6,tc_RealDef_Oreal)
| ~ spl9_30 ),
inference(forward_subsumption_resolution,[],[f2996,f1357]) ).
fof(f3000,plain,
( c_HOL_Oord__class_Oless(sF6,sF6,tc_RealDef_Oreal)
| ~ spl9_30
| ~ spl9_42 ),
inference(forward_demodulation,[],[f2998,f1459]) ).
fof(f3002,plain,
( $false
| ~ spl9_30
| ~ spl9_42 ),
inference(forward_subsumption_resolution,[],[f3000,f547]) ).
fof(f3003,plain,
( ~ spl9_30
| ~ spl9_42 ),
inference(avatar_contradiction_clause,[],[f3002]) ).
cnf(s2,plain,
( ~ spl9_2
| spl9_3 ),
inference(sat_conversion,[],[f824]) ).
cnf(s3,plain,
( ~ spl9_2
| spl9_4 ),
inference(sat_conversion,[],[f829]) ).
cnf(s6,plain,
( ~ spl9_3
| ~ spl9_4 ),
inference(sat_conversion,[],[f887]) ).
cnf(s20,plain,
( ~ spl9_33
| ~ spl9_34
| spl9_35 ),
inference(sat_conversion,[],[f1407]) ).
cnf(s22,plain,
spl9_30,
inference(sat_conversion,[],[f1413]) ).
cnf(s23,plain,
( ~ spl9_30
| spl9_33 ),
inference(sat_conversion,[],[f1417]) ).
cnf(s24,plain,
spl9_34,
inference(sat_conversion,[],[f1420]) ).
cnf(s72,plain,
( spl9_2
| ~ spl9_35
| spl9_84 ),
inference(sat_conversion,[],[f2807]) ).
cnf(s80,plain,
( spl9_42
| ~ spl9_84 ),
inference(sat_conversion,[],[f2934]) ).
cnf(s83,plain,
( ~ spl9_30
| ~ spl9_42 ),
inference(sat_conversion,[],[f3003]) ).
cnf(s89,plain,
~ spl9_42,
inference(rat,[],[s83,s22]) ).
cnf(s90,plain,
spl9_33,
inference(rat,[],[s23,s22]) ).
cnf(s91,plain,
~ spl9_84,
inference(rat,[],[s80,s89]) ).
cnf(s92,plain,
spl9_35,
inference(rat,[],[s20,s24,s90]) ).
cnf(s93,plain,
spl9_2,
inference(rat,[],[s72,s91,s92]) ).
cnf(s98,plain,
spl9_4,
inference(rat,[],[s3,s93]) ).
cnf(s99,plain,
~ spl9_3,
inference(rat,[],[s6,s98]) ).
cnf(s100,plain,
$false,
inference(rat,[],[s2,s99,s93]) ).
fof(f3014,plain,
$false,
inference(avatar_sat_refutation,[],[s100]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG374-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.19 % Computer : n017.cluster.edu
% 0.10/0.19 % Model : x86_64 x86_64
% 0.10/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.19 % Memory : 8046.5625MB
% 0.10/0.19 % OS : Linux 6.8.0-71-generic
% 0.10/0.20 % CPULimit : 300
% 0.10/0.20 % WCLimit : 300
% 0.10/0.20 % DateTime : Mon Sep 28 20:09:22 UTC 2026
% 0.10/0.20 % CPUTime :
% 0.10/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.23 Running first-order theorem proving
% 0.10/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 6.96/1.84 % (3962337)Input is clausal, will run a generic CNF schedule.
% 6.96/1.84 % (3962348)dis-21_1_sil=8000:lcm=predicate:random_seed=2304741454:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 6.96/1.84 % (3962348)Instruction limit reached!
% 6.96/1.84 % (3962348)------------------------------
% 6.96/1.84 % (3962348)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.96/1.84 % (3962348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.96/1.84 % (3962348)CaDiCaL version: 2.1.3
% 6.96/1.84 % (3962348)Termination reason: Instruction limit
% 6.96/1.84 % (3962348)Termination phase: Saturation
% 6.96/1.84 % (3962348)Time elapsed: 0.038 s
% 6.96/1.84 % (3962348)Peak memory usage: 89 MB
% 6.96/1.84 % (3962348)Instructions burned: 119 (million)
% 6.96/1.84 % (3962345)lrs+10_1_sil=8000:sp=occurrence:random_seed=3792675981:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 6.96/1.84 % (3962347)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1229558265:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 6.96/1.84 % (3962342)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=2997585203:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 6.96/1.84 % (3962344)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1529009915:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 6.96/1.84 % (3962346)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2154136584:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 6.96/1.84 % (3962343)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3989595725:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 6.96/1.84 % (3962345)Instruction limit reached!
% 6.96/1.84 % (3962345)------------------------------
% 6.96/1.84 % (3962345)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.96/1.84 % (3962345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.96/1.84 % (3962345)CaDiCaL version: 2.1.3
% 6.96/1.84 % (3962345)Termination reason: Instruction limit
% 6.96/1.84 % (3962345)Termination phase: Saturation
% 6.96/1.84 % (3962345)Time elapsed: 0.073 s
% 6.96/1.84 % (3962345)Peak memory usage: 89 MB
% 6.96/1.84 % (3962345)Instructions burned: 108 (million)
% 6.96/1.84 % (3962346)Instruction limit reached!
% 6.96/1.84 % (3962346)------------------------------
% 6.96/1.84 % (3962346)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.96/1.84 % (3962346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.96/1.84 % (3962346)CaDiCaL version: 2.1.3
% 6.96/1.84 % (3962346)Termination reason: Instruction limit
% 6.96/1.84 % (3962346)Termination phase: Saturation
% 6.96/1.84 % (3962346)Time elapsed: 0.083 s
% 6.96/1.84 % (3962346)Peak memory usage: 89 MB
% 6.96/1.84 % (3962346)Instructions burned: 115 (million)
% 6.96/1.84 % (3962356)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=2115728478:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 6.96/1.84 % (3962347)Instruction limit reached!
% 6.96/1.84 % (3962347)------------------------------
% 6.96/1.84 % (3962347)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.96/1.84 % (3962347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.96/1.84 % (3962347)CaDiCaL version: 2.1.3
% 6.96/1.84 % (3962347)Termination reason: Instruction limit
% 6.96/1.84 % (3962347)Termination phase: Saturation
% 6.96/1.84 % (3962347)Time elapsed: 0.134 s
% 6.96/1.84 % (3962347)Peak memory usage: 90 MB
% 6.96/1.84 % (3962347)Instructions burned: 181 (million)
% 6.96/1.84 % (3962356)Instruction limit reached!
% 6.96/1.84 % (3962356)------------------------------
% 6.96/1.84 % (3962356)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.96/1.84 % (3962356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.96/1.84 % (3962356)CaDiCaL version: 2.1.3
% 6.96/1.84 % (3962356)Termination reason: Instruction limit
% 6.96/1.84 % (3962356)Termination phase: Saturation
% 6.96/1.84 % (3962356)Time elapsed: 0.053 s
% 6.96/1.84 % (3962356)Peak memory usage: 90 MB
% 6.96/1.84 % (3962356)Instructions burned: 146 (million)
% 8.60/2.04 % (3962357)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2001961848:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 8.60/2.04 % (3962359)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=882614169:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 8.60/2.04 % (3962361)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=311377962:avsq=on:i=194:fgj=on:bd=preordered_2996 on theBenchmark for (2996ds/194Mi)
% 8.60/2.04 % (3962360)lrs+10_64_to=lpo:sil=8000:random_seed=2745679400:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 8.60/2.04 % (3962361)Instruction limit reached!
% 8.60/2.04 % (3962361)------------------------------
% 8.60/2.04 % (3962361)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.60/2.04 % (3962361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.60/2.04 % (3962361)CaDiCaL version: 2.1.3
% 8.60/2.04 % (3962361)Termination reason: Instruction limit
% 8.60/2.04 % (3962361)Termination phase: Saturation
% 8.60/2.04 % (3962361)Time elapsed: 0.068 s
% 8.60/2.04 % (3962361)Peak memory usage: 90 MB
% 8.60/2.04 % (3962361)Instructions burned: 195 (million)
% 8.60/2.04 % (3962357)Instruction limit reached!
% 8.60/2.04 % (3962357)------------------------------
% 8.60/2.04 % (3962357)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.60/2.04 % (3962357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.60/2.04 % (3962357)CaDiCaL version: 2.1.3
% 8.60/2.04 % (3962357)Termination reason: Instruction limit
% 8.60/2.04 % (3962357)Termination phase: Saturation
% 8.60/2.04 % (3962357)Time elapsed: 0.108 s
% 8.60/2.04 % (3962357)Peak memory usage: 91 MB
% 8.60/2.04 % (3962357)Instructions burned: 190 (million)
% 8.60/2.04 % (3962360)Instruction limit reached!
% 8.60/2.04 % (3962360)------------------------------
% 8.60/2.04 % (3962360)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.60/2.04 % (3962360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.60/2.04 % (3962360)CaDiCaL version: 2.1.3
% 8.60/2.04 % (3962360)Termination reason: Instruction limit
% 8.60/2.04 % (3962360)Termination phase: Saturation
% 8.60/2.04 % (3962360)Time elapsed: 0.080 s
% 8.60/2.04 % (3962360)Peak memory usage: 89 MB
% 8.60/2.04 % (3962360)Instructions burned: 126 (million)
% 8.60/2.04 % (3962359)Instruction limit reached!
% 8.60/2.04 % (3962359)------------------------------
% 8.60/2.04 % (3962359)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.60/2.04 % (3962359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.60/2.04 % (3962359)CaDiCaL version: 2.1.3
% 8.60/2.04 % (3962359)Termination reason: Instruction limit
% 8.60/2.04 % (3962359)Termination phase: Saturation
% 8.60/2.04 % (3962359)Time elapsed: 0.126 s
% 8.60/2.04 % (3962359)Peak memory usage: 90 MB
% 8.60/2.04 % (3962359)Instructions burned: 220 (million)
% 8.60/2.04 % (3962366)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=4061244182:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 8.60/2.04 % (3962367)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1899560826:i=3394:sd=4:ss=included:sgt=64_2995 on theBenchmark for (2995ds/3394Mi)
% 8.60/2.04 % (3962368)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=1746799980:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi)
% 8.60/2.04 % (3962366)Instruction limit reached!
% 8.60/2.04 % (3962366)------------------------------
% 8.60/2.04 % (3962366)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.60/2.04 % (3962366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.60/2.04 % (3962366)CaDiCaL version: 2.1.3
% 8.60/2.04 % (3962366)Termination reason: Instruction limit
% 8.60/2.04 % (3962366)Termination phase: Saturation
% 8.60/2.04 % (3962366)Time elapsed: 0.058 s
% 8.60/2.04 % (3962366)Peak memory usage: 91 MB
% 8.60/2.04 % (3962366)Instructions burned: 158 (million)
% 8.60/2.04 % (3962369)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1957735373:i=107_2994 on theBenchmark for (2994ds/107Mi)
% 8.60/2.04 % (3962368)Instruction limit reached!
% 8.60/2.04 % (3962368)------------------------------
% 8.60/2.04 % (3962368)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.60/2.04 % (3962368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.60/2.04 % (3962368)CaDiCaL version: 2.1.3
% 8.60/2.04 % (3962368)Termination reason: Instruction limit
% 8.60/2.04 % (3962368)Termination phase: Saturation
% 8.60/2.04 % (3962368)Time elapsed: 0.054 s
% 8.60/2.04 % (3962368)Peak memory usage: 89 MB
% 8.60/2.04 % (3962368)Instructions burned: 106 (million)
% 8.60/2.04 % (3962369)Instruction limit reached!
% 8.60/2.04 % (3962369)------------------------------
% 8.60/2.04 % (3962369)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.60/2.04 % (3962369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.60/2.04 % (3962369)CaDiCaL version: 2.1.3
% 8.60/2.04 % (3962369)Termination reason: Instruction limit
% 8.60/2.04 % (3962369)Termination phase: Saturation
% 8.60/2.04 % (3962369)Time elapsed: 0.067 s
% 8.60/2.04 % (3962369)Peak memory usage: 89 MB
% 8.60/2.04 % (3962369)Instructions burned: 108 (million)
% 8.60/2.04 % (3962373)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=4132380499:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2993 on theBenchmark for (2993ds/242Mi)
% 8.60/2.04 % (3962373)Instruction limit reached!
% 8.60/2.04 % (3962373)------------------------------
% 8.60/2.04 % (3962373)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.60/2.04 % (3962373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.60/2.04 % (3962373)CaDiCaL version: 2.1.3
% 8.60/2.04 % (3962373)Termination reason: Instruction limit
% 8.60/2.04 % (3962373)Termination phase: Saturation
% 8.60/2.04 % (3962373)Time elapsed: 0.084 s
% 8.60/2.04 % (3962373)Peak memory usage: 90 MB
% 8.60/2.04 % (3962373)Instructions burned: 242 (million)
% 8.60/2.04 % (3962375)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=1362625429:cond=fast:i=5208:av=off_2993 on theBenchmark for (2993ds/5208Mi)
% 8.60/2.04 % (3962376)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=218851337:i=134:sd=2:doe=on:ss=axioms:sgt=14_2992 on theBenchmark for (2992ds/134Mi)
% 8.60/2.04 % (3962379)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=4272569207:i=499:bd=all_2991 on theBenchmark for (2991ds/499Mi)
% 8.60/2.04 % (3962376)Instruction limit reached!
% 8.60/2.04 % (3962376)------------------------------
% 8.60/2.04 % (3962376)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.60/2.04 % (3962376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.60/2.04 % (3962376)CaDiCaL version: 2.1.3
% 8.60/2.04 % (3962376)Termination reason: Instruction limit
% 8.60/2.04 % (3962376)Termination phase: Saturation
% 8.60/2.04 % (3962376)Time elapsed: 0.077 s
% 8.60/2.04 % (3962376)Peak memory usage: 89 MB
% 8.60/2.04 % (3962376)Instructions burned: 135 (million)
% 8.60/2.04 % (3962382)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1431665367:i=191:fgj=on:bd=all_2990 on theBenchmark for (2990ds/191Mi)
% 8.60/2.04 % (3962379)Instruction limit reached!
% 8.60/2.04 % (3962379)------------------------------
% 8.60/2.04 % (3962379)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.60/2.04 % (3962379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.60/2.04 % (3962379)CaDiCaL version: 2.1.3
% 8.60/2.04 % (3962379)Termination reason: Instruction limit
% 8.60/2.04 % (3962379)Termination phase: Saturation
% 8.60/2.04 % (3962379)Time elapsed: 0.171 s
% 8.60/2.04 % (3962379)Peak memory usage: 93 MB
% 8.60/2.04 % (3962379)Instructions burned: 500 (million)
% 8.60/2.04 % (3962342)First to succeed.
% 8.60/2.04 % (3962342)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3962337"
% 8.60/2.04 % (3962384)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1986963697:i=264:kws=precedence:fsr=off_2989 on theBenchmark for (2989ds/264Mi)
% 8.60/2.04 % (3962382)Instruction limit reached!
% 8.60/2.04 % (3962382)------------------------------
% 8.60/2.04 % (3962382)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.60/2.04 % (3962382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.60/2.04 % (3962382)CaDiCaL version: 2.1.3
% 8.60/2.04 % (3962382)Termination reason: Instruction limit
% 8.60/2.04 % (3962382)Termination phase: Saturation
% 8.60/2.04 % (3962382)Time elapsed: 0.135 s
% 8.60/2.04 % (3962382)Peak memory usage: 91 MB
% 8.60/2.04 % (3962382)Instructions burned: 192 (million)
% 8.60/2.04 % (3962384)Instruction limit reached!
% 8.60/2.04 % (3962384)------------------------------
% 8.60/2.04 % (3962384)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.60/2.04 % (3962384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.60/2.04 % (3962384)CaDiCaL version: 2.1.3
% 8.60/2.04 % (3962384)Termination reason: Instruction limit
% 8.60/2.04 % (3962384)Termination phase: Saturation
% 8.60/2.04 % (3962384)Time elapsed: 0.093 s
% 8.60/2.04 % (3962384)Peak memory usage: 92 MB
% 8.60/2.04 % (3962384)Instructions burned: 267 (million)
% 8.60/2.04 % (3962386)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=2787980480:cond=on:i=156:bs=on:gtg=exists_all:er=known_2988 on theBenchmark for (2988ds/156Mi)
% 8.60/2.04 % (3962387)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=1736179030:i=3256:kws=precedence:bd=preordered:av=off_2987 on theBenchmark for (2987ds/3256Mi)
% 8.60/2.04 % (3962342)Refutation found. Thanks to Tanya!
% 8.60/2.04 % SZS status Unsatisfiable for theBenchmark
% 8.60/2.04 % SZS output start Proof for theBenchmark
% See solution above
% 10.24/2.24 % (3962342)------------------------------
% 10.24/2.24 % (3962342)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.24/2.24 % (3962342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.24/2.24 % (3962342)CaDiCaL version: 2.1.3
% 10.24/2.24 % (3962342)Termination reason: Refutation
% 10.24/2.24 % (3962342)Time elapsed: 0.944 s
% 10.24/2.24 % (3962342)Peak memory usage: 136 MB
% 10.24/2.24 % (3962342)Instructions burned: 1416 (million)
% 10.24/2.24 % (3962342)------------------------------
% 10.24/2.24 % (3962342)------------------------------
% 10.24/2.24 % (3962337)Success in time 1.374 s
% 10.24/2.24 % Vampire exiting
%------------------------------------------------------------------------------