%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT326+4 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n017.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:46:58 AM UTC 2026
% Result : Theorem 49.62s 10.97s
% Output : Refutation 57.84s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 41
% Syntax : Number of formulae : 367 ( 51 unt; 21 def)
% Number of atoms : 2081 ( 44 equ)
% Maximal formula atoms : 19 ( 5 avg)
% Number of connectives : 2919 (1205 ~;1395 |; 253 &)
% ( 20 <=>; 46 =>; 0 <=; 0 <~>)
% Maximal formula depth : 26 ( 7 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 48 ( 46 usr; 21 prp; 0-3 aty)
% Number of functors : 11 ( 11 usr; 4 con; 0-2 aty)
% Number of variables : 344 ( 0 sgn 336 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f18118,axiom,
! [X0] :
( l3_lattices(X0)
=> ( ( ~ v3_struct_0(X0)
& v10_lattices(X0) )
=> ( ~ v3_struct_0(X0)
& v4_lattices(X0)
& v5_lattices(X0)
& v6_lattices(X0)
& v7_lattices(X0)
& v8_lattices(X0)
& v9_lattices(X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc1_lattices) ).
fof(f18210,axiom,
! [X0] :
( l3_lattices(X0)
=> ( l1_lattices(X0)
& l2_lattices(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l3_lattices) ).
fof(f18228,axiom,
! [X0] :
( l1_lattices(X0)
=> ( v1_funct_1(u1_lattices(X0))
& v1_funct_2(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
& m2_relset_1(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_u1_lattices) ).
fof(f18229,axiom,
! [X0] :
( l2_lattices(X0)
=> ( v1_funct_1(u2_lattices(X0))
& v1_funct_2(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
& m2_relset_1(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_u2_lattices) ).
fof(f22747,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l3_lattices(X0) )
=> ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_lattice2) ).
fof(f22748,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v4_lattices(X0)
& l2_lattices(X0) )
=> ( v1_relat_1(u2_lattices(X0))
& v1_funct_1(u2_lattices(X0))
& v1_funct_2(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
& v1_binop_1(u2_lattices(X0),u1_struct_0(X0))
& v1_partfun1(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc2_lattice2) ).
fof(f22749,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v5_lattices(X0)
& l2_lattices(X0) )
=> ( v1_relat_1(u2_lattices(X0))
& v1_funct_1(u2_lattices(X0))
& v1_funct_2(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
& v2_binop_1(u2_lattices(X0),u1_struct_0(X0))
& v1_partfun1(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc3_lattice2) ).
fof(f22750,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v6_lattices(X0)
& l1_lattices(X0) )
=> ( v1_relat_1(u1_lattices(X0))
& v1_funct_1(u1_lattices(X0))
& v1_funct_2(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
& v1_binop_1(u1_lattices(X0),u1_struct_0(X0))
& v1_partfun1(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc4_lattice2) ).
fof(f22751,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v7_lattices(X0)
& l1_lattices(X0) )
=> ( v1_relat_1(u1_lattices(X0))
& v1_funct_1(u1_lattices(X0))
& v1_funct_2(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
& v2_binop_1(u1_lattices(X0),u1_struct_0(X0))
& v1_partfun1(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc5_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/sandbox2/benchmark/theBenchmark.p',fc6_lattice2) ).
fof(f22780,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l3_lattices(X0) )
=> ( u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0))
& u2_lattices(X0) = u1_lattices(k1_lattice2(X0))
& u1_lattices(X0) = u2_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t18_lattice2) ).
fof(f22802,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> r1_lattice2(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t40_lattice2) ).
fof(f22803,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> r1_lattice2(u1_struct_0(X0),u1_lattices(X0),u2_lattices(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t41_lattice2) ).
fof(f22852,axiom,
! [X0] :
( l3_lattices(X0)
=> ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k1_lattice2) ).
fof(f31985,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_lattice4(X1,X0)
=> m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m2_lattice4) ).
fof(f34485,axiom,
! [X0] :
( v1_xboole_0(X0)
=> ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(X0))
=> ( v1_xboole_0(X1)
& v1_finset_1(X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc1_sgraph1) ).
fof(f34650,axiom,
! [X0] :
( ~ v1_xboole_0(X0)
=> ! [X1] :
( ( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(X0)) )
=> ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
& m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0) )
=> ! [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) )
=> ( X3 = k1_realset1(X2,X1)
=> ( ( v1_binop_1(X2,X0)
=> v1_binop_1(X3,X1) )
& ( v3_binop_1(X2,X0)
=> v3_binop_1(X3,X1) )
& ( v2_binop_1(X2,X0)
=> v2_binop_1(X3,X1) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t1_filter_2) ).
fof(f34654,axiom,
! [X0] :
( ~ v1_xboole_0(X0)
=> ! [X1] :
( ( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(X0)) )
=> ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
& m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0) )
=> ! [X3] :
( ( v1_funct_1(X3)
& v1_funct_2(X3,k2_zfmisc_1(X0,X0),X0)
& m2_relset_1(X3,k2_zfmisc_1(X0,X0),X0) )
=> ! [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) )
=> ! [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) )
=> ( ( X4 = k1_realset1(X2,X1)
& X5 = k1_realset1(X3,X1)
& r1_lattice2(X0,X2,X3) )
=> r1_lattice2(X1,X4,X5) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_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/sandbox2/benchmark/theBenchmark.p',t61_filter_2) ).
fof(f34731,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) )
=> ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(X2,k2_zfmisc_1(X1,X1),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) )
=> ( ( X2 = k1_realset1(u2_lattices(X0),X1)
& X3 = k1_realset1(u1_lattices(X0),X1) )
=> ( v1_binop_1(X2,X1)
& v2_binop_1(X2,X1)
& v1_binop_1(X3,X1)
& v2_binop_1(X3,X1)
& r1_lattice2(X1,X2,X3)
& r1_lattice2(X1,X3,X2) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t62_filter_2) ).
fof(f34732,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) )
=> ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(X2,k2_zfmisc_1(X1,X1),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) )
=> ( ( X2 = k1_realset1(u2_lattices(X0),X1)
& X3 = k1_realset1(u1_lattices(X0),X1) )
=> ( v1_binop_1(X2,X1)
& v2_binop_1(X2,X1)
& v1_binop_1(X3,X1)
& v2_binop_1(X3,X1)
& r1_lattice2(X1,X2,X3)
& r1_lattice2(X1,X3,X2) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f34731]) ).
fof(f35198,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( ( ~ v1_binop_1(X2,X1)
| ~ v2_binop_1(X2,X1)
| ~ v1_binop_1(X3,X1)
| ~ v2_binop_1(X3,X1)
| ~ r1_lattice2(X1,X2,X3)
| ~ r1_lattice2(X1,X3,X2) )
& X2 = k1_realset1(u2_lattices(X0),X1)
& X3 = k1_realset1(u1_lattices(X0),X1)
& 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(X2)
& v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(X2,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,[],[f34732]) ).
fof(f35199,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( ( ~ v1_binop_1(X2,X1)
| ~ v2_binop_1(X2,X1)
| ~ v1_binop_1(X3,X1)
| ~ v2_binop_1(X3,X1)
| ~ r1_lattice2(X1,X2,X3)
| ~ r1_lattice2(X1,X3,X2) )
& X2 = k1_realset1(u2_lattices(X0),X1)
& X3 = k1_realset1(u1_lattices(X0),X1)
& 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(X2)
& v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(X2,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,[],[f35198]) ).
fof(f35362,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( r1_lattice2(X1,X4,X5)
| k1_realset1(X2,X1) != X4
| k1_realset1(X3,X1) != X5
| ~ r1_lattice2(X0,X2,X3)
| ~ v1_funct_1(X5)
| ~ v1_funct_2(X5,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(X5,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) )
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X3,k2_zfmisc_1(X0,X0),X0) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0)) )
| v1_xboole_0(X0) ),
inference(ennf_transformation,[],[f34654]) ).
fof(f35363,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( r1_lattice2(X1,X4,X5)
| k1_realset1(X2,X1) != X4
| k1_realset1(X3,X1) != X5
| ~ r1_lattice2(X0,X2,X3)
| ~ v1_funct_1(X5)
| ~ v1_funct_2(X5,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(X5,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) )
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X3,k2_zfmisc_1(X0,X0),X0) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0)) )
| v1_xboole_0(X0) ),
inference(flattening,[],[f35362]) ).
fof(f35370,plain,
! [X0] :
( r1_lattice2(u1_struct_0(X0),u1_lattices(X0),u2_lattices(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f22803]) ).
fof(f35371,plain,
! [X0] :
( r1_lattice2(u1_struct_0(X0),u1_lattices(X0),u2_lattices(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35370]) ).
fof(f35372,plain,
! [X0] :
( r1_lattice2(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f22802]) ).
fof(f35373,plain,
! [X0] :
( r1_lattice2(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35372]) ).
fof(f35378,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(f35379,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,[],[f35378]) ).
fof(f35382,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( ( v1_binop_1(X3,X1)
| ~ v1_binop_1(X2,X0) )
& ( v3_binop_1(X3,X1)
| ~ v3_binop_1(X2,X0) )
& ( v2_binop_1(X3,X1)
| ~ v2_binop_1(X2,X0) ) )
| k1_realset1(X2,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) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0)) )
| v1_xboole_0(X0) ),
inference(ennf_transformation,[],[f34650]) ).
fof(f35383,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( ( v1_binop_1(X3,X1)
| ~ v1_binop_1(X2,X0) )
& ( v3_binop_1(X3,X1)
| ~ v3_binop_1(X2,X0) )
& ( v2_binop_1(X3,X1)
| ~ v2_binop_1(X2,X0) ) )
| k1_realset1(X2,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) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0)) )
| v1_xboole_0(X0) ),
inference(flattening,[],[f35382]) ).
fof(f35416,plain,
! [X0] :
( ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m2_lattice4(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f31985]) ).
fof(f35417,plain,
! [X0] :
( ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m2_lattice4(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35416]) ).
fof(f35476,plain,
! [X0] :
( ( u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0))
& u2_lattices(X0) = u1_lattices(k1_lattice2(X0))
& u1_lattices(X0) = u2_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f22780]) ).
fof(f35477,plain,
! [X0] :
( ( u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0))
& u2_lattices(X0) = u1_lattices(k1_lattice2(X0))
& u1_lattices(X0) = u2_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35476]) ).
fof(f35479,plain,
! [X0] :
( ( v1_relat_1(u2_lattices(X0))
& v1_funct_1(u2_lattices(X0))
& v1_funct_2(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
& v2_binop_1(u2_lattices(X0),u1_struct_0(X0))
& v1_partfun1(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v5_lattices(X0)
| ~ l2_lattices(X0) ),
inference(ennf_transformation,[],[f22749]) ).
fof(f35480,plain,
! [X0] :
( ( v1_relat_1(u2_lattices(X0))
& v1_funct_1(u2_lattices(X0))
& v1_funct_2(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
& v2_binop_1(u2_lattices(X0),u1_struct_0(X0))
& v1_partfun1(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v5_lattices(X0)
| ~ l2_lattices(X0) ),
inference(flattening,[],[f35479]) ).
fof(f35481,plain,
! [X0] :
( ( v1_relat_1(u2_lattices(X0))
& v1_funct_1(u2_lattices(X0))
& v1_funct_2(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
& v1_binop_1(u2_lattices(X0),u1_struct_0(X0))
& v1_partfun1(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v4_lattices(X0)
| ~ l2_lattices(X0) ),
inference(ennf_transformation,[],[f22748]) ).
fof(f35482,plain,
! [X0] :
( ( v1_relat_1(u2_lattices(X0))
& v1_funct_1(u2_lattices(X0))
& v1_funct_2(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
& v1_binop_1(u2_lattices(X0),u1_struct_0(X0))
& v1_partfun1(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v4_lattices(X0)
| ~ l2_lattices(X0) ),
inference(flattening,[],[f35481]) ).
fof(f35483,plain,
! [X0] :
( ( v1_funct_1(u2_lattices(X0))
& v1_funct_2(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
& m2_relset_1(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0)) )
| ~ l2_lattices(X0) ),
inference(ennf_transformation,[],[f18229]) ).
fof(f35510,plain,
! [X0] :
( ( v1_relat_1(u1_lattices(X0))
& v1_funct_1(u1_lattices(X0))
& v1_funct_2(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
& v2_binop_1(u1_lattices(X0),u1_struct_0(X0))
& v1_partfun1(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v7_lattices(X0)
| ~ l1_lattices(X0) ),
inference(ennf_transformation,[],[f22751]) ).
fof(f35511,plain,
! [X0] :
( ( v1_relat_1(u1_lattices(X0))
& v1_funct_1(u1_lattices(X0))
& v1_funct_2(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
& v2_binop_1(u1_lattices(X0),u1_struct_0(X0))
& v1_partfun1(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v7_lattices(X0)
| ~ l1_lattices(X0) ),
inference(flattening,[],[f35510]) ).
fof(f35512,plain,
! [X0] :
( ( v1_relat_1(u1_lattices(X0))
& v1_funct_1(u1_lattices(X0))
& v1_funct_2(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
& v1_binop_1(u1_lattices(X0),u1_struct_0(X0))
& v1_partfun1(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v6_lattices(X0)
| ~ l1_lattices(X0) ),
inference(ennf_transformation,[],[f22750]) ).
fof(f35513,plain,
! [X0] :
( ( v1_relat_1(u1_lattices(X0))
& v1_funct_1(u1_lattices(X0))
& v1_funct_2(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
& v1_binop_1(u1_lattices(X0),u1_struct_0(X0))
& v1_partfun1(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v6_lattices(X0)
| ~ l1_lattices(X0) ),
inference(flattening,[],[f35512]) ).
fof(f35514,plain,
! [X0] :
( ( v1_funct_1(u1_lattices(X0))
& v1_funct_2(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
& m2_relset_1(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0)) )
| ~ l1_lattices(X0) ),
inference(ennf_transformation,[],[f18228]) ).
fof(f35889,plain,
! [X0] :
( ! [X1] :
( ( v1_xboole_0(X1)
& v1_finset_1(X1) )
| ~ m1_subset_1(X1,k1_zfmisc_1(X0)) )
| ~ v1_xboole_0(X0) ),
inference(ennf_transformation,[],[f34485]) ).
fof(f37868,plain,
! [X0] :
( ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f22852]) ).
fof(f37881,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(f37882,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,[],[f37881]) ).
fof(f37883,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(f37884,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f37883]) ).
fof(f37955,plain,
! [X0] :
( ( l1_lattices(X0)
& l2_lattices(X0) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f18210]) ).
fof(f37975,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v4_lattices(X0)
& v5_lattices(X0)
& v6_lattices(X0)
& v7_lattices(X0)
& v8_lattices(X0)
& v9_lattices(X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f18118]) ).
fof(f37976,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v4_lattices(X0)
& v5_lattices(X0)
& v6_lattices(X0)
& v7_lattices(X0)
& v8_lattices(X0)
& v9_lattices(X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f37975]) ).
fof(f44913,definition,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v4_lattices(k1_lattice2(X0))
& v5_lattices(k1_lattice2(X0))
& v6_lattices(k1_lattice2(X0))
& v7_lattices(k1_lattice2(X0))
& v8_lattices(k1_lattice2(X0))
& v9_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0)) )
| ~ sP53(X0) ),
introduced(definition,[new_symbols(definition,[sP53])],[predicate_definition_introduction]) ).
fof(f44914,plain,
! [X0] :
( sP53(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(definition_folding,[],[f37882,f44913]) ).
fof(f45362,plain,
( ( ~ v1_binop_1(sK355,sK354)
| ~ v2_binop_1(sK355,sK354)
| ~ v1_binop_1(sK356,sK354)
| ~ v2_binop_1(sK356,sK354)
| ~ r1_lattice2(sK354,sK355,sK356)
| ~ r1_lattice2(sK354,sK356,sK355) )
& sK355 = k1_realset1(u2_lattices(sK353),sK354)
& sK356 = k1_realset1(u1_lattices(sK353),sK354)
& v1_funct_1(sK356)
& v1_funct_2(sK356,k2_zfmisc_1(sK354,sK354),sK354)
& m2_relset_1(sK356,k2_zfmisc_1(sK354,sK354),sK354)
& v1_funct_1(sK355)
& v1_funct_2(sK355,k2_zfmisc_1(sK354,sK354),sK354)
& m2_relset_1(sK355,k2_zfmisc_1(sK354,sK354),sK354)
& ~ v1_xboole_0(sK354)
& m2_lattice4(sK354,sK353)
& ~ v3_struct_0(sK353)
& v10_lattices(sK353)
& l3_lattices(sK353) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK353,sK354,sK355,sK356]),skolemize(X0,sK353),skolemize(X1,sK354),skolemize(X2,sK355),skolemize(X3,sK356)],[f35199]) ).
fof(f46265,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)) )
| ~ sP53(X0) ),
inference(nnf_transformation,[],[f44913]) ).
fof(f48779,plain,
l3_lattices(sK353),
inference(cnf_transformation,[],[f45362]) ).
fof(f48780,plain,
v10_lattices(sK353),
inference(cnf_transformation,[],[f45362]) ).
fof(f48781,plain,
~ v3_struct_0(sK353),
inference(cnf_transformation,[],[f45362]) ).
fof(f48782,plain,
m2_lattice4(sK354,sK353),
inference(cnf_transformation,[],[f45362]) ).
fof(f48783,plain,
~ v1_xboole_0(sK354),
inference(cnf_transformation,[],[f45362]) ).
fof(f48784,plain,
m2_relset_1(sK355,k2_zfmisc_1(sK354,sK354),sK354),
inference(cnf_transformation,[],[f45362]) ).
fof(f48785,plain,
v1_funct_2(sK355,k2_zfmisc_1(sK354,sK354),sK354),
inference(cnf_transformation,[],[f45362]) ).
fof(f48786,plain,
v1_funct_1(sK355),
inference(cnf_transformation,[],[f45362]) ).
fof(f48787,plain,
m2_relset_1(sK356,k2_zfmisc_1(sK354,sK354),sK354),
inference(cnf_transformation,[],[f45362]) ).
fof(f48788,plain,
v1_funct_2(sK356,k2_zfmisc_1(sK354,sK354),sK354),
inference(cnf_transformation,[],[f45362]) ).
fof(f48789,plain,
v1_funct_1(sK356),
inference(cnf_transformation,[],[f45362]) ).
fof(f48790,plain,
sK356 = k1_realset1(u1_lattices(sK353),sK354),
inference(cnf_transformation,[],[f45362]) ).
fof(f48791,plain,
sK355 = k1_realset1(u2_lattices(sK353),sK354),
inference(cnf_transformation,[],[f45362]) ).
fof(f48792,plain,
( ~ v1_binop_1(sK355,sK354)
| ~ v2_binop_1(sK355,sK354)
| ~ v1_binop_1(sK356,sK354)
| ~ v2_binop_1(sK356,sK354)
| ~ r1_lattice2(sK354,sK355,sK356)
| ~ r1_lattice2(sK354,sK356,sK355) ),
inference(cnf_transformation,[],[f45362]) ).
fof(f49032,plain,
! [X2,X3,X0,X1,X4,X5] :
( r1_lattice2(X1,X4,X5)
| k1_realset1(X2,X1) != X4
| k1_realset1(X3,X1) != X5
| ~ r1_lattice2(X0,X2,X3)
| ~ v1_funct_1(X5)
| ~ v1_funct_2(X5,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(X5,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)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X3,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f35363]) ).
fof(f49038,plain,
! [X0] :
( r1_lattice2(u1_struct_0(X0),u1_lattices(X0),u2_lattices(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35371]) ).
fof(f49039,plain,
! [X0] :
( r1_lattice2(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35373]) ).
fof(f49045,plain,
! [X0,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(cnf_transformation,[],[f35379]) ).
fof(f49046,plain,
! [X0,X1] :
( v1_funct_2(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(cnf_transformation,[],[f35379]) ).
fof(f49047,plain,
! [X0,X1] :
( v1_funct_1(k1_realset1(u1_lattices(X0),X1))
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35379]) ).
fof(f49048,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,[],[f35379]) ).
fof(f49049,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,[],[f35379]) ).
fof(f49050,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,[],[f35379]) ).
fof(f49052,plain,
! [X2,X3,X0,X1] :
( v2_binop_1(X3,X1)
| ~ v2_binop_1(X2,X0)
| k1_realset1(X2,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)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f35383]) ).
fof(f49054,plain,
! [X2,X3,X0,X1] :
( v1_binop_1(X3,X1)
| ~ v1_binop_1(X2,X0)
| k1_realset1(X2,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)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f35383]) ).
fof(f49117,plain,
! [X0,X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35417]) ).
fof(f49161,plain,
! [X0] :
( ~ l3_lattices(X0)
| v3_struct_0(X0)
| u1_lattices(X0) = u2_lattices(k1_lattice2(X0)) ),
inference(cnf_transformation,[],[f35477]) ).
fof(f49162,plain,
! [X0] :
( ~ l3_lattices(X0)
| v3_struct_0(X0)
| u2_lattices(X0) = u1_lattices(k1_lattice2(X0)) ),
inference(cnf_transformation,[],[f35477]) ).
fof(f49163,plain,
! [X0] :
( ~ l3_lattices(X0)
| v3_struct_0(X0)
| u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0)) ),
inference(cnf_transformation,[],[f35477]) ).
fof(f49166,plain,
! [X0] :
( v2_binop_1(u2_lattices(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v5_lattices(X0)
| ~ l2_lattices(X0) ),
inference(cnf_transformation,[],[f35480]) ).
fof(f49171,plain,
! [X0] :
( v1_binop_1(u2_lattices(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v4_lattices(X0)
| ~ l2_lattices(X0) ),
inference(cnf_transformation,[],[f35482]) ).
fof(f49175,plain,
! [X0] :
( m2_relset_1(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| ~ l2_lattices(X0) ),
inference(cnf_transformation,[],[f35483]) ).
fof(f49176,plain,
! [X0] :
( v1_funct_2(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| ~ l2_lattices(X0) ),
inference(cnf_transformation,[],[f35483]) ).
fof(f49177,plain,
! [X0] :
( v1_funct_1(u2_lattices(X0))
| ~ l2_lattices(X0) ),
inference(cnf_transformation,[],[f35483]) ).
fof(f49193,plain,
! [X0] :
( v2_binop_1(u1_lattices(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v7_lattices(X0)
| ~ l1_lattices(X0) ),
inference(cnf_transformation,[],[f35511]) ).
fof(f49198,plain,
! [X0] :
( v1_binop_1(u1_lattices(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v6_lattices(X0)
| ~ l1_lattices(X0) ),
inference(cnf_transformation,[],[f35513]) ).
fof(f49202,plain,
! [X0] :
( m2_relset_1(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| ~ l1_lattices(X0) ),
inference(cnf_transformation,[],[f35514]) ).
fof(f49203,plain,
! [X0] :
( v1_funct_2(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| ~ l1_lattices(X0) ),
inference(cnf_transformation,[],[f35514]) ).
fof(f49204,plain,
! [X0] :
( v1_funct_1(u1_lattices(X0))
| ~ l1_lattices(X0) ),
inference(cnf_transformation,[],[f35514]) ).
fof(f49838,plain,
! [X0,X1] :
( v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f35889]) ).
fof(f52426,plain,
! [X0] :
( l3_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f37868]) ).
fof(f52443,plain,
! [X0] :
( v10_lattices(k1_lattice2(X0))
| ~ sP53(X0) ),
inference(cnf_transformation,[],[f46265]) ).
fof(f52452,plain,
! [X0] :
( ~ v10_lattices(X0)
| v3_struct_0(X0)
| sP53(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f44914]) ).
fof(f52454,plain,
! [X0] :
( ~ v3_struct_0(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f37884]) ).
fof(f52510,plain,
! [X0] :
( ~ l3_lattices(X0)
| l2_lattices(X0) ),
inference(cnf_transformation,[],[f37955]) ).
fof(f52511,plain,
! [X0] :
( ~ l3_lattices(X0)
| l1_lattices(X0) ),
inference(cnf_transformation,[],[f37955]) ).
fof(f52681,plain,
! [X0] :
( v7_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f37976]) ).
fof(f52682,plain,
! [X0] :
( v6_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f37976]) ).
fof(f52683,plain,
! [X0] :
( v5_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f37976]) ).
fof(f52684,plain,
! [X0] :
( v4_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f37976]) ).
fof(f65078,plain,
! [X2,X3,X0,X1,X5] :
( r1_lattice2(X1,k1_realset1(X2,X1),X5)
| k1_realset1(X3,X1) != X5
| ~ r1_lattice2(X0,X2,X3)
| ~ v1_funct_1(X5)
| ~ v1_funct_2(X5,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(X5,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(k1_realset1(X2,X1))
| ~ v1_funct_2(k1_realset1(X2,X1),k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(k1_realset1(X2,X1),k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X3,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| v1_xboole_0(X0) ),
inference(equality_resolution,[],[f49032]) ).
fof(f65079,plain,
! [X2,X3,X0,X1] :
( r1_lattice2(X1,k1_realset1(X2,X1),k1_realset1(X3,X1))
| ~ r1_lattice2(X0,X2,X3)
| ~ v1_funct_1(k1_realset1(X3,X1))
| ~ v1_funct_2(k1_realset1(X3,X1),k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(k1_realset1(X3,X1),k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(k1_realset1(X2,X1))
| ~ v1_funct_2(k1_realset1(X2,X1),k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(k1_realset1(X2,X1),k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X3,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| v1_xboole_0(X0) ),
inference(equality_resolution,[],[f65078]) ).
fof(f65082,plain,
! [X2,X0,X1] :
( v1_binop_1(k1_realset1(X2,X1),X1)
| ~ v1_binop_1(X2,X0)
| ~ v1_funct_1(k1_realset1(X2,X1))
| ~ v1_funct_2(k1_realset1(X2,X1),k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(k1_realset1(X2,X1),k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| v1_xboole_0(X0) ),
inference(equality_resolution,[],[f49054]) ).
fof(f65084,plain,
! [X2,X0,X1] :
( v2_binop_1(k1_realset1(X2,X1),X1)
| ~ v2_binop_1(X2,X0)
| ~ v1_funct_1(k1_realset1(X2,X1))
| ~ v1_funct_2(k1_realset1(X2,X1),k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(k1_realset1(X2,X1),k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| v1_xboole_0(X0) ),
inference(equality_resolution,[],[f49052]) ).
fof(f67468,plain,
! [X2,X0,X1] :
( ~ v1_funct_2(k1_realset1(X2,X1),k2_zfmisc_1(X1,X1),X1)
| ~ v2_binop_1(X2,X0)
| ~ v1_funct_1(k1_realset1(X2,X1))
| v2_binop_1(k1_realset1(X2,X1),X1)
| ~ m2_relset_1(k1_realset1(X2,X1),k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0)) ),
inference(forward_subsumption_resolution,[],[f65084,f49838]) ).
fof(f67470,plain,
! [X2,X0,X1] :
( ~ v1_funct_2(k1_realset1(X2,X1),k2_zfmisc_1(X1,X1),X1)
| ~ v1_binop_1(X2,X0)
| ~ v1_funct_1(k1_realset1(X2,X1))
| v1_binop_1(k1_realset1(X2,X1),X1)
| ~ m2_relset_1(k1_realset1(X2,X1),k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0)) ),
inference(forward_subsumption_resolution,[],[f65082,f49838]) ).
fof(f67472,plain,
! [X2,X3,X0,X1] :
( ~ v1_funct_2(k1_realset1(X3,X1),k2_zfmisc_1(X1,X1),X1)
| ~ r1_lattice2(X0,X2,X3)
| ~ v1_funct_1(k1_realset1(X3,X1))
| r1_lattice2(X1,k1_realset1(X2,X1),k1_realset1(X3,X1))
| ~ m2_relset_1(k1_realset1(X3,X1),k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(k1_realset1(X2,X1))
| ~ v1_funct_2(k1_realset1(X2,X1),k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(k1_realset1(X2,X1),k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X3,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0)) ),
inference(forward_subsumption_resolution,[],[f65079,f49838]) ).
fof(f67521,definition,
( spl2453_58
<=> r1_lattice2(sK354,sK356,sK355) ),
introduced(definition,[new_symbols(definition,[spl2453_58])],[avatar_definition]) ).
fof(f67523,plain,
( ~ r1_lattice2(sK354,sK356,sK355)
| spl2453_58 ),
inference(avatar_component_clause,[],[f67521]) ).
fof(f67525,definition,
( spl2453_59
<=> r1_lattice2(sK354,sK355,sK356) ),
introduced(definition,[new_symbols(definition,[spl2453_59])],[avatar_definition]) ).
fof(f67529,definition,
( spl2453_60
<=> v2_binop_1(sK356,sK354) ),
introduced(definition,[new_symbols(definition,[spl2453_60])],[avatar_definition]) ).
fof(f67531,plain,
( ~ v2_binop_1(sK356,sK354)
| spl2453_60 ),
inference(avatar_component_clause,[],[f67529]) ).
fof(f67533,definition,
( spl2453_61
<=> v1_binop_1(sK356,sK354) ),
introduced(definition,[new_symbols(definition,[spl2453_61])],[avatar_definition]) ).
fof(f67535,plain,
( ~ v1_binop_1(sK356,sK354)
| spl2453_61 ),
inference(avatar_component_clause,[],[f67533]) ).
fof(f67537,definition,
( spl2453_62
<=> v2_binop_1(sK355,sK354) ),
introduced(definition,[new_symbols(definition,[spl2453_62])],[avatar_definition]) ).
fof(f67539,plain,
( ~ v2_binop_1(sK355,sK354)
| spl2453_62 ),
inference(avatar_component_clause,[],[f67537]) ).
fof(f67541,definition,
( spl2453_63
<=> v1_binop_1(sK355,sK354) ),
introduced(definition,[new_symbols(definition,[spl2453_63])],[avatar_definition]) ).
fof(f67543,plain,
( ~ v1_binop_1(sK355,sK354)
| spl2453_63 ),
inference(avatar_component_clause,[],[f67541]) ).
fof(f67544,plain,
( ~ spl2453_58
| ~ spl2453_59
| ~ spl2453_60
| ~ spl2453_61
| ~ spl2453_62
| ~ spl2453_63 ),
inference(avatar_split_clause,[],[f48792,f67541,f67537,f67533,f67529,f67525,f67521]) ).
fof(f68569,plain,
! [X0,X1] :
( ~ v1_funct_2(sK355,k2_zfmisc_1(sK354,sK354),sK354)
| ~ r1_lattice2(X0,X1,u2_lattices(sK353))
| ~ v1_funct_1(sK355)
| r1_lattice2(sK354,k1_realset1(X1,sK354),sK355)
| ~ m2_relset_1(sK355,k2_zfmisc_1(sK354,sK354),sK354)
| ~ v1_funct_1(k1_realset1(X1,sK354))
| ~ v1_funct_2(k1_realset1(X1,sK354),k2_zfmisc_1(sK354,sK354),sK354)
| ~ m2_relset_1(k1_realset1(X1,sK354),k2_zfmisc_1(sK354,sK354),sK354)
| ~ v1_funct_1(u2_lattices(sK353))
| ~ v1_funct_2(u2_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(u2_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| v1_xboole_0(sK354)
| ~ m1_subset_1(sK354,k1_zfmisc_1(X0)) ),
inference(superposition,[],[f67472,f48791]) ).
fof(f68572,plain,
! [X0,X1] :
( ~ v1_funct_2(sK356,k2_zfmisc_1(sK354,sK354),sK354)
| ~ r1_lattice2(X0,X1,u1_lattices(sK353))
| ~ v1_funct_1(sK356)
| r1_lattice2(sK354,k1_realset1(X1,sK354),sK356)
| ~ m2_relset_1(sK356,k2_zfmisc_1(sK354,sK354),sK354)
| ~ v1_funct_1(k1_realset1(X1,sK354))
| ~ v1_funct_2(k1_realset1(X1,sK354),k2_zfmisc_1(sK354,sK354),sK354)
| ~ m2_relset_1(k1_realset1(X1,sK354),k2_zfmisc_1(sK354,sK354),sK354)
| ~ v1_funct_1(u1_lattices(sK353))
| ~ v1_funct_2(u1_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(u1_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| v1_xboole_0(sK354)
| ~ m1_subset_1(sK354,k1_zfmisc_1(X0)) ),
inference(superposition,[],[f67472,f48790]) ).
fof(f68585,plain,
! [X2,X0,X1] :
( ~ v2_binop_1(u2_lattices(X0),X1)
| ~ v1_funct_1(k1_realset1(u2_lattices(X0),X2))
| v2_binop_1(k1_realset1(u2_lattices(X0),X2),X2)
| ~ m2_relset_1(k1_realset1(u2_lattices(X0),X2),k2_zfmisc_1(X2,X2),X2)
| ~ v1_funct_1(u2_lattices(X0))
| ~ v1_funct_2(u2_lattices(X0),k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(u2_lattices(X0),k2_zfmisc_1(X1,X1),X1)
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(X1))
| v1_xboole_0(X2)
| ~ m2_lattice4(X2,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(resolution,[],[f67468,f49049]) ).
fof(f68586,plain,
! [X2,X0,X1] :
( ~ v2_binop_1(u1_lattices(X0),X1)
| ~ v1_funct_1(k1_realset1(u1_lattices(X0),X2))
| v2_binop_1(k1_realset1(u1_lattices(X0),X2),X2)
| ~ m2_relset_1(k1_realset1(u1_lattices(X0),X2),k2_zfmisc_1(X2,X2),X2)
| ~ v1_funct_1(u1_lattices(X0))
| ~ v1_funct_2(u1_lattices(X0),k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(u1_lattices(X0),k2_zfmisc_1(X1,X1),X1)
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(X1))
| v1_xboole_0(X2)
| ~ m2_lattice4(X2,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(resolution,[],[f67468,f49046]) ).
fof(f68589,plain,
! [X2,X0,X1] :
( ~ v2_binop_1(u1_lattices(X0),X1)
| ~ v1_funct_1(k1_realset1(u1_lattices(X0),X2))
| v2_binop_1(k1_realset1(u1_lattices(X0),X2),X2)
| ~ m2_relset_1(k1_realset1(u1_lattices(X0),X2),k2_zfmisc_1(X2,X2),X2)
| ~ v1_funct_1(u1_lattices(X0))
| ~ v1_funct_2(u1_lattices(X0),k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(u1_lattices(X0),k2_zfmisc_1(X1,X1),X1)
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(X1))
| ~ m2_lattice4(X2,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(duplicate_literal_removal,[],[f68586]) ).
fof(f68590,plain,
! [X2,X0,X1] :
( ~ v2_binop_1(u2_lattices(X0),X1)
| ~ v1_funct_1(k1_realset1(u2_lattices(X0),X2))
| v2_binop_1(k1_realset1(u2_lattices(X0),X2),X2)
| ~ m2_relset_1(k1_realset1(u2_lattices(X0),X2),k2_zfmisc_1(X2,X2),X2)
| ~ v1_funct_1(u2_lattices(X0))
| ~ v1_funct_2(u2_lattices(X0),k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(u2_lattices(X0),k2_zfmisc_1(X1,X1),X1)
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(X1))
| ~ m2_lattice4(X2,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(duplicate_literal_removal,[],[f68585]) ).
fof(f68591,plain,
! [X2,X0,X1] :
( ~ v1_binop_1(u2_lattices(X0),X1)
| ~ v1_funct_1(k1_realset1(u2_lattices(X0),X2))
| v1_binop_1(k1_realset1(u2_lattices(X0),X2),X2)
| ~ m2_relset_1(k1_realset1(u2_lattices(X0),X2),k2_zfmisc_1(X2,X2),X2)
| ~ v1_funct_1(u2_lattices(X0))
| ~ v1_funct_2(u2_lattices(X0),k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(u2_lattices(X0),k2_zfmisc_1(X1,X1),X1)
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(X1))
| v1_xboole_0(X2)
| ~ m2_lattice4(X2,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(resolution,[],[f67470,f49049]) ).
fof(f68592,plain,
! [X2,X0,X1] :
( ~ v1_binop_1(u1_lattices(X0),X1)
| ~ v1_funct_1(k1_realset1(u1_lattices(X0),X2))
| v1_binop_1(k1_realset1(u1_lattices(X0),X2),X2)
| ~ m2_relset_1(k1_realset1(u1_lattices(X0),X2),k2_zfmisc_1(X2,X2),X2)
| ~ v1_funct_1(u1_lattices(X0))
| ~ v1_funct_2(u1_lattices(X0),k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(u1_lattices(X0),k2_zfmisc_1(X1,X1),X1)
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(X1))
| v1_xboole_0(X2)
| ~ m2_lattice4(X2,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(resolution,[],[f67470,f49046]) ).
fof(f68595,plain,
! [X2,X0,X1] :
( ~ v1_binop_1(u1_lattices(X0),X1)
| ~ v1_funct_1(k1_realset1(u1_lattices(X0),X2))
| v1_binop_1(k1_realset1(u1_lattices(X0),X2),X2)
| ~ m2_relset_1(k1_realset1(u1_lattices(X0),X2),k2_zfmisc_1(X2,X2),X2)
| ~ v1_funct_1(u1_lattices(X0))
| ~ v1_funct_2(u1_lattices(X0),k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(u1_lattices(X0),k2_zfmisc_1(X1,X1),X1)
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(X1))
| ~ m2_lattice4(X2,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(duplicate_literal_removal,[],[f68592]) ).
fof(f68596,plain,
! [X2,X0,X1] :
( ~ v1_binop_1(u2_lattices(X0),X1)
| ~ v1_funct_1(k1_realset1(u2_lattices(X0),X2))
| v1_binop_1(k1_realset1(u2_lattices(X0),X2),X2)
| ~ m2_relset_1(k1_realset1(u2_lattices(X0),X2),k2_zfmisc_1(X2,X2),X2)
| ~ v1_funct_1(u2_lattices(X0))
| ~ v1_funct_2(u2_lattices(X0),k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(u2_lattices(X0),k2_zfmisc_1(X1,X1),X1)
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(X1))
| ~ m2_lattice4(X2,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(duplicate_literal_removal,[],[f68591]) ).
fof(f68597,plain,
( v3_struct_0(sK353)
| u1_lattices(sK353) = u2_lattices(k1_lattice2(sK353)) ),
inference(resolution,[],[f49161,f48779]) ).
fof(f68598,plain,
u1_lattices(sK353) = u2_lattices(k1_lattice2(sK353)),
inference(forward_subsumption_resolution,[],[f68597,f48781]) ).
fof(f68605,plain,
( v3_struct_0(sK353)
| u2_lattices(sK353) = u1_lattices(k1_lattice2(sK353)) ),
inference(resolution,[],[f49162,f48779]) ).
fof(f68606,plain,
u2_lattices(sK353) = u1_lattices(k1_lattice2(sK353)),
inference(forward_subsumption_resolution,[],[f68605,f48781]) ).
fof(f68679,definition,
( spl2453_71
<=> l1_lattices(k1_lattice2(sK353)) ),
introduced(definition,[new_symbols(definition,[spl2453_71])],[avatar_definition]) ).
fof(f68680,plain,
( l1_lattices(k1_lattice2(sK353))
| ~ spl2453_71 ),
inference(avatar_component_clause,[],[f68679]) ).
fof(f68681,plain,
( ~ l1_lattices(k1_lattice2(sK353))
| spl2453_71 ),
inference(avatar_component_clause,[],[f68679]) ).
fof(f68700,plain,
( v3_struct_0(sK353)
| sP53(sK353)
| ~ l3_lattices(sK353) ),
inference(resolution,[],[f52452,f48780]) ).
fof(f68701,plain,
( sP53(sK353)
| ~ l3_lattices(sK353) ),
inference(forward_subsumption_resolution,[],[f68700,f48781]) ).
fof(f68702,plain,
sP53(sK353),
inference(forward_subsumption_resolution,[],[f68701,f48779]) ).
fof(f68703,plain,
( v3_struct_0(sK353)
| u1_struct_0(k1_lattice2(sK353)) = u1_struct_0(sK353) ),
inference(resolution,[],[f49163,f48779]) ).
fof(f68705,plain,
u1_struct_0(k1_lattice2(sK353)) = u1_struct_0(sK353),
inference(forward_subsumption_resolution,[],[f68703,f48781]) ).
fof(f68706,plain,
( r1_lattice2(u1_struct_0(sK353),u1_lattices(k1_lattice2(sK353)),u2_lattices(k1_lattice2(sK353)))
| v3_struct_0(k1_lattice2(sK353))
| ~ v10_lattices(k1_lattice2(sK353))
| ~ l3_lattices(k1_lattice2(sK353)) ),
inference(superposition,[],[f49038,f68705]) ).
fof(f68707,plain,
( r1_lattice2(u1_struct_0(sK353),u2_lattices(k1_lattice2(sK353)),u1_lattices(k1_lattice2(sK353)))
| v3_struct_0(k1_lattice2(sK353))
| ~ v10_lattices(k1_lattice2(sK353))
| ~ l3_lattices(k1_lattice2(sK353)) ),
inference(superposition,[],[f49039,f68705]) ).
fof(f68714,plain,
( m2_relset_1(u1_lattices(k1_lattice2(sK353)),k2_zfmisc_1(u1_struct_0(sK353),u1_struct_0(sK353)),u1_struct_0(sK353))
| ~ l1_lattices(k1_lattice2(sK353)) ),
inference(superposition,[],[f49202,f68705]) ).
fof(f68723,definition,
( spl2453_74
<=> v3_struct_0(k1_lattice2(sK353)) ),
introduced(definition,[new_symbols(definition,[spl2453_74])],[avatar_definition]) ).
fof(f68725,plain,
( v3_struct_0(k1_lattice2(sK353))
| ~ spl2453_74 ),
inference(avatar_component_clause,[],[f68723]) ).
fof(f68735,plain,
( v1_funct_2(u1_lattices(k1_lattice2(sK353)),k2_zfmisc_1(u1_struct_0(sK353),u1_struct_0(sK353)),u1_struct_0(sK353))
| ~ l1_lattices(k1_lattice2(sK353)) ),
inference(superposition,[],[f49203,f68705]) ).
fof(f68827,plain,
l2_lattices(sK353),
inference(resolution,[],[f52510,f48779]) ).
fof(f68833,plain,
l1_lattices(sK353),
inference(resolution,[],[f52511,f48779]) ).
fof(f68908,definition,
( spl2453_83
<=> l3_lattices(k1_lattice2(sK353)) ),
introduced(definition,[new_symbols(definition,[spl2453_83])],[avatar_definition]) ).
fof(f68909,plain,
( l3_lattices(k1_lattice2(sK353))
| ~ spl2453_83 ),
inference(avatar_component_clause,[],[f68908]) ).
fof(f68910,plain,
( ~ l3_lattices(k1_lattice2(sK353))
| spl2453_83 ),
inference(avatar_component_clause,[],[f68908]) ).
fof(f68912,definition,
( spl2453_84
<=> v10_lattices(k1_lattice2(sK353)) ),
introduced(definition,[new_symbols(definition,[spl2453_84])],[avatar_definition]) ).
fof(f68914,plain,
( ~ v10_lattices(k1_lattice2(sK353))
| spl2453_84 ),
inference(avatar_component_clause,[],[f68912]) ).
fof(f68927,plain,
( r1_lattice2(u1_struct_0(sK353),u2_lattices(k1_lattice2(sK353)),u2_lattices(sK353))
| v3_struct_0(k1_lattice2(sK353))
| ~ v10_lattices(k1_lattice2(sK353))
| ~ l3_lattices(k1_lattice2(sK353)) ),
inference(forward_demodulation,[],[f68707,f68606]) ).
fof(f68928,plain,
( r1_lattice2(u1_struct_0(sK353),u1_lattices(k1_lattice2(sK353)),u1_lattices(sK353))
| v3_struct_0(k1_lattice2(sK353))
| ~ v10_lattices(k1_lattice2(sK353))
| ~ l3_lattices(k1_lattice2(sK353)) ),
inference(forward_demodulation,[],[f68706,f68598]) ).
fof(f68986,plain,
( r1_lattice2(u1_struct_0(sK353),u1_lattices(sK353),u2_lattices(sK353))
| v3_struct_0(k1_lattice2(sK353))
| ~ v10_lattices(k1_lattice2(sK353))
| ~ l3_lattices(k1_lattice2(sK353)) ),
inference(forward_demodulation,[],[f68927,f68598]) ).
fof(f68987,plain,
( r1_lattice2(u1_struct_0(sK353),u2_lattices(sK353),u1_lattices(sK353))
| v3_struct_0(k1_lattice2(sK353))
| ~ v10_lattices(k1_lattice2(sK353))
| ~ l3_lattices(k1_lattice2(sK353)) ),
inference(forward_demodulation,[],[f68928,f68606]) ).
fof(f69002,definition,
( spl2453_98
<=> r1_lattice2(u1_struct_0(sK353),u2_lattices(sK353),u1_lattices(sK353)) ),
introduced(definition,[new_symbols(definition,[spl2453_98])],[avatar_definition]) ).
fof(f69004,plain,
( r1_lattice2(u1_struct_0(sK353),u2_lattices(sK353),u1_lattices(sK353))
| ~ spl2453_98 ),
inference(avatar_component_clause,[],[f69002]) ).
fof(f69007,definition,
( spl2453_99
<=> r1_lattice2(u1_struct_0(sK353),u1_lattices(sK353),u2_lattices(sK353)) ),
introduced(definition,[new_symbols(definition,[spl2453_99])],[avatar_definition]) ).
fof(f69013,plain,
( ~ spl2453_83
| ~ spl2453_84
| spl2453_74
| spl2453_99 ),
inference(avatar_split_clause,[],[f68986,f69007,f68723,f68912,f68908]) ).
fof(f69014,plain,
( ~ spl2453_83
| ~ spl2453_84
| spl2453_74
| spl2453_98 ),
inference(avatar_split_clause,[],[f68987,f69002,f68723,f68912,f68908]) ).
fof(f69015,plain,
! [X0,X1] :
( ~ r1_lattice2(X0,X1,u2_lattices(sK353))
| ~ v1_funct_1(sK355)
| r1_lattice2(sK354,k1_realset1(X1,sK354),sK355)
| ~ m2_relset_1(sK355,k2_zfmisc_1(sK354,sK354),sK354)
| ~ v1_funct_1(k1_realset1(X1,sK354))
| ~ v1_funct_2(k1_realset1(X1,sK354),k2_zfmisc_1(sK354,sK354),sK354)
| ~ m2_relset_1(k1_realset1(X1,sK354),k2_zfmisc_1(sK354,sK354),sK354)
| ~ v1_funct_1(u2_lattices(sK353))
| ~ v1_funct_2(u2_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(u2_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| v1_xboole_0(sK354)
| ~ m1_subset_1(sK354,k1_zfmisc_1(X0)) ),
inference(forward_subsumption_resolution,[],[f68569,f48785]) ).
fof(f69017,plain,
! [X0,X1] :
( ~ r1_lattice2(X0,X1,u1_lattices(sK353))
| ~ v1_funct_1(sK356)
| r1_lattice2(sK354,k1_realset1(X1,sK354),sK356)
| ~ m2_relset_1(sK356,k2_zfmisc_1(sK354,sK354),sK354)
| ~ v1_funct_1(k1_realset1(X1,sK354))
| ~ v1_funct_2(k1_realset1(X1,sK354),k2_zfmisc_1(sK354,sK354),sK354)
| ~ m2_relset_1(k1_realset1(X1,sK354),k2_zfmisc_1(sK354,sK354),sK354)
| ~ v1_funct_1(u1_lattices(sK353))
| ~ v1_funct_2(u1_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(u1_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| v1_xboole_0(sK354)
| ~ m1_subset_1(sK354,k1_zfmisc_1(X0)) ),
inference(forward_subsumption_resolution,[],[f68572,f48788]) ).
fof(f69025,plain,
! [X2,X0,X1] :
( ~ v2_binop_1(u1_lattices(X0),X1)
| v2_binop_1(k1_realset1(u1_lattices(X0),X2),X2)
| ~ m2_relset_1(k1_realset1(u1_lattices(X0),X2),k2_zfmisc_1(X2,X2),X2)
| ~ v1_funct_1(u1_lattices(X0))
| ~ v1_funct_2(u1_lattices(X0),k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(u1_lattices(X0),k2_zfmisc_1(X1,X1),X1)
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(X1))
| ~ m2_lattice4(X2,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f68589,f49047]) ).
fof(f69026,plain,
! [X2,X0,X1] :
( ~ v2_binop_1(u2_lattices(X0),X1)
| v2_binop_1(k1_realset1(u2_lattices(X0),X2),X2)
| ~ m2_relset_1(k1_realset1(u2_lattices(X0),X2),k2_zfmisc_1(X2,X2),X2)
| ~ v1_funct_1(u2_lattices(X0))
| ~ v1_funct_2(u2_lattices(X0),k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(u2_lattices(X0),k2_zfmisc_1(X1,X1),X1)
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(X1))
| ~ m2_lattice4(X2,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f68590,f49050]) ).
fof(f69029,plain,
! [X2,X0,X1] :
( ~ v1_binop_1(u1_lattices(X0),X1)
| v1_binop_1(k1_realset1(u1_lattices(X0),X2),X2)
| ~ m2_relset_1(k1_realset1(u1_lattices(X0),X2),k2_zfmisc_1(X2,X2),X2)
| ~ v1_funct_1(u1_lattices(X0))
| ~ v1_funct_2(u1_lattices(X0),k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(u1_lattices(X0),k2_zfmisc_1(X1,X1),X1)
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(X1))
| ~ m2_lattice4(X2,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f68595,f49047]) ).
fof(f69030,plain,
! [X2,X0,X1] :
( ~ v1_binop_1(u2_lattices(X0),X1)
| v1_binop_1(k1_realset1(u2_lattices(X0),X2),X2)
| ~ m2_relset_1(k1_realset1(u2_lattices(X0),X2),k2_zfmisc_1(X2,X2),X2)
| ~ v1_funct_1(u2_lattices(X0))
| ~ v1_funct_2(u2_lattices(X0),k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(u2_lattices(X0),k2_zfmisc_1(X1,X1),X1)
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(X1))
| ~ m2_lattice4(X2,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f68596,f49050]) ).
fof(f69058,plain,
! [X0,X1] :
( ~ r1_lattice2(X0,X1,u2_lattices(sK353))
| r1_lattice2(sK354,k1_realset1(X1,sK354),sK355)
| ~ m2_relset_1(sK355,k2_zfmisc_1(sK354,sK354),sK354)
| ~ v1_funct_1(k1_realset1(X1,sK354))
| ~ v1_funct_2(k1_realset1(X1,sK354),k2_zfmisc_1(sK354,sK354),sK354)
| ~ m2_relset_1(k1_realset1(X1,sK354),k2_zfmisc_1(sK354,sK354),sK354)
| ~ v1_funct_1(u2_lattices(sK353))
| ~ v1_funct_2(u2_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(u2_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| v1_xboole_0(sK354)
| ~ m1_subset_1(sK354,k1_zfmisc_1(X0)) ),
inference(forward_subsumption_resolution,[],[f69015,f48786]) ).
fof(f69060,plain,
! [X0,X1] :
( ~ r1_lattice2(X0,X1,u1_lattices(sK353))
| r1_lattice2(sK354,k1_realset1(X1,sK354),sK356)
| ~ m2_relset_1(sK356,k2_zfmisc_1(sK354,sK354),sK354)
| ~ v1_funct_1(k1_realset1(X1,sK354))
| ~ v1_funct_2(k1_realset1(X1,sK354),k2_zfmisc_1(sK354,sK354),sK354)
| ~ m2_relset_1(k1_realset1(X1,sK354),k2_zfmisc_1(sK354,sK354),sK354)
| ~ v1_funct_1(u1_lattices(sK353))
| ~ v1_funct_2(u1_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(u1_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| v1_xboole_0(sK354)
| ~ m1_subset_1(sK354,k1_zfmisc_1(X0)) ),
inference(forward_subsumption_resolution,[],[f69017,f48789]) ).
fof(f69068,plain,
! [X2,X0,X1] :
( ~ v1_funct_2(u1_lattices(X0),k2_zfmisc_1(X1,X1),X1)
| v2_binop_1(k1_realset1(u1_lattices(X0),X2),X2)
| ~ v1_funct_1(u1_lattices(X0))
| ~ v2_binop_1(u1_lattices(X0),X1)
| ~ m2_relset_1(u1_lattices(X0),k2_zfmisc_1(X1,X1),X1)
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(X1))
| ~ m2_lattice4(X2,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f69025,f49045]) ).
fof(f69069,plain,
! [X2,X0,X1] :
( ~ v1_funct_2(u2_lattices(X0),k2_zfmisc_1(X1,X1),X1)
| v2_binop_1(k1_realset1(u2_lattices(X0),X2),X2)
| ~ v1_funct_1(u2_lattices(X0))
| ~ v2_binop_1(u2_lattices(X0),X1)
| ~ m2_relset_1(u2_lattices(X0),k2_zfmisc_1(X1,X1),X1)
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(X1))
| ~ m2_lattice4(X2,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f69026,f49048]) ).
fof(f69072,plain,
! [X2,X0,X1] :
( ~ v1_funct_2(u1_lattices(X0),k2_zfmisc_1(X1,X1),X1)
| v1_binop_1(k1_realset1(u1_lattices(X0),X2),X2)
| ~ v1_funct_1(u1_lattices(X0))
| ~ v1_binop_1(u1_lattices(X0),X1)
| ~ m2_relset_1(u1_lattices(X0),k2_zfmisc_1(X1,X1),X1)
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(X1))
| ~ m2_lattice4(X2,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f69029,f49045]) ).
fof(f69073,plain,
! [X2,X0,X1] :
( ~ v1_funct_2(u2_lattices(X0),k2_zfmisc_1(X1,X1),X1)
| v1_binop_1(k1_realset1(u2_lattices(X0),X2),X2)
| ~ v1_funct_1(u2_lattices(X0))
| ~ v1_binop_1(u2_lattices(X0),X1)
| ~ m2_relset_1(u2_lattices(X0),k2_zfmisc_1(X1,X1),X1)
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(X1))
| ~ m2_lattice4(X2,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f69030,f49048]) ).
fof(f69100,plain,
! [X0,X1] :
( ~ r1_lattice2(X0,X1,u2_lattices(sK353))
| r1_lattice2(sK354,k1_realset1(X1,sK354),sK355)
| ~ v1_funct_1(k1_realset1(X1,sK354))
| ~ v1_funct_2(k1_realset1(X1,sK354),k2_zfmisc_1(sK354,sK354),sK354)
| ~ m2_relset_1(k1_realset1(X1,sK354),k2_zfmisc_1(sK354,sK354),sK354)
| ~ v1_funct_1(u2_lattices(sK353))
| ~ v1_funct_2(u2_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(u2_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| v1_xboole_0(sK354)
| ~ m1_subset_1(sK354,k1_zfmisc_1(X0)) ),
inference(forward_subsumption_resolution,[],[f69058,f48784]) ).
fof(f69102,plain,
! [X0,X1] :
( ~ r1_lattice2(X0,X1,u1_lattices(sK353))
| r1_lattice2(sK354,k1_realset1(X1,sK354),sK356)
| ~ v1_funct_1(k1_realset1(X1,sK354))
| ~ v1_funct_2(k1_realset1(X1,sK354),k2_zfmisc_1(sK354,sK354),sK354)
| ~ m2_relset_1(k1_realset1(X1,sK354),k2_zfmisc_1(sK354,sK354),sK354)
| ~ v1_funct_1(u1_lattices(sK353))
| ~ v1_funct_2(u1_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(u1_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| v1_xboole_0(sK354)
| ~ m1_subset_1(sK354,k1_zfmisc_1(X0)) ),
inference(forward_subsumption_resolution,[],[f69060,f48787]) ).
fof(f69126,plain,
! [X0,X1] :
( ~ r1_lattice2(X0,X1,u2_lattices(sK353))
| r1_lattice2(sK354,k1_realset1(X1,sK354),sK355)
| ~ v1_funct_1(k1_realset1(X1,sK354))
| ~ v1_funct_2(k1_realset1(X1,sK354),k2_zfmisc_1(sK354,sK354),sK354)
| ~ m2_relset_1(k1_realset1(X1,sK354),k2_zfmisc_1(sK354,sK354),sK354)
| ~ v1_funct_1(u2_lattices(sK353))
| ~ v1_funct_2(u2_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(u2_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m1_subset_1(sK354,k1_zfmisc_1(X0)) ),
inference(forward_subsumption_resolution,[],[f69100,f48783]) ).
fof(f69128,plain,
! [X0,X1] :
( ~ r1_lattice2(X0,X1,u1_lattices(sK353))
| r1_lattice2(sK354,k1_realset1(X1,sK354),sK356)
| ~ v1_funct_1(k1_realset1(X1,sK354))
| ~ v1_funct_2(k1_realset1(X1,sK354),k2_zfmisc_1(sK354,sK354),sK354)
| ~ m2_relset_1(k1_realset1(X1,sK354),k2_zfmisc_1(sK354,sK354),sK354)
| ~ v1_funct_1(u1_lattices(sK353))
| ~ v1_funct_2(u1_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(u1_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m1_subset_1(sK354,k1_zfmisc_1(X0)) ),
inference(forward_subsumption_resolution,[],[f69102,f48783]) ).
fof(f69141,definition,
( spl2453_100
<=> v1_funct_1(u2_lattices(sK353)) ),
introduced(definition,[new_symbols(definition,[spl2453_100])],[avatar_definition]) ).
fof(f69142,plain,
( v1_funct_1(u2_lattices(sK353))
| ~ spl2453_100 ),
inference(avatar_component_clause,[],[f69141]) ).
fof(f69143,plain,
( ~ v1_funct_1(u2_lattices(sK353))
| spl2453_100 ),
inference(avatar_component_clause,[],[f69141]) ).
fof(f69145,definition,
( spl2453_101
<=> ! [X0,X1] :
( ~ r1_lattice2(X0,X1,u2_lattices(sK353))
| ~ m1_subset_1(sK354,k1_zfmisc_1(X0))
| ~ m2_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X1)
| ~ m2_relset_1(u2_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(u2_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(k1_realset1(X1,sK354),k2_zfmisc_1(sK354,sK354),sK354)
| ~ v1_funct_2(k1_realset1(X1,sK354),k2_zfmisc_1(sK354,sK354),sK354)
| ~ v1_funct_1(k1_realset1(X1,sK354))
| r1_lattice2(sK354,k1_realset1(X1,sK354),sK355) ) ),
introduced(definition,[new_symbols(definition,[spl2453_101])],[avatar_definition]) ).
fof(f69146,plain,
( ! [X0,X1] :
( ~ v1_funct_2(k1_realset1(X1,sK354),k2_zfmisc_1(sK354,sK354),sK354)
| ~ m1_subset_1(sK354,k1_zfmisc_1(X0))
| ~ m2_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X1)
| ~ m2_relset_1(u2_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(u2_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(k1_realset1(X1,sK354),k2_zfmisc_1(sK354,sK354),sK354)
| ~ r1_lattice2(X0,X1,u2_lattices(sK353))
| ~ v1_funct_1(k1_realset1(X1,sK354))
| r1_lattice2(sK354,k1_realset1(X1,sK354),sK355) )
| ~ spl2453_101 ),
inference(avatar_component_clause,[],[f69145]) ).
fof(f69147,plain,
( ~ spl2453_100
| spl2453_101 ),
inference(avatar_split_clause,[],[f69126,f69145,f69141]) ).
fof(f69153,definition,
( spl2453_103
<=> v1_funct_1(u1_lattices(sK353)) ),
introduced(definition,[new_symbols(definition,[spl2453_103])],[avatar_definition]) ).
fof(f69154,plain,
( v1_funct_1(u1_lattices(sK353))
| ~ spl2453_103 ),
inference(avatar_component_clause,[],[f69153]) ).
fof(f69155,plain,
( ~ v1_funct_1(u1_lattices(sK353))
| spl2453_103 ),
inference(avatar_component_clause,[],[f69153]) ).
fof(f69157,definition,
( spl2453_104
<=> ! [X0,X1] :
( ~ r1_lattice2(X0,X1,u1_lattices(sK353))
| ~ m1_subset_1(sK354,k1_zfmisc_1(X0))
| ~ m2_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X1)
| ~ m2_relset_1(u1_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(u1_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(k1_realset1(X1,sK354),k2_zfmisc_1(sK354,sK354),sK354)
| ~ v1_funct_2(k1_realset1(X1,sK354),k2_zfmisc_1(sK354,sK354),sK354)
| ~ v1_funct_1(k1_realset1(X1,sK354))
| r1_lattice2(sK354,k1_realset1(X1,sK354),sK356) ) ),
introduced(definition,[new_symbols(definition,[spl2453_104])],[avatar_definition]) ).
fof(f69158,plain,
( ! [X0,X1] :
( ~ v1_funct_2(k1_realset1(X1,sK354),k2_zfmisc_1(sK354,sK354),sK354)
| ~ m1_subset_1(sK354,k1_zfmisc_1(X0))
| ~ m2_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X1)
| ~ m2_relset_1(u1_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(u1_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(k1_realset1(X1,sK354),k2_zfmisc_1(sK354,sK354),sK354)
| ~ r1_lattice2(X0,X1,u1_lattices(sK353))
| ~ v1_funct_1(k1_realset1(X1,sK354))
| r1_lattice2(sK354,k1_realset1(X1,sK354),sK356) )
| ~ spl2453_104 ),
inference(avatar_component_clause,[],[f69157]) ).
fof(f69159,plain,
( ~ spl2453_103
| spl2453_104 ),
inference(avatar_split_clause,[],[f69128,f69157,f69153]) ).
fof(f69216,plain,
( ~ l1_lattices(sK353)
| spl2453_103 ),
inference(resolution,[],[f69155,f49204]) ).
fof(f69217,plain,
( $false
| spl2453_103 ),
inference(forward_subsumption_resolution,[],[f69216,f68833]) ).
fof(f69218,plain,
spl2453_103,
inference(avatar_contradiction_clause,[],[f69217]) ).
fof(f69219,plain,
( ~ l2_lattices(sK353)
| spl2453_100 ),
inference(resolution,[],[f69143,f49177]) ).
fof(f69220,plain,
( $false
| spl2453_100 ),
inference(forward_subsumption_resolution,[],[f69219,f68827]) ).
fof(f69221,plain,
spl2453_100,
inference(avatar_contradiction_clause,[],[f69220]) ).
fof(f69224,plain,
( ! [X0] :
( ~ v1_funct_2(sK355,k2_zfmisc_1(sK354,sK354),sK354)
| ~ m1_subset_1(sK354,k1_zfmisc_1(X0))
| ~ m2_relset_1(u2_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(u2_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(u2_lattices(sK353))
| ~ m2_relset_1(u1_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(u1_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(sK355,k2_zfmisc_1(sK354,sK354),sK354)
| ~ r1_lattice2(X0,u2_lattices(sK353),u1_lattices(sK353))
| ~ v1_funct_1(sK355)
| r1_lattice2(sK354,sK355,sK356) )
| ~ spl2453_104 ),
inference(superposition,[],[f69158,f48791]) ).
fof(f69228,plain,
( ! [X0] :
( ~ m1_subset_1(sK354,k1_zfmisc_1(X0))
| ~ m2_relset_1(u2_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(u2_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(u2_lattices(sK353))
| ~ m2_relset_1(u1_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(u1_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(sK355,k2_zfmisc_1(sK354,sK354),sK354)
| ~ r1_lattice2(X0,u2_lattices(sK353),u1_lattices(sK353))
| ~ v1_funct_1(sK355)
| r1_lattice2(sK354,sK355,sK356) )
| ~ spl2453_104 ),
inference(forward_subsumption_resolution,[],[f69224,f48785]) ).
fof(f69232,plain,
( ! [X0] :
( ~ m1_subset_1(sK354,k1_zfmisc_1(X0))
| ~ m2_relset_1(u2_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(u2_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(u1_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(u1_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(sK355,k2_zfmisc_1(sK354,sK354),sK354)
| ~ r1_lattice2(X0,u2_lattices(sK353),u1_lattices(sK353))
| ~ v1_funct_1(sK355)
| r1_lattice2(sK354,sK355,sK356) )
| ~ spl2453_100
| ~ spl2453_104 ),
inference(forward_subsumption_resolution,[],[f69228,f69142]) ).
fof(f69236,plain,
( ! [X0] :
( ~ m1_subset_1(sK354,k1_zfmisc_1(X0))
| ~ m2_relset_1(u2_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(u2_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(u1_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(u1_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ r1_lattice2(X0,u2_lattices(sK353),u1_lattices(sK353))
| ~ v1_funct_1(sK355)
| r1_lattice2(sK354,sK355,sK356) )
| ~ spl2453_100
| ~ spl2453_104 ),
inference(forward_subsumption_resolution,[],[f69232,f48784]) ).
fof(f69240,plain,
( ! [X0] :
( ~ m1_subset_1(sK354,k1_zfmisc_1(X0))
| ~ m2_relset_1(u2_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(u2_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(u1_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(u1_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ r1_lattice2(X0,u2_lattices(sK353),u1_lattices(sK353))
| r1_lattice2(sK354,sK355,sK356) )
| ~ spl2453_100
| ~ spl2453_104 ),
inference(forward_subsumption_resolution,[],[f69236,f48786]) ).
fof(f69250,definition,
( spl2453_120
<=> ! [X0] :
( ~ m1_subset_1(sK354,k1_zfmisc_1(X0))
| ~ r1_lattice2(X0,u2_lattices(sK353),u1_lattices(sK353))
| ~ v1_funct_2(u1_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(u1_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(u2_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(u2_lattices(sK353),k2_zfmisc_1(X0,X0),X0) ) ),
introduced(definition,[new_symbols(definition,[spl2453_120])],[avatar_definition]) ).
fof(f69251,plain,
( ! [X0] :
( ~ v1_funct_2(u1_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ r1_lattice2(X0,u2_lattices(sK353),u1_lattices(sK353))
| ~ m1_subset_1(sK354,k1_zfmisc_1(X0))
| ~ m2_relset_1(u1_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(u2_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(u2_lattices(sK353),k2_zfmisc_1(X0,X0),X0) )
| ~ spl2453_120 ),
inference(avatar_component_clause,[],[f69250]) ).
fof(f69252,plain,
( spl2453_59
| spl2453_120
| ~ spl2453_100
| ~ spl2453_104 ),
inference(avatar_split_clause,[],[f69240,f69157,f69141,f69250,f67525]) ).
fof(f69256,plain,
( ! [X0] :
( ~ v1_funct_2(sK356,k2_zfmisc_1(sK354,sK354),sK354)
| ~ m1_subset_1(sK354,k1_zfmisc_1(X0))
| ~ m2_relset_1(u1_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(u1_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(u1_lattices(sK353))
| ~ m2_relset_1(u2_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(u2_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(sK356,k2_zfmisc_1(sK354,sK354),sK354)
| ~ r1_lattice2(X0,u1_lattices(sK353),u2_lattices(sK353))
| ~ v1_funct_1(sK356)
| r1_lattice2(sK354,sK356,sK355) )
| ~ spl2453_101 ),
inference(superposition,[],[f69146,f48790]) ).
fof(f69258,plain,
( ! [X0] :
( ~ m1_subset_1(sK354,k1_zfmisc_1(X0))
| ~ m2_relset_1(u1_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(u1_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(u1_lattices(sK353))
| ~ m2_relset_1(u2_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(u2_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(sK356,k2_zfmisc_1(sK354,sK354),sK354)
| ~ r1_lattice2(X0,u1_lattices(sK353),u2_lattices(sK353))
| ~ v1_funct_1(sK356)
| r1_lattice2(sK354,sK356,sK355) )
| ~ spl2453_101 ),
inference(forward_subsumption_resolution,[],[f69256,f48788]) ).
fof(f69262,plain,
( ! [X0] :
( ~ m1_subset_1(sK354,k1_zfmisc_1(X0))
| ~ m2_relset_1(u1_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(u1_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(u2_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(u2_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(sK356,k2_zfmisc_1(sK354,sK354),sK354)
| ~ r1_lattice2(X0,u1_lattices(sK353),u2_lattices(sK353))
| ~ v1_funct_1(sK356)
| r1_lattice2(sK354,sK356,sK355) )
| ~ spl2453_101
| ~ spl2453_103 ),
inference(forward_subsumption_resolution,[],[f69258,f69154]) ).
fof(f69266,plain,
( ! [X0] :
( ~ m1_subset_1(sK354,k1_zfmisc_1(X0))
| ~ m2_relset_1(u1_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(u1_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(u2_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(u2_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ r1_lattice2(X0,u1_lattices(sK353),u2_lattices(sK353))
| ~ v1_funct_1(sK356)
| r1_lattice2(sK354,sK356,sK355) )
| ~ spl2453_101
| ~ spl2453_103 ),
inference(forward_subsumption_resolution,[],[f69262,f48787]) ).
fof(f69270,plain,
( ! [X0] :
( ~ m1_subset_1(sK354,k1_zfmisc_1(X0))
| ~ m2_relset_1(u1_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(u1_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(u2_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(u2_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ r1_lattice2(X0,u1_lattices(sK353),u2_lattices(sK353))
| r1_lattice2(sK354,sK356,sK355) )
| ~ spl2453_101
| ~ spl2453_103 ),
inference(forward_subsumption_resolution,[],[f69266,f48789]) ).
fof(f69272,plain,
( ! [X0] :
( ~ v1_funct_2(u1_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(u1_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ m1_subset_1(sK354,k1_zfmisc_1(X0))
| ~ m2_relset_1(u2_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(u2_lattices(sK353),k2_zfmisc_1(X0,X0),X0)
| ~ r1_lattice2(X0,u1_lattices(sK353),u2_lattices(sK353)) )
| spl2453_58
| ~ spl2453_101
| ~ spl2453_103 ),
inference(forward_subsumption_resolution,[],[f69270,f67523]) ).
fof(f69281,plain,
( ~ m2_relset_1(u1_lattices(sK353),k2_zfmisc_1(u1_struct_0(sK353),u1_struct_0(sK353)),u1_struct_0(sK353))
| ~ m1_subset_1(sK354,k1_zfmisc_1(u1_struct_0(sK353)))
| ~ m2_relset_1(u2_lattices(sK353),k2_zfmisc_1(u1_struct_0(sK353),u1_struct_0(sK353)),u1_struct_0(sK353))
| ~ v1_funct_2(u2_lattices(sK353),k2_zfmisc_1(u1_struct_0(sK353),u1_struct_0(sK353)),u1_struct_0(sK353))
| ~ r1_lattice2(u1_struct_0(sK353),u1_lattices(sK353),u2_lattices(sK353))
| ~ l1_lattices(sK353)
| spl2453_58
| ~ spl2453_101
| ~ spl2453_103 ),
inference(resolution,[],[f69272,f49203]) ).
fof(f69282,plain,
( ~ m1_subset_1(sK354,k1_zfmisc_1(u1_struct_0(sK353)))
| ~ m2_relset_1(u2_lattices(sK353),k2_zfmisc_1(u1_struct_0(sK353),u1_struct_0(sK353)),u1_struct_0(sK353))
| ~ v1_funct_2(u2_lattices(sK353),k2_zfmisc_1(u1_struct_0(sK353),u1_struct_0(sK353)),u1_struct_0(sK353))
| ~ r1_lattice2(u1_struct_0(sK353),u1_lattices(sK353),u2_lattices(sK353))
| ~ l1_lattices(sK353)
| spl2453_58
| ~ spl2453_101
| ~ spl2453_103 ),
inference(forward_subsumption_resolution,[],[f69281,f49202]) ).
fof(f69283,plain,
( ~ m1_subset_1(sK354,k1_zfmisc_1(u1_struct_0(sK353)))
| ~ m2_relset_1(u2_lattices(sK353),k2_zfmisc_1(u1_struct_0(sK353),u1_struct_0(sK353)),u1_struct_0(sK353))
| ~ v1_funct_2(u2_lattices(sK353),k2_zfmisc_1(u1_struct_0(sK353),u1_struct_0(sK353)),u1_struct_0(sK353))
| ~ r1_lattice2(u1_struct_0(sK353),u1_lattices(sK353),u2_lattices(sK353))
| spl2453_58
| ~ spl2453_101
| ~ spl2453_103 ),
inference(forward_subsumption_resolution,[],[f69282,f68833]) ).
fof(f69285,definition,
( spl2453_123
<=> v1_funct_2(u2_lattices(sK353),k2_zfmisc_1(u1_struct_0(sK353),u1_struct_0(sK353)),u1_struct_0(sK353)) ),
introduced(definition,[new_symbols(definition,[spl2453_123])],[avatar_definition]) ).
fof(f69286,plain,
( v1_funct_2(u2_lattices(sK353),k2_zfmisc_1(u1_struct_0(sK353),u1_struct_0(sK353)),u1_struct_0(sK353))
| ~ spl2453_123 ),
inference(avatar_component_clause,[],[f69285]) ).
fof(f69289,definition,
( spl2453_124
<=> m2_relset_1(u2_lattices(sK353),k2_zfmisc_1(u1_struct_0(sK353),u1_struct_0(sK353)),u1_struct_0(sK353)) ),
introduced(definition,[new_symbols(definition,[spl2453_124])],[avatar_definition]) ).
fof(f69290,plain,
( m2_relset_1(u2_lattices(sK353),k2_zfmisc_1(u1_struct_0(sK353),u1_struct_0(sK353)),u1_struct_0(sK353))
| ~ spl2453_124 ),
inference(avatar_component_clause,[],[f69289]) ).
fof(f69293,definition,
( spl2453_125
<=> m1_subset_1(sK354,k1_zfmisc_1(u1_struct_0(sK353))) ),
introduced(definition,[new_symbols(definition,[spl2453_125])],[avatar_definition]) ).
fof(f69294,plain,
( m1_subset_1(sK354,k1_zfmisc_1(u1_struct_0(sK353)))
| ~ spl2453_125 ),
inference(avatar_component_clause,[],[f69293]) ).
fof(f69295,plain,
( ~ m1_subset_1(sK354,k1_zfmisc_1(u1_struct_0(sK353)))
| spl2453_125 ),
inference(avatar_component_clause,[],[f69293]) ).
fof(f69296,plain,
( ~ spl2453_99
| ~ spl2453_123
| ~ spl2453_124
| ~ spl2453_125
| spl2453_58
| ~ spl2453_101
| ~ spl2453_103 ),
inference(avatar_split_clause,[],[f69283,f69153,f69145,f67521,f69293,f69289,f69285,f69007]) ).
fof(f69303,plain,
! [X0,X1] :
( v2_binop_1(k1_realset1(u1_lattices(X0),X1),X1)
| ~ v1_funct_1(u1_lattices(X0))
| ~ v2_binop_1(u1_lattices(X0),u1_struct_0(X0))
| ~ m2_relset_1(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ l1_lattices(X0) ),
inference(resolution,[],[f69068,f49203]) ).
fof(f69305,plain,
! [X0,X1] :
( v2_binop_1(k1_realset1(u1_lattices(X0),X1),X1)
| ~ v2_binop_1(u1_lattices(X0),u1_struct_0(X0))
| ~ m2_relset_1(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ l1_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f69303,f49204]) ).
fof(f69306,plain,
! [X0,X1] :
( v2_binop_1(k1_realset1(u1_lattices(X0),X1),X1)
| ~ v2_binop_1(u1_lattices(X0),u1_struct_0(X0))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ l1_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f69305,f49202]) ).
fof(f69307,plain,
! [X0,X1] :
( v2_binop_1(k1_realset1(u1_lattices(X0),X1),X1)
| ~ v2_binop_1(u1_lattices(X0),u1_struct_0(X0))
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ l1_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f69306,f49117]) ).
fof(f69308,plain,
! [X0,X1] :
( ~ v2_binop_1(u1_lattices(X0),u1_struct_0(X0))
| v2_binop_1(k1_realset1(u1_lattices(X0),X1),X1)
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f69307,f52511]) ).
fof(f69309,plain,
! [X0,X1] :
( v2_binop_1(k1_realset1(u1_lattices(X0),X1),X1)
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v3_struct_0(X0)
| ~ v7_lattices(X0)
| ~ l1_lattices(X0) ),
inference(resolution,[],[f69308,f49193]) ).
fof(f69312,plain,
! [X0,X1] :
( v2_binop_1(k1_realset1(u1_lattices(X0),X1),X1)
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ v7_lattices(X0)
| ~ l1_lattices(X0) ),
inference(duplicate_literal_removal,[],[f69309]) ).
fof(f69313,plain,
! [X0,X1] :
( v2_binop_1(k1_realset1(u1_lattices(X0),X1),X1)
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ l1_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f69312,f52681]) ).
fof(f69314,plain,
! [X0,X1] :
( v2_binop_1(k1_realset1(u1_lattices(X0),X1),X1)
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f69313,f52511]) ).
fof(f69316,plain,
( v2_binop_1(sK356,sK354)
| v1_xboole_0(sK354)
| ~ m2_lattice4(sK354,sK353)
| v3_struct_0(sK353)
| ~ v10_lattices(sK353)
| ~ l3_lattices(sK353) ),
inference(superposition,[],[f69314,f48790]) ).
fof(f69319,plain,
! [X0,X1] :
( v1_binop_1(k1_realset1(u1_lattices(X0),X1),X1)
| ~ v1_funct_1(u1_lattices(X0))
| ~ v1_binop_1(u1_lattices(X0),u1_struct_0(X0))
| ~ m2_relset_1(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ l1_lattices(X0) ),
inference(resolution,[],[f69072,f49203]) ).
fof(f69321,plain,
! [X0,X1] :
( v1_binop_1(k1_realset1(u1_lattices(X0),X1),X1)
| ~ v1_binop_1(u1_lattices(X0),u1_struct_0(X0))
| ~ m2_relset_1(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ l1_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f69319,f49204]) ).
fof(f69322,plain,
! [X0,X1] :
( v1_binop_1(k1_realset1(u1_lattices(X0),X1),X1)
| ~ v1_binop_1(u1_lattices(X0),u1_struct_0(X0))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ l1_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f69321,f49202]) ).
fof(f69323,plain,
! [X0,X1] :
( v1_binop_1(k1_realset1(u1_lattices(X0),X1),X1)
| ~ v1_binop_1(u1_lattices(X0),u1_struct_0(X0))
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ l1_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f69322,f49117]) ).
fof(f69324,plain,
! [X0,X1] :
( ~ v1_binop_1(u1_lattices(X0),u1_struct_0(X0))
| v1_binop_1(k1_realset1(u1_lattices(X0),X1),X1)
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f69323,f52511]) ).
fof(f69325,plain,
! [X0,X1] :
( v1_binop_1(k1_realset1(u1_lattices(X0),X1),X1)
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v3_struct_0(X0)
| ~ v6_lattices(X0)
| ~ l1_lattices(X0) ),
inference(resolution,[],[f69324,f49198]) ).
fof(f69328,plain,
! [X0,X1] :
( v1_binop_1(k1_realset1(u1_lattices(X0),X1),X1)
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ v6_lattices(X0)
| ~ l1_lattices(X0) ),
inference(duplicate_literal_removal,[],[f69325]) ).
fof(f69329,plain,
! [X0,X1] :
( v1_binop_1(k1_realset1(u1_lattices(X0),X1),X1)
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ l1_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f69328,f52682]) ).
fof(f69330,plain,
! [X0,X1] :
( v1_binop_1(k1_realset1(u1_lattices(X0),X1),X1)
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f69329,f52511]) ).
fof(f69332,plain,
( v1_binop_1(sK356,sK354)
| v1_xboole_0(sK354)
| ~ m2_lattice4(sK354,sK353)
| v3_struct_0(sK353)
| ~ v10_lattices(sK353)
| ~ l3_lattices(sK353) ),
inference(superposition,[],[f69330,f48790]) ).
fof(f69337,plain,
! [X0,X1] :
( v2_binop_1(k1_realset1(u2_lattices(X0),X1),X1)
| ~ v1_funct_1(u2_lattices(X0))
| ~ v2_binop_1(u2_lattices(X0),u1_struct_0(X0))
| ~ m2_relset_1(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ l2_lattices(X0) ),
inference(resolution,[],[f69069,f49176]) ).
fof(f69339,plain,
! [X0,X1] :
( v2_binop_1(k1_realset1(u2_lattices(X0),X1),X1)
| ~ v2_binop_1(u2_lattices(X0),u1_struct_0(X0))
| ~ m2_relset_1(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ l2_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f69337,f49177]) ).
fof(f69340,plain,
! [X0,X1] :
( v2_binop_1(k1_realset1(u2_lattices(X0),X1),X1)
| ~ v2_binop_1(u2_lattices(X0),u1_struct_0(X0))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ l2_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f69339,f49175]) ).
fof(f69341,plain,
! [X0,X1] :
( v2_binop_1(k1_realset1(u2_lattices(X0),X1),X1)
| ~ v2_binop_1(u2_lattices(X0),u1_struct_0(X0))
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ l2_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f69340,f49117]) ).
fof(f69342,plain,
! [X0,X1] :
( ~ v2_binop_1(u2_lattices(X0),u1_struct_0(X0))
| v2_binop_1(k1_realset1(u2_lattices(X0),X1),X1)
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f69341,f52510]) ).
fof(f69343,plain,
! [X0,X1] :
( v2_binop_1(k1_realset1(u2_lattices(X0),X1),X1)
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v3_struct_0(X0)
| ~ v5_lattices(X0)
| ~ l2_lattices(X0) ),
inference(resolution,[],[f69342,f49166]) ).
fof(f69346,plain,
! [X0,X1] :
( v2_binop_1(k1_realset1(u2_lattices(X0),X1),X1)
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ v5_lattices(X0)
| ~ l2_lattices(X0) ),
inference(duplicate_literal_removal,[],[f69343]) ).
fof(f69347,plain,
! [X0,X1] :
( v2_binop_1(k1_realset1(u2_lattices(X0),X1),X1)
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ l2_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f69346,f52683]) ).
fof(f69348,plain,
! [X0,X1] :
( v2_binop_1(k1_realset1(u2_lattices(X0),X1),X1)
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f69347,f52510]) ).
fof(f69350,plain,
( v2_binop_1(sK355,sK354)
| v1_xboole_0(sK354)
| ~ m2_lattice4(sK354,sK353)
| v3_struct_0(sK353)
| ~ v10_lattices(sK353)
| ~ l3_lattices(sK353) ),
inference(superposition,[],[f69348,f48791]) ).
fof(f69409,plain,
! [X0,X1] :
( v1_binop_1(k1_realset1(u2_lattices(X0),X1),X1)
| ~ v1_funct_1(u2_lattices(X0))
| ~ v1_binop_1(u2_lattices(X0),u1_struct_0(X0))
| ~ m2_relset_1(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ l2_lattices(X0) ),
inference(resolution,[],[f69073,f49176]) ).
fof(f69411,plain,
! [X0,X1] :
( v1_binop_1(k1_realset1(u2_lattices(X0),X1),X1)
| ~ v1_binop_1(u2_lattices(X0),u1_struct_0(X0))
| ~ m2_relset_1(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ l2_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f69409,f49177]) ).
fof(f69412,plain,
! [X0,X1] :
( v1_binop_1(k1_realset1(u2_lattices(X0),X1),X1)
| ~ v1_binop_1(u2_lattices(X0),u1_struct_0(X0))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ l2_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f69411,f49175]) ).
fof(f69413,plain,
! [X0,X1] :
( v1_binop_1(k1_realset1(u2_lattices(X0),X1),X1)
| ~ v1_binop_1(u2_lattices(X0),u1_struct_0(X0))
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ l2_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f69412,f49117]) ).
fof(f69414,plain,
! [X0,X1] :
( ~ v1_binop_1(u2_lattices(X0),u1_struct_0(X0))
| v1_binop_1(k1_realset1(u2_lattices(X0),X1),X1)
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f69413,f52510]) ).
fof(f69415,plain,
! [X0,X1] :
( v1_binop_1(k1_realset1(u2_lattices(X0),X1),X1)
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v3_struct_0(X0)
| ~ v4_lattices(X0)
| ~ l2_lattices(X0) ),
inference(resolution,[],[f69414,f49171]) ).
fof(f69418,plain,
! [X0,X1] :
( v1_binop_1(k1_realset1(u2_lattices(X0),X1),X1)
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ v4_lattices(X0)
| ~ l2_lattices(X0) ),
inference(duplicate_literal_removal,[],[f69415]) ).
fof(f69419,plain,
! [X0,X1] :
( v1_binop_1(k1_realset1(u2_lattices(X0),X1),X1)
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ l2_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f69418,f52684]) ).
fof(f69420,plain,
! [X0,X1] :
( v1_binop_1(k1_realset1(u2_lattices(X0),X1),X1)
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f69419,f52510]) ).
fof(f69422,plain,
( v1_binop_1(sK355,sK354)
| v1_xboole_0(sK354)
| ~ m2_lattice4(sK354,sK353)
| v3_struct_0(sK353)
| ~ v10_lattices(sK353)
| ~ l3_lattices(sK353) ),
inference(superposition,[],[f69420,f48791]) ).
fof(f69423,plain,
( ~ l3_lattices(sK353)
| spl2453_83 ),
inference(resolution,[],[f68910,f52426]) ).
fof(f69424,plain,
( $false
| spl2453_83 ),
inference(forward_subsumption_resolution,[],[f69423,f48779]) ).
fof(f69425,plain,
spl2453_83,
inference(avatar_contradiction_clause,[],[f69424]) ).
fof(f69426,plain,
( l1_lattices(k1_lattice2(sK353))
| ~ spl2453_83 ),
inference(resolution,[],[f68909,f52511]) ).
fof(f69438,plain,
( $false
| spl2453_71
| ~ spl2453_83 ),
inference(forward_subsumption_resolution,[],[f69426,f68681]) ).
fof(f69439,plain,
( spl2453_71
| ~ spl2453_83 ),
inference(avatar_contradiction_clause,[],[f69438]) ).
fof(f69459,plain,
( m2_relset_1(u1_lattices(k1_lattice2(sK353)),k2_zfmisc_1(u1_struct_0(sK353),u1_struct_0(sK353)),u1_struct_0(sK353))
| ~ spl2453_71 ),
inference(forward_subsumption_resolution,[],[f68714,f68680]) ).
fof(f69460,plain,
( v1_funct_2(u1_lattices(k1_lattice2(sK353)),k2_zfmisc_1(u1_struct_0(sK353),u1_struct_0(sK353)),u1_struct_0(sK353))
| ~ spl2453_71 ),
inference(forward_subsumption_resolution,[],[f68735,f68680]) ).
fof(f69466,plain,
( m2_relset_1(u2_lattices(sK353),k2_zfmisc_1(u1_struct_0(sK353),u1_struct_0(sK353)),u1_struct_0(sK353))
| ~ spl2453_71 ),
inference(forward_demodulation,[],[f69459,f68606]) ).
fof(f69467,plain,
( v1_funct_2(u2_lattices(sK353),k2_zfmisc_1(u1_struct_0(sK353),u1_struct_0(sK353)),u1_struct_0(sK353))
| ~ spl2453_71 ),
inference(forward_demodulation,[],[f69460,f68606]) ).
fof(f69472,plain,
( spl2453_124
| ~ spl2453_71 ),
inference(avatar_split_clause,[],[f69466,f68679,f69289]) ).
fof(f69473,plain,
( spl2453_123
| ~ spl2453_71 ),
inference(avatar_split_clause,[],[f69467,f68679,f69285]) ).
fof(f69474,plain,
( v3_struct_0(sK353)
| ~ l3_lattices(sK353)
| ~ spl2453_74 ),
inference(resolution,[],[f68725,f52454]) ).
fof(f69475,plain,
( ~ l3_lattices(sK353)
| ~ spl2453_74 ),
inference(forward_subsumption_resolution,[],[f69474,f48781]) ).
fof(f69476,plain,
( $false
| ~ spl2453_74 ),
inference(forward_subsumption_resolution,[],[f69475,f48779]) ).
fof(f69477,plain,
~ spl2453_74,
inference(avatar_contradiction_clause,[],[f69476]) ).
fof(f69542,plain,
( ~ sP53(sK353)
| spl2453_84 ),
inference(resolution,[],[f68914,f52443]) ).
fof(f69544,plain,
( $false
| spl2453_84 ),
inference(forward_subsumption_resolution,[],[f69542,f68702]) ).
fof(f69545,plain,
spl2453_84,
inference(avatar_contradiction_clause,[],[f69544]) ).
fof(f69650,plain,
( ~ m2_lattice4(sK354,sK353)
| v3_struct_0(sK353)
| ~ v10_lattices(sK353)
| ~ l3_lattices(sK353)
| spl2453_125 ),
inference(resolution,[],[f69295,f49117]) ).
fof(f69651,plain,
( v3_struct_0(sK353)
| ~ v10_lattices(sK353)
| ~ l3_lattices(sK353)
| spl2453_125 ),
inference(forward_subsumption_resolution,[],[f69650,f48782]) ).
fof(f69653,plain,
( ~ v10_lattices(sK353)
| ~ l3_lattices(sK353)
| spl2453_125 ),
inference(forward_subsumption_resolution,[],[f69651,f48781]) ).
fof(f69655,plain,
( ~ l3_lattices(sK353)
| spl2453_125 ),
inference(forward_subsumption_resolution,[],[f69653,f48780]) ).
fof(f69657,plain,
( $false
| spl2453_125 ),
inference(forward_subsumption_resolution,[],[f69655,f48779]) ).
fof(f69658,plain,
spl2453_125,
inference(avatar_contradiction_clause,[],[f69657]) ).
fof(f69659,plain,
( v1_xboole_0(sK354)
| ~ m2_lattice4(sK354,sK353)
| v3_struct_0(sK353)
| ~ v10_lattices(sK353)
| ~ l3_lattices(sK353)
| spl2453_60 ),
inference(forward_subsumption_resolution,[],[f69316,f67531]) ).
fof(f69660,plain,
( ~ m2_lattice4(sK354,sK353)
| v3_struct_0(sK353)
| ~ v10_lattices(sK353)
| ~ l3_lattices(sK353)
| spl2453_60 ),
inference(forward_subsumption_resolution,[],[f69659,f48783]) ).
fof(f69661,plain,
( v3_struct_0(sK353)
| ~ v10_lattices(sK353)
| ~ l3_lattices(sK353)
| spl2453_60 ),
inference(forward_subsumption_resolution,[],[f69660,f48782]) ).
fof(f69662,plain,
( ~ v10_lattices(sK353)
| ~ l3_lattices(sK353)
| spl2453_60 ),
inference(forward_subsumption_resolution,[],[f69661,f48781]) ).
fof(f69663,plain,
( ~ l3_lattices(sK353)
| spl2453_60 ),
inference(forward_subsumption_resolution,[],[f69662,f48780]) ).
fof(f69664,plain,
( $false
| spl2453_60 ),
inference(forward_subsumption_resolution,[],[f69663,f48779]) ).
fof(f69665,plain,
spl2453_60,
inference(avatar_contradiction_clause,[],[f69664]) ).
fof(f69666,plain,
( v1_xboole_0(sK354)
| ~ m2_lattice4(sK354,sK353)
| v3_struct_0(sK353)
| ~ v10_lattices(sK353)
| ~ l3_lattices(sK353)
| spl2453_62 ),
inference(forward_subsumption_resolution,[],[f69350,f67539]) ).
fof(f69667,plain,
( ~ m2_lattice4(sK354,sK353)
| v3_struct_0(sK353)
| ~ v10_lattices(sK353)
| ~ l3_lattices(sK353)
| spl2453_62 ),
inference(forward_subsumption_resolution,[],[f69666,f48783]) ).
fof(f69668,plain,
( v3_struct_0(sK353)
| ~ v10_lattices(sK353)
| ~ l3_lattices(sK353)
| spl2453_62 ),
inference(forward_subsumption_resolution,[],[f69667,f48782]) ).
fof(f69669,plain,
( ~ v10_lattices(sK353)
| ~ l3_lattices(sK353)
| spl2453_62 ),
inference(forward_subsumption_resolution,[],[f69668,f48781]) ).
fof(f69670,plain,
( ~ l3_lattices(sK353)
| spl2453_62 ),
inference(forward_subsumption_resolution,[],[f69669,f48780]) ).
fof(f69671,plain,
( $false
| spl2453_62 ),
inference(forward_subsumption_resolution,[],[f69670,f48779]) ).
fof(f69672,plain,
spl2453_62,
inference(avatar_contradiction_clause,[],[f69671]) ).
fof(f69673,plain,
( v1_xboole_0(sK354)
| ~ m2_lattice4(sK354,sK353)
| v3_struct_0(sK353)
| ~ v10_lattices(sK353)
| ~ l3_lattices(sK353)
| spl2453_61 ),
inference(forward_subsumption_resolution,[],[f69332,f67535]) ).
fof(f69674,plain,
( ~ m2_lattice4(sK354,sK353)
| v3_struct_0(sK353)
| ~ v10_lattices(sK353)
| ~ l3_lattices(sK353)
| spl2453_61 ),
inference(forward_subsumption_resolution,[],[f69673,f48783]) ).
fof(f69675,plain,
( v3_struct_0(sK353)
| ~ v10_lattices(sK353)
| ~ l3_lattices(sK353)
| spl2453_61 ),
inference(forward_subsumption_resolution,[],[f69674,f48782]) ).
fof(f69676,plain,
( ~ v10_lattices(sK353)
| ~ l3_lattices(sK353)
| spl2453_61 ),
inference(forward_subsumption_resolution,[],[f69675,f48781]) ).
fof(f69677,plain,
( ~ l3_lattices(sK353)
| spl2453_61 ),
inference(forward_subsumption_resolution,[],[f69676,f48780]) ).
fof(f69678,plain,
( $false
| spl2453_61 ),
inference(forward_subsumption_resolution,[],[f69677,f48779]) ).
fof(f69679,plain,
spl2453_61,
inference(avatar_contradiction_clause,[],[f69678]) ).
fof(f69680,plain,
( v1_xboole_0(sK354)
| ~ m2_lattice4(sK354,sK353)
| v3_struct_0(sK353)
| ~ v10_lattices(sK353)
| ~ l3_lattices(sK353)
| spl2453_63 ),
inference(forward_subsumption_resolution,[],[f69422,f67543]) ).
fof(f69681,plain,
( ~ m2_lattice4(sK354,sK353)
| v3_struct_0(sK353)
| ~ v10_lattices(sK353)
| ~ l3_lattices(sK353)
| spl2453_63 ),
inference(forward_subsumption_resolution,[],[f69680,f48783]) ).
fof(f69682,plain,
( v3_struct_0(sK353)
| ~ v10_lattices(sK353)
| ~ l3_lattices(sK353)
| spl2453_63 ),
inference(forward_subsumption_resolution,[],[f69681,f48782]) ).
fof(f69683,plain,
( ~ v10_lattices(sK353)
| ~ l3_lattices(sK353)
| spl2453_63 ),
inference(forward_subsumption_resolution,[],[f69682,f48781]) ).
fof(f69684,plain,
( ~ l3_lattices(sK353)
| spl2453_63 ),
inference(forward_subsumption_resolution,[],[f69683,f48780]) ).
fof(f69685,plain,
( $false
| spl2453_63 ),
inference(forward_subsumption_resolution,[],[f69684,f48779]) ).
fof(f69686,plain,
spl2453_63,
inference(avatar_contradiction_clause,[],[f69685]) ).
fof(f69713,plain,
( ~ r1_lattice2(u1_struct_0(sK353),u2_lattices(sK353),u1_lattices(sK353))
| ~ m1_subset_1(sK354,k1_zfmisc_1(u1_struct_0(sK353)))
| ~ m2_relset_1(u1_lattices(sK353),k2_zfmisc_1(u1_struct_0(sK353),u1_struct_0(sK353)),u1_struct_0(sK353))
| ~ v1_funct_2(u2_lattices(sK353),k2_zfmisc_1(u1_struct_0(sK353),u1_struct_0(sK353)),u1_struct_0(sK353))
| ~ m2_relset_1(u2_lattices(sK353),k2_zfmisc_1(u1_struct_0(sK353),u1_struct_0(sK353)),u1_struct_0(sK353))
| ~ l1_lattices(sK353)
| ~ spl2453_120 ),
inference(resolution,[],[f69251,f49203]) ).
fof(f69714,plain,
( ~ m1_subset_1(sK354,k1_zfmisc_1(u1_struct_0(sK353)))
| ~ m2_relset_1(u1_lattices(sK353),k2_zfmisc_1(u1_struct_0(sK353),u1_struct_0(sK353)),u1_struct_0(sK353))
| ~ v1_funct_2(u2_lattices(sK353),k2_zfmisc_1(u1_struct_0(sK353),u1_struct_0(sK353)),u1_struct_0(sK353))
| ~ m2_relset_1(u2_lattices(sK353),k2_zfmisc_1(u1_struct_0(sK353),u1_struct_0(sK353)),u1_struct_0(sK353))
| ~ l1_lattices(sK353)
| ~ spl2453_98
| ~ spl2453_120 ),
inference(forward_subsumption_resolution,[],[f69713,f69004]) ).
fof(f69715,plain,
( ~ m2_relset_1(u1_lattices(sK353),k2_zfmisc_1(u1_struct_0(sK353),u1_struct_0(sK353)),u1_struct_0(sK353))
| ~ v1_funct_2(u2_lattices(sK353),k2_zfmisc_1(u1_struct_0(sK353),u1_struct_0(sK353)),u1_struct_0(sK353))
| ~ m2_relset_1(u2_lattices(sK353),k2_zfmisc_1(u1_struct_0(sK353),u1_struct_0(sK353)),u1_struct_0(sK353))
| ~ l1_lattices(sK353)
| ~ spl2453_98
| ~ spl2453_120
| ~ spl2453_125 ),
inference(forward_subsumption_resolution,[],[f69714,f69294]) ).
fof(f69716,plain,
( ~ v1_funct_2(u2_lattices(sK353),k2_zfmisc_1(u1_struct_0(sK353),u1_struct_0(sK353)),u1_struct_0(sK353))
| ~ m2_relset_1(u2_lattices(sK353),k2_zfmisc_1(u1_struct_0(sK353),u1_struct_0(sK353)),u1_struct_0(sK353))
| ~ l1_lattices(sK353)
| ~ spl2453_98
| ~ spl2453_120
| ~ spl2453_125 ),
inference(forward_subsumption_resolution,[],[f69715,f49202]) ).
fof(f69717,plain,
( ~ m2_relset_1(u2_lattices(sK353),k2_zfmisc_1(u1_struct_0(sK353),u1_struct_0(sK353)),u1_struct_0(sK353))
| ~ l1_lattices(sK353)
| ~ spl2453_98
| ~ spl2453_120
| ~ spl2453_123
| ~ spl2453_125 ),
inference(forward_subsumption_resolution,[],[f69716,f69286]) ).
fof(f69718,plain,
( ~ l1_lattices(sK353)
| ~ spl2453_98
| ~ spl2453_120
| ~ spl2453_123
| ~ spl2453_124
| ~ spl2453_125 ),
inference(forward_subsumption_resolution,[],[f69717,f69290]) ).
fof(f69719,plain,
( $false
| ~ spl2453_98
| ~ spl2453_120
| ~ spl2453_123
| ~ spl2453_124
| ~ spl2453_125 ),
inference(forward_subsumption_resolution,[],[f69718,f68833]) ).
fof(f69720,plain,
( ~ spl2453_98
| ~ spl2453_120
| ~ spl2453_123
| ~ spl2453_124
| ~ spl2453_125 ),
inference(avatar_contradiction_clause,[],[f69719]) ).
cnf(s42,plain,
( ~ spl2453_58
| ~ spl2453_59
| ~ spl2453_60
| ~ spl2453_61
| ~ spl2453_62
| ~ spl2453_63 ),
inference(sat_conversion,[],[f67544]) ).
cnf(s80,plain,
( spl2453_74
| ~ spl2453_83
| ~ spl2453_84
| spl2453_99 ),
inference(sat_conversion,[],[f69013]) ).
cnf(s81,plain,
( spl2453_74
| ~ spl2453_83
| ~ spl2453_84
| spl2453_98 ),
inference(sat_conversion,[],[f69014]) ).
cnf(s82,plain,
( ~ spl2453_100
| spl2453_101 ),
inference(sat_conversion,[],[f69147]) ).
cnf(s84,plain,
( ~ spl2453_103
| spl2453_104 ),
inference(sat_conversion,[],[f69159]) ).
cnf(s96,plain,
spl2453_103,
inference(sat_conversion,[],[f69218]) ).
cnf(s97,plain,
spl2453_100,
inference(sat_conversion,[],[f69221]) ).
cnf(s99,plain,
( spl2453_59
| ~ spl2453_100
| ~ spl2453_104
| spl2453_120 ),
inference(sat_conversion,[],[f69252]) ).
cnf(s101,plain,
( spl2453_58
| ~ spl2453_99
| ~ spl2453_101
| ~ spl2453_103
| ~ spl2453_123
| ~ spl2453_124
| ~ spl2453_125 ),
inference(sat_conversion,[],[f69296]) ).
cnf(s106,plain,
spl2453_83,
inference(sat_conversion,[],[f69425]) ).
cnf(s108,plain,
( spl2453_71
| ~ spl2453_83 ),
inference(sat_conversion,[],[f69439]) ).
cnf(s113,plain,
( ~ spl2453_71
| spl2453_124 ),
inference(sat_conversion,[],[f69472]) ).
cnf(s114,plain,
( ~ spl2453_71
| spl2453_123 ),
inference(sat_conversion,[],[f69473]) ).
cnf(s116,plain,
~ spl2453_74,
inference(sat_conversion,[],[f69477]) ).
cnf(s125,plain,
spl2453_84,
inference(sat_conversion,[],[f69545]) ).
cnf(s126,plain,
spl2453_125,
inference(sat_conversion,[],[f69658]) ).
cnf(s127,plain,
spl2453_60,
inference(sat_conversion,[],[f69665]) ).
cnf(s128,plain,
spl2453_62,
inference(sat_conversion,[],[f69672]) ).
cnf(s129,plain,
spl2453_61,
inference(sat_conversion,[],[f69679]) ).
cnf(s130,plain,
spl2453_63,
inference(sat_conversion,[],[f69686]) ).
cnf(s135,plain,
( ~ spl2453_98
| ~ spl2453_120
| ~ spl2453_123
| ~ spl2453_124
| ~ spl2453_125 ),
inference(sat_conversion,[],[f69720]) ).
cnf(s142,plain,
spl2453_71,
inference(rat,[],[s108,s106]) ).
cnf(s144,plain,
spl2453_123,
inference(rat,[],[s114,s142]) ).
cnf(s145,plain,
spl2453_124,
inference(rat,[],[s113,s142]) ).
cnf(s146,plain,
( spl2453_58
| ~ spl2453_99
| ~ spl2453_101
| ~ spl2453_103 ),
inference(rat,[],[s101,s126,s145,s144]) ).
cnf(s154,plain,
spl2453_104,
inference(rat,[],[s84,s96]) ).
cnf(s156,plain,
spl2453_101,
inference(rat,[],[s82,s97]) ).
cnf(s157,plain,
spl2453_98,
inference(rat,[],[s81,s125,s106,s116]) ).
cnf(s158,plain,
~ spl2453_120,
inference(rat,[],[s135,s126,s145,s144,s157]) ).
cnf(s159,plain,
spl2453_59,
inference(rat,[],[s99,s154,s97,s158]) ).
cnf(s160,plain,
spl2453_99,
inference(rat,[],[s80,s125,s106,s116]) ).
cnf(s161,plain,
spl2453_58,
inference(rat,[],[s146,s96,s156,s160]) ).
cnf(s178,plain,
$false,
inference(rat,[],[s42,s130,s128,s129,s127,s159,s161]) ).
fof(f69721,plain,
$false,
inference(avatar_sat_refutation,[],[s178]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT326+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.41 % Computer : n017.cluster.edu
% 0.12/0.41 % Model : x86_64 x86_64
% 0.12/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.41 % Memory : 8046.5625MB
% 0.12/0.41 % OS : Linux 6.8.0-71-generic
% 0.12/0.41 % CPULimit : 300
% 0.12/0.41 % WCLimit : 300
% 0.12/0.41 % DateTime : Sun Sep 27 14:34:45 UTC 2026
% 0.12/0.41 % CPUTime :
% 0.12/0.41 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.44 Running first-order theorem proving
% 0.12/0.44 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 18.39/5.37 % (2635060)Detected formulas, will run a generic FOF schedule.
% 18.39/5.37 % (2635066)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=4082819143:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2978 on theBenchmark for (2978ds/134677Mi)
% 18.39/5.37 % (2635065)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=1201175646:i=141193_2978 on theBenchmark for (2978ds/141193Mi)
% 18.39/5.37 % (2635068)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=464137853:i=109:sd=1:ins=1:gsp=on:ss=axioms_2978 on theBenchmark for (2978ds/109Mi)
% 18.39/5.37 % (2635071)dis-21_1_sil=8000:lcm=predicate:random_seed=1032832866:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2978 on theBenchmark for (2978ds/129Mi)
% 18.39/5.37 % (2635067)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=3876876709:i=141695:sd=1:nm=32:gsp=on:ss=included_2978 on theBenchmark for (2978ds/141695Mi)
% 18.39/5.37 % (2635070)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3115045149:s2a=on:i=139:gtg=position_2978 on theBenchmark for (2978ds/139Mi)
% 18.39/5.37 % (2635069)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2339594738:i=119:av=off:ss=axioms_2978 on theBenchmark for (2978ds/119Mi)
% 18.39/5.37 % (2635070)Instruction limit reached!
% 18.39/5.37 % (2635070)------------------------------
% 18.39/5.37 % (2635070)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.39/5.37 % (2635070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.39/5.37 % (2635070)CaDiCaL version: 2.1.3
% 18.39/5.37 % (2635070)Termination reason: Instruction limit
% 18.39/5.37 % (2635070)Termination phase: Property scanning
% 18.39/5.37 % (2635070)Time elapsed: 0.062 s
% 18.39/5.37 % (2635070)Peak memory usage: 136 MB
% 18.39/5.37 % (2635070)Instructions burned: 140 (million)
% 18.39/5.37 % (2635068)Instruction limit reached!
% 18.39/5.37 % (2635068)------------------------------
% 18.39/5.37 % (2635068)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.39/5.37 % (2635068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.39/5.37 % (2635068)CaDiCaL version: 2.1.3
% 18.39/5.37 % (2635068)Termination reason: Instruction limit
% 18.39/5.37 % (2635068)Termination phase: SInE selection
% 18.39/5.37 % (2635068)Time elapsed: 0.084 s
% 18.39/5.37 % (2635068)Peak memory usage: 136 MB
% 18.39/5.37 % (2635068)Instructions burned: 110 (million)
% 18.39/5.37 % (2635069)Instruction limit reached!
% 18.39/5.37 % (2635069)------------------------------
% 18.39/5.37 % (2635069)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.39/5.37 % (2635069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.39/5.37 % (2635069)CaDiCaL version: 2.1.3
% 18.39/5.37 % (2635069)Termination reason: Instruction limit
% 18.39/5.37 % (2635069)Termination phase: SInE selection
% 18.39/5.37 % (2635069)Time elapsed: 0.090 s
% 18.39/5.37 % (2635069)Peak memory usage: 136 MB
% 18.39/5.37 % (2635069)Instructions burned: 119 (million)
% 18.39/5.37 % (2635071)Instruction limit reached!
% 18.39/5.37 % (2635071)------------------------------
% 18.39/5.37 % (2635071)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.39/5.37 % (2635071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.39/5.37 % (2635071)CaDiCaL version: 2.1.3
% 18.39/5.37 % (2635071)Termination reason: Instruction limit
% 18.39/5.37 % (2635071)Termination phase: SInE selection
% 18.39/5.37 % (2635071)Time elapsed: 0.093 s
% 18.39/5.37 % (2635071)Peak memory usage: 136 MB
% 18.39/5.37 % (2635071)Instructions burned: 129 (million)
% 18.39/5.37 % (2635079)lrs+10_1_sil=8000:sp=occurrence:random_seed=1158793652:i=285:sd=3:ss=axioms:sgt=8_2975 on theBenchmark for (2975ds/285Mi)
% 18.39/5.37 % (2635080)lrs+10_1_sil=32000:urr=on:br=off:random_seed=913820777:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2975 on theBenchmark for (2975ds/157Mi)
% 18.39/5.37 % (2635082)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=3568774875:s2a=on:i=248:s2at=1.23:gtg=position_2975 on theBenchmark for (2975ds/248Mi)
% 18.39/5.37 % (2635081)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3124509938:i=325:sd=1:ss=axioms:sgt=32_2975 on theBenchmark for (2975ds/325Mi)
% 18.39/5.37 % (2635080)Instruction limit reached!
% 25.27/6.34 % (2635080)------------------------------
% 25.27/6.34 % (2635080)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.27/6.34 % (2635080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.27/6.34 % (2635080)CaDiCaL version: 2.1.3
% 25.27/6.34 % (2635080)Termination reason: Instruction limit
% 25.27/6.34 % (2635080)Termination phase: Property scanning
% 25.27/6.34 % (2635080)Time elapsed: 0.070 s
% 25.27/6.34 % (2635080)Peak memory usage: 136 MB
% 25.27/6.34 % (2635080)Instructions burned: 159 (million)
% 25.27/6.34 % (2635082)Instruction limit reached!
% 25.27/6.34 % (2635082)------------------------------
% 25.27/6.34 % (2635082)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.27/6.34 % (2635082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.27/6.34 % (2635082)CaDiCaL version: 2.1.3
% 25.27/6.34 % (2635082)Termination reason: Instruction limit
% 25.27/6.34 % (2635082)Termination phase: Property scanning
% 25.27/6.34 % (2635082)Time elapsed: 0.109 s
% 25.27/6.34 % (2635082)Peak memory usage: 136 MB
% 25.27/6.34 % (2635082)Instructions burned: 250 (million)
% 25.27/6.34 % (2635079)Instruction limit reached!
% 25.27/6.34 % (2635079)------------------------------
% 25.27/6.34 % (2635079)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.27/6.34 % (2635079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.27/6.34 % (2635079)CaDiCaL version: 2.1.3
% 25.27/6.34 % (2635079)Termination reason: Instruction limit
% 25.27/6.34 % (2635079)Termination phase: Property scanning
% 25.27/6.34 % (2635079)Time elapsed: 0.231 s
% 25.27/6.34 % (2635079)Peak memory usage: 140 MB
% 25.27/6.34 % (2635079)Instructions burned: 286 (million)
% 25.27/6.34 % (2635087)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2246591761:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2973 on theBenchmark for (2973ds/294Mi)
% 25.27/6.34 % (2635081)Instruction limit reached!
% 25.27/6.34 % (2635081)------------------------------
% 25.27/6.34 % (2635081)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.27/6.34 % (2635081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.27/6.34 % (2635081)CaDiCaL version: 2.1.3
% 25.27/6.34 % (2635081)Termination reason: Instruction limit
% 25.27/6.34 % (2635081)Termination phase: Saturation
% 25.27/6.34 % (2635081)Time elapsed: 0.252 s
% 25.27/6.34 % (2635081)Peak memory usage: 142 MB
% 25.27/6.34 % (2635081)Instructions burned: 325 (million)
% 25.27/6.34 % (2635088)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=691232434:i=2350_2972 on theBenchmark for (2972ds/2350Mi)
% 25.27/6.34 % (2635089)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=467981179:cts=off:i=113:fsr=off:ss=included:sgt=4_2971 on theBenchmark for (2971ds/113Mi)
% 25.27/6.34 % (2635087)Instruction limit reached!
% 25.27/6.34 % (2635087)------------------------------
% 25.27/6.34 % (2635087)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.27/6.34 % (2635087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.27/6.34 % (2635087)CaDiCaL version: 2.1.3
% 25.27/6.34 % (2635087)Termination reason: Instruction limit
% 25.27/6.34 % (2635087)Termination phase: SInE selection
% 25.27/6.34 % (2635087)Time elapsed: 0.190 s
% 25.27/6.34 % (2635087)Peak memory usage: 137 MB
% 25.27/6.34 % (2635087)Instructions burned: 294 (million)
% 25.27/6.34 % (2635091)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=426714465:i=127:av=off:fsr=off:sup=off_2971 on theBenchmark for (2971ds/127Mi)
% 25.27/6.34 % (2635089)Instruction limit reached!
% 25.27/6.34 % (2635089)------------------------------
% 25.27/6.34 % (2635089)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.27/6.34 % (2635089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.27/6.34 % (2635089)CaDiCaL version: 2.1.3
% 25.27/6.34 % (2635089)Termination reason: Instruction limit
% 25.27/6.34 % (2635089)Termination phase: SInE selection
% 25.27/6.34 % (2635089)Time elapsed: 0.087 s
% 25.27/6.34 % (2635089)Peak memory usage: 136 MB
% 25.27/6.34 % (2635089)Instructions burned: 114 (million)
% 25.27/6.34 % (2635091)Instruction limit reached!
% 25.27/6.34 % (2635091)------------------------------
% 25.27/6.34 % (2635091)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.27/6.34 % (2635091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.27/6.34 % (2635091)CaDiCaL version: 2.1.3
% 49.62/10.96 % (2635091)Termination reason: Instruction limit
% 49.62/10.96 % (2635091)Termination phase: Preprocessing 1
% 49.62/10.96 % (2635091)Time elapsed: 0.099 s
% 49.62/10.96 % (2635091)Peak memory usage: 137 MB
% 49.62/10.96 % (2635091)Instructions burned: 128 (million)
% 49.62/10.96 % (2635094)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=4290612510:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2969 on theBenchmark for (2969ds/114Mi)
% 49.62/10.96 % (2635096)lrs+10_1_sil=8000:sp=occurrence:random_seed=1054657957:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2969 on theBenchmark for (2969ds/907Mi)
% 49.62/10.96 % (2635094)Instruction limit reached!
% 49.62/10.96 % (2635094)------------------------------
% 49.62/10.96 % (2635094)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.62/10.96 % (2635094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.62/10.96 % (2635094)CaDiCaL version: 2.1.3
% 49.62/10.96 % (2635094)Termination reason: Instruction limit
% 49.62/10.96 % (2635094)Termination phase: Property scanning
% 49.62/10.96 % (2635094)Time elapsed: 0.053 s
% 49.62/10.96 % (2635094)Peak memory usage: 136 MB
% 49.62/10.96 % (2635094)Instructions burned: 115 (million)
% 49.62/10.96 % (2635097)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1465742959:i=437:sd=1:aac=none:ss=included_2968 on theBenchmark for (2968ds/437Mi)
% 49.62/10.96 % (2635100)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=344828147:i=5202:ss=axioms:sgt=16_2967 on theBenchmark for (2967ds/5202Mi)
% 49.62/10.96 % (2635097)Instruction limit reached!
% 49.62/10.96 % (2635097)------------------------------
% 49.62/10.96 % (2635097)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.62/10.96 % (2635097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.62/10.96 % (2635097)CaDiCaL version: 2.1.3
% 49.62/10.96 % (2635097)Termination reason: Instruction limit
% 49.62/10.96 % (2635097)Termination phase: Saturation
% 49.62/10.96 % (2635097)Time elapsed: 0.295 s
% 49.62/10.96 % (2635097)Peak memory usage: 144 MB
% 49.62/10.96 % (2635097)Instructions burned: 437 (million)
% 49.62/10.96 % (2635103)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1806197945:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2963 on theBenchmark for (2963ds/134Mi)
% 49.62/10.96 % (2635096)Instruction limit reached!
% 49.62/10.96 % (2635096)------------------------------
% 49.62/10.96 % (2635096)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.62/10.96 % (2635096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.62/10.96 % (2635096)CaDiCaL version: 2.1.3
% 49.62/10.96 % (2635096)Termination reason: Instruction limit
% 49.62/10.96 % (2635096)Termination phase: Property scanning
% 49.62/10.96 % (2635096)Time elapsed: 0.619 s
% 49.62/10.96 % (2635096)Peak memory usage: 161 MB
% 49.62/10.96 % (2635096)Instructions burned: 908 (million)
% 49.62/10.96 % (2635103)Instruction limit reached!
% 49.62/10.96 % (2635103)------------------------------
% 49.62/10.96 % (2635103)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.62/10.96 % (2635103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.62/10.96 % (2635103)CaDiCaL version: 2.1.3
% 49.62/10.96 % (2635103)Termination reason: Instruction limit
% 49.62/10.96 % (2635103)Termination phase: SInE selection
% 49.62/10.96 % (2635103)Time elapsed: 0.104 s
% 49.62/10.96 % (2635103)Peak memory usage: 136 MB
% 49.62/10.96 % (2635103)Instructions burned: 134 (million)
% 49.62/10.96 % (2635105)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3421717743:st=8:i=592:sd=3:ep=RST:ss=axioms_2961 on theBenchmark for (2961ds/592Mi)
% 49.62/10.96 % (2635106)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=720586919:st=3:i=13193:sd=3:ss=axioms_2960 on theBenchmark for (2960ds/13193Mi)
% 49.62/10.96 % (2635105)Instruction limit reached!
% 49.62/10.96 % (2635105)------------------------------
% 49.62/10.96 % (2635105)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.62/10.96 % (2635105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.62/10.96 % (2635105)CaDiCaL version: 2.1.3
% 49.62/10.96 % (2635105)Termination reason: Instruction limit
% 49.62/10.96 % (2635105)Termination phase: Preprocessing 2
% 49.62/10.96 % (2635105)Time elapsed: 0.477 s
% 49.62/10.96 % (2635105)Peak memory usage: 142 MB
% 49.62/10.96 % (2635105)Instructions burned: 592 (million)
% 49.62/10.96 % (2635088)Instruction limit reached!
% 49.62/10.96 % (2635088)------------------------------
% 49.62/10.96 % (2635088)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.62/10.96 % (2635088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.62/10.96 % (2635088)CaDiCaL version: 2.1.3
% 49.62/10.96 % (2635088)Termination reason: Instruction limit
% 49.62/10.96 % (2635088)Termination phase: Property scanning
% 49.62/10.96 % (2635088)Time elapsed: 1.588 s
% 49.62/10.96 % (2635088)Peak memory usage: 233 MB
% 49.62/10.96 % (2635088)Instructions burned: 2351 (million)
% 49.62/10.96 % (2635109)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=444874103:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2954 on theBenchmark for (2954ds/125Mi)
% 49.62/10.96 % (2635110)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=710949695:i=134:gtgl=5:slsql=off:gtg=exists_sym_2954 on theBenchmark for (2954ds/134Mi)
% 49.62/10.96 % (2635109)Instruction limit reached!
% 49.62/10.96 % (2635109)------------------------------
% 49.62/10.96 % (2635109)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.62/10.96 % (2635109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.62/10.97 % (2635109)CaDiCaL version: 2.1.3
% 49.62/10.97 % (2635109)Termination reason: Instruction limit
% 49.62/10.97 % (2635109)Termination phase: Property scanning
% 49.62/10.97 % (2635109)Time elapsed: 0.056 s
% 49.62/10.97 % (2635109)Peak memory usage: 136 MB
% 49.62/10.97 % (2635109)Instructions burned: 126 (million)
% 49.62/10.97 % (2635110)Instruction limit reached!
% 49.62/10.97 % (2635110)------------------------------
% 49.62/10.97 % (2635110)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.62/10.97 % (2635110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.62/10.97 % (2635110)CaDiCaL version: 2.1.3
% 49.62/10.97 % (2635110)Termination reason: Instruction limit
% 49.62/10.97 % (2635110)Termination phase: Property scanning
% 49.62/10.97 % (2635110)Time elapsed: 0.059 s
% 49.62/10.97 % (2635110)Peak memory usage: 136 MB
% 49.62/10.97 % (2635110)Instructions burned: 135 (million)
% 49.62/10.97 % (2635114)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3208154619:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2952 on theBenchmark for (2952ds/431Mi)
% 49.62/10.97 % (2635113)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3009222450:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2952 on theBenchmark for (2952ds/141Mi)
% 49.62/10.97 % (2635113)Instruction limit reached!
% 49.62/10.97 % (2635113)------------------------------
% 49.62/10.97 % (2635113)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.62/10.97 % (2635113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.62/10.97 % (2635113)CaDiCaL version: 2.1.3
% 49.62/10.97 % (2635113)Termination reason: Instruction limit
% 49.62/10.97 % (2635113)Termination phase: SInE selection
% 49.62/10.97 % (2635113)Time elapsed: 0.101 s
% 49.62/10.97 % (2635113)Peak memory usage: 136 MB
% 49.62/10.97 % (2635113)Instructions burned: 141 (million)
% 49.62/10.97 % (2635117)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=1482327673:i=6060:aac=none:ins=25_2950 on theBenchmark for (2950ds/6060Mi)
% 49.62/10.97 % (2635114)Instruction limit reached!
% 49.62/10.97 % (2635114)------------------------------
% 49.62/10.97 % (2635114)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.62/10.97 % (2635114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.62/10.97 % (2635114)CaDiCaL version: 2.1.3
% 49.62/10.97 % (2635114)Termination reason: Instruction limit
% 49.62/10.97 % (2635114)Termination phase: Saturation
% 49.62/10.97 % (2635114)Time elapsed: 0.296 s
% 49.62/10.97 % (2635114)Peak memory usage: 144 MB
% 49.62/10.97 % (2635114)Instructions burned: 433 (million)
% 49.62/10.97 % (2635119)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=3934905552:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2948 on theBenchmark for (2948ds/150Mi)
% 49.62/10.97 % (2635119)Instruction limit reached!
% 49.62/10.97 % (2635119)------------------------------
% 49.62/10.97 % (2635119)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.62/10.97 % (2635119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.62/10.97 % (2635119)CaDiCaL version: 2.1.3
% 49.62/10.97 % (2635119)Termination reason: Instruction limit
% 49.62/10.97 % (2635119)Termination phase: SInE selection
% 49.62/10.97 % (2635119)Time elapsed: 0.114 s
% 49.62/10.97 % (2635119)Peak memory usage: 136 MB
% 49.62/10.97 % (2635119)Instructions burned: 151 (million)
% 49.62/10.97 % (2635121)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=799045951:i=14155:bd=all_2945 on theBenchmark for (2945ds/14155Mi)
% 49.62/10.97 % (2635100)Instruction limit reached!
% 49.62/10.97 % (2635100)------------------------------
% 49.62/10.97 % (2635100)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.62/10.97 % (2635100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.62/10.97 % (2635100)CaDiCaL version: 2.1.3
% 49.62/10.97 % (2635100)Termination reason: Instruction limit
% 49.62/10.97 % (2635100)Termination phase: Saturation
% 49.62/10.97 % (2635100)Time elapsed: 3.824 s
% 49.62/10.97 % (2635100)Peak memory usage: 568 MB
% 49.62/10.97 % (2635100)Instructions burned: 5202 (million)
% 49.62/10.97 % (2635123)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2099590604:i=667:av=off:fsr=off_2926 on theBenchmark for (2926ds/667Mi)
% 49.62/10.97 % (2635123)Instruction limit reached!
% 49.62/10.97 % (2635123)------------------------------
% 49.62/10.97 % (2635123)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.62/10.97 % (2635123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.62/10.97 % (2635123)CaDiCaL version: 2.1.3
% 49.62/10.97 % (2635123)Termination reason: Instruction limit
% 49.62/10.97 % (2635123)Termination phase: NewCNF
% 49.62/10.97 % (2635123)Time elapsed: 0.533 s
% 49.62/10.97 % (2635123)Peak memory usage: 186 MB
% 49.62/10.97 % (2635123)Instructions burned: 667 (million)
% 49.62/10.97 % (2635125)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=2531504352:s2a=on:i=185:s2at=1.8:fdi=4_2919 on theBenchmark for (2919ds/185Mi)
% 49.62/10.97 % (2635125)Instruction limit reached!
% 49.62/10.97 % (2635125)------------------------------
% 49.62/10.97 % (2635125)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.62/10.97 % (2635125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.62/10.97 % (2635125)CaDiCaL version: 2.1.3
% 49.62/10.97 % (2635125)Termination reason: Instruction limit
% 49.62/10.97 % (2635125)Termination phase: SInE selection
% 49.62/10.97 % (2635125)Time elapsed: 0.128 s
% 49.62/10.97 % (2635125)Peak memory usage: 136 MB
% 49.62/10.97 % (2635125)Instructions burned: 188 (million)
% 49.62/10.97 % (2635127)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2580350261:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2916 on theBenchmark for (2916ds/193Mi)
% 49.62/10.97 % (2635127)Instruction limit reached!
% 49.62/10.97 % (2635127)------------------------------
% 49.62/10.97 % (2635127)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.62/10.97 % (2635127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.62/10.97 % (2635127)CaDiCaL version: 2.1.3
% 49.62/10.97 % (2635127)Termination reason: Instruction limit
% 49.62/10.97 % (2635127)Termination phase: SInE selection
% 49.62/10.97 % (2635127)Time elapsed: 0.146 s
% 49.62/10.97 % (2635127)Peak memory usage: 137 MB
% 49.62/10.97 % (2635127)Instructions burned: 194 (million)
% 49.62/10.97 % (2635129)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=4264428332:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2913 on theBenchmark for (2913ds/4850Mi)
% 49.62/10.97 % (2635117)Instruction limit reached!
% 49.62/10.97 % (2635117)------------------------------
% 49.62/10.97 % (2635117)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.62/10.97 % (2635117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.62/10.97 % (2635117)CaDiCaL version: 2.1.3
% 49.62/10.97 % (2635117)Termination reason: Instruction limit
% 49.62/10.97 % (2635117)Termination phase: Function definition elimination
% 49.62/10.97 % (2635117)Time elapsed: 3.829 s
% 49.62/10.97 % (2635117)Peak memory usage: 245 MB
% 49.62/10.97 % (2635117)Instructions burned: 6062 (million)
% 49.62/10.97 % (2635131)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=4180219658:i=12111:sd=1:ss=included_2909 on theBenchmark for (2909ds/12111Mi)
% 49.62/10.97 % (2635106)First to succeed.
% 49.62/10.97 % (2635106)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2635060"
% 49.62/10.97 % (2635106)Refutation found. Thanks to Tanya!
% 49.62/10.97 % SZS status Theorem for theBenchmark
% 49.62/10.97 % SZS output start Proof for theBenchmark
% See solution above
% 57.84/11.22 % (2635106)------------------------------
% 57.84/11.22 % (2635106)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.84/11.22 % (2635106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.84/11.22 % (2635106)CaDiCaL version: 2.1.3
% 57.84/11.22 % (2635106)Termination reason: Refutation
% 57.84/11.22 % (2635106)Time elapsed: 5.480 s
% 57.84/11.22 % (2635106)Peak memory usage: 404 MB
% 57.84/11.22 % (2635106)Instructions burned: 9214 (million)
% 57.84/11.22 % (2635106)------------------------------
% 57.84/11.22 % (2635106)------------------------------
% 57.84/11.22 % (2635060)Success in time 10.081 s
% 57.84/11.22 % Vampire exiting
%------------------------------------------------------------------------------