%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU421+3 : 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:54 PM UTC 2026
% Result : Theorem 101.51s 28.88s
% Output : Refutation 192.55s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 30
% Syntax : Number of formulae : 195 ( 41 unt; 19 def)
% Number of atoms : 845 ( 78 equ)
% Maximal formula atoms : 15 ( 4 avg)
% Number of connectives : 1169 ( 519 ~; 529 |; 80 &)
% ( 27 <=>; 14 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 19 ( 17 usr; 14 prp; 0-2 aty)
% Number of functors : 26 ( 26 usr; 9 con; 0-4 aty)
% Number of variables : 329 ( 0 sgn 299 !; 30 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f8,axiom,
! [X0,X1] :
( r1_tarski(X0,X1)
<=> ! [X2] :
( r2_hidden(X2,X0)
=> r2_hidden(X2,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d3_tarski) ).
fof(f9,axiom,
! [X0,X1] :
( X1 = k3_tarski(X0)
<=> ! [X2] :
( r2_hidden(X2,X1)
<=> ? [X3] :
( r2_hidden(X2,X3)
& r2_hidden(X3,X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d4_tarski) ).
fof(f38,axiom,
! [X0,X1] :
( X0 = X1
<=> ( r1_tarski(X0,X1)
& r1_tarski(X1,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d10_xboole_0) ).
fof(f419,axiom,
! [X0,X1] :
( ! [X2] :
( r2_hidden(X2,X0)
=> r1_tarski(X2,X1) )
=> r1_tarski(k3_tarski(X0),X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t94_zfmisc_1) ).
fof(f669,axiom,
! [X0,X1] :
( m1_subset_1(X1,k1_zfmisc_1(k1_zfmisc_1(X0)))
=> k5_setfam_1(X0,X1) = k3_tarski(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k5_setfam_1) ).
fof(f678,axiom,
! [X0,X1,X2] :
( ( r2_hidden(X0,X1)
& m1_subset_1(X1,k1_zfmisc_1(X2)) )
=> m1_subset_1(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t4_subset) ).
fof(f849,axiom,
! [X0] :
( v1_relat_1(X0)
=> ! [X1,X2] :
( X2 = k9_relat_1(X0,X1)
<=> ! [X3] :
( r2_hidden(X3,X2)
<=> ? [X4] :
( r2_hidden(k4_tarski(X4,X3),X0)
& r2_hidden(X4,X1) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d13_relat_1) ).
fof(f852,axiom,
! [X0,X1,X2] :
( v1_relat_1(X2)
=> ( r2_hidden(X0,k9_relat_1(X2,X1))
<=> ? [X3] :
( r2_hidden(X3,k1_relat_1(X2))
& r2_hidden(k4_tarski(X3,X0),X2)
& r2_hidden(X3,X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t143_relat_1) ).
fof(f865,axiom,
! [X0,X1,X2] :
( v1_relat_1(X2)
=> ( r1_tarski(X0,X1)
=> r1_tarski(k9_relat_1(X2,X0),k9_relat_1(X2,X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t156_relat_1) ).
fof(f19052,axiom,
! [X0,X1,X2,X3] :
( ( m1_subset_1(X2,k1_zfmisc_1(k1_zfmisc_1(X1)))
& v1_relat_1(X3) )
=> ( r2_hidden(X0,a_3_0_relset_2(X1,X2,X3))
<=> ? [X4] :
( m1_subset_1(X4,k1_zfmisc_1(X1))
& X0 = k9_relat_1(X3,X4)
& r2_hidden(X4,X2) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fraenkel_a_3_0_relset_2) ).
fof(f19084,conjecture,
! [X0,X1] :
( m1_subset_1(X1,k1_zfmisc_1(k1_zfmisc_1(X0)))
=> ! [X2] :
( v1_relat_1(X2)
=> k9_relat_1(X2,k5_setfam_1(X0,X1)) = k3_tarski(a_3_0_relset_2(X0,X1,X2)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t14_relset_2) ).
fof(f19085,negated_conjecture,
~ ! [X0,X1] :
( m1_subset_1(X1,k1_zfmisc_1(k1_zfmisc_1(X0)))
=> ! [X2] :
( v1_relat_1(X2)
=> k9_relat_1(X2,k5_setfam_1(X0,X1)) = k3_tarski(a_3_0_relset_2(X0,X1,X2)) ) ),
inference(negated_conjecture,[status(cth)],[f19084]) ).
fof(f19118,plain,
? [X0,X1] :
( ? [X2] :
( k9_relat_1(X2,k5_setfam_1(X0,X1)) != k3_tarski(a_3_0_relset_2(X0,X1,X2))
& v1_relat_1(X2) )
& m1_subset_1(X1,k1_zfmisc_1(k1_zfmisc_1(X0))) ),
inference(ennf_transformation,[],[f19085]) ).
fof(f19134,plain,
! [X0,X1] :
( r1_tarski(k3_tarski(X0),X1)
| ? [X2] :
( ~ r1_tarski(X2,X1)
& r2_hidden(X2,X0) ) ),
inference(ennf_transformation,[],[f419]) ).
fof(f19155,plain,
! [X0,X1] :
( k5_setfam_1(X0,X1) = k3_tarski(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(k1_zfmisc_1(X0))) ),
inference(ennf_transformation,[],[f669]) ).
fof(f19210,plain,
! [X0,X1,X2] :
( r1_tarski(k9_relat_1(X2,X0),k9_relat_1(X2,X1))
| ~ r1_tarski(X0,X1)
| ~ v1_relat_1(X2) ),
inference(ennf_transformation,[],[f865]) ).
fof(f19211,plain,
! [X0,X1,X2] :
( r1_tarski(k9_relat_1(X2,X0),k9_relat_1(X2,X1))
| ~ r1_tarski(X0,X1)
| ~ v1_relat_1(X2) ),
inference(flattening,[],[f19210]) ).
fof(f19224,plain,
! [X0,X1,X2] :
( ( r2_hidden(X0,k9_relat_1(X2,X1))
<=> ? [X3] :
( r2_hidden(X3,k1_relat_1(X2))
& r2_hidden(k4_tarski(X3,X0),X2)
& r2_hidden(X3,X1) ) )
| ~ v1_relat_1(X2) ),
inference(ennf_transformation,[],[f852]) ).
fof(f19225,plain,
! [X0] :
( ! [X1,X2] :
( X2 = k9_relat_1(X0,X1)
<=> ! [X3] :
( r2_hidden(X3,X2)
<=> ? [X4] :
( r2_hidden(k4_tarski(X4,X3),X0)
& r2_hidden(X4,X1) ) ) )
| ~ v1_relat_1(X0) ),
inference(ennf_transformation,[],[f849]) ).
fof(f19226,plain,
! [X0,X1,X2,X3] :
( ( r2_hidden(X0,a_3_0_relset_2(X1,X2,X3))
<=> ? [X4] :
( m1_subset_1(X4,k1_zfmisc_1(X1))
& X0 = k9_relat_1(X3,X4)
& r2_hidden(X4,X2) ) )
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_zfmisc_1(X1)))
| ~ v1_relat_1(X3) ),
inference(ennf_transformation,[],[f19052]) ).
fof(f19227,plain,
! [X0,X1,X2,X3] :
( ( r2_hidden(X0,a_3_0_relset_2(X1,X2,X3))
<=> ? [X4] :
( m1_subset_1(X4,k1_zfmisc_1(X1))
& X0 = k9_relat_1(X3,X4)
& r2_hidden(X4,X2) ) )
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_zfmisc_1(X1)))
| ~ v1_relat_1(X3) ),
inference(flattening,[],[f19226]) ).
fof(f19257,plain,
! [X0,X1,X2] :
( m1_subset_1(X0,X2)
| ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2)) ),
inference(ennf_transformation,[],[f678]) ).
fof(f19258,plain,
! [X0,X1,X2] :
( m1_subset_1(X0,X2)
| ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2)) ),
inference(flattening,[],[f19257]) ).
fof(f19354,plain,
! [X0,X1] :
( r1_tarski(X0,X1)
<=> ! [X2] :
( r2_hidden(X2,X1)
| ~ r2_hidden(X2,X0) ) ),
inference(ennf_transformation,[],[f8]) ).
fof(f20443,plain,
( k9_relat_1(sK33,k5_setfam_1(sK31,sK32)) != k3_tarski(a_3_0_relset_2(sK31,sK32,sK33))
& v1_relat_1(sK33)
& m1_subset_1(sK32,k1_zfmisc_1(k1_zfmisc_1(sK31))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK31,sK32,sK33]),skolemize(X0,sK31),skolemize(X1,sK32),skolemize(X2,sK33)],[f19118]) ).
fof(f20453,plain,
! [X0,X1] :
( r1_tarski(k3_tarski(X0),X1)
| ( ~ r1_tarski(sK41(X0,X1),X1)
& r2_hidden(sK41(X0,X1),X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK41]),skolemize(X2,sK41(X0,X1))],[f19134]) ).
fof(f20454,plain,
! [X0,X1] :
( ( X1 = k3_tarski(X0)
| ? [X2] :
( ( ! [X3] :
( ~ r2_hidden(X2,X3)
| ~ r2_hidden(X3,X0) )
| ~ r2_hidden(X2,X1) )
& ( ? [X3] :
( r2_hidden(X2,X3)
& r2_hidden(X3,X0) )
| r2_hidden(X2,X1) ) ) )
& ( ! [X2] :
( ( r2_hidden(X2,X1)
| ! [X3] :
( ~ r2_hidden(X2,X3)
| ~ r2_hidden(X3,X0) ) )
& ( ? [X3] :
( r2_hidden(X2,X3)
& r2_hidden(X3,X0) )
| ~ r2_hidden(X2,X1) ) )
| k3_tarski(X0) != X1 ) ),
inference(nnf_transformation,[],[f9]) ).
fof(f20455,plain,
! [X0,X1] :
( ( X1 = k3_tarski(X0)
| ? [X2] :
( ( ! [X3] :
( ~ r2_hidden(X2,X3)
| ~ r2_hidden(X3,X0) )
| ~ r2_hidden(X2,X1) )
& ( ? [X4] :
( r2_hidden(X2,X4)
& r2_hidden(X4,X0) )
| r2_hidden(X2,X1) ) ) )
& ( ! [X5] :
( ( r2_hidden(X5,X1)
| ! [X6] :
( ~ r2_hidden(X5,X6)
| ~ r2_hidden(X6,X0) ) )
& ( ? [X7] :
( r2_hidden(X5,X7)
& r2_hidden(X7,X0) )
| ~ r2_hidden(X5,X1) ) )
| k3_tarski(X0) != X1 ) ),
inference(rectify,[],[f20454]) ).
fof(f20456,plain,
! [X0,X1] :
( ( X1 = k3_tarski(X0)
| ( ( ! [X3] :
( ~ r2_hidden(sK42(X0,X1),X3)
| ~ r2_hidden(X3,X0) )
| ~ r2_hidden(sK42(X0,X1),X1) )
& ( ( r2_hidden(sK42(X0,X1),sK43(X0,X1))
& r2_hidden(sK43(X0,X1),X0) )
| r2_hidden(sK42(X0,X1),X1) ) ) )
& ( ! [X5] :
( ( r2_hidden(X5,X1)
| ! [X6] :
( ~ r2_hidden(X5,X6)
| ~ r2_hidden(X6,X0) ) )
& ( ( r2_hidden(X5,sK44(X0,X5))
& r2_hidden(sK44(X0,X5),X0) )
| ~ r2_hidden(X5,X1) ) )
| k3_tarski(X0) != X1 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK42,sK43,sK44]),skolemize(X2,sK42(X0,X1)),skolemize(X4,sK43(X0,X1)),skolemize(X7,sK44(X0,X5))],[f20455]) ).
fof(f20502,plain,
! [X0,X1,X2] :
( ( ( r2_hidden(X0,k9_relat_1(X2,X1))
| ! [X3] :
( ~ r2_hidden(X3,k1_relat_1(X2))
| ~ r2_hidden(k4_tarski(X3,X0),X2)
| ~ r2_hidden(X3,X1) ) )
& ( ? [X3] :
( r2_hidden(X3,k1_relat_1(X2))
& r2_hidden(k4_tarski(X3,X0),X2)
& r2_hidden(X3,X1) )
| ~ r2_hidden(X0,k9_relat_1(X2,X1)) ) )
| ~ v1_relat_1(X2) ),
inference(nnf_transformation,[],[f19224]) ).
fof(f20503,plain,
! [X0,X1,X2] :
( ( ( r2_hidden(X0,k9_relat_1(X2,X1))
| ! [X3] :
( ~ r2_hidden(X3,k1_relat_1(X2))
| ~ r2_hidden(k4_tarski(X3,X0),X2)
| ~ r2_hidden(X3,X1) ) )
& ( ? [X4] :
( r2_hidden(X4,k1_relat_1(X2))
& r2_hidden(k4_tarski(X4,X0),X2)
& r2_hidden(X4,X1) )
| ~ r2_hidden(X0,k9_relat_1(X2,X1)) ) )
| ~ v1_relat_1(X2) ),
inference(rectify,[],[f20502]) ).
fof(f20504,plain,
! [X0,X1,X2] :
( ( ( r2_hidden(X0,k9_relat_1(X2,X1))
| ! [X3] :
( ~ r2_hidden(X3,k1_relat_1(X2))
| ~ r2_hidden(k4_tarski(X3,X0),X2)
| ~ r2_hidden(X3,X1) ) )
& ( ( r2_hidden(sK74(X0,X1,X2),k1_relat_1(X2))
& r2_hidden(k4_tarski(sK74(X0,X1,X2),X0),X2)
& r2_hidden(sK74(X0,X1,X2),X1) )
| ~ r2_hidden(X0,k9_relat_1(X2,X1)) ) )
| ~ v1_relat_1(X2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK74]),skolemize(X4,sK74(X0,X1,X2))],[f20503]) ).
fof(f20505,plain,
! [X0] :
( ! [X1,X2] :
( ( X2 = k9_relat_1(X0,X1)
| ? [X3] :
( ( ! [X4] :
( ~ r2_hidden(k4_tarski(X4,X3),X0)
| ~ r2_hidden(X4,X1) )
| ~ r2_hidden(X3,X2) )
& ( ? [X4] :
( r2_hidden(k4_tarski(X4,X3),X0)
& r2_hidden(X4,X1) )
| r2_hidden(X3,X2) ) ) )
& ( ! [X3] :
( ( r2_hidden(X3,X2)
| ! [X4] :
( ~ r2_hidden(k4_tarski(X4,X3),X0)
| ~ r2_hidden(X4,X1) ) )
& ( ? [X4] :
( r2_hidden(k4_tarski(X4,X3),X0)
& r2_hidden(X4,X1) )
| ~ r2_hidden(X3,X2) ) )
| k9_relat_1(X0,X1) != X2 ) )
| ~ v1_relat_1(X0) ),
inference(nnf_transformation,[],[f19225]) ).
fof(f20506,plain,
! [X0] :
( ! [X1,X2] :
( ( X2 = k9_relat_1(X0,X1)
| ? [X3] :
( ( ! [X4] :
( ~ r2_hidden(k4_tarski(X4,X3),X0)
| ~ r2_hidden(X4,X1) )
| ~ r2_hidden(X3,X2) )
& ( ? [X5] :
( r2_hidden(k4_tarski(X5,X3),X0)
& r2_hidden(X5,X1) )
| r2_hidden(X3,X2) ) ) )
& ( ! [X6] :
( ( r2_hidden(X6,X2)
| ! [X7] :
( ~ r2_hidden(k4_tarski(X7,X6),X0)
| ~ r2_hidden(X7,X1) ) )
& ( ? [X8] :
( r2_hidden(k4_tarski(X8,X6),X0)
& r2_hidden(X8,X1) )
| ~ r2_hidden(X6,X2) ) )
| k9_relat_1(X0,X1) != X2 ) )
| ~ v1_relat_1(X0) ),
inference(rectify,[],[f20505]) ).
fof(f20507,plain,
! [X0] :
( ! [X1,X2] :
( ( X2 = k9_relat_1(X0,X1)
| ( ( ! [X4] :
( ~ r2_hidden(k4_tarski(X4,sK75(X0,X1,X2)),X0)
| ~ r2_hidden(X4,X1) )
| ~ r2_hidden(sK75(X0,X1,X2),X2) )
& ( ( r2_hidden(k4_tarski(sK76(X0,X1,X2),sK75(X0,X1,X2)),X0)
& r2_hidden(sK76(X0,X1,X2),X1) )
| r2_hidden(sK75(X0,X1,X2),X2) ) ) )
& ( ! [X6] :
( ( r2_hidden(X6,X2)
| ! [X7] :
( ~ r2_hidden(k4_tarski(X7,X6),X0)
| ~ r2_hidden(X7,X1) ) )
& ( ( r2_hidden(k4_tarski(sK77(X0,X1,X6),X6),X0)
& r2_hidden(sK77(X0,X1,X6),X1) )
| ~ r2_hidden(X6,X2) ) )
| k9_relat_1(X0,X1) != X2 ) )
| ~ v1_relat_1(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK75,sK76,sK77]),skolemize(X3,sK75(X0,X1,X2)),skolemize(X5,sK76(X0,X1,X2)),skolemize(X8,sK77(X0,X1,X6))],[f20506]) ).
fof(f20508,plain,
! [X0,X1,X2,X3] :
( ( ( r2_hidden(X0,a_3_0_relset_2(X1,X2,X3))
| ! [X4] :
( ~ m1_subset_1(X4,k1_zfmisc_1(X1))
| k9_relat_1(X3,X4) != X0
| ~ r2_hidden(X4,X2) ) )
& ( ? [X4] :
( m1_subset_1(X4,k1_zfmisc_1(X1))
& X0 = k9_relat_1(X3,X4)
& r2_hidden(X4,X2) )
| ~ r2_hidden(X0,a_3_0_relset_2(X1,X2,X3)) ) )
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_zfmisc_1(X1)))
| ~ v1_relat_1(X3) ),
inference(nnf_transformation,[],[f19227]) ).
fof(f20509,plain,
! [X0,X1,X2,X3] :
( ( ( r2_hidden(X0,a_3_0_relset_2(X1,X2,X3))
| ! [X4] :
( ~ m1_subset_1(X4,k1_zfmisc_1(X1))
| k9_relat_1(X3,X4) != X0
| ~ r2_hidden(X4,X2) ) )
& ( ? [X5] :
( m1_subset_1(X5,k1_zfmisc_1(X1))
& k9_relat_1(X3,X5) = X0
& r2_hidden(X5,X2) )
| ~ r2_hidden(X0,a_3_0_relset_2(X1,X2,X3)) ) )
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_zfmisc_1(X1)))
| ~ v1_relat_1(X3) ),
inference(rectify,[],[f20508]) ).
fof(f20510,plain,
! [X0,X1,X2,X3] :
( ( ( r2_hidden(X0,a_3_0_relset_2(X1,X2,X3))
| ! [X4] :
( ~ m1_subset_1(X4,k1_zfmisc_1(X1))
| k9_relat_1(X3,X4) != X0
| ~ r2_hidden(X4,X2) ) )
& ( ( m1_subset_1(sK78(X0,X1,X2,X3),k1_zfmisc_1(X1))
& k9_relat_1(X3,sK78(X0,X1,X2,X3)) = X0
& r2_hidden(sK78(X0,X1,X2,X3),X2) )
| ~ r2_hidden(X0,a_3_0_relset_2(X1,X2,X3)) ) )
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_zfmisc_1(X1)))
| ~ v1_relat_1(X3) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK78]),skolemize(X5,sK78(X0,X1,X2,X3))],[f20509]) ).
fof(f20557,plain,
! [X0,X1] :
( ( X0 = X1
| ~ r1_tarski(X0,X1)
| ~ r1_tarski(X1,X0) )
& ( ( r1_tarski(X0,X1)
& r1_tarski(X1,X0) )
| X0 != X1 ) ),
inference(nnf_transformation,[],[f38]) ).
fof(f20558,plain,
! [X0,X1] :
( ( X0 = X1
| ~ r1_tarski(X0,X1)
| ~ r1_tarski(X1,X0) )
& ( ( r1_tarski(X0,X1)
& r1_tarski(X1,X0) )
| X0 != X1 ) ),
inference(flattening,[],[f20557]) ).
fof(f20559,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,[],[f19354]) ).
fof(f20560,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,[],[f20559]) ).
fof(f20561,plain,
! [X0,X1] :
( ( r1_tarski(X0,X1)
| ( ~ r2_hidden(sK112(X0,X1),X1)
& r2_hidden(sK112(X0,X1),X0) ) )
& ( ! [X3] :
( r2_hidden(X3,X1)
| ~ r2_hidden(X3,X0) )
| ~ r1_tarski(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK112]),skolemize(X2,sK112(X0,X1))],[f20560]) ).
fof(f20975,plain,
m1_subset_1(sK32,k1_zfmisc_1(k1_zfmisc_1(sK31))),
inference(cnf_transformation,[],[f20443]) ).
fof(f20976,plain,
v1_relat_1(sK33),
inference(cnf_transformation,[],[f20443]) ).
fof(f20977,plain,
k9_relat_1(sK33,k5_setfam_1(sK31,sK32)) != k3_tarski(a_3_0_relset_2(sK31,sK32,sK33)),
inference(cnf_transformation,[],[f20443]) ).
fof(f21004,plain,
! [X0,X1] :
( r2_hidden(sK41(X0,X1),X0)
| r1_tarski(k3_tarski(X0),X1) ),
inference(cnf_transformation,[],[f20453]) ).
fof(f21005,plain,
! [X0,X1] :
( ~ r1_tarski(sK41(X0,X1),X1)
| r1_tarski(k3_tarski(X0),X1) ),
inference(cnf_transformation,[],[f20453]) ).
fof(f21009,plain,
! [X0,X1,X5] :
( r2_hidden(sK44(X0,X5),X0)
| ~ r2_hidden(X5,X1)
| k3_tarski(X0) != X1 ),
inference(cnf_transformation,[],[f20456]) ).
fof(f21010,plain,
! [X0,X1,X5] :
( r2_hidden(X5,sK44(X0,X5))
| ~ r2_hidden(X5,X1)
| k3_tarski(X0) != X1 ),
inference(cnf_transformation,[],[f20456]) ).
fof(f21011,plain,
! [X0,X1,X6,X5] :
( r2_hidden(X5,X1)
| ~ r2_hidden(X5,X6)
| ~ r2_hidden(X6,X0)
| k3_tarski(X0) != X1 ),
inference(cnf_transformation,[],[f20456]) ).
fof(f21092,plain,
! [X0,X1] :
( k3_tarski(X1) = k5_setfam_1(X0,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(k1_zfmisc_1(X0))) ),
inference(cnf_transformation,[],[f19155]) ).
fof(f21134,plain,
! [X2,X0,X1] :
( r1_tarski(k9_relat_1(X2,X0),k9_relat_1(X2,X1))
| ~ r1_tarski(X0,X1)
| ~ v1_relat_1(X2) ),
inference(cnf_transformation,[],[f19211]) ).
fof(f21148,plain,
! [X2,X0,X1] :
( r2_hidden(sK74(X0,X1,X2),X1)
| ~ r2_hidden(X0,k9_relat_1(X2,X1))
| ~ v1_relat_1(X2) ),
inference(cnf_transformation,[],[f20504]) ).
fof(f21149,plain,
! [X2,X0,X1] :
( r2_hidden(k4_tarski(sK74(X0,X1,X2),X0),X2)
| ~ r2_hidden(X0,k9_relat_1(X2,X1))
| ~ v1_relat_1(X2) ),
inference(cnf_transformation,[],[f20504]) ).
fof(f21154,plain,
! [X2,X0,X1,X6,X7] :
( r2_hidden(X6,X2)
| ~ r2_hidden(k4_tarski(X7,X6),X0)
| ~ r2_hidden(X7,X1)
| k9_relat_1(X0,X1) != X2
| ~ v1_relat_1(X0) ),
inference(cnf_transformation,[],[f20507]) ).
fof(f21158,plain,
! [X2,X3,X0,X1] :
( r2_hidden(sK78(X0,X1,X2,X3),X2)
| ~ r2_hidden(X0,a_3_0_relset_2(X1,X2,X3))
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_zfmisc_1(X1)))
| ~ v1_relat_1(X3) ),
inference(cnf_transformation,[],[f20510]) ).
fof(f21159,plain,
! [X2,X3,X0,X1] :
( k9_relat_1(X3,sK78(X0,X1,X2,X3)) = X0
| ~ r2_hidden(X0,a_3_0_relset_2(X1,X2,X3))
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_zfmisc_1(X1)))
| ~ v1_relat_1(X3) ),
inference(cnf_transformation,[],[f20510]) ).
fof(f21161,plain,
! [X2,X3,X0,X1,X4] :
( r2_hidden(X0,a_3_0_relset_2(X1,X2,X3))
| ~ m1_subset_1(X4,k1_zfmisc_1(X1))
| k9_relat_1(X3,X4) != X0
| ~ r2_hidden(X4,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_zfmisc_1(X1)))
| ~ v1_relat_1(X3) ),
inference(cnf_transformation,[],[f20510]) ).
fof(f21198,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ r2_hidden(X0,X1)
| m1_subset_1(X0,X2) ),
inference(cnf_transformation,[],[f19258]) ).
fof(f21332,plain,
! [X0,X1] :
( ~ r1_tarski(X1,X0)
| ~ r1_tarski(X0,X1)
| X0 = X1 ),
inference(cnf_transformation,[],[f20558]) ).
fof(f21335,plain,
! [X0,X1] :
( r2_hidden(sK112(X0,X1),X0)
| r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f20561]) ).
fof(f21336,plain,
! [X0,X1] :
( ~ r2_hidden(sK112(X0,X1),X1)
| r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f20561]) ).
fof(f23017,plain,
! [X0,X6,X5] :
( r2_hidden(X5,k3_tarski(X0))
| ~ r2_hidden(X5,X6)
| ~ r2_hidden(X6,X0) ),
inference(equality_resolution,[],[f21011]) ).
fof(f23018,plain,
! [X0,X5] :
( r2_hidden(X5,sK44(X0,X5))
| ~ r2_hidden(X5,k3_tarski(X0)) ),
inference(equality_resolution,[],[f21010]) ).
fof(f23019,plain,
! [X0,X5] :
( r2_hidden(sK44(X0,X5),X0)
| ~ r2_hidden(X5,k3_tarski(X0)) ),
inference(equality_resolution,[],[f21009]) ).
fof(f23037,plain,
! [X0,X1,X6,X7] :
( ~ r2_hidden(k4_tarski(X7,X6),X0)
| r2_hidden(X6,k9_relat_1(X0,X1))
| ~ r2_hidden(X7,X1)
| ~ v1_relat_1(X0) ),
inference(equality_resolution,[],[f21154]) ).
fof(f23040,plain,
! [X2,X3,X1,X4] :
( r2_hidden(k9_relat_1(X3,X4),a_3_0_relset_2(X1,X2,X3))
| ~ m1_subset_1(X4,k1_zfmisc_1(X1))
| ~ r2_hidden(X4,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(k1_zfmisc_1(X1)))
| ~ v1_relat_1(X3) ),
inference(equality_resolution,[],[f21161]) ).
fof(f23185,definition,
sF385 = k5_setfam_1(sK31,sK32),
introduced(definition,[new_symbols(definition,[sF385])],[function_definition]) ).
fof(f23186,plain,
k5_setfam_1(sK31,sK32) = sF385,
inference(reorient_equations,[],[f23185]) ).
fof(f23187,definition,
sF386 = k9_relat_1(sK33,sF385),
introduced(definition,[new_symbols(definition,[sF386])],[function_definition]) ).
fof(f23188,plain,
k9_relat_1(sK33,sF385) = sF386,
inference(reorient_equations,[],[f23187]) ).
fof(f23189,definition,
sF387 = a_3_0_relset_2(sK31,sK32,sK33),
introduced(definition,[new_symbols(definition,[sF387])],[function_definition]) ).
fof(f23190,plain,
a_3_0_relset_2(sK31,sK32,sK33) = sF387,
inference(reorient_equations,[],[f23189]) ).
fof(f23191,definition,
sF388 = k3_tarski(sF387),
introduced(definition,[new_symbols(definition,[sF388])],[function_definition]) ).
fof(f23192,plain,
k3_tarski(sF387) = sF388,
inference(reorient_equations,[],[f23191]) ).
fof(f23193,plain,
sF386 != sF388,
inference(definition_folding,[],[f20977,f23192,f23190,f23188,f23186]) ).
fof(f23194,definition,
sF389 = k1_zfmisc_1(sK31),
introduced(definition,[new_symbols(definition,[sF389])],[function_definition]) ).
fof(f23195,plain,
k1_zfmisc_1(sK31) = sF389,
inference(reorient_equations,[],[f23194]) ).
fof(f23196,definition,
sF390 = k1_zfmisc_1(sF389),
introduced(definition,[new_symbols(definition,[sF390])],[function_definition]) ).
fof(f23197,plain,
k1_zfmisc_1(sF389) = sF390,
inference(reorient_equations,[],[f23196]) ).
fof(f23198,plain,
m1_subset_1(sK32,sF390),
inference(definition_folding,[],[f20975,f23197,f23195]) ).
fof(f23788,definition,
( spl391_116
<=> m1_subset_1(sK32,sF390) ),
introduced(definition,[new_symbols(definition,[spl391_116])],[avatar_definition]) ).
fof(f23790,plain,
( m1_subset_1(sK32,sF390)
| ~ spl391_116 ),
inference(avatar_component_clause,[],[f23788]) ).
fof(f23791,plain,
spl391_116,
inference(avatar_split_clause,[],[f23198,f23788]) ).
fof(f23793,definition,
( spl391_117
<=> v1_relat_1(sK33) ),
introduced(definition,[new_symbols(definition,[spl391_117])],[avatar_definition]) ).
fof(f23795,plain,
( v1_relat_1(sK33)
| ~ spl391_117 ),
inference(avatar_component_clause,[],[f23793]) ).
fof(f23796,plain,
spl391_117,
inference(avatar_split_clause,[],[f20976,f23793]) ).
fof(f23798,definition,
( spl391_118
<=> sF386 = sF388 ),
introduced(definition,[new_symbols(definition,[spl391_118])],[avatar_definition]) ).
fof(f23800,plain,
( sF386 != sF388
| spl391_118 ),
inference(avatar_component_clause,[],[f23798]) ).
fof(f23801,plain,
~ spl391_118,
inference(avatar_split_clause,[],[f23193,f23798]) ).
fof(f23803,definition,
( spl391_119
<=> k5_setfam_1(sK31,sK32) = sF385 ),
introduced(definition,[new_symbols(definition,[spl391_119])],[avatar_definition]) ).
fof(f23805,plain,
( k5_setfam_1(sK31,sK32) = sF385
| ~ spl391_119 ),
inference(avatar_component_clause,[],[f23803]) ).
fof(f23806,plain,
spl391_119,
inference(avatar_split_clause,[],[f23186,f23803]) ).
fof(f23808,definition,
( spl391_120
<=> k9_relat_1(sK33,sF385) = sF386 ),
introduced(definition,[new_symbols(definition,[spl391_120])],[avatar_definition]) ).
fof(f23810,plain,
( k9_relat_1(sK33,sF385) = sF386
| ~ spl391_120 ),
inference(avatar_component_clause,[],[f23808]) ).
fof(f23811,plain,
spl391_120,
inference(avatar_split_clause,[],[f23188,f23808]) ).
fof(f23813,definition,
( spl391_121
<=> a_3_0_relset_2(sK31,sK32,sK33) = sF387 ),
introduced(definition,[new_symbols(definition,[spl391_121])],[avatar_definition]) ).
fof(f23815,plain,
( a_3_0_relset_2(sK31,sK32,sK33) = sF387
| ~ spl391_121 ),
inference(avatar_component_clause,[],[f23813]) ).
fof(f23816,plain,
spl391_121,
inference(avatar_split_clause,[],[f23190,f23813]) ).
fof(f23818,definition,
( spl391_122
<=> k3_tarski(sF387) = sF388 ),
introduced(definition,[new_symbols(definition,[spl391_122])],[avatar_definition]) ).
fof(f23820,plain,
( k3_tarski(sF387) = sF388
| ~ spl391_122 ),
inference(avatar_component_clause,[],[f23818]) ).
fof(f23821,plain,
spl391_122,
inference(avatar_split_clause,[],[f23192,f23818]) ).
fof(f23823,definition,
( spl391_123
<=> k1_zfmisc_1(sK31) = sF389 ),
introduced(definition,[new_symbols(definition,[spl391_123])],[avatar_definition]) ).
fof(f23825,plain,
( k1_zfmisc_1(sK31) = sF389
| ~ spl391_123 ),
inference(avatar_component_clause,[],[f23823]) ).
fof(f23826,plain,
spl391_123,
inference(avatar_split_clause,[],[f23195,f23823]) ).
fof(f23828,definition,
( spl391_124
<=> k1_zfmisc_1(sF389) = sF390 ),
introduced(definition,[new_symbols(definition,[spl391_124])],[avatar_definition]) ).
fof(f23830,plain,
( k1_zfmisc_1(sF389) = sF390
| ~ spl391_124 ),
inference(avatar_component_clause,[],[f23828]) ).
fof(f23831,plain,
spl391_124,
inference(avatar_split_clause,[],[f23197,f23828]) ).
fof(f23834,plain,
( ! [X0] :
( r2_hidden(k9_relat_1(sK33,X0),sF387)
| ~ m1_subset_1(X0,k1_zfmisc_1(sK31))
| ~ r2_hidden(X0,sK32)
| ~ m1_subset_1(sK32,k1_zfmisc_1(k1_zfmisc_1(sK31)))
| ~ v1_relat_1(sK33) )
| ~ spl391_121 ),
inference(superposition,[],[f23040,f23815]) ).
fof(f23836,plain,
( ! [X0] :
( r2_hidden(k9_relat_1(sK33,X0),sF387)
| ~ m1_subset_1(X0,k1_zfmisc_1(sK31))
| ~ r2_hidden(X0,sK32)
| ~ m1_subset_1(sK32,k1_zfmisc_1(k1_zfmisc_1(sK31))) )
| ~ spl391_117
| ~ spl391_121 ),
inference(forward_subsumption_resolution,[],[f23834,f23795]) ).
fof(f23838,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF389)
| r2_hidden(k9_relat_1(sK33,X0),sF387)
| ~ r2_hidden(X0,sK32)
| ~ m1_subset_1(sK32,k1_zfmisc_1(k1_zfmisc_1(sK31))) )
| ~ spl391_117
| ~ spl391_121
| ~ spl391_123 ),
inference(forward_demodulation,[],[f23836,f23825]) ).
fof(f23839,plain,
( ! [X0] :
( ~ m1_subset_1(sK32,k1_zfmisc_1(sF389))
| ~ m1_subset_1(X0,sF389)
| r2_hidden(k9_relat_1(sK33,X0),sF387)
| ~ r2_hidden(X0,sK32) )
| ~ spl391_117
| ~ spl391_121
| ~ spl391_123 ),
inference(forward_demodulation,[],[f23838,f23825]) ).
fof(f23840,plain,
( ! [X0] :
( ~ m1_subset_1(sK32,sF390)
| ~ m1_subset_1(X0,sF389)
| r2_hidden(k9_relat_1(sK33,X0),sF387)
| ~ r2_hidden(X0,sK32) )
| ~ spl391_117
| ~ spl391_121
| ~ spl391_123
| ~ spl391_124 ),
inference(forward_demodulation,[],[f23839,f23830]) ).
fof(f23841,plain,
( ! [X0] :
( r2_hidden(k9_relat_1(sK33,X0),sF387)
| ~ m1_subset_1(X0,sF389)
| ~ r2_hidden(X0,sK32) )
| ~ spl391_116
| ~ spl391_117
| ~ spl391_121
| ~ spl391_123
| ~ spl391_124 ),
inference(forward_subsumption_resolution,[],[f23840,f23790]) ).
fof(f23859,plain,
( sF385 = k3_tarski(sK32)
| ~ m1_subset_1(sK32,k1_zfmisc_1(k1_zfmisc_1(sK31)))
| ~ spl391_119 ),
inference(superposition,[],[f23805,f21092]) ).
fof(f23860,plain,
( ~ m1_subset_1(sK32,k1_zfmisc_1(sF389))
| sF385 = k3_tarski(sK32)
| ~ spl391_119
| ~ spl391_123 ),
inference(forward_demodulation,[],[f23859,f23825]) ).
fof(f23862,plain,
( ~ m1_subset_1(sK32,sF390)
| sF385 = k3_tarski(sK32)
| ~ spl391_119
| ~ spl391_123
| ~ spl391_124 ),
inference(forward_demodulation,[],[f23860,f23830]) ).
fof(f23864,plain,
( sF385 = k3_tarski(sK32)
| ~ spl391_116
| ~ spl391_119
| ~ spl391_123
| ~ spl391_124 ),
inference(forward_subsumption_resolution,[],[f23862,f23790]) ).
fof(f23867,definition,
( spl391_128
<=> sF385 = k3_tarski(sK32) ),
introduced(definition,[new_symbols(definition,[spl391_128])],[avatar_definition]) ).
fof(f23869,plain,
( sF385 = k3_tarski(sK32)
| ~ spl391_128 ),
inference(avatar_component_clause,[],[f23867]) ).
fof(f23870,plain,
( spl391_128
| ~ spl391_116
| ~ spl391_119
| ~ spl391_123
| ~ spl391_124 ),
inference(avatar_split_clause,[],[f23864,f23828,f23823,f23803,f23788,f23867]) ).
fof(f23886,plain,
! [X2,X3,X0,X1] :
( ~ r2_hidden(X0,k9_relat_1(X1,X2))
| ~ v1_relat_1(X1)
| r2_hidden(X0,k9_relat_1(X1,X3))
| ~ r2_hidden(sK74(X0,X2,X1),X3)
| ~ v1_relat_1(X1) ),
inference(resolution,[],[f21149,f23037]) ).
fof(f23887,plain,
! [X2,X3,X0,X1] :
( ~ r2_hidden(sK74(X0,X2,X1),X3)
| ~ v1_relat_1(X1)
| r2_hidden(X0,k9_relat_1(X1,X3))
| ~ r2_hidden(X0,k9_relat_1(X1,X2)) ),
inference(duplicate_literal_removal,[],[f23886]) ).
fof(f23919,plain,
! [X2,X3,X0,X1,X4] :
( r1_tarski(X0,k9_relat_1(X1,X4))
| ~ r1_tarski(sK78(X0,X2,X3,X1),X4)
| ~ v1_relat_1(X1)
| ~ r2_hidden(X0,a_3_0_relset_2(X2,X3,X1))
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_zfmisc_1(X2)))
| ~ v1_relat_1(X1) ),
inference(superposition,[],[f21134,f21159]) ).
fof(f23923,plain,
! [X2,X3,X0,X1,X4] :
( ~ r1_tarski(sK78(X0,X2,X3,X1),X4)
| r1_tarski(X0,k9_relat_1(X1,X4))
| ~ v1_relat_1(X1)
| ~ r2_hidden(X0,a_3_0_relset_2(X2,X3,X1))
| ~ m1_subset_1(X3,k1_zfmisc_1(k1_zfmisc_1(X2))) ),
inference(duplicate_literal_removal,[],[f23919]) ).
fof(f23948,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,sF390)
| ~ r2_hidden(X1,X0)
| m1_subset_1(X1,sF389) )
| ~ spl391_124 ),
inference(superposition,[],[f21198,f23830]) ).
fof(f23960,plain,
( ! [X0,X1] :
( ~ r2_hidden(X1,sF387)
| ~ r2_hidden(X0,X1)
| r2_hidden(X0,sF388) )
| ~ spl391_122 ),
inference(superposition,[],[f23017,f23820]) ).
fof(f23961,plain,
( ! [X0,X1] :
( ~ r2_hidden(X1,sK32)
| ~ r2_hidden(X0,X1)
| r2_hidden(X0,sF385) )
| ~ spl391_128 ),
inference(superposition,[],[f23017,f23869]) ).
fof(f23968,plain,
( ! [X2,X3,X0,X1] :
( ~ r2_hidden(X0,sK78(X1,X2,sK32,X3))
| r2_hidden(X0,sF385)
| ~ r2_hidden(X1,a_3_0_relset_2(X2,sK32,X3))
| ~ m1_subset_1(sK32,k1_zfmisc_1(k1_zfmisc_1(X2)))
| ~ v1_relat_1(X3) )
| ~ spl391_128 ),
inference(resolution,[],[f23961,f21158]) ).
fof(f23989,plain,
( ! [X2,X3,X0,X1] :
( r2_hidden(sK112(sK78(X0,X1,sK32,X2),X3),sF385)
| ~ r2_hidden(X0,a_3_0_relset_2(X1,sK32,X2))
| ~ m1_subset_1(sK32,k1_zfmisc_1(k1_zfmisc_1(X1)))
| ~ v1_relat_1(X2)
| r1_tarski(sK78(X0,X1,sK32,X2),X3) )
| ~ spl391_128 ),
inference(resolution,[],[f23968,f21335]) ).
fof(f23992,plain,
( ! [X0,X1] :
( ~ r2_hidden(X0,k9_relat_1(sK33,X1))
| r2_hidden(X0,sF388)
| ~ m1_subset_1(X1,sF389)
| ~ r2_hidden(X1,sK32) )
| ~ spl391_116
| ~ spl391_117
| ~ spl391_121
| ~ spl391_122
| ~ spl391_123
| ~ spl391_124 ),
inference(resolution,[],[f23960,f23841]) ).
fof(f24030,definition,
( spl391_137
<=> ! [X0] :
( ~ r2_hidden(X0,sF386)
| r2_hidden(X0,sF388) ) ),
introduced(definition,[new_symbols(definition,[spl391_137])],[avatar_definition]) ).
fof(f24031,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF386)
| r2_hidden(X0,sF388) )
| ~ spl391_137 ),
inference(avatar_component_clause,[],[f24030]) ).
fof(f24108,plain,
! [X2,X3,X0,X1] :
( r2_hidden(X1,k9_relat_1(X0,sK44(X2,sK74(X1,X3,X0))))
| ~ v1_relat_1(X0)
| ~ r2_hidden(X1,k9_relat_1(X0,X3))
| ~ r2_hidden(sK74(X1,X3,X0),k3_tarski(X2)) ),
inference(resolution,[],[f23887,f23018]) ).
fof(f24120,plain,
( ! [X2,X0,X1] :
( ~ v1_relat_1(sK33)
| ~ r2_hidden(X0,k9_relat_1(sK33,X1))
| ~ r2_hidden(sK74(X0,X1,sK33),k3_tarski(X2))
| r2_hidden(X0,sF388)
| ~ m1_subset_1(sK44(X2,sK74(X0,X1,sK33)),sF389)
| ~ r2_hidden(sK44(X2,sK74(X0,X1,sK33)),sK32) )
| ~ spl391_116
| ~ spl391_117
| ~ spl391_121
| ~ spl391_122
| ~ spl391_123
| ~ spl391_124 ),
inference(resolution,[],[f24108,f23992]) ).
fof(f24127,plain,
( ! [X2,X0,X1] :
( ~ r2_hidden(X0,k9_relat_1(sK33,X1))
| ~ r2_hidden(sK74(X0,X1,sK33),k3_tarski(X2))
| r2_hidden(X0,sF388)
| ~ m1_subset_1(sK44(X2,sK74(X0,X1,sK33)),sF389)
| ~ r2_hidden(sK44(X2,sK74(X0,X1,sK33)),sK32) )
| ~ spl391_116
| ~ spl391_117
| ~ spl391_121
| ~ spl391_122
| ~ spl391_123
| ~ spl391_124 ),
inference(forward_subsumption_resolution,[],[f24120,f23795]) ).
fof(f24182,plain,
( ! [X2,X0,X1] :
( ~ r2_hidden(X0,a_3_0_relset_2(X1,sK32,X2))
| ~ m1_subset_1(sK32,k1_zfmisc_1(k1_zfmisc_1(X1)))
| ~ v1_relat_1(X2)
| r1_tarski(sK78(X0,X1,sK32,X2),sF385)
| r1_tarski(sK78(X0,X1,sK32,X2),sF385) )
| ~ spl391_128 ),
inference(resolution,[],[f23989,f21336]) ).
fof(f24184,plain,
( ! [X2,X0,X1] :
( r1_tarski(sK78(X0,X1,sK32,X2),sF385)
| ~ m1_subset_1(sK32,k1_zfmisc_1(k1_zfmisc_1(X1)))
| ~ v1_relat_1(X2)
| ~ r2_hidden(X0,a_3_0_relset_2(X1,sK32,X2)) )
| ~ spl391_128 ),
inference(duplicate_literal_removal,[],[f24182]) ).
fof(f24185,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(sK32,k1_zfmisc_1(k1_zfmisc_1(X0)))
| ~ v1_relat_1(X1)
| ~ r2_hidden(X2,a_3_0_relset_2(X0,sK32,X1))
| r1_tarski(X2,k9_relat_1(X1,sF385))
| ~ v1_relat_1(X1)
| ~ r2_hidden(X2,a_3_0_relset_2(X0,sK32,X1))
| ~ m1_subset_1(sK32,k1_zfmisc_1(k1_zfmisc_1(X0))) )
| ~ spl391_128 ),
inference(resolution,[],[f24184,f23923]) ).
fof(f24190,plain,
( ! [X2,X0,X1] :
( ~ r2_hidden(X2,a_3_0_relset_2(X0,sK32,X1))
| ~ v1_relat_1(X1)
| ~ m1_subset_1(sK32,k1_zfmisc_1(k1_zfmisc_1(X0)))
| r1_tarski(X2,k9_relat_1(X1,sF385)) )
| ~ spl391_128 ),
inference(duplicate_literal_removal,[],[f24185]) ).
fof(f24212,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF387)
| ~ v1_relat_1(sK33)
| ~ m1_subset_1(sK32,k1_zfmisc_1(k1_zfmisc_1(sK31)))
| r1_tarski(X0,k9_relat_1(sK33,sF385)) )
| ~ spl391_121
| ~ spl391_128 ),
inference(superposition,[],[f24190,f23815]) ).
fof(f24215,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF387)
| ~ m1_subset_1(sK32,k1_zfmisc_1(k1_zfmisc_1(sK31)))
| r1_tarski(X0,k9_relat_1(sK33,sF385)) )
| ~ spl391_117
| ~ spl391_121
| ~ spl391_128 ),
inference(forward_subsumption_resolution,[],[f24212,f23795]) ).
fof(f24218,plain,
( ! [X0] :
( ~ m1_subset_1(sK32,k1_zfmisc_1(sF389))
| ~ r2_hidden(X0,sF387)
| r1_tarski(X0,k9_relat_1(sK33,sF385)) )
| ~ spl391_117
| ~ spl391_121
| ~ spl391_123
| ~ spl391_128 ),
inference(forward_demodulation,[],[f24215,f23825]) ).
fof(f24227,plain,
( ! [X0] :
( ~ m1_subset_1(sK32,sF390)
| ~ r2_hidden(X0,sF387)
| r1_tarski(X0,k9_relat_1(sK33,sF385)) )
| ~ spl391_117
| ~ spl391_121
| ~ spl391_123
| ~ spl391_124
| ~ spl391_128 ),
inference(forward_demodulation,[],[f24218,f23830]) ).
fof(f24229,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF387)
| r1_tarski(X0,k9_relat_1(sK33,sF385)) )
| ~ spl391_116
| ~ spl391_117
| ~ spl391_121
| ~ spl391_123
| ~ spl391_124
| ~ spl391_128 ),
inference(forward_subsumption_resolution,[],[f24227,f23790]) ).
fof(f24235,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF387)
| r1_tarski(X0,sF386) )
| ~ spl391_116
| ~ spl391_117
| ~ spl391_120
| ~ spl391_121
| ~ spl391_123
| ~ spl391_124
| ~ spl391_128 ),
inference(forward_demodulation,[],[f24229,f23810]) ).
fof(f24240,plain,
( ! [X0] :
( r1_tarski(sK41(sF387,X0),sF386)
| r1_tarski(k3_tarski(sF387),X0) )
| ~ spl391_116
| ~ spl391_117
| ~ spl391_120
| ~ spl391_121
| ~ spl391_123
| ~ spl391_124
| ~ spl391_128 ),
inference(resolution,[],[f24235,f21004]) ).
fof(f24249,plain,
( ! [X0] :
( r1_tarski(sK41(sF387,X0),sF386)
| r1_tarski(sF388,X0) )
| ~ spl391_116
| ~ spl391_117
| ~ spl391_120
| ~ spl391_121
| ~ spl391_122
| ~ spl391_123
| ~ spl391_124
| ~ spl391_128 ),
inference(forward_demodulation,[],[f24240,f23820]) ).
fof(f24383,plain,
( r1_tarski(k3_tarski(sF387),sF386)
| r1_tarski(sF388,sF386)
| ~ spl391_116
| ~ spl391_117
| ~ spl391_120
| ~ spl391_121
| ~ spl391_122
| ~ spl391_123
| ~ spl391_124
| ~ spl391_128 ),
inference(resolution,[],[f21005,f24249]) ).
fof(f24384,plain,
( r1_tarski(sF388,sF386)
| r1_tarski(sF388,sF386)
| ~ spl391_116
| ~ spl391_117
| ~ spl391_120
| ~ spl391_121
| ~ spl391_122
| ~ spl391_123
| ~ spl391_124
| ~ spl391_128 ),
inference(forward_demodulation,[],[f24383,f23820]) ).
fof(f24385,plain,
( r1_tarski(sF388,sF386)
| ~ spl391_116
| ~ spl391_117
| ~ spl391_120
| ~ spl391_121
| ~ spl391_122
| ~ spl391_123
| ~ spl391_124
| ~ spl391_128 ),
inference(duplicate_literal_removal,[],[f24384]) ).
fof(f24387,definition,
( spl391_155
<=> r1_tarski(sF388,sF386) ),
introduced(definition,[new_symbols(definition,[spl391_155])],[avatar_definition]) ).
fof(f24389,plain,
( r1_tarski(sF388,sF386)
| ~ spl391_155 ),
inference(avatar_component_clause,[],[f24387]) ).
fof(f24390,plain,
( spl391_155
| ~ spl391_116
| ~ spl391_117
| ~ spl391_120
| ~ spl391_121
| ~ spl391_122
| ~ spl391_123
| ~ spl391_124
| ~ spl391_128 ),
inference(avatar_split_clause,[],[f24385,f23867,f23828,f23823,f23818,f23813,f23808,f23793,f23788,f24387]) ).
fof(f24394,plain,
( ~ r1_tarski(sF386,sF388)
| sF386 = sF388
| ~ spl391_155 ),
inference(resolution,[],[f24389,f21332]) ).
fof(f24395,plain,
( ~ r1_tarski(sF386,sF388)
| spl391_118
| ~ spl391_155 ),
inference(forward_subsumption_resolution,[],[f24394,f23800]) ).
fof(f24402,definition,
( spl391_157
<=> r1_tarski(sF386,sF388) ),
introduced(definition,[new_symbols(definition,[spl391_157])],[avatar_definition]) ).
fof(f24404,plain,
( ~ r1_tarski(sF386,sF388)
| spl391_157 ),
inference(avatar_component_clause,[],[f24402]) ).
fof(f24405,plain,
( ~ spl391_157
| spl391_118
| ~ spl391_155 ),
inference(avatar_split_clause,[],[f24395,f24387,f23798,f24402]) ).
fof(f24685,plain,
( ! [X0] :
( ~ r2_hidden(X0,sK32)
| m1_subset_1(X0,sF389) )
| ~ spl391_116
| ~ spl391_124 ),
inference(resolution,[],[f23948,f23790]) ).
fof(f27807,plain,
( ! [X0] :
( r2_hidden(sK112(sF386,X0),sF388)
| r1_tarski(sF386,X0) )
| ~ spl391_137 ),
inference(resolution,[],[f24031,f21335]) ).
fof(f27830,plain,
( r1_tarski(sF386,sF388)
| r1_tarski(sF386,sF388)
| ~ spl391_137 ),
inference(resolution,[],[f27807,f21336]) ).
fof(f27839,plain,
( r1_tarski(sF386,sF388)
| ~ spl391_137 ),
inference(duplicate_literal_removal,[],[f27830]) ).
fof(f27849,plain,
( $false
| ~ spl391_137
| spl391_157 ),
inference(forward_subsumption_resolution,[],[f27839,f24404]) ).
fof(f27850,plain,
( ~ spl391_137
| spl391_157 ),
inference(avatar_contradiction_clause,[],[f27849]) ).
fof(f36379,plain,
( ! [X2,X0,X1] :
( ~ r2_hidden(sK44(X2,sK74(X0,X1,sK33)),sK32)
| ~ r2_hidden(sK74(X0,X1,sK33),k3_tarski(X2))
| r2_hidden(X0,sF388)
| ~ r2_hidden(X0,k9_relat_1(sK33,X1)) )
| ~ spl391_116
| ~ spl391_117
| ~ spl391_121
| ~ spl391_122
| ~ spl391_123
| ~ spl391_124 ),
inference(forward_subsumption_resolution,[],[f24127,f24685]) ).
fof(f36609,plain,
( ! [X0,X1] :
( ~ r2_hidden(sK74(X0,X1,sK33),k3_tarski(sK32))
| r2_hidden(X0,sF388)
| ~ r2_hidden(X0,k9_relat_1(sK33,X1))
| ~ r2_hidden(sK74(X0,X1,sK33),k3_tarski(sK32)) )
| ~ spl391_116
| ~ spl391_117
| ~ spl391_121
| ~ spl391_122
| ~ spl391_123
| ~ spl391_124 ),
inference(resolution,[],[f36379,f23019]) ).
fof(f36610,plain,
( ! [X0,X1] :
( ~ r2_hidden(sK74(X0,X1,sK33),k3_tarski(sK32))
| r2_hidden(X0,sF388)
| ~ r2_hidden(X0,k9_relat_1(sK33,X1)) )
| ~ spl391_116
| ~ spl391_117
| ~ spl391_121
| ~ spl391_122
| ~ spl391_123
| ~ spl391_124 ),
inference(duplicate_literal_removal,[],[f36609]) ).
fof(f36611,plain,
( ! [X0,X1] :
( ~ r2_hidden(sK74(X0,X1,sK33),sF385)
| r2_hidden(X0,sF388)
| ~ r2_hidden(X0,k9_relat_1(sK33,X1)) )
| ~ spl391_116
| ~ spl391_117
| ~ spl391_121
| ~ spl391_122
| ~ spl391_123
| ~ spl391_124
| ~ spl391_128 ),
inference(forward_demodulation,[],[f36610,f23869]) ).
fof(f36612,plain,
( ! [X0] :
( r2_hidden(X0,sF388)
| ~ r2_hidden(X0,k9_relat_1(sK33,sF385))
| ~ r2_hidden(X0,k9_relat_1(sK33,sF385))
| ~ v1_relat_1(sK33) )
| ~ spl391_116
| ~ spl391_117
| ~ spl391_121
| ~ spl391_122
| ~ spl391_123
| ~ spl391_124
| ~ spl391_128 ),
inference(resolution,[],[f36611,f21148]) ).
fof(f36615,plain,
( ! [X0] :
( r2_hidden(X0,sF388)
| ~ r2_hidden(X0,k9_relat_1(sK33,sF385))
| ~ v1_relat_1(sK33) )
| ~ spl391_116
| ~ spl391_117
| ~ spl391_121
| ~ spl391_122
| ~ spl391_123
| ~ spl391_124
| ~ spl391_128 ),
inference(duplicate_literal_removal,[],[f36612]) ).
fof(f36617,plain,
( ! [X0] :
( r2_hidden(X0,sF388)
| ~ r2_hidden(X0,k9_relat_1(sK33,sF385)) )
| ~ spl391_116
| ~ spl391_117
| ~ spl391_121
| ~ spl391_122
| ~ spl391_123
| ~ spl391_124
| ~ spl391_128 ),
inference(forward_subsumption_resolution,[],[f36615,f23795]) ).
fof(f36618,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF386)
| r2_hidden(X0,sF388) )
| ~ spl391_116
| ~ spl391_117
| ~ spl391_120
| ~ spl391_121
| ~ spl391_122
| ~ spl391_123
| ~ spl391_124
| ~ spl391_128 ),
inference(forward_demodulation,[],[f36617,f23810]) ).
fof(f37548,plain,
( spl391_137
| ~ spl391_116
| ~ spl391_117
| ~ spl391_120
| ~ spl391_121
| ~ spl391_122
| ~ spl391_123
| ~ spl391_124
| ~ spl391_128 ),
inference(avatar_split_clause,[],[f36618,f23867,f23828,f23823,f23818,f23813,f23808,f23793,f23788,f24030]) ).
cnf(s122,plain,
spl391_116,
inference(sat_conversion,[],[f23791]) ).
cnf(s123,plain,
spl391_117,
inference(sat_conversion,[],[f23796]) ).
cnf(s124,plain,
~ spl391_118,
inference(sat_conversion,[],[f23801]) ).
cnf(s125,plain,
spl391_119,
inference(sat_conversion,[],[f23806]) ).
cnf(s126,plain,
spl391_120,
inference(sat_conversion,[],[f23811]) ).
cnf(s127,plain,
spl391_121,
inference(sat_conversion,[],[f23816]) ).
cnf(s128,plain,
spl391_122,
inference(sat_conversion,[],[f23821]) ).
cnf(s129,plain,
spl391_123,
inference(sat_conversion,[],[f23826]) ).
cnf(s130,plain,
spl391_124,
inference(sat_conversion,[],[f23831]) ).
cnf(s132,plain,
( ~ spl391_116
| ~ spl391_119
| ~ spl391_123
| ~ spl391_124
| spl391_128 ),
inference(sat_conversion,[],[f23870]) ).
cnf(s159,plain,
( ~ spl391_116
| ~ spl391_117
| ~ spl391_120
| ~ spl391_121
| ~ spl391_122
| ~ spl391_123
| ~ spl391_124
| ~ spl391_128
| spl391_155 ),
inference(sat_conversion,[],[f24390]) ).
cnf(s161,plain,
( spl391_118
| ~ spl391_155
| ~ spl391_157 ),
inference(sat_conversion,[],[f24405]) ).
cnf(s433,plain,
( ~ spl391_137
| spl391_157 ),
inference(sat_conversion,[],[f27850]) ).
cnf(s1145,plain,
( ~ spl391_116
| ~ spl391_117
| ~ spl391_120
| ~ spl391_121
| ~ spl391_122
| ~ spl391_123
| ~ spl391_124
| ~ spl391_128
| spl391_137 ),
inference(sat_conversion,[],[f37548]) ).
cnf(s1177,plain,
spl391_128,
inference(rat,[],[s132,s125,s130,s129,s122]) ).
cnf(s1194,plain,
spl391_137,
inference(rat,[],[s1145,s122,s123,s130,s129,s128,s127,s126,s1177]) ).
cnf(s1196,plain,
spl391_155,
inference(rat,[],[s159,s122,s123,s130,s129,s128,s127,s126,s1177]) ).
cnf(s1202,plain,
spl391_157,
inference(rat,[],[s433,s1194]) ).
cnf(s1204,plain,
$false,
inference(rat,[],[s161,s124,s1202,s1196]) ).
fof(f37567,plain,
$false,
inference(avatar_sat_refutation,[],[s1204]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU421+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.37 % Computer : n020.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Mon Sep 28 05:20:07 UTC 2026
% 0.16/0.38 % CPUTime :
% 0.16/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.16/0.40 Running first-order theorem proving
% 0.16/0.40 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
% 14.43/3.94 % (4046921)Detected formulas, will run a generic FOF schedule.
% 14.43/3.94 % (4046928)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=1835667121:i=141695:sd=1:nm=32:gsp=on:ss=included_2989 on theBenchmark for (2989ds/141695Mi)
% 14.43/3.94 % (4046930)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3212517097:i=119:av=off:ss=axioms_2989 on theBenchmark for (2989ds/119Mi)
% 14.43/3.94 % (4046929)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3301677704:i=109:sd=1:ins=1:gsp=on:ss=axioms_2989 on theBenchmark for (2989ds/109Mi)
% 14.43/3.94 % (4046926)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=3363690687:i=141193_2989 on theBenchmark for (2989ds/141193Mi)
% 14.43/3.94 % (4046927)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=2467083452:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2989 on theBenchmark for (2989ds/134677Mi)
% 14.43/3.94 % (4046931)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=856733399:s2a=on:i=139:gtg=position_2989 on theBenchmark for (2989ds/139Mi)
% 14.43/3.94 % (4046932)dis-21_1_sil=8000:lcm=predicate:random_seed=3958166326:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2989 on theBenchmark for (2989ds/129Mi)
% 14.43/3.94 % (4046931)Instruction limit reached!
% 14.43/3.94 % (4046931)------------------------------
% 14.43/3.94 % (4046931)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.43/3.94 % (4046931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.43/3.94 % (4046931)CaDiCaL version: 2.1.3
% 14.43/3.94 % (4046931)Termination reason: Instruction limit
% 14.43/3.94 % (4046931)Termination phase: Property scanning
% 14.43/3.94 % (4046931)Time elapsed: 0.059 s
% 14.43/3.94 % (4046931)Peak memory usage: 112 MB
% 14.43/3.94 % (4046931)Instructions burned: 140 (million)
% 14.43/3.94 % (4046929)Instruction limit reached!
% 14.43/3.94 % (4046929)------------------------------
% 14.43/3.94 % (4046929)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.43/3.94 % (4046929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.43/3.94 % (4046929)CaDiCaL version: 2.1.3
% 14.43/3.94 % (4046929)Termination reason: Instruction limit
% 14.43/3.94 % (4046929)Termination phase: SInE selection
% 14.43/3.94 % (4046929)Time elapsed: 0.081 s
% 14.43/3.94 % (4046929)Peak memory usage: 112 MB
% 14.43/3.94 % (4046929)Instructions burned: 109 (million)
% 14.43/3.94 % (4046930)Instruction limit reached!
% 14.43/3.94 % (4046930)------------------------------
% 14.43/3.94 % (4046930)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.43/3.94 % (4046930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.43/3.94 % (4046930)CaDiCaL version: 2.1.3
% 14.43/3.94 % (4046930)Termination reason: Instruction limit
% 14.43/3.94 % (4046930)Termination phase: Preprocessing 1
% 14.43/3.94 % (4046930)Time elapsed: 0.098 s
% 14.43/3.94 % (4046930)Peak memory usage: 113 MB
% 14.43/3.94 % (4046930)Instructions burned: 119 (million)
% 14.43/3.94 % (4046932)Instruction limit reached!
% 14.43/3.94 % (4046932)------------------------------
% 14.43/3.94 % (4046932)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.43/3.94 % (4046932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.43/3.94 % (4046932)CaDiCaL version: 2.1.3
% 14.43/3.94 % (4046932)Termination reason: Instruction limit
% 14.43/3.94 % (4046932)Termination phase: SInE selection
% 14.43/3.94 % (4046932)Time elapsed: 0.090 s
% 14.43/3.94 % (4046932)Peak memory usage: 112 MB
% 14.43/3.94 % (4046932)Instructions burned: 129 (million)
% 14.43/3.94 % (4046940)lrs+10_1_sil=8000:sp=occurrence:random_seed=2358106298:i=285:sd=3:ss=axioms:sgt=8_2986 on theBenchmark for (2986ds/285Mi)
% 14.43/3.94 % (4046942)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1740660554:i=325:sd=1:ss=axioms:sgt=32_2986 on theBenchmark for (2986ds/325Mi)
% 14.43/3.94 % (4046941)lrs+10_1_sil=32000:urr=on:br=off:random_seed=531339593:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2986 on theBenchmark for (2986ds/157Mi)
% 14.43/3.94 % (4046943)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=980988357:s2a=on:i=248:s2at=1.23:gtg=position_2986 on theBenchmark for (2986ds/248Mi)
% 14.43/3.94 % (4046941)Instruction limit reached!
% 21.68/4.90 % (4046941)------------------------------
% 21.68/4.90 % (4046941)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.68/4.90 % (4046941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.68/4.90 % (4046941)CaDiCaL version: 2.1.3
% 21.68/4.90 % (4046941)Termination reason: Instruction limit
% 21.68/4.90 % (4046941)Termination phase: Property scanning
% 21.68/4.90 % (4046941)Time elapsed: 0.068 s
% 21.68/4.90 % (4046941)Peak memory usage: 112 MB
% 21.68/4.90 % (4046941)Instructions burned: 158 (million)
% 21.68/4.90 % (4046943)Instruction limit reached!
% 21.68/4.90 % (4046943)------------------------------
% 21.68/4.90 % (4046943)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.68/4.90 % (4046943)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.68/4.90 % (4046943)CaDiCaL version: 2.1.3
% 21.68/4.90 % (4046943)Termination reason: Instruction limit
% 21.68/4.90 % (4046943)Termination phase: Property scanning
% 21.68/4.90 % (4046943)Time elapsed: 0.107 s
% 21.68/4.90 % (4046943)Peak memory usage: 112 MB
% 21.68/4.90 % (4046943)Instructions burned: 249 (million)
% 21.68/4.90 % (4046940)Instruction limit reached!
% 21.68/4.90 % (4046940)------------------------------
% 21.68/4.90 % (4046940)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.68/4.90 % (4046940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.68/4.90 % (4046940)CaDiCaL version: 2.1.3
% 21.68/4.90 % (4046940)Termination reason: Instruction limit
% 21.68/4.90 % (4046940)Termination phase: Saturation
% 21.68/4.90 % (4046940)Time elapsed: 0.199 s
% 21.68/4.90 % (4046940)Peak memory usage: 119 MB
% 21.68/4.90 % (4046940)Instructions burned: 286 (million)
% 21.68/4.90 % (4046948)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1518507948:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2984 on theBenchmark for (2984ds/294Mi)
% 21.68/4.90 % (4046942)Instruction limit reached!
% 21.68/4.90 % (4046942)------------------------------
% 21.68/4.90 % (4046942)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.68/4.90 % (4046942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.68/4.90 % (4046942)CaDiCaL version: 2.1.3
% 21.68/4.90 % (4046942)Termination reason: Instruction limit
% 21.68/4.90 % (4046942)Termination phase: Saturation
% 21.68/4.90 % (4046942)Time elapsed: 0.250 s
% 21.68/4.90 % (4046942)Peak memory usage: 120 MB
% 21.68/4.90 % (4046942)Instructions burned: 326 (million)
% 21.68/4.90 % (4046949)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1879542260:i=2350_2984 on theBenchmark for (2984ds/2350Mi)
% 21.68/4.90 % (4046950)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2223834708:cts=off:i=113:fsr=off:ss=included:sgt=4_2983 on theBenchmark for (2983ds/113Mi)
% 21.68/4.90 % (4046952)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=4039275501:i=127:av=off:fsr=off:sup=off_2982 on theBenchmark for (2982ds/127Mi)
% 21.68/4.90 % (4046950)Instruction limit reached!
% 21.68/4.90 % (4046950)------------------------------
% 21.68/4.90 % (4046950)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.68/4.90 % (4046950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.68/4.90 % (4046950)CaDiCaL version: 2.1.3
% 21.68/4.90 % (4046950)Termination reason: Instruction limit
% 21.68/4.90 % (4046950)Termination phase: SInE selection
% 21.68/4.90 % (4046950)Time elapsed: 0.089 s
% 21.68/4.90 % (4046950)Peak memory usage: 112 MB
% 21.68/4.90 % (4046950)Instructions burned: 114 (million)
% 21.68/4.90 % (4046948)Instruction limit reached!
% 21.68/4.90 % (4046948)------------------------------
% 21.68/4.90 % (4046948)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.68/4.90 % (4046948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.68/4.90 % (4046948)CaDiCaL version: 2.1.3
% 21.68/4.90 % (4046948)Termination reason: Instruction limit
% 21.68/4.90 % (4046948)Termination phase: Property scanning
% 21.68/4.90 % (4046948)Time elapsed: 0.217 s
% 21.68/4.90 % (4046948)Peak memory usage: 119 MB
% 21.68/4.90 % (4046948)Instructions burned: 295 (million)
% 21.68/4.90 % (4046952)Instruction limit reached!
% 21.68/4.90 % (4046952)------------------------------
% 21.68/4.90 % (4046952)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.68/4.90 % (4046952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.68/4.90 % (4046952)CaDiCaL version: 2.1.3
% 61.49/10.46 % (4046952)Termination reason: Instruction limit
% 61.49/10.46 % (4046952)Termination phase: Preprocessing 1
% 61.49/10.46 % (4046952)Time elapsed: 0.091 s
% 61.49/10.46 % (4046952)Peak memory usage: 113 MB
% 61.49/10.46 % (4046952)Instructions burned: 128 (million)
% 61.49/10.46 % (4046956)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2452956561:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2981 on theBenchmark for (2981ds/114Mi)
% 61.49/10.46 % (4046957)lrs+10_1_sil=8000:sp=occurrence:random_seed=69960195:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2981 on theBenchmark for (2981ds/907Mi)
% 61.49/10.46 % (4046956)Instruction limit reached!
% 61.49/10.46 % (4046956)------------------------------
% 61.49/10.46 % (4046956)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.49/10.46 % (4046956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.49/10.46 % (4046956)CaDiCaL version: 2.1.3
% 61.49/10.46 % (4046956)Termination reason: Instruction limit
% 61.49/10.46 % (4046956)Termination phase: Property scanning
% 61.49/10.46 % (4046956)Time elapsed: 0.050 s
% 61.49/10.46 % (4046956)Peak memory usage: 112 MB
% 61.49/10.46 % (4046956)Instructions burned: 116 (million)
% 61.49/10.46 % (4046958)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1431478812:i=437:sd=1:aac=none:ss=included_2980 on theBenchmark for (2980ds/437Mi)
% 61.49/10.46 % (4046961)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1705959487:i=5202:ss=axioms:sgt=16_2979 on theBenchmark for (2979ds/5202Mi)
% 61.49/10.46 % (4046958)Instruction limit reached!
% 61.49/10.46 % (4046958)------------------------------
% 61.49/10.46 % (4046958)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.49/10.46 % (4046958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.49/10.46 % (4046958)CaDiCaL version: 2.1.3
% 61.49/10.46 % (4046958)Termination reason: Instruction limit
% 61.49/10.46 % (4046958)Termination phase: Saturation
% 61.49/10.46 % (4046958)Time elapsed: 0.297 s
% 61.49/10.46 % (4046958)Peak memory usage: 120 MB
% 61.49/10.46 % (4046958)Instructions burned: 440 (million)
% 61.49/10.46 % (4046964)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2472159202:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2976 on theBenchmark for (2976ds/134Mi)
% 61.49/10.46 % (4046957)Instruction limit reached!
% 61.49/10.46 % (4046957)------------------------------
% 61.49/10.46 % (4046957)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.49/10.46 % (4046957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.49/10.46 % (4046957)CaDiCaL version: 2.1.3
% 61.49/10.46 % (4046957)Termination reason: Instruction limit
% 61.49/10.46 % (4046957)Termination phase: Saturation
% 61.49/10.46 % (4046957)Time elapsed: 0.525 s
% 61.49/10.46 % (4046957)Peak memory usage: 131 MB
% 61.49/10.46 % (4046957)Instructions burned: 908 (million)
% 61.49/10.46 % (4046964)Instruction limit reached!
% 61.49/10.46 % (4046964)------------------------------
% 61.49/10.46 % (4046964)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.49/10.46 % (4046964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.49/10.46 % (4046964)CaDiCaL version: 2.1.3
% 61.49/10.46 % (4046964)Termination reason: Instruction limit
% 61.49/10.46 % (4046964)Termination phase: NewCNF
% 61.49/10.46 % (4046964)Time elapsed: 0.116 s
% 61.49/10.46 % (4046964)Peak memory usage: 115 MB
% 61.49/10.46 % (4046964)Instructions burned: 134 (million)
% 61.49/10.46 % (4046966)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=4121094206:st=8:i=592:sd=3:ep=RST:ss=axioms_2974 on theBenchmark for (2974ds/592Mi)
% 61.49/10.46 % (4046967)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1403433838:st=3:i=13193:sd=3:ss=axioms_2973 on theBenchmark for (2973ds/13193Mi)
% 61.49/10.46 % (4046949)Instruction limit reached!
% 61.49/10.46 % (4046949)------------------------------
% 61.49/10.46 % (4046949)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.49/10.46 % (4046949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.49/10.46 % (4046949)CaDiCaL version: 2.1.3
% 61.49/10.46 % (4046949)Termination reason: Instruction limit
% 61.49/10.46 % (4046949)Termination phase: Property scanning
% 61.49/10.46 % (4046949)Time elapsed: 1.251 s
% 61.49/10.46 % (4046949)Peak memory usage: 171 MB
% 61.49/10.46 % (4046949)Instructions burned: 2351 (million)
% 61.49/10.46 % (4046966)Instruction limit reached!
% 61.49/10.46 % (4046966)------------------------------
% 61.49/10.46 % (4046966)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 92.03/14.70 % (4046966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.03/14.70 % (4046966)CaDiCaL version: 2.1.3
% 92.03/14.70 % (4046966)Termination reason: Instruction limit
% 92.03/14.70 % (4046966)Termination phase: Preprocessing 3
% 92.03/14.70 % (4046966)Time elapsed: 0.440 s
% 92.03/14.70 % (4046966)Peak memory usage: 135 MB
% 92.03/14.70 % (4046966)Instructions burned: 592 (million)
% 92.03/14.70 % (4046970)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=3499257169:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2969 on theBenchmark for (2969ds/125Mi)
% 92.03/14.70 % (4046970)Instruction limit reached!
% 92.03/14.70 % (4046970)------------------------------
% 92.03/14.70 % (4046970)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 92.03/14.70 % (4046970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.03/14.70 % (4046970)CaDiCaL version: 2.1.3
% 92.03/14.70 % (4046970)Termination reason: Instruction limit
% 92.03/14.70 % (4046970)Termination phase: Property scanning
% 92.03/14.70 % (4046970)Time elapsed: 0.055 s
% 92.03/14.70 % (4046970)Peak memory usage: 112 MB
% 92.03/14.70 % (4046970)Instructions burned: 125 (million)
% 92.03/14.70 % (4046971)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3221529592:i=134:gtgl=5:slsql=off:gtg=exists_sym_2968 on theBenchmark for (2968ds/134Mi)
% 92.03/14.70 % (4046971)Instruction limit reached!
% 92.03/14.70 % (4046971)------------------------------
% 92.03/14.70 % (4046971)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 92.03/14.70 % (4046971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.03/14.70 % (4046971)CaDiCaL version: 2.1.3
% 92.03/14.70 % (4046971)Termination reason: Instruction limit
% 92.03/14.70 % (4046971)Termination phase: Property scanning
% 92.03/14.70 % (4046971)Time elapsed: 0.059 s
% 92.03/14.70 % (4046971)Peak memory usage: 112 MB
% 92.03/14.70 % (4046971)Instructions burned: 138 (million)
% 92.03/14.70 % (4046973)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1450891643:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2967 on theBenchmark for (2967ds/141Mi)
% 92.03/14.70 % (4046975)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1168982760:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2967 on theBenchmark for (2967ds/431Mi)
% 92.03/14.70 % (4046973)Instruction limit reached!
% 92.03/14.70 % (4046973)------------------------------
% 92.03/14.70 % (4046973)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 92.03/14.70 % (4046973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.03/14.70 % (4046973)CaDiCaL version: 2.1.3
% 92.03/14.70 % (4046973)Termination reason: Instruction limit
% 92.03/14.70 % (4046973)Termination phase: Saturation
% 92.03/14.70 % (4046973)Time elapsed: 0.120 s
% 92.03/14.70 % (4046973)Peak memory usage: 117 MB
% 92.03/14.70 % (4046973)Instructions burned: 141 (million)
% 92.03/14.70 % (4046975)Refutation not found, incomplete strategy
% 92.03/14.70 % (4046975)------------------------------
% 92.03/14.70 % (4046975)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 92.03/14.70 % (4046975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.03/14.70 % (4046975)CaDiCaL version: 2.1.3
% 92.03/14.70 % (4046975)Termination reason: Refutation not found, incomplete strategy
% 92.03/14.70 % (4046975)Time elapsed: 0.116 s
% 92.03/14.70 % (4046975)Peak memory usage: 117 MB
% 92.03/14.70 % (4046975)Instructions burned: 129 (million)
% 92.03/14.70 % (4046978)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=2396034052:i=6060:aac=none:ins=25_2965 on theBenchmark for (2965ds/6060Mi)
% 92.03/14.70 % (4046975)------------------------------
% 92.03/14.70 % (4046975)------------------------------
% 92.03/14.70 % (4046980)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=2642050154:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2961 on theBenchmark for (2961ds/150Mi)
% 92.03/14.70 % (4046980)Instruction limit reached!
% 92.03/14.70 % (4046980)------------------------------
% 92.03/14.70 % (4046980)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 92.03/14.70 % (4046980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 131.69/20.31 % (4046980)CaDiCaL version: 2.1.3
% 131.69/20.31 % (4046980)Termination reason: Instruction limit
% 131.69/20.31 % (4046980)Termination phase: Preprocessing 1
% 131.69/20.31 % (4046980)Time elapsed: 0.123 s
% 131.69/20.31 % (4046980)Peak memory usage: 113 MB
% 131.69/20.31 % (4046980)Instructions burned: 151 (million)
% 131.69/20.31 % (4046982)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2964577000:i=14155:bd=all_2959 on theBenchmark for (2959ds/14155Mi)
% 131.69/20.31 % (4046961)Instruction limit reached!
% 131.69/20.31 % (4046961)------------------------------
% 131.69/20.31 % (4046961)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 131.69/20.31 % (4046961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 131.69/20.31 % (4046961)CaDiCaL version: 2.1.3
% 131.69/20.31 % (4046961)Termination reason: Instruction limit
% 131.69/20.31 % (4046961)Termination phase: Saturation
% 131.69/20.31 % (4046961)Time elapsed: 3.251 s
% 131.69/20.31 % (4046961)Peak memory usage: 201 MB
% 131.69/20.31 % (4046961)Instructions burned: 5203 (million)
% 131.69/20.31 % (4046984)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2623230099:i=667:av=off:fsr=off_2945 on theBenchmark for (2945ds/667Mi)
% 131.69/20.31 % (4046984)Instruction limit reached!
% 131.69/20.31 % (4046984)------------------------------
% 131.69/20.31 % (4046984)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 131.69/20.31 % (4046984)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 131.69/20.31 % (4046984)CaDiCaL version: 2.1.3
% 131.69/20.31 % (4046984)Termination reason: Instruction limit
% 131.69/20.31 % (4046984)Termination phase: NewCNF
% 131.69/20.31 % (4046984)Time elapsed: 0.510 s
% 131.69/20.31 % (4046984)Peak memory usage: 149 MB
% 131.69/20.31 % (4046984)Instructions burned: 667 (million)
% 131.69/20.31 % (4046986)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=1341086725:s2a=on:i=185:s2at=1.8:fdi=4_2939 on theBenchmark for (2939ds/185Mi)
% 131.69/20.31 % (4046986)Instruction limit reached!
% 131.69/20.31 % (4046986)------------------------------
% 131.69/20.31 % (4046986)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 131.69/20.31 % (4046986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 131.69/20.31 % (4046986)CaDiCaL version: 2.1.3
% 131.69/20.31 % (4046986)Termination reason: Instruction limit
% 131.69/20.31 % (4046986)Termination phase: SInE selection
% 131.69/20.31 % (4046986)Time elapsed: 0.147 s
% 131.69/20.31 % (4046986)Peak memory usage: 113 MB
% 131.69/20.31 % (4046986)Instructions burned: 185 (million)
% 131.69/20.31 % (4046988)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=1033069694:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2936 on theBenchmark for (2936ds/193Mi)
% 131.69/20.31 % (4046988)Instruction limit reached!
% 131.69/20.31 % (4046988)------------------------------
% 131.69/20.31 % (4046988)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 131.69/20.31 % (4046988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 131.69/20.31 % (4046988)CaDiCaL version: 2.1.3
% 131.69/20.31 % (4046988)Termination reason: Instruction limit
% 131.69/20.31 % (4046988)Termination phase: SInE selection
% 131.69/20.31 % (4046988)Time elapsed: 0.155 s
% 131.69/20.31 % (4046988)Peak memory usage: 112 MB
% 131.69/20.31 % (4046988)Instructions burned: 194 (million)
% 131.69/20.31 % (4046990)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=3869406192:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2933 on theBenchmark for (2933ds/4850Mi)
% 131.69/20.31 % (4046978)Instruction limit reached!
% 131.69/20.31 % (4046978)------------------------------
% 131.69/20.31 % (4046978)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 131.69/20.31 % (4046978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 131.69/20.31 % (4046978)CaDiCaL version: 2.1.3
% 131.69/20.31 % (4046978)Termination reason: Instruction limit
% 131.69/20.31 % (4046978)Termination phase: Saturation
% 131.69/20.31 % (4046978)Time elapsed: 4.583 s
% 131.69/20.31 % (4046978)Peak memory usage: 559 MB
% 131.69/20.31 % (4046978)Instructions burned: 6060 (million)
% 131.69/20.31 % (4046992)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=2863081429:i=12111:sd=1:ss=included_2917 on theBenchmark for (2917ds/12111Mi)
% 131.69/20.31 % (4046990)Instruction limit reached!
% 131.69/20.31 % (4046990)------------------------------
% 131.69/20.31 % (4046990)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 160.08/24.32 % (4046990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 160.08/24.32 % (4046990)CaDiCaL version: 2.1.3
% 160.08/24.32 % (4046990)Termination reason: Instruction limit
% 160.08/24.32 % (4046990)Termination phase: Saturation
% 160.08/24.32 % (4046990)Time elapsed: 2.826 s
% 160.08/24.32 % (4046990)Peak memory usage: 222 MB
% 160.08/24.32 % (4046990)Instructions burned: 4852 (million)
% 160.08/24.32 % (4046994)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2551633791:i=319:kws=precedence:fsr=off_2903 on theBenchmark for (2903ds/319Mi)
% 160.08/24.32 % (4046994)Instruction limit reached!
% 160.08/24.32 % (4046994)------------------------------
% 160.08/24.32 % (4046994)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 160.08/24.32 % (4046994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 160.08/24.32 % (4046994)CaDiCaL version: 2.1.3
% 160.08/24.32 % (4046994)Termination reason: Instruction limit
% 160.08/24.32 % (4046994)Termination phase: Naming
% 160.08/24.32 % (4046994)Time elapsed: 0.253 s
% 160.08/24.32 % (4046994)Peak memory usage: 135 MB
% 160.08/24.32 % (4046994)Instructions burned: 320 (million)
% 160.08/24.32 % (4046996)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=3220733559:i=2064:ep=RST_2899 on theBenchmark for (2899ds/2064Mi)
% 160.08/24.32 % (4046967)Instruction limit reached!
% 160.08/24.32 % (4046967)------------------------------
% 160.08/24.32 % (4046967)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 160.08/24.32 % (4046967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 160.08/24.32 % (4046967)CaDiCaL version: 2.1.3
% 160.08/24.32 % (4046967)Termination reason: Instruction limit
% 160.08/24.32 % (4046967)Termination phase: Saturation
% 160.08/24.32 % (4046967)Time elapsed: 8.126 s
% 160.08/24.32 % (4046967)Peak memory usage: 342 MB
% 160.08/24.32 % (4046967)Instructions burned: 13194 (million)
% 160.08/24.32 % (4046998)dis-1011_128_sil=32000:random_seed=2150901540:i=3706:ep=RST:av=off_2890 on theBenchmark for (2890ds/3706Mi)
% 160.08/24.32 % (4046996)Instruction limit reached!
% 160.08/24.32 % (4046996)------------------------------
% 160.08/24.32 % (4046996)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 160.08/24.32 % (4046996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 160.08/24.32 % (4046996)CaDiCaL version: 2.1.3
% 160.08/24.32 % (4046996)Termination reason: Instruction limit
% 160.08/24.32 % (4046996)Termination phase: Property scanning
% 160.08/24.32 % (4046996)Time elapsed: 1.087 s
% 160.08/24.32 % (4046996)Peak memory usage: 171 MB
% 160.08/24.32 % (4046996)Instructions burned: 2067 (million)
% 160.08/24.32 % (4047000)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=3836965117:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2887 on theBenchmark for (2887ds/757Mi)
% 160.08/24.32 % (4047000)Instruction limit reached!
% 160.08/24.32 % (4047000)------------------------------
% 160.08/24.32 % (4047000)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 160.08/24.32 % (4047000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 160.08/24.32 % (4047000)CaDiCaL version: 2.1.3
% 160.08/24.32 % (4047000)Termination reason: Instruction limit
% 160.08/24.32 % (4047000)Termination phase: Saturation
% 160.08/24.32 % (4047000)Time elapsed: 0.514 s
% 160.08/24.32 % (4047000)Peak memory usage: 128 MB
% 160.08/24.32 % (4047000)Instructions burned: 757 (million)
% 160.08/24.32 % (4047002)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=3229669132:i=13913:ss=axioms:sgt=8_2880 on theBenchmark for (2880ds/13913Mi)
% 160.08/24.32 % (4046998)Instruction limit reached!
% 160.08/24.32 % (4046998)------------------------------
% 160.08/24.32 % (4046998)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 160.08/24.32 % (4046998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 160.08/24.32 % (4046998)CaDiCaL version: 2.1.3
% 160.08/24.32 % (4046998)Termination reason: Instruction limit
% 160.08/24.32 % (4046998)Termination phase: Saturation
% 160.08/24.32 % (4046998)Time elapsed: 1.823 s
% 160.08/24.32 % (4046998)Peak memory usage: 186 MB
% 160.08/24.32 % (4046998)Instructions burned: 3706 (million)
% 160.08/24.32 % (4047004)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=2410573535:i=9925:aac=none_2871 on theBenchmark for (2871ds/9925Mi)
% 160.08/24.32 % (4046982)Instruction limit reached!
% 160.08/24.32 % (4046982)------------------------------
% 160.08/24.32 % (4046982)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 190.01/28.58 % (4046982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 190.01/28.58 % (4046982)CaDiCaL version: 2.1.3
% 190.01/28.58 % (4046982)Termination reason: Instruction limit
% 190.01/28.58 % (4046982)Termination phase: Saturation
% 190.01/28.58 % (4046982)Time elapsed: 9.647 s
% 190.01/28.58 % (4046982)Peak memory usage: 753 MB
% 190.01/28.58 % (4046982)Instructions burned: 14159 (million)
% 190.01/28.58 % (4047006)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=2029976686:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2860 on theBenchmark for (2860ds/2479Mi)
% 190.01/28.58 % (4047006)Instruction limit reached!
% 190.01/28.58 % (4047006)------------------------------
% 190.01/28.58 % (4047006)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 190.01/28.58 % (4047006)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 190.01/28.58 % (4047006)CaDiCaL version: 2.1.3
% 190.01/28.58 % (4047006)Termination reason: Instruction limit
% 190.01/28.58 % (4047006)Termination phase: Saturation
% 190.01/28.58 % (4047006)Time elapsed: 1.499 s
% 190.01/28.58 % (4047006)Peak memory usage: 138 MB
% 190.01/28.58 % (4047006)Instructions burned: 2479 (million)
% 190.01/28.58 % (4047008)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=2526502998:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2844 on theBenchmark for (2844ds/440Mi)
% 190.01/28.58 % (4047008)Instruction limit reached!
% 190.01/28.58 % (4047008)------------------------------
% 190.01/28.58 % (4047008)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 190.01/28.58 % (4047008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 190.01/28.58 % (4047008)CaDiCaL version: 2.1.3
% 190.01/28.58 % (4047008)Termination reason: Instruction limit
% 190.01/28.58 % (4047008)Termination phase: Property scanning
% 190.01/28.58 % (4047008)Time elapsed: 0.198 s
% 190.01/28.58 % (4047008)Peak memory usage: 112 MB
% 190.01/28.58 % (4047008)Instructions burned: 442 (million)
% 190.01/28.58 % (4047010)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=155076926:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2840 on theBenchmark for (2840ds/11145Mi)
% 190.01/28.58 % (4046992)Instruction limit reached!
% 190.01/28.58 % (4046992)------------------------------
% 190.01/28.58 % (4046992)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 190.01/28.58 % (4046992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 190.01/28.58 % (4046992)CaDiCaL version: 2.1.3
% 190.01/28.58 % (4046992)Termination reason: Instruction limit
% 190.01/28.58 % (4046992)Termination phase: Saturation
% 190.01/28.58 % (4046992)Time elapsed: 8.537 s
% 190.01/28.58 % (4046992)Peak memory usage: 247 MB
% 190.01/28.58 % (4046992)Instructions burned: 12112 (million)
% 190.01/28.58 % (4047012)lrs+1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_frequency:lcm=reverse:urr=on:bsr=on:random_seed=2355868851:cts=off:i=3034:av=off:er=known:fsd=on_2830 on theBenchmark for (2830ds/3034Mi)
% 190.01/28.58 % (4047012)Instruction limit reached!
% 190.01/28.58 % (4047012)------------------------------
% 190.01/28.58 % (4047012)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 190.01/28.58 % (4047012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 190.01/28.58 % (4047012)CaDiCaL version: 2.1.3
% 190.01/28.58 % (4047012)Termination reason: Instruction limit
% 190.01/28.58 % (4047012)Termination phase: Saturation
% 190.01/28.58 % (4047012)Time elapsed: 1.661 s
% 190.01/28.58 % (4047012)Peak memory usage: 190 MB
% 190.01/28.58 % (4047012)Instructions burned: 3035 (million)
% 190.01/28.58 % (4047014)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=3883825395:st=2:s2a=on:i=524:s2at=2:ss=axioms_2812 on theBenchmark for (2812ds/524Mi)
% 190.01/28.58 % (4047014)Instruction limit reached!
% 190.01/28.58 % (4047014)------------------------------
% 190.01/28.58 % (4047014)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 190.01/28.58 % (4047014)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 190.01/28.58 % (4047014)CaDiCaL version: 2.1.3
% 190.01/28.58 % (4047014)Termination reason: Instruction limit
% 190.01/28.58 % (4047014)Termination phase: Preprocessing 1
% 190.01/28.58 % (4047014)Time elapsed: 0.410 s
% 190.01/28.58 % (4047014)Peak memory usage: 114 MB
% 190.01/28.58 % (4047014)Instructions burned: 524 (million)
% 190.01/28.58 % (4047016)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=4079441282:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2806 on theBenchmark for (2806ds/1016Mi)
% 101.51/28.87 % (4047016)Instruction limit reached!
% 101.51/28.87 % (4047016)------------------------------
% 101.51/28.87 % (4047016)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 101.51/28.87 % (4047016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.51/28.87 % (4047016)CaDiCaL version: 2.1.3
% 101.51/28.87 % (4047016)Termination reason: Instruction limit
% 101.51/28.87 % (4047016)Termination phase: Saturation
% 101.51/28.87 % (4047016)Time elapsed: 0.670 s
% 101.51/28.87 % (4047016)Peak memory usage: 129 MB
% 101.51/28.87 % (4047016)Instructions burned: 1017 (million)
% 101.51/28.87 % (4047004)Instruction limit reached!
% 101.51/28.87 % (4047004)------------------------------
% 101.51/28.87 % (4047004)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 101.51/28.87 % (4047004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.51/28.87 % (4047004)CaDiCaL version: 2.1.3
% 101.51/28.87 % (4047004)Termination reason: Instruction limit
% 101.51/28.87 % (4047004)Termination phase: Saturation
% 101.51/28.87 % (4047004)Time elapsed: 7.152 s
% 101.51/28.87 % (4047004)Peak memory usage: 505 MB
% 101.51/28.87 % (4047004)Instructions burned: 9926 (million)
% 101.51/28.87 % (4047018)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=596047156:i=14123:bd=preordered:ins=4_2798 on theBenchmark for (2798ds/14123Mi)
% 101.51/28.87 % (4047019)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=1348268844:i=5781:kws=precedence:bd=all:rawr=on_2798 on theBenchmark for (2798ds/5781Mi)
% 101.51/28.87 % (4047002)Instruction limit reached!
% 101.51/28.87 % (4047002)------------------------------
% 101.51/28.87 % (4047002)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 101.51/28.87 % (4047002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.51/28.87 % (4047002)CaDiCaL version: 2.1.3
% 101.51/28.87 % (4047002)Termination reason: Instruction limit
% 101.51/28.87 % (4047002)Termination phase: Saturation
% 101.51/28.87 % (4047002)Time elapsed: 8.932 s
% 101.51/28.87 % (4047002)Peak memory usage: 278 MB
% 101.51/28.87 % (4047002)Instructions burned: 13913 (million)
% 101.51/28.87 % (4047022)lrs-1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:erd=off:urr=on:br=off:random_seed=3028499701:i=2448:gtgl=5:bd=preordered:gtg=all_2790 on theBenchmark for (2790ds/2448Mi)
% 101.51/28.87 % (4047022)Instruction limit reached!
% 101.51/28.87 % (4047022)------------------------------
% 101.51/28.87 % (4047022)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 101.51/28.87 % (4047022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.51/28.87 % (4047022)CaDiCaL version: 2.1.3
% 101.51/28.87 % (4047022)Termination reason: Instruction limit
% 101.51/28.87 % (4047022)Termination phase: Function definition elimination
% 101.51/28.87 % (4047022)Time elapsed: 1.291 s
% 101.51/28.87 % (4047022)Peak memory usage: 168 MB
% 101.51/28.87 % (4047022)Instructions burned: 2449 (million)
% 101.51/28.87 % (4047024)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=2979257493:i=3223:kws=precedence:fgj=on:av=off_2775 on theBenchmark for (2775ds/3223Mi)
% 101.51/28.87 % (4047019)Instruction limit reached!
% 101.51/28.87 % (4047019)------------------------------
% 101.51/28.87 % (4047019)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 101.51/28.87 % (4047019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.51/28.87 % (4047019)CaDiCaL version: 2.1.3
% 101.51/28.87 % (4047019)Termination reason: Instruction limit
% 101.51/28.87 % (4047019)Termination phase: Saturation
% 101.51/28.87 % (4047019)Time elapsed: 3.009 s
% 101.51/28.87 % (4047019)Peak memory usage: 192 MB
% 101.51/28.87 % (4047019)Instructions burned: 5782 (million)
% 101.51/28.87 % (4047010)Instruction limit reached!
% 101.51/28.87 % (4047010)------------------------------
% 101.51/28.87 % (4047010)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 101.51/28.87 % (4047010)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.51/28.87 % (4047010)CaDiCaL version: 2.1.3
% 101.51/28.87 % (4047010)Termination reason: Instruction limit
% 101.51/28.87 % (4047010)Termination phase: Saturation
% 101.51/28.87 % (4047010)Time elapsed: 7.327 s
% 101.51/28.87 % (4047010)Peak memory usage: 253 MB
% 101.51/28.87 % (4047010)Instructions burned: 11146 (million)
% 101.51/28.87 % (4047026)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=2005468589:st=5.6:i=2033:sd=3:ss=axioms_2766 on theBenchmark for (2766ds/2033Mi)
% 101.51/28.87 % (4047027)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=2237302923:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2765 on theBenchmark for (2765ds/2055Mi)
% 101.51/28.87 % (4047024)Instruction limit reached!
% 101.51/28.87 % (4047024)------------------------------
% 101.51/28.87 % (4047024)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 101.51/28.87 % (4047024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.51/28.87 % (4047024)CaDiCaL version: 2.1.3
% 101.51/28.87 % (4047024)Termination reason: Instruction limit
% 101.51/28.87 % (4047024)Termination phase: Saturation
% 101.51/28.87 % (4047024)Time elapsed: 1.788 s
% 101.51/28.87 % (4047024)Peak memory usage: 216 MB
% 101.51/28.87 % (4047024)Instructions burned: 3224 (million)
% 101.51/28.87 % (4047030)dis+1010_1_ncem=casc2026/models/loop7.pt:sil=64000:tgt=full:npcc=on:fde=unused:sp=const_frequency:spb=goal:acc=on:random_seed=583138127:i=21611:sd=3:ss=axioms_2756 on theBenchmark for (2756ds/21611Mi)
% 101.51/28.87 % (4047026)Instruction limit reached!
% 101.51/28.87 % (4047026)------------------------------
% 101.51/28.87 % (4047026)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 101.51/28.87 % (4047026)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.51/28.87 % (4047026)CaDiCaL version: 2.1.3
% 101.51/28.87 % (4047026)Termination reason: Instruction limit
% 101.51/28.87 % (4047026)Termination phase: Saturation
% 101.51/28.87 % (4047026)Time elapsed: 1.188 s
% 101.51/28.87 % (4047026)Peak memory usage: 162 MB
% 101.51/28.87 % (4047026)Instructions burned: 2034 (million)
% 101.51/28.87 % (4047027)Instruction limit reached!
% 101.51/28.87 % (4047027)------------------------------
% 101.51/28.87 % (4047027)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 101.51/28.87 % (4047027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.51/28.87 % (4047027)CaDiCaL version: 2.1.3
% 101.51/28.87 % (4047027)Termination reason: Instruction limit
% 101.51/28.87 % (4047027)Termination phase: Saturation
% 101.51/28.87 % (4047027)Time elapsed: 1.277 s
% 101.51/28.87 % (4047027)Peak memory usage: 184 MB
% 101.51/28.87 % (4047027)Instructions burned: 2056 (million)
% 101.51/28.87 % (4047032)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=3890565824:i=4835:sd=13:ss=axioms:sgt=23_2753 on theBenchmark for (2753ds/4835Mi)
% 101.51/28.87 % (4047034)lrs+10_1_to=lpo:sil=32000:plsq=on:plsqc=1:bsd=on:plsqr=64,1:sp=reverse_frequency:bsr=unit_only:plsql=on:fd=off:slsqc=4:newcnf=on:slsq=on:random_seed=4043549017:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2751 on theBenchmark for (2751ds/797Mi)
% 101.51/28.87 % (4047034)Instruction limit reached!
% 101.51/28.87 % (4047034)------------------------------
% 101.51/28.87 % (4047034)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 101.51/28.87 % (4047034)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.51/28.87 % (4047034)CaDiCaL version: 2.1.3
% 101.51/28.87 % (4047034)Termination reason: Instruction limit
% 101.51/28.87 % (4047034)Termination phase: NewCNF
% 101.51/28.87 % (4047034)Time elapsed: 0.628 s
% 101.51/28.87 % (4047034)Peak memory usage: 138 MB
% 101.51/28.87 % (4047034)Instructions burned: 797 (million)
% 101.51/28.87 % (4047036)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=3810821540:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2744 on theBenchmark for (2744ds/2326Mi)
% 101.51/28.88 % (4047036)Instruction limit reached!
% 101.51/28.88 % (4047036)------------------------------
% 101.51/28.88 % (4047036)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 101.51/28.88 % (4047036)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.51/28.88 % (4047036)CaDiCaL version: 2.1.3
% 101.51/28.88 % (4047036)Termination reason: Instruction limit
% 101.51/28.88 % (4047036)Termination phase: Property scanning
% 101.51/28.88 % (4047036)Time elapsed: 1.215 s
% 101.51/28.88 % (4047036)Peak memory usage: 178 MB
% 101.51/28.88 % (4047036)Instructions burned: 2326 (million)
% 101.51/28.88 % (4047038)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=2449221085:i=6038:nm=6_2730 on theBenchmark for (2730ds/6038Mi)
% 101.51/28.88 % (4047030)First to succeed.
% 101.51/28.88 % (4047030)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-4046921"
% 101.51/28.88 % (4047032)Instruction limit reached!
% 101.51/28.88 % (4047032)------------------------------
% 101.51/28.88 % (4047032)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 101.51/28.88 % (4047032)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.51/28.88 % (4047032)CaDiCaL version: 2.1.3
% 101.51/28.88 % (4047032)Termination reason: Instruction limit
% 101.51/28.88 % (4047032)Termination phase: Saturation
% 101.51/28.88 % (4047032)Time elapsed: 2.910 s
% 101.51/28.88 % (4047032)Peak memory usage: 150 MB
% 101.51/28.88 % (4047032)Instructions burned: 4836 (million)
% 101.51/28.88 % (4047040)lrs+10_1_sil=32000:sp=occurrence:random_seed=426446531:st=2:i=33334:sd=3:ss=included:sgt=32_2722 on theBenchmark for (2722ds/33334Mi)
% 101.51/28.88 % (4047030)Refutation found. Thanks to Tanya!
% 101.51/28.88 % SZS status Theorem for theBenchmark
% 101.51/28.88 % SZS output start Proof for theBenchmark
% See solution above
% 192.55/29.07 % (4047030)------------------------------
% 192.55/29.07 % (4047030)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 192.55/29.07 % (4047030)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 192.55/29.07 % (4047030)CaDiCaL version: 2.1.3
% 192.55/29.07 % (4047030)Termination reason: Refutation
% 192.55/29.07 % (4047030)Time elapsed: 3.179 s
% 192.55/29.07 % (4047030)Peak memory usage: 198 MB
% 192.55/29.07 % (4047030)Instructions burned: 4982 (million)
% 192.55/29.07 % (4047030)------------------------------
% 192.55/29.07 % (4047030)------------------------------
% 192.55/29.07 % (4046921)Success in time 28.035 s
% 192.55/29.07 % Vampire exiting
%------------------------------------------------------------------------------