%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT330+4 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n007.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:47:01 AM UTC 2026
% Result : Theorem 18.63s 9.08s
% Output : Refutation 39.64s
% Verified :
% SZS Type : Refutation
% Derivation depth : 39
% Number of leaves : 38
% Syntax : Number of formulae : 302 ( 31 unt; 12 def)
% Number of atoms : 1367 ( 55 equ)
% Maximal formula atoms : 14 ( 4 avg)
% Number of connectives : 1802 ( 737 ~; 839 |; 155 &)
% ( 26 <=>; 45 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 37 ( 35 usr; 12 prp; 0-3 aty)
% Number of functors : 14 ( 14 usr; 2 con; 0-3 aty)
% Number of variables : 323 ( 0 sgn 317 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f8,axiom,
! [X0,X1] :
( r1_tarski(X0,X1)
<=> ! [X2] :
( r2_hidden(X2,X0)
=> r2_hidden(X2,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d3_tarski) ).
fof(f38,axiom,
! [X0,X1] :
( X0 = X1
<=> ( r1_tarski(X0,X1)
& r1_tarski(X1,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d10_xboole_0) ).
fof(f678,axiom,
! [X0,X1,X2] :
( ( r2_hidden(X0,X1)
& m1_subset_1(X1,k1_zfmisc_1(X2)) )
=> m1_subset_1(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t4_subset) ).
fof(f18191,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v13_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> k4_lattices(X0,k5_lattices(X0),X1) = k5_lattices(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t40_lattices) ).
fof(f18192,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(f18210,axiom,
! [X0] :
( l3_lattices(X0)
=> ( l1_lattices(X0)
& l2_lattices(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l3_lattices) ).
fof(f18225,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(f21600,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_filter_0(X1,X0)
=> ( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m1_filter_0) ).
fof(f22747,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l3_lattices(X0) )
=> ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_lattice2) ).
fof(f22752,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v4_lattices(k1_lattice2(X0))
& v5_lattices(k1_lattice2(X0))
& v6_lattices(k1_lattice2(X0))
& v7_lattices(k1_lattice2(X0))
& v8_lattices(k1_lattice2(X0))
& v9_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc6_lattice2) ).
fof(f22780,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l3_lattices(X0) )
=> ( u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0))
& u2_lattices(X0) = u1_lattices(k1_lattice2(X0))
& u1_lattices(X0) = u2_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t18_lattice2) ).
fof(f22852,axiom,
! [X0] :
( l3_lattices(X0)
=> ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k1_lattice2) ).
fof(f31985,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(f34607,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_filter_2(X1,X0)
<=> m1_filter_0(X1,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_m1_filter_2) ).
fof(f34608,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(f34612,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/sandbox/benchmark/theBenchmark.p',redefinition_r1_filter_2) ).
fof(f34615,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& m1_subset_1(X1,u1_struct_0(X0)) )
=> m1_filter_2(k2_filter_2(X0,X1),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k2_filter_2) ).
fof(f34642,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(f34647,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(f34671,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> k5_filter_2(X0,X1) = X1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d4_filter_2) ).
fof(f34687,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> m2_filter_2(u1_struct_0(X0),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t28_filter_2) ).
fof(f34690,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(f34691,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ( k18_filter_2(X0,X1) = k2_filter_2(k1_lattice2(X0),k5_filter_2(X0,X1))
& k18_filter_2(k1_lattice2(X0),k5_filter_2(X0,X1)) = k2_filter_2(X0,X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t30_filter_2) ).
fof(f34692,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,X1))
& r2_hidden(k4_lattices(X0,X1,X2),k18_filter_2(X0,X1))
& r2_hidden(k4_lattices(X0,X2,X1),k18_filter_2(X0,X1)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t31_filter_2) ).
fof(f34734,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(f34738,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(f34739,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)],[f34738]) ).
fof(f35030,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,[],[f34739]) ).
fof(f35031,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,[],[f35030]) ).
fof(f35074,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,[],[f18192]) ).
fof(f35075,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,[],[f35074]) ).
fof(f35076,plain,
! [X0] :
( ! [X1] :
( k4_lattices(X0,k5_lattices(X0),X1) = k5_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v13_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f18191]) ).
fof(f35077,plain,
! [X0] :
( ! [X1] :
( k4_lattices(X0,k5_lattices(X0),X1) = k5_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v13_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35076]) ).
fof(f35107,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,[],[f34612]) ).
fof(f35108,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,[],[f35107]) ).
fof(f35147,plain,
! [X0] :
( m1_subset_1(k5_lattices(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_lattices(X0) ),
inference(ennf_transformation,[],[f18225]) ).
fof(f35148,plain,
! [X0] :
( m1_subset_1(k5_lattices(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_lattices(X0) ),
inference(flattening,[],[f35147]) ).
fof(f35159,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( r2_hidden(X1,k18_filter_2(X0,X1))
& r2_hidden(k4_lattices(X0,X1,X2),k18_filter_2(X0,X1))
& r2_hidden(k4_lattices(X0,X2,X1),k18_filter_2(X0,X1)) )
| ~ 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,[],[f34692]) ).
fof(f35160,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( r2_hidden(X1,k18_filter_2(X0,X1))
& r2_hidden(k4_lattices(X0,X1,X2),k18_filter_2(X0,X1))
& r2_hidden(k4_lattices(X0,X2,X1),k18_filter_2(X0,X1)) )
| ~ 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,[],[f35159]) ).
fof(f35161,plain,
! [X0] :
( ! [X1] :
( ( k18_filter_2(X0,X1) = k2_filter_2(k1_lattice2(X0),k5_filter_2(X0,X1))
& k18_filter_2(k1_lattice2(X0),k5_filter_2(X0,X1)) = k2_filter_2(X0,X1) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f34691]) ).
fof(f35162,plain,
! [X0] :
( ! [X1] :
( ( k18_filter_2(X0,X1) = k2_filter_2(k1_lattice2(X0),k5_filter_2(X0,X1))
& k18_filter_2(k1_lattice2(X0),k5_filter_2(X0,X1)) = k2_filter_2(X0,X1) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35161]) ).
fof(f35163,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,[],[f34690]) ).
fof(f35164,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,[],[f35163]) ).
fof(f35165,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,[],[f34642]) ).
fof(f35166,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,[],[f35165]) ).
fof(f35171,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,[],[f34734]) ).
fof(f35172,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,[],[f35171]) ).
fof(f35173,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,[],[f34647]) ).
fof(f35174,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,[],[f35173]) ).
fof(f35182,plain,
! [X0,X1,X2] :
( m1_subset_1(X0,X2)
| ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2)) ),
inference(ennf_transformation,[],[f678]) ).
fof(f35183,plain,
! [X0,X1,X2] :
( m1_subset_1(X0,X2)
| ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2)) ),
inference(flattening,[],[f35182]) ).
fof(f35196,plain,
! [X0,X1] :
( r1_tarski(X0,X1)
<=> ! [X2] :
( r2_hidden(X2,X1)
| ~ r2_hidden(X2,X0) ) ),
inference(ennf_transformation,[],[f8]) ).
fof(f35238,plain,
! [X0] :
( m2_filter_2(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f34687]) ).
fof(f35239,plain,
! [X0] :
( m2_filter_2(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35238]) ).
fof(f35254,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,[],[f34608]) ).
fof(f35255,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,[],[f35254]) ).
fof(f35299,plain,
! [X0] :
( ( u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0))
& u2_lattices(X0) = u1_lattices(k1_lattice2(X0))
& u1_lattices(X0) = u2_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f22780]) ).
fof(f35300,plain,
! [X0] :
( ( u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0))
& u2_lattices(X0) = u1_lattices(k1_lattice2(X0))
& u1_lattices(X0) = u2_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35299]) ).
fof(f35694,plain,
! [X0] :
( ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f22852]) ).
fof(f35701,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v4_lattices(k1_lattice2(X0))
& v5_lattices(k1_lattice2(X0))
& v6_lattices(k1_lattice2(X0))
& v7_lattices(k1_lattice2(X0))
& v8_lattices(k1_lattice2(X0))
& v9_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f22752]) ).
fof(f35702,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v4_lattices(k1_lattice2(X0))
& v5_lattices(k1_lattice2(X0))
& v6_lattices(k1_lattice2(X0))
& v7_lattices(k1_lattice2(X0))
& v8_lattices(k1_lattice2(X0))
& v9_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35701]) ).
fof(f35703,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f22747]) ).
fof(f35704,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35703]) ).
fof(f36322,plain,
! [X0] :
( ( l1_lattices(X0)
& l2_lattices(X0) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f18210]) ).
fof(f36339,plain,
! [X0,X1] :
( m1_filter_2(k2_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,[],[f34615]) ).
fof(f36340,plain,
! [X0,X1] :
( m1_filter_2(k2_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,[],[f36339]) ).
fof(f36351,plain,
! [X0] :
( ! [X1] :
( k5_filter_2(X0,X1) = X1
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f34671]) ).
fof(f36352,plain,
! [X0] :
( ! [X1] :
( k5_filter_2(X0,X1) = X1
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f36351]) ).
fof(f36363,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,[],[f31985]) ).
fof(f36364,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,[],[f36363]) ).
fof(f37532,plain,
! [X0] :
( ! [X1] :
( ( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f21600]) ).
fof(f37533,plain,
! [X0] :
( ! [X1] :
( ( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f37532]) ).
fof(f42415,plain,
! [X0] :
( ! [X1] :
( m1_filter_2(X1,X0)
<=> m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f34607]) ).
fof(f42416,plain,
! [X0] :
( ! [X1] :
( m1_filter_2(X1,X0)
<=> m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f42415]) ).
fof(f42458,definition,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v4_lattices(k1_lattice2(X0))
& v5_lattices(k1_lattice2(X0))
& v6_lattices(k1_lattice2(X0))
& v7_lattices(k1_lattice2(X0))
& v8_lattices(k1_lattice2(X0))
& v9_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0)) )
| ~ sP9(X0) ),
introduced(definition,[new_symbols(definition,[sP9])],[predicate_definition_introduction]) ).
fof(f42459,plain,
! [X0] :
( sP9(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(definition_folding,[],[f35702,f42458]) ).
fof(f42786,plain,
( ~ r1_filter_2(u1_struct_0(sK230),k18_filter_2(sK230,sK231),k22_filter_2(sK230,k5_lattices(sK230),sK231))
& v13_lattices(sK230)
& m1_subset_1(sK231,u1_struct_0(sK230))
& ~ v3_struct_0(sK230)
& v10_lattices(sK230)
& l3_lattices(sK230) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK230,sK231]),skolemize(X0,sK230),skolemize(X1,sK231)],[f35031]) ).
fof(f42807,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,[],[f35108]) ).
fof(f42818,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,[],[f35164]) ).
fof(f42819,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,[],[f35172]) ).
fof(f42820,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,[],[f42819]) ).
fof(f42838,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,[],[f35196]) ).
fof(f42839,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,[],[f42838]) ).
fof(f42840,plain,
! [X0,X1] :
( ( r1_tarski(X0,X1)
| ( ~ r2_hidden(sK249(X0,X1),X1)
& r2_hidden(sK249(X0,X1),X0) ) )
& ( ! [X3] :
( r2_hidden(X3,X1)
| ~ r2_hidden(X3,X0) )
| ~ r1_tarski(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK249]),skolemize(X2,sK249(X0,X1))],[f42839]) ).
fof(f42964,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v4_lattices(k1_lattice2(X0))
& v5_lattices(k1_lattice2(X0))
& v6_lattices(k1_lattice2(X0))
& v7_lattices(k1_lattice2(X0))
& v8_lattices(k1_lattice2(X0))
& v9_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0)) )
| ~ sP9(X0) ),
inference(nnf_transformation,[],[f42458]) ).
fof(f43116,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(f43117,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,[],[f43116]) ).
fof(f45436,plain,
! [X0] :
( ! [X1] :
( ( m1_filter_2(X1,X0)
| ~ m1_filter_0(X1,X0) )
& ( m1_filter_0(X1,X0)
| ~ m1_filter_2(X1,X0) ) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f42416]) ).
fof(f45440,plain,
l3_lattices(sK230),
inference(cnf_transformation,[],[f42786]) ).
fof(f45441,plain,
v10_lattices(sK230),
inference(cnf_transformation,[],[f42786]) ).
fof(f45442,plain,
~ v3_struct_0(sK230),
inference(cnf_transformation,[],[f42786]) ).
fof(f45443,plain,
m1_subset_1(sK231,u1_struct_0(sK230)),
inference(cnf_transformation,[],[f42786]) ).
fof(f45444,plain,
v13_lattices(sK230),
inference(cnf_transformation,[],[f42786]) ).
fof(f45445,plain,
~ r1_filter_2(u1_struct_0(sK230),k18_filter_2(sK230,sK231),k22_filter_2(sK230,k5_lattices(sK230),sK231)),
inference(cnf_transformation,[],[f42786]) ).
fof(f45501,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,[],[f35075]) ).
fof(f45502,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u1_struct_0(X0))
| k5_lattices(X0) = k4_lattices(X0,k5_lattices(X0),X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v13_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35077]) ).
fof(f45549,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,[],[f42807]) ).
fof(f45577,plain,
! [X0] :
( m1_subset_1(k5_lattices(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_lattices(X0) ),
inference(cnf_transformation,[],[f35148]) ).
fof(f45587,plain,
! [X2,X0,X1] :
( r2_hidden(k4_lattices(X0,X2,X1),k18_filter_2(X0,X1))
| ~ 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,[],[f35160]) ).
fof(f45591,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u1_struct_0(X0))
| k18_filter_2(X0,X1) = k2_filter_2(k1_lattice2(X0),k5_filter_2(X0,X1))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35162]) ).
fof(f45592,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,[],[f42818]) ).
fof(f45593,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,[],[f42818]) ).
fof(f45594,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,[],[f35166]) ).
fof(f45598,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,[],[f42820]) ).
fof(f45600,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,[],[f42820]) ).
fof(f45601,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,[],[f35174]) ).
fof(f45614,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ r2_hidden(X0,X1)
| m1_subset_1(X0,X2) ),
inference(cnf_transformation,[],[f35183]) ).
fof(f45636,plain,
! [X0,X1] :
( r2_hidden(sK249(X0,X1),X0)
| r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f42840]) ).
fof(f45637,plain,
! [X0,X1] :
( ~ r2_hidden(sK249(X0,X1),X1)
| r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f42840]) ).
fof(f45689,plain,
! [X0] :
( m2_filter_2(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35239]) ).
fof(f45722,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,[],[f35255]) ).
fof(f45723,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,[],[f35255]) ).
fof(f45763,plain,
! [X0] :
( ~ l3_lattices(X0)
| v3_struct_0(X0)
| u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0)) ),
inference(cnf_transformation,[],[f35300]) ).
fof(f46253,plain,
! [X0] :
( l3_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35694]) ).
fof(f46260,plain,
! [X0] :
( v10_lattices(k1_lattice2(X0))
| ~ sP9(X0) ),
inference(cnf_transformation,[],[f42964]) ).
fof(f46269,plain,
! [X0] :
( ~ v10_lattices(X0)
| v3_struct_0(X0)
| sP9(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f42459]) ).
fof(f46271,plain,
! [X0] :
( ~ v3_struct_0(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35704]) ).
fof(f47065,plain,
! [X0,X1] :
( ~ r1_tarski(X1,X0)
| ~ r1_tarski(X0,X1)
| X0 = X1 ),
inference(cnf_transformation,[],[f43117]) ).
fof(f47367,plain,
! [X0] :
( ~ l3_lattices(X0)
| l1_lattices(X0) ),
inference(cnf_transformation,[],[f36322]) ).
fof(f47401,plain,
! [X0,X1] :
( m1_filter_2(k2_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,[],[f36340]) ).
fof(f47415,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u1_struct_0(X0))
| k5_filter_2(X0,X1) = X1
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f36352]) ).
fof(f47430,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,[],[f36364]) ).
fof(f49131,plain,
! [X0,X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m1_filter_0(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f37533]) ).
fof(f56307,plain,
! [X0,X1] :
( ~ m1_filter_2(X1,X0)
| m1_filter_0(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f45436]) ).
fof(f57558,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,[],[f45549]) ).
fof(f58562,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,[],[f57558]) ).
fof(f59659,plain,
( k18_filter_2(sK230,sK231) = k2_filter_2(k1_lattice2(sK230),k5_filter_2(sK230,sK231))
| v3_struct_0(sK230)
| ~ v10_lattices(sK230)
| ~ l3_lattices(sK230) ),
inference(resolution,[],[f45591,f45443]) ).
fof(f59660,plain,
( k18_filter_2(sK230,sK231) = k2_filter_2(k1_lattice2(sK230),k5_filter_2(sK230,sK231))
| ~ v10_lattices(sK230)
| ~ l3_lattices(sK230) ),
inference(forward_subsumption_resolution,[],[f59659,f45442]) ).
fof(f59661,plain,
( k18_filter_2(sK230,sK231) = k2_filter_2(k1_lattice2(sK230),k5_filter_2(sK230,sK231))
| ~ l3_lattices(sK230) ),
inference(forward_subsumption_resolution,[],[f59660,f45441]) ).
fof(f59662,plain,
k18_filter_2(sK230,sK231) = k2_filter_2(k1_lattice2(sK230),k5_filter_2(sK230,sK231)),
inference(forward_subsumption_resolution,[],[f59661,f45440]) ).
fof(f59720,definition,
( spl1775_75
<=> m2_filter_2(k18_filter_2(sK230,sK231),sK230) ),
introduced(definition,[new_symbols(definition,[spl1775_75])],[avatar_definition]) ).
fof(f59721,plain,
( m2_filter_2(k18_filter_2(sK230,sK231),sK230)
| ~ spl1775_75 ),
inference(avatar_component_clause,[],[f59720]) ).
fof(f59722,plain,
( ~ m2_filter_2(k18_filter_2(sK230,sK231),sK230)
| spl1775_75 ),
inference(avatar_component_clause,[],[f59720]) ).
fof(f59732,definition,
( spl1775_78
<=> r1_tarski(k18_filter_2(sK230,sK231),k22_filter_2(sK230,k5_lattices(sK230),sK231)) ),
introduced(definition,[new_symbols(definition,[spl1775_78])],[avatar_definition]) ).
fof(f59733,plain,
( r1_tarski(k18_filter_2(sK230,sK231),k22_filter_2(sK230,k5_lattices(sK230),sK231))
| ~ spl1775_78 ),
inference(avatar_component_clause,[],[f59732]) ).
fof(f59740,plain,
( v3_struct_0(sK230)
| ~ v10_lattices(sK230)
| ~ l3_lattices(sK230)
| ~ m1_subset_1(sK231,u1_struct_0(sK230))
| spl1775_75 ),
inference(resolution,[],[f59722,f45594]) ).
fof(f59741,plain,
( ~ v10_lattices(sK230)
| ~ l3_lattices(sK230)
| ~ m1_subset_1(sK231,u1_struct_0(sK230))
| spl1775_75 ),
inference(forward_subsumption_resolution,[],[f59740,f45442]) ).
fof(f59742,plain,
( ~ l3_lattices(sK230)
| ~ m1_subset_1(sK231,u1_struct_0(sK230))
| spl1775_75 ),
inference(forward_subsumption_resolution,[],[f59741,f45441]) ).
fof(f59743,plain,
( ~ m1_subset_1(sK231,u1_struct_0(sK230))
| spl1775_75 ),
inference(forward_subsumption_resolution,[],[f59742,f45440]) ).
fof(f59744,plain,
( $false
| spl1775_75 ),
inference(forward_subsumption_resolution,[],[f59743,f45443]) ).
fof(f59745,plain,
spl1775_75,
inference(avatar_contradiction_clause,[],[f59744]) ).
fof(f59746,plain,
( m2_lattice4(k18_filter_2(sK230,sK231),sK230)
| v3_struct_0(sK230)
| ~ v10_lattices(sK230)
| ~ l3_lattices(sK230)
| ~ spl1775_75 ),
inference(resolution,[],[f59721,f45722]) ).
fof(f59747,plain,
( m2_lattice4(k18_filter_2(sK230,sK231),sK230)
| ~ v10_lattices(sK230)
| ~ l3_lattices(sK230)
| ~ spl1775_75 ),
inference(forward_subsumption_resolution,[],[f59746,f45442]) ).
fof(f59748,plain,
( m2_lattice4(k18_filter_2(sK230,sK231),sK230)
| ~ l3_lattices(sK230)
| ~ spl1775_75 ),
inference(forward_subsumption_resolution,[],[f59747,f45441]) ).
fof(f59749,plain,
( m2_lattice4(k18_filter_2(sK230,sK231),sK230)
| ~ spl1775_75 ),
inference(forward_subsumption_resolution,[],[f59748,f45440]) ).
fof(f59752,plain,
l1_lattices(sK230),
inference(resolution,[],[f47367,f45440]) ).
fof(f59757,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(resolution,[],[f45723,f45689]) ).
fof(f59759,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(duplicate_literal_removal,[],[f59757]) ).
fof(f59774,plain,
( v3_struct_0(sK230)
| sP9(sK230)
| ~ l3_lattices(sK230) ),
inference(resolution,[],[f46269,f45441]) ).
fof(f59779,plain,
( sP9(sK230)
| ~ l3_lattices(sK230) ),
inference(forward_subsumption_resolution,[],[f59774,f45442]) ).
fof(f59780,plain,
sP9(sK230),
inference(forward_subsumption_resolution,[],[f59779,f45440]) ).
fof(f59781,plain,
( v3_struct_0(sK230)
| u1_struct_0(sK230) = u1_struct_0(k1_lattice2(sK230)) ),
inference(resolution,[],[f45763,f45440]) ).
fof(f59783,plain,
u1_struct_0(sK230) = u1_struct_0(k1_lattice2(sK230)),
inference(forward_subsumption_resolution,[],[f59781,f45442]) ).
fof(f59793,plain,
! [X0] :
( m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK230)))
| ~ m1_filter_0(X0,k1_lattice2(sK230))
| v3_struct_0(k1_lattice2(sK230))
| ~ v10_lattices(k1_lattice2(sK230))
| ~ l3_lattices(k1_lattice2(sK230)) ),
inference(superposition,[],[f49131,f59783]) ).
fof(f59796,plain,
( ~ v1_xboole_0(u1_struct_0(sK230))
| v3_struct_0(k1_lattice2(sK230))
| ~ v10_lattices(k1_lattice2(sK230))
| ~ l3_lattices(k1_lattice2(sK230)) ),
inference(superposition,[],[f59759,f59783]) ).
fof(f59798,definition,
( spl1775_80
<=> l3_lattices(k1_lattice2(sK230)) ),
introduced(definition,[new_symbols(definition,[spl1775_80])],[avatar_definition]) ).
fof(f59799,plain,
( l3_lattices(k1_lattice2(sK230))
| ~ spl1775_80 ),
inference(avatar_component_clause,[],[f59798]) ).
fof(f59800,plain,
( ~ l3_lattices(k1_lattice2(sK230))
| spl1775_80 ),
inference(avatar_component_clause,[],[f59798]) ).
fof(f59802,definition,
( spl1775_81
<=> v10_lattices(k1_lattice2(sK230)) ),
introduced(definition,[new_symbols(definition,[spl1775_81])],[avatar_definition]) ).
fof(f59803,plain,
( v10_lattices(k1_lattice2(sK230))
| ~ spl1775_81 ),
inference(avatar_component_clause,[],[f59802]) ).
fof(f59804,plain,
( ~ v10_lattices(k1_lattice2(sK230))
| spl1775_81 ),
inference(avatar_component_clause,[],[f59802]) ).
fof(f59806,definition,
( spl1775_82
<=> v3_struct_0(k1_lattice2(sK230)) ),
introduced(definition,[new_symbols(definition,[spl1775_82])],[avatar_definition]) ).
fof(f59807,plain,
( ~ v3_struct_0(k1_lattice2(sK230))
| spl1775_82 ),
inference(avatar_component_clause,[],[f59806]) ).
fof(f59808,plain,
( v3_struct_0(k1_lattice2(sK230))
| ~ spl1775_82 ),
inference(avatar_component_clause,[],[f59806]) ).
fof(f59810,definition,
( spl1775_83
<=> v1_xboole_0(u1_struct_0(sK230)) ),
introduced(definition,[new_symbols(definition,[spl1775_83])],[avatar_definition]) ).
fof(f59812,plain,
( ~ v1_xboole_0(u1_struct_0(sK230))
| spl1775_83 ),
inference(avatar_component_clause,[],[f59810]) ).
fof(f59813,plain,
( ~ spl1775_80
| ~ spl1775_81
| spl1775_82
| ~ spl1775_83 ),
inference(avatar_split_clause,[],[f59796,f59810,f59806,f59802,f59798]) ).
fof(f59825,definition,
( spl1775_86
<=> ! [X0] :
( m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK230)))
| ~ m1_filter_0(X0,k1_lattice2(sK230)) ) ),
introduced(definition,[new_symbols(definition,[spl1775_86])],[avatar_definition]) ).
fof(f59826,plain,
( ! [X0] :
( m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK230)))
| ~ m1_filter_0(X0,k1_lattice2(sK230)) )
| ~ spl1775_86 ),
inference(avatar_component_clause,[],[f59825]) ).
fof(f59827,plain,
( ~ spl1775_80
| ~ spl1775_81
| spl1775_82
| spl1775_86 ),
inference(avatar_split_clause,[],[f59793,f59825,f59806,f59802,f59798]) ).
fof(f59873,plain,
( ~ l3_lattices(sK230)
| spl1775_80 ),
inference(resolution,[],[f59800,f46253]) ).
fof(f59874,plain,
( $false
| spl1775_80 ),
inference(forward_subsumption_resolution,[],[f59873,f45440]) ).
fof(f59875,plain,
spl1775_80,
inference(avatar_contradiction_clause,[],[f59874]) ).
fof(f59887,plain,
( v3_struct_0(sK230)
| ~ l3_lattices(sK230)
| ~ spl1775_82 ),
inference(resolution,[],[f59808,f46271]) ).
fof(f59888,plain,
( ~ l3_lattices(sK230)
| ~ spl1775_82 ),
inference(forward_subsumption_resolution,[],[f59887,f45442]) ).
fof(f59889,plain,
( $false
| ~ spl1775_82 ),
inference(forward_subsumption_resolution,[],[f59888,f45440]) ).
fof(f59890,plain,
~ spl1775_82,
inference(avatar_contradiction_clause,[],[f59889]) ).
fof(f59896,plain,
( ~ sP9(sK230)
| spl1775_81 ),
inference(resolution,[],[f59804,f46260]) ).
fof(f59898,plain,
( $false
| spl1775_81 ),
inference(forward_subsumption_resolution,[],[f59896,f59780]) ).
fof(f59899,plain,
spl1775_81,
inference(avatar_contradiction_clause,[],[f59898]) ).
fof(f60064,plain,
! [X2,X0,X1] :
( ~ r3_lattices(X1,sK249(X0,k18_filter_2(X1,X2)),X2)
| r1_tarski(X0,k18_filter_2(X1,X2))
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ m1_subset_1(sK249(X0,k18_filter_2(X1,X2)),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(resolution,[],[f45637,f45593]) ).
fof(f60065,plain,
! [X2,X3,X0,X1] :
( ~ r3_lattices(X1,sK249(X0,k22_filter_2(X1,X2,X3)),X3)
| ~ r3_lattices(X1,X2,sK249(X0,k22_filter_2(X1,X2,X3)))
| r1_tarski(X0,k22_filter_2(X1,X2,X3))
| ~ r3_lattices(X1,X2,X3)
| ~ m1_subset_1(sK249(X0,k22_filter_2(X1,X2,X3)),u1_struct_0(X1))
| ~ m1_subset_1(X3,u1_struct_0(X1))
| ~ m1_subset_1(X2,u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(resolution,[],[f45637,f45600]) ).
fof(f60066,plain,
( k5_lattices(sK230) = k4_lattices(sK230,k5_lattices(sK230),sK231)
| v3_struct_0(sK230)
| ~ v10_lattices(sK230)
| ~ v13_lattices(sK230)
| ~ l3_lattices(sK230) ),
inference(resolution,[],[f45502,f45443]) ).
fof(f60074,plain,
( k5_lattices(sK230) = k4_lattices(sK230,k5_lattices(sK230),sK231)
| ~ v10_lattices(sK230)
| ~ v13_lattices(sK230)
| ~ l3_lattices(sK230) ),
inference(forward_subsumption_resolution,[],[f60066,f45442]) ).
fof(f60077,plain,
( k5_lattices(sK230) = k4_lattices(sK230,k5_lattices(sK230),sK231)
| ~ v13_lattices(sK230)
| ~ l3_lattices(sK230) ),
inference(forward_subsumption_resolution,[],[f60074,f45441]) ).
fof(f60080,plain,
( k5_lattices(sK230) = k4_lattices(sK230,k5_lattices(sK230),sK231)
| ~ l3_lattices(sK230) ),
inference(forward_subsumption_resolution,[],[f60077,f45444]) ).
fof(f60090,plain,
k5_lattices(sK230) = k4_lattices(sK230,k5_lattices(sK230),sK231),
inference(forward_subsumption_resolution,[],[f60080,f45440]) ).
fof(f60092,plain,
( r2_hidden(k5_lattices(sK230),k18_filter_2(sK230,sK231))
| ~ m1_subset_1(k5_lattices(sK230),u1_struct_0(sK230))
| ~ m1_subset_1(sK231,u1_struct_0(sK230))
| v3_struct_0(sK230)
| ~ v10_lattices(sK230)
| ~ l3_lattices(sK230) ),
inference(superposition,[],[f45587,f60090]) ).
fof(f60093,plain,
( r2_hidden(k5_lattices(sK230),k18_filter_2(sK230,sK231))
| ~ m1_subset_1(k5_lattices(sK230),u1_struct_0(sK230))
| v3_struct_0(sK230)
| ~ v10_lattices(sK230)
| ~ l3_lattices(sK230) ),
inference(forward_subsumption_resolution,[],[f60092,f45443]) ).
fof(f60094,plain,
( r2_hidden(k5_lattices(sK230),k18_filter_2(sK230,sK231))
| ~ m1_subset_1(k5_lattices(sK230),u1_struct_0(sK230))
| ~ v10_lattices(sK230)
| ~ l3_lattices(sK230) ),
inference(forward_subsumption_resolution,[],[f60093,f45442]) ).
fof(f60095,plain,
( r2_hidden(k5_lattices(sK230),k18_filter_2(sK230,sK231))
| ~ m1_subset_1(k5_lattices(sK230),u1_struct_0(sK230))
| ~ l3_lattices(sK230) ),
inference(forward_subsumption_resolution,[],[f60094,f45441]) ).
fof(f60096,plain,
( r2_hidden(k5_lattices(sK230),k18_filter_2(sK230,sK231))
| ~ m1_subset_1(k5_lattices(sK230),u1_struct_0(sK230)) ),
inference(forward_subsumption_resolution,[],[f60095,f45440]) ).
fof(f60098,definition,
( spl1775_108
<=> m1_subset_1(k5_lattices(sK230),u1_struct_0(sK230)) ),
introduced(definition,[new_symbols(definition,[spl1775_108])],[avatar_definition]) ).
fof(f60099,plain,
( m1_subset_1(k5_lattices(sK230),u1_struct_0(sK230))
| ~ spl1775_108 ),
inference(avatar_component_clause,[],[f60098]) ).
fof(f60100,plain,
( ~ m1_subset_1(k5_lattices(sK230),u1_struct_0(sK230))
| spl1775_108 ),
inference(avatar_component_clause,[],[f60098]) ).
fof(f60102,definition,
( spl1775_109
<=> r2_hidden(k5_lattices(sK230),k18_filter_2(sK230,sK231)) ),
introduced(definition,[new_symbols(definition,[spl1775_109])],[avatar_definition]) ).
fof(f60104,plain,
( r2_hidden(k5_lattices(sK230),k18_filter_2(sK230,sK231))
| ~ spl1775_109 ),
inference(avatar_component_clause,[],[f60102]) ).
fof(f60105,plain,
( ~ spl1775_108
| spl1775_109 ),
inference(avatar_split_clause,[],[f60096,f60102,f60098]) ).
fof(f60106,plain,
( v3_struct_0(sK230)
| ~ l1_lattices(sK230)
| spl1775_108 ),
inference(resolution,[],[f60100,f45577]) ).
fof(f60107,plain,
( ~ l1_lattices(sK230)
| spl1775_108 ),
inference(forward_subsumption_resolution,[],[f60106,f45442]) ).
fof(f60108,plain,
( $false
| spl1775_108 ),
inference(forward_subsumption_resolution,[],[f60107,f59752]) ).
fof(f60109,plain,
spl1775_108,
inference(avatar_contradiction_clause,[],[f60108]) ).
fof(f60110,plain,
( r3_lattices(sK230,k5_lattices(sK230),sK231)
| ~ m1_subset_1(sK231,u1_struct_0(sK230))
| ~ m1_subset_1(k5_lattices(sK230),u1_struct_0(sK230))
| v3_struct_0(sK230)
| ~ v10_lattices(sK230)
| ~ l3_lattices(sK230)
| ~ spl1775_109 ),
inference(resolution,[],[f60104,f45592]) ).
fof(f60111,plain,
( r3_lattices(sK230,k5_lattices(sK230),sK231)
| ~ m1_subset_1(k5_lattices(sK230),u1_struct_0(sK230))
| v3_struct_0(sK230)
| ~ v10_lattices(sK230)
| ~ l3_lattices(sK230)
| ~ spl1775_109 ),
inference(forward_subsumption_resolution,[],[f60110,f45443]) ).
fof(f60112,plain,
( r3_lattices(sK230,k5_lattices(sK230),sK231)
| v3_struct_0(sK230)
| ~ v10_lattices(sK230)
| ~ l3_lattices(sK230)
| ~ spl1775_108
| ~ spl1775_109 ),
inference(forward_subsumption_resolution,[],[f60111,f60099]) ).
fof(f60113,plain,
( r3_lattices(sK230,k5_lattices(sK230),sK231)
| ~ v10_lattices(sK230)
| ~ l3_lattices(sK230)
| ~ spl1775_108
| ~ spl1775_109 ),
inference(forward_subsumption_resolution,[],[f60112,f45442]) ).
fof(f60114,plain,
( r3_lattices(sK230,k5_lattices(sK230),sK231)
| ~ l3_lattices(sK230)
| ~ spl1775_108
| ~ spl1775_109 ),
inference(forward_subsumption_resolution,[],[f60113,f45441]) ).
fof(f60115,plain,
( r3_lattices(sK230,k5_lattices(sK230),sK231)
| ~ spl1775_108
| ~ spl1775_109 ),
inference(forward_subsumption_resolution,[],[f60114,f45440]) ).
fof(f60125,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(sK249(k18_filter_2(X0,X1),X2),u1_struct_0(X0))
| r3_lattices(X0,sK249(k18_filter_2(X0,X1),X2),X1)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| r1_tarski(k18_filter_2(X0,X1),X2)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(resolution,[],[f45636,f45592]) ).
fof(f60127,plain,
! [X2,X3,X0,X1] :
( ~ m1_subset_1(sK249(k22_filter_2(X0,X1,X2),X3),u1_struct_0(X0))
| r3_lattices(X0,sK249(k22_filter_2(X0,X1,X2),X3),X2)
| ~ r3_lattices(X0,X1,X2)
| r1_tarski(k22_filter_2(X0,X1,X2),X3)
| ~ 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(resolution,[],[f45636,f45598]) ).
fof(f60216,plain,
! [X2,X0,X1] :
( ~ m2_lattice4(X1,X2)
| m1_subset_1(X0,u1_struct_0(X2))
| ~ r2_hidden(X0,X1)
| v3_struct_0(X2)
| ~ v10_lattices(X2)
| ~ l3_lattices(X2) ),
inference(resolution,[],[f45614,f47430]) ).
fof(f60228,plain,
! [X2,X3,X0,X1] :
( m1_subset_1(X0,u1_struct_0(X1))
| ~ r2_hidden(X0,k22_filter_2(X1,X2,X3))
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ m1_subset_1(X3,u1_struct_0(X1)) ),
inference(resolution,[],[f60216,f45601]) ).
fof(f60230,plain,
( ! [X0] :
( m1_subset_1(X0,u1_struct_0(sK230))
| ~ r2_hidden(X0,k18_filter_2(sK230,sK231))
| v3_struct_0(sK230)
| ~ v10_lattices(sK230)
| ~ l3_lattices(sK230) )
| ~ spl1775_75 ),
inference(resolution,[],[f60216,f59749]) ).
fof(f60232,plain,
! [X2,X3,X0,X1] :
( ~ r2_hidden(X0,k22_filter_2(X1,X2,X3))
| m1_subset_1(X0,u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ m1_subset_1(X3,u1_struct_0(X1)) ),
inference(duplicate_literal_removal,[],[f60228]) ).
fof(f60233,plain,
( ! [X0] :
( m1_subset_1(X0,u1_struct_0(sK230))
| ~ r2_hidden(X0,k18_filter_2(sK230,sK231))
| ~ v10_lattices(sK230)
| ~ l3_lattices(sK230) )
| ~ spl1775_75 ),
inference(forward_subsumption_resolution,[],[f60230,f45442]) ).
fof(f60234,plain,
( ! [X0] :
( m1_subset_1(X0,u1_struct_0(sK230))
| ~ r2_hidden(X0,k18_filter_2(sK230,sK231))
| ~ l3_lattices(sK230) )
| ~ spl1775_75 ),
inference(forward_subsumption_resolution,[],[f60233,f45441]) ).
fof(f60235,plain,
( ! [X0] :
( ~ r2_hidden(X0,k18_filter_2(sK230,sK231))
| m1_subset_1(X0,u1_struct_0(sK230)) )
| ~ spl1775_75 ),
inference(forward_subsumption_resolution,[],[f60234,f45440]) ).
fof(f60242,plain,
( ! [X0] :
( m1_subset_1(sK249(k18_filter_2(sK230,sK231),X0),u1_struct_0(sK230))
| r1_tarski(k18_filter_2(sK230,sK231),X0) )
| ~ spl1775_75 ),
inference(resolution,[],[f60235,f45636]) ).
fof(f60252,plain,
( ! [X0] :
( r1_tarski(k18_filter_2(sK230,sK231),X0)
| r3_lattices(sK230,sK249(k18_filter_2(sK230,sK231),X0),sK231)
| ~ m1_subset_1(sK231,u1_struct_0(sK230))
| r1_tarski(k18_filter_2(sK230,sK231),X0)
| v3_struct_0(sK230)
| ~ v10_lattices(sK230)
| ~ l3_lattices(sK230) )
| ~ spl1775_75 ),
inference(resolution,[],[f60242,f60125]) ).
fof(f60259,plain,
( ! [X0] :
( r1_tarski(k18_filter_2(sK230,sK231),X0)
| r3_lattices(sK230,sK249(k18_filter_2(sK230,sK231),X0),sK231)
| ~ m1_subset_1(sK231,u1_struct_0(sK230))
| v3_struct_0(sK230)
| ~ v10_lattices(sK230)
| ~ l3_lattices(sK230) )
| ~ spl1775_75 ),
inference(duplicate_literal_removal,[],[f60252]) ).
fof(f60264,plain,
( ! [X0] :
( r1_tarski(k18_filter_2(sK230,sK231),X0)
| r3_lattices(sK230,sK249(k18_filter_2(sK230,sK231),X0),sK231)
| v3_struct_0(sK230)
| ~ v10_lattices(sK230)
| ~ l3_lattices(sK230) )
| ~ spl1775_75 ),
inference(forward_subsumption_resolution,[],[f60259,f45443]) ).
fof(f60269,plain,
( ! [X0] :
( r1_tarski(k18_filter_2(sK230,sK231),X0)
| r3_lattices(sK230,sK249(k18_filter_2(sK230,sK231),X0),sK231)
| ~ v10_lattices(sK230)
| ~ l3_lattices(sK230) )
| ~ spl1775_75 ),
inference(forward_subsumption_resolution,[],[f60264,f45442]) ).
fof(f60274,plain,
( ! [X0] :
( r1_tarski(k18_filter_2(sK230,sK231),X0)
| r3_lattices(sK230,sK249(k18_filter_2(sK230,sK231),X0),sK231)
| ~ l3_lattices(sK230) )
| ~ spl1775_75 ),
inference(forward_subsumption_resolution,[],[f60269,f45441]) ).
fof(f60276,plain,
( ! [X0] :
( r3_lattices(sK230,sK249(k18_filter_2(sK230,sK231),X0),sK231)
| r1_tarski(k18_filter_2(sK230,sK231),X0) )
| ~ spl1775_75 ),
inference(forward_subsumption_resolution,[],[f60274,f45440]) ).
fof(f60278,plain,
( ! [X0] :
( r1_tarski(k18_filter_2(sK230,sK231),k22_filter_2(sK230,X0,sK231))
| ~ r3_lattices(sK230,X0,sK249(k18_filter_2(sK230,sK231),k22_filter_2(sK230,X0,sK231)))
| r1_tarski(k18_filter_2(sK230,sK231),k22_filter_2(sK230,X0,sK231))
| ~ r3_lattices(sK230,X0,sK231)
| ~ m1_subset_1(sK249(k18_filter_2(sK230,sK231),k22_filter_2(sK230,X0,sK231)),u1_struct_0(sK230))
| ~ m1_subset_1(sK231,u1_struct_0(sK230))
| ~ m1_subset_1(X0,u1_struct_0(sK230))
| v3_struct_0(sK230)
| ~ v10_lattices(sK230)
| ~ l3_lattices(sK230) )
| ~ spl1775_75 ),
inference(resolution,[],[f60276,f60065]) ).
fof(f60279,plain,
( ! [X0] :
( r1_tarski(k18_filter_2(sK230,sK231),k22_filter_2(sK230,X0,sK231))
| ~ r3_lattices(sK230,X0,sK249(k18_filter_2(sK230,sK231),k22_filter_2(sK230,X0,sK231)))
| ~ r3_lattices(sK230,X0,sK231)
| ~ m1_subset_1(sK249(k18_filter_2(sK230,sK231),k22_filter_2(sK230,X0,sK231)),u1_struct_0(sK230))
| ~ m1_subset_1(sK231,u1_struct_0(sK230))
| ~ m1_subset_1(X0,u1_struct_0(sK230))
| v3_struct_0(sK230)
| ~ v10_lattices(sK230)
| ~ l3_lattices(sK230) )
| ~ spl1775_75 ),
inference(duplicate_literal_removal,[],[f60278]) ).
fof(f60281,plain,
( ! [X0] :
( r1_tarski(k18_filter_2(sK230,sK231),k22_filter_2(sK230,X0,sK231))
| ~ r3_lattices(sK230,X0,sK249(k18_filter_2(sK230,sK231),k22_filter_2(sK230,X0,sK231)))
| ~ r3_lattices(sK230,X0,sK231)
| ~ m1_subset_1(sK249(k18_filter_2(sK230,sK231),k22_filter_2(sK230,X0,sK231)),u1_struct_0(sK230))
| ~ m1_subset_1(X0,u1_struct_0(sK230))
| v3_struct_0(sK230)
| ~ v10_lattices(sK230)
| ~ l3_lattices(sK230) )
| ~ spl1775_75 ),
inference(forward_subsumption_resolution,[],[f60279,f45443]) ).
fof(f60282,plain,
( ! [X0] :
( r1_tarski(k18_filter_2(sK230,sK231),k22_filter_2(sK230,X0,sK231))
| ~ r3_lattices(sK230,X0,sK249(k18_filter_2(sK230,sK231),k22_filter_2(sK230,X0,sK231)))
| ~ r3_lattices(sK230,X0,sK231)
| ~ m1_subset_1(sK249(k18_filter_2(sK230,sK231),k22_filter_2(sK230,X0,sK231)),u1_struct_0(sK230))
| ~ m1_subset_1(X0,u1_struct_0(sK230))
| ~ v10_lattices(sK230)
| ~ l3_lattices(sK230) )
| ~ spl1775_75 ),
inference(forward_subsumption_resolution,[],[f60281,f45442]) ).
fof(f60283,plain,
( ! [X0] :
( r1_tarski(k18_filter_2(sK230,sK231),k22_filter_2(sK230,X0,sK231))
| ~ r3_lattices(sK230,X0,sK249(k18_filter_2(sK230,sK231),k22_filter_2(sK230,X0,sK231)))
| ~ r3_lattices(sK230,X0,sK231)
| ~ m1_subset_1(sK249(k18_filter_2(sK230,sK231),k22_filter_2(sK230,X0,sK231)),u1_struct_0(sK230))
| ~ m1_subset_1(X0,u1_struct_0(sK230))
| ~ l3_lattices(sK230) )
| ~ spl1775_75 ),
inference(forward_subsumption_resolution,[],[f60282,f45441]) ).
fof(f60284,plain,
( ! [X0] :
( r1_tarski(k18_filter_2(sK230,sK231),k22_filter_2(sK230,X0,sK231))
| ~ r3_lattices(sK230,X0,sK249(k18_filter_2(sK230,sK231),k22_filter_2(sK230,X0,sK231)))
| ~ r3_lattices(sK230,X0,sK231)
| ~ m1_subset_1(sK249(k18_filter_2(sK230,sK231),k22_filter_2(sK230,X0,sK231)),u1_struct_0(sK230))
| ~ m1_subset_1(X0,u1_struct_0(sK230)) )
| ~ spl1775_75 ),
inference(forward_subsumption_resolution,[],[f60283,f45440]) ).
fof(f60285,plain,
( ! [X0] :
( ~ r3_lattices(sK230,X0,sK249(k18_filter_2(sK230,sK231),k22_filter_2(sK230,X0,sK231)))
| r1_tarski(k18_filter_2(sK230,sK231),k22_filter_2(sK230,X0,sK231))
| ~ r3_lattices(sK230,X0,sK231)
| ~ m1_subset_1(X0,u1_struct_0(sK230)) )
| ~ spl1775_75 ),
inference(forward_subsumption_resolution,[],[f60284,f60242]) ).
fof(f60286,plain,
( r1_tarski(k18_filter_2(sK230,sK231),k22_filter_2(sK230,k5_lattices(sK230),sK231))
| ~ r3_lattices(sK230,k5_lattices(sK230),sK231)
| ~ m1_subset_1(k5_lattices(sK230),u1_struct_0(sK230))
| ~ m1_subset_1(sK249(k18_filter_2(sK230,sK231),k22_filter_2(sK230,k5_lattices(sK230),sK231)),u1_struct_0(sK230))
| v3_struct_0(sK230)
| ~ v10_lattices(sK230)
| ~ v13_lattices(sK230)
| ~ l3_lattices(sK230)
| ~ spl1775_75 ),
inference(resolution,[],[f60285,f45501]) ).
fof(f60287,plain,
( r1_tarski(k18_filter_2(sK230,sK231),k22_filter_2(sK230,k5_lattices(sK230),sK231))
| ~ m1_subset_1(k5_lattices(sK230),u1_struct_0(sK230))
| ~ m1_subset_1(sK249(k18_filter_2(sK230,sK231),k22_filter_2(sK230,k5_lattices(sK230),sK231)),u1_struct_0(sK230))
| v3_struct_0(sK230)
| ~ v10_lattices(sK230)
| ~ v13_lattices(sK230)
| ~ l3_lattices(sK230)
| ~ spl1775_75
| ~ spl1775_108
| ~ spl1775_109 ),
inference(forward_subsumption_resolution,[],[f60286,f60115]) ).
fof(f60288,plain,
( r1_tarski(k18_filter_2(sK230,sK231),k22_filter_2(sK230,k5_lattices(sK230),sK231))
| ~ m1_subset_1(sK249(k18_filter_2(sK230,sK231),k22_filter_2(sK230,k5_lattices(sK230),sK231)),u1_struct_0(sK230))
| v3_struct_0(sK230)
| ~ v10_lattices(sK230)
| ~ v13_lattices(sK230)
| ~ l3_lattices(sK230)
| ~ spl1775_75
| ~ spl1775_108
| ~ spl1775_109 ),
inference(forward_subsumption_resolution,[],[f60287,f60099]) ).
fof(f60289,plain,
( r1_tarski(k18_filter_2(sK230,sK231),k22_filter_2(sK230,k5_lattices(sK230),sK231))
| v3_struct_0(sK230)
| ~ v10_lattices(sK230)
| ~ v13_lattices(sK230)
| ~ l3_lattices(sK230)
| ~ spl1775_75
| ~ spl1775_108
| ~ spl1775_109 ),
inference(forward_subsumption_resolution,[],[f60288,f60242]) ).
fof(f60290,plain,
( r1_tarski(k18_filter_2(sK230,sK231),k22_filter_2(sK230,k5_lattices(sK230),sK231))
| ~ v10_lattices(sK230)
| ~ v13_lattices(sK230)
| ~ l3_lattices(sK230)
| ~ spl1775_75
| ~ spl1775_108
| ~ spl1775_109 ),
inference(forward_subsumption_resolution,[],[f60289,f45442]) ).
fof(f60291,plain,
( r1_tarski(k18_filter_2(sK230,sK231),k22_filter_2(sK230,k5_lattices(sK230),sK231))
| ~ v13_lattices(sK230)
| ~ l3_lattices(sK230)
| ~ spl1775_75
| ~ spl1775_108
| ~ spl1775_109 ),
inference(forward_subsumption_resolution,[],[f60290,f45441]) ).
fof(f60292,plain,
( r1_tarski(k18_filter_2(sK230,sK231),k22_filter_2(sK230,k5_lattices(sK230),sK231))
| ~ l3_lattices(sK230)
| ~ spl1775_75
| ~ spl1775_108
| ~ spl1775_109 ),
inference(forward_subsumption_resolution,[],[f60291,f45444]) ).
fof(f60293,plain,
( r1_tarski(k18_filter_2(sK230,sK231),k22_filter_2(sK230,k5_lattices(sK230),sK231))
| ~ spl1775_75
| ~ spl1775_108
| ~ spl1775_109 ),
inference(forward_subsumption_resolution,[],[f60292,f45440]) ).
fof(f60294,plain,
( spl1775_78
| ~ spl1775_75
| ~ spl1775_108
| ~ spl1775_109 ),
inference(avatar_split_clause,[],[f60293,f60102,f60098,f59720,f59732]) ).
fof(f60318,plain,
( ! [X0] :
( ~ m1_filter_0(X0,k1_lattice2(sK230))
| v1_xboole_0(u1_struct_0(sK230))
| r1_filter_2(u1_struct_0(sK230),X0,X0) )
| ~ spl1775_86 ),
inference(resolution,[],[f59826,f58562]) ).
fof(f60319,plain,
( ! [X0] :
( r1_filter_2(u1_struct_0(sK230),X0,X0)
| ~ m1_filter_0(X0,k1_lattice2(sK230)) )
| spl1775_83
| ~ spl1775_86 ),
inference(forward_subsumption_resolution,[],[f60318,f59812]) ).
fof(f60512,plain,
( ~ r1_tarski(k22_filter_2(sK230,k5_lattices(sK230),sK231),k18_filter_2(sK230,sK231))
| k18_filter_2(sK230,sK231) = k22_filter_2(sK230,k5_lattices(sK230),sK231)
| ~ spl1775_78 ),
inference(resolution,[],[f47065,f59733]) ).
fof(f60516,definition,
( spl1775_114
<=> k18_filter_2(sK230,sK231) = k22_filter_2(sK230,k5_lattices(sK230),sK231) ),
introduced(definition,[new_symbols(definition,[spl1775_114])],[avatar_definition]) ).
fof(f60518,plain,
( k18_filter_2(sK230,sK231) = k22_filter_2(sK230,k5_lattices(sK230),sK231)
| ~ spl1775_114 ),
inference(avatar_component_clause,[],[f60516]) ).
fof(f60520,definition,
( spl1775_115
<=> r1_tarski(k22_filter_2(sK230,k5_lattices(sK230),sK231),k18_filter_2(sK230,sK231)) ),
introduced(definition,[new_symbols(definition,[spl1775_115])],[avatar_definition]) ).
fof(f60522,plain,
( ~ r1_tarski(k22_filter_2(sK230,k5_lattices(sK230),sK231),k18_filter_2(sK230,sK231))
| spl1775_115 ),
inference(avatar_component_clause,[],[f60520]) ).
fof(f60523,plain,
( spl1775_114
| ~ spl1775_115
| ~ spl1775_78 ),
inference(avatar_split_clause,[],[f60512,f59732,f60520,f60516]) ).
fof(f61187,plain,
( m1_filter_2(k18_filter_2(sK230,sK231),k1_lattice2(sK230))
| v3_struct_0(k1_lattice2(sK230))
| ~ v10_lattices(k1_lattice2(sK230))
| ~ l3_lattices(k1_lattice2(sK230))
| ~ m1_subset_1(k5_filter_2(sK230,sK231),u1_struct_0(k1_lattice2(sK230))) ),
inference(superposition,[],[f47401,f59662]) ).
fof(f61194,plain,
( m1_filter_2(k18_filter_2(sK230,sK231),k1_lattice2(sK230))
| ~ v10_lattices(k1_lattice2(sK230))
| ~ l3_lattices(k1_lattice2(sK230))
| ~ m1_subset_1(k5_filter_2(sK230,sK231),u1_struct_0(k1_lattice2(sK230)))
| spl1775_82 ),
inference(forward_subsumption_resolution,[],[f61187,f59807]) ).
fof(f61197,plain,
( m1_filter_2(k18_filter_2(sK230,sK231),k1_lattice2(sK230))
| ~ l3_lattices(k1_lattice2(sK230))
| ~ m1_subset_1(k5_filter_2(sK230,sK231),u1_struct_0(k1_lattice2(sK230)))
| ~ spl1775_81
| spl1775_82 ),
inference(forward_subsumption_resolution,[],[f61194,f59803]) ).
fof(f61200,plain,
( m1_filter_2(k18_filter_2(sK230,sK231),k1_lattice2(sK230))
| ~ m1_subset_1(k5_filter_2(sK230,sK231),u1_struct_0(k1_lattice2(sK230)))
| ~ spl1775_80
| ~ spl1775_81
| spl1775_82 ),
inference(forward_subsumption_resolution,[],[f61197,f59799]) ).
fof(f61202,plain,
( ~ m1_subset_1(k5_filter_2(sK230,sK231),u1_struct_0(sK230))
| m1_filter_2(k18_filter_2(sK230,sK231),k1_lattice2(sK230))
| ~ spl1775_80
| ~ spl1775_81
| spl1775_82 ),
inference(forward_demodulation,[],[f61200,f59783]) ).
fof(f62202,plain,
( sK231 = k5_filter_2(sK230,sK231)
| v3_struct_0(sK230)
| ~ v10_lattices(sK230)
| ~ l3_lattices(sK230) ),
inference(resolution,[],[f47415,f45443]) ).
fof(f62216,plain,
( sK231 = k5_filter_2(sK230,sK231)
| ~ v10_lattices(sK230)
| ~ l3_lattices(sK230) ),
inference(forward_subsumption_resolution,[],[f62202,f45442]) ).
fof(f62222,plain,
( sK231 = k5_filter_2(sK230,sK231)
| ~ l3_lattices(sK230) ),
inference(forward_subsumption_resolution,[],[f62216,f45441]) ).
fof(f62227,plain,
sK231 = k5_filter_2(sK230,sK231),
inference(forward_subsumption_resolution,[],[f62222,f45440]) ).
fof(f62238,plain,
( ~ m1_subset_1(sK231,u1_struct_0(sK230))
| m1_filter_2(k18_filter_2(sK230,sK231),k1_lattice2(sK230))
| ~ spl1775_80
| ~ spl1775_81
| spl1775_82 ),
inference(forward_demodulation,[],[f61202,f62227]) ).
fof(f62270,plain,
( m1_filter_2(k18_filter_2(sK230,sK231),k1_lattice2(sK230))
| ~ spl1775_80
| ~ spl1775_81
| spl1775_82 ),
inference(forward_subsumption_resolution,[],[f62238,f45443]) ).
fof(f62483,plain,
( m1_filter_0(k18_filter_2(sK230,sK231),k1_lattice2(sK230))
| v3_struct_0(k1_lattice2(sK230))
| ~ v10_lattices(k1_lattice2(sK230))
| ~ l3_lattices(k1_lattice2(sK230))
| ~ spl1775_80
| ~ spl1775_81
| spl1775_82 ),
inference(resolution,[],[f62270,f56307]) ).
fof(f62484,plain,
( m1_filter_0(k18_filter_2(sK230,sK231),k1_lattice2(sK230))
| ~ v10_lattices(k1_lattice2(sK230))
| ~ l3_lattices(k1_lattice2(sK230))
| ~ spl1775_80
| ~ spl1775_81
| spl1775_82 ),
inference(forward_subsumption_resolution,[],[f62483,f59807]) ).
fof(f62486,plain,
( m1_filter_0(k18_filter_2(sK230,sK231),k1_lattice2(sK230))
| ~ l3_lattices(k1_lattice2(sK230))
| ~ spl1775_80
| ~ spl1775_81
| spl1775_82 ),
inference(forward_subsumption_resolution,[],[f62484,f59803]) ).
fof(f62488,plain,
( m1_filter_0(k18_filter_2(sK230,sK231),k1_lattice2(sK230))
| ~ spl1775_80
| ~ spl1775_81
| spl1775_82 ),
inference(forward_subsumption_resolution,[],[f62486,f59799]) ).
fof(f63089,plain,
! [X2,X3,X0,X1] :
( m1_subset_1(sK249(k22_filter_2(X0,X1,X2),X3),u1_struct_0(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))
| r1_tarski(k22_filter_2(X0,X1,X2),X3) ),
inference(resolution,[],[f60232,f45636]) ).
fof(f63097,plain,
! [X2,X3,X0,X1] :
( 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))
| r1_tarski(k22_filter_2(X0,X1,X2),X3)
| r3_lattices(X0,sK249(k22_filter_2(X0,X1,X2),X3),X2)
| ~ r3_lattices(X0,X1,X2)
| r1_tarski(k22_filter_2(X0,X1,X2),X3)
| ~ 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(resolution,[],[f63089,f60127]) ).
fof(f63124,plain,
! [X2,X3,X0,X1] :
( r3_lattices(X0,sK249(k22_filter_2(X0,X1,X2),X3),X2)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| r1_tarski(k22_filter_2(X0,X1,X2),X3)
| v3_struct_0(X0)
| ~ r3_lattices(X0,X1,X2) ),
inference(duplicate_literal_removal,[],[f63097]) ).
fof(f63133,plain,
! [X2,X0,X1] :
( ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| r1_tarski(k22_filter_2(X0,X1,X2),k18_filter_2(X0,X2))
| v3_struct_0(X0)
| ~ r3_lattices(X0,X1,X2)
| r1_tarski(k22_filter_2(X0,X1,X2),k18_filter_2(X0,X2))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(sK249(k22_filter_2(X0,X1,X2),k18_filter_2(X0,X2)),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(resolution,[],[f63124,f60064]) ).
fof(f63146,plain,
! [X2,X0,X1] :
( ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| r1_tarski(k22_filter_2(X0,X1,X2),k18_filter_2(X0,X2))
| v3_struct_0(X0)
| ~ r3_lattices(X0,X1,X2)
| ~ m1_subset_1(sK249(k22_filter_2(X0,X1,X2),k18_filter_2(X0,X2)),u1_struct_0(X0)) ),
inference(duplicate_literal_removal,[],[f63133]) ).
fof(f63154,plain,
! [X2,X0,X1] :
( r1_tarski(k22_filter_2(X0,X1,X2),k18_filter_2(X0,X2))
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ r3_lattices(X0,X1,X2) ),
inference(forward_subsumption_resolution,[],[f63146,f63089]) ).
fof(f63177,plain,
( ~ l3_lattices(sK230)
| ~ m1_subset_1(k5_lattices(sK230),u1_struct_0(sK230))
| ~ m1_subset_1(sK231,u1_struct_0(sK230))
| ~ v10_lattices(sK230)
| v3_struct_0(sK230)
| ~ r3_lattices(sK230,k5_lattices(sK230),sK231)
| spl1775_115 ),
inference(resolution,[],[f63154,f60522]) ).
fof(f63195,plain,
( ~ m1_subset_1(k5_lattices(sK230),u1_struct_0(sK230))
| ~ m1_subset_1(sK231,u1_struct_0(sK230))
| ~ v10_lattices(sK230)
| v3_struct_0(sK230)
| ~ r3_lattices(sK230,k5_lattices(sK230),sK231)
| spl1775_115 ),
inference(forward_subsumption_resolution,[],[f63177,f45440]) ).
fof(f63201,plain,
( ~ m1_subset_1(sK231,u1_struct_0(sK230))
| ~ v10_lattices(sK230)
| v3_struct_0(sK230)
| ~ r3_lattices(sK230,k5_lattices(sK230),sK231)
| ~ spl1775_108
| spl1775_115 ),
inference(forward_subsumption_resolution,[],[f63195,f60099]) ).
fof(f63207,plain,
( ~ v10_lattices(sK230)
| v3_struct_0(sK230)
| ~ r3_lattices(sK230,k5_lattices(sK230),sK231)
| ~ spl1775_108
| spl1775_115 ),
inference(forward_subsumption_resolution,[],[f63201,f45443]) ).
fof(f63213,plain,
( v3_struct_0(sK230)
| ~ r3_lattices(sK230,k5_lattices(sK230),sK231)
| ~ spl1775_108
| spl1775_115 ),
inference(forward_subsumption_resolution,[],[f63207,f45441]) ).
fof(f63218,plain,
( ~ r3_lattices(sK230,k5_lattices(sK230),sK231)
| ~ spl1775_108
| spl1775_115 ),
inference(forward_subsumption_resolution,[],[f63213,f45442]) ).
fof(f63223,plain,
( $false
| ~ spl1775_108
| ~ spl1775_109
| spl1775_115 ),
inference(forward_subsumption_resolution,[],[f63218,f60115]) ).
fof(f63224,plain,
( ~ spl1775_108
| ~ spl1775_109
| spl1775_115 ),
inference(avatar_contradiction_clause,[],[f63223]) ).
fof(f63232,plain,
( ~ r1_filter_2(u1_struct_0(sK230),k18_filter_2(sK230,sK231),k18_filter_2(sK230,sK231))
| ~ spl1775_114 ),
inference(superposition,[],[f45445,f60518]) ).
fof(f63477,plain,
( ~ m1_filter_0(k18_filter_2(sK230,sK231),k1_lattice2(sK230))
| spl1775_83
| ~ spl1775_86
| ~ spl1775_114 ),
inference(resolution,[],[f63232,f60319]) ).
fof(f63484,plain,
( $false
| ~ spl1775_80
| ~ spl1775_81
| spl1775_82
| spl1775_83
| ~ spl1775_86
| ~ spl1775_114 ),
inference(forward_subsumption_resolution,[],[f63477,f62488]) ).
fof(f63485,plain,
( ~ spl1775_80
| ~ spl1775_81
| spl1775_82
| spl1775_83
| ~ spl1775_86
| ~ spl1775_114 ),
inference(avatar_contradiction_clause,[],[f63484]) ).
cnf(s56,plain,
spl1775_75,
inference(sat_conversion,[],[f59745]) ).
cnf(s58,plain,
( ~ spl1775_80
| ~ spl1775_81
| spl1775_82
| ~ spl1775_83 ),
inference(sat_conversion,[],[f59813]) ).
cnf(s61,plain,
( ~ spl1775_80
| ~ spl1775_81
| spl1775_82
| spl1775_86 ),
inference(sat_conversion,[],[f59827]) ).
cnf(s71,plain,
spl1775_80,
inference(sat_conversion,[],[f59875]) ).
cnf(s74,plain,
~ spl1775_82,
inference(sat_conversion,[],[f59890]) ).
cnf(s75,plain,
spl1775_81,
inference(sat_conversion,[],[f59899]) ).
cnf(s85,plain,
( ~ spl1775_108
| spl1775_109 ),
inference(sat_conversion,[],[f60105]) ).
cnf(s86,plain,
spl1775_108,
inference(sat_conversion,[],[f60109]) ).
cnf(s88,plain,
( ~ spl1775_75
| spl1775_78
| ~ spl1775_108
| ~ spl1775_109 ),
inference(sat_conversion,[],[f60294]) ).
cnf(s91,plain,
( ~ spl1775_78
| spl1775_114
| ~ spl1775_115 ),
inference(sat_conversion,[],[f60523]) ).
cnf(s152,plain,
( ~ spl1775_108
| ~ spl1775_109
| spl1775_115 ),
inference(sat_conversion,[],[f63224]) ).
cnf(s156,plain,
( ~ spl1775_80
| ~ spl1775_81
| spl1775_82
| spl1775_83
| ~ spl1775_86
| ~ spl1775_114 ),
inference(sat_conversion,[],[f63485]) ).
cnf(s163,plain,
spl1775_109,
inference(rat,[],[s85,s86]) ).
cnf(s164,plain,
spl1775_115,
inference(rat,[],[s152,s86,s163]) ).
cnf(s186,plain,
spl1775_86,
inference(rat,[],[s61,s74,s75,s71]) ).
cnf(s189,plain,
~ spl1775_83,
inference(rat,[],[s58,s74,s75,s71]) ).
cnf(s190,plain,
~ spl1775_114,
inference(rat,[],[s156,s186,s71,s74,s75,s189]) ).
cnf(s191,plain,
~ spl1775_78,
inference(rat,[],[s91,s164,s190]) ).
cnf(s192,plain,
~ spl1775_75,
inference(rat,[],[s88,s163,s86,s191]) ).
cnf(s193,plain,
$false,
inference(rat,[],[s56,s192]) ).
fof(f63491,plain,
$false,
inference(avatar_sat_refutation,[],[s193]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LAT330+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.10 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.19/0.47 % Computer : n007.cluster.edu
% 0.19/0.47 % Model : x86_64 x86_64
% 0.19/0.47 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.47 % Memory : 8046.5625MB
% 0.19/0.47 % OS : Linux 6.8.0-71-generic
% 0.19/0.47 % CPULimit : 300
% 0.19/0.47 % WCLimit : 300
% 0.19/0.47 % DateTime : Sun Sep 27 14:39:45 UTC 2026
% 0.19/0.48 % CPUTime :
% 0.19/0.48 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.27/0.52 Running first-order theorem proving
% 0.27/0.52 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 21.59/6.67 % (1486641)Detected formulas, will run a generic FOF schedule.
% 21.59/6.67 % (1486652)dis-21_1_sil=8000:lcm=predicate:random_seed=4234566761:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2973 on theBenchmark for (2973ds/129Mi)
% 21.59/6.67 % (1486647)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=1918694525:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2973 on theBenchmark for (2973ds/134677Mi)
% 21.59/6.67 % (1486646)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=2968195746:i=141193_2973 on theBenchmark for (2973ds/141193Mi)
% 21.59/6.67 % (1486648)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=3060739685:i=141695:sd=1:nm=32:gsp=on:ss=included_2973 on theBenchmark for (2973ds/141695Mi)
% 21.59/6.67 % (1486650)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2326444867:i=119:av=off:ss=axioms_2973 on theBenchmark for (2973ds/119Mi)
% 21.59/6.67 % (1486649)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=4270741093:i=109:sd=1:ins=1:gsp=on:ss=axioms_2973 on theBenchmark for (2973ds/109Mi)
% 21.59/6.67 % (1486652)Instruction limit reached!
% 21.59/6.67 % (1486652)------------------------------
% 21.59/6.67 % (1486652)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.59/6.67 % (1486652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.59/6.67 % (1486652)CaDiCaL version: 2.1.3
% 21.59/6.67 % (1486652)Termination reason: Instruction limit
% 21.59/6.67 % (1486652)Termination phase: SInE selection
% 21.59/6.67 % (1486652)Time elapsed: 0.084 s
% 21.59/6.67 % (1486652)Peak memory usage: 136 MB
% 21.59/6.67 % (1486652)Instructions burned: 130 (million)
% 21.59/6.67 % (1486651)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3190871581:s2a=on:i=139:gtg=position_2973 on theBenchmark for (2973ds/139Mi)
% 21.59/6.67 % (1486649)Instruction limit reached!
% 21.59/6.67 % (1486649)------------------------------
% 21.59/6.67 % (1486649)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.59/6.67 % (1486649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.59/6.67 % (1486649)CaDiCaL version: 2.1.3
% 21.59/6.67 % (1486649)Termination reason: Instruction limit
% 21.59/6.67 % (1486649)Termination phase: SInE selection
% 21.59/6.67 % (1486649)Time elapsed: 0.117 s
% 21.59/6.67 % (1486649)Peak memory usage: 136 MB
% 21.59/6.67 % (1486649)Instructions burned: 109 (million)
% 21.59/6.67 % (1486651)Instruction limit reached!
% 21.59/6.67 % (1486651)------------------------------
% 21.59/6.67 % (1486651)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.59/6.67 % (1486651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.59/6.67 % (1486651)CaDiCaL version: 2.1.3
% 21.59/6.67 % (1486651)Termination reason: Instruction limit
% 21.59/6.67 % (1486651)Termination phase: Property scanning
% 21.59/6.67 % (1486651)Time elapsed: 0.121 s
% 21.59/6.67 % (1486651)Peak memory usage: 136 MB
% 21.59/6.67 % (1486651)Instructions burned: 141 (million)
% 21.59/6.67 % (1486650)Instruction limit reached!
% 21.59/6.67 % (1486650)------------------------------
% 21.59/6.67 % (1486650)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.59/6.67 % (1486650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.59/6.67 % (1486650)CaDiCaL version: 2.1.3
% 21.59/6.67 % (1486650)Termination reason: Instruction limit
% 21.59/6.67 % (1486650)Termination phase: SInE selection
% 21.59/6.67 % (1486650)Time elapsed: 0.128 s
% 21.59/6.67 % (1486650)Peak memory usage: 136 MB
% 21.59/6.67 % (1486650)Instructions burned: 121 (million)
% 21.59/6.67 % (1486660)lrs+10_1_sil=8000:sp=occurrence:random_seed=3159404644:i=285:sd=3:ss=axioms:sgt=8_2970 on theBenchmark for (2970ds/285Mi)
% 21.59/6.67 % (1486661)lrs+10_1_sil=32000:urr=on:br=off:random_seed=4214607394:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2968 on theBenchmark for (2968ds/157Mi)
% 21.59/6.67 % (1486663)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=1782907066:s2a=on:i=248:s2at=1.23:gtg=position_2968 on theBenchmark for (2968ds/248Mi)
% 21.59/6.67 % (1486660)Instruction limit reached!
% 21.59/6.67 % (1486660)------------------------------
% 21.59/6.67 % (1486660)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.34/8.25 % (1486660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.34/8.25 % (1486660)CaDiCaL version: 2.1.3
% 33.34/8.25 % (1486660)Termination reason: Instruction limit
% 33.34/8.25 % (1486660)Termination phase: Saturation
% 33.34/8.25 % (1486660)Time elapsed: 0.213 s
% 33.34/8.25 % (1486660)Peak memory usage: 142 MB
% 33.34/8.25 % (1486660)Instructions burned: 285 (million)
% 33.34/8.25 % (1486662)lrs+1011_1_sil=32000:sp=occurrence:random_seed=16401567:i=325:sd=1:ss=axioms:sgt=32_2968 on theBenchmark for (2968ds/325Mi)
% 33.34/8.25 % (1486661)Instruction limit reached!
% 33.34/8.25 % (1486661)------------------------------
% 33.34/8.25 % (1486661)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.34/8.25 % (1486661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.34/8.25 % (1486661)CaDiCaL version: 2.1.3
% 33.34/8.25 % (1486661)Termination reason: Instruction limit
% 33.34/8.25 % (1486661)Termination phase: Property scanning
% 33.34/8.25 % (1486661)Time elapsed: 0.135 s
% 33.34/8.25 % (1486661)Peak memory usage: 136 MB
% 33.34/8.25 % (1486661)Instructions burned: 157 (million)
% 33.34/8.25 % (1486668)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=4129418658:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2965 on theBenchmark for (2965ds/294Mi)
% 33.34/8.25 % (1486663)Instruction limit reached!
% 33.34/8.25 % (1486663)------------------------------
% 33.34/8.25 % (1486663)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.34/8.25 % (1486663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.34/8.25 % (1486663)CaDiCaL version: 2.1.3
% 33.34/8.25 % (1486663)Termination reason: Instruction limit
% 33.34/8.25 % (1486663)Termination phase: Property scanning
% 33.34/8.25 % (1486663)Time elapsed: 0.209 s
% 33.34/8.25 % (1486663)Peak memory usage: 136 MB
% 33.34/8.25 % (1486663)Instructions burned: 249 (million)
% 33.34/8.25 % (1486669)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2662997790:i=2350_2964 on theBenchmark for (2964ds/2350Mi)
% 33.34/8.25 % (1486662)Instruction limit reached!
% 33.34/8.25 % (1486662)------------------------------
% 33.34/8.25 % (1486662)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.34/8.25 % (1486662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.34/8.25 % (1486662)CaDiCaL version: 2.1.3
% 33.34/8.25 % (1486662)Termination reason: Instruction limit
% 33.34/8.25 % (1486662)Termination phase: Saturation
% 33.34/8.25 % (1486662)Time elapsed: 0.364 s
% 33.34/8.25 % (1486662)Peak memory usage: 142 MB
% 33.34/8.25 % (1486662)Instructions burned: 325 (million)
% 33.34/8.25 % (1486668)Instruction limit reached!
% 33.34/8.25 % (1486668)------------------------------
% 33.34/8.25 % (1486668)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.34/8.25 % (1486668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.34/8.25 % (1486668)CaDiCaL version: 2.1.3
% 33.34/8.25 % (1486668)Termination reason: Instruction limit
% 33.34/8.25 % (1486668)Termination phase: SInE selection
% 33.34/8.25 % (1486668)Time elapsed: 0.278 s
% 33.34/8.25 % (1486668)Peak memory usage: 137 MB
% 33.34/8.25 % (1486668)Instructions burned: 294 (million)
% 33.34/8.25 % (1486671)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3768843033:cts=off:i=113:fsr=off:ss=included:sgt=4_2963 on theBenchmark for (2963ds/113Mi)
% 33.34/8.25 % (1486673)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=306117051:i=127:av=off:fsr=off:sup=off_2962 on theBenchmark for (2962ds/127Mi)
% 33.34/8.25 % (1486673)Instruction limit reached!
% 33.34/8.25 % (1486673)------------------------------
% 33.34/8.25 % (1486673)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.34/8.25 % (1486673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.34/8.25 % (1486673)CaDiCaL version: 2.1.3
% 33.34/8.25 % (1486673)Termination reason: Instruction limit
% 33.34/8.25 % (1486673)Termination phase: Preprocessing 1
% 33.34/8.25 % (1486673)Time elapsed: 0.056 s
% 33.34/8.25 % (1486673)Peak memory usage: 138 MB
% 33.34/8.25 % (1486673)Instructions burned: 128 (million)
% 33.34/8.25 % (1486671)Instruction limit reached!
% 33.34/8.25 % (1486671)------------------------------
% 33.34/8.25 % (1486671)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.34/8.25 % (1486671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.34/8.25 % (1486671)CaDiCaL version: 2.1.3
% 18.63/9.08 % (1486671)Termination reason: Instruction limit
% 18.63/9.08 % (1486671)Termination phase: SInE selection
% 18.63/9.08 % (1486671)Time elapsed: 0.125 s
% 18.63/9.08 % (1486671)Peak memory usage: 136 MB
% 18.63/9.08 % (1486671)Instructions burned: 113 (million)
% 18.63/9.08 % (1486674)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=495162713:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2961 on theBenchmark for (2961ds/114Mi)
% 18.63/9.08 % (1486674)Instruction limit reached!
% 18.63/9.08 % (1486674)------------------------------
% 18.63/9.08 % (1486674)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.63/9.08 % (1486674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.63/9.08 % (1486674)CaDiCaL version: 2.1.3
% 18.63/9.08 % (1486674)Termination reason: Instruction limit
% 18.63/9.08 % (1486674)Termination phase: Property scanning
% 18.63/9.08 % (1486674)Time elapsed: 0.055 s
% 18.63/9.08 % (1486674)Peak memory usage: 136 MB
% 18.63/9.08 % (1486674)Instructions burned: 117 (million)
% 18.63/9.08 % (1486678)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=389722409:i=437:sd=1:aac=none:ss=included_2959 on theBenchmark for (2959ds/437Mi)
% 18.63/9.08 % (1486677)lrs+10_1_sil=8000:sp=occurrence:random_seed=3969809343:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2960 on theBenchmark for (2960ds/907Mi)
% 18.63/9.08 % (1486680)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3138473032:i=5202:ss=axioms:sgt=16_2958 on theBenchmark for (2958ds/5202Mi)
% 18.63/9.08 % (1486678)Instruction limit reached!
% 18.63/9.08 % (1486678)------------------------------
% 18.63/9.08 % (1486678)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.63/9.08 % (1486678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.63/9.08 % (1486678)CaDiCaL version: 2.1.3
% 18.63/9.08 % (1486678)Termination reason: Instruction limit
% 18.63/9.08 % (1486678)Termination phase: Saturation
% 18.63/9.08 % (1486678)Time elapsed: 0.176 s
% 18.63/9.08 % (1486678)Peak memory usage: 144 MB
% 18.63/9.08 % (1486678)Instructions burned: 438 (million)
% 18.63/9.08 % (1486684)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3949609987:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2956 on theBenchmark for (2956ds/134Mi)
% 18.63/9.08 % (1486684)Instruction limit reached!
% 18.63/9.08 % (1486684)------------------------------
% 18.63/9.08 % (1486684)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.63/9.08 % (1486684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.63/9.08 % (1486684)CaDiCaL version: 2.1.3
% 18.63/9.08 % (1486684)Termination reason: Instruction limit
% 18.63/9.08 % (1486684)Termination phase: SInE selection
% 18.63/9.08 % (1486684)Time elapsed: 0.059 s
% 18.63/9.08 % (1486684)Peak memory usage: 136 MB
% 18.63/9.08 % (1486684)Instructions burned: 135 (million)
% 18.63/9.08 % (1486686)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=4201472524:st=8:i=592:sd=3:ep=RST:ss=axioms_2954 on theBenchmark for (2954ds/592Mi)
% 18.63/9.08 % (1486686)Instruction limit reached!
% 18.63/9.08 % (1486686)------------------------------
% 18.63/9.08 % (1486686)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.63/9.08 % (1486686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.63/9.08 % (1486686)CaDiCaL version: 2.1.3
% 18.63/9.08 % (1486686)Termination reason: Instruction limit
% 18.63/9.08 % (1486686)Termination phase: Naming
% 18.63/9.08 % (1486686)Time elapsed: 0.277 s
% 18.63/9.08 % (1486686)Peak memory usage: 154 MB
% 18.63/9.08 % (1486686)Instructions burned: 592 (million)
% 18.63/9.08 % (1486688)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2556795972:st=3:i=13193:sd=3:ss=axioms_2950 on theBenchmark for (2950ds/13193Mi)
% 18.63/9.08 % (1486677)Instruction limit reached!
% 18.63/9.08 % (1486677)------------------------------
% 18.63/9.08 % (1486677)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.63/9.08 % (1486677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.63/9.08 % (1486677)CaDiCaL version: 2.1.3
% 18.63/9.08 % (1486677)Termination reason: Instruction limit
% 18.63/9.08 % (1486677)Termination phase: Property scanning
% 18.63/9.08 % (1486677)Time elapsed: 0.951 s
% 18.63/9.08 % (1486677)Peak memory usage: 158 MB
% 18.63/9.08 % (1486677)Instructions burned: 908 (million)
% 18.63/9.08 % (1486690)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=197444326:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2948 on theBenchmark for (2948ds/125Mi)
% 18.63/9.08 % (1486690)Instruction limit reached!
% 18.63/9.08 % (1486690)------------------------------
% 18.63/9.08 % (1486690)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.63/9.08 % (1486690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.63/9.08 % (1486690)CaDiCaL version: 2.1.3
% 18.63/9.08 % (1486690)Termination reason: Instruction limit
% 18.63/9.08 % (1486690)Termination phase: Property scanning
% 18.63/9.08 % (1486690)Time elapsed: 0.063 s
% 18.63/9.08 % (1486690)Peak memory usage: 137 MB
% 18.63/9.08 % (1486690)Instructions burned: 126 (million)
% 18.63/9.08 % (1486692)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3940853368:i=134:gtgl=5:slsql=off:gtg=exists_sym_2945 on theBenchmark for (2945ds/134Mi)
% 18.63/9.08 % (1486692)Instruction limit reached!
% 18.63/9.08 % (1486692)------------------------------
% 18.63/9.08 % (1486692)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.63/9.08 % (1486692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.63/9.08 % (1486692)CaDiCaL version: 2.1.3
% 18.63/9.08 % (1486692)Termination reason: Instruction limit
% 18.63/9.08 % (1486692)Termination phase: Property scanning
% 18.63/9.08 % (1486692)Time elapsed: 0.061 s
% 18.63/9.08 % (1486692)Peak memory usage: 136 MB
% 18.63/9.08 % (1486692)Instructions burned: 134 (million)
% 18.63/9.08 % (1486694)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2989879334:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2943 on theBenchmark for (2943ds/141Mi)
% 18.63/9.08 % (1486669)Instruction limit reached!
% 18.63/9.08 % (1486669)------------------------------
% 18.63/9.08 % (1486669)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.63/9.08 % (1486669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.63/9.08 % (1486669)CaDiCaL version: 2.1.3
% 18.63/9.08 % (1486669)Termination reason: Instruction limit
% 18.63/9.08 % (1486669)Termination phase: Property scanning
% 18.63/9.08 % (1486669)Time elapsed: 2.292 s
% 18.63/9.08 % (1486669)Peak memory usage: 233 MB
% 18.63/9.08 % (1486669)Instructions burned: 2351 (million)
% 18.63/9.08 % (1486694)Instruction limit reached!
% 18.63/9.08 % (1486694)------------------------------
% 18.63/9.08 % (1486694)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.63/9.08 % (1486694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.63/9.08 % (1486694)CaDiCaL version: 2.1.3
% 18.63/9.08 % (1486694)Termination reason: Instruction limit
% 18.63/9.08 % (1486694)Termination phase: SInE selection
% 18.63/9.08 % (1486694)Time elapsed: 0.108 s
% 18.63/9.08 % (1486694)Peak memory usage: 136 MB
% 18.63/9.08 % (1486694)Instructions burned: 141 (million)
% 18.63/9.08 % (1486697)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=3968344852:i=6060:aac=none:ins=25_2940 on theBenchmark for (2940ds/6060Mi)
% 18.63/9.08 % (1486696)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3130853702:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2940 on theBenchmark for (2940ds/431Mi)
% 18.63/9.08 % (1486696)Refutation not found, incomplete strategy
% 18.63/9.08 % (1486696)------------------------------
% 18.63/9.08 % (1486696)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.63/9.08 % (1486696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.63/9.08 % (1486696)CaDiCaL version: 2.1.3
% 18.63/9.08 % (1486696)Termination reason: Refutation not found, incomplete strategy
% 18.63/9.08 % (1486696)Time elapsed: 0.198 s
% 18.63/9.08 % (1486696)Peak memory usage: 142 MB
% 18.63/9.08 % (1486696)Instructions burned: 246 (million)
% 18.63/9.08 % (1486696)------------------------------
% 18.63/9.08 % (1486696)------------------------------
% 18.63/9.08 % (1486701)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=2700168612:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2933 on theBenchmark for (2933ds/150Mi)
% 18.63/9.08 % (1486701)Instruction limit reached!
% 18.63/9.08 % (1486701)------------------------------
% 18.63/9.08 % (1486701)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.63/9.08 % (1486701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.63/9.08 % (1486701)CaDiCaL version: 2.1.3
% 18.63/9.08 % (1486701)Termination reason: Instruction limit
% 18.63/9.08 % (1486701)Termination phase: SInE selection
% 18.63/9.08 % (1486701)Time elapsed: 0.115 s
% 18.63/9.08 % (1486701)Peak memory usage: 136 MB
% 18.63/9.08 % (1486701)Instructions burned: 151 (million)
% 18.63/9.08 % (1486703)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=704427895:i=14155:bd=all_2930 on theBenchmark for (2930ds/14155Mi)
% 18.63/9.08 % (1486688)First to succeed.
% 18.63/9.08 % (1486688)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1486641"
% 18.63/9.08 % (1486688)Refutation found. Thanks to Tanya!
% 18.63/9.08 % SZS status Theorem for theBenchmark
% 18.63/9.08 % SZS output start Proof for theBenchmark
% See solution above
% 39.64/9.32 % (1486688)------------------------------
% 39.64/9.32 % (1486688)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.64/9.32 % (1486688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.64/9.32 % (1486688)CaDiCaL version: 2.1.3
% 39.64/9.32 % (1486688)Termination reason: Refutation
% 39.64/9.32 % (1486688)Time elapsed: 2.445 s
% 39.64/9.32 % (1486688)Peak memory usage: 346 MB
% 39.64/9.32 % (1486688)Instructions burned: 7044 (million)
% 39.64/9.32 % (1486688)------------------------------
% 39.64/9.32 % (1486688)------------------------------
% 39.64/9.32 % (1486641)Success in time 7.779 s
% 39.64/9.32 % Vampire exiting
%------------------------------------------------------------------------------