%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT332+4 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n007.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:47:02 AM UTC 2026
% Result : Theorem 24.17s 9.47s
% Output : Refutation 0.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 44
% Number of leaves : 36
% Syntax : Number of formulae : 332 ( 25 unt; 17 def)
% Number of atoms : 1952 ( 180 equ)
% Maximal formula atoms : 27 ( 5 avg)
% Number of connectives : 2704 (1084 ~;1376 |; 195 &)
% ( 23 <=>; 26 =>; 0 <=; 0 <~>)
% Maximal formula depth : 23 ( 7 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 39 ( 37 usr; 18 prp; 0-3 aty)
% Number of functors : 16 ( 16 usr; 1 con; 0-3 aty)
% Number of variables : 175 ( 0 sgn 163 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f21499,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& m1_filter_0(X1,X0) )
=> ( ~ v3_struct_0(k8_filter_0(X0,X1))
& v3_lattices(k8_filter_0(X0,X1))
& v4_lattices(k8_filter_0(X0,X1))
& v5_lattices(k8_filter_0(X0,X1))
& v6_lattices(k8_filter_0(X0,X1))
& v7_lattices(k8_filter_0(X0,X1))
& v8_lattices(k8_filter_0(X0,X1))
& v9_lattices(k8_filter_0(X0,X1))
& v10_lattices(k8_filter_0(X0,X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc2_filter_0) ).
fof(f21515,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> m1_filter_0(u1_struct_0(X0),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t15_filter_0) ).
fof(f21516,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> k1_filter_0(X0) = u1_struct_0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d2_filter_0) ).
fof(f21566,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_filter_0(X1,X0)
=> ! [X2] :
( ( ~ v3_struct_0(X2)
& v10_lattices(X2)
& l3_lattices(X2) )
=> ( X2 = k8_filter_0(X0,X1)
<=> ? [X3] :
( v1_funct_1(X3)
& v1_funct_2(X3,k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(X3,k2_zfmisc_1(X1,X1),X1)
& ? [X4] :
( v1_funct_1(X4)
& v1_funct_2(X4,k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(X4,k2_zfmisc_1(X1,X1),X1)
& X3 = k1_realset1(u2_lattices(X0),X1)
& X4 = k1_realset1(u1_lattices(X0),X1)
& X2 = g3_lattices(X1,X3,X4) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d10_filter_0) ).
fof(f21600,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_filter_0(X1,X0)
=> ( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m1_filter_0) ).
fof(f21611,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& m1_filter_0(X1,X0) )
=> ( ~ v3_struct_0(k8_filter_0(X0,X1))
& v10_lattices(k8_filter_0(X0,X1))
& l3_lattices(k8_filter_0(X0,X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k8_filter_0) ).
fof(f22747,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l3_lattices(X0) )
=> ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_lattice2) ).
fof(f22752,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v4_lattices(k1_lattice2(X0))
& v5_lattices(k1_lattice2(X0))
& v6_lattices(k1_lattice2(X0))
& v7_lattices(k1_lattice2(X0))
& v8_lattices(k1_lattice2(X0))
& v9_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc6_lattice2) ).
fof(f22852,axiom,
! [X0] :
( l3_lattices(X0)
=> ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k1_lattice2) ).
fof(f25560,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& l3_lattices(X1) )
=> ( m2_nat_lat(X1,X0)
<=> ( r1_tarski(u1_struct_0(X1),u1_struct_0(X0))
& u2_lattices(X1) = k1_realset1(u2_lattices(X0),u1_struct_0(X1))
& u1_lattices(X1) = k1_realset1(u1_lattices(X0),u1_struct_0(X1)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d16_nat_lat) ).
fof(f25565,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> m2_nat_lat(X0,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t75_nat_lat) ).
fof(f31937,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> m2_lattice4(u1_struct_0(X0),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t10_lattice4) ).
fof(f34612,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> m1_filter_2(k1_filter_2(X0),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k1_filter_2) ).
fof(f34613,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> k1_filter_2(X0) = k1_filter_0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k1_filter_2) ).
fof(f34657,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> k1_lattice2(k1_lattice2(X0)) = g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t7_filter_2) ).
fof(f34687,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> k17_filter_2(X0) = u1_struct_0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d8_filter_2) ).
fof(f34730,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) )
=> ( v1_funct_1(k1_realset1(u2_lattices(X0),X1))
& v1_funct_2(k1_realset1(u2_lattices(X0),X1),k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(k1_realset1(u2_lattices(X0),X1),k2_zfmisc_1(X1,X1),X1)
& v1_funct_1(k1_realset1(u1_lattices(X0),X1))
& v1_funct_2(k1_realset1(u1_lattices(X0),X1),k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(k1_realset1(u1_lattices(X0),X1),k2_zfmisc_1(X1,X1),X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t61_filter_2) ).
fof(f34743,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_filter_2(X1,X0)
=> k8_filter_0(X0,X1) = k23_filter_2(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t70_filter_2) ).
fof(f34745,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( k23_filter_2(X0,k17_filter_2(X0)) = g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))
& k23_filter_2(X0,k1_filter_2(X0)) = g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t72_filter_2) ).
fof(f34746,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( k23_filter_2(X0,k17_filter_2(X0)) = g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))
& k23_filter_2(X0,k1_filter_2(X0)) = g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) ) ),
inference(negated_conjecture,[status(cth)],[f34745]) ).
fof(f34794,plain,
! [X0] :
( m1_filter_2(k1_filter_2(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f34612]) ).
fof(f34795,plain,
! [X0] :
( m1_filter_2(k1_filter_2(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f34794]) ).
fof(f34796,plain,
! [X0] :
( k1_filter_2(X0) = k1_filter_0(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f34613]) ).
fof(f34797,plain,
! [X0] :
( k1_filter_2(X0) = k1_filter_0(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f34796]) ).
fof(f34883,plain,
! [X0] :
( k1_lattice2(k1_lattice2(X0)) = g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f34657]) ).
fof(f34884,plain,
! [X0] :
( k1_lattice2(k1_lattice2(X0)) = g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f34883]) ).
fof(f34941,plain,
! [X0] :
( k17_filter_2(X0) = u1_struct_0(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f34687]) ).
fof(f34942,plain,
! [X0] :
( k17_filter_2(X0) = u1_struct_0(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f34941]) ).
fof(f35027,plain,
! [X0] :
( ! [X1] :
( ( v1_funct_1(k1_realset1(u2_lattices(X0),X1))
& v1_funct_2(k1_realset1(u2_lattices(X0),X1),k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(k1_realset1(u2_lattices(X0),X1),k2_zfmisc_1(X1,X1),X1)
& v1_funct_1(k1_realset1(u1_lattices(X0),X1))
& v1_funct_2(k1_realset1(u1_lattices(X0),X1),k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(k1_realset1(u1_lattices(X0),X1),k2_zfmisc_1(X1,X1),X1) )
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f34730]) ).
fof(f35028,plain,
! [X0] :
( ! [X1] :
( ( v1_funct_1(k1_realset1(u2_lattices(X0),X1))
& v1_funct_2(k1_realset1(u2_lattices(X0),X1),k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(k1_realset1(u2_lattices(X0),X1),k2_zfmisc_1(X1,X1),X1)
& v1_funct_1(k1_realset1(u1_lattices(X0),X1))
& v1_funct_2(k1_realset1(u1_lattices(X0),X1),k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(k1_realset1(u1_lattices(X0),X1),k2_zfmisc_1(X1,X1),X1) )
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35027]) ).
fof(f35053,plain,
! [X0] :
( ! [X1] :
( k8_filter_0(X0,X1) = k23_filter_2(X0,X1)
| ~ m1_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f34743]) ).
fof(f35054,plain,
! [X0] :
( ! [X1] :
( k8_filter_0(X0,X1) = k23_filter_2(X0,X1)
| ~ m1_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35053]) ).
fof(f35057,plain,
? [X0] :
( ( g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) != k23_filter_2(X0,k17_filter_2(X0))
| g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) != k23_filter_2(X0,k1_filter_2(X0)) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(ennf_transformation,[],[f34746]) ).
fof(f35058,plain,
? [X0] :
( ( g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) != k23_filter_2(X0,k17_filter_2(X0))
| g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) != k23_filter_2(X0,k1_filter_2(X0)) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(flattening,[],[f35057]) ).
fof(f35072,plain,
! [X0] :
( m2_lattice4(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f31937]) ).
fof(f35073,plain,
! [X0] :
( m2_lattice4(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35072]) ).
fof(f35082,plain,
! [X0] :
( ! [X1] :
( ( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f21600]) ).
fof(f35083,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,[],[f35082]) ).
fof(f35084,plain,
! [X0] :
( m1_filter_0(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f21515]) ).
fof(f35085,plain,
! [X0] :
( m1_filter_0(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35084]) ).
fof(f35113,plain,
! [X0] :
( k1_filter_0(X0) = u1_struct_0(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f21516]) ).
fof(f35114,plain,
! [X0] :
( k1_filter_0(X0) = u1_struct_0(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35113]) ).
fof(f35175,plain,
! [X0] :
( ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f22852]) ).
fof(f35195,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f22747]) ).
fof(f35196,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35195]) ).
fof(f35201,plain,
! [X0] :
( m2_nat_lat(X0,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f25565]) ).
fof(f35202,plain,
! [X0] :
( m2_nat_lat(X0,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35201]) ).
fof(f35203,plain,
! [X0] :
( ! [X1] :
( ( m2_nat_lat(X1,X0)
<=> ( r1_tarski(u1_struct_0(X1),u1_struct_0(X0))
& u2_lattices(X1) = k1_realset1(u2_lattices(X0),u1_struct_0(X1))
& u1_lattices(X1) = k1_realset1(u1_lattices(X0),u1_struct_0(X1)) ) )
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f25560]) ).
fof(f35204,plain,
! [X0] :
( ! [X1] :
( ( m2_nat_lat(X1,X0)
<=> ( r1_tarski(u1_struct_0(X1),u1_struct_0(X0))
& u2_lattices(X1) = k1_realset1(u2_lattices(X0),u1_struct_0(X1))
& u1_lattices(X1) = k1_realset1(u1_lattices(X0),u1_struct_0(X1)) ) )
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35203]) ).
fof(f35585,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v4_lattices(k1_lattice2(X0))
& v5_lattices(k1_lattice2(X0))
& v6_lattices(k1_lattice2(X0))
& v7_lattices(k1_lattice2(X0))
& v8_lattices(k1_lattice2(X0))
& v9_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f22752]) ).
fof(f35586,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,[],[f35585]) ).
fof(f35607,plain,
! [X0,X1] :
( ( ~ v3_struct_0(k8_filter_0(X0,X1))
& v10_lattices(k8_filter_0(X0,X1))
& l3_lattices(k8_filter_0(X0,X1)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_filter_0(X1,X0) ),
inference(ennf_transformation,[],[f21611]) ).
fof(f35608,plain,
! [X0,X1] :
( ( ~ v3_struct_0(k8_filter_0(X0,X1))
& v10_lattices(k8_filter_0(X0,X1))
& l3_lattices(k8_filter_0(X0,X1)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_filter_0(X1,X0) ),
inference(flattening,[],[f35607]) ).
fof(f35623,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( X2 = k8_filter_0(X0,X1)
<=> ? [X3] :
( v1_funct_1(X3)
& v1_funct_2(X3,k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(X3,k2_zfmisc_1(X1,X1),X1)
& ? [X4] :
( v1_funct_1(X4)
& v1_funct_2(X4,k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(X4,k2_zfmisc_1(X1,X1),X1)
& X3 = k1_realset1(u2_lattices(X0),X1)
& X4 = k1_realset1(u1_lattices(X0),X1)
& X2 = g3_lattices(X1,X3,X4) ) ) )
| v3_struct_0(X2)
| ~ v10_lattices(X2)
| ~ l3_lattices(X2) )
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f21566]) ).
fof(f35624,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( X2 = k8_filter_0(X0,X1)
<=> ? [X3] :
( v1_funct_1(X3)
& v1_funct_2(X3,k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(X3,k2_zfmisc_1(X1,X1),X1)
& ? [X4] :
( v1_funct_1(X4)
& v1_funct_2(X4,k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(X4,k2_zfmisc_1(X1,X1),X1)
& X3 = k1_realset1(u2_lattices(X0),X1)
& X4 = k1_realset1(u1_lattices(X0),X1)
& X2 = g3_lattices(X1,X3,X4) ) ) )
| v3_struct_0(X2)
| ~ v10_lattices(X2)
| ~ l3_lattices(X2) )
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35623]) ).
fof(f35625,plain,
! [X0,X1] :
( ( ~ v3_struct_0(k8_filter_0(X0,X1))
& v3_lattices(k8_filter_0(X0,X1))
& v4_lattices(k8_filter_0(X0,X1))
& v5_lattices(k8_filter_0(X0,X1))
& v6_lattices(k8_filter_0(X0,X1))
& v7_lattices(k8_filter_0(X0,X1))
& v8_lattices(k8_filter_0(X0,X1))
& v9_lattices(k8_filter_0(X0,X1))
& v10_lattices(k8_filter_0(X0,X1)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_filter_0(X1,X0) ),
inference(ennf_transformation,[],[f21499]) ).
fof(f35626,plain,
! [X0,X1] :
( ( ~ v3_struct_0(k8_filter_0(X0,X1))
& v3_lattices(k8_filter_0(X0,X1))
& v4_lattices(k8_filter_0(X0,X1))
& v5_lattices(k8_filter_0(X0,X1))
& v6_lattices(k8_filter_0(X0,X1))
& v7_lattices(k8_filter_0(X0,X1))
& v8_lattices(k8_filter_0(X0,X1))
& v9_lattices(k8_filter_0(X0,X1))
& v10_lattices(k8_filter_0(X0,X1)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_filter_0(X1,X0) ),
inference(flattening,[],[f35625]) ).
fof(f35694,plain,
( ( g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),u1_lattices(sK32)) != k23_filter_2(sK32,k17_filter_2(sK32))
| g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),u1_lattices(sK32)) != k23_filter_2(sK32,k1_filter_2(sK32)) )
& ~ v3_struct_0(sK32)
& v10_lattices(sK32)
& l3_lattices(sK32) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK32]),skolemize(X0,sK32)],[f35058]) ).
fof(f35742,plain,
! [X0] :
( ! [X1] :
( ( ( m2_nat_lat(X1,X0)
| ~ r1_tarski(u1_struct_0(X1),u1_struct_0(X0))
| u2_lattices(X1) != k1_realset1(u2_lattices(X0),u1_struct_0(X1))
| u1_lattices(X1) != k1_realset1(u1_lattices(X0),u1_struct_0(X1)) )
& ( ( r1_tarski(u1_struct_0(X1),u1_struct_0(X0))
& u2_lattices(X1) = k1_realset1(u2_lattices(X0),u1_struct_0(X1))
& u1_lattices(X1) = k1_realset1(u1_lattices(X0),u1_struct_0(X1)) )
| ~ m2_nat_lat(X1,X0) ) )
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f35204]) ).
fof(f35743,plain,
! [X0] :
( ! [X1] :
( ( ( m2_nat_lat(X1,X0)
| ~ r1_tarski(u1_struct_0(X1),u1_struct_0(X0))
| u2_lattices(X1) != k1_realset1(u2_lattices(X0),u1_struct_0(X1))
| u1_lattices(X1) != k1_realset1(u1_lattices(X0),u1_struct_0(X1)) )
& ( ( r1_tarski(u1_struct_0(X1),u1_struct_0(X0))
& u2_lattices(X1) = k1_realset1(u2_lattices(X0),u1_struct_0(X1))
& u1_lattices(X1) = k1_realset1(u1_lattices(X0),u1_struct_0(X1)) )
| ~ m2_nat_lat(X1,X0) ) )
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35742]) ).
fof(f35942,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( X2 = k8_filter_0(X0,X1)
| ! [X3] :
( ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(X3,k2_zfmisc_1(X1,X1),X1)
| ! [X4] :
( ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(X4,k2_zfmisc_1(X1,X1),X1)
| k1_realset1(u2_lattices(X0),X1) != X3
| k1_realset1(u1_lattices(X0),X1) != X4
| g3_lattices(X1,X3,X4) != X2 ) ) )
& ( ? [X3] :
( v1_funct_1(X3)
& v1_funct_2(X3,k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(X3,k2_zfmisc_1(X1,X1),X1)
& ? [X4] :
( v1_funct_1(X4)
& v1_funct_2(X4,k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(X4,k2_zfmisc_1(X1,X1),X1)
& X3 = k1_realset1(u2_lattices(X0),X1)
& X4 = k1_realset1(u1_lattices(X0),X1)
& X2 = g3_lattices(X1,X3,X4) ) )
| k8_filter_0(X0,X1) != X2 ) )
| v3_struct_0(X2)
| ~ v10_lattices(X2)
| ~ l3_lattices(X2) )
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f35624]) ).
fof(f35943,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( X2 = k8_filter_0(X0,X1)
| ! [X3] :
( ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(X3,k2_zfmisc_1(X1,X1),X1)
| ! [X4] :
( ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(X4,k2_zfmisc_1(X1,X1),X1)
| k1_realset1(u2_lattices(X0),X1) != X3
| k1_realset1(u1_lattices(X0),X1) != X4
| g3_lattices(X1,X3,X4) != X2 ) ) )
& ( ? [X5] :
( v1_funct_1(X5)
& v1_funct_2(X5,k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(X5,k2_zfmisc_1(X1,X1),X1)
& ? [X6] :
( v1_funct_1(X6)
& v1_funct_2(X6,k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(X6,k2_zfmisc_1(X1,X1),X1)
& k1_realset1(u2_lattices(X0),X1) = X5
& k1_realset1(u1_lattices(X0),X1) = X6
& g3_lattices(X1,X5,X6) = X2 ) )
| k8_filter_0(X0,X1) != X2 ) )
| v3_struct_0(X2)
| ~ v10_lattices(X2)
| ~ l3_lattices(X2) )
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(rectify,[],[f35942]) ).
fof(f35944,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( X2 = k8_filter_0(X0,X1)
| ! [X3] :
( ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(X3,k2_zfmisc_1(X1,X1),X1)
| ! [X4] :
( ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(X4,k2_zfmisc_1(X1,X1),X1)
| k1_realset1(u2_lattices(X0),X1) != X3
| k1_realset1(u1_lattices(X0),X1) != X4
| g3_lattices(X1,X3,X4) != X2 ) ) )
& ( ( v1_funct_1(sK168(X0,X1,X2))
& v1_funct_2(sK168(X0,X1,X2),k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(sK168(X0,X1,X2),k2_zfmisc_1(X1,X1),X1)
& v1_funct_1(sK169(X0,X1,X2))
& v1_funct_2(sK169(X0,X1,X2),k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(sK169(X0,X1,X2),k2_zfmisc_1(X1,X1),X1)
& k1_realset1(u2_lattices(X0),X1) = sK168(X0,X1,X2)
& k1_realset1(u1_lattices(X0),X1) = sK169(X0,X1,X2)
& g3_lattices(X1,sK168(X0,X1,X2),sK169(X0,X1,X2)) = X2 )
| k8_filter_0(X0,X1) != X2 ) )
| v3_struct_0(X2)
| ~ v10_lattices(X2)
| ~ l3_lattices(X2) )
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK168,sK169]),skolemize(X5,sK168(X0,X1,X2)),skolemize(X6,sK169(X0,X1,X2))],[f35943]) ).
fof(f35957,plain,
! [X0] :
( m1_filter_2(k1_filter_2(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f34795]) ).
fof(f35958,plain,
! [X0] :
( k1_filter_0(X0) = k1_filter_2(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f34797]) ).
fof(f36015,plain,
! [X0] :
( g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) = k1_lattice2(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f34884]) ).
fof(f36102,plain,
! [X0] :
( u1_struct_0(X0) = k17_filter_2(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f34942]) ).
fof(f36235,plain,
! [X0,X1] :
( m2_relset_1(k1_realset1(u2_lattices(X0),X1),k2_zfmisc_1(X1,X1),X1)
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35028]) ).
fof(f36236,plain,
! [X0,X1] :
( v1_funct_2(k1_realset1(u2_lattices(X0),X1),k2_zfmisc_1(X1,X1),X1)
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35028]) ).
fof(f36237,plain,
! [X0,X1] :
( v1_funct_1(k1_realset1(u2_lattices(X0),X1))
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35028]) ).
fof(f36286,plain,
! [X0,X1] :
( k8_filter_0(X0,X1) = k23_filter_2(X0,X1)
| ~ m1_filter_2(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35054]) ).
fof(f36288,plain,
l3_lattices(sK32),
inference(cnf_transformation,[],[f35694]) ).
fof(f36289,plain,
v10_lattices(sK32),
inference(cnf_transformation,[],[f35694]) ).
fof(f36290,plain,
~ v3_struct_0(sK32),
inference(cnf_transformation,[],[f35694]) ).
fof(f36291,plain,
( g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),u1_lattices(sK32)) != k23_filter_2(sK32,k17_filter_2(sK32))
| g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),u1_lattices(sK32)) != k23_filter_2(sK32,k1_filter_2(sK32)) ),
inference(cnf_transformation,[],[f35694]) ).
fof(f36307,plain,
! [X0] :
( m2_lattice4(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35073]) ).
fof(f36320,plain,
! [X0,X1] :
( ~ v1_xboole_0(X1)
| ~ m1_filter_0(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35083]) ).
fof(f36321,plain,
! [X0] :
( m1_filter_0(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35085]) ).
fof(f36388,plain,
! [X0] :
( u1_struct_0(X0) = k1_filter_0(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35114]) ).
fof(f36443,plain,
! [X0] :
( l3_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35175]) ).
fof(f36469,plain,
! [X0] :
( ~ v3_struct_0(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35196]) ).
fof(f36474,plain,
! [X0] :
( m2_nat_lat(X0,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35202]) ).
fof(f36475,plain,
! [X0,X1] :
( u1_lattices(X1) = k1_realset1(u1_lattices(X0),u1_struct_0(X1))
| ~ m2_nat_lat(X1,X0)
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35743]) ).
fof(f36476,plain,
! [X0,X1] :
( u2_lattices(X1) = k1_realset1(u2_lattices(X0),u1_struct_0(X1))
| ~ m2_nat_lat(X1,X0)
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35743]) ).
fof(f37036,plain,
! [X0] :
( v10_lattices(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35586]) ).
fof(f37198,plain,
! [X0,X1] :
( l3_lattices(k8_filter_0(X0,X1))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_filter_0(X1,X0) ),
inference(cnf_transformation,[],[f35608]) ).
fof(f37213,plain,
! [X2,X0,X1] :
( k1_realset1(u1_lattices(X0),X1) = sK169(X0,X1,X2)
| k8_filter_0(X0,X1) != X2
| v3_struct_0(X2)
| ~ v10_lattices(X2)
| ~ l3_lattices(X2)
| ~ m1_filter_0(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35944]) ).
fof(f37215,plain,
! [X2,X0,X1] :
( m2_relset_1(sK169(X0,X1,X2),k2_zfmisc_1(X1,X1),X1)
| k8_filter_0(X0,X1) != X2
| v3_struct_0(X2)
| ~ v10_lattices(X2)
| ~ l3_lattices(X2)
| ~ m1_filter_0(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35944]) ).
fof(f37216,plain,
! [X2,X0,X1] :
( v1_funct_2(sK169(X0,X1,X2),k2_zfmisc_1(X1,X1),X1)
| k8_filter_0(X0,X1) != X2
| v3_struct_0(X2)
| ~ v10_lattices(X2)
| ~ l3_lattices(X2)
| ~ m1_filter_0(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35944]) ).
fof(f37217,plain,
! [X2,X0,X1] :
( v1_funct_1(sK169(X0,X1,X2))
| k8_filter_0(X0,X1) != X2
| v3_struct_0(X2)
| ~ v10_lattices(X2)
| ~ l3_lattices(X2)
| ~ m1_filter_0(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35944]) ).
fof(f37221,plain,
! [X2,X3,X0,X1,X4] :
( k8_filter_0(X0,X1) = X2
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(X3,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(X4,k2_zfmisc_1(X1,X1),X1)
| k1_realset1(u2_lattices(X0),X1) != X3
| k1_realset1(u1_lattices(X0),X1) != X4
| g3_lattices(X1,X3,X4) != X2
| v3_struct_0(X2)
| ~ v10_lattices(X2)
| ~ l3_lattices(X2)
| ~ m1_filter_0(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35944]) ).
fof(f37222,plain,
! [X0,X1] :
( v10_lattices(k8_filter_0(X0,X1))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_filter_0(X1,X0) ),
inference(cnf_transformation,[],[f35626]) ).
fof(f37230,plain,
! [X0,X1] :
( ~ v3_struct_0(k8_filter_0(X0,X1))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_filter_0(X1,X0) ),
inference(cnf_transformation,[],[f35626]) ).
fof(f37363,plain,
! [X2,X0,X1,X4] :
( k8_filter_0(X0,X1) = X2
| ~ v1_funct_1(k1_realset1(u2_lattices(X0),X1))
| ~ v1_funct_2(k1_realset1(u2_lattices(X0),X1),k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(k1_realset1(u2_lattices(X0),X1),k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(X4,k2_zfmisc_1(X1,X1),X1)
| k1_realset1(u1_lattices(X0),X1) != X4
| g3_lattices(X1,k1_realset1(u2_lattices(X0),X1),X4) != X2
| v3_struct_0(X2)
| ~ v10_lattices(X2)
| ~ l3_lattices(X2)
| ~ m1_filter_0(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(equality_resolution,[],[f37221]) ).
fof(f37364,plain,
! [X2,X0,X1] :
( k8_filter_0(X0,X1) = X2
| ~ v1_funct_1(k1_realset1(u2_lattices(X0),X1))
| ~ v1_funct_2(k1_realset1(u2_lattices(X0),X1),k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(k1_realset1(u2_lattices(X0),X1),k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(k1_realset1(u1_lattices(X0),X1))
| ~ v1_funct_2(k1_realset1(u1_lattices(X0),X1),k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(k1_realset1(u1_lattices(X0),X1),k2_zfmisc_1(X1,X1),X1)
| g3_lattices(X1,k1_realset1(u2_lattices(X0),X1),k1_realset1(u1_lattices(X0),X1)) != X2
| v3_struct_0(X2)
| ~ v10_lattices(X2)
| ~ l3_lattices(X2)
| ~ m1_filter_0(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(equality_resolution,[],[f37363]) ).
fof(f37365,plain,
! [X0,X1] :
( k8_filter_0(X0,X1) = g3_lattices(X1,k1_realset1(u2_lattices(X0),X1),k1_realset1(u1_lattices(X0),X1))
| ~ v1_funct_1(k1_realset1(u2_lattices(X0),X1))
| ~ v1_funct_2(k1_realset1(u2_lattices(X0),X1),k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(k1_realset1(u2_lattices(X0),X1),k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(k1_realset1(u1_lattices(X0),X1))
| ~ v1_funct_2(k1_realset1(u1_lattices(X0),X1),k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(k1_realset1(u1_lattices(X0),X1),k2_zfmisc_1(X1,X1),X1)
| v3_struct_0(g3_lattices(X1,k1_realset1(u2_lattices(X0),X1),k1_realset1(u1_lattices(X0),X1)))
| ~ v10_lattices(g3_lattices(X1,k1_realset1(u2_lattices(X0),X1),k1_realset1(u1_lattices(X0),X1)))
| ~ l3_lattices(g3_lattices(X1,k1_realset1(u2_lattices(X0),X1),k1_realset1(u1_lattices(X0),X1)))
| ~ m1_filter_0(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(equality_resolution,[],[f37364]) ).
fof(f37369,plain,
! [X0,X1] :
( v1_funct_1(sK169(X0,X1,k8_filter_0(X0,X1)))
| v3_struct_0(k8_filter_0(X0,X1))
| ~ v10_lattices(k8_filter_0(X0,X1))
| ~ l3_lattices(k8_filter_0(X0,X1))
| ~ m1_filter_0(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(equality_resolution,[],[f37217]) ).
fof(f37370,plain,
! [X0,X1] :
( v1_funct_2(sK169(X0,X1,k8_filter_0(X0,X1)),k2_zfmisc_1(X1,X1),X1)
| v3_struct_0(k8_filter_0(X0,X1))
| ~ v10_lattices(k8_filter_0(X0,X1))
| ~ l3_lattices(k8_filter_0(X0,X1))
| ~ m1_filter_0(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(equality_resolution,[],[f37216]) ).
fof(f37371,plain,
! [X0,X1] :
( m2_relset_1(sK169(X0,X1,k8_filter_0(X0,X1)),k2_zfmisc_1(X1,X1),X1)
| v3_struct_0(k8_filter_0(X0,X1))
| ~ v10_lattices(k8_filter_0(X0,X1))
| ~ l3_lattices(k8_filter_0(X0,X1))
| ~ m1_filter_0(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(equality_resolution,[],[f37215]) ).
fof(f37373,plain,
! [X0,X1] :
( k1_realset1(u1_lattices(X0),X1) = sK169(X0,X1,k8_filter_0(X0,X1))
| v3_struct_0(k8_filter_0(X0,X1))
| ~ v10_lattices(k8_filter_0(X0,X1))
| ~ l3_lattices(k8_filter_0(X0,X1))
| ~ m1_filter_0(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(equality_resolution,[],[f37213]) ).
fof(f37535,definition,
( spl226_1
<=> v3_struct_0(sK32) ),
introduced(definition,[new_symbols(definition,[spl226_1])],[avatar_definition]) ).
fof(f37537,plain,
( ~ v3_struct_0(sK32)
| spl226_1 ),
inference(avatar_component_clause,[],[f37535]) ).
fof(f37538,plain,
~ spl226_1,
inference(avatar_split_clause,[],[f36290,f37535]) ).
fof(f37540,definition,
( spl226_2
<=> g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),u1_lattices(sK32)) = k23_filter_2(sK32,k1_filter_2(sK32)) ),
introduced(definition,[new_symbols(definition,[spl226_2])],[avatar_definition]) ).
fof(f37542,plain,
( g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),u1_lattices(sK32)) != k23_filter_2(sK32,k1_filter_2(sK32))
| spl226_2 ),
inference(avatar_component_clause,[],[f37540]) ).
fof(f37544,definition,
( spl226_3
<=> g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),u1_lattices(sK32)) = k23_filter_2(sK32,k17_filter_2(sK32)) ),
introduced(definition,[new_symbols(definition,[spl226_3])],[avatar_definition]) ).
fof(f37546,plain,
( g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),u1_lattices(sK32)) != k23_filter_2(sK32,k17_filter_2(sK32))
| spl226_3 ),
inference(avatar_component_clause,[],[f37544]) ).
fof(f37547,plain,
( ~ spl226_2
| ~ spl226_3 ),
inference(avatar_split_clause,[],[f36291,f37544,f37540]) ).
fof(f37549,definition,
( spl226_4
<=> l3_lattices(sK32) ),
introduced(definition,[new_symbols(definition,[spl226_4])],[avatar_definition]) ).
fof(f37551,plain,
( l3_lattices(sK32)
| ~ spl226_4 ),
inference(avatar_component_clause,[],[f37549]) ).
fof(f37552,plain,
spl226_4,
inference(avatar_split_clause,[],[f36288,f37549]) ).
fof(f37554,definition,
( spl226_5
<=> v10_lattices(sK32) ),
introduced(definition,[new_symbols(definition,[spl226_5])],[avatar_definition]) ).
fof(f37556,plain,
( v10_lattices(sK32)
| ~ spl226_5 ),
inference(avatar_component_clause,[],[f37554]) ).
fof(f37557,plain,
spl226_5,
inference(avatar_split_clause,[],[f36289,f37554]) ).
fof(f37585,plain,
( k23_filter_2(sK32,k1_filter_2(sK32)) != k1_lattice2(k1_lattice2(sK32))
| v3_struct_0(sK32)
| ~ v10_lattices(sK32)
| ~ l3_lattices(sK32)
| spl226_2 ),
inference(superposition,[],[f37542,f36015]) ).
fof(f37586,plain,
( k23_filter_2(sK32,k1_filter_2(sK32)) != k1_lattice2(k1_lattice2(sK32))
| ~ v10_lattices(sK32)
| ~ l3_lattices(sK32)
| spl226_1
| spl226_2 ),
inference(forward_subsumption_resolution,[],[f37585,f37537]) ).
fof(f37614,plain,
( k23_filter_2(sK32,k1_filter_2(sK32)) != k1_lattice2(k1_lattice2(sK32))
| ~ l3_lattices(sK32)
| spl226_1
| spl226_2
| ~ spl226_5 ),
inference(forward_subsumption_resolution,[],[f37586,f37556]) ).
fof(f37641,plain,
( k23_filter_2(sK32,k1_filter_2(sK32)) != k1_lattice2(k1_lattice2(sK32))
| spl226_1
| spl226_2
| ~ spl226_4
| ~ spl226_5 ),
inference(forward_subsumption_resolution,[],[f37614,f37551]) ).
fof(f37677,plain,
( k1_filter_2(sK32) = k1_filter_0(sK32)
| v3_struct_0(sK32)
| ~ l3_lattices(sK32)
| ~ spl226_5 ),
inference(resolution,[],[f37556,f35958]) ).
fof(f37718,plain,
( g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),u1_lattices(sK32)) = k1_lattice2(k1_lattice2(sK32))
| v3_struct_0(sK32)
| ~ l3_lattices(sK32)
| ~ spl226_5 ),
inference(resolution,[],[f37556,f36015]) ).
fof(f37793,plain,
( u1_struct_0(sK32) = k17_filter_2(sK32)
| v3_struct_0(sK32)
| ~ l3_lattices(sK32)
| ~ spl226_5 ),
inference(resolution,[],[f37556,f36102]) ).
fof(f37951,plain,
( m1_filter_0(u1_struct_0(sK32),sK32)
| v3_struct_0(sK32)
| ~ l3_lattices(sK32)
| ~ spl226_5 ),
inference(resolution,[],[f37556,f36321]) ).
fof(f37991,plain,
( u1_struct_0(sK32) = k1_filter_0(sK32)
| v3_struct_0(sK32)
| ~ l3_lattices(sK32)
| ~ spl226_5 ),
inference(resolution,[],[f37556,f36388]) ).
fof(f38043,plain,
( m2_nat_lat(sK32,sK32)
| v3_struct_0(sK32)
| ~ l3_lattices(sK32)
| ~ spl226_5 ),
inference(resolution,[],[f37556,f36474]) ).
fof(f38217,plain,
( v10_lattices(k1_lattice2(sK32))
| v3_struct_0(sK32)
| ~ l3_lattices(sK32)
| ~ spl226_5 ),
inference(resolution,[],[f37556,f37036]) ).
fof(f38610,plain,
( v10_lattices(k1_lattice2(sK32))
| ~ l3_lattices(sK32)
| spl226_1
| ~ spl226_5 ),
inference(forward_subsumption_resolution,[],[f38217,f37537]) ).
fof(f38784,plain,
( m2_nat_lat(sK32,sK32)
| ~ l3_lattices(sK32)
| spl226_1
| ~ spl226_5 ),
inference(forward_subsumption_resolution,[],[f38043,f37537]) ).
fof(f38836,plain,
( u1_struct_0(sK32) = k1_filter_0(sK32)
| ~ l3_lattices(sK32)
| spl226_1
| ~ spl226_5 ),
inference(forward_subsumption_resolution,[],[f37991,f37537]) ).
fof(f38876,plain,
( m1_filter_0(u1_struct_0(sK32),sK32)
| ~ l3_lattices(sK32)
| spl226_1
| ~ spl226_5 ),
inference(forward_subsumption_resolution,[],[f37951,f37537]) ).
fof(f39032,plain,
( u1_struct_0(sK32) = k17_filter_2(sK32)
| ~ l3_lattices(sK32)
| spl226_1
| ~ spl226_5 ),
inference(forward_subsumption_resolution,[],[f37793,f37537]) ).
fof(f39107,plain,
( g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),u1_lattices(sK32)) = k1_lattice2(k1_lattice2(sK32))
| ~ l3_lattices(sK32)
| spl226_1
| ~ spl226_5 ),
inference(forward_subsumption_resolution,[],[f37718,f37537]) ).
fof(f39148,plain,
( k1_filter_2(sK32) = k1_filter_0(sK32)
| ~ l3_lattices(sK32)
| spl226_1
| ~ spl226_5 ),
inference(forward_subsumption_resolution,[],[f37677,f37537]) ).
fof(f39350,plain,
( v10_lattices(k1_lattice2(sK32))
| spl226_1
| ~ spl226_4
| ~ spl226_5 ),
inference(forward_subsumption_resolution,[],[f38610,f37551]) ).
fof(f39524,plain,
( m2_nat_lat(sK32,sK32)
| spl226_1
| ~ spl226_4
| ~ spl226_5 ),
inference(forward_subsumption_resolution,[],[f38784,f37551]) ).
fof(f39576,plain,
( u1_struct_0(sK32) = k1_filter_0(sK32)
| spl226_1
| ~ spl226_4
| ~ spl226_5 ),
inference(forward_subsumption_resolution,[],[f38836,f37551]) ).
fof(f39616,plain,
( m1_filter_0(u1_struct_0(sK32),sK32)
| spl226_1
| ~ spl226_4
| ~ spl226_5 ),
inference(forward_subsumption_resolution,[],[f38876,f37551]) ).
fof(f39772,plain,
( u1_struct_0(sK32) = k17_filter_2(sK32)
| spl226_1
| ~ spl226_4
| ~ spl226_5 ),
inference(forward_subsumption_resolution,[],[f39032,f37551]) ).
fof(f39847,plain,
( g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),u1_lattices(sK32)) = k1_lattice2(k1_lattice2(sK32))
| spl226_1
| ~ spl226_4
| ~ spl226_5 ),
inference(forward_subsumption_resolution,[],[f39107,f37551]) ).
fof(f39888,plain,
( k1_filter_2(sK32) = k1_filter_0(sK32)
| spl226_1
| ~ spl226_4
| ~ spl226_5 ),
inference(forward_subsumption_resolution,[],[f39148,f37551]) ).
fof(f39969,plain,
( u1_struct_0(sK32) = k1_filter_2(sK32)
| spl226_1
| ~ spl226_4
| ~ spl226_5 ),
inference(forward_demodulation,[],[f39888,f39576]) ).
fof(f40409,plain,
( l3_lattices(k1_lattice2(sK32))
| ~ spl226_4 ),
inference(resolution,[],[f37551,f36443]) ).
fof(f40424,plain,
( ~ v3_struct_0(k1_lattice2(sK32))
| v3_struct_0(sK32)
| ~ spl226_4 ),
inference(resolution,[],[f37551,f36469]) ).
fof(f40980,plain,
( ~ v3_struct_0(k1_lattice2(sK32))
| spl226_1
| ~ spl226_4 ),
inference(forward_subsumption_resolution,[],[f40424,f37537]) ).
fof(f42137,definition,
( spl226_6
<=> u1_struct_0(sK32) = k17_filter_2(sK32) ),
introduced(definition,[new_symbols(definition,[spl226_6])],[avatar_definition]) ).
fof(f42139,plain,
( u1_struct_0(sK32) = k17_filter_2(sK32)
| ~ spl226_6 ),
inference(avatar_component_clause,[],[f42137]) ).
fof(f42140,plain,
( spl226_6
| spl226_1
| ~ spl226_4
| ~ spl226_5 ),
inference(avatar_split_clause,[],[f39772,f37554,f37549,f37535,f42137]) ).
fof(f42167,definition,
( spl226_8
<=> k23_filter_2(sK32,k1_filter_2(sK32)) = k1_lattice2(k1_lattice2(sK32)) ),
introduced(definition,[new_symbols(definition,[spl226_8])],[avatar_definition]) ).
fof(f42169,plain,
( k23_filter_2(sK32,k1_filter_2(sK32)) != k1_lattice2(k1_lattice2(sK32))
| spl226_8 ),
inference(avatar_component_clause,[],[f42167]) ).
fof(f42170,plain,
( ~ spl226_8
| spl226_1
| spl226_2
| ~ spl226_4
| ~ spl226_5 ),
inference(avatar_split_clause,[],[f37641,f37554,f37549,f37540,f37535,f42167]) ).
fof(f42171,plain,
( k1_lattice2(k1_lattice2(sK32)) != k23_filter_2(sK32,u1_struct_0(sK32))
| spl226_1
| ~ spl226_4
| ~ spl226_5
| spl226_8 ),
inference(forward_demodulation,[],[f42169,f39969]) ).
fof(f42954,definition,
( spl226_15
<=> u1_struct_0(sK32) = k1_filter_2(sK32) ),
introduced(definition,[new_symbols(definition,[spl226_15])],[avatar_definition]) ).
fof(f42956,plain,
( u1_struct_0(sK32) = k1_filter_2(sK32)
| ~ spl226_15 ),
inference(avatar_component_clause,[],[f42954]) ).
fof(f42957,plain,
( spl226_15
| spl226_1
| ~ spl226_4
| ~ spl226_5 ),
inference(avatar_split_clause,[],[f39969,f37554,f37549,f37535,f42954]) ).
fof(f42960,plain,
( m1_filter_2(u1_struct_0(sK32),sK32)
| v3_struct_0(sK32)
| ~ v10_lattices(sK32)
| ~ l3_lattices(sK32)
| ~ spl226_15 ),
inference(superposition,[],[f35957,f42956]) ).
fof(f42961,plain,
( m1_filter_2(u1_struct_0(sK32),sK32)
| ~ v10_lattices(sK32)
| ~ l3_lattices(sK32)
| spl226_1
| ~ spl226_15 ),
inference(forward_subsumption_resolution,[],[f42960,f37537]) ).
fof(f42962,plain,
( m1_filter_2(u1_struct_0(sK32),sK32)
| ~ l3_lattices(sK32)
| spl226_1
| ~ spl226_5
| ~ spl226_15 ),
inference(forward_subsumption_resolution,[],[f42961,f37556]) ).
fof(f42963,plain,
( m1_filter_2(u1_struct_0(sK32),sK32)
| spl226_1
| ~ spl226_4
| ~ spl226_5
| ~ spl226_15 ),
inference(forward_subsumption_resolution,[],[f42962,f37551]) ).
fof(f42965,definition,
( spl226_16
<=> m1_filter_0(u1_struct_0(sK32),sK32) ),
introduced(definition,[new_symbols(definition,[spl226_16])],[avatar_definition]) ).
fof(f42967,plain,
( m1_filter_0(u1_struct_0(sK32),sK32)
| ~ spl226_16 ),
inference(avatar_component_clause,[],[f42965]) ).
fof(f42968,plain,
( spl226_16
| spl226_1
| ~ spl226_4
| ~ spl226_5 ),
inference(avatar_split_clause,[],[f39616,f37554,f37549,f37535,f42965]) ).
fof(f42983,plain,
( ~ v1_xboole_0(u1_struct_0(sK32))
| v3_struct_0(sK32)
| ~ v10_lattices(sK32)
| ~ l3_lattices(sK32)
| ~ spl226_16 ),
inference(resolution,[],[f42967,f36320]) ).
fof(f43034,plain,
( l3_lattices(k8_filter_0(sK32,u1_struct_0(sK32)))
| v3_struct_0(sK32)
| ~ v10_lattices(sK32)
| ~ l3_lattices(sK32)
| ~ spl226_16 ),
inference(resolution,[],[f42967,f37198]) ).
fof(f43043,plain,
( v10_lattices(k8_filter_0(sK32,u1_struct_0(sK32)))
| v3_struct_0(sK32)
| ~ v10_lattices(sK32)
| ~ l3_lattices(sK32)
| ~ spl226_16 ),
inference(resolution,[],[f42967,f37222]) ).
fof(f43051,plain,
( ~ v3_struct_0(k8_filter_0(sK32,u1_struct_0(sK32)))
| v3_struct_0(sK32)
| ~ v10_lattices(sK32)
| ~ l3_lattices(sK32)
| ~ spl226_16 ),
inference(resolution,[],[f42967,f37230]) ).
fof(f43063,plain,
( v1_funct_1(sK169(sK32,u1_struct_0(sK32),k8_filter_0(sK32,u1_struct_0(sK32))))
| v3_struct_0(k8_filter_0(sK32,u1_struct_0(sK32)))
| ~ v10_lattices(k8_filter_0(sK32,u1_struct_0(sK32)))
| ~ l3_lattices(k8_filter_0(sK32,u1_struct_0(sK32)))
| v3_struct_0(sK32)
| ~ v10_lattices(sK32)
| ~ l3_lattices(sK32)
| ~ spl226_16 ),
inference(resolution,[],[f42967,f37369]) ).
fof(f43064,plain,
( v1_funct_2(sK169(sK32,u1_struct_0(sK32),k8_filter_0(sK32,u1_struct_0(sK32))),k2_zfmisc_1(u1_struct_0(sK32),u1_struct_0(sK32)),u1_struct_0(sK32))
| v3_struct_0(k8_filter_0(sK32,u1_struct_0(sK32)))
| ~ v10_lattices(k8_filter_0(sK32,u1_struct_0(sK32)))
| ~ l3_lattices(k8_filter_0(sK32,u1_struct_0(sK32)))
| v3_struct_0(sK32)
| ~ v10_lattices(sK32)
| ~ l3_lattices(sK32)
| ~ spl226_16 ),
inference(resolution,[],[f42967,f37370]) ).
fof(f43065,plain,
( m2_relset_1(sK169(sK32,u1_struct_0(sK32),k8_filter_0(sK32,u1_struct_0(sK32))),k2_zfmisc_1(u1_struct_0(sK32),u1_struct_0(sK32)),u1_struct_0(sK32))
| v3_struct_0(k8_filter_0(sK32,u1_struct_0(sK32)))
| ~ v10_lattices(k8_filter_0(sK32,u1_struct_0(sK32)))
| ~ l3_lattices(k8_filter_0(sK32,u1_struct_0(sK32)))
| v3_struct_0(sK32)
| ~ v10_lattices(sK32)
| ~ l3_lattices(sK32)
| ~ spl226_16 ),
inference(resolution,[],[f42967,f37371]) ).
fof(f43067,plain,
( k1_realset1(u1_lattices(sK32),u1_struct_0(sK32)) = sK169(sK32,u1_struct_0(sK32),k8_filter_0(sK32,u1_struct_0(sK32)))
| v3_struct_0(k8_filter_0(sK32,u1_struct_0(sK32)))
| ~ v10_lattices(k8_filter_0(sK32,u1_struct_0(sK32)))
| ~ l3_lattices(k8_filter_0(sK32,u1_struct_0(sK32)))
| v3_struct_0(sK32)
| ~ v10_lattices(sK32)
| ~ l3_lattices(sK32)
| ~ spl226_16 ),
inference(resolution,[],[f42967,f37373]) ).
fof(f43115,plain,
( k1_realset1(u1_lattices(sK32),u1_struct_0(sK32)) = sK169(sK32,u1_struct_0(sK32),k8_filter_0(sK32,u1_struct_0(sK32)))
| v3_struct_0(k8_filter_0(sK32,u1_struct_0(sK32)))
| ~ v10_lattices(k8_filter_0(sK32,u1_struct_0(sK32)))
| ~ l3_lattices(k8_filter_0(sK32,u1_struct_0(sK32)))
| ~ v10_lattices(sK32)
| ~ l3_lattices(sK32)
| spl226_1
| ~ spl226_16 ),
inference(forward_subsumption_resolution,[],[f43067,f37537]) ).
fof(f43117,plain,
( m2_relset_1(sK169(sK32,u1_struct_0(sK32),k8_filter_0(sK32,u1_struct_0(sK32))),k2_zfmisc_1(u1_struct_0(sK32),u1_struct_0(sK32)),u1_struct_0(sK32))
| v3_struct_0(k8_filter_0(sK32,u1_struct_0(sK32)))
| ~ v10_lattices(k8_filter_0(sK32,u1_struct_0(sK32)))
| ~ l3_lattices(k8_filter_0(sK32,u1_struct_0(sK32)))
| ~ v10_lattices(sK32)
| ~ l3_lattices(sK32)
| spl226_1
| ~ spl226_16 ),
inference(forward_subsumption_resolution,[],[f43065,f37537]) ).
fof(f43118,plain,
( v1_funct_2(sK169(sK32,u1_struct_0(sK32),k8_filter_0(sK32,u1_struct_0(sK32))),k2_zfmisc_1(u1_struct_0(sK32),u1_struct_0(sK32)),u1_struct_0(sK32))
| v3_struct_0(k8_filter_0(sK32,u1_struct_0(sK32)))
| ~ v10_lattices(k8_filter_0(sK32,u1_struct_0(sK32)))
| ~ l3_lattices(k8_filter_0(sK32,u1_struct_0(sK32)))
| ~ v10_lattices(sK32)
| ~ l3_lattices(sK32)
| spl226_1
| ~ spl226_16 ),
inference(forward_subsumption_resolution,[],[f43064,f37537]) ).
fof(f43119,plain,
( v1_funct_1(sK169(sK32,u1_struct_0(sK32),k8_filter_0(sK32,u1_struct_0(sK32))))
| v3_struct_0(k8_filter_0(sK32,u1_struct_0(sK32)))
| ~ v10_lattices(k8_filter_0(sK32,u1_struct_0(sK32)))
| ~ l3_lattices(k8_filter_0(sK32,u1_struct_0(sK32)))
| ~ v10_lattices(sK32)
| ~ l3_lattices(sK32)
| spl226_1
| ~ spl226_16 ),
inference(forward_subsumption_resolution,[],[f43063,f37537]) ).
fof(f43129,plain,
( ~ v3_struct_0(k8_filter_0(sK32,u1_struct_0(sK32)))
| ~ v10_lattices(sK32)
| ~ l3_lattices(sK32)
| spl226_1
| ~ spl226_16 ),
inference(forward_subsumption_resolution,[],[f43051,f37537]) ).
fof(f43137,plain,
( v10_lattices(k8_filter_0(sK32,u1_struct_0(sK32)))
| ~ v10_lattices(sK32)
| ~ l3_lattices(sK32)
| spl226_1
| ~ spl226_16 ),
inference(forward_subsumption_resolution,[],[f43043,f37537]) ).
fof(f43146,plain,
( l3_lattices(k8_filter_0(sK32,u1_struct_0(sK32)))
| ~ v10_lattices(sK32)
| ~ l3_lattices(sK32)
| spl226_1
| ~ spl226_16 ),
inference(forward_subsumption_resolution,[],[f43034,f37537]) ).
fof(f43172,plain,
( ~ v1_xboole_0(u1_struct_0(sK32))
| ~ v10_lattices(sK32)
| ~ l3_lattices(sK32)
| spl226_1
| ~ spl226_16 ),
inference(forward_subsumption_resolution,[],[f42983,f37537]) ).
fof(f43197,plain,
( k1_realset1(u1_lattices(sK32),u1_struct_0(sK32)) = sK169(sK32,u1_struct_0(sK32),k8_filter_0(sK32,u1_struct_0(sK32)))
| v3_struct_0(k8_filter_0(sK32,u1_struct_0(sK32)))
| ~ v10_lattices(k8_filter_0(sK32,u1_struct_0(sK32)))
| ~ l3_lattices(k8_filter_0(sK32,u1_struct_0(sK32)))
| ~ l3_lattices(sK32)
| spl226_1
| ~ spl226_5
| ~ spl226_16 ),
inference(forward_subsumption_resolution,[],[f43115,f37556]) ).
fof(f43199,plain,
( m2_relset_1(sK169(sK32,u1_struct_0(sK32),k8_filter_0(sK32,u1_struct_0(sK32))),k2_zfmisc_1(u1_struct_0(sK32),u1_struct_0(sK32)),u1_struct_0(sK32))
| v3_struct_0(k8_filter_0(sK32,u1_struct_0(sK32)))
| ~ v10_lattices(k8_filter_0(sK32,u1_struct_0(sK32)))
| ~ l3_lattices(k8_filter_0(sK32,u1_struct_0(sK32)))
| ~ l3_lattices(sK32)
| spl226_1
| ~ spl226_5
| ~ spl226_16 ),
inference(forward_subsumption_resolution,[],[f43117,f37556]) ).
fof(f43200,plain,
( v1_funct_2(sK169(sK32,u1_struct_0(sK32),k8_filter_0(sK32,u1_struct_0(sK32))),k2_zfmisc_1(u1_struct_0(sK32),u1_struct_0(sK32)),u1_struct_0(sK32))
| v3_struct_0(k8_filter_0(sK32,u1_struct_0(sK32)))
| ~ v10_lattices(k8_filter_0(sK32,u1_struct_0(sK32)))
| ~ l3_lattices(k8_filter_0(sK32,u1_struct_0(sK32)))
| ~ l3_lattices(sK32)
| spl226_1
| ~ spl226_5
| ~ spl226_16 ),
inference(forward_subsumption_resolution,[],[f43118,f37556]) ).
fof(f43201,plain,
( v1_funct_1(sK169(sK32,u1_struct_0(sK32),k8_filter_0(sK32,u1_struct_0(sK32))))
| v3_struct_0(k8_filter_0(sK32,u1_struct_0(sK32)))
| ~ v10_lattices(k8_filter_0(sK32,u1_struct_0(sK32)))
| ~ l3_lattices(k8_filter_0(sK32,u1_struct_0(sK32)))
| ~ l3_lattices(sK32)
| spl226_1
| ~ spl226_5
| ~ spl226_16 ),
inference(forward_subsumption_resolution,[],[f43119,f37556]) ).
fof(f43211,plain,
( ~ v3_struct_0(k8_filter_0(sK32,u1_struct_0(sK32)))
| ~ l3_lattices(sK32)
| spl226_1
| ~ spl226_5
| ~ spl226_16 ),
inference(forward_subsumption_resolution,[],[f43129,f37556]) ).
fof(f43219,plain,
( v10_lattices(k8_filter_0(sK32,u1_struct_0(sK32)))
| ~ l3_lattices(sK32)
| spl226_1
| ~ spl226_5
| ~ spl226_16 ),
inference(forward_subsumption_resolution,[],[f43137,f37556]) ).
fof(f43228,plain,
( l3_lattices(k8_filter_0(sK32,u1_struct_0(sK32)))
| ~ l3_lattices(sK32)
| spl226_1
| ~ spl226_5
| ~ spl226_16 ),
inference(forward_subsumption_resolution,[],[f43146,f37556]) ).
fof(f43253,plain,
( ~ v1_xboole_0(u1_struct_0(sK32))
| ~ l3_lattices(sK32)
| spl226_1
| ~ spl226_5
| ~ spl226_16 ),
inference(forward_subsumption_resolution,[],[f43172,f37556]) ).
fof(f43278,plain,
( k1_realset1(u1_lattices(sK32),u1_struct_0(sK32)) = sK169(sK32,u1_struct_0(sK32),k8_filter_0(sK32,u1_struct_0(sK32)))
| v3_struct_0(k8_filter_0(sK32,u1_struct_0(sK32)))
| ~ v10_lattices(k8_filter_0(sK32,u1_struct_0(sK32)))
| ~ l3_lattices(k8_filter_0(sK32,u1_struct_0(sK32)))
| spl226_1
| ~ spl226_4
| ~ spl226_5
| ~ spl226_16 ),
inference(forward_subsumption_resolution,[],[f43197,f37551]) ).
fof(f43280,plain,
( m2_relset_1(sK169(sK32,u1_struct_0(sK32),k8_filter_0(sK32,u1_struct_0(sK32))),k2_zfmisc_1(u1_struct_0(sK32),u1_struct_0(sK32)),u1_struct_0(sK32))
| v3_struct_0(k8_filter_0(sK32,u1_struct_0(sK32)))
| ~ v10_lattices(k8_filter_0(sK32,u1_struct_0(sK32)))
| ~ l3_lattices(k8_filter_0(sK32,u1_struct_0(sK32)))
| spl226_1
| ~ spl226_4
| ~ spl226_5
| ~ spl226_16 ),
inference(forward_subsumption_resolution,[],[f43199,f37551]) ).
fof(f43281,plain,
( v1_funct_2(sK169(sK32,u1_struct_0(sK32),k8_filter_0(sK32,u1_struct_0(sK32))),k2_zfmisc_1(u1_struct_0(sK32),u1_struct_0(sK32)),u1_struct_0(sK32))
| v3_struct_0(k8_filter_0(sK32,u1_struct_0(sK32)))
| ~ v10_lattices(k8_filter_0(sK32,u1_struct_0(sK32)))
| ~ l3_lattices(k8_filter_0(sK32,u1_struct_0(sK32)))
| spl226_1
| ~ spl226_4
| ~ spl226_5
| ~ spl226_16 ),
inference(forward_subsumption_resolution,[],[f43200,f37551]) ).
fof(f43282,plain,
( v1_funct_1(sK169(sK32,u1_struct_0(sK32),k8_filter_0(sK32,u1_struct_0(sK32))))
| v3_struct_0(k8_filter_0(sK32,u1_struct_0(sK32)))
| ~ v10_lattices(k8_filter_0(sK32,u1_struct_0(sK32)))
| ~ l3_lattices(k8_filter_0(sK32,u1_struct_0(sK32)))
| spl226_1
| ~ spl226_4
| ~ spl226_5
| ~ spl226_16 ),
inference(forward_subsumption_resolution,[],[f43201,f37551]) ).
fof(f43292,plain,
( ~ v3_struct_0(k8_filter_0(sK32,u1_struct_0(sK32)))
| spl226_1
| ~ spl226_4
| ~ spl226_5
| ~ spl226_16 ),
inference(forward_subsumption_resolution,[],[f43211,f37551]) ).
fof(f43300,plain,
( v10_lattices(k8_filter_0(sK32,u1_struct_0(sK32)))
| spl226_1
| ~ spl226_4
| ~ spl226_5
| ~ spl226_16 ),
inference(forward_subsumption_resolution,[],[f43219,f37551]) ).
fof(f43309,plain,
( l3_lattices(k8_filter_0(sK32,u1_struct_0(sK32)))
| spl226_1
| ~ spl226_4
| ~ spl226_5
| ~ spl226_16 ),
inference(forward_subsumption_resolution,[],[f43228,f37551]) ).
fof(f43334,plain,
( ~ v1_xboole_0(u1_struct_0(sK32))
| spl226_1
| ~ spl226_4
| ~ spl226_5
| ~ spl226_16 ),
inference(forward_subsumption_resolution,[],[f43253,f37551]) ).
fof(f43346,plain,
( k1_realset1(u1_lattices(sK32),u1_struct_0(sK32)) = sK169(sK32,u1_struct_0(sK32),k8_filter_0(sK32,u1_struct_0(sK32)))
| ~ v10_lattices(k8_filter_0(sK32,u1_struct_0(sK32)))
| ~ l3_lattices(k8_filter_0(sK32,u1_struct_0(sK32)))
| spl226_1
| ~ spl226_4
| ~ spl226_5
| ~ spl226_16 ),
inference(backward_subsumption_resolution,[],[f43278,f43292]) ).
fof(f43348,plain,
( m2_relset_1(sK169(sK32,u1_struct_0(sK32),k8_filter_0(sK32,u1_struct_0(sK32))),k2_zfmisc_1(u1_struct_0(sK32),u1_struct_0(sK32)),u1_struct_0(sK32))
| ~ v10_lattices(k8_filter_0(sK32,u1_struct_0(sK32)))
| ~ l3_lattices(k8_filter_0(sK32,u1_struct_0(sK32)))
| spl226_1
| ~ spl226_4
| ~ spl226_5
| ~ spl226_16 ),
inference(backward_subsumption_resolution,[],[f43280,f43292]) ).
fof(f43349,plain,
( v1_funct_2(sK169(sK32,u1_struct_0(sK32),k8_filter_0(sK32,u1_struct_0(sK32))),k2_zfmisc_1(u1_struct_0(sK32),u1_struct_0(sK32)),u1_struct_0(sK32))
| ~ v10_lattices(k8_filter_0(sK32,u1_struct_0(sK32)))
| ~ l3_lattices(k8_filter_0(sK32,u1_struct_0(sK32)))
| spl226_1
| ~ spl226_4
| ~ spl226_5
| ~ spl226_16 ),
inference(backward_subsumption_resolution,[],[f43281,f43292]) ).
fof(f43350,plain,
( v1_funct_1(sK169(sK32,u1_struct_0(sK32),k8_filter_0(sK32,u1_struct_0(sK32))))
| ~ v10_lattices(k8_filter_0(sK32,u1_struct_0(sK32)))
| ~ l3_lattices(k8_filter_0(sK32,u1_struct_0(sK32)))
| spl226_1
| ~ spl226_4
| ~ spl226_5
| ~ spl226_16 ),
inference(backward_subsumption_resolution,[],[f43282,f43292]) ).
fof(f43383,plain,
( k1_realset1(u1_lattices(sK32),u1_struct_0(sK32)) = sK169(sK32,u1_struct_0(sK32),k8_filter_0(sK32,u1_struct_0(sK32)))
| ~ l3_lattices(k8_filter_0(sK32,u1_struct_0(sK32)))
| spl226_1
| ~ spl226_4
| ~ spl226_5
| ~ spl226_16 ),
inference(forward_subsumption_resolution,[],[f43346,f43300]) ).
fof(f43385,plain,
( m2_relset_1(sK169(sK32,u1_struct_0(sK32),k8_filter_0(sK32,u1_struct_0(sK32))),k2_zfmisc_1(u1_struct_0(sK32),u1_struct_0(sK32)),u1_struct_0(sK32))
| ~ l3_lattices(k8_filter_0(sK32,u1_struct_0(sK32)))
| spl226_1
| ~ spl226_4
| ~ spl226_5
| ~ spl226_16 ),
inference(forward_subsumption_resolution,[],[f43348,f43300]) ).
fof(f43386,plain,
( v1_funct_2(sK169(sK32,u1_struct_0(sK32),k8_filter_0(sK32,u1_struct_0(sK32))),k2_zfmisc_1(u1_struct_0(sK32),u1_struct_0(sK32)),u1_struct_0(sK32))
| ~ l3_lattices(k8_filter_0(sK32,u1_struct_0(sK32)))
| spl226_1
| ~ spl226_4
| ~ spl226_5
| ~ spl226_16 ),
inference(forward_subsumption_resolution,[],[f43349,f43300]) ).
fof(f43387,plain,
( v1_funct_1(sK169(sK32,u1_struct_0(sK32),k8_filter_0(sK32,u1_struct_0(sK32))))
| ~ l3_lattices(k8_filter_0(sK32,u1_struct_0(sK32)))
| spl226_1
| ~ spl226_4
| ~ spl226_5
| ~ spl226_16 ),
inference(forward_subsumption_resolution,[],[f43350,f43300]) ).
fof(f43394,plain,
( k1_realset1(u1_lattices(sK32),u1_struct_0(sK32)) = sK169(sK32,u1_struct_0(sK32),k8_filter_0(sK32,u1_struct_0(sK32)))
| spl226_1
| ~ spl226_4
| ~ spl226_5
| ~ spl226_16 ),
inference(forward_subsumption_resolution,[],[f43383,f43309]) ).
fof(f43396,plain,
( m2_relset_1(sK169(sK32,u1_struct_0(sK32),k8_filter_0(sK32,u1_struct_0(sK32))),k2_zfmisc_1(u1_struct_0(sK32),u1_struct_0(sK32)),u1_struct_0(sK32))
| spl226_1
| ~ spl226_4
| ~ spl226_5
| ~ spl226_16 ),
inference(forward_subsumption_resolution,[],[f43385,f43309]) ).
fof(f43397,plain,
( v1_funct_2(sK169(sK32,u1_struct_0(sK32),k8_filter_0(sK32,u1_struct_0(sK32))),k2_zfmisc_1(u1_struct_0(sK32),u1_struct_0(sK32)),u1_struct_0(sK32))
| spl226_1
| ~ spl226_4
| ~ spl226_5
| ~ spl226_16 ),
inference(forward_subsumption_resolution,[],[f43386,f43309]) ).
fof(f43398,plain,
( v1_funct_1(sK169(sK32,u1_struct_0(sK32),k8_filter_0(sK32,u1_struct_0(sK32))))
| spl226_1
| ~ spl226_4
| ~ spl226_5
| ~ spl226_16 ),
inference(forward_subsumption_resolution,[],[f43387,f43309]) ).
fof(f43404,plain,
( m2_relset_1(k1_realset1(u1_lattices(sK32),u1_struct_0(sK32)),k2_zfmisc_1(u1_struct_0(sK32),u1_struct_0(sK32)),u1_struct_0(sK32))
| spl226_1
| ~ spl226_4
| ~ spl226_5
| ~ spl226_16 ),
inference(forward_demodulation,[],[f43396,f43394]) ).
fof(f43405,plain,
( v1_funct_2(k1_realset1(u1_lattices(sK32),u1_struct_0(sK32)),k2_zfmisc_1(u1_struct_0(sK32),u1_struct_0(sK32)),u1_struct_0(sK32))
| spl226_1
| ~ spl226_4
| ~ spl226_5
| ~ spl226_16 ),
inference(forward_demodulation,[],[f43397,f43394]) ).
fof(f43406,plain,
( v1_funct_1(k1_realset1(u1_lattices(sK32),u1_struct_0(sK32)))
| spl226_1
| ~ spl226_4
| ~ spl226_5
| ~ spl226_16 ),
inference(forward_demodulation,[],[f43398,f43394]) ).
fof(f43598,definition,
( spl226_17
<=> g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),u1_lattices(sK32)) = k1_lattice2(k1_lattice2(sK32)) ),
introduced(definition,[new_symbols(definition,[spl226_17])],[avatar_definition]) ).
fof(f43600,plain,
( g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),u1_lattices(sK32)) = k1_lattice2(k1_lattice2(sK32))
| ~ spl226_17 ),
inference(avatar_component_clause,[],[f43598]) ).
fof(f43601,plain,
( spl226_17
| spl226_1
| ~ spl226_4
| ~ spl226_5 ),
inference(avatar_split_clause,[],[f39847,f37554,f37549,f37535,f43598]) ).
fof(f44109,definition,
( spl226_19
<=> m2_nat_lat(sK32,sK32) ),
introduced(definition,[new_symbols(definition,[spl226_19])],[avatar_definition]) ).
fof(f44111,plain,
( m2_nat_lat(sK32,sK32)
| ~ spl226_19 ),
inference(avatar_component_clause,[],[f44109]) ).
fof(f44112,plain,
( spl226_19
| spl226_1
| ~ spl226_4
| ~ spl226_5 ),
inference(avatar_split_clause,[],[f39524,f37554,f37549,f37535,f44109]) ).
fof(f44131,plain,
( u1_lattices(sK32) = k1_realset1(u1_lattices(sK32),u1_struct_0(sK32))
| v3_struct_0(sK32)
| ~ v10_lattices(sK32)
| ~ l3_lattices(sK32)
| v3_struct_0(sK32)
| ~ v10_lattices(sK32)
| ~ l3_lattices(sK32)
| ~ spl226_19 ),
inference(resolution,[],[f44111,f36475]) ).
fof(f44132,plain,
( u2_lattices(sK32) = k1_realset1(u2_lattices(sK32),u1_struct_0(sK32))
| v3_struct_0(sK32)
| ~ v10_lattices(sK32)
| ~ l3_lattices(sK32)
| v3_struct_0(sK32)
| ~ v10_lattices(sK32)
| ~ l3_lattices(sK32)
| ~ spl226_19 ),
inference(resolution,[],[f44111,f36476]) ).
fof(f44135,plain,
( u2_lattices(sK32) = k1_realset1(u2_lattices(sK32),u1_struct_0(sK32))
| v3_struct_0(sK32)
| ~ v10_lattices(sK32)
| ~ l3_lattices(sK32)
| ~ spl226_19 ),
inference(duplicate_literal_removal,[],[f44132]) ).
fof(f44136,plain,
( u1_lattices(sK32) = k1_realset1(u1_lattices(sK32),u1_struct_0(sK32))
| v3_struct_0(sK32)
| ~ v10_lattices(sK32)
| ~ l3_lattices(sK32)
| ~ spl226_19 ),
inference(duplicate_literal_removal,[],[f44131]) ).
fof(f44148,plain,
( u2_lattices(sK32) = k1_realset1(u2_lattices(sK32),u1_struct_0(sK32))
| ~ v10_lattices(sK32)
| ~ l3_lattices(sK32)
| spl226_1
| ~ spl226_19 ),
inference(forward_subsumption_resolution,[],[f44135,f37537]) ).
fof(f44149,plain,
( u1_lattices(sK32) = k1_realset1(u1_lattices(sK32),u1_struct_0(sK32))
| ~ v10_lattices(sK32)
| ~ l3_lattices(sK32)
| spl226_1
| ~ spl226_19 ),
inference(forward_subsumption_resolution,[],[f44136,f37537]) ).
fof(f44164,plain,
( u2_lattices(sK32) = k1_realset1(u2_lattices(sK32),u1_struct_0(sK32))
| ~ l3_lattices(sK32)
| spl226_1
| ~ spl226_5
| ~ spl226_19 ),
inference(forward_subsumption_resolution,[],[f44148,f37556]) ).
fof(f44165,plain,
( u1_lattices(sK32) = k1_realset1(u1_lattices(sK32),u1_struct_0(sK32))
| ~ l3_lattices(sK32)
| spl226_1
| ~ spl226_5
| ~ spl226_19 ),
inference(forward_subsumption_resolution,[],[f44149,f37556]) ).
fof(f44180,plain,
( u2_lattices(sK32) = k1_realset1(u2_lattices(sK32),u1_struct_0(sK32))
| spl226_1
| ~ spl226_4
| ~ spl226_5
| ~ spl226_19 ),
inference(forward_subsumption_resolution,[],[f44164,f37551]) ).
fof(f44181,plain,
( u1_lattices(sK32) = k1_realset1(u1_lattices(sK32),u1_struct_0(sK32))
| spl226_1
| ~ spl226_4
| ~ spl226_5
| ~ spl226_19 ),
inference(forward_subsumption_resolution,[],[f44165,f37551]) ).
fof(f46217,definition,
( spl226_28
<=> v3_struct_0(k1_lattice2(sK32)) ),
introduced(definition,[new_symbols(definition,[spl226_28])],[avatar_definition]) ).
fof(f46219,plain,
( ~ v3_struct_0(k1_lattice2(sK32))
| spl226_28 ),
inference(avatar_component_clause,[],[f46217]) ).
fof(f46220,plain,
( ~ spl226_28
| spl226_1
| ~ spl226_4 ),
inference(avatar_split_clause,[],[f40980,f37549,f37535,f46217]) ).
fof(f46601,plain,
( ~ v3_struct_0(k1_lattice2(k1_lattice2(sK32)))
| ~ l3_lattices(k1_lattice2(sK32))
| spl226_28 ),
inference(resolution,[],[f46219,f36469]) ).
fof(f46836,plain,
( v10_lattices(k1_lattice2(k1_lattice2(sK32)))
| ~ v10_lattices(k1_lattice2(sK32))
| ~ l3_lattices(k1_lattice2(sK32))
| spl226_28 ),
inference(resolution,[],[f46219,f37036]) ).
fof(f47257,plain,
( v10_lattices(k1_lattice2(k1_lattice2(sK32)))
| ~ l3_lattices(k1_lattice2(sK32))
| spl226_1
| ~ spl226_4
| ~ spl226_5
| spl226_28 ),
inference(forward_subsumption_resolution,[],[f46836,f39350]) ).
fof(f47460,plain,
( ~ v3_struct_0(k1_lattice2(k1_lattice2(sK32)))
| ~ spl226_4
| spl226_28 ),
inference(forward_subsumption_resolution,[],[f46601,f40409]) ).
fof(f48024,plain,
( v10_lattices(k1_lattice2(k1_lattice2(sK32)))
| spl226_1
| ~ spl226_4
| ~ spl226_5
| spl226_28 ),
inference(forward_subsumption_resolution,[],[f47257,f40409]) ).
fof(f53315,definition,
( spl226_35
<=> l3_lattices(k1_lattice2(sK32)) ),
introduced(definition,[new_symbols(definition,[spl226_35])],[avatar_definition]) ).
fof(f53317,plain,
( l3_lattices(k1_lattice2(sK32))
| ~ spl226_35 ),
inference(avatar_component_clause,[],[f53315]) ).
fof(f53318,plain,
( spl226_35
| ~ spl226_4 ),
inference(avatar_split_clause,[],[f40409,f37549,f53315]) ).
fof(f55345,plain,
( l3_lattices(k1_lattice2(k1_lattice2(sK32)))
| ~ spl226_35 ),
inference(resolution,[],[f53317,f36443]) ).
fof(f63153,definition,
( spl226_77
<=> v1_xboole_0(u1_struct_0(sK32)) ),
introduced(definition,[new_symbols(definition,[spl226_77])],[avatar_definition]) ).
fof(f63155,plain,
( ~ v1_xboole_0(u1_struct_0(sK32))
| spl226_77 ),
inference(avatar_component_clause,[],[f63153]) ).
fof(f63156,plain,
( ~ spl226_77
| spl226_1
| ~ spl226_4
| ~ spl226_5
| ~ spl226_16 ),
inference(avatar_split_clause,[],[f43334,f42965,f37554,f37549,f37535,f63153]) ).
fof(f71794,definition,
( spl226_102
<=> u2_lattices(sK32) = k1_realset1(u2_lattices(sK32),u1_struct_0(sK32)) ),
introduced(definition,[new_symbols(definition,[spl226_102])],[avatar_definition]) ).
fof(f71796,plain,
( u2_lattices(sK32) = k1_realset1(u2_lattices(sK32),u1_struct_0(sK32))
| ~ spl226_102 ),
inference(avatar_component_clause,[],[f71794]) ).
fof(f71797,plain,
( spl226_102
| spl226_1
| ~ spl226_4
| ~ spl226_5
| ~ spl226_19 ),
inference(avatar_split_clause,[],[f44180,f44109,f37554,f37549,f37535,f71794]) ).
fof(f72405,definition,
( spl226_106
<=> u1_lattices(sK32) = k1_realset1(u1_lattices(sK32),u1_struct_0(sK32)) ),
introduced(definition,[new_symbols(definition,[spl226_106])],[avatar_definition]) ).
fof(f72407,plain,
( u1_lattices(sK32) = k1_realset1(u1_lattices(sK32),u1_struct_0(sK32))
| ~ spl226_106 ),
inference(avatar_component_clause,[],[f72405]) ).
fof(f72408,plain,
( spl226_106
| spl226_1
| ~ spl226_4
| ~ spl226_5
| ~ spl226_19 ),
inference(avatar_split_clause,[],[f44181,f44109,f37554,f37549,f37535,f72405]) ).
fof(f72464,plain,
( m2_relset_1(u2_lattices(sK32),k2_zfmisc_1(u1_struct_0(sK32),u1_struct_0(sK32)),u1_struct_0(sK32))
| v1_xboole_0(u1_struct_0(sK32))
| ~ m2_lattice4(u1_struct_0(sK32),sK32)
| v3_struct_0(sK32)
| ~ v10_lattices(sK32)
| ~ l3_lattices(sK32)
| ~ spl226_102 ),
inference(superposition,[],[f36235,f71796]) ).
fof(f72465,plain,
( v1_funct_2(u2_lattices(sK32),k2_zfmisc_1(u1_struct_0(sK32),u1_struct_0(sK32)),u1_struct_0(sK32))
| v1_xboole_0(u1_struct_0(sK32))
| ~ m2_lattice4(u1_struct_0(sK32),sK32)
| v3_struct_0(sK32)
| ~ v10_lattices(sK32)
| ~ l3_lattices(sK32)
| ~ spl226_102 ),
inference(superposition,[],[f36236,f71796]) ).
fof(f72466,plain,
( v1_funct_1(u2_lattices(sK32))
| v1_xboole_0(u1_struct_0(sK32))
| ~ m2_lattice4(u1_struct_0(sK32),sK32)
| v3_struct_0(sK32)
| ~ v10_lattices(sK32)
| ~ l3_lattices(sK32)
| ~ spl226_102 ),
inference(superposition,[],[f36237,f71796]) ).
fof(f72504,plain,
( ~ l3_lattices(g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),k1_realset1(u1_lattices(sK32),u1_struct_0(sK32))))
| k8_filter_0(sK32,u1_struct_0(sK32)) = g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),k1_realset1(u1_lattices(sK32),u1_struct_0(sK32)))
| ~ v1_funct_1(u2_lattices(sK32))
| ~ v1_funct_2(u2_lattices(sK32),k2_zfmisc_1(u1_struct_0(sK32),u1_struct_0(sK32)),u1_struct_0(sK32))
| ~ m2_relset_1(u2_lattices(sK32),k2_zfmisc_1(u1_struct_0(sK32),u1_struct_0(sK32)),u1_struct_0(sK32))
| ~ v1_funct_1(k1_realset1(u1_lattices(sK32),u1_struct_0(sK32)))
| ~ v1_funct_2(k1_realset1(u1_lattices(sK32),u1_struct_0(sK32)),k2_zfmisc_1(u1_struct_0(sK32),u1_struct_0(sK32)),u1_struct_0(sK32))
| ~ m2_relset_1(k1_realset1(u1_lattices(sK32),u1_struct_0(sK32)),k2_zfmisc_1(u1_struct_0(sK32),u1_struct_0(sK32)),u1_struct_0(sK32))
| v3_struct_0(g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),k1_realset1(u1_lattices(sK32),u1_struct_0(sK32))))
| ~ v10_lattices(g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),k1_realset1(u1_lattices(sK32),u1_struct_0(sK32))))
| ~ m1_filter_0(u1_struct_0(sK32),sK32)
| v3_struct_0(sK32)
| ~ v10_lattices(sK32)
| ~ l3_lattices(sK32)
| ~ spl226_102 ),
inference(superposition,[],[f37365,f71796]) ).
fof(f72666,plain,
( ~ l3_lattices(g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),k1_realset1(u1_lattices(sK32),u1_struct_0(sK32))))
| k8_filter_0(sK32,u1_struct_0(sK32)) = g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),k1_realset1(u1_lattices(sK32),u1_struct_0(sK32)))
| ~ v1_funct_1(u2_lattices(sK32))
| ~ v1_funct_2(u2_lattices(sK32),k2_zfmisc_1(u1_struct_0(sK32),u1_struct_0(sK32)),u1_struct_0(sK32))
| ~ m2_relset_1(u2_lattices(sK32),k2_zfmisc_1(u1_struct_0(sK32),u1_struct_0(sK32)),u1_struct_0(sK32))
| ~ v1_funct_1(k1_realset1(u1_lattices(sK32),u1_struct_0(sK32)))
| ~ v1_funct_2(k1_realset1(u1_lattices(sK32),u1_struct_0(sK32)),k2_zfmisc_1(u1_struct_0(sK32),u1_struct_0(sK32)),u1_struct_0(sK32))
| ~ m2_relset_1(k1_realset1(u1_lattices(sK32),u1_struct_0(sK32)),k2_zfmisc_1(u1_struct_0(sK32),u1_struct_0(sK32)),u1_struct_0(sK32))
| v3_struct_0(g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),k1_realset1(u1_lattices(sK32),u1_struct_0(sK32))))
| ~ v10_lattices(g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),k1_realset1(u1_lattices(sK32),u1_struct_0(sK32))))
| v3_struct_0(sK32)
| ~ v10_lattices(sK32)
| ~ l3_lattices(sK32)
| ~ spl226_102 ),
inference(forward_subsumption_resolution,[],[f72504,f36321]) ).
fof(f72696,plain,
( v1_funct_1(u2_lattices(sK32))
| v1_xboole_0(u1_struct_0(sK32))
| v3_struct_0(sK32)
| ~ v10_lattices(sK32)
| ~ l3_lattices(sK32)
| ~ spl226_102 ),
inference(forward_subsumption_resolution,[],[f72466,f36307]) ).
fof(f72697,plain,
( v1_funct_2(u2_lattices(sK32),k2_zfmisc_1(u1_struct_0(sK32),u1_struct_0(sK32)),u1_struct_0(sK32))
| v1_xboole_0(u1_struct_0(sK32))
| v3_struct_0(sK32)
| ~ v10_lattices(sK32)
| ~ l3_lattices(sK32)
| ~ spl226_102 ),
inference(forward_subsumption_resolution,[],[f72465,f36307]) ).
fof(f72698,plain,
( m2_relset_1(u2_lattices(sK32),k2_zfmisc_1(u1_struct_0(sK32),u1_struct_0(sK32)),u1_struct_0(sK32))
| v1_xboole_0(u1_struct_0(sK32))
| v3_struct_0(sK32)
| ~ v10_lattices(sK32)
| ~ l3_lattices(sK32)
| ~ spl226_102 ),
inference(forward_subsumption_resolution,[],[f72464,f36307]) ).
fof(f72723,plain,
( ~ l3_lattices(g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),k1_realset1(u1_lattices(sK32),u1_struct_0(sK32))))
| k8_filter_0(sK32,u1_struct_0(sK32)) = g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),k1_realset1(u1_lattices(sK32),u1_struct_0(sK32)))
| ~ v1_funct_1(u2_lattices(sK32))
| ~ v1_funct_2(u2_lattices(sK32),k2_zfmisc_1(u1_struct_0(sK32),u1_struct_0(sK32)),u1_struct_0(sK32))
| ~ m2_relset_1(u2_lattices(sK32),k2_zfmisc_1(u1_struct_0(sK32),u1_struct_0(sK32)),u1_struct_0(sK32))
| ~ v1_funct_2(k1_realset1(u1_lattices(sK32),u1_struct_0(sK32)),k2_zfmisc_1(u1_struct_0(sK32),u1_struct_0(sK32)),u1_struct_0(sK32))
| ~ m2_relset_1(k1_realset1(u1_lattices(sK32),u1_struct_0(sK32)),k2_zfmisc_1(u1_struct_0(sK32),u1_struct_0(sK32)),u1_struct_0(sK32))
| v3_struct_0(g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),k1_realset1(u1_lattices(sK32),u1_struct_0(sK32))))
| ~ v10_lattices(g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),k1_realset1(u1_lattices(sK32),u1_struct_0(sK32))))
| v3_struct_0(sK32)
| ~ v10_lattices(sK32)
| ~ l3_lattices(sK32)
| spl226_1
| ~ spl226_4
| ~ spl226_5
| ~ spl226_16
| ~ spl226_102 ),
inference(forward_subsumption_resolution,[],[f72666,f43406]) ).
fof(f72753,plain,
( v1_funct_1(u2_lattices(sK32))
| v3_struct_0(sK32)
| ~ v10_lattices(sK32)
| ~ l3_lattices(sK32)
| spl226_77
| ~ spl226_102 ),
inference(forward_subsumption_resolution,[],[f72696,f63155]) ).
fof(f72754,plain,
( v1_funct_2(u2_lattices(sK32),k2_zfmisc_1(u1_struct_0(sK32),u1_struct_0(sK32)),u1_struct_0(sK32))
| v3_struct_0(sK32)
| ~ v10_lattices(sK32)
| ~ l3_lattices(sK32)
| spl226_77
| ~ spl226_102 ),
inference(forward_subsumption_resolution,[],[f72697,f63155]) ).
fof(f72755,plain,
( m2_relset_1(u2_lattices(sK32),k2_zfmisc_1(u1_struct_0(sK32),u1_struct_0(sK32)),u1_struct_0(sK32))
| v3_struct_0(sK32)
| ~ v10_lattices(sK32)
| ~ l3_lattices(sK32)
| spl226_77
| ~ spl226_102 ),
inference(forward_subsumption_resolution,[],[f72698,f63155]) ).
fof(f72768,plain,
( ~ l3_lattices(g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),k1_realset1(u1_lattices(sK32),u1_struct_0(sK32))))
| k8_filter_0(sK32,u1_struct_0(sK32)) = g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),k1_realset1(u1_lattices(sK32),u1_struct_0(sK32)))
| ~ v1_funct_1(u2_lattices(sK32))
| ~ v1_funct_2(u2_lattices(sK32),k2_zfmisc_1(u1_struct_0(sK32),u1_struct_0(sK32)),u1_struct_0(sK32))
| ~ m2_relset_1(u2_lattices(sK32),k2_zfmisc_1(u1_struct_0(sK32),u1_struct_0(sK32)),u1_struct_0(sK32))
| ~ m2_relset_1(k1_realset1(u1_lattices(sK32),u1_struct_0(sK32)),k2_zfmisc_1(u1_struct_0(sK32),u1_struct_0(sK32)),u1_struct_0(sK32))
| v3_struct_0(g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),k1_realset1(u1_lattices(sK32),u1_struct_0(sK32))))
| ~ v10_lattices(g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),k1_realset1(u1_lattices(sK32),u1_struct_0(sK32))))
| v3_struct_0(sK32)
| ~ v10_lattices(sK32)
| ~ l3_lattices(sK32)
| spl226_1
| ~ spl226_4
| ~ spl226_5
| ~ spl226_16
| ~ spl226_102 ),
inference(forward_subsumption_resolution,[],[f72723,f43405]) ).
fof(f72798,plain,
( v1_funct_1(u2_lattices(sK32))
| ~ v10_lattices(sK32)
| ~ l3_lattices(sK32)
| spl226_1
| spl226_77
| ~ spl226_102 ),
inference(forward_subsumption_resolution,[],[f72753,f37537]) ).
fof(f72799,plain,
( v1_funct_2(u2_lattices(sK32),k2_zfmisc_1(u1_struct_0(sK32),u1_struct_0(sK32)),u1_struct_0(sK32))
| ~ v10_lattices(sK32)
| ~ l3_lattices(sK32)
| spl226_1
| spl226_77
| ~ spl226_102 ),
inference(forward_subsumption_resolution,[],[f72754,f37537]) ).
fof(f72800,plain,
( m2_relset_1(u2_lattices(sK32),k2_zfmisc_1(u1_struct_0(sK32),u1_struct_0(sK32)),u1_struct_0(sK32))
| ~ v10_lattices(sK32)
| ~ l3_lattices(sK32)
| spl226_1
| spl226_77
| ~ spl226_102 ),
inference(forward_subsumption_resolution,[],[f72755,f37537]) ).
fof(f72813,plain,
( ~ l3_lattices(g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),k1_realset1(u1_lattices(sK32),u1_struct_0(sK32))))
| k8_filter_0(sK32,u1_struct_0(sK32)) = g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),k1_realset1(u1_lattices(sK32),u1_struct_0(sK32)))
| ~ v1_funct_1(u2_lattices(sK32))
| ~ v1_funct_2(u2_lattices(sK32),k2_zfmisc_1(u1_struct_0(sK32),u1_struct_0(sK32)),u1_struct_0(sK32))
| ~ m2_relset_1(u2_lattices(sK32),k2_zfmisc_1(u1_struct_0(sK32),u1_struct_0(sK32)),u1_struct_0(sK32))
| v3_struct_0(g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),k1_realset1(u1_lattices(sK32),u1_struct_0(sK32))))
| ~ v10_lattices(g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),k1_realset1(u1_lattices(sK32),u1_struct_0(sK32))))
| v3_struct_0(sK32)
| ~ v10_lattices(sK32)
| ~ l3_lattices(sK32)
| spl226_1
| ~ spl226_4
| ~ spl226_5
| ~ spl226_16
| ~ spl226_102 ),
inference(forward_subsumption_resolution,[],[f72768,f43404]) ).
fof(f72843,plain,
( v1_funct_1(u2_lattices(sK32))
| ~ l3_lattices(sK32)
| spl226_1
| ~ spl226_5
| spl226_77
| ~ spl226_102 ),
inference(forward_subsumption_resolution,[],[f72798,f37556]) ).
fof(f72844,plain,
( v1_funct_2(u2_lattices(sK32),k2_zfmisc_1(u1_struct_0(sK32),u1_struct_0(sK32)),u1_struct_0(sK32))
| ~ l3_lattices(sK32)
| spl226_1
| ~ spl226_5
| spl226_77
| ~ spl226_102 ),
inference(forward_subsumption_resolution,[],[f72799,f37556]) ).
fof(f72845,plain,
( m2_relset_1(u2_lattices(sK32),k2_zfmisc_1(u1_struct_0(sK32),u1_struct_0(sK32)),u1_struct_0(sK32))
| ~ l3_lattices(sK32)
| spl226_1
| ~ spl226_5
| spl226_77
| ~ spl226_102 ),
inference(forward_subsumption_resolution,[],[f72800,f37556]) ).
fof(f72846,plain,
( ~ l3_lattices(g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),k1_realset1(u1_lattices(sK32),u1_struct_0(sK32))))
| k8_filter_0(sK32,u1_struct_0(sK32)) = g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),k1_realset1(u1_lattices(sK32),u1_struct_0(sK32)))
| ~ v1_funct_1(u2_lattices(sK32))
| ~ v1_funct_2(u2_lattices(sK32),k2_zfmisc_1(u1_struct_0(sK32),u1_struct_0(sK32)),u1_struct_0(sK32))
| ~ m2_relset_1(u2_lattices(sK32),k2_zfmisc_1(u1_struct_0(sK32),u1_struct_0(sK32)),u1_struct_0(sK32))
| v3_struct_0(g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),k1_realset1(u1_lattices(sK32),u1_struct_0(sK32))))
| ~ v10_lattices(g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),k1_realset1(u1_lattices(sK32),u1_struct_0(sK32))))
| ~ v10_lattices(sK32)
| ~ l3_lattices(sK32)
| spl226_1
| ~ spl226_4
| ~ spl226_5
| ~ spl226_16
| ~ spl226_102 ),
inference(forward_subsumption_resolution,[],[f72813,f37537]) ).
fof(f72876,plain,
( v1_funct_1(u2_lattices(sK32))
| spl226_1
| ~ spl226_4
| ~ spl226_5
| spl226_77
| ~ spl226_102 ),
inference(forward_subsumption_resolution,[],[f72843,f37551]) ).
fof(f72877,plain,
( v1_funct_2(u2_lattices(sK32),k2_zfmisc_1(u1_struct_0(sK32),u1_struct_0(sK32)),u1_struct_0(sK32))
| spl226_1
| ~ spl226_4
| ~ spl226_5
| spl226_77
| ~ spl226_102 ),
inference(forward_subsumption_resolution,[],[f72844,f37551]) ).
fof(f72878,plain,
( m2_relset_1(u2_lattices(sK32),k2_zfmisc_1(u1_struct_0(sK32),u1_struct_0(sK32)),u1_struct_0(sK32))
| spl226_1
| ~ spl226_4
| ~ spl226_5
| spl226_77
| ~ spl226_102 ),
inference(forward_subsumption_resolution,[],[f72845,f37551]) ).
fof(f72879,plain,
( ~ l3_lattices(g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),k1_realset1(u1_lattices(sK32),u1_struct_0(sK32))))
| k8_filter_0(sK32,u1_struct_0(sK32)) = g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),k1_realset1(u1_lattices(sK32),u1_struct_0(sK32)))
| ~ v1_funct_1(u2_lattices(sK32))
| ~ v1_funct_2(u2_lattices(sK32),k2_zfmisc_1(u1_struct_0(sK32),u1_struct_0(sK32)),u1_struct_0(sK32))
| ~ m2_relset_1(u2_lattices(sK32),k2_zfmisc_1(u1_struct_0(sK32),u1_struct_0(sK32)),u1_struct_0(sK32))
| v3_struct_0(g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),k1_realset1(u1_lattices(sK32),u1_struct_0(sK32))))
| ~ v10_lattices(g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),k1_realset1(u1_lattices(sK32),u1_struct_0(sK32))))
| ~ l3_lattices(sK32)
| spl226_1
| ~ spl226_4
| ~ spl226_5
| ~ spl226_16
| ~ spl226_102 ),
inference(forward_subsumption_resolution,[],[f72846,f37556]) ).
fof(f73061,plain,
( ~ l3_lattices(g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),k1_realset1(u1_lattices(sK32),u1_struct_0(sK32))))
| k8_filter_0(sK32,u1_struct_0(sK32)) = g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),k1_realset1(u1_lattices(sK32),u1_struct_0(sK32)))
| ~ v1_funct_2(u2_lattices(sK32),k2_zfmisc_1(u1_struct_0(sK32),u1_struct_0(sK32)),u1_struct_0(sK32))
| ~ m2_relset_1(u2_lattices(sK32),k2_zfmisc_1(u1_struct_0(sK32),u1_struct_0(sK32)),u1_struct_0(sK32))
| v3_struct_0(g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),k1_realset1(u1_lattices(sK32),u1_struct_0(sK32))))
| ~ v10_lattices(g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),k1_realset1(u1_lattices(sK32),u1_struct_0(sK32))))
| ~ l3_lattices(sK32)
| spl226_1
| ~ spl226_4
| ~ spl226_5
| ~ spl226_16
| spl226_77
| ~ spl226_102 ),
inference(forward_subsumption_resolution,[],[f72879,f72876]) ).
fof(f73228,plain,
( ~ l3_lattices(g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),k1_realset1(u1_lattices(sK32),u1_struct_0(sK32))))
| k8_filter_0(sK32,u1_struct_0(sK32)) = g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),k1_realset1(u1_lattices(sK32),u1_struct_0(sK32)))
| ~ m2_relset_1(u2_lattices(sK32),k2_zfmisc_1(u1_struct_0(sK32),u1_struct_0(sK32)),u1_struct_0(sK32))
| v3_struct_0(g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),k1_realset1(u1_lattices(sK32),u1_struct_0(sK32))))
| ~ v10_lattices(g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),k1_realset1(u1_lattices(sK32),u1_struct_0(sK32))))
| ~ l3_lattices(sK32)
| spl226_1
| ~ spl226_4
| ~ spl226_5
| ~ spl226_16
| spl226_77
| ~ spl226_102 ),
inference(forward_subsumption_resolution,[],[f73061,f72877]) ).
fof(f73395,plain,
( ~ l3_lattices(g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),k1_realset1(u1_lattices(sK32),u1_struct_0(sK32))))
| k8_filter_0(sK32,u1_struct_0(sK32)) = g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),k1_realset1(u1_lattices(sK32),u1_struct_0(sK32)))
| v3_struct_0(g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),k1_realset1(u1_lattices(sK32),u1_struct_0(sK32))))
| ~ v10_lattices(g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),k1_realset1(u1_lattices(sK32),u1_struct_0(sK32))))
| ~ l3_lattices(sK32)
| spl226_1
| ~ spl226_4
| ~ spl226_5
| ~ spl226_16
| spl226_77
| ~ spl226_102 ),
inference(forward_subsumption_resolution,[],[f73228,f72878]) ).
fof(f73425,plain,
( ~ l3_lattices(g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),k1_realset1(u1_lattices(sK32),u1_struct_0(sK32))))
| k8_filter_0(sK32,u1_struct_0(sK32)) = g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),k1_realset1(u1_lattices(sK32),u1_struct_0(sK32)))
| v3_struct_0(g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),k1_realset1(u1_lattices(sK32),u1_struct_0(sK32))))
| ~ v10_lattices(g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),k1_realset1(u1_lattices(sK32),u1_struct_0(sK32))))
| spl226_1
| ~ spl226_4
| ~ spl226_5
| ~ spl226_16
| spl226_77
| ~ spl226_102 ),
inference(forward_subsumption_resolution,[],[f73395,f37551]) ).
fof(f73455,plain,
( ~ l3_lattices(g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),u1_lattices(sK32)))
| k8_filter_0(sK32,u1_struct_0(sK32)) = g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),k1_realset1(u1_lattices(sK32),u1_struct_0(sK32)))
| v3_struct_0(g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),k1_realset1(u1_lattices(sK32),u1_struct_0(sK32))))
| ~ v10_lattices(g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),k1_realset1(u1_lattices(sK32),u1_struct_0(sK32))))
| spl226_1
| ~ spl226_4
| ~ spl226_5
| ~ spl226_16
| spl226_77
| ~ spl226_102
| ~ spl226_106 ),
inference(forward_demodulation,[],[f73425,f72407]) ).
fof(f73485,plain,
( ~ l3_lattices(k1_lattice2(k1_lattice2(sK32)))
| k8_filter_0(sK32,u1_struct_0(sK32)) = g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),k1_realset1(u1_lattices(sK32),u1_struct_0(sK32)))
| v3_struct_0(g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),k1_realset1(u1_lattices(sK32),u1_struct_0(sK32))))
| ~ v10_lattices(g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),k1_realset1(u1_lattices(sK32),u1_struct_0(sK32))))
| spl226_1
| ~ spl226_4
| ~ spl226_5
| ~ spl226_16
| ~ spl226_17
| spl226_77
| ~ spl226_102
| ~ spl226_106 ),
inference(forward_demodulation,[],[f73455,f43600]) ).
fof(f73515,plain,
( k8_filter_0(sK32,u1_struct_0(sK32)) = g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),k1_realset1(u1_lattices(sK32),u1_struct_0(sK32)))
| v3_struct_0(g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),k1_realset1(u1_lattices(sK32),u1_struct_0(sK32))))
| ~ v10_lattices(g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),k1_realset1(u1_lattices(sK32),u1_struct_0(sK32))))
| spl226_1
| ~ spl226_4
| ~ spl226_5
| ~ spl226_16
| ~ spl226_17
| ~ spl226_35
| spl226_77
| ~ spl226_102
| ~ spl226_106 ),
inference(forward_subsumption_resolution,[],[f73485,f55345]) ).
fof(f73531,plain,
( g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),u1_lattices(sK32)) = k8_filter_0(sK32,u1_struct_0(sK32))
| v3_struct_0(g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),k1_realset1(u1_lattices(sK32),u1_struct_0(sK32))))
| ~ v10_lattices(g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),k1_realset1(u1_lattices(sK32),u1_struct_0(sK32))))
| spl226_1
| ~ spl226_4
| ~ spl226_5
| ~ spl226_16
| ~ spl226_17
| ~ spl226_35
| spl226_77
| ~ spl226_102
| ~ spl226_106 ),
inference(forward_demodulation,[],[f73515,f72407]) ).
fof(f73542,plain,
( k1_lattice2(k1_lattice2(sK32)) = k8_filter_0(sK32,u1_struct_0(sK32))
| v3_struct_0(g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),k1_realset1(u1_lattices(sK32),u1_struct_0(sK32))))
| ~ v10_lattices(g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),k1_realset1(u1_lattices(sK32),u1_struct_0(sK32))))
| spl226_1
| ~ spl226_4
| ~ spl226_5
| ~ spl226_16
| ~ spl226_17
| ~ spl226_35
| spl226_77
| ~ spl226_102
| ~ spl226_106 ),
inference(forward_demodulation,[],[f73531,f43600]) ).
fof(f73553,plain,
( v3_struct_0(g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),u1_lattices(sK32)))
| k1_lattice2(k1_lattice2(sK32)) = k8_filter_0(sK32,u1_struct_0(sK32))
| ~ v10_lattices(g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),k1_realset1(u1_lattices(sK32),u1_struct_0(sK32))))
| spl226_1
| ~ spl226_4
| ~ spl226_5
| ~ spl226_16
| ~ spl226_17
| ~ spl226_35
| spl226_77
| ~ spl226_102
| ~ spl226_106 ),
inference(forward_demodulation,[],[f73542,f72407]) ).
fof(f73564,plain,
( v3_struct_0(k1_lattice2(k1_lattice2(sK32)))
| k1_lattice2(k1_lattice2(sK32)) = k8_filter_0(sK32,u1_struct_0(sK32))
| ~ v10_lattices(g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),k1_realset1(u1_lattices(sK32),u1_struct_0(sK32))))
| spl226_1
| ~ spl226_4
| ~ spl226_5
| ~ spl226_16
| ~ spl226_17
| ~ spl226_35
| spl226_77
| ~ spl226_102
| ~ spl226_106 ),
inference(forward_demodulation,[],[f73553,f43600]) ).
fof(f73571,plain,
( k1_lattice2(k1_lattice2(sK32)) = k8_filter_0(sK32,u1_struct_0(sK32))
| ~ v10_lattices(g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),k1_realset1(u1_lattices(sK32),u1_struct_0(sK32))))
| spl226_1
| ~ spl226_4
| ~ spl226_5
| ~ spl226_16
| ~ spl226_17
| spl226_28
| ~ spl226_35
| spl226_77
| ~ spl226_102
| ~ spl226_106 ),
inference(forward_subsumption_resolution,[],[f73564,f47460]) ).
fof(f73578,plain,
( ~ v10_lattices(g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),u1_lattices(sK32)))
| k1_lattice2(k1_lattice2(sK32)) = k8_filter_0(sK32,u1_struct_0(sK32))
| spl226_1
| ~ spl226_4
| ~ spl226_5
| ~ spl226_16
| ~ spl226_17
| spl226_28
| ~ spl226_35
| spl226_77
| ~ spl226_102
| ~ spl226_106 ),
inference(forward_demodulation,[],[f73571,f72407]) ).
fof(f73585,plain,
( ~ v10_lattices(k1_lattice2(k1_lattice2(sK32)))
| k1_lattice2(k1_lattice2(sK32)) = k8_filter_0(sK32,u1_struct_0(sK32))
| spl226_1
| ~ spl226_4
| ~ spl226_5
| ~ spl226_16
| ~ spl226_17
| spl226_28
| ~ spl226_35
| spl226_77
| ~ spl226_102
| ~ spl226_106 ),
inference(forward_demodulation,[],[f73578,f43600]) ).
fof(f73592,plain,
( k1_lattice2(k1_lattice2(sK32)) = k8_filter_0(sK32,u1_struct_0(sK32))
| spl226_1
| ~ spl226_4
| ~ spl226_5
| ~ spl226_16
| ~ spl226_17
| spl226_28
| ~ spl226_35
| spl226_77
| ~ spl226_102
| ~ spl226_106 ),
inference(forward_subsumption_resolution,[],[f73585,f48024]) ).
fof(f90080,definition,
( spl226_160
<=> m1_filter_2(u1_struct_0(sK32),sK32) ),
introduced(definition,[new_symbols(definition,[spl226_160])],[avatar_definition]) ).
fof(f90082,plain,
( m1_filter_2(u1_struct_0(sK32),sK32)
| ~ spl226_160 ),
inference(avatar_component_clause,[],[f90080]) ).
fof(f90083,plain,
( spl226_160
| spl226_1
| ~ spl226_4
| ~ spl226_5
| ~ spl226_15 ),
inference(avatar_split_clause,[],[f42963,f42954,f37554,f37549,f37535,f90080]) ).
fof(f90090,plain,
( k8_filter_0(sK32,u1_struct_0(sK32)) = k23_filter_2(sK32,u1_struct_0(sK32))
| v3_struct_0(sK32)
| ~ v10_lattices(sK32)
| ~ l3_lattices(sK32)
| ~ spl226_160 ),
inference(resolution,[],[f90082,f36286]) ).
fof(f90126,plain,
( k8_filter_0(sK32,u1_struct_0(sK32)) = k23_filter_2(sK32,u1_struct_0(sK32))
| ~ v10_lattices(sK32)
| ~ l3_lattices(sK32)
| spl226_1
| ~ spl226_160 ),
inference(forward_subsumption_resolution,[],[f90090,f37537]) ).
fof(f90135,plain,
( k8_filter_0(sK32,u1_struct_0(sK32)) = k23_filter_2(sK32,u1_struct_0(sK32))
| ~ l3_lattices(sK32)
| spl226_1
| ~ spl226_5
| ~ spl226_160 ),
inference(forward_subsumption_resolution,[],[f90126,f37556]) ).
fof(f90144,plain,
( k8_filter_0(sK32,u1_struct_0(sK32)) = k23_filter_2(sK32,u1_struct_0(sK32))
| spl226_1
| ~ spl226_4
| ~ spl226_5
| ~ spl226_160 ),
inference(forward_subsumption_resolution,[],[f90135,f37551]) ).
fof(f90148,plain,
( k1_lattice2(k1_lattice2(sK32)) = k23_filter_2(sK32,u1_struct_0(sK32))
| spl226_1
| ~ spl226_4
| ~ spl226_5
| ~ spl226_16
| ~ spl226_17
| spl226_28
| ~ spl226_35
| spl226_77
| ~ spl226_102
| ~ spl226_106
| ~ spl226_160 ),
inference(forward_demodulation,[],[f90144,f73592]) ).
fof(f90152,plain,
( $false
| spl226_1
| ~ spl226_4
| ~ spl226_5
| spl226_8
| ~ spl226_16
| ~ spl226_17
| spl226_28
| ~ spl226_35
| spl226_77
| ~ spl226_102
| ~ spl226_106
| ~ spl226_160 ),
inference(forward_subsumption_resolution,[],[f90148,f42171]) ).
fof(f90153,plain,
( spl226_1
| ~ spl226_4
| ~ spl226_5
| spl226_8
| ~ spl226_16
| ~ spl226_17
| spl226_28
| ~ spl226_35
| spl226_77
| ~ spl226_102
| ~ spl226_106
| ~ spl226_160 ),
inference(avatar_contradiction_clause,[],[f90152]) ).
fof(f90157,plain,
( g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),u1_lattices(sK32)) != k23_filter_2(sK32,u1_struct_0(sK32))
| spl226_3
| ~ spl226_6 ),
inference(forward_demodulation,[],[f37546,f42139]) ).
fof(f90171,plain,
( g3_lattices(u1_struct_0(sK32),u2_lattices(sK32),u1_lattices(sK32)) != k1_lattice2(k1_lattice2(sK32))
| spl226_1
| spl226_3
| ~ spl226_4
| ~ spl226_5
| ~ spl226_6
| ~ spl226_16
| ~ spl226_17
| spl226_28
| ~ spl226_35
| spl226_77
| ~ spl226_102
| ~ spl226_106
| ~ spl226_160 ),
inference(forward_demodulation,[],[f90157,f90148]) ).
fof(f90174,plain,
( $false
| spl226_1
| spl226_3
| ~ spl226_4
| ~ spl226_5
| ~ spl226_6
| ~ spl226_16
| ~ spl226_17
| spl226_28
| ~ spl226_35
| spl226_77
| ~ spl226_102
| ~ spl226_106
| ~ spl226_160 ),
inference(forward_subsumption_resolution,[],[f90171,f43600]) ).
fof(f90175,plain,
( spl226_1
| spl226_3
| ~ spl226_4
| ~ spl226_5
| ~ spl226_6
| ~ spl226_16
| ~ spl226_17
| spl226_28
| ~ spl226_35
| spl226_77
| ~ spl226_102
| ~ spl226_106
| ~ spl226_160 ),
inference(avatar_contradiction_clause,[],[f90174]) ).
cnf(s1,plain,
~ spl226_1,
inference(sat_conversion,[],[f37538]) ).
cnf(s2,plain,
( ~ spl226_2
| ~ spl226_3 ),
inference(sat_conversion,[],[f37547]) ).
cnf(s3,plain,
spl226_4,
inference(sat_conversion,[],[f37552]) ).
cnf(s4,plain,
spl226_5,
inference(sat_conversion,[],[f37557]) ).
cnf(s5,plain,
( spl226_1
| ~ spl226_4
| ~ spl226_5
| spl226_6 ),
inference(sat_conversion,[],[f42140]) ).
cnf(s7,plain,
( spl226_1
| spl226_2
| ~ spl226_4
| ~ spl226_5
| ~ spl226_8 ),
inference(sat_conversion,[],[f42170]) ).
cnf(s14,plain,
( spl226_1
| ~ spl226_4
| ~ spl226_5
| spl226_15 ),
inference(sat_conversion,[],[f42957]) ).
cnf(s15,plain,
( spl226_1
| ~ spl226_4
| ~ spl226_5
| spl226_16 ),
inference(sat_conversion,[],[f42968]) ).
cnf(s16,plain,
( spl226_1
| ~ spl226_4
| ~ spl226_5
| spl226_17 ),
inference(sat_conversion,[],[f43601]) ).
cnf(s18,plain,
( spl226_1
| ~ spl226_4
| ~ spl226_5
| spl226_19 ),
inference(sat_conversion,[],[f44112]) ).
cnf(s26,plain,
( spl226_1
| ~ spl226_4
| ~ spl226_28 ),
inference(sat_conversion,[],[f46220]) ).
cnf(s33,plain,
( ~ spl226_4
| spl226_35 ),
inference(sat_conversion,[],[f53318]) ).
cnf(s74,plain,
( spl226_1
| ~ spl226_4
| ~ spl226_5
| ~ spl226_16
| ~ spl226_77 ),
inference(sat_conversion,[],[f63156]) ).
cnf(s141,plain,
( spl226_1
| ~ spl226_4
| ~ spl226_5
| ~ spl226_19
| spl226_102 ),
inference(sat_conversion,[],[f71797]) ).
cnf(s145,plain,
( spl226_1
| ~ spl226_4
| ~ spl226_5
| ~ spl226_19
| spl226_106 ),
inference(sat_conversion,[],[f72408]) ).
cnf(s311,plain,
( spl226_1
| ~ spl226_4
| ~ spl226_5
| ~ spl226_15
| spl226_160 ),
inference(sat_conversion,[],[f90083]) ).
cnf(s312,plain,
( spl226_1
| ~ spl226_4
| ~ spl226_5
| spl226_8
| ~ spl226_16
| ~ spl226_17
| spl226_28
| ~ spl226_35
| spl226_77
| ~ spl226_102
| ~ spl226_106
| ~ spl226_160 ),
inference(sat_conversion,[],[f90153]) ).
cnf(s313,plain,
( spl226_1
| spl226_3
| ~ spl226_4
| ~ spl226_5
| ~ spl226_6
| ~ spl226_16
| ~ spl226_17
| spl226_28
| ~ spl226_35
| spl226_77
| ~ spl226_102
| ~ spl226_106
| ~ spl226_160 ),
inference(sat_conversion,[],[f90175]) ).
cnf(s314,plain,
spl226_35,
inference(rat,[],[s33,s3]) ).
cnf(s362,plain,
~ spl226_28,
inference(rat,[],[s26,s3,s1]) ).
cnf(s367,plain,
spl226_19,
inference(rat,[],[s18,s3,s4,s1]) ).
cnf(s369,plain,
spl226_17,
inference(rat,[],[s16,s3,s4,s1]) ).
cnf(s370,plain,
spl226_16,
inference(rat,[],[s15,s3,s4,s1]) ).
cnf(s371,plain,
spl226_15,
inference(rat,[],[s14,s3,s4,s1]) ).
cnf(s378,plain,
spl226_6,
inference(rat,[],[s5,s3,s4,s1]) ).
cnf(s406,plain,
spl226_106,
inference(rat,[],[s145,s1,s3,s4,s367]) ).
cnf(s407,plain,
spl226_102,
inference(rat,[],[s141,s1,s3,s4,s367]) ).
cnf(s410,plain,
~ spl226_77,
inference(rat,[],[s74,s1,s3,s4,s370]) ).
cnf(s416,plain,
spl226_160,
inference(rat,[],[s311,s1,s3,s4,s371]) ).
cnf(s417,plain,
spl226_3,
inference(rat,[],[s313,s416,s406,s407,s410,s314,s362,s369,s370,s1,s4,s3,s378]) ).
cnf(s435,plain,
spl226_8,
inference(rat,[],[s312,s370,s406,s407,s410,s314,s362,s369,s1,s3,s4,s416]) ).
cnf(s436,plain,
~ spl226_2,
inference(rat,[],[s2,s417]) ).
cnf(s440,plain,
$false,
inference(rat,[],[s7,s1,s4,s3,s435,s436]) ).
fof(f90176,plain,
$false,
inference(avatar_sat_refutation,[],[s440]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT332+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.37 % Computer : n007.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sun Sep 27 14:41:16 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.40 Running first-order theorem proving
% 0.11/0.40 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 13.96/4.77 % (1493488)Detected formulas, will run a generic FOF schedule.
% 13.96/4.77 % (1493497)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3616236850:i=119:av=off:ss=axioms_2977 on theBenchmark for (2977ds/119Mi)
% 13.96/4.77 % (1493498)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4107483551:s2a=on:i=139:gtg=position_2977 on theBenchmark for (2977ds/139Mi)
% 13.96/4.77 % (1493493)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=3172066073:i=141193_2977 on theBenchmark for (2977ds/141193Mi)
% 13.96/4.77 % (1493494)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=1729900158:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2977 on theBenchmark for (2977ds/134677Mi)
% 13.96/4.77 % (1493496)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=427485234:i=109:sd=1:ins=1:gsp=on:ss=axioms_2977 on theBenchmark for (2977ds/109Mi)
% 13.96/4.77 % (1493495)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=225810642:i=141695:sd=1:nm=32:gsp=on:ss=included_2977 on theBenchmark for (2977ds/141695Mi)
% 13.96/4.77 % (1493499)dis-21_1_sil=8000:lcm=predicate:random_seed=1209739362:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2977 on theBenchmark for (2977ds/129Mi)
% 13.96/4.77 % (1493497)Instruction limit reached!
% 13.96/4.77 % (1493497)------------------------------
% 13.96/4.77 % (1493497)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.96/4.77 % (1493497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.96/4.77 % (1493497)CaDiCaL version: 2.1.3
% 13.96/4.77 % (1493497)Termination reason: Instruction limit
% 13.96/4.77 % (1493497)Termination phase: SInE selection
% 13.96/4.77 % (1493497)Time elapsed: 0.053 s
% 13.96/4.77 % (1493497)Peak memory usage: 136 MB
% 13.96/4.77 % (1493497)Instructions burned: 122 (million)
% 13.96/4.77 % (1493498)Instruction limit reached!
% 13.96/4.77 % (1493498)------------------------------
% 13.96/4.77 % (1493498)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.96/4.77 % (1493498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.96/4.77 % (1493498)CaDiCaL version: 2.1.3
% 13.96/4.77 % (1493498)Termination reason: Instruction limit
% 13.96/4.77 % (1493498)Termination phase: Property scanning
% 13.96/4.77 % (1493498)Time elapsed: 0.062 s
% 13.96/4.77 % (1493498)Peak memory usage: 136 MB
% 13.96/4.77 % (1493498)Instructions burned: 140 (million)
% 13.96/4.77 % (1493496)Instruction limit reached!
% 13.96/4.77 % (1493496)------------------------------
% 13.96/4.77 % (1493496)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.96/4.77 % (1493496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.96/4.77 % (1493496)CaDiCaL version: 2.1.3
% 13.96/4.77 % (1493496)Termination reason: Instruction limit
% 13.96/4.77 % (1493496)Termination phase: SInE selection
% 13.96/4.77 % (1493496)Time elapsed: 0.080 s
% 13.96/4.77 % (1493496)Peak memory usage: 136 MB
% 13.96/4.77 % (1493496)Instructions burned: 110 (million)
% 13.96/4.77 % (1493499)Instruction limit reached!
% 13.96/4.77 % (1493499)------------------------------
% 13.96/4.77 % (1493499)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.96/4.77 % (1493499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.96/4.77 % (1493499)CaDiCaL version: 2.1.3
% 13.96/4.77 % (1493499)Termination reason: Instruction limit
% 13.96/4.77 % (1493499)Termination phase: SInE selection
% 13.96/4.77 % (1493499)Time elapsed: 0.086 s
% 13.96/4.77 % (1493499)Peak memory usage: 136 MB
% 13.96/4.77 % (1493499)Instructions burned: 129 (million)
% 13.96/4.77 % (1493507)lrs+10_1_sil=8000:sp=occurrence:random_seed=3250195123:i=285:sd=3:ss=axioms:sgt=8_2976 on theBenchmark for (2976ds/285Mi)
% 13.96/4.77 % (1493508)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2110413778:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2975 on theBenchmark for (2975ds/157Mi)
% 13.96/4.77 % (1493507)Instruction limit reached!
% 13.96/4.77 % (1493507)------------------------------
% 13.96/4.77 % (1493507)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.96/4.77 % (1493507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.96/4.77 % (1493507)CaDiCaL version: 2.1.3
% 13.96/4.77 % (1493507)Termination reason: Instruction limit
% 23.85/6.08 % (1493507)Termination phase: Saturation
% 23.85/6.08 % (1493507)Time elapsed: 0.130 s
% 23.85/6.08 % (1493507)Peak memory usage: 141 MB
% 23.85/6.08 % (1493507)Instructions burned: 286 (million)
% 23.85/6.08 % (1493509)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1069466316:i=325:sd=1:ss=axioms:sgt=32_2975 on theBenchmark for (2975ds/325Mi)
% 23.85/6.08 % (1493511)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=3844072359:s2a=on:i=248:s2at=1.23:gtg=position_2975 on theBenchmark for (2975ds/248Mi)
% 23.85/6.08 % (1493508)Instruction limit reached!
% 23.85/6.08 % (1493508)------------------------------
% 23.85/6.08 % (1493508)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.85/6.08 % (1493508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.85/6.08 % (1493508)CaDiCaL version: 2.1.3
% 23.85/6.08 % (1493508)Termination reason: Instruction limit
% 23.85/6.08 % (1493508)Termination phase: Property scanning
% 23.85/6.08 % (1493508)Time elapsed: 0.072 s
% 23.85/6.08 % (1493508)Peak memory usage: 136 MB
% 23.85/6.08 % (1493508)Instructions burned: 159 (million)
% 23.85/6.08 % (1493515)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1301624677:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2974 on theBenchmark for (2974ds/294Mi)
% 23.85/6.08 % (1493511)Instruction limit reached!
% 23.85/6.08 % (1493511)------------------------------
% 23.85/6.08 % (1493511)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.85/6.08 % (1493511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.85/6.08 % (1493511)CaDiCaL version: 2.1.3
% 23.85/6.08 % (1493511)Termination reason: Instruction limit
% 23.85/6.08 % (1493511)Termination phase: Property scanning
% 23.85/6.08 % (1493511)Time elapsed: 0.109 s
% 23.85/6.08 % (1493511)Peak memory usage: 136 MB
% 23.85/6.08 % (1493511)Instructions burned: 250 (million)
% 23.85/6.08 % (1493516)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1561361844:i=2350_2973 on theBenchmark for (2973ds/2350Mi)
% 23.85/6.08 % (1493509)Refutation not found, incomplete strategy
% 23.85/6.08 % (1493509)------------------------------
% 23.85/6.08 % (1493509)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.85/6.08 % (1493509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.85/6.08 % (1493509)CaDiCaL version: 2.1.3
% 23.85/6.08 % (1493509)Termination reason: Refutation not found, incomplete strategy
% 23.85/6.08 % (1493509)Time elapsed: 0.190 s
% 23.85/6.08 % (1493509)Peak memory usage: 142 MB
% 23.85/6.08 % (1493509)Instructions burned: 240 (million)
% 23.85/6.08 % (1493515)Instruction limit reached!
% 23.85/6.08 % (1493515)------------------------------
% 23.85/6.08 % (1493515)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.85/6.08 % (1493515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.85/6.08 % (1493515)CaDiCaL version: 2.1.3
% 23.85/6.08 % (1493515)Termination reason: Instruction limit
% 23.85/6.08 % (1493515)Termination phase: SInE selection
% 23.85/6.08 % (1493515)Time elapsed: 0.104 s
% 23.85/6.08 % (1493515)Peak memory usage: 137 MB
% 23.85/6.08 % (1493515)Instructions burned: 296 (million)
% 23.85/6.08 % (1493518)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1960545073:cts=off:i=113:fsr=off:ss=included:sgt=4_2973 on theBenchmark for (2973ds/113Mi)
% 23.85/6.08 % (1493520)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1663097236:i=127:av=off:fsr=off:sup=off_2972 on theBenchmark for (2972ds/127Mi)
% 23.85/6.08 % (1493518)Instruction limit reached!
% 23.85/6.08 % (1493518)------------------------------
% 23.85/6.08 % (1493518)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.85/6.08 % (1493518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.85/6.08 % (1493518)CaDiCaL version: 2.1.3
% 23.85/6.08 % (1493518)Termination reason: Instruction limit
% 23.85/6.08 % (1493518)Termination phase: SInE selection
% 23.85/6.08 % (1493518)Time elapsed: 0.087 s
% 23.85/6.08 % (1493518)Peak memory usage: 136 MB
% 23.85/6.08 % (1493518)Instructions burned: 114 (million)
% 23.85/6.08 % (1493520)Instruction limit reached!
% 23.85/6.08 % (1493520)------------------------------
% 23.85/6.08 % (1493520)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.85/6.08 % (1493520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.85/6.08 % (1493520)CaDiCaL version: 2.1.3
% 23.85/6.08 % (1493520)Termination reason: Instruction limit
% 40.17/8.41 % (1493520)Termination phase: Preprocessing 1
% 40.17/8.41 % (1493520)Time elapsed: 0.056 s
% 40.17/8.41 % (1493520)Peak memory usage: 137 MB
% 40.17/8.41 % (1493520)Instructions burned: 128 (million)
% 40.17/8.41 % (1493509)------------------------------
% 40.17/8.41 % (1493509)------------------------------
% 40.17/8.41 % (1493524)lrs+10_1_sil=8000:sp=occurrence:random_seed=1798305615:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2970 on theBenchmark for (2970ds/907Mi)
% 40.17/8.41 % (1493523)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3177281887:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2970 on theBenchmark for (2970ds/114Mi)
% 40.17/8.41 % (1493523)Instruction limit reached!
% 40.17/8.41 % (1493523)------------------------------
% 40.17/8.41 % (1493523)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.17/8.41 % (1493523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.17/8.41 % (1493523)CaDiCaL version: 2.1.3
% 40.17/8.41 % (1493523)Termination reason: Instruction limit
% 40.17/8.41 % (1493523)Termination phase: Property scanning
% 40.17/8.41 % (1493523)Time elapsed: 0.054 s
% 40.17/8.41 % (1493523)Peak memory usage: 136 MB
% 40.17/8.41 % (1493523)Instructions burned: 114 (million)
% 40.17/8.41 % (1493527)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3851316144:i=437:sd=1:aac=none:ss=included_2969 on theBenchmark for (2969ds/437Mi)
% 40.17/8.41 % (1493528)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3879498730:i=5202:ss=axioms:sgt=16_2968 on theBenchmark for (2968ds/5202Mi)
% 40.17/8.41 % (1493524)Instruction limit reached!
% 40.17/8.41 % (1493524)------------------------------
% 40.17/8.41 % (1493524)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.17/8.41 % (1493524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.17/8.41 % (1493524)CaDiCaL version: 2.1.3
% 40.17/8.41 % (1493524)Termination reason: Instruction limit
% 40.17/8.41 % (1493524)Termination phase: Property scanning
% 40.17/8.41 % (1493524)Time elapsed: 0.370 s
% 40.17/8.41 % (1493524)Peak memory usage: 161 MB
% 40.17/8.41 % (1493524)Instructions burned: 910 (million)
% 40.17/8.41 % (1493527)Refutation not found, incomplete strategy
% 40.17/8.41 % (1493527)------------------------------
% 40.17/8.41 % (1493527)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.17/8.41 % (1493527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.17/8.41 % (1493527)CaDiCaL version: 2.1.3
% 40.17/8.41 % (1493527)Termination reason: Refutation not found, incomplete strategy
% 40.17/8.41 % (1493527)Time elapsed: 0.260 s
% 40.17/8.41 % (1493527)Peak memory usage: 144 MB
% 40.17/8.41 % (1493527)Instructions burned: 360 (million)
% 40.17/8.41 % (1493531)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2220049705:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2965 on theBenchmark for (2965ds/134Mi)
% 40.17/8.41 % (1493531)Instruction limit reached!
% 40.17/8.41 % (1493531)------------------------------
% 40.17/8.41 % (1493531)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.17/8.41 % (1493531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.17/8.41 % (1493531)CaDiCaL version: 2.1.3
% 40.17/8.41 % (1493531)Termination reason: Instruction limit
% 40.17/8.41 % (1493531)Termination phase: SInE selection
% 40.17/8.41 % (1493531)Time elapsed: 0.058 s
% 40.17/8.41 % (1493531)Peak memory usage: 136 MB
% 40.17/8.41 % (1493531)Instructions burned: 136 (million)
% 40.17/8.41 % (1493533)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3932838705:st=8:i=592:sd=3:ep=RST:ss=axioms_2964 on theBenchmark for (2964ds/592Mi)
% 40.17/8.41 % (1493527)------------------------------
% 40.17/8.41 % (1493527)------------------------------
% 40.17/8.41 % (1493535)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=960586347:st=3:i=13193:sd=3:ss=axioms_2962 on theBenchmark for (2962ds/13193Mi)
% 40.17/8.41 % (1493533)Instruction limit reached!
% 40.17/8.41 % (1493533)------------------------------
% 40.17/8.41 % (1493533)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.17/8.41 % (1493533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.17/8.41 % (1493533)CaDiCaL version: 2.1.3
% 40.17/8.41 % (1493533)Termination reason: Instruction limit
% 40.17/8.41 % (1493533)Termination phase: Naming
% 40.17/8.41 % (1493533)Time elapsed: 0.269 s
% 40.17/8.41 % (1493533)Peak memory usage: 153 MB
% 40.17/8.41 % (1493533)Instructions burned: 593 (million)
% 24.17/9.47 % (1493537)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=2230925425:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2960 on theBenchmark for (2960ds/125Mi)
% 24.17/9.47 % (1493537)Instruction limit reached!
% 24.17/9.47 % (1493537)------------------------------
% 24.17/9.47 % (1493537)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.17/9.47 % (1493537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.17/9.47 % (1493537)CaDiCaL version: 2.1.3
% 24.17/9.47 % (1493537)Termination reason: Instruction limit
% 24.17/9.47 % (1493537)Termination phase: Property scanning
% 24.17/9.47 % (1493537)Time elapsed: 0.031 s
% 24.17/9.47 % (1493537)Peak memory usage: 136 MB
% 24.17/9.47 % (1493537)Instructions burned: 126 (million)
% 24.17/9.47 % (1493539)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=442203182:i=134:gtgl=5:slsql=off:gtg=exists_sym_2959 on theBenchmark for (2959ds/134Mi)
% 24.17/9.47 % (1493539)Instruction limit reached!
% 24.17/9.47 % (1493539)------------------------------
% 24.17/9.47 % (1493539)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.17/9.47 % (1493539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.17/9.47 % (1493539)CaDiCaL version: 2.1.3
% 24.17/9.47 % (1493539)Termination reason: Instruction limit
% 24.17/9.47 % (1493539)Termination phase: Property scanning
% 24.17/9.47 % (1493539)Time elapsed: 0.033 s
% 24.17/9.47 % (1493539)Peak memory usage: 136 MB
% 24.17/9.47 % (1493539)Instructions burned: 136 (million)
% 24.17/9.47 % (1493541)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1644634547:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2958 on theBenchmark for (2958ds/141Mi)
% 24.17/9.47 % (1493516)Instruction limit reached!
% 24.17/9.47 % (1493516)------------------------------
% 24.17/9.47 % (1493516)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.17/9.47 % (1493516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.17/9.47 % (1493516)CaDiCaL version: 2.1.3
% 24.17/9.47 % (1493516)Termination reason: Instruction limit
% 24.17/9.47 % (1493516)Termination phase: Property scanning
% 24.17/9.47 % (1493516)Time elapsed: 1.564 s
% 24.17/9.47 % (1493516)Peak memory usage: 233 MB
% 24.17/9.47 % (1493516)Instructions burned: 2351 (million)
% 24.17/9.47 % (1493541)Instruction limit reached!
% 24.17/9.47 % (1493541)------------------------------
% 24.17/9.47 % (1493541)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.17/9.47 % (1493541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.17/9.47 % (1493541)CaDiCaL version: 2.1.3
% 24.17/9.47 % (1493541)Termination reason: Instruction limit
% 24.17/9.47 % (1493541)Termination phase: SInE selection
% 24.17/9.47 % (1493541)Time elapsed: 0.060 s
% 24.17/9.47 % (1493541)Peak memory usage: 136 MB
% 24.17/9.47 % (1493541)Instructions burned: 142 (million)
% 24.17/9.47 % (1493544)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=3167630165:i=6060:aac=none:ins=25_2956 on theBenchmark for (2956ds/6060Mi)
% 24.17/9.47 % (1493543)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=705303385:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2956 on theBenchmark for (2956ds/431Mi)
% 24.17/9.47 % (1493543)Refutation not found, incomplete strategy
% 24.17/9.47 % (1493543)------------------------------
% 24.17/9.47 % (1493543)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.17/9.47 % (1493543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.17/9.47 % (1493543)CaDiCaL version: 2.1.3
% 24.17/9.47 % (1493543)Termination reason: Refutation not found, incomplete strategy
% 24.17/9.47 % (1493543)Time elapsed: 0.206 s
% 24.17/9.47 % (1493543)Peak memory usage: 142 MB
% 24.17/9.47 % (1493543)Instructions burned: 252 (million)
% 24.17/9.47 % (1493543)------------------------------
% 24.17/9.47 % (1493543)------------------------------
% 24.17/9.47 % (1493547)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=2624293073:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2950 on theBenchmark for (2950ds/150Mi)
% 24.17/9.47 % (1493547)Instruction limit reached!
% 24.17/9.47 % (1493547)------------------------------
% 24.17/9.47 % (1493547)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.17/9.47 % (1493547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.17/9.47 % (1493547)CaDiCaL version: 2.1.3
% 24.17/9.47 % (1493547)Termination reason: Instruction limit
% 24.17/9.47 % (1493547)Termination phase: SInE selection
% 24.17/9.47 % (1493547)Time elapsed: 0.121 s
% 24.17/9.47 % (1493547)Peak memory usage: 136 MB
% 24.17/9.47 % (1493547)Instructions burned: 150 (million)
% 24.17/9.47 % (1493549)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1658049530:i=14155:bd=all_2947 on theBenchmark for (2947ds/14155Mi)
% 24.17/9.47 % (1493544)Instruction limit reached!
% 24.17/9.47 % (1493544)------------------------------
% 24.17/9.47 % (1493544)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.17/9.47 % (1493544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.17/9.47 % (1493544)CaDiCaL version: 2.1.3
% 24.17/9.47 % (1493544)Termination reason: Instruction limit
% 24.17/9.47 % (1493544)Termination phase: Function definition elimination
% 24.17/9.47 % (1493544)Time elapsed: 2.138 s
% 24.17/9.47 % (1493544)Peak memory usage: 245 MB
% 24.17/9.47 % (1493544)Instructions burned: 6065 (million)
% 24.17/9.47 % (1493551)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2754266169:i=667:av=off:fsr=off_2934 on theBenchmark for (2934ds/667Mi)
% 24.17/9.47 % (1493551)Instruction limit reached!
% 24.17/9.47 % (1493551)------------------------------
% 24.17/9.47 % (1493551)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.17/9.47 % (1493551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.17/9.47 % (1493551)CaDiCaL version: 2.1.3
% 24.17/9.47 % (1493551)Termination reason: Instruction limit
% 24.17/9.47 % (1493551)Termination phase: NewCNF
% 24.17/9.47 % (1493551)Time elapsed: 0.321 s
% 24.17/9.47 % (1493551)Peak memory usage: 186 MB
% 24.17/9.47 % (1493551)Instructions burned: 668 (million)
% 24.17/9.47 % (1493553)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=4040276873:s2a=on:i=185:s2at=1.8:fdi=4_2929 on theBenchmark for (2929ds/185Mi)
% 24.17/9.47 % (1493528)Instruction limit reached!
% 24.17/9.47 % (1493528)------------------------------
% 24.17/9.47 % (1493528)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.17/9.47 % (1493528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.17/9.47 % (1493528)CaDiCaL version: 2.1.3
% 24.17/9.47 % (1493528)Termination reason: Instruction limit
% 24.17/9.47 % (1493528)Termination phase: Saturation
% 24.17/9.47 % (1493528)Time elapsed: 3.869 s
% 24.17/9.47 % (1493528)Peak memory usage: 521 MB
% 24.17/9.47 % (1493528)Instructions burned: 5206 (million)
% 24.17/9.47 % (1493553)Instruction limit reached!
% 24.17/9.47 % (1493553)------------------------------
% 24.17/9.47 % (1493553)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.17/9.47 % (1493553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.17/9.47 % (1493553)CaDiCaL version: 2.1.3
% 24.17/9.47 % (1493553)Termination reason: Instruction limit
% 24.17/9.47 % (1493553)Termination phase: SInE selection
% 24.17/9.47 % (1493553)Time elapsed: 0.073 s
% 24.17/9.47 % (1493553)Peak memory usage: 136 MB
% 24.17/9.47 % (1493553)Instructions burned: 185 (million)
% 24.17/9.47 % (1493556)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=1476513126:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2928 on theBenchmark for (2928ds/4850Mi)
% 24.17/9.47 % (1493555)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=29196645:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2928 on theBenchmark for (2928ds/193Mi)
% 24.17/9.47 % (1493555)Instruction limit reached!
% 24.17/9.47 % (1493555)------------------------------
% 24.17/9.47 % (1493555)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.17/9.47 % (1493555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.17/9.47 % (1493555)CaDiCaL version: 2.1.3
% 24.17/9.47 % (1493555)Termination reason: Instruction limit
% 24.17/9.47 % (1493555)Termination phase: SInE selection
% 24.17/9.47 % (1493555)Time elapsed: 0.148 s
% 24.17/9.47 % (1493555)Peak memory usage: 137 MB
% 24.17/9.47 % (1493555)Instructions burned: 194 (million)
% 24.17/9.47 % (1493559)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=2873875508:i=12111:sd=1:ss=included_2925 on theBenchmark for (2925ds/12111Mi)
% 24.17/9.47 % (1493495)First to succeed.
% 24.17/9.47 % (1493495)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1493488"
% 24.17/9.47 % (1493495)Refutation found. Thanks to Tanya!
% 24.17/9.47 % SZS status Theorem for theBenchmark
% 24.17/9.47 % SZS output start Proof for theBenchmark
% See solution above
% 0.16/9.71 % (1493495)------------------------------
% 0.16/9.71 % (1493495)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.16/9.71 % (1493495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.16/9.71 % (1493495)CaDiCaL version: 2.1.3
% 0.16/9.71 % (1493495)Termination reason: Refutation
% 0.16/9.71 % (1493495)Time elapsed: 5.893 s
% 0.16/9.71 % (1493495)Peak memory usage: 252 MB
% 0.16/9.71 % (1493495)Instructions burned: 10003 (million)
% 0.16/9.71 % (1493495)------------------------------
% 0.16/9.71 % (1493495)------------------------------
% 0.16/9.71 % (1493488)Success in time 8.628 s
% 0.16/9.71 % Vampire exiting
%------------------------------------------------------------------------------