%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT289+2 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n016.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 11:46:34 AM UTC 2026
% Result : Theorem 2.99s 1.94s
% Output : Refutation 0.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 21
% Syntax : Number of formulae : 202 ( 30 unt; 10 def)
% Number of atoms : 927 ( 80 equ)
% Maximal formula atoms : 16 ( 4 avg)
% Number of connectives : 1208 ( 483 ~; 562 |; 121 &)
% ( 24 <=>; 18 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 27 ( 25 usr; 11 prp; 0-3 aty)
% Number of functors : 17 ( 17 usr; 4 con; 0-4 aty)
% Number of variables : 148 ( 0 sgn 132 !; 16 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f29,axiom,
! [X0] :
( X0 = k1_xboole_0
<=> ! [X1] : ~ r2_hidden(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_xboole_0) ).
fof(f68,axiom,
! [X0,X1] :
~ ( r2_hidden(X0,X1)
& v1_xboole_0(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t7_boole) ).
fof(f932,axiom,
! [X0] :
( ( v1_relat_1(X0)
& v1_funct_1(X0) )
=> ! [X1,X2] :
( ( r2_hidden(X1,k1_relat_1(X0))
=> ( X2 = k1_funct_1(X0,X1)
<=> r2_hidden(k4_tarski(X1,X2),X0) ) )
& ( ~ r2_hidden(X1,k1_relat_1(X0))
=> ( X2 = k1_funct_1(X0,X1)
<=> X2 = k1_xboole_0 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d4_funct_1) ).
fof(f1318,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
<=> m1_relset_1(X2,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(f1902,axiom,
! [X0,X1,X2,X3] :
( ( ~ v1_xboole_0(X0)
& v1_funct_1(X2)
& v1_funct_2(X2,X0,X1)
& m1_relset_1(X2,X0,X1)
& m1_subset_1(X3,X0) )
=> k8_funct_2(X0,X1,X2,X3) = k1_funct_1(X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k8_funct_2) ).
fof(f6400,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& ~ v3_realset2(X0)
& l3_lattices(X0) )
=> ( v1_relat_1(k8_lopclset(X0))
& v1_funct_1(k8_lopclset(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k8_lopclset) ).
fof(f6401,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& ~ v3_realset2(X0)
& l3_lattices(X0) )
=> ( v1_funct_1(k9_lopclset(X0))
& v1_funct_2(k9_lopclset(X0),u1_struct_0(X0),k1_zfmisc_1(k7_lopclset(X0)))
& m2_relset_1(k9_lopclset(X0),u1_struct_0(X0),k1_zfmisc_1(k7_lopclset(X0))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k9_lopclset) ).
fof(f6402,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& ~ v3_realset2(X0)
& l3_lattices(X0) )
=> k9_lopclset(X0) = k8_lopclset(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k9_lopclset) ).
fof(f6435,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& ~ v3_realset2(X0)
& l3_lattices(X0) )
=> ! [X1] :
( ( v1_relat_1(X1)
& v1_funct_1(X1) )
=> ( X1 = k8_lopclset(X0)
<=> ( k1_relat_1(X1) = u1_struct_0(X0)
& ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> k1_funct_1(X1,X2) = a_2_0_lopclset(X0,X2) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d6_lopclset) ).
fof(f6436,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& v17_lattices(X1)
& ~ v3_realset2(X1)
& l3_lattices(X1) )
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X1))
=> ( r2_hidden(X0,k1_funct_1(k8_lopclset(X1),X2))
<=> ? [X3] :
( m1_filter_0(X3,X1)
& X3 = X0
& v1_filter_0(X3,X1)
& r2_hidden(X2,X3) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t20_lopclset) ).
fof(f6447,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& ~ v3_realset2(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_filter_0(X2,X0)
=> ~ ( v1_filter_0(X2,X0)
& ~ r2_hidden(X2,k8_funct_2(u1_struct_0(X0),k1_zfmisc_1(k7_lopclset(X0)),k9_lopclset(X0),X1))
& r2_hidden(X1,X2) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t27_lopclset) ).
fof(f6448,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& ~ v3_realset2(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_filter_0(X2,X0)
=> ~ ( v1_filter_0(X2,X0)
& ~ r2_hidden(X2,k8_funct_2(u1_struct_0(X0),k1_zfmisc_1(k7_lopclset(X0)),k9_lopclset(X0),X1))
& r2_hidden(X1,X2) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f6447]) ).
fof(f6552,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( v1_filter_0(X2,X0)
& ~ r2_hidden(X2,k8_funct_2(u1_struct_0(X0),k1_zfmisc_1(k7_lopclset(X0)),k9_lopclset(X0),X1))
& r2_hidden(X1,X2)
& m1_filter_0(X2,X0) )
& m1_subset_1(X1,u1_struct_0(X0)) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& ~ v3_realset2(X0)
& l3_lattices(X0) ),
inference(ennf_transformation,[],[f6448]) ).
fof(f6553,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( v1_filter_0(X2,X0)
& ~ r2_hidden(X2,k8_funct_2(u1_struct_0(X0),k1_zfmisc_1(k7_lopclset(X0)),k9_lopclset(X0),X1))
& r2_hidden(X1,X2)
& m1_filter_0(X2,X0) )
& m1_subset_1(X1,u1_struct_0(X0)) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& ~ v3_realset2(X0)
& l3_lattices(X0) ),
inference(flattening,[],[f6552]) ).
fof(f6615,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| ~ v1_xboole_0(X1) ),
inference(ennf_transformation,[],[f68]) ).
fof(f6647,plain,
! [X0,X1,X2,X3] :
( k8_funct_2(X0,X1,X2,X3) = k1_funct_1(X2,X3)
| v1_xboole_0(X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1)
| ~ m1_subset_1(X3,X0) ),
inference(ennf_transformation,[],[f1902]) ).
fof(f6648,plain,
! [X0,X1,X2,X3] :
( k8_funct_2(X0,X1,X2,X3) = k1_funct_1(X2,X3)
| v1_xboole_0(X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1)
| ~ m1_subset_1(X3,X0) ),
inference(flattening,[],[f6647]) ).
fof(f6705,plain,
! [X0,X1] :
( ! [X2] :
( ( r2_hidden(X0,k1_funct_1(k8_lopclset(X1),X2))
<=> ? [X3] :
( m1_filter_0(X3,X1)
& X3 = X0
& v1_filter_0(X3,X1)
& r2_hidden(X2,X3) ) )
| ~ m1_subset_1(X2,u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ v17_lattices(X1)
| v3_realset2(X1)
| ~ l3_lattices(X1) ),
inference(ennf_transformation,[],[f6436]) ).
fof(f6706,plain,
! [X0,X1] :
( ! [X2] :
( ( r2_hidden(X0,k1_funct_1(k8_lopclset(X1),X2))
<=> ? [X3] :
( m1_filter_0(X3,X1)
& X3 = X0
& v1_filter_0(X3,X1)
& r2_hidden(X2,X3) ) )
| ~ m1_subset_1(X2,u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ v17_lattices(X1)
| v3_realset2(X1)
| ~ l3_lattices(X1) ),
inference(flattening,[],[f6705]) ).
fof(f6727,plain,
! [X0] :
( ( v1_funct_1(k9_lopclset(X0))
& v1_funct_2(k9_lopclset(X0),u1_struct_0(X0),k1_zfmisc_1(k7_lopclset(X0)))
& m2_relset_1(k9_lopclset(X0),u1_struct_0(X0),k1_zfmisc_1(k7_lopclset(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f6401]) ).
fof(f6728,plain,
! [X0] :
( ( v1_funct_1(k9_lopclset(X0))
& v1_funct_2(k9_lopclset(X0),u1_struct_0(X0),k1_zfmisc_1(k7_lopclset(X0)))
& m2_relset_1(k9_lopclset(X0),u1_struct_0(X0),k1_zfmisc_1(k7_lopclset(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f6727]) ).
fof(f6733,plain,
! [X0] :
( k9_lopclset(X0) = k8_lopclset(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f6402]) ).
fof(f6734,plain,
! [X0] :
( k9_lopclset(X0) = k8_lopclset(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f6733]) ).
fof(f6872,plain,
! [X0] :
( ! [X1,X2] :
( ( ( X2 = k1_funct_1(X0,X1)
<=> r2_hidden(k4_tarski(X1,X2),X0) )
| ~ r2_hidden(X1,k1_relat_1(X0)) )
& ( ( X2 = k1_funct_1(X0,X1)
<=> X2 = k1_xboole_0 )
| r2_hidden(X1,k1_relat_1(X0)) ) )
| ~ v1_relat_1(X0)
| ~ v1_funct_1(X0) ),
inference(ennf_transformation,[],[f932]) ).
fof(f6873,plain,
! [X0] :
( ! [X1,X2] :
( ( ( X2 = k1_funct_1(X0,X1)
<=> r2_hidden(k4_tarski(X1,X2),X0) )
| ~ r2_hidden(X1,k1_relat_1(X0)) )
& ( ( X2 = k1_funct_1(X0,X1)
<=> X2 = k1_xboole_0 )
| r2_hidden(X1,k1_relat_1(X0)) ) )
| ~ v1_relat_1(X0)
| ~ v1_funct_1(X0) ),
inference(flattening,[],[f6872]) ).
fof(f7969,plain,
! [X0] :
( ! [X1] :
( ( X1 = k8_lopclset(X0)
<=> ( k1_relat_1(X1) = u1_struct_0(X0)
& ! [X2] :
( k1_funct_1(X1,X2) = a_2_0_lopclset(X0,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0)) ) ) )
| ~ v1_relat_1(X1)
| ~ v1_funct_1(X1) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f6435]) ).
fof(f7970,plain,
! [X0] :
( ! [X1] :
( ( X1 = k8_lopclset(X0)
<=> ( k1_relat_1(X1) = u1_struct_0(X0)
& ! [X2] :
( k1_funct_1(X1,X2) = a_2_0_lopclset(X0,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0)) ) ) )
| ~ v1_relat_1(X1)
| ~ v1_funct_1(X1) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f7969]) ).
fof(f7973,plain,
! [X0] :
( ( v1_relat_1(k8_lopclset(X0))
& v1_funct_1(k8_lopclset(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f6400]) ).
fof(f7974,plain,
! [X0] :
( ( v1_relat_1(k8_lopclset(X0))
& v1_funct_1(k8_lopclset(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f7973]) ).
fof(f8007,plain,
( v1_filter_0(sK13,sK11)
& ~ r2_hidden(sK13,k8_funct_2(u1_struct_0(sK11),k1_zfmisc_1(k7_lopclset(sK11)),k9_lopclset(sK11),sK12))
& r2_hidden(sK12,sK13)
& m1_filter_0(sK13,sK11)
& m1_subset_1(sK12,u1_struct_0(sK11))
& ~ v3_struct_0(sK11)
& v10_lattices(sK11)
& v17_lattices(sK11)
& ~ v3_realset2(sK11)
& l3_lattices(sK11) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11,sK12,sK13]),skolemize(X0,sK11),skolemize(X1,sK12),skolemize(X2,sK13)],[f6553]) ).
fof(f8037,plain,
! [X0] :
( ( X0 = k1_xboole_0
| ? [X1] : r2_hidden(X1,X0) )
& ( ! [X1] : ~ r2_hidden(X1,X0)
| k1_xboole_0 != X0 ) ),
inference(nnf_transformation,[],[f29]) ).
fof(f8038,plain,
! [X0] :
( ( X0 = k1_xboole_0
| ? [X1] : r2_hidden(X1,X0) )
& ( ! [X2] : ~ r2_hidden(X2,X0)
| k1_xboole_0 != X0 ) ),
inference(rectify,[],[f8037]) ).
fof(f8039,plain,
! [X0] :
( ( X0 = k1_xboole_0
| r2_hidden(sK35(X0),X0) )
& ( ! [X2] : ~ r2_hidden(X2,X0)
| k1_xboole_0 != X0 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK35]),skolemize(X1,sK35(X0))],[f8038]) ).
fof(f8095,plain,
! [X0,X1] :
( ! [X2] :
( ( ( r2_hidden(X0,k1_funct_1(k8_lopclset(X1),X2))
| ! [X3] :
( ~ m1_filter_0(X3,X1)
| X0 != X3
| ~ v1_filter_0(X3,X1)
| ~ r2_hidden(X2,X3) ) )
& ( ? [X3] :
( m1_filter_0(X3,X1)
& X3 = X0
& v1_filter_0(X3,X1)
& r2_hidden(X2,X3) )
| ~ r2_hidden(X0,k1_funct_1(k8_lopclset(X1),X2)) ) )
| ~ m1_subset_1(X2,u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ v17_lattices(X1)
| v3_realset2(X1)
| ~ l3_lattices(X1) ),
inference(nnf_transformation,[],[f6706]) ).
fof(f8096,plain,
! [X0,X1] :
( ! [X2] :
( ( ( r2_hidden(X0,k1_funct_1(k8_lopclset(X1),X2))
| ! [X3] :
( ~ m1_filter_0(X3,X1)
| X0 != X3
| ~ v1_filter_0(X3,X1)
| ~ r2_hidden(X2,X3) ) )
& ( ? [X4] :
( m1_filter_0(X4,X1)
& X0 = X4
& v1_filter_0(X4,X1)
& r2_hidden(X2,X4) )
| ~ r2_hidden(X0,k1_funct_1(k8_lopclset(X1),X2)) ) )
| ~ m1_subset_1(X2,u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ v17_lattices(X1)
| v3_realset2(X1)
| ~ l3_lattices(X1) ),
inference(rectify,[],[f8095]) ).
fof(f8097,plain,
! [X0,X1] :
( ! [X2] :
( ( ( r2_hidden(X0,k1_funct_1(k8_lopclset(X1),X2))
| ! [X3] :
( ~ m1_filter_0(X3,X1)
| X0 != X3
| ~ v1_filter_0(X3,X1)
| ~ r2_hidden(X2,X3) ) )
& ( ( m1_filter_0(sK66(X0,X1,X2),X1)
& sK66(X0,X1,X2) = X0
& v1_filter_0(sK66(X0,X1,X2),X1)
& r2_hidden(X2,sK66(X0,X1,X2)) )
| ~ r2_hidden(X0,k1_funct_1(k8_lopclset(X1),X2)) ) )
| ~ m1_subset_1(X2,u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ v17_lattices(X1)
| v3_realset2(X1)
| ~ l3_lattices(X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK66]),skolemize(X4,sK66(X0,X1,X2))],[f8096]) ).
fof(f8178,plain,
! [X0] :
( ! [X1,X2] :
( ( ( ( X2 = k1_funct_1(X0,X1)
| ~ r2_hidden(k4_tarski(X1,X2),X0) )
& ( r2_hidden(k4_tarski(X1,X2),X0)
| k1_funct_1(X0,X1) != X2 ) )
| ~ r2_hidden(X1,k1_relat_1(X0)) )
& ( ( ( X2 = k1_funct_1(X0,X1)
| k1_xboole_0 != X2 )
& ( X2 = k1_xboole_0
| k1_funct_1(X0,X1) != X2 ) )
| r2_hidden(X1,k1_relat_1(X0)) ) )
| ~ v1_relat_1(X0)
| ~ v1_funct_1(X0) ),
inference(nnf_transformation,[],[f6873]) ).
fof(f8402,plain,
! [X0,X1,X2] :
( ( m2_relset_1(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1) )
& ( m1_relset_1(X2,X0,X1)
| ~ m2_relset_1(X2,X0,X1) ) ),
inference(nnf_transformation,[],[f1318]) ).
fof(f8494,plain,
! [X0] :
( ! [X1] :
( ( ( X1 = k8_lopclset(X0)
| k1_relat_1(X1) != u1_struct_0(X0)
| ? [X2] :
( k1_funct_1(X1,X2) != a_2_0_lopclset(X0,X2)
& m1_subset_1(X2,u1_struct_0(X0)) ) )
& ( ( k1_relat_1(X1) = u1_struct_0(X0)
& ! [X2] :
( k1_funct_1(X1,X2) = a_2_0_lopclset(X0,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0)) ) )
| k8_lopclset(X0) != X1 ) )
| ~ v1_relat_1(X1)
| ~ v1_funct_1(X1) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f7970]) ).
fof(f8495,plain,
! [X0] :
( ! [X1] :
( ( ( X1 = k8_lopclset(X0)
| k1_relat_1(X1) != u1_struct_0(X0)
| ? [X2] :
( k1_funct_1(X1,X2) != a_2_0_lopclset(X0,X2)
& m1_subset_1(X2,u1_struct_0(X0)) ) )
& ( ( k1_relat_1(X1) = u1_struct_0(X0)
& ! [X2] :
( k1_funct_1(X1,X2) = a_2_0_lopclset(X0,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0)) ) )
| k8_lopclset(X0) != X1 ) )
| ~ v1_relat_1(X1)
| ~ v1_funct_1(X1) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f8494]) ).
fof(f8496,plain,
! [X0] :
( ! [X1] :
( ( ( X1 = k8_lopclset(X0)
| k1_relat_1(X1) != u1_struct_0(X0)
| ? [X2] :
( k1_funct_1(X1,X2) != a_2_0_lopclset(X0,X2)
& m1_subset_1(X2,u1_struct_0(X0)) ) )
& ( ( k1_relat_1(X1) = u1_struct_0(X0)
& ! [X3] :
( k1_funct_1(X1,X3) = a_2_0_lopclset(X0,X3)
| ~ m1_subset_1(X3,u1_struct_0(X0)) ) )
| k8_lopclset(X0) != X1 ) )
| ~ v1_relat_1(X1)
| ~ v1_funct_1(X1) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(rectify,[],[f8495]) ).
fof(f8497,plain,
! [X0] :
( ! [X1] :
( ( ( X1 = k8_lopclset(X0)
| k1_relat_1(X1) != u1_struct_0(X0)
| ( k1_funct_1(X1,sK322(X0,X1)) != a_2_0_lopclset(X0,sK322(X0,X1))
& m1_subset_1(sK322(X0,X1),u1_struct_0(X0)) ) )
& ( ( k1_relat_1(X1) = u1_struct_0(X0)
& ! [X3] :
( k1_funct_1(X1,X3) = a_2_0_lopclset(X0,X3)
| ~ m1_subset_1(X3,u1_struct_0(X0)) ) )
| k8_lopclset(X0) != X1 ) )
| ~ v1_relat_1(X1)
| ~ v1_funct_1(X1) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK322]),skolemize(X2,sK322(X0,X1))],[f8496]) ).
fof(f8500,plain,
l3_lattices(sK11),
inference(cnf_transformation,[],[f8007]) ).
fof(f8501,plain,
~ v3_realset2(sK11),
inference(cnf_transformation,[],[f8007]) ).
fof(f8502,plain,
v17_lattices(sK11),
inference(cnf_transformation,[],[f8007]) ).
fof(f8503,plain,
v10_lattices(sK11),
inference(cnf_transformation,[],[f8007]) ).
fof(f8504,plain,
~ v3_struct_0(sK11),
inference(cnf_transformation,[],[f8007]) ).
fof(f8505,plain,
m1_subset_1(sK12,u1_struct_0(sK11)),
inference(cnf_transformation,[],[f8007]) ).
fof(f8506,plain,
m1_filter_0(sK13,sK11),
inference(cnf_transformation,[],[f8007]) ).
fof(f8507,plain,
r2_hidden(sK12,sK13),
inference(cnf_transformation,[],[f8007]) ).
fof(f8508,plain,
~ r2_hidden(sK13,k8_funct_2(u1_struct_0(sK11),k1_zfmisc_1(k7_lopclset(sK11)),k9_lopclset(sK11),sK12)),
inference(cnf_transformation,[],[f8007]) ).
fof(f8509,plain,
v1_filter_0(sK13,sK11),
inference(cnf_transformation,[],[f8007]) ).
fof(f8585,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| ~ v1_xboole_0(X1) ),
inference(cnf_transformation,[],[f6615]) ).
fof(f8586,plain,
! [X2,X0] :
( ~ r2_hidden(X2,X0)
| k1_xboole_0 != X0 ),
inference(cnf_transformation,[],[f8039]) ).
fof(f8649,plain,
! [X2,X3,X0,X1] :
( k1_funct_1(X2,X3) = k8_funct_2(X0,X1,X2,X3)
| v1_xboole_0(X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1)
| ~ m1_subset_1(X3,X0) ),
inference(cnf_transformation,[],[f6648]) ).
fof(f8729,plain,
! [X2,X3,X0,X1] :
( r2_hidden(X0,k1_funct_1(k8_lopclset(X1),X2))
| ~ m1_filter_0(X3,X1)
| X0 != X3
| ~ v1_filter_0(X3,X1)
| ~ r2_hidden(X2,X3)
| ~ m1_subset_1(X2,u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ v17_lattices(X1)
| v3_realset2(X1)
| ~ l3_lattices(X1) ),
inference(cnf_transformation,[],[f8097]) ).
fof(f8764,plain,
! [X0] :
( m2_relset_1(k9_lopclset(X0),u1_struct_0(X0),k1_zfmisc_1(k7_lopclset(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f6728]) ).
fof(f8765,plain,
! [X0] :
( v1_funct_2(k9_lopclset(X0),u1_struct_0(X0),k1_zfmisc_1(k7_lopclset(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f6728]) ).
fof(f8766,plain,
! [X0] :
( v1_funct_1(k9_lopclset(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f6728]) ).
fof(f8769,plain,
! [X0] :
( k8_lopclset(X0) = k9_lopclset(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f6734]) ).
fof(f8981,plain,
! [X2,X0,X1] :
( k1_xboole_0 = X2
| k1_funct_1(X0,X1) != X2
| r2_hidden(X1,k1_relat_1(X0))
| ~ v1_relat_1(X0)
| ~ v1_funct_1(X0) ),
inference(cnf_transformation,[],[f8178]) ).
fof(f10068,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f8402]) ).
fof(f10559,plain,
! [X0,X1] :
( k1_relat_1(X1) = u1_struct_0(X0)
| k8_lopclset(X0) != X1
| ~ v1_relat_1(X1)
| ~ v1_funct_1(X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f8497]) ).
fof(f10563,plain,
! [X0] :
( v1_funct_1(k8_lopclset(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f7974]) ).
fof(f10564,plain,
! [X0] :
( v1_relat_1(k8_lopclset(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f7974]) ).
fof(f10968,plain,
! [X2] : ~ r2_hidden(X2,k1_xboole_0),
inference(equality_resolution,[],[f8586]) ).
fof(f10972,plain,
! [X2,X3,X1] :
( r2_hidden(X3,k1_funct_1(k8_lopclset(X1),X2))
| ~ m1_filter_0(X3,X1)
| ~ v1_filter_0(X3,X1)
| ~ r2_hidden(X2,X3)
| ~ m1_subset_1(X2,u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ v17_lattices(X1)
| v3_realset2(X1)
| ~ l3_lattices(X1) ),
inference(equality_resolution,[],[f8729]) ).
fof(f11007,plain,
! [X0,X1] :
( k1_xboole_0 = k1_funct_1(X0,X1)
| r2_hidden(X1,k1_relat_1(X0))
| ~ v1_relat_1(X0)
| ~ v1_funct_1(X0) ),
inference(equality_resolution,[],[f8981]) ).
fof(f11136,plain,
! [X0] :
( u1_struct_0(X0) = k1_relat_1(k8_lopclset(X0))
| ~ v1_relat_1(k8_lopclset(X0))
| ~ v1_funct_1(k8_lopclset(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(equality_resolution,[],[f10559]) ).
fof(f11212,definition,
( spl323_3
<=> v1_xboole_0(u1_struct_0(sK11)) ),
introduced(definition,[new_symbols(definition,[spl323_3])],[avatar_definition]) ).
fof(f11213,plain,
( ~ v1_xboole_0(u1_struct_0(sK11))
| spl323_3 ),
inference(avatar_component_clause,[],[f11212]) ).
fof(f11214,plain,
( v1_xboole_0(u1_struct_0(sK11))
| ~ spl323_3 ),
inference(avatar_component_clause,[],[f11212]) ).
fof(f11244,plain,
( ~ r2_hidden(sK13,k1_funct_1(k9_lopclset(sK11),sK12))
| v1_xboole_0(u1_struct_0(sK11))
| ~ v1_funct_1(k9_lopclset(sK11))
| ~ v1_funct_2(k9_lopclset(sK11),u1_struct_0(sK11),k1_zfmisc_1(k7_lopclset(sK11)))
| ~ m1_relset_1(k9_lopclset(sK11),u1_struct_0(sK11),k1_zfmisc_1(k7_lopclset(sK11)))
| ~ m1_subset_1(sK12,u1_struct_0(sK11)) ),
inference(superposition,[],[f8508,f8649]) ).
fof(f11249,plain,
( ~ r2_hidden(sK13,k1_funct_1(k9_lopclset(sK11),sK12))
| ~ v1_funct_1(k9_lopclset(sK11))
| ~ v1_funct_2(k9_lopclset(sK11),u1_struct_0(sK11),k1_zfmisc_1(k7_lopclset(sK11)))
| ~ m1_relset_1(k9_lopclset(sK11),u1_struct_0(sK11),k1_zfmisc_1(k7_lopclset(sK11)))
| ~ m1_subset_1(sK12,u1_struct_0(sK11))
| spl323_3 ),
inference(forward_subsumption_resolution,[],[f11244,f11213]) ).
fof(f11254,plain,
( ~ r2_hidden(sK13,k1_funct_1(k9_lopclset(sK11),sK12))
| ~ v1_funct_1(k9_lopclset(sK11))
| ~ v1_funct_2(k9_lopclset(sK11),u1_struct_0(sK11),k1_zfmisc_1(k7_lopclset(sK11)))
| ~ m1_relset_1(k9_lopclset(sK11),u1_struct_0(sK11),k1_zfmisc_1(k7_lopclset(sK11)))
| spl323_3 ),
inference(forward_subsumption_resolution,[],[f11249,f8505]) ).
fof(f11260,definition,
( spl323_8
<=> m1_relset_1(k9_lopclset(sK11),u1_struct_0(sK11),k1_zfmisc_1(k7_lopclset(sK11))) ),
introduced(definition,[new_symbols(definition,[spl323_8])],[avatar_definition]) ).
fof(f11262,plain,
( ~ m1_relset_1(k9_lopclset(sK11),u1_struct_0(sK11),k1_zfmisc_1(k7_lopclset(sK11)))
| spl323_8 ),
inference(avatar_component_clause,[],[f11260]) ).
fof(f11264,definition,
( spl323_9
<=> v1_funct_2(k9_lopclset(sK11),u1_struct_0(sK11),k1_zfmisc_1(k7_lopclset(sK11))) ),
introduced(definition,[new_symbols(definition,[spl323_9])],[avatar_definition]) ).
fof(f11266,plain,
( ~ v1_funct_2(k9_lopclset(sK11),u1_struct_0(sK11),k1_zfmisc_1(k7_lopclset(sK11)))
| spl323_9 ),
inference(avatar_component_clause,[],[f11264]) ).
fof(f11268,definition,
( spl323_10
<=> v1_funct_1(k9_lopclset(sK11)) ),
introduced(definition,[new_symbols(definition,[spl323_10])],[avatar_definition]) ).
fof(f11269,plain,
( v1_funct_1(k9_lopclset(sK11))
| ~ spl323_10 ),
inference(avatar_component_clause,[],[f11268]) ).
fof(f11270,plain,
( ~ v1_funct_1(k9_lopclset(sK11))
| spl323_10 ),
inference(avatar_component_clause,[],[f11268]) ).
fof(f11272,definition,
( spl323_11
<=> r2_hidden(sK13,k1_funct_1(k9_lopclset(sK11),sK12)) ),
introduced(definition,[new_symbols(definition,[spl323_11])],[avatar_definition]) ).
fof(f11273,plain,
( r2_hidden(sK13,k1_funct_1(k9_lopclset(sK11),sK12))
| ~ spl323_11 ),
inference(avatar_component_clause,[],[f11272]) ).
fof(f11274,plain,
( ~ r2_hidden(sK13,k1_funct_1(k9_lopclset(sK11),sK12))
| spl323_11 ),
inference(avatar_component_clause,[],[f11272]) ).
fof(f11275,plain,
( ~ spl323_8
| ~ spl323_9
| ~ spl323_10
| ~ spl323_11
| spl323_3 ),
inference(avatar_split_clause,[],[f11254,f11212,f11272,f11268,f11264,f11260]) ).
fof(f11279,definition,
( spl323_12
<=> m2_relset_1(k9_lopclset(sK11),u1_struct_0(sK11),k1_zfmisc_1(k7_lopclset(sK11))) ),
introduced(definition,[new_symbols(definition,[spl323_12])],[avatar_definition]) ).
fof(f11280,plain,
( m2_relset_1(k9_lopclset(sK11),u1_struct_0(sK11),k1_zfmisc_1(k7_lopclset(sK11)))
| ~ spl323_12 ),
inference(avatar_component_clause,[],[f11279]) ).
fof(f11281,plain,
( ~ m2_relset_1(k9_lopclset(sK11),u1_struct_0(sK11),k1_zfmisc_1(k7_lopclset(sK11)))
| spl323_12 ),
inference(avatar_component_clause,[],[f11279]) ).
fof(f11293,plain,
( v3_struct_0(sK11)
| ~ v10_lattices(sK11)
| ~ v17_lattices(sK11)
| v3_realset2(sK11)
| ~ l3_lattices(sK11)
| spl323_10 ),
inference(resolution,[],[f11270,f8766]) ).
fof(f11297,plain,
( ~ v10_lattices(sK11)
| ~ v17_lattices(sK11)
| v3_realset2(sK11)
| ~ l3_lattices(sK11)
| spl323_10 ),
inference(forward_subsumption_resolution,[],[f11293,f8504]) ).
fof(f11299,plain,
( ~ v17_lattices(sK11)
| v3_realset2(sK11)
| ~ l3_lattices(sK11)
| spl323_10 ),
inference(forward_subsumption_resolution,[],[f11297,f8503]) ).
fof(f11301,plain,
( v3_realset2(sK11)
| ~ l3_lattices(sK11)
| spl323_10 ),
inference(forward_subsumption_resolution,[],[f11299,f8502]) ).
fof(f11303,plain,
( ~ l3_lattices(sK11)
| spl323_10 ),
inference(forward_subsumption_resolution,[],[f11301,f8501]) ).
fof(f11305,plain,
( $false
| spl323_10 ),
inference(forward_subsumption_resolution,[],[f11303,f8500]) ).
fof(f11306,plain,
spl323_10,
inference(avatar_contradiction_clause,[],[f11305]) ).
fof(f11379,plain,
( ~ r2_hidden(sK13,k1_funct_1(k8_lopclset(sK11),sK12))
| v3_struct_0(sK11)
| ~ v10_lattices(sK11)
| ~ v17_lattices(sK11)
| v3_realset2(sK11)
| ~ l3_lattices(sK11)
| spl323_11 ),
inference(superposition,[],[f11274,f8769]) ).
fof(f11382,plain,
( ~ r2_hidden(sK13,k1_funct_1(k8_lopclset(sK11),sK12))
| ~ v10_lattices(sK11)
| ~ v17_lattices(sK11)
| v3_realset2(sK11)
| ~ l3_lattices(sK11)
| spl323_11 ),
inference(forward_subsumption_resolution,[],[f11379,f8504]) ).
fof(f11383,plain,
( ~ r2_hidden(sK13,k1_funct_1(k8_lopclset(sK11),sK12))
| ~ v17_lattices(sK11)
| v3_realset2(sK11)
| ~ l3_lattices(sK11)
| spl323_11 ),
inference(forward_subsumption_resolution,[],[f11382,f8503]) ).
fof(f11384,plain,
( ~ r2_hidden(sK13,k1_funct_1(k8_lopclset(sK11),sK12))
| v3_realset2(sK11)
| ~ l3_lattices(sK11)
| spl323_11 ),
inference(forward_subsumption_resolution,[],[f11383,f8502]) ).
fof(f11385,plain,
( ~ r2_hidden(sK13,k1_funct_1(k8_lopclset(sK11),sK12))
| ~ l3_lattices(sK11)
| spl323_11 ),
inference(forward_subsumption_resolution,[],[f11384,f8501]) ).
fof(f11386,plain,
( ~ r2_hidden(sK13,k1_funct_1(k8_lopclset(sK11),sK12))
| spl323_11 ),
inference(forward_subsumption_resolution,[],[f11385,f8500]) ).
fof(f11399,plain,
( v3_struct_0(sK11)
| ~ v10_lattices(sK11)
| ~ v17_lattices(sK11)
| v3_realset2(sK11)
| ~ l3_lattices(sK11)
| spl323_9 ),
inference(resolution,[],[f11266,f8765]) ).
fof(f11409,plain,
( ~ v10_lattices(sK11)
| ~ v17_lattices(sK11)
| v3_realset2(sK11)
| ~ l3_lattices(sK11)
| spl323_9 ),
inference(forward_subsumption_resolution,[],[f11399,f8504]) ).
fof(f11420,plain,
( ~ v17_lattices(sK11)
| v3_realset2(sK11)
| ~ l3_lattices(sK11)
| spl323_9 ),
inference(forward_subsumption_resolution,[],[f11409,f8503]) ).
fof(f11423,plain,
( v3_realset2(sK11)
| ~ l3_lattices(sK11)
| spl323_9 ),
inference(forward_subsumption_resolution,[],[f11420,f8502]) ).
fof(f11425,plain,
( ~ l3_lattices(sK11)
| spl323_9 ),
inference(forward_subsumption_resolution,[],[f11423,f8501]) ).
fof(f11427,plain,
( $false
| spl323_9 ),
inference(forward_subsumption_resolution,[],[f11425,f8500]) ).
fof(f11428,plain,
spl323_9,
inference(avatar_contradiction_clause,[],[f11427]) ).
fof(f11429,plain,
( ~ m1_filter_0(sK13,sK11)
| ~ v1_filter_0(sK13,sK11)
| ~ r2_hidden(sK12,sK13)
| ~ m1_subset_1(sK12,u1_struct_0(sK11))
| v3_struct_0(sK11)
| ~ v10_lattices(sK11)
| ~ v17_lattices(sK11)
| v3_realset2(sK11)
| ~ l3_lattices(sK11)
| spl323_11 ),
inference(resolution,[],[f11386,f10972]) ).
fof(f11434,plain,
( ~ v1_filter_0(sK13,sK11)
| ~ r2_hidden(sK12,sK13)
| ~ m1_subset_1(sK12,u1_struct_0(sK11))
| v3_struct_0(sK11)
| ~ v10_lattices(sK11)
| ~ v17_lattices(sK11)
| v3_realset2(sK11)
| ~ l3_lattices(sK11)
| spl323_11 ),
inference(forward_subsumption_resolution,[],[f11429,f8506]) ).
fof(f11436,plain,
( ~ r2_hidden(sK12,sK13)
| ~ m1_subset_1(sK12,u1_struct_0(sK11))
| v3_struct_0(sK11)
| ~ v10_lattices(sK11)
| ~ v17_lattices(sK11)
| v3_realset2(sK11)
| ~ l3_lattices(sK11)
| spl323_11 ),
inference(forward_subsumption_resolution,[],[f11434,f8509]) ).
fof(f11438,plain,
( ~ m1_subset_1(sK12,u1_struct_0(sK11))
| v3_struct_0(sK11)
| ~ v10_lattices(sK11)
| ~ v17_lattices(sK11)
| v3_realset2(sK11)
| ~ l3_lattices(sK11)
| spl323_11 ),
inference(forward_subsumption_resolution,[],[f11436,f8507]) ).
fof(f11440,plain,
( v3_struct_0(sK11)
| ~ v10_lattices(sK11)
| ~ v17_lattices(sK11)
| v3_realset2(sK11)
| ~ l3_lattices(sK11)
| spl323_11 ),
inference(forward_subsumption_resolution,[],[f11438,f8505]) ).
fof(f11442,plain,
( ~ v10_lattices(sK11)
| ~ v17_lattices(sK11)
| v3_realset2(sK11)
| ~ l3_lattices(sK11)
| spl323_11 ),
inference(forward_subsumption_resolution,[],[f11440,f8504]) ).
fof(f11444,plain,
( ~ v17_lattices(sK11)
| v3_realset2(sK11)
| ~ l3_lattices(sK11)
| spl323_11 ),
inference(forward_subsumption_resolution,[],[f11442,f8503]) ).
fof(f11446,plain,
( v3_realset2(sK11)
| ~ l3_lattices(sK11)
| spl323_11 ),
inference(forward_subsumption_resolution,[],[f11444,f8502]) ).
fof(f11448,plain,
( ~ l3_lattices(sK11)
| spl323_11 ),
inference(forward_subsumption_resolution,[],[f11446,f8501]) ).
fof(f11451,plain,
( $false
| spl323_11 ),
inference(forward_subsumption_resolution,[],[f11448,f8500]) ).
fof(f11452,plain,
spl323_11,
inference(avatar_contradiction_clause,[],[f11451]) ).
fof(f11462,plain,
( r2_hidden(sK13,k1_xboole_0)
| r2_hidden(sK12,k1_relat_1(k9_lopclset(sK11)))
| ~ v1_relat_1(k9_lopclset(sK11))
| ~ v1_funct_1(k9_lopclset(sK11))
| ~ spl323_11 ),
inference(superposition,[],[f11273,f11007]) ).
fof(f11465,plain,
( r2_hidden(sK12,k1_relat_1(k9_lopclset(sK11)))
| ~ v1_relat_1(k9_lopclset(sK11))
| ~ v1_funct_1(k9_lopclset(sK11))
| ~ spl323_11 ),
inference(forward_subsumption_resolution,[],[f11462,f10968]) ).
fof(f11476,plain,
( r2_hidden(sK12,k1_relat_1(k9_lopclset(sK11)))
| ~ v1_relat_1(k9_lopclset(sK11))
| ~ spl323_10
| ~ spl323_11 ),
inference(forward_subsumption_resolution,[],[f11465,f11269]) ).
fof(f11479,definition,
( spl323_22
<=> v1_relat_1(k9_lopclset(sK11)) ),
introduced(definition,[new_symbols(definition,[spl323_22])],[avatar_definition]) ).
fof(f11481,plain,
( ~ v1_relat_1(k9_lopclset(sK11))
| spl323_22 ),
inference(avatar_component_clause,[],[f11479]) ).
fof(f11483,definition,
( spl323_23
<=> r2_hidden(sK12,k1_relat_1(k9_lopclset(sK11))) ),
introduced(definition,[new_symbols(definition,[spl323_23])],[avatar_definition]) ).
fof(f11485,plain,
( r2_hidden(sK12,k1_relat_1(k9_lopclset(sK11)))
| ~ spl323_23 ),
inference(avatar_component_clause,[],[f11483]) ).
fof(f11487,plain,
( ~ spl323_22
| spl323_23
| ~ spl323_10
| ~ spl323_11 ),
inference(avatar_split_clause,[],[f11476,f11272,f11268,f11483,f11479]) ).
fof(f11492,plain,
( ~ v1_relat_1(k8_lopclset(sK11))
| v3_struct_0(sK11)
| ~ v10_lattices(sK11)
| ~ v17_lattices(sK11)
| v3_realset2(sK11)
| ~ l3_lattices(sK11)
| spl323_22 ),
inference(superposition,[],[f11481,f8769]) ).
fof(f11493,plain,
( ~ v1_relat_1(k8_lopclset(sK11))
| ~ v10_lattices(sK11)
| ~ v17_lattices(sK11)
| v3_realset2(sK11)
| ~ l3_lattices(sK11)
| spl323_22 ),
inference(forward_subsumption_resolution,[],[f11492,f8504]) ).
fof(f11494,plain,
( ~ v1_relat_1(k8_lopclset(sK11))
| ~ v17_lattices(sK11)
| v3_realset2(sK11)
| ~ l3_lattices(sK11)
| spl323_22 ),
inference(forward_subsumption_resolution,[],[f11493,f8503]) ).
fof(f11495,plain,
( ~ v1_relat_1(k8_lopclset(sK11))
| v3_realset2(sK11)
| ~ l3_lattices(sK11)
| spl323_22 ),
inference(forward_subsumption_resolution,[],[f11494,f8502]) ).
fof(f11496,plain,
( ~ v1_relat_1(k8_lopclset(sK11))
| ~ l3_lattices(sK11)
| spl323_22 ),
inference(forward_subsumption_resolution,[],[f11495,f8501]) ).
fof(f11497,plain,
( ~ v1_relat_1(k8_lopclset(sK11))
| spl323_22 ),
inference(forward_subsumption_resolution,[],[f11496,f8500]) ).
fof(f11520,plain,
( v3_struct_0(sK11)
| ~ v10_lattices(sK11)
| ~ v17_lattices(sK11)
| v3_realset2(sK11)
| ~ l3_lattices(sK11)
| spl323_12 ),
inference(resolution,[],[f11281,f8764]) ).
fof(f11548,plain,
( ~ v10_lattices(sK11)
| ~ v17_lattices(sK11)
| v3_realset2(sK11)
| ~ l3_lattices(sK11)
| spl323_12 ),
inference(forward_subsumption_resolution,[],[f11520,f8504]) ).
fof(f11551,plain,
( ~ v17_lattices(sK11)
| v3_realset2(sK11)
| ~ l3_lattices(sK11)
| spl323_12 ),
inference(forward_subsumption_resolution,[],[f11548,f8503]) ).
fof(f11554,plain,
( v3_realset2(sK11)
| ~ l3_lattices(sK11)
| spl323_12 ),
inference(forward_subsumption_resolution,[],[f11551,f8502]) ).
fof(f11556,plain,
( ~ l3_lattices(sK11)
| spl323_12 ),
inference(forward_subsumption_resolution,[],[f11554,f8501]) ).
fof(f11558,plain,
( $false
| spl323_12 ),
inference(forward_subsumption_resolution,[],[f11556,f8500]) ).
fof(f11559,plain,
spl323_12,
inference(avatar_contradiction_clause,[],[f11558]) ).
fof(f11579,plain,
( v3_struct_0(sK11)
| ~ v10_lattices(sK11)
| ~ v17_lattices(sK11)
| v3_realset2(sK11)
| ~ l3_lattices(sK11)
| spl323_22 ),
inference(resolution,[],[f11497,f10564]) ).
fof(f11581,plain,
( ~ v10_lattices(sK11)
| ~ v17_lattices(sK11)
| v3_realset2(sK11)
| ~ l3_lattices(sK11)
| spl323_22 ),
inference(forward_subsumption_resolution,[],[f11579,f8504]) ).
fof(f11582,plain,
( ~ v17_lattices(sK11)
| v3_realset2(sK11)
| ~ l3_lattices(sK11)
| spl323_22 ),
inference(forward_subsumption_resolution,[],[f11581,f8503]) ).
fof(f11583,plain,
( v3_realset2(sK11)
| ~ l3_lattices(sK11)
| spl323_22 ),
inference(forward_subsumption_resolution,[],[f11582,f8502]) ).
fof(f11584,plain,
( ~ l3_lattices(sK11)
| spl323_22 ),
inference(forward_subsumption_resolution,[],[f11583,f8501]) ).
fof(f11585,plain,
( $false
| spl323_22 ),
inference(forward_subsumption_resolution,[],[f11584,f8500]) ).
fof(f11586,plain,
spl323_22,
inference(avatar_contradiction_clause,[],[f11585]) ).
fof(f11587,plain,
( m1_relset_1(k9_lopclset(sK11),u1_struct_0(sK11),k1_zfmisc_1(k7_lopclset(sK11)))
| ~ spl323_12 ),
inference(resolution,[],[f11280,f10068]) ).
fof(f11600,plain,
( $false
| spl323_8
| ~ spl323_12 ),
inference(forward_subsumption_resolution,[],[f11587,f11262]) ).
fof(f11601,plain,
( spl323_8
| ~ spl323_12 ),
inference(avatar_contradiction_clause,[],[f11600]) ).
fof(f11827,plain,
( ~ v1_xboole_0(k1_relat_1(k9_lopclset(sK11)))
| ~ spl323_23 ),
inference(resolution,[],[f11485,f8585]) ).
fof(f11855,plain,
( ~ v1_xboole_0(k1_relat_1(k8_lopclset(sK11)))
| v3_struct_0(sK11)
| ~ v10_lattices(sK11)
| ~ v17_lattices(sK11)
| v3_realset2(sK11)
| ~ l3_lattices(sK11)
| ~ spl323_23 ),
inference(superposition,[],[f11827,f8769]) ).
fof(f11857,plain,
( ~ v1_xboole_0(k1_relat_1(k8_lopclset(sK11)))
| ~ v10_lattices(sK11)
| ~ v17_lattices(sK11)
| v3_realset2(sK11)
| ~ l3_lattices(sK11)
| ~ spl323_23 ),
inference(forward_subsumption_resolution,[],[f11855,f8504]) ).
fof(f11858,plain,
( ~ v1_xboole_0(k1_relat_1(k8_lopclset(sK11)))
| ~ v17_lattices(sK11)
| v3_realset2(sK11)
| ~ l3_lattices(sK11)
| ~ spl323_23 ),
inference(forward_subsumption_resolution,[],[f11857,f8503]) ).
fof(f11859,plain,
( ~ v1_xboole_0(k1_relat_1(k8_lopclset(sK11)))
| v3_realset2(sK11)
| ~ l3_lattices(sK11)
| ~ spl323_23 ),
inference(forward_subsumption_resolution,[],[f11858,f8502]) ).
fof(f11860,plain,
( ~ v1_xboole_0(k1_relat_1(k8_lopclset(sK11)))
| ~ l3_lattices(sK11)
| ~ spl323_23 ),
inference(forward_subsumption_resolution,[],[f11859,f8501]) ).
fof(f11861,plain,
( ~ v1_xboole_0(k1_relat_1(k8_lopclset(sK11)))
| ~ spl323_23 ),
inference(forward_subsumption_resolution,[],[f11860,f8500]) ).
fof(f11955,plain,
( ~ v1_xboole_0(u1_struct_0(sK11))
| ~ v1_relat_1(k8_lopclset(sK11))
| ~ v1_funct_1(k8_lopclset(sK11))
| v3_struct_0(sK11)
| ~ v10_lattices(sK11)
| ~ v17_lattices(sK11)
| v3_realset2(sK11)
| ~ l3_lattices(sK11)
| ~ spl323_23 ),
inference(superposition,[],[f11861,f11136]) ).
fof(f11958,plain,
( ~ v1_relat_1(k8_lopclset(sK11))
| ~ v1_funct_1(k8_lopclset(sK11))
| v3_struct_0(sK11)
| ~ v10_lattices(sK11)
| ~ v17_lattices(sK11)
| v3_realset2(sK11)
| ~ l3_lattices(sK11)
| ~ spl323_3
| ~ spl323_23 ),
inference(forward_subsumption_resolution,[],[f11955,f11214]) ).
fof(f11960,definition,
( spl323_39
<=> v1_relat_1(k8_lopclset(sK11)) ),
introduced(definition,[new_symbols(definition,[spl323_39])],[avatar_definition]) ).
fof(f11962,plain,
( ~ v1_relat_1(k8_lopclset(sK11))
| spl323_39 ),
inference(avatar_component_clause,[],[f11960]) ).
fof(f11968,plain,
( ~ v1_relat_1(k8_lopclset(sK11))
| ~ v1_funct_1(k8_lopclset(sK11))
| ~ v10_lattices(sK11)
| ~ v17_lattices(sK11)
| v3_realset2(sK11)
| ~ l3_lattices(sK11)
| ~ spl323_3
| ~ spl323_23 ),
inference(forward_subsumption_resolution,[],[f11958,f8504]) ).
fof(f11969,plain,
( ~ v1_relat_1(k8_lopclset(sK11))
| ~ v1_funct_1(k8_lopclset(sK11))
| ~ v17_lattices(sK11)
| v3_realset2(sK11)
| ~ l3_lattices(sK11)
| ~ spl323_3
| ~ spl323_23 ),
inference(forward_subsumption_resolution,[],[f11968,f8503]) ).
fof(f11970,plain,
( ~ v1_relat_1(k8_lopclset(sK11))
| ~ v1_funct_1(k8_lopclset(sK11))
| v3_realset2(sK11)
| ~ l3_lattices(sK11)
| ~ spl323_3
| ~ spl323_23 ),
inference(forward_subsumption_resolution,[],[f11969,f8502]) ).
fof(f11971,plain,
( ~ v1_relat_1(k8_lopclset(sK11))
| ~ v1_funct_1(k8_lopclset(sK11))
| ~ l3_lattices(sK11)
| ~ spl323_3
| ~ spl323_23 ),
inference(forward_subsumption_resolution,[],[f11970,f8501]) ).
fof(f11972,plain,
( ~ v1_relat_1(k8_lopclset(sK11))
| ~ v1_funct_1(k8_lopclset(sK11))
| ~ spl323_3
| ~ spl323_23 ),
inference(forward_subsumption_resolution,[],[f11971,f8500]) ).
fof(f11974,definition,
( spl323_41
<=> v1_funct_1(k8_lopclset(sK11)) ),
introduced(definition,[new_symbols(definition,[spl323_41])],[avatar_definition]) ).
fof(f11976,plain,
( ~ v1_funct_1(k8_lopclset(sK11))
| spl323_41 ),
inference(avatar_component_clause,[],[f11974]) ).
fof(f11977,plain,
( ~ spl323_41
| ~ spl323_39
| ~ spl323_3
| ~ spl323_23 ),
inference(avatar_split_clause,[],[f11972,f11483,f11212,f11960,f11974]) ).
fof(f12199,plain,
( v3_struct_0(sK11)
| ~ v10_lattices(sK11)
| ~ v17_lattices(sK11)
| v3_realset2(sK11)
| ~ l3_lattices(sK11)
| spl323_39 ),
inference(resolution,[],[f11962,f10564]) ).
fof(f12201,plain,
( ~ v10_lattices(sK11)
| ~ v17_lattices(sK11)
| v3_realset2(sK11)
| ~ l3_lattices(sK11)
| spl323_39 ),
inference(forward_subsumption_resolution,[],[f12199,f8504]) ).
fof(f12202,plain,
( ~ v17_lattices(sK11)
| v3_realset2(sK11)
| ~ l3_lattices(sK11)
| spl323_39 ),
inference(forward_subsumption_resolution,[],[f12201,f8503]) ).
fof(f12203,plain,
( v3_realset2(sK11)
| ~ l3_lattices(sK11)
| spl323_39 ),
inference(forward_subsumption_resolution,[],[f12202,f8502]) ).
fof(f12204,plain,
( ~ l3_lattices(sK11)
| spl323_39 ),
inference(forward_subsumption_resolution,[],[f12203,f8501]) ).
fof(f12205,plain,
( $false
| spl323_39 ),
inference(forward_subsumption_resolution,[],[f12204,f8500]) ).
fof(f12206,plain,
spl323_39,
inference(avatar_contradiction_clause,[],[f12205]) ).
fof(f12219,plain,
( v3_struct_0(sK11)
| ~ v10_lattices(sK11)
| ~ v17_lattices(sK11)
| v3_realset2(sK11)
| ~ l3_lattices(sK11)
| spl323_41 ),
inference(resolution,[],[f11976,f10563]) ).
fof(f12221,plain,
( ~ v10_lattices(sK11)
| ~ v17_lattices(sK11)
| v3_realset2(sK11)
| ~ l3_lattices(sK11)
| spl323_41 ),
inference(forward_subsumption_resolution,[],[f12219,f8504]) ).
fof(f12222,plain,
( ~ v17_lattices(sK11)
| v3_realset2(sK11)
| ~ l3_lattices(sK11)
| spl323_41 ),
inference(forward_subsumption_resolution,[],[f12221,f8503]) ).
fof(f12223,plain,
( v3_realset2(sK11)
| ~ l3_lattices(sK11)
| spl323_41 ),
inference(forward_subsumption_resolution,[],[f12222,f8502]) ).
fof(f12224,plain,
( ~ l3_lattices(sK11)
| spl323_41 ),
inference(forward_subsumption_resolution,[],[f12223,f8501]) ).
fof(f12225,plain,
( $false
| spl323_41 ),
inference(forward_subsumption_resolution,[],[f12224,f8500]) ).
fof(f12226,plain,
spl323_41,
inference(avatar_contradiction_clause,[],[f12225]) ).
cnf(s6,plain,
( spl323_3
| ~ spl323_8
| ~ spl323_9
| ~ spl323_10
| ~ spl323_11 ),
inference(sat_conversion,[],[f11275]) ).
cnf(s9,plain,
spl323_10,
inference(sat_conversion,[],[f11306]) ).
cnf(s13,plain,
spl323_9,
inference(sat_conversion,[],[f11428]) ).
cnf(s15,plain,
spl323_11,
inference(sat_conversion,[],[f11452]) ).
cnf(s18,plain,
( ~ spl323_10
| ~ spl323_11
| ~ spl323_22
| spl323_23 ),
inference(sat_conversion,[],[f11487]) ).
cnf(s20,plain,
spl323_12,
inference(sat_conversion,[],[f11559]) ).
cnf(s25,plain,
spl323_22,
inference(sat_conversion,[],[f11586]) ).
cnf(s28,plain,
( spl323_8
| ~ spl323_12 ),
inference(sat_conversion,[],[f11601]) ).
cnf(s38,plain,
( ~ spl323_3
| ~ spl323_23
| ~ spl323_39
| ~ spl323_41 ),
inference(sat_conversion,[],[f11977]) ).
cnf(s48,plain,
spl323_39,
inference(sat_conversion,[],[f12206]) ).
cnf(s49,plain,
spl323_41,
inference(sat_conversion,[],[f12226]) ).
cnf(s50,plain,
( ~ spl323_3
| ~ spl323_23 ),
inference(rat,[],[s38,s49,s48]) ).
cnf(s52,plain,
spl323_8,
inference(rat,[],[s28,s20]) ).
cnf(s55,plain,
( ~ spl323_10
| ~ spl323_11
| spl323_23 ),
inference(rat,[],[s18,s25]) ).
cnf(s59,plain,
spl323_23,
inference(rat,[],[s55,s15,s9]) ).
cnf(s60,plain,
~ spl323_3,
inference(rat,[],[s50,s59]) ).
cnf(s63,plain,
$false,
inference(rat,[],[s6,s15,s9,s13,s52,s60]) ).
fof(f12227,plain,
$false,
inference(avatar_sat_refutation,[],[s63]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT289+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.41 % Computer : n016.cluster.edu
% 0.11/0.41 % Model : x86_64 x86_64
% 0.11/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.41 % Memory : 8046.5625MB
% 0.11/0.41 % OS : Linux 6.8.0-71-generic
% 0.11/0.41 % CPULimit : 300
% 0.11/0.41 % WCLimit : 300
% 0.11/0.41 % DateTime : Sun Sep 27 14:19:33 UTC 2026
% 0.11/0.41 % CPUTime :
% 0.11/0.41 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.45 Running first-order theorem proving
% 0.11/0.45 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
% 2.99/1.94 % (2686118)Detected formulas, will run a generic FOF schedule.
% 2.99/1.94 % (2686126)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3399178879:i=109:sd=1:ins=1:gsp=on:ss=axioms_2997 on theBenchmark for (2997ds/109Mi)
% 2.99/1.94 % (2686123)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=3596701390:i=141193_2997 on theBenchmark for (2997ds/141193Mi)
% 2.99/1.94 % (2686127)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2173303800:i=119:av=off:ss=axioms_2997 on theBenchmark for (2997ds/119Mi)
% 2.99/1.94 % (2686128)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1802514085:s2a=on:i=139:gtg=position_2997 on theBenchmark for (2997ds/139Mi)
% 2.99/1.94 % (2686125)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=1474556508:i=141695:sd=1:nm=32:gsp=on:ss=included_2997 on theBenchmark for (2997ds/141695Mi)
% 2.99/1.94 % (2686124)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=782851407:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2997 on theBenchmark for (2997ds/134677Mi)
% 2.99/1.94 % (2686126)Instruction limit reached!
% 2.99/1.94 % (2686126)------------------------------
% 2.99/1.94 % (2686126)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.99/1.94 % (2686126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.99/1.94 % (2686126)CaDiCaL version: 2.1.3
% 2.99/1.94 % (2686126)Termination reason: Instruction limit
% 2.99/1.94 % (2686126)Termination phase: Saturation
% 2.99/1.94 % (2686126)Time elapsed: 0.043 s
% 2.99/1.94 % (2686126)Peak memory usage: 97 MB
% 2.99/1.94 % (2686126)Instructions burned: 113 (million)
% 2.99/1.94 % (2686129)dis-21_1_sil=8000:lcm=predicate:random_seed=3707170841:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2997 on theBenchmark for (2997ds/129Mi)
% 2.99/1.94 % (2686128)Instruction limit reached!
% 2.99/1.94 % (2686128)------------------------------
% 2.99/1.94 % (2686128)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.99/1.94 % (2686128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.99/1.94 % (2686128)CaDiCaL version: 2.1.3
% 2.99/1.94 % (2686128)Termination reason: Instruction limit
% 2.99/1.94 % (2686128)Termination phase: Preprocessing 1
% 2.99/1.94 % (2686128)Time elapsed: 0.082 s
% 2.99/1.94 % (2686128)Peak memory usage: 93 MB
% 2.99/1.94 % (2686128)Instructions burned: 139 (million)
% 2.99/1.94 % (2686127)Instruction limit reached!
% 2.99/1.94 % (2686127)------------------------------
% 2.99/1.94 % (2686127)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.99/1.94 % (2686127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.99/1.94 % (2686127)CaDiCaL version: 2.1.3
% 2.99/1.94 % (2686127)Termination reason: Instruction limit
% 2.99/1.94 % (2686127)Termination phase: Saturation
% 2.99/1.94 % (2686127)Time elapsed: 0.087 s
% 2.99/1.94 % (2686127)Peak memory usage: 96 MB
% 2.99/1.94 % (2686127)Instructions burned: 120 (million)
% 2.99/1.94 % (2686129)Instruction limit reached!
% 2.99/1.94 % (2686129)------------------------------
% 2.99/1.94 % (2686129)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.99/1.94 % (2686129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.99/1.94 % (2686129)CaDiCaL version: 2.1.3
% 2.99/1.94 % (2686129)Termination reason: Instruction limit
% 2.99/1.94 % (2686129)Termination phase: Preprocessing 3
% 2.99/1.94 % (2686129)Time elapsed: 0.101 s
% 2.99/1.94 % (2686129)Peak memory usage: 97 MB
% 2.99/1.94 % (2686129)Instructions burned: 130 (million)
% 2.99/1.94 % (2686136)lrs+10_1_sil=8000:sp=occurrence:random_seed=73006507:i=285:sd=3:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/285Mi)
% 2.99/1.94 % (2686139)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1828221427:i=325:sd=1:ss=axioms:sgt=32_2994 on theBenchmark for (2994ds/325Mi)
% 2.99/1.94 % (2686138)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1238658095:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2994 on theBenchmark for (2994ds/157Mi)
% 2.99/1.94 % (2686136)Instruction limit reached!
% 2.99/1.94 % (2686136)------------------------------
% 2.99/1.94 % (2686136)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.99/1.94 % (2686136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.99/1.94 % (2686136)CaDiCaL version: 2.1.3
% 2.99/1.94 % (2686136)Termination reason: Instruction limit
% 2.99/1.94 % (2686136)Termination phase: Saturation
% 2.99/1.94 % (2686136)Time elapsed: 0.112 s
% 2.99/1.94 % (2686136)Peak memory usage: 99 MB
% 2.99/1.94 % (2686136)Instructions burned: 286 (million)
% 2.99/1.94 % (2686141)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=2371044320:s2a=on:i=248:s2at=1.23:gtg=position_2994 on theBenchmark for (2994ds/248Mi)
% 2.99/1.94 % (2686138)Instruction limit reached!
% 2.99/1.94 % (2686138)------------------------------
% 2.99/1.94 % (2686138)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.99/1.94 % (2686138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.99/1.94 % (2686138)CaDiCaL version: 2.1.3
% 2.99/1.94 % (2686138)Termination reason: Instruction limit
% 2.99/1.94 % (2686138)Termination phase: Saturation
% 2.99/1.94 % (2686138)Time elapsed: 0.089 s
% 2.99/1.94 % (2686138)Peak memory usage: 96 MB
% 2.99/1.94 % (2686138)Instructions burned: 158 (million)
% 2.99/1.94 % (2686144)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3661557293:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi)
% 2.99/1.94 % (2686144)First to succeed.
% 2.99/1.94 % (2686144)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2686118"
% 2.99/1.94 % (2686141)Instruction limit reached!
% 2.99/1.94 % (2686141)------------------------------
% 2.99/1.94 % (2686141)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.99/1.94 % (2686141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.99/1.94 % (2686141)CaDiCaL version: 2.1.3
% 2.99/1.94 % (2686141)Termination reason: Instruction limit
% 2.99/1.94 % (2686141)Termination phase: Preprocessing 3
% 2.99/1.94 % (2686141)Time elapsed: 0.158 s
% 2.99/1.94 % (2686141)Peak memory usage: 101 MB
% 2.99/1.94 % (2686141)Instructions burned: 248 (million)
% 2.99/1.94 % (2686139)Instruction limit reached!
% 2.99/1.94 % (2686139)------------------------------
% 2.99/1.94 % (2686139)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.99/1.94 % (2686139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.99/1.94 % (2686139)CaDiCaL version: 2.1.3
% 2.99/1.94 % (2686139)Termination reason: Instruction limit
% 2.99/1.94 % (2686139)Termination phase: Saturation
% 2.99/1.94 % (2686139)Time elapsed: 0.228 s
% 2.99/1.94 % (2686139)Peak memory usage: 99 MB
% 2.99/1.94 % (2686139)Instructions burned: 326 (million)
% 2.99/1.94 % (2686146)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2438993517:i=2350_2992 on theBenchmark for (2992ds/2350Mi)
% 2.99/1.94 % (2686144)Refutation found. Thanks to Tanya!
% 2.99/1.94 % SZS status Theorem for theBenchmark
% 2.99/1.94 % SZS output start Proof for theBenchmark
% See solution above
% 0.18/2.14 % (2686144)------------------------------
% 0.18/2.14 % (2686144)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.18/2.14 % (2686144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/2.14 % (2686144)CaDiCaL version: 2.1.3
% 0.18/2.14 % (2686144)Termination reason: Refutation
% 0.18/2.14 % (2686144)Time elapsed: 0.080 s
% 0.18/2.14 % (2686144)Peak memory usage: 101 MB
% 0.18/2.14 % (2686144)Instructions burned: 245 (million)
% 0.18/2.14 % (2686144)------------------------------
% 0.18/2.14 % (2686144)------------------------------
% 0.18/2.14 % (2686118)Success in time 1.047 s
% 0.18/2.14 % Vampire exiting
%------------------------------------------------------------------------------