%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV032+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n007.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:07:57 PM UTC 2026
% Result : Theorem 6.30s 2.02s
% Output : Refutation 8.56s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 24
% Syntax : Number of formulae : 164 ( 34 unt; 17 def)
% Number of atoms : 726 ( 185 equ)
% Maximal formula atoms : 32 ( 4 avg)
% Number of connectives : 949 ( 387 ~; 400 |; 130 &)
% ( 16 <=>; 16 =>; 0 <=; 0 <~>)
% Maximal formula depth : 21 ( 5 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 21 ( 19 usr; 18 prp; 0-2 aty)
% Number of functors : 20 ( 20 usr; 15 con; 0-3 aty)
% Number of variables : 89 ( 0 sgn 75 !; 14 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
! [X0] : leq(X0,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',reflexivity_leq) ).
fof(f8,axiom,
! [X0,X1] :
( gt(X1,X0)
=> leq(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',leq_gt1) ).
fof(f17,axiom,
! [X0,X1,X2,X3,X4,X5,X6] :
( ( leq(X1,X0)
& leq(X0,X2)
& leq(X4,X3)
& leq(X3,X5) )
=> a_select3(tptp_const_array2(dim(X1,X2),dim(X4,X5),X6),X0,X3) = X6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',const_array2_select) ).
fof(f53,conjecture,
( ( init = init
& leq(n0,pv19)
& leq(n0,pv20)
& leq(n0,pv1376)
& leq(pv19,minus(n410,n1))
& leq(pv20,minus(n330,n1))
& leq(pv1376,n3)
& ! [X0] :
( ( leq(n0,X0)
& leq(X0,n2) )
=> ! [X1] :
( ( leq(n0,X1)
& leq(X1,n3) )
=> a_select3(simplex7_init,X1,X0) = init ) )
& ! [X2] :
( ( leq(n0,X2)
& leq(X2,minus(pv1376,n1)) )
=> a_select2(s_values7_init,X2) = init ) )
=> ( init = init
& a_select3(simplex7_init,pv1376,n0) = init
& a_select3(simplex7_init,pv1376,n1) = init
& a_select3(simplex7_init,pv1376,n2) = init
& a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) = init
& leq(n0,pv19)
& leq(n0,pv1376)
& leq(pv19,minus(n410,n1))
& leq(pv1376,n3)
& ! [X3] :
( ( leq(n0,X3)
& leq(X3,n2) )
=> ! [X4] :
( ( leq(n0,X4)
& leq(X4,n3) )
=> a_select3(simplex7_init,X4,X3) = init ) )
& ! [X5] :
( ( leq(n0,X5)
& leq(X5,minus(pv1376,n1)) )
=> a_select2(s_values7_init,X5) = init ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gauss_init_0041) ).
fof(f54,negated_conjecture,
~ ( ( init = init
& leq(n0,pv19)
& leq(n0,pv20)
& leq(n0,pv1376)
& leq(pv19,minus(n410,n1))
& leq(pv20,minus(n330,n1))
& leq(pv1376,n3)
& ! [X0] :
( ( leq(n0,X0)
& leq(X0,n2) )
=> ! [X1] :
( ( leq(n0,X1)
& leq(X1,n3) )
=> a_select3(simplex7_init,X1,X0) = init ) )
& ! [X2] :
( ( leq(n0,X2)
& leq(X2,minus(pv1376,n1)) )
=> a_select2(s_values7_init,X2) = init ) )
=> ( init = init
& a_select3(simplex7_init,pv1376,n0) = init
& a_select3(simplex7_init,pv1376,n1) = init
& a_select3(simplex7_init,pv1376,n2) = init
& a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) = init
& leq(n0,pv19)
& leq(n0,pv1376)
& leq(pv19,minus(n410,n1))
& leq(pv1376,n3)
& ! [X3] :
( ( leq(n0,X3)
& leq(X3,n2) )
=> ! [X4] :
( ( leq(n0,X4)
& leq(X4,n3) )
=> a_select3(simplex7_init,X4,X3) = init ) )
& ! [X5] :
( ( leq(n0,X5)
& leq(X5,minus(pv1376,n1)) )
=> a_select2(s_values7_init,X5) = init ) ) ),
inference(negated_conjecture,[status(cth)],[f53]) ).
fof(f73,axiom,
gt(n1,n0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_1_0) ).
fof(f74,axiom,
gt(n2,n0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_2_0) ).
fof(f80,axiom,
gt(n2,n1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_2_1) ).
fof(f110,plain,
( ( init != init
| init != a_select3(simplex7_init,pv1376,n0)
| init != a_select3(simplex7_init,pv1376,n1)
| init != a_select3(simplex7_init,pv1376,n2)
| init != a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20)
| ~ leq(n0,pv19)
| ~ leq(n0,pv1376)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv1376,n3)
| ? [X3] :
( ? [X4] :
( init != a_select3(simplex7_init,X4,X3)
& leq(n0,X4)
& leq(X4,n3) )
& leq(n0,X3)
& leq(X3,n2) )
| ? [X5] :
( init != a_select2(s_values7_init,X5)
& leq(n0,X5)
& leq(X5,minus(pv1376,n1)) ) )
& init = init
& leq(n0,pv19)
& leq(n0,pv20)
& leq(n0,pv1376)
& leq(pv19,minus(n410,n1))
& leq(pv20,minus(n330,n1))
& leq(pv1376,n3)
& ! [X0] :
( ! [X1] :
( a_select3(simplex7_init,X1,X0) = init
| ~ leq(n0,X1)
| ~ leq(X1,n3) )
| ~ leq(n0,X0)
| ~ leq(X0,n2) )
& ! [X2] :
( a_select2(s_values7_init,X2) = init
| ~ leq(n0,X2)
| ~ leq(X2,minus(pv1376,n1)) ) ),
inference(ennf_transformation,[],[f54]) ).
fof(f111,plain,
( ( init != init
| init != a_select3(simplex7_init,pv1376,n0)
| init != a_select3(simplex7_init,pv1376,n1)
| init != a_select3(simplex7_init,pv1376,n2)
| init != a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20)
| ~ leq(n0,pv19)
| ~ leq(n0,pv1376)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv1376,n3)
| ? [X3] :
( ? [X4] :
( init != a_select3(simplex7_init,X4,X3)
& leq(n0,X4)
& leq(X4,n3) )
& leq(n0,X3)
& leq(X3,n2) )
| ? [X5] :
( init != a_select2(s_values7_init,X5)
& leq(n0,X5)
& leq(X5,minus(pv1376,n1)) ) )
& init = init
& leq(n0,pv19)
& leq(n0,pv20)
& leq(n0,pv1376)
& leq(pv19,minus(n410,n1))
& leq(pv20,minus(n330,n1))
& leq(pv1376,n3)
& ! [X0] :
( ! [X1] :
( a_select3(simplex7_init,X1,X0) = init
| ~ leq(n0,X1)
| ~ leq(X1,n3) )
| ~ leq(n0,X0)
| ~ leq(X0,n2) )
& ! [X2] :
( a_select2(s_values7_init,X2) = init
| ~ leq(n0,X2)
| ~ leq(X2,minus(pv1376,n1)) ) ),
inference(flattening,[],[f110]) ).
fof(f146,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( a_select3(tptp_const_array2(dim(X1,X2),dim(X4,X5),X6),X0,X3) = X6
| ~ leq(X1,X0)
| ~ leq(X0,X2)
| ~ leq(X4,X3)
| ~ leq(X3,X5) ),
inference(ennf_transformation,[],[f17]) ).
fof(f147,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( a_select3(tptp_const_array2(dim(X1,X2),dim(X4,X5),X6),X0,X3) = X6
| ~ leq(X1,X0)
| ~ leq(X0,X2)
| ~ leq(X4,X3)
| ~ leq(X3,X5) ),
inference(flattening,[],[f146]) ).
fof(f155,plain,
! [X0,X1] :
( leq(X0,X1)
| ~ gt(X1,X0) ),
inference(ennf_transformation,[],[f8]) ).
fof(f162,definition,
( ? [X3] :
( ? [X4] :
( init != a_select3(simplex7_init,X4,X3)
& leq(n0,X4)
& leq(X4,n3) )
& leq(n0,X3)
& leq(X3,n2) )
| ~ sP0 ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f163,plain,
( ( init != init
| init != a_select3(simplex7_init,pv1376,n0)
| init != a_select3(simplex7_init,pv1376,n1)
| init != a_select3(simplex7_init,pv1376,n2)
| init != a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20)
| ~ leq(n0,pv19)
| ~ leq(n0,pv1376)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv1376,n3)
| sP0
| ? [X5] :
( init != a_select2(s_values7_init,X5)
& leq(n0,X5)
& leq(X5,minus(pv1376,n1)) ) )
& init = init
& leq(n0,pv19)
& leq(n0,pv20)
& leq(n0,pv1376)
& leq(pv19,minus(n410,n1))
& leq(pv20,minus(n330,n1))
& leq(pv1376,n3)
& ! [X0] :
( ! [X1] :
( a_select3(simplex7_init,X1,X0) = init
| ~ leq(n0,X1)
| ~ leq(X1,n3) )
| ~ leq(n0,X0)
| ~ leq(X0,n2) )
& ! [X2] :
( a_select2(s_values7_init,X2) = init
| ~ leq(n0,X2)
| ~ leq(X2,minus(pv1376,n1)) ) ),
inference(definition_folding,[],[f111,f162]) ).
fof(f171,plain,
( ? [X3] :
( ? [X4] :
( init != a_select3(simplex7_init,X4,X3)
& leq(n0,X4)
& leq(X4,n3) )
& leq(n0,X3)
& leq(X3,n2) )
| ~ sP0 ),
inference(nnf_transformation,[],[f162]) ).
fof(f172,plain,
( ? [X0] :
( ? [X1] :
( init != a_select3(simplex7_init,X1,X0)
& leq(n0,X1)
& leq(X1,n3) )
& leq(n0,X0)
& leq(X0,n2) )
| ~ sP0 ),
inference(rectify,[],[f171]) ).
fof(f173,plain,
( ( init != a_select3(simplex7_init,sK6,sK5)
& leq(n0,sK6)
& leq(sK6,n3)
& leq(n0,sK5)
& leq(sK5,n2) )
| ~ sP0 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5,sK6]),skolemize(X0,sK5),skolemize(X1,sK6)],[f172]) ).
fof(f174,plain,
( ( init != init
| init != a_select3(simplex7_init,pv1376,n0)
| init != a_select3(simplex7_init,pv1376,n1)
| init != a_select3(simplex7_init,pv1376,n2)
| init != a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20)
| ~ leq(n0,pv19)
| ~ leq(n0,pv1376)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv1376,n3)
| sP0
| ? [X0] :
( init != a_select2(s_values7_init,X0)
& leq(n0,X0)
& leq(X0,minus(pv1376,n1)) ) )
& init = init
& leq(n0,pv19)
& leq(n0,pv20)
& leq(n0,pv1376)
& leq(pv19,minus(n410,n1))
& leq(pv20,minus(n330,n1))
& leq(pv1376,n3)
& ! [X1] :
( ! [X2] :
( init = a_select3(simplex7_init,X2,X1)
| ~ leq(n0,X2)
| ~ leq(X2,n3) )
| ~ leq(n0,X1)
| ~ leq(X1,n2) )
& ! [X3] :
( init = a_select2(s_values7_init,X3)
| ~ leq(n0,X3)
| ~ leq(X3,minus(pv1376,n1)) ) ),
inference(rectify,[],[f163]) ).
fof(f175,plain,
( ( init != init
| init != a_select3(simplex7_init,pv1376,n0)
| init != a_select3(simplex7_init,pv1376,n1)
| init != a_select3(simplex7_init,pv1376,n2)
| init != a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20)
| ~ leq(n0,pv19)
| ~ leq(n0,pv1376)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv1376,n3)
| sP0
| ( init != a_select2(s_values7_init,sK7)
& leq(n0,sK7)
& leq(sK7,minus(pv1376,n1)) ) )
& init = init
& leq(n0,pv19)
& leq(n0,pv20)
& leq(n0,pv1376)
& leq(pv19,minus(n410,n1))
& leq(pv20,minus(n330,n1))
& leq(pv1376,n3)
& ! [X1] :
( ! [X2] :
( init = a_select3(simplex7_init,X2,X1)
| ~ leq(n0,X2)
| ~ leq(X2,n3) )
| ~ leq(n0,X1)
| ~ leq(X1,n2) )
& ! [X3] :
( init = a_select2(s_values7_init,X3)
| ~ leq(n0,X3)
| ~ leq(X3,minus(pv1376,n1)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(X0,sK7)],[f174]) ).
fof(f209,plain,
( leq(sK5,n2)
| ~ sP0 ),
inference(cnf_transformation,[],[f173]) ).
fof(f210,plain,
( leq(n0,sK5)
| ~ sP0 ),
inference(cnf_transformation,[],[f173]) ).
fof(f211,plain,
( leq(sK6,n3)
| ~ sP0 ),
inference(cnf_transformation,[],[f173]) ).
fof(f212,plain,
( leq(n0,sK6)
| ~ sP0 ),
inference(cnf_transformation,[],[f173]) ).
fof(f213,plain,
( init != a_select3(simplex7_init,sK6,sK5)
| ~ sP0 ),
inference(cnf_transformation,[],[f173]) ).
fof(f214,plain,
! [X3] :
( ~ leq(X3,minus(pv1376,n1))
| ~ leq(n0,X3)
| init = a_select2(s_values7_init,X3) ),
inference(cnf_transformation,[],[f175]) ).
fof(f215,plain,
! [X2,X1] :
( ~ leq(X1,n2)
| ~ leq(n0,X2)
| ~ leq(X2,n3)
| ~ leq(n0,X1)
| init = a_select3(simplex7_init,X2,X1) ),
inference(cnf_transformation,[],[f175]) ).
fof(f216,plain,
leq(pv1376,n3),
inference(cnf_transformation,[],[f175]) ).
fof(f217,plain,
leq(pv20,minus(n330,n1)),
inference(cnf_transformation,[],[f175]) ).
fof(f218,plain,
leq(pv19,minus(n410,n1)),
inference(cnf_transformation,[],[f175]) ).
fof(f219,plain,
leq(n0,pv1376),
inference(cnf_transformation,[],[f175]) ).
fof(f220,plain,
leq(n0,pv20),
inference(cnf_transformation,[],[f175]) ).
fof(f221,plain,
leq(n0,pv19),
inference(cnf_transformation,[],[f175]) ).
fof(f223,plain,
( init != init
| init != a_select3(simplex7_init,pv1376,n0)
| init != a_select3(simplex7_init,pv1376,n1)
| init != a_select3(simplex7_init,pv1376,n2)
| init != a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20)
| ~ leq(n0,pv19)
| ~ leq(n0,pv1376)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv1376,n3)
| sP0
| leq(sK7,minus(pv1376,n1)) ),
inference(cnf_transformation,[],[f175]) ).
fof(f224,plain,
( init != init
| init != a_select3(simplex7_init,pv1376,n0)
| init != a_select3(simplex7_init,pv1376,n1)
| init != a_select3(simplex7_init,pv1376,n2)
| init != a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20)
| ~ leq(n0,pv19)
| ~ leq(n0,pv1376)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv1376,n3)
| sP0
| leq(n0,sK7) ),
inference(cnf_transformation,[],[f175]) ).
fof(f225,plain,
( init != init
| init != a_select3(simplex7_init,pv1376,n0)
| init != a_select3(simplex7_init,pv1376,n1)
| init != a_select3(simplex7_init,pv1376,n2)
| init != a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20)
| ~ leq(n0,pv19)
| ~ leq(n0,pv1376)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv1376,n3)
| sP0
| init != a_select2(s_values7_init,sK7) ),
inference(cnf_transformation,[],[f175]) ).
fof(f304,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( a_select3(tptp_const_array2(dim(X1,X2),dim(X4,X5),X6),X0,X3) = X6
| ~ leq(X1,X0)
| ~ leq(X0,X2)
| ~ leq(X4,X3)
| ~ leq(X3,X5) ),
inference(cnf_transformation,[],[f147]) ).
fof(f314,plain,
! [X0,X1] :
( leq(X0,X1)
| ~ gt(X1,X0) ),
inference(cnf_transformation,[],[f155]) ).
fof(f316,plain,
! [X0] : leq(X0,X0),
inference(cnf_transformation,[],[f4]) ).
fof(f323,plain,
gt(n2,n1),
inference(cnf_transformation,[],[f80]) ).
fof(f328,plain,
gt(n1,n0),
inference(cnf_transformation,[],[f73]) ).
fof(f339,plain,
gt(n2,n0),
inference(cnf_transformation,[],[f74]) ).
fof(f380,plain,
( init != a_select3(simplex7_init,pv1376,n0)
| init != a_select3(simplex7_init,pv1376,n1)
| init != a_select3(simplex7_init,pv1376,n2)
| init != a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20)
| ~ leq(n0,pv19)
| ~ leq(n0,pv1376)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv1376,n3)
| sP0
| leq(sK7,minus(pv1376,n1)) ),
inference(trivial_inequality_removal,[],[f223]) ).
fof(f381,plain,
( init != a_select3(simplex7_init,pv1376,n0)
| init != a_select3(simplex7_init,pv1376,n1)
| init != a_select3(simplex7_init,pv1376,n2)
| init != a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20)
| ~ leq(n0,pv19)
| ~ leq(n0,pv1376)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv1376,n3)
| sP0
| leq(n0,sK7) ),
inference(trivial_inequality_removal,[],[f224]) ).
fof(f382,plain,
( init != a_select3(simplex7_init,pv1376,n0)
| init != a_select3(simplex7_init,pv1376,n1)
| init != a_select3(simplex7_init,pv1376,n2)
| init != a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20)
| ~ leq(n0,pv19)
| ~ leq(n0,pv1376)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv1376,n3)
| sP0
| init != a_select2(s_values7_init,sK7) ),
inference(trivial_inequality_removal,[],[f225]) ).
fof(f386,plain,
( init != a_select3(simplex7_init,pv1376,n0)
| init != a_select3(simplex7_init,pv1376,n1)
| init != a_select3(simplex7_init,pv1376,n2)
| init != a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20)
| ~ leq(n0,pv1376)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv1376,n3)
| sP0
| leq(sK7,minus(pv1376,n1)) ),
inference(forward_subsumption_resolution,[],[f380,f221]) ).
fof(f387,plain,
( init != a_select3(simplex7_init,pv1376,n0)
| init != a_select3(simplex7_init,pv1376,n1)
| init != a_select3(simplex7_init,pv1376,n2)
| init != a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20)
| ~ leq(n0,pv1376)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv1376,n3)
| sP0
| leq(n0,sK7) ),
inference(forward_subsumption_resolution,[],[f381,f221]) ).
fof(f388,plain,
( init != a_select3(simplex7_init,pv1376,n0)
| init != a_select3(simplex7_init,pv1376,n1)
| init != a_select3(simplex7_init,pv1376,n2)
| init != a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20)
| ~ leq(n0,pv1376)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv1376,n3)
| sP0
| init != a_select2(s_values7_init,sK7) ),
inference(forward_subsumption_resolution,[],[f382,f221]) ).
fof(f390,definition,
( spl35_1
<=> sP0 ),
introduced(definition,[new_symbols(definition,[spl35_1])],[avatar_definition]) ).
fof(f394,definition,
( spl35_2
<=> leq(sK5,n2) ),
introduced(definition,[new_symbols(definition,[spl35_2])],[avatar_definition]) ).
fof(f396,plain,
( leq(sK5,n2)
| ~ spl35_2 ),
inference(avatar_component_clause,[],[f394]) ).
fof(f397,plain,
( ~ spl35_1
| spl35_2 ),
inference(avatar_split_clause,[],[f209,f394,f390]) ).
fof(f399,definition,
( spl35_3
<=> leq(n0,sK5) ),
introduced(definition,[new_symbols(definition,[spl35_3])],[avatar_definition]) ).
fof(f401,plain,
( leq(n0,sK5)
| ~ spl35_3 ),
inference(avatar_component_clause,[],[f399]) ).
fof(f402,plain,
( ~ spl35_1
| spl35_3 ),
inference(avatar_split_clause,[],[f210,f399,f390]) ).
fof(f404,definition,
( spl35_4
<=> leq(sK6,n3) ),
introduced(definition,[new_symbols(definition,[spl35_4])],[avatar_definition]) ).
fof(f406,plain,
( leq(sK6,n3)
| ~ spl35_4 ),
inference(avatar_component_clause,[],[f404]) ).
fof(f407,plain,
( ~ spl35_1
| spl35_4 ),
inference(avatar_split_clause,[],[f211,f404,f390]) ).
fof(f409,definition,
( spl35_5
<=> leq(n0,sK6) ),
introduced(definition,[new_symbols(definition,[spl35_5])],[avatar_definition]) ).
fof(f411,plain,
( leq(n0,sK6)
| ~ spl35_5 ),
inference(avatar_component_clause,[],[f409]) ).
fof(f412,plain,
( ~ spl35_1
| spl35_5 ),
inference(avatar_split_clause,[],[f212,f409,f390]) ).
fof(f414,definition,
( spl35_6
<=> init = a_select3(simplex7_init,sK6,sK5) ),
introduced(definition,[new_symbols(definition,[spl35_6])],[avatar_definition]) ).
fof(f416,plain,
( init != a_select3(simplex7_init,sK6,sK5)
| spl35_6 ),
inference(avatar_component_clause,[],[f414]) ).
fof(f417,plain,
( ~ spl35_1
| ~ spl35_6 ),
inference(avatar_split_clause,[],[f213,f414,f390]) ).
fof(f418,plain,
( init != a_select3(simplex7_init,pv1376,n0)
| init != a_select3(simplex7_init,pv1376,n1)
| init != a_select3(simplex7_init,pv1376,n2)
| init != a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv1376,n3)
| sP0
| leq(sK7,minus(pv1376,n1)) ),
inference(forward_subsumption_resolution,[],[f386,f219]) ).
fof(f419,plain,
( init != a_select3(simplex7_init,pv1376,n0)
| init != a_select3(simplex7_init,pv1376,n1)
| init != a_select3(simplex7_init,pv1376,n2)
| init != a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv1376,n3)
| sP0
| leq(n0,sK7) ),
inference(forward_subsumption_resolution,[],[f387,f219]) ).
fof(f420,plain,
( init != a_select3(simplex7_init,pv1376,n0)
| init != a_select3(simplex7_init,pv1376,n1)
| init != a_select3(simplex7_init,pv1376,n2)
| init != a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv1376,n3)
| sP0
| init != a_select2(s_values7_init,sK7) ),
inference(forward_subsumption_resolution,[],[f388,f219]) ).
fof(f421,plain,
( init != a_select3(simplex7_init,pv1376,n0)
| init != a_select3(simplex7_init,pv1376,n1)
| init != a_select3(simplex7_init,pv1376,n2)
| init != a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20)
| ~ leq(pv1376,n3)
| sP0
| leq(sK7,minus(pv1376,n1)) ),
inference(forward_subsumption_resolution,[],[f418,f218]) ).
fof(f422,plain,
( init != a_select3(simplex7_init,pv1376,n0)
| init != a_select3(simplex7_init,pv1376,n1)
| init != a_select3(simplex7_init,pv1376,n2)
| init != a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20)
| ~ leq(pv1376,n3)
| sP0
| leq(n0,sK7) ),
inference(forward_subsumption_resolution,[],[f419,f218]) ).
fof(f423,plain,
( init != a_select3(simplex7_init,pv1376,n0)
| init != a_select3(simplex7_init,pv1376,n1)
| init != a_select3(simplex7_init,pv1376,n2)
| init != a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20)
| ~ leq(pv1376,n3)
| sP0
| init != a_select2(s_values7_init,sK7) ),
inference(forward_subsumption_resolution,[],[f420,f218]) ).
fof(f424,plain,
( init != a_select3(simplex7_init,pv1376,n0)
| init != a_select3(simplex7_init,pv1376,n1)
| init != a_select3(simplex7_init,pv1376,n2)
| init != a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20)
| sP0
| leq(sK7,minus(pv1376,n1)) ),
inference(forward_subsumption_resolution,[],[f421,f216]) ).
fof(f425,plain,
( init != a_select3(simplex7_init,pv1376,n0)
| init != a_select3(simplex7_init,pv1376,n1)
| init != a_select3(simplex7_init,pv1376,n2)
| init != a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20)
| sP0
| leq(n0,sK7) ),
inference(forward_subsumption_resolution,[],[f422,f216]) ).
fof(f426,plain,
( init != a_select3(simplex7_init,pv1376,n0)
| init != a_select3(simplex7_init,pv1376,n1)
| init != a_select3(simplex7_init,pv1376,n2)
| init != a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20)
| sP0
| init != a_select2(s_values7_init,sK7) ),
inference(forward_subsumption_resolution,[],[f423,f216]) ).
fof(f428,definition,
( spl35_7
<=> leq(sK7,minus(pv1376,n1)) ),
introduced(definition,[new_symbols(definition,[spl35_7])],[avatar_definition]) ).
fof(f430,plain,
( leq(sK7,minus(pv1376,n1))
| ~ spl35_7 ),
inference(avatar_component_clause,[],[f428]) ).
fof(f432,definition,
( spl35_8
<=> init = a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20) ),
introduced(definition,[new_symbols(definition,[spl35_8])],[avatar_definition]) ).
fof(f434,plain,
( init != a_select3(tptp_const_array2(dim(n0,minus(n410,n1)),dim(n0,minus(n330,n1)),init),pv19,pv20)
| spl35_8 ),
inference(avatar_component_clause,[],[f432]) ).
fof(f436,definition,
( spl35_9
<=> init = a_select3(simplex7_init,pv1376,n2) ),
introduced(definition,[new_symbols(definition,[spl35_9])],[avatar_definition]) ).
fof(f438,plain,
( init != a_select3(simplex7_init,pv1376,n2)
| spl35_9 ),
inference(avatar_component_clause,[],[f436]) ).
fof(f440,definition,
( spl35_10
<=> init = a_select3(simplex7_init,pv1376,n1) ),
introduced(definition,[new_symbols(definition,[spl35_10])],[avatar_definition]) ).
fof(f444,definition,
( spl35_11
<=> init = a_select3(simplex7_init,pv1376,n0) ),
introduced(definition,[new_symbols(definition,[spl35_11])],[avatar_definition]) ).
fof(f447,plain,
( spl35_7
| spl35_1
| ~ spl35_8
| ~ spl35_9
| ~ spl35_10
| ~ spl35_11 ),
inference(avatar_split_clause,[],[f424,f444,f440,f436,f432,f390,f428]) ).
fof(f449,definition,
( spl35_12
<=> leq(n0,sK7) ),
introduced(definition,[new_symbols(definition,[spl35_12])],[avatar_definition]) ).
fof(f451,plain,
( leq(n0,sK7)
| ~ spl35_12 ),
inference(avatar_component_clause,[],[f449]) ).
fof(f452,plain,
( spl35_12
| spl35_1
| ~ spl35_8
| ~ spl35_9
| ~ spl35_10
| ~ spl35_11 ),
inference(avatar_split_clause,[],[f425,f444,f440,f436,f432,f390,f449]) ).
fof(f454,definition,
( spl35_13
<=> init = a_select2(s_values7_init,sK7) ),
introduced(definition,[new_symbols(definition,[spl35_13])],[avatar_definition]) ).
fof(f456,plain,
( init != a_select2(s_values7_init,sK7)
| spl35_13 ),
inference(avatar_component_clause,[],[f454]) ).
fof(f457,plain,
( ~ spl35_13
| spl35_1
| ~ spl35_8
| ~ spl35_9
| ~ spl35_10
| ~ spl35_11 ),
inference(avatar_split_clause,[],[f426,f444,f440,f436,f432,f390,f454]) ).
fof(f459,plain,
! [X0] :
( ~ leq(n0,X0)
| ~ leq(X0,n3)
| ~ leq(n0,n2)
| init = a_select3(simplex7_init,X0,n2) ),
inference(resolution,[],[f316,f215]) ).
fof(f461,definition,
( spl35_14
<=> leq(n0,n2) ),
introduced(definition,[new_symbols(definition,[spl35_14])],[avatar_definition]) ).
fof(f463,plain,
( ~ leq(n0,n2)
| spl35_14 ),
inference(avatar_component_clause,[],[f461]) ).
fof(f465,definition,
( spl35_15
<=> ! [X0] :
( ~ leq(n0,X0)
| init = a_select3(simplex7_init,X0,n2)
| ~ leq(X0,n3) ) ),
introduced(definition,[new_symbols(definition,[spl35_15])],[avatar_definition]) ).
fof(f466,plain,
( ! [X0] :
( init = a_select3(simplex7_init,X0,n2)
| ~ leq(n0,X0)
| ~ leq(X0,n3) )
| ~ spl35_15 ),
inference(avatar_component_clause,[],[f465]) ).
fof(f467,plain,
( ~ spl35_14
| spl35_15 ),
inference(avatar_split_clause,[],[f459,f465,f461]) ).
fof(f478,plain,
! [X0,X1] :
( ~ leq(X1,n3)
| ~ leq(n0,X1)
| ~ gt(n2,X0)
| ~ leq(n0,X0)
| init = a_select3(simplex7_init,X1,X0) ),
inference(resolution,[],[f314,f215]) ).
fof(f479,plain,
( ~ gt(n2,n0)
| spl35_14 ),
inference(resolution,[],[f314,f463]) ).
fof(f481,plain,
( $false
| spl35_14 ),
inference(forward_subsumption_resolution,[],[f479,f339]) ).
fof(f482,plain,
spl35_14,
inference(avatar_contradiction_clause,[],[f481]) ).
fof(f486,plain,
( init != init
| ~ leq(n0,pv1376)
| ~ leq(pv1376,n3)
| spl35_9
| ~ spl35_15 ),
inference(superposition,[],[f438,f466]) ).
fof(f487,plain,
( ~ leq(n0,pv1376)
| ~ leq(pv1376,n3)
| spl35_9
| ~ spl35_15 ),
inference(trivial_inequality_removal,[],[f486]) ).
fof(f488,plain,
( ~ leq(pv1376,n3)
| spl35_9
| ~ spl35_15 ),
inference(forward_subsumption_resolution,[],[f487,f219]) ).
fof(f489,plain,
( $false
| spl35_9
| ~ spl35_15 ),
inference(forward_subsumption_resolution,[],[f488,f216]) ).
fof(f490,plain,
( spl35_9
| ~ spl35_15 ),
inference(avatar_contradiction_clause,[],[f489]) ).
fof(f493,plain,
! [X0] :
( ~ leq(n0,pv1376)
| ~ gt(n2,X0)
| ~ leq(n0,X0)
| init = a_select3(simplex7_init,pv1376,X0) ),
inference(resolution,[],[f478,f216]) ).
fof(f494,plain,
! [X0] :
( ~ gt(n2,X0)
| ~ leq(n0,X0)
| init = a_select3(simplex7_init,pv1376,X0) ),
inference(forward_subsumption_resolution,[],[f493,f219]) ).
fof(f508,plain,
( ~ leq(n0,n0)
| init = a_select3(simplex7_init,pv1376,n0) ),
inference(resolution,[],[f494,f339]) ).
fof(f510,plain,
( ~ leq(n0,n1)
| init = a_select3(simplex7_init,pv1376,n1) ),
inference(resolution,[],[f494,f323]) ).
fof(f512,definition,
( spl35_20
<=> leq(n0,n1) ),
introduced(definition,[new_symbols(definition,[spl35_20])],[avatar_definition]) ).
fof(f514,plain,
( ~ leq(n0,n1)
| spl35_20 ),
inference(avatar_component_clause,[],[f512]) ).
fof(f515,plain,
( spl35_10
| ~ spl35_20 ),
inference(avatar_split_clause,[],[f510,f512,f440]) ).
fof(f525,plain,
init = a_select3(simplex7_init,pv1376,n0),
inference(forward_subsumption_resolution,[],[f508,f316]) ).
fof(f526,plain,
spl35_11,
inference(avatar_split_clause,[],[f525,f444]) ).
fof(f527,plain,
( ~ gt(n1,n0)
| spl35_20 ),
inference(resolution,[],[f514,f314]) ).
fof(f528,plain,
( $false
| spl35_20 ),
inference(forward_subsumption_resolution,[],[f527,f328]) ).
fof(f529,plain,
spl35_20,
inference(avatar_contradiction_clause,[],[f528]) ).
fof(f920,plain,
( init != init
| ~ leq(n0,pv19)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(n0,pv20)
| ~ leq(pv20,minus(n330,n1))
| spl35_8 ),
inference(superposition,[],[f434,f304]) ).
fof(f925,plain,
( ~ leq(n0,pv19)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(n0,pv20)
| ~ leq(pv20,minus(n330,n1))
| spl35_8 ),
inference(trivial_inequality_removal,[],[f920]) ).
fof(f926,plain,
( ~ leq(pv19,minus(n410,n1))
| ~ leq(n0,pv20)
| ~ leq(pv20,minus(n330,n1))
| spl35_8 ),
inference(forward_subsumption_resolution,[],[f925,f221]) ).
fof(f927,plain,
( ~ leq(n0,pv20)
| ~ leq(pv20,minus(n330,n1))
| spl35_8 ),
inference(forward_subsumption_resolution,[],[f926,f218]) ).
fof(f928,plain,
( ~ leq(pv20,minus(n330,n1))
| spl35_8 ),
inference(forward_subsumption_resolution,[],[f927,f220]) ).
fof(f929,plain,
( $false
| spl35_8 ),
inference(forward_subsumption_resolution,[],[f928,f217]) ).
fof(f930,plain,
spl35_8,
inference(avatar_contradiction_clause,[],[f929]) ).
fof(f1941,plain,
( ~ leq(n0,sK7)
| init = a_select2(s_values7_init,sK7)
| ~ spl35_7 ),
inference(resolution,[],[f430,f214]) ).
fof(f1944,plain,
( init = a_select2(s_values7_init,sK7)
| ~ spl35_7
| ~ spl35_12 ),
inference(forward_subsumption_resolution,[],[f1941,f451]) ).
fof(f1945,plain,
( $false
| ~ spl35_7
| ~ spl35_12
| spl35_13 ),
inference(forward_subsumption_resolution,[],[f1944,f456]) ).
fof(f1946,plain,
( ~ spl35_7
| ~ spl35_12
| spl35_13 ),
inference(avatar_contradiction_clause,[],[f1945]) ).
fof(f1966,plain,
( ! [X0] :
( ~ leq(n0,X0)
| ~ leq(X0,n3)
| ~ leq(n0,sK5)
| init = a_select3(simplex7_init,X0,sK5) )
| ~ spl35_2 ),
inference(resolution,[],[f396,f215]) ).
fof(f1967,plain,
( ! [X0] :
( init = a_select3(simplex7_init,X0,sK5)
| ~ leq(X0,n3)
| ~ leq(n0,X0) )
| ~ spl35_2
| ~ spl35_3 ),
inference(forward_subsumption_resolution,[],[f1966,f401]) ).
fof(f2026,plain,
( init != init
| ~ leq(sK6,n3)
| ~ leq(n0,sK6)
| ~ spl35_2
| ~ spl35_3
| spl35_6 ),
inference(superposition,[],[f416,f1967]) ).
fof(f2027,plain,
( ~ leq(sK6,n3)
| ~ leq(n0,sK6)
| ~ spl35_2
| ~ spl35_3
| spl35_6 ),
inference(trivial_inequality_removal,[],[f2026]) ).
fof(f2028,plain,
( ~ leq(n0,sK6)
| ~ spl35_2
| ~ spl35_3
| ~ spl35_4
| spl35_6 ),
inference(forward_subsumption_resolution,[],[f2027,f406]) ).
fof(f2029,plain,
( $false
| ~ spl35_2
| ~ spl35_3
| ~ spl35_4
| ~ spl35_5
| spl35_6 ),
inference(forward_subsumption_resolution,[],[f2028,f411]) ).
fof(f2030,plain,
( ~ spl35_2
| ~ spl35_3
| ~ spl35_4
| ~ spl35_5
| spl35_6 ),
inference(avatar_contradiction_clause,[],[f2029]) ).
cnf(s1,plain,
( ~ spl35_1
| spl35_2 ),
inference(sat_conversion,[],[f397]) ).
cnf(s2,plain,
( ~ spl35_1
| spl35_3 ),
inference(sat_conversion,[],[f402]) ).
cnf(s3,plain,
( ~ spl35_1
| spl35_4 ),
inference(sat_conversion,[],[f407]) ).
cnf(s4,plain,
( ~ spl35_1
| spl35_5 ),
inference(sat_conversion,[],[f412]) ).
cnf(s5,plain,
( ~ spl35_1
| ~ spl35_6 ),
inference(sat_conversion,[],[f417]) ).
cnf(s6,plain,
( spl35_1
| spl35_7
| ~ spl35_8
| ~ spl35_9
| ~ spl35_10
| ~ spl35_11 ),
inference(sat_conversion,[],[f447]) ).
cnf(s7,plain,
( spl35_1
| ~ spl35_8
| ~ spl35_9
| ~ spl35_10
| ~ spl35_11
| spl35_12 ),
inference(sat_conversion,[],[f452]) ).
cnf(s8,plain,
( spl35_1
| ~ spl35_8
| ~ spl35_9
| ~ spl35_10
| ~ spl35_11
| ~ spl35_13 ),
inference(sat_conversion,[],[f457]) ).
cnf(s9,plain,
( ~ spl35_14
| spl35_15 ),
inference(sat_conversion,[],[f467]) ).
cnf(s11,plain,
spl35_14,
inference(sat_conversion,[],[f482]) ).
cnf(s12,plain,
( spl35_9
| ~ spl35_15 ),
inference(sat_conversion,[],[f490]) ).
cnf(s15,plain,
( spl35_10
| ~ spl35_20 ),
inference(sat_conversion,[],[f515]) ).
cnf(s17,plain,
spl35_11,
inference(sat_conversion,[],[f526]) ).
cnf(s18,plain,
spl35_20,
inference(sat_conversion,[],[f529]) ).
cnf(s22,plain,
spl35_8,
inference(sat_conversion,[],[f930]) ).
cnf(s51,plain,
( ~ spl35_7
| ~ spl35_12
| spl35_13 ),
inference(sat_conversion,[],[f1946]) ).
cnf(s55,plain,
( ~ spl35_2
| ~ spl35_3
| ~ spl35_4
| ~ spl35_5
| spl35_6 ),
inference(sat_conversion,[],[f2030]) ).
cnf(s64,plain,
spl35_10,
inference(rat,[],[s15,s18]) ).
cnf(s69,plain,
spl35_15,
inference(rat,[],[s9,s11]) ).
cnf(s70,plain,
spl35_9,
inference(rat,[],[s12,s69]) ).
cnf(s71,plain,
( spl35_1
| ~ spl35_13 ),
inference(rat,[],[s8,s17,s64,s70,s22]) ).
cnf(s72,plain,
( spl35_1
| spl35_12 ),
inference(rat,[],[s7,s17,s64,s70,s22]) ).
cnf(s73,plain,
( spl35_1
| spl35_7 ),
inference(rat,[],[s6,s17,s64,s70,s22]) ).
cnf(s74,plain,
spl35_1,
inference(rat,[],[s51,s73,s72,s71]) ).
cnf(s75,plain,
~ spl35_6,
inference(rat,[],[s5,s74]) ).
cnf(s76,plain,
spl35_5,
inference(rat,[],[s4,s74]) ).
cnf(s77,plain,
spl35_4,
inference(rat,[],[s3,s74]) ).
cnf(s78,plain,
spl35_3,
inference(rat,[],[s2,s74]) ).
cnf(s79,plain,
spl35_2,
inference(rat,[],[s1,s74]) ).
cnf(s80,plain,
$false,
inference(rat,[],[s55,s75,s76,s77,s78,s79]) ).
fof(f2031,plain,
$false,
inference(avatar_sat_refutation,[],[s80]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWV032+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.23/0.28 % Computer : n007.cluster.edu
% 0.23/0.28 % Model : x86_64 x86_64
% 0.23/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.23/0.28 % Memory : 8046.5625MB
% 0.23/0.28 % OS : Linux 6.8.0-71-generic
% 0.23/0.28 % CPULimit : 300
% 0.23/0.28 % WCLimit : 300
% 0.23/0.28 % DateTime : Mon Sep 28 09:41:41 UTC 2026
% 0.23/0.28 % CPUTime :
% 0.23/0.28 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.23/0.32 Running first-order theorem proving
% 0.23/0.32 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 6.30/2.02 % (2281075)Detected formulas, will run a generic FOF schedule.
% 6.30/2.02 % (2281092)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=2080734160:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 6.30/2.02 % (2281096)dis-21_1_sil=8000:lcm=predicate:random_seed=457517827:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 6.30/2.02 % (2281093)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2641679593:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 6.30/2.02 % (2281094)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=482203461:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 6.30/2.02 % (2281090)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=2823637013:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 6.30/2.02 % (2281095)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1613779320:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 6.30/2.02 % (2281091)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=3897315872:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 6.30/2.02 % (2281096)Instruction limit reached!
% 6.30/2.02 % (2281096)------------------------------
% 6.30/2.02 % (2281096)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.30/2.02 % (2281096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.30/2.02 % (2281096)CaDiCaL version: 2.1.3
% 6.30/2.02 % (2281096)Termination reason: Instruction limit
% 6.30/2.02 % (2281096)Termination phase: Saturation
% 6.30/2.02 % (2281096)Time elapsed: 0.111 s
% 6.30/2.02 % (2281096)Peak memory usage: 89 MB
% 6.30/2.02 % (2281096)Instructions burned: 129 (million)
% 6.30/2.02 % (2281093)Instruction limit reached!
% 6.30/2.02 % (2281093)------------------------------
% 6.30/2.02 % (2281093)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.30/2.02 % (2281093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.30/2.02 % (2281093)CaDiCaL version: 2.1.3
% 6.30/2.02 % (2281093)Termination reason: Instruction limit
% 6.30/2.02 % (2281093)Termination phase: Saturation
% 6.30/2.02 % (2281093)Time elapsed: 0.100 s
% 6.30/2.02 % (2281093)Peak memory usage: 89 MB
% 6.30/2.02 % (2281093)Instructions burned: 109 (million)
% 6.30/2.02 % (2281094)Instruction limit reached!
% 6.30/2.02 % (2281094)------------------------------
% 6.30/2.02 % (2281094)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.30/2.02 % (2281094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.30/2.02 % (2281094)CaDiCaL version: 2.1.3
% 6.30/2.02 % (2281094)Termination reason: Instruction limit
% 6.30/2.02 % (2281094)Termination phase: Saturation
% 6.30/2.02 % (2281094)Time elapsed: 0.119 s
% 6.30/2.02 % (2281094)Peak memory usage: 88 MB
% 6.30/2.02 % (2281094)Instructions burned: 119 (million)
% 6.30/2.02 % (2281095)Instruction limit reached!
% 6.30/2.02 % (2281095)------------------------------
% 6.30/2.02 % (2281095)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.30/2.02 % (2281095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.30/2.02 % (2281095)CaDiCaL version: 2.1.3
% 6.30/2.02 % (2281095)Termination reason: Instruction limit
% 6.30/2.02 % (2281095)Termination phase: Saturation
% 6.30/2.02 % (2281095)Time elapsed: 0.141 s
% 6.30/2.02 % (2281095)Peak memory usage: 90 MB
% 6.30/2.02 % (2281095)Instructions burned: 140 (million)
% 6.30/2.02 % (2281104)lrs+10_1_sil=8000:sp=occurrence:random_seed=1642815570:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi)
% 6.30/2.02 % (2281106)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3425802419:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi)
% 6.30/2.02 % (2281107)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1308927375:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi)
% 6.30/2.02 % (2281109)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=1692880299:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi)
% 6.30/2.02 % (2281107)First to succeed.
% 6.30/2.02 % (2281106)Instruction limit reached!
% 6.30/2.02 % (2281106)------------------------------
% 6.30/2.02 % (2281106)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.30/2.02 % (2281106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.30/2.02 % (2281106)CaDiCaL version: 2.1.3
% 6.30/2.02 % (2281106)Termination reason: Instruction limit
% 6.30/2.02 % (2281106)Termination phase: Saturation
% 6.30/2.02 % (2281106)Time elapsed: 0.137 s
% 6.30/2.02 % (2281106)Peak memory usage: 92 MB
% 6.30/2.02 % (2281106)Instructions burned: 157 (million)
% 6.30/2.02 % (2281107)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2281075"
% 6.30/2.02 % (2281104)Instruction limit reached!
% 6.30/2.02 % (2281104)------------------------------
% 6.30/2.02 % (2281104)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.30/2.02 % (2281104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.30/2.02 % (2281104)CaDiCaL version: 2.1.3
% 6.30/2.02 % (2281104)Termination reason: Instruction limit
% 6.30/2.02 % (2281104)Termination phase: Saturation
% 6.30/2.02 % (2281104)Time elapsed: 0.287 s
% 6.30/2.02 % (2281104)Peak memory usage: 92 MB
% 6.30/2.02 % (2281104)Instructions burned: 285 (million)
% 6.30/2.02 % (2281109)Instruction limit reached!
% 6.30/2.02 % (2281109)------------------------------
% 6.30/2.02 % (2281109)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.30/2.02 % (2281109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.30/2.02 % (2281109)CaDiCaL version: 2.1.3
% 6.30/2.02 % (2281109)Termination reason: Instruction limit
% 6.30/2.02 % (2281109)Termination phase: Saturation
% 6.30/2.02 % (2281109)Time elapsed: 0.224 s
% 6.30/2.02 % (2281109)Peak memory usage: 92 MB
% 6.30/2.02 % (2281109)Instructions burned: 249 (million)
% 6.30/2.02 % (2281114)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3541263408:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi)
% 6.30/2.02 % (2281092)Also succeeded, but the first one will report.
% 6.30/2.02 % (2281114)Instruction limit reached!
% 6.30/2.02 % (2281114)------------------------------
% 6.30/2.02 % (2281114)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.30/2.02 % (2281114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.30/2.02 % (2281114)CaDiCaL version: 2.1.3
% 6.30/2.02 % (2281114)Termination reason: Instruction limit
% 6.30/2.02 % (2281114)Termination phase: Saturation
% 6.30/2.02 % (2281114)Time elapsed: 0.157 s
% 6.30/2.02 % (2281114)Peak memory usage: 90 MB
% 6.30/2.02 % (2281114)Instructions burned: 294 (million)
% 6.30/2.02 % (2281115)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=974034133:i=2350_2992 on theBenchmark for (2992ds/2350Mi)
% 6.30/2.02 % (2281116)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3131344040:cts=off:i=113:fsr=off:ss=included:sgt=4_2992 on theBenchmark for (2992ds/113Mi)
% 6.30/2.02 % (2281107)Refutation found. Thanks to Tanya!
% 6.30/2.02 % SZS status Theorem for theBenchmark
% 6.30/2.02 % SZS output start Proof for theBenchmark
% See solution above
% 8.56/2.21 % (2281107)------------------------------
% 8.56/2.21 % (2281107)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.56/2.21 % (2281107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.56/2.21 % (2281107)CaDiCaL version: 2.1.3
% 8.56/2.21 % (2281107)Termination reason: Refutation
% 8.56/2.21 % (2281107)Time elapsed: 0.121 s
% 8.56/2.21 % (2281107)Peak memory usage: 91 MB
% 8.56/2.21 % (2281107)Instructions burned: 115 (million)
% 8.56/2.21 % (2281107)------------------------------
% 8.56/2.21 % (2281107)------------------------------
% 8.56/2.21 % (2281075)Success in time 1.084 s
% 8.56/2.21 % Vampire exiting
%------------------------------------------------------------------------------