%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ANA019-1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n020.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:31:18 AM UTC 2026
% Result : Unsatisfiable 199.31s 33.72s
% Output : Refutation 199.31s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 31
% Syntax : Number of formulae : 108 ( 32 unt; 2 def)
% Number of atoms : 207 ( 31 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 173 ( 74 ~; 97 |; 0 &)
% ( 2 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 17 ( 15 usr; 3 prp; 0-3 aty)
% Number of functors : 16 ( 16 usr; 5 con; 0-3 aty)
% Number of variables : 83 ( 0 sgn 83 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1304,axiom,
! [X0] :
( c_less(c_0,X0,tc_nat)
| X0 = c_0 ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Nat_Onot__gr0_0) ).
fof(f1305,plain,
! [X0] :
( c_less(c_0,X0,tc_nat)
| c_0 = X0 ),
inference(reorient_equations,[],[f1304]) ).
fof(f1418,axiom,
! [X0] :
( ~ class_OrderedGroup_Olordered__ab__group__abs(X0)
| c_0 = c_HOL_Oabs(c_0,X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_OrderedGroup_Oabs__0__eq_1) ).
fof(f1425,axiom,
! [X0,X1] :
( ~ class_OrderedGroup_Olordered__ab__group__abs(X0)
| c_lessequals(c_0,c_HOL_Oabs(X1,X0),X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_OrderedGroup_Oabs__ge__zero_0) ).
fof(f1434,axiom,
! [X0,X1] :
( ~ class_OrderedGroup_Olordered__ab__group__abs(X0)
| ~ c_lessequals(c_0,X1,X0)
| c_HOL_Oabs(X1,X0) = X1 ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_OrderedGroup_Oabs__of__nonneg_0) ).
fof(f1477,axiom,
! [X0,X1] :
( ~ class_OrderedGroup_Oab__group__add(X0)
| c_uminus(c_uminus(X1,X0),X0) = X1 ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_OrderedGroup_Ominus__minus_0) ).
fof(f1482,axiom,
! [X0,X1] :
( ~ class_OrderedGroup_Opordered__ab__group__add(X0)
| ~ c_lessequals(c_0,c_uminus(X1,X0),X0)
| c_lessequals(X1,c_0,X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_OrderedGroup_Oneg__0__le__iff__le_0) ).
fof(f1492,axiom,
! [X0,X1] :
( ~ class_OrderedGroup_Opordered__ab__group__add(X0)
| ~ c_lessequals(c_uminus(X1,X0),c_0,X0)
| c_lessequals(c_0,X1,X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_OrderedGroup_Oneg__le__0__iff__le_0) ).
fof(f1512,axiom,
! [X0,X1] :
( ~ class_OrderedGroup_Olordered__ab__group(X0)
| ~ c_lessequals(c_0,X1,X0)
| c_OrderedGroup_Opprt(X1,X0) = X1 ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_OrderedGroup_Opprt__eq__id_0) ).
fof(f1518,axiom,
! [X0,X1] :
( ~ class_OrderedGroup_Olordered__ab__group(X0)
| c_lessequals(c_0,c_OrderedGroup_Opprt(X1,X0),X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_OrderedGroup_Ozero__le__pprt_0) ).
fof(f1924,axiom,
! [X0] : c_Finite__Set_Ocard(c_SetInterval_OatMost(X0,tc_nat),tc_nat) = c_Suc(X0),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_SetInterval_Ocard__atMost_0) ).
fof(f1925,plain,
! [X0] : c_Suc(X0) = c_Finite__Set_Ocard(c_SetInterval_OatMost(X0,tc_nat),tc_nat),
inference(reorient_equations,[],[f1924]) ).
fof(f2456,axiom,
! [X0] :
( ~ class_LOrder_Ojoin__semilorder(X0)
| class_Orderings_Oorder(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-0.ax',clsrel_LOrder_Ojoin__semilorder_1) ).
fof(f2460,axiom,
! [X0] :
( ~ class_LOrder_Olorder(X0)
| class_LOrder_Ojoin__semilorder(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-0.ax',clsrel_LOrder_Olorder_3) ).
fof(f2539,axiom,
! [X0] :
( ~ class_OrderedGroup_Olordered__ab__group__abs(X0)
| class_OrderedGroup_Olordered__ab__group(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-0.ax',clsrel_OrderedGroup_Olordered__ab__group__abs_0) ).
fof(f2566,axiom,
! [X0] :
( ~ class_OrderedGroup_Olordered__ab__group__join(X0)
| class_OrderedGroup_Olordered__ab__group(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-0.ax',clsrel_OrderedGroup_Olordered__ab__group__join_16) ).
fof(f2888,axiom,
! [X0] :
( ~ class_Ring__and__Field_Olordered__ring(X0)
| class_OrderedGroup_Opordered__ab__group__add(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-0.ax',clsrel_Ring__and__Field_Olordered__ring_2) ).
fof(f2893,axiom,
! [X0] :
( ~ class_Ring__and__Field_Olordered__ring(X0)
| class_OrderedGroup_Olordered__ab__group__abs(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-0.ax',clsrel_Ring__and__Field_Olordered__ring_24) ).
fof(f2899,axiom,
! [X0] :
( ~ class_Ring__and__Field_Olordered__ring(X0)
| class_OrderedGroup_Oab__group__add(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-0.ax',clsrel_Ring__and__Field_Olordered__ring_3) ).
fof(f2904,axiom,
! [X0] :
( ~ class_Ring__and__Field_Olordered__ring(X0)
| class_Ring__and__Field_Opordered__cancel__semiring(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-0.ax',clsrel_Ring__and__Field_Olordered__ring_7) ).
fof(f3026,axiom,
! [X0] :
( ~ class_Ring__and__Field_Oordered__idom(X0)
| class_LOrder_Olorder(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-0.ax',clsrel_Ring__and__Field_Oordered__idom_34) ).
fof(f3041,axiom,
! [X0] :
( ~ class_Ring__and__Field_Oordered__idom(X0)
| class_Ring__and__Field_Olordered__ring(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-0.ax',clsrel_Ring__and__Field_Oordered__idom_48) ).
fof(f3046,axiom,
! [X0] :
( ~ class_Ring__and__Field_Oordered__idom(X0)
| class_OrderedGroup_Olordered__ab__group__join(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-0.ax',clsrel_Ring__and__Field_Oordered__idom_52) ).
fof(f3362,axiom,
! [X0] :
( ~ c_less(c_0,X0,tc_nat)
| X0 = c_Suc(c_minus(X0,c_1,tc_nat)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_NatBin_OSuc__pred_H_0) ).
fof(f3363,plain,
! [X0] :
( ~ c_less(c_0,X0,tc_nat)
| c_Suc(c_minus(X0,c_1,tc_nat)) = X0 ),
inference(reorient_equations,[],[f3362]) ).
fof(f3364,axiom,
! [X2,X0,X1] :
( ~ class_Orderings_Oorder(X0)
| ~ c_less(X1,X2,X0)
| c_lessequals(X1,X2,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Orderings_Oorder__less__imp__le_0) ).
fof(f3365,axiom,
! [X2,X0,X1] :
( ~ class_Ring__and__Field_Opordered__cancel__semiring(X0)
| ~ c_lessequals(c_0,X1,X0)
| ~ c_lessequals(c_0,X2,X0)
| c_lessequals(c_0,c_times(X2,X1,X0),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Ring__and__Field_Omult__nonneg__nonneg_0) ).
fof(f3368,negated_conjecture,
v_f(c_0) = c_0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f3369,plain,
c_0 = v_f(c_0),
inference(reorient_equations,[],[f3368]) ).
fof(f3370,negated_conjecture,
c_less(c_0,v_x,t_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_1) ).
fof(f3371,negated_conjecture,
! [X0] : c_lessequals(c_HOL_Oabs(v_f(c_Suc(X0)),t_a),c_times(v_x,c_HOL_Oabs(v_h(c_Suc(X0)),t_a),t_a),t_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_2) ).
fof(f3372,negated_conjecture,
! [X0] :
( ~ c_lessequals(c_HOL_Oabs(v_f(v_xa(X0)),t_a),c_times(X0,c_HOL_Oabs(v_h(v_xa(X0)),t_a),t_a),t_a)
| ~ c_less(c_0,X0,t_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_3) ).
fof(f3373,negated_conjecture,
class_Ring__and__Field_Oordered__idom(t_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',tfree_tcs) ).
fof(f3594,plain,
! [X0] :
( ~ c_less(c_0,X0,tc_nat)
| c_Finite__Set_Ocard(c_SetInterval_OatMost(c_minus(X0,c_1,tc_nat),tc_nat),tc_nat) = X0 ),
inference(definition_unfolding,[],[f3363,f1925]) ).
fof(f3595,plain,
! [X0] : c_lessequals(c_HOL_Oabs(v_f(c_Finite__Set_Ocard(c_SetInterval_OatMost(X0,tc_nat),tc_nat)),t_a),c_times(v_x,c_HOL_Oabs(v_h(c_Finite__Set_Ocard(c_SetInterval_OatMost(X0,tc_nat),tc_nat)),t_a),t_a),t_a),
inference(definition_unfolding,[],[f3371,f1925,f1925]) ).
fof(f3917,plain,
! [X0] :
( ~ c_less(c_0,X0,tc_nat)
| c_0 = X0 ),
inference(consistent_polarity_flipping,[],[f1305]) ).
fof(f3956,plain,
! [X0] :
( class_OrderedGroup_Olordered__ab__group__abs(X0)
| c_0 = c_HOL_Oabs(c_0,X0) ),
inference(consistent_polarity_flipping,[],[f1418]) ).
fof(f3960,plain,
! [X0,X1] :
( c_lessequals(c_0,c_HOL_Oabs(X1,X0),X0)
| class_OrderedGroup_Olordered__ab__group__abs(X0) ),
inference(consistent_polarity_flipping,[],[f1425]) ).
fof(f3966,plain,
! [X0,X1] :
( ~ c_lessequals(c_0,X1,X0)
| class_OrderedGroup_Olordered__ab__group__abs(X0)
| c_HOL_Oabs(X1,X0) = X1 ),
inference(consistent_polarity_flipping,[],[f1434]) ).
fof(f3997,plain,
! [X0,X1] :
( ~ c_lessequals(c_0,X1,X0)
| class_OrderedGroup_Olordered__ab__group(X0)
| c_OrderedGroup_Opprt(X1,X0) = X1 ),
inference(consistent_polarity_flipping,[],[f1512]) ).
fof(f4001,plain,
! [X0,X1] :
( c_lessequals(c_0,c_OrderedGroup_Opprt(X1,X0),X0)
| class_OrderedGroup_Olordered__ab__group(X0) ),
inference(consistent_polarity_flipping,[],[f1518]) ).
fof(f4169,plain,
! [X0] :
( ~ class_Orderings_Oorder(X0)
| ~ class_LOrder_Ojoin__semilorder(X0) ),
inference(consistent_polarity_flipping,[],[f2456]) ).
fof(f4235,plain,
! [X0] :
( class_OrderedGroup_Olordered__ab__group__abs(X0)
| ~ class_OrderedGroup_Olordered__ab__group(X0) ),
inference(consistent_polarity_flipping,[],[f2539]) ).
fof(f4257,plain,
! [X0] :
( ~ class_OrderedGroup_Olordered__ab__group__join(X0)
| ~ class_OrderedGroup_Olordered__ab__group(X0) ),
inference(consistent_polarity_flipping,[],[f2566]) ).
fof(f4478,plain,
! [X0] :
( ~ class_Ring__and__Field_Olordered__ring(X0)
| ~ class_OrderedGroup_Olordered__ab__group__abs(X0) ),
inference(consistent_polarity_flipping,[],[f2893]) ).
fof(f4482,plain,
! [X0] :
( ~ class_Ring__and__Field_Opordered__cancel__semiring(X0)
| ~ class_Ring__and__Field_Olordered__ring(X0) ),
inference(consistent_polarity_flipping,[],[f2904]) ).
fof(f4702,plain,
! [X0] :
( c_less(c_0,X0,tc_nat)
| c_Finite__Set_Ocard(c_SetInterval_OatMost(c_minus(X0,c_1,tc_nat),tc_nat),tc_nat) = X0 ),
inference(consistent_polarity_flipping,[],[f3594]) ).
fof(f4703,plain,
! [X2,X0,X1] :
( c_lessequals(X1,X2,X0)
| c_less(X1,X2,X0)
| class_Orderings_Oorder(X0) ),
inference(consistent_polarity_flipping,[],[f3364]) ).
fof(f4704,plain,
! [X2,X0,X1] :
( c_lessequals(c_0,c_times(X2,X1,X0),X0)
| ~ c_lessequals(c_0,X1,X0)
| ~ c_lessequals(c_0,X2,X0)
| class_Ring__and__Field_Opordered__cancel__semiring(X0) ),
inference(consistent_polarity_flipping,[],[f3365]) ).
fof(f4705,plain,
~ c_less(c_0,v_x,t_a),
inference(consistent_polarity_flipping,[],[f3370]) ).
fof(f4706,plain,
! [X0] :
( ~ c_lessequals(c_HOL_Oabs(v_f(v_xa(X0)),t_a),c_times(X0,c_HOL_Oabs(v_h(v_xa(X0)),t_a),t_a),t_a)
| c_less(c_0,X0,t_a) ),
inference(consistent_polarity_flipping,[],[f3372]) ).
fof(f4936,plain,
class_LOrder_Olorder(t_a),
inference(resolution,[],[f3026,f3373]) ).
fof(f4948,plain,
class_LOrder_Ojoin__semilorder(t_a),
inference(resolution,[],[f4936,f2460]) ).
fof(f4966,plain,
class_Ring__and__Field_Olordered__ring(t_a),
inference(resolution,[],[f3041,f3373]) ).
fof(f4975,plain,
class_OrderedGroup_Opordered__ab__group__add(t_a),
inference(resolution,[],[f4966,f2888]) ).
fof(f4981,plain,
class_OrderedGroup_Oab__group__add(t_a),
inference(resolution,[],[f4966,f2899]) ).
fof(f4986,plain,
class_OrderedGroup_Olordered__ab__group__join(t_a),
inference(resolution,[],[f3046,f3373]) ).
fof(f5454,plain,
~ class_OrderedGroup_Olordered__ab__group(t_a),
inference(resolution,[],[f4257,f4986]) ).
fof(f5912,plain,
~ class_OrderedGroup_Olordered__ab__group__abs(t_a),
inference(resolution,[],[f4478,f4966]) ).
fof(f7090,plain,
c_0 = c_HOL_Oabs(c_0,t_a),
inference(resolution,[],[f3956,f5912]) ).
fof(f7503,plain,
! [X0] : c_uminus(c_uminus(X0,t_a),t_a) = X0,
inference(resolution,[],[f1477,f4981]) ).
fof(f7886,definition,
( spl0_21
<=> class_Orderings_Oorder(t_a) ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f7887,plain,
( ~ class_Orderings_Oorder(t_a)
| spl0_21 ),
inference(avatar_component_clause,[],[f7886]) ).
fof(f7888,plain,
( class_Orderings_Oorder(t_a)
| ~ spl0_21 ),
inference(avatar_component_clause,[],[f7886]) ).
fof(f7921,plain,
( ~ class_LOrder_Ojoin__semilorder(t_a)
| ~ spl0_21 ),
inference(resolution,[],[f7888,f4169]) ).
fof(f7975,plain,
( $false
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f7921,f4948]) ).
fof(f7976,plain,
~ spl0_21,
inference(avatar_contradiction_clause,[],[f7975]) ).
fof(f8349,plain,
! [X0,X1] :
( class_OrderedGroup_Olordered__ab__group(X0)
| c_HOL_Oabs(X1,X0) = c_OrderedGroup_Opprt(c_HOL_Oabs(X1,X0),X0)
| class_OrderedGroup_Olordered__ab__group__abs(X0) ),
inference(resolution,[],[f3997,f3960]) ).
fof(f8374,plain,
! [X0,X1] :
( class_OrderedGroup_Olordered__ab__group__abs(X0)
| c_HOL_Oabs(X1,X0) = c_OrderedGroup_Opprt(c_HOL_Oabs(X1,X0),X0) ),
inference(forward_subsumption_resolution,[],[f8349,f4235]) ).
fof(f8634,plain,
! [X0] :
( ~ c_lessequals(c_0,c_uminus(X0,t_a),t_a)
| c_lessequals(X0,c_0,t_a) ),
inference(resolution,[],[f1482,f4975]) ).
fof(f8661,plain,
! [X0] :
( ~ c_lessequals(c_uminus(X0,t_a),c_0,t_a)
| c_lessequals(c_0,X0,t_a) ),
inference(resolution,[],[f1492,f4975]) ).
fof(f8666,plain,
! [X0] :
( c_lessequals(X0,c_0,t_a)
| c_less(c_0,c_uminus(X0,t_a),t_a)
| class_Orderings_Oorder(t_a) ),
inference(resolution,[],[f8634,f4703]) ).
fof(f8669,plain,
( ! [X0] :
( c_less(c_0,c_uminus(X0,t_a),t_a)
| c_lessequals(X0,c_0,t_a) )
| spl0_21 ),
inference(forward_subsumption_resolution,[],[f8666,f7887]) ).
fof(f8725,plain,
( ! [X0] :
( c_lessequals(c_uminus(X0,t_a),c_0,t_a)
| c_less(c_0,X0,t_a) )
| spl0_21 ),
inference(superposition,[],[f8669,f7503]) ).
fof(f8755,plain,
( ! [X0] :
( c_lessequals(c_0,X0,t_a)
| c_less(c_0,X0,t_a) )
| spl0_21 ),
inference(resolution,[],[f8725,f8661]) ).
fof(f8766,plain,
( ! [X0] :
( c_less(c_0,X0,t_a)
| class_OrderedGroup_Olordered__ab__group__abs(t_a)
| c_HOL_Oabs(X0,t_a) = X0 )
| spl0_21 ),
inference(resolution,[],[f8755,f3966]) ).
fof(f8769,plain,
( ! [X0] :
( c_less(c_0,X0,t_a)
| c_HOL_Oabs(X0,t_a) = X0 )
| spl0_21 ),
inference(forward_subsumption_resolution,[],[f8766,f5912]) ).
fof(f8775,plain,
( v_x = c_HOL_Oabs(v_x,t_a)
| spl0_21 ),
inference(resolution,[],[f8769,f4705]) ).
fof(f8782,plain,
( c_lessequals(c_0,v_x,t_a)
| class_OrderedGroup_Olordered__ab__group__abs(t_a)
| spl0_21 ),
inference(superposition,[],[f3960,f8775]) ).
fof(f8783,plain,
( c_lessequals(c_0,v_x,t_a)
| spl0_21 ),
inference(forward_subsumption_resolution,[],[f8782,f5912]) ).
fof(f12095,plain,
! [X0] :
( c_Finite__Set_Ocard(c_SetInterval_OatMost(c_minus(X0,c_1,tc_nat),tc_nat),tc_nat) = X0
| c_0 = X0 ),
inference(resolution,[],[f4702,f3917]) ).
fof(f15690,definition,
( spl0_99
<=> class_Ring__and__Field_Opordered__cancel__semiring(t_a) ),
introduced(definition,[new_symbols(definition,[spl0_99])],[avatar_definition]) ).
fof(f15691,plain,
( ~ class_Ring__and__Field_Opordered__cancel__semiring(t_a)
| spl0_99 ),
inference(avatar_component_clause,[],[f15690]) ).
fof(f15692,plain,
( class_Ring__and__Field_Opordered__cancel__semiring(t_a)
| ~ spl0_99 ),
inference(avatar_component_clause,[],[f15690]) ).
fof(f15707,plain,
( ~ class_Ring__and__Field_Olordered__ring(t_a)
| ~ spl0_99 ),
inference(resolution,[],[f15692,f4482]) ).
fof(f15720,plain,
( $false
| ~ spl0_99 ),
inference(forward_subsumption_resolution,[],[f15707,f4966]) ).
fof(f15721,plain,
~ spl0_99,
inference(avatar_contradiction_clause,[],[f15720]) ).
fof(f65204,plain,
! [X0] : c_HOL_Oabs(X0,t_a) = c_OrderedGroup_Opprt(c_HOL_Oabs(X0,t_a),t_a),
inference(resolution,[],[f8374,f5912]) ).
fof(f65229,plain,
! [X0] :
( c_lessequals(c_0,c_HOL_Oabs(X0,t_a),t_a)
| class_OrderedGroup_Olordered__ab__group(t_a) ),
inference(superposition,[],[f4001,f65204]) ).
fof(f65230,plain,
! [X0] : c_lessequals(c_0,c_HOL_Oabs(X0,t_a),t_a),
inference(forward_subsumption_resolution,[],[f65229,f5454]) ).
fof(f90229,plain,
! [X0] :
( c_lessequals(c_HOL_Oabs(v_f(X0),t_a),c_times(v_x,c_HOL_Oabs(v_h(X0),t_a),t_a),t_a)
| c_0 = X0 ),
inference(superposition,[],[f3595,f12095]) ).
fof(f1253487,plain,
( c_0 = v_xa(v_x)
| c_less(c_0,v_x,t_a) ),
inference(resolution,[],[f90229,f4706]) ).
fof(f1253520,plain,
c_0 = v_xa(v_x),
inference(forward_subsumption_resolution,[],[f1253487,f4705]) ).
fof(f1254129,plain,
( ~ c_lessequals(c_HOL_Oabs(v_f(c_0),t_a),c_times(v_x,c_HOL_Oabs(v_h(c_0),t_a),t_a),t_a)
| c_less(c_0,v_x,t_a) ),
inference(superposition,[],[f4706,f1253520]) ).
fof(f1254130,plain,
~ c_lessequals(c_HOL_Oabs(v_f(c_0),t_a),c_times(v_x,c_HOL_Oabs(v_h(c_0),t_a),t_a),t_a),
inference(forward_subsumption_resolution,[],[f1254129,f4705]) ).
fof(f1254132,plain,
~ c_lessequals(c_HOL_Oabs(c_0,t_a),c_times(v_x,c_HOL_Oabs(v_h(c_0),t_a),t_a),t_a),
inference(forward_demodulation,[],[f1254130,f3369]) ).
fof(f1254134,plain,
~ c_lessequals(c_0,c_times(v_x,c_HOL_Oabs(v_h(c_0),t_a),t_a),t_a),
inference(forward_demodulation,[],[f1254132,f7090]) ).
fof(f1441001,plain,
( ~ c_lessequals(c_0,c_HOL_Oabs(v_h(c_0),t_a),t_a)
| ~ c_lessequals(c_0,v_x,t_a)
| class_Ring__and__Field_Opordered__cancel__semiring(t_a) ),
inference(resolution,[],[f1254134,f4704]) ).
fof(f1441004,plain,
( ~ c_lessequals(c_0,v_x,t_a)
| class_Ring__and__Field_Opordered__cancel__semiring(t_a) ),
inference(forward_subsumption_resolution,[],[f1441001,f65230]) ).
fof(f1441005,plain,
( class_Ring__and__Field_Opordered__cancel__semiring(t_a)
| spl0_21 ),
inference(forward_subsumption_resolution,[],[f1441004,f8783]) ).
fof(f1441006,plain,
( $false
| spl0_21
| spl0_99 ),
inference(forward_subsumption_resolution,[],[f1441005,f15691]) ).
fof(f1441007,plain,
( spl0_21
| spl0_99 ),
inference(avatar_contradiction_clause,[],[f1441006]) ).
cnf(s35,plain,
~ spl0_21,
inference(sat_conversion,[],[f7976]) ).
cnf(s135,plain,
~ spl0_99,
inference(sat_conversion,[],[f15721]) ).
cnf(s13973,plain,
( spl0_21
| spl0_99 ),
inference(sat_conversion,[],[f1441007]) ).
cnf(s14238,plain,
spl0_21,
inference(rat,[],[s13973,s135]) ).
cnf(s14285,plain,
$false,
inference(rat,[],[s35,s14238]) ).
fof(f1441008,plain,
$false,
inference(avatar_sat_refutation,[],[s14285]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ANA019-1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.19 % Computer : n020.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.19 % CPULimit : 300
% 0.10/0.19 % WCLimit : 300
% 0.10/0.19 % DateTime : Mon Sep 28 20:29:50 UTC 2026
% 0.10/0.19 % CPUTime :
% 0.10/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.22 Running first-order model finding
% 0.10/0.22 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 12.33/2.08 % (500767)Will run a generic schedule for satisfiability detection.
% 12.33/2.08 % (500773)% WARNING: option uhcvi not known.
% 12.33/2.08 % (500773)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1459993519:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 12.33/2.08 % (500772)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2104245989_2999 on theBenchmark for (2999ds/0Mi)
% 12.33/2.08 % (500774)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2738034511:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 12.33/2.08 % (500775)dis+10_1_sil=32000:sp=arity:random_seed=245614333:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 12.33/2.08 % (500776)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1803572596:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 12.33/2.08 % (500777)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=707498265:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 12.33/2.08 % (500778)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3302127898:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 12.33/2.08 % (500775)Instruction limit reached!
% 12.33/2.08 % (500775)------------------------------
% 12.33/2.08 % (500775)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.33/2.08 % (500775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.33/2.08 % (500775)CaDiCaL version: 2.1.3
% 12.33/2.08 % (500775)Termination reason: Instruction limit
% 12.33/2.08 % (500775)Termination phase: Saturation
% 12.33/2.08 % (500775)Time elapsed: 0.058 s
% 12.33/2.08 % (500775)Peak memory usage: 15 MB
% 12.33/2.08 % (500775)Instructions burned: 103 (million)
% 12.33/2.08 % (500776)Instruction limit reached!
% 12.33/2.08 % (500776)------------------------------
% 12.33/2.08 % (500776)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.33/2.08 % (500776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.33/2.08 % (500776)CaDiCaL version: 2.1.3
% 12.33/2.08 % (500776)Termination reason: Instruction limit
% 12.33/2.08 % (500776)Termination phase: Saturation
% 12.33/2.08 % (500776)Time elapsed: 0.063 s
% 12.33/2.08 % (500776)Peak memory usage: 15 MB
% 12.33/2.08 % (500776)Instructions burned: 117 (million)
% 12.33/2.08 % (500777)Instruction limit reached!
% 12.33/2.08 % (500777)------------------------------
% 12.33/2.08 % (500777)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.33/2.08 % (500777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.33/2.08 % (500777)CaDiCaL version: 2.1.3
% 12.33/2.08 % (500777)Termination reason: Instruction limit
% 12.33/2.08 % (500777)Termination phase: Saturation
% 12.33/2.08 % (500777)Time elapsed: 0.075 s
% 12.33/2.08 % (500777)Peak memory usage: 16 MB
% 12.33/2.08 % (500777)Instructions burned: 132 (million)
% 12.33/2.08 % (500786)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=701567014:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 12.33/2.08 % (500787)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2690194319:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 12.33/2.08 % (500788)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=2838937817:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 12.33/2.08 % (500778)Instruction limit reached!
% 12.33/2.08 % (500778)------------------------------
% 12.33/2.08 % (500778)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.33/2.08 % (500778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.33/2.08 % (500778)CaDiCaL version: 2.1.3
% 12.33/2.08 % (500778)Termination reason: Instruction limit
% 12.33/2.08 % (500778)Termination phase: Saturation
% 12.33/2.08 % (500778)Time elapsed: 0.093 s
% 12.33/2.08 % (500778)Peak memory usage: 16 MB
% 12.33/2.08 % (500778)Instructions burned: 159 (million)
% 12.33/2.08 % (500792)ott-21_1_sil=16000:fs=off:random_seed=983378273:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 12.33/2.08 % (500787)Instruction limit reached!
% 12.33/2.08 % (500787)------------------------------
% 12.33/2.08 % (500787)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.33/2.08 % (500787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.33/2.08 % (500787)CaDiCaL version: 2.1.3
% 12.33/2.08 % (500787)Termination reason: Instruction limit
% 46.19/6.91 % (500787)Termination phase: Saturation
% 46.19/6.91 % (500787)Time elapsed: 0.073 s
% 46.19/6.91 % (500787)Peak memory usage: 16 MB
% 46.19/6.91 % (500787)Instructions burned: 131 (million)
% 46.19/6.91 % (500794)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2704992700:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 46.19/6.91 % (500792)Instruction limit reached!
% 46.19/6.91 % (500792)------------------------------
% 46.19/6.91 % (500792)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.19/6.91 % (500792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.19/6.91 % (500792)CaDiCaL version: 2.1.3
% 46.19/6.91 % (500792)Termination reason: Instruction limit
% 46.19/6.91 % (500792)Termination phase: Saturation
% 46.19/6.91 % (500792)Time elapsed: 0.099 s
% 46.19/6.91 % (500792)Peak memory usage: 16 MB
% 46.19/6.91 % (500792)Instructions burned: 181 (million)
% 46.19/6.91 % (500796)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2273317202:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 46.19/6.91 % TRYING [1]
% 46.19/6.91 % TRYING [2]
% 46.19/6.91 % TRYING [1]
% 46.19/6.91 % TRYING [2]
% 46.19/6.91 % (500786)Instruction limit reached!
% 46.19/6.91 % (500786)------------------------------
% 46.19/6.91 % (500786)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.19/6.91 % (500786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.19/6.91 % (500786)CaDiCaL version: 2.1.3
% 46.19/6.91 % (500786)Termination reason: Instruction limit
% 46.19/6.91 % (500786)Termination phase: Finite model building constraint generation
% 46.19/6.91 % (500786)Time elapsed: 0.333 s
% 46.19/6.91 % (500786)Peak memory usage: 26 MB
% 46.19/6.91 % (500786)Instructions burned: 716 (million)
% 46.19/6.91 % (500798)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=929279459:i=1179_2994 on theBenchmark for (2994ds/1179Mi)
% 46.19/6.91 % (500788)Instruction limit reached!
% 46.19/6.91 % (500788)------------------------------
% 46.19/6.91 % (500788)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.19/6.91 % (500788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.19/6.91 % (500788)CaDiCaL version: 2.1.3
% 46.19/6.91 % (500788)Termination reason: Instruction limit
% 46.19/6.91 % (500788)Termination phase: Saturation
% 46.19/6.91 % (500788)Time elapsed: 0.369 s
% 46.19/6.91 % (500788)Peak memory usage: 22 MB
% 46.19/6.91 % (500788)Instructions burned: 684 (million)
% 46.19/6.91 % (500794)Instruction limit reached!
% 46.19/6.91 % (500794)------------------------------
% 46.19/6.91 % (500794)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.19/6.91 % (500794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.19/6.91 % (500794)CaDiCaL version: 2.1.3
% 46.19/6.91 % (500794)Termination reason: Instruction limit
% 46.19/6.91 % (500794)Termination phase: Saturation
% 46.19/6.91 % (500794)Time elapsed: 0.298 s
% 46.19/6.91 % (500794)Peak memory usage: 17 MB
% 46.19/6.91 % (500794)Instructions burned: 477 (million)
% 46.19/6.91 % (500800)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2020818243:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 46.19/6.91 % (500801)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=2777376949:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 46.19/6.91 % TRYING [1]
% 46.19/6.91 % (500796)Instruction limit reached!
% 46.19/6.91 % (500796)------------------------------
% 46.19/6.91 % (500796)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.19/6.91 % (500796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.19/6.91 % (500796)CaDiCaL version: 2.1.3
% 46.19/6.91 % (500796)Termination reason: Instruction limit
% 46.19/6.91 % (500796)Termination phase: Finite model building constraint generation
% 46.19/6.91 % (500796)Time elapsed: 0.426 s
% 46.19/6.91 % (500796)Peak memory usage: 50 MB
% 46.19/6.91 % (500796)Instructions burned: 867 (million)
% 46.19/6.91 % (500804)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1409059255:i=879:kws=inv_precedence:fsr=off_2992 on theBenchmark for (2992ds/879Mi)
% 46.19/6.91 % (500800)Cannot represent all propositional literals internally
% 46.19/6.91 % (500800)Refutation not found, incomplete strategy
% 46.19/6.91 % (500800)------------------------------
% 46.19/6.91 % (500800)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.19/6.91 % (500800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.23/10.91 % (500800)CaDiCaL version: 2.1.3
% 75.23/10.91 % (500800)Termination reason: Refutation not found, incomplete strategy
% 75.23/10.91 % (500800)Time elapsed: 0.282 s
% 75.23/10.91 % (500800)Peak memory usage: 23 MB
% 75.23/10.91 % (500800)Instructions burned: 577 (million)
% 75.23/10.91 % (500800)------------------------------
% 75.23/10.91 % (500800)------------------------------
% 75.23/10.91 % (500806)fmb+10_1_sil=64000:random_seed=1477600963:i=22061:nm=2:gsp=on_2991 on theBenchmark for (2991ds/22061Mi)
% 75.23/10.91 % (500801)Instruction limit reached!
% 75.23/10.91 % (500801)------------------------------
% 75.23/10.91 % (500801)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 75.23/10.91 % (500801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.23/10.91 % (500801)CaDiCaL version: 2.1.3
% 75.23/10.91 % (500801)Termination reason: Instruction limit
% 75.23/10.91 % (500801)Termination phase: Saturation
% 75.23/10.91 % (500801)Time elapsed: 0.312 s
% 75.23/10.91 % (500801)Peak memory usage: 18 MB
% 75.23/10.91 % (500801)Instructions burned: 693 (million)
% 75.23/10.91 % (500808)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3839654817:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 75.23/10.92 % TRYING [1]
% 75.23/10.92 % (500808)Cannot represent all propositional literals internally
% 75.23/10.92 % (500808)Refutation not found, incomplete strategy
% 75.23/10.92 % (500808)------------------------------
% 75.23/10.92 % (500808)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 75.23/10.92 % (500808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.23/10.92 % (500808)CaDiCaL version: 2.1.3
% 75.23/10.92 % (500808)Termination reason: Refutation not found, incomplete strategy
% 75.23/10.92 % (500808)Time elapsed: 0.284 s
% 75.23/10.92 % (500808)Peak memory usage: 23 MB
% 75.23/10.92 % (500808)Instructions burned: 573 (million)
% 75.23/10.92 % (500804)Instruction limit reached!
% 75.23/10.92 % (500804)------------------------------
% 75.23/10.92 % (500804)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 75.23/10.92 % (500804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.23/10.92 % (500804)CaDiCaL version: 2.1.3
% 75.23/10.92 % (500804)Termination reason: Instruction limit
% 75.23/10.92 % (500804)Termination phase: Saturation
% 75.23/10.92 % (500804)Time elapsed: 0.429 s
% 75.23/10.92 % (500804)Peak memory usage: 21 MB
% 75.23/10.92 % (500804)Instructions burned: 879 (million)
% 75.23/10.92 % (500808)------------------------------
% 75.23/10.92 % (500808)------------------------------
% 75.23/10.92 % (500810)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=876041226:fmbsr=1.7:i=920_2987 on theBenchmark for (2987ds/920Mi)
% 75.23/10.92 % (500811)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3104051699:i=5131_2987 on theBenchmark for (2987ds/5131Mi)
% 75.23/10.92 % (500798)Instruction limit reached!
% 75.23/10.92 % (500798)------------------------------
% 75.23/10.92 % (500798)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 75.23/10.92 % (500798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.23/10.92 % (500798)CaDiCaL version: 2.1.3
% 75.23/10.92 % (500798)Termination reason: Instruction limit
% 75.23/10.92 % (500798)Termination phase: Saturation
% 75.23/10.92 % (500798)Time elapsed: 0.741 s
% 75.23/10.92 % (500798)Peak memory usage: 26 MB
% 75.23/10.92 % (500798)Instructions burned: 1180 (million)
% 75.23/10.92 % (500815)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=333063723:i=1472:ins=7:fdi=8:gsp=on_2987 on theBenchmark for (2987ds/1472Mi)
% 75.23/10.92 % (500810)Cannot represent all propositional literals internally
% 75.23/10.92 % (500810)Refutation not found, incomplete strategy
% 75.23/10.92 % (500810)------------------------------
% 75.23/10.92 % (500810)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 75.23/10.92 % (500810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.23/10.92 % (500810)CaDiCaL version: 2.1.3
% 75.23/10.92 % (500810)Termination reason: Refutation not found, incomplete strategy
% 75.23/10.92 % (500810)Time elapsed: 0.284 s
% 75.23/10.92 % (500810)Peak memory usage: 23 MB
% 75.23/10.92 % (500810)Instructions burned: 573 (million)
% 75.23/10.92 % (500810)------------------------------
% 75.23/10.92 % (500810)------------------------------
% 75.23/10.92 % (500817)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=4211899182:i=6324_2984 on theBenchmark for (2984ds/6324Mi)
% 75.23/10.92 % TRYING [2]
% 75.23/10.92 % (500817)Cannot represent all propositional literals internally
% 104.55/15.08 % (500817)Refutation not found, incomplete strategy
% 104.55/15.08 % (500817)------------------------------
% 104.55/15.08 % (500817)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 104.55/15.08 % (500817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 104.55/15.08 % (500817)CaDiCaL version: 2.1.3
% 104.55/15.08 % (500817)Termination reason: Refutation not found, incomplete strategy
% 104.55/15.08 % (500817)Time elapsed: 0.294 s
% 104.55/15.08 % (500817)Peak memory usage: 23 MB
% 104.55/15.08 % (500817)Instructions burned: 594 (million)
% 104.55/15.08 % (500817)------------------------------
% 104.55/15.08 % (500817)------------------------------
% 104.55/15.08 % (500819)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3715940171:fmbsr=2.30978:i=2174_2981 on theBenchmark for (2981ds/2174Mi)
% 104.55/15.08 % (500815)Instruction limit reached!
% 104.55/15.08 % (500815)------------------------------
% 104.55/15.08 % (500815)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 104.55/15.08 % (500815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 104.55/15.08 % (500815)CaDiCaL version: 2.1.3
% 104.55/15.08 % (500815)Termination reason: Instruction limit
% 104.55/15.08 % (500815)Termination phase: Saturation
% 104.55/15.08 % (500815)Time elapsed: 0.776 s
% 104.55/15.08 % (500815)Peak memory usage: 32 MB
% 104.55/15.08 % (500815)Instructions burned: 1472 (million)
% 104.55/15.08 % (500821)ott-2_1_sil=16000:newcnf=on:random_seed=3936837507:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2979 on theBenchmark for (2979ds/869Mi)
% 104.55/15.08 % (500821)Instruction limit reached!
% 104.55/15.08 % (500821)------------------------------
% 104.55/15.08 % (500821)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 104.55/15.08 % (500821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 104.55/15.08 % (500821)CaDiCaL version: 2.1.3
% 104.55/15.08 % (500821)Termination reason: Instruction limit
% 104.55/15.08 % (500821)Termination phase: Saturation
% 104.55/15.08 % (500821)Time elapsed: 0.521 s
% 104.55/15.08 % (500821)Peak memory usage: 21 MB
% 104.55/15.08 % (500821)Instructions burned: 869 (million)
% 104.55/15.08 % (500823)ott+10_1_sil=32000:tgt=ground:random_seed=3019372289:i=5114:av=off_2973 on theBenchmark for (2973ds/5114Mi)
% 104.55/15.08 % (500819)Instruction limit reached!
% 104.55/15.08 % (500819)------------------------------
% 104.55/15.08 % (500819)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 104.55/15.08 % (500819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 104.55/15.08 % (500819)CaDiCaL version: 2.1.3
% 104.55/15.08 % (500819)Termination reason: Instruction limit
% 104.55/15.08 % (500819)Termination phase: Finite model building preprocessing
% 104.55/15.08 % (500819)Time elapsed: 1.098 s
% 104.55/15.08 % (500819)Peak memory usage: 41 MB
% 104.55/15.08 % (500819)Instructions burned: 2176 (million)
% 104.55/15.08 % (500825)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2313394007:i=54282_2970 on theBenchmark for (2970ds/54282Mi)
% 104.55/15.08 % TRYING [1]
% 104.55/15.08 % TRYING [2]
% 104.55/15.08 % (500811)Instruction limit reached!
% 104.55/15.08 % (500811)------------------------------
% 104.55/15.08 % (500811)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 104.55/15.08 % (500811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 104.55/15.08 % (500811)CaDiCaL version: 2.1.3
% 104.55/15.08 % (500811)Termination reason: Instruction limit
% 104.55/15.08 % (500811)Termination phase: Saturation
% 104.55/15.08 % (500811)Time elapsed: 3.268 s
% 104.55/15.08 % (500811)Peak memory usage: 53 MB
% 104.55/15.08 % (500811)Instructions burned: 5131 (million)
% 104.55/15.08 % (500827)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2475978192:i=3512:aac=none_2954 on theBenchmark for (2954ds/3512Mi)
% 104.55/15.08 % (500823)Instruction limit reached!
% 104.55/15.08 % (500823)------------------------------
% 104.55/15.08 % (500823)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 104.55/15.08 % (500823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 104.55/15.08 % (500823)CaDiCaL version: 2.1.3
% 104.55/15.08 % (500823)Termination reason: Instruction limit
% 104.55/15.08 % (500823)Termination phase: Saturation
% 104.55/15.08 % (500823)Time elapsed: 3.363 s
% 104.55/15.08 % (500823)Peak memory usage: 57 MB
% 104.55/15.08 % (500823)Instructions burned: 5115 (million)
% 104.55/15.08 % (500829)dis+21_1_sil=32000:sas=cadical:random_seed=2511725227:i=3773:amm=off_2939 on theBenchmark for (2939ds/3773Mi)
% 104.55/15.08 % (500827)Instruction limit reached!
% 104.55/15.08 % (500827)------------------------------
% 104.55/15.08 % (500827)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 188.77/27.02 % (500827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 188.77/27.02 % (500827)CaDiCaL version: 2.1.3
% 188.77/27.02 % (500827)Termination reason: Instruction limit
% 188.77/27.02 % (500827)Termination phase: Saturation
% 188.77/27.02 % (500827)Time elapsed: 2.140 s
% 188.77/27.02 % (500827)Peak memory usage: 42 MB
% 188.77/27.02 % (500827)Instructions burned: 3512 (million)
% 188.77/27.02 % (500831)ott+11_1_sil=16000:gs=on:random_seed=303716205:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2933 on theBenchmark for (2933ds/2251Mi)
% 188.77/27.02 % (500772)Cannot represent all propositional literals internally
% 188.77/27.02 % (500831)Instruction limit reached!
% 188.77/27.02 % (500831)------------------------------
% 188.77/27.02 % (500831)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 188.77/27.02 % (500831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 188.77/27.02 % (500831)CaDiCaL version: 2.1.3
% 188.77/27.02 % (500831)Termination reason: Instruction limit
% 188.77/27.02 % (500831)Termination phase: Saturation
% 188.77/27.02 % (500831)Time elapsed: 1.325 s
% 188.77/27.02 % (500831)Peak memory usage: 37 MB
% 188.77/27.02 % (500831)Instructions burned: 2252 (million)
% 188.77/27.02 % (500833)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1245774824:fmbsr=1.6:i=67534_2919 on theBenchmark for (2919ds/67534Mi)
% 188.77/27.02 % (500833)Cannot represent all propositional literals internally
% 188.77/27.02 % (500833)Refutation not found, incomplete strategy
% 188.77/27.02 % (500833)------------------------------
% 188.77/27.02 % (500833)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 188.77/27.02 % (500833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 188.77/27.02 % (500833)CaDiCaL version: 2.1.3
% 188.77/27.02 % (500833)Termination reason: Refutation not found, incomplete strategy
% 188.77/27.02 % (500833)Time elapsed: 0.293 s
% 188.77/27.02 % (500833)Peak memory usage: 21 MB
% 188.77/27.02 % (500833)Instructions burned: 603 (million)
% 188.77/27.02 % (500833)------------------------------
% 188.77/27.02 % (500833)------------------------------
% 188.77/27.02 % (500835)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=763362231:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2916 on theBenchmark for (2916ds/4591Mi)
% 188.77/27.02 % (500829)Instruction limit reached!
% 188.77/27.02 % (500829)------------------------------
% 188.77/27.02 % (500829)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 188.77/27.02 % (500829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 188.77/27.02 % (500829)CaDiCaL version: 2.1.3
% 188.77/27.02 % (500829)Termination reason: Instruction limit
% 188.77/27.02 % (500829)Termination phase: Saturation
% 188.77/27.02 % (500829)Time elapsed: 2.381 s
% 188.77/27.02 % (500829)Peak memory usage: 43 MB
% 188.77/27.02 % (500829)Instructions burned: 3773 (million)
% 188.77/27.02 % (500837)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=461686126:i=29340_2915 on theBenchmark for (2915ds/29340Mi)
% 188.77/27.02 % (500772)Refutation not found, incomplete strategy
% 188.77/27.02 % (500772)------------------------------
% 188.77/27.02 % (500772)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 188.77/27.02 % (500772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 188.77/27.02 % (500772)CaDiCaL version: 2.1.3
% 188.77/27.02 % (500772)Termination reason: Refutation not found, incomplete strategy
% 188.77/27.02 % (500772)Time elapsed: 8.786 s
% 188.77/27.02 % (500772)Peak memory usage: 978 MB
% 188.77/27.02 % (500772)Instructions burned: 14699 (million)
% 188.77/27.02 % (500772)------------------------------
% 188.77/27.02 % (500772)------------------------------
% 188.77/27.02 % (500839)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2846657684:i=5211_2909 on theBenchmark for (2909ds/5211Mi)
% 188.77/27.02 % (500835)Instruction limit reached!
% 188.77/27.02 % (500835)------------------------------
% 188.77/27.02 % (500835)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 188.77/27.02 % (500835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 188.77/27.02 % (500835)CaDiCaL version: 2.1.3
% 188.77/27.02 % (500835)Termination reason: Instruction limit
% 188.77/27.02 % (500835)Termination phase: Saturation
% 188.77/27.02 % (500835)Time elapsed: 2.287 s
% 188.77/27.02 % (500835)Peak memory usage: 51 MB
% 188.77/27.02 % (500835)Instructions burned: 4592 (million)
% 188.77/27.02 % (500841)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=313720402:i=5497:nm=2_2893 on theBenchmark for (2893ds/5497Mi)
% 207.01/29.60 % (500825)Cannot represent all propositional literals internally
% 207.01/29.60 % (500841)Cannot represent all propositional literals internally
% 207.01/29.60 % (500841)Refutation not found, incomplete strategy
% 207.01/29.60 % (500841)------------------------------
% 207.01/29.60 % (500841)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 207.01/29.60 % (500841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 207.01/29.60 % (500841)CaDiCaL version: 2.1.3
% 207.01/29.60 % (500841)Termination reason: Refutation not found, incomplete strategy
% 207.01/29.60 % (500841)Time elapsed: 0.300 s
% 207.01/29.60 % (500841)Peak memory usage: 23 MB
% 207.01/29.60 % (500841)Instructions burned: 594 (million)
% 207.01/29.60 % (500841)------------------------------
% 207.01/29.60 % (500841)------------------------------
% 207.01/29.60 % (500843)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1082581310:fmbsr=2:i=46332_2890 on theBenchmark for (2890ds/46332Mi)
% 207.01/29.60 % (500843)Cannot represent all propositional literals internally
% 207.01/29.60 % (500843)Refutation not found, incomplete strategy
% 207.01/29.60 % (500843)------------------------------
% 207.01/29.60 % (500843)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 207.01/29.60 % (500843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 207.01/29.60 % (500843)CaDiCaL version: 2.1.3
% 207.01/29.60 % (500843)Termination reason: Refutation not found, incomplete strategy
% 207.01/29.60 % (500843)Time elapsed: 0.293 s
% 207.01/29.60 % (500843)Peak memory usage: 21 MB
% 207.01/29.60 % (500843)Instructions burned: 603 (million)
% 207.01/29.60 % (500843)------------------------------
% 207.01/29.60 % (500843)------------------------------
% 207.01/29.60 % (500845)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2551932670:i=14071_2886 on theBenchmark for (2886ds/14071Mi)
% 207.01/29.60 % (500839)Instruction limit reached!
% 207.01/29.60 % (500839)------------------------------
% 207.01/29.60 % (500839)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 207.01/29.60 % (500839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 207.01/29.60 % (500839)CaDiCaL version: 2.1.3
% 207.01/29.60 % (500839)Termination reason: Instruction limit
% 207.01/29.60 % (500839)Termination phase: Saturation
% 207.01/29.60 % (500839)Time elapsed: 2.523 s
% 207.01/29.60 % (500839)Peak memory usage: 45 MB
% 207.01/29.60 % (500839)Instructions burned: 5212 (million)
% 207.01/29.60 % (500847)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3961675481:i=22565:add=on:rawr=on_2884 on theBenchmark for (2884ds/22565Mi)
% 207.01/29.60 % (500845)Cannot represent all propositional literals internally
% 207.01/29.60 % (500845)Refutation not found, incomplete strategy
% 207.01/29.60 % (500845)------------------------------
% 207.01/29.60 % (500845)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 207.01/29.60 % (500845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 207.01/29.60 % (500845)CaDiCaL version: 2.1.3
% 207.01/29.60 % (500845)Termination reason: Refutation not found, incomplete strategy
% 207.01/29.60 % (500845)Time elapsed: 0.287 s
% 207.01/29.60 % (500845)Peak memory usage: 23 MB
% 207.01/29.60 % (500845)Instructions burned: 573 (million)
% 207.01/29.60 % (500845)------------------------------
% 207.01/29.60 % (500845)------------------------------
% 207.01/29.60 % (500849)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=901800060:i=8173:av=off_2883 on theBenchmark for (2883ds/8173Mi)
% 207.01/29.60 % (500825)Refutation not found, incomplete strategy
% 207.01/29.60 % (500825)------------------------------
% 207.01/29.60 % (500825)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 207.01/29.60 % (500825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 207.01/29.60 % (500825)CaDiCaL version: 2.1.3
% 207.01/29.60 % (500825)Termination reason: Refutation not found, incomplete strategy
% 207.01/29.60 % (500825)Time elapsed: 8.871 s
% 207.01/29.60 % (500825)Peak memory usage: 978 MB
% 207.01/29.60 % (500825)Instructions burned: 14700 (million)
% 207.01/29.60 % (500825)------------------------------
% 207.01/29.60 % (500825)------------------------------
% 207.01/29.60 % (500851)dis+10_16:1_sil=16000:random_seed=3502736277:i=9155:fsr=off_2880 on theBenchmark for (2880ds/9155Mi)
% 207.01/29.60 % (500806)Instruction limit reached!
% 207.01/29.60 % (500806)------------------------------
% 207.01/29.60 % (500806)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 207.01/29.60 % (500806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 199.31/33.72 % (500806)CaDiCaL version: 2.1.3
% 199.31/33.72 % (500806)Termination reason: Instruction limit
% 199.31/33.72 % (500806)Termination phase: Finite model building SAT solving
% 199.31/33.72 % (500806)Time elapsed: 13.951 s
% 199.31/33.72 % (500806)Peak memory usage: 737 MB
% 199.31/33.72 % (500806)Instructions burned: 22063 (million)
% 199.31/33.72 % (500853)ott-3_8_sil=64000:random_seed=3332628402:i=20139:bs=on_2850 on theBenchmark for (2850ds/20139Mi)
% 199.31/33.72 % (500849)Instruction limit reached!
% 199.31/33.72 % (500849)------------------------------
% 199.31/33.72 % (500849)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 199.31/33.72 % (500849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 199.31/33.72 % (500849)CaDiCaL version: 2.1.3
% 199.31/33.72 % (500849)Termination reason: Instruction limit
% 199.31/33.72 % (500849)Termination phase: Saturation
% 199.31/33.72 % (500849)Time elapsed: 5.337 s
% 199.31/33.72 % (500849)Peak memory usage: 78 MB
% 199.31/33.72 % (500849)Instructions burned: 8173 (million)
% 199.31/33.72 % (500855)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=4032268981:fmbsr=2:i=32576_2830 on theBenchmark for (2830ds/32576Mi)
% 199.31/33.72 % (500851)Instruction limit reached!
% 199.31/33.72 % (500851)------------------------------
% 199.31/33.72 % (500851)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 199.31/33.72 % (500851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 199.31/33.72 % (500851)CaDiCaL version: 2.1.3
% 199.31/33.72 % (500851)Termination reason: Instruction limit
% 199.31/33.72 % (500851)Termination phase: Saturation
% 199.31/33.72 % (500851)Time elapsed: 5.140 s
% 199.31/33.72 % (500851)Peak memory usage: 87 MB
% 199.31/33.72 % (500851)Instructions burned: 9156 (million)
% 199.31/33.72 % (500857)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=4019007622:i=11404_2828 on theBenchmark for (2828ds/11404Mi)
% 199.31/33.72 % (500855)Cannot represent all propositional literals internally
% 199.31/33.72 % (500855)Refutation not found, incomplete strategy
% 199.31/33.72 % (500855)------------------------------
% 199.31/33.72 % (500855)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 199.31/33.72 % (500855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 199.31/33.72 % (500855)CaDiCaL version: 2.1.3
% 199.31/33.72 % (500855)Termination reason: Refutation not found, incomplete strategy
% 199.31/33.72 % (500855)Time elapsed: 0.296 s
% 199.31/33.72 % (500855)Peak memory usage: 23 MB
% 199.31/33.72 % (500855)Instructions burned: 595 (million)
% 199.31/33.72 % (500855)------------------------------
% 199.31/33.72 % (500855)------------------------------
% 199.31/33.72 % (500859)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3001988884:i=14134_2826 on theBenchmark for (2826ds/14134Mi)
% 199.31/33.72 % (500837)Instruction limit reached!
% 199.31/33.72 % (500837)------------------------------
% 199.31/33.72 % (500837)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 199.31/33.72 % (500837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 199.31/33.72 % (500837)CaDiCaL version: 2.1.3
% 199.31/33.72 % (500837)Termination reason: Instruction limit
% 199.31/33.72 % (500837)Termination phase: Saturation
% 199.31/33.72 % (500837)Time elapsed: 16.164 s
% 199.31/33.72 % (500837)Peak memory usage: 507 MB
% 199.31/33.72 % (500837)Instructions burned: 29340 (million)
% 199.31/33.72 % (500861)dis+33_16_sil=32000:sac=on:random_seed=1181214293:i=15851:nm=0_2753 on theBenchmark for (2753ds/15851Mi)
% 199.31/33.72 % (500857)Instruction limit reached!
% 199.31/33.72 % (500857)------------------------------
% 199.31/33.72 % (500857)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 199.31/33.72 % (500857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 199.31/33.72 % (500857)CaDiCaL version: 2.1.3
% 199.31/33.72 % (500857)Termination reason: Instruction limit
% 199.31/33.72 % (500857)Termination phase: Saturation
% 199.31/33.72 % (500857)Time elapsed: 7.614 s
% 199.31/33.72 % (500857)Peak memory usage: 140 MB
% 199.31/33.72 % (500857)Instructions burned: 11404 (million)
% 199.31/33.72 % (500863)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=130705814:avsq=on:i=17627:add=on:amm=off_2751 on theBenchmark for (2751ds/17627Mi)
% 199.31/33.72 % (500859)Instruction limit reached!
% 199.31/33.72 % (500859)------------------------------
% 199.31/33.72 % (500859)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 199.31/33.72 % (500859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 199.31/33.72 % (500859)CaDiCaL version: 2.1.3
% 199.31/33.72 % (500859)Termination reason: Instruction limit
% 199.31/33.72 % (500859)Termination phase: Saturation
% 199.31/33.72 % (500859)Time elapsed: 9.452 s
% 199.31/33.72 % (500859)Peak memory usage: 121 MB
% 199.31/33.72 % (500859)Instructions burned: 14135 (million)
% 199.31/33.72 % (500865)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=2047981260:s2a=on:i=53295_2731 on theBenchmark for (2731ds/53295Mi)
% 199.31/33.72 % (500847)Instruction limit reached!
% 199.31/33.72 % (500847)------------------------------
% 199.31/33.72 % (500847)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 199.31/33.72 % (500847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 199.31/33.72 % (500847)CaDiCaL version: 2.1.3
% 199.31/33.72 % (500847)Termination reason: Instruction limit
% 199.31/33.72 % (500847)Termination phase: Saturation
% 199.31/33.72 % (500847)Time elapsed: 15.391 s
% 199.31/33.72 % (500847)Peak memory usage: 456 MB
% 199.31/33.72 % (500847)Instructions burned: 22567 (million)
% 199.31/33.72 % (500867)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=3683393480:i=26857:ins=20_2729 on theBenchmark for (2729ds/26857Mi)
% 199.31/33.72 % (500867)Cannot represent all propositional literals internally
% 199.31/33.72 % (500867)Refutation not found, incomplete strategy
% 199.31/33.72 % (500867)------------------------------
% 199.31/33.72 % (500867)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 199.31/33.72 % (500867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 199.31/33.72 % (500867)CaDiCaL version: 2.1.3
% 199.31/33.72 % (500867)Termination reason: Refutation not found, incomplete strategy
% 199.31/33.72 % (500867)Time elapsed: 0.288 s
% 199.31/33.72 % (500867)Peak memory usage: 23 MB
% 199.31/33.72 % (500867)Instructions burned: 574 (million)
% 199.31/33.72 % (500867)------------------------------
% 199.31/33.72 % (500867)------------------------------
% 199.31/33.72 % (500869)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=517729857:i=28120:bs=on:fsr=off_2726 on theBenchmark for (2726ds/28120Mi)
% 199.31/33.72 % (500853)Instruction limit reached!
% 199.31/33.72 % (500853)------------------------------
% 199.31/33.72 % (500853)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 199.31/33.72 % (500853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 199.31/33.72 % (500853)CaDiCaL version: 2.1.3
% 199.31/33.72 % (500853)Termination reason: Instruction limit
% 199.31/33.72 % (500853)Termination phase: Saturation
% 199.31/33.72 % (500853)Time elapsed: 13.442 s
% 199.31/33.72 % (500853)Peak memory usage: 144 MB
% 199.31/33.72 % (500853)Instructions burned: 20139 (million)
% 199.31/33.72 % (500871)fmb+10_1_sil=256000:fmbss=7:random_seed=2683874647:fmbsr=1.6:i=182295_2715 on theBenchmark for (2715ds/182295Mi)
% 199.31/33.72 % (500871)Cannot represent all propositional literals internally
% 199.31/33.72 % (500871)Refutation not found, incomplete strategy
% 199.31/33.72 % (500871)------------------------------
% 199.31/33.72 % (500871)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 199.31/33.72 % (500871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 199.31/33.72 % (500871)CaDiCaL version: 2.1.3
% 199.31/33.72 % (500871)Termination reason: Refutation not found, incomplete strategy
% 199.31/33.72 % (500871)Time elapsed: 0.285 s
% 199.31/33.72 % (500871)Peak memory usage: 23 MB
% 199.31/33.72 % (500871)Instructions burned: 573 (million)
% 199.31/33.72 % (500871)------------------------------
% 199.31/33.72 % (500871)------------------------------
% 199.31/33.72 % (500873)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=3086386588:i=44625:gsp=on_2712 on theBenchmark for (2712ds/44625Mi)
% 199.31/33.72 % (500873)Cannot represent all propositional literals internally
% 199.31/33.72 % (500873)Refutation not found, incomplete strategy
% 199.31/33.72 % (500873)------------------------------
% 199.31/33.72 % (500873)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 199.31/33.72 % (500873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 199.31/33.72 % (500873)CaDiCaL version: 2.1.3
% 199.31/33.72 % (500873)Termination reason: Refutation not found, incomplete strategy
% 199.31/33.72 % (500873)Time elapsed: 0.288 s
% 199.31/33.72 % (500873)Peak memory usage: 23 MB
% 199.31/33.72 % (500873)Instructions burned: 581 (million)
% 199.31/33.72 % (500873)------------------------------
% 199.31/33.72 % (500873)------------------------------
% 199.31/33.72 % (500875)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=2829226835:i=160505_2709 on theBenchmark for (2709ds/160505Mi)
% 199.31/33.72 % (500875)Cannot represent all propositional literals internally
% 199.31/33.72 % (500875)Refutation not found, incomplete strategy
% 199.31/33.72 % (500875)------------------------------
% 199.31/33.72 % (500875)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 199.31/33.72 % (500875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 199.31/33.72 % (500875)CaDiCaL version: 2.1.3
% 199.31/33.72 % (500875)Termination reason: Refutation not found, incomplete strategy
% 199.31/33.72 % (500875)Time elapsed: 0.285 s
% 199.31/33.72 % (500875)Peak memory usage: 23 MB
% 199.31/33.72 % (500875)Instructions burned: 573 (million)
% 199.31/33.72 % (500875)------------------------------
% 199.31/33.72 % (500875)------------------------------
% 199.31/33.72 % (500877)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=3111526536:fmbsr=1.3:i=225729_2706 on theBenchmark for (2706ds/225729Mi)
% 199.31/33.72 % (500877)Cannot represent all propositional literals internally
% 199.31/33.72 % (500877)Refutation not found, incomplete strategy
% 199.31/33.72 % (500877)------------------------------
% 199.31/33.72 % (500877)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 199.31/33.72 % (500877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 199.31/33.72 % (500877)CaDiCaL version: 2.1.3
% 199.31/33.72 % (500877)Termination reason: Refutation not found, incomplete strategy
% 199.31/33.72 % (500877)Time elapsed: 0.285 s
% 199.31/33.72 % (500877)Peak memory usage: 23 MB
% 199.31/33.72 % (500877)Instructions burned: 573 (million)
% 199.31/33.72 % (500877)------------------------------
% 199.31/33.72 % (500877)------------------------------
% 199.31/33.72 % (500879)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=2241008496:fmbsr=2:i=185024:ins=7_2703 on theBenchmark for (2703ds/185024Mi)
% 199.31/33.72 % (500879)Cannot represent all propositional literals internally
% 199.31/33.72 % (500879)Refutation not found, incomplete strategy
% 199.31/33.72 % (500879)------------------------------
% 199.31/33.72 % (500879)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 199.31/33.72 % (500879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 199.31/33.72 % (500879)CaDiCaL version: 2.1.3
% 199.31/33.72 % (500879)Termination reason: Refutation not found, incomplete strategy
% 199.31/33.72 % (500879)Time elapsed: 0.289 s
% 199.31/33.72 % (500879)Peak memory usage: 23 MB
% 199.31/33.72 % (500879)Instructions burned: 573 (million)
% 199.31/33.72 % (500879)------------------------------
% 199.31/33.72 % (500879)------------------------------
% 199.31/33.72 % (500881)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=4142418603:rtra=on_2699 on theBenchmark for (2699ds/0Mi)
% 199.31/33.72 % TRYING [1]
% 199.31/33.72 % TRYING [2]
% 199.31/33.72 % (500773) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-500767-500773"...
% 199.31/33.72 % (500773)...printing done.
% 199.31/33.72 % (500773)Refutation found. Thanks to Tanya!
% 199.31/33.72 % SZS status Unsatisfiable for theBenchmark
% 199.31/33.72 % SZS output start Proof for theBenchmark
% See solution above
% 199.31/33.72 % (500773)------------------------------
% 199.31/33.72 % (500773)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 199.31/33.72 % (500773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 199.31/33.72 % (500773)CaDiCaL version: 2.1.3
% 199.31/33.72 % (500773)Termination reason: Refutation
% 199.31/33.72 % (500773)Time elapsed: 33.199 s
% 199.31/33.72 % (500773)Peak memory usage: 547 MB
% 199.31/33.72 % (500773)Instructions burned: 97604 (million)
% 199.31/33.72 % (500767)Success in time 33.488 s
% 199.31/33.72 % Vampire exiting
%------------------------------------------------------------------------------