%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU433+4 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:49:01 PM UTC 2026
% Result : Theorem 236.09s 44.35s
% Output : Refutation 274.81s
% Verified :
% SZS Type : Refutation
% Derivation depth : 34
% Number of leaves : 64
% Syntax : Number of formulae : 432 ( 70 unt; 46 def)
% Number of atoms : 2325 ( 132 equ)
% Maximal formula atoms : 20 ( 5 avg)
% Number of connectives : 3528 (1635 ~;1748 |; 69 &)
% ( 51 <=>; 24 =>; 0 <=; 1 <~>)
% Maximal formula depth : 24 ( 7 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 44 ( 42 usr; 39 prp; 0-2 aty)
% Number of functors : 28 ( 28 usr; 13 con; 0-4 aty)
% Number of variables : 470 ( 0 sgn 448 !; 22 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X0,X1] :
( ! [X2] :
( r2_hidden(X2,X0)
<=> r2_hidden(X2,X1) )
=> X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2_tarski) ).
fof(f4,axiom,
! [X0,X1] :
( X1 = k1_tarski(X0)
<=> ! [X2] :
( r2_hidden(X2,X1)
<=> X2 = X0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_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/sandbox2/benchmark/theBenchmark.p',d3_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/sandbox2/benchmark/theBenchmark.p',dt_k5_subset_1) ).
fof(f572,axiom,
! [X0,X1,X2] :
( ( m1_subset_1(X1,k1_zfmisc_1(X0))
& m1_subset_1(X2,k1_zfmisc_1(X0)) )
=> k5_subset_1(X0,X1,X2) = k5_subset_1(X0,X2,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_k5_subset_1) ).
fof(f574,axiom,
! [X0,X1,X2] :
( ( m1_subset_1(X1,k1_zfmisc_1(X0))
& m1_subset_1(X2,k1_zfmisc_1(X0)) )
=> k5_subset_1(X0,X1,X2) = k3_xboole_0(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k5_subset_1) ).
fof(f678,axiom,
! [X0,X1,X2] :
( ( r2_hidden(X0,X1)
& m1_subset_1(X1,k1_zfmisc_1(X2)) )
=> m1_subset_1(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t4_subset) ).
fof(f679,axiom,
! [X0,X1,X2] :
~ ( r2_hidden(X0,X1)
& m1_subset_1(X1,k1_zfmisc_1(X2))
& v1_xboole_0(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_subset) ).
fof(f849,axiom,
! [X0] :
( v1_relat_1(X0)
=> ! [X1,X2] :
( X2 = k9_relat_1(X0,X1)
<=> ! [X3] :
( r2_hidden(X3,X2)
<=> ? [X4] :
( r2_hidden(k4_tarski(X4,X3),X0)
& r2_hidden(X4,X1) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d13_relat_1) ).
fof(f1422,axiom,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
=> v1_relat_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc1_relset_1) ).
fof(f71075,axiom,
! [X0,X1,X2,X3] :
( ( m1_subset_1(X2,k1_zfmisc_1(X0))
& m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) )
=> m1_subset_1(k8_relset_2(X0,X1,X2,X3),k1_zfmisc_1(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k8_relset_2) ).
fof(f71088,axiom,
! [X0,X1,X2] :
( v1_relat_1(X2)
=> ( r2_hidden(X0,k9_relat_1(X2,k1_tarski(X1)))
<=> r2_hidden(k4_tarski(X1,X0),X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t9_relset_2) ).
fof(f71106,axiom,
! [X0,X1,X2,X3] :
( m1_subset_1(X3,k1_zfmisc_1(X0))
=> ! [X4] :
( m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
=> ( r2_hidden(X2,k8_relset_2(X0,X1,X3,X4))
=> ! [X5] :
( r2_hidden(X5,X3)
=> r2_hidden(X2,k9_relat_1(X4,k1_tarski(X5))) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t24_relset_2) ).
fof(f71107,axiom,
! [X0] :
( ~ v1_xboole_0(X0)
=> ! [X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(X1))
=> ! [X3] :
( m1_subset_1(X3,X0)
=> ! [X4] :
( m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X1,X0)))
=> ( r2_hidden(X3,k8_relset_2(X1,X0,X2,X4))
<=> ! [X5] :
( r2_hidden(X5,X2)
=> r2_hidden(X3,k9_relat_1(X4,k1_tarski(X5))) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t25_relset_2) ).
fof(f71116,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/sandbox2/benchmark/theBenchmark.p',t34_relset_2) ).
fof(f71117,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)],[f71116]) ).
fof(f71176,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,[],[f71117]) ).
fof(f71186,plain,
! [X0,X1,X2] :
( v1_relat_1(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(ennf_transformation,[],[f1422]) ).
fof(f71200,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(f71201,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,[],[f71200]) ).
fof(f71202,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(f71203,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,[],[f71202]) ).
fof(f71212,plain,
! [X0] :
( ! [X1,X2] :
( ! [X3] :
( ! [X4] :
( ( r2_hidden(X3,k8_relset_2(X1,X0,X2,X4))
<=> ! [X5] :
( r2_hidden(X3,k9_relat_1(X4,k1_tarski(X5)))
| ~ r2_hidden(X5,X2) ) )
| ~ m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X1,X0))) )
| ~ m1_subset_1(X3,X0) )
| ~ m1_subset_1(X2,k1_zfmisc_1(X1)) )
| v1_xboole_0(X0) ),
inference(ennf_transformation,[],[f71107]) ).
fof(f71213,plain,
! [X0,X1,X2,X3] :
( ! [X4] :
( ! [X5] :
( r2_hidden(X2,k9_relat_1(X4,k1_tarski(X5)))
| ~ r2_hidden(X5,X3) )
| ~ r2_hidden(X2,k8_relset_2(X0,X1,X3,X4))
| ~ m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) )
| ~ m1_subset_1(X3,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f71106]) ).
fof(f71214,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,[],[f71213]) ).
fof(f71215,plain,
! [X0,X1,X2,X3] :
( m1_subset_1(k8_relset_2(X0,X1,X2,X3),k1_zfmisc_1(X1))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| ~ m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(ennf_transformation,[],[f71075]) ).
fof(f71216,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,[],[f71215]) ).
fof(f71226,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(f71227,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(f71228,plain,
! [X0,X1,X2] :
( m1_subset_1(X0,X2)
| ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2)) ),
inference(flattening,[],[f71227]) ).
fof(f71241,plain,
! [X0,X1] :
( X0 = X1
| ? [X2] :
( r2_hidden(X2,X0)
<~> r2_hidden(X2,X1) ) ),
inference(ennf_transformation,[],[f3]) ).
fof(f71356,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,[],[f71088]) ).
fof(f71459,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(f71688,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(f71689,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,[],[f71688]) ).
fof(f72605,plain,
( k8_relset_2(sK22,sK23,sK24,k5_subset_1(k2_zfmisc_1(sK22,sK23),sK25,sK26)) != k5_subset_1(sK23,k8_relset_2(sK22,sK23,sK24,sK25),k8_relset_2(sK22,sK23,sK24,sK26))
& m1_subset_1(sK26,k1_zfmisc_1(k2_zfmisc_1(sK22,sK23)))
& m1_subset_1(sK25,k1_zfmisc_1(k2_zfmisc_1(sK22,sK23)))
& m1_subset_1(sK24,k1_zfmisc_1(sK22)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK22,sK23,sK24,sK25,sK26]),skolemize(X0,sK22),skolemize(X1,sK23),skolemize(X2,sK24),skolemize(X3,sK25),skolemize(X4,sK26)],[f71176]) ).
fof(f72614,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,[],[f71212]) ).
fof(f72615,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,[],[f72614]) ).
fof(f72616,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(sK33(X2,X3,X4))))
& r2_hidden(sK33(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,[sK33]),skolemize(X5,sK33(X2,X3,X4))],[f72615]) ).
fof(f72637,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,[],[f71241]) ).
fof(f72638,plain,
! [X0,X1] :
( X0 = X1
| ( ( ~ r2_hidden(sK46(X0,X1),X1)
| ~ r2_hidden(sK46(X0,X1),X0) )
& ( r2_hidden(sK46(X0,X1),X1)
| r2_hidden(sK46(X0,X1),X0) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK46]),skolemize(X2,sK46(X0,X1))],[f72637]) ).
fof(f72661,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(f72662,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,[],[f72661]) ).
fof(f72663,plain,
! [X0,X1] :
( ( X1 = k1_tarski(X0)
| ( ( sK60(X0,X1) != X0
| ~ r2_hidden(sK60(X0,X1),X1) )
& ( sK60(X0,X1) = X0
| r2_hidden(sK60(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,[sK60]),skolemize(X2,sK60(X0,X1))],[f72662]) ).
fof(f72682,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,[],[f71356]) ).
fof(f72707,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,[],[f71459]) ).
fof(f72708,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,[],[f72707]) ).
fof(f72709,plain,
! [X0] :
( ! [X1,X2] :
( ( X2 = k9_relat_1(X0,X1)
| ( ( ! [X4] :
( ~ r2_hidden(k4_tarski(X4,sK87(X0,X1,X2)),X0)
| ~ r2_hidden(X4,X1) )
| ~ r2_hidden(sK87(X0,X1,X2),X2) )
& ( ( r2_hidden(k4_tarski(sK88(X0,X1,X2),sK87(X0,X1,X2)),X0)
& r2_hidden(sK88(X0,X1,X2),X1) )
| r2_hidden(sK87(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(sK89(X0,X1,X6),X6),X0)
& r2_hidden(sK89(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,[sK87,sK88,sK89]),skolemize(X3,sK87(X0,X1,X2)),skolemize(X5,sK88(X0,X1,X2)),skolemize(X8,sK89(X0,X1,X6))],[f72708]) ).
fof(f72811,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(f72812,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,[],[f72811]) ).
fof(f72813,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,[],[f72812]) ).
fof(f72814,plain,
! [X0,X1,X2] :
( ( X2 = k3_xboole_0(X0,X1)
| ( ( ~ r2_hidden(sK154(X0,X1,X2),X0)
| ~ r2_hidden(sK154(X0,X1,X2),X1)
| ~ r2_hidden(sK154(X0,X1,X2),X2) )
& ( ( r2_hidden(sK154(X0,X1,X2),X0)
& r2_hidden(sK154(X0,X1,X2),X1) )
| r2_hidden(sK154(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,[sK154]),skolemize(X3,sK154(X0,X1,X2))],[f72813]) ).
fof(f73133,plain,
m1_subset_1(sK24,k1_zfmisc_1(sK22)),
inference(cnf_transformation,[],[f72605]) ).
fof(f73134,plain,
m1_subset_1(sK25,k1_zfmisc_1(k2_zfmisc_1(sK22,sK23))),
inference(cnf_transformation,[],[f72605]) ).
fof(f73135,plain,
m1_subset_1(sK26,k1_zfmisc_1(k2_zfmisc_1(sK22,sK23))),
inference(cnf_transformation,[],[f72605]) ).
fof(f73136,plain,
k8_relset_2(sK22,sK23,sK24,k5_subset_1(k2_zfmisc_1(sK22,sK23),sK25,sK26)) != k5_subset_1(sK23,k8_relset_2(sK22,sK23,sK24,sK25),k8_relset_2(sK22,sK23,sK24,sK26)),
inference(cnf_transformation,[],[f72605]) ).
fof(f73155,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| v1_relat_1(X2) ),
inference(cnf_transformation,[],[f71186]) ).
fof(f73171,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,[],[f71201]) ).
fof(f73172,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,[],[f71203]) ).
fof(f73182,plain,
! [X2,X3,X0,X1,X4] :
( r2_hidden(X3,k8_relset_2(X1,X0,X2,X4))
| r2_hidden(sK33(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,[],[f72616]) ).
fof(f73183,plain,
! [X2,X3,X0,X1,X4] :
( ~ r2_hidden(X3,k9_relat_1(X4,k1_tarski(sK33(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,[],[f72616]) ).
fof(f73184,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,[],[f71214]) ).
fof(f73185,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,[],[f71216]) ).
fof(f73212,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ r2_hidden(X0,X1)
| ~ v1_xboole_0(X2) ),
inference(cnf_transformation,[],[f71226]) ).
fof(f73213,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ r2_hidden(X0,X1)
| m1_subset_1(X0,X2) ),
inference(cnf_transformation,[],[f71228]) ).
fof(f73231,plain,
! [X0,X1] :
( r2_hidden(sK46(X0,X1),X1)
| X0 = X1
| r2_hidden(sK46(X0,X1),X0) ),
inference(cnf_transformation,[],[f72638]) ).
fof(f73232,plain,
! [X0,X1] :
( ~ r2_hidden(sK46(X0,X1),X1)
| X0 = X1
| ~ r2_hidden(sK46(X0,X1),X0) ),
inference(cnf_transformation,[],[f72638]) ).
fof(f73309,plain,
! [X3,X0,X1] :
( r2_hidden(X3,X1)
| X0 != X3
| k1_tarski(X0) != X1 ),
inference(cnf_transformation,[],[f72663]) ).
fof(f73396,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,[],[f72682]) ).
fof(f73397,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,[],[f72682]) ).
fof(f73501,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,[],[f72709]) ).
fof(f73904,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,[],[f71689]) ).
fof(f73960,plain,
! [X2,X0,X1,X4] :
( r2_hidden(X4,X1)
| ~ r2_hidden(X4,X2)
| k3_xboole_0(X0,X1) != X2 ),
inference(cnf_transformation,[],[f72814]) ).
fof(f73962,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,[],[f72814]) ).
fof(f75161,plain,
! [X3,X1] :
( r2_hidden(X3,X1)
| k1_tarski(X3) != X1 ),
inference(equality_resolution,[],[f73309]) ).
fof(f75162,plain,
! [X3] : r2_hidden(X3,k1_tarski(X3)),
inference(equality_resolution,[],[f75161]) ).
fof(f75182,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,[],[f73501]) ).
fof(f75214,plain,
! [X0,X1,X4] :
( r2_hidden(X4,k3_xboole_0(X0,X1))
| ~ r2_hidden(X4,X0)
| ~ r2_hidden(X4,X1) ),
inference(equality_resolution,[],[f73962]) ).
fof(f75216,plain,
! [X0,X1,X4] :
( ~ r2_hidden(X4,k3_xboole_0(X0,X1))
| r2_hidden(X4,X1) ),
inference(equality_resolution,[],[f73960]) ).
fof(f75328,definition,
sF388 = k2_zfmisc_1(sK22,sK23),
introduced(definition,[new_symbols(definition,[sF388])],[function_definition]) ).
fof(f75329,plain,
k2_zfmisc_1(sK22,sK23) = sF388,
inference(reorient_equations,[],[f75328]) ).
fof(f75330,definition,
sF389 = k5_subset_1(sF388,sK25,sK26),
introduced(definition,[new_symbols(definition,[sF389])],[function_definition]) ).
fof(f75331,plain,
k5_subset_1(sF388,sK25,sK26) = sF389,
inference(reorient_equations,[],[f75330]) ).
fof(f75332,definition,
sF390 = k8_relset_2(sK22,sK23,sK24,sF389),
introduced(definition,[new_symbols(definition,[sF390])],[function_definition]) ).
fof(f75333,plain,
k8_relset_2(sK22,sK23,sK24,sF389) = sF390,
inference(reorient_equations,[],[f75332]) ).
fof(f75334,definition,
sF391 = k8_relset_2(sK22,sK23,sK24,sK25),
introduced(definition,[new_symbols(definition,[sF391])],[function_definition]) ).
fof(f75335,plain,
k8_relset_2(sK22,sK23,sK24,sK25) = sF391,
inference(reorient_equations,[],[f75334]) ).
fof(f75336,definition,
sF392 = k8_relset_2(sK22,sK23,sK24,sK26),
introduced(definition,[new_symbols(definition,[sF392])],[function_definition]) ).
fof(f75337,plain,
k8_relset_2(sK22,sK23,sK24,sK26) = sF392,
inference(reorient_equations,[],[f75336]) ).
fof(f75338,definition,
sF393 = k5_subset_1(sK23,sF391,sF392),
introduced(definition,[new_symbols(definition,[sF393])],[function_definition]) ).
fof(f75339,plain,
k5_subset_1(sK23,sF391,sF392) = sF393,
inference(reorient_equations,[],[f75338]) ).
fof(f75340,plain,
sF390 != sF393,
inference(definition_folding,[],[f73136,f75339,f75337,f75335,f75333,f75331,f75329]) ).
fof(f75341,definition,
sF394 = k1_zfmisc_1(sF388),
introduced(definition,[new_symbols(definition,[sF394])],[function_definition]) ).
fof(f75342,plain,
k1_zfmisc_1(sF388) = sF394,
inference(reorient_equations,[],[f75341]) ).
fof(f75343,plain,
m1_subset_1(sK26,sF394),
inference(definition_folding,[],[f73135,f75342,f75329]) ).
fof(f75344,plain,
m1_subset_1(sK25,sF394),
inference(definition_folding,[],[f73134,f75342,f75329]) ).
fof(f75345,definition,
sF395 = k1_zfmisc_1(sK22),
introduced(definition,[new_symbols(definition,[sF395])],[function_definition]) ).
fof(f75346,plain,
k1_zfmisc_1(sK22) = sF395,
inference(reorient_equations,[],[f75345]) ).
fof(f75347,plain,
m1_subset_1(sK24,sF395),
inference(definition_folding,[],[f73133,f75346]) ).
fof(f75809,definition,
( spl396_91
<=> m1_subset_1(sK24,sF395) ),
introduced(definition,[new_symbols(definition,[spl396_91])],[avatar_definition]) ).
fof(f75811,plain,
( m1_subset_1(sK24,sF395)
| ~ spl396_91 ),
inference(avatar_component_clause,[],[f75809]) ).
fof(f75812,plain,
spl396_91,
inference(avatar_split_clause,[],[f75347,f75809]) ).
fof(f75814,definition,
( spl396_92
<=> m1_subset_1(sK25,sF394) ),
introduced(definition,[new_symbols(definition,[spl396_92])],[avatar_definition]) ).
fof(f75816,plain,
( m1_subset_1(sK25,sF394)
| ~ spl396_92 ),
inference(avatar_component_clause,[],[f75814]) ).
fof(f75817,plain,
spl396_92,
inference(avatar_split_clause,[],[f75344,f75814]) ).
fof(f75819,definition,
( spl396_93
<=> m1_subset_1(sK26,sF394) ),
introduced(definition,[new_symbols(definition,[spl396_93])],[avatar_definition]) ).
fof(f75821,plain,
( m1_subset_1(sK26,sF394)
| ~ spl396_93 ),
inference(avatar_component_clause,[],[f75819]) ).
fof(f75822,plain,
spl396_93,
inference(avatar_split_clause,[],[f75343,f75819]) ).
fof(f75824,definition,
( spl396_94
<=> sF390 = sF393 ),
introduced(definition,[new_symbols(definition,[spl396_94])],[avatar_definition]) ).
fof(f75826,plain,
( sF390 != sF393
| spl396_94 ),
inference(avatar_component_clause,[],[f75824]) ).
fof(f75827,plain,
~ spl396_94,
inference(avatar_split_clause,[],[f75340,f75824]) ).
fof(f75834,definition,
( spl396_96
<=> k2_zfmisc_1(sK22,sK23) = sF388 ),
introduced(definition,[new_symbols(definition,[spl396_96])],[avatar_definition]) ).
fof(f75836,plain,
( k2_zfmisc_1(sK22,sK23) = sF388
| ~ spl396_96 ),
inference(avatar_component_clause,[],[f75834]) ).
fof(f75837,plain,
spl396_96,
inference(avatar_split_clause,[],[f75329,f75834]) ).
fof(f75839,definition,
( spl396_97
<=> k5_subset_1(sF388,sK25,sK26) = sF389 ),
introduced(definition,[new_symbols(definition,[spl396_97])],[avatar_definition]) ).
fof(f75841,plain,
( k5_subset_1(sF388,sK25,sK26) = sF389
| ~ spl396_97 ),
inference(avatar_component_clause,[],[f75839]) ).
fof(f75842,plain,
spl396_97,
inference(avatar_split_clause,[],[f75331,f75839]) ).
fof(f75844,definition,
( spl396_98
<=> k8_relset_2(sK22,sK23,sK24,sF389) = sF390 ),
introduced(definition,[new_symbols(definition,[spl396_98])],[avatar_definition]) ).
fof(f75846,plain,
( k8_relset_2(sK22,sK23,sK24,sF389) = sF390
| ~ spl396_98 ),
inference(avatar_component_clause,[],[f75844]) ).
fof(f75847,plain,
spl396_98,
inference(avatar_split_clause,[],[f75333,f75844]) ).
fof(f75849,definition,
( spl396_99
<=> k8_relset_2(sK22,sK23,sK24,sK25) = sF391 ),
introduced(definition,[new_symbols(definition,[spl396_99])],[avatar_definition]) ).
fof(f75851,plain,
( k8_relset_2(sK22,sK23,sK24,sK25) = sF391
| ~ spl396_99 ),
inference(avatar_component_clause,[],[f75849]) ).
fof(f75852,plain,
spl396_99,
inference(avatar_split_clause,[],[f75335,f75849]) ).
fof(f75854,definition,
( spl396_100
<=> k8_relset_2(sK22,sK23,sK24,sK26) = sF392 ),
introduced(definition,[new_symbols(definition,[spl396_100])],[avatar_definition]) ).
fof(f75856,plain,
( k8_relset_2(sK22,sK23,sK24,sK26) = sF392
| ~ spl396_100 ),
inference(avatar_component_clause,[],[f75854]) ).
fof(f75857,plain,
spl396_100,
inference(avatar_split_clause,[],[f75337,f75854]) ).
fof(f75859,definition,
( spl396_101
<=> k5_subset_1(sK23,sF391,sF392) = sF393 ),
introduced(definition,[new_symbols(definition,[spl396_101])],[avatar_definition]) ).
fof(f75861,plain,
( k5_subset_1(sK23,sF391,sF392) = sF393
| ~ spl396_101 ),
inference(avatar_component_clause,[],[f75859]) ).
fof(f75862,plain,
spl396_101,
inference(avatar_split_clause,[],[f75339,f75859]) ).
fof(f75864,definition,
( spl396_102
<=> k1_zfmisc_1(sF388) = sF394 ),
introduced(definition,[new_symbols(definition,[spl396_102])],[avatar_definition]) ).
fof(f75866,plain,
( k1_zfmisc_1(sF388) = sF394
| ~ spl396_102 ),
inference(avatar_component_clause,[],[f75864]) ).
fof(f75867,plain,
spl396_102,
inference(avatar_split_clause,[],[f75342,f75864]) ).
fof(f75869,definition,
( spl396_103
<=> k1_zfmisc_1(sK22) = sF395 ),
introduced(definition,[new_symbols(definition,[spl396_103])],[avatar_definition]) ).
fof(f75871,plain,
( k1_zfmisc_1(sK22) = sF395
| ~ spl396_103 ),
inference(avatar_component_clause,[],[f75869]) ).
fof(f75872,plain,
spl396_103,
inference(avatar_split_clause,[],[f75346,f75869]) ).
fof(f75873,plain,
( m1_subset_1(sF390,k1_zfmisc_1(sK23))
| ~ m1_subset_1(sK24,k1_zfmisc_1(sK22))
| ~ m1_subset_1(sF389,k1_zfmisc_1(k2_zfmisc_1(sK22,sK23)))
| ~ spl396_98 ),
inference(superposition,[],[f73185,f75846]) ).
fof(f75875,definition,
( spl396_104
<=> m1_subset_1(sF389,k1_zfmisc_1(k2_zfmisc_1(sK22,sK23))) ),
introduced(definition,[new_symbols(definition,[spl396_104])],[avatar_definition]) ).
fof(f75877,plain,
( ~ m1_subset_1(sF389,k1_zfmisc_1(k2_zfmisc_1(sK22,sK23)))
| spl396_104 ),
inference(avatar_component_clause,[],[f75875]) ).
fof(f75879,definition,
( spl396_105
<=> m1_subset_1(sK24,k1_zfmisc_1(sK22)) ),
introduced(definition,[new_symbols(definition,[spl396_105])],[avatar_definition]) ).
fof(f75883,definition,
( spl396_106
<=> m1_subset_1(sF390,k1_zfmisc_1(sK23)) ),
introduced(definition,[new_symbols(definition,[spl396_106])],[avatar_definition]) ).
fof(f75885,plain,
( m1_subset_1(sF390,k1_zfmisc_1(sK23))
| ~ spl396_106 ),
inference(avatar_component_clause,[],[f75883]) ).
fof(f75886,plain,
( ~ spl396_104
| ~ spl396_105
| spl396_106
| ~ spl396_98 ),
inference(avatar_split_clause,[],[f75873,f75844,f75883,f75879,f75875]) ).
fof(f75888,plain,
( m1_subset_1(sF392,k1_zfmisc_1(sK23))
| ~ m1_subset_1(sK24,k1_zfmisc_1(sK22))
| ~ m1_subset_1(sK26,k1_zfmisc_1(k2_zfmisc_1(sK22,sK23)))
| ~ spl396_100 ),
inference(superposition,[],[f73185,f75856]) ).
fof(f75889,plain,
( ~ m1_subset_1(sK24,sF395)
| m1_subset_1(sF392,k1_zfmisc_1(sK23))
| ~ m1_subset_1(sK26,k1_zfmisc_1(k2_zfmisc_1(sK22,sK23)))
| ~ spl396_100
| ~ spl396_103 ),
inference(forward_demodulation,[],[f75888,f75871]) ).
fof(f75890,plain,
( m1_subset_1(sF392,k1_zfmisc_1(sK23))
| ~ m1_subset_1(sK26,k1_zfmisc_1(k2_zfmisc_1(sK22,sK23)))
| ~ spl396_91
| ~ spl396_100
| ~ spl396_103 ),
inference(forward_subsumption_resolution,[],[f75889,f75811]) ).
fof(f75892,definition,
( spl396_107
<=> m1_subset_1(sK26,k1_zfmisc_1(k2_zfmisc_1(sK22,sK23))) ),
introduced(definition,[new_symbols(definition,[spl396_107])],[avatar_definition]) ).
fof(f75896,definition,
( spl396_108
<=> m1_subset_1(sF392,k1_zfmisc_1(sK23)) ),
introduced(definition,[new_symbols(definition,[spl396_108])],[avatar_definition]) ).
fof(f75898,plain,
( m1_subset_1(sF392,k1_zfmisc_1(sK23))
| ~ spl396_108 ),
inference(avatar_component_clause,[],[f75896]) ).
fof(f75899,plain,
( ~ spl396_107
| spl396_108
| ~ spl396_91
| ~ spl396_100
| ~ spl396_103 ),
inference(avatar_split_clause,[],[f75890,f75869,f75854,f75809,f75896,f75892]) ).
fof(f75900,plain,
( k2_zfmisc_1(sK22,sK23) != sF388
| k1_zfmisc_1(sF388) != sF394
| m1_subset_1(sK26,k1_zfmisc_1(k2_zfmisc_1(sK22,sK23)))
| ~ m1_subset_1(sK26,sF394) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f75901,plain,
( m1_subset_1(sF391,k1_zfmisc_1(sK23))
| ~ m1_subset_1(sK24,k1_zfmisc_1(sK22))
| ~ m1_subset_1(sK25,k1_zfmisc_1(k2_zfmisc_1(sK22,sK23)))
| ~ spl396_99 ),
inference(superposition,[],[f73185,f75851]) ).
fof(f75902,plain,
( ~ m1_subset_1(sK24,sF395)
| m1_subset_1(sF391,k1_zfmisc_1(sK23))
| ~ m1_subset_1(sK25,k1_zfmisc_1(k2_zfmisc_1(sK22,sK23)))
| ~ spl396_99
| ~ spl396_103 ),
inference(forward_demodulation,[],[f75901,f75871]) ).
fof(f75903,plain,
( m1_subset_1(sF391,k1_zfmisc_1(sK23))
| ~ m1_subset_1(sK25,k1_zfmisc_1(k2_zfmisc_1(sK22,sK23)))
| ~ spl396_91
| ~ spl396_99
| ~ spl396_103 ),
inference(forward_subsumption_resolution,[],[f75902,f75811]) ).
fof(f75905,definition,
( spl396_109
<=> m1_subset_1(sK25,k1_zfmisc_1(k2_zfmisc_1(sK22,sK23))) ),
introduced(definition,[new_symbols(definition,[spl396_109])],[avatar_definition]) ).
fof(f75909,definition,
( spl396_110
<=> m1_subset_1(sF391,k1_zfmisc_1(sK23)) ),
introduced(definition,[new_symbols(definition,[spl396_110])],[avatar_definition]) ).
fof(f75911,plain,
( m1_subset_1(sF391,k1_zfmisc_1(sK23))
| ~ spl396_110 ),
inference(avatar_component_clause,[],[f75909]) ).
fof(f75912,plain,
( ~ spl396_109
| spl396_110
| ~ spl396_91
| ~ spl396_99
| ~ spl396_103 ),
inference(avatar_split_clause,[],[f75903,f75869,f75849,f75809,f75909,f75905]) ).
fof(f75913,plain,
( k2_zfmisc_1(sK22,sK23) != sF388
| k1_zfmisc_1(sF388) != sF394
| m1_subset_1(sK25,k1_zfmisc_1(k2_zfmisc_1(sK22,sK23)))
| ~ m1_subset_1(sK25,sF394) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f75916,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF388))
| v1_relat_1(X0) )
| ~ spl396_96 ),
inference(superposition,[],[f73155,f75836]) ).
fof(f75917,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF394)
| v1_relat_1(X0) )
| ~ spl396_96
| ~ spl396_102 ),
inference(forward_demodulation,[],[f75916,f75866]) ).
fof(f75918,plain,
( sF393 = k3_xboole_0(sF391,sF392)
| ~ m1_subset_1(sF391,k1_zfmisc_1(sK23))
| ~ m1_subset_1(sF392,k1_zfmisc_1(sK23))
| ~ spl396_101 ),
inference(superposition,[],[f73904,f75861]) ).
fof(f75921,plain,
( sF389 = k3_xboole_0(sK25,sK26)
| ~ m1_subset_1(sK25,k1_zfmisc_1(sF388))
| ~ m1_subset_1(sK26,k1_zfmisc_1(sF388))
| ~ spl396_97 ),
inference(superposition,[],[f75841,f73904]) ).
fof(f75922,plain,
( ~ m1_subset_1(sK25,sF394)
| sF389 = k3_xboole_0(sK25,sK26)
| ~ m1_subset_1(sK26,k1_zfmisc_1(sF388))
| ~ spl396_97
| ~ spl396_102 ),
inference(forward_demodulation,[],[f75921,f75866]) ).
fof(f75924,definition,
( spl396_111
<=> sF393 = k3_xboole_0(sF391,sF392) ),
introduced(definition,[new_symbols(definition,[spl396_111])],[avatar_definition]) ).
fof(f75926,plain,
( sF393 = k3_xboole_0(sF391,sF392)
| ~ spl396_111 ),
inference(avatar_component_clause,[],[f75924]) ).
fof(f75929,plain,
( ~ spl396_108
| ~ spl396_110
| spl396_111
| ~ spl396_101 ),
inference(avatar_split_clause,[],[f75918,f75859,f75924,f75909,f75896]) ).
fof(f75930,plain,
( sF389 = k3_xboole_0(sK25,sK26)
| ~ m1_subset_1(sK26,k1_zfmisc_1(sF388))
| ~ spl396_92
| ~ spl396_97
| ~ spl396_102 ),
inference(forward_subsumption_resolution,[],[f75922,f75816]) ).
fof(f75932,plain,
( ~ m1_subset_1(sK26,sF394)
| sF389 = k3_xboole_0(sK25,sK26)
| ~ spl396_92
| ~ spl396_97
| ~ spl396_102 ),
inference(forward_demodulation,[],[f75930,f75866]) ).
fof(f75934,plain,
( sF389 = k3_xboole_0(sK25,sK26)
| ~ spl396_92
| ~ spl396_93
| ~ spl396_97
| ~ spl396_102 ),
inference(forward_subsumption_resolution,[],[f75932,f75821]) ).
fof(f75937,definition,
( spl396_112
<=> sF389 = k3_xboole_0(sK25,sK26) ),
introduced(definition,[new_symbols(definition,[spl396_112])],[avatar_definition]) ).
fof(f75939,plain,
( sF389 = k3_xboole_0(sK25,sK26)
| ~ spl396_112 ),
inference(avatar_component_clause,[],[f75937]) ).
fof(f75940,plain,
( spl396_112
| ~ spl396_92
| ~ spl396_93
| ~ spl396_97
| ~ spl396_102 ),
inference(avatar_split_clause,[],[f75934,f75864,f75839,f75819,f75814,f75937]) ).
fof(f75941,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,[],[f73171,f73904]) ).
fof(f75948,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,[],[f75941]) ).
fof(f75949,plain,
( v1_relat_1(sK25)
| ~ spl396_92
| ~ spl396_96
| ~ spl396_102 ),
inference(resolution,[],[f75917,f75816]) ).
fof(f75950,plain,
( v1_relat_1(sK26)
| ~ spl396_93
| ~ spl396_96
| ~ spl396_102 ),
inference(resolution,[],[f75917,f75821]) ).
fof(f75952,definition,
( spl396_113
<=> v1_relat_1(sK26) ),
introduced(definition,[new_symbols(definition,[spl396_113])],[avatar_definition]) ).
fof(f75954,plain,
( v1_relat_1(sK26)
| ~ spl396_113 ),
inference(avatar_component_clause,[],[f75952]) ).
fof(f75955,plain,
( spl396_113
| ~ spl396_93
| ~ spl396_96
| ~ spl396_102 ),
inference(avatar_split_clause,[],[f75950,f75864,f75834,f75819,f75952]) ).
fof(f75957,definition,
( spl396_114
<=> v1_relat_1(sK25) ),
introduced(definition,[new_symbols(definition,[spl396_114])],[avatar_definition]) ).
fof(f75959,plain,
( v1_relat_1(sK25)
| ~ spl396_114 ),
inference(avatar_component_clause,[],[f75957]) ).
fof(f75960,plain,
( spl396_114
| ~ spl396_92
| ~ spl396_96
| ~ spl396_102 ),
inference(avatar_split_clause,[],[f75949,f75864,f75834,f75814,f75957]) ).
fof(f75961,plain,
( ~ m1_subset_1(sF389,k1_zfmisc_1(sF388))
| ~ spl396_96
| spl396_104 ),
inference(forward_demodulation,[],[f75877,f75836]) ).
fof(f75962,plain,
( ~ m1_subset_1(sF389,sF394)
| ~ spl396_96
| ~ spl396_102
| spl396_104 ),
inference(forward_demodulation,[],[f75961,f75866]) ).
fof(f75964,definition,
( spl396_115
<=> m1_subset_1(sF389,sF394) ),
introduced(definition,[new_symbols(definition,[spl396_115])],[avatar_definition]) ).
fof(f75965,plain,
( m1_subset_1(sF389,sF394)
| ~ spl396_115 ),
inference(avatar_component_clause,[],[f75964]) ).
fof(f75967,plain,
( ~ spl396_115
| ~ spl396_96
| ~ spl396_102
| spl396_104 ),
inference(avatar_split_clause,[],[f75962,f75875,f75864,f75834,f75964]) ).
fof(f75973,plain,
( m1_subset_1(sF393,k1_zfmisc_1(sK23))
| ~ m1_subset_1(sF391,k1_zfmisc_1(sK23))
| ~ m1_subset_1(sF392,k1_zfmisc_1(sK23))
| ~ spl396_101 ),
inference(superposition,[],[f73172,f75861]) ).
fof(f75974,plain,
( m1_subset_1(sF389,k1_zfmisc_1(sF388))
| ~ m1_subset_1(sK25,k1_zfmisc_1(sF388))
| ~ m1_subset_1(sK26,k1_zfmisc_1(sF388))
| ~ spl396_97 ),
inference(superposition,[],[f73172,f75841]) ).
fof(f75983,plain,
( m1_subset_1(sF389,sF394)
| ~ m1_subset_1(sK25,k1_zfmisc_1(sF388))
| ~ m1_subset_1(sK26,k1_zfmisc_1(sF388))
| ~ spl396_97
| ~ spl396_102 ),
inference(forward_demodulation,[],[f75974,f75866]) ).
fof(f75984,plain,
( m1_subset_1(sF393,k1_zfmisc_1(sK23))
| ~ m1_subset_1(sF392,k1_zfmisc_1(sK23))
| ~ spl396_101
| ~ spl396_110 ),
inference(forward_subsumption_resolution,[],[f75973,f75911]) ).
fof(f75985,plain,
( ~ m1_subset_1(sK25,sF394)
| m1_subset_1(sF389,sF394)
| ~ m1_subset_1(sK26,k1_zfmisc_1(sF388))
| ~ spl396_97
| ~ spl396_102 ),
inference(forward_demodulation,[],[f75983,f75866]) ).
fof(f75986,plain,
( m1_subset_1(sF393,k1_zfmisc_1(sK23))
| ~ spl396_101
| ~ spl396_108
| ~ spl396_110 ),
inference(forward_subsumption_resolution,[],[f75984,f75898]) ).
fof(f75987,plain,
( m1_subset_1(sF389,sF394)
| ~ m1_subset_1(sK26,k1_zfmisc_1(sF388))
| ~ spl396_92
| ~ spl396_97
| ~ spl396_102 ),
inference(forward_subsumption_resolution,[],[f75985,f75816]) ).
fof(f75989,definition,
( spl396_116
<=> m1_subset_1(sF393,k1_zfmisc_1(sK23)) ),
introduced(definition,[new_symbols(definition,[spl396_116])],[avatar_definition]) ).
fof(f75991,plain,
( m1_subset_1(sF393,k1_zfmisc_1(sK23))
| ~ spl396_116 ),
inference(avatar_component_clause,[],[f75989]) ).
fof(f75992,plain,
( spl396_116
| ~ spl396_101
| ~ spl396_108
| ~ spl396_110 ),
inference(avatar_split_clause,[],[f75986,f75909,f75896,f75859,f75989]) ).
fof(f75993,plain,
( ~ m1_subset_1(sK26,sF394)
| m1_subset_1(sF389,sF394)
| ~ spl396_92
| ~ spl396_97
| ~ spl396_102 ),
inference(forward_demodulation,[],[f75987,f75866]) ).
fof(f75994,plain,
( m1_subset_1(sF389,sF394)
| ~ spl396_92
| ~ spl396_93
| ~ spl396_97
| ~ spl396_102 ),
inference(forward_subsumption_resolution,[],[f75993,f75821]) ).
fof(f75995,plain,
( spl396_115
| ~ spl396_92
| ~ spl396_93
| ~ spl396_97
| ~ spl396_102 ),
inference(avatar_split_clause,[],[f75994,f75864,f75839,f75819,f75814,f75964]) ).
fof(f75996,plain,
( k1_zfmisc_1(sK22) != sF395
| m1_subset_1(sK24,k1_zfmisc_1(sK22))
| ~ m1_subset_1(sK24,sF395) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f76001,plain,
( v1_relat_1(sF389)
| ~ spl396_96
| ~ spl396_102
| ~ spl396_115 ),
inference(resolution,[],[f75965,f75917]) ).
fof(f76003,definition,
( spl396_117
<=> v1_relat_1(sF389) ),
introduced(definition,[new_symbols(definition,[spl396_117])],[avatar_definition]) ).
fof(f76005,plain,
( v1_relat_1(sF389)
| ~ spl396_117 ),
inference(avatar_component_clause,[],[f76003]) ).
fof(f76006,plain,
( spl396_117
| ~ spl396_96
| ~ spl396_102
| ~ spl396_115 ),
inference(avatar_split_clause,[],[f76001,f75964,f75864,f75834,f76003]) ).
fof(f76007,plain,
( ! [X0,X1] :
( ~ r2_hidden(X0,sF390)
| ~ r2_hidden(X1,sK24)
| r2_hidden(X0,k9_relat_1(sF389,k1_tarski(X1)))
| ~ m1_subset_1(sF389,k1_zfmisc_1(k2_zfmisc_1(sK22,sK23)))
| ~ m1_subset_1(sK24,k1_zfmisc_1(sK22)) )
| ~ spl396_98 ),
inference(superposition,[],[f73184,f75846]) ).
fof(f76008,plain,
( ! [X0,X1] :
( ~ r2_hidden(X0,sF392)
| ~ r2_hidden(X1,sK24)
| r2_hidden(X0,k9_relat_1(sK26,k1_tarski(X1)))
| ~ m1_subset_1(sK26,k1_zfmisc_1(k2_zfmisc_1(sK22,sK23)))
| ~ m1_subset_1(sK24,k1_zfmisc_1(sK22)) )
| ~ spl396_100 ),
inference(superposition,[],[f73184,f75856]) ).
fof(f76009,plain,
( ! [X0,X1] :
( ~ r2_hidden(X0,sF391)
| ~ r2_hidden(X1,sK24)
| r2_hidden(X0,k9_relat_1(sK25,k1_tarski(X1)))
| ~ m1_subset_1(sK25,k1_zfmisc_1(k2_zfmisc_1(sK22,sK23)))
| ~ m1_subset_1(sK24,k1_zfmisc_1(sK22)) )
| ~ spl396_99 ),
inference(superposition,[],[f73184,f75851]) ).
fof(f76010,plain,
( ! [X0,X1] :
( ~ m1_subset_1(sK25,k1_zfmisc_1(sF388))
| ~ r2_hidden(X0,sF391)
| ~ r2_hidden(X1,sK24)
| r2_hidden(X0,k9_relat_1(sK25,k1_tarski(X1)))
| ~ m1_subset_1(sK24,k1_zfmisc_1(sK22)) )
| ~ spl396_96
| ~ spl396_99 ),
inference(forward_demodulation,[],[f76009,f75836]) ).
fof(f76011,plain,
( ! [X0,X1] :
( ~ m1_subset_1(sK26,k1_zfmisc_1(sF388))
| ~ r2_hidden(X0,sF392)
| ~ r2_hidden(X1,sK24)
| r2_hidden(X0,k9_relat_1(sK26,k1_tarski(X1)))
| ~ m1_subset_1(sK24,k1_zfmisc_1(sK22)) )
| ~ spl396_96
| ~ spl396_100 ),
inference(forward_demodulation,[],[f76008,f75836]) ).
fof(f76012,plain,
( ! [X0,X1] :
( ~ m1_subset_1(sF389,k1_zfmisc_1(sF388))
| ~ r2_hidden(X0,sF390)
| ~ r2_hidden(X1,sK24)
| r2_hidden(X0,k9_relat_1(sF389,k1_tarski(X1)))
| ~ m1_subset_1(sK24,k1_zfmisc_1(sK22)) )
| ~ spl396_96
| ~ spl396_98 ),
inference(forward_demodulation,[],[f76007,f75836]) ).
fof(f76013,plain,
( ! [X0,X1] :
( ~ m1_subset_1(sK25,sF394)
| ~ r2_hidden(X0,sF391)
| ~ r2_hidden(X1,sK24)
| r2_hidden(X0,k9_relat_1(sK25,k1_tarski(X1)))
| ~ m1_subset_1(sK24,k1_zfmisc_1(sK22)) )
| ~ spl396_96
| ~ spl396_99
| ~ spl396_102 ),
inference(forward_demodulation,[],[f76010,f75866]) ).
fof(f76014,plain,
( ! [X0,X1] :
( ~ m1_subset_1(sK26,sF394)
| ~ r2_hidden(X0,sF392)
| ~ r2_hidden(X1,sK24)
| r2_hidden(X0,k9_relat_1(sK26,k1_tarski(X1)))
| ~ m1_subset_1(sK24,k1_zfmisc_1(sK22)) )
| ~ spl396_96
| ~ spl396_100
| ~ spl396_102 ),
inference(forward_demodulation,[],[f76011,f75866]) ).
fof(f76015,plain,
( ! [X0,X1] :
( ~ m1_subset_1(sF389,sF394)
| ~ r2_hidden(X0,sF390)
| ~ r2_hidden(X1,sK24)
| r2_hidden(X0,k9_relat_1(sF389,k1_tarski(X1)))
| ~ m1_subset_1(sK24,k1_zfmisc_1(sK22)) )
| ~ spl396_96
| ~ spl396_98
| ~ spl396_102 ),
inference(forward_demodulation,[],[f76012,f75866]) ).
fof(f76016,plain,
( ! [X0,X1] :
( ~ r2_hidden(X0,sF391)
| ~ r2_hidden(X1,sK24)
| r2_hidden(X0,k9_relat_1(sK25,k1_tarski(X1)))
| ~ m1_subset_1(sK24,k1_zfmisc_1(sK22)) )
| ~ spl396_92
| ~ spl396_96
| ~ spl396_99
| ~ spl396_102 ),
inference(forward_subsumption_resolution,[],[f76013,f75816]) ).
fof(f76017,plain,
( ! [X0,X1] :
( ~ r2_hidden(X0,sF392)
| ~ r2_hidden(X1,sK24)
| r2_hidden(X0,k9_relat_1(sK26,k1_tarski(X1)))
| ~ m1_subset_1(sK24,k1_zfmisc_1(sK22)) )
| ~ spl396_93
| ~ spl396_96
| ~ spl396_100
| ~ spl396_102 ),
inference(forward_subsumption_resolution,[],[f76014,f75821]) ).
fof(f76018,plain,
( ! [X0,X1] :
( ~ r2_hidden(X0,sF390)
| ~ r2_hidden(X1,sK24)
| r2_hidden(X0,k9_relat_1(sF389,k1_tarski(X1)))
| ~ m1_subset_1(sK24,k1_zfmisc_1(sK22)) )
| ~ spl396_96
| ~ spl396_98
| ~ spl396_102
| ~ spl396_115 ),
inference(forward_subsumption_resolution,[],[f76015,f75965]) ).
fof(f76019,plain,
( ! [X0,X1] :
( ~ m1_subset_1(sK24,sF395)
| ~ r2_hidden(X0,sF391)
| ~ r2_hidden(X1,sK24)
| r2_hidden(X0,k9_relat_1(sK25,k1_tarski(X1))) )
| ~ spl396_92
| ~ spl396_96
| ~ spl396_99
| ~ spl396_102
| ~ spl396_103 ),
inference(forward_demodulation,[],[f76016,f75871]) ).
fof(f76020,plain,
( ! [X0,X1] :
( ~ m1_subset_1(sK24,sF395)
| ~ r2_hidden(X0,sF392)
| ~ r2_hidden(X1,sK24)
| r2_hidden(X0,k9_relat_1(sK26,k1_tarski(X1))) )
| ~ spl396_93
| ~ spl396_96
| ~ spl396_100
| ~ spl396_102
| ~ spl396_103 ),
inference(forward_demodulation,[],[f76017,f75871]) ).
fof(f76021,plain,
( ! [X0,X1] :
( ~ m1_subset_1(sK24,sF395)
| ~ r2_hidden(X0,sF390)
| ~ r2_hidden(X1,sK24)
| r2_hidden(X0,k9_relat_1(sF389,k1_tarski(X1))) )
| ~ spl396_96
| ~ spl396_98
| ~ spl396_102
| ~ spl396_103
| ~ spl396_115 ),
inference(forward_demodulation,[],[f76018,f75871]) ).
fof(f76022,plain,
( ! [X0,X1] :
( r2_hidden(X0,k9_relat_1(sK25,k1_tarski(X1)))
| ~ r2_hidden(X1,sK24)
| ~ r2_hidden(X0,sF391) )
| ~ spl396_91
| ~ spl396_92
| ~ spl396_96
| ~ spl396_99
| ~ spl396_102
| ~ spl396_103 ),
inference(forward_subsumption_resolution,[],[f76019,f75811]) ).
fof(f76023,plain,
( ! [X0,X1] :
( r2_hidden(X0,k9_relat_1(sK26,k1_tarski(X1)))
| ~ r2_hidden(X1,sK24)
| ~ r2_hidden(X0,sF392) )
| ~ spl396_91
| ~ spl396_93
| ~ spl396_96
| ~ spl396_100
| ~ spl396_102
| ~ spl396_103 ),
inference(forward_subsumption_resolution,[],[f76020,f75811]) ).
fof(f76024,plain,
( ! [X0,X1] :
( r2_hidden(X0,k9_relat_1(sF389,k1_tarski(X1)))
| ~ r2_hidden(X1,sK24)
| ~ r2_hidden(X0,sF390) )
| ~ spl396_91
| ~ spl396_96
| ~ spl396_98
| ~ spl396_102
| ~ spl396_103
| ~ spl396_115 ),
inference(forward_subsumption_resolution,[],[f76021,f75811]) ).
fof(f76039,plain,
( sF393 = k3_xboole_0(sF392,sF391)
| ~ m1_subset_1(sF392,k1_zfmisc_1(sK23))
| ~ m1_subset_1(sF391,k1_zfmisc_1(sK23))
| ~ spl396_101 ),
inference(superposition,[],[f75861,f75948]) ).
fof(f76040,plain,
( sF389 = k3_xboole_0(sK26,sK25)
| ~ m1_subset_1(sK26,k1_zfmisc_1(sF388))
| ~ m1_subset_1(sK25,k1_zfmisc_1(sF388))
| ~ spl396_97 ),
inference(superposition,[],[f75841,f75948]) ).
fof(f76052,plain,
( ~ m1_subset_1(sK26,sF394)
| sF389 = k3_xboole_0(sK26,sK25)
| ~ m1_subset_1(sK25,k1_zfmisc_1(sF388))
| ~ spl396_97
| ~ spl396_102 ),
inference(forward_demodulation,[],[f76040,f75866]) ).
fof(f76053,plain,
( sF393 = k3_xboole_0(sF392,sF391)
| ~ m1_subset_1(sF391,k1_zfmisc_1(sK23))
| ~ spl396_101
| ~ spl396_108 ),
inference(forward_subsumption_resolution,[],[f76039,f75898]) ).
fof(f76056,plain,
( sF389 = k3_xboole_0(sK26,sK25)
| ~ m1_subset_1(sK25,k1_zfmisc_1(sF388))
| ~ spl396_93
| ~ spl396_97
| ~ spl396_102 ),
inference(forward_subsumption_resolution,[],[f76052,f75821]) ).
fof(f76057,plain,
( sF393 = k3_xboole_0(sF392,sF391)
| ~ spl396_101
| ~ spl396_108
| ~ spl396_110 ),
inference(forward_subsumption_resolution,[],[f76053,f75911]) ).
fof(f76060,plain,
( ~ m1_subset_1(sK25,sF394)
| sF389 = k3_xboole_0(sK26,sK25)
| ~ spl396_93
| ~ spl396_97
| ~ spl396_102 ),
inference(forward_demodulation,[],[f76056,f75866]) ).
fof(f76062,definition,
( spl396_118
<=> sF393 = k3_xboole_0(sF392,sF391) ),
introduced(definition,[new_symbols(definition,[spl396_118])],[avatar_definition]) ).
fof(f76064,plain,
( sF393 = k3_xboole_0(sF392,sF391)
| ~ spl396_118 ),
inference(avatar_component_clause,[],[f76062]) ).
fof(f76065,plain,
( spl396_118
| ~ spl396_101
| ~ spl396_108
| ~ spl396_110 ),
inference(avatar_split_clause,[],[f76057,f75909,f75896,f75859,f76062]) ).
fof(f76067,plain,
( sF389 = k3_xboole_0(sK26,sK25)
| ~ spl396_92
| ~ spl396_93
| ~ spl396_97
| ~ spl396_102 ),
inference(forward_subsumption_resolution,[],[f76060,f75816]) ).
fof(f76070,definition,
( spl396_119
<=> sF389 = k3_xboole_0(sK26,sK25) ),
introduced(definition,[new_symbols(definition,[spl396_119])],[avatar_definition]) ).
fof(f76072,plain,
( sF389 = k3_xboole_0(sK26,sK25)
| ~ spl396_119 ),
inference(avatar_component_clause,[],[f76070]) ).
fof(f76073,plain,
( spl396_119
| ~ spl396_92
| ~ spl396_93
| ~ spl396_97
| ~ spl396_102 ),
inference(avatar_split_clause,[],[f76067,f75864,f75839,f75819,f75814,f76070]) ).
fof(f76076,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF390)
| m1_subset_1(X0,sK23) )
| ~ spl396_106 ),
inference(resolution,[],[f73213,f75885]) ).
fof(f76078,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF392)
| m1_subset_1(X0,sK23) )
| ~ spl396_108 ),
inference(resolution,[],[f73213,f75898]) ).
fof(f76386,definition,
( spl396_138
<=> v1_xboole_0(sK23) ),
introduced(definition,[new_symbols(definition,[spl396_138])],[avatar_definition]) ).
fof(f76387,plain,
( ~ v1_xboole_0(sK23)
| spl396_138 ),
inference(avatar_component_clause,[],[f76386]) ).
fof(f76388,plain,
( v1_xboole_0(sK23)
| ~ spl396_138 ),
inference(avatar_component_clause,[],[f76386]) ).
fof(f76414,plain,
( ! [X0,X1] :
( r2_hidden(k4_tarski(X0,X1),sK25)
| ~ v1_relat_1(sK25)
| ~ r2_hidden(X0,sK24)
| ~ r2_hidden(X1,sF391) )
| ~ spl396_91
| ~ spl396_92
| ~ spl396_96
| ~ spl396_99
| ~ spl396_102
| ~ spl396_103 ),
inference(resolution,[],[f73396,f76022]) ).
fof(f76415,plain,
( ! [X0,X1] :
( r2_hidden(k4_tarski(X0,X1),sK26)
| ~ v1_relat_1(sK26)
| ~ r2_hidden(X0,sK24)
| ~ r2_hidden(X1,sF392) )
| ~ spl396_91
| ~ spl396_93
| ~ spl396_96
| ~ spl396_100
| ~ spl396_102
| ~ spl396_103 ),
inference(resolution,[],[f73396,f76023]) ).
fof(f76416,plain,
( ! [X0,X1] :
( r2_hidden(k4_tarski(X0,X1),sF389)
| ~ v1_relat_1(sF389)
| ~ r2_hidden(X0,sK24)
| ~ r2_hidden(X1,sF390) )
| ~ spl396_91
| ~ spl396_96
| ~ spl396_98
| ~ spl396_102
| ~ spl396_103
| ~ spl396_115 ),
inference(resolution,[],[f73396,f76024]) ).
fof(f76418,plain,
( ! [X0,X1] :
( r2_hidden(k4_tarski(X0,X1),sF389)
| ~ r2_hidden(X0,sK24)
| ~ r2_hidden(X1,sF390) )
| ~ spl396_91
| ~ spl396_96
| ~ spl396_98
| ~ spl396_102
| ~ spl396_103
| ~ spl396_115
| ~ spl396_117 ),
inference(forward_subsumption_resolution,[],[f76416,f76005]) ).
fof(f76419,plain,
( ! [X0,X1] :
( r2_hidden(k4_tarski(X0,X1),sK26)
| ~ r2_hidden(X0,sK24)
| ~ r2_hidden(X1,sF392) )
| ~ spl396_91
| ~ spl396_93
| ~ spl396_96
| ~ spl396_100
| ~ spl396_102
| ~ spl396_103
| ~ spl396_113 ),
inference(forward_subsumption_resolution,[],[f76415,f75954]) ).
fof(f76420,plain,
( ! [X0,X1] :
( r2_hidden(k4_tarski(X0,X1),sK25)
| ~ r2_hidden(X0,sK24)
| ~ r2_hidden(X1,sF391) )
| ~ spl396_91
| ~ spl396_92
| ~ spl396_96
| ~ spl396_99
| ~ spl396_102
| ~ spl396_103
| ~ spl396_114 ),
inference(forward_subsumption_resolution,[],[f76414,f75959]) ).
fof(f76692,plain,
( ! [X0] :
( r2_hidden(X0,sF390)
| r2_hidden(sK33(sK24,X0,sF389),sK24)
| ~ m1_subset_1(sF389,k1_zfmisc_1(k2_zfmisc_1(sK22,sK23)))
| ~ m1_subset_1(X0,sK23)
| ~ m1_subset_1(sK24,k1_zfmisc_1(sK22))
| v1_xboole_0(sK23) )
| ~ spl396_98 ),
inference(superposition,[],[f73182,f75846]) ).
fof(f76693,plain,
( ! [X0] :
( r2_hidden(X0,sF392)
| r2_hidden(sK33(sK24,X0,sK26),sK24)
| ~ m1_subset_1(sK26,k1_zfmisc_1(k2_zfmisc_1(sK22,sK23)))
| ~ m1_subset_1(X0,sK23)
| ~ m1_subset_1(sK24,k1_zfmisc_1(sK22))
| v1_xboole_0(sK23) )
| ~ spl396_100 ),
inference(superposition,[],[f73182,f75856]) ).
fof(f76694,plain,
( ! [X0] :
( r2_hidden(X0,sF391)
| r2_hidden(sK33(sK24,X0,sK25),sK24)
| ~ m1_subset_1(sK25,k1_zfmisc_1(k2_zfmisc_1(sK22,sK23)))
| ~ m1_subset_1(X0,sK23)
| ~ m1_subset_1(sK24,k1_zfmisc_1(sK22))
| v1_xboole_0(sK23) )
| ~ spl396_99 ),
inference(superposition,[],[f73182,f75851]) ).
fof(f76700,plain,
( ! [X0] :
( ~ m1_subset_1(sK25,k1_zfmisc_1(sF388))
| r2_hidden(X0,sF391)
| r2_hidden(sK33(sK24,X0,sK25),sK24)
| ~ m1_subset_1(X0,sK23)
| ~ m1_subset_1(sK24,k1_zfmisc_1(sK22))
| v1_xboole_0(sK23) )
| ~ spl396_96
| ~ spl396_99 ),
inference(forward_demodulation,[],[f76694,f75836]) ).
fof(f76701,plain,
( ! [X0] :
( ~ m1_subset_1(sK26,k1_zfmisc_1(sF388))
| r2_hidden(X0,sF392)
| r2_hidden(sK33(sK24,X0,sK26),sK24)
| ~ m1_subset_1(X0,sK23)
| ~ m1_subset_1(sK24,k1_zfmisc_1(sK22))
| v1_xboole_0(sK23) )
| ~ spl396_96
| ~ spl396_100 ),
inference(forward_demodulation,[],[f76693,f75836]) ).
fof(f76702,plain,
( ! [X0] :
( ~ m1_subset_1(sF389,k1_zfmisc_1(sF388))
| r2_hidden(X0,sF390)
| r2_hidden(sK33(sK24,X0,sF389),sK24)
| ~ m1_subset_1(X0,sK23)
| ~ m1_subset_1(sK24,k1_zfmisc_1(sK22))
| v1_xboole_0(sK23) )
| ~ spl396_96
| ~ spl396_98 ),
inference(forward_demodulation,[],[f76692,f75836]) ).
fof(f76705,plain,
( ! [X0] :
( ~ m1_subset_1(sK25,sF394)
| r2_hidden(X0,sF391)
| r2_hidden(sK33(sK24,X0,sK25),sK24)
| ~ m1_subset_1(X0,sK23)
| ~ m1_subset_1(sK24,k1_zfmisc_1(sK22))
| v1_xboole_0(sK23) )
| ~ spl396_96
| ~ spl396_99
| ~ spl396_102 ),
inference(forward_demodulation,[],[f76700,f75866]) ).
fof(f76706,plain,
( ! [X0] :
( ~ m1_subset_1(sK26,sF394)
| r2_hidden(X0,sF392)
| r2_hidden(sK33(sK24,X0,sK26),sK24)
| ~ m1_subset_1(X0,sK23)
| ~ m1_subset_1(sK24,k1_zfmisc_1(sK22))
| v1_xboole_0(sK23) )
| ~ spl396_96
| ~ spl396_100
| ~ spl396_102 ),
inference(forward_demodulation,[],[f76701,f75866]) ).
fof(f76707,plain,
( ! [X0] :
( ~ m1_subset_1(sF389,sF394)
| r2_hidden(X0,sF390)
| r2_hidden(sK33(sK24,X0,sF389),sK24)
| ~ m1_subset_1(X0,sK23)
| ~ m1_subset_1(sK24,k1_zfmisc_1(sK22))
| v1_xboole_0(sK23) )
| ~ spl396_96
| ~ spl396_98
| ~ spl396_102 ),
inference(forward_demodulation,[],[f76702,f75866]) ).
fof(f76710,plain,
( ! [X0] :
( r2_hidden(X0,sF391)
| r2_hidden(sK33(sK24,X0,sK25),sK24)
| ~ m1_subset_1(X0,sK23)
| ~ m1_subset_1(sK24,k1_zfmisc_1(sK22))
| v1_xboole_0(sK23) )
| ~ spl396_92
| ~ spl396_96
| ~ spl396_99
| ~ spl396_102 ),
inference(forward_subsumption_resolution,[],[f76705,f75816]) ).
fof(f76711,plain,
( ! [X0] :
( r2_hidden(X0,sF392)
| r2_hidden(sK33(sK24,X0,sK26),sK24)
| ~ m1_subset_1(X0,sK23)
| ~ m1_subset_1(sK24,k1_zfmisc_1(sK22))
| v1_xboole_0(sK23) )
| ~ spl396_93
| ~ spl396_96
| ~ spl396_100
| ~ spl396_102 ),
inference(forward_subsumption_resolution,[],[f76706,f75821]) ).
fof(f76712,plain,
( ! [X0] :
( r2_hidden(X0,sF390)
| r2_hidden(sK33(sK24,X0,sF389),sK24)
| ~ m1_subset_1(X0,sK23)
| ~ m1_subset_1(sK24,k1_zfmisc_1(sK22))
| v1_xboole_0(sK23) )
| ~ spl396_96
| ~ spl396_98
| ~ spl396_102
| ~ spl396_115 ),
inference(forward_subsumption_resolution,[],[f76707,f75965]) ).
fof(f76715,plain,
( ! [X0] :
( ~ m1_subset_1(sK24,sF395)
| r2_hidden(X0,sF391)
| r2_hidden(sK33(sK24,X0,sK25),sK24)
| ~ m1_subset_1(X0,sK23)
| v1_xboole_0(sK23) )
| ~ spl396_92
| ~ spl396_96
| ~ spl396_99
| ~ spl396_102
| ~ spl396_103 ),
inference(forward_demodulation,[],[f76710,f75871]) ).
fof(f76716,plain,
( ! [X0] :
( ~ m1_subset_1(sK24,sF395)
| r2_hidden(X0,sF392)
| r2_hidden(sK33(sK24,X0,sK26),sK24)
| ~ m1_subset_1(X0,sK23)
| v1_xboole_0(sK23) )
| ~ spl396_93
| ~ spl396_96
| ~ spl396_100
| ~ spl396_102
| ~ spl396_103 ),
inference(forward_demodulation,[],[f76711,f75871]) ).
fof(f76717,plain,
( ! [X0] :
( ~ m1_subset_1(sK24,sF395)
| r2_hidden(X0,sF390)
| r2_hidden(sK33(sK24,X0,sF389),sK24)
| ~ m1_subset_1(X0,sK23)
| v1_xboole_0(sK23) )
| ~ spl396_96
| ~ spl396_98
| ~ spl396_102
| ~ spl396_103
| ~ spl396_115 ),
inference(forward_demodulation,[],[f76712,f75871]) ).
fof(f76726,plain,
( ! [X0] :
( r2_hidden(X0,sF391)
| r2_hidden(sK33(sK24,X0,sK25),sK24)
| ~ m1_subset_1(X0,sK23)
| v1_xboole_0(sK23) )
| ~ spl396_91
| ~ spl396_92
| ~ spl396_96
| ~ spl396_99
| ~ spl396_102
| ~ spl396_103 ),
inference(forward_subsumption_resolution,[],[f76715,f75811]) ).
fof(f76727,plain,
( ! [X0] :
( r2_hidden(X0,sF392)
| r2_hidden(sK33(sK24,X0,sK26),sK24)
| ~ m1_subset_1(X0,sK23)
| v1_xboole_0(sK23) )
| ~ spl396_91
| ~ spl396_93
| ~ spl396_96
| ~ spl396_100
| ~ spl396_102
| ~ spl396_103 ),
inference(forward_subsumption_resolution,[],[f76716,f75811]) ).
fof(f76728,plain,
( ! [X0] :
( r2_hidden(X0,sF390)
| r2_hidden(sK33(sK24,X0,sF389),sK24)
| ~ m1_subset_1(X0,sK23)
| v1_xboole_0(sK23) )
| ~ spl396_91
| ~ spl396_96
| ~ spl396_98
| ~ spl396_102
| ~ spl396_103
| ~ spl396_115 ),
inference(forward_subsumption_resolution,[],[f76717,f75811]) ).
fof(f76730,definition,
( spl396_168
<=> ! [X0] :
( r2_hidden(X0,sF391)
| ~ m1_subset_1(X0,sK23)
| r2_hidden(sK33(sK24,X0,sK25),sK24) ) ),
introduced(definition,[new_symbols(definition,[spl396_168])],[avatar_definition]) ).
fof(f76731,plain,
( ! [X0] :
( r2_hidden(sK33(sK24,X0,sK25),sK24)
| ~ m1_subset_1(X0,sK23)
| r2_hidden(X0,sF391) )
| ~ spl396_168 ),
inference(avatar_component_clause,[],[f76730]) ).
fof(f76732,plain,
( spl396_138
| spl396_168
| ~ spl396_91
| ~ spl396_92
| ~ spl396_96
| ~ spl396_99
| ~ spl396_102
| ~ spl396_103 ),
inference(avatar_split_clause,[],[f76726,f75869,f75864,f75849,f75834,f75814,f75809,f76730,f76386]) ).
fof(f76734,definition,
( spl396_169
<=> ! [X0] :
( r2_hidden(X0,sF392)
| ~ m1_subset_1(X0,sK23)
| r2_hidden(sK33(sK24,X0,sK26),sK24) ) ),
introduced(definition,[new_symbols(definition,[spl396_169])],[avatar_definition]) ).
fof(f76735,plain,
( ! [X0] :
( r2_hidden(sK33(sK24,X0,sK26),sK24)
| ~ m1_subset_1(X0,sK23)
| r2_hidden(X0,sF392) )
| ~ spl396_169 ),
inference(avatar_component_clause,[],[f76734]) ).
fof(f76736,plain,
( spl396_138
| spl396_169
| ~ spl396_91
| ~ spl396_93
| ~ spl396_96
| ~ spl396_100
| ~ spl396_102
| ~ spl396_103 ),
inference(avatar_split_clause,[],[f76727,f75869,f75864,f75854,f75834,f75819,f75809,f76734,f76386]) ).
fof(f76738,definition,
( spl396_170
<=> ! [X0] :
( r2_hidden(X0,sF390)
| ~ m1_subset_1(X0,sK23)
| r2_hidden(sK33(sK24,X0,sF389),sK24) ) ),
introduced(definition,[new_symbols(definition,[spl396_170])],[avatar_definition]) ).
fof(f76739,plain,
( ! [X0] :
( r2_hidden(sK33(sK24,X0,sF389),sK24)
| ~ m1_subset_1(X0,sK23)
| r2_hidden(X0,sF390) )
| ~ spl396_170 ),
inference(avatar_component_clause,[],[f76738]) ).
fof(f76740,plain,
( spl396_138
| spl396_170
| ~ spl396_91
| ~ spl396_96
| ~ spl396_98
| ~ spl396_102
| ~ spl396_103
| ~ spl396_115 ),
inference(avatar_split_clause,[],[f76728,f75964,f75869,f75864,f75844,f75834,f75809,f76738,f76386]) ).
fof(f76765,plain,
( ! [X0] :
( ~ r2_hidden(X0,sK26)
| ~ r2_hidden(X0,sK25)
| r2_hidden(X0,sF389) )
| ~ spl396_112 ),
inference(superposition,[],[f75214,f75939]) ).
fof(f76767,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF392)
| ~ r2_hidden(X0,sF391)
| r2_hidden(X0,sF393) )
| ~ spl396_111 ),
inference(superposition,[],[f75214,f75926]) ).
fof(f76769,plain,
( ! [X0,X1] :
( ~ r2_hidden(k4_tarski(X0,X1),sK25)
| r2_hidden(k4_tarski(X0,X1),sF389)
| ~ r2_hidden(X0,sK24)
| ~ r2_hidden(X1,sF392) )
| ~ spl396_91
| ~ spl396_93
| ~ spl396_96
| ~ spl396_100
| ~ spl396_102
| ~ spl396_103
| ~ spl396_112
| ~ spl396_113 ),
inference(resolution,[],[f76765,f76419]) ).
fof(f76778,plain,
( ! [X0,X1] :
( r2_hidden(k4_tarski(X0,X1),sF389)
| ~ r2_hidden(X0,sK24)
| ~ r2_hidden(X1,sF392)
| ~ r2_hidden(X0,sK24)
| ~ r2_hidden(X1,sF391) )
| ~ spl396_91
| ~ spl396_92
| ~ spl396_93
| ~ spl396_96
| ~ spl396_99
| ~ spl396_100
| ~ spl396_102
| ~ spl396_103
| ~ spl396_112
| ~ spl396_113
| ~ spl396_114 ),
inference(resolution,[],[f76769,f76420]) ).
fof(f76779,plain,
( ! [X0,X1] :
( r2_hidden(k4_tarski(X0,X1),sF389)
| ~ r2_hidden(X0,sK24)
| ~ r2_hidden(X1,sF392)
| ~ r2_hidden(X1,sF391) )
| ~ spl396_91
| ~ spl396_92
| ~ spl396_93
| ~ spl396_96
| ~ spl396_99
| ~ spl396_100
| ~ spl396_102
| ~ spl396_103
| ~ spl396_112
| ~ spl396_113
| ~ spl396_114 ),
inference(duplicate_literal_removal,[],[f76778]) ).
fof(f77726,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF389)
| r2_hidden(X0,sK26) )
| ~ spl396_112 ),
inference(superposition,[],[f75216,f75939]) ).
fof(f77727,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF389)
| r2_hidden(X0,sK25) )
| ~ spl396_119 ),
inference(superposition,[],[f75216,f76072]) ).
fof(f77728,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF393)
| r2_hidden(X0,sF392) )
| ~ spl396_111 ),
inference(superposition,[],[f75216,f75926]) ).
fof(f77729,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF393)
| r2_hidden(X0,sF391) )
| ~ spl396_118 ),
inference(superposition,[],[f75216,f76064]) ).
fof(f77732,plain,
( ! [X0,X1] :
( r2_hidden(k4_tarski(X0,X1),sK26)
| ~ r2_hidden(X0,sK24)
| ~ r2_hidden(X1,sF390) )
| ~ spl396_91
| ~ spl396_96
| ~ spl396_98
| ~ spl396_102
| ~ spl396_103
| ~ spl396_112
| ~ spl396_115
| ~ spl396_117 ),
inference(resolution,[],[f77726,f76418]) ).
fof(f77742,plain,
( ! [X2,X0,X1] :
( ~ r2_hidden(X0,sK24)
| ~ r2_hidden(X1,sF390)
| r2_hidden(X1,k9_relat_1(sK26,X2))
| ~ r2_hidden(X0,X2)
| ~ v1_relat_1(sK26) )
| ~ spl396_91
| ~ spl396_96
| ~ spl396_98
| ~ spl396_102
| ~ spl396_103
| ~ spl396_112
| ~ spl396_115
| ~ spl396_117 ),
inference(resolution,[],[f77732,f75182]) ).
fof(f77746,plain,
( ! [X2,X0,X1] :
( r2_hidden(X1,k9_relat_1(sK26,X2))
| ~ r2_hidden(X1,sF390)
| ~ r2_hidden(X0,sK24)
| ~ r2_hidden(X0,X2) )
| ~ spl396_91
| ~ spl396_96
| ~ spl396_98
| ~ spl396_102
| ~ spl396_103
| ~ spl396_112
| ~ spl396_113
| ~ spl396_115
| ~ spl396_117 ),
inference(forward_subsumption_resolution,[],[f77742,f75954]) ).
fof(f77778,plain,
( ! [X0,X1] :
( r2_hidden(k4_tarski(X0,X1),sK25)
| ~ r2_hidden(X0,sK24)
| ~ r2_hidden(X1,sF390) )
| ~ spl396_91
| ~ spl396_96
| ~ spl396_98
| ~ spl396_102
| ~ spl396_103
| ~ spl396_115
| ~ spl396_117
| ~ spl396_119 ),
inference(resolution,[],[f77727,f76418]) ).
fof(f77825,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ r2_hidden(X1,k1_tarski(sK33(X2,X0,sK26)))
| ~ r2_hidden(X1,sK24)
| ~ r2_hidden(X0,sF390)
| r2_hidden(X0,k8_relset_2(X3,X4,X2,sK26))
| ~ m1_subset_1(sK26,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) )
| ~ spl396_91
| ~ spl396_96
| ~ spl396_98
| ~ spl396_102
| ~ spl396_103
| ~ spl396_112
| ~ spl396_113
| ~ spl396_115
| ~ spl396_117 ),
inference(resolution,[],[f77746,f73183]) ).
fof(f77834,plain,
( ! [X2,X0,X1] :
( ~ r2_hidden(X0,sK24)
| ~ r2_hidden(X1,sF390)
| r2_hidden(X1,k9_relat_1(sK25,X2))
| ~ r2_hidden(X0,X2)
| ~ v1_relat_1(sK25) )
| ~ spl396_91
| ~ spl396_96
| ~ spl396_98
| ~ spl396_102
| ~ spl396_103
| ~ spl396_115
| ~ spl396_117
| ~ spl396_119 ),
inference(resolution,[],[f77778,f75182]) ).
fof(f77838,plain,
( ! [X2,X0,X1] :
( r2_hidden(X1,k9_relat_1(sK25,X2))
| ~ r2_hidden(X1,sF390)
| ~ r2_hidden(X0,sK24)
| ~ r2_hidden(X0,X2) )
| ~ spl396_91
| ~ spl396_96
| ~ spl396_98
| ~ spl396_102
| ~ spl396_103
| ~ spl396_114
| ~ spl396_115
| ~ spl396_117
| ~ spl396_119 ),
inference(forward_subsumption_resolution,[],[f77834,f75959]) ).
fof(f77846,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ r2_hidden(X1,k1_tarski(sK33(X2,X0,sK25)))
| ~ r2_hidden(X1,sK24)
| ~ r2_hidden(X0,sF390)
| r2_hidden(X0,k8_relset_2(X3,X4,X2,sK25))
| ~ m1_subset_1(sK25,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) )
| ~ spl396_91
| ~ spl396_96
| ~ spl396_98
| ~ spl396_102
| ~ spl396_103
| ~ spl396_114
| ~ spl396_115
| ~ spl396_117
| ~ spl396_119 ),
inference(resolution,[],[f77838,f73183]) ).
fof(f78536,plain,
! [X2,X3,X0,X1,X4] :
( ~ r2_hidden(k4_tarski(sK33(X0,X1,X2),X1),X2)
| ~ v1_relat_1(X2)
| r2_hidden(X1,k8_relset_2(X3,X4,X0,X2))
| ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X3,X4)))
| ~ m1_subset_1(X1,X4)
| ~ m1_subset_1(X0,k1_zfmisc_1(X3))
| v1_xboole_0(X4) ),
inference(resolution,[],[f73397,f73183]) ).
fof(f78544,plain,
! [X2,X3,X0,X1,X4] :
( ~ r2_hidden(k4_tarski(sK33(X0,X1,X2),X1),X2)
| r2_hidden(X1,k8_relset_2(X3,X4,X0,X2))
| ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X3,X4)))
| ~ m1_subset_1(X1,X4)
| ~ m1_subset_1(X0,k1_zfmisc_1(X3))
| v1_xboole_0(X4) ),
inference(forward_subsumption_resolution,[],[f78536,f73155]) ).
fof(f78573,plain,
( ! [X2,X3,X0,X1] :
( r2_hidden(X0,k8_relset_2(X1,X2,X3,sF389))
| ~ m1_subset_1(sF389,k1_zfmisc_1(k2_zfmisc_1(X1,X2)))
| ~ m1_subset_1(X0,X2)
| ~ m1_subset_1(X3,k1_zfmisc_1(X1))
| v1_xboole_0(X2)
| ~ r2_hidden(sK33(X3,X0,sF389),sK24)
| ~ r2_hidden(X0,sF392)
| ~ r2_hidden(X0,sF391) )
| ~ spl396_91
| ~ spl396_92
| ~ spl396_93
| ~ spl396_96
| ~ spl396_99
| ~ spl396_100
| ~ spl396_102
| ~ spl396_103
| ~ spl396_112
| ~ spl396_113
| ~ spl396_114 ),
inference(resolution,[],[f78544,f76779]) ).
fof(f78874,definition,
( spl396_312
<=> ! [X0] :
( sF393 = X0
| r2_hidden(sK46(X0,sF393),X0) ) ),
introduced(definition,[new_symbols(definition,[spl396_312])],[avatar_definition]) ).
fof(f78875,plain,
( ! [X0] :
( r2_hidden(sK46(X0,sF393),X0)
| sF393 = X0 )
| ~ spl396_312 ),
inference(avatar_component_clause,[],[f78874]) ).
fof(f78892,definition,
( spl396_316
<=> ! [X1] : ~ r2_hidden(X1,sF390) ),
introduced(definition,[new_symbols(definition,[spl396_316])],[avatar_definition]) ).
fof(f78893,plain,
( ! [X1] : ~ r2_hidden(X1,sF390)
| ~ spl396_316 ),
inference(avatar_component_clause,[],[f78892]) ).
fof(f79262,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF390)
| ~ v1_xboole_0(sK23) )
| ~ spl396_106 ),
inference(resolution,[],[f73212,f75885]) ).
fof(f79265,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF393)
| ~ v1_xboole_0(sK23) )
| ~ spl396_116 ),
inference(resolution,[],[f73212,f75991]) ).
fof(f79276,plain,
( ! [X0] : ~ r2_hidden(X0,sF393)
| ~ spl396_116
| ~ spl396_138 ),
inference(forward_subsumption_resolution,[],[f79265,f76388]) ).
fof(f79285,plain,
( ! [X0] :
( sF393 = X0
| r2_hidden(sK46(X0,sF393),X0) )
| ~ spl396_116
| ~ spl396_138 ),
inference(resolution,[],[f79276,f73231]) ).
fof(f79295,plain,
( spl396_312
| ~ spl396_116
| ~ spl396_138 ),
inference(avatar_split_clause,[],[f79285,f76386,f75989,f78874]) ).
fof(f81476,plain,
( ~ spl396_138
| spl396_316
| ~ spl396_106 ),
inference(avatar_split_clause,[],[f79262,f75883,f78892,f76386]) ).
fof(f82168,plain,
( sF390 = sF393
| ~ spl396_312
| ~ spl396_316 ),
inference(resolution,[],[f78875,f78893]) ).
fof(f82189,plain,
( $false
| spl396_94
| ~ spl396_312
| ~ spl396_316 ),
inference(forward_subsumption_resolution,[],[f82168,f75826]) ).
fof(f82190,plain,
( spl396_94
| ~ spl396_312
| ~ spl396_316 ),
inference(avatar_contradiction_clause,[],[f82189]) ).
fof(f84115,definition,
( spl396_659
<=> r2_hidden(sK46(sF393,sF390),sF392) ),
introduced(definition,[new_symbols(definition,[spl396_659])],[avatar_definition]) ).
fof(f84117,plain,
( r2_hidden(sK46(sF393,sF390),sF392)
| ~ spl396_659 ),
inference(avatar_component_clause,[],[f84115]) ).
fof(f84120,definition,
( spl396_660
<=> r2_hidden(sK46(sF393,sF390),sF391) ),
introduced(definition,[new_symbols(definition,[spl396_660])],[avatar_definition]) ).
fof(f84121,plain,
( ~ r2_hidden(sK46(sF393,sF390),sF391)
| spl396_660 ),
inference(avatar_component_clause,[],[f84120]) ).
fof(f84252,definition,
( spl396_666
<=> r2_hidden(sK46(sF393,sF390),sF393) ),
introduced(definition,[new_symbols(definition,[spl396_666])],[avatar_definition]) ).
fof(f84253,plain,
( ~ r2_hidden(sK46(sF393,sF390),sF393)
| spl396_666 ),
inference(avatar_component_clause,[],[f84252]) ).
fof(f84254,plain,
( r2_hidden(sK46(sF393,sF390),sF393)
| ~ spl396_666 ),
inference(avatar_component_clause,[],[f84252]) ).
fof(f84263,plain,
( r2_hidden(sK46(sF393,sF390),sF391)
| ~ spl396_118
| ~ spl396_666 ),
inference(resolution,[],[f84254,f77729]) ).
fof(f84264,plain,
( r2_hidden(sK46(sF393,sF390),sF392)
| ~ spl396_111
| ~ spl396_666 ),
inference(resolution,[],[f84254,f77728]) ).
fof(f84277,plain,
( spl396_660
| ~ spl396_118
| ~ spl396_666 ),
inference(avatar_split_clause,[],[f84263,f84252,f76062,f84120]) ).
fof(f84299,definition,
( spl396_671
<=> r2_hidden(sK46(sF393,sF390),sF390) ),
introduced(definition,[new_symbols(definition,[spl396_671])],[avatar_definition]) ).
fof(f84300,plain,
( ~ r2_hidden(sK46(sF393,sF390),sF390)
| spl396_671 ),
inference(avatar_component_clause,[],[f84299]) ).
fof(f84301,plain,
( r2_hidden(sK46(sF393,sF390),sF390)
| ~ spl396_671 ),
inference(avatar_component_clause,[],[f84299]) ).
fof(f84303,plain,
( sF390 = sF393
| ~ r2_hidden(sK46(sF393,sF390),sF393)
| ~ spl396_671 ),
inference(resolution,[],[f84301,f73232]) ).
fof(f84317,plain,
( ~ r2_hidden(sK46(sF393,sF390),sF393)
| spl396_94
| ~ spl396_671 ),
inference(forward_subsumption_resolution,[],[f84303,f75826]) ).
fof(f84522,plain,
( sF390 = sF393
| r2_hidden(sK46(sF393,sF390),sF393)
| spl396_671 ),
inference(resolution,[],[f84300,f73231]) ).
fof(f84652,plain,
( r2_hidden(sK46(sF393,sF390),sF393)
| spl396_94
| spl396_671 ),
inference(forward_subsumption_resolution,[],[f84522,f75826]) ).
fof(f88467,plain,
( ! [X2,X3,X0,X1] :
( r2_hidden(X1,k8_relset_2(X2,X3,X0,sK26))
| ~ r2_hidden(X1,sF390)
| ~ r2_hidden(sK33(X0,X1,sK26),sK24)
| ~ m1_subset_1(sK26,k1_zfmisc_1(k2_zfmisc_1(X2,X3)))
| ~ m1_subset_1(X1,X3)
| ~ m1_subset_1(X0,k1_zfmisc_1(X2))
| v1_xboole_0(X3) )
| ~ spl396_91
| ~ spl396_96
| ~ spl396_98
| ~ spl396_102
| ~ spl396_103
| ~ spl396_112
| ~ spl396_113
| ~ spl396_115
| ~ spl396_117 ),
inference(resolution,[],[f75162,f77825]) ).
fof(f88469,plain,
( ! [X2,X3,X0,X1] :
( r2_hidden(X1,k8_relset_2(X2,X3,X0,sK25))
| ~ r2_hidden(X1,sF390)
| ~ r2_hidden(sK33(X0,X1,sK25),sK24)
| ~ m1_subset_1(sK25,k1_zfmisc_1(k2_zfmisc_1(X2,X3)))
| ~ m1_subset_1(X1,X3)
| ~ m1_subset_1(X0,k1_zfmisc_1(X2))
| v1_xboole_0(X3) )
| ~ spl396_91
| ~ spl396_96
| ~ spl396_98
| ~ spl396_102
| ~ spl396_103
| ~ spl396_114
| ~ spl396_115
| ~ spl396_117
| ~ spl396_119 ),
inference(resolution,[],[f75162,f77846]) ).
fof(f140727,plain,
( ! [X0] :
( r2_hidden(X0,sF390)
| ~ m1_subset_1(sF389,k1_zfmisc_1(k2_zfmisc_1(sK22,sK23)))
| ~ m1_subset_1(X0,sK23)
| ~ m1_subset_1(sK24,k1_zfmisc_1(sK22))
| v1_xboole_0(sK23)
| ~ r2_hidden(sK33(sK24,X0,sF389),sK24)
| ~ r2_hidden(X0,sF392)
| ~ r2_hidden(X0,sF391) )
| ~ spl396_91
| ~ spl396_92
| ~ spl396_93
| ~ spl396_96
| ~ spl396_98
| ~ spl396_99
| ~ spl396_100
| ~ spl396_102
| ~ spl396_103
| ~ spl396_112
| ~ spl396_113
| ~ spl396_114 ),
inference(superposition,[],[f78573,f75846]) ).
fof(f140743,plain,
( ! [X0] :
( r2_hidden(X0,sF390)
| ~ m1_subset_1(sF389,k1_zfmisc_1(k2_zfmisc_1(sK22,sK23)))
| ~ m1_subset_1(X0,sK23)
| ~ m1_subset_1(sK24,k1_zfmisc_1(sK22))
| v1_xboole_0(sK23)
| ~ r2_hidden(X0,sF392)
| ~ r2_hidden(X0,sF391) )
| ~ spl396_91
| ~ spl396_92
| ~ spl396_93
| ~ spl396_96
| ~ spl396_98
| ~ spl396_99
| ~ spl396_100
| ~ spl396_102
| ~ spl396_103
| ~ spl396_112
| ~ spl396_113
| ~ spl396_114
| ~ spl396_170 ),
inference(forward_subsumption_resolution,[],[f140727,f76739]) ).
fof(f140750,plain,
( ! [X0] :
( r2_hidden(X0,sF390)
| ~ m1_subset_1(sF389,k1_zfmisc_1(k2_zfmisc_1(sK22,sK23)))
| ~ m1_subset_1(sK24,k1_zfmisc_1(sK22))
| v1_xboole_0(sK23)
| ~ r2_hidden(X0,sF392)
| ~ r2_hidden(X0,sF391) )
| ~ spl396_91
| ~ spl396_92
| ~ spl396_93
| ~ spl396_96
| ~ spl396_98
| ~ spl396_99
| ~ spl396_100
| ~ spl396_102
| ~ spl396_103
| ~ spl396_108
| ~ spl396_112
| ~ spl396_113
| ~ spl396_114
| ~ spl396_170 ),
inference(forward_subsumption_resolution,[],[f140743,f76078]) ).
fof(f140756,plain,
( ! [X0] :
( r2_hidden(X0,sF390)
| ~ m1_subset_1(sF389,k1_zfmisc_1(k2_zfmisc_1(sK22,sK23)))
| ~ m1_subset_1(sK24,k1_zfmisc_1(sK22))
| ~ r2_hidden(X0,sF392)
| ~ r2_hidden(X0,sF391) )
| ~ spl396_91
| ~ spl396_92
| ~ spl396_93
| ~ spl396_96
| ~ spl396_98
| ~ spl396_99
| ~ spl396_100
| ~ spl396_102
| ~ spl396_103
| ~ spl396_108
| ~ spl396_112
| ~ spl396_113
| ~ spl396_114
| spl396_138
| ~ spl396_170 ),
inference(forward_subsumption_resolution,[],[f140750,f76387]) ).
fof(f152800,plain,
( ! [X0] :
( ~ m1_subset_1(sF389,k1_zfmisc_1(sF388))
| r2_hidden(X0,sF390)
| ~ m1_subset_1(sK24,k1_zfmisc_1(sK22))
| ~ r2_hidden(X0,sF392)
| ~ r2_hidden(X0,sF391) )
| ~ spl396_91
| ~ spl396_92
| ~ spl396_93
| ~ spl396_96
| ~ spl396_98
| ~ spl396_99
| ~ spl396_100
| ~ spl396_102
| ~ spl396_103
| ~ spl396_108
| ~ spl396_112
| ~ spl396_113
| ~ spl396_114
| spl396_138
| ~ spl396_170 ),
inference(forward_demodulation,[],[f140756,f75836]) ).
fof(f152850,plain,
( spl396_659
| ~ spl396_111
| ~ spl396_666 ),
inference(avatar_split_clause,[],[f84264,f84252,f75924,f84115]) ).
fof(f152851,plain,
( spl396_666
| spl396_94
| spl396_671 ),
inference(avatar_split_clause,[],[f84652,f84299,f75824,f84252]) ).
fof(f153146,plain,
( ! [X0] :
( ~ m1_subset_1(sF389,sF394)
| r2_hidden(X0,sF390)
| ~ m1_subset_1(sK24,k1_zfmisc_1(sK22))
| ~ r2_hidden(X0,sF392)
| ~ r2_hidden(X0,sF391) )
| ~ spl396_91
| ~ spl396_92
| ~ spl396_93
| ~ spl396_96
| ~ spl396_98
| ~ spl396_99
| ~ spl396_100
| ~ spl396_102
| ~ spl396_103
| ~ spl396_108
| ~ spl396_112
| ~ spl396_113
| ~ spl396_114
| spl396_138
| ~ spl396_170 ),
inference(forward_demodulation,[],[f152800,f75866]) ).
fof(f153357,plain,
( ! [X0] :
( r2_hidden(X0,sF390)
| ~ m1_subset_1(sK24,k1_zfmisc_1(sK22))
| ~ r2_hidden(X0,sF392)
| ~ r2_hidden(X0,sF391) )
| ~ spl396_91
| ~ spl396_92
| ~ spl396_93
| ~ spl396_96
| ~ spl396_98
| ~ spl396_99
| ~ spl396_100
| ~ spl396_102
| ~ spl396_103
| ~ spl396_108
| ~ spl396_112
| ~ spl396_113
| ~ spl396_114
| ~ spl396_115
| spl396_138
| ~ spl396_170 ),
inference(forward_subsumption_resolution,[],[f153146,f75965]) ).
fof(f153559,plain,
( ! [X0] :
( ~ m1_subset_1(sK24,sF395)
| r2_hidden(X0,sF390)
| ~ r2_hidden(X0,sF392)
| ~ r2_hidden(X0,sF391) )
| ~ spl396_91
| ~ spl396_92
| ~ spl396_93
| ~ spl396_96
| ~ spl396_98
| ~ spl396_99
| ~ spl396_100
| ~ spl396_102
| ~ spl396_103
| ~ spl396_108
| ~ spl396_112
| ~ spl396_113
| ~ spl396_114
| ~ spl396_115
| spl396_138
| ~ spl396_170 ),
inference(forward_demodulation,[],[f153357,f75871]) ).
fof(f153676,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF392)
| r2_hidden(X0,sF390)
| ~ r2_hidden(X0,sF391) )
| ~ spl396_91
| ~ spl396_92
| ~ spl396_93
| ~ spl396_96
| ~ spl396_98
| ~ spl396_99
| ~ spl396_100
| ~ spl396_102
| ~ spl396_103
| ~ spl396_108
| ~ spl396_112
| ~ spl396_113
| ~ spl396_114
| ~ spl396_115
| spl396_138
| ~ spl396_170 ),
inference(forward_subsumption_resolution,[],[f153559,f75811]) ).
fof(f153969,plain,
( r2_hidden(sK46(sF393,sF390),sF390)
| ~ r2_hidden(sK46(sF393,sF390),sF391)
| ~ spl396_91
| ~ spl396_92
| ~ spl396_93
| ~ spl396_96
| ~ spl396_98
| ~ spl396_99
| ~ spl396_100
| ~ spl396_102
| ~ spl396_103
| ~ spl396_108
| ~ spl396_112
| ~ spl396_113
| ~ spl396_114
| ~ spl396_115
| spl396_138
| ~ spl396_170
| ~ spl396_659 ),
inference(resolution,[],[f84117,f153676]) ).
fof(f153993,plain,
( ~ spl396_660
| spl396_671
| ~ spl396_91
| ~ spl396_92
| ~ spl396_93
| ~ spl396_96
| ~ spl396_98
| ~ spl396_99
| ~ spl396_100
| ~ spl396_102
| ~ spl396_103
| ~ spl396_108
| ~ spl396_112
| ~ spl396_113
| ~ spl396_114
| ~ spl396_115
| spl396_138
| ~ spl396_170
| ~ spl396_659 ),
inference(avatar_split_clause,[],[f153969,f84115,f76738,f76386,f75964,f75957,f75952,f75937,f75896,f75869,f75864,f75854,f75849,f75844,f75834,f75819,f75814,f75809,f84299,f84120]) ).
fof(f153995,plain,
( ~ spl396_666
| spl396_94
| ~ spl396_671 ),
inference(avatar_split_clause,[],[f84317,f84299,f75824,f84252]) ).
fof(f157650,plain,
( ! [X0] :
( r2_hidden(X0,sF392)
| ~ r2_hidden(X0,sF390)
| ~ r2_hidden(sK33(sK24,X0,sK26),sK24)
| ~ m1_subset_1(sK26,k1_zfmisc_1(k2_zfmisc_1(sK22,sK23)))
| ~ m1_subset_1(X0,sK23)
| ~ m1_subset_1(sK24,k1_zfmisc_1(sK22))
| v1_xboole_0(sK23) )
| ~ spl396_91
| ~ spl396_96
| ~ spl396_98
| ~ spl396_100
| ~ spl396_102
| ~ spl396_103
| ~ spl396_112
| ~ spl396_113
| ~ spl396_115
| ~ spl396_117 ),
inference(superposition,[],[f88467,f75856]) ).
fof(f157667,plain,
( ! [X0] :
( r2_hidden(X0,sF392)
| ~ r2_hidden(X0,sF390)
| ~ m1_subset_1(sK26,k1_zfmisc_1(k2_zfmisc_1(sK22,sK23)))
| ~ m1_subset_1(X0,sK23)
| ~ m1_subset_1(sK24,k1_zfmisc_1(sK22))
| v1_xboole_0(sK23) )
| ~ spl396_91
| ~ spl396_96
| ~ spl396_98
| ~ spl396_100
| ~ spl396_102
| ~ spl396_103
| ~ spl396_112
| ~ spl396_113
| ~ spl396_115
| ~ spl396_117
| ~ spl396_169 ),
inference(forward_subsumption_resolution,[],[f157650,f76735]) ).
fof(f157703,plain,
( ! [X0] :
( r2_hidden(X0,sF392)
| ~ r2_hidden(X0,sF390)
| ~ m1_subset_1(sK26,k1_zfmisc_1(k2_zfmisc_1(sK22,sK23)))
| ~ m1_subset_1(sK24,k1_zfmisc_1(sK22))
| v1_xboole_0(sK23) )
| ~ spl396_91
| ~ spl396_96
| ~ spl396_98
| ~ spl396_100
| ~ spl396_102
| ~ spl396_103
| ~ spl396_106
| ~ spl396_112
| ~ spl396_113
| ~ spl396_115
| ~ spl396_117
| ~ spl396_169 ),
inference(forward_subsumption_resolution,[],[f157667,f76076]) ).
fof(f157738,plain,
( ! [X0] :
( r2_hidden(X0,sF392)
| ~ r2_hidden(X0,sF390)
| ~ m1_subset_1(sK26,k1_zfmisc_1(k2_zfmisc_1(sK22,sK23)))
| ~ m1_subset_1(sK24,k1_zfmisc_1(sK22)) )
| ~ spl396_91
| ~ spl396_96
| ~ spl396_98
| ~ spl396_100
| ~ spl396_102
| ~ spl396_103
| ~ spl396_106
| ~ spl396_112
| ~ spl396_113
| ~ spl396_115
| ~ spl396_117
| spl396_138
| ~ spl396_169 ),
inference(forward_subsumption_resolution,[],[f157703,f76387]) ).
fof(f157773,plain,
( ! [X0] :
( ~ m1_subset_1(sK26,k1_zfmisc_1(sF388))
| r2_hidden(X0,sF392)
| ~ r2_hidden(X0,sF390)
| ~ m1_subset_1(sK24,k1_zfmisc_1(sK22)) )
| ~ spl396_91
| ~ spl396_96
| ~ spl396_98
| ~ spl396_100
| ~ spl396_102
| ~ spl396_103
| ~ spl396_106
| ~ spl396_112
| ~ spl396_113
| ~ spl396_115
| ~ spl396_117
| spl396_138
| ~ spl396_169 ),
inference(forward_demodulation,[],[f157738,f75836]) ).
fof(f157808,plain,
( ! [X0] :
( ~ m1_subset_1(sK26,sF394)
| r2_hidden(X0,sF392)
| ~ r2_hidden(X0,sF390)
| ~ m1_subset_1(sK24,k1_zfmisc_1(sK22)) )
| ~ spl396_91
| ~ spl396_96
| ~ spl396_98
| ~ spl396_100
| ~ spl396_102
| ~ spl396_103
| ~ spl396_106
| ~ spl396_112
| ~ spl396_113
| ~ spl396_115
| ~ spl396_117
| spl396_138
| ~ spl396_169 ),
inference(forward_demodulation,[],[f157773,f75866]) ).
fof(f157843,plain,
( ! [X0] :
( r2_hidden(X0,sF392)
| ~ r2_hidden(X0,sF390)
| ~ m1_subset_1(sK24,k1_zfmisc_1(sK22)) )
| ~ spl396_91
| ~ spl396_93
| ~ spl396_96
| ~ spl396_98
| ~ spl396_100
| ~ spl396_102
| ~ spl396_103
| ~ spl396_106
| ~ spl396_112
| ~ spl396_113
| ~ spl396_115
| ~ spl396_117
| spl396_138
| ~ spl396_169 ),
inference(forward_subsumption_resolution,[],[f157808,f75821]) ).
fof(f157888,plain,
( ! [X0] :
( ~ m1_subset_1(sK24,sF395)
| r2_hidden(X0,sF392)
| ~ r2_hidden(X0,sF390) )
| ~ spl396_91
| ~ spl396_93
| ~ spl396_96
| ~ spl396_98
| ~ spl396_100
| ~ spl396_102
| ~ spl396_103
| ~ spl396_106
| ~ spl396_112
| ~ spl396_113
| ~ spl396_115
| ~ spl396_117
| spl396_138
| ~ spl396_169 ),
inference(forward_demodulation,[],[f157843,f75871]) ).
fof(f157894,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF390)
| r2_hidden(X0,sF392) )
| ~ spl396_91
| ~ spl396_93
| ~ spl396_96
| ~ spl396_98
| ~ spl396_100
| ~ spl396_102
| ~ spl396_103
| ~ spl396_106
| ~ spl396_112
| ~ spl396_113
| ~ spl396_115
| ~ spl396_117
| spl396_138
| ~ spl396_169 ),
inference(forward_subsumption_resolution,[],[f157888,f75811]) ).
fof(f157906,plain,
( r2_hidden(sK46(sF393,sF390),sF392)
| ~ spl396_91
| ~ spl396_93
| ~ spl396_96
| ~ spl396_98
| ~ spl396_100
| ~ spl396_102
| ~ spl396_103
| ~ spl396_106
| ~ spl396_112
| ~ spl396_113
| ~ spl396_115
| ~ spl396_117
| spl396_138
| ~ spl396_169
| ~ spl396_671 ),
inference(resolution,[],[f157894,f84301]) ).
fof(f157981,plain,
( spl396_659
| ~ spl396_91
| ~ spl396_93
| ~ spl396_96
| ~ spl396_98
| ~ spl396_100
| ~ spl396_102
| ~ spl396_103
| ~ spl396_106
| ~ spl396_112
| ~ spl396_113
| ~ spl396_115
| ~ spl396_117
| spl396_138
| ~ spl396_169
| ~ spl396_671 ),
inference(avatar_split_clause,[],[f157906,f84299,f76734,f76386,f76003,f75964,f75952,f75937,f75883,f75869,f75864,f75854,f75844,f75834,f75819,f75809,f84115]) ).
fof(f158087,plain,
( ~ r2_hidden(sK46(sF393,sF390),sF391)
| r2_hidden(sK46(sF393,sF390),sF393)
| ~ spl396_111
| ~ spl396_659 ),
inference(resolution,[],[f84117,f76767]) ).
fof(f158092,plain,
( ~ r2_hidden(sK46(sF393,sF390),sF391)
| ~ spl396_111
| ~ spl396_659
| spl396_666 ),
inference(forward_subsumption_resolution,[],[f158087,f84253]) ).
fof(f158094,plain,
( ~ spl396_660
| ~ spl396_111
| ~ spl396_659
| spl396_666 ),
inference(avatar_split_clause,[],[f158092,f84252,f84115,f75924,f84120]) ).
fof(f163908,plain,
( ! [X0] :
( r2_hidden(X0,sF391)
| ~ r2_hidden(X0,sF390)
| ~ r2_hidden(sK33(sK24,X0,sK25),sK24)
| ~ m1_subset_1(sK25,k1_zfmisc_1(k2_zfmisc_1(sK22,sK23)))
| ~ m1_subset_1(X0,sK23)
| ~ m1_subset_1(sK24,k1_zfmisc_1(sK22))
| v1_xboole_0(sK23) )
| ~ spl396_91
| ~ spl396_96
| ~ spl396_98
| ~ spl396_99
| ~ spl396_102
| ~ spl396_103
| ~ spl396_114
| ~ spl396_115
| ~ spl396_117
| ~ spl396_119 ),
inference(superposition,[],[f88469,f75851]) ).
fof(f163925,plain,
( ! [X0] :
( r2_hidden(X0,sF391)
| ~ r2_hidden(X0,sF390)
| ~ m1_subset_1(sK25,k1_zfmisc_1(k2_zfmisc_1(sK22,sK23)))
| ~ m1_subset_1(X0,sK23)
| ~ m1_subset_1(sK24,k1_zfmisc_1(sK22))
| v1_xboole_0(sK23) )
| ~ spl396_91
| ~ spl396_96
| ~ spl396_98
| ~ spl396_99
| ~ spl396_102
| ~ spl396_103
| ~ spl396_114
| ~ spl396_115
| ~ spl396_117
| ~ spl396_119
| ~ spl396_168 ),
inference(forward_subsumption_resolution,[],[f163908,f76731]) ).
fof(f163960,plain,
( ! [X0] :
( r2_hidden(X0,sF391)
| ~ r2_hidden(X0,sF390)
| ~ m1_subset_1(sK25,k1_zfmisc_1(k2_zfmisc_1(sK22,sK23)))
| ~ m1_subset_1(sK24,k1_zfmisc_1(sK22))
| v1_xboole_0(sK23) )
| ~ spl396_91
| ~ spl396_96
| ~ spl396_98
| ~ spl396_99
| ~ spl396_102
| ~ spl396_103
| ~ spl396_106
| ~ spl396_114
| ~ spl396_115
| ~ spl396_117
| ~ spl396_119
| ~ spl396_168 ),
inference(forward_subsumption_resolution,[],[f163925,f76076]) ).
fof(f163994,plain,
( ! [X0] :
( r2_hidden(X0,sF391)
| ~ r2_hidden(X0,sF390)
| ~ m1_subset_1(sK25,k1_zfmisc_1(k2_zfmisc_1(sK22,sK23)))
| ~ m1_subset_1(sK24,k1_zfmisc_1(sK22)) )
| ~ spl396_91
| ~ spl396_96
| ~ spl396_98
| ~ spl396_99
| ~ spl396_102
| ~ spl396_103
| ~ spl396_106
| ~ spl396_114
| ~ spl396_115
| ~ spl396_117
| ~ spl396_119
| spl396_138
| ~ spl396_168 ),
inference(forward_subsumption_resolution,[],[f163960,f76387]) ).
fof(f164028,plain,
( ! [X0] :
( ~ m1_subset_1(sK25,k1_zfmisc_1(sF388))
| r2_hidden(X0,sF391)
| ~ r2_hidden(X0,sF390)
| ~ m1_subset_1(sK24,k1_zfmisc_1(sK22)) )
| ~ spl396_91
| ~ spl396_96
| ~ spl396_98
| ~ spl396_99
| ~ spl396_102
| ~ spl396_103
| ~ spl396_106
| ~ spl396_114
| ~ spl396_115
| ~ spl396_117
| ~ spl396_119
| spl396_138
| ~ spl396_168 ),
inference(forward_demodulation,[],[f163994,f75836]) ).
fof(f164062,plain,
( ! [X0] :
( ~ m1_subset_1(sK25,sF394)
| r2_hidden(X0,sF391)
| ~ r2_hidden(X0,sF390)
| ~ m1_subset_1(sK24,k1_zfmisc_1(sK22)) )
| ~ spl396_91
| ~ spl396_96
| ~ spl396_98
| ~ spl396_99
| ~ spl396_102
| ~ spl396_103
| ~ spl396_106
| ~ spl396_114
| ~ spl396_115
| ~ spl396_117
| ~ spl396_119
| spl396_138
| ~ spl396_168 ),
inference(forward_demodulation,[],[f164028,f75866]) ).
fof(f164096,plain,
( ! [X0] :
( r2_hidden(X0,sF391)
| ~ r2_hidden(X0,sF390)
| ~ m1_subset_1(sK24,k1_zfmisc_1(sK22)) )
| ~ spl396_91
| ~ spl396_92
| ~ spl396_96
| ~ spl396_98
| ~ spl396_99
| ~ spl396_102
| ~ spl396_103
| ~ spl396_106
| ~ spl396_114
| ~ spl396_115
| ~ spl396_117
| ~ spl396_119
| spl396_138
| ~ spl396_168 ),
inference(forward_subsumption_resolution,[],[f164062,f75816]) ).
fof(f164140,plain,
( ! [X0] :
( ~ m1_subset_1(sK24,sF395)
| r2_hidden(X0,sF391)
| ~ r2_hidden(X0,sF390) )
| ~ spl396_91
| ~ spl396_92
| ~ spl396_96
| ~ spl396_98
| ~ spl396_99
| ~ spl396_102
| ~ spl396_103
| ~ spl396_106
| ~ spl396_114
| ~ spl396_115
| ~ spl396_117
| ~ spl396_119
| spl396_138
| ~ spl396_168 ),
inference(forward_demodulation,[],[f164096,f75871]) ).
fof(f164145,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF390)
| r2_hidden(X0,sF391) )
| ~ spl396_91
| ~ spl396_92
| ~ spl396_96
| ~ spl396_98
| ~ spl396_99
| ~ spl396_102
| ~ spl396_103
| ~ spl396_106
| ~ spl396_114
| ~ spl396_115
| ~ spl396_117
| ~ spl396_119
| spl396_138
| ~ spl396_168 ),
inference(forward_subsumption_resolution,[],[f164140,f75811]) ).
fof(f164156,plain,
( r2_hidden(sK46(sF393,sF390),sF391)
| ~ spl396_91
| ~ spl396_92
| ~ spl396_96
| ~ spl396_98
| ~ spl396_99
| ~ spl396_102
| ~ spl396_103
| ~ spl396_106
| ~ spl396_114
| ~ spl396_115
| ~ spl396_117
| ~ spl396_119
| spl396_138
| ~ spl396_168
| ~ spl396_671 ),
inference(resolution,[],[f164145,f84301]) ).
fof(f164228,plain,
( $false
| ~ spl396_91
| ~ spl396_92
| ~ spl396_96
| ~ spl396_98
| ~ spl396_99
| ~ spl396_102
| ~ spl396_103
| ~ spl396_106
| ~ spl396_114
| ~ spl396_115
| ~ spl396_117
| ~ spl396_119
| spl396_138
| ~ spl396_168
| spl396_660
| ~ spl396_671 ),
inference(forward_subsumption_resolution,[],[f164156,f84121]) ).
fof(f164229,plain,
( ~ spl396_91
| ~ spl396_92
| ~ spl396_96
| ~ spl396_98
| ~ spl396_99
| ~ spl396_102
| ~ spl396_103
| ~ spl396_106
| ~ spl396_114
| ~ spl396_115
| ~ spl396_117
| ~ spl396_119
| spl396_138
| ~ spl396_168
| spl396_660
| ~ spl396_671 ),
inference(avatar_contradiction_clause,[],[f164228]) ).
cnf(s94,plain,
spl396_91,
inference(sat_conversion,[],[f75812]) ).
cnf(s95,plain,
spl396_92,
inference(sat_conversion,[],[f75817]) ).
cnf(s96,plain,
spl396_93,
inference(sat_conversion,[],[f75822]) ).
cnf(s97,plain,
~ spl396_94,
inference(sat_conversion,[],[f75827]) ).
cnf(s99,plain,
spl396_96,
inference(sat_conversion,[],[f75837]) ).
cnf(s100,plain,
spl396_97,
inference(sat_conversion,[],[f75842]) ).
cnf(s101,plain,
spl396_98,
inference(sat_conversion,[],[f75847]) ).
cnf(s102,plain,
spl396_99,
inference(sat_conversion,[],[f75852]) ).
cnf(s103,plain,
spl396_100,
inference(sat_conversion,[],[f75857]) ).
cnf(s104,plain,
spl396_101,
inference(sat_conversion,[],[f75862]) ).
cnf(s105,plain,
spl396_102,
inference(sat_conversion,[],[f75867]) ).
cnf(s106,plain,
spl396_103,
inference(sat_conversion,[],[f75872]) ).
cnf(s107,plain,
( ~ spl396_98
| ~ spl396_104
| ~ spl396_105
| spl396_106 ),
inference(sat_conversion,[],[f75886]) ).
cnf(s108,plain,
( ~ spl396_91
| ~ spl396_100
| ~ spl396_103
| ~ spl396_107
| spl396_108 ),
inference(sat_conversion,[],[f75899]) ).
cnf(s109,plain,
( ~ spl396_93
| ~ spl396_96
| ~ spl396_102
| spl396_107 ),
inference(sat_conversion,[],[f75900]) ).
cnf(s110,plain,
( ~ spl396_91
| ~ spl396_99
| ~ spl396_103
| ~ spl396_109
| spl396_110 ),
inference(sat_conversion,[],[f75912]) ).
cnf(s111,plain,
( ~ spl396_92
| ~ spl396_96
| ~ spl396_102
| spl396_109 ),
inference(sat_conversion,[],[f75913]) ).
cnf(s113,plain,
( ~ spl396_101
| ~ spl396_108
| ~ spl396_110
| spl396_111 ),
inference(sat_conversion,[],[f75929]) ).
cnf(s114,plain,
( ~ spl396_92
| ~ spl396_93
| ~ spl396_97
| ~ spl396_102
| spl396_112 ),
inference(sat_conversion,[],[f75940]) ).
cnf(s116,plain,
( ~ spl396_93
| ~ spl396_96
| ~ spl396_102
| spl396_113 ),
inference(sat_conversion,[],[f75955]) ).
cnf(s117,plain,
( ~ spl396_92
| ~ spl396_96
| ~ spl396_102
| spl396_114 ),
inference(sat_conversion,[],[f75960]) ).
cnf(s118,plain,
( ~ spl396_96
| ~ spl396_102
| spl396_104
| ~ spl396_115 ),
inference(sat_conversion,[],[f75967]) ).
cnf(s119,plain,
( ~ spl396_101
| ~ spl396_108
| ~ spl396_110
| spl396_116 ),
inference(sat_conversion,[],[f75992]) ).
cnf(s120,plain,
( ~ spl396_92
| ~ spl396_93
| ~ spl396_97
| ~ spl396_102
| spl396_115 ),
inference(sat_conversion,[],[f75995]) ).
cnf(s121,plain,
( ~ spl396_91
| ~ spl396_103
| spl396_105 ),
inference(sat_conversion,[],[f75996]) ).
cnf(s123,plain,
( ~ spl396_96
| ~ spl396_102
| ~ spl396_115
| spl396_117 ),
inference(sat_conversion,[],[f76006]) ).
cnf(s124,plain,
( ~ spl396_101
| ~ spl396_108
| ~ spl396_110
| spl396_118 ),
inference(sat_conversion,[],[f76065]) ).
cnf(s126,plain,
( ~ spl396_92
| ~ spl396_93
| ~ spl396_97
| ~ spl396_102
| spl396_119 ),
inference(sat_conversion,[],[f76073]) ).
cnf(s169,plain,
( ~ spl396_91
| ~ spl396_92
| ~ spl396_96
| ~ spl396_99
| ~ spl396_102
| ~ spl396_103
| spl396_138
| spl396_168 ),
inference(sat_conversion,[],[f76732]) ).
cnf(s170,plain,
( ~ spl396_91
| ~ spl396_93
| ~ spl396_96
| ~ spl396_100
| ~ spl396_102
| ~ spl396_103
| spl396_138
| spl396_169 ),
inference(sat_conversion,[],[f76736]) ).
cnf(s171,plain,
( ~ spl396_91
| ~ spl396_96
| ~ spl396_98
| ~ spl396_102
| ~ spl396_103
| ~ spl396_115
| spl396_138
| spl396_170 ),
inference(sat_conversion,[],[f76740]) ).
cnf(s348,plain,
( ~ spl396_116
| ~ spl396_138
| spl396_312 ),
inference(sat_conversion,[],[f79295]) ).
cnf(s490,plain,
( ~ spl396_106
| ~ spl396_138
| spl396_316 ),
inference(sat_conversion,[],[f81476]) ).
cnf(s579,plain,
( spl396_94
| ~ spl396_312
| ~ spl396_316 ),
inference(sat_conversion,[],[f82190]) ).
cnf(s732,plain,
( ~ spl396_118
| spl396_660
| ~ spl396_666 ),
inference(sat_conversion,[],[f84277]) ).
cnf(s3174,plain,
( ~ spl396_111
| spl396_659
| ~ spl396_666 ),
inference(sat_conversion,[],[f152850]) ).
cnf(s3176,plain,
( spl396_94
| spl396_666
| spl396_671 ),
inference(sat_conversion,[],[f152851]) ).
cnf(s3236,plain,
( ~ spl396_91
| ~ spl396_92
| ~ spl396_93
| ~ spl396_96
| ~ spl396_98
| ~ spl396_99
| ~ spl396_100
| ~ spl396_102
| ~ spl396_103
| ~ spl396_108
| ~ spl396_112
| ~ spl396_113
| ~ spl396_114
| ~ spl396_115
| spl396_138
| ~ spl396_170
| ~ spl396_659
| ~ spl396_660
| spl396_671 ),
inference(sat_conversion,[],[f153993]) ).
cnf(s3240,plain,
( spl396_94
| ~ spl396_666
| ~ spl396_671 ),
inference(sat_conversion,[],[f153995]) ).
cnf(s3540,plain,
( ~ spl396_91
| ~ spl396_93
| ~ spl396_96
| ~ spl396_98
| ~ spl396_100
| ~ spl396_102
| ~ spl396_103
| ~ spl396_106
| ~ spl396_112
| ~ spl396_113
| ~ spl396_115
| ~ spl396_117
| spl396_138
| ~ spl396_169
| spl396_659
| ~ spl396_671 ),
inference(sat_conversion,[],[f157981]) ).
cnf(s3556,plain,
( ~ spl396_111
| ~ spl396_659
| ~ spl396_660
| spl396_666 ),
inference(sat_conversion,[],[f158094]) ).
cnf(s4064,plain,
( ~ spl396_91
| ~ spl396_92
| ~ spl396_96
| ~ spl396_98
| ~ spl396_99
| ~ spl396_102
| ~ spl396_103
| ~ spl396_106
| ~ spl396_114
| ~ spl396_115
| ~ spl396_117
| ~ spl396_119
| spl396_138
| ~ spl396_168
| spl396_660
| ~ spl396_671 ),
inference(sat_conversion,[],[f164229]) ).
cnf(s4132,plain,
spl396_113,
inference(rat,[],[s116,s99,s105,s96]) ).
cnf(s4133,plain,
spl396_107,
inference(rat,[],[s109,s99,s105,s96]) ).
cnf(s4138,plain,
spl396_119,
inference(rat,[],[s126,s96,s105,s100,s95]) ).
cnf(s4139,plain,
spl396_115,
inference(rat,[],[s120,s96,s105,s100,s95]) ).
cnf(s4140,plain,
spl396_114,
inference(rat,[],[s117,s99,s105,s95]) ).
cnf(s4141,plain,
spl396_112,
inference(rat,[],[s114,s96,s105,s100,s95]) ).
cnf(s4142,plain,
spl396_109,
inference(rat,[],[s111,s99,s105,s95]) ).
cnf(s4148,plain,
spl396_117,
inference(rat,[],[s123,s99,s105,s4139]) ).
cnf(s4149,plain,
spl396_104,
inference(rat,[],[s118,s99,s105,s4139]) ).
cnf(s4206,plain,
spl396_105,
inference(rat,[],[s121,s106,s94]) ).
cnf(s4207,plain,
spl396_110,
inference(rat,[],[s110,s4142,s102,s106,s94]) ).
cnf(s4208,plain,
spl396_108,
inference(rat,[],[s108,s4133,s103,s106,s94]) ).
cnf(s4241,plain,
spl396_106,
inference(rat,[],[s107,s4149,s101,s4206]) ).
cnf(s4247,plain,
spl396_118,
inference(rat,[],[s124,s4207,s104,s4208]) ).
cnf(s4248,plain,
spl396_116,
inference(rat,[],[s119,s4207,s104,s4208]) ).
cnf(s4249,plain,
spl396_111,
inference(rat,[],[s113,s4207,s104,s4208]) ).
cnf(s4471,plain,
( spl396_659
| spl396_138 ),
inference(rat,[],[s3176,s3540,s3174,s170,s97,s99,s101,s103,s105,s106,s96,s4141,s4132,s4139,s4148,s94,s4241,s4249]) ).
cnf(s4472,plain,
( spl396_666
| spl396_138 ),
inference(rat,[],[s4064,s3556,s3176,s169,s4471,s99,s101,s102,s105,s106,s95,s4140,s4139,s4148,s4138,s94,s4241,s4249,s97]) ).
cnf(s4473,plain,
spl396_138,
inference(rat,[],[s3236,s732,s3240,s4472,s4471,s171,s96,s99,s101,s102,s103,s105,s106,s95,s4141,s4132,s4140,s4139,s94,s4208,s4247,s97]) ).
cnf(s4474,plain,
spl396_316,
inference(rat,[],[s490,s4241,s4473]) ).
cnf(s4479,plain,
spl396_312,
inference(rat,[],[s348,s4248,s4473]) ).
cnf(s4486,plain,
$false,
inference(rat,[],[s579,s97,s4474,s4479]) ).
fof(f164232,plain,
$false,
inference(avatar_sat_refutation,[],[s4486]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU433+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.36 % Computer : n020.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 28 05:27:50 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.40 Running first-order theorem proving
% 0.09/0.40 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 22.41/8.82 % (4063821)Detected formulas, will run a generic FOF schedule.
% 22.41/8.82 % (4063828)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=2312710363:i=141695:sd=1:nm=32:gsp=on:ss=included_2944 on theBenchmark for (2944ds/141695Mi)
% 22.41/8.82 % (4063826)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=826872478:i=141193_2944 on theBenchmark for (2944ds/141193Mi)
% 22.41/8.82 % (4063829)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1577805389:i=109:sd=1:ins=1:gsp=on:ss=axioms_2944 on theBenchmark for (2944ds/109Mi)
% 22.41/8.82 % (4063827)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=3526130878:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2944 on theBenchmark for (2944ds/134677Mi)
% 22.41/8.82 % (4063830)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2143981265:i=119:av=off:ss=axioms_2944 on theBenchmark for (2944ds/119Mi)
% 22.41/8.82 % (4063831)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=493021255:s2a=on:i=139:gtg=position_2944 on theBenchmark for (2944ds/139Mi)
% 22.41/8.82 % (4063832)dis-21_1_sil=8000:lcm=predicate:random_seed=1572045631:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2944 on theBenchmark for (2944ds/129Mi)
% 22.41/8.82 % (4063829)Instruction limit reached!
% 22.41/8.82 % (4063829)------------------------------
% 22.41/8.82 % (4063829)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.41/8.82 % (4063829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.41/8.82 % (4063829)CaDiCaL version: 2.1.3
% 22.41/8.82 % (4063829)Termination reason: Instruction limit
% 22.41/8.82 % (4063829)Termination phase: SInE selection
% 22.41/8.82 % (4063829)Time elapsed: 0.083 s
% 22.41/8.82 % (4063829)Peak memory usage: 200 MB
% 22.41/8.82 % (4063829)Instructions burned: 109 (million)
% 22.41/8.82 % (4063831)Instruction limit reached!
% 22.41/8.82 % (4063831)------------------------------
% 22.41/8.82 % (4063831)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.41/8.82 % (4063831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.41/8.82 % (4063831)CaDiCaL version: 2.1.3
% 22.41/8.82 % (4063831)Termination reason: Instruction limit
% 22.41/8.82 % (4063831)Termination phase: Property scanning
% 22.41/8.82 % (4063831)Time elapsed: 0.069 s
% 22.41/8.82 % (4063831)Peak memory usage: 201 MB
% 22.41/8.82 % (4063831)Instructions burned: 140 (million)
% 22.41/8.82 % (4063830)Instruction limit reached!
% 22.41/8.82 % (4063830)------------------------------
% 22.41/8.82 % (4063830)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.41/8.82 % (4063830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.41/8.82 % (4063830)CaDiCaL version: 2.1.3
% 22.41/8.82 % (4063830)Termination reason: Instruction limit
% 22.41/8.82 % (4063830)Termination phase: SInE selection
% 22.41/8.82 % (4063830)Time elapsed: 0.096 s
% 22.41/8.82 % (4063830)Peak memory usage: 201 MB
% 22.41/8.82 % (4063830)Instructions burned: 120 (million)
% 22.41/8.82 % (4063832)Instruction limit reached!
% 22.41/8.82 % (4063832)------------------------------
% 22.41/8.82 % (4063832)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.41/8.82 % (4063832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.41/8.82 % (4063832)CaDiCaL version: 2.1.3
% 22.41/8.82 % (4063832)Termination reason: Instruction limit
% 22.41/8.82 % (4063832)Termination phase: SInE selection
% 22.41/8.82 % (4063832)Time elapsed: 0.100 s
% 22.41/8.82 % (4063832)Peak memory usage: 201 MB
% 22.41/8.82 % (4063832)Instructions burned: 130 (million)
% 22.41/8.82 % (4063840)lrs+10_1_sil=8000:sp=occurrence:random_seed=3752955548:i=285:sd=3:ss=axioms:sgt=8_2942 on theBenchmark for (2942ds/285Mi)
% 22.41/8.82 % (4063841)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2056642367:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2942 on theBenchmark for (2942ds/157Mi)
% 22.41/8.82 % (4063842)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2924861029:i=325:sd=1:ss=axioms:sgt=32_2941 on theBenchmark for (2941ds/325Mi)
% 22.41/8.82 % (4063843)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=3909814641:s2a=on:i=248:s2at=1.23:gtg=position_2941 on theBenchmark for (2941ds/248Mi)
% 22.41/8.82 % (4063841)Instruction limit reached!
% 30.17/9.95 % (4063841)------------------------------
% 30.17/9.95 % (4063841)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.17/9.95 % (4063841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.17/9.95 % (4063841)CaDiCaL version: 2.1.3
% 30.17/9.95 % (4063841)Termination reason: Instruction limit
% 30.17/9.95 % (4063841)Termination phase: Property scanning
% 30.17/9.95 % (4063841)Time elapsed: 0.077 s
% 30.17/9.95 % (4063841)Peak memory usage: 201 MB
% 30.17/9.95 % (4063841)Instructions burned: 159 (million)
% 30.17/9.95 % (4063843)Instruction limit reached!
% 30.17/9.95 % (4063843)------------------------------
% 30.17/9.95 % (4063843)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.17/9.95 % (4063843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.17/9.95 % (4063843)CaDiCaL version: 2.1.3
% 30.17/9.95 % (4063843)Termination reason: Instruction limit
% 30.17/9.95 % (4063843)Termination phase: Property scanning
% 30.17/9.95 % (4063843)Time elapsed: 0.114 s
% 30.17/9.95 % (4063843)Peak memory usage: 201 MB
% 30.17/9.95 % (4063843)Instructions burned: 249 (million)
% 30.17/9.95 % (4063840)Instruction limit reached!
% 30.17/9.95 % (4063840)------------------------------
% 30.17/9.95 % (4063840)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.17/9.95 % (4063840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.17/9.95 % (4063840)CaDiCaL version: 2.1.3
% 30.17/9.95 % (4063840)Termination reason: Instruction limit
% 30.17/9.95 % (4063840)Termination phase: SInE selection
% 30.17/9.95 % (4063840)Time elapsed: 0.223 s
% 30.17/9.95 % (4063840)Peak memory usage: 201 MB
% 30.17/9.95 % (4063840)Instructions burned: 285 (million)
% 30.17/9.95 % (4063842)Instruction limit reached!
% 30.17/9.95 % (4063842)------------------------------
% 30.17/9.95 % (4063842)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.17/9.95 % (4063842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.17/9.95 % (4063842)CaDiCaL version: 2.1.3
% 30.17/9.95 % (4063842)Termination reason: Instruction limit
% 30.17/9.95 % (4063842)Termination phase: SInE selection
% 30.17/9.95 % (4063842)Time elapsed: 0.242 s
% 30.17/9.95 % (4063842)Peak memory usage: 201 MB
% 30.17/9.95 % (4063842)Instructions burned: 326 (million)
% 30.17/9.95 % (4063848)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1164972965:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2939 on theBenchmark for (2939ds/294Mi)
% 30.17/9.95 % (4063849)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3085180243:i=2350_2938 on theBenchmark for (2938ds/2350Mi)
% 30.17/9.95 % (4063850)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3040228621:cts=off:i=113:fsr=off:ss=included:sgt=4_2938 on theBenchmark for (2938ds/113Mi)
% 30.17/9.95 % (4063852)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2868811409:i=127:av=off:fsr=off:sup=off_2937 on theBenchmark for (2937ds/127Mi)
% 30.17/9.95 % (4063850)Instruction limit reached!
% 30.17/9.95 % (4063850)------------------------------
% 30.17/9.95 % (4063850)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.17/9.95 % (4063850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.17/9.95 % (4063850)CaDiCaL version: 2.1.3
% 30.17/9.95 % (4063850)Termination reason: Instruction limit
% 30.17/9.95 % (4063850)Termination phase: SInE selection
% 30.17/9.95 % (4063850)Time elapsed: 0.091 s
% 30.17/9.95 % (4063850)Peak memory usage: 201 MB
% 30.17/9.95 % (4063850)Instructions burned: 113 (million)
% 30.17/9.95 % (4063848)Instruction limit reached!
% 30.17/9.95 % (4063848)------------------------------
% 30.17/9.95 % (4063848)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.17/9.95 % (4063848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.17/9.95 % (4063848)CaDiCaL version: 2.1.3
% 30.17/9.95 % (4063848)Termination reason: Instruction limit
% 30.17/9.95 % (4063848)Termination phase: SInE selection
% 30.17/9.95 % (4063848)Time elapsed: 0.222 s
% 30.17/9.95 % (4063848)Peak memory usage: 201 MB
% 30.17/9.95 % (4063848)Instructions burned: 295 (million)
% 30.17/9.95 % (4063852)Instruction limit reached!
% 30.17/9.95 % (4063852)------------------------------
% 30.17/9.95 % (4063852)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.17/9.95 % (4063852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.17/9.95 % (4063852)CaDiCaL version: 2.1.3
% 74.51/16.11 % (4063852)Termination reason: Instruction limit
% 74.51/16.11 % (4063852)Termination phase: Preprocessing 1
% 74.51/16.11 % (4063852)Time elapsed: 0.100 s
% 74.51/16.11 % (4063852)Peak memory usage: 202 MB
% 74.51/16.11 % (4063852)Instructions burned: 127 (million)
% 74.51/16.11 % (4063856)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2919514089:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2935 on theBenchmark for (2935ds/114Mi)
% 74.51/16.11 % (4063857)lrs+10_1_sil=8000:sp=occurrence:random_seed=3895922181:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2935 on theBenchmark for (2935ds/907Mi)
% 74.51/16.11 % (4063858)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=171684483:i=437:sd=1:aac=none:ss=included_2935 on theBenchmark for (2935ds/437Mi)
% 74.51/16.11 % (4063856)Instruction limit reached!
% 74.51/16.11 % (4063856)------------------------------
% 74.51/16.11 % (4063856)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.51/16.11 % (4063856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.51/16.11 % (4063856)CaDiCaL version: 2.1.3
% 74.51/16.11 % (4063856)Termination reason: Instruction limit
% 74.51/16.11 % (4063856)Termination phase: Property scanning
% 74.51/16.11 % (4063856)Time elapsed: 0.057 s
% 74.51/16.11 % (4063856)Peak memory usage: 201 MB
% 74.51/16.11 % (4063856)Instructions burned: 115 (million)
% 74.51/16.11 % (4063862)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=578091521:i=5202:ss=axioms:sgt=16_2933 on theBenchmark for (2933ds/5202Mi)
% 74.51/16.11 % (4063858)Instruction limit reached!
% 74.51/16.11 % (4063858)------------------------------
% 74.51/16.11 % (4063858)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.51/16.11 % (4063858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.51/16.11 % (4063858)CaDiCaL version: 2.1.3
% 74.51/16.11 % (4063858)Termination reason: Instruction limit
% 74.51/16.11 % (4063858)Termination phase: SInE selection
% 74.51/16.11 % (4063858)Time elapsed: 0.314 s
% 74.51/16.11 % (4063858)Peak memory usage: 202 MB
% 74.51/16.11 % (4063858)Instructions burned: 437 (million)
% 74.51/16.11 % (4063864)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2665593964:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2930 on theBenchmark for (2930ds/134Mi)
% 74.51/16.11 % (4063864)Instruction limit reached!
% 74.51/16.11 % (4063864)------------------------------
% 74.51/16.11 % (4063864)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.51/16.11 % (4063864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.51/16.11 % (4063864)CaDiCaL version: 2.1.3
% 74.51/16.11 % (4063864)Termination reason: Instruction limit
% 74.51/16.11 % (4063864)Termination phase: SInE selection
% 74.51/16.11 % (4063864)Time elapsed: 0.103 s
% 74.51/16.11 % (4063864)Peak memory usage: 201 MB
% 74.51/16.11 % (4063864)Instructions burned: 135 (million)
% 74.51/16.11 % (4063857)Instruction limit reached!
% 74.51/16.11 % (4063857)------------------------------
% 74.51/16.11 % (4063857)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.51/16.11 % (4063857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.51/16.11 % (4063857)CaDiCaL version: 2.1.3
% 74.51/16.11 % (4063857)Termination reason: Instruction limit
% 74.51/16.11 % (4063857)Termination phase: Preprocessing 1
% 74.51/16.11 % (4063857)Time elapsed: 0.662 s
% 74.51/16.11 % (4063857)Peak memory usage: 204 MB
% 74.51/16.11 % (4063857)Instructions burned: 907 (million)
% 74.51/16.11 % (4063866)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2662270216:st=8:i=592:sd=3:ep=RST:ss=axioms_2927 on theBenchmark for (2927ds/592Mi)
% 74.51/16.11 % (4063867)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2707869590:st=3:i=13193:sd=3:ss=axioms_2927 on theBenchmark for (2927ds/13193Mi)
% 74.51/16.11 % (4063866)Instruction limit reached!
% 74.51/16.11 % (4063866)------------------------------
% 74.51/16.11 % (4063866)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.51/16.11 % (4063866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.51/16.11 % (4063866)CaDiCaL version: 2.1.3
% 74.51/16.11 % (4063866)Termination reason: Instruction limit
% 74.51/16.11 % (4063866)Termination phase: SInE selection
% 74.51/16.11 % (4063866)Time elapsed: 0.377 s
% 74.51/16.11 % (4063866)Peak memory usage: 203 MB
% 74.51/16.11 % (4063866)Instructions burned: 592 (million)
% 74.51/16.11 % (4063870)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=3498117737:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2921 on theBenchmark for (2921ds/125Mi)
% 97.69/19.31 % (4063870)Instruction limit reached!
% 97.69/19.31 % (4063870)------------------------------
% 97.69/19.31 % (4063870)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 97.69/19.31 % (4063870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.69/19.31 % (4063870)CaDiCaL version: 2.1.3
% 97.69/19.31 % (4063870)Termination reason: Instruction limit
% 97.69/19.31 % (4063870)Termination phase: Property scanning
% 97.69/19.31 % (4063870)Time elapsed: 0.063 s
% 97.69/19.31 % (4063870)Peak memory usage: 201 MB
% 97.69/19.31 % (4063870)Instructions burned: 125 (million)
% 97.69/19.31 % (4063849)Instruction limit reached!
% 97.69/19.31 % (4063849)------------------------------
% 97.69/19.31 % (4063849)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 97.69/19.31 % (4063849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.69/19.31 % (4063849)CaDiCaL version: 2.1.3
% 97.69/19.31 % (4063849)Termination reason: Instruction limit
% 97.69/19.31 % (4063849)Termination phase: Preprocessing 3
% 97.69/19.31 % (4063849)Time elapsed: 1.860 s
% 97.69/19.31 % (4063849)Peak memory usage: 305 MB
% 97.69/19.31 % (4063849)Instructions burned: 2350 (million)
% 97.69/19.31 % (4063872)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1850339816:i=134:gtgl=5:slsql=off:gtg=exists_sym_2919 on theBenchmark for (2919ds/134Mi)
% 97.69/19.31 % (4063872)Instruction limit reached!
% 97.69/19.31 % (4063872)------------------------------
% 97.69/19.31 % (4063872)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 97.69/19.31 % (4063872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.69/19.31 % (4063872)CaDiCaL version: 2.1.3
% 97.69/19.31 % (4063872)Termination reason: Instruction limit
% 97.69/19.31 % (4063872)Termination phase: Property scanning
% 97.69/19.31 % (4063872)Time elapsed: 0.067 s
% 97.69/19.31 % (4063872)Peak memory usage: 201 MB
% 97.69/19.31 % (4063872)Instructions burned: 135 (million)
% 97.69/19.31 % (4063873)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1869353004:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2918 on theBenchmark for (2918ds/141Mi)
% 97.69/19.31 % (4063873)Instruction limit reached!
% 97.69/19.31 % (4063873)------------------------------
% 97.69/19.31 % (4063873)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 97.69/19.31 % (4063873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.69/19.31 % (4063873)CaDiCaL version: 2.1.3
% 97.69/19.31 % (4063873)Termination reason: Instruction limit
% 97.69/19.31 % (4063873)Termination phase: SInE selection
% 97.69/19.31 % (4063873)Time elapsed: 0.112 s
% 97.69/19.31 % (4063873)Peak memory usage: 201 MB
% 97.69/19.31 % (4063873)Instructions burned: 142 (million)
% 97.69/19.31 % (4063875)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=722036946:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2916 on theBenchmark for (2916ds/431Mi)
% 97.69/19.31 % (4063877)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=3962406621:i=6060:aac=none:ins=25_2915 on theBenchmark for (2915ds/6060Mi)
% 97.69/19.31 % (4063875)Instruction limit reached!
% 97.69/19.31 % (4063875)------------------------------
% 97.69/19.31 % (4063875)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 97.69/19.31 % (4063875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.69/19.31 % (4063875)CaDiCaL version: 2.1.3
% 97.69/19.31 % (4063875)Termination reason: Instruction limit
% 97.69/19.31 % (4063875)Termination phase: SInE selection
% 97.69/19.31 % (4063875)Time elapsed: 0.326 s
% 97.69/19.31 % (4063875)Peak memory usage: 202 MB
% 97.69/19.31 % (4063875)Instructions burned: 431 (million)
% 97.69/19.31 % (4063880)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=1553044367:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2911 on theBenchmark for (2911ds/150Mi)
% 97.69/19.31 % (4063880)Instruction limit reached!
% 97.69/19.31 % (4063880)------------------------------
% 97.69/19.31 % (4063880)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 97.69/19.31 % (4063880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.69/19.31 % (4063880)CaDiCaL version: 2.1.3
% 97.69/19.31 % (4063880)Termination reason: Instruction limit
% 133.84/24.48 % (4063880)Termination phase: SInE selection
% 133.84/24.48 % (4063880)Time elapsed: 0.121 s
% 133.84/24.48 % (4063880)Peak memory usage: 201 MB
% 133.84/24.48 % (4063880)Instructions burned: 150 (million)
% 133.84/24.48 % (4063882)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3009926124:i=14155:bd=all_2908 on theBenchmark for (2908ds/14155Mi)
% 133.84/24.48 % (4063862)Instruction limit reached!
% 133.84/24.48 % (4063862)------------------------------
% 133.84/24.48 % (4063862)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 133.84/24.48 % (4063862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 133.84/24.48 % (4063862)CaDiCaL version: 2.1.3
% 133.84/24.48 % (4063862)Termination reason: Instruction limit
% 133.84/24.48 % (4063862)Termination phase: Saturation
% 133.84/24.48 % (4063862)Time elapsed: 3.462 s
% 133.84/24.48 % (4063862)Peak memory usage: 398 MB
% 133.84/24.48 % (4063862)Instructions burned: 5205 (million)
% 133.84/24.48 % (4063884)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1646614201:i=667:av=off:fsr=off_2896 on theBenchmark for (2896ds/667Mi)
% 133.84/24.48 % (4063884)Instruction limit reached!
% 133.84/24.48 % (4063884)------------------------------
% 133.84/24.48 % (4063884)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 133.84/24.48 % (4063884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 133.84/24.48 % (4063884)CaDiCaL version: 2.1.3
% 133.84/24.48 % (4063884)Termination reason: Instruction limit
% 133.84/24.48 % (4063884)Termination phase: Preprocessing 2
% 133.84/24.48 % (4063884)Time elapsed: 0.602 s
% 133.84/24.48 % (4063884)Peak memory usage: 218 MB
% 133.84/24.48 % (4063884)Instructions burned: 668 (million)
% 133.84/24.48 % (4063886)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=1371559450:s2a=on:i=185:s2at=1.8:fdi=4_2888 on theBenchmark for (2888ds/185Mi)
% 133.84/24.48 % (4063886)Instruction limit reached!
% 133.84/24.48 % (4063886)------------------------------
% 133.84/24.48 % (4063886)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 133.84/24.48 % (4063886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 133.84/24.49 % (4063886)CaDiCaL version: 2.1.3
% 133.84/24.49 % (4063886)Termination reason: Instruction limit
% 133.84/24.49 % (4063886)Termination phase: SInE selection
% 133.84/24.49 % (4063886)Time elapsed: 0.142 s
% 133.84/24.49 % (4063886)Peak memory usage: 201 MB
% 133.84/24.49 % (4063886)Instructions burned: 185 (million)
% 133.84/24.49 % (4063888)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=3538664896:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2885 on theBenchmark for (2885ds/193Mi)
% 133.84/24.49 % (4063888)Instruction limit reached!
% 133.84/24.49 % (4063888)------------------------------
% 133.84/24.49 % (4063888)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 133.84/24.49 % (4063888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 133.84/24.49 % (4063888)CaDiCaL version: 2.1.3
% 133.84/24.49 % (4063888)Termination reason: Instruction limit
% 133.84/24.49 % (4063888)Termination phase: SInE selection
% 133.84/24.49 % (4063888)Time elapsed: 0.152 s
% 133.84/24.49 % (4063888)Peak memory usage: 201 MB
% 133.84/24.49 % (4063888)Instructions burned: 193 (million)
% 133.84/24.49 % (4063890)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=3719580851:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2882 on theBenchmark for (2882ds/4850Mi)
% 133.84/24.49 % (4063877)Instruction limit reached!
% 133.84/24.49 % (4063877)------------------------------
% 133.84/24.49 % (4063877)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 133.84/24.49 % (4063877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 133.84/24.49 % (4063877)CaDiCaL version: 2.1.3
% 133.84/24.49 % (4063877)Termination reason: Instruction limit
% 133.84/24.49 % (4063877)Termination phase: NewCNF
% 133.84/24.49 % (4063877)Time elapsed: 4.887 s
% 133.84/24.49 % (4063877)Peak memory usage: 381 MB
% 133.84/24.49 % (4063877)Instructions burned: 6061 (million)
% 133.84/24.49 % (4063892)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=330696801:i=12111:sd=1:ss=included_2864 on theBenchmark for (2864ds/12111Mi)
% 133.84/24.49 % (4063890)Instruction limit reached!
% 133.84/24.49 % (4063890)------------------------------
% 133.84/24.49 % (4063890)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 168.53/29.37 % (4063890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 168.53/29.37 % (4063890)CaDiCaL version: 2.1.3
% 168.53/29.37 % (4063890)Termination reason: Instruction limit
% 168.53/29.37 % (4063890)Termination phase: Property scanning
% 168.53/29.37 % (4063890)Time elapsed: 3.324 s
% 168.53/29.37 % (4063890)Peak memory usage: 355 MB
% 168.53/29.37 % (4063890)Instructions burned: 4852 (million)
% 168.53/29.37 % (4063867)Instruction limit reached!
% 168.53/29.37 % (4063867)------------------------------
% 168.53/29.37 % (4063867)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 168.53/29.37 % (4063867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 168.53/29.37 % (4063867)CaDiCaL version: 2.1.3
% 168.53/29.37 % (4063867)Termination reason: Instruction limit
% 168.53/29.37 % (4063867)Termination phase: Saturation
% 168.53/29.37 % (4063867)Time elapsed: 7.819 s
% 168.53/29.37 % (4063867)Peak memory usage: 463 MB
% 168.53/29.37 % (4063867)Instructions burned: 13193 (million)
% 168.53/29.37 % (4063894)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=312782650:i=319:kws=precedence:fsr=off_2846 on theBenchmark for (2846ds/319Mi)
% 168.53/29.37 % (4063895)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=3900745389:i=2064:ep=RST_2846 on theBenchmark for (2846ds/2064Mi)
% 168.53/29.37 % (4063894)Instruction limit reached!
% 168.53/29.37 % (4063894)------------------------------
% 168.53/29.37 % (4063894)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 168.53/29.37 % (4063894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 168.53/29.37 % (4063894)CaDiCaL version: 2.1.3
% 168.53/29.37 % (4063894)Termination reason: Instruction limit
% 168.53/29.37 % (4063894)Termination phase: Preprocessing 1
% 168.53/29.37 % (4063894)Time elapsed: 0.230 s
% 168.53/29.37 % (4063894)Peak memory usage: 203 MB
% 168.53/29.37 % (4063894)Instructions burned: 319 (million)
% 168.53/29.37 % (4063898)dis-1011_128_sil=32000:random_seed=296585705:i=3706:ep=RST:av=off_2842 on theBenchmark for (2842ds/3706Mi)
% 168.53/29.37 % (4063882)Instruction limit reached!
% 168.53/29.37 % (4063882)------------------------------
% 168.53/29.37 % (4063882)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 168.53/29.37 % (4063882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 168.53/29.37 % (4063882)CaDiCaL version: 2.1.3
% 168.53/29.37 % (4063882)Termination reason: Instruction limit
% 168.53/29.37 % (4063882)Termination phase: Property scanning
% 168.53/29.37 % (4063882)Time elapsed: 7.101 s
% 168.53/29.37 % (4063882)Peak memory usage: 447 MB
% 168.53/29.37 % (4063882)Instructions burned: 14156 (million)
% 168.53/29.37 % (4063900)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=2451064317:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2835 on theBenchmark for (2835ds/757Mi)
% 168.53/29.37 % (4063895)Instruction limit reached!
% 168.53/29.37 % (4063895)------------------------------
% 168.53/29.37 % (4063895)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 168.53/29.37 % (4063895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 168.53/29.37 % (4063895)CaDiCaL version: 2.1.3
% 168.53/29.37 % (4063895)Termination reason: Instruction limit
% 168.53/29.37 % (4063895)Termination phase: Preprocessing 3
% 168.53/29.37 % (4063895)Time elapsed: 1.586 s
% 168.53/29.37 % (4063895)Peak memory usage: 317 MB
% 168.53/29.37 % (4063895)Instructions burned: 2065 (million)
% 168.53/29.38 % (4063900)Instruction limit reached!
% 168.53/29.38 % (4063900)------------------------------
% 168.53/29.38 % (4063900)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 168.53/29.38 % (4063900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 168.53/29.38 % (4063900)CaDiCaL version: 2.1.3
% 168.53/29.38 % (4063900)Termination reason: Instruction limit
% 168.53/29.38 % (4063900)Termination phase: Saturation
% 168.53/29.38 % (4063900)Time elapsed: 0.621 s
% 168.53/29.38 % (4063900)Peak memory usage: 209 MB
% 168.53/29.38 % (4063900)Instructions burned: 758 (million)
% 168.53/29.38 % (4063902)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=1199818731:i=13913:ss=axioms:sgt=8_2828 on theBenchmark for (2828ds/13913Mi)
% 168.53/29.38 % (4063903)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=3328469573:i=9925:aac=none_2827 on theBenchmark for (2827ds/9925Mi)
% 168.53/29.38 % (4063898)Instruction limit reached!
% 168.53/29.38 % (4063898)------------------------------
% 168.53/29.38 % (4063898)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 200.40/33.84 % (4063898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 200.40/33.84 % (4063898)CaDiCaL version: 2.1.3
% 200.40/33.84 % (4063898)Termination reason: Instruction limit
% 200.40/33.84 % (4063898)Termination phase: Preprocessing 3
% 200.40/33.84 % (4063898)Time elapsed: 2.588 s
% 200.40/33.84 % (4063898)Peak memory usage: 378 MB
% 200.40/33.84 % (4063898)Instructions burned: 3707 (million)
% 200.40/33.84 % (4063906)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=4205285018:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2814 on theBenchmark for (2814ds/2479Mi)
% 200.40/33.84 % (4063906)Instruction limit reached!
% 200.40/33.84 % (4063906)------------------------------
% 200.40/33.84 % (4063906)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 200.40/33.84 % (4063906)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 200.40/33.84 % (4063906)CaDiCaL version: 2.1.3
% 200.40/33.84 % (4063906)Termination reason: Instruction limit
% 200.40/33.84 % (4063906)Termination phase: Saturation
% 200.40/33.84 % (4063906)Time elapsed: 1.781 s
% 200.40/33.84 % (4063906)Peak memory usage: 216 MB
% 200.40/33.84 % (4063906)Instructions burned: 2480 (million)
% 200.40/33.84 % (4063908)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=596789215:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2795 on theBenchmark for (2795ds/440Mi)
% 200.40/33.84 % (4063908)Instruction limit reached!
% 200.40/33.84 % (4063908)------------------------------
% 200.40/33.84 % (4063908)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 200.40/33.84 % (4063908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 200.40/33.84 % (4063908)CaDiCaL version: 2.1.3
% 200.40/33.84 % (4063908)Termination reason: Instruction limit
% 200.40/33.84 % (4063908)Termination phase: Property scanning
% 200.40/33.84 % (4063908)Time elapsed: 0.197 s
% 200.40/33.84 % (4063908)Peak memory usage: 201 MB
% 200.40/33.84 % (4063908)Instructions burned: 443 (million)
% 200.40/33.84 % (4063910)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=1173755922:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2791 on theBenchmark for (2791ds/11145Mi)
% 200.40/33.84 % (4063892)Instruction limit reached!
% 200.40/33.84 % (4063892)------------------------------
% 200.40/33.84 % (4063892)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 200.40/33.84 % (4063892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 200.40/33.84 % (4063892)CaDiCaL version: 2.1.3
% 200.40/33.84 % (4063892)Termination reason: Instruction limit
% 200.40/33.84 % (4063892)Termination phase: Saturation
% 200.40/33.84 % (4063892)Time elapsed: 7.372 s
% 200.40/33.84 % (4063892)Peak memory usage: 355 MB
% 200.40/33.84 % (4063892)Instructions burned: 12112 (million)
% 200.40/33.84 % (4063912)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=1621790148:cts=off:i=3034:av=off:er=known:fsd=on_2788 on theBenchmark for (2788ds/3034Mi)
% 200.40/33.84 % (4063903)Instruction limit reached!
% 200.40/33.84 % (4063903)------------------------------
% 200.40/33.84 % (4063903)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 200.40/33.84 % (4063903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 200.40/33.84 % (4063903)CaDiCaL version: 2.1.3
% 200.40/33.84 % (4063903)Termination reason: Instruction limit
% 200.40/33.84 % (4063903)Termination phase: Property scanning
% 200.40/33.84 % (4063903)Time elapsed: 5.626 s
% 200.40/33.84 % (4063903)Peak memory usage: 447 MB
% 200.40/33.84 % (4063903)Instructions burned: 9928 (million)
% 200.40/33.84 % (4063914)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=3497220503:st=2:s2a=on:i=524:s2at=2:ss=axioms_2768 on theBenchmark for (2768ds/524Mi)
% 200.40/33.84 % (4063912)Instruction limit reached!
% 200.40/33.84 % (4063912)------------------------------
% 200.40/33.84 % (4063912)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 200.40/33.84 % (4063912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 200.40/33.84 % (4063912)CaDiCaL version: 2.1.3
% 200.40/33.84 % (4063912)Termination reason: Instruction limit
% 200.40/33.84 % (4063912)Termination phase: Preprocessing 3
% 200.40/33.84 % (4063912)Time elapsed: 2.290 s
% 200.40/33.84 % (4063912)Peak memory usage: 337 MB
% 200.40/33.84 % (4063912)Instructions burned: 3034 (million)
% 200.40/33.84 % (4063914)Instruction limit reached!
% 200.40/33.84 % (4063914)------------------------------
% 200.40/33.84 % (4063914)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 243.80/39.97 % (4063914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 243.80/39.97 % (4063914)CaDiCaL version: 2.1.3
% 243.80/39.97 % (4063914)Termination reason: Instruction limit
% 243.80/39.97 % (4063914)Termination phase: SInE selection
% 243.80/39.97 % (4063914)Time elapsed: 0.355 s
% 243.80/39.97 % (4063914)Peak memory usage: 202 MB
% 243.80/39.97 % (4063914)Instructions burned: 525 (million)
% 243.80/39.97 % (4063916)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=1677074461:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2763 on theBenchmark for (2763ds/1016Mi)
% 243.80/39.97 % (4063917)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=2265111155:i=14123:bd=preordered:ins=4_2763 on theBenchmark for (2763ds/14123Mi)
% 243.80/39.97 % (4063916)Instruction limit reached!
% 243.80/39.97 % (4063916)------------------------------
% 243.80/39.97 % (4063916)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 243.80/39.97 % (4063916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 243.80/39.97 % (4063916)CaDiCaL version: 2.1.3
% 243.80/39.97 % (4063916)Termination reason: Instruction limit
% 243.80/39.97 % (4063916)Termination phase: Saturation
% 243.80/39.97 % (4063916)Time elapsed: 0.691 s
% 243.80/39.97 % (4063916)Peak memory usage: 215 MB
% 243.80/39.97 % (4063916)Instructions burned: 1016 (million)
% 243.80/39.97 % (4063920)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=466934720:i=5781:kws=precedence:bd=all:rawr=on_2754 on theBenchmark for (2754ds/5781Mi)
% 243.80/39.97 % (4063902)Instruction limit reached!
% 243.80/39.97 % (4063902)------------------------------
% 243.80/39.97 % (4063902)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 243.80/39.97 % (4063902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 243.80/39.97 % (4063902)CaDiCaL version: 2.1.3
% 243.80/39.97 % (4063902)Termination reason: Instruction limit
% 243.80/39.97 % (4063902)Termination phase: Saturation
% 243.80/39.97 % (4063902)Time elapsed: 8.444 s
% 243.80/39.97 % (4063902)Peak memory usage: 368 MB
% 243.80/39.97 % (4063902)Instructions burned: 13914 (million)
% 243.80/39.97 % (4063922)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=3200685995:i=2448:gtgl=5:bd=preordered:gtg=all_2742 on theBenchmark for (2742ds/2448Mi)
% 243.80/39.97 % (4063922)Instruction limit reached!
% 243.80/39.97 % (4063922)------------------------------
% 243.80/39.97 % (4063922)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 243.80/39.97 % (4063922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 243.80/39.97 % (4063922)CaDiCaL version: 2.1.3
% 243.80/39.97 % (4063922)Termination reason: Instruction limit
% 243.80/39.97 % (4063922)Termination phase: Property scanning
% 243.80/39.97 % (4063922)Time elapsed: 1.047 s
% 243.80/39.97 % (4063922)Peak memory usage: 201 MB
% 243.80/39.97 % (4063922)Instructions burned: 2449 (million)
% 243.80/39.97 % (4063924)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=2354975081:i=3223:kws=precedence:fgj=on:av=off_2729 on theBenchmark for (2729ds/3223Mi)
% 243.80/39.97 % (4063910)Instruction limit reached!
% 243.80/39.97 % (4063910)------------------------------
% 243.80/39.97 % (4063910)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 243.80/39.97 % (4063910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 243.80/39.97 % (4063910)CaDiCaL version: 2.1.3
% 243.80/39.97 % (4063910)Termination reason: Instruction limit
% 243.80/39.97 % (4063910)Termination phase: Saturation
% 243.80/39.97 % (4063910)Time elapsed: 7.204 s
% 243.80/39.97 % (4063910)Peak memory usage: 325 MB
% 243.80/39.97 % (4063910)Instructions burned: 11145 (million)
% 243.80/39.97 % (4063926)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=3715635225:st=5.6:i=2033:sd=3:ss=axioms_2716 on theBenchmark for (2716ds/2033Mi)
% 243.80/39.97 % (4063920)Instruction limit reached!
% 243.80/39.97 % (4063920)------------------------------
% 243.80/39.97 % (4063920)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 243.80/39.97 % (4063920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 243.80/39.97 % (4063920)CaDiCaL version: 2.1.3
% 243.80/39.97 % (4063920)Termination reason: Instruction limit
% 243.80/39.97 % (4063920)Termination phase: Property scanning
% 243.80/39.97 % (4063920)Time elapsed: 3.839 s
% 236.09/44.34 % (4063920)Peak memory usage: 412 MB
% 236.09/44.34 % (4063920)Instructions burned: 5782 (million)
% 236.09/44.34 % (4063948)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=3968263511:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2714 on theBenchmark for (2714ds/2055Mi)
% 236.09/44.34 % (4063924)Instruction limit reached!
% 236.09/44.34 % (4063924)------------------------------
% 236.09/44.34 % (4063924)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 236.09/44.34 % (4063924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 236.09/44.34 % (4063924)CaDiCaL version: 2.1.3
% 236.09/44.34 % (4063924)Termination reason: Instruction limit
% 236.09/44.34 % (4063924)Termination phase: Preprocessing 3
% 236.09/44.34 % (4063924)Time elapsed: 2.334 s
% 236.09/44.34 % (4063924)Peak memory usage: 343 MB
% 236.09/44.34 % (4063924)Instructions burned: 3224 (million)
% 236.09/44.34 % (4064082)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=508826978:i=21611:sd=3:ss=axioms_2704 on theBenchmark for (2704ds/21611Mi)
% 236.09/44.34 % (4063948)Instruction limit reached!
% 236.09/44.34 % (4063948)------------------------------
% 236.09/44.34 % (4063948)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 236.09/44.34 % (4063948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 236.09/44.34 % (4063948)CaDiCaL version: 2.1.3
% 236.09/44.34 % (4063948)Termination reason: Instruction limit
% 236.09/44.34 % (4063948)Termination phase: SInE selection
% 236.09/44.34 % (4063948)Time elapsed: 1.060 s
% 236.09/44.34 % (4063948)Peak memory usage: 203 MB
% 236.09/44.34 % (4063948)Instructions burned: 2055 (million)
% 236.09/44.34 % (4064084)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=2821203407:i=4835:sd=13:ss=axioms:sgt=23_2701 on theBenchmark for (2701ds/4835Mi)
% 236.09/44.34 % (4063926)Instruction limit reached!
% 236.09/44.34 % (4063926)------------------------------
% 236.09/44.34 % (4063926)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 236.09/44.34 % (4063926)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 236.09/44.34 % (4063926)CaDiCaL version: 2.1.3
% 236.09/44.34 % (4063926)Termination reason: Instruction limit
% 236.09/44.35 % (4063926)Termination phase: Preprocessing 3
% 236.09/44.35 % (4063926)Time elapsed: 1.516 s
% 236.09/44.35 % (4063926)Peak memory usage: 230 MB
% 236.09/44.35 % (4063926)Instructions burned: 2034 (million)
% 236.09/44.35 % (4064086)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=361680889:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2699 on theBenchmark for (2699ds/797Mi)
% 236.09/44.35 % (4064086)Instruction limit reached!
% 236.09/44.35 % (4064086)------------------------------
% 236.09/44.35 % (4064086)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 236.09/44.35 % (4064086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 236.09/44.35 % (4064086)CaDiCaL version: 2.1.3
% 236.09/44.35 % (4064086)Termination reason: Instruction limit
% 236.09/44.35 % (4064086)Termination phase: SInE selection
% 236.09/44.35 % (4064086)Time elapsed: 0.531 s
% 236.09/44.35 % (4064086)Peak memory usage: 203 MB
% 236.09/44.35 % (4064086)Instructions burned: 799 (million)
% 236.09/44.35 % (4064088)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=3348448647:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2692 on theBenchmark for (2692ds/2326Mi)
% 236.09/44.35 % (4064088)Instruction limit reached!
% 236.09/44.35 % (4064088)------------------------------
% 236.09/44.35 % (4064088)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 236.09/44.35 % (4064088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 236.09/44.35 % (4064088)CaDiCaL version: 2.1.3
% 236.09/44.35 % (4064088)Termination reason: Instruction limit
% 236.09/44.35 % (4064088)Termination phase: Preprocessing 3
% 236.09/44.35 % (4064088)Time elapsed: 1.778 s
% 236.09/44.35 % (4064088)Peak memory usage: 335 MB
% 236.09/44.35 % (4064088)Instructions burned: 2326 (million)
% 236.09/44.35 % (4064090)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=3413604968:i=6038:nm=6_2672 on theBenchmark for (2672ds/6038Mi)
% 236.09/44.35 % (4064084)Instruction limit reached!
% 236.09/44.35 % (4064084)------------------------------
% 236.09/44.35 % (4064084)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 236.09/44.35 % (4064084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 236.09/44.35 % (4064084)CaDiCaL version: 2.1.3
% 236.09/44.35 % (4064084)Termination reason: Instruction limit
% 236.09/44.35 % (4064084)Termination phase: Saturation
% 236.09/44.35 % (4064084)Time elapsed: 2.998 s
% 236.09/44.35 % (4064084)Peak memory usage: 252 MB
% 236.09/44.35 % (4064084)Instructions burned: 4836 (million)
% 236.09/44.35 % (4064093)lrs+10_1_sil=32000:sp=occurrence:random_seed=380640761:st=2:i=33334:sd=3:ss=included:sgt=32_2669 on theBenchmark for (2669ds/33334Mi)
% 236.09/44.35 % (4063917)Instruction limit reached!
% 236.09/44.35 % (4063917)------------------------------
% 236.09/44.35 % (4063917)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 236.09/44.35 % (4063917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 236.09/44.35 % (4063917)CaDiCaL version: 2.1.3
% 236.09/44.35 % (4063917)Termination reason: Instruction limit
% 236.09/44.35 % (4063917)Termination phase: Saturation
% 236.09/44.35 % (4063917)Time elapsed: 10.038 s
% 236.09/44.35 % (4063917)Peak memory usage: 1207 MB
% 236.09/44.35 % (4063917)Instructions burned: 14125 (million)
% 236.09/44.35 % (4064095)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=285030990:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2660 on theBenchmark for (2660ds/1008Mi)
% 236.09/44.35 % (4064095)Instruction limit reached!
% 236.09/44.35 % (4064095)------------------------------
% 236.09/44.35 % (4064095)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 236.09/44.35 % (4064095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 236.09/44.35 % (4064095)CaDiCaL version: 2.1.3
% 236.09/44.35 % (4064095)Termination reason: Instruction limit
% 236.09/44.35 % (4064095)Termination phase: SInE selection
% 236.09/44.35 % (4064095)Time elapsed: 0.715 s
% 236.09/44.35 % (4064095)Peak memory usage: 203 MB
% 236.09/44.35 % (4064095)Instructions burned: 1009 (million)
% 236.09/44.35 % (4064097)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=128000:tgt=ground:npcc=on:fde=none:sp=const_frequency:spb=intro:gs=on:random_seed=17581858:i=8327:s2at=5:bd=preordered_2650 on theBenchmark for (2650ds/8327Mi)
% 236.09/44.35 % (4064090)Instruction limit reached!
% 236.09/44.35 % (4064090)------------------------------
% 236.09/44.35 % (4064090)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 236.09/44.35 % (4064090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 236.09/44.35 % (4064090)CaDiCaL version: 2.1.3
% 236.09/44.35 % (4064090)Termination reason: Instruction limit
% 236.09/44.35 % (4064090)Termination phase: Property scanning
% 236.09/44.35 % (4064090)Time elapsed: 3.903 s
% 236.09/44.35 % (4064090)Peak memory usage: 419 MB
% 236.09/44.35 % (4064090)Instructions burned: 6038 (million)
% 236.09/44.35 % (4064099)lrs+1002_1_slsqr=3,2:sil=8000:tgt=full:plsq=on:fde=unused:plsqc=1:plsqr=3,2:sp=reverse_arity:spb=intro:urr=on:plsql=on:s2agt=16:br=off:slsqc=2:slsq=on:random_seed=2153124929:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2631 on theBenchmark for (2631ds/1083Mi)
% 236.09/44.35 % (4064099)Instruction limit reached!
% 236.09/44.35 % (4064099)------------------------------
% 236.09/44.35 % (4064099)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 236.09/44.35 % (4064099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 236.09/44.35 % (4064099)CaDiCaL version: 2.1.3
% 236.09/44.35 % (4064099)Termination reason: Instruction limit
% 236.09/44.35 % (4064099)Termination phase: Preprocessing 1
% 236.09/44.35 % (4064099)Time elapsed: 0.904 s
% 236.09/44.35 % (4064099)Peak memory usage: 206 MB
% 236.09/44.35 % (4064099)Instructions burned: 1083 (million)
% 236.09/44.35 % (4064101)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=2114587318:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2620 on theBenchmark for (2620ds/1084Mi)
% 236.09/44.35 % (4064101)Instruction limit reached!
% 236.09/44.35 % (4064101)------------------------------
% 236.09/44.35 % (4064101)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 236.09/44.35 % (4064101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 236.09/44.35 % (4064101)CaDiCaL version: 2.1.3
% 236.09/44.35 % (4064101)Termination reason: Instruction limit
% 236.09/44.35 % (4064101)Termination phase: Saturation
% 236.09/44.35 % (4064101)Time elapsed: 0.788 s
% 236.09/44.35 % (4064101)Peak memory usage: 212 MB
% 236.09/44.35 % (4064101)Instructions burned: 1084 (million)
% 236.09/44.35 % (4064103)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=811395763:i=6995:s2at=5:gtg=all_2610 on theBenchmark for (2610ds/6995Mi)
% 236.09/44.35 % (4064097)Instruction limit reached!
% 236.09/44.35 % (4064097)------------------------------
% 236.09/44.35 % (4064097)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 236.09/44.35 % (4064097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 236.09/44.35 % (4064097)CaDiCaL version: 2.1.3
% 236.09/44.35 % (4064097)Termination reason: Instruction limit
% 236.09/44.35 % (4064097)Termination phase: Equality resolution with deletion
% 236.09/44.35 % (4064097)Time elapsed: 4.964 s
% 236.09/44.35 % (4064097)Peak memory usage: 416 MB
% 236.09/44.35 % (4064097)Instructions burned: 8328 (million)
% 236.09/44.35 % (4064105)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=3713337450:st=2:i=6225:sd=15:ss=axioms_2599 on theBenchmark for (2599ds/6225Mi)
% 236.09/44.35 % (4064082)First to succeed.
% 236.09/44.35 % (4064082)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-4063821"
% 236.09/44.35 % (4064082)Refutation found. Thanks to Tanya!
% 236.09/44.35 % SZS status Theorem for theBenchmark
% 236.09/44.35 % SZS output start Proof for theBenchmark
% See solution above
% 274.81/44.60 % (4064082)------------------------------
% 274.81/44.60 % (4064082)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 274.81/44.60 % (4064082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 274.81/44.60 % (4064082)CaDiCaL version: 2.1.3
% 274.81/44.60 % (4064082)Termination reason: Refutation
% 274.81/44.60 % (4064082)Time elapsed: 13.239 s
% 274.81/44.60 % (4064082)Peak memory usage: 404 MB
% 274.81/44.60 % (4064082)Instructions burned: 21649 (million)
% 274.81/44.60 % (4064082)------------------------------
% 274.81/44.60 % (4064082)------------------------------
% 274.81/44.60 % (4063821)Success in time 43.504 s
% 274.81/44.60 % Vampire exiting
%------------------------------------------------------------------------------