%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ANA036-1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 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 09:30:58 AM UTC 2026
% Result : Unsatisfiable 62.14s 17.24s
% Output : Refutation 117.27s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 32
% Syntax : Number of formulae : 102 ( 25 unt; 6 def)
% Number of atoms : 288 ( 9 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 374 ( 188 ~; 180 |; 0 &)
% ( 6 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 5 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 19 ( 17 usr; 7 prp; 0-3 aty)
% Number of functors : 13 ( 13 usr; 4 con; 0-3 aty)
% Number of variables : 128 ( 0 sgn 128 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1434,axiom,
! [X0,X1] :
( ~ c_lessequals(c_0,X1,X0)
| ~ class_OrderedGroup_Olordered__ab__group__abs(X0)
| c_HOL_Oabs(X1,X0) = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_OrderedGroup_Oabs__of__nonneg_0) ).
fof(f2548,axiom,
! [X0] :
( ~ class_OrderedGroup_Olordered__ab__group__abs(X0)
| class_Orderings_Oorder(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsrel_OrderedGroup_Olordered__ab__group__abs_17) ).
fof(f2552,axiom,
! [X0] :
( ~ class_OrderedGroup_Olordered__ab__group__abs(X0)
| class_OrderedGroup_Ocomm__monoid__add(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsrel_OrderedGroup_Olordered__ab__group__abs_4) ).
fof(f2555,axiom,
! [X0] :
( ~ class_OrderedGroup_Olordered__ab__group__abs(X0)
| class_OrderedGroup_Opordered__cancel__ab__semigroup__add(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsrel_OrderedGroup_Olordered__ab__group__abs_7) ).
fof(f3011,axiom,
! [X0] :
( ~ class_Ring__and__Field_Oordered__idom(X0)
| class_Ring__and__Field_Osemiring(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsrel_Ring__and__Field_Oordered__idom_20) ).
fof(f3025,axiom,
! [X0] :
( ~ class_Ring__and__Field_Oordered__idom(X0)
| class_Orderings_Olinorder(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsrel_Ring__and__Field_Oordered__idom_33) ).
fof(f3035,axiom,
! [X0] :
( ~ class_Ring__and__Field_Oordered__idom(X0)
| class_Ring__and__Field_Opordered__semiring(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsrel_Ring__and__Field_Oordered__idom_42) ).
fof(f3036,axiom,
! [X0] :
( ~ class_Ring__and__Field_Oordered__idom(X0)
| class_OrderedGroup_Opordered__ab__semigroup__add(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsrel_Ring__and__Field_Oordered__idom_43) ).
fof(f3037,axiom,
! [X0] :
( ~ class_Ring__and__Field_Oordered__idom(X0)
| class_Orderings_Oorder(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsrel_Ring__and__Field_Oordered__idom_44) ).
fof(f3044,axiom,
! [X0] :
( ~ class_Ring__and__Field_Oordered__idom(X0)
| class_OrderedGroup_Olordered__ab__group__abs(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsrel_Ring__and__Field_Oordered__idom_50) ).
fof(f3362,axiom,
! [X2,X0,X1] :
( c_lessequals(c_HOL_Oabs(c_plus(X1,X2,X0),X0),c_plus(c_HOL_Oabs(X1,X0),c_HOL_Oabs(X2,X0),X0),X0)
| ~ class_OrderedGroup_Olordered__ab__group__abs(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_OrderedGroup_Oabs__triangle__ineq_0) ).
fof(f3363,axiom,
! [X2,X3,X0,X1,X4] :
( c_lessequals(c_plus(X3,X1,X0),c_plus(X4,X2,X0),X0)
| ~ c_lessequals(X1,X2,X0)
| ~ c_lessequals(X3,X4,X0)
| ~ class_OrderedGroup_Opordered__ab__semigroup__add(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_OrderedGroup_Oadd__mono_0) ).
fof(f3364,axiom,
! [X2,X0,X1] :
( c_lessequals(c_0,c_plus(X2,X1,X0),X0)
| ~ class_OrderedGroup_Opordered__cancel__ab__semigroup__add(X0)
| ~ c_lessequals(c_0,X1,X0)
| ~ c_lessequals(c_0,X2,X0)
| ~ class_OrderedGroup_Ocomm__monoid__add(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_OrderedGroup_Oadd__nonneg__nonneg_0) ).
fof(f3365,axiom,
! [X2,X0,X1] :
( c_lessequals(X1,c_Orderings_Omax(X1,X2,X0),X0)
| ~ class_Orderings_Olinorder(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Orderings_Ole__maxI1_0) ).
fof(f3366,axiom,
! [X2,X0,X1] :
( c_lessequals(X1,c_Orderings_Omax(X2,X1,X0),X0)
| ~ class_Orderings_Olinorder(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Orderings_Ole__maxI2_0) ).
fof(f3367,axiom,
! [X2,X3,X0,X1] :
( ~ c_lessequals(X3,X1,X0)
| ~ c_lessequals(X1,X2,X0)
| ~ class_Orderings_Oorder(X0)
| c_lessequals(X3,X2,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Orderings_Oorder__class_Oorder__trans_0) ).
fof(f3368,axiom,
! [X2,X3,X0,X1] :
( ~ c_less(X1,X2,X0)
| ~ class_Orderings_Oorder(X0)
| ~ c_lessequals(X2,X3,X0)
| c_less(X1,X3,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Orderings_Oorder__less__le__trans_0) ).
fof(f3369,axiom,
! [X2,X3,X0,X1] :
( c_lessequals(c_times(X1,X3,X0),c_times(X2,X3,X0),X0)
| ~ c_lessequals(X1,X2,X0)
| ~ c_lessequals(c_0,X3,X0)
| ~ class_Ring__and__Field_Opordered__semiring(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Ring__and__Field_Opordered__semiring__class_Omult__right__mono_0) ).
fof(f3370,axiom,
! [X2,X3,X0,X1] :
( ~ class_Ring__and__Field_Osemiring(X0)
| c_times(X1,c_plus(X2,X3,X0),X0) = c_plus(c_times(X1,X2,X0),c_times(X1,X3,X0),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Ring__and__Field_Oring__distrib__1_0) ).
fof(f3374,negated_conjecture,
! [X0] : c_lessequals(c_0,v_f(X0),t_b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f3375,negated_conjecture,
! [X0] : c_lessequals(c_0,v_g(X0),t_b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_1) ).
fof(f3377,negated_conjecture,
! [X0] : c_lessequals(c_HOL_Oabs(v_a(X0),t_b),c_times(v_c,v_f(X0),t_b),t_b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_3) ).
fof(f3378,negated_conjecture,
c_less(c_0,v_ca,t_b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_4) ).
fof(f3379,negated_conjecture,
! [X0] : c_lessequals(c_HOL_Oabs(v_b(X0),t_b),c_times(v_ca,v_g(X0),t_b),t_b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_5) ).
fof(f3380,negated_conjecture,
! [X0] :
( ~ c_lessequals(c_HOL_Oabs(c_plus(v_a(v_xa(X0)),v_b(v_xa(X0)),t_b),t_b),c_times(X0,c_HOL_Oabs(c_plus(v_f(v_xa(X0)),v_g(v_xa(X0)),t_b),t_b),t_b),t_b)
| ~ c_less(c_0,X0,t_b) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_6) ).
fof(f3381,negated_conjecture,
class_Ring__and__Field_Oordered__idom(t_b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tfree_tcs) ).
fof(f3385,plain,
! [X0,X1] :
( ~ c_lessequals(c_times(v_ca,v_g(X0),t_b),X1,t_b)
| ~ class_Orderings_Oorder(t_b)
| c_lessequals(c_HOL_Oabs(v_b(X0),t_b),X1,t_b) ),
inference(resolution,[],[f3367,f3379]) ).
fof(f3386,plain,
! [X0,X1] :
( ~ c_lessequals(c_times(v_c,v_f(X0),t_b),X1,t_b)
| ~ class_Orderings_Oorder(t_b)
| c_lessequals(c_HOL_Oabs(v_a(X0),t_b),X1,t_b) ),
inference(resolution,[],[f3367,f3377]) ).
fof(f3388,plain,
! [X2,X3,X0,X1] :
( ~ c_lessequals(c_plus(c_HOL_Oabs(X0,X1),c_HOL_Oabs(X2,X1),X1),X3,X1)
| ~ class_Orderings_Oorder(X1)
| c_lessequals(c_HOL_Oabs(c_plus(X0,X2,X1),X1),X3,X1)
| ~ class_OrderedGroup_Olordered__ab__group__abs(X1) ),
inference(resolution,[],[f3367,f3362]) ).
fof(f3389,plain,
! [X2,X3,X0,X1] :
( ~ c_lessequals(c_plus(c_HOL_Oabs(X0,X1),c_HOL_Oabs(X2,X1),X1),X3,X1)
| c_lessequals(c_HOL_Oabs(c_plus(X0,X2,X1),X1),X3,X1)
| ~ class_OrderedGroup_Olordered__ab__group__abs(X1) ),
inference(forward_subsumption_resolution,[],[f3388,f2548]) ).
fof(f3392,definition,
( spl0_1
<=> class_Orderings_Oorder(t_b) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f3393,plain,
( class_Orderings_Oorder(t_b)
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f3392]) ).
fof(f3394,plain,
( ~ class_Orderings_Oorder(t_b)
| spl0_1 ),
inference(avatar_component_clause,[],[f3392]) ).
fof(f3396,definition,
( spl0_2
<=> ! [X0,X1] :
( ~ c_lessequals(c_times(v_c,v_f(X0),t_b),X1,t_b)
| c_lessequals(c_HOL_Oabs(v_a(X0),t_b),X1,t_b) ) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f3397,plain,
( ! [X0,X1] :
( ~ c_lessequals(c_times(v_c,v_f(X0),t_b),X1,t_b)
| c_lessequals(c_HOL_Oabs(v_a(X0),t_b),X1,t_b) )
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f3396]) ).
fof(f3398,plain,
( ~ spl0_1
| spl0_2 ),
inference(avatar_split_clause,[],[f3386,f3396,f3392]) ).
fof(f3400,definition,
( spl0_3
<=> ! [X0,X1] :
( ~ c_lessequals(c_times(v_ca,v_g(X0),t_b),X1,t_b)
| c_lessequals(c_HOL_Oabs(v_b(X0),t_b),X1,t_b) ) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f3401,plain,
( ! [X0,X1] :
( ~ c_lessequals(c_times(v_ca,v_g(X0),t_b),X1,t_b)
| c_lessequals(c_HOL_Oabs(v_b(X0),t_b),X1,t_b) )
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f3400]) ).
fof(f3402,plain,
( ~ spl0_1
| spl0_3 ),
inference(avatar_split_clause,[],[f3385,f3400,f3392]) ).
fof(f3411,plain,
! [X0] :
( ~ class_Orderings_Oorder(t_b)
| ~ c_lessequals(v_ca,X0,t_b)
| c_less(c_0,X0,t_b) ),
inference(resolution,[],[f3368,f3378]) ).
fof(f3419,definition,
( spl0_7
<=> class_OrderedGroup_Olordered__ab__group__abs(t_b) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f3420,plain,
( class_OrderedGroup_Olordered__ab__group__abs(t_b)
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f3419]) ).
fof(f3421,plain,
( ~ class_OrderedGroup_Olordered__ab__group__abs(t_b)
| spl0_7 ),
inference(avatar_component_clause,[],[f3419]) ).
fof(f3427,plain,
class_OrderedGroup_Olordered__ab__group__abs(t_b),
inference(resolution,[],[f3044,f3381]) ).
fof(f3428,plain,
( $false
| spl0_7 ),
inference(forward_subsumption_resolution,[],[f3427,f3421]) ).
fof(f3429,plain,
spl0_7,
inference(avatar_contradiction_clause,[],[f3428]) ).
fof(f3460,plain,
! [X2,X0,X1] :
( ~ class_OrderedGroup_Opordered__cancel__ab__semigroup__add(X0)
| ~ c_lessequals(c_0,X1,X0)
| ~ c_lessequals(c_0,X2,X0)
| ~ class_OrderedGroup_Ocomm__monoid__add(X0)
| ~ class_OrderedGroup_Olordered__ab__group__abs(X0)
| c_plus(X2,X1,X0) = c_HOL_Oabs(c_plus(X2,X1,X0),X0) ),
inference(resolution,[],[f3364,f1434]) ).
fof(f3463,plain,
! [X2,X0,X1] :
( ~ c_lessequals(c_0,X1,X0)
| ~ c_lessequals(c_0,X2,X0)
| ~ class_OrderedGroup_Ocomm__monoid__add(X0)
| ~ class_OrderedGroup_Olordered__ab__group__abs(X0)
| c_plus(X2,X1,X0) = c_HOL_Oabs(c_plus(X2,X1,X0),X0) ),
inference(forward_subsumption_resolution,[],[f3460,f2555]) ).
fof(f3464,plain,
! [X2,X0,X1] :
( ~ c_lessequals(c_0,X2,X0)
| ~ c_lessequals(c_0,X1,X0)
| ~ class_OrderedGroup_Olordered__ab__group__abs(X0)
| c_plus(X2,X1,X0) = c_HOL_Oabs(c_plus(X2,X1,X0),X0) ),
inference(forward_subsumption_resolution,[],[f3463,f2552]) ).
fof(f3465,plain,
class_Orderings_Olinorder(t_b),
inference(resolution,[],[f3025,f3381]) ).
fof(f3471,definition,
( spl0_9
<=> class_Ring__and__Field_Opordered__semiring(t_b) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f3472,plain,
( class_Ring__and__Field_Opordered__semiring(t_b)
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f3471]) ).
fof(f3473,plain,
( ~ class_Ring__and__Field_Opordered__semiring(t_b)
| spl0_9 ),
inference(avatar_component_clause,[],[f3471]) ).
fof(f3491,plain,
class_Orderings_Oorder(t_b),
inference(resolution,[],[f3037,f3381]) ).
fof(f3492,plain,
( $false
| spl0_1 ),
inference(forward_subsumption_resolution,[],[f3491,f3394]) ).
fof(f3493,plain,
spl0_1,
inference(avatar_contradiction_clause,[],[f3492]) ).
fof(f3495,plain,
( ! [X0] :
( ~ c_lessequals(v_ca,X0,t_b)
| c_less(c_0,X0,t_b) )
| ~ spl0_1 ),
inference(forward_subsumption_resolution,[],[f3411,f3393]) ).
fof(f3496,plain,
( ! [X0,X1] :
( c_lessequals(c_HOL_Oabs(v_b(X0),t_b),c_times(X1,v_g(X0),t_b),t_b)
| ~ c_lessequals(v_ca,X1,t_b)
| ~ c_lessequals(c_0,v_g(X0),t_b)
| ~ class_Ring__and__Field_Opordered__semiring(t_b) )
| ~ spl0_3 ),
inference(resolution,[],[f3401,f3369]) ).
fof(f3497,plain,
( ! [X0,X1] :
( c_lessequals(c_HOL_Oabs(v_a(X0),t_b),c_times(X1,v_f(X0),t_b),t_b)
| ~ c_lessequals(v_c,X1,t_b)
| ~ c_lessequals(c_0,v_f(X0),t_b)
| ~ class_Ring__and__Field_Opordered__semiring(t_b) )
| ~ spl0_2 ),
inference(resolution,[],[f3397,f3369]) ).
fof(f3535,definition,
( spl0_16
<=> class_OrderedGroup_Opordered__ab__semigroup__add(t_b) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f3536,plain,
( class_OrderedGroup_Opordered__ab__semigroup__add(t_b)
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f3535]) ).
fof(f3537,plain,
( ~ class_OrderedGroup_Opordered__ab__semigroup__add(t_b)
| spl0_16 ),
inference(avatar_component_clause,[],[f3535]) ).
fof(f3548,plain,
class_Ring__and__Field_Osemiring(t_b),
inference(resolution,[],[f3011,f3381]) ).
fof(f3587,plain,
class_OrderedGroup_Opordered__ab__semigroup__add(t_b),
inference(resolution,[],[f3036,f3381]) ).
fof(f3588,plain,
( $false
| spl0_16 ),
inference(forward_subsumption_resolution,[],[f3587,f3537]) ).
fof(f3589,plain,
spl0_16,
inference(avatar_contradiction_clause,[],[f3588]) ).
fof(f3672,plain,
! [X0,X1] :
( ~ c_lessequals(c_0,X0,t_b)
| ~ class_OrderedGroup_Olordered__ab__group__abs(t_b)
| c_plus(v_f(X1),X0,t_b) = c_HOL_Oabs(c_plus(v_f(X1),X0,t_b),t_b) ),
inference(resolution,[],[f3464,f3374]) ).
fof(f3683,plain,
( ! [X0,X1] :
( ~ c_lessequals(c_0,X0,t_b)
| c_plus(v_f(X1),X0,t_b) = c_HOL_Oabs(c_plus(v_f(X1),X0,t_b),t_b) )
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f3672,f3420]) ).
fof(f3696,plain,
( ! [X0,X1] : c_plus(v_f(X0),v_g(X1),t_b) = c_HOL_Oabs(c_plus(v_f(X0),v_g(X1),t_b),t_b)
| ~ spl0_7 ),
inference(resolution,[],[f3683,f3375]) ).
fof(f3827,plain,
( ! [X0] :
( ~ c_lessequals(c_HOL_Oabs(c_plus(v_a(v_xa(X0)),v_b(v_xa(X0)),t_b),t_b),c_times(X0,c_plus(v_f(v_xa(X0)),v_g(v_xa(X0)),t_b),t_b),t_b)
| ~ c_less(c_0,X0,t_b) )
| ~ spl0_7 ),
inference(superposition,[],[f3380,f3696]) ).
fof(f3898,plain,
! [X2,X0,X1] : c_times(X0,c_plus(X1,X2,t_b),t_b) = c_plus(c_times(X0,X1,t_b),c_times(X0,X2,t_b),t_b),
inference(resolution,[],[f3370,f3548]) ).
fof(f3909,plain,
! [X2,X3,X0,X1,X4] :
( c_lessequals(c_plus(X3,X4,t_b),c_times(X0,c_plus(X1,X2,t_b),t_b),t_b)
| ~ c_lessequals(X4,c_times(X0,X2,t_b),t_b)
| ~ c_lessequals(X3,c_times(X0,X1,t_b),t_b)
| ~ class_OrderedGroup_Opordered__ab__semigroup__add(t_b) ),
inference(superposition,[],[f3363,f3898]) ).
fof(f3914,plain,
( ! [X2,X3,X0,X1,X4] :
( c_lessequals(c_plus(X3,X4,t_b),c_times(X0,c_plus(X1,X2,t_b),t_b),t_b)
| ~ c_lessequals(X4,c_times(X0,X2,t_b),t_b)
| ~ c_lessequals(X3,c_times(X0,X1,t_b),t_b) )
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f3909,f3536]) ).
fof(f3918,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ c_lessequals(c_HOL_Oabs(X0,t_b),c_times(X1,X2,t_b),t_b)
| ~ c_lessequals(c_HOL_Oabs(X3,t_b),c_times(X1,X4,t_b),t_b)
| c_lessequals(c_HOL_Oabs(c_plus(X3,X0,t_b),t_b),c_times(X1,c_plus(X4,X2,t_b),t_b),t_b)
| ~ class_OrderedGroup_Olordered__ab__group__abs(t_b) )
| ~ spl0_16 ),
inference(resolution,[],[f3914,f3389]) ).
fof(f3931,plain,
( ! [X2,X3,X0,X1,X4] :
( c_lessequals(c_HOL_Oabs(c_plus(X3,X0,t_b),t_b),c_times(X1,c_plus(X4,X2,t_b),t_b),t_b)
| ~ c_lessequals(c_HOL_Oabs(X3,t_b),c_times(X1,X4,t_b),t_b)
| ~ c_lessequals(c_HOL_Oabs(X0,t_b),c_times(X1,X2,t_b),t_b) )
| ~ spl0_7
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f3918,f3420]) ).
fof(f3933,plain,
( ! [X0] :
( ~ c_lessequals(c_HOL_Oabs(v_b(v_xa(X0)),t_b),c_times(X0,v_g(v_xa(X0)),t_b),t_b)
| ~ c_lessequals(c_HOL_Oabs(v_a(v_xa(X0)),t_b),c_times(X0,v_f(v_xa(X0)),t_b),t_b)
| ~ c_less(c_0,X0,t_b) )
| ~ spl0_7
| ~ spl0_16 ),
inference(resolution,[],[f3931,f3827]) ).
fof(f4259,plain,
class_Ring__and__Field_Opordered__semiring(t_b),
inference(resolution,[],[f3035,f3381]) ).
fof(f4260,plain,
( $false
| spl0_9 ),
inference(forward_subsumption_resolution,[],[f4259,f3473]) ).
fof(f4261,plain,
spl0_9,
inference(avatar_contradiction_clause,[],[f4260]) ).
fof(f4262,plain,
( ! [X0,X1] :
( c_lessequals(c_HOL_Oabs(v_b(X0),t_b),c_times(X1,v_g(X0),t_b),t_b)
| ~ c_lessequals(v_ca,X1,t_b)
| ~ c_lessequals(c_0,v_g(X0),t_b) )
| ~ spl0_3
| ~ spl0_9 ),
inference(forward_subsumption_resolution,[],[f3496,f3472]) ).
fof(f4263,plain,
( ! [X0,X1] :
( c_lessequals(c_HOL_Oabs(v_a(X0),t_b),c_times(X1,v_f(X0),t_b),t_b)
| ~ c_lessequals(v_c,X1,t_b)
| ~ c_lessequals(c_0,v_f(X0),t_b) )
| ~ spl0_2
| ~ spl0_9 ),
inference(forward_subsumption_resolution,[],[f3497,f3472]) ).
fof(f4272,plain,
( ! [X0,X1] :
( c_lessequals(c_HOL_Oabs(v_b(X0),t_b),c_times(X1,v_g(X0),t_b),t_b)
| ~ c_lessequals(v_ca,X1,t_b) )
| ~ spl0_3
| ~ spl0_9 ),
inference(forward_subsumption_resolution,[],[f4262,f3375]) ).
fof(f4273,plain,
( ! [X0,X1] :
( c_lessequals(c_HOL_Oabs(v_a(X0),t_b),c_times(X1,v_f(X0),t_b),t_b)
| ~ c_lessequals(v_c,X1,t_b) )
| ~ spl0_2
| ~ spl0_9 ),
inference(forward_subsumption_resolution,[],[f4263,f3374]) ).
fof(f4276,plain,
( ! [X0] :
( ~ c_lessequals(v_ca,X0,t_b)
| ~ c_lessequals(c_HOL_Oabs(v_a(v_xa(X0)),t_b),c_times(X0,v_f(v_xa(X0)),t_b),t_b)
| ~ c_less(c_0,X0,t_b) )
| ~ spl0_3
| ~ spl0_7
| ~ spl0_9
| ~ spl0_16 ),
inference(resolution,[],[f4272,f3933]) ).
fof(f4291,plain,
( ! [X0] :
( ~ c_lessequals(c_HOL_Oabs(v_a(v_xa(X0)),t_b),c_times(X0,v_f(v_xa(X0)),t_b),t_b)
| ~ c_lessequals(v_ca,X0,t_b) )
| ~ spl0_1
| ~ spl0_3
| ~ spl0_7
| ~ spl0_9
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f4276,f3495]) ).
fof(f4308,plain,
( ! [X0] :
( ~ c_lessequals(v_ca,X0,t_b)
| ~ c_lessequals(v_c,X0,t_b) )
| ~ spl0_1
| ~ spl0_2
| ~ spl0_3
| ~ spl0_7
| ~ spl0_9
| ~ spl0_16 ),
inference(resolution,[],[f4291,f4273]) ).
fof(f4311,plain,
( ! [X0] :
( ~ c_lessequals(v_c,c_Orderings_Omax(v_ca,X0,t_b),t_b)
| ~ class_Orderings_Olinorder(t_b) )
| ~ spl0_1
| ~ spl0_2
| ~ spl0_3
| ~ spl0_7
| ~ spl0_9
| ~ spl0_16 ),
inference(resolution,[],[f4308,f3365]) ).
fof(f4315,plain,
( ! [X0] : ~ c_lessequals(v_c,c_Orderings_Omax(v_ca,X0,t_b),t_b)
| ~ spl0_1
| ~ spl0_2
| ~ spl0_3
| ~ spl0_7
| ~ spl0_9
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f4311,f3465]) ).
fof(f4759,plain,
( ~ class_Orderings_Olinorder(t_b)
| ~ spl0_1
| ~ spl0_2
| ~ spl0_3
| ~ spl0_7
| ~ spl0_9
| ~ spl0_16 ),
inference(resolution,[],[f4315,f3366]) ).
fof(f4760,plain,
( $false
| ~ spl0_1
| ~ spl0_2
| ~ spl0_3
| ~ spl0_7
| ~ spl0_9
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f4759,f3465]) ).
fof(f4761,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_3
| ~ spl0_7
| ~ spl0_9
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f4760]) ).
cnf(s1,plain,
( ~ spl0_1
| spl0_2 ),
inference(sat_conversion,[],[f3398]) ).
cnf(s2,plain,
( ~ spl0_1
| spl0_3 ),
inference(sat_conversion,[],[f3402]) ).
cnf(s7,plain,
spl0_7,
inference(sat_conversion,[],[f3429]) ).
cnf(s11,plain,
spl0_1,
inference(sat_conversion,[],[f3493]) ).
cnf(s15,plain,
spl0_16,
inference(sat_conversion,[],[f3589]) ).
cnf(s19,plain,
spl0_9,
inference(sat_conversion,[],[f4261]) ).
cnf(s31,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_3
| ~ spl0_7
| ~ spl0_9
| ~ spl0_16 ),
inference(sat_conversion,[],[f4761]) ).
cnf(s42,plain,
spl0_3,
inference(rat,[],[s2,s11]) ).
cnf(s43,plain,
~ spl0_2,
inference(rat,[],[s31,s15,s19,s7,s11,s42]) ).
cnf(s44,plain,
$false,
inference(rat,[],[s1,s43,s11]) ).
fof(f4762,plain,
$false,
inference(avatar_sat_refutation,[],[s44]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ANA036-1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.20 % Computer : n026.cluster.edu
% 0.08/0.20 % Model : x86_64 x86_64
% 0.08/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.20 % Memory : 8046.5625MB
% 0.08/0.20 % OS : Linux 6.8.0-71-generic
% 0.08/0.20 % CPULimit : 300
% 0.08/0.20 % WCLimit : 300
% 0.08/0.20 % DateTime : Mon Sep 28 20:36:12 UTC 2026
% 0.08/0.20 % CPUTime :
% 0.08/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.23 Running first-order theorem proving
% 0.08/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 9.51/2.06 % (16673)Input is clausal, will run a generic CNF schedule.
% 9.51/2.06 % (16684)dis-21_1_sil=8000:lcm=predicate:random_seed=1657386519: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)
% 9.51/2.06 % (16684)Instruction limit reached!
% 9.51/2.06 % (16684)------------------------------
% 9.51/2.06 % (16684)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.51/2.06 % (16684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.51/2.06 % (16684)CaDiCaL version: 2.1.3
% 9.51/2.06 % (16684)Termination reason: Instruction limit
% 9.51/2.06 % (16684)Termination phase: Saturation
% 9.51/2.06 % (16684)Time elapsed: 0.034 s
% 9.51/2.06 % (16684)Peak memory usage: 90 MB
% 9.51/2.06 % (16684)Instructions burned: 118 (million)
% 9.51/2.06 % (16682)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=4156573542:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 9.51/2.06 % (16681)lrs+10_1_sil=8000:sp=occurrence:random_seed=3311564985:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 9.51/2.06 % (16679)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1318838913:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 9.51/2.06 % (16683)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2327726587:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 9.51/2.06 % (16680)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=4194854048:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 9.51/2.06 % (16678)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=1039852184:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 9.51/2.06 % (16682)Instruction limit reached!
% 9.51/2.06 % (16682)------------------------------
% 9.51/2.06 % (16682)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.51/2.06 % (16682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.51/2.06 % (16682)CaDiCaL version: 2.1.3
% 9.51/2.06 % (16682)Termination reason: Instruction limit
% 9.51/2.06 % (16682)Termination phase: Saturation
% 9.51/2.06 % (16682)Time elapsed: 0.070 s
% 9.51/2.06 % (16682)Peak memory usage: 90 MB
% 9.51/2.06 % (16682)Instructions burned: 114 (million)
% 9.51/2.06 % (16681)Instruction limit reached!
% 9.51/2.06 % (16681)------------------------------
% 9.51/2.06 % (16681)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.51/2.06 % (16681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.51/2.06 % (16681)CaDiCaL version: 2.1.3
% 9.51/2.06 % (16681)Termination reason: Instruction limit
% 9.51/2.06 % (16681)Termination phase: Saturation
% 9.51/2.06 % (16681)Time elapsed: 0.075 s
% 9.51/2.06 % (16681)Peak memory usage: 91 MB
% 9.51/2.06 % (16681)Instructions burned: 108 (million)
% 9.51/2.06 % (16686)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=1486017989:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 9.51/2.06 % (16686)Refutation not found, incomplete strategy
% 9.51/2.06 % (16686)------------------------------
% 9.51/2.06 % (16686)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.51/2.06 % (16686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.51/2.06 % (16686)CaDiCaL version: 2.1.3
% 9.51/2.06 % (16686)Termination reason: Refutation not found, incomplete strategy
% 9.51/2.06 % (16686)Time elapsed: 0.009 s
% 9.51/2.06 % (16686)Peak memory usage: 90 MB
% 9.51/2.06 % (16686)Instructions burned: 23 (million)
% 9.51/2.06 % (16683)Instruction limit reached!
% 9.51/2.06 % (16683)------------------------------
% 9.51/2.06 % (16683)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.51/2.06 % (16683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.51/2.06 % (16683)CaDiCaL version: 2.1.3
% 9.51/2.06 % (16683)Termination reason: Instruction limit
% 9.51/2.06 % (16683)Termination phase: Saturation
% 9.51/2.06 % (16683)Time elapsed: 0.114 s
% 9.51/2.06 % (16683)Peak memory usage: 90 MB
% 9.51/2.06 % (16683)Instructions burned: 181 (million)
% 9.51/2.06 % (16693)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3064810784:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2996 on theBenchmark for (2996ds/189Mi)
% 18.40/3.40 % (16694)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3388483222:st=4:i=219:sd=3:ss=axioms_2996 on theBenchmark for (2996ds/219Mi)
% 18.40/3.40 % (16686)------------------------------
% 18.40/3.40 % (16686)------------------------------
% 18.40/3.40 % (16696)lrs+10_64_to=lpo:sil=8000:random_seed=928280894:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 18.40/3.40 % (16693)Instruction limit reached!
% 18.40/3.40 % (16693)------------------------------
% 18.40/3.40 % (16693)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.40/3.40 % (16693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.40/3.40 % (16693)CaDiCaL version: 2.1.3
% 18.40/3.40 % (16693)Termination reason: Instruction limit
% 18.40/3.40 % (16693)Termination phase: Saturation
% 18.40/3.40 % (16693)Time elapsed: 0.115 s
% 18.40/3.40 % (16693)Peak memory usage: 93 MB
% 18.40/3.40 % (16693)Instructions burned: 190 (million)
% 18.40/3.40 % (16696)Instruction limit reached!
% 18.40/3.40 % (16696)------------------------------
% 18.40/3.40 % (16696)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.40/3.40 % (16696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.40/3.40 % (16696)CaDiCaL version: 2.1.3
% 18.40/3.40 % (16696)Termination reason: Instruction limit
% 18.40/3.40 % (16696)Termination phase: Saturation
% 18.40/3.40 % (16696)Time elapsed: 0.072 s
% 18.40/3.40 % (16696)Peak memory usage: 92 MB
% 18.40/3.40 % (16696)Instructions burned: 126 (million)
% 18.40/3.40 % (16700)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=345814260:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 18.40/3.40 % (16694)Instruction limit reached!
% 18.40/3.40 % (16694)------------------------------
% 18.40/3.40 % (16694)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.40/3.40 % (16694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.40/3.40 % (16694)CaDiCaL version: 2.1.3
% 18.40/3.40 % (16694)Termination reason: Instruction limit
% 18.40/3.40 % (16694)Termination phase: Saturation
% 18.40/3.40 % (16694)Time elapsed: 0.142 s
% 18.40/3.40 % (16694)Peak memory usage: 92 MB
% 18.40/3.40 % (16694)Instructions burned: 220 (million)
% 18.40/3.40 % (16700)Instruction limit reached!
% 18.40/3.40 % (16700)------------------------------
% 18.40/3.40 % (16700)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.40/3.40 % (16700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.40/3.40 % (16700)CaDiCaL version: 2.1.3
% 18.40/3.40 % (16700)Termination reason: Instruction limit
% 18.40/3.40 % (16700)Termination phase: Saturation
% 18.40/3.40 % (16700)Time elapsed: 0.061 s
% 18.40/3.40 % (16700)Peak memory usage: 92 MB
% 18.40/3.40 % (16700)Instructions burned: 197 (million)
% 18.40/3.40 % (16701)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=5709243:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 18.40/3.40 % (16702)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3793411723:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 18.40/3.40 % (16705)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1833973911:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 18.40/3.40 % (16704)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=1485704907:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi)
% 18.40/3.40 % (16705)Instruction limit reached!
% 18.40/3.40 % (16705)------------------------------
% 18.40/3.40 % (16705)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.40/3.40 % (16705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.40/3.40 % (16705)CaDiCaL version: 2.1.3
% 18.40/3.40 % (16705)Termination reason: Instruction limit
% 18.40/3.40 % (16705)Termination phase: Saturation
% 18.40/3.40 % (16705)Time elapsed: 0.035 s
% 18.40/3.40 % (16705)Peak memory usage: 92 MB
% 18.40/3.40 % (16705)Instructions burned: 108 (million)
% 18.40/3.40 % (16701)Instruction limit reached!
% 18.40/3.40 % (16701)------------------------------
% 18.40/3.40 % (16701)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.40/3.40 % (16701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.40/3.40 % (16701)CaDiCaL version: 2.1.3
% 33.40/5.44 % (16701)Termination reason: Instruction limit
% 33.40/5.44 % (16701)Termination phase: Saturation
% 33.40/5.44 % (16701)Time elapsed: 0.082 s
% 33.40/5.44 % (16701)Peak memory usage: 92 MB
% 33.40/5.44 % (16701)Instructions burned: 157 (million)
% 33.40/5.44 % (16704)Instruction limit reached!
% 33.40/5.44 % (16704)------------------------------
% 33.40/5.44 % (16704)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.40/5.44 % (16704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.40/5.44 % (16704)CaDiCaL version: 2.1.3
% 33.40/5.44 % (16704)Termination reason: Instruction limit
% 33.40/5.44 % (16704)Termination phase: Saturation
% 33.40/5.44 % (16704)Time elapsed: 0.058 s
% 33.40/5.44 % (16704)Peak memory usage: 90 MB
% 33.40/5.44 % (16704)Instructions burned: 107 (million)
% 33.40/5.44 % (16710)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=2451618271:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi)
% 33.40/5.44 % (16711)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=4288553806:cond=fast:i=5208:av=off_2992 on theBenchmark for (2992ds/5208Mi)
% 33.40/5.44 % (16712)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=247236805:i=134:sd=2:doe=on:ss=axioms:sgt=14_2992 on theBenchmark for (2992ds/134Mi)
% 33.40/5.44 % (16710)Instruction limit reached!
% 33.40/5.44 % (16710)------------------------------
% 33.40/5.44 % (16710)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.40/5.44 % (16710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.40/5.44 % (16710)CaDiCaL version: 2.1.3
% 33.40/5.44 % (16710)Termination reason: Instruction limit
% 33.40/5.44 % (16710)Termination phase: Saturation
% 33.40/5.44 % (16710)Time elapsed: 0.124 s
% 33.40/5.44 % (16710)Peak memory usage: 91 MB
% 33.40/5.44 % (16710)Instructions burned: 244 (million)
% 33.40/5.44 % (16712)Instruction limit reached!
% 33.40/5.44 % (16712)------------------------------
% 33.40/5.44 % (16712)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.40/5.44 % (16712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.40/5.44 % (16712)CaDiCaL version: 2.1.3
% 33.40/5.44 % (16712)Termination reason: Instruction limit
% 33.40/5.44 % (16712)Termination phase: Saturation
% 33.40/5.44 % (16712)Time elapsed: 0.093 s
% 33.40/5.44 % (16712)Peak memory usage: 91 MB
% 33.40/5.44 % (16712)Instructions burned: 134 (million)
% 33.40/5.44 % (16716)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2061828349:i=499:bd=all_2990 on theBenchmark for (2990ds/499Mi)
% 33.40/5.44 % (16717)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=2646332002:i=191:fgj=on:bd=all_2989 on theBenchmark for (2989ds/191Mi)
% 33.40/5.44 % (16716)Instruction limit reached!
% 33.40/5.44 % (16716)------------------------------
% 33.40/5.44 % (16716)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.40/5.44 % (16716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.40/5.44 % (16716)CaDiCaL version: 2.1.3
% 33.40/5.44 % (16716)Termination reason: Instruction limit
% 33.40/5.44 % (16716)Termination phase: Saturation
% 33.40/5.44 % (16716)Time elapsed: 0.181 s
% 33.40/5.44 % (16716)Peak memory usage: 99 MB
% 33.40/5.44 % (16716)Instructions burned: 499 (million)
% 33.40/5.44 % (16717)Instruction limit reached!
% 33.40/5.44 % (16717)------------------------------
% 33.40/5.44 % (16717)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.40/5.44 % (16717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.40/5.44 % (16717)CaDiCaL version: 2.1.3
% 33.40/5.44 % (16717)Termination reason: Instruction limit
% 33.40/5.44 % (16717)Termination phase: Saturation
% 33.40/5.44 % (16717)Time elapsed: 0.113 s
% 33.40/5.44 % (16717)Peak memory usage: 92 MB
% 33.40/5.44 % (16717)Instructions burned: 191 (million)
% 33.40/5.44 % (16720)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=782066773:i=264:kws=precedence:fsr=off_2987 on theBenchmark for (2987ds/264Mi)
% 33.40/5.44 % (16721)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=1042083963:cond=on:i=156:bs=on:gtg=exists_all:er=known_2987 on theBenchmark for (2987ds/156Mi)
% 33.40/5.44 % (16720)Instruction limit reached!
% 33.40/5.44 % (16720)------------------------------
% 33.40/5.44 % (16720)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.95/7.62 % (16720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.95/7.62 % (16720)CaDiCaL version: 2.1.3
% 48.95/7.62 % (16720)Termination reason: Instruction limit
% 48.95/7.62 % (16720)Termination phase: Saturation
% 48.95/7.62 % (16720)Time elapsed: 0.064 s
% 48.95/7.62 % (16720)Peak memory usage: 94 MB
% 48.95/7.62 % (16720)Instructions burned: 267 (million)
% 48.95/7.62 % (16721)Instruction limit reached!
% 48.95/7.62 % (16721)------------------------------
% 48.95/7.62 % (16721)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.95/7.62 % (16721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.95/7.62 % (16721)CaDiCaL version: 2.1.3
% 48.95/7.62 % (16721)Termination reason: Instruction limit
% 48.95/7.62 % (16721)Termination phase: Saturation
% 48.95/7.62 % (16721)Time elapsed: 0.084 s
% 48.95/7.62 % (16721)Peak memory usage: 91 MB
% 48.95/7.62 % (16721)Instructions burned: 157 (million)
% 48.95/7.62 % (16724)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=2773262595:i=3256:kws=precedence:bd=preordered:av=off_2986 on theBenchmark for (2986ds/3256Mi)
% 48.95/7.62 % (16725)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=299980518:i=537:av=off:ss=included_2985 on theBenchmark for (2985ds/537Mi)
% 48.95/7.62 % (16725)Instruction limit reached!
% 48.95/7.62 % (16725)------------------------------
% 48.95/7.62 % (16725)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.95/7.62 % (16725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.95/7.62 % (16725)CaDiCaL version: 2.1.3
% 48.95/7.62 % (16725)Termination reason: Instruction limit
% 48.95/7.62 % (16725)Termination phase: Saturation
% 48.95/7.62 % (16725)Time elapsed: 0.291 s
% 48.95/7.62 % (16725)Peak memory usage: 92 MB
% 48.95/7.62 % (16725)Instructions burned: 537 (million)
% 48.95/7.62 % (16728)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=1234649887:i=180:bd=preordered:av=off_2981 on theBenchmark for (2981ds/180Mi)
% 48.95/7.62 % (16728)Instruction limit reached!
% 48.95/7.62 % (16728)------------------------------
% 48.95/7.62 % (16728)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.95/7.62 % (16728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.95/7.62 % (16728)CaDiCaL version: 2.1.3
% 48.95/7.62 % (16728)Termination reason: Instruction limit
% 48.95/7.62 % (16728)Termination phase: Saturation
% 48.95/7.62 % (16728)Time elapsed: 0.098 s
% 48.95/7.62 % (16728)Peak memory usage: 92 MB
% 48.95/7.62 % (16728)Instructions burned: 182 (million)
% 48.95/7.62 % (16730)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=2540708639:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2978 on theBenchmark for (2978ds/10307Mi)
% 48.95/7.62 % (16724)Instruction limit reached!
% 48.95/7.62 % (16724)------------------------------
% 48.95/7.62 % (16724)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.95/7.62 % (16724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.95/7.62 % (16724)CaDiCaL version: 2.1.3
% 48.95/7.62 % (16724)Termination reason: Instruction limit
% 48.95/7.62 % (16724)Termination phase: Saturation
% 48.95/7.62 % (16724)Time elapsed: 1.033 s
% 48.95/7.62 % (16724)Peak memory usage: 156 MB
% 48.95/7.62 % (16724)Instructions burned: 3258 (million)
% 48.95/7.62 % (16732)lrs-1010_1024_to=lpo:sil=8000:tgt=ground:plsq=on:plsqc=1:sas=cadical:plsqr=1,32:sp=arity:lma=off:spb=goal:acc=on:bce=on:nwc=1.2:alpa=false:random_seed=3763722737:i=412:gtgl=4:gtg=exists_all_2974 on theBenchmark for (2974ds/412Mi)
% 48.95/7.62 % (16702)Instruction limit reached!
% 48.95/7.62 % (16702)------------------------------
% 48.95/7.62 % (16702)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.95/7.62 % (16702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.95/7.62 % (16702)CaDiCaL version: 2.1.3
% 48.95/7.62 % (16702)Termination reason: Instruction limit
% 48.95/7.62 % (16702)Termination phase: Saturation
% 48.95/7.62 % (16702)Time elapsed: 1.931 s
% 48.95/7.62 % (16702)Peak memory usage: 151 MB
% 48.95/7.62 % (16702)Instructions burned: 3395 (million)
% 48.95/7.62 % (16732)Instruction limit reached!
% 48.95/7.62 % (16732)------------------------------
% 48.95/7.62 % (16732)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.95/7.62 % (16732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.95/7.62 % (16732)CaDiCaL version: 2.1.3
% 71.38/10.94 % (16732)Termination reason: Instruction limit
% 71.38/10.94 % (16732)Termination phase: Saturation
% 71.38/10.94 % (16732)Time elapsed: 0.125 s
% 71.38/10.94 % (16732)Peak memory usage: 95 MB
% 71.38/10.94 % (16732)Instructions burned: 414 (million)
% 71.38/10.94 % (16734)ott+1002_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:etr=on:spb=units:urr=on:bsr=unit_only:gs=on:s2agt=16:br=off:random_seed=3836269313:s2pl=no:i=8478:s2at=4:nm=6_2973 on theBenchmark for (2973ds/8478Mi)
% 71.38/10.94 % (16735)ott-1011_2_sil=32000:bsd=on:sp=reverse_frequency:erd=off:urr=on:rnwc=on:gs=on:s2agt=70:updr=off:lftc=20:random_seed=134823327:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2972 on theBenchmark for (2972ds/303Mi)
% 71.38/10.94 % (16735)Instruction limit reached!
% 71.38/10.94 % (16735)------------------------------
% 71.38/10.94 % (16735)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.38/10.94 % (16735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.38/10.94 % (16735)CaDiCaL version: 2.1.3
% 71.38/10.94 % (16735)Termination reason: Instruction limit
% 71.38/10.94 % (16735)Termination phase: Saturation
% 71.38/10.94 % (16735)Time elapsed: 0.088 s
% 71.38/10.94 % (16735)Peak memory usage: 94 MB
% 71.38/10.94 % (16735)Instructions burned: 304 (million)
% 71.38/10.94 % (16738)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=3717614155:st=4:i=720:sd=3:fsr=off:ss=axioms_2970 on theBenchmark for (2970ds/720Mi)
% 71.38/10.94 % (16738)Instruction limit reached!
% 71.38/10.94 % (16738)------------------------------
% 71.38/10.94 % (16738)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.38/10.94 % (16738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.38/10.94 % (16738)CaDiCaL version: 2.1.3
% 71.38/10.94 % (16738)Termination reason: Instruction limit
% 71.38/10.94 % (16738)Termination phase: Saturation
% 71.38/10.94 % (16738)Time elapsed: 0.226 s
% 71.38/10.94 % (16738)Peak memory usage: 100 MB
% 71.38/10.94 % (16738)Instructions burned: 721 (million)
% 71.38/10.94 % (16740)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=136742101:i=598:bs=on:bd=preordered:av=off:ss=axioms_2967 on theBenchmark for (2967ds/598Mi)
% 71.38/10.94 % (16740)Instruction limit reached!
% 71.38/10.94 % (16740)------------------------------
% 71.38/10.94 % (16740)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.38/10.94 % (16740)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.38/10.94 % (16740)CaDiCaL version: 2.1.3
% 71.38/10.94 % (16740)Termination reason: Instruction limit
% 71.38/10.94 % (16740)Termination phase: Saturation
% 71.38/10.94 % (16740)Time elapsed: 0.206 s
% 71.38/10.94 % (16740)Peak memory usage: 96 MB
% 71.38/10.94 % (16740)Instructions burned: 599 (million)
% 71.38/10.94 % (16742)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=783640971:i=2989:sd=3:ss=axioms:sgt=60_2964 on theBenchmark for (2964ds/2989Mi)
% 71.38/10.94 % (16711)Instruction limit reached!
% 71.38/10.94 % (16711)------------------------------
% 71.38/10.94 % (16711)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.38/10.94 % (16711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.38/10.94 % (16711)CaDiCaL version: 2.1.3
% 71.38/10.94 % (16711)Termination reason: Instruction limit
% 71.38/10.94 % (16711)Termination phase: Saturation
% 71.38/10.94 % (16711)Time elapsed: 3.095 s
% 71.38/10.94 % (16711)Peak memory usage: 169 MB
% 71.38/10.94 % (16711)Instructions burned: 5210 (million)
% 71.38/10.94 % (16744)dis+1011_1_ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:bsd=on:sp=const_min:spb=goal_then_units:lcm=predicate:urr=ec_only:s2agt=16:random_seed=1305835390:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2960 on theBenchmark for (2960ds/1997Mi)
% 71.38/10.94 % (16742)Instruction limit reached!
% 71.38/10.94 % (16742)------------------------------
% 71.38/10.94 % (16742)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.38/10.94 % (16742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.38/10.94 % (16742)CaDiCaL version: 2.1.3
% 71.38/10.94 % (16742)Termination reason: Instruction limit
% 71.38/10.94 % (16742)Termination phase: Saturation
% 71.38/10.94 % (16742)Time elapsed: 1.069 s
% 71.38/10.94 % (16742)Peak memory usage: 148 MB
% 71.38/10.94 % (16742)Instructions burned: 2991 (million)
% 71.38/10.94 % (16746)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:drc=off:sp=unary_frequency:urr=ec_only:fd=preordered:random_seed=1826173566:i=2088:bd=preordered:av=off_2953 on theBenchmark for (2953ds/2088Mi)
% 98.73/14.76 % (16744)Instruction limit reached!
% 98.73/14.76 % (16744)------------------------------
% 98.73/14.76 % (16744)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 98.73/14.76 % (16744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.73/14.76 % (16744)CaDiCaL version: 2.1.3
% 98.73/14.76 % (16744)Termination reason: Instruction limit
% 98.73/14.76 % (16744)Termination phase: Saturation
% 98.73/14.76 % (16744)Time elapsed: 1.223 s
% 98.73/14.76 % (16744)Peak memory usage: 157 MB
% 98.73/14.76 % (16744)Instructions burned: 1998 (million)
% 98.73/14.76 % (16748)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=2132500421:i=1098:nicw=on_2946 on theBenchmark for (2946ds/1098Mi)
% 98.73/14.76 % (16746)Instruction limit reached!
% 98.73/14.76 % (16746)------------------------------
% 98.73/14.76 % (16746)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 98.73/14.76 % (16746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.73/14.76 % (16746)CaDiCaL version: 2.1.3
% 98.73/14.76 % (16746)Termination reason: Instruction limit
% 98.73/14.76 % (16746)Termination phase: Saturation
% 98.73/14.76 % (16746)Time elapsed: 0.721 s
% 98.73/14.76 % (16746)Peak memory usage: 157 MB
% 98.73/14.76 % (16746)Instructions burned: 2089 (million)
% 98.73/14.76 % (16750)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=3444815414:i=433:bd=preordered_2944 on theBenchmark for (2944ds/433Mi)
% 98.73/14.76 % (16750)Instruction limit reached!
% 98.73/14.76 % (16750)------------------------------
% 98.73/14.76 % (16750)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 98.73/14.76 % (16750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.73/14.76 % (16750)CaDiCaL version: 2.1.3
% 98.73/14.76 % (16750)Termination reason: Instruction limit
% 98.73/14.76 % (16750)Termination phase: Saturation
% 98.73/14.76 % (16750)Time elapsed: 0.149 s
% 98.73/14.76 % (16750)Peak memory usage: 96 MB
% 98.73/14.76 % (16750)Instructions burned: 435 (million)
% 98.73/14.76 % (16752)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=1279624802:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2942 on theBenchmark for (2942ds/2942Mi)
% 98.73/14.76 % (16748)Instruction limit reached!
% 98.73/14.76 % (16748)------------------------------
% 98.73/14.76 % (16748)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 98.73/14.76 % (16748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.73/14.76 % (16748)CaDiCaL version: 2.1.3
% 98.73/14.76 % (16748)Termination reason: Instruction limit
% 98.73/14.76 % (16748)Termination phase: Saturation
% 98.73/14.76 % (16748)Time elapsed: 0.603 s
% 98.73/14.76 % (16748)Peak memory usage: 104 MB
% 98.73/14.76 % (16748)Instructions burned: 1099 (million)
% 98.73/14.76 % (16754)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=1990501995:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2939 on theBenchmark for (2939ds/6922Mi)
% 98.73/14.76 % (16752)Instruction limit reached!
% 98.73/14.76 % (16752)------------------------------
% 98.73/14.76 % (16752)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 98.73/14.76 % (16752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.73/14.76 % (16752)CaDiCaL version: 2.1.3
% 98.73/14.76 % (16752)Termination reason: Instruction limit
% 98.73/14.76 % (16752)Termination phase: Saturation
% 98.73/14.76 % (16752)Time elapsed: 1.034 s
% 98.73/14.76 % (16752)Peak memory usage: 153 MB
% 98.73/14.76 % (16752)Instructions burned: 2945 (million)
% 98.73/14.76 % (16734)Instruction limit reached!
% 98.73/14.76 % (16734)------------------------------
% 98.73/14.76 % (16734)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 98.73/14.76 % (16734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.73/14.76 % (16734)CaDiCaL version: 2.1.3
% 98.73/14.76 % (16734)Termination reason: Instruction limit
% 98.73/14.76 % (16734)Termination phase: Saturation
% 98.73/14.76 % (16734)Time elapsed: 4.151 s
% 98.73/14.76 % (16734)Peak memory usage: 185 MB
% 98.73/14.76 % (16734)Instructions burned: 8481 (million)
% 98.73/14.76 % (16756)dis+10_5:1_sil=8000:tgt=full:plsq=on:plsqc=1:plsqr=32,1:urr=on:fd=off:nwc=0.5:br=off:slsqc=3:slsq=on:random_seed=828285684:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2931 on theBenchmark for (2931ds/596Mi)
% 110.98/16.47 % (16757)lrs+21_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=non_intro:urr=on:fd=preordered:random_seed=3292599311:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2930 on theBenchmark for (2930ds/4123Mi)
% 110.98/16.47 % (16756)Instruction limit reached!
% 110.98/16.47 % (16756)------------------------------
% 110.98/16.47 % (16756)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 110.98/16.47 % (16756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.98/16.47 % (16756)CaDiCaL version: 2.1.3
% 110.98/16.47 % (16756)Termination reason: Instruction limit
% 110.98/16.47 % (16756)Termination phase: Saturation
% 110.98/16.47 % (16756)Time elapsed: 0.183 s
% 110.98/16.47 % (16756)Peak memory usage: 98 MB
% 110.98/16.47 % (16756)Instructions burned: 596 (million)
% 110.98/16.47 % (16760)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=2632492401:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2928 on theBenchmark for (2928ds/16411Mi)
% 110.98/16.47 % (16730)Instruction limit reached!
% 110.98/16.47 % (16730)------------------------------
% 110.98/16.47 % (16730)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 110.98/16.47 % (16730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.98/16.47 % (16730)CaDiCaL version: 2.1.3
% 110.98/16.47 % (16730)Termination reason: Instruction limit
% 110.98/16.47 % (16730)Termination phase: Saturation
% 110.98/16.47 % (16730)Time elapsed: 5.290 s
% 110.98/16.47 % (16730)Peak memory usage: 172 MB
% 110.98/16.47 % (16730)Instructions burned: 10308 (million)
% 110.98/16.47 % (16762)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=4156253343:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2924 on theBenchmark for (2924ds/1670Mi)
% 110.98/16.47 % (16762)Instruction limit reached!
% 110.98/16.47 % (16762)------------------------------
% 110.98/16.47 % (16762)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 110.98/16.47 % (16762)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.98/16.47 % (16762)CaDiCaL version: 2.1.3
% 110.98/16.47 % (16762)Termination reason: Instruction limit
% 110.98/16.47 % (16762)Termination phase: Saturation
% 110.98/16.47 % (16762)Time elapsed: 1.065 s
% 110.98/16.47 % (16762)Peak memory usage: 152 MB
% 110.98/16.47 % (16762)Instructions burned: 1670 (million)
% 110.98/16.47 % (16764)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:prc=on:drc=off:fde=unused:sp=reverse_frequency:updr=off:random_seed=3640976402:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2912 on theBenchmark for (2912ds/1722Mi)
% 110.98/16.47 % (16757)Instruction limit reached!
% 110.98/16.47 % (16757)------------------------------
% 110.98/16.47 % (16757)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 110.98/16.47 % (16757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.98/16.47 % (16757)CaDiCaL version: 2.1.3
% 110.98/16.47 % (16757)Termination reason: Instruction limit
% 110.98/16.47 % (16757)Termination phase: Saturation
% 110.98/16.47 % (16757)Time elapsed: 2.405 s
% 110.98/16.47 % (16757)Peak memory usage: 163 MB
% 110.98/16.47 % (16757)Instructions burned: 4124 (million)
% 110.98/16.47 % (16766)ott-1004_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:sas=cadical:sp=const_frequency:acc=on:urr=ec_only:gs=on:s2agt=40:alpa=false:sac=on:random_seed=3894621518:cts=off:cond=on:i=9530:bs=on:fsd=on_2905 on theBenchmark for (2905ds/9530Mi)
% 110.98/16.47 % (16764)Instruction limit reached!
% 110.98/16.47 % (16764)------------------------------
% 110.98/16.47 % (16764)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 110.98/16.47 % (16764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.98/16.47 % (16764)CaDiCaL version: 2.1.3
% 110.98/16.47 % (16764)Termination reason: Instruction limit
% 110.98/16.47 % (16764)Termination phase: Saturation
% 110.98/16.47 % (16764)Time elapsed: 1.096 s
% 110.98/16.47 % (16764)Peak memory usage: 149 MB
% 110.98/16.47 % (16764)Instructions burned: 1723 (million)
% 110.98/16.47 % (16768)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=751466971:st=2:i=4495:sd=10:ss=included_2899 on theBenchmark for (2899ds/4495Mi)
% 110.98/16.47 % (16754)Instruction limit reached!
% 110.98/16.47 % (16754)------------------------------
% 110.98/16.47 % (16754)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.14/17.24 % (16754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.14/17.24 % (16754)CaDiCaL version: 2.1.3
% 62.14/17.24 % (16754)Termination reason: Instruction limit
% 62.14/17.24 % (16754)Termination phase: Saturation
% 62.14/17.24 % (16754)Time elapsed: 4.046 s
% 62.14/17.24 % (16754)Peak memory usage: 184 MB
% 62.14/17.24 % (16754)Instructions burned: 6923 (million)
% 62.14/17.24 % (16770)lrs+1002_1_sfv=off:ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=reverse_arity:spb=non_intro:s2agt=16:random_seed=4106717865:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2897 on theBenchmark for (2897ds/4920Mi)
% 62.14/17.24 % (16760)Instruction limit reached!
% 62.14/17.24 % (16760)------------------------------
% 62.14/17.24 % (16760)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.14/17.24 % (16760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.14/17.24 % (16760)CaDiCaL version: 2.1.3
% 62.14/17.24 % (16760)Termination reason: Instruction limit
% 62.14/17.24 % (16760)Termination phase: Saturation
% 62.14/17.24 % (16760)Time elapsed: 5.453 s
% 62.14/17.24 % (16760)Peak memory usage: 256 MB
% 62.14/17.24 % (16760)Instructions burned: 16414 (million)
% 62.14/17.24 % (16772)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:lcm=reverse:bce=on:bsr=unit_only:random_seed=1295500817:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2873 on theBenchmark for (2873ds/2083Mi)
% 62.14/17.24 % (16768)Instruction limit reached!
% 62.14/17.24 % (16768)------------------------------
% 62.14/17.24 % (16768)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.14/17.24 % (16768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.14/17.24 % (16768)CaDiCaL version: 2.1.3
% 62.14/17.24 % (16768)Termination reason: Instruction limit
% 62.14/17.24 % (16768)Termination phase: Saturation
% 62.14/17.24 % (16768)Time elapsed: 2.692 s
% 62.14/17.24 % (16768)Peak memory usage: 162 MB
% 62.14/17.24 % (16768)Instructions burned: 4496 (million)
% 62.14/17.24 % (16774)lrs+31_1_to=lpo:ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=weighted_frequency:sos=all:spb=units:lcm=predicate:bsr=on:gs=on:random_seed=2077824849:i=4629:av=off:gsp=on_2871 on theBenchmark for (2871ds/4629Mi)
% 62.14/17.24 % (16772)Instruction limit reached!
% 62.14/17.24 % (16772)------------------------------
% 62.14/17.24 % (16772)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.14/17.24 % (16772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.14/17.24 % (16772)CaDiCaL version: 2.1.3
% 62.14/17.24 % (16772)Termination reason: Instruction limit
% 62.14/17.24 % (16772)Termination phase: Saturation
% 62.14/17.24 % (16772)Time elapsed: 0.707 s
% 62.14/17.24 % (16772)Peak memory usage: 159 MB
% 62.14/17.24 % (16772)Instructions burned: 2084 (million)
% 62.14/17.24 % (16770)Instruction limit reached!
% 62.14/17.24 % (16770)------------------------------
% 62.14/17.24 % (16770)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.14/17.24 % (16770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.14/17.24 % (16770)CaDiCaL version: 2.1.3
% 62.14/17.24 % (16770)Termination reason: Instruction limit
% 62.14/17.24 % (16770)Termination phase: Saturation
% 62.14/17.24 % (16770)Time elapsed: 3.123 s
% 62.14/17.24 % (16770)Peak memory usage: 171 MB
% 62.14/17.24 % (16770)Instructions burned: 4921 (million)
% 62.14/17.24 % (16776)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=353241023:i=1258:av=off_2865 on theBenchmark for (2865ds/1258Mi)
% 62.14/17.24 % (16777)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=525945952:i=7343:av=off:ss=included_2864 on theBenchmark for (2864ds/7343Mi)
% 62.14/17.24 % (16776)Instruction limit reached!
% 62.14/17.24 % (16776)------------------------------
% 62.14/17.24 % (16776)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.14/17.24 % (16776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.14/17.24 % (16776)CaDiCaL version: 2.1.3
% 62.14/17.24 % (16776)Termination reason: Instruction limit
% 62.14/17.24 % (16776)Termination phase: Saturation
% 62.14/17.24 % (16776)Time elapsed: 0.411 s
% 62.14/17.24 % (16776)Peak memory usage: 103 MB
% 62.14/17.24 % (16776)Instructions burned: 1261 (million)
% 62.14/17.24 % (16780)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=1116743619:i=1325:sd=2:ss=axioms:sgt=16_2860 on theBenchmark for (2860ds/1325Mi)
% 62.14/17.24 % (16780)Refutation not found, incomplete strategy
% 62.14/17.24 % (16780)------------------------------
% 62.14/17.24 % (16780)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.14/17.24 % (16780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.14/17.24 % (16780)CaDiCaL version: 2.1.3
% 62.14/17.24 % (16780)Termination reason: Refutation not found, incomplete strategy
% 62.14/17.24 % (16780)Time elapsed: 0.009 s
% 62.14/17.24 % (16780)Peak memory usage: 90 MB
% 62.14/17.24 % (16780)Instructions burned: 22 (million)
% 62.14/17.24 % (16780)------------------------------
% 62.14/17.24 % (16780)------------------------------
% 62.14/17.24 % (16782)dis+1011_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:sp=arity:lma=off:spb=intro:urr=ec_only:sac=on:random_seed=2649779257:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2857 on theBenchmark for (2857ds/2646Mi)
% 62.14/17.24 % (16766)Instruction limit reached!
% 62.14/17.24 % (16766)------------------------------
% 62.14/17.24 % (16766)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.14/17.24 % (16766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.14/17.24 % (16766)CaDiCaL version: 2.1.3
% 62.14/17.24 % (16766)Termination reason: Instruction limit
% 62.14/17.24 % (16766)Termination phase: Saturation
% 62.14/17.24 % (16766)Time elapsed: 4.966 s
% 62.14/17.24 % (16766)Peak memory usage: 159 MB
% 62.14/17.24 % (16766)Instructions burned: 9532 (million)
% 62.14/17.24 % (16784)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=3314021680:i=1489:sd=2:ep=R:ss=axioms_2854 on theBenchmark for (2854ds/1489Mi)
% 62.14/17.24 % (16782)Instruction limit reached!
% 62.14/17.24 % (16782)------------------------------
% 62.14/17.24 % (16782)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.14/17.24 % (16782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.14/17.24 % (16782)CaDiCaL version: 2.1.3
% 62.14/17.24 % (16782)Termination reason: Instruction limit
% 62.14/17.24 % (16782)Termination phase: Saturation
% 62.14/17.24 % (16782)Time elapsed: 0.819 s
% 62.14/17.24 % (16782)Peak memory usage: 152 MB
% 62.14/17.24 % (16782)Instructions burned: 2647 (million)
% 62.14/17.24 % (16786)lrs+20_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:fde=unused:sp=occurrence:sos=on:lcm=predicate:urr=full:sac=on:random_seed=2477421824:i=1503_2848 on theBenchmark for (2848ds/1503Mi)
% 62.14/17.24 % (16774)Instruction limit reached!
% 62.14/17.24 % (16774)------------------------------
% 62.14/17.24 % (16774)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.14/17.24 % (16774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.14/17.24 % (16774)CaDiCaL version: 2.1.3
% 62.14/17.24 % (16774)Termination reason: Instruction limit
% 62.14/17.24 % (16774)Termination phase: Saturation
% 62.14/17.24 % (16774)Time elapsed: 2.463 s
% 62.14/17.24 % (16774)Peak memory usage: 152 MB
% 62.14/17.24 % (16774)Instructions burned: 4629 (million)
% 62.14/17.24 % (16788)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=3680659420:i=13942:kws=frequency_2845 on theBenchmark for (2845ds/13942Mi)
% 62.14/17.24 % (16784)Instruction limit reached!
% 62.14/17.24 % (16784)------------------------------
% 62.14/17.24 % (16784)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.14/17.24 % (16784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.14/17.24 % (16784)CaDiCaL version: 2.1.3
% 62.14/17.24 % (16784)Termination reason: Instruction limit
% 62.14/17.24 % (16784)Termination phase: Saturation
% 62.14/17.24 % (16784)Time elapsed: 0.925 s
% 62.14/17.24 % (16784)Peak memory usage: 137 MB
% 62.14/17.24 % (16784)Instructions burned: 1490 (million)
% 62.14/17.24 % (16790)lrs-1002_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=16000:npcc=on:bsd=on:sp=unary_frequency:spb=goal:lcm=predicate:acc=on:urr=full:bce=on:bsr=unit_only:s2agt=64:sac=on:random_seed=2716383116:i=3604:fsr=off:er=filter_2843 on theBenchmark for (2843ds/3604Mi)
% 62.14/17.24 % (16786)Instruction limit reached!
% 62.14/17.24 % (16786)------------------------------
% 62.14/17.24 % (16786)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.14/17.24 % (16786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.14/17.24 % (16786)CaDiCaL version: 2.1.3
% 62.14/17.24 % (16786)Termination reason: Instruction limit
% 62.14/17.24 % (16786)Termination phase: Saturation
% 62.14/17.24 % (16786)Time elapsed: 0.554 s
% 62.14/17.24 % (16786)Peak memory usage: 151 MB
% 62.14/17.24 % (16786)Instructions burned: 1503 (million)
% 62.14/17.24 % (16792)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=2097693752:i=1876:sd=1:ss=included:sgt=32_2841 on theBenchmark for (2841ds/1876Mi)
% 62.14/17.24 % (16792)First to succeed.
% 62.14/17.24 % (16792)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-16673"
% 62.14/17.24 % (16792)Refutation found. Thanks to Tanya!
% 62.14/17.24 % SZS status Unsatisfiable for theBenchmark
% 62.14/17.24 % SZS output start Proof for theBenchmark
% See solution above
% 117.27/17.44 % (16792)------------------------------
% 117.27/17.44 % (16792)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.27/17.44 % (16792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.27/17.44 % (16792)CaDiCaL version: 2.1.3
% 117.27/17.44 % (16792)Termination reason: Refutation
% 117.27/17.44 % (16792)Time elapsed: 0.473 s
% 117.27/17.44 % (16792)Peak memory usage: 135 MB
% 117.27/17.44 % (16792)Instructions burned: 1319 (million)
% 117.27/17.44 % (16792)------------------------------
% 117.27/17.44 % (16792)------------------------------
% 117.27/17.44 % (16673)Success in time 16.571 s
% 117.27/17.44 % Vampire exiting
%------------------------------------------------------------------------------