%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ALG225+4 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:19:27 AM UTC 2026
% Result : Theorem 21.33s 6.50s
% Output : Refutation 24.51s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 26
% Syntax : Number of formulae : 157 ( 31 unt; 12 def)
% Number of atoms : 465 ( 86 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 531 ( 223 ~; 221 |; 46 &)
% ( 24 <=>; 17 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 22 ( 20 usr; 13 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 4 con; 0-3 aty)
% Number of variables : 159 ( 0 sgn 146 !; 13 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f8,axiom,
! [X0,X1] :
( r1_tarski(X0,X1)
<=> ! [X2] :
( r2_hidden(X2,X0)
=> r2_hidden(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d3_tarski) ).
fof(f675,axiom,
! [X0,X1] :
( r2_hidden(X0,X1)
=> m1_subset_1(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t1_subset) ).
fof(f685,axiom,
( v1_xboole_0(k1_xboole_0)
& v1_relat_1(k1_xboole_0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc4_relat_1) ).
fof(f804,axiom,
! [X0,X1] :
( v1_relat_1(X1)
=> ( r1_tarski(k1_relat_1(X1),X0)
=> k7_relat_1(X1,X0) = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t97_relat_1) ).
fof(f5328,axiom,
np__0 = k1_xboole_0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t51_card_1) ).
fof(f8084,axiom,
! [X0,X1] :
( ( v1_relat_1(X1)
& v1_funct_1(X1) )
=> ( m1_pboole(X1,X0)
<=> k1_relat_1(X1) = X0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d3_pboole) ).
fof(f8088,axiom,
! [X0] : k1_pboole(X0) = k2_funcop_1(X0,k1_xboole_0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d6_pboole) ).
fof(f8235,axiom,
! [X0,X1] :
( m1_pboole(X1,X0)
=> ( v2_relat_1(X1)
<=> ! [X2] :
~ ( r2_hidden(X2,X0)
& v1_xboole_0(k1_funct_1(X1,X2)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d16_pboole) ).
fof(f8263,axiom,
! [X0,X1] :
( m1_pboole(X1,X0)
=> ( v1_relat_1(X1)
& v1_funct_1(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m1_pboole) ).
fof(f8282,axiom,
! [X0] : m1_pboole(k1_pboole(X0),X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k1_pboole) ).
fof(f42783,axiom,
! [X0,X1,X2] :
( ( ~ v1_xboole_0(X1)
& m1_pboole(X2,X1) )
=> ( r2_hidden(X0,a_2_0_closure3(X1,X2))
<=> ? [X3] :
( m1_subset_1(X3,X1)
& X0 = X3
& k1_funct_1(X2,X3) != k1_xboole_0 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fraenkel_a_2_0_closure3) ).
fof(f42802,axiom,
! [X0] :
( ~ v1_xboole_0(X0)
=> ! [X1] :
( m1_pboole(X1,X0)
=> ! [X2] :
( m1_pboole(X2,X0)
=> k1_funct_4(X1,X2) = X2 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t1_closure3) ).
fof(f42809,axiom,
! [X0] :
( ~ v1_xboole_0(X0)
=> ! [X1] :
( m1_pboole(X1,X0)
=> ! [X2] :
( X2 = k1_closure3(X0,X1)
<=> X2 = a_2_0_closure3(X0,X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d3_closure3) ).
fof(f42810,conjecture,
! [X0] :
( ~ v1_xboole_0(X0)
=> ! [X1] :
( ( v2_relat_1(X1)
& m1_pboole(X1,X0) )
=> X1 = k1_funct_4(k1_pboole(X0),k7_relat_1(X1,k1_closure3(X0,X1))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t6_closure3) ).
fof(f42811,negated_conjecture,
~ ! [X0] :
( ~ v1_xboole_0(X0)
=> ! [X1] :
( ( v2_relat_1(X1)
& m1_pboole(X1,X0) )
=> X1 = k1_funct_4(k1_pboole(X0),k7_relat_1(X1,k1_closure3(X0,X1))) ) ),
inference(negated_conjecture,[status(cth)],[f42810]) ).
fof(f42845,plain,
! [X0,X1,X2] :
( ( r2_hidden(X0,a_2_0_closure3(X1,X2))
<=> ? [X3] :
( m1_subset_1(X3,X1)
& X0 = X3
& k1_funct_1(X2,X3) != k1_xboole_0 ) )
| v1_xboole_0(X1)
| ~ m1_pboole(X2,X1) ),
inference(ennf_transformation,[],[f42783]) ).
fof(f42846,plain,
! [X0,X1,X2] :
( ( r2_hidden(X0,a_2_0_closure3(X1,X2))
<=> ? [X3] :
( m1_subset_1(X3,X1)
& X0 = X3
& k1_funct_1(X2,X3) != k1_xboole_0 ) )
| v1_xboole_0(X1)
| ~ m1_pboole(X2,X1) ),
inference(flattening,[],[f42845]) ).
fof(f42879,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( k1_funct_4(X1,X2) = X2
| ~ m1_pboole(X2,X0) )
| ~ m1_pboole(X1,X0) )
| v1_xboole_0(X0) ),
inference(ennf_transformation,[],[f42802]) ).
fof(f42888,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( X2 = k1_closure3(X0,X1)
<=> X2 = a_2_0_closure3(X0,X1) )
| ~ m1_pboole(X1,X0) )
| v1_xboole_0(X0) ),
inference(ennf_transformation,[],[f42809]) ).
fof(f42889,plain,
? [X0] :
( ? [X1] :
( k1_funct_4(k1_pboole(X0),k7_relat_1(X1,k1_closure3(X0,X1))) != X1
& v2_relat_1(X1)
& m1_pboole(X1,X0) )
& ~ v1_xboole_0(X0) ),
inference(ennf_transformation,[],[f42811]) ).
fof(f42890,plain,
? [X0] :
( ? [X1] :
( k1_funct_4(k1_pboole(X0),k7_relat_1(X1,k1_closure3(X0,X1))) != X1
& v2_relat_1(X1)
& m1_pboole(X1,X0) )
& ~ v1_xboole_0(X0) ),
inference(flattening,[],[f42889]) ).
fof(f42897,plain,
! [X0,X1] :
( m1_subset_1(X0,X1)
| ~ r2_hidden(X0,X1) ),
inference(ennf_transformation,[],[f675]) ).
fof(f42942,plain,
! [X0,X1] :
( ( v1_relat_1(X1)
& v1_funct_1(X1) )
| ~ m1_pboole(X1,X0) ),
inference(ennf_transformation,[],[f8263]) ).
fof(f42946,plain,
! [X0,X1] :
( ( m1_pboole(X1,X0)
<=> k1_relat_1(X1) = X0 )
| ~ v1_relat_1(X1)
| ~ v1_funct_1(X1) ),
inference(ennf_transformation,[],[f8084]) ).
fof(f42947,plain,
! [X0,X1] :
( ( m1_pboole(X1,X0)
<=> k1_relat_1(X1) = X0 )
| ~ v1_relat_1(X1)
| ~ v1_funct_1(X1) ),
inference(flattening,[],[f42946]) ).
fof(f42965,plain,
! [X0,X1] :
( ( v2_relat_1(X1)
<=> ! [X2] :
( ~ r2_hidden(X2,X0)
| ~ v1_xboole_0(k1_funct_1(X1,X2)) ) )
| ~ m1_pboole(X1,X0) ),
inference(ennf_transformation,[],[f8235]) ).
fof(f43314,plain,
! [X0,X1] :
( r1_tarski(X0,X1)
<=> ! [X2] :
( r2_hidden(X2,X1)
| ~ r2_hidden(X2,X0) ) ),
inference(ennf_transformation,[],[f8]) ).
fof(f43413,plain,
! [X0,X1] :
( k7_relat_1(X1,X0) = X1
| ~ r1_tarski(k1_relat_1(X1),X0)
| ~ v1_relat_1(X1) ),
inference(ennf_transformation,[],[f804]) ).
fof(f43414,plain,
! [X0,X1] :
( k7_relat_1(X1,X0) = X1
| ~ r1_tarski(k1_relat_1(X1),X0)
| ~ v1_relat_1(X1) ),
inference(flattening,[],[f43413]) ).
fof(f43455,plain,
! [X0,X1,X2] :
( ( ( r2_hidden(X0,a_2_0_closure3(X1,X2))
| ! [X3] :
( ~ m1_subset_1(X3,X1)
| X0 != X3
| k1_xboole_0 = k1_funct_1(X2,X3) ) )
& ( ? [X3] :
( m1_subset_1(X3,X1)
& X0 = X3
& k1_funct_1(X2,X3) != k1_xboole_0 )
| ~ r2_hidden(X0,a_2_0_closure3(X1,X2)) ) )
| v1_xboole_0(X1)
| ~ m1_pboole(X2,X1) ),
inference(nnf_transformation,[],[f42846]) ).
fof(f43456,plain,
! [X0,X1,X2] :
( ( ( r2_hidden(X0,a_2_0_closure3(X1,X2))
| ! [X3] :
( ~ m1_subset_1(X3,X1)
| X0 != X3
| k1_xboole_0 = k1_funct_1(X2,X3) ) )
& ( ? [X4] :
( m1_subset_1(X4,X1)
& X0 = X4
& k1_xboole_0 != k1_funct_1(X2,X4) )
| ~ r2_hidden(X0,a_2_0_closure3(X1,X2)) ) )
| v1_xboole_0(X1)
| ~ m1_pboole(X2,X1) ),
inference(rectify,[],[f43455]) ).
fof(f43457,plain,
! [X0,X1,X2] :
( ( ( r2_hidden(X0,a_2_0_closure3(X1,X2))
| ! [X3] :
( ~ m1_subset_1(X3,X1)
| X0 != X3
| k1_xboole_0 = k1_funct_1(X2,X3) ) )
& ( ( m1_subset_1(sK0(X0,X1,X2),X1)
& sK0(X0,X1,X2) = X0
& k1_xboole_0 != k1_funct_1(X2,sK0(X0,X1,X2)) )
| ~ r2_hidden(X0,a_2_0_closure3(X1,X2)) ) )
| v1_xboole_0(X1)
| ~ m1_pboole(X2,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X4,sK0(X0,X1,X2))],[f43456]) ).
fof(f43469,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( X2 = k1_closure3(X0,X1)
| a_2_0_closure3(X0,X1) != X2 )
& ( X2 = a_2_0_closure3(X0,X1)
| k1_closure3(X0,X1) != X2 ) )
| ~ m1_pboole(X1,X0) )
| v1_xboole_0(X0) ),
inference(nnf_transformation,[],[f42888]) ).
fof(f43470,plain,
( sK8 != k1_funct_4(k1_pboole(sK7),k7_relat_1(sK8,k1_closure3(sK7,sK8)))
& v2_relat_1(sK8)
& m1_pboole(sK8,sK7)
& ~ v1_xboole_0(sK7) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7,sK8]),skolemize(X0,sK7),skolemize(X1,sK8)],[f42890]) ).
fof(f43490,plain,
! [X0,X1] :
( ( ( m1_pboole(X1,X0)
| k1_relat_1(X1) != X0 )
& ( k1_relat_1(X1) = X0
| ~ m1_pboole(X1,X0) ) )
| ~ v1_relat_1(X1)
| ~ v1_funct_1(X1) ),
inference(nnf_transformation,[],[f42947]) ).
fof(f43499,plain,
! [X0,X1] :
( ( ( v2_relat_1(X1)
| ? [X2] :
( r2_hidden(X2,X0)
& v1_xboole_0(k1_funct_1(X1,X2)) ) )
& ( ! [X2] :
( ~ r2_hidden(X2,X0)
| ~ v1_xboole_0(k1_funct_1(X1,X2)) )
| ~ v2_relat_1(X1) ) )
| ~ m1_pboole(X1,X0) ),
inference(nnf_transformation,[],[f42965]) ).
fof(f43500,plain,
! [X0,X1] :
( ( ( v2_relat_1(X1)
| ? [X2] :
( r2_hidden(X2,X0)
& v1_xboole_0(k1_funct_1(X1,X2)) ) )
& ( ! [X3] :
( ~ r2_hidden(X3,X0)
| ~ v1_xboole_0(k1_funct_1(X1,X3)) )
| ~ v2_relat_1(X1) ) )
| ~ m1_pboole(X1,X0) ),
inference(rectify,[],[f43499]) ).
fof(f43501,plain,
! [X0,X1] :
( ( ( v2_relat_1(X1)
| ( r2_hidden(sK24(X0,X1),X0)
& v1_xboole_0(k1_funct_1(X1,sK24(X0,X1))) ) )
& ( ! [X3] :
( ~ r2_hidden(X3,X0)
| ~ v1_xboole_0(k1_funct_1(X1,X3)) )
| ~ v2_relat_1(X1) ) )
| ~ m1_pboole(X1,X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK24]),skolemize(X2,sK24(X0,X1))],[f43500]) ).
fof(f43604,plain,
! [X0,X1] :
( ( r1_tarski(X0,X1)
| ? [X2] :
( ~ r2_hidden(X2,X1)
& r2_hidden(X2,X0) ) )
& ( ! [X2] :
( r2_hidden(X2,X1)
| ~ r2_hidden(X2,X0) )
| ~ r1_tarski(X0,X1) ) ),
inference(nnf_transformation,[],[f43314]) ).
fof(f43605,plain,
! [X0,X1] :
( ( r1_tarski(X0,X1)
| ? [X2] :
( ~ r2_hidden(X2,X1)
& r2_hidden(X2,X0) ) )
& ( ! [X3] :
( r2_hidden(X3,X1)
| ~ r2_hidden(X3,X0) )
| ~ r1_tarski(X0,X1) ) ),
inference(rectify,[],[f43604]) ).
fof(f43606,plain,
! [X0,X1] :
( ( r1_tarski(X0,X1)
| ( ~ r2_hidden(sK85(X0,X1),X1)
& r2_hidden(sK85(X0,X1),X0) ) )
& ( ! [X3] :
( r2_hidden(X3,X1)
| ~ r2_hidden(X3,X0) )
| ~ r1_tarski(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK85]),skolemize(X2,sK85(X0,X1))],[f43605]) ).
fof(f43633,plain,
! [X2,X3,X0,X1] :
( r2_hidden(X0,a_2_0_closure3(X1,X2))
| ~ m1_subset_1(X3,X1)
| X0 != X3
| k1_xboole_0 = k1_funct_1(X2,X3)
| v1_xboole_0(X1)
| ~ m1_pboole(X2,X1) ),
inference(cnf_transformation,[],[f43457]) ).
fof(f43655,plain,
! [X2,X0,X1] :
( k1_funct_4(X1,X2) = X2
| ~ m1_pboole(X2,X0)
| ~ m1_pboole(X1,X0)
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f42879]) ).
fof(f43667,plain,
! [X2,X0,X1] :
( a_2_0_closure3(X0,X1) = X2
| k1_closure3(X0,X1) != X2
| ~ m1_pboole(X1,X0)
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f43469]) ).
fof(f43669,plain,
~ v1_xboole_0(sK7),
inference(cnf_transformation,[],[f43470]) ).
fof(f43670,plain,
m1_pboole(sK8,sK7),
inference(cnf_transformation,[],[f43470]) ).
fof(f43671,plain,
v2_relat_1(sK8),
inference(cnf_transformation,[],[f43470]) ).
fof(f43672,plain,
sK8 != k1_funct_4(k1_pboole(sK7),k7_relat_1(sK8,k1_closure3(sK7,sK8))),
inference(cnf_transformation,[],[f43470]) ).
fof(f43678,plain,
! [X0,X1] :
( m1_subset_1(X0,X1)
| ~ r2_hidden(X0,X1) ),
inference(cnf_transformation,[],[f42897]) ).
fof(f43697,plain,
k1_xboole_0 = np__0,
inference(cnf_transformation,[],[f5328]) ).
fof(f43715,plain,
v1_xboole_0(k1_xboole_0),
inference(cnf_transformation,[],[f685]) ).
fof(f43748,plain,
! [X0,X1] :
( v1_funct_1(X1)
| ~ m1_pboole(X1,X0) ),
inference(cnf_transformation,[],[f42942]) ).
fof(f43749,plain,
! [X0,X1] :
( v1_relat_1(X1)
| ~ m1_pboole(X1,X0) ),
inference(cnf_transformation,[],[f42942]) ).
fof(f43753,plain,
! [X0,X1] :
( k1_relat_1(X1) = X0
| ~ m1_pboole(X1,X0)
| ~ v1_relat_1(X1)
| ~ v1_funct_1(X1) ),
inference(cnf_transformation,[],[f43490]) ).
fof(f43775,plain,
! [X3,X0,X1] :
( ~ r2_hidden(X3,X0)
| ~ v1_xboole_0(k1_funct_1(X1,X3))
| ~ v2_relat_1(X1)
| ~ m1_pboole(X1,X0) ),
inference(cnf_transformation,[],[f43501]) ).
fof(f44208,plain,
! [X0,X1] :
( r1_tarski(X0,X1)
| r2_hidden(sK85(X0,X1),X0) ),
inference(cnf_transformation,[],[f43606]) ).
fof(f44209,plain,
! [X0,X1] :
( r1_tarski(X0,X1)
| ~ r2_hidden(sK85(X0,X1),X1) ),
inference(cnf_transformation,[],[f43606]) ).
fof(f44285,plain,
! [X0,X1] :
( k7_relat_1(X1,X0) = X1
| ~ r1_tarski(k1_relat_1(X1),X0)
| ~ v1_relat_1(X1) ),
inference(cnf_transformation,[],[f43414]) ).
fof(f44310,plain,
! [X0] : m1_pboole(k1_pboole(X0),X0),
inference(cnf_transformation,[],[f8282]) ).
fof(f44341,plain,
! [X0] : k1_pboole(X0) = k2_funcop_1(X0,k1_xboole_0),
inference(cnf_transformation,[],[f8088]) ).
fof(f44345,plain,
! [X0] : k1_pboole(X0) = k2_funcop_1(X0,np__0),
inference(definition_unfolding,[],[f44341,f43697]) ).
fof(f44346,plain,
! [X2,X3,X0,X1] :
( r2_hidden(X0,a_2_0_closure3(X1,X2))
| ~ m1_subset_1(X3,X1)
| X0 != X3
| k1_funct_1(X2,X3) = np__0
| v1_xboole_0(X1)
| ~ m1_pboole(X2,X1) ),
inference(definition_unfolding,[],[f43633,f43697]) ).
fof(f44350,plain,
sK8 != k1_funct_4(k2_funcop_1(sK7,np__0),k7_relat_1(sK8,k1_closure3(sK7,sK8))),
inference(definition_unfolding,[],[f43672,f44345]) ).
fof(f44370,plain,
v1_xboole_0(np__0),
inference(definition_unfolding,[],[f43715,f43697]) ).
fof(f44445,plain,
! [X0] : m1_pboole(k2_funcop_1(X0,np__0),X0),
inference(definition_unfolding,[],[f44310,f44345]) ).
fof(f44479,plain,
! [X2,X3,X1] :
( r2_hidden(X3,a_2_0_closure3(X1,X2))
| ~ m1_subset_1(X3,X1)
| k1_funct_1(X2,X3) = np__0
| v1_xboole_0(X1)
| ~ m1_pboole(X2,X1) ),
inference(equality_resolution,[],[f44346]) ).
fof(f44482,plain,
! [X0,X1] :
( k1_closure3(X0,X1) = a_2_0_closure3(X0,X1)
| ~ m1_pboole(X1,X0)
| v1_xboole_0(X0) ),
inference(equality_resolution,[],[f43667]) ).
fof(f44679,definition,
( spl161_1
<=> sK8 = k1_funct_4(k2_funcop_1(sK7,np__0),k7_relat_1(sK8,k1_closure3(sK7,sK8))) ),
introduced(definition,[new_symbols(definition,[spl161_1])],[avatar_definition]) ).
fof(f44681,plain,
( sK8 != k1_funct_4(k2_funcop_1(sK7,np__0),k7_relat_1(sK8,k1_closure3(sK7,sK8)))
| spl161_1 ),
inference(avatar_component_clause,[],[f44679]) ).
fof(f44682,plain,
~ spl161_1,
inference(avatar_split_clause,[],[f44350,f44679]) ).
fof(f44738,plain,
( sK8 != k1_funct_4(k2_funcop_1(sK7,np__0),sK8)
| ~ r1_tarski(k1_relat_1(sK8),k1_closure3(sK7,sK8))
| ~ v1_relat_1(sK8)
| spl161_1 ),
inference(superposition,[],[f44681,f44285]) ).
fof(f44799,definition,
( spl161_2
<=> m1_pboole(sK8,sK7) ),
introduced(definition,[new_symbols(definition,[spl161_2])],[avatar_definition]) ).
fof(f44801,plain,
( m1_pboole(sK8,sK7)
| ~ spl161_2 ),
inference(avatar_component_clause,[],[f44799]) ).
fof(f44802,plain,
spl161_2,
inference(avatar_split_clause,[],[f43670,f44799]) ).
fof(f44819,plain,
( ! [X0] :
( sK8 = k1_funct_4(X0,sK8)
| ~ m1_pboole(X0,sK7)
| v1_xboole_0(sK7) )
| ~ spl161_2 ),
inference(resolution,[],[f44801,f43655]) ).
fof(f44827,plain,
( v1_funct_1(sK8)
| ~ spl161_2 ),
inference(resolution,[],[f44801,f43748]) ).
fof(f44828,plain,
( v1_relat_1(sK8)
| ~ spl161_2 ),
inference(resolution,[],[f44801,f43749]) ).
fof(f44833,plain,
( sK7 = k1_relat_1(sK8)
| ~ v1_relat_1(sK8)
| ~ v1_funct_1(sK8)
| ~ spl161_2 ),
inference(resolution,[],[f44801,f43753]) ).
fof(f44836,plain,
( ! [X0] :
( ~ r2_hidden(X0,sK7)
| ~ v1_xboole_0(k1_funct_1(sK8,X0))
| ~ v2_relat_1(sK8) )
| ~ spl161_2 ),
inference(resolution,[],[f44801,f43775]) ).
fof(f44963,plain,
( ! [X0] :
( r2_hidden(X0,a_2_0_closure3(sK7,sK8))
| ~ m1_subset_1(X0,sK7)
| np__0 = k1_funct_1(sK8,X0)
| v1_xboole_0(sK7) )
| ~ spl161_2 ),
inference(resolution,[],[f44801,f44479]) ).
fof(f44966,plain,
( k1_closure3(sK7,sK8) = a_2_0_closure3(sK7,sK8)
| v1_xboole_0(sK7)
| ~ spl161_2 ),
inference(resolution,[],[f44801,f44482]) ).
fof(f45008,plain,
( k1_closure3(sK7,sK8) = a_2_0_closure3(sK7,sK8)
| ~ spl161_2 ),
inference(forward_subsumption_resolution,[],[f44966,f43669]) ).
fof(f45011,plain,
( ! [X0] :
( r2_hidden(X0,a_2_0_closure3(sK7,sK8))
| ~ m1_subset_1(X0,sK7)
| np__0 = k1_funct_1(sK8,X0) )
| ~ spl161_2 ),
inference(forward_subsumption_resolution,[],[f44963,f43669]) ).
fof(f45021,plain,
( ! [X0] :
( ~ r2_hidden(X0,sK7)
| ~ v1_xboole_0(k1_funct_1(sK8,X0)) )
| ~ spl161_2 ),
inference(forward_subsumption_resolution,[],[f44836,f43671]) ).
fof(f45031,plain,
( sK8 != k1_funct_4(k2_funcop_1(sK7,np__0),sK8)
| ~ r1_tarski(k1_relat_1(sK8),k1_closure3(sK7,sK8))
| spl161_1
| ~ spl161_2 ),
inference(backward_subsumption_resolution,[],[f44738,f44828]) ).
fof(f45038,plain,
( sK7 = k1_relat_1(sK8)
| ~ v1_funct_1(sK8)
| ~ spl161_2 ),
inference(backward_subsumption_resolution,[],[f44833,f44828]) ).
fof(f45040,plain,
( ! [X0] :
( sK8 = k1_funct_4(X0,sK8)
| ~ m1_pboole(X0,sK7) )
| ~ spl161_2 ),
inference(forward_subsumption_resolution,[],[f44819,f43669]) ).
fof(f45058,plain,
( ~ r1_tarski(k1_relat_1(sK8),a_2_0_closure3(sK7,sK8))
| sK8 != k1_funct_4(k2_funcop_1(sK7,np__0),sK8)
| spl161_1
| ~ spl161_2 ),
inference(forward_demodulation,[],[f45031,f45008]) ).
fof(f45065,plain,
( sK7 = k1_relat_1(sK8)
| ~ spl161_2 ),
inference(forward_subsumption_resolution,[],[f45038,f44827]) ).
fof(f45703,definition,
( spl161_10
<=> ! [X0] :
( sK8 = k1_funct_4(X0,sK8)
| ~ m1_pboole(X0,sK7) ) ),
introduced(definition,[new_symbols(definition,[spl161_10])],[avatar_definition]) ).
fof(f45704,plain,
( ! [X0] :
( sK8 = k1_funct_4(X0,sK8)
| ~ m1_pboole(X0,sK7) )
| ~ spl161_10 ),
inference(avatar_component_clause,[],[f45703]) ).
fof(f45705,plain,
( spl161_10
| ~ spl161_2 ),
inference(avatar_split_clause,[],[f45040,f44799,f45703]) ).
fof(f46344,definition,
( spl161_17
<=> ! [X0] :
( r2_hidden(X0,a_2_0_closure3(sK7,sK8))
| ~ m1_subset_1(X0,sK7)
| np__0 = k1_funct_1(sK8,X0) ) ),
introduced(definition,[new_symbols(definition,[spl161_17])],[avatar_definition]) ).
fof(f46345,plain,
( ! [X0] :
( r2_hidden(X0,a_2_0_closure3(sK7,sK8))
| ~ m1_subset_1(X0,sK7)
| np__0 = k1_funct_1(sK8,X0) )
| ~ spl161_17 ),
inference(avatar_component_clause,[],[f46344]) ).
fof(f46346,plain,
( spl161_17
| ~ spl161_2 ),
inference(avatar_split_clause,[],[f45011,f44799,f46344]) ).
fof(f48144,definition,
( spl161_22
<=> sK8 = k1_funct_4(k2_funcop_1(sK7,np__0),sK8) ),
introduced(definition,[new_symbols(definition,[spl161_22])],[avatar_definition]) ).
fof(f48146,plain,
( sK8 != k1_funct_4(k2_funcop_1(sK7,np__0),sK8)
| spl161_22 ),
inference(avatar_component_clause,[],[f48144]) ).
fof(f48148,definition,
( spl161_23
<=> r1_tarski(k1_relat_1(sK8),a_2_0_closure3(sK7,sK8)) ),
introduced(definition,[new_symbols(definition,[spl161_23])],[avatar_definition]) ).
fof(f48150,plain,
( ~ r1_tarski(k1_relat_1(sK8),a_2_0_closure3(sK7,sK8))
| spl161_23 ),
inference(avatar_component_clause,[],[f48148]) ).
fof(f48151,plain,
( ~ spl161_22
| ~ spl161_23
| spl161_1
| ~ spl161_2 ),
inference(avatar_split_clause,[],[f45058,f44799,f44679,f48148,f48144]) ).
fof(f48298,definition,
( spl161_30
<=> sK7 = k1_relat_1(sK8) ),
introduced(definition,[new_symbols(definition,[spl161_30])],[avatar_definition]) ).
fof(f48300,plain,
( sK7 = k1_relat_1(sK8)
| ~ spl161_30 ),
inference(avatar_component_clause,[],[f48298]) ).
fof(f48301,plain,
( spl161_30
| ~ spl161_2 ),
inference(avatar_split_clause,[],[f45065,f44799,f48298]) ).
fof(f48563,plain,
( sK8 != sK8
| ~ m1_pboole(k2_funcop_1(sK7,np__0),sK7)
| ~ spl161_10
| spl161_22 ),
inference(superposition,[],[f48146,f45704]) ).
fof(f48587,plain,
( ~ m1_pboole(k2_funcop_1(sK7,np__0),sK7)
| ~ spl161_10
| spl161_22 ),
inference(trivial_inequality_removal,[],[f48563]) ).
fof(f48603,plain,
( $false
| ~ spl161_10
| spl161_22 ),
inference(forward_subsumption_resolution,[],[f48587,f44445]) ).
fof(f48604,plain,
( ~ spl161_10
| spl161_22 ),
inference(avatar_contradiction_clause,[],[f48603]) ).
fof(f48663,plain,
( ~ r1_tarski(sK7,a_2_0_closure3(sK7,sK8))
| spl161_23
| ~ spl161_30 ),
inference(forward_demodulation,[],[f48150,f48300]) ).
fof(f51753,definition,
( spl161_51
<=> r1_tarski(sK7,a_2_0_closure3(sK7,sK8)) ),
introduced(definition,[new_symbols(definition,[spl161_51])],[avatar_definition]) ).
fof(f51755,plain,
( ~ r1_tarski(sK7,a_2_0_closure3(sK7,sK8))
| spl161_51 ),
inference(avatar_component_clause,[],[f51753]) ).
fof(f51756,plain,
( ~ spl161_51
| spl161_23
| ~ spl161_30 ),
inference(avatar_split_clause,[],[f48663,f48298,f48148,f51753]) ).
fof(f51768,plain,
( r2_hidden(sK85(sK7,a_2_0_closure3(sK7,sK8)),sK7)
| spl161_51 ),
inference(resolution,[],[f51755,f44208]) ).
fof(f51769,plain,
( ~ r2_hidden(sK85(sK7,a_2_0_closure3(sK7,sK8)),a_2_0_closure3(sK7,sK8))
| spl161_51 ),
inference(resolution,[],[f51755,f44209]) ).
fof(f51857,definition,
( spl161_52
<=> r2_hidden(sK85(sK7,a_2_0_closure3(sK7,sK8)),sK7) ),
introduced(definition,[new_symbols(definition,[spl161_52])],[avatar_definition]) ).
fof(f51859,plain,
( r2_hidden(sK85(sK7,a_2_0_closure3(sK7,sK8)),sK7)
| ~ spl161_52 ),
inference(avatar_component_clause,[],[f51857]) ).
fof(f51860,plain,
( spl161_52
| spl161_51 ),
inference(avatar_split_clause,[],[f51768,f51753,f51857]) ).
fof(f51865,plain,
( m1_subset_1(sK85(sK7,a_2_0_closure3(sK7,sK8)),sK7)
| ~ spl161_52 ),
inference(resolution,[],[f51859,f43678]) ).
fof(f53729,definition,
( spl161_76
<=> ! [X0] :
( ~ r2_hidden(X0,sK7)
| ~ v1_xboole_0(k1_funct_1(sK8,X0)) ) ),
introduced(definition,[new_symbols(definition,[spl161_76])],[avatar_definition]) ).
fof(f53730,plain,
( ! [X0] :
( ~ v1_xboole_0(k1_funct_1(sK8,X0))
| ~ r2_hidden(X0,sK7) )
| ~ spl161_76 ),
inference(avatar_component_clause,[],[f53729]) ).
fof(f53731,plain,
( spl161_76
| ~ spl161_2 ),
inference(avatar_split_clause,[],[f45021,f44799,f53729]) ).
fof(f54004,definition,
( spl161_81
<=> r2_hidden(sK85(sK7,a_2_0_closure3(sK7,sK8)),a_2_0_closure3(sK7,sK8)) ),
introduced(definition,[new_symbols(definition,[spl161_81])],[avatar_definition]) ).
fof(f54006,plain,
( ~ r2_hidden(sK85(sK7,a_2_0_closure3(sK7,sK8)),a_2_0_closure3(sK7,sK8))
| spl161_81 ),
inference(avatar_component_clause,[],[f54004]) ).
fof(f54007,plain,
( ~ spl161_81
| spl161_51 ),
inference(avatar_split_clause,[],[f51769,f51753,f54004]) ).
fof(f54008,plain,
( ~ m1_subset_1(sK85(sK7,a_2_0_closure3(sK7,sK8)),sK7)
| np__0 = k1_funct_1(sK8,sK85(sK7,a_2_0_closure3(sK7,sK8)))
| ~ spl161_17
| spl161_81 ),
inference(resolution,[],[f54006,f46345]) ).
fof(f54034,plain,
( np__0 = k1_funct_1(sK8,sK85(sK7,a_2_0_closure3(sK7,sK8)))
| ~ spl161_17
| ~ spl161_52
| spl161_81 ),
inference(forward_subsumption_resolution,[],[f54008,f51865]) ).
fof(f54037,definition,
( spl161_82
<=> np__0 = k1_funct_1(sK8,sK85(sK7,a_2_0_closure3(sK7,sK8))) ),
introduced(definition,[new_symbols(definition,[spl161_82])],[avatar_definition]) ).
fof(f54039,plain,
( np__0 = k1_funct_1(sK8,sK85(sK7,a_2_0_closure3(sK7,sK8)))
| ~ spl161_82 ),
inference(avatar_component_clause,[],[f54037]) ).
fof(f54040,plain,
( spl161_82
| ~ spl161_17
| ~ spl161_52
| spl161_81 ),
inference(avatar_split_clause,[],[f54034,f54004,f51857,f46344,f54037]) ).
fof(f54046,plain,
( ~ v1_xboole_0(np__0)
| ~ r2_hidden(sK85(sK7,a_2_0_closure3(sK7,sK8)),sK7)
| ~ spl161_76
| ~ spl161_82 ),
inference(superposition,[],[f53730,f54039]) ).
fof(f54102,plain,
( ~ r2_hidden(sK85(sK7,a_2_0_closure3(sK7,sK8)),sK7)
| ~ spl161_76
| ~ spl161_82 ),
inference(forward_subsumption_resolution,[],[f54046,f44370]) ).
fof(f54130,plain,
( $false
| ~ spl161_52
| ~ spl161_76
| ~ spl161_82 ),
inference(forward_subsumption_resolution,[],[f54102,f51859]) ).
fof(f54131,plain,
( ~ spl161_52
| ~ spl161_76
| ~ spl161_82 ),
inference(avatar_contradiction_clause,[],[f54130]) ).
cnf(s1,plain,
~ spl161_1,
inference(sat_conversion,[],[f44682]) ).
cnf(s2,plain,
spl161_2,
inference(sat_conversion,[],[f44802]) ).
cnf(s10,plain,
( ~ spl161_2
| spl161_10 ),
inference(sat_conversion,[],[f45705]) ).
cnf(s17,plain,
( ~ spl161_2
| spl161_17 ),
inference(sat_conversion,[],[f46346]) ).
cnf(s22,plain,
( spl161_1
| ~ spl161_2
| ~ spl161_22
| ~ spl161_23 ),
inference(sat_conversion,[],[f48151]) ).
cnf(s29,plain,
( ~ spl161_2
| spl161_30 ),
inference(sat_conversion,[],[f48301]) ).
cnf(s30,plain,
( ~ spl161_10
| spl161_22 ),
inference(sat_conversion,[],[f48604]) ).
cnf(s53,plain,
( spl161_23
| ~ spl161_30
| ~ spl161_51 ),
inference(sat_conversion,[],[f51756]) ).
cnf(s54,plain,
( spl161_51
| spl161_52 ),
inference(sat_conversion,[],[f51860]) ).
cnf(s78,plain,
( ~ spl161_2
| spl161_76 ),
inference(sat_conversion,[],[f53731]) ).
cnf(s83,plain,
( spl161_51
| ~ spl161_81 ),
inference(sat_conversion,[],[f54007]) ).
cnf(s84,plain,
( ~ spl161_17
| ~ spl161_52
| spl161_81
| spl161_82 ),
inference(sat_conversion,[],[f54040]) ).
cnf(s86,plain,
( ~ spl161_52
| ~ spl161_76
| ~ spl161_82 ),
inference(sat_conversion,[],[f54131]) ).
cnf(s90,plain,
spl161_76,
inference(rat,[],[s78,s2]) ).
cnf(s106,plain,
spl161_30,
inference(rat,[],[s29,s2]) ).
cnf(s114,plain,
spl161_17,
inference(rat,[],[s17,s2]) ).
cnf(s119,plain,
spl161_10,
inference(rat,[],[s10,s2]) ).
cnf(s140,plain,
spl161_22,
inference(rat,[],[s30,s119]) ).
cnf(s157,plain,
~ spl161_23,
inference(rat,[],[s22,s140,s2,s1]) ).
cnf(s162,plain,
~ spl161_51,
inference(rat,[],[s53,s106,s157]) ).
cnf(s163,plain,
~ spl161_81,
inference(rat,[],[s83,s162]) ).
cnf(s164,plain,
spl161_52,
inference(rat,[],[s54,s162]) ).
cnf(s165,plain,
~ spl161_82,
inference(rat,[],[s86,s90,s164]) ).
cnf(s166,plain,
$false,
inference(rat,[],[s84,s163,s114,s165,s164]) ).
fof(f54175,plain,
$false,
inference(avatar_sat_refutation,[],[s166]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ALG225+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.19 % Computer : n003.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 19:52:20 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.23 Running first-order theorem proving
% 0.09/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 18.76/5.86 % (1922004)Detected formulas, will run a generic FOF schedule.
% 18.76/5.86 % (1922009)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=12591692:i=141193_2971 on theBenchmark for (2971ds/141193Mi)
% 18.76/5.86 % (1922010)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=3706035578:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2971 on theBenchmark for (2971ds/134677Mi)
% 18.76/5.86 % (1922013)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=4265064946:i=119:av=off:ss=axioms_2971 on theBenchmark for (2971ds/119Mi)
% 18.76/5.86 % (1922011)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=3824712667:i=141695:sd=1:nm=32:gsp=on:ss=included_2971 on theBenchmark for (2971ds/141695Mi)
% 18.76/5.86 % (1922012)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3907215584:i=109:sd=1:ins=1:gsp=on:ss=axioms_2971 on theBenchmark for (2971ds/109Mi)
% 18.76/5.86 % (1922015)dis-21_1_sil=8000:lcm=predicate:random_seed=2589718906:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2971 on theBenchmark for (2971ds/129Mi)
% 18.76/5.86 % (1922014)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=405020294:s2a=on:i=139:gtg=position_2971 on theBenchmark for (2971ds/139Mi)
% 18.76/5.86 % (1922012)Instruction limit reached!
% 18.76/5.86 % (1922012)------------------------------
% 18.76/5.86 % (1922012)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.76/5.86 % (1922012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.76/5.86 % (1922012)CaDiCaL version: 2.1.3
% 18.76/5.86 % (1922012)Termination reason: Instruction limit
% 18.76/5.86 % (1922012)Termination phase: SInE selection
% 18.76/5.86 % (1922012)Time elapsed: 0.080 s
% 18.76/5.86 % (1922012)Peak memory usage: 148 MB
% 18.76/5.86 % (1922012)Instructions burned: 109 (million)
% 18.76/5.86 % (1922014)Instruction limit reached!
% 18.76/5.86 % (1922014)------------------------------
% 18.76/5.86 % (1922014)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.76/5.86 % (1922014)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.76/5.86 % (1922014)CaDiCaL version: 2.1.3
% 18.76/5.86 % (1922014)Termination reason: Instruction limit
% 18.76/5.86 % (1922014)Termination phase: Property scanning
% 18.76/5.86 % (1922014)Time elapsed: 0.065 s
% 18.76/5.86 % (1922014)Peak memory usage: 149 MB
% 18.76/5.86 % (1922014)Instructions burned: 140 (million)
% 18.76/5.86 % (1922013)Instruction limit reached!
% 18.76/5.86 % (1922013)------------------------------
% 18.76/5.86 % (1922013)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.76/5.86 % (1922013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.76/5.86 % (1922013)CaDiCaL version: 2.1.3
% 18.76/5.86 % (1922013)Termination reason: Instruction limit
% 18.76/5.86 % (1922013)Termination phase: SInE selection
% 18.76/5.86 % (1922013)Time elapsed: 0.087 s
% 18.76/5.86 % (1922013)Peak memory usage: 148 MB
% 18.76/5.86 % (1922013)Instructions burned: 119 (million)
% 18.76/5.86 % (1922015)Instruction limit reached!
% 18.76/5.86 % (1922015)------------------------------
% 18.76/5.86 % (1922015)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.76/5.86 % (1922015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.76/5.86 % (1922015)CaDiCaL version: 2.1.3
% 18.76/5.86 % (1922015)Termination reason: Instruction limit
% 18.76/5.86 % (1922015)Termination phase: SInE selection
% 18.76/5.86 % (1922015)Time elapsed: 0.101 s
% 18.76/5.86 % (1922015)Peak memory usage: 148 MB
% 18.76/5.86 % (1922015)Instructions burned: 129 (million)
% 18.76/5.86 % (1922023)lrs+10_1_sil=8000:sp=occurrence:random_seed=1214076713:i=285:sd=3:ss=axioms:sgt=8_2968 on theBenchmark for (2968ds/285Mi)
% 18.76/5.86 % (1922025)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1223640248:i=325:sd=1:ss=axioms:sgt=32_2968 on theBenchmark for (2968ds/325Mi)
% 18.76/5.86 % (1922024)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2545739494:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2968 on theBenchmark for (2968ds/157Mi)
% 18.76/5.86 % (1922026)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=2722553344:s2a=on:i=248:s2at=1.23:gtg=position_2968 on theBenchmark for (2968ds/248Mi)
% 18.76/5.86 % (1922024)Instruction limit reached!
% 21.33/6.50 % (1922024)------------------------------
% 21.33/6.50 % (1922024)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.33/6.50 % (1922024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.33/6.50 % (1922024)CaDiCaL version: 2.1.3
% 21.33/6.50 % (1922024)Termination reason: Instruction limit
% 21.33/6.50 % (1922024)Termination phase: Property scanning
% 21.33/6.50 % (1922024)Time elapsed: 0.073 s
% 21.33/6.50 % (1922024)Peak memory usage: 149 MB
% 21.33/6.50 % (1922024)Instructions burned: 158 (million)
% 21.33/6.50 % (1922026)Instruction limit reached!
% 21.33/6.50 % (1922026)------------------------------
% 21.33/6.50 % (1922026)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.33/6.50 % (1922026)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.33/6.50 % (1922026)CaDiCaL version: 2.1.3
% 21.33/6.50 % (1922026)Termination reason: Instruction limit
% 21.33/6.50 % (1922026)Termination phase: Property scanning
% 21.33/6.50 % (1922026)Time elapsed: 0.114 s
% 21.33/6.50 % (1922026)Peak memory usage: 149 MB
% 21.33/6.50 % (1922026)Instructions burned: 250 (million)
% 21.33/6.50 % (1922023)Instruction limit reached!
% 21.33/6.50 % (1922023)------------------------------
% 21.33/6.50 % (1922023)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.33/6.50 % (1922023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.33/6.50 % (1922023)CaDiCaL version: 2.1.3
% 21.33/6.50 % (1922023)Termination reason: Instruction limit
% 21.33/6.50 % (1922023)Termination phase: SInE selection
% 21.33/6.50 % (1922023)Time elapsed: 0.201 s
% 21.33/6.50 % (1922023)Peak memory usage: 149 MB
% 21.33/6.50 % (1922023)Instructions burned: 285 (million)
% 21.33/6.50 % (1922031)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1882326101:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2966 on theBenchmark for (2966ds/294Mi)
% 21.33/6.50 % (1922025)Instruction limit reached!
% 21.33/6.50 % (1922025)------------------------------
% 21.33/6.50 % (1922025)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.33/6.50 % (1922025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.33/6.50 % (1922025)CaDiCaL version: 2.1.3
% 21.33/6.50 % (1922025)Termination reason: Instruction limit
% 21.33/6.50 % (1922025)Termination phase: Saturation
% 21.33/6.50 % (1922025)Time elapsed: 0.254 s
% 21.33/6.50 % (1922025)Peak memory usage: 154 MB
% 21.33/6.50 % (1922025)Instructions burned: 327 (million)
% 21.33/6.50 % (1922032)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3343803311:i=2350_2965 on theBenchmark for (2965ds/2350Mi)
% 21.33/6.50 % (1922033)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2585757826:cts=off:i=113:fsr=off:ss=included:sgt=4_2965 on theBenchmark for (2965ds/113Mi)
% 21.33/6.50 % (1922035)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1956587297:i=127:av=off:fsr=off:sup=off_2964 on theBenchmark for (2964ds/127Mi)
% 21.33/6.50 % (1922031)Instruction limit reached!
% 21.33/6.50 % (1922031)------------------------------
% 21.33/6.50 % (1922031)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.33/6.50 % (1922031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.33/6.50 % (1922031)CaDiCaL version: 2.1.3
% 21.33/6.50 % (1922031)Termination reason: Instruction limit
% 21.33/6.50 % (1922031)Termination phase: SInE selection
% 21.33/6.50 % (1922031)Time elapsed: 0.189 s
% 21.33/6.50 % (1922031)Peak memory usage: 149 MB
% 21.33/6.50 % (1922031)Instructions burned: 296 (million)
% 21.33/6.50 % (1922033)Instruction limit reached!
% 21.33/6.50 % (1922033)------------------------------
% 21.33/6.50 % (1922033)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.33/6.50 % (1922033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.33/6.50 % (1922033)CaDiCaL version: 2.1.3
% 21.33/6.50 % (1922033)Termination reason: Instruction limit
% 21.33/6.50 % (1922033)Termination phase: SInE selection
% 21.33/6.50 % (1922033)Time elapsed: 0.091 s
% 21.33/6.50 % (1922033)Peak memory usage: 149 MB
% 21.33/6.50 % (1922033)Instructions burned: 114 (million)
% 21.33/6.50 % (1922035)Instruction limit reached!
% 21.33/6.50 % (1922035)------------------------------
% 21.33/6.50 % (1922035)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.33/6.50 % (1922035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.33/6.50 % (1922035)CaDiCaL version: 2.1.3
% 21.33/6.50 % (1922035)Termination reason: Instruction limit
% 21.33/6.50 % (1922035)Termination phase: Preprocessing 1
% 21.33/6.50 % (1922035)Time elapsed: 0.096 s
% 21.33/6.50 % (1922035)Peak memory usage: 150 MB
% 21.33/6.50 % (1922035)Instructions burned: 128 (million)
% 21.33/6.50 % (1922039)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=287875708:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2963 on theBenchmark for (2963ds/114Mi)
% 21.33/6.50 % (1922040)lrs+10_1_sil=8000:sp=occurrence:random_seed=2273840640:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2962 on theBenchmark for (2962ds/907Mi)
% 21.33/6.50 % (1922039)Instruction limit reached!
% 21.33/6.50 % (1922039)------------------------------
% 21.33/6.50 % (1922039)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.33/6.50 % (1922039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.33/6.50 % (1922039)CaDiCaL version: 2.1.3
% 21.33/6.50 % (1922039)Termination reason: Instruction limit
% 21.33/6.50 % (1922039)Termination phase: Property scanning
% 21.33/6.50 % (1922039)Time elapsed: 0.055 s
% 21.33/6.50 % (1922039)Peak memory usage: 149 MB
% 21.33/6.50 % (1922039)Instructions burned: 116 (million)
% 21.33/6.50 % (1922041)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1869488305:i=437:sd=1:aac=none:ss=included_2962 on theBenchmark for (2962ds/437Mi)
% 21.33/6.50 % (1922044)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2689103041:i=5202:ss=axioms:sgt=16_2960 on theBenchmark for (2960ds/5202Mi)
% 21.33/6.50 % (1922041)Instruction limit reached!
% 21.33/6.50 % (1922041)------------------------------
% 21.33/6.50 % (1922041)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.33/6.50 % (1922041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.33/6.50 % (1922041)CaDiCaL version: 2.1.3
% 21.33/6.50 % (1922041)Termination reason: Instruction limit
% 21.33/6.50 % (1922041)Termination phase: Saturation
% 21.33/6.50 % (1922041)Time elapsed: 0.323 s
% 21.33/6.50 % (1922041)Peak memory usage: 155 MB
% 21.33/6.50 % (1922041)Instructions burned: 438 (million)
% 21.33/6.50 % (1922047)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=643838700:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2957 on theBenchmark for (2957ds/134Mi)
% 21.33/6.50 % (1922040)Instruction limit reached!
% 21.33/6.50 % (1922040)------------------------------
% 21.33/6.50 % (1922040)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.33/6.50 % (1922040)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.33/6.50 % (1922040)CaDiCaL version: 2.1.3
% 21.33/6.50 % (1922040)Termination reason: Instruction limit
% 21.33/6.50 % (1922040)Termination phase: Property scanning
% 21.33/6.50 % (1922040)Time elapsed: 0.580 s
% 21.33/6.50 % (1922040)Peak memory usage: 163 MB
% 21.33/6.50 % (1922040)Instructions burned: 907 (million)
% 21.33/6.50 % (1922047)Instruction limit reached!
% 21.33/6.50 % (1922047)------------------------------
% 21.33/6.50 % (1922047)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.33/6.50 % (1922047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.33/6.50 % (1922047)CaDiCaL version: 2.1.3
% 21.33/6.50 % (1922047)Termination reason: Instruction limit
% 21.33/6.50 % (1922047)Termination phase: SInE selection
% 21.33/6.50 % (1922047)Time elapsed: 0.106 s
% 21.33/6.50 % (1922047)Peak memory usage: 149 MB
% 21.33/6.50 % (1922047)Instructions burned: 134 (million)
% 21.33/6.50 % (1922049)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=773821124:st=8:i=592:sd=3:ep=RST:ss=axioms_2955 on theBenchmark for (2955ds/592Mi)
% 21.33/6.50 % (1922050)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3209642880:st=3:i=13193:sd=3:ss=axioms_2954 on theBenchmark for (2954ds/13193Mi)
% 21.33/6.50 % (1922049)Instruction limit reached!
% 21.33/6.50 % (1922049)------------------------------
% 21.33/6.50 % (1922049)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.33/6.50 % (1922049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.33/6.50 % (1922049)CaDiCaL version: 2.1.3
% 21.33/6.50 % (1922049)Termination reason: Instruction limit
% 21.33/6.50 % (1922049)Termination phase: Preprocessing 1
% 21.33/6.50 % (1922049)Time elapsed: 0.418 s
% 21.33/6.50 % (1922049)Peak memory usage: 152 MB
% 21.33/6.50 % (1922049)Instructions burned: 592 (million)
% 21.33/6.50 % (1922032)Instruction limit reached!
% 21.33/6.50 % (1922032)------------------------------
% 21.33/6.50 % (1922032)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.33/6.50 % (1922032)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.33/6.50 % (1922032)CaDiCaL version: 2.1.3
% 21.33/6.50 % (1922032)Termination reason: Instruction limit
% 21.33/6.50 % (1922032)Termination phase: Preprocessing 3
% 21.33/6.50 % (1922032)Time elapsed: 1.599 s
% 21.33/6.50 % (1922032)Peak memory usage: 249 MB
% 21.33/6.50 % (1922032)Instructions burned: 2351 (million)
% 21.33/6.50 % (1922053)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=1643921868:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2949 on theBenchmark for (2949ds/125Mi)
% 21.33/6.50 % (1922053)Instruction limit reached!
% 21.33/6.50 % (1922053)------------------------------
% 21.33/6.50 % (1922053)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.33/6.50 % (1922053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.33/6.50 % (1922053)CaDiCaL version: 2.1.3
% 21.33/6.50 % (1922053)Termination reason: Instruction limit
% 21.33/6.50 % (1922053)Termination phase: Property scanning
% 21.33/6.50 % (1922053)Time elapsed: 0.060 s
% 21.33/6.50 % (1922053)Peak memory usage: 149 MB
% 21.33/6.50 % (1922053)Instructions burned: 127 (million)
% 21.33/6.50 % (1922054)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3806532650:i=134:gtgl=5:slsql=off:gtg=exists_sym_2947 on theBenchmark for (2947ds/134Mi)
% 21.33/6.50 % (1922054)Instruction limit reached!
% 21.33/6.50 % (1922054)------------------------------
% 21.33/6.50 % (1922054)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.33/6.50 % (1922054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.33/6.50 % (1922054)CaDiCaL version: 2.1.3
% 21.33/6.50 % (1922054)Termination reason: Instruction limit
% 21.33/6.50 % (1922054)Termination phase: Property scanning
% 21.33/6.50 % (1922054)Time elapsed: 0.064 s
% 21.33/6.50 % (1922054)Peak memory usage: 149 MB
% 21.33/6.50 % (1922054)Instructions burned: 136 (million)
% 21.33/6.50 % (1922011)First to succeed.
% 21.33/6.50 % (1922011)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1922004"
% 21.33/6.50 % (1922056)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3519067724:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2946 on theBenchmark for (2946ds/141Mi)
% 21.33/6.50 % (1922056)Instruction limit reached!
% 21.33/6.50 % (1922056)------------------------------
% 21.33/6.50 % (1922056)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.33/6.50 % (1922056)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.33/6.50 % (1922056)CaDiCaL version: 2.1.3
% 21.33/6.50 % (1922056)Termination reason: Instruction limit
% 21.33/6.50 % (1922056)Termination phase: SInE selection
% 21.33/6.50 % (1922056)Time elapsed: 0.112 s
% 21.33/6.50 % (1922056)Peak memory usage: 149 MB
% 21.33/6.50 % (1922056)Instructions burned: 142 (million)
% 21.33/6.50 % (1922058)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2090522158:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2945 on theBenchmark for (2945ds/431Mi)
% 21.33/6.50 % (1922060)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=1935175979:i=6060:aac=none:ins=25_2943 on theBenchmark for (2943ds/6060Mi)
% 21.33/6.50 % (1922011)Refutation found. Thanks to Tanya!
% 21.33/6.50 % SZS status Theorem for theBenchmark
% 21.33/6.50 % SZS output start Proof for theBenchmark
% See solution above
% 24.51/6.74 % (1922011)------------------------------
% 24.51/6.74 % (1922011)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.51/6.74 % (1922011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.51/6.74 % (1922011)CaDiCaL version: 2.1.3
% 24.51/6.74 % (1922011)Termination reason: Refutation
% 24.51/6.74 % (1922011)Time elapsed: 2.452 s
% 24.51/6.74 % (1922011)Peak memory usage: 224 MB
% 24.51/6.74 % (1922011)Instructions burned: 3795 (million)
% 24.51/6.74 % (1922011)------------------------------
% 24.51/6.74 % (1922011)------------------------------
% 24.51/6.74 % (1922004)Success in time 5.823 s
% 24.51/6.74 % Vampire exiting
%------------------------------------------------------------------------------