%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT306+4 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n020.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:45 AM UTC 2026
% Result : Theorem 15.09s 6.54s
% Output : Refutation 27.46s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 39
% Syntax : Number of formulae : 256 ( 33 unt; 21 def)
% Number of atoms : 1075 ( 66 equ)
% Maximal formula atoms : 12 ( 4 avg)
% Number of connectives : 1377 ( 558 ~; 646 |; 111 &)
% ( 33 <=>; 29 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 42 ( 40 usr; 21 prp; 0-3 aty)
% Number of functors : 12 ( 12 usr; 1 con; 0-3 aty)
% Number of variables : 160 ( 0 sgn 158 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f675,axiom,
! [X0,X1] :
( r2_hidden(X0,X1)
=> m1_subset_1(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t1_subset) ).
fof(f21512,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_filter_0(X1,X0)
=> ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v14_lattices(X0)
& l3_lattices(X0) )
=> r2_hidden(k6_lattices(X0),X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t12_filter_0) ).
fof(f21515,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> m1_filter_0(u1_struct_0(X0),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t15_filter_0) ).
fof(f21535,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_filter_0(X1,X0)
=> ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v13_lattices(X0)
& l3_lattices(X0)
& r2_hidden(k5_lattices(X0),X1) )
=> ( X1 = k1_filter_0(X0)
& X1 = u1_struct_0(X0) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t32_filter_0) ).
fof(f21600,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_filter_0(X1,X0)
=> ( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m1_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/sandbox2/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/sandbox2/benchmark/theBenchmark.p',fc6_lattice2) ).
fof(f22780,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l3_lattices(X0) )
=> ( u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0))
& u2_lattices(X0) = u1_lattices(k1_lattice2(X0))
& u1_lattices(X0) = u2_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t18_lattice2) ).
fof(f22828,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( v14_lattices(X0)
<=> v13_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t64_lattice2) ).
fof(f22843,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v14_lattices(X0)
& l3_lattices(X0) )
=> k6_lattices(X0) = k5_lattices(k1_lattice2(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t79_lattice2) ).
fof(f22852,axiom,
! [X0] :
( l3_lattices(X0)
=> ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k1_lattice2) ).
fof(f34607,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_filter_2(X1,X0)
<=> m1_filter_0(X1,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_m1_filter_2) ).
fof(f34612,axiom,
! [X0,X1,X2] :
( ( ~ v1_xboole_0(X0)
& m1_subset_1(X1,k1_zfmisc_1(X0))
& m1_subset_1(X2,k1_zfmisc_1(X0)) )
=> ( r1_filter_2(X0,X1,X2)
<=> X1 = X2 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_r1_filter_2) ).
fof(f34642,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& m1_subset_1(X1,u1_struct_0(X0)) )
=> m2_filter_2(k18_filter_2(X0,X1),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k18_filter_2) ).
fof(f34676,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/sandbox2/benchmark/theBenchmark.p',t21_filter_2) ).
fof(f34688,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> k17_filter_2(X0) = u1_struct_0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d8_filter_2) ).
fof(f34692,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ( r2_hidden(X1,k18_filter_2(X0,X1))
& r2_hidden(k4_lattices(X0,X1,X2),k18_filter_2(X0,X1))
& r2_hidden(k4_lattices(X0,X2,X1),k18_filter_2(X0,X1)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t31_filter_2) ).
fof(f34693,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( v14_lattices(X0)
=> r1_filter_2(u1_struct_0(X0),k17_filter_2(X0),k18_filter_2(X0,k6_lattices(X0))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t32_filter_2) ).
fof(f34694,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( v14_lattices(X0)
=> r1_filter_2(u1_struct_0(X0),k17_filter_2(X0),k18_filter_2(X0,k6_lattices(X0))) ) ),
inference(negated_conjecture,[status(cth)],[f34693]) ).
fof(f34728,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( ~ v3_struct_0(k1_lattice2(X0))
& v3_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)) ) ),
inference(pure_predicate_removal,[],[f22752]) ).
fof(f34741,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,[],[f34607]) ).
fof(f34742,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,[],[f34741]) ).
fof(f34751,plain,
! [X0,X1,X2] :
( ( r1_filter_2(X0,X1,X2)
<=> X1 = X2 )
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f34612]) ).
fof(f34752,plain,
! [X0,X1,X2] :
( ( r1_filter_2(X0,X1,X2)
<=> X1 = X2 )
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(flattening,[],[f34751]) ).
fof(f34811,plain,
! [X0,X1] :
( m2_filter_2(k18_filter_2(X0,X1),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f34642]) ).
fof(f34812,plain,
! [X0,X1] :
( m2_filter_2(k18_filter_2(X0,X1),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(flattening,[],[f34811]) ).
fof(f34876,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,[],[f34676]) ).
fof(f34877,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,[],[f34876]) ).
fof(f34900,plain,
! [X0] :
( k17_filter_2(X0) = u1_struct_0(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f34688]) ).
fof(f34901,plain,
! [X0] :
( k17_filter_2(X0) = u1_struct_0(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f34900]) ).
fof(f34908,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( r2_hidden(X1,k18_filter_2(X0,X1))
& r2_hidden(k4_lattices(X0,X1,X2),k18_filter_2(X0,X1))
& r2_hidden(k4_lattices(X0,X2,X1),k18_filter_2(X0,X1)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f34692]) ).
fof(f34909,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( r2_hidden(X1,k18_filter_2(X0,X1))
& r2_hidden(k4_lattices(X0,X1,X2),k18_filter_2(X0,X1))
& r2_hidden(k4_lattices(X0,X2,X1),k18_filter_2(X0,X1)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f34908]) ).
fof(f34910,plain,
? [X0] :
( ~ r1_filter_2(u1_struct_0(X0),k17_filter_2(X0),k18_filter_2(X0,k6_lattices(X0)))
& v14_lattices(X0)
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(ennf_transformation,[],[f34694]) ).
fof(f34911,plain,
? [X0] :
( ~ r1_filter_2(u1_struct_0(X0),k17_filter_2(X0),k18_filter_2(X0,k6_lattices(X0)))
& v14_lattices(X0)
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(flattening,[],[f34910]) ).
fof(f34916,plain,
! [X0,X1] :
( m1_subset_1(X0,X1)
| ~ r2_hidden(X0,X1) ),
inference(ennf_transformation,[],[f675]) ).
fof(f34943,plain,
! [X0] :
( ! [X1] :
( ( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f21600]) ).
fof(f34944,plain,
! [X0] :
( ! [X1] :
( ( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f34943]) ).
fof(f34945,plain,
! [X0] :
( m1_filter_0(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f21515]) ).
fof(f34946,plain,
! [X0] :
( m1_filter_0(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f34945]) ).
fof(f34968,plain,
! [X0] :
( ! [X1] :
( ( X1 = k1_filter_0(X0)
& X1 = u1_struct_0(X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v13_lattices(X0)
| ~ l3_lattices(X0)
| ~ r2_hidden(k5_lattices(X0),X1)
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f21535]) ).
fof(f34969,plain,
! [X0] :
( ! [X1] :
( ( X1 = k1_filter_0(X0)
& X1 = u1_struct_0(X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v13_lattices(X0)
| ~ l3_lattices(X0)
| ~ r2_hidden(k5_lattices(X0),X1)
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f34968]) ).
fof(f35024,plain,
! [X0] :
( ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f22852]) ).
fof(f35029,plain,
! [X0] :
( ( v14_lattices(X0)
<=> v13_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f22828]) ).
fof(f35030,plain,
! [X0] :
( ( v14_lattices(X0)
<=> v13_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35029]) ).
fof(f35041,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(f35042,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,[],[f35041]) ).
fof(f35044,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_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,[],[f34728]) ).
fof(f35045,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_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,[],[f35044]) ).
fof(f35046,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(f35047,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35046]) ).
fof(f35251,plain,
! [X0] :
( k6_lattices(X0) = k5_lattices(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v14_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f22843]) ).
fof(f35252,plain,
! [X0] :
( k6_lattices(X0) = k5_lattices(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v14_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35251]) ).
fof(f35267,plain,
! [X0] :
( ! [X1] :
( r2_hidden(k6_lattices(X0),X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v14_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f21512]) ).
fof(f35268,plain,
! [X0] :
( ! [X1] :
( r2_hidden(k6_lattices(X0),X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v14_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35267]) ).
fof(f35363,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,[],[f34742]) ).
fof(f35365,plain,
! [X0,X1,X2] :
( ( ( r1_filter_2(X0,X1,X2)
| X1 != X2 )
& ( X1 = X2
| ~ r1_filter_2(X0,X1,X2) ) )
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(nnf_transformation,[],[f34752]) ).
fof(f35383,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,[],[f34877]) ).
fof(f35390,plain,
( ~ r1_filter_2(u1_struct_0(sK18),k17_filter_2(sK18),k18_filter_2(sK18,k6_lattices(sK18)))
& v14_lattices(sK18)
& ~ v3_struct_0(sK18)
& v10_lattices(sK18)
& l3_lattices(sK18) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18]),skolemize(X0,sK18)],[f34911]) ).
fof(f35438,plain,
! [X0] :
( ( ( v14_lattices(X0)
| ~ v13_lattices(k1_lattice2(X0)) )
& ( v13_lattices(k1_lattice2(X0))
| ~ v14_lattices(X0) ) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f35030]) ).
fof(f35593,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,[],[f35363]) ).
fof(f35601,plain,
! [X2,X0,X1] :
( r1_filter_2(X0,X1,X2)
| X1 != X2
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f35365]) ).
fof(f35633,plain,
! [X0,X1] :
( m2_filter_2(k18_filter_2(X0,X1),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f34812]) ).
fof(f35706,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,[],[f35383]) ).
fof(f35747,plain,
! [X0] :
( u1_struct_0(X0) = k17_filter_2(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f34901]) ).
fof(f35755,plain,
! [X2,X0,X1] :
( r2_hidden(X1,k18_filter_2(X0,X1))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f34909]) ).
fof(f35756,plain,
l3_lattices(sK18),
inference(cnf_transformation,[],[f35390]) ).
fof(f35757,plain,
v10_lattices(sK18),
inference(cnf_transformation,[],[f35390]) ).
fof(f35758,plain,
~ v3_struct_0(sK18),
inference(cnf_transformation,[],[f35390]) ).
fof(f35759,plain,
v14_lattices(sK18),
inference(cnf_transformation,[],[f35390]) ).
fof(f35760,plain,
~ r1_filter_2(u1_struct_0(sK18),k17_filter_2(sK18),k18_filter_2(sK18,k6_lattices(sK18))),
inference(cnf_transformation,[],[f35390]) ).
fof(f35765,plain,
! [X0,X1] :
( m1_subset_1(X0,X1)
| ~ r2_hidden(X0,X1) ),
inference(cnf_transformation,[],[f34916]) ).
fof(f35799,plain,
! [X0,X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m1_filter_0(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f34944]) ).
fof(f35800,plain,
! [X0,X1] :
( ~ v1_xboole_0(X1)
| ~ m1_filter_0(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f34944]) ).
fof(f35801,plain,
! [X0] :
( m1_filter_0(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f34946]) ).
fof(f35862,plain,
! [X0,X1] :
( u1_struct_0(X0) = X1
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v13_lattices(X0)
| ~ l3_lattices(X0)
| ~ r2_hidden(k5_lattices(X0),X1)
| ~ m1_filter_0(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f34969]) ).
fof(f35909,plain,
! [X0] :
( l3_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35024]) ).
fof(f35921,plain,
! [X0] :
( v13_lattices(k1_lattice2(X0))
| ~ v14_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35438]) ).
fof(f35932,plain,
! [X0] :
( u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35042]) ).
fof(f35934,plain,
! [X0] :
( v10_lattices(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35045]) ).
fof(f35943,plain,
! [X0] :
( ~ v3_struct_0(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35047]) ).
fof(f36220,plain,
! [X0] :
( k6_lattices(X0) = k5_lattices(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v14_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35252]) ).
fof(f36230,plain,
! [X0,X1] :
( r2_hidden(k6_lattices(X0),X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v14_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_filter_0(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35268]) ).
fof(f36399,plain,
! [X2,X0] :
( r1_filter_2(X0,X2,X2)
| v1_xboole_0(X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(equality_resolution,[],[f35601]) ).
fof(f36515,plain,
! [X2,X0] :
( ~ m1_subset_1(X2,u1_struct_0(X0))
| sP152(X0) ),
inference(cnf_transformation,[],[f36515_D]) ).
fof(f36515_D,definition,
! [X0] :
( ! [X2] : ~ m1_subset_1(X2,u1_struct_0(X0))
<=> ~ sP152(X0) ),
introduced(definition,[new_symbols(definition,[sP152])],[general_splitting_component_introduction]) ).
fof(f36516,plain,
! [X0,X1] :
( r2_hidden(X1,k18_filter_2(X0,X1))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ sP152(X0) ),
inference(general_splitting,[],[f35755,f36515_D]) ).
fof(f36537,plain,
! [X2,X0] :
( r1_filter_2(X0,X2,X2)
| v1_xboole_0(X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(duplicate_literal_removal,[],[f36399]) ).
fof(f36539,plain,
! [X0,X1] :
( u1_struct_0(X0) = X1
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v13_lattices(X0)
| ~ l3_lattices(X0)
| ~ r2_hidden(k5_lattices(X0),X1)
| ~ m1_filter_0(X1,X0) ),
inference(duplicate_literal_removal,[],[f35862]) ).
fof(f36550,plain,
! [X0,X1] :
( r2_hidden(k6_lattices(X0),X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v14_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_filter_0(X1,X0) ),
inference(duplicate_literal_removal,[],[f36230]) ).
fof(f36564,definition,
( spl163_1
<=> r1_filter_2(u1_struct_0(sK18),k17_filter_2(sK18),k18_filter_2(sK18,k6_lattices(sK18))) ),
introduced(definition,[new_symbols(definition,[spl163_1])],[avatar_definition]) ).
fof(f36566,plain,
( ~ r1_filter_2(u1_struct_0(sK18),k17_filter_2(sK18),k18_filter_2(sK18,k6_lattices(sK18)))
| spl163_1 ),
inference(avatar_component_clause,[],[f36564]) ).
fof(f36567,plain,
~ spl163_1,
inference(avatar_split_clause,[],[f35760,f36564]) ).
fof(f36569,definition,
( spl163_2
<=> v3_struct_0(sK18) ),
introduced(definition,[new_symbols(definition,[spl163_2])],[avatar_definition]) ).
fof(f36571,plain,
( ~ v3_struct_0(sK18)
| spl163_2 ),
inference(avatar_component_clause,[],[f36569]) ).
fof(f36572,plain,
~ spl163_2,
inference(avatar_split_clause,[],[f35758,f36569]) ).
fof(f36574,definition,
( spl163_3
<=> l3_lattices(sK18) ),
introduced(definition,[new_symbols(definition,[spl163_3])],[avatar_definition]) ).
fof(f36576,plain,
( l3_lattices(sK18)
| ~ spl163_3 ),
inference(avatar_component_clause,[],[f36574]) ).
fof(f36577,plain,
spl163_3,
inference(avatar_split_clause,[],[f35756,f36574]) ).
fof(f36579,definition,
( spl163_4
<=> v10_lattices(sK18) ),
introduced(definition,[new_symbols(definition,[spl163_4])],[avatar_definition]) ).
fof(f36581,plain,
( v10_lattices(sK18)
| ~ spl163_4 ),
inference(avatar_component_clause,[],[f36579]) ).
fof(f36582,plain,
spl163_4,
inference(avatar_split_clause,[],[f35757,f36579]) ).
fof(f36630,definition,
( spl163_5
<=> v14_lattices(sK18) ),
introduced(definition,[new_symbols(definition,[spl163_5])],[avatar_definition]) ).
fof(f36632,plain,
( v14_lattices(sK18)
| ~ spl163_5 ),
inference(avatar_component_clause,[],[f36630]) ).
fof(f36633,plain,
spl163_5,
inference(avatar_split_clause,[],[f35759,f36630]) ).
fof(f36721,plain,
( ! [X0] :
( m1_filter_2(X0,k1_lattice2(sK18))
| ~ m2_filter_2(X0,sK18)
| ~ v10_lattices(sK18)
| ~ l3_lattices(sK18) )
| spl163_2 ),
inference(resolution,[],[f36571,f35706]) ).
fof(f36762,plain,
( u1_struct_0(sK18) = k17_filter_2(sK18)
| ~ v10_lattices(sK18)
| ~ l3_lattices(sK18)
| spl163_2 ),
inference(resolution,[],[f36571,f35747]) ).
fof(f36787,plain,
( m1_filter_0(u1_struct_0(sK18),sK18)
| ~ v10_lattices(sK18)
| ~ l3_lattices(sK18)
| spl163_2 ),
inference(resolution,[],[f36571,f35801]) ).
fof(f36868,plain,
( v13_lattices(k1_lattice2(sK18))
| ~ v14_lattices(sK18)
| ~ v10_lattices(sK18)
| ~ l3_lattices(sK18)
| spl163_2 ),
inference(resolution,[],[f36571,f35921]) ).
fof(f36875,plain,
( u1_struct_0(sK18) = u1_struct_0(k1_lattice2(sK18))
| ~ l3_lattices(sK18)
| spl163_2 ),
inference(resolution,[],[f36571,f35932]) ).
fof(f36876,plain,
( v10_lattices(k1_lattice2(sK18))
| ~ v10_lattices(sK18)
| ~ l3_lattices(sK18)
| spl163_2 ),
inference(resolution,[],[f36571,f35934]) ).
fof(f36885,plain,
( ~ v3_struct_0(k1_lattice2(sK18))
| ~ l3_lattices(sK18)
| spl163_2 ),
inference(resolution,[],[f36571,f35943]) ).
fof(f36962,plain,
( k6_lattices(sK18) = k5_lattices(k1_lattice2(sK18))
| ~ v10_lattices(sK18)
| ~ v14_lattices(sK18)
| ~ l3_lattices(sK18)
| spl163_2 ),
inference(resolution,[],[f36571,f36220]) ).
fof(f37302,plain,
( k6_lattices(sK18) = k5_lattices(k1_lattice2(sK18))
| ~ v14_lattices(sK18)
| ~ l3_lattices(sK18)
| spl163_2
| ~ spl163_4 ),
inference(forward_subsumption_resolution,[],[f36962,f36581]) ).
fof(f37377,plain,
( ~ v3_struct_0(k1_lattice2(sK18))
| spl163_2
| ~ spl163_3 ),
inference(forward_subsumption_resolution,[],[f36885,f36576]) ).
fof(f37384,plain,
( v10_lattices(k1_lattice2(sK18))
| ~ l3_lattices(sK18)
| spl163_2
| ~ spl163_4 ),
inference(forward_subsumption_resolution,[],[f36876,f36581]) ).
fof(f37385,plain,
( u1_struct_0(sK18) = u1_struct_0(k1_lattice2(sK18))
| spl163_2
| ~ spl163_3 ),
inference(forward_subsumption_resolution,[],[f36875,f36576]) ).
fof(f37391,plain,
( v13_lattices(k1_lattice2(sK18))
| ~ v10_lattices(sK18)
| ~ l3_lattices(sK18)
| spl163_2
| ~ spl163_5 ),
inference(forward_subsumption_resolution,[],[f36868,f36632]) ).
fof(f37472,plain,
( m1_filter_0(u1_struct_0(sK18),sK18)
| ~ l3_lattices(sK18)
| spl163_2
| ~ spl163_4 ),
inference(forward_subsumption_resolution,[],[f36787,f36581]) ).
fof(f37497,plain,
( u1_struct_0(sK18) = k17_filter_2(sK18)
| ~ l3_lattices(sK18)
| spl163_2
| ~ spl163_4 ),
inference(forward_subsumption_resolution,[],[f36762,f36581]) ).
fof(f37538,plain,
( ! [X0] :
( m1_filter_2(X0,k1_lattice2(sK18))
| ~ m2_filter_2(X0,sK18)
| ~ l3_lattices(sK18) )
| spl163_2
| ~ spl163_4 ),
inference(forward_subsumption_resolution,[],[f36721,f36581]) ).
fof(f37756,plain,
( k6_lattices(sK18) = k5_lattices(k1_lattice2(sK18))
| ~ l3_lattices(sK18)
| spl163_2
| ~ spl163_4
| ~ spl163_5 ),
inference(forward_subsumption_resolution,[],[f37302,f36632]) ).
fof(f37807,plain,
( v10_lattices(k1_lattice2(sK18))
| spl163_2
| ~ spl163_3
| ~ spl163_4 ),
inference(forward_subsumption_resolution,[],[f37384,f36576]) ).
fof(f37810,plain,
( v13_lattices(k1_lattice2(sK18))
| ~ l3_lattices(sK18)
| spl163_2
| ~ spl163_4
| ~ spl163_5 ),
inference(forward_subsumption_resolution,[],[f37391,f36581]) ).
fof(f37891,plain,
( m1_filter_0(u1_struct_0(sK18),sK18)
| spl163_2
| ~ spl163_3
| ~ spl163_4 ),
inference(forward_subsumption_resolution,[],[f37472,f36576]) ).
fof(f37916,plain,
( u1_struct_0(sK18) = k17_filter_2(sK18)
| spl163_2
| ~ spl163_3
| ~ spl163_4 ),
inference(forward_subsumption_resolution,[],[f37497,f36576]) ).
fof(f37957,plain,
( ! [X0] :
( m1_filter_2(X0,k1_lattice2(sK18))
| ~ m2_filter_2(X0,sK18) )
| spl163_2
| ~ spl163_3
| ~ spl163_4 ),
inference(forward_subsumption_resolution,[],[f37538,f36576]) ).
fof(f38069,plain,
( k6_lattices(sK18) = k5_lattices(k1_lattice2(sK18))
| spl163_2
| ~ spl163_3
| ~ spl163_4
| ~ spl163_5 ),
inference(forward_subsumption_resolution,[],[f37756,f36576]) ).
fof(f38071,plain,
( v13_lattices(k1_lattice2(sK18))
| spl163_2
| ~ spl163_3
| ~ spl163_4
| ~ spl163_5 ),
inference(forward_subsumption_resolution,[],[f37810,f36576]) ).
fof(f38946,plain,
( l3_lattices(k1_lattice2(sK18))
| ~ spl163_3 ),
inference(resolution,[],[f36576,f35909]) ).
fof(f39735,definition,
( spl163_9
<=> u1_struct_0(sK18) = k17_filter_2(sK18) ),
introduced(definition,[new_symbols(definition,[spl163_9])],[avatar_definition]) ).
fof(f39737,plain,
( u1_struct_0(sK18) = k17_filter_2(sK18)
| ~ spl163_9 ),
inference(avatar_component_clause,[],[f39735]) ).
fof(f39738,plain,
( spl163_9
| spl163_2
| ~ spl163_3
| ~ spl163_4 ),
inference(avatar_split_clause,[],[f37916,f36579,f36574,f36569,f39735]) ).
fof(f39742,definition,
( spl163_10
<=> k6_lattices(sK18) = k5_lattices(k1_lattice2(sK18)) ),
introduced(definition,[new_symbols(definition,[spl163_10])],[avatar_definition]) ).
fof(f39744,plain,
( k6_lattices(sK18) = k5_lattices(k1_lattice2(sK18))
| ~ spl163_10 ),
inference(avatar_component_clause,[],[f39742]) ).
fof(f39745,plain,
( spl163_10
| spl163_2
| ~ spl163_3
| ~ spl163_4
| ~ spl163_5 ),
inference(avatar_split_clause,[],[f38069,f36630,f36579,f36574,f36569,f39742]) ).
fof(f39772,plain,
( ! [X0] :
( ~ r2_hidden(k6_lattices(sK18),X0)
| u1_struct_0(k1_lattice2(sK18)) = X0
| v3_struct_0(k1_lattice2(sK18))
| ~ v10_lattices(k1_lattice2(sK18))
| ~ v13_lattices(k1_lattice2(sK18))
| ~ l3_lattices(k1_lattice2(sK18))
| ~ m1_filter_0(X0,k1_lattice2(sK18)) )
| ~ spl163_10 ),
inference(superposition,[],[f36539,f39744]) ).
fof(f39779,plain,
( ! [X0] :
( ~ r2_hidden(k6_lattices(sK18),X0)
| u1_struct_0(k1_lattice2(sK18)) = X0
| ~ v10_lattices(k1_lattice2(sK18))
| ~ v13_lattices(k1_lattice2(sK18))
| ~ l3_lattices(k1_lattice2(sK18))
| ~ m1_filter_0(X0,k1_lattice2(sK18)) )
| spl163_2
| ~ spl163_3
| ~ spl163_10 ),
inference(forward_subsumption_resolution,[],[f39772,f37377]) ).
fof(f39809,plain,
( ! [X0] :
( ~ r2_hidden(k6_lattices(sK18),X0)
| u1_struct_0(k1_lattice2(sK18)) = X0
| ~ v13_lattices(k1_lattice2(sK18))
| ~ l3_lattices(k1_lattice2(sK18))
| ~ m1_filter_0(X0,k1_lattice2(sK18)) )
| spl163_2
| ~ spl163_3
| ~ spl163_4
| ~ spl163_10 ),
inference(forward_subsumption_resolution,[],[f39779,f37807]) ).
fof(f39839,plain,
( ! [X0] :
( ~ r2_hidden(k6_lattices(sK18),X0)
| u1_struct_0(k1_lattice2(sK18)) = X0
| ~ l3_lattices(k1_lattice2(sK18))
| ~ m1_filter_0(X0,k1_lattice2(sK18)) )
| spl163_2
| ~ spl163_3
| ~ spl163_4
| ~ spl163_5
| ~ spl163_10 ),
inference(forward_subsumption_resolution,[],[f39809,f38071]) ).
fof(f39867,plain,
( ! [X0] :
( ~ r2_hidden(k6_lattices(sK18),X0)
| u1_struct_0(k1_lattice2(sK18)) = X0
| ~ m1_filter_0(X0,k1_lattice2(sK18)) )
| spl163_2
| ~ spl163_3
| ~ spl163_4
| ~ spl163_5
| ~ spl163_10 ),
inference(forward_subsumption_resolution,[],[f39839,f38946]) ).
fof(f39893,plain,
( ! [X0] :
( u1_struct_0(sK18) = X0
| ~ r2_hidden(k6_lattices(sK18),X0)
| ~ m1_filter_0(X0,k1_lattice2(sK18)) )
| spl163_2
| ~ spl163_3
| ~ spl163_4
| ~ spl163_5
| ~ spl163_10 ),
inference(forward_demodulation,[],[f39867,f37385]) ).
fof(f39930,definition,
( spl163_11
<=> ! [X0] :
( u1_struct_0(sK18) = X0
| ~ r2_hidden(k6_lattices(sK18),X0)
| ~ m1_filter_0(X0,k1_lattice2(sK18)) ) ),
introduced(definition,[new_symbols(definition,[spl163_11])],[avatar_definition]) ).
fof(f39931,plain,
( ! [X0] :
( ~ m1_filter_0(X0,k1_lattice2(sK18))
| ~ r2_hidden(k6_lattices(sK18),X0)
| u1_struct_0(sK18) = X0 )
| ~ spl163_11 ),
inference(avatar_component_clause,[],[f39930]) ).
fof(f39932,plain,
( spl163_11
| spl163_2
| ~ spl163_3
| ~ spl163_4
| ~ spl163_5
| ~ spl163_10 ),
inference(avatar_split_clause,[],[f39893,f39742,f36630,f36579,f36574,f36569,f39930]) ).
fof(f39933,plain,
( ! [X0] :
( ~ r2_hidden(k6_lattices(sK18),X0)
| u1_struct_0(sK18) = X0
| ~ m1_filter_2(X0,k1_lattice2(sK18))
| v3_struct_0(k1_lattice2(sK18))
| ~ v10_lattices(k1_lattice2(sK18))
| ~ l3_lattices(k1_lattice2(sK18)) )
| ~ spl163_11 ),
inference(resolution,[],[f39931,f35593]) ).
fof(f40013,plain,
( ! [X0] :
( ~ r2_hidden(k6_lattices(sK18),X0)
| u1_struct_0(sK18) = X0
| ~ m1_filter_2(X0,k1_lattice2(sK18))
| ~ v10_lattices(k1_lattice2(sK18))
| ~ l3_lattices(k1_lattice2(sK18)) )
| spl163_2
| ~ spl163_3
| ~ spl163_11 ),
inference(forward_subsumption_resolution,[],[f39933,f37377]) ).
fof(f40053,plain,
( ! [X0] :
( ~ r2_hidden(k6_lattices(sK18),X0)
| u1_struct_0(sK18) = X0
| ~ m1_filter_2(X0,k1_lattice2(sK18))
| ~ l3_lattices(k1_lattice2(sK18)) )
| spl163_2
| ~ spl163_3
| ~ spl163_4
| ~ spl163_11 ),
inference(forward_subsumption_resolution,[],[f40013,f37807]) ).
fof(f40091,plain,
( ! [X0] :
( ~ r2_hidden(k6_lattices(sK18),X0)
| u1_struct_0(sK18) = X0
| ~ m1_filter_2(X0,k1_lattice2(sK18)) )
| spl163_2
| ~ spl163_3
| ~ spl163_4
| ~ spl163_11 ),
inference(forward_subsumption_resolution,[],[f40053,f38946]) ).
fof(f40375,definition,
( spl163_13
<=> m1_filter_0(u1_struct_0(sK18),sK18) ),
introduced(definition,[new_symbols(definition,[spl163_13])],[avatar_definition]) ).
fof(f40377,plain,
( m1_filter_0(u1_struct_0(sK18),sK18)
| ~ spl163_13 ),
inference(avatar_component_clause,[],[f40375]) ).
fof(f40378,plain,
( spl163_13
| spl163_2
| ~ spl163_3
| ~ spl163_4 ),
inference(avatar_split_clause,[],[f37891,f36579,f36574,f36569,f40375]) ).
fof(f40389,plain,
( m1_subset_1(u1_struct_0(sK18),k1_zfmisc_1(u1_struct_0(sK18)))
| v3_struct_0(sK18)
| ~ v10_lattices(sK18)
| ~ l3_lattices(sK18)
| ~ spl163_13 ),
inference(resolution,[],[f40377,f35799]) ).
fof(f40390,plain,
( ~ v1_xboole_0(u1_struct_0(sK18))
| v3_struct_0(sK18)
| ~ v10_lattices(sK18)
| ~ l3_lattices(sK18)
| ~ spl163_13 ),
inference(resolution,[],[f40377,f35800]) ).
fof(f40413,plain,
( r2_hidden(k6_lattices(sK18),u1_struct_0(sK18))
| v3_struct_0(sK18)
| ~ v10_lattices(sK18)
| ~ v14_lattices(sK18)
| ~ l3_lattices(sK18)
| ~ spl163_13 ),
inference(resolution,[],[f40377,f36550]) ).
fof(f40415,plain,
( r2_hidden(k6_lattices(sK18),u1_struct_0(sK18))
| ~ v10_lattices(sK18)
| ~ v14_lattices(sK18)
| ~ l3_lattices(sK18)
| spl163_2
| ~ spl163_13 ),
inference(forward_subsumption_resolution,[],[f40413,f36571]) ).
fof(f40433,plain,
( ~ v1_xboole_0(u1_struct_0(sK18))
| ~ v10_lattices(sK18)
| ~ l3_lattices(sK18)
| spl163_2
| ~ spl163_13 ),
inference(forward_subsumption_resolution,[],[f40390,f36571]) ).
fof(f40434,plain,
( m1_subset_1(u1_struct_0(sK18),k1_zfmisc_1(u1_struct_0(sK18)))
| ~ v10_lattices(sK18)
| ~ l3_lattices(sK18)
| spl163_2
| ~ spl163_13 ),
inference(forward_subsumption_resolution,[],[f40389,f36571]) ).
fof(f40444,plain,
( r2_hidden(k6_lattices(sK18),u1_struct_0(sK18))
| ~ v14_lattices(sK18)
| ~ l3_lattices(sK18)
| spl163_2
| ~ spl163_4
| ~ spl163_13 ),
inference(forward_subsumption_resolution,[],[f40415,f36581]) ).
fof(f40462,plain,
( ~ v1_xboole_0(u1_struct_0(sK18))
| ~ l3_lattices(sK18)
| spl163_2
| ~ spl163_4
| ~ spl163_13 ),
inference(forward_subsumption_resolution,[],[f40433,f36581]) ).
fof(f40463,plain,
( m1_subset_1(u1_struct_0(sK18),k1_zfmisc_1(u1_struct_0(sK18)))
| ~ l3_lattices(sK18)
| spl163_2
| ~ spl163_4
| ~ spl163_13 ),
inference(forward_subsumption_resolution,[],[f40434,f36581]) ).
fof(f40473,plain,
( r2_hidden(k6_lattices(sK18),u1_struct_0(sK18))
| ~ l3_lattices(sK18)
| spl163_2
| ~ spl163_4
| ~ spl163_5
| ~ spl163_13 ),
inference(forward_subsumption_resolution,[],[f40444,f36632]) ).
fof(f40491,plain,
( ~ v1_xboole_0(u1_struct_0(sK18))
| spl163_2
| ~ spl163_3
| ~ spl163_4
| ~ spl163_13 ),
inference(forward_subsumption_resolution,[],[f40462,f36576]) ).
fof(f40492,plain,
( m1_subset_1(u1_struct_0(sK18),k1_zfmisc_1(u1_struct_0(sK18)))
| spl163_2
| ~ spl163_3
| ~ spl163_4
| ~ spl163_13 ),
inference(forward_subsumption_resolution,[],[f40463,f36576]) ).
fof(f40502,plain,
( r2_hidden(k6_lattices(sK18),u1_struct_0(sK18))
| spl163_2
| ~ spl163_3
| ~ spl163_4
| ~ spl163_5
| ~ spl163_13 ),
inference(forward_subsumption_resolution,[],[f40473,f36576]) ).
fof(f44635,definition,
( spl163_29
<=> r2_hidden(k6_lattices(sK18),u1_struct_0(sK18)) ),
introduced(definition,[new_symbols(definition,[spl163_29])],[avatar_definition]) ).
fof(f44637,plain,
( r2_hidden(k6_lattices(sK18),u1_struct_0(sK18))
| ~ spl163_29 ),
inference(avatar_component_clause,[],[f44635]) ).
fof(f44638,plain,
( spl163_29
| spl163_2
| ~ spl163_3
| ~ spl163_4
| ~ spl163_5
| ~ spl163_13 ),
inference(avatar_split_clause,[],[f40502,f40375,f36630,f36579,f36574,f36569,f44635]) ).
fof(f44651,plain,
( m1_subset_1(k6_lattices(sK18),u1_struct_0(sK18))
| ~ spl163_29 ),
inference(resolution,[],[f44637,f35765]) ).
fof(f45974,definition,
( spl163_40
<=> m1_subset_1(k6_lattices(sK18),u1_struct_0(sK18)) ),
introduced(definition,[new_symbols(definition,[spl163_40])],[avatar_definition]) ).
fof(f45976,plain,
( m1_subset_1(k6_lattices(sK18),u1_struct_0(sK18))
| ~ spl163_40 ),
inference(avatar_component_clause,[],[f45974]) ).
fof(f45977,plain,
( spl163_40
| ~ spl163_29 ),
inference(avatar_split_clause,[],[f44651,f44635,f45974]) ).
fof(f51717,plain,
( m2_filter_2(k18_filter_2(sK18,k6_lattices(sK18)),sK18)
| v3_struct_0(sK18)
| ~ v10_lattices(sK18)
| ~ l3_lattices(sK18)
| ~ spl163_40 ),
inference(resolution,[],[f45976,f35633]) ).
fof(f52035,plain,
( sP152(sK18)
| ~ spl163_40 ),
inference(resolution,[],[f45976,f36515]) ).
fof(f52036,plain,
( r2_hidden(k6_lattices(sK18),k18_filter_2(sK18,k6_lattices(sK18)))
| v3_struct_0(sK18)
| ~ v10_lattices(sK18)
| ~ l3_lattices(sK18)
| ~ sP152(sK18)
| ~ spl163_40 ),
inference(resolution,[],[f45976,f36516]) ).
fof(f52270,plain,
( r2_hidden(k6_lattices(sK18),k18_filter_2(sK18,k6_lattices(sK18)))
| ~ v10_lattices(sK18)
| ~ l3_lattices(sK18)
| ~ sP152(sK18)
| spl163_2
| ~ spl163_40 ),
inference(forward_subsumption_resolution,[],[f52036,f36571]) ).
fof(f52522,plain,
( m2_filter_2(k18_filter_2(sK18,k6_lattices(sK18)),sK18)
| ~ v10_lattices(sK18)
| ~ l3_lattices(sK18)
| spl163_2
| ~ spl163_40 ),
inference(forward_subsumption_resolution,[],[f51717,f36571]) ).
fof(f52554,plain,
( r2_hidden(k6_lattices(sK18),k18_filter_2(sK18,k6_lattices(sK18)))
| ~ l3_lattices(sK18)
| ~ sP152(sK18)
| spl163_2
| ~ spl163_4
| ~ spl163_40 ),
inference(forward_subsumption_resolution,[],[f52270,f36581]) ).
fof(f52803,plain,
( m2_filter_2(k18_filter_2(sK18,k6_lattices(sK18)),sK18)
| ~ l3_lattices(sK18)
| spl163_2
| ~ spl163_4
| ~ spl163_40 ),
inference(forward_subsumption_resolution,[],[f52522,f36581]) ).
fof(f52833,plain,
( r2_hidden(k6_lattices(sK18),k18_filter_2(sK18,k6_lattices(sK18)))
| ~ sP152(sK18)
| spl163_2
| ~ spl163_3
| ~ spl163_4
| ~ spl163_40 ),
inference(forward_subsumption_resolution,[],[f52554,f36576]) ).
fof(f53035,plain,
( m2_filter_2(k18_filter_2(sK18,k6_lattices(sK18)),sK18)
| spl163_2
| ~ spl163_3
| ~ spl163_4
| ~ spl163_40 ),
inference(forward_subsumption_resolution,[],[f52803,f36576]) ).
fof(f53047,plain,
( r2_hidden(k6_lattices(sK18),k18_filter_2(sK18,k6_lattices(sK18)))
| spl163_2
| ~ spl163_3
| ~ spl163_4
| ~ spl163_40 ),
inference(forward_subsumption_resolution,[],[f52833,f52035]) ).
fof(f53119,definition,
( spl163_61
<=> r2_hidden(k6_lattices(sK18),k18_filter_2(sK18,k6_lattices(sK18))) ),
introduced(definition,[new_symbols(definition,[spl163_61])],[avatar_definition]) ).
fof(f53121,plain,
( r2_hidden(k6_lattices(sK18),k18_filter_2(sK18,k6_lattices(sK18)))
| ~ spl163_61 ),
inference(avatar_component_clause,[],[f53119]) ).
fof(f53122,plain,
( spl163_61
| spl163_2
| ~ spl163_3
| ~ spl163_4
| ~ spl163_40 ),
inference(avatar_split_clause,[],[f53047,f45974,f36579,f36574,f36569,f53119]) ).
fof(f54234,definition,
( spl163_63
<=> m2_filter_2(k18_filter_2(sK18,k6_lattices(sK18)),sK18) ),
introduced(definition,[new_symbols(definition,[spl163_63])],[avatar_definition]) ).
fof(f54236,plain,
( m2_filter_2(k18_filter_2(sK18,k6_lattices(sK18)),sK18)
| ~ spl163_63 ),
inference(avatar_component_clause,[],[f54234]) ).
fof(f54237,plain,
( spl163_63
| spl163_2
| ~ spl163_3
| ~ spl163_4
| ~ spl163_40 ),
inference(avatar_split_clause,[],[f53035,f45974,f36579,f36574,f36569,f54234]) ).
fof(f56224,definition,
( spl163_70
<=> v1_xboole_0(u1_struct_0(sK18)) ),
introduced(definition,[new_symbols(definition,[spl163_70])],[avatar_definition]) ).
fof(f56226,plain,
( ~ v1_xboole_0(u1_struct_0(sK18))
| spl163_70 ),
inference(avatar_component_clause,[],[f56224]) ).
fof(f56227,plain,
( ~ spl163_70
| spl163_2
| ~ spl163_3
| ~ spl163_4
| ~ spl163_13 ),
inference(avatar_split_clause,[],[f40491,f40375,f36579,f36574,f36569,f56224]) ).
fof(f60159,definition,
( spl163_86
<=> ! [X0] :
( m1_filter_2(X0,k1_lattice2(sK18))
| ~ m2_filter_2(X0,sK18) ) ),
introduced(definition,[new_symbols(definition,[spl163_86])],[avatar_definition]) ).
fof(f60160,plain,
( ! [X0] :
( m1_filter_2(X0,k1_lattice2(sK18))
| ~ m2_filter_2(X0,sK18) )
| ~ spl163_86 ),
inference(avatar_component_clause,[],[f60159]) ).
fof(f60161,plain,
( spl163_86
| spl163_2
| ~ spl163_3
| ~ spl163_4 ),
inference(avatar_split_clause,[],[f37957,f36579,f36574,f36569,f60159]) ).
fof(f67117,definition,
( spl163_113
<=> m1_subset_1(u1_struct_0(sK18),k1_zfmisc_1(u1_struct_0(sK18))) ),
introduced(definition,[new_symbols(definition,[spl163_113])],[avatar_definition]) ).
fof(f67119,plain,
( m1_subset_1(u1_struct_0(sK18),k1_zfmisc_1(u1_struct_0(sK18)))
| ~ spl163_113 ),
inference(avatar_component_clause,[],[f67117]) ).
fof(f67120,plain,
( spl163_113
| spl163_2
| ~ spl163_3
| ~ spl163_4
| ~ spl163_13 ),
inference(avatar_split_clause,[],[f40492,f40375,f36579,f36574,f36569,f67117]) ).
fof(f67289,plain,
( r1_filter_2(u1_struct_0(sK18),u1_struct_0(sK18),u1_struct_0(sK18))
| v1_xboole_0(u1_struct_0(sK18))
| ~ spl163_113 ),
inference(resolution,[],[f67119,f36537]) ).
fof(f67486,plain,
( r1_filter_2(u1_struct_0(sK18),u1_struct_0(sK18),u1_struct_0(sK18))
| spl163_70
| ~ spl163_113 ),
inference(forward_subsumption_resolution,[],[f67289,f56226]) ).
fof(f67716,definition,
( spl163_114
<=> r1_filter_2(u1_struct_0(sK18),u1_struct_0(sK18),u1_struct_0(sK18)) ),
introduced(definition,[new_symbols(definition,[spl163_114])],[avatar_definition]) ).
fof(f67718,plain,
( r1_filter_2(u1_struct_0(sK18),u1_struct_0(sK18),u1_struct_0(sK18))
| ~ spl163_114 ),
inference(avatar_component_clause,[],[f67716]) ).
fof(f67719,plain,
( spl163_114
| spl163_70
| ~ spl163_113 ),
inference(avatar_split_clause,[],[f67486,f67117,f56224,f67716]) ).
fof(f78341,definition,
( spl163_152
<=> ! [X0] :
( ~ r2_hidden(k6_lattices(sK18),X0)
| u1_struct_0(sK18) = X0
| ~ m1_filter_2(X0,k1_lattice2(sK18)) ) ),
introduced(definition,[new_symbols(definition,[spl163_152])],[avatar_definition]) ).
fof(f78342,plain,
( ! [X0] :
( ~ m1_filter_2(X0,k1_lattice2(sK18))
| u1_struct_0(sK18) = X0
| ~ r2_hidden(k6_lattices(sK18),X0) )
| ~ spl163_152 ),
inference(avatar_component_clause,[],[f78341]) ).
fof(f78343,plain,
( spl163_152
| spl163_2
| ~ spl163_3
| ~ spl163_4
| ~ spl163_11 ),
inference(avatar_split_clause,[],[f40091,f39930,f36579,f36574,f36569,f78341]) ).
fof(f78344,plain,
( ! [X0] :
( u1_struct_0(sK18) = X0
| ~ r2_hidden(k6_lattices(sK18),X0)
| ~ m2_filter_2(X0,sK18) )
| ~ spl163_86
| ~ spl163_152 ),
inference(resolution,[],[f78342,f60160]) ).
fof(f78394,definition,
( spl163_153
<=> ! [X0] :
( u1_struct_0(sK18) = X0
| ~ r2_hidden(k6_lattices(sK18),X0)
| ~ m2_filter_2(X0,sK18) ) ),
introduced(definition,[new_symbols(definition,[spl163_153])],[avatar_definition]) ).
fof(f78395,plain,
( ! [X0] :
( ~ r2_hidden(k6_lattices(sK18),X0)
| u1_struct_0(sK18) = X0
| ~ m2_filter_2(X0,sK18) )
| ~ spl163_153 ),
inference(avatar_component_clause,[],[f78394]) ).
fof(f78396,plain,
( spl163_153
| ~ spl163_86
| ~ spl163_152 ),
inference(avatar_split_clause,[],[f78344,f78341,f60159,f78394]) ).
fof(f78401,plain,
( u1_struct_0(sK18) = k18_filter_2(sK18,k6_lattices(sK18))
| ~ m2_filter_2(k18_filter_2(sK18,k6_lattices(sK18)),sK18)
| ~ spl163_61
| ~ spl163_153 ),
inference(resolution,[],[f78395,f53121]) ).
fof(f78465,plain,
( u1_struct_0(sK18) = k18_filter_2(sK18,k6_lattices(sK18))
| ~ spl163_61
| ~ spl163_63
| ~ spl163_153 ),
inference(forward_subsumption_resolution,[],[f78401,f54236]) ).
fof(f78501,definition,
( spl163_154
<=> u1_struct_0(sK18) = k18_filter_2(sK18,k6_lattices(sK18)) ),
introduced(definition,[new_symbols(definition,[spl163_154])],[avatar_definition]) ).
fof(f78503,plain,
( u1_struct_0(sK18) = k18_filter_2(sK18,k6_lattices(sK18))
| ~ spl163_154 ),
inference(avatar_component_clause,[],[f78501]) ).
fof(f78504,plain,
( spl163_154
| ~ spl163_61
| ~ spl163_63
| ~ spl163_153 ),
inference(avatar_split_clause,[],[f78465,f78394,f54234,f53119,f78501]) ).
fof(f78513,plain,
( ~ r1_filter_2(u1_struct_0(sK18),k17_filter_2(sK18),u1_struct_0(sK18))
| spl163_1
| ~ spl163_154 ),
inference(superposition,[],[f36566,f78503]) ).
fof(f78549,plain,
( ~ r1_filter_2(u1_struct_0(sK18),u1_struct_0(sK18),u1_struct_0(sK18))
| spl163_1
| ~ spl163_9
| ~ spl163_154 ),
inference(forward_demodulation,[],[f78513,f39737]) ).
fof(f78558,plain,
( $false
| spl163_1
| ~ spl163_9
| ~ spl163_114
| ~ spl163_154 ),
inference(forward_subsumption_resolution,[],[f78549,f67718]) ).
fof(f78559,plain,
( spl163_1
| ~ spl163_9
| ~ spl163_114
| ~ spl163_154 ),
inference(avatar_contradiction_clause,[],[f78558]) ).
cnf(s1,plain,
~ spl163_1,
inference(sat_conversion,[],[f36567]) ).
cnf(s2,plain,
~ spl163_2,
inference(sat_conversion,[],[f36572]) ).
cnf(s3,plain,
spl163_3,
inference(sat_conversion,[],[f36577]) ).
cnf(s4,plain,
spl163_4,
inference(sat_conversion,[],[f36582]) ).
cnf(s5,plain,
spl163_5,
inference(sat_conversion,[],[f36633]) ).
cnf(s9,plain,
( spl163_2
| ~ spl163_3
| ~ spl163_4
| spl163_9 ),
inference(sat_conversion,[],[f39738]) ).
cnf(s10,plain,
( spl163_2
| ~ spl163_3
| ~ spl163_4
| ~ spl163_5
| spl163_10 ),
inference(sat_conversion,[],[f39745]) ).
cnf(s11,plain,
( spl163_2
| ~ spl163_3
| ~ spl163_4
| ~ spl163_5
| ~ spl163_10
| spl163_11 ),
inference(sat_conversion,[],[f39932]) ).
cnf(s13,plain,
( spl163_2
| ~ spl163_3
| ~ spl163_4
| spl163_13 ),
inference(sat_conversion,[],[f40378]) ).
cnf(s28,plain,
( spl163_2
| ~ spl163_3
| ~ spl163_4
| ~ spl163_5
| ~ spl163_13
| spl163_29 ),
inference(sat_conversion,[],[f44638]) ).
cnf(s39,plain,
( ~ spl163_29
| spl163_40 ),
inference(sat_conversion,[],[f45977]) ).
cnf(s60,plain,
( spl163_2
| ~ spl163_3
| ~ spl163_4
| ~ spl163_40
| spl163_61 ),
inference(sat_conversion,[],[f53122]) ).
cnf(s62,plain,
( spl163_2
| ~ spl163_3
| ~ spl163_4
| ~ spl163_40
| spl163_63 ),
inference(sat_conversion,[],[f54237]) ).
cnf(s69,plain,
( spl163_2
| ~ spl163_3
| ~ spl163_4
| ~ spl163_13
| ~ spl163_70 ),
inference(sat_conversion,[],[f56227]) ).
cnf(s88,plain,
( spl163_2
| ~ spl163_3
| ~ spl163_4
| spl163_86 ),
inference(sat_conversion,[],[f60161]) ).
cnf(s119,plain,
( spl163_2
| ~ spl163_3
| ~ spl163_4
| ~ spl163_13
| spl163_113 ),
inference(sat_conversion,[],[f67120]) ).
cnf(s120,plain,
( spl163_70
| ~ spl163_113
| spl163_114 ),
inference(sat_conversion,[],[f67719]) ).
cnf(s245,plain,
( spl163_2
| ~ spl163_3
| ~ spl163_4
| ~ spl163_11
| spl163_152 ),
inference(sat_conversion,[],[f78343]) ).
cnf(s246,plain,
( ~ spl163_86
| ~ spl163_152
| spl163_153 ),
inference(sat_conversion,[],[f78396]) ).
cnf(s247,plain,
( ~ spl163_61
| ~ spl163_63
| ~ spl163_153
| spl163_154 ),
inference(sat_conversion,[],[f78504]) ).
cnf(s250,plain,
( spl163_1
| ~ spl163_9
| ~ spl163_114
| ~ spl163_154 ),
inference(sat_conversion,[],[f78559]) ).
cnf(s271,plain,
spl163_86,
inference(rat,[],[s88,s3,s4,s2]) ).
cnf(s315,plain,
spl163_13,
inference(rat,[],[s13,s3,s4,s2]) ).
cnf(s317,plain,
spl163_10,
inference(rat,[],[s10,s3,s5,s4,s2]) ).
cnf(s318,plain,
spl163_9,
inference(rat,[],[s9,s3,s4,s2]) ).
cnf(s341,plain,
spl163_113,
inference(rat,[],[s119,s2,s3,s4,s315]) ).
cnf(s343,plain,
~ spl163_70,
inference(rat,[],[s69,s2,s3,s4,s315]) ).
cnf(s346,plain,
spl163_29,
inference(rat,[],[s28,s2,s3,s5,s4,s315]) ).
cnf(s350,plain,
spl163_11,
inference(rat,[],[s11,s2,s3,s5,s4,s317]) ).
cnf(s355,plain,
spl163_114,
inference(rat,[],[s120,s341,s343]) ).
cnf(s356,plain,
spl163_40,
inference(rat,[],[s39,s346]) ).
cnf(s360,plain,
spl163_152,
inference(rat,[],[s245,s2,s3,s4,s350]) ).
cnf(s364,plain,
spl163_63,
inference(rat,[],[s62,s2,s3,s4,s356]) ).
cnf(s365,plain,
spl163_61,
inference(rat,[],[s60,s2,s3,s4,s356]) ).
cnf(s368,plain,
spl163_153,
inference(rat,[],[s246,s271,s360]) ).
cnf(s371,plain,
spl163_154,
inference(rat,[],[s247,s364,s368,s365]) ).
cnf(s376,plain,
spl163_1,
inference(rat,[],[s250,s355,s318,s371]) ).
cnf(s379,plain,
$false,
inference(rat,[],[s1,s376]) ).
fof(f78580,plain,
$false,
inference(avatar_sat_refutation,[],[s379]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT306+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.38 % Computer : n020.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % 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:26:59 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.42 Running first-order theorem proving
% 0.12/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 17.86/5.20 % (3429488)Detected formulas, will run a generic FOF schedule.
% 17.86/5.20 % (3429495)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=2663551688:i=141695:sd=1:nm=32:gsp=on:ss=included_2978 on theBenchmark for (2978ds/141695Mi)
% 17.86/5.20 % (3429494)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=1526452339:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2978 on theBenchmark for (2978ds/134677Mi)
% 17.86/5.20 % (3429493)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=1453417541:i=141193_2978 on theBenchmark for (2978ds/141193Mi)
% 17.86/5.20 % (3429497)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=84604955:i=119:av=off:ss=axioms_2978 on theBenchmark for (2978ds/119Mi)
% 17.86/5.20 % (3429498)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3539116245:s2a=on:i=139:gtg=position_2978 on theBenchmark for (2978ds/139Mi)
% 17.86/5.20 % (3429499)dis-21_1_sil=8000:lcm=predicate:random_seed=4042937224:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2978 on theBenchmark for (2978ds/129Mi)
% 17.86/5.20 % (3429496)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1994204158:i=109:sd=1:ins=1:gsp=on:ss=axioms_2978 on theBenchmark for (2978ds/109Mi)
% 17.86/5.20 % (3429498)Instruction limit reached!
% 17.86/5.20 % (3429498)------------------------------
% 17.86/5.20 % (3429498)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.86/5.20 % (3429498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.86/5.20 % (3429498)CaDiCaL version: 2.1.3
% 17.86/5.20 % (3429498)Termination reason: Instruction limit
% 17.86/5.20 % (3429498)Termination phase: Property scanning
% 17.86/5.20 % (3429498)Time elapsed: 0.061 s
% 17.86/5.20 % (3429498)Peak memory usage: 136 MB
% 17.86/5.20 % (3429498)Instructions burned: 141 (million)
% 17.86/5.20 % (3429496)Instruction limit reached!
% 17.86/5.20 % (3429496)------------------------------
% 17.86/5.20 % (3429496)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.86/5.21 % (3429496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.86/5.21 % (3429496)CaDiCaL version: 2.1.3
% 17.86/5.21 % (3429496)Termination reason: Instruction limit
% 17.86/5.21 % (3429496)Termination phase: SInE selection
% 17.86/5.21 % (3429496)Time elapsed: 0.077 s
% 17.86/5.21 % (3429496)Peak memory usage: 136 MB
% 17.86/5.21 % (3429496)Instructions burned: 109 (million)
% 17.86/5.21 % (3429497)Instruction limit reached!
% 17.86/5.21 % (3429497)------------------------------
% 17.86/5.21 % (3429497)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.86/5.21 % (3429497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.86/5.21 % (3429497)CaDiCaL version: 2.1.3
% 17.86/5.21 % (3429497)Termination reason: Instruction limit
% 17.86/5.21 % (3429497)Termination phase: SInE selection
% 17.86/5.21 % (3429497)Time elapsed: 0.084 s
% 17.86/5.21 % (3429497)Peak memory usage: 136 MB
% 17.86/5.21 % (3429497)Instructions burned: 120 (million)
% 17.86/5.21 % (3429499)Instruction limit reached!
% 17.86/5.21 % (3429499)------------------------------
% 17.86/5.21 % (3429499)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.86/5.21 % (3429499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.86/5.21 % (3429499)CaDiCaL version: 2.1.3
% 17.86/5.21 % (3429499)Termination reason: Instruction limit
% 17.86/5.21 % (3429499)Termination phase: SInE selection
% 17.86/5.21 % (3429499)Time elapsed: 0.087 s
% 17.86/5.21 % (3429499)Peak memory usage: 136 MB
% 17.86/5.21 % (3429499)Instructions burned: 130 (million)
% 17.86/5.21 % (3429507)lrs+10_1_sil=8000:sp=occurrence:random_seed=3740978182:i=285:sd=3:ss=axioms:sgt=8_2976 on theBenchmark for (2976ds/285Mi)
% 17.86/5.21 % (3429509)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3730418989:i=325:sd=1:ss=axioms:sgt=32_2975 on theBenchmark for (2975ds/325Mi)
% 17.86/5.21 % (3429508)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2154931918:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2975 on theBenchmark for (2975ds/157Mi)
% 17.86/5.21 % (3429510)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=3077511573:s2a=on:i=248:s2at=1.23:gtg=position_2975 on theBenchmark for (2975ds/248Mi)
% 17.86/5.21 % (3429508)Instruction limit reached!
% 25.47/6.31 % (3429508)------------------------------
% 25.47/6.31 % (3429508)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.47/6.31 % (3429508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.47/6.31 % (3429508)CaDiCaL version: 2.1.3
% 25.47/6.31 % (3429508)Termination reason: Instruction limit
% 25.47/6.31 % (3429508)Termination phase: Property scanning
% 25.47/6.31 % (3429508)Time elapsed: 0.070 s
% 25.47/6.31 % (3429508)Peak memory usage: 136 MB
% 25.47/6.31 % (3429508)Instructions burned: 158 (million)
% 25.47/6.31 % (3429510)Instruction limit reached!
% 25.47/6.31 % (3429510)------------------------------
% 25.47/6.31 % (3429510)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.47/6.31 % (3429510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.47/6.31 % (3429510)CaDiCaL version: 2.1.3
% 25.47/6.31 % (3429510)Termination reason: Instruction limit
% 25.47/6.31 % (3429510)Termination phase: Property scanning
% 25.47/6.31 % (3429510)Time elapsed: 0.108 s
% 25.47/6.31 % (3429510)Peak memory usage: 136 MB
% 25.47/6.31 % (3429510)Instructions burned: 250 (million)
% 25.47/6.31 % (3429509)Refutation not found, incomplete strategy
% 25.47/6.31 % (3429509)------------------------------
% 25.47/6.31 % (3429509)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.47/6.31 % (3429509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.47/6.31 % (3429509)CaDiCaL version: 2.1.3
% 25.47/6.31 % (3429509)Termination reason: Refutation not found, incomplete strategy
% 25.47/6.31 % (3429509)Time elapsed: 0.189 s
% 25.47/6.31 % (3429509)Peak memory usage: 142 MB
% 25.47/6.31 % (3429509)Instructions burned: 242 (million)
% 25.47/6.31 % (3429507)Instruction limit reached!
% 25.47/6.31 % (3429507)------------------------------
% 25.47/6.31 % (3429507)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.47/6.31 % (3429507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.47/6.31 % (3429507)CaDiCaL version: 2.1.3
% 25.47/6.31 % (3429507)Termination reason: Instruction limit
% 25.47/6.31 % (3429507)Termination phase: Saturation
% 25.47/6.31 % (3429507)Time elapsed: 0.220 s
% 25.47/6.31 % (3429507)Peak memory usage: 141 MB
% 25.47/6.31 % (3429507)Instructions burned: 285 (million)
% 25.47/6.31 % (3429515)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2914833462:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2973 on theBenchmark for (2973ds/294Mi)
% 25.47/6.31 % (3429516)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=803603346:i=2350_2973 on theBenchmark for (2973ds/2350Mi)
% 25.47/6.31 % (3429518)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=302941509:cts=off:i=113:fsr=off:ss=included:sgt=4_2972 on theBenchmark for (2972ds/113Mi)
% 25.47/6.31 % (3429515)Instruction limit reached!
% 25.47/6.31 % (3429515)------------------------------
% 25.47/6.31 % (3429515)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.47/6.31 % (3429515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.47/6.31 % (3429515)CaDiCaL version: 2.1.3
% 25.47/6.31 % (3429515)Termination reason: Instruction limit
% 25.47/6.31 % (3429515)Termination phase: SInE selection
% 25.47/6.31 % (3429515)Time elapsed: 0.182 s
% 25.47/6.31 % (3429515)Peak memory usage: 137 MB
% 25.47/6.31 % (3429515)Instructions burned: 294 (million)
% 25.47/6.31 % (3429518)Instruction limit reached!
% 25.47/6.31 % (3429518)------------------------------
% 25.47/6.31 % (3429518)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.47/6.31 % (3429518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.47/6.31 % (3429518)CaDiCaL version: 2.1.3
% 25.47/6.31 % (3429518)Termination reason: Instruction limit
% 25.47/6.31 % (3429518)Termination phase: SInE selection
% 25.47/6.31 % (3429518)Time elapsed: 0.086 s
% 25.47/6.31 % (3429518)Peak memory usage: 136 MB
% 25.47/6.31 % (3429518)Instructions burned: 114 (million)
% 25.47/6.31 % (3429509)------------------------------
% 25.47/6.31 % (3429509)------------------------------
% 25.47/6.31 % (3429521)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=360698001:i=127:av=off:fsr=off:sup=off_2970 on theBenchmark for (2970ds/127Mi)
% 25.47/6.31 % (3429522)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2988281634:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2970 on theBenchmark for (2970ds/114Mi)
% 25.47/6.31 % (3429523)lrs+10_1_sil=8000:sp=occurrence:random_seed=2660374543:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2969 on theBenchmark for (2969ds/907Mi)
% 15.09/6.54 % (3429521)Instruction limit reached!
% 15.09/6.54 % (3429521)------------------------------
% 15.09/6.54 % (3429521)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.09/6.54 % (3429521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.09/6.54 % (3429521)CaDiCaL version: 2.1.3
% 15.09/6.54 % (3429521)Termination reason: Instruction limit
% 15.09/6.54 % (3429521)Termination phase: Preprocessing 1
% 15.09/6.54 % (3429521)Time elapsed: 0.095 s
% 15.09/6.54 % (3429521)Peak memory usage: 137 MB
% 15.09/6.54 % (3429521)Instructions burned: 127 (million)
% 15.09/6.54 % (3429522)Instruction limit reached!
% 15.09/6.54 % (3429522)------------------------------
% 15.09/6.54 % (3429522)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.09/6.54 % (3429522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.09/6.54 % (3429522)CaDiCaL version: 2.1.3
% 15.09/6.54 % (3429522)Termination reason: Instruction limit
% 15.09/6.54 % (3429522)Termination phase: Property scanning
% 15.09/6.54 % (3429522)Time elapsed: 0.052 s
% 15.09/6.54 % (3429522)Peak memory usage: 136 MB
% 15.09/6.54 % (3429522)Instructions burned: 114 (million)
% 15.09/6.54 % (3429527)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2116430017:i=437:sd=1:aac=none:ss=included_2968 on theBenchmark for (2968ds/437Mi)
% 15.09/6.54 % (3429528)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=812865583:i=5202:ss=axioms:sgt=16_2968 on theBenchmark for (2968ds/5202Mi)
% 15.09/6.54 % (3429527)Refutation not found, incomplete strategy
% 15.09/6.54 % (3429527)------------------------------
% 15.09/6.54 % (3429527)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.09/6.54 % (3429527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.09/6.54 % (3429527)CaDiCaL version: 2.1.3
% 15.09/6.54 % (3429527)Termination reason: Refutation not found, incomplete strategy
% 15.09/6.54 % (3429527)Time elapsed: 0.231 s
% 15.09/6.54 % (3429527)Peak memory usage: 143 MB
% 15.09/6.54 % (3429527)Instructions burned: 318 (million)
% 15.09/6.54 % (3429523)Instruction limit reached!
% 15.09/6.54 % (3429523)------------------------------
% 15.09/6.54 % (3429523)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.09/6.54 % (3429523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.09/6.54 % (3429523)CaDiCaL version: 2.1.3
% 15.09/6.54 % (3429523)Termination reason: Instruction limit
% 15.09/6.54 % (3429523)Termination phase: Property scanning
% 15.09/6.54 % (3429523)Time elapsed: 0.586 s
% 15.09/6.54 % (3429523)Peak memory usage: 157 MB
% 15.09/6.54 % (3429523)Instructions burned: 908 (million)
% 15.09/6.54 % (3429527)------------------------------
% 15.09/6.54 % (3429527)------------------------------
% 15.09/6.54 % (3429531)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1929562621:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2962 on theBenchmark for (2962ds/134Mi)
% 15.09/6.54 % (3429532)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1235082289:st=8:i=592:sd=3:ep=RST:ss=axioms_2962 on theBenchmark for (2962ds/592Mi)
% 15.09/6.54 % (3429531)Instruction limit reached!
% 15.09/6.54 % (3429531)------------------------------
% 15.09/6.54 % (3429531)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.09/6.54 % (3429531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.09/6.54 % (3429531)CaDiCaL version: 2.1.3
% 15.09/6.54 % (3429531)Termination reason: Instruction limit
% 15.09/6.54 % (3429531)Termination phase: SInE selection
% 15.09/6.54 % (3429531)Time elapsed: 0.099 s
% 15.09/6.54 % (3429531)Peak memory usage: 136 MB
% 15.09/6.54 % (3429531)Instructions burned: 134 (million)
% 15.09/6.54 % (3429535)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1690286428:st=3:i=13193:sd=3:ss=axioms_2960 on theBenchmark for (2960ds/13193Mi)
% 15.09/6.54 % (3429516)Instruction limit reached!
% 15.09/6.54 % (3429516)------------------------------
% 15.09/6.54 % (3429516)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.09/6.54 % (3429516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.09/6.54 % (3429516)CaDiCaL version: 2.1.3
% 15.09/6.54 % (3429516)Termination reason: Instruction limit
% 15.09/6.54 % (3429516)Termination phase: Property scanning
% 15.09/6.54 % (3429516)Time elapsed: 1.539 s
% 15.09/6.54 % (3429516)Peak memory usage: 233 MB
% 15.09/6.54 % (3429516)Instructions burned: 2352 (million)
% 15.09/6.54 % (3429532)Instruction limit reached!
% 15.09/6.54 % (3429532)------------------------------
% 15.09/6.54 % (3429532)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.09/6.54 % (3429532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.09/6.54 % (3429532)CaDiCaL version: 2.1.3
% 15.09/6.54 % (3429532)Termination reason: Instruction limit
% 15.09/6.54 % (3429532)Termination phase: Preprocessing 2
% 15.09/6.54 % (3429532)Time elapsed: 0.462 s
% 15.09/6.54 % (3429532)Peak memory usage: 154 MB
% 15.09/6.54 % (3429532)Instructions burned: 592 (million)
% 15.09/6.54 % (3429537)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=3655937327:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2956 on theBenchmark for (2956ds/125Mi)
% 15.09/6.54 % (3429538)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2699535408:i=134:gtgl=5:slsql=off:gtg=exists_sym_2955 on theBenchmark for (2955ds/134Mi)
% 15.09/6.54 % (3429537)Instruction limit reached!
% 15.09/6.54 % (3429537)------------------------------
% 15.09/6.54 % (3429537)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.09/6.54 % (3429537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.09/6.54 % (3429537)CaDiCaL version: 2.1.3
% 15.09/6.54 % (3429537)Termination reason: Instruction limit
% 15.09/6.54 % (3429537)Termination phase: Property scanning
% 15.09/6.54 % (3429537)Time elapsed: 0.057 s
% 15.09/6.54 % (3429537)Peak memory usage: 136 MB
% 15.09/6.54 % (3429537)Instructions burned: 127 (million)
% 15.09/6.54 % (3429538)Instruction limit reached!
% 15.09/6.54 % (3429538)------------------------------
% 15.09/6.54 % (3429538)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.09/6.54 % (3429538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.09/6.54 % (3429538)CaDiCaL version: 2.1.3
% 15.09/6.54 % (3429538)Termination reason: Instruction limit
% 15.09/6.54 % (3429538)Termination phase: Property scanning
% 15.09/6.54 % (3429538)Time elapsed: 0.061 s
% 15.09/6.54 % (3429538)Peak memory usage: 136 MB
% 15.09/6.54 % (3429538)Instructions burned: 136 (million)
% 15.09/6.54 % (3429541)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3125181440:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2954 on theBenchmark for (2954ds/141Mi)
% 15.09/6.54 % (3429542)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2090123961:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2953 on theBenchmark for (2953ds/431Mi)
% 15.09/6.54 % (3429541)Instruction limit reached!
% 15.09/6.54 % (3429541)------------------------------
% 15.09/6.54 % (3429541)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.09/6.54 % (3429541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.09/6.54 % (3429541)CaDiCaL version: 2.1.3
% 15.09/6.54 % (3429541)Termination reason: Instruction limit
% 15.09/6.54 % (3429541)Termination phase: SInE selection
% 15.09/6.54 % (3429541)Time elapsed: 0.108 s
% 15.09/6.54 % (3429541)Peak memory usage: 136 MB
% 15.09/6.54 % (3429541)Instructions burned: 141 (million)
% 15.09/6.54 % (3429542)Refutation not found, incomplete strategy
% 15.09/6.54 % (3429542)------------------------------
% 15.09/6.54 % (3429542)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.09/6.54 % (3429542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.09/6.54 % (3429542)CaDiCaL version: 2.1.3
% 15.09/6.54 % (3429542)Termination reason: Refutation not found, incomplete strategy
% 15.09/6.54 % (3429542)Time elapsed: 0.203 s
% 15.09/6.54 % (3429542)Peak memory usage: 142 MB
% 15.09/6.54 % (3429542)Instructions burned: 245 (million)
% 15.09/6.54 % (3429545)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=3495780965:i=6060:aac=none:ins=25_2951 on theBenchmark for (2951ds/6060Mi)
% 15.09/6.54 % (3429542)------------------------------
% 15.09/6.54 % (3429542)------------------------------
% 15.09/6.54 % (3429547)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=2197599356:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2947 on theBenchmark for (2947ds/150Mi)
% 15.09/6.54 % (3429495)First to succeed.
% 15.09/6.54 % (3429495)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3429488"
% 15.09/6.54 % (3429547)Instruction limit reached!
% 15.09/6.54 % (3429547)------------------------------
% 15.09/6.54 % (3429547)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.09/6.54 % (3429547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.09/6.54 % (3429547)CaDiCaL version: 2.1.3
% 15.09/6.54 % (3429547)Termination reason: Instruction limit
% 15.09/6.54 % (3429547)Termination phase: SInE selection
% 15.09/6.54 % (3429547)Time elapsed: 0.122 s
% 15.09/6.54 % (3429547)Peak memory usage: 136 MB
% 15.09/6.54 % (3429547)Instructions burned: 151 (million)
% 15.09/6.54 % (3429495)Refutation found. Thanks to Tanya!
% 15.09/6.54 % SZS status Theorem for theBenchmark
% 15.09/6.54 % SZS output start Proof for theBenchmark
% See solution above
% 27.46/6.77 % (3429495)------------------------------
% 27.46/6.77 % (3429495)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.46/6.77 % (3429495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.46/6.77 % (3429495)CaDiCaL version: 2.1.3
% 27.46/6.77 % (3429495)Termination reason: Refutation
% 27.46/6.77 % (3429495)Time elapsed: 3.165 s
% 27.46/6.77 % (3429495)Peak memory usage: 246 MB
% 27.46/6.77 % (3429495)Instructions burned: 9796 (million)
% 27.46/6.77 % (3429495)------------------------------
% 27.46/6.77 % (3429495)------------------------------
% 27.46/6.77 % (3429488)Success in time 5.675 s
% 27.46/6.77 % Vampire exiting
%------------------------------------------------------------------------------