%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU428+2 : 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 : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:48:57 PM UTC 2026
% Result : Theorem 190.78s 29.01s
% Output : Refutation 0.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 41
% Number of leaves : 57
% Syntax : Number of formulae : 417 ( 63 unt; 39 def)
% Number of atoms : 2456 ( 113 equ)
% Maximal formula atoms : 19 ( 5 avg)
% Number of connectives : 3739 (1700 ~;1898 |; 75 &)
% ( 41 <=>; 24 =>; 0 <=; 1 <~>)
% Maximal formula depth : 24 ( 8 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 37 ( 35 usr; 32 prp; 0-2 aty)
% Number of functors : 27 ( 27 usr; 13 con; 0-4 aty)
% Number of variables : 531 ( 0 sgn 514 !; 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(f430,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(f431,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(f433,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(f434,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(f437,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(f541,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(f542,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(f4465,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(f4496,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(f4497,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(f4499,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(f4500,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)],[f4499]) ).
fof(f4532,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,[],[f4500]) ).
fof(f4538,plain,
! [X0,X1,X2] :
( ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ v1_xboole_0(X2) ),
inference(ennf_transformation,[],[f542]) ).
fof(f4539,plain,
! [X0,X1,X2] :
( m1_subset_1(X0,X2)
| ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2)) ),
inference(ennf_transformation,[],[f541]) ).
fof(f4540,plain,
! [X0,X1,X2] :
( m1_subset_1(X0,X2)
| ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2)) ),
inference(flattening,[],[f4539]) ).
fof(f4575,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,[],[f433]) ).
fof(f4576,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,[],[f4575]) ).
fof(f4579,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,[],[f431]) ).
fof(f4580,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,[],[f4579]) ).
fof(f4581,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,[],[f430]) ).
fof(f4582,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,[],[f4581]) ).
fof(f4588,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,[],[f437]) ).
fof(f4589,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,[],[f4588]) ).
fof(f4594,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,[],[f434]) ).
fof(f4595,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,[],[f4594]) ).
fof(f4601,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,[],[f4497]) ).
fof(f4602,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,[],[f4496]) ).
fof(f4603,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,[],[f4602]) ).
fof(f4604,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,[],[f4465]) ).
fof(f4605,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,[],[f4604]) ).
fof(f4612,plain,
! [X0,X1] :
( X0 = X1
| ? [X2] :
( r2_hidden(X2,X0)
<~> r2_hidden(X2,X1) ) ),
inference(ennf_transformation,[],[f3]) ).
fof(f4658,plain,
! [X0,X1] :
( r1_tarski(X0,X1)
<=> ! [X2] :
( r2_hidden(X2,X1)
| ~ r2_hidden(X2,X0) ) ),
inference(ennf_transformation,[],[f8]) ).
fof(f5426,plain,
( k8_relset_2(sK8,sK9,k4_subset_1(sK8,sK10,sK11),sK12) != k5_subset_1(sK9,k8_relset_2(sK8,sK9,sK10,sK12),k8_relset_2(sK8,sK9,sK11,sK12))
& m1_subset_1(sK12,k1_zfmisc_1(k2_zfmisc_1(sK8,sK9)))
& m1_subset_1(sK11,k1_zfmisc_1(sK8))
& m1_subset_1(sK10,k1_zfmisc_1(sK8)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8,sK9,sK10,sK11,sK12]),skolemize(X0,sK8),skolemize(X1,sK9),skolemize(X2,sK10),skolemize(X3,sK11),skolemize(X4,sK12)],[f4532]) ).
fof(f5454,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,[],[f4601]) ).
fof(f5455,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,[],[f5454]) ).
fof(f5456,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(sK27(X2,X3,X4))))
& r2_hidden(sK27(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,[sK27]),skolemize(X5,sK27(X2,X3,X4))],[f5455]) ).
fof(f5458,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,[],[f4612]) ).
fof(f5459,plain,
! [X0,X1] :
( X0 = X1
| ( ( ~ r2_hidden(sK29(X0,X1),X1)
| ~ r2_hidden(sK29(X0,X1),X0) )
& ( r2_hidden(sK29(X0,X1),X1)
| r2_hidden(sK29(X0,X1),X0) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK29]),skolemize(X2,sK29(X0,X1))],[f5458]) ).
fof(f5473,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(f5474,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,[],[f5473]) ).
fof(f5475,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,[],[f4658]) ).
fof(f5476,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,[],[f5475]) ).
fof(f5477,plain,
! [X0,X1] :
( ( r1_tarski(X0,X1)
| ( ~ r2_hidden(sK42(X0,X1),X1)
& r2_hidden(sK42(X0,X1),X0) ) )
& ( ! [X3] :
( r2_hidden(X3,X1)
| ~ r2_hidden(X3,X0) )
| ~ r1_tarski(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK42]),skolemize(X2,sK42(X0,X1))],[f5476]) ).
fof(f5489,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(f5490,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,[],[f5489]) ).
fof(f5491,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,[],[f5490]) ).
fof(f5492,plain,
! [X0,X1,X2] :
( ( X2 = k2_xboole_0(X0,X1)
| ( ( ( ~ r2_hidden(sK50(X0,X1,X2),X0)
& ~ r2_hidden(sK50(X0,X1,X2),X1) )
| ~ r2_hidden(sK50(X0,X1,X2),X2) )
& ( r2_hidden(sK50(X0,X1,X2),X0)
| r2_hidden(sK50(X0,X1,X2),X1)
| r2_hidden(sK50(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,[sK50]),skolemize(X3,sK50(X0,X1,X2))],[f5491]) ).
fof(f5514,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(f5515,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,[],[f5514]) ).
fof(f5516,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,[],[f5515]) ).
fof(f5517,plain,
! [X0,X1,X2] :
( ( X2 = k3_xboole_0(X0,X1)
| ( ( ~ r2_hidden(sK61(X0,X1,X2),X0)
| ~ r2_hidden(sK61(X0,X1,X2),X1)
| ~ r2_hidden(sK61(X0,X1,X2),X2) )
& ( ( r2_hidden(sK61(X0,X1,X2),X0)
& r2_hidden(sK61(X0,X1,X2),X1) )
| r2_hidden(sK61(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,[sK61]),skolemize(X3,sK61(X0,X1,X2))],[f5516]) ).
fof(f5759,plain,
m1_subset_1(sK10,k1_zfmisc_1(sK8)),
inference(cnf_transformation,[],[f5426]) ).
fof(f5760,plain,
m1_subset_1(sK11,k1_zfmisc_1(sK8)),
inference(cnf_transformation,[],[f5426]) ).
fof(f5761,plain,
m1_subset_1(sK12,k1_zfmisc_1(k2_zfmisc_1(sK8,sK9))),
inference(cnf_transformation,[],[f5426]) ).
fof(f5762,plain,
k8_relset_2(sK8,sK9,k4_subset_1(sK8,sK10,sK11),sK12) != k5_subset_1(sK9,k8_relset_2(sK8,sK9,sK10,sK12),k8_relset_2(sK8,sK9,sK11,sK12)),
inference(cnf_transformation,[],[f5426]) ).
fof(f5772,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ r2_hidden(X0,X1)
| ~ v1_xboole_0(X2) ),
inference(cnf_transformation,[],[f4538]) ).
fof(f5773,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ r2_hidden(X0,X1)
| m1_subset_1(X0,X2) ),
inference(cnf_transformation,[],[f4540]) ).
fof(f5826,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,[],[f4576]) ).
fof(f5828,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,[],[f4580]) ).
fof(f5829,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,[],[f4582]) ).
fof(f5837,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,[],[f4589]) ).
fof(f5840,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,[],[f4595]) ).
fof(f5848,plain,
! [X2,X3,X0,X1,X4] :
( r2_hidden(X3,k8_relset_2(X1,X0,X2,X4))
| r2_hidden(sK27(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,[],[f5456]) ).
fof(f5849,plain,
! [X2,X3,X0,X1,X4] :
( ~ r2_hidden(X3,k9_relat_1(X4,k1_tarski(sK27(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,[],[f5456]) ).
fof(f5850,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,[],[f4603]) ).
fof(f5851,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,[],[f4605]) ).
fof(f5859,plain,
! [X0,X1] :
( r2_hidden(sK29(X0,X1),X1)
| X0 = X1
| r2_hidden(sK29(X0,X1),X0) ),
inference(cnf_transformation,[],[f5459]) ).
fof(f5924,plain,
! [X0,X1] :
( ~ r1_tarski(X1,X0)
| ~ r1_tarski(X0,X1)
| X0 = X1 ),
inference(cnf_transformation,[],[f5474]) ).
fof(f5927,plain,
! [X0,X1] :
( r2_hidden(sK42(X0,X1),X0)
| r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f5477]) ).
fof(f5928,plain,
! [X0,X1] :
( ~ r2_hidden(sK42(X0,X1),X1)
| r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f5477]) ).
fof(f6038,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,[],[f5492]) ).
fof(f6040,plain,
! [X2,X0,X1,X4] :
( r2_hidden(X4,X2)
| ~ r2_hidden(X4,X0)
| k2_xboole_0(X0,X1) != X2 ),
inference(cnf_transformation,[],[f5492]) ).
fof(f6138,plain,
! [X2,X0,X1,X4] :
( r2_hidden(X4,X1)
| ~ r2_hidden(X4,X2)
| k3_xboole_0(X0,X1) != X2 ),
inference(cnf_transformation,[],[f5517]) ).
fof(f6139,plain,
! [X2,X0,X1,X4] :
( r2_hidden(X4,X0)
| ~ r2_hidden(X4,X2)
| k3_xboole_0(X0,X1) != X2 ),
inference(cnf_transformation,[],[f5517]) ).
fof(f6140,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,[],[f5517]) ).
fof(f7094,plain,
! [X0,X1,X4] :
( r2_hidden(X4,k2_xboole_0(X0,X1))
| ~ r2_hidden(X4,X0) ),
inference(equality_resolution,[],[f6040]) ).
fof(f7096,plain,
! [X0,X1,X4] :
( ~ r2_hidden(X4,k2_xboole_0(X0,X1))
| r2_hidden(X4,X1)
| r2_hidden(X4,X0) ),
inference(equality_resolution,[],[f6038]) ).
fof(f7106,plain,
! [X0,X1,X4] :
( r2_hidden(X4,k3_xboole_0(X0,X1))
| ~ r2_hidden(X4,X0)
| ~ r2_hidden(X4,X1) ),
inference(equality_resolution,[],[f6140]) ).
fof(f7107,plain,
! [X0,X1,X4] :
( ~ r2_hidden(X4,k3_xboole_0(X0,X1))
| r2_hidden(X4,X0) ),
inference(equality_resolution,[],[f6139]) ).
fof(f7108,plain,
! [X0,X1,X4] :
( ~ r2_hidden(X4,k3_xboole_0(X0,X1))
| r2_hidden(X4,X1) ),
inference(equality_resolution,[],[f6138]) ).
fof(f7226,definition,
sF214 = k4_subset_1(sK8,sK10,sK11),
introduced(definition,[new_symbols(definition,[sF214])],[function_definition]) ).
fof(f7227,plain,
k4_subset_1(sK8,sK10,sK11) = sF214,
inference(reorient_equations,[],[f7226]) ).
fof(f7228,definition,
sF215 = k8_relset_2(sK8,sK9,sF214,sK12),
introduced(definition,[new_symbols(definition,[sF215])],[function_definition]) ).
fof(f7229,plain,
k8_relset_2(sK8,sK9,sF214,sK12) = sF215,
inference(reorient_equations,[],[f7228]) ).
fof(f7230,definition,
sF216 = k8_relset_2(sK8,sK9,sK10,sK12),
introduced(definition,[new_symbols(definition,[sF216])],[function_definition]) ).
fof(f7231,plain,
k8_relset_2(sK8,sK9,sK10,sK12) = sF216,
inference(reorient_equations,[],[f7230]) ).
fof(f7232,definition,
sF217 = k8_relset_2(sK8,sK9,sK11,sK12),
introduced(definition,[new_symbols(definition,[sF217])],[function_definition]) ).
fof(f7233,plain,
k8_relset_2(sK8,sK9,sK11,sK12) = sF217,
inference(reorient_equations,[],[f7232]) ).
fof(f7234,definition,
sF218 = k5_subset_1(sK9,sF216,sF217),
introduced(definition,[new_symbols(definition,[sF218])],[function_definition]) ).
fof(f7235,plain,
k5_subset_1(sK9,sF216,sF217) = sF218,
inference(reorient_equations,[],[f7234]) ).
fof(f7236,plain,
sF215 != sF218,
inference(definition_folding,[],[f5762,f7235,f7233,f7231,f7229,f7227]) ).
fof(f7237,definition,
sF219 = k2_zfmisc_1(sK8,sK9),
introduced(definition,[new_symbols(definition,[sF219])],[function_definition]) ).
fof(f7238,plain,
k2_zfmisc_1(sK8,sK9) = sF219,
inference(reorient_equations,[],[f7237]) ).
fof(f7239,definition,
sF220 = k1_zfmisc_1(sF219),
introduced(definition,[new_symbols(definition,[sF220])],[function_definition]) ).
fof(f7240,plain,
k1_zfmisc_1(sF219) = sF220,
inference(reorient_equations,[],[f7239]) ).
fof(f7241,plain,
m1_subset_1(sK12,sF220),
inference(definition_folding,[],[f5761,f7240,f7238]) ).
fof(f7242,definition,
sF221 = k1_zfmisc_1(sK8),
introduced(definition,[new_symbols(definition,[sF221])],[function_definition]) ).
fof(f7243,plain,
k1_zfmisc_1(sK8) = sF221,
inference(reorient_equations,[],[f7242]) ).
fof(f7244,plain,
m1_subset_1(sK11,sF221),
inference(definition_folding,[],[f5760,f7243]) ).
fof(f7245,plain,
m1_subset_1(sK10,sF221),
inference(definition_folding,[],[f5759,f7243]) ).
fof(f7611,definition,
( spl222_74
<=> m1_subset_1(sK10,sF221) ),
introduced(definition,[new_symbols(definition,[spl222_74])],[avatar_definition]) ).
fof(f7613,plain,
( m1_subset_1(sK10,sF221)
| ~ spl222_74 ),
inference(avatar_component_clause,[],[f7611]) ).
fof(f7614,plain,
spl222_74,
inference(avatar_split_clause,[],[f7245,f7611]) ).
fof(f7616,definition,
( spl222_75
<=> m1_subset_1(sK11,sF221) ),
introduced(definition,[new_symbols(definition,[spl222_75])],[avatar_definition]) ).
fof(f7618,plain,
( m1_subset_1(sK11,sF221)
| ~ spl222_75 ),
inference(avatar_component_clause,[],[f7616]) ).
fof(f7619,plain,
spl222_75,
inference(avatar_split_clause,[],[f7244,f7616]) ).
fof(f7621,definition,
( spl222_76
<=> m1_subset_1(sK12,sF220) ),
introduced(definition,[new_symbols(definition,[spl222_76])],[avatar_definition]) ).
fof(f7623,plain,
( m1_subset_1(sK12,sF220)
| ~ spl222_76 ),
inference(avatar_component_clause,[],[f7621]) ).
fof(f7624,plain,
spl222_76,
inference(avatar_split_clause,[],[f7241,f7621]) ).
fof(f7626,definition,
( spl222_77
<=> sF215 = sF218 ),
introduced(definition,[new_symbols(definition,[spl222_77])],[avatar_definition]) ).
fof(f7628,plain,
( sF215 != sF218
| spl222_77 ),
inference(avatar_component_clause,[],[f7626]) ).
fof(f7629,plain,
~ spl222_77,
inference(avatar_split_clause,[],[f7236,f7626]) ).
fof(f7636,definition,
( spl222_79
<=> k4_subset_1(sK8,sK10,sK11) = sF214 ),
introduced(definition,[new_symbols(definition,[spl222_79])],[avatar_definition]) ).
fof(f7638,plain,
( k4_subset_1(sK8,sK10,sK11) = sF214
| ~ spl222_79 ),
inference(avatar_component_clause,[],[f7636]) ).
fof(f7639,plain,
spl222_79,
inference(avatar_split_clause,[],[f7227,f7636]) ).
fof(f7641,definition,
( spl222_80
<=> k8_relset_2(sK8,sK9,sF214,sK12) = sF215 ),
introduced(definition,[new_symbols(definition,[spl222_80])],[avatar_definition]) ).
fof(f7643,plain,
( k8_relset_2(sK8,sK9,sF214,sK12) = sF215
| ~ spl222_80 ),
inference(avatar_component_clause,[],[f7641]) ).
fof(f7644,plain,
spl222_80,
inference(avatar_split_clause,[],[f7229,f7641]) ).
fof(f7646,definition,
( spl222_81
<=> k8_relset_2(sK8,sK9,sK10,sK12) = sF216 ),
introduced(definition,[new_symbols(definition,[spl222_81])],[avatar_definition]) ).
fof(f7648,plain,
( k8_relset_2(sK8,sK9,sK10,sK12) = sF216
| ~ spl222_81 ),
inference(avatar_component_clause,[],[f7646]) ).
fof(f7649,plain,
spl222_81,
inference(avatar_split_clause,[],[f7231,f7646]) ).
fof(f7651,definition,
( spl222_82
<=> k8_relset_2(sK8,sK9,sK11,sK12) = sF217 ),
introduced(definition,[new_symbols(definition,[spl222_82])],[avatar_definition]) ).
fof(f7653,plain,
( k8_relset_2(sK8,sK9,sK11,sK12) = sF217
| ~ spl222_82 ),
inference(avatar_component_clause,[],[f7651]) ).
fof(f7654,plain,
spl222_82,
inference(avatar_split_clause,[],[f7233,f7651]) ).
fof(f7656,definition,
( spl222_83
<=> k5_subset_1(sK9,sF216,sF217) = sF218 ),
introduced(definition,[new_symbols(definition,[spl222_83])],[avatar_definition]) ).
fof(f7658,plain,
( k5_subset_1(sK9,sF216,sF217) = sF218
| ~ spl222_83 ),
inference(avatar_component_clause,[],[f7656]) ).
fof(f7659,plain,
spl222_83,
inference(avatar_split_clause,[],[f7235,f7656]) ).
fof(f7661,definition,
( spl222_84
<=> k2_zfmisc_1(sK8,sK9) = sF219 ),
introduced(definition,[new_symbols(definition,[spl222_84])],[avatar_definition]) ).
fof(f7663,plain,
( k2_zfmisc_1(sK8,sK9) = sF219
| ~ spl222_84 ),
inference(avatar_component_clause,[],[f7661]) ).
fof(f7664,plain,
spl222_84,
inference(avatar_split_clause,[],[f7238,f7661]) ).
fof(f7666,definition,
( spl222_85
<=> k1_zfmisc_1(sF219) = sF220 ),
introduced(definition,[new_symbols(definition,[spl222_85])],[avatar_definition]) ).
fof(f7668,plain,
( k1_zfmisc_1(sF219) = sF220
| ~ spl222_85 ),
inference(avatar_component_clause,[],[f7666]) ).
fof(f7669,plain,
spl222_85,
inference(avatar_split_clause,[],[f7240,f7666]) ).
fof(f7671,definition,
( spl222_86
<=> k1_zfmisc_1(sK8) = sF221 ),
introduced(definition,[new_symbols(definition,[spl222_86])],[avatar_definition]) ).
fof(f7673,plain,
( k1_zfmisc_1(sK8) = sF221
| ~ spl222_86 ),
inference(avatar_component_clause,[],[f7671]) ).
fof(f7674,plain,
spl222_86,
inference(avatar_split_clause,[],[f7243,f7671]) ).
fof(f7675,plain,
( m1_subset_1(sF215,k1_zfmisc_1(sK9))
| ~ m1_subset_1(sF214,k1_zfmisc_1(sK8))
| ~ m1_subset_1(sK12,k1_zfmisc_1(k2_zfmisc_1(sK8,sK9)))
| ~ spl222_80 ),
inference(superposition,[],[f5851,f7643]) ).
fof(f7677,definition,
( spl222_87
<=> m1_subset_1(sK12,k1_zfmisc_1(k2_zfmisc_1(sK8,sK9))) ),
introduced(definition,[new_symbols(definition,[spl222_87])],[avatar_definition]) ).
fof(f7681,definition,
( spl222_88
<=> m1_subset_1(sF214,k1_zfmisc_1(sK8)) ),
introduced(definition,[new_symbols(definition,[spl222_88])],[avatar_definition]) ).
fof(f7685,definition,
( spl222_89
<=> m1_subset_1(sF215,k1_zfmisc_1(sK9)) ),
introduced(definition,[new_symbols(definition,[spl222_89])],[avatar_definition]) ).
fof(f7687,plain,
( m1_subset_1(sF215,k1_zfmisc_1(sK9))
| ~ spl222_89 ),
inference(avatar_component_clause,[],[f7685]) ).
fof(f7688,plain,
( ~ spl222_87
| ~ spl222_88
| spl222_89
| ~ spl222_80 ),
inference(avatar_split_clause,[],[f7675,f7641,f7685,f7681,f7677]) ).
fof(f7689,plain,
( k2_zfmisc_1(sK8,sK9) != sF219
| k1_zfmisc_1(sF219) != sF220
| m1_subset_1(sK12,k1_zfmisc_1(k2_zfmisc_1(sK8,sK9)))
| ~ m1_subset_1(sK12,sF220) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f7691,plain,
( m1_subset_1(sF217,k1_zfmisc_1(sK9))
| ~ m1_subset_1(sK11,k1_zfmisc_1(sK8))
| ~ m1_subset_1(sK12,k1_zfmisc_1(k2_zfmisc_1(sK8,sK9)))
| ~ spl222_82 ),
inference(superposition,[],[f5851,f7653]) ).
fof(f7692,plain,
( ~ m1_subset_1(sK11,sF221)
| m1_subset_1(sF217,k1_zfmisc_1(sK9))
| ~ m1_subset_1(sK12,k1_zfmisc_1(k2_zfmisc_1(sK8,sK9)))
| ~ spl222_82
| ~ spl222_86 ),
inference(forward_demodulation,[],[f7691,f7673]) ).
fof(f7693,plain,
( m1_subset_1(sF217,k1_zfmisc_1(sK9))
| ~ m1_subset_1(sK12,k1_zfmisc_1(k2_zfmisc_1(sK8,sK9)))
| ~ spl222_75
| ~ spl222_82
| ~ spl222_86 ),
inference(forward_subsumption_resolution,[],[f7692,f7618]) ).
fof(f7695,definition,
( spl222_90
<=> m1_subset_1(sF217,k1_zfmisc_1(sK9)) ),
introduced(definition,[new_symbols(definition,[spl222_90])],[avatar_definition]) ).
fof(f7697,plain,
( m1_subset_1(sF217,k1_zfmisc_1(sK9))
| ~ spl222_90 ),
inference(avatar_component_clause,[],[f7695]) ).
fof(f7698,plain,
( ~ spl222_87
| spl222_90
| ~ spl222_75
| ~ spl222_82
| ~ spl222_86 ),
inference(avatar_split_clause,[],[f7693,f7671,f7651,f7616,f7695,f7677]) ).
fof(f7699,plain,
( m1_subset_1(sF216,k1_zfmisc_1(sK9))
| ~ m1_subset_1(sK10,k1_zfmisc_1(sK8))
| ~ m1_subset_1(sK12,k1_zfmisc_1(k2_zfmisc_1(sK8,sK9)))
| ~ spl222_81 ),
inference(superposition,[],[f5851,f7648]) ).
fof(f7700,plain,
( ~ m1_subset_1(sK10,sF221)
| m1_subset_1(sF216,k1_zfmisc_1(sK9))
| ~ m1_subset_1(sK12,k1_zfmisc_1(k2_zfmisc_1(sK8,sK9)))
| ~ spl222_81
| ~ spl222_86 ),
inference(forward_demodulation,[],[f7699,f7673]) ).
fof(f7701,plain,
( m1_subset_1(sF216,k1_zfmisc_1(sK9))
| ~ m1_subset_1(sK12,k1_zfmisc_1(k2_zfmisc_1(sK8,sK9)))
| ~ spl222_74
| ~ spl222_81
| ~ spl222_86 ),
inference(forward_subsumption_resolution,[],[f7700,f7613]) ).
fof(f7703,definition,
( spl222_91
<=> m1_subset_1(sF216,k1_zfmisc_1(sK9)) ),
introduced(definition,[new_symbols(definition,[spl222_91])],[avatar_definition]) ).
fof(f7705,plain,
( m1_subset_1(sF216,k1_zfmisc_1(sK9))
| ~ spl222_91 ),
inference(avatar_component_clause,[],[f7703]) ).
fof(f7706,plain,
( ~ spl222_87
| spl222_91
| ~ spl222_74
| ~ spl222_81
| ~ spl222_86 ),
inference(avatar_split_clause,[],[f7701,f7671,f7646,f7611,f7703,f7677]) ).
fof(f7720,plain,
( sF218 = k3_xboole_0(sF216,sF217)
| ~ m1_subset_1(sF216,k1_zfmisc_1(sK9))
| ~ m1_subset_1(sF217,k1_zfmisc_1(sK9))
| ~ spl222_83 ),
inference(superposition,[],[f7658,f5837]) ).
fof(f7727,plain,
( sF218 = k3_xboole_0(sF216,sF217)
| ~ m1_subset_1(sF217,k1_zfmisc_1(sK9))
| ~ spl222_83
| ~ spl222_91 ),
inference(forward_subsumption_resolution,[],[f7720,f7705]) ).
fof(f7729,plain,
( sF218 = k3_xboole_0(sF216,sF217)
| ~ spl222_83
| ~ spl222_90
| ~ spl222_91 ),
inference(forward_subsumption_resolution,[],[f7727,f7697]) ).
fof(f7732,definition,
( spl222_93
<=> sF218 = k3_xboole_0(sF216,sF217) ),
introduced(definition,[new_symbols(definition,[spl222_93])],[avatar_definition]) ).
fof(f7734,plain,
( sF218 = k3_xboole_0(sF216,sF217)
| ~ spl222_93 ),
inference(avatar_component_clause,[],[f7732]) ).
fof(f7735,plain,
( spl222_93
| ~ spl222_83
| ~ spl222_90
| ~ spl222_91 ),
inference(avatar_split_clause,[],[f7729,f7703,f7695,f7656,f7732]) ).
fof(f7739,plain,
( sF214 = k2_xboole_0(sK10,sK11)
| ~ m1_subset_1(sK10,k1_zfmisc_1(sK8))
| ~ m1_subset_1(sK11,k1_zfmisc_1(sK8))
| ~ spl222_79 ),
inference(superposition,[],[f7638,f5826]) ).
fof(f7741,plain,
! [X2,X0,X1] :
( k2_xboole_0(X0,X1) = k4_subset_1(X2,X1,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(X2))
| ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ m1_subset_1(X0,k1_zfmisc_1(X2))
| ~ m1_subset_1(X1,k1_zfmisc_1(X2)) ),
inference(superposition,[],[f5828,f5826]) ).
fof(f7742,plain,
! [X2,X0,X1] :
( k2_xboole_0(X0,X1) = k4_subset_1(X2,X1,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(X2))
| ~ m1_subset_1(X1,k1_zfmisc_1(X2)) ),
inference(duplicate_literal_removal,[],[f7741]) ).
fof(f7746,plain,
( ~ m1_subset_1(sK10,sF221)
| sF214 = k2_xboole_0(sK10,sK11)
| ~ m1_subset_1(sK11,k1_zfmisc_1(sK8))
| ~ spl222_79
| ~ spl222_86 ),
inference(forward_demodulation,[],[f7739,f7673]) ).
fof(f7748,plain,
( sF214 = k2_xboole_0(sK10,sK11)
| ~ m1_subset_1(sK11,k1_zfmisc_1(sK8))
| ~ spl222_74
| ~ spl222_79
| ~ spl222_86 ),
inference(forward_subsumption_resolution,[],[f7746,f7613]) ).
fof(f7750,plain,
( ~ m1_subset_1(sK11,sF221)
| sF214 = k2_xboole_0(sK10,sK11)
| ~ spl222_74
| ~ spl222_79
| ~ spl222_86 ),
inference(forward_demodulation,[],[f7748,f7673]) ).
fof(f7752,plain,
( sF214 = k2_xboole_0(sK10,sK11)
| ~ spl222_74
| ~ spl222_75
| ~ spl222_79
| ~ spl222_86 ),
inference(forward_subsumption_resolution,[],[f7750,f7618]) ).
fof(f7755,definition,
( spl222_94
<=> sF214 = k2_xboole_0(sK10,sK11) ),
introduced(definition,[new_symbols(definition,[spl222_94])],[avatar_definition]) ).
fof(f7757,plain,
( sF214 = k2_xboole_0(sK10,sK11)
| ~ spl222_94 ),
inference(avatar_component_clause,[],[f7755]) ).
fof(f7758,plain,
( spl222_94
| ~ spl222_74
| ~ spl222_75
| ~ spl222_79
| ~ spl222_86 ),
inference(avatar_split_clause,[],[f7752,f7671,f7636,f7616,f7611,f7755]) ).
fof(f7760,plain,
( m1_subset_1(sF214,k1_zfmisc_1(sK8))
| ~ m1_subset_1(sK10,k1_zfmisc_1(sK8))
| ~ m1_subset_1(sK11,k1_zfmisc_1(sK8))
| ~ spl222_79 ),
inference(superposition,[],[f5829,f7638]) ).
fof(f7769,plain,
( m1_subset_1(sF214,sF221)
| ~ m1_subset_1(sK10,k1_zfmisc_1(sK8))
| ~ m1_subset_1(sK11,k1_zfmisc_1(sK8))
| ~ spl222_79
| ~ spl222_86 ),
inference(forward_demodulation,[],[f7760,f7673]) ).
fof(f7770,plain,
( ~ m1_subset_1(sK10,sF221)
| m1_subset_1(sF214,sF221)
| ~ m1_subset_1(sK11,k1_zfmisc_1(sK8))
| ~ spl222_79
| ~ spl222_86 ),
inference(forward_demodulation,[],[f7769,f7673]) ).
fof(f7771,plain,
( m1_subset_1(sF214,sF221)
| ~ m1_subset_1(sK11,k1_zfmisc_1(sK8))
| ~ spl222_74
| ~ spl222_79
| ~ spl222_86 ),
inference(forward_subsumption_resolution,[],[f7770,f7613]) ).
fof(f7772,plain,
( ~ m1_subset_1(sK11,sF221)
| m1_subset_1(sF214,sF221)
| ~ spl222_74
| ~ spl222_79
| ~ spl222_86 ),
inference(forward_demodulation,[],[f7771,f7673]) ).
fof(f7773,plain,
( m1_subset_1(sF214,sF221)
| ~ spl222_74
| ~ spl222_75
| ~ spl222_79
| ~ spl222_86 ),
inference(forward_subsumption_resolution,[],[f7772,f7618]) ).
fof(f7775,definition,
( spl222_95
<=> m1_subset_1(sF214,sF221) ),
introduced(definition,[new_symbols(definition,[spl222_95])],[avatar_definition]) ).
fof(f7777,plain,
( m1_subset_1(sF214,sF221)
| ~ spl222_95 ),
inference(avatar_component_clause,[],[f7775]) ).
fof(f7778,plain,
( spl222_95
| ~ spl222_74
| ~ spl222_75
| ~ spl222_79
| ~ spl222_86 ),
inference(avatar_split_clause,[],[f7773,f7671,f7636,f7616,f7611,f7775]) ).
fof(f7779,plain,
( k1_zfmisc_1(sK8) != sF221
| m1_subset_1(sF214,k1_zfmisc_1(sK8))
| ~ m1_subset_1(sF214,sF221) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f7783,plain,
( m1_subset_1(sF218,k1_zfmisc_1(sK9))
| ~ m1_subset_1(sF216,k1_zfmisc_1(sK9))
| ~ m1_subset_1(sF217,k1_zfmisc_1(sK9))
| ~ spl222_83 ),
inference(superposition,[],[f5840,f7658]) ).
fof(f7792,plain,
( m1_subset_1(sF218,k1_zfmisc_1(sK9))
| ~ m1_subset_1(sF217,k1_zfmisc_1(sK9))
| ~ spl222_83
| ~ spl222_91 ),
inference(forward_subsumption_resolution,[],[f7783,f7705]) ).
fof(f7793,plain,
( m1_subset_1(sF218,k1_zfmisc_1(sK9))
| ~ spl222_83
| ~ spl222_90
| ~ spl222_91 ),
inference(forward_subsumption_resolution,[],[f7792,f7697]) ).
fof(f7795,definition,
( spl222_96
<=> m1_subset_1(sF218,k1_zfmisc_1(sK9)) ),
introduced(definition,[new_symbols(definition,[spl222_96])],[avatar_definition]) ).
fof(f7797,plain,
( m1_subset_1(sF218,k1_zfmisc_1(sK9))
| ~ spl222_96 ),
inference(avatar_component_clause,[],[f7795]) ).
fof(f7798,plain,
( spl222_96
| ~ spl222_83
| ~ spl222_90
| ~ spl222_91 ),
inference(avatar_split_clause,[],[f7793,f7703,f7695,f7656,f7795]) ).
fof(f7800,plain,
( ! [X0,X1] :
( ~ r2_hidden(X0,sF215)
| ~ r2_hidden(X1,sF214)
| r2_hidden(X0,k9_relat_1(sK12,k1_tarski(X1)))
| ~ m1_subset_1(sK12,k1_zfmisc_1(k2_zfmisc_1(sK8,sK9)))
| ~ m1_subset_1(sF214,k1_zfmisc_1(sK8)) )
| ~ spl222_80 ),
inference(superposition,[],[f5850,f7643]) ).
fof(f7801,plain,
( ! [X0,X1] :
( ~ r2_hidden(X0,sF217)
| ~ r2_hidden(X1,sK11)
| r2_hidden(X0,k9_relat_1(sK12,k1_tarski(X1)))
| ~ m1_subset_1(sK12,k1_zfmisc_1(k2_zfmisc_1(sK8,sK9)))
| ~ m1_subset_1(sK11,k1_zfmisc_1(sK8)) )
| ~ spl222_82 ),
inference(superposition,[],[f5850,f7653]) ).
fof(f7802,plain,
( ! [X0,X1] :
( ~ r2_hidden(X0,sF216)
| ~ r2_hidden(X1,sK10)
| r2_hidden(X0,k9_relat_1(sK12,k1_tarski(X1)))
| ~ m1_subset_1(sK12,k1_zfmisc_1(k2_zfmisc_1(sK8,sK9)))
| ~ m1_subset_1(sK10,k1_zfmisc_1(sK8)) )
| ~ spl222_81 ),
inference(superposition,[],[f5850,f7648]) ).
fof(f7803,plain,
( ! [X0,X1] :
( ~ m1_subset_1(sK12,k1_zfmisc_1(sF219))
| ~ r2_hidden(X0,sF216)
| ~ r2_hidden(X1,sK10)
| r2_hidden(X0,k9_relat_1(sK12,k1_tarski(X1)))
| ~ m1_subset_1(sK10,k1_zfmisc_1(sK8)) )
| ~ spl222_81
| ~ spl222_84 ),
inference(forward_demodulation,[],[f7802,f7663]) ).
fof(f7804,plain,
( ! [X0,X1] :
( ~ m1_subset_1(sK12,k1_zfmisc_1(sF219))
| ~ r2_hidden(X0,sF217)
| ~ r2_hidden(X1,sK11)
| r2_hidden(X0,k9_relat_1(sK12,k1_tarski(X1)))
| ~ m1_subset_1(sK11,k1_zfmisc_1(sK8)) )
| ~ spl222_82
| ~ spl222_84 ),
inference(forward_demodulation,[],[f7801,f7663]) ).
fof(f7805,plain,
( ! [X0,X1] :
( ~ m1_subset_1(sK12,k1_zfmisc_1(sF219))
| ~ r2_hidden(X0,sF215)
| ~ r2_hidden(X1,sF214)
| r2_hidden(X0,k9_relat_1(sK12,k1_tarski(X1)))
| ~ m1_subset_1(sF214,k1_zfmisc_1(sK8)) )
| ~ spl222_80
| ~ spl222_84 ),
inference(forward_demodulation,[],[f7800,f7663]) ).
fof(f7806,plain,
( ! [X0,X1] :
( ~ m1_subset_1(sK12,sF220)
| ~ r2_hidden(X0,sF216)
| ~ r2_hidden(X1,sK10)
| r2_hidden(X0,k9_relat_1(sK12,k1_tarski(X1)))
| ~ m1_subset_1(sK10,k1_zfmisc_1(sK8)) )
| ~ spl222_81
| ~ spl222_84
| ~ spl222_85 ),
inference(forward_demodulation,[],[f7803,f7668]) ).
fof(f7807,plain,
( ! [X0,X1] :
( ~ m1_subset_1(sK12,sF220)
| ~ r2_hidden(X0,sF217)
| ~ r2_hidden(X1,sK11)
| r2_hidden(X0,k9_relat_1(sK12,k1_tarski(X1)))
| ~ m1_subset_1(sK11,k1_zfmisc_1(sK8)) )
| ~ spl222_82
| ~ spl222_84
| ~ spl222_85 ),
inference(forward_demodulation,[],[f7804,f7668]) ).
fof(f7808,plain,
( ! [X0,X1] :
( ~ m1_subset_1(sK12,sF220)
| ~ r2_hidden(X0,sF215)
| ~ r2_hidden(X1,sF214)
| r2_hidden(X0,k9_relat_1(sK12,k1_tarski(X1)))
| ~ m1_subset_1(sF214,k1_zfmisc_1(sK8)) )
| ~ spl222_80
| ~ spl222_84
| ~ spl222_85 ),
inference(forward_demodulation,[],[f7805,f7668]) ).
fof(f7809,plain,
( ! [X0,X1] :
( ~ r2_hidden(X0,sF216)
| ~ r2_hidden(X1,sK10)
| r2_hidden(X0,k9_relat_1(sK12,k1_tarski(X1)))
| ~ m1_subset_1(sK10,k1_zfmisc_1(sK8)) )
| ~ spl222_76
| ~ spl222_81
| ~ spl222_84
| ~ spl222_85 ),
inference(forward_subsumption_resolution,[],[f7806,f7623]) ).
fof(f7810,plain,
( ! [X0,X1] :
( ~ r2_hidden(X0,sF217)
| ~ r2_hidden(X1,sK11)
| r2_hidden(X0,k9_relat_1(sK12,k1_tarski(X1)))
| ~ m1_subset_1(sK11,k1_zfmisc_1(sK8)) )
| ~ spl222_76
| ~ spl222_82
| ~ spl222_84
| ~ spl222_85 ),
inference(forward_subsumption_resolution,[],[f7807,f7623]) ).
fof(f7811,plain,
( ! [X0,X1] :
( ~ r2_hidden(X0,sF215)
| ~ r2_hidden(X1,sF214)
| r2_hidden(X0,k9_relat_1(sK12,k1_tarski(X1)))
| ~ m1_subset_1(sF214,k1_zfmisc_1(sK8)) )
| ~ spl222_76
| ~ spl222_80
| ~ spl222_84
| ~ spl222_85 ),
inference(forward_subsumption_resolution,[],[f7808,f7623]) ).
fof(f7812,plain,
( ! [X0,X1] :
( ~ m1_subset_1(sK10,sF221)
| ~ r2_hidden(X0,sF216)
| ~ r2_hidden(X1,sK10)
| r2_hidden(X0,k9_relat_1(sK12,k1_tarski(X1))) )
| ~ spl222_76
| ~ spl222_81
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86 ),
inference(forward_demodulation,[],[f7809,f7673]) ).
fof(f7813,plain,
( ! [X0,X1] :
( ~ m1_subset_1(sK11,sF221)
| ~ r2_hidden(X0,sF217)
| ~ r2_hidden(X1,sK11)
| r2_hidden(X0,k9_relat_1(sK12,k1_tarski(X1))) )
| ~ spl222_76
| ~ spl222_82
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86 ),
inference(forward_demodulation,[],[f7810,f7673]) ).
fof(f7814,plain,
( ! [X0,X1] :
( ~ m1_subset_1(sF214,sF221)
| ~ r2_hidden(X0,sF215)
| ~ r2_hidden(X1,sF214)
| r2_hidden(X0,k9_relat_1(sK12,k1_tarski(X1))) )
| ~ spl222_76
| ~ spl222_80
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86 ),
inference(forward_demodulation,[],[f7811,f7673]) ).
fof(f7815,plain,
( ! [X0,X1] :
( r2_hidden(X0,k9_relat_1(sK12,k1_tarski(X1)))
| ~ r2_hidden(X1,sK10)
| ~ r2_hidden(X0,sF216) )
| ~ spl222_74
| ~ spl222_76
| ~ spl222_81
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86 ),
inference(forward_subsumption_resolution,[],[f7812,f7613]) ).
fof(f7816,plain,
( ! [X0,X1] :
( r2_hidden(X0,k9_relat_1(sK12,k1_tarski(X1)))
| ~ r2_hidden(X1,sK11)
| ~ r2_hidden(X0,sF217) )
| ~ spl222_75
| ~ spl222_76
| ~ spl222_82
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86 ),
inference(forward_subsumption_resolution,[],[f7813,f7618]) ).
fof(f7817,plain,
( ! [X0,X1] :
( r2_hidden(X0,k9_relat_1(sK12,k1_tarski(X1)))
| ~ r2_hidden(X1,sF214)
| ~ r2_hidden(X0,sF215) )
| ~ spl222_76
| ~ spl222_80
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_95 ),
inference(forward_subsumption_resolution,[],[f7814,f7777]) ).
fof(f7819,plain,
( ! [X2,X3,X0,X1] :
( r2_hidden(X0,k8_relset_2(X1,X2,X3,sK12))
| ~ m1_subset_1(sK12,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(sK27(X3,X0,sK12),sK10)
| ~ r2_hidden(X0,sF216) )
| ~ spl222_74
| ~ spl222_76
| ~ spl222_81
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86 ),
inference(resolution,[],[f5849,f7815]) ).
fof(f7820,plain,
( ! [X2,X3,X0,X1] :
( r2_hidden(X0,k8_relset_2(X1,X2,X3,sK12))
| ~ m1_subset_1(sK12,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(sK27(X3,X0,sK12),sK11)
| ~ r2_hidden(X0,sF217) )
| ~ spl222_75
| ~ spl222_76
| ~ spl222_82
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86 ),
inference(resolution,[],[f5849,f7816]) ).
fof(f7822,plain,
( ! [X0] :
( r2_hidden(X0,sF215)
| ~ m1_subset_1(sK12,k1_zfmisc_1(k2_zfmisc_1(sK8,sK9)))
| ~ m1_subset_1(X0,sK9)
| ~ m1_subset_1(sF214,k1_zfmisc_1(sK8))
| v1_xboole_0(sK9)
| ~ r2_hidden(sK27(sF214,X0,sK12),sK11)
| ~ r2_hidden(X0,sF217) )
| ~ spl222_75
| ~ spl222_76
| ~ spl222_80
| ~ spl222_82
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86 ),
inference(superposition,[],[f7820,f7643]) ).
fof(f7827,plain,
( ! [X0] :
( ~ m1_subset_1(sK12,k1_zfmisc_1(sF219))
| r2_hidden(X0,sF215)
| ~ m1_subset_1(X0,sK9)
| ~ m1_subset_1(sF214,k1_zfmisc_1(sK8))
| v1_xboole_0(sK9)
| ~ r2_hidden(sK27(sF214,X0,sK12),sK11)
| ~ r2_hidden(X0,sF217) )
| ~ spl222_75
| ~ spl222_76
| ~ spl222_80
| ~ spl222_82
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86 ),
inference(forward_demodulation,[],[f7822,f7663]) ).
fof(f7829,plain,
( ! [X0] :
( ~ m1_subset_1(sK12,sF220)
| r2_hidden(X0,sF215)
| ~ m1_subset_1(X0,sK9)
| ~ m1_subset_1(sF214,k1_zfmisc_1(sK8))
| v1_xboole_0(sK9)
| ~ r2_hidden(sK27(sF214,X0,sK12),sK11)
| ~ r2_hidden(X0,sF217) )
| ~ spl222_75
| ~ spl222_76
| ~ spl222_80
| ~ spl222_82
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86 ),
inference(forward_demodulation,[],[f7827,f7668]) ).
fof(f7831,plain,
( ! [X0] :
( r2_hidden(X0,sF215)
| ~ m1_subset_1(X0,sK9)
| ~ m1_subset_1(sF214,k1_zfmisc_1(sK8))
| v1_xboole_0(sK9)
| ~ r2_hidden(sK27(sF214,X0,sK12),sK11)
| ~ r2_hidden(X0,sF217) )
| ~ spl222_75
| ~ spl222_76
| ~ spl222_80
| ~ spl222_82
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86 ),
inference(forward_subsumption_resolution,[],[f7829,f7623]) ).
fof(f7833,plain,
( ! [X0] :
( ~ m1_subset_1(sF214,sF221)
| r2_hidden(X0,sF215)
| ~ m1_subset_1(X0,sK9)
| v1_xboole_0(sK9)
| ~ r2_hidden(sK27(sF214,X0,sK12),sK11)
| ~ r2_hidden(X0,sF217) )
| ~ spl222_75
| ~ spl222_76
| ~ spl222_80
| ~ spl222_82
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86 ),
inference(forward_demodulation,[],[f7831,f7673]) ).
fof(f7835,plain,
( ! [X0] :
( r2_hidden(X0,sF215)
| ~ m1_subset_1(X0,sK9)
| v1_xboole_0(sK9)
| ~ r2_hidden(sK27(sF214,X0,sK12),sK11)
| ~ r2_hidden(X0,sF217) )
| ~ spl222_75
| ~ spl222_76
| ~ spl222_80
| ~ spl222_82
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_95 ),
inference(forward_subsumption_resolution,[],[f7833,f7777]) ).
fof(f7837,definition,
( spl222_97
<=> v1_xboole_0(sK9) ),
introduced(definition,[new_symbols(definition,[spl222_97])],[avatar_definition]) ).
fof(f7838,plain,
( ~ v1_xboole_0(sK9)
| spl222_97 ),
inference(avatar_component_clause,[],[f7837]) ).
fof(f7839,plain,
( v1_xboole_0(sK9)
| ~ spl222_97 ),
inference(avatar_component_clause,[],[f7837]) ).
fof(f7845,definition,
( spl222_99
<=> ! [X0] :
( r2_hidden(X0,sF215)
| ~ r2_hidden(X0,sF217)
| ~ r2_hidden(sK27(sF214,X0,sK12),sK11)
| ~ m1_subset_1(X0,sK9) ) ),
introduced(definition,[new_symbols(definition,[spl222_99])],[avatar_definition]) ).
fof(f7846,plain,
( ! [X0] :
( r2_hidden(X0,sF215)
| ~ r2_hidden(X0,sF217)
| ~ r2_hidden(sK27(sF214,X0,sK12),sK11)
| ~ m1_subset_1(X0,sK9) )
| ~ spl222_99 ),
inference(avatar_component_clause,[],[f7845]) ).
fof(f7847,plain,
( spl222_97
| spl222_99
| ~ spl222_75
| ~ spl222_76
| ~ spl222_80
| ~ spl222_82
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_95 ),
inference(avatar_split_clause,[],[f7835,f7775,f7671,f7666,f7661,f7651,f7641,f7621,f7616,f7845,f7837]) ).
fof(f7849,plain,
( ! [X0] :
( r2_hidden(X0,sF215)
| ~ m1_subset_1(sK12,k1_zfmisc_1(k2_zfmisc_1(sK8,sK9)))
| ~ m1_subset_1(X0,sK9)
| ~ m1_subset_1(sF214,k1_zfmisc_1(sK8))
| v1_xboole_0(sK9)
| ~ r2_hidden(sK27(sF214,X0,sK12),sK10)
| ~ r2_hidden(X0,sF216) )
| ~ spl222_74
| ~ spl222_76
| ~ spl222_80
| ~ spl222_81
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86 ),
inference(superposition,[],[f7819,f7643]) ).
fof(f7897,plain,
! [X2,X3,X0,X1,X4,X5] :
( r2_hidden(sK27(X0,X1,X2),X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X3,X4)))
| ~ m1_subset_1(X1,X4)
| ~ m1_subset_1(X0,k1_zfmisc_1(X3))
| v1_xboole_0(X4)
| ~ r2_hidden(X5,X0)
| r2_hidden(X1,k9_relat_1(X2,k1_tarski(X5)))
| ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X3,X4)))
| ~ m1_subset_1(X0,k1_zfmisc_1(X3)) ),
inference(resolution,[],[f5848,f5850]) ).
fof(f7898,plain,
! [X2,X3,X0,X1,X4] :
( r2_hidden(sK27(X0,sK42(X1,k8_relset_2(X2,X3,X0,X4)),X4),X0)
| ~ m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X2,X3)))
| ~ m1_subset_1(sK42(X1,k8_relset_2(X2,X3,X0,X4)),X3)
| ~ m1_subset_1(X0,k1_zfmisc_1(X2))
| v1_xboole_0(X3)
| r1_tarski(X1,k8_relset_2(X2,X3,X0,X4)) ),
inference(resolution,[],[f5848,f5928]) ).
fof(f7901,plain,
( ! [X0] :
( r2_hidden(X0,sF217)
| r2_hidden(sK27(sK11,X0,sK12),sK11)
| ~ m1_subset_1(sK12,k1_zfmisc_1(k2_zfmisc_1(sK8,sK9)))
| ~ m1_subset_1(X0,sK9)
| ~ m1_subset_1(sK11,k1_zfmisc_1(sK8))
| v1_xboole_0(sK9) )
| ~ spl222_82 ),
inference(superposition,[],[f5848,f7653]) ).
fof(f7902,plain,
( ! [X0] :
( r2_hidden(X0,sF216)
| r2_hidden(sK27(sK10,X0,sK12),sK10)
| ~ m1_subset_1(sK12,k1_zfmisc_1(k2_zfmisc_1(sK8,sK9)))
| ~ m1_subset_1(X0,sK9)
| ~ m1_subset_1(sK10,k1_zfmisc_1(sK8))
| v1_xboole_0(sK9) )
| ~ spl222_81 ),
inference(superposition,[],[f5848,f7648]) ).
fof(f7903,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X3,X4)))
| r2_hidden(sK27(X0,X1,X2),X0)
| ~ m1_subset_1(X1,X4)
| ~ m1_subset_1(X0,k1_zfmisc_1(X3))
| v1_xboole_0(X4)
| ~ r2_hidden(X5,X0)
| r2_hidden(X1,k9_relat_1(X2,k1_tarski(X5))) ),
inference(duplicate_literal_removal,[],[f7897]) ).
fof(f7909,plain,
! [X2,X3,X0,X1,X4,X5] :
( r2_hidden(sK42(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,[],[f5927,f5850]) ).
fof(f7955,plain,
( sF214 = k2_xboole_0(sK11,sK10)
| ~ m1_subset_1(sK11,k1_zfmisc_1(sK8))
| ~ m1_subset_1(sK10,k1_zfmisc_1(sK8))
| ~ spl222_79 ),
inference(superposition,[],[f7638,f7742]) ).
fof(f7967,plain,
( ~ m1_subset_1(sK11,sF221)
| sF214 = k2_xboole_0(sK11,sK10)
| ~ m1_subset_1(sK10,k1_zfmisc_1(sK8))
| ~ spl222_79
| ~ spl222_86 ),
inference(forward_demodulation,[],[f7955,f7673]) ).
fof(f7969,plain,
( sF214 = k2_xboole_0(sK11,sK10)
| ~ m1_subset_1(sK10,k1_zfmisc_1(sK8))
| ~ spl222_75
| ~ spl222_79
| ~ spl222_86 ),
inference(forward_subsumption_resolution,[],[f7967,f7618]) ).
fof(f7971,plain,
( ~ m1_subset_1(sK10,sF221)
| sF214 = k2_xboole_0(sK11,sK10)
| ~ spl222_75
| ~ spl222_79
| ~ spl222_86 ),
inference(forward_demodulation,[],[f7969,f7673]) ).
fof(f7973,plain,
( sF214 = k2_xboole_0(sK11,sK10)
| ~ spl222_74
| ~ spl222_75
| ~ spl222_79
| ~ spl222_86 ),
inference(forward_subsumption_resolution,[],[f7971,f7613]) ).
fof(f7976,definition,
( spl222_107
<=> sF214 = k2_xboole_0(sK11,sK10) ),
introduced(definition,[new_symbols(definition,[spl222_107])],[avatar_definition]) ).
fof(f7978,plain,
( sF214 = k2_xboole_0(sK11,sK10)
| ~ spl222_107 ),
inference(avatar_component_clause,[],[f7976]) ).
fof(f7979,plain,
( spl222_107
| ~ spl222_74
| ~ spl222_75
| ~ spl222_79
| ~ spl222_86 ),
inference(avatar_split_clause,[],[f7973,f7671,f7636,f7616,f7611,f7976]) ).
fof(f7983,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF215)
| m1_subset_1(X0,sK9) )
| ~ spl222_89 ),
inference(resolution,[],[f5773,f7687]) ).
fof(f7984,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF216)
| m1_subset_1(X0,sK9) )
| ~ spl222_91 ),
inference(resolution,[],[f5773,f7705]) ).
fof(f7985,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF217)
| m1_subset_1(X0,sK9) )
| ~ spl222_90 ),
inference(resolution,[],[f5773,f7697]) ).
fof(f8493,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF217)
| ~ r2_hidden(X0,sF216)
| r2_hidden(X0,sF218) )
| ~ spl222_93 ),
inference(superposition,[],[f7106,f7734]) ).
fof(f8619,plain,
( ! [X0] :
( m1_subset_1(sK42(sF215,X0),sK9)
| r1_tarski(sF215,X0) )
| ~ spl222_89 ),
inference(resolution,[],[f7983,f5927]) ).
fof(f8897,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF215)
| ~ v1_xboole_0(sK9) )
| ~ spl222_89 ),
inference(resolution,[],[f5772,f7687]) ).
fof(f8900,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF218)
| ~ v1_xboole_0(sK9) )
| ~ spl222_96 ),
inference(resolution,[],[f5772,f7797]) ).
fof(f8919,plain,
( ! [X0] : ~ r2_hidden(X0,sF218)
| ~ spl222_96
| ~ spl222_97 ),
inference(forward_subsumption_resolution,[],[f8900,f7839]) ).
fof(f8922,plain,
( ! [X0] : ~ r2_hidden(X0,sF215)
| ~ spl222_89
| ~ spl222_97 ),
inference(forward_subsumption_resolution,[],[f8897,f7839]) ).
fof(f8972,plain,
( ! [X0] :
( ~ r2_hidden(sK27(sF214,X0,sK12),sK11)
| ~ r2_hidden(X0,sF217)
| r2_hidden(X0,sF215) )
| ~ spl222_90
| ~ spl222_99 ),
inference(forward_subsumption_resolution,[],[f7846,f7985]) ).
fof(f8974,plain,
( ! [X0] :
( r2_hidden(X0,sF215)
| ~ m1_subset_1(sK12,k1_zfmisc_1(k2_zfmisc_1(sK8,sK9)))
| ~ m1_subset_1(sF214,k1_zfmisc_1(sK8))
| v1_xboole_0(sK9)
| ~ r2_hidden(sK27(sF214,X0,sK12),sK10)
| ~ r2_hidden(X0,sF216) )
| ~ spl222_74
| ~ spl222_76
| ~ spl222_80
| ~ spl222_81
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_91 ),
inference(forward_subsumption_resolution,[],[f7849,f7984]) ).
fof(f8977,plain,
( ! [X0] :
( ~ m1_subset_1(sK12,k1_zfmisc_1(sF219))
| r2_hidden(X0,sF216)
| r2_hidden(sK27(sK10,X0,sK12),sK10)
| ~ m1_subset_1(X0,sK9)
| ~ m1_subset_1(sK10,k1_zfmisc_1(sK8))
| v1_xboole_0(sK9) )
| ~ spl222_81
| ~ spl222_84 ),
inference(forward_demodulation,[],[f7902,f7663]) ).
fof(f8978,plain,
( ! [X0] :
( ~ m1_subset_1(sK12,k1_zfmisc_1(sF219))
| r2_hidden(X0,sF217)
| r2_hidden(sK27(sK11,X0,sK12),sK11)
| ~ m1_subset_1(X0,sK9)
| ~ m1_subset_1(sK11,k1_zfmisc_1(sK8))
| v1_xboole_0(sK9) )
| ~ spl222_82
| ~ spl222_84 ),
inference(forward_demodulation,[],[f7901,f7663]) ).
fof(f8985,definition,
( spl222_190
<=> ! [X0] : ~ r2_hidden(X0,sF218) ),
introduced(definition,[new_symbols(definition,[spl222_190])],[avatar_definition]) ).
fof(f8986,plain,
( ! [X0] : ~ r2_hidden(X0,sF218)
| ~ spl222_190 ),
inference(avatar_component_clause,[],[f8985]) ).
fof(f8997,definition,
( spl222_193
<=> ! [X0] : ~ r2_hidden(X0,sF215) ),
introduced(definition,[new_symbols(definition,[spl222_193])],[avatar_definition]) ).
fof(f8998,plain,
( ! [X0] : ~ r2_hidden(X0,sF215)
| ~ spl222_193 ),
inference(avatar_component_clause,[],[f8997]) ).
fof(f9001,plain,
( ! [X0] :
( ~ m1_subset_1(sK12,k1_zfmisc_1(sF219))
| r2_hidden(X0,sF215)
| ~ m1_subset_1(sF214,k1_zfmisc_1(sK8))
| v1_xboole_0(sK9)
| ~ r2_hidden(sK27(sF214,X0,sK12),sK10)
| ~ r2_hidden(X0,sF216) )
| ~ spl222_74
| ~ spl222_76
| ~ spl222_80
| ~ spl222_81
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_91 ),
inference(forward_demodulation,[],[f8974,f7663]) ).
fof(f9004,plain,
( ! [X0] :
( ~ m1_subset_1(sK12,sF220)
| r2_hidden(X0,sF216)
| r2_hidden(sK27(sK10,X0,sK12),sK10)
| ~ m1_subset_1(X0,sK9)
| ~ m1_subset_1(sK10,k1_zfmisc_1(sK8))
| v1_xboole_0(sK9) )
| ~ spl222_81
| ~ spl222_84
| ~ spl222_85 ),
inference(forward_demodulation,[],[f8977,f7668]) ).
fof(f9005,plain,
( ! [X0] :
( ~ m1_subset_1(sK12,sF220)
| r2_hidden(X0,sF217)
| r2_hidden(sK27(sK11,X0,sK12),sK11)
| ~ m1_subset_1(X0,sK9)
| ~ m1_subset_1(sK11,k1_zfmisc_1(sK8))
| v1_xboole_0(sK9) )
| ~ spl222_82
| ~ spl222_84
| ~ spl222_85 ),
inference(forward_demodulation,[],[f8978,f7668]) ).
fof(f9008,plain,
( ! [X0] :
( ~ m1_subset_1(sK12,sF220)
| r2_hidden(X0,sF215)
| ~ m1_subset_1(sF214,k1_zfmisc_1(sK8))
| v1_xboole_0(sK9)
| ~ r2_hidden(sK27(sF214,X0,sK12),sK10)
| ~ r2_hidden(X0,sF216) )
| ~ spl222_74
| ~ spl222_76
| ~ spl222_80
| ~ spl222_81
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_91 ),
inference(forward_demodulation,[],[f9001,f7668]) ).
fof(f9011,plain,
( ! [X0] :
( r2_hidden(X0,sF216)
| r2_hidden(sK27(sK10,X0,sK12),sK10)
| ~ m1_subset_1(X0,sK9)
| ~ m1_subset_1(sK10,k1_zfmisc_1(sK8))
| v1_xboole_0(sK9) )
| ~ spl222_76
| ~ spl222_81
| ~ spl222_84
| ~ spl222_85 ),
inference(forward_subsumption_resolution,[],[f9004,f7623]) ).
fof(f9012,plain,
( ! [X0] :
( r2_hidden(X0,sF217)
| r2_hidden(sK27(sK11,X0,sK12),sK11)
| ~ m1_subset_1(X0,sK9)
| ~ m1_subset_1(sK11,k1_zfmisc_1(sK8))
| v1_xboole_0(sK9) )
| ~ spl222_76
| ~ spl222_82
| ~ spl222_84
| ~ spl222_85 ),
inference(forward_subsumption_resolution,[],[f9005,f7623]) ).
fof(f9015,plain,
( ! [X0] :
( r2_hidden(X0,sF215)
| ~ m1_subset_1(sF214,k1_zfmisc_1(sK8))
| v1_xboole_0(sK9)
| ~ r2_hidden(sK27(sF214,X0,sK12),sK10)
| ~ r2_hidden(X0,sF216) )
| ~ spl222_74
| ~ spl222_76
| ~ spl222_80
| ~ spl222_81
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_91 ),
inference(forward_subsumption_resolution,[],[f9008,f7623]) ).
fof(f9018,plain,
( ! [X0] :
( ~ m1_subset_1(sK10,sF221)
| r2_hidden(X0,sF216)
| r2_hidden(sK27(sK10,X0,sK12),sK10)
| ~ m1_subset_1(X0,sK9)
| v1_xboole_0(sK9) )
| ~ spl222_76
| ~ spl222_81
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86 ),
inference(forward_demodulation,[],[f9011,f7673]) ).
fof(f9019,plain,
( ! [X0] :
( ~ m1_subset_1(sK11,sF221)
| r2_hidden(X0,sF217)
| r2_hidden(sK27(sK11,X0,sK12),sK11)
| ~ m1_subset_1(X0,sK9)
| v1_xboole_0(sK9) )
| ~ spl222_76
| ~ spl222_82
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86 ),
inference(forward_demodulation,[],[f9012,f7673]) ).
fof(f9022,plain,
( ! [X0] :
( ~ m1_subset_1(sF214,sF221)
| r2_hidden(X0,sF215)
| v1_xboole_0(sK9)
| ~ r2_hidden(sK27(sF214,X0,sK12),sK10)
| ~ r2_hidden(X0,sF216) )
| ~ spl222_74
| ~ spl222_76
| ~ spl222_80
| ~ spl222_81
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_91 ),
inference(forward_demodulation,[],[f9015,f7673]) ).
fof(f9025,plain,
( ! [X0] :
( r2_hidden(X0,sF216)
| r2_hidden(sK27(sK10,X0,sK12),sK10)
| ~ m1_subset_1(X0,sK9)
| v1_xboole_0(sK9) )
| ~ spl222_74
| ~ spl222_76
| ~ spl222_81
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86 ),
inference(forward_subsumption_resolution,[],[f9018,f7613]) ).
fof(f9026,plain,
( ! [X0] :
( r2_hidden(X0,sF217)
| r2_hidden(sK27(sK11,X0,sK12),sK11)
| ~ m1_subset_1(X0,sK9)
| v1_xboole_0(sK9) )
| ~ spl222_75
| ~ spl222_76
| ~ spl222_82
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86 ),
inference(forward_subsumption_resolution,[],[f9019,f7618]) ).
fof(f9029,plain,
( ! [X0] :
( r2_hidden(X0,sF215)
| v1_xboole_0(sK9)
| ~ r2_hidden(sK27(sF214,X0,sK12),sK10)
| ~ r2_hidden(X0,sF216) )
| ~ spl222_74
| ~ spl222_76
| ~ spl222_80
| ~ spl222_81
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_91
| ~ spl222_95 ),
inference(forward_subsumption_resolution,[],[f9022,f7777]) ).
fof(f9033,definition,
( spl222_194
<=> ! [X0] :
( r2_hidden(X0,sF216)
| ~ m1_subset_1(X0,sK9)
| r2_hidden(sK27(sK10,X0,sK12),sK10) ) ),
introduced(definition,[new_symbols(definition,[spl222_194])],[avatar_definition]) ).
fof(f9034,plain,
( ! [X0] :
( r2_hidden(sK27(sK10,X0,sK12),sK10)
| ~ m1_subset_1(X0,sK9)
| r2_hidden(X0,sF216) )
| ~ spl222_194 ),
inference(avatar_component_clause,[],[f9033]) ).
fof(f9035,plain,
( spl222_97
| spl222_194
| ~ spl222_74
| ~ spl222_76
| ~ spl222_81
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86 ),
inference(avatar_split_clause,[],[f9025,f7671,f7666,f7661,f7646,f7621,f7611,f9033,f7837]) ).
fof(f9037,definition,
( spl222_195
<=> ! [X0] :
( r2_hidden(X0,sF217)
| ~ m1_subset_1(X0,sK9)
| r2_hidden(sK27(sK11,X0,sK12),sK11) ) ),
introduced(definition,[new_symbols(definition,[spl222_195])],[avatar_definition]) ).
fof(f9038,plain,
( ! [X0] :
( r2_hidden(sK27(sK11,X0,sK12),sK11)
| ~ m1_subset_1(X0,sK9)
| r2_hidden(X0,sF217) )
| ~ spl222_195 ),
inference(avatar_component_clause,[],[f9037]) ).
fof(f9039,plain,
( spl222_97
| spl222_195
| ~ spl222_75
| ~ spl222_76
| ~ spl222_82
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86 ),
inference(avatar_split_clause,[],[f9026,f7671,f7666,f7661,f7651,f7621,f7616,f9037,f7837]) ).
fof(f9049,definition,
( spl222_198
<=> ! [X0] :
( r2_hidden(X0,sF215)
| ~ r2_hidden(X0,sF216)
| ~ r2_hidden(sK27(sF214,X0,sK12),sK10) ) ),
introduced(definition,[new_symbols(definition,[spl222_198])],[avatar_definition]) ).
fof(f9050,plain,
( ! [X0] :
( ~ r2_hidden(sK27(sF214,X0,sK12),sK10)
| ~ r2_hidden(X0,sF216)
| r2_hidden(X0,sF215) )
| ~ spl222_198 ),
inference(avatar_component_clause,[],[f9049]) ).
fof(f9051,plain,
( spl222_97
| spl222_198
| ~ spl222_74
| ~ spl222_76
| ~ spl222_80
| ~ spl222_81
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_91
| ~ spl222_95 ),
inference(avatar_split_clause,[],[f9029,f7775,f7703,f7671,f7666,f7661,f7646,f7641,f7621,f7611,f9049,f7837]) ).
fof(f9060,plain,
( spl222_190
| ~ spl222_96
| ~ spl222_97 ),
inference(avatar_split_clause,[],[f8919,f7837,f7795,f8985]) ).
fof(f9063,plain,
( spl222_193
| ~ spl222_89
| ~ spl222_97 ),
inference(avatar_split_clause,[],[f8922,f7837,f7685,f8997]) ).
fof(f9460,plain,
( ! [X0,X1] :
( r2_hidden(sK42(sF215,X0),k9_relat_1(sK12,k1_tarski(X1)))
| ~ r2_hidden(X1,sF214)
| r1_tarski(sF215,X0)
| ~ m1_subset_1(sK12,k1_zfmisc_1(k2_zfmisc_1(sK8,sK9)))
| ~ m1_subset_1(sF214,k1_zfmisc_1(sK8)) )
| ~ spl222_80 ),
inference(superposition,[],[f7909,f7643]) ).
fof(f9719,plain,
( ! [X0,X1] :
( ~ m1_subset_1(sK12,k1_zfmisc_1(sF219))
| r2_hidden(sK42(sF215,X0),k9_relat_1(sK12,k1_tarski(X1)))
| ~ r2_hidden(X1,sF214)
| r1_tarski(sF215,X0)
| ~ m1_subset_1(sF214,k1_zfmisc_1(sK8)) )
| ~ spl222_80
| ~ spl222_84 ),
inference(forward_demodulation,[],[f9460,f7663]) ).
fof(f9725,plain,
( ! [X0,X1] :
( ~ m1_subset_1(sK12,sF220)
| r2_hidden(sK42(sF215,X0),k9_relat_1(sK12,k1_tarski(X1)))
| ~ r2_hidden(X1,sF214)
| r1_tarski(sF215,X0)
| ~ m1_subset_1(sF214,k1_zfmisc_1(sK8)) )
| ~ spl222_80
| ~ spl222_84
| ~ spl222_85 ),
inference(forward_demodulation,[],[f9719,f7668]) ).
fof(f9731,plain,
( ! [X0,X1] :
( r2_hidden(sK42(sF215,X0),k9_relat_1(sK12,k1_tarski(X1)))
| ~ r2_hidden(X1,sF214)
| r1_tarski(sF215,X0)
| ~ m1_subset_1(sF214,k1_zfmisc_1(sK8)) )
| ~ spl222_76
| ~ spl222_80
| ~ spl222_84
| ~ spl222_85 ),
inference(forward_subsumption_resolution,[],[f9725,f7623]) ).
fof(f9737,plain,
( ! [X0,X1] :
( ~ m1_subset_1(sF214,sF221)
| r2_hidden(sK42(sF215,X0),k9_relat_1(sK12,k1_tarski(X1)))
| ~ r2_hidden(X1,sF214)
| r1_tarski(sF215,X0) )
| ~ spl222_76
| ~ spl222_80
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86 ),
inference(forward_demodulation,[],[f9731,f7673]) ).
fof(f9743,plain,
( ! [X0,X1] :
( r2_hidden(sK42(sF215,X0),k9_relat_1(sK12,k1_tarski(X1)))
| ~ r2_hidden(X1,sF214)
| r1_tarski(sF215,X0) )
| ~ spl222_76
| ~ spl222_80
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_95 ),
inference(forward_subsumption_resolution,[],[f9737,f7777]) ).
fof(f9778,plain,
( ! [X2,X3,X0,X1] :
( r2_hidden(sK42(sF215,X1),k8_relset_2(X2,X3,X0,sK12))
| r1_tarski(sF215,X1)
| ~ r2_hidden(sK27(X0,sK42(sF215,X1),sK12),sF214)
| ~ m1_subset_1(sK12,k1_zfmisc_1(k2_zfmisc_1(X2,X3)))
| ~ m1_subset_1(sK42(sF215,X1),X3)
| ~ m1_subset_1(X0,k1_zfmisc_1(X2))
| v1_xboole_0(X3) )
| ~ spl222_76
| ~ spl222_80
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_95 ),
inference(resolution,[],[f9743,f5849]) ).
fof(f9891,plain,
( ! [X0] :
( r2_hidden(sK42(sF215,X0),sF217)
| r1_tarski(sF215,X0)
| ~ r2_hidden(sK27(sK11,sK42(sF215,X0),sK12),sF214)
| ~ m1_subset_1(sK12,k1_zfmisc_1(k2_zfmisc_1(sK8,sK9)))
| ~ m1_subset_1(sK42(sF215,X0),sK9)
| ~ m1_subset_1(sK11,k1_zfmisc_1(sK8))
| v1_xboole_0(sK9) )
| ~ spl222_76
| ~ spl222_80
| ~ spl222_82
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_95 ),
inference(superposition,[],[f9778,f7653]) ).
fof(f9892,plain,
( ! [X0] :
( r2_hidden(sK42(sF215,X0),sF216)
| r1_tarski(sF215,X0)
| ~ r2_hidden(sK27(sK10,sK42(sF215,X0),sK12),sF214)
| ~ m1_subset_1(sK12,k1_zfmisc_1(k2_zfmisc_1(sK8,sK9)))
| ~ m1_subset_1(sK42(sF215,X0),sK9)
| ~ m1_subset_1(sK10,k1_zfmisc_1(sK8))
| v1_xboole_0(sK9) )
| ~ spl222_76
| ~ spl222_80
| ~ spl222_81
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_95 ),
inference(superposition,[],[f9778,f7648]) ).
fof(f10528,plain,
( ! [X0] :
( r2_hidden(sK29(X0,sF215),X0)
| sF215 = X0 )
| ~ spl222_193 ),
inference(resolution,[],[f8998,f5859]) ).
fof(f11221,plain,
( sF215 = sF218
| ~ spl222_190
| ~ spl222_193 ),
inference(resolution,[],[f10528,f8986]) ).
fof(f11225,plain,
( $false
| spl222_77
| ~ spl222_190
| ~ spl222_193 ),
inference(forward_subsumption_resolution,[],[f11221,f7628]) ).
fof(f11226,plain,
( spl222_77
| ~ spl222_190
| ~ spl222_193 ),
inference(avatar_contradiction_clause,[],[f11225]) ).
fof(f12055,plain,
( ! [X0] :
( r2_hidden(sK27(sF214,sK42(X0,sF215),sK12),sF214)
| ~ m1_subset_1(sK12,k1_zfmisc_1(k2_zfmisc_1(sK8,sK9)))
| ~ m1_subset_1(sK42(X0,sF215),sK9)
| ~ m1_subset_1(sF214,k1_zfmisc_1(sK8))
| v1_xboole_0(sK9)
| r1_tarski(X0,sF215) )
| ~ spl222_80 ),
inference(superposition,[],[f7898,f7643]) ).
fof(f12077,plain,
( ! [X0] :
( r2_hidden(sK27(sF214,sK42(X0,sF215),sK12),sF214)
| ~ m1_subset_1(sK12,k1_zfmisc_1(k2_zfmisc_1(sK8,sK9)))
| ~ m1_subset_1(sK42(X0,sF215),sK9)
| ~ m1_subset_1(sF214,k1_zfmisc_1(sK8))
| r1_tarski(X0,sF215) )
| ~ spl222_80
| spl222_97 ),
inference(forward_subsumption_resolution,[],[f12055,f7838]) ).
fof(f13369,plain,
( ! [X0] :
( ~ m1_subset_1(sK12,k1_zfmisc_1(sF219))
| r2_hidden(sK27(sF214,sK42(X0,sF215),sK12),sF214)
| ~ m1_subset_1(sK42(X0,sF215),sK9)
| ~ m1_subset_1(sF214,k1_zfmisc_1(sK8))
| r1_tarski(X0,sF215) )
| ~ spl222_80
| ~ spl222_84
| spl222_97 ),
inference(forward_demodulation,[],[f12077,f7663]) ).
fof(f13373,plain,
( ! [X0] :
( ~ m1_subset_1(sK12,sF220)
| r2_hidden(sK27(sF214,sK42(X0,sF215),sK12),sF214)
| ~ m1_subset_1(sK42(X0,sF215),sK9)
| ~ m1_subset_1(sF214,k1_zfmisc_1(sK8))
| r1_tarski(X0,sF215) )
| ~ spl222_80
| ~ spl222_84
| ~ spl222_85
| spl222_97 ),
inference(forward_demodulation,[],[f13369,f7668]) ).
fof(f13375,plain,
( ! [X0] :
( r2_hidden(sK27(sF214,sK42(X0,sF215),sK12),sF214)
| ~ m1_subset_1(sK42(X0,sF215),sK9)
| ~ m1_subset_1(sF214,k1_zfmisc_1(sK8))
| r1_tarski(X0,sF215) )
| ~ spl222_76
| ~ spl222_80
| ~ spl222_84
| ~ spl222_85
| spl222_97 ),
inference(forward_subsumption_resolution,[],[f13373,f7623]) ).
fof(f13377,plain,
( ! [X0] :
( ~ m1_subset_1(sF214,sF221)
| r2_hidden(sK27(sF214,sK42(X0,sF215),sK12),sF214)
| ~ m1_subset_1(sK42(X0,sF215),sK9)
| r1_tarski(X0,sF215) )
| ~ spl222_76
| ~ spl222_80
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| spl222_97 ),
inference(forward_demodulation,[],[f13375,f7673]) ).
fof(f13379,plain,
( ! [X0] :
( r2_hidden(sK27(sF214,sK42(X0,sF215),sK12),sF214)
| ~ m1_subset_1(sK42(X0,sF215),sK9)
| r1_tarski(X0,sF215) )
| ~ spl222_76
| ~ spl222_80
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_95
| spl222_97 ),
inference(forward_subsumption_resolution,[],[f13377,f7777]) ).
fof(f14852,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF218)
| r2_hidden(X0,sF217) )
| ~ spl222_93 ),
inference(superposition,[],[f7108,f7734]) ).
fof(f14974,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF218)
| r2_hidden(X0,sF216) )
| ~ spl222_93 ),
inference(superposition,[],[f7107,f7734]) ).
fof(f16185,plain,
( ! [X0] :
( ~ r2_hidden(X0,sK10)
| r2_hidden(X0,sF214) )
| ~ spl222_94 ),
inference(superposition,[],[f7094,f7757]) ).
fof(f16186,plain,
( ! [X0] :
( ~ r2_hidden(X0,sK11)
| r2_hidden(X0,sF214) )
| ~ spl222_107 ),
inference(superposition,[],[f7094,f7978]) ).
fof(f16326,plain,
( ! [X0] :
( r2_hidden(sK42(sF215,X0),sF216)
| r1_tarski(sF215,X0)
| ~ r2_hidden(sK27(sK10,sK42(sF215,X0),sK12),sF214)
| ~ m1_subset_1(sK12,k1_zfmisc_1(k2_zfmisc_1(sK8,sK9)))
| ~ m1_subset_1(sK42(sF215,X0),sK9)
| ~ m1_subset_1(sK10,k1_zfmisc_1(sK8)) )
| ~ spl222_76
| ~ spl222_80
| ~ spl222_81
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_95
| spl222_97 ),
inference(forward_subsumption_resolution,[],[f9892,f7838]) ).
fof(f16735,plain,
( ! [X0] :
( r2_hidden(sK27(sK10,X0,sK12),sF214)
| ~ m1_subset_1(X0,sK9)
| r2_hidden(X0,sF216) )
| ~ spl222_94
| ~ spl222_194 ),
inference(resolution,[],[f16185,f9034]) ).
fof(f16767,plain,
( ! [X0] :
( r2_hidden(sK42(sF218,X0),sF217)
| r1_tarski(sF218,X0) )
| ~ spl222_93 ),
inference(resolution,[],[f14852,f5927]) ).
fof(f17220,plain,
( ! [X0] :
( r2_hidden(sK42(sF215,X0),sF216)
| r1_tarski(sF215,X0)
| ~ r2_hidden(sK27(sK10,sK42(sF215,X0),sK12),sF214)
| ~ m1_subset_1(sK12,k1_zfmisc_1(k2_zfmisc_1(sK8,sK9)))
| ~ m1_subset_1(sK10,k1_zfmisc_1(sK8)) )
| ~ spl222_76
| ~ spl222_80
| ~ spl222_81
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_89
| ~ spl222_95
| spl222_97 ),
inference(forward_subsumption_resolution,[],[f16326,f8619]) ).
fof(f17233,plain,
( ! [X0] :
( ~ m1_subset_1(sK12,k1_zfmisc_1(sF219))
| r2_hidden(sK42(sF215,X0),sF216)
| r1_tarski(sF215,X0)
| ~ r2_hidden(sK27(sK10,sK42(sF215,X0),sK12),sF214)
| ~ m1_subset_1(sK10,k1_zfmisc_1(sK8)) )
| ~ spl222_76
| ~ spl222_80
| ~ spl222_81
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_89
| ~ spl222_95
| spl222_97 ),
inference(forward_demodulation,[],[f17220,f7663]) ).
fof(f17234,plain,
( ! [X0] :
( ~ m1_subset_1(sK12,sF220)
| r2_hidden(sK42(sF215,X0),sF216)
| r1_tarski(sF215,X0)
| ~ r2_hidden(sK27(sK10,sK42(sF215,X0),sK12),sF214)
| ~ m1_subset_1(sK10,k1_zfmisc_1(sK8)) )
| ~ spl222_76
| ~ spl222_80
| ~ spl222_81
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_89
| ~ spl222_95
| spl222_97 ),
inference(forward_demodulation,[],[f17233,f7668]) ).
fof(f17235,plain,
( ! [X0] :
( r2_hidden(sK42(sF215,X0),sF216)
| r1_tarski(sF215,X0)
| ~ r2_hidden(sK27(sK10,sK42(sF215,X0),sK12),sF214)
| ~ m1_subset_1(sK10,k1_zfmisc_1(sK8)) )
| ~ spl222_76
| ~ spl222_80
| ~ spl222_81
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_89
| ~ spl222_95
| spl222_97 ),
inference(forward_subsumption_resolution,[],[f17234,f7623]) ).
fof(f17236,plain,
( ! [X0] :
( ~ m1_subset_1(sK10,sF221)
| r2_hidden(sK42(sF215,X0),sF216)
| r1_tarski(sF215,X0)
| ~ r2_hidden(sK27(sK10,sK42(sF215,X0),sK12),sF214) )
| ~ spl222_76
| ~ spl222_80
| ~ spl222_81
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_89
| ~ spl222_95
| spl222_97 ),
inference(forward_demodulation,[],[f17235,f7673]) ).
fof(f17237,plain,
( ! [X0] :
( ~ r2_hidden(sK27(sK10,sK42(sF215,X0),sK12),sF214)
| r1_tarski(sF215,X0)
| r2_hidden(sK42(sF215,X0),sF216) )
| ~ spl222_74
| ~ spl222_76
| ~ spl222_80
| ~ spl222_81
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_89
| ~ spl222_95
| spl222_97 ),
inference(forward_subsumption_resolution,[],[f17236,f7613]) ).
fof(f17243,definition,
( spl222_682
<=> r1_tarski(sF215,sF218) ),
introduced(definition,[new_symbols(definition,[spl222_682])],[avatar_definition]) ).
fof(f17245,plain,
( r1_tarski(sF215,sF218)
| ~ spl222_682 ),
inference(avatar_component_clause,[],[f17243]) ).
fof(f17248,definition,
( spl222_683
<=> r1_tarski(sF218,sF215) ),
introduced(definition,[new_symbols(definition,[spl222_683])],[avatar_definition]) ).
fof(f17333,plain,
( ! [X0] :
( ~ m1_subset_1(sK42(sF215,X0),sK9)
| r2_hidden(sK42(sF215,X0),sF216)
| r1_tarski(sF215,X0)
| r2_hidden(sK42(sF215,X0),sF216) )
| ~ spl222_74
| ~ spl222_76
| ~ spl222_80
| ~ spl222_81
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_89
| ~ spl222_94
| ~ spl222_95
| spl222_97
| ~ spl222_194 ),
inference(resolution,[],[f16735,f17237]) ).
fof(f17342,plain,
( ! [X0] :
( ~ m1_subset_1(sK42(sF215,X0),sK9)
| r2_hidden(sK42(sF215,X0),sF216)
| r1_tarski(sF215,X0) )
| ~ spl222_74
| ~ spl222_76
| ~ spl222_80
| ~ spl222_81
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_89
| ~ spl222_94
| ~ spl222_95
| spl222_97
| ~ spl222_194 ),
inference(duplicate_literal_removal,[],[f17333]) ).
fof(f17346,plain,
( ! [X0] :
( r2_hidden(sK42(sF215,X0),sF216)
| r1_tarski(sF215,X0) )
| ~ spl222_74
| ~ spl222_76
| ~ spl222_80
| ~ spl222_81
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_89
| ~ spl222_94
| ~ spl222_95
| spl222_97
| ~ spl222_194 ),
inference(forward_subsumption_resolution,[],[f17342,f8619]) ).
fof(f17412,plain,
( ~ r1_tarski(sF218,sF215)
| sF215 = sF218
| ~ spl222_682 ),
inference(resolution,[],[f17245,f5924]) ).
fof(f17415,plain,
( ~ r1_tarski(sF218,sF215)
| spl222_77
| ~ spl222_682 ),
inference(forward_subsumption_resolution,[],[f17412,f7628]) ).
fof(f17417,plain,
( ~ spl222_683
| spl222_77
| ~ spl222_682 ),
inference(avatar_split_clause,[],[f17415,f17243,f7626,f17248]) ).
fof(f17425,plain,
( ! [X0] :
( r2_hidden(sK42(sF215,X0),sF217)
| r1_tarski(sF215,X0)
| ~ r2_hidden(sK27(sK11,sK42(sF215,X0),sK12),sF214)
| ~ m1_subset_1(sK12,k1_zfmisc_1(k2_zfmisc_1(sK8,sK9)))
| ~ m1_subset_1(sK42(sF215,X0),sK9)
| ~ m1_subset_1(sK11,k1_zfmisc_1(sK8)) )
| ~ spl222_76
| ~ spl222_80
| ~ spl222_82
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_95
| spl222_97 ),
inference(forward_subsumption_resolution,[],[f9891,f7838]) ).
fof(f17426,plain,
( ! [X0] :
( r2_hidden(sK42(sF215,X0),sF217)
| r1_tarski(sF215,X0)
| ~ r2_hidden(sK27(sK11,sK42(sF215,X0),sK12),sF214)
| ~ m1_subset_1(sK12,k1_zfmisc_1(k2_zfmisc_1(sK8,sK9)))
| ~ m1_subset_1(sK11,k1_zfmisc_1(sK8)) )
| ~ spl222_76
| ~ spl222_80
| ~ spl222_82
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_89
| ~ spl222_95
| spl222_97 ),
inference(forward_subsumption_resolution,[],[f17425,f8619]) ).
fof(f17427,plain,
( ! [X0] :
( ~ m1_subset_1(sK12,k1_zfmisc_1(sF219))
| r2_hidden(sK42(sF215,X0),sF217)
| r1_tarski(sF215,X0)
| ~ r2_hidden(sK27(sK11,sK42(sF215,X0),sK12),sF214)
| ~ m1_subset_1(sK11,k1_zfmisc_1(sK8)) )
| ~ spl222_76
| ~ spl222_80
| ~ spl222_82
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_89
| ~ spl222_95
| spl222_97 ),
inference(forward_demodulation,[],[f17426,f7663]) ).
fof(f17428,plain,
( ! [X0] :
( ~ m1_subset_1(sK12,sF220)
| r2_hidden(sK42(sF215,X0),sF217)
| r1_tarski(sF215,X0)
| ~ r2_hidden(sK27(sK11,sK42(sF215,X0),sK12),sF214)
| ~ m1_subset_1(sK11,k1_zfmisc_1(sK8)) )
| ~ spl222_76
| ~ spl222_80
| ~ spl222_82
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_89
| ~ spl222_95
| spl222_97 ),
inference(forward_demodulation,[],[f17427,f7668]) ).
fof(f17429,plain,
( ! [X0] :
( r2_hidden(sK42(sF215,X0),sF217)
| r1_tarski(sF215,X0)
| ~ r2_hidden(sK27(sK11,sK42(sF215,X0),sK12),sF214)
| ~ m1_subset_1(sK11,k1_zfmisc_1(sK8)) )
| ~ spl222_76
| ~ spl222_80
| ~ spl222_82
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_89
| ~ spl222_95
| spl222_97 ),
inference(forward_subsumption_resolution,[],[f17428,f7623]) ).
fof(f17430,plain,
( ! [X0] :
( ~ m1_subset_1(sK11,sF221)
| r2_hidden(sK42(sF215,X0),sF217)
| r1_tarski(sF215,X0)
| ~ r2_hidden(sK27(sK11,sK42(sF215,X0),sK12),sF214) )
| ~ spl222_76
| ~ spl222_80
| ~ spl222_82
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_89
| ~ spl222_95
| spl222_97 ),
inference(forward_demodulation,[],[f17429,f7673]) ).
fof(f17431,plain,
( ! [X0] :
( ~ r2_hidden(sK27(sK11,sK42(sF215,X0),sK12),sF214)
| r1_tarski(sF215,X0)
| r2_hidden(sK42(sF215,X0),sF217) )
| ~ spl222_75
| ~ spl222_76
| ~ spl222_80
| ~ spl222_82
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_89
| ~ spl222_95
| spl222_97 ),
inference(forward_subsumption_resolution,[],[f17430,f7618]) ).
fof(f17433,plain,
( ! [X0] :
( r2_hidden(sK27(sK11,X0,sK12),sF214)
| r2_hidden(X0,sF217)
| ~ m1_subset_1(X0,sK9) )
| ~ spl222_107
| ~ spl222_195 ),
inference(resolution,[],[f9038,f16186]) ).
fof(f17447,plain,
( ! [X0] :
( r2_hidden(sK42(sF215,X0),sF217)
| ~ m1_subset_1(sK42(sF215,X0),sK9)
| r1_tarski(sF215,X0)
| r2_hidden(sK42(sF215,X0),sF217) )
| ~ spl222_75
| ~ spl222_76
| ~ spl222_80
| ~ spl222_82
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_89
| ~ spl222_95
| spl222_97
| ~ spl222_107
| ~ spl222_195 ),
inference(resolution,[],[f17433,f17431]) ).
fof(f17458,plain,
( ! [X0] :
( r2_hidden(sK42(sF215,X0),sF217)
| ~ m1_subset_1(sK42(sF215,X0),sK9)
| r1_tarski(sF215,X0) )
| ~ spl222_75
| ~ spl222_76
| ~ spl222_80
| ~ spl222_82
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_89
| ~ spl222_95
| spl222_97
| ~ spl222_107
| ~ spl222_195 ),
inference(duplicate_literal_removal,[],[f17447]) ).
fof(f17462,plain,
( ! [X0] :
( r2_hidden(sK42(sF215,X0),sF217)
| r1_tarski(sF215,X0) )
| ~ spl222_75
| ~ spl222_76
| ~ spl222_80
| ~ spl222_82
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_89
| ~ spl222_95
| spl222_97
| ~ spl222_107
| ~ spl222_195 ),
inference(forward_subsumption_resolution,[],[f17458,f8619]) ).
fof(f17476,plain,
( ! [X0] :
( r1_tarski(sF215,X0)
| ~ r2_hidden(sK42(sF215,X0),sF216)
| r2_hidden(sK42(sF215,X0),sF218) )
| ~ spl222_75
| ~ spl222_76
| ~ spl222_80
| ~ spl222_82
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_89
| ~ spl222_93
| ~ spl222_95
| spl222_97
| ~ spl222_107
| ~ spl222_195 ),
inference(resolution,[],[f17462,f8493]) ).
fof(f17482,plain,
( ! [X0] :
( r2_hidden(sK42(sF215,X0),sF218)
| r1_tarski(sF215,X0) )
| ~ spl222_74
| ~ spl222_75
| ~ spl222_76
| ~ spl222_80
| ~ spl222_81
| ~ spl222_82
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_89
| ~ spl222_93
| ~ spl222_94
| ~ spl222_95
| spl222_97
| ~ spl222_107
| ~ spl222_194
| ~ spl222_195 ),
inference(forward_subsumption_resolution,[],[f17476,f17346]) ).
fof(f17489,plain,
( r1_tarski(sF215,sF218)
| r1_tarski(sF215,sF218)
| ~ spl222_74
| ~ spl222_75
| ~ spl222_76
| ~ spl222_80
| ~ spl222_81
| ~ spl222_82
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_89
| ~ spl222_93
| ~ spl222_94
| ~ spl222_95
| spl222_97
| ~ spl222_107
| ~ spl222_194
| ~ spl222_195 ),
inference(resolution,[],[f17482,f5928]) ).
fof(f17494,plain,
( r1_tarski(sF215,sF218)
| ~ spl222_74
| ~ spl222_75
| ~ spl222_76
| ~ spl222_80
| ~ spl222_81
| ~ spl222_82
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_89
| ~ spl222_93
| ~ spl222_94
| ~ spl222_95
| spl222_97
| ~ spl222_107
| ~ spl222_194
| ~ spl222_195 ),
inference(duplicate_literal_removal,[],[f17489]) ).
fof(f17496,plain,
( spl222_682
| ~ spl222_74
| ~ spl222_75
| ~ spl222_76
| ~ spl222_80
| ~ spl222_81
| ~ spl222_82
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_89
| ~ spl222_93
| ~ spl222_94
| ~ spl222_95
| spl222_97
| ~ spl222_107
| ~ spl222_194
| ~ spl222_195 ),
inference(avatar_split_clause,[],[f17494,f9037,f9033,f7976,f7837,f7775,f7755,f7732,f7685,f7671,f7666,f7661,f7651,f7646,f7641,f7621,f7616,f7611,f17243]) ).
fof(f17571,plain,
( ! [X0] :
( r2_hidden(sK42(sF218,X0),sF216)
| r1_tarski(sF218,X0) )
| ~ spl222_93 ),
inference(resolution,[],[f14974,f5927]) ).
fof(f19785,plain,
( ! [X2,X3,X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF219))
| r2_hidden(sK27(X1,X2,X0),X1)
| ~ m1_subset_1(X2,sK9)
| ~ m1_subset_1(X1,k1_zfmisc_1(sK8))
| v1_xboole_0(sK9)
| ~ r2_hidden(X3,X1)
| r2_hidden(X2,k9_relat_1(X0,k1_tarski(X3))) )
| ~ spl222_84 ),
inference(superposition,[],[f7903,f7663]) ).
fof(f19791,plain,
( ! [X2,X3,X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF219))
| r2_hidden(sK27(X1,X2,X0),X1)
| ~ m1_subset_1(X2,sK9)
| ~ m1_subset_1(X1,k1_zfmisc_1(sK8))
| ~ r2_hidden(X3,X1)
| r2_hidden(X2,k9_relat_1(X0,k1_tarski(X3))) )
| ~ spl222_84
| spl222_97 ),
inference(forward_subsumption_resolution,[],[f19785,f7838]) ).
fof(f19792,plain,
( ! [X2,X3,X0,X1] :
( ~ m1_subset_1(X0,sF220)
| r2_hidden(sK27(X1,X2,X0),X1)
| ~ m1_subset_1(X2,sK9)
| ~ m1_subset_1(X1,k1_zfmisc_1(sK8))
| ~ r2_hidden(X3,X1)
| r2_hidden(X2,k9_relat_1(X0,k1_tarski(X3))) )
| ~ spl222_84
| ~ spl222_85
| spl222_97 ),
inference(forward_demodulation,[],[f19791,f7668]) ).
fof(f19793,plain,
( ! [X2,X3,X0,X1] :
( r2_hidden(sK27(X1,X2,X0),X1)
| ~ m1_subset_1(X0,sF220)
| ~ m1_subset_1(X1,sF221)
| ~ m1_subset_1(X2,sK9)
| ~ r2_hidden(X3,X1)
| r2_hidden(X2,k9_relat_1(X0,k1_tarski(X3))) )
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| spl222_97 ),
inference(forward_demodulation,[],[f19792,f7673]) ).
fof(f25750,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF214)
| r2_hidden(X0,sK11)
| r2_hidden(X0,sK10) )
| ~ spl222_94 ),
inference(superposition,[],[f7096,f7757]) ).
fof(f25769,plain,
( ! [X2,X0,X1] :
( r2_hidden(sK27(sF214,X0,X1),sK11)
| r2_hidden(sK27(sF214,X0,X1),sK10)
| ~ m1_subset_1(X1,sF220)
| ~ m1_subset_1(sF214,sF221)
| ~ m1_subset_1(X0,sK9)
| ~ r2_hidden(X2,sF214)
| r2_hidden(X0,k9_relat_1(X1,k1_tarski(X2))) )
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_94
| spl222_97 ),
inference(resolution,[],[f25750,f19793]) ).
fof(f25820,plain,
( ! [X2,X0,X1] :
( r2_hidden(sK27(sF214,X0,X1),sK11)
| r2_hidden(sK27(sF214,X0,X1),sK10)
| ~ m1_subset_1(X1,sF220)
| ~ m1_subset_1(X0,sK9)
| ~ r2_hidden(X2,sF214)
| r2_hidden(X0,k9_relat_1(X1,k1_tarski(X2))) )
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_94
| ~ spl222_95
| spl222_97 ),
inference(forward_subsumption_resolution,[],[f25769,f7777]) ).
fof(f39375,plain,
( ! [X0,X1] :
( r2_hidden(sK27(sF214,X0,sK12),sK10)
| ~ m1_subset_1(sK12,sF220)
| ~ m1_subset_1(X0,sK9)
| ~ r2_hidden(X1,sF214)
| r2_hidden(X0,k9_relat_1(sK12,k1_tarski(X1)))
| ~ r2_hidden(X0,sF217)
| r2_hidden(X0,sF215) )
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_90
| ~ spl222_94
| ~ spl222_95
| spl222_97
| ~ spl222_99 ),
inference(resolution,[],[f25820,f8972]) ).
fof(f39414,plain,
( ! [X0,X1] :
( r2_hidden(sK27(sF214,X0,sK12),sK10)
| ~ m1_subset_1(sK12,sF220)
| ~ m1_subset_1(X0,sK9)
| ~ r2_hidden(X1,sF214)
| r2_hidden(X0,k9_relat_1(sK12,k1_tarski(X1)))
| ~ r2_hidden(X0,sF217) )
| ~ spl222_76
| ~ spl222_80
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_90
| ~ spl222_94
| ~ spl222_95
| spl222_97
| ~ spl222_99 ),
inference(forward_subsumption_resolution,[],[f39375,f7817]) ).
fof(f39439,plain,
( ! [X0,X1] :
( r2_hidden(sK27(sF214,X0,sK12),sK10)
| ~ m1_subset_1(sK12,sF220)
| ~ r2_hidden(X1,sF214)
| r2_hidden(X0,k9_relat_1(sK12,k1_tarski(X1)))
| ~ r2_hidden(X0,sF217) )
| ~ spl222_76
| ~ spl222_80
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_90
| ~ spl222_94
| ~ spl222_95
| spl222_97
| ~ spl222_99 ),
inference(forward_subsumption_resolution,[],[f39414,f7985]) ).
fof(f39442,plain,
( ! [X0,X1] :
( r2_hidden(sK27(sF214,X0,sK12),sK10)
| ~ r2_hidden(X1,sF214)
| r2_hidden(X0,k9_relat_1(sK12,k1_tarski(X1)))
| ~ r2_hidden(X0,sF217) )
| ~ spl222_76
| ~ spl222_80
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_90
| ~ spl222_94
| ~ spl222_95
| spl222_97
| ~ spl222_99 ),
inference(forward_subsumption_resolution,[],[f39439,f7623]) ).
fof(f39446,plain,
( ! [X0,X1] :
( ~ r2_hidden(X0,sF214)
| r2_hidden(X1,k9_relat_1(sK12,k1_tarski(X0)))
| ~ r2_hidden(X1,sF217)
| ~ r2_hidden(X1,sF216)
| r2_hidden(X1,sF215) )
| ~ spl222_76
| ~ spl222_80
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_90
| ~ spl222_94
| ~ spl222_95
| spl222_97
| ~ spl222_99
| ~ spl222_198 ),
inference(resolution,[],[f39442,f9050]) ).
fof(f39476,plain,
( ! [X0,X1] :
( r2_hidden(X1,k9_relat_1(sK12,k1_tarski(X0)))
| ~ r2_hidden(X0,sF214)
| ~ r2_hidden(X1,sF217)
| ~ r2_hidden(X1,sF216) )
| ~ spl222_76
| ~ spl222_80
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_90
| ~ spl222_94
| ~ spl222_95
| spl222_97
| ~ spl222_99
| ~ spl222_198 ),
inference(forward_subsumption_resolution,[],[f39446,f7817]) ).
fof(f39484,plain,
( ! [X2,X3,X0,X1] :
( r2_hidden(X1,k8_relset_2(X2,X3,X0,sK12))
| ~ r2_hidden(X1,sF217)
| ~ r2_hidden(X1,sF216)
| ~ r2_hidden(sK27(X0,X1,sK12),sF214)
| ~ m1_subset_1(sK12,k1_zfmisc_1(k2_zfmisc_1(X2,X3)))
| ~ m1_subset_1(X1,X3)
| ~ m1_subset_1(X0,k1_zfmisc_1(X2))
| v1_xboole_0(X3) )
| ~ spl222_76
| ~ spl222_80
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_90
| ~ spl222_94
| ~ spl222_95
| spl222_97
| ~ spl222_99
| ~ spl222_198 ),
inference(resolution,[],[f39476,f5849]) ).
fof(f39569,plain,
( ! [X2,X3,X0,X1] :
( ~ r2_hidden(sK27(X3,sK42(X0,k8_relset_2(X1,X2,X3,sK12)),sK12),sF214)
| ~ r2_hidden(sK42(X0,k8_relset_2(X1,X2,X3,sK12)),sF216)
| ~ r2_hidden(sK42(X0,k8_relset_2(X1,X2,X3,sK12)),sF217)
| ~ m1_subset_1(sK12,k1_zfmisc_1(k2_zfmisc_1(X1,X2)))
| ~ m1_subset_1(sK42(X0,k8_relset_2(X1,X2,X3,sK12)),X2)
| ~ m1_subset_1(X3,k1_zfmisc_1(X1))
| v1_xboole_0(X2)
| r1_tarski(X0,k8_relset_2(X1,X2,X3,sK12)) )
| ~ spl222_76
| ~ spl222_80
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_90
| ~ spl222_94
| ~ spl222_95
| spl222_97
| ~ spl222_99
| ~ spl222_198 ),
inference(resolution,[],[f39484,f5928]) ).
fof(f46929,plain,
( ! [X0] :
( ~ r2_hidden(sK27(sF214,sK42(X0,sF215),sK12),sF214)
| ~ r2_hidden(sK42(X0,sF215),sF216)
| ~ r2_hidden(sK42(X0,sF215),sF217)
| ~ m1_subset_1(sK12,k1_zfmisc_1(k2_zfmisc_1(sK8,sK9)))
| ~ m1_subset_1(sK42(X0,sF215),sK9)
| ~ m1_subset_1(sF214,k1_zfmisc_1(sK8))
| v1_xboole_0(sK9)
| r1_tarski(X0,sF215) )
| ~ spl222_76
| ~ spl222_80
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_90
| ~ spl222_94
| ~ spl222_95
| spl222_97
| ~ spl222_99
| ~ spl222_198 ),
inference(superposition,[],[f39569,f7643]) ).
fof(f46960,plain,
( ! [X0] :
( ~ r2_hidden(sK27(sF214,sK42(X0,sF215),sK12),sF214)
| ~ r2_hidden(sK42(X0,sF215),sF216)
| ~ r2_hidden(sK42(X0,sF215),sF217)
| ~ m1_subset_1(sK12,k1_zfmisc_1(k2_zfmisc_1(sK8,sK9)))
| ~ m1_subset_1(sF214,k1_zfmisc_1(sK8))
| v1_xboole_0(sK9)
| r1_tarski(X0,sF215) )
| ~ spl222_76
| ~ spl222_80
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_90
| ~ spl222_94
| ~ spl222_95
| spl222_97
| ~ spl222_99
| ~ spl222_198 ),
inference(forward_subsumption_resolution,[],[f46929,f7985]) ).
fof(f46965,plain,
( ! [X0] :
( ~ r2_hidden(sK27(sF214,sK42(X0,sF215),sK12),sF214)
| ~ r2_hidden(sK42(X0,sF215),sF216)
| ~ r2_hidden(sK42(X0,sF215),sF217)
| ~ m1_subset_1(sK12,k1_zfmisc_1(k2_zfmisc_1(sK8,sK9)))
| ~ m1_subset_1(sF214,k1_zfmisc_1(sK8))
| r1_tarski(X0,sF215) )
| ~ spl222_76
| ~ spl222_80
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_90
| ~ spl222_94
| ~ spl222_95
| spl222_97
| ~ spl222_99
| ~ spl222_198 ),
inference(forward_subsumption_resolution,[],[f46960,f7838]) ).
fof(f59135,plain,
( ! [X0] :
( ~ m1_subset_1(sK12,k1_zfmisc_1(sF219))
| ~ r2_hidden(sK27(sF214,sK42(X0,sF215),sK12),sF214)
| ~ r2_hidden(sK42(X0,sF215),sF216)
| ~ r2_hidden(sK42(X0,sF215),sF217)
| ~ m1_subset_1(sF214,k1_zfmisc_1(sK8))
| r1_tarski(X0,sF215) )
| ~ spl222_76
| ~ spl222_80
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_90
| ~ spl222_94
| ~ spl222_95
| spl222_97
| ~ spl222_99
| ~ spl222_198 ),
inference(forward_demodulation,[],[f46965,f7663]) ).
fof(f59460,plain,
( ! [X0] :
( ~ m1_subset_1(sK12,sF220)
| ~ r2_hidden(sK27(sF214,sK42(X0,sF215),sK12),sF214)
| ~ r2_hidden(sK42(X0,sF215),sF216)
| ~ r2_hidden(sK42(X0,sF215),sF217)
| ~ m1_subset_1(sF214,k1_zfmisc_1(sK8))
| r1_tarski(X0,sF215) )
| ~ spl222_76
| ~ spl222_80
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_90
| ~ spl222_94
| ~ spl222_95
| spl222_97
| ~ spl222_99
| ~ spl222_198 ),
inference(forward_demodulation,[],[f59135,f7668]) ).
fof(f59571,plain,
( ! [X0] :
( ~ r2_hidden(sK27(sF214,sK42(X0,sF215),sK12),sF214)
| ~ r2_hidden(sK42(X0,sF215),sF216)
| ~ r2_hidden(sK42(X0,sF215),sF217)
| ~ m1_subset_1(sF214,k1_zfmisc_1(sK8))
| r1_tarski(X0,sF215) )
| ~ spl222_76
| ~ spl222_80
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_90
| ~ spl222_94
| ~ spl222_95
| spl222_97
| ~ spl222_99
| ~ spl222_198 ),
inference(forward_subsumption_resolution,[],[f59460,f7623]) ).
fof(f59653,plain,
( ! [X0] :
( ~ m1_subset_1(sF214,sF221)
| ~ r2_hidden(sK27(sF214,sK42(X0,sF215),sK12),sF214)
| ~ r2_hidden(sK42(X0,sF215),sF216)
| ~ r2_hidden(sK42(X0,sF215),sF217)
| r1_tarski(X0,sF215) )
| ~ spl222_76
| ~ spl222_80
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_90
| ~ spl222_94
| ~ spl222_95
| spl222_97
| ~ spl222_99
| ~ spl222_198 ),
inference(forward_demodulation,[],[f59571,f7673]) ).
fof(f59732,plain,
( ! [X0] :
( ~ r2_hidden(sK27(sF214,sK42(X0,sF215),sK12),sF214)
| ~ r2_hidden(sK42(X0,sF215),sF216)
| ~ r2_hidden(sK42(X0,sF215),sF217)
| r1_tarski(X0,sF215) )
| ~ spl222_76
| ~ spl222_80
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_90
| ~ spl222_94
| ~ spl222_95
| spl222_97
| ~ spl222_99
| ~ spl222_198 ),
inference(forward_subsumption_resolution,[],[f59653,f7777]) ).
fof(f60022,plain,
( ! [X0] :
( ~ r2_hidden(sK42(X0,sF215),sF216)
| ~ r2_hidden(sK42(X0,sF215),sF217)
| r1_tarski(X0,sF215)
| ~ m1_subset_1(sK42(X0,sF215),sK9)
| r1_tarski(X0,sF215) )
| ~ spl222_76
| ~ spl222_80
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_90
| ~ spl222_94
| ~ spl222_95
| spl222_97
| ~ spl222_99
| ~ spl222_198 ),
inference(resolution,[],[f59732,f13379]) ).
fof(f60025,plain,
( ! [X0] :
( ~ r2_hidden(sK42(X0,sF215),sF216)
| ~ r2_hidden(sK42(X0,sF215),sF217)
| r1_tarski(X0,sF215)
| ~ m1_subset_1(sK42(X0,sF215),sK9) )
| ~ spl222_76
| ~ spl222_80
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_90
| ~ spl222_94
| ~ spl222_95
| spl222_97
| ~ spl222_99
| ~ spl222_198 ),
inference(duplicate_literal_removal,[],[f60022]) ).
fof(f60027,plain,
( ! [X0] :
( ~ r2_hidden(sK42(X0,sF215),sF217)
| ~ r2_hidden(sK42(X0,sF215),sF216)
| r1_tarski(X0,sF215) )
| ~ spl222_76
| ~ spl222_80
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_90
| ~ spl222_94
| ~ spl222_95
| spl222_97
| ~ spl222_99
| ~ spl222_198 ),
inference(forward_subsumption_resolution,[],[f60025,f7985]) ).
fof(f60028,plain,
( ~ r2_hidden(sK42(sF218,sF215),sF216)
| r1_tarski(sF218,sF215)
| r1_tarski(sF218,sF215)
| ~ spl222_76
| ~ spl222_80
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_90
| ~ spl222_93
| ~ spl222_94
| ~ spl222_95
| spl222_97
| ~ spl222_99
| ~ spl222_198 ),
inference(resolution,[],[f60027,f16767]) ).
fof(f60037,plain,
( ~ r2_hidden(sK42(sF218,sF215),sF216)
| r1_tarski(sF218,sF215)
| ~ spl222_76
| ~ spl222_80
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_90
| ~ spl222_93
| ~ spl222_94
| ~ spl222_95
| spl222_97
| ~ spl222_99
| ~ spl222_198 ),
inference(duplicate_literal_removal,[],[f60028]) ).
fof(f60039,plain,
( r1_tarski(sF218,sF215)
| ~ spl222_76
| ~ spl222_80
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_90
| ~ spl222_93
| ~ spl222_94
| ~ spl222_95
| spl222_97
| ~ spl222_99
| ~ spl222_198 ),
inference(forward_subsumption_resolution,[],[f60037,f17571]) ).
fof(f60356,plain,
( spl222_683
| ~ spl222_76
| ~ spl222_80
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_90
| ~ spl222_93
| ~ spl222_94
| ~ spl222_95
| spl222_97
| ~ spl222_99
| ~ spl222_198 ),
inference(avatar_split_clause,[],[f60039,f9049,f7845,f7837,f7775,f7755,f7732,f7695,f7671,f7666,f7661,f7641,f7621,f17248]) ).
cnf(s77,plain,
spl222_74,
inference(sat_conversion,[],[f7614]) ).
cnf(s78,plain,
spl222_75,
inference(sat_conversion,[],[f7619]) ).
cnf(s79,plain,
spl222_76,
inference(sat_conversion,[],[f7624]) ).
cnf(s80,plain,
~ spl222_77,
inference(sat_conversion,[],[f7629]) ).
cnf(s82,plain,
spl222_79,
inference(sat_conversion,[],[f7639]) ).
cnf(s83,plain,
spl222_80,
inference(sat_conversion,[],[f7644]) ).
cnf(s84,plain,
spl222_81,
inference(sat_conversion,[],[f7649]) ).
cnf(s85,plain,
spl222_82,
inference(sat_conversion,[],[f7654]) ).
cnf(s86,plain,
spl222_83,
inference(sat_conversion,[],[f7659]) ).
cnf(s87,plain,
spl222_84,
inference(sat_conversion,[],[f7664]) ).
cnf(s88,plain,
spl222_85,
inference(sat_conversion,[],[f7669]) ).
cnf(s89,plain,
spl222_86,
inference(sat_conversion,[],[f7674]) ).
cnf(s90,plain,
( ~ spl222_80
| ~ spl222_87
| ~ spl222_88
| spl222_89 ),
inference(sat_conversion,[],[f7688]) ).
cnf(s91,plain,
( ~ spl222_76
| ~ spl222_84
| ~ spl222_85
| spl222_87 ),
inference(sat_conversion,[],[f7689]) ).
cnf(s92,plain,
( ~ spl222_75
| ~ spl222_82
| ~ spl222_86
| ~ spl222_87
| spl222_90 ),
inference(sat_conversion,[],[f7698]) ).
cnf(s93,plain,
( ~ spl222_74
| ~ spl222_81
| ~ spl222_86
| ~ spl222_87
| spl222_91 ),
inference(sat_conversion,[],[f7706]) ).
cnf(s95,plain,
( ~ spl222_83
| ~ spl222_90
| ~ spl222_91
| spl222_93 ),
inference(sat_conversion,[],[f7735]) ).
cnf(s97,plain,
( ~ spl222_74
| ~ spl222_75
| ~ spl222_79
| ~ spl222_86
| spl222_94 ),
inference(sat_conversion,[],[f7758]) ).
cnf(s99,plain,
( ~ spl222_74
| ~ spl222_75
| ~ spl222_79
| ~ spl222_86
| spl222_95 ),
inference(sat_conversion,[],[f7778]) ).
cnf(s100,plain,
( ~ spl222_86
| spl222_88
| ~ spl222_95 ),
inference(sat_conversion,[],[f7779]) ).
cnf(s102,plain,
( ~ spl222_83
| ~ spl222_90
| ~ spl222_91
| spl222_96 ),
inference(sat_conversion,[],[f7798]) ).
cnf(s104,plain,
( ~ spl222_75
| ~ spl222_76
| ~ spl222_80
| ~ spl222_82
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_95
| spl222_97
| spl222_99 ),
inference(sat_conversion,[],[f7847]) ).
cnf(s112,plain,
( ~ spl222_74
| ~ spl222_75
| ~ spl222_79
| ~ spl222_86
| spl222_107 ),
inference(sat_conversion,[],[f7979]) ).
cnf(s182,plain,
( ~ spl222_74
| ~ spl222_76
| ~ spl222_81
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| spl222_97
| spl222_194 ),
inference(sat_conversion,[],[f9035]) ).
cnf(s183,plain,
( ~ spl222_75
| ~ spl222_76
| ~ spl222_82
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| spl222_97
| spl222_195 ),
inference(sat_conversion,[],[f9039]) ).
cnf(s186,plain,
( ~ spl222_74
| ~ spl222_76
| ~ spl222_80
| ~ spl222_81
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_91
| ~ spl222_95
| spl222_97
| spl222_198 ),
inference(sat_conversion,[],[f9051]) ).
cnf(s189,plain,
( ~ spl222_96
| ~ spl222_97
| spl222_190 ),
inference(sat_conversion,[],[f9060]) ).
cnf(s192,plain,
( ~ spl222_89
| ~ spl222_97
| spl222_193 ),
inference(sat_conversion,[],[f9063]) ).
cnf(s442,plain,
( spl222_77
| ~ spl222_190
| ~ spl222_193 ),
inference(sat_conversion,[],[f11226]) ).
cnf(s1109,plain,
( spl222_77
| ~ spl222_682
| ~ spl222_683 ),
inference(sat_conversion,[],[f17417]) ).
cnf(s1127,plain,
( ~ spl222_74
| ~ spl222_75
| ~ spl222_76
| ~ spl222_80
| ~ spl222_81
| ~ spl222_82
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_89
| ~ spl222_93
| ~ spl222_94
| ~ spl222_95
| spl222_97
| ~ spl222_107
| ~ spl222_194
| ~ spl222_195
| spl222_682 ),
inference(sat_conversion,[],[f17496]) ).
cnf(s3649,plain,
( ~ spl222_76
| ~ spl222_80
| ~ spl222_84
| ~ spl222_85
| ~ spl222_86
| ~ spl222_90
| ~ spl222_93
| ~ spl222_94
| ~ spl222_95
| spl222_97
| ~ spl222_99
| ~ spl222_198
| spl222_683 ),
inference(sat_conversion,[],[f60356]) ).
cnf(s3744,plain,
spl222_87,
inference(rat,[],[s91,s87,s88,s79]) ).
cnf(s3752,plain,
spl222_90,
inference(rat,[],[s92,s3744,s85,s89,s78]) ).
cnf(s3768,plain,
spl222_107,
inference(rat,[],[s112,s78,s89,s82,s77]) ).
cnf(s3769,plain,
spl222_95,
inference(rat,[],[s99,s78,s89,s82,s77]) ).
cnf(s3770,plain,
spl222_94,
inference(rat,[],[s97,s78,s89,s82,s77]) ).
cnf(s3771,plain,
spl222_91,
inference(rat,[],[s93,s3744,s84,s89,s77]) ).
cnf(s3781,plain,
spl222_88,
inference(rat,[],[s100,s89,s3769]) ).
cnf(s3801,plain,
spl222_96,
inference(rat,[],[s102,s3752,s86,s3771]) ).
cnf(s3802,plain,
spl222_93,
inference(rat,[],[s95,s3752,s86,s3771]) ).
cnf(s3804,plain,
spl222_89,
inference(rat,[],[s90,s3744,s83,s3781]) ).
cnf(s3826,plain,
spl222_97,
inference(rat,[],[s1109,s3649,s1127,s186,s104,s182,s183,s80,s87,s88,s89,s83,s79,s3752,s3769,s3770,s3802,s84,s85,s78,s77,s3768,s3804,s3771]) ).
cnf(s3827,plain,
spl222_193,
inference(rat,[],[s192,s3804,s3826]) ).
cnf(s3830,plain,
spl222_190,
inference(rat,[],[s189,s3801,s3826]) ).
cnf(s3836,plain,
$false,
inference(rat,[],[s442,s80,s3827,s3830]) ).
fof(f60362,plain,
$false,
inference(avatar_sat_refutation,[],[s3836]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU428+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.39 % Computer : n020.cluster.edu
% 0.10/0.39 % Model : x86_64 x86_64
% 0.10/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.39 % Memory : 8046.5625MB
% 0.10/0.39 % OS : Linux 6.8.0-71-generic
% 0.10/0.39 % CPULimit : 300
% 0.10/0.39 % WCLimit : 300
% 0.10/0.39 % DateTime : Mon Sep 28 05:23:50 UTC 2026
% 0.10/0.39 % CPUTime :
% 0.10/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.42 Running first-order theorem proving
% 0.10/0.42 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
% 10.40/2.19 % (4055785)Detected formulas, will run a generic FOF schedule.
% 10.40/2.19 % (4055790)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=3553084089:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 10.40/2.19 % (4055791)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=848870794:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 10.40/2.19 % (4055796)dis-21_1_sil=8000:lcm=predicate:random_seed=4290346137:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 10.40/2.19 % (4055792)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=3442828184:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 10.40/2.19 % (4055793)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3003390547:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 10.40/2.19 % (4055794)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3090134932:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 10.40/2.19 % (4055795)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3753150218:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 10.40/2.19 % (4055794)Instruction limit reached!
% 10.40/2.19 % (4055794)------------------------------
% 10.40/2.19 % (4055794)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.40/2.19 % (4055794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.40/2.19 % (4055794)CaDiCaL version: 2.1.3
% 10.40/2.19 % (4055794)Termination reason: Instruction limit
% 10.40/2.19 % (4055794)Termination phase: Saturation
% 10.40/2.19 % (4055794)Time elapsed: 0.069 s
% 10.40/2.19 % (4055794)Peak memory usage: 94 MB
% 10.40/2.19 % (4055794)Instructions burned: 120 (million)
% 10.40/2.19 % (4055793)Instruction limit reached!
% 10.40/2.19 % (4055793)------------------------------
% 10.40/2.19 % (4055793)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.40/2.19 % (4055793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.40/2.19 % (4055793)CaDiCaL version: 2.1.3
% 10.40/2.19 % (4055793)Termination reason: Instruction limit
% 10.40/2.19 % (4055793)Termination phase: Saturation
% 10.40/2.19 % (4055793)Time elapsed: 0.071 s
% 10.40/2.19 % (4055793)Peak memory usage: 94 MB
% 10.40/2.19 % (4055793)Instructions burned: 110 (million)
% 10.40/2.19 % (4055796)Instruction limit reached!
% 10.40/2.19 % (4055796)------------------------------
% 10.40/2.19 % (4055796)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.40/2.19 % (4055796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.40/2.19 % (4055796)CaDiCaL version: 2.1.3
% 10.40/2.19 % (4055796)Termination reason: Instruction limit
% 10.40/2.19 % (4055796)Termination phase: Clausification
% 10.40/2.19 % (4055796)Time elapsed: 0.088 s
% 10.40/2.19 % (4055796)Peak memory usage: 94 MB
% 10.40/2.19 % (4055796)Instructions burned: 129 (million)
% 10.40/2.19 % (4055795)Instruction limit reached!
% 10.40/2.19 % (4055795)------------------------------
% 10.40/2.19 % (4055795)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.40/2.19 % (4055795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.40/2.19 % (4055795)CaDiCaL version: 2.1.3
% 10.40/2.19 % (4055795)Termination reason: Instruction limit
% 10.40/2.19 % (4055795)Termination phase: Preprocessing 3
% 10.40/2.19 % (4055795)Time elapsed: 0.086 s
% 10.40/2.19 % (4055795)Peak memory usage: 94 MB
% 10.40/2.19 % (4055795)Instructions burned: 139 (million)
% 10.40/2.19 % (4055804)lrs+10_1_sil=8000:sp=occurrence:random_seed=2755990269:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 10.40/2.19 % (4055805)lrs+10_1_sil=32000:urr=on:br=off:random_seed=929609120:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 10.40/2.19 % (4055807)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=2878277568:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi)
% 10.40/2.19 % (4055806)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3080618374:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 10.40/2.19 % (4055805)Instruction limit reached!
% 14.40/2.89 % (4055805)------------------------------
% 14.40/2.89 % (4055805)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.40/2.89 % (4055805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.40/2.89 % (4055805)CaDiCaL version: 2.1.3
% 14.40/2.89 % (4055805)Termination reason: Instruction limit
% 14.40/2.89 % (4055805)Termination phase: Saturation
% 14.40/2.89 % (4055805)Time elapsed: 0.084 s
% 14.40/2.89 % (4055805)Peak memory usage: 94 MB
% 14.40/2.89 % (4055805)Instructions burned: 159 (million)
% 14.40/2.89 % (4055807)Instruction limit reached!
% 14.40/2.89 % (4055807)------------------------------
% 14.40/2.89 % (4055807)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.40/2.89 % (4055807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.40/2.89 % (4055807)CaDiCaL version: 2.1.3
% 14.40/2.89 % (4055807)Termination reason: Instruction limit
% 14.40/2.89 % (4055807)Termination phase: Property scanning
% 14.40/2.89 % (4055807)Time elapsed: 0.078 s
% 14.40/2.89 % (4055807)Peak memory usage: 99 MB
% 14.40/2.89 % (4055807)Instructions burned: 252 (million)
% 14.40/2.89 % (4055812)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=4015213305:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 14.40/2.89 % (4055804)Instruction limit reached!
% 14.40/2.89 % (4055804)------------------------------
% 14.40/2.89 % (4055804)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.40/2.89 % (4055804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.40/2.89 % (4055804)CaDiCaL version: 2.1.3
% 14.40/2.89 % (4055804)Termination reason: Instruction limit
% 14.40/2.89 % (4055804)Termination phase: Saturation
% 14.40/2.89 % (4055804)Time elapsed: 0.191 s
% 14.40/2.89 % (4055804)Peak memory usage: 98 MB
% 14.40/2.89 % (4055804)Instructions burned: 285 (million)
% 14.40/2.89 % (4055813)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=425157430:i=2350_2995 on theBenchmark for (2995ds/2350Mi)
% 14.40/2.89 % (4055806)Instruction limit reached!
% 14.40/2.89 % (4055806)------------------------------
% 14.40/2.89 % (4055806)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.40/2.89 % (4055806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.40/2.89 % (4055806)CaDiCaL version: 2.1.3
% 14.40/2.89 % (4055806)Termination reason: Instruction limit
% 14.40/2.89 % (4055806)Termination phase: Saturation
% 14.40/2.89 % (4055806)Time elapsed: 0.223 s
% 14.40/2.89 % (4055806)Peak memory usage: 96 MB
% 14.40/2.89 % (4055806)Instructions burned: 325 (million)
% 14.40/2.89 % (4055812)Instruction limit reached!
% 14.40/2.89 % (4055812)------------------------------
% 14.40/2.89 % (4055812)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.40/2.89 % (4055812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.40/2.89 % (4055812)CaDiCaL version: 2.1.3
% 14.40/2.89 % (4055812)Termination reason: Instruction limit
% 14.40/2.89 % (4055812)Termination phase: Saturation
% 14.40/2.89 % (4055812)Time elapsed: 0.096 s
% 14.40/2.89 % (4055812)Peak memory usage: 97 MB
% 14.40/2.89 % (4055812)Instructions burned: 297 (million)
% 14.40/2.89 % (4055815)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1552019193:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 14.40/2.89 % (4055818)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=124710683:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2993 on theBenchmark for (2993ds/114Mi)
% 14.40/2.89 % (4055817)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2065279025:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi)
% 14.40/2.89 % (4055818)Instruction limit reached!
% 14.40/2.89 % (4055818)------------------------------
% 14.40/2.89 % (4055818)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.40/2.89 % (4055818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.40/2.89 % (4055818)CaDiCaL version: 2.1.3
% 14.40/2.89 % (4055818)Termination reason: Instruction limit
% 14.40/2.89 % (4055818)Termination phase: SInE selection
% 14.40/2.89 % (4055818)Time elapsed: 0.029 s
% 14.40/2.89 % (4055818)Peak memory usage: 89 MB
% 14.40/2.89 % (4055818)Instructions burned: 115 (million)
% 14.40/2.89 % (4055815)Instruction limit reached!
% 14.40/2.89 % (4055815)------------------------------
% 14.40/2.89 % (4055815)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.16/7.36 % (4055815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.16/7.36 % (4055815)CaDiCaL version: 2.1.3
% 47.16/7.36 % (4055815)Termination reason: Instruction limit
% 47.16/7.36 % (4055815)Termination phase: Saturation
% 47.16/7.36 % (4055815)Time elapsed: 0.071 s
% 47.16/7.36 % (4055815)Peak memory usage: 95 MB
% 47.16/7.36 % (4055815)Instructions burned: 114 (million)
% 47.16/7.36 % (4055817)Instruction limit reached!
% 47.16/7.36 % (4055817)------------------------------
% 47.16/7.36 % (4055817)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.16/7.36 % (4055817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.16/7.36 % (4055817)CaDiCaL version: 2.1.3
% 47.16/7.36 % (4055817)Termination reason: Instruction limit
% 47.16/7.36 % (4055817)Termination phase: Preprocessing 3
% 47.16/7.36 % (4055817)Time elapsed: 0.087 s
% 47.16/7.36 % (4055817)Peak memory usage: 97 MB
% 47.16/7.36 % (4055817)Instructions burned: 128 (million)
% 47.16/7.36 % (4055822)lrs+10_1_sil=8000:sp=occurrence:random_seed=2258892704:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2992 on theBenchmark for (2992ds/907Mi)
% 47.16/7.36 % (4055823)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2304680977:i=437:sd=1:aac=none:ss=included_2992 on theBenchmark for (2992ds/437Mi)
% 47.16/7.36 % (4055825)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2267240690:i=5202:ss=axioms:sgt=16_2991 on theBenchmark for (2991ds/5202Mi)
% 47.16/7.36 % (4055823)Instruction limit reached!
% 47.16/7.36 % (4055823)------------------------------
% 47.16/7.36 % (4055823)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.16/7.36 % (4055823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.16/7.36 % (4055823)CaDiCaL version: 2.1.3
% 47.16/7.36 % (4055823)Termination reason: Instruction limit
% 47.16/7.36 % (4055823)Termination phase: Saturation
% 47.16/7.36 % (4055823)Time elapsed: 0.277 s
% 47.16/7.36 % (4055823)Peak memory usage: 98 MB
% 47.16/7.36 % (4055823)Instructions burned: 437 (million)
% 47.16/7.36 % (4055822)Instruction limit reached!
% 47.16/7.36 % (4055822)------------------------------
% 47.16/7.36 % (4055822)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.16/7.36 % (4055822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.16/7.36 % (4055822)CaDiCaL version: 2.1.3
% 47.16/7.36 % (4055822)Termination reason: Instruction limit
% 47.16/7.36 % (4055822)Termination phase: Saturation
% 47.16/7.36 % (4055822)Time elapsed: 0.341 s
% 47.16/7.36 % (4055822)Peak memory usage: 107 MB
% 47.16/7.36 % (4055822)Instructions burned: 909 (million)
% 47.16/7.36 % (4055829)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2871512541:st=8:i=592:sd=3:ep=RST:ss=axioms_2987 on theBenchmark for (2987ds/592Mi)
% 47.16/7.36 % (4055828)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2117895034:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2987 on theBenchmark for (2987ds/134Mi)
% 47.16/7.36 % (4055828)Instruction limit reached!
% 47.16/7.36 % (4055828)------------------------------
% 47.16/7.36 % (4055828)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.16/7.36 % (4055828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.16/7.36 % (4055828)CaDiCaL version: 2.1.3
% 47.16/7.36 % (4055828)Termination reason: Instruction limit
% 47.16/7.36 % (4055828)Termination phase: Saturation
% 47.16/7.36 % (4055828)Time elapsed: 0.085 s
% 47.16/7.36 % (4055828)Peak memory usage: 96 MB
% 47.16/7.36 % (4055828)Instructions burned: 135 (million)
% 47.16/7.36 % (4055829)Instruction limit reached!
% 47.16/7.36 % (4055829)------------------------------
% 47.16/7.36 % (4055829)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.16/7.36 % (4055829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.16/7.36 % (4055829)CaDiCaL version: 2.1.3
% 47.16/7.36 % (4055829)Termination reason: Instruction limit
% 47.16/7.36 % (4055829)Termination phase: Saturation
% 47.16/7.36 % (4055829)Time elapsed: 0.184 s
% 47.16/7.36 % (4055829)Peak memory usage: 106 MB
% 47.16/7.36 % (4055829)Instructions burned: 596 (million)
% 47.16/7.36 % (4055832)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=4089115243:st=3:i=13193:sd=3:ss=axioms_2985 on theBenchmark for (2985ds/13193Mi)
% 47.16/7.36 % (4055833)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=318179651:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2985 on theBenchmark for (2985ds/125Mi)
% 70.81/10.74 % (4055833)Instruction limit reached!
% 70.81/10.74 % (4055833)------------------------------
% 70.81/10.74 % (4055833)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.81/10.74 % (4055833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.81/10.74 % (4055833)CaDiCaL version: 2.1.3
% 70.81/10.74 % (4055833)Termination reason: Instruction limit
% 70.81/10.74 % (4055833)Termination phase: Property scanning
% 70.81/10.74 % (4055833)Time elapsed: 0.043 s
% 70.81/10.74 % (4055833)Peak memory usage: 92 MB
% 70.81/10.74 % (4055833)Instructions burned: 127 (million)
% 70.81/10.74 % (4055836)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3898162971:i=134:gtgl=5:slsql=off:gtg=exists_sym_2983 on theBenchmark for (2983ds/134Mi)
% 70.81/10.74 % (4055836)Instruction limit reached!
% 70.81/10.74 % (4055836)------------------------------
% 70.81/10.74 % (4055836)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.81/10.74 % (4055836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.81/10.74 % (4055836)CaDiCaL version: 2.1.3
% 70.81/10.74 % (4055836)Termination reason: Instruction limit
% 70.81/10.74 % (4055836)Termination phase: Preprocessing 1
% 70.81/10.74 % (4055836)Time elapsed: 0.040 s
% 70.81/10.74 % (4055836)Peak memory usage: 90 MB
% 70.81/10.74 % (4055836)Instructions burned: 134 (million)
% 70.81/10.74 % (4055838)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=4123965105:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2982 on theBenchmark for (2982ds/141Mi)
% 70.81/10.74 % (4055838)Instruction limit reached!
% 70.81/10.74 % (4055838)------------------------------
% 70.81/10.74 % (4055838)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.81/10.74 % (4055838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.81/10.74 % (4055838)CaDiCaL version: 2.1.3
% 70.81/10.74 % (4055838)Termination reason: Instruction limit
% 70.81/10.74 % (4055838)Termination phase: Saturation
% 70.81/10.74 % (4055838)Time elapsed: 0.050 s
% 70.81/10.74 % (4055838)Peak memory usage: 95 MB
% 70.81/10.74 % (4055838)Instructions burned: 143 (million)
% 70.81/10.74 % (4055840)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1379699492:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2980 on theBenchmark for (2980ds/431Mi)
% 70.81/10.74 % (4055813)Instruction limit reached!
% 70.81/10.74 % (4055813)------------------------------
% 70.81/10.74 % (4055813)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.81/10.74 % (4055813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.81/10.74 % (4055813)CaDiCaL version: 2.1.3
% 70.81/10.74 % (4055813)Termination reason: Instruction limit
% 70.81/10.74 % (4055813)Termination phase: Saturation
% 70.81/10.74 % (4055813)Time elapsed: 1.501 s
% 70.81/10.74 % (4055813)Peak memory usage: 183 MB
% 70.81/10.74 % (4055813)Instructions burned: 2350 (million)
% 70.81/10.74 % (4055840)Instruction limit reached!
% 70.81/10.74 % (4055840)------------------------------
% 70.81/10.74 % (4055840)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.81/10.74 % (4055840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.81/10.74 % (4055840)CaDiCaL version: 2.1.3
% 70.81/10.74 % (4055840)Termination reason: Instruction limit
% 70.81/10.74 % (4055840)Termination phase: Saturation
% 70.81/10.74 % (4055840)Time elapsed: 0.139 s
% 70.81/10.74 % (4055840)Peak memory usage: 96 MB
% 70.81/10.74 % (4055840)Instructions burned: 435 (million)
% 70.81/10.74 % (4055843)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=1847115594:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2978 on theBenchmark for (2978ds/150Mi)
% 70.81/10.74 % (4055842)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=1384860779:i=6060:aac=none:ins=25_2978 on theBenchmark for (2978ds/6060Mi)
% 70.81/10.74 % (4055843)Instruction limit reached!
% 70.81/10.74 % (4055843)------------------------------
% 70.81/10.74 % (4055843)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.81/10.74 % (4055843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.81/10.74 % (4055843)CaDiCaL version: 2.1.3
% 70.81/10.74 % (4055843)Termination reason: Instruction limit
% 70.81/10.74 % (4055843)Termination phase: Preprocessing 3
% 105.37/15.54 % (4055843)Time elapsed: 0.059 s
% 105.37/15.54 % (4055843)Peak memory usage: 97 MB
% 105.37/15.54 % (4055843)Instructions burned: 152 (million)
% 105.37/15.54 % (4055846)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3125377187:i=14155:bd=all_2977 on theBenchmark for (2977ds/14155Mi)
% 105.37/15.54 % (4055825)Instruction limit reached!
% 105.37/15.54 % (4055825)------------------------------
% 105.37/15.54 % (4055825)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 105.37/15.54 % (4055825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 105.37/15.54 % (4055825)CaDiCaL version: 2.1.3
% 105.37/15.54 % (4055825)Termination reason: Instruction limit
% 105.37/15.54 % (4055825)Termination phase: Saturation
% 105.37/15.54 % (4055825)Time elapsed: 3.097 s
% 105.37/15.54 % (4055825)Peak memory usage: 197 MB
% 105.37/15.54 % (4055825)Instructions burned: 5203 (million)
% 105.37/15.54 % (4055848)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2070126471:i=667:av=off:fsr=off_2958 on theBenchmark for (2958ds/667Mi)
% 105.37/15.54 % (4055848)Instruction limit reached!
% 105.37/15.54 % (4055848)------------------------------
% 105.37/15.54 % (4055848)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 105.37/15.54 % (4055848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 105.37/15.54 % (4055848)CaDiCaL version: 2.1.3
% 105.37/15.54 % (4055848)Termination reason: Instruction limit
% 105.37/15.54 % (4055848)Termination phase: Saturation
% 105.37/15.54 % (4055848)Time elapsed: 0.403 s
% 105.37/15.54 % (4055848)Peak memory usage: 107 MB
% 105.37/15.54 % (4055848)Instructions burned: 668 (million)
% 105.37/15.54 % (4055850)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=2269599878:s2a=on:i=185:s2at=1.8:fdi=4_2953 on theBenchmark for (2953ds/185Mi)
% 105.37/15.54 % (4055850)Instruction limit reached!
% 105.37/15.54 % (4055850)------------------------------
% 105.37/15.54 % (4055850)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 105.37/15.54 % (4055850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 105.37/15.54 % (4055850)CaDiCaL version: 2.1.3
% 105.37/15.54 % (4055850)Termination reason: Instruction limit
% 105.37/15.54 % (4055850)Termination phase: NewCNF
% 105.37/15.54 % (4055850)Time elapsed: 0.131 s
% 105.37/15.54 % (4055850)Peak memory usage: 98 MB
% 105.37/15.54 % (4055850)Instructions burned: 186 (million)
% 105.37/15.54 % (4055852)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=621707672:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2950 on theBenchmark for (2950ds/193Mi)
% 105.37/15.54 % (4055852)Instruction limit reached!
% 105.37/15.54 % (4055852)------------------------------
% 105.37/15.54 % (4055852)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 105.37/15.54 % (4055852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 105.37/15.54 % (4055852)CaDiCaL version: 2.1.3
% 105.37/15.54 % (4055852)Termination reason: Instruction limit
% 105.37/15.54 % (4055852)Termination phase: Saturation
% 105.37/15.54 % (4055852)Time elapsed: 0.120 s
% 105.37/15.54 % (4055852)Peak memory usage: 98 MB
% 105.37/15.54 % (4055852)Instructions burned: 195 (million)
% 105.37/15.54 % (4055854)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=453062169:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2948 on theBenchmark for (2948ds/4850Mi)
% 105.37/15.54 % (4055842)Instruction limit reached!
% 105.37/15.54 % (4055842)------------------------------
% 105.37/15.54 % (4055842)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 105.37/15.54 % (4055842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 105.37/15.54 % (4055842)CaDiCaL version: 2.1.3
% 105.37/15.54 % (4055842)Termination reason: Instruction limit
% 105.37/15.54 % (4055842)Termination phase: Saturation
% 105.37/15.54 % (4055842)Time elapsed: 3.700 s
% 105.37/15.54 % (4055842)Peak memory usage: 245 MB
% 105.37/15.54 % (4055842)Instructions burned: 6148 (million)
% 105.37/15.54 % (4055856)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=1867259568:i=12111:sd=1:ss=included_2940 on theBenchmark for (2940ds/12111Mi)
% 105.37/15.54 % (4055846)Instruction limit reached!
% 105.37/15.54 % (4055846)------------------------------
% 105.37/15.54 % (4055846)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 105.37/15.54 % (4055846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 131.50/19.21 % (4055846)CaDiCaL version: 2.1.3
% 131.50/19.21 % (4055846)Termination reason: Instruction limit
% 131.50/19.21 % (4055846)Termination phase: Saturation
% 131.50/19.21 % (4055846)Time elapsed: 4.373 s
% 131.50/19.21 % (4055846)Peak memory usage: 277 MB
% 131.50/19.21 % (4055846)Instructions burned: 14156 (million)
% 131.50/19.21 % (4055858)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1270588540:i=319:kws=precedence:fsr=off_2932 on theBenchmark for (2932ds/319Mi)
% 131.50/19.21 % (4055858)Instruction limit reached!
% 131.50/19.21 % (4055858)------------------------------
% 131.50/19.21 % (4055858)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 131.50/19.21 % (4055858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 131.50/19.21 % (4055858)CaDiCaL version: 2.1.3
% 131.50/19.21 % (4055858)Termination reason: Instruction limit
% 131.50/19.21 % (4055858)Termination phase: Property scanning
% 131.50/19.21 % (4055858)Time elapsed: 0.165 s
% 131.50/19.21 % (4055858)Peak memory usage: 99 MB
% 131.50/19.21 % (4055858)Instructions burned: 322 (million)
% 131.50/19.21 % (4055860)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=3408290610:i=2064:ep=RST_2929 on theBenchmark for (2929ds/2064Mi)
% 131.50/19.21 % (4055854)Instruction limit reached!
% 131.50/19.21 % (4055854)------------------------------
% 131.50/19.21 % (4055854)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 131.50/19.21 % (4055854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 131.50/19.21 % (4055854)CaDiCaL version: 2.1.3
% 131.50/19.21 % (4055854)Termination reason: Instruction limit
% 131.50/19.21 % (4055854)Termination phase: Saturation
% 131.50/19.21 % (4055854)Time elapsed: 2.749 s
% 131.50/19.21 % (4055854)Peak memory usage: 134 MB
% 131.50/19.21 % (4055854)Instructions burned: 4850 (million)
% 131.50/19.21 % (4055862)dis-1011_128_sil=32000:random_seed=2775849644:i=3706:ep=RST:av=off_2919 on theBenchmark for (2919ds/3706Mi)
% 131.50/19.21 % (4055860)Instruction limit reached!
% 131.50/19.21 % (4055860)------------------------------
% 131.50/19.21 % (4055860)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 131.50/19.21 % (4055860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 131.50/19.21 % (4055860)CaDiCaL version: 2.1.3
% 131.50/19.21 % (4055860)Termination reason: Instruction limit
% 131.50/19.21 % (4055860)Termination phase: Saturation
% 131.50/19.21 % (4055860)Time elapsed: 1.192 s
% 131.50/19.21 % (4055860)Peak memory usage: 127 MB
% 131.50/19.21 % (4055860)Instructions burned: 2064 (million)
% 131.50/19.21 % (4055864)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=3298441766:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2916 on theBenchmark for (2916ds/757Mi)
% 131.50/19.21 % (4055864)Instruction limit reached!
% 131.50/19.21 % (4055864)------------------------------
% 131.50/19.21 % (4055864)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 131.50/19.21 % (4055864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 131.50/19.21 % (4055864)CaDiCaL version: 2.1.3
% 131.50/19.21 % (4055864)Termination reason: Instruction limit
% 131.50/19.21 % (4055864)Termination phase: Saturation
% 131.50/19.21 % (4055864)Time elapsed: 0.508 s
% 131.50/19.21 % (4055864)Peak memory usage: 101 MB
% 131.50/19.21 % (4055864)Instructions burned: 757 (million)
% 131.50/19.21 % (4055866)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=3315041081:i=13913:ss=axioms:sgt=8_2909 on theBenchmark for (2909ds/13913Mi)
% 131.50/19.21 % (4055832)Instruction limit reached!
% 131.50/19.21 % (4055832)------------------------------
% 131.50/19.21 % (4055832)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 131.50/19.21 % (4055832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 131.50/19.21 % (4055832)CaDiCaL version: 2.1.3
% 131.50/19.21 % (4055832)Termination reason: Instruction limit
% 131.50/19.21 % (4055832)Termination phase: Saturation
% 131.50/19.21 % (4055832)Time elapsed: 8.009 s
% 131.50/19.21 % (4055832)Peak memory usage: 252 MB
% 131.50/19.21 % (4055832)Instructions burned: 13194 (million)
% 131.50/19.21 % (4055868)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=3146080272:i=9925:aac=none_2904 on theBenchmark for (2904ds/9925Mi)
% 131.50/19.21 % (4055862)Instruction limit reached!
% 131.50/19.21 % (4055862)------------------------------
% 131.50/19.21 % (4055862)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 131.50/19.21 % (4055862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 149.36/21.78 % (4055862)CaDiCaL version: 2.1.3
% 149.36/21.78 % (4055862)Termination reason: Instruction limit
% 149.36/21.78 % (4055862)Termination phase: Saturation
% 149.36/21.78 % (4055862)Time elapsed: 1.953 s
% 149.36/21.78 % (4055862)Peak memory usage: 126 MB
% 149.36/21.78 % (4055862)Instructions burned: 3706 (million)
% 149.36/21.78 % (4055870)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=853981769:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2898 on theBenchmark for (2898ds/2479Mi)
% 149.36/21.78 % (4055856)Instruction limit reached!
% 149.36/21.78 % (4055856)------------------------------
% 149.36/21.78 % (4055856)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 149.36/21.78 % (4055856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 149.36/21.78 % (4055856)CaDiCaL version: 2.1.3
% 149.36/21.78 % (4055856)Termination reason: Instruction limit
% 149.36/21.78 % (4055856)Termination phase: Saturation
% 149.36/21.78 % (4055856)Time elapsed: 4.674 s
% 149.36/21.78 % (4055856)Peak memory usage: 248 MB
% 149.36/21.78 % (4055856)Instructions burned: 12113 (million)
% 149.36/21.78 % (4055872)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=2572766988:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2891 on theBenchmark for (2891ds/440Mi)
% 149.36/21.78 % (4055872)Instruction limit reached!
% 149.36/21.78 % (4055872)------------------------------
% 149.36/21.78 % (4055872)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 149.36/21.78 % (4055872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 149.36/21.78 % (4055872)CaDiCaL version: 2.1.3
% 149.36/21.78 % (4055872)Termination reason: Instruction limit
% 149.36/21.78 % (4055872)Termination phase: Property scanning
% 149.36/21.78 % (4055872)Time elapsed: 0.125 s
% 149.36/21.78 % (4055872)Peak memory usage: 102 MB
% 149.36/21.78 % (4055872)Instructions burned: 441 (million)
% 149.36/21.78 % (4055874)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=2224918241:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2889 on theBenchmark for (2889ds/11145Mi)
% 149.36/21.78 % (4055870)Instruction limit reached!
% 149.36/21.78 % (4055870)------------------------------
% 149.36/21.78 % (4055870)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 149.36/21.78 % (4055870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 149.36/21.78 % (4055870)CaDiCaL version: 2.1.3
% 149.36/21.78 % (4055870)Termination reason: Instruction limit
% 149.36/21.78 % (4055870)Termination phase: Saturation
% 149.36/21.78 % (4055870)Time elapsed: 1.645 s
% 149.36/21.78 % (4055870)Peak memory usage: 112 MB
% 149.36/21.78 % (4055870)Instructions burned: 2479 (million)
% 149.36/21.78 % (4055876)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=4213290124:cts=off:i=3034:av=off:er=known:fsd=on_2880 on theBenchmark for (2880ds/3034Mi)
% 149.36/21.78 % (4055876)Instruction limit reached!
% 149.36/21.78 % (4055876)------------------------------
% 149.36/21.78 % (4055876)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 149.36/21.78 % (4055876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 149.36/21.78 % (4055876)CaDiCaL version: 2.1.3
% 149.36/21.78 % (4055876)Termination reason: Instruction limit
% 149.36/21.78 % (4055876)Termination phase: Saturation
% 149.36/21.78 % (4055876)Time elapsed: 1.816 s
% 149.36/21.78 % (4055876)Peak memory usage: 234 MB
% 149.36/21.78 % (4055876)Instructions burned: 3036 (million)
% 149.36/21.78 % (4055878)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=2356175640:st=2:s2a=on:i=524:s2at=2:ss=axioms_2861 on theBenchmark for (2861ds/524Mi)
% 149.36/21.78 % (4055878)Instruction limit reached!
% 149.36/21.78 % (4055878)------------------------------
% 149.36/21.78 % (4055878)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 149.36/21.78 % (4055878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 149.36/21.78 % (4055878)CaDiCaL version: 2.1.3
% 149.36/21.78 % (4055878)Termination reason: Instruction limit
% 149.36/21.78 % (4055878)Termination phase: Saturation
% 149.36/21.78 % (4055878)Time elapsed: 0.279 s
% 149.36/21.78 % (4055878)Peak memory usage: 102 MB
% 149.36/21.78 % (4055878)Instructions burned: 526 (million)
% 149.36/21.78 % (4055880)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=2588699444:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2857 on theBenchmark for (2857ds/1016Mi)
% 149.36/21.78 % (4055874)Instruction limit reached!
% 149.36/21.78 % (4055874)------------------------------
% 179.17/25.97 % (4055874)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 179.17/25.97 % (4055874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 179.17/25.97 % (4055874)CaDiCaL version: 2.1.3
% 179.17/25.97 % (4055874)Termination reason: Instruction limit
% 179.17/25.97 % (4055874)Termination phase: Saturation
% 179.17/25.97 % (4055874)Time elapsed: 3.816 s
% 179.17/25.97 % (4055874)Peak memory usage: 217 MB
% 179.17/25.97 % (4055874)Instructions burned: 11148 (million)
% 179.17/25.97 % (4055880)Instruction limit reached!
% 179.17/25.97 % (4055880)------------------------------
% 179.17/25.97 % (4055880)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 179.17/25.97 % (4055880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 179.17/25.97 % (4055880)CaDiCaL version: 2.1.3
% 179.17/25.97 % (4055880)Termination reason: Instruction limit
% 179.17/25.97 % (4055880)Termination phase: Saturation
% 179.17/25.97 % (4055880)Time elapsed: 0.531 s
% 179.17/25.97 % (4055880)Peak memory usage: 112 MB
% 179.17/25.97 % (4055880)Instructions burned: 1017 (million)
% 179.17/25.97 % (4055868)Instruction limit reached!
% 179.17/25.97 % (4055868)------------------------------
% 179.17/25.97 % (4055868)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 179.17/25.97 % (4055868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 179.17/25.97 % (4055868)CaDiCaL version: 2.1.3
% 179.17/25.97 % (4055868)Termination reason: Instruction limit
% 179.17/25.97 % (4055868)Termination phase: Saturation
% 179.17/25.97 % (4055868)Time elapsed: 5.290 s
% 179.17/25.97 % (4055868)Peak memory usage: 235 MB
% 179.17/25.97 % (4055868)Instructions burned: 9927 (million)
% 179.17/25.97 % (4055882)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=1974855280:i=14123:bd=preordered:ins=4_2850 on theBenchmark for (2850ds/14123Mi)
% 179.17/25.97 % (4055883)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=2361389015:i=5781:kws=precedence:bd=all:rawr=on_2850 on theBenchmark for (2850ds/5781Mi)
% 179.17/25.97 % (4055884)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=3817350134:i=2448:gtgl=5:bd=preordered:gtg=all_2849 on theBenchmark for (2849ds/2448Mi)
% 179.17/25.97 % (4055884)Instruction limit reached!
% 179.17/25.97 % (4055884)------------------------------
% 179.17/25.97 % (4055884)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 179.17/25.97 % (4055884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 179.17/25.97 % (4055884)CaDiCaL version: 2.1.3
% 179.17/25.97 % (4055884)Termination reason: Instruction limit
% 179.17/25.97 % (4055884)Termination phase: Saturation
% 179.17/25.97 % (4055884)Time elapsed: 1.524 s
% 179.17/25.97 % (4055884)Peak memory usage: 237 MB
% 179.17/25.97 % (4055884)Instructions burned: 2448 (million)
% 179.17/25.97 % (4055888)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=1357536154:i=3223:kws=precedence:fgj=on:av=off_2833 on theBenchmark for (2833ds/3223Mi)
% 179.17/25.97 % (4055866)Instruction limit reached!
% 179.17/25.97 % (4055866)------------------------------
% 179.17/25.97 % (4055866)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 179.17/25.97 % (4055866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 179.17/25.97 % (4055866)CaDiCaL version: 2.1.3
% 179.17/25.97 % (4055866)Termination reason: Instruction limit
% 179.17/25.97 % (4055866)Termination phase: Saturation
% 179.17/25.97 % (4055866)Time elapsed: 8.366 s
% 179.17/25.97 % (4055866)Peak memory usage: 255 MB
% 179.17/25.97 % (4055866)Instructions burned: 13914 (million)
% 179.17/25.97 % (4055890)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=1275063241:st=5.6:i=2033:sd=3:ss=axioms_2824 on theBenchmark for (2824ds/2033Mi)
% 179.17/25.97 % (4055883)Instruction limit reached!
% 179.17/25.97 % (4055883)------------------------------
% 179.17/25.97 % (4055883)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 179.17/25.97 % (4055883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 179.17/25.97 % (4055883)CaDiCaL version: 2.1.3
% 179.17/25.97 % (4055883)Termination reason: Instruction limit
% 179.17/25.97 % (4055883)Termination phase: Saturation
% 179.17/25.97 % (4055883)Time elapsed: 3.378 s
% 179.17/25.97 % (4055883)Peak memory usage: 142 MB
% 179.17/25.97 % (4055883)Instructions burned: 5781 (million)
% 179.17/25.97 % (4055892)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=1011345777:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2815 on theBenchmark for (2815ds/2055Mi)
% 190.78/29.01 % (4055888)Instruction limit reached!
% 190.78/29.01 % (4055888)------------------------------
% 190.78/29.01 % (4055888)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 190.78/29.01 % (4055888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 190.78/29.01 % (4055888)CaDiCaL version: 2.1.3
% 190.78/29.01 % (4055888)Termination reason: Instruction limit
% 190.78/29.01 % (4055888)Termination phase: Saturation
% 190.78/29.01 % (4055888)Time elapsed: 1.889 s
% 190.78/29.01 % (4055888)Peak memory usage: 244 MB
% 190.78/29.01 % (4055888)Instructions burned: 3223 (million)
% 190.78/29.01 % (4055894)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=3164724811:i=21611:sd=3:ss=axioms_2812 on theBenchmark for (2812ds/21611Mi)
% 190.78/29.01 % (4055890)Instruction limit reached!
% 190.78/29.01 % (4055890)------------------------------
% 190.78/29.01 % (4055890)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 190.78/29.01 % (4055890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 190.78/29.01 % (4055890)CaDiCaL version: 2.1.3
% 190.78/29.01 % (4055890)Termination reason: Instruction limit
% 190.78/29.01 % (4055890)Termination phase: Saturation
% 190.78/29.01 % (4055890)Time elapsed: 1.299 s
% 190.78/29.01 % (4055890)Peak memory usage: 196 MB
% 190.78/29.01 % (4055890)Instructions burned: 2035 (million)
% 190.78/29.01 % (4055896)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=2793620453:i=4835:sd=13:ss=axioms:sgt=23_2809 on theBenchmark for (2809ds/4835Mi)
% 190.78/29.01 % (4055882)Instruction limit reached!
% 190.78/29.01 % (4055882)------------------------------
% 190.78/29.01 % (4055882)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 190.78/29.01 % (4055882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 190.78/29.01 % (4055882)CaDiCaL version: 2.1.3
% 190.78/29.01 % (4055882)Termination reason: Instruction limit
% 190.78/29.01 % (4055882)Termination phase: Saturation
% 190.78/29.01 % (4055882)Time elapsed: 4.640 s
% 190.78/29.01 % (4055882)Peak memory usage: 266 MB
% 190.78/29.01 % (4055882)Instructions burned: 14123 (million)
% 190.78/29.01 % (4055898)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=287349277:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2803 on theBenchmark for (2803ds/797Mi)
% 190.78/29.01 % (4055892)Instruction limit reached!
% 190.78/29.01 % (4055892)------------------------------
% 190.78/29.01 % (4055892)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 190.78/29.01 % (4055892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 190.78/29.01 % (4055892)CaDiCaL version: 2.1.3
% 190.78/29.01 % (4055892)Termination reason: Instruction limit
% 190.78/29.01 % (4055892)Termination phase: Saturation
% 190.78/29.01 % (4055892)Time elapsed: 1.199 s
% 190.78/29.01 % (4055892)Peak memory usage: 161 MB
% 190.78/29.01 % (4055892)Instructions burned: 2057 (million)
% 190.78/29.01 % (4055900)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=812528303:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2801 on theBenchmark for (2801ds/2326Mi)
% 190.78/29.01 % (4055898)Instruction limit reached!
% 190.78/29.01 % (4055898)------------------------------
% 190.78/29.01 % (4055898)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 190.78/29.01 % (4055898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 190.78/29.01 % (4055898)CaDiCaL version: 2.1.3
% 190.78/29.01 % (4055898)Termination reason: Instruction limit
% 190.78/29.01 % (4055898)Termination phase: Saturation
% 190.78/29.01 % (4055898)Time elapsed: 0.233 s
% 190.78/29.01 % (4055898)Peak memory usage: 104 MB
% 190.78/29.01 % (4055898)Instructions burned: 797 (million)
% 190.78/29.01 % (4055902)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=367633907:i=6038:nm=6_2800 on theBenchmark for (2800ds/6038Mi)
% 190.78/29.01 % (4055900)Instruction limit reached!
% 190.78/29.01 % (4055900)------------------------------
% 190.78/29.01 % (4055900)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 190.78/29.01 % (4055900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 190.78/29.01 % (4055900)CaDiCaL version: 2.1.3
% 190.78/29.01 % (4055900)Termination reason: Instruction limit
% 190.78/29.01 % (4055900)Termination phase: Saturation
% 190.78/29.01 % (4055900)Time elapsed: 1.226 s
% 190.78/29.01 % (4055900)Peak memory usage: 118 MB
% 190.78/29.01 % (4055900)Instructions burned: 2328 (million)
% 190.78/29.01 % (4055904)lrs+10_1_sil=32000:sp=occurrence:random_seed=1661982405:st=2:i=33334:sd=3:ss=included:sgt=32_2788 on theBenchmark for (2788ds/33334Mi)
% 190.78/29.01 % (4055902)Instruction limit reached!
% 190.78/29.01 % (4055902)------------------------------
% 190.78/29.01 % (4055902)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 190.78/29.01 % (4055902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 190.78/29.01 % (4055902)CaDiCaL version: 2.1.3
% 190.78/29.01 % (4055902)Termination reason: Instruction limit
% 190.78/29.01 % (4055902)Termination phase: Saturation
% 190.78/29.01 % (4055902)Time elapsed: 1.786 s
% 190.78/29.01 % (4055902)Peak memory usage: 291 MB
% 190.78/29.01 % (4055902)Instructions burned: 6040 (million)
% 190.78/29.01 % (4055896)Instruction limit reached!
% 190.78/29.01 % (4055896)------------------------------
% 190.78/29.01 % (4055896)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 190.78/29.01 % (4055896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 190.78/29.01 % (4055896)CaDiCaL version: 2.1.3
% 190.78/29.01 % (4055896)Termination reason: Instruction limit
% 190.78/29.01 % (4055896)Termination phase: Saturation
% 190.78/29.01 % (4055896)Time elapsed: 2.791 s
% 190.78/29.01 % (4055896)Peak memory usage: 141 MB
% 190.78/29.01 % (4055896)Instructions burned: 4836 (million)
% 190.78/29.01 % (4055906)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=2868647512:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2781 on theBenchmark for (2781ds/1008Mi)
% 190.78/29.01 % (4055907)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=128000:tgt=ground:npcc=on:fde=none:sp=const_frequency:spb=intro:gs=on:random_seed=1300674922:i=8327:s2at=5:bd=preordered_2780 on theBenchmark for (2780ds/8327Mi)
% 190.78/29.01 % (4055906)Instruction limit reached!
% 190.78/29.01 % (4055906)------------------------------
% 190.78/29.01 % (4055906)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 190.78/29.01 % (4055906)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 190.78/29.01 % (4055906)CaDiCaL version: 2.1.3
% 190.78/29.01 % (4055906)Termination reason: Instruction limit
% 190.78/29.01 % (4055906)Termination phase: Saturation
% 190.78/29.01 % (4055906)Time elapsed: 0.325 s
% 190.78/29.01 % (4055906)Peak memory usage: 103 MB
% 190.78/29.01 % (4055906)Instructions burned: 1008 (million)
% 190.78/29.01 % (4055910)lrs+1002_1_slsqr=3,2:sil=8000:tgt=full:plsq=on:fde=unused:plsqc=1:plsqr=3,2:sp=reverse_arity:spb=intro:urr=on:plsql=on:s2agt=16:br=off:slsqc=2:slsq=on:random_seed=3004722613:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2776 on theBenchmark for (2776ds/1083Mi)
% 190.78/29.01 % (4055910)Instruction limit reached!
% 190.78/29.01 % (4055910)------------------------------
% 190.78/29.01 % (4055910)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 190.78/29.01 % (4055910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 190.78/29.01 % (4055910)CaDiCaL version: 2.1.3
% 190.78/29.01 % (4055910)Termination reason: Instruction limit
% 190.78/29.01 % (4055910)Termination phase: Saturation
% 190.78/29.01 % (4055910)Time elapsed: 0.297 s
% 190.78/29.01 % (4055910)Peak memory usage: 112 MB
% 190.78/29.01 % (4055910)Instructions burned: 1084 (million)
% 190.78/29.01 % (4055912)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=1183002931:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2773 on theBenchmark for (2773ds/1084Mi)
% 190.78/29.01 % (4055912)Instruction limit reached!
% 190.78/29.01 % (4055912)------------------------------
% 190.78/29.01 % (4055912)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 190.78/29.01 % (4055912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 190.78/29.01 % (4055912)CaDiCaL version: 2.1.3
% 190.78/29.01 % (4055912)Termination reason: Instruction limit
% 190.78/29.01 % (4055912)Termination phase: Saturation
% 190.78/29.01 % (4055912)Time elapsed: 0.340 s
% 190.78/29.01 % (4055912)Peak memory usage: 105 MB
% 190.78/29.01 % (4055912)Instructions burned: 1085 (million)
% 190.78/29.01 % (4055914)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=2947794532:i=6995:s2at=5:gtg=all_2768 on theBenchmark for (2768ds/6995Mi)
% 190.78/29.01 % (4055914)Instruction limit reached!
% 190.78/29.01 % (4055914)------------------------------
% 190.78/29.01 % (4055914)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 190.78/29.01 % (4055914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 190.78/29.01 % (4055914)CaDiCaL version: 2.1.3
% 190.78/29.01 % (4055914)Termination reason: Instruction limit
% 190.78/29.01 % (4055914)Termination phase: Saturation
% 190.78/29.01 % (4055914)Time elapsed: 2.137 s
% 190.78/29.01 % (4055914)Peak memory usage: 238 MB
% 190.78/29.01 % (4055914)Instructions burned: 6995 (million)
% 190.78/29.01 % (4055916)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=2918938049:st=2:i=6225:sd=15:ss=axioms_2746 on theBenchmark for (2746ds/6225Mi)
% 190.78/29.01 % (4055907)Instruction limit reached!
% 190.78/29.01 % (4055907)------------------------------
% 190.78/29.01 % (4055907)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 190.78/29.01 % (4055907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 190.78/29.01 % (4055907)CaDiCaL version: 2.1.3
% 190.78/29.01 % (4055907)Termination reason: Instruction limit
% 190.78/29.01 % (4055907)Termination phase: Saturation
% 190.78/29.01 % (4055907)Time elapsed: 5.099 s
% 190.78/29.01 % (4055907)Peak memory usage: 245 MB
% 190.78/29.01 % (4055907)Instructions burned: 8328 (million)
% 190.78/29.01 % (4055916)Instruction limit reached!
% 190.78/29.01 % (4055916)------------------------------
% 190.78/29.01 % (4055916)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 190.78/29.01 % (4055916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 190.78/29.01 % (4055916)CaDiCaL version: 2.1.3
% 190.78/29.01 % (4055916)Termination reason: Instruction limit
% 190.78/29.01 % (4055916)Termination phase: Saturation
% 190.78/29.01 % (4055916)Time elapsed: 1.869 s
% 190.78/29.01 % (4055916)Peak memory usage: 220 MB
% 190.78/29.01 % (4055916)Instructions burned: 6226 (million)
% 190.78/29.01 % (4055918)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=3920064220:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2728 on theBenchmark for (2728ds/3372Mi)
% 190.78/29.01 % (4055920)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=1191105903:st=2.3:i=26457:sd=10:ss=included:sgt=8_2726 on theBenchmark for (2726ds/26457Mi)
% 190.78/29.01 % (4055894)First to succeed.
% 190.78/29.01 % (4055894)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-4055785"
% 190.78/29.01 % (4055894)Refutation found. Thanks to Tanya!
% 190.78/29.01 % SZS status Theorem for theBenchmark
% 190.78/29.01 % SZS output start Proof for theBenchmark
% See solution above
% 0.17/29.21 % (4055894)------------------------------
% 0.17/29.21 % (4055894)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.17/29.21 % (4055894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.17/29.21 % (4055894)CaDiCaL version: 2.1.3
% 0.17/29.21 % (4055894)Termination reason: Refutation
% 0.17/29.21 % (4055894)Time elapsed: 9.184 s
% 0.17/29.21 % (4055894)Peak memory usage: 247 MB
% 0.17/29.21 % (4055894)Instructions burned: 14840 (million)
% 0.17/29.21 % (4055894)------------------------------
% 0.17/29.21 % (4055894)------------------------------
% 0.17/29.21 % (4055785)Success in time 28.394 s
% 0.17/29.21 % Vampire exiting
%------------------------------------------------------------------------------