%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LAT330+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n004.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:48:27 AM UTC 2026
% Result : Theorem 0.44s 0.49s
% Output : Refutation 0.44s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 22
% Syntax : Number of formulae : 216 ( 24 unt; 8 def)
% Number of atoms : 911 ( 0 equ)
% Maximal formula atoms : 11 ( 4 avg)
% Number of connectives : 1129 ( 434 ~; 600 |; 47 &)
% ( 18 <=>; 30 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 23 ( 22 usr; 9 prp; 0-3 aty)
% Number of functors : 8 ( 8 usr; 2 con; 0-3 aty)
% Number of variables : 237 ( 0 sgn 233 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,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/sandbox/benchmark/theBenchmark.p',t67_filter_2) ).
fof(f2,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)],[f1]) ).
fof(f7,axiom,
! [X0] :
( ~ v1_xboole_0(X0)
=> ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(X0))
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(X0))
=> ( r1_filter_2(X0,X1,X2)
<=> ! [X3] :
( m1_subset_1(X3,X0)
=> ( r2_hidden(X3,X1)
<=> r2_hidden(X3,X2) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d1_filter_2) ).
fof(f9,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/sandbox/benchmark/theBenchmark.p',dt_k18_filter_2) ).
fof(f12,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/sandbox/benchmark/theBenchmark.p',dt_k22_filter_2) ).
fof(f13,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_lattices(X0) )
=> m1_subset_1(k5_lattices(X0),u1_struct_0(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k5_lattices) ).
fof(f14,axiom,
! [X0] :
( l1_lattices(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l1_lattices) ).
fof(f17,axiom,
! [X0] :
( l3_lattices(X0)
=> ( l1_lattices(X0)
& l2_lattices(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l3_lattices) ).
fof(f19,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/sandbox/benchmark/theBenchmark.p',dt_m2_filter_2) ).
fof(f20,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/sandbox/benchmark/theBenchmark.p',dt_m2_lattice4) ).
fof(f29,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_struct_0(X0) )
=> ~ v1_xboole_0(u1_struct_0(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_struct_0) ).
fof(f47,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/sandbox/benchmark/theBenchmark.p',t29_filter_2) ).
fof(f51,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/sandbox/benchmark/theBenchmark.p',t41_lattices) ).
fof(f53,axiom,
! [X0,X1,X2] :
~ ( r2_hidden(X0,X1)
& m1_subset_1(X1,k1_zfmisc_1(X2))
& v1_xboole_0(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t5_subset) ).
fof(f54,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/sandbox/benchmark/theBenchmark.p',t63_filter_2) ).
fof(f61,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,[],[f2]) ).
fof(f62,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,[],[f61]) ).
fof(f68,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( r1_filter_2(X0,X1,X2)
<=> ! [X3] :
( ( r2_hidden(X3,X1)
<=> r2_hidden(X3,X2) )
| ~ m1_subset_1(X3,X0) ) )
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) )
| ~ m1_subset_1(X1,k1_zfmisc_1(X0)) )
| v1_xboole_0(X0) ),
inference(ennf_transformation,[],[f7]) ).
fof(f71,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,[],[f9]) ).
fof(f72,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,[],[f71]) ).
fof(f73,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,[],[f12]) ).
fof(f74,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,[],[f73]) ).
fof(f75,plain,
! [X0] :
( m1_subset_1(k5_lattices(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_lattices(X0) ),
inference(ennf_transformation,[],[f13]) ).
fof(f76,plain,
! [X0] :
( m1_subset_1(k5_lattices(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_lattices(X0) ),
inference(flattening,[],[f75]) ).
fof(f77,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_lattices(X0) ),
inference(ennf_transformation,[],[f14]) ).
fof(f79,plain,
! [X0] :
( ( l1_lattices(X0)
& l2_lattices(X0) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f17]) ).
fof(f80,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,[],[f19]) ).
fof(f81,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,[],[f80]) ).
fof(f82,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,[],[f20]) ).
fof(f83,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,[],[f82]) ).
fof(f88,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f29]) ).
fof(f89,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(flattening,[],[f88]) ).
fof(f108,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,[],[f47]) ).
fof(f109,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,[],[f108]) ).
fof(f114,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,[],[f51]) ).
fof(f115,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,[],[f114]) ).
fof(f118,plain,
! [X0,X1,X2] :
( ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ v1_xboole_0(X2) ),
inference(ennf_transformation,[],[f53]) ).
fof(f119,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,[],[f54]) ).
fof(f120,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,[],[f119]) ).
fof(f124,plain,
m1_subset_1(sK1,u1_struct_0(sK0)),
inference(cnf_transformation,[],[f62]) ).
fof(f125,plain,
v13_lattices(sK0),
inference(cnf_transformation,[],[f62]) ).
fof(f126,plain,
~ r1_filter_2(u1_struct_0(sK0),k18_filter_2(sK0,sK1),k22_filter_2(sK0,k5_lattices(sK0),sK1)),
inference(cnf_transformation,[],[f62]) ).
fof(f127,plain,
l3_lattices(sK0),
inference(cnf_transformation,[],[f62]) ).
fof(f128,plain,
v10_lattices(sK0),
inference(cnf_transformation,[],[f62]) ).
fof(f129,plain,
~ v3_struct_0(sK0),
inference(cnf_transformation,[],[f62]) ).
fof(f138,plain,
! [X2,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| r2_hidden(sK2(X0,X1,X2),X2)
| r2_hidden(sK2(X0,X1,X2),X1)
| r1_filter_2(X0,X1,X2) ),
inference(cnf_transformation,[],[f68]) ).
fof(f139,plain,
! [X2,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| ~ r2_hidden(sK2(X0,X1,X2),X2)
| ~ r2_hidden(sK2(X0,X1,X2),X1)
| r1_filter_2(X0,X1,X2) ),
inference(cnf_transformation,[],[f68]) ).
fof(f142,plain,
! [X2,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| m1_subset_1(sK2(X0,X1,X2),X0)
| r1_filter_2(X0,X1,X2) ),
inference(cnf_transformation,[],[f68]) ).
fof(f144,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| m2_filter_2(k18_filter_2(X0,X1),X0) ),
inference(cnf_transformation,[],[f72]) ).
fof(f145,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| m2_lattice4(k22_filter_2(X0,X1,X2),X0) ),
inference(cnf_transformation,[],[f74]) ).
fof(f147,plain,
! [X0] :
( ~ l1_lattices(X0)
| v3_struct_0(X0)
| m1_subset_1(k5_lattices(X0),u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f76]) ).
fof(f148,plain,
! [X0] :
( ~ l1_lattices(X0)
| l1_struct_0(X0) ),
inference(cnf_transformation,[],[f77]) ).
fof(f151,plain,
! [X0] :
( ~ l3_lattices(X0)
| l1_lattices(X0) ),
inference(cnf_transformation,[],[f79]) ).
fof(f152,plain,
! [X0,X1] :
( ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ m2_filter_2(X1,X0)
| m2_lattice4(X1,X0) ),
inference(cnf_transformation,[],[f81]) ).
fof(f154,plain,
! [X0,X1] :
( ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ m2_lattice4(X1,X0)
| m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ),
inference(cnf_transformation,[],[f83]) ).
fof(f162,plain,
! [X0] :
( ~ l1_struct_0(X0)
| v3_struct_0(X0)
| ~ v1_xboole_0(u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f89]) ).
fof(f190,plain,
! [X2,X0,X1] :
( ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ r3_lattices(X0,X1,X2)
| r2_hidden(X1,k18_filter_2(X0,X2)) ),
inference(cnf_transformation,[],[f109]) ).
fof(f191,plain,
! [X2,X0,X1] :
( ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| r3_lattices(X0,X1,X2)
| ~ r2_hidden(X1,k18_filter_2(X0,X2)) ),
inference(cnf_transformation,[],[f109]) ).
fof(f196,plain,
! [X0,X1] :
( ~ l3_lattices(X0)
| ~ v13_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| r3_lattices(X0,k5_lattices(X0),X1) ),
inference(cnf_transformation,[],[f115]) ).
fof(f198,plain,
! [X2,X0,X1] :
( ~ v1_xboole_0(X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ r2_hidden(X0,X1) ),
inference(cnf_transformation,[],[f118]) ).
fof(f199,plain,
! [X2,X3,X0,X1] :
( ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ r3_lattices(X0,X1,X2)
| r3_lattices(X0,X3,X2)
| ~ r2_hidden(X3,k22_filter_2(X0,X1,X2)) ),
inference(cnf_transformation,[],[f120]) ).
fof(f201,plain,
! [X2,X3,X0,X1] :
( ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ r3_lattices(X0,X1,X2)
| ~ r3_lattices(X0,X3,X2)
| ~ r3_lattices(X0,X1,X3)
| r2_hidden(X3,k22_filter_2(X0,X1,X2)) ),
inference(cnf_transformation,[],[f120]) ).
fof(f207,plain,
v3_struct_0(sK0),
inference(consistent_polarity_flipping,[],[f129]) ).
fof(f208,plain,
r1_filter_2(u1_struct_0(sK0),k18_filter_2(sK0,sK1),k22_filter_2(sK0,k5_lattices(sK0),sK1)),
inference(consistent_polarity_flipping,[],[f126]) ).
fof(f209,plain,
~ v13_lattices(sK0),
inference(consistent_polarity_flipping,[],[f125]) ).
fof(f210,plain,
~ m1_subset_1(sK1,u1_struct_0(sK0)),
inference(consistent_polarity_flipping,[],[f124]) ).
fof(f218,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(sK2(X0,X1,X2),X0)
| m1_subset_1(X1,k1_zfmisc_1(X0))
| m1_subset_1(X2,k1_zfmisc_1(X0))
| ~ v1_xboole_0(X0)
| ~ r1_filter_2(X0,X1,X2) ),
inference(consistent_polarity_flipping,[],[f142]) ).
fof(f221,plain,
! [X2,X0,X1] :
( ~ v1_xboole_0(X0)
| m1_subset_1(X1,k1_zfmisc_1(X0))
| m1_subset_1(X2,k1_zfmisc_1(X0))
| ~ r2_hidden(sK2(X0,X1,X2),X2)
| ~ r2_hidden(sK2(X0,X1,X2),X1)
| ~ r1_filter_2(X0,X1,X2) ),
inference(consistent_polarity_flipping,[],[f139]) ).
fof(f222,plain,
! [X2,X0,X1] :
( ~ r1_filter_2(X0,X1,X2)
| m1_subset_1(X1,k1_zfmisc_1(X0))
| m1_subset_1(X2,k1_zfmisc_1(X0))
| r2_hidden(sK2(X0,X1,X2),X2)
| r2_hidden(sK2(X0,X1,X2),X1)
| ~ v1_xboole_0(X0) ),
inference(consistent_polarity_flipping,[],[f138]) ).
fof(f224,plain,
! [X0,X1] :
( ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| m1_subset_1(X1,u1_struct_0(X0))
| ~ v3_struct_0(X0)
| ~ m2_filter_2(k18_filter_2(X0,X1),X0) ),
inference(consistent_polarity_flipping,[],[f144]) ).
fof(f226,plain,
! [X2,X0,X1] :
( m2_lattice4(k22_filter_2(X0,X1,X2),X0)
| m1_subset_1(X1,u1_struct_0(X0))
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| ~ v3_struct_0(X0)
| m1_subset_1(X2,u1_struct_0(X0)) ),
inference(consistent_polarity_flipping,[],[f145]) ).
fof(f227,plain,
! [X0] :
( ~ m1_subset_1(k5_lattices(X0),u1_struct_0(X0))
| ~ v3_struct_0(X0)
| ~ l1_lattices(X0) ),
inference(consistent_polarity_flipping,[],[f147]) ).
fof(f228,plain,
! [X0] :
( ~ l1_struct_0(X0)
| ~ l1_lattices(X0) ),
inference(consistent_polarity_flipping,[],[f148]) ).
fof(f232,plain,
! [X0,X1] :
( ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ v3_struct_0(X0)
| m2_filter_2(X1,X0)
| m2_lattice4(X1,X0) ),
inference(consistent_polarity_flipping,[],[f152]) ).
fof(f233,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v10_lattices(X0)
| ~ v3_struct_0(X0)
| ~ m2_lattice4(X1,X0)
| ~ l3_lattices(X0) ),
inference(consistent_polarity_flipping,[],[f154]) ).
fof(f239,plain,
! [X0] :
( v1_xboole_0(u1_struct_0(X0))
| ~ v3_struct_0(X0)
| l1_struct_0(X0) ),
inference(consistent_polarity_flipping,[],[f162]) ).
fof(f266,plain,
! [X2,X0,X1] :
( ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ v3_struct_0(X0)
| m1_subset_1(X1,u1_struct_0(X0))
| m1_subset_1(X2,u1_struct_0(X0))
| r3_lattices(X0,X1,X2)
| ~ r2_hidden(X1,k18_filter_2(X0,X2)) ),
inference(consistent_polarity_flipping,[],[f191]) ).
fof(f267,plain,
! [X2,X0,X1] :
( ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ v3_struct_0(X0)
| m1_subset_1(X1,u1_struct_0(X0))
| m1_subset_1(X2,u1_struct_0(X0))
| ~ r3_lattices(X0,X1,X2)
| r2_hidden(X1,k18_filter_2(X0,X2)) ),
inference(consistent_polarity_flipping,[],[f190]) ).
fof(f270,plain,
! [X0,X1] :
( r3_lattices(X0,k5_lattices(X0),X1)
| v13_lattices(X0)
| ~ v10_lattices(X0)
| ~ v3_struct_0(X0)
| m1_subset_1(X1,u1_struct_0(X0))
| ~ l3_lattices(X0) ),
inference(consistent_polarity_flipping,[],[f196]) ).
fof(f272,plain,
! [X2,X0,X1] :
( ~ r2_hidden(X0,X1)
| m1_subset_1(X1,k1_zfmisc_1(X2))
| v1_xboole_0(X2) ),
inference(consistent_polarity_flipping,[],[f198]) ).
fof(f273,plain,
! [X2,X3,X0,X1] :
( ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ v3_struct_0(X0)
| m1_subset_1(X1,u1_struct_0(X0))
| m1_subset_1(X2,u1_struct_0(X0))
| m1_subset_1(X3,u1_struct_0(X0))
| ~ r3_lattices(X0,X1,X2)
| ~ r3_lattices(X0,X3,X2)
| ~ r3_lattices(X0,X1,X3)
| r2_hidden(X3,k22_filter_2(X0,X1,X2)) ),
inference(consistent_polarity_flipping,[],[f201]) ).
fof(f275,plain,
! [X2,X3,X0,X1] :
( ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ v3_struct_0(X0)
| m1_subset_1(X1,u1_struct_0(X0))
| m1_subset_1(X2,u1_struct_0(X0))
| m1_subset_1(X3,u1_struct_0(X0))
| ~ r3_lattices(X0,X1,X2)
| r3_lattices(X0,X3,X2)
| ~ r2_hidden(X3,k22_filter_2(X0,X1,X2)) ),
inference(consistent_polarity_flipping,[],[f199]) ).
fof(f280,plain,
l1_lattices(sK0),
inference(resolution,[],[f151,f127]) ).
fof(f316,plain,
! [X0] :
( ~ l3_lattices(sK0)
| ~ v3_struct_0(sK0)
| m2_filter_2(X0,sK0)
| m2_lattice4(X0,sK0) ),
inference(resolution,[],[f232,f128]) ).
fof(f317,plain,
! [X0] :
( ~ v3_struct_0(sK0)
| m2_filter_2(X0,sK0)
| m2_lattice4(X0,sK0) ),
inference(forward_subsumption_resolution,[],[f316,f127]) ).
fof(f318,plain,
! [X0] :
( m2_filter_2(X0,sK0)
| m2_lattice4(X0,sK0) ),
inference(forward_subsumption_resolution,[],[f317,f207]) ).
fof(f338,plain,
! [X0] :
( ~ l3_lattices(sK0)
| m1_subset_1(X0,u1_struct_0(sK0))
| ~ v3_struct_0(sK0)
| ~ m2_filter_2(k18_filter_2(sK0,X0),sK0) ),
inference(resolution,[],[f224,f128]) ).
fof(f339,plain,
! [X0] :
( m1_subset_1(X0,u1_struct_0(sK0))
| ~ v3_struct_0(sK0)
| ~ m2_filter_2(k18_filter_2(sK0,X0),sK0) ),
inference(forward_subsumption_resolution,[],[f338,f127]) ).
fof(f340,plain,
! [X0] :
( ~ m2_filter_2(k18_filter_2(sK0,X0),sK0)
| m1_subset_1(X0,u1_struct_0(sK0)) ),
inference(forward_subsumption_resolution,[],[f339,f207]) ).
fof(f356,definition,
( spl19_1
<=> m1_subset_1(k18_filter_2(sK0,sK1),k1_zfmisc_1(u1_struct_0(sK0))) ),
introduced(definition,[new_symbols(definition,[spl19_1])],[avatar_definition]) ).
fof(f357,plain,
( ~ m1_subset_1(k18_filter_2(sK0,sK1),k1_zfmisc_1(u1_struct_0(sK0)))
| spl19_1 ),
inference(avatar_component_clause,[],[f356]) ).
fof(f358,plain,
( m1_subset_1(k18_filter_2(sK0,sK1),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ spl19_1 ),
inference(avatar_component_clause,[],[f356]) ).
fof(f364,definition,
( spl19_3
<=> v1_xboole_0(u1_struct_0(sK0)) ),
introduced(definition,[new_symbols(definition,[spl19_3])],[avatar_definition]) ).
fof(f365,plain,
( v1_xboole_0(u1_struct_0(sK0))
| ~ spl19_3 ),
inference(avatar_component_clause,[],[f364]) ).
fof(f366,plain,
( ~ v1_xboole_0(u1_struct_0(sK0))
| spl19_3 ),
inference(avatar_component_clause,[],[f364]) ).
fof(f368,definition,
( spl19_4
<=> m1_subset_1(k22_filter_2(sK0,k5_lattices(sK0),sK1),k1_zfmisc_1(u1_struct_0(sK0))) ),
introduced(definition,[new_symbols(definition,[spl19_4])],[avatar_definition]) ).
fof(f369,plain,
( ~ m1_subset_1(k22_filter_2(sK0,k5_lattices(sK0),sK1),k1_zfmisc_1(u1_struct_0(sK0)))
| spl19_4 ),
inference(avatar_component_clause,[],[f368]) ).
fof(f370,plain,
( m1_subset_1(k22_filter_2(sK0,k5_lattices(sK0),sK1),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ spl19_4 ),
inference(avatar_component_clause,[],[f368]) ).
fof(f372,plain,
( ~ v3_struct_0(sK0)
| l1_struct_0(sK0)
| spl19_3 ),
inference(resolution,[],[f366,f239]) ).
fof(f376,plain,
( l1_struct_0(sK0)
| spl19_3 ),
inference(forward_subsumption_resolution,[],[f372,f207]) ).
fof(f378,plain,
( ~ l1_lattices(sK0)
| spl19_3 ),
inference(resolution,[],[f376,f228]) ).
fof(f379,plain,
( $false
| spl19_3 ),
inference(forward_subsumption_resolution,[],[f378,f280]) ).
fof(f380,plain,
spl19_3,
inference(avatar_contradiction_clause,[],[f379]) ).
fof(f383,plain,
! [X0] :
( m2_lattice4(k18_filter_2(sK0,X0),sK0)
| m1_subset_1(X0,u1_struct_0(sK0)) ),
inference(resolution,[],[f340,f318]) ).
fof(f406,plain,
! [X0,X1] :
( ~ l3_lattices(sK0)
| ~ v3_struct_0(sK0)
| m1_subset_1(X0,u1_struct_0(sK0))
| m1_subset_1(X1,u1_struct_0(sK0))
| r3_lattices(sK0,X0,X1)
| ~ r2_hidden(X0,k18_filter_2(sK0,X1)) ),
inference(resolution,[],[f266,f128]) ).
fof(f407,plain,
! [X0,X1] :
( ~ v3_struct_0(sK0)
| m1_subset_1(X0,u1_struct_0(sK0))
| m1_subset_1(X1,u1_struct_0(sK0))
| r3_lattices(sK0,X0,X1)
| ~ r2_hidden(X0,k18_filter_2(sK0,X1)) ),
inference(forward_subsumption_resolution,[],[f406,f127]) ).
fof(f408,plain,
! [X0,X1] :
( ~ r2_hidden(X0,k18_filter_2(sK0,X1))
| m1_subset_1(X1,u1_struct_0(sK0))
| r3_lattices(sK0,X0,X1)
| m1_subset_1(X0,u1_struct_0(sK0)) ),
inference(forward_subsumption_resolution,[],[f407,f207]) ).
fof(f442,plain,
! [X0,X1] :
( ~ l3_lattices(sK0)
| ~ v3_struct_0(sK0)
| m1_subset_1(X0,u1_struct_0(sK0))
| m1_subset_1(X1,u1_struct_0(sK0))
| ~ r3_lattices(sK0,X0,X1)
| r2_hidden(X0,k18_filter_2(sK0,X1)) ),
inference(resolution,[],[f267,f128]) ).
fof(f443,plain,
! [X0,X1] :
( ~ v3_struct_0(sK0)
| m1_subset_1(X0,u1_struct_0(sK0))
| m1_subset_1(X1,u1_struct_0(sK0))
| ~ r3_lattices(sK0,X0,X1)
| r2_hidden(X0,k18_filter_2(sK0,X1)) ),
inference(forward_subsumption_resolution,[],[f442,f127]) ).
fof(f444,plain,
! [X0,X1] :
( ~ r3_lattices(sK0,X0,X1)
| m1_subset_1(X1,u1_struct_0(sK0))
| m1_subset_1(X0,u1_struct_0(sK0))
| r2_hidden(X0,k18_filter_2(sK0,X1)) ),
inference(forward_subsumption_resolution,[],[f443,f207]) ).
fof(f445,plain,
! [X2,X0,X1] :
( ~ r2_hidden(sK2(X0,X1,X2),X2)
| m1_subset_1(X2,k1_zfmisc_1(X0))
| m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ r2_hidden(sK2(X0,X1,X2),X1)
| ~ r1_filter_2(X0,X1,X2) ),
inference(forward_subsumption_resolution,[],[f221,f272]) ).
fof(f447,plain,
( m1_subset_1(k18_filter_2(sK0,sK1),k1_zfmisc_1(u1_struct_0(sK0)))
| m1_subset_1(k22_filter_2(sK0,k5_lattices(sK0),sK1),k1_zfmisc_1(u1_struct_0(sK0)))
| r2_hidden(sK2(u1_struct_0(sK0),k18_filter_2(sK0,sK1),k22_filter_2(sK0,k5_lattices(sK0),sK1)),k22_filter_2(sK0,k5_lattices(sK0),sK1))
| r2_hidden(sK2(u1_struct_0(sK0),k18_filter_2(sK0,sK1),k22_filter_2(sK0,k5_lattices(sK0),sK1)),k18_filter_2(sK0,sK1))
| ~ v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolution,[],[f222,f208]) ).
fof(f450,plain,
( m1_subset_1(k18_filter_2(sK0,sK1),k1_zfmisc_1(u1_struct_0(sK0)))
| m1_subset_1(k22_filter_2(sK0,k5_lattices(sK0),sK1),k1_zfmisc_1(u1_struct_0(sK0)))
| r2_hidden(sK2(u1_struct_0(sK0),k18_filter_2(sK0,sK1),k22_filter_2(sK0,k5_lattices(sK0),sK1)),k22_filter_2(sK0,k5_lattices(sK0),sK1))
| r2_hidden(sK2(u1_struct_0(sK0),k18_filter_2(sK0,sK1),k22_filter_2(sK0,k5_lattices(sK0),sK1)),k18_filter_2(sK0,sK1))
| ~ spl19_3 ),
inference(forward_subsumption_resolution,[],[f447,f365]) ).
fof(f452,definition,
( spl19_9
<=> r2_hidden(sK2(u1_struct_0(sK0),k18_filter_2(sK0,sK1),k22_filter_2(sK0,k5_lattices(sK0),sK1)),k18_filter_2(sK0,sK1)) ),
introduced(definition,[new_symbols(definition,[spl19_9])],[avatar_definition]) ).
fof(f454,plain,
( r2_hidden(sK2(u1_struct_0(sK0),k18_filter_2(sK0,sK1),k22_filter_2(sK0,k5_lattices(sK0),sK1)),k18_filter_2(sK0,sK1))
| ~ spl19_9 ),
inference(avatar_component_clause,[],[f452]) ).
fof(f456,definition,
( spl19_10
<=> r2_hidden(sK2(u1_struct_0(sK0),k18_filter_2(sK0,sK1),k22_filter_2(sK0,k5_lattices(sK0),sK1)),k22_filter_2(sK0,k5_lattices(sK0),sK1)) ),
introduced(definition,[new_symbols(definition,[spl19_10])],[avatar_definition]) ).
fof(f457,plain,
( ~ r2_hidden(sK2(u1_struct_0(sK0),k18_filter_2(sK0,sK1),k22_filter_2(sK0,k5_lattices(sK0),sK1)),k22_filter_2(sK0,k5_lattices(sK0),sK1))
| spl19_10 ),
inference(avatar_component_clause,[],[f456]) ).
fof(f458,plain,
( r2_hidden(sK2(u1_struct_0(sK0),k18_filter_2(sK0,sK1),k22_filter_2(sK0,k5_lattices(sK0),sK1)),k22_filter_2(sK0,k5_lattices(sK0),sK1))
| ~ spl19_10 ),
inference(avatar_component_clause,[],[f456]) ).
fof(f459,plain,
( spl19_9
| spl19_10
| spl19_4
| spl19_1
| ~ spl19_3 ),
inference(avatar_split_clause,[],[f450,f364,f356,f368,f456,f452]) ).
fof(f462,plain,
( ~ v10_lattices(sK0)
| ~ v3_struct_0(sK0)
| ~ m2_lattice4(k18_filter_2(sK0,sK1),sK0)
| ~ l3_lattices(sK0)
| ~ spl19_1 ),
inference(resolution,[],[f358,f233]) ).
fof(f465,plain,
( ~ v3_struct_0(sK0)
| ~ m2_lattice4(k18_filter_2(sK0,sK1),sK0)
| ~ l3_lattices(sK0)
| ~ spl19_1 ),
inference(forward_subsumption_resolution,[],[f462,f128]) ).
fof(f466,plain,
( ~ m2_lattice4(k18_filter_2(sK0,sK1),sK0)
| ~ l3_lattices(sK0)
| ~ spl19_1 ),
inference(forward_subsumption_resolution,[],[f465,f207]) ).
fof(f467,plain,
( ~ m2_lattice4(k18_filter_2(sK0,sK1),sK0)
| ~ spl19_1 ),
inference(forward_subsumption_resolution,[],[f466,f127]) ).
fof(f468,plain,
( m1_subset_1(sK1,u1_struct_0(sK0))
| ~ spl19_1 ),
inference(resolution,[],[f467,f383]) ).
fof(f469,plain,
( $false
| ~ spl19_1 ),
inference(forward_subsumption_resolution,[],[f468,f210]) ).
fof(f470,plain,
~ spl19_1,
inference(avatar_contradiction_clause,[],[f469]) ).
fof(f478,plain,
! [X2,X0,X1] :
( ~ l3_lattices(sK0)
| ~ v3_struct_0(sK0)
| m1_subset_1(X0,u1_struct_0(sK0))
| m1_subset_1(X1,u1_struct_0(sK0))
| m1_subset_1(X2,u1_struct_0(sK0))
| ~ r3_lattices(sK0,X0,X1)
| r3_lattices(sK0,X2,X1)
| ~ r2_hidden(X2,k22_filter_2(sK0,X0,X1)) ),
inference(resolution,[],[f275,f128]) ).
fof(f479,plain,
! [X2,X0,X1] :
( ~ v3_struct_0(sK0)
| m1_subset_1(X0,u1_struct_0(sK0))
| m1_subset_1(X1,u1_struct_0(sK0))
| m1_subset_1(X2,u1_struct_0(sK0))
| ~ r3_lattices(sK0,X0,X1)
| r3_lattices(sK0,X2,X1)
| ~ r2_hidden(X2,k22_filter_2(sK0,X0,X1)) ),
inference(forward_subsumption_resolution,[],[f478,f127]) ).
fof(f480,plain,
! [X2,X0,X1] :
( ~ r3_lattices(sK0,X0,X1)
| m1_subset_1(X1,u1_struct_0(sK0))
| m1_subset_1(X2,u1_struct_0(sK0))
| m1_subset_1(X0,u1_struct_0(sK0))
| r3_lattices(sK0,X2,X1)
| ~ r2_hidden(X2,k22_filter_2(sK0,X0,X1)) ),
inference(forward_subsumption_resolution,[],[f479,f207]) ).
fof(f481,plain,
! [X2,X0,X1] :
( ~ l3_lattices(sK0)
| ~ v3_struct_0(sK0)
| m1_subset_1(X0,u1_struct_0(sK0))
| m1_subset_1(X1,u1_struct_0(sK0))
| m1_subset_1(X2,u1_struct_0(sK0))
| ~ r3_lattices(sK0,X0,X1)
| ~ r3_lattices(sK0,X2,X1)
| ~ r3_lattices(sK0,X0,X2)
| r2_hidden(X2,k22_filter_2(sK0,X0,X1)) ),
inference(resolution,[],[f273,f128]) ).
fof(f482,plain,
! [X2,X0,X1] :
( ~ v3_struct_0(sK0)
| m1_subset_1(X0,u1_struct_0(sK0))
| m1_subset_1(X1,u1_struct_0(sK0))
| m1_subset_1(X2,u1_struct_0(sK0))
| ~ r3_lattices(sK0,X0,X1)
| ~ r3_lattices(sK0,X2,X1)
| ~ r3_lattices(sK0,X0,X2)
| r2_hidden(X2,k22_filter_2(sK0,X0,X1)) ),
inference(forward_subsumption_resolution,[],[f481,f127]) ).
fof(f483,plain,
! [X2,X0,X1] :
( ~ r3_lattices(sK0,X0,X2)
| m1_subset_1(X1,u1_struct_0(sK0))
| m1_subset_1(X2,u1_struct_0(sK0))
| ~ r3_lattices(sK0,X0,X1)
| ~ r3_lattices(sK0,X2,X1)
| m1_subset_1(X0,u1_struct_0(sK0))
| r2_hidden(X2,k22_filter_2(sK0,X0,X1)) ),
inference(forward_subsumption_resolution,[],[f482,f207]) ).
fof(f485,plain,
( ~ v10_lattices(sK0)
| ~ v3_struct_0(sK0)
| ~ m2_lattice4(k22_filter_2(sK0,k5_lattices(sK0),sK1),sK0)
| ~ l3_lattices(sK0)
| ~ spl19_4 ),
inference(resolution,[],[f370,f233]) ).
fof(f488,plain,
( ~ v3_struct_0(sK0)
| ~ m2_lattice4(k22_filter_2(sK0,k5_lattices(sK0),sK1),sK0)
| ~ l3_lattices(sK0)
| ~ spl19_4 ),
inference(forward_subsumption_resolution,[],[f485,f128]) ).
fof(f489,plain,
( ~ m2_lattice4(k22_filter_2(sK0,k5_lattices(sK0),sK1),sK0)
| ~ l3_lattices(sK0)
| ~ spl19_4 ),
inference(forward_subsumption_resolution,[],[f488,f207]) ).
fof(f490,plain,
( ~ m2_lattice4(k22_filter_2(sK0,k5_lattices(sK0),sK1),sK0)
| ~ spl19_4 ),
inference(forward_subsumption_resolution,[],[f489,f127]) ).
fof(f508,plain,
( m1_subset_1(k5_lattices(sK0),u1_struct_0(sK0))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| ~ v3_struct_0(sK0)
| m1_subset_1(sK1,u1_struct_0(sK0))
| ~ spl19_4 ),
inference(resolution,[],[f490,f226]) ).
fof(f509,plain,
( m1_subset_1(k5_lattices(sK0),u1_struct_0(sK0))
| ~ v10_lattices(sK0)
| ~ v3_struct_0(sK0)
| m1_subset_1(sK1,u1_struct_0(sK0))
| ~ spl19_4 ),
inference(forward_subsumption_resolution,[],[f508,f127]) ).
fof(f510,plain,
( m1_subset_1(k5_lattices(sK0),u1_struct_0(sK0))
| ~ v3_struct_0(sK0)
| m1_subset_1(sK1,u1_struct_0(sK0))
| ~ spl19_4 ),
inference(forward_subsumption_resolution,[],[f509,f128]) ).
fof(f511,plain,
( m1_subset_1(k5_lattices(sK0),u1_struct_0(sK0))
| m1_subset_1(sK1,u1_struct_0(sK0))
| ~ spl19_4 ),
inference(forward_subsumption_resolution,[],[f510,f207]) ).
fof(f512,plain,
( m1_subset_1(k5_lattices(sK0),u1_struct_0(sK0))
| ~ spl19_4 ),
inference(forward_subsumption_resolution,[],[f511,f210]) ).
fof(f526,definition,
( spl19_11
<=> m1_subset_1(k5_lattices(sK0),u1_struct_0(sK0)) ),
introduced(definition,[new_symbols(definition,[spl19_11])],[avatar_definition]) ).
fof(f527,plain,
( ~ m1_subset_1(k5_lattices(sK0),u1_struct_0(sK0))
| spl19_11 ),
inference(avatar_component_clause,[],[f526]) ).
fof(f528,plain,
( m1_subset_1(k5_lattices(sK0),u1_struct_0(sK0))
| ~ spl19_11 ),
inference(avatar_component_clause,[],[f526]) ).
fof(f537,plain,
( ~ v3_struct_0(sK0)
| ~ l1_lattices(sK0)
| ~ spl19_11 ),
inference(resolution,[],[f528,f227]) ).
fof(f539,plain,
( ~ l1_lattices(sK0)
| ~ spl19_11 ),
inference(forward_subsumption_resolution,[],[f537,f207]) ).
fof(f540,plain,
( $false
| ~ spl19_11 ),
inference(forward_subsumption_resolution,[],[f539,f280]) ).
fof(f541,plain,
~ spl19_11,
inference(avatar_contradiction_clause,[],[f540]) ).
fof(f567,plain,
! [X0,X1] :
( m1_subset_1(X0,u1_struct_0(sK0))
| m1_subset_1(X1,u1_struct_0(sK0))
| m1_subset_1(k5_lattices(sK0),u1_struct_0(sK0))
| r3_lattices(sK0,X1,X0)
| ~ r2_hidden(X1,k22_filter_2(sK0,k5_lattices(sK0),X0))
| v13_lattices(sK0)
| ~ v10_lattices(sK0)
| ~ v3_struct_0(sK0)
| m1_subset_1(X0,u1_struct_0(sK0))
| ~ l3_lattices(sK0) ),
inference(resolution,[],[f480,f270]) ).
fof(f570,plain,
! [X0,X1] :
( m1_subset_1(X0,u1_struct_0(sK0))
| m1_subset_1(X1,u1_struct_0(sK0))
| m1_subset_1(k5_lattices(sK0),u1_struct_0(sK0))
| r3_lattices(sK0,X1,X0)
| ~ r2_hidden(X1,k22_filter_2(sK0,k5_lattices(sK0),X0))
| v13_lattices(sK0)
| ~ v10_lattices(sK0)
| ~ v3_struct_0(sK0)
| ~ l3_lattices(sK0) ),
inference(duplicate_literal_removal,[],[f567]) ).
fof(f572,plain,
( ! [X0,X1] :
( m1_subset_1(X0,u1_struct_0(sK0))
| m1_subset_1(X1,u1_struct_0(sK0))
| r3_lattices(sK0,X1,X0)
| ~ r2_hidden(X1,k22_filter_2(sK0,k5_lattices(sK0),X0))
| v13_lattices(sK0)
| ~ v10_lattices(sK0)
| ~ v3_struct_0(sK0)
| ~ l3_lattices(sK0) )
| spl19_11 ),
inference(forward_subsumption_resolution,[],[f570,f527]) ).
fof(f574,plain,
( ! [X0,X1] :
( m1_subset_1(X0,u1_struct_0(sK0))
| m1_subset_1(X1,u1_struct_0(sK0))
| r3_lattices(sK0,X1,X0)
| ~ r2_hidden(X1,k22_filter_2(sK0,k5_lattices(sK0),X0))
| ~ v10_lattices(sK0)
| ~ v3_struct_0(sK0)
| ~ l3_lattices(sK0) )
| spl19_11 ),
inference(forward_subsumption_resolution,[],[f572,f209]) ).
fof(f576,plain,
( ! [X0,X1] :
( m1_subset_1(X0,u1_struct_0(sK0))
| m1_subset_1(X1,u1_struct_0(sK0))
| r3_lattices(sK0,X1,X0)
| ~ r2_hidden(X1,k22_filter_2(sK0,k5_lattices(sK0),X0))
| ~ v3_struct_0(sK0)
| ~ l3_lattices(sK0) )
| spl19_11 ),
inference(forward_subsumption_resolution,[],[f574,f128]) ).
fof(f578,plain,
( ! [X0,X1] :
( m1_subset_1(X0,u1_struct_0(sK0))
| m1_subset_1(X1,u1_struct_0(sK0))
| r3_lattices(sK0,X1,X0)
| ~ r2_hidden(X1,k22_filter_2(sK0,k5_lattices(sK0),X0))
| ~ l3_lattices(sK0) )
| spl19_11 ),
inference(forward_subsumption_resolution,[],[f576,f207]) ).
fof(f579,plain,
( ! [X0,X1] :
( ~ r2_hidden(X1,k22_filter_2(sK0,k5_lattices(sK0),X0))
| m1_subset_1(X1,u1_struct_0(sK0))
| r3_lattices(sK0,X1,X0)
| m1_subset_1(X0,u1_struct_0(sK0)) )
| spl19_11 ),
inference(forward_subsumption_resolution,[],[f578,f127]) ).
fof(f580,plain,
( $false
| ~ spl19_4
| spl19_11 ),
inference(forward_subsumption_resolution,[],[f512,f527]) ).
fof(f581,plain,
( ~ spl19_4
| spl19_11 ),
inference(avatar_contradiction_clause,[],[f580]) ).
fof(f612,definition,
( spl19_18
<=> m1_subset_1(sK2(u1_struct_0(sK0),k18_filter_2(sK0,sK1),k22_filter_2(sK0,k5_lattices(sK0),sK1)),u1_struct_0(sK0)) ),
introduced(definition,[new_symbols(definition,[spl19_18])],[avatar_definition]) ).
fof(f613,plain,
( ~ m1_subset_1(sK2(u1_struct_0(sK0),k18_filter_2(sK0,sK1),k22_filter_2(sK0,k5_lattices(sK0),sK1)),u1_struct_0(sK0))
| spl19_18 ),
inference(avatar_component_clause,[],[f612]) ).
fof(f614,plain,
( m1_subset_1(sK2(u1_struct_0(sK0),k18_filter_2(sK0,sK1),k22_filter_2(sK0,k5_lattices(sK0),sK1)),u1_struct_0(sK0))
| ~ spl19_18 ),
inference(avatar_component_clause,[],[f612]) ).
fof(f616,definition,
( spl19_19
<=> r3_lattices(sK0,sK2(u1_struct_0(sK0),k18_filter_2(sK0,sK1),k22_filter_2(sK0,k5_lattices(sK0),sK1)),sK1) ),
introduced(definition,[new_symbols(definition,[spl19_19])],[avatar_definition]) ).
fof(f618,plain,
( r3_lattices(sK0,sK2(u1_struct_0(sK0),k18_filter_2(sK0,sK1),k22_filter_2(sK0,k5_lattices(sK0),sK1)),sK1)
| ~ spl19_19 ),
inference(avatar_component_clause,[],[f616]) ).
fof(f640,plain,
( m1_subset_1(sK1,u1_struct_0(sK0))
| r3_lattices(sK0,sK2(u1_struct_0(sK0),k18_filter_2(sK0,sK1),k22_filter_2(sK0,k5_lattices(sK0),sK1)),sK1)
| m1_subset_1(sK2(u1_struct_0(sK0),k18_filter_2(sK0,sK1),k22_filter_2(sK0,k5_lattices(sK0),sK1)),u1_struct_0(sK0))
| ~ spl19_9 ),
inference(resolution,[],[f454,f408]) ).
fof(f649,plain,
( r3_lattices(sK0,sK2(u1_struct_0(sK0),k18_filter_2(sK0,sK1),k22_filter_2(sK0,k5_lattices(sK0),sK1)),sK1)
| m1_subset_1(sK2(u1_struct_0(sK0),k18_filter_2(sK0,sK1),k22_filter_2(sK0,k5_lattices(sK0),sK1)),u1_struct_0(sK0))
| ~ spl19_9 ),
inference(forward_subsumption_resolution,[],[f640,f210]) ).
fof(f650,plain,
( spl19_18
| spl19_19
| ~ spl19_9 ),
inference(avatar_split_clause,[],[f649,f452,f616,f612]) ).
fof(f658,plain,
( m1_subset_1(k22_filter_2(sK0,k5_lattices(sK0),sK1),k1_zfmisc_1(u1_struct_0(sK0)))
| m1_subset_1(k18_filter_2(sK0,sK1),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ r2_hidden(sK2(u1_struct_0(sK0),k18_filter_2(sK0,sK1),k22_filter_2(sK0,k5_lattices(sK0),sK1)),k18_filter_2(sK0,sK1))
| ~ r1_filter_2(u1_struct_0(sK0),k18_filter_2(sK0,sK1),k22_filter_2(sK0,k5_lattices(sK0),sK1))
| ~ spl19_10 ),
inference(resolution,[],[f458,f445]) ).
fof(f659,plain,
( m1_subset_1(k18_filter_2(sK0,sK1),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ r2_hidden(sK2(u1_struct_0(sK0),k18_filter_2(sK0,sK1),k22_filter_2(sK0,k5_lattices(sK0),sK1)),k18_filter_2(sK0,sK1))
| ~ r1_filter_2(u1_struct_0(sK0),k18_filter_2(sK0,sK1),k22_filter_2(sK0,k5_lattices(sK0),sK1))
| spl19_4
| ~ spl19_10 ),
inference(forward_subsumption_resolution,[],[f658,f369]) ).
fof(f665,plain,
( ~ r2_hidden(sK2(u1_struct_0(sK0),k18_filter_2(sK0,sK1),k22_filter_2(sK0,k5_lattices(sK0),sK1)),k18_filter_2(sK0,sK1))
| ~ r1_filter_2(u1_struct_0(sK0),k18_filter_2(sK0,sK1),k22_filter_2(sK0,k5_lattices(sK0),sK1))
| spl19_1
| spl19_4
| ~ spl19_10 ),
inference(forward_subsumption_resolution,[],[f659,f357]) ).
fof(f679,plain,
! [X0,X1] :
( m1_subset_1(X0,u1_struct_0(sK0))
| m1_subset_1(X1,u1_struct_0(sK0))
| ~ r3_lattices(sK0,k5_lattices(sK0),X0)
| ~ r3_lattices(sK0,X1,X0)
| m1_subset_1(k5_lattices(sK0),u1_struct_0(sK0))
| r2_hidden(X1,k22_filter_2(sK0,k5_lattices(sK0),X0))
| v13_lattices(sK0)
| ~ v10_lattices(sK0)
| ~ v3_struct_0(sK0)
| m1_subset_1(X1,u1_struct_0(sK0))
| ~ l3_lattices(sK0) ),
inference(resolution,[],[f483,f270]) ).
fof(f682,plain,
! [X0,X1] :
( m1_subset_1(X0,u1_struct_0(sK0))
| m1_subset_1(X1,u1_struct_0(sK0))
| ~ r3_lattices(sK0,k5_lattices(sK0),X0)
| ~ r3_lattices(sK0,X1,X0)
| m1_subset_1(k5_lattices(sK0),u1_struct_0(sK0))
| r2_hidden(X1,k22_filter_2(sK0,k5_lattices(sK0),X0))
| v13_lattices(sK0)
| ~ v10_lattices(sK0)
| ~ v3_struct_0(sK0)
| ~ l3_lattices(sK0) ),
inference(duplicate_literal_removal,[],[f679]) ).
fof(f684,plain,
! [X0,X1] :
( m1_subset_1(X0,u1_struct_0(sK0))
| m1_subset_1(X1,u1_struct_0(sK0))
| ~ r3_lattices(sK0,X1,X0)
| m1_subset_1(k5_lattices(sK0),u1_struct_0(sK0))
| r2_hidden(X1,k22_filter_2(sK0,k5_lattices(sK0),X0))
| v13_lattices(sK0)
| ~ v10_lattices(sK0)
| ~ v3_struct_0(sK0)
| ~ l3_lattices(sK0) ),
inference(forward_subsumption_resolution,[],[f682,f270]) ).
fof(f686,plain,
( ! [X0,X1] :
( m1_subset_1(X0,u1_struct_0(sK0))
| m1_subset_1(X1,u1_struct_0(sK0))
| ~ r3_lattices(sK0,X1,X0)
| r2_hidden(X1,k22_filter_2(sK0,k5_lattices(sK0),X0))
| v13_lattices(sK0)
| ~ v10_lattices(sK0)
| ~ v3_struct_0(sK0)
| ~ l3_lattices(sK0) )
| spl19_11 ),
inference(forward_subsumption_resolution,[],[f684,f527]) ).
fof(f688,plain,
( ! [X0,X1] :
( m1_subset_1(X0,u1_struct_0(sK0))
| m1_subset_1(X1,u1_struct_0(sK0))
| ~ r3_lattices(sK0,X1,X0)
| r2_hidden(X1,k22_filter_2(sK0,k5_lattices(sK0),X0))
| ~ v10_lattices(sK0)
| ~ v3_struct_0(sK0)
| ~ l3_lattices(sK0) )
| spl19_11 ),
inference(forward_subsumption_resolution,[],[f686,f209]) ).
fof(f690,plain,
( ! [X0,X1] :
( m1_subset_1(X0,u1_struct_0(sK0))
| m1_subset_1(X1,u1_struct_0(sK0))
| ~ r3_lattices(sK0,X1,X0)
| r2_hidden(X1,k22_filter_2(sK0,k5_lattices(sK0),X0))
| ~ v3_struct_0(sK0)
| ~ l3_lattices(sK0) )
| spl19_11 ),
inference(forward_subsumption_resolution,[],[f688,f128]) ).
fof(f691,plain,
( ! [X0,X1] :
( m1_subset_1(X0,u1_struct_0(sK0))
| m1_subset_1(X1,u1_struct_0(sK0))
| ~ r3_lattices(sK0,X1,X0)
| r2_hidden(X1,k22_filter_2(sK0,k5_lattices(sK0),X0))
| ~ l3_lattices(sK0) )
| spl19_11 ),
inference(forward_subsumption_resolution,[],[f690,f207]) ).
fof(f692,plain,
( ! [X0,X1] :
( ~ r3_lattices(sK0,X1,X0)
| m1_subset_1(X1,u1_struct_0(sK0))
| m1_subset_1(X0,u1_struct_0(sK0))
| r2_hidden(X1,k22_filter_2(sK0,k5_lattices(sK0),X0)) )
| spl19_11 ),
inference(forward_subsumption_resolution,[],[f691,f127]) ).
fof(f742,plain,
( ~ r2_hidden(sK2(u1_struct_0(sK0),k18_filter_2(sK0,sK1),k22_filter_2(sK0,k5_lattices(sK0),sK1)),k18_filter_2(sK0,sK1))
| spl19_1
| spl19_4
| ~ spl19_10 ),
inference(forward_subsumption_resolution,[],[f665,f208]) ).
fof(f746,plain,
( ~ spl19_9
| spl19_1
| spl19_4
| ~ spl19_10 ),
inference(avatar_split_clause,[],[f742,f456,f368,f356,f452]) ).
fof(f1195,plain,
( m1_subset_1(k18_filter_2(sK0,sK1),k1_zfmisc_1(u1_struct_0(sK0)))
| m1_subset_1(k22_filter_2(sK0,k5_lattices(sK0),sK1),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ v1_xboole_0(u1_struct_0(sK0))
| ~ r1_filter_2(u1_struct_0(sK0),k18_filter_2(sK0,sK1),k22_filter_2(sK0,k5_lattices(sK0),sK1))
| ~ spl19_18 ),
inference(resolution,[],[f614,f218]) ).
fof(f1197,plain,
( m1_subset_1(k22_filter_2(sK0,k5_lattices(sK0),sK1),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ v1_xboole_0(u1_struct_0(sK0))
| ~ r1_filter_2(u1_struct_0(sK0),k18_filter_2(sK0,sK1),k22_filter_2(sK0,k5_lattices(sK0),sK1))
| spl19_1
| ~ spl19_18 ),
inference(forward_subsumption_resolution,[],[f1195,f357]) ).
fof(f1198,plain,
( ~ v1_xboole_0(u1_struct_0(sK0))
| ~ r1_filter_2(u1_struct_0(sK0),k18_filter_2(sK0,sK1),k22_filter_2(sK0,k5_lattices(sK0),sK1))
| spl19_1
| spl19_4
| ~ spl19_18 ),
inference(forward_subsumption_resolution,[],[f1197,f369]) ).
fof(f1199,plain,
( ~ r1_filter_2(u1_struct_0(sK0),k18_filter_2(sK0,sK1),k22_filter_2(sK0,k5_lattices(sK0),sK1))
| spl19_1
| ~ spl19_3
| spl19_4
| ~ spl19_18 ),
inference(forward_subsumption_resolution,[],[f1198,f365]) ).
fof(f1200,plain,
( $false
| spl19_1
| ~ spl19_3
| spl19_4
| ~ spl19_18 ),
inference(forward_subsumption_resolution,[],[f1199,f208]) ).
fof(f1201,plain,
( spl19_1
| ~ spl19_3
| spl19_4
| ~ spl19_18 ),
inference(avatar_contradiction_clause,[],[f1200]) ).
fof(f1487,plain,
( m1_subset_1(sK2(u1_struct_0(sK0),k18_filter_2(sK0,sK1),k22_filter_2(sK0,k5_lattices(sK0),sK1)),u1_struct_0(sK0))
| r3_lattices(sK0,sK2(u1_struct_0(sK0),k18_filter_2(sK0,sK1),k22_filter_2(sK0,k5_lattices(sK0),sK1)),sK1)
| m1_subset_1(sK1,u1_struct_0(sK0))
| ~ spl19_10
| spl19_11 ),
inference(resolution,[],[f579,f458]) ).
fof(f1505,plain,
( r3_lattices(sK0,sK2(u1_struct_0(sK0),k18_filter_2(sK0,sK1),k22_filter_2(sK0,k5_lattices(sK0),sK1)),sK1)
| m1_subset_1(sK1,u1_struct_0(sK0))
| ~ spl19_10
| spl19_11
| spl19_18 ),
inference(forward_subsumption_resolution,[],[f1487,f613]) ).
fof(f1515,plain,
( r3_lattices(sK0,sK2(u1_struct_0(sK0),k18_filter_2(sK0,sK1),k22_filter_2(sK0,k5_lattices(sK0),sK1)),sK1)
| ~ spl19_10
| spl19_11
| spl19_18 ),
inference(forward_subsumption_resolution,[],[f1505,f210]) ).
fof(f1516,plain,
( spl19_19
| ~ spl19_10
| spl19_11
| spl19_18 ),
inference(avatar_split_clause,[],[f1515,f612,f526,f456,f616]) ).
fof(f1520,plain,
( m1_subset_1(sK1,u1_struct_0(sK0))
| m1_subset_1(sK2(u1_struct_0(sK0),k18_filter_2(sK0,sK1),k22_filter_2(sK0,k5_lattices(sK0),sK1)),u1_struct_0(sK0))
| r2_hidden(sK2(u1_struct_0(sK0),k18_filter_2(sK0,sK1),k22_filter_2(sK0,k5_lattices(sK0),sK1)),k18_filter_2(sK0,sK1))
| ~ spl19_19 ),
inference(resolution,[],[f618,f444]) ).
fof(f1523,plain,
( m1_subset_1(sK2(u1_struct_0(sK0),k18_filter_2(sK0,sK1),k22_filter_2(sK0,k5_lattices(sK0),sK1)),u1_struct_0(sK0))
| r2_hidden(sK2(u1_struct_0(sK0),k18_filter_2(sK0,sK1),k22_filter_2(sK0,k5_lattices(sK0),sK1)),k18_filter_2(sK0,sK1))
| ~ spl19_19 ),
inference(forward_subsumption_resolution,[],[f1520,f210]) ).
fof(f1528,plain,
( r2_hidden(sK2(u1_struct_0(sK0),k18_filter_2(sK0,sK1),k22_filter_2(sK0,k5_lattices(sK0),sK1)),k18_filter_2(sK0,sK1))
| spl19_18
| ~ spl19_19 ),
inference(forward_subsumption_resolution,[],[f1523,f613]) ).
fof(f1538,plain,
( spl19_9
| spl19_18
| ~ spl19_19 ),
inference(avatar_split_clause,[],[f1528,f616,f612,f452]) ).
fof(f1583,plain,
( m1_subset_1(sK2(u1_struct_0(sK0),k18_filter_2(sK0,sK1),k22_filter_2(sK0,k5_lattices(sK0),sK1)),u1_struct_0(sK0))
| m1_subset_1(sK1,u1_struct_0(sK0))
| r2_hidden(sK2(u1_struct_0(sK0),k18_filter_2(sK0,sK1),k22_filter_2(sK0,k5_lattices(sK0),sK1)),k22_filter_2(sK0,k5_lattices(sK0),sK1))
| spl19_11
| ~ spl19_19 ),
inference(resolution,[],[f692,f618]) ).
fof(f1593,plain,
( m1_subset_1(sK1,u1_struct_0(sK0))
| r2_hidden(sK2(u1_struct_0(sK0),k18_filter_2(sK0,sK1),k22_filter_2(sK0,k5_lattices(sK0),sK1)),k22_filter_2(sK0,k5_lattices(sK0),sK1))
| spl19_11
| spl19_18
| ~ spl19_19 ),
inference(forward_subsumption_resolution,[],[f1583,f613]) ).
fof(f1597,plain,
( r2_hidden(sK2(u1_struct_0(sK0),k18_filter_2(sK0,sK1),k22_filter_2(sK0,k5_lattices(sK0),sK1)),k22_filter_2(sK0,k5_lattices(sK0),sK1))
| spl19_11
| spl19_18
| ~ spl19_19 ),
inference(forward_subsumption_resolution,[],[f1593,f210]) ).
fof(f1600,plain,
( $false
| spl19_10
| spl19_11
| spl19_18
| ~ spl19_19 ),
inference(forward_subsumption_resolution,[],[f1597,f457]) ).
fof(f1601,plain,
( spl19_10
| spl19_11
| spl19_18
| ~ spl19_19 ),
inference(avatar_contradiction_clause,[],[f1600]) ).
cnf(s2,plain,
spl19_3,
inference(sat_conversion,[],[f380]) ).
cnf(s5,plain,
( spl19_1
| ~ spl19_3
| spl19_4
| spl19_9
| spl19_10 ),
inference(sat_conversion,[],[f459]) ).
cnf(s6,plain,
~ spl19_1,
inference(sat_conversion,[],[f470]) ).
cnf(s8,plain,
~ spl19_11,
inference(sat_conversion,[],[f541]) ).
cnf(s10,plain,
( ~ spl19_4
| spl19_11 ),
inference(sat_conversion,[],[f581]) ).
cnf(s23,plain,
( ~ spl19_9
| spl19_18
| spl19_19 ),
inference(sat_conversion,[],[f650]) ).
cnf(s33,plain,
( spl19_1
| spl19_4
| ~ spl19_9
| ~ spl19_10 ),
inference(sat_conversion,[],[f746]) ).
cnf(s62,plain,
( spl19_1
| ~ spl19_3
| spl19_4
| ~ spl19_18 ),
inference(sat_conversion,[],[f1201]) ).
cnf(s86,plain,
( ~ spl19_10
| spl19_11
| spl19_18
| spl19_19 ),
inference(sat_conversion,[],[f1516]) ).
cnf(s91,plain,
( spl19_9
| spl19_18
| ~ spl19_19 ),
inference(sat_conversion,[],[f1538]) ).
cnf(s97,plain,
( spl19_10
| spl19_11
| spl19_18
| ~ spl19_19 ),
inference(sat_conversion,[],[f1601]) ).
cnf(s109,plain,
~ spl19_4,
inference(rat,[],[s10,s8]) ).
cnf(s113,plain,
( ~ spl19_3
| spl19_9
| spl19_10 ),
inference(rat,[],[s5,s109,s6]) ).
cnf(s114,plain,
~ spl19_18,
inference(rat,[],[s62,s6,s109,s2]) ).
cnf(s117,plain,
spl19_9,
inference(rat,[],[s86,s113,s91,s8,s114,s2]) ).
cnf(s118,plain,
spl19_19,
inference(rat,[],[s23,s114,s117]) ).
cnf(s121,plain,
~ spl19_10,
inference(rat,[],[s33,s6,s109,s117]) ).
cnf(s122,plain,
$false,
inference(rat,[],[s97,s114,s8,s118,s121]) ).
fof(f1605,plain,
$false,
inference(avatar_sat_refutation,[],[s122]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT330+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.36 % Computer : n004.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sun Sep 27 14:41:36 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.39 Running first-order model finding
% 0.10/0.39 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.44/0.49 % (3593464)Will run a generic schedule for satisfiability detection.
% 0.44/0.49 % (3593475)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1258401162:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.44/0.49 % (3593470)% WARNING: option uhcvi not known.
% 0.44/0.49 % (3593469)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=21182715_2999 on theBenchmark for (2999ds/0Mi)
% 0.44/0.49 % (3593473)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=331091427:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.44/0.49 % (3593471)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=385016038:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.44/0.49 % (3593472)dis+10_1_sil=32000:sp=arity:random_seed=2539318641:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.44/0.49 % (3593474)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1868331118:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.44/0.49 % (3593470)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3298581217:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.44/0.49 % TRYING [1]
% 0.44/0.49 % TRYING [2]
% 0.44/0.49 % TRYING [3]
% 0.44/0.49 % TRYING [4]
% 0.44/0.49 % TRYING [5]
% 0.44/0.49 % (3593470) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3593464-3593470"...
% 0.44/0.49 % (3593470)...printing done.
% 0.44/0.49 % (3593470)Refutation found. Thanks to Tanya!
% 0.44/0.49 % SZS status Theorem for theBenchmark
% 0.44/0.49 % SZS output start Proof for theBenchmark
% See solution above
% 0.44/0.49 % (3593470)------------------------------
% 0.44/0.49 % (3593470)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.44/0.49 % (3593470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.44/0.49 % (3593470)CaDiCaL version: 2.1.3
% 0.44/0.49 % (3593470)Termination reason: Refutation
% 0.44/0.49 % (3593470)Time elapsed: 0.048 s
% 0.44/0.49 % (3593470)Peak memory usage: 13 MB
% 0.44/0.49 % (3593470)Instructions burned: 67 (million)
% 0.44/0.49 % (3593464)Success in time 0.085 s
% 0.44/0.49 % Vampire exiting
%------------------------------------------------------------------------------