%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT288+3 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:46:33 AM UTC 2026
% Result : Theorem 17.18s 4.10s
% Output : Refutation 17.77s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 15
% Syntax : Number of formulae : 122 ( 26 unt; 11 def)
% Number of atoms : 633 ( 29 equ)
% Maximal formula atoms : 16 ( 5 avg)
% Number of connectives : 834 ( 323 ~; 408 |; 77 &)
% ( 19 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 23 ( 21 usr; 12 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 2 con; 0-3 aty)
% Number of variables : 89 ( 0 sgn 73 !; 16 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f8,axiom,
! [X0,X1] :
( r1_tarski(X0,X1)
<=> ! [X2] :
( r2_hidden(X2,X0)
=> r2_hidden(X2,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d3_tarski) ).
fof(f12331,axiom,
! [X0,X1,X2] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& v17_lattices(X1)
& ~ v3_realset2(X1)
& l3_lattices(X1)
& m1_subset_1(X2,u1_struct_0(X1)) )
=> ( r2_hidden(X0,a_2_0_lopclset(X1,X2))
<=> ? [X3] :
( m1_filter_0(X3,X1)
& X0 = X3
& v1_filter_0(X3,X1)
& r2_hidden(X2,X3) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fraenkel_a_2_0_lopclset) ).
fof(f12378,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& v17_lattices(X1)
& ~ v3_realset2(X1)
& l3_lattices(X1) )
=> ( r2_hidden(X0,k7_lopclset(X1))
<=> ? [X2] :
( m1_filter_0(X2,X1)
& X2 = X0
& v1_filter_0(X2,X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t18_lopclset) ).
fof(f12379,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& ~ v3_realset2(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> r1_tarski(a_2_0_lopclset(X0,X1),k7_lopclset(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t19_lopclset) ).
fof(f12380,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& ~ v3_realset2(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> r1_tarski(a_2_0_lopclset(X0,X1),k7_lopclset(X0)) ) ),
inference(negated_conjecture,[status(cth)],[f12379]) ).
fof(f12446,plain,
! [X0,X1,X2] :
( ( r2_hidden(X0,a_2_0_lopclset(X1,X2))
<=> ? [X3] :
( m1_filter_0(X3,X1)
& X0 = X3
& v1_filter_0(X3,X1)
& r2_hidden(X2,X3) ) )
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ v17_lattices(X1)
| v3_realset2(X1)
| ~ l3_lattices(X1)
| ~ m1_subset_1(X2,u1_struct_0(X1)) ),
inference(ennf_transformation,[],[f12331]) ).
fof(f12447,plain,
! [X0,X1,X2] :
( ( r2_hidden(X0,a_2_0_lopclset(X1,X2))
<=> ? [X3] :
( m1_filter_0(X3,X1)
& X0 = X3
& v1_filter_0(X3,X1)
& r2_hidden(X2,X3) ) )
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ v17_lattices(X1)
| v3_realset2(X1)
| ~ l3_lattices(X1)
| ~ m1_subset_1(X2,u1_struct_0(X1)) ),
inference(flattening,[],[f12446]) ).
fof(f12532,plain,
! [X0,X1] :
( ( r2_hidden(X0,k7_lopclset(X1))
<=> ? [X2] :
( m1_filter_0(X2,X1)
& X2 = X0
& v1_filter_0(X2,X1) ) )
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ v17_lattices(X1)
| v3_realset2(X1)
| ~ l3_lattices(X1) ),
inference(ennf_transformation,[],[f12378]) ).
fof(f12533,plain,
! [X0,X1] :
( ( r2_hidden(X0,k7_lopclset(X1))
<=> ? [X2] :
( m1_filter_0(X2,X1)
& X2 = X0
& v1_filter_0(X2,X1) ) )
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ v17_lattices(X1)
| v3_realset2(X1)
| ~ l3_lattices(X1) ),
inference(flattening,[],[f12532]) ).
fof(f12534,plain,
? [X0] :
( ? [X1] :
( ~ r1_tarski(a_2_0_lopclset(X0,X1),k7_lopclset(X0))
& m1_subset_1(X1,u1_struct_0(X0)) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& ~ v3_realset2(X0)
& l3_lattices(X0) ),
inference(ennf_transformation,[],[f12380]) ).
fof(f12535,plain,
? [X0] :
( ? [X1] :
( ~ r1_tarski(a_2_0_lopclset(X0,X1),k7_lopclset(X0))
& m1_subset_1(X1,u1_struct_0(X0)) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& ~ v3_realset2(X0)
& l3_lattices(X0) ),
inference(flattening,[],[f12534]) ).
fof(f12919,plain,
! [X0,X1] :
( r1_tarski(X0,X1)
<=> ! [X2] :
( r2_hidden(X2,X1)
| ~ r2_hidden(X2,X0) ) ),
inference(ennf_transformation,[],[f8]) ).
fof(f12923,plain,
! [X0,X1,X2] :
( ( ( r2_hidden(X0,a_2_0_lopclset(X1,X2))
| ! [X3] :
( ~ m1_filter_0(X3,X1)
| X0 != X3
| ~ v1_filter_0(X3,X1)
| ~ r2_hidden(X2,X3) ) )
& ( ? [X3] :
( m1_filter_0(X3,X1)
& X0 = X3
& v1_filter_0(X3,X1)
& r2_hidden(X2,X3) )
| ~ r2_hidden(X0,a_2_0_lopclset(X1,X2)) ) )
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ v17_lattices(X1)
| v3_realset2(X1)
| ~ l3_lattices(X1)
| ~ m1_subset_1(X2,u1_struct_0(X1)) ),
inference(nnf_transformation,[],[f12447]) ).
fof(f12924,plain,
! [X0,X1,X2] :
( ( ( r2_hidden(X0,a_2_0_lopclset(X1,X2))
| ! [X3] :
( ~ m1_filter_0(X3,X1)
| X0 != X3
| ~ v1_filter_0(X3,X1)
| ~ r2_hidden(X2,X3) ) )
& ( ? [X4] :
( m1_filter_0(X4,X1)
& X0 = X4
& v1_filter_0(X4,X1)
& r2_hidden(X2,X4) )
| ~ r2_hidden(X0,a_2_0_lopclset(X1,X2)) ) )
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ v17_lattices(X1)
| v3_realset2(X1)
| ~ l3_lattices(X1)
| ~ m1_subset_1(X2,u1_struct_0(X1)) ),
inference(rectify,[],[f12923]) ).
fof(f12925,plain,
! [X0,X1,X2] :
( ( ( r2_hidden(X0,a_2_0_lopclset(X1,X2))
| ! [X3] :
( ~ m1_filter_0(X3,X1)
| X0 != X3
| ~ v1_filter_0(X3,X1)
| ~ r2_hidden(X2,X3) ) )
& ( ( m1_filter_0(sK1(X0,X1,X2),X1)
& sK1(X0,X1,X2) = X0
& v1_filter_0(sK1(X0,X1,X2),X1)
& r2_hidden(X2,sK1(X0,X1,X2)) )
| ~ r2_hidden(X0,a_2_0_lopclset(X1,X2)) ) )
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ v17_lattices(X1)
| v3_realset2(X1)
| ~ l3_lattices(X1)
| ~ m1_subset_1(X2,u1_struct_0(X1)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(X4,sK1(X0,X1,X2))],[f12924]) ).
fof(f12933,plain,
! [X0,X1] :
( ( ( r2_hidden(X0,k7_lopclset(X1))
| ! [X2] :
( ~ m1_filter_0(X2,X1)
| X0 != X2
| ~ v1_filter_0(X2,X1) ) )
& ( ? [X2] :
( m1_filter_0(X2,X1)
& X2 = X0
& v1_filter_0(X2,X1) )
| ~ r2_hidden(X0,k7_lopclset(X1)) ) )
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ v17_lattices(X1)
| v3_realset2(X1)
| ~ l3_lattices(X1) ),
inference(nnf_transformation,[],[f12533]) ).
fof(f12934,plain,
! [X0,X1] :
( ( ( r2_hidden(X0,k7_lopclset(X1))
| ! [X2] :
( ~ m1_filter_0(X2,X1)
| X0 != X2
| ~ v1_filter_0(X2,X1) ) )
& ( ? [X3] :
( m1_filter_0(X3,X1)
& X0 = X3
& v1_filter_0(X3,X1) )
| ~ r2_hidden(X0,k7_lopclset(X1)) ) )
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ v17_lattices(X1)
| v3_realset2(X1)
| ~ l3_lattices(X1) ),
inference(rectify,[],[f12933]) ).
fof(f12935,plain,
! [X0,X1] :
( ( ( r2_hidden(X0,k7_lopclset(X1))
| ! [X2] :
( ~ m1_filter_0(X2,X1)
| X0 != X2
| ~ v1_filter_0(X2,X1) ) )
& ( ( m1_filter_0(sK7(X0,X1),X1)
& sK7(X0,X1) = X0
& v1_filter_0(sK7(X0,X1),X1) )
| ~ r2_hidden(X0,k7_lopclset(X1)) ) )
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ v17_lattices(X1)
| v3_realset2(X1)
| ~ l3_lattices(X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(X3,sK7(X0,X1))],[f12934]) ).
fof(f12936,plain,
( ~ r1_tarski(a_2_0_lopclset(sK8,sK9),k7_lopclset(sK8))
& m1_subset_1(sK9,u1_struct_0(sK8))
& ~ v3_struct_0(sK8)
& v10_lattices(sK8)
& v17_lattices(sK8)
& ~ v3_realset2(sK8)
& l3_lattices(sK8) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8,sK9]),skolemize(X0,sK8),skolemize(X1,sK9)],[f12535]) ).
fof(f13095,plain,
! [X0,X1] :
( ( r1_tarski(X0,X1)
| ? [X2] :
( ~ r2_hidden(X2,X1)
& r2_hidden(X2,X0) ) )
& ( ! [X2] :
( r2_hidden(X2,X1)
| ~ r2_hidden(X2,X0) )
| ~ r1_tarski(X0,X1) ) ),
inference(nnf_transformation,[],[f12919]) ).
fof(f13096,plain,
! [X0,X1] :
( ( r1_tarski(X0,X1)
| ? [X2] :
( ~ r2_hidden(X2,X1)
& r2_hidden(X2,X0) ) )
& ( ! [X3] :
( r2_hidden(X3,X1)
| ~ r2_hidden(X3,X0) )
| ~ r1_tarski(X0,X1) ) ),
inference(rectify,[],[f13095]) ).
fof(f13097,plain,
! [X0,X1] :
( ( r1_tarski(X0,X1)
| ( ~ r2_hidden(sK104(X0,X1),X1)
& r2_hidden(sK104(X0,X1),X0) ) )
& ( ! [X3] :
( r2_hidden(X3,X1)
| ~ r2_hidden(X3,X0) )
| ~ r1_tarski(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK104]),skolemize(X2,sK104(X0,X1))],[f13096]) ).
fof(f13103,plain,
! [X2,X0,X1] :
( v1_filter_0(sK1(X0,X1,X2),X1)
| ~ r2_hidden(X0,a_2_0_lopclset(X1,X2))
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ v17_lattices(X1)
| v3_realset2(X1)
| ~ l3_lattices(X1)
| ~ m1_subset_1(X2,u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f12925]) ).
fof(f13104,plain,
! [X2,X0,X1] :
( sK1(X0,X1,X2) = X0
| ~ r2_hidden(X0,a_2_0_lopclset(X1,X2))
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ v17_lattices(X1)
| v3_realset2(X1)
| ~ l3_lattices(X1)
| ~ m1_subset_1(X2,u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f12925]) ).
fof(f13105,plain,
! [X2,X0,X1] :
( m1_filter_0(sK1(X0,X1,X2),X1)
| ~ r2_hidden(X0,a_2_0_lopclset(X1,X2))
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ v17_lattices(X1)
| v3_realset2(X1)
| ~ l3_lattices(X1)
| ~ m1_subset_1(X2,u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f12925]) ).
fof(f13189,plain,
! [X2,X0,X1] :
( r2_hidden(X0,k7_lopclset(X1))
| ~ m1_filter_0(X2,X1)
| X0 != X2
| ~ v1_filter_0(X2,X1)
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ v17_lattices(X1)
| v3_realset2(X1)
| ~ l3_lattices(X1) ),
inference(cnf_transformation,[],[f12935]) ).
fof(f13190,plain,
l3_lattices(sK8),
inference(cnf_transformation,[],[f12936]) ).
fof(f13191,plain,
~ v3_realset2(sK8),
inference(cnf_transformation,[],[f12936]) ).
fof(f13192,plain,
v17_lattices(sK8),
inference(cnf_transformation,[],[f12936]) ).
fof(f13193,plain,
v10_lattices(sK8),
inference(cnf_transformation,[],[f12936]) ).
fof(f13194,plain,
~ v3_struct_0(sK8),
inference(cnf_transformation,[],[f12936]) ).
fof(f13195,plain,
m1_subset_1(sK9,u1_struct_0(sK8)),
inference(cnf_transformation,[],[f12936]) ).
fof(f13196,plain,
~ r1_tarski(a_2_0_lopclset(sK8,sK9),k7_lopclset(sK8)),
inference(cnf_transformation,[],[f12936]) ).
fof(f13883,plain,
! [X0,X1] :
( r1_tarski(X0,X1)
| r2_hidden(sK104(X0,X1),X0) ),
inference(cnf_transformation,[],[f13097]) ).
fof(f13884,plain,
! [X0,X1] :
( r1_tarski(X0,X1)
| ~ r2_hidden(sK104(X0,X1),X1) ),
inference(cnf_transformation,[],[f13097]) ).
fof(f13893,plain,
! [X2,X1] :
( r2_hidden(X2,k7_lopclset(X1))
| ~ m1_filter_0(X2,X1)
| ~ v1_filter_0(X2,X1)
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ v17_lattices(X1)
| v3_realset2(X1)
| ~ l3_lattices(X1) ),
inference(equality_resolution,[],[f13189]) ).
fof(f13985,definition,
( spl124_1
<=> v3_realset2(sK8) ),
introduced(definition,[new_symbols(definition,[spl124_1])],[avatar_definition]) ).
fof(f13987,plain,
( ~ v3_realset2(sK8)
| spl124_1 ),
inference(avatar_component_clause,[],[f13985]) ).
fof(f13988,plain,
~ spl124_1,
inference(avatar_split_clause,[],[f13191,f13985]) ).
fof(f13990,definition,
( spl124_2
<=> v3_struct_0(sK8) ),
introduced(definition,[new_symbols(definition,[spl124_2])],[avatar_definition]) ).
fof(f13992,plain,
( ~ v3_struct_0(sK8)
| spl124_2 ),
inference(avatar_component_clause,[],[f13990]) ).
fof(f13993,plain,
~ spl124_2,
inference(avatar_split_clause,[],[f13194,f13990]) ).
fof(f13995,definition,
( spl124_3
<=> l3_lattices(sK8) ),
introduced(definition,[new_symbols(definition,[spl124_3])],[avatar_definition]) ).
fof(f13997,plain,
( l3_lattices(sK8)
| ~ spl124_3 ),
inference(avatar_component_clause,[],[f13995]) ).
fof(f13998,plain,
spl124_3,
inference(avatar_split_clause,[],[f13190,f13995]) ).
fof(f14000,definition,
( spl124_4
<=> r1_tarski(a_2_0_lopclset(sK8,sK9),k7_lopclset(sK8)) ),
introduced(definition,[new_symbols(definition,[spl124_4])],[avatar_definition]) ).
fof(f14002,plain,
( ~ r1_tarski(a_2_0_lopclset(sK8,sK9),k7_lopclset(sK8))
| spl124_4 ),
inference(avatar_component_clause,[],[f14000]) ).
fof(f14003,plain,
~ spl124_4,
inference(avatar_split_clause,[],[f13196,f14000]) ).
fof(f14005,definition,
( spl124_5
<=> v10_lattices(sK8) ),
introduced(definition,[new_symbols(definition,[spl124_5])],[avatar_definition]) ).
fof(f14007,plain,
( v10_lattices(sK8)
| ~ spl124_5 ),
inference(avatar_component_clause,[],[f14005]) ).
fof(f14008,plain,
spl124_5,
inference(avatar_split_clause,[],[f13193,f14005]) ).
fof(f14029,plain,
( r2_hidden(sK104(a_2_0_lopclset(sK8,sK9),k7_lopclset(sK8)),a_2_0_lopclset(sK8,sK9))
| spl124_4 ),
inference(resolution,[],[f14002,f13883]) ).
fof(f14030,plain,
( ~ r2_hidden(sK104(a_2_0_lopclset(sK8,sK9),k7_lopclset(sK8)),k7_lopclset(sK8))
| spl124_4 ),
inference(resolution,[],[f14002,f13884]) ).
fof(f14033,definition,
( spl124_6
<=> r2_hidden(sK104(a_2_0_lopclset(sK8,sK9),k7_lopclset(sK8)),a_2_0_lopclset(sK8,sK9)) ),
introduced(definition,[new_symbols(definition,[spl124_6])],[avatar_definition]) ).
fof(f14035,plain,
( r2_hidden(sK104(a_2_0_lopclset(sK8,sK9),k7_lopclset(sK8)),a_2_0_lopclset(sK8,sK9))
| ~ spl124_6 ),
inference(avatar_component_clause,[],[f14033]) ).
fof(f14036,plain,
( spl124_6
| spl124_4 ),
inference(avatar_split_clause,[],[f14029,f14000,f14033]) ).
fof(f14038,definition,
( spl124_7
<=> m1_subset_1(sK9,u1_struct_0(sK8)) ),
introduced(definition,[new_symbols(definition,[spl124_7])],[avatar_definition]) ).
fof(f14040,plain,
( m1_subset_1(sK9,u1_struct_0(sK8))
| ~ spl124_7 ),
inference(avatar_component_clause,[],[f14038]) ).
fof(f14041,plain,
spl124_7,
inference(avatar_split_clause,[],[f13195,f14038]) ).
fof(f14759,plain,
( v1_filter_0(sK1(sK104(a_2_0_lopclset(sK8,sK9),k7_lopclset(sK8)),sK8,sK9),sK8)
| v3_struct_0(sK8)
| ~ v10_lattices(sK8)
| ~ v17_lattices(sK8)
| v3_realset2(sK8)
| ~ l3_lattices(sK8)
| ~ m1_subset_1(sK9,u1_struct_0(sK8))
| ~ spl124_6 ),
inference(resolution,[],[f14035,f13103]) ).
fof(f14760,plain,
( sK104(a_2_0_lopclset(sK8,sK9),k7_lopclset(sK8)) = sK1(sK104(a_2_0_lopclset(sK8,sK9),k7_lopclset(sK8)),sK8,sK9)
| v3_struct_0(sK8)
| ~ v10_lattices(sK8)
| ~ v17_lattices(sK8)
| v3_realset2(sK8)
| ~ l3_lattices(sK8)
| ~ m1_subset_1(sK9,u1_struct_0(sK8))
| ~ spl124_6 ),
inference(resolution,[],[f14035,f13104]) ).
fof(f14818,plain,
( sK104(a_2_0_lopclset(sK8,sK9),k7_lopclset(sK8)) = sK1(sK104(a_2_0_lopclset(sK8,sK9),k7_lopclset(sK8)),sK8,sK9)
| ~ v10_lattices(sK8)
| ~ v17_lattices(sK8)
| v3_realset2(sK8)
| ~ l3_lattices(sK8)
| ~ m1_subset_1(sK9,u1_struct_0(sK8))
| spl124_2
| ~ spl124_6 ),
inference(forward_subsumption_resolution,[],[f14760,f13992]) ).
fof(f14819,plain,
( v1_filter_0(sK1(sK104(a_2_0_lopclset(sK8,sK9),k7_lopclset(sK8)),sK8,sK9),sK8)
| ~ v10_lattices(sK8)
| ~ v17_lattices(sK8)
| v3_realset2(sK8)
| ~ l3_lattices(sK8)
| ~ m1_subset_1(sK9,u1_struct_0(sK8))
| spl124_2
| ~ spl124_6 ),
inference(forward_subsumption_resolution,[],[f14759,f13992]) ).
fof(f14824,plain,
( sK104(a_2_0_lopclset(sK8,sK9),k7_lopclset(sK8)) = sK1(sK104(a_2_0_lopclset(sK8,sK9),k7_lopclset(sK8)),sK8,sK9)
| ~ v17_lattices(sK8)
| v3_realset2(sK8)
| ~ l3_lattices(sK8)
| ~ m1_subset_1(sK9,u1_struct_0(sK8))
| spl124_2
| ~ spl124_5
| ~ spl124_6 ),
inference(forward_subsumption_resolution,[],[f14818,f14007]) ).
fof(f14825,plain,
( v1_filter_0(sK1(sK104(a_2_0_lopclset(sK8,sK9),k7_lopclset(sK8)),sK8,sK9),sK8)
| ~ v17_lattices(sK8)
| v3_realset2(sK8)
| ~ l3_lattices(sK8)
| ~ m1_subset_1(sK9,u1_struct_0(sK8))
| spl124_2
| ~ spl124_5
| ~ spl124_6 ),
inference(forward_subsumption_resolution,[],[f14819,f14007]) ).
fof(f14830,plain,
( sK104(a_2_0_lopclset(sK8,sK9),k7_lopclset(sK8)) = sK1(sK104(a_2_0_lopclset(sK8,sK9),k7_lopclset(sK8)),sK8,sK9)
| v3_realset2(sK8)
| ~ l3_lattices(sK8)
| ~ m1_subset_1(sK9,u1_struct_0(sK8))
| spl124_2
| ~ spl124_5
| ~ spl124_6 ),
inference(forward_subsumption_resolution,[],[f14824,f13192]) ).
fof(f14831,plain,
( v1_filter_0(sK1(sK104(a_2_0_lopclset(sK8,sK9),k7_lopclset(sK8)),sK8,sK9),sK8)
| v3_realset2(sK8)
| ~ l3_lattices(sK8)
| ~ m1_subset_1(sK9,u1_struct_0(sK8))
| spl124_2
| ~ spl124_5
| ~ spl124_6 ),
inference(forward_subsumption_resolution,[],[f14825,f13192]) ).
fof(f14836,plain,
( sK104(a_2_0_lopclset(sK8,sK9),k7_lopclset(sK8)) = sK1(sK104(a_2_0_lopclset(sK8,sK9),k7_lopclset(sK8)),sK8,sK9)
| ~ l3_lattices(sK8)
| ~ m1_subset_1(sK9,u1_struct_0(sK8))
| spl124_1
| spl124_2
| ~ spl124_5
| ~ spl124_6 ),
inference(forward_subsumption_resolution,[],[f14830,f13987]) ).
fof(f14837,plain,
( v1_filter_0(sK1(sK104(a_2_0_lopclset(sK8,sK9),k7_lopclset(sK8)),sK8,sK9),sK8)
| ~ l3_lattices(sK8)
| ~ m1_subset_1(sK9,u1_struct_0(sK8))
| spl124_1
| spl124_2
| ~ spl124_5
| ~ spl124_6 ),
inference(forward_subsumption_resolution,[],[f14831,f13987]) ).
fof(f14840,plain,
( sK104(a_2_0_lopclset(sK8,sK9),k7_lopclset(sK8)) = sK1(sK104(a_2_0_lopclset(sK8,sK9),k7_lopclset(sK8)),sK8,sK9)
| ~ m1_subset_1(sK9,u1_struct_0(sK8))
| spl124_1
| spl124_2
| ~ spl124_3
| ~ spl124_5
| ~ spl124_6 ),
inference(forward_subsumption_resolution,[],[f14836,f13997]) ).
fof(f14841,plain,
( v1_filter_0(sK1(sK104(a_2_0_lopclset(sK8,sK9),k7_lopclset(sK8)),sK8,sK9),sK8)
| ~ m1_subset_1(sK9,u1_struct_0(sK8))
| spl124_1
| spl124_2
| ~ spl124_3
| ~ spl124_5
| ~ spl124_6 ),
inference(forward_subsumption_resolution,[],[f14837,f13997]) ).
fof(f14844,plain,
( sK104(a_2_0_lopclset(sK8,sK9),k7_lopclset(sK8)) = sK1(sK104(a_2_0_lopclset(sK8,sK9),k7_lopclset(sK8)),sK8,sK9)
| spl124_1
| spl124_2
| ~ spl124_3
| ~ spl124_5
| ~ spl124_6
| ~ spl124_7 ),
inference(forward_subsumption_resolution,[],[f14840,f14040]) ).
fof(f14845,plain,
( v1_filter_0(sK1(sK104(a_2_0_lopclset(sK8,sK9),k7_lopclset(sK8)),sK8,sK9),sK8)
| spl124_1
| spl124_2
| ~ spl124_3
| ~ spl124_5
| ~ spl124_6
| ~ spl124_7 ),
inference(forward_subsumption_resolution,[],[f14841,f14040]) ).
fof(f14847,plain,
( v1_filter_0(sK104(a_2_0_lopclset(sK8,sK9),k7_lopclset(sK8)),sK8)
| spl124_1
| spl124_2
| ~ spl124_3
| ~ spl124_5
| ~ spl124_6
| ~ spl124_7 ),
inference(forward_demodulation,[],[f14845,f14844]) ).
fof(f14850,definition,
( spl124_8
<=> v1_filter_0(sK104(a_2_0_lopclset(sK8,sK9),k7_lopclset(sK8)),sK8) ),
introduced(definition,[new_symbols(definition,[spl124_8])],[avatar_definition]) ).
fof(f14852,plain,
( v1_filter_0(sK104(a_2_0_lopclset(sK8,sK9),k7_lopclset(sK8)),sK8)
| ~ spl124_8 ),
inference(avatar_component_clause,[],[f14850]) ).
fof(f14853,plain,
( spl124_8
| spl124_1
| spl124_2
| ~ spl124_3
| ~ spl124_5
| ~ spl124_6
| ~ spl124_7 ),
inference(avatar_split_clause,[],[f14847,f14038,f14033,f14005,f13995,f13990,f13985,f14850]) ).
fof(f14860,definition,
( spl124_10
<=> sK104(a_2_0_lopclset(sK8,sK9),k7_lopclset(sK8)) = sK1(sK104(a_2_0_lopclset(sK8,sK9),k7_lopclset(sK8)),sK8,sK9) ),
introduced(definition,[new_symbols(definition,[spl124_10])],[avatar_definition]) ).
fof(f14862,plain,
( sK104(a_2_0_lopclset(sK8,sK9),k7_lopclset(sK8)) = sK1(sK104(a_2_0_lopclset(sK8,sK9),k7_lopclset(sK8)),sK8,sK9)
| ~ spl124_10 ),
inference(avatar_component_clause,[],[f14860]) ).
fof(f14863,plain,
( spl124_10
| spl124_1
| spl124_2
| ~ spl124_3
| ~ spl124_5
| ~ spl124_6
| ~ spl124_7 ),
inference(avatar_split_clause,[],[f14844,f14038,f14033,f14005,f13995,f13990,f13985,f14860]) ).
fof(f15968,definition,
( spl124_11
<=> r2_hidden(sK104(a_2_0_lopclset(sK8,sK9),k7_lopclset(sK8)),k7_lopclset(sK8)) ),
introduced(definition,[new_symbols(definition,[spl124_11])],[avatar_definition]) ).
fof(f15970,plain,
( ~ r2_hidden(sK104(a_2_0_lopclset(sK8,sK9),k7_lopclset(sK8)),k7_lopclset(sK8))
| spl124_11 ),
inference(avatar_component_clause,[],[f15968]) ).
fof(f15971,plain,
( ~ spl124_11
| spl124_4 ),
inference(avatar_split_clause,[],[f14030,f14000,f15968]) ).
fof(f15972,plain,
( ~ m1_filter_0(sK104(a_2_0_lopclset(sK8,sK9),k7_lopclset(sK8)),sK8)
| ~ v1_filter_0(sK104(a_2_0_lopclset(sK8,sK9),k7_lopclset(sK8)),sK8)
| v3_struct_0(sK8)
| ~ v10_lattices(sK8)
| ~ v17_lattices(sK8)
| v3_realset2(sK8)
| ~ l3_lattices(sK8)
| spl124_11 ),
inference(resolution,[],[f15970,f13893]) ).
fof(f15996,plain,
( ~ m1_filter_0(sK104(a_2_0_lopclset(sK8,sK9),k7_lopclset(sK8)),sK8)
| v3_struct_0(sK8)
| ~ v10_lattices(sK8)
| ~ v17_lattices(sK8)
| v3_realset2(sK8)
| ~ l3_lattices(sK8)
| ~ spl124_8
| spl124_11 ),
inference(forward_subsumption_resolution,[],[f15972,f14852]) ).
fof(f15999,plain,
( ~ m1_filter_0(sK104(a_2_0_lopclset(sK8,sK9),k7_lopclset(sK8)),sK8)
| ~ v10_lattices(sK8)
| ~ v17_lattices(sK8)
| v3_realset2(sK8)
| ~ l3_lattices(sK8)
| spl124_2
| ~ spl124_8
| spl124_11 ),
inference(forward_subsumption_resolution,[],[f15996,f13992]) ).
fof(f16000,plain,
( ~ m1_filter_0(sK104(a_2_0_lopclset(sK8,sK9),k7_lopclset(sK8)),sK8)
| ~ v17_lattices(sK8)
| v3_realset2(sK8)
| ~ l3_lattices(sK8)
| spl124_2
| ~ spl124_5
| ~ spl124_8
| spl124_11 ),
inference(forward_subsumption_resolution,[],[f15999,f14007]) ).
fof(f16001,plain,
( ~ m1_filter_0(sK104(a_2_0_lopclset(sK8,sK9),k7_lopclset(sK8)),sK8)
| v3_realset2(sK8)
| ~ l3_lattices(sK8)
| spl124_2
| ~ spl124_5
| ~ spl124_8
| spl124_11 ),
inference(forward_subsumption_resolution,[],[f16000,f13192]) ).
fof(f16002,plain,
( ~ m1_filter_0(sK104(a_2_0_lopclset(sK8,sK9),k7_lopclset(sK8)),sK8)
| ~ l3_lattices(sK8)
| spl124_1
| spl124_2
| ~ spl124_5
| ~ spl124_8
| spl124_11 ),
inference(forward_subsumption_resolution,[],[f16001,f13987]) ).
fof(f16003,plain,
( ~ m1_filter_0(sK104(a_2_0_lopclset(sK8,sK9),k7_lopclset(sK8)),sK8)
| spl124_1
| spl124_2
| ~ spl124_3
| ~ spl124_5
| ~ spl124_8
| spl124_11 ),
inference(forward_subsumption_resolution,[],[f16002,f13997]) ).
fof(f16005,definition,
( spl124_12
<=> m1_filter_0(sK104(a_2_0_lopclset(sK8,sK9),k7_lopclset(sK8)),sK8) ),
introduced(definition,[new_symbols(definition,[spl124_12])],[avatar_definition]) ).
fof(f16007,plain,
( ~ m1_filter_0(sK104(a_2_0_lopclset(sK8,sK9),k7_lopclset(sK8)),sK8)
| spl124_12 ),
inference(avatar_component_clause,[],[f16005]) ).
fof(f16008,plain,
( ~ spl124_12
| spl124_1
| spl124_2
| ~ spl124_3
| ~ spl124_5
| ~ spl124_8
| spl124_11 ),
inference(avatar_split_clause,[],[f16003,f15968,f14850,f14005,f13995,f13990,f13985,f16005]) ).
fof(f16348,plain,
( m1_filter_0(sK104(a_2_0_lopclset(sK8,sK9),k7_lopclset(sK8)),sK8)
| ~ r2_hidden(sK104(a_2_0_lopclset(sK8,sK9),k7_lopclset(sK8)),a_2_0_lopclset(sK8,sK9))
| v3_struct_0(sK8)
| ~ v10_lattices(sK8)
| ~ v17_lattices(sK8)
| v3_realset2(sK8)
| ~ l3_lattices(sK8)
| ~ m1_subset_1(sK9,u1_struct_0(sK8))
| ~ spl124_10 ),
inference(superposition,[],[f13105,f14862]) ).
fof(f16349,plain,
( ~ r2_hidden(sK104(a_2_0_lopclset(sK8,sK9),k7_lopclset(sK8)),a_2_0_lopclset(sK8,sK9))
| v3_struct_0(sK8)
| ~ v10_lattices(sK8)
| ~ v17_lattices(sK8)
| v3_realset2(sK8)
| ~ l3_lattices(sK8)
| ~ m1_subset_1(sK9,u1_struct_0(sK8))
| ~ spl124_10
| spl124_12 ),
inference(forward_subsumption_resolution,[],[f16348,f16007]) ).
fof(f16350,plain,
( v3_struct_0(sK8)
| ~ v10_lattices(sK8)
| ~ v17_lattices(sK8)
| v3_realset2(sK8)
| ~ l3_lattices(sK8)
| ~ m1_subset_1(sK9,u1_struct_0(sK8))
| ~ spl124_6
| ~ spl124_10
| spl124_12 ),
inference(forward_subsumption_resolution,[],[f16349,f14035]) ).
fof(f16351,plain,
( ~ v10_lattices(sK8)
| ~ v17_lattices(sK8)
| v3_realset2(sK8)
| ~ l3_lattices(sK8)
| ~ m1_subset_1(sK9,u1_struct_0(sK8))
| spl124_2
| ~ spl124_6
| ~ spl124_10
| spl124_12 ),
inference(forward_subsumption_resolution,[],[f16350,f13992]) ).
fof(f16352,plain,
( ~ v17_lattices(sK8)
| v3_realset2(sK8)
| ~ l3_lattices(sK8)
| ~ m1_subset_1(sK9,u1_struct_0(sK8))
| spl124_2
| ~ spl124_5
| ~ spl124_6
| ~ spl124_10
| spl124_12 ),
inference(forward_subsumption_resolution,[],[f16351,f14007]) ).
fof(f16353,plain,
( v3_realset2(sK8)
| ~ l3_lattices(sK8)
| ~ m1_subset_1(sK9,u1_struct_0(sK8))
| spl124_2
| ~ spl124_5
| ~ spl124_6
| ~ spl124_10
| spl124_12 ),
inference(forward_subsumption_resolution,[],[f16352,f13192]) ).
fof(f16354,plain,
( ~ l3_lattices(sK8)
| ~ m1_subset_1(sK9,u1_struct_0(sK8))
| spl124_1
| spl124_2
| ~ spl124_5
| ~ spl124_6
| ~ spl124_10
| spl124_12 ),
inference(forward_subsumption_resolution,[],[f16353,f13987]) ).
fof(f16355,plain,
( ~ m1_subset_1(sK9,u1_struct_0(sK8))
| spl124_1
| spl124_2
| ~ spl124_3
| ~ spl124_5
| ~ spl124_6
| ~ spl124_10
| spl124_12 ),
inference(forward_subsumption_resolution,[],[f16354,f13997]) ).
fof(f16356,plain,
( $false
| spl124_1
| spl124_2
| ~ spl124_3
| ~ spl124_5
| ~ spl124_6
| ~ spl124_7
| ~ spl124_10
| spl124_12 ),
inference(forward_subsumption_resolution,[],[f16355,f14040]) ).
fof(f16357,plain,
( spl124_1
| spl124_2
| ~ spl124_3
| ~ spl124_5
| ~ spl124_6
| ~ spl124_7
| ~ spl124_10
| spl124_12 ),
inference(avatar_contradiction_clause,[],[f16356]) ).
cnf(s1,plain,
~ spl124_1,
inference(sat_conversion,[],[f13988]) ).
cnf(s2,plain,
~ spl124_2,
inference(sat_conversion,[],[f13993]) ).
cnf(s3,plain,
spl124_3,
inference(sat_conversion,[],[f13998]) ).
cnf(s4,plain,
~ spl124_4,
inference(sat_conversion,[],[f14003]) ).
cnf(s5,plain,
spl124_5,
inference(sat_conversion,[],[f14008]) ).
cnf(s6,plain,
( spl124_4
| spl124_6 ),
inference(sat_conversion,[],[f14036]) ).
cnf(s7,plain,
spl124_7,
inference(sat_conversion,[],[f14041]) ).
cnf(s8,plain,
( spl124_1
| spl124_2
| ~ spl124_3
| ~ spl124_5
| ~ spl124_6
| ~ spl124_7
| spl124_8 ),
inference(sat_conversion,[],[f14853]) ).
cnf(s10,plain,
( spl124_1
| spl124_2
| ~ spl124_3
| ~ spl124_5
| ~ spl124_6
| ~ spl124_7
| spl124_10 ),
inference(sat_conversion,[],[f14863]) ).
cnf(s11,plain,
( spl124_4
| ~ spl124_11 ),
inference(sat_conversion,[],[f15971]) ).
cnf(s12,plain,
( spl124_1
| spl124_2
| ~ spl124_3
| ~ spl124_5
| ~ spl124_8
| spl124_11
| ~ spl124_12 ),
inference(sat_conversion,[],[f16008]) ).
cnf(s13,plain,
( spl124_1
| spl124_2
| ~ spl124_3
| ~ spl124_5
| ~ spl124_6
| ~ spl124_7
| ~ spl124_10
| spl124_12 ),
inference(sat_conversion,[],[f16357]) ).
cnf(s14,plain,
~ spl124_11,
inference(rat,[],[s11,s4]) ).
cnf(s15,plain,
spl124_6,
inference(rat,[],[s6,s4]) ).
cnf(s16,plain,
spl124_10,
inference(rat,[],[s10,s2,s7,s15,s5,s3,s1]) ).
cnf(s18,plain,
spl124_8,
inference(rat,[],[s8,s2,s7,s15,s5,s3,s1]) ).
cnf(s19,plain,
spl124_12,
inference(rat,[],[s13,s1,s2,s7,s15,s5,s3,s16]) ).
cnf(s20,plain,
$false,
inference(rat,[],[s12,s1,s14,s2,s5,s3,s19,s18]) ).
fof(f16358,plain,
$false,
inference(avatar_sat_refutation,[],[s20]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT288+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.14/0.40 % Computer : n026.cluster.edu
% 0.14/0.40 % Model : x86_64 x86_64
% 0.14/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.40 % Memory : 8046.5625MB
% 0.14/0.40 % OS : Linux 6.8.0-71-generic
% 0.14/0.40 % CPULimit : 300
% 0.14/0.40 % WCLimit : 300
% 0.14/0.40 % DateTime : Sun Sep 27 14:17:42 UTC 2026
% 0.14/0.41 % CPUTime :
% 0.14/0.41 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.14/0.46 Running first-order theorem proving
% 0.14/0.46 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.18/4.10 % (2884802)Detected formulas, will run a generic FOF schedule.
% 17.18/4.10 % (2884815)dis-21_1_sil=8000:lcm=predicate:random_seed=2688380854:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2993 on theBenchmark for (2993ds/129Mi)
% 17.18/4.10 % (2884809)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=4037904313:i=141193_2993 on theBenchmark for (2993ds/141193Mi)
% 17.18/4.10 % (2884812)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=542228665:i=109:sd=1:ins=1:gsp=on:ss=axioms_2993 on theBenchmark for (2993ds/109Mi)
% 17.18/4.10 % (2884810)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=2518650698:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2993 on theBenchmark for (2993ds/134677Mi)
% 17.18/4.10 % (2884811)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=3525082710:i=141695:sd=1:nm=32:gsp=on:ss=included_2993 on theBenchmark for (2993ds/141695Mi)
% 17.18/4.10 % (2884814)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=515372480:s2a=on:i=139:gtg=position_2993 on theBenchmark for (2993ds/139Mi)
% 17.18/4.10 % (2884813)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2164642893:i=119:av=off:ss=axioms_2993 on theBenchmark for (2993ds/119Mi)
% 17.18/4.10 % (2884815)Instruction limit reached!
% 17.18/4.10 % (2884815)------------------------------
% 17.18/4.10 % (2884815)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.18/4.10 % (2884815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.18/4.10 % (2884815)CaDiCaL version: 2.1.3
% 17.18/4.10 % (2884815)Termination reason: Instruction limit
% 17.18/4.10 % (2884815)Termination phase: Preprocessing 1
% 17.18/4.10 % (2884815)Time elapsed: 0.095 s
% 17.18/4.10 % (2884815)Peak memory usage: 102 MB
% 17.18/4.10 % (2884815)Instructions burned: 129 (million)
% 17.18/4.10 % (2884812)Refutation not found, incomplete strategy
% 17.18/4.10 % (2884812)------------------------------
% 17.18/4.10 % (2884812)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.18/4.10 % (2884812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.18/4.10 % (2884812)CaDiCaL version: 2.1.3
% 17.18/4.10 % (2884812)Termination reason: Refutation not found, incomplete strategy
% 17.18/4.10 % (2884812)Time elapsed: 0.089 s
% 17.18/4.10 % (2884812)Peak memory usage: 105 MB
% 17.18/4.10 % (2884812)Instructions burned: 74 (million)
% 17.18/4.10 % (2884814)Instruction limit reached!
% 17.18/4.10 % (2884814)------------------------------
% 17.18/4.10 % (2884814)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.18/4.10 % (2884814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.18/4.10 % (2884814)CaDiCaL version: 2.1.3
% 17.18/4.10 % (2884814)Termination reason: Instruction limit
% 17.18/4.10 % (2884814)Termination phase: Property scanning
% 17.18/4.10 % (2884814)Time elapsed: 0.114 s
% 17.18/4.10 % (2884814)Peak memory usage: 100 MB
% 17.18/4.10 % (2884814)Instructions burned: 139 (million)
% 17.18/4.10 % (2884813)Instruction limit reached!
% 17.18/4.10 % (2884813)------------------------------
% 17.18/4.10 % (2884813)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.18/4.10 % (2884813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.18/4.10 % (2884813)CaDiCaL version: 2.1.3
% 17.18/4.10 % (2884813)Termination reason: Instruction limit
% 17.18/4.10 % (2884813)Termination phase: Property scanning
% 17.18/4.10 % (2884813)Time elapsed: 0.140 s
% 17.18/4.10 % (2884813)Peak memory usage: 104 MB
% 17.18/4.10 % (2884813)Instructions burned: 119 (million)
% 17.18/4.10 % (2884823)lrs+10_1_sil=8000:sp=occurrence:random_seed=3662062068:i=285:sd=3:ss=axioms:sgt=8_2990 on theBenchmark for (2990ds/285Mi)
% 17.18/4.10 % (2884824)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2926549887:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2989 on theBenchmark for (2989ds/157Mi)
% 17.18/4.10 % (2884823)Instruction limit reached!
% 17.18/4.10 % (2884823)------------------------------
% 17.18/4.10 % (2884823)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.18/4.10 % (2884823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.18/4.10 % (2884823)CaDiCaL version: 2.1.3
% 17.18/4.10 % (2884823)Termination reason: Instruction limit
% 17.18/4.10 % (2884823)Termination phase: Saturation
% 17.18/4.10 % (2884823)Time elapsed: 0.174 s
% 17.18/4.10 % (2884823)Peak memory usage: 108 MB
% 17.18/4.10 % (2884823)Instructions burned: 285 (million)
% 17.18/4.10 % (2884825)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3458580344:i=325:sd=1:ss=axioms:sgt=32_2989 on theBenchmark for (2989ds/325Mi)
% 17.18/4.10 % (2884812)------------------------------
% 17.18/4.10 % (2884812)------------------------------
% 17.18/4.10 % (2884824)Instruction limit reached!
% 17.18/4.10 % (2884824)------------------------------
% 17.18/4.10 % (2884824)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.18/4.10 % (2884824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.18/4.10 % (2884824)CaDiCaL version: 2.1.3
% 17.18/4.10 % (2884824)Termination reason: Instruction limit
% 17.18/4.10 % (2884824)Termination phase: SInE selection
% 17.18/4.10 % (2884824)Time elapsed: 0.133 s
% 17.18/4.10 % (2884824)Peak memory usage: 101 MB
% 17.18/4.10 % (2884824)Instructions burned: 157 (million)
% 17.18/4.10 % (2884828)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=654558465:s2a=on:i=248:s2at=1.23:gtg=position_2987 on theBenchmark for (2987ds/248Mi)
% 17.18/4.10 % (2884825)Instruction limit reached!
% 17.18/4.10 % (2884825)------------------------------
% 17.18/4.10 % (2884825)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.18/4.10 % (2884825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.18/4.10 % (2884825)CaDiCaL version: 2.1.3
% 17.18/4.10 % (2884825)Termination reason: Instruction limit
% 17.18/4.10 % (2884825)Termination phase: Saturation
% 17.18/4.10 % (2884825)Time elapsed: 0.247 s
% 17.18/4.10 % (2884825)Peak memory usage: 105 MB
% 17.18/4.10 % (2884825)Instructions burned: 325 (million)
% 17.18/4.10 % (2884828)Instruction limit reached!
% 17.18/4.10 % (2884828)------------------------------
% 17.18/4.10 % (2884828)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.18/4.10 % (2884828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.18/4.10 % (2884828)CaDiCaL version: 2.1.3
% 17.18/4.10 % (2884828)Termination reason: Instruction limit
% 17.18/4.10 % (2884828)Termination phase: SInE selection
% 17.18/4.10 % (2884828)Time elapsed: 0.129 s
% 17.18/4.10 % (2884828)Peak memory usage: 101 MB
% 17.18/4.10 % (2884828)Instructions burned: 248 (million)
% 17.18/4.10 % (2884830)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=4069205813:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2986 on theBenchmark for (2986ds/294Mi)
% 17.18/4.10 % (2884831)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1720551647:i=2350_2986 on theBenchmark for (2986ds/2350Mi)
% 17.18/4.10 % (2884834)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=417325392:i=127:av=off:fsr=off:sup=off_2984 on theBenchmark for (2984ds/127Mi)
% 17.18/4.10 % (2884833)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2245774591:cts=off:i=113:fsr=off:ss=included:sgt=4_2984 on theBenchmark for (2984ds/113Mi)
% 17.18/4.10 % (2884834)Instruction limit reached!
% 17.18/4.10 % (2884834)------------------------------
% 17.18/4.10 % (2884834)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.18/4.10 % (2884834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.18/4.10 % (2884834)CaDiCaL version: 2.1.3
% 17.18/4.10 % (2884834)Termination reason: Instruction limit
% 17.18/4.10 % (2884834)Termination phase: Preprocessing 2
% 17.18/4.10 % (2884834)Time elapsed: 0.089 s
% 17.18/4.10 % (2884834)Peak memory usage: 107 MB
% 17.18/4.10 % (2884834)Instructions burned: 127 (million)
% 17.18/4.10 % (2884833)Instruction limit reached!
% 17.18/4.10 % (2884833)------------------------------
% 17.18/4.10 % (2884833)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.18/4.10 % (2884833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.18/4.10 % (2884833)CaDiCaL version: 2.1.3
% 17.18/4.10 % (2884833)Termination reason: Instruction limit
% 17.18/4.10 % (2884833)Termination phase: Preprocessing 3
% 17.18/4.10 % (2884833)Time elapsed: 0.137 s
% 17.18/4.10 % (2884833)Peak memory usage: 104 MB
% 17.18/4.10 % (2884833)Instructions burned: 113 (million)
% 17.18/4.10 % (2884830)Instruction limit reached!
% 17.18/4.10 % (2884830)------------------------------
% 17.18/4.10 % (2884830)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.18/4.10 % (2884830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.18/4.10 % (2884830)CaDiCaL version: 2.1.3
% 17.18/4.10 % (2884830)Termination reason: Instruction limit
% 17.18/4.10 % (2884830)Termination phase: Saturation
% 17.18/4.10 % (2884830)Time elapsed: 0.311 s
% 17.18/4.10 % (2884830)Peak memory usage: 109 MB
% 17.18/4.10 % (2884830)Instructions burned: 295 (million)
% 17.18/4.10 % (2884839)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1066897952:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2982 on theBenchmark for (2982ds/114Mi)
% 17.18/4.10 % (2884839)Instruction limit reached!
% 17.18/4.10 % (2884839)------------------------------
% 17.18/4.10 % (2884839)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.18/4.10 % (2884839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.18/4.10 % (2884839)CaDiCaL version: 2.1.3
% 17.18/4.10 % (2884839)Termination reason: Instruction limit
% 17.18/4.10 % (2884839)Termination phase: Property scanning
% 17.18/4.10 % (2884839)Time elapsed: 0.050 s
% 17.18/4.10 % (2884839)Peak memory usage: 101 MB
% 17.18/4.10 % (2884839)Instructions burned: 117 (million)
% 17.18/4.10 % (2884840)lrs+10_1_sil=8000:sp=occurrence:random_seed=4167758616:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2981 on theBenchmark for (2981ds/907Mi)
% 17.18/4.10 % (2884841)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2978060028:i=437:sd=1:aac=none:ss=included_2981 on theBenchmark for (2981ds/437Mi)
% 17.18/4.10 % (2884843)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3911802118:i=5202:ss=axioms:sgt=16_2980 on theBenchmark for (2980ds/5202Mi)
% 17.18/4.10 % (2884811)First to succeed.
% 17.18/4.10 % (2884811)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2884802"
% 17.18/4.10 % (2884841)Instruction limit reached!
% 17.18/4.10 % (2884841)------------------------------
% 17.18/4.10 % (2884841)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.18/4.10 % (2884841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.18/4.10 % (2884841)CaDiCaL version: 2.1.3
% 17.18/4.10 % (2884841)Termination reason: Instruction limit
% 17.18/4.10 % (2884841)Termination phase: Saturation
% 17.18/4.10 % (2884841)Time elapsed: 0.447 s
% 17.18/4.10 % (2884841)Peak memory usage: 108 MB
% 17.18/4.10 % (2884841)Instructions burned: 437 (million)
% 17.18/4.10 % (2884847)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2491174310:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2974 on theBenchmark for (2974ds/134Mi)
% 17.18/4.10 % (2884847)Instruction limit reached!
% 17.18/4.10 % (2884847)------------------------------
% 17.18/4.10 % (2884847)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.18/4.10 % (2884847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.18/4.10 % (2884847)CaDiCaL version: 2.1.3
% 17.18/4.10 % (2884847)Termination reason: Instruction limit
% 17.18/4.10 % (2884847)Termination phase: Property scanning
% 17.18/4.10 % (2884847)Time elapsed: 0.152 s
% 17.18/4.10 % (2884847)Peak memory usage: 104 MB
% 17.18/4.10 % (2884847)Instructions burned: 134 (million)
% 17.18/4.10 % (2884811)Refutation found. Thanks to Tanya!
% 17.18/4.10 % SZS status Theorem for theBenchmark
% 17.18/4.10 % SZS output start Proof for theBenchmark
% See solution above
% 17.77/4.32 % (2884811)------------------------------
% 17.77/4.32 % (2884811)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.77/4.32 % (2884811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.77/4.32 % (2884811)CaDiCaL version: 2.1.3
% 17.77/4.32 % (2884811)Termination reason: Refutation
% 17.77/4.32 % (2884811)Time elapsed: 1.575 s
% 17.77/4.32 % (2884811)Peak memory usage: 158 MB
% 17.77/4.32 % (2884811)Instructions burned: 1556 (million)
% 17.77/4.32 % (2884811)------------------------------
% 17.77/4.32 % (2884811)------------------------------
% 17.77/4.32 % (2884802)Success in time 2.972 s
% 17.77/4.32 % Vampire exiting
%------------------------------------------------------------------------------