%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LAT295+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n013.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:48:15 AM UTC 2026
% Result : Theorem 0.19s 0.51s
% Output : Refutation 0.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 25
% Syntax : Number of formulae : 224 ( 45 unt; 16 def)
% Number of atoms : 788 ( 151 equ)
% Maximal formula atoms : 17 ( 3 avg)
% Number of connectives : 978 ( 414 ~; 433 |; 77 &)
% ( 20 <=>; 34 =>; 0 <=; 0 <~>)
% Maximal formula depth : 22 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 28 ( 26 usr; 17 prp; 0-3 aty)
% Number of functors : 14 ( 14 usr; 6 con; 0-6 aty)
% Number of variables : 184 ( 0 sgn 172 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& l3_lattices(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& l3_lattices(X1) )
=> ( g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) = g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
=> ! [X4] :
( m1_subset_1(X4,u1_struct_0(X1))
=> ! [X5] :
( m1_subset_1(X5,u1_struct_0(X1))
=> ( ( X2 = X4
& X3 = X5 )
=> ( k1_lattices(X0,X2,X3) = k1_lattices(X1,X4,X5)
& k2_lattices(X0,X2,X3) = k2_lattices(X1,X4,X5)
& ( r1_lattices(X0,X2,X3)
=> r1_lattices(X1,X4,X5) )
& ( r1_lattices(X1,X4,X5)
=> r1_lattices(X0,X2,X3) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t8_filter_2) ).
fof(f2,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& l3_lattices(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& l3_lattices(X1) )
=> ( g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) = g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
=> ! [X4] :
( m1_subset_1(X4,u1_struct_0(X1))
=> ! [X5] :
( m1_subset_1(X5,u1_struct_0(X1))
=> ( ( X2 = X4
& X3 = X5 )
=> ( k1_lattices(X0,X2,X3) = k1_lattices(X1,X4,X5)
& k2_lattices(X0,X2,X3) = k2_lattices(X1,X4,X5)
& ( r1_lattices(X0,X2,X3)
=> r1_lattices(X1,X4,X5) )
& ( r1_lattices(X1,X4,X5)
=> r1_lattices(X0,X2,X3) ) ) ) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f11,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l2_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> k1_lattices(X0,X1,X2) = k2_binop_1(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),u2_lattices(X0),X1,X2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_lattices) ).
fof(f12,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> k2_lattices(X0,X1,X2) = k2_binop_1(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),u1_lattices(X0),X1,X2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d2_lattices) ).
fof(f13,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l2_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ( r1_lattices(X0,X1,X2)
<=> k1_lattices(X0,X1,X2) = X2 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d3_lattices) ).
fof(f30,axiom,
! [X0] :
( l3_lattices(X0)
=> ( l1_lattices(X0)
& l2_lattices(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l3_lattices) ).
fof(f34,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(f36,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(f52,axiom,
! [X0,X1,X2] :
( ( v1_funct_1(X1)
& v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
& m1_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
& v1_funct_1(X2)
& v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
& m1_relset_1(X2,k2_zfmisc_1(X0,X0),X0) )
=> ! [X3,X4,X5] :
( g3_lattices(X0,X1,X2) = g3_lattices(X3,X4,X5)
=> ( X0 = X3
& X1 = X4
& X2 = X5 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',free_g3_lattices) ).
fof(f67,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
<=> m1_relset_1(X2,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(f82,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( ? [X4] :
( ? [X5] :
( ( k1_lattices(X0,X2,X3) != k1_lattices(X1,X4,X5)
| k2_lattices(X0,X2,X3) != k2_lattices(X1,X4,X5)
| ( ~ r1_lattices(X1,X4,X5)
& r1_lattices(X0,X2,X3) )
| ( ~ r1_lattices(X0,X2,X3)
& r1_lattices(X1,X4,X5) ) )
& X2 = X4
& X3 = X5
& m1_subset_1(X5,u1_struct_0(X1)) )
& m1_subset_1(X4,u1_struct_0(X1)) )
& m1_subset_1(X3,u1_struct_0(X0)) )
& m1_subset_1(X2,u1_struct_0(X0)) )
& g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) = g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1))
& ~ v3_struct_0(X1)
& l3_lattices(X1) )
& ~ v3_struct_0(X0)
& l3_lattices(X0) ),
inference(ennf_transformation,[],[f2]) ).
fof(f83,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( ? [X4] :
( ? [X5] :
( ( k1_lattices(X0,X2,X3) != k1_lattices(X1,X4,X5)
| k2_lattices(X0,X2,X3) != k2_lattices(X1,X4,X5)
| ( ~ r1_lattices(X1,X4,X5)
& r1_lattices(X0,X2,X3) )
| ( ~ r1_lattices(X0,X2,X3)
& r1_lattices(X1,X4,X5) ) )
& X2 = X4
& X3 = X5
& m1_subset_1(X5,u1_struct_0(X1)) )
& m1_subset_1(X4,u1_struct_0(X1)) )
& m1_subset_1(X3,u1_struct_0(X0)) )
& m1_subset_1(X2,u1_struct_0(X0)) )
& g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) = g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1))
& ~ v3_struct_0(X1)
& l3_lattices(X1) )
& ~ v3_struct_0(X0)
& l3_lattices(X0) ),
inference(flattening,[],[f82]) ).
fof(f94,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( k1_lattices(X0,X1,X2) = k2_binop_1(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),u2_lattices(X0),X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ l2_lattices(X0) ),
inference(ennf_transformation,[],[f11]) ).
fof(f95,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( k1_lattices(X0,X1,X2) = k2_binop_1(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),u2_lattices(X0),X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ l2_lattices(X0) ),
inference(flattening,[],[f94]) ).
fof(f96,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( k2_lattices(X0,X1,X2) = k2_binop_1(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),u1_lattices(X0),X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ l1_lattices(X0) ),
inference(ennf_transformation,[],[f12]) ).
fof(f97,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( k2_lattices(X0,X1,X2) = k2_binop_1(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),u1_lattices(X0),X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ l1_lattices(X0) ),
inference(flattening,[],[f96]) ).
fof(f98,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( r1_lattices(X0,X1,X2)
<=> k1_lattices(X0,X1,X2) = X2 )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ l2_lattices(X0) ),
inference(ennf_transformation,[],[f13]) ).
fof(f99,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( r1_lattices(X0,X1,X2)
<=> k1_lattices(X0,X1,X2) = X2 )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ l2_lattices(X0) ),
inference(flattening,[],[f98]) ).
fof(f110,plain,
! [X0] :
( ( l1_lattices(X0)
& l2_lattices(X0) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f30]) ).
fof(f112,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,[],[f34]) ).
fof(f113,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,[],[f36]) ).
fof(f120,plain,
! [X0,X1,X2] :
( ! [X3,X4,X5] :
( ( X0 = X3
& X1 = X4
& X2 = X5 )
| g3_lattices(X0,X1,X2) != g3_lattices(X3,X4,X5) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m1_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m1_relset_1(X2,k2_zfmisc_1(X0,X0),X0) ),
inference(ennf_transformation,[],[f52]) ).
fof(f121,plain,
! [X0,X1,X2] :
( ! [X3,X4,X5] :
( ( X0 = X3
& X1 = X4
& X2 = X5 )
| g3_lattices(X0,X1,X2) != g3_lattices(X3,X4,X5) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m1_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m1_relset_1(X2,k2_zfmisc_1(X0,X0),X0) ),
inference(flattening,[],[f120]) ).
fof(f137,plain,
( ( k1_lattices(sK0,sK2,sK3) != k1_lattices(sK1,sK4,sK5)
| k2_lattices(sK0,sK2,sK3) != k2_lattices(sK1,sK4,sK5)
| ( ~ r1_lattices(sK1,sK4,sK5)
& r1_lattices(sK0,sK2,sK3) )
| ( ~ r1_lattices(sK0,sK2,sK3)
& r1_lattices(sK1,sK4,sK5) ) )
& sK2 = sK4
& sK3 = sK5
& m1_subset_1(sK5,u1_struct_0(sK1))
& m1_subset_1(sK4,u1_struct_0(sK1))
& m1_subset_1(sK3,u1_struct_0(sK0))
& m1_subset_1(sK2,u1_struct_0(sK0))
& g3_lattices(u1_struct_0(sK0),u2_lattices(sK0),u1_lattices(sK0)) = g3_lattices(u1_struct_0(sK1),u2_lattices(sK1),u1_lattices(sK1))
& ~ v3_struct_0(sK1)
& l3_lattices(sK1)
& ~ v3_struct_0(sK0)
& l3_lattices(sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3,sK4,sK5]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2),skolemize(X3,sK3),skolemize(X4,sK4),skolemize(X5,sK5)],[f83]) ).
fof(f138,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( r1_lattices(X0,X1,X2)
| k1_lattices(X0,X1,X2) != X2 )
& ( k1_lattices(X0,X1,X2) = X2
| ~ r1_lattices(X0,X1,X2) ) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ l2_lattices(X0) ),
inference(nnf_transformation,[],[f99]) ).
fof(f159,plain,
! [X0,X1,X2] :
( ( m2_relset_1(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1) )
& ( m1_relset_1(X2,X0,X1)
| ~ m2_relset_1(X2,X0,X1) ) ),
inference(nnf_transformation,[],[f67]) ).
fof(f160,plain,
l3_lattices(sK0),
inference(cnf_transformation,[],[f137]) ).
fof(f161,plain,
~ v3_struct_0(sK0),
inference(cnf_transformation,[],[f137]) ).
fof(f162,plain,
l3_lattices(sK1),
inference(cnf_transformation,[],[f137]) ).
fof(f163,plain,
~ v3_struct_0(sK1),
inference(cnf_transformation,[],[f137]) ).
fof(f164,plain,
g3_lattices(u1_struct_0(sK0),u2_lattices(sK0),u1_lattices(sK0)) = g3_lattices(u1_struct_0(sK1),u2_lattices(sK1),u1_lattices(sK1)),
inference(cnf_transformation,[],[f137]) ).
fof(f165,plain,
m1_subset_1(sK2,u1_struct_0(sK0)),
inference(cnf_transformation,[],[f137]) ).
fof(f166,plain,
m1_subset_1(sK3,u1_struct_0(sK0)),
inference(cnf_transformation,[],[f137]) ).
fof(f167,plain,
m1_subset_1(sK4,u1_struct_0(sK1)),
inference(cnf_transformation,[],[f137]) ).
fof(f168,plain,
m1_subset_1(sK5,u1_struct_0(sK1)),
inference(cnf_transformation,[],[f137]) ).
fof(f169,plain,
sK3 = sK5,
inference(cnf_transformation,[],[f137]) ).
fof(f170,plain,
sK2 = sK4,
inference(cnf_transformation,[],[f137]) ).
fof(f171,plain,
( k1_lattices(sK0,sK2,sK3) != k1_lattices(sK1,sK4,sK5)
| k2_lattices(sK0,sK2,sK3) != k2_lattices(sK1,sK4,sK5)
| r1_lattices(sK0,sK2,sK3)
| r1_lattices(sK1,sK4,sK5) ),
inference(cnf_transformation,[],[f137]) ).
fof(f174,plain,
( k1_lattices(sK0,sK2,sK3) != k1_lattices(sK1,sK4,sK5)
| k2_lattices(sK0,sK2,sK3) != k2_lattices(sK1,sK4,sK5)
| ~ r1_lattices(sK1,sK4,sK5)
| ~ r1_lattices(sK0,sK2,sK3) ),
inference(cnf_transformation,[],[f137]) ).
fof(f184,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,u1_struct_0(X0))
| k1_lattices(X0,X1,X2) = k2_binop_1(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),u2_lattices(X0),X1,X2)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l2_lattices(X0) ),
inference(cnf_transformation,[],[f95]) ).
fof(f185,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,u1_struct_0(X0))
| k2_lattices(X0,X1,X2) = k2_binop_1(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),u1_lattices(X0),X1,X2)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_lattices(X0) ),
inference(cnf_transformation,[],[f97]) ).
fof(f186,plain,
! [X2,X0,X1] :
( ~ r1_lattices(X0,X1,X2)
| k1_lattices(X0,X1,X2) = X2
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l2_lattices(X0) ),
inference(cnf_transformation,[],[f138]) ).
fof(f187,plain,
! [X2,X0,X1] :
( k1_lattices(X0,X1,X2) != X2
| r1_lattices(X0,X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l2_lattices(X0) ),
inference(cnf_transformation,[],[f138]) ).
fof(f196,plain,
! [X0] :
( ~ l3_lattices(X0)
| l2_lattices(X0) ),
inference(cnf_transformation,[],[f110]) ).
fof(f197,plain,
! [X0] :
( ~ l3_lattices(X0)
| l1_lattices(X0) ),
inference(cnf_transformation,[],[f110]) ).
fof(f199,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,[],[f112]) ).
fof(f200,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,[],[f112]) ).
fof(f201,plain,
! [X0] :
( v1_funct_1(u1_lattices(X0))
| ~ l1_lattices(X0) ),
inference(cnf_transformation,[],[f112]) ).
fof(f202,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,[],[f113]) ).
fof(f203,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,[],[f113]) ).
fof(f204,plain,
! [X0] :
( v1_funct_1(u2_lattices(X0))
| ~ l2_lattices(X0) ),
inference(cnf_transformation,[],[f113]) ).
fof(f222,plain,
! [X2,X3,X0,X1,X4,X5] :
( g3_lattices(X0,X1,X2) != g3_lattices(X3,X4,X5)
| X2 = X5
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m1_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m1_relset_1(X2,k2_zfmisc_1(X0,X0),X0) ),
inference(cnf_transformation,[],[f121]) ).
fof(f223,plain,
! [X2,X3,X0,X1,X4,X5] :
( g3_lattices(X0,X1,X2) != g3_lattices(X3,X4,X5)
| X1 = X4
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m1_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m1_relset_1(X2,k2_zfmisc_1(X0,X0),X0) ),
inference(cnf_transformation,[],[f121]) ).
fof(f224,plain,
! [X2,X3,X0,X1,X4,X5] :
( g3_lattices(X0,X1,X2) != g3_lattices(X3,X4,X5)
| X0 = X3
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m1_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m1_relset_1(X2,k2_zfmisc_1(X0,X0),X0) ),
inference(cnf_transformation,[],[f121]) ).
fof(f252,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f159]) ).
fof(f263,plain,
( k1_lattices(sK1,sK4,sK5) != k1_lattices(sK0,sK4,sK5)
| k2_lattices(sK1,sK4,sK5) != k2_lattices(sK0,sK4,sK5)
| ~ r1_lattices(sK1,sK4,sK5)
| ~ r1_lattices(sK0,sK4,sK5) ),
inference(definition_unfolding,[],[f174,f170,f169,f170,f169,f170,f169]) ).
fof(f266,plain,
( k1_lattices(sK1,sK4,sK5) != k1_lattices(sK0,sK4,sK5)
| k2_lattices(sK1,sK4,sK5) != k2_lattices(sK0,sK4,sK5)
| r1_lattices(sK0,sK4,sK5)
| r1_lattices(sK1,sK4,sK5) ),
inference(definition_unfolding,[],[f171,f170,f169,f170,f169,f170,f169]) ).
fof(f267,plain,
m1_subset_1(sK5,u1_struct_0(sK0)),
inference(definition_unfolding,[],[f166,f169]) ).
fof(f268,plain,
m1_subset_1(sK4,u1_struct_0(sK0)),
inference(definition_unfolding,[],[f165,f170]) ).
fof(f271,definition,
( spl26_1
<=> r1_lattices(sK1,sK4,sK5) ),
introduced(definition,[new_symbols(definition,[spl26_1])],[avatar_definition]) ).
fof(f272,plain,
( ~ r1_lattices(sK1,sK4,sK5)
| spl26_1 ),
inference(avatar_component_clause,[],[f271]) ).
fof(f273,plain,
( r1_lattices(sK1,sK4,sK5)
| ~ spl26_1 ),
inference(avatar_component_clause,[],[f271]) ).
fof(f275,definition,
( spl26_2
<=> r1_lattices(sK0,sK4,sK5) ),
introduced(definition,[new_symbols(definition,[spl26_2])],[avatar_definition]) ).
fof(f276,plain,
( ~ r1_lattices(sK0,sK4,sK5)
| spl26_2 ),
inference(avatar_component_clause,[],[f275]) ).
fof(f277,plain,
( r1_lattices(sK0,sK4,sK5)
| ~ spl26_2 ),
inference(avatar_component_clause,[],[f275]) ).
fof(f279,definition,
( spl26_3
<=> k2_lattices(sK1,sK4,sK5) = k2_lattices(sK0,sK4,sK5) ),
introduced(definition,[new_symbols(definition,[spl26_3])],[avatar_definition]) ).
fof(f283,definition,
( spl26_4
<=> k1_lattices(sK1,sK4,sK5) = k1_lattices(sK0,sK4,sK5) ),
introduced(definition,[new_symbols(definition,[spl26_4])],[avatar_definition]) ).
fof(f284,plain,
( k1_lattices(sK1,sK4,sK5) = k1_lattices(sK0,sK4,sK5)
| ~ spl26_4 ),
inference(avatar_component_clause,[],[f283]) ).
fof(f286,plain,
( spl26_1
| spl26_2
| ~ spl26_3
| ~ spl26_4 ),
inference(avatar_split_clause,[],[f266,f283,f279,f275,f271]) ).
fof(f287,plain,
( ~ spl26_2
| ~ spl26_1
| ~ spl26_3
| ~ spl26_4 ),
inference(avatar_split_clause,[],[f263,f283,f279,f271,f275]) ).
fof(f298,plain,
l2_lattices(sK0),
inference(resolution,[],[f196,f160]) ).
fof(f299,plain,
l2_lattices(sK1),
inference(resolution,[],[f196,f162]) ).
fof(f304,plain,
l1_lattices(sK0),
inference(resolution,[],[f197,f160]) ).
fof(f305,plain,
l1_lattices(sK1),
inference(resolution,[],[f197,f162]) ).
fof(f409,plain,
! [X0] :
( m1_relset_1(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| ~ l1_lattices(X0) ),
inference(resolution,[],[f199,f252]) ).
fof(f416,plain,
! [X0] :
( m1_relset_1(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| ~ l2_lattices(X0) ),
inference(resolution,[],[f202,f252]) ).
fof(f443,plain,
! [X0] :
( k1_lattices(sK1,X0,sK5) = k2_binop_1(u1_struct_0(sK1),u1_struct_0(sK1),u1_struct_0(sK1),u2_lattices(sK1),X0,sK5)
| ~ m1_subset_1(X0,u1_struct_0(sK1))
| v3_struct_0(sK1)
| ~ l2_lattices(sK1) ),
inference(resolution,[],[f184,f168]) ).
fof(f444,plain,
! [X0] :
( k1_lattices(sK0,X0,sK5) = k2_binop_1(u1_struct_0(sK0),u1_struct_0(sK0),u1_struct_0(sK0),u2_lattices(sK0),X0,sK5)
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| v3_struct_0(sK0)
| ~ l2_lattices(sK0) ),
inference(resolution,[],[f184,f267]) ).
fof(f452,plain,
! [X0] :
( k1_lattices(sK0,X0,sK5) = k2_binop_1(u1_struct_0(sK0),u1_struct_0(sK0),u1_struct_0(sK0),u2_lattices(sK0),X0,sK5)
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ l2_lattices(sK0) ),
inference(forward_subsumption_resolution,[],[f444,f161]) ).
fof(f453,plain,
! [X0] :
( k1_lattices(sK1,X0,sK5) = k2_binop_1(u1_struct_0(sK1),u1_struct_0(sK1),u1_struct_0(sK1),u2_lattices(sK1),X0,sK5)
| ~ m1_subset_1(X0,u1_struct_0(sK1))
| ~ l2_lattices(sK1) ),
inference(forward_subsumption_resolution,[],[f443,f163]) ).
fof(f456,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK0))
| k1_lattices(sK0,X0,sK5) = k2_binop_1(u1_struct_0(sK0),u1_struct_0(sK0),u1_struct_0(sK0),u2_lattices(sK0),X0,sK5) ),
inference(forward_subsumption_resolution,[],[f452,f298]) ).
fof(f457,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK1))
| k1_lattices(sK1,X0,sK5) = k2_binop_1(u1_struct_0(sK1),u1_struct_0(sK1),u1_struct_0(sK1),u2_lattices(sK1),X0,sK5) ),
inference(forward_subsumption_resolution,[],[f453,f299]) ).
fof(f469,plain,
! [X0] :
( k2_lattices(sK1,X0,sK5) = k2_binop_1(u1_struct_0(sK1),u1_struct_0(sK1),u1_struct_0(sK1),u1_lattices(sK1),X0,sK5)
| ~ m1_subset_1(X0,u1_struct_0(sK1))
| v3_struct_0(sK1)
| ~ l1_lattices(sK1) ),
inference(resolution,[],[f185,f168]) ).
fof(f470,plain,
! [X0] :
( k2_lattices(sK0,X0,sK5) = k2_binop_1(u1_struct_0(sK0),u1_struct_0(sK0),u1_struct_0(sK0),u1_lattices(sK0),X0,sK5)
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| v3_struct_0(sK0)
| ~ l1_lattices(sK0) ),
inference(resolution,[],[f185,f267]) ).
fof(f478,plain,
! [X0] :
( k2_lattices(sK0,X0,sK5) = k2_binop_1(u1_struct_0(sK0),u1_struct_0(sK0),u1_struct_0(sK0),u1_lattices(sK0),X0,sK5)
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ l1_lattices(sK0) ),
inference(forward_subsumption_resolution,[],[f470,f161]) ).
fof(f479,plain,
! [X0] :
( k2_lattices(sK1,X0,sK5) = k2_binop_1(u1_struct_0(sK1),u1_struct_0(sK1),u1_struct_0(sK1),u1_lattices(sK1),X0,sK5)
| ~ m1_subset_1(X0,u1_struct_0(sK1))
| ~ l1_lattices(sK1) ),
inference(forward_subsumption_resolution,[],[f469,f163]) ).
fof(f482,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK0))
| k2_lattices(sK0,X0,sK5) = k2_binop_1(u1_struct_0(sK0),u1_struct_0(sK0),u1_struct_0(sK0),u1_lattices(sK0),X0,sK5) ),
inference(forward_subsumption_resolution,[],[f478,f304]) ).
fof(f483,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK1))
| k2_lattices(sK1,X0,sK5) = k2_binop_1(u1_struct_0(sK1),u1_struct_0(sK1),u1_struct_0(sK1),u1_lattices(sK1),X0,sK5) ),
inference(forward_subsumption_resolution,[],[f479,f305]) ).
fof(f488,plain,
k1_lattices(sK0,sK4,sK5) = k2_binop_1(u1_struct_0(sK0),u1_struct_0(sK0),u1_struct_0(sK0),u2_lattices(sK0),sK4,sK5),
inference(resolution,[],[f456,f268]) ).
fof(f541,plain,
k1_lattices(sK1,sK4,sK5) = k2_binop_1(u1_struct_0(sK1),u1_struct_0(sK1),u1_struct_0(sK1),u2_lattices(sK1),sK4,sK5),
inference(resolution,[],[f457,f167]) ).
fof(f551,plain,
! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != g3_lattices(u1_struct_0(sK0),u2_lattices(sK0),u1_lattices(sK0))
| u1_lattices(sK1) = X2
| ~ v1_funct_1(u2_lattices(sK1))
| ~ v1_funct_2(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ m1_relset_1(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ v1_funct_1(u1_lattices(sK1))
| ~ v1_funct_2(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ m1_relset_1(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1)) ),
inference(superposition,[],[f222,f164]) ).
fof(f555,definition,
( spl26_16
<=> m1_relset_1(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1)) ),
introduced(definition,[new_symbols(definition,[spl26_16])],[avatar_definition]) ).
fof(f556,plain,
( m1_relset_1(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ spl26_16 ),
inference(avatar_component_clause,[],[f555]) ).
fof(f557,plain,
( ~ m1_relset_1(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| spl26_16 ),
inference(avatar_component_clause,[],[f555]) ).
fof(f559,definition,
( spl26_17
<=> v1_funct_2(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1)) ),
introduced(definition,[new_symbols(definition,[spl26_17])],[avatar_definition]) ).
fof(f560,plain,
( v1_funct_2(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ spl26_17 ),
inference(avatar_component_clause,[],[f559]) ).
fof(f561,plain,
( ~ v1_funct_2(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| spl26_17 ),
inference(avatar_component_clause,[],[f559]) ).
fof(f563,definition,
( spl26_18
<=> v1_funct_1(u1_lattices(sK1)) ),
introduced(definition,[new_symbols(definition,[spl26_18])],[avatar_definition]) ).
fof(f564,plain,
( v1_funct_1(u1_lattices(sK1))
| ~ spl26_18 ),
inference(avatar_component_clause,[],[f563]) ).
fof(f565,plain,
( ~ v1_funct_1(u1_lattices(sK1))
| spl26_18 ),
inference(avatar_component_clause,[],[f563]) ).
fof(f567,definition,
( spl26_19
<=> m1_relset_1(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1)) ),
introduced(definition,[new_symbols(definition,[spl26_19])],[avatar_definition]) ).
fof(f569,plain,
( ~ m1_relset_1(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| spl26_19 ),
inference(avatar_component_clause,[],[f567]) ).
fof(f571,definition,
( spl26_20
<=> v1_funct_2(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1)) ),
introduced(definition,[new_symbols(definition,[spl26_20])],[avatar_definition]) ).
fof(f573,plain,
( ~ v1_funct_2(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| spl26_20 ),
inference(avatar_component_clause,[],[f571]) ).
fof(f575,definition,
( spl26_21
<=> v1_funct_1(u2_lattices(sK1)) ),
introduced(definition,[new_symbols(definition,[spl26_21])],[avatar_definition]) ).
fof(f577,plain,
( ~ v1_funct_1(u2_lattices(sK1))
| spl26_21 ),
inference(avatar_component_clause,[],[f575]) ).
fof(f579,definition,
( spl26_22
<=> ! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != g3_lattices(u1_struct_0(sK0),u2_lattices(sK0),u1_lattices(sK0))
| u1_lattices(sK1) = X2 ) ),
introduced(definition,[new_symbols(definition,[spl26_22])],[avatar_definition]) ).
fof(f580,plain,
( ! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != g3_lattices(u1_struct_0(sK0),u2_lattices(sK0),u1_lattices(sK0))
| u1_lattices(sK1) = X2 )
| ~ spl26_22 ),
inference(avatar_component_clause,[],[f579]) ).
fof(f581,plain,
( ~ spl26_16
| ~ spl26_17
| ~ spl26_18
| ~ spl26_19
| ~ spl26_20
| ~ spl26_21
| spl26_22 ),
inference(avatar_split_clause,[],[f551,f579,f575,f571,f567,f563,f559,f555]) ).
fof(f582,plain,
! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != g3_lattices(u1_struct_0(sK0),u2_lattices(sK0),u1_lattices(sK0))
| u2_lattices(sK1) = X1
| ~ v1_funct_1(u2_lattices(sK1))
| ~ v1_funct_2(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ m1_relset_1(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ v1_funct_1(u1_lattices(sK1))
| ~ v1_funct_2(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ m1_relset_1(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1)) ),
inference(superposition,[],[f223,f164]) ).
fof(f595,plain,
! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != g3_lattices(u1_struct_0(sK0),u2_lattices(sK0),u1_lattices(sK0))
| u1_struct_0(sK1) = X0
| ~ v1_funct_1(u2_lattices(sK1))
| ~ v1_funct_2(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ m1_relset_1(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ v1_funct_1(u1_lattices(sK1))
| ~ v1_funct_2(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ m1_relset_1(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1)) ),
inference(superposition,[],[f224,f164]) ).
fof(f623,plain,
k2_lattices(sK0,sK4,sK5) = k2_binop_1(u1_struct_0(sK0),u1_struct_0(sK0),u1_struct_0(sK0),u1_lattices(sK0),sK4,sK5),
inference(resolution,[],[f482,f268]) ).
fof(f634,plain,
k2_lattices(sK1,sK4,sK5) = k2_binop_1(u1_struct_0(sK1),u1_struct_0(sK1),u1_struct_0(sK1),u1_lattices(sK1),sK4,sK5),
inference(resolution,[],[f483,f167]) ).
fof(f992,plain,
( ~ l1_lattices(sK1)
| spl26_16 ),
inference(resolution,[],[f409,f557]) ).
fof(f1009,plain,
( $false
| spl26_16 ),
inference(forward_subsumption_resolution,[],[f992,f305]) ).
fof(f1010,plain,
spl26_16,
inference(avatar_contradiction_clause,[],[f1009]) ).
fof(f1128,plain,
( ~ l1_lattices(sK1)
| spl26_17 ),
inference(resolution,[],[f561,f200]) ).
fof(f1129,plain,
( $false
| spl26_17 ),
inference(forward_subsumption_resolution,[],[f1128,f305]) ).
fof(f1130,plain,
spl26_17,
inference(avatar_contradiction_clause,[],[f1129]) ).
fof(f1131,plain,
( ~ l1_lattices(sK1)
| spl26_18 ),
inference(resolution,[],[f565,f201]) ).
fof(f1132,plain,
( $false
| spl26_18 ),
inference(forward_subsumption_resolution,[],[f1131,f305]) ).
fof(f1133,plain,
spl26_18,
inference(avatar_contradiction_clause,[],[f1132]) ).
fof(f1159,plain,
( ~ l2_lattices(sK1)
| spl26_19 ),
inference(resolution,[],[f416,f569]) ).
fof(f1170,plain,
( $false
| spl26_19 ),
inference(forward_subsumption_resolution,[],[f1159,f299]) ).
fof(f1171,plain,
spl26_19,
inference(avatar_contradiction_clause,[],[f1170]) ).
fof(f1183,plain,
( ! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != g3_lattices(u1_struct_0(sK0),u2_lattices(sK0),u1_lattices(sK0))
| u2_lattices(sK1) = X1
| ~ v1_funct_1(u2_lattices(sK1))
| ~ v1_funct_2(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ m1_relset_1(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ v1_funct_2(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ m1_relset_1(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1)) )
| ~ spl26_18 ),
inference(forward_subsumption_resolution,[],[f582,f564]) ).
fof(f1184,plain,
( ! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != g3_lattices(u1_struct_0(sK0),u2_lattices(sK0),u1_lattices(sK0))
| u1_struct_0(sK1) = X0
| ~ v1_funct_1(u2_lattices(sK1))
| ~ v1_funct_2(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ m1_relset_1(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ v1_funct_2(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ m1_relset_1(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1)) )
| ~ spl26_18 ),
inference(forward_subsumption_resolution,[],[f595,f564]) ).
fof(f1188,definition,
( spl26_71
<=> u1_lattices(sK0) = u1_lattices(sK1) ),
introduced(definition,[new_symbols(definition,[spl26_71])],[avatar_definition]) ).
fof(f1190,plain,
( u1_lattices(sK0) = u1_lattices(sK1)
| ~ spl26_71 ),
inference(avatar_component_clause,[],[f1188]) ).
fof(f1193,definition,
( spl26_72
<=> u2_lattices(sK0) = u2_lattices(sK1) ),
introduced(definition,[new_symbols(definition,[spl26_72])],[avatar_definition]) ).
fof(f1195,plain,
( u2_lattices(sK0) = u2_lattices(sK1)
| ~ spl26_72 ),
inference(avatar_component_clause,[],[f1193]) ).
fof(f1198,definition,
( spl26_73
<=> u1_struct_0(sK1) = u1_struct_0(sK0) ),
introduced(definition,[new_symbols(definition,[spl26_73])],[avatar_definition]) ).
fof(f1200,plain,
( u1_struct_0(sK1) = u1_struct_0(sK0)
| ~ spl26_73 ),
inference(avatar_component_clause,[],[f1198]) ).
fof(f1219,plain,
( ! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != g3_lattices(u1_struct_0(sK0),u2_lattices(sK0),u1_lattices(sK0))
| u2_lattices(sK1) = X1
| ~ v1_funct_1(u2_lattices(sK1))
| ~ v1_funct_2(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ m1_relset_1(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ m1_relset_1(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1)) )
| ~ spl26_17
| ~ spl26_18 ),
inference(forward_subsumption_resolution,[],[f1183,f560]) ).
fof(f1220,plain,
( ! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != g3_lattices(u1_struct_0(sK0),u2_lattices(sK0),u1_lattices(sK0))
| u1_struct_0(sK1) = X0
| ~ v1_funct_1(u2_lattices(sK1))
| ~ v1_funct_2(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ m1_relset_1(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ m1_relset_1(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1)) )
| ~ spl26_17
| ~ spl26_18 ),
inference(forward_subsumption_resolution,[],[f1184,f560]) ).
fof(f1248,plain,
( ! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != g3_lattices(u1_struct_0(sK0),u2_lattices(sK0),u1_lattices(sK0))
| u2_lattices(sK1) = X1
| ~ v1_funct_1(u2_lattices(sK1))
| ~ v1_funct_2(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ m1_relset_1(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1)) )
| ~ spl26_16
| ~ spl26_17
| ~ spl26_18 ),
inference(forward_subsumption_resolution,[],[f1219,f556]) ).
fof(f1249,plain,
( ! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != g3_lattices(u1_struct_0(sK0),u2_lattices(sK0),u1_lattices(sK0))
| u1_struct_0(sK1) = X0
| ~ v1_funct_1(u2_lattices(sK1))
| ~ v1_funct_2(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ m1_relset_1(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1)) )
| ~ spl26_16
| ~ spl26_17
| ~ spl26_18 ),
inference(forward_subsumption_resolution,[],[f1220,f556]) ).
fof(f1328,definition,
( spl26_91
<=> ! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != g3_lattices(u1_struct_0(sK0),u2_lattices(sK0),u1_lattices(sK0))
| u2_lattices(sK1) = X1 ) ),
introduced(definition,[new_symbols(definition,[spl26_91])],[avatar_definition]) ).
fof(f1329,plain,
( ! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != g3_lattices(u1_struct_0(sK0),u2_lattices(sK0),u1_lattices(sK0))
| u2_lattices(sK1) = X1 )
| ~ spl26_91 ),
inference(avatar_component_clause,[],[f1328]) ).
fof(f1330,plain,
( ~ spl26_19
| ~ spl26_20
| ~ spl26_21
| spl26_91
| ~ spl26_16
| ~ spl26_17
| ~ spl26_18 ),
inference(avatar_split_clause,[],[f1248,f563,f559,f555,f1328,f575,f571,f567]) ).
fof(f1332,definition,
( spl26_92
<=> ! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != g3_lattices(u1_struct_0(sK0),u2_lattices(sK0),u1_lattices(sK0))
| u1_struct_0(sK1) = X0 ) ),
introduced(definition,[new_symbols(definition,[spl26_92])],[avatar_definition]) ).
fof(f1333,plain,
( ! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != g3_lattices(u1_struct_0(sK0),u2_lattices(sK0),u1_lattices(sK0))
| u1_struct_0(sK1) = X0 )
| ~ spl26_92 ),
inference(avatar_component_clause,[],[f1332]) ).
fof(f1334,plain,
( ~ spl26_19
| ~ spl26_20
| ~ spl26_21
| spl26_92
| ~ spl26_16
| ~ spl26_17
| ~ spl26_18 ),
inference(avatar_split_clause,[],[f1249,f563,f559,f555,f1332,f575,f571,f567]) ).
fof(f1346,plain,
( ~ l2_lattices(sK1)
| spl26_21 ),
inference(resolution,[],[f577,f204]) ).
fof(f1347,plain,
( $false
| spl26_21 ),
inference(forward_subsumption_resolution,[],[f1346,f299]) ).
fof(f1348,plain,
spl26_21,
inference(avatar_contradiction_clause,[],[f1347]) ).
fof(f1401,plain,
( ~ l2_lattices(sK1)
| spl26_20 ),
inference(resolution,[],[f573,f203]) ).
fof(f1402,plain,
( $false
| spl26_20 ),
inference(forward_subsumption_resolution,[],[f1401,f299]) ).
fof(f1403,plain,
spl26_20,
inference(avatar_contradiction_clause,[],[f1402]) ).
fof(f1430,plain,
( u1_lattices(sK0) = u1_lattices(sK1)
| ~ spl26_22 ),
inference(equality_resolution,[],[f580]) ).
fof(f1431,plain,
( spl26_71
| ~ spl26_22 ),
inference(avatar_split_clause,[],[f1430,f579,f1188]) ).
fof(f1456,plain,
( u2_lattices(sK0) = u2_lattices(sK1)
| ~ spl26_91 ),
inference(equality_resolution,[],[f1329]) ).
fof(f1457,plain,
( spl26_72
| ~ spl26_91 ),
inference(avatar_split_clause,[],[f1456,f1328,f1193]) ).
fof(f1462,plain,
( u1_struct_0(sK1) = u1_struct_0(sK0)
| ~ spl26_92 ),
inference(equality_resolution,[],[f1333]) ).
fof(f1463,plain,
( spl26_73
| ~ spl26_92 ),
inference(avatar_split_clause,[],[f1462,f1332,f1198]) ).
fof(f1502,plain,
( k1_lattices(sK1,sK4,sK5) = k2_binop_1(u1_struct_0(sK0),u1_struct_0(sK0),u1_struct_0(sK0),u2_lattices(sK1),sK4,sK5)
| ~ spl26_73 ),
inference(superposition,[],[f541,f1200]) ).
fof(f1513,plain,
( k2_lattices(sK1,sK4,sK5) = k2_binop_1(u1_struct_0(sK0),u1_struct_0(sK0),u1_struct_0(sK0),u1_lattices(sK1),sK4,sK5)
| ~ spl26_73 ),
inference(superposition,[],[f634,f1200]) ).
fof(f1554,plain,
( k2_lattices(sK1,sK4,sK5) = k2_binop_1(u1_struct_0(sK0),u1_struct_0(sK0),u1_struct_0(sK0),u1_lattices(sK0),sK4,sK5)
| ~ spl26_71
| ~ spl26_73 ),
inference(forward_demodulation,[],[f1513,f1190]) ).
fof(f1564,plain,
( k1_lattices(sK1,sK4,sK5) = k2_binop_1(u1_struct_0(sK0),u1_struct_0(sK0),u1_struct_0(sK0),u2_lattices(sK0),sK4,sK5)
| ~ spl26_72
| ~ spl26_73 ),
inference(forward_demodulation,[],[f1502,f1195]) ).
fof(f1587,plain,
( k2_lattices(sK1,sK4,sK5) = k2_lattices(sK0,sK4,sK5)
| ~ spl26_71
| ~ spl26_73 ),
inference(forward_demodulation,[],[f1554,f623]) ).
fof(f1597,plain,
( k1_lattices(sK1,sK4,sK5) = k1_lattices(sK0,sK4,sK5)
| ~ spl26_72
| ~ spl26_73 ),
inference(forward_demodulation,[],[f1564,f488]) ).
fof(f1604,plain,
( spl26_3
| ~ spl26_71
| ~ spl26_73 ),
inference(avatar_split_clause,[],[f1587,f1198,f1188,f279]) ).
fof(f1607,plain,
( spl26_4
| ~ spl26_72
| ~ spl26_73 ),
inference(avatar_split_clause,[],[f1597,f1198,f1193,f283]) ).
fof(f1608,plain,
( sK5 = k1_lattices(sK1,sK4,sK5)
| ~ m1_subset_1(sK5,u1_struct_0(sK1))
| ~ m1_subset_1(sK4,u1_struct_0(sK1))
| v3_struct_0(sK1)
| ~ l2_lattices(sK1)
| ~ spl26_1 ),
inference(resolution,[],[f273,f186]) ).
fof(f1609,plain,
( sK5 = k1_lattices(sK1,sK4,sK5)
| ~ m1_subset_1(sK4,u1_struct_0(sK1))
| v3_struct_0(sK1)
| ~ l2_lattices(sK1)
| ~ spl26_1 ),
inference(forward_subsumption_resolution,[],[f1608,f168]) ).
fof(f1610,plain,
( sK5 = k1_lattices(sK1,sK4,sK5)
| v3_struct_0(sK1)
| ~ l2_lattices(sK1)
| ~ spl26_1 ),
inference(forward_subsumption_resolution,[],[f1609,f167]) ).
fof(f1611,plain,
( sK5 = k1_lattices(sK1,sK4,sK5)
| ~ l2_lattices(sK1)
| ~ spl26_1 ),
inference(forward_subsumption_resolution,[],[f1610,f163]) ).
fof(f1612,plain,
( sK5 = k1_lattices(sK1,sK4,sK5)
| ~ spl26_1 ),
inference(forward_subsumption_resolution,[],[f1611,f299]) ).
fof(f1627,plain,
( sK5 = k1_lattices(sK0,sK4,sK5)
| ~ spl26_1
| ~ spl26_4 ),
inference(forward_demodulation,[],[f284,f1612]) ).
fof(f1629,plain,
( sK5 != sK5
| r1_lattices(sK0,sK4,sK5)
| ~ m1_subset_1(sK5,u1_struct_0(sK0))
| ~ m1_subset_1(sK4,u1_struct_0(sK0))
| v3_struct_0(sK0)
| ~ l2_lattices(sK0)
| ~ spl26_1
| ~ spl26_4 ),
inference(superposition,[],[f187,f1627]) ).
fof(f1631,plain,
( r1_lattices(sK0,sK4,sK5)
| ~ m1_subset_1(sK5,u1_struct_0(sK0))
| ~ m1_subset_1(sK4,u1_struct_0(sK0))
| v3_struct_0(sK0)
| ~ l2_lattices(sK0)
| ~ spl26_1
| ~ spl26_4 ),
inference(trivial_inequality_removal,[],[f1629]) ).
fof(f1632,plain,
( ~ m1_subset_1(sK5,u1_struct_0(sK0))
| ~ m1_subset_1(sK4,u1_struct_0(sK0))
| v3_struct_0(sK0)
| ~ l2_lattices(sK0)
| ~ spl26_1
| spl26_2
| ~ spl26_4 ),
inference(forward_subsumption_resolution,[],[f1631,f276]) ).
fof(f1633,plain,
( ~ m1_subset_1(sK4,u1_struct_0(sK0))
| v3_struct_0(sK0)
| ~ l2_lattices(sK0)
| ~ spl26_1
| spl26_2
| ~ spl26_4 ),
inference(forward_subsumption_resolution,[],[f1632,f267]) ).
fof(f1634,plain,
( v3_struct_0(sK0)
| ~ l2_lattices(sK0)
| ~ spl26_1
| spl26_2
| ~ spl26_4 ),
inference(forward_subsumption_resolution,[],[f1633,f268]) ).
fof(f1635,plain,
( ~ l2_lattices(sK0)
| ~ spl26_1
| spl26_2
| ~ spl26_4 ),
inference(forward_subsumption_resolution,[],[f1634,f161]) ).
fof(f1636,plain,
( $false
| ~ spl26_1
| spl26_2
| ~ spl26_4 ),
inference(forward_subsumption_resolution,[],[f1635,f298]) ).
fof(f1637,plain,
( ~ spl26_1
| spl26_2
| ~ spl26_4 ),
inference(avatar_contradiction_clause,[],[f1636]) ).
fof(f1638,plain,
( sK5 = k1_lattices(sK0,sK4,sK5)
| ~ m1_subset_1(sK5,u1_struct_0(sK0))
| ~ m1_subset_1(sK4,u1_struct_0(sK0))
| v3_struct_0(sK0)
| ~ l2_lattices(sK0)
| ~ spl26_2 ),
inference(resolution,[],[f277,f186]) ).
fof(f1639,plain,
( sK5 = k1_lattices(sK0,sK4,sK5)
| ~ m1_subset_1(sK4,u1_struct_0(sK0))
| v3_struct_0(sK0)
| ~ l2_lattices(sK0)
| ~ spl26_2 ),
inference(forward_subsumption_resolution,[],[f1638,f267]) ).
fof(f1640,plain,
( sK5 = k1_lattices(sK0,sK4,sK5)
| v3_struct_0(sK0)
| ~ l2_lattices(sK0)
| ~ spl26_2 ),
inference(forward_subsumption_resolution,[],[f1639,f268]) ).
fof(f1641,plain,
( sK5 = k1_lattices(sK0,sK4,sK5)
| ~ l2_lattices(sK0)
| ~ spl26_2 ),
inference(forward_subsumption_resolution,[],[f1640,f161]) ).
fof(f1642,plain,
( sK5 = k1_lattices(sK0,sK4,sK5)
| ~ spl26_2 ),
inference(forward_subsumption_resolution,[],[f1641,f298]) ).
fof(f1644,plain,
( sK5 != k1_lattices(sK0,sK4,sK5)
| r1_lattices(sK1,sK4,sK5)
| ~ m1_subset_1(sK5,u1_struct_0(sK1))
| ~ m1_subset_1(sK4,u1_struct_0(sK1))
| v3_struct_0(sK1)
| ~ l2_lattices(sK1)
| ~ spl26_4 ),
inference(superposition,[],[f187,f284]) ).
fof(f1647,plain,
( sK5 != k1_lattices(sK0,sK4,sK5)
| ~ m1_subset_1(sK5,u1_struct_0(sK1))
| ~ m1_subset_1(sK4,u1_struct_0(sK1))
| v3_struct_0(sK1)
| ~ l2_lattices(sK1)
| spl26_1
| ~ spl26_4 ),
inference(forward_subsumption_resolution,[],[f1644,f272]) ).
fof(f1650,plain,
( sK5 != k1_lattices(sK0,sK4,sK5)
| ~ m1_subset_1(sK4,u1_struct_0(sK1))
| v3_struct_0(sK1)
| ~ l2_lattices(sK1)
| spl26_1
| ~ spl26_4 ),
inference(forward_subsumption_resolution,[],[f1647,f168]) ).
fof(f1653,plain,
( sK5 != k1_lattices(sK0,sK4,sK5)
| v3_struct_0(sK1)
| ~ l2_lattices(sK1)
| spl26_1
| ~ spl26_4 ),
inference(forward_subsumption_resolution,[],[f1650,f167]) ).
fof(f1655,plain,
( sK5 != k1_lattices(sK0,sK4,sK5)
| ~ l2_lattices(sK1)
| spl26_1
| ~ spl26_4 ),
inference(forward_subsumption_resolution,[],[f1653,f163]) ).
fof(f1657,plain,
( sK5 != k1_lattices(sK0,sK4,sK5)
| spl26_1
| ~ spl26_4 ),
inference(forward_subsumption_resolution,[],[f1655,f299]) ).
fof(f1663,plain,
( $false
| spl26_1
| ~ spl26_2
| ~ spl26_4 ),
inference(forward_subsumption_resolution,[],[f1657,f1642]) ).
fof(f1664,plain,
( spl26_1
| ~ spl26_2
| ~ spl26_4 ),
inference(avatar_contradiction_clause,[],[f1663]) ).
cnf(s1,plain,
( spl26_1
| spl26_2
| ~ spl26_3
| ~ spl26_4 ),
inference(sat_conversion,[],[f286]) ).
cnf(s2,plain,
( ~ spl26_1
| ~ spl26_2
| ~ spl26_3
| ~ spl26_4 ),
inference(sat_conversion,[],[f287]) ).
cnf(s11,plain,
( ~ spl26_16
| ~ spl26_17
| ~ spl26_18
| ~ spl26_19
| ~ spl26_20
| ~ spl26_21
| spl26_22 ),
inference(sat_conversion,[],[f581]) ).
cnf(s33,plain,
spl26_16,
inference(sat_conversion,[],[f1010]) ).
cnf(s51,plain,
spl26_17,
inference(sat_conversion,[],[f1130]) ).
cnf(s52,plain,
spl26_18,
inference(sat_conversion,[],[f1133]) ).
cnf(s53,plain,
spl26_19,
inference(sat_conversion,[],[f1171]) ).
cnf(s74,plain,
( ~ spl26_16
| ~ spl26_17
| ~ spl26_18
| ~ spl26_19
| ~ spl26_20
| ~ spl26_21
| spl26_91 ),
inference(sat_conversion,[],[f1330]) ).
cnf(s75,plain,
( ~ spl26_16
| ~ spl26_17
| ~ spl26_18
| ~ spl26_19
| ~ spl26_20
| ~ spl26_21
| spl26_92 ),
inference(sat_conversion,[],[f1334]) ).
cnf(s79,plain,
spl26_21,
inference(sat_conversion,[],[f1348]) ).
cnf(s84,plain,
spl26_20,
inference(sat_conversion,[],[f1403]) ).
cnf(s85,plain,
( ~ spl26_22
| spl26_71 ),
inference(sat_conversion,[],[f1431]) ).
cnf(s90,plain,
( spl26_72
| ~ spl26_91 ),
inference(sat_conversion,[],[f1457]) ).
cnf(s93,plain,
( spl26_73
| ~ spl26_92 ),
inference(sat_conversion,[],[f1463]) ).
cnf(s106,plain,
( spl26_3
| ~ spl26_71
| ~ spl26_73 ),
inference(sat_conversion,[],[f1604]) ).
cnf(s108,plain,
( spl26_4
| ~ spl26_72
| ~ spl26_73 ),
inference(sat_conversion,[],[f1607]) ).
cnf(s111,plain,
( ~ spl26_1
| spl26_2
| ~ spl26_4 ),
inference(sat_conversion,[],[f1637]) ).
cnf(s114,plain,
( spl26_1
| ~ spl26_2
| ~ spl26_4 ),
inference(sat_conversion,[],[f1664]) ).
cnf(s119,plain,
( ~ spl26_16
| ~ spl26_17
| ~ spl26_18
| ~ spl26_19
| spl26_92 ),
inference(rat,[],[s75,s79,s84]) ).
cnf(s120,plain,
( ~ spl26_16
| ~ spl26_17
| ~ spl26_18
| ~ spl26_19
| spl26_91 ),
inference(rat,[],[s74,s79,s84]) ).
cnf(s138,plain,
spl26_92,
inference(rat,[],[s119,s51,s53,s52,s33]) ).
cnf(s139,plain,
spl26_91,
inference(rat,[],[s120,s51,s53,s52,s33]) ).
cnf(s142,plain,
spl26_73,
inference(rat,[],[s93,s138]) ).
cnf(s143,plain,
spl26_72,
inference(rat,[],[s90,s139]) ).
cnf(s144,plain,
spl26_4,
inference(rat,[],[s108,s142,s143]) ).
cnf(s163,plain,
spl26_22,
inference(rat,[],[s11,s79,s84,s53,s52,s51,s33]) ).
cnf(s164,plain,
spl26_71,
inference(rat,[],[s85,s163]) ).
cnf(s165,plain,
spl26_3,
inference(rat,[],[s106,s142,s164]) ).
cnf(s211,plain,
( ~ spl26_1
| ~ spl26_2 ),
inference(rat,[],[s2,s144,s165]) ).
cnf(s212,plain,
( spl26_1
| spl26_2 ),
inference(rat,[],[s1,s144,s165]) ).
cnf(s213,plain,
spl26_1,
inference(rat,[],[s212,s114,s144]) ).
cnf(s214,plain,
spl26_2,
inference(rat,[],[s111,s144,s213]) ).
cnf(s215,plain,
$false,
inference(rat,[],[s211,s214,s213]) ).
fof(f1665,plain,
$false,
inference(avatar_sat_refutation,[],[s215]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT295+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.39 % Computer : n013.cluster.edu
% 0.12/0.39 % Model : x86_64 x86_64
% 0.12/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.39 % Memory : 8046.5625MB
% 0.12/0.39 % OS : Linux 6.8.0-71-generic
% 0.12/0.39 % CPULimit : 300
% 0.12/0.39 % WCLimit : 300
% 0.12/0.39 % DateTime : Sun Sep 27 14:19:07 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.42 Running first-order model finding
% 0.12/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.51 % (277533)Will run a generic schedule for satisfiability detection.
% 0.19/0.51 % (277542)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=218009025:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.19/0.51 % (277539)% WARNING: option uhcvi not known.
% 0.19/0.51 % (277539)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1764832933:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.19/0.51 % (277538)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3917350878_2999 on theBenchmark for (2999ds/0Mi)
% 0.19/0.51 % (277543)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=52042222:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.19/0.51 % (277540)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4006680587:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.19/0.51 % (277541)dis+10_1_sil=32000:sp=arity:random_seed=2065536723:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.19/0.51 % (277544)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=41423157:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.19/0.51 % TRYING [1]
% 0.19/0.51 % TRYING [2]
% 0.19/0.51 % TRYING [3]
% 0.19/0.51 % (277542)Instruction limit reached!
% 0.19/0.51 % (277542)------------------------------
% 0.19/0.51 % (277542)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.51 % (277542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.51 % (277542)CaDiCaL version: 2.1.3
% 0.19/0.51 % (277542)Termination reason: Instruction limit
% 0.19/0.51 % (277542)Termination phase: Saturation
% 0.19/0.51 % (277542)Time elapsed: 0.041 s
% 0.19/0.51 % (277542)Peak memory usage: 13 MB
% 0.19/0.51 % (277542)Instructions burned: 118 (million)
% 0.19/0.51 % (277541) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-277533-277541"...
% 0.19/0.51 % (277541)...printing done.
% 0.19/0.51 % (277541)Refutation found. Thanks to Tanya!
% 0.19/0.51 % SZS status Theorem for theBenchmark
% 0.19/0.51 % SZS output start Proof for theBenchmark
% See solution above
% 0.19/0.51 % (277541)------------------------------
% 0.19/0.51 % (277541)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.51 % (277541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.51 % (277541)CaDiCaL version: 2.1.3
% 0.19/0.51 % (277541)Termination reason: Refutation
% 0.19/0.51 % (277541)Time elapsed: 0.039 s
% 0.19/0.51 % (277541)Peak memory usage: 13 MB
% 0.19/0.51 % (277541)Instructions burned: 61 (million)
% 0.19/0.51 % (277533)Success in time 0.077 s
% 0.19/0.51 % Vampire exiting
%------------------------------------------------------------------------------