%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ANA028-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 : n005.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:20 AM UTC 2026
% Result : Unsatisfiable 17.75s 7.97s
% Output : Refutation 17.75s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 20
% Syntax : Number of formulae : 93 ( 37 unt; 0 def)
% Number of atoms : 157 ( 48 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 129 ( 65 ~; 64 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 5 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-3 aty)
% Number of functors : 9 ( 9 usr; 3 con; 0-3 aty)
% Number of variables : 215 ( 215 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1449,axiom,
! [X0,X1] :
( ~ class_OrderedGroup_Oab__group__add(X0)
| c_minus(c_0,X1,X0) = c_uminus(X1,X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_OrderedGroup_Odiff__0_0) ).
fof(f1450,plain,
! [X0,X1] :
( ~ class_OrderedGroup_Oab__group__add(X0)
| c_uminus(X1,X0) = c_minus(c_0,X1,X0) ),
inference(reorient_equations,[],[f1449]) ).
fof(f1451,axiom,
! [X0,X1] :
( ~ class_OrderedGroup_Oab__group__add(X0)
| c_minus(X1,c_0,X0) = X1 ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_OrderedGroup_Odiff__0__right_0) ).
fof(f1454,axiom,
! [X2,X0,X1] :
( ~ class_OrderedGroup_Opordered__ab__group__add(X0)
| ~ c_lessequals(c_minus(X1,X2,X0),c_0,X0)
| c_lessequals(X1,X2,X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_OrderedGroup_Odiff__le__0__iff__le_0) ).
fof(f1455,axiom,
! [X2,X0,X1] :
( ~ class_OrderedGroup_Opordered__ab__group__add(X0)
| ~ c_lessequals(X1,X2,X0)
| c_lessequals(c_minus(X1,X2,X0),c_0,X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_OrderedGroup_Odiff__le__0__iff__le_1) ).
fof(f1458,axiom,
! [X2,X0,X1] :
( ~ class_OrderedGroup_Oab__group__add(X0)
| c_minus(X1,c_uminus(X2,X0),X0) = c_plus(X1,X2,X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_OrderedGroup_Odiff__minus__eq__add_0) ).
fof(f1459,plain,
! [X2,X0,X1] :
( ~ class_OrderedGroup_Oab__group__add(X0)
| c_plus(X1,X2,X0) = c_minus(X1,c_uminus(X2,X0),X0) ),
inference(reorient_equations,[],[f1458]) ).
fof(f1460,axiom,
! [X0,X1] :
( ~ class_OrderedGroup_Oab__group__add(X0)
| c_minus(X1,X1,X0) = c_0 ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_OrderedGroup_Odiff__self_0) ).
fof(f1461,plain,
! [X0,X1] :
( ~ class_OrderedGroup_Oab__group__add(X0)
| c_0 = c_minus(X1,X1,X0) ),
inference(reorient_equations,[],[f1460]) ).
fof(f1475,axiom,
! [X2,X0,X1] :
( ~ class_OrderedGroup_Oab__group__add(X0)
| c_uminus(c_minus(X1,X2,X0),X0) = c_minus(X2,X1,X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_OrderedGroup_Ominus__diff__eq_0) ).
fof(f1476,plain,
! [X2,X0,X1] :
( ~ class_OrderedGroup_Oab__group__add(X0)
| c_minus(X2,X1,X0) = c_uminus(c_minus(X1,X2,X0),X0) ),
inference(reorient_equations,[],[f1475]) ).
fof(f3032,axiom,
! [X0] :
( class_OrderedGroup_Oab__group__add(X0)
| ~ class_Ring__and__Field_Oordered__idom(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-0.ax',clsrel_Ring__and__Field_Oordered__idom_4) ).
fof(f3048,axiom,
! [X0] :
( class_OrderedGroup_Opordered__ab__group__add(X0)
| ~ class_Ring__and__Field_Oordered__idom(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-0.ax',clsrel_Ring__and__Field_Oordered__idom_54) ).
fof(f3365,axiom,
! [X2,X0,X1] :
( ~ class_OrderedGroup_Oab__group__add(X0)
| c_plus(c_minus(X1,X2,X0),X2,X0) = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_OrderedGroup_Ocompare__rls__11_0) ).
fof(f3366,axiom,
! [X2,X0,X1] :
( ~ class_OrderedGroup_Oab__group__add(X0)
| X1 = c_minus(c_plus(X1,X2,X0),X2,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_OrderedGroup_Ocompare__rls__11_1) ).
fof(f3367,plain,
! [X2,X0,X1] :
( ~ class_OrderedGroup_Oab__group__add(X0)
| c_minus(c_plus(X1,X2,X0),X2,X0) = X1 ),
inference(reorient_equations,[],[f3366]) ).
fof(f3370,axiom,
! [X2,X3,X0,X1] :
( ~ class_OrderedGroup_Oab__group__add(X0)
| c_plus(X1,c_minus(X2,X3,X0),X0) = c_minus(c_plus(X1,X2,X0),X3,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_OrderedGroup_Ocompare__rls__2_0) ).
fof(f3371,axiom,
! [X2,X3,X0,X1] :
( ~ class_OrderedGroup_Oab__group__add(X0)
| c_plus(c_minus(X1,X2,X0),X3,X0) = c_minus(c_plus(X1,X3,X0),X2,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_OrderedGroup_Ocompare__rls__3_0) ).
fof(f3372,axiom,
! [X2,X3,X0,X1] :
( ~ class_OrderedGroup_Oab__group__add(X0)
| c_minus(c_minus(X1,X2,X0),X3,X0) = c_minus(X1,c_plus(X2,X3,X0),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_OrderedGroup_Ocompare__rls__4_0) ).
fof(f3379,axiom,
! [X2,X3,X0,X1] :
( ~ class_OrderedGroup_Opordered__ab__group__add(X0)
| ~ c_lessequals(c_minus(X1,X2,X0),X3,X0)
| c_lessequals(X1,c_plus(X3,X2,X0),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_OrderedGroup_Ocompare__rls__8_0) ).
fof(f3380,axiom,
! [X2,X3,X0,X1] :
( ~ class_OrderedGroup_Opordered__ab__group__add(X0)
| ~ c_lessequals(X1,c_plus(X2,X3,X0),X0)
| c_lessequals(c_minus(X1,X3,X0),X2,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_OrderedGroup_Ocompare__rls__8_1) ).
fof(f3385,axiom,
! [X2,X0,X1] :
( ~ class_OrderedGroup_Oab__group__add(X0)
| c_minus(X1,X2,X0) = c_plus(X1,c_uminus(X2,X0),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_OrderedGroup_Oab__group__add__class_Odiff__minus_0) ).
fof(f3391,negated_conjecture,
! [X0] : c_lessequals(v_g(X0),v_k(X0),t_b),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_1) ).
fof(f3393,negated_conjecture,
~ c_lessequals(c_minus(v_f(v_x),v_k(v_x),t_b),c_minus(v_f(v_x),v_g(v_x),t_b),t_b),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_3) ).
fof(f3394,negated_conjecture,
class_Ring__and__Field_Oordered__idom(t_b),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',tfree_tcs) ).
fof(f3763,plain,
! [X0,X1] :
( ~ class_Ring__and__Field_Oordered__idom(X1)
| c_minus(X0,c_0,X1) = X0 ),
inference(resolution,[],[f1451,f3032]) ).
fof(f3765,plain,
! [X0,X1] :
( ~ class_Ring__and__Field_Oordered__idom(X1)
| c_0 = c_minus(X0,X0,X1) ),
inference(resolution,[],[f1461,f3032]) ).
fof(f3783,plain,
! [X0,X1] :
( ~ class_Ring__and__Field_Oordered__idom(X1)
| c_uminus(X0,X1) = c_minus(c_0,X0,X1) ),
inference(resolution,[],[f1450,f3032]) ).
fof(f3793,plain,
! [X2,X0,X1] :
( ~ class_Ring__and__Field_Oordered__idom(X2)
| c_plus(c_minus(X0,X1,X2),X1,X2) = X0 ),
inference(resolution,[],[f3365,f3032]) ).
fof(f3795,plain,
! [X2,X0,X1] :
( ~ class_Ring__and__Field_Oordered__idom(X2)
| c_minus(c_plus(X0,X1,X2),X1,X2) = X0 ),
inference(resolution,[],[f3367,f3032]) ).
fof(f3822,plain,
! [X2,X0,X1] :
( ~ class_Ring__and__Field_Oordered__idom(X2)
| c_lessequals(X0,X1,X2)
| ~ c_lessequals(c_minus(X0,X1,X2),c_0,X2) ),
inference(resolution,[],[f1454,f3048]) ).
fof(f3824,plain,
! [X2,X0,X1] :
( ~ class_Ring__and__Field_Oordered__idom(X2)
| c_lessequals(c_minus(X0,X1,X2),c_0,X2)
| ~ c_lessequals(X0,X1,X2) ),
inference(resolution,[],[f1455,f3048]) ).
fof(f3843,plain,
! [X2,X0,X1] :
( ~ class_Ring__and__Field_Oordered__idom(X2)
| c_plus(X0,X1,X2) = c_minus(X0,c_uminus(X1,X2),X2) ),
inference(resolution,[],[f1459,f3032]) ).
fof(f3845,plain,
! [X2,X0,X1] :
( ~ class_Ring__and__Field_Oordered__idom(X2)
| c_minus(X0,X1,X2) = c_uminus(c_minus(X1,X0,X2),X2) ),
inference(resolution,[],[f1476,f3032]) ).
fof(f3854,plain,
! [X2,X0,X1] :
( ~ class_Ring__and__Field_Oordered__idom(X2)
| c_minus(X0,X1,X2) = c_plus(X0,c_uminus(X1,X2),X2) ),
inference(resolution,[],[f3385,f3032]) ).
fof(f3942,plain,
! [X2,X3,X0,X1] :
( ~ class_Ring__and__Field_Oordered__idom(X2)
| c_lessequals(X0,c_plus(X3,X1,X2),X2)
| ~ c_lessequals(c_minus(X0,X1,X2),X3,X2) ),
inference(resolution,[],[f3379,f3048]) ).
fof(f3944,plain,
! [X2,X3,X0,X1] :
( ~ class_Ring__and__Field_Oordered__idom(X3)
| c_lessequals(c_minus(X0,X2,X3),X1,X3)
| ~ c_lessequals(X0,c_plus(X1,X2,X3),X3) ),
inference(resolution,[],[f3380,f3048]) ).
fof(f3965,plain,
! [X2,X3,X0,X1] :
( ~ class_Ring__and__Field_Oordered__idom(X3)
| c_plus(X0,c_minus(X1,X2,X3),X3) = c_minus(c_plus(X0,X1,X3),X2,X3) ),
inference(resolution,[],[f3370,f3032]) ).
fof(f3967,plain,
! [X2,X3,X0,X1] :
( c_plus(c_minus(X0,X1,X2),X3,X2) = c_minus(c_plus(X0,X3,X2),X1,X2)
| ~ class_Ring__and__Field_Oordered__idom(X2) ),
inference(resolution,[],[f3371,f3032]) ).
fof(f3968,plain,
! [X2,X3,X0,X1] :
( ~ class_Ring__and__Field_Oordered__idom(X2)
| c_plus(c_minus(X0,X1,X2),X3,X2) = c_plus(X0,c_minus(X3,X1,X2),X2) ),
inference(forward_subsumption_demodulation,[],[f3967,f3965]) ).
fof(f3971,plain,
! [X2,X3,X0,X1] :
( ~ class_Ring__and__Field_Oordered__idom(X2)
| c_minus(c_minus(X0,X1,X2),X3,X2) = c_minus(X0,c_plus(X1,X3,X2),X2) ),
inference(resolution,[],[f3372,f3032]) ).
fof(f4962,plain,
! [X0] : c_minus(X0,c_0,t_b) = X0,
inference(resolution,[],[f3763,f3394]) ).
fof(f4964,plain,
! [X0] : c_0 = c_minus(X0,X0,t_b),
inference(resolution,[],[f3765,f3394]) ).
fof(f5246,plain,
! [X0] : c_uminus(X0,t_b) = c_minus(c_0,X0,t_b),
inference(resolution,[],[f3783,f3394]) ).
fof(f5403,plain,
! [X0,X1] : c_plus(c_minus(X0,X1,t_b),X1,t_b) = X0,
inference(resolution,[],[f3793,f3394]) ).
fof(f5405,plain,
! [X0,X1] : c_minus(c_plus(X0,X1,t_b),X1,t_b) = X0,
inference(resolution,[],[f3795,f3394]) ).
fof(f5407,plain,
! [X0] : c_plus(X0,c_0,t_b) = X0,
inference(superposition,[],[f5403,f4962]) ).
fof(f5408,plain,
! [X0] : c_plus(c_0,X0,t_b) = X0,
inference(superposition,[],[f5403,f4964]) ).
fof(f6089,plain,
! [X0,X1] :
( ~ c_lessequals(c_minus(X0,X1,t_b),c_0,t_b)
| c_lessequals(X0,X1,t_b) ),
inference(resolution,[],[f3822,f3394]) ).
fof(f6093,plain,
! [X0] :
( ~ c_lessequals(c_uminus(X0,t_b),c_0,t_b)
| c_lessequals(c_0,X0,t_b) ),
inference(superposition,[],[f6089,f5246]) ).
fof(f6103,plain,
! [X0,X1] :
( ~ c_lessequals(X0,X1,t_b)
| c_lessequals(c_minus(X0,X1,t_b),c_0,t_b) ),
inference(resolution,[],[f3824,f3394]) ).
fof(f6108,plain,
! [X0,X1] : c_plus(X0,X1,t_b) = c_minus(X0,c_uminus(X1,t_b),t_b),
inference(resolution,[],[f3843,f3394]) ).
fof(f6111,plain,
! [X0] : c_lessequals(c_minus(v_g(X0),v_k(X0),t_b),c_0,t_b),
inference(resolution,[],[f6103,f3391]) ).
fof(f6115,plain,
! [X0,X1] : c_minus(X0,X1,t_b) = c_uminus(c_minus(X1,X0,t_b),t_b),
inference(resolution,[],[f3845,f3394]) ).
fof(f6120,plain,
! [X0,X1] : c_minus(X0,X1,t_b) = c_plus(X0,c_uminus(X1,t_b),t_b),
inference(resolution,[],[f3854,f3394]) ).
fof(f6255,plain,
! [X0] : c_plus(c_0,X0,t_b) = c_uminus(c_uminus(X0,t_b),t_b),
inference(superposition,[],[f5246,f6108]) ).
fof(f6256,plain,
! [X0] : c_uminus(c_uminus(X0,t_b),t_b) = X0,
inference(forward_demodulation,[],[f6255,f5408]) ).
fof(f6271,plain,
! [X0] :
( ~ c_lessequals(X0,c_0,t_b)
| c_lessequals(c_0,c_uminus(X0,t_b),t_b) ),
inference(superposition,[],[f6093,f6256]) ).
fof(f6301,plain,
! [X0] : c_lessequals(c_0,c_uminus(c_minus(v_g(X0),v_k(X0),t_b),t_b),t_b),
inference(resolution,[],[f6271,f6111]) ).
fof(f6302,plain,
! [X0] : c_lessequals(c_0,c_minus(v_k(X0),v_g(X0),t_b),t_b),
inference(forward_demodulation,[],[f6301,f6115]) ).
fof(f6323,plain,
! [X0,X1] : c_minus(c_uminus(X1,t_b),X0,t_b) = c_uminus(c_plus(X0,X1,t_b),t_b),
inference(superposition,[],[f6115,f6108]) ).
fof(f6325,plain,
! [X0,X1] : c_uminus(X0,t_b) = c_minus(X1,c_plus(X0,X1,t_b),t_b),
inference(superposition,[],[f6115,f5405]) ).
fof(f6479,plain,
! [X0,X1] : c_plus(c_uminus(X0,t_b),c_plus(X0,X1,t_b),t_b) = X1,
inference(superposition,[],[f5403,f6325]) ).
fof(f6491,plain,
! [X0,X1] : c_plus(X0,c_plus(c_uminus(X0,t_b),X1,t_b),t_b) = X1,
inference(superposition,[],[f6479,f6256]) ).
fof(f6788,plain,
! [X2,X0,X1] : c_uminus(c_plus(X2,c_minus(X1,X0,t_b),t_b),t_b) = c_minus(c_minus(X0,X1,t_b),X2,t_b),
inference(superposition,[],[f6323,f6115]) ).
fof(f6804,plain,
! [X0,X1] : c_plus(c_uminus(X1,t_b),X0,t_b) = c_uminus(c_plus(c_uminus(X0,t_b),X1,t_b),t_b),
inference(superposition,[],[f6108,f6323]) ).
fof(f9892,plain,
! [X2,X0,X1] :
( ~ c_lessequals(c_minus(X0,X2,t_b),X1,t_b)
| c_lessequals(X0,c_plus(X1,X2,t_b),t_b) ),
inference(resolution,[],[f3942,f3394]) ).
fof(f9925,plain,
! [X2,X0,X1] :
( c_lessequals(c_minus(X0,X1,t_b),X2,t_b)
| ~ c_lessequals(X0,c_plus(X2,X1,t_b),t_b) ),
inference(resolution,[],[f3944,f3394]) ).
fof(f9966,plain,
! [X2,X0,X1] :
( ~ c_lessequals(X0,X2,t_b)
| c_lessequals(c_plus(X0,X1,t_b),c_plus(X2,X1,t_b),t_b) ),
inference(superposition,[],[f9892,f5405]) ).
fof(f9967,plain,
! [X0,X1] :
( ~ c_lessequals(c_uminus(X0,t_b),X1,t_b)
| c_lessequals(c_0,c_plus(X1,X0,t_b),t_b) ),
inference(superposition,[],[f9892,f5246]) ).
fof(f10008,plain,
! [X0,X1] :
( ~ c_lessequals(X0,X1,t_b)
| c_lessequals(c_0,c_plus(X1,c_uminus(X0,t_b),t_b),t_b) ),
inference(superposition,[],[f9967,f6256]) ).
fof(f10009,plain,
! [X0,X1] :
( c_lessequals(c_0,c_minus(X1,X0,t_b),t_b)
| ~ c_lessequals(X0,X1,t_b) ),
inference(forward_demodulation,[],[f10008,f6120]) ).
fof(f10252,plain,
! [X0,X1] :
( ~ c_lessequals(c_0,c_plus(X1,X0,t_b),t_b)
| c_lessequals(c_uminus(X0,t_b),X1,t_b) ),
inference(superposition,[],[f9925,f5246]) ).
fof(f10355,plain,
! [X0,X1] :
( ~ c_lessequals(c_0,X0,t_b)
| c_lessequals(c_uminus(c_plus(c_uminus(X1,t_b),X0,t_b),t_b),X1,t_b) ),
inference(superposition,[],[f10252,f6491]) ).
fof(f10385,plain,
! [X0,X1] :
( ~ c_lessequals(c_0,X0,t_b)
| c_lessequals(c_plus(c_uminus(X0,t_b),X1,t_b),X1,t_b) ),
inference(forward_demodulation,[],[f10355,f6804]) ).
fof(f10564,plain,
! [X2,X0,X1] : c_plus(X0,c_minus(X2,X1,t_b),t_b) = c_plus(c_minus(X0,X1,t_b),X2,t_b),
inference(resolution,[],[f3968,f3394]) ).
fof(f10605,plain,
! [X2,X0,X1] : c_minus(c_minus(X0,X1,t_b),X2,t_b) = c_minus(X0,c_plus(X1,X2,t_b),t_b),
inference(resolution,[],[f3971,f3394]) ).
fof(f10810,plain,
! [X0,X1] : c_lessequals(c_plus(c_0,X0,t_b),c_plus(c_minus(v_k(X1),v_g(X1),t_b),X0,t_b),t_b),
inference(resolution,[],[f9966,f6302]) ).
fof(f10811,plain,
! [X2,X0,X1] :
( c_lessequals(c_plus(c_0,X0,t_b),c_plus(c_minus(X1,X2,t_b),X0,t_b),t_b)
| ~ c_lessequals(X2,X1,t_b) ),
inference(resolution,[],[f9966,f10009]) ).
fof(f10831,plain,
! [X2,X0,X1] :
( c_lessequals(c_plus(c_0,X0,t_b),c_plus(X1,c_minus(X0,X2,t_b),t_b),t_b)
| ~ c_lessequals(X2,X1,t_b) ),
inference(forward_demodulation,[],[f10811,f10564]) ).
fof(f10832,plain,
! [X0,X1] : c_lessequals(c_plus(c_0,X0,t_b),c_plus(v_k(X1),c_minus(X0,v_g(X1),t_b),t_b),t_b),
inference(forward_demodulation,[],[f10810,f10564]) ).
fof(f10850,plain,
! [X2,X0,X1] :
( c_lessequals(X0,c_plus(X1,c_minus(X0,X2,t_b),t_b),t_b)
| ~ c_lessequals(X2,X1,t_b) ),
inference(forward_demodulation,[],[f10831,f5408]) ).
fof(f10851,plain,
! [X0,X1] : c_lessequals(X0,c_plus(v_k(X1),c_minus(X0,v_g(X1),t_b),t_b),t_b),
inference(forward_demodulation,[],[f10832,f5408]) ).
fof(f11054,plain,
! [X0,X1] : c_lessequals(c_plus(c_uminus(c_plus(v_k(X0),c_minus(c_0,v_g(X0),t_b),t_b),t_b),X1,t_b),X1,t_b),
inference(resolution,[],[f10851,f10385]) ).
fof(f11072,plain,
! [X0,X1] : c_lessequals(c_plus(c_minus(c_minus(v_g(X0),c_0,t_b),v_k(X0),t_b),X1,t_b),X1,t_b),
inference(forward_demodulation,[],[f11054,f6788]) ).
fof(f11080,plain,
! [X0,X1] : c_lessequals(c_plus(c_minus(v_g(X0),c_0,t_b),c_minus(X1,v_k(X0),t_b),t_b),X1,t_b),
inference(forward_demodulation,[],[f11072,f10564]) ).
fof(f11087,plain,
! [X0,X1] : c_lessequals(c_plus(v_g(X0),c_minus(c_minus(X1,v_k(X0),t_b),c_0,t_b),t_b),X1,t_b),
inference(forward_demodulation,[],[f11080,f10564]) ).
fof(f11091,plain,
! [X0,X1] : c_lessequals(c_plus(v_g(X0),c_minus(X1,c_plus(v_k(X0),c_0,t_b),t_b),t_b),X1,t_b),
inference(forward_demodulation,[],[f11087,f10605]) ).
fof(f11094,plain,
! [X0,X1] : c_lessequals(c_plus(v_g(X0),c_minus(X1,v_k(X0),t_b),t_b),X1,t_b),
inference(forward_demodulation,[],[f11091,f5407]) ).
fof(f12369,plain,
! [X2,X0,X1] :
( c_lessequals(X1,c_plus(X2,c_uminus(X0,t_b),t_b),t_b)
| ~ c_lessequals(c_plus(X0,X1,t_b),X2,t_b) ),
inference(superposition,[],[f10850,f6325]) ).
fof(f12391,plain,
! [X2,X0,X1] :
( ~ c_lessequals(c_plus(X0,X1,t_b),X2,t_b)
| c_lessequals(X1,c_minus(X2,X0,t_b),t_b) ),
inference(forward_demodulation,[],[f12369,f6120]) ).
fof(f15412,plain,
! [X0,X1] : c_lessequals(c_minus(X0,v_k(X1),t_b),c_minus(X0,v_g(X1),t_b),t_b),
inference(resolution,[],[f12391,f11094]) ).
fof(f15912,plain,
$false,
inference(resolution,[],[f15412,f3393]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ANA028-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.09/0.18 % Computer : n005.cluster.edu
% 0.09/0.18 % Model : x86_64 x86_64
% 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.18 % Memory : 8046.5625MB
% 0.09/0.18 % OS : Linux 6.8.0-71-generic
% 0.09/0.18 % CPULimit : 300
% 0.09/0.18 % WCLimit : 300
% 0.09/0.18 % DateTime : Mon Sep 28 20:30:47 UTC 2026
% 0.09/0.18 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.21 Running first-order model finding
% 0.09/0.21 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
% 8.89/1.77 % (1121246)Will run a generic schedule for satisfiability detection.
% 8.89/1.77 % (1121253)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=847681921:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 8.89/1.77 % (1121252)% WARNING: option uhcvi not known.
% 8.89/1.77 % (1121251)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2750840487_2999 on theBenchmark for (2999ds/0Mi)
% 8.89/1.77 % (1121252)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1657218692:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 8.89/1.77 % (1121254)dis+10_1_sil=32000:sp=arity:random_seed=2400351242:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 8.89/1.77 % (1121255)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2178057775:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 8.89/1.77 % (1121256)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2511082500:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 8.89/1.77 % (1121257)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=299643127:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 8.89/1.77 % (1121254)Instruction limit reached!
% 8.89/1.77 % (1121254)------------------------------
% 8.89/1.77 % (1121254)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.89/1.77 % (1121254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.89/1.77 % (1121254)CaDiCaL version: 2.1.3
% 8.89/1.77 % (1121254)Termination reason: Instruction limit
% 8.89/1.77 % (1121254)Termination phase: Saturation
% 8.89/1.77 % (1121254)Time elapsed: 0.057 s
% 8.89/1.77 % (1121254)Peak memory usage: 15 MB
% 8.89/1.77 % (1121254)Instructions burned: 103 (million)
% 8.89/1.77 % (1121255)Instruction limit reached!
% 8.89/1.77 % (1121255)------------------------------
% 8.89/1.77 % (1121255)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.89/1.77 % (1121255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.89/1.77 % (1121255)CaDiCaL version: 2.1.3
% 8.89/1.77 % (1121255)Termination reason: Instruction limit
% 8.89/1.77 % (1121255)Termination phase: Saturation
% 8.89/1.77 % (1121255)Time elapsed: 0.062 s
% 8.89/1.77 % (1121255)Peak memory usage: 15 MB
% 8.89/1.77 % (1121255)Instructions burned: 116 (million)
% 8.89/1.77 % (1121256)Instruction limit reached!
% 8.89/1.77 % (1121256)------------------------------
% 8.89/1.77 % (1121256)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.89/1.77 % (1121256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.89/1.77 % (1121256)CaDiCaL version: 2.1.3
% 8.89/1.77 % (1121256)Termination reason: Instruction limit
% 8.89/1.77 % (1121256)Termination phase: Saturation
% 8.89/1.77 % (1121256)Time elapsed: 0.074 s
% 8.89/1.77 % (1121256)Peak memory usage: 16 MB
% 8.89/1.77 % (1121256)Instructions burned: 132 (million)
% 8.89/1.77 % (1121265)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3864460597:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 8.89/1.77 % (1121266)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=165658659:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 8.89/1.77 % (1121267)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=3169312106:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 8.89/1.77 % (1121257)Instruction limit reached!
% 8.89/1.77 % (1121257)------------------------------
% 8.89/1.77 % (1121257)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.89/1.77 % (1121257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.89/1.77 % (1121257)CaDiCaL version: 2.1.3
% 8.89/1.77 % (1121257)Termination reason: Instruction limit
% 8.89/1.77 % (1121257)Termination phase: Saturation
% 8.89/1.77 % (1121257)Time elapsed: 0.102 s
% 8.89/1.77 % (1121257)Peak memory usage: 16 MB
% 8.89/1.77 % (1121257)Instructions burned: 160 (million)
% 8.89/1.77 % (1121271)ott-21_1_sil=16000:fs=off:random_seed=1016505757:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 8.89/1.77 % (1121266)Instruction limit reached!
% 8.89/1.77 % (1121266)------------------------------
% 8.89/1.77 % (1121266)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.89/1.77 % (1121266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.89/1.77 % (1121266)CaDiCaL version: 2.1.3
% 42.73/6.30 % (1121266)Termination reason: Instruction limit
% 42.73/6.30 % (1121266)Termination phase: Saturation
% 42.73/6.30 % (1121266)Time elapsed: 0.074 s
% 42.73/6.30 % (1121266)Peak memory usage: 16 MB
% 42.73/6.30 % (1121266)Instructions burned: 132 (million)
% 42.73/6.30 % (1121273)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3814326279:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 42.73/6.30 % (1121271)Instruction limit reached!
% 42.73/6.30 % (1121271)------------------------------
% 42.73/6.30 % (1121271)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.73/6.30 % (1121271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.73/6.30 % (1121271)CaDiCaL version: 2.1.3
% 42.73/6.30 % (1121271)Termination reason: Instruction limit
% 42.73/6.30 % (1121271)Termination phase: Saturation
% 42.73/6.30 % (1121271)Time elapsed: 0.098 s
% 42.73/6.30 % (1121271)Peak memory usage: 16 MB
% 42.73/6.30 % (1121271)Instructions burned: 180 (million)
% 42.73/6.30 % (1121275)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=4170747674:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 42.73/6.30 % TRYING [1]
% 42.73/6.30 % TRYING [2]
% 42.73/6.30 % TRYING [1]
% 42.73/6.30 % TRYING [2]
% 42.73/6.30 % (1121265)Instruction limit reached!
% 42.73/6.30 % (1121265)------------------------------
% 42.73/6.30 % (1121265)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.73/6.30 % (1121265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.73/6.30 % (1121265)CaDiCaL version: 2.1.3
% 42.73/6.30 % (1121265)Termination reason: Instruction limit
% 42.73/6.30 % (1121265)Termination phase: Finite model building constraint generation
% 42.73/6.30 % (1121265)Time elapsed: 0.335 s
% 42.73/6.30 % (1121265)Peak memory usage: 26 MB
% 42.73/6.30 % (1121265)Instructions burned: 717 (million)
% 42.73/6.30 % (1121277)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3385358792:i=1179_2994 on theBenchmark for (2994ds/1179Mi)
% 42.73/6.30 % (1121267)Instruction limit reached!
% 42.73/6.30 % (1121267)------------------------------
% 42.73/6.30 % (1121267)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.73/6.30 % (1121267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.73/6.30 % (1121267)CaDiCaL version: 2.1.3
% 42.73/6.30 % (1121267)Termination reason: Instruction limit
% 42.73/6.30 % (1121267)Termination phase: Saturation
% 42.73/6.30 % (1121267)Time elapsed: 0.370 s
% 42.73/6.30 % (1121267)Peak memory usage: 21 MB
% 42.73/6.30 % (1121267)Instructions burned: 685 (million)
% 42.73/6.30 % (1121273)Instruction limit reached!
% 42.73/6.30 % (1121273)------------------------------
% 42.73/6.30 % (1121273)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.73/6.30 % (1121273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.73/6.30 % (1121273)CaDiCaL version: 2.1.3
% 42.73/6.30 % (1121273)Termination reason: Instruction limit
% 42.73/6.30 % (1121273)Termination phase: Saturation
% 42.73/6.30 % (1121273)Time elapsed: 0.299 s
% 42.73/6.30 % (1121273)Peak memory usage: 17 MB
% 42.73/6.30 % (1121273)Instructions burned: 477 (million)
% 42.73/6.30 % (1121279)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3167625262:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 42.73/6.30 % (1121280)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=469609870: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)
% 42.73/6.30 % TRYING [1]
% 42.73/6.30 % (1121275)Instruction limit reached!
% 42.73/6.30 % (1121275)------------------------------
% 42.73/6.30 % (1121275)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.73/6.30 % (1121275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.73/6.30 % (1121275)CaDiCaL version: 2.1.3
% 42.73/6.30 % (1121275)Termination reason: Instruction limit
% 42.73/6.30 % (1121275)Termination phase: Finite model building constraint generation
% 42.73/6.30 % (1121275)Time elapsed: 0.423 s
% 42.73/6.30 % (1121275)Peak memory usage: 49 MB
% 42.73/6.30 % (1121275)Instructions burned: 865 (million)
% 42.73/6.30 % (1121283)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2212677556:i=879:kws=inv_precedence:fsr=off_2992 on theBenchmark for (2992ds/879Mi)
% 42.73/6.30 % (1121279)Cannot represent all propositional literals internally
% 42.73/6.30 % (1121279)Refutation not found, incomplete strategy
% 42.73/6.30 % (1121279)------------------------------
% 42.73/6.30 % (1121279)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.75/7.97 % (1121279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.75/7.97 % (1121279)CaDiCaL version: 2.1.3
% 17.75/7.97 % (1121279)Termination reason: Refutation not found, incomplete strategy
% 17.75/7.97 % (1121279)Time elapsed: 0.284 s
% 17.75/7.97 % (1121279)Peak memory usage: 23 MB
% 17.75/7.97 % (1121279)Instructions burned: 577 (million)
% 17.75/7.97 % (1121279)------------------------------
% 17.75/7.97 % (1121279)------------------------------
% 17.75/7.97 % (1121285)fmb+10_1_sil=64000:random_seed=3922870778:i=22061:nm=2:gsp=on_2991 on theBenchmark for (2991ds/22061Mi)
% 17.75/7.97 % (1121280)Instruction limit reached!
% 17.75/7.97 % (1121280)------------------------------
% 17.75/7.97 % (1121280)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.75/7.97 % (1121280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.75/7.97 % (1121280)CaDiCaL version: 2.1.3
% 17.75/7.97 % (1121280)Termination reason: Instruction limit
% 17.75/7.97 % (1121280)Termination phase: Saturation
% 17.75/7.97 % (1121280)Time elapsed: 0.370 s
% 17.75/7.97 % (1121280)Peak memory usage: 20 MB
% 17.75/7.97 % (1121280)Instructions burned: 692 (million)
% 17.75/7.97 % (1121287)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2057551124:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 17.75/7.97 % TRYING [1]
% 17.75/7.97 % (1121283)Instruction limit reached!
% 17.75/7.97 % (1121283)------------------------------
% 17.75/7.97 % (1121283)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.75/7.97 % (1121283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.75/7.97 % (1121283)CaDiCaL version: 2.1.3
% 17.75/7.97 % (1121283)Termination reason: Instruction limit
% 17.75/7.97 % (1121283)Termination phase: Saturation
% 17.75/7.97 % (1121283)Time elapsed: 0.436 s
% 17.75/7.97 % (1121283)Peak memory usage: 21 MB
% 17.75/7.97 % (1121283)Instructions burned: 880 (million)
% 17.75/7.97 % (1121290)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3166863437:fmbsr=1.7:i=920_2987 on theBenchmark for (2987ds/920Mi)
% 17.75/7.97 % (1121287)Cannot represent all propositional literals internally
% 17.75/7.97 % (1121287)Refutation not found, incomplete strategy
% 17.75/7.97 % (1121287)------------------------------
% 17.75/7.97 % (1121287)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.75/7.97 % (1121287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.75/7.97 % (1121287)CaDiCaL version: 2.1.3
% 17.75/7.97 % (1121287)Termination reason: Refutation not found, incomplete strategy
% 17.75/7.97 % (1121287)Time elapsed: 0.283 s
% 17.75/7.97 % (1121287)Peak memory usage: 23 MB
% 17.75/7.97 % (1121287)Instructions burned: 574 (million)
% 17.75/7.97 % (1121287)------------------------------
% 17.75/7.97 % (1121287)------------------------------
% 17.75/7.97 % (1121277)Instruction limit reached!
% 17.75/7.97 % (1121277)------------------------------
% 17.75/7.97 % (1121277)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.75/7.97 % (1121277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.75/7.97 % (1121277)CaDiCaL version: 2.1.3
% 17.75/7.97 % (1121277)Termination reason: Instruction limit
% 17.75/7.97 % (1121277)Termination phase: Saturation
% 17.75/7.97 % (1121277)Time elapsed: 0.752 s
% 17.75/7.97 % (1121277)Peak memory usage: 26 MB
% 17.75/7.97 % (1121277)Instructions burned: 1180 (million)
% 17.75/7.97 % (1121292)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=967414743:i=5131_2987 on theBenchmark for (2987ds/5131Mi)
% 17.75/7.97 % (1121293)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1016355370:i=1472:ins=7:fdi=8:gsp=on_2987 on theBenchmark for (2987ds/1472Mi)
% 17.75/7.97 % (1121290)Cannot represent all propositional literals internally
% 17.75/7.97 % (1121290)Refutation not found, incomplete strategy
% 17.75/7.97 % (1121290)------------------------------
% 17.75/7.97 % (1121290)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.75/7.97 % (1121290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.75/7.97 % (1121290)CaDiCaL version: 2.1.3
% 17.75/7.97 % (1121290)Termination reason: Refutation not found, incomplete strategy
% 17.75/7.97 % (1121290)Time elapsed: 0.284 s
% 17.75/7.97 % (1121290)Peak memory usage: 23 MB
% 17.75/7.97 % (1121290)Instructions burned: 574 (million)
% 17.75/7.97 % (1121290)------------------------------
% 17.75/7.97 % (1121290)------------------------------
% 17.75/7.97 % (1121296)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2903215805:i=6324_2984 on theBenchmark for (2984ds/6324Mi)
% 17.75/7.97 % TRYING [2]
% 17.75/7.97 % (1121296)Cannot represent all propositional literals internally
% 17.75/7.97 % (1121296)Refutation not found, incomplete strategy
% 17.75/7.97 % (1121296)------------------------------
% 17.75/7.97 % (1121296)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.75/7.97 % (1121296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.75/7.97 % (1121296)CaDiCaL version: 2.1.3
% 17.75/7.97 % (1121296)Termination reason: Refutation not found, incomplete strategy
% 17.75/7.97 % (1121296)Time elapsed: 0.294 s
% 17.75/7.97 % (1121296)Peak memory usage: 23 MB
% 17.75/7.97 % (1121296)Instructions burned: 595 (million)
% 17.75/7.97 % (1121296)------------------------------
% 17.75/7.97 % (1121296)------------------------------
% 17.75/7.97 % (1121298)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1885210043:fmbsr=2.30978:i=2174_2981 on theBenchmark for (2981ds/2174Mi)
% 17.75/7.97 % (1121293)Instruction limit reached!
% 17.75/7.97 % (1121293)------------------------------
% 17.75/7.97 % (1121293)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.75/7.97 % (1121293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.75/7.97 % (1121293)CaDiCaL version: 2.1.3
% 17.75/7.97 % (1121293)Termination reason: Instruction limit
% 17.75/7.97 % (1121293)Termination phase: Saturation
% 17.75/7.97 % (1121293)Time elapsed: 0.775 s
% 17.75/7.97 % (1121293)Peak memory usage: 32 MB
% 17.75/7.97 % (1121293)Instructions burned: 1472 (million)
% 17.75/7.97 % (1121300)ott-2_1_sil=16000:newcnf=on:random_seed=206481473:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2979 on theBenchmark for (2979ds/869Mi)
% 17.75/7.97 % (1121300)Instruction limit reached!
% 17.75/7.97 % (1121300)------------------------------
% 17.75/7.97 % (1121300)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.75/7.97 % (1121300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.75/7.97 % (1121300)CaDiCaL version: 2.1.3
% 17.75/7.97 % (1121300)Termination reason: Instruction limit
% 17.75/7.97 % (1121300)Termination phase: Saturation
% 17.75/7.97 % (1121300)Time elapsed: 0.530 s
% 17.75/7.97 % (1121300)Peak memory usage: 22 MB
% 17.75/7.97 % (1121300)Instructions burned: 869 (million)
% 17.75/7.97 % (1121302)ott+10_1_sil=32000:tgt=ground:random_seed=333405985:i=5114:av=off_2973 on theBenchmark for (2973ds/5114Mi)
% 17.75/7.97 % (1121298)Instruction limit reached!
% 17.75/7.97 % (1121298)------------------------------
% 17.75/7.97 % (1121298)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.75/7.97 % (1121298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.75/7.97 % (1121298)CaDiCaL version: 2.1.3
% 17.75/7.97 % (1121298)Termination reason: Instruction limit
% 17.75/7.97 % (1121298)Termination phase: Finite model building preprocessing
% 17.75/7.97 % (1121298)Time elapsed: 1.092 s
% 17.75/7.97 % (1121298)Peak memory usage: 42 MB
% 17.75/7.97 % (1121298)Instructions burned: 2174 (million)
% 17.75/7.97 % (1121304)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3627352812:i=54282_2970 on theBenchmark for (2970ds/54282Mi)
% 17.75/7.97 % TRYING [1]
% 17.75/7.97 % TRYING [2]
% 17.75/7.97 % (1121292)Instruction limit reached!
% 17.75/7.97 % (1121292)------------------------------
% 17.75/7.97 % (1121292)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.75/7.97 % (1121292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.75/7.97 % (1121292)CaDiCaL version: 2.1.3
% 17.75/7.97 % (1121292)Termination reason: Instruction limit
% 17.75/7.97 % (1121292)Termination phase: Saturation
% 17.75/7.97 % (1121292)Time elapsed: 3.252 s
% 17.75/7.97 % (1121292)Peak memory usage: 53 MB
% 17.75/7.97 % (1121292)Instructions burned: 5131 (million)
% 17.75/7.97 % (1121306)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3012525128:i=3512:aac=none_2954 on theBenchmark for (2954ds/3512Mi)
% 17.75/7.97 % (1121302)Instruction limit reached!
% 17.75/7.97 % (1121302)------------------------------
% 17.75/7.97 % (1121302)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.75/7.97 % (1121302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.75/7.97 % (1121302)CaDiCaL version: 2.1.3
% 17.75/7.97 % (1121302)Termination reason: Instruction limit
% 17.75/7.97 % (1121302)Termination phase: Saturation
% 17.75/7.97 % (1121302)Time elapsed: 3.422 s
% 17.75/7.97 % (1121302)Peak memory usage: 53 MB
% 17.75/7.97 % (1121302)Instructions burned: 5117 (million)
% 17.75/7.97 % (1121308)dis+21_1_sil=32000:sas=cadical:random_seed=2842796069:i=3773:amm=off_2939 on theBenchmark for (2939ds/3773Mi)
% 17.75/7.97 % (1121306)Instruction limit reached!
% 17.75/7.97 % (1121306)------------------------------
% 17.75/7.97 % (1121306)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.75/7.97 % (1121306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.75/7.97 % (1121306)CaDiCaL version: 2.1.3
% 17.75/7.97 % (1121306)Termination reason: Instruction limit
% 17.75/7.97 % (1121306)Termination phase: Saturation
% 17.75/7.97 % (1121306)Time elapsed: 2.161 s
% 17.75/7.97 % (1121306)Peak memory usage: 42 MB
% 17.75/7.97 % (1121306)Instructions burned: 3512 (million)
% 17.75/7.97 % (1121310)ott+11_1_sil=16000:gs=on:random_seed=3078480161:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2932 on theBenchmark for (2932ds/2251Mi)
% 17.75/7.97 % (1121310) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1121246-1121310"...
% 17.75/7.97 % (1121310)...printing done.
% 17.75/7.97 % (1121310)Refutation found. Thanks to Tanya!
% 17.75/7.97 % SZS status Unsatisfiable for theBenchmark
% 17.75/7.97 % SZS output start Proof for theBenchmark
% See solution above
% 17.75/7.98 % (1121310)------------------------------
% 17.75/7.98 % (1121310)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.75/7.98 % (1121310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.75/7.98 % (1121310)CaDiCaL version: 2.1.3
% 17.75/7.98 % (1121310)Termination reason: Refutation
% 17.75/7.98 % (1121310)Time elapsed: 0.831 s
% 17.75/7.98 % (1121310)Peak memory usage: 31 MB
% 17.75/7.98 % (1121310)Instructions burned: 1332 (million)
% 17.75/7.98 % (1121246)Success in time 7.753 s
% 17.75/7.98 % Vampire exiting
%------------------------------------------------------------------------------