%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT329+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 : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:47:00 AM UTC 2026
% Result : Theorem 62.47s 20.78s
% Output : Refutation 0.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 52
% Syntax : Number of formulae : 310 ( 53 unt; 35 def)
% Number of atoms : 1300 ( 33 equ)
% Maximal formula atoms : 13 ( 4 avg)
% Number of connectives : 1739 ( 749 ~; 830 |; 82 &)
% ( 46 <=>; 32 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 46 ( 44 usr; 32 prp; 0-3 aty)
% Number of functors : 13 ( 13 usr; 6 con; 0-3 aty)
% Number of variables : 248 ( 0 sgn 242 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f8,axiom,
! [X0,X1] :
( r1_tarski(X0,X1)
<=> ! [X2] :
( r2_hidden(X2,X0)
=> r2_hidden(X2,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d3_tarski) ).
fof(f38,axiom,
! [X0,X1] :
( X0 = X1
<=> ( r1_tarski(X0,X1)
& r1_tarski(X1,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d10_xboole_0) ).
fof(f678,axiom,
! [X0,X1,X2] :
( ( r2_hidden(X0,X1)
& m1_subset_1(X1,k1_zfmisc_1(X2)) )
=> m1_subset_1(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t4_subset) ).
fof(f18196,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v14_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> r3_lattices(X0,X1,k6_lattices(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t45_lattices) ).
fof(f21512,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_filter_0(X1,X0)
=> ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v14_lattices(X0)
& l3_lattices(X0) )
=> r2_hidden(k6_lattices(X0),X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t12_filter_0) ).
fof(f21515,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> m1_filter_0(u1_struct_0(X0),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t15_filter_0) ).
fof(f21519,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ( r2_hidden(X1,k2_filter_0(X0,X2))
<=> r3_lattices(X0,X2,X1) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t18_filter_0) ).
fof(f21603,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& m1_subset_1(X1,u1_struct_0(X0)) )
=> m1_filter_0(k2_filter_0(X0,X1),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k2_filter_0) ).
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(f34604,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_filter_2(X1,X0)
=> ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m1_filter_2) ).
fof(f34606,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(f34611,axiom,
! [X0,X1,X2] :
( ( ~ v1_xboole_0(X0)
& m1_subset_1(X1,k1_zfmisc_1(X0))
& m1_subset_1(X2,k1_zfmisc_1(X0)) )
=> ( r1_filter_2(X0,X1,X2)
<=> X1 = X2 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_r1_filter_2) ).
fof(f34614,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& m1_subset_1(X1,u1_struct_0(X0)) )
=> m1_filter_2(k2_filter_2(X0,X1),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k2_filter_2) ).
fof(f34615,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& m1_subset_1(X1,u1_struct_0(X0)) )
=> k2_filter_2(X0,X1) = k2_filter_0(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k2_filter_2) ).
fof(f34646,axiom,
! [X0,X1,X2] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& m1_subset_1(X1,u1_struct_0(X0))
& m1_subset_1(X2,u1_struct_0(X0)) )
=> ( ~ v1_xboole_0(k22_filter_2(X0,X1,X2))
& m2_lattice4(k22_filter_2(X0,X1,X2),X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k22_filter_2) ).
fof(f34733,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
=> ( r3_lattices(X0,X1,X2)
=> ( r2_hidden(X3,k22_filter_2(X0,X1,X2))
<=> ( r3_lattices(X0,X1,X3)
& r3_lattices(X0,X3,X2) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t63_filter_2) ).
fof(f34736,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ( v14_lattices(X0)
=> r1_filter_2(u1_struct_0(X0),k2_filter_2(X0,X1),k22_filter_2(X0,X1,k6_lattices(X0))) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t66_filter_2) ).
fof(f34737,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ( v14_lattices(X0)
=> r1_filter_2(u1_struct_0(X0),k2_filter_2(X0,X1),k22_filter_2(X0,X1,k6_lattices(X0))) ) ) ),
inference(negated_conjecture,[status(cth)],[f34736]) ).
fof(f34866,plain,
? [X0] :
( ? [X1] :
( ~ r1_filter_2(u1_struct_0(X0),k2_filter_2(X0,X1),k22_filter_2(X0,X1,k6_lattices(X0)))
& v14_lattices(X0)
& m1_subset_1(X1,u1_struct_0(X0)) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(ennf_transformation,[],[f34737]) ).
fof(f34867,plain,
? [X0] :
( ? [X1] :
( ~ r1_filter_2(u1_struct_0(X0),k2_filter_2(X0,X1),k22_filter_2(X0,X1,k6_lattices(X0)))
& v14_lattices(X0)
& m1_subset_1(X1,u1_struct_0(X0)) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(flattening,[],[f34866]) ).
fof(f34894,plain,
! [X0] :
( ! [X1] :
( r2_hidden(k6_lattices(X0),X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v14_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f21512]) ).
fof(f34895,plain,
! [X0] :
( ! [X1] :
( r2_hidden(k6_lattices(X0),X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v14_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f34894]) ).
fof(f34896,plain,
! [X0] :
( ! [X1] :
( r3_lattices(X0,X1,k6_lattices(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v14_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f18196]) ).
fof(f34897,plain,
! [X0] :
( ! [X1] :
( r3_lattices(X0,X1,k6_lattices(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v14_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f34896]) ).
fof(f34907,plain,
! [X0,X1,X2] :
( ( r1_filter_2(X0,X1,X2)
<=> X1 = X2 )
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f34611]) ).
fof(f34908,plain,
! [X0,X1,X2] :
( ( r1_filter_2(X0,X1,X2)
<=> X1 = X2 )
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(flattening,[],[f34907]) ).
fof(f34931,plain,
! [X0,X1] :
( k2_filter_2(X0,X1) = k2_filter_0(X0,X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f34615]) ).
fof(f34932,plain,
! [X0,X1] :
( k2_filter_2(X0,X1) = k2_filter_0(X0,X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(flattening,[],[f34931]) ).
fof(f34933,plain,
! [X0,X1] :
( m1_filter_2(k2_filter_2(X0,X1),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f34614]) ).
fof(f34934,plain,
! [X0,X1] :
( m1_filter_2(k2_filter_2(X0,X1),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(flattening,[],[f34933]) ).
fof(f34939,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( r2_hidden(X3,k22_filter_2(X0,X1,X2))
<=> ( r3_lattices(X0,X1,X3)
& r3_lattices(X0,X3,X2) ) )
| ~ r3_lattices(X0,X1,X2)
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f34733]) ).
fof(f34940,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( r2_hidden(X3,k22_filter_2(X0,X1,X2))
<=> ( r3_lattices(X0,X1,X3)
& r3_lattices(X0,X3,X2) ) )
| ~ r3_lattices(X0,X1,X2)
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f34939]) ).
fof(f34941,plain,
! [X0,X1,X2] :
( ( ~ v1_xboole_0(k22_filter_2(X0,X1,X2))
& m2_lattice4(k22_filter_2(X0,X1,X2),X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f34646]) ).
fof(f34942,plain,
! [X0,X1,X2] :
( ( ~ v1_xboole_0(k22_filter_2(X0,X1,X2))
& m2_lattice4(k22_filter_2(X0,X1,X2),X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(flattening,[],[f34941]) ).
fof(f35138,plain,
! [X0] :
( m1_filter_0(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f21515]) ).
fof(f35139,plain,
! [X0] :
( m1_filter_0(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35138]) ).
fof(f35154,plain,
! [X0,X1,X2] :
( m1_subset_1(X0,X2)
| ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2)) ),
inference(ennf_transformation,[],[f678]) ).
fof(f35155,plain,
! [X0,X1,X2] :
( m1_subset_1(X0,X2)
| ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2)) ),
inference(flattening,[],[f35154]) ).
fof(f35446,plain,
! [X0,X1] :
( m1_filter_0(k2_filter_0(X0,X1),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f21603]) ).
fof(f35447,plain,
! [X0,X1] :
( m1_filter_0(k2_filter_0(X0,X1),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(flattening,[],[f35446]) ).
fof(f35468,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( r2_hidden(X1,k2_filter_0(X0,X2))
<=> r3_lattices(X0,X2,X1) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f21519]) ).
fof(f35469,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( r2_hidden(X1,k2_filter_0(X0,X2))
<=> r3_lattices(X0,X2,X1) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35468]) ).
fof(f35474,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,[],[f34606]) ).
fof(f35475,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,[],[f35474]) ).
fof(f35478,plain,
! [X0] :
( ! [X1] :
( ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) )
| ~ m1_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f34604]) ).
fof(f35479,plain,
! [X0] :
( ! [X1] :
( ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) )
| ~ m1_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35478]) ).
fof(f35488,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(f35489,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,[],[f35488]) ).
fof(f35910,plain,
! [X0,X1] :
( r1_tarski(X0,X1)
<=> ! [X2] :
( r2_hidden(X2,X1)
| ~ r2_hidden(X2,X0) ) ),
inference(ennf_transformation,[],[f8]) ).
fof(f36574,plain,
( ~ r1_filter_2(u1_struct_0(sK45),k2_filter_2(sK45,sK46),k22_filter_2(sK45,sK46,k6_lattices(sK45)))
& v14_lattices(sK45)
& m1_subset_1(sK46,u1_struct_0(sK45))
& ~ v3_struct_0(sK45)
& v10_lattices(sK45)
& l3_lattices(sK45) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK45,sK46]),skolemize(X0,sK45),skolemize(X1,sK46)],[f34867]) ).
fof(f36585,plain,
! [X0,X1,X2] :
( ( ( r1_filter_2(X0,X1,X2)
| X1 != X2 )
& ( X1 = X2
| ~ r1_filter_2(X0,X1,X2) ) )
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(nnf_transformation,[],[f34908]) ).
fof(f36589,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( ( r2_hidden(X3,k22_filter_2(X0,X1,X2))
| ~ r3_lattices(X0,X1,X3)
| ~ r3_lattices(X0,X3,X2) )
& ( ( r3_lattices(X0,X1,X3)
& r3_lattices(X0,X3,X2) )
| ~ r2_hidden(X3,k22_filter_2(X0,X1,X2)) ) )
| ~ r3_lattices(X0,X1,X2)
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f34940]) ).
fof(f36590,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( ( r2_hidden(X3,k22_filter_2(X0,X1,X2))
| ~ r3_lattices(X0,X1,X3)
| ~ r3_lattices(X0,X3,X2) )
& ( ( r3_lattices(X0,X1,X3)
& r3_lattices(X0,X3,X2) )
| ~ r2_hidden(X3,k22_filter_2(X0,X1,X2)) ) )
| ~ r3_lattices(X0,X1,X2)
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f36589]) ).
fof(f36809,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( r2_hidden(X1,k2_filter_0(X0,X2))
| ~ r3_lattices(X0,X2,X1) )
& ( r3_lattices(X0,X2,X1)
| ~ r2_hidden(X1,k2_filter_0(X0,X2)) ) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f35469]) ).
fof(f36811,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,[],[f35475]) ).
fof(f37000,plain,
! [X0,X1] :
( ( X0 = X1
| ~ r1_tarski(X0,X1)
| ~ r1_tarski(X1,X0) )
& ( ( r1_tarski(X0,X1)
& r1_tarski(X1,X0) )
| X0 != X1 ) ),
inference(nnf_transformation,[],[f38]) ).
fof(f37001,plain,
! [X0,X1] :
( ( X0 = X1
| ~ r1_tarski(X0,X1)
| ~ r1_tarski(X1,X0) )
& ( ( r1_tarski(X0,X1)
& r1_tarski(X1,X0) )
| X0 != X1 ) ),
inference(flattening,[],[f37000]) ).
fof(f37002,plain,
! [X0,X1] :
( ( r1_tarski(X0,X1)
| ? [X2] :
( ~ r2_hidden(X2,X1)
& r2_hidden(X2,X0) ) )
& ( ! [X2] :
( r2_hidden(X2,X1)
| ~ r2_hidden(X2,X0) )
| ~ r1_tarski(X0,X1) ) ),
inference(nnf_transformation,[],[f35910]) ).
fof(f37003,plain,
! [X0,X1] :
( ( r1_tarski(X0,X1)
| ? [X2] :
( ~ r2_hidden(X2,X1)
& r2_hidden(X2,X0) ) )
& ( ! [X3] :
( r2_hidden(X3,X1)
| ~ r2_hidden(X3,X0) )
| ~ r1_tarski(X0,X1) ) ),
inference(rectify,[],[f37002]) ).
fof(f37004,plain,
! [X0,X1] :
( ( r1_tarski(X0,X1)
| ( ~ r2_hidden(sK346(X0,X1),X1)
& r2_hidden(sK346(X0,X1),X0) ) )
& ( ! [X3] :
( r2_hidden(X3,X1)
| ~ r2_hidden(X3,X0) )
| ~ r1_tarski(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK346]),skolemize(X2,sK346(X0,X1))],[f37003]) ).
fof(f37259,plain,
l3_lattices(sK45),
inference(cnf_transformation,[],[f36574]) ).
fof(f37260,plain,
v10_lattices(sK45),
inference(cnf_transformation,[],[f36574]) ).
fof(f37261,plain,
~ v3_struct_0(sK45),
inference(cnf_transformation,[],[f36574]) ).
fof(f37262,plain,
m1_subset_1(sK46,u1_struct_0(sK45)),
inference(cnf_transformation,[],[f36574]) ).
fof(f37263,plain,
v14_lattices(sK45),
inference(cnf_transformation,[],[f36574]) ).
fof(f37264,plain,
~ r1_filter_2(u1_struct_0(sK45),k2_filter_2(sK45,sK46),k22_filter_2(sK45,sK46,k6_lattices(sK45))),
inference(cnf_transformation,[],[f36574]) ).
fof(f37304,plain,
! [X0,X1] :
( r2_hidden(k6_lattices(X0),X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v14_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_filter_0(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f34895]) ).
fof(f37305,plain,
! [X0,X1] :
( r3_lattices(X0,X1,k6_lattices(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v14_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f34897]) ).
fof(f37317,plain,
! [X2,X0,X1] :
( X1 != X2
| r1_filter_2(X0,X1,X2)
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f36585]) ).
fof(f37334,plain,
! [X0,X1] :
( k2_filter_0(X0,X1) = k2_filter_2(X0,X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f34932]) ).
fof(f37335,plain,
! [X0,X1] :
( m1_filter_2(k2_filter_2(X0,X1),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f34934]) ).
fof(f37340,plain,
! [X2,X3,X0,X1] :
( ~ r2_hidden(X3,k22_filter_2(X0,X1,X2))
| r3_lattices(X0,X1,X3)
| ~ r3_lattices(X0,X1,X2)
| ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f36590]) ).
fof(f37341,plain,
! [X2,X3,X0,X1] :
( r2_hidden(X3,k22_filter_2(X0,X1,X2))
| ~ r3_lattices(X0,X1,X3)
| ~ r3_lattices(X0,X3,X2)
| ~ r3_lattices(X0,X1,X2)
| ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f36590]) ).
fof(f37342,plain,
! [X2,X0,X1] :
( m2_lattice4(k22_filter_2(X0,X1,X2),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f34942]) ).
fof(f37615,plain,
! [X0] :
( m1_filter_0(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35139]) ).
fof(f37651,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ r2_hidden(X0,X1)
| m1_subset_1(X0,X2) ),
inference(cnf_transformation,[],[f35155]) ).
fof(f38105,plain,
! [X0,X1] :
( m1_filter_0(k2_filter_0(X0,X1),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f35447]) ).
fof(f38125,plain,
! [X2,X0,X1] :
( ~ r2_hidden(X1,k2_filter_0(X0,X2))
| r3_lattices(X0,X2,X1)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f36809]) ).
fof(f38126,plain,
! [X2,X0,X1] :
( r2_hidden(X1,k2_filter_0(X0,X2))
| ~ r3_lattices(X0,X2,X1)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f36809]) ).
fof(f38131,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,[],[f36811]) ).
fof(f38133,plain,
! [X0,X1] :
( m2_lattice4(X1,X0)
| ~ m1_filter_2(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35479]) ).
fof(f38134,plain,
! [X0,X1] :
( ~ v10_lattices(X0)
| ~ m1_filter_2(X1,X0)
| v3_struct_0(X0)
| ~ v1_xboole_0(X1)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35479]) ).
fof(f38152,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,[],[f35489]) ).
fof(f38815,plain,
! [X0,X1] :
( ~ r1_tarski(X0,X1)
| X0 = X1
| ~ r1_tarski(X1,X0) ),
inference(cnf_transformation,[],[f37001]) ).
fof(f38818,plain,
! [X0,X1] :
( r1_tarski(X0,X1)
| r2_hidden(sK346(X0,X1),X0) ),
inference(cnf_transformation,[],[f37004]) ).
fof(f38819,plain,
! [X0,X1] :
( ~ r2_hidden(sK346(X0,X1),X1)
| r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f37004]) ).
fof(f40307,definition,
sF503 = u1_struct_0(sK45),
introduced(definition,[new_symbols(definition,[sF503])],[function_definition]) ).
fof(f40308,plain,
u1_struct_0(sK45) = sF503,
inference(reorient_equations,[],[f40307]) ).
fof(f40309,definition,
sF504 = k2_filter_2(sK45,sK46),
introduced(definition,[new_symbols(definition,[sF504])],[function_definition]) ).
fof(f40310,plain,
k2_filter_2(sK45,sK46) = sF504,
inference(reorient_equations,[],[f40309]) ).
fof(f40311,definition,
sF505 = k6_lattices(sK45),
introduced(definition,[new_symbols(definition,[sF505])],[function_definition]) ).
fof(f40312,plain,
k6_lattices(sK45) = sF505,
inference(reorient_equations,[],[f40311]) ).
fof(f40313,definition,
sF506 = k22_filter_2(sK45,sK46,sF505),
introduced(definition,[new_symbols(definition,[sF506])],[function_definition]) ).
fof(f40314,plain,
k22_filter_2(sK45,sK46,sF505) = sF506,
inference(reorient_equations,[],[f40313]) ).
fof(f40315,plain,
~ r1_filter_2(sF503,sF504,sF506),
inference(definition_folding,[],[f37264,f40314,f40312,f40310,f40308]) ).
fof(f40316,plain,
m1_subset_1(sK46,sF503),
inference(definition_folding,[],[f37262,f40308]) ).
fof(f40362,plain,
! [X0,X1] :
( r2_hidden(k6_lattices(X0),X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v14_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_filter_0(X1,X0) ),
inference(duplicate_literal_removal,[],[f37304]) ).
fof(f40371,plain,
( sF504 = k2_filter_0(sK45,sK46)
| v3_struct_0(sK45)
| ~ v10_lattices(sK45)
| ~ l3_lattices(sK45)
| ~ m1_subset_1(sK46,u1_struct_0(sK45)) ),
inference(superposition,[],[f37334,f40310]) ).
fof(f40374,plain,
( ~ m1_subset_1(sK46,sF503)
| sF504 = k2_filter_0(sK45,sK46)
| v3_struct_0(sK45)
| ~ v10_lattices(sK45)
| ~ l3_lattices(sK45) ),
inference(forward_demodulation,[],[f40371,f40308]) ).
fof(f40376,definition,
( spl507_3
<=> l3_lattices(sK45) ),
introduced(definition,[new_symbols(definition,[spl507_3])],[avatar_definition]) ).
fof(f40380,definition,
( spl507_4
<=> v10_lattices(sK45) ),
introduced(definition,[new_symbols(definition,[spl507_4])],[avatar_definition]) ).
fof(f40381,plain,
( v10_lattices(sK45)
| ~ spl507_4 ),
inference(avatar_component_clause,[],[f40380]) ).
fof(f40384,definition,
( spl507_5
<=> v3_struct_0(sK45) ),
introduced(definition,[new_symbols(definition,[spl507_5])],[avatar_definition]) ).
fof(f40388,definition,
( spl507_6
<=> sF504 = k2_filter_0(sK45,sK46) ),
introduced(definition,[new_symbols(definition,[spl507_6])],[avatar_definition]) ).
fof(f40390,plain,
( sF504 = k2_filter_0(sK45,sK46)
| ~ spl507_6 ),
inference(avatar_component_clause,[],[f40388]) ).
fof(f40392,definition,
( spl507_7
<=> m1_subset_1(sK46,sF503) ),
introduced(definition,[new_symbols(definition,[spl507_7])],[avatar_definition]) ).
fof(f40396,plain,
( ~ spl507_3
| ~ spl507_4
| spl507_5
| spl507_6
| ~ spl507_7 ),
inference(avatar_split_clause,[],[f40374,f40392,f40388,f40384,f40380,f40376]) ).
fof(f40400,definition,
( spl507_8
<=> v14_lattices(sK45) ),
introduced(definition,[new_symbols(definition,[spl507_8])],[avatar_definition]) ).
fof(f40409,plain,
spl507_3,
inference(avatar_split_clause,[],[f37259,f40376]) ).
fof(f40411,plain,
! [X0] :
( r2_hidden(sF505,X0)
| v3_struct_0(sK45)
| ~ v10_lattices(sK45)
| ~ v14_lattices(sK45)
| ~ l3_lattices(sK45)
| ~ m1_filter_0(X0,sK45) ),
inference(superposition,[],[f40362,f40312]) ).
fof(f40414,definition,
( spl507_10
<=> ! [X0] :
( r2_hidden(sF505,X0)
| ~ m1_filter_0(X0,sK45) ) ),
introduced(definition,[new_symbols(definition,[spl507_10])],[avatar_definition]) ).
fof(f40415,plain,
( ! [X0] :
( r2_hidden(sF505,X0)
| ~ m1_filter_0(X0,sK45) )
| ~ spl507_10 ),
inference(avatar_component_clause,[],[f40414]) ).
fof(f40416,plain,
( ~ spl507_3
| ~ spl507_8
| ~ spl507_4
| spl507_5
| spl507_10 ),
inference(avatar_split_clause,[],[f40411,f40414,f40384,f40380,f40400,f40376]) ).
fof(f40417,plain,
( m1_filter_2(sF504,sK45)
| v3_struct_0(sK45)
| ~ v10_lattices(sK45)
| ~ l3_lattices(sK45)
| ~ m1_subset_1(sK46,u1_struct_0(sK45)) ),
inference(superposition,[],[f37335,f40310]) ).
fof(f40420,plain,
( ~ m1_subset_1(sK46,sF503)
| m1_filter_2(sF504,sK45)
| v3_struct_0(sK45)
| ~ v10_lattices(sK45)
| ~ l3_lattices(sK45) ),
inference(forward_demodulation,[],[f40417,f40308]) ).
fof(f40422,definition,
( spl507_11
<=> m1_filter_2(sF504,sK45) ),
introduced(definition,[new_symbols(definition,[spl507_11])],[avatar_definition]) ).
fof(f40425,plain,
( ~ spl507_3
| ~ spl507_4
| spl507_5
| spl507_11
| ~ spl507_7 ),
inference(avatar_split_clause,[],[f40420,f40392,f40422,f40384,f40380,f40376]) ).
fof(f40428,plain,
spl507_4,
inference(avatar_split_clause,[],[f37260,f40380]) ).
fof(f40431,plain,
spl507_7,
inference(avatar_split_clause,[],[f40316,f40392]) ).
fof(f40434,plain,
~ spl507_5,
inference(avatar_split_clause,[],[f37261,f40384]) ).
fof(f40437,plain,
spl507_8,
inference(avatar_split_clause,[],[f37263,f40400]) ).
fof(f40459,definition,
( spl507_14
<=> m1_subset_1(sF504,k1_zfmisc_1(sF503)) ),
introduced(definition,[new_symbols(definition,[spl507_14])],[avatar_definition]) ).
fof(f40460,plain,
( m1_subset_1(sF504,k1_zfmisc_1(sF503))
| ~ spl507_14 ),
inference(avatar_component_clause,[],[f40459]) ).
fof(f40461,plain,
( ~ m1_subset_1(sF504,k1_zfmisc_1(sF503))
| spl507_14 ),
inference(avatar_component_clause,[],[f40459]) ).
fof(f40463,definition,
( spl507_15
<=> m1_subset_1(sF506,k1_zfmisc_1(sF503)) ),
introduced(definition,[new_symbols(definition,[spl507_15])],[avatar_definition]) ).
fof(f40464,plain,
( m1_subset_1(sF506,k1_zfmisc_1(sF503))
| ~ spl507_15 ),
inference(avatar_component_clause,[],[f40463]) ).
fof(f40465,plain,
( ~ m1_subset_1(sF506,k1_zfmisc_1(sF503))
| spl507_15 ),
inference(avatar_component_clause,[],[f40463]) ).
fof(f40467,definition,
( spl507_16
<=> v1_xboole_0(sF503) ),
introduced(definition,[new_symbols(definition,[spl507_16])],[avatar_definition]) ).
fof(f40469,plain,
( v1_xboole_0(sF503)
| ~ spl507_16 ),
inference(avatar_component_clause,[],[f40467]) ).
fof(f40486,definition,
( spl507_19
<=> r3_lattices(sK45,sK46,sF505) ),
introduced(definition,[new_symbols(definition,[spl507_19])],[avatar_definition]) ).
fof(f40488,plain,
( ~ r3_lattices(sK45,sK46,sF505)
| spl507_19 ),
inference(avatar_component_clause,[],[f40486]) ).
fof(f40494,definition,
( spl507_21
<=> m1_subset_1(sF505,sF503) ),
introduced(definition,[new_symbols(definition,[spl507_21])],[avatar_definition]) ).
fof(f40496,plain,
( ~ m1_subset_1(sF505,sF503)
| spl507_21 ),
inference(avatar_component_clause,[],[f40494]) ).
fof(f40498,plain,
( m2_lattice4(sF506,sK45)
| v3_struct_0(sK45)
| ~ v10_lattices(sK45)
| ~ l3_lattices(sK45)
| ~ m1_subset_1(sK46,u1_struct_0(sK45))
| ~ m1_subset_1(sF505,u1_struct_0(sK45)) ),
inference(superposition,[],[f37342,f40314]) ).
fof(f40499,plain,
( ~ m1_subset_1(sK46,sF503)
| m2_lattice4(sF506,sK45)
| v3_struct_0(sK45)
| ~ v10_lattices(sK45)
| ~ l3_lattices(sK45)
| ~ m1_subset_1(sF505,u1_struct_0(sK45)) ),
inference(forward_demodulation,[],[f40498,f40308]) ).
fof(f40500,plain,
( ~ m1_subset_1(sF505,sF503)
| ~ m1_subset_1(sK46,sF503)
| m2_lattice4(sF506,sK45)
| v3_struct_0(sK45)
| ~ v10_lattices(sK45)
| ~ l3_lattices(sK45) ),
inference(forward_demodulation,[],[f40499,f40308]) ).
fof(f40502,definition,
( spl507_22
<=> m2_lattice4(sF506,sK45) ),
introduced(definition,[new_symbols(definition,[spl507_22])],[avatar_definition]) ).
fof(f40505,plain,
( ~ spl507_3
| ~ spl507_4
| spl507_5
| spl507_22
| ~ spl507_7
| ~ spl507_21 ),
inference(avatar_split_clause,[],[f40500,f40494,f40392,f40502,f40384,f40380,f40376]) ).
fof(f40518,plain,
! [X0] :
( r2_hidden(X0,sF506)
| ~ r3_lattices(sK45,sK46,X0)
| ~ r3_lattices(sK45,X0,sF505)
| ~ r3_lattices(sK45,sK46,sF505)
| ~ m1_subset_1(X0,u1_struct_0(sK45))
| ~ m1_subset_1(sF505,u1_struct_0(sK45))
| ~ m1_subset_1(sK46,u1_struct_0(sK45))
| v3_struct_0(sK45)
| ~ v10_lattices(sK45)
| ~ l3_lattices(sK45) ),
inference(superposition,[],[f37341,f40314]) ).
fof(f40533,plain,
( m1_filter_0(sF503,sK45)
| v3_struct_0(sK45)
| ~ v10_lattices(sK45)
| ~ l3_lattices(sK45) ),
inference(superposition,[],[f37615,f40308]) ).
fof(f40536,definition,
( spl507_26
<=> m1_filter_0(sF503,sK45) ),
introduced(definition,[new_symbols(definition,[spl507_26])],[avatar_definition]) ).
fof(f40539,plain,
( ~ spl507_3
| ~ spl507_4
| spl507_5
| spl507_26 ),
inference(avatar_split_clause,[],[f40533,f40536,f40384,f40380,f40376]) ).
fof(f40567,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF504)
| r3_lattices(sK45,sK46,X0)
| ~ m1_subset_1(sK46,u1_struct_0(sK45))
| ~ m1_subset_1(X0,u1_struct_0(sK45))
| v3_struct_0(sK45)
| ~ v10_lattices(sK45)
| ~ l3_lattices(sK45) )
| ~ spl507_6 ),
inference(superposition,[],[f38125,f40390]) ).
fof(f40569,plain,
( ! [X0] :
( ~ m1_subset_1(sK46,sF503)
| ~ r2_hidden(X0,sF504)
| r3_lattices(sK45,sK46,X0)
| ~ m1_subset_1(X0,u1_struct_0(sK45))
| v3_struct_0(sK45)
| ~ v10_lattices(sK45)
| ~ l3_lattices(sK45) )
| ~ spl507_6 ),
inference(forward_demodulation,[],[f40567,f40308]) ).
fof(f40570,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF503)
| ~ m1_subset_1(sK46,sF503)
| ~ r2_hidden(X0,sF504)
| r3_lattices(sK45,sK46,X0)
| v3_struct_0(sK45)
| ~ v10_lattices(sK45)
| ~ l3_lattices(sK45) )
| ~ spl507_6 ),
inference(forward_demodulation,[],[f40569,f40308]) ).
fof(f40572,definition,
( spl507_30
<=> ! [X0] :
( ~ m1_subset_1(X0,sF503)
| r3_lattices(sK45,sK46,X0)
| ~ r2_hidden(X0,sF504) ) ),
introduced(definition,[new_symbols(definition,[spl507_30])],[avatar_definition]) ).
fof(f40573,plain,
( ! [X0] :
( r3_lattices(sK45,sK46,X0)
| ~ m1_subset_1(X0,sF503)
| ~ r2_hidden(X0,sF504) )
| ~ spl507_30 ),
inference(avatar_component_clause,[],[f40572]) ).
fof(f40574,plain,
( ~ spl507_3
| ~ spl507_4
| spl507_5
| ~ spl507_7
| spl507_30
| ~ spl507_6 ),
inference(avatar_split_clause,[],[f40570,f40388,f40572,f40392,f40384,f40380,f40376]) ).
fof(f40575,plain,
( ~ m1_subset_1(sF505,sF503)
| ~ r2_hidden(sF505,sF504)
| spl507_19
| ~ spl507_30 ),
inference(resolution,[],[f40573,f40488]) ).
fof(f40610,plain,
! [X0] :
( m1_subset_1(X0,k1_zfmisc_1(sF503))
| ~ m2_lattice4(X0,sK45)
| v3_struct_0(sK45)
| ~ v10_lattices(sK45)
| ~ l3_lattices(sK45) ),
inference(superposition,[],[f38152,f40308]) ).
fof(f40613,definition,
( spl507_34
<=> ! [X0] :
( m1_subset_1(X0,k1_zfmisc_1(sF503))
| ~ m2_lattice4(X0,sK45) ) ),
introduced(definition,[new_symbols(definition,[spl507_34])],[avatar_definition]) ).
fof(f40614,plain,
( ! [X0] :
( m1_subset_1(X0,k1_zfmisc_1(sF503))
| ~ m2_lattice4(X0,sK45) )
| ~ spl507_34 ),
inference(avatar_component_clause,[],[f40613]) ).
fof(f40615,plain,
( ~ spl507_3
| ~ spl507_4
| spl507_5
| spl507_34 ),
inference(avatar_split_clause,[],[f40610,f40613,f40384,f40380,f40376]) ).
fof(f40616,plain,
( ~ m2_lattice4(sF504,sK45)
| spl507_14
| ~ spl507_34 ),
inference(resolution,[],[f40614,f40461]) ).
fof(f40631,plain,
! [X0,X1] :
( r1_filter_2(X0,X1,X1)
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(X0)) ),
inference(equality_resolution,[],[f37317]) ).
fof(f40632,plain,
! [X0,X1] :
( r1_filter_2(X0,X1,X1)
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0)) ),
inference(duplicate_literal_removal,[],[f40631]) ).
fof(f40635,plain,
( ~ m1_filter_2(sF504,sK45)
| v3_struct_0(sK45)
| ~ v10_lattices(sK45)
| ~ l3_lattices(sK45)
| spl507_14
| ~ spl507_34 ),
inference(resolution,[],[f38133,f40616]) ).
fof(f40636,plain,
( ~ spl507_3
| ~ spl507_4
| spl507_5
| ~ spl507_11
| spl507_14
| ~ spl507_34 ),
inference(avatar_split_clause,[],[f40635,f40613,f40459,f40422,f40384,f40380,f40376]) ).
fof(f40640,plain,
( m1_filter_0(sF504,sK45)
| v3_struct_0(sK45)
| ~ v10_lattices(sK45)
| ~ l3_lattices(sK45)
| ~ m1_subset_1(sK46,u1_struct_0(sK45))
| ~ spl507_6 ),
inference(superposition,[],[f38105,f40390]) ).
fof(f40641,plain,
( ~ m1_subset_1(sK46,sF503)
| m1_filter_0(sF504,sK45)
| v3_struct_0(sK45)
| ~ v10_lattices(sK45)
| ~ l3_lattices(sK45)
| ~ spl507_6 ),
inference(forward_demodulation,[],[f40640,f40308]) ).
fof(f40643,definition,
( spl507_36
<=> m1_filter_0(sF504,sK45) ),
introduced(definition,[new_symbols(definition,[spl507_36])],[avatar_definition]) ).
fof(f40646,plain,
( ~ spl507_3
| ~ spl507_4
| spl507_5
| spl507_36
| ~ spl507_7
| ~ spl507_6 ),
inference(avatar_split_clause,[],[f40641,f40388,f40392,f40643,f40384,f40380,f40376]) ).
fof(f40669,plain,
( ! [X0] :
( r2_hidden(X0,sF504)
| ~ r3_lattices(sK45,sK46,X0)
| ~ m1_subset_1(sK46,u1_struct_0(sK45))
| ~ m1_subset_1(X0,u1_struct_0(sK45))
| v3_struct_0(sK45)
| ~ v10_lattices(sK45)
| ~ l3_lattices(sK45) )
| ~ spl507_6 ),
inference(superposition,[],[f38126,f40390]) ).
fof(f40671,plain,
( ! [X0] :
( ~ m1_subset_1(sK46,sF503)
| r2_hidden(X0,sF504)
| ~ r3_lattices(sK45,sK46,X0)
| ~ m1_subset_1(X0,u1_struct_0(sK45))
| v3_struct_0(sK45)
| ~ v10_lattices(sK45)
| ~ l3_lattices(sK45) )
| ~ spl507_6 ),
inference(forward_demodulation,[],[f40669,f40308]) ).
fof(f40672,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF503)
| ~ m1_subset_1(sK46,sF503)
| r2_hidden(X0,sF504)
| ~ r3_lattices(sK45,sK46,X0)
| v3_struct_0(sK45)
| ~ v10_lattices(sK45)
| ~ l3_lattices(sK45) )
| ~ spl507_6 ),
inference(forward_demodulation,[],[f40671,f40308]) ).
fof(f40674,definition,
( spl507_38
<=> ! [X0] :
( ~ m1_subset_1(X0,sF503)
| ~ r3_lattices(sK45,sK46,X0)
| r2_hidden(X0,sF504) ) ),
introduced(definition,[new_symbols(definition,[spl507_38])],[avatar_definition]) ).
fof(f40675,plain,
( ! [X0] :
( ~ r3_lattices(sK45,sK46,X0)
| ~ m1_subset_1(X0,sF503)
| r2_hidden(X0,sF504) )
| ~ spl507_38 ),
inference(avatar_component_clause,[],[f40674]) ).
fof(f40676,plain,
( ~ spl507_3
| ~ spl507_4
| spl507_5
| ~ spl507_7
| spl507_38
| ~ spl507_6 ),
inference(avatar_split_clause,[],[f40672,f40388,f40674,f40392,f40384,f40380,f40376]) ).
fof(f40718,plain,
( ~ m1_subset_1(sK46,u1_struct_0(sK45))
| v3_struct_0(sK45)
| ~ v10_lattices(sK45)
| ~ v14_lattices(sK45)
| ~ l3_lattices(sK45)
| ~ m1_subset_1(k6_lattices(sK45),sF503)
| r2_hidden(k6_lattices(sK45),sF504)
| ~ spl507_38 ),
inference(resolution,[],[f37305,f40675]) ).
fof(f40719,plain,
! [X0] :
( r3_lattices(sK45,X0,sF505)
| ~ m1_subset_1(X0,u1_struct_0(sK45))
| v3_struct_0(sK45)
| ~ v10_lattices(sK45)
| ~ v14_lattices(sK45)
| ~ l3_lattices(sK45) ),
inference(superposition,[],[f37305,f40312]) ).
fof(f40720,plain,
! [X0] :
( ~ m1_subset_1(X0,sF503)
| r3_lattices(sK45,X0,sF505)
| v3_struct_0(sK45)
| ~ v10_lattices(sK45)
| ~ v14_lattices(sK45)
| ~ l3_lattices(sK45) ),
inference(forward_demodulation,[],[f40719,f40308]) ).
fof(f40721,plain,
( ~ m1_subset_1(sK46,sF503)
| v3_struct_0(sK45)
| ~ v10_lattices(sK45)
| ~ v14_lattices(sK45)
| ~ l3_lattices(sK45)
| ~ m1_subset_1(k6_lattices(sK45),sF503)
| r2_hidden(k6_lattices(sK45),sF504)
| ~ spl507_38 ),
inference(forward_demodulation,[],[f40718,f40308]) ).
fof(f40723,definition,
( spl507_42
<=> ! [X0] :
( ~ m1_subset_1(X0,sF503)
| r3_lattices(sK45,X0,sF505) ) ),
introduced(definition,[new_symbols(definition,[spl507_42])],[avatar_definition]) ).
fof(f40724,plain,
( ! [X0] :
( r3_lattices(sK45,X0,sF505)
| ~ m1_subset_1(X0,sF503) )
| ~ spl507_42 ),
inference(avatar_component_clause,[],[f40723]) ).
fof(f40725,plain,
( ~ spl507_3
| ~ spl507_8
| ~ spl507_4
| spl507_5
| spl507_42 ),
inference(avatar_split_clause,[],[f40720,f40723,f40384,f40380,f40400,f40376]) ).
fof(f40726,plain,
( ~ m1_subset_1(sF505,sF503)
| ~ m1_subset_1(sK46,sF503)
| v3_struct_0(sK45)
| ~ v10_lattices(sK45)
| ~ v14_lattices(sK45)
| ~ l3_lattices(sK45)
| r2_hidden(k6_lattices(sK45),sF504)
| ~ spl507_38 ),
inference(forward_demodulation,[],[f40721,f40312]) ).
fof(f40746,plain,
( ! [X0] :
( m1_subset_1(X0,sF503)
| ~ r2_hidden(X0,sF504) )
| ~ spl507_14 ),
inference(resolution,[],[f37651,f40460]) ).
fof(f40747,plain,
( ~ r2_hidden(sF505,sF504)
| ~ spl507_14
| spl507_21 ),
inference(resolution,[],[f40746,f40496]) ).
fof(f40751,plain,
( ~ m1_filter_0(sF504,sK45)
| ~ spl507_10
| ~ spl507_14
| spl507_21 ),
inference(resolution,[],[f40747,f40415]) ).
fof(f40752,plain,
( ~ spl507_36
| ~ spl507_10
| ~ spl507_14
| spl507_21 ),
inference(avatar_split_clause,[],[f40751,f40494,f40459,f40414,f40643]) ).
fof(f40754,definition,
( spl507_43
<=> r2_hidden(sF505,sF504) ),
introduced(definition,[new_symbols(definition,[spl507_43])],[avatar_definition]) ).
fof(f40757,plain,
( ~ spl507_43
| ~ spl507_21
| spl507_19
| ~ spl507_30 ),
inference(avatar_split_clause,[],[f40575,f40572,f40486,f40494,f40754]) ).
fof(f40764,plain,
( r2_hidden(sF505,sF504)
| ~ m1_subset_1(sF505,sF503)
| ~ m1_subset_1(sK46,sF503)
| v3_struct_0(sK45)
| ~ v10_lattices(sK45)
| ~ v14_lattices(sK45)
| ~ l3_lattices(sK45)
| ~ spl507_38 ),
inference(forward_demodulation,[],[f40726,f40312]) ).
fof(f40770,plain,
( ~ spl507_3
| ~ spl507_8
| ~ spl507_4
| spl507_5
| ~ spl507_7
| ~ spl507_21
| spl507_43
| ~ spl507_38 ),
inference(avatar_split_clause,[],[f40764,f40674,f40754,f40494,f40392,f40384,f40380,f40400,f40376]) ).
fof(f40771,plain,
! [X0] :
( ~ m1_subset_1(X0,sF503)
| r2_hidden(X0,sF506)
| ~ r3_lattices(sK45,sK46,X0)
| ~ r3_lattices(sK45,X0,sF505)
| ~ r3_lattices(sK45,sK46,sF505)
| ~ m1_subset_1(sF505,u1_struct_0(sK45))
| ~ m1_subset_1(sK46,u1_struct_0(sK45))
| v3_struct_0(sK45)
| ~ v10_lattices(sK45)
| ~ l3_lattices(sK45) ),
inference(forward_demodulation,[],[f40518,f40308]) ).
fof(f40774,plain,
! [X0] :
( ~ m1_subset_1(sF505,sF503)
| ~ m1_subset_1(X0,sF503)
| r2_hidden(X0,sF506)
| ~ r3_lattices(sK45,sK46,X0)
| ~ r3_lattices(sK45,X0,sF505)
| ~ r3_lattices(sK45,sK46,sF505)
| ~ m1_subset_1(sK46,u1_struct_0(sK45))
| v3_struct_0(sK45)
| ~ v10_lattices(sK45)
| ~ l3_lattices(sK45) ),
inference(forward_demodulation,[],[f40771,f40308]) ).
fof(f40781,plain,
! [X0] :
( ~ m1_subset_1(sK46,sF503)
| ~ m1_subset_1(sF505,sF503)
| ~ m1_subset_1(X0,sF503)
| r2_hidden(X0,sF506)
| ~ r3_lattices(sK45,sK46,X0)
| ~ r3_lattices(sK45,X0,sF505)
| ~ r3_lattices(sK45,sK46,sF505)
| v3_struct_0(sK45)
| ~ v10_lattices(sK45)
| ~ l3_lattices(sK45) ),
inference(forward_demodulation,[],[f40774,f40308]) ).
fof(f40784,definition,
( spl507_47
<=> ! [X0] :
( ~ m1_subset_1(X0,sF503)
| ~ r3_lattices(sK45,X0,sF505)
| ~ r3_lattices(sK45,sK46,X0)
| r2_hidden(X0,sF506) ) ),
introduced(definition,[new_symbols(definition,[spl507_47])],[avatar_definition]) ).
fof(f40785,plain,
( ! [X0] :
( ~ r3_lattices(sK45,sK46,X0)
| ~ r3_lattices(sK45,X0,sF505)
| ~ m1_subset_1(X0,sF503)
| r2_hidden(X0,sF506) )
| ~ spl507_47 ),
inference(avatar_component_clause,[],[f40784]) ).
fof(f40786,plain,
( ~ spl507_3
| ~ spl507_4
| spl507_5
| ~ spl507_19
| spl507_47
| ~ spl507_21
| ~ spl507_7 ),
inference(avatar_split_clause,[],[f40781,f40392,f40494,f40784,f40486,f40384,f40380,f40376]) ).
fof(f40791,plain,
( ! [X0] :
( ~ r3_lattices(sK45,X0,sF505)
| ~ m1_subset_1(X0,sF503)
| r2_hidden(X0,sF506)
| ~ m1_subset_1(X0,sF503)
| ~ r2_hidden(X0,sF504) )
| ~ spl507_30
| ~ spl507_47 ),
inference(resolution,[],[f40785,f40573]) ).
fof(f40796,plain,
( ! [X0] :
( ~ r3_lattices(sK45,X0,sF505)
| ~ m1_subset_1(X0,sF503)
| r2_hidden(X0,sF506)
| ~ r2_hidden(X0,sF504) )
| ~ spl507_30
| ~ spl507_47 ),
inference(duplicate_literal_removal,[],[f40791]) ).
fof(f40886,plain,
! [X0] :
( ~ r2_hidden(X0,sF506)
| r3_lattices(sK45,sK46,X0)
| ~ r3_lattices(sK45,sK46,sF505)
| ~ m1_subset_1(X0,u1_struct_0(sK45))
| ~ m1_subset_1(sF505,u1_struct_0(sK45))
| ~ m1_subset_1(sK46,u1_struct_0(sK45))
| v3_struct_0(sK45)
| ~ v10_lattices(sK45)
| ~ l3_lattices(sK45) ),
inference(superposition,[],[f37340,f40314]) ).
fof(f40890,plain,
! [X0] :
( ~ m1_subset_1(X0,sF503)
| ~ r2_hidden(X0,sF506)
| r3_lattices(sK45,sK46,X0)
| ~ r3_lattices(sK45,sK46,sF505)
| ~ m1_subset_1(sF505,u1_struct_0(sK45))
| ~ m1_subset_1(sK46,u1_struct_0(sK45))
| v3_struct_0(sK45)
| ~ v10_lattices(sK45)
| ~ l3_lattices(sK45) ),
inference(forward_demodulation,[],[f40886,f40308]) ).
fof(f40891,plain,
! [X0] :
( ~ m1_subset_1(sF505,sF503)
| ~ m1_subset_1(X0,sF503)
| ~ r2_hidden(X0,sF506)
| r3_lattices(sK45,sK46,X0)
| ~ r3_lattices(sK45,sK46,sF505)
| ~ m1_subset_1(sK46,u1_struct_0(sK45))
| v3_struct_0(sK45)
| ~ v10_lattices(sK45)
| ~ l3_lattices(sK45) ),
inference(forward_demodulation,[],[f40890,f40308]) ).
fof(f40892,plain,
! [X0] :
( ~ m1_subset_1(sK46,sF503)
| ~ m1_subset_1(sF505,sF503)
| ~ m1_subset_1(X0,sF503)
| ~ r2_hidden(X0,sF506)
| r3_lattices(sK45,sK46,X0)
| ~ r3_lattices(sK45,sK46,sF505)
| v3_struct_0(sK45)
| ~ v10_lattices(sK45)
| ~ l3_lattices(sK45) ),
inference(forward_demodulation,[],[f40891,f40308]) ).
fof(f40894,definition,
( spl507_56
<=> ! [X0] :
( ~ m1_subset_1(X0,sF503)
| r3_lattices(sK45,sK46,X0)
| ~ r2_hidden(X0,sF506) ) ),
introduced(definition,[new_symbols(definition,[spl507_56])],[avatar_definition]) ).
fof(f40895,plain,
( ! [X0] :
( r3_lattices(sK45,sK46,X0)
| ~ m1_subset_1(X0,sF503)
| ~ r2_hidden(X0,sF506) )
| ~ spl507_56 ),
inference(avatar_component_clause,[],[f40894]) ).
fof(f40896,plain,
( ~ spl507_3
| ~ spl507_4
| spl507_5
| ~ spl507_19
| spl507_56
| ~ spl507_21
| ~ spl507_7 ),
inference(avatar_split_clause,[],[f40892,f40392,f40494,f40894,f40486,f40384,f40380,f40376]) ).
fof(f40898,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF503)
| ~ r2_hidden(X0,sF506)
| ~ m1_subset_1(X0,sF503)
| r2_hidden(X0,sF504) )
| ~ spl507_38
| ~ spl507_56 ),
inference(resolution,[],[f40895,f40675]) ).
fof(f40900,plain,
( ! [X0] :
( r2_hidden(X0,sF504)
| ~ r2_hidden(X0,sF506)
| ~ m1_subset_1(X0,sF503) )
| ~ spl507_38
| ~ spl507_56 ),
inference(duplicate_literal_removal,[],[f40898]) ).
fof(f40922,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF503)
| ~ m1_subset_1(X0,sF503)
| r2_hidden(X0,sF506)
| ~ r2_hidden(X0,sF504) )
| ~ spl507_30
| ~ spl507_42
| ~ spl507_47 ),
inference(resolution,[],[f40724,f40796]) ).
fof(f40923,plain,
( ! [X0] :
( r2_hidden(X0,sF506)
| ~ m1_subset_1(X0,sF503)
| ~ r2_hidden(X0,sF504) )
| ~ spl507_30
| ~ spl507_42
| ~ spl507_47 ),
inference(duplicate_literal_removal,[],[f40922]) ).
fof(f40961,plain,
( ! [X0] :
( ~ m1_subset_1(sK346(X0,sF506),sF503)
| r1_tarski(X0,sF506)
| ~ r2_hidden(sK346(X0,sF506),sF504) )
| ~ spl507_30
| ~ spl507_42
| ~ spl507_47 ),
inference(resolution,[],[f38819,f40923]) ).
fof(f40966,plain,
( ! [X0] :
( r1_tarski(X0,sF506)
| ~ r2_hidden(sK346(X0,sF506),sF504)
| ~ r2_hidden(sK346(X0,sF506),sF504) )
| ~ spl507_14
| ~ spl507_30
| ~ spl507_42
| ~ spl507_47 ),
inference(resolution,[],[f40961,f40746]) ).
fof(f40968,plain,
( ! [X0] :
( ~ r2_hidden(sK346(X0,sF506),sF504)
| r1_tarski(X0,sF506) )
| ~ spl507_14
| ~ spl507_30
| ~ spl507_42
| ~ spl507_47 ),
inference(duplicate_literal_removal,[],[f40966]) ).
fof(f41027,plain,
( ! [X0] :
( ~ m1_filter_2(X0,sK45)
| v3_struct_0(sK45)
| ~ v1_xboole_0(X0)
| ~ l3_lattices(sK45) )
| ~ spl507_4 ),
inference(resolution,[],[f38134,f40381]) ).
fof(f41029,definition,
( spl507_69
<=> ! [X0] :
( ~ m1_filter_2(X0,sK45)
| ~ v1_xboole_0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl507_69])],[avatar_definition]) ).
fof(f41030,plain,
( ! [X0] :
( ~ v1_xboole_0(X0)
| ~ m1_filter_2(X0,sK45) )
| ~ spl507_69 ),
inference(avatar_component_clause,[],[f41029]) ).
fof(f41031,plain,
( ~ spl507_3
| spl507_5
| spl507_69
| ~ spl507_4 ),
inference(avatar_split_clause,[],[f41027,f40380,f41029,f40384,f40376]) ).
fof(f41244,plain,
( ~ m1_filter_2(sF503,sK45)
| ~ spl507_16
| ~ spl507_69 ),
inference(resolution,[],[f41030,f40469]) ).
fof(f41248,plain,
( ~ m1_filter_0(sF503,sK45)
| v3_struct_0(sK45)
| ~ v10_lattices(sK45)
| ~ l3_lattices(sK45)
| ~ spl507_16
| ~ spl507_69 ),
inference(resolution,[],[f41244,f38131]) ).
fof(f41249,plain,
( ~ spl507_3
| ~ spl507_4
| spl507_5
| ~ spl507_26
| ~ spl507_16
| ~ spl507_69 ),
inference(avatar_split_clause,[],[f41248,f41029,f40467,f40536,f40384,f40380,f40376]) ).
fof(f41289,plain,
( ~ m2_lattice4(sF506,sK45)
| spl507_15
| ~ spl507_34 ),
inference(resolution,[],[f40465,f40614]) ).
fof(f41291,plain,
( ~ spl507_22
| spl507_15
| ~ spl507_34 ),
inference(avatar_split_clause,[],[f41289,f40613,f40463,f40502]) ).
fof(f41293,plain,
( ! [X0] :
( m1_subset_1(X0,sF503)
| ~ r2_hidden(X0,sF506) )
| ~ spl507_15 ),
inference(resolution,[],[f40464,f37651]) ).
fof(f41340,definition,
( spl507_113
<=> r2_hidden(sK346(sF506,sF504),sF504) ),
introduced(definition,[new_symbols(definition,[spl507_113])],[avatar_definition]) ).
fof(f41341,plain,
( ~ r2_hidden(sK346(sF506,sF504),sF504)
| spl507_113 ),
inference(avatar_component_clause,[],[f41340]) ).
fof(f41342,plain,
( r2_hidden(sK346(sF506,sF504),sF504)
| ~ spl507_113 ),
inference(avatar_component_clause,[],[f41340]) ).
fof(f41344,definition,
( spl507_114
<=> r2_hidden(sK346(sF506,sF504),sF506) ),
introduced(definition,[new_symbols(definition,[spl507_114])],[avatar_definition]) ).
fof(f41351,definition,
( spl507_115
<=> m1_subset_1(sK346(sF506,sF504),sF503) ),
introduced(definition,[new_symbols(definition,[spl507_115])],[avatar_definition]) ).
fof(f41353,plain,
( ~ m1_subset_1(sK346(sF506,sF504),sF503)
| spl507_115 ),
inference(avatar_component_clause,[],[f41351]) ).
fof(f41389,plain,
! [X0,X1] :
( ~ r1_tarski(X1,X0)
| X0 = X1
| r2_hidden(sK346(X0,X1),X0) ),
inference(resolution,[],[f38815,f38818]) ).
fof(f41501,definition,
( spl507_131
<=> r1_tarski(sF506,sF504) ),
introduced(definition,[new_symbols(definition,[spl507_131])],[avatar_definition]) ).
fof(f41503,plain,
( r1_tarski(sF506,sF504)
| ~ spl507_131 ),
inference(avatar_component_clause,[],[f41501]) ).
fof(f41510,definition,
( spl507_133
<=> r1_tarski(sF504,sF506) ),
introduced(definition,[new_symbols(definition,[spl507_133])],[avatar_definition]) ).
fof(f41511,plain,
( ~ r1_tarski(sF504,sF506)
| spl507_133 ),
inference(avatar_component_clause,[],[f41510]) ).
fof(f41512,plain,
( r1_tarski(sF504,sF506)
| ~ spl507_133 ),
inference(avatar_component_clause,[],[f41510]) ).
fof(f41543,plain,
( sF504 = sF506
| r2_hidden(sK346(sF506,sF504),sF506)
| ~ spl507_133 ),
inference(resolution,[],[f41512,f41389]) ).
fof(f41548,definition,
( spl507_138
<=> sF504 = sF506 ),
introduced(definition,[new_symbols(definition,[spl507_138])],[avatar_definition]) ).
fof(f41550,plain,
( sF504 = sF506
| ~ spl507_138 ),
inference(avatar_component_clause,[],[f41548]) ).
fof(f41552,plain,
( spl507_114
| spl507_138
| ~ spl507_133 ),
inference(avatar_split_clause,[],[f41543,f41510,f41548,f41344]) ).
fof(f41553,plain,
( r1_tarski(sF506,sF504)
| ~ spl507_113 ),
inference(resolution,[],[f41342,f38819]) ).
fof(f41554,plain,
( spl507_131
| ~ spl507_113 ),
inference(avatar_split_clause,[],[f41553,f41340,f41501]) ).
fof(f41566,plain,
( ~ r2_hidden(sK346(sF506,sF504),sF506)
| ~ spl507_15
| spl507_115 ),
inference(resolution,[],[f41353,f41293]) ).
fof(f41573,plain,
( ~ spl507_114
| ~ spl507_15
| spl507_115 ),
inference(avatar_split_clause,[],[f41566,f41351,f40463,f41344]) ).
fof(f41575,plain,
( ~ r1_filter_2(sF503,sF504,sF504)
| ~ spl507_138 ),
inference(superposition,[],[f40315,f41550]) ).
fof(f41605,plain,
( v1_xboole_0(sF503)
| ~ m1_subset_1(sF504,k1_zfmisc_1(sF503))
| ~ spl507_138 ),
inference(resolution,[],[f41575,f40632]) ).
fof(f41608,plain,
( ~ spl507_14
| spl507_16
| ~ spl507_138 ),
inference(avatar_split_clause,[],[f41605,f41548,f40467,f40459]) ).
fof(f41630,plain,
( sF504 = sF506
| ~ r1_tarski(sF504,sF506)
| ~ spl507_131 ),
inference(resolution,[],[f41503,f38815]) ).
fof(f41633,plain,
( ~ spl507_133
| spl507_138
| ~ spl507_131 ),
inference(avatar_split_clause,[],[f41630,f41501,f41548,f41510]) ).
fof(f41635,definition,
( spl507_140
<=> r2_hidden(sK346(sF504,sF506),sF504) ),
introduced(definition,[new_symbols(definition,[spl507_140])],[avatar_definition]) ).
fof(f41637,plain,
( r2_hidden(sK346(sF504,sF506),sF504)
| ~ spl507_140 ),
inference(avatar_component_clause,[],[f41635]) ).
fof(f41709,plain,
( r1_tarski(sF504,sF506)
| ~ spl507_14
| ~ spl507_30
| ~ spl507_42
| ~ spl507_47
| ~ spl507_140 ),
inference(resolution,[],[f41637,f40968]) ).
fof(f41710,plain,
( spl507_133
| ~ spl507_14
| ~ spl507_30
| ~ spl507_42
| ~ spl507_47
| ~ spl507_140 ),
inference(avatar_split_clause,[],[f41709,f41635,f40784,f40723,f40572,f40459,f41510]) ).
fof(f41717,plain,
( ~ r2_hidden(sK346(sF506,sF504),sF506)
| ~ m1_subset_1(sK346(sF506,sF504),sF503)
| ~ spl507_38
| ~ spl507_56
| spl507_113 ),
inference(resolution,[],[f41341,f40900]) ).
fof(f41720,plain,
( ~ spl507_115
| ~ spl507_114
| ~ spl507_38
| ~ spl507_56
| spl507_113 ),
inference(avatar_split_clause,[],[f41717,f41340,f40894,f40674,f41344,f41351]) ).
fof(f41741,plain,
( r2_hidden(sK346(sF504,sF506),sF504)
| spl507_133 ),
inference(resolution,[],[f41511,f38818]) ).
fof(f41742,plain,
( spl507_140
| spl507_133 ),
inference(avatar_split_clause,[],[f41741,f41510,f41635]) ).
cnf(s3,plain,
( ~ spl507_3
| ~ spl507_4
| spl507_5
| spl507_6
| ~ spl507_7 ),
inference(sat_conversion,[],[f40396]) ).
cnf(s6,plain,
spl507_3,
inference(sat_conversion,[],[f40409]) ).
cnf(s7,plain,
( ~ spl507_3
| ~ spl507_4
| spl507_5
| ~ spl507_8
| spl507_10 ),
inference(sat_conversion,[],[f40416]) ).
cnf(s8,plain,
( ~ spl507_3
| ~ spl507_4
| spl507_5
| ~ spl507_7
| spl507_11 ),
inference(sat_conversion,[],[f40425]) ).
cnf(s10,plain,
spl507_4,
inference(sat_conversion,[],[f40428]) ).
cnf(s12,plain,
spl507_7,
inference(sat_conversion,[],[f40431]) ).
cnf(s14,plain,
~ spl507_5,
inference(sat_conversion,[],[f40434]) ).
cnf(s16,plain,
spl507_8,
inference(sat_conversion,[],[f40437]) ).
cnf(s22,plain,
( ~ spl507_3
| ~ spl507_4
| spl507_5
| ~ spl507_7
| ~ spl507_21
| spl507_22 ),
inference(sat_conversion,[],[f40505]) ).
cnf(s25,plain,
( ~ spl507_3
| ~ spl507_4
| spl507_5
| spl507_26 ),
inference(sat_conversion,[],[f40539]) ).
cnf(s28,plain,
( ~ spl507_3
| ~ spl507_4
| spl507_5
| ~ spl507_6
| ~ spl507_7
| spl507_30 ),
inference(sat_conversion,[],[f40574]) ).
cnf(s33,plain,
( ~ spl507_3
| ~ spl507_4
| spl507_5
| spl507_34 ),
inference(sat_conversion,[],[f40615]) ).
cnf(s35,plain,
( ~ spl507_3
| ~ spl507_4
| spl507_5
| ~ spl507_11
| spl507_14
| ~ spl507_34 ),
inference(sat_conversion,[],[f40636]) ).
cnf(s36,plain,
( ~ spl507_3
| ~ spl507_4
| spl507_5
| ~ spl507_6
| ~ spl507_7
| spl507_36 ),
inference(sat_conversion,[],[f40646]) ).
cnf(s38,plain,
( ~ spl507_3
| ~ spl507_4
| spl507_5
| ~ spl507_6
| ~ spl507_7
| spl507_38 ),
inference(sat_conversion,[],[f40676]) ).
cnf(s44,plain,
( ~ spl507_3
| ~ spl507_4
| spl507_5
| ~ spl507_8
| spl507_42 ),
inference(sat_conversion,[],[f40725]) ).
cnf(s45,plain,
( ~ spl507_10
| ~ spl507_14
| spl507_21
| ~ spl507_36 ),
inference(sat_conversion,[],[f40752]) ).
cnf(s46,plain,
( spl507_19
| ~ spl507_21
| ~ spl507_30
| ~ spl507_43 ),
inference(sat_conversion,[],[f40757]) ).
cnf(s49,plain,
( ~ spl507_3
| ~ spl507_4
| spl507_5
| ~ spl507_7
| ~ spl507_8
| ~ spl507_21
| ~ spl507_38
| spl507_43 ),
inference(sat_conversion,[],[f40770]) ).
cnf(s51,plain,
( ~ spl507_3
| ~ spl507_4
| spl507_5
| ~ spl507_7
| ~ spl507_19
| ~ spl507_21
| spl507_47 ),
inference(sat_conversion,[],[f40786]) ).
cnf(s63,plain,
( ~ spl507_3
| ~ spl507_4
| spl507_5
| ~ spl507_7
| ~ spl507_19
| ~ spl507_21
| spl507_56 ),
inference(sat_conversion,[],[f40896]) ).
cnf(s74,plain,
( ~ spl507_3
| ~ spl507_4
| spl507_5
| spl507_69 ),
inference(sat_conversion,[],[f41031]) ).
cnf(s101,plain,
( ~ spl507_3
| ~ spl507_4
| spl507_5
| ~ spl507_16
| ~ spl507_26
| ~ spl507_69 ),
inference(sat_conversion,[],[f41249]) ).
cnf(s109,plain,
( spl507_15
| ~ spl507_22
| ~ spl507_34 ),
inference(sat_conversion,[],[f41291]) ).
cnf(s142,plain,
( spl507_114
| ~ spl507_133
| spl507_138 ),
inference(sat_conversion,[],[f41552]) ).
cnf(s143,plain,
( ~ spl507_113
| spl507_131 ),
inference(sat_conversion,[],[f41554]) ).
cnf(s154,plain,
( ~ spl507_15
| ~ spl507_114
| spl507_115 ),
inference(sat_conversion,[],[f41573]) ).
cnf(s159,plain,
( ~ spl507_14
| spl507_16
| ~ spl507_138 ),
inference(sat_conversion,[],[f41608]) ).
cnf(s165,plain,
( ~ spl507_131
| ~ spl507_133
| spl507_138 ),
inference(sat_conversion,[],[f41633]) ).
cnf(s178,plain,
( ~ spl507_14
| ~ spl507_30
| ~ spl507_42
| ~ spl507_47
| spl507_133
| ~ spl507_140 ),
inference(sat_conversion,[],[f41710]) ).
cnf(s183,plain,
( ~ spl507_38
| ~ spl507_56
| spl507_113
| ~ spl507_114
| ~ spl507_115 ),
inference(sat_conversion,[],[f41720]) ).
cnf(s188,plain,
( spl507_133
| spl507_140 ),
inference(sat_conversion,[],[f41742]) ).
cnf(s190,plain,
( ~ spl507_3
| spl507_11 ),
inference(rat,[],[s8,s12,s14,s10]) ).
cnf(s191,plain,
( ~ spl507_3
| spl507_10 ),
inference(rat,[],[s7,s16,s14,s10]) ).
cnf(s220,plain,
spl507_69,
inference(rat,[],[s74,s10,s14,s6]) ).
cnf(s227,plain,
spl507_42,
inference(rat,[],[s44,s10,s16,s14,s6]) ).
cnf(s230,plain,
spl507_34,
inference(rat,[],[s33,s10,s14,s6]) ).
cnf(s233,plain,
spl507_26,
inference(rat,[],[s25,s10,s14,s6]) ).
cnf(s237,plain,
spl507_11,
inference(rat,[],[s190,s6]) ).
cnf(s238,plain,
spl507_10,
inference(rat,[],[s191,s6]) ).
cnf(s242,plain,
~ spl507_16,
inference(rat,[],[s101,s220,s6,s10,s14,s233]) ).
cnf(s246,plain,
spl507_14,
inference(rat,[],[s35,s230,s6,s10,s14,s237]) ).
cnf(s253,plain,
~ spl507_138,
inference(rat,[],[s159,s242,s246]) ).
cnf(s256,plain,
spl507_6,
inference(rat,[],[s3,s12,s14,s10,s6]) ).
cnf(s259,plain,
spl507_38,
inference(rat,[],[s38,s6,s12,s10,s14,s256]) ).
cnf(s260,plain,
spl507_36,
inference(rat,[],[s36,s6,s12,s10,s14,s256]) ).
cnf(s261,plain,
spl507_30,
inference(rat,[],[s28,s6,s12,s10,s14,s256]) ).
cnf(s264,plain,
spl507_21,
inference(rat,[],[s45,s246,s238,s260]) ).
cnf(s266,plain,
spl507_43,
inference(rat,[],[s49,s259,s6,s10,s16,s12,s14,s264]) ).
cnf(s267,plain,
spl507_22,
inference(rat,[],[s22,s6,s10,s12,s14,s264]) ).
cnf(s268,plain,
spl507_19,
inference(rat,[],[s46,s264,s261,s266]) ).
cnf(s269,plain,
spl507_15,
inference(rat,[],[s109,s230,s267]) ).
cnf(s271,plain,
spl507_56,
inference(rat,[],[s63,s264,s6,s10,s12,s14,s268]) ).
cnf(s273,plain,
spl507_47,
inference(rat,[],[s51,s264,s6,s10,s12,s14,s268]) ).
cnf(s285,plain,
spl507_133,
inference(rat,[],[s178,s188,s227,s246,s261,s273]) ).
cnf(s286,plain,
~ spl507_131,
inference(rat,[],[s165,s253,s285]) ).
cnf(s287,plain,
spl507_114,
inference(rat,[],[s142,s253,s285]) ).
cnf(s289,plain,
~ spl507_113,
inference(rat,[],[s143,s286]) ).
cnf(s290,plain,
spl507_115,
inference(rat,[],[s154,s269,s287]) ).
cnf(s292,plain,
$false,
inference(rat,[],[s183,s290,s271,s259,s289,s287]) ).
fof(f41756,plain,
$false,
inference(avatar_sat_refutation,[],[s292]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT329+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.39 % Computer : n004.cluster.edu
% 0.12/0.39 % Model : x86_64 x86_64
% 0.12/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.39 % Memory : 8046.5625MB
% 0.12/0.39 % OS : Linux 6.8.0-71-generic
% 0.12/0.39 % CPULimit : 300
% 0.12/0.39 % WCLimit : 300
% 0.12/0.39 % DateTime : Sun Sep 27 14:41:12 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.43 Running first-order theorem proving
% 0.12/0.43 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
% 14.65/4.97 % (3592991)Detected formulas, will run a generic FOF schedule.
% 14.65/4.97 % (3593000)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2478625928:i=119:av=off:ss=axioms_2978 on theBenchmark for (2978ds/119Mi)
% 14.65/4.97 % (3592999)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=728788430:i=109:sd=1:ins=1:gsp=on:ss=axioms_2978 on theBenchmark for (2978ds/109Mi)
% 14.65/4.97 % (3592997)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=1366270972:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2978 on theBenchmark for (2978ds/134677Mi)
% 14.65/4.97 % (3592998)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=2446933999:i=141695:sd=1:nm=32:gsp=on:ss=included_2978 on theBenchmark for (2978ds/141695Mi)
% 14.65/4.97 % (3592996)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=3703980852:i=141193_2978 on theBenchmark for (2978ds/141193Mi)
% 14.65/4.97 % (3593002)dis-21_1_sil=8000:lcm=predicate:random_seed=1300741514: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)
% 14.65/4.97 % (3593001)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=855914837:s2a=on:i=139:gtg=position_2978 on theBenchmark for (2978ds/139Mi)
% 14.65/4.97 % (3593000)Instruction limit reached!
% 14.65/4.97 % (3593000)------------------------------
% 14.65/4.97 % (3593000)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.65/4.97 % (3593000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.65/4.97 % (3593000)CaDiCaL version: 2.1.3
% 14.65/4.97 % (3593000)Termination reason: Instruction limit
% 14.65/4.97 % (3593000)Termination phase: SInE selection
% 14.65/4.97 % (3593000)Time elapsed: 0.052 s
% 14.65/4.97 % (3593000)Peak memory usage: 136 MB
% 14.65/4.97 % (3593000)Instructions burned: 119 (million)
% 14.65/4.97 % (3593001)Instruction limit reached!
% 14.65/4.97 % (3593001)------------------------------
% 14.65/4.97 % (3593001)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.65/4.97 % (3593001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.65/4.97 % (3593001)CaDiCaL version: 2.1.3
% 14.65/4.97 % (3593001)Termination reason: Instruction limit
% 14.65/4.97 % (3593001)Termination phase: Property scanning
% 14.65/4.97 % (3593001)Time elapsed: 0.062 s
% 14.65/4.97 % (3593001)Peak memory usage: 136 MB
% 14.65/4.97 % (3593001)Instructions burned: 139 (million)
% 14.65/4.97 % (3592999)Instruction limit reached!
% 14.65/4.97 % (3592999)------------------------------
% 14.65/4.97 % (3592999)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.65/4.97 % (3592999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.65/4.97 % (3592999)CaDiCaL version: 2.1.3
% 14.65/4.97 % (3592999)Termination reason: Instruction limit
% 14.65/4.97 % (3592999)Termination phase: SInE selection
% 14.65/4.97 % (3592999)Time elapsed: 0.100 s
% 14.65/4.97 % (3592999)Peak memory usage: 136 MB
% 14.65/4.97 % (3592999)Instructions burned: 112 (million)
% 14.65/4.97 % (3593002)Instruction limit reached!
% 14.65/4.97 % (3593002)------------------------------
% 14.65/4.97 % (3593002)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.65/4.97 % (3593002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.65/4.97 % (3593002)CaDiCaL version: 2.1.3
% 14.65/4.97 % (3593002)Termination reason: Instruction limit
% 14.65/4.97 % (3593002)Termination phase: SInE selection
% 14.65/4.97 % (3593002)Time elapsed: 0.091 s
% 14.65/4.97 % (3593002)Peak memory usage: 136 MB
% 14.65/4.97 % (3593002)Instructions burned: 129 (million)
% 14.65/4.97 % (3593010)lrs+10_1_sil=8000:sp=occurrence:random_seed=1037936579:i=285:sd=3:ss=axioms:sgt=8_2976 on theBenchmark for (2976ds/285Mi)
% 14.65/4.97 % (3593012)lrs+1011_1_sil=32000:sp=occurrence:random_seed=412587885:i=325:sd=1:ss=axioms:sgt=32_2975 on theBenchmark for (2975ds/325Mi)
% 14.65/4.97 % (3593011)lrs+10_1_sil=32000:urr=on:br=off:random_seed=955649511:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2975 on theBenchmark for (2975ds/157Mi)
% 14.65/4.97 % (3593013)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=1168456385:s2a=on:i=248:s2at=1.23:gtg=position_2975 on theBenchmark for (2975ds/248Mi)
% 14.65/4.97 % (3593011)Instruction limit reached!
% 25.01/6.28 % (3593011)------------------------------
% 25.01/6.28 % (3593011)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.01/6.28 % (3593011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.01/6.28 % (3593011)CaDiCaL version: 2.1.3
% 25.01/6.28 % (3593011)Termination reason: Instruction limit
% 25.01/6.28 % (3593011)Termination phase: Property scanning
% 25.01/6.28 % (3593011)Time elapsed: 0.070 s
% 25.01/6.28 % (3593011)Peak memory usage: 136 MB
% 25.01/6.28 % (3593011)Instructions burned: 159 (million)
% 25.01/6.28 % (3593012)Refutation not found, incomplete strategy
% 25.01/6.28 % (3593012)------------------------------
% 25.01/6.28 % (3593012)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.01/6.28 % (3593012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.01/6.28 % (3593012)CaDiCaL version: 2.1.3
% 25.01/6.28 % (3593012)Termination reason: Refutation not found, incomplete strategy
% 25.01/6.28 % (3593012)Time elapsed: 0.126 s
% 25.01/6.28 % (3593012)Peak memory usage: 142 MB
% 25.01/6.28 % (3593012)Instructions burned: 266 (million)
% 25.01/6.28 % (3593010)Instruction limit reached!
% 25.01/6.28 % (3593010)------------------------------
% 25.01/6.28 % (3593010)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.01/6.28 % (3593010)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.01/6.28 % (3593010)CaDiCaL version: 2.1.3
% 25.01/6.28 % (3593010)Termination reason: Instruction limit
% 25.01/6.28 % (3593010)Termination phase: Saturation
% 25.01/6.28 % (3593010)Time elapsed: 0.214 s
% 25.01/6.28 % (3593010)Peak memory usage: 141 MB
% 25.01/6.28 % (3593010)Instructions burned: 286 (million)
% 25.01/6.28 % (3593013)Instruction limit reached!
% 25.01/6.28 % (3593013)------------------------------
% 25.01/6.28 % (3593013)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.01/6.28 % (3593013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.01/6.28 % (3593013)CaDiCaL version: 2.1.3
% 25.01/6.28 % (3593013)Termination reason: Instruction limit
% 25.01/6.28 % (3593013)Termination phase: Property scanning
% 25.01/6.28 % (3593013)Time elapsed: 0.111 s
% 25.01/6.28 % (3593013)Peak memory usage: 136 MB
% 25.01/6.28 % (3593013)Instructions burned: 249 (million)
% 25.01/6.28 % (3593018)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1316643107:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2973 on theBenchmark for (2973ds/294Mi)
% 25.01/6.28 % (3593012)------------------------------
% 25.01/6.28 % (3593012)------------------------------
% 25.01/6.28 % (3593019)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=975838335:i=2350_2972 on theBenchmark for (2972ds/2350Mi)
% 25.01/6.28 % (3593020)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3319402855:cts=off:i=113:fsr=off:ss=included:sgt=4_2972 on theBenchmark for (2972ds/113Mi)
% 25.01/6.28 % (3593018)Instruction limit reached!
% 25.01/6.28 % (3593018)------------------------------
% 25.01/6.28 % (3593018)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.01/6.28 % (3593018)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.01/6.28 % (3593018)CaDiCaL version: 2.1.3
% 25.01/6.28 % (3593018)Termination reason: Instruction limit
% 25.01/6.28 % (3593018)Termination phase: SInE selection
% 25.01/6.28 % (3593018)Time elapsed: 0.182 s
% 25.01/6.28 % (3593018)Peak memory usage: 137 MB
% 25.01/6.28 % (3593018)Instructions burned: 296 (million)
% 25.01/6.28 % (3593022)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2645383808:i=127:av=off:fsr=off:sup=off_2971 on theBenchmark for (2971ds/127Mi)
% 25.01/6.28 % (3593020)Instruction limit reached!
% 25.01/6.28 % (3593020)------------------------------
% 25.01/6.28 % (3593020)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.01/6.28 % (3593020)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.01/6.28 % (3593020)CaDiCaL version: 2.1.3
% 25.01/6.28 % (3593020)Termination reason: Instruction limit
% 25.01/6.28 % (3593020)Termination phase: SInE selection
% 25.01/6.28 % (3593020)Time elapsed: 0.088 s
% 25.01/6.28 % (3593020)Peak memory usage: 136 MB
% 25.01/6.28 % (3593020)Instructions burned: 114 (million)
% 25.01/6.28 % (3593022)Instruction limit reached!
% 25.01/6.28 % (3593022)------------------------------
% 25.01/6.28 % (3593022)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.01/6.28 % (3593022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.02/9.52 % (3593022)CaDiCaL version: 2.1.3
% 48.02/9.52 % (3593022)Termination reason: Instruction limit
% 48.02/9.52 % (3593022)Termination phase: Preprocessing 1
% 48.02/9.52 % (3593022)Time elapsed: 0.058 s
% 48.02/9.52 % (3593022)Peak memory usage: 137 MB
% 48.02/9.52 % (3593022)Instructions burned: 129 (million)
% 48.02/9.52 % (3593025)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2727374566:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2970 on theBenchmark for (2970ds/114Mi)
% 48.02/9.52 % (3593027)lrs+10_1_sil=8000:sp=occurrence:random_seed=2324079975:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2970 on theBenchmark for (2970ds/907Mi)
% 48.02/9.52 % (3593025)Instruction limit reached!
% 48.02/9.52 % (3593025)------------------------------
% 48.02/9.52 % (3593025)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.02/9.52 % (3593025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.02/9.52 % (3593025)CaDiCaL version: 2.1.3
% 48.02/9.52 % (3593025)Termination reason: Instruction limit
% 48.02/9.52 % (3593025)Termination phase: Property scanning
% 48.02/9.52 % (3593025)Time elapsed: 0.052 s
% 48.02/9.52 % (3593025)Peak memory usage: 136 MB
% 48.02/9.52 % (3593025)Instructions burned: 116 (million)
% 48.02/9.52 % (3593028)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=873844487:i=437:sd=1:aac=none:ss=included_2969 on theBenchmark for (2969ds/437Mi)
% 48.02/9.52 % (3593032)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2765229585:i=5202:ss=axioms:sgt=16_2968 on theBenchmark for (2968ds/5202Mi)
% 48.02/9.52 % (3593028)Instruction limit reached!
% 48.02/9.52 % (3593028)------------------------------
% 48.02/9.52 % (3593028)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.02/9.52 % (3593028)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.02/9.52 % (3593028)CaDiCaL version: 2.1.3
% 48.02/9.52 % (3593028)Termination reason: Instruction limit
% 48.02/9.52 % (3593028)Termination phase: Saturation
% 48.02/9.52 % (3593028)Time elapsed: 0.178 s
% 48.02/9.52 % (3593028)Peak memory usage: 144 MB
% 48.02/9.52 % (3593028)Instructions burned: 439 (million)
% 48.02/9.52 % (3593034)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=977293157:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2966 on theBenchmark for (2966ds/134Mi)
% 48.02/9.52 % (3593034)Instruction limit reached!
% 48.02/9.52 % (3593034)------------------------------
% 48.02/9.52 % (3593034)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.02/9.52 % (3593034)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.02/9.52 % (3593034)CaDiCaL version: 2.1.3
% 48.02/9.52 % (3593034)Termination reason: Instruction limit
% 48.02/9.52 % (3593034)Termination phase: SInE selection
% 48.02/9.52 % (3593034)Time elapsed: 0.060 s
% 48.02/9.52 % (3593034)Peak memory usage: 136 MB
% 48.02/9.52 % (3593034)Instructions burned: 135 (million)
% 48.02/9.52 % (3593036)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2648076698:st=8:i=592:sd=3:ep=RST:ss=axioms_2964 on theBenchmark for (2964ds/592Mi)
% 48.02/9.52 % (3593027)Instruction limit reached!
% 48.02/9.52 % (3593027)------------------------------
% 48.02/9.52 % (3593027)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.02/9.52 % (3593027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.02/9.52 % (3593027)CaDiCaL version: 2.1.3
% 48.02/9.52 % (3593027)Termination reason: Instruction limit
% 48.02/9.52 % (3593027)Termination phase: Property scanning
% 48.02/9.52 % (3593027)Time elapsed: 0.621 s
% 48.02/9.52 % (3593027)Peak memory usage: 158 MB
% 48.02/9.52 % (3593027)Instructions burned: 909 (million)
% 48.02/9.52 % (3593038)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=87756693:st=3:i=13193:sd=3:ss=axioms_2962 on theBenchmark for (2962ds/13193Mi)
% 48.02/9.52 % (3593036)Instruction limit reached!
% 48.02/9.52 % (3593036)------------------------------
% 48.02/9.52 % (3593036)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.02/9.52 % (3593036)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.02/9.52 % (3593036)CaDiCaL version: 2.1.3
% 48.02/9.52 % (3593036)Termination reason: Instruction limit
% 48.02/9.52 % (3593036)Termination phase: Preprocessing 2
% 48.02/9.52 % (3593036)Time elapsed: 0.271 s
% 48.02/9.52 % (3593036)Peak memory usage: 153 MB
% 48.02/9.52 % (3593036)Instructions burned: 593 (million)
% 48.02/9.52 % (3593040)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=298853240:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2960 on theBenchmark for (2960ds/125Mi)
% 89.40/15.31 % (3593040)Instruction limit reached!
% 89.40/15.31 % (3593040)------------------------------
% 89.40/15.31 % (3593040)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.40/15.31 % (3593040)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.40/15.31 % (3593040)CaDiCaL version: 2.1.3
% 89.40/15.31 % (3593040)Termination reason: Instruction limit
% 89.40/15.31 % (3593040)Termination phase: Property scanning
% 89.40/15.31 % (3593040)Time elapsed: 0.031 s
% 89.40/15.31 % (3593040)Peak memory usage: 136 MB
% 89.40/15.31 % (3593040)Instructions burned: 126 (million)
% 89.40/15.31 % (3593042)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2566176072:i=134:gtgl=5:slsql=off:gtg=exists_sym_2958 on theBenchmark for (2958ds/134Mi)
% 89.40/15.31 % (3593042)Instruction limit reached!
% 89.40/15.31 % (3593042)------------------------------
% 89.40/15.31 % (3593042)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.40/15.31 % (3593042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.40/15.31 % (3593042)CaDiCaL version: 2.1.3
% 89.40/15.31 % (3593042)Termination reason: Instruction limit
% 89.40/15.31 % (3593042)Termination phase: Property scanning
% 89.40/15.31 % (3593042)Time elapsed: 0.034 s
% 89.40/15.31 % (3593042)Peak memory usage: 136 MB
% 89.40/15.31 % (3593042)Instructions burned: 138 (million)
% 89.40/15.31 % (3593044)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1913615067:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2957 on theBenchmark for (2957ds/141Mi)
% 89.40/15.31 % (3593019)Instruction limit reached!
% 89.40/15.31 % (3593019)------------------------------
% 89.40/15.31 % (3593019)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.40/15.31 % (3593019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.40/15.31 % (3593019)CaDiCaL version: 2.1.3
% 89.40/15.31 % (3593019)Termination reason: Instruction limit
% 89.40/15.31 % (3593019)Termination phase: Property scanning
% 89.40/15.31 % (3593019)Time elapsed: 1.553 s
% 89.40/15.31 % (3593019)Peak memory usage: 233 MB
% 89.40/15.31 % (3593019)Instructions burned: 2352 (million)
% 89.40/15.31 % (3593044)Instruction limit reached!
% 89.40/15.31 % (3593044)------------------------------
% 89.40/15.31 % (3593044)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.40/15.31 % (3593044)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.40/15.31 % (3593044)CaDiCaL version: 2.1.3
% 89.40/15.31 % (3593044)Termination reason: Instruction limit
% 89.40/15.31 % (3593044)Termination phase: SInE selection
% 89.40/15.31 % (3593044)Time elapsed: 0.064 s
% 89.40/15.31 % (3593044)Peak memory usage: 136 MB
% 89.40/15.31 % (3593044)Instructions burned: 143 (million)
% 89.40/15.31 % (3593046)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2880049150:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2955 on theBenchmark for (2955ds/431Mi)
% 89.40/15.31 % (3593047)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=2417817361:i=6060:aac=none:ins=25_2954 on theBenchmark for (2954ds/6060Mi)
% 89.40/15.31 % (3593046)Refutation not found, incomplete strategy
% 89.40/15.31 % (3593046)------------------------------
% 89.40/15.31 % (3593046)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.40/15.31 % (3593046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.40/15.31 % (3593046)CaDiCaL version: 2.1.3
% 89.40/15.31 % (3593046)Termination reason: Refutation not found, incomplete strategy
% 89.40/15.31 % (3593046)Time elapsed: 0.205 s
% 89.40/15.31 % (3593046)Peak memory usage: 142 MB
% 89.40/15.31 % (3593046)Instructions burned: 253 (million)
% 89.40/15.31 % (3593046)------------------------------
% 89.40/15.31 % (3593046)------------------------------
% 89.40/15.31 % (3593050)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=3514852103:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2948 on theBenchmark for (2948ds/150Mi)
% 89.40/15.31 % (3593050)Instruction limit reached!
% 89.40/15.31 % (3593050)------------------------------
% 89.40/15.31 % (3593050)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.47/20.78 % (3593050)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.47/20.78 % (3593050)CaDiCaL version: 2.1.3
% 62.47/20.78 % (3593050)Termination reason: Instruction limit
% 62.47/20.78 % (3593050)Termination phase: SInE selection
% 62.47/20.78 % (3593050)Time elapsed: 0.121 s
% 62.47/20.78 % (3593050)Peak memory usage: 136 MB
% 62.47/20.78 % (3593050)Instructions burned: 151 (million)
% 62.47/20.78 % (3593052)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3896480296:i=14155:bd=all_2945 on theBenchmark for (2945ds/14155Mi)
% 62.47/20.78 % (3593032)Instruction limit reached!
% 62.47/20.78 % (3593032)------------------------------
% 62.47/20.78 % (3593032)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.47/20.78 % (3593032)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.47/20.78 % (3593032)CaDiCaL version: 2.1.3
% 62.47/20.78 % (3593032)Termination reason: Instruction limit
% 62.47/20.78 % (3593032)Termination phase: Saturation
% 62.47/20.78 % (3593032)Time elapsed: 3.743 s
% 62.47/20.78 % (3593032)Peak memory usage: 557 MB
% 62.47/20.78 % (3593032)Instructions burned: 5202 (million)
% 62.47/20.78 % (3593054)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=855348262:i=667:av=off:fsr=off_2928 on theBenchmark for (2928ds/667Mi)
% 62.47/20.78 % (3593054)Instruction limit reached!
% 62.47/20.78 % (3593054)------------------------------
% 62.47/20.78 % (3593054)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.47/20.78 % (3593054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.47/20.78 % (3593054)CaDiCaL version: 2.1.3
% 62.47/20.78 % (3593054)Termination reason: Instruction limit
% 62.47/20.78 % (3593054)Termination phase: NewCNF
% 62.47/20.78 % (3593054)Time elapsed: 0.527 s
% 62.47/20.78 % (3593054)Peak memory usage: 186 MB
% 62.47/20.78 % (3593054)Instructions burned: 667 (million)
% 62.47/20.78 % (3593056)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=3713879068:s2a=on:i=185:s2at=1.8:fdi=4_2921 on theBenchmark for (2921ds/185Mi)
% 62.47/20.78 % (3593056)Instruction limit reached!
% 62.47/20.78 % (3593056)------------------------------
% 62.47/20.78 % (3593056)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.47/20.78 % (3593056)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.47/20.78 % (3593056)CaDiCaL version: 2.1.3
% 62.47/20.78 % (3593056)Termination reason: Instruction limit
% 62.47/20.78 % (3593056)Termination phase: SInE selection
% 62.47/20.78 % (3593056)Time elapsed: 0.131 s
% 62.47/20.78 % (3593056)Peak memory usage: 136 MB
% 62.47/20.78 % (3593056)Instructions burned: 187 (million)
% 62.47/20.78 % (3593058)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=3510421505:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2918 on theBenchmark for (2918ds/193Mi)
% 62.47/20.78 % (3593047)Instruction limit reached!
% 62.47/20.78 % (3593047)------------------------------
% 62.47/20.78 % (3593047)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.47/20.78 % (3593047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.47/20.78 % (3593047)CaDiCaL version: 2.1.3
% 62.47/20.78 % (3593047)Termination reason: Instruction limit
% 62.47/20.78 % (3593047)Termination phase: Function definition elimination
% 62.47/20.78 % (3593047)Time elapsed: 3.743 s
% 62.47/20.78 % (3593047)Peak memory usage: 245 MB
% 62.47/20.78 % (3593047)Instructions burned: 6062 (million)
% 62.47/20.78 % (3593058)Instruction limit reached!
% 62.47/20.78 % (3593058)------------------------------
% 62.47/20.78 % (3593058)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.47/20.78 % (3593058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.47/20.78 % (3593058)CaDiCaL version: 2.1.3
% 62.47/20.78 % (3593058)Termination reason: Instruction limit
% 62.47/20.78 % (3593058)Termination phase: SInE selection
% 62.47/20.78 % (3593058)Time elapsed: 0.151 s
% 62.47/20.78 % (3593058)Peak memory usage: 137 MB
% 62.47/20.78 % (3593058)Instructions burned: 194 (million)
% 62.47/20.78 % (3593060)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=3465362143:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2916 on theBenchmark for (2916ds/4850Mi)
% 62.47/20.78 % (3593061)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=299812083:i=12111:sd=1:ss=included_2915 on theBenchmark for (2915ds/12111Mi)
% 62.47/20.78 % (3593060)Instruction limit reached!
% 62.47/20.78 % (3593060)------------------------------
% 62.47/20.78 % (3593060)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.47/20.78 % (3593060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.47/20.78 % (3593060)CaDiCaL version: 2.1.3
% 62.47/20.78 % (3593060)Termination reason: Instruction limit
% 62.47/20.78 % (3593060)Termination phase: Property scanning
% 62.47/20.78 % (3593060)Time elapsed: 2.527 s
% 62.47/20.78 % (3593060)Peak memory usage: 220 MB
% 62.47/20.78 % (3593060)Instructions burned: 4852 (million)
% 62.47/20.78 % (3593064)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3531879653:i=319:kws=precedence:fsr=off_2888 on theBenchmark for (2888ds/319Mi)
% 62.47/20.78 % (3593064)Instruction limit reached!
% 62.47/20.78 % (3593064)------------------------------
% 62.47/20.78 % (3593064)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.47/20.78 % (3593064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.47/20.78 % (3593064)CaDiCaL version: 2.1.3
% 62.47/20.78 % (3593064)Termination reason: Instruction limit
% 62.47/20.78 % (3593064)Termination phase: Unused predicate definition removal
% 62.47/20.78 % (3593064)Time elapsed: 0.253 s
% 62.47/20.78 % (3593064)Peak memory usage: 142 MB
% 62.47/20.78 % (3593064)Instructions burned: 319 (million)
% 62.47/20.78 % (3593066)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=1793907878:i=2064:ep=RST_2884 on theBenchmark for (2884ds/2064Mi)
% 62.47/20.78 % (3593038)Instruction limit reached!
% 62.47/20.78 % (3593038)------------------------------
% 62.47/20.78 % (3593038)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.47/20.78 % (3593038)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.47/20.78 % (3593038)CaDiCaL version: 2.1.3
% 62.47/20.78 % (3593038)Termination reason: Instruction limit
% 62.47/20.78 % (3593038)Termination phase: Saturation
% 62.47/20.78 % (3593038)Time elapsed: 8.010 s
% 62.47/20.78 % (3593038)Peak memory usage: 302 MB
% 62.47/20.78 % (3593038)Instructions burned: 13193 (million)
% 62.47/20.78 % (3593068)dis-1011_128_sil=32000:random_seed=3325527311:i=3706:ep=RST:av=off_2880 on theBenchmark for (2880ds/3706Mi)
% 62.47/20.78 % (3593066)Instruction limit reached!
% 62.47/20.78 % (3593066)------------------------------
% 62.47/20.78 % (3593066)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.47/20.78 % (3593066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.47/20.78 % (3593066)CaDiCaL version: 2.1.3
% 62.47/20.78 % (3593066)Termination reason: Instruction limit
% 62.47/20.78 % (3593066)Termination phase: Property scanning
% 62.47/20.78 % (3593066)Time elapsed: 1.418 s
% 62.47/20.78 % (3593066)Peak memory usage: 233 MB
% 62.47/20.78 % (3593066)Instructions burned: 2064 (million)
% 62.47/20.78 % (3593070)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=2873828126:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2868 on theBenchmark for (2868ds/757Mi)
% 62.47/20.78 % (3593070)Instruction limit reached!
% 62.47/20.78 % (3593070)------------------------------
% 62.47/20.78 % (3593070)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.47/20.78 % (3593070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.47/20.78 % (3593070)CaDiCaL version: 2.1.3
% 62.47/20.78 % (3593070)Termination reason: Instruction limit
% 62.47/20.78 % (3593070)Termination phase: Saturation
% 62.47/20.78 % (3593070)Time elapsed: 0.540 s
% 62.47/20.78 % (3593070)Peak memory usage: 146 MB
% 62.47/20.78 % (3593070)Instructions burned: 757 (million)
% 62.47/20.78 % (3593072)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2970631185:i=13913:ss=axioms:sgt=8_2861 on theBenchmark for (2861ds/13913Mi)
% 62.47/20.78 % (3593068)Instruction limit reached!
% 62.47/20.78 % (3593068)------------------------------
% 62.47/20.78 % (3593068)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.47/20.78 % (3593068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.47/20.78 % (3593068)CaDiCaL version: 2.1.3
% 62.47/20.78 % (3593068)Termination reason: Instruction limit
% 62.47/20.78 % (3593068)Termination phase: Function definition elimination
% 62.47/20.78 % (3593068)Time elapsed: 2.068 s
% 62.47/20.78 % (3593068)Peak memory usage: 242 MB
% 62.47/20.78 % (3593068)Instructions burned: 3706 (million)
% 62.47/20.78 % (3593074)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=862096331:i=9925:aac=none_2857 on theBenchmark for (2857ds/9925Mi)
% 62.47/20.78 % (3593052)Instruction limit reached!
% 62.47/20.78 % (3593052)------------------------------
% 62.47/20.78 % (3593052)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.47/20.78 % (3593052)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.47/20.78 % (3593052)CaDiCaL version: 2.1.3
% 62.47/20.78 % (3593052)Termination reason: Instruction limit
% 62.47/20.78 % (3593052)Termination phase: Saturation
% 62.47/20.78 % (3593052)Time elapsed: 9.849 s
% 62.47/20.78 % (3593052)Peak memory usage: 1383 MB
% 62.47/20.78 % (3593052)Instructions burned: 14156 (million)
% 62.47/20.78 % (3593076)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=2217794210:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2844 on theBenchmark for (2844ds/2479Mi)
% 62.47/20.78 % (3593061)Instruction limit reached!
% 62.47/20.78 % (3593061)------------------------------
% 62.47/20.78 % (3593061)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.47/20.78 % (3593061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.47/20.78 % (3593061)CaDiCaL version: 2.1.3
% 62.47/20.78 % (3593061)Termination reason: Instruction limit
% 62.47/20.78 % (3593061)Termination phase: Saturation
% 62.47/20.78 % (3593061)Time elapsed: 8.546 s
% 62.47/20.78 % (3593061)Peak memory usage: 291 MB
% 62.47/20.78 % (3593061)Instructions burned: 12111 (million)
% 62.47/20.78 % (3593076)Instruction limit reached!
% 62.47/20.78 % (3593076)------------------------------
% 62.47/20.78 % (3593076)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.47/20.78 % (3593076)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.47/20.78 % (3593076)CaDiCaL version: 2.1.3
% 62.47/20.78 % (3593076)Termination reason: Instruction limit
% 62.47/20.78 % (3593076)Termination phase: Saturation
% 62.47/20.78 % (3593076)Time elapsed: 1.602 s
% 62.47/20.78 % (3593076)Peak memory usage: 159 MB
% 62.47/20.78 % (3593076)Instructions burned: 2479 (million)
% 62.47/20.78 % (3593078)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=2072364876:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2827 on theBenchmark for (2827ds/440Mi)
% 62.47/20.78 % (3593079)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=1663351242:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2826 on theBenchmark for (2826ds/11145Mi)
% 62.47/20.78 % (3593078)Instruction limit reached!
% 62.47/20.78 % (3593078)------------------------------
% 62.47/20.78 % (3593078)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.47/20.78 % (3593078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.47/20.78 % (3593078)CaDiCaL version: 2.1.3
% 62.47/20.78 % (3593078)Termination reason: Instruction limit
% 62.47/20.78 % (3593078)Termination phase: Property scanning
% 62.47/20.78 % (3593078)Time elapsed: 0.186 s
% 62.47/20.78 % (3593078)Peak memory usage: 136 MB
% 62.47/20.78 % (3593078)Instructions burned: 440 (million)
% 62.47/20.78 % (3593082)lrs+1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_frequency:lcm=reverse:urr=on:bsr=on:random_seed=3449053935:cts=off:i=3034:av=off:er=known:fsd=on_2824 on theBenchmark for (2824ds/3034Mi)
% 62.47/20.78 % (3593079)First to succeed.
% 62.47/20.78 % (3593082)Instruction limit reached!
% 62.47/20.78 % (3593082)------------------------------
% 62.47/20.78 % (3593082)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.47/20.78 % (3593082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.47/20.78 % (3593082)CaDiCaL version: 2.1.3
% 62.47/20.78 % (3593082)Termination reason: Instruction limit
% 62.47/20.78 % (3593082)Termination phase: Property scanning
% 62.47/20.78 % (3593082)Time elapsed: 1.794 s
% 62.47/20.78 % (3593082)Peak memory usage: 233 MB
% 62.47/20.78 % (3593082)Instructions burned: 3036 (million)
% 62.47/20.78 % (3593079)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3592991"
% 62.47/20.78 % (3593084)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=669073783:st=2:s2a=on:i=524:s2at=2:ss=axioms_2804 on theBenchmark for (2804ds/524Mi)
% 62.47/20.78 % (3593079)Refutation found. Thanks to Tanya!
% 62.47/20.78 % SZS status Theorem for theBenchmark
% 62.47/20.78 % SZS output start Proof for theBenchmark
% See solution above
% 0.17/21.03 % (3593079)------------------------------
% 0.17/21.03 % (3593079)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.17/21.03 % (3593079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.17/21.03 % (3593079)CaDiCaL version: 2.1.3
% 0.17/21.03 % (3593079)Termination reason: Refutation
% 0.17/21.03 % (3593079)Time elapsed: 2.021 s
% 0.17/21.03 % (3593079)Peak memory usage: 233 MB
% 0.17/21.03 % (3593079)Instructions burned: 3088 (million)
% 0.17/21.03 % (3593079)------------------------------
% 0.17/21.03 % (3593079)------------------------------
% 0.17/21.03 % (3592991)Success in time 19.912 s
% 0.17/21.03 % Vampire exiting
%------------------------------------------------------------------------------