%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT310+4 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n012.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:47 AM UTC 2026
% Result : Theorem 17.14s 4.00s
% Output : Refutation 19.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 10
% Syntax : Number of formulae : 107 ( 22 unt; 3 def)
% Number of atoms : 506 ( 27 equ)
% Maximal formula atoms : 16 ( 4 avg)
% Number of connectives : 661 ( 262 ~; 296 |; 76 &)
% ( 6 <=>; 21 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 13 ( 11 usr; 4 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 4 con; 0-3 aty)
% Number of variables : 132 ( 1 sgn 121 !; 11 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f18,axiom,
! [X0,X1] : r1_tarski(X0,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reflexivity_r1_tarski) ).
fof(f70,axiom,
! [X0,X1,X2] :
( ( r1_tarski(X0,X1)
& r1_tarski(X1,X2) )
=> r1_tarski(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_xboole_1) ).
fof(f31985,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_lattice4(X1,X0)
=> m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m2_lattice4) ).
fof(f34607,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_filter_2(X1,X0)
=> ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m2_filter_2) ).
fof(f34642,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
=> m2_filter_2(k19_filter_2(X0,X1),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k19_filter_2) ).
fof(f34698,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( ( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
=> ! [X2] :
( m2_filter_2(X2,X0)
=> ( X2 = k19_filter_2(X0,X1)
<=> ( r1_tarski(X1,X2)
& ! [X3] :
( m2_filter_2(X3,X0)
=> ( r1_tarski(X1,X3)
=> r1_tarski(X2,X3) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d11_filter_2) ).
fof(f34702,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( ( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
=> ! [X2] :
( ( ~ v1_xboole_0(X2)
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
=> ! [X3] :
( ( ~ v1_xboole_0(X3)
& m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) )
=> ( ( r1_tarski(X2,X3)
=> r1_tarski(k19_filter_2(X0,X2),k19_filter_2(X0,X3)) )
& r1_tarski(k19_filter_2(X0,k19_filter_2(X0,X1)),k19_filter_2(X0,X1)) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t39_filter_2) ).
fof(f34703,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( ( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
=> ! [X2] :
( ( ~ v1_xboole_0(X2)
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
=> ! [X3] :
( ( ~ v1_xboole_0(X3)
& m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) )
=> ( ( r1_tarski(X2,X3)
=> r1_tarski(k19_filter_2(X0,X2),k19_filter_2(X0,X3)) )
& r1_tarski(k19_filter_2(X0,k19_filter_2(X0,X1)),k19_filter_2(X0,X1)) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f34702]) ).
fof(f34704,plain,
! [X0] : r1_tarski(X0,X0),
inference(rectify,[],[f18]) ).
fof(f34831,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( ( ( ~ r1_tarski(k19_filter_2(X0,X2),k19_filter_2(X0,X3))
& r1_tarski(X2,X3) )
| ~ r1_tarski(k19_filter_2(X0,k19_filter_2(X0,X1)),k19_filter_2(X0,X1)) )
& ~ v1_xboole_0(X3)
& m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) )
& ~ v1_xboole_0(X2)
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
& ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(ennf_transformation,[],[f34703]) ).
fof(f34832,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( ( ( ~ r1_tarski(k19_filter_2(X0,X2),k19_filter_2(X0,X3))
& r1_tarski(X2,X3) )
| ~ r1_tarski(k19_filter_2(X0,k19_filter_2(X0,X1)),k19_filter_2(X0,X1)) )
& ~ v1_xboole_0(X3)
& m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) )
& ~ v1_xboole_0(X2)
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
& ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(flattening,[],[f34831]) ).
fof(f34918,plain,
! [X0,X1,X2] :
( r1_tarski(X0,X2)
| ~ r1_tarski(X0,X1)
| ~ r1_tarski(X1,X2) ),
inference(ennf_transformation,[],[f70]) ).
fof(f34919,plain,
! [X0,X1,X2] :
( r1_tarski(X0,X2)
| ~ r1_tarski(X0,X1)
| ~ r1_tarski(X1,X2) ),
inference(flattening,[],[f34918]) ).
fof(f34962,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( X2 = k19_filter_2(X0,X1)
<=> ( r1_tarski(X1,X2)
& ! [X3] :
( r1_tarski(X2,X3)
| ~ r1_tarski(X1,X3)
| ~ m2_filter_2(X3,X0) ) ) )
| ~ m2_filter_2(X2,X0) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f34698]) ).
fof(f34963,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( X2 = k19_filter_2(X0,X1)
<=> ( r1_tarski(X1,X2)
& ! [X3] :
( r1_tarski(X2,X3)
| ~ r1_tarski(X1,X3)
| ~ m2_filter_2(X3,X0) ) ) )
| ~ m2_filter_2(X2,X0) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f34962]) ).
fof(f34964,plain,
! [X0,X1] :
( m2_filter_2(k19_filter_2(X0,X1),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ),
inference(ennf_transformation,[],[f34642]) ).
fof(f34965,plain,
! [X0,X1] :
( m2_filter_2(k19_filter_2(X0,X1),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ),
inference(flattening,[],[f34964]) ).
fof(f35549,plain,
! [X0] :
( ! [X1] :
( ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f34607]) ).
fof(f35550,plain,
! [X0] :
( ! [X1] :
( ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35549]) ).
fof(f37476,plain,
! [X0] :
( ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m2_lattice4(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f31985]) ).
fof(f37477,plain,
! [X0] :
( ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m2_lattice4(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f37476]) ).
fof(f38224,plain,
( ( ( ~ r1_tarski(k19_filter_2(sK56,sK58),k19_filter_2(sK56,sK59))
& r1_tarski(sK58,sK59) )
| ~ r1_tarski(k19_filter_2(sK56,k19_filter_2(sK56,sK57)),k19_filter_2(sK56,sK57)) )
& ~ v1_xboole_0(sK59)
& m1_subset_1(sK59,k1_zfmisc_1(u1_struct_0(sK56)))
& ~ v1_xboole_0(sK58)
& m1_subset_1(sK58,k1_zfmisc_1(u1_struct_0(sK56)))
& ~ v1_xboole_0(sK57)
& m1_subset_1(sK57,k1_zfmisc_1(u1_struct_0(sK56)))
& ~ v3_struct_0(sK56)
& v10_lattices(sK56)
& l3_lattices(sK56) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK56,sK57,sK58,sK59]),skolemize(X0,sK56),skolemize(X1,sK57),skolemize(X2,sK58),skolemize(X3,sK59)],[f34832]) ).
fof(f38278,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( X2 = k19_filter_2(X0,X1)
| ~ r1_tarski(X1,X2)
| ? [X3] :
( ~ r1_tarski(X2,X3)
& r1_tarski(X1,X3)
& m2_filter_2(X3,X0) ) )
& ( ( r1_tarski(X1,X2)
& ! [X3] :
( r1_tarski(X2,X3)
| ~ r1_tarski(X1,X3)
| ~ m2_filter_2(X3,X0) ) )
| k19_filter_2(X0,X1) != X2 ) )
| ~ m2_filter_2(X2,X0) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f34963]) ).
fof(f38279,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( X2 = k19_filter_2(X0,X1)
| ~ r1_tarski(X1,X2)
| ? [X3] :
( ~ r1_tarski(X2,X3)
& r1_tarski(X1,X3)
& m2_filter_2(X3,X0) ) )
& ( ( r1_tarski(X1,X2)
& ! [X3] :
( r1_tarski(X2,X3)
| ~ r1_tarski(X1,X3)
| ~ m2_filter_2(X3,X0) ) )
| k19_filter_2(X0,X1) != X2 ) )
| ~ m2_filter_2(X2,X0) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f38278]) ).
fof(f38280,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( X2 = k19_filter_2(X0,X1)
| ~ r1_tarski(X1,X2)
| ? [X3] :
( ~ r1_tarski(X2,X3)
& r1_tarski(X1,X3)
& m2_filter_2(X3,X0) ) )
& ( ( r1_tarski(X1,X2)
& ! [X4] :
( r1_tarski(X2,X4)
| ~ r1_tarski(X1,X4)
| ~ m2_filter_2(X4,X0) ) )
| k19_filter_2(X0,X1) != X2 ) )
| ~ m2_filter_2(X2,X0) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(rectify,[],[f38279]) ).
fof(f38281,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( X2 = k19_filter_2(X0,X1)
| ~ r1_tarski(X1,X2)
| ( ~ r1_tarski(X2,sK91(X0,X1,X2))
& r1_tarski(X1,sK91(X0,X1,X2))
& m2_filter_2(sK91(X0,X1,X2),X0) ) )
& ( ( r1_tarski(X1,X2)
& ! [X4] :
( r1_tarski(X2,X4)
| ~ r1_tarski(X1,X4)
| ~ m2_filter_2(X4,X0) ) )
| k19_filter_2(X0,X1) != X2 ) )
| ~ m2_filter_2(X2,X0) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK91]),skolemize(X3,sK91(X0,X1,X2))],[f38280]) ).
fof(f39256,plain,
l3_lattices(sK56),
inference(cnf_transformation,[],[f38224]) ).
fof(f39257,plain,
v10_lattices(sK56),
inference(cnf_transformation,[],[f38224]) ).
fof(f39258,plain,
~ v3_struct_0(sK56),
inference(cnf_transformation,[],[f38224]) ).
fof(f39259,plain,
m1_subset_1(sK57,k1_zfmisc_1(u1_struct_0(sK56))),
inference(cnf_transformation,[],[f38224]) ).
fof(f39260,plain,
~ v1_xboole_0(sK57),
inference(cnf_transformation,[],[f38224]) ).
fof(f39261,plain,
m1_subset_1(sK58,k1_zfmisc_1(u1_struct_0(sK56))),
inference(cnf_transformation,[],[f38224]) ).
fof(f39262,plain,
~ v1_xboole_0(sK58),
inference(cnf_transformation,[],[f38224]) ).
fof(f39263,plain,
m1_subset_1(sK59,k1_zfmisc_1(u1_struct_0(sK56))),
inference(cnf_transformation,[],[f38224]) ).
fof(f39264,plain,
~ v1_xboole_0(sK59),
inference(cnf_transformation,[],[f38224]) ).
fof(f39265,plain,
( r1_tarski(sK58,sK59)
| ~ r1_tarski(k19_filter_2(sK56,k19_filter_2(sK56,sK57)),k19_filter_2(sK56,sK57)) ),
inference(cnf_transformation,[],[f38224]) ).
fof(f39266,plain,
( ~ r1_tarski(k19_filter_2(sK56,sK58),k19_filter_2(sK56,sK59))
| ~ r1_tarski(k19_filter_2(sK56,k19_filter_2(sK56,sK57)),k19_filter_2(sK56,sK57)) ),
inference(cnf_transformation,[],[f38224]) ).
fof(f39386,plain,
! [X2,X0,X1] :
( ~ r1_tarski(X1,X2)
| ~ r1_tarski(X0,X1)
| r1_tarski(X0,X2) ),
inference(cnf_transformation,[],[f34919]) ).
fof(f39390,plain,
! [X0] : r1_tarski(X0,X0),
inference(cnf_transformation,[],[f34704]) ).
fof(f39461,plain,
! [X2,X0,X1,X4] :
( r1_tarski(X2,X4)
| ~ r1_tarski(X1,X4)
| ~ m2_filter_2(X4,X0)
| k19_filter_2(X0,X1) != X2
| ~ m2_filter_2(X2,X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f38281]) ).
fof(f39462,plain,
! [X2,X0,X1] :
( r1_tarski(X1,X2)
| k19_filter_2(X0,X1) != X2
| ~ m2_filter_2(X2,X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f38281]) ).
fof(f39464,plain,
! [X2,X0,X1] :
( r1_tarski(X1,sK91(X0,X1,X2))
| ~ r1_tarski(X1,X2)
| k19_filter_2(X0,X1) = X2
| ~ m2_filter_2(X2,X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f38281]) ).
fof(f39465,plain,
! [X2,X0,X1] :
( ~ r1_tarski(X2,sK91(X0,X1,X2))
| ~ r1_tarski(X1,X2)
| k19_filter_2(X0,X1) = X2
| ~ m2_filter_2(X2,X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f38281]) ).
fof(f39466,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v1_xboole_0(X1)
| m2_filter_2(k19_filter_2(X0,X1),X0) ),
inference(cnf_transformation,[],[f34965]) ).
fof(f40336,plain,
! [X0,X1] :
( m2_lattice4(X1,X0)
| ~ m2_filter_2(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35550]) ).
fof(f40337,plain,
! [X0,X1] :
( ~ m2_filter_2(X1,X0)
| ~ v1_xboole_0(X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35550]) ).
fof(f42736,plain,
! [X0,X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f37477]) ).
fof(f44570,plain,
! [X0,X1] :
( r1_tarski(X1,k19_filter_2(X0,X1))
| ~ m2_filter_2(k19_filter_2(X0,X1),X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(equality_resolution,[],[f39462]) ).
fof(f44571,plain,
! [X0,X1,X4] :
( r1_tarski(k19_filter_2(X0,X1),X4)
| ~ r1_tarski(X1,X4)
| ~ m2_filter_2(X4,X0)
| ~ m2_filter_2(k19_filter_2(X0,X1),X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(equality_resolution,[],[f39461]) ).
fof(f45288,plain,
! [X0,X1,X4] :
( ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ r1_tarski(X1,X4)
| ~ m2_filter_2(X4,X0)
| v1_xboole_0(X1)
| r1_tarski(k19_filter_2(X0,X1),X4)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f44571,f39466]) ).
fof(f45289,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v1_xboole_0(X1)
| r1_tarski(X1,k19_filter_2(X0,X1))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f44570,f39466]) ).
fof(f45301,definition,
( spl711_32
<=> r1_tarski(k19_filter_2(sK56,k19_filter_2(sK56,sK57)),k19_filter_2(sK56,sK57)) ),
introduced(definition,[new_symbols(definition,[spl711_32])],[avatar_definition]) ).
fof(f45303,plain,
( ~ r1_tarski(k19_filter_2(sK56,k19_filter_2(sK56,sK57)),k19_filter_2(sK56,sK57))
| spl711_32 ),
inference(avatar_component_clause,[],[f45301]) ).
fof(f45305,definition,
( spl711_33
<=> r1_tarski(sK58,sK59) ),
introduced(definition,[new_symbols(definition,[spl711_33])],[avatar_definition]) ).
fof(f45307,plain,
( r1_tarski(sK58,sK59)
| ~ spl711_33 ),
inference(avatar_component_clause,[],[f45305]) ).
fof(f45308,plain,
( ~ spl711_32
| spl711_33 ),
inference(avatar_split_clause,[],[f39265,f45305,f45301]) ).
fof(f45310,definition,
( spl711_34
<=> r1_tarski(k19_filter_2(sK56,sK58),k19_filter_2(sK56,sK59)) ),
introduced(definition,[new_symbols(definition,[spl711_34])],[avatar_definition]) ).
fof(f45312,plain,
( ~ r1_tarski(k19_filter_2(sK56,sK58),k19_filter_2(sK56,sK59))
| spl711_34 ),
inference(avatar_component_clause,[],[f45310]) ).
fof(f45313,plain,
( ~ spl711_32
| ~ spl711_34 ),
inference(avatar_split_clause,[],[f39266,f45310,f45301]) ).
fof(f45431,plain,
( v1_xboole_0(sK59)
| r1_tarski(sK59,k19_filter_2(sK56,sK59))
| v3_struct_0(sK56)
| ~ v10_lattices(sK56)
| ~ l3_lattices(sK56) ),
inference(resolution,[],[f39263,f45289]) ).
fof(f45432,plain,
( r1_tarski(sK59,k19_filter_2(sK56,sK59))
| v3_struct_0(sK56)
| ~ v10_lattices(sK56)
| ~ l3_lattices(sK56) ),
inference(forward_subsumption_resolution,[],[f45431,f39264]) ).
fof(f45433,plain,
( r1_tarski(sK59,k19_filter_2(sK56,sK59))
| ~ v10_lattices(sK56)
| ~ l3_lattices(sK56) ),
inference(forward_subsumption_resolution,[],[f45432,f39258]) ).
fof(f45434,plain,
( r1_tarski(sK59,k19_filter_2(sK56,sK59))
| ~ l3_lattices(sK56) ),
inference(forward_subsumption_resolution,[],[f45433,f39257]) ).
fof(f45435,plain,
r1_tarski(sK59,k19_filter_2(sK56,sK59)),
inference(forward_subsumption_resolution,[],[f45434,f39256]) ).
fof(f45437,plain,
! [X0] :
( ~ r1_tarski(sK58,X0)
| ~ m2_filter_2(X0,sK56)
| v1_xboole_0(sK58)
| r1_tarski(k19_filter_2(sK56,sK58),X0)
| v3_struct_0(sK56)
| ~ v10_lattices(sK56)
| ~ l3_lattices(sK56) ),
inference(resolution,[],[f45288,f39261]) ).
fof(f45440,plain,
! [X0] :
( ~ r1_tarski(sK58,X0)
| ~ m2_filter_2(X0,sK56)
| r1_tarski(k19_filter_2(sK56,sK58),X0)
| v3_struct_0(sK56)
| ~ v10_lattices(sK56)
| ~ l3_lattices(sK56) ),
inference(forward_subsumption_resolution,[],[f45437,f39262]) ).
fof(f45443,plain,
! [X0] :
( ~ r1_tarski(sK58,X0)
| ~ m2_filter_2(X0,sK56)
| r1_tarski(k19_filter_2(sK56,sK58),X0)
| ~ v10_lattices(sK56)
| ~ l3_lattices(sK56) ),
inference(forward_subsumption_resolution,[],[f45440,f39258]) ).
fof(f45446,plain,
! [X0] :
( ~ r1_tarski(sK58,X0)
| ~ m2_filter_2(X0,sK56)
| r1_tarski(k19_filter_2(sK56,sK58),X0)
| ~ l3_lattices(sK56) ),
inference(forward_subsumption_resolution,[],[f45443,f39257]) ).
fof(f45449,plain,
! [X0] :
( r1_tarski(k19_filter_2(sK56,sK58),X0)
| ~ m2_filter_2(X0,sK56)
| ~ r1_tarski(sK58,X0) ),
inference(forward_subsumption_resolution,[],[f45446,f39256]) ).
fof(f45451,plain,
( v3_struct_0(sK56)
| ~ v10_lattices(sK56)
| ~ l3_lattices(sK56)
| v1_xboole_0(sK57)
| m2_filter_2(k19_filter_2(sK56,sK57),sK56) ),
inference(resolution,[],[f39466,f39259]) ).
fof(f45453,plain,
( v3_struct_0(sK56)
| ~ v10_lattices(sK56)
| ~ l3_lattices(sK56)
| v1_xboole_0(sK59)
| m2_filter_2(k19_filter_2(sK56,sK59),sK56) ),
inference(resolution,[],[f39466,f39263]) ).
fof(f45454,plain,
( ~ v10_lattices(sK56)
| ~ l3_lattices(sK56)
| v1_xboole_0(sK59)
| m2_filter_2(k19_filter_2(sK56,sK59),sK56) ),
inference(forward_subsumption_resolution,[],[f45453,f39258]) ).
fof(f45456,plain,
( ~ v10_lattices(sK56)
| ~ l3_lattices(sK56)
| v1_xboole_0(sK57)
| m2_filter_2(k19_filter_2(sK56,sK57),sK56) ),
inference(forward_subsumption_resolution,[],[f45451,f39258]) ).
fof(f45457,plain,
( ~ l3_lattices(sK56)
| v1_xboole_0(sK59)
| m2_filter_2(k19_filter_2(sK56,sK59),sK56) ),
inference(forward_subsumption_resolution,[],[f45454,f39257]) ).
fof(f45459,plain,
( ~ l3_lattices(sK56)
| v1_xboole_0(sK57)
| m2_filter_2(k19_filter_2(sK56,sK57),sK56) ),
inference(forward_subsumption_resolution,[],[f45456,f39257]) ).
fof(f45460,plain,
( v1_xboole_0(sK59)
| m2_filter_2(k19_filter_2(sK56,sK59),sK56) ),
inference(forward_subsumption_resolution,[],[f45457,f39256]) ).
fof(f45462,plain,
( v1_xboole_0(sK57)
| m2_filter_2(k19_filter_2(sK56,sK57),sK56) ),
inference(forward_subsumption_resolution,[],[f45459,f39256]) ).
fof(f45463,plain,
m2_filter_2(k19_filter_2(sK56,sK59),sK56),
inference(forward_subsumption_resolution,[],[f45460,f39264]) ).
fof(f45465,plain,
m2_filter_2(k19_filter_2(sK56,sK57),sK56),
inference(forward_subsumption_resolution,[],[f45462,f39260]) ).
fof(f45468,plain,
! [X0,X1] :
( ~ r1_tarski(X0,X0)
| k19_filter_2(X1,X0) = X0
| ~ m2_filter_2(X0,X1)
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(X1)))
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| ~ r1_tarski(X0,X0)
| k19_filter_2(X1,X0) = X0
| ~ m2_filter_2(X0,X1)
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(X1)))
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(resolution,[],[f39465,f39464]) ).
fof(f45472,plain,
! [X0,X1] :
( ~ r1_tarski(X0,X0)
| k19_filter_2(X1,X0) = X0
| ~ m2_filter_2(X0,X1)
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(X1)))
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(duplicate_literal_removal,[],[f45468]) ).
fof(f45473,plain,
! [X0,X1] :
( k19_filter_2(X1,X0) = X0
| ~ m2_filter_2(X0,X1)
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(X1)))
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(forward_subsumption_resolution,[],[f45472,f39390]) ).
fof(f45474,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(X1)))
| ~ m2_filter_2(X0,X1)
| k19_filter_2(X1,X0) = X0
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(forward_subsumption_resolution,[],[f45473,f40337]) ).
fof(f45646,plain,
! [X0] :
( r1_tarski(X0,k19_filter_2(sK56,sK59))
| ~ r1_tarski(X0,sK59) ),
inference(resolution,[],[f39386,f45435]) ).
fof(f45890,plain,
! [X0,X1] :
( ~ m2_lattice4(X0,X1)
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| ~ m2_filter_2(X0,X1)
| k19_filter_2(X1,X0) = X0
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(resolution,[],[f42736,f45474]) ).
fof(f45900,plain,
! [X0,X1] :
( ~ m2_lattice4(X0,X1)
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| ~ m2_filter_2(X0,X1)
| k19_filter_2(X1,X0) = X0 ),
inference(duplicate_literal_removal,[],[f45890]) ).
fof(f45913,plain,
! [X0,X1] :
( ~ m2_filter_2(X0,X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| v3_struct_0(X1)
| k19_filter_2(X1,X0) = X0 ),
inference(forward_subsumption_resolution,[],[f45900,f40336]) ).
fof(f45925,plain,
( ~ v10_lattices(sK56)
| ~ l3_lattices(sK56)
| v3_struct_0(sK56)
| k19_filter_2(sK56,sK57) = k19_filter_2(sK56,k19_filter_2(sK56,sK57)) ),
inference(resolution,[],[f45913,f45465]) ).
fof(f45930,plain,
( ~ l3_lattices(sK56)
| v3_struct_0(sK56)
| k19_filter_2(sK56,sK57) = k19_filter_2(sK56,k19_filter_2(sK56,sK57)) ),
inference(forward_subsumption_resolution,[],[f45925,f39257]) ).
fof(f45933,plain,
( v3_struct_0(sK56)
| k19_filter_2(sK56,sK57) = k19_filter_2(sK56,k19_filter_2(sK56,sK57)) ),
inference(forward_subsumption_resolution,[],[f45930,f39256]) ).
fof(f45936,plain,
k19_filter_2(sK56,sK57) = k19_filter_2(sK56,k19_filter_2(sK56,sK57)),
inference(forward_subsumption_resolution,[],[f45933,f39258]) ).
fof(f45940,plain,
( ~ r1_tarski(k19_filter_2(sK56,sK57),k19_filter_2(sK56,sK57))
| spl711_32 ),
inference(superposition,[],[f45303,f45936]) ).
fof(f45941,plain,
( $false
| spl711_32 ),
inference(forward_subsumption_resolution,[],[f45940,f39390]) ).
fof(f45942,plain,
spl711_32,
inference(avatar_contradiction_clause,[],[f45941]) ).
fof(f45945,plain,
( ~ m2_filter_2(k19_filter_2(sK56,sK59),sK56)
| ~ r1_tarski(sK58,k19_filter_2(sK56,sK59))
| spl711_34 ),
inference(resolution,[],[f45312,f45449]) ).
fof(f45946,plain,
( ~ r1_tarski(sK58,k19_filter_2(sK56,sK59))
| spl711_34 ),
inference(forward_subsumption_resolution,[],[f45945,f45463]) ).
fof(f45947,plain,
( ~ r1_tarski(sK58,sK59)
| spl711_34 ),
inference(resolution,[],[f45946,f45646]) ).
fof(f45948,plain,
( $false
| ~ spl711_33
| spl711_34 ),
inference(forward_subsumption_resolution,[],[f45947,f45307]) ).
fof(f45949,plain,
( ~ spl711_33
| spl711_34 ),
inference(avatar_contradiction_clause,[],[f45948]) ).
cnf(s32,plain,
( ~ spl711_32
| spl711_33 ),
inference(sat_conversion,[],[f45308]) ).
cnf(s33,plain,
( ~ spl711_32
| ~ spl711_34 ),
inference(sat_conversion,[],[f45313]) ).
cnf(s52,plain,
spl711_32,
inference(sat_conversion,[],[f45942]) ).
cnf(s53,plain,
( ~ spl711_33
| spl711_34 ),
inference(sat_conversion,[],[f45949]) ).
cnf(s61,plain,
~ spl711_34,
inference(rat,[],[s33,s52]) ).
cnf(s62,plain,
~ spl711_33,
inference(rat,[],[s53,s61]) ).
cnf(s63,plain,
$false,
inference(rat,[],[s32,s62,s52]) ).
fof(f45950,plain,
$false,
inference(avatar_sat_refutation,[],[s63]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : LAT310+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.03/0.31 % Computer : n012.cluster.edu
% 0.03/0.31 % Model : x86_64 x86_64
% 0.03/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.31 % Memory : 8046.5625MB
% 0.03/0.31 % OS : Linux 6.8.0-71-generic
% 0.03/0.31 % CPULimit : 300
% 0.03/0.31 % WCLimit : 300
% 0.03/0.31 % DateTime : Sun Sep 27 14:28:26 UTC 2026
% 0.03/0.31 % CPUTime :
% 0.03/0.31 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.33 Running first-order theorem proving
% 0.07/0.33 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
% 8.77/2.75 % (2433625)Detected formulas, will run a generic FOF schedule.
% 8.77/2.75 % (2433630)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=2279065110:i=141193_2991 on theBenchmark for (2991ds/141193Mi)
% 8.77/2.75 % (2433631)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=812585815:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2991 on theBenchmark for (2991ds/134677Mi)
% 8.77/2.75 % (2433633)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2338484140:i=109:sd=1:ins=1:gsp=on:ss=axioms_2991 on theBenchmark for (2991ds/109Mi)
% 8.77/2.75 % (2433634)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3806795022:i=119:av=off:ss=axioms_2991 on theBenchmark for (2991ds/119Mi)
% 8.77/2.75 % (2433635)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1341647673:s2a=on:i=139:gtg=position_2991 on theBenchmark for (2991ds/139Mi)
% 8.77/2.75 % (2433636)dis-21_1_sil=8000:lcm=predicate:random_seed=1492219200:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2991 on theBenchmark for (2991ds/129Mi)
% 8.77/2.75 % (2433632)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=2747128703:i=141695:sd=1:nm=32:gsp=on:ss=included_2991 on theBenchmark for (2991ds/141695Mi)
% 8.77/2.75 % (2433635)Instruction limit reached!
% 8.77/2.75 % (2433635)------------------------------
% 8.77/2.75 % (2433635)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.77/2.75 % (2433635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.77/2.75 % (2433635)CaDiCaL version: 2.1.3
% 8.77/2.75 % (2433635)Termination reason: Instruction limit
% 8.77/2.75 % (2433635)Termination phase: Property scanning
% 8.77/2.75 % (2433635)Time elapsed: 0.033 s
% 8.77/2.75 % (2433635)Peak memory usage: 136 MB
% 8.77/2.75 % (2433635)Instructions burned: 141 (million)
% 8.77/2.75 % (2433633)Instruction limit reached!
% 8.77/2.75 % (2433633)------------------------------
% 8.77/2.75 % (2433633)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.77/2.75 % (2433633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.77/2.75 % (2433633)CaDiCaL version: 2.1.3
% 8.77/2.75 % (2433633)Termination reason: Instruction limit
% 8.77/2.75 % (2433633)Termination phase: SInE selection
% 8.77/2.75 % (2433633)Time elapsed: 0.047 s
% 8.77/2.75 % (2433633)Peak memory usage: 136 MB
% 8.77/2.75 % (2433633)Instructions burned: 111 (million)
% 8.77/2.75 % (2433634)Instruction limit reached!
% 8.77/2.75 % (2433634)------------------------------
% 8.77/2.75 % (2433634)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.77/2.75 % (2433634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.77/2.75 % (2433634)CaDiCaL version: 2.1.3
% 8.77/2.75 % (2433634)Termination reason: Instruction limit
% 8.77/2.75 % (2433634)Termination phase: SInE selection
% 8.77/2.75 % (2433634)Time elapsed: 0.050 s
% 8.77/2.75 % (2433634)Peak memory usage: 136 MB
% 8.77/2.75 % (2433634)Instructions burned: 121 (million)
% 8.77/2.75 % (2433636)Instruction limit reached!
% 8.77/2.75 % (2433636)------------------------------
% 8.77/2.75 % (2433636)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.77/2.75 % (2433636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.77/2.75 % (2433636)CaDiCaL version: 2.1.3
% 8.77/2.75 % (2433636)Termination reason: Instruction limit
% 8.77/2.75 % (2433636)Termination phase: SInE selection
% 8.77/2.75 % (2433636)Time elapsed: 0.051 s
% 8.77/2.75 % (2433636)Peak memory usage: 136 MB
% 8.77/2.75 % (2433636)Instructions burned: 131 (million)
% 8.77/2.75 % (2433644)lrs+10_1_sil=8000:sp=occurrence:random_seed=448742566:i=285:sd=3:ss=axioms:sgt=8_2989 on theBenchmark for (2989ds/285Mi)
% 8.77/2.75 % (2433646)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1076787996:i=325:sd=1:ss=axioms:sgt=32_2989 on theBenchmark for (2989ds/325Mi)
% 8.77/2.75 % (2433645)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3817410672:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2989 on theBenchmark for (2989ds/157Mi)
% 8.77/2.75 % (2433647)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=1123440134:s2a=on:i=248:s2at=1.23:gtg=position_2989 on theBenchmark for (2989ds/248Mi)
% 8.77/2.75 % (2433645)Instruction limit reached!
% 13.91/3.39 % (2433645)------------------------------
% 13.91/3.39 % (2433645)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.91/3.39 % (2433645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.91/3.39 % (2433645)CaDiCaL version: 2.1.3
% 13.91/3.39 % (2433645)Termination reason: Instruction limit
% 13.91/3.39 % (2433645)Termination phase: Property scanning
% 13.91/3.39 % (2433645)Time elapsed: 0.039 s
% 13.91/3.39 % (2433645)Peak memory usage: 136 MB
% 13.91/3.39 % (2433645)Instructions burned: 158 (million)
% 13.91/3.39 % (2433647)Instruction limit reached!
% 13.91/3.39 % (2433647)------------------------------
% 13.91/3.39 % (2433647)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.91/3.39 % (2433647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.91/3.39 % (2433647)CaDiCaL version: 2.1.3
% 13.91/3.39 % (2433647)Termination reason: Instruction limit
% 13.91/3.39 % (2433647)Termination phase: Property scanning
% 13.91/3.39 % (2433647)Time elapsed: 0.060 s
% 13.91/3.39 % (2433647)Peak memory usage: 136 MB
% 13.91/3.39 % (2433647)Instructions burned: 251 (million)
% 13.91/3.39 % (2433644)Instruction limit reached!
% 13.91/3.39 % (2433644)------------------------------
% 13.91/3.39 % (2433644)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.91/3.39 % (2433644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.91/3.39 % (2433644)CaDiCaL version: 2.1.3
% 13.91/3.39 % (2433644)Termination reason: Instruction limit
% 13.91/3.39 % (2433644)Termination phase: Saturation
% 13.91/3.39 % (2433644)Time elapsed: 0.130 s
% 13.91/3.39 % (2433644)Peak memory usage: 142 MB
% 13.91/3.39 % (2433644)Instructions burned: 286 (million)
% 13.91/3.39 % (2433652)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3908046636:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2988 on theBenchmark for (2988ds/294Mi)
% 13.91/3.39 % (2433646)Instruction limit reached!
% 13.91/3.39 % (2433646)------------------------------
% 13.91/3.39 % (2433646)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.91/3.39 % (2433646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.91/3.39 % (2433646)CaDiCaL version: 2.1.3
% 13.91/3.39 % (2433646)Termination reason: Instruction limit
% 13.91/3.39 % (2433646)Termination phase: Saturation
% 13.91/3.39 % (2433646)Time elapsed: 0.150 s
% 13.91/3.39 % (2433646)Peak memory usage: 142 MB
% 13.91/3.39 % (2433646)Instructions burned: 327 (million)
% 13.91/3.39 % (2433653)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=87164196:i=2350_2987 on theBenchmark for (2987ds/2350Mi)
% 13.91/3.39 % (2433654)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=190176239:cts=off:i=113:fsr=off:ss=included:sgt=4_2987 on theBenchmark for (2987ds/113Mi)
% 13.91/3.39 % (2433652)Instruction limit reached!
% 13.91/3.39 % (2433652)------------------------------
% 13.91/3.39 % (2433652)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.91/3.39 % (2433652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.91/3.39 % (2433652)CaDiCaL version: 2.1.3
% 13.91/3.39 % (2433652)Termination reason: Instruction limit
% 13.91/3.39 % (2433652)Termination phase: SInE selection
% 13.91/3.39 % (2433652)Time elapsed: 0.106 s
% 13.91/3.39 % (2433652)Peak memory usage: 137 MB
% 13.91/3.39 % (2433652)Instructions burned: 294 (million)
% 13.91/3.39 % (2433656)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3012059610:i=127:av=off:fsr=off:sup=off_2987 on theBenchmark for (2987ds/127Mi)
% 13.91/3.39 % (2433654)Instruction limit reached!
% 13.91/3.39 % (2433654)------------------------------
% 13.91/3.39 % (2433654)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.91/3.39 % (2433654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.91/3.39 % (2433654)CaDiCaL version: 2.1.3
% 13.91/3.39 % (2433654)Termination reason: Instruction limit
% 13.91/3.39 % (2433654)Termination phase: SInE selection
% 13.91/3.39 % (2433654)Time elapsed: 0.051 s
% 13.91/3.39 % (2433654)Peak memory usage: 136 MB
% 13.91/3.39 % (2433654)Instructions burned: 115 (million)
% 13.91/3.39 % (2433656)Instruction limit reached!
% 13.91/3.39 % (2433656)------------------------------
% 13.91/3.39 % (2433656)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.91/3.39 % (2433656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.91/3.39 % (2433656)CaDiCaL version: 2.1.3
% 13.91/3.39 % (2433656)Termination reason: Instruction limit
% 17.14/4.00 % (2433656)Termination phase: Preprocessing 1
% 17.14/4.00 % (2433656)Time elapsed: 0.057 s
% 17.14/4.00 % (2433656)Peak memory usage: 137 MB
% 17.14/4.00 % (2433656)Instructions burned: 128 (million)
% 17.14/4.00 % (2433660)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=4157781646:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2986 on theBenchmark for (2986ds/114Mi)
% 17.14/4.00 % (2433661)lrs+10_1_sil=8000:sp=occurrence:random_seed=39255800:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2986 on theBenchmark for (2986ds/907Mi)
% 17.14/4.00 % (2433660)Instruction limit reached!
% 17.14/4.00 % (2433660)------------------------------
% 17.14/4.00 % (2433660)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.14/4.00 % (2433660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.14/4.00 % (2433660)CaDiCaL version: 2.1.3
% 17.14/4.00 % (2433660)Termination reason: Instruction limit
% 17.14/4.00 % (2433660)Termination phase: Property scanning
% 17.14/4.00 % (2433660)Time elapsed: 0.029 s
% 17.14/4.00 % (2433660)Peak memory usage: 136 MB
% 17.14/4.00 % (2433660)Instructions burned: 118 (million)
% 17.14/4.00 % (2433662)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1607089822:i=437:sd=1:aac=none:ss=included_2985 on theBenchmark for (2985ds/437Mi)
% 17.14/4.00 % (2433665)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1472668876:i=5202:ss=axioms:sgt=16_2985 on theBenchmark for (2985ds/5202Mi)
% 17.14/4.00 % (2433662)Instruction limit reached!
% 17.14/4.00 % (2433662)------------------------------
% 17.14/4.00 % (2433662)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.14/4.00 % (2433662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.14/4.00 % (2433662)CaDiCaL version: 2.1.3
% 17.14/4.00 % (2433662)Termination reason: Instruction limit
% 17.14/4.00 % (2433662)Termination phase: Saturation
% 17.14/4.00 % (2433662)Time elapsed: 0.180 s
% 17.14/4.00 % (2433662)Peak memory usage: 143 MB
% 17.14/4.00 % (2433662)Instructions burned: 440 (million)
% 17.14/4.00 % (2433668)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2116815617:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2982 on theBenchmark for (2982ds/134Mi)
% 17.14/4.00 % (2433661)Instruction limit reached!
% 17.14/4.00 % (2433661)------------------------------
% 17.14/4.00 % (2433661)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.14/4.00 % (2433661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.14/4.00 % (2433661)CaDiCaL version: 2.1.3
% 17.14/4.00 % (2433661)Termination reason: Instruction limit
% 17.14/4.00 % (2433661)Termination phase: Property scanning
% 17.14/4.00 % (2433661)Time elapsed: 0.378 s
% 17.14/4.00 % (2433661)Peak memory usage: 157 MB
% 17.14/4.00 % (2433661)Instructions burned: 909 (million)
% 17.14/4.00 % (2433668)Instruction limit reached!
% 17.14/4.00 % (2433668)------------------------------
% 17.14/4.00 % (2433668)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.14/4.00 % (2433668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.14/4.00 % (2433668)CaDiCaL version: 2.1.3
% 17.14/4.00 % (2433668)Termination reason: Instruction limit
% 17.14/4.00 % (2433668)Termination phase: SInE selection
% 17.14/4.00 % (2433668)Time elapsed: 0.057 s
% 17.14/4.00 % (2433668)Peak memory usage: 136 MB
% 17.14/4.00 % (2433668)Instructions burned: 135 (million)
% 17.14/4.00 % (2433670)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1404546754:st=8:i=592:sd=3:ep=RST:ss=axioms_2981 on theBenchmark for (2981ds/592Mi)
% 17.14/4.00 % (2433671)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1798409072:st=3:i=13193:sd=3:ss=axioms_2981 on theBenchmark for (2981ds/13193Mi)
% 17.14/4.00 % (2433653)Instruction limit reached!
% 17.14/4.00 % (2433653)------------------------------
% 17.14/4.00 % (2433653)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.14/4.00 % (2433653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.14/4.00 % (2433653)CaDiCaL version: 2.1.3
% 17.14/4.00 % (2433653)Termination reason: Instruction limit
% 17.14/4.00 % (2433653)Termination phase: Property scanning
% 17.14/4.00 % (2433653)Time elapsed: 0.877 s
% 17.14/4.00 % (2433653)Peak memory usage: 233 MB
% 17.14/4.00 % (2433653)Instructions burned: 2353 (million)
% 17.14/4.00 % (2433670)Instruction limit reached!
% 17.14/4.00 % (2433670)------------------------------
% 17.14/4.00 % (2433670)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.14/4.00 % (2433670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.14/4.00 % (2433670)CaDiCaL version: 2.1.3
% 17.14/4.00 % (2433670)Termination reason: Instruction limit
% 17.14/4.00 % (2433670)Termination phase: Naming
% 17.14/4.00 % (2433670)Time elapsed: 0.277 s
% 17.14/4.00 % (2433670)Peak memory usage: 154 MB
% 17.14/4.00 % (2433670)Instructions burned: 594 (million)
% 17.14/4.00 % (2433674)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=1601795513:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2978 on theBenchmark for (2978ds/125Mi)
% 17.14/4.00 % (2433674)Instruction limit reached!
% 17.14/4.00 % (2433674)------------------------------
% 17.14/4.00 % (2433674)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.14/4.00 % (2433674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.14/4.00 % (2433674)CaDiCaL version: 2.1.3
% 17.14/4.00 % (2433674)Termination reason: Instruction limit
% 17.14/4.00 % (2433674)Termination phase: Property scanning
% 17.14/4.00 % (2433674)Time elapsed: 0.032 s
% 17.14/4.00 % (2433674)Peak memory usage: 136 MB
% 17.14/4.00 % (2433674)Instructions burned: 129 (million)
% 17.14/4.00 % (2433675)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3416923868:i=134:gtgl=5:slsql=off:gtg=exists_sym_2977 on theBenchmark for (2977ds/134Mi)
% 17.14/4.00 % (2433675)Instruction limit reached!
% 17.14/4.00 % (2433675)------------------------------
% 17.14/4.00 % (2433675)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.14/4.00 % (2433675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.14/4.00 % (2433675)CaDiCaL version: 2.1.3
% 17.14/4.00 % (2433675)Termination reason: Instruction limit
% 17.14/4.00 % (2433675)Termination phase: Property scanning
% 17.14/4.00 % (2433675)Time elapsed: 0.034 s
% 17.14/4.00 % (2433675)Peak memory usage: 136 MB
% 17.14/4.00 % (2433675)Instructions burned: 138 (million)
% 17.14/4.00 % (2433677)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3969696164:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2976 on theBenchmark for (2976ds/141Mi)
% 17.14/4.00 % (2433679)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2888598276:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2976 on theBenchmark for (2976ds/431Mi)
% 17.14/4.00 % (2433677)Instruction limit reached!
% 17.14/4.00 % (2433677)------------------------------
% 17.14/4.00 % (2433677)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.14/4.00 % (2433677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.14/4.00 % (2433677)CaDiCaL version: 2.1.3
% 17.14/4.00 % (2433677)Termination reason: Instruction limit
% 17.14/4.00 % (2433677)Termination phase: SInE selection
% 17.14/4.00 % (2433677)Time elapsed: 0.066 s
% 17.14/4.00 % (2433677)Peak memory usage: 136 MB
% 17.14/4.00 % (2433677)Instructions burned: 143 (million)
% 17.14/4.00 % (2433682)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=537031537:i=6060:aac=none:ins=25_2975 on theBenchmark for (2975ds/6060Mi)
% 17.14/4.00 % (2433679)Instruction limit reached!
% 17.14/4.00 % (2433679)------------------------------
% 17.14/4.00 % (2433679)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.14/4.00 % (2433679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.14/4.00 % (2433679)CaDiCaL version: 2.1.3
% 17.14/4.00 % (2433679)Termination reason: Instruction limit
% 17.14/4.00 % (2433679)Termination phase: Saturation
% 17.14/4.00 % (2433679)Time elapsed: 0.195 s
% 17.14/4.00 % (2433679)Peak memory usage: 144 MB
% 17.14/4.00 % (2433679)Instructions burned: 432 (million)
% 17.14/4.00 % (2433684)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=3845505132:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2973 on theBenchmark for (2973ds/150Mi)
% 17.14/4.00 % (2433684)Instruction limit reached!
% 17.14/4.00 % (2433684)------------------------------
% 17.14/4.00 % (2433684)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.14/4.00 % (2433684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.14/4.00 % (2433684)CaDiCaL version: 2.1.3
% 17.14/4.00 % (2433684)Termination reason: Instruction limit
% 17.14/4.00 % (2433684)Termination phase: SInE selection
% 17.14/4.00 % (2433684)Time elapsed: 0.074 s
% 17.14/4.00 % (2433684)Peak memory usage: 136 MB
% 17.14/4.00 % (2433684)Instructions burned: 150 (million)
% 17.14/4.00 % (2433686)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3258746770:i=14155:bd=all_2971 on theBenchmark for (2971ds/14155Mi)
% 17.14/4.00 % (2433671)First to succeed.
% 17.14/4.00 % (2433671)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2433625"
% 17.14/4.00 % (2433671)Refutation found. Thanks to Tanya!
% 17.14/4.00 % SZS status Theorem for theBenchmark
% 17.14/4.00 % SZS output start Proof for theBenchmark
% See solution above
% 19.20/4.10 % (2433671)------------------------------
% 19.20/4.10 % (2433671)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.20/4.10 % (2433671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.20/4.10 % (2433671)CaDiCaL version: 2.1.3
% 19.20/4.10 % (2433671)Termination reason: Refutation
% 19.20/4.10 % (2433671)Time elapsed: 1.309 s
% 19.20/4.10 % (2433671)Peak memory usage: 244 MB
% 19.20/4.10 % (2433671)Instructions burned: 3730 (million)
% 19.20/4.10 % (2433671)------------------------------
% 19.20/4.10 % (2433671)------------------------------
% 19.20/4.10 % (2433625)Success in time 3.475 s
% 19.20/4.10 % Vampire exiting
%------------------------------------------------------------------------------