%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU425+4 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:48:56 PM UTC 2026
% Result : Theorem 15.17s 9.23s
% Output : Refutation 25.63s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 22
% Syntax : Number of formulae : 125 ( 20 unt; 8 def)
% Number of atoms : 365 ( 45 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 423 ( 183 ~; 174 |; 44 &)
% ( 12 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 20 ( 18 usr; 7 prp; 0-3 aty)
% Number of functors : 15 ( 15 usr; 5 con; 0-4 aty)
% Number of variables : 165 ( 0 sgn 157 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f29,axiom,
! [X0] :
( X0 = k1_xboole_0
<=> ! [X1] : ~ r2_hidden(X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d1_xboole_0) ).
fof(f322,axiom,
! [X0,X1] :
( X1 = k1_zfmisc_1(X0)
<=> ! [X2] :
( r2_hidden(X2,X1)
<=> r1_tarski(X2,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d1_zfmisc_1) ).
fof(f327,axiom,
k3_tarski(k1_xboole_0) = k1_xboole_0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2_zfmisc_1) ).
fof(f424,axiom,
! [X0] : k3_tarski(k1_zfmisc_1(X0)) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t99_zfmisc_1) ).
fof(f677,axiom,
! [X0,X1] :
( m1_subset_1(X0,k1_zfmisc_1(X1))
<=> r1_tarski(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t3_subset) ).
fof(f1507,axiom,
! [X0,X1,X2,X3] :
( m1_relset_1(X2,X0,X1)
=> m1_subset_1(k10_relset_1(X0,X1,X2,X3),k1_zfmisc_1(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k10_relset_1) ).
fof(f1545,axiom,
! [X0,X1,X2,X3] :
( ( v1_funct_1(X3)
& m2_relset_1(X3,X0,X1) )
=> ( r1_tarski(k2_relat_1(X3),X2)
=> ( v1_funct_1(X3)
& m2_relset_1(X3,X0,X2) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t29_partfun1) ).
fof(f1912,axiom,
! [X0,X1,X2,X3] :
( ( v1_funct_1(X3)
& v1_funct_2(X3,X0,X1)
& m2_relset_1(X3,X0,X1) )
=> ( r1_tarski(k2_relat_1(X3),X2)
=> ( ( X1 = k1_xboole_0
& X0 != k1_xboole_0 )
| ( v1_funct_1(X3)
& v1_funct_2(X3,X0,X2)
& m2_relset_1(X3,X0,X2) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t8_funct_2) ).
fof(f5328,axiom,
np__0 = k1_xboole_0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t51_card_1) ).
fof(f58664,axiom,
! [X0] :
? [X1] :
( m1_relset_1(X1,k1_zfmisc_1(X0),k1_zfmisc_1(X0))
& v1_relat_1(X1)
& ~ v1_xboole_0(X1)
& v1_finset_1(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc4_armstrng) ).
fof(f71072,axiom,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X1,X0)))
=> ( v1_funct_1(k6_relset_2(X0,X1,X2))
& v1_funct_2(k6_relset_2(X0,X1,X2),k1_zfmisc_1(X1),k1_zfmisc_1(X0))
& m2_relset_1(k6_relset_2(X0,X1,X2),k1_zfmisc_1(X1),k1_zfmisc_1(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k6_relset_2) ).
fof(f71073,axiom,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X1,X0)))
=> k6_relset_2(X0,X1,X2) = k5_relset_2(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k6_relset_2) ).
fof(f71101,axiom,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
=> r1_tarski(k2_relat_1(k5_relset_2(X0,X2)),k1_zfmisc_1(k2_relat_1(X2))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t20_relset_2) ).
fof(f71102,conjecture,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
=> ( v1_funct_1(k5_relset_2(X0,X2))
& v1_funct_2(k5_relset_2(X0,X2),k1_zfmisc_1(X0),k1_zfmisc_1(k2_relat_1(X2)))
& m2_relset_1(k5_relset_2(X0,X2),k1_zfmisc_1(X0),k1_zfmisc_1(k2_relat_1(X2))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t21_relset_2) ).
fof(f71103,negated_conjecture,
~ ! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
=> ( v1_funct_1(k5_relset_2(X0,X2))
& v1_funct_2(k5_relset_2(X0,X2),k1_zfmisc_1(X0),k1_zfmisc_1(k2_relat_1(X2)))
& m2_relset_1(k5_relset_2(X0,X2),k1_zfmisc_1(X0),k1_zfmisc_1(k2_relat_1(X2))) ) ),
inference(negated_conjecture,[status(cth)],[f71102]) ).
fof(f71166,plain,
! [X0,X1,X2] :
( ( v1_funct_1(k6_relset_2(X0,X1,X2))
& v1_funct_2(k6_relset_2(X0,X1,X2),k1_zfmisc_1(X1),k1_zfmisc_1(X0))
& m2_relset_1(k6_relset_2(X0,X1,X2),k1_zfmisc_1(X1),k1_zfmisc_1(X0)) )
| ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X1,X0))) ),
inference(ennf_transformation,[],[f71072]) ).
fof(f71167,plain,
! [X0,X1,X2] :
( k6_relset_2(X0,X1,X2) = k5_relset_2(X1,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X1,X0))) ),
inference(ennf_transformation,[],[f71073]) ).
fof(f71194,plain,
! [X0,X1,X2] :
( r1_tarski(k2_relat_1(k5_relset_2(X0,X2)),k1_zfmisc_1(k2_relat_1(X2)))
| ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(ennf_transformation,[],[f71101]) ).
fof(f71195,plain,
? [X0,X1,X2] :
( ( ~ v1_funct_1(k5_relset_2(X0,X2))
| ~ v1_funct_2(k5_relset_2(X0,X2),k1_zfmisc_1(X0),k1_zfmisc_1(k2_relat_1(X2)))
| ~ m2_relset_1(k5_relset_2(X0,X2),k1_zfmisc_1(X0),k1_zfmisc_1(k2_relat_1(X2))) )
& m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(ennf_transformation,[],[f71103]) ).
fof(f71752,plain,
! [X0,X1,X2,X3] :
( m1_subset_1(k10_relset_1(X0,X1,X2,X3),k1_zfmisc_1(X1))
| ~ m1_relset_1(X2,X0,X1) ),
inference(ennf_transformation,[],[f1507]) ).
fof(f71955,plain,
! [X0,X1,X2,X3] :
( ( X1 = k1_xboole_0
& X0 != k1_xboole_0 )
| ( v1_funct_1(X3)
& v1_funct_2(X3,X0,X2)
& m2_relset_1(X3,X0,X2) )
| ~ r1_tarski(k2_relat_1(X3),X2)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,X0,X1)
| ~ m2_relset_1(X3,X0,X1) ),
inference(ennf_transformation,[],[f1912]) ).
fof(f71956,plain,
! [X0,X1,X2,X3] :
( ( X1 = k1_xboole_0
& X0 != k1_xboole_0 )
| ( v1_funct_1(X3)
& v1_funct_2(X3,X0,X2)
& m2_relset_1(X3,X0,X2) )
| ~ r1_tarski(k2_relat_1(X3),X2)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,X0,X1)
| ~ m2_relset_1(X3,X0,X1) ),
inference(flattening,[],[f71955]) ).
fof(f71967,plain,
! [X0,X1,X2,X3] :
( ( v1_funct_1(X3)
& m2_relset_1(X3,X0,X2) )
| ~ r1_tarski(k2_relat_1(X3),X2)
| ~ v1_funct_1(X3)
| ~ m2_relset_1(X3,X0,X1) ),
inference(ennf_transformation,[],[f1545]) ).
fof(f71968,plain,
! [X0,X1,X2,X3] :
( ( v1_funct_1(X3)
& m2_relset_1(X3,X0,X2) )
| ~ r1_tarski(k2_relat_1(X3),X2)
| ~ v1_funct_1(X3)
| ~ m2_relset_1(X3,X0,X1) ),
inference(flattening,[],[f71967]) ).
fof(f72031,plain,
( ( ~ v1_funct_1(k5_relset_2(sK4,sK6))
| ~ v1_funct_2(k5_relset_2(sK4,sK6),k1_zfmisc_1(sK4),k1_zfmisc_1(k2_relat_1(sK6)))
| ~ m2_relset_1(k5_relset_2(sK4,sK6),k1_zfmisc_1(sK4),k1_zfmisc_1(k2_relat_1(sK6))) )
& m1_subset_1(sK6,k1_zfmisc_1(k2_zfmisc_1(sK4,sK5))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4,sK5,sK6]),skolemize(X0,sK4),skolemize(X1,sK5),skolemize(X2,sK6)],[f71195]) ).
fof(f72051,plain,
! [X0] :
( m1_relset_1(sK26(X0),k1_zfmisc_1(X0),k1_zfmisc_1(X0))
& v1_relat_1(sK26(X0))
& ~ v1_xboole_0(sK26(X0))
& v1_finset_1(sK26(X0)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK26]),skolemize(X1,sK26(X0))],[f58664]) ).
fof(f72135,plain,
! [X0] :
( ( X0 = k1_xboole_0
| ? [X1] : r2_hidden(X1,X0) )
& ( ! [X1] : ~ r2_hidden(X1,X0)
| k1_xboole_0 != X0 ) ),
inference(nnf_transformation,[],[f29]) ).
fof(f72136,plain,
! [X0] :
( ( X0 = k1_xboole_0
| ? [X1] : r2_hidden(X1,X0) )
& ( ! [X2] : ~ r2_hidden(X2,X0)
| k1_xboole_0 != X0 ) ),
inference(rectify,[],[f72135]) ).
fof(f72137,plain,
! [X0] :
( ( X0 = k1_xboole_0
| r2_hidden(sK86(X0),X0) )
& ( ! [X2] : ~ r2_hidden(X2,X0)
| k1_xboole_0 != X0 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK86]),skolemize(X1,sK86(X0))],[f72136]) ).
fof(f72183,plain,
! [X0,X1] :
( ( m1_subset_1(X0,k1_zfmisc_1(X1))
| ~ r1_tarski(X0,X1) )
& ( r1_tarski(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(X1)) ) ),
inference(nnf_transformation,[],[f677]) ).
fof(f72186,plain,
! [X0,X1] :
( ( X1 = k1_zfmisc_1(X0)
| ? [X2] :
( ( ~ r1_tarski(X2,X0)
| ~ r2_hidden(X2,X1) )
& ( r1_tarski(X2,X0)
| r2_hidden(X2,X1) ) ) )
& ( ! [X2] :
( ( r2_hidden(X2,X1)
| ~ r1_tarski(X2,X0) )
& ( r1_tarski(X2,X0)
| ~ r2_hidden(X2,X1) ) )
| k1_zfmisc_1(X0) != X1 ) ),
inference(nnf_transformation,[],[f322]) ).
fof(f72187,plain,
! [X0,X1] :
( ( X1 = k1_zfmisc_1(X0)
| ? [X2] :
( ( ~ r1_tarski(X2,X0)
| ~ r2_hidden(X2,X1) )
& ( r1_tarski(X2,X0)
| r2_hidden(X2,X1) ) ) )
& ( ! [X3] :
( ( r2_hidden(X3,X1)
| ~ r1_tarski(X3,X0) )
& ( r1_tarski(X3,X0)
| ~ r2_hidden(X3,X1) ) )
| k1_zfmisc_1(X0) != X1 ) ),
inference(rectify,[],[f72186]) ).
fof(f72188,plain,
! [X0,X1] :
( ( X1 = k1_zfmisc_1(X0)
| ( ( ~ r1_tarski(sK103(X0,X1),X0)
| ~ r2_hidden(sK103(X0,X1),X1) )
& ( r1_tarski(sK103(X0,X1),X0)
| r2_hidden(sK103(X0,X1),X1) ) ) )
& ( ! [X3] :
( ( r2_hidden(X3,X1)
| ~ r1_tarski(X3,X0) )
& ( r1_tarski(X3,X0)
| ~ r2_hidden(X3,X1) ) )
| k1_zfmisc_1(X0) != X1 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK103]),skolemize(X2,sK103(X0,X1))],[f72187]) ).
fof(f72362,plain,
! [X2,X0,X1] :
( m2_relset_1(k6_relset_2(X0,X1,X2),k1_zfmisc_1(X1),k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X1,X0))) ),
inference(cnf_transformation,[],[f71166]) ).
fof(f72363,plain,
! [X2,X0,X1] :
( v1_funct_2(k6_relset_2(X0,X1,X2),k1_zfmisc_1(X1),k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X1,X0))) ),
inference(cnf_transformation,[],[f71166]) ).
fof(f72364,plain,
! [X2,X0,X1] :
( v1_funct_1(k6_relset_2(X0,X1,X2))
| ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X1,X0))) ),
inference(cnf_transformation,[],[f71166]) ).
fof(f72365,plain,
! [X2,X0,X1] :
( k6_relset_2(X0,X1,X2) = k5_relset_2(X1,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X1,X0))) ),
inference(cnf_transformation,[],[f71167]) ).
fof(f72400,plain,
! [X2,X0,X1] :
( r1_tarski(k2_relat_1(k5_relset_2(X0,X2)),k1_zfmisc_1(k2_relat_1(X2)))
| ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(cnf_transformation,[],[f71194]) ).
fof(f72401,plain,
m1_subset_1(sK6,k1_zfmisc_1(k2_zfmisc_1(sK4,sK5))),
inference(cnf_transformation,[],[f72031]) ).
fof(f72402,plain,
( ~ v1_funct_1(k5_relset_2(sK4,sK6))
| ~ v1_funct_2(k5_relset_2(sK4,sK6),k1_zfmisc_1(sK4),k1_zfmisc_1(k2_relat_1(sK6)))
| ~ m2_relset_1(k5_relset_2(sK4,sK6),k1_zfmisc_1(sK4),k1_zfmisc_1(k2_relat_1(sK6))) ),
inference(cnf_transformation,[],[f72031]) ).
fof(f72528,plain,
! [X0] : m1_relset_1(sK26(X0),k1_zfmisc_1(X0),k1_zfmisc_1(X0)),
inference(cnf_transformation,[],[f72051]) ).
fof(f72868,plain,
k1_xboole_0 = np__0,
inference(cnf_transformation,[],[f5328]) ).
fof(f72918,plain,
! [X2,X0] :
( ~ r2_hidden(X2,X0)
| k1_xboole_0 != X0 ),
inference(cnf_transformation,[],[f72137]) ).
fof(f73161,plain,
! [X0,X1] :
( r1_tarski(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(X1)) ),
inference(cnf_transformation,[],[f72183]) ).
fof(f73170,plain,
! [X3,X0,X1] :
( r2_hidden(X3,X1)
| ~ r1_tarski(X3,X0)
| k1_zfmisc_1(X0) != X1 ),
inference(cnf_transformation,[],[f72188]) ).
fof(f73249,plain,
! [X2,X3,X0,X1] :
( m1_subset_1(k10_relset_1(X0,X1,X2,X3),k1_zfmisc_1(X1))
| ~ m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f71752]) ).
fof(f73454,plain,
! [X0] : k3_tarski(k1_zfmisc_1(X0)) = X0,
inference(cnf_transformation,[],[f424]) ).
fof(f73463,plain,
k1_xboole_0 = k3_tarski(k1_xboole_0),
inference(cnf_transformation,[],[f327]) ).
fof(f73647,plain,
! [X2,X3,X0,X1] :
( k1_xboole_0 = X1
| v1_funct_2(X3,X0,X2)
| ~ r1_tarski(k2_relat_1(X3),X2)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,X0,X1)
| ~ m2_relset_1(X3,X0,X1) ),
inference(cnf_transformation,[],[f71956]) ).
fof(f73659,plain,
! [X2,X3,X0,X1] :
( m2_relset_1(X3,X0,X2)
| ~ r1_tarski(k2_relat_1(X3),X2)
| ~ v1_funct_1(X3)
| ~ m2_relset_1(X3,X0,X1) ),
inference(cnf_transformation,[],[f71968]) ).
fof(f73965,plain,
! [X2,X0] :
( ~ r2_hidden(X2,X0)
| np__0 != X0 ),
inference(definition_unfolding,[],[f72918,f72868]) ).
fof(f74179,plain,
np__0 = k3_tarski(np__0),
inference(definition_unfolding,[],[f73463,f72868,f72868]) ).
fof(f74219,plain,
! [X2,X3,X0,X1] :
( np__0 = X1
| v1_funct_2(X3,X0,X2)
| ~ r1_tarski(k2_relat_1(X3),X2)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,X0,X1)
| ~ m2_relset_1(X3,X0,X1) ),
inference(definition_unfolding,[],[f73647,f72868]) ).
fof(f74308,plain,
! [X2] : ~ r2_hidden(X2,np__0),
inference(equality_resolution,[],[f73965]) ).
fof(f74327,plain,
! [X3,X0] :
( r2_hidden(X3,k1_zfmisc_1(X0))
| ~ r1_tarski(X3,X0) ),
inference(equality_resolution,[],[f73170]) ).
fof(f74635,plain,
! [X2,X3,X0] :
( v1_funct_2(X3,X0,X2)
| ~ r1_tarski(k2_relat_1(X3),X2)
| sP359(X0,X3) ),
inference(cnf_transformation,[],[f74635_D]) ).
fof(f74635_D,definition,
! [X3,X0] :
( ! [X2] :
( v1_funct_2(X3,X0,X2)
| ~ r1_tarski(k2_relat_1(X3),X2) )
<=> ~ sP359(X0,X3) ),
introduced(definition,[new_symbols(definition,[sP359])],[general_splitting_component_introduction]) ).
fof(f74636,plain,
! [X3,X0,X1] :
( np__0 = X1
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,X0,X1)
| ~ m2_relset_1(X3,X0,X1)
| ~ sP359(X0,X3) ),
inference(general_splitting,[],[f74219,f74635_D]) ).
fof(f74649,plain,
! [X2,X3,X0] :
( m2_relset_1(X3,X0,X2)
| ~ r1_tarski(k2_relat_1(X3),X2)
| sP366(X0,X3) ),
inference(cnf_transformation,[],[f74649_D]) ).
fof(f74649_D,definition,
! [X3,X0] :
( ! [X2] :
( m2_relset_1(X3,X0,X2)
| ~ r1_tarski(k2_relat_1(X3),X2) )
<=> ~ sP366(X0,X3) ),
introduced(definition,[new_symbols(definition,[sP366])],[general_splitting_component_introduction]) ).
fof(f74650,plain,
! [X3,X0,X1] :
( ~ v1_funct_1(X3)
| ~ m2_relset_1(X3,X0,X1)
| ~ sP366(X0,X3) ),
inference(general_splitting,[],[f73659,f74649_D]) ).
fof(f74681,definition,
( spl368_1
<=> m1_subset_1(sK6,k1_zfmisc_1(k2_zfmisc_1(sK4,sK5))) ),
introduced(definition,[new_symbols(definition,[spl368_1])],[avatar_definition]) ).
fof(f74683,plain,
( m1_subset_1(sK6,k1_zfmisc_1(k2_zfmisc_1(sK4,sK5)))
| ~ spl368_1 ),
inference(avatar_component_clause,[],[f74681]) ).
fof(f74684,plain,
spl368_1,
inference(avatar_split_clause,[],[f72401,f74681]) ).
fof(f74685,plain,
( m2_relset_1(k6_relset_2(sK5,sK4,sK6),k1_zfmisc_1(sK4),k1_zfmisc_1(sK5))
| ~ spl368_1 ),
inference(resolution,[],[f74683,f72362]) ).
fof(f74686,plain,
( v1_funct_2(k6_relset_2(sK5,sK4,sK6),k1_zfmisc_1(sK4),k1_zfmisc_1(sK5))
| ~ spl368_1 ),
inference(resolution,[],[f74683,f72363]) ).
fof(f74687,plain,
( v1_funct_1(k6_relset_2(sK5,sK4,sK6))
| ~ spl368_1 ),
inference(resolution,[],[f74683,f72364]) ).
fof(f74688,plain,
( k5_relset_2(sK4,sK6) = k6_relset_2(sK5,sK4,sK6)
| ~ spl368_1 ),
inference(resolution,[],[f74683,f72365]) ).
fof(f74695,plain,
( r1_tarski(k2_relat_1(k5_relset_2(sK4,sK6)),k1_zfmisc_1(k2_relat_1(sK6)))
| ~ spl368_1 ),
inference(resolution,[],[f74683,f72400]) ).
fof(f74900,plain,
( v1_funct_1(k5_relset_2(sK4,sK6))
| ~ spl368_1 ),
inference(forward_demodulation,[],[f74687,f74688]) ).
fof(f74901,plain,
( v1_funct_2(k5_relset_2(sK4,sK6),k1_zfmisc_1(sK4),k1_zfmisc_1(sK5))
| ~ spl368_1 ),
inference(forward_demodulation,[],[f74686,f74688]) ).
fof(f74902,plain,
( m2_relset_1(k5_relset_2(sK4,sK6),k1_zfmisc_1(sK4),k1_zfmisc_1(sK5))
| ~ spl368_1 ),
inference(forward_demodulation,[],[f74685,f74688]) ).
fof(f74911,plain,
( ~ v1_funct_2(k5_relset_2(sK4,sK6),k1_zfmisc_1(sK4),k1_zfmisc_1(k2_relat_1(sK6)))
| ~ m2_relset_1(k5_relset_2(sK4,sK6),k1_zfmisc_1(sK4),k1_zfmisc_1(k2_relat_1(sK6)))
| ~ spl368_1 ),
inference(backward_subsumption_resolution,[],[f72402,f74900]) ).
fof(f74921,definition,
( spl368_3
<=> v1_funct_2(k5_relset_2(sK4,sK6),k1_zfmisc_1(sK4),k1_zfmisc_1(sK5)) ),
introduced(definition,[new_symbols(definition,[spl368_3])],[avatar_definition]) ).
fof(f74923,plain,
( v1_funct_2(k5_relset_2(sK4,sK6),k1_zfmisc_1(sK4),k1_zfmisc_1(sK5))
| ~ spl368_3 ),
inference(avatar_component_clause,[],[f74921]) ).
fof(f74924,plain,
( spl368_3
| ~ spl368_1 ),
inference(avatar_split_clause,[],[f74901,f74681,f74921]) ).
fof(f74926,definition,
( spl368_4
<=> m2_relset_1(k5_relset_2(sK4,sK6),k1_zfmisc_1(sK4),k1_zfmisc_1(sK5)) ),
introduced(definition,[new_symbols(definition,[spl368_4])],[avatar_definition]) ).
fof(f74928,plain,
( m2_relset_1(k5_relset_2(sK4,sK6),k1_zfmisc_1(sK4),k1_zfmisc_1(sK5))
| ~ spl368_4 ),
inference(avatar_component_clause,[],[f74926]) ).
fof(f74929,plain,
( spl368_4
| ~ spl368_1 ),
inference(avatar_split_clause,[],[f74902,f74681,f74926]) ).
fof(f74931,definition,
( spl368_5
<=> m2_relset_1(k5_relset_2(sK4,sK6),k1_zfmisc_1(sK4),k1_zfmisc_1(k2_relat_1(sK6))) ),
introduced(definition,[new_symbols(definition,[spl368_5])],[avatar_definition]) ).
fof(f74933,plain,
( ~ m2_relset_1(k5_relset_2(sK4,sK6),k1_zfmisc_1(sK4),k1_zfmisc_1(k2_relat_1(sK6)))
| spl368_5 ),
inference(avatar_component_clause,[],[f74931]) ).
fof(f74935,definition,
( spl368_6
<=> v1_funct_2(k5_relset_2(sK4,sK6),k1_zfmisc_1(sK4),k1_zfmisc_1(k2_relat_1(sK6))) ),
introduced(definition,[new_symbols(definition,[spl368_6])],[avatar_definition]) ).
fof(f74937,plain,
( ~ v1_funct_2(k5_relset_2(sK4,sK6),k1_zfmisc_1(sK4),k1_zfmisc_1(k2_relat_1(sK6)))
| spl368_6 ),
inference(avatar_component_clause,[],[f74935]) ).
fof(f74938,plain,
( ~ spl368_5
| ~ spl368_6
| ~ spl368_1 ),
inference(avatar_split_clause,[],[f74911,f74681,f74935,f74931]) ).
fof(f74955,plain,
( ~ r1_tarski(k2_relat_1(k5_relset_2(sK4,sK6)),k1_zfmisc_1(k2_relat_1(sK6)))
| sP366(k1_zfmisc_1(sK4),k5_relset_2(sK4,sK6))
| spl368_5 ),
inference(resolution,[],[f74933,f74649]) ).
fof(f74997,plain,
( sP366(k1_zfmisc_1(sK4),k5_relset_2(sK4,sK6))
| ~ spl368_1
| spl368_5 ),
inference(forward_subsumption_resolution,[],[f74955,f74695]) ).
fof(f75102,plain,
( np__0 = k1_zfmisc_1(sK5)
| ~ v1_funct_1(k5_relset_2(sK4,sK6))
| ~ v1_funct_2(k5_relset_2(sK4,sK6),k1_zfmisc_1(sK4),k1_zfmisc_1(sK5))
| ~ sP359(k1_zfmisc_1(sK4),k5_relset_2(sK4,sK6))
| ~ spl368_4 ),
inference(resolution,[],[f74928,f74636]) ).
fof(f75105,plain,
( ~ v1_funct_1(k5_relset_2(sK4,sK6))
| ~ sP366(k1_zfmisc_1(sK4),k5_relset_2(sK4,sK6))
| ~ spl368_4 ),
inference(resolution,[],[f74928,f74650]) ).
fof(f75117,plain,
( ~ sP366(k1_zfmisc_1(sK4),k5_relset_2(sK4,sK6))
| ~ spl368_1
| ~ spl368_4 ),
inference(forward_subsumption_resolution,[],[f75105,f74900]) ).
fof(f75120,plain,
( np__0 = k1_zfmisc_1(sK5)
| ~ v1_funct_2(k5_relset_2(sK4,sK6),k1_zfmisc_1(sK4),k1_zfmisc_1(sK5))
| ~ sP359(k1_zfmisc_1(sK4),k5_relset_2(sK4,sK6))
| ~ spl368_1
| ~ spl368_4 ),
inference(forward_subsumption_resolution,[],[f75102,f74900]) ).
fof(f75197,plain,
( $false
| ~ spl368_1
| ~ spl368_4
| spl368_5 ),
inference(forward_subsumption_resolution,[],[f75117,f74997]) ).
fof(f75198,plain,
( ~ spl368_1
| ~ spl368_4
| spl368_5 ),
inference(avatar_contradiction_clause,[],[f75197]) ).
fof(f75201,plain,
( np__0 = k1_zfmisc_1(sK5)
| ~ sP359(k1_zfmisc_1(sK4),k5_relset_2(sK4,sK6))
| ~ spl368_1
| ~ spl368_3
| ~ spl368_4 ),
inference(forward_subsumption_resolution,[],[f75120,f74923]) ).
fof(f75431,plain,
( ~ r1_tarski(k2_relat_1(k5_relset_2(sK4,sK6)),k1_zfmisc_1(k2_relat_1(sK6)))
| sP359(k1_zfmisc_1(sK4),k5_relset_2(sK4,sK6))
| spl368_6 ),
inference(resolution,[],[f74937,f74635]) ).
fof(f75471,plain,
( sP359(k1_zfmisc_1(sK4),k5_relset_2(sK4,sK6))
| ~ spl368_1
| spl368_6 ),
inference(forward_subsumption_resolution,[],[f75431,f74695]) ).
fof(f75476,plain,
( np__0 = k1_zfmisc_1(sK5)
| ~ spl368_1
| ~ spl368_3
| ~ spl368_4
| spl368_6 ),
inference(backward_subsumption_resolution,[],[f75201,f75471]) ).
fof(f75826,definition,
( spl368_7
<=> np__0 = k1_zfmisc_1(sK5) ),
introduced(definition,[new_symbols(definition,[spl368_7])],[avatar_definition]) ).
fof(f75828,plain,
( np__0 = k1_zfmisc_1(sK5)
| ~ spl368_7 ),
inference(avatar_component_clause,[],[f75826]) ).
fof(f75829,plain,
( spl368_7
| ~ spl368_1
| ~ spl368_3
| ~ spl368_4
| spl368_6 ),
inference(avatar_split_clause,[],[f75476,f74935,f74926,f74921,f74681,f75826]) ).
fof(f76605,plain,
( m1_relset_1(sK26(sK5),np__0,np__0)
| ~ spl368_7 ),
inference(superposition,[],[f72528,f75828]) ).
fof(f76637,plain,
( ! [X0] :
( ~ m1_subset_1(X0,np__0)
| r1_tarski(X0,sK5) )
| ~ spl368_7 ),
inference(superposition,[],[f73161,f75828]) ).
fof(f76689,plain,
( ! [X2,X0,X1] :
( m1_subset_1(k10_relset_1(X0,sK5,X1,X2),np__0)
| ~ m1_relset_1(X1,X0,sK5) )
| ~ spl368_7 ),
inference(superposition,[],[f73249,f75828]) ).
fof(f76701,plain,
( sK5 = k3_tarski(np__0)
| ~ spl368_7 ),
inference(superposition,[],[f73454,f75828]) ).
fof(f76757,plain,
( ! [X0] :
( r2_hidden(X0,np__0)
| ~ r1_tarski(X0,sK5) )
| ~ spl368_7 ),
inference(superposition,[],[f74327,f75828]) ).
fof(f76857,plain,
( ! [X0] : ~ r1_tarski(X0,sK5)
| ~ spl368_7 ),
inference(forward_subsumption_resolution,[],[f76757,f74308]) ).
fof(f76894,plain,
( np__0 = sK5
| ~ spl368_7 ),
inference(forward_demodulation,[],[f76701,f74179]) ).
fof(f76945,plain,
( ! [X0] : ~ m1_subset_1(X0,np__0)
| ~ spl368_7 ),
inference(backward_subsumption_resolution,[],[f76637,f76857]) ).
fof(f77008,plain,
( ! [X0,X1] : ~ m1_relset_1(X1,X0,sK5)
| ~ spl368_7 ),
inference(backward_subsumption_resolution,[],[f76689,f76945]) ).
fof(f77071,plain,
( ! [X0,X1] : ~ m1_relset_1(X1,X0,np__0)
| ~ spl368_7 ),
inference(forward_demodulation,[],[f77008,f76894]) ).
fof(f77086,plain,
( $false
| ~ spl368_7 ),
inference(backward_subsumption_resolution,[],[f76605,f77071]) ).
fof(f77087,plain,
~ spl368_7,
inference(avatar_contradiction_clause,[],[f77086]) ).
cnf(s1,plain,
spl368_1,
inference(sat_conversion,[],[f74684]) ).
cnf(s3,plain,
( ~ spl368_1
| spl368_3 ),
inference(sat_conversion,[],[f74924]) ).
cnf(s4,plain,
( ~ spl368_1
| spl368_4 ),
inference(sat_conversion,[],[f74929]) ).
cnf(s5,plain,
( ~ spl368_1
| ~ spl368_5
| ~ spl368_6 ),
inference(sat_conversion,[],[f74938]) ).
cnf(s7,plain,
( ~ spl368_1
| ~ spl368_4
| spl368_5 ),
inference(sat_conversion,[],[f75198]) ).
cnf(s8,plain,
( ~ spl368_1
| ~ spl368_3
| ~ spl368_4
| spl368_6
| spl368_7 ),
inference(sat_conversion,[],[f75829]) ).
cnf(s14,plain,
~ spl368_7,
inference(sat_conversion,[],[f77087]) ).
cnf(s15,plain,
( ~ spl368_1
| ~ spl368_3
| ~ spl368_4
| spl368_6 ),
inference(rat,[],[s8,s14]) ).
cnf(s17,plain,
spl368_4,
inference(rat,[],[s4,s1]) ).
cnf(s18,plain,
spl368_3,
inference(rat,[],[s3,s1]) ).
cnf(s20,plain,
spl368_5,
inference(rat,[],[s7,s1,s17]) ).
cnf(s21,plain,
spl368_6,
inference(rat,[],[s15,s17,s1,s18]) ).
cnf(s22,plain,
$false,
inference(rat,[],[s5,s1,s21,s20]) ).
fof(f77099,plain,
$false,
inference(avatar_sat_refutation,[],[s22]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU425+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.37 % Computer : n020.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Mon Sep 28 05:22:36 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.41 Running first-order theorem proving
% 0.11/0.41 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 22.49/8.93 % (4053351)Detected formulas, will run a generic FOF schedule.
% 22.49/8.93 % (4053357)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=611606097:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2943 on theBenchmark for (2943ds/134677Mi)
% 22.49/8.93 % (4053356)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=2802714924:i=141193_2943 on theBenchmark for (2943ds/141193Mi)
% 22.49/8.93 % (4053358)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=94379676:i=141695:sd=1:nm=32:gsp=on:ss=included_2943 on theBenchmark for (2943ds/141695Mi)
% 22.49/8.93 % (4053361)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1974620780:s2a=on:i=139:gtg=position_2943 on theBenchmark for (2943ds/139Mi)
% 22.49/8.93 % (4053360)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2954058878:i=119:av=off:ss=axioms_2943 on theBenchmark for (2943ds/119Mi)
% 22.49/8.93 % (4053359)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1773821121:i=109:sd=1:ins=1:gsp=on:ss=axioms_2943 on theBenchmark for (2943ds/109Mi)
% 22.49/8.93 % (4053362)dis-21_1_sil=8000:lcm=predicate:random_seed=399230903:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2943 on theBenchmark for (2943ds/129Mi)
% 22.49/8.93 % (4053361)Instruction limit reached!
% 22.49/8.93 % (4053361)------------------------------
% 22.49/8.93 % (4053361)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.49/8.93 % (4053361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.49/8.93 % (4053361)CaDiCaL version: 2.1.3
% 22.49/8.93 % (4053361)Termination reason: Instruction limit
% 22.49/8.93 % (4053361)Termination phase: Property scanning
% 22.49/8.93 % (4053361)Time elapsed: 0.069 s
% 22.49/8.93 % (4053361)Peak memory usage: 201 MB
% 22.49/8.93 % (4053361)Instructions burned: 141 (million)
% 22.49/8.93 % (4053359)Instruction limit reached!
% 22.49/8.93 % (4053359)------------------------------
% 22.49/8.93 % (4053359)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.49/8.93 % (4053359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.49/8.93 % (4053359)CaDiCaL version: 2.1.3
% 22.49/8.93 % (4053359)Termination reason: Instruction limit
% 22.49/8.93 % (4053359)Termination phase: SInE selection
% 22.49/8.93 % (4053359)Time elapsed: 0.084 s
% 22.49/8.93 % (4053359)Peak memory usage: 201 MB
% 22.49/8.93 % (4053359)Instructions burned: 109 (million)
% 22.49/8.93 % (4053360)Instruction limit reached!
% 22.49/8.93 % (4053360)------------------------------
% 22.49/8.93 % (4053360)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.49/8.93 % (4053360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.49/8.93 % (4053360)CaDiCaL version: 2.1.3
% 22.49/8.93 % (4053360)Termination reason: Instruction limit
% 22.49/8.93 % (4053360)Termination phase: SInE selection
% 22.49/8.93 % (4053360)Time elapsed: 0.097 s
% 22.49/8.93 % (4053360)Peak memory usage: 200 MB
% 22.49/8.93 % (4053360)Instructions burned: 124 (million)
% 22.49/8.93 % (4053362)Instruction limit reached!
% 22.49/8.93 % (4053362)------------------------------
% 22.49/8.93 % (4053362)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.49/8.93 % (4053362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.49/8.93 % (4053362)CaDiCaL version: 2.1.3
% 22.49/8.93 % (4053362)Termination reason: Instruction limit
% 22.49/8.93 % (4053362)Termination phase: SInE selection
% 22.49/8.93 % (4053362)Time elapsed: 0.103 s
% 22.49/8.93 % (4053362)Peak memory usage: 201 MB
% 22.49/8.93 % (4053362)Instructions burned: 129 (million)
% 22.49/8.93 % (4053370)lrs+10_1_sil=8000:sp=occurrence:random_seed=3359108339:i=285:sd=3:ss=axioms:sgt=8_2941 on theBenchmark for (2941ds/285Mi)
% 22.49/8.93 % (4053371)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2202722706:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2941 on theBenchmark for (2941ds/157Mi)
% 22.49/8.93 % (4053372)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2337339051:i=325:sd=1:ss=axioms:sgt=32_2941 on theBenchmark for (2941ds/325Mi)
% 22.49/8.93 % (4053371)Instruction limit reached!
% 22.49/8.93 % (4053371)------------------------------
% 22.49/8.93 % (4053371)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.49/8.93 % (4053371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.17/9.23 % (4053371)CaDiCaL version: 2.1.3
% 15.17/9.23 % (4053371)Termination reason: Instruction limit
% 15.17/9.23 % (4053371)Termination phase: Property scanning
% 15.17/9.23 % (4053371)Time elapsed: 0.075 s
% 15.17/9.23 % (4053371)Peak memory usage: 201 MB
% 15.17/9.23 % (4053371)Instructions burned: 158 (million)
% 15.17/9.23 % (4053373)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=763529479:s2a=on:i=248:s2at=1.23:gtg=position_2940 on theBenchmark for (2940ds/248Mi)
% 15.17/9.23 % (4053373)Instruction limit reached!
% 15.17/9.23 % (4053373)------------------------------
% 15.17/9.23 % (4053373)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.17/9.23 % (4053373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.17/9.23 % (4053373)CaDiCaL version: 2.1.3
% 15.17/9.23 % (4053373)Termination reason: Instruction limit
% 15.17/9.23 % (4053373)Termination phase: Property scanning
% 15.17/9.23 % (4053373)Time elapsed: 0.113 s
% 15.17/9.23 % (4053373)Peak memory usage: 201 MB
% 15.17/9.23 % (4053373)Instructions burned: 248 (million)
% 15.17/9.23 % (4053370)Instruction limit reached!
% 15.17/9.23 % (4053370)------------------------------
% 15.17/9.23 % (4053370)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.17/9.23 % (4053370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.17/9.23 % (4053370)CaDiCaL version: 2.1.3
% 15.17/9.23 % (4053370)Termination reason: Instruction limit
% 15.17/9.23 % (4053370)Termination phase: SInE selection
% 15.17/9.23 % (4053370)Time elapsed: 0.207 s
% 15.17/9.23 % (4053370)Peak memory usage: 201 MB
% 15.17/9.23 % (4053370)Instructions burned: 286 (million)
% 15.17/9.23 % (4053378)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=678333756:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2938 on theBenchmark for (2938ds/294Mi)
% 15.17/9.23 % (4053372)Instruction limit reached!
% 15.17/9.23 % (4053372)------------------------------
% 15.17/9.23 % (4053372)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.17/9.23 % (4053372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.17/9.23 % (4053372)CaDiCaL version: 2.1.3
% 15.17/9.23 % (4053372)Termination reason: Instruction limit
% 15.17/9.23 % (4053372)Termination phase: SInE selection
% 15.17/9.23 % (4053372)Time elapsed: 0.241 s
% 15.17/9.23 % (4053372)Peak memory usage: 201 MB
% 15.17/9.23 % (4053372)Instructions burned: 325 (million)
% 15.17/9.23 % (4053380)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3982114595:cts=off:i=113:fsr=off:ss=included:sgt=4_2937 on theBenchmark for (2937ds/113Mi)
% 15.17/9.23 % (4053379)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=267272604:i=2350_2937 on theBenchmark for (2937ds/2350Mi)
% 15.17/9.23 % (4053382)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3583019103:i=127:av=off:fsr=off:sup=off_2937 on theBenchmark for (2937ds/127Mi)
% 15.17/9.23 % (4053380)Instruction limit reached!
% 15.17/9.23 % (4053380)------------------------------
% 15.17/9.23 % (4053380)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.17/9.23 % (4053380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.17/9.23 % (4053380)CaDiCaL version: 2.1.3
% 15.17/9.23 % (4053380)Termination reason: Instruction limit
% 15.17/9.23 % (4053380)Termination phase: SInE selection
% 15.17/9.23 % (4053380)Time elapsed: 0.086 s
% 15.17/9.23 % (4053380)Peak memory usage: 201 MB
% 15.17/9.23 % (4053380)Instructions burned: 113 (million)
% 15.17/9.23 % (4053378)Instruction limit reached!
% 15.17/9.23 % (4053378)------------------------------
% 15.17/9.23 % (4053378)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.17/9.23 % (4053378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.17/9.23 % (4053378)CaDiCaL version: 2.1.3
% 15.17/9.23 % (4053378)Termination reason: Instruction limit
% 15.17/9.23 % (4053378)Termination phase: SInE selection
% 15.17/9.23 % (4053378)Time elapsed: 0.217 s
% 15.17/9.23 % (4053378)Peak memory usage: 201 MB
% 15.17/9.23 % (4053378)Instructions burned: 295 (million)
% 15.17/9.23 % (4053382)Instruction limit reached!
% 15.17/9.23 % (4053382)------------------------------
% 15.17/9.23 % (4053382)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.17/9.23 % (4053382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.17/9.23 % (4053382)CaDiCaL version: 2.1.3
% 15.17/9.23 % (4053382)Termination reason: Instruction limit
% 15.17/9.23 % (4053382)Termination phase: Preprocessing 1
% 15.17/9.23 % (4053382)Time elapsed: 0.101 s
% 15.17/9.23 % (4053382)Peak memory usage: 202 MB
% 15.17/9.23 % (4053382)Instructions burned: 127 (million)
% 15.17/9.23 % (4053386)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2648042078:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2935 on theBenchmark for (2935ds/114Mi)
% 15.17/9.23 % (4053387)lrs+10_1_sil=8000:sp=occurrence:random_seed=3914111339:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2935 on theBenchmark for (2935ds/907Mi)
% 15.17/9.23 % (4053386)Instruction limit reached!
% 15.17/9.23 % (4053386)------------------------------
% 15.17/9.23 % (4053386)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.17/9.23 % (4053386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.17/9.23 % (4053386)CaDiCaL version: 2.1.3
% 15.17/9.23 % (4053386)Termination reason: Instruction limit
% 15.17/9.23 % (4053386)Termination phase: Property scanning
% 15.17/9.23 % (4053386)Time elapsed: 0.057 s
% 15.17/9.23 % (4053386)Peak memory usage: 201 MB
% 15.17/9.23 % (4053386)Instructions burned: 114 (million)
% 15.17/9.23 % (4053388)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3066049922:i=437:sd=1:aac=none:ss=included_2934 on theBenchmark for (2934ds/437Mi)
% 15.17/9.23 % (4053391)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2810395871:i=5202:ss=axioms:sgt=16_2932 on theBenchmark for (2932ds/5202Mi)
% 15.17/9.23 % (4053388)Instruction limit reached!
% 15.17/9.23 % (4053388)------------------------------
% 15.17/9.23 % (4053388)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.17/9.23 % (4053388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.17/9.23 % (4053388)CaDiCaL version: 2.1.3
% 15.17/9.23 % (4053388)Termination reason: Instruction limit
% 15.17/9.23 % (4053388)Termination phase: SInE selection
% 15.17/9.23 % (4053388)Time elapsed: 0.329 s
% 15.17/9.23 % (4053388)Peak memory usage: 202 MB
% 15.17/9.23 % (4053388)Instructions burned: 437 (million)
% 15.17/9.23 % (4053394)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2590782732:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2929 on theBenchmark for (2929ds/134Mi)
% 15.17/9.23 % (4053387)Instruction limit reached!
% 15.17/9.23 % (4053387)------------------------------
% 15.17/9.23 % (4053387)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.17/9.23 % (4053387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.17/9.23 % (4053387)CaDiCaL version: 2.1.3
% 15.17/9.23 % (4053387)Termination reason: Instruction limit
% 15.17/9.23 % (4053387)Termination phase: Preprocessing 2
% 15.17/9.23 % (4053387)Time elapsed: 0.677 s
% 15.17/9.23 % (4053387)Peak memory usage: 208 MB
% 15.17/9.23 % (4053387)Instructions burned: 907 (million)
% 15.17/9.23 % (4053394)Instruction limit reached!
% 15.17/9.23 % (4053394)------------------------------
% 15.17/9.23 % (4053394)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.17/9.23 % (4053394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.17/9.23 % (4053394)CaDiCaL version: 2.1.3
% 15.17/9.23 % (4053394)Termination reason: Instruction limit
% 15.17/9.23 % (4053394)Termination phase: SInE selection
% 15.17/9.23 % (4053394)Time elapsed: 0.102 s
% 15.17/9.23 % (4053394)Peak memory usage: 201 MB
% 15.17/9.23 % (4053394)Instructions burned: 135 (million)
% 15.17/9.23 % (4053396)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1224887681:st=8:i=592:sd=3:ep=RST:ss=axioms_2926 on theBenchmark for (2926ds/592Mi)
% 15.17/9.23 % (4053397)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2685808265:st=3:i=13193:sd=3:ss=axioms_2926 on theBenchmark for (2926ds/13193Mi)
% 15.17/9.23 % (4053396)Instruction limit reached!
% 15.17/9.23 % (4053396)------------------------------
% 15.17/9.23 % (4053396)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.17/9.23 % (4053396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.17/9.23 % (4053396)CaDiCaL version: 2.1.3
% 15.17/9.23 % (4053396)Termination reason: Instruction limit
% 15.17/9.23 % (4053396)Termination phase: SInE selection
% 15.17/9.23 % (4053396)Time elapsed: 0.379 s
% 15.17/9.23 % (4053396)Peak memory usage: 203 MB
% 15.17/9.23 % (4053396)Instructions burned: 594 (million)
% 15.17/9.23 % (4053358)First to succeed.
% 15.17/9.23 % (4053358)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-4053351"
% 15.17/9.23 % (4053400)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=2629137375:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2920 on theBenchmark for (2920ds/125Mi)
% 15.17/9.23 % (4053400)Instruction limit reached!
% 15.17/9.23 % (4053400)------------------------------
% 15.17/9.23 % (4053400)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.17/9.23 % (4053400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.17/9.23 % (4053400)CaDiCaL version: 2.1.3
% 15.17/9.23 % (4053400)Termination reason: Instruction limit
% 15.17/9.23 % (4053400)Termination phase: Property scanning
% 15.17/9.23 % (4053400)Time elapsed: 0.062 s
% 15.17/9.23 % (4053400)Peak memory usage: 201 MB
% 15.17/9.23 % (4053400)Instructions burned: 126 (million)
% 15.17/9.23 % (4053379)Instruction limit reached!
% 15.17/9.23 % (4053379)------------------------------
% 15.17/9.23 % (4053379)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.17/9.23 % (4053379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.17/9.23 % (4053379)CaDiCaL version: 2.1.3
% 15.17/9.23 % (4053379)Termination reason: Instruction limit
% 15.17/9.23 % (4053379)Termination phase: Preprocessing 3
% 15.17/9.23 % (4053379)Time elapsed: 1.903 s
% 15.17/9.23 % (4053379)Peak memory usage: 305 MB
% 15.17/9.23 % (4053379)Instructions burned: 2351 (million)
% 15.17/9.23 % (4053402)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=843684313:i=134:gtgl=5:slsql=off:gtg=exists_sym_2918 on theBenchmark for (2918ds/134Mi)
% 15.17/9.23 % (4053358)Refutation found. Thanks to Tanya!
% 15.17/9.23 % SZS status Theorem for theBenchmark
% 15.17/9.23 % SZS output start Proof for theBenchmark
% See solution above
% 25.63/9.48 % (4053358)------------------------------
% 25.63/9.48 % (4053358)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.63/9.48 % (4053358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.63/9.48 % (4053358)CaDiCaL version: 2.1.3
% 25.63/9.48 % (4053358)Termination reason: Refutation
% 25.63/9.48 % (4053358)Time elapsed: 2.243 s
% 25.63/9.48 % (4053358)Peak memory usage: 271 MB
% 25.63/9.48 % (4053358)Instructions burned: 3269 (million)
% 25.63/9.48 % (4053358)------------------------------
% 25.63/9.48 % (4053358)------------------------------
% 25.63/9.48 % (4053351)Success in time 8.372 s
% 25.63/9.48 % Vampire exiting
%------------------------------------------------------------------------------