%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU433+3 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n007.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:49:01 PM UTC 2026
% Result : Theorem 100.89s 28.11s
% Output : Refutation 186.96s
% Verified :
% SZS Type : Refutation
% Derivation depth : 34
% Number of leaves : 67
% Syntax : Number of formulae : 440 ( 72 unt; 47 def)
% Number of atoms : 2333 ( 136 equ)
% Maximal formula atoms : 17 ( 5 avg)
% Number of connectives : 3473 (1580 ~;1732 |; 80 &)
% ( 55 <=>; 25 =>; 0 <=; 1 <~>)
% Maximal formula depth : 23 ( 7 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 46 ( 44 usr; 40 prp; 0-2 aty)
% Number of functors : 29 ( 29 usr; 13 con; 0-4 aty)
% Number of variables : 531 ( 0 sgn 507 !; 24 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X0,X1] :
( ! [X2] :
( r2_hidden(X2,X0)
<=> r2_hidden(X2,X1) )
=> X0 = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2_tarski) ).
fof(f4,axiom,
! [X0,X1] :
( X1 = k1_tarski(X0)
<=> ! [X2] :
( r2_hidden(X2,X1)
<=> X2 = X0 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d1_tarski) ).
fof(f8,axiom,
! [X0,X1] :
( r1_tarski(X0,X1)
<=> ! [X2] :
( r2_hidden(X2,X0)
=> r2_hidden(X2,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d3_tarski) ).
fof(f31,axiom,
! [X0,X1,X2] :
( X2 = k3_xboole_0(X0,X1)
<=> ! [X3] :
( r2_hidden(X3,X2)
<=> ( r2_hidden(X3,X0)
& r2_hidden(X3,X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d3_xboole_0) ).
fof(f38,axiom,
! [X0,X1] :
( X0 = X1
<=> ( r1_tarski(X0,X1)
& r1_tarski(X1,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d10_xboole_0) ).
fof(f571,axiom,
! [X0,X1,X2] :
( ( m1_subset_1(X1,k1_zfmisc_1(X0))
& m1_subset_1(X2,k1_zfmisc_1(X0)) )
=> m1_subset_1(k5_subset_1(X0,X1,X2),k1_zfmisc_1(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k5_subset_1) ).
fof(f572,axiom,
! [X0,X1,X2] :
( ( m1_subset_1(X1,k1_zfmisc_1(X0))
& m1_subset_1(X2,k1_zfmisc_1(X0)) )
=> k5_subset_1(X0,X1,X2) = k5_subset_1(X0,X2,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_k5_subset_1) ).
fof(f574,axiom,
! [X0,X1,X2] :
( ( m1_subset_1(X1,k1_zfmisc_1(X0))
& m1_subset_1(X2,k1_zfmisc_1(X0)) )
=> k5_subset_1(X0,X1,X2) = k3_xboole_0(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k5_subset_1) ).
fof(f678,axiom,
! [X0,X1,X2] :
( ( r2_hidden(X0,X1)
& m1_subset_1(X1,k1_zfmisc_1(X2)) )
=> m1_subset_1(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t4_subset) ).
fof(f679,axiom,
! [X0,X1,X2] :
~ ( r2_hidden(X0,X1)
& m1_subset_1(X1,k1_zfmisc_1(X2))
& v1_xboole_0(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t5_subset) ).
fof(f849,axiom,
! [X0] :
( v1_relat_1(X0)
=> ! [X1,X2] :
( X2 = k9_relat_1(X0,X1)
<=> ! [X3] :
( r2_hidden(X3,X2)
<=> ? [X4] :
( r2_hidden(k4_tarski(X4,X3),X0)
& r2_hidden(X4,X1) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d13_relat_1) ).
fof(f1333,axiom,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
=> v1_relat_1(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc1_relset_1) ).
fof(f19064,axiom,
! [X0,X1,X2,X3] :
( ( m1_subset_1(X2,k1_zfmisc_1(X0))
& m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) )
=> m1_subset_1(k8_relset_2(X0,X1,X2,X3),k1_zfmisc_1(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k8_relset_2) ).
fof(f19077,axiom,
! [X0,X1,X2] :
( v1_relat_1(X2)
=> ( r2_hidden(X0,k9_relat_1(X2,k1_tarski(X1)))
<=> r2_hidden(k4_tarski(X1,X0),X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t9_relset_2) ).
fof(f19095,axiom,
! [X0,X1,X2,X3] :
( m1_subset_1(X3,k1_zfmisc_1(X0))
=> ! [X4] :
( m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
=> ( r2_hidden(X2,k8_relset_2(X0,X1,X3,X4))
=> ! [X5] :
( r2_hidden(X5,X3)
=> r2_hidden(X2,k9_relat_1(X4,k1_tarski(X5))) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t24_relset_2) ).
fof(f19096,axiom,
! [X0] :
( ~ v1_xboole_0(X0)
=> ! [X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(X1))
=> ! [X3] :
( m1_subset_1(X3,X0)
=> ! [X4] :
( m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X1,X0)))
=> ( r2_hidden(X3,k8_relset_2(X1,X0,X2,X4))
<=> ! [X5] :
( r2_hidden(X5,X2)
=> r2_hidden(X3,k9_relat_1(X4,k1_tarski(X5))) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t25_relset_2) ).
fof(f19105,conjecture,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(X0))
=> ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
=> ! [X4] :
( m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
=> k8_relset_2(X0,X1,X2,k5_subset_1(k2_zfmisc_1(X0,X1),X3,X4)) = k5_subset_1(X1,k8_relset_2(X0,X1,X2,X3),k8_relset_2(X0,X1,X2,X4)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t34_relset_2) ).
fof(f19106,negated_conjecture,
~ ! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(X0))
=> ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
=> ! [X4] :
( m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
=> k8_relset_2(X0,X1,X2,k5_subset_1(k2_zfmisc_1(X0,X1),X3,X4)) = k5_subset_1(X1,k8_relset_2(X0,X1,X2,X3),k8_relset_2(X0,X1,X2,X4)) ) ) ),
inference(negated_conjecture,[status(cth)],[f19105]) ).
fof(f19127,plain,
? [X0,X1,X2] :
( ? [X3] :
( ? [X4] :
( k8_relset_2(X0,X1,X2,k5_subset_1(k2_zfmisc_1(X0,X1),X3,X4)) != k5_subset_1(X1,k8_relset_2(X0,X1,X2,X3),k8_relset_2(X0,X1,X2,X4))
& m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) )
& m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) )
& m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f19106]) ).
fof(f19129,plain,
! [X0,X1,X2] :
( v1_relat_1(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(ennf_transformation,[],[f1333]) ).
fof(f19163,plain,
! [X0,X1,X2] :
( k5_subset_1(X0,X1,X2) = k3_xboole_0(X1,X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f574]) ).
fof(f19164,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,[],[f19163]) ).
fof(f19167,plain,
! [X0,X1,X2] :
( k5_subset_1(X0,X1,X2) = k5_subset_1(X0,X2,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f572]) ).
fof(f19168,plain,
! [X0,X1,X2] :
( k5_subset_1(X0,X1,X2) = k5_subset_1(X0,X2,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(flattening,[],[f19167]) ).
fof(f19169,plain,
! [X0,X1,X2] :
( m1_subset_1(k5_subset_1(X0,X1,X2),k1_zfmisc_1(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f571]) ).
fof(f19170,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,[],[f19169]) ).
fof(f19179,plain,
! [X0] :
( ! [X1,X2] :
( ! [X3] :
( ! [X4] :
( ( r2_hidden(X3,k8_relset_2(X1,X0,X2,X4))
<=> ! [X5] :
( r2_hidden(X3,k9_relat_1(X4,k1_tarski(X5)))
| ~ r2_hidden(X5,X2) ) )
| ~ m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X1,X0))) )
| ~ m1_subset_1(X3,X0) )
| ~ m1_subset_1(X2,k1_zfmisc_1(X1)) )
| v1_xboole_0(X0) ),
inference(ennf_transformation,[],[f19096]) ).
fof(f19180,plain,
! [X0,X1,X2,X3] :
( ! [X4] :
( ! [X5] :
( r2_hidden(X2,k9_relat_1(X4,k1_tarski(X5)))
| ~ r2_hidden(X5,X3) )
| ~ r2_hidden(X2,k8_relset_2(X0,X1,X3,X4))
| ~ m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) )
| ~ m1_subset_1(X3,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f19095]) ).
fof(f19181,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,[],[f19180]) ).
fof(f19182,plain,
! [X0,X1,X2,X3] :
( m1_subset_1(k8_relset_2(X0,X1,X2,X3),k1_zfmisc_1(X1))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| ~ m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(ennf_transformation,[],[f19064]) ).
fof(f19183,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,[],[f19182]) ).
fof(f19186,plain,
! [X0,X1,X2] :
( ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ v1_xboole_0(X2) ),
inference(ennf_transformation,[],[f679]) ).
fof(f19219,plain,
! [X0,X1] :
( r1_tarski(X0,X1)
<=> ! [X2] :
( r2_hidden(X2,X1)
| ~ r2_hidden(X2,X0) ) ),
inference(ennf_transformation,[],[f8]) ).
fof(f19342,plain,
! [X0,X1,X2] :
( m1_subset_1(X0,X2)
| ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2)) ),
inference(ennf_transformation,[],[f678]) ).
fof(f19343,plain,
! [X0,X1,X2] :
( m1_subset_1(X0,X2)
| ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2)) ),
inference(flattening,[],[f19342]) ).
fof(f19352,plain,
! [X0,X1] :
( X0 = X1
| ? [X2] :
( r2_hidden(X2,X0)
<~> r2_hidden(X2,X1) ) ),
inference(ennf_transformation,[],[f3]) ).
fof(f19410,plain,
! [X0,X1,X2] :
( ( r2_hidden(X0,k9_relat_1(X2,k1_tarski(X1)))
<=> r2_hidden(k4_tarski(X1,X0),X2) )
| ~ v1_relat_1(X2) ),
inference(ennf_transformation,[],[f19077]) ).
fof(f19475,plain,
! [X0] :
( ! [X1,X2] :
( X2 = k9_relat_1(X0,X1)
<=> ! [X3] :
( r2_hidden(X3,X2)
<=> ? [X4] :
( r2_hidden(k4_tarski(X4,X3),X0)
& r2_hidden(X4,X1) ) ) )
| ~ v1_relat_1(X0) ),
inference(ennf_transformation,[],[f849]) ).
fof(f20113,plain,
( k8_relset_2(sK21,sK22,sK23,k5_subset_1(k2_zfmisc_1(sK21,sK22),sK24,sK25)) != k5_subset_1(sK22,k8_relset_2(sK21,sK22,sK23,sK24),k8_relset_2(sK21,sK22,sK23,sK25))
& m1_subset_1(sK25,k1_zfmisc_1(k2_zfmisc_1(sK21,sK22)))
& m1_subset_1(sK24,k1_zfmisc_1(k2_zfmisc_1(sK21,sK22)))
& m1_subset_1(sK23,k1_zfmisc_1(sK21)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK21,sK22,sK23,sK24,sK25]),skolemize(X0,sK21),skolemize(X1,sK22),skolemize(X2,sK23),skolemize(X3,sK24),skolemize(X4,sK25)],[f19127]) ).
fof(f20120,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,[],[f19179]) ).
fof(f20121,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,[],[f20120]) ).
fof(f20122,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(sK28(X2,X3,X4))))
& r2_hidden(sK28(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,[sK28]),skolemize(X5,sK28(X2,X3,X4))],[f20121]) ).
fof(f20139,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(f20140,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,[],[f20139]) ).
fof(f20141,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,[],[f19219]) ).
fof(f20142,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,[],[f20141]) ).
fof(f20143,plain,
! [X0,X1] :
( ( r1_tarski(X0,X1)
| ( ~ r2_hidden(sK41(X0,X1),X1)
& r2_hidden(sK41(X0,X1),X0) ) )
& ( ! [X3] :
( r2_hidden(X3,X1)
| ~ r2_hidden(X3,X0) )
| ~ r1_tarski(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK41]),skolemize(X2,sK41(X0,X1))],[f20142]) ).
fof(f20198,plain,
! [X0,X1] :
( ( X1 = k1_tarski(X0)
| ? [X2] :
( ( X0 != X2
| ~ r2_hidden(X2,X1) )
& ( X2 = X0
| r2_hidden(X2,X1) ) ) )
& ( ! [X2] :
( ( r2_hidden(X2,X1)
| X0 != X2 )
& ( X2 = X0
| ~ r2_hidden(X2,X1) ) )
| k1_tarski(X0) != X1 ) ),
inference(nnf_transformation,[],[f4]) ).
fof(f20199,plain,
! [X0,X1] :
( ( X1 = k1_tarski(X0)
| ? [X2] :
( ( X0 != X2
| ~ r2_hidden(X2,X1) )
& ( X2 = X0
| r2_hidden(X2,X1) ) ) )
& ( ! [X3] :
( ( r2_hidden(X3,X1)
| X0 != X3 )
& ( X0 = X3
| ~ r2_hidden(X3,X1) ) )
| k1_tarski(X0) != X1 ) ),
inference(rectify,[],[f20198]) ).
fof(f20200,plain,
! [X0,X1] :
( ( X1 = k1_tarski(X0)
| ( ( sK72(X0,X1) != X0
| ~ r2_hidden(sK72(X0,X1),X1) )
& ( sK72(X0,X1) = X0
| r2_hidden(sK72(X0,X1),X1) ) ) )
& ( ! [X3] :
( ( r2_hidden(X3,X1)
| X0 != X3 )
& ( X0 = X3
| ~ r2_hidden(X3,X1) ) )
| k1_tarski(X0) != X1 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK72]),skolemize(X2,sK72(X0,X1))],[f20199]) ).
fof(f20209,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,[],[f19352]) ).
fof(f20210,plain,
! [X0,X1] :
( X0 = X1
| ( ( ~ r2_hidden(sK77(X0,X1),X1)
| ~ r2_hidden(sK77(X0,X1),X0) )
& ( r2_hidden(sK77(X0,X1),X1)
| r2_hidden(sK77(X0,X1),X0) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK77]),skolemize(X2,sK77(X0,X1))],[f20209]) ).
fof(f20213,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(f20214,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,[],[f20213]) ).
fof(f20215,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,[],[f20214]) ).
fof(f20216,plain,
! [X0,X1,X2] :
( ( X2 = k3_xboole_0(X0,X1)
| ( ( ~ r2_hidden(sK81(X0,X1,X2),X0)
| ~ r2_hidden(sK81(X0,X1,X2),X1)
| ~ r2_hidden(sK81(X0,X1,X2),X2) )
& ( ( r2_hidden(sK81(X0,X1,X2),X0)
& r2_hidden(sK81(X0,X1,X2),X1) )
| r2_hidden(sK81(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,[sK81]),skolemize(X3,sK81(X0,X1,X2))],[f20215]) ).
fof(f20220,plain,
! [X0,X1,X2] :
( ( ( r2_hidden(X0,k9_relat_1(X2,k1_tarski(X1)))
| ~ r2_hidden(k4_tarski(X1,X0),X2) )
& ( r2_hidden(k4_tarski(X1,X0),X2)
| ~ r2_hidden(X0,k9_relat_1(X2,k1_tarski(X1))) ) )
| ~ v1_relat_1(X2) ),
inference(nnf_transformation,[],[f19410]) ).
fof(f20231,plain,
! [X0] :
( ! [X1,X2] :
( ( X2 = k9_relat_1(X0,X1)
| ? [X3] :
( ( ! [X4] :
( ~ r2_hidden(k4_tarski(X4,X3),X0)
| ~ r2_hidden(X4,X1) )
| ~ r2_hidden(X3,X2) )
& ( ? [X4] :
( r2_hidden(k4_tarski(X4,X3),X0)
& r2_hidden(X4,X1) )
| r2_hidden(X3,X2) ) ) )
& ( ! [X3] :
( ( r2_hidden(X3,X2)
| ! [X4] :
( ~ r2_hidden(k4_tarski(X4,X3),X0)
| ~ r2_hidden(X4,X1) ) )
& ( ? [X4] :
( r2_hidden(k4_tarski(X4,X3),X0)
& r2_hidden(X4,X1) )
| ~ r2_hidden(X3,X2) ) )
| k9_relat_1(X0,X1) != X2 ) )
| ~ v1_relat_1(X0) ),
inference(nnf_transformation,[],[f19475]) ).
fof(f20232,plain,
! [X0] :
( ! [X1,X2] :
( ( X2 = k9_relat_1(X0,X1)
| ? [X3] :
( ( ! [X4] :
( ~ r2_hidden(k4_tarski(X4,X3),X0)
| ~ r2_hidden(X4,X1) )
| ~ r2_hidden(X3,X2) )
& ( ? [X5] :
( r2_hidden(k4_tarski(X5,X3),X0)
& r2_hidden(X5,X1) )
| r2_hidden(X3,X2) ) ) )
& ( ! [X6] :
( ( r2_hidden(X6,X2)
| ! [X7] :
( ~ r2_hidden(k4_tarski(X7,X6),X0)
| ~ r2_hidden(X7,X1) ) )
& ( ? [X8] :
( r2_hidden(k4_tarski(X8,X6),X0)
& r2_hidden(X8,X1) )
| ~ r2_hidden(X6,X2) ) )
| k9_relat_1(X0,X1) != X2 ) )
| ~ v1_relat_1(X0) ),
inference(rectify,[],[f20231]) ).
fof(f20233,plain,
! [X0] :
( ! [X1,X2] :
( ( X2 = k9_relat_1(X0,X1)
| ( ( ! [X4] :
( ~ r2_hidden(k4_tarski(X4,sK92(X0,X1,X2)),X0)
| ~ r2_hidden(X4,X1) )
| ~ r2_hidden(sK92(X0,X1,X2),X2) )
& ( ( r2_hidden(k4_tarski(sK93(X0,X1,X2),sK92(X0,X1,X2)),X0)
& r2_hidden(sK93(X0,X1,X2),X1) )
| r2_hidden(sK92(X0,X1,X2),X2) ) ) )
& ( ! [X6] :
( ( r2_hidden(X6,X2)
| ! [X7] :
( ~ r2_hidden(k4_tarski(X7,X6),X0)
| ~ r2_hidden(X7,X1) ) )
& ( ( r2_hidden(k4_tarski(sK94(X0,X1,X6),X6),X0)
& r2_hidden(sK94(X0,X1,X6),X1) )
| ~ r2_hidden(X6,X2) ) )
| k9_relat_1(X0,X1) != X2 ) )
| ~ v1_relat_1(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK92,sK93,sK94]),skolemize(X3,sK92(X0,X1,X2)),skolemize(X5,sK93(X0,X1,X2)),skolemize(X8,sK94(X0,X1,X6))],[f20232]) ).
fof(f20495,plain,
m1_subset_1(sK23,k1_zfmisc_1(sK21)),
inference(cnf_transformation,[],[f20113]) ).
fof(f20496,plain,
m1_subset_1(sK24,k1_zfmisc_1(k2_zfmisc_1(sK21,sK22))),
inference(cnf_transformation,[],[f20113]) ).
fof(f20497,plain,
m1_subset_1(sK25,k1_zfmisc_1(k2_zfmisc_1(sK21,sK22))),
inference(cnf_transformation,[],[f20113]) ).
fof(f20498,plain,
k8_relset_2(sK21,sK22,sK23,k5_subset_1(k2_zfmisc_1(sK21,sK22),sK24,sK25)) != k5_subset_1(sK22,k8_relset_2(sK21,sK22,sK23,sK24),k8_relset_2(sK21,sK22,sK23,sK25)),
inference(cnf_transformation,[],[f20113]) ).
fof(f20502,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| v1_relat_1(X2) ),
inference(cnf_transformation,[],[f19129]) ).
fof(f20538,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,[],[f19164]) ).
fof(f20540,plain,
! [X2,X0,X1] :
( k5_subset_1(X0,X1,X2) = k5_subset_1(X0,X2,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f19168]) ).
fof(f20541,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,[],[f19170]) ).
fof(f20551,plain,
! [X2,X3,X0,X1,X4] :
( r2_hidden(X3,k8_relset_2(X1,X0,X2,X4))
| r2_hidden(sK28(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,[],[f20122]) ).
fof(f20552,plain,
! [X2,X3,X0,X1,X4] :
( ~ r2_hidden(X3,k9_relat_1(X4,k1_tarski(sK28(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,[],[f20122]) ).
fof(f20553,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,[],[f19181]) ).
fof(f20554,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,[],[f19183]) ).
fof(f20567,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ r2_hidden(X0,X1)
| ~ v1_xboole_0(X2) ),
inference(cnf_transformation,[],[f19186]) ).
fof(f20611,plain,
! [X0,X1] :
( ~ r1_tarski(X1,X0)
| ~ r1_tarski(X0,X1)
| X0 = X1 ),
inference(cnf_transformation,[],[f20140]) ).
fof(f20614,plain,
! [X0,X1] :
( r2_hidden(sK41(X0,X1),X0)
| r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f20143]) ).
fof(f20615,plain,
! [X0,X1] :
( ~ r2_hidden(sK41(X0,X1),X1)
| r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f20143]) ).
fof(f20808,plain,
! [X3,X0,X1] :
( r2_hidden(X3,X1)
| X0 != X3
| k1_tarski(X0) != X1 ),
inference(cnf_transformation,[],[f20200]) ).
fof(f20815,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ r2_hidden(X0,X1)
| m1_subset_1(X0,X2) ),
inference(cnf_transformation,[],[f19343]) ).
fof(f20827,plain,
! [X0,X1] :
( r2_hidden(sK77(X0,X1),X1)
| X0 = X1
| r2_hidden(sK77(X0,X1),X0) ),
inference(cnf_transformation,[],[f20210]) ).
fof(f20869,plain,
! [X2,X0,X1,X4] :
( r2_hidden(X4,X0)
| ~ r2_hidden(X4,X2)
| k3_xboole_0(X0,X1) != X2 ),
inference(cnf_transformation,[],[f20216]) ).
fof(f20870,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,[],[f20216]) ).
fof(f20893,plain,
! [X2,X0,X1] :
( ~ r2_hidden(X0,k9_relat_1(X2,k1_tarski(X1)))
| r2_hidden(k4_tarski(X1,X0),X2)
| ~ v1_relat_1(X2) ),
inference(cnf_transformation,[],[f20220]) ).
fof(f20950,plain,
! [X2,X0,X1,X6,X7] :
( r2_hidden(X6,X2)
| ~ r2_hidden(k4_tarski(X7,X6),X0)
| ~ r2_hidden(X7,X1)
| k9_relat_1(X0,X1) != X2
| ~ v1_relat_1(X0) ),
inference(cnf_transformation,[],[f20233]) ).
fof(f22000,plain,
! [X3,X1] :
( r2_hidden(X3,X1)
| k1_tarski(X3) != X1 ),
inference(equality_resolution,[],[f20808]) ).
fof(f22001,plain,
! [X3] : r2_hidden(X3,k1_tarski(X3)),
inference(equality_resolution,[],[f22000]) ).
fof(f22003,plain,
! [X0,X1,X4] :
( r2_hidden(X4,k3_xboole_0(X0,X1))
| ~ r2_hidden(X4,X0)
| ~ r2_hidden(X4,X1) ),
inference(equality_resolution,[],[f20870]) ).
fof(f22004,plain,
! [X0,X1,X4] :
( ~ r2_hidden(X4,k3_xboole_0(X0,X1))
| r2_hidden(X4,X0) ),
inference(equality_resolution,[],[f20869]) ).
fof(f22012,plain,
! [X0,X1,X6,X7] :
( ~ r2_hidden(k4_tarski(X7,X6),X0)
| r2_hidden(X6,k9_relat_1(X0,X1))
| ~ r2_hidden(X7,X1)
| ~ v1_relat_1(X0) ),
inference(equality_resolution,[],[f20950]) ).
fof(f22104,definition,
sF284 = k2_zfmisc_1(sK21,sK22),
introduced(definition,[new_symbols(definition,[sF284])],[function_definition]) ).
fof(f22105,plain,
k2_zfmisc_1(sK21,sK22) = sF284,
inference(reorient_equations,[],[f22104]) ).
fof(f22106,definition,
sF285 = k5_subset_1(sF284,sK24,sK25),
introduced(definition,[new_symbols(definition,[sF285])],[function_definition]) ).
fof(f22107,plain,
k5_subset_1(sF284,sK24,sK25) = sF285,
inference(reorient_equations,[],[f22106]) ).
fof(f22108,definition,
sF286 = k8_relset_2(sK21,sK22,sK23,sF285),
introduced(definition,[new_symbols(definition,[sF286])],[function_definition]) ).
fof(f22109,plain,
k8_relset_2(sK21,sK22,sK23,sF285) = sF286,
inference(reorient_equations,[],[f22108]) ).
fof(f22110,definition,
sF287 = k8_relset_2(sK21,sK22,sK23,sK24),
introduced(definition,[new_symbols(definition,[sF287])],[function_definition]) ).
fof(f22111,plain,
k8_relset_2(sK21,sK22,sK23,sK24) = sF287,
inference(reorient_equations,[],[f22110]) ).
fof(f22112,definition,
sF288 = k8_relset_2(sK21,sK22,sK23,sK25),
introduced(definition,[new_symbols(definition,[sF288])],[function_definition]) ).
fof(f22113,plain,
k8_relset_2(sK21,sK22,sK23,sK25) = sF288,
inference(reorient_equations,[],[f22112]) ).
fof(f22114,definition,
sF289 = k5_subset_1(sK22,sF287,sF288),
introduced(definition,[new_symbols(definition,[sF289])],[function_definition]) ).
fof(f22115,plain,
k5_subset_1(sK22,sF287,sF288) = sF289,
inference(reorient_equations,[],[f22114]) ).
fof(f22116,plain,
sF286 != sF289,
inference(definition_folding,[],[f20498,f22115,f22113,f22111,f22109,f22107,f22105]) ).
fof(f22117,definition,
sF290 = k1_zfmisc_1(sF284),
introduced(definition,[new_symbols(definition,[sF290])],[function_definition]) ).
fof(f22118,plain,
k1_zfmisc_1(sF284) = sF290,
inference(reorient_equations,[],[f22117]) ).
fof(f22119,plain,
m1_subset_1(sK25,sF290),
inference(definition_folding,[],[f20497,f22118,f22105]) ).
fof(f22120,plain,
m1_subset_1(sK24,sF290),
inference(definition_folding,[],[f20496,f22118,f22105]) ).
fof(f22121,definition,
sF291 = k1_zfmisc_1(sK21),
introduced(definition,[new_symbols(definition,[sF291])],[function_definition]) ).
fof(f22122,plain,
k1_zfmisc_1(sK21) = sF291,
inference(reorient_equations,[],[f22121]) ).
fof(f22123,plain,
m1_subset_1(sK23,sF291),
inference(definition_folding,[],[f20495,f22122]) ).
fof(f22440,definition,
( spl292_62
<=> m1_subset_1(sK23,sF291) ),
introduced(definition,[new_symbols(definition,[spl292_62])],[avatar_definition]) ).
fof(f22442,plain,
( m1_subset_1(sK23,sF291)
| ~ spl292_62 ),
inference(avatar_component_clause,[],[f22440]) ).
fof(f22443,plain,
spl292_62,
inference(avatar_split_clause,[],[f22123,f22440]) ).
fof(f22445,definition,
( spl292_63
<=> m1_subset_1(sK24,sF290) ),
introduced(definition,[new_symbols(definition,[spl292_63])],[avatar_definition]) ).
fof(f22447,plain,
( m1_subset_1(sK24,sF290)
| ~ spl292_63 ),
inference(avatar_component_clause,[],[f22445]) ).
fof(f22448,plain,
spl292_63,
inference(avatar_split_clause,[],[f22120,f22445]) ).
fof(f22450,definition,
( spl292_64
<=> m1_subset_1(sK25,sF290) ),
introduced(definition,[new_symbols(definition,[spl292_64])],[avatar_definition]) ).
fof(f22452,plain,
( m1_subset_1(sK25,sF290)
| ~ spl292_64 ),
inference(avatar_component_clause,[],[f22450]) ).
fof(f22453,plain,
spl292_64,
inference(avatar_split_clause,[],[f22119,f22450]) ).
fof(f22455,definition,
( spl292_65
<=> sF286 = sF289 ),
introduced(definition,[new_symbols(definition,[spl292_65])],[avatar_definition]) ).
fof(f22457,plain,
( sF286 != sF289
| spl292_65 ),
inference(avatar_component_clause,[],[f22455]) ).
fof(f22458,plain,
~ spl292_65,
inference(avatar_split_clause,[],[f22116,f22455]) ).
fof(f22460,definition,
( spl292_66
<=> k2_zfmisc_1(sK21,sK22) = sF284 ),
introduced(definition,[new_symbols(definition,[spl292_66])],[avatar_definition]) ).
fof(f22462,plain,
( k2_zfmisc_1(sK21,sK22) = sF284
| ~ spl292_66 ),
inference(avatar_component_clause,[],[f22460]) ).
fof(f22463,plain,
spl292_66,
inference(avatar_split_clause,[],[f22105,f22460]) ).
fof(f22465,definition,
( spl292_67
<=> k5_subset_1(sF284,sK24,sK25) = sF285 ),
introduced(definition,[new_symbols(definition,[spl292_67])],[avatar_definition]) ).
fof(f22467,plain,
( k5_subset_1(sF284,sK24,sK25) = sF285
| ~ spl292_67 ),
inference(avatar_component_clause,[],[f22465]) ).
fof(f22468,plain,
spl292_67,
inference(avatar_split_clause,[],[f22107,f22465]) ).
fof(f22470,definition,
( spl292_68
<=> k8_relset_2(sK21,sK22,sK23,sF285) = sF286 ),
introduced(definition,[new_symbols(definition,[spl292_68])],[avatar_definition]) ).
fof(f22472,plain,
( k8_relset_2(sK21,sK22,sK23,sF285) = sF286
| ~ spl292_68 ),
inference(avatar_component_clause,[],[f22470]) ).
fof(f22473,plain,
spl292_68,
inference(avatar_split_clause,[],[f22109,f22470]) ).
fof(f22475,definition,
( spl292_69
<=> k8_relset_2(sK21,sK22,sK23,sK24) = sF287 ),
introduced(definition,[new_symbols(definition,[spl292_69])],[avatar_definition]) ).
fof(f22477,plain,
( k8_relset_2(sK21,sK22,sK23,sK24) = sF287
| ~ spl292_69 ),
inference(avatar_component_clause,[],[f22475]) ).
fof(f22478,plain,
spl292_69,
inference(avatar_split_clause,[],[f22111,f22475]) ).
fof(f22480,definition,
( spl292_70
<=> k8_relset_2(sK21,sK22,sK23,sK25) = sF288 ),
introduced(definition,[new_symbols(definition,[spl292_70])],[avatar_definition]) ).
fof(f22482,plain,
( k8_relset_2(sK21,sK22,sK23,sK25) = sF288
| ~ spl292_70 ),
inference(avatar_component_clause,[],[f22480]) ).
fof(f22483,plain,
spl292_70,
inference(avatar_split_clause,[],[f22113,f22480]) ).
fof(f22485,definition,
( spl292_71
<=> k5_subset_1(sK22,sF287,sF288) = sF289 ),
introduced(definition,[new_symbols(definition,[spl292_71])],[avatar_definition]) ).
fof(f22487,plain,
( k5_subset_1(sK22,sF287,sF288) = sF289
| ~ spl292_71 ),
inference(avatar_component_clause,[],[f22485]) ).
fof(f22488,plain,
spl292_71,
inference(avatar_split_clause,[],[f22115,f22485]) ).
fof(f22490,definition,
( spl292_72
<=> k1_zfmisc_1(sF284) = sF290 ),
introduced(definition,[new_symbols(definition,[spl292_72])],[avatar_definition]) ).
fof(f22492,plain,
( k1_zfmisc_1(sF284) = sF290
| ~ spl292_72 ),
inference(avatar_component_clause,[],[f22490]) ).
fof(f22493,plain,
spl292_72,
inference(avatar_split_clause,[],[f22118,f22490]) ).
fof(f22495,definition,
( spl292_73
<=> k1_zfmisc_1(sK21) = sF291 ),
introduced(definition,[new_symbols(definition,[spl292_73])],[avatar_definition]) ).
fof(f22497,plain,
( k1_zfmisc_1(sK21) = sF291
| ~ spl292_73 ),
inference(avatar_component_clause,[],[f22495]) ).
fof(f22498,plain,
spl292_73,
inference(avatar_split_clause,[],[f22122,f22495]) ).
fof(f22499,plain,
( m1_subset_1(sF286,k1_zfmisc_1(sK22))
| ~ m1_subset_1(sK23,k1_zfmisc_1(sK21))
| ~ m1_subset_1(sF285,k1_zfmisc_1(k2_zfmisc_1(sK21,sK22)))
| ~ spl292_68 ),
inference(superposition,[],[f20554,f22472]) ).
fof(f22501,definition,
( spl292_74
<=> m1_subset_1(sF285,k1_zfmisc_1(k2_zfmisc_1(sK21,sK22))) ),
introduced(definition,[new_symbols(definition,[spl292_74])],[avatar_definition]) ).
fof(f22503,plain,
( ~ m1_subset_1(sF285,k1_zfmisc_1(k2_zfmisc_1(sK21,sK22)))
| spl292_74 ),
inference(avatar_component_clause,[],[f22501]) ).
fof(f22505,definition,
( spl292_75
<=> m1_subset_1(sK23,k1_zfmisc_1(sK21)) ),
introduced(definition,[new_symbols(definition,[spl292_75])],[avatar_definition]) ).
fof(f22509,definition,
( spl292_76
<=> m1_subset_1(sF286,k1_zfmisc_1(sK22)) ),
introduced(definition,[new_symbols(definition,[spl292_76])],[avatar_definition]) ).
fof(f22511,plain,
( m1_subset_1(sF286,k1_zfmisc_1(sK22))
| ~ spl292_76 ),
inference(avatar_component_clause,[],[f22509]) ).
fof(f22512,plain,
( ~ spl292_74
| ~ spl292_75
| spl292_76
| ~ spl292_68 ),
inference(avatar_split_clause,[],[f22499,f22470,f22509,f22505,f22501]) ).
fof(f22513,plain,
( m1_subset_1(sF287,k1_zfmisc_1(sK22))
| ~ m1_subset_1(sK23,k1_zfmisc_1(sK21))
| ~ m1_subset_1(sK24,k1_zfmisc_1(k2_zfmisc_1(sK21,sK22)))
| ~ spl292_69 ),
inference(superposition,[],[f20554,f22477]) ).
fof(f22515,definition,
( spl292_77
<=> m1_subset_1(sK24,k1_zfmisc_1(k2_zfmisc_1(sK21,sK22))) ),
introduced(definition,[new_symbols(definition,[spl292_77])],[avatar_definition]) ).
fof(f22519,definition,
( spl292_78
<=> m1_subset_1(sF287,k1_zfmisc_1(sK22)) ),
introduced(definition,[new_symbols(definition,[spl292_78])],[avatar_definition]) ).
fof(f22521,plain,
( m1_subset_1(sF287,k1_zfmisc_1(sK22))
| ~ spl292_78 ),
inference(avatar_component_clause,[],[f22519]) ).
fof(f22522,plain,
( ~ spl292_77
| ~ spl292_75
| spl292_78
| ~ spl292_69 ),
inference(avatar_split_clause,[],[f22513,f22475,f22519,f22505,f22515]) ).
fof(f22523,plain,
( k1_zfmisc_1(sK21) != sF291
| m1_subset_1(sK23,k1_zfmisc_1(sK21))
| ~ m1_subset_1(sK23,sF291) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f22524,plain,
( k2_zfmisc_1(sK21,sK22) != sF284
| k1_zfmisc_1(sF284) != sF290
| m1_subset_1(sK24,k1_zfmisc_1(k2_zfmisc_1(sK21,sK22)))
| ~ m1_subset_1(sK24,sF290) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f22525,plain,
( m1_subset_1(sF288,k1_zfmisc_1(sK22))
| ~ m1_subset_1(sK23,k1_zfmisc_1(sK21))
| ~ m1_subset_1(sK25,k1_zfmisc_1(k2_zfmisc_1(sK21,sK22)))
| ~ spl292_70 ),
inference(superposition,[],[f20554,f22482]) ).
fof(f22527,definition,
( spl292_79
<=> m1_subset_1(sK25,k1_zfmisc_1(k2_zfmisc_1(sK21,sK22))) ),
introduced(definition,[new_symbols(definition,[spl292_79])],[avatar_definition]) ).
fof(f22531,definition,
( spl292_80
<=> m1_subset_1(sF288,k1_zfmisc_1(sK22)) ),
introduced(definition,[new_symbols(definition,[spl292_80])],[avatar_definition]) ).
fof(f22533,plain,
( m1_subset_1(sF288,k1_zfmisc_1(sK22))
| ~ spl292_80 ),
inference(avatar_component_clause,[],[f22531]) ).
fof(f22534,plain,
( ~ spl292_79
| ~ spl292_75
| spl292_80
| ~ spl292_70 ),
inference(avatar_split_clause,[],[f22525,f22480,f22531,f22505,f22527]) ).
fof(f22535,plain,
( k2_zfmisc_1(sK21,sK22) != sF284
| k1_zfmisc_1(sF284) != sF290
| m1_subset_1(sK25,k1_zfmisc_1(k2_zfmisc_1(sK21,sK22)))
| ~ m1_subset_1(sK25,sF290) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f22538,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF284))
| v1_relat_1(X0) )
| ~ spl292_66 ),
inference(superposition,[],[f20502,f22462]) ).
fof(f22545,plain,
( sF289 = k3_xboole_0(sF287,sF288)
| ~ m1_subset_1(sF287,k1_zfmisc_1(sK22))
| ~ m1_subset_1(sF288,k1_zfmisc_1(sK22))
| ~ spl292_71 ),
inference(superposition,[],[f22487,f20538]) ).
fof(f22546,plain,
( sF285 = k3_xboole_0(sK24,sK25)
| ~ m1_subset_1(sK24,k1_zfmisc_1(sF284))
| ~ m1_subset_1(sK25,k1_zfmisc_1(sF284))
| ~ spl292_67 ),
inference(superposition,[],[f22467,f20538]) ).
fof(f22548,plain,
! [X2,X0,X1] :
( k3_xboole_0(X0,X1) = k5_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,[],[f20540,f20538]) ).
fof(f22549,plain,
! [X2,X0,X1] :
( k3_xboole_0(X0,X1) = k5_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,[],[f22548]) ).
fof(f22553,plain,
( ~ m1_subset_1(sK24,sF290)
| sF285 = k3_xboole_0(sK24,sK25)
| ~ m1_subset_1(sK25,k1_zfmisc_1(sF284))
| ~ spl292_67
| ~ spl292_72 ),
inference(forward_demodulation,[],[f22546,f22492]) ).
fof(f22554,plain,
( sF289 = k3_xboole_0(sF287,sF288)
| ~ m1_subset_1(sF288,k1_zfmisc_1(sK22))
| ~ spl292_71
| ~ spl292_78 ),
inference(forward_subsumption_resolution,[],[f22545,f22521]) ).
fof(f22557,plain,
( sF285 = k3_xboole_0(sK24,sK25)
| ~ m1_subset_1(sK25,k1_zfmisc_1(sF284))
| ~ spl292_63
| ~ spl292_67
| ~ spl292_72 ),
inference(forward_subsumption_resolution,[],[f22553,f22447]) ).
fof(f22558,plain,
( sF289 = k3_xboole_0(sF287,sF288)
| ~ spl292_71
| ~ spl292_78
| ~ spl292_80 ),
inference(forward_subsumption_resolution,[],[f22554,f22533]) ).
fof(f22561,plain,
( ~ m1_subset_1(sK25,sF290)
| sF285 = k3_xboole_0(sK24,sK25)
| ~ spl292_63
| ~ spl292_67
| ~ spl292_72 ),
inference(forward_demodulation,[],[f22557,f22492]) ).
fof(f22563,definition,
( spl292_81
<=> sF289 = k3_xboole_0(sF287,sF288) ),
introduced(definition,[new_symbols(definition,[spl292_81])],[avatar_definition]) ).
fof(f22565,plain,
( sF289 = k3_xboole_0(sF287,sF288)
| ~ spl292_81 ),
inference(avatar_component_clause,[],[f22563]) ).
fof(f22566,plain,
( spl292_81
| ~ spl292_71
| ~ spl292_78
| ~ spl292_80 ),
inference(avatar_split_clause,[],[f22558,f22531,f22519,f22485,f22563]) ).
fof(f22568,plain,
( sF285 = k3_xboole_0(sK24,sK25)
| ~ spl292_63
| ~ spl292_64
| ~ spl292_67
| ~ spl292_72 ),
inference(forward_subsumption_resolution,[],[f22561,f22452]) ).
fof(f22571,definition,
( spl292_82
<=> sF285 = k3_xboole_0(sK24,sK25) ),
introduced(definition,[new_symbols(definition,[spl292_82])],[avatar_definition]) ).
fof(f22573,plain,
( sF285 = k3_xboole_0(sK24,sK25)
| ~ spl292_82 ),
inference(avatar_component_clause,[],[f22571]) ).
fof(f22574,plain,
( spl292_82
| ~ spl292_63
| ~ spl292_64
| ~ spl292_67
| ~ spl292_72 ),
inference(avatar_split_clause,[],[f22568,f22490,f22465,f22450,f22445,f22571]) ).
fof(f22575,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF290)
| v1_relat_1(X0) )
| ~ spl292_66
| ~ spl292_72 ),
inference(forward_demodulation,[],[f22538,f22492]) ).
fof(f22576,plain,
( v1_relat_1(sK24)
| ~ spl292_63
| ~ spl292_66
| ~ spl292_72 ),
inference(resolution,[],[f22575,f22447]) ).
fof(f22577,plain,
( v1_relat_1(sK25)
| ~ spl292_64
| ~ spl292_66
| ~ spl292_72 ),
inference(resolution,[],[f22575,f22452]) ).
fof(f22579,definition,
( spl292_83
<=> v1_relat_1(sK25) ),
introduced(definition,[new_symbols(definition,[spl292_83])],[avatar_definition]) ).
fof(f22581,plain,
( v1_relat_1(sK25)
| ~ spl292_83 ),
inference(avatar_component_clause,[],[f22579]) ).
fof(f22582,plain,
( spl292_83
| ~ spl292_64
| ~ spl292_66
| ~ spl292_72 ),
inference(avatar_split_clause,[],[f22577,f22490,f22460,f22450,f22579]) ).
fof(f22584,definition,
( spl292_84
<=> v1_relat_1(sK24) ),
introduced(definition,[new_symbols(definition,[spl292_84])],[avatar_definition]) ).
fof(f22586,plain,
( v1_relat_1(sK24)
| ~ spl292_84 ),
inference(avatar_component_clause,[],[f22584]) ).
fof(f22587,plain,
( spl292_84
| ~ spl292_63
| ~ spl292_66
| ~ spl292_72 ),
inference(avatar_split_clause,[],[f22576,f22490,f22460,f22445,f22584]) ).
fof(f22588,plain,
( ~ m1_subset_1(sF285,k1_zfmisc_1(sF284))
| ~ spl292_66
| spl292_74 ),
inference(forward_demodulation,[],[f22503,f22462]) ).
fof(f22589,plain,
( ~ m1_subset_1(sF285,sF290)
| ~ spl292_66
| ~ spl292_72
| spl292_74 ),
inference(forward_demodulation,[],[f22588,f22492]) ).
fof(f22591,definition,
( spl292_85
<=> m1_subset_1(sF285,sF290) ),
introduced(definition,[new_symbols(definition,[spl292_85])],[avatar_definition]) ).
fof(f22592,plain,
( m1_subset_1(sF285,sF290)
| ~ spl292_85 ),
inference(avatar_component_clause,[],[f22591]) ).
fof(f22594,plain,
( ~ spl292_85
| ~ spl292_66
| ~ spl292_72
| spl292_74 ),
inference(avatar_split_clause,[],[f22589,f22501,f22490,f22460,f22591]) ).
fof(f22597,plain,
( m1_subset_1(sF285,k1_zfmisc_1(sF284))
| ~ m1_subset_1(sK24,k1_zfmisc_1(sF284))
| ~ m1_subset_1(sK25,k1_zfmisc_1(sF284))
| ~ spl292_67 ),
inference(superposition,[],[f20541,f22467]) ).
fof(f22606,plain,
( m1_subset_1(sF285,sF290)
| ~ m1_subset_1(sK24,k1_zfmisc_1(sF284))
| ~ m1_subset_1(sK25,k1_zfmisc_1(sF284))
| ~ spl292_67
| ~ spl292_72 ),
inference(forward_demodulation,[],[f22597,f22492]) ).
fof(f22608,plain,
( ~ m1_subset_1(sK24,sF290)
| m1_subset_1(sF285,sF290)
| ~ m1_subset_1(sK25,k1_zfmisc_1(sF284))
| ~ spl292_67
| ~ spl292_72 ),
inference(forward_demodulation,[],[f22606,f22492]) ).
fof(f22610,plain,
( m1_subset_1(sF285,sF290)
| ~ m1_subset_1(sK25,k1_zfmisc_1(sF284))
| ~ spl292_63
| ~ spl292_67
| ~ spl292_72 ),
inference(forward_subsumption_resolution,[],[f22608,f22447]) ).
fof(f22616,plain,
( ~ m1_subset_1(sK25,sF290)
| m1_subset_1(sF285,sF290)
| ~ spl292_63
| ~ spl292_67
| ~ spl292_72 ),
inference(forward_demodulation,[],[f22610,f22492]) ).
fof(f22617,plain,
( m1_subset_1(sF285,sF290)
| ~ spl292_63
| ~ spl292_64
| ~ spl292_67
| ~ spl292_72 ),
inference(forward_subsumption_resolution,[],[f22616,f22452]) ).
fof(f22618,plain,
( spl292_85
| ~ spl292_63
| ~ spl292_64
| ~ spl292_67
| ~ spl292_72 ),
inference(avatar_split_clause,[],[f22617,f22490,f22465,f22450,f22445,f22591]) ).
fof(f22622,plain,
( v1_relat_1(sF285)
| ~ spl292_66
| ~ spl292_72
| ~ spl292_85 ),
inference(resolution,[],[f22592,f22575]) ).
fof(f22624,definition,
( spl292_87
<=> v1_relat_1(sF285) ),
introduced(definition,[new_symbols(definition,[spl292_87])],[avatar_definition]) ).
fof(f22626,plain,
( v1_relat_1(sF285)
| ~ spl292_87 ),
inference(avatar_component_clause,[],[f22624]) ).
fof(f22627,plain,
( spl292_87
| ~ spl292_66
| ~ spl292_72
| ~ spl292_85 ),
inference(avatar_split_clause,[],[f22622,f22591,f22490,f22460,f22624]) ).
fof(f22633,plain,
! [X2,X3,X0,X1,X4] :
( ~ r2_hidden(X0,k8_relset_2(X1,X2,X3,X4))
| m1_subset_1(X0,X2)
| ~ m1_subset_1(X3,k1_zfmisc_1(X1))
| ~ m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X1,X2))) ),
inference(resolution,[],[f20815,f20554]) ).
fof(f22634,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF286)
| m1_subset_1(X0,sK22) )
| ~ spl292_76 ),
inference(resolution,[],[f20815,f22511]) ).
fof(f22908,plain,
! [X2,X3,X0,X1,X4,X5] :
( r2_hidden(sK41(k8_relset_2(X2,X3,X1,X4),X5),k9_relat_1(X4,k1_tarski(X0)))
| ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X2,X3)))
| ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| r1_tarski(k8_relset_2(X2,X3,X1,X4),X5) ),
inference(resolution,[],[f20553,f20614]) ).
fof(f22910,plain,
( ! [X0,X1] :
( ~ r2_hidden(X0,sF287)
| ~ r2_hidden(X1,sK23)
| r2_hidden(X0,k9_relat_1(sK24,k1_tarski(X1)))
| ~ m1_subset_1(sK24,k1_zfmisc_1(k2_zfmisc_1(sK21,sK22)))
| ~ m1_subset_1(sK23,k1_zfmisc_1(sK21)) )
| ~ spl292_69 ),
inference(superposition,[],[f20553,f22477]) ).
fof(f22911,plain,
( ! [X0,X1] :
( ~ r2_hidden(X0,sF288)
| ~ r2_hidden(X1,sK23)
| r2_hidden(X0,k9_relat_1(sK25,k1_tarski(X1)))
| ~ m1_subset_1(sK25,k1_zfmisc_1(k2_zfmisc_1(sK21,sK22)))
| ~ m1_subset_1(sK23,k1_zfmisc_1(sK21)) )
| ~ spl292_70 ),
inference(superposition,[],[f20553,f22482]) ).
fof(f22920,plain,
( ! [X0,X1] :
( ~ m1_subset_1(sK25,k1_zfmisc_1(sF284))
| ~ r2_hidden(X0,sF288)
| ~ r2_hidden(X1,sK23)
| r2_hidden(X0,k9_relat_1(sK25,k1_tarski(X1)))
| ~ m1_subset_1(sK23,k1_zfmisc_1(sK21)) )
| ~ spl292_66
| ~ spl292_70 ),
inference(forward_demodulation,[],[f22911,f22462]) ).
fof(f22921,plain,
( ! [X0,X1] :
( ~ m1_subset_1(sK24,k1_zfmisc_1(sF284))
| ~ r2_hidden(X0,sF287)
| ~ r2_hidden(X1,sK23)
| r2_hidden(X0,k9_relat_1(sK24,k1_tarski(X1)))
| ~ m1_subset_1(sK23,k1_zfmisc_1(sK21)) )
| ~ spl292_66
| ~ spl292_69 ),
inference(forward_demodulation,[],[f22910,f22462]) ).
fof(f22927,plain,
( ! [X0,X1] :
( ~ m1_subset_1(sK25,sF290)
| ~ r2_hidden(X0,sF288)
| ~ r2_hidden(X1,sK23)
| r2_hidden(X0,k9_relat_1(sK25,k1_tarski(X1)))
| ~ m1_subset_1(sK23,k1_zfmisc_1(sK21)) )
| ~ spl292_66
| ~ spl292_70
| ~ spl292_72 ),
inference(forward_demodulation,[],[f22920,f22492]) ).
fof(f22928,plain,
( ! [X0,X1] :
( ~ m1_subset_1(sK24,sF290)
| ~ r2_hidden(X0,sF287)
| ~ r2_hidden(X1,sK23)
| r2_hidden(X0,k9_relat_1(sK24,k1_tarski(X1)))
| ~ m1_subset_1(sK23,k1_zfmisc_1(sK21)) )
| ~ spl292_66
| ~ spl292_69
| ~ spl292_72 ),
inference(forward_demodulation,[],[f22921,f22492]) ).
fof(f22934,plain,
( ! [X0,X1] :
( ~ r2_hidden(X0,sF288)
| ~ r2_hidden(X1,sK23)
| r2_hidden(X0,k9_relat_1(sK25,k1_tarski(X1)))
| ~ m1_subset_1(sK23,k1_zfmisc_1(sK21)) )
| ~ spl292_64
| ~ spl292_66
| ~ spl292_70
| ~ spl292_72 ),
inference(forward_subsumption_resolution,[],[f22927,f22452]) ).
fof(f22935,plain,
( ! [X0,X1] :
( ~ r2_hidden(X0,sF287)
| ~ r2_hidden(X1,sK23)
| r2_hidden(X0,k9_relat_1(sK24,k1_tarski(X1)))
| ~ m1_subset_1(sK23,k1_zfmisc_1(sK21)) )
| ~ spl292_63
| ~ spl292_66
| ~ spl292_69
| ~ spl292_72 ),
inference(forward_subsumption_resolution,[],[f22928,f22447]) ).
fof(f22941,plain,
( ! [X0,X1] :
( ~ m1_subset_1(sK23,sF291)
| ~ r2_hidden(X0,sF288)
| ~ r2_hidden(X1,sK23)
| r2_hidden(X0,k9_relat_1(sK25,k1_tarski(X1))) )
| ~ spl292_64
| ~ spl292_66
| ~ spl292_70
| ~ spl292_72
| ~ spl292_73 ),
inference(forward_demodulation,[],[f22934,f22497]) ).
fof(f22942,plain,
( ! [X0,X1] :
( ~ m1_subset_1(sK23,sF291)
| ~ r2_hidden(X0,sF287)
| ~ r2_hidden(X1,sK23)
| r2_hidden(X0,k9_relat_1(sK24,k1_tarski(X1))) )
| ~ spl292_63
| ~ spl292_66
| ~ spl292_69
| ~ spl292_72
| ~ spl292_73 ),
inference(forward_demodulation,[],[f22935,f22497]) ).
fof(f22944,plain,
( ! [X0,X1] :
( r2_hidden(X0,k9_relat_1(sK25,k1_tarski(X1)))
| ~ r2_hidden(X1,sK23)
| ~ r2_hidden(X0,sF288) )
| ~ spl292_62
| ~ spl292_64
| ~ spl292_66
| ~ spl292_70
| ~ spl292_72
| ~ spl292_73 ),
inference(forward_subsumption_resolution,[],[f22941,f22442]) ).
fof(f22945,plain,
( ! [X0,X1] :
( r2_hidden(X0,k9_relat_1(sK24,k1_tarski(X1)))
| ~ r2_hidden(X1,sK23)
| ~ r2_hidden(X0,sF287) )
| ~ spl292_62
| ~ spl292_63
| ~ spl292_66
| ~ spl292_69
| ~ spl292_72
| ~ spl292_73 ),
inference(forward_subsumption_resolution,[],[f22942,f22442]) ).
fof(f22949,plain,
( ! [X0,X1] :
( ~ r2_hidden(X0,sK23)
| ~ r2_hidden(X1,sF287)
| r2_hidden(k4_tarski(X0,X1),sK24)
| ~ v1_relat_1(sK24) )
| ~ spl292_62
| ~ spl292_63
| ~ spl292_66
| ~ spl292_69
| ~ spl292_72
| ~ spl292_73 ),
inference(resolution,[],[f22945,f20893]) ).
fof(f22951,definition,
( spl292_90
<=> ! [X0,X1] :
( ~ r2_hidden(X0,sK23)
| r2_hidden(k4_tarski(X0,X1),sK24)
| ~ r2_hidden(X1,sF287) ) ),
introduced(definition,[new_symbols(definition,[spl292_90])],[avatar_definition]) ).
fof(f22952,plain,
( ! [X0,X1] :
( r2_hidden(k4_tarski(X0,X1),sK24)
| ~ r2_hidden(X0,sK23)
| ~ r2_hidden(X1,sF287) )
| ~ spl292_90 ),
inference(avatar_component_clause,[],[f22951]) ).
fof(f22953,plain,
( ~ spl292_84
| spl292_90
| ~ spl292_62
| ~ spl292_63
| ~ spl292_66
| ~ spl292_69
| ~ spl292_72
| ~ spl292_73 ),
inference(avatar_split_clause,[],[f22949,f22495,f22490,f22475,f22460,f22445,f22440,f22951,f22584]) ).
fof(f22956,plain,
( ! [X0,X1] :
( ~ r2_hidden(X0,sK23)
| ~ r2_hidden(X1,sF288)
| r2_hidden(k4_tarski(X0,X1),sK25)
| ~ v1_relat_1(sK25) )
| ~ spl292_62
| ~ spl292_64
| ~ spl292_66
| ~ spl292_70
| ~ spl292_72
| ~ spl292_73 ),
inference(resolution,[],[f22944,f20893]) ).
fof(f22958,definition,
( spl292_91
<=> ! [X0,X1] :
( ~ r2_hidden(X0,sK23)
| r2_hidden(k4_tarski(X0,X1),sK25)
| ~ r2_hidden(X1,sF288) ) ),
introduced(definition,[new_symbols(definition,[spl292_91])],[avatar_definition]) ).
fof(f22959,plain,
( ! [X0,X1] :
( r2_hidden(k4_tarski(X0,X1),sK25)
| ~ r2_hidden(X0,sK23)
| ~ r2_hidden(X1,sF288) )
| ~ spl292_91 ),
inference(avatar_component_clause,[],[f22958]) ).
fof(f22960,plain,
( ~ spl292_83
| spl292_91
| ~ spl292_62
| ~ spl292_64
| ~ spl292_66
| ~ spl292_70
| ~ spl292_72
| ~ spl292_73 ),
inference(avatar_split_clause,[],[f22956,f22495,f22490,f22480,f22460,f22450,f22440,f22958,f22579]) ).
fof(f23010,plain,
( sF289 = k3_xboole_0(sF288,sF287)
| ~ m1_subset_1(sF288,k1_zfmisc_1(sK22))
| ~ m1_subset_1(sF287,k1_zfmisc_1(sK22))
| ~ spl292_71 ),
inference(superposition,[],[f22487,f22549]) ).
fof(f23011,plain,
( sF285 = k3_xboole_0(sK25,sK24)
| ~ m1_subset_1(sK25,k1_zfmisc_1(sF284))
| ~ m1_subset_1(sK24,k1_zfmisc_1(sF284))
| ~ spl292_67 ),
inference(superposition,[],[f22467,f22549]) ).
fof(f23027,plain,
( ~ m1_subset_1(sK25,sF290)
| sF285 = k3_xboole_0(sK25,sK24)
| ~ m1_subset_1(sK24,k1_zfmisc_1(sF284))
| ~ spl292_67
| ~ spl292_72 ),
inference(forward_demodulation,[],[f23011,f22492]) ).
fof(f23028,plain,
( sF289 = k3_xboole_0(sF288,sF287)
| ~ m1_subset_1(sF287,k1_zfmisc_1(sK22))
| ~ spl292_71
| ~ spl292_80 ),
inference(forward_subsumption_resolution,[],[f23010,f22533]) ).
fof(f23033,plain,
( sF285 = k3_xboole_0(sK25,sK24)
| ~ m1_subset_1(sK24,k1_zfmisc_1(sF284))
| ~ spl292_64
| ~ spl292_67
| ~ spl292_72 ),
inference(forward_subsumption_resolution,[],[f23027,f22452]) ).
fof(f23034,plain,
( sF289 = k3_xboole_0(sF288,sF287)
| ~ spl292_71
| ~ spl292_78
| ~ spl292_80 ),
inference(forward_subsumption_resolution,[],[f23028,f22521]) ).
fof(f23038,plain,
( ~ m1_subset_1(sK24,sF290)
| sF285 = k3_xboole_0(sK25,sK24)
| ~ spl292_64
| ~ spl292_67
| ~ spl292_72 ),
inference(forward_demodulation,[],[f23033,f22492]) ).
fof(f23040,definition,
( spl292_99
<=> sF289 = k3_xboole_0(sF288,sF287) ),
introduced(definition,[new_symbols(definition,[spl292_99])],[avatar_definition]) ).
fof(f23042,plain,
( sF289 = k3_xboole_0(sF288,sF287)
| ~ spl292_99 ),
inference(avatar_component_clause,[],[f23040]) ).
fof(f23043,plain,
( spl292_99
| ~ spl292_71
| ~ spl292_78
| ~ spl292_80 ),
inference(avatar_split_clause,[],[f23034,f22531,f22519,f22485,f23040]) ).
fof(f23045,plain,
( sF285 = k3_xboole_0(sK25,sK24)
| ~ spl292_63
| ~ spl292_64
| ~ spl292_67
| ~ spl292_72 ),
inference(forward_subsumption_resolution,[],[f23038,f22447]) ).
fof(f23048,definition,
( spl292_100
<=> sF285 = k3_xboole_0(sK25,sK24) ),
introduced(definition,[new_symbols(definition,[spl292_100])],[avatar_definition]) ).
fof(f23050,plain,
( sF285 = k3_xboole_0(sK25,sK24)
| ~ spl292_100 ),
inference(avatar_component_clause,[],[f23048]) ).
fof(f23051,plain,
( spl292_100
| ~ spl292_63
| ~ spl292_64
| ~ spl292_67
| ~ spl292_72 ),
inference(avatar_split_clause,[],[f23045,f22490,f22465,f22450,f22445,f23048]) ).
fof(f23231,definition,
( spl292_103
<=> v1_xboole_0(sK22) ),
introduced(definition,[new_symbols(definition,[spl292_103])],[avatar_definition]) ).
fof(f23232,plain,
( ~ v1_xboole_0(sK22)
| spl292_103 ),
inference(avatar_component_clause,[],[f23231]) ).
fof(f23472,plain,
( ! [X0] :
( ~ r2_hidden(X0,sK25)
| ~ r2_hidden(X0,sK24)
| r2_hidden(X0,sF285) )
| ~ spl292_82 ),
inference(superposition,[],[f22003,f22573]) ).
fof(f23474,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF288)
| ~ r2_hidden(X0,sF287)
| r2_hidden(X0,sF289) )
| ~ spl292_81 ),
inference(superposition,[],[f22003,f22565]) ).
fof(f23477,plain,
( ! [X0,X1] :
( ~ r2_hidden(k4_tarski(X0,X1),sK24)
| r2_hidden(k4_tarski(X0,X1),sF285)
| ~ r2_hidden(X0,sK23)
| ~ r2_hidden(X1,sF288) )
| ~ spl292_82
| ~ spl292_91 ),
inference(resolution,[],[f23472,f22959]) ).
fof(f23509,plain,
( ! [X0,X1] :
( r2_hidden(k4_tarski(X0,X1),sF285)
| ~ r2_hidden(X0,sK23)
| ~ r2_hidden(X1,sF288)
| ~ r2_hidden(X0,sK23)
| ~ r2_hidden(X1,sF287) )
| ~ spl292_82
| ~ spl292_90
| ~ spl292_91 ),
inference(resolution,[],[f23477,f22952]) ).
fof(f23512,plain,
( ! [X0,X1] :
( r2_hidden(k4_tarski(X0,X1),sF285)
| ~ r2_hidden(X0,sK23)
| ~ r2_hidden(X1,sF288)
| ~ r2_hidden(X1,sF287) )
| ~ spl292_82
| ~ spl292_90
| ~ spl292_91 ),
inference(duplicate_literal_removal,[],[f23509]) ).
fof(f23515,plain,
( ! [X2,X0,X1] :
( ~ r2_hidden(X0,sK23)
| ~ r2_hidden(X1,sF288)
| ~ r2_hidden(X1,sF287)
| r2_hidden(X1,k9_relat_1(sF285,X2))
| ~ r2_hidden(X0,X2)
| ~ v1_relat_1(sF285) )
| ~ spl292_82
| ~ spl292_90
| ~ spl292_91 ),
inference(resolution,[],[f23512,f22012]) ).
fof(f23518,plain,
( ! [X2,X0,X1] :
( r2_hidden(X1,k9_relat_1(sF285,X2))
| ~ r2_hidden(X1,sF288)
| ~ r2_hidden(X1,sF287)
| ~ r2_hidden(X0,sK23)
| ~ r2_hidden(X0,X2) )
| ~ spl292_82
| ~ spl292_87
| ~ spl292_90
| ~ spl292_91 ),
inference(forward_subsumption_resolution,[],[f23515,f22626]) ).
fof(f23526,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ r2_hidden(X1,k1_tarski(sK28(X2,X0,sF285)))
| ~ r2_hidden(X0,sF287)
| ~ r2_hidden(X1,sK23)
| ~ r2_hidden(X0,sF288)
| r2_hidden(X0,k8_relset_2(X3,X4,X2,sF285))
| ~ m1_subset_1(sF285,k1_zfmisc_1(k2_zfmisc_1(X3,X4)))
| ~ m1_subset_1(X0,X4)
| ~ m1_subset_1(X2,k1_zfmisc_1(X3))
| v1_xboole_0(X4) )
| ~ spl292_82
| ~ spl292_87
| ~ spl292_90
| ~ spl292_91 ),
inference(resolution,[],[f23518,f20552]) ).
fof(f23855,plain,
! [X2,X3,X0,X1,X4] :
( r2_hidden(sK28(X0,sK41(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(sK41(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,[],[f20551,f20615]) ).
fof(f23858,plain,
( ! [X0] :
( r2_hidden(X0,sF287)
| r2_hidden(sK28(sK23,X0,sK24),sK23)
| ~ m1_subset_1(sK24,k1_zfmisc_1(k2_zfmisc_1(sK21,sK22)))
| ~ m1_subset_1(X0,sK22)
| ~ m1_subset_1(sK23,k1_zfmisc_1(sK21))
| v1_xboole_0(sK22) )
| ~ spl292_69 ),
inference(superposition,[],[f20551,f22477]) ).
fof(f23859,plain,
( ! [X0] :
( r2_hidden(X0,sF288)
| r2_hidden(sK28(sK23,X0,sK25),sK23)
| ~ m1_subset_1(sK25,k1_zfmisc_1(k2_zfmisc_1(sK21,sK22)))
| ~ m1_subset_1(X0,sK22)
| ~ m1_subset_1(sK23,k1_zfmisc_1(sK21))
| v1_xboole_0(sK22) )
| ~ spl292_70 ),
inference(superposition,[],[f20551,f22482]) ).
fof(f24769,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF285)
| r2_hidden(X0,sK24) )
| ~ spl292_82 ),
inference(superposition,[],[f22004,f22573]) ).
fof(f24770,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF285)
| r2_hidden(X0,sK25) )
| ~ spl292_100 ),
inference(superposition,[],[f22004,f23050]) ).
fof(f24771,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF289)
| r2_hidden(X0,sF287) )
| ~ spl292_81 ),
inference(superposition,[],[f22004,f22565]) ).
fof(f24772,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF289)
| r2_hidden(X0,sF288) )
| ~ spl292_99 ),
inference(superposition,[],[f22004,f23042]) ).
fof(f24788,plain,
( ! [X0] :
( r2_hidden(sK41(sF289,X0),sF287)
| r1_tarski(sF289,X0) )
| ~ spl292_81 ),
inference(resolution,[],[f24771,f20614]) ).
fof(f24871,plain,
( ! [X0] :
( r2_hidden(sK41(sF289,X0),sF288)
| r1_tarski(sF289,X0) )
| ~ spl292_99 ),
inference(resolution,[],[f24772,f20614]) ).
fof(f26281,plain,
( ! [X0,X1] :
( r2_hidden(sK41(sF286,X0),k9_relat_1(sF285,k1_tarski(X1)))
| ~ r2_hidden(X1,sK23)
| ~ m1_subset_1(sF285,k1_zfmisc_1(k2_zfmisc_1(sK21,sK22)))
| ~ m1_subset_1(sK23,k1_zfmisc_1(sK21))
| r1_tarski(sF286,X0) )
| ~ spl292_68 ),
inference(superposition,[],[f22908,f22472]) ).
fof(f26318,plain,
( ! [X0,X1] :
( ~ m1_subset_1(sF285,k1_zfmisc_1(sF284))
| r2_hidden(sK41(sF286,X0),k9_relat_1(sF285,k1_tarski(X1)))
| ~ r2_hidden(X1,sK23)
| ~ m1_subset_1(sK23,k1_zfmisc_1(sK21))
| r1_tarski(sF286,X0) )
| ~ spl292_66
| ~ spl292_68 ),
inference(forward_demodulation,[],[f26281,f22462]) ).
fof(f26336,plain,
( ! [X0,X1] :
( ~ m1_subset_1(sF285,sF290)
| r2_hidden(sK41(sF286,X0),k9_relat_1(sF285,k1_tarski(X1)))
| ~ r2_hidden(X1,sK23)
| ~ m1_subset_1(sK23,k1_zfmisc_1(sK21))
| r1_tarski(sF286,X0) )
| ~ spl292_66
| ~ spl292_68
| ~ spl292_72 ),
inference(forward_demodulation,[],[f26318,f22492]) ).
fof(f26353,plain,
( ! [X0,X1] :
( r2_hidden(sK41(sF286,X0),k9_relat_1(sF285,k1_tarski(X1)))
| ~ r2_hidden(X1,sK23)
| ~ m1_subset_1(sK23,k1_zfmisc_1(sK21))
| r1_tarski(sF286,X0) )
| ~ spl292_66
| ~ spl292_68
| ~ spl292_72
| ~ spl292_85 ),
inference(forward_subsumption_resolution,[],[f26336,f22592]) ).
fof(f26370,plain,
( ! [X0,X1] :
( ~ m1_subset_1(sK23,sF291)
| r2_hidden(sK41(sF286,X0),k9_relat_1(sF285,k1_tarski(X1)))
| ~ r2_hidden(X1,sK23)
| r1_tarski(sF286,X0) )
| ~ spl292_66
| ~ spl292_68
| ~ spl292_72
| ~ spl292_73
| ~ spl292_85 ),
inference(forward_demodulation,[],[f26353,f22497]) ).
fof(f26375,plain,
( ! [X0,X1] :
( r2_hidden(sK41(sF286,X0),k9_relat_1(sF285,k1_tarski(X1)))
| ~ r2_hidden(X1,sK23)
| r1_tarski(sF286,X0) )
| ~ spl292_62
| ~ spl292_66
| ~ spl292_68
| ~ spl292_72
| ~ spl292_73
| ~ spl292_85 ),
inference(forward_subsumption_resolution,[],[f26370,f22442]) ).
fof(f26387,plain,
( ! [X0,X1] :
( ~ r2_hidden(X0,sK23)
| r1_tarski(sF286,X1)
| r2_hidden(k4_tarski(X0,sK41(sF286,X1)),sF285)
| ~ v1_relat_1(sF285) )
| ~ spl292_62
| ~ spl292_66
| ~ spl292_68
| ~ spl292_72
| ~ spl292_73
| ~ spl292_85 ),
inference(resolution,[],[f26375,f20893]) ).
fof(f26391,plain,
( ! [X0,X1] :
( r2_hidden(k4_tarski(X0,sK41(sF286,X1)),sF285)
| r1_tarski(sF286,X1)
| ~ r2_hidden(X0,sK23) )
| ~ spl292_62
| ~ spl292_66
| ~ spl292_68
| ~ spl292_72
| ~ spl292_73
| ~ spl292_85
| ~ spl292_87 ),
inference(forward_subsumption_resolution,[],[f26387,f22626]) ).
fof(f26394,plain,
( ! [X0,X1] :
( r2_hidden(k4_tarski(X1,sK41(sF286,X0)),sK25)
| ~ r2_hidden(X1,sK23)
| r1_tarski(sF286,X0) )
| ~ spl292_62
| ~ spl292_66
| ~ spl292_68
| ~ spl292_72
| ~ spl292_73
| ~ spl292_85
| ~ spl292_87
| ~ spl292_100 ),
inference(resolution,[],[f26391,f24770]) ).
fof(f26395,plain,
( ! [X0,X1] :
( r2_hidden(k4_tarski(X1,sK41(sF286,X0)),sK24)
| ~ r2_hidden(X1,sK23)
| r1_tarski(sF286,X0) )
| ~ spl292_62
| ~ spl292_66
| ~ spl292_68
| ~ spl292_72
| ~ spl292_73
| ~ spl292_82
| ~ spl292_85
| ~ spl292_87 ),
inference(resolution,[],[f26391,f24769]) ).
fof(f26407,plain,
( ! [X2,X0,X1] :
( ~ r2_hidden(X0,sK23)
| r1_tarski(sF286,X1)
| r2_hidden(sK41(sF286,X1),k9_relat_1(sK24,X2))
| ~ r2_hidden(X0,X2)
| ~ v1_relat_1(sK24) )
| ~ spl292_62
| ~ spl292_66
| ~ spl292_68
| ~ spl292_72
| ~ spl292_73
| ~ spl292_82
| ~ spl292_85
| ~ spl292_87 ),
inference(resolution,[],[f26395,f22012]) ).
fof(f26412,plain,
( ! [X2,X0,X1] :
( r2_hidden(sK41(sF286,X1),k9_relat_1(sK24,X2))
| r1_tarski(sF286,X1)
| ~ r2_hidden(X0,sK23)
| ~ r2_hidden(X0,X2) )
| ~ spl292_62
| ~ spl292_66
| ~ spl292_68
| ~ spl292_72
| ~ spl292_73
| ~ spl292_82
| ~ spl292_84
| ~ spl292_85
| ~ spl292_87 ),
inference(forward_subsumption_resolution,[],[f26407,f22586]) ).
fof(f26415,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ r2_hidden(X1,k1_tarski(sK28(X2,sK41(sF286,X0),sK24)))
| ~ r2_hidden(X1,sK23)
| r1_tarski(sF286,X0)
| r2_hidden(sK41(sF286,X0),k8_relset_2(X3,X4,X2,sK24))
| ~ m1_subset_1(sK24,k1_zfmisc_1(k2_zfmisc_1(X3,X4)))
| ~ m1_subset_1(sK41(sF286,X0),X4)
| ~ m1_subset_1(X2,k1_zfmisc_1(X3))
| v1_xboole_0(X4) )
| ~ spl292_62
| ~ spl292_66
| ~ spl292_68
| ~ spl292_72
| ~ spl292_73
| ~ spl292_82
| ~ spl292_84
| ~ spl292_85
| ~ spl292_87 ),
inference(resolution,[],[f26412,f20552]) ).
fof(f26419,plain,
( ! [X2,X0,X1] :
( ~ r2_hidden(X0,sK23)
| r1_tarski(sF286,X1)
| r2_hidden(sK41(sF286,X1),k9_relat_1(sK25,X2))
| ~ r2_hidden(X0,X2)
| ~ v1_relat_1(sK25) )
| ~ spl292_62
| ~ spl292_66
| ~ spl292_68
| ~ spl292_72
| ~ spl292_73
| ~ spl292_85
| ~ spl292_87
| ~ spl292_100 ),
inference(resolution,[],[f26394,f22012]) ).
fof(f26424,plain,
( ! [X2,X0,X1] :
( r2_hidden(sK41(sF286,X1),k9_relat_1(sK25,X2))
| r1_tarski(sF286,X1)
| ~ r2_hidden(X0,sK23)
| ~ r2_hidden(X0,X2) )
| ~ spl292_62
| ~ spl292_66
| ~ spl292_68
| ~ spl292_72
| ~ spl292_73
| ~ spl292_83
| ~ spl292_85
| ~ spl292_87
| ~ spl292_100 ),
inference(forward_subsumption_resolution,[],[f26419,f22581]) ).
fof(f26427,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ r2_hidden(X1,k1_tarski(sK28(X2,sK41(sF286,X0),sK25)))
| ~ r2_hidden(X1,sK23)
| r1_tarski(sF286,X0)
| r2_hidden(sK41(sF286,X0),k8_relset_2(X3,X4,X2,sK25))
| ~ m1_subset_1(sK25,k1_zfmisc_1(k2_zfmisc_1(X3,X4)))
| ~ m1_subset_1(sK41(sF286,X0),X4)
| ~ m1_subset_1(X2,k1_zfmisc_1(X3))
| v1_xboole_0(X4) )
| ~ spl292_62
| ~ spl292_66
| ~ spl292_68
| ~ spl292_72
| ~ spl292_73
| ~ spl292_83
| ~ spl292_85
| ~ spl292_87
| ~ spl292_100 ),
inference(resolution,[],[f26424,f20552]) ).
fof(f26486,plain,
( ! [X0] :
( m1_subset_1(sK41(sF286,X0),sK22)
| r1_tarski(sF286,X0) )
| ~ spl292_76 ),
inference(resolution,[],[f22634,f20614]) ).
fof(f28138,definition,
( spl292_367
<=> ! [X1] : ~ r2_hidden(X1,sF286) ),
introduced(definition,[new_symbols(definition,[spl292_367])],[avatar_definition]) ).
fof(f28139,plain,
( ! [X1] : ~ r2_hidden(X1,sF286)
| ~ spl292_367 ),
inference(avatar_component_clause,[],[f28138]) ).
fof(f28153,definition,
( spl292_370
<=> ! [X1] : ~ r2_hidden(X1,sF288) ),
introduced(definition,[new_symbols(definition,[spl292_370])],[avatar_definition]) ).
fof(f28154,plain,
( ! [X1] : ~ r2_hidden(X1,sF288)
| ~ spl292_370 ),
inference(avatar_component_clause,[],[f28153]) ).
fof(f28257,plain,
( ! [X0] :
( ~ m1_subset_1(sK25,k1_zfmisc_1(sF284))
| r2_hidden(X0,sF288)
| r2_hidden(sK28(sK23,X0,sK25),sK23)
| ~ m1_subset_1(X0,sK22)
| ~ m1_subset_1(sK23,k1_zfmisc_1(sK21))
| v1_xboole_0(sK22) )
| ~ spl292_66
| ~ spl292_70 ),
inference(forward_demodulation,[],[f23859,f22462]) ).
fof(f28258,plain,
( ! [X0] :
( ~ m1_subset_1(sK24,k1_zfmisc_1(sF284))
| r2_hidden(X0,sF287)
| r2_hidden(sK28(sK23,X0,sK24),sK23)
| ~ m1_subset_1(X0,sK22)
| ~ m1_subset_1(sK23,k1_zfmisc_1(sK21))
| v1_xboole_0(sK22) )
| ~ spl292_66
| ~ spl292_69 ),
inference(forward_demodulation,[],[f23858,f22462]) ).
fof(f28330,plain,
( ! [X0] :
( ~ m1_subset_1(sK25,sF290)
| r2_hidden(X0,sF288)
| r2_hidden(sK28(sK23,X0,sK25),sK23)
| ~ m1_subset_1(X0,sK22)
| ~ m1_subset_1(sK23,k1_zfmisc_1(sK21))
| v1_xboole_0(sK22) )
| ~ spl292_66
| ~ spl292_70
| ~ spl292_72 ),
inference(forward_demodulation,[],[f28257,f22492]) ).
fof(f28331,plain,
( ! [X0] :
( ~ m1_subset_1(sK24,sF290)
| r2_hidden(X0,sF287)
| r2_hidden(sK28(sK23,X0,sK24),sK23)
| ~ m1_subset_1(X0,sK22)
| ~ m1_subset_1(sK23,k1_zfmisc_1(sK21))
| v1_xboole_0(sK22) )
| ~ spl292_66
| ~ spl292_69
| ~ spl292_72 ),
inference(forward_demodulation,[],[f28258,f22492]) ).
fof(f28439,plain,
( ! [X0] :
( r2_hidden(X0,sF288)
| r2_hidden(sK28(sK23,X0,sK25),sK23)
| ~ m1_subset_1(X0,sK22)
| ~ m1_subset_1(sK23,k1_zfmisc_1(sK21))
| v1_xboole_0(sK22) )
| ~ spl292_64
| ~ spl292_66
| ~ spl292_70
| ~ spl292_72 ),
inference(forward_subsumption_resolution,[],[f28330,f22452]) ).
fof(f28440,plain,
( ! [X0] :
( r2_hidden(X0,sF287)
| r2_hidden(sK28(sK23,X0,sK24),sK23)
| ~ m1_subset_1(X0,sK22)
| ~ m1_subset_1(sK23,k1_zfmisc_1(sK21))
| v1_xboole_0(sK22) )
| ~ spl292_63
| ~ spl292_66
| ~ spl292_69
| ~ spl292_72 ),
inference(forward_subsumption_resolution,[],[f28331,f22447]) ).
fof(f28505,plain,
( ! [X0] :
( ~ m1_subset_1(sK23,sF291)
| r2_hidden(X0,sF288)
| r2_hidden(sK28(sK23,X0,sK25),sK23)
| ~ m1_subset_1(X0,sK22)
| v1_xboole_0(sK22) )
| ~ spl292_64
| ~ spl292_66
| ~ spl292_70
| ~ spl292_72
| ~ spl292_73 ),
inference(forward_demodulation,[],[f28439,f22497]) ).
fof(f28506,plain,
( ! [X0] :
( ~ m1_subset_1(sK23,sF291)
| r2_hidden(X0,sF287)
| r2_hidden(sK28(sK23,X0,sK24),sK23)
| ~ m1_subset_1(X0,sK22)
| v1_xboole_0(sK22) )
| ~ spl292_63
| ~ spl292_66
| ~ spl292_69
| ~ spl292_72
| ~ spl292_73 ),
inference(forward_demodulation,[],[f28440,f22497]) ).
fof(f28590,plain,
( ! [X0] :
( r2_hidden(X0,sF288)
| r2_hidden(sK28(sK23,X0,sK25),sK23)
| ~ m1_subset_1(X0,sK22)
| v1_xboole_0(sK22) )
| ~ spl292_62
| ~ spl292_64
| ~ spl292_66
| ~ spl292_70
| ~ spl292_72
| ~ spl292_73 ),
inference(forward_subsumption_resolution,[],[f28505,f22442]) ).
fof(f28591,plain,
( ! [X0] :
( r2_hidden(X0,sF287)
| r2_hidden(sK28(sK23,X0,sK24),sK23)
| ~ m1_subset_1(X0,sK22)
| v1_xboole_0(sK22) )
| ~ spl292_62
| ~ spl292_63
| ~ spl292_66
| ~ spl292_69
| ~ spl292_72
| ~ spl292_73 ),
inference(forward_subsumption_resolution,[],[f28506,f22442]) ).
fof(f28735,definition,
( spl292_439
<=> ! [X0] :
( r2_hidden(X0,sF288)
| ~ m1_subset_1(X0,sK22)
| r2_hidden(sK28(sK23,X0,sK25),sK23) ) ),
introduced(definition,[new_symbols(definition,[spl292_439])],[avatar_definition]) ).
fof(f28736,plain,
( ! [X0] :
( r2_hidden(sK28(sK23,X0,sK25),sK23)
| ~ m1_subset_1(X0,sK22)
| r2_hidden(X0,sF288) )
| ~ spl292_439 ),
inference(avatar_component_clause,[],[f28735]) ).
fof(f28737,plain,
( spl292_103
| spl292_439
| ~ spl292_62
| ~ spl292_64
| ~ spl292_66
| ~ spl292_70
| ~ spl292_72
| ~ spl292_73 ),
inference(avatar_split_clause,[],[f28590,f22495,f22490,f22480,f22460,f22450,f22440,f28735,f23231]) ).
fof(f28739,definition,
( spl292_440
<=> ! [X0] :
( r2_hidden(X0,sF287)
| ~ m1_subset_1(X0,sK22)
| r2_hidden(sK28(sK23,X0,sK24),sK23) ) ),
introduced(definition,[new_symbols(definition,[spl292_440])],[avatar_definition]) ).
fof(f28740,plain,
( ! [X0] :
( r2_hidden(sK28(sK23,X0,sK24),sK23)
| ~ m1_subset_1(X0,sK22)
| r2_hidden(X0,sF287) )
| ~ spl292_440 ),
inference(avatar_component_clause,[],[f28739]) ).
fof(f28741,plain,
( spl292_103
| spl292_440
| ~ spl292_62
| ~ spl292_63
| ~ spl292_66
| ~ spl292_69
| ~ spl292_72
| ~ spl292_73 ),
inference(avatar_split_clause,[],[f28591,f22495,f22490,f22475,f22460,f22445,f22440,f28739,f23231]) ).
fof(f29044,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF288)
| m1_subset_1(X0,sK22)
| ~ m1_subset_1(sK23,k1_zfmisc_1(sK21))
| ~ m1_subset_1(sK25,k1_zfmisc_1(k2_zfmisc_1(sK21,sK22))) )
| ~ spl292_70 ),
inference(superposition,[],[f22633,f22482]) ).
fof(f30313,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF286)
| ~ v1_xboole_0(sK22) )
| ~ spl292_76 ),
inference(resolution,[],[f20567,f22511]) ).
fof(f30315,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF288)
| ~ v1_xboole_0(sK22) )
| ~ spl292_80 ),
inference(resolution,[],[f20567,f22533]) ).
fof(f30340,plain,
( ~ spl292_103
| spl292_367
| ~ spl292_76 ),
inference(avatar_split_clause,[],[f30313,f22509,f28138,f23231]) ).
fof(f30397,plain,
( ! [X0] :
( r2_hidden(sK77(X0,sF286),X0)
| sF286 = X0 )
| ~ spl292_367 ),
inference(resolution,[],[f28139,f20827]) ).
fof(f30452,plain,
( sF286 = sF289
| r2_hidden(sK77(sF289,sF286),sF288)
| ~ spl292_99
| ~ spl292_367 ),
inference(resolution,[],[f30397,f24772]) ).
fof(f30456,plain,
( r2_hidden(sK77(sF289,sF286),sF288)
| spl292_65
| ~ spl292_99
| ~ spl292_367 ),
inference(forward_subsumption_resolution,[],[f30452,f22457]) ).
fof(f30609,plain,
( $false
| spl292_65
| ~ spl292_99
| ~ spl292_367
| ~ spl292_370 ),
inference(forward_subsumption_resolution,[],[f30456,f28154]) ).
fof(f30610,plain,
( spl292_65
| ~ spl292_99
| ~ spl292_367
| ~ spl292_370 ),
inference(avatar_contradiction_clause,[],[f30609]) ).
fof(f30672,plain,
( ! [X0] :
( ~ m1_subset_1(sK23,sF291)
| ~ r2_hidden(X0,sF288)
| m1_subset_1(X0,sK22)
| ~ m1_subset_1(sK25,k1_zfmisc_1(k2_zfmisc_1(sK21,sK22))) )
| ~ spl292_70
| ~ spl292_73 ),
inference(forward_demodulation,[],[f29044,f22497]) ).
fof(f30675,plain,
( ~ spl292_103
| spl292_370
| ~ spl292_80 ),
inference(avatar_split_clause,[],[f30315,f22531,f28153,f23231]) ).
fof(f30684,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF288)
| m1_subset_1(X0,sK22)
| ~ m1_subset_1(sK25,k1_zfmisc_1(k2_zfmisc_1(sK21,sK22))) )
| ~ spl292_62
| ~ spl292_70
| ~ spl292_73 ),
inference(forward_subsumption_resolution,[],[f30672,f22442]) ).
fof(f30694,plain,
( ! [X0] :
( ~ m1_subset_1(sK25,k1_zfmisc_1(sF284))
| ~ r2_hidden(X0,sF288)
| m1_subset_1(X0,sK22) )
| ~ spl292_62
| ~ spl292_66
| ~ spl292_70
| ~ spl292_73 ),
inference(forward_demodulation,[],[f30684,f22462]) ).
fof(f30704,plain,
( ! [X0] :
( ~ m1_subset_1(sK25,sF290)
| ~ r2_hidden(X0,sF288)
| m1_subset_1(X0,sK22) )
| ~ spl292_62
| ~ spl292_66
| ~ spl292_70
| ~ spl292_72
| ~ spl292_73 ),
inference(forward_demodulation,[],[f30694,f22492]) ).
fof(f30729,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF288)
| m1_subset_1(X0,sK22) )
| ~ spl292_62
| ~ spl292_64
| ~ spl292_66
| ~ spl292_70
| ~ spl292_72
| ~ spl292_73 ),
inference(forward_subsumption_resolution,[],[f30704,f22452]) ).
fof(f30731,definition,
( spl292_579
<=> ! [X0] :
( m1_subset_1(X0,sK22)
| ~ r2_hidden(X0,sF288) ) ),
introduced(definition,[new_symbols(definition,[spl292_579])],[avatar_definition]) ).
fof(f30732,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF288)
| m1_subset_1(X0,sK22) )
| ~ spl292_579 ),
inference(avatar_component_clause,[],[f30731]) ).
fof(f30747,plain,
( spl292_579
| ~ spl292_62
| ~ spl292_64
| ~ spl292_66
| ~ spl292_70
| ~ spl292_72
| ~ spl292_73 ),
inference(avatar_split_clause,[],[f30729,f22495,f22490,f22480,f22460,f22450,f22440,f30731]) ).
fof(f33587,definition,
( spl292_748
<=> r1_tarski(sF289,sF286) ),
introduced(definition,[new_symbols(definition,[spl292_748])],[avatar_definition]) ).
fof(f33589,plain,
( r1_tarski(sF289,sF286)
| ~ spl292_748 ),
inference(avatar_component_clause,[],[f33587]) ).
fof(f33594,plain,
( ~ r1_tarski(sF286,sF289)
| sF286 = sF289
| ~ spl292_748 ),
inference(resolution,[],[f33589,f20611]) ).
fof(f33595,plain,
( ~ r1_tarski(sF286,sF289)
| spl292_65
| ~ spl292_748 ),
inference(forward_subsumption_resolution,[],[f33594,f22457]) ).
fof(f33598,definition,
( spl292_749
<=> r1_tarski(sF286,sF289) ),
introduced(definition,[new_symbols(definition,[spl292_749])],[avatar_definition]) ).
fof(f33601,plain,
( ~ spl292_749
| spl292_65
| ~ spl292_748 ),
inference(avatar_split_clause,[],[f33595,f33587,f22455,f33598]) ).
fof(f36058,definition,
( spl292_927
<=> ! [X0] :
( r1_tarski(sF286,X0)
| r2_hidden(sK41(sF286,X0),sF287) ) ),
introduced(definition,[new_symbols(definition,[spl292_927])],[avatar_definition]) ).
fof(f36059,plain,
( ! [X0] :
( r2_hidden(sK41(sF286,X0),sF287)
| r1_tarski(sF286,X0) )
| ~ spl292_927 ),
inference(avatar_component_clause,[],[f36058]) ).
fof(f36314,plain,
( ! [X2,X3,X0,X1] :
( r2_hidden(X0,k8_relset_2(X2,X3,X1,sF285))
| ~ r2_hidden(sK28(X1,X0,sF285),sK23)
| ~ r2_hidden(X0,sF288)
| ~ r2_hidden(X0,sF287)
| ~ m1_subset_1(sF285,k1_zfmisc_1(k2_zfmisc_1(X2,X3)))
| ~ m1_subset_1(X0,X3)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| v1_xboole_0(X3) )
| ~ spl292_82
| ~ spl292_87
| ~ spl292_90
| ~ spl292_91 ),
inference(resolution,[],[f23526,f22001]) ).
fof(f37836,plain,
( ! [X2,X3,X0,X1] :
( r2_hidden(sK41(sF286,X1),k8_relset_2(X2,X3,X0,sK24))
| r1_tarski(sF286,X1)
| ~ r2_hidden(sK28(X0,sK41(sF286,X1),sK24),sK23)
| ~ m1_subset_1(sK24,k1_zfmisc_1(k2_zfmisc_1(X2,X3)))
| ~ m1_subset_1(sK41(sF286,X1),X3)
| ~ m1_subset_1(X0,k1_zfmisc_1(X2))
| v1_xboole_0(X3) )
| ~ spl292_62
| ~ spl292_66
| ~ spl292_68
| ~ spl292_72
| ~ spl292_73
| ~ spl292_82
| ~ spl292_84
| ~ spl292_85
| ~ spl292_87 ),
inference(resolution,[],[f26415,f22001]) ).
fof(f37865,plain,
( ! [X0] :
( r2_hidden(sK41(sF286,X0),sF287)
| r1_tarski(sF286,X0)
| ~ r2_hidden(sK28(sK23,sK41(sF286,X0),sK24),sK23)
| ~ m1_subset_1(sK24,k1_zfmisc_1(k2_zfmisc_1(sK21,sK22)))
| ~ m1_subset_1(sK41(sF286,X0),sK22)
| ~ m1_subset_1(sK23,k1_zfmisc_1(sK21))
| v1_xboole_0(sK22) )
| ~ spl292_62
| ~ spl292_66
| ~ spl292_68
| ~ spl292_69
| ~ spl292_72
| ~ spl292_73
| ~ spl292_82
| ~ spl292_84
| ~ spl292_85
| ~ spl292_87 ),
inference(superposition,[],[f37836,f22477]) ).
fof(f37875,plain,
( ! [X0] :
( r2_hidden(sK41(sF286,X0),sF287)
| r1_tarski(sF286,X0)
| ~ m1_subset_1(sK24,k1_zfmisc_1(k2_zfmisc_1(sK21,sK22)))
| ~ m1_subset_1(sK41(sF286,X0),sK22)
| ~ m1_subset_1(sK23,k1_zfmisc_1(sK21))
| v1_xboole_0(sK22) )
| ~ spl292_62
| ~ spl292_66
| ~ spl292_68
| ~ spl292_69
| ~ spl292_72
| ~ spl292_73
| ~ spl292_82
| ~ spl292_84
| ~ spl292_85
| ~ spl292_87
| ~ spl292_440 ),
inference(forward_subsumption_resolution,[],[f37865,f28740]) ).
fof(f40937,plain,
( ! [X2,X3,X0,X1] :
( r2_hidden(sK41(sF286,X1),k8_relset_2(X2,X3,X0,sK25))
| r1_tarski(sF286,X1)
| ~ r2_hidden(sK28(X0,sK41(sF286,X1),sK25),sK23)
| ~ m1_subset_1(sK25,k1_zfmisc_1(k2_zfmisc_1(X2,X3)))
| ~ m1_subset_1(sK41(sF286,X1),X3)
| ~ m1_subset_1(X0,k1_zfmisc_1(X2))
| v1_xboole_0(X3) )
| ~ spl292_62
| ~ spl292_66
| ~ spl292_68
| ~ spl292_72
| ~ spl292_73
| ~ spl292_83
| ~ spl292_85
| ~ spl292_87
| ~ spl292_100 ),
inference(resolution,[],[f26427,f22001]) ).
fof(f40968,plain,
( ! [X0] :
( r2_hidden(sK41(sF286,X0),sF288)
| r1_tarski(sF286,X0)
| ~ r2_hidden(sK28(sK23,sK41(sF286,X0),sK25),sK23)
| ~ m1_subset_1(sK25,k1_zfmisc_1(k2_zfmisc_1(sK21,sK22)))
| ~ m1_subset_1(sK41(sF286,X0),sK22)
| ~ m1_subset_1(sK23,k1_zfmisc_1(sK21))
| v1_xboole_0(sK22) )
| ~ spl292_62
| ~ spl292_66
| ~ spl292_68
| ~ spl292_70
| ~ spl292_72
| ~ spl292_73
| ~ spl292_83
| ~ spl292_85
| ~ spl292_87
| ~ spl292_100 ),
inference(superposition,[],[f40937,f22482]) ).
fof(f40979,plain,
( ! [X0] :
( r2_hidden(sK41(sF286,X0),sF288)
| r1_tarski(sF286,X0)
| ~ m1_subset_1(sK25,k1_zfmisc_1(k2_zfmisc_1(sK21,sK22)))
| ~ m1_subset_1(sK41(sF286,X0),sK22)
| ~ m1_subset_1(sK23,k1_zfmisc_1(sK21))
| v1_xboole_0(sK22) )
| ~ spl292_62
| ~ spl292_66
| ~ spl292_68
| ~ spl292_70
| ~ spl292_72
| ~ spl292_73
| ~ spl292_83
| ~ spl292_85
| ~ spl292_87
| ~ spl292_100
| ~ spl292_439 ),
inference(forward_subsumption_resolution,[],[f40968,f28736]) ).
fof(f40988,plain,
( ! [X0] :
( r2_hidden(sK41(sF286,X0),sF288)
| r1_tarski(sF286,X0)
| ~ m1_subset_1(sK25,k1_zfmisc_1(k2_zfmisc_1(sK21,sK22)))
| ~ m1_subset_1(sK23,k1_zfmisc_1(sK21))
| v1_xboole_0(sK22) )
| ~ spl292_62
| ~ spl292_66
| ~ spl292_68
| ~ spl292_70
| ~ spl292_72
| ~ spl292_73
| ~ spl292_76
| ~ spl292_83
| ~ spl292_85
| ~ spl292_87
| ~ spl292_100
| ~ spl292_439 ),
inference(forward_subsumption_resolution,[],[f40979,f26486]) ).
fof(f40997,plain,
( ! [X0] :
( r2_hidden(sK41(sF286,X0),sF288)
| r1_tarski(sF286,X0)
| ~ m1_subset_1(sK25,k1_zfmisc_1(k2_zfmisc_1(sK21,sK22)))
| ~ m1_subset_1(sK23,k1_zfmisc_1(sK21)) )
| ~ spl292_62
| ~ spl292_66
| ~ spl292_68
| ~ spl292_70
| ~ spl292_72
| ~ spl292_73
| ~ spl292_76
| ~ spl292_83
| ~ spl292_85
| ~ spl292_87
| ~ spl292_100
| spl292_103
| ~ spl292_439 ),
inference(forward_subsumption_resolution,[],[f40988,f23232]) ).
fof(f41006,plain,
( ! [X0] :
( ~ m1_subset_1(sK25,k1_zfmisc_1(sF284))
| r2_hidden(sK41(sF286,X0),sF288)
| r1_tarski(sF286,X0)
| ~ m1_subset_1(sK23,k1_zfmisc_1(sK21)) )
| ~ spl292_62
| ~ spl292_66
| ~ spl292_68
| ~ spl292_70
| ~ spl292_72
| ~ spl292_73
| ~ spl292_76
| ~ spl292_83
| ~ spl292_85
| ~ spl292_87
| ~ spl292_100
| spl292_103
| ~ spl292_439 ),
inference(forward_demodulation,[],[f40997,f22462]) ).
fof(f41015,plain,
( ! [X0] :
( ~ m1_subset_1(sK25,sF290)
| r2_hidden(sK41(sF286,X0),sF288)
| r1_tarski(sF286,X0)
| ~ m1_subset_1(sK23,k1_zfmisc_1(sK21)) )
| ~ spl292_62
| ~ spl292_66
| ~ spl292_68
| ~ spl292_70
| ~ spl292_72
| ~ spl292_73
| ~ spl292_76
| ~ spl292_83
| ~ spl292_85
| ~ spl292_87
| ~ spl292_100
| spl292_103
| ~ spl292_439 ),
inference(forward_demodulation,[],[f41006,f22492]) ).
fof(f41024,plain,
( ! [X0] :
( r2_hidden(sK41(sF286,X0),sF288)
| r1_tarski(sF286,X0)
| ~ m1_subset_1(sK23,k1_zfmisc_1(sK21)) )
| ~ spl292_62
| ~ spl292_64
| ~ spl292_66
| ~ spl292_68
| ~ spl292_70
| ~ spl292_72
| ~ spl292_73
| ~ spl292_76
| ~ spl292_83
| ~ spl292_85
| ~ spl292_87
| ~ spl292_100
| spl292_103
| ~ spl292_439 ),
inference(forward_subsumption_resolution,[],[f41015,f22452]) ).
fof(f41034,plain,
( ! [X0] :
( ~ m1_subset_1(sK23,sF291)
| r2_hidden(sK41(sF286,X0),sF288)
| r1_tarski(sF286,X0) )
| ~ spl292_62
| ~ spl292_64
| ~ spl292_66
| ~ spl292_68
| ~ spl292_70
| ~ spl292_72
| ~ spl292_73
| ~ spl292_76
| ~ spl292_83
| ~ spl292_85
| ~ spl292_87
| ~ spl292_100
| spl292_103
| ~ spl292_439 ),
inference(forward_demodulation,[],[f41024,f22497]) ).
fof(f41042,definition,
( spl292_1178
<=> ! [X0] :
( r2_hidden(sK41(sF286,X0),sF288)
| r1_tarski(sF286,X0) ) ),
introduced(definition,[new_symbols(definition,[spl292_1178])],[avatar_definition]) ).
fof(f41043,plain,
( ! [X0] :
( r2_hidden(sK41(sF286,X0),sF288)
| r1_tarski(sF286,X0) )
| ~ spl292_1178 ),
inference(avatar_component_clause,[],[f41042]) ).
fof(f41045,plain,
( ! [X0] :
( r2_hidden(sK41(sF286,X0),sF288)
| r1_tarski(sF286,X0) )
| ~ spl292_62
| ~ spl292_64
| ~ spl292_66
| ~ spl292_68
| ~ spl292_70
| ~ spl292_72
| ~ spl292_73
| ~ spl292_76
| ~ spl292_83
| ~ spl292_85
| ~ spl292_87
| ~ spl292_100
| spl292_103
| ~ spl292_439 ),
inference(forward_subsumption_resolution,[],[f41034,f22442]) ).
fof(f41047,plain,
( spl292_1178
| ~ spl292_62
| ~ spl292_64
| ~ spl292_66
| ~ spl292_68
| ~ spl292_70
| ~ spl292_72
| ~ spl292_73
| ~ spl292_76
| ~ spl292_83
| ~ spl292_85
| ~ spl292_87
| ~ spl292_100
| spl292_103
| ~ spl292_439 ),
inference(avatar_split_clause,[],[f41045,f28735,f23231,f23048,f22624,f22591,f22579,f22509,f22495,f22490,f22480,f22470,f22460,f22450,f22440,f41042]) ).
fof(f41054,plain,
( ! [X0] :
( ~ r2_hidden(sK41(sF286,X0),sF287)
| r1_tarski(sF286,X0)
| r2_hidden(sK41(sF286,X0),sF289) )
| ~ spl292_81
| ~ spl292_1178 ),
inference(resolution,[],[f41043,f23474]) ).
fof(f41061,plain,
( ! [X0] :
( r2_hidden(sK41(sF286,X0),sF289)
| r1_tarski(sF286,X0) )
| ~ spl292_81
| ~ spl292_927
| ~ spl292_1178 ),
inference(forward_subsumption_resolution,[],[f41054,f36059]) ).
fof(f41081,plain,
( ! [X0] :
( r2_hidden(sK41(sF286,X0),sF287)
| r1_tarski(sF286,X0)
| ~ m1_subset_1(sK24,k1_zfmisc_1(k2_zfmisc_1(sK21,sK22)))
| ~ m1_subset_1(sK23,k1_zfmisc_1(sK21))
| v1_xboole_0(sK22) )
| ~ spl292_62
| ~ spl292_66
| ~ spl292_68
| ~ spl292_69
| ~ spl292_72
| ~ spl292_73
| ~ spl292_76
| ~ spl292_82
| ~ spl292_84
| ~ spl292_85
| ~ spl292_87
| ~ spl292_440 ),
inference(forward_subsumption_resolution,[],[f37875,f26486]) ).
fof(f41200,plain,
( ! [X0] :
( r2_hidden(sK41(sF286,X0),sF287)
| r1_tarski(sF286,X0)
| ~ m1_subset_1(sK24,k1_zfmisc_1(k2_zfmisc_1(sK21,sK22)))
| ~ m1_subset_1(sK23,k1_zfmisc_1(sK21)) )
| ~ spl292_62
| ~ spl292_66
| ~ spl292_68
| ~ spl292_69
| ~ spl292_72
| ~ spl292_73
| ~ spl292_76
| ~ spl292_82
| ~ spl292_84
| ~ spl292_85
| ~ spl292_87
| spl292_103
| ~ spl292_440 ),
inference(forward_subsumption_resolution,[],[f41081,f23232]) ).
fof(f41283,plain,
( ! [X0] :
( ~ m1_subset_1(sK24,k1_zfmisc_1(sF284))
| r2_hidden(sK41(sF286,X0),sF287)
| r1_tarski(sF286,X0)
| ~ m1_subset_1(sK23,k1_zfmisc_1(sK21)) )
| ~ spl292_62
| ~ spl292_66
| ~ spl292_68
| ~ spl292_69
| ~ spl292_72
| ~ spl292_73
| ~ spl292_76
| ~ spl292_82
| ~ spl292_84
| ~ spl292_85
| ~ spl292_87
| spl292_103
| ~ spl292_440 ),
inference(forward_demodulation,[],[f41200,f22462]) ).
fof(f41363,plain,
( ! [X0] :
( ~ m1_subset_1(sK24,sF290)
| r2_hidden(sK41(sF286,X0),sF287)
| r1_tarski(sF286,X0)
| ~ m1_subset_1(sK23,k1_zfmisc_1(sK21)) )
| ~ spl292_62
| ~ spl292_66
| ~ spl292_68
| ~ spl292_69
| ~ spl292_72
| ~ spl292_73
| ~ spl292_76
| ~ spl292_82
| ~ spl292_84
| ~ spl292_85
| ~ spl292_87
| spl292_103
| ~ spl292_440 ),
inference(forward_demodulation,[],[f41283,f22492]) ).
fof(f41443,plain,
( ! [X0] :
( r2_hidden(sK41(sF286,X0),sF287)
| r1_tarski(sF286,X0)
| ~ m1_subset_1(sK23,k1_zfmisc_1(sK21)) )
| ~ spl292_62
| ~ spl292_63
| ~ spl292_66
| ~ spl292_68
| ~ spl292_69
| ~ spl292_72
| ~ spl292_73
| ~ spl292_76
| ~ spl292_82
| ~ spl292_84
| ~ spl292_85
| ~ spl292_87
| spl292_103
| ~ spl292_440 ),
inference(forward_subsumption_resolution,[],[f41363,f22447]) ).
fof(f41455,plain,
( ! [X0] :
( ~ m1_subset_1(sK23,sF291)
| r2_hidden(sK41(sF286,X0),sF287)
| r1_tarski(sF286,X0) )
| ~ spl292_62
| ~ spl292_63
| ~ spl292_66
| ~ spl292_68
| ~ spl292_69
| ~ spl292_72
| ~ spl292_73
| ~ spl292_76
| ~ spl292_82
| ~ spl292_84
| ~ spl292_85
| ~ spl292_87
| spl292_103
| ~ spl292_440 ),
inference(forward_demodulation,[],[f41443,f22497]) ).
fof(f41462,plain,
( ! [X0] :
( r2_hidden(sK41(sF286,X0),sF287)
| r1_tarski(sF286,X0) )
| ~ spl292_62
| ~ spl292_63
| ~ spl292_66
| ~ spl292_68
| ~ spl292_69
| ~ spl292_72
| ~ spl292_73
| ~ spl292_76
| ~ spl292_82
| ~ spl292_84
| ~ spl292_85
| ~ spl292_87
| spl292_103
| ~ spl292_440 ),
inference(forward_subsumption_resolution,[],[f41455,f22442]) ).
fof(f41463,plain,
( spl292_927
| ~ spl292_62
| ~ spl292_63
| ~ spl292_66
| ~ spl292_68
| ~ spl292_69
| ~ spl292_72
| ~ spl292_73
| ~ spl292_76
| ~ spl292_82
| ~ spl292_84
| ~ spl292_85
| ~ spl292_87
| spl292_103
| ~ spl292_440 ),
inference(avatar_split_clause,[],[f41462,f28739,f23231,f22624,f22591,f22584,f22571,f22509,f22495,f22490,f22475,f22470,f22460,f22445,f22440,f36058]) ).
fof(f41482,plain,
( r1_tarski(sF286,sF289)
| r1_tarski(sF286,sF289)
| ~ spl292_81
| ~ spl292_927
| ~ spl292_1178 ),
inference(resolution,[],[f41061,f20615]) ).
fof(f41488,plain,
( r1_tarski(sF286,sF289)
| ~ spl292_81
| ~ spl292_927
| ~ spl292_1178 ),
inference(duplicate_literal_removal,[],[f41482]) ).
fof(f41496,plain,
( spl292_749
| ~ spl292_81
| ~ spl292_927
| ~ spl292_1178 ),
inference(avatar_split_clause,[],[f41488,f41042,f36058,f22563,f33598]) ).
fof(f48615,plain,
( ! [X0] :
( r2_hidden(sK28(sK23,sK41(X0,sF286),sF285),sK23)
| ~ m1_subset_1(sF285,k1_zfmisc_1(k2_zfmisc_1(sK21,sK22)))
| ~ m1_subset_1(sK41(X0,sF286),sK22)
| ~ m1_subset_1(sK23,k1_zfmisc_1(sK21))
| v1_xboole_0(sK22)
| r1_tarski(X0,sF286) )
| ~ spl292_68 ),
inference(superposition,[],[f23855,f22472]) ).
fof(f48652,plain,
( ! [X0] :
( r2_hidden(sK28(sK23,sK41(X0,sF286),sF285),sK23)
| ~ m1_subset_1(sF285,k1_zfmisc_1(k2_zfmisc_1(sK21,sK22)))
| ~ m1_subset_1(sK41(X0,sF286),sK22)
| ~ m1_subset_1(sK23,k1_zfmisc_1(sK21))
| r1_tarski(X0,sF286) )
| ~ spl292_68
| spl292_103 ),
inference(forward_subsumption_resolution,[],[f48615,f23232]) ).
fof(f48705,plain,
( ! [X0] :
( ~ m1_subset_1(sF285,k1_zfmisc_1(sF284))
| r2_hidden(sK28(sK23,sK41(X0,sF286),sF285),sK23)
| ~ m1_subset_1(sK41(X0,sF286),sK22)
| ~ m1_subset_1(sK23,k1_zfmisc_1(sK21))
| r1_tarski(X0,sF286) )
| ~ spl292_66
| ~ spl292_68
| spl292_103 ),
inference(forward_demodulation,[],[f48652,f22462]) ).
fof(f48744,plain,
( ! [X0] :
( ~ m1_subset_1(sF285,sF290)
| r2_hidden(sK28(sK23,sK41(X0,sF286),sF285),sK23)
| ~ m1_subset_1(sK41(X0,sF286),sK22)
| ~ m1_subset_1(sK23,k1_zfmisc_1(sK21))
| r1_tarski(X0,sF286) )
| ~ spl292_66
| ~ spl292_68
| ~ spl292_72
| spl292_103 ),
inference(forward_demodulation,[],[f48705,f22492]) ).
fof(f48783,plain,
( ! [X0] :
( r2_hidden(sK28(sK23,sK41(X0,sF286),sF285),sK23)
| ~ m1_subset_1(sK41(X0,sF286),sK22)
| ~ m1_subset_1(sK23,k1_zfmisc_1(sK21))
| r1_tarski(X0,sF286) )
| ~ spl292_66
| ~ spl292_68
| ~ spl292_72
| ~ spl292_85
| spl292_103 ),
inference(forward_subsumption_resolution,[],[f48744,f22592]) ).
fof(f70769,plain,
( ! [X0] :
( ~ m1_subset_1(sK23,sF291)
| r2_hidden(sK28(sK23,sK41(X0,sF286),sF285),sK23)
| ~ m1_subset_1(sK41(X0,sF286),sK22)
| r1_tarski(X0,sF286) )
| ~ spl292_66
| ~ spl292_68
| ~ spl292_72
| ~ spl292_73
| ~ spl292_85
| spl292_103 ),
inference(forward_demodulation,[],[f48783,f22497]) ).
fof(f71309,plain,
( ! [X0] :
( r2_hidden(sK28(sK23,sK41(X0,sF286),sF285),sK23)
| ~ m1_subset_1(sK41(X0,sF286),sK22)
| r1_tarski(X0,sF286) )
| ~ spl292_62
| ~ spl292_66
| ~ spl292_68
| ~ spl292_72
| ~ spl292_73
| ~ spl292_85
| spl292_103 ),
inference(forward_subsumption_resolution,[],[f70769,f22442]) ).
fof(f95881,plain,
( ! [X0] :
( r2_hidden(X0,sF286)
| ~ r2_hidden(sK28(sK23,X0,sF285),sK23)
| ~ r2_hidden(X0,sF288)
| ~ r2_hidden(X0,sF287)
| ~ m1_subset_1(sF285,k1_zfmisc_1(k2_zfmisc_1(sK21,sK22)))
| ~ m1_subset_1(X0,sK22)
| ~ m1_subset_1(sK23,k1_zfmisc_1(sK21))
| v1_xboole_0(sK22) )
| ~ spl292_68
| ~ spl292_82
| ~ spl292_87
| ~ spl292_90
| ~ spl292_91 ),
inference(superposition,[],[f36314,f22472]) ).
fof(f95893,plain,
( ! [X0] :
( r2_hidden(X0,sF286)
| ~ r2_hidden(sK28(sK23,X0,sF285),sK23)
| ~ r2_hidden(X0,sF288)
| ~ r2_hidden(X0,sF287)
| ~ m1_subset_1(sF285,k1_zfmisc_1(k2_zfmisc_1(sK21,sK22)))
| ~ m1_subset_1(sK23,k1_zfmisc_1(sK21))
| v1_xboole_0(sK22) )
| ~ spl292_68
| ~ spl292_82
| ~ spl292_87
| ~ spl292_90
| ~ spl292_91
| ~ spl292_579 ),
inference(forward_subsumption_resolution,[],[f95881,f30732]) ).
fof(f95913,plain,
( ! [X0] :
( r2_hidden(X0,sF286)
| ~ r2_hidden(sK28(sK23,X0,sF285),sK23)
| ~ r2_hidden(X0,sF288)
| ~ r2_hidden(X0,sF287)
| ~ m1_subset_1(sF285,k1_zfmisc_1(k2_zfmisc_1(sK21,sK22)))
| ~ m1_subset_1(sK23,k1_zfmisc_1(sK21)) )
| ~ spl292_68
| ~ spl292_82
| ~ spl292_87
| ~ spl292_90
| ~ spl292_91
| spl292_103
| ~ spl292_579 ),
inference(forward_subsumption_resolution,[],[f95893,f23232]) ).
fof(f95928,plain,
( ! [X0] :
( ~ m1_subset_1(sF285,k1_zfmisc_1(sF284))
| r2_hidden(X0,sF286)
| ~ r2_hidden(sK28(sK23,X0,sF285),sK23)
| ~ r2_hidden(X0,sF288)
| ~ r2_hidden(X0,sF287)
| ~ m1_subset_1(sK23,k1_zfmisc_1(sK21)) )
| ~ spl292_66
| ~ spl292_68
| ~ spl292_82
| ~ spl292_87
| ~ spl292_90
| ~ spl292_91
| spl292_103
| ~ spl292_579 ),
inference(forward_demodulation,[],[f95913,f22462]) ).
fof(f95943,plain,
( ! [X0] :
( ~ m1_subset_1(sF285,sF290)
| r2_hidden(X0,sF286)
| ~ r2_hidden(sK28(sK23,X0,sF285),sK23)
| ~ r2_hidden(X0,sF288)
| ~ r2_hidden(X0,sF287)
| ~ m1_subset_1(sK23,k1_zfmisc_1(sK21)) )
| ~ spl292_66
| ~ spl292_68
| ~ spl292_72
| ~ spl292_82
| ~ spl292_87
| ~ spl292_90
| ~ spl292_91
| spl292_103
| ~ spl292_579 ),
inference(forward_demodulation,[],[f95928,f22492]) ).
fof(f95958,plain,
( ! [X0] :
( r2_hidden(X0,sF286)
| ~ r2_hidden(sK28(sK23,X0,sF285),sK23)
| ~ r2_hidden(X0,sF288)
| ~ r2_hidden(X0,sF287)
| ~ m1_subset_1(sK23,k1_zfmisc_1(sK21)) )
| ~ spl292_66
| ~ spl292_68
| ~ spl292_72
| ~ spl292_82
| ~ spl292_85
| ~ spl292_87
| ~ spl292_90
| ~ spl292_91
| spl292_103
| ~ spl292_579 ),
inference(forward_subsumption_resolution,[],[f95943,f22592]) ).
fof(f95973,plain,
( ! [X0] :
( ~ m1_subset_1(sK23,sF291)
| r2_hidden(X0,sF286)
| ~ r2_hidden(sK28(sK23,X0,sF285),sK23)
| ~ r2_hidden(X0,sF288)
| ~ r2_hidden(X0,sF287) )
| ~ spl292_66
| ~ spl292_68
| ~ spl292_72
| ~ spl292_73
| ~ spl292_82
| ~ spl292_85
| ~ spl292_87
| ~ spl292_90
| ~ spl292_91
| spl292_103
| ~ spl292_579 ),
inference(forward_demodulation,[],[f95958,f22497]) ).
fof(f95992,plain,
( ! [X0] :
( ~ r2_hidden(sK28(sK23,X0,sF285),sK23)
| r2_hidden(X0,sF286)
| ~ r2_hidden(X0,sF288)
| ~ r2_hidden(X0,sF287) )
| ~ spl292_62
| ~ spl292_66
| ~ spl292_68
| ~ spl292_72
| ~ spl292_73
| ~ spl292_82
| ~ spl292_85
| ~ spl292_87
| ~ spl292_90
| ~ spl292_91
| spl292_103
| ~ spl292_579 ),
inference(forward_subsumption_resolution,[],[f95973,f22442]) ).
fof(f96001,plain,
( ! [X0] :
( r2_hidden(sK41(X0,sF286),sF286)
| ~ r2_hidden(sK41(X0,sF286),sF288)
| ~ r2_hidden(sK41(X0,sF286),sF287)
| ~ m1_subset_1(sK41(X0,sF286),sK22)
| r1_tarski(X0,sF286) )
| ~ spl292_62
| ~ spl292_66
| ~ spl292_68
| ~ spl292_72
| ~ spl292_73
| ~ spl292_82
| ~ spl292_85
| ~ spl292_87
| ~ spl292_90
| ~ spl292_91
| spl292_103
| ~ spl292_579 ),
inference(resolution,[],[f95992,f71309]) ).
fof(f96014,plain,
( ! [X0] :
( r2_hidden(sK41(X0,sF286),sF286)
| ~ r2_hidden(sK41(X0,sF286),sF288)
| ~ r2_hidden(sK41(X0,sF286),sF287)
| r1_tarski(X0,sF286) )
| ~ spl292_62
| ~ spl292_66
| ~ spl292_68
| ~ spl292_72
| ~ spl292_73
| ~ spl292_82
| ~ spl292_85
| ~ spl292_87
| ~ spl292_90
| ~ spl292_91
| spl292_103
| ~ spl292_579 ),
inference(forward_subsumption_resolution,[],[f96001,f30732]) ).
fof(f96020,plain,
( ! [X0] :
( ~ r2_hidden(sK41(X0,sF286),sF288)
| ~ r2_hidden(sK41(X0,sF286),sF287)
| r1_tarski(X0,sF286) )
| ~ spl292_62
| ~ spl292_66
| ~ spl292_68
| ~ spl292_72
| ~ spl292_73
| ~ spl292_82
| ~ spl292_85
| ~ spl292_87
| ~ spl292_90
| ~ spl292_91
| spl292_103
| ~ spl292_579 ),
inference(forward_subsumption_resolution,[],[f96014,f20615]) ).
fof(f96025,plain,
( ~ r2_hidden(sK41(sF289,sF286),sF287)
| r1_tarski(sF289,sF286)
| r1_tarski(sF289,sF286)
| ~ spl292_62
| ~ spl292_66
| ~ spl292_68
| ~ spl292_72
| ~ spl292_73
| ~ spl292_82
| ~ spl292_85
| ~ spl292_87
| ~ spl292_90
| ~ spl292_91
| ~ spl292_99
| spl292_103
| ~ spl292_579 ),
inference(resolution,[],[f96020,f24871]) ).
fof(f96036,plain,
( ~ r2_hidden(sK41(sF289,sF286),sF287)
| r1_tarski(sF289,sF286)
| ~ spl292_62
| ~ spl292_66
| ~ spl292_68
| ~ spl292_72
| ~ spl292_73
| ~ spl292_82
| ~ spl292_85
| ~ spl292_87
| ~ spl292_90
| ~ spl292_91
| ~ spl292_99
| spl292_103
| ~ spl292_579 ),
inference(duplicate_literal_removal,[],[f96025]) ).
fof(f96039,plain,
( r1_tarski(sF289,sF286)
| ~ spl292_62
| ~ spl292_66
| ~ spl292_68
| ~ spl292_72
| ~ spl292_73
| ~ spl292_81
| ~ spl292_82
| ~ spl292_85
| ~ spl292_87
| ~ spl292_90
| ~ spl292_91
| ~ spl292_99
| spl292_103
| ~ spl292_579 ),
inference(forward_subsumption_resolution,[],[f96036,f24788]) ).
fof(f96045,plain,
( spl292_748
| ~ spl292_62
| ~ spl292_66
| ~ spl292_68
| ~ spl292_72
| ~ spl292_73
| ~ spl292_81
| ~ spl292_82
| ~ spl292_85
| ~ spl292_87
| ~ spl292_90
| ~ spl292_91
| ~ spl292_99
| spl292_103
| ~ spl292_579 ),
inference(avatar_split_clause,[],[f96039,f30731,f23231,f23040,f22958,f22951,f22624,f22591,f22571,f22563,f22495,f22490,f22470,f22460,f22440,f33587]) ).
cnf(s66,plain,
spl292_62,
inference(sat_conversion,[],[f22443]) ).
cnf(s67,plain,
spl292_63,
inference(sat_conversion,[],[f22448]) ).
cnf(s68,plain,
spl292_64,
inference(sat_conversion,[],[f22453]) ).
cnf(s69,plain,
~ spl292_65,
inference(sat_conversion,[],[f22458]) ).
cnf(s70,plain,
spl292_66,
inference(sat_conversion,[],[f22463]) ).
cnf(s71,plain,
spl292_67,
inference(sat_conversion,[],[f22468]) ).
cnf(s72,plain,
spl292_68,
inference(sat_conversion,[],[f22473]) ).
cnf(s73,plain,
spl292_69,
inference(sat_conversion,[],[f22478]) ).
cnf(s74,plain,
spl292_70,
inference(sat_conversion,[],[f22483]) ).
cnf(s75,plain,
spl292_71,
inference(sat_conversion,[],[f22488]) ).
cnf(s76,plain,
spl292_72,
inference(sat_conversion,[],[f22493]) ).
cnf(s77,plain,
spl292_73,
inference(sat_conversion,[],[f22498]) ).
cnf(s78,plain,
( ~ spl292_68
| ~ spl292_74
| ~ spl292_75
| spl292_76 ),
inference(sat_conversion,[],[f22512]) ).
cnf(s79,plain,
( ~ spl292_69
| ~ spl292_75
| ~ spl292_77
| spl292_78 ),
inference(sat_conversion,[],[f22522]) ).
cnf(s80,plain,
( ~ spl292_62
| ~ spl292_73
| spl292_75 ),
inference(sat_conversion,[],[f22523]) ).
cnf(s81,plain,
( ~ spl292_63
| ~ spl292_66
| ~ spl292_72
| spl292_77 ),
inference(sat_conversion,[],[f22524]) ).
cnf(s82,plain,
( ~ spl292_70
| ~ spl292_75
| ~ spl292_79
| spl292_80 ),
inference(sat_conversion,[],[f22534]) ).
cnf(s83,plain,
( ~ spl292_64
| ~ spl292_66
| ~ spl292_72
| spl292_79 ),
inference(sat_conversion,[],[f22535]) ).
cnf(s84,plain,
( ~ spl292_71
| ~ spl292_78
| ~ spl292_80
| spl292_81 ),
inference(sat_conversion,[],[f22566]) ).
cnf(s86,plain,
( ~ spl292_63
| ~ spl292_64
| ~ spl292_67
| ~ spl292_72
| spl292_82 ),
inference(sat_conversion,[],[f22574]) ).
cnf(s88,plain,
( ~ spl292_64
| ~ spl292_66
| ~ spl292_72
| spl292_83 ),
inference(sat_conversion,[],[f22582]) ).
cnf(s89,plain,
( ~ spl292_63
| ~ spl292_66
| ~ spl292_72
| spl292_84 ),
inference(sat_conversion,[],[f22587]) ).
cnf(s90,plain,
( ~ spl292_66
| ~ spl292_72
| spl292_74
| ~ spl292_85 ),
inference(sat_conversion,[],[f22594]) ).
cnf(s92,plain,
( ~ spl292_63
| ~ spl292_64
| ~ spl292_67
| ~ spl292_72
| spl292_85 ),
inference(sat_conversion,[],[f22618]) ).
cnf(s94,plain,
( ~ spl292_66
| ~ spl292_72
| ~ spl292_85
| spl292_87 ),
inference(sat_conversion,[],[f22627]) ).
cnf(s96,plain,
( ~ spl292_62
| ~ spl292_63
| ~ spl292_66
| ~ spl292_69
| ~ spl292_72
| ~ spl292_73
| ~ spl292_84
| spl292_90 ),
inference(sat_conversion,[],[f22953]) ).
cnf(s97,plain,
( ~ spl292_62
| ~ spl292_64
| ~ spl292_66
| ~ spl292_70
| ~ spl292_72
| ~ spl292_73
| ~ spl292_83
| spl292_91 ),
inference(sat_conversion,[],[f22960]) ).
cnf(s105,plain,
( ~ spl292_71
| ~ spl292_78
| ~ spl292_80
| spl292_99 ),
inference(sat_conversion,[],[f23043]) ).
cnf(s107,plain,
( ~ spl292_63
| ~ spl292_64
| ~ spl292_67
| ~ spl292_72
| spl292_100 ),
inference(sat_conversion,[],[f23051]) ).
cnf(s440,plain,
( ~ spl292_62
| ~ spl292_64
| ~ spl292_66
| ~ spl292_70
| ~ spl292_72
| ~ spl292_73
| spl292_103
| spl292_439 ),
inference(sat_conversion,[],[f28737]) ).
cnf(s441,plain,
( ~ spl292_62
| ~ spl292_63
| ~ spl292_66
| ~ spl292_69
| ~ spl292_72
| ~ spl292_73
| spl292_103
| spl292_440 ),
inference(sat_conversion,[],[f28741]) ).
cnf(s547,plain,
( ~ spl292_76
| ~ spl292_103
| spl292_367 ),
inference(sat_conversion,[],[f30340]) ).
cnf(s581,plain,
( spl292_65
| ~ spl292_99
| ~ spl292_367
| ~ spl292_370 ),
inference(sat_conversion,[],[f30610]) ).
cnf(s600,plain,
( ~ spl292_80
| ~ spl292_103
| spl292_370 ),
inference(sat_conversion,[],[f30675]) ).
cnf(s610,plain,
( ~ spl292_62
| ~ spl292_64
| ~ spl292_66
| ~ spl292_70
| ~ spl292_72
| ~ spl292_73
| spl292_579 ),
inference(sat_conversion,[],[f30747]) ).
cnf(s802,plain,
( spl292_65
| ~ spl292_748
| ~ spl292_749 ),
inference(sat_conversion,[],[f33601]) ).
cnf(s1386,plain,
( ~ spl292_62
| ~ spl292_64
| ~ spl292_66
| ~ spl292_68
| ~ spl292_70
| ~ spl292_72
| ~ spl292_73
| ~ spl292_76
| ~ spl292_83
| ~ spl292_85
| ~ spl292_87
| ~ spl292_100
| spl292_103
| ~ spl292_439
| spl292_1178 ),
inference(sat_conversion,[],[f41047]) ).
cnf(s1415,plain,
( ~ spl292_62
| ~ spl292_63
| ~ spl292_66
| ~ spl292_68
| ~ spl292_69
| ~ spl292_72
| ~ spl292_73
| ~ spl292_76
| ~ spl292_82
| ~ spl292_84
| ~ spl292_85
| ~ spl292_87
| spl292_103
| ~ spl292_440
| spl292_927 ),
inference(sat_conversion,[],[f41463]) ).
cnf(s1423,plain,
( ~ spl292_81
| spl292_749
| ~ spl292_927
| ~ spl292_1178 ),
inference(sat_conversion,[],[f41496]) ).
cnf(s5832,plain,
( ~ spl292_62
| ~ spl292_66
| ~ spl292_68
| ~ spl292_72
| ~ spl292_73
| ~ spl292_81
| ~ spl292_82
| ~ spl292_85
| ~ spl292_87
| ~ spl292_90
| ~ spl292_91
| ~ spl292_99
| spl292_103
| ~ spl292_579
| spl292_748 ),
inference(sat_conversion,[],[f96045]) ).
cnf(s5873,plain,
spl292_83,
inference(rat,[],[s88,s70,s76,s68]) ).
cnf(s5874,plain,
spl292_79,
inference(rat,[],[s83,s70,s76,s68]) ).
cnf(s5878,plain,
spl292_100,
inference(rat,[],[s107,s68,s76,s71,s67]) ).
cnf(s5879,plain,
spl292_85,
inference(rat,[],[s92,s68,s76,s71,s67]) ).
cnf(s5880,plain,
spl292_84,
inference(rat,[],[s89,s70,s76,s67]) ).
cnf(s5881,plain,
spl292_82,
inference(rat,[],[s86,s68,s76,s71,s67]) ).
cnf(s5882,plain,
spl292_77,
inference(rat,[],[s81,s70,s76,s67]) ).
cnf(s5888,plain,
spl292_87,
inference(rat,[],[s94,s70,s76,s5879]) ).
cnf(s5889,plain,
spl292_74,
inference(rat,[],[s90,s70,s76,s5879]) ).
cnf(s5940,plain,
spl292_579,
inference(rat,[],[s610,s68,s77,s76,s74,s70,s66]) ).
cnf(s5977,plain,
spl292_91,
inference(rat,[],[s97,s5873,s68,s77,s76,s74,s70,s66]) ).
cnf(s5978,plain,
spl292_90,
inference(rat,[],[s96,s5880,s67,s77,s76,s73,s70,s66]) ).
cnf(s5979,plain,
spl292_75,
inference(rat,[],[s80,s77,s66]) ).
cnf(s6021,plain,
spl292_80,
inference(rat,[],[s82,s5874,s74,s5979]) ).
cnf(s6022,plain,
spl292_78,
inference(rat,[],[s79,s5882,s73,s5979]) ).
cnf(s6023,plain,
spl292_76,
inference(rat,[],[s78,s5889,s72,s5979]) ).
cnf(s6050,plain,
spl292_99,
inference(rat,[],[s105,s6021,s75,s6022]) ).
cnf(s6052,plain,
spl292_81,
inference(rat,[],[s84,s6021,s75,s6022]) ).
cnf(s6103,plain,
spl292_103,
inference(rat,[],[s1423,s802,s1415,s1386,s5832,s441,s440,s6052,s69,s70,s72,s73,s76,s77,s67,s5881,s5880,s5879,s5888,s66,s6023,s74,s68,s5873,s5878,s5977,s5978,s6050,s5940]) ).
cnf(s6104,plain,
spl292_370,
inference(rat,[],[s600,s6021,s6103]) ).
cnf(s6107,plain,
spl292_367,
inference(rat,[],[s547,s6023,s6103]) ).
cnf(s6115,plain,
$false,
inference(rat,[],[s581,s6050,s69,s6104,s6107]) ).
fof(f96046,plain,
$false,
inference(avatar_sat_refutation,[],[s6115]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU433+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.38 % Computer : n007.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Mon Sep 28 05:24:43 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.41 Running first-order theorem proving
% 0.12/0.41 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 12.70/3.64 % (2067900)Detected formulas, will run a generic FOF schedule.
% 12.70/3.64 % (2067909)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1274504727:i=119:av=off:ss=axioms_2988 on theBenchmark for (2988ds/119Mi)
% 12.70/3.64 % (2067905)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=790610003:i=141193_2988 on theBenchmark for (2988ds/141193Mi)
% 12.70/3.64 % (2067906)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=2115183629:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2988 on theBenchmark for (2988ds/134677Mi)
% 12.70/3.64 % (2067908)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3709873738:i=109:sd=1:ins=1:gsp=on:ss=axioms_2988 on theBenchmark for (2988ds/109Mi)
% 12.70/3.64 % (2067907)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=3864151727:i=141695:sd=1:nm=32:gsp=on:ss=included_2988 on theBenchmark for (2988ds/141695Mi)
% 12.70/3.64 % (2067910)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3721598877:s2a=on:i=139:gtg=position_2988 on theBenchmark for (2988ds/139Mi)
% 12.70/3.64 % (2067911)dis-21_1_sil=8000:lcm=predicate:random_seed=411394989:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2988 on theBenchmark for (2988ds/129Mi)
% 12.70/3.64 % (2067909)Instruction limit reached!
% 12.70/3.64 % (2067909)------------------------------
% 12.70/3.64 % (2067909)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.70/3.64 % (2067909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.70/3.64 % (2067909)CaDiCaL version: 2.1.3
% 12.70/3.64 % (2067909)Termination reason: Instruction limit
% 12.70/3.64 % (2067909)Termination phase: Preprocessing 1
% 12.70/3.64 % (2067909)Time elapsed: 0.060 s
% 12.70/3.64 % (2067909)Peak memory usage: 113 MB
% 12.70/3.64 % (2067909)Instructions burned: 120 (million)
% 12.70/3.64 % (2067910)Instruction limit reached!
% 12.70/3.64 % (2067910)------------------------------
% 12.70/3.64 % (2067910)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.70/3.64 % (2067910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.70/3.64 % (2067910)CaDiCaL version: 2.1.3
% 12.70/3.64 % (2067910)Termination reason: Instruction limit
% 12.70/3.64 % (2067910)Termination phase: Property scanning
% 12.70/3.64 % (2067910)Time elapsed: 0.060 s
% 12.70/3.64 % (2067910)Peak memory usage: 112 MB
% 12.70/3.64 % (2067910)Instructions burned: 141 (million)
% 12.70/3.64 % (2067908)Instruction limit reached!
% 12.70/3.64 % (2067908)------------------------------
% 12.70/3.64 % (2067908)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.70/3.64 % (2067908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.70/3.64 % (2067908)CaDiCaL version: 2.1.3
% 12.70/3.64 % (2067908)Termination reason: Instruction limit
% 12.70/3.64 % (2067908)Termination phase: SInE selection
% 12.70/3.64 % (2067908)Time elapsed: 0.084 s
% 12.70/3.64 % (2067908)Peak memory usage: 112 MB
% 12.70/3.64 % (2067908)Instructions burned: 109 (million)
% 12.70/3.64 % (2067911)Instruction limit reached!
% 12.70/3.64 % (2067911)------------------------------
% 12.70/3.64 % (2067911)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.70/3.64 % (2067911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.70/3.64 % (2067911)CaDiCaL version: 2.1.3
% 12.70/3.64 % (2067911)Termination reason: Instruction limit
% 12.70/3.64 % (2067911)Termination phase: SInE selection
% 12.70/3.64 % (2067911)Time elapsed: 0.087 s
% 12.70/3.64 % (2067911)Peak memory usage: 112 MB
% 12.70/3.64 % (2067911)Instructions burned: 130 (million)
% 12.70/3.64 % (2067919)lrs+10_1_sil=8000:sp=occurrence:random_seed=2608376934:i=285:sd=3:ss=axioms:sgt=8_2987 on theBenchmark for (2987ds/285Mi)
% 12.70/3.64 % (2067920)lrs+10_1_sil=32000:urr=on:br=off:random_seed=530558051:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2986 on theBenchmark for (2986ds/157Mi)
% 12.70/3.64 % (2067921)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3250236709:i=325:sd=1:ss=axioms:sgt=32_2986 on theBenchmark for (2986ds/325Mi)
% 12.70/3.64 % (2067922)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=3935705812:s2a=on:i=248:s2at=1.23:gtg=position_2986 on theBenchmark for (2986ds/248Mi)
% 12.70/3.64 % (2067919)Instruction limit reached!
% 20.03/4.71 % (2067919)------------------------------
% 20.03/4.71 % (2067919)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.03/4.71 % (2067919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.03/4.71 % (2067919)CaDiCaL version: 2.1.3
% 20.03/4.71 % (2067919)Termination reason: Instruction limit
% 20.03/4.71 % (2067919)Termination phase: Saturation
% 20.03/4.71 % (2067919)Time elapsed: 0.120 s
% 20.03/4.71 % (2067919)Peak memory usage: 120 MB
% 20.03/4.71 % (2067919)Instructions burned: 287 (million)
% 20.03/4.71 % (2067920)Instruction limit reached!
% 20.03/4.71 % (2067920)------------------------------
% 20.03/4.71 % (2067920)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.03/4.71 % (2067920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.03/4.71 % (2067920)CaDiCaL version: 2.1.3
% 20.03/4.71 % (2067920)Termination reason: Instruction limit
% 20.03/4.71 % (2067920)Termination phase: Property scanning
% 20.03/4.71 % (2067920)Time elapsed: 0.059 s
% 20.03/4.71 % (2067920)Peak memory usage: 113 MB
% 20.03/4.71 % (2067920)Instructions burned: 158 (million)
% 20.03/4.71 % (2067922)Instruction limit reached!
% 20.03/4.71 % (2067922)------------------------------
% 20.03/4.71 % (2067922)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.03/4.71 % (2067922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.03/4.71 % (2067922)CaDiCaL version: 2.1.3
% 20.03/4.71 % (2067922)Termination reason: Instruction limit
% 20.03/4.71 % (2067922)Termination phase: Property scanning
% 20.03/4.71 % (2067922)Time elapsed: 0.104 s
% 20.03/4.71 % (2067922)Peak memory usage: 112 MB
% 20.03/4.71 % (2067922)Instructions burned: 248 (million)
% 20.03/4.71 % (2067927)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=583119994:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2984 on theBenchmark for (2984ds/294Mi)
% 20.03/4.71 % (2067928)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1827670412:i=2350_2984 on theBenchmark for (2984ds/2350Mi)
% 20.03/4.71 % (2067921)Instruction limit reached!
% 20.03/4.71 % (2067921)------------------------------
% 20.03/4.71 % (2067921)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.03/4.71 % (2067921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.03/4.71 % (2067921)CaDiCaL version: 2.1.3
% 20.03/4.71 % (2067921)Termination reason: Instruction limit
% 20.03/4.71 % (2067921)Termination phase: Saturation
% 20.03/4.71 % (2067921)Time elapsed: 0.234 s
% 20.03/4.71 % (2067921)Peak memory usage: 120 MB
% 20.03/4.71 % (2067921)Instructions burned: 326 (million)
% 20.03/4.71 % (2067929)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=963940808:cts=off:i=113:fsr=off:ss=included:sgt=4_2983 on theBenchmark for (2983ds/113Mi)
% 20.03/4.71 % (2067929)Instruction limit reached!
% 20.03/4.71 % (2067929)------------------------------
% 20.03/4.71 % (2067929)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.03/4.71 % (2067929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.03/4.71 % (2067929)CaDiCaL version: 2.1.3
% 20.03/4.71 % (2067929)Termination reason: Instruction limit
% 20.03/4.71 % (2067929)Termination phase: SInE selection
% 20.03/4.71 % (2067929)Time elapsed: 0.093 s
% 20.03/4.71 % (2067929)Peak memory usage: 112 MB
% 20.03/4.71 % (2067929)Instructions burned: 113 (million)
% 20.03/4.71 % (2067932)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1477792951:i=127:av=off:fsr=off:sup=off_2982 on theBenchmark for (2982ds/127Mi)
% 20.03/4.71 % (2067927)Instruction limit reached!
% 20.03/4.71 % (2067927)------------------------------
% 20.03/4.71 % (2067927)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.03/4.71 % (2067927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.03/4.71 % (2067927)CaDiCaL version: 2.1.3
% 20.03/4.71 % (2067927)Termination reason: Instruction limit
% 20.03/4.71 % (2067927)Termination phase: Function definition elimination
% 20.03/4.71 % (2067927)Time elapsed: 0.212 s
% 20.03/4.71 % (2067927)Peak memory usage: 118 MB
% 20.03/4.71 % (2067927)Instructions burned: 294 (million)
% 20.03/4.71 % (2067932)Instruction limit reached!
% 20.03/4.71 % (2067932)------------------------------
% 20.03/4.71 % (2067932)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.03/4.71 % (2067932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.03/4.71 % (2067932)CaDiCaL version: 2.1.3
% 62.08/10.53 % (2067932)Termination reason: Instruction limit
% 62.08/10.53 % (2067932)Termination phase: Preprocessing 1
% 62.08/10.53 % (2067932)Time elapsed: 0.092 s
% 62.08/10.53 % (2067932)Peak memory usage: 113 MB
% 62.08/10.53 % (2067932)Instructions burned: 128 (million)
% 62.08/10.53 % (2067934)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1822578635:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2981 on theBenchmark for (2981ds/114Mi)
% 62.08/10.53 % (2067936)lrs+10_1_sil=8000:sp=occurrence:random_seed=4047323806:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2980 on theBenchmark for (2980ds/907Mi)
% 62.08/10.53 % (2067934)Instruction limit reached!
% 62.08/10.53 % (2067934)------------------------------
% 62.08/10.53 % (2067934)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.08/10.53 % (2067934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.08/10.53 % (2067934)CaDiCaL version: 2.1.3
% 62.08/10.53 % (2067934)Termination reason: Instruction limit
% 62.08/10.53 % (2067934)Termination phase: Property scanning
% 62.08/10.53 % (2067934)Time elapsed: 0.051 s
% 62.08/10.53 % (2067934)Peak memory usage: 112 MB
% 62.08/10.53 % (2067934)Instructions burned: 116 (million)
% 62.08/10.53 % (2067937)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2814534508:i=437:sd=1:aac=none:ss=included_2979 on theBenchmark for (2979ds/437Mi)
% 62.08/10.53 % (2067940)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1292966512:i=5202:ss=axioms:sgt=16_2979 on theBenchmark for (2979ds/5202Mi)
% 62.08/10.53 % (2067928)Instruction limit reached!
% 62.08/10.53 % (2067928)------------------------------
% 62.08/10.53 % (2067928)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.08/10.53 % (2067928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.08/10.53 % (2067928)CaDiCaL version: 2.1.3
% 62.08/10.53 % (2067928)Termination reason: Instruction limit
% 62.08/10.53 % (2067928)Termination phase: Property scanning
% 62.08/10.53 % (2067928)Time elapsed: 0.732 s
% 62.08/10.53 % (2067928)Peak memory usage: 171 MB
% 62.08/10.53 % (2067928)Instructions burned: 2352 (million)
% 62.08/10.53 % (2067937)Instruction limit reached!
% 62.08/10.53 % (2067937)------------------------------
% 62.08/10.53 % (2067937)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.08/10.53 % (2067937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.08/10.53 % (2067937)CaDiCaL version: 2.1.3
% 62.08/10.53 % (2067937)Termination reason: Instruction limit
% 62.08/10.53 % (2067937)Termination phase: Saturation
% 62.08/10.53 % (2067937)Time elapsed: 0.304 s
% 62.08/10.53 % (2067937)Peak memory usage: 120 MB
% 62.08/10.53 % (2067937)Instructions burned: 437 (million)
% 62.08/10.53 % (2067943)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1943303015:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2975 on theBenchmark for (2975ds/134Mi)
% 62.08/10.53 % (2067936)Instruction limit reached!
% 62.08/10.53 % (2067936)------------------------------
% 62.08/10.53 % (2067936)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.08/10.53 % (2067936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.08/10.53 % (2067936)CaDiCaL version: 2.1.3
% 62.08/10.53 % (2067936)Termination reason: Instruction limit
% 62.08/10.53 % (2067936)Termination phase: Saturation
% 62.08/10.53 % (2067936)Time elapsed: 0.532 s
% 62.08/10.53 % (2067936)Peak memory usage: 131 MB
% 62.08/10.53 % (2067936)Instructions burned: 908 (million)
% 62.08/10.53 % (2067944)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=4091708467:st=8:i=592:sd=3:ep=RST:ss=axioms_2975 on theBenchmark for (2975ds/592Mi)
% 62.08/10.53 % (2067943)Instruction limit reached!
% 62.08/10.53 % (2067943)------------------------------
% 62.08/10.53 % (2067943)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.08/10.53 % (2067943)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.08/10.53 % (2067943)CaDiCaL version: 2.1.3
% 62.08/10.53 % (2067943)Termination reason: Instruction limit
% 62.08/10.53 % (2067943)Termination phase: NewCNF
% 62.08/10.53 % (2067943)Time elapsed: 0.073 s
% 62.08/10.53 % (2067943)Peak memory usage: 115 MB
% 62.08/10.53 % (2067943)Instructions burned: 136 (million)
% 62.08/10.53 % (2067946)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=109327526:st=3:i=13193:sd=3:ss=axioms_2973 on theBenchmark for (2973ds/13193Mi)
% 62.08/10.53 % (2067948)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=1969379860:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2973 on theBenchmark for (2973ds/125Mi)
% 84.79/13.77 % (2067948)Instruction limit reached!
% 84.79/13.77 % (2067948)------------------------------
% 84.79/13.77 % (2067948)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.79/13.77 % (2067948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.79/13.77 % (2067948)CaDiCaL version: 2.1.3
% 84.79/13.77 % (2067948)Termination reason: Instruction limit
% 84.79/13.77 % (2067948)Termination phase: Property scanning
% 84.79/13.77 % (2067948)Time elapsed: 0.029 s
% 84.79/13.77 % (2067948)Peak memory usage: 112 MB
% 84.79/13.77 % (2067948)Instructions burned: 126 (million)
% 84.79/13.77 % (2067951)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=729652635:i=134:gtgl=5:slsql=off:gtg=exists_sym_2971 on theBenchmark for (2971ds/134Mi)
% 84.79/13.77 % (2067951)Instruction limit reached!
% 84.79/13.77 % (2067951)------------------------------
% 84.79/13.77 % (2067951)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.79/13.77 % (2067951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.79/13.77 % (2067951)CaDiCaL version: 2.1.3
% 84.79/13.77 % (2067951)Termination reason: Instruction limit
% 84.79/13.77 % (2067951)Termination phase: Property scanning
% 84.79/13.77 % (2067951)Time elapsed: 0.032 s
% 84.79/13.77 % (2067951)Peak memory usage: 112 MB
% 84.79/13.77 % (2067951)Instructions burned: 137 (million)
% 84.79/13.77 % (2067944)Instruction limit reached!
% 84.79/13.77 % (2067944)------------------------------
% 84.79/13.77 % (2067944)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.79/13.77 % (2067944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.79/13.77 % (2067944)CaDiCaL version: 2.1.3
% 84.79/13.77 % (2067944)Termination reason: Instruction limit
% 84.79/13.77 % (2067944)Termination phase: Preprocessing 3
% 84.79/13.77 % (2067944)Time elapsed: 0.455 s
% 84.79/13.77 % (2067944)Peak memory usage: 134 MB
% 84.79/13.77 % (2067944)Instructions burned: 593 (million)
% 84.79/13.77 % (2067953)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3959821006:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2970 on theBenchmark for (2970ds/141Mi)
% 84.79/13.77 % (2067953)Instruction limit reached!
% 84.79/13.77 % (2067953)------------------------------
% 84.79/13.77 % (2067953)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.79/13.77 % (2067953)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.79/13.77 % (2067953)CaDiCaL version: 2.1.3
% 84.79/13.77 % (2067953)Termination reason: Instruction limit
% 84.79/13.77 % (2067953)Termination phase: Saturation
% 84.79/13.77 % (2067953)Time elapsed: 0.071 s
% 84.79/13.77 % (2067953)Peak memory usage: 117 MB
% 84.79/13.77 % (2067953)Instructions burned: 144 (million)
% 84.79/13.77 % (2067955)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1185990163:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2968 on theBenchmark for (2968ds/431Mi)
% 84.79/13.77 % (2067956)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=3047967118:i=6060:aac=none:ins=25_2968 on theBenchmark for (2968ds/6060Mi)
% 84.79/13.77 % (2067955)Instruction limit reached!
% 84.79/13.77 % (2067955)------------------------------
% 84.79/13.77 % (2067955)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.79/13.77 % (2067955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.79/13.77 % (2067955)CaDiCaL version: 2.1.3
% 84.79/13.77 % (2067955)Termination reason: Instruction limit
% 84.79/13.77 % (2067955)Termination phase: Saturation
% 84.79/13.77 % (2067955)Time elapsed: 0.296 s
% 84.79/13.77 % (2067955)Peak memory usage: 122 MB
% 84.79/13.77 % (2067955)Instructions burned: 432 (million)
% 84.79/13.77 % (2067959)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=1939559676:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2964 on theBenchmark for (2964ds/150Mi)
% 84.79/13.77 % (2067959)Instruction limit reached!
% 84.79/13.77 % (2067959)------------------------------
% 84.79/13.77 % (2067959)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.79/13.77 % (2067959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.79/13.77 % (2067959)CaDiCaL version: 2.1.3
% 84.79/13.77 % (2067959)Termination reason: Instruction limit
% 110.32/17.38 % (2067959)Termination phase: Preprocessing 1
% 110.32/17.38 % (2067959)Time elapsed: 0.120 s
% 110.32/17.38 % (2067959)Peak memory usage: 113 MB
% 110.32/17.38 % (2067959)Instructions burned: 150 (million)
% 110.32/17.38 % (2067961)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2364825585:i=14155:bd=all_2961 on theBenchmark for (2961ds/14155Mi)
% 110.32/17.38 % (2067956)Instruction limit reached!
% 110.32/17.38 % (2067956)------------------------------
% 110.32/17.38 % (2067956)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 110.32/17.38 % (2067956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.32/17.38 % (2067956)CaDiCaL version: 2.1.3
% 110.32/17.38 % (2067956)Termination reason: Instruction limit
% 110.32/17.38 % (2067956)Termination phase: Saturation
% 110.32/17.38 % (2067956)Time elapsed: 2.724 s
% 110.32/17.38 % (2067956)Peak memory usage: 612 MB
% 110.32/17.38 % (2067956)Instructions burned: 6061 (million)
% 110.32/17.38 % (2067963)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3374681411:i=667:av=off:fsr=off_2939 on theBenchmark for (2939ds/667Mi)
% 110.32/17.38 % (2067940)Instruction limit reached!
% 110.32/17.38 % (2067940)------------------------------
% 110.32/17.38 % (2067940)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 110.32/17.38 % (2067940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.32/17.38 % (2067940)CaDiCaL version: 2.1.3
% 110.32/17.38 % (2067940)Termination reason: Instruction limit
% 110.32/17.38 % (2067940)Termination phase: Saturation
% 110.32/17.38 % (2067940)Time elapsed: 4.084 s
% 110.32/17.38 % (2067940)Peak memory usage: 562 MB
% 110.32/17.38 % (2067940)Instructions burned: 5202 (million)
% 110.32/17.38 % (2067963)Instruction limit reached!
% 110.32/17.38 % (2067963)------------------------------
% 110.32/17.38 % (2067963)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 110.32/17.38 % (2067963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.32/17.38 % (2067963)CaDiCaL version: 2.1.3
% 110.32/17.38 % (2067963)Termination reason: Instruction limit
% 110.32/17.38 % (2067963)Termination phase: NewCNF
% 110.32/17.38 % (2067963)Time elapsed: 0.299 s
% 110.32/17.38 % (2067963)Peak memory usage: 149 MB
% 110.32/17.38 % (2067963)Instructions burned: 670 (million)
% 110.32/17.38 % (2067965)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=792903901:s2a=on:i=185:s2at=1.8:fdi=4_2935 on theBenchmark for (2935ds/185Mi)
% 110.32/17.38 % (2067966)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2119097172:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2934 on theBenchmark for (2934ds/193Mi)
% 110.32/17.38 % (2067965)Instruction limit reached!
% 110.32/17.38 % (2067965)------------------------------
% 110.32/17.38 % (2067965)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 110.32/17.38 % (2067965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.32/17.38 % (2067965)CaDiCaL version: 2.1.3
% 110.32/17.38 % (2067965)Termination reason: Instruction limit
% 110.32/17.38 % (2067965)Termination phase: SInE selection
% 110.32/17.38 % (2067965)Time elapsed: 0.148 s
% 110.32/17.38 % (2067965)Peak memory usage: 113 MB
% 110.32/17.38 % (2067965)Instructions burned: 185 (million)
% 110.32/17.38 % (2067966)Instruction limit reached!
% 110.32/17.38 % (2067966)------------------------------
% 110.32/17.38 % (2067966)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 110.32/17.38 % (2067966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.32/17.38 % (2067966)CaDiCaL version: 2.1.3
% 110.32/17.38 % (2067966)Termination reason: Instruction limit
% 110.32/17.38 % (2067966)Termination phase: SInE selection
% 110.32/17.38 % (2067966)Time elapsed: 0.089 s
% 110.32/17.38 % (2067966)Peak memory usage: 112 MB
% 110.32/17.38 % (2067966)Instructions burned: 193 (million)
% 110.32/17.38 % (2067970)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=4191756455:i=12111:sd=1:ss=included_2932 on theBenchmark for (2932ds/12111Mi)
% 110.32/17.38 % (2067969)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=1167189443:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2932 on theBenchmark for (2932ds/4850Mi)
% 110.32/17.38 % (2067969)Instruction limit reached!
% 110.32/17.38 % (2067969)------------------------------
% 110.32/17.38 % (2067969)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 138.76/21.35 % (2067969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.76/21.35 % (2067969)CaDiCaL version: 2.1.3
% 138.76/21.35 % (2067969)Termination reason: Instruction limit
% 138.76/21.35 % (2067969)Termination phase: Saturation
% 138.76/21.35 % (2067969)Time elapsed: 2.782 s
% 138.76/21.35 % (2067969)Peak memory usage: 218 MB
% 138.76/21.35 % (2067969)Instructions burned: 4851 (million)
% 138.76/21.35 % (2067973)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=245629796:i=319:kws=precedence:fsr=off_2903 on theBenchmark for (2903ds/319Mi)
% 138.76/21.35 % (2067973)Instruction limit reached!
% 138.76/21.35 % (2067973)------------------------------
% 138.76/21.35 % (2067973)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 138.76/21.35 % (2067973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.76/21.35 % (2067973)CaDiCaL version: 2.1.3
% 138.76/21.35 % (2067973)Termination reason: Instruction limit
% 138.76/21.35 % (2067973)Termination phase: Naming
% 138.76/21.35 % (2067973)Time elapsed: 0.265 s
% 138.76/21.35 % (2067973)Peak memory usage: 135 MB
% 138.76/21.35 % (2067973)Instructions burned: 320 (million)
% 138.76/21.35 % (2067975)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=2200254287:i=2064:ep=RST_2898 on theBenchmark for (2898ds/2064Mi)
% 138.76/21.35 % (2067946)Instruction limit reached!
% 138.76/21.35 % (2067946)------------------------------
% 138.76/21.35 % (2067946)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 138.76/21.35 % (2067946)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.76/21.35 % (2067946)CaDiCaL version: 2.1.3
% 138.76/21.35 % (2067946)Termination reason: Instruction limit
% 138.76/21.35 % (2067946)Termination phase: Saturation
% 138.76/21.35 % (2067946)Time elapsed: 8.073 s
% 138.76/21.35 % (2067946)Peak memory usage: 289 MB
% 138.76/21.35 % (2067946)Instructions burned: 13193 (million)
% 138.76/21.35 % (2067970)Instruction limit reached!
% 138.76/21.35 % (2067970)------------------------------
% 138.76/21.35 % (2067970)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 138.76/21.35 % (2067970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.76/21.35 % (2067970)CaDiCaL version: 2.1.3
% 138.76/21.35 % (2067970)Termination reason: Instruction limit
% 138.76/21.35 % (2067970)Termination phase: Saturation
% 138.76/21.35 % (2067970)Time elapsed: 4.163 s
% 138.76/21.35 % (2067970)Peak memory usage: 278 MB
% 138.76/21.35 % (2067970)Instructions burned: 12114 (million)
% 138.76/21.35 % (2067977)dis-1011_128_sil=32000:random_seed=4150542755:i=3706:ep=RST:av=off_2891 on theBenchmark for (2891ds/3706Mi)
% 138.76/21.35 % (2067979)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=3633996853:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2889 on theBenchmark for (2889ds/757Mi)
% 138.76/21.35 % (2067975)Instruction limit reached!
% 138.76/21.35 % (2067975)------------------------------
% 138.76/21.35 % (2067975)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 138.76/21.35 % (2067975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.76/21.35 % (2067975)CaDiCaL version: 2.1.3
% 138.76/21.35 % (2067975)Termination reason: Instruction limit
% 138.76/21.35 % (2067975)Termination phase: Property scanning
% 138.76/21.35 % (2067975)Time elapsed: 1.112 s
% 138.76/21.35 % (2067975)Peak memory usage: 171 MB
% 138.76/21.35 % (2067975)Instructions burned: 2064 (million)
% 138.76/21.35 % (2067979)Instruction limit reached!
% 138.76/21.35 % (2067979)------------------------------
% 138.76/21.35 % (2067979)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 138.76/21.35 % (2067979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.76/21.35 % (2067979)CaDiCaL version: 2.1.3
% 138.76/21.35 % (2067979)Termination reason: Instruction limit
% 138.76/21.35 % (2067979)Termination phase: Saturation
% 138.76/21.35 % (2067979)Time elapsed: 0.316 s
% 138.76/21.35 % (2067979)Peak memory usage: 123 MB
% 138.76/21.35 % (2067979)Instructions burned: 758 (million)
% 138.76/21.35 % (2067981)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=3232270389:i=13913:ss=axioms:sgt=8_2885 on theBenchmark for (2885ds/13913Mi)
% 138.76/21.35 % (2067982)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=921727091:i=9925:aac=none_2885 on theBenchmark for (2885ds/9925Mi)
% 138.76/21.35 % (2067977)Instruction limit reached!
% 138.76/21.35 % (2067977)------------------------------
% 138.76/21.35 % (2067977)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 166.43/25.27 % (2067977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 166.43/25.27 % (2067977)CaDiCaL version: 2.1.3
% 166.43/25.27 % (2067977)Termination reason: Instruction limit
% 166.43/25.27 % (2067977)Termination phase: Saturation
% 166.43/25.27 % (2067977)Time elapsed: 1.862 s
% 166.43/25.27 % (2067977)Peak memory usage: 186 MB
% 166.43/25.27 % (2067977)Instructions burned: 3707 (million)
% 166.43/25.27 % (2067985)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=3914325247:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2870 on theBenchmark for (2870ds/2479Mi)
% 166.43/25.27 % (2067961)Instruction limit reached!
% 166.43/25.27 % (2067961)------------------------------
% 166.43/25.27 % (2067961)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 166.43/25.27 % (2067961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 166.43/25.27 % (2067961)CaDiCaL version: 2.1.3
% 166.43/25.27 % (2067961)Termination reason: Instruction limit
% 166.43/25.27 % (2067961)Termination phase: Saturation
% 166.43/25.27 % (2067961)Time elapsed: 9.633 s
% 166.43/25.27 % (2067961)Peak memory usage: 504 MB
% 166.43/25.27 % (2067961)Instructions burned: 14155 (million)
% 166.43/25.27 % (2067987)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=1416474765:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2862 on theBenchmark for (2862ds/440Mi)
% 166.43/25.27 % (2067987)Instruction limit reached!
% 166.43/25.27 % (2067987)------------------------------
% 166.43/25.27 % (2067987)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 166.43/25.27 % (2067987)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 166.43/25.27 % (2067987)CaDiCaL version: 2.1.3
% 166.43/25.27 % (2067987)Termination reason: Instruction limit
% 166.43/25.27 % (2067987)Termination phase: Property scanning
% 166.43/25.27 % (2067987)Time elapsed: 0.191 s
% 166.43/25.27 % (2067987)Peak memory usage: 112 MB
% 166.43/25.27 % (2067987)Instructions burned: 443 (million)
% 166.43/25.27 % (2067989)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=4180752111:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2859 on theBenchmark for (2859ds/11145Mi)
% 166.43/25.27 % (2067985)Instruction limit reached!
% 166.43/25.27 % (2067985)------------------------------
% 166.43/25.27 % (2067985)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 166.43/25.27 % (2067985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 166.43/25.27 % (2067985)CaDiCaL version: 2.1.3
% 166.43/25.27 % (2067985)Termination reason: Instruction limit
% 166.43/25.27 % (2067985)Termination phase: Saturation
% 166.43/25.27 % (2067985)Time elapsed: 1.778 s
% 166.43/25.27 % (2067985)Peak memory usage: 133 MB
% 166.43/25.27 % (2067985)Instructions burned: 2480 (million)
% 166.43/25.27 % (2067991)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=282856611:cts=off:i=3034:av=off:er=known:fsd=on_2851 on theBenchmark for (2851ds/3034Mi)
% 166.43/25.27 % (2067982)Instruction limit reached!
% 166.43/25.27 % (2067982)------------------------------
% 166.43/25.27 % (2067982)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 166.43/25.27 % (2067982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 166.43/25.27 % (2067982)CaDiCaL version: 2.1.3
% 166.43/25.27 % (2067982)Termination reason: Instruction limit
% 166.43/25.27 % (2067982)Termination phase: Saturation
% 166.43/25.27 % (2067982)Time elapsed: 4.347 s
% 166.43/25.27 % (2067982)Peak memory usage: 514 MB
% 166.43/25.27 % (2067982)Instructions burned: 9929 (million)
% 166.43/25.27 % (2067993)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=2262363339:st=2:s2a=on:i=524:s2at=2:ss=axioms_2840 on theBenchmark for (2840ds/524Mi)
% 166.43/25.27 % (2067993)Instruction limit reached!
% 166.43/25.27 % (2067993)------------------------------
% 166.43/25.27 % (2067993)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 166.43/25.27 % (2067993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 166.43/25.27 % (2067993)CaDiCaL version: 2.1.3
% 166.43/25.27 % (2067993)Termination reason: Instruction limit
% 166.43/25.27 % (2067993)Termination phase: Preprocessing 1
% 166.43/25.27 % (2067993)Time elapsed: 0.234 s
% 166.43/25.27 % (2067993)Peak memory usage: 114 MB
% 166.43/25.27 % (2067993)Instructions burned: 528 (million)
% 166.43/25.27 % (2067995)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=1798257332:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2836 on theBenchmark for (2836ds/1016Mi)
% 100.89/28.11 % (2067991)Instruction limit reached!
% 100.89/28.11 % (2067991)------------------------------
% 100.89/28.11 % (2067991)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.89/28.11 % (2067991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.89/28.11 % (2067991)CaDiCaL version: 2.1.3
% 100.89/28.11 % (2067991)Termination reason: Instruction limit
% 100.89/28.11 % (2067991)Termination phase: Saturation
% 100.89/28.11 % (2067991)Time elapsed: 1.658 s
% 100.89/28.11 % (2067991)Peak memory usage: 190 MB
% 100.89/28.11 % (2067991)Instructions burned: 3035 (million)
% 100.89/28.11 % (2067995)Instruction limit reached!
% 100.89/28.11 % (2067995)------------------------------
% 100.89/28.11 % (2067995)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.89/28.11 % (2067995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.89/28.11 % (2067995)CaDiCaL version: 2.1.3
% 100.89/28.11 % (2067995)Termination reason: Instruction limit
% 100.89/28.11 % (2067995)Termination phase: Saturation
% 100.89/28.11 % (2067995)Time elapsed: 0.302 s
% 100.89/28.11 % (2067995)Peak memory usage: 130 MB
% 100.89/28.11 % (2067995)Instructions burned: 1019 (million)
% 100.89/28.11 % (2067997)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=1290815980:i=14123:bd=preordered:ins=4_2832 on theBenchmark for (2832ds/14123Mi)
% 100.89/28.11 % (2067998)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=3876130491:i=5781:kws=precedence:bd=all:rawr=on_2831 on theBenchmark for (2831ds/5781Mi)
% 100.89/28.11 % (2067998)Instruction limit reached!
% 100.89/28.11 % (2067998)------------------------------
% 100.89/28.11 % (2067998)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.89/28.11 % (2067998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.89/28.11 % (2067998)CaDiCaL version: 2.1.3
% 100.89/28.11 % (2067998)Termination reason: Instruction limit
% 100.89/28.11 % (2067998)Termination phase: Saturation
% 100.89/28.11 % (2067998)Time elapsed: 1.734 s
% 100.89/28.11 % (2067998)Peak memory usage: 201 MB
% 100.89/28.11 % (2067998)Instructions burned: 5784 (million)
% 100.89/28.11 % (2068001)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=3239123429:i=2448:gtgl=5:bd=preordered:gtg=all_2812 on theBenchmark for (2812ds/2448Mi)
% 100.89/28.11 % (2067981)Instruction limit reached!
% 100.89/28.11 % (2067981)------------------------------
% 100.89/28.11 % (2067981)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.89/28.11 % (2067981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.89/28.11 % (2067981)CaDiCaL version: 2.1.3
% 100.89/28.11 % (2067981)Termination reason: Instruction limit
% 100.89/28.11 % (2067981)Termination phase: Saturation
% 100.89/28.11 % (2067981)Time elapsed: 7.970 s
% 100.89/28.11 % (2067981)Peak memory usage: 278 MB
% 100.89/28.11 % (2067981)Instructions burned: 13914 (million)
% 100.89/28.11 % (2068001)Instruction limit reached!
% 100.89/28.11 % (2068001)------------------------------
% 100.89/28.11 % (2068001)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.89/28.11 % (2068001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.89/28.11 % (2068001)CaDiCaL version: 2.1.3
% 100.89/28.11 % (2068001)Termination reason: Instruction limit
% 100.89/28.11 % (2068001)Termination phase: Function definition elimination
% 100.89/28.11 % (2068001)Time elapsed: 0.752 s
% 100.89/28.11 % (2068001)Peak memory usage: 168 MB
% 100.89/28.11 % (2068001)Instructions burned: 2450 (million)
% 100.89/28.11 % (2068004)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=2937567160:st=5.6:i=2033:sd=3:ss=axioms_2803 on theBenchmark for (2803ds/2033Mi)
% 100.89/28.11 % (2068003)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=1191189965:i=3223:kws=precedence:fgj=on:av=off_2804 on theBenchmark for (2804ds/3223Mi)
% 100.89/28.11 % (2068004)Instruction limit reached!
% 100.89/28.11 % (2068004)------------------------------
% 100.89/28.11 % (2068004)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.89/28.11 % (2068004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.89/28.11 % (2068004)CaDiCaL version: 2.1.3
% 100.89/28.11 % (2068004)Termination reason: Instruction limit
% 100.89/28.11 % (2068004)Termination phase: Saturation
% 100.89/28.11 % (2068004)Time elapsed: 0.746 s
% 100.89/28.11 % (2068004)Peak memory usage: 197 MB
% 100.89/28.11 % (2068004)Instructions burned: 2036 (million)
% 100.89/28.11 % (2068007)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=1677380366:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2794 on theBenchmark for (2794ds/2055Mi)
% 100.89/28.11 % (2068007)Instruction limit reached!
% 100.89/28.11 % (2068007)------------------------------
% 100.89/28.11 % (2068007)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.89/28.11 % (2068007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.89/28.11 % (2068007)CaDiCaL version: 2.1.3
% 100.89/28.11 % (2068007)Termination reason: Instruction limit
% 100.89/28.11 % (2068007)Termination phase: Saturation
% 100.89/28.11 % (2068007)Time elapsed: 0.712 s
% 100.89/28.11 % (2068007)Peak memory usage: 178 MB
% 100.89/28.11 % (2068007)Instructions burned: 2058 (million)
% 100.89/28.11 % (2067989)Instruction limit reached!
% 100.89/28.11 % (2067989)------------------------------
% 100.89/28.11 % (2067989)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.89/28.11 % (2067989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.89/28.11 % (2067989)CaDiCaL version: 2.1.3
% 100.89/28.11 % (2067989)Termination reason: Instruction limit
% 100.89/28.11 % (2067989)Termination phase: Saturation
% 100.89/28.11 % (2067989)Time elapsed: 7.180 s
% 100.89/28.11 % (2067989)Peak memory usage: 248 MB
% 100.89/28.11 % (2067989)Instructions burned: 11147 (million)
% 100.89/28.11 % (2068009)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=817629166:i=21611:sd=3:ss=axioms_2786 on theBenchmark for (2786ds/21611Mi)
% 100.89/28.11 % (2068003)Instruction limit reached!
% 100.89/28.11 % (2068003)------------------------------
% 100.89/28.11 % (2068003)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.89/28.11 % (2068003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.89/28.11 % (2068003)CaDiCaL version: 2.1.3
% 100.89/28.11 % (2068003)Termination reason: Instruction limit
% 100.89/28.11 % (2068003)Termination phase: Saturation
% 100.89/28.11 % (2068003)Time elapsed: 1.839 s
% 100.89/28.11 % (2068003)Peak memory usage: 215 MB
% 100.89/28.11 % (2068003)Instructions burned: 3223 (million)
% 100.89/28.11 % (2068010)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=118913904:i=4835:sd=13:ss=axioms:sgt=23_2785 on theBenchmark for (2785ds/4835Mi)
% 100.89/28.11 % (2068012)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=2647438386:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2783 on theBenchmark for (2783ds/797Mi)
% 100.89/28.11 % (2068012)Instruction limit reached!
% 100.89/28.11 % (2068012)------------------------------
% 100.89/28.11 % (2068012)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.89/28.11 % (2068012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.89/28.11 % (2068012)CaDiCaL version: 2.1.3
% 100.89/28.11 % (2068012)Termination reason: Instruction limit
% 100.89/28.11 % (2068012)Termination phase: NewCNF
% 100.89/28.11 % (2068012)Time elapsed: 0.649 s
% 100.89/28.11 % (2068012)Peak memory usage: 138 MB
% 100.89/28.11 % (2068012)Instructions burned: 798 (million)
% 100.89/28.11 % (2068015)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=3679048461:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2775 on theBenchmark for (2775ds/2326Mi)
% 100.89/28.11 % (2068015)Instruction limit reached!
% 100.89/28.11 % (2068015)------------------------------
% 100.89/28.11 % (2068015)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.89/28.11 % (2068015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.89/28.11 % (2068015)CaDiCaL version: 2.1.3
% 100.89/28.11 % (2068015)Termination reason: Instruction limit
% 100.89/28.11 % (2068015)Termination phase: Property scanning
% 100.89/28.11 % (2068015)Time elapsed: 1.216 s
% 100.89/28.11 % (2068015)Peak memory usage: 178 MB
% 100.89/28.11 % (2068015)Instructions burned: 2328 (million)
% 100.89/28.11 % (2068017)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=3053114781:i=6038:nm=6_2761 on theBenchmark for (2761ds/6038Mi)
% 100.89/28.11 % (2068010)Instruction limit reached!
% 100.89/28.11 % (2068010)------------------------------
% 100.89/28.11 % (2068010)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.89/28.11 % (2068010)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.89/28.11 % (2068010)CaDiCaL version: 2.1.3
% 100.89/28.11 % (2068010)Termination reason: Instruction limit
% 100.89/28.11 % (2068010)Termination phase: Saturation
% 100.89/28.11 % (2068010)Time elapsed: 2.796 s
% 100.89/28.11 % (2068010)Peak memory usage: 227 MB
% 100.89/28.11 % (2068010)Instructions burned: 4835 (million)
% 100.89/28.11 % (2068019)lrs+10_1_sil=32000:sp=occurrence:random_seed=4056692510:st=2:i=33334:sd=3:ss=included:sgt=32_2755 on theBenchmark for (2755ds/33334Mi)
% 100.89/28.11 % (2067997)Instruction limit reached!
% 100.89/28.11 % (2067997)------------------------------
% 100.89/28.11 % (2067997)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.89/28.11 % (2067997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.89/28.11 % (2067997)CaDiCaL version: 2.1.3
% 100.89/28.11 % (2067997)Termination reason: Instruction limit
% 100.89/28.11 % (2067997)Termination phase: Saturation
% 100.89/28.11 % (2067997)Time elapsed: 9.780 s
% 100.89/28.11 % (2067997)Peak memory usage: 669 MB
% 100.89/28.11 % (2067997)Instructions burned: 14124 (million)
% 100.89/28.11 % (2068021)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=2574939367:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2732 on theBenchmark for (2732ds/1008Mi)
% 100.89/28.11 % (2068009)First to succeed.
% 100.89/28.11 % (2068009)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2067900"
% 100.89/28.11 % (2068009)Refutation found. Thanks to Tanya!
% 100.89/28.11 % SZS status Theorem for theBenchmark
% 100.89/28.11 % SZS output start Proof for theBenchmark
% See solution above
% 186.96/28.21 % (2068009)------------------------------
% 186.96/28.21 % (2068009)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 186.96/28.21 % (2068009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 186.96/28.21 % (2068009)CaDiCaL version: 2.1.3
% 186.96/28.21 % (2068009)Termination reason: Refutation
% 186.96/28.21 % (2068009)Time elapsed: 5.470 s
% 186.96/28.21 % (2068009)Peak memory usage: 274 MB
% 186.96/28.21 % (2068009)Instructions burned: 16402 (million)
% 186.96/28.21 % (2068009)------------------------------
% 186.96/28.21 % (2068009)------------------------------
% 186.96/28.21 % (2067900)Success in time 27.249 s
% 186.96/28.21 % Vampire exiting
%------------------------------------------------------------------------------