%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU428+4 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n005.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 171.08s 33.61s
% Output : Refutation 198.85s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 61
% Syntax : Number of formulae : 403 ( 65 unt; 42 def)
% Number of atoms : 2065 ( 123 equ)
% Maximal formula atoms : 19 ( 5 avg)
% Number of connectives : 3033 (1371 ~;1516 |; 76 &)
% ( 44 <=>; 25 =>; 0 <=; 1 <~>)
% Maximal formula depth : 20 ( 7 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 40 ( 38 usr; 35 prp; 0-2 aty)
% Number of functors : 27 ( 27 usr; 13 con; 0-4 aty)
% Number of variables : 468 ( 0 sgn 451 !; 17 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X0,X1] :
( ! [X2] :
( r2_hidden(X2,X0)
<=> r2_hidden(X2,X1) )
=> X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2_tarski) ).
fof(f8,axiom,
! [X0,X1] :
( r1_tarski(X0,X1)
<=> ! [X2] :
( r2_hidden(X2,X0)
=> r2_hidden(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d3_tarski) ).
fof(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/sandbox2/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/sandbox2/benchmark/theBenchmark.p',d3_xboole_0) ).
fof(f38,axiom,
! [X0,X1] :
( X0 = X1
<=> ( r1_tarski(X0,X1)
& r1_tarski(X1,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d10_xboole_0) ).
fof(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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/benchmark/theBenchmark.p',t5_subset) ).
fof(f71075,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/sandbox2/benchmark/theBenchmark.p',dt_k8_relset_2) ).
fof(f71106,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/sandbox2/benchmark/theBenchmark.p',t24_relset_2) ).
fof(f71107,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/sandbox2/benchmark/theBenchmark.p',t25_relset_2) ).
fof(f71109,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/sandbox2/benchmark/theBenchmark.p',t27_relset_2) ).
fof(f71110,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)],[f71109]) ).
fof(f71202,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,[],[f71110]) ).
fof(f71222,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(f71223,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,[],[f71222]) ).
fof(f71226,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(f71227,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,[],[f71226]) ).
fof(f71228,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(f71229,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,[],[f71228]) ).
fof(f71238,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(f71239,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,[],[f71238]) ).
fof(f71240,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(f71241,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,[],[f71240]) ).
fof(f71246,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,[],[f71107]) ).
fof(f71247,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,[],[f71106]) ).
fof(f71248,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,[],[f71247]) ).
fof(f71249,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,[],[f71075]) ).
fof(f71250,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,[],[f71249]) ).
fof(f71260,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(f71261,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(f71262,plain,
! [X0,X1,X2] :
( m1_subset_1(X0,X2)
| ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2)) ),
inference(flattening,[],[f71261]) ).
fof(f71275,plain,
! [X0,X1] :
( X0 = X1
| ? [X2] :
( r2_hidden(X2,X0)
<~> r2_hidden(X2,X1) ) ),
inference(ennf_transformation,[],[f3]) ).
fof(f71311,plain,
! [X0,X1] :
( r1_tarski(X0,X1)
<=> ! [X2] :
( r2_hidden(X2,X1)
| ~ r2_hidden(X2,X0) ) ),
inference(ennf_transformation,[],[f8]) ).
fof(f71766,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(f71767,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,[],[f71766]) ).
fof(f72894,plain,
( k8_relset_2(sK30,sK31,k4_subset_1(sK30,sK32,sK33),sK34) != k5_subset_1(sK31,k8_relset_2(sK30,sK31,sK32,sK34),k8_relset_2(sK30,sK31,sK33,sK34))
& m1_subset_1(sK34,k1_zfmisc_1(k2_zfmisc_1(sK30,sK31)))
& m1_subset_1(sK33,k1_zfmisc_1(sK30))
& m1_subset_1(sK32,k1_zfmisc_1(sK30)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK30,sK31,sK32,sK33,sK34]),skolemize(X0,sK30),skolemize(X1,sK31),skolemize(X2,sK32),skolemize(X3,sK33),skolemize(X4,sK34)],[f71202]) ).
fof(f72906,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,[],[f71246]) ).
fof(f72907,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,[],[f72906]) ).
fof(f72908,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(sK42(X2,X3,X4))))
& r2_hidden(sK42(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,[sK42]),skolemize(X5,sK42(X2,X3,X4))],[f72907]) ).
fof(f72929,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,[],[f71275]) ).
fof(f72930,plain,
! [X0,X1] :
( X0 = X1
| ( ( ~ r2_hidden(sK55(X0,X1),X1)
| ~ r2_hidden(sK55(X0,X1),X0) )
& ( r2_hidden(sK55(X0,X1),X1)
| r2_hidden(sK55(X0,X1),X0) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK55]),skolemize(X2,sK55(X0,X1))],[f72929]) ).
fof(f72941,plain,
! [X0,X1] :
( ( X0 = X1
| ~ r1_tarski(X0,X1)
| ~ r1_tarski(X1,X0) )
& ( ( r1_tarski(X0,X1)
& r1_tarski(X1,X0) )
| X0 != X1 ) ),
inference(nnf_transformation,[],[f38]) ).
fof(f72942,plain,
! [X0,X1] :
( ( X0 = X1
| ~ r1_tarski(X0,X1)
| ~ r1_tarski(X1,X0) )
& ( ( r1_tarski(X0,X1)
& r1_tarski(X1,X0) )
| X0 != X1 ) ),
inference(flattening,[],[f72941]) ).
fof(f72943,plain,
! [X0,X1] :
( ( r1_tarski(X0,X1)
| ? [X2] :
( ~ r2_hidden(X2,X1)
& r2_hidden(X2,X0) ) )
& ( ! [X2] :
( r2_hidden(X2,X1)
| ~ r2_hidden(X2,X0) )
| ~ r1_tarski(X0,X1) ) ),
inference(nnf_transformation,[],[f71311]) ).
fof(f72944,plain,
! [X0,X1] :
( ( r1_tarski(X0,X1)
| ? [X2] :
( ~ r2_hidden(X2,X1)
& r2_hidden(X2,X0) ) )
& ( ! [X3] :
( r2_hidden(X3,X1)
| ~ r2_hidden(X3,X0) )
| ~ r1_tarski(X0,X1) ) ),
inference(rectify,[],[f72943]) ).
fof(f72945,plain,
! [X0,X1] :
( ( r1_tarski(X0,X1)
| ( ~ r2_hidden(sK63(X0,X1),X1)
& r2_hidden(sK63(X0,X1),X0) ) )
& ( ! [X3] :
( r2_hidden(X3,X1)
| ~ r2_hidden(X3,X0) )
| ~ r1_tarski(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK63]),skolemize(X2,sK63(X0,X1))],[f72944]) ).
fof(f72960,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(f72961,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,[],[f72960]) ).
fof(f72962,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,[],[f72961]) ).
fof(f72963,plain,
! [X0,X1,X2] :
( ( X2 = k2_xboole_0(X0,X1)
| ( ( ( ~ r2_hidden(sK72(X0,X1,X2),X0)
& ~ r2_hidden(sK72(X0,X1,X2),X1) )
| ~ r2_hidden(sK72(X0,X1,X2),X2) )
& ( r2_hidden(sK72(X0,X1,X2),X0)
| r2_hidden(sK72(X0,X1,X2),X1)
| r2_hidden(sK72(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,[sK72]),skolemize(X3,sK72(X0,X1,X2))],[f72962]) ).
fof(f73134,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(f73135,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,[],[f73134]) ).
fof(f73136,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,[],[f73135]) ).
fof(f73137,plain,
! [X0,X1,X2] :
( ( X2 = k3_xboole_0(X0,X1)
| ( ( ~ r2_hidden(sK187(X0,X1,X2),X0)
| ~ r2_hidden(sK187(X0,X1,X2),X1)
| ~ r2_hidden(sK187(X0,X1,X2),X2) )
& ( ( r2_hidden(sK187(X0,X1,X2),X0)
& r2_hidden(sK187(X0,X1,X2),X1) )
| r2_hidden(sK187(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,[sK187]),skolemize(X3,sK187(X0,X1,X2))],[f73136]) ).
fof(f73550,plain,
m1_subset_1(sK32,k1_zfmisc_1(sK30)),
inference(cnf_transformation,[],[f72894]) ).
fof(f73551,plain,
m1_subset_1(sK33,k1_zfmisc_1(sK30)),
inference(cnf_transformation,[],[f72894]) ).
fof(f73552,plain,
m1_subset_1(sK34,k1_zfmisc_1(k2_zfmisc_1(sK30,sK31))),
inference(cnf_transformation,[],[f72894]) ).
fof(f73553,plain,
k8_relset_2(sK30,sK31,k4_subset_1(sK30,sK32,sK33),sK34) != k5_subset_1(sK31,k8_relset_2(sK30,sK31,sK32,sK34),k8_relset_2(sK30,sK31,sK33,sK34)),
inference(cnf_transformation,[],[f72894]) ).
fof(f73582,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,[],[f71223]) ).
fof(f73584,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,[],[f71227]) ).
fof(f73585,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,[],[f71229]) ).
fof(f73597,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,[],[f71239]) ).
fof(f73598,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,[],[f71241]) ).
fof(f73605,plain,
! [X2,X3,X0,X1,X4] :
( r2_hidden(X3,k8_relset_2(X1,X0,X2,X4))
| r2_hidden(sK42(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,[],[f72908]) ).
fof(f73606,plain,
! [X2,X3,X0,X1,X4] :
( ~ r2_hidden(X3,k9_relat_1(X4,k1_tarski(sK42(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,[],[f72908]) ).
fof(f73607,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,[],[f71248]) ).
fof(f73608,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,[],[f71250]) ).
fof(f73635,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ r2_hidden(X0,X1)
| ~ v1_xboole_0(X2) ),
inference(cnf_transformation,[],[f71260]) ).
fof(f73636,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ r2_hidden(X0,X1)
| m1_subset_1(X0,X2) ),
inference(cnf_transformation,[],[f71262]) ).
fof(f73654,plain,
! [X0,X1] :
( r2_hidden(sK55(X0,X1),X1)
| X0 = X1
| r2_hidden(sK55(X0,X1),X0) ),
inference(cnf_transformation,[],[f72930]) ).
fof(f73696,plain,
! [X0,X1] :
( ~ r1_tarski(X1,X0)
| ~ r1_tarski(X0,X1)
| X0 = X1 ),
inference(cnf_transformation,[],[f72942]) ).
fof(f73699,plain,
! [X0,X1] :
( r2_hidden(sK63(X0,X1),X0)
| r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f72945]) ).
fof(f73700,plain,
! [X0,X1] :
( ~ r2_hidden(sK63(X0,X1),X1)
| r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f72945]) ).
fof(f73786,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,[],[f72963]) ).
fof(f73787,plain,
! [X2,X0,X1,X4] :
( r2_hidden(X4,X2)
| ~ r2_hidden(X4,X1)
| k2_xboole_0(X0,X1) != X2 ),
inference(cnf_transformation,[],[f72963]) ).
fof(f74414,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,[],[f71767]) ).
fof(f74470,plain,
! [X2,X0,X1,X4] :
( r2_hidden(X4,X1)
| ~ r2_hidden(X4,X2)
| k3_xboole_0(X0,X1) != X2 ),
inference(cnf_transformation,[],[f73137]) ).
fof(f74472,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,[],[f73137]) ).
fof(f75990,plain,
! [X0,X1,X4] :
( r2_hidden(X4,k2_xboole_0(X0,X1))
| ~ r2_hidden(X4,X1) ),
inference(equality_resolution,[],[f73787]) ).
fof(f75991,plain,
! [X0,X1,X4] :
( ~ r2_hidden(X4,k2_xboole_0(X0,X1))
| r2_hidden(X4,X1)
| r2_hidden(X4,X0) ),
inference(equality_resolution,[],[f73786]) ).
fof(f76049,plain,
! [X0,X1,X4] :
( r2_hidden(X4,k3_xboole_0(X0,X1))
| ~ r2_hidden(X4,X0)
| ~ r2_hidden(X4,X1) ),
inference(equality_resolution,[],[f74472]) ).
fof(f76051,plain,
! [X0,X1,X4] :
( ~ r2_hidden(X4,k3_xboole_0(X0,X1))
| r2_hidden(X4,X1) ),
inference(equality_resolution,[],[f74470]) ).
fof(f76179,definition,
sF477 = k4_subset_1(sK30,sK32,sK33),
introduced(definition,[new_symbols(definition,[sF477])],[function_definition]) ).
fof(f76180,plain,
k4_subset_1(sK30,sK32,sK33) = sF477,
inference(reorient_equations,[],[f76179]) ).
fof(f76181,definition,
sF478 = k8_relset_2(sK30,sK31,sF477,sK34),
introduced(definition,[new_symbols(definition,[sF478])],[function_definition]) ).
fof(f76182,plain,
k8_relset_2(sK30,sK31,sF477,sK34) = sF478,
inference(reorient_equations,[],[f76181]) ).
fof(f76183,definition,
sF479 = k8_relset_2(sK30,sK31,sK32,sK34),
introduced(definition,[new_symbols(definition,[sF479])],[function_definition]) ).
fof(f76184,plain,
k8_relset_2(sK30,sK31,sK32,sK34) = sF479,
inference(reorient_equations,[],[f76183]) ).
fof(f76185,definition,
sF480 = k8_relset_2(sK30,sK31,sK33,sK34),
introduced(definition,[new_symbols(definition,[sF480])],[function_definition]) ).
fof(f76186,plain,
k8_relset_2(sK30,sK31,sK33,sK34) = sF480,
inference(reorient_equations,[],[f76185]) ).
fof(f76187,definition,
sF481 = k5_subset_1(sK31,sF479,sF480),
introduced(definition,[new_symbols(definition,[sF481])],[function_definition]) ).
fof(f76188,plain,
k5_subset_1(sK31,sF479,sF480) = sF481,
inference(reorient_equations,[],[f76187]) ).
fof(f76189,plain,
sF478 != sF481,
inference(definition_folding,[],[f73553,f76188,f76186,f76184,f76182,f76180]) ).
fof(f76190,definition,
sF482 = k2_zfmisc_1(sK30,sK31),
introduced(definition,[new_symbols(definition,[sF482])],[function_definition]) ).
fof(f76191,plain,
k2_zfmisc_1(sK30,sK31) = sF482,
inference(reorient_equations,[],[f76190]) ).
fof(f76192,definition,
sF483 = k1_zfmisc_1(sF482),
introduced(definition,[new_symbols(definition,[sF483])],[function_definition]) ).
fof(f76193,plain,
k1_zfmisc_1(sF482) = sF483,
inference(reorient_equations,[],[f76192]) ).
fof(f76194,plain,
m1_subset_1(sK34,sF483),
inference(definition_folding,[],[f73552,f76193,f76191]) ).
fof(f76195,definition,
sF484 = k1_zfmisc_1(sK30),
introduced(definition,[new_symbols(definition,[sF484])],[function_definition]) ).
fof(f76196,plain,
k1_zfmisc_1(sK30) = sF484,
inference(reorient_equations,[],[f76195]) ).
fof(f76197,plain,
m1_subset_1(sK33,sF484),
inference(definition_folding,[],[f73551,f76196]) ).
fof(f76198,plain,
m1_subset_1(sK32,sF484),
inference(definition_folding,[],[f73550,f76196]) ).
fof(f76709,definition,
( spl485_101
<=> m1_subset_1(sK32,sF484) ),
introduced(definition,[new_symbols(definition,[spl485_101])],[avatar_definition]) ).
fof(f76711,plain,
( m1_subset_1(sK32,sF484)
| ~ spl485_101 ),
inference(avatar_component_clause,[],[f76709]) ).
fof(f76712,plain,
spl485_101,
inference(avatar_split_clause,[],[f76198,f76709]) ).
fof(f76714,definition,
( spl485_102
<=> m1_subset_1(sK33,sF484) ),
introduced(definition,[new_symbols(definition,[spl485_102])],[avatar_definition]) ).
fof(f76716,plain,
( m1_subset_1(sK33,sF484)
| ~ spl485_102 ),
inference(avatar_component_clause,[],[f76714]) ).
fof(f76717,plain,
spl485_102,
inference(avatar_split_clause,[],[f76197,f76714]) ).
fof(f76719,definition,
( spl485_103
<=> m1_subset_1(sK34,sF483) ),
introduced(definition,[new_symbols(definition,[spl485_103])],[avatar_definition]) ).
fof(f76721,plain,
( m1_subset_1(sK34,sF483)
| ~ spl485_103 ),
inference(avatar_component_clause,[],[f76719]) ).
fof(f76722,plain,
spl485_103,
inference(avatar_split_clause,[],[f76194,f76719]) ).
fof(f76724,definition,
( spl485_104
<=> sF478 = sF481 ),
introduced(definition,[new_symbols(definition,[spl485_104])],[avatar_definition]) ).
fof(f76726,plain,
( sF478 != sF481
| spl485_104 ),
inference(avatar_component_clause,[],[f76724]) ).
fof(f76727,plain,
~ spl485_104,
inference(avatar_split_clause,[],[f76189,f76724]) ).
fof(f76734,definition,
( spl485_106
<=> k4_subset_1(sK30,sK32,sK33) = sF477 ),
introduced(definition,[new_symbols(definition,[spl485_106])],[avatar_definition]) ).
fof(f76736,plain,
( k4_subset_1(sK30,sK32,sK33) = sF477
| ~ spl485_106 ),
inference(avatar_component_clause,[],[f76734]) ).
fof(f76737,plain,
spl485_106,
inference(avatar_split_clause,[],[f76180,f76734]) ).
fof(f76739,definition,
( spl485_107
<=> k8_relset_2(sK30,sK31,sF477,sK34) = sF478 ),
introduced(definition,[new_symbols(definition,[spl485_107])],[avatar_definition]) ).
fof(f76741,plain,
( k8_relset_2(sK30,sK31,sF477,sK34) = sF478
| ~ spl485_107 ),
inference(avatar_component_clause,[],[f76739]) ).
fof(f76742,plain,
spl485_107,
inference(avatar_split_clause,[],[f76182,f76739]) ).
fof(f76744,definition,
( spl485_108
<=> k8_relset_2(sK30,sK31,sK32,sK34) = sF479 ),
introduced(definition,[new_symbols(definition,[spl485_108])],[avatar_definition]) ).
fof(f76746,plain,
( k8_relset_2(sK30,sK31,sK32,sK34) = sF479
| ~ spl485_108 ),
inference(avatar_component_clause,[],[f76744]) ).
fof(f76747,plain,
spl485_108,
inference(avatar_split_clause,[],[f76184,f76744]) ).
fof(f76749,definition,
( spl485_109
<=> k8_relset_2(sK30,sK31,sK33,sK34) = sF480 ),
introduced(definition,[new_symbols(definition,[spl485_109])],[avatar_definition]) ).
fof(f76751,plain,
( k8_relset_2(sK30,sK31,sK33,sK34) = sF480
| ~ spl485_109 ),
inference(avatar_component_clause,[],[f76749]) ).
fof(f76752,plain,
spl485_109,
inference(avatar_split_clause,[],[f76186,f76749]) ).
fof(f76754,definition,
( spl485_110
<=> k5_subset_1(sK31,sF479,sF480) = sF481 ),
introduced(definition,[new_symbols(definition,[spl485_110])],[avatar_definition]) ).
fof(f76756,plain,
( k5_subset_1(sK31,sF479,sF480) = sF481
| ~ spl485_110 ),
inference(avatar_component_clause,[],[f76754]) ).
fof(f76757,plain,
spl485_110,
inference(avatar_split_clause,[],[f76188,f76754]) ).
fof(f76759,definition,
( spl485_111
<=> k2_zfmisc_1(sK30,sK31) = sF482 ),
introduced(definition,[new_symbols(definition,[spl485_111])],[avatar_definition]) ).
fof(f76761,plain,
( k2_zfmisc_1(sK30,sK31) = sF482
| ~ spl485_111 ),
inference(avatar_component_clause,[],[f76759]) ).
fof(f76762,plain,
spl485_111,
inference(avatar_split_clause,[],[f76191,f76759]) ).
fof(f76764,definition,
( spl485_112
<=> k1_zfmisc_1(sF482) = sF483 ),
introduced(definition,[new_symbols(definition,[spl485_112])],[avatar_definition]) ).
fof(f76766,plain,
( k1_zfmisc_1(sF482) = sF483
| ~ spl485_112 ),
inference(avatar_component_clause,[],[f76764]) ).
fof(f76767,plain,
spl485_112,
inference(avatar_split_clause,[],[f76193,f76764]) ).
fof(f76769,definition,
( spl485_113
<=> k1_zfmisc_1(sK30) = sF484 ),
introduced(definition,[new_symbols(definition,[spl485_113])],[avatar_definition]) ).
fof(f76771,plain,
( k1_zfmisc_1(sK30) = sF484
| ~ spl485_113 ),
inference(avatar_component_clause,[],[f76769]) ).
fof(f76772,plain,
spl485_113,
inference(avatar_split_clause,[],[f76196,f76769]) ).
fof(f76773,plain,
( m1_subset_1(sF478,k1_zfmisc_1(sK31))
| ~ m1_subset_1(sF477,k1_zfmisc_1(sK30))
| ~ m1_subset_1(sK34,k1_zfmisc_1(k2_zfmisc_1(sK30,sK31)))
| ~ spl485_107 ),
inference(superposition,[],[f73608,f76741]) ).
fof(f76775,definition,
( spl485_114
<=> m1_subset_1(sK34,k1_zfmisc_1(k2_zfmisc_1(sK30,sK31))) ),
introduced(definition,[new_symbols(definition,[spl485_114])],[avatar_definition]) ).
fof(f76779,definition,
( spl485_115
<=> m1_subset_1(sF477,k1_zfmisc_1(sK30)) ),
introduced(definition,[new_symbols(definition,[spl485_115])],[avatar_definition]) ).
fof(f76783,definition,
( spl485_116
<=> m1_subset_1(sF478,k1_zfmisc_1(sK31)) ),
introduced(definition,[new_symbols(definition,[spl485_116])],[avatar_definition]) ).
fof(f76785,plain,
( m1_subset_1(sF478,k1_zfmisc_1(sK31))
| ~ spl485_116 ),
inference(avatar_component_clause,[],[f76783]) ).
fof(f76786,plain,
( ~ spl485_114
| ~ spl485_115
| spl485_116
| ~ spl485_107 ),
inference(avatar_split_clause,[],[f76773,f76739,f76783,f76779,f76775]) ).
fof(f76787,plain,
( k2_zfmisc_1(sK30,sK31) != sF482
| k1_zfmisc_1(sF482) != sF483
| m1_subset_1(sK34,k1_zfmisc_1(k2_zfmisc_1(sK30,sK31)))
| ~ m1_subset_1(sK34,sF483) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f76789,plain,
( m1_subset_1(sF480,k1_zfmisc_1(sK31))
| ~ m1_subset_1(sK33,k1_zfmisc_1(sK30))
| ~ m1_subset_1(sK34,k1_zfmisc_1(k2_zfmisc_1(sK30,sK31)))
| ~ spl485_109 ),
inference(superposition,[],[f73608,f76751]) ).
fof(f76790,plain,
( ~ m1_subset_1(sK33,sF484)
| m1_subset_1(sF480,k1_zfmisc_1(sK31))
| ~ m1_subset_1(sK34,k1_zfmisc_1(k2_zfmisc_1(sK30,sK31)))
| ~ spl485_109
| ~ spl485_113 ),
inference(forward_demodulation,[],[f76789,f76771]) ).
fof(f76791,plain,
( m1_subset_1(sF480,k1_zfmisc_1(sK31))
| ~ m1_subset_1(sK34,k1_zfmisc_1(k2_zfmisc_1(sK30,sK31)))
| ~ spl485_102
| ~ spl485_109
| ~ spl485_113 ),
inference(forward_subsumption_resolution,[],[f76790,f76716]) ).
fof(f76793,definition,
( spl485_117
<=> m1_subset_1(sF480,k1_zfmisc_1(sK31)) ),
introduced(definition,[new_symbols(definition,[spl485_117])],[avatar_definition]) ).
fof(f76795,plain,
( m1_subset_1(sF480,k1_zfmisc_1(sK31))
| ~ spl485_117 ),
inference(avatar_component_clause,[],[f76793]) ).
fof(f76796,plain,
( ~ spl485_114
| spl485_117
| ~ spl485_102
| ~ spl485_109
| ~ spl485_113 ),
inference(avatar_split_clause,[],[f76791,f76769,f76749,f76714,f76793,f76775]) ).
fof(f76797,plain,
( m1_subset_1(sF479,k1_zfmisc_1(sK31))
| ~ m1_subset_1(sK32,k1_zfmisc_1(sK30))
| ~ m1_subset_1(sK34,k1_zfmisc_1(k2_zfmisc_1(sK30,sK31)))
| ~ spl485_108 ),
inference(superposition,[],[f73608,f76746]) ).
fof(f76798,plain,
( ~ m1_subset_1(sK32,sF484)
| m1_subset_1(sF479,k1_zfmisc_1(sK31))
| ~ m1_subset_1(sK34,k1_zfmisc_1(k2_zfmisc_1(sK30,sK31)))
| ~ spl485_108
| ~ spl485_113 ),
inference(forward_demodulation,[],[f76797,f76771]) ).
fof(f76799,plain,
( m1_subset_1(sF479,k1_zfmisc_1(sK31))
| ~ m1_subset_1(sK34,k1_zfmisc_1(k2_zfmisc_1(sK30,sK31)))
| ~ spl485_101
| ~ spl485_108
| ~ spl485_113 ),
inference(forward_subsumption_resolution,[],[f76798,f76711]) ).
fof(f76801,definition,
( spl485_118
<=> m1_subset_1(sF479,k1_zfmisc_1(sK31)) ),
introduced(definition,[new_symbols(definition,[spl485_118])],[avatar_definition]) ).
fof(f76803,plain,
( m1_subset_1(sF479,k1_zfmisc_1(sK31))
| ~ spl485_118 ),
inference(avatar_component_clause,[],[f76801]) ).
fof(f76804,plain,
( ~ spl485_114
| spl485_118
| ~ spl485_101
| ~ spl485_108
| ~ spl485_113 ),
inference(avatar_split_clause,[],[f76799,f76769,f76744,f76709,f76801,f76775]) ).
fof(f76805,plain,
( sF481 = k3_xboole_0(sF479,sF480)
| ~ m1_subset_1(sF479,k1_zfmisc_1(sK31))
| ~ m1_subset_1(sF480,k1_zfmisc_1(sK31))
| ~ spl485_110 ),
inference(superposition,[],[f74414,f76756]) ).
fof(f76808,definition,
( spl485_119
<=> sF481 = k3_xboole_0(sF479,sF480) ),
introduced(definition,[new_symbols(definition,[spl485_119])],[avatar_definition]) ).
fof(f76810,plain,
( sF481 = k3_xboole_0(sF479,sF480)
| ~ spl485_119 ),
inference(avatar_component_clause,[],[f76808]) ).
fof(f76812,plain,
( ~ spl485_117
| ~ spl485_118
| spl485_119
| ~ spl485_110 ),
inference(avatar_split_clause,[],[f76805,f76754,f76808,f76801,f76793]) ).
fof(f76817,plain,
( sF477 = k2_xboole_0(sK32,sK33)
| ~ m1_subset_1(sK32,k1_zfmisc_1(sK30))
| ~ m1_subset_1(sK33,k1_zfmisc_1(sK30))
| ~ spl485_106 ),
inference(superposition,[],[f76736,f73582]) ).
fof(f76818,plain,
( ~ m1_subset_1(sK32,sF484)
| sF477 = k2_xboole_0(sK32,sK33)
| ~ m1_subset_1(sK33,k1_zfmisc_1(sK30))
| ~ spl485_106
| ~ spl485_113 ),
inference(forward_demodulation,[],[f76817,f76771]) ).
fof(f76820,plain,
( sF477 = k2_xboole_0(sK32,sK33)
| ~ m1_subset_1(sK33,k1_zfmisc_1(sK30))
| ~ spl485_101
| ~ spl485_106
| ~ spl485_113 ),
inference(forward_subsumption_resolution,[],[f76818,f76711]) ).
fof(f76822,plain,
( ~ m1_subset_1(sK33,sF484)
| sF477 = k2_xboole_0(sK32,sK33)
| ~ spl485_101
| ~ spl485_106
| ~ spl485_113 ),
inference(forward_demodulation,[],[f76820,f76771]) ).
fof(f76824,plain,
( sF477 = k2_xboole_0(sK32,sK33)
| ~ spl485_101
| ~ spl485_102
| ~ spl485_106
| ~ spl485_113 ),
inference(forward_subsumption_resolution,[],[f76822,f76716]) ).
fof(f76827,definition,
( spl485_120
<=> sF477 = k2_xboole_0(sK32,sK33) ),
introduced(definition,[new_symbols(definition,[spl485_120])],[avatar_definition]) ).
fof(f76829,plain,
( sF477 = k2_xboole_0(sK32,sK33)
| ~ spl485_120 ),
inference(avatar_component_clause,[],[f76827]) ).
fof(f76830,plain,
( spl485_120
| ~ spl485_101
| ~ spl485_102
| ~ spl485_106
| ~ spl485_113 ),
inference(avatar_split_clause,[],[f76824,f76769,f76734,f76714,f76709,f76827]) ).
fof(f76832,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,[],[f73597,f74414]) ).
fof(f76837,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,[],[f76832]) ).
fof(f76840,plain,
( m1_subset_1(sF477,k1_zfmisc_1(sK30))
| ~ m1_subset_1(sK32,k1_zfmisc_1(sK30))
| ~ m1_subset_1(sK33,k1_zfmisc_1(sK30))
| ~ spl485_106 ),
inference(superposition,[],[f73585,f76736]) ).
fof(f76845,plain,
( m1_subset_1(sF477,sF484)
| ~ m1_subset_1(sK32,k1_zfmisc_1(sK30))
| ~ m1_subset_1(sK33,k1_zfmisc_1(sK30))
| ~ spl485_106
| ~ spl485_113 ),
inference(forward_demodulation,[],[f76840,f76771]) ).
fof(f76846,plain,
( ~ m1_subset_1(sK32,sF484)
| m1_subset_1(sF477,sF484)
| ~ m1_subset_1(sK33,k1_zfmisc_1(sK30))
| ~ spl485_106
| ~ spl485_113 ),
inference(forward_demodulation,[],[f76845,f76771]) ).
fof(f76847,plain,
( m1_subset_1(sF477,sF484)
| ~ m1_subset_1(sK33,k1_zfmisc_1(sK30))
| ~ spl485_101
| ~ spl485_106
| ~ spl485_113 ),
inference(forward_subsumption_resolution,[],[f76846,f76711]) ).
fof(f76848,plain,
( ~ m1_subset_1(sK33,sF484)
| m1_subset_1(sF477,sF484)
| ~ spl485_101
| ~ spl485_106
| ~ spl485_113 ),
inference(forward_demodulation,[],[f76847,f76771]) ).
fof(f76849,plain,
( m1_subset_1(sF477,sF484)
| ~ spl485_101
| ~ spl485_102
| ~ spl485_106
| ~ spl485_113 ),
inference(forward_subsumption_resolution,[],[f76848,f76716]) ).
fof(f76851,definition,
( spl485_121
<=> m1_subset_1(sF477,sF484) ),
introduced(definition,[new_symbols(definition,[spl485_121])],[avatar_definition]) ).
fof(f76853,plain,
( m1_subset_1(sF477,sF484)
| ~ spl485_121 ),
inference(avatar_component_clause,[],[f76851]) ).
fof(f76854,plain,
( spl485_121
| ~ spl485_101
| ~ spl485_102
| ~ spl485_106
| ~ spl485_113 ),
inference(avatar_split_clause,[],[f76849,f76769,f76734,f76714,f76709,f76851]) ).
fof(f76855,plain,
( k1_zfmisc_1(sK30) != sF484
| m1_subset_1(sF477,k1_zfmisc_1(sK30))
| ~ m1_subset_1(sF477,sF484) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f76859,plain,
( m1_subset_1(sF481,k1_zfmisc_1(sK31))
| ~ m1_subset_1(sF479,k1_zfmisc_1(sK31))
| ~ m1_subset_1(sF480,k1_zfmisc_1(sK31))
| ~ spl485_110 ),
inference(superposition,[],[f73598,f76756]) ).
fof(f76868,plain,
( m1_subset_1(sF481,k1_zfmisc_1(sK31))
| ~ m1_subset_1(sF480,k1_zfmisc_1(sK31))
| ~ spl485_110
| ~ spl485_118 ),
inference(forward_subsumption_resolution,[],[f76859,f76803]) ).
fof(f76869,plain,
( m1_subset_1(sF481,k1_zfmisc_1(sK31))
| ~ spl485_110
| ~ spl485_117
| ~ spl485_118 ),
inference(forward_subsumption_resolution,[],[f76868,f76795]) ).
fof(f76871,definition,
( spl485_122
<=> m1_subset_1(sF481,k1_zfmisc_1(sK31)) ),
introduced(definition,[new_symbols(definition,[spl485_122])],[avatar_definition]) ).
fof(f76873,plain,
( m1_subset_1(sF481,k1_zfmisc_1(sK31))
| ~ spl485_122 ),
inference(avatar_component_clause,[],[f76871]) ).
fof(f76874,plain,
( spl485_122
| ~ spl485_110
| ~ spl485_117
| ~ spl485_118 ),
inference(avatar_split_clause,[],[f76869,f76801,f76793,f76754,f76871]) ).
fof(f76876,plain,
! [X2,X0,X1] :
( k2_xboole_0(X0,X1) = k4_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,[],[f73584,f73582]) ).
fof(f76885,plain,
! [X2,X0,X1] :
( k2_xboole_0(X0,X1) = k4_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,[],[f76876]) ).
fof(f76888,plain,
( ! [X0,X1] :
( ~ r2_hidden(X0,sF480)
| ~ r2_hidden(X1,sK33)
| r2_hidden(X0,k9_relat_1(sK34,k1_tarski(X1)))
| ~ m1_subset_1(sK34,k1_zfmisc_1(k2_zfmisc_1(sK30,sK31)))
| ~ m1_subset_1(sK33,k1_zfmisc_1(sK30)) )
| ~ spl485_109 ),
inference(superposition,[],[f73607,f76751]) ).
fof(f76889,plain,
( ! [X0,X1] :
( ~ r2_hidden(X0,sF479)
| ~ r2_hidden(X1,sK32)
| r2_hidden(X0,k9_relat_1(sK34,k1_tarski(X1)))
| ~ m1_subset_1(sK34,k1_zfmisc_1(k2_zfmisc_1(sK30,sK31)))
| ~ m1_subset_1(sK32,k1_zfmisc_1(sK30)) )
| ~ spl485_108 ),
inference(superposition,[],[f73607,f76746]) ).
fof(f76890,plain,
( ! [X0,X1] :
( ~ m1_subset_1(sK34,k1_zfmisc_1(sF482))
| ~ r2_hidden(X0,sF479)
| ~ r2_hidden(X1,sK32)
| r2_hidden(X0,k9_relat_1(sK34,k1_tarski(X1)))
| ~ m1_subset_1(sK32,k1_zfmisc_1(sK30)) )
| ~ spl485_108
| ~ spl485_111 ),
inference(forward_demodulation,[],[f76889,f76761]) ).
fof(f76891,plain,
( ! [X0,X1] :
( ~ m1_subset_1(sK34,k1_zfmisc_1(sF482))
| ~ r2_hidden(X0,sF480)
| ~ r2_hidden(X1,sK33)
| r2_hidden(X0,k9_relat_1(sK34,k1_tarski(X1)))
| ~ m1_subset_1(sK33,k1_zfmisc_1(sK30)) )
| ~ spl485_109
| ~ spl485_111 ),
inference(forward_demodulation,[],[f76888,f76761]) ).
fof(f76893,plain,
( ! [X0,X1] :
( ~ m1_subset_1(sK34,sF483)
| ~ r2_hidden(X0,sF479)
| ~ r2_hidden(X1,sK32)
| r2_hidden(X0,k9_relat_1(sK34,k1_tarski(X1)))
| ~ m1_subset_1(sK32,k1_zfmisc_1(sK30)) )
| ~ spl485_108
| ~ spl485_111
| ~ spl485_112 ),
inference(forward_demodulation,[],[f76890,f76766]) ).
fof(f76894,plain,
( ! [X0,X1] :
( ~ m1_subset_1(sK34,sF483)
| ~ r2_hidden(X0,sF480)
| ~ r2_hidden(X1,sK33)
| r2_hidden(X0,k9_relat_1(sK34,k1_tarski(X1)))
| ~ m1_subset_1(sK33,k1_zfmisc_1(sK30)) )
| ~ spl485_109
| ~ spl485_111
| ~ spl485_112 ),
inference(forward_demodulation,[],[f76891,f76766]) ).
fof(f76896,plain,
( ! [X0,X1] :
( ~ r2_hidden(X0,sF479)
| ~ r2_hidden(X1,sK32)
| r2_hidden(X0,k9_relat_1(sK34,k1_tarski(X1)))
| ~ m1_subset_1(sK32,k1_zfmisc_1(sK30)) )
| ~ spl485_103
| ~ spl485_108
| ~ spl485_111
| ~ spl485_112 ),
inference(forward_subsumption_resolution,[],[f76893,f76721]) ).
fof(f76897,plain,
( ! [X0,X1] :
( ~ r2_hidden(X0,sF480)
| ~ r2_hidden(X1,sK33)
| r2_hidden(X0,k9_relat_1(sK34,k1_tarski(X1)))
| ~ m1_subset_1(sK33,k1_zfmisc_1(sK30)) )
| ~ spl485_103
| ~ spl485_109
| ~ spl485_111
| ~ spl485_112 ),
inference(forward_subsumption_resolution,[],[f76894,f76721]) ).
fof(f76899,plain,
( ! [X0,X1] :
( ~ m1_subset_1(sK32,sF484)
| ~ r2_hidden(X0,sF479)
| ~ r2_hidden(X1,sK32)
| r2_hidden(X0,k9_relat_1(sK34,k1_tarski(X1))) )
| ~ spl485_103
| ~ spl485_108
| ~ spl485_111
| ~ spl485_112
| ~ spl485_113 ),
inference(forward_demodulation,[],[f76896,f76771]) ).
fof(f76900,plain,
( ! [X0,X1] :
( ~ m1_subset_1(sK33,sF484)
| ~ r2_hidden(X0,sF480)
| ~ r2_hidden(X1,sK33)
| r2_hidden(X0,k9_relat_1(sK34,k1_tarski(X1))) )
| ~ spl485_103
| ~ spl485_109
| ~ spl485_111
| ~ spl485_112
| ~ spl485_113 ),
inference(forward_demodulation,[],[f76897,f76771]) ).
fof(f76902,plain,
( ! [X0,X1] :
( r2_hidden(X0,k9_relat_1(sK34,k1_tarski(X1)))
| ~ r2_hidden(X1,sK32)
| ~ r2_hidden(X0,sF479) )
| ~ spl485_101
| ~ spl485_103
| ~ spl485_108
| ~ spl485_111
| ~ spl485_112
| ~ spl485_113 ),
inference(forward_subsumption_resolution,[],[f76899,f76711]) ).
fof(f76903,plain,
( ! [X0,X1] :
( r2_hidden(X0,k9_relat_1(sK34,k1_tarski(X1)))
| ~ r2_hidden(X1,sK33)
| ~ r2_hidden(X0,sF480) )
| ~ spl485_102
| ~ spl485_103
| ~ spl485_109
| ~ spl485_111
| ~ spl485_112
| ~ spl485_113 ),
inference(forward_subsumption_resolution,[],[f76900,f76716]) ).
fof(f76909,plain,
! [X2,X3,X0,X1,X4,X5] :
( r2_hidden(sK63(k8_relset_2(X0,X1,X2,X3),X4),k9_relat_1(X3,k1_tarski(X5)))
| ~ r2_hidden(X5,X2)
| r1_tarski(k8_relset_2(X0,X1,X2,X3),X4)
| ~ m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(resolution,[],[f73699,f73607]) ).
fof(f76923,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF478)
| m1_subset_1(X0,sK31) )
| ~ spl485_116 ),
inference(resolution,[],[f73636,f76785]) ).
fof(f76924,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF479)
| m1_subset_1(X0,sK31) )
| ~ spl485_118 ),
inference(resolution,[],[f73636,f76803]) ).
fof(f76925,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF480)
| m1_subset_1(X0,sK31) )
| ~ spl485_117 ),
inference(resolution,[],[f73636,f76795]) ).
fof(f76949,plain,
( sF481 = k3_xboole_0(sF480,sF479)
| ~ m1_subset_1(sF479,k1_zfmisc_1(sK31))
| ~ m1_subset_1(sF480,k1_zfmisc_1(sK31))
| ~ spl485_110 ),
inference(superposition,[],[f76756,f76837]) ).
fof(f76961,plain,
( sF481 = k3_xboole_0(sF480,sF479)
| ~ m1_subset_1(sF480,k1_zfmisc_1(sK31))
| ~ spl485_110
| ~ spl485_118 ),
inference(forward_subsumption_resolution,[],[f76949,f76803]) ).
fof(f76963,plain,
( sF481 = k3_xboole_0(sF480,sF479)
| ~ spl485_110
| ~ spl485_117
| ~ spl485_118 ),
inference(forward_subsumption_resolution,[],[f76961,f76795]) ).
fof(f76966,definition,
( spl485_126
<=> sF481 = k3_xboole_0(sF480,sF479) ),
introduced(definition,[new_symbols(definition,[spl485_126])],[avatar_definition]) ).
fof(f76968,plain,
( sF481 = k3_xboole_0(sF480,sF479)
| ~ spl485_126 ),
inference(avatar_component_clause,[],[f76966]) ).
fof(f76969,plain,
( spl485_126
| ~ spl485_110
| ~ spl485_117
| ~ spl485_118 ),
inference(avatar_split_clause,[],[f76963,f76801,f76793,f76754,f76966]) ).
fof(f77008,plain,
( ! [X2,X3,X0,X1] :
( r2_hidden(X0,k8_relset_2(X1,X2,X3,sK34))
| ~ m1_subset_1(sK34,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(sK42(X3,X0,sK34),sK32)
| ~ r2_hidden(X0,sF479) )
| ~ spl485_101
| ~ spl485_103
| ~ spl485_108
| ~ spl485_111
| ~ spl485_112
| ~ spl485_113 ),
inference(resolution,[],[f73606,f76902]) ).
fof(f77009,plain,
( ! [X2,X3,X0,X1] :
( r2_hidden(X0,k8_relset_2(X1,X2,X3,sK34))
| ~ m1_subset_1(sK34,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(sK42(X3,X0,sK34),sK33)
| ~ r2_hidden(X0,sF480) )
| ~ spl485_102
| ~ spl485_103
| ~ spl485_109
| ~ spl485_111
| ~ spl485_112
| ~ spl485_113 ),
inference(resolution,[],[f73606,f76903]) ).
fof(f77017,plain,
( ! [X0] :
( r2_hidden(X0,sF478)
| ~ m1_subset_1(sK34,k1_zfmisc_1(k2_zfmisc_1(sK30,sK31)))
| ~ m1_subset_1(X0,sK31)
| ~ m1_subset_1(sF477,k1_zfmisc_1(sK30))
| v1_xboole_0(sK31)
| ~ r2_hidden(sK42(sF477,X0,sK34),sK33)
| ~ r2_hidden(X0,sF480) )
| ~ spl485_102
| ~ spl485_103
| ~ spl485_107
| ~ spl485_109
| ~ spl485_111
| ~ spl485_112
| ~ spl485_113 ),
inference(superposition,[],[f77009,f76741]) ).
fof(f77022,plain,
( ! [X0] :
( ~ m1_subset_1(sK34,k1_zfmisc_1(sF482))
| r2_hidden(X0,sF478)
| ~ m1_subset_1(X0,sK31)
| ~ m1_subset_1(sF477,k1_zfmisc_1(sK30))
| v1_xboole_0(sK31)
| ~ r2_hidden(sK42(sF477,X0,sK34),sK33)
| ~ r2_hidden(X0,sF480) )
| ~ spl485_102
| ~ spl485_103
| ~ spl485_107
| ~ spl485_109
| ~ spl485_111
| ~ spl485_112
| ~ spl485_113 ),
inference(forward_demodulation,[],[f77017,f76761]) ).
fof(f77024,plain,
( ! [X0] :
( ~ m1_subset_1(sK34,sF483)
| r2_hidden(X0,sF478)
| ~ m1_subset_1(X0,sK31)
| ~ m1_subset_1(sF477,k1_zfmisc_1(sK30))
| v1_xboole_0(sK31)
| ~ r2_hidden(sK42(sF477,X0,sK34),sK33)
| ~ r2_hidden(X0,sF480) )
| ~ spl485_102
| ~ spl485_103
| ~ spl485_107
| ~ spl485_109
| ~ spl485_111
| ~ spl485_112
| ~ spl485_113 ),
inference(forward_demodulation,[],[f77022,f76766]) ).
fof(f77026,plain,
( ! [X0] :
( r2_hidden(X0,sF478)
| ~ m1_subset_1(X0,sK31)
| ~ m1_subset_1(sF477,k1_zfmisc_1(sK30))
| v1_xboole_0(sK31)
| ~ r2_hidden(sK42(sF477,X0,sK34),sK33)
| ~ r2_hidden(X0,sF480) )
| ~ spl485_102
| ~ spl485_103
| ~ spl485_107
| ~ spl485_109
| ~ spl485_111
| ~ spl485_112
| ~ spl485_113 ),
inference(forward_subsumption_resolution,[],[f77024,f76721]) ).
fof(f77028,plain,
( ! [X0] :
( ~ m1_subset_1(sF477,sF484)
| r2_hidden(X0,sF478)
| ~ m1_subset_1(X0,sK31)
| v1_xboole_0(sK31)
| ~ r2_hidden(sK42(sF477,X0,sK34),sK33)
| ~ r2_hidden(X0,sF480) )
| ~ spl485_102
| ~ spl485_103
| ~ spl485_107
| ~ spl485_109
| ~ spl485_111
| ~ spl485_112
| ~ spl485_113 ),
inference(forward_demodulation,[],[f77026,f76771]) ).
fof(f77030,plain,
( ! [X0] :
( r2_hidden(X0,sF478)
| ~ m1_subset_1(X0,sK31)
| v1_xboole_0(sK31)
| ~ r2_hidden(sK42(sF477,X0,sK34),sK33)
| ~ r2_hidden(X0,sF480) )
| ~ spl485_102
| ~ spl485_103
| ~ spl485_107
| ~ spl485_109
| ~ spl485_111
| ~ spl485_112
| ~ spl485_113
| ~ spl485_121 ),
inference(forward_subsumption_resolution,[],[f77028,f76853]) ).
fof(f77032,definition,
( spl485_127
<=> v1_xboole_0(sK31) ),
introduced(definition,[new_symbols(definition,[spl485_127])],[avatar_definition]) ).
fof(f77033,plain,
( ~ v1_xboole_0(sK31)
| spl485_127 ),
inference(avatar_component_clause,[],[f77032]) ).
fof(f77034,plain,
( v1_xboole_0(sK31)
| ~ spl485_127 ),
inference(avatar_component_clause,[],[f77032]) ).
fof(f77040,definition,
( spl485_129
<=> ! [X0] :
( r2_hidden(X0,sF478)
| ~ r2_hidden(X0,sF480)
| ~ r2_hidden(sK42(sF477,X0,sK34),sK33)
| ~ m1_subset_1(X0,sK31) ) ),
introduced(definition,[new_symbols(definition,[spl485_129])],[avatar_definition]) ).
fof(f77041,plain,
( ! [X0] :
( r2_hidden(X0,sF478)
| ~ r2_hidden(X0,sF480)
| ~ r2_hidden(sK42(sF477,X0,sK34),sK33)
| ~ m1_subset_1(X0,sK31) )
| ~ spl485_129 ),
inference(avatar_component_clause,[],[f77040]) ).
fof(f77042,plain,
( spl485_127
| spl485_129
| ~ spl485_102
| ~ spl485_103
| ~ spl485_107
| ~ spl485_109
| ~ spl485_111
| ~ spl485_112
| ~ spl485_113
| ~ spl485_121 ),
inference(avatar_split_clause,[],[f77030,f76851,f76769,f76764,f76759,f76749,f76739,f76719,f76714,f77040,f77032]) ).
fof(f77043,plain,
( ! [X2,X3,X0,X1] :
( ~ r2_hidden(sK42(X3,sK63(X2,k8_relset_2(X0,X1,X3,sK34)),sK34),sK32)
| ~ m1_subset_1(sK63(X2,k8_relset_2(X0,X1,X3,sK34)),X1)
| ~ m1_subset_1(X3,k1_zfmisc_1(X0))
| v1_xboole_0(X1)
| ~ m1_subset_1(sK34,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| ~ r2_hidden(sK63(X2,k8_relset_2(X0,X1,X3,sK34)),sF479)
| r1_tarski(X2,k8_relset_2(X0,X1,X3,sK34)) )
| ~ spl485_101
| ~ spl485_103
| ~ spl485_108
| ~ spl485_111
| ~ spl485_112
| ~ spl485_113 ),
inference(resolution,[],[f77008,f73700]) ).
fof(f77069,plain,
( ! [X0] :
( r2_hidden(X0,sF478)
| r2_hidden(sK42(sF477,X0,sK34),sF477)
| ~ m1_subset_1(sK34,k1_zfmisc_1(k2_zfmisc_1(sK30,sK31)))
| ~ m1_subset_1(X0,sK31)
| ~ m1_subset_1(sF477,k1_zfmisc_1(sK30))
| v1_xboole_0(sK31) )
| ~ spl485_107 ),
inference(superposition,[],[f73605,f76741]) ).
fof(f77070,plain,
( ! [X0] :
( r2_hidden(X0,sF480)
| r2_hidden(sK42(sK33,X0,sK34),sK33)
| ~ m1_subset_1(sK34,k1_zfmisc_1(k2_zfmisc_1(sK30,sK31)))
| ~ m1_subset_1(X0,sK31)
| ~ m1_subset_1(sK33,k1_zfmisc_1(sK30))
| v1_xboole_0(sK31) )
| ~ spl485_109 ),
inference(superposition,[],[f73605,f76751]) ).
fof(f77071,plain,
( ! [X0] :
( r2_hidden(X0,sF479)
| r2_hidden(sK42(sK32,X0,sK34),sK32)
| ~ m1_subset_1(sK34,k1_zfmisc_1(k2_zfmisc_1(sK30,sK31)))
| ~ m1_subset_1(X0,sK31)
| ~ m1_subset_1(sK32,k1_zfmisc_1(sK30))
| v1_xboole_0(sK31) )
| ~ spl485_108 ),
inference(superposition,[],[f73605,f76746]) ).
fof(f77077,plain,
( sF477 = k2_xboole_0(sK33,sK32)
| ~ m1_subset_1(sK32,k1_zfmisc_1(sK30))
| ~ m1_subset_1(sK33,k1_zfmisc_1(sK30))
| ~ spl485_106 ),
inference(superposition,[],[f76736,f76885]) ).
fof(f77089,plain,
( ~ m1_subset_1(sK32,sF484)
| sF477 = k2_xboole_0(sK33,sK32)
| ~ m1_subset_1(sK33,k1_zfmisc_1(sK30))
| ~ spl485_106
| ~ spl485_113 ),
inference(forward_demodulation,[],[f77077,f76771]) ).
fof(f77091,plain,
( sF477 = k2_xboole_0(sK33,sK32)
| ~ m1_subset_1(sK33,k1_zfmisc_1(sK30))
| ~ spl485_101
| ~ spl485_106
| ~ spl485_113 ),
inference(forward_subsumption_resolution,[],[f77089,f76711]) ).
fof(f77093,plain,
( ~ m1_subset_1(sK33,sF484)
| sF477 = k2_xboole_0(sK33,sK32)
| ~ spl485_101
| ~ spl485_106
| ~ spl485_113 ),
inference(forward_demodulation,[],[f77091,f76771]) ).
fof(f77095,plain,
( sF477 = k2_xboole_0(sK33,sK32)
| ~ spl485_101
| ~ spl485_102
| ~ spl485_106
| ~ spl485_113 ),
inference(forward_subsumption_resolution,[],[f77093,f76716]) ).
fof(f77098,definition,
( spl485_130
<=> sF477 = k2_xboole_0(sK33,sK32) ),
introduced(definition,[new_symbols(definition,[spl485_130])],[avatar_definition]) ).
fof(f77100,plain,
( sF477 = k2_xboole_0(sK33,sK32)
| ~ spl485_130 ),
inference(avatar_component_clause,[],[f77098]) ).
fof(f77101,plain,
( spl485_130
| ~ spl485_101
| ~ spl485_102
| ~ spl485_106
| ~ spl485_113 ),
inference(avatar_split_clause,[],[f77095,f76769,f76734,f76714,f76709,f77098]) ).
fof(f77171,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF480)
| ~ r2_hidden(X0,sF479)
| r2_hidden(X0,sF481) )
| ~ spl485_119 ),
inference(superposition,[],[f76049,f76810]) ).
fof(f77267,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF481)
| r2_hidden(X0,sF480) )
| ~ spl485_119 ),
inference(superposition,[],[f76051,f76810]) ).
fof(f77268,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF481)
| r2_hidden(X0,sF479) )
| ~ spl485_126 ),
inference(superposition,[],[f76051,f76968]) ).
fof(f77271,plain,
( ! [X0] :
( r2_hidden(sK63(sF481,X0),sF480)
| r1_tarski(sF481,X0) )
| ~ spl485_119 ),
inference(resolution,[],[f77267,f73699]) ).
fof(f77284,plain,
( ! [X0] :
( r2_hidden(sK63(sF481,X0),sF479)
| r1_tarski(sF481,X0) )
| ~ spl485_126 ),
inference(resolution,[],[f77268,f73699]) ).
fof(f77765,plain,
( ! [X0] :
( m1_subset_1(sK63(sF478,X0),sK31)
| r1_tarski(sF478,X0) )
| ~ spl485_116 ),
inference(resolution,[],[f76923,f73699]) ).
fof(f77896,definition,
( spl485_193
<=> ! [X1] : ~ r2_hidden(X1,sF478) ),
introduced(definition,[new_symbols(definition,[spl485_193])],[avatar_definition]) ).
fof(f77897,plain,
( ! [X1] : ~ r2_hidden(X1,sF478)
| ~ spl485_193 ),
inference(avatar_component_clause,[],[f77896]) ).
fof(f77955,plain,
( ! [X0] :
( ~ r2_hidden(sK42(sF477,sK63(X0,sF478),sK34),sK32)
| ~ m1_subset_1(sK63(X0,sF478),sK31)
| ~ m1_subset_1(sF477,k1_zfmisc_1(sK30))
| v1_xboole_0(sK31)
| ~ m1_subset_1(sK34,k1_zfmisc_1(k2_zfmisc_1(sK30,sK31)))
| ~ r2_hidden(sK63(X0,sF478),sF479)
| r1_tarski(X0,sF478) )
| ~ spl485_101
| ~ spl485_103
| ~ spl485_107
| ~ spl485_108
| ~ spl485_111
| ~ spl485_112
| ~ spl485_113 ),
inference(superposition,[],[f77043,f76741]) ).
fof(f78087,plain,
( ! [X0] :
( ~ r2_hidden(X0,sK33)
| r2_hidden(X0,sF477) )
| ~ spl485_120 ),
inference(superposition,[],[f75990,f76829]) ).
fof(f78088,plain,
( ! [X0] :
( ~ r2_hidden(X0,sK32)
| r2_hidden(X0,sF477) )
| ~ spl485_130 ),
inference(superposition,[],[f75990,f77100]) ).
fof(f78275,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF478)
| ~ v1_xboole_0(sK31) )
| ~ spl485_116 ),
inference(resolution,[],[f73635,f76785]) ).
fof(f78278,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF481)
| ~ v1_xboole_0(sK31) )
| ~ spl485_122 ),
inference(resolution,[],[f73635,f76873]) ).
fof(f78293,plain,
( ! [X0] : ~ r2_hidden(X0,sF481)
| ~ spl485_122
| ~ spl485_127 ),
inference(forward_subsumption_resolution,[],[f78278,f77034]) ).
fof(f78328,plain,
( ! [X0] :
( ~ r2_hidden(sK42(sF477,X0,sK34),sK33)
| ~ r2_hidden(X0,sF480)
| r2_hidden(X0,sF478) )
| ~ spl485_117
| ~ spl485_129 ),
inference(forward_subsumption_resolution,[],[f77041,f76925]) ).
fof(f78333,plain,
( ! [X0] :
( ~ m1_subset_1(sK34,k1_zfmisc_1(sF482))
| r2_hidden(X0,sF479)
| r2_hidden(sK42(sK32,X0,sK34),sK32)
| ~ m1_subset_1(X0,sK31)
| ~ m1_subset_1(sK32,k1_zfmisc_1(sK30))
| v1_xboole_0(sK31) )
| ~ spl485_108
| ~ spl485_111 ),
inference(forward_demodulation,[],[f77071,f76761]) ).
fof(f78334,plain,
( ! [X0] :
( ~ m1_subset_1(sK34,k1_zfmisc_1(sF482))
| r2_hidden(X0,sF480)
| r2_hidden(sK42(sK33,X0,sK34),sK33)
| ~ m1_subset_1(X0,sK31)
| ~ m1_subset_1(sK33,k1_zfmisc_1(sK30))
| v1_xboole_0(sK31) )
| ~ spl485_109
| ~ spl485_111 ),
inference(forward_demodulation,[],[f77070,f76761]) ).
fof(f78335,plain,
( ! [X0] :
( ~ m1_subset_1(sK34,k1_zfmisc_1(sF482))
| r2_hidden(X0,sF478)
| r2_hidden(sK42(sF477,X0,sK34),sF477)
| ~ m1_subset_1(X0,sK31)
| ~ m1_subset_1(sF477,k1_zfmisc_1(sK30))
| v1_xboole_0(sK31) )
| ~ spl485_107
| ~ spl485_111 ),
inference(forward_demodulation,[],[f77069,f76761]) ).
fof(f78350,plain,
( ! [X0] :
( ~ r2_hidden(sK42(sF477,sK63(X0,sF478),sK34),sK32)
| ~ m1_subset_1(sF477,k1_zfmisc_1(sK30))
| v1_xboole_0(sK31)
| ~ m1_subset_1(sK34,k1_zfmisc_1(k2_zfmisc_1(sK30,sK31)))
| ~ r2_hidden(sK63(X0,sF478),sF479)
| r1_tarski(X0,sF478) )
| ~ spl485_101
| ~ spl485_103
| ~ spl485_107
| ~ spl485_108
| ~ spl485_111
| ~ spl485_112
| ~ spl485_113
| ~ spl485_118 ),
inference(forward_subsumption_resolution,[],[f77955,f76924]) ).
fof(f78356,definition,
( spl485_237
<=> ! [X0] : ~ r2_hidden(X0,sF481) ),
introduced(definition,[new_symbols(definition,[spl485_237])],[avatar_definition]) ).
fof(f78357,plain,
( ! [X0] : ~ r2_hidden(X0,sF481)
| ~ spl485_237 ),
inference(avatar_component_clause,[],[f78356]) ).
fof(f78361,plain,
( ~ spl485_127
| spl485_193
| ~ spl485_116 ),
inference(avatar_split_clause,[],[f78275,f76783,f77896,f77032]) ).
fof(f78366,plain,
( ! [X0] :
( ~ m1_subset_1(sK34,sF483)
| r2_hidden(X0,sF479)
| r2_hidden(sK42(sK32,X0,sK34),sK32)
| ~ m1_subset_1(X0,sK31)
| ~ m1_subset_1(sK32,k1_zfmisc_1(sK30))
| v1_xboole_0(sK31) )
| ~ spl485_108
| ~ spl485_111
| ~ spl485_112 ),
inference(forward_demodulation,[],[f78333,f76766]) ).
fof(f78367,plain,
( ! [X0] :
( ~ m1_subset_1(sK34,sF483)
| r2_hidden(X0,sF480)
| r2_hidden(sK42(sK33,X0,sK34),sK33)
| ~ m1_subset_1(X0,sK31)
| ~ m1_subset_1(sK33,k1_zfmisc_1(sK30))
| v1_xboole_0(sK31) )
| ~ spl485_109
| ~ spl485_111
| ~ spl485_112 ),
inference(forward_demodulation,[],[f78334,f76766]) ).
fof(f78368,plain,
( ! [X0] :
( ~ m1_subset_1(sK34,sF483)
| r2_hidden(X0,sF478)
| r2_hidden(sK42(sF477,X0,sK34),sF477)
| ~ m1_subset_1(X0,sK31)
| ~ m1_subset_1(sF477,k1_zfmisc_1(sK30))
| v1_xboole_0(sK31) )
| ~ spl485_107
| ~ spl485_111
| ~ spl485_112 ),
inference(forward_demodulation,[],[f78335,f76766]) ).
fof(f78371,plain,
( ! [X0] :
( ~ m1_subset_1(sF477,sF484)
| ~ r2_hidden(sK42(sF477,sK63(X0,sF478),sK34),sK32)
| v1_xboole_0(sK31)
| ~ m1_subset_1(sK34,k1_zfmisc_1(k2_zfmisc_1(sK30,sK31)))
| ~ r2_hidden(sK63(X0,sF478),sF479)
| r1_tarski(X0,sF478) )
| ~ spl485_101
| ~ spl485_103
| ~ spl485_107
| ~ spl485_108
| ~ spl485_111
| ~ spl485_112
| ~ spl485_113
| ~ spl485_118 ),
inference(forward_demodulation,[],[f78350,f76771]) ).
fof(f78380,plain,
( ! [X0] :
( r2_hidden(X0,sF479)
| r2_hidden(sK42(sK32,X0,sK34),sK32)
| ~ m1_subset_1(X0,sK31)
| ~ m1_subset_1(sK32,k1_zfmisc_1(sK30))
| v1_xboole_0(sK31) )
| ~ spl485_103
| ~ spl485_108
| ~ spl485_111
| ~ spl485_112 ),
inference(forward_subsumption_resolution,[],[f78366,f76721]) ).
fof(f78381,plain,
( ! [X0] :
( r2_hidden(X0,sF480)
| r2_hidden(sK42(sK33,X0,sK34),sK33)
| ~ m1_subset_1(X0,sK31)
| ~ m1_subset_1(sK33,k1_zfmisc_1(sK30))
| v1_xboole_0(sK31) )
| ~ spl485_103
| ~ spl485_109
| ~ spl485_111
| ~ spl485_112 ),
inference(forward_subsumption_resolution,[],[f78367,f76721]) ).
fof(f78382,plain,
( ! [X0] :
( r2_hidden(X0,sF478)
| r2_hidden(sK42(sF477,X0,sK34),sF477)
| ~ m1_subset_1(X0,sK31)
| ~ m1_subset_1(sF477,k1_zfmisc_1(sK30))
| v1_xboole_0(sK31) )
| ~ spl485_103
| ~ spl485_107
| ~ spl485_111
| ~ spl485_112 ),
inference(forward_subsumption_resolution,[],[f78368,f76721]) ).
fof(f78397,plain,
( ! [X0] :
( ~ r2_hidden(sK42(sF477,sK63(X0,sF478),sK34),sK32)
| v1_xboole_0(sK31)
| ~ m1_subset_1(sK34,k1_zfmisc_1(k2_zfmisc_1(sK30,sK31)))
| ~ r2_hidden(sK63(X0,sF478),sF479)
| r1_tarski(X0,sF478) )
| ~ spl485_101
| ~ spl485_103
| ~ spl485_107
| ~ spl485_108
| ~ spl485_111
| ~ spl485_112
| ~ spl485_113
| ~ spl485_118
| ~ spl485_121 ),
inference(forward_subsumption_resolution,[],[f78371,f76853]) ).
fof(f78406,plain,
( ! [X0] :
( ~ m1_subset_1(sK32,sF484)
| r2_hidden(X0,sF479)
| r2_hidden(sK42(sK32,X0,sK34),sK32)
| ~ m1_subset_1(X0,sK31)
| v1_xboole_0(sK31) )
| ~ spl485_103
| ~ spl485_108
| ~ spl485_111
| ~ spl485_112
| ~ spl485_113 ),
inference(forward_demodulation,[],[f78380,f76771]) ).
fof(f78407,plain,
( ! [X0] :
( ~ m1_subset_1(sK33,sF484)
| r2_hidden(X0,sF480)
| r2_hidden(sK42(sK33,X0,sK34),sK33)
| ~ m1_subset_1(X0,sK31)
| v1_xboole_0(sK31) )
| ~ spl485_103
| ~ spl485_109
| ~ spl485_111
| ~ spl485_112
| ~ spl485_113 ),
inference(forward_demodulation,[],[f78381,f76771]) ).
fof(f78408,plain,
( ! [X0] :
( ~ m1_subset_1(sF477,sF484)
| r2_hidden(X0,sF478)
| r2_hidden(sK42(sF477,X0,sK34),sF477)
| ~ m1_subset_1(X0,sK31)
| v1_xboole_0(sK31) )
| ~ spl485_103
| ~ spl485_107
| ~ spl485_111
| ~ spl485_112
| ~ spl485_113 ),
inference(forward_demodulation,[],[f78382,f76771]) ).
fof(f78410,plain,
( ! [X0] :
( ~ m1_subset_1(sK34,k1_zfmisc_1(sF482))
| ~ r2_hidden(sK42(sF477,sK63(X0,sF478),sK34),sK32)
| v1_xboole_0(sK31)
| ~ r2_hidden(sK63(X0,sF478),sF479)
| r1_tarski(X0,sF478) )
| ~ spl485_101
| ~ spl485_103
| ~ spl485_107
| ~ spl485_108
| ~ spl485_111
| ~ spl485_112
| ~ spl485_113
| ~ spl485_118
| ~ spl485_121 ),
inference(forward_demodulation,[],[f78397,f76761]) ).
fof(f78419,plain,
( ! [X0] :
( r2_hidden(X0,sF479)
| r2_hidden(sK42(sK32,X0,sK34),sK32)
| ~ m1_subset_1(X0,sK31)
| v1_xboole_0(sK31) )
| ~ spl485_101
| ~ spl485_103
| ~ spl485_108
| ~ spl485_111
| ~ spl485_112
| ~ spl485_113 ),
inference(forward_subsumption_resolution,[],[f78406,f76711]) ).
fof(f78420,plain,
( ! [X0] :
( r2_hidden(X0,sF480)
| r2_hidden(sK42(sK33,X0,sK34),sK33)
| ~ m1_subset_1(X0,sK31)
| v1_xboole_0(sK31) )
| ~ spl485_102
| ~ spl485_103
| ~ spl485_109
| ~ spl485_111
| ~ spl485_112
| ~ spl485_113 ),
inference(forward_subsumption_resolution,[],[f78407,f76716]) ).
fof(f78421,plain,
( ! [X0] :
( r2_hidden(X0,sF478)
| r2_hidden(sK42(sF477,X0,sK34),sF477)
| ~ m1_subset_1(X0,sK31)
| v1_xboole_0(sK31) )
| ~ spl485_103
| ~ spl485_107
| ~ spl485_111
| ~ spl485_112
| ~ spl485_113
| ~ spl485_121 ),
inference(forward_subsumption_resolution,[],[f78408,f76853]) ).
fof(f78423,plain,
( ! [X0] :
( ~ m1_subset_1(sK34,sF483)
| ~ r2_hidden(sK42(sF477,sK63(X0,sF478),sK34),sK32)
| v1_xboole_0(sK31)
| ~ r2_hidden(sK63(X0,sF478),sF479)
| r1_tarski(X0,sF478) )
| ~ spl485_101
| ~ spl485_103
| ~ spl485_107
| ~ spl485_108
| ~ spl485_111
| ~ spl485_112
| ~ spl485_113
| ~ spl485_118
| ~ spl485_121 ),
inference(forward_demodulation,[],[f78410,f76766]) ).
fof(f78433,definition,
( spl485_241
<=> ! [X0] :
( r2_hidden(X0,sF479)
| ~ m1_subset_1(X0,sK31)
| r2_hidden(sK42(sK32,X0,sK34),sK32) ) ),
introduced(definition,[new_symbols(definition,[spl485_241])],[avatar_definition]) ).
fof(f78434,plain,
( ! [X0] :
( r2_hidden(sK42(sK32,X0,sK34),sK32)
| ~ m1_subset_1(X0,sK31)
| r2_hidden(X0,sF479) )
| ~ spl485_241 ),
inference(avatar_component_clause,[],[f78433]) ).
fof(f78435,plain,
( spl485_127
| spl485_241
| ~ spl485_101
| ~ spl485_103
| ~ spl485_108
| ~ spl485_111
| ~ spl485_112
| ~ spl485_113 ),
inference(avatar_split_clause,[],[f78419,f76769,f76764,f76759,f76744,f76719,f76709,f78433,f77032]) ).
fof(f78437,definition,
( spl485_242
<=> ! [X0] :
( r2_hidden(X0,sF480)
| ~ m1_subset_1(X0,sK31)
| r2_hidden(sK42(sK33,X0,sK34),sK33) ) ),
introduced(definition,[new_symbols(definition,[spl485_242])],[avatar_definition]) ).
fof(f78438,plain,
( ! [X0] :
( r2_hidden(sK42(sK33,X0,sK34),sK33)
| ~ m1_subset_1(X0,sK31)
| r2_hidden(X0,sF480) )
| ~ spl485_242 ),
inference(avatar_component_clause,[],[f78437]) ).
fof(f78439,plain,
( spl485_127
| spl485_242
| ~ spl485_102
| ~ spl485_103
| ~ spl485_109
| ~ spl485_111
| ~ spl485_112
| ~ spl485_113 ),
inference(avatar_split_clause,[],[f78420,f76769,f76764,f76759,f76749,f76719,f76714,f78437,f77032]) ).
fof(f78441,definition,
( spl485_243
<=> ! [X0] :
( r2_hidden(X0,sF478)
| ~ m1_subset_1(X0,sK31)
| r2_hidden(sK42(sF477,X0,sK34),sF477) ) ),
introduced(definition,[new_symbols(definition,[spl485_243])],[avatar_definition]) ).
fof(f78442,plain,
( ! [X0] :
( r2_hidden(sK42(sF477,X0,sK34),sF477)
| ~ m1_subset_1(X0,sK31)
| r2_hidden(X0,sF478) )
| ~ spl485_243 ),
inference(avatar_component_clause,[],[f78441]) ).
fof(f78443,plain,
( spl485_127
| spl485_243
| ~ spl485_103
| ~ spl485_107
| ~ spl485_111
| ~ spl485_112
| ~ spl485_113
| ~ spl485_121 ),
inference(avatar_split_clause,[],[f78421,f76851,f76769,f76764,f76759,f76739,f76719,f78441,f77032]) ).
fof(f78445,plain,
( ! [X0] :
( ~ r2_hidden(sK42(sF477,sK63(X0,sF478),sK34),sK32)
| v1_xboole_0(sK31)
| ~ r2_hidden(sK63(X0,sF478),sF479)
| r1_tarski(X0,sF478) )
| ~ spl485_101
| ~ spl485_103
| ~ spl485_107
| ~ spl485_108
| ~ spl485_111
| ~ spl485_112
| ~ spl485_113
| ~ spl485_118
| ~ spl485_121 ),
inference(forward_subsumption_resolution,[],[f78423,f76721]) ).
fof(f78471,definition,
( spl485_249
<=> ! [X0] :
( ~ r2_hidden(sK42(sF477,sK63(X0,sF478),sK34),sK32)
| r1_tarski(X0,sF478)
| ~ r2_hidden(sK63(X0,sF478),sF479) ) ),
introduced(definition,[new_symbols(definition,[spl485_249])],[avatar_definition]) ).
fof(f78472,plain,
( ! [X0] :
( ~ r2_hidden(sK42(sF477,sK63(X0,sF478),sK34),sK32)
| r1_tarski(X0,sF478)
| ~ r2_hidden(sK63(X0,sF478),sF479) )
| ~ spl485_249 ),
inference(avatar_component_clause,[],[f78471]) ).
fof(f78473,plain,
( spl485_127
| spl485_249
| ~ spl485_101
| ~ spl485_103
| ~ spl485_107
| ~ spl485_108
| ~ spl485_111
| ~ spl485_112
| ~ spl485_113
| ~ spl485_118
| ~ spl485_121 ),
inference(avatar_split_clause,[],[f78445,f76851,f76801,f76769,f76764,f76759,f76744,f76739,f76719,f76709,f78471,f77032]) ).
fof(f78490,plain,
( spl485_237
| ~ spl485_122
| ~ spl485_127 ),
inference(avatar_split_clause,[],[f78293,f77032,f76871,f78356]) ).
fof(f78609,plain,
( ! [X0,X1] :
( r2_hidden(sK63(sF478,X0),k9_relat_1(sK34,k1_tarski(X1)))
| ~ r2_hidden(X1,sF477)
| r1_tarski(sF478,X0)
| ~ m1_subset_1(sK34,k1_zfmisc_1(k2_zfmisc_1(sK30,sK31)))
| ~ m1_subset_1(sF477,k1_zfmisc_1(sK30)) )
| ~ spl485_107 ),
inference(superposition,[],[f76909,f76741]) ).
fof(f79232,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF477)
| r2_hidden(X0,sK33)
| r2_hidden(X0,sK32) )
| ~ spl485_120 ),
inference(superposition,[],[f75991,f76829]) ).
fof(f80092,plain,
( ! [X0,X1] :
( ~ m1_subset_1(sK34,k1_zfmisc_1(sF482))
| r2_hidden(sK63(sF478,X0),k9_relat_1(sK34,k1_tarski(X1)))
| ~ r2_hidden(X1,sF477)
| r1_tarski(sF478,X0)
| ~ m1_subset_1(sF477,k1_zfmisc_1(sK30)) )
| ~ spl485_107
| ~ spl485_111 ),
inference(forward_demodulation,[],[f78609,f76761]) ).
fof(f80124,plain,
( ! [X0,X1] :
( ~ m1_subset_1(sK34,sF483)
| r2_hidden(sK63(sF478,X0),k9_relat_1(sK34,k1_tarski(X1)))
| ~ r2_hidden(X1,sF477)
| r1_tarski(sF478,X0)
| ~ m1_subset_1(sF477,k1_zfmisc_1(sK30)) )
| ~ spl485_107
| ~ spl485_111
| ~ spl485_112 ),
inference(forward_demodulation,[],[f80092,f76766]) ).
fof(f80136,plain,
( ! [X0,X1] :
( r2_hidden(sK63(sF478,X0),k9_relat_1(sK34,k1_tarski(X1)))
| ~ r2_hidden(X1,sF477)
| r1_tarski(sF478,X0)
| ~ m1_subset_1(sF477,k1_zfmisc_1(sK30)) )
| ~ spl485_103
| ~ spl485_107
| ~ spl485_111
| ~ spl485_112 ),
inference(forward_subsumption_resolution,[],[f80124,f76721]) ).
fof(f80148,plain,
( ! [X0,X1] :
( ~ m1_subset_1(sF477,sF484)
| r2_hidden(sK63(sF478,X0),k9_relat_1(sK34,k1_tarski(X1)))
| ~ r2_hidden(X1,sF477)
| r1_tarski(sF478,X0) )
| ~ spl485_103
| ~ spl485_107
| ~ spl485_111
| ~ spl485_112
| ~ spl485_113 ),
inference(forward_demodulation,[],[f80136,f76771]) ).
fof(f80160,plain,
( ! [X0,X1] :
( r2_hidden(sK63(sF478,X0),k9_relat_1(sK34,k1_tarski(X1)))
| ~ r2_hidden(X1,sF477)
| r1_tarski(sF478,X0) )
| ~ spl485_103
| ~ spl485_107
| ~ spl485_111
| ~ spl485_112
| ~ spl485_113
| ~ spl485_121 ),
inference(forward_subsumption_resolution,[],[f80148,f76853]) ).
fof(f80211,plain,
( ! [X0] :
( r2_hidden(sK42(sF477,X0,sK34),sK33)
| r2_hidden(X0,sF478)
| ~ m1_subset_1(X0,sK31)
| r2_hidden(sK42(sF477,X0,sK34),sK32) )
| ~ spl485_120
| ~ spl485_243 ),
inference(resolution,[],[f78442,f79232]) ).
fof(f80221,plain,
( ! [X0] :
( r2_hidden(sK42(sK33,X0,sK34),sF477)
| r2_hidden(X0,sF480)
| ~ m1_subset_1(X0,sK31) )
| ~ spl485_120
| ~ spl485_242 ),
inference(resolution,[],[f78438,f78087]) ).
fof(f80231,plain,
( ! [X0] :
( r2_hidden(sK42(sK32,X0,sK34),sF477)
| r2_hidden(X0,sF479)
| ~ m1_subset_1(X0,sK31) )
| ~ spl485_130
| ~ spl485_241 ),
inference(resolution,[],[f78434,f78088]) ).
fof(f80256,plain,
( ! [X2,X3,X0,X1] :
( r2_hidden(sK63(sF478,X1),k8_relset_2(X2,X3,X0,sK34))
| r1_tarski(sF478,X1)
| ~ r2_hidden(sK42(X0,sK63(sF478,X1),sK34),sF477)
| ~ m1_subset_1(sK34,k1_zfmisc_1(k2_zfmisc_1(X2,X3)))
| ~ m1_subset_1(sK63(sF478,X1),X3)
| ~ m1_subset_1(X0,k1_zfmisc_1(X2))
| v1_xboole_0(X3) )
| ~ spl485_103
| ~ spl485_107
| ~ spl485_111
| ~ spl485_112
| ~ spl485_113
| ~ spl485_121 ),
inference(resolution,[],[f80160,f73606]) ).
fof(f80267,plain,
( ! [X0] :
( r2_hidden(sK63(sF478,X0),sF480)
| r1_tarski(sF478,X0)
| ~ r2_hidden(sK42(sK33,sK63(sF478,X0),sK34),sF477)
| ~ m1_subset_1(sK34,k1_zfmisc_1(k2_zfmisc_1(sK30,sK31)))
| ~ m1_subset_1(sK63(sF478,X0),sK31)
| ~ m1_subset_1(sK33,k1_zfmisc_1(sK30))
| v1_xboole_0(sK31) )
| ~ spl485_103
| ~ spl485_107
| ~ spl485_109
| ~ spl485_111
| ~ spl485_112
| ~ spl485_113
| ~ spl485_121 ),
inference(superposition,[],[f80256,f76751]) ).
fof(f80268,plain,
( ! [X0] :
( r2_hidden(sK63(sF478,X0),sF479)
| r1_tarski(sF478,X0)
| ~ r2_hidden(sK42(sK32,sK63(sF478,X0),sK34),sF477)
| ~ m1_subset_1(sK34,k1_zfmisc_1(k2_zfmisc_1(sK30,sK31)))
| ~ m1_subset_1(sK63(sF478,X0),sK31)
| ~ m1_subset_1(sK32,k1_zfmisc_1(sK30))
| v1_xboole_0(sK31) )
| ~ spl485_103
| ~ spl485_107
| ~ spl485_108
| ~ spl485_111
| ~ spl485_112
| ~ spl485_113
| ~ spl485_121 ),
inference(superposition,[],[f80256,f76746]) ).
fof(f80329,plain,
( ! [X0] :
( r2_hidden(X0,sF478)
| ~ m1_subset_1(X0,sK31)
| r2_hidden(sK42(sF477,X0,sK34),sK32)
| ~ r2_hidden(X0,sF480)
| r2_hidden(X0,sF478) )
| ~ spl485_117
| ~ spl485_120
| ~ spl485_129
| ~ spl485_243 ),
inference(resolution,[],[f80211,f78328]) ).
fof(f80337,plain,
( ! [X0] :
( r2_hidden(X0,sF478)
| ~ m1_subset_1(X0,sK31)
| r2_hidden(sK42(sF477,X0,sK34),sK32)
| ~ r2_hidden(X0,sF480) )
| ~ spl485_117
| ~ spl485_120
| ~ spl485_129
| ~ spl485_243 ),
inference(duplicate_literal_removal,[],[f80329]) ).
fof(f80345,plain,
( ! [X0] :
( r2_hidden(sK42(sF477,X0,sK34),sK32)
| r2_hidden(X0,sF478)
| ~ r2_hidden(X0,sF480) )
| ~ spl485_117
| ~ spl485_120
| ~ spl485_129
| ~ spl485_243 ),
inference(forward_subsumption_resolution,[],[f80337,f76925]) ).
fof(f80348,plain,
( ! [X0] :
( r2_hidden(sK63(X0,sF478),sF478)
| ~ r2_hidden(sK63(X0,sF478),sF480)
| r1_tarski(X0,sF478)
| ~ r2_hidden(sK63(X0,sF478),sF479) )
| ~ spl485_117
| ~ spl485_120
| ~ spl485_129
| ~ spl485_243
| ~ spl485_249 ),
inference(resolution,[],[f80345,f78472]) ).
fof(f80360,plain,
( ! [X0] :
( ~ r2_hidden(sK63(X0,sF478),sF480)
| r1_tarski(X0,sF478)
| ~ r2_hidden(sK63(X0,sF478),sF479) )
| ~ spl485_117
| ~ spl485_120
| ~ spl485_129
| ~ spl485_243
| ~ spl485_249 ),
inference(forward_subsumption_resolution,[],[f80348,f73700]) ).
fof(f80401,definition,
( spl485_376
<=> r1_tarski(sF481,sF478) ),
introduced(definition,[new_symbols(definition,[spl485_376])],[avatar_definition]) ).
fof(f80403,plain,
( r1_tarski(sF481,sF478)
| ~ spl485_376 ),
inference(avatar_component_clause,[],[f80401]) ).
fof(f80405,plain,
( r1_tarski(sF481,sF478)
| ~ r2_hidden(sK63(sF481,sF478),sF479)
| r1_tarski(sF481,sF478)
| ~ spl485_117
| ~ spl485_119
| ~ spl485_120
| ~ spl485_129
| ~ spl485_243
| ~ spl485_249 ),
inference(resolution,[],[f80360,f77271]) ).
fof(f80408,plain,
( r1_tarski(sF481,sF478)
| ~ r2_hidden(sK63(sF481,sF478),sF479)
| ~ spl485_117
| ~ spl485_119
| ~ spl485_120
| ~ spl485_129
| ~ spl485_243
| ~ spl485_249 ),
inference(duplicate_literal_removal,[],[f80405]) ).
fof(f80418,plain,
( r1_tarski(sF481,sF478)
| ~ spl485_117
| ~ spl485_119
| ~ spl485_120
| ~ spl485_126
| ~ spl485_129
| ~ spl485_243
| ~ spl485_249 ),
inference(forward_subsumption_resolution,[],[f80408,f77284]) ).
fof(f80419,plain,
( spl485_376
| ~ spl485_117
| ~ spl485_119
| ~ spl485_120
| ~ spl485_126
| ~ spl485_129
| ~ spl485_243
| ~ spl485_249 ),
inference(avatar_split_clause,[],[f80418,f78471,f78441,f77040,f76966,f76827,f76808,f76793,f80401]) ).
fof(f80511,definition,
( spl485_385
<=> ! [X0] :
( sF478 = X0
| r2_hidden(sK55(X0,sF478),X0) ) ),
introduced(definition,[new_symbols(definition,[spl485_385])],[avatar_definition]) ).
fof(f80512,plain,
( ! [X0] :
( r2_hidden(sK55(X0,sF478),X0)
| sF478 = X0 )
| ~ spl485_385 ),
inference(avatar_component_clause,[],[f80511]) ).
fof(f80522,plain,
( ! [X0] :
( sF478 = X0
| r2_hidden(sK55(X0,sF478),X0) )
| ~ spl485_193 ),
inference(resolution,[],[f77897,f73654]) ).
fof(f80534,plain,
( spl485_385
| ~ spl485_193 ),
inference(avatar_split_clause,[],[f80522,f77896,f80511]) ).
fof(f80924,plain,
( sF478 = sF481
| ~ spl485_237
| ~ spl485_385 ),
inference(resolution,[],[f80512,f78357]) ).
fof(f80940,plain,
( $false
| spl485_104
| ~ spl485_237
| ~ spl485_385 ),
inference(forward_subsumption_resolution,[],[f80924,f76726]) ).
fof(f80941,plain,
( spl485_104
| ~ spl485_237
| ~ spl485_385 ),
inference(avatar_contradiction_clause,[],[f80940]) ).
fof(f81108,plain,
( ! [X0] :
( r2_hidden(sK63(sF478,X0),sF479)
| r1_tarski(sF478,X0)
| ~ m1_subset_1(sK34,k1_zfmisc_1(k2_zfmisc_1(sK30,sK31)))
| ~ m1_subset_1(sK63(sF478,X0),sK31)
| ~ m1_subset_1(sK32,k1_zfmisc_1(sK30))
| v1_xboole_0(sK31) )
| ~ spl485_103
| ~ spl485_107
| ~ spl485_108
| ~ spl485_111
| ~ spl485_112
| ~ spl485_113
| ~ spl485_121
| ~ spl485_130
| ~ spl485_241 ),
inference(forward_subsumption_resolution,[],[f80268,f80231]) ).
fof(f81109,plain,
( ! [X0] :
( r2_hidden(sK63(sF478,X0),sF480)
| r1_tarski(sF478,X0)
| ~ m1_subset_1(sK34,k1_zfmisc_1(k2_zfmisc_1(sK30,sK31)))
| ~ m1_subset_1(sK63(sF478,X0),sK31)
| ~ m1_subset_1(sK33,k1_zfmisc_1(sK30))
| v1_xboole_0(sK31) )
| ~ spl485_103
| ~ spl485_107
| ~ spl485_109
| ~ spl485_111
| ~ spl485_112
| ~ spl485_113
| ~ spl485_120
| ~ spl485_121
| ~ spl485_242 ),
inference(forward_subsumption_resolution,[],[f80267,f80221]) ).
fof(f81223,plain,
( ~ r1_tarski(sF478,sF481)
| sF478 = sF481
| ~ spl485_376 ),
inference(resolution,[],[f80403,f73696]) ).
fof(f81232,plain,
( ! [X0] :
( r2_hidden(sK63(sF478,X0),sF479)
| r1_tarski(sF478,X0)
| ~ m1_subset_1(sK34,k1_zfmisc_1(k2_zfmisc_1(sK30,sK31)))
| ~ m1_subset_1(sK63(sF478,X0),sK31)
| ~ m1_subset_1(sK32,k1_zfmisc_1(sK30)) )
| ~ spl485_103
| ~ spl485_107
| ~ spl485_108
| ~ spl485_111
| ~ spl485_112
| ~ spl485_113
| ~ spl485_121
| spl485_127
| ~ spl485_130
| ~ spl485_241 ),
inference(forward_subsumption_resolution,[],[f81108,f77033]) ).
fof(f81233,plain,
( ! [X0] :
( r2_hidden(sK63(sF478,X0),sF480)
| r1_tarski(sF478,X0)
| ~ m1_subset_1(sK34,k1_zfmisc_1(k2_zfmisc_1(sK30,sK31)))
| ~ m1_subset_1(sK63(sF478,X0),sK31)
| ~ m1_subset_1(sK33,k1_zfmisc_1(sK30)) )
| ~ spl485_103
| ~ spl485_107
| ~ spl485_109
| ~ spl485_111
| ~ spl485_112
| ~ spl485_113
| ~ spl485_120
| ~ spl485_121
| spl485_127
| ~ spl485_242 ),
inference(forward_subsumption_resolution,[],[f81109,f77033]) ).
fof(f81234,plain,
( ~ r1_tarski(sF478,sF481)
| spl485_104
| ~ spl485_376 ),
inference(forward_subsumption_resolution,[],[f81223,f76726]) ).
fof(f81242,plain,
( ! [X0] :
( r2_hidden(sK63(sF478,X0),sF479)
| r1_tarski(sF478,X0)
| ~ m1_subset_1(sK34,k1_zfmisc_1(k2_zfmisc_1(sK30,sK31)))
| ~ m1_subset_1(sK32,k1_zfmisc_1(sK30)) )
| ~ spl485_103
| ~ spl485_107
| ~ spl485_108
| ~ spl485_111
| ~ spl485_112
| ~ spl485_113
| ~ spl485_116
| ~ spl485_121
| spl485_127
| ~ spl485_130
| ~ spl485_241 ),
inference(forward_subsumption_resolution,[],[f81232,f77765]) ).
fof(f81243,plain,
( ! [X0] :
( r2_hidden(sK63(sF478,X0),sF480)
| r1_tarski(sF478,X0)
| ~ m1_subset_1(sK34,k1_zfmisc_1(k2_zfmisc_1(sK30,sK31)))
| ~ m1_subset_1(sK33,k1_zfmisc_1(sK30)) )
| ~ spl485_103
| ~ spl485_107
| ~ spl485_109
| ~ spl485_111
| ~ spl485_112
| ~ spl485_113
| ~ spl485_116
| ~ spl485_120
| ~ spl485_121
| spl485_127
| ~ spl485_242 ),
inference(forward_subsumption_resolution,[],[f81233,f77765]) ).
fof(f81245,definition,
( spl485_433
<=> r1_tarski(sF478,sF481) ),
introduced(definition,[new_symbols(definition,[spl485_433])],[avatar_definition]) ).
fof(f81248,plain,
( ~ spl485_433
| spl485_104
| ~ spl485_376 ),
inference(avatar_split_clause,[],[f81234,f80401,f76724,f81245]) ).
fof(f81251,plain,
( ! [X0] :
( ~ m1_subset_1(sK34,k1_zfmisc_1(sF482))
| r2_hidden(sK63(sF478,X0),sF479)
| r1_tarski(sF478,X0)
| ~ m1_subset_1(sK32,k1_zfmisc_1(sK30)) )
| ~ spl485_103
| ~ spl485_107
| ~ spl485_108
| ~ spl485_111
| ~ spl485_112
| ~ spl485_113
| ~ spl485_116
| ~ spl485_121
| spl485_127
| ~ spl485_130
| ~ spl485_241 ),
inference(forward_demodulation,[],[f81242,f76761]) ).
fof(f81252,plain,
( ! [X0] :
( ~ m1_subset_1(sK34,k1_zfmisc_1(sF482))
| r2_hidden(sK63(sF478,X0),sF480)
| r1_tarski(sF478,X0)
| ~ m1_subset_1(sK33,k1_zfmisc_1(sK30)) )
| ~ spl485_103
| ~ spl485_107
| ~ spl485_109
| ~ spl485_111
| ~ spl485_112
| ~ spl485_113
| ~ spl485_116
| ~ spl485_120
| ~ spl485_121
| spl485_127
| ~ spl485_242 ),
inference(forward_demodulation,[],[f81243,f76761]) ).
fof(f81255,plain,
( ! [X0] :
( ~ m1_subset_1(sK34,sF483)
| r2_hidden(sK63(sF478,X0),sF479)
| r1_tarski(sF478,X0)
| ~ m1_subset_1(sK32,k1_zfmisc_1(sK30)) )
| ~ spl485_103
| ~ spl485_107
| ~ spl485_108
| ~ spl485_111
| ~ spl485_112
| ~ spl485_113
| ~ spl485_116
| ~ spl485_121
| spl485_127
| ~ spl485_130
| ~ spl485_241 ),
inference(forward_demodulation,[],[f81251,f76766]) ).
fof(f81256,plain,
( ! [X0] :
( ~ m1_subset_1(sK34,sF483)
| r2_hidden(sK63(sF478,X0),sF480)
| r1_tarski(sF478,X0)
| ~ m1_subset_1(sK33,k1_zfmisc_1(sK30)) )
| ~ spl485_103
| ~ spl485_107
| ~ spl485_109
| ~ spl485_111
| ~ spl485_112
| ~ spl485_113
| ~ spl485_116
| ~ spl485_120
| ~ spl485_121
| spl485_127
| ~ spl485_242 ),
inference(forward_demodulation,[],[f81252,f76766]) ).
fof(f81259,plain,
( ! [X0] :
( r2_hidden(sK63(sF478,X0),sF479)
| r1_tarski(sF478,X0)
| ~ m1_subset_1(sK32,k1_zfmisc_1(sK30)) )
| ~ spl485_103
| ~ spl485_107
| ~ spl485_108
| ~ spl485_111
| ~ spl485_112
| ~ spl485_113
| ~ spl485_116
| ~ spl485_121
| spl485_127
| ~ spl485_130
| ~ spl485_241 ),
inference(forward_subsumption_resolution,[],[f81255,f76721]) ).
fof(f81260,plain,
( ! [X0] :
( r2_hidden(sK63(sF478,X0),sF480)
| r1_tarski(sF478,X0)
| ~ m1_subset_1(sK33,k1_zfmisc_1(sK30)) )
| ~ spl485_103
| ~ spl485_107
| ~ spl485_109
| ~ spl485_111
| ~ spl485_112
| ~ spl485_113
| ~ spl485_116
| ~ spl485_120
| ~ spl485_121
| spl485_127
| ~ spl485_242 ),
inference(forward_subsumption_resolution,[],[f81256,f76721]) ).
fof(f81263,plain,
( ! [X0] :
( ~ m1_subset_1(sK32,sF484)
| r2_hidden(sK63(sF478,X0),sF479)
| r1_tarski(sF478,X0) )
| ~ spl485_103
| ~ spl485_107
| ~ spl485_108
| ~ spl485_111
| ~ spl485_112
| ~ spl485_113
| ~ spl485_116
| ~ spl485_121
| spl485_127
| ~ spl485_130
| ~ spl485_241 ),
inference(forward_demodulation,[],[f81259,f76771]) ).
fof(f81264,plain,
( ! [X0] :
( ~ m1_subset_1(sK33,sF484)
| r2_hidden(sK63(sF478,X0),sF480)
| r1_tarski(sF478,X0) )
| ~ spl485_103
| ~ spl485_107
| ~ spl485_109
| ~ spl485_111
| ~ spl485_112
| ~ spl485_113
| ~ spl485_116
| ~ spl485_120
| ~ spl485_121
| spl485_127
| ~ spl485_242 ),
inference(forward_demodulation,[],[f81260,f76771]) ).
fof(f81267,plain,
( ! [X0] :
( r2_hidden(sK63(sF478,X0),sF479)
| r1_tarski(sF478,X0) )
| ~ spl485_101
| ~ spl485_103
| ~ spl485_107
| ~ spl485_108
| ~ spl485_111
| ~ spl485_112
| ~ spl485_113
| ~ spl485_116
| ~ spl485_121
| spl485_127
| ~ spl485_130
| ~ spl485_241 ),
inference(forward_subsumption_resolution,[],[f81263,f76711]) ).
fof(f81268,plain,
( ! [X0] :
( r2_hidden(sK63(sF478,X0),sF480)
| r1_tarski(sF478,X0) )
| ~ spl485_102
| ~ spl485_103
| ~ spl485_107
| ~ spl485_109
| ~ spl485_111
| ~ spl485_112
| ~ spl485_113
| ~ spl485_116
| ~ spl485_120
| ~ spl485_121
| spl485_127
| ~ spl485_242 ),
inference(forward_subsumption_resolution,[],[f81264,f76716]) ).
fof(f81291,plain,
( ! [X0] :
( r1_tarski(sF478,X0)
| ~ r2_hidden(sK63(sF478,X0),sF479)
| r2_hidden(sK63(sF478,X0),sF481) )
| ~ spl485_102
| ~ spl485_103
| ~ spl485_107
| ~ spl485_109
| ~ spl485_111
| ~ spl485_112
| ~ spl485_113
| ~ spl485_116
| ~ spl485_119
| ~ spl485_120
| ~ spl485_121
| spl485_127
| ~ spl485_242 ),
inference(resolution,[],[f81268,f77171]) ).
fof(f81308,plain,
( ! [X0] :
( r2_hidden(sK63(sF478,X0),sF481)
| r1_tarski(sF478,X0) )
| ~ spl485_101
| ~ spl485_102
| ~ spl485_103
| ~ spl485_107
| ~ spl485_108
| ~ spl485_109
| ~ spl485_111
| ~ spl485_112
| ~ spl485_113
| ~ spl485_116
| ~ spl485_119
| ~ spl485_120
| ~ spl485_121
| spl485_127
| ~ spl485_130
| ~ spl485_241
| ~ spl485_242 ),
inference(forward_subsumption_resolution,[],[f81291,f81267]) ).
fof(f81309,plain,
( r1_tarski(sF478,sF481)
| r1_tarski(sF478,sF481)
| ~ spl485_101
| ~ spl485_102
| ~ spl485_103
| ~ spl485_107
| ~ spl485_108
| ~ spl485_109
| ~ spl485_111
| ~ spl485_112
| ~ spl485_113
| ~ spl485_116
| ~ spl485_119
| ~ spl485_120
| ~ spl485_121
| spl485_127
| ~ spl485_130
| ~ spl485_241
| ~ spl485_242 ),
inference(resolution,[],[f81308,f73700]) ).
fof(f81314,plain,
( r1_tarski(sF478,sF481)
| ~ spl485_101
| ~ spl485_102
| ~ spl485_103
| ~ spl485_107
| ~ spl485_108
| ~ spl485_109
| ~ spl485_111
| ~ spl485_112
| ~ spl485_113
| ~ spl485_116
| ~ spl485_119
| ~ spl485_120
| ~ spl485_121
| spl485_127
| ~ spl485_130
| ~ spl485_241
| ~ spl485_242 ),
inference(duplicate_literal_removal,[],[f81309]) ).
fof(f81316,plain,
( spl485_433
| ~ spl485_101
| ~ spl485_102
| ~ spl485_103
| ~ spl485_107
| ~ spl485_108
| ~ spl485_109
| ~ spl485_111
| ~ spl485_112
| ~ spl485_113
| ~ spl485_116
| ~ spl485_119
| ~ spl485_120
| ~ spl485_121
| spl485_127
| ~ spl485_130
| ~ spl485_241
| ~ spl485_242 ),
inference(avatar_split_clause,[],[f81314,f78437,f78433,f77098,f77032,f76851,f76827,f76808,f76783,f76769,f76764,f76759,f76749,f76744,f76739,f76719,f76714,f76709,f81245]) ).
cnf(s103,plain,
spl485_101,
inference(sat_conversion,[],[f76712]) ).
cnf(s104,plain,
spl485_102,
inference(sat_conversion,[],[f76717]) ).
cnf(s105,plain,
spl485_103,
inference(sat_conversion,[],[f76722]) ).
cnf(s106,plain,
~ spl485_104,
inference(sat_conversion,[],[f76727]) ).
cnf(s108,plain,
spl485_106,
inference(sat_conversion,[],[f76737]) ).
cnf(s109,plain,
spl485_107,
inference(sat_conversion,[],[f76742]) ).
cnf(s110,plain,
spl485_108,
inference(sat_conversion,[],[f76747]) ).
cnf(s111,plain,
spl485_109,
inference(sat_conversion,[],[f76752]) ).
cnf(s112,plain,
spl485_110,
inference(sat_conversion,[],[f76757]) ).
cnf(s113,plain,
spl485_111,
inference(sat_conversion,[],[f76762]) ).
cnf(s114,plain,
spl485_112,
inference(sat_conversion,[],[f76767]) ).
cnf(s115,plain,
spl485_113,
inference(sat_conversion,[],[f76772]) ).
cnf(s116,plain,
( ~ spl485_107
| ~ spl485_114
| ~ spl485_115
| spl485_116 ),
inference(sat_conversion,[],[f76786]) ).
cnf(s117,plain,
( ~ spl485_103
| ~ spl485_111
| ~ spl485_112
| spl485_114 ),
inference(sat_conversion,[],[f76787]) ).
cnf(s118,plain,
( ~ spl485_102
| ~ spl485_109
| ~ spl485_113
| ~ spl485_114
| spl485_117 ),
inference(sat_conversion,[],[f76796]) ).
cnf(s119,plain,
( ~ spl485_101
| ~ spl485_108
| ~ spl485_113
| ~ spl485_114
| spl485_118 ),
inference(sat_conversion,[],[f76804]) ).
cnf(s121,plain,
( ~ spl485_110
| ~ spl485_117
| ~ spl485_118
| spl485_119 ),
inference(sat_conversion,[],[f76812]) ).
cnf(s122,plain,
( ~ spl485_101
| ~ spl485_102
| ~ spl485_106
| ~ spl485_113
| spl485_120 ),
inference(sat_conversion,[],[f76830]) ).
cnf(s124,plain,
( ~ spl485_101
| ~ spl485_102
| ~ spl485_106
| ~ spl485_113
| spl485_121 ),
inference(sat_conversion,[],[f76854]) ).
cnf(s125,plain,
( ~ spl485_113
| spl485_115
| ~ spl485_121 ),
inference(sat_conversion,[],[f76855]) ).
cnf(s127,plain,
( ~ spl485_110
| ~ spl485_117
| ~ spl485_118
| spl485_122 ),
inference(sat_conversion,[],[f76874]) ).
cnf(s130,plain,
( ~ spl485_110
| ~ spl485_117
| ~ spl485_118
| spl485_126 ),
inference(sat_conversion,[],[f76969]) ).
cnf(s133,plain,
( ~ spl485_102
| ~ spl485_103
| ~ spl485_107
| ~ spl485_109
| ~ spl485_111
| ~ spl485_112
| ~ spl485_113
| ~ spl485_121
| spl485_127
| spl485_129 ),
inference(sat_conversion,[],[f77042]) ).
cnf(s134,plain,
( ~ spl485_101
| ~ spl485_102
| ~ spl485_106
| ~ spl485_113
| spl485_130 ),
inference(sat_conversion,[],[f77101]) ).
cnf(s231,plain,
( ~ spl485_116
| ~ spl485_127
| spl485_193 ),
inference(sat_conversion,[],[f78361]) ).
cnf(s233,plain,
( ~ spl485_101
| ~ spl485_103
| ~ spl485_108
| ~ spl485_111
| ~ spl485_112
| ~ spl485_113
| spl485_127
| spl485_241 ),
inference(sat_conversion,[],[f78435]) ).
cnf(s234,plain,
( ~ spl485_102
| ~ spl485_103
| ~ spl485_109
| ~ spl485_111
| ~ spl485_112
| ~ spl485_113
| spl485_127
| spl485_242 ),
inference(sat_conversion,[],[f78439]) ).
cnf(s235,plain,
( ~ spl485_103
| ~ spl485_107
| ~ spl485_111
| ~ spl485_112
| ~ spl485_113
| ~ spl485_121
| spl485_127
| spl485_243 ),
inference(sat_conversion,[],[f78443]) ).
cnf(s241,plain,
( ~ spl485_101
| ~ spl485_103
| ~ spl485_107
| ~ spl485_108
| ~ spl485_111
| ~ spl485_112
| ~ spl485_113
| ~ spl485_118
| ~ spl485_121
| spl485_127
| spl485_249 ),
inference(sat_conversion,[],[f78473]) ).
cnf(s246,plain,
( ~ spl485_122
| ~ spl485_127
| spl485_237 ),
inference(sat_conversion,[],[f78490]) ).
cnf(s455,plain,
( ~ spl485_117
| ~ spl485_119
| ~ spl485_120
| ~ spl485_126
| ~ spl485_129
| ~ spl485_243
| ~ spl485_249
| spl485_376 ),
inference(sat_conversion,[],[f80419]) ).
cnf(s473,plain,
( ~ spl485_193
| spl485_385 ),
inference(sat_conversion,[],[f80534]) ).
cnf(s495,plain,
( spl485_104
| ~ spl485_237
| ~ spl485_385 ),
inference(sat_conversion,[],[f80941]) ).
cnf(s558,plain,
( spl485_104
| ~ spl485_376
| ~ spl485_433 ),
inference(sat_conversion,[],[f81248]) ).
cnf(s566,plain,
( ~ spl485_101
| ~ spl485_102
| ~ spl485_103
| ~ spl485_107
| ~ spl485_108
| ~ spl485_109
| ~ spl485_111
| ~ spl485_112
| ~ spl485_113
| ~ spl485_116
| ~ spl485_119
| ~ spl485_120
| ~ spl485_121
| spl485_127
| ~ spl485_130
| ~ spl485_241
| ~ spl485_242
| spl485_433 ),
inference(sat_conversion,[],[f81316]) ).
cnf(s572,plain,
spl485_114,
inference(rat,[],[s117,s113,s114,s105]) ).
cnf(s574,plain,
spl485_117,
inference(rat,[],[s118,s572,s111,s115,s104]) ).
cnf(s577,plain,
spl485_130,
inference(rat,[],[s134,s104,s115,s108,s103]) ).
cnf(s578,plain,
spl485_121,
inference(rat,[],[s124,s104,s115,s108,s103]) ).
cnf(s579,plain,
spl485_120,
inference(rat,[],[s122,s104,s115,s108,s103]) ).
cnf(s580,plain,
spl485_118,
inference(rat,[],[s119,s572,s110,s115,s103]) ).
cnf(s582,plain,
spl485_115,
inference(rat,[],[s125,s115,s578]) ).
cnf(s585,plain,
spl485_126,
inference(rat,[],[s130,s574,s112,s580]) ).
cnf(s586,plain,
spl485_122,
inference(rat,[],[s127,s574,s112,s580]) ).
cnf(s587,plain,
spl485_119,
inference(rat,[],[s121,s574,s112,s580]) ).
cnf(s588,plain,
spl485_116,
inference(rat,[],[s116,s572,s109,s582]) ).
cnf(s594,plain,
spl485_127,
inference(rat,[],[s558,s455,s566,s241,s133,s233,s234,s235,s106,s574,s579,s585,s587,s105,s109,s110,s111,s113,s114,s115,s104,s103,s578,s577,s588,s580]) ).
cnf(s596,plain,
spl485_237,
inference(rat,[],[s246,s586,s594]) ).
cnf(s597,plain,
spl485_193,
inference(rat,[],[s231,s588,s594]) ).
cnf(s603,plain,
~ spl485_385,
inference(rat,[],[s495,s106,s596]) ).
cnf(s609,plain,
$false,
inference(rat,[],[s473,s603,s597]) ).
fof(f81317,plain,
$false,
inference(avatar_sat_refutation,[],[s609]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU428+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.36 % Computer : n005.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.37 % DateTime : Mon Sep 28 05:22:46 UTC 2026
% 0.08/0.37 % CPUTime :
% 0.08/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.40 Running first-order theorem proving
% 0.08/0.40 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 21.66/8.65 % (468631)Detected formulas, will run a generic FOF schedule.
% 21.66/8.65 % (468638)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=799459010:i=141695:sd=1:nm=32:gsp=on:ss=included_2944 on theBenchmark for (2944ds/141695Mi)
% 21.66/8.65 % (468637)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=170227559:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2944 on theBenchmark for (2944ds/134677Mi)
% 21.66/8.65 % (468636)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=3262953034:i=141193_2944 on theBenchmark for (2944ds/141193Mi)
% 21.66/8.65 % (468640)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3176859827:i=119:av=off:ss=axioms_2944 on theBenchmark for (2944ds/119Mi)
% 21.66/8.65 % (468639)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=702779567:i=109:sd=1:ins=1:gsp=on:ss=axioms_2944 on theBenchmark for (2944ds/109Mi)
% 21.66/8.65 % (468641)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=541981962:s2a=on:i=139:gtg=position_2944 on theBenchmark for (2944ds/139Mi)
% 21.66/8.65 % (468642)dis-21_1_sil=8000:lcm=predicate:random_seed=2347334931:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2944 on theBenchmark for (2944ds/129Mi)
% 21.66/8.65 % (468639)Instruction limit reached!
% 21.66/8.65 % (468639)------------------------------
% 21.66/8.65 % (468639)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.66/8.65 % (468639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.66/8.65 % (468639)CaDiCaL version: 2.1.3
% 21.66/8.65 % (468639)Termination reason: Instruction limit
% 21.66/8.65 % (468639)Termination phase: SInE selection
% 21.66/8.65 % (468639)Time elapsed: 0.080 s
% 21.66/8.65 % (468639)Peak memory usage: 201 MB
% 21.66/8.65 % (468639)Instructions burned: 110 (million)
% 21.66/8.65 % (468641)Instruction limit reached!
% 21.66/8.65 % (468641)------------------------------
% 21.66/8.65 % (468641)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.66/8.65 % (468641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.66/8.65 % (468641)CaDiCaL version: 2.1.3
% 21.66/8.65 % (468641)Termination reason: Instruction limit
% 21.66/8.65 % (468641)Termination phase: Property scanning
% 21.66/8.65 % (468641)Time elapsed: 0.068 s
% 21.66/8.65 % (468641)Peak memory usage: 201 MB
% 21.66/8.65 % (468641)Instructions burned: 141 (million)
% 21.66/8.65 % (468640)Instruction limit reached!
% 21.66/8.65 % (468640)------------------------------
% 21.66/8.65 % (468640)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.66/8.65 % (468640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.66/8.65 % (468640)CaDiCaL version: 2.1.3
% 21.66/8.65 % (468640)Termination reason: Instruction limit
% 21.66/8.65 % (468640)Termination phase: SInE selection
% 21.66/8.65 % (468640)Time elapsed: 0.090 s
% 21.66/8.65 % (468640)Peak memory usage: 201 MB
% 21.66/8.65 % (468640)Instructions burned: 120 (million)
% 21.66/8.65 % (468642)Instruction limit reached!
% 21.66/8.65 % (468642)------------------------------
% 21.66/8.65 % (468642)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.66/8.65 % (468642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.66/8.65 % (468642)CaDiCaL version: 2.1.3
% 21.66/8.65 % (468642)Termination reason: Instruction limit
% 21.66/8.65 % (468642)Termination phase: SInE selection
% 21.66/8.65 % (468642)Time elapsed: 0.101 s
% 21.66/8.65 % (468642)Peak memory usage: 201 MB
% 21.66/8.65 % (468642)Instructions burned: 129 (million)
% 21.66/8.65 % (468651)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3402097667:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2942 on theBenchmark for (2942ds/157Mi)
% 21.66/8.65 % (468652)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3653239828:i=325:sd=1:ss=axioms:sgt=32_2942 on theBenchmark for (2942ds/325Mi)
% 21.66/8.65 % (468650)lrs+10_1_sil=8000:sp=occurrence:random_seed=3594361004:i=285:sd=3:ss=axioms:sgt=8_2942 on theBenchmark for (2942ds/285Mi)
% 21.66/8.65 % (468653)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=1083392207:s2a=on:i=248:s2at=1.23:gtg=position_2941 on theBenchmark for (2941ds/248Mi)
% 21.66/8.65 % (468651)Instruction limit reached!
% 21.66/8.65 % (468651)------------------------------
% 29.59/9.86 % (468651)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.59/9.86 % (468651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.59/9.86 % (468651)CaDiCaL version: 2.1.3
% 29.59/9.86 % (468651)Termination reason: Instruction limit
% 29.59/9.86 % (468651)Termination phase: Property scanning
% 29.59/9.86 % (468651)Time elapsed: 0.076 s
% 29.59/9.86 % (468651)Peak memory usage: 201 MB
% 29.59/9.86 % (468651)Instructions burned: 157 (million)
% 29.59/9.86 % (468653)Instruction limit reached!
% 29.59/9.86 % (468653)------------------------------
% 29.59/9.86 % (468653)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.59/9.86 % (468653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.59/9.86 % (468653)CaDiCaL version: 2.1.3
% 29.59/9.86 % (468653)Termination reason: Instruction limit
% 29.59/9.86 % (468653)Termination phase: Property scanning
% 29.59/9.86 % (468653)Time elapsed: 0.112 s
% 29.59/9.86 % (468653)Peak memory usage: 201 MB
% 29.59/9.86 % (468653)Instructions burned: 248 (million)
% 29.59/9.86 % (468650)Instruction limit reached!
% 29.59/9.86 % (468650)------------------------------
% 29.59/9.86 % (468650)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.59/9.86 % (468650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.59/9.86 % (468650)CaDiCaL version: 2.1.3
% 29.59/9.86 % (468650)Termination reason: Instruction limit
% 29.59/9.86 % (468650)Termination phase: SInE selection
% 29.59/9.86 % (468650)Time elapsed: 0.207 s
% 29.59/9.86 % (468650)Peak memory usage: 201 MB
% 29.59/9.86 % (468650)Instructions burned: 286 (million)
% 29.59/9.86 % (468658)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3937726678:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2940 on theBenchmark for (2940ds/294Mi)
% 29.59/9.86 % (468652)Instruction limit reached!
% 29.59/9.86 % (468652)------------------------------
% 29.59/9.86 % (468652)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.59/9.86 % (468652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.59/9.86 % (468652)CaDiCaL version: 2.1.3
% 29.59/9.86 % (468652)Termination reason: Instruction limit
% 29.59/9.86 % (468652)Termination phase: SInE selection
% 29.59/9.86 % (468652)Time elapsed: 0.234 s
% 29.59/9.86 % (468652)Peak memory usage: 201 MB
% 29.59/9.86 % (468652)Instructions burned: 326 (million)
% 29.59/9.86 % (468659)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=233527673:i=2350_2939 on theBenchmark for (2939ds/2350Mi)
% 29.59/9.86 % (468660)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3159301803:cts=off:i=113:fsr=off:ss=included:sgt=4_2938 on theBenchmark for (2938ds/113Mi)
% 29.59/9.86 % (468662)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=300079660:i=127:av=off:fsr=off:sup=off_2938 on theBenchmark for (2938ds/127Mi)
% 29.59/9.86 % (468660)Instruction limit reached!
% 29.59/9.86 % (468660)------------------------------
% 29.59/9.86 % (468660)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.59/9.86 % (468660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.59/9.86 % (468660)CaDiCaL version: 2.1.3
% 29.59/9.86 % (468660)Termination reason: Instruction limit
% 29.59/9.86 % (468660)Termination phase: SInE selection
% 29.59/9.86 % (468660)Time elapsed: 0.091 s
% 29.59/9.86 % (468660)Peak memory usage: 201 MB
% 29.59/9.86 % (468660)Instructions burned: 114 (million)
% 29.59/9.86 % (468658)Instruction limit reached!
% 29.59/9.86 % (468658)------------------------------
% 29.59/9.86 % (468658)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.59/9.86 % (468658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.59/9.86 % (468658)CaDiCaL version: 2.1.3
% 29.59/9.86 % (468658)Termination reason: Instruction limit
% 29.59/9.86 % (468658)Termination phase: SInE selection
% 29.59/9.86 % (468658)Time elapsed: 0.229 s
% 29.59/9.86 % (468658)Peak memory usage: 201 MB
% 29.59/9.86 % (468658)Instructions burned: 295 (million)
% 29.59/9.86 % (468662)Instruction limit reached!
% 29.59/9.86 % (468662)------------------------------
% 29.59/9.86 % (468662)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.59/9.86 % (468662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.59/9.86 % (468662)CaDiCaL version: 2.1.3
% 29.59/9.86 % (468662)Termination reason: Instruction limit
% 29.59/9.86 % (468662)Termination phase: Preprocessing 1
% 29.59/9.86 % (468662)Time elapsed: 0.099 s
% 73.66/15.93 % (468662)Peak memory usage: 202 MB
% 73.66/15.93 % (468662)Instructions burned: 127 (million)
% 73.66/15.93 % (468666)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=54067620:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2936 on theBenchmark for (2936ds/114Mi)
% 73.66/15.93 % (468667)lrs+10_1_sil=8000:sp=occurrence:random_seed=550226830:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2936 on theBenchmark for (2936ds/907Mi)
% 73.66/15.93 % (468668)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2423863753:i=437:sd=1:aac=none:ss=included_2936 on theBenchmark for (2936ds/437Mi)
% 73.66/15.93 % (468666)Instruction limit reached!
% 73.66/15.93 % (468666)------------------------------
% 73.66/15.93 % (468666)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 73.66/15.93 % (468666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.66/15.93 % (468666)CaDiCaL version: 2.1.3
% 73.66/15.93 % (468666)Termination reason: Instruction limit
% 73.66/15.93 % (468666)Termination phase: Property scanning
% 73.66/15.93 % (468666)Time elapsed: 0.056 s
% 73.66/15.93 % (468666)Peak memory usage: 201 MB
% 73.66/15.93 % (468666)Instructions burned: 114 (million)
% 73.66/15.93 % (468672)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1550614480:i=5202:ss=axioms:sgt=16_2934 on theBenchmark for (2934ds/5202Mi)
% 73.66/15.93 % (468668)Instruction limit reached!
% 73.66/15.93 % (468668)------------------------------
% 73.66/15.93 % (468668)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 73.66/15.93 % (468668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.66/15.93 % (468668)CaDiCaL version: 2.1.3
% 73.66/15.93 % (468668)Termination reason: Instruction limit
% 73.66/15.93 % (468668)Termination phase: SInE selection
% 73.66/15.93 % (468668)Time elapsed: 0.313 s
% 73.66/15.93 % (468668)Peak memory usage: 202 MB
% 73.66/15.93 % (468668)Instructions burned: 437 (million)
% 73.66/15.93 % (468674)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=851248543:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2931 on theBenchmark for (2931ds/134Mi)
% 73.66/15.93 % (468674)Instruction limit reached!
% 73.66/15.93 % (468674)------------------------------
% 73.66/15.93 % (468674)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 73.66/15.93 % (468674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.66/15.93 % (468674)CaDiCaL version: 2.1.3
% 73.66/15.93 % (468674)Termination reason: Instruction limit
% 73.66/15.93 % (468674)Termination phase: SInE selection
% 73.66/15.93 % (468674)Time elapsed: 0.101 s
% 73.66/15.93 % (468674)Peak memory usage: 201 MB
% 73.66/15.93 % (468674)Instructions burned: 135 (million)
% 73.66/15.93 % (468667)Instruction limit reached!
% 73.66/15.93 % (468667)------------------------------
% 73.66/15.93 % (468667)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 73.66/15.93 % (468667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.66/15.93 % (468667)CaDiCaL version: 2.1.3
% 73.66/15.93 % (468667)Termination reason: Instruction limit
% 73.66/15.93 % (468667)Termination phase: Preprocessing 1
% 73.66/15.93 % (468667)Time elapsed: 0.644 s
% 73.66/15.93 % (468667)Peak memory usage: 204 MB
% 73.66/15.93 % (468667)Instructions burned: 907 (million)
% 73.66/15.93 % (468676)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2699600162:st=8:i=592:sd=3:ep=RST:ss=axioms_2929 on theBenchmark for (2929ds/592Mi)
% 73.66/15.93 % (468677)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2433660741:st=3:i=13193:sd=3:ss=axioms_2928 on theBenchmark for (2928ds/13193Mi)
% 73.66/15.93 % (468676)Instruction limit reached!
% 73.66/15.93 % (468676)------------------------------
% 73.66/15.93 % (468676)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 73.66/15.93 % (468676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.66/15.93 % (468676)CaDiCaL version: 2.1.3
% 73.66/15.93 % (468676)Termination reason: Instruction limit
% 73.66/15.93 % (468676)Termination phase: SInE selection
% 73.66/15.93 % (468676)Time elapsed: 0.379 s
% 73.66/15.93 % (468676)Peak memory usage: 203 MB
% 73.66/15.93 % (468676)Instructions burned: 593 (million)
% 73.66/15.93 % (468680)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=2393537417:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2924 on theBenchmark for (2924ds/125Mi)
% 73.66/15.93 % (468680)Instruction limit reached!
% 73.66/15.93 % (468680)------------------------------
% 95.88/19.08 % (468680)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.88/19.08 % (468680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.88/19.08 % (468680)CaDiCaL version: 2.1.3
% 95.88/19.08 % (468680)Termination reason: Instruction limit
% 95.88/19.08 % (468680)Termination phase: Property scanning
% 95.88/19.08 % (468680)Time elapsed: 0.061 s
% 95.88/19.08 % (468680)Peak memory usage: 201 MB
% 95.88/19.08 % (468680)Instructions burned: 127 (million)
% 95.88/19.08 % (468682)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=197881353:i=134:gtgl=5:slsql=off:gtg=exists_sym_2921 on theBenchmark for (2921ds/134Mi)
% 95.88/19.08 % (468682)Instruction limit reached!
% 95.88/19.08 % (468682)------------------------------
% 95.88/19.08 % (468682)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.88/19.08 % (468682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.88/19.08 % (468682)CaDiCaL version: 2.1.3
% 95.88/19.08 % (468682)Termination reason: Instruction limit
% 95.88/19.08 % (468682)Termination phase: Property scanning
% 95.88/19.08 % (468682)Time elapsed: 0.065 s
% 95.88/19.08 % (468682)Peak memory usage: 201 MB
% 95.88/19.08 % (468682)Instructions burned: 135 (million)
% 95.88/19.08 % (468659)Instruction limit reached!
% 95.88/19.08 % (468659)------------------------------
% 95.88/19.08 % (468659)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.88/19.08 % (468659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.88/19.08 % (468659)CaDiCaL version: 2.1.3
% 95.88/19.08 % (468659)Termination reason: Instruction limit
% 95.88/19.08 % (468659)Termination phase: Preprocessing 3
% 95.88/19.08 % (468659)Time elapsed: 1.879 s
% 95.88/19.08 % (468659)Peak memory usage: 305 MB
% 95.88/19.08 % (468659)Instructions burned: 2351 (million)
% 95.88/19.08 % (468684)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1000129818:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2919 on theBenchmark for (2919ds/141Mi)
% 95.88/19.08 % (468684)Instruction limit reached!
% 95.88/19.08 % (468684)------------------------------
% 95.88/19.08 % (468684)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.88/19.08 % (468684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.88/19.08 % (468684)CaDiCaL version: 2.1.3
% 95.88/19.08 % (468684)Termination reason: Instruction limit
% 95.88/19.08 % (468684)Termination phase: SInE selection
% 95.88/19.08 % (468684)Time elapsed: 0.106 s
% 95.88/19.08 % (468684)Peak memory usage: 201 MB
% 95.88/19.08 % (468684)Instructions burned: 141 (million)
% 95.88/19.08 % (468685)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=340817581:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2918 on theBenchmark for (2918ds/431Mi)
% 95.88/19.08 % (468688)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=845653892:i=6060:aac=none:ins=25_2917 on theBenchmark for (2917ds/6060Mi)
% 95.88/19.08 % (468685)Instruction limit reached!
% 95.88/19.08 % (468685)------------------------------
% 95.88/19.08 % (468685)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.88/19.08 % (468685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.88/19.08 % (468685)CaDiCaL version: 2.1.3
% 95.88/19.08 % (468685)Termination reason: Instruction limit
% 95.88/19.08 % (468685)Termination phase: SInE selection
% 95.88/19.08 % (468685)Time elapsed: 0.325 s
% 95.88/19.08 % (468685)Peak memory usage: 202 MB
% 95.88/19.08 % (468685)Instructions burned: 432 (million)
% 95.88/19.08 % (468690)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=2538455691:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2913 on theBenchmark for (2913ds/150Mi)
% 95.88/19.08 % (468690)Instruction limit reached!
% 95.88/19.08 % (468690)------------------------------
% 95.88/19.08 % (468690)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.88/19.08 % (468690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.88/19.08 % (468690)CaDiCaL version: 2.1.3
% 95.88/19.08 % (468690)Termination reason: Instruction limit
% 95.88/19.08 % (468690)Termination phase: SInE selection
% 95.88/19.08 % (468690)Time elapsed: 0.120 s
% 95.88/19.08 % (468690)Peak memory usage: 201 MB
% 95.88/19.08 % (468690)Instructions burned: 151 (million)
% 95.88/19.08 % (468692)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=459658447:i=14155:bd=all_2911 on theBenchmark for (2911ds/14155Mi)
% 136.83/25.03 % (468672)Instruction limit reached!
% 136.83/25.03 % (468672)------------------------------
% 136.83/25.03 % (468672)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 136.83/25.03 % (468672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.83/25.03 % (468672)CaDiCaL version: 2.1.3
% 136.83/25.03 % (468672)Termination reason: Instruction limit
% 136.83/25.03 % (468672)Termination phase: Saturation
% 136.83/25.03 % (468672)Time elapsed: 3.553 s
% 136.83/25.03 % (468672)Peak memory usage: 437 MB
% 136.83/25.03 % (468672)Instructions burned: 5203 (million)
% 136.83/25.03 % (468694)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3803253232:i=667:av=off:fsr=off_2897 on theBenchmark for (2897ds/667Mi)
% 136.83/25.03 % (468694)Instruction limit reached!
% 136.83/25.03 % (468694)------------------------------
% 136.83/25.03 % (468694)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 136.83/25.03 % (468694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.83/25.03 % (468694)CaDiCaL version: 2.1.3
% 136.83/25.03 % (468694)Termination reason: Instruction limit
% 136.83/25.03 % (468694)Termination phase: Preprocessing 2
% 136.83/25.03 % (468694)Time elapsed: 0.600 s
% 136.83/25.03 % (468694)Peak memory usage: 218 MB
% 136.83/25.03 % (468694)Instructions burned: 668 (million)
% 136.83/25.03 % (468696)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=3488164515:s2a=on:i=185:s2at=1.8:fdi=4_2889 on theBenchmark for (2889ds/185Mi)
% 136.83/25.03 % (468696)Instruction limit reached!
% 136.83/25.03 % (468696)------------------------------
% 136.83/25.03 % (468696)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 136.83/25.03 % (468696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.83/25.03 % (468696)CaDiCaL version: 2.1.3
% 136.83/25.03 % (468696)Termination reason: Instruction limit
% 136.83/25.03 % (468696)Termination phase: SInE selection
% 136.83/25.03 % (468696)Time elapsed: 0.140 s
% 136.83/25.03 % (468696)Peak memory usage: 201 MB
% 136.83/25.03 % (468696)Instructions burned: 186 (million)
% 136.83/25.03 % (468698)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=356560328:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2886 on theBenchmark for (2886ds/193Mi)
% 136.83/25.03 % (468698)Instruction limit reached!
% 136.83/25.03 % (468698)------------------------------
% 136.83/25.03 % (468698)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 136.83/25.03 % (468698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.83/25.03 % (468698)CaDiCaL version: 2.1.3
% 136.83/25.03 % (468698)Termination reason: Instruction limit
% 136.83/25.03 % (468698)Termination phase: SInE selection
% 136.83/25.03 % (468698)Time elapsed: 0.145 s
% 136.83/25.03 % (468698)Peak memory usage: 201 MB
% 136.83/25.03 % (468698)Instructions burned: 194 (million)
% 136.83/25.03 % (468700)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=3998424104:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2883 on theBenchmark for (2883ds/4850Mi)
% 136.83/25.03 % (468688)Instruction limit reached!
% 136.83/25.03 % (468688)------------------------------
% 136.83/25.03 % (468688)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 136.83/25.03 % (468688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.83/25.03 % (468688)CaDiCaL version: 2.1.3
% 136.83/25.03 % (468688)Termination reason: Instruction limit
% 136.83/25.03 % (468688)Termination phase: NewCNF
% 136.83/25.03 % (468688)Time elapsed: 4.849 s
% 136.83/25.03 % (468688)Peak memory usage: 381 MB
% 136.83/25.03 % (468688)Instructions burned: 6060 (million)
% 136.83/25.03 % (468702)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=2124445885:i=12111:sd=1:ss=included_2867 on theBenchmark for (2867ds/12111Mi)
% 136.83/25.03 % (468700)Instruction limit reached!
% 136.83/25.03 % (468700)------------------------------
% 136.83/25.03 % (468700)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 136.83/25.03 % (468700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.83/25.03 % (468700)CaDiCaL version: 2.1.3
% 136.83/25.03 % (468700)Termination reason: Instruction limit
% 136.83/25.03 % (468700)Termination phase: Property scanning
% 136.83/25.03 % (468700)Time elapsed: 3.343 s
% 136.83/25.03 % (468700)Peak memory usage: 356 MB
% 172.24/29.98 % (468700)Instructions burned: 4853 (million)
% 172.24/29.98 % (468677)Instruction limit reached!
% 172.24/29.98 % (468677)------------------------------
% 172.24/29.98 % (468677)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 172.24/29.98 % (468677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 172.24/29.98 % (468677)CaDiCaL version: 2.1.3
% 172.24/29.98 % (468677)Termination reason: Instruction limit
% 172.24/29.98 % (468677)Termination phase: Saturation
% 172.24/29.98 % (468677)Time elapsed: 7.952 s
% 172.24/29.98 % (468677)Peak memory usage: 477 MB
% 172.24/29.98 % (468677)Instructions burned: 13193 (million)
% 172.24/29.98 % (468704)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3512322797:i=319:kws=precedence:fsr=off_2848 on theBenchmark for (2848ds/319Mi)
% 172.24/29.98 % (468706)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=2776565699:i=2064:ep=RST_2847 on theBenchmark for (2847ds/2064Mi)
% 172.24/29.98 % (468704)Instruction limit reached!
% 172.24/29.98 % (468704)------------------------------
% 172.24/29.98 % (468704)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 172.24/29.98 % (468704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 172.24/29.98 % (468704)CaDiCaL version: 2.1.3
% 172.24/29.98 % (468704)Termination reason: Instruction limit
% 172.24/29.98 % (468704)Termination phase: Preprocessing 1
% 172.24/29.98 % (468704)Time elapsed: 0.230 s
% 172.24/29.98 % (468704)Peak memory usage: 203 MB
% 172.24/29.98 % (468704)Instructions burned: 320 (million)
% 172.24/29.98 % (468708)dis-1011_128_sil=32000:random_seed=1847049163:i=3706:ep=RST:av=off_2844 on theBenchmark for (2844ds/3706Mi)
% 172.24/29.98 % (468692)Instruction limit reached!
% 172.24/29.98 % (468692)------------------------------
% 172.24/29.98 % (468692)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 172.24/29.98 % (468692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 172.24/29.98 % (468692)CaDiCaL version: 2.1.3
% 172.24/29.98 % (468692)Termination reason: Instruction limit
% 172.24/29.98 % (468692)Termination phase: Property scanning
% 172.24/29.98 % (468692)Time elapsed: 7.149 s
% 172.24/29.98 % (468692)Peak memory usage: 447 MB
% 172.24/29.98 % (468692)Instructions burned: 14157 (million)
% 172.24/29.98 % (468710)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=783709428:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2837 on theBenchmark for (2837ds/757Mi)
% 172.24/29.98 % (468710)Instruction limit reached!
% 172.24/29.98 % (468710)------------------------------
% 172.24/29.98 % (468710)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 172.24/29.98 % (468710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 172.24/29.98 % (468710)CaDiCaL version: 2.1.3
% 172.24/29.98 % (468710)Termination reason: Instruction limit
% 172.24/29.98 % (468710)Termination phase: Saturation
% 172.24/29.98 % (468710)Time elapsed: 0.592 s
% 172.24/29.98 % (468710)Peak memory usage: 209 MB
% 172.24/29.98 % (468710)Instructions burned: 757 (million)
% 172.24/29.98 % (468706)Instruction limit reached!
% 172.24/29.98 % (468706)------------------------------
% 172.24/29.98 % (468706)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 172.24/29.98 % (468706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 172.24/29.98 % (468706)CaDiCaL version: 2.1.3
% 172.24/29.98 % (468706)Termination reason: Instruction limit
% 172.24/29.98 % (468706)Termination phase: Preprocessing 3
% 172.24/29.98 % (468706)Time elapsed: 1.593 s
% 172.24/29.98 % (468706)Peak memory usage: 317 MB
% 172.24/29.98 % (468706)Instructions burned: 2064 (million)
% 172.24/29.98 % (468712)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2179838018:i=13913:ss=axioms:sgt=8_2830 on theBenchmark for (2830ds/13913Mi)
% 172.24/29.98 % (468713)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=760845366:i=9925:aac=none_2829 on theBenchmark for (2829ds/9925Mi)
% 172.24/29.98 % (468708)Instruction limit reached!
% 172.24/29.98 % (468708)------------------------------
% 172.24/29.98 % (468708)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 172.24/29.98 % (468708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 172.24/29.98 % (468708)CaDiCaL version: 2.1.3
% 172.24/29.98 % (468708)Termination reason: Instruction limit
% 172.24/29.98 % (468708)Termination phase: Preprocessing 3
% 172.24/29.98 % (468708)Time elapsed: 2.598 s
% 172.24/29.98 % (468708)Peak memory usage: 378 MB
% 172.24/29.98 % (468708)Instructions burned: 3706 (million)
% 171.08/33.61 % (468716)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=3574403961:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2817 on theBenchmark for (2817ds/2479Mi)
% 171.08/33.61 % (468716)Instruction limit reached!
% 171.08/33.61 % (468716)------------------------------
% 171.08/33.61 % (468716)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 171.08/33.61 % (468716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 171.08/33.61 % (468716)CaDiCaL version: 2.1.3
% 171.08/33.61 % (468716)Termination reason: Instruction limit
% 171.08/33.61 % (468716)Termination phase: Saturation
% 171.08/33.61 % (468716)Time elapsed: 1.799 s
% 171.08/33.61 % (468716)Peak memory usage: 216 MB
% 171.08/33.61 % (468716)Instructions burned: 2480 (million)
% 171.08/33.61 % (468718)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=938368882:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2797 on theBenchmark for (2797ds/440Mi)
% 171.08/33.61 % (468718)Instruction limit reached!
% 171.08/33.61 % (468718)------------------------------
% 171.08/33.61 % (468718)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 171.08/33.61 % (468718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 171.08/33.61 % (468718)CaDiCaL version: 2.1.3
% 171.08/33.61 % (468718)Termination reason: Instruction limit
% 171.08/33.61 % (468718)Termination phase: Property scanning
% 171.08/33.61 % (468718)Time elapsed: 0.192 s
% 171.08/33.61 % (468718)Peak memory usage: 201 MB
% 171.08/33.61 % (468718)Instructions burned: 441 (million)
% 171.08/33.61 % (468720)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=949952391:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2794 on theBenchmark for (2794ds/11145Mi)
% 171.08/33.61 % (468702)Instruction limit reached!
% 171.08/33.61 % (468702)------------------------------
% 171.08/33.61 % (468702)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 171.08/33.61 % (468702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 171.08/33.61 % (468702)CaDiCaL version: 2.1.3
% 171.08/33.61 % (468702)Termination reason: Instruction limit
% 171.08/33.61 % (468702)Termination phase: Saturation
% 171.08/33.61 % (468702)Time elapsed: 8.334 s
% 171.08/33.61 % (468702)Peak memory usage: 355 MB
% 171.08/33.61 % (468702)Instructions burned: 12113 (million)
% 171.08/33.61 % (468722)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=3309955004:cts=off:i=3034:av=off:er=known:fsd=on_2782 on theBenchmark for (2782ds/3034Mi)
% 171.08/33.61 % (468713)Instruction limit reached!
% 171.08/33.61 % (468713)------------------------------
% 171.08/33.61 % (468713)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 171.08/33.61 % (468713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 171.08/33.61 % (468713)CaDiCaL version: 2.1.3
% 171.08/33.61 % (468713)Termination reason: Instruction limit
% 171.08/33.61 % (468713)Termination phase: Property scanning
% 171.08/33.61 % (468713)Time elapsed: 5.574 s
% 171.08/33.61 % (468713)Peak memory usage: 447 MB
% 171.08/33.61 % (468713)Instructions burned: 9927 (million)
% 171.08/33.61 % (468724)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=1076977864:st=2:s2a=on:i=524:s2at=2:ss=axioms_2771 on theBenchmark for (2771ds/524Mi)
% 171.08/33.61 % (468724)Instruction limit reached!
% 171.08/33.61 % (468724)------------------------------
% 171.08/33.61 % (468724)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 171.08/33.61 % (468724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 171.08/33.61 % (468724)CaDiCaL version: 2.1.3
% 171.08/33.61 % (468724)Termination reason: Instruction limit
% 171.08/33.61 % (468724)Termination phase: SInE selection
% 171.08/33.61 % (468724)Time elapsed: 0.361 s
% 171.08/33.61 % (468724)Peak memory usage: 202 MB
% 171.08/33.61 % (468724)Instructions burned: 525 (million)
% 171.08/33.61 % (468726)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=4122389490:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2766 on theBenchmark for (2766ds/1016Mi)
% 171.08/33.61 % (468722)Instruction limit reached!
% 171.08/33.61 % (468722)------------------------------
% 171.08/33.61 % (468722)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 171.08/33.61 % (468722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 171.08/33.61 % (468722)CaDiCaL version: 2.1.3
% 171.08/33.61 % (468722)Termination reason: Instruction limit
% 171.08/33.61 % (468722)Termination phase: Preprocessing 3
% 171.08/33.61 % (468722)Time elapsed: 2.257 s
% 171.08/33.61 % (468722)Peak memory usage: 337 MB
% 171.08/33.61 % (468722)Instructions burned: 3034 (million)
% 171.08/33.61 % (468726)Instruction limit reached!
% 171.08/33.61 % (468726)------------------------------
% 171.08/33.61 % (468726)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 171.08/33.61 % (468726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 171.08/33.61 % (468726)CaDiCaL version: 2.1.3
% 171.08/33.61 % (468726)Termination reason: Instruction limit
% 171.08/33.61 % (468726)Termination phase: Saturation
% 171.08/33.61 % (468726)Time elapsed: 0.709 s
% 171.08/33.61 % (468726)Peak memory usage: 215 MB
% 171.08/33.61 % (468726)Instructions burned: 1018 (million)
% 171.08/33.61 % (468728)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=2103121717:i=14123:bd=preordered:ins=4_2757 on theBenchmark for (2757ds/14123Mi)
% 171.08/33.61 % (468729)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=4156247330:i=5781:kws=precedence:bd=all:rawr=on_2757 on theBenchmark for (2757ds/5781Mi)
% 171.08/33.61 % (468712)Instruction limit reached!
% 171.08/33.61 % (468712)------------------------------
% 171.08/33.61 % (468712)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 171.08/33.61 % (468712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 171.08/33.61 % (468712)CaDiCaL version: 2.1.3
% 171.08/33.61 % (468712)Termination reason: Instruction limit
% 171.08/33.61 % (468712)Termination phase: Saturation
% 171.08/33.61 % (468712)Time elapsed: 8.314 s
% 171.08/33.61 % (468712)Peak memory usage: 386 MB
% 171.08/33.61 % (468712)Instructions burned: 13914 (million)
% 171.08/33.61 % (468732)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=3691295061:i=2448:gtgl=5:bd=preordered:gtg=all_2745 on theBenchmark for (2745ds/2448Mi)
% 171.08/33.61 % (468732)Instruction limit reached!
% 171.08/33.61 % (468732)------------------------------
% 171.08/33.61 % (468732)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 171.08/33.61 % (468732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 171.08/33.61 % (468732)CaDiCaL version: 2.1.3
% 171.08/33.61 % (468732)Termination reason: Instruction limit
% 171.08/33.61 % (468732)Termination phase: Property scanning
% 171.08/33.61 % (468732)Time elapsed: 1.034 s
% 171.08/33.61 % (468732)Peak memory usage: 201 MB
% 171.08/33.61 % (468732)Instructions burned: 2450 (million)
% 171.08/33.61 % (468734)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=3712523509:i=3223:kws=precedence:fgj=on:av=off_2733 on theBenchmark for (2733ds/3223Mi)
% 171.08/33.61 % (468720)Instruction limit reached!
% 171.08/33.61 % (468720)------------------------------
% 171.08/33.61 % (468720)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 171.08/33.61 % (468720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 171.08/33.61 % (468720)CaDiCaL version: 2.1.3
% 171.08/33.61 % (468720)Termination reason: Instruction limit
% 171.08/33.61 % (468720)Termination phase: Saturation
% 171.08/33.61 % (468720)Time elapsed: 7.386 s
% 171.08/33.61 % (468720)Peak memory usage: 337 MB
% 171.08/33.61 % (468720)Instructions burned: 11145 (million)
% 171.08/33.61 % (468729)Instruction limit reached!
% 171.08/33.61 % (468729)------------------------------
% 171.08/33.61 % (468729)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 171.08/33.61 % (468729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 171.08/33.61 % (468729)CaDiCaL version: 2.1.3
% 171.08/33.61 % (468729)Termination reason: Instruction limit
% 171.08/33.61 % (468729)Termination phase: Property scanning
% 171.08/33.61 % (468729)Time elapsed: 3.860 s
% 171.08/33.61 % (468729)Peak memory usage: 412 MB
% 171.08/33.61 % (468729)Instructions burned: 5782 (million)
% 171.08/33.61 % (468736)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=1151505493:st=5.6:i=2033:sd=3:ss=axioms_2718 on theBenchmark for (2718ds/2033Mi)
% 171.08/33.61 % (468737)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=1534040208:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2717 on theBenchmark for (2717ds/2055Mi)
% 171.08/33.61 % (468734)Instruction limit reached!
% 171.08/33.61 % (468734)------------------------------
% 171.08/33.61 % (468734)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 171.08/33.61 % (468734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 171.08/33.61 % (468734)CaDiCaL version: 2.1.3
% 171.08/33.61 % (468734)Termination reason: Instruction limit
% 171.08/33.61 % (468734)Termination phase: Preprocessing 3
% 171.08/33.61 % (468734)Time elapsed: 2.365 s
% 171.08/33.61 % (468734)Peak memory usage: 342 MB
% 171.08/33.61 % (468734)Instructions burned: 3224 (million)
% 171.08/33.61 % (468740)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=2795929459:i=21611:sd=3:ss=axioms_2708 on theBenchmark for (2708ds/21611Mi)
% 171.08/33.61 % (468737)Instruction limit reached!
% 171.08/33.61 % (468737)------------------------------
% 171.08/33.61 % (468737)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 171.08/33.61 % (468737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 171.08/33.61 % (468737)CaDiCaL version: 2.1.3
% 171.08/33.61 % (468737)Termination reason: Instruction limit
% 171.08/33.61 % (468737)Termination phase: SInE selection
% 171.08/33.61 % (468737)Time elapsed: 1.008 s
% 171.08/33.61 % (468737)Peak memory usage: 203 MB
% 171.08/33.61 % (468737)Instructions burned: 2055 (million)
% 171.08/33.61 % (468742)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=3455780197:i=4835:sd=13:ss=axioms:sgt=23_2705 on theBenchmark for (2705ds/4835Mi)
% 171.08/33.61 % (468736)Instruction limit reached!
% 171.08/33.61 % (468736)------------------------------
% 171.08/33.61 % (468736)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 171.08/33.61 % (468736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 171.08/33.61 % (468736)CaDiCaL version: 2.1.3
% 171.08/33.61 % (468736)Termination reason: Instruction limit
% 171.08/33.61 % (468736)Termination phase: Naming
% 171.08/33.61 % (468736)Time elapsed: 1.544 s
% 171.08/33.61 % (468736)Peak memory usage: 232 MB
% 171.08/33.61 % (468736)Instructions burned: 2033 (million)
% 171.08/33.61 % (468744)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=2651151665:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2701 on theBenchmark for (2701ds/797Mi)
% 171.08/33.61 % (468744)Instruction limit reached!
% 171.08/33.61 % (468744)------------------------------
% 171.08/33.61 % (468744)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 171.08/33.61 % (468744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 171.08/33.61 % (468744)CaDiCaL version: 2.1.3
% 171.08/33.61 % (468744)Termination reason: Instruction limit
% 171.08/33.61 % (468744)Termination phase: SInE selection
% 171.08/33.61 % (468744)Time elapsed: 0.508 s
% 171.08/33.61 % (468744)Peak memory usage: 203 MB
% 171.08/33.61 % (468744)Instructions burned: 798 (million)
% 171.08/33.61 % (468746)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=2932860812:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2694 on theBenchmark for (2694ds/2326Mi)
% 171.08/33.61 % (468740)First to succeed.
% 171.08/33.61 % (468740)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-468631"
% 171.08/33.61 % (468746)Instruction limit reached!
% 171.08/33.61 % (468746)------------------------------
% 171.08/33.61 % (468746)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 171.08/33.61 % (468746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 171.08/33.61 % (468746)CaDiCaL version: 2.1.3
% 171.08/33.61 % (468746)Termination reason: Instruction limit
% 171.08/33.61 % (468746)Termination phase: Preprocessing 3
% 171.08/33.61 % (468746)Time elapsed: 1.757 s
% 171.08/33.61 % (468746)Peak memory usage: 335 MB
% 171.08/33.61 % (468746)Instructions burned: 2327 (million)
% 171.08/33.61 % (468742)Instruction limit reached!
% 171.08/33.61 % (468742)------------------------------
% 171.08/33.61 % (468742)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 171.08/33.61 % (468742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 171.08/33.61 % (468742)CaDiCaL version: 2.1.3
% 171.08/33.61 % (468742)Termination reason: Instruction limit
% 171.08/33.61 % (468742)Termination phase: Saturation
% 171.08/33.61 % (468742)Time elapsed: 2.922 s
% 171.08/33.61 % (468742)Peak memory usage: 254 MB
% 171.08/33.61 % (468742)Instructions burned: 4835 (million)
% 171.08/33.61 % (468740)Refutation found. Thanks to Tanya!
% 171.08/33.61 % SZS status Theorem for theBenchmark
% 171.08/33.61 % SZS output start Proof for theBenchmark
% See solution above
% 198.85/33.86 % (468740)------------------------------
% 198.85/33.86 % (468740)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 198.85/33.86 % (468740)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 198.85/33.86 % (468740)CaDiCaL version: 2.1.3
% 198.85/33.86 % (468740)Termination reason: Refutation
% 198.85/33.86 % (468740)Time elapsed: 2.975 s
% 198.85/33.86 % (468740)Peak memory usage: 306 MB
% 198.85/33.86 % (468740)Instructions burned: 4400 (million)
% 198.85/33.86 % (468740)------------------------------
% 198.85/33.86 % (468740)------------------------------
% 198.85/33.86 % (468631)Success in time 32.768 s
% 198.85/33.86 % Vampire exiting
%------------------------------------------------------------------------------