%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LAT327+2 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n011.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:48:26 AM UTC 2026
% Result : Theorem 165.17s 33.60s
% Output : Refutation 165.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 8
% Syntax : Number of formulae : 84 ( 17 unt; 4 def)
% Number of atoms : 354 ( 0 equ)
% Maximal formula atoms : 10 ( 4 avg)
% Number of connectives : 380 ( 110 ~; 208 |; 33 &)
% ( 10 <=>; 19 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 11 ( 10 usr; 5 prp; 0-3 aty)
% Number of functors : 7 ( 7 usr; 3 con; 0-3 aty)
% Number of variables : 81 ( 0 sgn 75 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2955,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,X2))
<=> r3_lattices(X0,X1,X2) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t29_filter_2) ).
fof(f2957,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ( r2_hidden(X1,k18_filter_2(X0,X1))
& r2_hidden(k4_lattices(X0,X1,X2),k18_filter_2(X0,X1))
& r2_hidden(k4_lattices(X0,X2,X1),k18_filter_2(X0,X1)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t31_filter_2) ).
fof(f2999,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))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
=> ( r3_lattices(X0,X1,X2)
=> ( r2_hidden(X3,k22_filter_2(X0,X1,X2))
<=> ( r3_lattices(X0,X1,X3)
& r3_lattices(X0,X3,X2) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t63_filter_2) ).
fof(f3000,conjecture,
! [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))
=> ( r3_lattices(X0,X1,X2)
=> ( r2_hidden(X1,k22_filter_2(X0,X1,X2))
& r2_hidden(X2,k22_filter_2(X0,X1,X2)) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t64_filter_2) ).
fof(f3001,negated_conjecture,
~ ! [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))
=> ( r3_lattices(X0,X1,X2)
=> ( r2_hidden(X1,k22_filter_2(X0,X1,X2))
& r2_hidden(X2,k22_filter_2(X0,X1,X2)) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f3000]) ).
fof(f6246,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( r2_hidden(X1,k18_filter_2(X0,X2))
<=> r3_lattices(X0,X1,X2) )
| ~ 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,[],[f2955]) ).
fof(f6247,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( r2_hidden(X1,k18_filter_2(X0,X2))
<=> r3_lattices(X0,X1,X2) )
| ~ 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,[],[f6246]) ).
fof(f6250,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,[],[f2957]) ).
fof(f6251,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,[],[f6250]) ).
fof(f6334,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( r2_hidden(X3,k22_filter_2(X0,X1,X2))
<=> ( r3_lattices(X0,X1,X3)
& r3_lattices(X0,X3,X2) ) )
| ~ r3_lattices(X0,X1,X2)
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ 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,[],[f2999]) ).
fof(f6335,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( r2_hidden(X3,k22_filter_2(X0,X1,X2))
<=> ( r3_lattices(X0,X1,X3)
& r3_lattices(X0,X3,X2) ) )
| ~ r3_lattices(X0,X1,X2)
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ 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,[],[f6334]) ).
fof(f6336,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ( ~ r2_hidden(X1,k22_filter_2(X0,X1,X2))
| ~ r2_hidden(X2,k22_filter_2(X0,X1,X2)) )
& r3_lattices(X0,X1,X2)
& 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,[],[f3001]) ).
fof(f6337,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ( ~ r2_hidden(X1,k22_filter_2(X0,X1,X2))
| ~ r2_hidden(X2,k22_filter_2(X0,X1,X2)) )
& r3_lattices(X0,X1,X2)
& 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,[],[f6336]) ).
fof(f11894,plain,
! [X2,X0,X1] :
( ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| r3_lattices(X0,X1,X2)
| ~ r2_hidden(X1,k18_filter_2(X0,X2)) ),
inference(cnf_transformation,[],[f6247]) ).
fof(f11899,plain,
! [X2,X0,X1] :
( ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| r2_hidden(X1,k18_filter_2(X0,X1)) ),
inference(cnf_transformation,[],[f6251]) ).
fof(f12028,plain,
! [X2,X3,X0,X1] :
( ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ r3_lattices(X0,X1,X2)
| ~ r3_lattices(X0,X3,X2)
| ~ r3_lattices(X0,X1,X3)
| r2_hidden(X3,k22_filter_2(X0,X1,X2)) ),
inference(cnf_transformation,[],[f6335]) ).
fof(f12029,plain,
( ~ r2_hidden(sK974,k22_filter_2(sK972,sK973,sK974))
| ~ r2_hidden(sK973,k22_filter_2(sK972,sK973,sK974)) ),
inference(cnf_transformation,[],[f6337]) ).
fof(f12030,plain,
m1_subset_1(sK974,u1_struct_0(sK972)),
inference(cnf_transformation,[],[f6337]) ).
fof(f12031,plain,
r3_lattices(sK972,sK973,sK974),
inference(cnf_transformation,[],[f6337]) ).
fof(f12032,plain,
m1_subset_1(sK973,u1_struct_0(sK972)),
inference(cnf_transformation,[],[f6337]) ).
fof(f12033,plain,
l3_lattices(sK972),
inference(cnf_transformation,[],[f6337]) ).
fof(f12034,plain,
v10_lattices(sK972),
inference(cnf_transformation,[],[f6337]) ).
fof(f12035,plain,
~ v3_struct_0(sK972),
inference(cnf_transformation,[],[f6337]) ).
fof(f18571,plain,
! [X2,X0,X1] :
( ~ r3_lattices(X0,X1,X2)
| v10_lattices(X0)
| v3_struct_0(X0)
| m1_subset_1(X1,u1_struct_0(X0))
| m1_subset_1(X2,u1_struct_0(X0))
| ~ l3_lattices(X0)
| ~ r2_hidden(X1,k18_filter_2(X0,X2)) ),
inference(consistent_polarity_flipping,[],[f11894]) ).
fof(f18575,plain,
! [X2,X0,X1] :
( ~ l3_lattices(X0)
| v10_lattices(X0)
| v3_struct_0(X0)
| m1_subset_1(X1,u1_struct_0(X0))
| m1_subset_1(X2,u1_struct_0(X0))
| r2_hidden(X1,k18_filter_2(X0,X1)) ),
inference(consistent_polarity_flipping,[],[f11899]) ).
fof(f18704,plain,
! [X2,X3,X0,X1] :
( ~ l3_lattices(X0)
| v10_lattices(X0)
| v3_struct_0(X0)
| m1_subset_1(X1,u1_struct_0(X0))
| m1_subset_1(X2,u1_struct_0(X0))
| m1_subset_1(X3,u1_struct_0(X0))
| r3_lattices(X0,X1,X2)
| r3_lattices(X0,X3,X2)
| r3_lattices(X0,X1,X3)
| r2_hidden(X3,k22_filter_2(X0,X1,X2)) ),
inference(consistent_polarity_flipping,[],[f12028]) ).
fof(f18707,plain,
~ v10_lattices(sK972),
inference(consistent_polarity_flipping,[],[f12034]) ).
fof(f18708,plain,
~ m1_subset_1(sK973,u1_struct_0(sK972)),
inference(consistent_polarity_flipping,[],[f12032]) ).
fof(f18709,plain,
~ r3_lattices(sK972,sK973,sK974),
inference(consistent_polarity_flipping,[],[f12031]) ).
fof(f18710,plain,
~ m1_subset_1(sK974,u1_struct_0(sK972)),
inference(consistent_polarity_flipping,[],[f12030]) ).
fof(f18720,definition,
( spl975_1
<=> r2_hidden(sK973,k22_filter_2(sK972,sK973,sK974)) ),
introduced(definition,[new_symbols(definition,[spl975_1])],[avatar_definition]) ).
fof(f18722,plain,
( ~ r2_hidden(sK973,k22_filter_2(sK972,sK973,sK974))
| spl975_1 ),
inference(avatar_component_clause,[],[f18720]) ).
fof(f18724,definition,
( spl975_2
<=> r2_hidden(sK974,k22_filter_2(sK972,sK973,sK974)) ),
introduced(definition,[new_symbols(definition,[spl975_2])],[avatar_definition]) ).
fof(f18726,plain,
( ~ r2_hidden(sK974,k22_filter_2(sK972,sK973,sK974))
| spl975_2 ),
inference(avatar_component_clause,[],[f18724]) ).
fof(f18727,plain,
( ~ spl975_1
| ~ spl975_2 ),
inference(avatar_split_clause,[],[f12029,f18724,f18720]) ).
fof(f78631,definition,
( spl975_3188
<=> ! [X0] : m1_subset_1(X0,u1_struct_0(sK972)) ),
introduced(definition,[new_symbols(definition,[spl975_3188])],[avatar_definition]) ).
fof(f78632,plain,
( ! [X0] : m1_subset_1(X0,u1_struct_0(sK972))
| ~ spl975_3188 ),
inference(avatar_component_clause,[],[f78631]) ).
fof(f122910,plain,
( $false
| ~ spl975_3188 ),
inference(backward_subsumption_resolution,[],[f18710,f78632]) ).
fof(f123013,plain,
~ spl975_3188,
inference(avatar_contradiction_clause,[],[f122910]) ).
fof(f123640,plain,
! [X0,X1] :
( v10_lattices(sK972)
| v3_struct_0(sK972)
| m1_subset_1(X0,u1_struct_0(sK972))
| m1_subset_1(X1,u1_struct_0(sK972))
| r2_hidden(X0,k18_filter_2(sK972,X0)) ),
inference(resolution,[],[f18575,f12033]) ).
fof(f123641,plain,
! [X0,X1] :
( v3_struct_0(sK972)
| m1_subset_1(X0,u1_struct_0(sK972))
| m1_subset_1(X1,u1_struct_0(sK972))
| r2_hidden(X0,k18_filter_2(sK972,X0)) ),
inference(forward_subsumption_resolution,[],[f123640,f18707]) ).
fof(f123665,plain,
! [X0,X1] :
( m1_subset_1(X0,u1_struct_0(sK972))
| m1_subset_1(X1,u1_struct_0(sK972))
| r2_hidden(X0,k18_filter_2(sK972,X0)) ),
inference(forward_subsumption_resolution,[],[f123641,f12035]) ).
fof(f123685,definition,
( spl975_5664
<=> ! [X0] :
( m1_subset_1(X0,u1_struct_0(sK972))
| r2_hidden(X0,k18_filter_2(sK972,X0)) ) ),
introduced(definition,[new_symbols(definition,[spl975_5664])],[avatar_definition]) ).
fof(f123686,plain,
( ! [X0] :
( r2_hidden(X0,k18_filter_2(sK972,X0))
| m1_subset_1(X0,u1_struct_0(sK972)) )
| ~ spl975_5664 ),
inference(avatar_component_clause,[],[f123685]) ).
fof(f123687,plain,
( spl975_3188
| spl975_5664 ),
inference(avatar_split_clause,[],[f123665,f123685,f78631]) ).
fof(f290735,plain,
! [X2,X0,X1] :
( v10_lattices(sK972)
| v3_struct_0(sK972)
| m1_subset_1(X0,u1_struct_0(sK972))
| m1_subset_1(X1,u1_struct_0(sK972))
| m1_subset_1(X2,u1_struct_0(sK972))
| r3_lattices(sK972,X0,X1)
| r3_lattices(sK972,X2,X1)
| r3_lattices(sK972,X0,X2)
| r2_hidden(X2,k22_filter_2(sK972,X0,X1)) ),
inference(resolution,[],[f18704,f12033]) ).
fof(f290736,plain,
! [X2,X0,X1] :
( v3_struct_0(sK972)
| m1_subset_1(X0,u1_struct_0(sK972))
| m1_subset_1(X1,u1_struct_0(sK972))
| m1_subset_1(X2,u1_struct_0(sK972))
| r3_lattices(sK972,X0,X1)
| r3_lattices(sK972,X2,X1)
| r3_lattices(sK972,X0,X2)
| r2_hidden(X2,k22_filter_2(sK972,X0,X1)) ),
inference(forward_subsumption_resolution,[],[f290735,f18707]) ).
fof(f290760,plain,
! [X2,X0,X1] :
( r2_hidden(X2,k22_filter_2(sK972,X0,X1))
| m1_subset_1(X1,u1_struct_0(sK972))
| m1_subset_1(X2,u1_struct_0(sK972))
| r3_lattices(sK972,X0,X1)
| r3_lattices(sK972,X2,X1)
| r3_lattices(sK972,X0,X2)
| m1_subset_1(X0,u1_struct_0(sK972)) ),
inference(forward_subsumption_resolution,[],[f290736,f12035]) ).
fof(f595740,plain,
( m1_subset_1(sK974,u1_struct_0(sK972))
| m1_subset_1(sK973,u1_struct_0(sK972))
| r3_lattices(sK972,sK973,sK974)
| r3_lattices(sK972,sK973,sK974)
| r3_lattices(sK972,sK973,sK973)
| m1_subset_1(sK973,u1_struct_0(sK972))
| spl975_1 ),
inference(resolution,[],[f290760,f18722]) ).
fof(f595741,plain,
( m1_subset_1(sK974,u1_struct_0(sK972))
| m1_subset_1(sK974,u1_struct_0(sK972))
| r3_lattices(sK972,sK973,sK974)
| r3_lattices(sK972,sK974,sK974)
| r3_lattices(sK972,sK973,sK974)
| m1_subset_1(sK973,u1_struct_0(sK972))
| spl975_2 ),
inference(resolution,[],[f290760,f18726]) ).
fof(f595742,plain,
( m1_subset_1(sK974,u1_struct_0(sK972))
| r3_lattices(sK972,sK973,sK974)
| r3_lattices(sK972,sK974,sK974)
| m1_subset_1(sK973,u1_struct_0(sK972))
| spl975_2 ),
inference(duplicate_literal_removal,[],[f595741]) ).
fof(f595743,plain,
( m1_subset_1(sK974,u1_struct_0(sK972))
| m1_subset_1(sK973,u1_struct_0(sK972))
| r3_lattices(sK972,sK973,sK974)
| r3_lattices(sK972,sK973,sK973)
| spl975_1 ),
inference(duplicate_literal_removal,[],[f595740]) ).
fof(f595744,plain,
( r3_lattices(sK972,sK973,sK974)
| r3_lattices(sK972,sK974,sK974)
| m1_subset_1(sK973,u1_struct_0(sK972))
| spl975_2 ),
inference(forward_subsumption_resolution,[],[f595742,f18710]) ).
fof(f595745,plain,
( m1_subset_1(sK973,u1_struct_0(sK972))
| r3_lattices(sK972,sK973,sK974)
| r3_lattices(sK972,sK973,sK973)
| spl975_1 ),
inference(forward_subsumption_resolution,[],[f595743,f18710]) ).
fof(f595760,plain,
( r3_lattices(sK972,sK974,sK974)
| m1_subset_1(sK973,u1_struct_0(sK972))
| spl975_2 ),
inference(forward_subsumption_resolution,[],[f595744,f18709]) ).
fof(f595761,plain,
( r3_lattices(sK972,sK973,sK974)
| r3_lattices(sK972,sK973,sK973)
| spl975_1 ),
inference(forward_subsumption_resolution,[],[f595745,f18708]) ).
fof(f595762,plain,
( r3_lattices(sK972,sK974,sK974)
| spl975_2 ),
inference(forward_subsumption_resolution,[],[f595760,f18708]) ).
fof(f595763,plain,
( r3_lattices(sK972,sK973,sK973)
| spl975_1 ),
inference(forward_subsumption_resolution,[],[f595761,f18709]) ).
fof(f596019,plain,
( v10_lattices(sK972)
| v3_struct_0(sK972)
| m1_subset_1(sK974,u1_struct_0(sK972))
| m1_subset_1(sK974,u1_struct_0(sK972))
| ~ l3_lattices(sK972)
| ~ r2_hidden(sK974,k18_filter_2(sK972,sK974))
| spl975_2 ),
inference(resolution,[],[f595762,f18571]) ).
fof(f596024,plain,
( v10_lattices(sK972)
| v3_struct_0(sK972)
| m1_subset_1(sK974,u1_struct_0(sK972))
| ~ l3_lattices(sK972)
| ~ r2_hidden(sK974,k18_filter_2(sK972,sK974))
| spl975_2 ),
inference(duplicate_literal_removal,[],[f596019]) ).
fof(f596033,plain,
( v10_lattices(sK972)
| v3_struct_0(sK972)
| m1_subset_1(sK974,u1_struct_0(sK972))
| ~ l3_lattices(sK972)
| spl975_2
| ~ spl975_5664 ),
inference(forward_subsumption_resolution,[],[f596024,f123686]) ).
fof(f596043,plain,
( v3_struct_0(sK972)
| m1_subset_1(sK974,u1_struct_0(sK972))
| ~ l3_lattices(sK972)
| spl975_2
| ~ spl975_5664 ),
inference(forward_subsumption_resolution,[],[f596033,f18707]) ).
fof(f596053,plain,
( m1_subset_1(sK974,u1_struct_0(sK972))
| ~ l3_lattices(sK972)
| spl975_2
| ~ spl975_5664 ),
inference(forward_subsumption_resolution,[],[f596043,f12035]) ).
fof(f596063,plain,
( ~ l3_lattices(sK972)
| spl975_2
| ~ spl975_5664 ),
inference(forward_subsumption_resolution,[],[f596053,f18710]) ).
fof(f596071,plain,
( $false
| spl975_2
| ~ spl975_5664 ),
inference(forward_subsumption_resolution,[],[f596063,f12033]) ).
fof(f596072,plain,
( spl975_2
| ~ spl975_5664 ),
inference(avatar_contradiction_clause,[],[f596071]) ).
fof(f596268,plain,
( v10_lattices(sK972)
| v3_struct_0(sK972)
| m1_subset_1(sK973,u1_struct_0(sK972))
| m1_subset_1(sK973,u1_struct_0(sK972))
| ~ l3_lattices(sK972)
| ~ r2_hidden(sK973,k18_filter_2(sK972,sK973))
| spl975_1 ),
inference(resolution,[],[f595763,f18571]) ).
fof(f596273,plain,
( v10_lattices(sK972)
| v3_struct_0(sK972)
| m1_subset_1(sK973,u1_struct_0(sK972))
| ~ l3_lattices(sK972)
| ~ r2_hidden(sK973,k18_filter_2(sK972,sK973))
| spl975_1 ),
inference(duplicate_literal_removal,[],[f596268]) ).
fof(f596282,plain,
( v10_lattices(sK972)
| v3_struct_0(sK972)
| m1_subset_1(sK973,u1_struct_0(sK972))
| ~ l3_lattices(sK972)
| spl975_1
| ~ spl975_5664 ),
inference(forward_subsumption_resolution,[],[f596273,f123686]) ).
fof(f596292,plain,
( v3_struct_0(sK972)
| m1_subset_1(sK973,u1_struct_0(sK972))
| ~ l3_lattices(sK972)
| spl975_1
| ~ spl975_5664 ),
inference(forward_subsumption_resolution,[],[f596282,f18707]) ).
fof(f596302,plain,
( m1_subset_1(sK973,u1_struct_0(sK972))
| ~ l3_lattices(sK972)
| spl975_1
| ~ spl975_5664 ),
inference(forward_subsumption_resolution,[],[f596292,f12035]) ).
fof(f596312,plain,
( ~ l3_lattices(sK972)
| spl975_1
| ~ spl975_5664 ),
inference(forward_subsumption_resolution,[],[f596302,f18708]) ).
fof(f596320,plain,
( $false
| spl975_1
| ~ spl975_5664 ),
inference(forward_subsumption_resolution,[],[f596312,f12033]) ).
fof(f596321,plain,
( spl975_1
| ~ spl975_5664 ),
inference(avatar_contradiction_clause,[],[f596320]) ).
cnf(s1,plain,
( ~ spl975_1
| ~ spl975_2 ),
inference(sat_conversion,[],[f18727]) ).
cnf(s5933,plain,
~ spl975_3188,
inference(sat_conversion,[],[f123013]) ).
cnf(s5983,plain,
( spl975_3188
| spl975_5664 ),
inference(sat_conversion,[],[f123687]) ).
cnf(s30272,plain,
( spl975_2
| ~ spl975_5664 ),
inference(sat_conversion,[],[f596072]) ).
cnf(s30343,plain,
( spl975_1
| ~ spl975_5664 ),
inference(sat_conversion,[],[f596321]) ).
cnf(s31292,plain,
spl975_5664,
inference(rat,[],[s5983,s5933]) ).
cnf(s31293,plain,
spl975_1,
inference(rat,[],[s30343,s31292]) ).
cnf(s31294,plain,
spl975_2,
inference(rat,[],[s30272,s31292]) ).
cnf(s31950,plain,
$false,
inference(rat,[],[s1,s31294,s31293]) ).
fof(f596341,plain,
$false,
inference(avatar_sat_refutation,[],[s31950]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT327+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.40 % Computer : n011.cluster.edu
% 0.10/0.40 % Model : x86_64 x86_64
% 0.10/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.40 % Memory : 8046.5625MB
% 0.10/0.40 % OS : Linux 6.8.0-71-generic
% 0.10/0.40 % CPULimit : 300
% 0.10/0.40 % WCLimit : 300
% 0.10/0.40 % DateTime : Sun Sep 27 14:39:46 UTC 2026
% 0.10/0.40 % CPUTime :
% 0.10/0.40 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.43 Running first-order model finding
% 0.10/0.43 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 24.81/4.10 % (2495377)Will run a generic schedule for satisfiability detection.
% 24.81/4.10 % (2495386)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=315738429:i=116_2998 on theBenchmark for (2998ds/116Mi)
% 24.81/4.10 % (2495383)% WARNING: option uhcvi not known.
% 24.81/4.10 % (2495382)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1952506391_2998 on theBenchmark for (2998ds/0Mi)
% 24.81/4.10 % (2495383)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4268407245:i=135531:add=off:rawr=on_2998 on theBenchmark for (2998ds/135531Mi)
% 24.81/4.10 % (2495384)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2123394254:i=88024:add=on:rawr=on_2998 on theBenchmark for (2998ds/88024Mi)
% 24.81/4.10 % (2495385)dis+10_1_sil=32000:sp=arity:random_seed=2134036433:i=103:fgj=on_2998 on theBenchmark for (2998ds/103Mi)
% 24.81/4.10 % (2495387)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1558168861:i=131_2998 on theBenchmark for (2998ds/131Mi)
% 24.81/4.10 % (2495388)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3934969093:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2998 on theBenchmark for (2998ds/159Mi)
% 24.81/4.10 % (2495386)Instruction limit reached!
% 24.81/4.10 % (2495386)------------------------------
% 24.81/4.10 % (2495386)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.81/4.10 % (2495386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.81/4.10 % (2495386)CaDiCaL version: 2.1.3
% 24.81/4.10 % (2495386)Termination reason: Instruction limit
% 24.81/4.10 % (2495386)Termination phase: NewCNF
% 24.81/4.10 % (2495386)Time elapsed: 0.042 s
% 24.81/4.10 % (2495386)Peak memory usage: 20 MB
% 24.81/4.10 % (2495386)Instructions burned: 119 (million)
% 24.81/4.10 % (2495396)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4153801136:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 24.81/4.10 % (2495385)Instruction limit reached!
% 24.81/4.10 % (2495385)------------------------------
% 24.81/4.10 % (2495385)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.81/4.10 % (2495385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.81/4.10 % (2495385)CaDiCaL version: 2.1.3
% 24.81/4.10 % (2495385)Termination reason: Instruction limit
% 24.81/4.10 % (2495385)Termination phase: Clausification
% 24.81/4.10 % (2495385)Time elapsed: 0.067 s
% 24.81/4.10 % (2495385)Peak memory usage: 19 MB
% 24.81/4.10 % (2495385)Instructions burned: 103 (million)
% 24.81/4.10 % (2495387)Instruction limit reached!
% 24.81/4.10 % (2495387)------------------------------
% 24.81/4.10 % (2495387)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.81/4.10 % (2495387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.81/4.10 % (2495387)CaDiCaL version: 2.1.3
% 24.81/4.10 % (2495387)Termination reason: Instruction limit
% 24.81/4.10 % (2495387)Termination phase: Property scanning
% 24.81/4.10 % (2495387)Time elapsed: 0.081 s
% 24.81/4.10 % (2495387)Peak memory usage: 20 MB
% 24.81/4.10 % (2495387)Instructions burned: 132 (million)
% 24.81/4.10 % (2495398)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=262037145:i=131:bd=preordered:fsd=on_2997 on theBenchmark for (2997ds/131Mi)
% 24.81/4.10 % (2495388)Instruction limit reached!
% 24.81/4.10 % (2495388)------------------------------
% 24.81/4.10 % (2495388)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.81/4.10 % (2495388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.81/4.10 % (2495388)CaDiCaL version: 2.1.3
% 24.81/4.10 % (2495388)Termination reason: Instruction limit
% 24.81/4.10 % (2495388)Termination phase: Property scanning
% 24.81/4.10 % (2495388)Time elapsed: 0.093 s
% 24.81/4.10 % (2495388)Peak memory usage: 20 MB
% 24.81/4.10 % (2495388)Instructions burned: 161 (million)
% 24.81/4.10 % (2495399)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=3168469710:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2997 on theBenchmark for (2997ds/684Mi)
% 24.81/4.10 % (2495401)ott-21_1_sil=16000:fs=off:random_seed=2388663075:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 24.81/4.10 % (2495398)Instruction limit reached!
% 24.81/4.10 % (2495398)------------------------------
% 24.81/4.10 % (2495398)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.81/4.10 % (2495398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.95/7.32 % (2495398)CaDiCaL version: 2.1.3
% 47.95/7.32 % (2495398)Termination reason: Instruction limit
% 47.95/7.32 % (2495398)Termination phase: Property scanning
% 47.95/7.32 % (2495398)Time elapsed: 0.079 s
% 47.95/7.32 % (2495398)Peak memory usage: 20 MB
% 47.95/7.32 % (2495398)Instructions burned: 131 (million)
% 47.95/7.32 % (2495404)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1974513740:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 47.95/7.32 % (2495401)Instruction limit reached!
% 47.95/7.32 % (2495401)------------------------------
% 47.95/7.32 % (2495401)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.95/7.32 % (2495401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.95/7.32 % (2495401)CaDiCaL version: 2.1.3
% 47.95/7.32 % (2495401)Termination reason: Instruction limit
% 47.95/7.32 % (2495401)Termination phase: Function definition elimination
% 47.95/7.32 % (2495401)Time elapsed: 0.098 s
% 47.95/7.32 % (2495401)Peak memory usage: 20 MB
% 47.95/7.32 % (2495401)Instructions burned: 182 (million)
% 47.95/7.32 % (2495396)Instruction limit reached!
% 47.95/7.32 % (2495396)------------------------------
% 47.95/7.32 % (2495396)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.95/7.32 % (2495396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.95/7.32 % (2495396)CaDiCaL version: 2.1.3
% 47.95/7.32 % (2495396)Termination reason: Instruction limit
% 47.95/7.32 % (2495396)Termination phase: Finite model building preprocessing
% 47.95/7.32 % (2495396)Time elapsed: 0.171 s
% 47.95/7.32 % (2495396)Peak memory usage: 28 MB
% 47.95/7.32 % (2495396)Instructions burned: 722 (million)
% 47.95/7.32 % (2495407)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2093496228:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 47.95/7.32 % (2495406)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2092136677:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 47.95/7.32 % (2495404)Instruction limit reached!
% 47.95/7.32 % (2495404)------------------------------
% 47.95/7.32 % (2495404)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.95/7.32 % (2495404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.95/7.32 % (2495404)CaDiCaL version: 2.1.3
% 47.95/7.32 % (2495404)Termination reason: Instruction limit
% 47.95/7.32 % (2495404)Termination phase: Saturation
% 47.95/7.32 % (2495404)Time elapsed: 0.242 s
% 47.95/7.32 % (2495404)Peak memory usage: 24 MB
% 47.95/7.32 % (2495404)Instructions burned: 478 (million)
% 47.95/7.32 % (2495399)Instruction limit reached!
% 47.95/7.32 % (2495399)------------------------------
% 47.95/7.32 % (2495399)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.95/7.32 % (2495399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.95/7.32 % (2495399)CaDiCaL version: 2.1.3
% 47.95/7.32 % (2495399)Termination reason: Instruction limit
% 47.95/7.32 % (2495399)Termination phase: Saturation
% 47.95/7.32 % (2495399)Time elapsed: 0.333 s
% 47.95/7.32 % (2495399)Peak memory usage: 25 MB
% 47.95/7.32 % (2495399)Instructions burned: 685 (million)
% 47.95/7.32 % (2495410)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=957534303:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 47.95/7.32 % (2495411)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=3865603861:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 47.95/7.32 % (2495407)Instruction limit reached!
% 47.95/7.32 % (2495407)------------------------------
% 47.95/7.32 % (2495407)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.95/7.32 % (2495407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.95/7.32 % (2495407)CaDiCaL version: 2.1.3
% 47.95/7.32 % (2495407)Termination reason: Instruction limit
% 47.95/7.32 % (2495407)Termination phase: Saturation
% 47.95/7.32 % (2495407)Time elapsed: 0.342 s
% 47.95/7.32 % (2495407)Peak memory usage: 35 MB
% 47.95/7.32 % (2495407)Instructions burned: 1182 (million)
% 47.95/7.32 % (2495414)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1771661999:i=879:kws=inv_precedence:fsr=off_2992 on theBenchmark for (2992ds/879Mi)
% 47.95/7.32 % (2495406)Instruction limit reached!
% 47.95/7.32 % (2495406)------------------------------
% 47.95/7.32 % (2495406)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.95/7.32 % (2495406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.02/17.65 % (2495406)CaDiCaL version: 2.1.3
% 121.02/17.65 % (2495406)Termination reason: Instruction limit
% 121.02/17.65 % (2495406)Termination phase: Finite model building preprocessing
% 121.02/17.65 % (2495406)Time elapsed: 0.379 s
% 121.02/17.65 % (2495406)Peak memory usage: 30 MB
% 121.02/17.65 % (2495406)Instructions burned: 868 (million)
% 121.02/17.65 % (2495416)fmb+10_1_sil=64000:random_seed=3464974088:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi)
% 121.02/17.65 % (2495414)Instruction limit reached!
% 121.02/17.65 % (2495414)------------------------------
% 121.02/17.65 % (2495414)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 121.02/17.65 % (2495414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.02/17.65 % (2495414)CaDiCaL version: 2.1.3
% 121.02/17.65 % (2495414)Termination reason: Instruction limit
% 121.02/17.65 % (2495414)Termination phase: Saturation
% 121.02/17.65 % (2495414)Time elapsed: 0.208 s
% 121.02/17.65 % (2495414)Peak memory usage: 30 MB
% 121.02/17.65 % (2495414)Instructions burned: 882 (million)
% 121.02/17.65 % (2495418)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3952472532:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 121.02/17.65 % (2495411)Instruction limit reached!
% 121.02/17.65 % (2495411)------------------------------
% 121.02/17.65 % (2495411)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 121.02/17.65 % (2495411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.02/17.65 % (2495411)CaDiCaL version: 2.1.3
% 121.02/17.65 % (2495411)Termination reason: Instruction limit
% 121.02/17.65 % (2495411)Termination phase: Saturation
% 121.02/17.65 % (2495411)Time elapsed: 0.360 s
% 121.02/17.65 % (2495411)Peak memory usage: 30 MB
% 121.02/17.65 % (2495411)Instructions burned: 692 (million)
% 121.02/17.65 % (2495420)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2551174063:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 121.02/17.65 % (2495410)Instruction limit reached!
% 121.02/17.65 % (2495410)------------------------------
% 121.02/17.65 % (2495410)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 121.02/17.65 % (2495410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.02/17.65 % (2495410)CaDiCaL version: 2.1.3
% 121.02/17.65 % (2495410)Termination reason: Instruction limit
% 121.02/17.65 % (2495410)Termination phase: Finite model building preprocessing
% 121.02/17.65 % (2495410)Time elapsed: 0.390 s
% 121.02/17.65 % (2495410)Peak memory usage: 31 MB
% 121.02/17.65 % (2495410)Instructions burned: 889 (million)
% 121.02/17.65 % (2495422)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1479456030:i=5131_2990 on theBenchmark for (2990ds/5131Mi)
% 121.02/17.65 % (2495420)Instruction limit reached!
% 121.02/17.65 % (2495420)------------------------------
% 121.02/17.65 % (2495420)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 121.02/17.65 % (2495420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.02/17.65 % (2495420)CaDiCaL version: 2.1.3
% 121.02/17.65 % (2495420)Termination reason: Instruction limit
% 121.02/17.65 % (2495420)Termination phase: Finite model building preprocessing
% 121.02/17.65 % (2495420)Time elapsed: 0.403 s
% 121.02/17.65 % (2495420)Peak memory usage: 31 MB
% 121.02/17.65 % (2495420)Instructions burned: 921 (million)
% 121.02/17.65 % (2495424)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=894672713:i=1472:ins=7:fdi=8:gsp=on_2986 on theBenchmark for (2986ds/1472Mi)
% 121.02/17.66 % (2495424)Instruction limit reached!
% 121.02/17.66 % (2495424)------------------------------
% 121.02/17.66 % (2495424)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 121.02/17.66 % (2495424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.02/17.66 % (2495424)CaDiCaL version: 2.1.3
% 121.02/17.66 % (2495424)Termination reason: Instruction limit
% 121.02/17.66 % (2495424)Termination phase: Saturation
% 121.02/17.66 % (2495424)Time elapsed: 0.619 s
% 121.02/17.66 % (2495424)Peak memory usage: 26 MB
% 121.02/17.66 % (2495424)Instructions burned: 1474 (million)
% 121.02/17.66 % (2495426)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3671056533:i=6324_2979 on theBenchmark for (2979ds/6324Mi)
% 121.02/17.66 % (2495418)Instruction limit reached!
% 121.02/17.66 % (2495418)------------------------------
% 121.02/17.66 % (2495418)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 121.02/17.66 % (2495418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.02/17.66 % (2495418)CaDiCaL version: 2.1.3
% 121.02/17.66 % (2495418)Termination reason: Instruction limit
% 165.17/33.60 % (2495418)Termination phase: Finite model building preprocessing
% 165.17/33.60 % (2495418)Time elapsed: 2.699 s
% 165.17/33.60 % (2495418)Peak memory usage: 51 MB
% 165.17/33.60 % (2495418)Instructions burned: 9516 (million)
% 165.17/33.60 % (2495428)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3605759006:fmbsr=2.30978:i=2174_2963 on theBenchmark for (2963ds/2174Mi)
% 165.17/33.60 % (2495422)Instruction limit reached!
% 165.17/33.60 % (2495422)------------------------------
% 165.17/33.60 % (2495422)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 165.17/33.60 % (2495422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 165.17/33.60 % (2495422)CaDiCaL version: 2.1.3
% 165.17/33.60 % (2495422)Termination reason: Instruction limit
% 165.17/33.60 % (2495422)Termination phase: Saturation
% 165.17/33.60 % (2495422)Time elapsed: 2.879 s
% 165.17/33.60 % (2495422)Peak memory usage: 61 MB
% 165.17/33.60 % (2495422)Instructions burned: 5133 (million)
% 165.17/33.60 % (2495430)ott-2_1_sil=16000:newcnf=on:random_seed=860691307:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2961 on theBenchmark for (2961ds/869Mi)
% 165.17/33.60 % (2495428)Instruction limit reached!
% 165.17/33.60 % (2495428)------------------------------
% 165.17/33.60 % (2495428)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 165.17/33.60 % (2495428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 165.17/33.60 % (2495428)CaDiCaL version: 2.1.3
% 165.17/33.60 % (2495428)Termination reason: Instruction limit
% 165.17/33.60 % (2495428)Termination phase: Finite model building preprocessing
% 165.17/33.60 % (2495428)Time elapsed: 0.359 s
% 165.17/33.60 % (2495428)Peak memory usage: 37 MB
% 165.17/33.60 % (2495428)Instructions burned: 2182 (million)
% 165.17/33.60 % (2495432)ott+10_1_sil=32000:tgt=ground:random_seed=3868917350:i=5114:av=off_2959 on theBenchmark for (2959ds/5114Mi)
% 165.17/33.60 % (2495430)Instruction limit reached!
% 165.17/33.60 % (2495430)------------------------------
% 165.17/33.60 % (2495430)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 165.17/33.60 % (2495430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 165.17/33.60 % (2495430)CaDiCaL version: 2.1.3
% 165.17/33.60 % (2495430)Termination reason: Instruction limit
% 165.17/33.60 % (2495430)Termination phase: Saturation
% 165.17/33.60 % (2495430)Time elapsed: 0.429 s
% 165.17/33.60 % (2495430)Peak memory usage: 30 MB
% 165.17/33.60 % (2495430)Instructions burned: 870 (million)
% 165.17/33.60 % (2495434)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2567123737:i=54282_2956 on theBenchmark for (2956ds/54282Mi)
% 165.17/33.60 % (2495426)Instruction limit reached!
% 165.17/33.60 % (2495426)------------------------------
% 165.17/33.60 % (2495426)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 165.17/33.60 % (2495426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 165.17/33.60 % (2495426)CaDiCaL version: 2.1.3
% 165.17/33.60 % (2495426)Termination reason: Instruction limit
% 165.17/33.60 % (2495426)Termination phase: Finite model building preprocessing
% 165.17/33.60 % (2495426)Time elapsed: 3.331 s
% 165.17/33.60 % (2495426)Peak memory usage: 47 MB
% 165.17/33.60 % (2495426)Instructions burned: 6324 (million)
% 165.17/33.60 % (2495436)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=4222453939:i=3512:aac=none_2946 on theBenchmark for (2946ds/3512Mi)
% 165.17/33.60 % (2495432)Instruction limit reached!
% 165.17/33.60 % (2495432)------------------------------
% 165.17/33.60 % (2495432)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 165.17/33.60 % (2495432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 165.17/33.60 % (2495432)CaDiCaL version: 2.1.3
% 165.17/33.60 % (2495432)Termination reason: Instruction limit
% 165.17/33.60 % (2495432)Termination phase: Saturation
% 165.17/33.60 % (2495432)Time elapsed: 1.661 s
% 165.17/33.60 % (2495432)Peak memory usage: 80 MB
% 165.17/33.60 % (2495432)Instructions burned: 5116 (million)
% 165.17/33.60 % (2495438)dis+21_1_sil=32000:sas=cadical:random_seed=3633444861:i=3773:amm=off_2942 on theBenchmark for (2942ds/3773Mi)
% 165.17/33.60 % (2495438)Instruction limit reached!
% 165.17/33.60 % (2495438)------------------------------
% 165.17/33.60 % (2495438)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 165.17/33.60 % (2495438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 165.17/33.60 % (2495438)CaDiCaL version: 2.1.3
% 165.17/33.60 % (2495438)Termination reason: Instruction limit
% 165.17/33.60 % (2495438)Termination phase: Saturation
% 165.17/33.60 % (2495438)Time elapsed: 1.152 s
% 165.17/33.60 % (2495438)Peak memory usage: 59 MB
% 165.17/33.60 % (2495438)Instructions burned: 3776 (million)
% 165.17/33.60 % (2495440)ott+11_1_sil=16000:gs=on:random_seed=288829071:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2931 on theBenchmark for (2931ds/2251Mi)
% 165.17/33.60 % (2495436)Instruction limit reached!
% 165.17/33.60 % (2495436)------------------------------
% 165.17/33.60 % (2495436)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 165.17/33.60 % (2495436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 165.17/33.60 % (2495436)CaDiCaL version: 2.1.3
% 165.17/33.60 % (2495436)Termination reason: Instruction limit
% 165.17/33.60 % (2495436)Termination phase: Saturation
% 165.17/33.60 % (2495436)Time elapsed: 1.938 s
% 165.17/33.60 % (2495436)Peak memory usage: 51 MB
% 165.17/33.60 % (2495436)Instructions burned: 3513 (million)
% 165.17/33.60 % (2495440)Instruction limit reached!
% 165.17/33.60 % (2495440)------------------------------
% 165.17/33.60 % (2495440)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 165.17/33.60 % (2495440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 165.17/33.60 % (2495440)CaDiCaL version: 2.1.3
% 165.17/33.60 % (2495440)Termination reason: Instruction limit
% 165.17/33.60 % (2495440)Termination phase: Saturation
% 165.17/33.60 % (2495440)Time elapsed: 0.468 s
% 165.17/33.60 % (2495440)Peak memory usage: 28 MB
% 165.17/33.60 % (2495440)Instructions burned: 2257 (million)
% 165.17/33.60 % (2495442)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=25790266:fmbsr=1.6:i=67534_2926 on theBenchmark for (2926ds/67534Mi)
% 165.17/33.60 % (2495443)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=96977904:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2926 on theBenchmark for (2926ds/4591Mi)
% 165.17/33.60 % (2495443)Instruction limit reached!
% 165.17/33.60 % (2495443)------------------------------
% 165.17/33.60 % (2495443)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 165.17/33.60 % (2495443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 165.17/33.60 % (2495443)CaDiCaL version: 2.1.3
% 165.17/33.60 % (2495443)Termination reason: Instruction limit
% 165.17/33.60 % (2495443)Termination phase: Saturation
% 165.17/33.60 % (2495443)Time elapsed: 1.694 s
% 165.17/33.60 % (2495443)Peak memory usage: 119 MB
% 165.17/33.60 % (2495443)Instructions burned: 4591 (million)
% 165.17/33.60 % (2495447)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=4128686601:i=29340_2909 on theBenchmark for (2909ds/29340Mi)
% 165.17/33.60 % (2495416)Instruction limit reached!
% 165.17/33.60 % (2495416)------------------------------
% 165.17/33.60 % (2495416)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 165.17/33.60 % (2495416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 165.17/33.60 % (2495416)CaDiCaL version: 2.1.3
% 165.17/33.60 % (2495416)Termination reason: Instruction limit
% 165.17/33.60 % (2495416)Termination phase: Finite model building preprocessing
% 165.17/33.60 % (2495416)Time elapsed: 12.008 s
% 165.17/33.60 % (2495416)Peak memory usage: 68 MB
% 165.17/33.60 % (2495416)Instructions burned: 22062 (million)
% 165.17/33.60 % (2495449)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2840359117:i=5211_2872 on theBenchmark for (2872ds/5211Mi)
% 165.17/33.60 % (2495449)Instruction limit reached!
% 165.17/33.60 % (2495449)------------------------------
% 165.17/33.60 % (2495449)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 165.17/33.60 % (2495449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 165.17/33.60 % (2495449)CaDiCaL version: 2.1.3
% 165.17/33.60 % (2495449)Termination reason: Instruction limit
% 165.17/33.60 % (2495449)Termination phase: Saturation
% 165.17/33.60 % (2495449)Time elapsed: 2.020 s
% 165.17/33.60 % (2495449)Peak memory usage: 50 MB
% 165.17/33.60 % (2495449)Instructions burned: 5211 (million)
% 165.17/33.60 % (2495451)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3841064806:i=5497:nm=2_2851 on theBenchmark for (2851ds/5497Mi)
% 165.17/33.60 % (2495447)Instruction limit reached!
% 165.17/33.60 % (2495447)------------------------------
% 165.17/33.60 % (2495447)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 165.17/33.60 % (2495447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 165.17/33.60 % (2495447)CaDiCaL version: 2.1.3
% 165.17/33.60 % (2495447)Termination reason: Instruction limit
% 165.17/33.60 % (2495447)Termination phase: Saturation
% 165.17/33.60 % (2495447)Time elapsed: 8.105 s
% 165.17/33.60 % (2495447)Peak memory usage: 654 MB
% 165.17/33.60 % (2495447)Instructions burned: 29344 (million)
% 165.17/33.60 % (2495453)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3249168163:fmbsr=2:i=46332_2827 on theBenchmark for (2827ds/46332Mi)
% 165.17/33.60 % (2495451)Instruction limit reached!
% 165.17/33.60 % (2495451)------------------------------
% 165.17/33.60 % (2495451)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 165.17/33.60 % (2495451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 165.17/33.60 % (2495451)CaDiCaL version: 2.1.3
% 165.17/33.60 % (2495451)Termination reason: Instruction limit
% 165.17/33.60 % (2495451)Termination phase: Finite model building preprocessing
% 165.17/33.60 % (2495451)Time elapsed: 2.931 s
% 165.17/33.60 % (2495451)Peak memory usage: 44 MB
% 165.17/33.60 % (2495451)Instructions burned: 5500 (million)
% 165.17/33.60 % (2495455)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2766993450:i=14071_2821 on theBenchmark for (2821ds/14071Mi)
% 165.17/33.60 % (2495455)Instruction limit reached!
% 165.17/33.60 % (2495455)------------------------------
% 165.17/33.60 % (2495455)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 165.17/33.60 % (2495455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 165.17/33.60 % (2495455)CaDiCaL version: 2.1.3
% 165.17/33.60 % (2495455)Termination reason: Instruction limit
% 165.17/33.60 % (2495455)Termination phase: Finite model building preprocessing
% 165.17/33.60 % (2495455)Time elapsed: 7.550 s
% 165.17/33.60 % (2495455)Peak memory usage: 58 MB
% 165.17/33.60 % (2495455)Instructions burned: 14071 (million)
% 165.17/33.60 % (2495457)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2129196335:i=22565:add=on:rawr=on_2746 on theBenchmark for (2746ds/22565Mi)
% 165.17/33.60 % (2495384)Instruction limit reached!
% 165.17/33.60 % (2495384)------------------------------
% 165.17/33.60 % (2495384)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 165.17/33.60 % (2495384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 165.17/33.60 % (2495384)CaDiCaL version: 2.1.3
% 165.17/33.60 % (2495384)Termination reason: Instruction limit
% 165.17/33.60 % (2495384)Termination phase: Saturation
% 165.17/33.60 % (2495384)Time elapsed: 26.279 s
% 165.17/33.60 % (2495384)Peak memory usage: 202 MB
% 165.17/33.60 % (2495384)Instructions burned: 88027 (million)
% 165.17/33.60 % (2495459)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1699091530:i=8173:av=off_2735 on theBenchmark for (2735ds/8173Mi)
% 165.17/33.60 % (2495453)Instruction limit reached!
% 165.17/33.60 % (2495453)------------------------------
% 165.17/33.60 % (2495453)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 165.17/33.60 % (2495453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 165.17/33.60 % (2495453)CaDiCaL version: 2.1.3
% 165.17/33.60 % (2495453)Termination reason: Instruction limit
% 165.17/33.60 % (2495453)Termination phase: Finite model building preprocessing
% 165.17/33.60 % (2495453)Time elapsed: 13.603 s
% 165.17/33.60 % (2495453)Peak memory usage: 113 MB
% 165.17/33.60 % (2495453)Instructions burned: 46334 (million)
% 165.17/33.60 % (2495461)dis+10_16:1_sil=16000:random_seed=2516870490:i=9155:fsr=off_2691 on theBenchmark for (2691ds/9155Mi)
% 165.17/33.60 % (2495459)Instruction limit reached!
% 165.17/33.60 % (2495459)------------------------------
% 165.17/33.60 % (2495459)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 165.17/33.60 % (2495459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 165.17/33.60 % (2495459)CaDiCaL version: 2.1.3
% 165.17/33.60 % (2495459)Termination reason: Instruction limit
% 165.17/33.60 % (2495459)Termination phase: Saturation
% 165.17/33.60 % (2495459)Time elapsed: 4.700 s
% 165.17/33.60 % (2495459)Peak memory usage: 226 MB
% 165.17/33.60 % (2495459)Instructions burned: 8173 (million)
% 165.17/33.60 % (2495463)ott-3_8_sil=64000:random_seed=2209805094:i=20139:bs=on_2688 on theBenchmark for (2688ds/20139Mi)
% 165.17/33.60 % (2495383) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2495377-2495383"...
% 165.17/33.60 % (2495383)...printing done.
% 165.17/33.60 % (2495383)Refutation found. Thanks to Tanya!
% 165.17/33.60 % SZS status Theorem for theBenchmark
% 165.17/33.60 % SZS output start Proof for theBenchmark
% See solution above
% 165.17/33.61 % (2495383)------------------------------
% 165.17/33.61 % (2495383)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 165.17/33.61 % (2495383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 165.17/33.61 % (2495383)CaDiCaL version: 2.1.3
% 165.17/33.61 % (2495383)Termination reason: Refutation
% 165.17/33.61 % (2495383)Time elapsed: 32.934 s
% 165.17/33.61 % (2495383)Peak memory usage: 307 MB
% 165.17/33.61 % (2495383)Instructions burned: 62369 (million)
% 165.17/33.61 % (2495377)Success in time 33.16 s
% 165.17/33.61 % Vampire exiting
%------------------------------------------------------------------------------