%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWV491+4 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n004.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:24:26 PM UTC 2026
% Result : Theorem 53.77s 7.94s
% Output : Refutation 53.77s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 28
% Syntax : Number of formulae : 212 ( 19 unt; 18 def)
% Number of atoms : 733 ( 144 equ)
% Maximal formula atoms : 17 ( 3 avg)
% Number of connectives : 894 ( 373 ~; 417 |; 63 &)
% ( 20 <=>; 21 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 22 ( 20 usr; 19 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 7 con; 0-2 aty)
% Number of variables : 165 ( 0 sgn 158 !; 7 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( int_leq(X0,X1)
<=> ( int_less(X0,X1)
| X0 = X1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',int_leq) ).
fof(f2,axiom,
! [X0,X1,X2] :
( ( int_less(X0,X1)
& int_less(X1,X2) )
=> int_less(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',int_less_transitive) ).
fof(f3,axiom,
! [X0,X1] :
( int_less(X0,X1)
=> X0 != X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',int_less_irreflexive) ).
fof(f4,axiom,
! [X0,X1] :
( int_less(X0,X1)
| int_leq(X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',int_less_total) ).
fof(f6,axiom,
! [X0,X1] : plus(X0,X1) = plus(X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',plus_commutative) ).
fof(f7,axiom,
! [X0] : plus(X0,int_zero) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',plus_zero) ).
fof(f8,axiom,
! [X0,X1,X2,X3] :
( ( int_less(X0,X1)
& int_leq(X2,X3) )
=> int_leq(plus(X0,X2),plus(X1,X3)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',plus_and_order1) ).
fof(f9,axiom,
! [X0,X1] :
( int_less(X0,X1)
<=> ? [X2] :
( plus(X0,X2) = X1
& int_less(int_zero,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',plus_and_inverse) ).
fof(f12,axiom,
! [X0,X1] :
( ( int_leq(int_one,X0)
& int_leq(X0,n)
& int_leq(int_one,X1)
& int_leq(X1,n) )
=> ( ! [X2] :
( ( int_less(int_zero,X2)
& X0 = plus(X1,X2) )
=> ! [X3] :
( ( int_leq(int_one,X3)
& int_leq(X3,X1) )
=> a(plus(X3,X2),X3) = real_zero ) )
& ! [X3] :
( ( int_leq(int_one,X3)
& int_leq(X3,X1) )
=> a(X3,X3) = real_one )
& ! [X2] :
( ( int_less(int_zero,X2)
& X1 = plus(X0,X2) )
=> ! [X3] :
( ( int_leq(int_one,X3)
& int_leq(X3,X0) )
=> a(X3,plus(X3,X2)) = real_zero ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qii) ).
fof(f13,conjecture,
! [X0,X1] :
( ( int_leq(int_one,X0)
& int_leq(X0,n)
& int_leq(int_one,X1)
& int_leq(X1,n) )
=> ( ( X0 != X1
=> a(X0,X1) = real_zero )
& ( X0 = X1
=> a(X0,X1) = real_one ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',id) ).
fof(f14,negated_conjecture,
~ ! [X0,X1] :
( ( int_leq(int_one,X0)
& int_leq(X0,n)
& int_leq(int_one,X1)
& int_leq(X1,n) )
=> ( ( X0 != X1
=> a(X0,X1) = real_zero )
& ( X0 = X1
=> a(X0,X1) = real_one ) ) ),
inference(negated_conjecture,[status(cth)],[f13]) ).
fof(f15,plain,
! [X0,X1] :
( ( int_leq(int_one,X0)
& int_leq(X0,n)
& int_leq(int_one,X1)
& int_leq(X1,n) )
=> ( ! [X2] :
( ( int_less(int_zero,X2)
& X0 = plus(X1,X2) )
=> ! [X3] :
( ( int_leq(int_one,X3)
& int_leq(X3,X1) )
=> a(plus(X3,X2),X3) = real_zero ) )
& ! [X4] :
( ( int_leq(int_one,X4)
& int_leq(X4,X1) )
=> real_one = a(X4,X4) )
& ! [X5] :
( ( int_less(int_zero,X5)
& plus(X0,X5) = X1 )
=> ! [X6] :
( ( int_leq(int_one,X6)
& int_leq(X6,X0) )
=> real_zero = a(X6,plus(X6,X5)) ) ) ) ),
inference(rectify,[],[f12]) ).
fof(f16,plain,
! [X0,X1,X2] :
( int_less(X0,X2)
| ~ int_less(X0,X1)
| ~ int_less(X1,X2) ),
inference(ennf_transformation,[],[f2]) ).
fof(f17,plain,
! [X0,X1,X2] :
( int_less(X0,X2)
| ~ int_less(X0,X1)
| ~ int_less(X1,X2) ),
inference(flattening,[],[f16]) ).
fof(f18,plain,
! [X0,X1] :
( X0 != X1
| ~ int_less(X0,X1) ),
inference(ennf_transformation,[],[f3]) ).
fof(f19,plain,
! [X0,X1,X2,X3] :
( int_leq(plus(X0,X2),plus(X1,X3))
| ~ int_less(X0,X1)
| ~ int_leq(X2,X3) ),
inference(ennf_transformation,[],[f8]) ).
fof(f20,plain,
! [X0,X1,X2,X3] :
( int_leq(plus(X0,X2),plus(X1,X3))
| ~ int_less(X0,X1)
| ~ int_leq(X2,X3) ),
inference(flattening,[],[f19]) ).
fof(f21,plain,
! [X0,X1] :
( ( ! [X2] :
( ! [X3] :
( a(plus(X3,X2),X3) = real_zero
| ~ int_leq(int_one,X3)
| ~ int_leq(X3,X1) )
| ~ int_less(int_zero,X2)
| plus(X1,X2) != X0 )
& ! [X4] :
( real_one = a(X4,X4)
| ~ int_leq(int_one,X4)
| ~ int_leq(X4,X1) )
& ! [X5] :
( ! [X6] :
( real_zero = a(X6,plus(X6,X5))
| ~ int_leq(int_one,X6)
| ~ int_leq(X6,X0) )
| ~ int_less(int_zero,X5)
| plus(X0,X5) != X1 ) )
| ~ int_leq(int_one,X0)
| ~ int_leq(X0,n)
| ~ int_leq(int_one,X1)
| ~ int_leq(X1,n) ),
inference(ennf_transformation,[],[f15]) ).
fof(f22,plain,
! [X0,X1] :
( ( ! [X2] :
( ! [X3] :
( a(plus(X3,X2),X3) = real_zero
| ~ int_leq(int_one,X3)
| ~ int_leq(X3,X1) )
| ~ int_less(int_zero,X2)
| plus(X1,X2) != X0 )
& ! [X4] :
( real_one = a(X4,X4)
| ~ int_leq(int_one,X4)
| ~ int_leq(X4,X1) )
& ! [X5] :
( ! [X6] :
( real_zero = a(X6,plus(X6,X5))
| ~ int_leq(int_one,X6)
| ~ int_leq(X6,X0) )
| ~ int_less(int_zero,X5)
| plus(X0,X5) != X1 ) )
| ~ int_leq(int_one,X0)
| ~ int_leq(X0,n)
| ~ int_leq(int_one,X1)
| ~ int_leq(X1,n) ),
inference(flattening,[],[f21]) ).
fof(f23,plain,
? [X0,X1] :
( ( ( real_zero != a(X0,X1)
& X0 != X1 )
| ( real_one != a(X0,X1)
& X0 = X1 ) )
& int_leq(int_one,X0)
& int_leq(X0,n)
& int_leq(int_one,X1)
& int_leq(X1,n) ),
inference(ennf_transformation,[],[f14]) ).
fof(f24,plain,
? [X0,X1] :
( ( ( real_zero != a(X0,X1)
& X0 != X1 )
| ( real_one != a(X0,X1)
& X0 = X1 ) )
& int_leq(int_one,X0)
& int_leq(X0,n)
& int_leq(int_one,X1)
& int_leq(X1,n) ),
inference(flattening,[],[f23]) ).
fof(f25,plain,
! [X0,X1] :
( ( int_leq(X0,X1)
| ( ~ int_less(X0,X1)
& X0 != X1 ) )
& ( int_less(X0,X1)
| X0 = X1
| ~ int_leq(X0,X1) ) ),
inference(nnf_transformation,[],[f1]) ).
fof(f26,plain,
! [X0,X1] :
( ( int_leq(X0,X1)
| ( ~ int_less(X0,X1)
& X0 != X1 ) )
& ( int_less(X0,X1)
| X0 = X1
| ~ int_leq(X0,X1) ) ),
inference(flattening,[],[f25]) ).
fof(f27,plain,
! [X0,X1] :
( ( int_less(X0,X1)
| ! [X2] :
( plus(X0,X2) != X1
| ~ int_less(int_zero,X2) ) )
& ( ? [X2] :
( plus(X0,X2) = X1
& int_less(int_zero,X2) )
| ~ int_less(X0,X1) ) ),
inference(nnf_transformation,[],[f9]) ).
fof(f28,plain,
! [X0,X1] :
( ( int_less(X0,X1)
| ! [X2] :
( plus(X0,X2) != X1
| ~ int_less(int_zero,X2) ) )
& ( ? [X3] :
( plus(X0,X3) = X1
& int_less(int_zero,X3) )
| ~ int_less(X0,X1) ) ),
inference(rectify,[],[f27]) ).
fof(f29,plain,
! [X0,X1] :
( ( int_less(X0,X1)
| ! [X2] :
( plus(X0,X2) != X1
| ~ int_less(int_zero,X2) ) )
& ( ( plus(X0,sK0(X0,X1)) = X1
& int_less(int_zero,sK0(X0,X1)) )
| ~ int_less(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X3,sK0(X0,X1))],[f28]) ).
fof(f31,plain,
( ( ( real_zero != a(sK1,sK2)
& sK1 != sK2 )
| ( real_one != a(sK1,sK2)
& sK1 = sK2 ) )
& int_leq(int_one,sK1)
& int_leq(sK1,n)
& int_leq(int_one,sK2)
& int_leq(sK2,n) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2]),skolemize(X0,sK1),skolemize(X1,sK2)],[f24]) ).
fof(f32,plain,
! [X0,X1] :
( int_less(X0,X1)
| X0 = X1
| ~ int_leq(X0,X1) ),
inference(cnf_transformation,[],[f26]) ).
fof(f33,plain,
! [X0,X1] :
( int_leq(X0,X1)
| X0 != X1 ),
inference(cnf_transformation,[],[f26]) ).
fof(f34,plain,
! [X0,X1] :
( int_leq(X0,X1)
| ~ int_less(X0,X1) ),
inference(cnf_transformation,[],[f26]) ).
fof(f35,plain,
! [X2,X0,X1] :
( int_less(X0,X2)
| ~ int_less(X0,X1)
| ~ int_less(X1,X2) ),
inference(cnf_transformation,[],[f17]) ).
fof(f36,plain,
! [X0,X1] :
( X0 != X1
| ~ int_less(X0,X1) ),
inference(cnf_transformation,[],[f18]) ).
fof(f37,plain,
! [X0,X1] :
( int_leq(X1,X0)
| int_less(X0,X1) ),
inference(cnf_transformation,[],[f4]) ).
fof(f39,plain,
! [X0,X1] : plus(X0,X1) = plus(X1,X0),
inference(cnf_transformation,[],[f6]) ).
fof(f40,plain,
! [X0] : plus(X0,int_zero) = X0,
inference(cnf_transformation,[],[f7]) ).
fof(f41,plain,
! [X2,X3,X0,X1] :
( int_leq(plus(X0,X2),plus(X1,X3))
| ~ int_less(X0,X1)
| ~ int_leq(X2,X3) ),
inference(cnf_transformation,[],[f20]) ).
fof(f42,plain,
! [X0,X1] :
( int_less(int_zero,sK0(X0,X1))
| ~ int_less(X0,X1) ),
inference(cnf_transformation,[],[f29]) ).
fof(f43,plain,
! [X0,X1] :
( ~ int_less(X0,X1)
| plus(X0,sK0(X0,X1)) = X1 ),
inference(cnf_transformation,[],[f29]) ).
fof(f48,plain,
! [X0,X1,X6,X5] :
( real_zero = a(X6,plus(X6,X5))
| ~ int_leq(int_one,X6)
| ~ int_leq(X6,X0)
| ~ int_less(int_zero,X5)
| plus(X0,X5) != X1
| ~ int_leq(int_one,X0)
| ~ int_leq(X0,n)
| ~ int_leq(int_one,X1)
| ~ int_leq(X1,n) ),
inference(cnf_transformation,[],[f22]) ).
fof(f49,plain,
! [X0,X1,X4] :
( real_one = a(X4,X4)
| ~ int_leq(int_one,X4)
| ~ int_leq(X4,X1)
| ~ int_leq(int_one,X0)
| ~ int_leq(X0,n)
| ~ int_leq(int_one,X1)
| ~ int_leq(X1,n) ),
inference(cnf_transformation,[],[f22]) ).
fof(f50,plain,
! [X2,X3,X0,X1] :
( real_zero = a(plus(X3,X2),X3)
| ~ int_leq(int_one,X3)
| ~ int_leq(X3,X1)
| ~ int_less(int_zero,X2)
| plus(X1,X2) != X0
| ~ int_leq(int_one,X0)
| ~ int_leq(X0,n)
| ~ int_leq(int_one,X1)
| ~ int_leq(X1,n) ),
inference(cnf_transformation,[],[f22]) ).
fof(f51,plain,
int_leq(sK2,n),
inference(cnf_transformation,[],[f31]) ).
fof(f52,plain,
int_leq(int_one,sK2),
inference(cnf_transformation,[],[f31]) ).
fof(f53,plain,
int_leq(sK1,n),
inference(cnf_transformation,[],[f31]) ).
fof(f54,plain,
int_leq(int_one,sK1),
inference(cnf_transformation,[],[f31]) ).
fof(f56,plain,
( sK1 != sK2
| real_one != a(sK1,sK2) ),
inference(cnf_transformation,[],[f31]) ).
fof(f57,plain,
( real_zero != a(sK1,sK2)
| sK1 = sK2 ),
inference(cnf_transformation,[],[f31]) ).
fof(f59,plain,
! [X1] : int_leq(X1,X1),
inference(equality_resolution,[],[f33]) ).
fof(f60,plain,
! [X1] : ~ int_less(X1,X1),
inference(equality_resolution,[],[f36]) ).
fof(f62,plain,
! [X2,X3,X1] :
( ~ int_leq(int_one,X3)
| ~ int_leq(X3,X1)
| ~ int_leq(plus(X1,X2),n)
| ~ int_less(int_zero,X2)
| ~ int_leq(int_one,plus(X1,X2))
| real_zero = a(plus(X3,X2),X3)
| ~ int_leq(int_one,X1)
| ~ int_leq(X1,n) ),
inference(equality_resolution,[],[f50]) ).
fof(f63,plain,
! [X0,X6,X5] :
( ~ int_leq(int_one,X6)
| ~ int_leq(X6,X0)
| ~ int_leq(plus(X0,X5),n)
| ~ int_less(int_zero,X5)
| ~ int_leq(int_one,X0)
| ~ int_leq(X0,n)
| ~ int_leq(int_one,plus(X0,X5))
| real_zero = a(X6,plus(X6,X5)) ),
inference(equality_resolution,[],[f48]) ).
fof(f65,definition,
( spl3_1
<=> real_one = a(sK1,sK2) ),
introduced(definition,[new_symbols(definition,[spl3_1])],[avatar_definition]) ).
fof(f66,plain,
( real_one != a(sK1,sK2)
| spl3_1 ),
inference(avatar_component_clause,[],[f65]) ).
fof(f68,definition,
( spl3_2
<=> sK1 = sK2 ),
introduced(definition,[new_symbols(definition,[spl3_2])],[avatar_definition]) ).
fof(f69,plain,
( sK1 != sK2
| spl3_2 ),
inference(avatar_component_clause,[],[f68]) ).
fof(f70,plain,
( ~ spl3_1
| ~ spl3_2 ),
inference(avatar_split_clause,[],[f56,f68,f65]) ).
fof(f71,plain,
( sK1 = sK2
| ~ spl3_2 ),
inference(avatar_component_clause,[],[f68]) ).
fof(f73,definition,
( spl3_3
<=> real_zero = a(sK1,sK2) ),
introduced(definition,[new_symbols(definition,[spl3_3])],[avatar_definition]) ).
fof(f74,plain,
( real_zero != a(sK1,sK2)
| spl3_3 ),
inference(avatar_component_clause,[],[f73]) ).
fof(f75,plain,
( spl3_2
| ~ spl3_3 ),
inference(avatar_split_clause,[],[f57,f73,f68]) ).
fof(f78,definition,
( spl3_4
<=> ! [X0] :
( ~ int_leq(int_one,X0)
| ~ int_leq(X0,n) ) ),
introduced(definition,[new_symbols(definition,[spl3_4])],[avatar_definition]) ).
fof(f79,plain,
( ! [X0] :
( ~ int_leq(int_one,X0)
| ~ int_leq(X0,n) )
| ~ spl3_4 ),
inference(avatar_component_clause,[],[f78]) ).
fof(f81,definition,
( spl3_5
<=> ! [X4,X1] :
( real_one = a(X4,X4)
| ~ int_leq(X1,n)
| ~ int_leq(int_one,X1)
| ~ int_leq(X4,X1)
| ~ int_leq(int_one,X4) ) ),
introduced(definition,[new_symbols(definition,[spl3_5])],[avatar_definition]) ).
fof(f82,plain,
( ! [X1,X4] :
( ~ int_leq(X1,n)
| ~ int_leq(int_one,X1)
| ~ int_leq(X4,X1)
| ~ int_leq(int_one,X4)
| real_one = a(X4,X4) )
| ~ spl3_5 ),
inference(avatar_component_clause,[],[f81]) ).
fof(f83,plain,
( spl3_4
| spl3_5 ),
inference(avatar_split_clause,[],[f49,f81,f78]) ).
fof(f84,plain,
( ~ int_leq(sK2,n)
| ~ spl3_4 ),
inference(resolution,[],[f79,f52]) ).
fof(f89,plain,
( $false
| ~ spl3_4 ),
inference(forward_subsumption_resolution,[],[f84,f51]) ).
fof(f90,plain,
~ spl3_4,
inference(avatar_contradiction_clause,[],[f89]) ).
fof(f95,plain,
! [X0] : plus(int_zero,X0) = X0,
inference(superposition,[],[f39,f40]) ).
fof(f109,plain,
! [X0,X1] :
( ~ int_less(X0,X1)
| ~ int_less(X1,X0) ),
inference(resolution,[],[f35,f60]) ).
fof(f116,plain,
! [X0,X1] :
( ~ int_leq(X0,X1)
| X0 = X1
| plus(X0,sK0(X0,X1)) = X1 ),
inference(resolution,[],[f43,f32]) ).
fof(f126,plain,
! [X2,X3,X0,X1] :
( int_leq(plus(X2,X3),plus(X0,X1))
| ~ int_less(X2,X1)
| ~ int_leq(X3,X0) ),
inference(superposition,[],[f41,f39]) ).
fof(f131,plain,
! [X0,X1] :
( ~ int_leq(X0,X1)
| X0 = X1
| ~ int_less(X1,X0) ),
inference(resolution,[],[f109,f32]) ).
fof(f139,plain,
( ! [X0] :
( ~ int_leq(sK1,n)
| ~ int_leq(X0,sK1)
| ~ int_leq(int_one,X0)
| real_one = a(X0,X0) )
| ~ spl3_5 ),
inference(resolution,[],[f82,f54]) ).
fof(f168,definition,
( spl3_7
<=> real_one = a(sK1,sK1) ),
introduced(definition,[new_symbols(definition,[spl3_7])],[avatar_definition]) ).
fof(f169,plain,
( real_one = a(sK1,sK1)
| ~ spl3_7 ),
inference(avatar_component_clause,[],[f168]) ).
fof(f188,plain,
( ! [X0] :
( ~ int_leq(X0,sK1)
| ~ int_leq(int_one,X0)
| real_one = a(X0,X0) )
| ~ spl3_5 ),
inference(forward_subsumption_resolution,[],[f139,f53]) ).
fof(f195,plain,
! [X0,X1] :
( ~ int_leq(int_one,X0)
| ~ int_leq(plus(X0,X1),n)
| ~ int_less(int_zero,X1)
| ~ int_leq(int_one,plus(X0,X1))
| real_zero = a(plus(X0,X1),X0)
| ~ int_leq(int_one,X0)
| ~ int_leq(X0,n) ),
inference(resolution,[],[f62,f59]) ).
fof(f208,plain,
! [X0,X1] :
( ~ int_leq(plus(X0,X1),n)
| ~ int_leq(int_one,X0)
| ~ int_less(int_zero,X1)
| ~ int_leq(int_one,plus(X0,X1))
| real_zero = a(plus(X0,X1),X0)
| ~ int_leq(X0,n) ),
inference(duplicate_literal_removal,[],[f195]) ).
fof(f234,plain,
! [X0,X1] :
( ~ int_leq(int_one,X0)
| ~ int_leq(plus(X0,X1),n)
| ~ int_less(int_zero,X1)
| ~ int_leq(int_one,X0)
| ~ int_leq(X0,n)
| ~ int_leq(int_one,plus(X0,X1))
| real_zero = a(X0,plus(X0,X1)) ),
inference(resolution,[],[f63,f59]) ).
fof(f247,plain,
! [X0,X1] :
( ~ int_leq(plus(X0,X1),n)
| ~ int_leq(int_one,X0)
| ~ int_less(int_zero,X1)
| ~ int_leq(X0,n)
| ~ int_leq(int_one,plus(X0,X1))
| real_zero = a(X0,plus(X0,X1)) ),
inference(duplicate_literal_removal,[],[f234]) ).
fof(f257,plain,
( ~ int_leq(sK1,sK1)
| real_one = a(sK1,sK1)
| ~ spl3_5 ),
inference(resolution,[],[f188,f54]) ).
fof(f402,plain,
! [X0,X1] :
( int_less(X1,X0)
| plus(X0,sK0(X0,X1)) = X1
| X0 = X1 ),
inference(resolution,[],[f116,f37]) ).
fof(f410,plain,
( n = sK1
| n = plus(sK1,sK0(sK1,n)) ),
inference(resolution,[],[f116,f53]) ).
fof(f411,plain,
( n = sK2
| n = plus(sK2,sK0(sK2,n)) ),
inference(resolution,[],[f116,f51]) ).
fof(f413,definition,
( spl3_16
<=> n = plus(sK2,sK0(sK2,n)) ),
introduced(definition,[new_symbols(definition,[spl3_16])],[avatar_definition]) ).
fof(f414,plain,
( n = plus(sK2,sK0(sK2,n))
| ~ spl3_16 ),
inference(avatar_component_clause,[],[f413]) ).
fof(f416,definition,
( spl3_17
<=> n = sK2 ),
introduced(definition,[new_symbols(definition,[spl3_17])],[avatar_definition]) ).
fof(f417,plain,
( n = sK2
| ~ spl3_17 ),
inference(avatar_component_clause,[],[f416]) ).
fof(f418,plain,
( spl3_16
| spl3_17 ),
inference(avatar_split_clause,[],[f411,f416,f413]) ).
fof(f420,definition,
( spl3_18
<=> n = plus(sK1,sK0(sK1,n)) ),
introduced(definition,[new_symbols(definition,[spl3_18])],[avatar_definition]) ).
fof(f421,plain,
( n = plus(sK1,sK0(sK1,n))
| ~ spl3_18 ),
inference(avatar_component_clause,[],[f420]) ).
fof(f423,definition,
( spl3_19
<=> n = sK1 ),
introduced(definition,[new_symbols(definition,[spl3_19])],[avatar_definition]) ).
fof(f424,plain,
( n = sK1
| ~ spl3_19 ),
inference(avatar_component_clause,[],[f423]) ).
fof(f425,plain,
( spl3_18
| spl3_19 ),
inference(avatar_split_clause,[],[f410,f423,f420]) ).
fof(f441,plain,
( int_leq(int_one,n)
| ~ spl3_19 ),
inference(superposition,[],[f54,f424]) ).
fof(f534,plain,
! [X2,X0,X1] :
( int_leq(X0,plus(X1,X2))
| ~ int_less(int_zero,X2)
| ~ int_leq(X0,X1) ),
inference(superposition,[],[f126,f95]) ).
fof(f548,plain,
( int_leq(int_one,n)
| ~ spl3_17 ),
inference(superposition,[],[f52,f417]) ).
fof(f1008,definition,
( spl3_45
<=> int_less(sK1,n) ),
introduced(definition,[new_symbols(definition,[spl3_45])],[avatar_definition]) ).
fof(f1009,plain,
( ~ int_less(sK1,n)
| spl3_45 ),
inference(avatar_component_clause,[],[f1008]) ).
fof(f1265,definition,
( spl3_54
<=> int_less(int_zero,sK0(sK1,n)) ),
introduced(definition,[new_symbols(definition,[spl3_54])],[avatar_definition]) ).
fof(f1266,plain,
( ~ int_less(int_zero,sK0(sK1,n))
| spl3_54 ),
inference(avatar_component_clause,[],[f1265]) ).
fof(f1267,plain,
( int_less(sK1,n)
| ~ spl3_45 ),
inference(avatar_component_clause,[],[f1008]) ).
fof(f1325,plain,
( ~ int_less(sK1,n)
| spl3_54 ),
inference(resolution,[],[f1266,f42]) ).
fof(f1331,plain,
( ~ spl3_45
| spl3_54 ),
inference(avatar_split_clause,[],[f1325,f1265,f1008]) ).
fof(f1337,plain,
( n = sK1
| ~ int_leq(sK1,n)
| spl3_45 ),
inference(resolution,[],[f1009,f32]) ).
fof(f1339,plain,
( n = sK1
| spl3_45 ),
inference(forward_subsumption_resolution,[],[f1337,f53]) ).
fof(f1340,plain,
( spl3_19
| spl3_45 ),
inference(avatar_split_clause,[],[f1339,f1008,f423]) ).
fof(f1363,plain,
( n != sK1
| spl3_2
| ~ spl3_17 ),
inference(forward_demodulation,[],[f69,f417]) ).
fof(f1364,plain,
( real_zero != a(sK1,n)
| spl3_3
| ~ spl3_17 ),
inference(forward_demodulation,[],[f74,f417]) ).
fof(f1664,plain,
! [X0,X1] :
( ~ int_leq(int_one,X0)
| ~ int_less(int_zero,X1)
| ~ int_leq(int_one,plus(X0,X1))
| real_zero = a(plus(X0,X1),X0)
| ~ int_leq(X0,n)
| ~ int_less(plus(X0,X1),n) ),
inference(resolution,[],[f208,f34]) ).
fof(f1681,plain,
( ~ int_leq(n,n)
| ~ int_leq(int_one,sK1)
| ~ int_less(int_zero,sK0(sK1,n))
| ~ int_leq(sK1,n)
| ~ int_leq(int_one,n)
| real_zero = a(sK1,n)
| ~ spl3_18 ),
inference(superposition,[],[f247,f421]) ).
fof(f1683,plain,
( ~ int_leq(int_one,sK1)
| ~ int_less(int_zero,sK0(sK1,n))
| ~ int_leq(sK1,n)
| ~ int_leq(int_one,n)
| real_zero = a(sK1,n)
| ~ spl3_18 ),
inference(forward_subsumption_resolution,[],[f1681,f59]) ).
fof(f1685,plain,
( ~ int_less(int_zero,sK0(sK1,n))
| ~ int_leq(sK1,n)
| ~ int_leq(int_one,n)
| real_zero = a(sK1,n)
| ~ spl3_18 ),
inference(forward_subsumption_resolution,[],[f1683,f54]) ).
fof(f1691,plain,
( ~ int_less(int_zero,sK0(sK1,n))
| ~ int_leq(int_one,n)
| real_zero = a(sK1,n)
| ~ spl3_18 ),
inference(forward_subsumption_resolution,[],[f1685,f53]) ).
fof(f1692,plain,
( ~ int_less(int_zero,sK0(sK1,n))
| real_zero = a(sK1,n)
| ~ spl3_17
| ~ spl3_18 ),
inference(forward_subsumption_resolution,[],[f1691,f548]) ).
fof(f1693,plain,
( ~ int_less(int_zero,sK0(sK1,n))
| spl3_3
| ~ spl3_17
| ~ spl3_18 ),
inference(forward_subsumption_resolution,[],[f1692,f1364]) ).
fof(f1694,plain,
( ~ spl3_54
| spl3_3
| ~ spl3_17
| ~ spl3_18 ),
inference(avatar_split_clause,[],[f1693,f420,f416,f73,f1265]) ).
fof(f1695,plain,
( $false
| spl3_2
| ~ spl3_17
| ~ spl3_19 ),
inference(forward_subsumption_resolution,[],[f424,f1363]) ).
fof(f1696,plain,
( spl3_2
| ~ spl3_17
| ~ spl3_19 ),
inference(avatar_contradiction_clause,[],[f1695]) ).
fof(f1759,plain,
( real_one != a(sK1,sK1)
| spl3_1
| ~ spl3_2 ),
inference(forward_demodulation,[],[f66,f71]) ).
fof(f1760,plain,
( $false
| spl3_1
| ~ spl3_2
| ~ spl3_7 ),
inference(forward_subsumption_resolution,[],[f1759,f169]) ).
fof(f1761,plain,
( spl3_1
| ~ spl3_2
| ~ spl3_7 ),
inference(avatar_contradiction_clause,[],[f1760]) ).
fof(f1762,plain,
( real_one = a(sK1,sK1)
| ~ spl3_5 ),
inference(forward_subsumption_resolution,[],[f257,f59]) ).
fof(f1794,plain,
( spl3_7
| ~ spl3_5 ),
inference(avatar_split_clause,[],[f1762,f81,f168]) ).
fof(f1800,definition,
( spl3_86
<=> int_leq(sK1,sK2) ),
introduced(definition,[new_symbols(definition,[spl3_86])],[avatar_definition]) ).
fof(f1801,plain,
( ~ int_leq(sK1,sK2)
| spl3_86 ),
inference(avatar_component_clause,[],[f1800]) ).
fof(f1804,definition,
( spl3_87
<=> int_less(sK1,sK2) ),
introduced(definition,[new_symbols(definition,[spl3_87])],[avatar_definition]) ).
fof(f1805,plain,
( ~ int_less(sK1,sK2)
| spl3_87 ),
inference(avatar_component_clause,[],[f1804]) ).
fof(f1828,plain,
( real_zero != a(n,sK2)
| spl3_3
| ~ spl3_19 ),
inference(forward_demodulation,[],[f74,f424]) ).
fof(f2398,plain,
( ~ int_leq(n,n)
| ~ int_leq(int_one,sK2)
| ~ int_less(int_zero,sK0(sK2,n))
| ~ int_leq(int_one,n)
| real_zero = a(n,sK2)
| ~ int_leq(sK2,n)
| ~ spl3_16 ),
inference(superposition,[],[f208,f414]) ).
fof(f2414,plain,
( ~ int_leq(int_one,sK2)
| ~ int_less(int_zero,sK0(sK2,n))
| ~ int_leq(int_one,n)
| real_zero = a(n,sK2)
| ~ int_leq(sK2,n)
| ~ spl3_16 ),
inference(forward_subsumption_resolution,[],[f2398,f59]) ).
fof(f2446,definition,
( spl3_106
<=> int_less(int_zero,sK0(sK2,n)) ),
introduced(definition,[new_symbols(definition,[spl3_106])],[avatar_definition]) ).
fof(f2447,plain,
( ~ int_less(int_zero,sK0(sK2,n))
| spl3_106 ),
inference(avatar_component_clause,[],[f2446]) ).
fof(f2449,definition,
( spl3_107
<=> int_less(sK2,n) ),
introduced(definition,[new_symbols(definition,[spl3_107])],[avatar_definition]) ).
fof(f2459,plain,
( ~ int_less(int_zero,sK0(sK2,n))
| ~ int_leq(int_one,n)
| real_zero = a(n,sK2)
| ~ int_leq(sK2,n)
| ~ spl3_16 ),
inference(forward_subsumption_resolution,[],[f2414,f52]) ).
fof(f2484,plain,
( ~ int_less(int_zero,sK0(sK2,n))
| real_zero = a(n,sK2)
| ~ int_leq(sK2,n)
| ~ spl3_16
| ~ spl3_19 ),
inference(forward_subsumption_resolution,[],[f2459,f441]) ).
fof(f2500,plain,
( ~ int_less(int_zero,sK0(sK2,n))
| ~ int_leq(sK2,n)
| spl3_3
| ~ spl3_16
| ~ spl3_19 ),
inference(forward_subsumption_resolution,[],[f2484,f1828]) ).
fof(f2527,plain,
( ~ int_less(int_zero,sK0(sK2,n))
| spl3_3
| ~ spl3_16
| ~ spl3_19 ),
inference(forward_subsumption_resolution,[],[f2500,f51]) ).
fof(f2546,plain,
( ~ spl3_106
| spl3_3
| ~ spl3_16
| ~ spl3_19 ),
inference(avatar_split_clause,[],[f2527,f423,f413,f73,f2446]) ).
fof(f2571,plain,
( ~ int_less(sK2,n)
| spl3_106 ),
inference(resolution,[],[f2447,f42]) ).
fof(f2700,plain,
( ~ int_less(sK2,n)
| spl3_107 ),
inference(avatar_component_clause,[],[f2449]) ).
fof(f2759,plain,
( ~ spl3_107
| spl3_106 ),
inference(avatar_split_clause,[],[f2571,f2446,f2449]) ).
fof(f2817,plain,
( n = sK2
| ~ int_leq(sK2,n)
| spl3_107 ),
inference(resolution,[],[f2700,f32]) ).
fof(f2818,plain,
( n = sK2
| spl3_107 ),
inference(forward_subsumption_resolution,[],[f2817,f51]) ).
fof(f2821,plain,
( spl3_17
| spl3_107 ),
inference(avatar_split_clause,[],[f2818,f2449,f416]) ).
fof(f7560,plain,
( int_less(sK2,sK1)
| spl3_86 ),
inference(resolution,[],[f1801,f37]) ).
fof(f7561,plain,
( ~ int_less(sK1,sK2)
| spl3_86 ),
inference(resolution,[],[f1801,f34]) ).
fof(f14061,plain,
( int_leq(sK1,sK2)
| ~ spl3_86 ),
inference(avatar_component_clause,[],[f1800]) ).
fof(f15011,plain,
( sK1 = sK2
| sK2 = plus(sK1,sK0(sK1,sK2))
| ~ spl3_86 ),
inference(resolution,[],[f14061,f116]) ).
fof(f15012,plain,
( sK1 = sK2
| ~ int_less(sK2,sK1)
| ~ spl3_86 ),
inference(resolution,[],[f14061,f131]) ).
fof(f15019,plain,
( ~ int_less(sK2,sK1)
| spl3_2
| ~ spl3_86 ),
inference(forward_subsumption_resolution,[],[f15012,f69]) ).
fof(f15020,plain,
( sK2 = plus(sK1,sK0(sK1,sK2))
| spl3_2
| ~ spl3_86 ),
inference(forward_subsumption_resolution,[],[f15011,f69]) ).
fof(f15202,plain,
( sK1 = sK2
| ~ int_leq(sK2,sK1)
| spl3_2
| ~ spl3_86 ),
inference(resolution,[],[f15019,f32]) ).
fof(f15216,plain,
( ~ int_leq(sK2,sK1)
| spl3_2
| ~ spl3_86 ),
inference(forward_subsumption_resolution,[],[f15202,f69]) ).
fof(f15250,plain,
( int_less(sK1,sK2)
| spl3_2
| ~ spl3_86 ),
inference(resolution,[],[f15216,f37]) ).
fof(f16670,plain,
( ~ int_leq(sK2,n)
| ~ int_leq(int_one,sK1)
| ~ int_less(int_zero,sK0(sK1,sK2))
| ~ int_leq(sK1,n)
| ~ int_leq(int_one,sK2)
| real_zero = a(sK1,sK2)
| spl3_2
| ~ spl3_86 ),
inference(superposition,[],[f247,f15020]) ).
fof(f16715,definition,
( spl3_505
<=> int_less(int_zero,sK0(sK1,sK2)) ),
introduced(definition,[new_symbols(definition,[spl3_505])],[avatar_definition]) ).
fof(f16716,plain,
( ~ int_less(int_zero,sK0(sK1,sK2))
| spl3_505 ),
inference(avatar_component_clause,[],[f16715]) ).
fof(f16735,plain,
( ~ int_leq(int_one,sK1)
| ~ int_less(int_zero,sK0(sK1,sK2))
| ~ int_leq(sK1,n)
| ~ int_leq(int_one,sK2)
| real_zero = a(sK1,sK2)
| spl3_2
| ~ spl3_86 ),
inference(forward_subsumption_resolution,[],[f16670,f51]) ).
fof(f16774,plain,
( ~ int_less(int_zero,sK0(sK1,sK2))
| ~ int_leq(sK1,n)
| ~ int_leq(int_one,sK2)
| real_zero = a(sK1,sK2)
| spl3_2
| ~ spl3_86 ),
inference(forward_subsumption_resolution,[],[f16735,f54]) ).
fof(f16803,plain,
( ~ int_less(int_zero,sK0(sK1,sK2))
| ~ int_leq(int_one,sK2)
| real_zero = a(sK1,sK2)
| spl3_2
| ~ spl3_86 ),
inference(forward_subsumption_resolution,[],[f16774,f53]) ).
fof(f16819,plain,
( ~ int_less(int_zero,sK0(sK1,sK2))
| real_zero = a(sK1,sK2)
| spl3_2
| ~ spl3_86 ),
inference(forward_subsumption_resolution,[],[f16803,f52]) ).
fof(f16844,plain,
( ~ int_less(int_zero,sK0(sK1,sK2))
| spl3_2
| spl3_3
| ~ spl3_86 ),
inference(forward_subsumption_resolution,[],[f16819,f74]) ).
fof(f16885,plain,
( ~ spl3_505
| spl3_2
| spl3_3
| ~ spl3_86 ),
inference(avatar_split_clause,[],[f16844,f1800,f73,f68,f16715]) ).
fof(f16922,plain,
( ~ int_less(sK1,sK2)
| spl3_505 ),
inference(resolution,[],[f16716,f42]) ).
fof(f16944,plain,
( $false
| spl3_2
| ~ spl3_86
| spl3_505 ),
inference(forward_subsumption_resolution,[],[f16922,f15250]) ).
fof(f16945,plain,
( spl3_2
| ~ spl3_86
| spl3_505 ),
inference(avatar_contradiction_clause,[],[f16944]) ).
fof(f16946,plain,
( ~ spl3_87
| spl3_86 ),
inference(avatar_split_clause,[],[f7561,f1800,f1804]) ).
fof(f16961,plain,
( sK1 = plus(sK2,sK0(sK2,sK1))
| sK1 = sK2
| spl3_87 ),
inference(resolution,[],[f1805,f402]) ).
fof(f16967,plain,
( sK1 = plus(sK2,sK0(sK2,sK1))
| spl3_2
| spl3_87 ),
inference(forward_subsumption_resolution,[],[f16961,f69]) ).
fof(f16974,plain,
! [X0,X1] :
( ~ int_less(plus(X0,X1),n)
| ~ int_less(int_zero,X1)
| real_zero = a(plus(X0,X1),X0)
| ~ int_leq(X0,n)
| ~ int_leq(int_one,X0) ),
inference(forward_subsumption_resolution,[],[f1664,f534]) ).
fof(f20401,plain,
( ~ int_less(sK1,n)
| ~ int_less(int_zero,sK0(sK2,sK1))
| real_zero = a(sK1,sK2)
| ~ int_leq(sK2,n)
| ~ int_leq(int_one,sK2)
| spl3_2
| spl3_87 ),
inference(superposition,[],[f16974,f16967]) ).
fof(f20418,plain,
( ~ int_less(int_zero,sK0(sK2,sK1))
| real_zero = a(sK1,sK2)
| ~ int_leq(sK2,n)
| ~ int_leq(int_one,sK2)
| spl3_2
| ~ spl3_45
| spl3_87 ),
inference(forward_subsumption_resolution,[],[f20401,f1267]) ).
fof(f20438,definition,
( spl3_555
<=> int_less(int_zero,sK0(sK2,sK1)) ),
introduced(definition,[new_symbols(definition,[spl3_555])],[avatar_definition]) ).
fof(f20439,plain,
( ~ int_less(int_zero,sK0(sK2,sK1))
| spl3_555 ),
inference(avatar_component_clause,[],[f20438]) ).
fof(f20503,plain,
( ~ int_less(int_zero,sK0(sK2,sK1))
| ~ int_leq(sK2,n)
| ~ int_leq(int_one,sK2)
| spl3_2
| spl3_3
| ~ spl3_45
| spl3_87 ),
inference(forward_subsumption_resolution,[],[f20418,f74]) ).
fof(f20563,plain,
( ~ int_less(int_zero,sK0(sK2,sK1))
| ~ int_leq(int_one,sK2)
| spl3_2
| spl3_3
| ~ spl3_45
| spl3_87 ),
inference(forward_subsumption_resolution,[],[f20503,f51]) ).
fof(f20602,plain,
( ~ int_less(int_zero,sK0(sK2,sK1))
| spl3_2
| spl3_3
| ~ spl3_45
| spl3_87 ),
inference(forward_subsumption_resolution,[],[f20563,f52]) ).
fof(f20636,plain,
( ~ spl3_555
| spl3_2
| spl3_3
| ~ spl3_45
| spl3_87 ),
inference(avatar_split_clause,[],[f20602,f1804,f1008,f73,f68,f20438]) ).
fof(f20784,plain,
( ~ int_less(sK2,sK1)
| spl3_555 ),
inference(resolution,[],[f20439,f42]) ).
fof(f20810,plain,
( $false
| spl3_86
| spl3_555 ),
inference(forward_subsumption_resolution,[],[f20784,f7560]) ).
fof(f20811,plain,
( spl3_86
| spl3_555 ),
inference(avatar_contradiction_clause,[],[f20810]) ).
cnf(s1,plain,
( ~ spl3_1
| ~ spl3_2 ),
inference(sat_conversion,[],[f70]) ).
cnf(s2,plain,
( spl3_2
| ~ spl3_3 ),
inference(sat_conversion,[],[f75]) ).
cnf(s4,plain,
( spl3_4
| spl3_5 ),
inference(sat_conversion,[],[f83]) ).
cnf(s6,plain,
~ spl3_4,
inference(sat_conversion,[],[f90]) ).
cnf(s19,plain,
( spl3_16
| spl3_17 ),
inference(sat_conversion,[],[f418]) ).
cnf(s20,plain,
( spl3_18
| spl3_19 ),
inference(sat_conversion,[],[f425]) ).
cnf(s78,plain,
( ~ spl3_45
| spl3_54 ),
inference(sat_conversion,[],[f1331]) ).
cnf(s79,plain,
( spl3_19
| spl3_45 ),
inference(sat_conversion,[],[f1340]) ).
cnf(s97,plain,
( spl3_3
| ~ spl3_17
| ~ spl3_18
| ~ spl3_54 ),
inference(sat_conversion,[],[f1694]) ).
cnf(s98,plain,
( spl3_2
| ~ spl3_17
| ~ spl3_19 ),
inference(sat_conversion,[],[f1696]) ).
cnf(s118,plain,
( spl3_1
| ~ spl3_2
| ~ spl3_7 ),
inference(sat_conversion,[],[f1761]) ).
cnf(s127,plain,
( ~ spl3_5
| spl3_7 ),
inference(sat_conversion,[],[f1794]) ).
cnf(s180,plain,
( spl3_3
| ~ spl3_16
| ~ spl3_19
| ~ spl3_106 ),
inference(sat_conversion,[],[f2546]) ).
cnf(s205,plain,
( spl3_106
| ~ spl3_107 ),
inference(sat_conversion,[],[f2759]) ).
cnf(s206,plain,
( spl3_17
| spl3_107 ),
inference(sat_conversion,[],[f2821]) ).
cnf(s1244,plain,
( spl3_2
| spl3_3
| ~ spl3_86
| ~ spl3_505 ),
inference(sat_conversion,[],[f16885]) ).
cnf(s1249,plain,
( spl3_2
| ~ spl3_86
| spl3_505 ),
inference(sat_conversion,[],[f16945]) ).
cnf(s1250,plain,
( spl3_86
| ~ spl3_87 ),
inference(sat_conversion,[],[f16946]) ).
cnf(s1359,plain,
( spl3_2
| spl3_3
| ~ spl3_45
| spl3_87
| ~ spl3_555 ),
inference(sat_conversion,[],[f20636]) ).
cnf(s1378,plain,
( spl3_86
| spl3_555 ),
inference(sat_conversion,[],[f20811]) ).
cnf(s1404,plain,
spl3_5,
inference(rat,[],[s4,s6]) ).
cnf(s1417,plain,
spl3_7,
inference(rat,[],[s127,s1404]) ).
cnf(s1469,plain,
( ~ spl3_17
| spl3_2 ),
inference(rat,[],[s97,s78,s20,s79,s98,s2]) ).
cnf(s1470,plain,
( spl3_86
| spl3_2 ),
inference(rat,[],[s1359,s1250,s1378,s79,s180,s205,s206,s2,s19,s1469]) ).
cnf(s1471,plain,
( ~ spl3_86
| spl3_3
| spl3_2 ),
inference(rat,[],[s1249,s1244]) ).
cnf(s1472,plain,
spl3_2,
inference(rat,[],[s1471,s1470,s2]) ).
cnf(s1473,plain,
spl3_1,
inference(rat,[],[s118,s1417,s1472]) ).
cnf(s1474,plain,
$false,
inference(rat,[],[s1,s1472,s1473]) ).
fof(f20812,plain,
$false,
inference(avatar_sat_refutation,[],[s1474]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV491+4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.19 % Computer : n004.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 11:14:37 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
% 16.84/2.68 % (289200)Will run a generic schedule for satisfiability detection.
% 16.84/2.68 % (289206)% WARNING: option uhcvi not known.
% 16.84/2.68 % (289206)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1045398993:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 16.84/2.68 % (289205)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3673294050_2999 on theBenchmark for (2999ds/0Mi)
% 16.84/2.68 % (289207)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=877687438:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 16.84/2.68 % (289208)dis+10_1_sil=32000:sp=arity:random_seed=4290312428:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 16.84/2.68 % (289209)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=553961136:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 16.84/2.68 % (289211)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3562357251:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 16.84/2.68 % (289210)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=332602670:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 16.84/2.68 % TRYING [1]
% 16.84/2.68 % TRYING [2]
% 16.84/2.68 % TRYING [3]
% 16.84/2.68 % TRYING [4]
% 16.84/2.68 % TRYING [5]
% 16.84/2.68 % TRYING [6]
% 16.84/2.68 % TRYING [7]
% 16.84/2.68 % (289208)Instruction limit reached!
% 16.84/2.68 % (289208)------------------------------
% 16.84/2.68 % (289208)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.84/2.68 % (289208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.84/2.68 % (289208)CaDiCaL version: 2.1.3
% 16.84/2.68 % (289208)Termination reason: Instruction limit
% 16.84/2.68 % (289208)Termination phase: Saturation
% 16.84/2.68 % (289208)Time elapsed: 0.066 s
% 16.84/2.68 % (289208)Peak memory usage: 12 MB
% 16.84/2.68 % (289208)Instructions burned: 104 (million)
% 16.84/2.68 % TRYING [8]
% 16.84/2.68 % (289209)Instruction limit reached!
% 16.84/2.68 % (289209)------------------------------
% 16.84/2.68 % (289209)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.84/2.68 % (289209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.84/2.68 % (289209)CaDiCaL version: 2.1.3
% 16.84/2.68 % (289209)Termination reason: Instruction limit
% 16.84/2.68 % (289209)Termination phase: Saturation
% 16.84/2.68 % (289209)Time elapsed: 0.073 s
% 16.84/2.68 % (289209)Peak memory usage: 12 MB
% 16.84/2.68 % (289209)Instructions burned: 117 (million)
% 16.84/2.68 % (289210)Instruction limit reached!
% 16.84/2.68 % (289210)------------------------------
% 16.84/2.68 % (289210)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.84/2.68 % (289210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.84/2.68 % (289210)CaDiCaL version: 2.1.3
% 16.84/2.68 % (289210)Termination reason: Instruction limit
% 16.84/2.68 % (289210)Termination phase: Saturation
% 16.84/2.68 % (289210)Time elapsed: 0.081 s
% 16.84/2.68 % (289210)Peak memory usage: 13 MB
% 16.84/2.68 % (289210)Instructions burned: 132 (million)
% 16.84/2.68 % (289219)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2619971878:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 16.84/2.68 % TRYING [1]
% 16.84/2.68 % TRYING [2]
% 16.84/2.68 % TRYING [3]
% 16.84/2.68 % TRYING [4]
% 16.84/2.68 % (289220)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=867128584:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 16.84/2.68 % TRYING [5]
% 16.84/2.68 % (289211)Instruction limit reached!
% 16.84/2.68 % (289211)------------------------------
% 16.84/2.68 % (289211)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.84/2.68 % (289211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.84/2.68 % (289211)CaDiCaL version: 2.1.3
% 16.84/2.68 % (289211)Termination reason: Instruction limit
% 16.84/2.68 % (289211)Termination phase: Saturation
% 16.84/2.68 % (289211)Time elapsed: 0.101 s
% 16.84/2.68 % (289211)Peak memory usage: 14 MB
% 16.84/2.68 % (289211)Instructions burned: 159 (million)
% 16.84/2.68 % (289221)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=1203986223:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 16.84/2.68 % TRYING [6]
% 16.84/2.68 % (289225)ott-21_1_sil=16000:fs=off:random_seed=3189879207:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 16.84/2.68 % TRYING [7]
% 16.84/2.68 % TRYING [9]
% 16.84/2.68 % TRYING [8]
% 16.84/2.68 % (289220)Instruction limit reached!
% 16.84/2.68 % (289220)------------------------------
% 16.84/2.68 % (289220)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.77/7.94 % (289220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.77/7.94 % (289220)CaDiCaL version: 2.1.3
% 53.77/7.94 % (289220)Termination reason: Instruction limit
% 53.77/7.94 % (289220)Termination phase: Saturation
% 53.77/7.94 % (289220)Time elapsed: 0.091 s
% 53.77/7.94 % (289220)Peak memory usage: 13 MB
% 53.77/7.94 % (289220)Instructions burned: 131 (million)
% 53.77/7.94 % (289227)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1739529421:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 53.77/7.94 % (289225)Instruction limit reached!
% 53.77/7.94 % (289225)------------------------------
% 53.77/7.94 % (289225)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.77/7.94 % (289225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.77/7.94 % (289225)CaDiCaL version: 2.1.3
% 53.77/7.94 % (289225)Termination reason: Instruction limit
% 53.77/7.94 % (289225)Termination phase: Saturation
% 53.77/7.94 % (289225)Time elapsed: 0.088 s
% 53.77/7.94 % (289225)Peak memory usage: 12 MB
% 53.77/7.94 % (289225)Instructions burned: 182 (million)
% 53.77/7.94 % (289229)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2364267826:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 53.77/7.94 % TRYING [1]
% 53.77/7.94 % TRYING [2]
% 53.77/7.94 % TRYING [3]
% 53.77/7.94 % TRYING [4]
% 53.77/7.94 % TRYING [5]
% 53.77/7.94 % TRYING [6]
% 53.77/7.94 % TRYING [7]
% 53.77/7.94 % TRYING [10]
% 53.77/7.94 % TRYING [9]
% 53.77/7.94 % TRYING [8]
% 53.77/7.94 % (289219)Instruction limit reached!
% 53.77/7.94 % (289219)------------------------------
% 53.77/7.94 % (289219)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.77/7.94 % (289219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.77/7.94 % (289219)CaDiCaL version: 2.1.3
% 53.77/7.94 % (289219)Termination reason: Instruction limit
% 53.77/7.94 % (289219)Termination phase: Finite model building SAT solving
% 53.77/7.94 % (289219)Time elapsed: 0.364 s
% 53.77/7.94 % (289219)Peak memory usage: 21 MB
% 53.77/7.94 % (289219)Instructions burned: 714 (million)
% 53.77/7.94 % TRYING [9]
% 53.77/7.94 % (289231)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3715743597:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 53.77/7.94 % (289221)Instruction limit reached!
% 53.77/7.94 % (289221)------------------------------
% 53.77/7.94 % (289221)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.77/7.94 % (289221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.77/7.94 % (289221)CaDiCaL version: 2.1.3
% 53.77/7.94 % (289221)Termination reason: Instruction limit
% 53.77/7.94 % (289221)Termination phase: Saturation
% 53.77/7.94 % (289221)Time elapsed: 0.400 s
% 53.77/7.94 % (289221)Peak memory usage: 17 MB
% 53.77/7.94 % (289221)Instructions burned: 685 (million)
% 53.77/7.94 % (289227)Instruction limit reached!
% 53.77/7.94 % (289227)------------------------------
% 53.77/7.94 % (289227)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.77/7.94 % (289227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.77/7.94 % (289227)CaDiCaL version: 2.1.3
% 53.77/7.94 % (289227)Termination reason: Instruction limit
% 53.77/7.94 % (289227)Termination phase: Saturation
% 53.77/7.94 % (289227)Time elapsed: 0.311 s
% 53.77/7.94 % (289227)Peak memory usage: 14 MB
% 53.77/7.94 % (289227)Instructions burned: 477 (million)
% 53.77/7.94 % (289233)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=597096905:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 53.77/7.94 % TRYING [14]
% 53.77/7.94 % (289234)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=325981965: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)
% 53.77/7.94 % (289229)Instruction limit reached!
% 53.77/7.94 % (289229)------------------------------
% 53.77/7.94 % (289229)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.77/7.94 % (289229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.77/7.94 % (289229)CaDiCaL version: 2.1.3
% 53.77/7.94 % (289229)Termination reason: Instruction limit
% 53.77/7.94 % (289229)Termination phase: Finite model building SAT solving
% 53.77/7.94 % (289229)Time elapsed: 0.336 s
% 53.77/7.94 % (289229)Peak memory usage: 18 MB
% 53.77/7.94 % (289229)Instructions burned: 865 (million)
% 53.77/7.94 % (289237)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1789031899:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 53.77/7.94 % TRYING [11]
% 53.77/7.94 % (289233)Instruction limit reached!
% 53.77/7.94 % (289233)------------------------------
% 53.77/7.94 % (289233)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.77/7.94 % (289233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.77/7.94 % (289233)CaDiCaL version: 2.1.3
% 53.77/7.94 % (289233)Termination reason: Instruction limit
% 53.77/7.94 % (289233)Termination phase: Finite model building SAT solving
% 53.77/7.94 % (289233)Time elapsed: 0.338 s
% 53.77/7.94 % (289233)Peak memory usage: 44 MB
% 53.77/7.94 % (289233)Instructions burned: 892 (million)
% 53.77/7.94 % (289239)fmb+10_1_sil=64000:random_seed=2647519586:i=22061:nm=2:gsp=on_2991 on theBenchmark for (2991ds/22061Mi)
% 53.77/7.94 % TRYING [1]
% 53.77/7.94 % TRYING [2]
% 53.77/7.94 % TRYING [3]
% 53.77/7.94 % TRYING [4]
% 53.77/7.94 % TRYING [5]
% 53.77/7.94 % TRYING [6]
% 53.77/7.94 % (289234)Instruction limit reached!
% 53.77/7.94 % (289234)------------------------------
% 53.77/7.94 % (289234)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.77/7.94 % (289234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.77/7.94 % (289234)CaDiCaL version: 2.1.3
% 53.77/7.94 % (289234)Termination reason: Instruction limit
% 53.77/7.94 % (289234)Termination phase: Saturation
% 53.77/7.94 % (289234)Time elapsed: 0.398 s
% 53.77/7.94 % (289234)Peak memory usage: 16 MB
% 53.77/7.94 % (289234)Instructions burned: 692 (million)
% 53.77/7.94 % TRYING [7]
% 53.77/7.94 % (289241)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2073299645:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 53.77/7.94 % TRYING [20]
% 53.77/7.94 % TRYING [8]
% 53.77/7.94 % (289237)Instruction limit reached!
% 53.77/7.94 % (289237)------------------------------
% 53.77/7.94 % (289237)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.77/7.94 % (289237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.77/7.94 % (289237)CaDiCaL version: 2.1.3
% 53.77/7.94 % (289237)Termination reason: Instruction limit
% 53.77/7.94 % (289237)Termination phase: Saturation
% 53.77/7.94 % (289237)Time elapsed: 0.500 s
% 53.77/7.94 % (289237)Peak memory usage: 17 MB
% 53.77/7.94 % (289237)Instructions burned: 879 (million)
% 53.77/7.94 % TRYING [12]
% 53.77/7.94 % TRYING [9]
% 53.77/7.94 % (289243)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1788586356:fmbsr=1.7:i=920_2988 on theBenchmark for (2988ds/920Mi)
% 53.77/7.94 % TRYING [8]
% 53.77/7.94 % (289231)Instruction limit reached!
% 53.77/7.94 % (289231)------------------------------
% 53.77/7.94 % (289231)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.77/7.94 % (289231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.77/7.94 % (289231)CaDiCaL version: 2.1.3
% 53.77/7.94 % (289231)Termination reason: Instruction limit
% 53.77/7.94 % (289231)Termination phase: Saturation
% 53.77/7.94 % (289231)Time elapsed: 0.714 s
% 53.77/7.94 % (289231)Peak memory usage: 19 MB
% 53.77/7.94 % (289231)Instructions burned: 1179 (million)
% 53.77/7.94 % TRYING [9]
% 53.77/7.94 % (289245)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3308475164:i=5131_2987 on theBenchmark for (2987ds/5131Mi)
% 53.77/7.94 % TRYING [10]
% 53.77/7.94 % TRYING [10]
% 53.77/7.94 % TRYING [11]
% 53.77/7.94 % (289243)Instruction limit reached!
% 53.77/7.94 % (289243)------------------------------
% 53.77/7.94 % (289243)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.77/7.94 % (289243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.77/7.94 % (289243)CaDiCaL version: 2.1.3
% 53.77/7.94 % (289243)Termination reason: Instruction limit
% 53.77/7.94 % (289243)Termination phase: Finite model building SAT solving
% 53.77/7.94 % (289243)Time elapsed: 0.466 s
% 53.77/7.94 % (289243)Peak memory usage: 25 MB
% 53.77/7.94 % (289243)Instructions burned: 921 (million)
% 53.77/7.94 % (289247)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2445741029:i=1472:ins=7:fdi=8:gsp=on_2983 on theBenchmark for (2983ds/1472Mi)
% 53.77/7.94 % TRYING [12]
% 53.77/7.94 % TRYING [13]
% 53.77/7.94 % (289247)Instruction limit reached!
% 53.77/7.94 % (289247)------------------------------
% 53.77/7.94 % (289247)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.77/7.94 % (289247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.77/7.94 % (289247)CaDiCaL version: 2.1.3
% 53.77/7.94 % (289247)Termination reason: Instruction limit
% 53.77/7.94 % (289247)Termination phase: Saturation
% 53.77/7.94 % (289247)Time elapsed: 0.804 s
% 53.77/7.94 % (289247)Peak memory usage: 32 MB
% 53.77/7.94 % (289247)Instructions burned: 1473 (million)
% 53.77/7.94 % (289249)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=510840475:i=6324_2975 on theBenchmark for (2975ds/6324Mi)
% 53.77/7.94 % TRYING [77]
% 53.77/7.94 % TRYING [13]
% 53.77/7.94 % TRYING [14]
% 53.77/7.94 % TRYING [14]
% 53.77/7.94 % (289245)Instruction limit reached!
% 53.77/7.94 % (289245)------------------------------
% 53.77/7.94 % (289245)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.77/7.94 % (289245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.77/7.94 % (289245)CaDiCaL version: 2.1.3
% 53.77/7.94 % (289245)Termination reason: Instruction limit
% 53.77/7.94 % (289245)Termination phase: Saturation
% 53.77/7.94 % (289245)Time elapsed: 2.860 s
% 53.77/7.94 % (289245)Peak memory usage: 21 MB
% 53.77/7.94 % (289245)Instructions burned: 5132 (million)
% 53.77/7.94 % (289251)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1290245263:fmbsr=2.30978:i=2174_2958 on theBenchmark for (2958ds/2174Mi)
% 53.77/7.94 % TRYING [16]
% 53.77/7.94 % (289249)Instruction limit reached!
% 53.77/7.94 % (289249)------------------------------
% 53.77/7.94 % (289249)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.77/7.94 % (289249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.77/7.94 % (289249)CaDiCaL version: 2.1.3
% 53.77/7.94 % (289249)Termination reason: Instruction limit
% 53.77/7.94 % (289249)Termination phase: Finite model building constraint generation
% 53.77/7.94 % (289249)Time elapsed: 2.225 s
% 53.77/7.94 % (289249)Peak memory usage: 453 MB
% 53.77/7.94 % (289249)Instructions burned: 6325 (million)
% 53.77/7.94 % (289253)ott-2_1_sil=16000:newcnf=on:random_seed=1694907426:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2952 on theBenchmark for (2952ds/869Mi)
% 53.77/7.94 % (289251)Instruction limit reached!
% 53.77/7.94 % (289251)------------------------------
% 53.77/7.94 % (289251)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.77/7.94 % (289251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.77/7.94 % (289251)CaDiCaL version: 2.1.3
% 53.77/7.94 % (289251)Termination reason: Instruction limit
% 53.77/7.94 % (289251)Termination phase: Finite model building constraint generation
% 53.77/7.94 % (289251)Time elapsed: 0.851 s
% 53.77/7.94 % (289251)Peak memory usage: 150 MB
% 53.77/7.94 % (289251)Instructions burned: 2177 (million)
% 53.77/7.94 % (289255)ott+10_1_sil=32000:tgt=ground:random_seed=1330679700:i=5114:av=off_2950 on theBenchmark for (2950ds/5114Mi)
% 53.77/7.94 % (289253)Instruction limit reached!
% 53.77/7.94 % (289253)------------------------------
% 53.77/7.94 % (289253)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.77/7.94 % (289253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.77/7.94 % (289253)CaDiCaL version: 2.1.3
% 53.77/7.94 % (289253)Termination reason: Instruction limit
% 53.77/7.94 % (289253)Termination phase: Saturation
% 53.77/7.94 % (289253)Time elapsed: 0.506 s
% 53.77/7.94 % (289253)Peak memory usage: 14 MB
% 53.77/7.94 % (289253)Instructions burned: 869 (million)
% 53.77/7.94 % (289257)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=550974223:i=54282_2947 on theBenchmark for (2947ds/54282Mi)
% 53.77/7.94 % TRYING [1]
% 53.77/7.94 % TRYING [2]
% 53.77/7.94 % TRYING [3]
% 53.77/7.94 % TRYING [4]
% 53.77/7.94 % TRYING [5]
% 53.77/7.94 % TRYING [6]
% 53.77/7.94 % TRYING [7]
% 53.77/7.94 % TRYING [8]
% 53.77/7.94 % TRYING [9]
% 53.77/7.94 % TRYING [10]
% 53.77/7.94 % TRYING [11]
% 53.77/7.94 % TRYING [15]
% 53.77/7.94 % TRYING [15]
% 53.77/7.94 % TRYING [12]
% 53.77/7.94 % (289241)Instruction limit reached!
% 53.77/7.94 % (289241)------------------------------
% 53.77/7.94 % (289241)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.77/7.94 % (289241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.77/7.94 % (289241)CaDiCaL version: 2.1.3
% 53.77/7.94 % (289241)Termination reason: Instruction limit
% 53.77/7.94 % (289241)Termination phase: Finite model building SAT solving
% 53.77/7.94 % (289241)Time elapsed: 5.957 s
% 53.77/7.94 % (289241)Peak memory usage: 246 MB
% 53.77/7.94 % (289241)Instructions burned: 9516 (million)
% 53.77/7.94 % (289259)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2685154486:i=3512:aac=none_2930 on theBenchmark for (2930ds/3512Mi)
% 53.77/7.94 % TRYING [13]
% 53.77/7.94 % (289259) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-289200-289259"...
% 53.77/7.94 % (289259)...printing done.
% 53.77/7.94 % (289259)Refutation found. Thanks to Tanya!
% 53.77/7.94 % SZS status Theorem for theBenchmark
% 53.77/7.94 % SZS output start Proof for theBenchmark
% See solution above
% 53.77/7.94 % (289259)------------------------------
% 53.77/7.94 % (289259)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.77/7.94 % (289259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.77/7.94 % (289259)CaDiCaL version: 2.1.3
% 53.77/7.94 % (289259)Termination reason: Refutation
% 53.77/7.94 % (289259)Time elapsed: 0.702 s
% 53.77/7.94 % (289259)Peak memory usage: 18 MB
% 53.77/7.94 % (289259)Instructions burned: 1257 (million)
% 53.77/7.94 % (289200)Success in time 7.711 s
% 53.77/7.94 % Vampire exiting
%------------------------------------------------------------------------------