%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LAT307+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:48:20 AM UTC 2026
% Result : Theorem 80.20s 13.67s
% Output : Refutation 80.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 43
% Syntax : Number of formulae : 370 ( 42 unt; 19 def)
% Number of atoms : 1374 ( 155 equ)
% Maximal formula atoms : 12 ( 3 avg)
% Number of connectives : 1548 ( 544 ~; 819 |; 115 &)
% ( 29 <=>; 41 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 48 ( 46 usr; 20 prp; 0-3 aty)
% Number of functors : 14 ( 14 usr; 2 con; 0-3 aty)
% Number of variables : 320 ( 0 sgn 314 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( v14_lattices(X0)
=> ! [X1] :
( m2_filter_2(X1,X0)
=> ~ ( X1 != u1_struct_0(X0)
& ! [X2] :
( m2_filter_2(X2,X0)
=> ~ ( r1_tarski(X1,X2)
& r2_filter_2(X0,X2) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t34_filter_2) ).
fof(f2,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( v14_lattices(X0)
=> ! [X1] :
( m2_filter_2(X1,X0)
=> ~ ( X1 != u1_struct_0(X0)
& ! [X2] :
( m2_filter_2(X2,X0)
=> ~ ( r1_tarski(X1,X2)
& r2_filter_2(X0,X2) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,axiom,
! [X0] :
( l3_lattices(X0)
=> ( v3_lattices(X0)
=> X0 = g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',abstractness_v3_lattices) ).
fof(f12,axiom,
! [X0] :
( l3_lattices(X0)
=> k1_lattice2(X0) = g3_lattices(u1_struct_0(X0),u1_lattices(X0),u2_lattices(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d2_lattice2) ).
fof(f13,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
=> k7_filter_2(X0,X1) = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d6_filter_2) ).
fof(f14,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(k1_lattice2(X0))))
=> k8_filter_2(X0,X1) = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d7_filter_2) ).
fof(f16,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& m1_filter_0(X1,k1_lattice2(X0)) )
=> m2_filter_2(k14_filter_2(X0,X1),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k14_filter_2) ).
fof(f17,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& m2_filter_2(X1,X0) )
=> m1_filter_2(k15_filter_2(X0,X1),k1_lattice2(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k15_filter_2) ).
fof(f18,axiom,
! [X0] :
( l3_lattices(X0)
=> ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k1_lattice2) ).
fof(f27,axiom,
! [X0] :
( l3_lattices(X0)
=> ( l1_lattices(X0)
& l2_lattices(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l3_lattices) ).
fof(f28,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/sandbox2/benchmark/theBenchmark.p',dt_m1_filter_0) ).
fof(f32,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_filter_2(X1,X0)
=> ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m2_filter_2) ).
fof(f33,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_lattice4(X1,X0)
=> m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m2_lattice4) ).
fof(f35,axiom,
! [X0] :
( l1_lattices(X0)
=> ( v1_funct_1(u1_lattices(X0))
& v1_funct_2(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
& m2_relset_1(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_u1_lattices) ).
fof(f37,axiom,
! [X0] :
( l2_lattices(X0)
=> ( v1_funct_1(u2_lattices(X0))
& v1_funct_2(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
& m2_relset_1(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_u2_lattices) ).
fof(f50,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l3_lattices(X0) )
=> ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_lattice2) ).
fof(f61,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/sandbox2/benchmark/theBenchmark.p',fc6_lattice2) ).
fof(f62,axiom,
! [X0,X1,X2] :
( ( v1_funct_1(X1)
& v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
& m1_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
& v1_funct_1(X2)
& v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
& m1_relset_1(X2,k2_zfmisc_1(X0,X0),X0) )
=> ! [X3,X4,X5] :
( g3_lattices(X0,X1,X2) = g3_lattices(X3,X4,X5)
=> ( X0 = X3
& X1 = X4
& X2 = X5 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',free_g3_lattices) ).
fof(f77,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& m1_filter_0(X1,k1_lattice2(X0)) )
=> k14_filter_2(X0,X1) = k8_filter_2(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k14_filter_2) ).
fof(f78,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& m2_filter_2(X1,X0) )
=> k15_filter_2(X0,X1) = k7_filter_2(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k15_filter_2) ).
fof(f79,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/sandbox2/benchmark/theBenchmark.p',redefinition_m1_filter_2) ).
fof(f80,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
<=> m1_relset_1(X2,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(f83,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( v13_lattices(X0)
=> ! [X1] :
( m1_filter_0(X1,X0)
=> ~ ( X1 != u1_struct_0(X0)
& ! [X2] :
( m1_filter_0(X2,X0)
=> ~ ( r1_tarski(X1,X2)
& v1_filter_0(X2,X0) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t22_filter_0) ).
fof(f85,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_filter_2(X1,X0)
=> ( r2_filter_2(X0,X1)
<=> v1_filter_0(k15_filter_2(X0,X1),k1_lattice2(X0)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t33_filter_2) ).
fof(f89,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( v14_lattices(X0)
<=> v13_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t64_lattice2) ).
fof(f104,plain,
? [X0] :
( ? [X1] :
( X1 != u1_struct_0(X0)
& ! [X2] :
( ~ r1_tarski(X1,X2)
| ~ r2_filter_2(X0,X2)
| ~ m2_filter_2(X2,X0) )
& m2_filter_2(X1,X0) )
& v14_lattices(X0)
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(ennf_transformation,[],[f2]) ).
fof(f105,plain,
? [X0] :
( ? [X1] :
( X1 != u1_struct_0(X0)
& ! [X2] :
( ~ r1_tarski(X1,X2)
| ~ r2_filter_2(X0,X2)
| ~ m2_filter_2(X2,X0) )
& m2_filter_2(X1,X0) )
& v14_lattices(X0)
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(flattening,[],[f104]) ).
fof(f106,plain,
! [X0] :
( X0 = g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))
| ~ v3_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f3]) ).
fof(f107,plain,
! [X0] :
( X0 = g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))
| ~ v3_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f106]) ).
fof(f121,plain,
! [X0] :
( k1_lattice2(X0) = g3_lattices(u1_struct_0(X0),u1_lattices(X0),u2_lattices(X0))
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f12]) ).
fof(f122,plain,
! [X0] :
( ! [X1] :
( k7_filter_2(X0,X1) = X1
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f13]) ).
fof(f123,plain,
! [X0] :
( ! [X1] :
( k7_filter_2(X0,X1) = X1
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f122]) ).
fof(f124,plain,
! [X0] :
( ! [X1] :
( k8_filter_2(X0,X1) = X1
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(k1_lattice2(X0)))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f14]) ).
fof(f125,plain,
! [X0] :
( ! [X1] :
( k8_filter_2(X0,X1) = X1
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(k1_lattice2(X0)))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f124]) ).
fof(f128,plain,
! [X0,X1] :
( m2_filter_2(k14_filter_2(X0,X1),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_filter_0(X1,k1_lattice2(X0)) ),
inference(ennf_transformation,[],[f16]) ).
fof(f129,plain,
! [X0,X1] :
( m2_filter_2(k14_filter_2(X0,X1),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_filter_0(X1,k1_lattice2(X0)) ),
inference(flattening,[],[f128]) ).
fof(f130,plain,
! [X0,X1] :
( m1_filter_2(k15_filter_2(X0,X1),k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m2_filter_2(X1,X0) ),
inference(ennf_transformation,[],[f17]) ).
fof(f131,plain,
! [X0,X1] :
( m1_filter_2(k15_filter_2(X0,X1),k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m2_filter_2(X1,X0) ),
inference(flattening,[],[f130]) ).
fof(f132,plain,
! [X0] :
( ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f18]) ).
fof(f139,plain,
! [X0] :
( ( l1_lattices(X0)
& l2_lattices(X0) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f27]) ).
fof(f140,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,[],[f28]) ).
fof(f141,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,[],[f140]) ).
fof(f144,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,[],[f32]) ).
fof(f145,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,[],[f144]) ).
fof(f146,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,[],[f33]) ).
fof(f147,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,[],[f146]) ).
fof(f149,plain,
! [X0] :
( ( v1_funct_1(u1_lattices(X0))
& v1_funct_2(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
& m2_relset_1(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0)) )
| ~ l1_lattices(X0) ),
inference(ennf_transformation,[],[f35]) ).
fof(f150,plain,
! [X0] :
( ( v1_funct_1(u2_lattices(X0))
& v1_funct_2(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
& m2_relset_1(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0)) )
| ~ l2_lattices(X0) ),
inference(ennf_transformation,[],[f37]) ).
fof(f161,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f50]) ).
fof(f162,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f161]) ).
fof(f179,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,[],[f61]) ).
fof(f180,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,[],[f179]) ).
fof(f181,plain,
! [X0,X1,X2] :
( ! [X3,X4,X5] :
( ( X0 = X3
& X1 = X4
& X2 = X5 )
| g3_lattices(X0,X1,X2) != g3_lattices(X3,X4,X5) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m1_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m1_relset_1(X2,k2_zfmisc_1(X0,X0),X0) ),
inference(ennf_transformation,[],[f62]) ).
fof(f182,plain,
! [X0,X1,X2] :
( ! [X3,X4,X5] :
( ( X0 = X3
& X1 = X4
& X2 = X5 )
| g3_lattices(X0,X1,X2) != g3_lattices(X3,X4,X5) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m1_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m1_relset_1(X2,k2_zfmisc_1(X0,X0),X0) ),
inference(flattening,[],[f181]) ).
fof(f188,plain,
! [X0,X1] :
( k14_filter_2(X0,X1) = k8_filter_2(X0,X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_filter_0(X1,k1_lattice2(X0)) ),
inference(ennf_transformation,[],[f77]) ).
fof(f189,plain,
! [X0,X1] :
( k14_filter_2(X0,X1) = k8_filter_2(X0,X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_filter_0(X1,k1_lattice2(X0)) ),
inference(flattening,[],[f188]) ).
fof(f190,plain,
! [X0,X1] :
( k15_filter_2(X0,X1) = k7_filter_2(X0,X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m2_filter_2(X1,X0) ),
inference(ennf_transformation,[],[f78]) ).
fof(f191,plain,
! [X0,X1] :
( k15_filter_2(X0,X1) = k7_filter_2(X0,X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m2_filter_2(X1,X0) ),
inference(flattening,[],[f190]) ).
fof(f192,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,[],[f79]) ).
fof(f193,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,[],[f192]) ).
fof(f195,plain,
! [X0] :
( ! [X1] :
( u1_struct_0(X0) = X1
| ? [X2] :
( r1_tarski(X1,X2)
& v1_filter_0(X2,X0)
& m1_filter_0(X2,X0) )
| ~ m1_filter_0(X1,X0) )
| ~ v13_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f83]) ).
fof(f196,plain,
! [X0] :
( ! [X1] :
( u1_struct_0(X0) = X1
| ? [X2] :
( r1_tarski(X1,X2)
& v1_filter_0(X2,X0)
& m1_filter_0(X2,X0) )
| ~ m1_filter_0(X1,X0) )
| ~ v13_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f195]) ).
fof(f199,plain,
! [X0] :
( ! [X1] :
( ( r2_filter_2(X0,X1)
<=> v1_filter_0(k15_filter_2(X0,X1),k1_lattice2(X0)) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f85]) ).
fof(f200,plain,
! [X0] :
( ! [X1] :
( ( r2_filter_2(X0,X1)
<=> v1_filter_0(k15_filter_2(X0,X1),k1_lattice2(X0)) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f199]) ).
fof(f204,plain,
! [X0] :
( ( v14_lattices(X0)
<=> v13_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f89]) ).
fof(f205,plain,
! [X0] :
( ( v14_lattices(X0)
<=> v13_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f204]) ).
fof(f209,plain,
! [X2] :
( ~ m2_filter_2(X2,sK0)
| ~ r2_filter_2(sK0,X2)
| ~ r1_tarski(sK1,X2) ),
inference(cnf_transformation,[],[f105]) ).
fof(f210,plain,
m2_filter_2(sK1,sK0),
inference(cnf_transformation,[],[f105]) ).
fof(f211,plain,
sK1 != u1_struct_0(sK0),
inference(cnf_transformation,[],[f105]) ).
fof(f212,plain,
l3_lattices(sK0),
inference(cnf_transformation,[],[f105]) ).
fof(f213,plain,
v10_lattices(sK0),
inference(cnf_transformation,[],[f105]) ).
fof(f214,plain,
~ v3_struct_0(sK0),
inference(cnf_transformation,[],[f105]) ).
fof(f215,plain,
v14_lattices(sK0),
inference(cnf_transformation,[],[f105]) ).
fof(f216,plain,
! [X0] :
( ~ l3_lattices(X0)
| ~ v3_lattices(X0)
| g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) = X0 ),
inference(cnf_transformation,[],[f107]) ).
fof(f230,plain,
! [X0] :
( ~ l3_lattices(X0)
| k1_lattice2(X0) = g3_lattices(u1_struct_0(X0),u1_lattices(X0),u2_lattices(X0)) ),
inference(cnf_transformation,[],[f121]) ).
fof(f231,plain,
! [X0,X1] :
( ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| k7_filter_2(X0,X1) = X1 ),
inference(cnf_transformation,[],[f123]) ).
fof(f232,plain,
! [X0,X1] :
( ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(k1_lattice2(X0))))
| k8_filter_2(X0,X1) = X1 ),
inference(cnf_transformation,[],[f125]) ).
fof(f235,plain,
! [X0,X1] :
( ~ m1_filter_0(X1,k1_lattice2(X0))
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| m2_filter_2(k14_filter_2(X0,X1),X0) ),
inference(cnf_transformation,[],[f129]) ).
fof(f236,plain,
! [X0,X1] :
( ~ m2_filter_2(X1,X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| m1_filter_2(k15_filter_2(X0,X1),k1_lattice2(X0)) ),
inference(cnf_transformation,[],[f131]) ).
fof(f237,plain,
! [X0] :
( ~ l3_lattices(X0)
| l3_lattices(k1_lattice2(X0)) ),
inference(cnf_transformation,[],[f132]) ).
fof(f238,plain,
! [X0] :
( ~ l3_lattices(X0)
| v3_lattices(k1_lattice2(X0)) ),
inference(cnf_transformation,[],[f132]) ).
fof(f243,plain,
! [X0] :
( ~ l3_lattices(X0)
| l2_lattices(X0) ),
inference(cnf_transformation,[],[f139]) ).
fof(f244,plain,
! [X0] :
( ~ l3_lattices(X0)
| l1_lattices(X0) ),
inference(cnf_transformation,[],[f139]) ).
fof(f245,plain,
! [X0,X1] :
( ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ m1_filter_0(X1,X0)
| m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ),
inference(cnf_transformation,[],[f141]) ).
fof(f249,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,[],[f145]) ).
fof(f251,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,[],[f147]) ).
fof(f253,plain,
! [X0] :
( ~ l1_lattices(X0)
| m2_relset_1(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f149]) ).
fof(f254,plain,
! [X0] :
( v1_funct_2(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| ~ l1_lattices(X0) ),
inference(cnf_transformation,[],[f149]) ).
fof(f255,plain,
! [X0] :
( v1_funct_1(u1_lattices(X0))
| ~ l1_lattices(X0) ),
inference(cnf_transformation,[],[f149]) ).
fof(f256,plain,
! [X0] :
( ~ l2_lattices(X0)
| m2_relset_1(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f150]) ).
fof(f257,plain,
! [X0] :
( ~ l2_lattices(X0)
| v1_funct_2(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f150]) ).
fof(f258,plain,
! [X0] :
( ~ l2_lattices(X0)
| v1_funct_1(u2_lattices(X0)) ),
inference(cnf_transformation,[],[f150]) ).
fof(f272,plain,
! [X0] :
( ~ l3_lattices(X0)
| v3_struct_0(X0)
| ~ v3_struct_0(k1_lattice2(X0)) ),
inference(cnf_transformation,[],[f162]) ).
fof(f292,plain,
! [X0] :
( ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| v10_lattices(k1_lattice2(X0)) ),
inference(cnf_transformation,[],[f180]) ).
fof(f303,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ m1_relset_1(X2,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X2)
| ~ m1_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X1)
| g3_lattices(X0,X1,X2) != g3_lattices(X3,X4,X5)
| X0 = X3 ),
inference(cnf_transformation,[],[f182]) ).
fof(f351,plain,
! [X0,X1] :
( ~ m1_filter_0(X1,k1_lattice2(X0))
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| k8_filter_2(X0,X1) = k14_filter_2(X0,X1) ),
inference(cnf_transformation,[],[f189]) ).
fof(f352,plain,
! [X0,X1] :
( ~ m2_filter_2(X1,X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| k7_filter_2(X0,X1) = k15_filter_2(X0,X1) ),
inference(cnf_transformation,[],[f191]) ).
fof(f354,plain,
! [X0,X1] :
( ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| m1_filter_0(X1,X0)
| ~ m1_filter_2(X1,X0) ),
inference(cnf_transformation,[],[f193]) ).
fof(f356,plain,
! [X2,X0,X1] :
( m1_relset_1(X2,X0,X1)
| ~ m2_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f80]) ).
fof(f359,plain,
! [X0,X1] :
( ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ v13_lattices(X0)
| ~ m1_filter_0(X1,X0)
| m1_filter_0(sK27(X0,X1),X0)
| u1_struct_0(X0) = X1 ),
inference(cnf_transformation,[],[f196]) ).
fof(f360,plain,
! [X0,X1] :
( ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ v13_lattices(X0)
| ~ m1_filter_0(X1,X0)
| v1_filter_0(sK27(X0,X1),X0)
| u1_struct_0(X0) = X1 ),
inference(cnf_transformation,[],[f196]) ).
fof(f361,plain,
! [X0,X1] :
( ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ v13_lattices(X0)
| ~ m1_filter_0(X1,X0)
| r1_tarski(X1,sK27(X0,X1))
| u1_struct_0(X0) = X1 ),
inference(cnf_transformation,[],[f196]) ).
fof(f363,plain,
! [X0,X1] :
( ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ m2_filter_2(X1,X0)
| ~ v1_filter_0(k15_filter_2(X0,X1),k1_lattice2(X0))
| r2_filter_2(X0,X1) ),
inference(cnf_transformation,[],[f200]) ).
fof(f370,plain,
! [X0] :
( ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| v13_lattices(k1_lattice2(X0))
| ~ v14_lattices(X0) ),
inference(cnf_transformation,[],[f205]) ).
fof(f374,plain,
~ l3_lattices(sK0),
inference(consistent_polarity_flipping,[],[f212]) ).
fof(f375,plain,
! [X2] :
( ~ r1_tarski(sK1,X2)
| r2_filter_2(sK0,X2)
| ~ m2_filter_2(X2,sK0) ),
inference(consistent_polarity_flipping,[],[f209]) ).
fof(f376,plain,
! [X0] :
( v3_lattices(X0)
| l3_lattices(X0)
| g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) = X0 ),
inference(consistent_polarity_flipping,[],[f216]) ).
fof(f389,plain,
! [X0] :
( l3_lattices(X0)
| k1_lattice2(X0) = g3_lattices(u1_struct_0(X0),u1_lattices(X0),u2_lattices(X0)) ),
inference(consistent_polarity_flipping,[],[f230]) ).
fof(f390,plain,
! [X0,X1] :
( ~ v10_lattices(X0)
| l3_lattices(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| k7_filter_2(X0,X1) = X1 ),
inference(consistent_polarity_flipping,[],[f231]) ).
fof(f391,plain,
! [X0,X1] :
( ~ v10_lattices(X0)
| l3_lattices(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(k1_lattice2(X0))))
| k8_filter_2(X0,X1) = X1 ),
inference(consistent_polarity_flipping,[],[f232]) ).
fof(f394,plain,
! [X0,X1] :
( m2_filter_2(k14_filter_2(X0,X1),X0)
| l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| m1_filter_0(X1,k1_lattice2(X0)) ),
inference(consistent_polarity_flipping,[],[f235]) ).
fof(f395,plain,
! [X0,X1] :
( m1_filter_2(k15_filter_2(X0,X1),k1_lattice2(X0))
| l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ m2_filter_2(X1,X0) ),
inference(consistent_polarity_flipping,[],[f236]) ).
fof(f396,plain,
! [X0] :
( ~ v3_lattices(k1_lattice2(X0))
| l3_lattices(X0) ),
inference(consistent_polarity_flipping,[],[f238]) ).
fof(f397,plain,
! [X0] :
( ~ l3_lattices(k1_lattice2(X0))
| l3_lattices(X0) ),
inference(consistent_polarity_flipping,[],[f237]) ).
fof(f401,plain,
! [X0] :
( l1_lattices(X0)
| l3_lattices(X0) ),
inference(consistent_polarity_flipping,[],[f244]) ).
fof(f402,plain,
! [X0] :
( ~ l2_lattices(X0)
| l3_lattices(X0) ),
inference(consistent_polarity_flipping,[],[f243]) ).
fof(f404,plain,
! [X0,X1] :
( ~ v10_lattices(X0)
| l3_lattices(X0)
| v3_struct_0(X0)
| m1_filter_0(X1,X0)
| m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ),
inference(consistent_polarity_flipping,[],[f245]) ).
fof(f408,plain,
! [X0,X1] :
( m2_lattice4(X1,X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ m2_filter_2(X1,X0)
| l3_lattices(X0) ),
inference(consistent_polarity_flipping,[],[f249]) ).
fof(f409,plain,
! [X0,X1] :
( ~ v10_lattices(X0)
| l3_lattices(X0)
| v3_struct_0(X0)
| ~ m2_lattice4(X1,X0)
| m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ),
inference(consistent_polarity_flipping,[],[f251]) ).
fof(f411,plain,
! [X0] :
( ~ m2_relset_1(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| ~ l1_lattices(X0) ),
inference(consistent_polarity_flipping,[],[f253]) ).
fof(f412,plain,
! [X0] :
( v1_funct_1(u2_lattices(X0))
| l2_lattices(X0) ),
inference(consistent_polarity_flipping,[],[f258]) ).
fof(f413,plain,
! [X0] :
( v1_funct_2(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| l2_lattices(X0) ),
inference(consistent_polarity_flipping,[],[f257]) ).
fof(f414,plain,
! [X0] :
( ~ m2_relset_1(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| l2_lattices(X0) ),
inference(consistent_polarity_flipping,[],[f256]) ).
fof(f424,plain,
! [X0] :
( ~ v3_struct_0(k1_lattice2(X0))
| v3_struct_0(X0)
| l3_lattices(X0) ),
inference(consistent_polarity_flipping,[],[f272]) ).
fof(f453,plain,
! [X0] :
( v10_lattices(k1_lattice2(X0))
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| l3_lattices(X0) ),
inference(consistent_polarity_flipping,[],[f292]) ).
fof(f454,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X2)
| m1_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| m1_relset_1(X2,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X1)
| g3_lattices(X0,X1,X2) != g3_lattices(X3,X4,X5)
| X0 = X3 ),
inference(consistent_polarity_flipping,[],[f303]) ).
fof(f482,plain,
! [X0,X1] :
( m1_filter_0(X1,k1_lattice2(X0))
| l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| k8_filter_2(X0,X1) = k14_filter_2(X0,X1) ),
inference(consistent_polarity_flipping,[],[f351]) ).
fof(f483,plain,
! [X0,X1] :
( ~ m2_filter_2(X1,X0)
| l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| k7_filter_2(X0,X1) = k15_filter_2(X0,X1) ),
inference(consistent_polarity_flipping,[],[f352]) ).
fof(f484,plain,
! [X0,X1] :
( ~ m1_filter_2(X1,X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ m1_filter_0(X1,X0)
| l3_lattices(X0) ),
inference(consistent_polarity_flipping,[],[f354]) ).
fof(f486,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,X0,X1)
| m2_relset_1(X2,X0,X1) ),
inference(consistent_polarity_flipping,[],[f356]) ).
fof(f489,plain,
! [X0,X1] :
( ~ v13_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| l3_lattices(X0)
| m1_filter_0(X1,X0)
| r1_tarski(X1,sK27(X0,X1))
| u1_struct_0(X0) = X1 ),
inference(consistent_polarity_flipping,[],[f361]) ).
fof(f490,plain,
! [X0,X1] :
( ~ v1_filter_0(sK27(X0,X1),X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ v13_lattices(X0)
| m1_filter_0(X1,X0)
| l3_lattices(X0)
| u1_struct_0(X0) = X1 ),
inference(consistent_polarity_flipping,[],[f360]) ).
fof(f491,plain,
! [X0,X1] :
( ~ v13_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| l3_lattices(X0)
| m1_filter_0(X1,X0)
| ~ m1_filter_0(sK27(X0,X1),X0)
| u1_struct_0(X0) = X1 ),
inference(consistent_polarity_flipping,[],[f359]) ).
fof(f494,plain,
! [X0,X1] :
( ~ r2_filter_2(X0,X1)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ m2_filter_2(X1,X0)
| v1_filter_0(k15_filter_2(X0,X1),k1_lattice2(X0))
| l3_lattices(X0) ),
inference(consistent_polarity_flipping,[],[f363]) ).
fof(f497,plain,
! [X0] :
( v13_lattices(k1_lattice2(X0))
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| l3_lattices(X0)
| ~ v14_lattices(X0) ),
inference(consistent_polarity_flipping,[],[f370]) ).
fof(f687,plain,
k1_lattice2(sK0) = g3_lattices(u1_struct_0(sK0),u1_lattices(sK0),u2_lattices(sK0)),
inference(resolution,[],[f389,f374]) ).
fof(f701,plain,
! [X0] :
( l3_lattices(k1_lattice2(X0))
| k1_lattice2(X0) = g3_lattices(u1_struct_0(k1_lattice2(X0)),u2_lattices(k1_lattice2(X0)),u1_lattices(k1_lattice2(X0)))
| l3_lattices(X0) ),
inference(resolution,[],[f376,f396]) ).
fof(f710,plain,
! [X0] :
( l3_lattices(X0)
| k1_lattice2(X0) = g3_lattices(u1_struct_0(k1_lattice2(X0)),u2_lattices(k1_lattice2(X0)),u1_lattices(k1_lattice2(X0))) ),
inference(forward_subsumption_resolution,[],[f701,f397]) ).
fof(f721,plain,
! [X0,X1] :
( l3_lattices(k1_lattice2(X0))
| v3_struct_0(k1_lattice2(X0))
| m1_filter_0(X1,k1_lattice2(X0))
| m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(k1_lattice2(X0))))
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| l3_lattices(X0) ),
inference(resolution,[],[f404,f453]) ).
fof(f728,plain,
! [X0,X1] :
( v3_struct_0(k1_lattice2(X0))
| m1_filter_0(X1,k1_lattice2(X0))
| m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(k1_lattice2(X0))))
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| l3_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f721,f397]) ).
fof(f732,plain,
! [X0,X1] :
( ~ v10_lattices(X0)
| m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(k1_lattice2(X0))))
| m1_filter_0(X1,k1_lattice2(X0))
| v3_struct_0(X0)
| l3_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f728,f424]) ).
fof(f734,plain,
! [X0] :
( l3_lattices(sK0)
| v3_struct_0(sK0)
| ~ m2_lattice4(X0,sK0)
| m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0))) ),
inference(resolution,[],[f409,f213]) ).
fof(f739,plain,
! [X0] :
( v3_struct_0(sK0)
| ~ m2_lattice4(X0,sK0)
| m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0))) ),
inference(forward_subsumption_resolution,[],[f734,f374]) ).
fof(f743,plain,
! [X0] :
( ~ m2_lattice4(X0,sK0)
| m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0))) ),
inference(forward_subsumption_resolution,[],[f739,f214]) ).
fof(f774,plain,
! [X0] :
( l3_lattices(sK0)
| v3_struct_0(sK0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0)))
| k7_filter_2(sK0,X0) = X0 ),
inference(resolution,[],[f390,f213]) ).
fof(f779,plain,
! [X0] :
( v3_struct_0(sK0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0)))
| k7_filter_2(sK0,X0) = X0 ),
inference(forward_subsumption_resolution,[],[f774,f374]) ).
fof(f783,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0)))
| k7_filter_2(sK0,X0) = X0 ),
inference(forward_subsumption_resolution,[],[f779,f214]) ).
fof(f785,plain,
( l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0)
| k7_filter_2(sK0,sK1) = k15_filter_2(sK0,sK1) ),
inference(resolution,[],[f483,f210]) ).
fof(f790,plain,
( ~ v10_lattices(sK0)
| v3_struct_0(sK0)
| k7_filter_2(sK0,sK1) = k15_filter_2(sK0,sK1) ),
inference(forward_subsumption_resolution,[],[f785,f374]) ).
fof(f791,plain,
( v3_struct_0(sK0)
| k7_filter_2(sK0,sK1) = k15_filter_2(sK0,sK1) ),
inference(forward_subsumption_resolution,[],[f790,f213]) ).
fof(f792,plain,
k7_filter_2(sK0,sK1) = k15_filter_2(sK0,sK1),
inference(forward_subsumption_resolution,[],[f791,f214]) ).
fof(f794,plain,
! [X0] :
( l3_lattices(sK0)
| v3_struct_0(sK0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK0))))
| k8_filter_2(sK0,X0) = X0 ),
inference(resolution,[],[f391,f213]) ).
fof(f799,plain,
! [X0] :
( v3_struct_0(sK0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK0))))
| k8_filter_2(sK0,X0) = X0 ),
inference(forward_subsumption_resolution,[],[f794,f374]) ).
fof(f803,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK0))))
| k8_filter_2(sK0,X0) = X0 ),
inference(forward_subsumption_resolution,[],[f799,f214]) ).
fof(f859,plain,
( m1_filter_2(k7_filter_2(sK0,sK1),k1_lattice2(sK0))
| l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0)
| ~ m2_filter_2(sK1,sK0) ),
inference(superposition,[],[f395,f792]) ).
fof(f860,plain,
( m1_filter_2(k7_filter_2(sK0,sK1),k1_lattice2(sK0))
| ~ v10_lattices(sK0)
| v3_struct_0(sK0)
| ~ m2_filter_2(sK1,sK0) ),
inference(forward_subsumption_resolution,[],[f859,f374]) ).
fof(f861,plain,
( m1_filter_2(k7_filter_2(sK0,sK1),k1_lattice2(sK0))
| v3_struct_0(sK0)
| ~ m2_filter_2(sK1,sK0) ),
inference(forward_subsumption_resolution,[],[f860,f213]) ).
fof(f862,plain,
( m1_filter_2(k7_filter_2(sK0,sK1),k1_lattice2(sK0))
| ~ m2_filter_2(sK1,sK0) ),
inference(forward_subsumption_resolution,[],[f861,f214]) ).
fof(f863,plain,
m1_filter_2(k7_filter_2(sK0,sK1),k1_lattice2(sK0)),
inference(forward_subsumption_resolution,[],[f862,f210]) ).
fof(f876,plain,
( ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0))
| ~ m1_filter_0(k7_filter_2(sK0,sK1),k1_lattice2(sK0))
| l3_lattices(k1_lattice2(sK0)) ),
inference(resolution,[],[f863,f484]) ).
fof(f883,definition,
( spl28_6
<=> l3_lattices(k1_lattice2(sK0)) ),
introduced(definition,[new_symbols(definition,[spl28_6])],[avatar_definition]) ).
fof(f884,plain,
( ~ l3_lattices(k1_lattice2(sK0))
| spl28_6 ),
inference(avatar_component_clause,[],[f883]) ).
fof(f885,plain,
( l3_lattices(k1_lattice2(sK0))
| ~ spl28_6 ),
inference(avatar_component_clause,[],[f883]) ).
fof(f887,definition,
( spl28_7
<=> v3_struct_0(k1_lattice2(sK0)) ),
introduced(definition,[new_symbols(definition,[spl28_7])],[avatar_definition]) ).
fof(f888,plain,
( ~ v3_struct_0(k1_lattice2(sK0))
| spl28_7 ),
inference(avatar_component_clause,[],[f887]) ).
fof(f889,plain,
( v3_struct_0(k1_lattice2(sK0))
| ~ spl28_7 ),
inference(avatar_component_clause,[],[f887]) ).
fof(f891,definition,
( spl28_8
<=> v10_lattices(k1_lattice2(sK0)) ),
introduced(definition,[new_symbols(definition,[spl28_8])],[avatar_definition]) ).
fof(f892,plain,
( v10_lattices(k1_lattice2(sK0))
| ~ spl28_8 ),
inference(avatar_component_clause,[],[f891]) ).
fof(f893,plain,
( ~ v10_lattices(k1_lattice2(sK0))
| spl28_8 ),
inference(avatar_component_clause,[],[f891]) ).
fof(f896,definition,
( spl28_9
<=> m1_filter_0(k7_filter_2(sK0,sK1),k1_lattice2(sK0)) ),
introduced(definition,[new_symbols(definition,[spl28_9])],[avatar_definition]) ).
fof(f898,plain,
( ~ m1_filter_0(k7_filter_2(sK0,sK1),k1_lattice2(sK0))
| spl28_9 ),
inference(avatar_component_clause,[],[f896]) ).
fof(f899,plain,
( spl28_6
| ~ spl28_9
| spl28_7
| ~ spl28_8 ),
inference(avatar_split_clause,[],[f876,f891,f887,f896,f883]) ).
fof(f900,plain,
( ~ v10_lattices(sK0)
| v3_struct_0(sK0)
| l3_lattices(sK0)
| spl28_8 ),
inference(resolution,[],[f893,f453]) ).
fof(f901,plain,
( v3_struct_0(sK0)
| l3_lattices(sK0)
| spl28_8 ),
inference(forward_subsumption_resolution,[],[f900,f213]) ).
fof(f902,plain,
( l3_lattices(sK0)
| spl28_8 ),
inference(forward_subsumption_resolution,[],[f901,f214]) ).
fof(f903,plain,
( $false
| spl28_8 ),
inference(forward_subsumption_resolution,[],[f902,f374]) ).
fof(f904,plain,
spl28_8,
inference(avatar_contradiction_clause,[],[f903]) ).
fof(f911,plain,
! [X0,X1] :
( ~ v10_lattices(k1_lattice2(X0))
| v3_struct_0(k1_lattice2(X0))
| l3_lattices(k1_lattice2(X0))
| m1_filter_0(X1,k1_lattice2(X0))
| r1_tarski(X1,sK27(k1_lattice2(X0),X1))
| u1_struct_0(k1_lattice2(X0)) = X1
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| l3_lattices(X0)
| ~ v14_lattices(X0) ),
inference(resolution,[],[f489,f497]) ).
fof(f912,plain,
! [X0,X1] :
( v3_struct_0(k1_lattice2(X0))
| l3_lattices(k1_lattice2(X0))
| m1_filter_0(X1,k1_lattice2(X0))
| r1_tarski(X1,sK27(k1_lattice2(X0),X1))
| u1_struct_0(k1_lattice2(X0)) = X1
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| l3_lattices(X0)
| ~ v14_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f911,f453]) ).
fof(f914,plain,
! [X0,X1] :
( l3_lattices(k1_lattice2(X0))
| m1_filter_0(X1,k1_lattice2(X0))
| r1_tarski(X1,sK27(k1_lattice2(X0),X1))
| u1_struct_0(k1_lattice2(X0)) = X1
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| l3_lattices(X0)
| ~ v14_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f912,f424]) ).
fof(f916,plain,
! [X0,X1] :
( ~ v14_lattices(X0)
| r1_tarski(X1,sK27(k1_lattice2(X0),X1))
| u1_struct_0(k1_lattice2(X0)) = X1
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| l3_lattices(X0)
| m1_filter_0(X1,k1_lattice2(X0)) ),
inference(forward_subsumption_resolution,[],[f914,f397]) ).
fof(f918,plain,
( l3_lattices(sK0)
| ~ spl28_6 ),
inference(resolution,[],[f885,f397]) ).
fof(f919,plain,
( $false
| ~ spl28_6 ),
inference(forward_subsumption_resolution,[],[f918,f374]) ).
fof(f920,plain,
~ spl28_6,
inference(avatar_contradiction_clause,[],[f919]) ).
fof(f922,plain,
( v3_struct_0(sK0)
| l3_lattices(sK0)
| ~ spl28_7 ),
inference(resolution,[],[f889,f424]) ).
fof(f923,plain,
( l3_lattices(sK0)
| ~ spl28_7 ),
inference(forward_subsumption_resolution,[],[f922,f214]) ).
fof(f924,plain,
( $false
| ~ spl28_7 ),
inference(forward_subsumption_resolution,[],[f923,f374]) ).
fof(f925,plain,
~ spl28_7,
inference(avatar_contradiction_clause,[],[f924]) ).
fof(f927,plain,
! [X0,X1] :
( ~ v10_lattices(k1_lattice2(X0))
| v3_struct_0(k1_lattice2(X0))
| l3_lattices(k1_lattice2(X0))
| m1_filter_0(X1,k1_lattice2(X0))
| ~ m1_filter_0(sK27(k1_lattice2(X0),X1),k1_lattice2(X0))
| u1_struct_0(k1_lattice2(X0)) = X1
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| l3_lattices(X0)
| ~ v14_lattices(X0) ),
inference(resolution,[],[f491,f497]) ).
fof(f928,plain,
! [X0,X1] :
( v3_struct_0(k1_lattice2(X0))
| l3_lattices(k1_lattice2(X0))
| m1_filter_0(X1,k1_lattice2(X0))
| ~ m1_filter_0(sK27(k1_lattice2(X0),X1),k1_lattice2(X0))
| u1_struct_0(k1_lattice2(X0)) = X1
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| l3_lattices(X0)
| ~ v14_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f927,f453]) ).
fof(f930,plain,
! [X0,X1] :
( l3_lattices(k1_lattice2(X0))
| m1_filter_0(X1,k1_lattice2(X0))
| ~ m1_filter_0(sK27(k1_lattice2(X0),X1),k1_lattice2(X0))
| u1_struct_0(k1_lattice2(X0)) = X1
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| l3_lattices(X0)
| ~ v14_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f928,f424]) ).
fof(f932,plain,
! [X0,X1] :
( ~ v14_lattices(X0)
| ~ m1_filter_0(sK27(k1_lattice2(X0),X1),k1_lattice2(X0))
| u1_struct_0(k1_lattice2(X0)) = X1
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| l3_lattices(X0)
| m1_filter_0(X1,k1_lattice2(X0)) ),
inference(forward_subsumption_resolution,[],[f930,f397]) ).
fof(f937,definition,
( spl28_10
<=> m1_relset_1(u2_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0)) ),
introduced(definition,[new_symbols(definition,[spl28_10])],[avatar_definition]) ).
fof(f938,plain,
( ~ m1_relset_1(u2_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| spl28_10 ),
inference(avatar_component_clause,[],[f937]) ).
fof(f939,plain,
( m1_relset_1(u2_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ spl28_10 ),
inference(avatar_component_clause,[],[f937]) ).
fof(f941,definition,
( spl28_11
<=> v1_funct_1(u1_lattices(sK0)) ),
introduced(definition,[new_symbols(definition,[spl28_11])],[avatar_definition]) ).
fof(f942,plain,
( v1_funct_1(u1_lattices(sK0))
| ~ spl28_11 ),
inference(avatar_component_clause,[],[f941]) ).
fof(f943,plain,
( ~ v1_funct_1(u1_lattices(sK0))
| spl28_11 ),
inference(avatar_component_clause,[],[f941]) ).
fof(f945,definition,
( spl28_12
<=> v1_funct_2(u1_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0)) ),
introduced(definition,[new_symbols(definition,[spl28_12])],[avatar_definition]) ).
fof(f946,plain,
( v1_funct_2(u1_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ spl28_12 ),
inference(avatar_component_clause,[],[f945]) ).
fof(f947,plain,
( ~ v1_funct_2(u1_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| spl28_12 ),
inference(avatar_component_clause,[],[f945]) ).
fof(f949,definition,
( spl28_13
<=> m1_relset_1(u1_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0)) ),
introduced(definition,[new_symbols(definition,[spl28_13])],[avatar_definition]) ).
fof(f951,plain,
( m1_relset_1(u1_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ spl28_13 ),
inference(avatar_component_clause,[],[f949]) ).
fof(f965,plain,
( ~ l1_lattices(sK0)
| spl28_11 ),
inference(resolution,[],[f943,f255]) ).
fof(f970,plain,
( l3_lattices(sK0)
| spl28_11 ),
inference(resolution,[],[f965,f401]) ).
fof(f971,plain,
( $false
| spl28_11 ),
inference(forward_subsumption_resolution,[],[f970,f374]) ).
fof(f972,plain,
spl28_11,
inference(avatar_contradiction_clause,[],[f971]) ).
fof(f1005,plain,
! [X0] :
( m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ v10_lattices(sK0)
| v3_struct_0(sK0)
| ~ m2_filter_2(X0,sK0)
| l3_lattices(sK0) ),
inference(resolution,[],[f743,f408]) ).
fof(f1008,plain,
! [X0] :
( m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0)))
| v3_struct_0(sK0)
| ~ m2_filter_2(X0,sK0)
| l3_lattices(sK0) ),
inference(forward_subsumption_resolution,[],[f1005,f213]) ).
fof(f1012,plain,
! [X0] :
( m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ m2_filter_2(X0,sK0)
| l3_lattices(sK0) ),
inference(forward_subsumption_resolution,[],[f1008,f214]) ).
fof(f1016,plain,
! [X0] :
( ~ m2_filter_2(X0,sK0)
| m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0))) ),
inference(forward_subsumption_resolution,[],[f1012,f374]) ).
fof(f1949,plain,
k1_lattice2(sK0) = g3_lattices(u1_struct_0(k1_lattice2(sK0)),u2_lattices(k1_lattice2(sK0)),u1_lattices(k1_lattice2(sK0))),
inference(resolution,[],[f710,f374]) ).
fof(f1992,plain,
! [X0] :
( m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK0))))
| m1_filter_0(X0,k1_lattice2(sK0))
| v3_struct_0(sK0)
| l3_lattices(sK0) ),
inference(resolution,[],[f732,f213]) ).
fof(f1997,plain,
! [X0] :
( m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK0))))
| m1_filter_0(X0,k1_lattice2(sK0))
| l3_lattices(sK0) ),
inference(forward_subsumption_resolution,[],[f1992,f214]) ).
fof(f2002,plain,
! [X0] :
( m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK0))))
| m1_filter_0(X0,k1_lattice2(sK0)) ),
inference(forward_subsumption_resolution,[],[f1997,f374]) ).
fof(f2187,plain,
! [X0] :
( r1_tarski(X0,sK27(k1_lattice2(sK0),X0))
| u1_struct_0(k1_lattice2(sK0)) = X0
| ~ v10_lattices(sK0)
| v3_struct_0(sK0)
| l3_lattices(sK0)
| m1_filter_0(X0,k1_lattice2(sK0)) ),
inference(resolution,[],[f916,f215]) ).
fof(f2190,plain,
! [X0] :
( r1_tarski(X0,sK27(k1_lattice2(sK0),X0))
| u1_struct_0(k1_lattice2(sK0)) = X0
| v3_struct_0(sK0)
| l3_lattices(sK0)
| m1_filter_0(X0,k1_lattice2(sK0)) ),
inference(forward_subsumption_resolution,[],[f2187,f213]) ).
fof(f2192,plain,
! [X0] :
( r1_tarski(X0,sK27(k1_lattice2(sK0),X0))
| u1_struct_0(k1_lattice2(sK0)) = X0
| l3_lattices(sK0)
| m1_filter_0(X0,k1_lattice2(sK0)) ),
inference(forward_subsumption_resolution,[],[f2190,f214]) ).
fof(f2194,plain,
! [X0] :
( r1_tarski(X0,sK27(k1_lattice2(sK0),X0))
| u1_struct_0(k1_lattice2(sK0)) = X0
| m1_filter_0(X0,k1_lattice2(sK0)) ),
inference(forward_subsumption_resolution,[],[f2192,f374]) ).
fof(f2195,plain,
! [X0] :
( ~ m1_filter_0(sK27(k1_lattice2(sK0),X0),k1_lattice2(sK0))
| u1_struct_0(k1_lattice2(sK0)) = X0
| ~ v10_lattices(sK0)
| v3_struct_0(sK0)
| l3_lattices(sK0)
| m1_filter_0(X0,k1_lattice2(sK0)) ),
inference(resolution,[],[f932,f215]) ).
fof(f2198,plain,
! [X0] :
( ~ m1_filter_0(sK27(k1_lattice2(sK0),X0),k1_lattice2(sK0))
| u1_struct_0(k1_lattice2(sK0)) = X0
| v3_struct_0(sK0)
| l3_lattices(sK0)
| m1_filter_0(X0,k1_lattice2(sK0)) ),
inference(forward_subsumption_resolution,[],[f2195,f213]) ).
fof(f2200,plain,
! [X0] :
( ~ m1_filter_0(sK27(k1_lattice2(sK0),X0),k1_lattice2(sK0))
| u1_struct_0(k1_lattice2(sK0)) = X0
| l3_lattices(sK0)
| m1_filter_0(X0,k1_lattice2(sK0)) ),
inference(forward_subsumption_resolution,[],[f2198,f214]) ).
fof(f2202,plain,
! [X0] :
( ~ m1_filter_0(sK27(k1_lattice2(sK0),X0),k1_lattice2(sK0))
| u1_struct_0(k1_lattice2(sK0)) = X0
| m1_filter_0(X0,k1_lattice2(sK0)) ),
inference(forward_subsumption_resolution,[],[f2200,f374]) ).
fof(f2333,plain,
m1_subset_1(sK1,k1_zfmisc_1(u1_struct_0(sK0))),
inference(resolution,[],[f1016,f210]) ).
fof(f2476,plain,
( ~ l1_lattices(sK0)
| spl28_12 ),
inference(resolution,[],[f947,f254]) ).
fof(f2477,plain,
( l3_lattices(sK0)
| spl28_12 ),
inference(resolution,[],[f2476,f401]) ).
fof(f2478,plain,
( $false
| spl28_12 ),
inference(forward_subsumption_resolution,[],[f2477,f374]) ).
fof(f2479,plain,
spl28_12,
inference(avatar_contradiction_clause,[],[f2478]) ).
fof(f2489,plain,
( ! [X2,X3,X0,X1] :
( ~ v1_funct_2(X0,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_1(X0)
| m1_relset_1(u1_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| m1_relset_1(X0,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_1(u1_lattices(sK0))
| g3_lattices(X1,X2,X3) != g3_lattices(u1_struct_0(sK0),u1_lattices(sK0),X0)
| u1_struct_0(sK0) = X1 )
| ~ spl28_12 ),
inference(resolution,[],[f946,f454]) ).
fof(f2490,plain,
( ! [X2,X3,X0,X1] :
( ~ v1_funct_2(X0,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_1(X0)
| m1_relset_1(u1_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| m1_relset_1(X0,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| g3_lattices(X1,X2,X3) != g3_lattices(u1_struct_0(sK0),u1_lattices(sK0),X0)
| u1_struct_0(sK0) = X1 )
| ~ spl28_11
| ~ spl28_12 ),
inference(forward_subsumption_resolution,[],[f2489,f942]) ).
fof(f2499,definition,
( spl28_161
<=> ! [X0,X3,X2,X1] :
( ~ v1_funct_2(X0,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| u1_struct_0(sK0) = X1
| g3_lattices(X1,X2,X3) != g3_lattices(u1_struct_0(sK0),u1_lattices(sK0),X0)
| m1_relset_1(X0,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl28_161])],[avatar_definition]) ).
fof(f2500,plain,
( ! [X2,X3,X0,X1] :
( ~ v1_funct_2(X0,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| u1_struct_0(sK0) = X1
| g3_lattices(X1,X2,X3) != g3_lattices(u1_struct_0(sK0),u1_lattices(sK0),X0)
| m1_relset_1(X0,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_1(X0) )
| ~ spl28_161 ),
inference(avatar_component_clause,[],[f2499]) ).
fof(f2501,plain,
( spl28_13
| spl28_161
| ~ spl28_11
| ~ spl28_12 ),
inference(avatar_split_clause,[],[f2490,f945,f941,f2499,f949]) ).
fof(f2519,definition,
( spl28_166
<=> l2_lattices(sK0) ),
introduced(definition,[new_symbols(definition,[spl28_166])],[avatar_definition]) ).
fof(f2520,plain,
( ~ l2_lattices(sK0)
| spl28_166 ),
inference(avatar_component_clause,[],[f2519]) ).
fof(f2521,plain,
( l2_lattices(sK0)
| ~ spl28_166 ),
inference(avatar_component_clause,[],[f2519]) ).
fof(f2534,plain,
( m2_relset_1(u2_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ spl28_10 ),
inference(resolution,[],[f939,f486]) ).
fof(f2563,plain,
( l3_lattices(sK0)
| ~ spl28_166 ),
inference(resolution,[],[f2521,f402]) ).
fof(f2564,plain,
( $false
| ~ spl28_166 ),
inference(forward_subsumption_resolution,[],[f2563,f374]) ).
fof(f2565,plain,
~ spl28_166,
inference(avatar_contradiction_clause,[],[f2564]) ).
fof(f2567,plain,
! [X0] :
( m1_filter_0(X0,k1_lattice2(sK0))
| k8_filter_2(sK0,X0) = X0 ),
inference(resolution,[],[f2002,f803]) ).
fof(f2971,plain,
( sK1 = u1_struct_0(k1_lattice2(sK0))
| m1_filter_0(sK1,k1_lattice2(sK0))
| r2_filter_2(sK0,sK27(k1_lattice2(sK0),sK1))
| ~ m2_filter_2(sK27(k1_lattice2(sK0),sK1),sK0) ),
inference(resolution,[],[f2194,f375]) ).
fof(f2976,definition,
( spl28_202
<=> m2_filter_2(sK27(k1_lattice2(sK0),sK1),sK0) ),
introduced(definition,[new_symbols(definition,[spl28_202])],[avatar_definition]) ).
fof(f2977,plain,
( m2_filter_2(sK27(k1_lattice2(sK0),sK1),sK0)
| ~ spl28_202 ),
inference(avatar_component_clause,[],[f2976]) ).
fof(f2978,plain,
( ~ m2_filter_2(sK27(k1_lattice2(sK0),sK1),sK0)
| spl28_202 ),
inference(avatar_component_clause,[],[f2976]) ).
fof(f2980,definition,
( spl28_203
<=> r2_filter_2(sK0,sK27(k1_lattice2(sK0),sK1)) ),
introduced(definition,[new_symbols(definition,[spl28_203])],[avatar_definition]) ).
fof(f2982,plain,
( r2_filter_2(sK0,sK27(k1_lattice2(sK0),sK1))
| ~ spl28_203 ),
inference(avatar_component_clause,[],[f2980]) ).
fof(f2984,definition,
( spl28_204
<=> m1_filter_0(sK1,k1_lattice2(sK0)) ),
introduced(definition,[new_symbols(definition,[spl28_204])],[avatar_definition]) ).
fof(f2985,plain,
( ~ m1_filter_0(sK1,k1_lattice2(sK0))
| spl28_204 ),
inference(avatar_component_clause,[],[f2984]) ).
fof(f2988,definition,
( spl28_205
<=> sK1 = u1_struct_0(k1_lattice2(sK0)) ),
introduced(definition,[new_symbols(definition,[spl28_205])],[avatar_definition]) ).
fof(f2989,plain,
( sK1 != u1_struct_0(k1_lattice2(sK0))
| spl28_205 ),
inference(avatar_component_clause,[],[f2988]) ).
fof(f2990,plain,
( sK1 = u1_struct_0(k1_lattice2(sK0))
| ~ spl28_205 ),
inference(avatar_component_clause,[],[f2988]) ).
fof(f2991,plain,
( ~ spl28_202
| spl28_203
| spl28_204
| spl28_205 ),
inference(avatar_split_clause,[],[f2971,f2988,f2984,f2980,f2976]) ).
fof(f3033,plain,
! [X0] :
( u1_struct_0(k1_lattice2(sK0)) = X0
| m1_filter_0(X0,k1_lattice2(sK0))
| l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0)
| k14_filter_2(sK0,sK27(k1_lattice2(sK0),X0)) = k8_filter_2(sK0,sK27(k1_lattice2(sK0),X0)) ),
inference(resolution,[],[f2202,f482]) ).
fof(f3036,plain,
! [X0] :
( u1_struct_0(k1_lattice2(sK0)) = X0
| m1_filter_0(X0,k1_lattice2(sK0))
| ~ v10_lattices(sK0)
| v3_struct_0(sK0)
| k14_filter_2(sK0,sK27(k1_lattice2(sK0),X0)) = k8_filter_2(sK0,sK27(k1_lattice2(sK0),X0)) ),
inference(forward_subsumption_resolution,[],[f3033,f374]) ).
fof(f3040,plain,
! [X0] :
( u1_struct_0(k1_lattice2(sK0)) = X0
| m1_filter_0(X0,k1_lattice2(sK0))
| v3_struct_0(sK0)
| k14_filter_2(sK0,sK27(k1_lattice2(sK0),X0)) = k8_filter_2(sK0,sK27(k1_lattice2(sK0),X0)) ),
inference(forward_subsumption_resolution,[],[f3036,f213]) ).
fof(f3044,plain,
! [X0] :
( m1_filter_0(X0,k1_lattice2(sK0))
| u1_struct_0(k1_lattice2(sK0)) = X0
| k14_filter_2(sK0,sK27(k1_lattice2(sK0),X0)) = k8_filter_2(sK0,sK27(k1_lattice2(sK0),X0)) ),
inference(forward_subsumption_resolution,[],[f3040,f214]) ).
fof(f3210,plain,
sK1 = k7_filter_2(sK0,sK1),
inference(resolution,[],[f2333,f783]) ).
fof(f3250,plain,
( ~ m1_filter_0(sK1,k1_lattice2(sK0))
| spl28_9 ),
inference(superposition,[],[f898,f3210]) ).
fof(f3266,plain,
( ~ spl28_204
| spl28_9 ),
inference(avatar_split_clause,[],[f3250,f896,f2984]) ).
fof(f6802,plain,
( m2_relset_1(u1_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ spl28_13 ),
inference(resolution,[],[f951,f486]) ).
fof(f7109,plain,
! [X0] :
( sK27(k1_lattice2(sK0),X0) = k8_filter_2(sK0,sK27(k1_lattice2(sK0),X0))
| u1_struct_0(k1_lattice2(sK0)) = X0
| m1_filter_0(X0,k1_lattice2(sK0)) ),
inference(resolution,[],[f2567,f2202]) ).
fof(f7235,plain,
( l2_lattices(sK0)
| ~ spl28_10 ),
inference(resolution,[],[f2534,f414]) ).
fof(f7237,plain,
( $false
| ~ spl28_10
| spl28_166 ),
inference(forward_subsumption_resolution,[],[f7235,f2520]) ).
fof(f7238,plain,
( ~ spl28_10
| spl28_166 ),
inference(avatar_contradiction_clause,[],[f7237]) ).
fof(f7381,plain,
( ~ l1_lattices(sK0)
| ~ spl28_13 ),
inference(resolution,[],[f6802,f411]) ).
fof(f7383,plain,
( l3_lattices(sK0)
| ~ spl28_13 ),
inference(resolution,[],[f7381,f401]) ).
fof(f7384,plain,
( $false
| ~ spl28_13 ),
inference(forward_subsumption_resolution,[],[f7383,f374]) ).
fof(f7385,plain,
~ spl28_13,
inference(avatar_contradiction_clause,[],[f7384]) ).
fof(f9012,definition,
( spl28_622
<=> u1_struct_0(sK0) = u1_struct_0(k1_lattice2(sK0)) ),
introduced(definition,[new_symbols(definition,[spl28_622])],[avatar_definition]) ).
fof(f9014,plain,
( u1_struct_0(sK0) = u1_struct_0(k1_lattice2(sK0))
| ~ spl28_622 ),
inference(avatar_component_clause,[],[f9012]) ).
fof(f11563,plain,
( k7_filter_2(sK0,sK1) = u1_struct_0(k1_lattice2(sK0))
| k14_filter_2(sK0,sK27(k1_lattice2(sK0),k7_filter_2(sK0,sK1))) = k8_filter_2(sK0,sK27(k1_lattice2(sK0),k7_filter_2(sK0,sK1)))
| spl28_9 ),
inference(resolution,[],[f3044,f898]) ).
fof(f11607,definition,
( spl28_824
<=> k14_filter_2(sK0,sK27(k1_lattice2(sK0),sK1)) = k8_filter_2(sK0,sK27(k1_lattice2(sK0),sK1)) ),
introduced(definition,[new_symbols(definition,[spl28_824])],[avatar_definition]) ).
fof(f11609,plain,
( k14_filter_2(sK0,sK27(k1_lattice2(sK0),sK1)) = k8_filter_2(sK0,sK27(k1_lattice2(sK0),sK1))
| ~ spl28_824 ),
inference(avatar_component_clause,[],[f11607]) ).
fof(f11613,plain,
( sK1 = u1_struct_0(k1_lattice2(sK0))
| k14_filter_2(sK0,sK27(k1_lattice2(sK0),k7_filter_2(sK0,sK1))) = k8_filter_2(sK0,sK27(k1_lattice2(sK0),k7_filter_2(sK0,sK1)))
| spl28_9 ),
inference(forward_demodulation,[],[f11563,f3210]) ).
fof(f11620,plain,
( k14_filter_2(sK0,sK27(k1_lattice2(sK0),sK1)) = k8_filter_2(sK0,sK27(k1_lattice2(sK0),sK1))
| sK1 = u1_struct_0(k1_lattice2(sK0))
| spl28_9 ),
inference(forward_demodulation,[],[f11613,f3210]) ).
fof(f11635,plain,
( spl28_205
| spl28_824
| spl28_9 ),
inference(avatar_split_clause,[],[f11620,f896,f11607,f2988]) ).
fof(f12792,plain,
( ! [X2,X0,X1] :
( u1_struct_0(sK0) = X0
| g3_lattices(X0,X1,X2) != g3_lattices(u1_struct_0(sK0),u1_lattices(sK0),u2_lattices(sK0))
| m1_relset_1(u2_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_1(u2_lattices(sK0))
| l2_lattices(sK0) )
| ~ spl28_161 ),
inference(resolution,[],[f2500,f413]) ).
fof(f12793,plain,
( ! [X2,X0,X1] :
( u1_struct_0(sK0) = X0
| g3_lattices(X0,X1,X2) != g3_lattices(u1_struct_0(sK0),u1_lattices(sK0),u2_lattices(sK0))
| ~ v1_funct_1(u2_lattices(sK0))
| l2_lattices(sK0) )
| spl28_10
| ~ spl28_161 ),
inference(forward_subsumption_resolution,[],[f12792,f938]) ).
fof(f12794,plain,
( ! [X2,X0,X1] :
( u1_struct_0(sK0) = X0
| g3_lattices(X0,X1,X2) != g3_lattices(u1_struct_0(sK0),u1_lattices(sK0),u2_lattices(sK0))
| l2_lattices(sK0) )
| spl28_10
| ~ spl28_161 ),
inference(forward_subsumption_resolution,[],[f12793,f412]) ).
fof(f12795,plain,
( ! [X2,X0,X1] :
( u1_struct_0(sK0) = X0
| g3_lattices(X0,X1,X2) != g3_lattices(u1_struct_0(sK0),u1_lattices(sK0),u2_lattices(sK0)) )
| spl28_10
| ~ spl28_161
| spl28_166 ),
inference(forward_subsumption_resolution,[],[f12794,f2520]) ).
fof(f12796,plain,
( ! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != k1_lattice2(sK0)
| u1_struct_0(sK0) = X0 )
| spl28_10
| ~ spl28_161
| spl28_166 ),
inference(forward_demodulation,[],[f12795,f687]) ).
fof(f34632,plain,
( k1_lattice2(sK0) != k1_lattice2(sK0)
| u1_struct_0(sK0) = u1_struct_0(k1_lattice2(sK0))
| spl28_10
| ~ spl28_161
| spl28_166 ),
inference(superposition,[],[f12796,f1949]) ).
fof(f34653,plain,
( u1_struct_0(sK0) = u1_struct_0(k1_lattice2(sK0))
| spl28_10
| ~ spl28_161
| spl28_166 ),
inference(trivial_inequality_removal,[],[f34632]) ).
fof(f34745,plain,
( spl28_622
| spl28_10
| ~ spl28_161
| spl28_166 ),
inference(avatar_split_clause,[],[f34653,f2519,f2499,f937,f9012]) ).
fof(f36905,definition,
( spl28_2602
<=> v13_lattices(k1_lattice2(sK0)) ),
introduced(definition,[new_symbols(definition,[spl28_2602])],[avatar_definition]) ).
fof(f36906,plain,
( v13_lattices(k1_lattice2(sK0))
| ~ spl28_2602 ),
inference(avatar_component_clause,[],[f36905]) ).
fof(f36907,plain,
( ~ v13_lattices(k1_lattice2(sK0))
| spl28_2602 ),
inference(avatar_component_clause,[],[f36905]) ).
fof(f36937,plain,
( ~ v10_lattices(sK0)
| v3_struct_0(sK0)
| l3_lattices(sK0)
| ~ v14_lattices(sK0)
| spl28_2602 ),
inference(resolution,[],[f36907,f497]) ).
fof(f36938,plain,
( v3_struct_0(sK0)
| l3_lattices(sK0)
| ~ v14_lattices(sK0)
| spl28_2602 ),
inference(forward_subsumption_resolution,[],[f36937,f213]) ).
fof(f36939,plain,
( l3_lattices(sK0)
| ~ v14_lattices(sK0)
| spl28_2602 ),
inference(forward_subsumption_resolution,[],[f36938,f214]) ).
fof(f36940,plain,
( ~ v14_lattices(sK0)
| spl28_2602 ),
inference(forward_subsumption_resolution,[],[f36939,f374]) ).
fof(f36941,plain,
( $false
| spl28_2602 ),
inference(forward_subsumption_resolution,[],[f36940,f215]) ).
fof(f36942,plain,
spl28_2602,
inference(avatar_contradiction_clause,[],[f36941]) ).
fof(f37413,definition,
( spl28_2603
<=> m1_filter_0(sK27(k1_lattice2(sK0),sK1),k1_lattice2(sK0)) ),
introduced(definition,[new_symbols(definition,[spl28_2603])],[avatar_definition]) ).
fof(f37415,plain,
( m1_filter_0(sK27(k1_lattice2(sK0),sK1),k1_lattice2(sK0))
| ~ spl28_2603 ),
inference(avatar_component_clause,[],[f37413]) ).
fof(f37438,definition,
( spl28_2607
<=> m2_filter_2(k8_filter_2(sK0,sK27(k1_lattice2(sK0),sK1)),sK0) ),
introduced(definition,[new_symbols(definition,[spl28_2607])],[avatar_definition]) ).
fof(f37440,plain,
( m2_filter_2(k8_filter_2(sK0,sK27(k1_lattice2(sK0),sK1)),sK0)
| ~ spl28_2607 ),
inference(avatar_component_clause,[],[f37438]) ).
fof(f37989,plain,
( sK1 = u1_struct_0(k1_lattice2(sK0))
| m1_filter_0(sK1,k1_lattice2(sK0))
| ~ spl28_2603 ),
inference(resolution,[],[f37415,f2202]) ).
fof(f38172,plain,
( sK1 = u1_struct_0(k1_lattice2(sK0))
| spl28_204
| ~ spl28_2603 ),
inference(forward_subsumption_resolution,[],[f37989,f2985]) ).
fof(f38228,plain,
( spl28_205
| spl28_204
| ~ spl28_2603 ),
inference(avatar_split_clause,[],[f38172,f37413,f2984,f2988]) ).
fof(f38270,plain,
( sK1 = u1_struct_0(sK0)
| ~ spl28_205
| ~ spl28_622 ),
inference(superposition,[],[f2990,f9014]) ).
fof(f38597,plain,
( $false
| ~ spl28_205
| ~ spl28_622 ),
inference(forward_subsumption_resolution,[],[f38270,f211]) ).
fof(f38598,plain,
( ~ spl28_205
| ~ spl28_622 ),
inference(avatar_contradiction_clause,[],[f38597]) ).
fof(f38775,plain,
( m2_filter_2(k8_filter_2(sK0,sK27(k1_lattice2(sK0),sK1)),sK0)
| l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0)
| m1_filter_0(sK27(k1_lattice2(sK0),sK1),k1_lattice2(sK0))
| ~ spl28_824 ),
inference(superposition,[],[f394,f11609]) ).
fof(f38776,plain,
( m2_filter_2(k8_filter_2(sK0,sK27(k1_lattice2(sK0),sK1)),sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0)
| m1_filter_0(sK27(k1_lattice2(sK0),sK1),k1_lattice2(sK0))
| ~ spl28_824 ),
inference(forward_subsumption_resolution,[],[f38775,f374]) ).
fof(f38782,plain,
( m2_filter_2(k8_filter_2(sK0,sK27(k1_lattice2(sK0),sK1)),sK0)
| v3_struct_0(sK0)
| m1_filter_0(sK27(k1_lattice2(sK0),sK1),k1_lattice2(sK0))
| ~ spl28_824 ),
inference(forward_subsumption_resolution,[],[f38776,f213]) ).
fof(f38785,plain,
( m2_filter_2(k8_filter_2(sK0,sK27(k1_lattice2(sK0),sK1)),sK0)
| m1_filter_0(sK27(k1_lattice2(sK0),sK1),k1_lattice2(sK0))
| ~ spl28_824 ),
inference(forward_subsumption_resolution,[],[f38782,f214]) ).
fof(f38787,plain,
( spl28_2603
| spl28_2607
| ~ spl28_824 ),
inference(avatar_split_clause,[],[f38785,f11607,f37438,f37413]) ).
fof(f42116,plain,
( m1_subset_1(sK27(k1_lattice2(sK0),sK1),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ spl28_202 ),
inference(resolution,[],[f2977,f1016]) ).
fof(f42118,plain,
( l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0)
| k15_filter_2(sK0,sK27(k1_lattice2(sK0),sK1)) = k7_filter_2(sK0,sK27(k1_lattice2(sK0),sK1))
| ~ spl28_202 ),
inference(resolution,[],[f2977,f483]) ).
fof(f42120,plain,
( ~ v10_lattices(sK0)
| v3_struct_0(sK0)
| k15_filter_2(sK0,sK27(k1_lattice2(sK0),sK1)) = k7_filter_2(sK0,sK27(k1_lattice2(sK0),sK1))
| ~ spl28_202 ),
inference(forward_subsumption_resolution,[],[f42118,f374]) ).
fof(f42122,plain,
( v3_struct_0(sK0)
| k15_filter_2(sK0,sK27(k1_lattice2(sK0),sK1)) = k7_filter_2(sK0,sK27(k1_lattice2(sK0),sK1))
| ~ spl28_202 ),
inference(forward_subsumption_resolution,[],[f42120,f213]) ).
fof(f42124,plain,
( k15_filter_2(sK0,sK27(k1_lattice2(sK0),sK1)) = k7_filter_2(sK0,sK27(k1_lattice2(sK0),sK1))
| ~ spl28_202 ),
inference(forward_subsumption_resolution,[],[f42122,f214]) ).
fof(f42126,plain,
( ~ v10_lattices(sK0)
| v3_struct_0(sK0)
| ~ m2_filter_2(sK27(k1_lattice2(sK0),sK1),sK0)
| v1_filter_0(k15_filter_2(sK0,sK27(k1_lattice2(sK0),sK1)),k1_lattice2(sK0))
| l3_lattices(sK0)
| ~ spl28_203 ),
inference(resolution,[],[f2982,f494]) ).
fof(f42127,plain,
( v3_struct_0(sK0)
| ~ m2_filter_2(sK27(k1_lattice2(sK0),sK1),sK0)
| v1_filter_0(k15_filter_2(sK0,sK27(k1_lattice2(sK0),sK1)),k1_lattice2(sK0))
| l3_lattices(sK0)
| ~ spl28_203 ),
inference(forward_subsumption_resolution,[],[f42126,f213]) ).
fof(f42128,plain,
( ~ m2_filter_2(sK27(k1_lattice2(sK0),sK1),sK0)
| v1_filter_0(k15_filter_2(sK0,sK27(k1_lattice2(sK0),sK1)),k1_lattice2(sK0))
| l3_lattices(sK0)
| ~ spl28_203 ),
inference(forward_subsumption_resolution,[],[f42127,f214]) ).
fof(f42129,plain,
( v1_filter_0(k15_filter_2(sK0,sK27(k1_lattice2(sK0),sK1)),k1_lattice2(sK0))
| l3_lattices(sK0)
| ~ spl28_202
| ~ spl28_203 ),
inference(forward_subsumption_resolution,[],[f42128,f2977]) ).
fof(f42130,plain,
( v1_filter_0(k15_filter_2(sK0,sK27(k1_lattice2(sK0),sK1)),k1_lattice2(sK0))
| ~ spl28_202
| ~ spl28_203 ),
inference(forward_subsumption_resolution,[],[f42129,f374]) ).
fof(f42131,plain,
( sK27(k1_lattice2(sK0),sK1) = k7_filter_2(sK0,sK27(k1_lattice2(sK0),sK1))
| ~ spl28_202 ),
inference(resolution,[],[f42116,f783]) ).
fof(f42251,plain,
( v1_filter_0(k7_filter_2(sK0,sK27(k1_lattice2(sK0),sK1)),k1_lattice2(sK0))
| ~ spl28_202
| ~ spl28_203 ),
inference(superposition,[],[f42130,f42124]) ).
fof(f50700,plain,
( ! [X0] :
( m1_filter_0(X0,k1_lattice2(sK0))
| sK27(k1_lattice2(sK0),X0) = k8_filter_2(sK0,sK27(k1_lattice2(sK0),X0))
| u1_struct_0(sK0) = X0 )
| ~ spl28_622 ),
inference(forward_demodulation,[],[f7109,f9014]) ).
fof(f50709,plain,
( sK27(k1_lattice2(sK0),sK1) = k8_filter_2(sK0,sK27(k1_lattice2(sK0),sK1))
| sK1 = u1_struct_0(sK0)
| spl28_204
| ~ spl28_622 ),
inference(resolution,[],[f50700,f2985]) ).
fof(f50744,plain,
( sK27(k1_lattice2(sK0),sK1) = k8_filter_2(sK0,sK27(k1_lattice2(sK0),sK1))
| spl28_204
| ~ spl28_622 ),
inference(forward_subsumption_resolution,[],[f50709,f211]) ).
fof(f261803,plain,
( v1_filter_0(sK27(k1_lattice2(sK0),sK1),k1_lattice2(sK0))
| ~ spl28_202
| ~ spl28_203 ),
inference(superposition,[],[f42251,f42131]) ).
fof(f261891,plain,
( ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0))
| ~ v13_lattices(k1_lattice2(sK0))
| m1_filter_0(sK1,k1_lattice2(sK0))
| l3_lattices(k1_lattice2(sK0))
| sK1 = u1_struct_0(k1_lattice2(sK0))
| ~ spl28_202
| ~ spl28_203 ),
inference(resolution,[],[f261803,f490]) ).
fof(f261892,plain,
( v3_struct_0(k1_lattice2(sK0))
| ~ v13_lattices(k1_lattice2(sK0))
| m1_filter_0(sK1,k1_lattice2(sK0))
| l3_lattices(k1_lattice2(sK0))
| sK1 = u1_struct_0(k1_lattice2(sK0))
| ~ spl28_8
| ~ spl28_202
| ~ spl28_203 ),
inference(forward_subsumption_resolution,[],[f261891,f892]) ).
fof(f261893,plain,
( ~ v13_lattices(k1_lattice2(sK0))
| m1_filter_0(sK1,k1_lattice2(sK0))
| l3_lattices(k1_lattice2(sK0))
| sK1 = u1_struct_0(k1_lattice2(sK0))
| spl28_7
| ~ spl28_8
| ~ spl28_202
| ~ spl28_203 ),
inference(forward_subsumption_resolution,[],[f261892,f888]) ).
fof(f261894,plain,
( m1_filter_0(sK1,k1_lattice2(sK0))
| l3_lattices(k1_lattice2(sK0))
| sK1 = u1_struct_0(k1_lattice2(sK0))
| spl28_7
| ~ spl28_8
| ~ spl28_202
| ~ spl28_203
| ~ spl28_2602 ),
inference(forward_subsumption_resolution,[],[f261893,f36906]) ).
fof(f261895,plain,
( l3_lattices(k1_lattice2(sK0))
| sK1 = u1_struct_0(k1_lattice2(sK0))
| spl28_7
| ~ spl28_8
| ~ spl28_202
| ~ spl28_203
| spl28_204
| ~ spl28_2602 ),
inference(forward_subsumption_resolution,[],[f261894,f2985]) ).
fof(f261896,plain,
( sK1 = u1_struct_0(k1_lattice2(sK0))
| spl28_6
| spl28_7
| ~ spl28_8
| ~ spl28_202
| ~ spl28_203
| spl28_204
| ~ spl28_2602 ),
inference(forward_subsumption_resolution,[],[f261895,f884]) ).
fof(f261897,plain,
( $false
| spl28_6
| spl28_7
| ~ spl28_8
| ~ spl28_202
| ~ spl28_203
| spl28_204
| spl28_205
| ~ spl28_2602 ),
inference(forward_subsumption_resolution,[],[f261896,f2989]) ).
fof(f261898,plain,
( spl28_6
| spl28_7
| ~ spl28_8
| ~ spl28_202
| ~ spl28_203
| spl28_204
| spl28_205
| ~ spl28_2602 ),
inference(avatar_contradiction_clause,[],[f261897]) ).
fof(f262630,plain,
( m2_filter_2(sK27(k1_lattice2(sK0),sK1),sK0)
| spl28_204
| ~ spl28_622
| ~ spl28_2607 ),
inference(superposition,[],[f37440,f50744]) ).
fof(f262676,plain,
( $false
| spl28_202
| spl28_204
| ~ spl28_622
| ~ spl28_2607 ),
inference(forward_subsumption_resolution,[],[f262630,f2978]) ).
fof(f262677,plain,
( spl28_202
| spl28_204
| ~ spl28_622
| ~ spl28_2607 ),
inference(avatar_contradiction_clause,[],[f262676]) ).
cnf(s10,plain,
( spl28_6
| spl28_7
| ~ spl28_8
| ~ spl28_9 ),
inference(sat_conversion,[],[f899]) ).
cnf(s11,plain,
spl28_8,
inference(sat_conversion,[],[f904]) ).
cnf(s12,plain,
~ spl28_6,
inference(sat_conversion,[],[f920]) ).
cnf(s13,plain,
~ spl28_7,
inference(sat_conversion,[],[f925]) ).
cnf(s15,plain,
spl28_11,
inference(sat_conversion,[],[f972]) ).
cnf(s98,plain,
spl28_12,
inference(sat_conversion,[],[f2479]) ).
cnf(s99,plain,
( ~ spl28_11
| ~ spl28_12
| spl28_13
| spl28_161 ),
inference(sat_conversion,[],[f2501]) ).
cnf(s109,plain,
~ spl28_166,
inference(sat_conversion,[],[f2565]) ).
cnf(s131,plain,
( ~ spl28_202
| spl28_203
| spl28_204
| spl28_205 ),
inference(sat_conversion,[],[f2991]) ).
cnf(s163,plain,
( spl28_9
| ~ spl28_204 ),
inference(sat_conversion,[],[f3266]) ).
cnf(s414,plain,
( ~ spl28_10
| spl28_166 ),
inference(sat_conversion,[],[f7238]) ).
cnf(s420,plain,
~ spl28_13,
inference(sat_conversion,[],[f7385]) ).
cnf(s898,plain,
( spl28_9
| spl28_205
| spl28_824 ),
inference(sat_conversion,[],[f11635]) ).
cnf(s3502,plain,
( spl28_10
| ~ spl28_161
| spl28_166
| spl28_622 ),
inference(sat_conversion,[],[f34745]) ).
cnf(s3676,plain,
spl28_2602,
inference(sat_conversion,[],[f36942]) ).
cnf(s3831,plain,
( spl28_204
| spl28_205
| ~ spl28_2603 ),
inference(sat_conversion,[],[f38228]) ).
cnf(s3847,plain,
( ~ spl28_205
| ~ spl28_622 ),
inference(sat_conversion,[],[f38598]) ).
cnf(s3892,plain,
( ~ spl28_824
| spl28_2603
| spl28_2607 ),
inference(sat_conversion,[],[f38787]) ).
cnf(s33848,plain,
( spl28_6
| spl28_7
| ~ spl28_8
| ~ spl28_202
| ~ spl28_203
| spl28_204
| spl28_205
| ~ spl28_2602 ),
inference(sat_conversion,[],[f261898]) ).
cnf(s33923,plain,
( spl28_202
| spl28_204
| ~ spl28_622
| ~ spl28_2607 ),
inference(sat_conversion,[],[f262677]) ).
cnf(s35013,plain,
~ spl28_10,
inference(rat,[],[s414,s109]) ).
cnf(s35022,plain,
( ~ spl28_11
| ~ spl28_12
| spl28_161 ),
inference(rat,[],[s99,s420]) ).
cnf(s35274,plain,
spl28_161,
inference(rat,[],[s35022,s98,s15]) ).
cnf(s35286,plain,
spl28_622,
inference(rat,[],[s3502,s35013,s109,s35274]) ).
cnf(s35312,plain,
~ spl28_205,
inference(rat,[],[s3847,s35286]) ).
cnf(s35623,plain,
~ spl28_9,
inference(rat,[],[s10,s11,s13,s12]) ).
cnf(s35624,plain,
spl28_824,
inference(rat,[],[s898,s35312,s35623]) ).
cnf(s35625,plain,
~ spl28_204,
inference(rat,[],[s163,s35623]) ).
cnf(s35627,plain,
~ spl28_2603,
inference(rat,[],[s3831,s35312,s35625]) ).
cnf(s35629,plain,
spl28_2607,
inference(rat,[],[s3892,s35624,s35627]) ).
cnf(s35636,plain,
spl28_202,
inference(rat,[],[s33923,s35625,s35286,s35629]) ).
cnf(s35641,plain,
spl28_203,
inference(rat,[],[s131,s35312,s35625,s35636]) ).
cnf(s35642,plain,
$false,
inference(rat,[],[s33848,s3676,s35312,s35625,s11,s12,s13,s35641,s35636]) ).
fof(f262684,plain,
$false,
inference(avatar_sat_refutation,[],[s35642]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT307+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.39 % Computer : n020.cluster.edu
% 0.11/0.39 % Model : x86_64 x86_64
% 0.11/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.39 % Memory : 8046.5625MB
% 0.11/0.39 % OS : Linux 6.8.0-71-generic
% 0.11/0.39 % CPULimit : 300
% 0.11/0.39 % WCLimit : 300
% 0.11/0.39 % DateTime : Sun Sep 27 14:27:34 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.43 Running first-order model finding
% 0.11/0.43 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 16.04/2.80 % (3430963)Will run a generic schedule for satisfiability detection.
% 16.04/2.80 % (3430974)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2612110337_2999 on theBenchmark for (2999ds/0Mi)
% 16.04/2.80 % (3430975)% WARNING: option uhcvi not known.
% 16.04/2.80 % TRYING [1]
% 16.04/2.80 % TRYING [2]
% 16.04/2.80 % TRYING [3]
% 16.04/2.80 % (3430976)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=110671953:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 16.04/2.80 % (3430975)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3050408239:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 16.04/2.80 % (3430978)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2796653419:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 16.04/2.80 % (3430977)dis+10_1_sil=32000:sp=arity:random_seed=1731124106:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 16.04/2.80 % (3430979)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2671121182:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 16.04/2.80 % (3430980)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=285011076:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 16.04/2.80 % TRYING [4]
% 16.04/2.80 % TRYING [5]
% 16.04/2.80 % TRYING [6]
% 16.04/2.80 % (3430977)Instruction limit reached!
% 16.04/2.80 % (3430977)------------------------------
% 16.04/2.80 % (3430977)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.04/2.80 % (3430977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.04/2.80 % (3430977)CaDiCaL version: 2.1.3
% 16.04/2.80 % (3430977)Termination reason: Instruction limit
% 16.04/2.80 % (3430977)Termination phase: Saturation
% 16.04/2.80 % (3430977)Time elapsed: 0.065 s
% 16.04/2.80 % (3430977)Peak memory usage: 13 MB
% 16.04/2.80 % (3430977)Instructions burned: 104 (million)
% 16.04/2.80 % (3430979)Instruction limit reached!
% 16.04/2.80 % (3430979)------------------------------
% 16.04/2.80 % (3430979)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.04/2.80 % (3430979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.04/2.80 % (3430979)CaDiCaL version: 2.1.3
% 16.04/2.80 % (3430979)Termination reason: Instruction limit
% 16.04/2.80 % (3430979)Termination phase: Saturation
% 16.04/2.80 % (3430979)Time elapsed: 0.071 s
% 16.04/2.80 % (3430979)Peak memory usage: 14 MB
% 16.04/2.80 % (3430979)Instructions burned: 132 (million)
% 16.04/2.80 % (3430978)Instruction limit reached!
% 16.04/2.80 % (3430978)------------------------------
% 16.04/2.80 % (3430978)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.04/2.80 % (3430978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.04/2.80 % (3430978)CaDiCaL version: 2.1.3
% 16.04/2.80 % (3430978)Termination reason: Instruction limit
% 16.04/2.80 % (3430978)Termination phase: Saturation
% 16.04/2.80 % (3430978)Time elapsed: 0.074 s
% 16.04/2.80 % (3430978)Peak memory usage: 13 MB
% 16.04/2.80 % (3430978)Instructions burned: 116 (million)
% 16.04/2.80 % (3431008)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1954141155:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 16.04/2.80 % (3431010)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2935781223:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 16.04/2.80 % (3431012)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=882081862:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 16.04/2.80 % TRYING [1]
% 16.04/2.80 % TRYING [2]
% 16.04/2.80 % (3430980)Instruction limit reached!
% 16.04/2.80 % (3430980)------------------------------
% 16.04/2.80 % (3430980)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.04/2.80 % (3430980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.04/2.80 % (3430980)CaDiCaL version: 2.1.3
% 16.04/2.80 % (3430980)Termination reason: Instruction limit
% 16.04/2.80 % (3430980)Termination phase: Saturation
% 16.04/2.80 % (3430980)Time elapsed: 0.096 s
% 16.04/2.80 % (3430980)Peak memory usage: 14 MB
% 16.04/2.80 % (3430980)Instructions burned: 159 (million)
% 16.04/2.80 % TRYING [3]
% 16.04/2.80 % TRYING [4]
% 16.04/2.80 % (3431022)ott-21_1_sil=16000:fs=off:random_seed=4268956376:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 16.04/2.80 % TRYING [7]
% 16.04/2.80 % (3431010)Instruction limit reached!
% 16.04/2.80 % (3431010)------------------------------
% 16.04/2.80 % (3431010)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.55/7.77 % (3431010)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.55/7.77 % (3431010)CaDiCaL version: 2.1.3
% 51.55/7.77 % (3431010)Termination reason: Instruction limit
% 51.55/7.77 % (3431010)Termination phase: Saturation
% 51.55/7.77 % (3431010)Time elapsed: 0.082 s
% 51.55/7.77 % (3431010)Peak memory usage: 14 MB
% 51.55/7.77 % (3431010)Instructions burned: 131 (million)
% 51.55/7.77 % (3431053)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2361664733:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 51.55/7.77 % TRYING [5]
% 51.55/7.77 % (3431022)Instruction limit reached!
% 51.55/7.77 % (3431022)------------------------------
% 51.55/7.77 % (3431022)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.55/7.77 % (3431022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.55/7.77 % (3431022)CaDiCaL version: 2.1.3
% 51.55/7.77 % (3431022)Termination reason: Instruction limit
% 51.55/7.77 % (3431022)Termination phase: Saturation
% 51.55/7.77 % (3431022)Time elapsed: 0.098 s
% 51.55/7.77 % (3431022)Peak memory usage: 13 MB
% 51.55/7.77 % (3431022)Instructions burned: 180 (million)
% 51.55/7.77 % (3431071)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=989405621:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 51.55/7.77 % TRYING [1]
% 51.55/7.77 % TRYING [2]
% 51.55/7.77 % TRYING [3]
% 51.55/7.77 % TRYING [4]
% 51.55/7.77 % (3431008)Instruction limit reached!
% 51.55/7.77 % (3431008)------------------------------
% 51.55/7.77 % (3431008)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.55/7.77 % (3431008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.55/7.77 % (3431008)CaDiCaL version: 2.1.3
% 51.55/7.77 % (3431008)Termination reason: Instruction limit
% 51.55/7.77 % (3431008)Termination phase: Finite model building constraint generation
% 51.55/7.77 % (3431008)Time elapsed: 0.250 s
% 51.55/7.77 % (3431008)Peak memory usage: 30 MB
% 51.55/7.77 % (3431008)Instructions burned: 715 (million)
% 51.55/7.77 % (3431120)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2915833486:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 51.55/7.77 % TRYING [5]
% 51.55/7.77 % TRYING [8]
% 51.55/7.77 % (3431012)Instruction limit reached!
% 51.55/7.77 % (3431012)------------------------------
% 51.55/7.77 % (3431012)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.55/7.77 % (3431012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.55/7.77 % (3431012)CaDiCaL version: 2.1.3
% 51.55/7.77 % (3431012)Termination reason: Instruction limit
% 51.55/7.77 % (3431012)Termination phase: Saturation
% 51.55/7.77 % (3431012)Time elapsed: 0.419 s
% 51.55/7.77 % (3431012)Peak memory usage: 21 MB
% 51.55/7.77 % (3431012)Instructions burned: 684 (million)
% 51.55/7.77 % (3431053)Instruction limit reached!
% 51.55/7.77 % (3431053)------------------------------
% 51.55/7.77 % (3431053)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.55/7.77 % (3431053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.55/7.77 % (3431053)CaDiCaL version: 2.1.3
% 51.55/7.77 % (3431053)Termination reason: Instruction limit
% 51.55/7.77 % (3431053)Termination phase: Saturation
% 51.55/7.77 % (3431053)Time elapsed: 0.321 s
% 51.55/7.77 % (3431053)Peak memory usage: 15 MB
% 51.55/7.77 % (3431053)Instructions burned: 478 (million)
% 51.55/7.77 % (3431197)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=694633585:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 51.55/7.77 % (3431199)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=2814511449:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 51.55/7.77 % (3431071)Instruction limit reached!
% 51.55/7.77 % (3431071)------------------------------
% 51.55/7.77 % (3431071)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.55/7.77 % (3431071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.55/7.77 % (3431071)CaDiCaL version: 2.1.3
% 51.55/7.77 % (3431071)Termination reason: Instruction limit
% 51.55/7.77 % (3431071)Termination phase: Finite model building SAT solving
% 51.55/7.77 % (3431071)Time elapsed: 0.323 s
% 51.55/7.77 % (3431071)Peak memory usage: 20 MB
% 51.55/7.77 % (3431071)Instructions burned: 866 (million)
% 51.55/7.77 % (3431222)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=729814206:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 51.55/7.77 % TRYING [14]
% 51.55/7.77 % (3431197)Instruction limit reached!
% 80.20/13.67 % (3431197)------------------------------
% 80.20/13.67 % (3431197)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 80.20/13.67 % (3431197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.20/13.67 % (3431197)CaDiCaL version: 2.1.3
% 80.20/13.67 % (3431197)Termination reason: Instruction limit
% 80.20/13.67 % (3431197)Termination phase: Finite model building constraint generation
% 80.20/13.67 % (3431197)Time elapsed: 0.313 s
% 80.20/13.67 % (3431197)Peak memory usage: 66 MB
% 80.20/13.67 % (3431197)Instructions burned: 889 (million)
% 80.20/13.67 % (3431348)fmb+10_1_sil=64000:random_seed=2067336569:i=22061:nm=2:gsp=on_2991 on theBenchmark for (2991ds/22061Mi)
% 80.20/13.67 % TRYING [1]
% 80.20/13.67 % TRYING [2]
% 80.20/13.67 % TRYING [3]
% 80.20/13.67 % TRYING [4]
% 80.20/13.67 % (3431199)Instruction limit reached!
% 80.20/13.67 % (3431199)------------------------------
% 80.20/13.67 % (3431199)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 80.20/13.67 % (3431199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.20/13.67 % (3431199)CaDiCaL version: 2.1.3
% 80.20/13.67 % (3431199)Termination reason: Instruction limit
% 80.20/13.67 % (3431199)Termination phase: Saturation
% 80.20/13.67 % (3431199)Time elapsed: 0.410 s
% 80.20/13.67 % (3431199)Peak memory usage: 21 MB
% 80.20/13.67 % (3431199)Instructions burned: 693 (million)
% 80.20/13.67 % (3431390)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2125638513:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 80.20/13.67 % TRYING [20]
% 80.20/13.67 % (3431120)Instruction limit reached!
% 80.20/13.67 % (3431120)------------------------------
% 80.20/13.67 % (3431120)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 80.20/13.67 % (3431120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.20/13.67 % (3431120)CaDiCaL version: 2.1.3
% 80.20/13.67 % (3431120)Termination reason: Instruction limit
% 80.20/13.67 % (3431120)Termination phase: Saturation
% 80.20/13.67 % (3431120)Time elapsed: 0.671 s
% 80.20/13.67 % (3431120)Peak memory usage: 28 MB
% 80.20/13.67 % (3431120)Instructions burned: 1181 (million)
% 80.20/13.67 % (3431427)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2812067844:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 80.20/13.67 % TRYING [8]
% 80.20/13.67 % (3431222)Instruction limit reached!
% 80.20/13.67 % (3431222)------------------------------
% 80.20/13.67 % (3431222)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 80.20/13.67 % (3431222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.20/13.67 % (3431222)CaDiCaL version: 2.1.3
% 80.20/13.67 % (3431222)Termination reason: Instruction limit
% 80.20/13.67 % (3431222)Termination phase: Saturation
% 80.20/13.67 % (3431222)Time elapsed: 0.488 s
% 80.20/13.67 % (3431222)Peak memory usage: 20 MB
% 80.20/13.67 % (3431222)Instructions burned: 880 (million)
% 80.20/13.67 % (3431444)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1288358225:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 80.20/13.67 % TRYING [5]
% 80.20/13.67 % (3431427)Instruction limit reached!
% 80.20/13.67 % (3431427)------------------------------
% 80.20/13.67 % (3431427)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 80.20/13.67 % (3431427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.20/13.67 % (3431427)CaDiCaL version: 2.1.3
% 80.20/13.67 % (3431427)Termination reason: Instruction limit
% 80.20/13.67 % (3431427)Termination phase: Finite model building SAT solving
% 80.20/13.67 % (3431427)Time elapsed: 0.369 s
% 80.20/13.67 % (3431427)Peak memory usage: 57 MB
% 80.20/13.67 % (3431427)Instructions burned: 921 (million)
% 80.20/13.67 % (3431602)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2624778123:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi)
% 80.20/13.67 % (3431602)Instruction limit reached!
% 80.20/13.67 % (3431602)------------------------------
% 80.20/13.67 % (3431602)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 80.20/13.67 % (3431602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.20/13.67 % (3431602)CaDiCaL version: 2.1.3
% 80.20/13.67 % (3431602)Termination reason: Instruction limit
% 80.20/13.67 % (3431602)Termination phase: Saturation
% 80.20/13.67 % (3431602)Time elapsed: 0.841 s
% 80.20/13.67 % (3431602)Peak memory usage: 29 MB
% 80.20/13.67 % (3431602)Instructions burned: 1473 (million)
% 80.20/13.67 % (3431986)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3055857755:i=6324_2976 on theBenchmark for (2976ds/6324Mi)
% 80.20/13.67 % TRYING [77]
% 80.20/13.67 % TRYING [6]
% 80.20/13.67 % (3431444)Instruction limit reached!
% 80.20/13.67 % (3431444)------------------------------
% 80.20/13.67 % (3431444)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 80.20/13.67 % (3431444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.20/13.67 % (3431444)CaDiCaL version: 2.1.3
% 80.20/13.67 % (3431444)Termination reason: Instruction limit
% 80.20/13.67 % (3431444)Termination phase: Saturation
% 80.20/13.67 % (3431444)Time elapsed: 2.730 s
% 80.20/13.67 % (3431444)Peak memory usage: 36 MB
% 80.20/13.67 % (3431444)Instructions burned: 5132 (million)
% 80.20/13.67 % (3432657)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=187430195:fmbsr=2.30978:i=2174_2961 on theBenchmark for (2961ds/2174Mi)
% 80.20/13.67 % TRYING [16]
% 80.20/13.67 % (3431390)Instruction limit reached!
% 80.20/13.67 % (3431390)------------------------------
% 80.20/13.67 % (3431390)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 80.20/13.67 % (3431390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.20/13.67 % (3431390)CaDiCaL version: 2.1.3
% 80.20/13.67 % (3431390)Termination reason: Instruction limit
% 80.20/13.67 % (3431390)Termination phase: Finite model building constraint generation
% 80.20/13.67 % (3431390)Time elapsed: 3.336 s
% 80.20/13.67 % (3431390)Peak memory usage: 537 MB
% 80.20/13.67 % (3431390)Instructions burned: 9515 (million)
% 80.20/13.67 % TRYING [9]
% 80.20/13.67 % (3432894)ott-2_1_sil=16000:newcnf=on:random_seed=2584420638:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2955 on theBenchmark for (2955ds/869Mi)
% 80.20/13.67 % (3431986)Instruction limit reached!
% 80.20/13.67 % (3431986)------------------------------
% 80.20/13.67 % (3431986)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 80.20/13.67 % (3431986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.20/13.67 % (3431986)CaDiCaL version: 2.1.3
% 80.20/13.67 % (3431986)Termination reason: Instruction limit
% 80.20/13.67 % (3431986)Termination phase: Finite model building constraint generation
% 80.20/13.67 % (3431986)Time elapsed: 2.148 s
% 80.20/13.67 % (3431986)Peak memory usage: 352 MB
% 80.20/13.67 % (3431986)Instructions burned: 6326 (million)
% 80.20/13.67 % (3432954)ott+10_1_sil=32000:tgt=ground:random_seed=1048415988:i=5114:av=off_2954 on theBenchmark for (2954ds/5114Mi)
% 80.20/13.67 % (3432657)Instruction limit reached!
% 80.20/13.67 % (3432657)------------------------------
% 80.20/13.67 % (3432657)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 80.20/13.67 % (3432657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.20/13.67 % (3432657)CaDiCaL version: 2.1.3
% 80.20/13.67 % (3432657)Termination reason: Instruction limit
% 80.20/13.67 % (3432657)Termination phase: Finite model building constraint generation
% 80.20/13.67 % (3432657)Time elapsed: 0.744 s
% 80.20/13.67 % (3432657)Peak memory usage: 132 MB
% 80.20/13.67 % (3432657)Instructions burned: 2176 (million)
% 80.20/13.67 % (3433001)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1073653404:i=54282_2953 on theBenchmark for (2953ds/54282Mi)
% 80.20/13.67 % TRYING [1]
% 80.20/13.67 % TRYING [2]
% 80.20/13.67 % TRYING [3]
% 80.20/13.67 % TRYING [4]
% 80.20/13.67 % TRYING [5]
% 80.20/13.67 % TRYING [6]
% 80.20/13.67 % (3432894)Instruction limit reached!
% 80.20/13.67 % (3432894)------------------------------
% 80.20/13.67 % (3432894)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 80.20/13.67 % (3432894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.20/13.67 % (3432894)CaDiCaL version: 2.1.3
% 80.20/13.67 % (3432894)Termination reason: Instruction limit
% 80.20/13.67 % (3432894)Termination phase: Saturation
% 80.20/13.67 % (3432894)Time elapsed: 0.401 s
% 80.20/13.67 % (3432894)Peak memory usage: 15 MB
% 80.20/13.67 % (3432894)Instructions burned: 869 (million)
% 80.20/13.67 % (3433088)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2236869467:i=3512:aac=none_2951 on theBenchmark for (2951ds/3512Mi)
% 80.20/13.67 % TRYING [7]
% 80.20/13.67 % TRYING [8]
% 80.20/13.67 % (3433088)Instruction limit reached!
% 80.20/13.67 % (3433088)------------------------------
% 80.20/13.67 % (3433088)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 80.20/13.67 % (3433088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.20/13.67 % (3433088)CaDiCaL version: 2.1.3
% 80.20/13.67 % (3433088)Termination reason: Instruction limit
% 80.20/13.67 % (3433088)Termination phase: Saturation
% 80.20/13.67 % (3433088)Time elapsed: 2.416 s
% 80.20/13.67 % (3433088)Peak memory usage: 34 MB
% 80.20/13.67 % (3433088)Instructions burned: 3512 (million)
% 80.20/13.67 % (3433305)dis+21_1_sil=32000:sas=cadical:random_seed=1209559463:i=3773:amm=off_2927 on theBenchmark for (2927ds/3773Mi)
% 80.20/13.67 % (3432954)Instruction limit reached!
% 80.20/13.67 % (3432954)------------------------------
% 80.20/13.67 % (3432954)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 80.20/13.67 % (3432954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.20/13.67 % (3432954)CaDiCaL version: 2.1.3
% 80.20/13.67 % (3432954)Termination reason: Instruction limit
% 80.20/13.67 % (3432954)Termination phase: Saturation
% 80.20/13.67 % (3432954)Time elapsed: 3.862 s
% 80.20/13.67 % (3432954)Peak memory usage: 38 MB
% 80.20/13.67 % (3432954)Instructions burned: 5114 (million)
% 80.20/13.67 % (3433307)ott+11_1_sil=16000:gs=on:random_seed=2129006976:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2915 on theBenchmark for (2915ds/2251Mi)
% 80.20/13.67 % (3431348)Instruction limit reached!
% 80.20/13.67 % (3431348)------------------------------
% 80.20/13.67 % (3431348)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 80.20/13.67 % (3431348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.20/13.67 % (3431348)CaDiCaL version: 2.1.3
% 80.20/13.67 % (3431348)Termination reason: Instruction limit
% 80.20/13.67 % (3431348)Termination phase: Finite model building SAT solving
% 80.20/13.67 % (3431348)Time elapsed: 9.485 s
% 80.20/13.67 % (3431348)Peak memory usage: 100 MB
% 80.20/13.67 % (3431348)Instructions burned: 22062 (million)
% 80.20/13.67 % (3433309)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3457748715:fmbsr=1.6:i=67534_2895 on theBenchmark for (2895ds/67534Mi)
% 80.20/13.67 % TRYING [7]
% 80.20/13.67 % (3433307)Instruction limit reached!
% 80.20/13.67 % (3433307)------------------------------
% 80.20/13.67 % (3433307)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 80.20/13.67 % (3433307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.20/13.67 % (3433307)CaDiCaL version: 2.1.3
% 80.20/13.67 % (3433307)Termination reason: Instruction limit
% 80.20/13.67 % (3433307)Termination phase: Saturation
% 80.20/13.67 % (3433307)Time elapsed: 2.404 s
% 80.20/13.67 % (3433307)Peak memory usage: 38 MB
% 80.20/13.67 % (3433307)Instructions burned: 2252 (million)
% 80.20/13.67 % (3433305)Instruction limit reached!
% 80.20/13.67 % (3433305)------------------------------
% 80.20/13.67 % (3433305)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 80.20/13.67 % (3433305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.20/13.67 % (3433305)CaDiCaL version: 2.1.3
% 80.20/13.67 % (3433305)Termination reason: Instruction limit
% 80.20/13.67 % (3433305)Termination phase: Saturation
% 80.20/13.67 % (3433305)Time elapsed: 3.606 s
% 80.20/13.67 % (3433305)Peak memory usage: 41 MB
% 80.20/13.67 % (3433305)Instructions burned: 3773 (million)
% 80.20/13.67 % (3433311)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3839268634:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2891 on theBenchmark for (2891ds/4591Mi)
% 80.20/13.67 % (3433313)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=736335183:i=29340_2890 on theBenchmark for (2890ds/29340Mi)
% 80.20/13.67 % TRYING [8]
% 80.20/13.67 % (3430975) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3430963-3430975"...
% 80.20/13.67 % (3430975)...printing done.
% 80.20/13.67 % (3430975)Refutation found. Thanks to Tanya!
% 80.20/13.67 % SZS status Theorem for theBenchmark
% 80.20/13.67 % SZS output start Proof for theBenchmark
% See solution above
% 80.20/13.68 % (3430975)------------------------------
% 80.20/13.68 % (3430975)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 80.20/13.68 % (3430975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.20/13.68 % (3430975)CaDiCaL version: 2.1.3
% 80.20/13.68 % (3430975)Termination reason: Refutation
% 80.20/13.68 % (3430975)Time elapsed: 13.123 s
% 80.20/13.68 % (3430975)Peak memory usage: 113 MB
% 80.20/13.68 % (3430975)Instructions burned: 18089 (million)
% 80.20/13.68 % (3430963)Success in time 13.235 s
% 80.20/13.68 % Vampire exiting
%------------------------------------------------------------------------------