%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LAT312+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 : n015.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:21 AM UTC 2026
% Result : Theorem 207.57s 40.15s
% Output : Refutation 207.57s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 70
% Syntax : Number of formulae : 513 ( 60 unt; 28 def)
% Number of atoms : 1887 ( 199 equ)
% Maximal formula atoms : 13 ( 3 avg)
% Number of connectives : 2338 ( 964 ~;1092 |; 188 &)
% ( 34 <=>; 60 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 58 ( 56 usr; 28 prp; 0-3 aty)
% Number of functors : 24 ( 24 usr; 4 con; 0-3 aty)
% Number of variables : 438 ( 0 sgn 430 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( ( ~ v1_xboole_0(X2)
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
=> ( r1_filter_2(u1_struct_0(X0),X2,k6_domain_1(u1_struct_0(X0),X1))
=> r1_filter_2(u1_struct_0(X0),k19_filter_2(X0,X2),k18_filter_2(X0,X1)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t41_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))
=> ! [X2] :
( ( ~ v1_xboole_0(X2)
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
=> ( r1_filter_2(u1_struct_0(X0),X2,k6_domain_1(u1_struct_0(X0),X1))
=> r1_filter_2(u1_struct_0(X0),k19_filter_2(X0,X2),k18_filter_2(X0,X1)) ) ) ) ),
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(f11,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(f12,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> k2_filter_0(X0,X1) = a_2_0_filter_0(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d3_filter_0) ).
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(f19,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
=> m2_filter_2(k19_filter_2(X0,X1),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k19_filter_2) ).
fof(f20,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(f25,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& m1_subset_1(X1,u1_struct_0(X0)) )
=> m1_filter_2(k2_filter_2(X0,X1),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k2_filter_2) ).
fof(f29,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(f30,axiom,
! [X0,X1] :
( ( ~ v1_xboole_0(X0)
& m1_subset_1(X1,X0) )
=> m1_subset_1(k6_domain_1(X0,X1),k1_zfmisc_1(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k6_domain_1) ).
fof(f31,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
=> m1_subset_1(k7_filter_2(X0,X1),k1_zfmisc_1(u1_struct_0(k1_lattice2(X0)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k7_filter_2) ).
fof(f32,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(k1_lattice2(X0)))) )
=> m1_subset_1(k8_filter_2(X0,X1),k1_zfmisc_1(u1_struct_0(X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k8_filter_2) ).
fof(f35,axiom,
! [X0] :
( l2_lattices(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l2_lattices) ).
fof(f36,axiom,
! [X0] :
( l3_lattices(X0)
=> ( l1_lattices(X0)
& l2_lattices(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l3_lattices) ).
fof(f37,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(f38,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_filter_2(X1,X0)
=> ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m1_filter_2) ).
fof(f41,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(f42,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(f44,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(f46,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] :
? [X1] : m1_subset_1(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',existence_m1_subset_1) ).
fof(f59,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(f60,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_struct_0(X0) )
=> ~ v1_xboole_0(u1_struct_0(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_struct_0) ).
fof(f68,axiom,
! [X0] :
( ~ v1_xboole_0(k1_tarski(X0))
& v1_finset_1(k1_tarski(X0))
& v1_realset1(k1_tarski(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc3_realset1) ).
fof(f72,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(f75,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] :
( v1_relat_1(X0)
& v1_xboole_0(X0)
& v1_funct_1(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc2_funct_1) ).
fof(f91,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& m1_subset_1(X1,u1_struct_0(X0)) )
=> k2_filter_2(X0,X1) = k2_filter_0(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k2_filter_2) ).
fof(f92,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
=> k3_filter_2(X0,X1) = k3_filter_0(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k3_filter_2) ).
fof(f93,axiom,
! [X0,X1] :
( ( ~ v1_xboole_0(X0)
& m1_subset_1(X1,X0) )
=> k6_domain_1(X0,X1) = k1_tarski(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k6_domain_1) ).
fof(f94,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_filter_2(X1,X0)
<=> m1_filter_0(X1,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_m1_filter_2) ).
fof(f95,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(f96,axiom,
! [X0,X1,X2] :
( ( ~ v1_xboole_0(X0)
& m1_subset_1(X1,k1_zfmisc_1(X0))
& m1_subset_1(X2,k1_zfmisc_1(X0)) )
=> ( r1_filter_2(X0,X1,X2)
<=> X1 = X2 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_r1_filter_2) ).
fof(f101,axiom,
! [X0,X1,X2] :
( ( ~ v1_xboole_0(X0)
& m1_subset_1(X1,k1_zfmisc_1(X0))
& m1_subset_1(X2,k1_zfmisc_1(X0)) )
=> ( r1_filter_2(X0,X1,X2)
=> r1_filter_2(X0,X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',symmetry_r1_filter_2) ).
fof(f103,axiom,
! [X0,X1] :
( m1_subset_1(X0,X1)
=> ( v1_xboole_0(X1)
| r2_hidden(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2_subset) ).
fof(f105,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( ( ~ v1_xboole_0(X2)
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
=> ( X2 = k6_domain_1(u1_struct_0(X0),X1)
=> k3_filter_0(X0,X2) = k2_filter_0(X0,X1) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t30_filter_0) ).
fof(f106,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ( k18_filter_2(X0,X1) = k2_filter_2(k1_lattice2(X0),k5_filter_2(X0,X1))
& k18_filter_2(k1_lattice2(X0),k5_filter_2(X0,X1)) = k2_filter_2(X0,X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t30_filter_2) ).
fof(f107,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( ( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
=> ! [X2] :
( ( ~ v1_xboole_0(X2)
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(k1_lattice2(X0)))) )
=> ( k3_filter_2(k1_lattice2(X0),k7_filter_2(X0,X1)) = k19_filter_2(X0,X1)
& k3_filter_2(X0,X1) = k19_filter_2(k1_lattice2(X0),k7_filter_2(X0,X1))
& k3_filter_2(X0,k8_filter_2(X0,X2)) = k19_filter_2(k1_lattice2(X0),X2)
& k3_filter_2(k1_lattice2(X0),X2) = k19_filter_2(X0,k8_filter_2(X0,X2)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t37_filter_2) ).
fof(f110,axiom,
! [X0,X1,X2] :
~ ( r2_hidden(X0,X1)
& m1_subset_1(X1,k1_zfmisc_1(X2))
& v1_xboole_0(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_subset) ).
fof(f113,axiom,
! [X0,X1] :
~ ( v1_xboole_0(X0)
& X0 != X1
& v1_xboole_0(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t8_boole) ).
fof(f116,plain,
! [X0] :
( ~ v1_xboole_0(k1_tarski(X0))
& v1_realset1(k1_tarski(X0)) ),
inference(pure_predicate_removal,[],[f68]) ).
fof(f127,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ~ r1_filter_2(u1_struct_0(X0),k19_filter_2(X0,X2),k18_filter_2(X0,X1))
& r1_filter_2(u1_struct_0(X0),X2,k6_domain_1(u1_struct_0(X0),X1))
& ~ v1_xboole_0(X2)
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
& m1_subset_1(X1,u1_struct_0(X0)) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(ennf_transformation,[],[f2]) ).
fof(f128,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ~ r1_filter_2(u1_struct_0(X0),k19_filter_2(X0,X2),k18_filter_2(X0,X1))
& r1_filter_2(u1_struct_0(X0),X2,k6_domain_1(u1_struct_0(X0),X1))
& ~ v1_xboole_0(X2)
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
& m1_subset_1(X1,u1_struct_0(X0)) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(flattening,[],[f127]) ).
fof(f129,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(f130,plain,
! [X0] :
( X0 = g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))
| ~ v3_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f129]) ).
fof(f141,plain,
! [X0] :
( k1_lattice2(X0) = g3_lattices(u1_struct_0(X0),u1_lattices(X0),u2_lattices(X0))
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f11]) ).
fof(f142,plain,
! [X0] :
( ! [X1] :
( k2_filter_0(X0,X1) = a_2_0_filter_0(X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f12]) ).
fof(f143,plain,
! [X0] :
( ! [X1] :
( k2_filter_0(X0,X1) = a_2_0_filter_0(X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f142]) ).
fof(f144,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(f145,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,[],[f144]) ).
fof(f146,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(f147,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,[],[f146]) ).
fof(f148,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(f149,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,[],[f148]) ).
fof(f156,plain,
! [X0,X1] :
( m2_filter_2(k19_filter_2(X0,X1),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ),
inference(ennf_transformation,[],[f19]) ).
fof(f157,plain,
! [X0,X1] :
( m2_filter_2(k19_filter_2(X0,X1),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ),
inference(flattening,[],[f156]) ).
fof(f158,plain,
! [X0] :
( ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f20]) ).
fof(f161,plain,
! [X0,X1] :
( m1_filter_2(k2_filter_2(X0,X1),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f25]) ).
fof(f162,plain,
! [X0,X1] :
( m1_filter_2(k2_filter_2(X0,X1),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(flattening,[],[f161]) ).
fof(f167,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,[],[f29]) ).
fof(f168,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,[],[f167]) ).
fof(f169,plain,
! [X0,X1] :
( m1_subset_1(k6_domain_1(X0,X1),k1_zfmisc_1(X0))
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0) ),
inference(ennf_transformation,[],[f30]) ).
fof(f170,plain,
! [X0,X1] :
( m1_subset_1(k6_domain_1(X0,X1),k1_zfmisc_1(X0))
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0) ),
inference(flattening,[],[f169]) ).
fof(f171,plain,
! [X0,X1] :
( m1_subset_1(k7_filter_2(X0,X1),k1_zfmisc_1(u1_struct_0(k1_lattice2(X0))))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ),
inference(ennf_transformation,[],[f31]) ).
fof(f172,plain,
! [X0,X1] :
( m1_subset_1(k7_filter_2(X0,X1),k1_zfmisc_1(u1_struct_0(k1_lattice2(X0))))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ),
inference(flattening,[],[f171]) ).
fof(f173,plain,
! [X0,X1] :
( m1_subset_1(k8_filter_2(X0,X1),k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(k1_lattice2(X0)))) ),
inference(ennf_transformation,[],[f32]) ).
fof(f174,plain,
! [X0,X1] :
( m1_subset_1(k8_filter_2(X0,X1),k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(k1_lattice2(X0)))) ),
inference(flattening,[],[f173]) ).
fof(f176,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l2_lattices(X0) ),
inference(ennf_transformation,[],[f35]) ).
fof(f177,plain,
! [X0] :
( ( l1_lattices(X0)
& l2_lattices(X0) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f36]) ).
fof(f178,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,[],[f37]) ).
fof(f179,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,[],[f178]) ).
fof(f180,plain,
! [X0] :
( ! [X1] :
( ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) )
| ~ m1_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f38]) ).
fof(f181,plain,
! [X0] :
( ! [X1] :
( ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) )
| ~ m1_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f180]) ).
fof(f182,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,[],[f41]) ).
fof(f183,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,[],[f182]) ).
fof(f184,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,[],[f42]) ).
fof(f185,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,[],[f184]) ).
fof(f187,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,[],[f44]) ).
fof(f188,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,[],[f46]) ).
fof(f199,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f59]) ).
fof(f200,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f199]) ).
fof(f201,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f60]) ).
fof(f202,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(flattening,[],[f201]) ).
fof(f217,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,[],[f72]) ).
fof(f218,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,[],[f217]) ).
fof(f223,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,[],[f75]) ).
fof(f224,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,[],[f223]) ).
fof(f230,plain,
! [X0,X1] :
( k2_filter_2(X0,X1) = k2_filter_0(X0,X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f91]) ).
fof(f231,plain,
! [X0,X1] :
( k2_filter_2(X0,X1) = k2_filter_0(X0,X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(flattening,[],[f230]) ).
fof(f232,plain,
! [X0,X1] :
( k3_filter_2(X0,X1) = k3_filter_0(X0,X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ),
inference(ennf_transformation,[],[f92]) ).
fof(f233,plain,
! [X0,X1] :
( k3_filter_2(X0,X1) = k3_filter_0(X0,X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ),
inference(flattening,[],[f232]) ).
fof(f234,plain,
! [X0,X1] :
( k6_domain_1(X0,X1) = k1_tarski(X1)
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0) ),
inference(ennf_transformation,[],[f93]) ).
fof(f235,plain,
! [X0,X1] :
( k6_domain_1(X0,X1) = k1_tarski(X1)
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0) ),
inference(flattening,[],[f234]) ).
fof(f236,plain,
! [X0] :
( ! [X1] :
( m1_filter_2(X1,X0)
<=> m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f94]) ).
fof(f237,plain,
! [X0] :
( ! [X1] :
( m1_filter_2(X1,X0)
<=> m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f236]) ).
fof(f238,plain,
! [X0,X1,X2] :
( ( r1_filter_2(X0,X1,X2)
<=> X1 = X2 )
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f96]) ).
fof(f239,plain,
! [X0,X1,X2] :
( ( r1_filter_2(X0,X1,X2)
<=> X1 = X2 )
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(flattening,[],[f238]) ).
fof(f246,plain,
! [X0,X1,X2] :
( r1_filter_2(X0,X2,X1)
| ~ r1_filter_2(X0,X1,X2)
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f101]) ).
fof(f247,plain,
! [X0,X1,X2] :
( r1_filter_2(X0,X2,X1)
| ~ r1_filter_2(X0,X1,X2)
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(flattening,[],[f246]) ).
fof(f249,plain,
! [X0,X1] :
( v1_xboole_0(X1)
| r2_hidden(X0,X1)
| ~ m1_subset_1(X0,X1) ),
inference(ennf_transformation,[],[f103]) ).
fof(f250,plain,
! [X0,X1] :
( v1_xboole_0(X1)
| r2_hidden(X0,X1)
| ~ m1_subset_1(X0,X1) ),
inference(flattening,[],[f249]) ).
fof(f252,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( k3_filter_0(X0,X2) = k2_filter_0(X0,X1)
| k6_domain_1(u1_struct_0(X0),X1) != X2
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f105]) ).
fof(f253,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( k3_filter_0(X0,X2) = k2_filter_0(X0,X1)
| k6_domain_1(u1_struct_0(X0),X1) != X2
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f252]) ).
fof(f254,plain,
! [X0] :
( ! [X1] :
( ( k18_filter_2(X0,X1) = k2_filter_2(k1_lattice2(X0),k5_filter_2(X0,X1))
& k18_filter_2(k1_lattice2(X0),k5_filter_2(X0,X1)) = k2_filter_2(X0,X1) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f106]) ).
fof(f255,plain,
! [X0] :
( ! [X1] :
( ( k18_filter_2(X0,X1) = k2_filter_2(k1_lattice2(X0),k5_filter_2(X0,X1))
& k18_filter_2(k1_lattice2(X0),k5_filter_2(X0,X1)) = k2_filter_2(X0,X1) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f254]) ).
fof(f256,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( k3_filter_2(k1_lattice2(X0),k7_filter_2(X0,X1)) = k19_filter_2(X0,X1)
& k3_filter_2(X0,X1) = k19_filter_2(k1_lattice2(X0),k7_filter_2(X0,X1))
& k3_filter_2(X0,k8_filter_2(X0,X2)) = k19_filter_2(k1_lattice2(X0),X2)
& k3_filter_2(k1_lattice2(X0),X2) = k19_filter_2(X0,k8_filter_2(X0,X2)) )
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(k1_lattice2(X0)))) )
| v1_xboole_0(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,[],[f107]) ).
fof(f257,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( k3_filter_2(k1_lattice2(X0),k7_filter_2(X0,X1)) = k19_filter_2(X0,X1)
& k3_filter_2(X0,X1) = k19_filter_2(k1_lattice2(X0),k7_filter_2(X0,X1))
& k3_filter_2(X0,k8_filter_2(X0,X2)) = k19_filter_2(k1_lattice2(X0),X2)
& k3_filter_2(k1_lattice2(X0),X2) = k19_filter_2(X0,k8_filter_2(X0,X2)) )
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(k1_lattice2(X0)))) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f256]) ).
fof(f261,plain,
! [X0,X1,X2] :
( ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ v1_xboole_0(X2) ),
inference(ennf_transformation,[],[f110]) ).
fof(f264,plain,
! [X0,X1] :
( ~ v1_xboole_0(X0)
| X0 = X1
| ~ v1_xboole_0(X1) ),
inference(ennf_transformation,[],[f113]) ).
fof(f265,definition,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v4_lattices(k1_lattice2(X0))
& v5_lattices(k1_lattice2(X0))
& v6_lattices(k1_lattice2(X0))
& v7_lattices(k1_lattice2(X0))
& v8_lattices(k1_lattice2(X0))
& v9_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0)) )
| ~ sP0(X0) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f266,plain,
! [X0] :
( sP0(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(definition_folding,[],[f218,f265]) ).
fof(f267,plain,
( ~ r1_filter_2(u1_struct_0(sK1),k19_filter_2(sK1,sK3),k18_filter_2(sK1,sK2))
& r1_filter_2(u1_struct_0(sK1),sK3,k6_domain_1(u1_struct_0(sK1),sK2))
& ~ v1_xboole_0(sK3)
& m1_subset_1(sK3,k1_zfmisc_1(u1_struct_0(sK1)))
& m1_subset_1(sK2,u1_struct_0(sK1))
& ~ v3_struct_0(sK1)
& v10_lattices(sK1)
& l3_lattices(sK1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2,sK3]),skolemize(X0,sK1),skolemize(X1,sK2),skolemize(X2,sK3)],[f128]) ).
fof(f275,plain,
! [X0] : m1_subset_1(sK11(X0),X0),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11]),skolemize(X1,sK11(X0))],[f54]) ).
fof(f279,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)) )
| ~ sP0(X0) ),
inference(nnf_transformation,[],[f265]) ).
fof(f291,plain,
( v1_relat_1(sK22)
& v1_xboole_0(sK22)
& v1_funct_1(sK22) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK22]),skolemize(X0,sK22)],[f81]) ).
fof(f301,plain,
! [X0] :
( ! [X1] :
( ( m1_filter_2(X1,X0)
| ~ m1_filter_0(X1,X0) )
& ( m1_filter_0(X1,X0)
| ~ m1_filter_2(X1,X0) ) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f237]) ).
fof(f302,plain,
! [X0,X1,X2] :
( ( m2_relset_1(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1) )
& ( m1_relset_1(X2,X0,X1)
| ~ m2_relset_1(X2,X0,X1) ) ),
inference(nnf_transformation,[],[f95]) ).
fof(f303,plain,
! [X0,X1,X2] :
( ( ( r1_filter_2(X0,X1,X2)
| X1 != X2 )
& ( X1 = X2
| ~ r1_filter_2(X0,X1,X2) ) )
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(nnf_transformation,[],[f239]) ).
fof(f307,plain,
l3_lattices(sK1),
inference(cnf_transformation,[],[f267]) ).
fof(f308,plain,
v10_lattices(sK1),
inference(cnf_transformation,[],[f267]) ).
fof(f309,plain,
~ v3_struct_0(sK1),
inference(cnf_transformation,[],[f267]) ).
fof(f310,plain,
m1_subset_1(sK2,u1_struct_0(sK1)),
inference(cnf_transformation,[],[f267]) ).
fof(f311,plain,
m1_subset_1(sK3,k1_zfmisc_1(u1_struct_0(sK1))),
inference(cnf_transformation,[],[f267]) ).
fof(f312,plain,
~ v1_xboole_0(sK3),
inference(cnf_transformation,[],[f267]) ).
fof(f313,plain,
r1_filter_2(u1_struct_0(sK1),sK3,k6_domain_1(u1_struct_0(sK1),sK2)),
inference(cnf_transformation,[],[f267]) ).
fof(f314,plain,
~ r1_filter_2(u1_struct_0(sK1),k19_filter_2(sK1,sK3),k18_filter_2(sK1,sK2)),
inference(cnf_transformation,[],[f267]) ).
fof(f315,plain,
! [X0] :
( ~ v3_lattices(X0)
| g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) = X0
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f130]) ).
fof(f331,plain,
! [X0] :
( ~ l3_lattices(X0)
| k1_lattice2(X0) = g3_lattices(u1_struct_0(X0),u1_lattices(X0),u2_lattices(X0)) ),
inference(cnf_transformation,[],[f141]) ).
fof(f332,plain,
! [X0,X1] :
( v3_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| k2_filter_0(X0,X1) = a_2_0_filter_0(X0,X1)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f143]) ).
fof(f333,plain,
! [X0,X1] :
( v3_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| k5_filter_2(X0,X1) = X1
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f145]) ).
fof(f334,plain,
! [X0,X1] :
( v3_struct_0(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| k7_filter_2(X0,X1) = X1
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f147]) ).
fof(f335,plain,
! [X0,X1] :
( v3_struct_0(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(k1_lattice2(X0))))
| k8_filter_2(X0,X1) = X1
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f149]) ).
fof(f340,plain,
! [X0,X1] :
( v1_xboole_0(X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| m2_filter_2(k19_filter_2(X0,X1),X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ),
inference(cnf_transformation,[],[f157]) ).
fof(f341,plain,
! [X0] :
( l3_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f158]) ).
fof(f342,plain,
! [X0] :
( v3_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f158]) ).
fof(f344,plain,
! [X0,X1] :
( v3_struct_0(X0)
| m1_filter_2(k2_filter_2(X0,X1),X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f162]) ).
fof(f347,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(cnf_transformation,[],[f168]) ).
fof(f348,plain,
! [X0,X1] :
( m1_subset_1(k6_domain_1(X0,X1),k1_zfmisc_1(X0))
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0) ),
inference(cnf_transformation,[],[f170]) ).
fof(f349,plain,
! [X0,X1] :
( m1_subset_1(k7_filter_2(X0,X1),k1_zfmisc_1(u1_struct_0(k1_lattice2(X0))))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ),
inference(cnf_transformation,[],[f172]) ).
fof(f350,plain,
! [X0,X1] :
( m1_subset_1(k8_filter_2(X0,X1),k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(k1_lattice2(X0)))) ),
inference(cnf_transformation,[],[f174]) ).
fof(f352,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l2_lattices(X0) ),
inference(cnf_transformation,[],[f176]) ).
fof(f353,plain,
! [X0] :
( l2_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f177]) ).
fof(f354,plain,
! [X0] :
( l1_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f177]) ).
fof(f355,plain,
! [X0,X1] :
( v3_struct_0(X0)
| ~ m1_filter_0(X1,X0)
| m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f179]) ).
fof(f357,plain,
! [X0,X1] :
( v3_struct_0(X0)
| ~ m1_filter_2(X1,X0)
| m2_lattice4(X1,X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f181]) ).
fof(f359,plain,
! [X0,X1] :
( v3_struct_0(X0)
| ~ m2_filter_2(X1,X0)
| m2_lattice4(X1,X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f183]) ).
fof(f361,plain,
! [X0,X1] :
( v3_struct_0(X0)
| ~ m2_lattice4(X1,X0)
| m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f185]) ).
fof(f363,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(cnf_transformation,[],[f187]) ).
fof(f364,plain,
! [X0] :
( v1_funct_2(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| ~ l1_lattices(X0) ),
inference(cnf_transformation,[],[f187]) ).
fof(f365,plain,
! [X0] :
( v1_funct_1(u1_lattices(X0))
| ~ l1_lattices(X0) ),
inference(cnf_transformation,[],[f187]) ).
fof(f366,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(cnf_transformation,[],[f188]) ).
fof(f367,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(cnf_transformation,[],[f188]) ).
fof(f368,plain,
! [X0] :
( v1_funct_1(u2_lattices(X0))
| ~ l2_lattices(X0) ),
inference(cnf_transformation,[],[f188]) ).
fof(f376,plain,
! [X0] : m1_subset_1(sK11(X0),X0),
inference(cnf_transformation,[],[f275]) ).
fof(f382,plain,
! [X0] :
( ~ v3_struct_0(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f200]) ).
fof(f383,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[],[f202]) ).
fof(f397,plain,
! [X0] : ~ v1_xboole_0(k1_tarski(X0)),
inference(cnf_transformation,[],[f116]) ).
fof(f405,plain,
! [X0] :
( v10_lattices(k1_lattice2(X0))
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f279]) ).
fof(f413,plain,
! [X0] :
( ~ v3_struct_0(k1_lattice2(X0))
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f279]) ).
fof(f414,plain,
! [X0] :
( sP0(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f266]) ).
fof(f425,plain,
! [X2,X3,X0,X1,X4,X5] :
( g3_lattices(X0,X1,X2) != g3_lattices(X3,X4,X5)
| X0 = X3
| ~ 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(cnf_transformation,[],[f224]) ).
fof(f436,plain,
v1_xboole_0(sK22),
inference(cnf_transformation,[],[f291]) ).
fof(f464,plain,
! [X0,X1] :
( v3_struct_0(X0)
| k2_filter_0(X0,X1) = k2_filter_2(X0,X1)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f231]) ).
fof(f465,plain,
! [X0,X1] :
( v1_xboole_0(X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| k3_filter_0(X0,X1) = k3_filter_2(X0,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ),
inference(cnf_transformation,[],[f233]) ).
fof(f466,plain,
! [X0,X1] :
( v1_xboole_0(X0)
| k6_domain_1(X0,X1) = k1_tarski(X1)
| ~ m1_subset_1(X1,X0) ),
inference(cnf_transformation,[],[f235]) ).
fof(f467,plain,
! [X0,X1] :
( v3_struct_0(X0)
| ~ m1_filter_2(X1,X0)
| m1_filter_0(X1,X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f301]) ).
fof(f469,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f302]) ).
fof(f471,plain,
! [X2,X0,X1] :
( v1_xboole_0(X0)
| ~ r1_filter_2(X0,X1,X2)
| X1 = X2
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f303]) ).
fof(f472,plain,
! [X2,X0,X1] :
( r1_filter_2(X0,X1,X2)
| X1 != X2
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f303]) ).
fof(f478,plain,
! [X2,X0,X1] :
( v1_xboole_0(X0)
| ~ r1_filter_2(X0,X1,X2)
| r1_filter_2(X0,X2,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f247]) ).
fof(f480,plain,
! [X0,X1] :
( v1_xboole_0(X1)
| r2_hidden(X0,X1)
| ~ m1_subset_1(X0,X1) ),
inference(cnf_transformation,[],[f250]) ).
fof(f483,plain,
! [X2,X0,X1] :
( k2_filter_0(X0,X1) = k3_filter_0(X0,X2)
| k6_domain_1(u1_struct_0(X0),X1) != X2
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f253]) ).
fof(f485,plain,
! [X0,X1] :
( v3_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| k18_filter_2(X0,X1) = k2_filter_2(k1_lattice2(X0),k5_filter_2(X0,X1))
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f255]) ).
fof(f486,plain,
! [X2,X0,X1] :
( v1_xboole_0(X2)
| k3_filter_2(k1_lattice2(X0),X2) = k19_filter_2(X0,k8_filter_2(X0,X2))
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(k1_lattice2(X0))))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f257]) ).
fof(f492,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ r2_hidden(X0,X1)
| ~ v1_xboole_0(X2) ),
inference(cnf_transformation,[],[f261]) ).
fof(f495,plain,
! [X0,X1] :
( ~ v1_xboole_0(X1)
| ~ v1_xboole_0(X0)
| X0 = X1 ),
inference(cnf_transformation,[],[f264]) ).
fof(f498,plain,
! [X2,X0] :
( r1_filter_2(X0,X2,X2)
| v1_xboole_0(X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(equality_resolution,[],[f472]) ).
fof(f499,plain,
! [X0,X1] :
( v1_xboole_0(k6_domain_1(u1_struct_0(X0),X1))
| k2_filter_0(X0,X1) = k3_filter_0(X0,k6_domain_1(u1_struct_0(X0),X1))
| ~ m1_subset_1(k6_domain_1(u1_struct_0(X0),X1),k1_zfmisc_1(u1_struct_0(X0)))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(equality_resolution,[],[f483]) ).
fof(f500,plain,
! [X2,X0] :
( v1_xboole_0(X0)
| r1_filter_2(X0,X2,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(duplicate_literal_removal,[],[f498]) ).
fof(f544,plain,
! [X0] :
( r2_hidden(X0,sK3)
| ~ m1_subset_1(X0,sK3) ),
inference(resolution,[],[f480,f312]) ).
fof(f678,plain,
! [X0] :
( ~ r2_hidden(X0,sK3)
| ~ v1_xboole_0(u1_struct_0(sK1)) ),
inference(resolution,[],[f492,f311]) ).
fof(f711,definition,
( spl33_19
<=> ! [X0] : ~ m1_subset_1(X0,sK3) ),
introduced(definition,[new_symbols(definition,[spl33_19])],[avatar_definition]) ).
fof(f712,plain,
( ! [X0] : ~ m1_subset_1(X0,sK3)
| ~ spl33_19 ),
inference(avatar_component_clause,[],[f711]) ).
fof(f726,definition,
( spl33_23
<=> v1_xboole_0(u1_struct_0(sK1)) ),
introduced(definition,[new_symbols(definition,[spl33_23])],[avatar_definition]) ).
fof(f728,plain,
( ~ v1_xboole_0(u1_struct_0(sK1))
| spl33_23 ),
inference(avatar_component_clause,[],[f726]) ).
fof(f730,definition,
( spl33_24
<=> ! [X0] : ~ r2_hidden(X0,sK3) ),
introduced(definition,[new_symbols(definition,[spl33_24])],[avatar_definition]) ).
fof(f731,plain,
( ! [X0] : ~ r2_hidden(X0,sK3)
| ~ spl33_24 ),
inference(avatar_component_clause,[],[f730]) ).
fof(f732,plain,
( ~ spl33_23
| spl33_24 ),
inference(avatar_split_clause,[],[f678,f730,f726]) ).
fof(f735,plain,
( $false
| ~ spl33_19 ),
inference(resolution,[],[f712,f376]) ).
fof(f736,plain,
~ spl33_19,
inference(avatar_contradiction_clause,[],[f735]) ).
fof(f941,plain,
( ! [X0] : ~ m1_subset_1(X0,sK3)
| ~ spl33_24 ),
inference(resolution,[],[f731,f544]) ).
fof(f942,plain,
( spl33_19
| ~ spl33_24 ),
inference(avatar_split_clause,[],[f941,f730,f711]) ).
fof(f1158,plain,
! [X2,X0,X1] :
( r1_filter_2(X0,X1,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ v1_xboole_0(X2)
| X0 = X2 ),
inference(resolution,[],[f500,f495]) ).
fof(f1428,plain,
! [X2,X0,X1] :
( ~ v1_xboole_0(X2)
| ~ m1_subset_1(X1,X0)
| k6_domain_1(X0,X1) = k1_tarski(X1)
| X0 = X2 ),
inference(resolution,[],[f466,f495]) ).
fof(f1542,plain,
k1_lattice2(sK1) = g3_lattices(u1_struct_0(sK1),u1_lattices(sK1),u2_lattices(sK1)),
inference(resolution,[],[f331,f307]) ).
fof(f1666,plain,
! [X0] :
( ~ m2_filter_2(X0,sK1)
| m2_lattice4(X0,sK1)
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1) ),
inference(resolution,[],[f359,f309]) ).
fof(f1671,plain,
! [X0] :
( ~ m2_filter_2(X0,sK1)
| m2_lattice4(X0,sK1)
| ~ l3_lattices(sK1) ),
inference(forward_subsumption_resolution,[],[f1666,f308]) ).
fof(f1675,plain,
! [X0] :
( m2_lattice4(X0,sK1)
| ~ m2_filter_2(X0,sK1) ),
inference(forward_subsumption_resolution,[],[f1671,f307]) ).
fof(f1705,definition,
( spl33_99
<=> l1_struct_0(sK1) ),
introduced(definition,[new_symbols(definition,[spl33_99])],[avatar_definition]) ).
fof(f1706,plain,
( l1_struct_0(sK1)
| ~ spl33_99 ),
inference(avatar_component_clause,[],[f1705]) ).
fof(f1707,plain,
( ~ l1_struct_0(sK1)
| spl33_99 ),
inference(avatar_component_clause,[],[f1705]) ).
fof(f1714,plain,
( ~ l2_lattices(sK1)
| spl33_99 ),
inference(resolution,[],[f1707,f352]) ).
fof(f1716,plain,
( ~ l3_lattices(sK1)
| spl33_99 ),
inference(resolution,[],[f1714,f353]) ).
fof(f1717,plain,
( $false
| spl33_99 ),
inference(forward_subsumption_resolution,[],[f1716,f307]) ).
fof(f1718,plain,
spl33_99,
inference(avatar_contradiction_clause,[],[f1717]) ).
fof(f1730,plain,
! [X0] :
( m1_relset_1(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| ~ l1_lattices(X0) ),
inference(resolution,[],[f363,f469]) ).
fof(f1810,plain,
! [X0] :
( m1_relset_1(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| ~ l2_lattices(X0) ),
inference(resolution,[],[f366,f469]) ).
fof(f2040,plain,
! [X0] :
( k1_lattice2(X0) = g3_lattices(u1_struct_0(k1_lattice2(X0)),u2_lattices(k1_lattice2(X0)),u1_lattices(k1_lattice2(X0)))
| ~ l3_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(resolution,[],[f315,f342]) ).
fof(f2047,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,[],[f2040,f341]) ).
fof(f2197,plain,
! [X0,X1] :
( ~ m1_filter_0(X0,k1_lattice2(X1))
| m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k1_lattice2(X1))))
| ~ v10_lattices(k1_lattice2(X1))
| ~ l3_lattices(k1_lattice2(X1))
| ~ sP0(X1) ),
inference(resolution,[],[f355,f413]) ).
fof(f2204,plain,
! [X0,X1] :
( m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k1_lattice2(X1))))
| ~ m1_filter_0(X0,k1_lattice2(X1))
| ~ l3_lattices(k1_lattice2(X1))
| ~ sP0(X1) ),
inference(forward_subsumption_resolution,[],[f2197,f405]) ).
fof(f2252,plain,
! [X0,X1] :
( ~ m2_lattice4(X0,k1_lattice2(X1))
| m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k1_lattice2(X1))))
| ~ v10_lattices(k1_lattice2(X1))
| ~ l3_lattices(k1_lattice2(X1))
| ~ sP0(X1) ),
inference(resolution,[],[f361,f413]) ).
fof(f2253,plain,
! [X0] :
( ~ m2_lattice4(X0,sK1)
| m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1) ),
inference(resolution,[],[f361,f309]) ).
fof(f2258,plain,
! [X0] :
( ~ m2_lattice4(X0,sK1)
| m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ l3_lattices(sK1) ),
inference(forward_subsumption_resolution,[],[f2253,f308]) ).
fof(f2259,plain,
! [X0,X1] :
( m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k1_lattice2(X1))))
| ~ m2_lattice4(X0,k1_lattice2(X1))
| ~ l3_lattices(k1_lattice2(X1))
| ~ sP0(X1) ),
inference(forward_subsumption_resolution,[],[f2252,f405]) ).
fof(f2262,plain,
! [X0] :
( m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ m2_lattice4(X0,sK1) ),
inference(forward_subsumption_resolution,[],[f2258,f307]) ).
fof(f2309,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK1))
| k5_filter_2(sK1,X0) = X0
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1) ),
inference(resolution,[],[f333,f309]) ).
fof(f2314,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK1))
| k5_filter_2(sK1,X0) = X0
| ~ l3_lattices(sK1) ),
inference(forward_subsumption_resolution,[],[f2309,f308]) ).
fof(f2318,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK1))
| k5_filter_2(sK1,X0) = X0 ),
inference(forward_subsumption_resolution,[],[f2314,f307]) ).
fof(f2448,plain,
! [X0,X1] :
( m1_filter_2(k2_filter_2(k1_lattice2(X0),X1),k1_lattice2(X0))
| ~ v10_lattices(k1_lattice2(X0))
| ~ l3_lattices(k1_lattice2(X0))
| ~ m1_subset_1(X1,u1_struct_0(k1_lattice2(X0)))
| ~ sP0(X0) ),
inference(resolution,[],[f344,f413]) ).
fof(f2455,plain,
! [X0,X1] :
( m1_filter_2(k2_filter_2(k1_lattice2(X0),X1),k1_lattice2(X0))
| ~ l3_lattices(k1_lattice2(X0))
| ~ m1_subset_1(X1,u1_struct_0(k1_lattice2(X0)))
| ~ sP0(X0) ),
inference(forward_subsumption_resolution,[],[f2448,f405]) ).
fof(f2498,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1)))
| k7_filter_2(sK1,X0) = X0
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1) ),
inference(resolution,[],[f334,f309]) ).
fof(f2503,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1)))
| k7_filter_2(sK1,X0) = X0
| ~ l3_lattices(sK1) ),
inference(forward_subsumption_resolution,[],[f2498,f308]) ).
fof(f2507,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1)))
| k7_filter_2(sK1,X0) = X0 ),
inference(forward_subsumption_resolution,[],[f2503,f307]) ).
fof(f2561,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(X1)))
| k2_filter_0(k1_lattice2(X1),X0) = a_2_0_filter_0(k1_lattice2(X1),X0)
| ~ v10_lattices(k1_lattice2(X1))
| ~ l3_lattices(k1_lattice2(X1))
| ~ sP0(X1) ),
inference(resolution,[],[f332,f413]) ).
fof(f2568,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(X1)))
| k2_filter_0(k1_lattice2(X1),X0) = a_2_0_filter_0(k1_lattice2(X1),X0)
| ~ l3_lattices(k1_lattice2(X1))
| ~ sP0(X1) ),
inference(forward_subsumption_resolution,[],[f2561,f405]) ).
fof(f2599,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK1))))
| k8_filter_2(sK1,X0) = X0
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1) ),
inference(resolution,[],[f335,f309]) ).
fof(f2604,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK1))))
| k8_filter_2(sK1,X0) = X0
| ~ l3_lattices(sK1) ),
inference(forward_subsumption_resolution,[],[f2599,f308]) ).
fof(f2608,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK1))))
| k8_filter_2(sK1,X0) = X0 ),
inference(forward_subsumption_resolution,[],[f2604,f307]) ).
fof(f2815,plain,
! [X0,X1] :
( k2_filter_0(k1_lattice2(X0),X1) = k2_filter_2(k1_lattice2(X0),X1)
| ~ v10_lattices(k1_lattice2(X0))
| ~ l3_lattices(k1_lattice2(X0))
| ~ m1_subset_1(X1,u1_struct_0(k1_lattice2(X0)))
| ~ sP0(X0) ),
inference(resolution,[],[f464,f413]) ).
fof(f2822,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u1_struct_0(k1_lattice2(X0)))
| ~ l3_lattices(k1_lattice2(X0))
| k2_filter_0(k1_lattice2(X0),X1) = k2_filter_2(k1_lattice2(X0),X1)
| ~ sP0(X0) ),
inference(forward_subsumption_resolution,[],[f2815,f405]) ).
fof(f2860,plain,
! [X2,X3,X0,X1] :
( ~ v1_xboole_0(X3)
| ~ r1_filter_2(X0,X1,X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| X1 = X2
| X0 = X3 ),
inference(resolution,[],[f471,f495]) ).
fof(f2987,plain,
! [X0] :
( m2_filter_2(k19_filter_2(X0,sK3),X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(sK3,k1_zfmisc_1(u1_struct_0(X0))) ),
inference(resolution,[],[f340,f312]) ).
fof(f3214,plain,
! [X2,X3,X0,X1] :
( r1_filter_2(X0,X2,X1)
| ~ r1_filter_2(X0,X1,X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| ~ v1_xboole_0(X3)
| X0 = X3 ),
inference(resolution,[],[f478,f495]) ).
fof(f3377,plain,
! [X0] :
( ~ m1_subset_1(sK3,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| k3_filter_0(X0,sK3) = k3_filter_2(X0,sK3)
| v3_struct_0(X0) ),
inference(resolution,[],[f465,f312]) ).
fof(f3504,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK1))
| k18_filter_2(sK1,X0) = k2_filter_2(k1_lattice2(sK1),k5_filter_2(sK1,X0))
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1) ),
inference(resolution,[],[f485,f309]) ).
fof(f3509,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK1))
| k18_filter_2(sK1,X0) = k2_filter_2(k1_lattice2(sK1),k5_filter_2(sK1,X0))
| ~ l3_lattices(sK1) ),
inference(forward_subsumption_resolution,[],[f3504,f308]) ).
fof(f3513,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK1))
| k18_filter_2(sK1,X0) = k2_filter_2(k1_lattice2(sK1),k5_filter_2(sK1,X0)) ),
inference(forward_subsumption_resolution,[],[f3509,f307]) ).
fof(f4399,plain,
! [X0,X1] :
( v1_xboole_0(X1)
| ~ m1_subset_1(sK3,k1_zfmisc_1(u1_struct_0(k1_lattice2(X0))))
| k3_filter_2(k1_lattice2(X0),sK3) = k19_filter_2(X0,k8_filter_2(X0,sK3))
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(resolution,[],[f486,f312]) ).
fof(f4863,plain,
sK2 = k5_filter_2(sK1,sK2),
inference(resolution,[],[f2318,f310]) ).
fof(f4876,plain,
( m1_subset_1(sK2,u1_struct_0(k1_lattice2(sK1)))
| v3_struct_0(sK1)
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ m1_subset_1(sK2,u1_struct_0(sK1)) ),
inference(superposition,[],[f347,f4863]) ).
fof(f4877,plain,
( m1_subset_1(sK2,u1_struct_0(k1_lattice2(sK1)))
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ m1_subset_1(sK2,u1_struct_0(sK1)) ),
inference(forward_subsumption_resolution,[],[f4876,f309]) ).
fof(f4878,plain,
( m1_subset_1(sK2,u1_struct_0(k1_lattice2(sK1)))
| ~ l3_lattices(sK1)
| ~ m1_subset_1(sK2,u1_struct_0(sK1)) ),
inference(forward_subsumption_resolution,[],[f4877,f308]) ).
fof(f4879,plain,
( m1_subset_1(sK2,u1_struct_0(k1_lattice2(sK1)))
| ~ m1_subset_1(sK2,u1_struct_0(sK1)) ),
inference(forward_subsumption_resolution,[],[f4878,f307]) ).
fof(f4880,plain,
m1_subset_1(sK2,u1_struct_0(k1_lattice2(sK1))),
inference(forward_subsumption_resolution,[],[f4879,f310]) ).
fof(f4986,plain,
! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != k1_lattice2(sK1)
| u1_struct_0(sK1) = X0
| ~ v1_funct_1(u1_lattices(sK1))
| ~ v1_funct_2(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ m1_relset_1(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ v1_funct_1(u2_lattices(sK1))
| ~ v1_funct_2(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ m1_relset_1(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1)) ),
inference(superposition,[],[f425,f1542]) ).
fof(f4989,definition,
( spl33_308
<=> m1_relset_1(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1)) ),
introduced(definition,[new_symbols(definition,[spl33_308])],[avatar_definition]) ).
fof(f4991,plain,
( ~ m1_relset_1(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| spl33_308 ),
inference(avatar_component_clause,[],[f4989]) ).
fof(f4993,definition,
( spl33_309
<=> v1_funct_2(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1)) ),
introduced(definition,[new_symbols(definition,[spl33_309])],[avatar_definition]) ).
fof(f4995,plain,
( ~ v1_funct_2(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| spl33_309 ),
inference(avatar_component_clause,[],[f4993]) ).
fof(f4997,definition,
( spl33_310
<=> v1_funct_1(u2_lattices(sK1)) ),
introduced(definition,[new_symbols(definition,[spl33_310])],[avatar_definition]) ).
fof(f4999,plain,
( ~ v1_funct_1(u2_lattices(sK1))
| spl33_310 ),
inference(avatar_component_clause,[],[f4997]) ).
fof(f5001,definition,
( spl33_311
<=> m1_relset_1(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1)) ),
introduced(definition,[new_symbols(definition,[spl33_311])],[avatar_definition]) ).
fof(f5003,plain,
( ~ m1_relset_1(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| spl33_311 ),
inference(avatar_component_clause,[],[f5001]) ).
fof(f5005,definition,
( spl33_312
<=> v1_funct_2(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1)) ),
introduced(definition,[new_symbols(definition,[spl33_312])],[avatar_definition]) ).
fof(f5007,plain,
( ~ v1_funct_2(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| spl33_312 ),
inference(avatar_component_clause,[],[f5005]) ).
fof(f5009,definition,
( spl33_313
<=> v1_funct_1(u1_lattices(sK1)) ),
introduced(definition,[new_symbols(definition,[spl33_313])],[avatar_definition]) ).
fof(f5011,plain,
( ~ v1_funct_1(u1_lattices(sK1))
| spl33_313 ),
inference(avatar_component_clause,[],[f5009]) ).
fof(f5013,definition,
( spl33_314
<=> ! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != k1_lattice2(sK1)
| u1_struct_0(sK1) = X0 ) ),
introduced(definition,[new_symbols(definition,[spl33_314])],[avatar_definition]) ).
fof(f5014,plain,
( ! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != k1_lattice2(sK1)
| u1_struct_0(sK1) = X0 )
| ~ spl33_314 ),
inference(avatar_component_clause,[],[f5013]) ).
fof(f5015,plain,
( ~ spl33_308
| ~ spl33_309
| ~ spl33_310
| ~ spl33_311
| ~ spl33_312
| ~ spl33_313
| spl33_314 ),
inference(avatar_split_clause,[],[f4986,f5013,f5009,f5005,f5001,f4997,f4993,f4989]) ).
fof(f5030,definition,
( spl33_318
<=> l3_lattices(k1_lattice2(sK1)) ),
introduced(definition,[new_symbols(definition,[spl33_318])],[avatar_definition]) ).
fof(f5031,plain,
( ~ l3_lattices(k1_lattice2(sK1))
| spl33_318 ),
inference(avatar_component_clause,[],[f5030]) ).
fof(f5032,plain,
( l3_lattices(k1_lattice2(sK1))
| ~ spl33_318 ),
inference(avatar_component_clause,[],[f5030]) ).
fof(f5092,plain,
sK3 = k7_filter_2(sK1,sK3),
inference(resolution,[],[f2507,f311]) ).
fof(f5107,plain,
( m1_subset_1(sK3,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK1))))
| v3_struct_0(sK1)
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ m1_subset_1(sK3,k1_zfmisc_1(u1_struct_0(sK1))) ),
inference(superposition,[],[f349,f5092]) ).
fof(f5108,plain,
( m1_subset_1(sK3,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK1))))
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ m1_subset_1(sK3,k1_zfmisc_1(u1_struct_0(sK1))) ),
inference(forward_subsumption_resolution,[],[f5107,f309]) ).
fof(f5109,plain,
( m1_subset_1(sK3,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK1))))
| ~ l3_lattices(sK1)
| ~ m1_subset_1(sK3,k1_zfmisc_1(u1_struct_0(sK1))) ),
inference(forward_subsumption_resolution,[],[f5108,f308]) ).
fof(f5110,plain,
( m1_subset_1(sK3,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK1))))
| ~ m1_subset_1(sK3,k1_zfmisc_1(u1_struct_0(sK1))) ),
inference(forward_subsumption_resolution,[],[f5109,f307]) ).
fof(f5111,plain,
m1_subset_1(sK3,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK1)))),
inference(forward_subsumption_resolution,[],[f5110,f311]) ).
fof(f5232,plain,
sK3 = k8_filter_2(sK1,sK3),
inference(resolution,[],[f2608,f5111]) ).
fof(f5240,definition,
( spl33_325
<=> l1_struct_0(k1_lattice2(sK1)) ),
introduced(definition,[new_symbols(definition,[spl33_325])],[avatar_definition]) ).
fof(f5241,plain,
( l1_struct_0(k1_lattice2(sK1))
| ~ spl33_325 ),
inference(avatar_component_clause,[],[f5240]) ).
fof(f5242,plain,
( ~ l1_struct_0(k1_lattice2(sK1))
| spl33_325 ),
inference(avatar_component_clause,[],[f5240]) ).
fof(f5244,definition,
( spl33_326
<=> v3_struct_0(k1_lattice2(sK1)) ),
introduced(definition,[new_symbols(definition,[spl33_326])],[avatar_definition]) ).
fof(f5245,plain,
( ~ v3_struct_0(k1_lattice2(sK1))
| spl33_326 ),
inference(avatar_component_clause,[],[f5244]) ).
fof(f5246,plain,
( v3_struct_0(k1_lattice2(sK1))
| ~ spl33_326 ),
inference(avatar_component_clause,[],[f5244]) ).
fof(f5255,definition,
( spl33_328
<=> v10_lattices(k1_lattice2(sK1)) ),
introduced(definition,[new_symbols(definition,[spl33_328])],[avatar_definition]) ).
fof(f5256,plain,
( v10_lattices(k1_lattice2(sK1))
| ~ spl33_328 ),
inference(avatar_component_clause,[],[f5255]) ).
fof(f5257,plain,
( ~ v10_lattices(k1_lattice2(sK1))
| spl33_328 ),
inference(avatar_component_clause,[],[f5255]) ).
fof(f5267,plain,
( ~ l3_lattices(sK1)
| spl33_318 ),
inference(resolution,[],[f5031,f341]) ).
fof(f5268,plain,
( $false
| spl33_318 ),
inference(forward_subsumption_resolution,[],[f5267,f307]) ).
fof(f5269,plain,
spl33_318,
inference(avatar_contradiction_clause,[],[f5268]) ).
fof(f5271,plain,
( ~ l2_lattices(k1_lattice2(sK1))
| spl33_325 ),
inference(resolution,[],[f5242,f352]) ).
fof(f5273,plain,
( ~ sP0(sK1)
| spl33_328 ),
inference(resolution,[],[f5257,f405]) ).
fof(f5274,plain,
( v3_struct_0(sK1)
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| spl33_328 ),
inference(resolution,[],[f5273,f414]) ).
fof(f5275,plain,
( ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| spl33_328 ),
inference(forward_subsumption_resolution,[],[f5274,f309]) ).
fof(f5276,plain,
( ~ l3_lattices(sK1)
| spl33_328 ),
inference(forward_subsumption_resolution,[],[f5275,f308]) ).
fof(f5277,plain,
( $false
| spl33_328 ),
inference(forward_subsumption_resolution,[],[f5276,f307]) ).
fof(f5278,plain,
spl33_328,
inference(avatar_contradiction_clause,[],[f5277]) ).
fof(f5279,plain,
( v3_struct_0(sK1)
| ~ l3_lattices(sK1)
| ~ spl33_326 ),
inference(resolution,[],[f5246,f382]) ).
fof(f5281,plain,
( ~ l3_lattices(sK1)
| ~ spl33_326 ),
inference(forward_subsumption_resolution,[],[f5279,f309]) ).
fof(f5282,plain,
( $false
| ~ spl33_326 ),
inference(forward_subsumption_resolution,[],[f5281,f307]) ).
fof(f5283,plain,
~ spl33_326,
inference(avatar_contradiction_clause,[],[f5282]) ).
fof(f5294,plain,
( ! [X0] :
( ~ m1_filter_2(X0,k1_lattice2(sK1))
| m2_lattice4(X0,k1_lattice2(sK1))
| ~ v10_lattices(k1_lattice2(sK1))
| ~ l3_lattices(k1_lattice2(sK1)) )
| spl33_326 ),
inference(resolution,[],[f5245,f357]) ).
fof(f5304,plain,
( ! [X0] :
( ~ m1_filter_2(X0,k1_lattice2(sK1))
| m1_filter_0(X0,k1_lattice2(sK1))
| ~ v10_lattices(k1_lattice2(sK1))
| ~ l3_lattices(k1_lattice2(sK1)) )
| spl33_326 ),
inference(resolution,[],[f5245,f467]) ).
fof(f5321,plain,
( ! [X0] :
( ~ m1_filter_2(X0,k1_lattice2(sK1))
| m1_filter_0(X0,k1_lattice2(sK1))
| ~ l3_lattices(k1_lattice2(sK1)) )
| spl33_326
| ~ spl33_328 ),
inference(forward_subsumption_resolution,[],[f5304,f5256]) ).
fof(f5331,plain,
( ! [X0] :
( ~ m1_filter_2(X0,k1_lattice2(sK1))
| m2_lattice4(X0,k1_lattice2(sK1))
| ~ l3_lattices(k1_lattice2(sK1)) )
| spl33_326
| ~ spl33_328 ),
inference(forward_subsumption_resolution,[],[f5294,f5256]) ).
fof(f5374,plain,
( ! [X0] :
( ~ m1_filter_2(X0,k1_lattice2(sK1))
| m1_filter_0(X0,k1_lattice2(sK1)) )
| ~ spl33_318
| spl33_326
| ~ spl33_328 ),
inference(forward_subsumption_resolution,[],[f5321,f5032]) ).
fof(f5384,plain,
( ! [X0] :
( m2_lattice4(X0,k1_lattice2(sK1))
| ~ m1_filter_2(X0,k1_lattice2(sK1)) )
| ~ spl33_318
| spl33_326
| ~ spl33_328 ),
inference(forward_subsumption_resolution,[],[f5331,f5032]) ).
fof(f5409,plain,
( ~ l3_lattices(k1_lattice2(sK1))
| spl33_325 ),
inference(resolution,[],[f5271,f353]) ).
fof(f5410,plain,
( $false
| ~ spl33_318
| spl33_325 ),
inference(forward_subsumption_resolution,[],[f5409,f5032]) ).
fof(f5411,plain,
( ~ spl33_318
| spl33_325 ),
inference(avatar_contradiction_clause,[],[f5410]) ).
fof(f5588,plain,
k18_filter_2(sK1,sK2) = k2_filter_2(k1_lattice2(sK1),k5_filter_2(sK1,sK2)),
inference(resolution,[],[f3513,f310]) ).
fof(f5601,plain,
k18_filter_2(sK1,sK2) = k2_filter_2(k1_lattice2(sK1),sK2),
inference(forward_demodulation,[],[f5588,f4863]) ).
fof(f6448,plain,
( ~ v10_lattices(k1_lattice2(sK1))
| ~ l3_lattices(k1_lattice2(sK1))
| k3_filter_0(k1_lattice2(sK1),sK3) = k3_filter_2(k1_lattice2(sK1),sK3)
| v3_struct_0(k1_lattice2(sK1)) ),
inference(resolution,[],[f3377,f5111]) ).
fof(f6455,plain,
( ~ l3_lattices(k1_lattice2(sK1))
| k3_filter_0(k1_lattice2(sK1),sK3) = k3_filter_2(k1_lattice2(sK1),sK3)
| v3_struct_0(k1_lattice2(sK1))
| ~ spl33_328 ),
inference(forward_subsumption_resolution,[],[f6448,f5256]) ).
fof(f6459,plain,
( k3_filter_0(k1_lattice2(sK1),sK3) = k3_filter_2(k1_lattice2(sK1),sK3)
| v3_struct_0(k1_lattice2(sK1))
| ~ spl33_318
| ~ spl33_328 ),
inference(forward_subsumption_resolution,[],[f6455,f5032]) ).
fof(f6463,plain,
( k3_filter_0(k1_lattice2(sK1),sK3) = k3_filter_2(k1_lattice2(sK1),sK3)
| ~ spl33_318
| spl33_326
| ~ spl33_328 ),
inference(forward_subsumption_resolution,[],[f6459,f5245]) ).
fof(f6656,plain,
! [X0] :
( ~ m1_subset_1(sK3,k1_zfmisc_1(u1_struct_0(k1_lattice2(X0))))
| k3_filter_2(k1_lattice2(X0),sK3) = k19_filter_2(X0,k8_filter_2(X0,sK3))
| ~ m1_subset_1(sK3,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(resolution,[],[f4399,f312]) ).
fof(f7640,definition,
( spl33_441
<=> m1_subset_1(k19_filter_2(sK1,sK3),k1_zfmisc_1(u1_struct_0(sK1))) ),
introduced(definition,[new_symbols(definition,[spl33_441])],[avatar_definition]) ).
fof(f7641,plain,
( m1_subset_1(k19_filter_2(sK1,sK3),k1_zfmisc_1(u1_struct_0(sK1)))
| ~ spl33_441 ),
inference(avatar_component_clause,[],[f7640]) ).
fof(f7642,plain,
( ~ m1_subset_1(k19_filter_2(sK1,sK3),k1_zfmisc_1(u1_struct_0(sK1)))
| spl33_441 ),
inference(avatar_component_clause,[],[f7640]) ).
fof(f7648,plain,
( ~ m2_lattice4(k19_filter_2(sK1,sK3),sK1)
| spl33_441 ),
inference(resolution,[],[f7642,f2262]) ).
fof(f7652,plain,
( ~ m2_filter_2(k19_filter_2(sK1,sK3),sK1)
| spl33_441 ),
inference(resolution,[],[f7648,f1675]) ).
fof(f7654,plain,
( ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| v3_struct_0(sK1)
| ~ m1_subset_1(sK3,k1_zfmisc_1(u1_struct_0(sK1)))
| spl33_441 ),
inference(resolution,[],[f7652,f2987]) ).
fof(f7655,plain,
( ~ l3_lattices(sK1)
| v3_struct_0(sK1)
| ~ m1_subset_1(sK3,k1_zfmisc_1(u1_struct_0(sK1)))
| spl33_441 ),
inference(forward_subsumption_resolution,[],[f7654,f308]) ).
fof(f7656,plain,
( v3_struct_0(sK1)
| ~ m1_subset_1(sK3,k1_zfmisc_1(u1_struct_0(sK1)))
| spl33_441 ),
inference(forward_subsumption_resolution,[],[f7655,f307]) ).
fof(f7657,plain,
( ~ m1_subset_1(sK3,k1_zfmisc_1(u1_struct_0(sK1)))
| spl33_441 ),
inference(forward_subsumption_resolution,[],[f7656,f309]) ).
fof(f7658,plain,
( $false
| spl33_441 ),
inference(forward_subsumption_resolution,[],[f7657,f311]) ).
fof(f7659,plain,
spl33_441,
inference(avatar_contradiction_clause,[],[f7658]) ).
fof(f11717,plain,
! [X0] :
( ~ v1_xboole_0(X0)
| k6_domain_1(u1_struct_0(sK1),sK2) = k1_tarski(sK2)
| u1_struct_0(sK1) = X0 ),
inference(resolution,[],[f1428,f310]) ).
fof(f11718,plain,
! [X0] :
( ~ v1_xboole_0(X0)
| k1_tarski(sK2) = k6_domain_1(u1_struct_0(k1_lattice2(sK1)),sK2)
| u1_struct_0(k1_lattice2(sK1)) = X0 ),
inference(resolution,[],[f1428,f4880]) ).
fof(f11760,definition,
( spl33_684
<=> ! [X0] :
( ~ v1_xboole_0(X0)
| u1_struct_0(k1_lattice2(sK1)) = X0 ) ),
introduced(definition,[new_symbols(definition,[spl33_684])],[avatar_definition]) ).
fof(f11761,plain,
( ! [X0] :
( ~ v1_xboole_0(X0)
| u1_struct_0(k1_lattice2(sK1)) = X0 )
| ~ spl33_684 ),
inference(avatar_component_clause,[],[f11760]) ).
fof(f11781,definition,
( spl33_689
<=> ! [X0] :
( ~ v1_xboole_0(X0)
| u1_struct_0(sK1) = X0 ) ),
introduced(definition,[new_symbols(definition,[spl33_689])],[avatar_definition]) ).
fof(f11782,plain,
( ! [X0] :
( ~ v1_xboole_0(X0)
| u1_struct_0(sK1) = X0 )
| ~ spl33_689 ),
inference(avatar_component_clause,[],[f11781]) ).
fof(f11785,definition,
( spl33_690
<=> k1_tarski(sK2) = k6_domain_1(u1_struct_0(k1_lattice2(sK1)),sK2) ),
introduced(definition,[new_symbols(definition,[spl33_690])],[avatar_definition]) ).
fof(f11787,plain,
( k1_tarski(sK2) = k6_domain_1(u1_struct_0(k1_lattice2(sK1)),sK2)
| ~ spl33_690 ),
inference(avatar_component_clause,[],[f11785]) ).
fof(f11788,plain,
( spl33_690
| spl33_684 ),
inference(avatar_split_clause,[],[f11718,f11760,f11785]) ).
fof(f11790,definition,
( spl33_691
<=> k6_domain_1(u1_struct_0(sK1),sK2) = k1_tarski(sK2) ),
introduced(definition,[new_symbols(definition,[spl33_691])],[avatar_definition]) ).
fof(f11792,plain,
( k6_domain_1(u1_struct_0(sK1),sK2) = k1_tarski(sK2)
| ~ spl33_691 ),
inference(avatar_component_clause,[],[f11790]) ).
fof(f11793,plain,
( spl33_691
| spl33_689 ),
inference(avatar_split_clause,[],[f11717,f11781,f11790]) ).
fof(f11868,plain,
( u1_struct_0(sK1) = sK22
| ~ spl33_689 ),
inference(resolution,[],[f11782,f436]) ).
fof(f12089,plain,
( ~ v1_xboole_0(sK22)
| v3_struct_0(sK1)
| ~ l1_struct_0(sK1)
| ~ spl33_689 ),
inference(superposition,[],[f383,f11868]) ).
fof(f12100,definition,
( spl33_692
<=> l2_lattices(sK1) ),
introduced(definition,[new_symbols(definition,[spl33_692])],[avatar_definition]) ).
fof(f12101,plain,
( l2_lattices(sK1)
| ~ spl33_692 ),
inference(avatar_component_clause,[],[f12100]) ).
fof(f12102,plain,
( ~ l2_lattices(sK1)
| spl33_692 ),
inference(avatar_component_clause,[],[f12100]) ).
fof(f12109,definition,
( spl33_694
<=> l1_lattices(sK1) ),
introduced(definition,[new_symbols(definition,[spl33_694])],[avatar_definition]) ).
fof(f12110,plain,
( l1_lattices(sK1)
| ~ spl33_694 ),
inference(avatar_component_clause,[],[f12109]) ).
fof(f12111,plain,
( ~ l1_lattices(sK1)
| spl33_694 ),
inference(avatar_component_clause,[],[f12109]) ).
fof(f12121,plain,
( v3_struct_0(sK1)
| ~ l1_struct_0(sK1)
| ~ spl33_689 ),
inference(forward_subsumption_resolution,[],[f12089,f436]) ).
fof(f12168,plain,
( ~ l1_struct_0(sK1)
| ~ spl33_689 ),
inference(forward_subsumption_resolution,[],[f12121,f309]) ).
fof(f12173,plain,
( $false
| ~ spl33_99
| ~ spl33_689 ),
inference(forward_subsumption_resolution,[],[f12168,f1706]) ).
fof(f12174,plain,
( ~ spl33_99
| ~ spl33_689 ),
inference(avatar_contradiction_clause,[],[f12173]) ).
fof(f12276,plain,
( m1_subset_1(k1_tarski(sK2),k1_zfmisc_1(u1_struct_0(sK1)))
| v1_xboole_0(u1_struct_0(sK1))
| ~ m1_subset_1(sK2,u1_struct_0(sK1))
| ~ spl33_691 ),
inference(superposition,[],[f348,f11792]) ).
fof(f12277,plain,
( m1_subset_1(k1_tarski(sK2),k1_zfmisc_1(u1_struct_0(sK1)))
| ~ m1_subset_1(sK2,u1_struct_0(sK1))
| spl33_23
| ~ spl33_691 ),
inference(forward_subsumption_resolution,[],[f12276,f728]) ).
fof(f12279,plain,
( m1_subset_1(k1_tarski(sK2),k1_zfmisc_1(u1_struct_0(sK1)))
| spl33_23
| ~ spl33_691 ),
inference(forward_subsumption_resolution,[],[f12277,f310]) ).
fof(f12289,plain,
( k1_tarski(sK2) = k7_filter_2(sK1,k1_tarski(sK2))
| spl33_23
| ~ spl33_691 ),
inference(resolution,[],[f12279,f2507]) ).
fof(f12437,plain,
( sK22 = u1_struct_0(k1_lattice2(sK1))
| ~ spl33_684 ),
inference(resolution,[],[f11761,f436]) ).
fof(f12501,plain,
( ~ v1_xboole_0(sK22)
| v3_struct_0(k1_lattice2(sK1))
| ~ l1_struct_0(k1_lattice2(sK1))
| ~ spl33_684 ),
inference(superposition,[],[f383,f12437]) ).
fof(f12532,plain,
( v3_struct_0(k1_lattice2(sK1))
| ~ l1_struct_0(k1_lattice2(sK1))
| ~ spl33_684 ),
inference(forward_subsumption_resolution,[],[f12501,f436]) ).
fof(f12564,plain,
( ~ l1_struct_0(k1_lattice2(sK1))
| spl33_326
| ~ spl33_684 ),
inference(forward_subsumption_resolution,[],[f12532,f5245]) ).
fof(f12572,plain,
( $false
| ~ spl33_325
| spl33_326
| ~ spl33_684 ),
inference(forward_subsumption_resolution,[],[f12564,f5241]) ).
fof(f12573,plain,
( ~ spl33_325
| spl33_326
| ~ spl33_684 ),
inference(avatar_contradiction_clause,[],[f12572]) ).
fof(f12592,plain,
( m1_subset_1(k1_tarski(sK2),k1_zfmisc_1(u1_struct_0(k1_lattice2(sK1))))
| v3_struct_0(sK1)
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ m1_subset_1(k1_tarski(sK2),k1_zfmisc_1(u1_struct_0(sK1)))
| spl33_23
| ~ spl33_691 ),
inference(superposition,[],[f349,f12289]) ).
fof(f12593,plain,
( m1_subset_1(k1_tarski(sK2),k1_zfmisc_1(u1_struct_0(k1_lattice2(sK1))))
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ m1_subset_1(k1_tarski(sK2),k1_zfmisc_1(u1_struct_0(sK1)))
| spl33_23
| ~ spl33_691 ),
inference(forward_subsumption_resolution,[],[f12592,f309]) ).
fof(f12594,plain,
( m1_subset_1(k1_tarski(sK2),k1_zfmisc_1(u1_struct_0(k1_lattice2(sK1))))
| ~ l3_lattices(sK1)
| ~ m1_subset_1(k1_tarski(sK2),k1_zfmisc_1(u1_struct_0(sK1)))
| spl33_23
| ~ spl33_691 ),
inference(forward_subsumption_resolution,[],[f12593,f308]) ).
fof(f12595,plain,
( m1_subset_1(k1_tarski(sK2),k1_zfmisc_1(u1_struct_0(k1_lattice2(sK1))))
| ~ m1_subset_1(k1_tarski(sK2),k1_zfmisc_1(u1_struct_0(sK1)))
| spl33_23
| ~ spl33_691 ),
inference(forward_subsumption_resolution,[],[f12594,f307]) ).
fof(f12596,plain,
( m1_subset_1(k1_tarski(sK2),k1_zfmisc_1(u1_struct_0(k1_lattice2(sK1))))
| spl33_23
| ~ spl33_691 ),
inference(forward_subsumption_resolution,[],[f12595,f12279]) ).
fof(f12611,plain,
( v1_xboole_0(k1_tarski(sK2))
| k2_filter_0(k1_lattice2(sK1),sK2) = k3_filter_0(k1_lattice2(sK1),k1_tarski(sK2))
| ~ m1_subset_1(k1_tarski(sK2),k1_zfmisc_1(u1_struct_0(k1_lattice2(sK1))))
| ~ m1_subset_1(sK2,u1_struct_0(k1_lattice2(sK1)))
| v3_struct_0(k1_lattice2(sK1))
| ~ v10_lattices(k1_lattice2(sK1))
| ~ l3_lattices(k1_lattice2(sK1))
| ~ spl33_690 ),
inference(superposition,[],[f499,f11787]) ).
fof(f12613,plain,
( k2_filter_0(k1_lattice2(sK1),sK2) = k3_filter_0(k1_lattice2(sK1),k1_tarski(sK2))
| ~ m1_subset_1(k1_tarski(sK2),k1_zfmisc_1(u1_struct_0(k1_lattice2(sK1))))
| ~ m1_subset_1(sK2,u1_struct_0(k1_lattice2(sK1)))
| v3_struct_0(k1_lattice2(sK1))
| ~ v10_lattices(k1_lattice2(sK1))
| ~ l3_lattices(k1_lattice2(sK1))
| ~ spl33_690 ),
inference(forward_subsumption_resolution,[],[f12611,f397]) ).
fof(f12614,plain,
( k2_filter_0(k1_lattice2(sK1),sK2) = k3_filter_0(k1_lattice2(sK1),k1_tarski(sK2))
| ~ m1_subset_1(sK2,u1_struct_0(k1_lattice2(sK1)))
| v3_struct_0(k1_lattice2(sK1))
| ~ v10_lattices(k1_lattice2(sK1))
| ~ l3_lattices(k1_lattice2(sK1))
| spl33_23
| ~ spl33_690
| ~ spl33_691 ),
inference(forward_subsumption_resolution,[],[f12613,f12596]) ).
fof(f12615,plain,
( k2_filter_0(k1_lattice2(sK1),sK2) = k3_filter_0(k1_lattice2(sK1),k1_tarski(sK2))
| v3_struct_0(k1_lattice2(sK1))
| ~ v10_lattices(k1_lattice2(sK1))
| ~ l3_lattices(k1_lattice2(sK1))
| spl33_23
| ~ spl33_690
| ~ spl33_691 ),
inference(forward_subsumption_resolution,[],[f12614,f4880]) ).
fof(f12616,plain,
( k2_filter_0(k1_lattice2(sK1),sK2) = k3_filter_0(k1_lattice2(sK1),k1_tarski(sK2))
| ~ v10_lattices(k1_lattice2(sK1))
| ~ l3_lattices(k1_lattice2(sK1))
| spl33_23
| spl33_326
| ~ spl33_690
| ~ spl33_691 ),
inference(forward_subsumption_resolution,[],[f12615,f5245]) ).
fof(f12617,plain,
( k2_filter_0(k1_lattice2(sK1),sK2) = k3_filter_0(k1_lattice2(sK1),k1_tarski(sK2))
| ~ l3_lattices(k1_lattice2(sK1))
| spl33_23
| spl33_326
| ~ spl33_328
| ~ spl33_690
| ~ spl33_691 ),
inference(forward_subsumption_resolution,[],[f12616,f5256]) ).
fof(f12618,plain,
( k2_filter_0(k1_lattice2(sK1),sK2) = k3_filter_0(k1_lattice2(sK1),k1_tarski(sK2))
| spl33_23
| ~ spl33_318
| spl33_326
| ~ spl33_328
| ~ spl33_690
| ~ spl33_691 ),
inference(forward_subsumption_resolution,[],[f12617,f5032]) ).
fof(f12836,plain,
k1_lattice2(sK1) = g3_lattices(u1_struct_0(k1_lattice2(sK1)),u2_lattices(k1_lattice2(sK1)),u1_lattices(k1_lattice2(sK1))),
inference(resolution,[],[f2047,f307]) ).
fof(f12923,definition,
( spl33_739
<=> sP0(sK1) ),
introduced(definition,[new_symbols(definition,[spl33_739])],[avatar_definition]) ).
fof(f12924,plain,
( sP0(sK1)
| ~ spl33_739 ),
inference(avatar_component_clause,[],[f12923]) ).
fof(f12925,plain,
( ~ sP0(sK1)
| spl33_739 ),
inference(avatar_component_clause,[],[f12923]) ).
fof(f12947,plain,
( v3_struct_0(sK1)
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| spl33_739 ),
inference(resolution,[],[f12925,f414]) ).
fof(f12948,plain,
( ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| spl33_739 ),
inference(forward_subsumption_resolution,[],[f12947,f309]) ).
fof(f12949,plain,
( ~ l3_lattices(sK1)
| spl33_739 ),
inference(forward_subsumption_resolution,[],[f12948,f308]) ).
fof(f12950,plain,
( $false
| spl33_739 ),
inference(forward_subsumption_resolution,[],[f12949,f307]) ).
fof(f12951,plain,
spl33_739,
inference(avatar_contradiction_clause,[],[f12950]) ).
fof(f12970,plain,
! [X0] :
( ~ m2_lattice4(X0,k1_lattice2(sK1))
| ~ l3_lattices(k1_lattice2(sK1))
| ~ sP0(sK1)
| k8_filter_2(sK1,X0) = X0 ),
inference(resolution,[],[f2259,f2608]) ).
fof(f13000,plain,
( ! [X0] :
( ~ m2_lattice4(X0,k1_lattice2(sK1))
| ~ sP0(sK1)
| k8_filter_2(sK1,X0) = X0 )
| ~ spl33_318 ),
inference(forward_subsumption_resolution,[],[f12970,f5032]) ).
fof(f13010,plain,
( ! [X0] :
( ~ m2_lattice4(X0,k1_lattice2(sK1))
| k8_filter_2(sK1,X0) = X0 )
| ~ spl33_318
| ~ spl33_739 ),
inference(forward_subsumption_resolution,[],[f13000,f12924]) ).
fof(f13118,plain,
( ! [X0] :
( ~ m1_filter_2(X0,k1_lattice2(sK1))
| k8_filter_2(sK1,X0) = X0 )
| ~ spl33_318
| spl33_326
| ~ spl33_328
| ~ spl33_739 ),
inference(resolution,[],[f13010,f5384]) ).
fof(f15957,plain,
( m1_filter_2(k18_filter_2(sK1,sK2),k1_lattice2(sK1))
| ~ l3_lattices(k1_lattice2(sK1))
| ~ m1_subset_1(sK2,u1_struct_0(k1_lattice2(sK1)))
| ~ sP0(sK1) ),
inference(superposition,[],[f2455,f5601]) ).
fof(f15960,plain,
( m1_filter_2(k18_filter_2(sK1,sK2),k1_lattice2(sK1))
| ~ m1_subset_1(sK2,u1_struct_0(k1_lattice2(sK1)))
| ~ sP0(sK1)
| ~ spl33_318 ),
inference(forward_subsumption_resolution,[],[f15957,f5032]) ).
fof(f15964,plain,
( m1_filter_2(k18_filter_2(sK1,sK2),k1_lattice2(sK1))
| ~ sP0(sK1)
| ~ spl33_318 ),
inference(forward_subsumption_resolution,[],[f15960,f4880]) ).
fof(f15968,plain,
( m1_filter_2(k18_filter_2(sK1,sK2),k1_lattice2(sK1))
| ~ spl33_318
| ~ spl33_739 ),
inference(forward_subsumption_resolution,[],[f15964,f12924]) ).
fof(f15969,plain,
( k18_filter_2(sK1,sK2) = k8_filter_2(sK1,k18_filter_2(sK1,sK2))
| ~ spl33_318
| spl33_326
| ~ spl33_328
| ~ spl33_739 ),
inference(resolution,[],[f15968,f13118]) ).
fof(f15970,plain,
( m1_filter_0(k18_filter_2(sK1,sK2),k1_lattice2(sK1))
| ~ spl33_318
| spl33_326
| ~ spl33_328
| ~ spl33_739 ),
inference(resolution,[],[f15968,f5374]) ).
fof(f16005,plain,
( m1_subset_1(k18_filter_2(sK1,sK2),k1_zfmisc_1(u1_struct_0(sK1)))
| v3_struct_0(sK1)
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ m1_subset_1(k18_filter_2(sK1,sK2),k1_zfmisc_1(u1_struct_0(k1_lattice2(sK1))))
| ~ spl33_318
| spl33_326
| ~ spl33_328
| ~ spl33_739 ),
inference(superposition,[],[f350,f15969]) ).
fof(f16006,plain,
( m1_subset_1(k18_filter_2(sK1,sK2),k1_zfmisc_1(u1_struct_0(sK1)))
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ m1_subset_1(k18_filter_2(sK1,sK2),k1_zfmisc_1(u1_struct_0(k1_lattice2(sK1))))
| ~ spl33_318
| spl33_326
| ~ spl33_328
| ~ spl33_739 ),
inference(forward_subsumption_resolution,[],[f16005,f309]) ).
fof(f16007,plain,
( m1_subset_1(k18_filter_2(sK1,sK2),k1_zfmisc_1(u1_struct_0(sK1)))
| ~ l3_lattices(sK1)
| ~ m1_subset_1(k18_filter_2(sK1,sK2),k1_zfmisc_1(u1_struct_0(k1_lattice2(sK1))))
| ~ spl33_318
| spl33_326
| ~ spl33_328
| ~ spl33_739 ),
inference(forward_subsumption_resolution,[],[f16006,f308]) ).
fof(f16008,plain,
( m1_subset_1(k18_filter_2(sK1,sK2),k1_zfmisc_1(u1_struct_0(sK1)))
| ~ m1_subset_1(k18_filter_2(sK1,sK2),k1_zfmisc_1(u1_struct_0(k1_lattice2(sK1))))
| ~ spl33_318
| spl33_326
| ~ spl33_328
| ~ spl33_739 ),
inference(forward_subsumption_resolution,[],[f16007,f307]) ).
fof(f16010,definition,
( spl33_973
<=> m1_subset_1(k18_filter_2(sK1,sK2),k1_zfmisc_1(u1_struct_0(k1_lattice2(sK1)))) ),
introduced(definition,[new_symbols(definition,[spl33_973])],[avatar_definition]) ).
fof(f16012,plain,
( ~ m1_subset_1(k18_filter_2(sK1,sK2),k1_zfmisc_1(u1_struct_0(k1_lattice2(sK1))))
| spl33_973 ),
inference(avatar_component_clause,[],[f16010]) ).
fof(f16014,definition,
( spl33_974
<=> m1_subset_1(k18_filter_2(sK1,sK2),k1_zfmisc_1(u1_struct_0(sK1))) ),
introduced(definition,[new_symbols(definition,[spl33_974])],[avatar_definition]) ).
fof(f16016,plain,
( m1_subset_1(k18_filter_2(sK1,sK2),k1_zfmisc_1(u1_struct_0(sK1)))
| ~ spl33_974 ),
inference(avatar_component_clause,[],[f16014]) ).
fof(f16017,plain,
( ~ spl33_973
| spl33_974
| ~ spl33_318
| spl33_326
| ~ spl33_328
| ~ spl33_739 ),
inference(avatar_split_clause,[],[f16008,f12923,f5255,f5244,f5030,f16014,f16010]) ).
fof(f16019,plain,
( ~ m1_filter_0(k18_filter_2(sK1,sK2),k1_lattice2(sK1))
| ~ l3_lattices(k1_lattice2(sK1))
| ~ sP0(sK1)
| spl33_973 ),
inference(resolution,[],[f16012,f2204]) ).
fof(f16022,plain,
( ~ l3_lattices(k1_lattice2(sK1))
| ~ sP0(sK1)
| ~ spl33_318
| spl33_326
| ~ spl33_328
| ~ spl33_739
| spl33_973 ),
inference(forward_subsumption_resolution,[],[f16019,f15970]) ).
fof(f16024,plain,
( ~ sP0(sK1)
| ~ spl33_318
| spl33_326
| ~ spl33_328
| ~ spl33_739
| spl33_973 ),
inference(forward_subsumption_resolution,[],[f16022,f5032]) ).
fof(f16026,plain,
( $false
| ~ spl33_318
| spl33_326
| ~ spl33_328
| ~ spl33_739
| spl33_973 ),
inference(forward_subsumption_resolution,[],[f16024,f12924]) ).
fof(f16027,plain,
( ~ spl33_318
| spl33_326
| ~ spl33_328
| ~ spl33_739
| spl33_973 ),
inference(avatar_contradiction_clause,[],[f16026]) ).
fof(f18355,plain,
( k2_filter_0(k1_lattice2(sK1),sK2) = a_2_0_filter_0(k1_lattice2(sK1),sK2)
| ~ l3_lattices(k1_lattice2(sK1))
| ~ sP0(sK1) ),
inference(resolution,[],[f2568,f4880]) ).
fof(f18375,plain,
( k2_filter_0(k1_lattice2(sK1),sK2) = a_2_0_filter_0(k1_lattice2(sK1),sK2)
| ~ sP0(sK1)
| ~ spl33_318 ),
inference(forward_subsumption_resolution,[],[f18355,f5032]) ).
fof(f18385,plain,
( k2_filter_0(k1_lattice2(sK1),sK2) = a_2_0_filter_0(k1_lattice2(sK1),sK2)
| ~ spl33_318
| ~ spl33_739 ),
inference(forward_subsumption_resolution,[],[f18375,f12924]) ).
fof(f18655,plain,
( ~ l3_lattices(k1_lattice2(sK1))
| k2_filter_2(k1_lattice2(sK1),sK2) = k2_filter_0(k1_lattice2(sK1),sK2)
| ~ sP0(sK1) ),
inference(resolution,[],[f2822,f4880]) ).
fof(f18677,plain,
( k2_filter_2(k1_lattice2(sK1),sK2) = k2_filter_0(k1_lattice2(sK1),sK2)
| ~ sP0(sK1)
| ~ spl33_318 ),
inference(forward_subsumption_resolution,[],[f18655,f5032]) ).
fof(f18688,plain,
( k2_filter_2(k1_lattice2(sK1),sK2) = k2_filter_0(k1_lattice2(sK1),sK2)
| ~ spl33_318
| ~ spl33_739 ),
inference(forward_subsumption_resolution,[],[f18677,f12924]) ).
fof(f18697,plain,
( k2_filter_2(k1_lattice2(sK1),sK2) = a_2_0_filter_0(k1_lattice2(sK1),sK2)
| ~ spl33_318
| ~ spl33_739 ),
inference(forward_demodulation,[],[f18688,f18385]) ).
fof(f18699,plain,
( k18_filter_2(sK1,sK2) = a_2_0_filter_0(k1_lattice2(sK1),sK2)
| ~ spl33_318
| ~ spl33_739 ),
inference(forward_demodulation,[],[f18697,f5601]) ).
fof(f18931,plain,
! [X0] :
( ~ v1_xboole_0(X0)
| ~ m1_subset_1(sK3,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ m1_subset_1(k6_domain_1(u1_struct_0(sK1),sK2),k1_zfmisc_1(u1_struct_0(sK1)))
| sK3 = k6_domain_1(u1_struct_0(sK1),sK2)
| u1_struct_0(sK1) = X0 ),
inference(resolution,[],[f2860,f313]) ).
fof(f18955,plain,
! [X0] :
( ~ v1_xboole_0(X0)
| ~ m1_subset_1(k6_domain_1(u1_struct_0(sK1),sK2),k1_zfmisc_1(u1_struct_0(sK1)))
| sK3 = k6_domain_1(u1_struct_0(sK1),sK2)
| u1_struct_0(sK1) = X0 ),
inference(forward_subsumption_resolution,[],[f18931,f311]) ).
fof(f18958,plain,
( ! [X0] :
( ~ m1_subset_1(k1_tarski(sK2),k1_zfmisc_1(u1_struct_0(sK1)))
| ~ v1_xboole_0(X0)
| sK3 = k6_domain_1(u1_struct_0(sK1),sK2)
| u1_struct_0(sK1) = X0 )
| ~ spl33_691 ),
inference(forward_demodulation,[],[f18955,f11792]) ).
fof(f18961,definition,
( spl33_1120
<=> sK3 = k1_tarski(sK2) ),
introduced(definition,[new_symbols(definition,[spl33_1120])],[avatar_definition]) ).
fof(f18963,plain,
( sK3 = k1_tarski(sK2)
| ~ spl33_1120 ),
inference(avatar_component_clause,[],[f18961]) ).
fof(f18965,plain,
( ! [X0] :
( ~ v1_xboole_0(X0)
| sK3 = k6_domain_1(u1_struct_0(sK1),sK2)
| u1_struct_0(sK1) = X0 )
| spl33_23
| ~ spl33_691 ),
inference(forward_subsumption_resolution,[],[f18958,f12279]) ).
fof(f18966,plain,
( ! [X0] :
( sK3 = k1_tarski(sK2)
| ~ v1_xboole_0(X0)
| u1_struct_0(sK1) = X0 )
| spl33_23
| ~ spl33_691 ),
inference(forward_demodulation,[],[f18965,f11792]) ).
fof(f18967,plain,
( spl33_689
| spl33_1120
| spl33_23
| ~ spl33_691 ),
inference(avatar_split_clause,[],[f18966,f11790,f726,f18961,f11781]) ).
fof(f20607,plain,
! [X0] :
( ~ r1_filter_2(u1_struct_0(sK1),k18_filter_2(sK1,sK2),k19_filter_2(sK1,sK3))
| ~ m1_subset_1(k18_filter_2(sK1,sK2),k1_zfmisc_1(u1_struct_0(sK1)))
| ~ m1_subset_1(k19_filter_2(sK1,sK3),k1_zfmisc_1(u1_struct_0(sK1)))
| ~ v1_xboole_0(X0)
| u1_struct_0(sK1) = X0 ),
inference(resolution,[],[f3214,f314]) ).
fof(f20621,plain,
( ! [X0] :
( ~ r1_filter_2(u1_struct_0(sK1),k18_filter_2(sK1,sK2),k19_filter_2(sK1,sK3))
| ~ m1_subset_1(k19_filter_2(sK1,sK3),k1_zfmisc_1(u1_struct_0(sK1)))
| ~ v1_xboole_0(X0)
| u1_struct_0(sK1) = X0 )
| ~ spl33_974 ),
inference(forward_subsumption_resolution,[],[f20607,f16016]) ).
fof(f20622,plain,
( ! [X0] :
( ~ r1_filter_2(u1_struct_0(sK1),k18_filter_2(sK1,sK2),k19_filter_2(sK1,sK3))
| ~ v1_xboole_0(X0)
| u1_struct_0(sK1) = X0 )
| ~ spl33_441
| ~ spl33_974 ),
inference(forward_subsumption_resolution,[],[f20621,f7641]) ).
fof(f20624,definition,
( spl33_1177
<=> r1_filter_2(u1_struct_0(sK1),k18_filter_2(sK1,sK2),k19_filter_2(sK1,sK3)) ),
introduced(definition,[new_symbols(definition,[spl33_1177])],[avatar_definition]) ).
fof(f20626,plain,
( ~ r1_filter_2(u1_struct_0(sK1),k18_filter_2(sK1,sK2),k19_filter_2(sK1,sK3))
| spl33_1177 ),
inference(avatar_component_clause,[],[f20624]) ).
fof(f20627,plain,
( spl33_689
| ~ spl33_1177
| ~ spl33_441
| ~ spl33_974 ),
inference(avatar_split_clause,[],[f20622,f16014,f7640,f20624,f11781]) ).
fof(f35911,plain,
( ~ l2_lattices(sK1)
| spl33_308 ),
inference(resolution,[],[f4991,f1810]) ).
fof(f35912,plain,
( ~ spl33_692
| spl33_308 ),
inference(avatar_split_clause,[],[f35911,f4989,f12100]) ).
fof(f35913,plain,
( ~ l3_lattices(sK1)
| spl33_692 ),
inference(resolution,[],[f12102,f353]) ).
fof(f35914,plain,
( $false
| spl33_692 ),
inference(forward_subsumption_resolution,[],[f35913,f307]) ).
fof(f35915,plain,
spl33_692,
inference(avatar_contradiction_clause,[],[f35914]) ).
fof(f35975,plain,
( ~ l2_lattices(sK1)
| spl33_309 ),
inference(resolution,[],[f4995,f367]) ).
fof(f35976,plain,
( $false
| spl33_309
| ~ spl33_692 ),
inference(forward_subsumption_resolution,[],[f35975,f12101]) ).
fof(f35977,plain,
( spl33_309
| ~ spl33_692 ),
inference(avatar_contradiction_clause,[],[f35976]) ).
fof(f35978,plain,
( ~ l2_lattices(sK1)
| spl33_310 ),
inference(resolution,[],[f4999,f368]) ).
fof(f35980,plain,
( $false
| spl33_310
| ~ spl33_692 ),
inference(forward_subsumption_resolution,[],[f35978,f12101]) ).
fof(f35981,plain,
( spl33_310
| ~ spl33_692 ),
inference(avatar_contradiction_clause,[],[f35980]) ).
fof(f36080,plain,
( ~ l1_lattices(sK1)
| spl33_311 ),
inference(resolution,[],[f5003,f1730]) ).
fof(f36081,plain,
( ~ spl33_694
| spl33_311 ),
inference(avatar_split_clause,[],[f36080,f5001,f12109]) ).
fof(f36082,plain,
( ~ l3_lattices(sK1)
| spl33_694 ),
inference(resolution,[],[f12111,f354]) ).
fof(f36083,plain,
( $false
| spl33_694 ),
inference(forward_subsumption_resolution,[],[f36082,f307]) ).
fof(f36084,plain,
spl33_694,
inference(avatar_contradiction_clause,[],[f36083]) ).
fof(f36160,plain,
( ~ l1_lattices(sK1)
| spl33_312 ),
inference(resolution,[],[f5007,f364]) ).
fof(f36161,plain,
( $false
| spl33_312
| ~ spl33_694 ),
inference(forward_subsumption_resolution,[],[f36160,f12110]) ).
fof(f36162,plain,
( spl33_312
| ~ spl33_694 ),
inference(avatar_contradiction_clause,[],[f36161]) ).
fof(f36163,plain,
( ~ l1_lattices(sK1)
| spl33_313 ),
inference(resolution,[],[f5011,f365]) ).
fof(f36165,plain,
( $false
| spl33_313
| ~ spl33_694 ),
inference(forward_subsumption_resolution,[],[f36163,f12110]) ).
fof(f36166,plain,
( spl33_313
| ~ spl33_694 ),
inference(avatar_contradiction_clause,[],[f36165]) ).
fof(f39524,plain,
( k1_lattice2(sK1) != k1_lattice2(sK1)
| u1_struct_0(sK1) = u1_struct_0(k1_lattice2(sK1))
| ~ spl33_314 ),
inference(superposition,[],[f5014,f12836]) ).
fof(f39529,plain,
( u1_struct_0(sK1) = u1_struct_0(k1_lattice2(sK1))
| ~ spl33_314 ),
inference(trivial_inequality_removal,[],[f39524]) ).
fof(f60485,plain,
( ~ m1_subset_1(sK3,k1_zfmisc_1(u1_struct_0(sK1)))
| k3_filter_2(k1_lattice2(sK1),sK3) = k19_filter_2(sK1,k8_filter_2(sK1,sK3))
| ~ m1_subset_1(sK3,k1_zfmisc_1(u1_struct_0(sK1)))
| v3_struct_0(sK1)
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ spl33_314 ),
inference(superposition,[],[f6656,f39529]) ).
fof(f60486,plain,
( ~ m1_subset_1(sK3,k1_zfmisc_1(u1_struct_0(sK1)))
| k3_filter_2(k1_lattice2(sK1),sK3) = k19_filter_2(sK1,k8_filter_2(sK1,sK3))
| v3_struct_0(sK1)
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ spl33_314 ),
inference(duplicate_literal_removal,[],[f60485]) ).
fof(f60487,plain,
( k3_filter_2(k1_lattice2(sK1),sK3) = k19_filter_2(sK1,k8_filter_2(sK1,sK3))
| v3_struct_0(sK1)
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ spl33_314 ),
inference(forward_subsumption_resolution,[],[f60486,f311]) ).
fof(f60494,plain,
( k3_filter_2(k1_lattice2(sK1),sK3) = k19_filter_2(sK1,k8_filter_2(sK1,sK3))
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ spl33_314 ),
inference(forward_subsumption_resolution,[],[f60487,f309]) ).
fof(f60501,plain,
( k3_filter_2(k1_lattice2(sK1),sK3) = k19_filter_2(sK1,k8_filter_2(sK1,sK3))
| ~ l3_lattices(sK1)
| ~ spl33_314 ),
inference(forward_subsumption_resolution,[],[f60494,f308]) ).
fof(f60506,plain,
( k3_filter_2(k1_lattice2(sK1),sK3) = k19_filter_2(sK1,k8_filter_2(sK1,sK3))
| ~ spl33_314 ),
inference(forward_subsumption_resolution,[],[f60501,f307]) ).
fof(f60511,plain,
( k19_filter_2(sK1,sK3) = k3_filter_2(k1_lattice2(sK1),sK3)
| ~ spl33_314 ),
inference(forward_demodulation,[],[f60506,f5232]) ).
fof(f114228,plain,
( k3_filter_0(k1_lattice2(sK1),sK3) = k2_filter_0(k1_lattice2(sK1),sK2)
| spl33_23
| ~ spl33_318
| spl33_326
| ~ spl33_328
| ~ spl33_690
| ~ spl33_691
| ~ spl33_1120 ),
inference(superposition,[],[f12618,f18963]) ).
fof(f114229,plain,
( k3_filter_0(k1_lattice2(sK1),sK3) = a_2_0_filter_0(k1_lattice2(sK1),sK2)
| spl33_23
| ~ spl33_318
| spl33_326
| ~ spl33_328
| ~ spl33_690
| ~ spl33_691
| ~ spl33_739
| ~ spl33_1120 ),
inference(forward_demodulation,[],[f114228,f18385]) ).
fof(f114230,plain,
( k18_filter_2(sK1,sK2) = k3_filter_0(k1_lattice2(sK1),sK3)
| spl33_23
| ~ spl33_318
| spl33_326
| ~ spl33_328
| ~ spl33_690
| ~ spl33_691
| ~ spl33_739
| ~ spl33_1120 ),
inference(forward_demodulation,[],[f114229,f18699]) ).
fof(f114232,plain,
( k18_filter_2(sK1,sK2) = k3_filter_2(k1_lattice2(sK1),sK3)
| spl33_23
| ~ spl33_318
| spl33_326
| ~ spl33_328
| ~ spl33_690
| ~ spl33_691
| ~ spl33_739
| ~ spl33_1120 ),
inference(superposition,[],[f6463,f114230]) ).
fof(f114235,plain,
( k19_filter_2(sK1,sK3) = k18_filter_2(sK1,sK2)
| spl33_23
| ~ spl33_314
| ~ spl33_318
| spl33_326
| ~ spl33_328
| ~ spl33_690
| ~ spl33_691
| ~ spl33_739
| ~ spl33_1120 ),
inference(forward_demodulation,[],[f114232,f60511]) ).
fof(f114264,plain,
( ~ r1_filter_2(u1_struct_0(sK1),k19_filter_2(sK1,sK3),k19_filter_2(sK1,sK3))
| spl33_23
| ~ spl33_314
| ~ spl33_318
| spl33_326
| ~ spl33_328
| ~ spl33_690
| ~ spl33_691
| ~ spl33_739
| ~ spl33_1120
| spl33_1177 ),
inference(superposition,[],[f20626,f114235]) ).
fof(f114308,plain,
( ! [X0] :
( ~ m1_subset_1(k19_filter_2(sK1,sK3),k1_zfmisc_1(u1_struct_0(sK1)))
| ~ v1_xboole_0(X0)
| u1_struct_0(sK1) = X0 )
| spl33_23
| ~ spl33_314
| ~ spl33_318
| spl33_326
| ~ spl33_328
| ~ spl33_690
| ~ spl33_691
| ~ spl33_739
| ~ spl33_1120
| spl33_1177 ),
inference(resolution,[],[f114264,f1158]) ).
fof(f114312,plain,
( ! [X0] :
( ~ v1_xboole_0(X0)
| u1_struct_0(sK1) = X0 )
| spl33_23
| ~ spl33_314
| ~ spl33_318
| spl33_326
| ~ spl33_328
| ~ spl33_441
| ~ spl33_690
| ~ spl33_691
| ~ spl33_739
| ~ spl33_1120
| spl33_1177 ),
inference(forward_subsumption_resolution,[],[f114308,f7641]) ).
fof(f114315,plain,
( spl33_689
| spl33_23
| ~ spl33_314
| ~ spl33_318
| spl33_326
| ~ spl33_328
| ~ spl33_441
| ~ spl33_690
| ~ spl33_691
| ~ spl33_739
| ~ spl33_1120
| spl33_1177 ),
inference(avatar_split_clause,[],[f114312,f20624,f18961,f12923,f11790,f11785,f7640,f5255,f5244,f5030,f5013,f726,f11781]) ).
cnf(s12,plain,
( ~ spl33_23
| spl33_24 ),
inference(sat_conversion,[],[f732]) ).
cnf(s14,plain,
~ spl33_19,
inference(sat_conversion,[],[f736]) ).
cnf(s28,plain,
( spl33_19
| ~ spl33_24 ),
inference(sat_conversion,[],[f942]) ).
cnf(s71,plain,
spl33_99,
inference(sat_conversion,[],[f1718]) ).
cnf(s290,plain,
( ~ spl33_308
| ~ spl33_309
| ~ spl33_310
| ~ spl33_311
| ~ spl33_312
| ~ spl33_313
| spl33_314 ),
inference(sat_conversion,[],[f5015]) ).
cnf(s304,plain,
spl33_318,
inference(sat_conversion,[],[f5269]) ).
cnf(s305,plain,
spl33_328,
inference(sat_conversion,[],[f5278]) ).
cnf(s306,plain,
~ spl33_326,
inference(sat_conversion,[],[f5283]) ).
cnf(s310,plain,
( ~ spl33_318
| spl33_325 ),
inference(sat_conversion,[],[f5411]) ).
cnf(s431,plain,
spl33_441,
inference(sat_conversion,[],[f7659]) ).
cnf(s649,plain,
( spl33_684
| spl33_690 ),
inference(sat_conversion,[],[f11788]) ).
cnf(s650,plain,
( spl33_689
| spl33_691 ),
inference(sat_conversion,[],[f11793]) ).
cnf(s669,plain,
( ~ spl33_99
| ~ spl33_689 ),
inference(sat_conversion,[],[f12174]) ).
cnf(s702,plain,
( ~ spl33_325
| spl33_326
| ~ spl33_684 ),
inference(sat_conversion,[],[f12573]) ).
cnf(s728,plain,
spl33_739,
inference(sat_conversion,[],[f12951]) ).
cnf(s1006,plain,
( ~ spl33_318
| spl33_326
| ~ spl33_328
| ~ spl33_739
| ~ spl33_973
| spl33_974 ),
inference(sat_conversion,[],[f16017]) ).
cnf(s1007,plain,
( ~ spl33_318
| spl33_326
| ~ spl33_328
| ~ spl33_739
| spl33_973 ),
inference(sat_conversion,[],[f16027]) ).
cnf(s1214,plain,
( spl33_23
| spl33_689
| ~ spl33_691
| spl33_1120 ),
inference(sat_conversion,[],[f18967]) ).
cnf(s1290,plain,
( ~ spl33_441
| spl33_689
| ~ spl33_974
| ~ spl33_1177 ),
inference(sat_conversion,[],[f20627]) ).
cnf(s1974,plain,
( spl33_308
| ~ spl33_692 ),
inference(sat_conversion,[],[f35912]) ).
cnf(s1975,plain,
spl33_692,
inference(sat_conversion,[],[f35915]) ).
cnf(s1976,plain,
( spl33_309
| ~ spl33_692 ),
inference(sat_conversion,[],[f35977]) ).
cnf(s1977,plain,
( spl33_310
| ~ spl33_692 ),
inference(sat_conversion,[],[f35981]) ).
cnf(s1988,plain,
( spl33_311
| ~ spl33_694 ),
inference(sat_conversion,[],[f36081]) ).
cnf(s1989,plain,
spl33_694,
inference(sat_conversion,[],[f36084]) ).
cnf(s2000,plain,
( spl33_312
| ~ spl33_694 ),
inference(sat_conversion,[],[f36162]) ).
cnf(s2001,plain,
( spl33_313
| ~ spl33_694 ),
inference(sat_conversion,[],[f36166]) ).
cnf(s5671,plain,
( spl33_23
| ~ spl33_314
| ~ spl33_318
| spl33_326
| ~ spl33_328
| ~ spl33_441
| spl33_689
| ~ spl33_690
| ~ spl33_691
| ~ spl33_739
| ~ spl33_1120
| spl33_1177 ),
inference(sat_conversion,[],[f114315]) ).
cnf(s5771,plain,
spl33_313,
inference(rat,[],[s2001,s1989]) ).
cnf(s5772,plain,
spl33_312,
inference(rat,[],[s2000,s1989]) ).
cnf(s5773,plain,
spl33_311,
inference(rat,[],[s1988,s1989]) ).
cnf(s5774,plain,
spl33_310,
inference(rat,[],[s1977,s1975]) ).
cnf(s5775,plain,
spl33_309,
inference(rat,[],[s1976,s1975]) ).
cnf(s5776,plain,
spl33_308,
inference(rat,[],[s1974,s1975]) ).
cnf(s5890,plain,
spl33_973,
inference(rat,[],[s1007,s305,s728,s306,s304]) ).
cnf(s5904,plain,
spl33_325,
inference(rat,[],[s310,s304]) ).
cnf(s5908,plain,
spl33_974,
inference(rat,[],[s1006,s304,s305,s728,s306,s5890]) ).
cnf(s5946,plain,
~ spl33_684,
inference(rat,[],[s702,s306,s5904]) ).
cnf(s5985,plain,
spl33_690,
inference(rat,[],[s649,s5946]) ).
cnf(s6083,plain,
spl33_314,
inference(rat,[],[s290,s5771,s5772,s5773,s5774,s5775,s5776]) ).
cnf(s6119,plain,
~ spl33_689,
inference(rat,[],[s669,s71]) ).
cnf(s6128,plain,
~ spl33_1177,
inference(rat,[],[s1290,s5908,s431,s6119]) ).
cnf(s6129,plain,
spl33_691,
inference(rat,[],[s650,s6119]) ).
cnf(s6162,plain,
~ spl33_24,
inference(rat,[],[s28,s14]) ).
cnf(s6171,plain,
~ spl33_23,
inference(rat,[],[s12,s6162]) ).
cnf(s6172,plain,
~ spl33_1120,
inference(rat,[],[s5671,s6128,s6119,s728,s6129,s5985,s6083,s431,s305,s306,s304,s6171]) ).
cnf(s6180,plain,
$false,
inference(rat,[],[s1214,s6129,s6119,s6172,s6171]) ).
fof(f114316,plain,
$false,
inference(avatar_sat_refutation,[],[s6180]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT312+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.13/0.38 % Computer : n015.cluster.edu
% 0.13/0.38 % Model : x86_64 x86_64
% 0.13/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.38 % Memory : 8046.5625MB
% 0.13/0.38 % OS : Linux 6.8.0-71-generic
% 0.14/0.38 % CPULimit : 300
% 0.14/0.38 % WCLimit : 300
% 0.14/0.38 % DateTime : Sun Sep 27 14:33:00 UTC 2026
% 0.14/0.38 % CPUTime :
% 0.14/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.14/0.41 Running first-order model finding
% 0.14/0.41 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
% 14.78/2.58 % (1720340)Will run a generic schedule for satisfiability detection.
% 14.78/2.58 % (1720351)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4163670954:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 14.78/2.58 % (1720346)% WARNING: option uhcvi not known.
% 14.78/2.58 % (1720345)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=467959956_2999 on theBenchmark for (2999ds/0Mi)
% 14.78/2.58 % (1720347)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=518665271:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 14.78/2.58 % (1720348)dis+10_1_sil=32000:sp=arity:random_seed=385888835:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 14.78/2.58 % (1720346)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1102151835:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 14.78/2.58 % (1720349)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1014626649:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 14.78/2.58 % (1720350)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=397330584:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 14.78/2.58 % TRYING [1]
% 14.78/2.58 % TRYING [2]
% 14.78/2.58 % TRYING [3]
% 14.78/2.58 % TRYING [4]
% 14.78/2.58 % (1720351)Instruction limit reached!
% 14.78/2.58 % (1720351)------------------------------
% 14.78/2.58 % (1720351)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.78/2.58 % (1720351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.78/2.58 % (1720351)CaDiCaL version: 2.1.3
% 14.78/2.58 % (1720351)Termination reason: Instruction limit
% 14.78/2.58 % (1720351)Termination phase: Saturation
% 14.78/2.58 % (1720351)Time elapsed: 0.061 s
% 14.78/2.58 % (1720351)Peak memory usage: 15 MB
% 14.78/2.58 % (1720351)Instructions burned: 161 (million)
% 14.78/2.58 % (1720349)Instruction limit reached!
% 14.78/2.58 % (1720349)------------------------------
% 14.78/2.58 % (1720349)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.78/2.58 % (1720349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.78/2.58 % (1720349)CaDiCaL version: 2.1.3
% 14.78/2.58 % (1720349)Termination reason: Instruction limit
% 14.78/2.58 % (1720349)Termination phase: Saturation
% 14.78/2.58 % (1720349)Time elapsed: 0.064 s
% 14.78/2.58 % (1720349)Peak memory usage: 13 MB
% 14.78/2.58 % (1720349)Instructions burned: 118 (million)
% 14.78/2.58 % (1720348)Instruction limit reached!
% 14.78/2.58 % (1720348)------------------------------
% 14.78/2.58 % (1720348)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.78/2.58 % (1720348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.78/2.58 % (1720348)CaDiCaL version: 2.1.3
% 14.78/2.58 % (1720348)Termination reason: Instruction limit
% 14.78/2.58 % (1720348)Termination phase: Saturation
% 14.78/2.58 % (1720348)Time elapsed: 0.067 s
% 14.78/2.58 % (1720348)Peak memory usage: 13 MB
% 14.78/2.58 % (1720348)Instructions burned: 103 (million)
% 14.78/2.58 % (1720350)Instruction limit reached!
% 14.78/2.58 % (1720350)------------------------------
% 14.78/2.58 % (1720350)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.78/2.58 % (1720350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.78/2.58 % (1720350)CaDiCaL version: 2.1.3
% 14.78/2.58 % (1720350)Termination reason: Instruction limit
% 14.78/2.58 % (1720350)Termination phase: Saturation
% 14.78/2.58 % (1720350)Time elapsed: 0.067 s
% 14.78/2.58 % (1720350)Peak memory usage: 14 MB
% 14.78/2.58 % (1720350)Instructions burned: 131 (million)
% 14.78/2.58 % (1720359)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1809356309:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 14.78/2.58 % TRYING [5]
% 14.78/2.58 % (1720360)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2994011173:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 14.78/2.58 % TRYING [1]
% 14.78/2.58 % TRYING [2]
% 14.78/2.58 % (1720361)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=1426807652:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 14.78/2.58 % (1720362)ott-21_1_sil=16000:fs=off:random_seed=1769951064:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 14.78/2.58 % TRYING [3]
% 14.78/2.58 % TRYING [4]
% 14.78/2.58 % TRYING [5]
% 14.78/2.58 % (1720360)Instruction limit reached!
% 14.78/2.58 % (1720360)------------------------------
% 14.78/2.58 % (1720360)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.84/5.28 % (1720360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.84/5.28 % (1720360)CaDiCaL version: 2.1.3
% 33.84/5.28 % (1720360)Termination reason: Instruction limit
% 33.84/5.28 % (1720360)Termination phase: Saturation
% 33.84/5.28 % (1720360)Time elapsed: 0.079 s
% 33.84/5.28 % (1720360)Peak memory usage: 13 MB
% 33.84/5.28 % (1720360)Instructions burned: 132 (million)
% 33.84/5.28 % TRYING [6]
% 33.84/5.28 % (1720362)Instruction limit reached!
% 33.84/5.28 % (1720362)------------------------------
% 33.84/5.28 % (1720362)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.84/5.28 % (1720362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.84/5.28 % (1720362)CaDiCaL version: 2.1.3
% 33.84/5.28 % (1720362)Termination reason: Instruction limit
% 33.84/5.28 % (1720362)Termination phase: Saturation
% 33.84/5.28 % (1720362)Time elapsed: 0.095 s
% 33.84/5.28 % (1720362)Peak memory usage: 12 MB
% 33.84/5.28 % (1720362)Instructions burned: 182 (million)
% 33.84/5.28 % (1720367)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=154054848:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 33.84/5.28 % (1720369)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=543536512:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 33.84/5.28 % (1720359)Instruction limit reached!
% 33.84/5.28 % (1720359)------------------------------
% 33.84/5.28 % (1720359)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.84/5.28 % (1720359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.84/5.28 % (1720359)CaDiCaL version: 2.1.3
% 33.84/5.28 % (1720359)Termination reason: Instruction limit
% 33.84/5.28 % (1720359)Termination phase: Finite model building constraint generation
% 33.84/5.28 % (1720359)Time elapsed: 0.134 s
% 33.84/5.28 % (1720359)Peak memory usage: 25 MB
% 33.84/5.28 % (1720359)Instructions burned: 720 (million)
% 33.84/5.28 % TRYING [1]
% 33.84/5.28 % TRYING [2]
% 33.84/5.28 % (1720371)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2044247163:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 33.84/5.28 % TRYING [3]
% 33.84/5.28 % TRYING [4]
% 33.84/5.28 % TRYING [5]
% 33.84/5.28 % TRYING [7]
% 33.84/5.28 % (1720361)Instruction limit reached!
% 33.84/5.28 % (1720361)------------------------------
% 33.84/5.28 % (1720361)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.84/5.28 % (1720361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.84/5.28 % (1720361)CaDiCaL version: 2.1.3
% 33.84/5.28 % (1720361)Termination reason: Instruction limit
% 33.84/5.28 % (1720361)Termination phase: Saturation
% 33.84/5.28 % (1720361)Time elapsed: 0.362 s
% 33.84/5.28 % (1720361)Peak memory usage: 19 MB
% 33.84/5.28 % (1720361)Instructions burned: 686 (million)
% 33.84/5.28 % (1720373)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=308405341:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 33.84/5.28 % (1720367)Instruction limit reached!
% 33.84/5.28 % (1720367)------------------------------
% 33.84/5.28 % (1720367)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.84/5.28 % (1720367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.84/5.28 % (1720367)CaDiCaL version: 2.1.3
% 33.84/5.28 % (1720367)Termination reason: Instruction limit
% 33.84/5.28 % (1720367)Termination phase: Saturation
% 33.84/5.28 % (1720367)Time elapsed: 0.335 s
% 33.84/5.28 % (1720367)Peak memory usage: 15 MB
% 33.84/5.28 % (1720367)Instructions burned: 477 (million)
% 33.84/5.28 % (1720375)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=2462160781:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 33.84/5.28 % (1720369)Instruction limit reached!
% 33.84/5.28 % (1720369)------------------------------
% 33.84/5.28 % (1720369)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.84/5.28 % (1720369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.84/5.28 % (1720369)CaDiCaL version: 2.1.3
% 33.84/5.28 % (1720369)Termination reason: Instruction limit
% 33.84/5.28 % (1720369)Termination phase: Finite model building SAT solving
% 33.84/5.28 % (1720369)Time elapsed: 0.341 s
% 33.84/5.28 % (1720369)Peak memory usage: 25 MB
% 33.84/5.28 % (1720369)Instructions burned: 865 (million)
% 33.84/5.28 % (1720377)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=4245293481:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 33.84/5.28 % (1720371)Instruction limit reached!
% 80.36/12.16 % (1720371)------------------------------
% 80.36/12.16 % (1720371)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 80.36/12.16 % (1720371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.36/12.16 % (1720371)CaDiCaL version: 2.1.3
% 80.36/12.16 % (1720371)Termination reason: Instruction limit
% 80.36/12.16 % (1720371)Termination phase: Saturation
% 80.36/12.16 % (1720371)Time elapsed: 0.352 s
% 80.36/12.16 % (1720371)Peak memory usage: 22 MB
% 80.36/12.16 % (1720371)Instructions burned: 1181 (million)
% 80.36/12.16 % (1720379)fmb+10_1_sil=64000:random_seed=3774881269:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 80.36/12.16 % TRYING [1]
% 80.36/12.16 % TRYING [2]
% 80.36/12.16 % TRYING [3]
% 80.36/12.16 % TRYING [14]
% 80.36/12.16 % TRYING [4]
% 80.36/12.16 % (1720373)Instruction limit reached!
% 80.36/12.16 % (1720373)------------------------------
% 80.36/12.16 % (1720373)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 80.36/12.16 % (1720373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.36/12.16 % (1720373)CaDiCaL version: 2.1.3
% 80.36/12.16 % (1720373)Termination reason: Instruction limit
% 80.36/12.16 % (1720373)Termination phase: Finite model building constraint generation
% 80.36/12.16 % (1720373)Time elapsed: 0.341 s
% 80.36/12.16 % (1720373)Peak memory usage: 77 MB
% 80.36/12.16 % (1720373)Instructions burned: 890 (million)
% 80.36/12.16 % TRYING [5]
% 80.36/12.16 % (1720381)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=250807979:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 80.36/12.16 % TRYING [20]
% 80.36/12.16 % (1720375)Instruction limit reached!
% 80.36/12.16 % (1720375)------------------------------
% 80.36/12.16 % (1720375)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 80.36/12.16 % (1720375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.36/12.16 % (1720375)CaDiCaL version: 2.1.3
% 80.36/12.16 % (1720375)Termination reason: Instruction limit
% 80.36/12.16 % (1720375)Termination phase: Saturation
% 80.36/12.16 % (1720375)Time elapsed: 0.386 s
% 80.36/12.16 % (1720375)Peak memory usage: 22 MB
% 80.36/12.16 % (1720375)Instructions burned: 692 (million)
% 80.36/12.16 % (1720383)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2839690282:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 80.36/12.16 % TRYING [8]
% 80.36/12.16 % (1720377)Instruction limit reached!
% 80.36/12.16 % (1720377)------------------------------
% 80.36/12.16 % (1720377)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 80.36/12.16 % (1720377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.36/12.16 % (1720377)CaDiCaL version: 2.1.3
% 80.36/12.16 % (1720377)Termination reason: Instruction limit
% 80.36/12.16 % (1720377)Termination phase: Saturation
% 80.36/12.16 % (1720377)Time elapsed: 0.515 s
% 80.36/12.16 % (1720377)Peak memory usage: 19 MB
% 80.36/12.16 % (1720377)Instructions burned: 879 (million)
% 80.36/12.16 % (1720385)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=818104051:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 80.36/12.16 % (1720383)Instruction limit reached!
% 80.36/12.16 % (1720383)------------------------------
% 80.36/12.16 % (1720383)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 80.36/12.16 % (1720383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.36/12.16 % (1720383)CaDiCaL version: 2.1.3
% 80.36/12.16 % (1720383)Termination reason: Instruction limit
% 80.36/12.16 % (1720383)Termination phase: Finite model building constraint generation
% 80.36/12.16 % (1720383)Time elapsed: 0.351 s
% 80.36/12.16 % (1720383)Peak memory usage: 71 MB
% 80.36/12.16 % (1720383)Instructions burned: 922 (million)
% 80.36/12.16 % (1720387)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3464714731:i=1472:ins=7:fdi=8:gsp=on_2986 on theBenchmark for (2986ds/1472Mi)
% 80.36/12.16 % TRYING [8]
% 80.36/12.16 % TRYING [6]
% 80.36/12.16 % (1720387)Instruction limit reached!
% 80.36/12.16 % (1720387)------------------------------
% 80.36/12.16 % (1720387)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 80.36/12.16 % (1720387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.36/12.16 % (1720387)CaDiCaL version: 2.1.3
% 80.36/12.16 % (1720387)Termination reason: Instruction limit
% 80.36/12.16 % (1720387)Termination phase: Saturation
% 80.36/12.16 % (1720387)Time elapsed: 0.783 s
% 80.36/12.16 % (1720387)Peak memory usage: 27 MB
% 80.36/12.16 % (1720387)Instructions burned: 1473 (million)
% 80.36/12.16 % (1720389)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3822615806:i=6324_2978 on theBenchmark for (2978ds/6324Mi)
% 232.16/33.14 % TRYING [77]
% 232.16/33.14 % (1720385)Instruction limit reached!
% 232.16/33.14 % (1720385)------------------------------
% 232.16/33.14 % (1720385)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 232.16/33.14 % (1720385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 232.16/33.14 % (1720385)CaDiCaL version: 2.1.3
% 232.16/33.14 % (1720385)Termination reason: Instruction limit
% 232.16/33.14 % (1720385)Termination phase: Saturation
% 232.16/33.14 % (1720385)Time elapsed: 2.759 s
% 232.16/33.14 % (1720385)Peak memory usage: 35 MB
% 232.16/33.14 % (1720385)Instructions burned: 5133 (million)
% 232.16/33.14 % (1720396)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=275156691:fmbsr=2.30978:i=2174_2961 on theBenchmark for (2961ds/2174Mi)
% 232.16/33.14 % TRYING [16]
% 232.16/33.14 % (1720381)Instruction limit reached!
% 232.16/33.14 % (1720381)------------------------------
% 232.16/33.14 % (1720381)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 232.16/33.14 % (1720381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 232.16/33.14 % (1720381)CaDiCaL version: 2.1.3
% 232.16/33.14 % (1720381)Termination reason: Instruction limit
% 232.16/33.14 % (1720381)Termination phase: Finite model building constraint generation
% 232.16/33.14 % (1720381)Time elapsed: 3.278 s
% 232.16/33.14 % (1720381)Peak memory usage: 553 MB
% 232.16/33.14 % (1720381)Instructions burned: 9517 (million)
% 232.16/33.14 % (1720398)ott-2_1_sil=16000:newcnf=on:random_seed=1928606869:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2957 on theBenchmark for (2957ds/869Mi)
% 232.16/33.14 % (1720389)Instruction limit reached!
% 232.16/33.14 % (1720389)------------------------------
% 232.16/33.14 % (1720389)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 232.16/33.14 % (1720389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 232.16/33.14 % (1720389)CaDiCaL version: 2.1.3
% 232.16/33.14 % (1720389)Termination reason: Instruction limit
% 232.16/33.14 % (1720389)Termination phase: Finite model building constraint generation
% 232.16/33.14 % (1720389)Time elapsed: 2.337 s
% 232.16/33.14 % (1720389)Peak memory usage: 434 MB
% 232.16/33.14 % (1720389)Instructions burned: 6324 (million)
% 232.16/33.14 % (1720400)ott+10_1_sil=32000:tgt=ground:random_seed=4270640062:i=5114:av=off_2954 on theBenchmark for (2954ds/5114Mi)
% 232.16/33.14 % (1720396)Instruction limit reached!
% 232.16/33.14 % (1720396)------------------------------
% 232.16/33.14 % (1720396)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 232.16/33.14 % (1720396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 232.16/33.14 % (1720396)CaDiCaL version: 2.1.3
% 232.16/33.14 % (1720396)Termination reason: Instruction limit
% 232.16/33.14 % (1720396)Termination phase: Finite model building constraint generation
% 232.16/33.14 % (1720396)Time elapsed: 0.755 s
% 232.16/33.14 % (1720396)Peak memory usage: 130 MB
% 232.16/33.14 % (1720396)Instructions burned: 2175 (million)
% 232.16/33.14 % (1720402)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3731858579:i=54282_2953 on theBenchmark for (2953ds/54282Mi)
% 232.16/33.14 % TRYING [1]
% 232.16/33.14 % TRYING [2]
% 232.16/33.14 % TRYING [3]
% 232.16/33.14 % TRYING [4]
% 232.16/33.14 % (1720398)Instruction limit reached!
% 232.16/33.14 % (1720398)------------------------------
% 232.16/33.14 % (1720398)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 232.16/33.14 % (1720398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 232.16/33.14 % (1720398)CaDiCaL version: 2.1.3
% 232.16/33.14 % (1720398)Termination reason: Instruction limit
% 232.16/33.14 % (1720398)Termination phase: Saturation
% 232.16/33.14 % (1720398)Time elapsed: 0.529 s
% 232.16/33.14 % (1720398)Peak memory usage: 19 MB
% 232.16/33.14 % (1720398)Instructions burned: 870 (million)
% 232.16/33.14 % TRYING [5]
% 232.16/33.14 % (1720404)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1268352671:i=3512:aac=none_2952 on theBenchmark for (2952ds/3512Mi)
% 232.16/33.14 % (1720379)Instruction limit reached!
% 232.16/33.14 % (1720379)------------------------------
% 232.16/33.14 % (1720379)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 232.16/33.14 % (1720379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 232.16/33.14 % (1720379)CaDiCaL version: 2.1.3
% 232.16/33.14 % (1720379)Termination reason: Instruction limit
% 232.16/33.14 % (1720379)Termination phase: Finite model building SAT solving
% 232.16/33.14 % (1720379)Time elapsed: 4.218 s
% 232.16/33.14 % (1720379)Peak memory usage: 111 MB
% 232.16/33.14 % (1720379)Instructions burned: 22068 (million)
% 232.16/33.14 % (1720406)dis+21_1_sil=32000:sas=cadical:random_seed=214871105:i=3773:amm=off_2951 on theBenchmark for (2951ds/3773Mi)
% 207.57/40.15 % TRYING [6]
% 207.57/40.15 % TRYING [7]
% 207.57/40.15 % (1720406)Instruction limit reached!
% 207.57/40.15 % (1720406)------------------------------
% 207.57/40.15 % (1720406)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 207.57/40.15 % (1720406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 207.57/40.15 % (1720406)CaDiCaL version: 2.1.3
% 207.57/40.15 % (1720406)Termination reason: Instruction limit
% 207.57/40.15 % (1720406)Termination phase: Saturation
% 207.57/40.15 % (1720406)Time elapsed: 1.088 s
% 207.57/40.15 % (1720406)Peak memory usage: 34 MB
% 207.57/40.15 % (1720406)Instructions burned: 3776 (million)
% 207.57/40.15 % (1720408)ott+11_1_sil=16000:gs=on:random_seed=2419225055:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2940 on theBenchmark for (2940ds/2251Mi)
% 207.57/40.15 % TRYING [8]
% 207.57/40.15 % (1720408)Instruction limit reached!
% 207.57/40.15 % (1720408)------------------------------
% 207.57/40.15 % (1720408)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 207.57/40.15 % (1720408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 207.57/40.15 % (1720408)CaDiCaL version: 2.1.3
% 207.57/40.15 % (1720408)Termination reason: Instruction limit
% 207.57/40.15 % (1720408)Termination phase: Saturation
% 207.57/40.15 % (1720408)Time elapsed: 0.581 s
% 207.57/40.15 % (1720408)Peak memory usage: 22 MB
% 207.57/40.15 % (1720408)Instructions burned: 2256 (million)
% 207.57/40.15 % (1720410)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=182236012:fmbsr=1.6:i=67534_2934 on theBenchmark for (2934ds/67534Mi)
% 207.57/40.15 % TRYING [7]
% 207.57/40.15 % (1720404)Instruction limit reached!
% 207.57/40.15 % (1720404)------------------------------
% 207.57/40.15 % (1720404)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 207.57/40.15 % (1720404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 207.57/40.15 % (1720404)CaDiCaL version: 2.1.3
% 207.57/40.15 % (1720404)Termination reason: Instruction limit
% 207.57/40.15 % (1720404)Termination phase: Saturation
% 207.57/40.15 % (1720404)Time elapsed: 1.879 s
% 207.57/40.15 % (1720404)Peak memory usage: 32 MB
% 207.57/40.15 % (1720404)Instructions burned: 3512 (million)
% 207.57/40.15 % (1720412)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1298069259:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2933 on theBenchmark for (2933ds/4591Mi)
% 207.57/40.15 % (1720400)Instruction limit reached!
% 207.57/40.15 % (1720400)------------------------------
% 207.57/40.15 % (1720400)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 207.57/40.15 % (1720400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 207.57/40.15 % (1720400)CaDiCaL version: 2.1.3
% 207.57/40.15 % (1720400)Termination reason: Instruction limit
% 207.57/40.15 % (1720400)Termination phase: Saturation
% 207.57/40.15 % (1720400)Time elapsed: 2.830 s
% 207.57/40.15 % (1720400)Peak memory usage: 48 MB
% 207.57/40.15 % (1720400)Instructions burned: 5114 (million)
% 207.57/40.15 % TRYING [8]
% 207.57/40.15 % (1720414)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1730105272:i=29340_2925 on theBenchmark for (2925ds/29340Mi)
% 207.57/40.15 % (1720412)Instruction limit reached!
% 207.57/40.15 % (1720412)------------------------------
% 207.57/40.15 % (1720412)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 207.57/40.15 % (1720412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 207.57/40.15 % (1720412)CaDiCaL version: 2.1.3
% 207.57/40.15 % (1720412)Termination reason: Instruction limit
% 207.57/40.15 % (1720412)Termination phase: Saturation
% 207.57/40.15 % (1720412)Time elapsed: 2.261 s
% 207.57/40.15 % (1720412)Peak memory usage: 37 MB
% 207.57/40.15 % (1720412)Instructions burned: 4593 (million)
% 207.57/40.15 % (1720416)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=791831199:i=5211_2910 on theBenchmark for (2910ds/5211Mi)
% 207.57/40.15 % (1720416)Instruction limit reached!
% 207.57/40.15 % (1720416)------------------------------
% 207.57/40.15 % (1720416)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 207.57/40.15 % (1720416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 207.57/40.15 % (1720416)CaDiCaL version: 2.1.3
% 207.57/40.15 % (1720416)Termination reason: Instruction limit
% 207.57/40.15 % (1720416)Termination phase: Saturation
% 207.57/40.15 % (1720416)Time elapsed: 2.724 s
% 207.57/40.15 % (1720416)Peak memory usage: 44 MB
% 207.57/40.15 % (1720416)Instructions burned: 5214 (million)
% 207.57/40.15 % (1720418)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2200843730:i=5497:nm=2_2882 on theBenchmark for (2882ds/5497Mi)
% 207.57/40.15 % TRYING [17]
% 207.57/40.15 % TRYING [9]
% 207.57/40.15 % TRYING [9]
% 207.57/40.15 % (1720418)Instruction limit reached!
% 207.57/40.15 % (1720418)------------------------------
% 207.57/40.15 % (1720418)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 207.57/40.15 % (1720418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 207.57/40.15 % (1720418)CaDiCaL version: 2.1.3
% 207.57/40.15 % (1720418)Termination reason: Instruction limit
% 207.57/40.15 % (1720418)Termination phase: Finite model building constraint generation
% 207.57/40.15 % (1720418)Time elapsed: 1.820 s
% 207.57/40.15 % (1720418)Peak memory usage: 292 MB
% 207.57/40.15 % (1720418)Instructions burned: 5498 (million)
% 207.57/40.15 % (1720420)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1162155627:fmbsr=2:i=46332_2864 on theBenchmark for (2864ds/46332Mi)
% 207.57/40.15 % TRYING [15]
% 207.57/40.15 % TRYING [9]
% 207.57/40.15 % (1720414)Instruction limit reached!
% 207.57/40.15 % (1720414)------------------------------
% 207.57/40.15 % (1720414)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 207.57/40.15 % (1720414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 207.57/40.15 % (1720414)CaDiCaL version: 2.1.3
% 207.57/40.15 % (1720414)Termination reason: Instruction limit
% 207.57/40.15 % (1720414)Termination phase: Saturation
% 207.57/40.15 % (1720414)Time elapsed: 12.673 s
% 207.57/40.15 % (1720414)Peak memory usage: 193 MB
% 207.57/40.15 % (1720414)Instructions burned: 29340 (million)
% 207.57/40.15 % (1720422)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=833908591:i=14071_2798 on theBenchmark for (2798ds/14071Mi)
% 207.57/40.15 % TRYING [12]
% 207.57/40.15 % (1720410)Instruction limit reached!
% 207.57/40.15 % (1720410)------------------------------
% 207.57/40.15 % (1720410)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 207.57/40.15 % (1720410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 207.57/40.15 % (1720410)CaDiCaL version: 2.1.3
% 207.57/40.15 % (1720410)Termination reason: Instruction limit
% 207.57/40.15 % (1720410)Termination phase: Finite model building SAT solving
% 207.57/40.15 % (1720410)Time elapsed: 17.426 s
% 207.57/40.15 % (1720410)Peak memory usage: 160 MB
% 207.57/40.15 % (1720410)Instructions burned: 67538 (million)
% 207.57/40.15 % (1720424)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=448503708:i=22565:add=on:rawr=on_2760 on theBenchmark for (2760ds/22565Mi)
% 207.57/40.15 % (1720422)Instruction limit reached!
% 207.57/40.15 % (1720422)------------------------------
% 207.57/40.15 % (1720422)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 207.57/40.15 % (1720422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 207.57/40.15 % (1720422)CaDiCaL version: 2.1.3
% 207.57/40.15 % (1720422)Termination reason: Instruction limit
% 207.57/40.15 % (1720422)Termination phase: Finite model building SAT solving
% 207.57/40.15 % (1720422)Time elapsed: 7.589 s
% 207.57/40.15 % (1720422)Peak memory usage: 656 MB
% 207.57/40.15 % (1720422)Instructions burned: 14072 (million)
% 207.57/40.15 % (1720426)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=4263489856:i=8173:av=off_2721 on theBenchmark for (2721ds/8173Mi)
% 207.57/40.15 % (1720402)Instruction limit reached!
% 207.57/40.15 % (1720402)------------------------------
% 207.57/40.15 % (1720402)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 207.57/40.15 % (1720402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 207.57/40.15 % (1720402)CaDiCaL version: 2.1.3
% 207.57/40.15 % (1720402)Termination reason: Instruction limit
% 207.57/40.15 % (1720402)Termination phase: Finite model building SAT solving
% 207.57/40.15 % (1720402)Time elapsed: 25.490 s
% 207.57/40.15 % (1720402)Peak memory usage: 287 MB
% 207.57/40.15 % (1720402)Instructions burned: 54285 (million)
% 207.57/40.15 % (1720428)dis+10_16:1_sil=16000:random_seed=2805754984:i=9155:fsr=off_2697 on theBenchmark for (2697ds/9155Mi)
% 207.57/40.15 % (1720424)Instruction limit reached!
% 207.57/40.15 % (1720424)------------------------------
% 207.57/40.15 % (1720424)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 207.57/40.15 % (1720424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 207.57/40.15 % (1720424)CaDiCaL version: 2.1.3
% 207.57/40.15 % (1720424)Termination reason: Instruction limit
% 207.57/40.15 % (1720424)Termination phase: Saturation
% 207.57/40.15 % (1720424)Time elapsed: 8.699 s
% 207.57/40.15 % (1720424)Peak memory usage: 87 MB
% 207.57/40.15 % (1720424)Instructions burned: 22567 (million)
% 207.57/40.15 % (1720430)ott-3_8_sil=64000:random_seed=527981551:i=20139:bs=on_2672 on theBenchmark for (2672ds/20139Mi)
% 207.57/40.15 % (1720426)Instruction limit reached!
% 207.57/40.15 % (1720426)------------------------------
% 207.57/40.15 % (1720426)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 207.57/40.15 % (1720426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 207.57/40.15 % (1720426)CaDiCaL version: 2.1.3
% 207.57/40.15 % (1720426)Termination reason: Instruction limit
% 207.57/40.15 % (1720426)Termination phase: Saturation
% 207.57/40.15 % (1720426)Time elapsed: 4.904 s
% 207.57/40.15 % (1720426)Peak memory usage: 91 MB
% 207.57/40.15 % (1720426)Instructions burned: 8174 (million)
% 207.57/40.15 % (1720432)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3741241573:fmbsr=2:i=32576_2672 on theBenchmark for (2672ds/32576Mi)
% 207.57/40.15 % TRYING [9]
% 207.57/40.15 % (1720428)Instruction limit reached!
% 207.57/40.15 % (1720428)------------------------------
% 207.57/40.15 % (1720428)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 207.57/40.15 % (1720428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 207.57/40.15 % (1720428)CaDiCaL version: 2.1.3
% 207.57/40.15 % (1720428)Termination reason: Instruction limit
% 207.57/40.15 % (1720428)Termination phase: Saturation
% 207.57/40.15 % (1720428)Time elapsed: 5.185 s
% 207.57/40.15 % (1720428)Peak memory usage: 44 MB
% 207.57/40.15 % (1720428)Instructions burned: 9157 (million)
% 207.57/40.15 % (1720434)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=4236569256:i=11404_2645 on theBenchmark for (2645ds/11404Mi)
% 207.57/40.15 % (1720430) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1720340-1720430"...
% 207.57/40.15 % (1720430)...printing done.
% 207.57/40.15 % (1720430)Refutation found. Thanks to Tanya!
% 207.57/40.15 % SZS status Theorem for theBenchmark
% 207.57/40.15 % SZS output start Proof for theBenchmark
% See solution above
% 207.57/40.16 % (1720430)------------------------------
% 207.57/40.16 % (1720430)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 207.57/40.16 % (1720430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 207.57/40.16 % (1720430)CaDiCaL version: 2.1.3
% 207.57/40.16 % (1720430)Termination reason: Refutation
% 207.57/40.16 % (1720430)Time elapsed: 6.789 s
% 207.57/40.16 % (1720430)Peak memory usage: 86 MB
% 207.57/40.16 % (1720430)Instructions burned: 19539 (million)
% 207.57/40.16 % (1720340)Success in time 39.732 s
% 207.57/40.16 % Vampire exiting
%------------------------------------------------------------------------------