%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT306+3 : 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 : n019.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:44 AM UTC 2026
% Result : Theorem 21.46s 4.60s
% Output : Refutation 22.49s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 33
% Syntax : Number of formulae : 247 ( 40 unt; 10 def)
% Number of atoms : 932 ( 69 equ)
% Maximal formula atoms : 12 ( 3 avg)
% Number of connectives : 1137 ( 452 ~; 510 |; 115 &)
% ( 25 <=>; 35 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 32 ( 30 usr; 11 prp; 0-3 aty)
% Number of functors : 13 ( 13 usr; 1 con; 0-3 aty)
% Number of variables : 202 ( 0 sgn 200 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f675,axiom,
! [X0,X1] :
( r2_hidden(X0,X1)
=> m1_subset_1(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_subset) ).
fof(f8585,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/sandbox/benchmark/theBenchmark.p',t12_filter_0) ).
fof(f8588,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> m1_filter_0(u1_struct_0(X0),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t15_filter_0) ).
fof(f8589,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(f8608,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/sandbox/benchmark/theBenchmark.p',t32_filter_0) ).
fof(f8673,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_filter_0(X1,X0)
=> ( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m1_filter_0) ).
fof(f9358,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(f9363,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(f9391,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(f9438,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( v13_lattices(X0)
<=> v14_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t63_lattice2) ).
fof(f9439,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( v14_lattices(X0)
<=> v13_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t64_lattice2) ).
fof(f9454,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/sandbox/benchmark/theBenchmark.p',t79_lattice2) ).
fof(f9463,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(f12269,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> m2_lattice4(u1_struct_0(X0),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t10_lattice4) ).
fof(f12317,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(f13532,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(f13537,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/sandbox/benchmark/theBenchmark.p',redefinition_r1_filter_2) ).
fof(f13567,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/sandbox/benchmark/theBenchmark.p',dt_k18_filter_2) ).
fof(f13601,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(f13613,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(f13614,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> k18_filter_2(X0,X1) = a_2_0_filter_2(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d9_filter_2) ).
fof(f13617,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/sandbox/benchmark/theBenchmark.p',t31_filter_2) ).
fof(f13618,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/sandbox/benchmark/theBenchmark.p',t32_filter_2) ).
fof(f13619,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)],[f13618]) ).
fof(f13668,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,[],[f13532]) ).
fof(f13669,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,[],[f13668]) ).
fof(f13678,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,[],[f13537]) ).
fof(f13679,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,[],[f13678]) ).
fof(f13738,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,[],[f13567]) ).
fof(f13739,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,[],[f13738]) ).
fof(f13803,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,[],[f13601]) ).
fof(f13804,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,[],[f13803]) ).
fof(f13827,plain,
! [X0] :
( k17_filter_2(X0) = u1_struct_0(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f13613]) ).
fof(f13828,plain,
! [X0] :
( k17_filter_2(X0) = u1_struct_0(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13827]) ).
fof(f13829,plain,
! [X0] :
( ! [X1] :
( k18_filter_2(X0,X1) = a_2_0_filter_2(X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f13614]) ).
fof(f13830,plain,
! [X0] :
( ! [X1] :
( k18_filter_2(X0,X1) = a_2_0_filter_2(X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13829]) ).
fof(f13835,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,[],[f13617]) ).
fof(f13836,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,[],[f13835]) ).
fof(f13837,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,[],[f13619]) ).
fof(f13838,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,[],[f13837]) ).
fof(f13843,plain,
! [X0,X1] :
( m1_subset_1(X0,X1)
| ~ r2_hidden(X0,X1) ),
inference(ennf_transformation,[],[f675]) ).
fof(f13857,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,[],[f12317]) ).
fof(f13858,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,[],[f13857]) ).
fof(f13861,plain,
! [X0] :
( m2_lattice4(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f12269]) ).
fof(f13862,plain,
! [X0] :
( m2_lattice4(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13861]) ).
fof(f13871,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,[],[f8673]) ).
fof(f13872,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,[],[f13871]) ).
fof(f13873,plain,
! [X0] :
( m1_filter_0(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f8588]) ).
fof(f13874,plain,
! [X0] :
( m1_filter_0(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13873]) ).
fof(f13893,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,[],[f8608]) ).
fof(f13894,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,[],[f13893]) ).
fof(f13899,plain,
! [X0] :
( k1_filter_0(X0) = u1_struct_0(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f8589]) ).
fof(f13900,plain,
! [X0] :
( k1_filter_0(X0) = u1_struct_0(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13899]) ).
fof(f13955,plain,
! [X0] :
( ( v14_lattices(X0)
<=> v13_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f9439]) ).
fof(f13956,plain,
! [X0] :
( ( v14_lattices(X0)
<=> v13_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13955]) ).
fof(f13957,plain,
! [X0] :
( ( v13_lattices(X0)
<=> v14_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f9438]) ).
fof(f13958,plain,
! [X0] :
( ( v13_lattices(X0)
<=> v14_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13957]) ).
fof(f13965,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,[],[f9391]) ).
fof(f13966,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,[],[f13965]) ).
fof(f13978,plain,
! [X0] :
( ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f9463]) ).
fof(f13981,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,[],[f9363]) ).
fof(f13982,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,[],[f13981]) ).
fof(f13983,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f9358]) ).
fof(f13984,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13983]) ).
fof(f14205,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,[],[f9454]) ).
fof(f14206,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,[],[f14205]) ).
fof(f14217,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,[],[f8585]) ).
fof(f14218,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,[],[f14217]) ).
fof(f18170,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,[],[f13669]) ).
fof(f18172,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,[],[f13679]) ).
fof(f18190,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,[],[f13804]) ).
fof(f18200,plain,
( ~ r1_filter_2(u1_struct_0(sK35),k17_filter_2(sK35),k18_filter_2(sK35,k6_lattices(sK35)))
& v14_lattices(sK35)
& ~ v3_struct_0(sK35)
& v10_lattices(sK35)
& l3_lattices(sK35) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK35]),skolemize(X0,sK35)],[f13838]) ).
fof(f18237,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,[],[f13956]) ).
fof(f18238,plain,
! [X0] :
( ( ( v13_lattices(X0)
| ~ v14_lattices(k1_lattice2(X0)) )
& ( v14_lattices(k1_lattice2(X0))
| ~ v13_lattices(X0) ) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f13958]) ).
fof(f19642,plain,
! [X0,X1] :
( ~ m1_filter_2(X1,X0)
| m1_filter_0(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f18170]) ).
fof(f19650,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,[],[f18172]) ).
fof(f19682,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,[],[f13739]) ).
fof(f19755,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,[],[f18190]) ).
fof(f19782,plain,
! [X0] :
( ~ v10_lattices(X0)
| v3_struct_0(X0)
| u1_struct_0(X0) = k17_filter_2(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13828]) ).
fof(f19783,plain,
! [X0,X1] :
( ~ v10_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| k18_filter_2(X0,X1) = a_2_0_filter_2(X0,X1)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13830]) ).
fof(f19790,plain,
! [X2,X0,X1] :
( ~ v10_lattices(X0)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| r2_hidden(X1,k18_filter_2(X0,X1))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13836]) ).
fof(f19791,plain,
l3_lattices(sK35),
inference(cnf_transformation,[],[f18200]) ).
fof(f19792,plain,
v10_lattices(sK35),
inference(cnf_transformation,[],[f18200]) ).
fof(f19793,plain,
~ v3_struct_0(sK35),
inference(cnf_transformation,[],[f18200]) ).
fof(f19794,plain,
v14_lattices(sK35),
inference(cnf_transformation,[],[f18200]) ).
fof(f19795,plain,
~ r1_filter_2(u1_struct_0(sK35),k17_filter_2(sK35),k18_filter_2(sK35,k6_lattices(sK35))),
inference(cnf_transformation,[],[f18200]) ).
fof(f19800,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| m1_subset_1(X0,X1) ),
inference(cnf_transformation,[],[f13843]) ).
fof(f19825,plain,
! [X0,X1] :
( ~ m2_lattice4(X1,X0)
| m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13858]) ).
fof(f19827,plain,
! [X0] :
( ~ l3_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| m2_lattice4(u1_struct_0(X0),X0) ),
inference(cnf_transformation,[],[f13862]) ).
fof(f19840,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,[],[f13872]) ).
fof(f19841,plain,
! [X0] :
( ~ v10_lattices(X0)
| v3_struct_0(X0)
| m1_filter_0(u1_struct_0(X0),X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13874]) ).
fof(f19859,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,[],[f13894]) ).
fof(f19864,plain,
! [X0] :
( ~ v10_lattices(X0)
| v3_struct_0(X0)
| u1_struct_0(X0) = k1_filter_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13900]) ).
fof(f19917,plain,
! [X0] :
( v13_lattices(k1_lattice2(X0))
| ~ v14_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f18237]) ).
fof(f19919,plain,
! [X0] :
( ~ v13_lattices(X0)
| v14_lattices(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f18238]) ).
fof(f19920,plain,
! [X0] :
( ~ v14_lattices(k1_lattice2(X0))
| v13_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f18238]) ).
fof(f19927,plain,
! [X0] :
( ~ l3_lattices(X0)
| v3_struct_0(X0)
| u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0)) ),
inference(cnf_transformation,[],[f13966]) ).
fof(f19949,plain,
! [X0] :
( l3_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13978]) ).
fof(f19952,plain,
! [X0] :
( ~ v10_lattices(X0)
| v3_struct_0(X0)
| v10_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13982]) ).
fof(f19962,plain,
! [X0] :
( ~ v3_struct_0(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13984]) ).
fof(f20260,plain,
! [X0] :
( ~ v14_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| k6_lattices(X0) = k5_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f14206]) ).
fof(f20268,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,[],[f14218]) ).
fof(f26996,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,[],[f19650]) ).
fof(f27631,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,[],[f20268]) ).
fof(f27643,plain,
! [X0,X1] :
( ~ v13_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| u1_struct_0(X0) = X1
| ~ l3_lattices(X0)
| ~ r2_hidden(k5_lattices(X0),X1)
| ~ m1_filter_0(X1,X0) ),
inference(duplicate_literal_removal,[],[f19859]) ).
fof(f27645,plain,
! [X2,X0] :
( ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| v1_xboole_0(X0)
| r1_filter_2(X0,X2,X2) ),
inference(duplicate_literal_removal,[],[f26996]) ).
fof(f28503,plain,
( v3_struct_0(sK35)
| ~ v10_lattices(sK35)
| k6_lattices(sK35) = k5_lattices(k1_lattice2(sK35))
| ~ l3_lattices(sK35) ),
inference(resolution,[],[f20260,f19794]) ).
fof(f28504,plain,
( ~ v10_lattices(sK35)
| k6_lattices(sK35) = k5_lattices(k1_lattice2(sK35))
| ~ l3_lattices(sK35) ),
inference(forward_subsumption_resolution,[],[f28503,f19793]) ).
fof(f28505,plain,
( k6_lattices(sK35) = k5_lattices(k1_lattice2(sK35))
| ~ l3_lattices(sK35) ),
inference(forward_subsumption_resolution,[],[f28504,f19792]) ).
fof(f28506,plain,
k6_lattices(sK35) = k5_lattices(k1_lattice2(sK35)),
inference(forward_subsumption_resolution,[],[f28505,f19791]) ).
fof(f28507,plain,
( v3_struct_0(sK35)
| u1_struct_0(sK35) = k17_filter_2(sK35)
| ~ l3_lattices(sK35) ),
inference(resolution,[],[f19782,f19792]) ).
fof(f28508,plain,
( u1_struct_0(sK35) = k17_filter_2(sK35)
| ~ l3_lattices(sK35) ),
inference(forward_subsumption_resolution,[],[f28507,f19793]) ).
fof(f28509,plain,
u1_struct_0(sK35) = k17_filter_2(sK35),
inference(forward_subsumption_resolution,[],[f28508,f19791]) ).
fof(f28510,plain,
~ r1_filter_2(u1_struct_0(sK35),u1_struct_0(sK35),k18_filter_2(sK35,k6_lattices(sK35))),
inference(superposition,[],[f19795,f28509]) ).
fof(f28511,plain,
( v3_struct_0(sK35)
| u1_struct_0(sK35) = u1_struct_0(k1_lattice2(sK35)) ),
inference(resolution,[],[f19927,f19791]) ).
fof(f28512,plain,
u1_struct_0(sK35) = u1_struct_0(k1_lattice2(sK35)),
inference(forward_subsumption_resolution,[],[f28511,f19793]) ).
fof(f28513,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK35))
| v3_struct_0(sK35)
| k18_filter_2(sK35,X0) = a_2_0_filter_2(sK35,X0)
| ~ l3_lattices(sK35) ),
inference(resolution,[],[f19783,f19792]) ).
fof(f28514,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK35))
| k18_filter_2(sK35,X0) = a_2_0_filter_2(sK35,X0)
| ~ l3_lattices(sK35) ),
inference(forward_subsumption_resolution,[],[f28513,f19793]) ).
fof(f28515,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK35))
| k18_filter_2(sK35,X0) = a_2_0_filter_2(sK35,X0) ),
inference(forward_subsumption_resolution,[],[f28514,f19791]) ).
fof(f28516,plain,
( v3_struct_0(sK35)
| u1_struct_0(sK35) = k1_filter_0(sK35)
| ~ l3_lattices(sK35) ),
inference(resolution,[],[f19864,f19792]) ).
fof(f28517,plain,
( u1_struct_0(sK35) = k1_filter_0(sK35)
| ~ l3_lattices(sK35) ),
inference(forward_subsumption_resolution,[],[f28516,f19793]) ).
fof(f28518,plain,
u1_struct_0(sK35) = k1_filter_0(sK35),
inference(forward_subsumption_resolution,[],[f28517,f19791]) ).
fof(f28519,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_filter_0(sK35))
| k18_filter_2(sK35,X0) = a_2_0_filter_2(sK35,X0) ),
inference(superposition,[],[f28515,f28518]) ).
fof(f28520,plain,
~ r1_filter_2(k1_filter_0(sK35),k1_filter_0(sK35),k18_filter_2(sK35,k6_lattices(sK35))),
inference(superposition,[],[f28510,f28518]) ).
fof(f28524,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(sK35))
| ~ m1_subset_1(X1,u1_struct_0(sK35))
| v3_struct_0(sK35)
| r2_hidden(X1,k18_filter_2(sK35,X1))
| ~ l3_lattices(sK35) ),
inference(resolution,[],[f19790,f19792]) ).
fof(f28525,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(sK35))
| ~ m1_subset_1(X1,u1_struct_0(sK35))
| r2_hidden(X1,k18_filter_2(sK35,X1))
| ~ l3_lattices(sK35) ),
inference(forward_subsumption_resolution,[],[f28524,f19793]) ).
fof(f28526,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(sK35))
| ~ m1_subset_1(X1,u1_struct_0(sK35))
| r2_hidden(X1,k18_filter_2(sK35,X1)) ),
inference(forward_subsumption_resolution,[],[f28525,f19791]) ).
fof(f28527,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_filter_0(sK35))
| ~ m1_subset_1(X1,u1_struct_0(sK35))
| r2_hidden(X1,k18_filter_2(sK35,X1)) ),
inference(forward_demodulation,[],[f28526,f28518]) ).
fof(f28528,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,k1_filter_0(sK35))
| ~ m1_subset_1(X0,k1_filter_0(sK35))
| r2_hidden(X1,k18_filter_2(sK35,X1)) ),
inference(forward_demodulation,[],[f28527,f28518]) ).
fof(f28530,definition,
( spl863_39
<=> ! [X0] : ~ m1_subset_1(X0,k1_filter_0(sK35)) ),
introduced(definition,[new_symbols(definition,[spl863_39])],[avatar_definition]) ).
fof(f28531,plain,
( ! [X0] : ~ m1_subset_1(X0,k1_filter_0(sK35))
| ~ spl863_39 ),
inference(avatar_component_clause,[],[f28530]) ).
fof(f28533,definition,
( spl863_40
<=> ! [X1] :
( ~ m1_subset_1(X1,k1_filter_0(sK35))
| r2_hidden(X1,k18_filter_2(sK35,X1)) ) ),
introduced(definition,[new_symbols(definition,[spl863_40])],[avatar_definition]) ).
fof(f28534,plain,
( ! [X1] :
( ~ m1_subset_1(X1,k1_filter_0(sK35))
| r2_hidden(X1,k18_filter_2(sK35,X1)) )
| ~ spl863_40 ),
inference(avatar_component_clause,[],[f28533]) ).
fof(f28535,plain,
( spl863_39
| spl863_40 ),
inference(avatar_split_clause,[],[f28528,f28533,f28530]) ).
fof(f28541,plain,
( v3_struct_0(sK35)
| m1_filter_0(u1_struct_0(sK35),sK35)
| ~ l3_lattices(sK35) ),
inference(resolution,[],[f19841,f19792]) ).
fof(f28542,plain,
( m1_filter_0(u1_struct_0(sK35),sK35)
| ~ l3_lattices(sK35) ),
inference(forward_subsumption_resolution,[],[f28541,f19793]) ).
fof(f28543,plain,
m1_filter_0(u1_struct_0(sK35),sK35),
inference(forward_subsumption_resolution,[],[f28542,f19791]) ).
fof(f28544,plain,
m1_filter_0(k1_filter_0(sK35),sK35),
inference(forward_demodulation,[],[f28543,f28518]) ).
fof(f28546,plain,
( v3_struct_0(sK35)
| v10_lattices(k1_lattice2(sK35))
| ~ l3_lattices(sK35) ),
inference(resolution,[],[f19952,f19792]) ).
fof(f28547,plain,
( v10_lattices(k1_lattice2(sK35))
| ~ l3_lattices(sK35) ),
inference(forward_subsumption_resolution,[],[f28546,f19793]) ).
fof(f28548,plain,
v10_lattices(k1_lattice2(sK35)),
inference(forward_subsumption_resolution,[],[f28547,f19791]) ).
fof(f28557,definition,
( spl863_41
<=> l3_lattices(k1_lattice2(sK35)) ),
introduced(definition,[new_symbols(definition,[spl863_41])],[avatar_definition]) ).
fof(f28558,plain,
( ~ l3_lattices(k1_lattice2(sK35))
| spl863_41 ),
inference(avatar_component_clause,[],[f28557]) ).
fof(f28563,definition,
( spl863_43
<=> v3_struct_0(k1_lattice2(sK35)) ),
introduced(definition,[new_symbols(definition,[spl863_43])],[avatar_definition]) ).
fof(f28564,plain,
( v3_struct_0(k1_lattice2(sK35))
| ~ spl863_43 ),
inference(avatar_component_clause,[],[f28563]) ).
fof(f28591,plain,
( ~ l3_lattices(sK35)
| spl863_41 ),
inference(resolution,[],[f28558,f19949]) ).
fof(f28593,plain,
( $false
| spl863_41 ),
inference(forward_subsumption_resolution,[],[f28591,f19791]) ).
fof(f28594,plain,
spl863_41,
inference(avatar_contradiction_clause,[],[f28593]) ).
fof(f28596,plain,
( v3_struct_0(sK35)
| ~ l3_lattices(sK35)
| ~ spl863_43 ),
inference(resolution,[],[f28564,f19962]) ).
fof(f28598,plain,
( ~ l3_lattices(sK35)
| ~ spl863_43 ),
inference(forward_subsumption_resolution,[],[f28596,f19793]) ).
fof(f28599,plain,
( $false
| ~ spl863_43 ),
inference(forward_subsumption_resolution,[],[f28598,f19791]) ).
fof(f28600,plain,
~ spl863_43,
inference(avatar_contradiction_clause,[],[f28599]) ).
fof(f28620,plain,
! [X0,X1] :
( ~ m2_filter_2(X0,X1)
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| m1_filter_0(X0,k1_lattice2(X1))
| v3_struct_0(k1_lattice2(X1))
| ~ v10_lattices(k1_lattice2(X1))
| ~ l3_lattices(k1_lattice2(X1)) ),
inference(resolution,[],[f19755,f19642]) ).
fof(f28621,plain,
! [X0,X1] :
( ~ m2_filter_2(X0,X1)
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| m1_filter_0(X0,k1_lattice2(X1))
| ~ v10_lattices(k1_lattice2(X1))
| ~ l3_lattices(k1_lattice2(X1)) ),
inference(forward_subsumption_resolution,[],[f28620,f19962]) ).
fof(f28622,plain,
! [X0,X1] :
( ~ m2_filter_2(X0,X1)
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| m1_filter_0(X0,k1_lattice2(X1))
| ~ l3_lattices(k1_lattice2(X1)) ),
inference(forward_subsumption_resolution,[],[f28621,f19952]) ).
fof(f28623,plain,
! [X0,X1] :
( m1_filter_0(X0,k1_lattice2(X1))
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| ~ m2_filter_2(X0,X1) ),
inference(forward_subsumption_resolution,[],[f28622,f19949]) ).
fof(f28651,definition,
( spl863_49
<=> v1_xboole_0(k1_filter_0(sK35)) ),
introduced(definition,[new_symbols(definition,[spl863_49])],[avatar_definition]) ).
fof(f28652,plain,
( v1_xboole_0(k1_filter_0(sK35))
| ~ spl863_49 ),
inference(avatar_component_clause,[],[f28651]) ).
fof(f28755,plain,
( $false
| ~ spl863_49 ),
inference(unit_resulting_resolution,[],[f19840,f19791,f19792,f19793,f28544,f28652]) ).
fof(f28757,plain,
~ spl863_49,
inference(avatar_contradiction_clause,[],[f28755]) ).
fof(f28762,plain,
! [X0] :
( v14_lattices(k1_lattice2(k1_lattice2(X0)))
| v3_struct_0(k1_lattice2(X0))
| ~ v10_lattices(k1_lattice2(X0))
| ~ l3_lattices(k1_lattice2(X0))
| ~ v14_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(resolution,[],[f19919,f19917]) ).
fof(f28763,plain,
! [X0] :
( v14_lattices(k1_lattice2(k1_lattice2(X0)))
| ~ v10_lattices(k1_lattice2(X0))
| ~ l3_lattices(k1_lattice2(X0))
| ~ v14_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f28762,f19962]) ).
fof(f28764,plain,
! [X0] :
( v14_lattices(k1_lattice2(k1_lattice2(X0)))
| ~ l3_lattices(k1_lattice2(X0))
| ~ v14_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f28763,f19952]) ).
fof(f28765,plain,
! [X0] :
( ~ v14_lattices(X0)
| v14_lattices(k1_lattice2(k1_lattice2(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f28764,f19949]) ).
fof(f28913,plain,
( v14_lattices(k1_lattice2(k1_lattice2(sK35)))
| v3_struct_0(sK35)
| ~ v10_lattices(sK35)
| ~ l3_lattices(sK35) ),
inference(resolution,[],[f28765,f19794]) ).
fof(f28914,plain,
( v14_lattices(k1_lattice2(k1_lattice2(sK35)))
| ~ v10_lattices(sK35)
| ~ l3_lattices(sK35) ),
inference(forward_subsumption_resolution,[],[f28913,f19793]) ).
fof(f28915,plain,
( v14_lattices(k1_lattice2(k1_lattice2(sK35)))
| ~ l3_lattices(sK35) ),
inference(forward_subsumption_resolution,[],[f28914,f19792]) ).
fof(f28916,plain,
v14_lattices(k1_lattice2(k1_lattice2(sK35))),
inference(forward_subsumption_resolution,[],[f28915,f19791]) ).
fof(f28917,plain,
( v13_lattices(k1_lattice2(sK35))
| v3_struct_0(k1_lattice2(sK35))
| ~ v10_lattices(k1_lattice2(sK35))
| ~ l3_lattices(k1_lattice2(sK35)) ),
inference(resolution,[],[f28916,f19920]) ).
fof(f28922,plain,
( v13_lattices(k1_lattice2(sK35))
| v3_struct_0(k1_lattice2(sK35))
| ~ l3_lattices(k1_lattice2(sK35)) ),
inference(forward_subsumption_resolution,[],[f28917,f28548]) ).
fof(f28924,definition,
( spl863_75
<=> v13_lattices(k1_lattice2(sK35)) ),
introduced(definition,[new_symbols(definition,[spl863_75])],[avatar_definition]) ).
fof(f28925,plain,
( v13_lattices(k1_lattice2(sK35))
| ~ spl863_75 ),
inference(avatar_component_clause,[],[f28924]) ).
fof(f28926,plain,
( ~ spl863_41
| spl863_43
| spl863_75 ),
inference(avatar_split_clause,[],[f28922,f28924,f28563,f28557]) ).
fof(f29001,plain,
( ! [X0] :
( v3_struct_0(k1_lattice2(sK35))
| ~ v10_lattices(k1_lattice2(sK35))
| u1_struct_0(k1_lattice2(sK35)) = X0
| ~ l3_lattices(k1_lattice2(sK35))
| ~ r2_hidden(k5_lattices(k1_lattice2(sK35)),X0)
| ~ m1_filter_0(X0,k1_lattice2(sK35)) )
| ~ spl863_75 ),
inference(resolution,[],[f27643,f28925]) ).
fof(f29002,plain,
( ! [X0] :
( v3_struct_0(k1_lattice2(sK35))
| u1_struct_0(k1_lattice2(sK35)) = X0
| ~ l3_lattices(k1_lattice2(sK35))
| ~ r2_hidden(k5_lattices(k1_lattice2(sK35)),X0)
| ~ m1_filter_0(X0,k1_lattice2(sK35)) )
| ~ spl863_75 ),
inference(forward_subsumption_resolution,[],[f29001,f28548]) ).
fof(f29004,plain,
( ! [X0] :
( u1_struct_0(sK35) = X0
| v3_struct_0(k1_lattice2(sK35))
| ~ l3_lattices(k1_lattice2(sK35))
| ~ r2_hidden(k5_lattices(k1_lattice2(sK35)),X0)
| ~ m1_filter_0(X0,k1_lattice2(sK35)) )
| ~ spl863_75 ),
inference(forward_demodulation,[],[f29002,f28512]) ).
fof(f29006,plain,
( ! [X0] :
( k1_filter_0(sK35) = X0
| v3_struct_0(k1_lattice2(sK35))
| ~ l3_lattices(k1_lattice2(sK35))
| ~ r2_hidden(k5_lattices(k1_lattice2(sK35)),X0)
| ~ m1_filter_0(X0,k1_lattice2(sK35)) )
| ~ spl863_75 ),
inference(forward_demodulation,[],[f29004,f28518]) ).
fof(f29008,plain,
( ! [X0] :
( ~ r2_hidden(k6_lattices(sK35),X0)
| k1_filter_0(sK35) = X0
| v3_struct_0(k1_lattice2(sK35))
| ~ l3_lattices(k1_lattice2(sK35))
| ~ m1_filter_0(X0,k1_lattice2(sK35)) )
| ~ spl863_75 ),
inference(forward_demodulation,[],[f29006,f28506]) ).
fof(f29010,definition,
( spl863_80
<=> ! [X0] :
( ~ r2_hidden(k6_lattices(sK35),X0)
| ~ m1_filter_0(X0,k1_lattice2(sK35))
| k1_filter_0(sK35) = X0 ) ),
introduced(definition,[new_symbols(definition,[spl863_80])],[avatar_definition]) ).
fof(f29011,plain,
( ! [X0] :
( ~ r2_hidden(k6_lattices(sK35),X0)
| ~ m1_filter_0(X0,k1_lattice2(sK35))
| k1_filter_0(sK35) = X0 )
| ~ spl863_80 ),
inference(avatar_component_clause,[],[f29010]) ).
fof(f29012,plain,
( ~ spl863_41
| spl863_43
| spl863_80
| ~ spl863_75 ),
inference(avatar_split_clause,[],[f29008,f28924,f29010,f28563,f28557]) ).
fof(f29111,plain,
( v3_struct_0(sK35)
| ~ v10_lattices(sK35)
| m2_lattice4(u1_struct_0(sK35),sK35) ),
inference(resolution,[],[f19827,f19791]) ).
fof(f29113,plain,
( ~ v10_lattices(sK35)
| m2_lattice4(u1_struct_0(sK35),sK35) ),
inference(forward_subsumption_resolution,[],[f29111,f19793]) ).
fof(f29114,plain,
m2_lattice4(u1_struct_0(sK35),sK35),
inference(forward_subsumption_resolution,[],[f29113,f19792]) ).
fof(f29115,plain,
m2_lattice4(k1_filter_0(sK35),sK35),
inference(forward_demodulation,[],[f29114,f28518]) ).
fof(f29116,plain,
( m1_subset_1(k1_filter_0(sK35),k1_zfmisc_1(u1_struct_0(sK35)))
| v3_struct_0(sK35)
| ~ v10_lattices(sK35)
| ~ l3_lattices(sK35) ),
inference(resolution,[],[f29115,f19825]) ).
fof(f29117,plain,
( m1_subset_1(k1_filter_0(sK35),k1_zfmisc_1(u1_struct_0(sK35)))
| ~ v10_lattices(sK35)
| ~ l3_lattices(sK35) ),
inference(forward_subsumption_resolution,[],[f29116,f19793]) ).
fof(f29118,plain,
( m1_subset_1(k1_filter_0(sK35),k1_zfmisc_1(u1_struct_0(sK35)))
| ~ l3_lattices(sK35) ),
inference(forward_subsumption_resolution,[],[f29117,f19792]) ).
fof(f29119,plain,
m1_subset_1(k1_filter_0(sK35),k1_zfmisc_1(u1_struct_0(sK35))),
inference(forward_subsumption_resolution,[],[f29118,f19791]) ).
fof(f29120,plain,
m1_subset_1(k1_filter_0(sK35),k1_zfmisc_1(k1_filter_0(sK35))),
inference(forward_demodulation,[],[f29119,f28518]) ).
fof(f29122,plain,
( v1_xboole_0(k1_filter_0(sK35))
| r1_filter_2(k1_filter_0(sK35),k1_filter_0(sK35),k1_filter_0(sK35)) ),
inference(resolution,[],[f29120,f27645]) ).
fof(f29124,definition,
( spl863_94
<=> r1_filter_2(k1_filter_0(sK35),k1_filter_0(sK35),k1_filter_0(sK35)) ),
introduced(definition,[new_symbols(definition,[spl863_94])],[avatar_definition]) ).
fof(f29125,plain,
( r1_filter_2(k1_filter_0(sK35),k1_filter_0(sK35),k1_filter_0(sK35))
| ~ spl863_94 ),
inference(avatar_component_clause,[],[f29124]) ).
fof(f29126,plain,
( spl863_94
| spl863_49 ),
inference(avatar_split_clause,[],[f29122,f28651,f29124]) ).
fof(f29594,plain,
! [X0,X1] :
( ~ v14_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| m1_subset_1(k6_lattices(X0),X1)
| ~ l3_lattices(X0)
| ~ m1_filter_0(X1,X0) ),
inference(resolution,[],[f19800,f27631]) ).
fof(f29879,plain,
( $false
| ~ spl863_39 ),
inference(unit_resulting_resolution,[],[f29594,f19793,f19791,f19794,f19792,f28544,f28531]) ).
fof(f29880,plain,
! [X0] :
( v3_struct_0(sK35)
| ~ v10_lattices(sK35)
| m1_subset_1(k6_lattices(sK35),X0)
| ~ l3_lattices(sK35)
| ~ m1_filter_0(X0,sK35) ),
inference(resolution,[],[f29594,f19794]) ).
fof(f29882,plain,
~ spl863_39,
inference(avatar_contradiction_clause,[],[f29879]) ).
fof(f29883,plain,
! [X0] :
( ~ v10_lattices(sK35)
| m1_subset_1(k6_lattices(sK35),X0)
| ~ l3_lattices(sK35)
| ~ m1_filter_0(X0,sK35) ),
inference(forward_subsumption_resolution,[],[f29880,f19793]) ).
fof(f29884,plain,
! [X0] :
( m1_subset_1(k6_lattices(sK35),X0)
| ~ l3_lattices(sK35)
| ~ m1_filter_0(X0,sK35) ),
inference(forward_subsumption_resolution,[],[f29883,f19792]) ).
fof(f29885,plain,
! [X0] :
( ~ m1_filter_0(X0,sK35)
| m1_subset_1(k6_lattices(sK35),X0) ),
inference(forward_subsumption_resolution,[],[f29884,f19791]) ).
fof(f29949,plain,
m1_subset_1(k6_lattices(sK35),k1_filter_0(sK35)),
inference(resolution,[],[f29885,f28544]) ).
fof(f29955,plain,
k18_filter_2(sK35,k6_lattices(sK35)) = a_2_0_filter_2(sK35,k6_lattices(sK35)),
inference(resolution,[],[f29949,f28519]) ).
fof(f29956,plain,
( r2_hidden(k6_lattices(sK35),k18_filter_2(sK35,k6_lattices(sK35)))
| ~ spl863_40 ),
inference(resolution,[],[f29949,f28534]) ).
fof(f29964,plain,
( ~ m1_filter_0(k18_filter_2(sK35,k6_lattices(sK35)),k1_lattice2(sK35))
| k18_filter_2(sK35,k6_lattices(sK35)) = k1_filter_0(sK35)
| ~ spl863_40
| ~ spl863_80 ),
inference(resolution,[],[f29956,f29011]) ).
fof(f29967,plain,
( ~ m1_filter_0(a_2_0_filter_2(sK35,k6_lattices(sK35)),k1_lattice2(sK35))
| k18_filter_2(sK35,k6_lattices(sK35)) = k1_filter_0(sK35)
| ~ spl863_40
| ~ spl863_80 ),
inference(forward_demodulation,[],[f29964,f29955]) ).
fof(f29968,plain,
( k1_filter_0(sK35) = a_2_0_filter_2(sK35,k6_lattices(sK35))
| ~ m1_filter_0(a_2_0_filter_2(sK35,k6_lattices(sK35)),k1_lattice2(sK35))
| ~ spl863_40
| ~ spl863_80 ),
inference(forward_demodulation,[],[f29967,f29955]) ).
fof(f29970,definition,
( spl863_190
<=> m1_filter_0(a_2_0_filter_2(sK35,k6_lattices(sK35)),k1_lattice2(sK35)) ),
introduced(definition,[new_symbols(definition,[spl863_190])],[avatar_definition]) ).
fof(f29971,plain,
( ~ m1_filter_0(a_2_0_filter_2(sK35,k6_lattices(sK35)),k1_lattice2(sK35))
| spl863_190 ),
inference(avatar_component_clause,[],[f29970]) ).
fof(f29973,definition,
( spl863_191
<=> k1_filter_0(sK35) = a_2_0_filter_2(sK35,k6_lattices(sK35)) ),
introduced(definition,[new_symbols(definition,[spl863_191])],[avatar_definition]) ).
fof(f29974,plain,
( k1_filter_0(sK35) = a_2_0_filter_2(sK35,k6_lattices(sK35))
| ~ spl863_191 ),
inference(avatar_component_clause,[],[f29973]) ).
fof(f29975,plain,
( ~ spl863_190
| spl863_191
| ~ spl863_40
| ~ spl863_80 ),
inference(avatar_split_clause,[],[f29968,f29010,f28533,f29973,f29970]) ).
fof(f29978,plain,
~ r1_filter_2(k1_filter_0(sK35),k1_filter_0(sK35),a_2_0_filter_2(sK35,k6_lattices(sK35))),
inference(superposition,[],[f28520,f29955]) ).
fof(f29985,plain,
( m2_filter_2(a_2_0_filter_2(sK35,k6_lattices(sK35)),sK35)
| v3_struct_0(sK35)
| ~ v10_lattices(sK35)
| ~ l3_lattices(sK35)
| ~ m1_subset_1(k6_lattices(sK35),u1_struct_0(sK35)) ),
inference(superposition,[],[f19682,f29955]) ).
fof(f29987,plain,
( m2_filter_2(a_2_0_filter_2(sK35,k6_lattices(sK35)),sK35)
| ~ v10_lattices(sK35)
| ~ l3_lattices(sK35)
| ~ m1_subset_1(k6_lattices(sK35),u1_struct_0(sK35)) ),
inference(forward_subsumption_resolution,[],[f29985,f19793]) ).
fof(f29994,plain,
( m2_filter_2(a_2_0_filter_2(sK35,k6_lattices(sK35)),sK35)
| ~ l3_lattices(sK35)
| ~ m1_subset_1(k6_lattices(sK35),u1_struct_0(sK35)) ),
inference(forward_subsumption_resolution,[],[f29987,f19792]) ).
fof(f30000,plain,
( m2_filter_2(a_2_0_filter_2(sK35,k6_lattices(sK35)),sK35)
| ~ m1_subset_1(k6_lattices(sK35),u1_struct_0(sK35)) ),
inference(forward_subsumption_resolution,[],[f29994,f19791]) ).
fof(f30005,plain,
( ~ m1_subset_1(k6_lattices(sK35),k1_filter_0(sK35))
| m2_filter_2(a_2_0_filter_2(sK35,k6_lattices(sK35)),sK35) ),
inference(forward_demodulation,[],[f30000,f28518]) ).
fof(f30010,plain,
m2_filter_2(a_2_0_filter_2(sK35,k6_lattices(sK35)),sK35),
inference(forward_subsumption_resolution,[],[f30005,f29949]) ).
fof(f30087,plain,
( v3_struct_0(sK35)
| ~ v10_lattices(sK35)
| ~ l3_lattices(sK35)
| ~ m2_filter_2(a_2_0_filter_2(sK35,k6_lattices(sK35)),sK35)
| spl863_190 ),
inference(resolution,[],[f29971,f28623]) ).
fof(f30088,plain,
( ~ v10_lattices(sK35)
| ~ l3_lattices(sK35)
| ~ m2_filter_2(a_2_0_filter_2(sK35,k6_lattices(sK35)),sK35)
| spl863_190 ),
inference(forward_subsumption_resolution,[],[f30087,f19793]) ).
fof(f30089,plain,
( ~ l3_lattices(sK35)
| ~ m2_filter_2(a_2_0_filter_2(sK35,k6_lattices(sK35)),sK35)
| spl863_190 ),
inference(forward_subsumption_resolution,[],[f30088,f19792]) ).
fof(f30090,plain,
( ~ m2_filter_2(a_2_0_filter_2(sK35,k6_lattices(sK35)),sK35)
| spl863_190 ),
inference(forward_subsumption_resolution,[],[f30089,f19791]) ).
fof(f30091,plain,
( $false
| spl863_190 ),
inference(forward_subsumption_resolution,[],[f30090,f30010]) ).
fof(f30092,plain,
spl863_190,
inference(avatar_contradiction_clause,[],[f30091]) ).
fof(f30096,plain,
( ~ r1_filter_2(k1_filter_0(sK35),k1_filter_0(sK35),k1_filter_0(sK35))
| ~ spl863_191 ),
inference(superposition,[],[f29978,f29974]) ).
fof(f30097,plain,
( $false
| ~ spl863_94
| ~ spl863_191 ),
inference(forward_subsumption_resolution,[],[f30096,f29125]) ).
fof(f30098,plain,
( ~ spl863_94
| ~ spl863_191 ),
inference(avatar_contradiction_clause,[],[f30097]) ).
cnf(s34,plain,
( spl863_39
| spl863_40 ),
inference(sat_conversion,[],[f28535]) ).
cnf(s40,plain,
spl863_41,
inference(sat_conversion,[],[f28594]) ).
cnf(s42,plain,
~ spl863_43,
inference(sat_conversion,[],[f28600]) ).
cnf(s59,plain,
~ spl863_49,
inference(sat_conversion,[],[f28757]) ).
cnf(s66,plain,
( ~ spl863_41
| spl863_43
| spl863_75 ),
inference(sat_conversion,[],[f28926]) ).
cnf(s71,plain,
( ~ spl863_41
| spl863_43
| ~ spl863_75
| spl863_80 ),
inference(sat_conversion,[],[f29012]) ).
cnf(s82,plain,
( spl863_49
| spl863_94 ),
inference(sat_conversion,[],[f29126]) ).
cnf(s152,plain,
~ spl863_39,
inference(sat_conversion,[],[f29882]) ).
cnf(s165,plain,
( ~ spl863_40
| ~ spl863_80
| ~ spl863_190
| spl863_191 ),
inference(sat_conversion,[],[f29975]) ).
cnf(s172,plain,
spl863_190,
inference(sat_conversion,[],[f30092]) ).
cnf(s173,plain,
( ~ spl863_94
| ~ spl863_191 ),
inference(sat_conversion,[],[f30098]) ).
cnf(s174,plain,
( ~ spl863_40
| ~ spl863_80
| spl863_191 ),
inference(rat,[],[s165,s172]) ).
cnf(s208,plain,
spl863_94,
inference(rat,[],[s82,s59]) ).
cnf(s209,plain,
~ spl863_191,
inference(rat,[],[s173,s208]) ).
cnf(s220,plain,
spl863_75,
inference(rat,[],[s66,s42,s40]) ).
cnf(s231,plain,
spl863_80,
inference(rat,[],[s71,s40,s42,s220]) ).
cnf(s239,plain,
~ spl863_40,
inference(rat,[],[s174,s209,s231]) ).
cnf(s247,plain,
$false,
inference(rat,[],[s34,s239,s152]) ).
fof(f30099,plain,
$false,
inference(avatar_sat_refutation,[],[s247]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT306+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.39 % Computer : n019.cluster.edu
% 0.11/0.39 % Model : x86_64 x86_64
% 0.11/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.39 % Memory : 8046.5625MB
% 0.11/0.39 % OS : Linux 6.8.0-71-generic
% 0.11/0.39 % CPULimit : 300
% 0.11/0.39 % WCLimit : 300
% 0.11/0.39 % DateTime : Sun Sep 27 14:26:06 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.43 Running first-order theorem proving
% 0.11/0.43 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 13.07/3.38 % (3140456)Detected formulas, will run a generic FOF schedule.
% 13.07/3.38 % (3140467)dis-21_1_sil=8000:lcm=predicate:random_seed=1059640945:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2993 on theBenchmark for (2993ds/129Mi)
% 13.07/3.38 % (3140464)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=945079857:i=109:sd=1:ins=1:gsp=on:ss=axioms_2993 on theBenchmark for (2993ds/109Mi)
% 13.07/3.38 % (3140461)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=2470582097:i=141193_2993 on theBenchmark for (2993ds/141193Mi)
% 13.07/3.38 % (3140463)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=2768709397:i=141695:sd=1:nm=32:gsp=on:ss=included_2993 on theBenchmark for (2993ds/141695Mi)
% 13.07/3.38 % (3140462)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=2704884515:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2993 on theBenchmark for (2993ds/134677Mi)
% 13.07/3.38 % (3140465)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3718446336:i=119:av=off:ss=axioms_2993 on theBenchmark for (2993ds/119Mi)
% 13.07/3.38 % (3140467)Instruction limit reached!
% 13.07/3.38 % (3140467)------------------------------
% 13.07/3.38 % (3140467)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.07/3.38 % (3140467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.07/3.38 % (3140467)CaDiCaL version: 2.1.3
% 13.07/3.38 % (3140467)Termination reason: Instruction limit
% 13.07/3.38 % (3140467)Termination phase: Preprocessing 1
% 13.07/3.38 % (3140467)Time elapsed: 0.057 s
% 13.07/3.38 % (3140467)Peak memory usage: 104 MB
% 13.07/3.38 % (3140467)Instructions burned: 130 (million)
% 13.07/3.38 % (3140466)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3076823622:s2a=on:i=139:gtg=position_2993 on theBenchmark for (2993ds/139Mi)
% 13.07/3.38 % (3140464)Refutation not found, incomplete strategy
% 13.07/3.38 % (3140464)------------------------------
% 13.07/3.38 % (3140464)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.07/3.38 % (3140464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.07/3.38 % (3140464)CaDiCaL version: 2.1.3
% 13.07/3.38 % (3140464)Termination reason: Refutation not found, incomplete strategy
% 13.07/3.38 % (3140464)Time elapsed: 0.065 s
% 13.07/3.38 % (3140464)Peak memory usage: 107 MB
% 13.07/3.38 % (3140464)Instructions burned: 80 (million)
% 13.07/3.38 % (3140466)Instruction limit reached!
% 13.07/3.38 % (3140466)------------------------------
% 13.07/3.38 % (3140466)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.07/3.38 % (3140466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.07/3.38 % (3140466)CaDiCaL version: 2.1.3
% 13.07/3.38 % (3140466)Termination reason: Instruction limit
% 13.07/3.38 % (3140466)Termination phase: Property scanning
% 13.07/3.38 % (3140466)Time elapsed: 0.059 s
% 13.07/3.38 % (3140466)Peak memory usage: 102 MB
% 13.07/3.38 % (3140466)Instructions burned: 141 (million)
% 13.07/3.38 % (3140465)Instruction limit reached!
% 13.07/3.38 % (3140465)------------------------------
% 13.07/3.38 % (3140465)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.07/3.38 % (3140465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.07/3.38 % (3140465)CaDiCaL version: 2.1.3
% 13.07/3.38 % (3140465)Termination reason: Instruction limit
% 13.07/3.38 % (3140465)Termination phase: Function definition elimination
% 13.07/3.38 % (3140465)Time elapsed: 0.091 s
% 13.07/3.38 % (3140465)Peak memory usage: 105 MB
% 13.07/3.38 % (3140465)Instructions burned: 120 (million)
% 13.07/3.38 % (3140475)lrs+10_1_sil=8000:sp=occurrence:random_seed=2202142068:i=285:sd=3:ss=axioms:sgt=8_2991 on theBenchmark for (2991ds/285Mi)
% 13.07/3.38 % (3140476)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2176715948:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2990 on theBenchmark for (2990ds/157Mi)
% 13.07/3.38 % (3140475)Instruction limit reached!
% 13.07/3.38 % (3140475)------------------------------
% 13.07/3.38 % (3140475)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.07/3.38 % (3140475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.07/3.38 % (3140475)CaDiCaL version: 2.1.3
% 13.07/3.38 % (3140475)Termination reason: Instruction limit
% 20.14/4.32 % (3140475)Termination phase: Saturation
% 20.14/4.32 % (3140475)Time elapsed: 0.108 s
% 20.14/4.32 % (3140475)Peak memory usage: 109 MB
% 20.14/4.32 % (3140475)Instructions burned: 288 (million)
% 20.14/4.32 % (3140477)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1511963920:i=325:sd=1:ss=axioms:sgt=32_2990 on theBenchmark for (2990ds/325Mi)
% 20.14/4.32 % (3140476)Instruction limit reached!
% 20.14/4.32 % (3140476)------------------------------
% 20.14/4.32 % (3140476)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.14/4.32 % (3140476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.14/4.32 % (3140476)CaDiCaL version: 2.1.3
% 20.14/4.32 % (3140476)Termination reason: Instruction limit
% 20.14/4.32 % (3140476)Termination phase: Property scanning
% 20.14/4.32 % (3140476)Time elapsed: 0.068 s
% 20.14/4.32 % (3140476)Peak memory usage: 102 MB
% 20.14/4.32 % (3140476)Instructions burned: 158 (million)
% 20.14/4.32 % (3140464)------------------------------
% 20.14/4.32 % (3140464)------------------------------
% 20.14/4.32 % (3140477)Refutation not found, incomplete strategy
% 20.14/4.32 % (3140477)------------------------------
% 20.14/4.32 % (3140477)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.14/4.32 % (3140477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.14/4.32 % (3140477)CaDiCaL version: 2.1.3
% 20.14/4.32 % (3140477)Termination reason: Refutation not found, incomplete strategy
% 20.14/4.32 % (3140477)Time elapsed: 0.068 s
% 20.14/4.32 % (3140477)Peak memory usage: 107 MB
% 20.14/4.32 % (3140477)Instructions burned: 78 (million)
% 20.14/4.32 % (3140480)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=4232240152:s2a=on:i=248:s2at=1.23:gtg=position_2989 on theBenchmark for (2989ds/248Mi)
% 20.14/4.32 % (3140480)Instruction limit reached!
% 20.14/4.32 % (3140480)------------------------------
% 20.14/4.32 % (3140480)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.14/4.32 % (3140480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.14/4.32 % (3140480)CaDiCaL version: 2.1.3
% 20.14/4.32 % (3140480)Termination reason: Instruction limit
% 20.14/4.32 % (3140480)Termination phase: SInE selection
% 20.14/4.32 % (3140480)Time elapsed: 0.071 s
% 20.14/4.32 % (3140480)Peak memory usage: 103 MB
% 20.14/4.32 % (3140480)Instructions burned: 250 (million)
% 20.14/4.32 % (3140483)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2637840440:i=2350_2988 on theBenchmark for (2988ds/2350Mi)
% 20.14/4.32 % (3140482)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2392261262:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2988 on theBenchmark for (2988ds/294Mi)
% 20.14/4.32 % (3140477)------------------------------
% 20.14/4.32 % (3140477)------------------------------
% 20.14/4.32 % (3140485)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1601488113:cts=off:i=113:fsr=off:ss=included:sgt=4_2987 on theBenchmark for (2987ds/113Mi)
% 20.14/4.32 % (3140485)Instruction limit reached!
% 20.14/4.32 % (3140485)------------------------------
% 20.14/4.32 % (3140485)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.14/4.32 % (3140485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.14/4.32 % (3140485)CaDiCaL version: 2.1.3
% 20.14/4.32 % (3140485)Termination reason: Instruction limit
% 20.14/4.32 % (3140485)Termination phase: Preprocessing 3
% 20.14/4.32 % (3140485)Time elapsed: 0.055 s
% 20.14/4.32 % (3140485)Peak memory usage: 105 MB
% 20.14/4.32 % (3140485)Instructions burned: 115 (million)
% 20.14/4.32 % (3140482)Instruction limit reached!
% 20.14/4.32 % (3140482)------------------------------
% 20.14/4.32 % (3140482)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.14/4.32 % (3140482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.14/4.32 % (3140482)CaDiCaL version: 2.1.3
% 20.14/4.32 % (3140482)Termination reason: Instruction limit
% 20.14/4.32 % (3140482)Termination phase: Saturation
% 20.14/4.32 % (3140482)Time elapsed: 0.191 s
% 20.14/4.32 % (3140482)Peak memory usage: 110 MB
% 20.14/4.32 % (3140482)Instructions burned: 294 (million)
% 20.14/4.32 % (3140489)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1200293267:i=127:av=off:fsr=off:sup=off_2985 on theBenchmark for (2985ds/127Mi)
% 20.14/4.32 % (3140490)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=4034036175:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2985 on theBenchmark for (2985ds/114Mi)
% 21.46/4.59 % (3140490)Instruction limit reached!
% 21.46/4.59 % (3140490)------------------------------
% 21.46/4.59 % (3140490)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.46/4.59 % (3140490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.46/4.59 % (3140490)CaDiCaL version: 2.1.3
% 21.46/4.59 % (3140490)Termination reason: Instruction limit
% 21.46/4.59 % (3140490)Termination phase: Property scanning
% 21.46/4.59 % (3140490)Time elapsed: 0.027 s
% 21.46/4.59 % (3140490)Peak memory usage: 102 MB
% 21.46/4.59 % (3140490)Instructions burned: 118 (million)
% 21.46/4.59 % (3140491)lrs+10_1_sil=8000:sp=occurrence:random_seed=3566417146:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2984 on theBenchmark for (2984ds/907Mi)
% 21.46/4.59 % (3140489)Instruction limit reached!
% 21.46/4.59 % (3140489)------------------------------
% 21.46/4.59 % (3140489)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.46/4.59 % (3140489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.46/4.59 % (3140489)CaDiCaL version: 2.1.3
% 21.46/4.59 % (3140489)Termination reason: Instruction limit
% 21.46/4.59 % (3140489)Termination phase: Preprocessing 2
% 21.46/4.59 % (3140489)Time elapsed: 0.104 s
% 21.46/4.59 % (3140489)Peak memory usage: 106 MB
% 21.46/4.59 % (3140489)Instructions burned: 128 (million)
% 21.46/4.59 % (3140494)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1260017876:i=437:sd=1:aac=none:ss=included_2983 on theBenchmark for (2983ds/437Mi)
% 21.46/4.59 % (3140494)Refutation not found, incomplete strategy
% 21.46/4.59 % (3140494)------------------------------
% 21.46/4.59 % (3140494)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.46/4.59 % (3140494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.46/4.59 % (3140494)CaDiCaL version: 2.1.3
% 21.46/4.59 % (3140494)Termination reason: Refutation not found, incomplete strategy
% 21.46/4.59 % (3140494)Time elapsed: 0.053 s
% 21.46/4.59 % (3140494)Peak memory usage: 108 MB
% 21.46/4.59 % (3140494)Instructions burned: 127 (million)
% 21.46/4.59 % (3140496)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=4175692399:i=5202:ss=axioms:sgt=16_2982 on theBenchmark for (2982ds/5202Mi)
% 21.46/4.59 % (3140494)------------------------------
% 21.46/4.59 % (3140494)------------------------------
% 21.46/4.59 % (3140499)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=239724605:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2980 on theBenchmark for (2980ds/134Mi)
% 21.46/4.59 % (3140499)Instruction limit reached!
% 21.46/4.59 % (3140499)------------------------------
% 21.46/4.59 % (3140499)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.46/4.59 % (3140499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.46/4.59 % (3140499)CaDiCaL version: 2.1.3
% 21.46/4.59 % (3140499)Termination reason: Instruction limit
% 21.46/4.59 % (3140499)Termination phase: Property scanning
% 21.46/4.59 % (3140499)Time elapsed: 0.058 s
% 21.46/4.59 % (3140499)Peak memory usage: 106 MB
% 21.46/4.59 % (3140499)Instructions burned: 137 (million)
% 21.46/4.59 % (3140491)Instruction limit reached!
% 21.46/4.59 % (3140491)------------------------------
% 21.46/4.59 % (3140491)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.46/4.59 % (3140491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.46/4.59 % (3140491)CaDiCaL version: 2.1.3
% 21.46/4.59 % (3140491)Termination reason: Instruction limit
% 21.46/4.59 % (3140491)Termination phase: Saturation
% 21.46/4.59 % (3140491)Time elapsed: 0.588 s
% 21.46/4.59 % (3140491)Peak memory usage: 121 MB
% 21.46/4.59 % (3140491)Instructions burned: 908 (million)
% 21.46/4.59 % (3140501)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=4241916271:st=8:i=592:sd=3:ep=RST:ss=axioms_2978 on theBenchmark for (2978ds/592Mi)
% 21.46/4.59 % (3140502)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2237928384:st=3:i=13193:sd=3:ss=axioms_2977 on theBenchmark for (2977ds/13193Mi)
% 21.46/4.59 % (3140501)Instruction limit reached!
% 21.46/4.59 % (3140501)------------------------------
% 21.46/4.59 % (3140501)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.46/4.59 % (3140501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.46/4.59 % (3140501)CaDiCaL version: 2.1.3
% 21.46/4.59 % (3140501)Termination reason: Instruction limit
% 21.46/4.59 % (3140501)Termination phase: Property scanning
% 21.46/4.59 % (3140501)Time elapsed: 0.226 s
% 21.46/4.59 % (3140501)Peak memory usage: 123 MB
% 21.46/4.59 % (3140501)Instructions burned: 597 (million)
% 21.46/4.59 % (3140506)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=196947236:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2974 on theBenchmark for (2974ds/125Mi)
% 21.46/4.59 % (3140506)Instruction limit reached!
% 21.46/4.59 % (3140506)------------------------------
% 21.46/4.59 % (3140506)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.46/4.59 % (3140506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.46/4.59 % (3140506)CaDiCaL version: 2.1.3
% 21.46/4.59 % (3140506)Termination reason: Instruction limit
% 21.46/4.59 % (3140506)Termination phase: Property scanning
% 21.46/4.59 % (3140506)Time elapsed: 0.029 s
% 21.46/4.59 % (3140506)Peak memory usage: 102 MB
% 21.46/4.59 % (3140506)Instructions burned: 126 (million)
% 21.46/4.59 % (3140483)Instruction limit reached!
% 21.46/4.59 % (3140483)------------------------------
% 21.46/4.59 % (3140483)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.46/4.59 % (3140483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.46/4.59 % (3140483)CaDiCaL version: 2.1.3
% 21.46/4.59 % (3140483)Termination reason: Instruction limit
% 21.46/4.59 % (3140483)Termination phase: Saturation
% 21.46/4.59 % (3140483)Time elapsed: 1.434 s
% 21.46/4.59 % (3140483)Peak memory usage: 240 MB
% 21.46/4.59 % (3140483)Instructions burned: 2351 (million)
% 21.46/4.59 % (3140508)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2551881888:i=134:gtgl=5:slsql=off:gtg=exists_sym_2973 on theBenchmark for (2973ds/134Mi)
% 21.46/4.59 % (3140508)Instruction limit reached!
% 21.46/4.59 % (3140508)------------------------------
% 21.46/4.59 % (3140508)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.46/4.59 % (3140508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.46/4.59 % (3140508)CaDiCaL version: 2.1.3
% 21.46/4.59 % (3140508)Termination reason: Instruction limit
% 21.46/4.59 % (3140508)Termination phase: Property scanning
% 21.46/4.59 % (3140508)Time elapsed: 0.032 s
% 21.46/4.59 % (3140508)Peak memory usage: 102 MB
% 21.46/4.59 % (3140508)Instructions burned: 138 (million)
% 21.46/4.59 % (3140509)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2265889287:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2972 on theBenchmark for (2972ds/141Mi)
% 21.46/4.59 % (3140511)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1094067671:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2971 on theBenchmark for (2971ds/431Mi)
% 21.46/4.59 % (3140511)Refutation not found, incomplete strategy
% 21.46/4.59 % (3140511)------------------------------
% 21.46/4.59 % (3140511)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.46/4.59 % (3140511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.46/4.59 % (3140511)CaDiCaL version: 2.1.3
% 21.46/4.59 % (3140511)Termination reason: Refutation not found, incomplete strategy
% 21.46/4.59 % (3140511)Time elapsed: 0.041 s
% 21.46/4.59 % (3140511)Peak memory usage: 107 MB
% 21.46/4.59 % (3140511)Instructions burned: 80 (million)
% 21.46/4.59 % (3140509)Refutation not found, incomplete strategy
% 21.46/4.59 % (3140509)------------------------------
% 21.46/4.59 % (3140509)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.46/4.59 % (3140509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.46/4.59 % (3140509)CaDiCaL version: 2.1.3
% 21.46/4.59 % (3140509)Termination reason: Refutation not found, incomplete strategy
% 21.46/4.59 % (3140509)Time elapsed: 0.068 s
% 21.46/4.59 % (3140509)Peak memory usage: 107 MB
% 21.46/4.59 % (3140509)Instructions burned: 78 (million)
% 21.46/4.59 % (3140511)------------------------------
% 21.46/4.59 % (3140511)------------------------------
% 21.46/4.59 % (3140509)------------------------------
% 21.46/4.59 % (3140509)------------------------------
% 21.46/4.59 % (3140514)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=118896873:i=6060:aac=none:ins=25_2968 on theBenchmark for (2968ds/6060Mi)
% 21.46/4.59 % (3140462)First to succeed.
% 21.46/4.59 % (3140462)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3140456"
% 21.46/4.59 % (3140515)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=4168728679:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2967 on theBenchmark for (2967ds/150Mi)
% 21.46/4.60 % (3140515)Instruction limit reached!
% 21.46/4.60 % (3140515)------------------------------
% 21.46/4.60 % (3140515)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.46/4.60 % (3140515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.46/4.60 % (3140515)CaDiCaL version: 2.1.3
% 21.46/4.60 % (3140515)Termination reason: Instruction limit
% 21.46/4.60 % (3140515)Termination phase: Preprocessing 1
% 21.46/4.60 % (3140515)Time elapsed: 0.113 s
% 21.46/4.60 % (3140515)Peak memory usage: 103 MB
% 21.46/4.60 % (3140515)Instructions burned: 151 (million)
% 21.46/4.60 % (3140462)Refutation found. Thanks to Tanya!
% 21.46/4.60 % SZS status Theorem for theBenchmark
% 21.46/4.60 % SZS output start Proof for theBenchmark
% See solution above
% 22.49/4.70 % (3140462)------------------------------
% 22.49/4.70 % (3140462)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.49/4.70 % (3140462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.49/4.70 % (3140462)CaDiCaL version: 2.1.3
% 22.49/4.70 % (3140462)Termination reason: Refutation
% 22.49/4.70 % (3140462)Time elapsed: 2.541 s
% 22.49/4.70 % (3140462)Peak memory usage: 224 MB
% 22.49/4.70 % (3140462)Instructions burned: 4136 (million)
% 22.49/4.70 % (3140462)------------------------------
% 22.49/4.70 % (3140462)------------------------------
% 22.49/4.70 % (3140456)Success in time 3.721 s
% 22.49/4.70 % Vampire exiting
%------------------------------------------------------------------------------