%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT317+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 : n005.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:52 AM UTC 2026
% Result : Theorem 20.97s 8.24s
% Output : Refutation 39.41s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 24
% Syntax : Number of formulae : 220 ( 35 unt; 11 def)
% Number of atoms : 922 ( 63 equ)
% Maximal formula atoms : 15 ( 4 avg)
% Number of connectives : 1172 ( 470 ~; 548 |; 114 &)
% ( 13 <=>; 27 =>; 0 <=; 0 <~>)
% Maximal formula depth : 20 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 30 ( 28 usr; 11 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 3 con; 0-3 aty)
% Number of variables : 151 ( 0 sgn 145 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f21554,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_filter_0(X1,X0)
=> ! [X2] :
( m1_filter_0(X2,X0)
=> ( r1_tarski(X1,k5_filter_0(X0,X1,X2))
& r1_tarski(X2,k5_filter_0(X0,X1,X2)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t49_filter_0) ).
fof(f22747,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l3_lattices(X0) )
=> ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_lattice2) ).
fof(f22752,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v4_lattices(k1_lattice2(X0))
& v5_lattices(k1_lattice2(X0))
& v6_lattices(k1_lattice2(X0))
& v7_lattices(k1_lattice2(X0))
& v8_lattices(k1_lattice2(X0))
& v9_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc6_lattice2) ).
fof(f22780,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l3_lattices(X0) )
=> ( u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0))
& u2_lattices(X0) = u1_lattices(k1_lattice2(X0))
& u1_lattices(X0) = u2_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t18_lattice2) ).
fof(f22852,axiom,
! [X0] :
( l3_lattices(X0)
=> ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k1_lattice2) ).
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] :
( m1_filter_2(X1,X0)
<=> m1_filter_0(X1,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_m1_filter_2) ).
fof(f34608,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(f34637,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& m2_filter_2(X1,X0) )
=> m1_filter_2(k15_filter_2(X0,X1),k1_lattice2(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k15_filter_2) ).
fof(f34638,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& m2_filter_2(X1,X0) )
=> k15_filter_2(X0,X1) = k7_filter_2(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k15_filter_2) ).
fof(f34677,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
=> k7_filter_2(X0,X1) = X1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d6_filter_2) ).
fof(f34713,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] :
( ( ~ 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(k1_lattice2(X0)))) )
=> ! [X4] :
( ( ~ v1_xboole_0(X4)
& m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(k1_lattice2(X0)))) )
=> ( k20_filter_2(X0,X1,X2) = k5_filter_0(k1_lattice2(X0),k7_filter_2(X0,X1),k7_filter_2(X0,X2))
& k20_filter_2(k1_lattice2(X0),k7_filter_2(X0,X1),k7_filter_2(X0,X2)) = k5_filter_0(X0,X1,X2)
& k20_filter_2(k1_lattice2(X0),X3,X4) = k5_filter_0(X0,k8_filter_2(X0,X3),k8_filter_2(X0,X4))
& k20_filter_2(X0,k8_filter_2(X0,X3),k8_filter_2(X0,X4)) = k5_filter_0(k1_lattice2(X0),X3,X4) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t45_filter_2) ).
fof(f34719,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_filter_2(X1,X0)
=> ! [X2] :
( m2_filter_2(X2,X0)
=> ( r1_tarski(X1,k20_filter_2(X0,X1,X2))
& r1_tarski(X2,k20_filter_2(X0,X1,X2)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t51_filter_2) ).
fof(f34720,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_filter_2(X1,X0)
=> ! [X2] :
( m2_filter_2(X2,X0)
=> ( r1_tarski(X1,k20_filter_2(X0,X1,X2))
& r1_tarski(X2,k20_filter_2(X0,X1,X2)) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f34719]) ).
fof(f34936,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ( ~ r1_tarski(X1,k20_filter_2(X0,X1,X2))
| ~ r1_tarski(X2,k20_filter_2(X0,X1,X2)) )
& m2_filter_2(X2,X0) )
& m2_filter_2(X1,X0) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(ennf_transformation,[],[f34720]) ).
fof(f34937,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ( ~ r1_tarski(X1,k20_filter_2(X0,X1,X2))
| ~ r1_tarski(X2,k20_filter_2(X0,X1,X2)) )
& m2_filter_2(X2,X0) )
& m2_filter_2(X1,X0) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(flattening,[],[f34936]) ).
fof(f35048,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,[],[f34608]) ).
fof(f35049,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,[],[f35048]) ).
fof(f35056,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ( k20_filter_2(X0,X1,X2) = k5_filter_0(k1_lattice2(X0),k7_filter_2(X0,X1),k7_filter_2(X0,X2))
& k20_filter_2(k1_lattice2(X0),k7_filter_2(X0,X1),k7_filter_2(X0,X2)) = k5_filter_0(X0,X1,X2)
& k20_filter_2(k1_lattice2(X0),X3,X4) = k5_filter_0(X0,k8_filter_2(X0,X3),k8_filter_2(X0,X4))
& k20_filter_2(X0,k8_filter_2(X0,X3),k8_filter_2(X0,X4)) = k5_filter_0(k1_lattice2(X0),X3,X4) )
| v1_xboole_0(X4)
| ~ m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(k1_lattice2(X0)))) )
| v1_xboole_0(X3)
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(k1_lattice2(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,[],[f34713]) ).
fof(f35057,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ( k20_filter_2(X0,X1,X2) = k5_filter_0(k1_lattice2(X0),k7_filter_2(X0,X1),k7_filter_2(X0,X2))
& k20_filter_2(k1_lattice2(X0),k7_filter_2(X0,X1),k7_filter_2(X0,X2)) = k5_filter_0(X0,X1,X2)
& k20_filter_2(k1_lattice2(X0),X3,X4) = k5_filter_0(X0,k8_filter_2(X0,X3),k8_filter_2(X0,X4))
& k20_filter_2(X0,k8_filter_2(X0,X3),k8_filter_2(X0,X4)) = k5_filter_0(k1_lattice2(X0),X3,X4) )
| v1_xboole_0(X4)
| ~ m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(k1_lattice2(X0)))) )
| v1_xboole_0(X3)
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(k1_lattice2(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,[],[f35056]) ).
fof(f35938,plain,
! [X0] :
( ( u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0))
& u2_lattices(X0) = u1_lattices(k1_lattice2(X0))
& u1_lattices(X0) = u2_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f22780]) ).
fof(f35939,plain,
! [X0] :
( ( u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0))
& u2_lattices(X0) = u1_lattices(k1_lattice2(X0))
& u1_lattices(X0) = u2_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35938]) ).
fof(f35984,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(f35985,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,[],[f35984]) ).
fof(f36027,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( r1_tarski(X1,k5_filter_0(X0,X1,X2))
& r1_tarski(X2,k5_filter_0(X0,X1,X2)) )
| ~ m1_filter_0(X2,X0) )
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f21554]) ).
fof(f36028,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( r1_tarski(X1,k5_filter_0(X0,X1,X2))
& r1_tarski(X2,k5_filter_0(X0,X1,X2)) )
| ~ m1_filter_0(X2,X0) )
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f36027]) ).
fof(f36039,plain,
! [X0] :
( ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f22852]) ).
fof(f36048,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v4_lattices(k1_lattice2(X0))
& v5_lattices(k1_lattice2(X0))
& v6_lattices(k1_lattice2(X0))
& v7_lattices(k1_lattice2(X0))
& v8_lattices(k1_lattice2(X0))
& v9_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f22752]) ).
fof(f36049,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v4_lattices(k1_lattice2(X0))
& v5_lattices(k1_lattice2(X0))
& v6_lattices(k1_lattice2(X0))
& v7_lattices(k1_lattice2(X0))
& v8_lattices(k1_lattice2(X0))
& v9_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f36048]) ).
fof(f36050,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f22747]) ).
fof(f36051,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f36050]) ).
fof(f36056,plain,
! [X0] :
( ! [X1] :
( k7_filter_2(X0,X1) = 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,[],[f34677]) ).
fof(f36057,plain,
! [X0] :
( ! [X1] :
( k7_filter_2(X0,X1) = X1
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f36056]) ).
fof(f36058,plain,
! [X0,X1] :
( k15_filter_2(X0,X1) = k7_filter_2(X0,X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m2_filter_2(X1,X0) ),
inference(ennf_transformation,[],[f34638]) ).
fof(f36059,plain,
! [X0,X1] :
( k15_filter_2(X0,X1) = k7_filter_2(X0,X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m2_filter_2(X1,X0) ),
inference(flattening,[],[f36058]) ).
fof(f39309,plain,
! [X0,X1] :
( m1_filter_2(k15_filter_2(X0,X1),k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m2_filter_2(X1,X0) ),
inference(ennf_transformation,[],[f34637]) ).
fof(f39310,plain,
! [X0,X1] :
( m1_filter_2(k15_filter_2(X0,X1),k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m2_filter_2(X1,X0) ),
inference(flattening,[],[f39309]) ).
fof(f39313,plain,
! [X0] :
( ! [X1] :
( m1_filter_2(X1,X0)
<=> m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f34607]) ).
fof(f39314,plain,
! [X0] :
( ! [X1] :
( m1_filter_2(X1,X0)
<=> m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f39313]) ).
fof(f39490,definition,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v4_lattices(k1_lattice2(X0))
& v5_lattices(k1_lattice2(X0))
& v6_lattices(k1_lattice2(X0))
& v7_lattices(k1_lattice2(X0))
& v8_lattices(k1_lattice2(X0))
& v9_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0)) )
| ~ sP13(X0) ),
introduced(definition,[new_symbols(definition,[sP13])],[predicate_definition_introduction]) ).
fof(f39491,plain,
! [X0] :
( sP13(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(definition_folding,[],[f36049,f39490]) ).
fof(f39599,plain,
( ( ~ r1_tarski(sK79,k20_filter_2(sK78,sK79,sK80))
| ~ r1_tarski(sK80,k20_filter_2(sK78,sK79,sK80)) )
& m2_filter_2(sK80,sK78)
& m2_filter_2(sK79,sK78)
& ~ v3_struct_0(sK78)
& v10_lattices(sK78)
& l3_lattices(sK78) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK78,sK79,sK80]),skolemize(X0,sK78),skolemize(X1,sK79),skolemize(X2,sK80)],[f34937]) ).
fof(f39955,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v4_lattices(k1_lattice2(X0))
& v5_lattices(k1_lattice2(X0))
& v6_lattices(k1_lattice2(X0))
& v7_lattices(k1_lattice2(X0))
& v8_lattices(k1_lattice2(X0))
& v9_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0)) )
| ~ sP13(X0) ),
inference(nnf_transformation,[],[f39490]) ).
fof(f40856,plain,
! [X0] :
( ! [X1] :
( ( m1_filter_2(X1,X0)
| ~ m1_filter_0(X1,X0) )
& ( m1_filter_0(X1,X0)
| ~ m1_filter_2(X1,X0) ) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f39314]) ).
fof(f40903,plain,
l3_lattices(sK78),
inference(cnf_transformation,[],[f39599]) ).
fof(f40904,plain,
v10_lattices(sK78),
inference(cnf_transformation,[],[f39599]) ).
fof(f40905,plain,
~ v3_struct_0(sK78),
inference(cnf_transformation,[],[f39599]) ).
fof(f40906,plain,
m2_filter_2(sK79,sK78),
inference(cnf_transformation,[],[f39599]) ).
fof(f40907,plain,
m2_filter_2(sK80,sK78),
inference(cnf_transformation,[],[f39599]) ).
fof(f40908,plain,
( ~ r1_tarski(sK79,k20_filter_2(sK78,sK79,sK80))
| ~ r1_tarski(sK80,k20_filter_2(sK78,sK79,sK80)) ),
inference(cnf_transformation,[],[f39599]) ).
fof(f41073,plain,
! [X0,X1] :
( ~ m2_filter_2(X1,X0)
| m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35049]) ).
fof(f41074,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,[],[f35049]) ).
fof(f41086,plain,
! [X2,X3,X0,X1,X4] :
( ~ m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(k1_lattice2(X0))))
| v1_xboole_0(X4)
| k20_filter_2(X0,X1,X2) = k5_filter_0(k1_lattice2(X0),k7_filter_2(X0,X1),k7_filter_2(X0,X2))
| v1_xboole_0(X3)
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(k1_lattice2(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(cnf_transformation,[],[f35057]) ).
fof(f42267,plain,
! [X0] :
( ~ l3_lattices(X0)
| v3_struct_0(X0)
| u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0)) ),
inference(cnf_transformation,[],[f35939]) ).
fof(f42321,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,[],[f35985]) ).
fof(f42363,plain,
! [X2,X0,X1] :
( r1_tarski(X2,k5_filter_0(X0,X1,X2))
| ~ m1_filter_0(X2,X0)
| ~ m1_filter_0(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f36028]) ).
fof(f42364,plain,
! [X2,X0,X1] :
( r1_tarski(X1,k5_filter_0(X0,X1,X2))
| ~ m1_filter_0(X2,X0)
| ~ m1_filter_0(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f36028]) ).
fof(f42375,plain,
! [X0] :
( l3_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f36039]) ).
fof(f42390,plain,
! [X0] :
( v10_lattices(k1_lattice2(X0))
| ~ sP13(X0) ),
inference(cnf_transformation,[],[f39955]) ).
fof(f42399,plain,
! [X0] :
( ~ v10_lattices(X0)
| v3_struct_0(X0)
| sP13(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f39491]) ).
fof(f42401,plain,
! [X0] :
( ~ v3_struct_0(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f36051]) ).
fof(f42407,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| k7_filter_2(X0,X1) = X1
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f36057]) ).
fof(f42408,plain,
! [X0,X1] :
( ~ m2_filter_2(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| k7_filter_2(X0,X1) = k15_filter_2(X0,X1) ),
inference(cnf_transformation,[],[f36059]) ).
fof(f46764,plain,
! [X0,X1] :
( m1_filter_2(k15_filter_2(X0,X1),k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m2_filter_2(X1,X0) ),
inference(cnf_transformation,[],[f39310]) ).
fof(f46766,plain,
! [X0,X1] :
( ~ m1_filter_2(X1,X0)
| m1_filter_0(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f40856]) ).
fof(f48808,definition,
( spl885_34
<=> r1_tarski(sK80,k20_filter_2(sK78,sK79,sK80)) ),
introduced(definition,[new_symbols(definition,[spl885_34])],[avatar_definition]) ).
fof(f48812,definition,
( spl885_35
<=> r1_tarski(sK79,k20_filter_2(sK78,sK79,sK80)) ),
introduced(definition,[new_symbols(definition,[spl885_35])],[avatar_definition]) ).
fof(f48814,plain,
( ~ r1_tarski(sK79,k20_filter_2(sK78,sK79,sK80))
| spl885_35 ),
inference(avatar_component_clause,[],[f48812]) ).
fof(f48815,plain,
( ~ spl885_34
| ~ spl885_35 ),
inference(avatar_split_clause,[],[f40908,f48812,f48808]) ).
fof(f49134,plain,
( ~ v1_xboole_0(sK79)
| v3_struct_0(sK78)
| ~ v10_lattices(sK78)
| ~ l3_lattices(sK78) ),
inference(resolution,[],[f41074,f40906]) ).
fof(f49135,plain,
( ~ v1_xboole_0(sK80)
| v3_struct_0(sK78)
| ~ v10_lattices(sK78)
| ~ l3_lattices(sK78) ),
inference(resolution,[],[f41074,f40907]) ).
fof(f49136,plain,
( ~ v1_xboole_0(sK80)
| ~ v10_lattices(sK78)
| ~ l3_lattices(sK78) ),
inference(forward_subsumption_resolution,[],[f49135,f40905]) ).
fof(f49137,plain,
( ~ v1_xboole_0(sK79)
| ~ v10_lattices(sK78)
| ~ l3_lattices(sK78) ),
inference(forward_subsumption_resolution,[],[f49134,f40905]) ).
fof(f49138,plain,
( ~ v1_xboole_0(sK80)
| ~ l3_lattices(sK78) ),
inference(forward_subsumption_resolution,[],[f49136,f40904]) ).
fof(f49139,plain,
( ~ v1_xboole_0(sK79)
| ~ l3_lattices(sK78) ),
inference(forward_subsumption_resolution,[],[f49137,f40904]) ).
fof(f49140,plain,
~ v1_xboole_0(sK80),
inference(forward_subsumption_resolution,[],[f49138,f40903]) ).
fof(f49141,plain,
~ v1_xboole_0(sK79),
inference(forward_subsumption_resolution,[],[f49139,f40903]) ).
fof(f49142,plain,
( m2_lattice4(sK79,sK78)
| v3_struct_0(sK78)
| ~ v10_lattices(sK78)
| ~ l3_lattices(sK78) ),
inference(resolution,[],[f41073,f40906]) ).
fof(f49143,plain,
( m2_lattice4(sK80,sK78)
| v3_struct_0(sK78)
| ~ v10_lattices(sK78)
| ~ l3_lattices(sK78) ),
inference(resolution,[],[f41073,f40907]) ).
fof(f49144,plain,
( m2_lattice4(sK80,sK78)
| ~ v10_lattices(sK78)
| ~ l3_lattices(sK78) ),
inference(forward_subsumption_resolution,[],[f49143,f40905]) ).
fof(f49145,plain,
( m2_lattice4(sK79,sK78)
| ~ v10_lattices(sK78)
| ~ l3_lattices(sK78) ),
inference(forward_subsumption_resolution,[],[f49142,f40905]) ).
fof(f49146,plain,
( m2_lattice4(sK80,sK78)
| ~ l3_lattices(sK78) ),
inference(forward_subsumption_resolution,[],[f49144,f40904]) ).
fof(f49147,plain,
( m2_lattice4(sK79,sK78)
| ~ l3_lattices(sK78) ),
inference(forward_subsumption_resolution,[],[f49145,f40904]) ).
fof(f49148,plain,
m2_lattice4(sK80,sK78),
inference(forward_subsumption_resolution,[],[f49146,f40903]) ).
fof(f49149,plain,
m2_lattice4(sK79,sK78),
inference(forward_subsumption_resolution,[],[f49147,f40903]) ).
fof(f49160,plain,
( v3_struct_0(sK78)
| ~ v10_lattices(sK78)
| ~ l3_lattices(sK78)
| k7_filter_2(sK78,sK79) = k15_filter_2(sK78,sK79) ),
inference(resolution,[],[f42408,f40906]) ).
fof(f49161,plain,
( v3_struct_0(sK78)
| ~ v10_lattices(sK78)
| ~ l3_lattices(sK78)
| k7_filter_2(sK78,sK80) = k15_filter_2(sK78,sK80) ),
inference(resolution,[],[f42408,f40907]) ).
fof(f49162,plain,
( ~ v10_lattices(sK78)
| ~ l3_lattices(sK78)
| k7_filter_2(sK78,sK80) = k15_filter_2(sK78,sK80) ),
inference(forward_subsumption_resolution,[],[f49161,f40905]) ).
fof(f49163,plain,
( ~ v10_lattices(sK78)
| ~ l3_lattices(sK78)
| k7_filter_2(sK78,sK79) = k15_filter_2(sK78,sK79) ),
inference(forward_subsumption_resolution,[],[f49160,f40905]) ).
fof(f49164,plain,
( ~ l3_lattices(sK78)
| k7_filter_2(sK78,sK80) = k15_filter_2(sK78,sK80) ),
inference(forward_subsumption_resolution,[],[f49162,f40904]) ).
fof(f49165,plain,
( ~ l3_lattices(sK78)
| k7_filter_2(sK78,sK79) = k15_filter_2(sK78,sK79) ),
inference(forward_subsumption_resolution,[],[f49163,f40904]) ).
fof(f49166,plain,
k7_filter_2(sK78,sK80) = k15_filter_2(sK78,sK80),
inference(forward_subsumption_resolution,[],[f49164,f40903]) ).
fof(f49167,plain,
k7_filter_2(sK78,sK79) = k15_filter_2(sK78,sK79),
inference(forward_subsumption_resolution,[],[f49165,f40903]) ).
fof(f49172,plain,
( m1_filter_2(k7_filter_2(sK78,sK79),k1_lattice2(sK78))
| v3_struct_0(sK78)
| ~ v10_lattices(sK78)
| ~ l3_lattices(sK78)
| ~ m2_filter_2(sK79,sK78) ),
inference(superposition,[],[f46764,f49167]) ).
fof(f49173,plain,
( m1_filter_2(k7_filter_2(sK78,sK80),k1_lattice2(sK78))
| v3_struct_0(sK78)
| ~ v10_lattices(sK78)
| ~ l3_lattices(sK78)
| ~ m2_filter_2(sK80,sK78) ),
inference(superposition,[],[f46764,f49166]) ).
fof(f49174,plain,
( m1_filter_2(k7_filter_2(sK78,sK80),k1_lattice2(sK78))
| ~ v10_lattices(sK78)
| ~ l3_lattices(sK78)
| ~ m2_filter_2(sK80,sK78) ),
inference(forward_subsumption_resolution,[],[f49173,f40905]) ).
fof(f49175,plain,
( m1_filter_2(k7_filter_2(sK78,sK79),k1_lattice2(sK78))
| ~ v10_lattices(sK78)
| ~ l3_lattices(sK78)
| ~ m2_filter_2(sK79,sK78) ),
inference(forward_subsumption_resolution,[],[f49172,f40905]) ).
fof(f49177,plain,
( m1_filter_2(k7_filter_2(sK78,sK80),k1_lattice2(sK78))
| ~ l3_lattices(sK78)
| ~ m2_filter_2(sK80,sK78) ),
inference(forward_subsumption_resolution,[],[f49174,f40904]) ).
fof(f49178,plain,
( m1_filter_2(k7_filter_2(sK78,sK79),k1_lattice2(sK78))
| ~ l3_lattices(sK78)
| ~ m2_filter_2(sK79,sK78) ),
inference(forward_subsumption_resolution,[],[f49175,f40904]) ).
fof(f49180,plain,
( m1_filter_2(k7_filter_2(sK78,sK80),k1_lattice2(sK78))
| ~ m2_filter_2(sK80,sK78) ),
inference(forward_subsumption_resolution,[],[f49177,f40903]) ).
fof(f49181,plain,
( m1_filter_2(k7_filter_2(sK78,sK79),k1_lattice2(sK78))
| ~ m2_filter_2(sK79,sK78) ),
inference(forward_subsumption_resolution,[],[f49178,f40903]) ).
fof(f49182,plain,
m1_filter_2(k7_filter_2(sK78,sK80),k1_lattice2(sK78)),
inference(forward_subsumption_resolution,[],[f49180,f40907]) ).
fof(f49183,plain,
m1_filter_2(k7_filter_2(sK78,sK79),k1_lattice2(sK78)),
inference(forward_subsumption_resolution,[],[f49181,f40906]) ).
fof(f49184,plain,
( m1_filter_0(k7_filter_2(sK78,sK80),k1_lattice2(sK78))
| v3_struct_0(k1_lattice2(sK78))
| ~ v10_lattices(k1_lattice2(sK78))
| ~ l3_lattices(k1_lattice2(sK78)) ),
inference(resolution,[],[f49182,f46766]) ).
fof(f49186,definition,
( spl885_36
<=> l3_lattices(k1_lattice2(sK78)) ),
introduced(definition,[new_symbols(definition,[spl885_36])],[avatar_definition]) ).
fof(f49187,plain,
( l3_lattices(k1_lattice2(sK78))
| ~ spl885_36 ),
inference(avatar_component_clause,[],[f49186]) ).
fof(f49188,plain,
( ~ l3_lattices(k1_lattice2(sK78))
| spl885_36 ),
inference(avatar_component_clause,[],[f49186]) ).
fof(f49190,definition,
( spl885_37
<=> v10_lattices(k1_lattice2(sK78)) ),
introduced(definition,[new_symbols(definition,[spl885_37])],[avatar_definition]) ).
fof(f49191,plain,
( v10_lattices(k1_lattice2(sK78))
| ~ spl885_37 ),
inference(avatar_component_clause,[],[f49190]) ).
fof(f49192,plain,
( ~ v10_lattices(k1_lattice2(sK78))
| spl885_37 ),
inference(avatar_component_clause,[],[f49190]) ).
fof(f49194,definition,
( spl885_38
<=> v3_struct_0(k1_lattice2(sK78)) ),
introduced(definition,[new_symbols(definition,[spl885_38])],[avatar_definition]) ).
fof(f49195,plain,
( ~ v3_struct_0(k1_lattice2(sK78))
| spl885_38 ),
inference(avatar_component_clause,[],[f49194]) ).
fof(f49196,plain,
( v3_struct_0(k1_lattice2(sK78))
| ~ spl885_38 ),
inference(avatar_component_clause,[],[f49194]) ).
fof(f49198,definition,
( spl885_39
<=> m1_filter_0(k7_filter_2(sK78,sK80),k1_lattice2(sK78)) ),
introduced(definition,[new_symbols(definition,[spl885_39])],[avatar_definition]) ).
fof(f49200,plain,
( m1_filter_0(k7_filter_2(sK78,sK80),k1_lattice2(sK78))
| ~ spl885_39 ),
inference(avatar_component_clause,[],[f49198]) ).
fof(f49201,plain,
( ~ spl885_36
| ~ spl885_37
| spl885_38
| spl885_39 ),
inference(avatar_split_clause,[],[f49184,f49198,f49194,f49190,f49186]) ).
fof(f49202,plain,
( ~ l3_lattices(sK78)
| spl885_36 ),
inference(resolution,[],[f49188,f42375]) ).
fof(f49203,plain,
( $false
| spl885_36 ),
inference(forward_subsumption_resolution,[],[f49202,f40903]) ).
fof(f49204,plain,
spl885_36,
inference(avatar_contradiction_clause,[],[f49203]) ).
fof(f49205,plain,
( m1_filter_0(k7_filter_2(sK78,sK79),k1_lattice2(sK78))
| v3_struct_0(k1_lattice2(sK78))
| ~ v10_lattices(k1_lattice2(sK78))
| ~ l3_lattices(k1_lattice2(sK78)) ),
inference(resolution,[],[f49183,f46766]) ).
fof(f49206,plain,
( v3_struct_0(sK78)
| sP13(sK78)
| ~ l3_lattices(sK78) ),
inference(resolution,[],[f42399,f40904]) ).
fof(f49207,plain,
( sP13(sK78)
| ~ l3_lattices(sK78) ),
inference(forward_subsumption_resolution,[],[f49206,f40905]) ).
fof(f49208,plain,
sP13(sK78),
inference(forward_subsumption_resolution,[],[f49207,f40903]) ).
fof(f49221,plain,
( ~ sP13(sK78)
| spl885_37 ),
inference(resolution,[],[f42390,f49192]) ).
fof(f49224,plain,
( $false
| spl885_37 ),
inference(forward_subsumption_resolution,[],[f49221,f49208]) ).
fof(f49225,plain,
spl885_37,
inference(avatar_contradiction_clause,[],[f49224]) ).
fof(f49226,plain,
( v3_struct_0(sK78)
| ~ l3_lattices(sK78)
| ~ spl885_38 ),
inference(resolution,[],[f49196,f42401]) ).
fof(f49227,plain,
( ~ l3_lattices(sK78)
| ~ spl885_38 ),
inference(forward_subsumption_resolution,[],[f49226,f40905]) ).
fof(f49228,plain,
( $false
| ~ spl885_38 ),
inference(forward_subsumption_resolution,[],[f49227,f40903]) ).
fof(f49229,plain,
~ spl885_38,
inference(avatar_contradiction_clause,[],[f49228]) ).
fof(f49230,plain,
( m1_filter_0(k7_filter_2(sK78,sK79),k1_lattice2(sK78))
| ~ v10_lattices(k1_lattice2(sK78))
| ~ l3_lattices(k1_lattice2(sK78))
| spl885_38 ),
inference(forward_subsumption_resolution,[],[f49205,f49195]) ).
fof(f49231,plain,
( m1_filter_0(k7_filter_2(sK78,sK79),k1_lattice2(sK78))
| ~ l3_lattices(k1_lattice2(sK78))
| ~ spl885_37
| spl885_38 ),
inference(forward_subsumption_resolution,[],[f49230,f49191]) ).
fof(f49232,plain,
( m1_filter_0(k7_filter_2(sK78,sK79),k1_lattice2(sK78))
| ~ spl885_36
| ~ spl885_37
| spl885_38 ),
inference(forward_subsumption_resolution,[],[f49231,f49187]) ).
fof(f49244,plain,
! [X0,X1] :
( ~ m2_lattice4(X0,X1)
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| k7_filter_2(X1,X0) = X0
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(resolution,[],[f42321,f42407]) ).
fof(f49245,plain,
! [X0,X1] :
( ~ m2_lattice4(X0,X1)
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| k7_filter_2(X1,X0) = X0 ),
inference(duplicate_literal_removal,[],[f49244]) ).
fof(f49257,plain,
( v3_struct_0(sK78)
| u1_struct_0(sK78) = u1_struct_0(k1_lattice2(sK78)) ),
inference(resolution,[],[f42267,f40903]) ).
fof(f49261,plain,
u1_struct_0(sK78) = u1_struct_0(k1_lattice2(sK78)),
inference(forward_subsumption_resolution,[],[f49257,f40905]) ).
fof(f49262,plain,
! [X2,X3,X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK78)))
| v1_xboole_0(X0)
| k20_filter_2(sK78,X1,X2) = k5_filter_0(k1_lattice2(sK78),k7_filter_2(sK78,X1),k7_filter_2(sK78,X2))
| v1_xboole_0(X3)
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(sK78)))
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(sK78)))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK78)))
| v3_struct_0(sK78)
| ~ v10_lattices(sK78)
| ~ l3_lattices(sK78) ),
inference(superposition,[],[f41086,f49261]) ).
fof(f49279,plain,
! [X2,X3,X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK78)))
| v1_xboole_0(X0)
| k20_filter_2(sK78,X1,X2) = k5_filter_0(k1_lattice2(sK78),k7_filter_2(sK78,X1),k7_filter_2(sK78,X2))
| v1_xboole_0(X3)
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(sK78)))
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(sK78)))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK78)))
| ~ v10_lattices(sK78)
| ~ l3_lattices(sK78) ),
inference(forward_subsumption_resolution,[],[f49262,f40905]) ).
fof(f49288,plain,
! [X2,X3,X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK78)))
| v1_xboole_0(X0)
| k20_filter_2(sK78,X1,X2) = k5_filter_0(k1_lattice2(sK78),k7_filter_2(sK78,X1),k7_filter_2(sK78,X2))
| v1_xboole_0(X3)
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(sK78)))
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(sK78)))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK78)))
| ~ l3_lattices(sK78) ),
inference(forward_subsumption_resolution,[],[f49279,f40904]) ).
fof(f49297,plain,
! [X2,X3,X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK78)))
| v1_xboole_0(X0)
| k20_filter_2(sK78,X1,X2) = k5_filter_0(k1_lattice2(sK78),k7_filter_2(sK78,X1),k7_filter_2(sK78,X2))
| v1_xboole_0(X3)
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(sK78)))
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(sK78)))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK78))) ),
inference(forward_subsumption_resolution,[],[f49288,f40903]) ).
fof(f49309,definition,
( spl885_42
<=> ! [X3] :
( v1_xboole_0(X3)
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(sK78))) ) ),
introduced(definition,[new_symbols(definition,[spl885_42])],[avatar_definition]) ).
fof(f49310,plain,
( ! [X3] :
( ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(sK78)))
| v1_xboole_0(X3) )
| ~ spl885_42 ),
inference(avatar_component_clause,[],[f49309]) ).
fof(f49312,definition,
( spl885_43
<=> ! [X2,X1] :
( k20_filter_2(sK78,X1,X2) = k5_filter_0(k1_lattice2(sK78),k7_filter_2(sK78,X1),k7_filter_2(sK78,X2))
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK78)))
| v1_xboole_0(X1)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(sK78)))
| v1_xboole_0(X2) ) ),
introduced(definition,[new_symbols(definition,[spl885_43])],[avatar_definition]) ).
fof(f49313,plain,
( ! [X2,X1] :
( ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(sK78)))
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK78)))
| v1_xboole_0(X1)
| k20_filter_2(sK78,X1,X2) = k5_filter_0(k1_lattice2(sK78),k7_filter_2(sK78,X1),k7_filter_2(sK78,X2))
| v1_xboole_0(X2) )
| ~ spl885_43 ),
inference(avatar_component_clause,[],[f49312]) ).
fof(f49314,plain,
( spl885_42
| spl885_43
| spl885_42 ),
inference(avatar_split_clause,[],[f49297,f49309,f49312,f49309]) ).
fof(f49315,plain,
( ! [X0] :
( v1_xboole_0(X0)
| ~ m2_lattice4(X0,sK78)
| v3_struct_0(sK78)
| ~ v10_lattices(sK78)
| ~ l3_lattices(sK78) )
| ~ spl885_42 ),
inference(resolution,[],[f49310,f42321]) ).
fof(f49320,plain,
( ! [X0] :
( v1_xboole_0(X0)
| ~ m2_lattice4(X0,sK78)
| ~ v10_lattices(sK78)
| ~ l3_lattices(sK78) )
| ~ spl885_42 ),
inference(forward_subsumption_resolution,[],[f49315,f40905]) ).
fof(f49322,plain,
( ! [X0] :
( v1_xboole_0(X0)
| ~ m2_lattice4(X0,sK78)
| ~ l3_lattices(sK78) )
| ~ spl885_42 ),
inference(forward_subsumption_resolution,[],[f49320,f40904]) ).
fof(f49324,plain,
( ! [X0] :
( ~ m2_lattice4(X0,sK78)
| v1_xboole_0(X0) )
| ~ spl885_42 ),
inference(forward_subsumption_resolution,[],[f49322,f40903]) ).
fof(f49326,plain,
( v1_xboole_0(sK79)
| ~ spl885_42 ),
inference(resolution,[],[f49324,f49149]) ).
fof(f49330,plain,
( $false
| ~ spl885_42 ),
inference(forward_subsumption_resolution,[],[f49326,f49141]) ).
fof(f49331,plain,
~ spl885_42,
inference(avatar_contradiction_clause,[],[f49330]) ).
fof(f49413,plain,
( v3_struct_0(sK78)
| ~ v10_lattices(sK78)
| ~ l3_lattices(sK78)
| sK79 = k7_filter_2(sK78,sK79) ),
inference(resolution,[],[f49245,f49149]) ).
fof(f49414,plain,
( v3_struct_0(sK78)
| ~ v10_lattices(sK78)
| ~ l3_lattices(sK78)
| sK80 = k7_filter_2(sK78,sK80) ),
inference(resolution,[],[f49245,f49148]) ).
fof(f49415,plain,
( ~ v10_lattices(sK78)
| ~ l3_lattices(sK78)
| sK80 = k7_filter_2(sK78,sK80) ),
inference(forward_subsumption_resolution,[],[f49414,f40905]) ).
fof(f49416,plain,
( ~ v10_lattices(sK78)
| ~ l3_lattices(sK78)
| sK79 = k7_filter_2(sK78,sK79) ),
inference(forward_subsumption_resolution,[],[f49413,f40905]) ).
fof(f49417,plain,
( ~ l3_lattices(sK78)
| sK80 = k7_filter_2(sK78,sK80) ),
inference(forward_subsumption_resolution,[],[f49415,f40904]) ).
fof(f49418,plain,
( ~ l3_lattices(sK78)
| sK79 = k7_filter_2(sK78,sK79) ),
inference(forward_subsumption_resolution,[],[f49416,f40904]) ).
fof(f49419,plain,
sK80 = k7_filter_2(sK78,sK80),
inference(forward_subsumption_resolution,[],[f49417,f40903]) ).
fof(f49420,plain,
sK79 = k7_filter_2(sK78,sK79),
inference(forward_subsumption_resolution,[],[f49418,f40903]) ).
fof(f49421,plain,
( m1_filter_0(sK79,k1_lattice2(sK78))
| ~ spl885_36
| ~ spl885_37
| spl885_38 ),
inference(superposition,[],[f49232,f49420]) ).
fof(f49423,plain,
( m1_filter_0(sK80,k1_lattice2(sK78))
| ~ spl885_39 ),
inference(superposition,[],[f49200,f49419]) ).
fof(f51357,definition,
( spl885_80
<=> m1_subset_1(sK80,k1_zfmisc_1(u1_struct_0(sK78))) ),
introduced(definition,[new_symbols(definition,[spl885_80])],[avatar_definition]) ).
fof(f51358,plain,
( m1_subset_1(sK80,k1_zfmisc_1(u1_struct_0(sK78)))
| ~ spl885_80 ),
inference(avatar_component_clause,[],[f51357]) ).
fof(f51359,plain,
( ~ m1_subset_1(sK80,k1_zfmisc_1(u1_struct_0(sK78)))
| spl885_80 ),
inference(avatar_component_clause,[],[f51357]) ).
fof(f51365,definition,
( spl885_82
<=> m1_subset_1(sK79,k1_zfmisc_1(u1_struct_0(sK78))) ),
introduced(definition,[new_symbols(definition,[spl885_82])],[avatar_definition]) ).
fof(f51366,plain,
( m1_subset_1(sK79,k1_zfmisc_1(u1_struct_0(sK78)))
| ~ spl885_82 ),
inference(avatar_component_clause,[],[f51365]) ).
fof(f51367,plain,
( ~ m1_subset_1(sK79,k1_zfmisc_1(u1_struct_0(sK78)))
| spl885_82 ),
inference(avatar_component_clause,[],[f51365]) ).
fof(f51372,plain,
( ~ m2_lattice4(sK79,sK78)
| v3_struct_0(sK78)
| ~ v10_lattices(sK78)
| ~ l3_lattices(sK78)
| spl885_82 ),
inference(resolution,[],[f51367,f42321]) ).
fof(f51378,plain,
( v3_struct_0(sK78)
| ~ v10_lattices(sK78)
| ~ l3_lattices(sK78)
| spl885_82 ),
inference(forward_subsumption_resolution,[],[f51372,f49149]) ).
fof(f51384,plain,
( ~ v10_lattices(sK78)
| ~ l3_lattices(sK78)
| spl885_82 ),
inference(forward_subsumption_resolution,[],[f51378,f40905]) ).
fof(f51386,plain,
( ~ l3_lattices(sK78)
| spl885_82 ),
inference(forward_subsumption_resolution,[],[f51384,f40904]) ).
fof(f51388,plain,
( $false
| spl885_82 ),
inference(forward_subsumption_resolution,[],[f51386,f40903]) ).
fof(f51389,plain,
spl885_82,
inference(avatar_contradiction_clause,[],[f51388]) ).
fof(f51445,plain,
( ~ m2_lattice4(sK80,sK78)
| v3_struct_0(sK78)
| ~ v10_lattices(sK78)
| ~ l3_lattices(sK78)
| spl885_80 ),
inference(resolution,[],[f51359,f42321]) ).
fof(f51449,plain,
( v3_struct_0(sK78)
| ~ v10_lattices(sK78)
| ~ l3_lattices(sK78)
| spl885_80 ),
inference(forward_subsumption_resolution,[],[f51445,f49148]) ).
fof(f51455,plain,
( ~ v10_lattices(sK78)
| ~ l3_lattices(sK78)
| spl885_80 ),
inference(forward_subsumption_resolution,[],[f51449,f40905]) ).
fof(f51457,plain,
( ~ l3_lattices(sK78)
| spl885_80 ),
inference(forward_subsumption_resolution,[],[f51455,f40904]) ).
fof(f51459,plain,
( $false
| spl885_80 ),
inference(forward_subsumption_resolution,[],[f51457,f40903]) ).
fof(f51460,plain,
spl885_80,
inference(avatar_contradiction_clause,[],[f51459]) ).
fof(f51461,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK78)))
| v1_xboole_0(X0)
| k20_filter_2(sK78,X0,sK80) = k5_filter_0(k1_lattice2(sK78),k7_filter_2(sK78,X0),k7_filter_2(sK78,sK80))
| v1_xboole_0(sK80) )
| ~ spl885_43
| ~ spl885_80 ),
inference(resolution,[],[f51358,f49313]) ).
fof(f51490,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK78)))
| v1_xboole_0(X0)
| k20_filter_2(sK78,X0,sK80) = k5_filter_0(k1_lattice2(sK78),k7_filter_2(sK78,X0),k7_filter_2(sK78,sK80)) )
| ~ spl885_43
| ~ spl885_80 ),
inference(forward_subsumption_resolution,[],[f51461,f49140]) ).
fof(f51501,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK78)))
| k20_filter_2(sK78,X0,sK80) = k5_filter_0(k1_lattice2(sK78),k7_filter_2(sK78,X0),sK80)
| v1_xboole_0(X0) )
| ~ spl885_43
| ~ spl885_80 ),
inference(forward_demodulation,[],[f51490,f49419]) ).
fof(f51525,plain,
( k20_filter_2(sK78,sK79,sK80) = k5_filter_0(k1_lattice2(sK78),k7_filter_2(sK78,sK79),sK80)
| v1_xboole_0(sK79)
| ~ spl885_43
| ~ spl885_80
| ~ spl885_82 ),
inference(resolution,[],[f51501,f51366]) ).
fof(f51529,plain,
( k20_filter_2(sK78,sK79,sK80) = k5_filter_0(k1_lattice2(sK78),k7_filter_2(sK78,sK79),sK80)
| ~ spl885_43
| ~ spl885_80
| ~ spl885_82 ),
inference(forward_subsumption_resolution,[],[f51525,f49141]) ).
fof(f51537,plain,
( k20_filter_2(sK78,sK79,sK80) = k5_filter_0(k1_lattice2(sK78),sK79,sK80)
| ~ spl885_43
| ~ spl885_80
| ~ spl885_82 ),
inference(forward_demodulation,[],[f51529,f49420]) ).
fof(f51574,plain,
( r1_tarski(sK80,k20_filter_2(sK78,sK79,sK80))
| ~ m1_filter_0(sK80,k1_lattice2(sK78))
| ~ m1_filter_0(sK79,k1_lattice2(sK78))
| v3_struct_0(k1_lattice2(sK78))
| ~ v10_lattices(k1_lattice2(sK78))
| ~ l3_lattices(k1_lattice2(sK78))
| ~ spl885_43
| ~ spl885_80
| ~ spl885_82 ),
inference(superposition,[],[f42363,f51537]) ).
fof(f51575,plain,
( r1_tarski(sK79,k20_filter_2(sK78,sK79,sK80))
| ~ m1_filter_0(sK80,k1_lattice2(sK78))
| ~ m1_filter_0(sK79,k1_lattice2(sK78))
| v3_struct_0(k1_lattice2(sK78))
| ~ v10_lattices(k1_lattice2(sK78))
| ~ l3_lattices(k1_lattice2(sK78))
| ~ spl885_43
| ~ spl885_80
| ~ spl885_82 ),
inference(superposition,[],[f42364,f51537]) ).
fof(f51576,plain,
( ~ m1_filter_0(sK80,k1_lattice2(sK78))
| ~ m1_filter_0(sK79,k1_lattice2(sK78))
| v3_struct_0(k1_lattice2(sK78))
| ~ v10_lattices(k1_lattice2(sK78))
| ~ l3_lattices(k1_lattice2(sK78))
| spl885_35
| ~ spl885_43
| ~ spl885_80
| ~ spl885_82 ),
inference(forward_subsumption_resolution,[],[f51575,f48814]) ).
fof(f51577,plain,
( r1_tarski(sK80,k20_filter_2(sK78,sK79,sK80))
| ~ m1_filter_0(sK79,k1_lattice2(sK78))
| v3_struct_0(k1_lattice2(sK78))
| ~ v10_lattices(k1_lattice2(sK78))
| ~ l3_lattices(k1_lattice2(sK78))
| ~ spl885_39
| ~ spl885_43
| ~ spl885_80
| ~ spl885_82 ),
inference(forward_subsumption_resolution,[],[f51574,f49423]) ).
fof(f51579,plain,
( ~ m1_filter_0(sK79,k1_lattice2(sK78))
| v3_struct_0(k1_lattice2(sK78))
| ~ v10_lattices(k1_lattice2(sK78))
| ~ l3_lattices(k1_lattice2(sK78))
| spl885_35
| ~ spl885_39
| ~ spl885_43
| ~ spl885_80
| ~ spl885_82 ),
inference(forward_subsumption_resolution,[],[f51576,f49423]) ).
fof(f51580,plain,
( r1_tarski(sK80,k20_filter_2(sK78,sK79,sK80))
| v3_struct_0(k1_lattice2(sK78))
| ~ v10_lattices(k1_lattice2(sK78))
| ~ l3_lattices(k1_lattice2(sK78))
| ~ spl885_36
| ~ spl885_37
| spl885_38
| ~ spl885_39
| ~ spl885_43
| ~ spl885_80
| ~ spl885_82 ),
inference(forward_subsumption_resolution,[],[f51577,f49421]) ).
fof(f51582,plain,
( v3_struct_0(k1_lattice2(sK78))
| ~ v10_lattices(k1_lattice2(sK78))
| ~ l3_lattices(k1_lattice2(sK78))
| spl885_35
| ~ spl885_36
| ~ spl885_37
| spl885_38
| ~ spl885_39
| ~ spl885_43
| ~ spl885_80
| ~ spl885_82 ),
inference(forward_subsumption_resolution,[],[f51579,f49421]) ).
fof(f51583,plain,
( r1_tarski(sK80,k20_filter_2(sK78,sK79,sK80))
| ~ v10_lattices(k1_lattice2(sK78))
| ~ l3_lattices(k1_lattice2(sK78))
| ~ spl885_36
| ~ spl885_37
| spl885_38
| ~ spl885_39
| ~ spl885_43
| ~ spl885_80
| ~ spl885_82 ),
inference(forward_subsumption_resolution,[],[f51580,f49195]) ).
fof(f51585,plain,
( ~ v10_lattices(k1_lattice2(sK78))
| ~ l3_lattices(k1_lattice2(sK78))
| spl885_35
| ~ spl885_36
| ~ spl885_37
| spl885_38
| ~ spl885_39
| ~ spl885_43
| ~ spl885_80
| ~ spl885_82 ),
inference(forward_subsumption_resolution,[],[f51582,f49195]) ).
fof(f51586,plain,
( r1_tarski(sK80,k20_filter_2(sK78,sK79,sK80))
| ~ l3_lattices(k1_lattice2(sK78))
| ~ spl885_36
| ~ spl885_37
| spl885_38
| ~ spl885_39
| ~ spl885_43
| ~ spl885_80
| ~ spl885_82 ),
inference(forward_subsumption_resolution,[],[f51583,f49191]) ).
fof(f51588,plain,
( ~ l3_lattices(k1_lattice2(sK78))
| spl885_35
| ~ spl885_36
| ~ spl885_37
| spl885_38
| ~ spl885_39
| ~ spl885_43
| ~ spl885_80
| ~ spl885_82 ),
inference(forward_subsumption_resolution,[],[f51585,f49191]) ).
fof(f51589,plain,
( r1_tarski(sK80,k20_filter_2(sK78,sK79,sK80))
| ~ spl885_36
| ~ spl885_37
| spl885_38
| ~ spl885_39
| ~ spl885_43
| ~ spl885_80
| ~ spl885_82 ),
inference(forward_subsumption_resolution,[],[f51586,f49187]) ).
fof(f51591,plain,
( $false
| spl885_35
| ~ spl885_36
| ~ spl885_37
| spl885_38
| ~ spl885_39
| ~ spl885_43
| ~ spl885_80
| ~ spl885_82 ),
inference(forward_subsumption_resolution,[],[f51588,f49187]) ).
fof(f51592,plain,
( spl885_35
| ~ spl885_36
| ~ spl885_37
| spl885_38
| ~ spl885_39
| ~ spl885_43
| ~ spl885_80
| ~ spl885_82 ),
inference(avatar_contradiction_clause,[],[f51591]) ).
fof(f51593,plain,
( spl885_34
| ~ spl885_36
| ~ spl885_37
| spl885_38
| ~ spl885_39
| ~ spl885_43
| ~ spl885_80
| ~ spl885_82 ),
inference(avatar_split_clause,[],[f51589,f51365,f51357,f49312,f49198,f49194,f49190,f49186,f48808]) ).
cnf(s33,plain,
( ~ spl885_34
| ~ spl885_35 ),
inference(sat_conversion,[],[f48815]) ).
cnf(s34,plain,
( ~ spl885_36
| ~ spl885_37
| spl885_38
| spl885_39 ),
inference(sat_conversion,[],[f49201]) ).
cnf(s35,plain,
spl885_36,
inference(sat_conversion,[],[f49204]) ).
cnf(s36,plain,
spl885_37,
inference(sat_conversion,[],[f49225]) ).
cnf(s37,plain,
~ spl885_38,
inference(sat_conversion,[],[f49229]) ).
cnf(s40,plain,
( spl885_42
| spl885_42
| spl885_43 ),
inference(sat_conversion,[],[f49314]) ).
cnf(s41,plain,
( spl885_42
| spl885_43 ),
inference(rat,[],[s40]) ).
cnf(s43,plain,
~ spl885_42,
inference(sat_conversion,[],[f49331]) ).
cnf(s83,plain,
spl885_82,
inference(sat_conversion,[],[f51389]) ).
cnf(s87,plain,
spl885_80,
inference(sat_conversion,[],[f51460]) ).
cnf(s88,plain,
( spl885_35
| ~ spl885_36
| ~ spl885_37
| spl885_38
| ~ spl885_39
| ~ spl885_43
| ~ spl885_80
| ~ spl885_82 ),
inference(sat_conversion,[],[f51592]) ).
cnf(s89,plain,
( spl885_34
| ~ spl885_36
| ~ spl885_37
| spl885_38
| ~ spl885_39
| ~ spl885_43
| ~ spl885_80
| ~ spl885_82 ),
inference(sat_conversion,[],[f51593]) ).
cnf(s99,plain,
spl885_43,
inference(rat,[],[s41,s43]) ).
cnf(s108,plain,
spl885_39,
inference(rat,[],[s34,s37,s36,s35]) ).
cnf(s111,plain,
spl885_34,
inference(rat,[],[s89,s83,s87,s99,s35,s37,s36,s108]) ).
cnf(s112,plain,
spl885_35,
inference(rat,[],[s88,s83,s87,s99,s35,s37,s36,s108]) ).
cnf(s113,plain,
$false,
inference(rat,[],[s33,s112,s111]) ).
fof(f51599,plain,
$false,
inference(avatar_sat_refutation,[],[s113]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT317+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.40 % Computer : n005.cluster.edu
% 0.12/0.40 % Model : x86_64 x86_64
% 0.12/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.40 % Memory : 8046.5625MB
% 0.12/0.40 % OS : Linux 6.8.0-71-generic
% 0.12/0.40 % CPULimit : 300
% 0.12/0.40 % WCLimit : 300
% 0.12/0.40 % DateTime : Sun Sep 27 14:33:23 UTC 2026
% 0.12/0.40 % CPUTime :
% 0.12/0.40 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.44 Running first-order theorem proving
% 0.12/0.44 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
% 15.40/4.98 % (4051926)Detected formulas, will run a generic FOF schedule.
% 15.40/4.98 % (4051936)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2965853394:s2a=on:i=139:gtg=position_2978 on theBenchmark for (2978ds/139Mi)
% 15.40/4.98 % (4051933)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=1079401586:i=141695:sd=1:nm=32:gsp=on:ss=included_2978 on theBenchmark for (2978ds/141695Mi)
% 15.40/4.98 % (4051932)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=3160763025:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2978 on theBenchmark for (2978ds/134677Mi)
% 15.40/4.98 % (4051931)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=2377416350:i=141193_2978 on theBenchmark for (2978ds/141193Mi)
% 15.40/4.98 % (4051935)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1460050553:i=119:av=off:ss=axioms_2978 on theBenchmark for (2978ds/119Mi)
% 15.40/4.98 % (4051937)dis-21_1_sil=8000:lcm=predicate:random_seed=3683026326:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2978 on theBenchmark for (2978ds/129Mi)
% 15.40/4.98 % (4051934)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=4050260834:i=109:sd=1:ins=1:gsp=on:ss=axioms_2978 on theBenchmark for (2978ds/109Mi)
% 15.40/4.98 % (4051936)Instruction limit reached!
% 15.40/4.98 % (4051936)------------------------------
% 15.40/4.98 % (4051936)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.40/4.98 % (4051936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.40/4.98 % (4051936)CaDiCaL version: 2.1.3
% 15.40/4.98 % (4051936)Termination reason: Instruction limit
% 15.40/4.98 % (4051936)Termination phase: Property scanning
% 15.40/4.98 % (4051936)Time elapsed: 0.034 s
% 15.40/4.98 % (4051936)Peak memory usage: 136 MB
% 15.40/4.98 % (4051936)Instructions burned: 141 (million)
% 15.40/4.98 % (4051934)Instruction limit reached!
% 15.40/4.98 % (4051934)------------------------------
% 15.40/4.98 % (4051934)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.40/4.98 % (4051934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.40/4.98 % (4051934)CaDiCaL version: 2.1.3
% 15.40/4.98 % (4051934)Termination reason: Instruction limit
% 15.40/4.98 % (4051934)Termination phase: SInE selection
% 15.40/4.98 % (4051934)Time elapsed: 0.079 s
% 15.40/4.98 % (4051934)Peak memory usage: 136 MB
% 15.40/4.98 % (4051934)Instructions burned: 109 (million)
% 15.40/4.98 % (4051935)Instruction limit reached!
% 15.40/4.98 % (4051935)------------------------------
% 15.40/4.98 % (4051935)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.40/4.98 % (4051935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.40/4.98 % (4051935)CaDiCaL version: 2.1.3
% 15.40/4.98 % (4051935)Termination reason: Instruction limit
% 15.40/4.98 % (4051935)Termination phase: SInE selection
% 15.40/4.98 % (4051935)Time elapsed: 0.084 s
% 15.40/4.98 % (4051935)Peak memory usage: 136 MB
% 15.40/4.98 % (4051935)Instructions burned: 119 (million)
% 15.40/4.98 % (4051937)Instruction limit reached!
% 15.40/4.98 % (4051937)------------------------------
% 15.40/4.98 % (4051937)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.40/4.98 % (4051937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.40/4.98 % (4051937)CaDiCaL version: 2.1.3
% 15.40/4.98 % (4051937)Termination reason: Instruction limit
% 15.40/4.98 % (4051937)Termination phase: SInE selection
% 15.40/4.98 % (4051937)Time elapsed: 0.090 s
% 15.40/4.98 % (4051937)Peak memory usage: 136 MB
% 15.40/4.98 % (4051937)Instructions burned: 131 (million)
% 15.40/4.98 % (4051945)lrs+10_1_sil=8000:sp=occurrence:random_seed=4188096678:i=285:sd=3:ss=axioms:sgt=8_2976 on theBenchmark for (2976ds/285Mi)
% 15.40/4.98 % (4051947)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2962290979:i=325:sd=1:ss=axioms:sgt=32_2975 on theBenchmark for (2975ds/325Mi)
% 15.40/4.98 % (4051946)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1525624614:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2975 on theBenchmark for (2975ds/157Mi)
% 15.40/4.98 % (4051945)Instruction limit reached!
% 15.40/4.98 % (4051945)------------------------------
% 15.40/4.98 % (4051945)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.40/4.98 % (4051945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.76/6.12 % (4051945)CaDiCaL version: 2.1.3
% 23.76/6.12 % (4051945)Termination reason: Instruction limit
% 23.76/6.12 % (4051945)Termination phase: Saturation
% 23.76/6.12 % (4051945)Time elapsed: 0.128 s
% 23.76/6.12 % (4051945)Peak memory usage: 142 MB
% 23.76/6.12 % (4051945)Instructions burned: 285 (million)
% 23.76/6.12 % (4051948)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=3376077810:s2a=on:i=248:s2at=1.23:gtg=position_2975 on theBenchmark for (2975ds/248Mi)
% 23.76/6.12 % (4051946)Instruction limit reached!
% 23.76/6.12 % (4051946)------------------------------
% 23.76/6.12 % (4051946)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.76/6.12 % (4051946)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.76/6.12 % (4051946)CaDiCaL version: 2.1.3
% 23.76/6.12 % (4051946)Termination reason: Instruction limit
% 23.76/6.12 % (4051946)Termination phase: Property scanning
% 23.76/6.12 % (4051946)Time elapsed: 0.071 s
% 23.76/6.12 % (4051946)Peak memory usage: 136 MB
% 23.76/6.12 % (4051946)Instructions burned: 158 (million)
% 23.76/6.12 % (4051948)Instruction limit reached!
% 23.76/6.12 % (4051948)------------------------------
% 23.76/6.12 % (4051948)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.76/6.12 % (4051948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.76/6.12 % (4051948)CaDiCaL version: 2.1.3
% 23.76/6.12 % (4051948)Termination reason: Instruction limit
% 23.76/6.12 % (4051948)Termination phase: Property scanning
% 23.76/6.12 % (4051948)Time elapsed: 0.109 s
% 23.76/6.12 % (4051948)Peak memory usage: 136 MB
% 23.76/6.12 % (4051948)Instructions burned: 248 (million)
% 23.76/6.12 % (4051953)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2110699193:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2973 on theBenchmark for (2973ds/294Mi)
% 23.76/6.12 % (4051954)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=816886786:i=2350_2973 on theBenchmark for (2973ds/2350Mi)
% 23.76/6.12 % (4051947)Instruction limit reached!
% 23.76/6.12 % (4051947)------------------------------
% 23.76/6.12 % (4051947)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.76/6.12 % (4051947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.76/6.12 % (4051947)CaDiCaL version: 2.1.3
% 23.76/6.12 % (4051947)Termination reason: Instruction limit
% 23.76/6.12 % (4051947)Termination phase: Saturation
% 23.76/6.12 % (4051947)Time elapsed: 0.253 s
% 23.76/6.12 % (4051947)Peak memory usage: 142 MB
% 23.76/6.12 % (4051947)Instructions burned: 325 (million)
% 23.76/6.12 % (4051953)Instruction limit reached!
% 23.76/6.12 % (4051953)------------------------------
% 23.76/6.12 % (4051953)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.76/6.12 % (4051953)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.76/6.12 % (4051953)CaDiCaL version: 2.1.3
% 23.76/6.12 % (4051953)Termination reason: Instruction limit
% 23.76/6.12 % (4051953)Termination phase: SInE selection
% 23.76/6.12 % (4051953)Time elapsed: 0.105 s
% 23.76/6.12 % (4051953)Peak memory usage: 137 MB
% 23.76/6.12 % (4051953)Instructions burned: 297 (million)
% 23.76/6.12 % (4051955)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1341245612:cts=off:i=113:fsr=off:ss=included:sgt=4_2972 on theBenchmark for (2972ds/113Mi)
% 23.76/6.12 % (4051959)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=4209433541:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2971 on theBenchmark for (2971ds/114Mi)
% 23.76/6.12 % (4051955)Instruction limit reached!
% 23.76/6.12 % (4051955)------------------------------
% 23.76/6.12 % (4051955)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.76/6.12 % (4051955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.76/6.12 % (4051955)CaDiCaL version: 2.1.3
% 23.76/6.12 % (4051955)Termination reason: Instruction limit
% 23.76/6.12 % (4051955)Termination phase: SInE selection
% 23.76/6.12 % (4051955)Time elapsed: 0.091 s
% 23.76/6.12 % (4051955)Peak memory usage: 136 MB
% 23.76/6.12 % (4051955)Instructions burned: 113 (million)
% 23.76/6.12 % (4051958)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=307677258:i=127:av=off:fsr=off:sup=off_2971 on theBenchmark for (2971ds/127Mi)
% 23.76/6.12 % (4051959)Instruction limit reached!
% 23.76/6.12 % (4051959)------------------------------
% 23.76/6.12 % (4051959)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.97/8.24 % (4051959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.97/8.24 % (4051959)CaDiCaL version: 2.1.3
% 20.97/8.24 % (4051959)Termination reason: Instruction limit
% 20.97/8.24 % (4051959)Termination phase: Property scanning
% 20.97/8.24 % (4051959)Time elapsed: 0.030 s
% 20.97/8.24 % (4051959)Peak memory usage: 136 MB
% 20.97/8.24 % (4051959)Instructions burned: 116 (million)
% 20.97/8.24 % (4051958)Instruction limit reached!
% 20.97/8.24 % (4051958)------------------------------
% 20.97/8.24 % (4051958)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.97/8.24 % (4051958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.97/8.24 % (4051958)CaDiCaL version: 2.1.3
% 20.97/8.24 % (4051958)Termination reason: Instruction limit
% 20.97/8.24 % (4051958)Termination phase: Preprocessing 1
% 20.97/8.24 % (4051958)Time elapsed: 0.096 s
% 20.97/8.24 % (4051958)Peak memory usage: 137 MB
% 20.97/8.24 % (4051958)Instructions burned: 128 (million)
% 20.97/8.24 % (4051962)lrs+10_1_sil=8000:sp=occurrence:random_seed=1405555830:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2970 on theBenchmark for (2970ds/907Mi)
% 20.97/8.24 % (4051964)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3714265351:i=437:sd=1:aac=none:ss=included_2969 on theBenchmark for (2969ds/437Mi)
% 20.97/8.24 % (4051965)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3413526390:i=5202:ss=axioms:sgt=16_2968 on theBenchmark for (2968ds/5202Mi)
% 20.97/8.24 % (4051964)Instruction limit reached!
% 20.97/8.24 % (4051964)------------------------------
% 20.97/8.24 % (4051964)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.97/8.24 % (4051964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.97/8.24 % (4051964)CaDiCaL version: 2.1.3
% 20.97/8.24 % (4051964)Termination reason: Instruction limit
% 20.97/8.24 % (4051964)Termination phase: Saturation
% 20.97/8.24 % (4051964)Time elapsed: 0.181 s
% 20.97/8.24 % (4051964)Peak memory usage: 143 MB
% 20.97/8.24 % (4051964)Instructions burned: 438 (million)
% 20.97/8.24 % (4051969)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1269798259:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2966 on theBenchmark for (2966ds/134Mi)
% 20.97/8.24 % (4051969)Instruction limit reached!
% 20.97/8.24 % (4051969)------------------------------
% 20.97/8.24 % (4051969)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.97/8.24 % (4051969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.97/8.24 % (4051969)CaDiCaL version: 2.1.3
% 20.97/8.24 % (4051969)Termination reason: Instruction limit
% 20.97/8.24 % (4051969)Termination phase: SInE selection
% 20.97/8.24 % (4051969)Time elapsed: 0.057 s
% 20.97/8.24 % (4051969)Peak memory usage: 136 MB
% 20.97/8.24 % (4051969)Instructions burned: 135 (million)
% 20.97/8.24 % (4051971)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3477337488:st=8:i=592:sd=3:ep=RST:ss=axioms_2964 on theBenchmark for (2964ds/592Mi)
% 20.97/8.24 % (4051962)Instruction limit reached!
% 20.97/8.24 % (4051962)------------------------------
% 20.97/8.24 % (4051962)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.97/8.24 % (4051962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.97/8.24 % (4051962)CaDiCaL version: 2.1.3
% 20.97/8.24 % (4051962)Termination reason: Instruction limit
% 20.97/8.24 % (4051962)Termination phase: Property scanning
% 20.97/8.24 % (4051962)Time elapsed: 0.599 s
% 20.97/8.24 % (4051962)Peak memory usage: 157 MB
% 20.97/8.24 % (4051962)Instructions burned: 908 (million)
% 20.97/8.24 % (4051973)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2237910978:st=3:i=13193:sd=3:ss=axioms_2962 on theBenchmark for (2962ds/13193Mi)
% 20.97/8.24 % (4051971)Instruction limit reached!
% 20.97/8.24 % (4051971)------------------------------
% 20.97/8.24 % (4051971)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.97/8.24 % (4051971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.97/8.24 % (4051971)CaDiCaL version: 2.1.3
% 20.97/8.24 % (4051971)Termination reason: Instruction limit
% 20.97/8.24 % (4051971)Termination phase: Preprocessing 2
% 20.97/8.24 % (4051971)Time elapsed: 0.291 s
% 20.97/8.24 % (4051971)Peak memory usage: 154 MB
% 20.97/8.24 % (4051971)Instructions burned: 593 (million)
% 20.97/8.24 % (4051975)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=105814194:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2960 on theBenchmark for (2960ds/125Mi)
% 20.97/8.24 % (4051975)Instruction limit reached!
% 20.97/8.24 % (4051975)------------------------------
% 20.97/8.24 % (4051975)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.97/8.24 % (4051975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.97/8.24 % (4051975)CaDiCaL version: 2.1.3
% 20.97/8.24 % (4051975)Termination reason: Instruction limit
% 20.97/8.24 % (4051975)Termination phase: Property scanning
% 20.97/8.24 % (4051975)Time elapsed: 0.030 s
% 20.97/8.24 % (4051975)Peak memory usage: 136 MB
% 20.97/8.24 % (4051975)Instructions burned: 126 (million)
% 20.97/8.24 % (4051977)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2464679853:i=134:gtgl=5:slsql=off:gtg=exists_sym_2958 on theBenchmark for (2958ds/134Mi)
% 20.97/8.24 % (4051977)Instruction limit reached!
% 20.97/8.24 % (4051977)------------------------------
% 20.97/8.24 % (4051977)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.97/8.24 % (4051977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.97/8.24 % (4051977)CaDiCaL version: 2.1.3
% 20.97/8.24 % (4051977)Termination reason: Instruction limit
% 20.97/8.24 % (4051977)Termination phase: Property scanning
% 20.97/8.24 % (4051977)Time elapsed: 0.033 s
% 20.97/8.24 % (4051977)Peak memory usage: 136 MB
% 20.97/8.24 % (4051977)Instructions burned: 136 (million)
% 20.97/8.24 % (4051979)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3630190342:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2957 on theBenchmark for (2957ds/141Mi)
% 20.97/8.24 % (4051954)Instruction limit reached!
% 20.97/8.24 % (4051954)------------------------------
% 20.97/8.24 % (4051954)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.97/8.24 % (4051954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.97/8.24 % (4051954)CaDiCaL version: 2.1.3
% 20.97/8.24 % (4051954)Termination reason: Instruction limit
% 20.97/8.24 % (4051954)Termination phase: Property scanning
% 20.97/8.24 % (4051954)Time elapsed: 1.607 s
% 20.97/8.24 % (4051954)Peak memory usage: 233 MB
% 20.97/8.24 % (4051954)Instructions burned: 2351 (million)
% 20.97/8.24 % (4051979)Instruction limit reached!
% 20.97/8.24 % (4051979)------------------------------
% 20.97/8.24 % (4051979)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.97/8.24 % (4051979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.97/8.24 % (4051979)CaDiCaL version: 2.1.3
% 20.97/8.24 % (4051979)Termination reason: Instruction limit
% 20.97/8.24 % (4051979)Termination phase: SInE selection
% 20.97/8.24 % (4051979)Time elapsed: 0.060 s
% 20.97/8.24 % (4051979)Peak memory usage: 136 MB
% 20.97/8.24 % (4051979)Instructions burned: 143 (million)
% 20.97/8.24 % (4051982)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=221187164:i=6060:aac=none:ins=25_2955 on theBenchmark for (2955ds/6060Mi)
% 20.97/8.24 % (4051981)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2929513761:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2955 on theBenchmark for (2955ds/431Mi)
% 20.97/8.24 % (4051981)Instruction limit reached!
% 20.97/8.24 % (4051981)------------------------------
% 20.97/8.24 % (4051981)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.97/8.24 % (4051981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.97/8.24 % (4051981)CaDiCaL version: 2.1.3
% 20.97/8.24 % (4051981)Termination reason: Instruction limit
% 20.97/8.24 % (4051981)Termination phase: Saturation
% 20.97/8.24 % (4051981)Time elapsed: 0.326 s
% 20.97/8.24 % (4051981)Peak memory usage: 144 MB
% 20.97/8.24 % (4051981)Instructions burned: 432 (million)
% 20.97/8.24 % (4051985)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=3328878443:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2950 on theBenchmark for (2950ds/150Mi)
% 20.97/8.24 % (4051985)Instruction limit reached!
% 20.97/8.24 % (4051985)------------------------------
% 20.97/8.24 % (4051985)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.97/8.24 % (4051985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.97/8.24 % (4051985)CaDiCaL version: 2.1.3
% 20.97/8.24 % (4051985)Termination reason: Instruction limit
% 20.97/8.24 % (4051985)Termination phase: SInE selection
% 20.97/8.24 % (4051985)Time elapsed: 0.117 s
% 20.97/8.24 % (4051985)Peak memory usage: 136 MB
% 20.97/8.24 % (4051985)Instructions burned: 151 (million)
% 20.97/8.24 % (4051987)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=82507949:i=14155:bd=all_2947 on theBenchmark for (2947ds/14155Mi)
% 20.97/8.24 % (4051982)Instruction limit reached!
% 20.97/8.24 % (4051982)------------------------------
% 20.97/8.24 % (4051982)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.97/8.24 % (4051982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.97/8.24 % (4051982)CaDiCaL version: 2.1.3
% 20.97/8.24 % (4051982)Termination reason: Instruction limit
% 20.97/8.24 % (4051982)Termination phase: Function definition elimination
% 20.97/8.24 % (4051982)Time elapsed: 2.180 s
% 20.97/8.24 % (4051982)Peak memory usage: 245 MB
% 20.97/8.24 % (4051982)Instructions burned: 6064 (million)
% 20.97/8.24 % (4051989)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3092952485:i=667:av=off:fsr=off_2931 on theBenchmark for (2931ds/667Mi)
% 20.97/8.24 % (4051973)First to succeed.
% 20.97/8.24 % (4051973)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-4051926"
% 20.97/8.24 % (4051965)Instruction limit reached!
% 20.97/8.24 % (4051965)------------------------------
% 20.97/8.24 % (4051965)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.97/8.24 % (4051965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.97/8.24 % (4051965)CaDiCaL version: 2.1.3
% 20.97/8.24 % (4051965)Termination reason: Instruction limit
% 20.97/8.24 % (4051965)Termination phase: Saturation
% 20.97/8.24 % (4051965)Time elapsed: 3.859 s
% 20.97/8.24 % (4051965)Peak memory usage: 613 MB
% 20.97/8.24 % (4051965)Instructions burned: 5203 (million)
% 20.97/8.24 % (4051973)Refutation found. Thanks to Tanya!
% 20.97/8.24 % SZS status Theorem for theBenchmark
% 20.97/8.24 % SZS output start Proof for theBenchmark
% See solution above
% 39.41/8.48 % (4051973)------------------------------
% 39.41/8.48 % (4051973)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.41/8.48 % (4051973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.41/8.48 % (4051973)CaDiCaL version: 2.1.3
% 39.41/8.48 % (4051973)Termination reason: Refutation
% 39.41/8.48 % (4051973)Time elapsed: 3.080 s
% 39.41/8.48 % (4051973)Peak memory usage: 272 MB
% 39.41/8.48 % (4051973)Instructions burned: 4826 (million)
% 39.41/8.48 % (4051973)------------------------------
% 39.41/8.48 % (4051973)------------------------------
% 39.41/8.48 % (4051926)Success in time 7.36 s
% 39.41/8.48 % Vampire exiting
%------------------------------------------------------------------------------