%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT322+4 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n012.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:55 AM UTC 2026
% Result : Theorem 18.52s 4.35s
% Output : Refutation 21.81s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 39
% Syntax : Number of formulae : 328 ( 27 unt; 20 def)
% Number of atoms : 1609 ( 87 equ)
% Maximal formula atoms : 19 ( 4 avg)
% Number of connectives : 2136 ( 855 ~;1029 |; 177 &)
% ( 43 <=>; 30 =>; 0 <=; 2 <~>)
% Maximal formula depth : 14 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 44 ( 42 usr; 21 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 2 con; 0-2 aty)
% Number of variables : 167 ( 0 sgn 156 !; 11 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f21516,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> k1_filter_0(X0) = u1_struct_0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d2_filter_0) ).
fof(f21563,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_filter_0(X1,X0)
=> ( ( X1 != k1_filter_0(X0)
& v2_filter_0(X1,X0) )
<=> v1_filter_0(X1,X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t58_filter_0) ).
fof(f22747,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l3_lattices(X0) )
=> ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_lattice2) ).
fof(f22752,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v4_lattices(k1_lattice2(X0))
& v5_lattices(k1_lattice2(X0))
& v6_lattices(k1_lattice2(X0))
& v7_lattices(k1_lattice2(X0))
& v8_lattices(k1_lattice2(X0))
& v9_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc6_lattice2) ).
fof(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/sandbox/benchmark/theBenchmark.p',t18_lattice2) ).
fof(f22852,axiom,
! [X0] :
( l3_lattices(X0)
=> ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k1_lattice2) ).
fof(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/sandbox/benchmark/theBenchmark.p',dt_m2_lattice4) ).
fof(f34606,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_filter_2(X1,X0)
<=> m1_filter_0(X1,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_m1_filter_2) ).
fof(f34607,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_filter_2(X1,X0)
=> ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m2_filter_2) ).
fof(f34636,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& m2_filter_2(X1,X0) )
=> m1_filter_2(k15_filter_2(X0,X1),k1_lattice2(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k15_filter_2) ).
fof(f34637,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& m2_filter_2(X1,X0) )
=> k15_filter_2(X0,X1) = k7_filter_2(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k15_filter_2) ).
fof(f34675,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_filter_2(X1,X0)
<=> m1_filter_2(X1,k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t21_filter_2) ).
fof(f34676,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
=> k7_filter_2(X0,X1) = X1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d6_filter_2) ).
fof(f34687,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> k17_filter_2(X0) = u1_struct_0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d8_filter_2) ).
fof(f34694,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_filter_2(X1,X0)
=> ( r2_filter_2(X0,X1)
<=> v1_filter_0(k15_filter_2(X0,X1),k1_lattice2(X0)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t33_filter_2) ).
fof(f34708,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_filter_2(X1,X0)
=> ( v1_filter_2(X1,X0)
<=> v2_filter_0(k15_filter_2(X0,X1),k1_lattice2(X0)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t44_filter_2) ).
fof(f34721,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) )
<=> ( ~ v3_struct_0(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v17_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t54_filter_2) ).
fof(f34726,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_filter_2(X1,X0)
=> ( r2_filter_2(X0,X1)
<=> ( X1 != u1_struct_0(X0)
& ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ( r2_hidden(X2,X1)
| r2_hidden(k7_lattices(X0,X2),X1) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t57_filter_2) ).
fof(f34727,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_filter_2(X1,X0)
=> ( ( X1 != k17_filter_2(X0)
& v1_filter_2(X1,X0) )
<=> r2_filter_2(X0,X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t58_filter_2) ).
fof(f34728,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_filter_2(X1,X0)
=> ( ( X1 != k17_filter_2(X0)
& v1_filter_2(X1,X0) )
<=> r2_filter_2(X0,X1) ) ) ),
inference(negated_conjecture,[status(cth)],[f34727]) ).
fof(f34764,plain,
! [X0] :
( ! [X1] :
( m1_filter_2(X1,X0)
<=> m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f34606]) ).
fof(f34765,plain,
! [X0] :
( ! [X1] :
( m1_filter_2(X1,X0)
<=> m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f34764]) ).
fof(f34766,plain,
! [X0] :
( ! [X1] :
( ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f34607]) ).
fof(f34767,plain,
! [X0] :
( ! [X1] :
( ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f34766]) ).
fof(f34824,plain,
! [X0,X1] :
( m1_filter_2(k15_filter_2(X0,X1),k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m2_filter_2(X1,X0) ),
inference(ennf_transformation,[],[f34636]) ).
fof(f34825,plain,
! [X0,X1] :
( m1_filter_2(k15_filter_2(X0,X1),k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m2_filter_2(X1,X0) ),
inference(flattening,[],[f34824]) ).
fof(f34826,plain,
! [X0,X1] :
( k15_filter_2(X0,X1) = k7_filter_2(X0,X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m2_filter_2(X1,X0) ),
inference(ennf_transformation,[],[f34637]) ).
fof(f34827,plain,
! [X0,X1] :
( k15_filter_2(X0,X1) = k7_filter_2(X0,X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m2_filter_2(X1,X0) ),
inference(flattening,[],[f34826]) ).
fof(f34899,plain,
! [X0] :
( ! [X1] :
( m2_filter_2(X1,X0)
<=> m1_filter_2(X1,k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f34675]) ).
fof(f34900,plain,
! [X0] :
( ! [X1] :
( m2_filter_2(X1,X0)
<=> m1_filter_2(X1,k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f34899]) ).
fof(f34901,plain,
! [X0] :
( ! [X1] :
( k7_filter_2(X0,X1) = X1
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f34676]) ).
fof(f34902,plain,
! [X0] :
( ! [X1] :
( k7_filter_2(X0,X1) = X1
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f34901]) ).
fof(f34923,plain,
! [X0] :
( k17_filter_2(X0) = u1_struct_0(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f34687]) ).
fof(f34924,plain,
! [X0] :
( k17_filter_2(X0) = u1_struct_0(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f34923]) ).
fof(f34937,plain,
! [X0] :
( ! [X1] :
( ( r2_filter_2(X0,X1)
<=> v1_filter_0(k15_filter_2(X0,X1),k1_lattice2(X0)) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f34694]) ).
fof(f34938,plain,
! [X0] :
( ! [X1] :
( ( r2_filter_2(X0,X1)
<=> v1_filter_0(k15_filter_2(X0,X1),k1_lattice2(X0)) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f34937]) ).
fof(f34965,plain,
! [X0] :
( ! [X1] :
( ( v1_filter_2(X1,X0)
<=> v2_filter_0(k15_filter_2(X0,X1),k1_lattice2(X0)) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f34708]) ).
fof(f34966,plain,
! [X0] :
( ! [X1] :
( ( v1_filter_2(X1,X0)
<=> v2_filter_0(k15_filter_2(X0,X1),k1_lattice2(X0)) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f34965]) ).
fof(f34991,plain,
! [X0] :
( ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) )
<=> ( ~ v3_struct_0(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v17_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f34721]) ).
fof(f34992,plain,
! [X0] :
( ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) )
<=> ( ~ v3_struct_0(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v17_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f34991]) ).
fof(f35001,plain,
! [X0] :
( ! [X1] :
( ( r2_filter_2(X0,X1)
<=> ( X1 != u1_struct_0(X0)
& ! [X2] :
( r2_hidden(X2,X1)
| r2_hidden(k7_lattices(X0,X2),X1)
| ~ m1_subset_1(X2,u1_struct_0(X0)) ) ) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f34726]) ).
fof(f35002,plain,
! [X0] :
( ! [X1] :
( ( r2_filter_2(X0,X1)
<=> ( X1 != u1_struct_0(X0)
& ! [X2] :
( r2_hidden(X2,X1)
| r2_hidden(k7_lattices(X0,X2),X1)
| ~ m1_subset_1(X2,u1_struct_0(X0)) ) ) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35001]) ).
fof(f35003,plain,
? [X0] :
( ? [X1] :
( ( ( X1 != k17_filter_2(X0)
& v1_filter_2(X1,X0) )
<~> r2_filter_2(X0,X1) )
& m2_filter_2(X1,X0) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) ),
inference(ennf_transformation,[],[f34728]) ).
fof(f35004,plain,
? [X0] :
( ? [X1] :
( ( ( X1 != k17_filter_2(X0)
& v1_filter_2(X1,X0) )
<~> r2_filter_2(X0,X1) )
& m2_filter_2(X1,X0) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) ),
inference(flattening,[],[f35003]) ).
fof(f35014,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(f35015,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,[],[f35014]) ).
fof(f35059,plain,
! [X0] :
( k1_filter_0(X0) = u1_struct_0(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f21516]) ).
fof(f35060,plain,
! [X0] :
( k1_filter_0(X0) = u1_struct_0(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35059]) ).
fof(f35109,plain,
! [X0] :
( ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f22852]) ).
fof(f35126,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(f35127,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,[],[f35126]) ).
fof(f35129,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(f35130,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35129]) ).
fof(f35499,plain,
! [X0] :
( ! [X1] :
( ( ( X1 != k1_filter_0(X0)
& v2_filter_0(X1,X0) )
<=> v1_filter_0(X1,X0) )
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f21563]) ).
fof(f35500,plain,
! [X0] :
( ! [X1] :
( ( ( X1 != k1_filter_0(X0)
& v2_filter_0(X1,X0) )
<=> v1_filter_0(X1,X0) )
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35499]) ).
fof(f35519,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(f35520,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,[],[f35519]) ).
fof(f35544,plain,
! [X0] :
( ! [X1] :
( ( m1_filter_2(X1,X0)
| ~ m1_filter_0(X1,X0) )
& ( m1_filter_0(X1,X0)
| ~ m1_filter_2(X1,X0) ) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f34765]) ).
fof(f35564,plain,
! [X0] :
( ! [X1] :
( ( m2_filter_2(X1,X0)
| ~ m1_filter_2(X1,k1_lattice2(X0)) )
& ( m1_filter_2(X1,k1_lattice2(X0))
| ~ m2_filter_2(X1,X0) ) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f34900]) ).
fof(f35575,plain,
! [X0] :
( ! [X1] :
( ( ( r2_filter_2(X0,X1)
| ~ v1_filter_0(k15_filter_2(X0,X1),k1_lattice2(X0)) )
& ( v1_filter_0(k15_filter_2(X0,X1),k1_lattice2(X0))
| ~ r2_filter_2(X0,X1) ) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f34938]) ).
fof(f35586,plain,
! [X0] :
( ! [X1] :
( ( ( v1_filter_2(X1,X0)
| ~ v2_filter_0(k15_filter_2(X0,X1),k1_lattice2(X0)) )
& ( v2_filter_0(k15_filter_2(X0,X1),k1_lattice2(X0))
| ~ v1_filter_2(X1,X0) ) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f34966]) ).
fof(f35590,plain,
! [X0] :
( ( ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) )
| v3_struct_0(k1_lattice2(X0))
| ~ v10_lattices(k1_lattice2(X0))
| ~ v17_lattices(k1_lattice2(X0))
| ~ l3_lattices(k1_lattice2(X0)) )
& ( ( ~ v3_struct_0(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v17_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f34992]) ).
fof(f35591,plain,
! [X0] :
( ( ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) )
| v3_struct_0(k1_lattice2(X0))
| ~ v10_lattices(k1_lattice2(X0))
| ~ v17_lattices(k1_lattice2(X0))
| ~ l3_lattices(k1_lattice2(X0)) )
& ( ( ~ v3_struct_0(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v17_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35590]) ).
fof(f35592,plain,
! [X0] :
( ! [X1] :
( ( ( r2_filter_2(X0,X1)
| u1_struct_0(X0) = X1
| ? [X2] :
( ~ r2_hidden(X2,X1)
& ~ r2_hidden(k7_lattices(X0,X2),X1)
& m1_subset_1(X2,u1_struct_0(X0)) ) )
& ( ( X1 != u1_struct_0(X0)
& ! [X2] :
( r2_hidden(X2,X1)
| r2_hidden(k7_lattices(X0,X2),X1)
| ~ m1_subset_1(X2,u1_struct_0(X0)) ) )
| ~ r2_filter_2(X0,X1) ) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f35002]) ).
fof(f35593,plain,
! [X0] :
( ! [X1] :
( ( ( r2_filter_2(X0,X1)
| u1_struct_0(X0) = X1
| ? [X2] :
( ~ r2_hidden(X2,X1)
& ~ r2_hidden(k7_lattices(X0,X2),X1)
& m1_subset_1(X2,u1_struct_0(X0)) ) )
& ( ( X1 != u1_struct_0(X0)
& ! [X2] :
( r2_hidden(X2,X1)
| r2_hidden(k7_lattices(X0,X2),X1)
| ~ m1_subset_1(X2,u1_struct_0(X0)) ) )
| ~ r2_filter_2(X0,X1) ) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35592]) ).
fof(f35594,plain,
! [X0] :
( ! [X1] :
( ( ( r2_filter_2(X0,X1)
| u1_struct_0(X0) = X1
| ? [X2] :
( ~ r2_hidden(X2,X1)
& ~ r2_hidden(k7_lattices(X0,X2),X1)
& m1_subset_1(X2,u1_struct_0(X0)) ) )
& ( ( X1 != u1_struct_0(X0)
& ! [X3] :
( r2_hidden(X3,X1)
| r2_hidden(k7_lattices(X0,X3),X1)
| ~ m1_subset_1(X3,u1_struct_0(X0)) ) )
| ~ r2_filter_2(X0,X1) ) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(rectify,[],[f35593]) ).
fof(f35595,plain,
! [X0] :
( ! [X1] :
( ( ( r2_filter_2(X0,X1)
| u1_struct_0(X0) = X1
| ( ~ r2_hidden(sK25(X0,X1),X1)
& ~ r2_hidden(k7_lattices(X0,sK25(X0,X1)),X1)
& m1_subset_1(sK25(X0,X1),u1_struct_0(X0)) ) )
& ( ( X1 != u1_struct_0(X0)
& ! [X3] :
( r2_hidden(X3,X1)
| r2_hidden(k7_lattices(X0,X3),X1)
| ~ m1_subset_1(X3,u1_struct_0(X0)) ) )
| ~ r2_filter_2(X0,X1) ) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK25]),skolemize(X2,sK25(X0,X1))],[f35594]) ).
fof(f35596,plain,
? [X0] :
( ? [X1] :
( ( ~ r2_filter_2(X0,X1)
| k17_filter_2(X0) = X1
| ~ v1_filter_2(X1,X0) )
& ( r2_filter_2(X0,X1)
| ( X1 != k17_filter_2(X0)
& v1_filter_2(X1,X0) ) )
& m2_filter_2(X1,X0) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) ),
inference(nnf_transformation,[],[f35004]) ).
fof(f35597,plain,
? [X0] :
( ? [X1] :
( ( ~ r2_filter_2(X0,X1)
| k17_filter_2(X0) = X1
| ~ v1_filter_2(X1,X0) )
& ( r2_filter_2(X0,X1)
| ( X1 != k17_filter_2(X0)
& v1_filter_2(X1,X0) ) )
& m2_filter_2(X1,X0) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) ),
inference(flattening,[],[f35596]) ).
fof(f35598,plain,
( ( ~ r2_filter_2(sK26,sK27)
| sK27 = k17_filter_2(sK26)
| ~ v1_filter_2(sK27,sK26) )
& ( r2_filter_2(sK26,sK27)
| ( sK27 != k17_filter_2(sK26)
& v1_filter_2(sK27,sK26) ) )
& m2_filter_2(sK27,sK26)
& ~ v3_struct_0(sK26)
& v10_lattices(sK26)
& v17_lattices(sK26)
& l3_lattices(sK26) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK26,sK27]),skolemize(X0,sK26),skolemize(X1,sK27)],[f35597]) ).
fof(f35824,plain,
! [X0] :
( ! [X1] :
( ( ( ( X1 != k1_filter_0(X0)
& v2_filter_0(X1,X0) )
| ~ v1_filter_0(X1,X0) )
& ( v1_filter_0(X1,X0)
| k1_filter_0(X0) = X1
| ~ v2_filter_0(X1,X0) ) )
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f35500]) ).
fof(f35825,plain,
! [X0] :
( ! [X1] :
( ( ( ( X1 != k1_filter_0(X0)
& v2_filter_0(X1,X0) )
| ~ v1_filter_0(X1,X0) )
& ( v1_filter_0(X1,X0)
| k1_filter_0(X0) = X1
| ~ v2_filter_0(X1,X0) ) )
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35824]) ).
fof(f35848,plain,
! [X0,X1] :
( m1_filter_0(X1,X0)
| ~ m1_filter_2(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35544]) ).
fof(f35850,plain,
! [X0,X1] :
( m2_lattice4(X1,X0)
| ~ m2_filter_2(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f34767]) ).
fof(f35883,plain,
! [X0,X1] :
( m1_filter_2(k15_filter_2(X0,X1),k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m2_filter_2(X1,X0) ),
inference(cnf_transformation,[],[f34825]) ).
fof(f35884,plain,
! [X0,X1] :
( k7_filter_2(X0,X1) = k15_filter_2(X0,X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m2_filter_2(X1,X0) ),
inference(cnf_transformation,[],[f34827]) ).
fof(f35961,plain,
! [X0,X1] :
( m1_filter_2(X1,k1_lattice2(X0))
| ~ m2_filter_2(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35564]) ).
fof(f35963,plain,
! [X0,X1] :
( k7_filter_2(X0,X1) = X1
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f34902]) ).
fof(f36002,plain,
! [X0] :
( u1_struct_0(X0) = k17_filter_2(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f34924]) ).
fof(f36018,plain,
! [X0,X1] :
( v1_filter_0(k15_filter_2(X0,X1),k1_lattice2(X0))
| ~ r2_filter_2(X0,X1)
| ~ m2_filter_2(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35575]) ).
fof(f36019,plain,
! [X0,X1] :
( r2_filter_2(X0,X1)
| ~ v1_filter_0(k15_filter_2(X0,X1),k1_lattice2(X0))
| ~ m2_filter_2(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35575]) ).
fof(f36055,plain,
! [X0,X1] :
( v2_filter_0(k15_filter_2(X0,X1),k1_lattice2(X0))
| ~ v1_filter_2(X1,X0)
| ~ m2_filter_2(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35586]) ).
fof(f36056,plain,
! [X0,X1] :
( v1_filter_2(X1,X0)
| ~ v2_filter_0(k15_filter_2(X0,X1),k1_lattice2(X0))
| ~ m2_filter_2(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35586]) ).
fof(f36089,plain,
! [X0] :
( v17_lattices(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35591]) ).
fof(f36117,plain,
! [X0,X1] :
( u1_struct_0(X0) != X1
| ~ r2_filter_2(X0,X1)
| ~ m2_filter_2(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35595]) ).
fof(f36121,plain,
l3_lattices(sK26),
inference(cnf_transformation,[],[f35598]) ).
fof(f36122,plain,
v17_lattices(sK26),
inference(cnf_transformation,[],[f35598]) ).
fof(f36123,plain,
v10_lattices(sK26),
inference(cnf_transformation,[],[f35598]) ).
fof(f36124,plain,
~ v3_struct_0(sK26),
inference(cnf_transformation,[],[f35598]) ).
fof(f36125,plain,
m2_filter_2(sK27,sK26),
inference(cnf_transformation,[],[f35598]) ).
fof(f36126,plain,
( r2_filter_2(sK26,sK27)
| v1_filter_2(sK27,sK26) ),
inference(cnf_transformation,[],[f35598]) ).
fof(f36127,plain,
( r2_filter_2(sK26,sK27)
| sK27 != k17_filter_2(sK26) ),
inference(cnf_transformation,[],[f35598]) ).
fof(f36128,plain,
( ~ r2_filter_2(sK26,sK27)
| sK27 = k17_filter_2(sK26)
| ~ v1_filter_2(sK27,sK26) ),
inference(cnf_transformation,[],[f35598]) ).
fof(f36142,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,[],[f35015]) ).
fof(f36225,plain,
! [X0] :
( u1_struct_0(X0) = k1_filter_0(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35060]) ).
fof(f36267,plain,
! [X0] :
( l3_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35109]) ).
fof(f36290,plain,
! [X0] :
( u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35127]) ).
fof(f36293,plain,
! [X0] :
( ~ v3_struct_0(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35130]) ).
fof(f36814,plain,
! [X0,X1] :
( v1_filter_0(X1,X0)
| k1_filter_0(X0) = X1
| ~ v2_filter_0(X1,X0)
| ~ m1_filter_0(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35825]) ).
fof(f36815,plain,
! [X0,X1] :
( v2_filter_0(X1,X0)
| ~ v1_filter_0(X1,X0)
| ~ m1_filter_0(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35825]) ).
fof(f36860,plain,
! [X0] :
( v10_lattices(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35520]) ).
fof(f37058,plain,
! [X0] :
( ~ r2_filter_2(X0,u1_struct_0(X0))
| ~ m2_filter_2(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(equality_resolution,[],[f36117]) ).
fof(f37241,plain,
! [X0] :
( v17_lattices(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(duplicate_literal_removal,[],[f36089]) ).
fof(f37267,definition,
( spl219_1
<=> v3_struct_0(sK26) ),
introduced(definition,[new_symbols(definition,[spl219_1])],[avatar_definition]) ).
fof(f37269,plain,
( ~ v3_struct_0(sK26)
| spl219_1 ),
inference(avatar_component_clause,[],[f37267]) ).
fof(f37270,plain,
~ spl219_1,
inference(avatar_split_clause,[],[f36124,f37267]) ).
fof(f37272,definition,
( spl219_2
<=> sK27 = k17_filter_2(sK26) ),
introduced(definition,[new_symbols(definition,[spl219_2])],[avatar_definition]) ).
fof(f37273,plain,
( sK27 = k17_filter_2(sK26)
| ~ spl219_2 ),
inference(avatar_component_clause,[],[f37272]) ).
fof(f37274,plain,
( sK27 != k17_filter_2(sK26)
| spl219_2 ),
inference(avatar_component_clause,[],[f37272]) ).
fof(f37276,definition,
( spl219_3
<=> r2_filter_2(sK26,sK27) ),
introduced(definition,[new_symbols(definition,[spl219_3])],[avatar_definition]) ).
fof(f37278,plain,
( r2_filter_2(sK26,sK27)
| ~ spl219_3 ),
inference(avatar_component_clause,[],[f37276]) ).
fof(f37279,plain,
( ~ spl219_2
| spl219_3 ),
inference(avatar_split_clause,[],[f36127,f37276,f37272]) ).
fof(f37280,plain,
( ~ r2_filter_2(sK26,sK27)
| ~ v1_filter_2(sK27,sK26)
| spl219_2 ),
inference(backward_subsumption_resolution,[],[f36128,f37274]) ).
fof(f37282,definition,
( spl219_4
<=> v1_filter_2(sK27,sK26) ),
introduced(definition,[new_symbols(definition,[spl219_4])],[avatar_definition]) ).
fof(f37283,plain,
( ~ v1_filter_2(sK27,sK26)
| spl219_4 ),
inference(avatar_component_clause,[],[f37282]) ).
fof(f37284,plain,
( v1_filter_2(sK27,sK26)
| ~ spl219_4 ),
inference(avatar_component_clause,[],[f37282]) ).
fof(f37285,plain,
( spl219_4
| spl219_3 ),
inference(avatar_split_clause,[],[f36126,f37276,f37282]) ).
fof(f37286,plain,
( ~ r2_filter_2(sK26,sK27)
| spl219_2
| ~ spl219_4 ),
inference(backward_subsumption_resolution,[],[f37280,f37284]) ).
fof(f37299,plain,
( sK27 != u1_struct_0(sK26)
| v3_struct_0(sK26)
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| spl219_2 ),
inference(superposition,[],[f37274,f36002]) ).
fof(f37300,plain,
( sK27 != u1_struct_0(sK26)
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| spl219_1
| spl219_2 ),
inference(forward_subsumption_resolution,[],[f37299,f37269]) ).
fof(f37301,plain,
( sK27 != u1_struct_0(sK26)
| ~ l3_lattices(sK26)
| spl219_1
| spl219_2 ),
inference(forward_subsumption_resolution,[],[f37300,f36123]) ).
fof(f37302,plain,
( sK27 != u1_struct_0(sK26)
| spl219_1
| spl219_2 ),
inference(forward_subsumption_resolution,[],[f37301,f36121]) ).
fof(f37304,definition,
( spl219_5
<=> l3_lattices(sK26) ),
introduced(definition,[new_symbols(definition,[spl219_5])],[avatar_definition]) ).
fof(f37306,plain,
( l3_lattices(sK26)
| ~ spl219_5 ),
inference(avatar_component_clause,[],[f37304]) ).
fof(f37307,plain,
spl219_5,
inference(avatar_split_clause,[],[f36121,f37304]) ).
fof(f37309,definition,
( spl219_6
<=> m2_filter_2(sK27,sK26) ),
introduced(definition,[new_symbols(definition,[spl219_6])],[avatar_definition]) ).
fof(f37311,plain,
( m2_filter_2(sK27,sK26)
| ~ spl219_6 ),
inference(avatar_component_clause,[],[f37309]) ).
fof(f37312,plain,
spl219_6,
inference(avatar_split_clause,[],[f36125,f37309]) ).
fof(f37313,plain,
( m2_lattice4(sK27,sK26)
| v3_struct_0(sK26)
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| ~ spl219_6 ),
inference(resolution,[],[f37311,f35850]) ).
fof(f37315,plain,
( m1_filter_2(k15_filter_2(sK26,sK27),k1_lattice2(sK26))
| v3_struct_0(sK26)
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| ~ spl219_6 ),
inference(resolution,[],[f37311,f35883]) ).
fof(f37316,plain,
( k15_filter_2(sK26,sK27) = k7_filter_2(sK26,sK27)
| v3_struct_0(sK26)
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| ~ spl219_6 ),
inference(resolution,[],[f37311,f35884]) ).
fof(f37325,plain,
( m1_filter_2(sK27,k1_lattice2(sK26))
| v3_struct_0(sK26)
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| ~ spl219_6 ),
inference(resolution,[],[f37311,f35961]) ).
fof(f37339,plain,
( v1_filter_0(k15_filter_2(sK26,sK27),k1_lattice2(sK26))
| ~ r2_filter_2(sK26,sK27)
| v3_struct_0(sK26)
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| ~ spl219_6 ),
inference(resolution,[],[f37311,f36018]) ).
fof(f37340,plain,
( r2_filter_2(sK26,sK27)
| ~ v1_filter_0(k15_filter_2(sK26,sK27),k1_lattice2(sK26))
| v3_struct_0(sK26)
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| ~ spl219_6 ),
inference(resolution,[],[f37311,f36019]) ).
fof(f37358,plain,
( v2_filter_0(k15_filter_2(sK26,sK27),k1_lattice2(sK26))
| ~ v1_filter_2(sK27,sK26)
| v3_struct_0(sK26)
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| ~ spl219_6 ),
inference(resolution,[],[f37311,f36055]) ).
fof(f37359,plain,
( v1_filter_2(sK27,sK26)
| ~ v2_filter_0(k15_filter_2(sK26,sK27),k1_lattice2(sK26))
| v3_struct_0(sK26)
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| ~ spl219_6 ),
inference(resolution,[],[f37311,f36056]) ).
fof(f37400,plain,
( ~ v1_filter_0(k15_filter_2(sK26,sK27),k1_lattice2(sK26))
| v3_struct_0(sK26)
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| spl219_2
| ~ spl219_4
| ~ spl219_6 ),
inference(forward_subsumption_resolution,[],[f37340,f37286]) ).
fof(f37413,plain,
( m1_filter_2(sK27,k1_lattice2(sK26))
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| spl219_1
| ~ spl219_6 ),
inference(forward_subsumption_resolution,[],[f37325,f37269]) ).
fof(f37422,plain,
( k15_filter_2(sK26,sK27) = k7_filter_2(sK26,sK27)
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| spl219_1
| ~ spl219_6 ),
inference(forward_subsumption_resolution,[],[f37316,f37269]) ).
fof(f37423,plain,
( m1_filter_2(k15_filter_2(sK26,sK27),k1_lattice2(sK26))
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| spl219_1
| ~ spl219_6 ),
inference(forward_subsumption_resolution,[],[f37315,f37269]) ).
fof(f37425,plain,
( m2_lattice4(sK27,sK26)
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| spl219_1
| ~ spl219_6 ),
inference(forward_subsumption_resolution,[],[f37313,f37269]) ).
fof(f37451,plain,
( ~ v1_filter_0(k15_filter_2(sK26,sK27),k1_lattice2(sK26))
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| spl219_1
| spl219_2
| ~ spl219_4
| ~ spl219_6 ),
inference(forward_subsumption_resolution,[],[f37400,f37269]) ).
fof(f37464,plain,
( m1_filter_2(sK27,k1_lattice2(sK26))
| ~ l3_lattices(sK26)
| spl219_1
| ~ spl219_6 ),
inference(forward_subsumption_resolution,[],[f37413,f36123]) ).
fof(f37473,plain,
( k15_filter_2(sK26,sK27) = k7_filter_2(sK26,sK27)
| ~ l3_lattices(sK26)
| spl219_1
| ~ spl219_6 ),
inference(forward_subsumption_resolution,[],[f37422,f36123]) ).
fof(f37474,plain,
( m1_filter_2(k15_filter_2(sK26,sK27),k1_lattice2(sK26))
| ~ l3_lattices(sK26)
| spl219_1
| ~ spl219_6 ),
inference(forward_subsumption_resolution,[],[f37423,f36123]) ).
fof(f37476,plain,
( m2_lattice4(sK27,sK26)
| ~ l3_lattices(sK26)
| spl219_1
| ~ spl219_6 ),
inference(forward_subsumption_resolution,[],[f37425,f36123]) ).
fof(f37502,plain,
( ~ v1_filter_0(k15_filter_2(sK26,sK27),k1_lattice2(sK26))
| ~ l3_lattices(sK26)
| spl219_1
| spl219_2
| ~ spl219_4
| ~ spl219_6 ),
inference(forward_subsumption_resolution,[],[f37451,f36123]) ).
fof(f37515,plain,
( m1_filter_2(sK27,k1_lattice2(sK26))
| spl219_1
| ~ spl219_5
| ~ spl219_6 ),
inference(forward_subsumption_resolution,[],[f37464,f37306]) ).
fof(f37524,plain,
( k15_filter_2(sK26,sK27) = k7_filter_2(sK26,sK27)
| spl219_1
| ~ spl219_5
| ~ spl219_6 ),
inference(forward_subsumption_resolution,[],[f37473,f37306]) ).
fof(f37525,plain,
( m1_filter_2(k15_filter_2(sK26,sK27),k1_lattice2(sK26))
| spl219_1
| ~ spl219_5
| ~ spl219_6 ),
inference(forward_subsumption_resolution,[],[f37474,f37306]) ).
fof(f37527,plain,
( m2_lattice4(sK27,sK26)
| spl219_1
| ~ spl219_5
| ~ spl219_6 ),
inference(forward_subsumption_resolution,[],[f37476,f37306]) ).
fof(f37540,plain,
( ~ v1_filter_0(k15_filter_2(sK26,sK27),k1_lattice2(sK26))
| spl219_1
| spl219_2
| ~ spl219_4
| ~ spl219_5
| ~ spl219_6 ),
inference(forward_subsumption_resolution,[],[f37502,f37306]) ).
fof(f37551,plain,
( m1_filter_2(k7_filter_2(sK26,sK27),k1_lattice2(sK26))
| spl219_1
| ~ spl219_5
| ~ spl219_6 ),
inference(forward_demodulation,[],[f37525,f37524]) ).
fof(f37555,plain,
( ~ v1_filter_0(k7_filter_2(sK26,sK27),k1_lattice2(sK26))
| spl219_1
| spl219_2
| ~ spl219_4
| ~ spl219_5
| ~ spl219_6 ),
inference(forward_demodulation,[],[f37540,f37524]) ).
fof(f37885,plain,
( ~ v3_struct_0(k1_lattice2(sK26))
| ~ l3_lattices(sK26)
| spl219_1 ),
inference(resolution,[],[f37269,f36293]) ).
fof(f38120,plain,
( v10_lattices(k1_lattice2(sK26))
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| spl219_1 ),
inference(resolution,[],[f37269,f36860]) ).
fof(f38255,plain,
( v17_lattices(k1_lattice2(sK26))
| ~ v10_lattices(sK26)
| ~ v17_lattices(sK26)
| ~ l3_lattices(sK26)
| spl219_1 ),
inference(resolution,[],[f37269,f37241]) ).
fof(f38308,plain,
( v17_lattices(k1_lattice2(sK26))
| ~ v17_lattices(sK26)
| ~ l3_lattices(sK26)
| spl219_1 ),
inference(forward_subsumption_resolution,[],[f38255,f36123]) ).
fof(f38439,plain,
( v10_lattices(k1_lattice2(sK26))
| ~ l3_lattices(sK26)
| spl219_1 ),
inference(forward_subsumption_resolution,[],[f38120,f36123]) ).
fof(f38671,plain,
( ~ v3_struct_0(k1_lattice2(sK26))
| spl219_1
| ~ spl219_5 ),
inference(forward_subsumption_resolution,[],[f37885,f37306]) ).
fof(f39010,plain,
( v17_lattices(k1_lattice2(sK26))
| ~ l3_lattices(sK26)
| spl219_1 ),
inference(forward_subsumption_resolution,[],[f38308,f36122]) ).
fof(f39118,plain,
( v10_lattices(k1_lattice2(sK26))
| spl219_1
| ~ spl219_5 ),
inference(forward_subsumption_resolution,[],[f38439,f37306]) ).
fof(f39618,plain,
( v17_lattices(k1_lattice2(sK26))
| spl219_1
| ~ spl219_5 ),
inference(forward_subsumption_resolution,[],[f39010,f37306]) ).
fof(f39981,definition,
( spl219_7
<=> v10_lattices(sK26) ),
introduced(definition,[new_symbols(definition,[spl219_7])],[avatar_definition]) ).
fof(f39983,plain,
( v10_lattices(sK26)
| ~ spl219_7 ),
inference(avatar_component_clause,[],[f39981]) ).
fof(f39984,plain,
spl219_7,
inference(avatar_split_clause,[],[f36123,f39981]) ).
fof(f39986,definition,
( spl219_8
<=> v17_lattices(sK26) ),
introduced(definition,[new_symbols(definition,[spl219_8])],[avatar_definition]) ).
fof(f39988,plain,
( v17_lattices(sK26)
| ~ spl219_8 ),
inference(avatar_component_clause,[],[f39986]) ).
fof(f39989,plain,
spl219_8,
inference(avatar_split_clause,[],[f36122,f39986]) ).
fof(f41139,plain,
( l3_lattices(k1_lattice2(sK26))
| ~ spl219_5 ),
inference(resolution,[],[f37306,f36267]) ).
fof(f41923,definition,
( spl219_11
<=> v1_filter_0(k7_filter_2(sK26,sK27),k1_lattice2(sK26)) ),
introduced(definition,[new_symbols(definition,[spl219_11])],[avatar_definition]) ).
fof(f41924,plain,
( v1_filter_0(k7_filter_2(sK26,sK27),k1_lattice2(sK26))
| ~ spl219_11 ),
inference(avatar_component_clause,[],[f41923]) ).
fof(f41925,plain,
( ~ v1_filter_0(k7_filter_2(sK26,sK27),k1_lattice2(sK26))
| spl219_11 ),
inference(avatar_component_clause,[],[f41923]) ).
fof(f41926,plain,
( ~ spl219_11
| spl219_1
| spl219_2
| ~ spl219_4
| ~ spl219_5
| ~ spl219_6 ),
inference(avatar_split_clause,[],[f37555,f37309,f37304,f37282,f37272,f37267,f41923]) ).
fof(f41972,plain,
( ~ v1_filter_0(sK27,k1_lattice2(sK26))
| ~ m1_subset_1(sK27,k1_zfmisc_1(u1_struct_0(sK26)))
| v3_struct_0(sK26)
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| spl219_11 ),
inference(superposition,[],[f41925,f35963]) ).
fof(f41977,plain,
( ~ v1_filter_0(sK27,k1_lattice2(sK26))
| ~ m1_subset_1(sK27,k1_zfmisc_1(u1_struct_0(sK26)))
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| spl219_1
| spl219_11 ),
inference(forward_subsumption_resolution,[],[f41972,f37269]) ).
fof(f41988,plain,
( ~ v1_filter_0(sK27,k1_lattice2(sK26))
| ~ m1_subset_1(sK27,k1_zfmisc_1(u1_struct_0(sK26)))
| ~ l3_lattices(sK26)
| spl219_1
| ~ spl219_7
| spl219_11 ),
inference(forward_subsumption_resolution,[],[f41977,f39983]) ).
fof(f41997,plain,
( ~ v1_filter_0(sK27,k1_lattice2(sK26))
| ~ m1_subset_1(sK27,k1_zfmisc_1(u1_struct_0(sK26)))
| spl219_1
| ~ spl219_5
| ~ spl219_7
| spl219_11 ),
inference(forward_subsumption_resolution,[],[f41988,f37306]) ).
fof(f42025,definition,
( spl219_13
<=> sK27 = u1_struct_0(sK26) ),
introduced(definition,[new_symbols(definition,[spl219_13])],[avatar_definition]) ).
fof(f42026,plain,
( sK27 = u1_struct_0(sK26)
| ~ spl219_13 ),
inference(avatar_component_clause,[],[f42025]) ).
fof(f42027,plain,
( sK27 != u1_struct_0(sK26)
| spl219_13 ),
inference(avatar_component_clause,[],[f42025]) ).
fof(f42028,plain,
( ~ spl219_13
| spl219_1
| spl219_2 ),
inference(avatar_split_clause,[],[f37302,f37272,f37267,f42025]) ).
fof(f42258,definition,
( spl219_14
<=> m2_lattice4(sK27,sK26) ),
introduced(definition,[new_symbols(definition,[spl219_14])],[avatar_definition]) ).
fof(f42260,plain,
( m2_lattice4(sK27,sK26)
| ~ spl219_14 ),
inference(avatar_component_clause,[],[f42258]) ).
fof(f42261,plain,
( spl219_14
| spl219_1
| ~ spl219_5
| ~ spl219_6 ),
inference(avatar_split_clause,[],[f37527,f37309,f37304,f37267,f42258]) ).
fof(f42276,plain,
( m1_subset_1(sK27,k1_zfmisc_1(u1_struct_0(sK26)))
| v3_struct_0(sK26)
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| ~ spl219_14 ),
inference(resolution,[],[f42260,f36142]) ).
fof(f42281,plain,
( m1_subset_1(sK27,k1_zfmisc_1(u1_struct_0(sK26)))
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| spl219_1
| ~ spl219_14 ),
inference(forward_subsumption_resolution,[],[f42276,f37269]) ).
fof(f42293,plain,
( m1_subset_1(sK27,k1_zfmisc_1(u1_struct_0(sK26)))
| ~ l3_lattices(sK26)
| spl219_1
| ~ spl219_7
| ~ spl219_14 ),
inference(forward_subsumption_resolution,[],[f42281,f39983]) ).
fof(f42301,plain,
( m1_subset_1(sK27,k1_zfmisc_1(u1_struct_0(sK26)))
| spl219_1
| ~ spl219_5
| ~ spl219_7
| ~ spl219_14 ),
inference(forward_subsumption_resolution,[],[f42293,f37306]) ).
fof(f42309,plain,
( ~ v1_filter_0(sK27,k1_lattice2(sK26))
| spl219_1
| ~ spl219_5
| ~ spl219_7
| spl219_11
| ~ spl219_14 ),
inference(backward_subsumption_resolution,[],[f41997,f42301]) ).
fof(f42389,definition,
( spl219_17
<=> m1_filter_2(sK27,k1_lattice2(sK26)) ),
introduced(definition,[new_symbols(definition,[spl219_17])],[avatar_definition]) ).
fof(f42391,plain,
( m1_filter_2(sK27,k1_lattice2(sK26))
| ~ spl219_17 ),
inference(avatar_component_clause,[],[f42389]) ).
fof(f42392,plain,
( spl219_17
| spl219_1
| ~ spl219_5
| ~ spl219_6 ),
inference(avatar_split_clause,[],[f37515,f37309,f37304,f37267,f42389]) ).
fof(f42395,plain,
( m1_filter_0(sK27,k1_lattice2(sK26))
| v3_struct_0(k1_lattice2(sK26))
| ~ v10_lattices(k1_lattice2(sK26))
| ~ l3_lattices(k1_lattice2(sK26))
| ~ spl219_17 ),
inference(resolution,[],[f42391,f35848]) ).
fof(f42403,plain,
( m1_filter_0(sK27,k1_lattice2(sK26))
| ~ v10_lattices(k1_lattice2(sK26))
| ~ l3_lattices(k1_lattice2(sK26))
| spl219_1
| ~ spl219_5
| ~ spl219_17 ),
inference(forward_subsumption_resolution,[],[f42395,f38671]) ).
fof(f42408,plain,
( m1_filter_0(sK27,k1_lattice2(sK26))
| ~ l3_lattices(k1_lattice2(sK26))
| spl219_1
| ~ spl219_5
| ~ spl219_17 ),
inference(forward_subsumption_resolution,[],[f42403,f39118]) ).
fof(f42411,plain,
( m1_filter_0(sK27,k1_lattice2(sK26))
| spl219_1
| ~ spl219_5
| ~ spl219_17 ),
inference(forward_subsumption_resolution,[],[f42408,f41139]) ).
fof(f44489,definition,
( spl219_23
<=> v1_filter_0(sK27,k1_lattice2(sK26)) ),
introduced(definition,[new_symbols(definition,[spl219_23])],[avatar_definition]) ).
fof(f44491,plain,
( ~ v1_filter_0(sK27,k1_lattice2(sK26))
| spl219_23 ),
inference(avatar_component_clause,[],[f44489]) ).
fof(f44492,plain,
( ~ spl219_23
| spl219_1
| ~ spl219_5
| ~ spl219_7
| spl219_11
| ~ spl219_14 ),
inference(avatar_split_clause,[],[f42309,f42258,f41923,f39981,f37304,f37267,f44489]) ).
fof(f44494,definition,
( spl219_24
<=> m1_filter_0(sK27,k1_lattice2(sK26)) ),
introduced(definition,[new_symbols(definition,[spl219_24])],[avatar_definition]) ).
fof(f44496,plain,
( m1_filter_0(sK27,k1_lattice2(sK26))
| ~ spl219_24 ),
inference(avatar_component_clause,[],[f44494]) ).
fof(f44497,plain,
( spl219_24
| spl219_1
| ~ spl219_5
| ~ spl219_17 ),
inference(avatar_split_clause,[],[f42411,f42389,f37304,f37267,f44494]) ).
fof(f44914,definition,
( spl219_27
<=> m1_filter_2(k7_filter_2(sK26,sK27),k1_lattice2(sK26)) ),
introduced(definition,[new_symbols(definition,[spl219_27])],[avatar_definition]) ).
fof(f44916,plain,
( m1_filter_2(k7_filter_2(sK26,sK27),k1_lattice2(sK26))
| ~ spl219_27 ),
inference(avatar_component_clause,[],[f44914]) ).
fof(f44917,plain,
( spl219_27
| spl219_1
| ~ spl219_5
| ~ spl219_6 ),
inference(avatar_split_clause,[],[f37551,f37309,f37304,f37267,f44914]) ).
fof(f46387,plain,
( v1_filter_0(sK27,k1_lattice2(sK26))
| sK27 = k1_filter_0(k1_lattice2(sK26))
| ~ v2_filter_0(sK27,k1_lattice2(sK26))
| v3_struct_0(k1_lattice2(sK26))
| ~ v10_lattices(k1_lattice2(sK26))
| ~ v17_lattices(k1_lattice2(sK26))
| ~ l3_lattices(k1_lattice2(sK26))
| ~ spl219_24 ),
inference(resolution,[],[f44496,f36814]) ).
fof(f46420,plain,
( sK27 = k1_filter_0(k1_lattice2(sK26))
| ~ v2_filter_0(sK27,k1_lattice2(sK26))
| v3_struct_0(k1_lattice2(sK26))
| ~ v10_lattices(k1_lattice2(sK26))
| ~ v17_lattices(k1_lattice2(sK26))
| ~ l3_lattices(k1_lattice2(sK26))
| spl219_23
| ~ spl219_24 ),
inference(forward_subsumption_resolution,[],[f46387,f44491]) ).
fof(f46479,plain,
( sK27 = k1_filter_0(k1_lattice2(sK26))
| ~ v2_filter_0(sK27,k1_lattice2(sK26))
| ~ v10_lattices(k1_lattice2(sK26))
| ~ v17_lattices(k1_lattice2(sK26))
| ~ l3_lattices(k1_lattice2(sK26))
| spl219_1
| ~ spl219_5
| spl219_23
| ~ spl219_24 ),
inference(forward_subsumption_resolution,[],[f46420,f38671]) ).
fof(f46536,plain,
( sK27 = k1_filter_0(k1_lattice2(sK26))
| ~ v2_filter_0(sK27,k1_lattice2(sK26))
| ~ v17_lattices(k1_lattice2(sK26))
| ~ l3_lattices(k1_lattice2(sK26))
| spl219_1
| ~ spl219_5
| spl219_23
| ~ spl219_24 ),
inference(forward_subsumption_resolution,[],[f46479,f39118]) ).
fof(f46590,plain,
( sK27 = k1_filter_0(k1_lattice2(sK26))
| ~ v2_filter_0(sK27,k1_lattice2(sK26))
| ~ l3_lattices(k1_lattice2(sK26))
| spl219_1
| ~ spl219_5
| spl219_23
| ~ spl219_24 ),
inference(forward_subsumption_resolution,[],[f46536,f39618]) ).
fof(f46633,plain,
( sK27 = k1_filter_0(k1_lattice2(sK26))
| ~ v2_filter_0(sK27,k1_lattice2(sK26))
| spl219_1
| ~ spl219_5
| spl219_23
| ~ spl219_24 ),
inference(forward_subsumption_resolution,[],[f46590,f41139]) ).
fof(f48345,plain,
( ~ v2_filter_0(k15_filter_2(sK26,sK27),k1_lattice2(sK26))
| v3_struct_0(sK26)
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| spl219_4
| ~ spl219_6 ),
inference(forward_subsumption_resolution,[],[f37359,f37283]) ).
fof(f48351,plain,
( v1_filter_0(k15_filter_2(sK26,sK27),k1_lattice2(sK26))
| v3_struct_0(sK26)
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| ~ spl219_3
| ~ spl219_6 ),
inference(forward_subsumption_resolution,[],[f37339,f37278]) ).
fof(f48359,plain,
( ~ v2_filter_0(k15_filter_2(sK26,sK27),k1_lattice2(sK26))
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| spl219_1
| spl219_4
| ~ spl219_6 ),
inference(forward_subsumption_resolution,[],[f48345,f37269]) ).
fof(f48365,plain,
( v1_filter_0(k15_filter_2(sK26,sK27),k1_lattice2(sK26))
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| spl219_1
| ~ spl219_3
| ~ spl219_6 ),
inference(forward_subsumption_resolution,[],[f48351,f37269]) ).
fof(f48372,plain,
( ~ v2_filter_0(k15_filter_2(sK26,sK27),k1_lattice2(sK26))
| ~ l3_lattices(sK26)
| spl219_1
| spl219_4
| ~ spl219_6
| ~ spl219_7 ),
inference(forward_subsumption_resolution,[],[f48359,f39983]) ).
fof(f48378,plain,
( v1_filter_0(k15_filter_2(sK26,sK27),k1_lattice2(sK26))
| ~ l3_lattices(sK26)
| spl219_1
| ~ spl219_3
| ~ spl219_6
| ~ spl219_7 ),
inference(forward_subsumption_resolution,[],[f48365,f39983]) ).
fof(f48385,plain,
( ~ v2_filter_0(k15_filter_2(sK26,sK27),k1_lattice2(sK26))
| spl219_1
| spl219_4
| ~ spl219_5
| ~ spl219_6
| ~ spl219_7 ),
inference(forward_subsumption_resolution,[],[f48372,f37306]) ).
fof(f48391,plain,
( v1_filter_0(k15_filter_2(sK26,sK27),k1_lattice2(sK26))
| spl219_1
| ~ spl219_3
| ~ spl219_5
| ~ spl219_6
| ~ spl219_7 ),
inference(forward_subsumption_resolution,[],[f48378,f37306]) ).
fof(f48398,plain,
( ~ v2_filter_0(k7_filter_2(sK26,sK27),k1_lattice2(sK26))
| spl219_1
| spl219_4
| ~ spl219_5
| ~ spl219_6
| ~ spl219_7 ),
inference(forward_demodulation,[],[f48385,f37524]) ).
fof(f48399,plain,
( v1_filter_0(k7_filter_2(sK26,sK27),k1_lattice2(sK26))
| spl219_1
| ~ spl219_3
| ~ spl219_5
| ~ spl219_6
| ~ spl219_7 ),
inference(forward_demodulation,[],[f48391,f37524]) ).
fof(f48404,plain,
( $false
| spl219_1
| ~ spl219_3
| ~ spl219_5
| ~ spl219_6
| ~ spl219_7
| spl219_11 ),
inference(forward_subsumption_resolution,[],[f48399,f41925]) ).
fof(f48405,plain,
( spl219_1
| ~ spl219_3
| ~ spl219_5
| ~ spl219_6
| ~ spl219_7
| spl219_11 ),
inference(avatar_contradiction_clause,[],[f48404]) ).
fof(f48423,definition,
( spl219_42
<=> v2_filter_0(k7_filter_2(sK26,sK27),k1_lattice2(sK26)) ),
introduced(definition,[new_symbols(definition,[spl219_42])],[avatar_definition]) ).
fof(f48424,plain,
( v2_filter_0(k7_filter_2(sK26,sK27),k1_lattice2(sK26))
| ~ spl219_42 ),
inference(avatar_component_clause,[],[f48423]) ).
fof(f48425,plain,
( ~ v2_filter_0(k7_filter_2(sK26,sK27),k1_lattice2(sK26))
| spl219_42 ),
inference(avatar_component_clause,[],[f48423]) ).
fof(f48426,plain,
( ~ spl219_42
| spl219_1
| spl219_4
| ~ spl219_5
| ~ spl219_6
| ~ spl219_7 ),
inference(avatar_split_clause,[],[f48398,f39981,f37309,f37304,f37282,f37267,f48423]) ).
fof(f48428,plain,
( ~ v1_filter_0(k7_filter_2(sK26,sK27),k1_lattice2(sK26))
| ~ m1_filter_0(k7_filter_2(sK26,sK27),k1_lattice2(sK26))
| v3_struct_0(k1_lattice2(sK26))
| ~ v10_lattices(k1_lattice2(sK26))
| ~ v17_lattices(k1_lattice2(sK26))
| ~ l3_lattices(k1_lattice2(sK26))
| spl219_42 ),
inference(resolution,[],[f48425,f36815]) ).
fof(f48445,plain,
( ~ m1_filter_0(k7_filter_2(sK26,sK27),k1_lattice2(sK26))
| v3_struct_0(k1_lattice2(sK26))
| ~ v10_lattices(k1_lattice2(sK26))
| ~ v17_lattices(k1_lattice2(sK26))
| ~ l3_lattices(k1_lattice2(sK26))
| ~ spl219_11
| spl219_42 ),
inference(forward_subsumption_resolution,[],[f48428,f41924]) ).
fof(f48455,plain,
( ~ m1_filter_0(k7_filter_2(sK26,sK27),k1_lattice2(sK26))
| ~ v10_lattices(k1_lattice2(sK26))
| ~ v17_lattices(k1_lattice2(sK26))
| ~ l3_lattices(k1_lattice2(sK26))
| spl219_1
| ~ spl219_5
| ~ spl219_11
| spl219_42 ),
inference(forward_subsumption_resolution,[],[f48445,f38671]) ).
fof(f48463,plain,
( ~ m1_filter_0(k7_filter_2(sK26,sK27),k1_lattice2(sK26))
| ~ v17_lattices(k1_lattice2(sK26))
| ~ l3_lattices(k1_lattice2(sK26))
| spl219_1
| ~ spl219_5
| ~ spl219_11
| spl219_42 ),
inference(forward_subsumption_resolution,[],[f48455,f39118]) ).
fof(f48468,plain,
( ~ m1_filter_0(k7_filter_2(sK26,sK27),k1_lattice2(sK26))
| ~ l3_lattices(k1_lattice2(sK26))
| spl219_1
| ~ spl219_5
| ~ spl219_11
| spl219_42 ),
inference(forward_subsumption_resolution,[],[f48463,f39618]) ).
fof(f48476,plain,
( ~ m1_filter_0(k7_filter_2(sK26,sK27),k1_lattice2(sK26))
| spl219_1
| ~ spl219_5
| ~ spl219_11
| spl219_42 ),
inference(forward_subsumption_resolution,[],[f48468,f41139]) ).
fof(f48576,plain,
( v2_filter_0(k15_filter_2(sK26,sK27),k1_lattice2(sK26))
| v3_struct_0(sK26)
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| ~ spl219_4
| ~ spl219_6 ),
inference(forward_subsumption_resolution,[],[f37358,f37284]) ).
fof(f48589,plain,
( v2_filter_0(k15_filter_2(sK26,sK27),k1_lattice2(sK26))
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| spl219_1
| ~ spl219_4
| ~ spl219_6 ),
inference(forward_subsumption_resolution,[],[f48576,f37269]) ).
fof(f48600,plain,
( v2_filter_0(k15_filter_2(sK26,sK27),k1_lattice2(sK26))
| ~ l3_lattices(sK26)
| spl219_1
| ~ spl219_4
| ~ spl219_6
| ~ spl219_7 ),
inference(forward_subsumption_resolution,[],[f48589,f39983]) ).
fof(f48611,plain,
( v2_filter_0(k15_filter_2(sK26,sK27),k1_lattice2(sK26))
| spl219_1
| ~ spl219_4
| ~ spl219_5
| ~ spl219_6
| ~ spl219_7 ),
inference(forward_subsumption_resolution,[],[f48600,f37306]) ).
fof(f48619,plain,
( v2_filter_0(k7_filter_2(sK26,sK27),k1_lattice2(sK26))
| spl219_1
| ~ spl219_4
| ~ spl219_5
| ~ spl219_6
| ~ spl219_7 ),
inference(forward_demodulation,[],[f48611,f37524]) ).
fof(f48622,plain,
( $false
| spl219_1
| ~ spl219_4
| ~ spl219_5
| ~ spl219_6
| ~ spl219_7
| spl219_42 ),
inference(forward_subsumption_resolution,[],[f48619,f48425]) ).
fof(f48623,plain,
( spl219_1
| ~ spl219_4
| ~ spl219_5
| ~ spl219_6
| ~ spl219_7
| spl219_42 ),
inference(avatar_contradiction_clause,[],[f48622]) ).
fof(f48634,plain,
( sK27 = u1_struct_0(sK26)
| v3_struct_0(sK26)
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| ~ spl219_2 ),
inference(superposition,[],[f37273,f36002]) ).
fof(f48647,plain,
( v3_struct_0(sK26)
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| ~ spl219_2
| spl219_13 ),
inference(forward_subsumption_resolution,[],[f48634,f42027]) ).
fof(f48654,plain,
( ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| spl219_1
| ~ spl219_2
| spl219_13 ),
inference(forward_subsumption_resolution,[],[f48647,f37269]) ).
fof(f48659,plain,
( ~ l3_lattices(sK26)
| spl219_1
| ~ spl219_2
| ~ spl219_7
| spl219_13 ),
inference(forward_subsumption_resolution,[],[f48654,f39983]) ).
fof(f48665,plain,
( $false
| spl219_1
| ~ spl219_2
| ~ spl219_5
| ~ spl219_7
| spl219_13 ),
inference(forward_subsumption_resolution,[],[f48659,f37306]) ).
fof(f48666,plain,
( spl219_1
| ~ spl219_2
| ~ spl219_5
| ~ spl219_7
| spl219_13 ),
inference(avatar_contradiction_clause,[],[f48665]) ).
fof(f49424,plain,
( ~ r2_filter_2(sK26,sK27)
| ~ m2_filter_2(sK27,sK26)
| v3_struct_0(sK26)
| ~ v10_lattices(sK26)
| ~ v17_lattices(sK26)
| ~ l3_lattices(sK26)
| ~ spl219_13 ),
inference(superposition,[],[f37058,f42026]) ).
fof(f49669,plain,
( ~ m2_filter_2(sK27,sK26)
| v3_struct_0(sK26)
| ~ v10_lattices(sK26)
| ~ v17_lattices(sK26)
| ~ l3_lattices(sK26)
| ~ spl219_3
| ~ spl219_13 ),
inference(forward_subsumption_resolution,[],[f49424,f37278]) ).
fof(f50465,plain,
( v3_struct_0(sK26)
| ~ v10_lattices(sK26)
| ~ v17_lattices(sK26)
| ~ l3_lattices(sK26)
| ~ spl219_3
| ~ spl219_6
| ~ spl219_13 ),
inference(forward_subsumption_resolution,[],[f49669,f37311]) ).
fof(f51229,plain,
( ~ v10_lattices(sK26)
| ~ v17_lattices(sK26)
| ~ l3_lattices(sK26)
| spl219_1
| ~ spl219_3
| ~ spl219_6
| ~ spl219_13 ),
inference(forward_subsumption_resolution,[],[f50465,f37269]) ).
fof(f51902,plain,
( ~ v17_lattices(sK26)
| ~ l3_lattices(sK26)
| spl219_1
| ~ spl219_3
| ~ spl219_6
| ~ spl219_7
| ~ spl219_13 ),
inference(forward_subsumption_resolution,[],[f51229,f39983]) ).
fof(f52152,plain,
( ~ l3_lattices(sK26)
| spl219_1
| ~ spl219_3
| ~ spl219_6
| ~ spl219_7
| ~ spl219_8
| ~ spl219_13 ),
inference(forward_subsumption_resolution,[],[f51902,f39988]) ).
fof(f52250,plain,
( $false
| spl219_1
| ~ spl219_3
| ~ spl219_5
| ~ spl219_6
| ~ spl219_7
| ~ spl219_8
| ~ spl219_13 ),
inference(forward_subsumption_resolution,[],[f52152,f37306]) ).
fof(f52251,plain,
( spl219_1
| ~ spl219_3
| ~ spl219_5
| ~ spl219_6
| ~ spl219_7
| ~ spl219_8
| ~ spl219_13 ),
inference(avatar_contradiction_clause,[],[f52250]) ).
fof(f52913,definition,
( spl219_46
<=> v2_filter_0(sK27,k1_lattice2(sK26)) ),
introduced(definition,[new_symbols(definition,[spl219_46])],[avatar_definition]) ).
fof(f52914,plain,
( v2_filter_0(sK27,k1_lattice2(sK26))
| ~ spl219_46 ),
inference(avatar_component_clause,[],[f52913]) ).
fof(f52915,plain,
( ~ v2_filter_0(sK27,k1_lattice2(sK26))
| spl219_46 ),
inference(avatar_component_clause,[],[f52913]) ).
fof(f52918,definition,
( spl219_47
<=> m1_filter_0(k7_filter_2(sK26,sK27),k1_lattice2(sK26)) ),
introduced(definition,[new_symbols(definition,[spl219_47])],[avatar_definition]) ).
fof(f52920,plain,
( ~ m1_filter_0(k7_filter_2(sK26,sK27),k1_lattice2(sK26))
| spl219_47 ),
inference(avatar_component_clause,[],[f52918]) ).
fof(f52921,plain,
( ~ spl219_47
| spl219_1
| ~ spl219_5
| ~ spl219_11
| spl219_42 ),
inference(avatar_split_clause,[],[f48476,f48423,f41923,f37304,f37267,f52918]) ).
fof(f57026,plain,
( ~ m1_filter_2(k7_filter_2(sK26,sK27),k1_lattice2(sK26))
| v3_struct_0(k1_lattice2(sK26))
| ~ v10_lattices(k1_lattice2(sK26))
| ~ l3_lattices(k1_lattice2(sK26))
| spl219_47 ),
inference(resolution,[],[f52920,f35848]) ).
fof(f57093,plain,
( v3_struct_0(k1_lattice2(sK26))
| ~ v10_lattices(k1_lattice2(sK26))
| ~ l3_lattices(k1_lattice2(sK26))
| ~ spl219_27
| spl219_47 ),
inference(forward_subsumption_resolution,[],[f57026,f44916]) ).
fof(f57127,plain,
( ~ v10_lattices(k1_lattice2(sK26))
| ~ l3_lattices(k1_lattice2(sK26))
| spl219_1
| ~ spl219_5
| ~ spl219_27
| spl219_47 ),
inference(forward_subsumption_resolution,[],[f57093,f38671]) ).
fof(f57159,plain,
( ~ l3_lattices(k1_lattice2(sK26))
| spl219_1
| ~ spl219_5
| ~ spl219_27
| spl219_47 ),
inference(forward_subsumption_resolution,[],[f57127,f39118]) ).
fof(f57191,plain,
( $false
| spl219_1
| ~ spl219_5
| ~ spl219_27
| spl219_47 ),
inference(forward_subsumption_resolution,[],[f57159,f41139]) ).
fof(f57192,plain,
( spl219_1
| ~ spl219_5
| ~ spl219_27
| spl219_47 ),
inference(avatar_contradiction_clause,[],[f57191]) ).
fof(f57564,plain,
( v2_filter_0(sK27,k1_lattice2(sK26))
| ~ m1_subset_1(sK27,k1_zfmisc_1(u1_struct_0(sK26)))
| v3_struct_0(sK26)
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| ~ spl219_42 ),
inference(superposition,[],[f48424,f35963]) ).
fof(f57569,plain,
( ~ m1_subset_1(sK27,k1_zfmisc_1(u1_struct_0(sK26)))
| v3_struct_0(sK26)
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| ~ spl219_42
| spl219_46 ),
inference(forward_subsumption_resolution,[],[f57564,f52915]) ).
fof(f57575,plain,
( v3_struct_0(sK26)
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| spl219_1
| ~ spl219_5
| ~ spl219_7
| ~ spl219_14
| ~ spl219_42
| spl219_46 ),
inference(forward_subsumption_resolution,[],[f57569,f42301]) ).
fof(f57579,plain,
( ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| spl219_1
| ~ spl219_5
| ~ spl219_7
| ~ spl219_14
| ~ spl219_42
| spl219_46 ),
inference(forward_subsumption_resolution,[],[f57575,f37269]) ).
fof(f57583,plain,
( ~ l3_lattices(sK26)
| spl219_1
| ~ spl219_5
| ~ spl219_7
| ~ spl219_14
| ~ spl219_42
| spl219_46 ),
inference(forward_subsumption_resolution,[],[f57579,f39983]) ).
fof(f57587,plain,
( $false
| spl219_1
| ~ spl219_5
| ~ spl219_7
| ~ spl219_14
| ~ spl219_42
| spl219_46 ),
inference(forward_subsumption_resolution,[],[f57583,f37306]) ).
fof(f57588,plain,
( spl219_1
| ~ spl219_5
| ~ spl219_7
| ~ spl219_14
| ~ spl219_42
| spl219_46 ),
inference(avatar_contradiction_clause,[],[f57587]) ).
fof(f57599,plain,
( sK27 = k1_filter_0(k1_lattice2(sK26))
| spl219_1
| ~ spl219_5
| spl219_23
| ~ spl219_24
| ~ spl219_46 ),
inference(backward_subsumption_resolution,[],[f46633,f52914]) ).
fof(f60034,definition,
( spl219_71
<=> l3_lattices(k1_lattice2(sK26)) ),
introduced(definition,[new_symbols(definition,[spl219_71])],[avatar_definition]) ).
fof(f60036,plain,
( l3_lattices(k1_lattice2(sK26))
| ~ spl219_71 ),
inference(avatar_component_clause,[],[f60034]) ).
fof(f60037,plain,
( spl219_71
| ~ spl219_5 ),
inference(avatar_split_clause,[],[f41139,f37304,f60034]) ).
fof(f63605,plain,
( u1_struct_0(k1_lattice2(sK26)) = k1_filter_0(k1_lattice2(sK26))
| v3_struct_0(k1_lattice2(sK26))
| ~ v10_lattices(k1_lattice2(sK26))
| ~ spl219_71 ),
inference(resolution,[],[f60036,f36225]) ).
fof(f64394,plain,
( u1_struct_0(k1_lattice2(sK26)) = k1_filter_0(k1_lattice2(sK26))
| ~ v10_lattices(k1_lattice2(sK26))
| spl219_1
| ~ spl219_5
| ~ spl219_71 ),
inference(forward_subsumption_resolution,[],[f63605,f38671]) ).
fof(f64987,plain,
( u1_struct_0(k1_lattice2(sK26)) = k1_filter_0(k1_lattice2(sK26))
| spl219_1
| ~ spl219_5
| ~ spl219_71 ),
inference(forward_subsumption_resolution,[],[f64394,f39118]) ).
fof(f65530,plain,
( sK27 = u1_struct_0(k1_lattice2(sK26))
| spl219_1
| ~ spl219_5
| spl219_23
| ~ spl219_24
| ~ spl219_46
| ~ spl219_71 ),
inference(forward_demodulation,[],[f64987,f57599]) ).
fof(f73798,definition,
( spl219_100
<=> sK27 = u1_struct_0(k1_lattice2(sK26)) ),
introduced(definition,[new_symbols(definition,[spl219_100])],[avatar_definition]) ).
fof(f73800,plain,
( sK27 = u1_struct_0(k1_lattice2(sK26))
| ~ spl219_100 ),
inference(avatar_component_clause,[],[f73798]) ).
fof(f73801,plain,
( spl219_100
| spl219_1
| ~ spl219_5
| spl219_23
| ~ spl219_24
| ~ spl219_46
| ~ spl219_71 ),
inference(avatar_split_clause,[],[f65530,f60034,f52913,f44494,f44489,f37304,f37267,f73798]) ).
fof(f73804,plain,
( sK27 = u1_struct_0(sK26)
| v3_struct_0(sK26)
| ~ l3_lattices(sK26)
| ~ spl219_100 ),
inference(superposition,[],[f73800,f36290]) ).
fof(f75538,plain,
( v3_struct_0(sK26)
| ~ l3_lattices(sK26)
| spl219_13
| ~ spl219_100 ),
inference(forward_subsumption_resolution,[],[f73804,f42027]) ).
fof(f76361,plain,
( ~ l3_lattices(sK26)
| spl219_1
| spl219_13
| ~ spl219_100 ),
inference(forward_subsumption_resolution,[],[f75538,f37269]) ).
fof(f77167,plain,
( $false
| spl219_1
| ~ spl219_5
| spl219_13
| ~ spl219_100 ),
inference(forward_subsumption_resolution,[],[f76361,f37306]) ).
fof(f77168,plain,
( spl219_1
| ~ spl219_5
| spl219_13
| ~ spl219_100 ),
inference(avatar_contradiction_clause,[],[f77167]) ).
cnf(s1,plain,
~ spl219_1,
inference(sat_conversion,[],[f37270]) ).
cnf(s2,plain,
( ~ spl219_2
| spl219_3 ),
inference(sat_conversion,[],[f37279]) ).
cnf(s3,plain,
( spl219_3
| spl219_4 ),
inference(sat_conversion,[],[f37285]) ).
cnf(s4,plain,
spl219_5,
inference(sat_conversion,[],[f37307]) ).
cnf(s5,plain,
spl219_6,
inference(sat_conversion,[],[f37312]) ).
cnf(s6,plain,
spl219_7,
inference(sat_conversion,[],[f39984]) ).
cnf(s7,plain,
spl219_8,
inference(sat_conversion,[],[f39989]) ).
cnf(s11,plain,
( spl219_1
| spl219_2
| ~ spl219_4
| ~ spl219_5
| ~ spl219_6
| ~ spl219_11 ),
inference(sat_conversion,[],[f41926]) ).
cnf(s13,plain,
( spl219_1
| spl219_2
| ~ spl219_13 ),
inference(sat_conversion,[],[f42028]) ).
cnf(s14,plain,
( spl219_1
| ~ spl219_5
| ~ spl219_6
| spl219_14 ),
inference(sat_conversion,[],[f42261]) ).
cnf(s17,plain,
( spl219_1
| ~ spl219_5
| ~ spl219_6
| spl219_17 ),
inference(sat_conversion,[],[f42392]) ).
cnf(s23,plain,
( spl219_1
| ~ spl219_5
| ~ spl219_7
| spl219_11
| ~ spl219_14
| ~ spl219_23 ),
inference(sat_conversion,[],[f44492]) ).
cnf(s24,plain,
( spl219_1
| ~ spl219_5
| ~ spl219_17
| spl219_24 ),
inference(sat_conversion,[],[f44497]) ).
cnf(s27,plain,
( spl219_1
| ~ spl219_5
| ~ spl219_6
| spl219_27 ),
inference(sat_conversion,[],[f44917]) ).
cnf(s42,plain,
( spl219_1
| ~ spl219_3
| ~ spl219_5
| ~ spl219_6
| ~ spl219_7
| spl219_11 ),
inference(sat_conversion,[],[f48405]) ).
cnf(s44,plain,
( spl219_1
| spl219_4
| ~ spl219_5
| ~ spl219_6
| ~ spl219_7
| ~ spl219_42 ),
inference(sat_conversion,[],[f48426]) ).
cnf(s48,plain,
( spl219_1
| ~ spl219_4
| ~ spl219_5
| ~ spl219_6
| ~ spl219_7
| spl219_42 ),
inference(sat_conversion,[],[f48623]) ).
cnf(s52,plain,
( spl219_1
| ~ spl219_2
| ~ spl219_5
| ~ spl219_7
| spl219_13 ),
inference(sat_conversion,[],[f48666]) ).
cnf(s58,plain,
( spl219_1
| ~ spl219_3
| ~ spl219_5
| ~ spl219_6
| ~ spl219_7
| ~ spl219_8
| ~ spl219_13 ),
inference(sat_conversion,[],[f52251]) ).
cnf(s62,plain,
( spl219_1
| ~ spl219_5
| ~ spl219_11
| spl219_42
| ~ spl219_47 ),
inference(sat_conversion,[],[f52921]) ).
cnf(s66,plain,
( spl219_1
| ~ spl219_5
| ~ spl219_27
| spl219_47 ),
inference(sat_conversion,[],[f57192]) ).
cnf(s72,plain,
( spl219_1
| ~ spl219_5
| ~ spl219_7
| ~ spl219_14
| ~ spl219_42
| spl219_46 ),
inference(sat_conversion,[],[f57588]) ).
cnf(s92,plain,
( ~ spl219_5
| spl219_71 ),
inference(sat_conversion,[],[f60037]) ).
cnf(s121,plain,
( spl219_1
| ~ spl219_5
| spl219_23
| ~ spl219_24
| ~ spl219_46
| ~ spl219_71
| spl219_100 ),
inference(sat_conversion,[],[f73801]) ).
cnf(s123,plain,
( spl219_1
| ~ spl219_5
| spl219_13
| ~ spl219_100 ),
inference(sat_conversion,[],[f77168]) ).
cnf(s126,plain,
spl219_71,
inference(rat,[],[s92,s4]) ).
cnf(s167,plain,
spl219_27,
inference(rat,[],[s27,s4,s5,s1]) ).
cnf(s172,plain,
spl219_17,
inference(rat,[],[s17,s4,s5,s1]) ).
cnf(s174,plain,
spl219_14,
inference(rat,[],[s14,s4,s5,s1]) ).
cnf(s179,plain,
spl219_47,
inference(rat,[],[s66,s1,s4,s167]) ).
cnf(s181,plain,
spl219_24,
inference(rat,[],[s24,s1,s4,s172]) ).
cnf(s186,plain,
( ~ spl219_4
| spl219_2 ),
inference(rat,[],[s121,s23,s72,s11,s48,s123,s13,s4,s1,s181,s126,s6,s174,s5]) ).
cnf(s187,plain,
spl219_4,
inference(rat,[],[s42,s62,s3,s44,s4,s5,s6,s1,s179]) ).
cnf(s191,plain,
spl219_2,
inference(rat,[],[s186,s187]) ).
cnf(s193,plain,
spl219_13,
inference(rat,[],[s52,s1,s6,s4,s191]) ).
cnf(s194,plain,
spl219_3,
inference(rat,[],[s2,s191]) ).
cnf(s196,plain,
$false,
inference(rat,[],[s58,s1,s7,s6,s5,s4,s193,s194]) ).
fof(f77870,plain,
$false,
inference(avatar_sat_refutation,[],[s196]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : LAT322+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.04/0.30 % Computer : n012.cluster.edu
% 0.04/0.30 % Model : x86_64 x86_64
% 0.04/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/0.30 % Memory : 8046.5625MB
% 0.04/0.30 % OS : Linux 6.8.0-71-generic
% 0.04/0.30 % CPULimit : 300
% 0.04/0.30 % WCLimit : 300
% 0.04/0.30 % DateTime : Sun Sep 27 14:36:24 UTC 2026
% 0.04/0.30 % CPUTime :
% 0.04/0.30 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.04/0.32 Running first-order theorem proving
% 0.04/0.32 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.72/2.68 % (2442662)Detected formulas, will run a generic FOF schedule.
% 8.72/2.68 % (2442671)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2190712201:i=119:av=off:ss=axioms_2991 on theBenchmark for (2991ds/119Mi)
% 8.72/2.68 % (2442668)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=2545122569:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2991 on theBenchmark for (2991ds/134677Mi)
% 8.72/2.68 % (2442667)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=1587340840:i=141193_2991 on theBenchmark for (2991ds/141193Mi)
% 8.72/2.68 % (2442670)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2038901357:i=109:sd=1:ins=1:gsp=on:ss=axioms_2991 on theBenchmark for (2991ds/109Mi)
% 8.72/2.68 % (2442669)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=75313581:i=141695:sd=1:nm=32:gsp=on:ss=included_2991 on theBenchmark for (2991ds/141695Mi)
% 8.72/2.68 % (2442673)dis-21_1_sil=8000:lcm=predicate:random_seed=3403161167:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2991 on theBenchmark for (2991ds/129Mi)
% 8.72/2.68 % (2442672)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=833241518:s2a=on:i=139:gtg=position_2991 on theBenchmark for (2991ds/139Mi)
% 8.72/2.68 % (2442672)Instruction limit reached!
% 8.72/2.68 % (2442672)------------------------------
% 8.72/2.68 % (2442672)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.72/2.68 % (2442672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.72/2.68 % (2442672)CaDiCaL version: 2.1.3
% 8.72/2.68 % (2442672)Termination reason: Instruction limit
% 8.72/2.68 % (2442672)Termination phase: Property scanning
% 8.72/2.68 % (2442672)Time elapsed: 0.035 s
% 8.72/2.68 % (2442672)Peak memory usage: 136 MB
% 8.72/2.68 % (2442672)Instructions burned: 141 (million)
% 8.72/2.68 % (2442670)Instruction limit reached!
% 8.72/2.68 % (2442670)------------------------------
% 8.72/2.68 % (2442670)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.72/2.68 % (2442670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.72/2.68 % (2442670)CaDiCaL version: 2.1.3
% 8.72/2.68 % (2442670)Termination reason: Instruction limit
% 8.72/2.68 % (2442670)Termination phase: SInE selection
% 8.72/2.68 % (2442670)Time elapsed: 0.045 s
% 8.72/2.68 % (2442670)Peak memory usage: 136 MB
% 8.72/2.68 % (2442670)Instructions burned: 110 (million)
% 8.72/2.68 % (2442671)Instruction limit reached!
% 8.72/2.68 % (2442671)------------------------------
% 8.72/2.68 % (2442671)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.72/2.68 % (2442671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.72/2.68 % (2442671)CaDiCaL version: 2.1.3
% 8.72/2.68 % (2442671)Termination reason: Instruction limit
% 8.72/2.68 % (2442671)Termination phase: SInE selection
% 8.72/2.68 % (2442671)Time elapsed: 0.050 s
% 8.72/2.68 % (2442671)Peak memory usage: 136 MB
% 8.72/2.68 % (2442671)Instructions burned: 119 (million)
% 8.72/2.68 % (2442673)Instruction limit reached!
% 8.72/2.68 % (2442673)------------------------------
% 8.72/2.68 % (2442673)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.72/2.68 % (2442673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.72/2.68 % (2442673)CaDiCaL version: 2.1.3
% 8.72/2.68 % (2442673)Termination reason: Instruction limit
% 8.72/2.68 % (2442673)Termination phase: SInE selection
% 8.72/2.68 % (2442673)Time elapsed: 0.044 s
% 8.72/2.68 % (2442673)Peak memory usage: 136 MB
% 8.72/2.68 % (2442673)Instructions burned: 129 (million)
% 8.72/2.68 % (2442682)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1282246351:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2989 on theBenchmark for (2989ds/157Mi)
% 8.72/2.68 % (2442683)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1249678820:i=325:sd=1:ss=axioms:sgt=32_2989 on theBenchmark for (2989ds/325Mi)
% 8.72/2.68 % (2442684)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=763729151:s2a=on:i=248:s2at=1.23:gtg=position_2989 on theBenchmark for (2989ds/248Mi)
% 8.72/2.68 % (2442681)lrs+10_1_sil=8000:sp=occurrence:random_seed=2522767602:i=285:sd=3:ss=axioms:sgt=8_2989 on theBenchmark for (2989ds/285Mi)
% 8.72/2.68 % (2442682)Instruction limit reached!
% 15.06/3.48 % (2442682)------------------------------
% 15.06/3.48 % (2442682)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.06/3.48 % (2442682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.06/3.48 % (2442682)CaDiCaL version: 2.1.3
% 15.06/3.48 % (2442682)Termination reason: Instruction limit
% 15.06/3.48 % (2442682)Termination phase: Property scanning
% 15.06/3.48 % (2442682)Time elapsed: 0.038 s
% 15.06/3.48 % (2442682)Peak memory usage: 136 MB
% 15.06/3.48 % (2442682)Instructions burned: 161 (million)
% 15.06/3.48 % (2442684)Instruction limit reached!
% 15.06/3.48 % (2442684)------------------------------
% 15.06/3.48 % (2442684)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.06/3.48 % (2442684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.06/3.48 % (2442684)CaDiCaL version: 2.1.3
% 15.06/3.48 % (2442684)Termination reason: Instruction limit
% 15.06/3.48 % (2442684)Termination phase: Property scanning
% 15.06/3.48 % (2442684)Time elapsed: 0.059 s
% 15.06/3.48 % (2442684)Peak memory usage: 136 MB
% 15.06/3.48 % (2442684)Instructions burned: 252 (million)
% 15.06/3.48 % (2442683)Refutation not found, incomplete strategy
% 15.06/3.48 % (2442683)------------------------------
% 15.06/3.48 % (2442683)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.06/3.48 % (2442683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.06/3.48 % (2442683)CaDiCaL version: 2.1.3
% 15.06/3.48 % (2442683)Termination reason: Refutation not found, incomplete strategy
% 15.06/3.48 % (2442683)Time elapsed: 0.113 s
% 15.06/3.48 % (2442683)Peak memory usage: 142 MB
% 15.06/3.48 % (2442683)Instructions burned: 245 (million)
% 15.06/3.48 % (2442681)Instruction limit reached!
% 15.06/3.48 % (2442681)------------------------------
% 15.06/3.48 % (2442681)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.06/3.48 % (2442681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.06/3.48 % (2442681)CaDiCaL version: 2.1.3
% 15.06/3.48 % (2442681)Termination reason: Instruction limit
% 15.06/3.48 % (2442681)Termination phase: Saturation
% 15.06/3.48 % (2442681)Time elapsed: 0.127 s
% 15.06/3.48 % (2442681)Peak memory usage: 141 MB
% 15.06/3.48 % (2442681)Instructions burned: 289 (million)
% 15.06/3.48 % (2442689)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2633394069:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2988 on theBenchmark for (2988ds/294Mi)
% 15.06/3.48 % (2442690)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2530739449:i=2350_2988 on theBenchmark for (2988ds/2350Mi)
% 15.06/3.48 % (2442691)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1753684094:cts=off:i=113:fsr=off:ss=included:sgt=4_2987 on theBenchmark for (2987ds/113Mi)
% 15.06/3.48 % (2442689)Instruction limit reached!
% 15.06/3.48 % (2442689)------------------------------
% 15.06/3.48 % (2442689)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.06/3.48 % (2442689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.06/3.48 % (2442689)CaDiCaL version: 2.1.3
% 15.06/3.48 % (2442689)Termination reason: Instruction limit
% 15.06/3.48 % (2442689)Termination phase: SInE selection
% 15.06/3.48 % (2442689)Time elapsed: 0.111 s
% 15.06/3.48 % (2442689)Peak memory usage: 137 MB
% 15.06/3.48 % (2442689)Instructions burned: 295 (million)
% 15.06/3.48 % (2442683)------------------------------
% 15.06/3.48 % (2442683)------------------------------
% 15.06/3.48 % (2442691)Instruction limit reached!
% 15.06/3.48 % (2442691)------------------------------
% 15.06/3.48 % (2442691)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.06/3.48 % (2442691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.06/3.48 % (2442691)CaDiCaL version: 2.1.3
% 15.06/3.48 % (2442691)Termination reason: Instruction limit
% 15.06/3.48 % (2442691)Termination phase: SInE selection
% 15.06/3.48 % (2442691)Time elapsed: 0.051 s
% 15.06/3.48 % (2442691)Peak memory usage: 136 MB
% 15.06/3.48 % (2442691)Instructions burned: 113 (million)
% 15.06/3.48 % (2442695)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3505007256:i=127:av=off:fsr=off:sup=off_2986 on theBenchmark for (2986ds/127Mi)
% 15.06/3.48 % (2442696)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=750208999:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2986 on theBenchmark for (2986ds/114Mi)
% 15.06/3.48 % (2442696)Instruction limit reached!
% 15.06/3.48 % (2442696)------------------------------
% 18.52/4.35 % (2442696)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.52/4.35 % (2442696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.52/4.35 % (2442696)CaDiCaL version: 2.1.3
% 18.52/4.35 % (2442696)Termination reason: Instruction limit
% 18.52/4.35 % (2442696)Termination phase: Property scanning
% 18.52/4.35 % (2442696)Time elapsed: 0.029 s
% 18.52/4.35 % (2442696)Peak memory usage: 136 MB
% 18.52/4.35 % (2442696)Instructions burned: 119 (million)
% 18.52/4.35 % (2442697)lrs+10_1_sil=8000:sp=occurrence:random_seed=1640880164:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2985 on theBenchmark for (2985ds/907Mi)
% 18.52/4.35 % (2442695)Instruction limit reached!
% 18.52/4.35 % (2442695)------------------------------
% 18.52/4.35 % (2442695)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.52/4.35 % (2442695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.52/4.35 % (2442695)CaDiCaL version: 2.1.3
% 18.52/4.35 % (2442695)Termination reason: Instruction limit
% 18.52/4.35 % (2442695)Termination phase: Preprocessing 1
% 18.52/4.35 % (2442695)Time elapsed: 0.058 s
% 18.52/4.35 % (2442695)Peak memory usage: 137 MB
% 18.52/4.35 % (2442695)Instructions burned: 129 (million)
% 18.52/4.35 % (2442701)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1744114644:i=437:sd=1:aac=none:ss=included_2984 on theBenchmark for (2984ds/437Mi)
% 18.52/4.35 % (2442702)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=280171604:i=5202:ss=axioms:sgt=16_2984 on theBenchmark for (2984ds/5202Mi)
% 18.52/4.35 % (2442701)Refutation not found, incomplete strategy
% 18.52/4.35 % (2442701)------------------------------
% 18.52/4.35 % (2442701)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.52/4.35 % (2442701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.52/4.35 % (2442701)CaDiCaL version: 2.1.3
% 18.52/4.35 % (2442701)Termination reason: Refutation not found, incomplete strategy
% 18.52/4.35 % (2442701)Time elapsed: 0.142 s
% 18.52/4.35 % (2442701)Peak memory usage: 143 MB
% 18.52/4.35 % (2442701)Instructions burned: 331 (million)
% 18.52/4.35 % (2442697)Instruction limit reached!
% 18.52/4.35 % (2442697)------------------------------
% 18.52/4.35 % (2442697)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.52/4.35 % (2442697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.52/4.35 % (2442697)CaDiCaL version: 2.1.3
% 18.52/4.35 % (2442697)Termination reason: Instruction limit
% 18.52/4.35 % (2442697)Termination phase: Property scanning
% 18.52/4.35 % (2442697)Time elapsed: 0.368 s
% 18.52/4.35 % (2442697)Peak memory usage: 159 MB
% 18.52/4.35 % (2442697)Instructions burned: 907 (million)
% 18.52/4.35 % (2442701)------------------------------
% 18.52/4.35 % (2442701)------------------------------
% 18.52/4.35 % (2442705)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=717979523:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2981 on theBenchmark for (2981ds/134Mi)
% 18.52/4.35 % (2442706)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1453314032:st=8:i=592:sd=3:ep=RST:ss=axioms_2980 on theBenchmark for (2980ds/592Mi)
% 18.52/4.35 % (2442705)Instruction limit reached!
% 18.52/4.35 % (2442705)------------------------------
% 18.52/4.35 % (2442705)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.52/4.35 % (2442705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.52/4.35 % (2442705)CaDiCaL version: 2.1.3
% 18.52/4.35 % (2442705)Termination reason: Instruction limit
% 18.52/4.35 % (2442705)Termination phase: SInE selection
% 18.52/4.35 % (2442705)Time elapsed: 0.063 s
% 18.52/4.35 % (2442705)Peak memory usage: 136 MB
% 18.52/4.35 % (2442705)Instructions burned: 136 (million)
% 18.52/4.35 % (2442690)Instruction limit reached!
% 18.52/4.35 % (2442690)------------------------------
% 18.52/4.35 % (2442690)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.52/4.35 % (2442690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.52/4.35 % (2442690)CaDiCaL version: 2.1.3
% 18.52/4.35 % (2442690)Termination reason: Instruction limit
% 18.52/4.35 % (2442690)Termination phase: Property scanning
% 18.52/4.35 % (2442690)Time elapsed: 0.878 s
% 18.52/4.35 % (2442690)Peak memory usage: 233 MB
% 18.52/4.35 % (2442690)Instructions burned: 2354 (million)
% 18.52/4.35 % (2442709)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=4112859475:st=3:i=13193:sd=3:ss=axioms_2979 on theBenchmark for (2979ds/13193Mi)
% 18.52/4.35 % (2442711)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=3648574093:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2978 on theBenchmark for (2978ds/125Mi)
% 18.52/4.35 % (2442711)Instruction limit reached!
% 18.52/4.35 % (2442711)------------------------------
% 18.52/4.35 % (2442711)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.52/4.35 % (2442711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.52/4.35 % (2442711)CaDiCaL version: 2.1.3
% 18.52/4.35 % (2442711)Termination reason: Instruction limit
% 18.52/4.35 % (2442711)Termination phase: Property scanning
% 18.52/4.35 % (2442711)Time elapsed: 0.031 s
% 18.52/4.35 % (2442711)Peak memory usage: 136 MB
% 18.52/4.35 % (2442711)Instructions burned: 129 (million)
% 18.52/4.35 % (2442706)Instruction limit reached!
% 18.52/4.35 % (2442706)------------------------------
% 18.52/4.35 % (2442706)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.52/4.35 % (2442706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.52/4.35 % (2442706)CaDiCaL version: 2.1.3
% 18.52/4.35 % (2442706)Termination reason: Instruction limit
% 18.52/4.35 % (2442706)Termination phase: Naming
% 18.52/4.35 % (2442706)Time elapsed: 0.287 s
% 18.52/4.35 % (2442706)Peak memory usage: 151 MB
% 18.52/4.35 % (2442706)Instructions burned: 593 (million)
% 18.52/4.35 % (2442713)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1915076888:i=134:gtgl=5:slsql=off:gtg=exists_sym_2977 on theBenchmark for (2977ds/134Mi)
% 18.52/4.35 % (2442714)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=4158969609:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2976 on theBenchmark for (2976ds/141Mi)
% 18.52/4.35 % (2442713)Instruction limit reached!
% 18.52/4.35 % (2442713)------------------------------
% 18.52/4.35 % (2442713)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.52/4.35 % (2442713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.52/4.35 % (2442713)CaDiCaL version: 2.1.3
% 18.52/4.35 % (2442713)Termination reason: Instruction limit
% 18.52/4.35 % (2442713)Termination phase: Property scanning
% 18.52/4.35 % (2442713)Time elapsed: 0.033 s
% 18.52/4.35 % (2442713)Peak memory usage: 136 MB
% 18.52/4.35 % (2442713)Instructions burned: 136 (million)
% 18.52/4.35 % (2442714)Instruction limit reached!
% 18.52/4.35 % (2442714)------------------------------
% 18.52/4.35 % (2442714)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.52/4.35 % (2442714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.52/4.35 % (2442714)CaDiCaL version: 2.1.3
% 18.52/4.35 % (2442714)Termination reason: Instruction limit
% 18.52/4.35 % (2442714)Termination phase: SInE selection
% 18.52/4.35 % (2442714)Time elapsed: 0.062 s
% 18.52/4.35 % (2442714)Peak memory usage: 136 MB
% 18.52/4.35 % (2442714)Instructions burned: 142 (million)
% 18.52/4.35 % (2442717)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=689825440:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2975 on theBenchmark for (2975ds/431Mi)
% 18.52/4.35 % (2442718)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=1621003267:i=6060:aac=none:ins=25_2975 on theBenchmark for (2975ds/6060Mi)
% 18.52/4.35 % (2442717)Refutation not found, incomplete strategy
% 18.52/4.35 % (2442717)------------------------------
% 18.52/4.35 % (2442717)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.52/4.35 % (2442717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.52/4.35 % (2442717)CaDiCaL version: 2.1.3
% 18.52/4.35 % (2442717)Termination reason: Refutation not found, incomplete strategy
% 18.52/4.35 % (2442717)Time elapsed: 0.119 s
% 18.52/4.35 % (2442717)Peak memory usage: 142 MB
% 18.52/4.35 % (2442717)Instructions burned: 248 (million)
% 18.52/4.35 % (2442717)------------------------------
% 18.52/4.35 % (2442717)------------------------------
% 18.52/4.35 % (2442721)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=314177523:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2972 on theBenchmark for (2972ds/150Mi)
% 18.52/4.35 % (2442721)Instruction limit reached!
% 18.52/4.35 % (2442721)------------------------------
% 18.52/4.35 % (2442721)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.52/4.35 % (2442721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.52/4.35 % (2442721)CaDiCaL version: 2.1.3
% 18.52/4.35 % (2442721)Termination reason: Instruction limit
% 18.52/4.35 % (2442721)Termination phase: SInE selection
% 18.52/4.35 % (2442721)Time elapsed: 0.069 s
% 18.52/4.35 % (2442721)Peak memory usage: 136 MB
% 18.52/4.35 % (2442721)Instructions burned: 152 (million)
% 18.52/4.35 % (2442723)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1243936947:i=14155:bd=all_2970 on theBenchmark for (2970ds/14155Mi)
% 18.52/4.35 % (2442669)First to succeed.
% 18.52/4.35 % (2442669)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2442662"
% 18.52/4.35 % (2442709)Also succeeded, but the first one will report.
% 18.52/4.35 % (2442669)Refutation found. Thanks to Tanya!
% 18.52/4.35 % SZS status Theorem for theBenchmark
% 18.52/4.35 % SZS output start Proof for theBenchmark
% See solution above
% 21.81/4.45 % (2442669)------------------------------
% 21.81/4.45 % (2442669)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.81/4.45 % (2442669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.81/4.45 % (2442669)CaDiCaL version: 2.1.3
% 21.81/4.45 % (2442669)Termination reason: Refutation
% 21.81/4.45 % (2442669)Time elapsed: 2.640 s
% 21.81/4.45 % (2442669)Peak memory usage: 237 MB
% 21.81/4.45 % (2442669)Instructions burned: 8021 (million)
% 21.81/4.45 % (2442669)------------------------------
% 21.81/4.45 % (2442669)------------------------------
% 21.81/4.45 % (2442662)Success in time 3.831 s
% 21.81/4.45 % Vampire exiting
%------------------------------------------------------------------------------