%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT338+4 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n018.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:47:05 AM UTC 2026
% Result : Theorem 35.75s 8.99s
% Output : Refutation 36.61s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 16
% Syntax : Number of formulae : 119 ( 15 unt; 9 def)
% Number of atoms : 363 ( 10 equ)
% Maximal formula atoms : 11 ( 3 avg)
% Number of connectives : 402 ( 158 ~; 157 |; 67 &)
% ( 9 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 28 ( 26 usr; 10 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 2 con; 0-2 aty)
% Number of variables : 82 ( 0 sgn 78 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f28693,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& l3_lattices(X0) )
=> m1_subset_1(k15_lattice3(X0,X1),u1_struct_0(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k15_lattice3) ).
fof(f28694,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& l3_lattices(X0) )
=> m1_subset_1(k16_lattice3(X0,X1),u1_struct_0(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k16_lattice3) ).
fof(f46212,axiom,
! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0) )
=> ( ~ v3_struct_0(k11_conlat_1(X0))
& v3_lattices(k11_conlat_1(X0))
& v4_lattices(k11_conlat_1(X0))
& v5_lattices(k11_conlat_1(X0))
& v6_lattices(k11_conlat_1(X0))
& v7_lattices(k11_conlat_1(X0))
& v8_lattices(k11_conlat_1(X0))
& v9_lattices(k11_conlat_1(X0))
& v10_lattices(k11_conlat_1(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc4_conlat_1) ).
fof(f46277,axiom,
! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0) )
=> ( ~ v3_struct_0(k11_conlat_1(X0))
& v10_lattices(k11_conlat_1(X0))
& l3_lattices(k11_conlat_1(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t46_conlat_1) ).
fof(f46278,axiom,
! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(k11_conlat_1(X0)))
=> k12_conlat_1(X0,X1) = X1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d24_conlat_1) ).
fof(f46310,axiom,
! [X0,X1] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0)
& m1_subset_1(X1,u1_struct_0(k11_conlat_1(X0))) )
=> ( v6_conlat_1(k12_conlat_1(X0,X1),X0)
& ~ v7_conlat_1(k12_conlat_1(X0,X1),X0)
& v9_conlat_1(k12_conlat_1(X0,X1),X0)
& l3_conlat_1(k12_conlat_1(X0,X1),X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k12_conlat_1) ).
fof(f49798,conjecture,
! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0) )
=> ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(k11_conlat_1(X0))))
=> ( ~ v7_conlat_1(k16_lattice3(k11_conlat_1(X0),X1),X0)
& v9_conlat_1(k16_lattice3(k11_conlat_1(X0),X1),X0)
& l3_conlat_1(k16_lattice3(k11_conlat_1(X0),X1),X0)
& ~ v7_conlat_1(k15_lattice3(k11_conlat_1(X0),X1),X0)
& v9_conlat_1(k15_lattice3(k11_conlat_1(X0),X1),X0)
& l3_conlat_1(k15_lattice3(k11_conlat_1(X0),X1),X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t4_conlat_2) ).
fof(f49799,negated_conjecture,
~ ! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0) )
=> ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(k11_conlat_1(X0))))
=> ( ~ v7_conlat_1(k16_lattice3(k11_conlat_1(X0),X1),X0)
& v9_conlat_1(k16_lattice3(k11_conlat_1(X0),X1),X0)
& l3_conlat_1(k16_lattice3(k11_conlat_1(X0),X1),X0)
& ~ v7_conlat_1(k15_lattice3(k11_conlat_1(X0),X1),X0)
& v9_conlat_1(k15_lattice3(k11_conlat_1(X0),X1),X0)
& l3_conlat_1(k15_lattice3(k11_conlat_1(X0),X1),X0) ) ) ),
inference(negated_conjecture,[status(cth)],[f49798]) ).
fof(f49921,plain,
? [X0] :
( ? [X1] :
( ( v7_conlat_1(k16_lattice3(k11_conlat_1(X0),X1),X0)
| ~ v9_conlat_1(k16_lattice3(k11_conlat_1(X0),X1),X0)
| ~ l3_conlat_1(k16_lattice3(k11_conlat_1(X0),X1),X0)
| v7_conlat_1(k15_lattice3(k11_conlat_1(X0),X1),X0)
| ~ v9_conlat_1(k15_lattice3(k11_conlat_1(X0),X1),X0)
| ~ l3_conlat_1(k15_lattice3(k11_conlat_1(X0),X1),X0) )
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(k11_conlat_1(X0)))) )
& ~ v3_conlat_1(X0)
& l2_conlat_1(X0) ),
inference(ennf_transformation,[],[f49799]) ).
fof(f49922,plain,
? [X0] :
( ? [X1] :
( ( v7_conlat_1(k16_lattice3(k11_conlat_1(X0),X1),X0)
| ~ v9_conlat_1(k16_lattice3(k11_conlat_1(X0),X1),X0)
| ~ l3_conlat_1(k16_lattice3(k11_conlat_1(X0),X1),X0)
| v7_conlat_1(k15_lattice3(k11_conlat_1(X0),X1),X0)
| ~ v9_conlat_1(k15_lattice3(k11_conlat_1(X0),X1),X0)
| ~ l3_conlat_1(k15_lattice3(k11_conlat_1(X0),X1),X0) )
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(k11_conlat_1(X0)))) )
& ~ v3_conlat_1(X0)
& l2_conlat_1(X0) ),
inference(flattening,[],[f49921]) ).
fof(f49931,plain,
! [X0] :
( ( ~ v3_struct_0(k11_conlat_1(X0))
& v10_lattices(k11_conlat_1(X0))
& l3_lattices(k11_conlat_1(X0)) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(ennf_transformation,[],[f46277]) ).
fof(f49932,plain,
! [X0] :
( ( ~ v3_struct_0(k11_conlat_1(X0))
& v10_lattices(k11_conlat_1(X0))
& l3_lattices(k11_conlat_1(X0)) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(flattening,[],[f49931]) ).
fof(f49935,plain,
! [X0] :
( ( ~ v3_struct_0(k11_conlat_1(X0))
& v3_lattices(k11_conlat_1(X0))
& v4_lattices(k11_conlat_1(X0))
& v5_lattices(k11_conlat_1(X0))
& v6_lattices(k11_conlat_1(X0))
& v7_lattices(k11_conlat_1(X0))
& v8_lattices(k11_conlat_1(X0))
& v9_lattices(k11_conlat_1(X0))
& v10_lattices(k11_conlat_1(X0)) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(ennf_transformation,[],[f46212]) ).
fof(f49936,plain,
! [X0] :
( ( ~ v3_struct_0(k11_conlat_1(X0))
& v3_lattices(k11_conlat_1(X0))
& v4_lattices(k11_conlat_1(X0))
& v5_lattices(k11_conlat_1(X0))
& v6_lattices(k11_conlat_1(X0))
& v7_lattices(k11_conlat_1(X0))
& v8_lattices(k11_conlat_1(X0))
& v9_lattices(k11_conlat_1(X0))
& v10_lattices(k11_conlat_1(X0)) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(flattening,[],[f49935]) ).
fof(f50167,plain,
! [X0,X1] :
( m1_subset_1(k15_lattice3(X0,X1),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f28693]) ).
fof(f50168,plain,
! [X0,X1] :
( m1_subset_1(k15_lattice3(X0,X1),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f50167]) ).
fof(f50177,plain,
! [X0,X1] :
( m1_subset_1(k16_lattice3(X0,X1),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f28694]) ).
fof(f50178,plain,
! [X0,X1] :
( m1_subset_1(k16_lattice3(X0,X1),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f50177]) ).
fof(f51789,plain,
! [X0,X1] :
( ( v6_conlat_1(k12_conlat_1(X0,X1),X0)
& ~ v7_conlat_1(k12_conlat_1(X0,X1),X0)
& v9_conlat_1(k12_conlat_1(X0,X1),X0)
& l3_conlat_1(k12_conlat_1(X0,X1),X0) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0)
| ~ m1_subset_1(X1,u1_struct_0(k11_conlat_1(X0))) ),
inference(ennf_transformation,[],[f46310]) ).
fof(f51790,plain,
! [X0,X1] :
( ( v6_conlat_1(k12_conlat_1(X0,X1),X0)
& ~ v7_conlat_1(k12_conlat_1(X0,X1),X0)
& v9_conlat_1(k12_conlat_1(X0,X1),X0)
& l3_conlat_1(k12_conlat_1(X0,X1),X0) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0)
| ~ m1_subset_1(X1,u1_struct_0(k11_conlat_1(X0))) ),
inference(flattening,[],[f51789]) ).
fof(f51791,plain,
! [X0] :
( ! [X1] :
( k12_conlat_1(X0,X1) = X1
| ~ m1_subset_1(X1,u1_struct_0(k11_conlat_1(X0))) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(ennf_transformation,[],[f46278]) ).
fof(f51792,plain,
! [X0] :
( ! [X1] :
( k12_conlat_1(X0,X1) = X1
| ~ m1_subset_1(X1,u1_struct_0(k11_conlat_1(X0))) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(flattening,[],[f51791]) ).
fof(f57084,plain,
( ( v7_conlat_1(k16_lattice3(k11_conlat_1(sK35),sK36),sK35)
| ~ v9_conlat_1(k16_lattice3(k11_conlat_1(sK35),sK36),sK35)
| ~ l3_conlat_1(k16_lattice3(k11_conlat_1(sK35),sK36),sK35)
| v7_conlat_1(k15_lattice3(k11_conlat_1(sK35),sK36),sK35)
| ~ v9_conlat_1(k15_lattice3(k11_conlat_1(sK35),sK36),sK35)
| ~ l3_conlat_1(k15_lattice3(k11_conlat_1(sK35),sK36),sK35) )
& m1_subset_1(sK36,k1_zfmisc_1(u1_struct_0(k11_conlat_1(sK35))))
& ~ v3_conlat_1(sK35)
& l2_conlat_1(sK35) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK35,sK36]),skolemize(X0,sK35),skolemize(X1,sK36)],[f49922]) ).
fof(f59068,plain,
l2_conlat_1(sK35),
inference(cnf_transformation,[],[f57084]) ).
fof(f59069,plain,
~ v3_conlat_1(sK35),
inference(cnf_transformation,[],[f57084]) ).
fof(f59071,plain,
( v7_conlat_1(k16_lattice3(k11_conlat_1(sK35),sK36),sK35)
| ~ v9_conlat_1(k16_lattice3(k11_conlat_1(sK35),sK36),sK35)
| ~ l3_conlat_1(k16_lattice3(k11_conlat_1(sK35),sK36),sK35)
| v7_conlat_1(k15_lattice3(k11_conlat_1(sK35),sK36),sK35)
| ~ v9_conlat_1(k15_lattice3(k11_conlat_1(sK35),sK36),sK35)
| ~ l3_conlat_1(k15_lattice3(k11_conlat_1(sK35),sK36),sK35) ),
inference(cnf_transformation,[],[f57084]) ).
fof(f59088,plain,
! [X0] :
( ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| l3_lattices(k11_conlat_1(X0)) ),
inference(cnf_transformation,[],[f49932]) ).
fof(f59109,plain,
! [X0] :
( ~ v3_struct_0(k11_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f49936]) ).
fof(f59557,plain,
! [X0,X1] :
( ~ l3_lattices(X0)
| v3_struct_0(X0)
| m1_subset_1(k15_lattice3(X0,X1),u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f50168]) ).
fof(f59573,plain,
! [X0,X1] :
( ~ l3_lattices(X0)
| v3_struct_0(X0)
| m1_subset_1(k16_lattice3(X0,X1),u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f50178]) ).
fof(f62300,plain,
! [X0,X1] :
( ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| l3_conlat_1(k12_conlat_1(X0,X1),X0)
| ~ m1_subset_1(X1,u1_struct_0(k11_conlat_1(X0))) ),
inference(cnf_transformation,[],[f51790]) ).
fof(f62301,plain,
! [X0,X1] :
( ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| v9_conlat_1(k12_conlat_1(X0,X1),X0)
| ~ m1_subset_1(X1,u1_struct_0(k11_conlat_1(X0))) ),
inference(cnf_transformation,[],[f51790]) ).
fof(f62302,plain,
! [X0,X1] :
( ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| ~ v7_conlat_1(k12_conlat_1(X0,X1),X0)
| ~ m1_subset_1(X1,u1_struct_0(k11_conlat_1(X0))) ),
inference(cnf_transformation,[],[f51790]) ).
fof(f62304,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u1_struct_0(k11_conlat_1(X0)))
| k12_conlat_1(X0,X1) = X1
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f51792]) ).
fof(f71772,definition,
( spl1311_41
<=> l3_conlat_1(k15_lattice3(k11_conlat_1(sK35),sK36),sK35) ),
introduced(definition,[new_symbols(definition,[spl1311_41])],[avatar_definition]) ).
fof(f71773,plain,
( ~ l3_conlat_1(k15_lattice3(k11_conlat_1(sK35),sK36),sK35)
| spl1311_41 ),
inference(avatar_component_clause,[],[f71772]) ).
fof(f71775,definition,
( spl1311_42
<=> v9_conlat_1(k15_lattice3(k11_conlat_1(sK35),sK36),sK35) ),
introduced(definition,[new_symbols(definition,[spl1311_42])],[avatar_definition]) ).
fof(f71776,plain,
( ~ v9_conlat_1(k15_lattice3(k11_conlat_1(sK35),sK36),sK35)
| spl1311_42 ),
inference(avatar_component_clause,[],[f71775]) ).
fof(f71778,definition,
( spl1311_43
<=> v7_conlat_1(k15_lattice3(k11_conlat_1(sK35),sK36),sK35) ),
introduced(definition,[new_symbols(definition,[spl1311_43])],[avatar_definition]) ).
fof(f71779,plain,
( v7_conlat_1(k15_lattice3(k11_conlat_1(sK35),sK36),sK35)
| ~ spl1311_43 ),
inference(avatar_component_clause,[],[f71778]) ).
fof(f71781,definition,
( spl1311_44
<=> l3_conlat_1(k16_lattice3(k11_conlat_1(sK35),sK36),sK35) ),
introduced(definition,[new_symbols(definition,[spl1311_44])],[avatar_definition]) ).
fof(f71782,plain,
( ~ l3_conlat_1(k16_lattice3(k11_conlat_1(sK35),sK36),sK35)
| spl1311_44 ),
inference(avatar_component_clause,[],[f71781]) ).
fof(f71784,definition,
( spl1311_45
<=> v9_conlat_1(k16_lattice3(k11_conlat_1(sK35),sK36),sK35) ),
introduced(definition,[new_symbols(definition,[spl1311_45])],[avatar_definition]) ).
fof(f71785,plain,
( ~ v9_conlat_1(k16_lattice3(k11_conlat_1(sK35),sK36),sK35)
| spl1311_45 ),
inference(avatar_component_clause,[],[f71784]) ).
fof(f71787,definition,
( spl1311_46
<=> v7_conlat_1(k16_lattice3(k11_conlat_1(sK35),sK36),sK35) ),
introduced(definition,[new_symbols(definition,[spl1311_46])],[avatar_definition]) ).
fof(f71788,plain,
( v7_conlat_1(k16_lattice3(k11_conlat_1(sK35),sK36),sK35)
| ~ spl1311_46 ),
inference(avatar_component_clause,[],[f71787]) ).
fof(f71789,plain,
( ~ spl1311_41
| ~ spl1311_42
| spl1311_43
| ~ spl1311_44
| ~ spl1311_45
| spl1311_46 ),
inference(avatar_split_clause,[],[f59071,f71787,f71784,f71781,f71778,f71775,f71772]) ).
fof(f71956,plain,
! [X0] :
( v3_conlat_1(sK35)
| v9_conlat_1(k12_conlat_1(sK35,X0),sK35)
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK35))) ),
inference(resolution,[],[f59068,f62301]) ).
fof(f71957,plain,
! [X0] :
( v3_conlat_1(sK35)
| l3_conlat_1(k12_conlat_1(sK35,X0),sK35)
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK35))) ),
inference(resolution,[],[f59068,f62300]) ).
fof(f71958,plain,
! [X0] :
( v3_conlat_1(sK35)
| ~ v7_conlat_1(k12_conlat_1(sK35,X0),sK35)
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK35))) ),
inference(resolution,[],[f59068,f62302]) ).
fof(f71959,plain,
! [X0] :
( ~ v7_conlat_1(k12_conlat_1(sK35,X0),sK35)
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK35))) ),
inference(forward_subsumption_resolution,[],[f71958,f59069]) ).
fof(f71960,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK35)))
| l3_conlat_1(k12_conlat_1(sK35,X0),sK35) ),
inference(forward_subsumption_resolution,[],[f71957,f59069]) ).
fof(f71961,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK35)))
| v9_conlat_1(k12_conlat_1(sK35,X0),sK35) ),
inference(forward_subsumption_resolution,[],[f71956,f59069]) ).
fof(f71965,plain,
( v3_conlat_1(sK35)
| l3_lattices(k11_conlat_1(sK35)) ),
inference(resolution,[],[f59088,f59068]) ).
fof(f71966,plain,
l3_lattices(k11_conlat_1(sK35)),
inference(forward_subsumption_resolution,[],[f71965,f59069]) ).
fof(f71967,plain,
! [X0] :
( v3_struct_0(k11_conlat_1(sK35))
| m1_subset_1(k15_lattice3(k11_conlat_1(sK35),X0),u1_struct_0(k11_conlat_1(sK35))) ),
inference(resolution,[],[f71966,f59557]) ).
fof(f71968,plain,
! [X0] :
( v3_struct_0(k11_conlat_1(sK35))
| m1_subset_1(k16_lattice3(k11_conlat_1(sK35),X0),u1_struct_0(k11_conlat_1(sK35))) ),
inference(resolution,[],[f71966,f59573]) ).
fof(f71970,definition,
( spl1311_51
<=> ! [X0] : m1_subset_1(k16_lattice3(k11_conlat_1(sK35),X0),u1_struct_0(k11_conlat_1(sK35))) ),
introduced(definition,[new_symbols(definition,[spl1311_51])],[avatar_definition]) ).
fof(f71971,plain,
( ! [X0] : m1_subset_1(k16_lattice3(k11_conlat_1(sK35),X0),u1_struct_0(k11_conlat_1(sK35)))
| ~ spl1311_51 ),
inference(avatar_component_clause,[],[f71970]) ).
fof(f71973,definition,
( spl1311_52
<=> v3_struct_0(k11_conlat_1(sK35)) ),
introduced(definition,[new_symbols(definition,[spl1311_52])],[avatar_definition]) ).
fof(f71974,plain,
( v3_struct_0(k11_conlat_1(sK35))
| ~ spl1311_52 ),
inference(avatar_component_clause,[],[f71973]) ).
fof(f71975,plain,
( spl1311_51
| spl1311_52 ),
inference(avatar_split_clause,[],[f71968,f71973,f71970]) ).
fof(f71977,definition,
( spl1311_53
<=> ! [X0] : m1_subset_1(k15_lattice3(k11_conlat_1(sK35),X0),u1_struct_0(k11_conlat_1(sK35))) ),
introduced(definition,[new_symbols(definition,[spl1311_53])],[avatar_definition]) ).
fof(f71978,plain,
( ! [X0] : m1_subset_1(k15_lattice3(k11_conlat_1(sK35),X0),u1_struct_0(k11_conlat_1(sK35)))
| ~ spl1311_53 ),
inference(avatar_component_clause,[],[f71977]) ).
fof(f71979,plain,
( spl1311_53
| spl1311_52 ),
inference(avatar_split_clause,[],[f71967,f71973,f71977]) ).
fof(f71981,plain,
( v3_conlat_1(sK35)
| ~ l2_conlat_1(sK35)
| ~ spl1311_52 ),
inference(resolution,[],[f71974,f59109]) ).
fof(f71983,plain,
( ~ l2_conlat_1(sK35)
| ~ spl1311_52 ),
inference(forward_subsumption_resolution,[],[f71981,f59069]) ).
fof(f71984,plain,
( $false
| ~ spl1311_52 ),
inference(forward_subsumption_resolution,[],[f71983,f59068]) ).
fof(f71985,plain,
~ spl1311_52,
inference(avatar_contradiction_clause,[],[f71984]) ).
fof(f71986,plain,
( ! [X0] : l3_conlat_1(k12_conlat_1(sK35,k15_lattice3(k11_conlat_1(sK35),X0)),sK35)
| ~ spl1311_53 ),
inference(resolution,[],[f71978,f71960]) ).
fof(f71987,plain,
( ! [X0] : v9_conlat_1(k12_conlat_1(sK35,k15_lattice3(k11_conlat_1(sK35),X0)),sK35)
| ~ spl1311_53 ),
inference(resolution,[],[f71978,f71961]) ).
fof(f71988,plain,
( ! [X0] :
( k15_lattice3(k11_conlat_1(sK35),X0) = k12_conlat_1(sK35,k15_lattice3(k11_conlat_1(sK35),X0))
| v3_conlat_1(sK35)
| ~ l2_conlat_1(sK35) )
| ~ spl1311_53 ),
inference(resolution,[],[f71978,f62304]) ).
fof(f71989,plain,
( ! [X0] :
( k15_lattice3(k11_conlat_1(sK35),X0) = k12_conlat_1(sK35,k15_lattice3(k11_conlat_1(sK35),X0))
| ~ l2_conlat_1(sK35) )
| ~ spl1311_53 ),
inference(forward_subsumption_resolution,[],[f71988,f59069]) ).
fof(f71990,plain,
( ! [X0] : k15_lattice3(k11_conlat_1(sK35),X0) = k12_conlat_1(sK35,k15_lattice3(k11_conlat_1(sK35),X0))
| ~ spl1311_53 ),
inference(forward_subsumption_resolution,[],[f71989,f59068]) ).
fof(f71991,plain,
( ! [X0] : l3_conlat_1(k12_conlat_1(sK35,k16_lattice3(k11_conlat_1(sK35),X0)),sK35)
| ~ spl1311_51 ),
inference(resolution,[],[f71971,f71960]) ).
fof(f71992,plain,
( ! [X0] : v9_conlat_1(k12_conlat_1(sK35,k16_lattice3(k11_conlat_1(sK35),X0)),sK35)
| ~ spl1311_51 ),
inference(resolution,[],[f71971,f71961]) ).
fof(f71993,plain,
( ! [X0] :
( k16_lattice3(k11_conlat_1(sK35),X0) = k12_conlat_1(sK35,k16_lattice3(k11_conlat_1(sK35),X0))
| v3_conlat_1(sK35)
| ~ l2_conlat_1(sK35) )
| ~ spl1311_51 ),
inference(resolution,[],[f71971,f62304]) ).
fof(f71994,plain,
( ! [X0] :
( k16_lattice3(k11_conlat_1(sK35),X0) = k12_conlat_1(sK35,k16_lattice3(k11_conlat_1(sK35),X0))
| ~ l2_conlat_1(sK35) )
| ~ spl1311_51 ),
inference(forward_subsumption_resolution,[],[f71993,f59069]) ).
fof(f71995,plain,
( ! [X0] : k16_lattice3(k11_conlat_1(sK35),X0) = k12_conlat_1(sK35,k16_lattice3(k11_conlat_1(sK35),X0))
| ~ spl1311_51 ),
inference(forward_subsumption_resolution,[],[f71994,f59068]) ).
fof(f71996,plain,
( ! [X0] :
( ~ v7_conlat_1(k15_lattice3(k11_conlat_1(sK35),X0),sK35)
| ~ m1_subset_1(k15_lattice3(k11_conlat_1(sK35),X0),u1_struct_0(k11_conlat_1(sK35))) )
| ~ spl1311_53 ),
inference(superposition,[],[f71959,f71990]) ).
fof(f71997,plain,
( ! [X0] : ~ v7_conlat_1(k15_lattice3(k11_conlat_1(sK35),X0),sK35)
| ~ spl1311_53 ),
inference(forward_subsumption_resolution,[],[f71996,f71978]) ).
fof(f71998,plain,
( ! [X0] : l3_conlat_1(k15_lattice3(k11_conlat_1(sK35),X0),sK35)
| ~ spl1311_53 ),
inference(superposition,[],[f71986,f71990]) ).
fof(f71999,plain,
( ! [X0] : v9_conlat_1(k15_lattice3(k11_conlat_1(sK35),X0),sK35)
| ~ spl1311_53 ),
inference(superposition,[],[f71987,f71990]) ).
fof(f72000,plain,
( ! [X0] :
( ~ v7_conlat_1(k16_lattice3(k11_conlat_1(sK35),X0),sK35)
| ~ m1_subset_1(k16_lattice3(k11_conlat_1(sK35),X0),u1_struct_0(k11_conlat_1(sK35))) )
| ~ spl1311_51 ),
inference(superposition,[],[f71959,f71995]) ).
fof(f72001,plain,
( ! [X0] : ~ v7_conlat_1(k16_lattice3(k11_conlat_1(sK35),X0),sK35)
| ~ spl1311_51 ),
inference(forward_subsumption_resolution,[],[f72000,f71971]) ).
fof(f72002,plain,
( ! [X0] : l3_conlat_1(k16_lattice3(k11_conlat_1(sK35),X0),sK35)
| ~ spl1311_51 ),
inference(superposition,[],[f71991,f71995]) ).
fof(f72003,plain,
( ! [X0] : v9_conlat_1(k16_lattice3(k11_conlat_1(sK35),X0),sK35)
| ~ spl1311_51 ),
inference(superposition,[],[f71992,f71995]) ).
fof(f72004,plain,
( $false
| spl1311_45
| ~ spl1311_51 ),
inference(unit_resulting_resolution,[],[f72003,f71785]) ).
fof(f72007,plain,
( spl1311_45
| ~ spl1311_51 ),
inference(avatar_contradiction_clause,[],[f72004]) ).
fof(f72008,plain,
( $false
| spl1311_41
| ~ spl1311_53 ),
inference(forward_subsumption_resolution,[],[f71773,f71998]) ).
fof(f72009,plain,
( spl1311_41
| ~ spl1311_53 ),
inference(avatar_contradiction_clause,[],[f72008]) ).
fof(f72010,plain,
( $false
| spl1311_42
| ~ spl1311_53 ),
inference(forward_subsumption_resolution,[],[f71776,f71999]) ).
fof(f72011,plain,
( spl1311_42
| ~ spl1311_53 ),
inference(avatar_contradiction_clause,[],[f72010]) ).
fof(f72012,plain,
( $false
| spl1311_44
| ~ spl1311_51 ),
inference(forward_subsumption_resolution,[],[f71782,f72002]) ).
fof(f72013,plain,
( spl1311_44
| ~ spl1311_51 ),
inference(avatar_contradiction_clause,[],[f72012]) ).
fof(f72014,plain,
( $false
| ~ spl1311_43
| ~ spl1311_53 ),
inference(forward_subsumption_resolution,[],[f71779,f71997]) ).
fof(f72015,plain,
( ~ spl1311_43
| ~ spl1311_53 ),
inference(avatar_contradiction_clause,[],[f72014]) ).
fof(f72016,plain,
( $false
| ~ spl1311_46
| ~ spl1311_51 ),
inference(forward_subsumption_resolution,[],[f71788,f72001]) ).
fof(f72017,plain,
( ~ spl1311_46
| ~ spl1311_51 ),
inference(avatar_contradiction_clause,[],[f72016]) ).
cnf(s32,plain,
( ~ spl1311_41
| ~ spl1311_42
| spl1311_43
| ~ spl1311_44
| ~ spl1311_45
| spl1311_46 ),
inference(sat_conversion,[],[f71789]) ).
cnf(s38,plain,
( spl1311_51
| spl1311_52 ),
inference(sat_conversion,[],[f71975]) ).
cnf(s39,plain,
( spl1311_52
| spl1311_53 ),
inference(sat_conversion,[],[f71979]) ).
cnf(s41,plain,
~ spl1311_52,
inference(sat_conversion,[],[f71985]) ).
cnf(s43,plain,
( spl1311_45
| ~ spl1311_51 ),
inference(sat_conversion,[],[f72007]) ).
cnf(s44,plain,
( spl1311_41
| ~ spl1311_53 ),
inference(sat_conversion,[],[f72009]) ).
cnf(s45,plain,
( spl1311_42
| ~ spl1311_53 ),
inference(sat_conversion,[],[f72011]) ).
cnf(s46,plain,
( spl1311_44
| ~ spl1311_51 ),
inference(sat_conversion,[],[f72013]) ).
cnf(s47,plain,
( ~ spl1311_43
| ~ spl1311_53 ),
inference(sat_conversion,[],[f72015]) ).
cnf(s48,plain,
( ~ spl1311_46
| ~ spl1311_51 ),
inference(sat_conversion,[],[f72017]) ).
cnf(s49,plain,
spl1311_53,
inference(rat,[],[s39,s41]) ).
cnf(s50,plain,
~ spl1311_43,
inference(rat,[],[s47,s49]) ).
cnf(s51,plain,
spl1311_42,
inference(rat,[],[s45,s49]) ).
cnf(s52,plain,
spl1311_41,
inference(rat,[],[s44,s49]) ).
cnf(s53,plain,
spl1311_51,
inference(rat,[],[s38,s41]) ).
cnf(s54,plain,
~ spl1311_46,
inference(rat,[],[s48,s53]) ).
cnf(s55,plain,
spl1311_44,
inference(rat,[],[s46,s53]) ).
cnf(s56,plain,
spl1311_45,
inference(rat,[],[s43,s53]) ).
cnf(s57,plain,
$false,
inference(rat,[],[s32,s54,s56,s55,s50,s51,s52]) ).
fof(f72018,plain,
$false,
inference(avatar_sat_refutation,[],[s57]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT338+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.38 % Computer : n018.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Sun Sep 27 14:49:49 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.42 Running first-order theorem proving
% 0.10/0.42 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
% 17.09/6.32 % (2432768)Detected formulas, will run a generic FOF schedule.
% 17.09/6.32 % (2432777)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2904832731:i=119:av=off:ss=axioms_2964 on theBenchmark for (2964ds/119Mi)
% 17.09/6.32 % (2432773)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=2008494846:i=141193_2964 on theBenchmark for (2964ds/141193Mi)
% 17.09/6.32 % (2432774)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=357238046:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2964 on theBenchmark for (2964ds/134677Mi)
% 17.09/6.32 % (2432776)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2725177505:i=109:sd=1:ins=1:gsp=on:ss=axioms_2964 on theBenchmark for (2964ds/109Mi)
% 17.09/6.32 % (2432775)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=3453625688:i=141695:sd=1:nm=32:gsp=on:ss=included_2964 on theBenchmark for (2964ds/141695Mi)
% 17.09/6.32 % (2432779)dis-21_1_sil=8000:lcm=predicate:random_seed=286436040:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2964 on theBenchmark for (2964ds/129Mi)
% 17.09/6.32 % (2432778)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1770721619:s2a=on:i=139:gtg=position_2964 on theBenchmark for (2964ds/139Mi)
% 17.09/6.32 % (2432777)Instruction limit reached!
% 17.09/6.32 % (2432777)------------------------------
% 17.09/6.32 % (2432777)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.09/6.32 % (2432777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.09/6.32 % (2432777)CaDiCaL version: 2.1.3
% 17.09/6.32 % (2432777)Termination reason: Instruction limit
% 17.09/6.32 % (2432777)Termination phase: SInE selection
% 17.09/6.32 % (2432777)Time elapsed: 0.054 s
% 17.09/6.32 % (2432777)Peak memory usage: 163 MB
% 17.09/6.32 % (2432777)Instructions burned: 121 (million)
% 17.09/6.32 % (2432776)Instruction limit reached!
% 17.09/6.32 % (2432776)------------------------------
% 17.09/6.32 % (2432776)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.09/6.32 % (2432776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.09/6.32 % (2432776)CaDiCaL version: 2.1.3
% 17.09/6.32 % (2432776)Termination reason: Instruction limit
% 17.09/6.32 % (2432776)Termination phase: SInE selection
% 17.09/6.32 % (2432776)Time elapsed: 0.084 s
% 17.09/6.32 % (2432776)Peak memory usage: 163 MB
% 17.09/6.32 % (2432776)Instructions burned: 109 (million)
% 17.09/6.32 % (2432778)Instruction limit reached!
% 17.09/6.32 % (2432778)------------------------------
% 17.09/6.32 % (2432778)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.09/6.32 % (2432778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.09/6.32 % (2432778)CaDiCaL version: 2.1.3
% 17.09/6.32 % (2432778)Termination reason: Instruction limit
% 17.09/6.32 % (2432778)Termination phase: Property scanning
% 17.09/6.32 % (2432778)Time elapsed: 0.066 s
% 17.09/6.32 % (2432778)Peak memory usage: 163 MB
% 17.09/6.32 % (2432778)Instructions burned: 141 (million)
% 17.09/6.32 % (2432779)Instruction limit reached!
% 17.09/6.32 % (2432779)------------------------------
% 17.09/6.32 % (2432779)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.09/6.32 % (2432779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.09/6.32 % (2432779)CaDiCaL version: 2.1.3
% 17.09/6.32 % (2432779)Termination reason: Instruction limit
% 17.09/6.32 % (2432779)Termination phase: SInE selection
% 17.09/6.32 % (2432779)Time elapsed: 0.100 s
% 17.09/6.32 % (2432779)Peak memory usage: 163 MB
% 17.09/6.32 % (2432779)Instructions burned: 129 (million)
% 17.09/6.32 % (2432787)lrs+10_1_sil=8000:sp=occurrence:random_seed=1583439911:i=285:sd=3:ss=axioms:sgt=8_2962 on theBenchmark for (2962ds/285Mi)
% 17.09/6.32 % (2432788)lrs+10_1_sil=32000:urr=on:br=off:random_seed=790664019:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2961 on theBenchmark for (2961ds/157Mi)
% 17.09/6.32 % (2432789)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3795598162:i=325:sd=1:ss=axioms:sgt=32_2961 on theBenchmark for (2961ds/325Mi)
% 17.09/6.32 % (2432787)Instruction limit reached!
% 17.09/6.32 % (2432787)------------------------------
% 17.09/6.32 % (2432787)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.09/6.32 % (2432787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.29/7.31 % (2432787)CaDiCaL version: 2.1.3
% 24.29/7.31 % (2432787)Termination reason: Instruction limit
% 24.29/7.31 % (2432787)Termination phase: SInE selection
% 24.29/7.31 % (2432787)Time elapsed: 0.119 s
% 24.29/7.31 % (2432787)Peak memory usage: 164 MB
% 24.29/7.31 % (2432787)Instructions burned: 287 (million)
% 24.29/7.31 % (2432790)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=2848464272:s2a=on:i=248:s2at=1.23:gtg=position_2961 on theBenchmark for (2961ds/248Mi)
% 24.29/7.31 % (2432788)Instruction limit reached!
% 24.29/7.31 % (2432788)------------------------------
% 24.29/7.31 % (2432788)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.29/7.31 % (2432788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.29/7.31 % (2432788)CaDiCaL version: 2.1.3
% 24.29/7.31 % (2432788)Termination reason: Instruction limit
% 24.29/7.31 % (2432788)Termination phase: Property scanning
% 24.29/7.31 % (2432788)Time elapsed: 0.073 s
% 24.29/7.31 % (2432788)Peak memory usage: 164 MB
% 24.29/7.31 % (2432788)Instructions burned: 158 (million)
% 24.29/7.31 % (2432794)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3287140892:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2960 on theBenchmark for (2960ds/294Mi)
% 24.29/7.31 % (2432790)Instruction limit reached!
% 24.29/7.31 % (2432790)------------------------------
% 24.29/7.31 % (2432790)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.29/7.31 % (2432790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.29/7.31 % (2432790)CaDiCaL version: 2.1.3
% 24.29/7.31 % (2432790)Termination reason: Instruction limit
% 24.29/7.31 % (2432790)Termination phase: Property scanning
% 24.29/7.31 % (2432790)Time elapsed: 0.110 s
% 24.29/7.31 % (2432790)Peak memory usage: 164 MB
% 24.29/7.31 % (2432790)Instructions burned: 250 (million)
% 24.29/7.31 % (2432796)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2351990760:i=2350_2959 on theBenchmark for (2959ds/2350Mi)
% 24.29/7.31 % (2432789)Instruction limit reached!
% 24.29/7.31 % (2432789)------------------------------
% 24.29/7.31 % (2432789)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.29/7.31 % (2432789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.29/7.31 % (2432789)CaDiCaL version: 2.1.3
% 24.29/7.31 % (2432789)Termination reason: Instruction limit
% 24.29/7.31 % (2432789)Termination phase: SInE selection
% 24.29/7.31 % (2432789)Time elapsed: 0.245 s
% 24.29/7.31 % (2432789)Peak memory usage: 164 MB
% 24.29/7.31 % (2432789)Instructions burned: 326 (million)
% 24.29/7.31 % (2432794)Instruction limit reached!
% 24.29/7.31 % (2432794)------------------------------
% 24.29/7.31 % (2432794)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.29/7.31 % (2432794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.29/7.31 % (2432794)CaDiCaL version: 2.1.3
% 24.29/7.31 % (2432794)Termination reason: Instruction limit
% 24.29/7.31 % (2432794)Termination phase: SInE selection
% 24.29/7.31 % (2432794)Time elapsed: 0.118 s
% 24.29/7.31 % (2432794)Peak memory usage: 164 MB
% 24.29/7.31 % (2432794)Instructions burned: 296 (million)
% 24.29/7.31 % (2432798)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1990672256:cts=off:i=113:fsr=off:ss=included:sgt=4_2958 on theBenchmark for (2958ds/113Mi)
% 24.29/7.31 % (2432801)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=810020833:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2957 on theBenchmark for (2957ds/114Mi)
% 24.29/7.31 % (2432798)Instruction limit reached!
% 24.29/7.31 % (2432798)------------------------------
% 24.29/7.31 % (2432798)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.29/7.31 % (2432798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.29/7.31 % (2432798)CaDiCaL version: 2.1.3
% 24.29/7.31 % (2432798)Termination reason: Instruction limit
% 24.29/7.31 % (2432798)Termination phase: SInE selection
% 24.29/7.31 % (2432798)Time elapsed: 0.092 s
% 24.29/7.31 % (2432798)Peak memory usage: 163 MB
% 24.29/7.31 % (2432798)Instructions burned: 113 (million)
% 24.29/7.31 % (2432801)Instruction limit reached!
% 24.29/7.31 % (2432801)------------------------------
% 24.29/7.31 % (2432801)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.29/7.31 % (2432801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.29/7.31 % (2432801)CaDiCaL version: 2.1.3
% 35.75/8.99 % (2432801)Termination reason: Instruction limit
% 35.75/8.99 % (2432801)Termination phase: Property scanning
% 35.75/8.99 % (2432801)Time elapsed: 0.031 s
% 35.75/8.99 % (2432801)Peak memory usage: 164 MB
% 35.75/8.99 % (2432801)Instructions burned: 118 (million)
% 35.75/8.99 % (2432800)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1430612083:i=127:av=off:fsr=off:sup=off_2957 on theBenchmark for (2957ds/127Mi)
% 35.75/8.99 % (2432800)Instruction limit reached!
% 35.75/8.99 % (2432800)------------------------------
% 35.75/8.99 % (2432800)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.75/8.99 % (2432800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.75/8.99 % (2432800)CaDiCaL version: 2.1.3
% 35.75/8.99 % (2432800)Termination reason: Instruction limit
% 35.75/8.99 % (2432800)Termination phase: Preprocessing 1
% 35.75/8.99 % (2432800)Time elapsed: 0.102 s
% 35.75/8.99 % (2432800)Peak memory usage: 165 MB
% 35.75/8.99 % (2432800)Instructions burned: 127 (million)
% 35.75/8.99 % (2432806)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1531578047:i=437:sd=1:aac=none:ss=included_2956 on theBenchmark for (2956ds/437Mi)
% 35.75/8.99 % (2432805)lrs+10_1_sil=8000:sp=occurrence:random_seed=3175145481:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2956 on theBenchmark for (2956ds/907Mi)
% 35.75/8.99 % (2432807)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=106268991:i=5202:ss=axioms:sgt=16_2954 on theBenchmark for (2954ds/5202Mi)
% 35.75/8.99 % (2432806)Instruction limit reached!
% 35.75/8.99 % (2432806)------------------------------
% 35.75/8.99 % (2432806)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.75/8.99 % (2432806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.75/8.99 % (2432806)CaDiCaL version: 2.1.3
% 35.75/8.99 % (2432806)Termination reason: Instruction limit
% 35.75/8.99 % (2432806)Termination phase: Saturation
% 35.75/8.99 % (2432806)Time elapsed: 0.196 s
% 35.75/8.99 % (2432806)Peak memory usage: 170 MB
% 35.75/8.99 % (2432806)Instructions burned: 438 (million)
% 35.75/8.99 % (2432811)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2327268838:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2952 on theBenchmark for (2952ds/134Mi)
% 35.75/8.99 % (2432811)Instruction limit reached!
% 35.75/8.99 % (2432811)------------------------------
% 35.75/8.99 % (2432811)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.75/8.99 % (2432811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.75/8.99 % (2432811)CaDiCaL version: 2.1.3
% 35.75/8.99 % (2432811)Termination reason: Instruction limit
% 35.75/8.99 % (2432811)Termination phase: SInE selection
% 35.75/8.99 % (2432811)Time elapsed: 0.063 s
% 35.75/8.99 % (2432811)Peak memory usage: 163 MB
% 35.75/8.99 % (2432811)Instructions burned: 135 (million)
% 35.75/8.99 % (2432813)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1914479330:st=8:i=592:sd=3:ep=RST:ss=axioms_2950 on theBenchmark for (2950ds/592Mi)
% 35.75/8.99 % (2432805)Instruction limit reached!
% 35.75/8.99 % (2432805)------------------------------
% 35.75/8.99 % (2432805)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.75/8.99 % (2432805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.75/8.99 % (2432805)CaDiCaL version: 2.1.3
% 35.75/8.99 % (2432805)Termination reason: Instruction limit
% 35.75/8.99 % (2432805)Termination phase: Property scanning
% 35.75/8.99 % (2432805)Time elapsed: 0.645 s
% 35.75/8.99 % (2432805)Peak memory usage: 178 MB
% 35.75/8.99 % (2432805)Instructions burned: 908 (million)
% 35.75/8.99 % (2432813)Instruction limit reached!
% 35.75/8.99 % (2432813)------------------------------
% 35.75/8.99 % (2432813)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.75/8.99 % (2432813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.75/8.99 % (2432813)CaDiCaL version: 2.1.3
% 35.75/8.99 % (2432813)Termination reason: Instruction limit
% 35.75/8.99 % (2432813)Termination phase: Preprocessing 1
% 35.75/8.99 % (2432813)Time elapsed: 0.247 s
% 35.75/8.99 % (2432813)Peak memory usage: 167 MB
% 35.75/8.99 % (2432813)Instructions burned: 593 (million)
% 35.75/8.99 % (2432815)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3426395205:st=3:i=13193:sd=3:ss=axioms_2947 on theBenchmark for (2947ds/13193Mi)
% 35.75/8.99 % (2432816)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=4273751419:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2946 on theBenchmark for (2946ds/125Mi)
% 35.75/8.99 % (2432816)Instruction limit reached!
% 35.75/8.99 % (2432816)------------------------------
% 35.75/8.99 % (2432816)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.75/8.99 % (2432816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.75/8.99 % (2432816)CaDiCaL version: 2.1.3
% 35.75/8.99 % (2432816)Termination reason: Instruction limit
% 35.75/8.99 % (2432816)Termination phase: Property scanning
% 35.75/8.99 % (2432816)Time elapsed: 0.033 s
% 35.75/8.99 % (2432816)Peak memory usage: 164 MB
% 35.75/8.99 % (2432816)Instructions burned: 126 (million)
% 35.75/8.99 % (2432819)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1286806233:i=134:gtgl=5:slsql=off:gtg=exists_sym_2945 on theBenchmark for (2945ds/134Mi)
% 35.75/8.99 % (2432819)Instruction limit reached!
% 35.75/8.99 % (2432819)------------------------------
% 35.75/8.99 % (2432819)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.75/8.99 % (2432819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.75/8.99 % (2432819)CaDiCaL version: 2.1.3
% 35.75/8.99 % (2432819)Termination reason: Instruction limit
% 35.75/8.99 % (2432819)Termination phase: Property scanning
% 35.75/8.99 % (2432819)Time elapsed: 0.034 s
% 35.75/8.99 % (2432819)Peak memory usage: 164 MB
% 35.75/8.99 % (2432819)Instructions burned: 137 (million)
% 35.75/8.99 % (2432821)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2206267635:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2943 on theBenchmark for (2943ds/141Mi)
% 35.75/8.99 % (2432821)Instruction limit reached!
% 35.75/8.99 % (2432821)------------------------------
% 35.75/8.99 % (2432821)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.75/8.99 % (2432821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.75/8.99 % (2432821)CaDiCaL version: 2.1.3
% 35.75/8.99 % (2432821)Termination reason: Instruction limit
% 35.75/8.99 % (2432821)Termination phase: SInE selection
% 35.75/8.99 % (2432821)Time elapsed: 0.067 s
% 35.75/8.99 % (2432821)Peak memory usage: 163 MB
% 35.75/8.99 % (2432821)Instructions burned: 141 (million)
% 35.75/8.99 % (2432796)Instruction limit reached!
% 35.75/8.99 % (2432796)------------------------------
% 35.75/8.99 % (2432796)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.75/8.99 % (2432796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.75/8.99 % (2432796)CaDiCaL version: 2.1.3
% 35.75/8.99 % (2432796)Termination reason: Instruction limit
% 35.75/8.99 % (2432796)Termination phase: Preprocessing 3
% 35.75/8.99 % (2432796)Time elapsed: 1.688 s
% 35.75/8.99 % (2432796)Peak memory usage: 264 MB
% 35.75/8.99 % (2432796)Instructions burned: 2350 (million)
% 35.75/8.99 % (2432823)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=31677667:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2941 on theBenchmark for (2941ds/431Mi)
% 35.75/8.99 % (2432824)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=4093200108:i=6060:aac=none:ins=25_2940 on theBenchmark for (2940ds/6060Mi)
% 35.75/8.99 % (2432823)Instruction limit reached!
% 35.75/8.99 % (2432823)------------------------------
% 35.75/8.99 % (2432823)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.75/8.99 % (2432823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.75/8.99 % (2432823)CaDiCaL version: 2.1.3
% 35.75/8.99 % (2432823)Termination reason: Instruction limit
% 35.75/8.99 % (2432823)Termination phase: Saturation
% 35.75/8.99 % (2432823)Time elapsed: 0.214 s
% 35.75/8.99 % (2432823)Peak memory usage: 170 MB
% 35.75/8.99 % (2432823)Instructions burned: 433 (million)
% 35.75/8.99 % (2432827)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=898365049:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2937 on theBenchmark for (2937ds/150Mi)
% 35.75/8.99 % (2432827)Instruction limit reached!
% 35.75/8.99 % (2432827)------------------------------
% 35.75/8.99 % (2432827)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.75/8.99 % (2432827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.75/8.99 % (2432827)CaDiCaL version: 2.1.3
% 35.75/8.99 % (2432827)Termination reason: Instruction limit
% 35.75/8.99 % (2432827)Termination phase: SInE selection
% 35.75/8.99 % (2432827)Time elapsed: 0.071 s
% 35.75/8.99 % (2432827)Peak memory usage: 163 MB
% 35.75/8.99 % (2432827)Instructions burned: 152 (million)
% 35.75/8.99 % (2432829)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3495573689:i=14155:bd=all_2935 on theBenchmark for (2935ds/14155Mi)
% 35.75/8.99 % (2432774)First to succeed.
% 35.75/8.99 % (2432774)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2432768"
% 35.75/8.99 % (2432807)Instruction limit reached!
% 35.75/8.99 % (2432807)------------------------------
% 35.75/8.99 % (2432807)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.75/8.99 % (2432807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.75/8.99 % (2432807)CaDiCaL version: 2.1.3
% 35.75/8.99 % (2432807)Termination reason: Instruction limit
% 35.75/8.99 % (2432807)Termination phase: Saturation
% 35.75/8.99 % (2432807)Time elapsed: 3.247 s
% 35.75/8.99 % (2432807)Peak memory usage: 319 MB
% 35.75/8.99 % (2432807)Instructions burned: 5204 (million)
% 35.75/8.99 % (2432774)Refutation found. Thanks to Tanya!
% 35.75/8.99 % SZS status Theorem for theBenchmark
% 35.75/8.99 % SZS output start Proof for theBenchmark
% See solution above
% 36.61/9.26 % (2432774)------------------------------
% 36.61/9.26 % (2432774)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.61/9.26 % (2432774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.61/9.26 % (2432774)CaDiCaL version: 2.1.3
% 36.61/9.26 % (2432774)Termination reason: Refutation
% 36.61/9.26 % (2432774)Time elapsed: 4.081 s
% 36.61/9.26 % (2432774)Peak memory usage: 301 MB
% 36.61/9.26 % (2432774)Instructions burned: 6689 (million)
% 36.61/9.26 % (2432774)------------------------------
% 36.61/9.26 % (2432774)------------------------------
% 36.61/9.26 % (2432768)Success in time 8.133 s
% 36.61/9.26 % Vampire exiting
%------------------------------------------------------------------------------