%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU423+4 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n015.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:48:55 PM UTC 2026
% Result : Theorem 149.53s 30.76s
% Output : Refutation 177.60s
% Verified :
% SZS Type : Refutation
% Derivation depth : 34
% Number of leaves : 31
% Syntax : Number of formulae : 203 ( 37 unt; 17 def)
% Number of atoms : 931 ( 74 equ)
% Maximal formula atoms : 15 ( 4 avg)
% Number of connectives : 1270 ( 542 ~; 598 |; 83 &)
% ( 30 <=>; 17 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 7 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 22 ( 20 usr; 14 prp; 0-3 aty)
% Number of functors : 27 ( 27 usr; 8 con; 0-5 aty)
% Number of variables : 412 ( 0 sgn 382 !; 30 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f8,axiom,
! [X0,X1] :
( r1_tarski(X0,X1)
<=> ! [X2] :
( r2_hidden(X2,X0)
=> r2_hidden(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d3_tarski) ).
fof(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/sandbox2/benchmark/theBenchmark.p',d4_tarski) ).
fof(f38,axiom,
! [X0,X1] :
( X0 = X1
<=> ( r1_tarski(X0,X1)
& r1_tarski(X1,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d10_xboole_0) ).
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/sandbox2/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/sandbox2/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/sandbox2/benchmark/theBenchmark.p',t143_relat_1) ).
fof(f1422,axiom,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
=> v1_relat_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc1_relset_1) ).
fof(f1481,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/sandbox2/benchmark/theBenchmark.p',dt_m2_relset_1) ).
fof(f1483,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
<=> m1_relset_1(X2,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(f1508,axiom,
! [X0,X1,X2,X3] :
( m1_relset_1(X2,X0,X1)
=> k10_relset_1(X0,X1,X2,X3) = k9_relat_1(X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k10_relset_1) ).
fof(f71064,axiom,
! [X0,X1,X2,X3,X4] :
( ( ~ v1_xboole_0(X1)
& m1_subset_1(X3,k1_zfmisc_1(X1))
& m2_relset_1(X4,X1,X2) )
=> ( r2_hidden(X0,a_4_0_relset_2(X1,X2,X3,X4))
<=> ? [X5] :
( m1_subset_1(X5,X1)
& X0 = k2_relset_2(X1,X2,X4,X5)
& r2_hidden(X5,X3) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fraenkel_a_4_0_relset_2) ).
fof(f71089,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
=> ! [X3] :
( m1_subset_1(X3,X0)
=> k2_relset_2(X0,X1,X2,X3) = k10_relset_1(X0,X1,X2,k1_tarski(X3)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_relset_2) ).
fof(f71090,axiom,
! [X0,X1,X2] :
( v1_relat_1(X2)
=> ( r2_hidden(X0,k9_relat_1(X2,k1_tarski(X1)))
<=> r2_hidden(k4_tarski(X1,X0),X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t9_relset_2) ).
fof(f71099,conjecture,
! [X0] :
( ~ v1_xboole_0(X0)
=> ! [X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(X0))
=> ! [X3] :
( m2_relset_1(X3,X0,X1)
=> k10_relset_1(X0,X1,X3,X2) = k3_tarski(a_4_0_relset_2(X0,X1,X2,X3)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t17_relset_2) ).
fof(f71100,negated_conjecture,
~ ! [X0] :
( ~ v1_xboole_0(X0)
=> ! [X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(X0))
=> ! [X3] :
( m2_relset_1(X3,X0,X1)
=> k10_relset_1(X0,X1,X3,X2) = k3_tarski(a_4_0_relset_2(X0,X1,X2,X3)) ) ) ),
inference(negated_conjecture,[status(cth)],[f71099]) ).
fof(f71222,plain,
? [X0] :
( ? [X1,X2] :
( ? [X3] :
( k10_relset_1(X0,X1,X3,X2) != k3_tarski(a_4_0_relset_2(X0,X1,X2,X3))
& m2_relset_1(X3,X0,X1) )
& m1_subset_1(X2,k1_zfmisc_1(X0)) )
& ~ v1_xboole_0(X0) ),
inference(ennf_transformation,[],[f71100]) ).
fof(f71258,plain,
! [X0,X1,X2,X3] :
( k10_relset_1(X0,X1,X2,X3) = k9_relat_1(X2,X3)
| ~ m1_relset_1(X2,X0,X1) ),
inference(ennf_transformation,[],[f1508]) ).
fof(f71261,plain,
! [X0,X1,X2,X3,X4] :
( ( r2_hidden(X0,a_4_0_relset_2(X1,X2,X3,X4))
<=> ? [X5] :
( m1_subset_1(X5,X1)
& X0 = k2_relset_2(X1,X2,X4,X5)
& r2_hidden(X5,X3) ) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X3,k1_zfmisc_1(X1))
| ~ m2_relset_1(X4,X1,X2) ),
inference(ennf_transformation,[],[f71064]) ).
fof(f71262,plain,
! [X0,X1,X2,X3,X4] :
( ( r2_hidden(X0,a_4_0_relset_2(X1,X2,X3,X4))
<=> ? [X5] :
( m1_subset_1(X5,X1)
& X0 = k2_relset_2(X1,X2,X4,X5)
& r2_hidden(X5,X3) ) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X3,k1_zfmisc_1(X1))
| ~ m2_relset_1(X4,X1,X2) ),
inference(flattening,[],[f71261]) ).
fof(f71269,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(f71270,plain,
! [X0,X1,X2] :
( m1_subset_1(X0,X2)
| ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2)) ),
inference(flattening,[],[f71269]) ).
fof(f71389,plain,
! [X0,X1] :
( r1_tarski(X0,X1)
<=> ! [X2] :
( r2_hidden(X2,X1)
| ~ r2_hidden(X2,X0) ) ),
inference(ennf_transformation,[],[f8]) ).
fof(f72078,plain,
! [X0,X1,X2] :
( ( r2_hidden(X0,k9_relat_1(X2,k1_tarski(X1)))
<=> r2_hidden(k4_tarski(X1,X0),X2) )
| ~ v1_relat_1(X2) ),
inference(ennf_transformation,[],[f71090]) ).
fof(f72180,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(f72181,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(f72249,plain,
! [X0,X1,X2] :
( ! [X3] :
( k2_relset_2(X0,X1,X2,X3) = k10_relset_1(X0,X1,X2,k1_tarski(X3))
| ~ m1_subset_1(X3,X0) )
| ~ m2_relset_1(X2,X0,X1) ),
inference(ennf_transformation,[],[f71089]) ).
fof(f72300,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,[],[f1481]) ).
fof(f72301,plain,
! [X0,X1,X2] :
( v1_relat_1(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(ennf_transformation,[],[f1422]) ).
fof(f75302,plain,
( k10_relset_1(sK48,sK49,sK51,sK50) != k3_tarski(a_4_0_relset_2(sK48,sK49,sK50,sK51))
& m2_relset_1(sK51,sK48,sK49)
& m1_subset_1(sK50,k1_zfmisc_1(sK48))
& ~ v1_xboole_0(sK48) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK48,sK49,sK50,sK51]),skolemize(X0,sK48),skolemize(X1,sK49),skolemize(X2,sK50),skolemize(X3,sK51)],[f71222]) ).
fof(f75314,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(f75315,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,[],[f75314]) ).
fof(f75316,plain,
! [X0,X1] :
( ( X1 = k3_tarski(X0)
| ( ( ! [X3] :
( ~ r2_hidden(sK61(X0,X1),X3)
| ~ r2_hidden(X3,X0) )
| ~ r2_hidden(sK61(X0,X1),X1) )
& ( ( r2_hidden(sK61(X0,X1),sK62(X0,X1))
& r2_hidden(sK62(X0,X1),X0) )
| r2_hidden(sK61(X0,X1),X1) ) ) )
& ( ! [X5] :
( ( r2_hidden(X5,X1)
| ! [X6] :
( ~ r2_hidden(X5,X6)
| ~ r2_hidden(X6,X0) ) )
& ( ( r2_hidden(X5,sK63(X0,X5))
& r2_hidden(sK63(X0,X5),X0) )
| ~ r2_hidden(X5,X1) ) )
| k3_tarski(X0) != X1 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK61,sK62,sK63]),skolemize(X2,sK61(X0,X1)),skolemize(X4,sK62(X0,X1)),skolemize(X7,sK63(X0,X5))],[f75315]) ).
fof(f75330,plain,
! [X0,X1,X2,X3,X4] :
( ( ( r2_hidden(X0,a_4_0_relset_2(X1,X2,X3,X4))
| ! [X5] :
( ~ m1_subset_1(X5,X1)
| k2_relset_2(X1,X2,X4,X5) != X0
| ~ r2_hidden(X5,X3) ) )
& ( ? [X5] :
( m1_subset_1(X5,X1)
& X0 = k2_relset_2(X1,X2,X4,X5)
& r2_hidden(X5,X3) )
| ~ r2_hidden(X0,a_4_0_relset_2(X1,X2,X3,X4)) ) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X3,k1_zfmisc_1(X1))
| ~ m2_relset_1(X4,X1,X2) ),
inference(nnf_transformation,[],[f71262]) ).
fof(f75331,plain,
! [X0,X1,X2,X3,X4] :
( ( ( r2_hidden(X0,a_4_0_relset_2(X1,X2,X3,X4))
| ! [X5] :
( ~ m1_subset_1(X5,X1)
| k2_relset_2(X1,X2,X4,X5) != X0
| ~ r2_hidden(X5,X3) ) )
& ( ? [X6] :
( m1_subset_1(X6,X1)
& k2_relset_2(X1,X2,X4,X6) = X0
& r2_hidden(X6,X3) )
| ~ r2_hidden(X0,a_4_0_relset_2(X1,X2,X3,X4)) ) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X3,k1_zfmisc_1(X1))
| ~ m2_relset_1(X4,X1,X2) ),
inference(rectify,[],[f75330]) ).
fof(f75332,plain,
! [X0,X1,X2,X3,X4] :
( ( ( r2_hidden(X0,a_4_0_relset_2(X1,X2,X3,X4))
| ! [X5] :
( ~ m1_subset_1(X5,X1)
| k2_relset_2(X1,X2,X4,X5) != X0
| ~ r2_hidden(X5,X3) ) )
& ( ( m1_subset_1(sK73(X0,X1,X2,X3,X4),X1)
& k2_relset_2(X1,X2,X4,sK73(X0,X1,X2,X3,X4)) = X0
& r2_hidden(sK73(X0,X1,X2,X3,X4),X3) )
| ~ r2_hidden(X0,a_4_0_relset_2(X1,X2,X3,X4)) ) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X3,k1_zfmisc_1(X1))
| ~ m2_relset_1(X4,X1,X2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK73]),skolemize(X6,sK73(X0,X1,X2,X3,X4))],[f75331]) ).
fof(f75386,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(f75387,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,[],[f75386]) ).
fof(f75388,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,[],[f71389]) ).
fof(f75389,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,[],[f75388]) ).
fof(f75390,plain,
! [X0,X1] :
( ( r1_tarski(X0,X1)
| ( ~ r2_hidden(sK109(X0,X1),X1)
& r2_hidden(sK109(X0,X1),X0) ) )
& ( ! [X3] :
( r2_hidden(X3,X1)
| ~ r2_hidden(X3,X0) )
| ~ r1_tarski(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK109]),skolemize(X2,sK109(X0,X1))],[f75389]) ).
fof(f75633,plain,
! [X0,X1,X2] :
( ( ( r2_hidden(X0,k9_relat_1(X2,k1_tarski(X1)))
| ~ r2_hidden(k4_tarski(X1,X0),X2) )
& ( r2_hidden(k4_tarski(X1,X0),X2)
| ~ r2_hidden(X0,k9_relat_1(X2,k1_tarski(X1))) ) )
| ~ v1_relat_1(X2) ),
inference(nnf_transformation,[],[f72078]) ).
fof(f75655,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,[],[f72180]) ).
fof(f75656,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,[],[f75655]) ).
fof(f75657,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(sK269(X0,X1,X2),k1_relat_1(X2))
& r2_hidden(k4_tarski(sK269(X0,X1,X2),X0),X2)
& r2_hidden(sK269(X0,X1,X2),X1) )
| ~ r2_hidden(X0,k9_relat_1(X2,X1)) ) )
| ~ v1_relat_1(X2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK269]),skolemize(X4,sK269(X0,X1,X2))],[f75656]) ).
fof(f75658,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,[],[f72181]) ).
fof(f75659,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,[],[f75658]) ).
fof(f75660,plain,
! [X0] :
( ! [X1,X2] :
( ( X2 = k9_relat_1(X0,X1)
| ( ( ! [X4] :
( ~ r2_hidden(k4_tarski(X4,sK270(X0,X1,X2)),X0)
| ~ r2_hidden(X4,X1) )
| ~ r2_hidden(sK270(X0,X1,X2),X2) )
& ( ( r2_hidden(k4_tarski(sK271(X0,X1,X2),sK270(X0,X1,X2)),X0)
& r2_hidden(sK271(X0,X1,X2),X1) )
| r2_hidden(sK270(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(sK272(X0,X1,X6),X6),X0)
& r2_hidden(sK272(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,[sK270,sK271,sK272]),skolemize(X3,sK270(X0,X1,X2)),skolemize(X5,sK271(X0,X1,X2)),skolemize(X8,sK272(X0,X1,X6))],[f75659]) ).
fof(f75667,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,[],[f1483]) ).
fof(f76367,plain,
~ v1_xboole_0(sK48),
inference(cnf_transformation,[],[f75302]) ).
fof(f76368,plain,
m1_subset_1(sK50,k1_zfmisc_1(sK48)),
inference(cnf_transformation,[],[f75302]) ).
fof(f76369,plain,
m2_relset_1(sK51,sK48,sK49),
inference(cnf_transformation,[],[f75302]) ).
fof(f76370,plain,
k10_relset_1(sK48,sK49,sK51,sK50) != k3_tarski(a_4_0_relset_2(sK48,sK49,sK50,sK51)),
inference(cnf_transformation,[],[f75302]) ).
fof(f76413,plain,
! [X0,X1,X5] :
( r2_hidden(sK63(X0,X5),X0)
| ~ r2_hidden(X5,X1)
| k3_tarski(X0) != X1 ),
inference(cnf_transformation,[],[f75316]) ).
fof(f76414,plain,
! [X0,X1,X5] :
( r2_hidden(X5,sK63(X0,X5))
| ~ r2_hidden(X5,X1)
| k3_tarski(X0) != X1 ),
inference(cnf_transformation,[],[f75316]) ).
fof(f76415,plain,
! [X0,X1,X6,X5] :
( r2_hidden(X5,X1)
| ~ r2_hidden(X5,X6)
| ~ r2_hidden(X6,X0)
| k3_tarski(X0) != X1 ),
inference(cnf_transformation,[],[f75316]) ).
fof(f76448,plain,
! [X2,X3,X0,X1] :
( k10_relset_1(X0,X1,X2,X3) = k9_relat_1(X2,X3)
| ~ m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f71258]) ).
fof(f76454,plain,
! [X2,X3,X0,X1,X4] :
( r2_hidden(sK73(X0,X1,X2,X3,X4),X3)
| ~ r2_hidden(X0,a_4_0_relset_2(X1,X2,X3,X4))
| v1_xboole_0(X1)
| ~ m1_subset_1(X3,k1_zfmisc_1(X1))
| ~ m2_relset_1(X4,X1,X2) ),
inference(cnf_transformation,[],[f75332]) ).
fof(f76455,plain,
! [X2,X3,X0,X1,X4] :
( k2_relset_2(X1,X2,X4,sK73(X0,X1,X2,X3,X4)) = X0
| ~ r2_hidden(X0,a_4_0_relset_2(X1,X2,X3,X4))
| v1_xboole_0(X1)
| ~ m1_subset_1(X3,k1_zfmisc_1(X1))
| ~ m2_relset_1(X4,X1,X2) ),
inference(cnf_transformation,[],[f75332]) ).
fof(f76456,plain,
! [X2,X3,X0,X1,X4] :
( m1_subset_1(sK73(X0,X1,X2,X3,X4),X1)
| ~ r2_hidden(X0,a_4_0_relset_2(X1,X2,X3,X4))
| v1_xboole_0(X1)
| ~ m1_subset_1(X3,k1_zfmisc_1(X1))
| ~ m2_relset_1(X4,X1,X2) ),
inference(cnf_transformation,[],[f75332]) ).
fof(f76457,plain,
! [X2,X3,X0,X1,X4,X5] :
( r2_hidden(X0,a_4_0_relset_2(X1,X2,X3,X4))
| ~ m1_subset_1(X5,X1)
| k2_relset_2(X1,X2,X4,X5) != X0
| ~ r2_hidden(X5,X3)
| v1_xboole_0(X1)
| ~ m1_subset_1(X3,k1_zfmisc_1(X1))
| ~ m2_relset_1(X4,X1,X2) ),
inference(cnf_transformation,[],[f75332]) ).
fof(f76468,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ r2_hidden(X0,X1)
| m1_subset_1(X0,X2) ),
inference(cnf_transformation,[],[f71270]) ).
fof(f76659,plain,
! [X0,X1] :
( ~ r1_tarski(X1,X0)
| ~ r1_tarski(X0,X1)
| X0 = X1 ),
inference(cnf_transformation,[],[f75387]) ).
fof(f76662,plain,
! [X0,X1] :
( r2_hidden(sK109(X0,X1),X0)
| r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f75390]) ).
fof(f76663,plain,
! [X0,X1] :
( ~ r2_hidden(sK109(X0,X1),X1)
| r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f75390]) ).
fof(f77804,plain,
! [X2,X0,X1] :
( ~ r2_hidden(X0,k9_relat_1(X2,k1_tarski(X1)))
| r2_hidden(k4_tarski(X1,X0),X2)
| ~ v1_relat_1(X2) ),
inference(cnf_transformation,[],[f75633]) ).
fof(f77805,plain,
! [X2,X0,X1] :
( r2_hidden(X0,k9_relat_1(X2,k1_tarski(X1)))
| ~ r2_hidden(k4_tarski(X1,X0),X2)
| ~ v1_relat_1(X2) ),
inference(cnf_transformation,[],[f75633]) ).
fof(f77903,plain,
! [X2,X0,X1] :
( r2_hidden(sK269(X0,X1,X2),X1)
| ~ r2_hidden(X0,k9_relat_1(X2,X1))
| ~ v1_relat_1(X2) ),
inference(cnf_transformation,[],[f75657]) ).
fof(f77904,plain,
! [X2,X0,X1] :
( r2_hidden(k4_tarski(sK269(X0,X1,X2),X0),X2)
| ~ r2_hidden(X0,k9_relat_1(X2,X1))
| ~ v1_relat_1(X2) ),
inference(cnf_transformation,[],[f75657]) ).
fof(f77909,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,[],[f75660]) ).
fof(f77939,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f75667]) ).
fof(f78090,plain,
! [X2,X3,X0,X1] :
( k2_relset_2(X0,X1,X2,X3) = k10_relset_1(X0,X1,X2,k1_tarski(X3))
| ~ m1_subset_1(X3,X0)
| ~ m2_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f72249]) ).
fof(f78170,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,[],[f72300]) ).
fof(f78171,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| v1_relat_1(X2) ),
inference(cnf_transformation,[],[f72301]) ).
fof(f81555,plain,
! [X0,X6,X5] :
( r2_hidden(X5,k3_tarski(X0))
| ~ r2_hidden(X5,X6)
| ~ r2_hidden(X6,X0) ),
inference(equality_resolution,[],[f76415]) ).
fof(f81556,plain,
! [X0,X5] :
( r2_hidden(X5,sK63(X0,X5))
| ~ r2_hidden(X5,k3_tarski(X0)) ),
inference(equality_resolution,[],[f76414]) ).
fof(f81557,plain,
! [X0,X5] :
( r2_hidden(sK63(X0,X5),X0)
| ~ r2_hidden(X5,k3_tarski(X0)) ),
inference(equality_resolution,[],[f76413]) ).
fof(f81559,plain,
! [X2,X3,X1,X4,X5] :
( r2_hidden(k2_relset_2(X1,X2,X4,X5),a_4_0_relset_2(X1,X2,X3,X4))
| ~ m1_subset_1(X5,X1)
| ~ r2_hidden(X5,X3)
| v1_xboole_0(X1)
| ~ m1_subset_1(X3,k1_zfmisc_1(X1))
| ~ m2_relset_1(X4,X1,X2) ),
inference(equality_resolution,[],[f76457]) ).
fof(f81704,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,[],[f77909]) ).
fof(f82058,definition,
sF741 = k10_relset_1(sK48,sK49,sK51,sK50),
introduced(definition,[new_symbols(definition,[sF741])],[function_definition]) ).
fof(f82059,plain,
k10_relset_1(sK48,sK49,sK51,sK50) = sF741,
inference(reorient_equations,[],[f82058]) ).
fof(f82060,definition,
sF742 = a_4_0_relset_2(sK48,sK49,sK50,sK51),
introduced(definition,[new_symbols(definition,[sF742])],[function_definition]) ).
fof(f82061,plain,
a_4_0_relset_2(sK48,sK49,sK50,sK51) = sF742,
inference(reorient_equations,[],[f82060]) ).
fof(f82062,definition,
sF743 = k3_tarski(sF742),
introduced(definition,[new_symbols(definition,[sF743])],[function_definition]) ).
fof(f82063,plain,
k3_tarski(sF742) = sF743,
inference(reorient_equations,[],[f82062]) ).
fof(f82064,plain,
sF741 != sF743,
inference(definition_folding,[],[f76370,f82063,f82061,f82059]) ).
fof(f82065,definition,
sF744 = k1_zfmisc_1(sK48),
introduced(definition,[new_symbols(definition,[sF744])],[function_definition]) ).
fof(f82066,plain,
k1_zfmisc_1(sK48) = sF744,
inference(reorient_equations,[],[f82065]) ).
fof(f82067,plain,
m1_subset_1(sK50,sF744),
inference(definition_folding,[],[f76368,f82066]) ).
fof(f83822,definition,
( spl745_349
<=> v1_xboole_0(sK48) ),
introduced(definition,[new_symbols(definition,[spl745_349])],[avatar_definition]) ).
fof(f83824,plain,
( ~ v1_xboole_0(sK48)
| spl745_349 ),
inference(avatar_component_clause,[],[f83822]) ).
fof(f83825,plain,
~ spl745_349,
inference(avatar_split_clause,[],[f76367,f83822]) ).
fof(f83827,definition,
( spl745_350
<=> m1_subset_1(sK50,sF744) ),
introduced(definition,[new_symbols(definition,[spl745_350])],[avatar_definition]) ).
fof(f83829,plain,
( m1_subset_1(sK50,sF744)
| ~ spl745_350 ),
inference(avatar_component_clause,[],[f83827]) ).
fof(f83830,plain,
spl745_350,
inference(avatar_split_clause,[],[f82067,f83827]) ).
fof(f83832,definition,
( spl745_351
<=> m2_relset_1(sK51,sK48,sK49) ),
introduced(definition,[new_symbols(definition,[spl745_351])],[avatar_definition]) ).
fof(f83834,plain,
( m2_relset_1(sK51,sK48,sK49)
| ~ spl745_351 ),
inference(avatar_component_clause,[],[f83832]) ).
fof(f83835,plain,
spl745_351,
inference(avatar_split_clause,[],[f76369,f83832]) ).
fof(f83837,definition,
( spl745_352
<=> sF741 = sF743 ),
introduced(definition,[new_symbols(definition,[spl745_352])],[avatar_definition]) ).
fof(f83839,plain,
( sF741 != sF743
| spl745_352 ),
inference(avatar_component_clause,[],[f83837]) ).
fof(f83840,plain,
~ spl745_352,
inference(avatar_split_clause,[],[f82064,f83837]) ).
fof(f83847,definition,
( spl745_354
<=> k10_relset_1(sK48,sK49,sK51,sK50) = sF741 ),
introduced(definition,[new_symbols(definition,[spl745_354])],[avatar_definition]) ).
fof(f83849,plain,
( k10_relset_1(sK48,sK49,sK51,sK50) = sF741
| ~ spl745_354 ),
inference(avatar_component_clause,[],[f83847]) ).
fof(f83850,plain,
spl745_354,
inference(avatar_split_clause,[],[f82059,f83847]) ).
fof(f83852,definition,
( spl745_355
<=> a_4_0_relset_2(sK48,sK49,sK50,sK51) = sF742 ),
introduced(definition,[new_symbols(definition,[spl745_355])],[avatar_definition]) ).
fof(f83854,plain,
( a_4_0_relset_2(sK48,sK49,sK50,sK51) = sF742
| ~ spl745_355 ),
inference(avatar_component_clause,[],[f83852]) ).
fof(f83855,plain,
spl745_355,
inference(avatar_split_clause,[],[f82061,f83852]) ).
fof(f83857,definition,
( spl745_356
<=> k3_tarski(sF742) = sF743 ),
introduced(definition,[new_symbols(definition,[spl745_356])],[avatar_definition]) ).
fof(f83859,plain,
( k3_tarski(sF742) = sF743
| ~ spl745_356 ),
inference(avatar_component_clause,[],[f83857]) ).
fof(f83860,plain,
spl745_356,
inference(avatar_split_clause,[],[f82063,f83857]) ).
fof(f83862,definition,
( spl745_357
<=> k1_zfmisc_1(sK48) = sF744 ),
introduced(definition,[new_symbols(definition,[spl745_357])],[avatar_definition]) ).
fof(f83864,plain,
( k1_zfmisc_1(sK48) = sF744
| ~ spl745_357 ),
inference(avatar_component_clause,[],[f83862]) ).
fof(f83865,plain,
spl745_357,
inference(avatar_split_clause,[],[f82066,f83862]) ).
fof(f83870,definition,
( spl745_358
<=> m1_relset_1(sK51,sK48,sK49) ),
introduced(definition,[new_symbols(definition,[spl745_358])],[avatar_definition]) ).
fof(f83878,plain,
( sF741 = k9_relat_1(sK51,sK50)
| ~ m1_relset_1(sK51,sK48,sK49)
| ~ spl745_354 ),
inference(superposition,[],[f76448,f83849]) ).
fof(f83883,definition,
( spl745_360
<=> sF741 = k9_relat_1(sK51,sK50) ),
introduced(definition,[new_symbols(definition,[spl745_360])],[avatar_definition]) ).
fof(f83885,plain,
( sF741 = k9_relat_1(sK51,sK50)
| ~ spl745_360 ),
inference(avatar_component_clause,[],[f83883]) ).
fof(f83887,plain,
( ~ spl745_358
| spl745_360
| ~ spl745_354 ),
inference(avatar_split_clause,[],[f83878,f83847,f83883,f83870]) ).
fof(f83890,plain,
( ! [X0] :
( r2_hidden(k2_relset_2(sK48,sK49,sK51,X0),sF742)
| ~ m1_subset_1(X0,sK48)
| ~ r2_hidden(X0,sK50)
| v1_xboole_0(sK48)
| ~ m1_subset_1(sK50,k1_zfmisc_1(sK48))
| ~ m2_relset_1(sK51,sK48,sK49) )
| ~ spl745_355 ),
inference(superposition,[],[f81559,f83854]) ).
fof(f83892,plain,
( ! [X0] :
( r2_hidden(k2_relset_2(sK48,sK49,sK51,X0),sF742)
| ~ m1_subset_1(X0,sK48)
| ~ r2_hidden(X0,sK50)
| ~ m1_subset_1(sK50,k1_zfmisc_1(sK48))
| ~ m2_relset_1(sK51,sK48,sK49) )
| spl745_349
| ~ spl745_355 ),
inference(forward_subsumption_resolution,[],[f83890,f83824]) ).
fof(f83893,plain,
( ! [X0] :
( r2_hidden(k2_relset_2(sK48,sK49,sK51,X0),sF742)
| ~ m1_subset_1(X0,sK48)
| ~ r2_hidden(X0,sK50)
| ~ m1_subset_1(sK50,k1_zfmisc_1(sK48)) )
| spl745_349
| ~ spl745_351
| ~ spl745_355 ),
inference(forward_subsumption_resolution,[],[f83892,f83834]) ).
fof(f83894,plain,
( ! [X0] :
( ~ m1_subset_1(sK50,sF744)
| r2_hidden(k2_relset_2(sK48,sK49,sK51,X0),sF742)
| ~ m1_subset_1(X0,sK48)
| ~ r2_hidden(X0,sK50) )
| spl745_349
| ~ spl745_351
| ~ spl745_355
| ~ spl745_357 ),
inference(forward_demodulation,[],[f83893,f83864]) ).
fof(f83895,plain,
( ! [X0] :
( r2_hidden(k2_relset_2(sK48,sK49,sK51,X0),sF742)
| ~ m1_subset_1(X0,sK48)
| ~ r2_hidden(X0,sK50) )
| spl745_349
| ~ spl745_350
| ~ spl745_351
| ~ spl745_355
| ~ spl745_357 ),
inference(forward_subsumption_resolution,[],[f83894,f83829]) ).
fof(f83900,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X0,X1,X2)
| v1_relat_1(X0) ),
inference(resolution,[],[f78170,f78171]) ).
fof(f83901,plain,
( v1_relat_1(sK51)
| ~ spl745_351 ),
inference(resolution,[],[f83900,f83834]) ).
fof(f83903,definition,
( spl745_361
<=> v1_relat_1(sK51) ),
introduced(definition,[new_symbols(definition,[spl745_361])],[avatar_definition]) ).
fof(f83905,plain,
( v1_relat_1(sK51)
| ~ spl745_361 ),
inference(avatar_component_clause,[],[f83903]) ).
fof(f83906,plain,
( spl745_361
| ~ spl745_351 ),
inference(avatar_split_clause,[],[f83901,f83832,f83903]) ).
fof(f83907,plain,
( m1_relset_1(sK51,sK48,sK49)
| ~ spl745_351 ),
inference(resolution,[],[f77939,f83834]) ).
fof(f83908,plain,
( spl745_358
| ~ spl745_351 ),
inference(avatar_split_clause,[],[f83907,f83832,f83870]) ).
fof(f83917,plain,
! [X2,X3,X0,X1] :
( k9_relat_1(X0,k1_tarski(X1)) = k2_relset_2(X2,X3,X0,X1)
| ~ m1_subset_1(X1,X2)
| ~ m2_relset_1(X0,X2,X3)
| ~ m1_relset_1(X0,X2,X3) ),
inference(superposition,[],[f78090,f76448]) ).
fof(f83922,plain,
! [X2,X3,X0,X1] :
( k9_relat_1(X0,k1_tarski(X1)) = k2_relset_2(X2,X3,X0,X1)
| ~ m1_subset_1(X1,X2)
| ~ m2_relset_1(X0,X2,X3) ),
inference(forward_subsumption_resolution,[],[f83917,f77939]) ).
fof(f83924,plain,
! [X2,X3,X0,X1,X4] :
( k9_relat_1(X0,k1_tarski(sK73(X1,X2,X3,X4,X0))) = X1
| ~ r2_hidden(X1,a_4_0_relset_2(X2,X3,X4,X0))
| v1_xboole_0(X2)
| ~ m1_subset_1(X4,k1_zfmisc_1(X2))
| ~ m2_relset_1(X0,X2,X3)
| ~ m1_subset_1(sK73(X1,X2,X3,X4,X0),X2)
| ~ m2_relset_1(X0,X2,X3) ),
inference(superposition,[],[f76455,f83922]) ).
fof(f83929,plain,
! [X2,X3,X0,X1,X4] :
( k9_relat_1(X0,k1_tarski(sK73(X1,X2,X3,X4,X0))) = X1
| ~ r2_hidden(X1,a_4_0_relset_2(X2,X3,X4,X0))
| v1_xboole_0(X2)
| ~ m1_subset_1(X4,k1_zfmisc_1(X2))
| ~ m2_relset_1(X0,X2,X3)
| ~ m1_subset_1(sK73(X1,X2,X3,X4,X0),X2) ),
inference(duplicate_literal_removal,[],[f83924]) ).
fof(f83980,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,sF744)
| ~ r2_hidden(X1,X0)
| m1_subset_1(X1,sK48) )
| ~ spl745_357 ),
inference(superposition,[],[f76468,f83864]) ).
fof(f83981,plain,
( ! [X0] :
( ~ r2_hidden(X0,sK50)
| m1_subset_1(X0,sK48) )
| ~ spl745_350
| ~ spl745_357 ),
inference(resolution,[],[f83980,f83829]) ).
fof(f83997,plain,
( ! [X0,X1] :
( ~ r2_hidden(X1,sF742)
| ~ r2_hidden(X0,X1)
| r2_hidden(X0,sF743) )
| ~ spl745_356 ),
inference(superposition,[],[f81555,f83859]) ).
fof(f83999,plain,
( ! [X0,X1] :
( ~ r2_hidden(X0,k2_relset_2(sK48,sK49,sK51,X1))
| r2_hidden(X0,sF743)
| ~ m1_subset_1(X1,sK48)
| ~ r2_hidden(X1,sK50) )
| spl745_349
| ~ spl745_350
| ~ spl745_351
| ~ spl745_355
| ~ spl745_356
| ~ spl745_357 ),
inference(resolution,[],[f83997,f83895]) ).
fof(f84006,plain,
( ! [X0,X1] :
( ~ r2_hidden(X0,k2_relset_2(sK48,sK49,sK51,X1))
| r2_hidden(X0,sF743)
| ~ r2_hidden(X1,sK50) )
| spl745_349
| ~ spl745_350
| ~ spl745_351
| ~ spl745_355
| ~ spl745_356
| ~ spl745_357 ),
inference(forward_subsumption_resolution,[],[f83999,f83981]) ).
fof(f84012,plain,
( ! [X0,X1] :
( ~ r2_hidden(X1,k9_relat_1(sK51,k1_tarski(X0)))
| r2_hidden(X1,sF743)
| ~ r2_hidden(X0,sK50)
| ~ m1_subset_1(X0,sK48)
| ~ m2_relset_1(sK51,sK48,sK49) )
| spl745_349
| ~ spl745_350
| ~ spl745_351
| ~ spl745_355
| ~ spl745_356
| ~ spl745_357 ),
inference(superposition,[],[f84006,f83922]) ).
fof(f84013,plain,
( ! [X0,X1] :
( ~ r2_hidden(X1,k9_relat_1(sK51,k1_tarski(X0)))
| r2_hidden(X1,sF743)
| ~ r2_hidden(X0,sK50)
| ~ m1_subset_1(X0,sK48) )
| spl745_349
| ~ spl745_350
| ~ spl745_351
| ~ spl745_355
| ~ spl745_356
| ~ spl745_357 ),
inference(forward_subsumption_resolution,[],[f84012,f83834]) ).
fof(f84015,plain,
( ! [X0,X1] :
( ~ r2_hidden(X1,k9_relat_1(sK51,k1_tarski(X0)))
| r2_hidden(X1,sF743)
| ~ r2_hidden(X0,sK50) )
| spl745_349
| ~ spl745_350
| ~ spl745_351
| ~ spl745_355
| ~ spl745_356
| ~ spl745_357 ),
inference(forward_subsumption_resolution,[],[f84013,f83981]) ).
fof(f84044,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ r2_hidden(X1,X0)
| r2_hidden(k4_tarski(sK73(X0,X3,X4,X5,X2),X1),X2)
| ~ v1_relat_1(X2)
| ~ r2_hidden(X0,a_4_0_relset_2(X3,X4,X5,X2))
| v1_xboole_0(X3)
| ~ m1_subset_1(X5,k1_zfmisc_1(X3))
| ~ m2_relset_1(X2,X3,X4)
| ~ m1_subset_1(sK73(X0,X3,X4,X5,X2),X3) ),
inference(superposition,[],[f77804,f83929]) ).
fof(f84045,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ r2_hidden(X1,X0)
| r2_hidden(k4_tarski(sK73(X0,X3,X4,X5,X2),X1),X2)
| ~ v1_relat_1(X2)
| ~ r2_hidden(X0,a_4_0_relset_2(X3,X4,X5,X2))
| v1_xboole_0(X3)
| ~ m1_subset_1(X5,k1_zfmisc_1(X3))
| ~ m2_relset_1(X2,X3,X4) ),
inference(forward_subsumption_resolution,[],[f84044,f76456]) ).
fof(f84046,plain,
! [X2,X3,X0,X1,X4,X5] :
( r2_hidden(k4_tarski(sK73(X0,X3,X4,X5,X2),X1),X2)
| ~ r2_hidden(X1,X0)
| ~ r2_hidden(X0,a_4_0_relset_2(X3,X4,X5,X2))
| v1_xboole_0(X3)
| ~ m1_subset_1(X5,k1_zfmisc_1(X3))
| ~ m2_relset_1(X2,X3,X4) ),
inference(forward_subsumption_resolution,[],[f84045,f83900]) ).
fof(f84466,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ r2_hidden(X0,X1)
| ~ r2_hidden(X1,a_4_0_relset_2(X2,X3,X4,X5))
| v1_xboole_0(X2)
| ~ m1_subset_1(X4,k1_zfmisc_1(X2))
| ~ m2_relset_1(X5,X2,X3)
| r2_hidden(X0,k9_relat_1(X5,X6))
| ~ r2_hidden(sK73(X1,X2,X3,X4,X5),X6)
| ~ v1_relat_1(X5) ),
inference(resolution,[],[f84046,f81704]) ).
fof(f84483,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ r2_hidden(sK73(X1,X2,X3,X4,X5),X6)
| ~ r2_hidden(X1,a_4_0_relset_2(X2,X3,X4,X5))
| v1_xboole_0(X2)
| ~ m1_subset_1(X4,k1_zfmisc_1(X2))
| ~ m2_relset_1(X5,X2,X3)
| r2_hidden(X0,k9_relat_1(X5,X6))
| ~ r2_hidden(X0,X1) ),
inference(forward_subsumption_resolution,[],[f84466,f83900]) ).
fof(f84484,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ r2_hidden(X0,a_4_0_relset_2(X1,X2,X3,X4))
| v1_xboole_0(X1)
| ~ m1_subset_1(X3,k1_zfmisc_1(X1))
| ~ m2_relset_1(X4,X1,X2)
| r2_hidden(X5,k9_relat_1(X4,X3))
| ~ r2_hidden(X5,X0)
| ~ r2_hidden(X0,a_4_0_relset_2(X1,X2,X3,X4))
| v1_xboole_0(X1)
| ~ m1_subset_1(X3,k1_zfmisc_1(X1))
| ~ m2_relset_1(X4,X1,X2) ),
inference(resolution,[],[f84483,f76454]) ).
fof(f84488,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ r2_hidden(X0,a_4_0_relset_2(X1,X2,X3,X4))
| v1_xboole_0(X1)
| ~ m1_subset_1(X3,k1_zfmisc_1(X1))
| ~ m2_relset_1(X4,X1,X2)
| r2_hidden(X5,k9_relat_1(X4,X3))
| ~ r2_hidden(X5,X0) ),
inference(duplicate_literal_removal,[],[f84484]) ).
fof(f84501,plain,
( ! [X0,X1] :
( ~ r2_hidden(X0,sF742)
| v1_xboole_0(sK48)
| ~ m1_subset_1(sK50,k1_zfmisc_1(sK48))
| ~ m2_relset_1(sK51,sK48,sK49)
| r2_hidden(X1,k9_relat_1(sK51,sK50))
| ~ r2_hidden(X1,X0) )
| ~ spl745_355 ),
inference(superposition,[],[f84488,f83854]) ).
fof(f84503,plain,
( ! [X0,X1] :
( ~ r2_hidden(X0,sF742)
| ~ m1_subset_1(sK50,k1_zfmisc_1(sK48))
| ~ m2_relset_1(sK51,sK48,sK49)
| r2_hidden(X1,k9_relat_1(sK51,sK50))
| ~ r2_hidden(X1,X0) )
| spl745_349
| ~ spl745_355 ),
inference(forward_subsumption_resolution,[],[f84501,f83824]) ).
fof(f84505,plain,
( ! [X0,X1] :
( ~ r2_hidden(X0,sF742)
| ~ m1_subset_1(sK50,k1_zfmisc_1(sK48))
| r2_hidden(X1,k9_relat_1(sK51,sK50))
| ~ r2_hidden(X1,X0) )
| spl745_349
| ~ spl745_351
| ~ spl745_355 ),
inference(forward_subsumption_resolution,[],[f84503,f83834]) ).
fof(f84506,plain,
( ! [X0,X1] :
( ~ m1_subset_1(sK50,sF744)
| ~ r2_hidden(X0,sF742)
| r2_hidden(X1,k9_relat_1(sK51,sK50))
| ~ r2_hidden(X1,X0) )
| spl745_349
| ~ spl745_351
| ~ spl745_355
| ~ spl745_357 ),
inference(forward_demodulation,[],[f84505,f83864]) ).
fof(f84507,plain,
( ! [X0,X1] :
( ~ r2_hidden(X0,sF742)
| r2_hidden(X1,k9_relat_1(sK51,sK50))
| ~ r2_hidden(X1,X0) )
| spl745_349
| ~ spl745_350
| ~ spl745_351
| ~ spl745_355
| ~ spl745_357 ),
inference(forward_subsumption_resolution,[],[f84506,f83829]) ).
fof(f84508,plain,
( ! [X0,X1] :
( ~ r2_hidden(X1,X0)
| ~ r2_hidden(X0,sF742)
| r2_hidden(X1,sF741) )
| spl745_349
| ~ spl745_350
| ~ spl745_351
| ~ spl745_355
| ~ spl745_357
| ~ spl745_360 ),
inference(forward_demodulation,[],[f84507,f83885]) ).
fof(f84509,plain,
( ! [X0,X1] :
( ~ r2_hidden(sK63(X0,X1),sF742)
| r2_hidden(X1,sF741)
| ~ r2_hidden(X1,k3_tarski(X0)) )
| spl745_349
| ~ spl745_350
| ~ spl745_351
| ~ spl745_355
| ~ spl745_357
| ~ spl745_360 ),
inference(resolution,[],[f84508,f81556]) ).
fof(f84542,plain,
( ! [X0] :
( r2_hidden(X0,sF741)
| ~ r2_hidden(X0,k3_tarski(sF742))
| ~ r2_hidden(X0,k3_tarski(sF742)) )
| spl745_349
| ~ spl745_350
| ~ spl745_351
| ~ spl745_355
| ~ spl745_357
| ~ spl745_360 ),
inference(resolution,[],[f84509,f81557]) ).
fof(f84543,plain,
( ! [X0] :
( r2_hidden(X0,sF741)
| ~ r2_hidden(X0,k3_tarski(sF742)) )
| spl745_349
| ~ spl745_350
| ~ spl745_351
| ~ spl745_355
| ~ spl745_357
| ~ spl745_360 ),
inference(duplicate_literal_removal,[],[f84542]) ).
fof(f84544,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF743)
| r2_hidden(X0,sF741) )
| spl745_349
| ~ spl745_350
| ~ spl745_351
| ~ spl745_355
| ~ spl745_356
| ~ spl745_357
| ~ spl745_360 ),
inference(forward_demodulation,[],[f84543,f83859]) ).
fof(f84553,plain,
( ! [X0] :
( r2_hidden(sK109(sF743,X0),sF741)
| r1_tarski(sF743,X0) )
| spl745_349
| ~ spl745_350
| ~ spl745_351
| ~ spl745_355
| ~ spl745_356
| ~ spl745_357
| ~ spl745_360 ),
inference(resolution,[],[f84544,f76662]) ).
fof(f84585,plain,
( r1_tarski(sF743,sF741)
| r1_tarski(sF743,sF741)
| spl745_349
| ~ spl745_350
| ~ spl745_351
| ~ spl745_355
| ~ spl745_356
| ~ spl745_357
| ~ spl745_360 ),
inference(resolution,[],[f84553,f76663]) ).
fof(f84589,plain,
( r1_tarski(sF743,sF741)
| spl745_349
| ~ spl745_350
| ~ spl745_351
| ~ spl745_355
| ~ spl745_356
| ~ spl745_357
| ~ spl745_360 ),
inference(duplicate_literal_removal,[],[f84585]) ).
fof(f84591,definition,
( spl745_409
<=> r1_tarski(sF743,sF741) ),
introduced(definition,[new_symbols(definition,[spl745_409])],[avatar_definition]) ).
fof(f84593,plain,
( r1_tarski(sF743,sF741)
| ~ spl745_409 ),
inference(avatar_component_clause,[],[f84591]) ).
fof(f84594,plain,
( spl745_409
| spl745_349
| ~ spl745_350
| ~ spl745_351
| ~ spl745_355
| ~ spl745_356
| ~ spl745_357
| ~ spl745_360 ),
inference(avatar_split_clause,[],[f84589,f83883,f83862,f83857,f83852,f83832,f83827,f83822,f84591]) ).
fof(f84597,plain,
( ~ r1_tarski(sF741,sF743)
| sF741 = sF743
| ~ spl745_409 ),
inference(resolution,[],[f84593,f76659]) ).
fof(f84598,plain,
( ~ r1_tarski(sF741,sF743)
| spl745_352
| ~ spl745_409 ),
inference(forward_subsumption_resolution,[],[f84597,f83839]) ).
fof(f84600,definition,
( spl745_410
<=> r1_tarski(sF741,sF743) ),
introduced(definition,[new_symbols(definition,[spl745_410])],[avatar_definition]) ).
fof(f84602,plain,
( ~ r1_tarski(sF741,sF743)
| spl745_410 ),
inference(avatar_component_clause,[],[f84600]) ).
fof(f84603,plain,
( ~ spl745_410
| spl745_352
| ~ spl745_409 ),
inference(avatar_split_clause,[],[f84598,f84591,f83837,f84600]) ).
fof(f85370,plain,
( ! [X0,X1] :
( ~ r2_hidden(k4_tarski(X0,X1),sK51)
| ~ v1_relat_1(sK51)
| r2_hidden(X1,sF743)
| ~ r2_hidden(X0,sK50) )
| spl745_349
| ~ spl745_350
| ~ spl745_351
| ~ spl745_355
| ~ spl745_356
| ~ spl745_357 ),
inference(resolution,[],[f77805,f84015]) ).
fof(f86117,plain,
( ! [X0,X1] :
( ~ r2_hidden(k4_tarski(X0,X1),sK51)
| r2_hidden(X1,sF743)
| ~ r2_hidden(X0,sK50) )
| spl745_349
| ~ spl745_350
| ~ spl745_351
| ~ spl745_355
| ~ spl745_356
| ~ spl745_357
| ~ spl745_361 ),
inference(forward_subsumption_resolution,[],[f85370,f83905]) ).
fof(f86128,plain,
( ! [X0,X1] :
( r2_hidden(X0,sF743)
| ~ r2_hidden(sK269(X0,X1,sK51),sK50)
| ~ r2_hidden(X0,k9_relat_1(sK51,X1))
| ~ v1_relat_1(sK51) )
| spl745_349
| ~ spl745_350
| ~ spl745_351
| ~ spl745_355
| ~ spl745_356
| ~ spl745_357
| ~ spl745_361 ),
inference(resolution,[],[f86117,f77904]) ).
fof(f86130,plain,
( ! [X0,X1] :
( ~ r2_hidden(sK269(X0,X1,sK51),sK50)
| r2_hidden(X0,sF743)
| ~ r2_hidden(X0,k9_relat_1(sK51,X1)) )
| spl745_349
| ~ spl745_350
| ~ spl745_351
| ~ spl745_355
| ~ spl745_356
| ~ spl745_357
| ~ spl745_361 ),
inference(forward_subsumption_resolution,[],[f86128,f83905]) ).
fof(f86137,plain,
( ! [X0] :
( r2_hidden(X0,sF743)
| ~ r2_hidden(X0,k9_relat_1(sK51,sK50))
| ~ r2_hidden(X0,k9_relat_1(sK51,sK50))
| ~ v1_relat_1(sK51) )
| spl745_349
| ~ spl745_350
| ~ spl745_351
| ~ spl745_355
| ~ spl745_356
| ~ spl745_357
| ~ spl745_361 ),
inference(resolution,[],[f86130,f77903]) ).
fof(f86138,plain,
( ! [X0] :
( r2_hidden(X0,sF743)
| ~ r2_hidden(X0,k9_relat_1(sK51,sK50))
| ~ v1_relat_1(sK51) )
| spl745_349
| ~ spl745_350
| ~ spl745_351
| ~ spl745_355
| ~ spl745_356
| ~ spl745_357
| ~ spl745_361 ),
inference(duplicate_literal_removal,[],[f86137]) ).
fof(f86139,plain,
( ! [X0] :
( r2_hidden(X0,sF743)
| ~ r2_hidden(X0,k9_relat_1(sK51,sK50)) )
| spl745_349
| ~ spl745_350
| ~ spl745_351
| ~ spl745_355
| ~ spl745_356
| ~ spl745_357
| ~ spl745_361 ),
inference(forward_subsumption_resolution,[],[f86138,f83905]) ).
fof(f86140,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF741)
| r2_hidden(X0,sF743) )
| spl745_349
| ~ spl745_350
| ~ spl745_351
| ~ spl745_355
| ~ spl745_356
| ~ spl745_357
| ~ spl745_360
| ~ spl745_361 ),
inference(forward_demodulation,[],[f86139,f83885]) ).
fof(f86162,plain,
( ! [X0] :
( r2_hidden(sK109(sF741,X0),sF743)
| r1_tarski(sF741,X0) )
| spl745_349
| ~ spl745_350
| ~ spl745_351
| ~ spl745_355
| ~ spl745_356
| ~ spl745_357
| ~ spl745_360
| ~ spl745_361 ),
inference(resolution,[],[f86140,f76662]) ).
fof(f86208,plain,
( r1_tarski(sF741,sF743)
| r1_tarski(sF741,sF743)
| spl745_349
| ~ spl745_350
| ~ spl745_351
| ~ spl745_355
| ~ spl745_356
| ~ spl745_357
| ~ spl745_360
| ~ spl745_361 ),
inference(resolution,[],[f86162,f76663]) ).
fof(f86213,plain,
( r1_tarski(sF741,sF743)
| spl745_349
| ~ spl745_350
| ~ spl745_351
| ~ spl745_355
| ~ spl745_356
| ~ spl745_357
| ~ spl745_360
| ~ spl745_361 ),
inference(duplicate_literal_removal,[],[f86208]) ).
fof(f86215,plain,
( $false
| spl745_349
| ~ spl745_350
| ~ spl745_351
| ~ spl745_355
| ~ spl745_356
| ~ spl745_357
| ~ spl745_360
| ~ spl745_361
| spl745_410 ),
inference(forward_subsumption_resolution,[],[f86213,f84602]) ).
fof(f86216,plain,
( spl745_349
| ~ spl745_350
| ~ spl745_351
| ~ spl745_355
| ~ spl745_356
| ~ spl745_357
| ~ spl745_360
| ~ spl745_361
| spl745_410 ),
inference(avatar_contradiction_clause,[],[f86215]) ).
cnf(s359,plain,
~ spl745_349,
inference(sat_conversion,[],[f83825]) ).
cnf(s360,plain,
spl745_350,
inference(sat_conversion,[],[f83830]) ).
cnf(s361,plain,
spl745_351,
inference(sat_conversion,[],[f83835]) ).
cnf(s362,plain,
~ spl745_352,
inference(sat_conversion,[],[f83840]) ).
cnf(s364,plain,
spl745_354,
inference(sat_conversion,[],[f83850]) ).
cnf(s365,plain,
spl745_355,
inference(sat_conversion,[],[f83855]) ).
cnf(s366,plain,
spl745_356,
inference(sat_conversion,[],[f83860]) ).
cnf(s367,plain,
spl745_357,
inference(sat_conversion,[],[f83865]) ).
cnf(s371,plain,
( ~ spl745_354
| ~ spl745_358
| spl745_360 ),
inference(sat_conversion,[],[f83887]) ).
cnf(s372,plain,
( ~ spl745_351
| spl745_361 ),
inference(sat_conversion,[],[f83906]) ).
cnf(s373,plain,
( ~ spl745_351
| spl745_358 ),
inference(sat_conversion,[],[f83908]) ).
cnf(s403,plain,
( spl745_349
| ~ spl745_350
| ~ spl745_351
| ~ spl745_355
| ~ spl745_356
| ~ spl745_357
| ~ spl745_360
| spl745_409 ),
inference(sat_conversion,[],[f84594]) ).
cnf(s404,plain,
( spl745_352
| ~ spl745_409
| ~ spl745_410 ),
inference(sat_conversion,[],[f84603]) ).
cnf(s529,plain,
( spl745_349
| ~ spl745_350
| ~ spl745_351
| ~ spl745_355
| ~ spl745_356
| ~ spl745_357
| ~ spl745_360
| ~ spl745_361
| spl745_410 ),
inference(sat_conversion,[],[f86216]) ).
cnf(s534,plain,
spl745_358,
inference(rat,[],[s373,s361]) ).
cnf(s535,plain,
spl745_361,
inference(rat,[],[s372,s361]) ).
cnf(s536,plain,
spl745_360,
inference(rat,[],[s371,s364,s534]) ).
cnf(s557,plain,
spl745_410,
inference(rat,[],[s529,s360,s535,s536,s367,s366,s365,s361,s359]) ).
cnf(s559,plain,
spl745_409,
inference(rat,[],[s403,s360,s536,s367,s366,s365,s361,s359]) ).
cnf(s560,plain,
$false,
inference(rat,[],[s404,s362,s557,s559]) ).
fof(f86217,plain,
$false,
inference(avatar_sat_refutation,[],[s560]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU423+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.43 % Computer : n015.cluster.edu
% 0.12/0.43 % Model : x86_64 x86_64
% 0.12/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.43 % Memory : 8046.5625MB
% 0.12/0.43 % OS : Linux 6.8.0-71-generic
% 0.12/0.43 % CPULimit : 300
% 0.12/0.43 % WCLimit : 300
% 0.12/0.43 % DateTime : Mon Sep 28 05:23:39 UTC 2026
% 0.12/0.43 % CPUTime :
% 0.12/0.43 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.17/0.46 Running first-order theorem proving
% 0.17/0.46 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 18.97/8.33 % (2295277)Detected formulas, will run a generic FOF schedule.
% 18.97/8.33 % (2295326)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2710061399:i=119:av=off:ss=axioms_2944 on theBenchmark for (2944ds/119Mi)
% 18.97/8.33 % (2295318)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=3040364031:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2944 on theBenchmark for (2944ds/134677Mi)
% 18.97/8.33 % (2295316)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=3161737710:i=141193_2944 on theBenchmark for (2944ds/141193Mi)
% 18.97/8.33 % (2295319)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=1133346493:i=141695:sd=1:nm=32:gsp=on:ss=included_2944 on theBenchmark for (2944ds/141695Mi)
% 18.97/8.33 % (2295322)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1775154137:i=109:sd=1:ins=1:gsp=on:ss=axioms_2944 on theBenchmark for (2944ds/109Mi)
% 18.97/8.33 % (2295326)Instruction limit reached!
% 18.97/8.33 % (2295326)------------------------------
% 18.97/8.33 % (2295326)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.97/8.33 % (2295326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.97/8.33 % (2295326)CaDiCaL version: 2.1.3
% 18.97/8.33 % (2295326)Termination reason: Instruction limit
% 18.97/8.33 % (2295326)Termination phase: SInE selection
% 18.97/8.33 % (2295326)Time elapsed: 0.054 s
% 18.97/8.33 % (2295326)Peak memory usage: 201 MB
% 18.97/8.33 % (2295326)Instructions burned: 119 (million)
% 18.97/8.33 % (2295327)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1634014282:s2a=on:i=139:gtg=position_2944 on theBenchmark for (2944ds/139Mi)
% 18.97/8.33 % (2295328)dis-21_1_sil=8000:lcm=predicate:random_seed=535021200:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2944 on theBenchmark for (2944ds/129Mi)
% 18.97/8.33 % (2295322)Instruction limit reached!
% 18.97/8.33 % (2295322)------------------------------
% 18.97/8.33 % (2295322)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.97/8.33 % (2295322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.97/8.33 % (2295322)CaDiCaL version: 2.1.3
% 18.97/8.33 % (2295322)Termination reason: Instruction limit
% 18.97/8.33 % (2295322)Termination phase: SInE selection
% 18.97/8.33 % (2295322)Time elapsed: 0.084 s
% 18.97/8.33 % (2295322)Peak memory usage: 201 MB
% 18.97/8.33 % (2295322)Instructions burned: 109 (million)
% 18.97/8.33 % (2295327)Instruction limit reached!
% 18.97/8.33 % (2295327)------------------------------
% 18.97/8.33 % (2295327)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.97/8.33 % (2295327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.97/8.33 % (2295327)CaDiCaL version: 2.1.3
% 18.97/8.33 % (2295327)Termination reason: Instruction limit
% 18.97/8.33 % (2295327)Termination phase: Property scanning
% 18.97/8.33 % (2295327)Time elapsed: 0.067 s
% 18.97/8.33 % (2295327)Peak memory usage: 201 MB
% 18.97/8.33 % (2295327)Instructions burned: 140 (million)
% 18.97/8.33 % (2295328)Instruction limit reached!
% 18.97/8.33 % (2295328)------------------------------
% 18.97/8.33 % (2295328)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.97/8.33 % (2295328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.97/8.33 % (2295328)CaDiCaL version: 2.1.3
% 18.97/8.33 % (2295328)Termination reason: Instruction limit
% 18.97/8.33 % (2295328)Termination phase: SInE selection
% 18.97/8.33 % (2295328)Time elapsed: 0.100 s
% 18.97/8.33 % (2295328)Peak memory usage: 201 MB
% 18.97/8.33 % (2295328)Instructions burned: 129 (million)
% 18.97/8.33 % (2295337)lrs+10_1_sil=8000:sp=occurrence:random_seed=298739145:i=285:sd=3:ss=axioms:sgt=8_2942 on theBenchmark for (2942ds/285Mi)
% 18.97/8.33 % (2295343)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1902360587:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2942 on theBenchmark for (2942ds/157Mi)
% 18.97/8.33 % (2295344)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3533502362:i=325:sd=1:ss=axioms:sgt=32_2942 on theBenchmark for (2942ds/325Mi)
% 18.97/8.33 % (2295337)Instruction limit reached!
% 18.97/8.33 % (2295337)------------------------------
% 18.97/8.33 % (2295337)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.97/8.33 % (2295337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.45/9.26 % (2295337)CaDiCaL version: 2.1.3
% 25.45/9.26 % (2295337)Termination reason: Instruction limit
% 25.45/9.26 % (2295337)Termination phase: SInE selection
% 25.45/9.26 % (2295337)Time elapsed: 0.126 s
% 25.45/9.26 % (2295337)Peak memory usage: 201 MB
% 25.45/9.26 % (2295337)Instructions burned: 286 (million)
% 25.45/9.26 % (2295345)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=1804604047:s2a=on:i=248:s2at=1.23:gtg=position_2941 on theBenchmark for (2941ds/248Mi)
% 25.45/9.26 % (2295343)Instruction limit reached!
% 25.45/9.26 % (2295343)------------------------------
% 25.45/9.26 % (2295343)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.45/9.26 % (2295343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.45/9.26 % (2295343)CaDiCaL version: 2.1.3
% 25.45/9.26 % (2295343)Termination reason: Instruction limit
% 25.45/9.26 % (2295343)Termination phase: Property scanning
% 25.45/9.26 % (2295343)Time elapsed: 0.075 s
% 25.45/9.26 % (2295343)Peak memory usage: 201 MB
% 25.45/9.26 % (2295343)Instructions burned: 158 (million)
% 25.45/9.26 % (2295345)Instruction limit reached!
% 25.45/9.26 % (2295345)------------------------------
% 25.45/9.26 % (2295345)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.45/9.26 % (2295345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.45/9.26 % (2295345)CaDiCaL version: 2.1.3
% 25.45/9.26 % (2295345)Termination reason: Instruction limit
% 25.45/9.26 % (2295345)Termination phase: Property scanning
% 25.45/9.26 % (2295345)Time elapsed: 0.112 s
% 25.45/9.26 % (2295345)Peak memory usage: 201 MB
% 25.45/9.26 % (2295345)Instructions burned: 248 (million)
% 25.45/9.26 % (2295349)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3472790438:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2940 on theBenchmark for (2940ds/294Mi)
% 25.45/9.26 % (2295351)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=208079171:i=2350_2939 on theBenchmark for (2939ds/2350Mi)
% 25.45/9.26 % (2295344)Instruction limit reached!
% 25.45/9.26 % (2295344)------------------------------
% 25.45/9.26 % (2295344)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.45/9.26 % (2295344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.45/9.26 % (2295344)CaDiCaL version: 2.1.3
% 25.45/9.26 % (2295344)Termination reason: Instruction limit
% 25.45/9.26 % (2295344)Termination phase: SInE selection
% 25.45/9.26 % (2295344)Time elapsed: 0.245 s
% 25.45/9.26 % (2295344)Peak memory usage: 201 MB
% 25.45/9.26 % (2295344)Instructions burned: 326 (million)
% 25.45/9.26 % (2295349)Instruction limit reached!
% 25.45/9.26 % (2295349)------------------------------
% 25.45/9.26 % (2295349)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.45/9.26 % (2295349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.45/9.26 % (2295349)CaDiCaL version: 2.1.3
% 25.45/9.26 % (2295349)Termination reason: Instruction limit
% 25.45/9.26 % (2295349)Termination phase: SInE selection
% 25.45/9.26 % (2295349)Time elapsed: 0.128 s
% 25.45/9.26 % (2295349)Peak memory usage: 201 MB
% 25.45/9.26 % (2295349)Instructions burned: 296 (million)
% 25.45/9.26 % (2295352)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3850375650:cts=off:i=113:fsr=off:ss=included:sgt=4_2939 on theBenchmark for (2939ds/113Mi)
% 25.45/9.26 % (2295352)Instruction limit reached!
% 25.45/9.26 % (2295352)------------------------------
% 25.45/9.26 % (2295352)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.45/9.26 % (2295352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.45/9.26 % (2295352)CaDiCaL version: 2.1.3
% 25.45/9.26 % (2295352)Termination reason: Instruction limit
% 25.45/9.26 % (2295352)Termination phase: SInE selection
% 25.45/9.26 % (2295352)Time elapsed: 0.088 s
% 25.45/9.26 % (2295352)Peak memory usage: 201 MB
% 25.45/9.26 % (2295352)Instructions burned: 113 (million)
% 25.45/9.26 % (2295355)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=511966603:i=127:av=off:fsr=off:sup=off_2937 on theBenchmark for (2937ds/127Mi)
% 25.45/9.26 % (2295357)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1667484839:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2937 on theBenchmark for (2937ds/114Mi)
% 25.45/9.26 % (2295357)Instruction limit reached!
% 25.45/9.26 % (2295357)------------------------------
% 25.45/9.26 % (2295357)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.89/14.08 % (2295357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.89/14.08 % (2295357)CaDiCaL version: 2.1.3
% 59.89/14.08 % (2295357)Termination reason: Instruction limit
% 59.89/14.08 % (2295357)Termination phase: Property scanning
% 59.89/14.08 % (2295357)Time elapsed: 0.031 s
% 59.89/14.08 % (2295357)Peak memory usage: 201 MB
% 59.89/14.08 % (2295357)Instructions burned: 114 (million)
% 59.89/14.08 % (2295355)Instruction limit reached!
% 59.89/14.08 % (2295355)------------------------------
% 59.89/14.08 % (2295355)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.89/14.08 % (2295355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.89/14.08 % (2295355)CaDiCaL version: 2.1.3
% 59.89/14.08 % (2295355)Termination reason: Instruction limit
% 59.89/14.08 % (2295355)Termination phase: Preprocessing 1
% 59.89/14.08 % (2295355)Time elapsed: 0.103 s
% 59.89/14.08 % (2295355)Peak memory usage: 202 MB
% 59.89/14.08 % (2295355)Instructions burned: 127 (million)
% 59.89/14.08 % (2295358)lrs+10_1_sil=8000:sp=occurrence:random_seed=2675752168:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2936 on theBenchmark for (2936ds/907Mi)
% 59.89/14.08 % (2295361)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2845418179:i=437:sd=1:aac=none:ss=included_2935 on theBenchmark for (2935ds/437Mi)
% 59.89/14.08 % (2295362)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3096826395:i=5202:ss=axioms:sgt=16_2935 on theBenchmark for (2935ds/5202Mi)
% 59.89/14.08 % (2295361)Instruction limit reached!
% 59.89/14.08 % (2295361)------------------------------
% 59.89/14.08 % (2295361)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.89/14.08 % (2295361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.89/14.08 % (2295361)CaDiCaL version: 2.1.3
% 59.89/14.08 % (2295361)Termination reason: Instruction limit
% 59.89/14.08 % (2295361)Termination phase: SInE selection
% 59.89/14.08 % (2295361)Time elapsed: 0.187 s
% 59.89/14.08 % (2295361)Peak memory usage: 202 MB
% 59.89/14.08 % (2295361)Instructions burned: 439 (million)
% 59.89/14.08 % (2295366)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2965743206:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2932 on theBenchmark for (2932ds/134Mi)
% 59.89/14.08 % (2295366)Instruction limit reached!
% 59.89/14.08 % (2295366)------------------------------
% 59.89/14.08 % (2295366)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.89/14.08 % (2295366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.89/14.08 % (2295366)CaDiCaL version: 2.1.3
% 59.89/14.08 % (2295366)Termination reason: Instruction limit
% 59.89/14.08 % (2295366)Termination phase: SInE selection
% 59.89/14.08 % (2295366)Time elapsed: 0.060 s
% 59.89/14.08 % (2295366)Peak memory usage: 201 MB
% 59.89/14.08 % (2295366)Instructions burned: 136 (million)
% 59.89/14.08 % (2295368)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2873743329:st=8:i=592:sd=3:ep=RST:ss=axioms_2930 on theBenchmark for (2930ds/592Mi)
% 59.89/14.08 % (2295358)Instruction limit reached!
% 59.89/14.08 % (2295358)------------------------------
% 59.89/14.08 % (2295358)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.89/14.08 % (2295358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.89/14.08 % (2295358)CaDiCaL version: 2.1.3
% 59.89/14.08 % (2295358)Termination reason: Instruction limit
% 59.89/14.08 % (2295358)Termination phase: Preprocessing 2
% 59.89/14.08 % (2295358)Time elapsed: 0.684 s
% 59.89/14.08 % (2295358)Peak memory usage: 207 MB
% 59.89/14.08 % (2295358)Instructions burned: 907 (million)
% 59.89/14.08 % (2295368)Instruction limit reached!
% 59.89/14.08 % (2295368)------------------------------
% 59.89/14.08 % (2295368)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.89/14.08 % (2295368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.89/14.08 % (2295368)CaDiCaL version: 2.1.3
% 59.89/14.08 % (2295368)Termination reason: Instruction limit
% 59.89/14.08 % (2295368)Termination phase: SInE selection
% 59.89/14.08 % (2295368)Time elapsed: 0.222 s
% 59.89/14.08 % (2295368)Peak memory usage: 203 MB
% 59.89/14.08 % (2295368)Instructions burned: 594 (million)
% 59.89/14.08 % (2295370)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=931183532:st=3:i=13193:sd=3:ss=axioms_2927 on theBenchmark for (2927ds/13193Mi)
% 59.89/14.08 % (2295371)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=2152227716:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2927 on theBenchmark for (2927ds/125Mi)
% 92.33/18.61 % (2295371)Instruction limit reached!
% 92.33/18.61 % (2295371)------------------------------
% 92.33/18.61 % (2295371)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 92.33/18.61 % (2295371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.33/18.61 % (2295371)CaDiCaL version: 2.1.3
% 92.33/18.61 % (2295371)Termination reason: Instruction limit
% 92.33/18.61 % (2295371)Termination phase: Property scanning
% 92.33/18.61 % (2295371)Time elapsed: 0.035 s
% 92.33/18.61 % (2295371)Peak memory usage: 201 MB
% 92.33/18.61 % (2295371)Instructions burned: 128 (million)
% 92.33/18.61 % (2295374)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3260024966:i=134:gtgl=5:slsql=off:gtg=exists_sym_2925 on theBenchmark for (2925ds/134Mi)
% 92.33/18.61 % (2295374)Instruction limit reached!
% 92.33/18.61 % (2295374)------------------------------
% 92.33/18.61 % (2295374)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 92.33/18.61 % (2295374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.33/18.61 % (2295374)CaDiCaL version: 2.1.3
% 92.33/18.61 % (2295374)Termination reason: Instruction limit
% 92.33/18.61 % (2295374)Termination phase: Property scanning
% 92.33/18.61 % (2295374)Time elapsed: 0.036 s
% 92.33/18.61 % (2295374)Peak memory usage: 201 MB
% 92.33/18.61 % (2295374)Instructions burned: 139 (million)
% 92.33/18.61 % (2295376)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=601318690:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2923 on theBenchmark for (2923ds/141Mi)
% 92.33/18.61 % (2295376)Instruction limit reached!
% 92.33/18.61 % (2295376)------------------------------
% 92.33/18.61 % (2295376)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 92.33/18.61 % (2295376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.33/18.61 % (2295376)CaDiCaL version: 2.1.3
% 92.33/18.61 % (2295376)Termination reason: Instruction limit
% 92.33/18.61 % (2295376)Termination phase: SInE selection
% 92.33/18.61 % (2295376)Time elapsed: 0.063 s
% 92.33/18.61 % (2295376)Peak memory usage: 201 MB
% 92.33/18.61 % (2295376)Instructions burned: 142 (million)
% 92.33/18.61 % (2295378)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3489105718:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2921 on theBenchmark for (2921ds/431Mi)
% 92.33/18.61 % (2295351)Instruction limit reached!
% 92.33/18.61 % (2295351)------------------------------
% 92.33/18.61 % (2295351)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 92.33/18.61 % (2295351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.33/18.61 % (2295351)CaDiCaL version: 2.1.3
% 92.33/18.61 % (2295351)Termination reason: Instruction limit
% 92.33/18.61 % (2295351)Termination phase: Preprocessing 3
% 92.33/18.61 % (2295351)Time elapsed: 1.879 s
% 92.33/18.61 % (2295351)Peak memory usage: 305 MB
% 92.33/18.61 % (2295351)Instructions burned: 2350 (million)
% 92.33/18.61 % (2295378)Instruction limit reached!
% 92.33/18.61 % (2295378)------------------------------
% 92.33/18.61 % (2295378)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 92.33/18.61 % (2295378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.33/18.61 % (2295378)CaDiCaL version: 2.1.3
% 92.33/18.61 % (2295378)Termination reason: Instruction limit
% 92.33/18.61 % (2295378)Termination phase: SInE selection
% 92.33/18.61 % (2295378)Time elapsed: 0.181 s
% 92.33/18.61 % (2295378)Peak memory usage: 202 MB
% 92.33/18.61 % (2295378)Instructions burned: 431 (million)
% 92.33/18.61 % (2295380)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=527488642:i=6060:aac=none:ins=25_2919 on theBenchmark for (2919ds/6060Mi)
% 92.33/18.61 % (2295381)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=3470450411:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2918 on theBenchmark for (2918ds/150Mi)
% 92.33/18.61 % (2295381)Instruction limit reached!
% 92.33/18.61 % (2295381)------------------------------
% 92.33/18.61 % (2295381)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 92.33/18.61 % (2295381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.33/18.61 % (2295381)CaDiCaL version: 2.1.3
% 92.33/18.61 % (2295381)Termination reason: Instruction limit
% 113.58/21.69 % (2295381)Termination phase: SInE selection
% 113.58/21.69 % (2295381)Time elapsed: 0.066 s
% 113.58/21.69 % (2295381)Peak memory usage: 201 MB
% 113.58/21.69 % (2295381)Instructions burned: 152 (million)
% 113.58/21.69 % (2295384)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3324305922:i=14155:bd=all_2916 on theBenchmark for (2916ds/14155Mi)
% 113.58/21.69 % (2295362)Instruction limit reached!
% 113.58/21.69 % (2295362)------------------------------
% 113.58/21.69 % (2295362)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 113.58/21.69 % (2295362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 113.58/21.69 % (2295362)CaDiCaL version: 2.1.3
% 113.58/21.69 % (2295362)Termination reason: Instruction limit
% 113.58/21.69 % (2295362)Termination phase: Saturation
% 113.58/21.69 % (2295362)Time elapsed: 3.464 s
% 113.58/21.69 % (2295362)Peak memory usage: 380 MB
% 113.58/21.69 % (2295362)Instructions burned: 5202 (million)
% 113.58/21.69 % (2295386)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3121383242:i=667:av=off:fsr=off_2898 on theBenchmark for (2898ds/667Mi)
% 113.58/21.69 % (2295386)Instruction limit reached!
% 113.58/21.69 % (2295386)------------------------------
% 113.58/21.69 % (2295386)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 113.58/21.69 % (2295386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 113.58/21.69 % (2295386)CaDiCaL version: 2.1.3
% 113.58/21.69 % (2295386)Termination reason: Instruction limit
% 113.58/21.69 % (2295386)Termination phase: Preprocessing 2
% 113.58/21.69 % (2295386)Time elapsed: 0.615 s
% 113.58/21.69 % (2295386)Peak memory usage: 218 MB
% 113.58/21.69 % (2295386)Instructions burned: 667 (million)
% 113.58/21.69 % (2295388)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=3715397834:s2a=on:i=185:s2at=1.8:fdi=4_2889 on theBenchmark for (2889ds/185Mi)
% 113.58/21.69 % (2295388)Instruction limit reached!
% 113.58/21.69 % (2295388)------------------------------
% 113.58/21.69 % (2295388)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 113.58/21.69 % (2295388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 113.58/21.69 % (2295388)CaDiCaL version: 2.1.3
% 113.58/21.69 % (2295388)Termination reason: Instruction limit
% 113.58/21.69 % (2295388)Termination phase: SInE selection
% 113.58/21.69 % (2295388)Time elapsed: 0.143 s
% 113.58/21.69 % (2295388)Peak memory usage: 201 MB
% 113.58/21.69 % (2295388)Instructions burned: 185 (million)
% 113.58/21.69 % (2295390)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2933611812:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2886 on theBenchmark for (2886ds/193Mi)
% 113.58/21.69 % (2295390)Instruction limit reached!
% 113.58/21.69 % (2295390)------------------------------
% 113.58/21.69 % (2295390)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 113.58/21.69 % (2295390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 113.58/21.69 % (2295390)CaDiCaL version: 2.1.3
% 113.58/21.69 % (2295390)Termination reason: Instruction limit
% 113.58/21.69 % (2295390)Termination phase: SInE selection
% 113.58/21.69 % (2295390)Time elapsed: 0.149 s
% 113.58/21.69 % (2295390)Peak memory usage: 201 MB
% 113.58/21.69 % (2295390)Instructions burned: 194 (million)
% 113.58/21.69 % (2295392)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=2544825677:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2883 on theBenchmark for (2883ds/4850Mi)
% 113.58/21.69 % (2295384)Instruction limit reached!
% 113.58/21.69 % (2295384)------------------------------
% 113.58/21.69 % (2295384)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 113.58/21.69 % (2295384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 113.58/21.69 % (2295384)CaDiCaL version: 2.1.3
% 113.58/21.69 % (2295384)Termination reason: Instruction limit
% 113.58/21.69 % (2295384)Termination phase: Property scanning
% 113.58/21.69 % (2295384)Time elapsed: 4.064 s
% 113.58/21.69 % (2295384)Peak memory usage: 447 MB
% 113.58/21.69 % (2295384)Instructions burned: 14156 (million)
% 113.58/21.69 % (2295394)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=1344657769:i=12111:sd=1:ss=included_2874 on theBenchmark for (2874ds/12111Mi)
% 113.58/21.69 % (2295380)Instruction limit reached!
% 113.58/21.69 % (2295380)------------------------------
% 113.58/21.69 % (2295380)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 152.73/27.17 % (2295380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.73/27.17 % (2295380)CaDiCaL version: 2.1.3
% 152.73/27.17 % (2295380)Termination reason: Instruction limit
% 152.73/27.17 % (2295380)Termination phase: NewCNF
% 152.73/27.17 % (2295380)Time elapsed: 4.917 s
% 152.73/27.17 % (2295380)Peak memory usage: 381 MB
% 152.73/27.17 % (2295380)Instructions burned: 6060 (million)
% 152.73/27.17 % (2295396)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=223365826:i=319:kws=precedence:fsr=off_2867 on theBenchmark for (2867ds/319Mi)
% 152.73/27.17 % (2295396)Instruction limit reached!
% 152.73/27.17 % (2295396)------------------------------
% 152.73/27.17 % (2295396)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 152.73/27.17 % (2295396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.73/27.17 % (2295396)CaDiCaL version: 2.1.3
% 152.73/27.17 % (2295396)Termination reason: Instruction limit
% 152.73/27.17 % (2295396)Termination phase: Preprocessing 1
% 152.73/27.17 % (2295396)Time elapsed: 0.238 s
% 152.73/27.17 % (2295396)Peak memory usage: 203 MB
% 152.73/27.17 % (2295396)Instructions burned: 319 (million)
% 152.73/27.17 % (2295398)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=3491573998:i=2064:ep=RST_2863 on theBenchmark for (2863ds/2064Mi)
% 152.73/27.17 % (2295392)Instruction limit reached!
% 152.73/27.17 % (2295392)------------------------------
% 152.73/27.17 % (2295392)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 152.73/27.17 % (2295392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.73/27.17 % (2295392)CaDiCaL version: 2.1.3
% 152.73/27.17 % (2295392)Termination reason: Instruction limit
% 152.73/27.17 % (2295392)Termination phase: Property scanning
% 152.73/27.17 % (2295392)Time elapsed: 3.337 s
% 152.73/27.17 % (2295392)Peak memory usage: 355 MB
% 152.73/27.17 % (2295392)Instructions burned: 4853 (million)
% 152.73/27.17 % (2295400)dis-1011_128_sil=32000:random_seed=4198826503:i=3706:ep=RST:av=off_2848 on theBenchmark for (2848ds/3706Mi)
% 152.73/27.17 % (2295398)Instruction limit reached!
% 152.73/27.17 % (2295398)------------------------------
% 152.73/27.17 % (2295398)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 152.73/27.17 % (2295398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.73/27.17 % (2295398)CaDiCaL version: 2.1.3
% 152.73/27.17 % (2295398)Termination reason: Instruction limit
% 152.73/27.17 % (2295398)Termination phase: Preprocessing 3
% 152.73/27.17 % (2295398)Time elapsed: 1.583 s
% 152.73/27.17 % (2295398)Peak memory usage: 317 MB
% 152.73/27.17 % (2295398)Instructions burned: 2064 (million)
% 152.73/27.17 % (2295370)Instruction limit reached!
% 152.73/27.17 % (2295370)------------------------------
% 152.73/27.17 % (2295370)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 152.73/27.17 % (2295370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.73/27.17 % (2295370)CaDiCaL version: 2.1.3
% 152.73/27.17 % (2295370)Termination reason: Instruction limit
% 152.73/27.17 % (2295370)Termination phase: Saturation
% 152.73/27.17 % (2295370)Time elapsed: 8.139 s
% 152.73/27.17 % (2295370)Peak memory usage: 561 MB
% 152.73/27.17 % (2295370)Instructions burned: 13193 (million)
% 152.73/27.17 % (2295402)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=1474299678:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2845 on theBenchmark for (2845ds/757Mi)
% 152.73/27.17 % (2295404)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2728185734:i=13913:ss=axioms:sgt=8_2844 on theBenchmark for (2844ds/13913Mi)
% 152.73/27.17 % (2295402)Instruction limit reached!
% 152.73/27.17 % (2295402)------------------------------
% 152.73/27.17 % (2295402)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 152.73/27.17 % (2295402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.73/27.17 % (2295402)CaDiCaL version: 2.1.3
% 152.73/27.17 % (2295402)Termination reason: Instruction limit
% 152.73/27.17 % (2295402)Termination phase: Saturation
% 152.73/27.17 % (2295402)Time elapsed: 0.607 s
% 152.73/27.17 % (2295402)Peak memory usage: 211 MB
% 152.73/27.17 % (2295402)Instructions burned: 759 (million)
% 152.73/27.17 % (2295406)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=3353569042:i=9925:aac=none_2837 on theBenchmark for (2837ds/9925Mi)
% 152.73/27.17 % (2295394)Instruction limit reached!
% 152.73/27.17 % (2295394)------------------------------
% 152.73/27.17 % (2295394)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 149.53/30.76 % (2295394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 149.53/30.76 % (2295394)CaDiCaL version: 2.1.3
% 149.53/30.76 % (2295394)Termination reason: Instruction limit
% 149.53/30.76 % (2295394)Termination phase: Saturation
% 149.53/30.76 % (2295394)Time elapsed: 4.959 s
% 149.53/30.76 % (2295394)Peak memory usage: 340 MB
% 149.53/30.76 % (2295394)Instructions burned: 12112 (million)
% 149.53/30.76 % (2295408)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=2090997174:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2822 on theBenchmark for (2822ds/2479Mi)
% 149.53/30.76 % (2295400)Instruction limit reached!
% 149.53/30.76 % (2295400)------------------------------
% 149.53/30.76 % (2295400)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 149.53/30.76 % (2295400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 149.53/30.76 % (2295400)CaDiCaL version: 2.1.3
% 149.53/30.76 % (2295400)Termination reason: Instruction limit
% 149.53/30.76 % (2295400)Termination phase: Preprocessing 3
% 149.53/30.76 % (2295400)Time elapsed: 2.606 s
% 149.53/30.76 % (2295400)Peak memory usage: 378 MB
% 149.53/30.76 % (2295400)Instructions burned: 3708 (million)
% 149.53/30.76 % (2295410)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=3900961547:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2819 on theBenchmark for (2819ds/440Mi)
% 149.53/30.76 % (2295410)Instruction limit reached!
% 149.53/30.76 % (2295410)------------------------------
% 149.53/30.76 % (2295410)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 149.53/30.76 % (2295410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 149.53/30.76 % (2295410)CaDiCaL version: 2.1.3
% 149.53/30.76 % (2295410)Termination reason: Instruction limit
% 149.53/30.76 % (2295410)Termination phase: Property scanning
% 149.53/30.76 % (2295410)Time elapsed: 0.193 s
% 149.53/30.76 % (2295410)Peak memory usage: 201 MB
% 149.53/30.76 % (2295410)Instructions burned: 441 (million)
% 149.53/30.76 % (2295412)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=1707606633:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2816 on theBenchmark for (2816ds/11145Mi)
% 149.53/30.76 % (2295408)Instruction limit reached!
% 149.53/30.76 % (2295408)------------------------------
% 149.53/30.76 % (2295408)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 149.53/30.76 % (2295408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 149.53/30.76 % (2295408)CaDiCaL version: 2.1.3
% 149.53/30.76 % (2295408)Termination reason: Instruction limit
% 149.53/30.76 % (2295408)Termination phase: Saturation
% 149.53/30.76 % (2295408)Time elapsed: 0.978 s
% 149.53/30.76 % (2295408)Peak memory usage: 220 MB
% 149.53/30.76 % (2295408)Instructions burned: 2481 (million)
% 149.53/30.76 % (2295414)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=554826625:cts=off:i=3034:av=off:er=known:fsd=on_2811 on theBenchmark for (2811ds/3034Mi)
% 149.53/30.76 % (2295414)Instruction limit reached!
% 149.53/30.76 % (2295414)------------------------------
% 149.53/30.76 % (2295414)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 149.53/30.76 % (2295414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 149.53/30.76 % (2295414)CaDiCaL version: 2.1.3
% 149.53/30.76 % (2295414)Termination reason: Instruction limit
% 149.53/30.76 % (2295414)Termination phase: Preprocessing 3
% 149.53/30.76 % (2295414)Time elapsed: 1.312 s
% 149.53/30.76 % (2295414)Peak memory usage: 337 MB
% 149.53/30.76 % (2295414)Instructions burned: 3035 (million)
% 149.53/30.76 % (2295416)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=2198049096:st=2:s2a=on:i=524:s2at=2:ss=axioms_2796 on theBenchmark for (2796ds/524Mi)
% 149.53/30.76 % (2295416)Instruction limit reached!
% 149.53/30.76 % (2295416)------------------------------
% 149.53/30.76 % (2295416)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 149.53/30.76 % (2295416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 149.53/30.76 % (2295416)CaDiCaL version: 2.1.3
% 149.53/30.76 % (2295416)Termination reason: Instruction limit
% 149.53/30.76 % (2295416)Termination phase: SInE selection
% 149.53/30.76 % (2295416)Time elapsed: 0.203 s
% 149.53/30.76 % (2295416)Peak memory usage: 202 MB
% 149.53/30.76 % (2295416)Instructions burned: 525 (million)
% 149.53/30.76 % (2295418)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=4273652107:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2793 on theBenchmark for (2793ds/1016Mi)
% 149.53/30.76 % (2295418)Instruction limit reached!
% 149.53/30.76 % (2295418)------------------------------
% 149.53/30.76 % (2295418)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 149.53/30.76 % (2295418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 149.53/30.76 % (2295418)CaDiCaL version: 2.1.3
% 149.53/30.76 % (2295418)Termination reason: Instruction limit
% 149.53/30.76 % (2295418)Termination phase: Saturation
% 149.53/30.76 % (2295418)Time elapsed: 0.435 s
% 149.53/30.76 % (2295418)Peak memory usage: 212 MB
% 149.53/30.76 % (2295418)Instructions burned: 1017 (million)
% 149.53/30.76 % (2295420)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=2399938173:i=14123:bd=preordered:ins=4_2787 on theBenchmark for (2787ds/14123Mi)
% 149.53/30.76 % (2295406)Instruction limit reached!
% 149.53/30.76 % (2295406)------------------------------
% 149.53/30.76 % (2295406)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 149.53/30.76 % (2295406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 149.53/30.76 % (2295406)CaDiCaL version: 2.1.3
% 149.53/30.76 % (2295406)Termination reason: Instruction limit
% 149.53/30.76 % (2295406)Termination phase: Property scanning
% 149.53/30.76 % (2295406)Time elapsed: 5.691 s
% 149.53/30.76 % (2295406)Peak memory usage: 447 MB
% 149.53/30.76 % (2295406)Instructions burned: 9925 (million)
% 149.53/30.76 % (2295422)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=3484711451:i=5781:kws=precedence:bd=all:rawr=on_2778 on theBenchmark for (2778ds/5781Mi)
% 149.53/30.76 % (2295404)Instruction limit reached!
% 149.53/30.76 % (2295404)------------------------------
% 149.53/30.76 % (2295404)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 149.53/30.76 % (2295404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 149.53/30.76 % (2295404)CaDiCaL version: 2.1.3
% 149.53/30.76 % (2295404)Termination reason: Instruction limit
% 149.53/30.76 % (2295404)Termination phase: Saturation
% 149.53/30.76 % (2295404)Time elapsed: 8.960 s
% 149.53/30.76 % (2295404)Peak memory usage: 394 MB
% 149.53/30.76 % (2295404)Instructions burned: 13913 (million)
% 149.53/30.76 % (2295424)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=2658760690:i=2448:gtgl=5:bd=preordered:gtg=all_2752 on theBenchmark for (2752ds/2448Mi)
% 149.53/30.76 % (2295424)Instruction limit reached!
% 149.53/30.76 % (2295424)------------------------------
% 149.53/30.76 % (2295424)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 149.53/30.76 % (2295424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 149.53/30.76 % (2295424)CaDiCaL version: 2.1.3
% 149.53/30.76 % (2295424)Termination reason: Instruction limit
% 149.53/30.76 % (2295424)Termination phase: Property scanning
% 149.53/30.76 % (2295424)Time elapsed: 1.042 s
% 149.53/30.76 % (2295424)Peak memory usage: 201 MB
% 149.53/30.76 % (2295424)Instructions burned: 2449 (million)
% 149.53/30.76 % (2295412)Instruction limit reached!
% 149.53/30.76 % (2295412)------------------------------
% 149.53/30.76 % (2295412)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 149.53/30.76 % (2295412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 149.53/30.76 % (2295412)CaDiCaL version: 2.1.3
% 149.53/30.76 % (2295412)Termination reason: Instruction limit
% 149.53/30.76 % (2295412)Termination phase: Saturation
% 149.53/30.76 % (2295412)Time elapsed: 7.488 s
% 149.53/30.76 % (2295412)Peak memory usage: 388 MB
% 149.53/30.76 % (2295412)Instructions burned: 11145 (million)
% 149.53/30.76 % (2295422)Instruction limit reached!
% 149.53/30.76 % (2295422)------------------------------
% 149.53/30.76 % (2295422)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 149.53/30.76 % (2295422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 149.53/30.76 % (2295422)CaDiCaL version: 2.1.3
% 149.53/30.76 % (2295422)Termination reason: Instruction limit
% 149.53/30.76 % (2295422)Termination phase: Property scanning
% 149.53/30.76 % (2295422)Time elapsed: 3.815 s
% 149.53/30.76 % (2295422)Peak memory usage: 412 MB
% 149.53/30.76 % (2295422)Instructions burned: 5782 (million)
% 149.53/30.76 % (2295426)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=4145413624:i=3223:kws=precedence:fgj=on:av=off_2740 on theBenchmark for (2740ds/3223Mi)
% 149.53/30.76 % (2295427)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=3099924019:st=5.6:i=2033:sd=3:ss=axioms_2739 on theBenchmark for (2739ds/2033Mi)
% 149.53/30.76 % (2295429)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=2658425440:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2738 on theBenchmark for (2738ds/2055Mi)
% 149.53/30.76 % (2295420)Instruction limit reached!
% 149.53/30.76 % (2295420)------------------------------
% 149.53/30.76 % (2295420)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 149.53/30.76 % (2295420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 149.53/30.76 % (2295420)CaDiCaL version: 2.1.3
% 149.53/30.76 % (2295420)Termination reason: Instruction limit
% 149.53/30.76 % (2295420)Termination phase: Saturation
% 149.53/30.76 % (2295420)Time elapsed: 5.910 s
% 149.53/30.76 % (2295420)Peak memory usage: 1271 MB
% 149.53/30.76 % (2295420)Instructions burned: 14124 (million)
% 149.53/30.76 % (2295429)Instruction limit reached!
% 149.53/30.76 % (2295429)------------------------------
% 149.53/30.76 % (2295429)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 149.53/30.76 % (2295429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 149.53/30.76 % (2295429)CaDiCaL version: 2.1.3
% 149.53/30.76 % (2295429)Termination reason: Instruction limit
% 149.53/30.76 % (2295429)Termination phase: SInE selection
% 149.53/30.76 % (2295429)Time elapsed: 1.030 s
% 149.53/30.76 % (2295429)Peak memory usage: 203 MB
% 149.53/30.76 % (2295429)Instructions burned: 2056 (million)
% 149.53/30.76 % (2295432)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=1452987123:i=21611:sd=3:ss=axioms_2726 on theBenchmark for (2726ds/21611Mi)
% 149.53/30.76 % (2295433)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=4110049727:i=4835:sd=13:ss=axioms:sgt=23_2726 on theBenchmark for (2726ds/4835Mi)
% 149.53/30.76 % (2295427)Instruction limit reached!
% 149.53/30.76 % (2295427)------------------------------
% 149.53/30.76 % (2295427)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 149.53/30.76 % (2295427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 149.53/30.76 % (2295427)CaDiCaL version: 2.1.3
% 149.53/30.76 % (2295427)Termination reason: Instruction limit
% 149.53/30.76 % (2295427)Termination phase: Preprocessing 3
% 149.53/30.76 % (2295427)Time elapsed: 1.557 s
% 149.53/30.76 % (2295427)Peak memory usage: 233 MB
% 149.53/30.76 % (2295427)Instructions burned: 2033 (million)
% 149.53/30.76 % (2295436)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=569612354:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2721 on theBenchmark for (2721ds/797Mi)
% 149.53/30.76 % (2295436)Instruction limit reached!
% 149.53/30.76 % (2295436)------------------------------
% 149.53/30.76 % (2295436)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 149.53/30.76 % (2295436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 149.53/30.76 % (2295436)CaDiCaL version: 2.1.3
% 149.53/30.76 % (2295436)Termination reason: Instruction limit
% 149.53/30.76 % (2295436)Termination phase: SInE selection
% 149.53/30.76 % (2295436)Time elapsed: 0.516 s
% 149.53/30.76 % (2295436)Peak memory usage: 203 MB
% 149.53/30.76 % (2295436)Instructions burned: 798 (million)
% 149.53/30.76 % (2295426)Instruction limit reached!
% 149.53/30.76 % (2295426)------------------------------
% 149.53/30.76 % (2295426)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 149.53/30.76 % (2295426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 149.53/30.76 % (2295426)CaDiCaL version: 2.1.3
% 149.53/30.76 % (2295426)Termination reason: Instruction limit
% 149.53/30.76 % (2295426)Termination phase: Preprocessing 3
% 149.53/30.76 % (2295426)Time elapsed: 2.392 s
% 149.53/30.76 % (2295426)Peak memory usage: 343 MB
% 149.53/30.76 % (2295426)Instructions burned: 3223 (million)
% 149.53/30.76 % (2295438)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=468030941:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2714 on theBenchmark for (2714ds/2326Mi)
% 149.53/30.76 % (2295439)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=3770155573:i=6038:nm=6_2713 on theBenchmark for (2713ds/6038Mi)
% 149.53/30.76 % (2295432)First to succeed.
% 149.53/30.76 % (2295432)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2295277"
% 149.53/30.76 % (2295432)Refutation found. Thanks to Tanya!
% 149.53/30.76 % SZS status Theorem for theBenchmark
% 149.53/30.76 % SZS output start Proof for theBenchmark
% See solution above
% 177.60/30.89 % (2295432)------------------------------
% 177.60/30.89 % (2295432)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 177.60/30.89 % (2295432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 177.60/30.89 % (2295432)CaDiCaL version: 2.1.3
% 177.60/30.89 % (2295432)Termination reason: Refutation
% 177.60/30.89 % (2295432)Time elapsed: 1.932 s
% 177.60/30.89 % (2295432)Peak memory usage: 350 MB
% 177.60/30.89 % (2295432)Instructions burned: 5058 (million)
% 177.60/30.89 % (2295432)------------------------------
% 177.60/30.89 % (2295432)------------------------------
% 177.60/30.89 % (2295277)Success in time 29.852 s
% 177.60/30.89 % Vampire exiting
%------------------------------------------------------------------------------