%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT338+3 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n016.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 5.67s 2.64s
% Output : Refutation 7.06s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 15
% Syntax : Number of formulae : 129 ( 14 unt; 8 def)
% Number of atoms : 444 ( 6 equ)
% Maximal formula atoms : 11 ( 3 avg)
% Number of connectives : 509 ( 194 ~; 201 |; 88 &)
% ( 8 <=>; 18 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 27 ( 25 usr; 9 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 2 con; 0-2 aty)
% Number of variables : 73 ( 0 sgn 69 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f11649,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& l3_lattices(X0) )
=> m1_subset_1(k15_lattice3(X0,X1),u1_struct_0(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k15_lattice3) ).
fof(f11650,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& l3_lattices(X0) )
=> m1_subset_1(k16_lattice3(X0,X1),u1_struct_0(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k16_lattice3) ).
fof(f17832,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/sandbox2/benchmark/theBenchmark.p',fc4_conlat_1) ).
fof(f17897,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/sandbox2/benchmark/theBenchmark.p',t46_conlat_1) ).
fof(f17898,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/sandbox2/benchmark/theBenchmark.p',d24_conlat_1) ).
fof(f17930,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/sandbox2/benchmark/theBenchmark.p',dt_k12_conlat_1) ).
fof(f18297,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/sandbox2/benchmark/theBenchmark.p',t4_conlat_2) ).
fof(f18298,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)],[f18297]) ).
fof(f18311,plain,
! [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))
& v10_lattices(k11_conlat_1(X0)) ) ),
inference(pure_predicate_removal,[],[f17832]) ).
fof(f18315,plain,
! [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))
& v10_lattices(k11_conlat_1(X0)) ) ),
inference(pure_predicate_removal,[],[f18311]) ).
fof(f18318,plain,
! [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))
& v10_lattices(k11_conlat_1(X0)) ) ),
inference(pure_predicate_removal,[],[f18315]) ).
fof(f18320,plain,
! [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))
& v10_lattices(k11_conlat_1(X0)) ) ),
inference(pure_predicate_removal,[],[f18318]) ).
fof(f18325,plain,
! [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))
& v10_lattices(k11_conlat_1(X0)) ) ),
inference(pure_predicate_removal,[],[f18320]) ).
fof(f18328,plain,
! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0) )
=> ( ~ v3_struct_0(k11_conlat_1(X0))
& v3_lattices(k11_conlat_1(X0))
& v10_lattices(k11_conlat_1(X0)) ) ),
inference(pure_predicate_removal,[],[f18325]) ).
fof(f18329,plain,
! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0) )
=> ( ~ v3_struct_0(k11_conlat_1(X0))
& v10_lattices(k11_conlat_1(X0)) ) ),
inference(pure_predicate_removal,[],[f18328]) ).
fof(f18343,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,[],[f18298]) ).
fof(f18344,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,[],[f18343]) ).
fof(f18347,plain,
! [X0,X1] :
( m1_subset_1(k15_lattice3(X0,X1),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f11649]) ).
fof(f18348,plain,
! [X0,X1] :
( m1_subset_1(k15_lattice3(X0,X1),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f18347]) ).
fof(f18377,plain,
! [X0,X1] :
( m1_subset_1(k16_lattice3(X0,X1),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f11650]) ).
fof(f18378,plain,
! [X0,X1] :
( m1_subset_1(k16_lattice3(X0,X1),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f18377]) ).
fof(f18401,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,[],[f17930]) ).
fof(f18402,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,[],[f18401]) ).
fof(f18409,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,[],[f17898]) ).
fof(f18410,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,[],[f18409]) ).
fof(f18411,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,[],[f17897]) ).
fof(f18412,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,[],[f18411]) ).
fof(f18417,plain,
! [X0] :
( ( ~ v3_struct_0(k11_conlat_1(X0))
& v10_lattices(k11_conlat_1(X0)) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(ennf_transformation,[],[f18329]) ).
fof(f18418,plain,
! [X0] :
( ( ~ v3_struct_0(k11_conlat_1(X0))
& v10_lattices(k11_conlat_1(X0)) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(flattening,[],[f18417]) ).
fof(f18419,plain,
( ( v7_conlat_1(k16_lattice3(k11_conlat_1(sK0),sK1),sK0)
| ~ v9_conlat_1(k16_lattice3(k11_conlat_1(sK0),sK1),sK0)
| ~ l3_conlat_1(k16_lattice3(k11_conlat_1(sK0),sK1),sK0)
| v7_conlat_1(k15_lattice3(k11_conlat_1(sK0),sK1),sK0)
| ~ v9_conlat_1(k15_lattice3(k11_conlat_1(sK0),sK1),sK0)
| ~ l3_conlat_1(k15_lattice3(k11_conlat_1(sK0),sK1),sK0) )
& m1_subset_1(sK1,k1_zfmisc_1(u1_struct_0(k11_conlat_1(sK0))))
& ~ v3_conlat_1(sK0)
& l2_conlat_1(sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(X0,sK0),skolemize(X1,sK1)],[f18344]) ).
fof(f18438,plain,
l2_conlat_1(sK0),
inference(cnf_transformation,[],[f18419]) ).
fof(f18439,plain,
~ v3_conlat_1(sK0),
inference(cnf_transformation,[],[f18419]) ).
fof(f18441,plain,
( v7_conlat_1(k16_lattice3(k11_conlat_1(sK0),sK1),sK0)
| ~ v9_conlat_1(k16_lattice3(k11_conlat_1(sK0),sK1),sK0)
| ~ l3_conlat_1(k16_lattice3(k11_conlat_1(sK0),sK1),sK0)
| v7_conlat_1(k15_lattice3(k11_conlat_1(sK0),sK1),sK0)
| ~ v9_conlat_1(k15_lattice3(k11_conlat_1(sK0),sK1),sK0)
| ~ l3_conlat_1(k15_lattice3(k11_conlat_1(sK0),sK1),sK0) ),
inference(cnf_transformation,[],[f18419]) ).
fof(f18447,plain,
! [X0,X1] :
( m1_subset_1(k15_lattice3(X0,X1),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f18348]) ).
fof(f18481,plain,
! [X0,X1] :
( m1_subset_1(k16_lattice3(X0,X1),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f18378]) ).
fof(f18507,plain,
! [X0,X1] :
( 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(cnf_transformation,[],[f18402]) ).
fof(f18508,plain,
! [X0,X1] :
( v9_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(cnf_transformation,[],[f18402]) ).
fof(f18509,plain,
! [X0,X1] :
( ~ v7_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(cnf_transformation,[],[f18402]) ).
fof(f18519,plain,
! [X0,X1] :
( v3_conlat_1(X0)
| ~ m1_subset_1(X1,u1_struct_0(k11_conlat_1(X0)))
| k12_conlat_1(X0,X1) = X1
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f18410]) ).
fof(f18520,plain,
! [X0] :
( l3_lattices(k11_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f18412]) ).
fof(f18528,plain,
! [X0] :
( ~ v3_struct_0(k11_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f18418]) ).
fof(f18532,definition,
( spl12_1
<=> l3_conlat_1(k15_lattice3(k11_conlat_1(sK0),sK1),sK0) ),
introduced(definition,[new_symbols(definition,[spl12_1])],[avatar_definition]) ).
fof(f18534,plain,
( ~ l3_conlat_1(k15_lattice3(k11_conlat_1(sK0),sK1),sK0)
| spl12_1 ),
inference(avatar_component_clause,[],[f18532]) ).
fof(f18536,definition,
( spl12_2
<=> v9_conlat_1(k15_lattice3(k11_conlat_1(sK0),sK1),sK0) ),
introduced(definition,[new_symbols(definition,[spl12_2])],[avatar_definition]) ).
fof(f18538,plain,
( ~ v9_conlat_1(k15_lattice3(k11_conlat_1(sK0),sK1),sK0)
| spl12_2 ),
inference(avatar_component_clause,[],[f18536]) ).
fof(f18540,definition,
( spl12_3
<=> v7_conlat_1(k15_lattice3(k11_conlat_1(sK0),sK1),sK0) ),
introduced(definition,[new_symbols(definition,[spl12_3])],[avatar_definition]) ).
fof(f18542,plain,
( v7_conlat_1(k15_lattice3(k11_conlat_1(sK0),sK1),sK0)
| ~ spl12_3 ),
inference(avatar_component_clause,[],[f18540]) ).
fof(f18544,definition,
( spl12_4
<=> l3_conlat_1(k16_lattice3(k11_conlat_1(sK0),sK1),sK0) ),
introduced(definition,[new_symbols(definition,[spl12_4])],[avatar_definition]) ).
fof(f18546,plain,
( ~ l3_conlat_1(k16_lattice3(k11_conlat_1(sK0),sK1),sK0)
| spl12_4 ),
inference(avatar_component_clause,[],[f18544]) ).
fof(f18548,definition,
( spl12_5
<=> v9_conlat_1(k16_lattice3(k11_conlat_1(sK0),sK1),sK0) ),
introduced(definition,[new_symbols(definition,[spl12_5])],[avatar_definition]) ).
fof(f18550,plain,
( ~ v9_conlat_1(k16_lattice3(k11_conlat_1(sK0),sK1),sK0)
| spl12_5 ),
inference(avatar_component_clause,[],[f18548]) ).
fof(f18552,definition,
( spl12_6
<=> v7_conlat_1(k16_lattice3(k11_conlat_1(sK0),sK1),sK0) ),
introduced(definition,[new_symbols(definition,[spl12_6])],[avatar_definition]) ).
fof(f18554,plain,
( v7_conlat_1(k16_lattice3(k11_conlat_1(sK0),sK1),sK0)
| ~ spl12_6 ),
inference(avatar_component_clause,[],[f18552]) ).
fof(f18555,plain,
( ~ spl12_1
| ~ spl12_2
| spl12_3
| ~ spl12_4
| ~ spl12_5
| spl12_6 ),
inference(avatar_split_clause,[],[f18441,f18552,f18548,f18544,f18540,f18536,f18532]) ).
fof(f18566,definition,
( spl12_7
<=> l3_lattices(k11_conlat_1(sK0)) ),
introduced(definition,[new_symbols(definition,[spl12_7])],[avatar_definition]) ).
fof(f18567,plain,
( l3_lattices(k11_conlat_1(sK0))
| ~ spl12_7 ),
inference(avatar_component_clause,[],[f18566]) ).
fof(f18568,plain,
( ~ l3_lattices(k11_conlat_1(sK0))
| spl12_7 ),
inference(avatar_component_clause,[],[f18566]) ).
fof(f18570,definition,
( spl12_8
<=> v3_struct_0(k11_conlat_1(sK0)) ),
introduced(definition,[new_symbols(definition,[spl12_8])],[avatar_definition]) ).
fof(f18571,plain,
( ~ v3_struct_0(k11_conlat_1(sK0))
| spl12_8 ),
inference(avatar_component_clause,[],[f18570]) ).
fof(f18572,plain,
( v3_struct_0(k11_conlat_1(sK0))
| ~ spl12_8 ),
inference(avatar_component_clause,[],[f18570]) ).
fof(f18578,plain,
( v3_conlat_1(sK0)
| ~ l2_conlat_1(sK0)
| spl12_7 ),
inference(resolution,[],[f18568,f18520]) ).
fof(f18579,plain,
( ~ l2_conlat_1(sK0)
| spl12_7 ),
inference(forward_subsumption_resolution,[],[f18578,f18439]) ).
fof(f18580,plain,
( $false
| spl12_7 ),
inference(forward_subsumption_resolution,[],[f18579,f18438]) ).
fof(f18581,plain,
spl12_7,
inference(avatar_contradiction_clause,[],[f18580]) ).
fof(f18583,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK0)))
| k12_conlat_1(sK0,X0) = X0
| ~ l2_conlat_1(sK0) ),
inference(resolution,[],[f18519,f18439]) ).
fof(f18584,plain,
! [X0] :
( k12_conlat_1(sK0,X0) = X0
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK0))) ),
inference(forward_subsumption_resolution,[],[f18583,f18438]) ).
fof(f18585,plain,
( v3_conlat_1(sK0)
| ~ l2_conlat_1(sK0)
| ~ spl12_8 ),
inference(resolution,[],[f18572,f18528]) ).
fof(f18586,plain,
( ~ l2_conlat_1(sK0)
| ~ spl12_8 ),
inference(forward_subsumption_resolution,[],[f18585,f18439]) ).
fof(f18587,plain,
( $false
| ~ spl12_8 ),
inference(forward_subsumption_resolution,[],[f18586,f18438]) ).
fof(f18588,plain,
~ spl12_8,
inference(avatar_contradiction_clause,[],[f18587]) ).
fof(f18598,plain,
! [X0] :
( ~ v7_conlat_1(X0,sK0)
| v3_conlat_1(sK0)
| ~ l2_conlat_1(sK0)
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK0)))
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK0))) ),
inference(superposition,[],[f18509,f18584]) ).
fof(f18599,plain,
! [X0] :
( v9_conlat_1(X0,sK0)
| v3_conlat_1(sK0)
| ~ l2_conlat_1(sK0)
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK0)))
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK0))) ),
inference(superposition,[],[f18508,f18584]) ).
fof(f18600,plain,
! [X0] :
( l3_conlat_1(X0,sK0)
| v3_conlat_1(sK0)
| ~ l2_conlat_1(sK0)
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK0)))
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK0))) ),
inference(superposition,[],[f18507,f18584]) ).
fof(f18601,plain,
! [X0] :
( l3_conlat_1(X0,sK0)
| v3_conlat_1(sK0)
| ~ l2_conlat_1(sK0)
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK0))) ),
inference(duplicate_literal_removal,[],[f18600]) ).
fof(f18602,plain,
! [X0] :
( v9_conlat_1(X0,sK0)
| v3_conlat_1(sK0)
| ~ l2_conlat_1(sK0)
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK0))) ),
inference(duplicate_literal_removal,[],[f18599]) ).
fof(f18603,plain,
! [X0] :
( ~ v7_conlat_1(X0,sK0)
| v3_conlat_1(sK0)
| ~ l2_conlat_1(sK0)
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK0))) ),
inference(duplicate_literal_removal,[],[f18598]) ).
fof(f18605,plain,
! [X0] :
( l3_conlat_1(X0,sK0)
| ~ l2_conlat_1(sK0)
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK0))) ),
inference(forward_subsumption_resolution,[],[f18601,f18439]) ).
fof(f18606,plain,
! [X0] :
( v9_conlat_1(X0,sK0)
| ~ l2_conlat_1(sK0)
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK0))) ),
inference(forward_subsumption_resolution,[],[f18602,f18439]) ).
fof(f18607,plain,
! [X0] :
( ~ v7_conlat_1(X0,sK0)
| ~ l2_conlat_1(sK0)
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK0))) ),
inference(forward_subsumption_resolution,[],[f18603,f18439]) ).
fof(f18609,plain,
! [X0] :
( l3_conlat_1(X0,sK0)
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK0))) ),
inference(forward_subsumption_resolution,[],[f18605,f18438]) ).
fof(f18610,plain,
! [X0] :
( v9_conlat_1(X0,sK0)
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK0))) ),
inference(forward_subsumption_resolution,[],[f18606,f18438]) ).
fof(f18611,plain,
! [X0] :
( ~ v7_conlat_1(X0,sK0)
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK0))) ),
inference(forward_subsumption_resolution,[],[f18607,f18438]) ).
fof(f18613,plain,
( ~ m1_subset_1(k15_lattice3(k11_conlat_1(sK0),sK1),u1_struct_0(k11_conlat_1(sK0)))
| spl12_1 ),
inference(resolution,[],[f18609,f18534]) ).
fof(f18614,plain,
( v3_struct_0(k11_conlat_1(sK0))
| ~ l3_lattices(k11_conlat_1(sK0))
| spl12_1 ),
inference(resolution,[],[f18613,f18447]) ).
fof(f18615,plain,
( ~ l3_lattices(k11_conlat_1(sK0))
| spl12_1
| spl12_8 ),
inference(forward_subsumption_resolution,[],[f18614,f18571]) ).
fof(f18616,plain,
( $false
| spl12_1
| ~ spl12_7
| spl12_8 ),
inference(forward_subsumption_resolution,[],[f18615,f18567]) ).
fof(f18617,plain,
( spl12_1
| ~ spl12_7
| spl12_8 ),
inference(avatar_contradiction_clause,[],[f18616]) ).
fof(f18618,plain,
( ~ m1_subset_1(k15_lattice3(k11_conlat_1(sK0),sK1),u1_struct_0(k11_conlat_1(sK0)))
| spl12_2 ),
inference(resolution,[],[f18538,f18610]) ).
fof(f18619,plain,
( v3_struct_0(k11_conlat_1(sK0))
| ~ l3_lattices(k11_conlat_1(sK0))
| spl12_2 ),
inference(resolution,[],[f18618,f18447]) ).
fof(f18620,plain,
( ~ l3_lattices(k11_conlat_1(sK0))
| spl12_2
| spl12_8 ),
inference(forward_subsumption_resolution,[],[f18619,f18571]) ).
fof(f18621,plain,
( $false
| spl12_2
| ~ spl12_7
| spl12_8 ),
inference(forward_subsumption_resolution,[],[f18620,f18567]) ).
fof(f18622,plain,
( spl12_2
| ~ spl12_7
| spl12_8 ),
inference(avatar_contradiction_clause,[],[f18621]) ).
fof(f18623,plain,
( ~ m1_subset_1(k16_lattice3(k11_conlat_1(sK0),sK1),u1_struct_0(k11_conlat_1(sK0)))
| spl12_4 ),
inference(resolution,[],[f18546,f18609]) ).
fof(f18624,plain,
( v3_struct_0(k11_conlat_1(sK0))
| ~ l3_lattices(k11_conlat_1(sK0))
| spl12_4 ),
inference(resolution,[],[f18623,f18481]) ).
fof(f18625,plain,
( ~ l3_lattices(k11_conlat_1(sK0))
| spl12_4
| spl12_8 ),
inference(forward_subsumption_resolution,[],[f18624,f18571]) ).
fof(f18626,plain,
( $false
| spl12_4
| ~ spl12_7
| spl12_8 ),
inference(forward_subsumption_resolution,[],[f18625,f18567]) ).
fof(f18627,plain,
( spl12_4
| ~ spl12_7
| spl12_8 ),
inference(avatar_contradiction_clause,[],[f18626]) ).
fof(f18628,plain,
( ~ m1_subset_1(k16_lattice3(k11_conlat_1(sK0),sK1),u1_struct_0(k11_conlat_1(sK0)))
| spl12_5 ),
inference(resolution,[],[f18550,f18610]) ).
fof(f18633,plain,
( v3_struct_0(k11_conlat_1(sK0))
| ~ l3_lattices(k11_conlat_1(sK0))
| spl12_5 ),
inference(resolution,[],[f18628,f18481]) ).
fof(f18634,plain,
( ~ l3_lattices(k11_conlat_1(sK0))
| spl12_5
| spl12_8 ),
inference(forward_subsumption_resolution,[],[f18633,f18571]) ).
fof(f18635,plain,
( $false
| spl12_5
| ~ spl12_7
| spl12_8 ),
inference(forward_subsumption_resolution,[],[f18634,f18567]) ).
fof(f18636,plain,
( spl12_5
| ~ spl12_7
| spl12_8 ),
inference(avatar_contradiction_clause,[],[f18635]) ).
fof(f18637,plain,
( ~ m1_subset_1(k16_lattice3(k11_conlat_1(sK0),sK1),u1_struct_0(k11_conlat_1(sK0)))
| ~ spl12_6 ),
inference(resolution,[],[f18554,f18611]) ).
fof(f18642,plain,
( v3_struct_0(k11_conlat_1(sK0))
| ~ l3_lattices(k11_conlat_1(sK0))
| ~ spl12_6 ),
inference(resolution,[],[f18637,f18481]) ).
fof(f18643,plain,
( ~ l3_lattices(k11_conlat_1(sK0))
| ~ spl12_6
| spl12_8 ),
inference(forward_subsumption_resolution,[],[f18642,f18571]) ).
fof(f18644,plain,
( $false
| ~ spl12_6
| ~ spl12_7
| spl12_8 ),
inference(forward_subsumption_resolution,[],[f18643,f18567]) ).
fof(f18645,plain,
( ~ spl12_6
| ~ spl12_7
| spl12_8 ),
inference(avatar_contradiction_clause,[],[f18644]) ).
fof(f18646,plain,
( ~ m1_subset_1(k15_lattice3(k11_conlat_1(sK0),sK1),u1_struct_0(k11_conlat_1(sK0)))
| ~ spl12_3 ),
inference(resolution,[],[f18542,f18611]) ).
fof(f18651,plain,
( v3_struct_0(k11_conlat_1(sK0))
| ~ l3_lattices(k11_conlat_1(sK0))
| ~ spl12_3 ),
inference(resolution,[],[f18646,f18447]) ).
fof(f18652,plain,
( ~ l3_lattices(k11_conlat_1(sK0))
| ~ spl12_3
| spl12_8 ),
inference(forward_subsumption_resolution,[],[f18651,f18571]) ).
fof(f18653,plain,
( $false
| ~ spl12_3
| ~ spl12_7
| spl12_8 ),
inference(forward_subsumption_resolution,[],[f18652,f18567]) ).
fof(f18654,plain,
( ~ spl12_3
| ~ spl12_7
| spl12_8 ),
inference(avatar_contradiction_clause,[],[f18653]) ).
cnf(s1,plain,
( ~ spl12_1
| ~ spl12_2
| spl12_3
| ~ spl12_4
| ~ spl12_5
| spl12_6 ),
inference(sat_conversion,[],[f18555]) ).
cnf(s3,plain,
spl12_7,
inference(sat_conversion,[],[f18581]) ).
cnf(s4,plain,
~ spl12_8,
inference(sat_conversion,[],[f18588]) ).
cnf(s5,plain,
( spl12_1
| ~ spl12_7
| spl12_8 ),
inference(sat_conversion,[],[f18617]) ).
cnf(s6,plain,
( spl12_2
| ~ spl12_7
| spl12_8 ),
inference(sat_conversion,[],[f18622]) ).
cnf(s7,plain,
( spl12_4
| ~ spl12_7
| spl12_8 ),
inference(sat_conversion,[],[f18627]) ).
cnf(s8,plain,
( spl12_5
| ~ spl12_7
| spl12_8 ),
inference(sat_conversion,[],[f18636]) ).
cnf(s9,plain,
( ~ spl12_6
| ~ spl12_7
| spl12_8 ),
inference(sat_conversion,[],[f18645]) ).
cnf(s10,plain,
( ~ spl12_3
| ~ spl12_7
| spl12_8 ),
inference(sat_conversion,[],[f18654]) ).
cnf(s11,plain,
~ spl12_3,
inference(rat,[],[s10,s4,s3]) ).
cnf(s12,plain,
~ spl12_6,
inference(rat,[],[s9,s4,s3]) ).
cnf(s13,plain,
spl12_5,
inference(rat,[],[s8,s4,s3]) ).
cnf(s14,plain,
spl12_4,
inference(rat,[],[s7,s4,s3]) ).
cnf(s15,plain,
spl12_2,
inference(rat,[],[s6,s4,s3]) ).
cnf(s16,plain,
spl12_1,
inference(rat,[],[s5,s4,s3]) ).
cnf(s18,plain,
$false,
inference(rat,[],[s1,s12,s13,s14,s11,s15,s16]) ).
fof(f18655,plain,
$false,
inference(avatar_sat_refutation,[],[s18]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT338+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.37 % Computer : n016.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sun Sep 27 14:52:20 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.40 Running first-order theorem proving
% 0.11/0.40 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.67/2.64 % (2720949)Detected formulas, will run a generic FOF schedule.
% 5.67/2.64 % (2720957)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1505706926:i=109:sd=1:ins=1:gsp=on:ss=axioms_2989 on theBenchmark for (2989ds/109Mi)
% 5.67/2.64 % (2720958)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=513816874:i=119:av=off:ss=axioms_2989 on theBenchmark for (2989ds/119Mi)
% 5.67/2.64 % (2720954)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=1662152346:i=141193_2989 on theBenchmark for (2989ds/141193Mi)
% 5.67/2.64 % (2720959)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3566928443:s2a=on:i=139:gtg=position_2989 on theBenchmark for (2989ds/139Mi)
% 5.67/2.64 % (2720960)dis-21_1_sil=8000:lcm=predicate:random_seed=3568514707:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2989 on theBenchmark for (2989ds/129Mi)
% 5.67/2.64 % (2720956)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=406820818:i=141695:sd=1:nm=32:gsp=on:ss=included_2989 on theBenchmark for (2989ds/141695Mi)
% 5.67/2.64 % (2720955)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=2737405371:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2989 on theBenchmark for (2989ds/134677Mi)
% 5.67/2.64 % (2720957)Instruction limit reached!
% 5.67/2.64 % (2720957)------------------------------
% 5.67/2.64 % (2720957)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.67/2.64 % (2720957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.67/2.64 % (2720957)CaDiCaL version: 2.1.3
% 5.67/2.64 % (2720957)Termination reason: Instruction limit
% 5.67/2.64 % (2720957)Termination phase: Property scanning
% 5.67/2.64 % (2720957)Time elapsed: 0.054 s
% 5.67/2.64 % (2720957)Peak memory usage: 113 MB
% 5.67/2.64 % (2720957)Instructions burned: 109 (million)
% 5.67/2.64 % (2720959)Instruction limit reached!
% 5.67/2.64 % (2720959)------------------------------
% 5.67/2.64 % (2720959)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.67/2.64 % (2720959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.67/2.64 % (2720959)CaDiCaL version: 2.1.3
% 5.67/2.64 % (2720959)Termination reason: Instruction limit
% 5.67/2.64 % (2720959)Termination phase: Property scanning
% 5.67/2.64 % (2720959)Time elapsed: 0.061 s
% 5.67/2.64 % (2720959)Peak memory usage: 110 MB
% 5.67/2.64 % (2720959)Instructions burned: 139 (million)
% 5.67/2.64 % (2720960)Instruction limit reached!
% 5.67/2.64 % (2720960)------------------------------
% 5.67/2.64 % (2720960)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.67/2.64 % (2720960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.67/2.64 % (2720960)CaDiCaL version: 2.1.3
% 5.67/2.64 % (2720960)Termination reason: Instruction limit
% 5.67/2.64 % (2720960)Termination phase: SInE selection
% 5.67/2.64 % (2720960)Time elapsed: 0.085 s
% 5.67/2.64 % (2720960)Peak memory usage: 111 MB
% 5.67/2.64 % (2720960)Instructions burned: 130 (million)
% 5.67/2.64 % (2720958)Instruction limit reached!
% 5.67/2.64 % (2720958)------------------------------
% 5.67/2.64 % (2720958)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.67/2.64 % (2720958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.67/2.64 % (2720958)CaDiCaL version: 2.1.3
% 5.67/2.64 % (2720958)Termination reason: Instruction limit
% 5.67/2.64 % (2720958)Termination phase: Preprocessing 1
% 5.67/2.64 % (2720958)Time elapsed: 0.101 s
% 5.67/2.64 % (2720958)Peak memory usage: 111 MB
% 5.67/2.64 % (2720958)Instructions burned: 119 (million)
% 5.67/2.64 % (2720968)lrs+10_1_sil=8000:sp=occurrence:random_seed=4075976974:i=285:sd=3:ss=axioms:sgt=8_2988 on theBenchmark for (2988ds/285Mi)
% 5.67/2.64 % (2720969)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2369857951:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2987 on theBenchmark for (2987ds/157Mi)
% 5.67/2.64 % (2720970)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1555021397:i=325:sd=1:ss=axioms:sgt=32_2987 on theBenchmark for (2987ds/325Mi)
% 5.67/2.64 % (2720968)Instruction limit reached!
% 5.67/2.64 % (2720968)------------------------------
% 5.67/2.64 % (2720968)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.67/2.64 % (2720968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.67/2.64 % (2720968)CaDiCaL version: 2.1.3
% 5.67/2.64 % (2720968)Termination reason: Instruction limit
% 5.67/2.64 % (2720968)Termination phase: Saturation
% 5.67/2.64 % (2720968)Time elapsed: 0.117 s
% 5.67/2.64 % (2720968)Peak memory usage: 118 MB
% 5.67/2.64 % (2720968)Instructions burned: 285 (million)
% 5.67/2.64 % (2720971)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=1844907027:s2a=on:i=248:s2at=1.23:gtg=position_2987 on theBenchmark for (2987ds/248Mi)
% 5.67/2.64 % (2720969)Instruction limit reached!
% 5.67/2.64 % (2720969)------------------------------
% 5.67/2.64 % (2720969)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.67/2.64 % (2720969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.67/2.64 % (2720969)CaDiCaL version: 2.1.3
% 5.67/2.64 % (2720969)Termination reason: Instruction limit
% 5.67/2.64 % (2720969)Termination phase: Property scanning
% 5.67/2.64 % (2720969)Time elapsed: 0.068 s
% 5.67/2.64 % (2720969)Peak memory usage: 111 MB
% 5.67/2.64 % (2720969)Instructions burned: 158 (million)
% 5.67/2.64 % (2720970)First to succeed.
% 5.67/2.64 % (2720970)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2720949"
% 5.67/2.64 % (2720971)Instruction limit reached!
% 5.67/2.64 % (2720971)------------------------------
% 5.67/2.64 % (2720971)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.67/2.64 % (2720971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.67/2.64 % (2720971)CaDiCaL version: 2.1.3
% 5.67/2.64 % (2720971)Termination reason: Instruction limit
% 5.67/2.64 % (2720971)Termination phase: Property scanning
% 5.67/2.64 % (2720971)Time elapsed: 0.108 s
% 5.67/2.64 % (2720971)Peak memory usage: 111 MB
% 5.67/2.64 % (2720971)Instructions burned: 251 (million)
% 5.67/2.64 % (2720975)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=98044169:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2985 on theBenchmark for (2985ds/294Mi)
% 5.67/2.64 % (2720977)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1506215046:i=2350_2985 on theBenchmark for (2985ds/2350Mi)
% 5.67/2.64 % (2720975)Instruction limit reached!
% 5.67/2.64 % (2720975)------------------------------
% 5.67/2.64 % (2720975)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.67/2.64 % (2720975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.67/2.64 % (2720975)CaDiCaL version: 2.1.3
% 5.67/2.64 % (2720975)Termination reason: Instruction limit
% 5.67/2.64 % (2720975)Termination phase: Saturation
% 5.67/2.64 % (2720975)Time elapsed: 0.112 s
% 5.67/2.64 % (2720975)Peak memory usage: 118 MB
% 5.67/2.64 % (2720975)Instructions burned: 298 (million)
% 5.67/2.64 % (2720979)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1167059455:cts=off:i=113:fsr=off:ss=included:sgt=4_2984 on theBenchmark for (2984ds/113Mi)
% 5.67/2.64 % (2720970)Refutation found. Thanks to Tanya!
% 5.67/2.64 % SZS status Theorem for theBenchmark
% 5.67/2.64 % SZS output start Proof for theBenchmark
% See solution above
% 7.06/2.74 % (2720970)------------------------------
% 7.06/2.74 % (2720970)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.06/2.74 % (2720970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.06/2.74 % (2720970)CaDiCaL version: 2.1.3
% 7.06/2.74 % (2720970)Termination reason: Refutation
% 7.06/2.74 % (2720970)Time elapsed: 0.108 s
% 7.06/2.74 % (2720970)Peak memory usage: 117 MB
% 7.06/2.74 % (2720970)Instructions burned: 125 (million)
% 7.06/2.74 % (2720970)------------------------------
% 7.06/2.74 % (2720970)------------------------------
% 7.06/2.74 % (2720949)Success in time 1.799 s
% 7.06/2.74 % Vampire exiting
%------------------------------------------------------------------------------