%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU434+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 : n018.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:49:02 PM UTC 2026
% Result : Theorem 114.21s 30.78s
% Output : Refutation 206.02s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 54
% Syntax : Number of formulae : 305 ( 63 unt; 32 def)
% Number of atoms : 1208 ( 95 equ)
% Maximal formula atoms : 15 ( 3 avg)
% Number of connectives : 1631 ( 728 ~; 739 |; 97 &)
% ( 46 <=>; 21 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 33 ( 31 usr; 25 prp; 0-3 aty)
% Number of functors : 31 ( 31 usr; 12 con; 0-5 aty)
% Number of variables : 493 ( 0 sgn 460 !; 33 ?)
% 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(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(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(f424,axiom,
! [X0] : k3_tarski(k1_zfmisc_1(X0)) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t99_zfmisc_1) ).
fof(f471,axiom,
! [X0] : ~ v1_xboole_0(k1_zfmisc_1(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_subset_1) ).
fof(f480,axiom,
! [X0,X1] :
( ( ~ v1_xboole_0(X0)
=> ( m1_subset_1(X1,X0)
<=> r2_hidden(X1,X0) ) )
& ( v1_xboole_0(X0)
=> ( m1_subset_1(X1,X0)
<=> v1_xboole_0(X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d2_subset_1) ).
fof(f654,axiom,
! [X0,X1,X2] :
( ( r1_tarski(k3_tarski(X0),X1)
& r2_hidden(X2,X0) )
=> r1_tarski(X2,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t56_setfam_1) ).
fof(f668,axiom,
! [X0,X1] :
( m1_subset_1(X1,k1_zfmisc_1(k1_zfmisc_1(X0)))
=> m1_subset_1(k5_setfam_1(X0,X1),k1_zfmisc_1(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k5_setfam_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(f866,axiom,
! [X0,X1] :
( v1_relat_1(X1)
=> ! [X2] :
( v1_relat_1(X2)
=> ( r1_tarski(X1,X2)
=> r1_tarski(k9_relat_1(X1,X0),k9_relat_1(X2,X0)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t157_relat_1) ).
fof(f1333,axiom,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
=> v1_relat_1(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc1_relset_1) ).
fof(f1334,axiom,
! [X0,X1,X2] :
( m1_relset_1(X2,X0,X1)
<=> r1_tarski(X2,k2_zfmisc_1(X0,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d1_relset_1) ).
fof(f1392,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
=> m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m2_relset_1) ).
fof(f1394,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
<=> m1_relset_1(X2,X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(f19052,axiom,
! [X0,X1,X2,X3,X4] :
( ( m1_subset_1(X3,k1_zfmisc_1(X1))
& m1_subset_1(X4,k1_zfmisc_1(k1_zfmisc_1(k2_zfmisc_1(X1,X2)))) )
=> ( r2_hidden(X0,a_4_3_relset_2(X1,X2,X3,X4))
<=> ? [X5] :
( m1_subset_1(X5,k1_zfmisc_1(k2_zfmisc_1(X1,X2)))
& X0 = k9_relat_1(X5,X3)
& r2_hidden(X5,X4) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fraenkel_a_4_3_relset_2) ).
fof(f19107,conjecture,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(X0))
=> ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(k1_zfmisc_1(k2_zfmisc_1(X0,X1))))
=> k9_relat_1(k5_setfam_1(k2_zfmisc_1(X0,X1),X3),X2) = k3_tarski(a_4_3_relset_2(X0,X1,X2,X3)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t35_relset_2) ).
fof(f19108,negated_conjecture,
~ ! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(X0))
=> ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(k1_zfmisc_1(k2_zfmisc_1(X0,X1))))
=> k9_relat_1(k5_setfam_1(k2_zfmisc_1(X0,X1),X3),X2) = k3_tarski(a_4_3_relset_2(X0,X1,X2,X3)) ) ),
inference(negated_conjecture,[status(cth)],[f19107]) ).
fof(f19141,plain,
? [X0,X1,X2] :
( ? [X3] :
( k9_relat_1(k5_setfam_1(k2_zfmisc_1(X0,X1),X3),X2) != k3_tarski(a_4_3_relset_2(X0,X1,X2,X3))
& m1_subset_1(X3,k1_zfmisc_1(k1_zfmisc_1(k2_zfmisc_1(X0,X1)))) )
& m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f19108]) ).
fof(f19151,plain,
! [X0,X1,X2] :
( r1_tarski(X2,X1)
| ~ r1_tarski(k3_tarski(X0),X1)
| ~ r2_hidden(X2,X0) ),
inference(ennf_transformation,[],[f654]) ).
fof(f19152,plain,
! [X0,X1,X2] :
( r1_tarski(X2,X1)
| ~ r1_tarski(k3_tarski(X0),X1)
| ~ r2_hidden(X2,X0) ),
inference(flattening,[],[f19151]) ).
fof(f19157,plain,
! [X0,X1] :
( r1_tarski(k3_tarski(X0),X1)
| ? [X2] :
( ~ r1_tarski(X2,X1)
& r2_hidden(X2,X0) ) ),
inference(ennf_transformation,[],[f419]) ).
fof(f19159,plain,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| ~ m2_relset_1(X2,X0,X1) ),
inference(ennf_transformation,[],[f1392]) ).
fof(f19160,plain,
! [X0,X1,X2] :
( v1_relat_1(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(ennf_transformation,[],[f1333]) ).
fof(f19196,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(f19197,plain,
! [X0,X1] :
( m1_subset_1(k5_setfam_1(X0,X1),k1_zfmisc_1(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(k1_zfmisc_1(X0))) ),
inference(ennf_transformation,[],[f668]) ).
fof(f19249,plain,
! [X0,X1] :
( ! [X2] :
( r1_tarski(k9_relat_1(X1,X0),k9_relat_1(X2,X0))
| ~ r1_tarski(X1,X2)
| ~ v1_relat_1(X2) )
| ~ v1_relat_1(X1) ),
inference(ennf_transformation,[],[f866]) ).
fof(f19250,plain,
! [X0,X1] :
( ! [X2] :
( r1_tarski(k9_relat_1(X1,X0),k9_relat_1(X2,X0))
| ~ r1_tarski(X1,X2)
| ~ v1_relat_1(X2) )
| ~ v1_relat_1(X1) ),
inference(flattening,[],[f19249]) ).
fof(f19265,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(f19266,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(f19267,plain,
! [X0,X1,X2,X3,X4] :
( ( r2_hidden(X0,a_4_3_relset_2(X1,X2,X3,X4))
<=> ? [X5] :
( m1_subset_1(X5,k1_zfmisc_1(k2_zfmisc_1(X1,X2)))
& X0 = k9_relat_1(X5,X3)
& r2_hidden(X5,X4) ) )
| ~ m1_subset_1(X3,k1_zfmisc_1(X1))
| ~ m1_subset_1(X4,k1_zfmisc_1(k1_zfmisc_1(k2_zfmisc_1(X1,X2)))) ),
inference(ennf_transformation,[],[f19052]) ).
fof(f19268,plain,
! [X0,X1,X2,X3,X4] :
( ( r2_hidden(X0,a_4_3_relset_2(X1,X2,X3,X4))
<=> ? [X5] :
( m1_subset_1(X5,k1_zfmisc_1(k2_zfmisc_1(X1,X2)))
& X0 = k9_relat_1(X5,X3)
& r2_hidden(X5,X4) ) )
| ~ m1_subset_1(X3,k1_zfmisc_1(X1))
| ~ m1_subset_1(X4,k1_zfmisc_1(k1_zfmisc_1(k2_zfmisc_1(X1,X2)))) ),
inference(flattening,[],[f19267]) ).
fof(f19290,plain,
! [X0,X1] :
( ( ( m1_subset_1(X1,X0)
<=> r2_hidden(X1,X0) )
| v1_xboole_0(X0) )
& ( ( m1_subset_1(X1,X0)
<=> v1_xboole_0(X1) )
| ~ v1_xboole_0(X0) ) ),
inference(ennf_transformation,[],[f480]) ).
fof(f19298,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(f19299,plain,
! [X0,X1,X2] :
( m1_subset_1(X0,X2)
| ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2)) ),
inference(flattening,[],[f19298]) ).
fof(f19395,plain,
! [X0,X1] :
( r1_tarski(X0,X1)
<=> ! [X2] :
( r2_hidden(X2,X1)
| ~ r2_hidden(X2,X0) ) ),
inference(ennf_transformation,[],[f8]) ).
fof(f20467,plain,
( k9_relat_1(k5_setfam_1(k2_zfmisc_1(sK31,sK32),sK34),sK33) != k3_tarski(a_4_3_relset_2(sK31,sK32,sK33,sK34))
& m1_subset_1(sK34,k1_zfmisc_1(k1_zfmisc_1(k2_zfmisc_1(sK31,sK32))))
& m1_subset_1(sK33,k1_zfmisc_1(sK31)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK31,sK32,sK33,sK34]),skolemize(X0,sK31),skolemize(X1,sK32),skolemize(X2,sK33),skolemize(X3,sK34)],[f19141]) ).
fof(f20477,plain,
! [X0,X1] :
( r1_tarski(k3_tarski(X0),X1)
| ( ~ r1_tarski(sK42(X0,X1),X1)
& r2_hidden(sK42(X0,X1),X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK42]),skolemize(X2,sK42(X0,X1))],[f19157]) ).
fof(f20478,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(f20479,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,[],[f20478]) ).
fof(f20480,plain,
! [X0,X1] :
( ( X1 = k3_tarski(X0)
| ( ( ! [X3] :
( ~ r2_hidden(sK43(X0,X1),X3)
| ~ r2_hidden(X3,X0) )
| ~ r2_hidden(sK43(X0,X1),X1) )
& ( ( r2_hidden(sK43(X0,X1),sK44(X0,X1))
& r2_hidden(sK44(X0,X1),X0) )
| r2_hidden(sK43(X0,X1),X1) ) ) )
& ( ! [X5] :
( ( r2_hidden(X5,X1)
| ! [X6] :
( ~ r2_hidden(X5,X6)
| ~ r2_hidden(X6,X0) ) )
& ( ( r2_hidden(X5,sK45(X0,X5))
& r2_hidden(sK45(X0,X5),X0) )
| ~ r2_hidden(X5,X1) ) )
| k3_tarski(X0) != X1 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK43,sK44,sK45]),skolemize(X2,sK43(X0,X1)),skolemize(X4,sK44(X0,X1)),skolemize(X7,sK45(X0,X5))],[f20479]) ).
fof(f20527,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,[],[f19265]) ).
fof(f20528,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,[],[f20527]) ).
fof(f20529,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(sK72(X0,X1,X2),k1_relat_1(X2))
& r2_hidden(k4_tarski(sK72(X0,X1,X2),X0),X2)
& r2_hidden(sK72(X0,X1,X2),X1) )
| ~ r2_hidden(X0,k9_relat_1(X2,X1)) ) )
| ~ v1_relat_1(X2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK72]),skolemize(X4,sK72(X0,X1,X2))],[f20528]) ).
fof(f20530,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,[],[f19266]) ).
fof(f20531,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,[],[f20530]) ).
fof(f20532,plain,
! [X0] :
( ! [X1,X2] :
( ( X2 = k9_relat_1(X0,X1)
| ( ( ! [X4] :
( ~ r2_hidden(k4_tarski(X4,sK73(X0,X1,X2)),X0)
| ~ r2_hidden(X4,X1) )
| ~ r2_hidden(sK73(X0,X1,X2),X2) )
& ( ( r2_hidden(k4_tarski(sK74(X0,X1,X2),sK73(X0,X1,X2)),X0)
& r2_hidden(sK74(X0,X1,X2),X1) )
| r2_hidden(sK73(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(sK75(X0,X1,X6),X6),X0)
& r2_hidden(sK75(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,[sK73,sK74,sK75]),skolemize(X3,sK73(X0,X1,X2)),skolemize(X5,sK74(X0,X1,X2)),skolemize(X8,sK75(X0,X1,X6))],[f20531]) ).
fof(f20533,plain,
! [X0,X1,X2,X3,X4] :
( ( ( r2_hidden(X0,a_4_3_relset_2(X1,X2,X3,X4))
| ! [X5] :
( ~ m1_subset_1(X5,k1_zfmisc_1(k2_zfmisc_1(X1,X2)))
| k9_relat_1(X5,X3) != X0
| ~ r2_hidden(X5,X4) ) )
& ( ? [X5] :
( m1_subset_1(X5,k1_zfmisc_1(k2_zfmisc_1(X1,X2)))
& X0 = k9_relat_1(X5,X3)
& r2_hidden(X5,X4) )
| ~ r2_hidden(X0,a_4_3_relset_2(X1,X2,X3,X4)) ) )
| ~ m1_subset_1(X3,k1_zfmisc_1(X1))
| ~ m1_subset_1(X4,k1_zfmisc_1(k1_zfmisc_1(k2_zfmisc_1(X1,X2)))) ),
inference(nnf_transformation,[],[f19268]) ).
fof(f20534,plain,
! [X0,X1,X2,X3,X4] :
( ( ( r2_hidden(X0,a_4_3_relset_2(X1,X2,X3,X4))
| ! [X5] :
( ~ m1_subset_1(X5,k1_zfmisc_1(k2_zfmisc_1(X1,X2)))
| k9_relat_1(X5,X3) != X0
| ~ r2_hidden(X5,X4) ) )
& ( ? [X6] :
( m1_subset_1(X6,k1_zfmisc_1(k2_zfmisc_1(X1,X2)))
& k9_relat_1(X6,X3) = X0
& r2_hidden(X6,X4) )
| ~ r2_hidden(X0,a_4_3_relset_2(X1,X2,X3,X4)) ) )
| ~ m1_subset_1(X3,k1_zfmisc_1(X1))
| ~ m1_subset_1(X4,k1_zfmisc_1(k1_zfmisc_1(k2_zfmisc_1(X1,X2)))) ),
inference(rectify,[],[f20533]) ).
fof(f20535,plain,
! [X0,X1,X2,X3,X4] :
( ( ( r2_hidden(X0,a_4_3_relset_2(X1,X2,X3,X4))
| ! [X5] :
( ~ m1_subset_1(X5,k1_zfmisc_1(k2_zfmisc_1(X1,X2)))
| k9_relat_1(X5,X3) != X0
| ~ r2_hidden(X5,X4) ) )
& ( ( m1_subset_1(sK76(X0,X1,X2,X3,X4),k1_zfmisc_1(k2_zfmisc_1(X1,X2)))
& k9_relat_1(sK76(X0,X1,X2,X3,X4),X3) = X0
& r2_hidden(sK76(X0,X1,X2,X3,X4),X4) )
| ~ r2_hidden(X0,a_4_3_relset_2(X1,X2,X3,X4)) ) )
| ~ m1_subset_1(X3,k1_zfmisc_1(X1))
| ~ m1_subset_1(X4,k1_zfmisc_1(k1_zfmisc_1(k2_zfmisc_1(X1,X2)))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK76]),skolemize(X6,sK76(X0,X1,X2,X3,X4))],[f20534]) ).
fof(f20540,plain,
! [X0,X1] :
( ( ( ( m1_subset_1(X1,X0)
| ~ r2_hidden(X1,X0) )
& ( r2_hidden(X1,X0)
| ~ m1_subset_1(X1,X0) ) )
| v1_xboole_0(X0) )
& ( ( ( m1_subset_1(X1,X0)
| ~ v1_xboole_0(X1) )
& ( v1_xboole_0(X1)
| ~ m1_subset_1(X1,X0) ) )
| ~ v1_xboole_0(X0) ) ),
inference(nnf_transformation,[],[f19290]) ).
fof(f20579,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(f20580,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,[],[f20579]) ).
fof(f20581,plain,
! [X0,X1] :
( ( X1 = k1_zfmisc_1(X0)
| ( ( ~ r1_tarski(sK109(X0,X1),X0)
| ~ r2_hidden(sK109(X0,X1),X1) )
& ( r1_tarski(sK109(X0,X1),X0)
| r2_hidden(sK109(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,[sK109]),skolemize(X2,sK109(X0,X1))],[f20580]) ).
fof(f20582,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(f20583,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,[],[f20582]) ).
fof(f20584,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,[],[f19395]) ).
fof(f20585,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,[],[f20584]) ).
fof(f20586,plain,
! [X0,X1] :
( ( r1_tarski(X0,X1)
| ( ~ r2_hidden(sK110(X0,X1),X1)
& r2_hidden(sK110(X0,X1),X0) ) )
& ( ! [X3] :
( r2_hidden(X3,X1)
| ~ r2_hidden(X3,X0) )
| ~ r1_tarski(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK110]),skolemize(X2,sK110(X0,X1))],[f20585]) ).
fof(f20785,plain,
! [X0,X1,X2] :
( ( m2_relset_1(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1) )
& ( m1_relset_1(X2,X0,X1)
| ~ m2_relset_1(X2,X0,X1) ) ),
inference(nnf_transformation,[],[f1394]) ).
fof(f20787,plain,
! [X0,X1,X2] :
( ( m1_relset_1(X2,X0,X1)
| ~ r1_tarski(X2,k2_zfmisc_1(X0,X1)) )
& ( r1_tarski(X2,k2_zfmisc_1(X0,X1))
| ~ m1_relset_1(X2,X0,X1) ) ),
inference(nnf_transformation,[],[f1334]) ).
fof(f21002,plain,
m1_subset_1(sK33,k1_zfmisc_1(sK31)),
inference(cnf_transformation,[],[f20467]) ).
fof(f21003,plain,
m1_subset_1(sK34,k1_zfmisc_1(k1_zfmisc_1(k2_zfmisc_1(sK31,sK32)))),
inference(cnf_transformation,[],[f20467]) ).
fof(f21004,plain,
k9_relat_1(k5_setfam_1(k2_zfmisc_1(sK31,sK32),sK34),sK33) != k3_tarski(a_4_3_relset_2(sK31,sK32,sK33,sK34)),
inference(cnf_transformation,[],[f20467]) ).
fof(f21019,plain,
! [X2,X0,X1] :
( ~ r1_tarski(k3_tarski(X0),X1)
| r1_tarski(X2,X1)
| ~ r2_hidden(X2,X0) ),
inference(cnf_transformation,[],[f19152]) ).
fof(f21025,plain,
! [X0] : k3_tarski(k1_zfmisc_1(X0)) = X0,
inference(cnf_transformation,[],[f424]) ).
fof(f21031,plain,
! [X0,X1] :
( r2_hidden(sK42(X0,X1),X0)
| r1_tarski(k3_tarski(X0),X1) ),
inference(cnf_transformation,[],[f20477]) ).
fof(f21032,plain,
! [X0,X1] :
( ~ r1_tarski(sK42(X0,X1),X1)
| r1_tarski(k3_tarski(X0),X1) ),
inference(cnf_transformation,[],[f20477]) ).
fof(f21036,plain,
! [X0,X1,X5] :
( r2_hidden(sK45(X0,X5),X0)
| ~ r2_hidden(X5,X1)
| k3_tarski(X0) != X1 ),
inference(cnf_transformation,[],[f20480]) ).
fof(f21037,plain,
! [X0,X1,X5] :
( r2_hidden(X5,sK45(X0,X5))
| ~ r2_hidden(X5,X1)
| k3_tarski(X0) != X1 ),
inference(cnf_transformation,[],[f20480]) ).
fof(f21038,plain,
! [X0,X1,X6,X5] :
( r2_hidden(X5,X1)
| ~ r2_hidden(X5,X6)
| ~ r2_hidden(X6,X0)
| k3_tarski(X0) != X1 ),
inference(cnf_transformation,[],[f20480]) ).
fof(f21044,plain,
! [X2,X0,X1] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| ~ m2_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f19159]) ).
fof(f21045,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| v1_relat_1(X2) ),
inference(cnf_transformation,[],[f19160]) ).
fof(f21136,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,[],[f19196]) ).
fof(f21137,plain,
! [X0,X1] :
( m1_subset_1(k5_setfam_1(X0,X1),k1_zfmisc_1(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(k1_zfmisc_1(X0))) ),
inference(cnf_transformation,[],[f19197]) ).
fof(f21177,plain,
! [X2,X0,X1] :
( r1_tarski(k9_relat_1(X1,X0),k9_relat_1(X2,X0))
| ~ r1_tarski(X1,X2)
| ~ v1_relat_1(X2)
| ~ v1_relat_1(X1) ),
inference(cnf_transformation,[],[f19250]) ).
fof(f21192,plain,
! [X2,X0,X1] :
( r2_hidden(sK72(X0,X1,X2),X1)
| ~ r2_hidden(X0,k9_relat_1(X2,X1))
| ~ v1_relat_1(X2) ),
inference(cnf_transformation,[],[f20529]) ).
fof(f21193,plain,
! [X2,X0,X1] :
( r2_hidden(k4_tarski(sK72(X0,X1,X2),X0),X2)
| ~ r2_hidden(X0,k9_relat_1(X2,X1))
| ~ v1_relat_1(X2) ),
inference(cnf_transformation,[],[f20529]) ).
fof(f21198,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,[],[f20532]) ).
fof(f21202,plain,
! [X2,X3,X0,X1,X4] :
( r2_hidden(sK76(X0,X1,X2,X3,X4),X4)
| ~ r2_hidden(X0,a_4_3_relset_2(X1,X2,X3,X4))
| ~ m1_subset_1(X3,k1_zfmisc_1(X1))
| ~ m1_subset_1(X4,k1_zfmisc_1(k1_zfmisc_1(k2_zfmisc_1(X1,X2)))) ),
inference(cnf_transformation,[],[f20535]) ).
fof(f21203,plain,
! [X2,X3,X0,X1,X4] :
( k9_relat_1(sK76(X0,X1,X2,X3,X4),X3) = X0
| ~ r2_hidden(X0,a_4_3_relset_2(X1,X2,X3,X4))
| ~ m1_subset_1(X3,k1_zfmisc_1(X1))
| ~ m1_subset_1(X4,k1_zfmisc_1(k1_zfmisc_1(k2_zfmisc_1(X1,X2)))) ),
inference(cnf_transformation,[],[f20535]) ).
fof(f21204,plain,
! [X2,X3,X0,X1,X4] :
( m1_subset_1(sK76(X0,X1,X2,X3,X4),k1_zfmisc_1(k2_zfmisc_1(X1,X2)))
| ~ r2_hidden(X0,a_4_3_relset_2(X1,X2,X3,X4))
| ~ m1_subset_1(X3,k1_zfmisc_1(X1))
| ~ m1_subset_1(X4,k1_zfmisc_1(k1_zfmisc_1(k2_zfmisc_1(X1,X2)))) ),
inference(cnf_transformation,[],[f20535]) ).
fof(f21205,plain,
! [X2,X3,X0,X1,X4,X5] :
( r2_hidden(X0,a_4_3_relset_2(X1,X2,X3,X4))
| ~ m1_subset_1(X5,k1_zfmisc_1(k2_zfmisc_1(X1,X2)))
| k9_relat_1(X5,X3) != X0
| ~ r2_hidden(X5,X4)
| ~ m1_subset_1(X3,k1_zfmisc_1(X1))
| ~ m1_subset_1(X4,k1_zfmisc_1(k1_zfmisc_1(k2_zfmisc_1(X1,X2)))) ),
inference(cnf_transformation,[],[f20535]) ).
fof(f21227,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,X0)
| r2_hidden(X1,X0)
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f20540]) ).
fof(f21233,plain,
! [X0] : ~ v1_xboole_0(k1_zfmisc_1(X0)),
inference(cnf_transformation,[],[f471]) ).
fof(f21242,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ r2_hidden(X0,X1)
| m1_subset_1(X0,X2) ),
inference(cnf_transformation,[],[f19299]) ).
fof(f21369,plain,
! [X3,X0,X1] :
( r1_tarski(X3,X0)
| ~ r2_hidden(X3,X1)
| k1_zfmisc_1(X0) != X1 ),
inference(cnf_transformation,[],[f20581]) ).
fof(f21376,plain,
! [X0,X1] :
( ~ r1_tarski(X1,X0)
| ~ r1_tarski(X0,X1)
| X0 = X1 ),
inference(cnf_transformation,[],[f20583]) ).
fof(f21379,plain,
! [X0,X1] :
( r2_hidden(sK110(X0,X1),X0)
| r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f20586]) ).
fof(f21380,plain,
! [X0,X1] :
( ~ r2_hidden(sK110(X0,X1),X1)
| r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f20586]) ).
fof(f22121,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,X0,X1)
| m2_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f20785]) ).
fof(f22123,plain,
! [X2,X0,X1] :
( r1_tarski(X2,k2_zfmisc_1(X0,X1))
| ~ m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f20787]) ).
fof(f22124,plain,
! [X2,X0,X1] :
( ~ r1_tarski(X2,k2_zfmisc_1(X0,X1))
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f20787]) ).
fof(f23047,plain,
! [X0,X6,X5] :
( r2_hidden(X5,k3_tarski(X0))
| ~ r2_hidden(X5,X6)
| ~ r2_hidden(X6,X0) ),
inference(equality_resolution,[],[f21038]) ).
fof(f23048,plain,
! [X0,X5] :
( r2_hidden(X5,sK45(X0,X5))
| ~ r2_hidden(X5,k3_tarski(X0)) ),
inference(equality_resolution,[],[f21037]) ).
fof(f23049,plain,
! [X0,X5] :
( r2_hidden(sK45(X0,X5),X0)
| ~ r2_hidden(X5,k3_tarski(X0)) ),
inference(equality_resolution,[],[f21036]) ).
fof(f23069,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,[],[f21198]) ).
fof(f23072,plain,
! [X2,X3,X1,X4,X5] :
( r2_hidden(k9_relat_1(X5,X3),a_4_3_relset_2(X1,X2,X3,X4))
| ~ m1_subset_1(X5,k1_zfmisc_1(k2_zfmisc_1(X1,X2)))
| ~ r2_hidden(X5,X4)
| ~ m1_subset_1(X3,k1_zfmisc_1(X1))
| ~ m1_subset_1(X4,k1_zfmisc_1(k1_zfmisc_1(k2_zfmisc_1(X1,X2)))) ),
inference(equality_resolution,[],[f21205]) ).
fof(f23079,plain,
! [X3,X0] :
( ~ r2_hidden(X3,k1_zfmisc_1(X0))
| r1_tarski(X3,X0) ),
inference(equality_resolution,[],[f21369]) ).
fof(f23215,definition,
sF387 = k2_zfmisc_1(sK31,sK32),
introduced(definition,[new_symbols(definition,[sF387])],[function_definition]) ).
fof(f23216,plain,
k2_zfmisc_1(sK31,sK32) = sF387,
inference(reorient_equations,[],[f23215]) ).
fof(f23217,definition,
sF388 = k5_setfam_1(sF387,sK34),
introduced(definition,[new_symbols(definition,[sF388])],[function_definition]) ).
fof(f23218,plain,
k5_setfam_1(sF387,sK34) = sF388,
inference(reorient_equations,[],[f23217]) ).
fof(f23219,definition,
sF389 = k9_relat_1(sF388,sK33),
introduced(definition,[new_symbols(definition,[sF389])],[function_definition]) ).
fof(f23220,plain,
k9_relat_1(sF388,sK33) = sF389,
inference(reorient_equations,[],[f23219]) ).
fof(f23221,definition,
sF390 = a_4_3_relset_2(sK31,sK32,sK33,sK34),
introduced(definition,[new_symbols(definition,[sF390])],[function_definition]) ).
fof(f23222,plain,
a_4_3_relset_2(sK31,sK32,sK33,sK34) = sF390,
inference(reorient_equations,[],[f23221]) ).
fof(f23223,definition,
sF391 = k3_tarski(sF390),
introduced(definition,[new_symbols(definition,[sF391])],[function_definition]) ).
fof(f23224,plain,
k3_tarski(sF390) = sF391,
inference(reorient_equations,[],[f23223]) ).
fof(f23225,plain,
sF389 != sF391,
inference(definition_folding,[],[f21004,f23224,f23222,f23220,f23218,f23216]) ).
fof(f23226,definition,
sF392 = k1_zfmisc_1(sF387),
introduced(definition,[new_symbols(definition,[sF392])],[function_definition]) ).
fof(f23227,plain,
k1_zfmisc_1(sF387) = sF392,
inference(reorient_equations,[],[f23226]) ).
fof(f23228,definition,
sF393 = k1_zfmisc_1(sF392),
introduced(definition,[new_symbols(definition,[sF393])],[function_definition]) ).
fof(f23229,plain,
k1_zfmisc_1(sF392) = sF393,
inference(reorient_equations,[],[f23228]) ).
fof(f23230,plain,
m1_subset_1(sK34,sF393),
inference(definition_folding,[],[f21003,f23229,f23227,f23216]) ).
fof(f23231,definition,
sF394 = k1_zfmisc_1(sK31),
introduced(definition,[new_symbols(definition,[sF394])],[function_definition]) ).
fof(f23232,plain,
k1_zfmisc_1(sK31) = sF394,
inference(reorient_equations,[],[f23231]) ).
fof(f23233,plain,
m1_subset_1(sK33,sF394),
inference(definition_folding,[],[f21002,f23232]) ).
fof(f23823,definition,
( spl395_116
<=> m1_subset_1(sK33,sF394) ),
introduced(definition,[new_symbols(definition,[spl395_116])],[avatar_definition]) ).
fof(f23825,plain,
( m1_subset_1(sK33,sF394)
| ~ spl395_116 ),
inference(avatar_component_clause,[],[f23823]) ).
fof(f23826,plain,
spl395_116,
inference(avatar_split_clause,[],[f23233,f23823]) ).
fof(f23828,definition,
( spl395_117
<=> m1_subset_1(sK34,sF393) ),
introduced(definition,[new_symbols(definition,[spl395_117])],[avatar_definition]) ).
fof(f23831,plain,
spl395_117,
inference(avatar_split_clause,[],[f23230,f23828]) ).
fof(f23833,definition,
( spl395_118
<=> sF389 = sF391 ),
introduced(definition,[new_symbols(definition,[spl395_118])],[avatar_definition]) ).
fof(f23835,plain,
( sF389 != sF391
| spl395_118 ),
inference(avatar_component_clause,[],[f23833]) ).
fof(f23836,plain,
~ spl395_118,
inference(avatar_split_clause,[],[f23225,f23833]) ).
fof(f23838,definition,
( spl395_119
<=> k2_zfmisc_1(sK31,sK32) = sF387 ),
introduced(definition,[new_symbols(definition,[spl395_119])],[avatar_definition]) ).
fof(f23840,plain,
( k2_zfmisc_1(sK31,sK32) = sF387
| ~ spl395_119 ),
inference(avatar_component_clause,[],[f23838]) ).
fof(f23841,plain,
spl395_119,
inference(avatar_split_clause,[],[f23216,f23838]) ).
fof(f23843,definition,
( spl395_120
<=> k5_setfam_1(sF387,sK34) = sF388 ),
introduced(definition,[new_symbols(definition,[spl395_120])],[avatar_definition]) ).
fof(f23845,plain,
( k5_setfam_1(sF387,sK34) = sF388
| ~ spl395_120 ),
inference(avatar_component_clause,[],[f23843]) ).
fof(f23846,plain,
spl395_120,
inference(avatar_split_clause,[],[f23218,f23843]) ).
fof(f23848,definition,
( spl395_121
<=> k9_relat_1(sF388,sK33) = sF389 ),
introduced(definition,[new_symbols(definition,[spl395_121])],[avatar_definition]) ).
fof(f23850,plain,
( k9_relat_1(sF388,sK33) = sF389
| ~ spl395_121 ),
inference(avatar_component_clause,[],[f23848]) ).
fof(f23851,plain,
spl395_121,
inference(avatar_split_clause,[],[f23220,f23848]) ).
fof(f23853,definition,
( spl395_122
<=> a_4_3_relset_2(sK31,sK32,sK33,sK34) = sF390 ),
introduced(definition,[new_symbols(definition,[spl395_122])],[avatar_definition]) ).
fof(f23855,plain,
( a_4_3_relset_2(sK31,sK32,sK33,sK34) = sF390
| ~ spl395_122 ),
inference(avatar_component_clause,[],[f23853]) ).
fof(f23856,plain,
spl395_122,
inference(avatar_split_clause,[],[f23222,f23853]) ).
fof(f23858,definition,
( spl395_123
<=> k3_tarski(sF390) = sF391 ),
introduced(definition,[new_symbols(definition,[spl395_123])],[avatar_definition]) ).
fof(f23860,plain,
( k3_tarski(sF390) = sF391
| ~ spl395_123 ),
inference(avatar_component_clause,[],[f23858]) ).
fof(f23861,plain,
spl395_123,
inference(avatar_split_clause,[],[f23224,f23858]) ).
fof(f23863,definition,
( spl395_124
<=> k1_zfmisc_1(sF387) = sF392 ),
introduced(definition,[new_symbols(definition,[spl395_124])],[avatar_definition]) ).
fof(f23865,plain,
( k1_zfmisc_1(sF387) = sF392
| ~ spl395_124 ),
inference(avatar_component_clause,[],[f23863]) ).
fof(f23866,plain,
spl395_124,
inference(avatar_split_clause,[],[f23227,f23863]) ).
fof(f23868,definition,
( spl395_125
<=> k1_zfmisc_1(sF392) = sF393 ),
introduced(definition,[new_symbols(definition,[spl395_125])],[avatar_definition]) ).
fof(f23871,plain,
spl395_125,
inference(avatar_split_clause,[],[f23229,f23868]) ).
fof(f23873,definition,
( spl395_126
<=> k1_zfmisc_1(sK31) = sF394 ),
introduced(definition,[new_symbols(definition,[spl395_126])],[avatar_definition]) ).
fof(f23875,plain,
( k1_zfmisc_1(sK31) = sF394
| ~ spl395_126 ),
inference(avatar_component_clause,[],[f23873]) ).
fof(f23876,plain,
spl395_126,
inference(avatar_split_clause,[],[f23232,f23873]) ).
fof(f23877,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF387))
| v1_relat_1(X0) )
| ~ spl395_119 ),
inference(superposition,[],[f21045,f23840]) ).
fof(f23879,plain,
( ! [X0] :
( r2_hidden(k9_relat_1(X0,sK33),sF390)
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_zfmisc_1(sK31,sK32)))
| ~ r2_hidden(X0,sK34)
| ~ m1_subset_1(sK33,k1_zfmisc_1(sK31))
| ~ m1_subset_1(sK34,k1_zfmisc_1(k1_zfmisc_1(k2_zfmisc_1(sK31,sK32)))) )
| ~ spl395_122 ),
inference(superposition,[],[f23072,f23855]) ).
fof(f23880,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF387))
| r2_hidden(k9_relat_1(X0,sK33),sF390)
| ~ r2_hidden(X0,sK34)
| ~ m1_subset_1(sK33,k1_zfmisc_1(sK31))
| ~ m1_subset_1(sK34,k1_zfmisc_1(k1_zfmisc_1(k2_zfmisc_1(sK31,sK32)))) )
| ~ spl395_119
| ~ spl395_122 ),
inference(forward_demodulation,[],[f23879,f23840]) ).
fof(f23881,plain,
( ! [X0] :
( ~ m1_subset_1(sK33,sF394)
| ~ m1_subset_1(X0,k1_zfmisc_1(sF387))
| r2_hidden(k9_relat_1(X0,sK33),sF390)
| ~ r2_hidden(X0,sK34)
| ~ m1_subset_1(sK34,k1_zfmisc_1(k1_zfmisc_1(k2_zfmisc_1(sK31,sK32)))) )
| ~ spl395_119
| ~ spl395_122
| ~ spl395_126 ),
inference(forward_demodulation,[],[f23880,f23875]) ).
fof(f23882,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF387))
| r2_hidden(k9_relat_1(X0,sK33),sF390)
| ~ r2_hidden(X0,sK34)
| ~ m1_subset_1(sK34,k1_zfmisc_1(k1_zfmisc_1(k2_zfmisc_1(sK31,sK32)))) )
| ~ spl395_116
| ~ spl395_119
| ~ spl395_122
| ~ spl395_126 ),
inference(forward_subsumption_resolution,[],[f23881,f23825]) ).
fof(f23883,plain,
( ! [X0] :
( ~ m1_subset_1(sK34,k1_zfmisc_1(k1_zfmisc_1(sF387)))
| ~ m1_subset_1(X0,k1_zfmisc_1(sF387))
| r2_hidden(k9_relat_1(X0,sK33),sF390)
| ~ r2_hidden(X0,sK34) )
| ~ spl395_116
| ~ spl395_119
| ~ spl395_122
| ~ spl395_126 ),
inference(forward_demodulation,[],[f23882,f23840]) ).
fof(f23885,definition,
( spl395_127
<=> ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF387))
| ~ r2_hidden(X0,sK34)
| r2_hidden(k9_relat_1(X0,sK33),sF390) ) ),
introduced(definition,[new_symbols(definition,[spl395_127])],[avatar_definition]) ).
fof(f23886,plain,
( ! [X0] :
( r2_hidden(k9_relat_1(X0,sK33),sF390)
| ~ r2_hidden(X0,sK34)
| ~ m1_subset_1(X0,k1_zfmisc_1(sF387)) )
| ~ spl395_127 ),
inference(avatar_component_clause,[],[f23885]) ).
fof(f23888,definition,
( spl395_128
<=> m1_subset_1(sK34,k1_zfmisc_1(k1_zfmisc_1(sF387))) ),
introduced(definition,[new_symbols(definition,[spl395_128])],[avatar_definition]) ).
fof(f23889,plain,
( m1_subset_1(sK34,k1_zfmisc_1(k1_zfmisc_1(sF387)))
| ~ spl395_128 ),
inference(avatar_component_clause,[],[f23888]) ).
fof(f23891,plain,
( spl395_127
| ~ spl395_128
| ~ spl395_116
| ~ spl395_119
| ~ spl395_122
| ~ spl395_126 ),
inference(avatar_split_clause,[],[f23883,f23873,f23853,f23838,f23823,f23888,f23885]) ).
fof(f23892,plain,
( k1_zfmisc_1(sF387) != sF392
| k1_zfmisc_1(sF392) != sF393
| m1_subset_1(sK34,k1_zfmisc_1(k1_zfmisc_1(sF387)))
| ~ m1_subset_1(sK34,sF393) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f23922,plain,
( sF388 = k3_tarski(sK34)
| ~ m1_subset_1(sK34,k1_zfmisc_1(k1_zfmisc_1(sF387)))
| ~ spl395_120 ),
inference(superposition,[],[f23845,f21136]) ).
fof(f23923,plain,
( sF388 = k3_tarski(sK34)
| ~ spl395_120
| ~ spl395_128 ),
inference(forward_subsumption_resolution,[],[f23922,f23889]) ).
fof(f23926,definition,
( spl395_134
<=> sF388 = k3_tarski(sK34) ),
introduced(definition,[new_symbols(definition,[spl395_134])],[avatar_definition]) ).
fof(f23928,plain,
( sF388 = k3_tarski(sK34)
| ~ spl395_134 ),
inference(avatar_component_clause,[],[f23926]) ).
fof(f23929,plain,
( spl395_134
| ~ spl395_120
| ~ spl395_128 ),
inference(avatar_split_clause,[],[f23923,f23888,f23843,f23926]) ).
fof(f23936,definition,
( spl395_135
<=> m1_subset_1(sF388,sF392) ),
introduced(definition,[new_symbols(definition,[spl395_135])],[avatar_definition]) ).
fof(f23937,plain,
( m1_subset_1(sF388,sF392)
| ~ spl395_135 ),
inference(avatar_component_clause,[],[f23936]) ).
fof(f23942,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF392)
| v1_relat_1(X0) )
| ~ spl395_119
| ~ spl395_124 ),
inference(forward_demodulation,[],[f23877,f23865]) ).
fof(f23947,plain,
( ! [X0] :
( ~ r2_hidden(X0,sK34)
| m1_subset_1(X0,k1_zfmisc_1(sF387)) )
| ~ spl395_128 ),
inference(resolution,[],[f21242,f23889]) ).
fof(f23952,plain,
( ! [X0] :
( ~ r2_hidden(X0,sK34)
| m1_subset_1(X0,sF392) )
| ~ spl395_124
| ~ spl395_128 ),
inference(forward_demodulation,[],[f23947,f23865]) ).
fof(f23978,definition,
( spl395_139
<=> v1_relat_1(sF388) ),
introduced(definition,[new_symbols(definition,[spl395_139])],[avatar_definition]) ).
fof(f23979,plain,
( v1_relat_1(sF388)
| ~ spl395_139 ),
inference(avatar_component_clause,[],[f23978]) ).
fof(f24012,plain,
( m1_subset_1(sF388,k1_zfmisc_1(sF387))
| ~ m1_subset_1(sK34,k1_zfmisc_1(k1_zfmisc_1(sF387)))
| ~ spl395_120 ),
inference(superposition,[],[f21137,f23845]) ).
fof(f24019,plain,
( m1_subset_1(sF388,k1_zfmisc_1(sF387))
| ~ spl395_120
| ~ spl395_128 ),
inference(forward_subsumption_resolution,[],[f24012,f23889]) ).
fof(f24020,plain,
( m1_subset_1(sF388,sF392)
| ~ spl395_120
| ~ spl395_124
| ~ spl395_128 ),
inference(forward_demodulation,[],[f24019,f23865]) ).
fof(f24025,plain,
( spl395_135
| ~ spl395_120
| ~ spl395_124
| ~ spl395_128 ),
inference(avatar_split_clause,[],[f24020,f23888,f23863,f23843,f23936]) ).
fof(f24028,plain,
( v1_relat_1(sF388)
| ~ spl395_119
| ~ spl395_124
| ~ spl395_135 ),
inference(resolution,[],[f23937,f23942]) ).
fof(f24029,plain,
( spl395_139
| ~ spl395_119
| ~ spl395_124
| ~ spl395_135 ),
inference(avatar_split_clause,[],[f24028,f23936,f23863,f23838,f23978]) ).
fof(f24041,plain,
! [X2,X3,X0,X1,X4] :
( r2_hidden(X1,k9_relat_1(k3_tarski(X3),X4))
| ~ r2_hidden(X2,X3)
| ~ r2_hidden(k4_tarski(X0,X1),X2)
| ~ r2_hidden(X0,X4)
| ~ v1_relat_1(k3_tarski(X3)) ),
inference(resolution,[],[f23047,f23069]) ).
fof(f24043,plain,
( ! [X0,X1] :
( ~ r2_hidden(X1,sF390)
| ~ r2_hidden(X0,X1)
| r2_hidden(X0,sF391) )
| ~ spl395_123 ),
inference(superposition,[],[f23047,f23860]) ).
fof(f24044,plain,
( ! [X0,X1] :
( ~ r2_hidden(X1,sK34)
| ~ r2_hidden(X0,X1)
| r2_hidden(X0,sF388) )
| ~ spl395_134 ),
inference(superposition,[],[f23047,f23928]) ).
fof(f24051,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ r2_hidden(X0,sK76(X1,X2,X3,X4,sK34))
| r2_hidden(X0,sF388)
| ~ r2_hidden(X1,a_4_3_relset_2(X2,X3,X4,sK34))
| ~ m1_subset_1(X4,k1_zfmisc_1(X2))
| ~ m1_subset_1(sK34,k1_zfmisc_1(k1_zfmisc_1(k2_zfmisc_1(X2,X3)))) )
| ~ spl395_134 ),
inference(resolution,[],[f24044,f21202]) ).
fof(f24064,plain,
( ! [X0,X1] :
( ~ r2_hidden(X0,k9_relat_1(X1,sK33))
| r2_hidden(X0,sF391)
| ~ r2_hidden(X1,sK34)
| ~ m1_subset_1(X1,k1_zfmisc_1(sF387)) )
| ~ spl395_123
| ~ spl395_127 ),
inference(resolution,[],[f24043,f23886]) ).
fof(f24071,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X1,sF392)
| ~ r2_hidden(X0,k9_relat_1(X1,sK33))
| r2_hidden(X0,sF391)
| ~ r2_hidden(X1,sK34) )
| ~ spl395_123
| ~ spl395_124
| ~ spl395_127 ),
inference(forward_demodulation,[],[f24064,f23865]) ).
fof(f24084,plain,
( ! [X0,X1] :
( ~ r2_hidden(X0,k9_relat_1(X1,sK33))
| r2_hidden(X0,sF391)
| ~ r2_hidden(X1,sK34) )
| ~ spl395_123
| ~ spl395_124
| ~ spl395_127
| ~ spl395_128 ),
inference(forward_subsumption_resolution,[],[f24071,f23952]) ).
fof(f24095,definition,
( spl395_150
<=> ! [X0] :
( ~ r2_hidden(X0,sF389)
| r2_hidden(X0,sF391) ) ),
introduced(definition,[new_symbols(definition,[spl395_150])],[avatar_definition]) ).
fof(f24096,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF389)
| r2_hidden(X0,sF391) )
| ~ spl395_150 ),
inference(avatar_component_clause,[],[f24095]) ).
fof(f24134,plain,
! [X2,X3,X0,X1,X4] :
( ~ m1_subset_1(X4,k1_zfmisc_1(k1_zfmisc_1(k2_zfmisc_1(X1,X2))))
| ~ m1_subset_1(X3,k1_zfmisc_1(X1))
| ~ r2_hidden(X0,a_4_3_relset_2(X1,X2,X3,X4))
| v1_relat_1(sK76(X0,X1,X2,X3,X4)) ),
inference(resolution,[],[f21204,f21045]) ).
fof(f24258,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF392)
| r1_tarski(X0,sF387) )
| ~ spl395_124 ),
inference(superposition,[],[f23079,f23865]) ).
fof(f24280,plain,
( ! [X2,X3,X0,X1,X4] :
( r2_hidden(sK110(sK76(X0,X1,X2,X3,sK34),X4),sF388)
| ~ r2_hidden(X0,a_4_3_relset_2(X1,X2,X3,sK34))
| ~ m1_subset_1(X3,k1_zfmisc_1(X1))
| ~ m1_subset_1(sK34,k1_zfmisc_1(k1_zfmisc_1(k2_zfmisc_1(X1,X2))))
| r1_tarski(sK76(X0,X1,X2,X3,sK34),X4) )
| ~ spl395_134 ),
inference(resolution,[],[f24051,f21379]) ).
fof(f24450,plain,
( ! [X0,X1] :
( ~ r1_tarski(sF388,X0)
| r1_tarski(X1,X0)
| ~ r2_hidden(X1,sK34) )
| ~ spl395_134 ),
inference(superposition,[],[f21019,f23928]) ).
fof(f24453,plain,
( ! [X2,X0,X1] :
( r1_tarski(X0,k2_zfmisc_1(X1,X2))
| ~ r2_hidden(X0,sK34)
| ~ m1_relset_1(sF388,X1,X2) )
| ~ spl395_134 ),
inference(resolution,[],[f24450,f22123]) ).
fof(f24507,plain,
( r2_hidden(sF388,sF392)
| v1_xboole_0(sF392)
| ~ spl395_135 ),
inference(resolution,[],[f21227,f23937]) ).
fof(f24509,definition,
( spl395_168
<=> v1_xboole_0(sF392) ),
introduced(definition,[new_symbols(definition,[spl395_168])],[avatar_definition]) ).
fof(f24513,definition,
( spl395_169
<=> r2_hidden(sF388,sF392) ),
introduced(definition,[new_symbols(definition,[spl395_169])],[avatar_definition]) ).
fof(f24515,plain,
( r2_hidden(sF388,sF392)
| ~ spl395_169 ),
inference(avatar_component_clause,[],[f24513]) ).
fof(f24516,plain,
( spl395_168
| spl395_169
| ~ spl395_135 ),
inference(avatar_split_clause,[],[f24507,f23936,f24513,f24509]) ).
fof(f24718,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X0,X1,X2)
| v1_relat_1(X0) ),
inference(resolution,[],[f21044,f21045]) ).
fof(f24776,plain,
! [X2,X3,X0,X1,X4,X5] :
( r1_tarski(X0,k9_relat_1(X5,X3))
| ~ r1_tarski(sK76(X0,X1,X2,X3,X4),X5)
| ~ v1_relat_1(X5)
| ~ v1_relat_1(sK76(X0,X1,X2,X3,X4))
| ~ r2_hidden(X0,a_4_3_relset_2(X1,X2,X3,X4))
| ~ m1_subset_1(X3,k1_zfmisc_1(X1))
| ~ m1_subset_1(X4,k1_zfmisc_1(k1_zfmisc_1(k2_zfmisc_1(X1,X2)))) ),
inference(superposition,[],[f21177,f21203]) ).
fof(f24783,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ r1_tarski(sK76(X0,X1,X2,X3,X4),X5)
| r1_tarski(X0,k9_relat_1(X5,X3))
| ~ v1_relat_1(X5)
| ~ r2_hidden(X0,a_4_3_relset_2(X1,X2,X3,X4))
| ~ m1_subset_1(X3,k1_zfmisc_1(X1))
| ~ m1_subset_1(X4,k1_zfmisc_1(k1_zfmisc_1(k2_zfmisc_1(X1,X2)))) ),
inference(forward_subsumption_resolution,[],[f24776,f24134]) ).
fof(f24877,definition,
( spl395_196
<=> r1_tarski(sF389,sF391) ),
introduced(definition,[new_symbols(definition,[spl395_196])],[avatar_definition]) ).
fof(f24879,plain,
( r1_tarski(sF389,sF391)
| ~ spl395_196 ),
inference(avatar_component_clause,[],[f24877]) ).
fof(f26373,definition,
( spl395_290
<=> ! [X0] :
( r2_hidden(sK110(sF389,X0),sF391)
| r1_tarski(sF389,X0) ) ),
introduced(definition,[new_symbols(definition,[spl395_290])],[avatar_definition]) ).
fof(f26374,plain,
( ! [X0] :
( r2_hidden(sK110(sF389,X0),sF391)
| r1_tarski(sF389,X0) )
| ~ spl395_290 ),
inference(avatar_component_clause,[],[f26373]) ).
fof(f26379,definition,
( spl395_291
<=> r1_tarski(sF391,sF389) ),
introduced(definition,[new_symbols(definition,[spl395_291])],[avatar_definition]) ).
fof(f27120,plain,
( ! [X2,X3,X0,X1] :
( ~ r2_hidden(X0,X1)
| ~ r2_hidden(k4_tarski(X2,X3),X0)
| ~ r2_hidden(X2,sK33)
| ~ v1_relat_1(k3_tarski(X1))
| r2_hidden(X3,sF391)
| ~ r2_hidden(k3_tarski(X1),sK34) )
| ~ spl395_123
| ~ spl395_124
| ~ spl395_127
| ~ spl395_128 ),
inference(resolution,[],[f24041,f24084]) ).
fof(f27403,plain,
( ! [X2,X0,X1] :
( ~ m1_relset_1(sF388,X1,X2)
| ~ r2_hidden(X0,sK34)
| m1_relset_1(X0,X1,X2) )
| ~ spl395_134 ),
inference(resolution,[],[f22124,f24453]) ).
fof(f27410,plain,
( ! [X0] :
( m1_relset_1(X0,sK31,sK32)
| ~ r1_tarski(X0,sF387) )
| ~ spl395_119 ),
inference(superposition,[],[f22124,f23840]) ).
fof(f27610,plain,
( ! [X0] :
( ~ r2_hidden(X0,sK34)
| m1_relset_1(X0,sK31,sK32)
| ~ r1_tarski(sF388,sF387) )
| ~ spl395_119
| ~ spl395_134 ),
inference(resolution,[],[f27403,f27410]) ).
fof(f27612,definition,
( spl395_358
<=> r1_tarski(sF388,sF387) ),
introduced(definition,[new_symbols(definition,[spl395_358])],[avatar_definition]) ).
fof(f27616,definition,
( spl395_359
<=> ! [X0] :
( ~ r2_hidden(X0,sK34)
| m1_relset_1(X0,sK31,sK32) ) ),
introduced(definition,[new_symbols(definition,[spl395_359])],[avatar_definition]) ).
fof(f27617,plain,
( ! [X0] :
( m1_relset_1(X0,sK31,sK32)
| ~ r2_hidden(X0,sK34) )
| ~ spl395_359 ),
inference(avatar_component_clause,[],[f27616]) ).
fof(f27618,plain,
( ~ spl395_358
| spl395_359
| ~ spl395_119
| ~ spl395_134 ),
inference(avatar_split_clause,[],[f27610,f23926,f23838,f27616,f27612]) ).
fof(f29651,plain,
( ~ v1_xboole_0(sF392)
| ~ spl395_124 ),
inference(superposition,[],[f21233,f23865]) ).
fof(f29689,plain,
( r1_tarski(sF388,sF387)
| ~ spl395_124
| ~ spl395_169 ),
inference(resolution,[],[f24258,f24515]) ).
fof(f29690,plain,
( spl395_358
| ~ spl395_124
| ~ spl395_169 ),
inference(avatar_split_clause,[],[f29689,f24513,f23863,f27612]) ).
fof(f29771,plain,
( ! [X0] :
( m2_relset_1(X0,sK31,sK32)
| ~ r2_hidden(X0,sK34) )
| ~ spl395_359 ),
inference(resolution,[],[f27617,f22121]) ).
fof(f29774,plain,
( ! [X0] :
( ~ r2_hidden(X0,sK34)
| v1_relat_1(X0) )
| ~ spl395_359 ),
inference(resolution,[],[f29771,f24718]) ).
fof(f31198,plain,
( ~ r1_tarski(sF391,sF389)
| sF389 = sF391
| ~ spl395_196 ),
inference(resolution,[],[f24879,f21376]) ).
fof(f31201,plain,
( ~ r1_tarski(sF391,sF389)
| spl395_118
| ~ spl395_196 ),
inference(forward_subsumption_resolution,[],[f31198,f23835]) ).
fof(f31203,plain,
( ~ spl395_291
| spl395_118
| ~ spl395_196 ),
inference(avatar_split_clause,[],[f31201,f24877,f23833,f26379]) ).
fof(f31219,plain,
( ! [X0] :
( r2_hidden(sK110(sF389,X0),sF391)
| r1_tarski(sF389,X0) )
| ~ spl395_150 ),
inference(resolution,[],[f24096,f21379]) ).
fof(f31227,plain,
( spl395_290
| ~ spl395_150 ),
inference(avatar_split_clause,[],[f31219,f24095,f26373]) ).
fof(f31233,plain,
( r1_tarski(sF389,sF391)
| r1_tarski(sF389,sF391)
| ~ spl395_290 ),
inference(resolution,[],[f26374,f21380]) ).
fof(f31240,plain,
( r1_tarski(sF389,sF391)
| ~ spl395_290 ),
inference(duplicate_literal_removal,[],[f31233]) ).
fof(f31561,plain,
( ! [X2,X3,X0,X1] :
( ~ r2_hidden(X0,a_4_3_relset_2(X1,X2,X3,sK34))
| ~ m1_subset_1(X3,k1_zfmisc_1(X1))
| ~ m1_subset_1(sK34,k1_zfmisc_1(k1_zfmisc_1(k2_zfmisc_1(X1,X2))))
| r1_tarski(sK76(X0,X1,X2,X3,sK34),sF388)
| r1_tarski(sK76(X0,X1,X2,X3,sK34),sF388) )
| ~ spl395_134 ),
inference(resolution,[],[f24280,f21380]) ).
fof(f31573,plain,
( ! [X2,X3,X0,X1] :
( r1_tarski(sK76(X0,X1,X2,X3,sK34),sF388)
| ~ m1_subset_1(X3,k1_zfmisc_1(X1))
| ~ m1_subset_1(sK34,k1_zfmisc_1(k1_zfmisc_1(k2_zfmisc_1(X1,X2))))
| ~ r2_hidden(X0,a_4_3_relset_2(X1,X2,X3,sK34)) )
| ~ spl395_134 ),
inference(duplicate_literal_removal,[],[f31561]) ).
fof(f31582,plain,
( ! [X2,X3,X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(X1))
| ~ m1_subset_1(sK34,k1_zfmisc_1(k1_zfmisc_1(k2_zfmisc_1(X1,X2))))
| ~ r2_hidden(X3,a_4_3_relset_2(X1,X2,X0,sK34))
| r1_tarski(X3,k9_relat_1(sF388,X0))
| ~ v1_relat_1(sF388)
| ~ r2_hidden(X3,a_4_3_relset_2(X1,X2,X0,sK34))
| ~ m1_subset_1(X0,k1_zfmisc_1(X1))
| ~ m1_subset_1(sK34,k1_zfmisc_1(k1_zfmisc_1(k2_zfmisc_1(X1,X2)))) )
| ~ spl395_134 ),
inference(resolution,[],[f31573,f24783]) ).
fof(f31583,plain,
( ! [X2,X3,X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(X1))
| ~ m1_subset_1(sK34,k1_zfmisc_1(k1_zfmisc_1(k2_zfmisc_1(X1,X2))))
| ~ r2_hidden(X3,a_4_3_relset_2(X1,X2,X0,sK34))
| r1_tarski(X3,k9_relat_1(sF388,X0))
| ~ v1_relat_1(sF388) )
| ~ spl395_134 ),
inference(duplicate_literal_removal,[],[f31582]) ).
fof(f31584,plain,
( ! [X2,X3,X0,X1] :
( ~ m1_subset_1(sK34,k1_zfmisc_1(k1_zfmisc_1(k2_zfmisc_1(X1,X2))))
| ~ m1_subset_1(X0,k1_zfmisc_1(X1))
| ~ r2_hidden(X3,a_4_3_relset_2(X1,X2,X0,sK34))
| r1_tarski(X3,k9_relat_1(sF388,X0)) )
| ~ spl395_134
| ~ spl395_139 ),
inference(forward_subsumption_resolution,[],[f31583,f23979]) ).
fof(f31586,plain,
( ! [X0,X1] :
( ~ m1_subset_1(sK34,k1_zfmisc_1(k1_zfmisc_1(sF387)))
| ~ m1_subset_1(X0,k1_zfmisc_1(sK31))
| ~ r2_hidden(X1,a_4_3_relset_2(sK31,sK32,X0,sK34))
| r1_tarski(X1,k9_relat_1(sF388,X0)) )
| ~ spl395_119
| ~ spl395_134
| ~ spl395_139 ),
inference(superposition,[],[f31584,f23840]) ).
fof(f31592,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sK31))
| ~ r2_hidden(X1,a_4_3_relset_2(sK31,sK32,X0,sK34))
| r1_tarski(X1,k9_relat_1(sF388,X0)) )
| ~ spl395_119
| ~ spl395_128
| ~ spl395_134
| ~ spl395_139 ),
inference(forward_subsumption_resolution,[],[f31586,f23889]) ).
fof(f31593,plain,
( ! [X0,X1] :
( ~ r2_hidden(X1,a_4_3_relset_2(sK31,sK32,X0,sK34))
| ~ m1_subset_1(X0,sF394)
| r1_tarski(X1,k9_relat_1(sF388,X0)) )
| ~ spl395_119
| ~ spl395_126
| ~ spl395_128
| ~ spl395_134
| ~ spl395_139 ),
inference(forward_demodulation,[],[f31592,f23875]) ).
fof(f31619,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF390)
| ~ m1_subset_1(sK33,sF394)
| r1_tarski(X0,k9_relat_1(sF388,sK33)) )
| ~ spl395_119
| ~ spl395_122
| ~ spl395_126
| ~ spl395_128
| ~ spl395_134
| ~ spl395_139 ),
inference(superposition,[],[f31593,f23855]) ).
fof(f31620,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF390)
| r1_tarski(X0,k9_relat_1(sF388,sK33)) )
| ~ spl395_116
| ~ spl395_119
| ~ spl395_122
| ~ spl395_126
| ~ spl395_128
| ~ spl395_134
| ~ spl395_139 ),
inference(forward_subsumption_resolution,[],[f31619,f23825]) ).
fof(f31626,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF390)
| r1_tarski(X0,sF389) )
| ~ spl395_116
| ~ spl395_119
| ~ spl395_121
| ~ spl395_122
| ~ spl395_126
| ~ spl395_128
| ~ spl395_134
| ~ spl395_139 ),
inference(forward_demodulation,[],[f31620,f23850]) ).
fof(f31651,plain,
( ! [X0] :
( r1_tarski(sK42(sF390,X0),sF389)
| r1_tarski(k3_tarski(sF390),X0) )
| ~ spl395_116
| ~ spl395_119
| ~ spl395_121
| ~ spl395_122
| ~ spl395_126
| ~ spl395_128
| ~ spl395_134
| ~ spl395_139 ),
inference(resolution,[],[f31626,f21031]) ).
fof(f31671,plain,
( ! [X0] :
( r1_tarski(sK42(sF390,X0),sF389)
| r1_tarski(sF391,X0) )
| ~ spl395_116
| ~ spl395_119
| ~ spl395_121
| ~ spl395_122
| ~ spl395_123
| ~ spl395_126
| ~ spl395_128
| ~ spl395_134
| ~ spl395_139 ),
inference(forward_demodulation,[],[f31651,f23860]) ).
fof(f31785,plain,
( r1_tarski(sF391,sF389)
| r1_tarski(k3_tarski(sF390),sF389)
| ~ spl395_116
| ~ spl395_119
| ~ spl395_121
| ~ spl395_122
| ~ spl395_123
| ~ spl395_126
| ~ spl395_128
| ~ spl395_134
| ~ spl395_139 ),
inference(resolution,[],[f31671,f21032]) ).
fof(f31793,plain,
( r1_tarski(sF391,sF389)
| r1_tarski(sF391,sF389)
| ~ spl395_116
| ~ spl395_119
| ~ spl395_121
| ~ spl395_122
| ~ spl395_123
| ~ spl395_126
| ~ spl395_128
| ~ spl395_134
| ~ spl395_139 ),
inference(forward_demodulation,[],[f31785,f23860]) ).
fof(f31794,plain,
( r1_tarski(sF391,sF389)
| ~ spl395_116
| ~ spl395_119
| ~ spl395_121
| ~ spl395_122
| ~ spl395_123
| ~ spl395_126
| ~ spl395_128
| ~ spl395_134
| ~ spl395_139 ),
inference(duplicate_literal_removal,[],[f31793]) ).
fof(f31800,plain,
( spl395_196
| ~ spl395_290 ),
inference(avatar_split_clause,[],[f31240,f26373,f24877]) ).
fof(f31802,plain,
( spl395_291
| ~ spl395_116
| ~ spl395_119
| ~ spl395_121
| ~ spl395_122
| ~ spl395_123
| ~ spl395_126
| ~ spl395_128
| ~ spl395_134
| ~ spl395_139 ),
inference(avatar_split_clause,[],[f31794,f23978,f23926,f23888,f23873,f23858,f23853,f23848,f23838,f23823,f26379]) ).
fof(f34979,plain,
( ~ spl395_168
| ~ spl395_124 ),
inference(avatar_split_clause,[],[f29651,f23863,f24509]) ).
fof(f37723,plain,
( ! [X2,X3,X0,X1] :
( ~ r2_hidden(k4_tarski(X2,X3),X0)
| ~ r2_hidden(X0,X1)
| ~ r2_hidden(X2,sK33)
| r2_hidden(X3,sF391)
| ~ r2_hidden(k3_tarski(X1),sK34) )
| ~ spl395_123
| ~ spl395_124
| ~ spl395_127
| ~ spl395_128
| ~ spl395_359 ),
inference(forward_subsumption_resolution,[],[f27120,f29774]) ).
fof(f37751,plain,
( ! [X2,X3,X0,X1] :
( ~ r2_hidden(sK45(X0,k4_tarski(X1,X2)),X3)
| ~ r2_hidden(X1,sK33)
| r2_hidden(X2,sF391)
| ~ r2_hidden(k3_tarski(X3),sK34)
| ~ r2_hidden(k4_tarski(X1,X2),k3_tarski(X0)) )
| ~ spl395_123
| ~ spl395_124
| ~ spl395_127
| ~ spl395_128
| ~ spl395_359 ),
inference(resolution,[],[f37723,f23048]) ).
fof(f47761,plain,
( ! [X2,X0,X1] :
( ~ r2_hidden(X0,sK33)
| r2_hidden(X1,sF391)
| ~ r2_hidden(k3_tarski(X2),sK34)
| ~ r2_hidden(k4_tarski(X0,X1),k3_tarski(X2))
| ~ r2_hidden(k4_tarski(X0,X1),k3_tarski(X2)) )
| ~ spl395_123
| ~ spl395_124
| ~ spl395_127
| ~ spl395_128
| ~ spl395_359 ),
inference(resolution,[],[f37751,f23049]) ).
fof(f47810,plain,
( ! [X2,X0,X1] :
( ~ r2_hidden(k4_tarski(X0,X1),k3_tarski(X2))
| r2_hidden(X1,sF391)
| ~ r2_hidden(k3_tarski(X2),sK34)
| ~ r2_hidden(X0,sK33) )
| ~ spl395_123
| ~ spl395_124
| ~ spl395_127
| ~ spl395_128
| ~ spl395_359 ),
inference(duplicate_literal_removal,[],[f47761]) ).
fof(f47886,plain,
( ! [X2,X0,X1] :
( ~ r2_hidden(k4_tarski(X1,X2),X0)
| r2_hidden(X2,sF391)
| ~ r2_hidden(X0,sK34)
| ~ r2_hidden(X1,sK33) )
| ~ spl395_123
| ~ spl395_124
| ~ spl395_127
| ~ spl395_128
| ~ spl395_359 ),
inference(superposition,[],[f47810,f21025]) ).
fof(f47939,plain,
( ! [X2,X0,X1] :
( ~ r2_hidden(sK45(X1,k4_tarski(X2,X0)),sK34)
| r2_hidden(X0,sF391)
| ~ r2_hidden(X2,sK33)
| ~ r2_hidden(k4_tarski(X2,X0),k3_tarski(X1)) )
| ~ spl395_123
| ~ spl395_124
| ~ spl395_127
| ~ spl395_128
| ~ spl395_359 ),
inference(resolution,[],[f47886,f23048]) ).
fof(f48033,plain,
( ! [X0,X1] :
( r2_hidden(X0,sF391)
| ~ r2_hidden(X1,sK33)
| ~ r2_hidden(k4_tarski(X1,X0),k3_tarski(sK34))
| ~ r2_hidden(k4_tarski(X1,X0),k3_tarski(sK34)) )
| ~ spl395_123
| ~ spl395_124
| ~ spl395_127
| ~ spl395_128
| ~ spl395_359 ),
inference(resolution,[],[f47939,f23049]) ).
fof(f48036,plain,
( ! [X0,X1] :
( r2_hidden(X0,sF391)
| ~ r2_hidden(X1,sK33)
| ~ r2_hidden(k4_tarski(X1,X0),k3_tarski(sK34)) )
| ~ spl395_123
| ~ spl395_124
| ~ spl395_127
| ~ spl395_128
| ~ spl395_359 ),
inference(duplicate_literal_removal,[],[f48033]) ).
fof(f48037,plain,
( ! [X0,X1] :
( ~ r2_hidden(k4_tarski(X1,X0),sF388)
| r2_hidden(X0,sF391)
| ~ r2_hidden(X1,sK33) )
| ~ spl395_123
| ~ spl395_124
| ~ spl395_127
| ~ spl395_128
| ~ spl395_134
| ~ spl395_359 ),
inference(forward_demodulation,[],[f48036,f23928]) ).
fof(f48042,plain,
( ! [X0,X1] :
( r2_hidden(X0,sF391)
| ~ r2_hidden(sK72(X0,X1,sF388),sK33)
| ~ r2_hidden(X0,k9_relat_1(sF388,X1))
| ~ v1_relat_1(sF388) )
| ~ spl395_123
| ~ spl395_124
| ~ spl395_127
| ~ spl395_128
| ~ spl395_134
| ~ spl395_359 ),
inference(resolution,[],[f48037,f21193]) ).
fof(f48045,plain,
( ! [X0,X1] :
( ~ r2_hidden(sK72(X0,X1,sF388),sK33)
| r2_hidden(X0,sF391)
| ~ r2_hidden(X0,k9_relat_1(sF388,X1)) )
| ~ spl395_123
| ~ spl395_124
| ~ spl395_127
| ~ spl395_128
| ~ spl395_134
| ~ spl395_139
| ~ spl395_359 ),
inference(forward_subsumption_resolution,[],[f48042,f23979]) ).
fof(f48052,plain,
( ! [X0] :
( r2_hidden(X0,sF391)
| ~ r2_hidden(X0,k9_relat_1(sF388,sK33))
| ~ r2_hidden(X0,k9_relat_1(sF388,sK33))
| ~ v1_relat_1(sF388) )
| ~ spl395_123
| ~ spl395_124
| ~ spl395_127
| ~ spl395_128
| ~ spl395_134
| ~ spl395_139
| ~ spl395_359 ),
inference(resolution,[],[f48045,f21192]) ).
fof(f48053,plain,
( ! [X0] :
( r2_hidden(X0,sF391)
| ~ r2_hidden(X0,k9_relat_1(sF388,sK33))
| ~ v1_relat_1(sF388) )
| ~ spl395_123
| ~ spl395_124
| ~ spl395_127
| ~ spl395_128
| ~ spl395_134
| ~ spl395_139
| ~ spl395_359 ),
inference(duplicate_literal_removal,[],[f48052]) ).
fof(f48054,plain,
( ! [X0] :
( r2_hidden(X0,sF391)
| ~ r2_hidden(X0,k9_relat_1(sF388,sK33)) )
| ~ spl395_123
| ~ spl395_124
| ~ spl395_127
| ~ spl395_128
| ~ spl395_134
| ~ spl395_139
| ~ spl395_359 ),
inference(forward_subsumption_resolution,[],[f48053,f23979]) ).
fof(f48055,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF389)
| r2_hidden(X0,sF391) )
| ~ spl395_121
| ~ spl395_123
| ~ spl395_124
| ~ spl395_127
| ~ spl395_128
| ~ spl395_134
| ~ spl395_139
| ~ spl395_359 ),
inference(forward_demodulation,[],[f48054,f23850]) ).
fof(f48056,plain,
( spl395_150
| ~ spl395_121
| ~ spl395_123
| ~ spl395_124
| ~ spl395_127
| ~ spl395_128
| ~ spl395_134
| ~ spl395_139
| ~ spl395_359 ),
inference(avatar_split_clause,[],[f48055,f27616,f23978,f23926,f23888,f23885,f23863,f23858,f23848,f24095]) ).
cnf(s122,plain,
spl395_116,
inference(sat_conversion,[],[f23826]) ).
cnf(s123,plain,
spl395_117,
inference(sat_conversion,[],[f23831]) ).
cnf(s124,plain,
~ spl395_118,
inference(sat_conversion,[],[f23836]) ).
cnf(s125,plain,
spl395_119,
inference(sat_conversion,[],[f23841]) ).
cnf(s126,plain,
spl395_120,
inference(sat_conversion,[],[f23846]) ).
cnf(s127,plain,
spl395_121,
inference(sat_conversion,[],[f23851]) ).
cnf(s128,plain,
spl395_122,
inference(sat_conversion,[],[f23856]) ).
cnf(s129,plain,
spl395_123,
inference(sat_conversion,[],[f23861]) ).
cnf(s130,plain,
spl395_124,
inference(sat_conversion,[],[f23866]) ).
cnf(s131,plain,
spl395_125,
inference(sat_conversion,[],[f23871]) ).
cnf(s132,plain,
spl395_126,
inference(sat_conversion,[],[f23876]) ).
cnf(s133,plain,
( ~ spl395_116
| ~ spl395_119
| ~ spl395_122
| ~ spl395_126
| spl395_127
| ~ spl395_128 ),
inference(sat_conversion,[],[f23891]) ).
cnf(s134,plain,
( ~ spl395_117
| ~ spl395_124
| ~ spl395_125
| spl395_128 ),
inference(sat_conversion,[],[f23892]) ).
cnf(s138,plain,
( ~ spl395_120
| ~ spl395_128
| spl395_134 ),
inference(sat_conversion,[],[f23929]) ).
cnf(s149,plain,
( ~ spl395_120
| ~ spl395_124
| ~ spl395_128
| spl395_135 ),
inference(sat_conversion,[],[f24025]) ).
cnf(s151,plain,
( ~ spl395_119
| ~ spl395_124
| ~ spl395_135
| spl395_139 ),
inference(sat_conversion,[],[f24029]) ).
cnf(s169,plain,
( ~ spl395_135
| spl395_168
| spl395_169 ),
inference(sat_conversion,[],[f24516]) ).
cnf(s465,plain,
( ~ spl395_119
| ~ spl395_134
| ~ spl395_358
| spl395_359 ),
inference(sat_conversion,[],[f27618]) ).
cnf(s639,plain,
( ~ spl395_124
| ~ spl395_169
| spl395_358 ),
inference(sat_conversion,[],[f29690]) ).
cnf(s752,plain,
( spl395_118
| ~ spl395_196
| ~ spl395_291 ),
inference(sat_conversion,[],[f31203]) ).
cnf(s753,plain,
( ~ spl395_150
| spl395_290 ),
inference(sat_conversion,[],[f31227]) ).
cnf(s797,plain,
( spl395_196
| ~ spl395_290 ),
inference(sat_conversion,[],[f31800]) ).
cnf(s799,plain,
( ~ spl395_116
| ~ spl395_119
| ~ spl395_121
| ~ spl395_122
| ~ spl395_123
| ~ spl395_126
| ~ spl395_128
| ~ spl395_134
| ~ spl395_139
| spl395_291 ),
inference(sat_conversion,[],[f31802]) ).
cnf(s1135,plain,
( ~ spl395_124
| ~ spl395_168 ),
inference(sat_conversion,[],[f34979]) ).
cnf(s2422,plain,
( ~ spl395_121
| ~ spl395_123
| ~ spl395_124
| ~ spl395_127
| ~ spl395_128
| ~ spl395_134
| ~ spl395_139
| spl395_150
| ~ spl395_359 ),
inference(sat_conversion,[],[f48056]) ).
cnf(s2446,plain,
~ spl395_168,
inference(rat,[],[s1135,s130]) ).
cnf(s2480,plain,
spl395_128,
inference(rat,[],[s134,s130,s131,s123]) ).
cnf(s2490,plain,
spl395_134,
inference(rat,[],[s138,s126,s2480]) ).
cnf(s2492,plain,
spl395_135,
inference(rat,[],[s149,s126,s130,s2480]) ).
cnf(s2496,plain,
spl395_169,
inference(rat,[],[s169,s2446,s2492]) ).
cnf(s2497,plain,
spl395_139,
inference(rat,[],[s151,s125,s130,s2492]) ).
cnf(s2500,plain,
spl395_358,
inference(rat,[],[s639,s130,s2496]) ).
cnf(s2511,plain,
spl395_359,
inference(rat,[],[s465,s2490,s125,s2500]) ).
cnf(s2525,plain,
spl395_291,
inference(rat,[],[s799,s2497,s2480,s2490,s125,s132,s129,s128,s127,s122]) ).
cnf(s2530,plain,
spl395_127,
inference(rat,[],[s133,s2480,s125,s132,s128,s122]) ).
cnf(s2532,plain,
~ spl395_196,
inference(rat,[],[s752,s124,s2525]) ).
cnf(s2541,plain,
spl395_150,
inference(rat,[],[s2422,s2511,s2497,s2480,s2490,s127,s129,s130,s2530]) ).
cnf(s2545,plain,
~ spl395_290,
inference(rat,[],[s797,s2532]) ).
cnf(s2548,plain,
$false,
inference(rat,[],[s753,s2545,s2541]) ).
fof(f48057,plain,
$false,
inference(avatar_sat_refutation,[],[s2548]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU434+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.09/0.35 % Computer : n018.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 28 05:29:13 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.35 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.14/0.39 Running first-order theorem proving
% 0.14/0.39 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
% 16.38/4.09 % (3048307)Detected formulas, will run a generic FOF schedule.
% 16.38/4.09 % (3048313)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=292156964:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2988 on theBenchmark for (2988ds/134677Mi)
% 16.38/4.09 % (3048312)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=1545054088:i=141193_2988 on theBenchmark for (2988ds/141193Mi)
% 16.38/4.09 % (3048317)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3359326556:s2a=on:i=139:gtg=position_2988 on theBenchmark for (2988ds/139Mi)
% 16.38/4.09 % (3048315)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3409727473:i=109:sd=1:ins=1:gsp=on:ss=axioms_2988 on theBenchmark for (2988ds/109Mi)
% 16.38/4.09 % (3048318)dis-21_1_sil=8000:lcm=predicate:random_seed=3737561481:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2988 on theBenchmark for (2988ds/129Mi)
% 16.38/4.09 % (3048316)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1028036509:i=119:av=off:ss=axioms_2988 on theBenchmark for (2988ds/119Mi)
% 16.38/4.09 % (3048314)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=1002808303:i=141695:sd=1:nm=32:gsp=on:ss=included_2988 on theBenchmark for (2988ds/141695Mi)
% 16.38/4.09 % (3048317)Instruction limit reached!
% 16.38/4.09 % (3048317)------------------------------
% 16.38/4.09 % (3048317)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.38/4.09 % (3048317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.38/4.09 % (3048317)CaDiCaL version: 2.1.3
% 16.38/4.09 % (3048317)Termination reason: Instruction limit
% 16.38/4.09 % (3048317)Termination phase: Property scanning
% 16.38/4.09 % (3048317)Time elapsed: 0.062 s
% 16.38/4.09 % (3048317)Peak memory usage: 112 MB
% 16.38/4.09 % (3048317)Instructions burned: 139 (million)
% 16.38/4.09 % (3048315)Instruction limit reached!
% 16.38/4.09 % (3048315)------------------------------
% 16.38/4.09 % (3048315)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.38/4.09 % (3048315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.38/4.09 % (3048315)CaDiCaL version: 2.1.3
% 16.38/4.09 % (3048315)Termination reason: Instruction limit
% 16.38/4.09 % (3048315)Termination phase: SInE selection
% 16.38/4.09 % (3048315)Time elapsed: 0.081 s
% 16.38/4.09 % (3048315)Peak memory usage: 112 MB
% 16.38/4.09 % (3048315)Instructions burned: 110 (million)
% 16.38/4.09 % (3048318)Instruction limit reached!
% 16.38/4.09 % (3048318)------------------------------
% 16.38/4.09 % (3048318)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.38/4.09 % (3048318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.38/4.09 % (3048318)CaDiCaL version: 2.1.3
% 16.38/4.09 % (3048318)Termination reason: Instruction limit
% 16.38/4.09 % (3048318)Termination phase: SInE selection
% 16.38/4.09 % (3048318)Time elapsed: 0.086 s
% 16.38/4.09 % (3048318)Peak memory usage: 112 MB
% 16.38/4.09 % (3048318)Instructions burned: 130 (million)
% 16.38/4.09 % (3048316)Instruction limit reached!
% 16.38/4.09 % (3048316)------------------------------
% 16.38/4.09 % (3048316)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.38/4.09 % (3048316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.38/4.09 % (3048316)CaDiCaL version: 2.1.3
% 16.38/4.09 % (3048316)Termination reason: Instruction limit
% 16.38/4.09 % (3048316)Termination phase: Preprocessing 1
% 16.38/4.09 % (3048316)Time elapsed: 0.096 s
% 16.38/4.09 % (3048316)Peak memory usage: 113 MB
% 16.38/4.09 % (3048316)Instructions burned: 119 (million)
% 16.38/4.09 % (3048326)lrs+10_1_sil=8000:sp=occurrence:random_seed=3548784176:i=285:sd=3:ss=axioms:sgt=8_2986 on theBenchmark for (2986ds/285Mi)
% 16.38/4.09 % (3048327)lrs+10_1_sil=32000:urr=on:br=off:random_seed=945119226:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2986 on theBenchmark for (2986ds/157Mi)
% 16.38/4.09 % (3048328)lrs+1011_1_sil=32000:sp=occurrence:random_seed=691676021:i=325:sd=1:ss=axioms:sgt=32_2986 on theBenchmark for (2986ds/325Mi)
% 16.38/4.09 % (3048329)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=924502402:s2a=on:i=248:s2at=1.23:gtg=position_2986 on theBenchmark for (2986ds/248Mi)
% 16.38/4.09 % (3048327)Instruction limit reached!
% 23.43/5.08 % (3048327)------------------------------
% 23.43/5.08 % (3048327)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.43/5.08 % (3048327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.43/5.08 % (3048327)CaDiCaL version: 2.1.3
% 23.43/5.08 % (3048327)Termination reason: Instruction limit
% 23.43/5.08 % (3048327)Termination phase: Property scanning
% 23.43/5.08 % (3048327)Time elapsed: 0.068 s
% 23.43/5.08 % (3048327)Peak memory usage: 112 MB
% 23.43/5.08 % (3048327)Instructions burned: 159 (million)
% 23.43/5.08 % (3048329)Instruction limit reached!
% 23.43/5.08 % (3048329)------------------------------
% 23.43/5.08 % (3048329)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.43/5.08 % (3048329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.43/5.08 % (3048329)CaDiCaL version: 2.1.3
% 23.43/5.08 % (3048329)Termination reason: Instruction limit
% 23.43/5.08 % (3048329)Termination phase: Property scanning
% 23.43/5.08 % (3048329)Time elapsed: 0.108 s
% 23.43/5.08 % (3048329)Peak memory usage: 112 MB
% 23.43/5.08 % (3048329)Instructions burned: 249 (million)
% 23.43/5.08 % (3048326)Instruction limit reached!
% 23.43/5.08 % (3048326)------------------------------
% 23.43/5.08 % (3048326)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.43/5.08 % (3048326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.43/5.08 % (3048326)CaDiCaL version: 2.1.3
% 23.43/5.08 % (3048326)Termination reason: Instruction limit
% 23.43/5.08 % (3048326)Termination phase: Saturation
% 23.43/5.08 % (3048326)Time elapsed: 0.204 s
% 23.43/5.08 % (3048326)Peak memory usage: 119 MB
% 23.43/5.08 % (3048326)Instructions burned: 286 (million)
% 23.43/5.08 % (3048334)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2938299134:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2984 on theBenchmark for (2984ds/294Mi)
% 23.43/5.08 % (3048328)Instruction limit reached!
% 23.43/5.08 % (3048328)------------------------------
% 23.43/5.08 % (3048328)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.43/5.08 % (3048328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.43/5.08 % (3048328)CaDiCaL version: 2.1.3
% 23.43/5.08 % (3048328)Termination reason: Instruction limit
% 23.43/5.08 % (3048328)Termination phase: Saturation
% 23.43/5.08 % (3048328)Time elapsed: 0.261 s
% 23.43/5.08 % (3048328)Peak memory usage: 119 MB
% 23.43/5.08 % (3048328)Instructions burned: 325 (million)
% 23.43/5.08 % (3048335)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3681030199:i=2350_2983 on theBenchmark for (2983ds/2350Mi)
% 23.43/5.08 % (3048336)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2621949506:cts=off:i=113:fsr=off:ss=included:sgt=4_2982 on theBenchmark for (2982ds/113Mi)
% 23.43/5.08 % (3048334)Instruction limit reached!
% 23.43/5.08 % (3048334)------------------------------
% 23.43/5.08 % (3048334)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.43/5.08 % (3048334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.43/5.08 % (3048334)CaDiCaL version: 2.1.3
% 23.43/5.08 % (3048334)Termination reason: Instruction limit
% 23.43/5.08 % (3048334)Termination phase: Property scanning
% 23.43/5.08 % (3048334)Time elapsed: 0.219 s
% 23.43/5.08 % (3048334)Peak memory usage: 119 MB
% 23.43/5.08 % (3048334)Instructions burned: 294 (million)
% 23.43/5.08 % (3048338)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3129628151:i=127:av=off:fsr=off:sup=off_2982 on theBenchmark for (2982ds/127Mi)
% 23.43/5.08 % (3048336)Instruction limit reached!
% 23.43/5.08 % (3048336)------------------------------
% 23.43/5.08 % (3048336)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.43/5.08 % (3048336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.43/5.08 % (3048336)CaDiCaL version: 2.1.3
% 23.43/5.08 % (3048336)Termination reason: Instruction limit
% 23.43/5.08 % (3048336)Termination phase: SInE selection
% 23.43/5.08 % (3048336)Time elapsed: 0.092 s
% 23.43/5.08 % (3048336)Peak memory usage: 112 MB
% 23.43/5.08 % (3048336)Instructions burned: 113 (million)
% 23.43/5.08 % (3048338)Instruction limit reached!
% 23.43/5.08 % (3048338)------------------------------
% 23.43/5.08 % (3048338)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.43/5.08 % (3048338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.43/5.08 % (3048338)CaDiCaL version: 2.1.3
% 62.95/10.61 % (3048338)Termination reason: Instruction limit
% 62.95/10.61 % (3048338)Termination phase: Preprocessing 1
% 62.95/10.61 % (3048338)Time elapsed: 0.094 s
% 62.95/10.61 % (3048338)Peak memory usage: 113 MB
% 62.95/10.61 % (3048338)Instructions burned: 128 (million)
% 62.95/10.61 % (3048342)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2425684253:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2980 on theBenchmark for (2980ds/114Mi)
% 62.95/10.61 % (3048343)lrs+10_1_sil=8000:sp=occurrence:random_seed=4082467177:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2980 on theBenchmark for (2980ds/907Mi)
% 62.95/10.61 % (3048342)Instruction limit reached!
% 62.95/10.61 % (3048342)------------------------------
% 62.95/10.61 % (3048342)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.95/10.61 % (3048342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.95/10.61 % (3048342)CaDiCaL version: 2.1.3
% 62.95/10.61 % (3048342)Termination reason: Instruction limit
% 62.95/10.61 % (3048342)Termination phase: Property scanning
% 62.95/10.61 % (3048342)Time elapsed: 0.050 s
% 62.95/10.61 % (3048342)Peak memory usage: 112 MB
% 62.95/10.61 % (3048342)Instructions burned: 114 (million)
% 62.95/10.61 % (3048344)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1079197480:i=437:sd=1:aac=none:ss=included_2979 on theBenchmark for (2979ds/437Mi)
% 62.95/10.61 % (3048347)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2795669213:i=5202:ss=axioms:sgt=16_2978 on theBenchmark for (2978ds/5202Mi)
% 62.95/10.61 % (3048344)Instruction limit reached!
% 62.95/10.61 % (3048344)------------------------------
% 62.95/10.61 % (3048344)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.95/10.61 % (3048344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.95/10.61 % (3048344)CaDiCaL version: 2.1.3
% 62.95/10.61 % (3048344)Termination reason: Instruction limit
% 62.95/10.61 % (3048344)Termination phase: Saturation
% 62.95/10.61 % (3048344)Time elapsed: 0.300 s
% 62.95/10.61 % (3048344)Peak memory usage: 120 MB
% 62.95/10.61 % (3048344)Instructions burned: 438 (million)
% 62.95/10.61 % (3048343)Instruction limit reached!
% 62.95/10.61 % (3048343)------------------------------
% 62.95/10.61 % (3048343)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.95/10.61 % (3048343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.95/10.61 % (3048343)CaDiCaL version: 2.1.3
% 62.95/10.61 % (3048343)Termination reason: Instruction limit
% 62.95/10.61 % (3048343)Termination phase: Saturation
% 62.95/10.61 % (3048343)Time elapsed: 0.525 s
% 62.95/10.61 % (3048343)Peak memory usage: 131 MB
% 62.95/10.61 % (3048343)Instructions burned: 908 (million)
% 62.95/10.61 % (3048350)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2696260979:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2974 on theBenchmark for (2974ds/134Mi)
% 62.95/10.61 % (3048350)Instruction limit reached!
% 62.95/10.61 % (3048350)------------------------------
% 62.95/10.61 % (3048350)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.95/10.61 % (3048350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.95/10.61 % (3048350)CaDiCaL version: 2.1.3
% 62.95/10.61 % (3048350)Termination reason: Instruction limit
% 62.95/10.61 % (3048350)Termination phase: NewCNF
% 62.95/10.61 % (3048350)Time elapsed: 0.120 s
% 62.95/10.61 % (3048350)Peak memory usage: 115 MB
% 62.95/10.61 % (3048350)Instructions burned: 134 (million)
% 62.95/10.61 % (3048351)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2754882999:st=8:i=592:sd=3:ep=RST:ss=axioms_2973 on theBenchmark for (2973ds/592Mi)
% 62.95/10.61 % (3048354)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2964011012:st=3:i=13193:sd=3:ss=axioms_2971 on theBenchmark for (2971ds/13193Mi)
% 62.95/10.61 % (3048335)Instruction limit reached!
% 62.95/10.61 % (3048335)------------------------------
% 62.95/10.61 % (3048335)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.95/10.61 % (3048335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.95/10.61 % (3048335)CaDiCaL version: 2.1.3
% 62.95/10.61 % (3048335)Termination reason: Instruction limit
% 62.95/10.61 % (3048335)Termination phase: Property scanning
% 62.95/10.61 % (3048335)Time elapsed: 1.292 s
% 62.95/10.61 % (3048335)Peak memory usage: 171 MB
% 62.95/10.61 % (3048335)Instructions burned: 2390 (million)
% 62.95/10.61 % (3048351)Instruction limit reached!
% 62.95/10.61 % (3048351)------------------------------
% 62.95/10.61 % (3048351)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.18/15.14 % (3048351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.18/15.14 % (3048351)CaDiCaL version: 2.1.3
% 95.18/15.14 % (3048351)Termination reason: Instruction limit
% 95.18/15.14 % (3048351)Termination phase: Preprocessing 3
% 95.18/15.14 % (3048351)Time elapsed: 0.446 s
% 95.18/15.14 % (3048351)Peak memory usage: 135 MB
% 95.18/15.14 % (3048351)Instructions burned: 593 (million)
% 95.18/15.14 % (3048356)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=2796173081:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2968 on theBenchmark for (2968ds/125Mi)
% 95.18/15.14 % (3048356)Instruction limit reached!
% 95.18/15.14 % (3048356)------------------------------
% 95.18/15.14 % (3048356)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.18/15.14 % (3048356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.18/15.14 % (3048356)CaDiCaL version: 2.1.3
% 95.18/15.14 % (3048356)Termination reason: Instruction limit
% 95.18/15.14 % (3048356)Termination phase: Property scanning
% 95.18/15.14 % (3048356)Time elapsed: 0.054 s
% 95.18/15.14 % (3048356)Peak memory usage: 112 MB
% 95.18/15.14 % (3048356)Instructions burned: 126 (million)
% 95.18/15.14 % (3048357)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2466028105:i=134:gtgl=5:slsql=off:gtg=exists_sym_2967 on theBenchmark for (2967ds/134Mi)
% 95.18/15.14 % (3048359)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1572498719:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2966 on theBenchmark for (2966ds/141Mi)
% 95.18/15.14 % (3048357)Instruction limit reached!
% 95.18/15.14 % (3048357)------------------------------
% 95.18/15.14 % (3048357)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.18/15.14 % (3048357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.18/15.14 % (3048357)CaDiCaL version: 2.1.3
% 95.18/15.14 % (3048357)Termination reason: Instruction limit
% 95.18/15.14 % (3048357)Termination phase: Property scanning
% 95.18/15.14 % (3048357)Time elapsed: 0.059 s
% 95.18/15.14 % (3048357)Peak memory usage: 112 MB
% 95.18/15.14 % (3048357)Instructions burned: 136 (million)
% 95.18/15.14 % (3048359)Instruction limit reached!
% 95.18/15.14 % (3048359)------------------------------
% 95.18/15.14 % (3048359)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.18/15.14 % (3048359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.18/15.14 % (3048359)CaDiCaL version: 2.1.3
% 95.18/15.14 % (3048359)Termination reason: Instruction limit
% 95.18/15.14 % (3048359)Termination phase: Saturation
% 95.18/15.14 % (3048359)Time elapsed: 0.119 s
% 95.18/15.14 % (3048359)Peak memory usage: 117 MB
% 95.18/15.14 % (3048359)Instructions burned: 142 (million)
% 95.18/15.14 % (3048362)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=757124808:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2965 on theBenchmark for (2965ds/431Mi)
% 95.18/15.14 % (3048363)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=3041801274:i=6060:aac=none:ins=25_2963 on theBenchmark for (2963ds/6060Mi)
% 95.18/15.14 % (3048362)Instruction limit reached!
% 95.18/15.14 % (3048362)------------------------------
% 95.18/15.14 % (3048362)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.18/15.14 % (3048362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.18/15.14 % (3048362)CaDiCaL version: 2.1.3
% 95.18/15.14 % (3048362)Termination reason: Instruction limit
% 95.18/15.14 % (3048362)Termination phase: Saturation
% 95.18/15.14 % (3048362)Time elapsed: 0.286 s
% 95.18/15.14 % (3048362)Peak memory usage: 120 MB
% 95.18/15.14 % (3048362)Instructions burned: 431 (million)
% 95.18/15.14 % (3048366)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=3021177345:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2960 on theBenchmark for (2960ds/150Mi)
% 95.18/15.14 % (3048366)Instruction limit reached!
% 95.18/15.14 % (3048366)------------------------------
% 95.18/15.14 % (3048366)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.18/15.14 % (3048366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.18/15.14 % (3048366)CaDiCaL version: 2.1.3
% 95.18/15.14 % (3048366)Termination reason: Instruction limit
% 129.94/20.10 % (3048366)Termination phase: Preprocessing 1
% 129.94/20.10 % (3048366)Time elapsed: 0.123 s
% 129.94/20.10 % (3048366)Peak memory usage: 113 MB
% 129.94/20.10 % (3048366)Instructions burned: 151 (million)
% 129.94/20.10 % (3048368)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3778377757:i=14155:bd=all_2957 on theBenchmark for (2957ds/14155Mi)
% 129.94/20.10 % (3048347)Instruction limit reached!
% 129.94/20.10 % (3048347)------------------------------
% 129.94/20.10 % (3048347)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 129.94/20.10 % (3048347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 129.94/20.10 % (3048347)CaDiCaL version: 2.1.3
% 129.94/20.10 % (3048347)Termination reason: Instruction limit
% 129.94/20.10 % (3048347)Termination phase: Saturation
% 129.94/20.10 % (3048347)Time elapsed: 3.065 s
% 129.94/20.10 % (3048347)Peak memory usage: 192 MB
% 129.94/20.10 % (3048347)Instructions burned: 5204 (million)
% 129.94/20.10 % (3048370)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=4060019162:i=667:av=off:fsr=off_2945 on theBenchmark for (2945ds/667Mi)
% 129.94/20.11 % (3048370)Instruction limit reached!
% 129.94/20.11 % (3048370)------------------------------
% 129.94/20.11 % (3048370)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 129.94/20.11 % (3048370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 129.94/20.11 % (3048370)CaDiCaL version: 2.1.3
% 129.94/20.11 % (3048370)Termination reason: Instruction limit
% 129.94/20.11 % (3048370)Termination phase: NewCNF
% 129.94/20.11 % (3048370)Time elapsed: 0.527 s
% 129.94/20.11 % (3048370)Peak memory usage: 149 MB
% 129.94/20.11 % (3048370)Instructions burned: 669 (million)
% 129.94/20.11 % (3048372)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=3428072426:s2a=on:i=185:s2at=1.8:fdi=4_2938 on theBenchmark for (2938ds/185Mi)
% 129.94/20.11 % (3048372)Instruction limit reached!
% 129.94/20.11 % (3048372)------------------------------
% 129.94/20.11 % (3048372)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 129.94/20.11 % (3048372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 129.94/20.11 % (3048372)CaDiCaL version: 2.1.3
% 129.94/20.11 % (3048372)Termination reason: Instruction limit
% 129.94/20.11 % (3048372)Termination phase: SInE selection
% 129.94/20.11 % (3048372)Time elapsed: 0.145 s
% 129.94/20.11 % (3048372)Peak memory usage: 113 MB
% 129.94/20.11 % (3048372)Instructions burned: 185 (million)
% 129.94/20.11 % (3048374)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=3373650443:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2935 on theBenchmark for (2935ds/193Mi)
% 129.94/20.11 % (3048374)Instruction limit reached!
% 129.94/20.11 % (3048374)------------------------------
% 129.94/20.11 % (3048374)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 129.94/20.11 % (3048374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 129.94/20.11 % (3048374)CaDiCaL version: 2.1.3
% 129.94/20.11 % (3048374)Termination reason: Instruction limit
% 129.94/20.11 % (3048374)Termination phase: SInE selection
% 129.94/20.11 % (3048374)Time elapsed: 0.161 s
% 129.94/20.11 % (3048374)Peak memory usage: 112 MB
% 129.94/20.11 % (3048374)Instructions burned: 194 (million)
% 129.94/20.11 % (3048376)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=3158313008:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2932 on theBenchmark for (2932ds/4850Mi)
% 129.94/20.11 % (3048363)Instruction limit reached!
% 129.94/20.11 % (3048363)------------------------------
% 129.94/20.11 % (3048363)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 129.94/20.11 % (3048363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 129.94/20.11 % (3048363)CaDiCaL version: 2.1.3
% 129.94/20.11 % (3048363)Termination reason: Instruction limit
% 129.94/20.11 % (3048363)Termination phase: Saturation
% 129.94/20.11 % (3048363)Time elapsed: 4.540 s
% 129.94/20.11 % (3048363)Peak memory usage: 632 MB
% 129.94/20.11 % (3048363)Instructions burned: 6061 (million)
% 129.94/20.11 % (3048378)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=4261318959:i=12111:sd=1:ss=included_2916 on theBenchmark for (2916ds/12111Mi)
% 129.94/20.11 % (3048376)Instruction limit reached!
% 129.94/20.11 % (3048376)------------------------------
% 129.94/20.11 % (3048376)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 164.08/24.93 % (3048376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 164.08/24.93 % (3048376)CaDiCaL version: 2.1.3
% 164.08/24.93 % (3048376)Termination reason: Instruction limit
% 164.08/24.93 % (3048376)Termination phase: Saturation
% 164.08/24.93 % (3048376)Time elapsed: 2.820 s
% 164.08/24.93 % (3048376)Peak memory usage: 222 MB
% 164.08/24.93 % (3048376)Instructions burned: 4850 (million)
% 164.08/24.93 % (3048380)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2671642453:i=319:kws=precedence:fsr=off_2902 on theBenchmark for (2902ds/319Mi)
% 164.08/24.93 % (3048380)Instruction limit reached!
% 164.08/24.93 % (3048380)------------------------------
% 164.08/24.93 % (3048380)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 164.08/24.93 % (3048380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 164.08/24.93 % (3048380)CaDiCaL version: 2.1.3
% 164.08/24.93 % (3048380)Termination reason: Instruction limit
% 164.08/24.93 % (3048380)Termination phase: Naming
% 164.08/24.93 % (3048380)Time elapsed: 0.265 s
% 164.08/24.93 % (3048380)Peak memory usage: 135 MB
% 164.08/24.93 % (3048380)Instructions burned: 319 (million)
% 164.08/24.93 % (3048382)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=3172319398:i=2064:ep=RST_2897 on theBenchmark for (2897ds/2064Mi)
% 164.08/24.93 % (3048354)Instruction limit reached!
% 164.08/24.93 % (3048354)------------------------------
% 164.08/24.93 % (3048354)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 164.08/24.93 % (3048354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 164.08/24.93 % (3048354)CaDiCaL version: 2.1.3
% 164.08/24.93 % (3048354)Termination reason: Instruction limit
% 164.08/24.93 % (3048354)Termination phase: Saturation
% 164.08/24.93 % (3048354)Time elapsed: 8.082 s
% 164.08/24.93 % (3048354)Peak memory usage: 314 MB
% 164.08/24.93 % (3048354)Instructions burned: 13194 (million)
% 164.08/24.93 % (3048384)dis-1011_128_sil=32000:random_seed=763861554:i=3706:ep=RST:av=off_2889 on theBenchmark for (2889ds/3706Mi)
% 164.08/24.93 % (3048382)Instruction limit reached!
% 164.08/24.93 % (3048382)------------------------------
% 164.08/24.93 % (3048382)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 164.08/24.93 % (3048382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 164.08/24.93 % (3048382)CaDiCaL version: 2.1.3
% 164.08/24.93 % (3048382)Termination reason: Instruction limit
% 164.08/24.93 % (3048382)Termination phase: Property scanning
% 164.08/24.93 % (3048382)Time elapsed: 1.129 s
% 164.08/24.93 % (3048382)Peak memory usage: 171 MB
% 164.08/24.93 % (3048382)Instructions burned: 2065 (million)
% 164.08/24.93 % (3048386)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=99347584:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2884 on theBenchmark for (2884ds/757Mi)
% 164.08/24.93 % (3048386)Instruction limit reached!
% 164.08/24.93 % (3048386)------------------------------
% 164.08/24.93 % (3048386)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 164.08/24.93 % (3048386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 164.08/24.93 % (3048386)CaDiCaL version: 2.1.3
% 164.08/24.93 % (3048386)Termination reason: Instruction limit
% 164.08/24.93 % (3048386)Termination phase: Saturation
% 164.08/24.93 % (3048386)Time elapsed: 0.544 s
% 164.08/24.93 % (3048386)Peak memory usage: 127 MB
% 164.08/24.93 % (3048386)Instructions burned: 757 (million)
% 164.08/24.93 % (3048388)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=586597593:i=13913:ss=axioms:sgt=8_2877 on theBenchmark for (2877ds/13913Mi)
% 164.08/24.93 % (3048384)Instruction limit reached!
% 164.08/24.93 % (3048384)------------------------------
% 164.08/24.93 % (3048384)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 164.08/24.93 % (3048384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 164.08/24.93 % (3048384)CaDiCaL version: 2.1.3
% 164.08/24.93 % (3048384)Termination reason: Instruction limit
% 164.08/24.93 % (3048384)Termination phase: Saturation
% 164.08/24.93 % (3048384)Time elapsed: 1.843 s
% 164.08/24.93 % (3048384)Peak memory usage: 186 MB
% 164.08/24.93 % (3048384)Instructions burned: 3706 (million)
% 164.08/24.93 % (3048390)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=3887396463:i=9925:aac=none_2868 on theBenchmark for (2868ds/9925Mi)
% 164.08/24.93 % (3048368)Instruction limit reached!
% 164.08/24.93 % (3048368)------------------------------
% 164.08/24.93 % (3048368)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 192.66/28.91 % (3048368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 192.66/28.91 % (3048368)CaDiCaL version: 2.1.3
% 192.66/28.91 % (3048368)Termination reason: Instruction limit
% 192.66/28.91 % (3048368)Termination phase: Saturation
% 192.66/28.91 % (3048368)Time elapsed: 9.883 s
% 192.66/28.91 % (3048368)Peak memory usage: 761 MB
% 192.66/28.91 % (3048368)Instructions burned: 14155 (million)
% 192.66/28.91 % (3048392)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=985427288:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2856 on theBenchmark for (2856ds/2479Mi)
% 192.66/28.91 % (3048392)Instruction limit reached!
% 192.66/28.91 % (3048392)------------------------------
% 192.66/28.91 % (3048392)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 192.66/28.91 % (3048392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 192.66/28.91 % (3048392)CaDiCaL version: 2.1.3
% 192.66/28.91 % (3048392)Termination reason: Instruction limit
% 192.66/28.91 % (3048392)Termination phase: Saturation
% 192.66/28.91 % (3048392)Time elapsed: 1.514 s
% 192.66/28.91 % (3048392)Peak memory usage: 138 MB
% 192.66/28.91 % (3048392)Instructions burned: 2479 (million)
% 192.66/28.91 % (3048394)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=1582799875:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2839 on theBenchmark for (2839ds/440Mi)
% 192.66/28.91 % (3048394)Instruction limit reached!
% 192.66/28.91 % (3048394)------------------------------
% 192.66/28.91 % (3048394)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 192.66/28.91 % (3048394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 192.66/28.91 % (3048394)CaDiCaL version: 2.1.3
% 192.66/28.91 % (3048394)Termination reason: Instruction limit
% 192.66/28.91 % (3048394)Termination phase: Property scanning
% 192.66/28.91 % (3048394)Time elapsed: 0.197 s
% 192.66/28.91 % (3048394)Peak memory usage: 112 MB
% 192.66/28.91 % (3048394)Instructions burned: 443 (million)
% 192.66/28.91 % (3048396)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=3523702228:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2835 on theBenchmark for (2835ds/11145Mi)
% 192.66/28.91 % (3048378)Instruction limit reached!
% 192.66/28.91 % (3048378)------------------------------
% 192.66/28.91 % (3048378)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 192.66/28.91 % (3048378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 192.66/28.91 % (3048378)CaDiCaL version: 2.1.3
% 192.66/28.91 % (3048378)Termination reason: Instruction limit
% 192.66/28.91 % (3048378)Termination phase: Saturation
% 192.66/28.91 % (3048378)Time elapsed: 8.100 s
% 192.66/28.91 % (3048378)Peak memory usage: 269 MB
% 192.66/28.91 % (3048378)Instructions burned: 12112 (million)
% 192.66/28.91 % (3048398)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=4053806517:cts=off:i=3034:av=off:er=known:fsd=on_2833 on theBenchmark for (2833ds/3034Mi)
% 192.66/28.91 % (3048398)Instruction limit reached!
% 192.66/28.91 % (3048398)------------------------------
% 192.66/28.91 % (3048398)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 192.66/28.91 % (3048398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 192.66/28.91 % (3048398)CaDiCaL version: 2.1.3
% 192.66/28.91 % (3048398)Termination reason: Instruction limit
% 192.66/28.91 % (3048398)Termination phase: Saturation
% 192.66/28.91 % (3048398)Time elapsed: 1.650 s
% 192.66/28.91 % (3048398)Peak memory usage: 190 MB
% 192.66/28.91 % (3048398)Instructions burned: 3034 (million)
% 192.66/28.91 % (3048400)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=1718889087:st=2:s2a=on:i=524:s2at=2:ss=axioms_2815 on theBenchmark for (2815ds/524Mi)
% 192.66/28.91 % (3048400)Instruction limit reached!
% 192.66/28.91 % (3048400)------------------------------
% 192.66/28.91 % (3048400)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 192.66/28.91 % (3048400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 192.66/28.91 % (3048400)CaDiCaL version: 2.1.3
% 192.66/28.91 % (3048400)Termination reason: Instruction limit
% 192.66/28.91 % (3048400)Termination phase: Preprocessing 1
% 192.66/28.91 % (3048400)Time elapsed: 0.414 s
% 192.66/28.91 % (3048400)Peak memory usage: 114 MB
% 192.66/28.91 % (3048400)Instructions burned: 524 (million)
% 192.66/28.91 % (3048402)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=1216261585:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2809 on theBenchmark for (2809ds/1016Mi)
% 114.21/30.78 % (3048402)Instruction limit reached!
% 114.21/30.78 % (3048402)------------------------------
% 114.21/30.78 % (3048402)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 114.21/30.78 % (3048402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.21/30.78 % (3048402)CaDiCaL version: 2.1.3
% 114.21/30.78 % (3048402)Termination reason: Instruction limit
% 114.21/30.78 % (3048402)Termination phase: Saturation
% 114.21/30.78 % (3048402)Time elapsed: 0.639 s
% 114.21/30.78 % (3048402)Peak memory usage: 129 MB
% 114.21/30.78 % (3048402)Instructions burned: 1017 (million)
% 114.21/30.78 % (3048404)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=2788098446:i=14123:bd=preordered:ins=4_2800 on theBenchmark for (2800ds/14123Mi)
% 114.21/30.78 % (3048390)Instruction limit reached!
% 114.21/30.78 % (3048390)------------------------------
% 114.21/30.78 % (3048390)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 114.21/30.78 % (3048390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.21/30.78 % (3048390)CaDiCaL version: 2.1.3
% 114.21/30.78 % (3048390)Termination reason: Instruction limit
% 114.21/30.78 % (3048390)Termination phase: Saturation
% 114.21/30.78 % (3048390)Time elapsed: 7.085 s
% 114.21/30.78 % (3048390)Peak memory usage: 503 MB
% 114.21/30.78 % (3048390)Instructions burned: 9925 (million)
% 114.21/30.78 % (3048406)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=4073142883:i=5781:kws=precedence:bd=all:rawr=on_2795 on theBenchmark for (2795ds/5781Mi)
% 114.21/30.78 % (3048388)Instruction limit reached!
% 114.21/30.78 % (3048388)------------------------------
% 114.21/30.78 % (3048388)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 114.21/30.78 % (3048388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.21/30.78 % (3048388)CaDiCaL version: 2.1.3
% 114.21/30.78 % (3048388)Termination reason: Instruction limit
% 114.21/30.78 % (3048388)Termination phase: Saturation
% 114.21/30.78 % (3048388)Time elapsed: 8.926 s
% 114.21/30.78 % (3048388)Peak memory usage: 274 MB
% 114.21/30.78 % (3048388)Instructions burned: 13914 (million)
% 114.21/30.78 % (3048408)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=2670753033:i=2448:gtgl=5:bd=preordered:gtg=all_2785 on theBenchmark for (2785ds/2448Mi)
% 114.21/30.78 % (3048408)Instruction limit reached!
% 114.21/30.78 % (3048408)------------------------------
% 114.21/30.78 % (3048408)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 114.21/30.78 % (3048408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.21/30.78 % (3048408)CaDiCaL version: 2.1.3
% 114.21/30.78 % (3048408)Termination reason: Instruction limit
% 114.21/30.78 % (3048408)Termination phase: Function definition elimination
% 114.21/30.78 % (3048408)Time elapsed: 1.310 s
% 114.21/30.78 % (3048408)Peak memory usage: 168 MB
% 114.21/30.78 % (3048408)Instructions burned: 2450 (million)
% 114.21/30.78 % (3048410)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=813179166:i=3223:kws=precedence:fgj=on:av=off_2771 on theBenchmark for (2771ds/3223Mi)
% 114.21/30.78 % (3048406)Instruction limit reached!
% 114.21/30.78 % (3048406)------------------------------
% 114.21/30.78 % (3048406)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 114.21/30.78 % (3048406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.21/30.78 % (3048406)CaDiCaL version: 2.1.3
% 114.21/30.78 % (3048406)Termination reason: Instruction limit
% 114.21/30.78 % (3048406)Termination phase: Saturation
% 114.21/30.78 % (3048406)Time elapsed: 3.058 s
% 114.21/30.78 % (3048406)Peak memory usage: 197 MB
% 114.21/30.78 % (3048406)Instructions burned: 5783 (million)
% 114.21/30.78 % (3048412)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=671668772:st=5.6:i=2033:sd=3:ss=axioms_2763 on theBenchmark for (2763ds/2033Mi)
% 114.21/30.78 % (3048396)Instruction limit reached!
% 114.21/30.78 % (3048396)------------------------------
% 114.21/30.78 % (3048396)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 114.21/30.78 % (3048396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.21/30.78 % (3048396)CaDiCaL version: 2.1.3
% 114.21/30.78 % (3048396)Termination reason: Instruction limit
% 114.21/30.78 % (3048396)Termination phase: Saturation
% 114.21/30.78 % (3048396)Time elapsed: 7.466 s
% 114.21/30.78 % (3048396)Peak memory usage: 246 MB
% 114.21/30.78 % (3048396)Instructions burned: 11145 (million)
% 114.21/30.78 % (3048414)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=3218286132:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2758 on theBenchmark for (2758ds/2055Mi)
% 114.21/30.78 % (3048410)Instruction limit reached!
% 114.21/30.78 % (3048410)------------------------------
% 114.21/30.78 % (3048410)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 114.21/30.78 % (3048410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.21/30.78 % (3048410)CaDiCaL version: 2.1.3
% 114.21/30.78 % (3048410)Termination reason: Instruction limit
% 114.21/30.78 % (3048410)Termination phase: Saturation
% 114.21/30.78 % (3048410)Time elapsed: 1.801 s
% 114.21/30.78 % (3048410)Peak memory usage: 214 MB
% 114.21/30.78 % (3048410)Instructions burned: 3223 (million)
% 114.21/30.78 % (3048412)Instruction limit reached!
% 114.21/30.78 % (3048412)------------------------------
% 114.21/30.78 % (3048412)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 114.21/30.78 % (3048412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.21/30.78 % (3048412)CaDiCaL version: 2.1.3
% 114.21/30.78 % (3048412)Termination reason: Instruction limit
% 114.21/30.78 % (3048412)Termination phase: Saturation
% 114.21/30.78 % (3048412)Time elapsed: 1.202 s
% 114.21/30.78 % (3048412)Peak memory usage: 162 MB
% 114.21/30.78 % (3048412)Instructions burned: 2034 (million)
% 114.21/30.78 % (3048416)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=2280092474:i=21611:sd=3:ss=axioms_2751 on theBenchmark for (2751ds/21611Mi)
% 114.21/30.78 % (3048417)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=3445534187:i=4835:sd=13:ss=axioms:sgt=23_2749 on theBenchmark for (2749ds/4835Mi)
% 114.21/30.78 % (3048414)Instruction limit reached!
% 114.21/30.78 % (3048414)------------------------------
% 114.21/30.78 % (3048414)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 114.21/30.78 % (3048414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.21/30.78 % (3048414)CaDiCaL version: 2.1.3
% 114.21/30.78 % (3048414)Termination reason: Instruction limit
% 114.21/30.78 % (3048414)Termination phase: Saturation
% 114.21/30.78 % (3048414)Time elapsed: 1.311 s
% 114.21/30.78 % (3048414)Peak memory usage: 191 MB
% 114.21/30.78 % (3048414)Instructions burned: 2056 (million)
% 114.21/30.78 % (3048420)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=2182111223:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2743 on theBenchmark for (2743ds/797Mi)
% 114.21/30.78 % (3048420)Instruction limit reached!
% 114.21/30.78 % (3048420)------------------------------
% 114.21/30.78 % (3048420)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 114.21/30.78 % (3048420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.21/30.78 % (3048420)CaDiCaL version: 2.1.3
% 114.21/30.78 % (3048420)Termination reason: Instruction limit
% 114.21/30.78 % (3048420)Termination phase: NewCNF
% 114.21/30.78 % (3048420)Time elapsed: 0.628 s
% 114.21/30.78 % (3048420)Peak memory usage: 138 MB
% 114.21/30.78 % (3048420)Instructions burned: 798 (million)
% 114.21/30.78 % (3048422)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=3514536819:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2735 on theBenchmark for (2735ds/2326Mi)
% 114.21/30.78 % (3048422)Instruction limit reached!
% 114.21/30.78 % (3048422)------------------------------
% 114.21/30.78 % (3048422)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 114.21/30.78 % (3048422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.21/30.78 % (3048422)CaDiCaL version: 2.1.3
% 114.21/30.78 % (3048422)Termination reason: Instruction limit
% 114.21/30.78 % (3048422)Termination phase: Property scanning
% 114.21/30.78 % (3048422)Time elapsed: 1.210 s
% 114.21/30.78 % (3048422)Peak memory usage: 177 MB
% 114.21/30.78 % (3048422)Instructions burned: 2328 (million)
% 114.21/30.78 % (3048424)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=3275916045:i=6038:nm=6_2721 on theBenchmark for (2721ds/6038Mi)
% 114.21/30.78 % (3048417)Instruction limit reached!
% 114.21/30.78 % (3048417)------------------------------
% 114.21/30.78 % (3048417)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 114.21/30.78 % (3048417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.21/30.78 % (3048417)CaDiCaL version: 2.1.3
% 114.21/30.78 % (3048417)Termination reason: Instruction limit
% 114.21/30.78 % (3048417)Termination phase: Saturation
% 114.21/30.78 % (3048417)Time elapsed: 2.890 s
% 114.21/30.78 % (3048417)Peak memory usage: 147 MB
% 114.21/30.78 % (3048417)Instructions burned: 4836 (million)
% 114.21/30.78 % (3048426)lrs+10_1_sil=32000:sp=occurrence:random_seed=3409103987:st=2:i=33334:sd=3:ss=included:sgt=32_2719 on theBenchmark for (2719ds/33334Mi)
% 114.21/30.78 % (3048404)Instruction limit reached!
% 114.21/30.78 % (3048404)------------------------------
% 114.21/30.78 % (3048404)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 114.21/30.78 % (3048404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.21/30.78 % (3048404)CaDiCaL version: 2.1.3
% 114.21/30.78 % (3048404)Termination reason: Instruction limit
% 114.21/30.78 % (3048404)Termination phase: Saturation
% 114.21/30.78 % (3048404)Time elapsed: 9.441 s
% 114.21/30.78 % (3048404)Peak memory usage: 500 MB
% 114.21/30.78 % (3048404)Instructions burned: 14123 (million)
% 114.21/30.78 % (3048416)First to succeed.
% 114.21/30.78 % (3048416)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3048307"
% 114.21/30.78 % (3048428)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=979080562:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2704 on theBenchmark for (2704ds/1008Mi)
% 114.21/30.78 % (3048416)Refutation found. Thanks to Tanya!
% 114.21/30.78 % SZS status Theorem for theBenchmark
% 114.21/30.78 % SZS output start Proof for theBenchmark
% See solution above
% 206.02/30.98 % (3048416)------------------------------
% 206.02/30.98 % (3048416)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 206.02/30.98 % (3048416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 206.02/30.98 % (3048416)CaDiCaL version: 2.1.3
% 206.02/30.98 % (3048416)Termination reason: Refutation
% 206.02/30.98 % (3048416)Time elapsed: 4.543 s
% 206.02/30.98 % (3048416)Peak memory usage: 214 MB
% 206.02/30.98 % (3048416)Instructions burned: 7058 (million)
% 206.02/30.98 % (3048416)------------------------------
% 206.02/30.98 % (3048416)------------------------------
% 206.02/30.98 % (3048307)Success in time 29.945 s
% 206.02/30.98 % Vampire exiting
%------------------------------------------------------------------------------