%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LAT309+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 : n007.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:48:20 AM UTC 2026
% Result : Theorem 50.84s 7.97s
% Output : Refutation 50.84s
% Verified :
% SZS Type : Refutation
% Derivation depth : 36
% Number of leaves : 44
% Syntax : Number of formulae : 480 ( 44 unt; 19 def)
% Number of atoms : 2048 ( 363 equ)
% Maximal formula atoms : 12 ( 4 avg)
% Number of connectives : 2297 ( 729 ~;1378 |; 124 &)
% ( 26 <=>; 40 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 6 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 47 ( 45 usr; 20 prp; 0-3 aty)
% Number of functors : 17 ( 17 usr; 2 con; 0-3 aty)
% Number of variables : 542 ( 0 sgn 536 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ~ ( v14_lattices(X0)
& X1 != k6_lattices(X0)
& ! [X2] :
( m2_filter_2(X2,X0)
=> ~ ( r2_hidden(X1,X2)
& r2_filter_2(X0,X2) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t36_filter_2) ).
fof(f2,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ~ ( v14_lattices(X0)
& X1 != k6_lattices(X0)
& ! [X2] :
( m2_filter_2(X2,X0)
=> ~ ( r2_hidden(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,u1_struct_0(X0))
=> k5_filter_2(X0,X1) = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d4_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(X0)))
=> k7_filter_2(X0,X1) = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d6_filter_2) ).
fof(f15,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(f17,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(f19,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(f23,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& m1_subset_1(X1,u1_struct_0(X0)) )
=> m1_subset_1(k5_filter_2(X0,X1),u1_struct_0(k1_lattice2(X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k5_filter_2) ).
fof(f31,axiom,
! [X0] :
( l3_lattices(X0)
=> ( l1_lattices(X0)
& l2_lattices(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l3_lattices) ).
fof(f32,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(f36,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(f37,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(f39,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(f41,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(f54,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(f65,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(f66,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(f81,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(f82,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(f84,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(f87,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ~ ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v13_lattices(X0)
& l3_lattices(X0)
& X1 != k5_lattices(X0)
& ! [X2] :
( m1_filter_0(X2,X0)
=> ~ ( r2_hidden(X1,X2)
& v1_filter_0(X2,X0) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t24_filter_0) ).
fof(f89,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(f93,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(f95,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v14_lattices(X0)
& l3_lattices(X0) )
=> k6_lattices(X0) = k5_lattices(k1_lattice2(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t79_lattice2) ).
fof(f110,plain,
? [X0] :
( ? [X1] :
( v14_lattices(X0)
& X1 != k6_lattices(X0)
& ! [X2] :
( ~ r2_hidden(X1,X2)
| ~ r2_filter_2(X0,X2)
| ~ m2_filter_2(X2,X0) )
& m1_subset_1(X1,u1_struct_0(X0)) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(ennf_transformation,[],[f2]) ).
fof(f111,plain,
? [X0] :
( ? [X1] :
( v14_lattices(X0)
& X1 != k6_lattices(X0)
& ! [X2] :
( ~ r2_hidden(X1,X2)
| ~ r2_filter_2(X0,X2)
| ~ m2_filter_2(X2,X0) )
& m1_subset_1(X1,u1_struct_0(X0)) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(flattening,[],[f110]) ).
fof(f112,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(f113,plain,
! [X0] :
( X0 = g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))
| ~ v3_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f112]) ).
fof(f127,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(f128,plain,
! [X0] :
( ! [X1] :
( k5_filter_2(X0,X1) = X1
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f13]) ).
fof(f129,plain,
! [X0] :
( ! [X1] :
( k5_filter_2(X0,X1) = X1
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f128]) ).
fof(f130,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,[],[f14]) ).
fof(f131,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,[],[f130]) ).
fof(f132,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,[],[f15]) ).
fof(f133,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,[],[f132]) ).
fof(f136,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,[],[f17]) ).
fof(f137,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,[],[f136]) ).
fof(f140,plain,
! [X0] :
( ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f19]) ).
fof(f141,plain,
! [X0,X1] :
( m1_subset_1(k5_filter_2(X0,X1),u1_struct_0(k1_lattice2(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f23]) ).
fof(f142,plain,
! [X0,X1] :
( m1_subset_1(k5_filter_2(X0,X1),u1_struct_0(k1_lattice2(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(flattening,[],[f141]) ).
fof(f153,plain,
! [X0] :
( ( l1_lattices(X0)
& l2_lattices(X0) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f31]) ).
fof(f154,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,[],[f32]) ).
fof(f155,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,[],[f154]) ).
fof(f158,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,[],[f36]) ).
fof(f159,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,[],[f158]) ).
fof(f160,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,[],[f37]) ).
fof(f161,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,[],[f160]) ).
fof(f163,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,[],[f39]) ).
fof(f164,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,[],[f41]) ).
fof(f175,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f54]) ).
fof(f176,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f175]) ).
fof(f193,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,[],[f65]) ).
fof(f194,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,[],[f193]) ).
fof(f195,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,[],[f66]) ).
fof(f196,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,[],[f195]) ).
fof(f202,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,[],[f81]) ).
fof(f203,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,[],[f202]) ).
fof(f204,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,[],[f82]) ).
fof(f205,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,[],[f204]) ).
fof(f209,plain,
! [X0] :
( ! [X1] :
( v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v13_lattices(X0)
| ~ l3_lattices(X0)
| k5_lattices(X0) = X1
| ? [X2] :
( r2_hidden(X1,X2)
& v1_filter_0(X2,X0)
& m1_filter_0(X2,X0) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f87]) ).
fof(f210,plain,
! [X0] :
( ! [X1] :
( v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v13_lattices(X0)
| ~ l3_lattices(X0)
| k5_lattices(X0) = X1
| ? [X2] :
( r2_hidden(X1,X2)
& v1_filter_0(X2,X0)
& m1_filter_0(X2,X0) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f209]) ).
fof(f213,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,[],[f89]) ).
fof(f214,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,[],[f213]) ).
fof(f219,plain,
! [X0] :
( ( v14_lattices(X0)
<=> v13_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f93]) ).
fof(f220,plain,
! [X0] :
( ( v14_lattices(X0)
<=> v13_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f219]) ).
fof(f222,plain,
! [X0] :
( k6_lattices(X0) = k5_lattices(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v14_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f95]) ).
fof(f223,plain,
! [X0] :
( k6_lattices(X0) = k5_lattices(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v14_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f222]) ).
fof(f226,plain,
! [X2] :
( ~ m2_filter_2(X2,sK0)
| ~ r2_filter_2(sK0,X2)
| ~ r2_hidden(sK1,X2) ),
inference(cnf_transformation,[],[f111]) ).
fof(f227,plain,
m1_subset_1(sK1,u1_struct_0(sK0)),
inference(cnf_transformation,[],[f111]) ).
fof(f228,plain,
sK1 != k6_lattices(sK0),
inference(cnf_transformation,[],[f111]) ).
fof(f229,plain,
v14_lattices(sK0),
inference(cnf_transformation,[],[f111]) ).
fof(f230,plain,
l3_lattices(sK0),
inference(cnf_transformation,[],[f111]) ).
fof(f231,plain,
v10_lattices(sK0),
inference(cnf_transformation,[],[f111]) ).
fof(f232,plain,
~ v3_struct_0(sK0),
inference(cnf_transformation,[],[f111]) ).
fof(f233,plain,
! [X0] :
( ~ l3_lattices(X0)
| ~ v3_lattices(X0)
| g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) = X0 ),
inference(cnf_transformation,[],[f113]) ).
fof(f247,plain,
! [X0] :
( ~ l3_lattices(X0)
| k1_lattice2(X0) = g3_lattices(u1_struct_0(X0),u1_lattices(X0),u2_lattices(X0)) ),
inference(cnf_transformation,[],[f127]) ).
fof(f248,plain,
! [X0,X1] :
( ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| k5_filter_2(X0,X1) = X1 ),
inference(cnf_transformation,[],[f129]) ).
fof(f249,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,[],[f131]) ).
fof(f250,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,[],[f133]) ).
fof(f253,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,[],[f137]) ).
fof(f255,plain,
! [X0] :
( ~ l3_lattices(X0)
| l3_lattices(k1_lattice2(X0)) ),
inference(cnf_transformation,[],[f140]) ).
fof(f256,plain,
! [X0] :
( ~ l3_lattices(X0)
| v3_lattices(k1_lattice2(X0)) ),
inference(cnf_transformation,[],[f140]) ).
fof(f257,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| m1_subset_1(k5_filter_2(X0,X1),u1_struct_0(k1_lattice2(X0))) ),
inference(cnf_transformation,[],[f142]) ).
fof(f264,plain,
! [X0] :
( ~ l3_lattices(X0)
| l2_lattices(X0) ),
inference(cnf_transformation,[],[f153]) ).
fof(f265,plain,
! [X0] :
( ~ l3_lattices(X0)
| l1_lattices(X0) ),
inference(cnf_transformation,[],[f153]) ).
fof(f266,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,[],[f155]) ).
fof(f270,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,[],[f159]) ).
fof(f272,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,[],[f161]) ).
fof(f274,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,[],[f163]) ).
fof(f275,plain,
! [X0] :
( ~ l1_lattices(X0)
| v1_funct_2(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f163]) ).
fof(f276,plain,
! [X0] :
( ~ l1_lattices(X0)
| v1_funct_1(u1_lattices(X0)) ),
inference(cnf_transformation,[],[f163]) ).
fof(f277,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,[],[f164]) ).
fof(f278,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,[],[f164]) ).
fof(f279,plain,
! [X0] :
( ~ l2_lattices(X0)
| v1_funct_1(u2_lattices(X0)) ),
inference(cnf_transformation,[],[f164]) ).
fof(f293,plain,
! [X0] :
( ~ l3_lattices(X0)
| v3_struct_0(X0)
| ~ v3_struct_0(k1_lattice2(X0)) ),
inference(cnf_transformation,[],[f176]) ).
fof(f313,plain,
! [X0] :
( ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| v10_lattices(k1_lattice2(X0)) ),
inference(cnf_transformation,[],[f194]) ).
fof(f322,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)
| X2 = X5 ),
inference(cnf_transformation,[],[f196]) ).
fof(f323,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)
| X1 = X4 ),
inference(cnf_transformation,[],[f196]) ).
fof(f324,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,[],[f196]) ).
fof(f372,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,[],[f203]) ).
fof(f373,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,[],[f205]) ).
fof(f377,plain,
! [X2,X0,X1] :
( m1_relset_1(X2,X0,X1)
| ~ m2_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f84]) ).
fof(f380,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u1_struct_0(X0))
| m1_filter_0(sK27(X0,X1),X0)
| k5_lattices(X0) = X1
| ~ l3_lattices(X0)
| ~ v13_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[],[f210]) ).
fof(f381,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u1_struct_0(X0))
| v1_filter_0(sK27(X0,X1),X0)
| k5_lattices(X0) = X1
| ~ l3_lattices(X0)
| ~ v13_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[],[f210]) ).
fof(f382,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u1_struct_0(X0))
| r2_hidden(X1,sK27(X0,X1))
| k5_lattices(X0) = X1
| ~ l3_lattices(X0)
| ~ v13_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[],[f210]) ).
fof(f384,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,[],[f214]) ).
fof(f390,plain,
! [X0] :
( ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| v13_lattices(k1_lattice2(X0))
| ~ v14_lattices(X0) ),
inference(cnf_transformation,[],[f220]) ).
fof(f392,plain,
! [X0] :
( ~ l3_lattices(X0)
| ~ v14_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| k6_lattices(X0) = k5_lattices(k1_lattice2(X0)) ),
inference(cnf_transformation,[],[f223]) ).
fof(f395,plain,
~ l3_lattices(sK0),
inference(consistent_polarity_flipping,[],[f230]) ).
fof(f396,plain,
~ v14_lattices(sK0),
inference(consistent_polarity_flipping,[],[f229]) ).
fof(f397,plain,
! [X2] :
( ~ r2_filter_2(sK0,X2)
| m2_filter_2(X2,sK0)
| ~ r2_hidden(sK1,X2) ),
inference(consistent_polarity_flipping,[],[f226]) ).
fof(f398,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,[],[f233]) ).
fof(f410,plain,
! [X0] :
( l3_lattices(X0)
| k1_lattice2(X0) = g3_lattices(u1_struct_0(X0),u1_lattices(X0),u2_lattices(X0)) ),
inference(consistent_polarity_flipping,[],[f247]) ).
fof(f411,plain,
! [X0,X1] :
( ~ v10_lattices(X0)
| l3_lattices(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| k5_filter_2(X0,X1) = X1 ),
inference(consistent_polarity_flipping,[],[f248]) ).
fof(f412,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,[],[f249]) ).
fof(f413,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,[],[f250]) ).
fof(f416,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(consistent_polarity_flipping,[],[f253]) ).
fof(f418,plain,
! [X0] :
( ~ v3_lattices(k1_lattice2(X0))
| l3_lattices(X0) ),
inference(consistent_polarity_flipping,[],[f256]) ).
fof(f419,plain,
! [X0] :
( ~ l3_lattices(k1_lattice2(X0))
| l3_lattices(X0) ),
inference(consistent_polarity_flipping,[],[f255]) ).
fof(f420,plain,
! [X0,X1] :
( m1_subset_1(k5_filter_2(X0,X1),u1_struct_0(k1_lattice2(X0)))
| l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(consistent_polarity_flipping,[],[f257]) ).
fof(f427,plain,
! [X0] :
( ~ l1_lattices(X0)
| l3_lattices(X0) ),
inference(consistent_polarity_flipping,[],[f265]) ).
fof(f428,plain,
! [X0] :
( ~ l2_lattices(X0)
| l3_lattices(X0) ),
inference(consistent_polarity_flipping,[],[f264]) ).
fof(f430,plain,
! [X0,X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ m1_filter_0(X1,X0)
| l3_lattices(X0) ),
inference(consistent_polarity_flipping,[],[f266]) ).
fof(f434,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,[],[f270]) ).
fof(f435,plain,
! [X0,X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| m2_lattice4(X1,X0)
| l3_lattices(X0) ),
inference(consistent_polarity_flipping,[],[f272]) ).
fof(f436,plain,
! [X0] :
( ~ v1_funct_1(u1_lattices(X0))
| l1_lattices(X0) ),
inference(consistent_polarity_flipping,[],[f276]) ).
fof(f437,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(consistent_polarity_flipping,[],[f275]) ).
fof(f438,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,[],[f274]) ).
fof(f439,plain,
! [X0] :
( ~ v1_funct_1(u2_lattices(X0))
| l2_lattices(X0) ),
inference(consistent_polarity_flipping,[],[f279]) ).
fof(f440,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,[],[f278]) ).
fof(f441,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,[],[f277]) ).
fof(f451,plain,
! [X0] :
( ~ v3_struct_0(k1_lattice2(X0))
| v3_struct_0(X0)
| l3_lattices(X0) ),
inference(consistent_polarity_flipping,[],[f293]) ).
fof(f476,plain,
! [X0] :
( v10_lattices(k1_lattice2(X0))
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| l3_lattices(X0) ),
inference(consistent_polarity_flipping,[],[f313]) ).
fof(f477,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,[],[f324]) ).
fof(f478,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)
| X1 = X4 ),
inference(consistent_polarity_flipping,[],[f323]) ).
fof(f479,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)
| X2 = X5 ),
inference(consistent_polarity_flipping,[],[f322]) ).
fof(f500,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,[],[f372]) ).
fof(f501,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,[],[f373]) ).
fof(f504,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,X0,X1)
| ~ m2_relset_1(X2,X0,X1) ),
inference(consistent_polarity_flipping,[],[f377]) ).
fof(f507,plain,
! [X0,X1] :
( ~ v10_lattices(X0)
| r2_hidden(X1,sK27(X0,X1))
| k5_lattices(X0) = X1
| l3_lattices(X0)
| v13_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0) ),
inference(consistent_polarity_flipping,[],[f382]) ).
fof(f508,plain,
! [X0,X1] :
( v1_filter_0(sK27(X0,X1),X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| k5_lattices(X0) = X1
| l3_lattices(X0)
| v13_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(consistent_polarity_flipping,[],[f381]) ).
fof(f509,plain,
! [X0,X1] :
( ~ v10_lattices(X0)
| m1_filter_0(sK27(X0,X1),X0)
| k5_lattices(X0) = X1
| l3_lattices(X0)
| v13_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0) ),
inference(consistent_polarity_flipping,[],[f380]) ).
fof(f511,plain,
! [X0,X1] :
( ~ v1_filter_0(k15_filter_2(X0,X1),k1_lattice2(X0))
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| m2_filter_2(X1,X0)
| l3_lattices(X0)
| r2_filter_2(X0,X1) ),
inference(consistent_polarity_flipping,[],[f384]) ).
fof(f513,plain,
! [X0] :
( ~ v13_lattices(k1_lattice2(X0))
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| l3_lattices(X0)
| v14_lattices(X0) ),
inference(consistent_polarity_flipping,[],[f390]) ).
fof(f515,plain,
! [X0] :
( v14_lattices(X0)
| l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| k6_lattices(X0) = k5_lattices(k1_lattice2(X0)) ),
inference(consistent_polarity_flipping,[],[f392]) ).
fof(f591,plain,
! [X0] :
( l3_lattices(X0)
| k1_lattice2(k1_lattice2(X0)) = g3_lattices(u1_struct_0(k1_lattice2(X0)),u1_lattices(k1_lattice2(X0)),u2_lattices(k1_lattice2(X0))) ),
inference(resolution,[],[f410,f419]) ).
fof(f592,plain,
k1_lattice2(sK0) = g3_lattices(u1_struct_0(sK0),u1_lattices(sK0),u2_lattices(sK0)),
inference(resolution,[],[f410,f395]) ).
fof(f604,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,[],[f398,f418]) ).
fof(f613,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,[],[f604,f419]) ).
fof(f619,plain,
( l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0)
| k6_lattices(sK0) = k5_lattices(k1_lattice2(sK0)) ),
inference(resolution,[],[f515,f396]) ).
fof(f626,plain,
( ~ v10_lattices(sK0)
| v3_struct_0(sK0)
| k6_lattices(sK0) = k5_lattices(k1_lattice2(sK0)) ),
inference(forward_subsumption_resolution,[],[f619,f395]) ).
fof(f628,plain,
( v3_struct_0(sK0)
| k6_lattices(sK0) = k5_lattices(k1_lattice2(sK0)) ),
inference(forward_subsumption_resolution,[],[f626,f231]) ).
fof(f630,plain,
k6_lattices(sK0) = k5_lattices(k1_lattice2(sK0)),
inference(forward_subsumption_resolution,[],[f628,f232]) ).
fof(f631,plain,
! [X0,X1] :
( l3_lattices(k1_lattice2(X0))
| v3_struct_0(k1_lattice2(X0))
| ~ m1_subset_1(X1,u1_struct_0(k1_lattice2(X0)))
| k5_filter_2(k1_lattice2(X0),X1) = X1
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| l3_lattices(X0) ),
inference(resolution,[],[f411,f476]) ).
fof(f632,plain,
! [X0] :
( l3_lattices(sK0)
| v3_struct_0(sK0)
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| k5_filter_2(sK0,X0) = X0 ),
inference(resolution,[],[f411,f231]) ).
fof(f637,plain,
! [X0] :
( v3_struct_0(sK0)
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| k5_filter_2(sK0,X0) = X0 ),
inference(forward_subsumption_resolution,[],[f632,f395]) ).
fof(f638,plain,
! [X0,X1] :
( v3_struct_0(k1_lattice2(X0))
| ~ m1_subset_1(X1,u1_struct_0(k1_lattice2(X0)))
| k5_filter_2(k1_lattice2(X0),X1) = X1
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| l3_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f631,f419]) ).
fof(f641,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK0))
| k5_filter_2(sK0,X0) = X0 ),
inference(forward_subsumption_resolution,[],[f637,f232]) ).
fof(f642,plain,
! [X0,X1] :
( ~ v10_lattices(X0)
| k5_filter_2(k1_lattice2(X0),X1) = X1
| ~ m1_subset_1(X1,u1_struct_0(k1_lattice2(X0)))
| v3_struct_0(X0)
| l3_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f638,f451]) ).
fof(f645,definition,
( spl28_4
<=> l1_lattices(k1_lattice2(sK0)) ),
introduced(definition,[new_symbols(definition,[spl28_4])],[avatar_definition]) ).
fof(f646,plain,
( ~ l1_lattices(k1_lattice2(sK0))
| spl28_4 ),
inference(avatar_component_clause,[],[f645]) ).
fof(f647,plain,
( l1_lattices(k1_lattice2(sK0))
| ~ spl28_4 ),
inference(avatar_component_clause,[],[f645]) ).
fof(f649,definition,
( spl28_5
<=> v3_struct_0(k1_lattice2(sK0)) ),
introduced(definition,[new_symbols(definition,[spl28_5])],[avatar_definition]) ).
fof(f650,plain,
( ~ v3_struct_0(k1_lattice2(sK0))
| spl28_5 ),
inference(avatar_component_clause,[],[f649]) ).
fof(f651,plain,
( v3_struct_0(k1_lattice2(sK0))
| ~ spl28_5 ),
inference(avatar_component_clause,[],[f649]) ).
fof(f661,plain,
( l3_lattices(k1_lattice2(sK0))
| ~ spl28_4 ),
inference(resolution,[],[f647,f427]) ).
fof(f662,plain,
( l3_lattices(sK0)
| ~ spl28_4 ),
inference(resolution,[],[f661,f419]) ).
fof(f663,plain,
( $false
| ~ spl28_4 ),
inference(forward_subsumption_resolution,[],[f662,f395]) ).
fof(f664,plain,
~ spl28_4,
inference(avatar_contradiction_clause,[],[f663]) ).
fof(f674,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,[],[f412,f231]) ).
fof(f679,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,[],[f674,f395]) ).
fof(f683,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0)))
| k7_filter_2(sK0,X0) = X0 ),
inference(forward_subsumption_resolution,[],[f679,f232]) ).
fof(f685,plain,
( v3_struct_0(sK0)
| l3_lattices(sK0)
| ~ spl28_5 ),
inference(resolution,[],[f651,f451]) ).
fof(f686,plain,
( l3_lattices(sK0)
| ~ spl28_5 ),
inference(forward_subsumption_resolution,[],[f685,f232]) ).
fof(f687,plain,
( $false
| ~ spl28_5 ),
inference(forward_subsumption_resolution,[],[f686,f395]) ).
fof(f688,plain,
~ spl28_5,
inference(avatar_contradiction_clause,[],[f687]) ).
fof(f706,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,[],[f413,f231]) ).
fof(f711,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,[],[f706,f395]) ).
fof(f715,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,[],[f711,f232]) ).
fof(f719,plain,
sK1 = k5_filter_2(sK0,sK1),
inference(resolution,[],[f641,f227]) ).
fof(f724,definition,
( spl28_10
<=> l1_lattices(sK0) ),
introduced(definition,[new_symbols(definition,[spl28_10])],[avatar_definition]) ).
fof(f725,plain,
( ~ l1_lattices(sK0)
| spl28_10 ),
inference(avatar_component_clause,[],[f724]) ).
fof(f726,plain,
( l1_lattices(sK0)
| ~ spl28_10 ),
inference(avatar_component_clause,[],[f724]) ).
fof(f733,definition,
( spl28_12
<=> l2_lattices(sK0) ),
introduced(definition,[new_symbols(definition,[spl28_12])],[avatar_definition]) ).
fof(f734,plain,
( ~ l2_lattices(sK0)
| spl28_12 ),
inference(avatar_component_clause,[],[f733]) ).
fof(f735,plain,
( l2_lattices(sK0)
| ~ spl28_12 ),
inference(avatar_component_clause,[],[f733]) ).
fof(f751,plain,
( l3_lattices(sK0)
| ~ spl28_10 ),
inference(resolution,[],[f726,f427]) ).
fof(f752,plain,
( $false
| ~ spl28_10 ),
inference(forward_subsumption_resolution,[],[f751,f395]) ).
fof(f753,plain,
~ spl28_10,
inference(avatar_contradiction_clause,[],[f752]) ).
fof(f760,plain,
( l3_lattices(sK0)
| ~ spl28_12 ),
inference(resolution,[],[f735,f428]) ).
fof(f761,plain,
( $false
| ~ spl28_12 ),
inference(forward_subsumption_resolution,[],[f760,f395]) ).
fof(f762,plain,
~ spl28_12,
inference(avatar_contradiction_clause,[],[f761]) ).
fof(f763,plain,
! [X0,X1] :
( r2_hidden(X0,sK27(k1_lattice2(X1),X0))
| k5_lattices(k1_lattice2(X1)) = X0
| l3_lattices(k1_lattice2(X1))
| v13_lattices(k1_lattice2(X1))
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(X1)))
| v3_struct_0(k1_lattice2(X1))
| ~ v10_lattices(X1)
| v3_struct_0(X1)
| l3_lattices(X1) ),
inference(resolution,[],[f507,f476]) ).
fof(f770,plain,
! [X0,X1] :
( r2_hidden(X0,sK27(k1_lattice2(X1),X0))
| k5_lattices(k1_lattice2(X1)) = X0
| v13_lattices(k1_lattice2(X1))
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(X1)))
| v3_struct_0(k1_lattice2(X1))
| ~ v10_lattices(X1)
| v3_struct_0(X1)
| l3_lattices(X1) ),
inference(forward_subsumption_resolution,[],[f763,f419]) ).
fof(f774,plain,
! [X0,X1] :
( ~ v10_lattices(X1)
| k5_lattices(k1_lattice2(X1)) = X0
| v13_lattices(k1_lattice2(X1))
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(X1)))
| r2_hidden(X0,sK27(k1_lattice2(X1),X0))
| v3_struct_0(X1)
| l3_lattices(X1) ),
inference(forward_subsumption_resolution,[],[f770,f451]) ).
fof(f792,plain,
! [X0,X1] :
( m1_filter_0(sK27(k1_lattice2(X0),X1),k1_lattice2(X0))
| k5_lattices(k1_lattice2(X0)) = X1
| l3_lattices(k1_lattice2(X0))
| v13_lattices(k1_lattice2(X0))
| ~ m1_subset_1(X1,u1_struct_0(k1_lattice2(X0)))
| v3_struct_0(k1_lattice2(X0))
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| l3_lattices(X0) ),
inference(resolution,[],[f509,f476]) ).
fof(f799,plain,
! [X0,X1] :
( m1_filter_0(sK27(k1_lattice2(X0),X1),k1_lattice2(X0))
| k5_lattices(k1_lattice2(X0)) = X1
| v13_lattices(k1_lattice2(X0))
| ~ m1_subset_1(X1,u1_struct_0(k1_lattice2(X0)))
| v3_struct_0(k1_lattice2(X0))
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| l3_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f792,f419]) ).
fof(f803,plain,
! [X0,X1] :
( m1_filter_0(sK27(k1_lattice2(X0),X1),k1_lattice2(X0))
| k5_lattices(k1_lattice2(X0)) = X1
| v13_lattices(k1_lattice2(X0))
| ~ m1_subset_1(X1,u1_struct_0(k1_lattice2(X0)))
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| l3_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f799,f451]) ).
fof(f829,plain,
! [X2,X3,X0,X1,X4] :
( ~ v1_funct_2(X0,k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| v1_funct_1(X0)
| m1_relset_1(u1_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| m1_relset_1(X0,k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| v1_funct_1(u1_lattices(X1))
| g3_lattices(u1_struct_0(X1),u1_lattices(X1),X0) != g3_lattices(X2,X3,X4)
| u1_struct_0(X1) = X2
| l1_lattices(X1) ),
inference(resolution,[],[f477,f437]) ).
fof(f832,plain,
! [X2,X3,X0,X1,X4] :
( ~ v1_funct_2(X0,k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| v1_funct_1(X0)
| m1_relset_1(u1_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| m1_relset_1(X0,k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| g3_lattices(u1_struct_0(X1),u1_lattices(X1),X0) != g3_lattices(X2,X3,X4)
| u1_struct_0(X1) = X2
| l1_lattices(X1) ),
inference(forward_subsumption_resolution,[],[f829,f436]) ).
fof(f833,plain,
! [X2,X3,X0,X1,X4] :
( ~ v1_funct_2(X0,k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| v1_funct_1(X0)
| m1_relset_1(u1_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| m1_relset_1(X0,k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| v1_funct_1(u1_lattices(X1))
| g3_lattices(u1_struct_0(X1),u1_lattices(X1),X0) != g3_lattices(X2,X3,X4)
| u1_lattices(X1) = X3
| l1_lattices(X1) ),
inference(resolution,[],[f478,f437]) ).
fof(f836,plain,
! [X2,X3,X0,X1,X4] :
( ~ v1_funct_2(X0,k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| v1_funct_1(X0)
| m1_relset_1(u1_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| m1_relset_1(X0,k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| g3_lattices(u1_struct_0(X1),u1_lattices(X1),X0) != g3_lattices(X2,X3,X4)
| u1_lattices(X1) = X3
| l1_lattices(X1) ),
inference(forward_subsumption_resolution,[],[f833,f436]) ).
fof(f837,plain,
( m1_subset_1(sK1,u1_struct_0(k1_lattice2(sK0)))
| l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0)
| ~ m1_subset_1(sK1,u1_struct_0(sK0)) ),
inference(superposition,[],[f420,f719]) ).
fof(f838,plain,
( m1_subset_1(sK1,u1_struct_0(k1_lattice2(sK0)))
| ~ v10_lattices(sK0)
| v3_struct_0(sK0)
| ~ m1_subset_1(sK1,u1_struct_0(sK0)) ),
inference(forward_subsumption_resolution,[],[f837,f395]) ).
fof(f839,plain,
( m1_subset_1(sK1,u1_struct_0(k1_lattice2(sK0)))
| v3_struct_0(sK0)
| ~ m1_subset_1(sK1,u1_struct_0(sK0)) ),
inference(forward_subsumption_resolution,[],[f838,f231]) ).
fof(f840,plain,
( m1_subset_1(sK1,u1_struct_0(k1_lattice2(sK0)))
| ~ m1_subset_1(sK1,u1_struct_0(sK0)) ),
inference(forward_subsumption_resolution,[],[f839,f232]) ).
fof(f841,plain,
m1_subset_1(sK1,u1_struct_0(k1_lattice2(sK0))),
inference(forward_subsumption_resolution,[],[f840,f227]) ).
fof(f842,plain,
! [X2,X3,X0,X1,X4] :
( ~ v1_funct_2(X0,k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| v1_funct_1(X0)
| m1_relset_1(u1_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| m1_relset_1(X0,k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| v1_funct_1(u1_lattices(X1))
| g3_lattices(u1_struct_0(X1),u1_lattices(X1),X0) != g3_lattices(X2,X3,X4)
| X0 = X4
| l1_lattices(X1) ),
inference(resolution,[],[f479,f437]) ).
fof(f845,plain,
! [X2,X3,X0,X1,X4] :
( ~ v1_funct_2(X0,k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| v1_funct_1(X0)
| m1_relset_1(u1_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| m1_relset_1(X0,k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| g3_lattices(u1_struct_0(X1),u1_lattices(X1),X0) != g3_lattices(X2,X3,X4)
| X0 = X4
| l1_lattices(X1) ),
inference(forward_subsumption_resolution,[],[f842,f436]) ).
fof(f846,plain,
! [X0] :
( k7_filter_2(sK0,X0) = X0
| ~ v10_lattices(sK0)
| v3_struct_0(sK0)
| m2_lattice4(X0,sK0)
| l3_lattices(sK0) ),
inference(resolution,[],[f683,f435]) ).
fof(f864,plain,
! [X0] :
( k7_filter_2(sK0,X0) = X0
| v3_struct_0(sK0)
| m2_lattice4(X0,sK0)
| l3_lattices(sK0) ),
inference(forward_subsumption_resolution,[],[f846,f231]) ).
fof(f876,plain,
! [X0] :
( k7_filter_2(sK0,X0) = X0
| m2_lattice4(X0,sK0)
| l3_lattices(sK0) ),
inference(forward_subsumption_resolution,[],[f864,f232]) ).
fof(f879,plain,
! [X0] :
( m2_lattice4(X0,sK0)
| k7_filter_2(sK0,X0) = X0 ),
inference(forward_subsumption_resolution,[],[f876,f395]) ).
fof(f887,plain,
! [X0] :
( k8_filter_2(sK0,X0) = X0
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0))
| ~ m1_filter_0(X0,k1_lattice2(sK0))
| l3_lattices(k1_lattice2(sK0)) ),
inference(resolution,[],[f715,f430]) ).
fof(f905,plain,
( ! [X0] :
( k8_filter_2(sK0,X0) = X0
| ~ v10_lattices(k1_lattice2(sK0))
| ~ m1_filter_0(X0,k1_lattice2(sK0))
| l3_lattices(k1_lattice2(sK0)) )
| spl28_5 ),
inference(forward_subsumption_resolution,[],[f887,f650]) ).
fof(f917,definition,
( spl28_26
<=> v10_lattices(k1_lattice2(sK0)) ),
introduced(definition,[new_symbols(definition,[spl28_26])],[avatar_definition]) ).
fof(f918,plain,
( v10_lattices(k1_lattice2(sK0))
| ~ spl28_26 ),
inference(avatar_component_clause,[],[f917]) ).
fof(f919,plain,
( ~ v10_lattices(k1_lattice2(sK0))
| spl28_26 ),
inference(avatar_component_clause,[],[f917]) ).
fof(f921,definition,
( spl28_27
<=> l3_lattices(k1_lattice2(sK0)) ),
introduced(definition,[new_symbols(definition,[spl28_27])],[avatar_definition]) ).
fof(f922,plain,
( ~ l3_lattices(k1_lattice2(sK0))
| spl28_27 ),
inference(avatar_component_clause,[],[f921]) ).
fof(f923,plain,
( l3_lattices(k1_lattice2(sK0))
| ~ spl28_27 ),
inference(avatar_component_clause,[],[f921]) ).
fof(f930,definition,
( spl28_29
<=> ! [X0] :
( k8_filter_2(sK0,X0) = X0
| ~ m1_filter_0(X0,k1_lattice2(sK0)) ) ),
introduced(definition,[new_symbols(definition,[spl28_29])],[avatar_definition]) ).
fof(f931,plain,
( ! [X0] :
( ~ m1_filter_0(X0,k1_lattice2(sK0))
| k8_filter_2(sK0,X0) = X0 )
| ~ spl28_29 ),
inference(avatar_component_clause,[],[f930]) ).
fof(f932,plain,
( spl28_27
| ~ spl28_26
| spl28_29
| spl28_5 ),
inference(avatar_split_clause,[],[f905,f649,f930,f917,f921]) ).
fof(f959,plain,
( ~ v10_lattices(sK0)
| v3_struct_0(sK0)
| l3_lattices(sK0)
| spl28_26 ),
inference(resolution,[],[f919,f476]) ).
fof(f960,plain,
( v3_struct_0(sK0)
| l3_lattices(sK0)
| spl28_26 ),
inference(forward_subsumption_resolution,[],[f959,f231]) ).
fof(f961,plain,
( l3_lattices(sK0)
| spl28_26 ),
inference(forward_subsumption_resolution,[],[f960,f232]) ).
fof(f962,plain,
( $false
| spl28_26 ),
inference(forward_subsumption_resolution,[],[f961,f395]) ).
fof(f963,plain,
spl28_26,
inference(avatar_contradiction_clause,[],[f962]) ).
fof(f998,definition,
( spl28_38
<=> ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK0)))
| k5_filter_2(k1_lattice2(sK0),X0) = X0 ) ),
introduced(definition,[new_symbols(definition,[spl28_38])],[avatar_definition]) ).
fof(f999,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK0)))
| k5_filter_2(k1_lattice2(sK0),X0) = X0 )
| ~ spl28_38 ),
inference(avatar_component_clause,[],[f998]) ).
fof(f1012,definition,
( spl28_41
<=> v13_lattices(k1_lattice2(sK0)) ),
introduced(definition,[new_symbols(definition,[spl28_41])],[avatar_definition]) ).
fof(f1013,plain,
( ~ v13_lattices(k1_lattice2(sK0))
| spl28_41 ),
inference(avatar_component_clause,[],[f1012]) ).
fof(f1014,plain,
( v13_lattices(k1_lattice2(sK0))
| ~ spl28_41 ),
inference(avatar_component_clause,[],[f1012]) ).
fof(f1046,plain,
( l3_lattices(sK0)
| ~ spl28_27 ),
inference(resolution,[],[f923,f419]) ).
fof(f1047,plain,
( $false
| ~ spl28_27 ),
inference(forward_subsumption_resolution,[],[f1046,f395]) ).
fof(f1048,plain,
~ spl28_27,
inference(avatar_contradiction_clause,[],[f1047]) ).
fof(f1112,plain,
( ~ v10_lattices(sK0)
| v3_struct_0(sK0)
| l3_lattices(sK0)
| v14_lattices(sK0)
| ~ spl28_41 ),
inference(resolution,[],[f1014,f513]) ).
fof(f1115,plain,
( v3_struct_0(sK0)
| l3_lattices(sK0)
| v14_lattices(sK0)
| ~ spl28_41 ),
inference(forward_subsumption_resolution,[],[f1112,f231]) ).
fof(f1117,plain,
( l3_lattices(sK0)
| v14_lattices(sK0)
| ~ spl28_41 ),
inference(forward_subsumption_resolution,[],[f1115,f232]) ).
fof(f1118,plain,
( v14_lattices(sK0)
| ~ spl28_41 ),
inference(forward_subsumption_resolution,[],[f1117,f395]) ).
fof(f1119,plain,
( $false
| ~ spl28_41 ),
inference(forward_subsumption_resolution,[],[f1118,f396]) ).
fof(f1120,plain,
~ spl28_41,
inference(avatar_contradiction_clause,[],[f1119]) ).
fof(f1336,plain,
( k1_lattice2(k1_lattice2(sK0)) = g3_lattices(u1_struct_0(k1_lattice2(k1_lattice2(sK0))),u2_lattices(k1_lattice2(k1_lattice2(sK0))),u1_lattices(k1_lattice2(k1_lattice2(sK0))))
| spl28_27 ),
inference(resolution,[],[f613,f922]) ).
fof(f1337,plain,
k1_lattice2(sK0) = g3_lattices(u1_struct_0(k1_lattice2(sK0)),u2_lattices(k1_lattice2(sK0)),u1_lattices(k1_lattice2(sK0))),
inference(resolution,[],[f613,f395]) ).
fof(f1371,plain,
( k1_lattice2(k1_lattice2(k1_lattice2(sK0))) = g3_lattices(u1_struct_0(k1_lattice2(k1_lattice2(sK0))),u1_lattices(k1_lattice2(k1_lattice2(sK0))),u2_lattices(k1_lattice2(k1_lattice2(sK0))))
| spl28_27 ),
inference(resolution,[],[f591,f922]) ).
fof(f1372,plain,
k1_lattice2(k1_lattice2(sK0)) = g3_lattices(u1_struct_0(k1_lattice2(sK0)),u1_lattices(k1_lattice2(sK0)),u2_lattices(k1_lattice2(sK0))),
inference(resolution,[],[f591,f395]) ).
fof(f1378,plain,
! [X0,X1] :
( k5_filter_2(k1_lattice2(k1_lattice2(X0)),X1) = X1
| ~ m1_subset_1(X1,u1_struct_0(k1_lattice2(k1_lattice2(X0))))
| v3_struct_0(k1_lattice2(X0))
| l3_lattices(k1_lattice2(X0))
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| l3_lattices(X0) ),
inference(resolution,[],[f642,f476]) ).
fof(f1380,plain,
! [X0] :
( k5_filter_2(k1_lattice2(sK0),X0) = X0
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK0)))
| v3_struct_0(sK0)
| l3_lattices(sK0) ),
inference(resolution,[],[f642,f231]) ).
fof(f1385,plain,
! [X0] :
( k5_filter_2(k1_lattice2(sK0),X0) = X0
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK0)))
| l3_lattices(sK0) ),
inference(forward_subsumption_resolution,[],[f1380,f232]) ).
fof(f1387,plain,
! [X0,X1] :
( k5_filter_2(k1_lattice2(k1_lattice2(X0)),X1) = X1
| ~ m1_subset_1(X1,u1_struct_0(k1_lattice2(k1_lattice2(X0))))
| l3_lattices(k1_lattice2(X0))
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| l3_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f1378,f451]) ).
fof(f1390,plain,
! [X0] :
( k5_filter_2(k1_lattice2(sK0),X0) = X0
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK0))) ),
inference(forward_subsumption_resolution,[],[f1385,f395]) ).
fof(f1392,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u1_struct_0(k1_lattice2(k1_lattice2(X0))))
| k5_filter_2(k1_lattice2(k1_lattice2(X0)),X1) = X1
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| l3_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f1387,f419]) ).
fof(f1393,plain,
spl28_38,
inference(avatar_split_clause,[],[f1390,f998]) ).
fof(f1441,plain,
! [X0,X1] :
( k5_lattices(k1_lattice2(k1_lattice2(X0))) = X1
| v13_lattices(k1_lattice2(k1_lattice2(X0)))
| ~ m1_subset_1(X1,u1_struct_0(k1_lattice2(k1_lattice2(X0))))
| r2_hidden(X1,sK27(k1_lattice2(k1_lattice2(X0)),X1))
| v3_struct_0(k1_lattice2(X0))
| l3_lattices(k1_lattice2(X0))
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| l3_lattices(X0) ),
inference(resolution,[],[f774,f476]) ).
fof(f1450,plain,
! [X0,X1] :
( k5_lattices(k1_lattice2(k1_lattice2(X0))) = X1
| v13_lattices(k1_lattice2(k1_lattice2(X0)))
| ~ m1_subset_1(X1,u1_struct_0(k1_lattice2(k1_lattice2(X0))))
| r2_hidden(X1,sK27(k1_lattice2(k1_lattice2(X0)),X1))
| l3_lattices(k1_lattice2(X0))
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| l3_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f1441,f451]) ).
fof(f1455,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u1_struct_0(k1_lattice2(k1_lattice2(X0))))
| v13_lattices(k1_lattice2(k1_lattice2(X0)))
| k5_lattices(k1_lattice2(k1_lattice2(X0))) = X1
| r2_hidden(X1,sK27(k1_lattice2(k1_lattice2(X0)),X1))
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| l3_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f1450,f419]) ).
fof(f1506,plain,
! [X0,X1] :
( k5_lattices(k1_lattice2(X0)) = X1
| v13_lattices(k1_lattice2(X0))
| ~ m1_subset_1(X1,u1_struct_0(k1_lattice2(X0)))
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| l3_lattices(X0)
| l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| k8_filter_2(X0,sK27(k1_lattice2(X0),X1)) = k14_filter_2(X0,sK27(k1_lattice2(X0),X1)) ),
inference(resolution,[],[f803,f500]) ).
fof(f1507,plain,
! [X0,X1] :
( k5_lattices(k1_lattice2(X0)) = X1
| v13_lattices(k1_lattice2(X0))
| ~ m1_subset_1(X1,u1_struct_0(k1_lattice2(X0)))
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| l3_lattices(X0)
| l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ m2_filter_2(k14_filter_2(X0,sK27(k1_lattice2(X0),X1)),X0) ),
inference(resolution,[],[f803,f416]) ).
fof(f1510,plain,
! [X0,X1] :
( ~ m2_filter_2(k14_filter_2(X0,sK27(k1_lattice2(X0),X1)),X0)
| v13_lattices(k1_lattice2(X0))
| ~ m1_subset_1(X1,u1_struct_0(k1_lattice2(X0)))
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| l3_lattices(X0)
| k5_lattices(k1_lattice2(X0)) = X1 ),
inference(duplicate_literal_removal,[],[f1507]) ).
fof(f1511,plain,
! [X0,X1] :
( ~ v10_lattices(X0)
| v13_lattices(k1_lattice2(X0))
| ~ m1_subset_1(X1,u1_struct_0(k1_lattice2(X0)))
| k5_lattices(k1_lattice2(X0)) = X1
| v3_struct_0(X0)
| l3_lattices(X0)
| k8_filter_2(X0,sK27(k1_lattice2(X0),X1)) = k14_filter_2(X0,sK27(k1_lattice2(X0),X1)) ),
inference(duplicate_literal_removal,[],[f1506]) ).
fof(f1556,plain,
! [X2,X3,X0,X1] :
( v1_funct_1(u2_lattices(X0))
| m1_relset_1(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| m1_relset_1(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| g3_lattices(u1_struct_0(X0),u1_lattices(X0),u2_lattices(X0)) != g3_lattices(X1,X2,X3)
| u2_lattices(X0) = X3
| l1_lattices(X0)
| l2_lattices(X0) ),
inference(resolution,[],[f845,f440]) ).
fof(f1558,plain,
! [X2,X3,X0,X1] :
( m1_relset_1(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| m1_relset_1(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| g3_lattices(u1_struct_0(X0),u1_lattices(X0),u2_lattices(X0)) != g3_lattices(X1,X2,X3)
| u2_lattices(X0) = X3
| l1_lattices(X0)
| l2_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f1556,f439]) ).
fof(f1575,plain,
! [X2,X3,X0,X1] :
( v1_funct_1(u2_lattices(X0))
| m1_relset_1(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| m1_relset_1(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| g3_lattices(u1_struct_0(X0),u1_lattices(X0),u2_lattices(X0)) != g3_lattices(X1,X2,X3)
| u1_struct_0(X0) = X1
| l1_lattices(X0)
| l2_lattices(X0) ),
inference(resolution,[],[f832,f440]) ).
fof(f1577,plain,
! [X2,X3,X0,X1] :
( m1_relset_1(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| m1_relset_1(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| g3_lattices(u1_struct_0(X0),u1_lattices(X0),u2_lattices(X0)) != g3_lattices(X1,X2,X3)
| u1_struct_0(X0) = X1
| l1_lattices(X0)
| l2_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f1575,f439]) ).
fof(f1585,plain,
! [X2,X3,X0,X1] :
( v1_funct_1(u2_lattices(X0))
| m1_relset_1(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| m1_relset_1(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| g3_lattices(u1_struct_0(X0),u1_lattices(X0),u2_lattices(X0)) != g3_lattices(X1,X2,X3)
| u1_lattices(X0) = X2
| l1_lattices(X0)
| l2_lattices(X0) ),
inference(resolution,[],[f836,f440]) ).
fof(f1587,plain,
! [X2,X3,X0,X1] :
( m1_relset_1(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| m1_relset_1(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| g3_lattices(u1_struct_0(X0),u1_lattices(X0),u2_lattices(X0)) != g3_lattices(X1,X2,X3)
| u1_lattices(X0) = X2
| l1_lattices(X0)
| l2_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f1585,f439]) ).
fof(f1631,plain,
! [X0] :
( k7_filter_2(sK0,X0) = X0
| ~ v10_lattices(sK0)
| v3_struct_0(sK0)
| m2_filter_2(X0,sK0)
| l3_lattices(sK0) ),
inference(resolution,[],[f879,f434]) ).
fof(f1634,plain,
! [X0] :
( k7_filter_2(sK0,X0) = X0
| v3_struct_0(sK0)
| m2_filter_2(X0,sK0)
| l3_lattices(sK0) ),
inference(forward_subsumption_resolution,[],[f1631,f231]) ).
fof(f1638,plain,
! [X0] :
( k7_filter_2(sK0,X0) = X0
| m2_filter_2(X0,sK0)
| l3_lattices(sK0) ),
inference(forward_subsumption_resolution,[],[f1634,f232]) ).
fof(f1642,plain,
! [X0] :
( m2_filter_2(X0,sK0)
| k7_filter_2(sK0,X0) = X0 ),
inference(forward_subsumption_resolution,[],[f1638,f395]) ).
fof(f1692,plain,
( ! [X0] :
( sK27(k1_lattice2(sK0),X0) = k8_filter_2(sK0,sK27(k1_lattice2(sK0),X0))
| k5_lattices(k1_lattice2(sK0)) = X0
| v13_lattices(k1_lattice2(sK0))
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK0)))
| ~ v10_lattices(sK0)
| v3_struct_0(sK0)
| l3_lattices(sK0) )
| ~ spl28_29 ),
inference(resolution,[],[f931,f803]) ).
fof(f1697,plain,
( ! [X0] :
( sK27(k1_lattice2(sK0),X0) = k8_filter_2(sK0,sK27(k1_lattice2(sK0),X0))
| k5_lattices(k1_lattice2(sK0)) = X0
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK0)))
| ~ v10_lattices(sK0)
| v3_struct_0(sK0)
| l3_lattices(sK0) )
| ~ spl28_29
| spl28_41 ),
inference(forward_subsumption_resolution,[],[f1692,f1013]) ).
fof(f1701,plain,
( ! [X0] :
( sK27(k1_lattice2(sK0),X0) = k8_filter_2(sK0,sK27(k1_lattice2(sK0),X0))
| k5_lattices(k1_lattice2(sK0)) = X0
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK0)))
| v3_struct_0(sK0)
| l3_lattices(sK0) )
| ~ spl28_29
| spl28_41 ),
inference(forward_subsumption_resolution,[],[f1697,f231]) ).
fof(f1705,plain,
( ! [X0] :
( sK27(k1_lattice2(sK0),X0) = k8_filter_2(sK0,sK27(k1_lattice2(sK0),X0))
| k5_lattices(k1_lattice2(sK0)) = X0
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK0)))
| l3_lattices(sK0) )
| ~ spl28_29
| spl28_41 ),
inference(forward_subsumption_resolution,[],[f1701,f232]) ).
fof(f1707,plain,
( ! [X0] :
( sK27(k1_lattice2(sK0),X0) = k8_filter_2(sK0,sK27(k1_lattice2(sK0),X0))
| k5_lattices(k1_lattice2(sK0)) = X0
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK0))) )
| ~ spl28_29
| spl28_41 ),
inference(forward_subsumption_resolution,[],[f1705,f395]) ).
fof(f1708,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK0)))
| sK27(k1_lattice2(sK0),X0) = k8_filter_2(sK0,sK27(k1_lattice2(sK0),X0))
| k6_lattices(sK0) = X0 )
| ~ spl28_29
| spl28_41 ),
inference(forward_demodulation,[],[f1707,f630]) ).
fof(f3526,plain,
! [X0,X1] :
( k5_filter_2(k1_lattice2(X0),X1) = k5_filter_2(k1_lattice2(k1_lattice2(X0)),k5_filter_2(k1_lattice2(X0),X1))
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| l3_lattices(X0)
| l3_lattices(k1_lattice2(X0))
| ~ v10_lattices(k1_lattice2(X0))
| v3_struct_0(k1_lattice2(X0))
| ~ m1_subset_1(X1,u1_struct_0(k1_lattice2(X0))) ),
inference(resolution,[],[f1392,f420]) ).
fof(f3529,plain,
! [X0,X1] :
( k5_filter_2(k1_lattice2(X0),X1) = k5_filter_2(k1_lattice2(k1_lattice2(X0)),k5_filter_2(k1_lattice2(X0),X1))
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| l3_lattices(X0)
| ~ v10_lattices(k1_lattice2(X0))
| v3_struct_0(k1_lattice2(X0))
| ~ m1_subset_1(X1,u1_struct_0(k1_lattice2(X0))) ),
inference(forward_subsumption_resolution,[],[f3526,f419]) ).
fof(f3530,plain,
! [X0,X1] :
( k5_filter_2(k1_lattice2(X0),X1) = k5_filter_2(k1_lattice2(k1_lattice2(X0)),k5_filter_2(k1_lattice2(X0),X1))
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| l3_lattices(X0)
| v3_struct_0(k1_lattice2(X0))
| ~ m1_subset_1(X1,u1_struct_0(k1_lattice2(X0))) ),
inference(forward_subsumption_resolution,[],[f3529,f476]) ).
fof(f3531,plain,
! [X0,X1] :
( ~ v10_lattices(X0)
| k5_filter_2(k1_lattice2(X0),X1) = k5_filter_2(k1_lattice2(k1_lattice2(X0)),k5_filter_2(k1_lattice2(X0),X1))
| v3_struct_0(X0)
| l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(k1_lattice2(X0))) ),
inference(forward_subsumption_resolution,[],[f3530,f451]) ).
fof(f3821,plain,
! [X0,X1] :
( v13_lattices(k1_lattice2(X0))
| ~ m1_subset_1(X1,u1_struct_0(k1_lattice2(X0)))
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| l3_lattices(X0)
| k5_lattices(k1_lattice2(X0)) = X1
| l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| k15_filter_2(X0,k14_filter_2(X0,sK27(k1_lattice2(X0),X1))) = k7_filter_2(X0,k14_filter_2(X0,sK27(k1_lattice2(X0),X1))) ),
inference(resolution,[],[f1510,f501]) ).
fof(f3824,plain,
! [X0,X1] :
( ~ v10_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(k1_lattice2(X0)))
| v13_lattices(k1_lattice2(X0))
| v3_struct_0(X0)
| l3_lattices(X0)
| k5_lattices(k1_lattice2(X0)) = X1
| k15_filter_2(X0,k14_filter_2(X0,sK27(k1_lattice2(X0),X1))) = k7_filter_2(X0,k14_filter_2(X0,sK27(k1_lattice2(X0),X1))) ),
inference(duplicate_literal_removal,[],[f3821]) ).
fof(f3860,plain,
! [X0,X1] :
( v13_lattices(k1_lattice2(k1_lattice2(X0)))
| k5_filter_2(k1_lattice2(X0),X1) = k5_lattices(k1_lattice2(k1_lattice2(X0)))
| r2_hidden(k5_filter_2(k1_lattice2(X0),X1),sK27(k1_lattice2(k1_lattice2(X0)),k5_filter_2(k1_lattice2(X0),X1)))
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| l3_lattices(X0)
| l3_lattices(k1_lattice2(X0))
| ~ v10_lattices(k1_lattice2(X0))
| v3_struct_0(k1_lattice2(X0))
| ~ m1_subset_1(X1,u1_struct_0(k1_lattice2(X0))) ),
inference(resolution,[],[f1455,f420]) ).
fof(f3863,plain,
! [X0,X1] :
( v13_lattices(k1_lattice2(k1_lattice2(X0)))
| k5_filter_2(k1_lattice2(X0),X1) = k5_lattices(k1_lattice2(k1_lattice2(X0)))
| r2_hidden(k5_filter_2(k1_lattice2(X0),X1),sK27(k1_lattice2(k1_lattice2(X0)),k5_filter_2(k1_lattice2(X0),X1)))
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| l3_lattices(X0)
| ~ v10_lattices(k1_lattice2(X0))
| v3_struct_0(k1_lattice2(X0))
| ~ m1_subset_1(X1,u1_struct_0(k1_lattice2(X0))) ),
inference(forward_subsumption_resolution,[],[f3860,f419]) ).
fof(f3864,plain,
! [X0,X1] :
( v13_lattices(k1_lattice2(k1_lattice2(X0)))
| k5_filter_2(k1_lattice2(X0),X1) = k5_lattices(k1_lattice2(k1_lattice2(X0)))
| r2_hidden(k5_filter_2(k1_lattice2(X0),X1),sK27(k1_lattice2(k1_lattice2(X0)),k5_filter_2(k1_lattice2(X0),X1)))
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| l3_lattices(X0)
| v3_struct_0(k1_lattice2(X0))
| ~ m1_subset_1(X1,u1_struct_0(k1_lattice2(X0))) ),
inference(forward_subsumption_resolution,[],[f3863,f476]) ).
fof(f3865,plain,
! [X0,X1] :
( r2_hidden(k5_filter_2(k1_lattice2(X0),X1),sK27(k1_lattice2(k1_lattice2(X0)),k5_filter_2(k1_lattice2(X0),X1)))
| k5_filter_2(k1_lattice2(X0),X1) = k5_lattices(k1_lattice2(k1_lattice2(X0)))
| v13_lattices(k1_lattice2(k1_lattice2(X0)))
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(k1_lattice2(X0))) ),
inference(forward_subsumption_resolution,[],[f3864,f451]) ).
fof(f3871,plain,
! [X0] :
( v13_lattices(k1_lattice2(sK0))
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK0)))
| k5_lattices(k1_lattice2(sK0)) = X0
| v3_struct_0(sK0)
| l3_lattices(sK0)
| k8_filter_2(sK0,sK27(k1_lattice2(sK0),X0)) = k14_filter_2(sK0,sK27(k1_lattice2(sK0),X0)) ),
inference(resolution,[],[f1511,f231]) ).
fof(f3875,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK0)))
| k5_lattices(k1_lattice2(sK0)) = X0
| v3_struct_0(sK0)
| l3_lattices(sK0)
| k8_filter_2(sK0,sK27(k1_lattice2(sK0),X0)) = k14_filter_2(sK0,sK27(k1_lattice2(sK0),X0)) )
| spl28_41 ),
inference(forward_subsumption_resolution,[],[f3871,f1013]) ).
fof(f3881,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK0)))
| k5_lattices(k1_lattice2(sK0)) = X0
| l3_lattices(sK0)
| k8_filter_2(sK0,sK27(k1_lattice2(sK0),X0)) = k14_filter_2(sK0,sK27(k1_lattice2(sK0),X0)) )
| spl28_41 ),
inference(forward_subsumption_resolution,[],[f3875,f232]) ).
fof(f3887,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK0)))
| k5_lattices(k1_lattice2(sK0)) = X0
| k8_filter_2(sK0,sK27(k1_lattice2(sK0),X0)) = k14_filter_2(sK0,sK27(k1_lattice2(sK0),X0)) )
| spl28_41 ),
inference(forward_subsumption_resolution,[],[f3881,f395]) ).
fof(f3898,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK0)))
| k6_lattices(sK0) = X0
| k8_filter_2(sK0,sK27(k1_lattice2(sK0),X0)) = k14_filter_2(sK0,sK27(k1_lattice2(sK0),X0)) )
| spl28_41 ),
inference(forward_demodulation,[],[f3887,f630]) ).
fof(f3931,plain,
! [X2,X3,X0,X1] :
( m1_relset_1(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| g3_lattices(u1_struct_0(X0),u1_lattices(X0),u2_lattices(X0)) != g3_lattices(X1,X2,X3)
| u2_lattices(X0) = X3
| l1_lattices(X0)
| l2_lattices(X0)
| ~ m2_relset_1(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0)) ),
inference(resolution,[],[f1558,f504]) ).
fof(f3932,plain,
! [X2,X3,X0,X1] :
( m1_relset_1(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| g3_lattices(u1_struct_0(X0),u1_lattices(X0),u2_lattices(X0)) != g3_lattices(X1,X2,X3)
| u2_lattices(X0) = X3
| l1_lattices(X0)
| l2_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f3931,f438]) ).
fof(f3935,plain,
! [X2,X3,X0,X1] :
( m1_relset_1(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| g3_lattices(u1_struct_0(X0),u1_lattices(X0),u2_lattices(X0)) != g3_lattices(X1,X2,X3)
| u1_struct_0(X0) = X1
| l1_lattices(X0)
| l2_lattices(X0)
| ~ m2_relset_1(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0)) ),
inference(resolution,[],[f1577,f504]) ).
fof(f3936,plain,
! [X2,X3,X0,X1] :
( m1_relset_1(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| g3_lattices(u1_struct_0(X0),u1_lattices(X0),u2_lattices(X0)) != g3_lattices(X1,X2,X3)
| u1_struct_0(X0) = X1
| l1_lattices(X0)
| l2_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f3935,f438]) ).
fof(f3940,plain,
! [X2,X3,X0,X1] :
( m1_relset_1(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| g3_lattices(u1_struct_0(X0),u1_lattices(X0),u2_lattices(X0)) != g3_lattices(X1,X2,X3)
| u1_lattices(X0) = X2
| l1_lattices(X0)
| l2_lattices(X0)
| ~ m2_relset_1(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0)) ),
inference(resolution,[],[f1587,f504]) ).
fof(f3941,plain,
! [X2,X3,X0,X1] :
( m1_relset_1(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| g3_lattices(u1_struct_0(X0),u1_lattices(X0),u2_lattices(X0)) != g3_lattices(X1,X2,X3)
| u1_lattices(X0) = X2
| l1_lattices(X0)
| l2_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f3940,f438]) ).
fof(f3950,plain,
! [X0] :
( k14_filter_2(sK0,sK27(k1_lattice2(sK0),X0)) = k7_filter_2(sK0,k14_filter_2(sK0,sK27(k1_lattice2(sK0),X0)))
| v13_lattices(k1_lattice2(sK0))
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK0)))
| ~ v10_lattices(sK0)
| v3_struct_0(sK0)
| l3_lattices(sK0)
| k5_lattices(k1_lattice2(sK0)) = X0 ),
inference(resolution,[],[f1642,f1510]) ).
fof(f3951,plain,
( ! [X0] :
( k14_filter_2(sK0,sK27(k1_lattice2(sK0),X0)) = k7_filter_2(sK0,k14_filter_2(sK0,sK27(k1_lattice2(sK0),X0)))
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK0)))
| ~ v10_lattices(sK0)
| v3_struct_0(sK0)
| l3_lattices(sK0)
| k5_lattices(k1_lattice2(sK0)) = X0 )
| spl28_41 ),
inference(forward_subsumption_resolution,[],[f3950,f1013]) ).
fof(f3956,plain,
( ! [X0] :
( k14_filter_2(sK0,sK27(k1_lattice2(sK0),X0)) = k7_filter_2(sK0,k14_filter_2(sK0,sK27(k1_lattice2(sK0),X0)))
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK0)))
| v3_struct_0(sK0)
| l3_lattices(sK0)
| k5_lattices(k1_lattice2(sK0)) = X0 )
| spl28_41 ),
inference(forward_subsumption_resolution,[],[f3951,f231]) ).
fof(f3961,plain,
( ! [X0] :
( k14_filter_2(sK0,sK27(k1_lattice2(sK0),X0)) = k7_filter_2(sK0,k14_filter_2(sK0,sK27(k1_lattice2(sK0),X0)))
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK0)))
| l3_lattices(sK0)
| k5_lattices(k1_lattice2(sK0)) = X0 )
| spl28_41 ),
inference(forward_subsumption_resolution,[],[f3956,f232]) ).
fof(f3966,plain,
( ! [X0] :
( k14_filter_2(sK0,sK27(k1_lattice2(sK0),X0)) = k7_filter_2(sK0,k14_filter_2(sK0,sK27(k1_lattice2(sK0),X0)))
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK0)))
| k5_lattices(k1_lattice2(sK0)) = X0 )
| spl28_41 ),
inference(forward_subsumption_resolution,[],[f3961,f395]) ).
fof(f3968,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK0)))
| k14_filter_2(sK0,sK27(k1_lattice2(sK0),X0)) = k7_filter_2(sK0,k14_filter_2(sK0,sK27(k1_lattice2(sK0),X0)))
| k6_lattices(sK0) = X0 )
| spl28_41 ),
inference(forward_demodulation,[],[f3966,f630]) ).
fof(f4302,plain,
( sK1 = k5_filter_2(k1_lattice2(sK0),sK1)
| ~ spl28_38 ),
inference(resolution,[],[f999,f841]) ).
fof(f4311,definition,
( spl28_276
<=> l2_lattices(k1_lattice2(sK0)) ),
introduced(definition,[new_symbols(definition,[spl28_276])],[avatar_definition]) ).
fof(f4312,plain,
( ~ l2_lattices(k1_lattice2(sK0))
| spl28_276 ),
inference(avatar_component_clause,[],[f4311]) ).
fof(f4313,plain,
( l2_lattices(k1_lattice2(sK0))
| ~ spl28_276 ),
inference(avatar_component_clause,[],[f4311]) ).
fof(f4339,plain,
( l3_lattices(k1_lattice2(sK0))
| ~ spl28_276 ),
inference(resolution,[],[f4313,f428]) ).
fof(f4340,plain,
( $false
| spl28_27
| ~ spl28_276 ),
inference(forward_subsumption_resolution,[],[f4339,f922]) ).
fof(f4341,plain,
( spl28_27
| ~ spl28_276 ),
inference(avatar_contradiction_clause,[],[f4340]) ).
fof(f5388,plain,
( sK27(k1_lattice2(sK0),sK1) = k8_filter_2(sK0,sK27(k1_lattice2(sK0),sK1))
| sK1 = k6_lattices(sK0)
| ~ spl28_29
| spl28_41 ),
inference(resolution,[],[f1708,f841]) ).
fof(f5409,plain,
( sK27(k1_lattice2(sK0),sK1) = k8_filter_2(sK0,sK27(k1_lattice2(sK0),sK1))
| ~ spl28_29
| spl28_41 ),
inference(forward_subsumption_resolution,[],[f5388,f228]) ).
fof(f5464,plain,
( m1_subset_1(sK1,u1_struct_0(k1_lattice2(k1_lattice2(sK0))))
| l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(k1_lattice2(sK0)))
| ~ spl28_38 ),
inference(superposition,[],[f420,f4302]) ).
fof(f5465,plain,
( m1_subset_1(sK1,u1_struct_0(k1_lattice2(k1_lattice2(sK0))))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(k1_lattice2(sK0)))
| spl28_27
| ~ spl28_38 ),
inference(forward_subsumption_resolution,[],[f5464,f922]) ).
fof(f5466,plain,
( m1_subset_1(sK1,u1_struct_0(k1_lattice2(k1_lattice2(sK0))))
| v3_struct_0(k1_lattice2(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(k1_lattice2(sK0)))
| ~ spl28_26
| spl28_27
| ~ spl28_38 ),
inference(forward_subsumption_resolution,[],[f5465,f918]) ).
fof(f5467,plain,
( m1_subset_1(sK1,u1_struct_0(k1_lattice2(k1_lattice2(sK0))))
| ~ m1_subset_1(sK1,u1_struct_0(k1_lattice2(sK0)))
| spl28_5
| ~ spl28_26
| spl28_27
| ~ spl28_38 ),
inference(forward_subsumption_resolution,[],[f5466,f650]) ).
fof(f5468,plain,
( m1_subset_1(sK1,u1_struct_0(k1_lattice2(k1_lattice2(sK0))))
| spl28_5
| ~ spl28_26
| spl28_27
| ~ spl28_38 ),
inference(forward_subsumption_resolution,[],[f5467,f841]) ).
fof(f5613,plain,
( sK1 = k6_lattices(sK0)
| k8_filter_2(sK0,sK27(k1_lattice2(sK0),sK1)) = k14_filter_2(sK0,sK27(k1_lattice2(sK0),sK1))
| spl28_41 ),
inference(resolution,[],[f3898,f841]) ).
fof(f5618,plain,
( k8_filter_2(sK0,sK27(k1_lattice2(sK0),sK1)) = k14_filter_2(sK0,sK27(k1_lattice2(sK0),sK1))
| spl28_41 ),
inference(forward_subsumption_resolution,[],[f5613,f228]) ).
fof(f13806,plain,
! [X0] :
( k5_filter_2(k1_lattice2(sK0),X0) = k5_filter_2(k1_lattice2(k1_lattice2(sK0)),k5_filter_2(k1_lattice2(sK0),X0))
| v3_struct_0(sK0)
| l3_lattices(sK0)
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK0))) ),
inference(resolution,[],[f3531,f231]) ).
fof(f13811,plain,
! [X0] :
( k5_filter_2(k1_lattice2(sK0),X0) = k5_filter_2(k1_lattice2(k1_lattice2(sK0)),k5_filter_2(k1_lattice2(sK0),X0))
| l3_lattices(sK0)
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK0))) ),
inference(forward_subsumption_resolution,[],[f13806,f232]) ).
fof(f13822,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK0)))
| k5_filter_2(k1_lattice2(sK0),X0) = k5_filter_2(k1_lattice2(k1_lattice2(sK0)),k5_filter_2(k1_lattice2(sK0),X0)) ),
inference(forward_subsumption_resolution,[],[f13811,f395]) ).
fof(f14333,plain,
! [X2,X3,X0,X1] :
( g3_lattices(u1_struct_0(X0),u1_lattices(X0),u2_lattices(X0)) != g3_lattices(X1,X2,X3)
| u2_lattices(X0) = X3
| l1_lattices(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(resolution,[],[f3932,f504]) ).
fof(f14334,plain,
! [X2,X3,X0,X1] :
( l2_lattices(X0)
| u2_lattices(X0) = X3
| l1_lattices(X0)
| g3_lattices(u1_struct_0(X0),u1_lattices(X0),u2_lattices(X0)) != g3_lattices(X1,X2,X3) ),
inference(forward_subsumption_resolution,[],[f14333,f441]) ).
fof(f14337,plain,
! [X2,X3,X0,X1] :
( g3_lattices(u1_struct_0(X0),u1_lattices(X0),u2_lattices(X0)) != g3_lattices(X1,X2,X3)
| u1_struct_0(X0) = X1
| l1_lattices(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(resolution,[],[f3936,f504]) ).
fof(f14338,plain,
! [X2,X3,X0,X1] :
( l2_lattices(X0)
| u1_struct_0(X0) = X1
| l1_lattices(X0)
| g3_lattices(u1_struct_0(X0),u1_lattices(X0),u2_lattices(X0)) != g3_lattices(X1,X2,X3) ),
inference(forward_subsumption_resolution,[],[f14337,f441]) ).
fof(f14341,plain,
! [X2,X3,X0,X1] :
( g3_lattices(u1_struct_0(X0),u1_lattices(X0),u2_lattices(X0)) != g3_lattices(X1,X2,X3)
| u1_lattices(X0) = X2
| l1_lattices(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(resolution,[],[f3941,f504]) ).
fof(f14342,plain,
! [X2,X3,X0,X1] :
( l2_lattices(X0)
| u1_lattices(X0) = X2
| l1_lattices(X0)
| g3_lattices(u1_struct_0(X0),u1_lattices(X0),u2_lattices(X0)) != g3_lattices(X1,X2,X3) ),
inference(forward_subsumption_resolution,[],[f14341,f441]) ).
fof(f14363,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK0)))
| v13_lattices(k1_lattice2(sK0))
| v3_struct_0(sK0)
| l3_lattices(sK0)
| k5_lattices(k1_lattice2(sK0)) = X0
| k7_filter_2(sK0,k14_filter_2(sK0,sK27(k1_lattice2(sK0),X0))) = k15_filter_2(sK0,k14_filter_2(sK0,sK27(k1_lattice2(sK0),X0))) ),
inference(resolution,[],[f3824,f231]) ).
fof(f14367,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK0)))
| v3_struct_0(sK0)
| l3_lattices(sK0)
| k5_lattices(k1_lattice2(sK0)) = X0
| k7_filter_2(sK0,k14_filter_2(sK0,sK27(k1_lattice2(sK0),X0))) = k15_filter_2(sK0,k14_filter_2(sK0,sK27(k1_lattice2(sK0),X0))) )
| spl28_41 ),
inference(forward_subsumption_resolution,[],[f14363,f1013]) ).
fof(f14373,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK0)))
| l3_lattices(sK0)
| k5_lattices(k1_lattice2(sK0)) = X0
| k7_filter_2(sK0,k14_filter_2(sK0,sK27(k1_lattice2(sK0),X0))) = k15_filter_2(sK0,k14_filter_2(sK0,sK27(k1_lattice2(sK0),X0))) )
| spl28_41 ),
inference(forward_subsumption_resolution,[],[f14367,f232]) ).
fof(f14379,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK0)))
| k5_lattices(k1_lattice2(sK0)) = X0
| k7_filter_2(sK0,k14_filter_2(sK0,sK27(k1_lattice2(sK0),X0))) = k15_filter_2(sK0,k14_filter_2(sK0,sK27(k1_lattice2(sK0),X0))) )
| spl28_41 ),
inference(forward_subsumption_resolution,[],[f14373,f395]) ).
fof(f14390,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK0)))
| k6_lattices(sK0) = X0
| k7_filter_2(sK0,k14_filter_2(sK0,sK27(k1_lattice2(sK0),X0))) = k15_filter_2(sK0,k14_filter_2(sK0,sK27(k1_lattice2(sK0),X0))) )
| spl28_41 ),
inference(forward_demodulation,[],[f14379,f630]) ).
fof(f17655,plain,
( sK27(k1_lattice2(sK0),sK1) = k14_filter_2(sK0,sK27(k1_lattice2(sK0),sK1))
| ~ spl28_29
| spl28_41 ),
inference(forward_demodulation,[],[f5618,f5409]) ).
fof(f17657,plain,
( ~ m2_filter_2(sK27(k1_lattice2(sK0),sK1),sK0)
| v13_lattices(k1_lattice2(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(k1_lattice2(sK0)))
| ~ v10_lattices(sK0)
| v3_struct_0(sK0)
| l3_lattices(sK0)
| sK1 = k5_lattices(k1_lattice2(sK0))
| ~ spl28_29
| spl28_41 ),
inference(superposition,[],[f1510,f17655]) ).
fof(f17658,plain,
( ~ m2_filter_2(sK27(k1_lattice2(sK0),sK1),sK0)
| ~ m1_subset_1(sK1,u1_struct_0(k1_lattice2(sK0)))
| ~ v10_lattices(sK0)
| v3_struct_0(sK0)
| l3_lattices(sK0)
| sK1 = k5_lattices(k1_lattice2(sK0))
| ~ spl28_29
| spl28_41 ),
inference(forward_subsumption_resolution,[],[f17657,f1013]) ).
fof(f17659,plain,
( ~ m2_filter_2(sK27(k1_lattice2(sK0),sK1),sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0)
| l3_lattices(sK0)
| sK1 = k5_lattices(k1_lattice2(sK0))
| ~ spl28_29
| spl28_41 ),
inference(forward_subsumption_resolution,[],[f17658,f841]) ).
fof(f17660,plain,
( ~ m2_filter_2(sK27(k1_lattice2(sK0),sK1),sK0)
| v3_struct_0(sK0)
| l3_lattices(sK0)
| sK1 = k5_lattices(k1_lattice2(sK0))
| ~ spl28_29
| spl28_41 ),
inference(forward_subsumption_resolution,[],[f17659,f231]) ).
fof(f17661,plain,
( ~ m2_filter_2(sK27(k1_lattice2(sK0),sK1),sK0)
| l3_lattices(sK0)
| sK1 = k5_lattices(k1_lattice2(sK0))
| ~ spl28_29
| spl28_41 ),
inference(forward_subsumption_resolution,[],[f17660,f232]) ).
fof(f17662,plain,
( ~ m2_filter_2(sK27(k1_lattice2(sK0),sK1),sK0)
| sK1 = k5_lattices(k1_lattice2(sK0))
| ~ spl28_29
| spl28_41 ),
inference(forward_subsumption_resolution,[],[f17661,f395]) ).
fof(f17663,plain,
( sK1 = k6_lattices(sK0)
| ~ m2_filter_2(sK27(k1_lattice2(sK0),sK1),sK0)
| ~ spl28_29
| spl28_41 ),
inference(forward_demodulation,[],[f17662,f630]) ).
fof(f17664,plain,
( ~ m2_filter_2(sK27(k1_lattice2(sK0),sK1),sK0)
| ~ spl28_29
| spl28_41 ),
inference(forward_subsumption_resolution,[],[f17663,f228]) ).
fof(f21798,definition,
( spl28_1672
<=> u2_lattices(sK0) = u1_lattices(k1_lattice2(sK0)) ),
introduced(definition,[new_symbols(definition,[spl28_1672])],[avatar_definition]) ).
fof(f21800,plain,
( u2_lattices(sK0) = u1_lattices(k1_lattice2(sK0))
| ~ spl28_1672 ),
inference(avatar_component_clause,[],[f21798]) ).
fof(f21877,definition,
( spl28_1689
<=> u2_lattices(sK0) = u2_lattices(k1_lattice2(k1_lattice2(sK0))) ),
introduced(definition,[new_symbols(definition,[spl28_1689])],[avatar_definition]) ).
fof(f21879,plain,
( u2_lattices(sK0) = u2_lattices(k1_lattice2(k1_lattice2(sK0)))
| ~ spl28_1689 ),
inference(avatar_component_clause,[],[f21877]) ).
fof(f22092,definition,
( spl28_1728
<=> u1_lattices(sK0) = u2_lattices(k1_lattice2(sK0)) ),
introduced(definition,[new_symbols(definition,[spl28_1728])],[avatar_definition]) ).
fof(f22094,plain,
( u1_lattices(sK0) = u2_lattices(k1_lattice2(sK0))
| ~ spl28_1728 ),
inference(avatar_component_clause,[],[f22092]) ).
fof(f22189,definition,
( spl28_1749
<=> u1_lattices(sK0) = u1_lattices(k1_lattice2(k1_lattice2(sK0))) ),
introduced(definition,[new_symbols(definition,[spl28_1749])],[avatar_definition]) ).
fof(f22191,plain,
( u1_lattices(sK0) = u1_lattices(k1_lattice2(k1_lattice2(sK0)))
| ~ spl28_1749 ),
inference(avatar_component_clause,[],[f22189]) ).
fof(f22319,definition,
( spl28_1767
<=> u1_struct_0(sK0) = u1_struct_0(k1_lattice2(sK0)) ),
introduced(definition,[new_symbols(definition,[spl28_1767])],[avatar_definition]) ).
fof(f22321,plain,
( u1_struct_0(sK0) = u1_struct_0(k1_lattice2(sK0))
| ~ spl28_1767 ),
inference(avatar_component_clause,[],[f22319]) ).
fof(f22355,definition,
( spl28_1773
<=> u1_struct_0(sK0) = u1_struct_0(k1_lattice2(k1_lattice2(sK0))) ),
introduced(definition,[new_symbols(definition,[spl28_1773])],[avatar_definition]) ).
fof(f22357,plain,
( u1_struct_0(sK0) = u1_struct_0(k1_lattice2(k1_lattice2(sK0)))
| ~ spl28_1773 ),
inference(avatar_component_clause,[],[f22355]) ).
fof(f25014,plain,
k5_filter_2(k1_lattice2(sK0),sK1) = k5_filter_2(k1_lattice2(k1_lattice2(sK0)),k5_filter_2(k1_lattice2(sK0),sK1)),
inference(resolution,[],[f13822,f841]) ).
fof(f25045,plain,
( sK1 = k5_filter_2(k1_lattice2(k1_lattice2(sK0)),sK1)
| ~ spl28_38 ),
inference(forward_demodulation,[],[f25014,f4302]) ).
fof(f28438,plain,
( k14_filter_2(sK0,sK27(k1_lattice2(sK0),sK1)) = k7_filter_2(sK0,k14_filter_2(sK0,sK27(k1_lattice2(sK0),sK1)))
| sK1 = k6_lattices(sK0)
| spl28_41 ),
inference(resolution,[],[f3968,f841]) ).
fof(f28475,plain,
( k14_filter_2(sK0,sK27(k1_lattice2(sK0),sK1)) = k7_filter_2(sK0,k14_filter_2(sK0,sK27(k1_lattice2(sK0),sK1)))
| spl28_41 ),
inference(forward_subsumption_resolution,[],[f28438,f228]) ).
fof(f28490,plain,
( sK27(k1_lattice2(sK0),sK1) = k7_filter_2(sK0,sK27(k1_lattice2(sK0),sK1))
| ~ spl28_29
| spl28_41 ),
inference(forward_demodulation,[],[f28475,f17655]) ).
fof(f29955,plain,
( sK1 = k6_lattices(sK0)
| k7_filter_2(sK0,k14_filter_2(sK0,sK27(k1_lattice2(sK0),sK1))) = k15_filter_2(sK0,k14_filter_2(sK0,sK27(k1_lattice2(sK0),sK1)))
| spl28_41 ),
inference(resolution,[],[f14390,f841]) ).
fof(f29988,plain,
( k7_filter_2(sK0,k14_filter_2(sK0,sK27(k1_lattice2(sK0),sK1))) = k15_filter_2(sK0,k14_filter_2(sK0,sK27(k1_lattice2(sK0),sK1)))
| spl28_41 ),
inference(forward_subsumption_resolution,[],[f29955,f228]) ).
fof(f30003,plain,
( k7_filter_2(sK0,sK27(k1_lattice2(sK0),sK1)) = k15_filter_2(sK0,sK27(k1_lattice2(sK0),sK1))
| ~ spl28_29
| spl28_41 ),
inference(forward_demodulation,[],[f29988,f17655]) ).
fof(f33474,plain,
( r2_hidden(sK1,sK27(k1_lattice2(k1_lattice2(k1_lattice2(sK0))),sK1))
| sK1 = k5_lattices(k1_lattice2(k1_lattice2(k1_lattice2(sK0))))
| v13_lattices(k1_lattice2(k1_lattice2(k1_lattice2(sK0))))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0))
| l3_lattices(k1_lattice2(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(k1_lattice2(k1_lattice2(sK0))))
| ~ spl28_38 ),
inference(superposition,[],[f3865,f25045]) ).
fof(f82558,plain,
( ! [X2,X0,X1] :
( u2_lattices(k1_lattice2(sK0)) = X0
| l1_lattices(k1_lattice2(sK0))
| g3_lattices(u1_struct_0(k1_lattice2(sK0)),u1_lattices(k1_lattice2(sK0)),u2_lattices(k1_lattice2(sK0))) != g3_lattices(X1,X2,X0) )
| spl28_276 ),
inference(resolution,[],[f14334,f4312]) ).
fof(f82561,plain,
( ! [X2,X0,X1] :
( u2_lattices(sK0) = X0
| l1_lattices(sK0)
| g3_lattices(u1_struct_0(sK0),u1_lattices(sK0),u2_lattices(sK0)) != g3_lattices(X1,X2,X0) )
| spl28_12 ),
inference(resolution,[],[f14334,f734]) ).
fof(f82571,plain,
( ! [X2,X0,X1] :
( u2_lattices(sK0) = X0
| g3_lattices(u1_struct_0(sK0),u1_lattices(sK0),u2_lattices(sK0)) != g3_lattices(X1,X2,X0) )
| spl28_10
| spl28_12 ),
inference(forward_subsumption_resolution,[],[f82561,f725]) ).
fof(f82574,plain,
( ! [X2,X0,X1] :
( u2_lattices(k1_lattice2(sK0)) = X0
| g3_lattices(u1_struct_0(k1_lattice2(sK0)),u1_lattices(k1_lattice2(sK0)),u2_lattices(k1_lattice2(sK0))) != g3_lattices(X1,X2,X0) )
| spl28_4
| spl28_276 ),
inference(forward_subsumption_resolution,[],[f82558,f646]) ).
fof(f82581,plain,
( ! [X2,X0,X1] :
( k1_lattice2(sK0) != g3_lattices(X1,X2,X0)
| u2_lattices(sK0) = X0 )
| spl28_10
| spl28_12 ),
inference(forward_demodulation,[],[f82571,f592]) ).
fof(f82584,plain,
( ! [X2,X0,X1] :
( k1_lattice2(k1_lattice2(sK0)) != g3_lattices(X1,X2,X0)
| u2_lattices(k1_lattice2(sK0)) = X0 )
| spl28_4
| spl28_276 ),
inference(forward_demodulation,[],[f82574,f1372]) ).
fof(f82634,plain,
( ! [X2,X0,X1] :
( u1_struct_0(k1_lattice2(sK0)) = X0
| l1_lattices(k1_lattice2(sK0))
| g3_lattices(X0,X1,X2) != g3_lattices(u1_struct_0(k1_lattice2(sK0)),u1_lattices(k1_lattice2(sK0)),u2_lattices(k1_lattice2(sK0))) )
| spl28_276 ),
inference(resolution,[],[f14338,f4312]) ).
fof(f82637,plain,
( ! [X2,X0,X1] :
( u1_struct_0(sK0) = X0
| l1_lattices(sK0)
| g3_lattices(X0,X1,X2) != g3_lattices(u1_struct_0(sK0),u1_lattices(sK0),u2_lattices(sK0)) )
| spl28_12 ),
inference(resolution,[],[f14338,f734]) ).
fof(f82647,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_12 ),
inference(forward_subsumption_resolution,[],[f82637,f725]) ).
fof(f82650,plain,
( ! [X2,X0,X1] :
( u1_struct_0(k1_lattice2(sK0)) = X0
| g3_lattices(X0,X1,X2) != g3_lattices(u1_struct_0(k1_lattice2(sK0)),u1_lattices(k1_lattice2(sK0)),u2_lattices(k1_lattice2(sK0))) )
| spl28_4
| spl28_276 ),
inference(forward_subsumption_resolution,[],[f82634,f646]) ).
fof(f82657,plain,
( ! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != k1_lattice2(sK0)
| u1_struct_0(sK0) = X0 )
| spl28_10
| spl28_12 ),
inference(forward_demodulation,[],[f82647,f592]) ).
fof(f82660,plain,
( ! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != k1_lattice2(k1_lattice2(sK0))
| u1_struct_0(k1_lattice2(sK0)) = X0 )
| spl28_4
| spl28_276 ),
inference(forward_demodulation,[],[f82650,f1372]) ).
fof(f82716,plain,
( ! [X2,X0,X1] :
( u1_lattices(k1_lattice2(sK0)) = X0
| l1_lattices(k1_lattice2(sK0))
| g3_lattices(u1_struct_0(k1_lattice2(sK0)),u1_lattices(k1_lattice2(sK0)),u2_lattices(k1_lattice2(sK0))) != g3_lattices(X1,X0,X2) )
| spl28_276 ),
inference(resolution,[],[f14342,f4312]) ).
fof(f82719,plain,
( ! [X2,X0,X1] :
( u1_lattices(sK0) = X0
| l1_lattices(sK0)
| g3_lattices(u1_struct_0(sK0),u1_lattices(sK0),u2_lattices(sK0)) != g3_lattices(X1,X0,X2) )
| spl28_12 ),
inference(resolution,[],[f14342,f734]) ).
fof(f82729,plain,
( ! [X2,X0,X1] :
( u1_lattices(sK0) = X0
| g3_lattices(u1_struct_0(sK0),u1_lattices(sK0),u2_lattices(sK0)) != g3_lattices(X1,X0,X2) )
| spl28_10
| spl28_12 ),
inference(forward_subsumption_resolution,[],[f82719,f725]) ).
fof(f82732,plain,
( ! [X2,X0,X1] :
( u1_lattices(k1_lattice2(sK0)) = X0
| g3_lattices(u1_struct_0(k1_lattice2(sK0)),u1_lattices(k1_lattice2(sK0)),u2_lattices(k1_lattice2(sK0))) != g3_lattices(X1,X0,X2) )
| spl28_4
| spl28_276 ),
inference(forward_subsumption_resolution,[],[f82716,f646]) ).
fof(f82739,plain,
( ! [X2,X0,X1] :
( k1_lattice2(sK0) != g3_lattices(X1,X0,X2)
| u1_lattices(sK0) = X0 )
| spl28_10
| spl28_12 ),
inference(forward_demodulation,[],[f82729,f592]) ).
fof(f82742,plain,
( ! [X2,X0,X1] :
( k1_lattice2(k1_lattice2(sK0)) != g3_lattices(X1,X0,X2)
| u1_lattices(k1_lattice2(sK0)) = X0 )
| spl28_4
| spl28_276 ),
inference(forward_demodulation,[],[f82732,f1372]) ).
fof(f143001,plain,
( k1_lattice2(sK0) != k1_lattice2(sK0)
| u2_lattices(sK0) = u1_lattices(k1_lattice2(sK0))
| spl28_10
| spl28_12 ),
inference(superposition,[],[f82581,f1337]) ).
fof(f143022,plain,
( u2_lattices(sK0) = u1_lattices(k1_lattice2(sK0))
| spl28_10
| spl28_12 ),
inference(trivial_inequality_removal,[],[f143001]) ).
fof(f143103,plain,
( spl28_1672
| spl28_10
| spl28_12 ),
inference(avatar_split_clause,[],[f143022,f733,f724,f21798]) ).
fof(f143135,definition,
( spl28_12194
<=> k1_lattice2(sK0) = k1_lattice2(k1_lattice2(k1_lattice2(sK0))) ),
introduced(definition,[new_symbols(definition,[spl28_12194])],[avatar_definition]) ).
fof(f143136,plain,
( k1_lattice2(sK0) = k1_lattice2(k1_lattice2(k1_lattice2(sK0)))
| ~ spl28_12194 ),
inference(avatar_component_clause,[],[f143135]) ).
fof(f143485,plain,
( k1_lattice2(sK0) != k1_lattice2(sK0)
| u1_struct_0(sK0) = u1_struct_0(k1_lattice2(sK0))
| spl28_10
| spl28_12 ),
inference(superposition,[],[f82657,f1337]) ).
fof(f143506,plain,
( u1_struct_0(sK0) = u1_struct_0(k1_lattice2(sK0))
| spl28_10
| spl28_12 ),
inference(trivial_inequality_removal,[],[f143485]) ).
fof(f143527,plain,
( spl28_1767
| spl28_10
| spl28_12 ),
inference(avatar_split_clause,[],[f143506,f733,f724,f22319]) ).
fof(f155364,plain,
( k1_lattice2(sK0) != k1_lattice2(sK0)
| u1_lattices(sK0) = u2_lattices(k1_lattice2(sK0))
| spl28_10
| spl28_12 ),
inference(superposition,[],[f82739,f1337]) ).
fof(f155385,plain,
( u1_lattices(sK0) = u2_lattices(k1_lattice2(sK0))
| spl28_10
| spl28_12 ),
inference(trivial_inequality_removal,[],[f155364]) ).
fof(f155614,plain,
( spl28_1728
| spl28_10
| spl28_12 ),
inference(avatar_split_clause,[],[f155385,f733,f724,f22092]) ).
fof(f173317,plain,
( sK27(k1_lattice2(sK0),sK1) = k15_filter_2(sK0,sK27(k1_lattice2(sK0),sK1))
| ~ spl28_29
| spl28_41 ),
inference(forward_demodulation,[],[f30003,f28490]) ).
fof(f173330,plain,
( ~ v1_filter_0(sK27(k1_lattice2(sK0),sK1),k1_lattice2(sK0))
| ~ v10_lattices(sK0)
| v3_struct_0(sK0)
| m2_filter_2(sK27(k1_lattice2(sK0),sK1),sK0)
| l3_lattices(sK0)
| r2_filter_2(sK0,sK27(k1_lattice2(sK0),sK1))
| ~ spl28_29
| spl28_41 ),
inference(superposition,[],[f511,f173317]) ).
fof(f173338,plain,
( ~ v1_filter_0(sK27(k1_lattice2(sK0),sK1),k1_lattice2(sK0))
| v3_struct_0(sK0)
| m2_filter_2(sK27(k1_lattice2(sK0),sK1),sK0)
| l3_lattices(sK0)
| r2_filter_2(sK0,sK27(k1_lattice2(sK0),sK1))
| ~ spl28_29
| spl28_41 ),
inference(forward_subsumption_resolution,[],[f173330,f231]) ).
fof(f173354,plain,
( ~ v1_filter_0(sK27(k1_lattice2(sK0),sK1),k1_lattice2(sK0))
| m2_filter_2(sK27(k1_lattice2(sK0),sK1),sK0)
| l3_lattices(sK0)
| r2_filter_2(sK0,sK27(k1_lattice2(sK0),sK1))
| ~ spl28_29
| spl28_41 ),
inference(forward_subsumption_resolution,[],[f173338,f232]) ).
fof(f173368,plain,
( ~ v1_filter_0(sK27(k1_lattice2(sK0),sK1),k1_lattice2(sK0))
| l3_lattices(sK0)
| r2_filter_2(sK0,sK27(k1_lattice2(sK0),sK1))
| ~ spl28_29
| spl28_41 ),
inference(forward_subsumption_resolution,[],[f173354,f17664]) ).
fof(f173375,plain,
( ~ v1_filter_0(sK27(k1_lattice2(sK0),sK1),k1_lattice2(sK0))
| r2_filter_2(sK0,sK27(k1_lattice2(sK0),sK1))
| ~ spl28_29
| spl28_41 ),
inference(forward_subsumption_resolution,[],[f173368,f395]) ).
fof(f173381,definition,
( spl28_13929
<=> r2_filter_2(sK0,sK27(k1_lattice2(sK0),sK1)) ),
introduced(definition,[new_symbols(definition,[spl28_13929])],[avatar_definition]) ).
fof(f173383,plain,
( r2_filter_2(sK0,sK27(k1_lattice2(sK0),sK1))
| ~ spl28_13929 ),
inference(avatar_component_clause,[],[f173381]) ).
fof(f173385,definition,
( spl28_13930
<=> v1_filter_0(sK27(k1_lattice2(sK0),sK1),k1_lattice2(sK0)) ),
introduced(definition,[new_symbols(definition,[spl28_13930])],[avatar_definition]) ).
fof(f173387,plain,
( ~ v1_filter_0(sK27(k1_lattice2(sK0),sK1),k1_lattice2(sK0))
| spl28_13930 ),
inference(avatar_component_clause,[],[f173385]) ).
fof(f173388,plain,
( spl28_13929
| ~ spl28_13930
| ~ spl28_29
| spl28_41 ),
inference(avatar_split_clause,[],[f173375,f1012,f930,f173385,f173381]) ).
fof(f179078,plain,
( ! [X2,X0,X1] :
( k1_lattice2(k1_lattice2(sK0)) != g3_lattices(X1,X2,X0)
| u1_lattices(sK0) = X0 )
| spl28_4
| spl28_276
| ~ spl28_1728 ),
inference(forward_demodulation,[],[f82584,f22094]) ).
fof(f179101,plain,
( k1_lattice2(k1_lattice2(sK0)) != k1_lattice2(k1_lattice2(sK0))
| u1_lattices(sK0) = u1_lattices(k1_lattice2(k1_lattice2(sK0)))
| spl28_4
| spl28_27
| spl28_276
| ~ spl28_1728 ),
inference(superposition,[],[f179078,f1336]) ).
fof(f179136,plain,
( u1_lattices(sK0) = u1_lattices(k1_lattice2(k1_lattice2(sK0)))
| spl28_4
| spl28_27
| spl28_276
| ~ spl28_1728 ),
inference(trivial_inequality_removal,[],[f179101]) ).
fof(f179247,plain,
( spl28_1749
| spl28_4
| spl28_27
| spl28_276
| ~ spl28_1728 ),
inference(avatar_split_clause,[],[f179136,f22092,f4311,f921,f645,f22189]) ).
fof(f179495,plain,
( ! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != k1_lattice2(k1_lattice2(sK0))
| u1_struct_0(sK0) = X0 )
| spl28_4
| spl28_276
| ~ spl28_1767 ),
inference(forward_demodulation,[],[f82660,f22321]) ).
fof(f179518,plain,
( k1_lattice2(k1_lattice2(sK0)) != k1_lattice2(k1_lattice2(sK0))
| u1_struct_0(sK0) = u1_struct_0(k1_lattice2(k1_lattice2(sK0)))
| spl28_4
| spl28_27
| spl28_276
| ~ spl28_1767 ),
inference(superposition,[],[f179495,f1336]) ).
fof(f179552,plain,
( u1_struct_0(sK0) = u1_struct_0(k1_lattice2(k1_lattice2(sK0)))
| spl28_4
| spl28_27
| spl28_276
| ~ spl28_1767 ),
inference(trivial_inequality_removal,[],[f179518]) ).
fof(f179581,plain,
( spl28_1773
| spl28_4
| spl28_27
| spl28_276
| ~ spl28_1767 ),
inference(avatar_split_clause,[],[f179552,f22319,f4311,f921,f645,f22355]) ).
fof(f184969,plain,
( ! [X2,X0,X1] :
( k1_lattice2(k1_lattice2(sK0)) != g3_lattices(X1,X0,X2)
| u2_lattices(sK0) = X0 )
| spl28_4
| spl28_276
| ~ spl28_1672 ),
inference(forward_demodulation,[],[f82742,f21800]) ).
fof(f185588,plain,
( k1_lattice2(k1_lattice2(sK0)) != k1_lattice2(k1_lattice2(sK0))
| u2_lattices(sK0) = u2_lattices(k1_lattice2(k1_lattice2(sK0)))
| spl28_4
| spl28_27
| spl28_276
| ~ spl28_1672 ),
inference(superposition,[],[f184969,f1336]) ).
fof(f185623,plain,
( u2_lattices(sK0) = u2_lattices(k1_lattice2(k1_lattice2(sK0)))
| spl28_4
| spl28_27
| spl28_276
| ~ spl28_1672 ),
inference(trivial_inequality_removal,[],[f185588]) ).
fof(f185650,plain,
( spl28_1689
| spl28_4
| spl28_27
| spl28_276
| ~ spl28_1672 ),
inference(avatar_split_clause,[],[f185623,f21798,f4311,f921,f645,f21877]) ).
fof(f185674,plain,
( k1_lattice2(k1_lattice2(k1_lattice2(sK0))) = g3_lattices(u1_struct_0(k1_lattice2(k1_lattice2(sK0))),u1_lattices(k1_lattice2(k1_lattice2(sK0))),u2_lattices(sK0))
| spl28_27
| ~ spl28_1689 ),
inference(superposition,[],[f1371,f21879]) ).
fof(f185748,plain,
( k1_lattice2(k1_lattice2(k1_lattice2(sK0))) = g3_lattices(u1_struct_0(k1_lattice2(k1_lattice2(sK0))),u1_lattices(sK0),u2_lattices(sK0))
| spl28_27
| ~ spl28_1689
| ~ spl28_1749 ),
inference(forward_demodulation,[],[f185674,f22191]) ).
fof(f185785,plain,
( g3_lattices(u1_struct_0(sK0),u1_lattices(sK0),u2_lattices(sK0)) = k1_lattice2(k1_lattice2(k1_lattice2(sK0)))
| spl28_27
| ~ spl28_1689
| ~ spl28_1749
| ~ spl28_1773 ),
inference(forward_demodulation,[],[f185748,f22357]) ).
fof(f185817,plain,
( k1_lattice2(sK0) = k1_lattice2(k1_lattice2(k1_lattice2(sK0)))
| spl28_27
| ~ spl28_1689
| ~ spl28_1749
| ~ spl28_1773 ),
inference(forward_demodulation,[],[f185785,f592]) ).
fof(f186100,plain,
( spl28_12194
| spl28_27
| ~ spl28_1689
| ~ spl28_1749
| ~ spl28_1773 ),
inference(avatar_split_clause,[],[f185817,f22355,f22189,f21877,f921,f143135]) ).
fof(f191533,plain,
( r2_hidden(sK1,sK27(k1_lattice2(k1_lattice2(k1_lattice2(sK0))),sK1))
| sK1 = k5_lattices(k1_lattice2(k1_lattice2(k1_lattice2(sK0))))
| v13_lattices(k1_lattice2(k1_lattice2(k1_lattice2(sK0))))
| v3_struct_0(k1_lattice2(sK0))
| l3_lattices(k1_lattice2(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(k1_lattice2(k1_lattice2(sK0))))
| ~ spl28_26
| ~ spl28_38 ),
inference(forward_subsumption_resolution,[],[f33474,f918]) ).
fof(f191646,plain,
( r2_hidden(sK1,sK27(k1_lattice2(k1_lattice2(k1_lattice2(sK0))),sK1))
| sK1 = k5_lattices(k1_lattice2(k1_lattice2(k1_lattice2(sK0))))
| v13_lattices(k1_lattice2(k1_lattice2(k1_lattice2(sK0))))
| l3_lattices(k1_lattice2(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(k1_lattice2(k1_lattice2(sK0))))
| spl28_5
| ~ spl28_26
| ~ spl28_38 ),
inference(forward_subsumption_resolution,[],[f191533,f650]) ).
fof(f191755,plain,
( r2_hidden(sK1,sK27(k1_lattice2(k1_lattice2(k1_lattice2(sK0))),sK1))
| sK1 = k5_lattices(k1_lattice2(k1_lattice2(k1_lattice2(sK0))))
| v13_lattices(k1_lattice2(k1_lattice2(k1_lattice2(sK0))))
| ~ m1_subset_1(sK1,u1_struct_0(k1_lattice2(k1_lattice2(sK0))))
| spl28_5
| ~ spl28_26
| spl28_27
| ~ spl28_38 ),
inference(forward_subsumption_resolution,[],[f191646,f922]) ).
fof(f191857,plain,
( r2_hidden(sK1,sK27(k1_lattice2(k1_lattice2(k1_lattice2(sK0))),sK1))
| sK1 = k5_lattices(k1_lattice2(k1_lattice2(k1_lattice2(sK0))))
| v13_lattices(k1_lattice2(k1_lattice2(k1_lattice2(sK0))))
| spl28_5
| ~ spl28_26
| spl28_27
| ~ spl28_38 ),
inference(forward_subsumption_resolution,[],[f191755,f5468]) ).
fof(f191950,plain,
( r2_hidden(sK1,sK27(k1_lattice2(sK0),sK1))
| sK1 = k5_lattices(k1_lattice2(k1_lattice2(k1_lattice2(sK0))))
| v13_lattices(k1_lattice2(k1_lattice2(k1_lattice2(sK0))))
| spl28_5
| ~ spl28_26
| spl28_27
| ~ spl28_38
| ~ spl28_12194 ),
inference(forward_demodulation,[],[f191857,f143136]) ).
fof(f192035,plain,
( sK1 = k5_lattices(k1_lattice2(sK0))
| r2_hidden(sK1,sK27(k1_lattice2(sK0),sK1))
| v13_lattices(k1_lattice2(k1_lattice2(k1_lattice2(sK0))))
| spl28_5
| ~ spl28_26
| spl28_27
| ~ spl28_38
| ~ spl28_12194 ),
inference(forward_demodulation,[],[f191950,f143136]) ).
fof(f192115,plain,
( sK1 = k6_lattices(sK0)
| r2_hidden(sK1,sK27(k1_lattice2(sK0),sK1))
| v13_lattices(k1_lattice2(k1_lattice2(k1_lattice2(sK0))))
| spl28_5
| ~ spl28_26
| spl28_27
| ~ spl28_38
| ~ spl28_12194 ),
inference(forward_demodulation,[],[f192035,f630]) ).
fof(f192193,plain,
( r2_hidden(sK1,sK27(k1_lattice2(sK0),sK1))
| v13_lattices(k1_lattice2(k1_lattice2(k1_lattice2(sK0))))
| spl28_5
| ~ spl28_26
| spl28_27
| ~ spl28_38
| ~ spl28_12194 ),
inference(forward_subsumption_resolution,[],[f192115,f228]) ).
fof(f192267,plain,
( v13_lattices(k1_lattice2(sK0))
| r2_hidden(sK1,sK27(k1_lattice2(sK0),sK1))
| spl28_5
| ~ spl28_26
| spl28_27
| ~ spl28_38
| ~ spl28_12194 ),
inference(forward_demodulation,[],[f192193,f143136]) ).
fof(f192335,plain,
( r2_hidden(sK1,sK27(k1_lattice2(sK0),sK1))
| spl28_5
| ~ spl28_26
| spl28_27
| ~ spl28_38
| spl28_41
| ~ spl28_12194 ),
inference(forward_subsumption_resolution,[],[f192267,f1013]) ).
fof(f235871,plain,
( ~ m1_subset_1(sK1,u1_struct_0(k1_lattice2(sK0)))
| sK1 = k5_lattices(k1_lattice2(sK0))
| l3_lattices(k1_lattice2(sK0))
| v13_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0))
| spl28_13930 ),
inference(resolution,[],[f173387,f508]) ).
fof(f235872,plain,
( sK1 = k5_lattices(k1_lattice2(sK0))
| l3_lattices(k1_lattice2(sK0))
| v13_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0))
| spl28_13930 ),
inference(forward_subsumption_resolution,[],[f235871,f841]) ).
fof(f235873,plain,
( sK1 = k5_lattices(k1_lattice2(sK0))
| v13_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0))
| spl28_27
| spl28_13930 ),
inference(forward_subsumption_resolution,[],[f235872,f922]) ).
fof(f235874,plain,
( sK1 = k5_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0))
| spl28_27
| spl28_41
| spl28_13930 ),
inference(forward_subsumption_resolution,[],[f235873,f1013]) ).
fof(f235875,plain,
( sK1 = k5_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0))
| ~ spl28_26
| spl28_27
| spl28_41
| spl28_13930 ),
inference(forward_subsumption_resolution,[],[f235874,f918]) ).
fof(f235876,plain,
( sK1 = k5_lattices(k1_lattice2(sK0))
| spl28_5
| ~ spl28_26
| spl28_27
| spl28_41
| spl28_13930 ),
inference(forward_subsumption_resolution,[],[f235875,f650]) ).
fof(f235878,plain,
( sK1 = k6_lattices(sK0)
| spl28_5
| ~ spl28_26
| spl28_27
| spl28_41
| spl28_13930 ),
inference(superposition,[],[f235876,f630]) ).
fof(f235895,plain,
( $false
| spl28_5
| ~ spl28_26
| spl28_27
| spl28_41
| spl28_13930 ),
inference(forward_subsumption_resolution,[],[f235878,f228]) ).
fof(f235896,plain,
( spl28_5
| ~ spl28_26
| spl28_27
| spl28_41
| spl28_13930 ),
inference(avatar_contradiction_clause,[],[f235895]) ).
fof(f235899,plain,
( m2_filter_2(sK27(k1_lattice2(sK0),sK1),sK0)
| ~ r2_hidden(sK1,sK27(k1_lattice2(sK0),sK1))
| ~ spl28_13929 ),
inference(resolution,[],[f173383,f397]) ).
fof(f235900,plain,
( ~ r2_hidden(sK1,sK27(k1_lattice2(sK0),sK1))
| ~ spl28_29
| spl28_41
| ~ spl28_13929 ),
inference(forward_subsumption_resolution,[],[f235899,f17664]) ).
fof(f235901,plain,
( $false
| spl28_5
| ~ spl28_26
| spl28_27
| ~ spl28_29
| ~ spl28_38
| spl28_41
| ~ spl28_12194
| ~ spl28_13929 ),
inference(forward_subsumption_resolution,[],[f235900,f192335]) ).
fof(f235902,plain,
( spl28_5
| ~ spl28_26
| spl28_27
| ~ spl28_29
| ~ spl28_38
| spl28_41
| ~ spl28_12194
| ~ spl28_13929 ),
inference(avatar_contradiction_clause,[],[f235901]) ).
cnf(s3,plain,
~ spl28_4,
inference(sat_conversion,[],[f664]) ).
cnf(s4,plain,
~ spl28_5,
inference(sat_conversion,[],[f688]) ).
cnf(s8,plain,
~ spl28_10,
inference(sat_conversion,[],[f753]) ).
cnf(s9,plain,
~ spl28_12,
inference(sat_conversion,[],[f762]) ).
cnf(s21,plain,
( spl28_5
| ~ spl28_26
| spl28_27
| spl28_29 ),
inference(sat_conversion,[],[f932]) ).
cnf(s25,plain,
spl28_26,
inference(sat_conversion,[],[f963]) ).
cnf(s35,plain,
~ spl28_27,
inference(sat_conversion,[],[f1048]) ).
cnf(s39,plain,
~ spl28_41,
inference(sat_conversion,[],[f1120]) ).
cnf(s55,plain,
spl28_38,
inference(sat_conversion,[],[f1393]) ).
cnf(s260,plain,
( spl28_27
| ~ spl28_276 ),
inference(sat_conversion,[],[f4341]) ).
cnf(s16871,plain,
( spl28_10
| spl28_12
| spl28_1672 ),
inference(sat_conversion,[],[f143103]) ).
cnf(s16952,plain,
( spl28_10
| spl28_12
| spl28_1767 ),
inference(sat_conversion,[],[f143527]) ).
cnf(s19017,plain,
( spl28_10
| spl28_12
| spl28_1728 ),
inference(sat_conversion,[],[f155614]) ).
cnf(s21194,plain,
( ~ spl28_29
| spl28_41
| spl28_13929
| ~ spl28_13930 ),
inference(sat_conversion,[],[f173388]) ).
cnf(s22209,plain,
( spl28_4
| spl28_27
| spl28_276
| ~ spl28_1728
| spl28_1749 ),
inference(sat_conversion,[],[f179247]) ).
cnf(s22284,plain,
( spl28_4
| spl28_27
| spl28_276
| ~ spl28_1767
| spl28_1773 ),
inference(sat_conversion,[],[f179581]) ).
cnf(s23381,plain,
( spl28_4
| spl28_27
| spl28_276
| ~ spl28_1672
| spl28_1689 ),
inference(sat_conversion,[],[f185650]) ).
cnf(s23533,plain,
( spl28_27
| ~ spl28_1689
| ~ spl28_1749
| ~ spl28_1773
| spl28_12194 ),
inference(sat_conversion,[],[f186100]) ).
cnf(s31545,plain,
( spl28_5
| ~ spl28_26
| spl28_27
| spl28_41
| spl28_13930 ),
inference(sat_conversion,[],[f235896]) ).
cnf(s31547,plain,
( spl28_5
| ~ spl28_26
| spl28_27
| ~ spl28_29
| ~ spl28_38
| spl28_41
| ~ spl28_12194
| ~ spl28_13929 ),
inference(sat_conversion,[],[f235902]) ).
cnf(s32117,plain,
~ spl28_276,
inference(rat,[],[s260,s35]) ).
cnf(s32149,plain,
( spl28_5
| spl28_29 ),
inference(rat,[],[s21,s35,s25]) ).
cnf(s32174,plain,
spl28_1728,
inference(rat,[],[s19017,s9,s8]) ).
cnf(s32175,plain,
spl28_1767,
inference(rat,[],[s16952,s9,s8]) ).
cnf(s32176,plain,
spl28_1672,
inference(rat,[],[s16871,s9,s8]) ).
cnf(s32202,plain,
spl28_13930,
inference(rat,[],[s31545,s25,s39,s35,s4]) ).
cnf(s32268,plain,
spl28_29,
inference(rat,[],[s32149,s4]) ).
cnf(s32334,plain,
spl28_13929,
inference(rat,[],[s21194,s32202,s39,s32268]) ).
cnf(s32337,plain,
~ spl28_12194,
inference(rat,[],[s31547,s32334,s4,s39,s55,s25,s35,s32268]) ).
cnf(s32473,plain,
spl28_1689,
inference(rat,[],[s23381,s32176,s32117,s35,s3]) ).
cnf(s32474,plain,
spl28_1773,
inference(rat,[],[s22284,s32175,s32117,s35,s3]) ).
cnf(s32475,plain,
spl28_1749,
inference(rat,[],[s22209,s32174,s32117,s35,s3]) ).
cnf(s32478,plain,
$false,
inference(rat,[],[s23533,s32337,s32474,s35,s32475,s32473]) ).
fof(f235903,plain,
$false,
inference(avatar_sat_refutation,[],[s32478]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT309+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.07 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.18/0.44 % Computer : n007.cluster.edu
% 0.18/0.44 % Model : x86_64 x86_64
% 0.18/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.44 % Memory : 8046.5625MB
% 0.18/0.44 % OS : Linux 6.8.0-71-generic
% 0.18/0.44 % CPULimit : 300
% 0.18/0.44 % WCLimit : 300
% 0.18/0.44 % DateTime : Sun Sep 27 14:25:55 UTC 2026
% 0.18/0.44 % CPUTime :
% 0.18/0.45 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.23/0.49 Running first-order model finding
% 0.23/0.49 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
% 26.44/4.26 % (1466413)Will run a generic schedule for satisfiability detection.
% 26.44/4.26 % (1466419)% WARNING: option uhcvi not known.
% 26.44/4.26 % (1466419)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=831819505:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 26.44/4.26 % (1466418)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2811816160_2999 on theBenchmark for (2999ds/0Mi)
% 26.44/4.26 % (1466423)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3778556201:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 26.44/4.26 % (1466422)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3377731348:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 26.44/4.26 % (1466421)dis+10_1_sil=32000:sp=arity:random_seed=1151956422:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 26.44/4.26 % (1466424)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3837432700:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 26.44/4.26 % (1466420)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1757070831:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 26.44/4.26 % TRYING [1]
% 26.44/4.26 % TRYING [2]
% 26.44/4.26 % TRYING [3]
% 26.44/4.26 % TRYING [4]
% 26.44/4.26 % TRYING [5]
% 26.44/4.26 % (1466421)Instruction limit reached!
% 26.44/4.26 % (1466421)------------------------------
% 26.44/4.26 % (1466421)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.44/4.26 % (1466421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.44/4.26 % (1466421)CaDiCaL version: 2.1.3
% 26.44/4.26 % (1466421)Termination reason: Instruction limit
% 26.44/4.26 % (1466421)Termination phase: Saturation
% 26.44/4.26 % (1466421)Time elapsed: 0.107 s
% 26.44/4.26 % (1466421)Peak memory usage: 13 MB
% 26.44/4.26 % (1466421)Instructions burned: 105 (million)
% 26.44/4.26 % (1466423)Instruction limit reached!
% 26.44/4.26 % (1466423)------------------------------
% 26.44/4.26 % (1466423)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.44/4.26 % (1466423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.44/4.26 % (1466423)CaDiCaL version: 2.1.3
% 26.44/4.26 % (1466423)Termination reason: Instruction limit
% 26.44/4.26 % (1466423)Termination phase: Saturation
% 26.44/4.26 % (1466423)Time elapsed: 0.110 s
% 26.44/4.26 % (1466423)Peak memory usage: 14 MB
% 26.44/4.26 % (1466423)Instructions burned: 131 (million)
% 26.44/4.26 % (1466422)Instruction limit reached!
% 26.44/4.26 % (1466422)------------------------------
% 26.44/4.26 % (1466422)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.44/4.26 % (1466422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.44/4.26 % (1466422)CaDiCaL version: 2.1.3
% 26.44/4.26 % (1466422)Termination reason: Instruction limit
% 26.44/4.26 % (1466422)Termination phase: Saturation
% 26.44/4.26 % (1466422)Time elapsed: 0.119 s
% 26.44/4.26 % (1466422)Peak memory usage: 13 MB
% 26.44/4.26 % (1466422)Instructions burned: 116 (million)
% 26.44/4.26 % (1466424)Instruction limit reached!
% 26.44/4.26 % (1466424)------------------------------
% 26.44/4.26 % (1466424)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.44/4.26 % (1466424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.44/4.26 % (1466424)CaDiCaL version: 2.1.3
% 26.44/4.26 % (1466424)Termination reason: Instruction limit
% 26.44/4.26 % (1466424)Termination phase: Saturation
% 26.44/4.26 % (1466424)Time elapsed: 0.134 s
% 26.44/4.26 % (1466424)Peak memory usage: 13 MB
% 26.44/4.26 % (1466424)Instructions burned: 159 (million)
% 26.44/4.26 % (1466432)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3702327672:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 26.44/4.26 % (1466434)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=3522638822:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 26.44/4.26 % (1466433)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=828263490:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 26.44/4.26 % TRYING [1]
% 26.44/4.26 % TRYING [2]
% 26.44/4.26 % TRYING [3]
% 26.44/4.26 % (1466435)ott-21_1_sil=16000:fs=off:random_seed=3515197334:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 26.44/4.26 % TRYING [6]
% 26.44/4.26 % TRYING [4]
% 26.44/4.26 % (1466433)Instruction limit reached!
% 26.44/4.26 % (1466433)------------------------------
% 26.44/4.26 % (1466433)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.84/7.97 % (1466433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.84/7.97 % (1466433)CaDiCaL version: 2.1.3
% 50.84/7.97 % (1466433)Termination reason: Instruction limit
% 50.84/7.97 % (1466433)Termination phase: Saturation
% 50.84/7.97 % (1466433)Time elapsed: 0.134 s
% 50.84/7.97 % (1466433)Peak memory usage: 14 MB
% 50.84/7.97 % (1466433)Instructions burned: 131 (million)
% 50.84/7.97 % (1466440)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2960671820:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 50.84/7.97 % (1466435)Instruction limit reached!
% 50.84/7.97 % (1466435)------------------------------
% 50.84/7.97 % (1466435)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.84/7.97 % (1466435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.84/7.97 % (1466435)CaDiCaL version: 2.1.3
% 50.84/7.97 % (1466435)Termination reason: Instruction limit
% 50.84/7.97 % (1466435)Termination phase: Saturation
% 50.84/7.97 % (1466435)Time elapsed: 0.164 s
% 50.84/7.97 % (1466435)Peak memory usage: 13 MB
% 50.84/7.97 % (1466435)Instructions burned: 181 (million)
% 50.84/7.97 % TRYING [5]
% 50.84/7.97 % (1466442)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2661643703:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 50.84/7.97 % TRYING [1]
% 50.84/7.97 % TRYING [2]
% 50.84/7.97 % TRYING [3]
% 50.84/7.97 % TRYING [4]
% 50.84/7.97 % TRYING [7]
% 50.84/7.97 % TRYING [5]
% 50.84/7.97 % (1466432)Instruction limit reached!
% 50.84/7.97 % (1466432)------------------------------
% 50.84/7.97 % (1466432)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.84/7.97 % (1466432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.84/7.97 % (1466432)CaDiCaL version: 2.1.3
% 50.84/7.97 % (1466432)Termination reason: Instruction limit
% 50.84/7.97 % (1466432)Termination phase: Finite model building constraint generation
% 50.84/7.97 % (1466432)Time elapsed: 0.480 s
% 50.84/7.97 % (1466432)Peak memory usage: 30 MB
% 50.84/7.97 % (1466432)Instructions burned: 714 (million)
% 50.84/7.97 % (1466446)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3092280292:i=1179_2993 on theBenchmark for (2993ds/1179Mi)
% 50.84/7.97 % (1466440)Instruction limit reached!
% 50.84/7.97 % (1466440)------------------------------
% 50.84/7.97 % (1466440)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.84/7.97 % (1466440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.84/7.97 % (1466440)CaDiCaL version: 2.1.3
% 50.84/7.97 % (1466440)Termination reason: Instruction limit
% 50.84/7.97 % (1466440)Termination phase: Saturation
% 50.84/7.97 % (1466440)Time elapsed: 0.521 s
% 50.84/7.97 % (1466440)Peak memory usage: 15 MB
% 50.84/7.97 % (1466440)Instructions burned: 477 (million)
% 50.84/7.97 % (1466442)Instruction limit reached!
% 50.84/7.97 % (1466442)------------------------------
% 50.84/7.97 % (1466442)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.84/7.97 % (1466442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.84/7.97 % (1466442)CaDiCaL version: 2.1.3
% 50.84/7.97 % (1466442)Termination reason: Instruction limit
% 50.84/7.97 % (1466442)Termination phase: Finite model building SAT solving
% 50.84/7.97 % (1466442)Time elapsed: 0.484 s
% 50.84/7.97 % (1466442)Peak memory usage: 21 MB
% 50.84/7.97 % (1466442)Instructions burned: 867 (million)
% 50.84/7.97 % (1466434)Instruction limit reached!
% 50.84/7.97 % (1466434)------------------------------
% 50.84/7.97 % (1466434)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.84/7.97 % (1466434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.84/7.97 % (1466434)CaDiCaL version: 2.1.3
% 50.84/7.97 % (1466434)Termination reason: Instruction limit
% 50.84/7.97 % (1466434)Termination phase: Saturation
% 50.84/7.97 % (1466434)Time elapsed: 0.705 s
% 50.84/7.97 % (1466434)Peak memory usage: 20 MB
% 50.84/7.97 % (1466434)Instructions burned: 684 (million)
% 50.84/7.97 % (1466448)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1532970461:i=889:ins=1_2991 on theBenchmark for (2991ds/889Mi)
% 50.84/7.97 % (1466450)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3577655645:i=879:kws=inv_precedence:fsr=off_2991 on theBenchmark for (2991ds/879Mi)
% 50.84/7.97 % (1466449)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=772581056:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2991 on theBenchmark for (2991ds/692Mi)
% 50.84/7.97 % TRYING [14]
% 50.84/7.97 % TRYING [8]
% 50.84/7.97 % (1466448)Instruction limit reached!
% 50.84/7.97 % (1466448)------------------------------
% 50.84/7.97 % (1466448)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.84/7.97 % (1466448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.84/7.97 % (1466448)CaDiCaL version: 2.1.3
% 50.84/7.97 % (1466448)Termination reason: Instruction limit
% 50.84/7.97 % (1466448)Termination phase: Finite model building constraint generation
% 50.84/7.97 % (1466448)Time elapsed: 0.641 s
% 50.84/7.97 % (1466448)Peak memory usage: 66 MB
% 50.84/7.97 % (1466448)Instructions burned: 890 (million)
% 50.84/7.97 % (1466449)Instruction limit reached!
% 50.84/7.97 % (1466449)------------------------------
% 50.84/7.97 % (1466449)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.84/7.97 % (1466449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.84/7.97 % (1466449)CaDiCaL version: 2.1.3
% 50.84/7.97 % (1466449)Termination reason: Instruction limit
% 50.84/7.97 % (1466449)Termination phase: Saturation
% 50.84/7.97 % (1466449)Time elapsed: 0.614 s
% 50.84/7.97 % (1466449)Peak memory usage: 16 MB
% 50.84/7.97 % (1466449)Instructions burned: 693 (million)
% 50.84/7.97 % (1466454)fmb+10_1_sil=64000:random_seed=4019571800:i=22061:nm=2:gsp=on_2984 on theBenchmark for (2984ds/22061Mi)
% 50.84/7.97 % (1466455)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2227072924:i=9515:nm=5_2984 on theBenchmark for (2984ds/9515Mi)
% 50.84/7.97 % TRYING [1]
% 50.84/7.97 % TRYING [2]
% 50.84/7.97 % TRYING [20]
% 50.84/7.97 % TRYING [3]
% 50.84/7.97 % (1466450)Instruction limit reached!
% 50.84/7.97 % (1466450)------------------------------
% 50.84/7.97 % (1466450)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.84/7.97 % (1466450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.84/7.97 % (1466450)CaDiCaL version: 2.1.3
% 50.84/7.97 % (1466450)Termination reason: Instruction limit
% 50.84/7.97 % (1466450)Termination phase: Saturation
% 50.84/7.97 % (1466450)Time elapsed: 0.748 s
% 50.84/7.97 % (1466450)Peak memory usage: 20 MB
% 50.84/7.97 % (1466450)Instructions burned: 879 (million)
% 50.84/7.97 % (1466458)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3268178019:fmbsr=1.7:i=920_2983 on theBenchmark for (2983ds/920Mi)
% 50.84/7.97 % TRYING [4]
% 50.84/7.97 % TRYING [8]
% 50.84/7.97 % (1466446)Instruction limit reached!
% 50.84/7.97 % (1466446)------------------------------
% 50.84/7.97 % (1466446)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.84/7.97 % (1466446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.84/7.97 % (1466446)CaDiCaL version: 2.1.3
% 50.84/7.97 % (1466446)Termination reason: Instruction limit
% 50.84/7.97 % (1466446)Termination phase: Saturation
% 50.84/7.97 % (1466446)Time elapsed: 1.120 s
% 50.84/7.97 % (1466446)Peak memory usage: 25 MB
% 50.84/7.97 % (1466446)Instructions burned: 1180 (million)
% 50.84/7.97 % (1466460)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2196900569:i=5131_2981 on theBenchmark for (2981ds/5131Mi)
% 50.84/7.97 % TRYING [5]
% 50.84/7.97 % (1466458)Instruction limit reached!
% 50.84/7.97 % (1466458)------------------------------
% 50.84/7.97 % (1466458)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.84/7.97 % (1466458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.84/7.97 % (1466458)CaDiCaL version: 2.1.3
% 50.84/7.97 % (1466458)Termination reason: Instruction limit
% 50.84/7.97 % (1466458)Termination phase: Finite model building SAT solving
% 50.84/7.97 % (1466458)Time elapsed: 0.646 s
% 50.84/7.97 % (1466458)Peak memory usage: 58 MB
% 50.84/7.97 % (1466458)Instructions burned: 922 (million)
% 50.84/7.97 % (1466462)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1712506602:i=1472:ins=7:fdi=8:gsp=on_2976 on theBenchmark for (2976ds/1472Mi)
% 50.84/7.97 % (1466462)Instruction limit reached!
% 50.84/7.97 % (1466462)------------------------------
% 50.84/7.97 % (1466462)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.84/7.97 % (1466462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.84/7.97 % (1466462)CaDiCaL version: 2.1.3
% 50.84/7.97 % (1466462)Termination reason: Instruction limit
% 50.84/7.97 % (1466462)Termination phase: Saturation
% 50.84/7.97 % (1466462)Time elapsed: 1.346 s
% 50.84/7.97 % (1466462)Peak memory usage: 27 MB
% 50.84/7.97 % (1466462)Instructions burned: 1472 (million)
% 50.84/7.97 % (1466466)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2320879787:i=6324_2962 on theBenchmark for (2962ds/6324Mi)
% 50.84/7.97 % TRYING [77]
% 50.84/7.97 % TRYING [6]
% 50.84/7.97 % (1466460)Instruction limit reached!
% 50.84/7.97 % (1466460)------------------------------
% 50.84/7.97 % (1466460)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.84/7.97 % (1466460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.84/7.97 % (1466460)CaDiCaL version: 2.1.3
% 50.84/7.97 % (1466460)Termination reason: Instruction limit
% 50.84/7.97 % (1466460)Termination phase: Saturation
% 50.84/7.97 % (1466460)Time elapsed: 4.054 s
% 50.84/7.97 % (1466460)Peak memory usage: 36 MB
% 50.84/7.97 % (1466460)Instructions burned: 5132 (million)
% 50.84/7.97 % (1466579)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=970783826:fmbsr=2.30978:i=2174_2941 on theBenchmark for (2941ds/2174Mi)
% 50.84/7.97 % TRYING [16]
% 50.84/7.97 % (1466466)Instruction limit reached!
% 50.84/7.97 % (1466466)------------------------------
% 50.84/7.97 % (1466466)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.84/7.97 % (1466466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.84/7.97 % (1466466)CaDiCaL version: 2.1.3
% 50.84/7.97 % (1466466)Termination reason: Instruction limit
% 50.84/7.97 % (1466466)Termination phase: Finite model building constraint generation
% 50.84/7.97 % (1466466)Time elapsed: 2.722 s
% 50.84/7.97 % (1466466)Peak memory usage: 394 MB
% 50.84/7.97 % (1466466)Instructions burned: 6326 (million)
% 50.84/7.97 % (1466623)ott-2_1_sil=16000:newcnf=on:random_seed=2258631707:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2934 on theBenchmark for (2934ds/869Mi)
% 50.84/7.97 % (1466579)Instruction limit reached!
% 50.84/7.97 % (1466579)------------------------------
% 50.84/7.97 % (1466579)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.84/7.97 % (1466579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.84/7.97 % (1466579)CaDiCaL version: 2.1.3
% 50.84/7.97 % (1466579)Termination reason: Instruction limit
% 50.84/7.97 % (1466579)Termination phase: Finite model building constraint generation
% 50.84/7.97 % (1466579)Time elapsed: 0.743 s
% 50.84/7.97 % (1466579)Peak memory usage: 129 MB
% 50.84/7.97 % (1466579)Instructions burned: 2174 (million)
% 50.84/7.97 % (1466455)Instruction limit reached!
% 50.84/7.97 % (1466455)------------------------------
% 50.84/7.97 % (1466455)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.84/7.97 % (1466455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.84/7.97 % (1466455)CaDiCaL version: 2.1.3
% 50.84/7.97 % (1466455)Termination reason: Instruction limit
% 50.84/7.97 % (1466455)Termination phase: Finite model building constraint generation
% 50.84/7.97 % (1466455)Time elapsed: 5.092 s
% 50.84/7.97 % (1466455)Peak memory usage: 538 MB
% 50.84/7.97 % (1466455)Instructions burned: 9516 (million)
% 50.84/7.97 % (1466625)ott+10_1_sil=32000:tgt=ground:random_seed=2997154356:i=5114:av=off_2933 on theBenchmark for (2933ds/5114Mi)
% 50.84/7.97 % (1466627)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2140379021:i=54282_2932 on theBenchmark for (2932ds/54282Mi)
% 50.84/7.97 % TRYING [1]
% 50.84/7.97 % TRYING [2]
% 50.84/7.97 % TRYING [3]
% 50.84/7.97 % TRYING [4]
% 50.84/7.97 % TRYING [5]
% 50.84/7.97 % TRYING [6]
% 50.84/7.97 % (1466623)Instruction limit reached!
% 50.84/7.97 % (1466623)------------------------------
% 50.84/7.97 % (1466623)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.84/7.97 % (1466623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.84/7.97 % (1466623)CaDiCaL version: 2.1.3
% 50.84/7.97 % (1466623)Termination reason: Instruction limit
% 50.84/7.97 % (1466623)Termination phase: Saturation
% 50.84/7.97 % (1466623)Time elapsed: 0.451 s
% 50.84/7.97 % (1466623)Peak memory usage: 18 MB
% 50.84/7.97 % (1466623)Instructions burned: 871 (million)
% 50.84/7.97 % TRYING [7]
% 50.84/7.97 % (1466629)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=442653152:i=3512:aac=none_2930 on theBenchmark for (2930ds/3512Mi)
% 50.84/7.97 % (1466419) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1466413-1466419"...
% 50.84/7.97 % (1466419)...printing done.
% 50.84/7.97 % (1466419)Refutation found. Thanks to Tanya!
% 50.84/7.97 % SZS status Theorem for theBenchmark
% 50.84/7.97 % SZS output start Proof for theBenchmark
% See solution above
% 50.84/7.98 % (1466419)------------------------------
% 50.84/7.98 % (1466419)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.84/7.98 % (1466419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.84/7.98 % (1466419)CaDiCaL version: 2.1.3
% 50.84/7.98 % (1466419)Termination reason: Refutation
% 50.84/7.98 % (1466419)Time elapsed: 7.423 s
% 50.84/7.98 % (1466419)Peak memory usage: 115 MB
% 50.84/7.98 % (1466419)Instructions burned: 17687 (million)
% 50.84/7.98 % (1466413)Success in time 7.475 s
% 50.84/7.98 % Vampire exiting
%------------------------------------------------------------------------------