%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT330+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 : n026.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:47:00 AM UTC 2026
% Result : Theorem 16.15s 3.26s
% Output : Refutation 16.82s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 24
% Syntax : Number of formulae : 214 ( 30 unt; 9 def)
% Number of atoms : 860 ( 22 equ)
% Maximal formula atoms : 13 ( 4 avg)
% Number of connectives : 1152 ( 506 ~; 530 |; 71 &)
% ( 17 <=>; 28 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 21 ( 19 usr; 6 prp; 0-3 aty)
% Number of functors : 12 ( 12 usr; 6 con; 0-3 aty)
% Number of variables : 233 ( 0 sgn 227 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f8,axiom,
! [X0,X1] :
( r1_tarski(X0,X1)
<=> ! [X2] :
( r2_hidden(X2,X0)
=> r2_hidden(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d3_tarski) ).
fof(f38,axiom,
! [X0,X1] :
( X0 = X1
<=> ( r1_tarski(X0,X1)
& r1_tarski(X1,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d10_xboole_0) ).
fof(f584,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(f2392,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v13_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> r3_lattices(X0,k5_lattices(X0),X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t41_lattices) ).
fof(f2410,axiom,
! [X0] :
( l3_lattices(X0)
=> ( l1_lattices(X0)
& l2_lattices(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l3_lattices) ).
fof(f2425,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_lattices(X0) )
=> m1_subset_1(k5_lattices(X0),u1_struct_0(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k5_lattices) ).
fof(f2857,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_lattice4(X1,X0)
=> m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m2_lattice4) ).
fof(f2874,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_filter_2(X1,X0)
=> ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m2_filter_2) ).
fof(f2878,axiom,
! [X0,X1,X2] :
( ( ~ v1_xboole_0(X0)
& m1_subset_1(X1,k1_zfmisc_1(X0))
& m1_subset_1(X2,k1_zfmisc_1(X0)) )
=> ( r1_filter_2(X0,X1,X2)
<=> X1 = X2 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_r1_filter_2) ).
fof(f2908,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& m1_subset_1(X1,u1_struct_0(X0)) )
=> m2_filter_2(k18_filter_2(X0,X1),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k18_filter_2) ).
fof(f2913,axiom,
! [X0,X1,X2] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& m1_subset_1(X1,u1_struct_0(X0))
& m1_subset_1(X2,u1_struct_0(X0)) )
=> ( ~ v1_xboole_0(k22_filter_2(X0,X1,X2))
& m2_lattice4(k22_filter_2(X0,X1,X2),X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k22_filter_2) ).
fof(f2953,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> m2_filter_2(u1_struct_0(X0),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t28_filter_2) ).
fof(f2956,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ( r2_hidden(X1,k18_filter_2(X0,X2))
<=> r3_lattices(X0,X1,X2) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t29_filter_2) ).
fof(f3000,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
=> ( r3_lattices(X0,X1,X2)
=> ( r2_hidden(X3,k22_filter_2(X0,X1,X2))
<=> ( r3_lattices(X0,X1,X3)
& r3_lattices(X0,X3,X2) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t63_filter_2) ).
fof(f3004,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ( v13_lattices(X0)
=> r1_filter_2(u1_struct_0(X0),k18_filter_2(X0,X1),k22_filter_2(X0,k5_lattices(X0),X1)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t67_filter_2) ).
fof(f3005,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ( v13_lattices(X0)
=> r1_filter_2(u1_struct_0(X0),k18_filter_2(X0,X1),k22_filter_2(X0,k5_lattices(X0),X1)) ) ) ),
inference(negated_conjecture,[status(cth)],[f3004]) ).
fof(f3097,plain,
! [X0,X1] :
( r1_tarski(X0,X1)
<=> ! [X2] :
( r2_hidden(X2,X1)
| ~ r2_hidden(X2,X0) ) ),
inference(ennf_transformation,[],[f8]) ).
fof(f3434,plain,
! [X0,X1,X2] :
( m1_subset_1(X0,X2)
| ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2)) ),
inference(ennf_transformation,[],[f584]) ).
fof(f3435,plain,
! [X0,X1,X2] :
( m1_subset_1(X0,X2)
| ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2)) ),
inference(flattening,[],[f3434]) ).
fof(f5394,plain,
! [X0] :
( ! [X1] :
( r3_lattices(X0,k5_lattices(X0),X1)
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v13_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2392]) ).
fof(f5395,plain,
! [X0] :
( ! [X1] :
( r3_lattices(X0,k5_lattices(X0),X1)
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v13_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f5394]) ).
fof(f5420,plain,
! [X0] :
( ( l1_lattices(X0)
& l2_lattices(X0) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2410]) ).
fof(f5447,plain,
! [X0] :
( m1_subset_1(k5_lattices(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_lattices(X0) ),
inference(ennf_transformation,[],[f2425]) ).
fof(f5448,plain,
! [X0] :
( m1_subset_1(k5_lattices(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_lattices(X0) ),
inference(flattening,[],[f5447]) ).
fof(f6059,plain,
! [X0] :
( ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m2_lattice4(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2857]) ).
fof(f6060,plain,
! [X0] :
( ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m2_lattice4(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f6059]) ).
fof(f6093,plain,
! [X0] :
( ! [X1] :
( ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2874]) ).
fof(f6094,plain,
! [X0] :
( ! [X1] :
( ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f6093]) ).
fof(f6101,plain,
! [X0,X1,X2] :
( ( r1_filter_2(X0,X1,X2)
<=> X1 = X2 )
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f2878]) ).
fof(f6102,plain,
! [X0,X1,X2] :
( ( r1_filter_2(X0,X1,X2)
<=> X1 = X2 )
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(flattening,[],[f6101]) ).
fof(f6161,plain,
! [X0,X1] :
( m2_filter_2(k18_filter_2(X0,X1),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f2908]) ).
fof(f6162,plain,
! [X0,X1] :
( m2_filter_2(k18_filter_2(X0,X1),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(flattening,[],[f6161]) ).
fof(f6171,plain,
! [X0,X1,X2] :
( ( ~ v1_xboole_0(k22_filter_2(X0,X1,X2))
& m2_lattice4(k22_filter_2(X0,X1,X2),X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f2913]) ).
fof(f6172,plain,
! [X0,X1,X2] :
( ( ~ v1_xboole_0(k22_filter_2(X0,X1,X2))
& m2_lattice4(k22_filter_2(X0,X1,X2),X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(flattening,[],[f6171]) ).
fof(f6248,plain,
! [X0] :
( m2_filter_2(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2953]) ).
fof(f6249,plain,
! [X0] :
( m2_filter_2(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f6248]) ).
fof(f6254,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( r2_hidden(X1,k18_filter_2(X0,X2))
<=> r3_lattices(X0,X1,X2) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2956]) ).
fof(f6255,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( r2_hidden(X1,k18_filter_2(X0,X2))
<=> r3_lattices(X0,X1,X2) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f6254]) ).
fof(f6342,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( r2_hidden(X3,k22_filter_2(X0,X1,X2))
<=> ( r3_lattices(X0,X1,X3)
& r3_lattices(X0,X3,X2) ) )
| ~ r3_lattices(X0,X1,X2)
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f3000]) ).
fof(f6343,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( r2_hidden(X3,k22_filter_2(X0,X1,X2))
<=> ( r3_lattices(X0,X1,X3)
& r3_lattices(X0,X3,X2) ) )
| ~ r3_lattices(X0,X1,X2)
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f6342]) ).
fof(f6350,plain,
? [X0] :
( ? [X1] :
( ~ r1_filter_2(u1_struct_0(X0),k18_filter_2(X0,X1),k22_filter_2(X0,k5_lattices(X0),X1))
& v13_lattices(X0)
& m1_subset_1(X1,u1_struct_0(X0)) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(ennf_transformation,[],[f3005]) ).
fof(f6351,plain,
? [X0] :
( ? [X1] :
( ~ r1_filter_2(u1_struct_0(X0),k18_filter_2(X0,X1),k22_filter_2(X0,k5_lattices(X0),X1))
& v13_lattices(X0)
& m1_subset_1(X1,u1_struct_0(X0)) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(flattening,[],[f6350]) ).
fof(f6563,plain,
! [X0,X1] :
( ( r1_tarski(X0,X1)
| ? [X2] :
( ~ r2_hidden(X2,X1)
& r2_hidden(X2,X0) ) )
& ( ! [X2] :
( r2_hidden(X2,X1)
| ~ r2_hidden(X2,X0) )
| ~ r1_tarski(X0,X1) ) ),
inference(nnf_transformation,[],[f3097]) ).
fof(f6564,plain,
! [X0,X1] :
( ( r1_tarski(X0,X1)
| ? [X2] :
( ~ r2_hidden(X2,X1)
& r2_hidden(X2,X0) ) )
& ( ! [X3] :
( r2_hidden(X3,X1)
| ~ r2_hidden(X3,X0) )
| ~ r1_tarski(X0,X1) ) ),
inference(rectify,[],[f6563]) ).
fof(f6565,plain,
! [X0,X1] :
( ( r1_tarski(X0,X1)
| ( ~ r2_hidden(sK130(X0,X1),X1)
& r2_hidden(sK130(X0,X1),X0) ) )
& ( ! [X3] :
( r2_hidden(X3,X1)
| ~ r2_hidden(X3,X0) )
| ~ r1_tarski(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK130]),skolemize(X2,sK130(X0,X1))],[f6564]) ).
fof(f6601,plain,
! [X0,X1] :
( ( X0 = X1
| ~ r1_tarski(X0,X1)
| ~ r1_tarski(X1,X0) )
& ( ( r1_tarski(X0,X1)
& r1_tarski(X1,X0) )
| X0 != X1 ) ),
inference(nnf_transformation,[],[f38]) ).
fof(f6602,plain,
! [X0,X1] :
( ( X0 = X1
| ~ r1_tarski(X0,X1)
| ~ r1_tarski(X1,X0) )
& ( ( r1_tarski(X0,X1)
& r1_tarski(X1,X0) )
| X0 != X1 ) ),
inference(flattening,[],[f6601]) ).
fof(f8061,plain,
! [X0,X1,X2] :
( ( ( r1_filter_2(X0,X1,X2)
| X1 != X2 )
& ( X1 = X2
| ~ r1_filter_2(X0,X1,X2) ) )
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(nnf_transformation,[],[f6102]) ).
fof(f8088,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( r2_hidden(X1,k18_filter_2(X0,X2))
| ~ r3_lattices(X0,X1,X2) )
& ( r3_lattices(X0,X1,X2)
| ~ r2_hidden(X1,k18_filter_2(X0,X2)) ) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f6255]) ).
fof(f8121,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( ( r2_hidden(X3,k22_filter_2(X0,X1,X2))
| ~ r3_lattices(X0,X1,X3)
| ~ r3_lattices(X0,X3,X2) )
& ( ( r3_lattices(X0,X1,X3)
& r3_lattices(X0,X3,X2) )
| ~ r2_hidden(X3,k22_filter_2(X0,X1,X2)) ) )
| ~ r3_lattices(X0,X1,X2)
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f6343]) ).
fof(f8122,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( ( r2_hidden(X3,k22_filter_2(X0,X1,X2))
| ~ r3_lattices(X0,X1,X3)
| ~ r3_lattices(X0,X3,X2) )
& ( ( r3_lattices(X0,X1,X3)
& r3_lattices(X0,X3,X2) )
| ~ r2_hidden(X3,k22_filter_2(X0,X1,X2)) ) )
| ~ r3_lattices(X0,X1,X2)
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f8121]) ).
fof(f8123,plain,
( ~ r1_filter_2(u1_struct_0(sK1080),k18_filter_2(sK1080,sK1081),k22_filter_2(sK1080,k5_lattices(sK1080),sK1081))
& v13_lattices(sK1080)
& m1_subset_1(sK1081,u1_struct_0(sK1080))
& ~ v3_struct_0(sK1080)
& v10_lattices(sK1080)
& l3_lattices(sK1080) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1080,sK1081]),skolemize(X0,sK1080),skolemize(X1,sK1081)],[f6351]) ).
fof(f8138,plain,
! [X0,X1] :
( r2_hidden(sK130(X0,X1),X0)
| r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f6565]) ).
fof(f8139,plain,
! [X0,X1] :
( ~ r2_hidden(sK130(X0,X1),X1)
| r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f6565]) ).
fof(f8206,plain,
! [X0,X1] :
( ~ r1_tarski(X1,X0)
| ~ r1_tarski(X0,X1)
| X0 = X1 ),
inference(cnf_transformation,[],[f6602]) ).
fof(f8912,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ r2_hidden(X0,X1)
| m1_subset_1(X0,X2) ),
inference(cnf_transformation,[],[f3435]) ).
fof(f12473,plain,
! [X0,X1] :
( r3_lattices(X0,k5_lattices(X0),X1)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v13_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f5395]) ).
fof(f12492,plain,
! [X0] :
( ~ l3_lattices(X0)
| l1_lattices(X0) ),
inference(cnf_transformation,[],[f5420]) ).
fof(f12508,plain,
! [X0] :
( m1_subset_1(k5_lattices(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_lattices(X0) ),
inference(cnf_transformation,[],[f5448]) ).
fof(f13349,plain,
! [X0,X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f6060]) ).
fof(f13382,plain,
! [X0,X1] :
( ~ m2_filter_2(X1,X0)
| m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f6094]) ).
fof(f13383,plain,
! [X0,X1] :
( ~ m2_filter_2(X1,X0)
| ~ v1_xboole_0(X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f6094]) ).
fof(f13388,plain,
! [X2,X0,X1] :
( r1_filter_2(X0,X1,X2)
| X1 != X2
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f8061]) ).
fof(f13420,plain,
! [X0,X1] :
( m2_filter_2(k18_filter_2(X0,X1),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f6162]) ).
fof(f13425,plain,
! [X2,X0,X1] :
( m2_lattice4(k22_filter_2(X0,X1,X2),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f6172]) ).
fof(f13519,plain,
! [X0] :
( m2_filter_2(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f6249]) ).
fof(f13522,plain,
! [X2,X0,X1] :
( ~ r2_hidden(X1,k18_filter_2(X0,X2))
| r3_lattices(X0,X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f8088]) ).
fof(f13523,plain,
! [X2,X0,X1] :
( r2_hidden(X1,k18_filter_2(X0,X2))
| ~ r3_lattices(X0,X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f8088]) ).
fof(f13667,plain,
! [X2,X3,X0,X1] :
( ~ r2_hidden(X3,k22_filter_2(X0,X1,X2))
| r3_lattices(X0,X3,X2)
| ~ r3_lattices(X0,X1,X2)
| ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f8122]) ).
fof(f13669,plain,
! [X2,X3,X0,X1] :
( r2_hidden(X3,k22_filter_2(X0,X1,X2))
| ~ r3_lattices(X0,X1,X3)
| ~ r3_lattices(X0,X3,X2)
| ~ r3_lattices(X0,X1,X2)
| ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f8122]) ).
fof(f13674,plain,
l3_lattices(sK1080),
inference(cnf_transformation,[],[f8123]) ).
fof(f13675,plain,
v10_lattices(sK1080),
inference(cnf_transformation,[],[f8123]) ).
fof(f13676,plain,
~ v3_struct_0(sK1080),
inference(cnf_transformation,[],[f8123]) ).
fof(f13677,plain,
m1_subset_1(sK1081,u1_struct_0(sK1080)),
inference(cnf_transformation,[],[f8123]) ).
fof(f13678,plain,
v13_lattices(sK1080),
inference(cnf_transformation,[],[f8123]) ).
fof(f13679,plain,
~ r1_filter_2(u1_struct_0(sK1080),k18_filter_2(sK1080,sK1081),k22_filter_2(sK1080,k5_lattices(sK1080),sK1081)),
inference(cnf_transformation,[],[f8123]) ).
fof(f15569,plain,
! [X2,X0] :
( r1_filter_2(X0,X2,X2)
| v1_xboole_0(X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(equality_resolution,[],[f13388]) ).
fof(f15619,definition,
sF1082 = u1_struct_0(sK1080),
introduced(definition,[new_symbols(definition,[sF1082])],[function_definition]) ).
fof(f15620,plain,
u1_struct_0(sK1080) = sF1082,
inference(reorient_equations,[],[f15619]) ).
fof(f15621,definition,
sF1083 = k18_filter_2(sK1080,sK1081),
introduced(definition,[new_symbols(definition,[sF1083])],[function_definition]) ).
fof(f15622,plain,
k18_filter_2(sK1080,sK1081) = sF1083,
inference(reorient_equations,[],[f15621]) ).
fof(f15623,definition,
sF1084 = k5_lattices(sK1080),
introduced(definition,[new_symbols(definition,[sF1084])],[function_definition]) ).
fof(f15624,plain,
k5_lattices(sK1080) = sF1084,
inference(reorient_equations,[],[f15623]) ).
fof(f15625,definition,
sF1085 = k22_filter_2(sK1080,sF1084,sK1081),
introduced(definition,[new_symbols(definition,[sF1085])],[function_definition]) ).
fof(f15626,plain,
k22_filter_2(sK1080,sF1084,sK1081) = sF1085,
inference(reorient_equations,[],[f15625]) ).
fof(f15627,plain,
~ r1_filter_2(sF1082,sF1083,sF1085),
inference(definition_folding,[],[f13679,f15626,f15624,f15622,f15620]) ).
fof(f15628,plain,
m1_subset_1(sK1081,sF1082),
inference(definition_folding,[],[f13677,f15620]) ).
fof(f15636,plain,
! [X2,X0] :
( ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| v1_xboole_0(X0)
| r1_filter_2(X0,X2,X2) ),
inference(duplicate_literal_removal,[],[f15569]) ).
fof(f18171,plain,
( m2_filter_2(sF1083,sK1080)
| v3_struct_0(sK1080)
| ~ v10_lattices(sK1080)
| ~ l3_lattices(sK1080)
| ~ m1_subset_1(sK1081,u1_struct_0(sK1080)) ),
inference(superposition,[],[f13420,f15622]) ).
fof(f18172,plain,
( m2_filter_2(sF1083,sK1080)
| ~ v10_lattices(sK1080)
| ~ l3_lattices(sK1080)
| ~ m1_subset_1(sK1081,u1_struct_0(sK1080)) ),
inference(forward_subsumption_resolution,[],[f18171,f13676]) ).
fof(f18173,plain,
( m2_filter_2(sF1083,sK1080)
| ~ l3_lattices(sK1080)
| ~ m1_subset_1(sK1081,u1_struct_0(sK1080)) ),
inference(forward_subsumption_resolution,[],[f18172,f13675]) ).
fof(f18174,plain,
( m2_filter_2(sF1083,sK1080)
| ~ m1_subset_1(sK1081,u1_struct_0(sK1080)) ),
inference(forward_subsumption_resolution,[],[f18173,f13674]) ).
fof(f18175,plain,
( ~ m1_subset_1(sK1081,sF1082)
| m2_filter_2(sF1083,sK1080) ),
inference(forward_demodulation,[],[f18174,f15620]) ).
fof(f18176,plain,
m2_filter_2(sF1083,sK1080),
inference(forward_subsumption_resolution,[],[f18175,f15628]) ).
fof(f18228,plain,
! [X0] :
( ~ r2_hidden(X0,sF1083)
| r3_lattices(sK1080,X0,sK1081)
| ~ m1_subset_1(sK1081,u1_struct_0(sK1080))
| ~ m1_subset_1(X0,u1_struct_0(sK1080))
| v3_struct_0(sK1080)
| ~ v10_lattices(sK1080)
| ~ l3_lattices(sK1080) ),
inference(superposition,[],[f13522,f15622]) ).
fof(f18230,plain,
! [X0] :
( ~ r2_hidden(X0,sF1083)
| r3_lattices(sK1080,X0,sK1081)
| ~ m1_subset_1(sK1081,u1_struct_0(sK1080))
| ~ m1_subset_1(X0,u1_struct_0(sK1080))
| ~ v10_lattices(sK1080)
| ~ l3_lattices(sK1080) ),
inference(forward_subsumption_resolution,[],[f18228,f13676]) ).
fof(f18232,plain,
! [X0] :
( ~ r2_hidden(X0,sF1083)
| r3_lattices(sK1080,X0,sK1081)
| ~ m1_subset_1(sK1081,u1_struct_0(sK1080))
| ~ m1_subset_1(X0,u1_struct_0(sK1080))
| ~ l3_lattices(sK1080) ),
inference(forward_subsumption_resolution,[],[f18230,f13675]) ).
fof(f18234,plain,
! [X0] :
( ~ r2_hidden(X0,sF1083)
| r3_lattices(sK1080,X0,sK1081)
| ~ m1_subset_1(sK1081,u1_struct_0(sK1080))
| ~ m1_subset_1(X0,u1_struct_0(sK1080)) ),
inference(forward_subsumption_resolution,[],[f18232,f13674]) ).
fof(f18236,plain,
! [X0] :
( ~ m1_subset_1(sK1081,sF1082)
| ~ r2_hidden(X0,sF1083)
| r3_lattices(sK1080,X0,sK1081)
| ~ m1_subset_1(X0,u1_struct_0(sK1080)) ),
inference(forward_demodulation,[],[f18234,f15620]) ).
fof(f18239,plain,
! [X0] :
( ~ r2_hidden(X0,sF1083)
| r3_lattices(sK1080,X0,sK1081)
| ~ m1_subset_1(X0,u1_struct_0(sK1080)) ),
inference(forward_subsumption_resolution,[],[f18236,f15628]) ).
fof(f18240,plain,
! [X0] :
( r3_lattices(sK1080,X0,sK1081)
| ~ r2_hidden(X0,sF1083)
| ~ m1_subset_1(X0,sF1082) ),
inference(forward_demodulation,[],[f18239,f15620]) ).
fof(f18278,plain,
! [X0] :
( r2_hidden(X0,sF1083)
| ~ r3_lattices(sK1080,X0,sK1081)
| ~ m1_subset_1(sK1081,u1_struct_0(sK1080))
| ~ m1_subset_1(X0,u1_struct_0(sK1080))
| v3_struct_0(sK1080)
| ~ v10_lattices(sK1080)
| ~ l3_lattices(sK1080) ),
inference(superposition,[],[f13523,f15622]) ).
fof(f18280,plain,
! [X0] :
( r2_hidden(X0,sF1083)
| ~ r3_lattices(sK1080,X0,sK1081)
| ~ m1_subset_1(sK1081,u1_struct_0(sK1080))
| ~ m1_subset_1(X0,u1_struct_0(sK1080))
| ~ v10_lattices(sK1080)
| ~ l3_lattices(sK1080) ),
inference(forward_subsumption_resolution,[],[f18278,f13676]) ).
fof(f18281,plain,
! [X0] :
( r2_hidden(X0,sF1083)
| ~ r3_lattices(sK1080,X0,sK1081)
| ~ m1_subset_1(sK1081,u1_struct_0(sK1080))
| ~ m1_subset_1(X0,u1_struct_0(sK1080))
| ~ l3_lattices(sK1080) ),
inference(forward_subsumption_resolution,[],[f18280,f13675]) ).
fof(f18282,plain,
! [X0] :
( r2_hidden(X0,sF1083)
| ~ r3_lattices(sK1080,X0,sK1081)
| ~ m1_subset_1(sK1081,u1_struct_0(sK1080))
| ~ m1_subset_1(X0,u1_struct_0(sK1080)) ),
inference(forward_subsumption_resolution,[],[f18281,f13674]) ).
fof(f18283,plain,
! [X0] :
( ~ m1_subset_1(sK1081,sF1082)
| r2_hidden(X0,sF1083)
| ~ r3_lattices(sK1080,X0,sK1081)
| ~ m1_subset_1(X0,u1_struct_0(sK1080)) ),
inference(forward_demodulation,[],[f18282,f15620]) ).
fof(f18284,plain,
! [X0] :
( r2_hidden(X0,sF1083)
| ~ r3_lattices(sK1080,X0,sK1081)
| ~ m1_subset_1(X0,u1_struct_0(sK1080)) ),
inference(forward_subsumption_resolution,[],[f18283,f15628]) ).
fof(f18285,plain,
! [X0] :
( ~ r3_lattices(sK1080,X0,sK1081)
| r2_hidden(X0,sF1083)
| ~ m1_subset_1(X0,sF1082) ),
inference(forward_demodulation,[],[f18284,f15620]) ).
fof(f18291,plain,
! [X0] :
( m1_subset_1(X0,k1_zfmisc_1(sF1082))
| ~ m2_lattice4(X0,sK1080)
| v3_struct_0(sK1080)
| ~ v10_lattices(sK1080)
| ~ l3_lattices(sK1080) ),
inference(superposition,[],[f13349,f15620]) ).
fof(f18293,plain,
! [X0] :
( m1_subset_1(X0,k1_zfmisc_1(sF1082))
| ~ m2_lattice4(X0,sK1080)
| ~ v10_lattices(sK1080)
| ~ l3_lattices(sK1080) ),
inference(forward_subsumption_resolution,[],[f18291,f13676]) ).
fof(f18294,plain,
! [X0] :
( m1_subset_1(X0,k1_zfmisc_1(sF1082))
| ~ m2_lattice4(X0,sK1080)
| ~ l3_lattices(sK1080) ),
inference(forward_subsumption_resolution,[],[f18293,f13675]) ).
fof(f18295,plain,
! [X0] :
( m1_subset_1(X0,k1_zfmisc_1(sF1082))
| ~ m2_lattice4(X0,sK1080) ),
inference(forward_subsumption_resolution,[],[f18294,f13674]) ).
fof(f18296,plain,
! [X0] :
( ~ m2_lattice4(X0,sK1080)
| v1_xboole_0(sF1082)
| r1_filter_2(sF1082,X0,X0) ),
inference(resolution,[],[f18295,f15636]) ).
fof(f18298,plain,
( m2_filter_2(sF1082,sK1080)
| v3_struct_0(sK1080)
| ~ v10_lattices(sK1080)
| ~ l3_lattices(sK1080) ),
inference(superposition,[],[f13519,f15620]) ).
fof(f18300,plain,
( m2_filter_2(sF1082,sK1080)
| ~ v10_lattices(sK1080)
| ~ l3_lattices(sK1080) ),
inference(forward_subsumption_resolution,[],[f18298,f13676]) ).
fof(f18302,plain,
( m2_filter_2(sF1082,sK1080)
| ~ l3_lattices(sK1080) ),
inference(forward_subsumption_resolution,[],[f18300,f13675]) ).
fof(f18304,plain,
m2_filter_2(sF1082,sK1080),
inference(forward_subsumption_resolution,[],[f18302,f13674]) ).
fof(f18309,plain,
! [X0] :
( r3_lattices(sK1080,sF1084,X0)
| ~ m1_subset_1(X0,u1_struct_0(sK1080))
| v3_struct_0(sK1080)
| ~ v10_lattices(sK1080)
| ~ v13_lattices(sK1080)
| ~ l3_lattices(sK1080) ),
inference(superposition,[],[f12473,f15624]) ).
fof(f18310,plain,
! [X0] :
( r3_lattices(sK1080,sF1084,X0)
| ~ m1_subset_1(X0,u1_struct_0(sK1080))
| ~ v10_lattices(sK1080)
| ~ v13_lattices(sK1080)
| ~ l3_lattices(sK1080) ),
inference(forward_subsumption_resolution,[],[f18309,f13676]) ).
fof(f18312,plain,
! [X0] :
( r3_lattices(sK1080,sF1084,X0)
| ~ m1_subset_1(X0,u1_struct_0(sK1080))
| ~ v13_lattices(sK1080)
| ~ l3_lattices(sK1080) ),
inference(forward_subsumption_resolution,[],[f18310,f13675]) ).
fof(f18314,plain,
! [X0] :
( r3_lattices(sK1080,sF1084,X0)
| ~ m1_subset_1(X0,u1_struct_0(sK1080))
| ~ l3_lattices(sK1080) ),
inference(forward_subsumption_resolution,[],[f18312,f13678]) ).
fof(f18316,plain,
! [X0] :
( r3_lattices(sK1080,sF1084,X0)
| ~ m1_subset_1(X0,u1_struct_0(sK1080)) ),
inference(forward_subsumption_resolution,[],[f18314,f13674]) ).
fof(f18318,plain,
! [X0] :
( r3_lattices(sK1080,sF1084,X0)
| ~ m1_subset_1(X0,sF1082) ),
inference(forward_demodulation,[],[f18316,f15620]) ).
fof(f18323,plain,
( m2_lattice4(sF1085,sK1080)
| v3_struct_0(sK1080)
| ~ v10_lattices(sK1080)
| ~ l3_lattices(sK1080)
| ~ m1_subset_1(sF1084,u1_struct_0(sK1080))
| ~ m1_subset_1(sK1081,u1_struct_0(sK1080)) ),
inference(superposition,[],[f13425,f15626]) ).
fof(f18324,plain,
( m2_lattice4(sF1085,sK1080)
| ~ v10_lattices(sK1080)
| ~ l3_lattices(sK1080)
| ~ m1_subset_1(sF1084,u1_struct_0(sK1080))
| ~ m1_subset_1(sK1081,u1_struct_0(sK1080)) ),
inference(forward_subsumption_resolution,[],[f18323,f13676]) ).
fof(f18325,plain,
( m2_lattice4(sF1085,sK1080)
| ~ l3_lattices(sK1080)
| ~ m1_subset_1(sF1084,u1_struct_0(sK1080))
| ~ m1_subset_1(sK1081,u1_struct_0(sK1080)) ),
inference(forward_subsumption_resolution,[],[f18324,f13675]) ).
fof(f18326,plain,
( m2_lattice4(sF1085,sK1080)
| ~ m1_subset_1(sF1084,u1_struct_0(sK1080))
| ~ m1_subset_1(sK1081,u1_struct_0(sK1080)) ),
inference(forward_subsumption_resolution,[],[f18325,f13674]) ).
fof(f18327,plain,
( ~ m1_subset_1(sF1084,sF1082)
| m2_lattice4(sF1085,sK1080)
| ~ m1_subset_1(sK1081,u1_struct_0(sK1080)) ),
inference(forward_demodulation,[],[f18326,f15620]) ).
fof(f18328,plain,
( ~ m1_subset_1(sK1081,sF1082)
| ~ m1_subset_1(sF1084,sF1082)
| m2_lattice4(sF1085,sK1080) ),
inference(forward_demodulation,[],[f18327,f15620]) ).
fof(f18329,plain,
( ~ m1_subset_1(sF1084,sF1082)
| m2_lattice4(sF1085,sK1080) ),
inference(forward_subsumption_resolution,[],[f18328,f15628]) ).
fof(f18331,definition,
( spl1086_348
<=> m2_lattice4(sF1085,sK1080) ),
introduced(definition,[new_symbols(definition,[spl1086_348])],[avatar_definition]) ).
fof(f18333,plain,
( m2_lattice4(sF1085,sK1080)
| ~ spl1086_348 ),
inference(avatar_component_clause,[],[f18331]) ).
fof(f18335,definition,
( spl1086_349
<=> m1_subset_1(sF1084,sF1082) ),
introduced(definition,[new_symbols(definition,[spl1086_349])],[avatar_definition]) ).
fof(f18336,plain,
( m1_subset_1(sF1084,sF1082)
| ~ spl1086_349 ),
inference(avatar_component_clause,[],[f18335]) ).
fof(f18337,plain,
( ~ m1_subset_1(sF1084,sF1082)
| spl1086_349 ),
inference(avatar_component_clause,[],[f18335]) ).
fof(f18338,plain,
( spl1086_348
| ~ spl1086_349 ),
inference(avatar_split_clause,[],[f18329,f18335,f18331]) ).
fof(f18371,definition,
( spl1086_352
<=> r1_tarski(sF1083,sF1085) ),
introduced(definition,[new_symbols(definition,[spl1086_352])],[avatar_definition]) ).
fof(f18372,plain,
( r1_tarski(sF1083,sF1085)
| ~ spl1086_352 ),
inference(avatar_component_clause,[],[f18371]) ).
fof(f18435,plain,
( m2_lattice4(sF1083,sK1080)
| v3_struct_0(sK1080)
| ~ v10_lattices(sK1080)
| ~ l3_lattices(sK1080) ),
inference(resolution,[],[f13382,f18176]) ).
fof(f18438,plain,
( m2_lattice4(sF1083,sK1080)
| ~ v10_lattices(sK1080)
| ~ l3_lattices(sK1080) ),
inference(forward_subsumption_resolution,[],[f18435,f13676]) ).
fof(f18439,plain,
( m2_lattice4(sF1083,sK1080)
| ~ l3_lattices(sK1080) ),
inference(forward_subsumption_resolution,[],[f18438,f13675]) ).
fof(f18440,plain,
m2_lattice4(sF1083,sK1080),
inference(forward_subsumption_resolution,[],[f18439,f13674]) ).
fof(f18441,plain,
! [X0] :
( r2_hidden(X0,sF1085)
| ~ r3_lattices(sK1080,sF1084,X0)
| ~ r3_lattices(sK1080,X0,sK1081)
| ~ r3_lattices(sK1080,sF1084,sK1081)
| ~ m1_subset_1(X0,u1_struct_0(sK1080))
| ~ m1_subset_1(sK1081,u1_struct_0(sK1080))
| ~ m1_subset_1(sF1084,u1_struct_0(sK1080))
| v3_struct_0(sK1080)
| ~ v10_lattices(sK1080)
| ~ l3_lattices(sK1080) ),
inference(superposition,[],[f13669,f15626]) ).
fof(f18442,plain,
! [X0] :
( r2_hidden(X0,sF1085)
| ~ r3_lattices(sK1080,sF1084,X0)
| ~ r3_lattices(sK1080,X0,sK1081)
| ~ r3_lattices(sK1080,sF1084,sK1081)
| ~ m1_subset_1(X0,u1_struct_0(sK1080))
| ~ m1_subset_1(sK1081,u1_struct_0(sK1080))
| ~ m1_subset_1(sF1084,u1_struct_0(sK1080))
| ~ v10_lattices(sK1080)
| ~ l3_lattices(sK1080) ),
inference(forward_subsumption_resolution,[],[f18441,f13676]) ).
fof(f18443,plain,
! [X0] :
( r2_hidden(X0,sF1085)
| ~ r3_lattices(sK1080,sF1084,X0)
| ~ r3_lattices(sK1080,X0,sK1081)
| ~ r3_lattices(sK1080,sF1084,sK1081)
| ~ m1_subset_1(X0,u1_struct_0(sK1080))
| ~ m1_subset_1(sK1081,u1_struct_0(sK1080))
| ~ m1_subset_1(sF1084,u1_struct_0(sK1080))
| ~ l3_lattices(sK1080) ),
inference(forward_subsumption_resolution,[],[f18442,f13675]) ).
fof(f18444,plain,
! [X0] :
( r2_hidden(X0,sF1085)
| ~ r3_lattices(sK1080,sF1084,X0)
| ~ r3_lattices(sK1080,X0,sK1081)
| ~ r3_lattices(sK1080,sF1084,sK1081)
| ~ m1_subset_1(X0,u1_struct_0(sK1080))
| ~ m1_subset_1(sK1081,u1_struct_0(sK1080))
| ~ m1_subset_1(sF1084,u1_struct_0(sK1080)) ),
inference(forward_subsumption_resolution,[],[f18443,f13674]) ).
fof(f18445,plain,
! [X0] :
( ~ m1_subset_1(X0,sF1082)
| r2_hidden(X0,sF1085)
| ~ r3_lattices(sK1080,sF1084,X0)
| ~ r3_lattices(sK1080,X0,sK1081)
| ~ r3_lattices(sK1080,sF1084,sK1081)
| ~ m1_subset_1(sK1081,u1_struct_0(sK1080))
| ~ m1_subset_1(sF1084,u1_struct_0(sK1080)) ),
inference(forward_demodulation,[],[f18444,f15620]) ).
fof(f18446,plain,
! [X0] :
( ~ m1_subset_1(X0,sF1082)
| r2_hidden(X0,sF1085)
| ~ r3_lattices(sK1080,X0,sK1081)
| ~ r3_lattices(sK1080,sF1084,sK1081)
| ~ m1_subset_1(sK1081,u1_struct_0(sK1080))
| ~ m1_subset_1(sF1084,u1_struct_0(sK1080)) ),
inference(forward_subsumption_resolution,[],[f18445,f18318]) ).
fof(f18447,plain,
! [X0] :
( ~ m1_subset_1(sK1081,sF1082)
| ~ m1_subset_1(X0,sF1082)
| r2_hidden(X0,sF1085)
| ~ r3_lattices(sK1080,X0,sK1081)
| ~ r3_lattices(sK1080,sF1084,sK1081)
| ~ m1_subset_1(sF1084,u1_struct_0(sK1080)) ),
inference(forward_demodulation,[],[f18446,f15620]) ).
fof(f18448,plain,
! [X0] :
( ~ m1_subset_1(sK1081,sF1082)
| ~ m1_subset_1(X0,sF1082)
| r2_hidden(X0,sF1085)
| ~ r3_lattices(sK1080,X0,sK1081)
| ~ m1_subset_1(sF1084,u1_struct_0(sK1080)) ),
inference(forward_subsumption_resolution,[],[f18447,f18318]) ).
fof(f18449,plain,
! [X0] :
( ~ m1_subset_1(X0,sF1082)
| r2_hidden(X0,sF1085)
| ~ r3_lattices(sK1080,X0,sK1081)
| ~ m1_subset_1(sF1084,u1_struct_0(sK1080)) ),
inference(forward_subsumption_resolution,[],[f18448,f15628]) ).
fof(f18450,plain,
! [X0] :
( ~ m1_subset_1(sF1084,sF1082)
| ~ m1_subset_1(X0,sF1082)
| r2_hidden(X0,sF1085)
| ~ r3_lattices(sK1080,X0,sK1081) ),
inference(forward_demodulation,[],[f18449,f15620]) ).
fof(f18485,plain,
! [X0] :
( ~ r2_hidden(X0,sF1085)
| r3_lattices(sK1080,X0,sK1081)
| ~ r3_lattices(sK1080,sF1084,sK1081)
| ~ m1_subset_1(X0,u1_struct_0(sK1080))
| ~ m1_subset_1(sK1081,u1_struct_0(sK1080))
| ~ m1_subset_1(sF1084,u1_struct_0(sK1080))
| v3_struct_0(sK1080)
| ~ v10_lattices(sK1080)
| ~ l3_lattices(sK1080) ),
inference(superposition,[],[f13667,f15626]) ).
fof(f18489,plain,
! [X0] :
( ~ r2_hidden(X0,sF1085)
| r3_lattices(sK1080,X0,sK1081)
| ~ r3_lattices(sK1080,sF1084,sK1081)
| ~ m1_subset_1(X0,u1_struct_0(sK1080))
| ~ m1_subset_1(sK1081,u1_struct_0(sK1080))
| ~ m1_subset_1(sF1084,u1_struct_0(sK1080))
| ~ v10_lattices(sK1080)
| ~ l3_lattices(sK1080) ),
inference(forward_subsumption_resolution,[],[f18485,f13676]) ).
fof(f18490,plain,
! [X0] :
( ~ r2_hidden(X0,sF1085)
| r3_lattices(sK1080,X0,sK1081)
| ~ r3_lattices(sK1080,sF1084,sK1081)
| ~ m1_subset_1(X0,u1_struct_0(sK1080))
| ~ m1_subset_1(sK1081,u1_struct_0(sK1080))
| ~ m1_subset_1(sF1084,u1_struct_0(sK1080))
| ~ l3_lattices(sK1080) ),
inference(forward_subsumption_resolution,[],[f18489,f13675]) ).
fof(f18491,plain,
! [X0] :
( ~ r2_hidden(X0,sF1085)
| r3_lattices(sK1080,X0,sK1081)
| ~ r3_lattices(sK1080,sF1084,sK1081)
| ~ m1_subset_1(X0,u1_struct_0(sK1080))
| ~ m1_subset_1(sK1081,u1_struct_0(sK1080))
| ~ m1_subset_1(sF1084,u1_struct_0(sK1080)) ),
inference(forward_subsumption_resolution,[],[f18490,f13674]) ).
fof(f18492,plain,
! [X0] :
( ~ m1_subset_1(X0,sF1082)
| ~ r2_hidden(X0,sF1085)
| r3_lattices(sK1080,X0,sK1081)
| ~ r3_lattices(sK1080,sF1084,sK1081)
| ~ m1_subset_1(sK1081,u1_struct_0(sK1080))
| ~ m1_subset_1(sF1084,u1_struct_0(sK1080)) ),
inference(forward_demodulation,[],[f18491,f15620]) ).
fof(f18493,plain,
! [X0] :
( ~ m1_subset_1(sK1081,sF1082)
| ~ m1_subset_1(X0,sF1082)
| ~ r2_hidden(X0,sF1085)
| r3_lattices(sK1080,X0,sK1081)
| ~ r3_lattices(sK1080,sF1084,sK1081)
| ~ m1_subset_1(sF1084,u1_struct_0(sK1080)) ),
inference(forward_demodulation,[],[f18492,f15620]) ).
fof(f18494,plain,
! [X0] :
( ~ m1_subset_1(sK1081,sF1082)
| ~ m1_subset_1(X0,sF1082)
| ~ r2_hidden(X0,sF1085)
| r3_lattices(sK1080,X0,sK1081)
| ~ m1_subset_1(sF1084,u1_struct_0(sK1080)) ),
inference(forward_subsumption_resolution,[],[f18493,f18318]) ).
fof(f18495,plain,
! [X0] :
( ~ m1_subset_1(X0,sF1082)
| ~ r2_hidden(X0,sF1085)
| r3_lattices(sK1080,X0,sK1081)
| ~ m1_subset_1(sF1084,u1_struct_0(sK1080)) ),
inference(forward_subsumption_resolution,[],[f18494,f15628]) ).
fof(f18496,plain,
! [X0] :
( ~ m1_subset_1(sF1084,sF1082)
| ~ m1_subset_1(X0,sF1082)
| ~ r2_hidden(X0,sF1085)
| r3_lattices(sK1080,X0,sK1081) ),
inference(forward_demodulation,[],[f18495,f15620]) ).
fof(f18514,plain,
( m1_subset_1(k5_lattices(sK1080),sF1082)
| v3_struct_0(sK1080)
| ~ l1_lattices(sK1080) ),
inference(superposition,[],[f12508,f15620]) ).
fof(f18521,plain,
( m1_subset_1(k5_lattices(sK1080),sF1082)
| ~ l1_lattices(sK1080) ),
inference(forward_subsumption_resolution,[],[f18514,f13676]) ).
fof(f18536,plain,
( m1_subset_1(sF1084,sF1082)
| ~ l1_lattices(sK1080) ),
inference(forward_demodulation,[],[f18521,f15624]) ).
fof(f18538,plain,
( ~ l1_lattices(sK1080)
| spl1086_349 ),
inference(forward_subsumption_resolution,[],[f18536,f18337]) ).
fof(f18555,plain,
( ~ v1_xboole_0(sF1082)
| v3_struct_0(sK1080)
| ~ v10_lattices(sK1080)
| ~ l3_lattices(sK1080) ),
inference(resolution,[],[f13383,f18304]) ).
fof(f18572,definition,
( spl1086_357
<=> v1_xboole_0(sF1082) ),
introduced(definition,[new_symbols(definition,[spl1086_357])],[avatar_definition]) ).
fof(f18582,definition,
( spl1086_359
<=> ! [X0] :
( ~ m2_lattice4(X0,sK1080)
| r1_filter_2(sF1082,X0,X0) ) ),
introduced(definition,[new_symbols(definition,[spl1086_359])],[avatar_definition]) ).
fof(f18583,plain,
( ! [X0] :
( r1_filter_2(sF1082,X0,X0)
| ~ m2_lattice4(X0,sK1080) )
| ~ spl1086_359 ),
inference(avatar_component_clause,[],[f18582]) ).
fof(f18584,plain,
( spl1086_357
| spl1086_359 ),
inference(avatar_split_clause,[],[f18296,f18582,f18572]) ).
fof(f18607,plain,
( ~ v1_xboole_0(sF1082)
| ~ v10_lattices(sK1080)
| ~ l3_lattices(sK1080) ),
inference(forward_subsumption_resolution,[],[f18555,f13676]) ).
fof(f18630,plain,
( ~ v1_xboole_0(sF1082)
| ~ l3_lattices(sK1080) ),
inference(forward_subsumption_resolution,[],[f18607,f13675]) ).
fof(f18634,plain,
~ v1_xboole_0(sF1082),
inference(forward_subsumption_resolution,[],[f18630,f13674]) ).
fof(f18636,plain,
~ spl1086_357,
inference(avatar_split_clause,[],[f18634,f18572]) ).
fof(f19026,plain,
l1_lattices(sK1080),
inference(resolution,[],[f12492,f13674]) ).
fof(f19031,plain,
( $false
| spl1086_349 ),
inference(forward_subsumption_resolution,[],[f19026,f18538]) ).
fof(f19032,plain,
spl1086_349,
inference(avatar_contradiction_clause,[],[f19031]) ).
fof(f19035,plain,
( ! [X0] :
( ~ r3_lattices(sK1080,X0,sK1081)
| r2_hidden(X0,sF1085)
| ~ m1_subset_1(X0,sF1082) )
| ~ spl1086_349 ),
inference(forward_subsumption_resolution,[],[f18450,f18336]) ).
fof(f19036,plain,
( ! [X0] :
( r3_lattices(sK1080,X0,sK1081)
| ~ r2_hidden(X0,sF1085)
| ~ m1_subset_1(X0,sF1082) )
| ~ spl1086_349 ),
inference(forward_subsumption_resolution,[],[f18496,f18336]) ).
fof(f19047,plain,
( ! [X0] :
( r2_hidden(X0,sF1085)
| ~ m1_subset_1(X0,sF1082)
| ~ r2_hidden(X0,sF1083)
| ~ m1_subset_1(X0,sF1082) )
| ~ spl1086_349 ),
inference(resolution,[],[f19035,f18240]) ).
fof(f19052,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF1082)
| r2_hidden(X0,sF1085)
| ~ r2_hidden(X0,sF1083) )
| ~ spl1086_349 ),
inference(duplicate_literal_removal,[],[f19047]) ).
fof(f19061,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF1085)
| ~ m1_subset_1(X0,sF1082)
| r2_hidden(X0,sF1083)
| ~ m1_subset_1(X0,sF1082) )
| ~ spl1086_349 ),
inference(resolution,[],[f19036,f18285]) ).
fof(f19062,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF1082)
| ~ r2_hidden(X0,sF1085)
| r2_hidden(X0,sF1083) )
| ~ spl1086_349 ),
inference(duplicate_literal_removal,[],[f19061]) ).
fof(f19313,plain,
! [X0,X1] :
( ~ m2_lattice4(X1,sK1080)
| m1_subset_1(X0,sF1082)
| ~ r2_hidden(X0,X1) ),
inference(resolution,[],[f8912,f18295]) ).
fof(f19319,plain,
! [X0] :
( ~ r2_hidden(X0,sF1083)
| m1_subset_1(X0,sF1082) ),
inference(resolution,[],[f19313,f18440]) ).
fof(f19320,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF1085)
| m1_subset_1(X0,sF1082) )
| ~ spl1086_348 ),
inference(resolution,[],[f19313,f18333]) ).
fof(f19438,plain,
! [X0] :
( m1_subset_1(sK130(sF1083,X0),sF1082)
| r1_tarski(sF1083,X0) ),
inference(resolution,[],[f8138,f19319]) ).
fof(f19439,plain,
( ! [X0] :
( m1_subset_1(sK130(sF1085,X0),sF1082)
| r1_tarski(sF1085,X0) )
| ~ spl1086_348 ),
inference(resolution,[],[f8138,f19320]) ).
fof(f19445,plain,
( ! [X0] :
( r1_tarski(sF1083,X0)
| r2_hidden(sK130(sF1083,X0),sF1085)
| ~ r2_hidden(sK130(sF1083,X0),sF1083) )
| ~ spl1086_349 ),
inference(resolution,[],[f19438,f19052]) ).
fof(f19450,plain,
( ! [X0] :
( r2_hidden(sK130(sF1083,X0),sF1085)
| r1_tarski(sF1083,X0) )
| ~ spl1086_349 ),
inference(forward_subsumption_resolution,[],[f19445,f8138]) ).
fof(f19458,plain,
( ! [X0] :
( r1_tarski(sF1085,X0)
| ~ r2_hidden(sK130(sF1085,X0),sF1085)
| r2_hidden(sK130(sF1085,X0),sF1083) )
| ~ spl1086_348
| ~ spl1086_349 ),
inference(resolution,[],[f19439,f19062]) ).
fof(f19462,plain,
( ! [X0] :
( r2_hidden(sK130(sF1085,X0),sF1083)
| r1_tarski(sF1085,X0) )
| ~ spl1086_348
| ~ spl1086_349 ),
inference(forward_subsumption_resolution,[],[f19458,f8138]) ).
fof(f19824,plain,
( r1_tarski(sF1085,sF1083)
| r1_tarski(sF1085,sF1083)
| ~ spl1086_348
| ~ spl1086_349 ),
inference(resolution,[],[f8139,f19462]) ).
fof(f19825,plain,
( r1_tarski(sF1083,sF1085)
| r1_tarski(sF1083,sF1085)
| ~ spl1086_349 ),
inference(resolution,[],[f8139,f19450]) ).
fof(f19829,plain,
( r1_tarski(sF1083,sF1085)
| ~ spl1086_349 ),
inference(duplicate_literal_removal,[],[f19825]) ).
fof(f19830,plain,
( r1_tarski(sF1085,sF1083)
| ~ spl1086_348
| ~ spl1086_349 ),
inference(duplicate_literal_removal,[],[f19824]) ).
fof(f19834,plain,
( spl1086_352
| ~ spl1086_349 ),
inference(avatar_split_clause,[],[f19829,f18335,f18371]) ).
fof(f19837,plain,
( ~ r1_tarski(sF1085,sF1083)
| sF1083 = sF1085
| ~ spl1086_352 ),
inference(resolution,[],[f18372,f8206]) ).
fof(f19838,plain,
( sF1083 = sF1085
| ~ spl1086_348
| ~ spl1086_349
| ~ spl1086_352 ),
inference(forward_subsumption_resolution,[],[f19837,f19830]) ).
fof(f19843,plain,
( ~ r1_filter_2(sF1082,sF1083,sF1083)
| ~ spl1086_348
| ~ spl1086_349
| ~ spl1086_352 ),
inference(superposition,[],[f15627,f19838]) ).
fof(f19864,plain,
( ~ m2_lattice4(sF1083,sK1080)
| ~ spl1086_348
| ~ spl1086_349
| ~ spl1086_352
| ~ spl1086_359 ),
inference(resolution,[],[f19843,f18583]) ).
fof(f19866,plain,
( $false
| ~ spl1086_348
| ~ spl1086_349
| ~ spl1086_352
| ~ spl1086_359 ),
inference(forward_subsumption_resolution,[],[f19864,f18440]) ).
fof(f19867,plain,
( ~ spl1086_348
| ~ spl1086_349
| ~ spl1086_352
| ~ spl1086_359 ),
inference(avatar_contradiction_clause,[],[f19866]) ).
cnf(s298,plain,
( spl1086_348
| ~ spl1086_349 ),
inference(sat_conversion,[],[f18338]) ).
cnf(s307,plain,
( spl1086_357
| spl1086_359 ),
inference(sat_conversion,[],[f18584]) ).
cnf(s316,plain,
~ spl1086_357,
inference(sat_conversion,[],[f18636]) ).
cnf(s347,plain,
spl1086_349,
inference(sat_conversion,[],[f19032]) ).
cnf(s367,plain,
( ~ spl1086_349
| spl1086_352 ),
inference(sat_conversion,[],[f19834]) ).
cnf(s368,plain,
( ~ spl1086_348
| ~ spl1086_349
| ~ spl1086_352
| ~ spl1086_359 ),
inference(sat_conversion,[],[f19867]) ).
cnf(s369,plain,
spl1086_352,
inference(rat,[],[s367,s347]) ).
cnf(s381,plain,
spl1086_359,
inference(rat,[],[s307,s316]) ).
cnf(s382,plain,
~ spl1086_348,
inference(rat,[],[s368,s369,s347,s381]) ).
cnf(s389,plain,
$false,
inference(rat,[],[s298,s347,s382]) ).
fof(f19868,plain,
$false,
inference(avatar_sat_refutation,[],[s389]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT330+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.38 % Computer : n026.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Sun Sep 27 14:44:27 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.42 Running first-order theorem proving
% 0.12/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 12.10/2.89 % (2908517)Detected formulas, will run a generic FOF schedule.
% 12.10/2.89 % (2908522)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=3755209958:i=141193_2998 on theBenchmark for (2998ds/141193Mi)
% 12.10/2.89 % (2908528)dis-21_1_sil=8000:lcm=predicate:random_seed=3319687199:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2998 on theBenchmark for (2998ds/129Mi)
% 12.10/2.89 % (2908525)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=4136244890:i=109:sd=1:ins=1:gsp=on:ss=axioms_2998 on theBenchmark for (2998ds/109Mi)
% 12.10/2.89 % (2908526)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1771812157:i=119:av=off:ss=axioms_2998 on theBenchmark for (2998ds/119Mi)
% 12.10/2.89 % (2908523)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=744452620:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2998 on theBenchmark for (2998ds/134677Mi)
% 12.10/2.89 % (2908524)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=1098433915:i=141695:sd=1:nm=32:gsp=on:ss=included_2998 on theBenchmark for (2998ds/141695Mi)
% 12.10/2.89 % (2908525)Refutation not found, incomplete strategy
% 12.10/2.89 % (2908525)------------------------------
% 12.10/2.89 % (2908525)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.10/2.89 % (2908525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.10/2.89 % (2908525)CaDiCaL version: 2.1.3
% 12.10/2.89 % (2908525)Termination reason: Refutation not found, incomplete strategy
% 12.10/2.89 % (2908525)Time elapsed: 0.014 s
% 12.10/2.89 % (2908525)Peak memory usage: 92 MB
% 12.10/2.89 % (2908525)Instructions burned: 17 (million)
% 12.10/2.89 % (2908527)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1238373972:s2a=on:i=139:gtg=position_2998 on theBenchmark for (2998ds/139Mi)
% 12.10/2.89 % (2908526)Instruction limit reached!
% 12.10/2.89 % (2908526)------------------------------
% 12.10/2.89 % (2908526)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.10/2.89 % (2908526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.10/2.89 % (2908526)CaDiCaL version: 2.1.3
% 12.10/2.89 % (2908526)Termination reason: Instruction limit
% 12.10/2.89 % (2908526)Termination phase: Saturation
% 12.10/2.89 % (2908526)Time elapsed: 0.076 s
% 12.10/2.89 % (2908526)Peak memory usage: 93 MB
% 12.10/2.89 % (2908526)Instructions burned: 120 (million)
% 12.10/2.89 % (2908528)Instruction limit reached!
% 12.10/2.89 % (2908528)------------------------------
% 12.10/2.89 % (2908528)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.10/2.89 % (2908528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.10/2.89 % (2908528)CaDiCaL version: 2.1.3
% 12.10/2.89 % (2908528)Termination reason: Instruction limit
% 12.10/2.89 % (2908528)Termination phase: Property scanning
% 12.10/2.89 % (2908528)Time elapsed: 0.078 s
% 12.10/2.89 % (2908528)Peak memory usage: 92 MB
% 12.10/2.89 % (2908528)Instructions burned: 129 (million)
% 12.10/2.89 % (2908527)Instruction limit reached!
% 12.10/2.89 % (2908527)------------------------------
% 12.10/2.89 % (2908527)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.10/2.89 % (2908527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.10/2.89 % (2908527)CaDiCaL version: 2.1.3
% 12.10/2.89 % (2908527)Termination reason: Instruction limit
% 12.10/2.89 % (2908527)Termination phase: Clausification
% 12.10/2.89 % (2908527)Time elapsed: 0.086 s
% 12.10/2.89 % (2908527)Peak memory usage: 94 MB
% 12.10/2.89 % (2908527)Instructions burned: 140 (million)
% 12.10/2.89 % (2908537)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2046119725:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi)
% 12.10/2.89 % (2908536)lrs+10_1_sil=8000:sp=occurrence:random_seed=699702510:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi)
% 12.10/2.89 % (2908538)lrs+1011_1_sil=32000:sp=occurrence:random_seed=252734922:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi)
% 12.10/2.89 % (2908537)Refutation not found, incomplete strategy
% 12.10/2.89 % (2908537)------------------------------
% 12.10/2.89 % (2908537)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.10/2.89 % (2908537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.15/3.26 % (2908537)CaDiCaL version: 2.1.3
% 16.15/3.26 % (2908537)Termination reason: Refutation not found, incomplete strategy
% 16.15/3.26 % (2908537)Time elapsed: 0.030 s
% 16.15/3.26 % (2908537)Peak memory usage: 92 MB
% 16.15/3.26 % (2908537)Instructions burned: 51 (million)
% 16.15/3.26 % (2908525)------------------------------
% 16.15/3.26 % (2908525)------------------------------
% 16.15/3.26 % (2908538)Refutation not found, incomplete strategy
% 16.15/3.26 % (2908538)------------------------------
% 16.15/3.26 % (2908538)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.15/3.26 % (2908538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.15/3.26 % (2908538)CaDiCaL version: 2.1.3
% 16.15/3.26 % (2908538)Termination reason: Refutation not found, incomplete strategy
% 16.15/3.26 % (2908538)Time elapsed: 0.029 s
% 16.15/3.26 % (2908538)Peak memory usage: 92 MB
% 16.15/3.26 % (2908538)Instructions burned: 38 (million)
% 16.15/3.26 % (2908536)Instruction limit reached!
% 16.15/3.26 % (2908536)------------------------------
% 16.15/3.26 % (2908536)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.15/3.26 % (2908536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.15/3.26 % (2908536)CaDiCaL version: 2.1.3
% 16.15/3.26 % (2908536)Termination reason: Instruction limit
% 16.15/3.26 % (2908536)Termination phase: Saturation
% 16.15/3.26 % (2908536)Time elapsed: 0.178 s
% 16.15/3.26 % (2908536)Peak memory usage: 95 MB
% 16.15/3.26 % (2908536)Instructions burned: 287 (million)
% 16.15/3.26 % (2908542)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=995101466:s2a=on:i=248:s2at=1.23:gtg=position_2994 on theBenchmark for (2994ds/248Mi)
% 16.15/3.26 % (2908537)------------------------------
% 16.15/3.26 % (2908537)------------------------------
% 16.15/3.26 % (2908538)------------------------------
% 16.15/3.26 % (2908538)------------------------------
% 16.15/3.26 % (2908543)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3448345189:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi)
% 16.15/3.26 % (2908542)Instruction limit reached!
% 16.15/3.26 % (2908542)------------------------------
% 16.15/3.26 % (2908542)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.15/3.26 % (2908542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.15/3.26 % (2908542)CaDiCaL version: 2.1.3
% 16.15/3.26 % (2908542)Termination reason: Instruction limit
% 16.15/3.26 % (2908542)Termination phase: Saturation
% 16.15/3.26 % (2908542)Time elapsed: 0.144 s
% 16.15/3.26 % (2908542)Peak memory usage: 97 MB
% 16.15/3.26 % (2908542)Instructions burned: 249 (million)
% 16.15/3.26 % (2908545)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=4283099987:i=2350_2992 on theBenchmark for (2992ds/2350Mi)
% 16.15/3.26 % (2908546)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1872859018:cts=off:i=113:fsr=off:ss=included:sgt=4_2992 on theBenchmark for (2992ds/113Mi)
% 16.15/3.26 % (2908548)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3641148663:i=127:av=off:fsr=off:sup=off_2991 on theBenchmark for (2991ds/127Mi)
% 16.15/3.26 % (2908543)Instruction limit reached!
% 16.15/3.26 % (2908543)------------------------------
% 16.15/3.26 % (2908543)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.15/3.26 % (2908543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.15/3.26 % (2908543)CaDiCaL version: 2.1.3
% 16.15/3.26 % (2908543)Termination reason: Instruction limit
% 16.15/3.26 % (2908543)Termination phase: Saturation
% 16.15/3.26 % (2908543)Time elapsed: 0.176 s
% 16.15/3.26 % (2908543)Peak memory usage: 95 MB
% 16.15/3.26 % (2908543)Instructions burned: 295 (million)
% 16.15/3.26 % (2908546)Instruction limit reached!
% 16.15/3.26 % (2908546)------------------------------
% 16.15/3.26 % (2908546)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.15/3.26 % (2908546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.15/3.26 % (2908546)CaDiCaL version: 2.1.3
% 16.15/3.26 % (2908546)Termination reason: Instruction limit
% 16.15/3.26 % (2908546)Termination phase: Saturation
% 16.15/3.26 % (2908546)Time elapsed: 0.065 s
% 16.15/3.26 % (2908546)Peak memory usage: 93 MB
% 16.15/3.26 % (2908546)Instructions burned: 113 (million)
% 16.15/3.26 % (2908548)Instruction limit reached!
% 16.15/3.26 % (2908548)------------------------------
% 16.15/3.26 % (2908548)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.15/3.26 % (2908548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.15/3.26 % (2908548)CaDiCaL version: 2.1.3
% 16.15/3.26 % (2908548)Termination reason: Instruction limit
% 16.15/3.26 % (2908548)Termination phase: Property scanning
% 16.15/3.26 % (2908548)Time elapsed: 0.079 s
% 16.15/3.26 % (2908548)Peak memory usage: 94 MB
% 16.15/3.26 % (2908548)Instructions burned: 129 (million)
% 16.15/3.26 % (2908553)lrs+10_1_sil=8000:sp=occurrence:random_seed=3962611997:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi)
% 16.15/3.26 % (2908552)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3877441711:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2990 on theBenchmark for (2990ds/114Mi)
% 16.15/3.26 % (2908552)Instruction limit reached!
% 16.15/3.26 % (2908552)------------------------------
% 16.15/3.26 % (2908552)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.15/3.26 % (2908552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.15/3.26 % (2908552)CaDiCaL version: 2.1.3
% 16.15/3.26 % (2908552)Termination reason: Instruction limit
% 16.15/3.26 % (2908552)Termination phase: Property scanning
% 16.15/3.26 % (2908552)Time elapsed: 0.058 s
% 16.15/3.26 % (2908552)Peak memory usage: 91 MB
% 16.15/3.26 % (2908552)Instructions burned: 116 (million)
% 16.15/3.26 % (2908554)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3759330523:i=437:sd=1:aac=none:ss=included_2989 on theBenchmark for (2989ds/437Mi)
% 16.15/3.26 % (2908558)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2467775560:i=5202:ss=axioms:sgt=16_2988 on theBenchmark for (2988ds/5202Mi)
% 16.15/3.26 % (2908554)Instruction limit reached!
% 16.15/3.26 % (2908554)------------------------------
% 16.15/3.26 % (2908554)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.15/3.26 % (2908554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.15/3.26 % (2908554)CaDiCaL version: 2.1.3
% 16.15/3.26 % (2908554)Termination reason: Instruction limit
% 16.15/3.26 % (2908554)Termination phase: Saturation
% 16.15/3.26 % (2908554)Time elapsed: 0.234 s
% 16.15/3.26 % (2908554)Peak memory usage: 95 MB
% 16.15/3.26 % (2908554)Instructions burned: 437 (million)
% 16.15/3.26 % (2908560)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2759312974:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2985 on theBenchmark for (2985ds/134Mi)
% 16.15/3.26 % (2908560)Instruction limit reached!
% 16.15/3.26 % (2908560)------------------------------
% 16.15/3.26 % (2908560)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.15/3.26 % (2908560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.15/3.26 % (2908560)CaDiCaL version: 2.1.3
% 16.15/3.26 % (2908560)Termination reason: Instruction limit
% 16.15/3.26 % (2908560)Termination phase: Saturation
% 16.15/3.26 % (2908560)Time elapsed: 0.080 s
% 16.15/3.26 % (2908560)Peak memory usage: 95 MB
% 16.15/3.26 % (2908560)Instructions burned: 135 (million)
% 16.15/3.26 % (2908553)Instruction limit reached!
% 16.15/3.26 % (2908553)------------------------------
% 16.15/3.26 % (2908553)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.15/3.26 % (2908553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.15/3.26 % (2908553)CaDiCaL version: 2.1.3
% 16.15/3.26 % (2908553)Termination reason: Instruction limit
% 16.15/3.26 % (2908553)Termination phase: Saturation
% 16.15/3.26 % (2908553)Time elapsed: 0.585 s
% 16.15/3.26 % (2908553)Peak memory usage: 104 MB
% 16.15/3.26 % (2908553)Instructions burned: 907 (million)
% 16.15/3.26 % (2908562)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=4081201919:st=8:i=592:sd=3:ep=RST:ss=axioms_2983 on theBenchmark for (2983ds/592Mi)
% 16.15/3.26 % (2908563)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1237608434:st=3:i=13193:sd=3:ss=axioms_2982 on theBenchmark for (2982ds/13193Mi)
% 16.15/3.26 % (2908562)Instruction limit reached!
% 16.15/3.26 % (2908562)------------------------------
% 16.15/3.26 % (2908562)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.15/3.26 % (2908562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.15/3.26 % (2908562)CaDiCaL version: 2.1.3
% 16.15/3.26 % (2908562)Termination reason: Instruction limit
% 16.15/3.26 % (2908562)Termination phase: Saturation
% 16.15/3.26 % (2908562)Time elapsed: 0.297 s
% 16.15/3.26 % (2908562)Peak memory usage: 102 MB
% 16.15/3.26 % (2908562)Instructions burned: 593 (million)
% 16.15/3.26 % (2908522)First to succeed.
% 16.15/3.26 % (2908522)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2908517"
% 16.15/3.26 % (2908566)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=93085687:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2979 on theBenchmark for (2979ds/125Mi)
% 16.15/3.26 % (2908566)Instruction limit reached!
% 16.15/3.26 % (2908566)------------------------------
% 16.15/3.26 % (2908566)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.15/3.26 % (2908566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.15/3.26 % (2908566)CaDiCaL version: 2.1.3
% 16.15/3.26 % (2908566)Termination reason: Instruction limit
% 16.15/3.26 % (2908566)Termination phase: Saturation
% 16.15/3.26 % (2908566)Time elapsed: 0.070 s
% 16.15/3.26 % (2908566)Peak memory usage: 93 MB
% 16.15/3.26 % (2908566)Instructions burned: 126 (million)
% 16.15/3.26 % (2908568)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2906580395:i=134:gtgl=5:slsql=off:gtg=exists_sym_2977 on theBenchmark for (2977ds/134Mi)
% 16.15/3.26 % (2908545)Instruction limit reached!
% 16.15/3.26 % (2908545)------------------------------
% 16.15/3.26 % (2908545)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.15/3.26 % (2908545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.15/3.26 % (2908545)CaDiCaL version: 2.1.3
% 16.15/3.26 % (2908545)Termination reason: Instruction limit
% 16.15/3.26 % (2908545)Termination phase: Saturation
% 16.15/3.26 % (2908545)Time elapsed: 1.478 s
% 16.15/3.26 % (2908545)Peak memory usage: 209 MB
% 16.15/3.26 % (2908545)Instructions burned: 2350 (million)
% 16.15/3.26 % (2908522)Refutation found. Thanks to Tanya!
% 16.15/3.26 % SZS status Theorem for theBenchmark
% 16.15/3.26 % SZS output start Proof for theBenchmark
% See solution above
% 16.82/3.46 % (2908522)------------------------------
% 16.82/3.46 % (2908522)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.82/3.46 % (2908522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.82/3.46 % (2908522)CaDiCaL version: 2.1.3
% 16.82/3.46 % (2908522)Termination reason: Refutation
% 16.82/3.46 % (2908522)Time elapsed: 1.894 s
% 16.82/3.46 % (2908522)Peak memory usage: 196 MB
% 16.82/3.46 % (2908522)Instructions burned: 3803 (million)
% 16.82/3.46 % (2908522)------------------------------
% 16.82/3.46 % (2908522)------------------------------
% 16.82/3.46 % (2908517)Success in time 2.406 s
% 16.82/3.46 % Vampire exiting
%------------------------------------------------------------------------------