%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU428+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 : n006.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:58 PM UTC 2026
% Result : Theorem 103.92s 27.42s
% Output : Refutation 182.11s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 66
% Syntax : Number of formulae : 425 ( 66 unt; 47 def)
% Number of atoms : 2156 ( 123 equ)
% Maximal formula atoms : 15 ( 5 avg)
% Number of connectives : 3207 (1476 ~;1595 |; 65 &)
% ( 46 <=>; 24 =>; 0 <=; 1 <~>)
% Maximal formula depth : 18 ( 7 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 44 ( 42 usr; 40 prp; 0-2 aty)
% Number of functors : 26 ( 26 usr; 13 con; 0-4 aty)
% Number of variables : 454 ( 0 sgn 439 !; 15 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X0,X1] :
( ! [X2] :
( r2_hidden(X2,X0)
<=> r2_hidden(X2,X1) )
=> X0 = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2_tarski) ).
fof(f30,axiom,
! [X0,X1,X2] :
( X2 = k2_xboole_0(X0,X1)
<=> ! [X3] :
( r2_hidden(X3,X2)
<=> ( r2_hidden(X3,X0)
| r2_hidden(X3,X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d2_xboole_0) ).
fof(f31,axiom,
! [X0,X1,X2] :
( X2 = k3_xboole_0(X0,X1)
<=> ! [X3] :
( r2_hidden(X3,X2)
<=> ( r2_hidden(X3,X0)
& r2_hidden(X3,X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d3_xboole_0) ).
fof(f567,axiom,
! [X0,X1,X2] :
( ( m1_subset_1(X1,k1_zfmisc_1(X0))
& m1_subset_1(X2,k1_zfmisc_1(X0)) )
=> m1_subset_1(k4_subset_1(X0,X1,X2),k1_zfmisc_1(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k4_subset_1) ).
fof(f568,axiom,
! [X0,X1,X2] :
( ( m1_subset_1(X1,k1_zfmisc_1(X0))
& m1_subset_1(X2,k1_zfmisc_1(X0)) )
=> k4_subset_1(X0,X1,X2) = k4_subset_1(X0,X2,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_k4_subset_1) ).
fof(f570,axiom,
! [X0,X1,X2] :
( ( m1_subset_1(X1,k1_zfmisc_1(X0))
& m1_subset_1(X2,k1_zfmisc_1(X0)) )
=> k4_subset_1(X0,X1,X2) = k2_xboole_0(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k4_subset_1) ).
fof(f571,axiom,
! [X0,X1,X2] :
( ( m1_subset_1(X1,k1_zfmisc_1(X0))
& m1_subset_1(X2,k1_zfmisc_1(X0)) )
=> m1_subset_1(k5_subset_1(X0,X1,X2),k1_zfmisc_1(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k5_subset_1) ).
fof(f572,axiom,
! [X0,X1,X2] :
( ( m1_subset_1(X1,k1_zfmisc_1(X0))
& m1_subset_1(X2,k1_zfmisc_1(X0)) )
=> k5_subset_1(X0,X1,X2) = k5_subset_1(X0,X2,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_k5_subset_1) ).
fof(f574,axiom,
! [X0,X1,X2] :
( ( m1_subset_1(X1,k1_zfmisc_1(X0))
& m1_subset_1(X2,k1_zfmisc_1(X0)) )
=> k5_subset_1(X0,X1,X2) = k3_xboole_0(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k5_subset_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(f679,axiom,
! [X0,X1,X2] :
~ ( r2_hidden(X0,X1)
& m1_subset_1(X1,k1_zfmisc_1(X2))
& v1_xboole_0(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t5_subset) ).
fof(f19064,axiom,
! [X0,X1,X2,X3] :
( ( m1_subset_1(X2,k1_zfmisc_1(X0))
& m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) )
=> m1_subset_1(k8_relset_2(X0,X1,X2,X3),k1_zfmisc_1(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k8_relset_2) ).
fof(f19095,axiom,
! [X0,X1,X2,X3] :
( m1_subset_1(X3,k1_zfmisc_1(X0))
=> ! [X4] :
( m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
=> ( r2_hidden(X2,k8_relset_2(X0,X1,X3,X4))
=> ! [X5] :
( r2_hidden(X5,X3)
=> r2_hidden(X2,k9_relat_1(X4,k1_tarski(X5))) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t24_relset_2) ).
fof(f19096,axiom,
! [X0] :
( ~ v1_xboole_0(X0)
=> ! [X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(X1))
=> ! [X3] :
( m1_subset_1(X3,X0)
=> ! [X4] :
( m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X1,X0)))
=> ( r2_hidden(X3,k8_relset_2(X1,X0,X2,X4))
<=> ! [X5] :
( r2_hidden(X5,X2)
=> r2_hidden(X3,k9_relat_1(X4,k1_tarski(X5))) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t25_relset_2) ).
fof(f19098,conjecture,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(X0))
=> ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(X0))
=> ! [X4] :
( m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
=> k8_relset_2(X0,X1,k4_subset_1(X0,X2,X3),X4) = k5_subset_1(X1,k8_relset_2(X0,X1,X2,X4),k8_relset_2(X0,X1,X3,X4)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t27_relset_2) ).
fof(f19099,negated_conjecture,
~ ! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(X0))
=> ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(X0))
=> ! [X4] :
( m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
=> k8_relset_2(X0,X1,k4_subset_1(X0,X2,X3),X4) = k5_subset_1(X1,k8_relset_2(X0,X1,X2,X4),k8_relset_2(X0,X1,X3,X4)) ) ) ),
inference(negated_conjecture,[status(cth)],[f19098]) ).
fof(f19137,plain,
? [X0,X1,X2] :
( ? [X3] :
( ? [X4] :
( k8_relset_2(X0,X1,k4_subset_1(X0,X2,X3),X4) != k5_subset_1(X1,k8_relset_2(X0,X1,X2,X4),k8_relset_2(X0,X1,X3,X4))
& m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) )
& m1_subset_1(X3,k1_zfmisc_1(X0)) )
& m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f19099]) ).
fof(f19167,plain,
! [X0,X1,X2] :
( k4_subset_1(X0,X1,X2) = k2_xboole_0(X1,X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f570]) ).
fof(f19168,plain,
! [X0,X1,X2] :
( k4_subset_1(X0,X1,X2) = k2_xboole_0(X1,X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(flattening,[],[f19167]) ).
fof(f19171,plain,
! [X0,X1,X2] :
( k4_subset_1(X0,X1,X2) = k4_subset_1(X0,X2,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f568]) ).
fof(f19172,plain,
! [X0,X1,X2] :
( k4_subset_1(X0,X1,X2) = k4_subset_1(X0,X2,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(flattening,[],[f19171]) ).
fof(f19173,plain,
! [X0,X1,X2] :
( m1_subset_1(k4_subset_1(X0,X1,X2),k1_zfmisc_1(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f567]) ).
fof(f19174,plain,
! [X0,X1,X2] :
( m1_subset_1(k4_subset_1(X0,X1,X2),k1_zfmisc_1(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(flattening,[],[f19173]) ).
fof(f19194,plain,
! [X0,X1,X2] :
( k5_subset_1(X0,X1,X2) = k3_xboole_0(X1,X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f574]) ).
fof(f19195,plain,
! [X0,X1,X2] :
( k5_subset_1(X0,X1,X2) = k3_xboole_0(X1,X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(flattening,[],[f19194]) ).
fof(f19198,plain,
! [X0,X1,X2] :
( k5_subset_1(X0,X1,X2) = k5_subset_1(X0,X2,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f572]) ).
fof(f19199,plain,
! [X0,X1,X2] :
( k5_subset_1(X0,X1,X2) = k5_subset_1(X0,X2,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(flattening,[],[f19198]) ).
fof(f19200,plain,
! [X0,X1,X2] :
( m1_subset_1(k5_subset_1(X0,X1,X2),k1_zfmisc_1(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f571]) ).
fof(f19201,plain,
! [X0,X1,X2] :
( m1_subset_1(k5_subset_1(X0,X1,X2),k1_zfmisc_1(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(flattening,[],[f19200]) ).
fof(f19206,plain,
! [X0] :
( ! [X1,X2] :
( ! [X3] :
( ! [X4] :
( ( r2_hidden(X3,k8_relset_2(X1,X0,X2,X4))
<=> ! [X5] :
( r2_hidden(X3,k9_relat_1(X4,k1_tarski(X5)))
| ~ r2_hidden(X5,X2) ) )
| ~ m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X1,X0))) )
| ~ m1_subset_1(X3,X0) )
| ~ m1_subset_1(X2,k1_zfmisc_1(X1)) )
| v1_xboole_0(X0) ),
inference(ennf_transformation,[],[f19096]) ).
fof(f19207,plain,
! [X0,X1,X2,X3] :
( ! [X4] :
( ! [X5] :
( r2_hidden(X2,k9_relat_1(X4,k1_tarski(X5)))
| ~ r2_hidden(X5,X3) )
| ~ r2_hidden(X2,k8_relset_2(X0,X1,X3,X4))
| ~ m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) )
| ~ m1_subset_1(X3,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f19095]) ).
fof(f19208,plain,
! [X0,X1,X2,X3] :
( ! [X4] :
( ! [X5] :
( r2_hidden(X2,k9_relat_1(X4,k1_tarski(X5)))
| ~ r2_hidden(X5,X3) )
| ~ r2_hidden(X2,k8_relset_2(X0,X1,X3,X4))
| ~ m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) )
| ~ m1_subset_1(X3,k1_zfmisc_1(X0)) ),
inference(flattening,[],[f19207]) ).
fof(f19209,plain,
! [X0,X1,X2,X3] :
( m1_subset_1(k8_relset_2(X0,X1,X2,X3),k1_zfmisc_1(X1))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| ~ m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(ennf_transformation,[],[f19064]) ).
fof(f19210,plain,
! [X0,X1,X2,X3] :
( m1_subset_1(k8_relset_2(X0,X1,X2,X3),k1_zfmisc_1(X1))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| ~ m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(flattening,[],[f19209]) ).
fof(f19213,plain,
! [X0,X1,X2] :
( ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ v1_xboole_0(X2) ),
inference(ennf_transformation,[],[f679]) ).
fof(f19427,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(f19428,plain,
! [X0,X1,X2] :
( m1_subset_1(X0,X2)
| ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2)) ),
inference(flattening,[],[f19427]) ).
fof(f19437,plain,
! [X0,X1] :
( X0 = X1
| ? [X2] :
( r2_hidden(X2,X0)
<~> r2_hidden(X2,X1) ) ),
inference(ennf_transformation,[],[f3]) ).
fof(f20249,plain,
( k8_relset_2(sK29,sK30,k4_subset_1(sK29,sK31,sK32),sK33) != k5_subset_1(sK30,k8_relset_2(sK29,sK30,sK31,sK33),k8_relset_2(sK29,sK30,sK32,sK33))
& m1_subset_1(sK33,k1_zfmisc_1(k2_zfmisc_1(sK29,sK30)))
& m1_subset_1(sK32,k1_zfmisc_1(sK29))
& m1_subset_1(sK31,k1_zfmisc_1(sK29)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK29,sK30,sK31,sK32,sK33]),skolemize(X0,sK29),skolemize(X1,sK30),skolemize(X2,sK31),skolemize(X3,sK32),skolemize(X4,sK33)],[f19137]) ).
fof(f20259,plain,
! [X0] :
( ! [X1,X2] :
( ! [X3] :
( ! [X4] :
( ( ( r2_hidden(X3,k8_relset_2(X1,X0,X2,X4))
| ? [X5] :
( ~ r2_hidden(X3,k9_relat_1(X4,k1_tarski(X5)))
& r2_hidden(X5,X2) ) )
& ( ! [X5] :
( r2_hidden(X3,k9_relat_1(X4,k1_tarski(X5)))
| ~ r2_hidden(X5,X2) )
| ~ r2_hidden(X3,k8_relset_2(X1,X0,X2,X4)) ) )
| ~ m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X1,X0))) )
| ~ m1_subset_1(X3,X0) )
| ~ m1_subset_1(X2,k1_zfmisc_1(X1)) )
| v1_xboole_0(X0) ),
inference(nnf_transformation,[],[f19206]) ).
fof(f20260,plain,
! [X0] :
( ! [X1,X2] :
( ! [X3] :
( ! [X4] :
( ( ( r2_hidden(X3,k8_relset_2(X1,X0,X2,X4))
| ? [X5] :
( ~ r2_hidden(X3,k9_relat_1(X4,k1_tarski(X5)))
& r2_hidden(X5,X2) ) )
& ( ! [X6] :
( r2_hidden(X3,k9_relat_1(X4,k1_tarski(X6)))
| ~ r2_hidden(X6,X2) )
| ~ r2_hidden(X3,k8_relset_2(X1,X0,X2,X4)) ) )
| ~ m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X1,X0))) )
| ~ m1_subset_1(X3,X0) )
| ~ m1_subset_1(X2,k1_zfmisc_1(X1)) )
| v1_xboole_0(X0) ),
inference(rectify,[],[f20259]) ).
fof(f20261,plain,
! [X0] :
( ! [X1,X2] :
( ! [X3] :
( ! [X4] :
( ( ( r2_hidden(X3,k8_relset_2(X1,X0,X2,X4))
| ( ~ r2_hidden(X3,k9_relat_1(X4,k1_tarski(sK37(X2,X3,X4))))
& r2_hidden(sK37(X2,X3,X4),X2) ) )
& ( ! [X6] :
( r2_hidden(X3,k9_relat_1(X4,k1_tarski(X6)))
| ~ r2_hidden(X6,X2) )
| ~ r2_hidden(X3,k8_relset_2(X1,X0,X2,X4)) ) )
| ~ m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X1,X0))) )
| ~ m1_subset_1(X3,X0) )
| ~ m1_subset_1(X2,k1_zfmisc_1(X1)) )
| v1_xboole_0(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK37]),skolemize(X5,sK37(X2,X3,X4))],[f20260]) ).
fof(f20364,plain,
! [X0,X1,X2] :
( ( X2 = k2_xboole_0(X0,X1)
| ? [X3] :
( ( ( ~ r2_hidden(X3,X0)
& ~ r2_hidden(X3,X1) )
| ~ r2_hidden(X3,X2) )
& ( r2_hidden(X3,X0)
| r2_hidden(X3,X1)
| r2_hidden(X3,X2) ) ) )
& ( ! [X3] :
( ( r2_hidden(X3,X2)
| ( ~ r2_hidden(X3,X0)
& ~ r2_hidden(X3,X1) ) )
& ( r2_hidden(X3,X0)
| r2_hidden(X3,X1)
| ~ r2_hidden(X3,X2) ) )
| k2_xboole_0(X0,X1) != X2 ) ),
inference(nnf_transformation,[],[f30]) ).
fof(f20365,plain,
! [X0,X1,X2] :
( ( X2 = k2_xboole_0(X0,X1)
| ? [X3] :
( ( ( ~ r2_hidden(X3,X0)
& ~ r2_hidden(X3,X1) )
| ~ r2_hidden(X3,X2) )
& ( r2_hidden(X3,X0)
| r2_hidden(X3,X1)
| r2_hidden(X3,X2) ) ) )
& ( ! [X3] :
( ( r2_hidden(X3,X2)
| ( ~ r2_hidden(X3,X0)
& ~ r2_hidden(X3,X1) ) )
& ( r2_hidden(X3,X0)
| r2_hidden(X3,X1)
| ~ r2_hidden(X3,X2) ) )
| k2_xboole_0(X0,X1) != X2 ) ),
inference(flattening,[],[f20364]) ).
fof(f20366,plain,
! [X0,X1,X2] :
( ( X2 = k2_xboole_0(X0,X1)
| ? [X3] :
( ( ( ~ r2_hidden(X3,X0)
& ~ r2_hidden(X3,X1) )
| ~ r2_hidden(X3,X2) )
& ( r2_hidden(X3,X0)
| r2_hidden(X3,X1)
| r2_hidden(X3,X2) ) ) )
& ( ! [X4] :
( ( r2_hidden(X4,X2)
| ( ~ r2_hidden(X4,X0)
& ~ r2_hidden(X4,X1) ) )
& ( r2_hidden(X4,X0)
| r2_hidden(X4,X1)
| ~ r2_hidden(X4,X2) ) )
| k2_xboole_0(X0,X1) != X2 ) ),
inference(rectify,[],[f20365]) ).
fof(f20367,plain,
! [X0,X1,X2] :
( ( X2 = k2_xboole_0(X0,X1)
| ( ( ( ~ r2_hidden(sK95(X0,X1,X2),X0)
& ~ r2_hidden(sK95(X0,X1,X2),X1) )
| ~ r2_hidden(sK95(X0,X1,X2),X2) )
& ( r2_hidden(sK95(X0,X1,X2),X0)
| r2_hidden(sK95(X0,X1,X2),X1)
| r2_hidden(sK95(X0,X1,X2),X2) ) ) )
& ( ! [X4] :
( ( r2_hidden(X4,X2)
| ( ~ r2_hidden(X4,X0)
& ~ r2_hidden(X4,X1) ) )
& ( r2_hidden(X4,X0)
| r2_hidden(X4,X1)
| ~ r2_hidden(X4,X2) ) )
| k2_xboole_0(X0,X1) != X2 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK95]),skolemize(X3,sK95(X0,X1,X2))],[f20366]) ).
fof(f20376,plain,
! [X0,X1] :
( X0 = X1
| ? [X2] :
( ( ~ r2_hidden(X2,X1)
| ~ r2_hidden(X2,X0) )
& ( r2_hidden(X2,X1)
| r2_hidden(X2,X0) ) ) ),
inference(nnf_transformation,[],[f19437]) ).
fof(f20377,plain,
! [X0,X1] :
( X0 = X1
| ( ( ~ r2_hidden(sK100(X0,X1),X1)
| ~ r2_hidden(sK100(X0,X1),X0) )
& ( r2_hidden(sK100(X0,X1),X1)
| r2_hidden(sK100(X0,X1),X0) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK100]),skolemize(X2,sK100(X0,X1))],[f20376]) ).
fof(f20396,plain,
! [X0,X1,X2] :
( ( X2 = k3_xboole_0(X0,X1)
| ? [X3] :
( ( ~ r2_hidden(X3,X0)
| ~ r2_hidden(X3,X1)
| ~ r2_hidden(X3,X2) )
& ( ( r2_hidden(X3,X0)
& r2_hidden(X3,X1) )
| r2_hidden(X3,X2) ) ) )
& ( ! [X3] :
( ( r2_hidden(X3,X2)
| ~ r2_hidden(X3,X0)
| ~ r2_hidden(X3,X1) )
& ( ( r2_hidden(X3,X0)
& r2_hidden(X3,X1) )
| ~ r2_hidden(X3,X2) ) )
| k3_xboole_0(X0,X1) != X2 ) ),
inference(nnf_transformation,[],[f31]) ).
fof(f20397,plain,
! [X0,X1,X2] :
( ( X2 = k3_xboole_0(X0,X1)
| ? [X3] :
( ( ~ r2_hidden(X3,X0)
| ~ r2_hidden(X3,X1)
| ~ r2_hidden(X3,X2) )
& ( ( r2_hidden(X3,X0)
& r2_hidden(X3,X1) )
| r2_hidden(X3,X2) ) ) )
& ( ! [X3] :
( ( r2_hidden(X3,X2)
| ~ r2_hidden(X3,X0)
| ~ r2_hidden(X3,X1) )
& ( ( r2_hidden(X3,X0)
& r2_hidden(X3,X1) )
| ~ r2_hidden(X3,X2) ) )
| k3_xboole_0(X0,X1) != X2 ) ),
inference(flattening,[],[f20396]) ).
fof(f20398,plain,
! [X0,X1,X2] :
( ( X2 = k3_xboole_0(X0,X1)
| ? [X3] :
( ( ~ r2_hidden(X3,X0)
| ~ r2_hidden(X3,X1)
| ~ r2_hidden(X3,X2) )
& ( ( r2_hidden(X3,X0)
& r2_hidden(X3,X1) )
| r2_hidden(X3,X2) ) ) )
& ( ! [X4] :
( ( r2_hidden(X4,X2)
| ~ r2_hidden(X4,X0)
| ~ r2_hidden(X4,X1) )
& ( ( r2_hidden(X4,X0)
& r2_hidden(X4,X1) )
| ~ r2_hidden(X4,X2) ) )
| k3_xboole_0(X0,X1) != X2 ) ),
inference(rectify,[],[f20397]) ).
fof(f20399,plain,
! [X0,X1,X2] :
( ( X2 = k3_xboole_0(X0,X1)
| ( ( ~ r2_hidden(sK114(X0,X1,X2),X0)
| ~ r2_hidden(sK114(X0,X1,X2),X1)
| ~ r2_hidden(sK114(X0,X1,X2),X2) )
& ( ( r2_hidden(sK114(X0,X1,X2),X0)
& r2_hidden(sK114(X0,X1,X2),X1) )
| r2_hidden(sK114(X0,X1,X2),X2) ) ) )
& ( ! [X4] :
( ( r2_hidden(X4,X2)
| ~ r2_hidden(X4,X0)
| ~ r2_hidden(X4,X1) )
& ( ( r2_hidden(X4,X0)
& r2_hidden(X4,X1) )
| ~ r2_hidden(X4,X2) ) )
| k3_xboole_0(X0,X1) != X2 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK114]),skolemize(X3,sK114(X0,X1,X2))],[f20398]) ).
fof(f20721,plain,
m1_subset_1(sK31,k1_zfmisc_1(sK29)),
inference(cnf_transformation,[],[f20249]) ).
fof(f20722,plain,
m1_subset_1(sK32,k1_zfmisc_1(sK29)),
inference(cnf_transformation,[],[f20249]) ).
fof(f20723,plain,
m1_subset_1(sK33,k1_zfmisc_1(k2_zfmisc_1(sK29,sK30))),
inference(cnf_transformation,[],[f20249]) ).
fof(f20724,plain,
k8_relset_2(sK29,sK30,k4_subset_1(sK29,sK31,sK32),sK33) != k5_subset_1(sK30,k8_relset_2(sK29,sK30,sK31,sK33),k8_relset_2(sK29,sK30,sK32,sK33)),
inference(cnf_transformation,[],[f20249]) ).
fof(f20758,plain,
! [X2,X0,X1] :
( k2_xboole_0(X1,X2) = k4_subset_1(X0,X1,X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f19168]) ).
fof(f20760,plain,
! [X2,X0,X1] :
( k4_subset_1(X0,X1,X2) = k4_subset_1(X0,X2,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f19172]) ).
fof(f20761,plain,
! [X2,X0,X1] :
( m1_subset_1(k4_subset_1(X0,X1,X2),k1_zfmisc_1(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f19174]) ).
fof(f20780,plain,
! [X2,X0,X1] :
( k3_xboole_0(X1,X2) = k5_subset_1(X0,X1,X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f19195]) ).
fof(f20782,plain,
! [X2,X0,X1] :
( k5_subset_1(X0,X1,X2) = k5_subset_1(X0,X2,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f19199]) ).
fof(f20783,plain,
! [X2,X0,X1] :
( m1_subset_1(k5_subset_1(X0,X1,X2),k1_zfmisc_1(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f19201]) ).
fof(f20790,plain,
! [X2,X3,X0,X1,X4] :
( r2_hidden(X3,k8_relset_2(X1,X0,X2,X4))
| r2_hidden(sK37(X2,X3,X4),X2)
| ~ m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X1,X0)))
| ~ m1_subset_1(X3,X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(X1))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f20261]) ).
fof(f20791,plain,
! [X2,X3,X0,X1,X4] :
( ~ r2_hidden(X3,k9_relat_1(X4,k1_tarski(sK37(X2,X3,X4))))
| r2_hidden(X3,k8_relset_2(X1,X0,X2,X4))
| ~ m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X1,X0)))
| ~ m1_subset_1(X3,X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(X1))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f20261]) ).
fof(f20792,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ r2_hidden(X2,k8_relset_2(X0,X1,X3,X4))
| ~ r2_hidden(X5,X3)
| r2_hidden(X2,k9_relat_1(X4,k1_tarski(X5)))
| ~ m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| ~ m1_subset_1(X3,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f19208]) ).
fof(f20793,plain,
! [X2,X3,X0,X1] :
( m1_subset_1(k8_relset_2(X0,X1,X2,X3),k1_zfmisc_1(X1))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| ~ m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(cnf_transformation,[],[f19210]) ).
fof(f20806,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ r2_hidden(X0,X1)
| ~ v1_xboole_0(X2) ),
inference(cnf_transformation,[],[f19213]) ).
fof(f21153,plain,
! [X2,X0,X1,X4] :
( r2_hidden(X4,X0)
| r2_hidden(X4,X1)
| ~ r2_hidden(X4,X2)
| k2_xboole_0(X0,X1) != X2 ),
inference(cnf_transformation,[],[f20367]) ).
fof(f21154,plain,
! [X2,X0,X1,X4] :
( r2_hidden(X4,X2)
| ~ r2_hidden(X4,X1)
| k2_xboole_0(X0,X1) != X2 ),
inference(cnf_transformation,[],[f20367]) ).
fof(f21165,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ r2_hidden(X0,X1)
| m1_subset_1(X0,X2) ),
inference(cnf_transformation,[],[f19428]) ).
fof(f21177,plain,
! [X0,X1] :
( r2_hidden(sK100(X0,X1),X1)
| X0 = X1
| r2_hidden(sK100(X0,X1),X0) ),
inference(cnf_transformation,[],[f20377]) ).
fof(f21178,plain,
! [X0,X1] :
( ~ r2_hidden(sK100(X0,X1),X1)
| X0 = X1
| ~ r2_hidden(sK100(X0,X1),X0) ),
inference(cnf_transformation,[],[f20377]) ).
fof(f21289,plain,
! [X2,X0,X1,X4] :
( r2_hidden(X4,X0)
| ~ r2_hidden(X4,X2)
| k3_xboole_0(X0,X1) != X2 ),
inference(cnf_transformation,[],[f20399]) ).
fof(f21290,plain,
! [X2,X0,X1,X4] :
( r2_hidden(X4,X2)
| ~ r2_hidden(X4,X0)
| ~ r2_hidden(X4,X1)
| k3_xboole_0(X0,X1) != X2 ),
inference(cnf_transformation,[],[f20399]) ).
fof(f22489,plain,
! [X0,X1,X4] :
( r2_hidden(X4,k2_xboole_0(X0,X1))
| ~ r2_hidden(X4,X1) ),
inference(equality_resolution,[],[f21154]) ).
fof(f22490,plain,
! [X0,X1,X4] :
( ~ r2_hidden(X4,k2_xboole_0(X0,X1))
| r2_hidden(X4,X1)
| r2_hidden(X4,X0) ),
inference(equality_resolution,[],[f21153]) ).
fof(f22496,plain,
! [X0,X1,X4] :
( r2_hidden(X4,k3_xboole_0(X0,X1))
| ~ r2_hidden(X4,X0)
| ~ r2_hidden(X4,X1) ),
inference(equality_resolution,[],[f21290]) ).
fof(f22497,plain,
! [X0,X1,X4] :
( ~ r2_hidden(X4,k3_xboole_0(X0,X1))
| r2_hidden(X4,X0) ),
inference(equality_resolution,[],[f21289]) ).
fof(f22613,definition,
sF343 = k4_subset_1(sK29,sK31,sK32),
introduced(definition,[new_symbols(definition,[sF343])],[function_definition]) ).
fof(f22614,plain,
k4_subset_1(sK29,sK31,sK32) = sF343,
inference(reorient_equations,[],[f22613]) ).
fof(f22615,definition,
sF344 = k8_relset_2(sK29,sK30,sF343,sK33),
introduced(definition,[new_symbols(definition,[sF344])],[function_definition]) ).
fof(f22616,plain,
k8_relset_2(sK29,sK30,sF343,sK33) = sF344,
inference(reorient_equations,[],[f22615]) ).
fof(f22617,definition,
sF345 = k8_relset_2(sK29,sK30,sK31,sK33),
introduced(definition,[new_symbols(definition,[sF345])],[function_definition]) ).
fof(f22618,plain,
k8_relset_2(sK29,sK30,sK31,sK33) = sF345,
inference(reorient_equations,[],[f22617]) ).
fof(f22619,definition,
sF346 = k8_relset_2(sK29,sK30,sK32,sK33),
introduced(definition,[new_symbols(definition,[sF346])],[function_definition]) ).
fof(f22620,plain,
k8_relset_2(sK29,sK30,sK32,sK33) = sF346,
inference(reorient_equations,[],[f22619]) ).
fof(f22621,definition,
sF347 = k5_subset_1(sK30,sF345,sF346),
introduced(definition,[new_symbols(definition,[sF347])],[function_definition]) ).
fof(f22622,plain,
k5_subset_1(sK30,sF345,sF346) = sF347,
inference(reorient_equations,[],[f22621]) ).
fof(f22623,plain,
sF344 != sF347,
inference(definition_folding,[],[f20724,f22622,f22620,f22618,f22616,f22614]) ).
fof(f22624,definition,
sF348 = k2_zfmisc_1(sK29,sK30),
introduced(definition,[new_symbols(definition,[sF348])],[function_definition]) ).
fof(f22625,plain,
k2_zfmisc_1(sK29,sK30) = sF348,
inference(reorient_equations,[],[f22624]) ).
fof(f22626,definition,
sF349 = k1_zfmisc_1(sF348),
introduced(definition,[new_symbols(definition,[sF349])],[function_definition]) ).
fof(f22627,plain,
k1_zfmisc_1(sF348) = sF349,
inference(reorient_equations,[],[f22626]) ).
fof(f22628,plain,
m1_subset_1(sK33,sF349),
inference(definition_folding,[],[f20723,f22627,f22625]) ).
fof(f22629,definition,
sF350 = k1_zfmisc_1(sK29),
introduced(definition,[new_symbols(definition,[sF350])],[function_definition]) ).
fof(f22630,plain,
k1_zfmisc_1(sK29) = sF350,
inference(reorient_equations,[],[f22629]) ).
fof(f22631,plain,
m1_subset_1(sK32,sF350),
inference(definition_folding,[],[f20722,f22630]) ).
fof(f22632,plain,
m1_subset_1(sK31,sF350),
inference(definition_folding,[],[f20721,f22630]) ).
fof(f22978,definition,
( spl351_68
<=> m1_subset_1(sK31,sF350) ),
introduced(definition,[new_symbols(definition,[spl351_68])],[avatar_definition]) ).
fof(f22980,plain,
( m1_subset_1(sK31,sF350)
| ~ spl351_68 ),
inference(avatar_component_clause,[],[f22978]) ).
fof(f22981,plain,
spl351_68,
inference(avatar_split_clause,[],[f22632,f22978]) ).
fof(f22983,definition,
( spl351_69
<=> m1_subset_1(sK32,sF350) ),
introduced(definition,[new_symbols(definition,[spl351_69])],[avatar_definition]) ).
fof(f22985,plain,
( m1_subset_1(sK32,sF350)
| ~ spl351_69 ),
inference(avatar_component_clause,[],[f22983]) ).
fof(f22986,plain,
spl351_69,
inference(avatar_split_clause,[],[f22631,f22983]) ).
fof(f22988,definition,
( spl351_70
<=> m1_subset_1(sK33,sF349) ),
introduced(definition,[new_symbols(definition,[spl351_70])],[avatar_definition]) ).
fof(f22990,plain,
( m1_subset_1(sK33,sF349)
| ~ spl351_70 ),
inference(avatar_component_clause,[],[f22988]) ).
fof(f22991,plain,
spl351_70,
inference(avatar_split_clause,[],[f22628,f22988]) ).
fof(f22993,definition,
( spl351_71
<=> sF344 = sF347 ),
introduced(definition,[new_symbols(definition,[spl351_71])],[avatar_definition]) ).
fof(f22995,plain,
( sF344 != sF347
| spl351_71 ),
inference(avatar_component_clause,[],[f22993]) ).
fof(f22996,plain,
~ spl351_71,
inference(avatar_split_clause,[],[f22623,f22993]) ).
fof(f22998,definition,
( spl351_72
<=> k4_subset_1(sK29,sK31,sK32) = sF343 ),
introduced(definition,[new_symbols(definition,[spl351_72])],[avatar_definition]) ).
fof(f23000,plain,
( k4_subset_1(sK29,sK31,sK32) = sF343
| ~ spl351_72 ),
inference(avatar_component_clause,[],[f22998]) ).
fof(f23001,plain,
spl351_72,
inference(avatar_split_clause,[],[f22614,f22998]) ).
fof(f23003,definition,
( spl351_73
<=> k8_relset_2(sK29,sK30,sF343,sK33) = sF344 ),
introduced(definition,[new_symbols(definition,[spl351_73])],[avatar_definition]) ).
fof(f23005,plain,
( k8_relset_2(sK29,sK30,sF343,sK33) = sF344
| ~ spl351_73 ),
inference(avatar_component_clause,[],[f23003]) ).
fof(f23006,plain,
spl351_73,
inference(avatar_split_clause,[],[f22616,f23003]) ).
fof(f23008,definition,
( spl351_74
<=> k8_relset_2(sK29,sK30,sK31,sK33) = sF345 ),
introduced(definition,[new_symbols(definition,[spl351_74])],[avatar_definition]) ).
fof(f23010,plain,
( k8_relset_2(sK29,sK30,sK31,sK33) = sF345
| ~ spl351_74 ),
inference(avatar_component_clause,[],[f23008]) ).
fof(f23011,plain,
spl351_74,
inference(avatar_split_clause,[],[f22618,f23008]) ).
fof(f23013,definition,
( spl351_75
<=> k8_relset_2(sK29,sK30,sK32,sK33) = sF346 ),
introduced(definition,[new_symbols(definition,[spl351_75])],[avatar_definition]) ).
fof(f23015,plain,
( k8_relset_2(sK29,sK30,sK32,sK33) = sF346
| ~ spl351_75 ),
inference(avatar_component_clause,[],[f23013]) ).
fof(f23016,plain,
spl351_75,
inference(avatar_split_clause,[],[f22620,f23013]) ).
fof(f23018,definition,
( spl351_76
<=> k5_subset_1(sK30,sF345,sF346) = sF347 ),
introduced(definition,[new_symbols(definition,[spl351_76])],[avatar_definition]) ).
fof(f23020,plain,
( k5_subset_1(sK30,sF345,sF346) = sF347
| ~ spl351_76 ),
inference(avatar_component_clause,[],[f23018]) ).
fof(f23021,plain,
spl351_76,
inference(avatar_split_clause,[],[f22622,f23018]) ).
fof(f23023,definition,
( spl351_77
<=> k2_zfmisc_1(sK29,sK30) = sF348 ),
introduced(definition,[new_symbols(definition,[spl351_77])],[avatar_definition]) ).
fof(f23025,plain,
( k2_zfmisc_1(sK29,sK30) = sF348
| ~ spl351_77 ),
inference(avatar_component_clause,[],[f23023]) ).
fof(f23026,plain,
spl351_77,
inference(avatar_split_clause,[],[f22625,f23023]) ).
fof(f23028,definition,
( spl351_78
<=> k1_zfmisc_1(sF348) = sF349 ),
introduced(definition,[new_symbols(definition,[spl351_78])],[avatar_definition]) ).
fof(f23030,plain,
( k1_zfmisc_1(sF348) = sF349
| ~ spl351_78 ),
inference(avatar_component_clause,[],[f23028]) ).
fof(f23031,plain,
spl351_78,
inference(avatar_split_clause,[],[f22627,f23028]) ).
fof(f23033,definition,
( spl351_79
<=> k1_zfmisc_1(sK29) = sF350 ),
introduced(definition,[new_symbols(definition,[spl351_79])],[avatar_definition]) ).
fof(f23035,plain,
( k1_zfmisc_1(sK29) = sF350
| ~ spl351_79 ),
inference(avatar_component_clause,[],[f23033]) ).
fof(f23036,plain,
spl351_79,
inference(avatar_split_clause,[],[f22630,f23033]) ).
fof(f23037,plain,
( m1_subset_1(sF344,k1_zfmisc_1(sK30))
| ~ m1_subset_1(sF343,k1_zfmisc_1(sK29))
| ~ m1_subset_1(sK33,k1_zfmisc_1(k2_zfmisc_1(sK29,sK30)))
| ~ spl351_73 ),
inference(superposition,[],[f20793,f23005]) ).
fof(f23039,definition,
( spl351_80
<=> m1_subset_1(sK33,k1_zfmisc_1(k2_zfmisc_1(sK29,sK30))) ),
introduced(definition,[new_symbols(definition,[spl351_80])],[avatar_definition]) ).
fof(f23043,definition,
( spl351_81
<=> m1_subset_1(sF343,k1_zfmisc_1(sK29)) ),
introduced(definition,[new_symbols(definition,[spl351_81])],[avatar_definition]) ).
fof(f23047,definition,
( spl351_82
<=> m1_subset_1(sF344,k1_zfmisc_1(sK30)) ),
introduced(definition,[new_symbols(definition,[spl351_82])],[avatar_definition]) ).
fof(f23049,plain,
( m1_subset_1(sF344,k1_zfmisc_1(sK30))
| ~ spl351_82 ),
inference(avatar_component_clause,[],[f23047]) ).
fof(f23050,plain,
( ~ spl351_80
| ~ spl351_81
| spl351_82
| ~ spl351_73 ),
inference(avatar_split_clause,[],[f23037,f23003,f23047,f23043,f23039]) ).
fof(f23051,plain,
( k2_zfmisc_1(sK29,sK30) != sF348
| k1_zfmisc_1(sF348) != sF349
| m1_subset_1(sK33,k1_zfmisc_1(k2_zfmisc_1(sK29,sK30)))
| ~ m1_subset_1(sK33,sF349) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f23052,plain,
( m1_subset_1(sF345,k1_zfmisc_1(sK30))
| ~ m1_subset_1(sK31,k1_zfmisc_1(sK29))
| ~ m1_subset_1(sK33,k1_zfmisc_1(k2_zfmisc_1(sK29,sK30)))
| ~ spl351_74 ),
inference(superposition,[],[f20793,f23010]) ).
fof(f23054,definition,
( spl351_83
<=> m1_subset_1(sK31,k1_zfmisc_1(sK29)) ),
introduced(definition,[new_symbols(definition,[spl351_83])],[avatar_definition]) ).
fof(f23058,definition,
( spl351_84
<=> m1_subset_1(sF345,k1_zfmisc_1(sK30)) ),
introduced(definition,[new_symbols(definition,[spl351_84])],[avatar_definition]) ).
fof(f23060,plain,
( m1_subset_1(sF345,k1_zfmisc_1(sK30))
| ~ spl351_84 ),
inference(avatar_component_clause,[],[f23058]) ).
fof(f23061,plain,
( ~ spl351_80
| ~ spl351_83
| spl351_84
| ~ spl351_74 ),
inference(avatar_split_clause,[],[f23052,f23008,f23058,f23054,f23039]) ).
fof(f23062,plain,
( k1_zfmisc_1(sK29) != sF350
| m1_subset_1(sK31,k1_zfmisc_1(sK29))
| ~ m1_subset_1(sK31,sF350) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f23063,plain,
( m1_subset_1(sF346,k1_zfmisc_1(sK30))
| ~ m1_subset_1(sK32,k1_zfmisc_1(sK29))
| ~ m1_subset_1(sK33,k1_zfmisc_1(k2_zfmisc_1(sK29,sK30)))
| ~ spl351_75 ),
inference(superposition,[],[f20793,f23015]) ).
fof(f23065,definition,
( spl351_85
<=> m1_subset_1(sK32,k1_zfmisc_1(sK29)) ),
introduced(definition,[new_symbols(definition,[spl351_85])],[avatar_definition]) ).
fof(f23069,definition,
( spl351_86
<=> m1_subset_1(sF346,k1_zfmisc_1(sK30)) ),
introduced(definition,[new_symbols(definition,[spl351_86])],[avatar_definition]) ).
fof(f23071,plain,
( m1_subset_1(sF346,k1_zfmisc_1(sK30))
| ~ spl351_86 ),
inference(avatar_component_clause,[],[f23069]) ).
fof(f23072,plain,
( ~ spl351_80
| ~ spl351_85
| spl351_86
| ~ spl351_75 ),
inference(avatar_split_clause,[],[f23063,f23013,f23069,f23065,f23039]) ).
fof(f23073,plain,
( k1_zfmisc_1(sK29) != sF350
| m1_subset_1(sK32,k1_zfmisc_1(sK29))
| ~ m1_subset_1(sK32,sF350) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f23080,plain,
( sF347 = k3_xboole_0(sF345,sF346)
| ~ m1_subset_1(sF345,k1_zfmisc_1(sK30))
| ~ m1_subset_1(sF346,k1_zfmisc_1(sK30))
| ~ spl351_76 ),
inference(superposition,[],[f20780,f23020]) ).
fof(f23083,definition,
( spl351_87
<=> sF347 = k3_xboole_0(sF345,sF346) ),
introduced(definition,[new_symbols(definition,[spl351_87])],[avatar_definition]) ).
fof(f23085,plain,
( sF347 = k3_xboole_0(sF345,sF346)
| ~ spl351_87 ),
inference(avatar_component_clause,[],[f23083]) ).
fof(f23087,plain,
( ~ spl351_86
| ~ spl351_84
| spl351_87
| ~ spl351_76 ),
inference(avatar_split_clause,[],[f23080,f23018,f23083,f23058,f23069]) ).
fof(f23089,plain,
! [X2,X0,X1] :
( k3_xboole_0(X0,X1) = k5_subset_1(X2,X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ m1_subset_1(X0,k1_zfmisc_1(X2))
| ~ m1_subset_1(X0,k1_zfmisc_1(X2))
| ~ m1_subset_1(X1,k1_zfmisc_1(X2)) ),
inference(superposition,[],[f20782,f20780]) ).
fof(f23094,plain,
! [X2,X0,X1] :
( k3_xboole_0(X0,X1) = k5_subset_1(X2,X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ m1_subset_1(X0,k1_zfmisc_1(X2)) ),
inference(duplicate_literal_removal,[],[f23089]) ).
fof(f23097,plain,
( sF343 = k2_xboole_0(sK31,sK32)
| ~ m1_subset_1(sK31,k1_zfmisc_1(sK29))
| ~ m1_subset_1(sK32,k1_zfmisc_1(sK29))
| ~ spl351_72 ),
inference(superposition,[],[f23000,f20758]) ).
fof(f23098,plain,
( ~ m1_subset_1(sK31,sF350)
| sF343 = k2_xboole_0(sK31,sK32)
| ~ m1_subset_1(sK32,k1_zfmisc_1(sK29))
| ~ spl351_72
| ~ spl351_79 ),
inference(forward_demodulation,[],[f23097,f23035]) ).
fof(f23100,plain,
( sF343 = k2_xboole_0(sK31,sK32)
| ~ m1_subset_1(sK32,k1_zfmisc_1(sK29))
| ~ spl351_68
| ~ spl351_72
| ~ spl351_79 ),
inference(forward_subsumption_resolution,[],[f23098,f22980]) ).
fof(f23102,plain,
( ~ m1_subset_1(sK32,sF350)
| sF343 = k2_xboole_0(sK31,sK32)
| ~ spl351_68
| ~ spl351_72
| ~ spl351_79 ),
inference(forward_demodulation,[],[f23100,f23035]) ).
fof(f23104,plain,
( sF343 = k2_xboole_0(sK31,sK32)
| ~ spl351_68
| ~ spl351_69
| ~ spl351_72
| ~ spl351_79 ),
inference(forward_subsumption_resolution,[],[f23102,f22985]) ).
fof(f23107,definition,
( spl351_88
<=> sF343 = k2_xboole_0(sK31,sK32) ),
introduced(definition,[new_symbols(definition,[spl351_88])],[avatar_definition]) ).
fof(f23109,plain,
( sF343 = k2_xboole_0(sK31,sK32)
| ~ spl351_88 ),
inference(avatar_component_clause,[],[f23107]) ).
fof(f23110,plain,
( spl351_88
| ~ spl351_68
| ~ spl351_69
| ~ spl351_72
| ~ spl351_79 ),
inference(avatar_split_clause,[],[f23104,f23033,f22998,f22983,f22978,f23107]) ).
fof(f23112,plain,
( m1_subset_1(sF347,k1_zfmisc_1(sK30))
| ~ m1_subset_1(sF345,k1_zfmisc_1(sK30))
| ~ m1_subset_1(sF346,k1_zfmisc_1(sK30))
| ~ spl351_76 ),
inference(superposition,[],[f20783,f23020]) ).
fof(f23121,plain,
( m1_subset_1(sF347,k1_zfmisc_1(sK30))
| ~ m1_subset_1(sF346,k1_zfmisc_1(sK30))
| ~ spl351_76
| ~ spl351_84 ),
inference(forward_subsumption_resolution,[],[f23112,f23060]) ).
fof(f23122,plain,
( m1_subset_1(sF347,k1_zfmisc_1(sK30))
| ~ spl351_76
| ~ spl351_84
| ~ spl351_86 ),
inference(forward_subsumption_resolution,[],[f23121,f23071]) ).
fof(f23124,definition,
( spl351_89
<=> m1_subset_1(sF347,k1_zfmisc_1(sK30)) ),
introduced(definition,[new_symbols(definition,[spl351_89])],[avatar_definition]) ).
fof(f23126,plain,
( m1_subset_1(sF347,k1_zfmisc_1(sK30))
| ~ spl351_89 ),
inference(avatar_component_clause,[],[f23124]) ).
fof(f23127,plain,
( spl351_89
| ~ spl351_76
| ~ spl351_84
| ~ spl351_86 ),
inference(avatar_split_clause,[],[f23122,f23069,f23058,f23018,f23124]) ).
fof(f23128,plain,
! [X2,X0,X1] :
( k2_xboole_0(X0,X1) = k4_subset_1(X2,X1,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(X2))
| ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ m1_subset_1(X0,k1_zfmisc_1(X2))
| ~ m1_subset_1(X1,k1_zfmisc_1(X2)) ),
inference(superposition,[],[f20760,f20758]) ).
fof(f23135,plain,
! [X2,X0,X1] :
( k2_xboole_0(X0,X1) = k4_subset_1(X2,X1,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(X2))
| ~ m1_subset_1(X1,k1_zfmisc_1(X2)) ),
inference(duplicate_literal_removal,[],[f23128]) ).
fof(f23137,plain,
! [X2,X3,X0,X1,X4] :
( ~ r2_hidden(X0,k8_relset_2(X1,X2,X3,X4))
| m1_subset_1(X0,X2)
| ~ m1_subset_1(X3,k1_zfmisc_1(X1))
| ~ m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X1,X2))) ),
inference(resolution,[],[f21165,f20793]) ).
fof(f23151,plain,
( m1_subset_1(sF343,k1_zfmisc_1(sK29))
| ~ m1_subset_1(sK31,k1_zfmisc_1(sK29))
| ~ m1_subset_1(sK32,k1_zfmisc_1(sK29))
| ~ spl351_72 ),
inference(superposition,[],[f20761,f23000]) ).
fof(f23160,plain,
( m1_subset_1(sF343,sF350)
| ~ m1_subset_1(sK31,k1_zfmisc_1(sK29))
| ~ m1_subset_1(sK32,k1_zfmisc_1(sK29))
| ~ spl351_72
| ~ spl351_79 ),
inference(forward_demodulation,[],[f23151,f23035]) ).
fof(f23161,plain,
( ~ m1_subset_1(sK31,sF350)
| m1_subset_1(sF343,sF350)
| ~ m1_subset_1(sK32,k1_zfmisc_1(sK29))
| ~ spl351_72
| ~ spl351_79 ),
inference(forward_demodulation,[],[f23160,f23035]) ).
fof(f23162,plain,
( m1_subset_1(sF343,sF350)
| ~ m1_subset_1(sK32,k1_zfmisc_1(sK29))
| ~ spl351_68
| ~ spl351_72
| ~ spl351_79 ),
inference(forward_subsumption_resolution,[],[f23161,f22980]) ).
fof(f23163,plain,
( ~ m1_subset_1(sK32,sF350)
| m1_subset_1(sF343,sF350)
| ~ spl351_68
| ~ spl351_72
| ~ spl351_79 ),
inference(forward_demodulation,[],[f23162,f23035]) ).
fof(f23164,plain,
( m1_subset_1(sF343,sF350)
| ~ spl351_68
| ~ spl351_69
| ~ spl351_72
| ~ spl351_79 ),
inference(forward_subsumption_resolution,[],[f23163,f22985]) ).
fof(f23166,definition,
( spl351_91
<=> m1_subset_1(sF343,sF350) ),
introduced(definition,[new_symbols(definition,[spl351_91])],[avatar_definition]) ).
fof(f23168,plain,
( m1_subset_1(sF343,sF350)
| ~ spl351_91 ),
inference(avatar_component_clause,[],[f23166]) ).
fof(f23169,plain,
( spl351_91
| ~ spl351_68
| ~ spl351_69
| ~ spl351_72
| ~ spl351_79 ),
inference(avatar_split_clause,[],[f23164,f23033,f22998,f22983,f22978,f23166]) ).
fof(f23170,plain,
( k1_zfmisc_1(sK29) != sF350
| m1_subset_1(sF343,k1_zfmisc_1(sK29))
| ~ m1_subset_1(sF343,sF350) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f23177,plain,
( ! [X0,X1] :
( ~ r2_hidden(X0,sF344)
| ~ r2_hidden(X1,sF343)
| r2_hidden(X0,k9_relat_1(sK33,k1_tarski(X1)))
| ~ m1_subset_1(sK33,k1_zfmisc_1(k2_zfmisc_1(sK29,sK30)))
| ~ m1_subset_1(sF343,k1_zfmisc_1(sK29)) )
| ~ spl351_73 ),
inference(superposition,[],[f20792,f23005]) ).
fof(f23178,plain,
( ! [X0,X1] :
( ~ r2_hidden(X0,sF345)
| ~ r2_hidden(X1,sK31)
| r2_hidden(X0,k9_relat_1(sK33,k1_tarski(X1)))
| ~ m1_subset_1(sK33,k1_zfmisc_1(k2_zfmisc_1(sK29,sK30)))
| ~ m1_subset_1(sK31,k1_zfmisc_1(sK29)) )
| ~ spl351_74 ),
inference(superposition,[],[f20792,f23010]) ).
fof(f23179,plain,
( ! [X0,X1] :
( ~ r2_hidden(X0,sF346)
| ~ r2_hidden(X1,sK32)
| r2_hidden(X0,k9_relat_1(sK33,k1_tarski(X1)))
| ~ m1_subset_1(sK33,k1_zfmisc_1(k2_zfmisc_1(sK29,sK30)))
| ~ m1_subset_1(sK32,k1_zfmisc_1(sK29)) )
| ~ spl351_75 ),
inference(superposition,[],[f20792,f23015]) ).
fof(f23180,plain,
( ! [X0,X1] :
( ~ m1_subset_1(sK33,k1_zfmisc_1(sF348))
| ~ r2_hidden(X0,sF346)
| ~ r2_hidden(X1,sK32)
| r2_hidden(X0,k9_relat_1(sK33,k1_tarski(X1)))
| ~ m1_subset_1(sK32,k1_zfmisc_1(sK29)) )
| ~ spl351_75
| ~ spl351_77 ),
inference(forward_demodulation,[],[f23179,f23025]) ).
fof(f23181,plain,
( ! [X0,X1] :
( ~ m1_subset_1(sK33,k1_zfmisc_1(sF348))
| ~ r2_hidden(X0,sF345)
| ~ r2_hidden(X1,sK31)
| r2_hidden(X0,k9_relat_1(sK33,k1_tarski(X1)))
| ~ m1_subset_1(sK31,k1_zfmisc_1(sK29)) )
| ~ spl351_74
| ~ spl351_77 ),
inference(forward_demodulation,[],[f23178,f23025]) ).
fof(f23182,plain,
( ! [X0,X1] :
( ~ m1_subset_1(sK33,k1_zfmisc_1(sF348))
| ~ r2_hidden(X0,sF344)
| ~ r2_hidden(X1,sF343)
| r2_hidden(X0,k9_relat_1(sK33,k1_tarski(X1)))
| ~ m1_subset_1(sF343,k1_zfmisc_1(sK29)) )
| ~ spl351_73
| ~ spl351_77 ),
inference(forward_demodulation,[],[f23177,f23025]) ).
fof(f23183,plain,
( ! [X0,X1] :
( ~ m1_subset_1(sK33,sF349)
| ~ r2_hidden(X0,sF346)
| ~ r2_hidden(X1,sK32)
| r2_hidden(X0,k9_relat_1(sK33,k1_tarski(X1)))
| ~ m1_subset_1(sK32,k1_zfmisc_1(sK29)) )
| ~ spl351_75
| ~ spl351_77
| ~ spl351_78 ),
inference(forward_demodulation,[],[f23180,f23030]) ).
fof(f23184,plain,
( ! [X0,X1] :
( ~ m1_subset_1(sK33,sF349)
| ~ r2_hidden(X0,sF345)
| ~ r2_hidden(X1,sK31)
| r2_hidden(X0,k9_relat_1(sK33,k1_tarski(X1)))
| ~ m1_subset_1(sK31,k1_zfmisc_1(sK29)) )
| ~ spl351_74
| ~ spl351_77
| ~ spl351_78 ),
inference(forward_demodulation,[],[f23181,f23030]) ).
fof(f23185,plain,
( ! [X0,X1] :
( ~ m1_subset_1(sK33,sF349)
| ~ r2_hidden(X0,sF344)
| ~ r2_hidden(X1,sF343)
| r2_hidden(X0,k9_relat_1(sK33,k1_tarski(X1)))
| ~ m1_subset_1(sF343,k1_zfmisc_1(sK29)) )
| ~ spl351_73
| ~ spl351_77
| ~ spl351_78 ),
inference(forward_demodulation,[],[f23182,f23030]) ).
fof(f23186,plain,
( ! [X0,X1] :
( ~ r2_hidden(X0,sF346)
| ~ r2_hidden(X1,sK32)
| r2_hidden(X0,k9_relat_1(sK33,k1_tarski(X1)))
| ~ m1_subset_1(sK32,k1_zfmisc_1(sK29)) )
| ~ spl351_70
| ~ spl351_75
| ~ spl351_77
| ~ spl351_78 ),
inference(forward_subsumption_resolution,[],[f23183,f22990]) ).
fof(f23187,plain,
( ! [X0,X1] :
( ~ r2_hidden(X0,sF345)
| ~ r2_hidden(X1,sK31)
| r2_hidden(X0,k9_relat_1(sK33,k1_tarski(X1)))
| ~ m1_subset_1(sK31,k1_zfmisc_1(sK29)) )
| ~ spl351_70
| ~ spl351_74
| ~ spl351_77
| ~ spl351_78 ),
inference(forward_subsumption_resolution,[],[f23184,f22990]) ).
fof(f23188,plain,
( ! [X0,X1] :
( ~ r2_hidden(X0,sF344)
| ~ r2_hidden(X1,sF343)
| r2_hidden(X0,k9_relat_1(sK33,k1_tarski(X1)))
| ~ m1_subset_1(sF343,k1_zfmisc_1(sK29)) )
| ~ spl351_70
| ~ spl351_73
| ~ spl351_77
| ~ spl351_78 ),
inference(forward_subsumption_resolution,[],[f23185,f22990]) ).
fof(f23189,plain,
( ! [X0,X1] :
( ~ m1_subset_1(sK32,sF350)
| ~ r2_hidden(X0,sF346)
| ~ r2_hidden(X1,sK32)
| r2_hidden(X0,k9_relat_1(sK33,k1_tarski(X1))) )
| ~ spl351_70
| ~ spl351_75
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79 ),
inference(forward_demodulation,[],[f23186,f23035]) ).
fof(f23190,plain,
( ! [X0,X1] :
( ~ m1_subset_1(sK31,sF350)
| ~ r2_hidden(X0,sF345)
| ~ r2_hidden(X1,sK31)
| r2_hidden(X0,k9_relat_1(sK33,k1_tarski(X1))) )
| ~ spl351_70
| ~ spl351_74
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79 ),
inference(forward_demodulation,[],[f23187,f23035]) ).
fof(f23191,plain,
( ! [X0,X1] :
( ~ m1_subset_1(sF343,sF350)
| ~ r2_hidden(X0,sF344)
| ~ r2_hidden(X1,sF343)
| r2_hidden(X0,k9_relat_1(sK33,k1_tarski(X1))) )
| ~ spl351_70
| ~ spl351_73
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79 ),
inference(forward_demodulation,[],[f23188,f23035]) ).
fof(f23192,plain,
( ! [X0,X1] :
( r2_hidden(X0,k9_relat_1(sK33,k1_tarski(X1)))
| ~ r2_hidden(X1,sK32)
| ~ r2_hidden(X0,sF346) )
| ~ spl351_69
| ~ spl351_70
| ~ spl351_75
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79 ),
inference(forward_subsumption_resolution,[],[f23189,f22985]) ).
fof(f23193,plain,
( ! [X0,X1] :
( r2_hidden(X0,k9_relat_1(sK33,k1_tarski(X1)))
| ~ r2_hidden(X1,sK31)
| ~ r2_hidden(X0,sF345) )
| ~ spl351_68
| ~ spl351_70
| ~ spl351_74
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79 ),
inference(forward_subsumption_resolution,[],[f23190,f22980]) ).
fof(f23194,plain,
( ! [X0,X1] :
( r2_hidden(X0,k9_relat_1(sK33,k1_tarski(X1)))
| ~ r2_hidden(X1,sF343)
| ~ r2_hidden(X0,sF344) )
| ~ spl351_70
| ~ spl351_73
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79
| ~ spl351_91 ),
inference(forward_subsumption_resolution,[],[f23191,f23168]) ).
fof(f23233,plain,
( sF347 = k3_xboole_0(sF346,sF345)
| ~ m1_subset_1(sF345,k1_zfmisc_1(sK30))
| ~ m1_subset_1(sF346,k1_zfmisc_1(sK30))
| ~ spl351_76 ),
inference(superposition,[],[f23020,f23094]) ).
fof(f23245,plain,
( sF347 = k3_xboole_0(sF346,sF345)
| ~ m1_subset_1(sF346,k1_zfmisc_1(sK30))
| ~ spl351_76
| ~ spl351_84 ),
inference(forward_subsumption_resolution,[],[f23233,f23060]) ).
fof(f23247,plain,
( sF347 = k3_xboole_0(sF346,sF345)
| ~ spl351_76
| ~ spl351_84
| ~ spl351_86 ),
inference(forward_subsumption_resolution,[],[f23245,f23071]) ).
fof(f23250,definition,
( spl351_92
<=> sF347 = k3_xboole_0(sF346,sF345) ),
introduced(definition,[new_symbols(definition,[spl351_92])],[avatar_definition]) ).
fof(f23252,plain,
( sF347 = k3_xboole_0(sF346,sF345)
| ~ spl351_92 ),
inference(avatar_component_clause,[],[f23250]) ).
fof(f23253,plain,
( spl351_92
| ~ spl351_76
| ~ spl351_84
| ~ spl351_86 ),
inference(avatar_split_clause,[],[f23247,f23069,f23058,f23018,f23250]) ).
fof(f23286,plain,
( sF343 = k2_xboole_0(sK32,sK31)
| ~ m1_subset_1(sK32,k1_zfmisc_1(sK29))
| ~ m1_subset_1(sK31,k1_zfmisc_1(sK29))
| ~ spl351_72 ),
inference(superposition,[],[f23000,f23135]) ).
fof(f23298,plain,
( ~ m1_subset_1(sK32,sF350)
| sF343 = k2_xboole_0(sK32,sK31)
| ~ m1_subset_1(sK31,k1_zfmisc_1(sK29))
| ~ spl351_72
| ~ spl351_79 ),
inference(forward_demodulation,[],[f23286,f23035]) ).
fof(f23300,plain,
( sF343 = k2_xboole_0(sK32,sK31)
| ~ m1_subset_1(sK31,k1_zfmisc_1(sK29))
| ~ spl351_69
| ~ spl351_72
| ~ spl351_79 ),
inference(forward_subsumption_resolution,[],[f23298,f22985]) ).
fof(f23302,plain,
( ~ m1_subset_1(sK31,sF350)
| sF343 = k2_xboole_0(sK32,sK31)
| ~ spl351_69
| ~ spl351_72
| ~ spl351_79 ),
inference(forward_demodulation,[],[f23300,f23035]) ).
fof(f23304,plain,
( sF343 = k2_xboole_0(sK32,sK31)
| ~ spl351_68
| ~ spl351_69
| ~ spl351_72
| ~ spl351_79 ),
inference(forward_subsumption_resolution,[],[f23302,f22980]) ).
fof(f23307,definition,
( spl351_95
<=> sF343 = k2_xboole_0(sK32,sK31) ),
introduced(definition,[new_symbols(definition,[spl351_95])],[avatar_definition]) ).
fof(f23309,plain,
( sF343 = k2_xboole_0(sK32,sK31)
| ~ spl351_95 ),
inference(avatar_component_clause,[],[f23307]) ).
fof(f23310,plain,
( spl351_95
| ~ spl351_68
| ~ spl351_69
| ~ spl351_72
| ~ spl351_79 ),
inference(avatar_split_clause,[],[f23304,f23033,f22998,f22983,f22978,f23307]) ).
fof(f23315,plain,
( ! [X0] :
( r2_hidden(X0,sF344)
| r2_hidden(sK37(sF343,X0,sK33),sF343)
| ~ m1_subset_1(sK33,k1_zfmisc_1(k2_zfmisc_1(sK29,sK30)))
| ~ m1_subset_1(X0,sK30)
| ~ m1_subset_1(sF343,k1_zfmisc_1(sK29))
| v1_xboole_0(sK30) )
| ~ spl351_73 ),
inference(superposition,[],[f20790,f23005]) ).
fof(f23316,plain,
( ! [X0] :
( r2_hidden(X0,sF345)
| r2_hidden(sK37(sK31,X0,sK33),sK31)
| ~ m1_subset_1(sK33,k1_zfmisc_1(k2_zfmisc_1(sK29,sK30)))
| ~ m1_subset_1(X0,sK30)
| ~ m1_subset_1(sK31,k1_zfmisc_1(sK29))
| v1_xboole_0(sK30) )
| ~ spl351_74 ),
inference(superposition,[],[f20790,f23010]) ).
fof(f23317,plain,
( ! [X0] :
( r2_hidden(X0,sF346)
| r2_hidden(sK37(sK32,X0,sK33),sK32)
| ~ m1_subset_1(sK33,k1_zfmisc_1(k2_zfmisc_1(sK29,sK30)))
| ~ m1_subset_1(X0,sK30)
| ~ m1_subset_1(sK32,k1_zfmisc_1(sK29))
| v1_xboole_0(sK30) )
| ~ spl351_75 ),
inference(superposition,[],[f20790,f23015]) ).
fof(f23319,plain,
( ! [X0] :
( ~ m1_subset_1(sK33,k1_zfmisc_1(sF348))
| r2_hidden(X0,sF346)
| r2_hidden(sK37(sK32,X0,sK33),sK32)
| ~ m1_subset_1(X0,sK30)
| ~ m1_subset_1(sK32,k1_zfmisc_1(sK29))
| v1_xboole_0(sK30) )
| ~ spl351_75
| ~ spl351_77 ),
inference(forward_demodulation,[],[f23317,f23025]) ).
fof(f23320,plain,
( ! [X0] :
( ~ m1_subset_1(sK33,k1_zfmisc_1(sF348))
| r2_hidden(X0,sF345)
| r2_hidden(sK37(sK31,X0,sK33),sK31)
| ~ m1_subset_1(X0,sK30)
| ~ m1_subset_1(sK31,k1_zfmisc_1(sK29))
| v1_xboole_0(sK30) )
| ~ spl351_74
| ~ spl351_77 ),
inference(forward_demodulation,[],[f23316,f23025]) ).
fof(f23321,plain,
( ! [X0] :
( ~ m1_subset_1(sK33,k1_zfmisc_1(sF348))
| r2_hidden(X0,sF344)
| r2_hidden(sK37(sF343,X0,sK33),sF343)
| ~ m1_subset_1(X0,sK30)
| ~ m1_subset_1(sF343,k1_zfmisc_1(sK29))
| v1_xboole_0(sK30) )
| ~ spl351_73
| ~ spl351_77 ),
inference(forward_demodulation,[],[f23315,f23025]) ).
fof(f23322,plain,
( ! [X0] :
( ~ m1_subset_1(sK33,sF349)
| r2_hidden(X0,sF346)
| r2_hidden(sK37(sK32,X0,sK33),sK32)
| ~ m1_subset_1(X0,sK30)
| ~ m1_subset_1(sK32,k1_zfmisc_1(sK29))
| v1_xboole_0(sK30) )
| ~ spl351_75
| ~ spl351_77
| ~ spl351_78 ),
inference(forward_demodulation,[],[f23319,f23030]) ).
fof(f23323,plain,
( ! [X0] :
( ~ m1_subset_1(sK33,sF349)
| r2_hidden(X0,sF345)
| r2_hidden(sK37(sK31,X0,sK33),sK31)
| ~ m1_subset_1(X0,sK30)
| ~ m1_subset_1(sK31,k1_zfmisc_1(sK29))
| v1_xboole_0(sK30) )
| ~ spl351_74
| ~ spl351_77
| ~ spl351_78 ),
inference(forward_demodulation,[],[f23320,f23030]) ).
fof(f23324,plain,
( ! [X0] :
( ~ m1_subset_1(sK33,sF349)
| r2_hidden(X0,sF344)
| r2_hidden(sK37(sF343,X0,sK33),sF343)
| ~ m1_subset_1(X0,sK30)
| ~ m1_subset_1(sF343,k1_zfmisc_1(sK29))
| v1_xboole_0(sK30) )
| ~ spl351_73
| ~ spl351_77
| ~ spl351_78 ),
inference(forward_demodulation,[],[f23321,f23030]) ).
fof(f23325,plain,
( ! [X0] :
( r2_hidden(X0,sF346)
| r2_hidden(sK37(sK32,X0,sK33),sK32)
| ~ m1_subset_1(X0,sK30)
| ~ m1_subset_1(sK32,k1_zfmisc_1(sK29))
| v1_xboole_0(sK30) )
| ~ spl351_70
| ~ spl351_75
| ~ spl351_77
| ~ spl351_78 ),
inference(forward_subsumption_resolution,[],[f23322,f22990]) ).
fof(f23326,plain,
( ! [X0] :
( r2_hidden(X0,sF345)
| r2_hidden(sK37(sK31,X0,sK33),sK31)
| ~ m1_subset_1(X0,sK30)
| ~ m1_subset_1(sK31,k1_zfmisc_1(sK29))
| v1_xboole_0(sK30) )
| ~ spl351_70
| ~ spl351_74
| ~ spl351_77
| ~ spl351_78 ),
inference(forward_subsumption_resolution,[],[f23323,f22990]) ).
fof(f23327,plain,
( ! [X0] :
( r2_hidden(X0,sF344)
| r2_hidden(sK37(sF343,X0,sK33),sF343)
| ~ m1_subset_1(X0,sK30)
| ~ m1_subset_1(sF343,k1_zfmisc_1(sK29))
| v1_xboole_0(sK30) )
| ~ spl351_70
| ~ spl351_73
| ~ spl351_77
| ~ spl351_78 ),
inference(forward_subsumption_resolution,[],[f23324,f22990]) ).
fof(f23328,plain,
( ! [X0] :
( ~ m1_subset_1(sK32,sF350)
| r2_hidden(X0,sF346)
| r2_hidden(sK37(sK32,X0,sK33),sK32)
| ~ m1_subset_1(X0,sK30)
| v1_xboole_0(sK30) )
| ~ spl351_70
| ~ spl351_75
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79 ),
inference(forward_demodulation,[],[f23325,f23035]) ).
fof(f23329,plain,
( ! [X0] :
( ~ m1_subset_1(sK31,sF350)
| r2_hidden(X0,sF345)
| r2_hidden(sK37(sK31,X0,sK33),sK31)
| ~ m1_subset_1(X0,sK30)
| v1_xboole_0(sK30) )
| ~ spl351_70
| ~ spl351_74
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79 ),
inference(forward_demodulation,[],[f23326,f23035]) ).
fof(f23330,plain,
( ! [X0] :
( ~ m1_subset_1(sF343,sF350)
| r2_hidden(X0,sF344)
| r2_hidden(sK37(sF343,X0,sK33),sF343)
| ~ m1_subset_1(X0,sK30)
| v1_xboole_0(sK30) )
| ~ spl351_70
| ~ spl351_73
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79 ),
inference(forward_demodulation,[],[f23327,f23035]) ).
fof(f23331,plain,
( ! [X0] :
( r2_hidden(X0,sF346)
| r2_hidden(sK37(sK32,X0,sK33),sK32)
| ~ m1_subset_1(X0,sK30)
| v1_xboole_0(sK30) )
| ~ spl351_69
| ~ spl351_70
| ~ spl351_75
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79 ),
inference(forward_subsumption_resolution,[],[f23328,f22985]) ).
fof(f23332,plain,
( ! [X0] :
( r2_hidden(X0,sF345)
| r2_hidden(sK37(sK31,X0,sK33),sK31)
| ~ m1_subset_1(X0,sK30)
| v1_xboole_0(sK30) )
| ~ spl351_68
| ~ spl351_70
| ~ spl351_74
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79 ),
inference(forward_subsumption_resolution,[],[f23329,f22980]) ).
fof(f23333,plain,
( ! [X0] :
( r2_hidden(X0,sF344)
| r2_hidden(sK37(sF343,X0,sK33),sF343)
| ~ m1_subset_1(X0,sK30)
| v1_xboole_0(sK30) )
| ~ spl351_70
| ~ spl351_73
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79
| ~ spl351_91 ),
inference(forward_subsumption_resolution,[],[f23330,f23168]) ).
fof(f23335,definition,
( spl351_96
<=> v1_xboole_0(sK30) ),
introduced(definition,[new_symbols(definition,[spl351_96])],[avatar_definition]) ).
fof(f23337,plain,
( v1_xboole_0(sK30)
| ~ spl351_96 ),
inference(avatar_component_clause,[],[f23335]) ).
fof(f23339,definition,
( spl351_97
<=> ! [X0] :
( r2_hidden(X0,sF346)
| ~ m1_subset_1(X0,sK30)
| r2_hidden(sK37(sK32,X0,sK33),sK32) ) ),
introduced(definition,[new_symbols(definition,[spl351_97])],[avatar_definition]) ).
fof(f23340,plain,
( ! [X0] :
( r2_hidden(sK37(sK32,X0,sK33),sK32)
| ~ m1_subset_1(X0,sK30)
| r2_hidden(X0,sF346) )
| ~ spl351_97 ),
inference(avatar_component_clause,[],[f23339]) ).
fof(f23341,plain,
( spl351_96
| spl351_97
| ~ spl351_69
| ~ spl351_70
| ~ spl351_75
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79 ),
inference(avatar_split_clause,[],[f23331,f23033,f23028,f23023,f23013,f22988,f22983,f23339,f23335]) ).
fof(f23343,definition,
( spl351_98
<=> ! [X0] :
( r2_hidden(X0,sF345)
| ~ m1_subset_1(X0,sK30)
| r2_hidden(sK37(sK31,X0,sK33),sK31) ) ),
introduced(definition,[new_symbols(definition,[spl351_98])],[avatar_definition]) ).
fof(f23344,plain,
( ! [X0] :
( r2_hidden(sK37(sK31,X0,sK33),sK31)
| ~ m1_subset_1(X0,sK30)
| r2_hidden(X0,sF345) )
| ~ spl351_98 ),
inference(avatar_component_clause,[],[f23343]) ).
fof(f23345,plain,
( spl351_96
| spl351_98
| ~ spl351_68
| ~ spl351_70
| ~ spl351_74
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79 ),
inference(avatar_split_clause,[],[f23332,f23033,f23028,f23023,f23008,f22988,f22978,f23343,f23335]) ).
fof(f23347,definition,
( spl351_99
<=> ! [X0] :
( r2_hidden(X0,sF344)
| ~ m1_subset_1(X0,sK30)
| r2_hidden(sK37(sF343,X0,sK33),sF343) ) ),
introduced(definition,[new_symbols(definition,[spl351_99])],[avatar_definition]) ).
fof(f23348,plain,
( ! [X0] :
( r2_hidden(sK37(sF343,X0,sK33),sF343)
| ~ m1_subset_1(X0,sK30)
| r2_hidden(X0,sF344) )
| ~ spl351_99 ),
inference(avatar_component_clause,[],[f23347]) ).
fof(f23349,plain,
( spl351_96
| spl351_99
| ~ spl351_70
| ~ spl351_73
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79
| ~ spl351_91 ),
inference(avatar_split_clause,[],[f23333,f23166,f23033,f23028,f23023,f23003,f22988,f23347,f23335]) ).
fof(f23369,plain,
( ! [X2,X3,X0,X1] :
( r2_hidden(X0,k8_relset_2(X1,X2,X3,sK33))
| ~ m1_subset_1(sK33,k1_zfmisc_1(k2_zfmisc_1(X1,X2)))
| ~ m1_subset_1(X0,X2)
| ~ m1_subset_1(X3,k1_zfmisc_1(X1))
| v1_xboole_0(X2)
| ~ r2_hidden(sK37(X3,X0,sK33),sF343)
| ~ r2_hidden(X0,sF344) )
| ~ spl351_70
| ~ spl351_73
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79
| ~ spl351_91 ),
inference(resolution,[],[f20791,f23194]) ).
fof(f23370,plain,
( ! [X2,X3,X0,X1] :
( r2_hidden(X0,k8_relset_2(X1,X2,X3,sK33))
| ~ m1_subset_1(sK33,k1_zfmisc_1(k2_zfmisc_1(X1,X2)))
| ~ m1_subset_1(X0,X2)
| ~ m1_subset_1(X3,k1_zfmisc_1(X1))
| v1_xboole_0(X2)
| ~ r2_hidden(sK37(X3,X0,sK33),sK32)
| ~ r2_hidden(X0,sF346) )
| ~ spl351_69
| ~ spl351_70
| ~ spl351_75
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79 ),
inference(resolution,[],[f20791,f23192]) ).
fof(f23371,plain,
( ! [X2,X3,X0,X1] :
( r2_hidden(X0,k8_relset_2(X1,X2,X3,sK33))
| ~ m1_subset_1(sK33,k1_zfmisc_1(k2_zfmisc_1(X1,X2)))
| ~ m1_subset_1(X0,X2)
| ~ m1_subset_1(X3,k1_zfmisc_1(X1))
| v1_xboole_0(X2)
| ~ r2_hidden(sK37(X3,X0,sK33),sK31)
| ~ r2_hidden(X0,sF345) )
| ~ spl351_68
| ~ spl351_70
| ~ spl351_74
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79 ),
inference(resolution,[],[f20791,f23193]) ).
fof(f23379,plain,
( ! [X0] :
( r2_hidden(X0,sF344)
| ~ m1_subset_1(sK33,k1_zfmisc_1(k2_zfmisc_1(sK29,sK30)))
| ~ m1_subset_1(X0,sK30)
| ~ m1_subset_1(sF343,k1_zfmisc_1(sK29))
| v1_xboole_0(sK30)
| ~ r2_hidden(sK37(sF343,X0,sK33),sK31)
| ~ r2_hidden(X0,sF345) )
| ~ spl351_68
| ~ spl351_70
| ~ spl351_73
| ~ spl351_74
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79 ),
inference(superposition,[],[f23371,f23005]) ).
fof(f23387,plain,
( ! [X0] :
( r2_hidden(X0,sF344)
| ~ m1_subset_1(sK33,k1_zfmisc_1(k2_zfmisc_1(sK29,sK30)))
| ~ m1_subset_1(X0,sK30)
| ~ m1_subset_1(sF343,k1_zfmisc_1(sK29))
| v1_xboole_0(sK30)
| ~ r2_hidden(sK37(sF343,X0,sK33),sK32)
| ~ r2_hidden(X0,sF346) )
| ~ spl351_69
| ~ spl351_70
| ~ spl351_73
| ~ spl351_75
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79 ),
inference(superposition,[],[f23370,f23005]) ).
fof(f23396,plain,
( ! [X0] :
( r2_hidden(X0,sF345)
| ~ m1_subset_1(sK33,k1_zfmisc_1(k2_zfmisc_1(sK29,sK30)))
| ~ m1_subset_1(X0,sK30)
| ~ m1_subset_1(sK31,k1_zfmisc_1(sK29))
| v1_xboole_0(sK30)
| ~ r2_hidden(sK37(sK31,X0,sK33),sF343)
| ~ r2_hidden(X0,sF344) )
| ~ spl351_70
| ~ spl351_73
| ~ spl351_74
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79
| ~ spl351_91 ),
inference(superposition,[],[f23369,f23010]) ).
fof(f23397,plain,
( ! [X0] :
( r2_hidden(X0,sF346)
| ~ m1_subset_1(sK33,k1_zfmisc_1(k2_zfmisc_1(sK29,sK30)))
| ~ m1_subset_1(X0,sK30)
| ~ m1_subset_1(sK32,k1_zfmisc_1(sK29))
| v1_xboole_0(sK30)
| ~ r2_hidden(sK37(sK32,X0,sK33),sF343)
| ~ r2_hidden(X0,sF344) )
| ~ spl351_70
| ~ spl351_73
| ~ spl351_75
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79
| ~ spl351_91 ),
inference(superposition,[],[f23369,f23015]) ).
fof(f23455,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF346)
| ~ r2_hidden(X0,sF345)
| r2_hidden(X0,sF347) )
| ~ spl351_87 ),
inference(superposition,[],[f22496,f23085]) ).
fof(f23730,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF347)
| r2_hidden(X0,sF345) )
| ~ spl351_87 ),
inference(superposition,[],[f22497,f23085]) ).
fof(f23731,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF347)
| r2_hidden(X0,sF346) )
| ~ spl351_92 ),
inference(superposition,[],[f22497,f23252]) ).
fof(f23737,plain,
( ! [X0] :
( r2_hidden(sK100(X0,sF347),sF345)
| sF347 = X0
| r2_hidden(sK100(X0,sF347),X0) )
| ~ spl351_87 ),
inference(resolution,[],[f23730,f21177]) ).
fof(f23778,plain,
( ! [X0] :
( r2_hidden(sK100(X0,sF347),sF346)
| sF347 = X0
| r2_hidden(sK100(X0,sF347),X0) )
| ~ spl351_92 ),
inference(resolution,[],[f23731,f21177]) ).
fof(f24255,plain,
( ! [X0] :
( ~ r2_hidden(X0,sK32)
| r2_hidden(X0,sF343) )
| ~ spl351_88 ),
inference(superposition,[],[f22489,f23109]) ).
fof(f24256,plain,
( ! [X0] :
( ~ r2_hidden(X0,sK31)
| r2_hidden(X0,sF343) )
| ~ spl351_95 ),
inference(superposition,[],[f22489,f23309]) ).
fof(f24368,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF344)
| m1_subset_1(X0,sK30)
| ~ m1_subset_1(sF343,k1_zfmisc_1(sK29))
| ~ m1_subset_1(sK33,k1_zfmisc_1(k2_zfmisc_1(sK29,sK30))) )
| ~ spl351_73 ),
inference(superposition,[],[f23137,f23005]) ).
fof(f24369,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF345)
| m1_subset_1(X0,sK30)
| ~ m1_subset_1(sK31,k1_zfmisc_1(sK29))
| ~ m1_subset_1(sK33,k1_zfmisc_1(k2_zfmisc_1(sK29,sK30))) )
| ~ spl351_74 ),
inference(superposition,[],[f23137,f23010]) ).
fof(f24370,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF346)
| m1_subset_1(X0,sK30)
| ~ m1_subset_1(sK32,k1_zfmisc_1(sK29))
| ~ m1_subset_1(sK33,k1_zfmisc_1(k2_zfmisc_1(sK29,sK30))) )
| ~ spl351_75 ),
inference(superposition,[],[f23137,f23015]) ).
fof(f24376,plain,
( ! [X0] :
( ~ m1_subset_1(sK32,sF350)
| ~ r2_hidden(X0,sF346)
| m1_subset_1(X0,sK30)
| ~ m1_subset_1(sK33,k1_zfmisc_1(k2_zfmisc_1(sK29,sK30))) )
| ~ spl351_75
| ~ spl351_79 ),
inference(forward_demodulation,[],[f24370,f23035]) ).
fof(f24377,plain,
( ! [X0] :
( ~ m1_subset_1(sK31,sF350)
| ~ r2_hidden(X0,sF345)
| m1_subset_1(X0,sK30)
| ~ m1_subset_1(sK33,k1_zfmisc_1(k2_zfmisc_1(sK29,sK30))) )
| ~ spl351_74
| ~ spl351_79 ),
inference(forward_demodulation,[],[f24369,f23035]) ).
fof(f24378,plain,
( ! [X0] :
( ~ m1_subset_1(sF343,sF350)
| ~ r2_hidden(X0,sF344)
| m1_subset_1(X0,sK30)
| ~ m1_subset_1(sK33,k1_zfmisc_1(k2_zfmisc_1(sK29,sK30))) )
| ~ spl351_73
| ~ spl351_79 ),
inference(forward_demodulation,[],[f24368,f23035]) ).
fof(f24379,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF346)
| m1_subset_1(X0,sK30)
| ~ m1_subset_1(sK33,k1_zfmisc_1(k2_zfmisc_1(sK29,sK30))) )
| ~ spl351_69
| ~ spl351_75
| ~ spl351_79 ),
inference(forward_subsumption_resolution,[],[f24376,f22985]) ).
fof(f24380,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF345)
| m1_subset_1(X0,sK30)
| ~ m1_subset_1(sK33,k1_zfmisc_1(k2_zfmisc_1(sK29,sK30))) )
| ~ spl351_68
| ~ spl351_74
| ~ spl351_79 ),
inference(forward_subsumption_resolution,[],[f24377,f22980]) ).
fof(f24381,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF344)
| m1_subset_1(X0,sK30)
| ~ m1_subset_1(sK33,k1_zfmisc_1(k2_zfmisc_1(sK29,sK30))) )
| ~ spl351_73
| ~ spl351_79
| ~ spl351_91 ),
inference(forward_subsumption_resolution,[],[f24378,f23168]) ).
fof(f24382,plain,
( ! [X0] :
( ~ m1_subset_1(sK33,k1_zfmisc_1(sF348))
| ~ r2_hidden(X0,sF346)
| m1_subset_1(X0,sK30) )
| ~ spl351_69
| ~ spl351_75
| ~ spl351_77
| ~ spl351_79 ),
inference(forward_demodulation,[],[f24379,f23025]) ).
fof(f24383,plain,
( ! [X0] :
( ~ m1_subset_1(sK33,k1_zfmisc_1(sF348))
| ~ r2_hidden(X0,sF345)
| m1_subset_1(X0,sK30) )
| ~ spl351_68
| ~ spl351_74
| ~ spl351_77
| ~ spl351_79 ),
inference(forward_demodulation,[],[f24380,f23025]) ).
fof(f24384,plain,
( ! [X0] :
( ~ m1_subset_1(sK33,k1_zfmisc_1(sF348))
| ~ r2_hidden(X0,sF344)
| m1_subset_1(X0,sK30) )
| ~ spl351_73
| ~ spl351_77
| ~ spl351_79
| ~ spl351_91 ),
inference(forward_demodulation,[],[f24381,f23025]) ).
fof(f24385,plain,
( ! [X0] :
( ~ m1_subset_1(sK33,sF349)
| ~ r2_hidden(X0,sF346)
| m1_subset_1(X0,sK30) )
| ~ spl351_69
| ~ spl351_75
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79 ),
inference(forward_demodulation,[],[f24382,f23030]) ).
fof(f24386,plain,
( ! [X0] :
( ~ m1_subset_1(sK33,sF349)
| ~ r2_hidden(X0,sF345)
| m1_subset_1(X0,sK30) )
| ~ spl351_68
| ~ spl351_74
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79 ),
inference(forward_demodulation,[],[f24383,f23030]) ).
fof(f24387,plain,
( ! [X0] :
( ~ m1_subset_1(sK33,sF349)
| ~ r2_hidden(X0,sF344)
| m1_subset_1(X0,sK30) )
| ~ spl351_73
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79
| ~ spl351_91 ),
inference(forward_demodulation,[],[f24384,f23030]) ).
fof(f24388,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF346)
| m1_subset_1(X0,sK30) )
| ~ spl351_69
| ~ spl351_70
| ~ spl351_75
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79 ),
inference(forward_subsumption_resolution,[],[f24385,f22990]) ).
fof(f24389,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF345)
| m1_subset_1(X0,sK30) )
| ~ spl351_68
| ~ spl351_70
| ~ spl351_74
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79 ),
inference(forward_subsumption_resolution,[],[f24386,f22990]) ).
fof(f24390,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF344)
| m1_subset_1(X0,sK30) )
| ~ spl351_70
| ~ spl351_73
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79
| ~ spl351_91 ),
inference(forward_subsumption_resolution,[],[f24387,f22990]) ).
fof(f25078,definition,
( spl351_254
<=> ! [X1] : ~ r2_hidden(X1,sF344) ),
introduced(definition,[new_symbols(definition,[spl351_254])],[avatar_definition]) ).
fof(f25079,plain,
( ! [X1] : ~ r2_hidden(X1,sF344)
| ~ spl351_254 ),
inference(avatar_component_clause,[],[f25078]) ).
fof(f25157,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF344)
| ~ v1_xboole_0(sK30) )
| ~ spl351_82 ),
inference(resolution,[],[f20806,f23049]) ).
fof(f25160,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF347)
| ~ v1_xboole_0(sK30) )
| ~ spl351_89 ),
inference(resolution,[],[f20806,f23126]) ).
fof(f25175,plain,
( ! [X0] : ~ r2_hidden(X0,sF347)
| ~ spl351_89
| ~ spl351_96 ),
inference(forward_subsumption_resolution,[],[f25160,f23337]) ).
fof(f25183,plain,
( ! [X0] :
( r2_hidden(X0,sF344)
| ~ m1_subset_1(sK33,k1_zfmisc_1(k2_zfmisc_1(sK29,sK30)))
| ~ m1_subset_1(sF343,k1_zfmisc_1(sK29))
| v1_xboole_0(sK30)
| ~ r2_hidden(sK37(sF343,X0,sK33),sK31)
| ~ r2_hidden(X0,sF345) )
| ~ spl351_68
| ~ spl351_70
| ~ spl351_73
| ~ spl351_74
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79 ),
inference(forward_subsumption_resolution,[],[f23379,f24389]) ).
fof(f25185,plain,
( ! [X0] :
( r2_hidden(X0,sF344)
| ~ m1_subset_1(sK33,k1_zfmisc_1(k2_zfmisc_1(sK29,sK30)))
| ~ m1_subset_1(sF343,k1_zfmisc_1(sK29))
| v1_xboole_0(sK30)
| ~ r2_hidden(sK37(sF343,X0,sK33),sK32)
| ~ r2_hidden(X0,sF346) )
| ~ spl351_69
| ~ spl351_70
| ~ spl351_73
| ~ spl351_75
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79 ),
inference(forward_subsumption_resolution,[],[f23387,f24388]) ).
fof(f25186,plain,
( ! [X0] :
( r2_hidden(X0,sF346)
| ~ m1_subset_1(sK33,k1_zfmisc_1(k2_zfmisc_1(sK29,sK30)))
| ~ m1_subset_1(sK32,k1_zfmisc_1(sK29))
| v1_xboole_0(sK30)
| ~ r2_hidden(sK37(sK32,X0,sK33),sF343)
| ~ r2_hidden(X0,sF344) )
| ~ spl351_70
| ~ spl351_73
| ~ spl351_75
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79
| ~ spl351_91 ),
inference(forward_subsumption_resolution,[],[f23397,f24390]) ).
fof(f25187,plain,
( ! [X0] :
( r2_hidden(X0,sF345)
| ~ m1_subset_1(sK33,k1_zfmisc_1(k2_zfmisc_1(sK29,sK30)))
| ~ m1_subset_1(sK31,k1_zfmisc_1(sK29))
| v1_xboole_0(sK30)
| ~ r2_hidden(sK37(sK31,X0,sK33),sF343)
| ~ r2_hidden(X0,sF344) )
| ~ spl351_70
| ~ spl351_73
| ~ spl351_74
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79
| ~ spl351_91 ),
inference(forward_subsumption_resolution,[],[f23396,f24390]) ).
fof(f25222,definition,
( spl351_267
<=> ! [X0] : ~ r2_hidden(X0,sF347) ),
introduced(definition,[new_symbols(definition,[spl351_267])],[avatar_definition]) ).
fof(f25223,plain,
( ! [X0] : ~ r2_hidden(X0,sF347)
| ~ spl351_267 ),
inference(avatar_component_clause,[],[f25222]) ).
fof(f25227,plain,
( ~ spl351_96
| spl351_254
| ~ spl351_82 ),
inference(avatar_split_clause,[],[f25157,f23047,f25078,f23335]) ).
fof(f25229,plain,
( ! [X0] :
( ~ m1_subset_1(sK33,k1_zfmisc_1(sF348))
| r2_hidden(X0,sF344)
| ~ m1_subset_1(sF343,k1_zfmisc_1(sK29))
| v1_xboole_0(sK30)
| ~ r2_hidden(sK37(sF343,X0,sK33),sK31)
| ~ r2_hidden(X0,sF345) )
| ~ spl351_68
| ~ spl351_70
| ~ spl351_73
| ~ spl351_74
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79 ),
inference(forward_demodulation,[],[f25183,f23025]) ).
fof(f25231,plain,
( ! [X0] :
( ~ m1_subset_1(sK33,k1_zfmisc_1(sF348))
| r2_hidden(X0,sF344)
| ~ m1_subset_1(sF343,k1_zfmisc_1(sK29))
| v1_xboole_0(sK30)
| ~ r2_hidden(sK37(sF343,X0,sK33),sK32)
| ~ r2_hidden(X0,sF346) )
| ~ spl351_69
| ~ spl351_70
| ~ spl351_73
| ~ spl351_75
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79 ),
inference(forward_demodulation,[],[f25185,f23025]) ).
fof(f25232,plain,
( ! [X0] :
( ~ m1_subset_1(sK33,k1_zfmisc_1(sF348))
| r2_hidden(X0,sF346)
| ~ m1_subset_1(sK32,k1_zfmisc_1(sK29))
| v1_xboole_0(sK30)
| ~ r2_hidden(sK37(sK32,X0,sK33),sF343)
| ~ r2_hidden(X0,sF344) )
| ~ spl351_70
| ~ spl351_73
| ~ spl351_75
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79
| ~ spl351_91 ),
inference(forward_demodulation,[],[f25186,f23025]) ).
fof(f25233,plain,
( ! [X0] :
( ~ m1_subset_1(sK33,k1_zfmisc_1(sF348))
| r2_hidden(X0,sF345)
| ~ m1_subset_1(sK31,k1_zfmisc_1(sK29))
| v1_xboole_0(sK30)
| ~ r2_hidden(sK37(sK31,X0,sK33),sF343)
| ~ r2_hidden(X0,sF344) )
| ~ spl351_70
| ~ spl351_73
| ~ spl351_74
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79
| ~ spl351_91 ),
inference(forward_demodulation,[],[f25187,f23025]) ).
fof(f25248,plain,
( ! [X0] :
( ~ m1_subset_1(sK33,sF349)
| r2_hidden(X0,sF344)
| ~ m1_subset_1(sF343,k1_zfmisc_1(sK29))
| v1_xboole_0(sK30)
| ~ r2_hidden(sK37(sF343,X0,sK33),sK31)
| ~ r2_hidden(X0,sF345) )
| ~ spl351_68
| ~ spl351_70
| ~ spl351_73
| ~ spl351_74
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79 ),
inference(forward_demodulation,[],[f25229,f23030]) ).
fof(f25250,plain,
( ! [X0] :
( ~ m1_subset_1(sK33,sF349)
| r2_hidden(X0,sF344)
| ~ m1_subset_1(sF343,k1_zfmisc_1(sK29))
| v1_xboole_0(sK30)
| ~ r2_hidden(sK37(sF343,X0,sK33),sK32)
| ~ r2_hidden(X0,sF346) )
| ~ spl351_69
| ~ spl351_70
| ~ spl351_73
| ~ spl351_75
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79 ),
inference(forward_demodulation,[],[f25231,f23030]) ).
fof(f25251,plain,
( ! [X0] :
( ~ m1_subset_1(sK33,sF349)
| r2_hidden(X0,sF346)
| ~ m1_subset_1(sK32,k1_zfmisc_1(sK29))
| v1_xboole_0(sK30)
| ~ r2_hidden(sK37(sK32,X0,sK33),sF343)
| ~ r2_hidden(X0,sF344) )
| ~ spl351_70
| ~ spl351_73
| ~ spl351_75
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79
| ~ spl351_91 ),
inference(forward_demodulation,[],[f25232,f23030]) ).
fof(f25252,plain,
( ! [X0] :
( ~ m1_subset_1(sK33,sF349)
| r2_hidden(X0,sF345)
| ~ m1_subset_1(sK31,k1_zfmisc_1(sK29))
| v1_xboole_0(sK30)
| ~ r2_hidden(sK37(sK31,X0,sK33),sF343)
| ~ r2_hidden(X0,sF344) )
| ~ spl351_70
| ~ spl351_73
| ~ spl351_74
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79
| ~ spl351_91 ),
inference(forward_demodulation,[],[f25233,f23030]) ).
fof(f25279,plain,
( ! [X0] :
( r2_hidden(X0,sF344)
| ~ m1_subset_1(sF343,k1_zfmisc_1(sK29))
| v1_xboole_0(sK30)
| ~ r2_hidden(sK37(sF343,X0,sK33),sK31)
| ~ r2_hidden(X0,sF345) )
| ~ spl351_68
| ~ spl351_70
| ~ spl351_73
| ~ spl351_74
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79 ),
inference(forward_subsumption_resolution,[],[f25248,f22990]) ).
fof(f25281,plain,
( ! [X0] :
( r2_hidden(X0,sF344)
| ~ m1_subset_1(sF343,k1_zfmisc_1(sK29))
| v1_xboole_0(sK30)
| ~ r2_hidden(sK37(sF343,X0,sK33),sK32)
| ~ r2_hidden(X0,sF346) )
| ~ spl351_69
| ~ spl351_70
| ~ spl351_73
| ~ spl351_75
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79 ),
inference(forward_subsumption_resolution,[],[f25250,f22990]) ).
fof(f25282,plain,
( ! [X0] :
( r2_hidden(X0,sF346)
| ~ m1_subset_1(sK32,k1_zfmisc_1(sK29))
| v1_xboole_0(sK30)
| ~ r2_hidden(sK37(sK32,X0,sK33),sF343)
| ~ r2_hidden(X0,sF344) )
| ~ spl351_70
| ~ spl351_73
| ~ spl351_75
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79
| ~ spl351_91 ),
inference(forward_subsumption_resolution,[],[f25251,f22990]) ).
fof(f25283,plain,
( ! [X0] :
( r2_hidden(X0,sF345)
| ~ m1_subset_1(sK31,k1_zfmisc_1(sK29))
| v1_xboole_0(sK30)
| ~ r2_hidden(sK37(sK31,X0,sK33),sF343)
| ~ r2_hidden(X0,sF344) )
| ~ spl351_70
| ~ spl351_73
| ~ spl351_74
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79
| ~ spl351_91 ),
inference(forward_subsumption_resolution,[],[f25252,f22990]) ).
fof(f25297,plain,
( ! [X0] :
( ~ m1_subset_1(sF343,sF350)
| r2_hidden(X0,sF344)
| v1_xboole_0(sK30)
| ~ r2_hidden(sK37(sF343,X0,sK33),sK31)
| ~ r2_hidden(X0,sF345) )
| ~ spl351_68
| ~ spl351_70
| ~ spl351_73
| ~ spl351_74
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79 ),
inference(forward_demodulation,[],[f25279,f23035]) ).
fof(f25299,plain,
( ! [X0] :
( ~ m1_subset_1(sF343,sF350)
| r2_hidden(X0,sF344)
| v1_xboole_0(sK30)
| ~ r2_hidden(sK37(sF343,X0,sK33),sK32)
| ~ r2_hidden(X0,sF346) )
| ~ spl351_69
| ~ spl351_70
| ~ spl351_73
| ~ spl351_75
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79 ),
inference(forward_demodulation,[],[f25281,f23035]) ).
fof(f25300,plain,
( ! [X0] :
( ~ m1_subset_1(sK32,sF350)
| r2_hidden(X0,sF346)
| v1_xboole_0(sK30)
| ~ r2_hidden(sK37(sK32,X0,sK33),sF343)
| ~ r2_hidden(X0,sF344) )
| ~ spl351_70
| ~ spl351_73
| ~ spl351_75
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79
| ~ spl351_91 ),
inference(forward_demodulation,[],[f25282,f23035]) ).
fof(f25301,plain,
( ! [X0] :
( ~ m1_subset_1(sK31,sF350)
| r2_hidden(X0,sF345)
| v1_xboole_0(sK30)
| ~ r2_hidden(sK37(sK31,X0,sK33),sF343)
| ~ r2_hidden(X0,sF344) )
| ~ spl351_70
| ~ spl351_73
| ~ spl351_74
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79
| ~ spl351_91 ),
inference(forward_demodulation,[],[f25283,f23035]) ).
fof(f25315,plain,
( ! [X0] :
( r2_hidden(X0,sF344)
| v1_xboole_0(sK30)
| ~ r2_hidden(sK37(sF343,X0,sK33),sK31)
| ~ r2_hidden(X0,sF345) )
| ~ spl351_68
| ~ spl351_70
| ~ spl351_73
| ~ spl351_74
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79
| ~ spl351_91 ),
inference(forward_subsumption_resolution,[],[f25297,f23168]) ).
fof(f25317,plain,
( ! [X0] :
( r2_hidden(X0,sF344)
| v1_xboole_0(sK30)
| ~ r2_hidden(sK37(sF343,X0,sK33),sK32)
| ~ r2_hidden(X0,sF346) )
| ~ spl351_69
| ~ spl351_70
| ~ spl351_73
| ~ spl351_75
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79
| ~ spl351_91 ),
inference(forward_subsumption_resolution,[],[f25299,f23168]) ).
fof(f25318,plain,
( ! [X0] :
( r2_hidden(X0,sF346)
| v1_xboole_0(sK30)
| ~ r2_hidden(sK37(sK32,X0,sK33),sF343)
| ~ r2_hidden(X0,sF344) )
| ~ spl351_69
| ~ spl351_70
| ~ spl351_73
| ~ spl351_75
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79
| ~ spl351_91 ),
inference(forward_subsumption_resolution,[],[f25300,f22985]) ).
fof(f25319,plain,
( ! [X0] :
( r2_hidden(X0,sF345)
| v1_xboole_0(sK30)
| ~ r2_hidden(sK37(sK31,X0,sK33),sF343)
| ~ r2_hidden(X0,sF344) )
| ~ spl351_68
| ~ spl351_70
| ~ spl351_73
| ~ spl351_74
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79
| ~ spl351_91 ),
inference(forward_subsumption_resolution,[],[f25301,f22980]) ).
fof(f25343,definition,
( spl351_274
<=> ! [X0] :
( r2_hidden(X0,sF344)
| ~ r2_hidden(X0,sF345)
| ~ r2_hidden(sK37(sF343,X0,sK33),sK31) ) ),
introduced(definition,[new_symbols(definition,[spl351_274])],[avatar_definition]) ).
fof(f25344,plain,
( ! [X0] :
( ~ r2_hidden(sK37(sF343,X0,sK33),sK31)
| ~ r2_hidden(X0,sF345)
| r2_hidden(X0,sF344) )
| ~ spl351_274 ),
inference(avatar_component_clause,[],[f25343]) ).
fof(f25345,plain,
( spl351_96
| spl351_274
| ~ spl351_68
| ~ spl351_70
| ~ spl351_73
| ~ spl351_74
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79
| ~ spl351_91 ),
inference(avatar_split_clause,[],[f25315,f23166,f23033,f23028,f23023,f23008,f23003,f22988,f22978,f25343,f23335]) ).
fof(f25351,definition,
( spl351_276
<=> ! [X0] :
( r2_hidden(X0,sF344)
| ~ r2_hidden(X0,sF346)
| ~ r2_hidden(sK37(sF343,X0,sK33),sK32) ) ),
introduced(definition,[new_symbols(definition,[spl351_276])],[avatar_definition]) ).
fof(f25352,plain,
( ! [X0] :
( ~ r2_hidden(sK37(sF343,X0,sK33),sK32)
| ~ r2_hidden(X0,sF346)
| r2_hidden(X0,sF344) )
| ~ spl351_276 ),
inference(avatar_component_clause,[],[f25351]) ).
fof(f25353,plain,
( spl351_96
| spl351_276
| ~ spl351_69
| ~ spl351_70
| ~ spl351_73
| ~ spl351_75
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79
| ~ spl351_91 ),
inference(avatar_split_clause,[],[f25317,f23166,f23033,f23028,f23023,f23013,f23003,f22988,f22983,f25351,f23335]) ).
fof(f25355,definition,
( spl351_277
<=> ! [X0] :
( r2_hidden(X0,sF346)
| ~ r2_hidden(X0,sF344)
| ~ r2_hidden(sK37(sK32,X0,sK33),sF343) ) ),
introduced(definition,[new_symbols(definition,[spl351_277])],[avatar_definition]) ).
fof(f25356,plain,
( ! [X0] :
( ~ r2_hidden(sK37(sK32,X0,sK33),sF343)
| ~ r2_hidden(X0,sF344)
| r2_hidden(X0,sF346) )
| ~ spl351_277 ),
inference(avatar_component_clause,[],[f25355]) ).
fof(f25357,plain,
( spl351_96
| spl351_277
| ~ spl351_69
| ~ spl351_70
| ~ spl351_73
| ~ spl351_75
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79
| ~ spl351_91 ),
inference(avatar_split_clause,[],[f25318,f23166,f23033,f23028,f23023,f23013,f23003,f22988,f22983,f25355,f23335]) ).
fof(f25359,definition,
( spl351_278
<=> ! [X0] :
( r2_hidden(X0,sF345)
| ~ r2_hidden(X0,sF344)
| ~ r2_hidden(sK37(sK31,X0,sK33),sF343) ) ),
introduced(definition,[new_symbols(definition,[spl351_278])],[avatar_definition]) ).
fof(f25360,plain,
( ! [X0] :
( ~ r2_hidden(sK37(sK31,X0,sK33),sF343)
| ~ r2_hidden(X0,sF344)
| r2_hidden(X0,sF345) )
| ~ spl351_278 ),
inference(avatar_component_clause,[],[f25359]) ).
fof(f25361,plain,
( spl351_96
| spl351_278
| ~ spl351_68
| ~ spl351_70
| ~ spl351_73
| ~ spl351_74
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79
| ~ spl351_91 ),
inference(avatar_split_clause,[],[f25319,f23166,f23033,f23028,f23023,f23008,f23003,f22988,f22978,f25359,f23335]) ).
fof(f25412,plain,
( spl351_267
| ~ spl351_89
| ~ spl351_96 ),
inference(avatar_split_clause,[],[f25175,f23335,f23124,f25222]) ).
fof(f25424,plain,
( ! [X0] :
( r2_hidden(sK37(sK31,X0,sK33),sF343)
| r2_hidden(X0,sF345)
| ~ m1_subset_1(X0,sK30) )
| ~ spl351_95
| ~ spl351_98 ),
inference(resolution,[],[f23344,f24256]) ).
fof(f25438,plain,
( ! [X0] :
( r2_hidden(sK37(sK32,X0,sK33),sF343)
| r2_hidden(X0,sF346)
| ~ m1_subset_1(X0,sK30) )
| ~ spl351_88
| ~ spl351_97 ),
inference(resolution,[],[f23340,f24255]) ).
fof(f25486,plain,
( ! [X0] :
( r2_hidden(sK100(X0,sF344),X0)
| sF344 = X0 )
| ~ spl351_254 ),
inference(resolution,[],[f25079,f21177]) ).
fof(f25547,plain,
( sF344 = sF347
| ~ spl351_254
| ~ spl351_267 ),
inference(resolution,[],[f25486,f25223]) ).
fof(f25553,plain,
( $false
| spl351_71
| ~ spl351_254
| ~ spl351_267 ),
inference(forward_subsumption_resolution,[],[f25547,f22995]) ).
fof(f25554,plain,
( spl351_71
| ~ spl351_254
| ~ spl351_267 ),
inference(avatar_contradiction_clause,[],[f25553]) ).
fof(f25643,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF344)
| r2_hidden(X0,sF345)
| r2_hidden(X0,sF345)
| ~ m1_subset_1(X0,sK30) )
| ~ spl351_95
| ~ spl351_98
| ~ spl351_278 ),
inference(resolution,[],[f25360,f25424]) ).
fof(f25644,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF344)
| r2_hidden(X0,sF345)
| ~ m1_subset_1(X0,sK30) )
| ~ spl351_95
| ~ spl351_98
| ~ spl351_278 ),
inference(duplicate_literal_removal,[],[f25643]) ).
fof(f25645,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF344)
| r2_hidden(X0,sF345) )
| ~ spl351_70
| ~ spl351_73
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79
| ~ spl351_91
| ~ spl351_95
| ~ spl351_98
| ~ spl351_278 ),
inference(forward_subsumption_resolution,[],[f25644,f24390]) ).
fof(f25662,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF344)
| r2_hidden(X0,sF346)
| r2_hidden(X0,sF346)
| ~ m1_subset_1(X0,sK30) )
| ~ spl351_88
| ~ spl351_97
| ~ spl351_277 ),
inference(resolution,[],[f25356,f25438]) ).
fof(f25663,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF344)
| r2_hidden(X0,sF346)
| ~ m1_subset_1(X0,sK30) )
| ~ spl351_88
| ~ spl351_97
| ~ spl351_277 ),
inference(duplicate_literal_removal,[],[f25662]) ).
fof(f25664,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF344)
| r2_hidden(X0,sF346) )
| ~ spl351_70
| ~ spl351_73
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79
| ~ spl351_88
| ~ spl351_91
| ~ spl351_97
| ~ spl351_277 ),
inference(forward_subsumption_resolution,[],[f25663,f24390]) ).
fof(f25952,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF343)
| r2_hidden(X0,sK32)
| r2_hidden(X0,sK31) )
| ~ spl351_88 ),
inference(superposition,[],[f22490,f23109]) ).
fof(f25957,plain,
( ! [X0] :
( r2_hidden(sK37(sF343,X0,sK33),sK32)
| r2_hidden(sK37(sF343,X0,sK33),sK31)
| ~ m1_subset_1(X0,sK30)
| r2_hidden(X0,sF344) )
| ~ spl351_88
| ~ spl351_99 ),
inference(resolution,[],[f25952,f23348]) ).
fof(f25996,plain,
( ! [X0] :
( r2_hidden(sK37(sF343,X0,sK33),sK31)
| ~ m1_subset_1(X0,sK30)
| r2_hidden(X0,sF344)
| ~ r2_hidden(X0,sF346)
| r2_hidden(X0,sF344) )
| ~ spl351_88
| ~ spl351_99
| ~ spl351_276 ),
inference(resolution,[],[f25957,f25352]) ).
fof(f26002,plain,
( ! [X0] :
( r2_hidden(sK37(sF343,X0,sK33),sK31)
| ~ m1_subset_1(X0,sK30)
| r2_hidden(X0,sF344)
| ~ r2_hidden(X0,sF346) )
| ~ spl351_88
| ~ spl351_99
| ~ spl351_276 ),
inference(duplicate_literal_removal,[],[f25996]) ).
fof(f26007,plain,
( ! [X0] :
( r2_hidden(sK37(sF343,X0,sK33),sK31)
| r2_hidden(X0,sF344)
| ~ r2_hidden(X0,sF346) )
| ~ spl351_69
| ~ spl351_70
| ~ spl351_75
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79
| ~ spl351_88
| ~ spl351_99
| ~ spl351_276 ),
inference(forward_subsumption_resolution,[],[f26002,f24388]) ).
fof(f26013,plain,
( ! [X0] :
( r2_hidden(X0,sF344)
| ~ r2_hidden(X0,sF346)
| ~ r2_hidden(X0,sF345)
| r2_hidden(X0,sF344) )
| ~ spl351_69
| ~ spl351_70
| ~ spl351_75
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79
| ~ spl351_88
| ~ spl351_99
| ~ spl351_274
| ~ spl351_276 ),
inference(resolution,[],[f26007,f25344]) ).
fof(f26019,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF346)
| r2_hidden(X0,sF344)
| ~ r2_hidden(X0,sF345) )
| ~ spl351_69
| ~ spl351_70
| ~ spl351_75
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79
| ~ spl351_88
| ~ spl351_99
| ~ spl351_274
| ~ spl351_276 ),
inference(duplicate_literal_removal,[],[f26013]) ).
fof(f26031,plain,
( ! [X0] :
( r2_hidden(sK100(X0,sF347),sF344)
| ~ r2_hidden(sK100(X0,sF347),sF345)
| sF347 = X0
| r2_hidden(sK100(X0,sF347),X0) )
| ~ spl351_69
| ~ spl351_70
| ~ spl351_75
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79
| ~ spl351_88
| ~ spl351_92
| ~ spl351_99
| ~ spl351_274
| ~ spl351_276 ),
inference(resolution,[],[f26019,f23778]) ).
fof(f26051,plain,
( ! [X0] :
( r2_hidden(sK100(X0,sF347),sF344)
| sF347 = X0
| r2_hidden(sK100(X0,sF347),X0) )
| ~ spl351_69
| ~ spl351_70
| ~ spl351_75
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79
| ~ spl351_87
| ~ spl351_88
| ~ spl351_92
| ~ spl351_99
| ~ spl351_274
| ~ spl351_276 ),
inference(forward_subsumption_resolution,[],[f26031,f23737]) ).
fof(f26101,plain,
( r2_hidden(sK100(sF344,sF347),sF344)
| sF344 = sF347
| ~ spl351_69
| ~ spl351_70
| ~ spl351_75
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79
| ~ spl351_87
| ~ spl351_88
| ~ spl351_92
| ~ spl351_99
| ~ spl351_274
| ~ spl351_276 ),
inference(factoring,[],[f26051]) ).
fof(f26102,plain,
( r2_hidden(sK100(sF344,sF347),sF344)
| ~ spl351_69
| ~ spl351_70
| spl351_71
| ~ spl351_75
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79
| ~ spl351_87
| ~ spl351_88
| ~ spl351_92
| ~ spl351_99
| ~ spl351_274
| ~ spl351_276 ),
inference(forward_subsumption_resolution,[],[f26101,f22995]) ).
fof(f26105,definition,
( spl351_356
<=> r2_hidden(sK100(sF344,sF347),sF344) ),
introduced(definition,[new_symbols(definition,[spl351_356])],[avatar_definition]) ).
fof(f26107,plain,
( r2_hidden(sK100(sF344,sF347),sF344)
| ~ spl351_356 ),
inference(avatar_component_clause,[],[f26105]) ).
fof(f26108,plain,
( spl351_356
| ~ spl351_69
| ~ spl351_70
| spl351_71
| ~ spl351_75
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79
| ~ spl351_87
| ~ spl351_88
| ~ spl351_92
| ~ spl351_99
| ~ spl351_274
| ~ spl351_276 ),
inference(avatar_split_clause,[],[f26102,f25351,f25343,f23347,f23250,f23107,f23083,f23033,f23028,f23023,f23013,f22993,f22988,f22983,f26105]) ).
fof(f26109,plain,
( r2_hidden(sK100(sF344,sF347),sF346)
| ~ spl351_70
| ~ spl351_73
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79
| ~ spl351_88
| ~ spl351_91
| ~ spl351_97
| ~ spl351_277
| ~ spl351_356 ),
inference(resolution,[],[f26107,f25664]) ).
fof(f26110,plain,
( r2_hidden(sK100(sF344,sF347),sF345)
| ~ spl351_70
| ~ spl351_73
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79
| ~ spl351_91
| ~ spl351_95
| ~ spl351_98
| ~ spl351_278
| ~ spl351_356 ),
inference(resolution,[],[f26107,f25645]) ).
fof(f26126,definition,
( spl351_359
<=> r2_hidden(sK100(sF344,sF347),sF345) ),
introduced(definition,[new_symbols(definition,[spl351_359])],[avatar_definition]) ).
fof(f26128,plain,
( r2_hidden(sK100(sF344,sF347),sF345)
| ~ spl351_359 ),
inference(avatar_component_clause,[],[f26126]) ).
fof(f26129,plain,
( spl351_359
| ~ spl351_70
| ~ spl351_73
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79
| ~ spl351_91
| ~ spl351_95
| ~ spl351_98
| ~ spl351_278
| ~ spl351_356 ),
inference(avatar_split_clause,[],[f26110,f26105,f25359,f23343,f23307,f23166,f23033,f23028,f23023,f23003,f22988,f26126]) ).
fof(f26131,definition,
( spl351_360
<=> r2_hidden(sK100(sF344,sF347),sF346) ),
introduced(definition,[new_symbols(definition,[spl351_360])],[avatar_definition]) ).
fof(f26133,plain,
( r2_hidden(sK100(sF344,sF347),sF346)
| ~ spl351_360 ),
inference(avatar_component_clause,[],[f26131]) ).
fof(f26134,plain,
( spl351_360
| ~ spl351_70
| ~ spl351_73
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79
| ~ spl351_88
| ~ spl351_91
| ~ spl351_97
| ~ spl351_277
| ~ spl351_356 ),
inference(avatar_split_clause,[],[f26109,f26105,f25355,f23339,f23166,f23107,f23033,f23028,f23023,f23003,f22988,f26131]) ).
fof(f26159,plain,
( ~ r2_hidden(sK100(sF344,sF347),sF345)
| r2_hidden(sK100(sF344,sF347),sF347)
| ~ spl351_87
| ~ spl351_360 ),
inference(resolution,[],[f26133,f23455]) ).
fof(f26168,plain,
( r2_hidden(sK100(sF344,sF347),sF347)
| ~ spl351_87
| ~ spl351_359
| ~ spl351_360 ),
inference(forward_subsumption_resolution,[],[f26159,f26128]) ).
fof(f26171,definition,
( spl351_364
<=> r2_hidden(sK100(sF344,sF347),sF347) ),
introduced(definition,[new_symbols(definition,[spl351_364])],[avatar_definition]) ).
fof(f26173,plain,
( r2_hidden(sK100(sF344,sF347),sF347)
| ~ spl351_364 ),
inference(avatar_component_clause,[],[f26171]) ).
fof(f26174,plain,
( spl351_364
| ~ spl351_87
| ~ spl351_359
| ~ spl351_360 ),
inference(avatar_split_clause,[],[f26168,f26131,f26126,f23083,f26171]) ).
fof(f26175,plain,
( sF344 = sF347
| ~ r2_hidden(sK100(sF344,sF347),sF344)
| ~ spl351_364 ),
inference(resolution,[],[f26173,f21178]) ).
fof(f26186,plain,
( ~ r2_hidden(sK100(sF344,sF347),sF344)
| spl351_71
| ~ spl351_364 ),
inference(forward_subsumption_resolution,[],[f26175,f22995]) ).
fof(f26187,plain,
( $false
| spl351_71
| ~ spl351_356
| ~ spl351_364 ),
inference(forward_subsumption_resolution,[],[f26186,f26107]) ).
fof(f26188,plain,
( spl351_71
| ~ spl351_356
| ~ spl351_364 ),
inference(avatar_contradiction_clause,[],[f26187]) ).
cnf(s71,plain,
spl351_68,
inference(sat_conversion,[],[f22981]) ).
cnf(s72,plain,
spl351_69,
inference(sat_conversion,[],[f22986]) ).
cnf(s73,plain,
spl351_70,
inference(sat_conversion,[],[f22991]) ).
cnf(s74,plain,
~ spl351_71,
inference(sat_conversion,[],[f22996]) ).
cnf(s75,plain,
spl351_72,
inference(sat_conversion,[],[f23001]) ).
cnf(s76,plain,
spl351_73,
inference(sat_conversion,[],[f23006]) ).
cnf(s77,plain,
spl351_74,
inference(sat_conversion,[],[f23011]) ).
cnf(s78,plain,
spl351_75,
inference(sat_conversion,[],[f23016]) ).
cnf(s79,plain,
spl351_76,
inference(sat_conversion,[],[f23021]) ).
cnf(s80,plain,
spl351_77,
inference(sat_conversion,[],[f23026]) ).
cnf(s81,plain,
spl351_78,
inference(sat_conversion,[],[f23031]) ).
cnf(s82,plain,
spl351_79,
inference(sat_conversion,[],[f23036]) ).
cnf(s83,plain,
( ~ spl351_73
| ~ spl351_80
| ~ spl351_81
| spl351_82 ),
inference(sat_conversion,[],[f23050]) ).
cnf(s84,plain,
( ~ spl351_70
| ~ spl351_77
| ~ spl351_78
| spl351_80 ),
inference(sat_conversion,[],[f23051]) ).
cnf(s85,plain,
( ~ spl351_74
| ~ spl351_80
| ~ spl351_83
| spl351_84 ),
inference(sat_conversion,[],[f23061]) ).
cnf(s86,plain,
( ~ spl351_68
| ~ spl351_79
| spl351_83 ),
inference(sat_conversion,[],[f23062]) ).
cnf(s87,plain,
( ~ spl351_75
| ~ spl351_80
| ~ spl351_85
| spl351_86 ),
inference(sat_conversion,[],[f23072]) ).
cnf(s88,plain,
( ~ spl351_69
| ~ spl351_79
| spl351_85 ),
inference(sat_conversion,[],[f23073]) ).
cnf(s90,plain,
( ~ spl351_76
| ~ spl351_84
| ~ spl351_86
| spl351_87 ),
inference(sat_conversion,[],[f23087]) ).
cnf(s91,plain,
( ~ spl351_68
| ~ spl351_69
| ~ spl351_72
| ~ spl351_79
| spl351_88 ),
inference(sat_conversion,[],[f23110]) ).
cnf(s93,plain,
( ~ spl351_76
| ~ spl351_84
| ~ spl351_86
| spl351_89 ),
inference(sat_conversion,[],[f23127]) ).
cnf(s95,plain,
( ~ spl351_68
| ~ spl351_69
| ~ spl351_72
| ~ spl351_79
| spl351_91 ),
inference(sat_conversion,[],[f23169]) ).
cnf(s96,plain,
( ~ spl351_79
| spl351_81
| ~ spl351_91 ),
inference(sat_conversion,[],[f23170]) ).
cnf(s98,plain,
( ~ spl351_76
| ~ spl351_84
| ~ spl351_86
| spl351_92 ),
inference(sat_conversion,[],[f23253]) ).
cnf(s101,plain,
( ~ spl351_68
| ~ spl351_69
| ~ spl351_72
| ~ spl351_79
| spl351_95 ),
inference(sat_conversion,[],[f23310]) ).
cnf(s103,plain,
( ~ spl351_69
| ~ spl351_70
| ~ spl351_75
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79
| spl351_96
| spl351_97 ),
inference(sat_conversion,[],[f23341]) ).
cnf(s104,plain,
( ~ spl351_68
| ~ spl351_70
| ~ spl351_74
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79
| spl351_96
| spl351_98 ),
inference(sat_conversion,[],[f23345]) ).
cnf(s105,plain,
( ~ spl351_70
| ~ spl351_73
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79
| ~ spl351_91
| spl351_96
| spl351_99 ),
inference(sat_conversion,[],[f23349]) ).
cnf(s256,plain,
( ~ spl351_82
| ~ spl351_96
| spl351_254 ),
inference(sat_conversion,[],[f25227]) ).
cnf(s261,plain,
( ~ spl351_68
| ~ spl351_70
| ~ spl351_73
| ~ spl351_74
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79
| ~ spl351_91
| spl351_96
| spl351_274 ),
inference(sat_conversion,[],[f25345]) ).
cnf(s263,plain,
( ~ spl351_69
| ~ spl351_70
| ~ spl351_73
| ~ spl351_75
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79
| ~ spl351_91
| spl351_96
| spl351_276 ),
inference(sat_conversion,[],[f25353]) ).
cnf(s264,plain,
( ~ spl351_69
| ~ spl351_70
| ~ spl351_73
| ~ spl351_75
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79
| ~ spl351_91
| spl351_96
| spl351_277 ),
inference(sat_conversion,[],[f25357]) ).
cnf(s265,plain,
( ~ spl351_68
| ~ spl351_70
| ~ spl351_73
| ~ spl351_74
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79
| ~ spl351_91
| spl351_96
| spl351_278 ),
inference(sat_conversion,[],[f25361]) ).
cnf(s276,plain,
( ~ spl351_89
| ~ spl351_96
| spl351_267 ),
inference(sat_conversion,[],[f25412]) ).
cnf(s294,plain,
( spl351_71
| ~ spl351_254
| ~ spl351_267 ),
inference(sat_conversion,[],[f25554]) ).
cnf(s375,plain,
( ~ spl351_69
| ~ spl351_70
| spl351_71
| ~ spl351_75
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79
| ~ spl351_87
| ~ spl351_88
| ~ spl351_92
| ~ spl351_99
| ~ spl351_274
| ~ spl351_276
| spl351_356 ),
inference(sat_conversion,[],[f26108]) ).
cnf(s379,plain,
( ~ spl351_70
| ~ spl351_73
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79
| ~ spl351_91
| ~ spl351_95
| ~ spl351_98
| ~ spl351_278
| ~ spl351_356
| spl351_359 ),
inference(sat_conversion,[],[f26129]) ).
cnf(s380,plain,
( ~ spl351_70
| ~ spl351_73
| ~ spl351_77
| ~ spl351_78
| ~ spl351_79
| ~ spl351_88
| ~ spl351_91
| ~ spl351_97
| ~ spl351_277
| ~ spl351_356
| spl351_360 ),
inference(sat_conversion,[],[f26134]) ).
cnf(s388,plain,
( ~ spl351_87
| ~ spl351_359
| ~ spl351_360
| spl351_364 ),
inference(sat_conversion,[],[f26174]) ).
cnf(s391,plain,
( spl351_71
| ~ spl351_356
| ~ spl351_364 ),
inference(sat_conversion,[],[f26188]) ).
cnf(s395,plain,
spl351_80,
inference(rat,[],[s84,s80,s81,s73]) ).
cnf(s397,plain,
spl351_85,
inference(rat,[],[s88,s82,s72]) ).
cnf(s398,plain,
spl351_86,
inference(rat,[],[s87,s395,s78,s397]) ).
cnf(s401,plain,
spl351_95,
inference(rat,[],[s101,s72,s82,s75,s71]) ).
cnf(s402,plain,
spl351_91,
inference(rat,[],[s95,s72,s82,s75,s71]) ).
cnf(s403,plain,
spl351_88,
inference(rat,[],[s91,s72,s82,s75,s71]) ).
cnf(s404,plain,
spl351_83,
inference(rat,[],[s86,s82,s71]) ).
cnf(s406,plain,
spl351_81,
inference(rat,[],[s96,s82,s402]) ).
cnf(s407,plain,
spl351_84,
inference(rat,[],[s85,s395,s77,s404]) ).
cnf(s408,plain,
spl351_82,
inference(rat,[],[s83,s395,s76,s406]) ).
cnf(s410,plain,
spl351_92,
inference(rat,[],[s98,s398,s79,s407]) ).
cnf(s411,plain,
spl351_89,
inference(rat,[],[s93,s398,s79,s407]) ).
cnf(s412,plain,
spl351_87,
inference(rat,[],[s90,s398,s79,s407]) ).
cnf(s417,plain,
spl351_96,
inference(rat,[],[s388,s380,s379,s391,s375,s261,s265,s263,s264,s103,s104,s105,s412,s80,s81,s82,s76,s73,s402,s403,s401,s74,s78,s72,s410,s77,s71]) ).
cnf(s418,plain,
spl351_267,
inference(rat,[],[s276,s411,s417]) ).
cnf(s419,plain,
spl351_254,
inference(rat,[],[s256,s408,s417]) ).
cnf(s425,plain,
$false,
inference(rat,[],[s294,s74,s418,s419]) ).
fof(f26189,plain,
$false,
inference(avatar_sat_refutation,[],[s425]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU428+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.38 % Computer : n006.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Mon Sep 28 05:22:29 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.42 Running first-order theorem proving
% 0.12/0.42 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 14.37/3.96 % (3641407)Detected formulas, will run a generic FOF schedule.
% 14.37/3.96 % (3641413)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=2749538074:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2988 on theBenchmark for (2988ds/134677Mi)
% 14.37/3.96 % (3641415)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=544628932:i=109:sd=1:ins=1:gsp=on:ss=axioms_2988 on theBenchmark for (2988ds/109Mi)
% 14.37/3.96 % (3641417)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3118140947:s2a=on:i=139:gtg=position_2988 on theBenchmark for (2988ds/139Mi)
% 14.37/3.96 % (3641412)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=776311031:i=141193_2988 on theBenchmark for (2988ds/141193Mi)
% 14.37/3.96 % (3641414)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=4220834652:i=141695:sd=1:nm=32:gsp=on:ss=included_2988 on theBenchmark for (2988ds/141695Mi)
% 14.37/3.96 % (3641418)dis-21_1_sil=8000:lcm=predicate:random_seed=2504241990: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)
% 14.37/3.96 % (3641416)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=207051014:i=119:av=off:ss=axioms_2988 on theBenchmark for (2988ds/119Mi)
% 14.37/3.96 % (3641417)Instruction limit reached!
% 14.37/3.96 % (3641417)------------------------------
% 14.37/3.96 % (3641417)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.37/3.96 % (3641417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.37/3.96 % (3641417)CaDiCaL version: 2.1.3
% 14.37/3.96 % (3641417)Termination reason: Instruction limit
% 14.37/3.96 % (3641417)Termination phase: Property scanning
% 14.37/3.96 % (3641417)Time elapsed: 0.059 s
% 14.37/3.96 % (3641417)Peak memory usage: 112 MB
% 14.37/3.96 % (3641417)Instructions burned: 139 (million)
% 14.37/3.96 % (3641415)Instruction limit reached!
% 14.37/3.96 % (3641415)------------------------------
% 14.37/3.96 % (3641415)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.37/3.96 % (3641415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.37/3.96 % (3641415)CaDiCaL version: 2.1.3
% 14.37/3.96 % (3641415)Termination reason: Instruction limit
% 14.37/3.96 % (3641415)Termination phase: SInE selection
% 14.37/3.96 % (3641415)Time elapsed: 0.087 s
% 14.37/3.96 % (3641415)Peak memory usage: 112 MB
% 14.37/3.96 % (3641415)Instructions burned: 109 (million)
% 14.37/3.96 % (3641418)Instruction limit reached!
% 14.37/3.96 % (3641418)------------------------------
% 14.37/3.96 % (3641418)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.37/3.96 % (3641418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.37/3.96 % (3641418)CaDiCaL version: 2.1.3
% 14.37/3.96 % (3641418)Termination reason: Instruction limit
% 14.37/3.96 % (3641418)Termination phase: SInE selection
% 14.37/3.96 % (3641418)Time elapsed: 0.087 s
% 14.37/3.96 % (3641418)Peak memory usage: 112 MB
% 14.37/3.96 % (3641418)Instructions burned: 130 (million)
% 14.37/3.96 % (3641416)Instruction limit reached!
% 14.37/3.96 % (3641416)------------------------------
% 14.37/3.96 % (3641416)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.37/3.96 % (3641416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.37/3.96 % (3641416)CaDiCaL version: 2.1.3
% 14.37/3.96 % (3641416)Termination reason: Instruction limit
% 14.37/3.96 % (3641416)Termination phase: Preprocessing 1
% 14.37/3.96 % (3641416)Time elapsed: 0.095 s
% 14.37/3.96 % (3641416)Peak memory usage: 113 MB
% 14.37/3.96 % (3641416)Instructions burned: 119 (million)
% 14.37/3.96 % (3641426)lrs+10_1_sil=8000:sp=occurrence:random_seed=1636449664:i=285:sd=3:ss=axioms:sgt=8_2986 on theBenchmark for (2986ds/285Mi)
% 14.37/3.96 % (3641427)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1604996491:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2986 on theBenchmark for (2986ds/157Mi)
% 14.37/3.96 % (3641428)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3075904411:i=325:sd=1:ss=axioms:sgt=32_2986 on theBenchmark for (2986ds/325Mi)
% 14.37/3.96 % (3641429)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=1800239766:s2a=on:i=248:s2at=1.23:gtg=position_2986 on theBenchmark for (2986ds/248Mi)
% 14.37/3.96 % (3641427)Instruction limit reached!
% 21.00/4.88 % (3641427)------------------------------
% 21.00/4.88 % (3641427)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.00/4.88 % (3641427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.00/4.88 % (3641427)CaDiCaL version: 2.1.3
% 21.00/4.88 % (3641427)Termination reason: Instruction limit
% 21.00/4.88 % (3641427)Termination phase: Property scanning
% 21.00/4.88 % (3641427)Time elapsed: 0.068 s
% 21.00/4.88 % (3641427)Peak memory usage: 112 MB
% 21.00/4.88 % (3641427)Instructions burned: 159 (million)
% 21.00/4.88 % (3641429)Instruction limit reached!
% 21.00/4.88 % (3641429)------------------------------
% 21.00/4.88 % (3641429)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.00/4.88 % (3641429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.00/4.88 % (3641429)CaDiCaL version: 2.1.3
% 21.00/4.88 % (3641429)Termination reason: Instruction limit
% 21.00/4.88 % (3641429)Termination phase: Property scanning
% 21.00/4.88 % (3641429)Time elapsed: 0.106 s
% 21.00/4.88 % (3641429)Peak memory usage: 112 MB
% 21.00/4.88 % (3641429)Instructions burned: 250 (million)
% 21.00/4.88 % (3641426)Instruction limit reached!
% 21.00/4.88 % (3641426)------------------------------
% 21.00/4.88 % (3641426)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.00/4.88 % (3641426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.00/4.88 % (3641426)CaDiCaL version: 2.1.3
% 21.00/4.88 % (3641426)Termination reason: Instruction limit
% 21.00/4.88 % (3641426)Termination phase: Saturation
% 21.00/4.88 % (3641426)Time elapsed: 0.207 s
% 21.00/4.88 % (3641426)Peak memory usage: 119 MB
% 21.00/4.88 % (3641426)Instructions burned: 285 (million)
% 21.00/4.88 % (3641434)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2303438874:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2984 on theBenchmark for (2984ds/294Mi)
% 21.00/4.88 % (3641428)Instruction limit reached!
% 21.00/4.88 % (3641428)------------------------------
% 21.00/4.88 % (3641428)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.00/4.88 % (3641428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.00/4.88 % (3641428)CaDiCaL version: 2.1.3
% 21.00/4.88 % (3641428)Termination reason: Instruction limit
% 21.00/4.88 % (3641428)Termination phase: Saturation
% 21.00/4.88 % (3641428)Time elapsed: 0.235 s
% 21.00/4.88 % (3641428)Peak memory usage: 119 MB
% 21.00/4.88 % (3641428)Instructions burned: 325 (million)
% 21.00/4.88 % (3641435)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1947920386:i=2350_2984 on theBenchmark for (2984ds/2350Mi)
% 21.00/4.88 % (3641436)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=84143277:cts=off:i=113:fsr=off:ss=included:sgt=4_2983 on theBenchmark for (2983ds/113Mi)
% 21.00/4.88 % (3641438)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=265912010:i=127:av=off:fsr=off:sup=off_2982 on theBenchmark for (2982ds/127Mi)
% 21.00/4.88 % (3641436)Instruction limit reached!
% 21.00/4.88 % (3641436)------------------------------
% 21.00/4.88 % (3641436)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.00/4.88 % (3641436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.00/4.88 % (3641436)CaDiCaL version: 2.1.3
% 21.00/4.88 % (3641436)Termination reason: Instruction limit
% 21.00/4.88 % (3641436)Termination phase: SInE selection
% 21.00/4.88 % (3641436)Time elapsed: 0.088 s
% 21.00/4.88 % (3641436)Peak memory usage: 112 MB
% 21.00/4.88 % (3641436)Instructions burned: 114 (million)
% 21.00/4.88 % (3641434)Instruction limit reached!
% 21.00/4.88 % (3641434)------------------------------
% 21.00/4.88 % (3641434)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.00/4.88 % (3641434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.00/4.88 % (3641434)CaDiCaL version: 2.1.3
% 21.00/4.88 % (3641434)Termination reason: Instruction limit
% 21.00/4.88 % (3641434)Termination phase: Property scanning
% 21.00/4.88 % (3641434)Time elapsed: 0.210 s
% 21.00/4.88 % (3641434)Peak memory usage: 118 MB
% 21.00/4.88 % (3641434)Instructions burned: 294 (million)
% 21.00/4.88 % (3641438)Instruction limit reached!
% 21.00/4.88 % (3641438)------------------------------
% 21.00/4.88 % (3641438)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.00/4.88 % (3641438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.00/4.88 % (3641438)CaDiCaL version: 2.1.3
% 67.78/11.35 % (3641438)Termination reason: Instruction limit
% 67.78/11.35 % (3641438)Termination phase: Preprocessing 1
% 67.78/11.35 % (3641438)Time elapsed: 0.094 s
% 67.78/11.35 % (3641438)Peak memory usage: 113 MB
% 67.78/11.35 % (3641438)Instructions burned: 129 (million)
% 67.78/11.35 % (3641442)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3317319875:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2981 on theBenchmark for (2981ds/114Mi)
% 67.78/11.35 % (3641443)lrs+10_1_sil=8000:sp=occurrence:random_seed=1748068202:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2981 on theBenchmark for (2981ds/907Mi)
% 67.78/11.35 % (3641442)Instruction limit reached!
% 67.78/11.35 % (3641442)------------------------------
% 67.78/11.35 % (3641442)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.78/11.35 % (3641442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.78/11.35 % (3641442)CaDiCaL version: 2.1.3
% 67.78/11.35 % (3641442)Termination reason: Instruction limit
% 67.78/11.35 % (3641442)Termination phase: Property scanning
% 67.78/11.35 % (3641442)Time elapsed: 0.050 s
% 67.78/11.35 % (3641442)Peak memory usage: 112 MB
% 67.78/11.35 % (3641442)Instructions burned: 116 (million)
% 67.78/11.35 % (3641444)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=325242739:i=437:sd=1:aac=none:ss=included_2980 on theBenchmark for (2980ds/437Mi)
% 67.78/11.35 % (3641447)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2234004070:i=5202:ss=axioms:sgt=16_2979 on theBenchmark for (2979ds/5202Mi)
% 67.78/11.35 % (3641444)Instruction limit reached!
% 67.78/11.35 % (3641444)------------------------------
% 67.78/11.35 % (3641444)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.78/11.35 % (3641444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.78/11.35 % (3641444)CaDiCaL version: 2.1.3
% 67.78/11.35 % (3641444)Termination reason: Instruction limit
% 67.78/11.35 % (3641444)Termination phase: Saturation
% 67.78/11.35 % (3641444)Time elapsed: 0.299 s
% 67.78/11.35 % (3641444)Peak memory usage: 121 MB
% 67.78/11.35 % (3641444)Instructions burned: 437 (million)
% 67.78/11.35 % (3641450)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=750129057:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2976 on theBenchmark for (2976ds/134Mi)
% 67.78/11.35 % (3641443)Instruction limit reached!
% 67.78/11.35 % (3641443)------------------------------
% 67.78/11.35 % (3641443)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.78/11.35 % (3641443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.78/11.35 % (3641443)CaDiCaL version: 2.1.3
% 67.78/11.35 % (3641443)Termination reason: Instruction limit
% 67.78/11.35 % (3641443)Termination phase: Saturation
% 67.78/11.35 % (3641443)Time elapsed: 0.521 s
% 67.78/11.35 % (3641443)Peak memory usage: 131 MB
% 67.78/11.35 % (3641443)Instructions burned: 907 (million)
% 67.78/11.35 % (3641450)Instruction limit reached!
% 67.78/11.35 % (3641450)------------------------------
% 67.78/11.35 % (3641450)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.78/11.35 % (3641450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.78/11.35 % (3641450)CaDiCaL version: 2.1.3
% 67.78/11.35 % (3641450)Termination reason: Instruction limit
% 67.78/11.35 % (3641450)Termination phase: NewCNF
% 67.78/11.35 % (3641450)Time elapsed: 0.116 s
% 67.78/11.35 % (3641450)Peak memory usage: 115 MB
% 67.78/11.35 % (3641450)Instructions burned: 135 (million)
% 67.78/11.35 % (3641452)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=23940257:st=8:i=592:sd=3:ep=RST:ss=axioms_2974 on theBenchmark for (2974ds/592Mi)
% 67.78/11.35 % (3641453)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=627976330:st=3:i=13193:sd=3:ss=axioms_2973 on theBenchmark for (2973ds/13193Mi)
% 67.78/11.35 % (3641435)Instruction limit reached!
% 67.78/11.35 % (3641435)------------------------------
% 67.78/11.35 % (3641435)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.78/11.35 % (3641435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.78/11.35 % (3641435)CaDiCaL version: 2.1.3
% 67.78/11.35 % (3641435)Termination reason: Instruction limit
% 67.78/11.35 % (3641435)Termination phase: Property scanning
% 67.78/11.35 % (3641435)Time elapsed: 1.267 s
% 67.78/11.35 % (3641435)Peak memory usage: 171 MB
% 67.78/11.35 % (3641435)Instructions burned: 2350 (million)
% 67.78/11.35 % (3641452)Instruction limit reached!
% 67.78/11.35 % (3641452)------------------------------
% 67.78/11.35 % (3641452)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 91.18/14.67 % (3641452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.18/14.67 % (3641452)CaDiCaL version: 2.1.3
% 91.18/14.67 % (3641452)Termination reason: Instruction limit
% 91.18/14.67 % (3641452)Termination phase: Preprocessing 3
% 91.18/14.67 % (3641452)Time elapsed: 0.435 s
% 91.18/14.67 % (3641452)Peak memory usage: 135 MB
% 91.18/14.67 % (3641452)Instructions burned: 593 (million)
% 91.18/14.67 % (3641456)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=3340738546:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2969 on theBenchmark for (2969ds/125Mi)
% 91.18/14.67 % (3641456)Instruction limit reached!
% 91.18/14.67 % (3641456)------------------------------
% 91.18/14.67 % (3641456)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 91.18/14.67 % (3641456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.18/14.67 % (3641456)CaDiCaL version: 2.1.3
% 91.18/14.67 % (3641456)Termination reason: Instruction limit
% 91.18/14.67 % (3641456)Termination phase: Property scanning
% 91.18/14.67 % (3641456)Time elapsed: 0.055 s
% 91.18/14.67 % (3641456)Peak memory usage: 112 MB
% 91.18/14.67 % (3641456)Instructions burned: 127 (million)
% 91.18/14.67 % (3641457)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2089855079:i=134:gtgl=5:slsql=off:gtg=exists_sym_2968 on theBenchmark for (2968ds/134Mi)
% 91.18/14.67 % (3641457)Instruction limit reached!
% 91.18/14.67 % (3641457)------------------------------
% 91.18/14.67 % (3641457)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 91.18/14.67 % (3641457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.18/14.67 % (3641457)CaDiCaL version: 2.1.3
% 91.18/14.67 % (3641457)Termination reason: Instruction limit
% 91.18/14.67 % (3641457)Termination phase: Property scanning
% 91.18/14.67 % (3641457)Time elapsed: 0.058 s
% 91.18/14.67 % (3641457)Peak memory usage: 112 MB
% 91.18/14.67 % (3641457)Instructions burned: 135 (million)
% 91.18/14.67 % (3641459)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3636465634:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2967 on theBenchmark for (2967ds/141Mi)
% 91.18/14.67 % (3641461)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3428962086:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2967 on theBenchmark for (2967ds/431Mi)
% 91.18/14.67 % (3641459)Instruction limit reached!
% 91.18/14.67 % (3641459)------------------------------
% 91.18/14.67 % (3641459)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 91.18/14.67 % (3641459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.18/14.67 % (3641459)CaDiCaL version: 2.1.3
% 91.18/14.67 % (3641459)Termination reason: Instruction limit
% 91.18/14.67 % (3641459)Termination phase: Saturation
% 91.18/14.67 % (3641459)Time elapsed: 0.119 s
% 91.18/14.67 % (3641459)Peak memory usage: 117 MB
% 91.18/14.67 % (3641459)Instructions burned: 141 (million)
% 91.18/14.67 % (3641461)Refutation not found, incomplete strategy
% 91.18/14.67 % (3641461)------------------------------
% 91.18/14.67 % (3641461)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 91.18/14.67 % (3641461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.18/14.67 % (3641461)CaDiCaL version: 2.1.3
% 91.18/14.67 % (3641461)Termination reason: Refutation not found, incomplete strategy
% 91.18/14.67 % (3641461)Time elapsed: 0.106 s
% 91.18/14.67 % (3641461)Peak memory usage: 117 MB
% 91.18/14.67 % (3641461)Instructions burned: 122 (million)
% 91.18/14.67 % (3641464)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=3953423722:i=6060:aac=none:ins=25_2965 on theBenchmark for (2965ds/6060Mi)
% 91.18/14.67 % (3641461)------------------------------
% 91.18/14.67 % (3641461)------------------------------
% 91.18/14.67 % (3641466)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=1815669203:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2962 on theBenchmark for (2962ds/150Mi)
% 91.18/14.67 % (3641466)Instruction limit reached!
% 91.18/14.67 % (3641466)------------------------------
% 91.18/14.67 % (3641466)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 91.18/14.67 % (3641466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.82/19.29 % (3641466)CaDiCaL version: 2.1.3
% 123.82/19.29 % (3641466)Termination reason: Instruction limit
% 123.82/19.29 % (3641466)Termination phase: Preprocessing 1
% 123.82/19.29 % (3641466)Time elapsed: 0.122 s
% 123.82/19.29 % (3641466)Peak memory usage: 113 MB
% 123.82/19.29 % (3641466)Instructions burned: 150 (million)
% 123.82/19.29 % (3641468)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3338665202:i=14155:bd=all_2959 on theBenchmark for (2959ds/14155Mi)
% 123.82/19.29 % (3641447)Instruction limit reached!
% 123.82/19.29 % (3641447)------------------------------
% 123.82/19.29 % (3641447)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 123.82/19.29 % (3641447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.82/19.29 % (3641447)CaDiCaL version: 2.1.3
% 123.82/19.29 % (3641447)Termination reason: Instruction limit
% 123.82/19.29 % (3641447)Termination phase: Saturation
% 123.82/19.29 % (3641447)Time elapsed: 4.036 s
% 123.82/19.29 % (3641447)Peak memory usage: 572 MB
% 123.82/19.29 % (3641447)Instructions burned: 5203 (million)
% 123.82/19.29 % (3641470)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=650499129:i=667:av=off:fsr=off_2937 on theBenchmark for (2937ds/667Mi)
% 123.82/19.29 % (3641470)Instruction limit reached!
% 123.82/19.29 % (3641470)------------------------------
% 123.82/19.29 % (3641470)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 123.82/19.29 % (3641470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.82/19.29 % (3641470)CaDiCaL version: 2.1.3
% 123.82/19.29 % (3641470)Termination reason: Instruction limit
% 123.82/19.29 % (3641470)Termination phase: NewCNF
% 123.82/19.29 % (3641470)Time elapsed: 0.526 s
% 123.82/19.29 % (3641470)Peak memory usage: 149 MB
% 123.82/19.29 % (3641470)Instructions burned: 668 (million)
% 123.82/19.29 % (3641472)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=958994730:s2a=on:i=185:s2at=1.8:fdi=4_2930 on theBenchmark for (2930ds/185Mi)
% 123.82/19.29 % (3641472)Instruction limit reached!
% 123.82/19.29 % (3641472)------------------------------
% 123.82/19.29 % (3641472)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 123.82/19.29 % (3641472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.82/19.29 % (3641472)CaDiCaL version: 2.1.3
% 123.82/19.29 % (3641472)Termination reason: Instruction limit
% 123.82/19.29 % (3641472)Termination phase: SInE selection
% 123.82/19.29 % (3641472)Time elapsed: 0.148 s
% 123.82/19.29 % (3641472)Peak memory usage: 113 MB
% 123.82/19.29 % (3641472)Instructions burned: 185 (million)
% 123.82/19.29 % (3641474)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=795055044:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2927 on theBenchmark for (2927ds/193Mi)
% 123.82/19.29 % (3641474)Instruction limit reached!
% 123.82/19.29 % (3641474)------------------------------
% 123.82/19.29 % (3641474)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 123.82/19.29 % (3641474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.82/19.29 % (3641474)CaDiCaL version: 2.1.3
% 123.82/19.29 % (3641474)Termination reason: Instruction limit
% 123.82/19.29 % (3641474)Termination phase: SInE selection
% 123.82/19.29 % (3641474)Time elapsed: 0.163 s
% 123.82/19.29 % (3641474)Peak memory usage: 112 MB
% 123.82/19.29 % (3641474)Instructions burned: 193 (million)
% 123.82/19.29 % (3641476)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=813052332:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2924 on theBenchmark for (2924ds/4850Mi)
% 123.82/19.29 % (3641464)Instruction limit reached!
% 123.82/19.29 % (3641464)------------------------------
% 123.82/19.29 % (3641464)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 123.82/19.29 % (3641464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.82/19.29 % (3641464)CaDiCaL version: 2.1.3
% 123.82/19.29 % (3641464)Termination reason: Instruction limit
% 123.82/19.29 % (3641464)Termination phase: Saturation
% 123.82/19.29 % (3641464)Time elapsed: 4.476 s
% 123.82/19.29 % (3641464)Peak memory usage: 513 MB
% 123.82/19.29 % (3641464)Instructions burned: 6060 (million)
% 123.82/19.29 % (3641478)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=2824937638:i=12111:sd=1:ss=included_2918 on theBenchmark for (2918ds/12111Mi)
% 123.82/19.29 % (3641453)Instruction limit reached!
% 123.82/19.29 % (3641453)------------------------------
% 123.82/19.29 % (3641453)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 159.92/24.32 % (3641453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 159.92/24.32 % (3641453)CaDiCaL version: 2.1.3
% 159.92/24.32 % (3641453)Termination reason: Instruction limit
% 159.92/24.32 % (3641453)Termination phase: Saturation
% 159.92/24.32 % (3641453)Time elapsed: 7.730 s
% 159.92/24.32 % (3641453)Peak memory usage: 306 MB
% 159.92/24.32 % (3641453)Instructions burned: 13194 (million)
% 159.92/24.32 % (3641476)Instruction limit reached!
% 159.92/24.32 % (3641476)------------------------------
% 159.92/24.32 % (3641476)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 159.92/24.32 % (3641476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 159.92/24.32 % (3641476)CaDiCaL version: 2.1.3
% 159.92/24.32 % (3641476)Termination reason: Instruction limit
% 159.92/24.32 % (3641476)Termination phase: Saturation
% 159.92/24.32 % (3641476)Time elapsed: 2.816 s
% 159.92/24.32 % (3641476)Peak memory usage: 216 MB
% 159.92/24.32 % (3641476)Instructions burned: 4850 (million)
% 159.92/24.32 % (3641480)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=4058076494:i=319:kws=precedence:fsr=off_2894 on theBenchmark for (2894ds/319Mi)
% 159.92/24.32 % (3641481)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=818248562:i=2064:ep=RST_2894 on theBenchmark for (2894ds/2064Mi)
% 159.92/24.32 % (3641480)Instruction limit reached!
% 159.92/24.32 % (3641480)------------------------------
% 159.92/24.32 % (3641480)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 159.92/24.32 % (3641480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 159.92/24.32 % (3641480)CaDiCaL version: 2.1.3
% 159.92/24.32 % (3641480)Termination reason: Instruction limit
% 159.92/24.32 % (3641480)Termination phase: Naming
% 159.92/24.32 % (3641480)Time elapsed: 0.259 s
% 159.92/24.32 % (3641480)Peak memory usage: 135 MB
% 159.92/24.32 % (3641480)Instructions burned: 320 (million)
% 159.92/24.32 % (3641484)dis-1011_128_sil=32000:random_seed=1566707328:i=3706:ep=RST:av=off_2890 on theBenchmark for (2890ds/3706Mi)
% 159.92/24.32 % (3641481)Instruction limit reached!
% 159.92/24.32 % (3641481)------------------------------
% 159.92/24.32 % (3641481)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 159.92/24.32 % (3641481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 159.92/24.32 % (3641481)CaDiCaL version: 2.1.3
% 159.92/24.32 % (3641481)Termination reason: Instruction limit
% 159.92/24.32 % (3641481)Termination phase: Property scanning
% 159.92/24.32 % (3641481)Time elapsed: 1.111 s
% 159.92/24.32 % (3641481)Peak memory usage: 171 MB
% 159.92/24.32 % (3641481)Instructions burned: 2066 (million)
% 159.92/24.32 % (3641486)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=3202803146:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2881 on theBenchmark for (2881ds/757Mi)
% 159.92/24.32 % (3641486)Instruction limit reached!
% 159.92/24.32 % (3641486)------------------------------
% 159.92/24.32 % (3641486)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 159.92/24.32 % (3641486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 159.92/24.32 % (3641486)CaDiCaL version: 2.1.3
% 159.92/24.32 % (3641486)Termination reason: Instruction limit
% 159.92/24.32 % (3641486)Termination phase: Saturation
% 159.92/24.32 % (3641486)Time elapsed: 0.596 s
% 159.92/24.32 % (3641486)Peak memory usage: 122 MB
% 159.92/24.32 % (3641486)Instructions burned: 757 (million)
% 159.92/24.32 % (3641488)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=3231402067:i=13913:ss=axioms:sgt=8_2874 on theBenchmark for (2874ds/13913Mi)
% 159.92/24.32 % (3641484)Instruction limit reached!
% 159.92/24.32 % (3641484)------------------------------
% 159.92/24.32 % (3641484)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 159.92/24.32 % (3641484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 159.92/24.32 % (3641484)CaDiCaL version: 2.1.3
% 159.92/24.32 % (3641484)Termination reason: Instruction limit
% 159.92/24.32 % (3641484)Termination phase: Saturation
% 159.92/24.32 % (3641484)Time elapsed: 1.826 s
% 159.92/24.32 % (3641484)Peak memory usage: 186 MB
% 159.92/24.32 % (3641484)Instructions burned: 3707 (million)
% 159.92/24.32 % (3641490)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=1391019898:i=9925:aac=none_2871 on theBenchmark for (2871ds/9925Mi)
% 159.92/24.32 % (3641468)Instruction limit reached!
% 159.92/24.32 % (3641468)------------------------------
% 159.92/24.32 % (3641468)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 103.92/27.42 % (3641468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 103.92/27.42 % (3641468)CaDiCaL version: 2.1.3
% 103.92/27.42 % (3641468)Termination reason: Instruction limit
% 103.92/27.42 % (3641468)Termination phase: Saturation
% 103.92/27.42 % (3641468)Time elapsed: 9.650 s
% 103.92/27.42 % (3641468)Peak memory usage: 641 MB
% 103.92/27.42 % (3641468)Instructions burned: 14156 (million)
% 103.92/27.42 % (3641493)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=3006724535:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2861 on theBenchmark for (2861ds/2479Mi)
% 103.92/27.42 % (3641493)Instruction limit reached!
% 103.92/27.42 % (3641493)------------------------------
% 103.92/27.42 % (3641493)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 103.92/27.42 % (3641493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 103.92/27.42 % (3641493)CaDiCaL version: 2.1.3
% 103.92/27.42 % (3641493)Termination reason: Instruction limit
% 103.92/27.42 % (3641493)Termination phase: Saturation
% 103.92/27.42 % (3641493)Time elapsed: 1.664 s
% 103.92/27.42 % (3641493)Peak memory usage: 136 MB
% 103.92/27.42 % (3641493)Instructions burned: 2479 (million)
% 103.92/27.42 % (3641495)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=635932733:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2843 on theBenchmark for (2843ds/440Mi)
% 103.92/27.42 % (3641478)Instruction limit reached!
% 103.92/27.42 % (3641478)------------------------------
% 103.92/27.42 % (3641478)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 103.92/27.42 % (3641478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 103.92/27.42 % (3641478)CaDiCaL version: 2.1.3
% 103.92/27.42 % (3641478)Termination reason: Instruction limit
% 103.92/27.42 % (3641478)Termination phase: Saturation
% 103.92/27.42 % (3641478)Time elapsed: 7.618 s
% 103.92/27.42 % (3641478)Peak memory usage: 270 MB
% 103.92/27.42 % (3641478)Instructions burned: 12111 (million)
% 103.92/27.42 % (3641495)Instruction limit reached!
% 103.92/27.42 % (3641495)------------------------------
% 103.92/27.42 % (3641495)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 103.92/27.42 % (3641495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 103.92/27.42 % (3641495)CaDiCaL version: 2.1.3
% 103.92/27.42 % (3641495)Termination reason: Instruction limit
% 103.92/27.42 % (3641495)Termination phase: Property scanning
% 103.92/27.42 % (3641495)Time elapsed: 0.189 s
% 103.92/27.42 % (3641495)Peak memory usage: 112 MB
% 103.92/27.42 % (3641495)Instructions burned: 441 (million)
% 103.92/27.42 % (3641497)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=2762273097:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2841 on theBenchmark for (2841ds/11145Mi)
% 103.92/27.42 % (3641498)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=2836948401:cts=off:i=3034:av=off:er=known:fsd=on_2840 on theBenchmark for (2840ds/3034Mi)
% 103.92/27.42 % (3641498)Instruction limit reached!
% 103.92/27.42 % (3641498)------------------------------
% 103.92/27.42 % (3641498)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 103.92/27.42 % (3641498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 103.92/27.42 % (3641498)CaDiCaL version: 2.1.3
% 103.92/27.42 % (3641498)Termination reason: Instruction limit
% 103.92/27.42 % (3641498)Termination phase: Saturation
% 103.92/27.42 % (3641498)Time elapsed: 1.632 s
% 103.92/27.42 % (3641498)Peak memory usage: 190 MB
% 103.92/27.42 % (3641498)Instructions burned: 3034 (million)
% 103.92/27.42 % (3641501)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=530301026:st=2:s2a=on:i=524:s2at=2:ss=axioms_2822 on theBenchmark for (2822ds/524Mi)
% 103.92/27.42 % (3641501)Instruction limit reached!
% 103.92/27.42 % (3641501)------------------------------
% 103.92/27.42 % (3641501)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 103.92/27.42 % (3641501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 103.92/27.42 % (3641501)CaDiCaL version: 2.1.3
% 103.92/27.42 % (3641501)Termination reason: Instruction limit
% 103.92/27.42 % (3641501)Termination phase: Preprocessing 1
% 103.92/27.42 % (3641501)Time elapsed: 0.392 s
% 103.92/27.42 % (3641501)Peak memory usage: 114 MB
% 103.92/27.42 % (3641501)Instructions burned: 525 (million)
% 103.92/27.42 % (3641503)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=573498266:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2817 on theBenchmark for (2817ds/1016Mi)
% 103.92/27.42 % (3641503)Instruction limit reached!
% 103.92/27.42 % (3641503)------------------------------
% 103.92/27.42 % (3641503)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 103.92/27.42 % (3641503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 103.92/27.42 % (3641503)CaDiCaL version: 2.1.3
% 103.92/27.42 % (3641503)Termination reason: Instruction limit
% 103.92/27.42 % (3641503)Termination phase: Saturation
% 103.92/27.42 % (3641503)Time elapsed: 0.563 s
% 103.92/27.42 % (3641503)Peak memory usage: 135 MB
% 103.92/27.42 % (3641503)Instructions burned: 1017 (million)
% 103.92/27.42 % (3641505)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=950589491:i=14123:bd=preordered:ins=4_2810 on theBenchmark for (2810ds/14123Mi)
% 103.92/27.42 % (3641490)Instruction limit reached!
% 103.92/27.42 % (3641490)------------------------------
% 103.92/27.42 % (3641490)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 103.92/27.42 % (3641490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 103.92/27.42 % (3641490)CaDiCaL version: 2.1.3
% 103.92/27.42 % (3641490)Termination reason: Instruction limit
% 103.92/27.42 % (3641490)Termination phase: Saturation
% 103.92/27.42 % (3641490)Time elapsed: 6.993 s
% 103.92/27.42 % (3641490)Peak memory usage: 774 MB
% 103.92/27.42 % (3641490)Instructions burned: 9926 (million)
% 103.92/27.42 % (3641507)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=148621152:i=5781:kws=precedence:bd=all:rawr=on_2799 on theBenchmark for (2799ds/5781Mi)
% 103.92/27.42 % (3641488)Instruction limit reached!
% 103.92/27.42 % (3641488)------------------------------
% 103.92/27.42 % (3641488)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 103.92/27.42 % (3641488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 103.92/27.42 % (3641488)CaDiCaL version: 2.1.3
% 103.92/27.42 % (3641488)Termination reason: Instruction limit
% 103.92/27.42 % (3641488)Termination phase: Saturation
% 103.92/27.42 % (3641488)Time elapsed: 8.274 s
% 103.92/27.42 % (3641488)Peak memory usage: 279 MB
% 103.92/27.42 % (3641488)Instructions burned: 13914 (million)
% 103.92/27.42 % (3641509)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=2093470500:i=2448:gtgl=5:bd=preordered:gtg=all_2790 on theBenchmark for (2790ds/2448Mi)
% 103.92/27.42 % (3641509)Instruction limit reached!
% 103.92/27.42 % (3641509)------------------------------
% 103.92/27.42 % (3641509)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 103.92/27.42 % (3641509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 103.92/27.42 % (3641509)CaDiCaL version: 2.1.3
% 103.92/27.42 % (3641509)Termination reason: Instruction limit
% 103.92/27.42 % (3641509)Termination phase: Function definition elimination
% 103.92/27.42 % (3641509)Time elapsed: 1.321 s
% 103.92/27.42 % (3641509)Peak memory usage: 168 MB
% 103.92/27.42 % (3641509)Instructions burned: 2449 (million)
% 103.92/27.42 % (3641511)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=1508578980:i=3223:kws=precedence:fgj=on:av=off_2775 on theBenchmark for (2775ds/3223Mi)
% 103.92/27.42 % (3641497)Instruction limit reached!
% 103.92/27.42 % (3641497)------------------------------
% 103.92/27.42 % (3641497)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 103.92/27.42 % (3641497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 103.92/27.42 % (3641497)CaDiCaL version: 2.1.3
% 103.92/27.42 % (3641497)Termination reason: Instruction limit
% 103.92/27.42 % (3641497)Termination phase: Saturation
% 103.92/27.42 % (3641497)Time elapsed: 7.258 s
% 103.92/27.42 % (3641497)Peak memory usage: 244 MB
% 103.92/27.42 % (3641497)Instructions burned: 11146 (million)
% 103.92/27.42 % (3641513)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=667362623:st=5.6:i=2033:sd=3:ss=axioms_2766 on theBenchmark for (2766ds/2033Mi)
% 103.92/27.42 % (3641507)Instruction limit reached!
% 103.92/27.42 % (3641507)------------------------------
% 103.92/27.42 % (3641507)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 103.92/27.42 % (3641507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 103.92/27.42 % (3641507)CaDiCaL version: 2.1.3
% 103.92/27.42 % (3641507)Termination reason: Instruction limit
% 103.92/27.42 % (3641507)Termination phase: Saturation
% 103.92/27.42 % (3641507)Time elapsed: 3.248 s
% 103.92/27.42 % (3641507)Peak memory usage: 203 MB
% 103.92/27.42 % (3641507)Instructions burned: 5782 (million)
% 103.92/27.42 % (3641515)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=498179290:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2765 on theBenchmark for (2765ds/2055Mi)
% 103.92/27.42 % (3641511)Instruction limit reached!
% 103.92/27.42 % (3641511)------------------------------
% 103.92/27.42 % (3641511)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 103.92/27.42 % (3641511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 103.92/27.42 % (3641511)CaDiCaL version: 2.1.3
% 103.92/27.42 % (3641511)Termination reason: Instruction limit
% 103.92/27.42 % (3641511)Termination phase: Saturation
% 103.92/27.42 % (3641511)Time elapsed: 1.826 s
% 103.92/27.42 % (3641511)Peak memory usage: 215 MB
% 103.92/27.42 % (3641511)Instructions burned: 3223 (million)
% 103.92/27.42 % (3641517)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=3894581814:i=21611:sd=3:ss=axioms_2755 on theBenchmark for (2755ds/21611Mi)
% 103.92/27.42 % (3641513)Instruction limit reached!
% 103.92/27.42 % (3641513)------------------------------
% 103.92/27.42 % (3641513)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 103.92/27.42 % (3641513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 103.92/27.42 % (3641513)CaDiCaL version: 2.1.3
% 103.92/27.42 % (3641513)Termination reason: Instruction limit
% 103.92/27.42 % (3641513)Termination phase: Saturation
% 103.92/27.42 % (3641513)Time elapsed: 1.311 s
% 103.92/27.42 % (3641513)Peak memory usage: 190 MB
% 103.92/27.42 % (3641513)Instructions burned: 2033 (million)
% 103.92/27.42 % (3641515)Instruction limit reached!
% 103.92/27.42 % (3641515)------------------------------
% 103.92/27.42 % (3641515)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 103.92/27.42 % (3641515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 103.92/27.42 % (3641515)CaDiCaL version: 2.1.3
% 103.92/27.42 % (3641515)Termination reason: Instruction limit
% 103.92/27.42 % (3641515)Termination phase: Saturation
% 103.92/27.42 % (3641515)Time elapsed: 1.294 s
% 103.92/27.42 % (3641515)Peak memory usage: 185 MB
% 103.92/27.42 % (3641515)Instructions burned: 2056 (million)
% 103.92/27.42 % (3641519)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=1991676987:i=4835:sd=13:ss=axioms:sgt=23_2752 on theBenchmark for (2752ds/4835Mi)
% 103.92/27.42 % (3641521)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=2416396286:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2750 on theBenchmark for (2750ds/797Mi)
% 103.92/27.42 % (3641521)Instruction limit reached!
% 103.92/27.42 % (3641521)------------------------------
% 103.92/27.42 % (3641521)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 103.92/27.42 % (3641521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 103.92/27.42 % (3641521)CaDiCaL version: 2.1.3
% 103.92/27.42 % (3641521)Termination reason: Instruction limit
% 103.92/27.42 % (3641521)Termination phase: NewCNF
% 103.92/27.42 % (3641521)Time elapsed: 0.645 s
% 103.92/27.42 % (3641521)Peak memory usage: 138 MB
% 103.92/27.42 % (3641521)Instructions burned: 798 (million)
% 103.92/27.42 % (3641523)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=1046618841:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2742 on theBenchmark for (2742ds/2326Mi)
% 103.92/27.42 % (3641517)First to succeed.
% 103.92/27.42 % (3641517)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3641407"
% 103.92/27.42 % (3641517)Refutation found. Thanks to Tanya!
% 103.92/27.42 % SZS status Theorem for theBenchmark
% 103.92/27.42 % SZS output start Proof for theBenchmark
% See solution above
% 182.11/27.62 % (3641517)------------------------------
% 182.11/27.62 % (3641517)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 182.11/27.62 % (3641517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 182.11/27.62 % (3641517)CaDiCaL version: 2.1.3
% 182.11/27.62 % (3641517)Termination reason: Refutation
% 182.11/27.62 % (3641517)Time elapsed: 1.639 s
% 182.11/27.62 % (3641517)Peak memory usage: 190 MB
% 182.11/27.62 % (3641517)Instructions burned: 2490 (million)
% 182.11/27.62 % (3641517)------------------------------
% 182.11/27.62 % (3641517)------------------------------
% 182.11/27.62 % (3641407)Success in time 26.555 s
% 182.11/27.62 % Vampire exiting
%------------------------------------------------------------------------------