%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT329+3 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:47:00 AM UTC 2026
% Result : Theorem 58.14s 9.69s
% Output : Refutation 58.85s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 66
% Syntax : Number of formulae : 429 ( 65 unt; 46 def)
% Number of atoms : 1855 ( 46 equ)
% Maximal formula atoms : 13 ( 4 avg)
% Number of connectives : 2507 (1081 ~;1244 |; 86 &)
% ( 61 <=>; 35 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 57 ( 55 usr; 43 prp; 0-3 aty)
% Number of functors : 13 ( 13 usr; 6 con; 0-3 aty)
% Number of variables : 292 ( 0 sgn 286 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f8,axiom,
! [X0,X1] :
( r1_tarski(X0,X1)
<=> ! [X2] :
( r2_hidden(X2,X0)
=> r2_hidden(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d3_tarski) ).
fof(f38,axiom,
! [X0,X1] :
( X0 = X1
<=> ( r1_tarski(X0,X1)
& r1_tarski(X1,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d10_xboole_0) ).
fof(f480,axiom,
! [X0,X1] :
( ( ~ v1_xboole_0(X0)
=> ( m1_subset_1(X1,X0)
<=> r2_hidden(X1,X0) ) )
& ( v1_xboole_0(X0)
=> ( m1_subset_1(X1,X0)
<=> v1_xboole_0(X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d2_subset_1) ).
fof(f675,axiom,
! [X0,X1] :
( r2_hidden(X0,X1)
=> m1_subset_1(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t1_subset) ).
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/sandbox2/benchmark/theBenchmark.p',t4_subset) ).
fof(f6728,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/sandbox2/benchmark/theBenchmark.p',t45_lattices) ).
fof(f8585,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/sandbox2/benchmark/theBenchmark.p',t12_filter_0) ).
fof(f8588,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> m1_filter_0(u1_struct_0(X0),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t15_filter_0) ).
fof(f8592,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/sandbox2/benchmark/theBenchmark.p',t18_filter_0) ).
fof(f12269,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> m2_lattice4(u1_struct_0(X0),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t10_lattice4) ).
fof(f12317,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/sandbox2/benchmark/theBenchmark.p',dt_m2_lattice4) ).
fof(f13529,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/sandbox2/benchmark/theBenchmark.p',dt_m1_filter_2) ).
fof(f13531,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/sandbox2/benchmark/theBenchmark.p',redefinition_m1_filter_2) ).
fof(f13536,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/sandbox2/benchmark/theBenchmark.p',redefinition_r1_filter_2) ).
fof(f13539,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/sandbox2/benchmark/theBenchmark.p',dt_k2_filter_2) ).
fof(f13540,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/sandbox2/benchmark/theBenchmark.p',redefinition_k2_filter_2) ).
fof(f13571,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/sandbox2/benchmark/theBenchmark.p',dt_k22_filter_2) ).
fof(f13658,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
=> ( r3_lattices(X0,X1,X2)
=> ( r2_hidden(X3,k22_filter_2(X0,X1,X2))
<=> ( r3_lattices(X0,X1,X3)
& r3_lattices(X0,X3,X2) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t63_filter_2) ).
fof(f13661,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/sandbox2/benchmark/theBenchmark.p',t66_filter_2) ).
fof(f13662,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)],[f13661]) ).
fof(f13692,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,[],[f13529]) ).
fof(f13693,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,[],[f13692]) ).
fof(f13696,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,[],[f13531]) ).
fof(f13697,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,[],[f13696]) ).
fof(f13706,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,[],[f13536]) ).
fof(f13707,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,[],[f13706]) ).
fof(f13712,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,[],[f13539]) ).
fof(f13713,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,[],[f13712]) ).
fof(f13714,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,[],[f13540]) ).
fof(f13715,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,[],[f13714]) ).
fof(f13776,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,[],[f13571]) ).
fof(f13777,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,[],[f13776]) ).
fof(f13947,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,[],[f13658]) ).
fof(f13948,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,[],[f13947]) ).
fof(f13953,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,[],[f13662]) ).
fof(f13954,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,[],[f13953]) ).
fof(f13959,plain,
! [X0,X1] :
( ( ( m1_subset_1(X1,X0)
<=> r2_hidden(X1,X0) )
| v1_xboole_0(X0) )
& ( ( m1_subset_1(X1,X0)
<=> v1_xboole_0(X1) )
| ~ v1_xboole_0(X0) ) ),
inference(ennf_transformation,[],[f480]) ).
fof(f13965,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,[],[f12317]) ).
fof(f13966,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,[],[f13965]) ).
fof(f13969,plain,
! [X0] :
( m2_lattice4(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f12269]) ).
fof(f13970,plain,
! [X0] :
( m2_lattice4(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13969]) ).
fof(f13981,plain,
! [X0] :
( m1_filter_0(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f8588]) ).
fof(f13982,plain,
! [X0] :
( m1_filter_0(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13981]) ).
fof(f13985,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(f13986,plain,
! [X0,X1,X2] :
( m1_subset_1(X0,X2)
| ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2)) ),
inference(flattening,[],[f13985]) ).
fof(f14013,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,[],[f8592]) ).
fof(f14014,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,[],[f14013]) ).
fof(f14235,plain,
! [X0,X1] :
( m1_subset_1(X0,X1)
| ~ r2_hidden(X0,X1) ),
inference(ennf_transformation,[],[f675]) ).
fof(f14287,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,[],[f8585]) ).
fof(f14288,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,[],[f14287]) ).
fof(f14289,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,[],[f6728]) ).
fof(f14290,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,[],[f14289]) ).
fof(f14395,plain,
! [X0,X1] :
( r1_tarski(X0,X1)
<=> ! [X2] :
( r2_hidden(X2,X1)
| ~ r2_hidden(X2,X0) ) ),
inference(ennf_transformation,[],[f8]) ).
fof(f14483,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,[],[f13697]) ).
fof(f14485,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,[],[f13707]) ).
fof(f14545,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,[],[f13948]) ).
fof(f14546,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,[],[f14545]) ).
fof(f14547,plain,
( ~ r1_filter_2(u1_struct_0(sK40),k2_filter_2(sK40,sK41),k22_filter_2(sK40,sK41,k6_lattices(sK40)))
& v14_lattices(sK40)
& m1_subset_1(sK41,u1_struct_0(sK40))
& ~ v3_struct_0(sK40)
& v10_lattices(sK40)
& l3_lattices(sK40) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK40,sK41]),skolemize(X0,sK40),skolemize(X1,sK41)],[f13954]) ).
fof(f14548,plain,
! [X0,X1] :
( ( ( ( m1_subset_1(X1,X0)
| ~ r2_hidden(X1,X0) )
& ( r2_hidden(X1,X0)
| ~ m1_subset_1(X1,X0) ) )
| v1_xboole_0(X0) )
& ( ( ( m1_subset_1(X1,X0)
| ~ v1_xboole_0(X1) )
& ( v1_xboole_0(X1)
| ~ m1_subset_1(X1,X0) ) )
| ~ v1_xboole_0(X0) ) ),
inference(nnf_transformation,[],[f13959]) ).
fof(f14569,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,[],[f14014]) ).
fof(f14749,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(f14750,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,[],[f14749]) ).
fof(f14751,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,[],[f14395]) ).
fof(f14752,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,[],[f14751]) ).
fof(f14753,plain,
! [X0,X1] :
( ( r1_tarski(X0,X1)
| ( ~ r2_hidden(sK146(X0,X1),X1)
& r2_hidden(sK146(X0,X1),X0) ) )
& ( ! [X3] :
( r2_hidden(X3,X1)
| ~ r2_hidden(X3,X0) )
| ~ r1_tarski(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK146]),skolemize(X2,sK146(X0,X1))],[f14752]) ).
fof(f14793,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,[],[f13693]) ).
fof(f14794,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,[],[f13693]) ).
fof(f14797,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,[],[f14483]) ).
fof(f14804,plain,
! [X2,X0,X1] :
( 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(cnf_transformation,[],[f14485]) ).
fof(f14807,plain,
! [X0,X1] :
( v3_struct_0(X0)
| m1_filter_2(k2_filter_2(X0,X1),X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f13713]) ).
fof(f14808,plain,
! [X0,X1] :
( v3_struct_0(X0)
| k2_filter_0(X0,X1) = k2_filter_2(X0,X1)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f13715]) ).
fof(f14841,plain,
! [X2,X0,X1] :
( ~ v10_lattices(X0)
| v3_struct_0(X0)
| m2_lattice4(k22_filter_2(X0,X1,X2),X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f13777]) ).
fof(f15084,plain,
! [X2,X3,X0,X1] :
( ~ v10_lattices(X0)
| ~ 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)
| r3_lattices(X0,X1,X3)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f14546]) ).
fof(f15085,plain,
! [X2,X3,X0,X1] :
( ~ r3_lattices(X0,X1,X3)
| r2_hidden(X3,k22_filter_2(X0,X1,X2))
| ~ 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,[],[f14546]) ).
fof(f15089,plain,
l3_lattices(sK40),
inference(cnf_transformation,[],[f14547]) ).
fof(f15090,plain,
v10_lattices(sK40),
inference(cnf_transformation,[],[f14547]) ).
fof(f15091,plain,
~ v3_struct_0(sK40),
inference(cnf_transformation,[],[f14547]) ).
fof(f15092,plain,
m1_subset_1(sK41,u1_struct_0(sK40)),
inference(cnf_transformation,[],[f14547]) ).
fof(f15093,plain,
v14_lattices(sK40),
inference(cnf_transformation,[],[f14547]) ).
fof(f15094,plain,
~ r1_filter_2(u1_struct_0(sK40),k2_filter_2(sK40,sK41),k22_filter_2(sK40,sK41,k6_lattices(sK40))),
inference(cnf_transformation,[],[f14547]) ).
fof(f15100,plain,
! [X0,X1] :
( r2_hidden(X1,X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f14548]) ).
fof(f15113,plain,
! [X0,X1] :
( ~ v10_lattices(X0)
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13966]) ).
fof(f15115,plain,
! [X0] :
( ~ v10_lattices(X0)
| v3_struct_0(X0)
| m2_lattice4(u1_struct_0(X0),X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13970]) ).
fof(f15129,plain,
! [X0] :
( ~ v10_lattices(X0)
| v3_struct_0(X0)
| m1_filter_0(u1_struct_0(X0),X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13982]) ).
fof(f15133,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ r2_hidden(X0,X1)
| m1_subset_1(X0,X2) ),
inference(cnf_transformation,[],[f13986]) ).
fof(f15156,plain,
! [X2,X0,X1] :
( ~ v10_lattices(X0)
| ~ 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)
| r3_lattices(X0,X2,X1)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f14569]) ).
fof(f15157,plain,
! [X2,X0,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(cnf_transformation,[],[f14569]) ).
fof(f15460,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| m1_subset_1(X0,X1) ),
inference(cnf_transformation,[],[f14235]) ).
fof(f15516,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,[],[f14288]) ).
fof(f15517,plain,
! [X0,X1] :
( ~ v14_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| r3_lattices(X0,X1,k6_lattices(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f14290]) ).
fof(f15718,plain,
! [X0,X1] :
( ~ r1_tarski(X0,X1)
| X0 = X1
| ~ r1_tarski(X1,X0) ),
inference(cnf_transformation,[],[f14750]) ).
fof(f15720,plain,
! [X3,X0,X1] :
( ~ r1_tarski(X0,X1)
| ~ r2_hidden(X3,X0)
| r2_hidden(X3,X1) ),
inference(cnf_transformation,[],[f14753]) ).
fof(f15721,plain,
! [X0,X1] :
( r1_tarski(X0,X1)
| r2_hidden(sK146(X0,X1),X0) ),
inference(cnf_transformation,[],[f14753]) ).
fof(f15722,plain,
! [X0,X1] :
( ~ r2_hidden(sK146(X0,X1),X1)
| r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f14753]) ).
fof(f15897,plain,
! [X2,X0] :
( r1_filter_2(X0,X2,X2)
| v1_xboole_0(X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(equality_resolution,[],[f14804]) ).
fof(f15978,definition,
sF161 = u1_struct_0(sK40),
introduced(definition,[new_symbols(definition,[sF161])],[function_definition]) ).
fof(f15979,plain,
u1_struct_0(sK40) = sF161,
inference(reorient_equations,[],[f15978]) ).
fof(f15980,definition,
sF162 = k2_filter_2(sK40,sK41),
introduced(definition,[new_symbols(definition,[sF162])],[function_definition]) ).
fof(f15981,plain,
k2_filter_2(sK40,sK41) = sF162,
inference(reorient_equations,[],[f15980]) ).
fof(f15982,definition,
sF163 = k6_lattices(sK40),
introduced(definition,[new_symbols(definition,[sF163])],[function_definition]) ).
fof(f15983,plain,
k6_lattices(sK40) = sF163,
inference(reorient_equations,[],[f15982]) ).
fof(f15984,definition,
sF164 = k22_filter_2(sK40,sK41,sF163),
introduced(definition,[new_symbols(definition,[sF164])],[function_definition]) ).
fof(f15985,plain,
k22_filter_2(sK40,sK41,sF163) = sF164,
inference(reorient_equations,[],[f15984]) ).
fof(f15986,plain,
~ r1_filter_2(sF161,sF162,sF164),
inference(definition_folding,[],[f15094,f15985,f15983,f15981,f15979]) ).
fof(f15987,plain,
m1_subset_1(sK41,sF161),
inference(definition_folding,[],[f15092,f15979]) ).
fof(f16003,plain,
! [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) ),
inference(duplicate_literal_removal,[],[f15516]) ).
fof(f16024,plain,
! [X2,X0] :
( v1_xboole_0(X0)
| r1_filter_2(X0,X2,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(duplicate_literal_removal,[],[f15897]) ).
fof(f16545,definition,
( spl165_104
<=> l3_lattices(sK40) ),
introduced(definition,[new_symbols(definition,[spl165_104])],[avatar_definition]) ).
fof(f16547,plain,
( l3_lattices(sK40)
| ~ spl165_104 ),
inference(avatar_component_clause,[],[f16545]) ).
fof(f16548,plain,
spl165_104,
inference(avatar_split_clause,[],[f15089,f16545]) ).
fof(f16550,definition,
( spl165_105
<=> v10_lattices(sK40) ),
introduced(definition,[new_symbols(definition,[spl165_105])],[avatar_definition]) ).
fof(f16552,plain,
( v10_lattices(sK40)
| ~ spl165_105 ),
inference(avatar_component_clause,[],[f16550]) ).
fof(f16553,plain,
spl165_105,
inference(avatar_split_clause,[],[f15090,f16550]) ).
fof(f16555,definition,
( spl165_106
<=> v3_struct_0(sK40) ),
introduced(definition,[new_symbols(definition,[spl165_106])],[avatar_definition]) ).
fof(f16557,plain,
( ~ v3_struct_0(sK40)
| spl165_106 ),
inference(avatar_component_clause,[],[f16555]) ).
fof(f16558,plain,
~ spl165_106,
inference(avatar_split_clause,[],[f15091,f16555]) ).
fof(f16560,definition,
( spl165_107
<=> m1_subset_1(sK41,sF161) ),
introduced(definition,[new_symbols(definition,[spl165_107])],[avatar_definition]) ).
fof(f16562,plain,
( m1_subset_1(sK41,sF161)
| ~ spl165_107 ),
inference(avatar_component_clause,[],[f16560]) ).
fof(f16563,plain,
spl165_107,
inference(avatar_split_clause,[],[f15987,f16560]) ).
fof(f16565,definition,
( spl165_108
<=> v14_lattices(sK40) ),
introduced(definition,[new_symbols(definition,[spl165_108])],[avatar_definition]) ).
fof(f16567,plain,
( v14_lattices(sK40)
| ~ spl165_108 ),
inference(avatar_component_clause,[],[f16565]) ).
fof(f16568,plain,
spl165_108,
inference(avatar_split_clause,[],[f15093,f16565]) ).
fof(f16570,definition,
( spl165_109
<=> r1_filter_2(sF161,sF162,sF164) ),
introduced(definition,[new_symbols(definition,[spl165_109])],[avatar_definition]) ).
fof(f16573,plain,
~ spl165_109,
inference(avatar_split_clause,[],[f15986,f16570]) ).
fof(f16594,definition,
( spl165_110
<=> u1_struct_0(sK40) = sF161 ),
introduced(definition,[new_symbols(definition,[spl165_110])],[avatar_definition]) ).
fof(f16596,plain,
( u1_struct_0(sK40) = sF161
| ~ spl165_110 ),
inference(avatar_component_clause,[],[f16594]) ).
fof(f16597,plain,
spl165_110,
inference(avatar_split_clause,[],[f15979,f16594]) ).
fof(f16599,definition,
( spl165_111
<=> k2_filter_2(sK40,sK41) = sF162 ),
introduced(definition,[new_symbols(definition,[spl165_111])],[avatar_definition]) ).
fof(f16601,plain,
( k2_filter_2(sK40,sK41) = sF162
| ~ spl165_111 ),
inference(avatar_component_clause,[],[f16599]) ).
fof(f16602,plain,
spl165_111,
inference(avatar_split_clause,[],[f15981,f16599]) ).
fof(f16604,definition,
( spl165_112
<=> k6_lattices(sK40) = sF163 ),
introduced(definition,[new_symbols(definition,[spl165_112])],[avatar_definition]) ).
fof(f16606,plain,
( k6_lattices(sK40) = sF163
| ~ spl165_112 ),
inference(avatar_component_clause,[],[f16604]) ).
fof(f16607,plain,
spl165_112,
inference(avatar_split_clause,[],[f15983,f16604]) ).
fof(f16609,definition,
( spl165_113
<=> k22_filter_2(sK40,sK41,sF163) = sF164 ),
introduced(definition,[new_symbols(definition,[spl165_113])],[avatar_definition]) ).
fof(f16611,plain,
( k22_filter_2(sK40,sK41,sF163) = sF164
| ~ spl165_113 ),
inference(avatar_component_clause,[],[f16609]) ).
fof(f16612,plain,
spl165_113,
inference(avatar_split_clause,[],[f15985,f16609]) ).
fof(f16633,plain,
( ! [X0] :
( m1_filter_2(k2_filter_2(sK40,X0),sK40)
| ~ v10_lattices(sK40)
| ~ l3_lattices(sK40)
| ~ m1_subset_1(X0,u1_struct_0(sK40)) )
| spl165_106 ),
inference(resolution,[],[f16557,f14807]) ).
fof(f16634,plain,
( ! [X0] :
( k2_filter_2(sK40,X0) = k2_filter_0(sK40,X0)
| ~ v10_lattices(sK40)
| ~ l3_lattices(sK40)
| ~ m1_subset_1(X0,u1_struct_0(sK40)) )
| spl165_106 ),
inference(resolution,[],[f16557,f14808]) ).
fof(f16637,plain,
( ! [X0] :
( k2_filter_2(sK40,X0) = k2_filter_0(sK40,X0)
| ~ l3_lattices(sK40)
| ~ m1_subset_1(X0,u1_struct_0(sK40)) )
| ~ spl165_105
| spl165_106 ),
inference(forward_subsumption_resolution,[],[f16634,f16552]) ).
fof(f16638,plain,
( ! [X0] :
( m1_filter_2(k2_filter_2(sK40,X0),sK40)
| ~ l3_lattices(sK40)
| ~ m1_subset_1(X0,u1_struct_0(sK40)) )
| ~ spl165_105
| spl165_106 ),
inference(forward_subsumption_resolution,[],[f16633,f16552]) ).
fof(f16640,plain,
( ! [X0] :
( k2_filter_2(sK40,X0) = k2_filter_0(sK40,X0)
| ~ m1_subset_1(X0,u1_struct_0(sK40)) )
| ~ spl165_104
| ~ spl165_105
| spl165_106 ),
inference(forward_subsumption_resolution,[],[f16637,f16547]) ).
fof(f16641,plain,
( ! [X0] :
( m1_filter_2(k2_filter_2(sK40,X0),sK40)
| ~ m1_subset_1(X0,u1_struct_0(sK40)) )
| ~ spl165_104
| ~ spl165_105
| spl165_106 ),
inference(forward_subsumption_resolution,[],[f16638,f16547]) ).
fof(f16643,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF161)
| k2_filter_2(sK40,X0) = k2_filter_0(sK40,X0) )
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_110 ),
inference(forward_demodulation,[],[f16640,f16596]) ).
fof(f16644,plain,
( ! [X0] :
( m1_filter_2(k2_filter_2(sK40,X0),sK40)
| ~ m1_subset_1(X0,sF161) )
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_110 ),
inference(forward_demodulation,[],[f16641,f16596]) ).
fof(f16653,plain,
( k2_filter_2(sK40,sK41) = k2_filter_0(sK40,sK41)
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_107
| ~ spl165_110 ),
inference(resolution,[],[f16643,f16562]) ).
fof(f16654,plain,
( sF162 = k2_filter_0(sK40,sK41)
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_107
| ~ spl165_110
| ~ spl165_111 ),
inference(forward_demodulation,[],[f16653,f16601]) ).
fof(f16657,definition,
( spl165_115
<=> sF162 = k2_filter_0(sK40,sK41) ),
introduced(definition,[new_symbols(definition,[spl165_115])],[avatar_definition]) ).
fof(f16659,plain,
( sF162 = k2_filter_0(sK40,sK41)
| ~ spl165_115 ),
inference(avatar_component_clause,[],[f16657]) ).
fof(f16660,plain,
( spl165_115
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_107
| ~ spl165_110
| ~ spl165_111 ),
inference(avatar_split_clause,[],[f16654,f16599,f16594,f16560,f16555,f16550,f16545,f16657]) ).
fof(f16673,plain,
( m1_filter_2(sF162,sK40)
| ~ m1_subset_1(sK41,sF161)
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_110
| ~ spl165_111 ),
inference(superposition,[],[f16644,f16601]) ).
fof(f16674,plain,
( m1_filter_2(sF162,sK40)
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_107
| ~ spl165_110
| ~ spl165_111 ),
inference(forward_subsumption_resolution,[],[f16673,f16562]) ).
fof(f16677,definition,
( spl165_117
<=> m1_filter_2(sF162,sK40) ),
introduced(definition,[new_symbols(definition,[spl165_117])],[avatar_definition]) ).
fof(f16679,plain,
( m1_filter_2(sF162,sK40)
| ~ spl165_117 ),
inference(avatar_component_clause,[],[f16677]) ).
fof(f16680,plain,
( spl165_117
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_107
| ~ spl165_110
| ~ spl165_111 ),
inference(avatar_split_clause,[],[f16674,f16599,f16594,f16560,f16555,f16550,f16545,f16677]) ).
fof(f16688,plain,
( ! [X0,X1] :
( v3_struct_0(sK40)
| m2_lattice4(k22_filter_2(sK40,X0,X1),sK40)
| ~ l3_lattices(sK40)
| ~ m1_subset_1(X0,u1_struct_0(sK40))
| ~ m1_subset_1(X1,u1_struct_0(sK40)) )
| ~ spl165_105 ),
inference(resolution,[],[f14841,f16552]) ).
fof(f16689,plain,
( ! [X0,X1] :
( m2_lattice4(k22_filter_2(sK40,X0,X1),sK40)
| ~ l3_lattices(sK40)
| ~ m1_subset_1(X0,u1_struct_0(sK40))
| ~ m1_subset_1(X1,u1_struct_0(sK40)) )
| ~ spl165_105
| spl165_106 ),
inference(forward_subsumption_resolution,[],[f16688,f16557]) ).
fof(f16690,plain,
( ! [X0,X1] :
( m2_lattice4(k22_filter_2(sK40,X0,X1),sK40)
| ~ m1_subset_1(X0,u1_struct_0(sK40))
| ~ m1_subset_1(X1,u1_struct_0(sK40)) )
| ~ spl165_104
| ~ spl165_105
| spl165_106 ),
inference(forward_subsumption_resolution,[],[f16689,f16547]) ).
fof(f16691,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,sF161)
| m2_lattice4(k22_filter_2(sK40,X0,X1),sK40)
| ~ m1_subset_1(X1,u1_struct_0(sK40)) )
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_110 ),
inference(forward_demodulation,[],[f16690,f16596]) ).
fof(f16692,plain,
( ! [X0,X1] :
( m2_lattice4(k22_filter_2(sK40,X0,X1),sK40)
| ~ m1_subset_1(X0,sF161)
| ~ m1_subset_1(X1,sF161) )
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_110 ),
inference(forward_demodulation,[],[f16691,f16596]) ).
fof(f16731,plain,
( m1_filter_0(u1_struct_0(sK40),sK40)
| ~ spl165_104
| ~ spl165_105
| spl165_106 ),
inference(unit_resulting_resolution,[],[f15129,f16547,f16552,f16557]) ).
fof(f16734,plain,
( m1_filter_0(sF161,sK40)
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_110 ),
inference(forward_demodulation,[],[f16731,f16596]) ).
fof(f16737,definition,
( spl165_122
<=> m1_filter_0(sF161,sK40) ),
introduced(definition,[new_symbols(definition,[spl165_122])],[avatar_definition]) ).
fof(f16739,plain,
( m1_filter_0(sF161,sK40)
| ~ spl165_122 ),
inference(avatar_component_clause,[],[f16737]) ).
fof(f16740,plain,
( spl165_122
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_110 ),
inference(avatar_split_clause,[],[f16734,f16594,f16555,f16550,f16545,f16737]) ).
fof(f16742,plain,
( r2_hidden(k6_lattices(sK40),sF161)
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_108
| ~ spl165_122 ),
inference(unit_resulting_resolution,[],[f16003,f16557,f16547,f16567,f16552,f16739]) ).
fof(f16745,plain,
( r2_hidden(sF163,sF161)
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_108
| ~ spl165_112
| ~ spl165_122 ),
inference(forward_demodulation,[],[f16742,f16606]) ).
fof(f16748,definition,
( spl165_123
<=> r2_hidden(sF163,sF161) ),
introduced(definition,[new_symbols(definition,[spl165_123])],[avatar_definition]) ).
fof(f16750,plain,
( r2_hidden(sF163,sF161)
| ~ spl165_123 ),
inference(avatar_component_clause,[],[f16748]) ).
fof(f16751,plain,
( spl165_123
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_108
| ~ spl165_112
| ~ spl165_122 ),
inference(avatar_split_clause,[],[f16745,f16737,f16604,f16565,f16555,f16550,f16545,f16748]) ).
fof(f16770,plain,
( m2_lattice4(sF164,sK40)
| ~ m1_subset_1(sK41,sF161)
| ~ m1_subset_1(sF163,sF161)
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_110
| ~ spl165_113 ),
inference(superposition,[],[f16692,f16611]) ).
fof(f16771,plain,
( m2_lattice4(sF164,sK40)
| ~ m1_subset_1(sF163,sF161)
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_107
| ~ spl165_110
| ~ spl165_113 ),
inference(forward_subsumption_resolution,[],[f16770,f16562]) ).
fof(f16778,definition,
( spl165_126
<=> m1_subset_1(sF163,sF161) ),
introduced(definition,[new_symbols(definition,[spl165_126])],[avatar_definition]) ).
fof(f16779,plain,
( m1_subset_1(sF163,sF161)
| ~ spl165_126 ),
inference(avatar_component_clause,[],[f16778]) ).
fof(f16780,plain,
( ~ m1_subset_1(sF163,sF161)
| spl165_126 ),
inference(avatar_component_clause,[],[f16778]) ).
fof(f16782,definition,
( spl165_127
<=> m2_lattice4(sF164,sK40) ),
introduced(definition,[new_symbols(definition,[spl165_127])],[avatar_definition]) ).
fof(f16784,plain,
( m2_lattice4(sF164,sK40)
| ~ spl165_127 ),
inference(avatar_component_clause,[],[f16782]) ).
fof(f16785,plain,
( ~ spl165_126
| spl165_127
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_107
| ~ spl165_110
| ~ spl165_113 ),
inference(avatar_split_clause,[],[f16771,f16609,f16594,f16560,f16555,f16550,f16545,f16782,f16778]) ).
fof(f16901,plain,
( m2_lattice4(u1_struct_0(sK40),sK40)
| ~ spl165_104
| ~ spl165_105
| spl165_106 ),
inference(unit_resulting_resolution,[],[f15115,f16547,f16552,f16557]) ).
fof(f16904,plain,
( m2_lattice4(sF161,sK40)
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_110 ),
inference(forward_demodulation,[],[f16901,f16596]) ).
fof(f16907,definition,
( spl165_142
<=> m2_lattice4(sF161,sK40) ),
introduced(definition,[new_symbols(definition,[spl165_142])],[avatar_definition]) ).
fof(f16909,plain,
( m2_lattice4(sF161,sK40)
| ~ spl165_142 ),
inference(avatar_component_clause,[],[f16907]) ).
fof(f16910,plain,
( spl165_142
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_110 ),
inference(avatar_split_clause,[],[f16904,f16594,f16555,f16550,f16545,f16907]) ).
fof(f16913,plain,
( m1_filter_2(sF161,sK40)
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_122 ),
inference(unit_resulting_resolution,[],[f14797,f16547,f16552,f16557,f16739]) ).
fof(f16915,definition,
( spl165_143
<=> m1_filter_2(sF161,sK40) ),
introduced(definition,[new_symbols(definition,[spl165_143])],[avatar_definition]) ).
fof(f16917,plain,
( m1_filter_2(sF161,sK40)
| ~ spl165_143 ),
inference(avatar_component_clause,[],[f16915]) ).
fof(f16918,plain,
( spl165_143
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_122 ),
inference(avatar_split_clause,[],[f16913,f16737,f16555,f16550,f16545,f16915]) ).
fof(f16995,plain,
( m1_subset_1(sF161,k1_zfmisc_1(u1_struct_0(sK40)))
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_142 ),
inference(unit_resulting_resolution,[],[f15113,f16547,f16552,f16557,f16909]) ).
fof(f16996,plain,
( ! [X0] :
( ~ m2_lattice4(X0,sK40)
| v3_struct_0(sK40)
| m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK40)))
| ~ l3_lattices(sK40) )
| ~ spl165_105 ),
inference(resolution,[],[f15113,f16552]) ).
fof(f16997,plain,
( ! [X0] :
( ~ m2_lattice4(X0,sK40)
| m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK40)))
| ~ l3_lattices(sK40) )
| ~ spl165_105
| spl165_106 ),
inference(forward_subsumption_resolution,[],[f16996,f16557]) ).
fof(f16999,plain,
( m1_subset_1(sF161,k1_zfmisc_1(sF161))
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_110
| ~ spl165_142 ),
inference(forward_demodulation,[],[f16995,f16596]) ).
fof(f17000,plain,
( ! [X0] :
( ~ m2_lattice4(X0,sK40)
| m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK40))) )
| ~ spl165_104
| ~ spl165_105
| spl165_106 ),
inference(forward_subsumption_resolution,[],[f16997,f16547]) ).
fof(f17007,definition,
( spl165_151
<=> m1_subset_1(sF161,k1_zfmisc_1(sF161)) ),
introduced(definition,[new_symbols(definition,[spl165_151])],[avatar_definition]) ).
fof(f17009,plain,
( m1_subset_1(sF161,k1_zfmisc_1(sF161))
| ~ spl165_151 ),
inference(avatar_component_clause,[],[f17007]) ).
fof(f17010,plain,
( spl165_151
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_110
| ~ spl165_142 ),
inference(avatar_split_clause,[],[f16999,f16907,f16594,f16555,f16550,f16545,f17007]) ).
fof(f17011,plain,
( ! [X0] :
( m1_subset_1(X0,k1_zfmisc_1(sF161))
| ~ m2_lattice4(X0,sK40) )
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_110 ),
inference(forward_demodulation,[],[f17000,f16596]) ).
fof(f17113,plain,
( m2_lattice4(sF162,sK40)
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_117 ),
inference(unit_resulting_resolution,[],[f14793,f16547,f16552,f16557,f16679]) ).
fof(f17116,definition,
( spl165_163
<=> m2_lattice4(sF162,sK40) ),
introduced(definition,[new_symbols(definition,[spl165_163])],[avatar_definition]) ).
fof(f17118,plain,
( m2_lattice4(sF162,sK40)
| ~ spl165_163 ),
inference(avatar_component_clause,[],[f17116]) ).
fof(f17119,plain,
( spl165_163
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_117 ),
inference(avatar_split_clause,[],[f17113,f16677,f16555,f16550,f16545,f17116]) ).
fof(f17120,plain,
( m1_subset_1(sF162,k1_zfmisc_1(sF161))
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_110
| ~ spl165_163 ),
inference(unit_resulting_resolution,[],[f17011,f17118]) ).
fof(f17123,definition,
( spl165_164
<=> m1_subset_1(sF162,k1_zfmisc_1(sF161)) ),
introduced(definition,[new_symbols(definition,[spl165_164])],[avatar_definition]) ).
fof(f17125,plain,
( m1_subset_1(sF162,k1_zfmisc_1(sF161))
| ~ spl165_164 ),
inference(avatar_component_clause,[],[f17123]) ).
fof(f17126,plain,
( spl165_164
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_110
| ~ spl165_163 ),
inference(avatar_split_clause,[],[f17120,f17116,f16594,f16555,f16550,f16545,f17123]) ).
fof(f17172,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK40))
| v3_struct_0(sK40)
| ~ v10_lattices(sK40)
| r3_lattices(sK40,X0,k6_lattices(sK40))
| ~ l3_lattices(sK40) )
| ~ spl165_108 ),
inference(resolution,[],[f15517,f16567]) ).
fof(f17173,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK40))
| ~ v10_lattices(sK40)
| r3_lattices(sK40,X0,k6_lattices(sK40))
| ~ l3_lattices(sK40) )
| spl165_106
| ~ spl165_108 ),
inference(forward_subsumption_resolution,[],[f17172,f16557]) ).
fof(f17174,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK40))
| r3_lattices(sK40,X0,k6_lattices(sK40))
| ~ l3_lattices(sK40) )
| ~ spl165_105
| spl165_106
| ~ spl165_108 ),
inference(forward_subsumption_resolution,[],[f17173,f16552]) ).
fof(f17175,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK40))
| r3_lattices(sK40,X0,k6_lattices(sK40)) )
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_108 ),
inference(forward_subsumption_resolution,[],[f17174,f16547]) ).
fof(f17176,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF161)
| r3_lattices(sK40,X0,k6_lattices(sK40)) )
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_108
| ~ spl165_110 ),
inference(forward_demodulation,[],[f17175,f16596]) ).
fof(f17177,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF161)
| r3_lattices(sK40,X0,sF163) )
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_108
| ~ spl165_110
| ~ spl165_112 ),
inference(forward_demodulation,[],[f17176,f16606]) ).
fof(f17179,plain,
( r3_lattices(sK40,sK41,sF163)
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_107
| ~ spl165_108
| ~ spl165_110
| ~ spl165_112 ),
inference(resolution,[],[f17177,f16562]) ).
fof(f17181,definition,
( spl165_167
<=> r3_lattices(sK40,sK41,sF163) ),
introduced(definition,[new_symbols(definition,[spl165_167])],[avatar_definition]) ).
fof(f17183,plain,
( r3_lattices(sK40,sK41,sF163)
| ~ spl165_167 ),
inference(avatar_component_clause,[],[f17181]) ).
fof(f17184,plain,
( spl165_167
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_107
| ~ spl165_108
| ~ spl165_110
| ~ spl165_112 ),
inference(avatar_split_clause,[],[f17179,f16604,f16594,f16565,f16560,f16555,f16550,f16545,f17181]) ).
fof(f17242,plain,
( ! [X2,X0,X1] :
( ~ r2_hidden(X0,k22_filter_2(sK40,X1,X2))
| ~ r3_lattices(sK40,X1,X2)
| ~ m1_subset_1(X0,u1_struct_0(sK40))
| ~ m1_subset_1(X2,u1_struct_0(sK40))
| ~ m1_subset_1(X1,u1_struct_0(sK40))
| v3_struct_0(sK40)
| r3_lattices(sK40,X1,X0)
| ~ l3_lattices(sK40) )
| ~ spl165_105 ),
inference(resolution,[],[f15084,f16552]) ).
fof(f17243,plain,
( ! [X2,X0,X1] :
( ~ r2_hidden(X0,k22_filter_2(sK40,X1,X2))
| ~ r3_lattices(sK40,X1,X2)
| ~ m1_subset_1(X0,u1_struct_0(sK40))
| ~ m1_subset_1(X2,u1_struct_0(sK40))
| ~ m1_subset_1(X1,u1_struct_0(sK40))
| r3_lattices(sK40,X1,X0)
| ~ l3_lattices(sK40) )
| ~ spl165_105
| spl165_106 ),
inference(forward_subsumption_resolution,[],[f17242,f16557]) ).
fof(f17244,plain,
( ! [X2,X0,X1] :
( ~ r2_hidden(X0,k22_filter_2(sK40,X1,X2))
| ~ r3_lattices(sK40,X1,X2)
| ~ m1_subset_1(X0,u1_struct_0(sK40))
| ~ m1_subset_1(X2,u1_struct_0(sK40))
| ~ m1_subset_1(X1,u1_struct_0(sK40))
| r3_lattices(sK40,X1,X0) )
| ~ spl165_104
| ~ spl165_105
| spl165_106 ),
inference(forward_subsumption_resolution,[],[f17243,f16547]) ).
fof(f17245,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X0,sF161)
| ~ r2_hidden(X0,k22_filter_2(sK40,X1,X2))
| ~ r3_lattices(sK40,X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(sK40))
| ~ m1_subset_1(X1,u1_struct_0(sK40))
| r3_lattices(sK40,X1,X0) )
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_110 ),
inference(forward_demodulation,[],[f17244,f16596]) ).
fof(f17246,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X2,sF161)
| ~ m1_subset_1(X0,sF161)
| ~ r2_hidden(X0,k22_filter_2(sK40,X1,X2))
| ~ r3_lattices(sK40,X1,X2)
| ~ m1_subset_1(X1,u1_struct_0(sK40))
| r3_lattices(sK40,X1,X0) )
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_110 ),
inference(forward_demodulation,[],[f17245,f16596]) ).
fof(f17247,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X1,sF161)
| ~ m1_subset_1(X2,sF161)
| ~ m1_subset_1(X0,sF161)
| ~ r2_hidden(X0,k22_filter_2(sK40,X1,X2))
| ~ r3_lattices(sK40,X1,X2)
| r3_lattices(sK40,X1,X0) )
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_110 ),
inference(forward_demodulation,[],[f17246,f16596]) ).
fof(f17250,plain,
( m1_subset_1(sF163,sF161)
| ~ spl165_123 ),
inference(unit_resulting_resolution,[],[f15460,f16750]) ).
fof(f17281,plain,
( $false
| ~ spl165_123
| spl165_126 ),
inference(forward_subsumption_resolution,[],[f17250,f16780]) ).
fof(f17282,plain,
( ~ spl165_123
| spl165_126 ),
inference(avatar_contradiction_clause,[],[f17281]) ).
fof(f17459,plain,
( m1_subset_1(sF164,k1_zfmisc_1(sF161))
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_110
| ~ spl165_127 ),
inference(unit_resulting_resolution,[],[f17011,f16784]) ).
fof(f17462,definition,
( spl165_198
<=> m1_subset_1(sF164,k1_zfmisc_1(sF161)) ),
introduced(definition,[new_symbols(definition,[spl165_198])],[avatar_definition]) ).
fof(f17464,plain,
( m1_subset_1(sF164,k1_zfmisc_1(sF161))
| ~ spl165_198 ),
inference(avatar_component_clause,[],[f17462]) ).
fof(f17465,plain,
( spl165_198
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_110
| ~ spl165_127 ),
inference(avatar_split_clause,[],[f17459,f16782,f16594,f16555,f16550,f16545,f17462]) ).
fof(f17629,plain,
( ! [X0,X1] :
( ~ r2_hidden(X0,k2_filter_0(sK40,X1))
| ~ m1_subset_1(X1,u1_struct_0(sK40))
| ~ m1_subset_1(X0,u1_struct_0(sK40))
| v3_struct_0(sK40)
| r3_lattices(sK40,X1,X0)
| ~ l3_lattices(sK40) )
| ~ spl165_105 ),
inference(resolution,[],[f15156,f16552]) ).
fof(f17630,plain,
( ! [X0,X1] :
( ~ r2_hidden(X0,k2_filter_0(sK40,X1))
| ~ m1_subset_1(X1,u1_struct_0(sK40))
| ~ m1_subset_1(X0,u1_struct_0(sK40))
| r3_lattices(sK40,X1,X0)
| ~ l3_lattices(sK40) )
| ~ spl165_105
| spl165_106 ),
inference(forward_subsumption_resolution,[],[f17629,f16557]) ).
fof(f17631,plain,
( ! [X0,X1] :
( ~ r2_hidden(X0,k2_filter_0(sK40,X1))
| ~ m1_subset_1(X1,u1_struct_0(sK40))
| ~ m1_subset_1(X0,u1_struct_0(sK40))
| r3_lattices(sK40,X1,X0) )
| ~ spl165_104
| ~ spl165_105
| spl165_106 ),
inference(forward_subsumption_resolution,[],[f17630,f16547]) ).
fof(f17632,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X1,sF161)
| ~ r2_hidden(X0,k2_filter_0(sK40,X1))
| ~ m1_subset_1(X0,u1_struct_0(sK40))
| r3_lattices(sK40,X1,X0) )
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_110 ),
inference(forward_demodulation,[],[f17631,f16596]) ).
fof(f17633,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,sF161)
| ~ m1_subset_1(X1,sF161)
| ~ r2_hidden(X0,k2_filter_0(sK40,X1))
| r3_lattices(sK40,X1,X0) )
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_110 ),
inference(forward_demodulation,[],[f17632,f16596]) ).
fof(f17641,plain,
( ! [X0,X1] :
( ~ r3_lattices(sK40,sK41,X0)
| ~ m1_subset_1(X1,sF161)
| ~ r2_hidden(X1,k22_filter_2(sK40,sK41,X0))
| ~ m1_subset_1(X0,sF161)
| r3_lattices(sK40,sK41,X1) )
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_107
| ~ spl165_110 ),
inference(resolution,[],[f17247,f16562]) ).
fof(f18237,definition,
( spl165_280
<=> v1_xboole_0(sF161) ),
introduced(definition,[new_symbols(definition,[spl165_280])],[avatar_definition]) ).
fof(f18238,plain,
( ~ v1_xboole_0(sF161)
| spl165_280 ),
inference(avatar_component_clause,[],[f18237]) ).
fof(f18239,plain,
( v1_xboole_0(sF161)
| ~ spl165_280 ),
inference(avatar_component_clause,[],[f18237]) ).
fof(f18318,plain,
( ~ l3_lattices(sK40)
| ~ spl165_105
| spl165_106
| ~ spl165_143
| ~ spl165_280 ),
inference(unit_resulting_resolution,[],[f14794,f18239,f16557,f16917,f16552]) ).
fof(f18336,plain,
( $false
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_143
| ~ spl165_280 ),
inference(forward_subsumption_resolution,[],[f18318,f16547]) ).
fof(f18337,plain,
( ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_143
| ~ spl165_280 ),
inference(avatar_contradiction_clause,[],[f18336]) ).
fof(f18343,plain,
( r1_filter_2(sF161,sF162,sF162)
| ~ spl165_164
| spl165_280 ),
inference(unit_resulting_resolution,[],[f16024,f17125,f18238]) ).
fof(f18347,definition,
( spl165_290
<=> r1_filter_2(sF161,sF162,sF162) ),
introduced(definition,[new_symbols(definition,[spl165_290])],[avatar_definition]) ).
fof(f18350,plain,
( spl165_290
| ~ spl165_164
| spl165_280 ),
inference(avatar_split_clause,[],[f18343,f18237,f17123,f18347]) ).
fof(f18427,plain,
! [X0,X1] :
( ~ r1_tarski(X1,X0)
| X0 = X1
| r2_hidden(sK146(X0,X1),X0) ),
inference(resolution,[],[f15721,f15718]) ).
fof(f19532,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF162)
| m1_subset_1(X0,sF161) )
| ~ spl165_164 ),
inference(resolution,[],[f15133,f17125]) ).
fof(f19533,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF164)
| m1_subset_1(X0,sF161) )
| ~ spl165_198 ),
inference(resolution,[],[f15133,f17464]) ).
fof(f19853,plain,
! [X2,X0,X1] :
( r2_hidden(sK146(X1,X2),X1)
| r2_hidden(X0,X2)
| ~ r2_hidden(X0,X1) ),
inference(resolution,[],[f15720,f15721]) ).
fof(f19931,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF161)
| ~ r2_hidden(X0,k22_filter_2(sK40,sK41,sF163))
| ~ m1_subset_1(sF163,sF161)
| r3_lattices(sK40,sK41,X0) )
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_107
| ~ spl165_110
| ~ spl165_167 ),
inference(resolution,[],[f17641,f17183]) ).
fof(f19934,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF161)
| ~ r2_hidden(X0,k22_filter_2(sK40,sK41,sF163))
| r3_lattices(sK40,sK41,X0) )
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_107
| ~ spl165_110
| ~ spl165_126
| ~ spl165_167 ),
inference(forward_subsumption_resolution,[],[f19931,f16779]) ).
fof(f19936,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF164)
| ~ m1_subset_1(X0,sF161)
| r3_lattices(sK40,sK41,X0) )
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_107
| ~ spl165_110
| ~ spl165_113
| ~ spl165_126
| ~ spl165_167 ),
inference(forward_demodulation,[],[f19934,f16611]) ).
fof(f19937,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF164)
| r3_lattices(sK40,sK41,X0) )
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_107
| ~ spl165_110
| ~ spl165_113
| ~ spl165_126
| ~ spl165_167
| ~ spl165_198 ),
inference(forward_subsumption_resolution,[],[f19936,f19533]) ).
fof(f26974,definition,
( spl165_1203
<=> r2_hidden(sK146(sF162,sF161),sF162) ),
introduced(definition,[new_symbols(definition,[spl165_1203])],[avatar_definition]) ).
fof(f26975,plain,
( ~ r2_hidden(sK146(sF162,sF161),sF162)
| spl165_1203 ),
inference(avatar_component_clause,[],[f26974]) ).
fof(f26976,plain,
( r2_hidden(sK146(sF162,sF161),sF162)
| ~ spl165_1203 ),
inference(avatar_component_clause,[],[f26974]) ).
fof(f27024,definition,
( spl165_1209
<=> r1_tarski(sF162,sF161) ),
introduced(definition,[new_symbols(definition,[spl165_1209])],[avatar_definition]) ).
fof(f27025,plain,
( ~ r1_tarski(sF162,sF161)
| spl165_1209 ),
inference(avatar_component_clause,[],[f27024]) ).
fof(f27026,plain,
( r1_tarski(sF162,sF161)
| ~ spl165_1209 ),
inference(avatar_component_clause,[],[f27024]) ).
fof(f27043,plain,
( m1_subset_1(sK146(sF162,sF161),sF161)
| ~ spl165_164
| ~ spl165_1203 ),
inference(resolution,[],[f26976,f19532]) ).
fof(f27046,definition,
( spl165_1211
<=> m1_subset_1(sK146(sF162,sF161),sF161) ),
introduced(definition,[new_symbols(definition,[spl165_1211])],[avatar_definition]) ).
fof(f27048,plain,
( m1_subset_1(sK146(sF162,sF161),sF161)
| ~ spl165_1211 ),
inference(avatar_component_clause,[],[f27046]) ).
fof(f27049,plain,
( spl165_1211
| ~ spl165_164
| ~ spl165_1203 ),
inference(avatar_split_clause,[],[f27043,f26974,f17123,f27046]) ).
fof(f28405,plain,
( r2_hidden(sK146(sF162,sF161),sF161)
| spl165_280
| ~ spl165_1211 ),
inference(unit_resulting_resolution,[],[f15100,f18238,f27048]) ).
fof(f28971,definition,
( spl165_1445
<=> r2_hidden(sK146(sF162,sF161),sF161) ),
introduced(definition,[new_symbols(definition,[spl165_1445])],[avatar_definition]) ).
fof(f28973,plain,
( r2_hidden(sK146(sF162,sF161),sF161)
| ~ spl165_1445 ),
inference(avatar_component_clause,[],[f28971]) ).
fof(f28974,plain,
( spl165_1445
| spl165_280
| ~ spl165_1211 ),
inference(avatar_split_clause,[],[f28405,f27046,f18237,f28971]) ).
fof(f30129,plain,
( r1_tarski(sF162,sF161)
| ~ spl165_1445 ),
inference(unit_resulting_resolution,[],[f15722,f28973]) ).
fof(f30145,plain,
( $false
| spl165_1209
| ~ spl165_1445 ),
inference(forward_subsumption_resolution,[],[f30129,f27025]) ).
fof(f30146,plain,
( spl165_1209
| ~ spl165_1445 ),
inference(avatar_contradiction_clause,[],[f30145]) ).
fof(f30227,plain,
( ! [X0] :
( r2_hidden(X0,sF161)
| ~ r2_hidden(X0,sF162) )
| ~ spl165_1209 ),
inference(resolution,[],[f27026,f15720]) ).
fof(f38286,definition,
( spl165_2536
<=> r1_tarski(sF162,sF164) ),
introduced(definition,[new_symbols(definition,[spl165_2536])],[avatar_definition]) ).
fof(f38287,plain,
( ~ r1_tarski(sF162,sF164)
| spl165_2536 ),
inference(avatar_component_clause,[],[f38286]) ).
fof(f38288,plain,
( r1_tarski(sF162,sF164)
| ~ spl165_2536 ),
inference(avatar_component_clause,[],[f38286]) ).
fof(f38322,definition,
( spl165_2542
<=> r1_tarski(sF164,sF162) ),
introduced(definition,[new_symbols(definition,[spl165_2542])],[avatar_definition]) ).
fof(f38323,plain,
( r1_tarski(sF164,sF162)
| ~ spl165_2542 ),
inference(avatar_component_clause,[],[f38322]) ).
fof(f38324,plain,
( ~ r1_tarski(sF164,sF162)
| spl165_2542 ),
inference(avatar_component_clause,[],[f38322]) ).
fof(f39204,definition,
( spl165_2637
<=> r2_hidden(sK146(sF162,sF164),sF161) ),
introduced(definition,[new_symbols(definition,[spl165_2637])],[avatar_definition]) ).
fof(f39205,plain,
( ~ r2_hidden(sK146(sF162,sF164),sF161)
| spl165_2637 ),
inference(avatar_component_clause,[],[f39204]) ).
fof(f39206,plain,
( r2_hidden(sK146(sF162,sF164),sF161)
| ~ spl165_2637 ),
inference(avatar_component_clause,[],[f39204]) ).
fof(f39216,plain,
( m1_subset_1(sK146(sF162,sF164),sF161)
| ~ spl165_151
| ~ spl165_2637 ),
inference(unit_resulting_resolution,[],[f15133,f17009,f39206]) ).
fof(f39229,definition,
( spl165_2639
<=> m1_subset_1(sK146(sF162,sF164),sF161) ),
introduced(definition,[new_symbols(definition,[spl165_2639])],[avatar_definition]) ).
fof(f39231,plain,
( m1_subset_1(sK146(sF162,sF164),sF161)
| ~ spl165_2639 ),
inference(avatar_component_clause,[],[f39229]) ).
fof(f39233,plain,
( spl165_2639
| ~ spl165_151
| ~ spl165_2637 ),
inference(avatar_split_clause,[],[f39216,f39204,f17007,f39229]) ).
fof(f39235,definition,
( spl165_2640
<=> r2_hidden(sK146(sF162,sF164),sF164) ),
introduced(definition,[new_symbols(definition,[spl165_2640])],[avatar_definition]) ).
fof(f39236,plain,
( ~ r2_hidden(sK146(sF162,sF164),sF164)
| spl165_2640 ),
inference(avatar_component_clause,[],[f39235]) ).
fof(f39237,plain,
( r2_hidden(sK146(sF162,sF164),sF164)
| ~ spl165_2640 ),
inference(avatar_component_clause,[],[f39235]) ).
fof(f39253,plain,
( sF162 = sF164
| r2_hidden(sK146(sF164,sF162),sF164)
| ~ spl165_2536 ),
inference(resolution,[],[f38288,f18427]) ).
fof(f39257,definition,
( spl165_2641
<=> r2_hidden(sK146(sF164,sF162),sF164) ),
introduced(definition,[new_symbols(definition,[spl165_2641])],[avatar_definition]) ).
fof(f39259,plain,
( r2_hidden(sK146(sF164,sF162),sF164)
| ~ spl165_2641 ),
inference(avatar_component_clause,[],[f39257]) ).
fof(f39261,definition,
( spl165_2642
<=> sF162 = sF164 ),
introduced(definition,[new_symbols(definition,[spl165_2642])],[avatar_definition]) ).
fof(f39262,plain,
( sF162 != sF164
| spl165_2642 ),
inference(avatar_component_clause,[],[f39261]) ).
fof(f39264,plain,
( spl165_2641
| spl165_2642
| ~ spl165_2536 ),
inference(avatar_split_clause,[],[f39253,f38286,f39261,f39257]) ).
fof(f39379,plain,
( r1_tarski(sF162,sF164)
| ~ spl165_2640 ),
inference(resolution,[],[f39237,f15722]) ).
fof(f39389,definition,
( spl165_2650
<=> r3_lattices(sK40,sK41,sK146(sF162,sF164)) ),
introduced(definition,[new_symbols(definition,[spl165_2650])],[avatar_definition]) ).
fof(f39390,plain,
( ~ r3_lattices(sK40,sK41,sK146(sF162,sF164))
| spl165_2650 ),
inference(avatar_component_clause,[],[f39389]) ).
fof(f39391,plain,
( r3_lattices(sK40,sK41,sK146(sF162,sF164))
| ~ spl165_2650 ),
inference(avatar_component_clause,[],[f39389]) ).
fof(f41568,plain,
( ~ r2_hidden(sK146(sF162,sF164),sF162)
| spl165_1203
| spl165_2637 ),
inference(unit_resulting_resolution,[],[f19853,f26975,f39205]) ).
fof(f41574,plain,
( ~ r2_hidden(sK146(sF162,sF164),sF162)
| ~ spl165_1209
| spl165_2637 ),
inference(resolution,[],[f39205,f30227]) ).
fof(f41577,definition,
( spl165_2893
<=> r2_hidden(sK146(sF162,sF164),sF162) ),
introduced(definition,[new_symbols(definition,[spl165_2893])],[avatar_definition]) ).
fof(f41578,plain,
( r2_hidden(sK146(sF162,sF164),sF162)
| ~ spl165_2893 ),
inference(avatar_component_clause,[],[f41577]) ).
fof(f41579,plain,
( ~ r2_hidden(sK146(sF162,sF164),sF162)
| spl165_2893 ),
inference(avatar_component_clause,[],[f41577]) ).
fof(f41580,plain,
( ~ spl165_2893
| ~ spl165_1209
| spl165_2637 ),
inference(avatar_split_clause,[],[f41574,f39204,f27024,f41577]) ).
fof(f41581,plain,
( ~ spl165_2893
| spl165_1203
| spl165_2637 ),
inference(avatar_split_clause,[],[f41568,f39204,f26974,f41577]) ).
fof(f45125,plain,
( r3_lattices(sK40,sK41,sK146(sF164,sF162))
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_107
| ~ spl165_110
| ~ spl165_113
| ~ spl165_126
| ~ spl165_167
| ~ spl165_198
| ~ spl165_2641 ),
inference(resolution,[],[f39259,f19937]) ).
fof(f45126,plain,
( m1_subset_1(sK146(sF164,sF162),sF161)
| ~ spl165_198
| ~ spl165_2641 ),
inference(resolution,[],[f39259,f19533]) ).
fof(f45134,definition,
( spl165_3234
<=> m1_subset_1(sK146(sF164,sF162),sF161) ),
introduced(definition,[new_symbols(definition,[spl165_3234])],[avatar_definition]) ).
fof(f45136,plain,
( m1_subset_1(sK146(sF164,sF162),sF161)
| ~ spl165_3234 ),
inference(avatar_component_clause,[],[f45134]) ).
fof(f45137,plain,
( spl165_3234
| ~ spl165_198
| ~ spl165_2641 ),
inference(avatar_split_clause,[],[f45126,f39257,f17462,f45134]) ).
fof(f45139,definition,
( spl165_3235
<=> r3_lattices(sK40,sK41,sK146(sF164,sF162)) ),
introduced(definition,[new_symbols(definition,[spl165_3235])],[avatar_definition]) ).
fof(f45141,plain,
( r3_lattices(sK40,sK41,sK146(sF164,sF162))
| ~ spl165_3235 ),
inference(avatar_component_clause,[],[f45139]) ).
fof(f45142,plain,
( spl165_3235
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_107
| ~ spl165_110
| ~ spl165_113
| ~ spl165_126
| ~ spl165_167
| ~ spl165_198
| ~ spl165_2641 ),
inference(avatar_split_clause,[],[f45125,f39257,f17462,f17181,f16778,f16609,f16594,f16560,f16555,f16550,f16545,f45139]) ).
fof(f49125,plain,
( r1_tarski(sF162,sF164)
| spl165_2893 ),
inference(unit_resulting_resolution,[],[f15721,f41579]) ).
fof(f49134,plain,
( $false
| spl165_2536
| spl165_2893 ),
inference(forward_subsumption_resolution,[],[f49125,f38287]) ).
fof(f49135,plain,
( spl165_2536
| spl165_2893 ),
inference(avatar_contradiction_clause,[],[f49134]) ).
fof(f49137,plain,
( sF162 != sF164
| r1_filter_2(sF161,sF162,sF164)
| ~ r1_filter_2(sF161,sF162,sF162) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f49302,plain,
( sF162 = sF164
| ~ r1_tarski(sF164,sF162)
| ~ spl165_2536 ),
inference(resolution,[],[f38288,f15718]) ).
fof(f52152,plain,
( r2_hidden(sK146(sF164,sF162),k2_filter_0(sK40,sK41))
| ~ m1_subset_1(sK41,u1_struct_0(sK40))
| ~ m1_subset_1(sK146(sF164,sF162),u1_struct_0(sK40))
| v3_struct_0(sK40)
| ~ v10_lattices(sK40)
| ~ l3_lattices(sK40)
| ~ spl165_3235 ),
inference(resolution,[],[f45141,f15157]) ).
fof(f52159,plain,
( r2_hidden(sK146(sF164,sF162),k2_filter_0(sK40,sK41))
| ~ m1_subset_1(sK41,u1_struct_0(sK40))
| ~ m1_subset_1(sK146(sF164,sF162),u1_struct_0(sK40))
| ~ v10_lattices(sK40)
| ~ l3_lattices(sK40)
| spl165_106
| ~ spl165_3235 ),
inference(forward_subsumption_resolution,[],[f52152,f16557]) ).
fof(f52165,plain,
( r2_hidden(sK146(sF164,sF162),k2_filter_0(sK40,sK41))
| ~ m1_subset_1(sK41,u1_struct_0(sK40))
| ~ m1_subset_1(sK146(sF164,sF162),u1_struct_0(sK40))
| ~ l3_lattices(sK40)
| ~ spl165_105
| spl165_106
| ~ spl165_3235 ),
inference(forward_subsumption_resolution,[],[f52159,f16552]) ).
fof(f52169,plain,
( r2_hidden(sK146(sF164,sF162),k2_filter_0(sK40,sK41))
| ~ m1_subset_1(sK41,u1_struct_0(sK40))
| ~ m1_subset_1(sK146(sF164,sF162),u1_struct_0(sK40))
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_3235 ),
inference(forward_subsumption_resolution,[],[f52165,f16547]) ).
fof(f52173,plain,
( r2_hidden(sK146(sF164,sF162),sF162)
| ~ m1_subset_1(sK41,u1_struct_0(sK40))
| ~ m1_subset_1(sK146(sF164,sF162),u1_struct_0(sK40))
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_115
| ~ spl165_3235 ),
inference(forward_demodulation,[],[f52169,f16659]) ).
fof(f52177,plain,
( ~ m1_subset_1(sK41,sF161)
| r2_hidden(sK146(sF164,sF162),sF162)
| ~ m1_subset_1(sK146(sF164,sF162),u1_struct_0(sK40))
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_110
| ~ spl165_115
| ~ spl165_3235 ),
inference(forward_demodulation,[],[f52173,f16596]) ).
fof(f52181,plain,
( r2_hidden(sK146(sF164,sF162),sF162)
| ~ m1_subset_1(sK146(sF164,sF162),u1_struct_0(sK40))
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_107
| ~ spl165_110
| ~ spl165_115
| ~ spl165_3235 ),
inference(forward_subsumption_resolution,[],[f52177,f16562]) ).
fof(f52185,plain,
( ~ m1_subset_1(sK146(sF164,sF162),sF161)
| r2_hidden(sK146(sF164,sF162),sF162)
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_107
| ~ spl165_110
| ~ spl165_115
| ~ spl165_3235 ),
inference(forward_demodulation,[],[f52181,f16596]) ).
fof(f52197,plain,
( r2_hidden(sK146(sF164,sF162),sF162)
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_107
| ~ spl165_110
| ~ spl165_115
| ~ spl165_3234
| ~ spl165_3235 ),
inference(forward_subsumption_resolution,[],[f52185,f45136]) ).
fof(f52199,definition,
( spl165_3900
<=> r2_hidden(sK146(sF164,sF162),sF162) ),
introduced(definition,[new_symbols(definition,[spl165_3900])],[avatar_definition]) ).
fof(f52201,plain,
( r2_hidden(sK146(sF164,sF162),sF162)
| ~ spl165_3900 ),
inference(avatar_component_clause,[],[f52199]) ).
fof(f52202,plain,
( spl165_3900
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_107
| ~ spl165_110
| ~ spl165_115
| ~ spl165_3234
| ~ spl165_3235 ),
inference(avatar_split_clause,[],[f52197,f45139,f45134,f16657,f16594,f16560,f16555,f16550,f16545,f52199]) ).
fof(f52203,plain,
( r1_tarski(sF164,sF162)
| ~ spl165_3900 ),
inference(unit_resulting_resolution,[],[f15722,f52201]) ).
fof(f52226,plain,
( $false
| spl165_2542
| ~ spl165_3900 ),
inference(forward_subsumption_resolution,[],[f52203,f38324]) ).
fof(f52227,plain,
( spl165_2542
| ~ spl165_3900 ),
inference(avatar_contradiction_clause,[],[f52226]) ).
fof(f52228,plain,
( ~ r1_tarski(sF164,sF162)
| ~ spl165_2536
| spl165_2642 ),
inference(forward_subsumption_resolution,[],[f49302,f39262]) ).
fof(f52229,plain,
( $false
| ~ spl165_2536
| ~ spl165_2542
| spl165_2642 ),
inference(forward_subsumption_resolution,[],[f52228,f38323]) ).
fof(f52230,plain,
( ~ spl165_2536
| ~ spl165_2542
| spl165_2642 ),
inference(avatar_contradiction_clause,[],[f52229]) ).
fof(f52322,plain,
( $false
| spl165_2536
| ~ spl165_2640 ),
inference(forward_subsumption_resolution,[],[f39379,f38287]) ).
fof(f52323,plain,
( spl165_2536
| ~ spl165_2640 ),
inference(avatar_contradiction_clause,[],[f52322]) ).
fof(f53040,plain,
( r3_lattices(sK40,sK146(sF162,sF164),sF163)
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_108
| ~ spl165_110
| ~ spl165_112
| ~ spl165_2639 ),
inference(resolution,[],[f39231,f17177]) ).
fof(f54742,plain,
( ~ r2_hidden(sK146(sF162,sF164),k2_filter_0(sK40,sK41))
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_107
| ~ spl165_110
| ~ spl165_2639
| spl165_2650 ),
inference(unit_resulting_resolution,[],[f17633,f16562,f39231,f39390]) ).
fof(f54758,plain,
( ~ r2_hidden(sK146(sF162,sF164),sF162)
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_107
| ~ spl165_110
| ~ spl165_115
| ~ spl165_2639
| spl165_2650 ),
inference(forward_demodulation,[],[f54742,f16659]) ).
fof(f54763,plain,
( $false
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_107
| ~ spl165_110
| ~ spl165_115
| ~ spl165_2639
| spl165_2650
| ~ spl165_2893 ),
inference(forward_subsumption_resolution,[],[f54758,f41578]) ).
fof(f54764,plain,
( ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_107
| ~ spl165_110
| ~ spl165_115
| ~ spl165_2639
| spl165_2650
| ~ spl165_2893 ),
inference(avatar_contradiction_clause,[],[f54763]) ).
fof(f56105,definition,
( spl165_4218
<=> r3_lattices(sK40,sK146(sF162,sF164),sF163) ),
introduced(definition,[new_symbols(definition,[spl165_4218])],[avatar_definition]) ).
fof(f56107,plain,
( r3_lattices(sK40,sK146(sF162,sF164),sF163)
| ~ spl165_4218 ),
inference(avatar_component_clause,[],[f56105]) ).
fof(f56108,plain,
( spl165_4218
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_108
| ~ spl165_110
| ~ spl165_112
| ~ spl165_2639 ),
inference(avatar_split_clause,[],[f53040,f39229,f16604,f16594,f16565,f16555,f16550,f16545,f56105]) ).
fof(f60293,plain,
( ! [X0] :
( r2_hidden(sK146(sF162,sF164),k22_filter_2(sK40,sK41,X0))
| ~ r3_lattices(sK40,sK146(sF162,sF164),X0)
| ~ r3_lattices(sK40,sK41,X0)
| ~ m1_subset_1(sK146(sF162,sF164),u1_struct_0(sK40))
| ~ m1_subset_1(X0,u1_struct_0(sK40))
| ~ m1_subset_1(sK41,u1_struct_0(sK40))
| v3_struct_0(sK40)
| ~ v10_lattices(sK40)
| ~ l3_lattices(sK40) )
| ~ spl165_2650 ),
inference(resolution,[],[f39391,f15085]) ).
fof(f60296,plain,
( ! [X0] :
( r2_hidden(sK146(sF162,sF164),k22_filter_2(sK40,sK41,X0))
| ~ r3_lattices(sK40,sK146(sF162,sF164),X0)
| ~ r3_lattices(sK40,sK41,X0)
| ~ m1_subset_1(sK146(sF162,sF164),u1_struct_0(sK40))
| ~ m1_subset_1(X0,u1_struct_0(sK40))
| ~ m1_subset_1(sK41,u1_struct_0(sK40))
| ~ v10_lattices(sK40)
| ~ l3_lattices(sK40) )
| spl165_106
| ~ spl165_2650 ),
inference(forward_subsumption_resolution,[],[f60293,f16557]) ).
fof(f60300,plain,
( ! [X0] :
( r2_hidden(sK146(sF162,sF164),k22_filter_2(sK40,sK41,X0))
| ~ r3_lattices(sK40,sK146(sF162,sF164),X0)
| ~ r3_lattices(sK40,sK41,X0)
| ~ m1_subset_1(sK146(sF162,sF164),u1_struct_0(sK40))
| ~ m1_subset_1(X0,u1_struct_0(sK40))
| ~ m1_subset_1(sK41,u1_struct_0(sK40))
| ~ l3_lattices(sK40) )
| ~ spl165_105
| spl165_106
| ~ spl165_2650 ),
inference(forward_subsumption_resolution,[],[f60296,f16552]) ).
fof(f60302,plain,
( ! [X0] :
( r2_hidden(sK146(sF162,sF164),k22_filter_2(sK40,sK41,X0))
| ~ r3_lattices(sK40,sK146(sF162,sF164),X0)
| ~ r3_lattices(sK40,sK41,X0)
| ~ m1_subset_1(sK146(sF162,sF164),u1_struct_0(sK40))
| ~ m1_subset_1(X0,u1_struct_0(sK40))
| ~ m1_subset_1(sK41,u1_struct_0(sK40)) )
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_2650 ),
inference(forward_subsumption_resolution,[],[f60300,f16547]) ).
fof(f60304,plain,
( ! [X0] :
( ~ m1_subset_1(sK146(sF162,sF164),sF161)
| r2_hidden(sK146(sF162,sF164),k22_filter_2(sK40,sK41,X0))
| ~ r3_lattices(sK40,sK146(sF162,sF164),X0)
| ~ r3_lattices(sK40,sK41,X0)
| ~ m1_subset_1(X0,u1_struct_0(sK40))
| ~ m1_subset_1(sK41,u1_struct_0(sK40)) )
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_110
| ~ spl165_2650 ),
inference(forward_demodulation,[],[f60302,f16596]) ).
fof(f60306,plain,
( ! [X0] :
( r2_hidden(sK146(sF162,sF164),k22_filter_2(sK40,sK41,X0))
| ~ r3_lattices(sK40,sK146(sF162,sF164),X0)
| ~ r3_lattices(sK40,sK41,X0)
| ~ m1_subset_1(X0,u1_struct_0(sK40))
| ~ m1_subset_1(sK41,u1_struct_0(sK40)) )
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_110
| ~ spl165_2639
| ~ spl165_2650 ),
inference(forward_subsumption_resolution,[],[f60304,f39231]) ).
fof(f60307,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF161)
| r2_hidden(sK146(sF162,sF164),k22_filter_2(sK40,sK41,X0))
| ~ r3_lattices(sK40,sK146(sF162,sF164),X0)
| ~ r3_lattices(sK40,sK41,X0)
| ~ m1_subset_1(sK41,u1_struct_0(sK40)) )
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_110
| ~ spl165_2639
| ~ spl165_2650 ),
inference(forward_demodulation,[],[f60306,f16596]) ).
fof(f60308,plain,
( ! [X0] :
( ~ m1_subset_1(sK41,sF161)
| ~ m1_subset_1(X0,sF161)
| r2_hidden(sK146(sF162,sF164),k22_filter_2(sK40,sK41,X0))
| ~ r3_lattices(sK40,sK146(sF162,sF164),X0)
| ~ r3_lattices(sK40,sK41,X0) )
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_110
| ~ spl165_2639
| ~ spl165_2650 ),
inference(forward_demodulation,[],[f60307,f16596]) ).
fof(f60309,plain,
( ! [X0] :
( ~ r3_lattices(sK40,sK146(sF162,sF164),X0)
| r2_hidden(sK146(sF162,sF164),k22_filter_2(sK40,sK41,X0))
| ~ m1_subset_1(X0,sF161)
| ~ r3_lattices(sK40,sK41,X0) )
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_107
| ~ spl165_110
| ~ spl165_2639
| ~ spl165_2650 ),
inference(forward_subsumption_resolution,[],[f60308,f16562]) ).
fof(f61472,plain,
( r2_hidden(sK146(sF162,sF164),k22_filter_2(sK40,sK41,sF163))
| ~ m1_subset_1(sF163,sF161)
| ~ r3_lattices(sK40,sK41,sF163)
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_107
| ~ spl165_110
| ~ spl165_2639
| ~ spl165_2650
| ~ spl165_4218 ),
inference(resolution,[],[f56107,f60309]) ).
fof(f61480,plain,
( r2_hidden(sK146(sF162,sF164),k22_filter_2(sK40,sK41,sF163))
| ~ r3_lattices(sK40,sK41,sF163)
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_107
| ~ spl165_110
| ~ spl165_126
| ~ spl165_2639
| ~ spl165_2650
| ~ spl165_4218 ),
inference(forward_subsumption_resolution,[],[f61472,f16779]) ).
fof(f61512,plain,
( r2_hidden(sK146(sF162,sF164),k22_filter_2(sK40,sK41,sF163))
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_107
| ~ spl165_110
| ~ spl165_126
| ~ spl165_167
| ~ spl165_2639
| ~ spl165_2650
| ~ spl165_4218 ),
inference(forward_subsumption_resolution,[],[f61480,f17183]) ).
fof(f61518,plain,
( r2_hidden(sK146(sF162,sF164),sF164)
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_107
| ~ spl165_110
| ~ spl165_113
| ~ spl165_126
| ~ spl165_167
| ~ spl165_2639
| ~ spl165_2650
| ~ spl165_4218 ),
inference(forward_demodulation,[],[f61512,f16611]) ).
fof(f61522,plain,
( $false
| ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_107
| ~ spl165_110
| ~ spl165_113
| ~ spl165_126
| ~ spl165_167
| ~ spl165_2639
| spl165_2640
| ~ spl165_2650
| ~ spl165_4218 ),
inference(forward_subsumption_resolution,[],[f61518,f39236]) ).
fof(f61523,plain,
( ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_107
| ~ spl165_110
| ~ spl165_113
| ~ spl165_126
| ~ spl165_167
| ~ spl165_2639
| spl165_2640
| ~ spl165_2650
| ~ spl165_4218 ),
inference(avatar_contradiction_clause,[],[f61522]) ).
cnf(s104,plain,
spl165_104,
inference(sat_conversion,[],[f16548]) ).
cnf(s105,plain,
spl165_105,
inference(sat_conversion,[],[f16553]) ).
cnf(s106,plain,
~ spl165_106,
inference(sat_conversion,[],[f16558]) ).
cnf(s107,plain,
spl165_107,
inference(sat_conversion,[],[f16563]) ).
cnf(s108,plain,
spl165_108,
inference(sat_conversion,[],[f16568]) ).
cnf(s109,plain,
~ spl165_109,
inference(sat_conversion,[],[f16573]) ).
cnf(s110,plain,
spl165_110,
inference(sat_conversion,[],[f16597]) ).
cnf(s111,plain,
spl165_111,
inference(sat_conversion,[],[f16602]) ).
cnf(s112,plain,
spl165_112,
inference(sat_conversion,[],[f16607]) ).
cnf(s113,plain,
spl165_113,
inference(sat_conversion,[],[f16612]) ).
cnf(s115,plain,
( ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_107
| ~ spl165_110
| ~ spl165_111
| spl165_115 ),
inference(sat_conversion,[],[f16660]) ).
cnf(s118,plain,
( ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_107
| ~ spl165_110
| ~ spl165_111
| spl165_117 ),
inference(sat_conversion,[],[f16680]) ).
cnf(s125,plain,
( ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_110
| spl165_122 ),
inference(sat_conversion,[],[f16740]) ).
cnf(s127,plain,
( ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_108
| ~ spl165_112
| ~ spl165_122
| spl165_123 ),
inference(sat_conversion,[],[f16751]) ).
cnf(s131,plain,
( ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_107
| ~ spl165_110
| ~ spl165_113
| ~ spl165_126
| spl165_127 ),
inference(sat_conversion,[],[f16785]) ).
cnf(s149,plain,
( ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_110
| spl165_142 ),
inference(sat_conversion,[],[f16910]) ).
cnf(s151,plain,
( ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_122
| spl165_143 ),
inference(sat_conversion,[],[f16918]) ).
cnf(s165,plain,
( ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_110
| ~ spl165_142
| spl165_151 ),
inference(sat_conversion,[],[f17010]) ).
cnf(s182,plain,
( ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_117
| spl165_163 ),
inference(sat_conversion,[],[f17119]) ).
cnf(s183,plain,
( ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_110
| ~ spl165_163
| spl165_164 ),
inference(sat_conversion,[],[f17126]) ).
cnf(s188,plain,
( ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_107
| ~ spl165_108
| ~ spl165_110
| ~ spl165_112
| spl165_167 ),
inference(sat_conversion,[],[f17184]) ).
cnf(s199,plain,
( ~ spl165_123
| spl165_126 ),
inference(sat_conversion,[],[f17282]) ).
cnf(s238,plain,
( ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_110
| ~ spl165_127
| spl165_198 ),
inference(sat_conversion,[],[f17465]) ).
cnf(s373,plain,
( ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_143
| ~ spl165_280 ),
inference(sat_conversion,[],[f18337]) ).
cnf(s374,plain,
( ~ spl165_164
| spl165_280
| spl165_290 ),
inference(sat_conversion,[],[f18350]) ).
cnf(s1792,plain,
( ~ spl165_164
| ~ spl165_1203
| spl165_1211 ),
inference(sat_conversion,[],[f27049]) ).
cnf(s2186,plain,
( spl165_280
| ~ spl165_1211
| spl165_1445 ),
inference(sat_conversion,[],[f28974]) ).
cnf(s2482,plain,
( spl165_1209
| ~ spl165_1445 ),
inference(sat_conversion,[],[f30146]) ).
cnf(s4241,plain,
( ~ spl165_151
| ~ spl165_2637
| spl165_2639 ),
inference(sat_conversion,[],[f39233]) ).
cnf(s4250,plain,
( ~ spl165_2536
| spl165_2641
| spl165_2642 ),
inference(sat_conversion,[],[f39264]) ).
cnf(s4613,plain,
( ~ spl165_1209
| spl165_2637
| ~ spl165_2893 ),
inference(sat_conversion,[],[f41580]) ).
cnf(s4615,plain,
( spl165_1203
| spl165_2637
| ~ spl165_2893 ),
inference(sat_conversion,[],[f41581]) ).
cnf(s5160,plain,
( ~ spl165_198
| ~ spl165_2641
| spl165_3234 ),
inference(sat_conversion,[],[f45137]) ).
cnf(s5161,plain,
( ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_107
| ~ spl165_110
| ~ spl165_113
| ~ spl165_126
| ~ spl165_167
| ~ spl165_198
| ~ spl165_2641
| spl165_3235 ),
inference(sat_conversion,[],[f45142]) ).
cnf(s5779,plain,
( spl165_2536
| spl165_2893 ),
inference(sat_conversion,[],[f49135]) ).
cnf(s5781,plain,
( spl165_109
| ~ spl165_290
| ~ spl165_2642 ),
inference(sat_conversion,[],[f49137]) ).
cnf(s6413,plain,
( ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_107
| ~ spl165_110
| ~ spl165_115
| ~ spl165_3234
| ~ spl165_3235
| spl165_3900 ),
inference(sat_conversion,[],[f52202]) ).
cnf(s6416,plain,
( spl165_2542
| ~ spl165_3900 ),
inference(sat_conversion,[],[f52227]) ).
cnf(s6418,plain,
( ~ spl165_2536
| ~ spl165_2542
| spl165_2642 ),
inference(sat_conversion,[],[f52230]) ).
cnf(s6467,plain,
( spl165_2536
| ~ spl165_2640 ),
inference(sat_conversion,[],[f52323]) ).
cnf(s6605,plain,
( ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_107
| ~ spl165_110
| ~ spl165_115
| ~ spl165_2639
| spl165_2650
| ~ spl165_2893 ),
inference(sat_conversion,[],[f54764]) ).
cnf(s7043,plain,
( ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_108
| ~ spl165_110
| ~ spl165_112
| ~ spl165_2639
| spl165_4218 ),
inference(sat_conversion,[],[f56108]) ).
cnf(s7957,plain,
( ~ spl165_104
| ~ spl165_105
| spl165_106
| ~ spl165_107
| ~ spl165_110
| ~ spl165_113
| ~ spl165_126
| ~ spl165_167
| ~ spl165_2639
| spl165_2640
| ~ spl165_2650
| ~ spl165_4218 ),
inference(sat_conversion,[],[f61523]) ).
cnf(s7978,plain,
spl165_167,
inference(rat,[],[s188,s105,s112,s110,s108,s107,s106,s104]) ).
cnf(s7987,plain,
spl165_142,
inference(rat,[],[s149,s105,s110,s106,s104]) ).
cnf(s7995,plain,
spl165_122,
inference(rat,[],[s125,s105,s110,s106,s104]) ).
cnf(s7998,plain,
spl165_117,
inference(rat,[],[s118,s105,s111,s110,s107,s106,s104]) ).
cnf(s8000,plain,
spl165_115,
inference(rat,[],[s115,s105,s111,s110,s107,s106,s104]) ).
cnf(s8046,plain,
spl165_151,
inference(rat,[],[s165,s104,s105,s110,s106,s7987]) ).
cnf(s8077,plain,
spl165_143,
inference(rat,[],[s151,s104,s105,s106,s7995]) ).
cnf(s8078,plain,
spl165_123,
inference(rat,[],[s127,s104,s105,s112,s108,s106,s7995]) ).
cnf(s8080,plain,
spl165_163,
inference(rat,[],[s182,s104,s105,s106,s7998]) ).
cnf(s8115,plain,
~ spl165_280,
inference(rat,[],[s373,s104,s105,s106,s8077]) ).
cnf(s8116,plain,
spl165_126,
inference(rat,[],[s199,s8078]) ).
cnf(s8120,plain,
spl165_164,
inference(rat,[],[s183,s104,s105,s110,s106,s8080]) ).
cnf(s8266,plain,
spl165_127,
inference(rat,[],[s131,s104,s105,s113,s110,s107,s106,s8116]) ).
cnf(s8281,plain,
spl165_290,
inference(rat,[],[s374,s8115,s8120]) ).
cnf(s8395,plain,
spl165_198,
inference(rat,[],[s238,s104,s105,s110,s106,s8266]) ).
cnf(s8401,plain,
~ spl165_2642,
inference(rat,[],[s5781,s109,s8281]) ).
cnf(s8425,plain,
( spl165_2536
| spl165_1203 ),
inference(rat,[],[s7957,s6605,s7043,s4241,s4615,s5779,s6467,s106,s107,s110,s113,s105,s104,s7978,s8116,s8000,s108,s112,s8046]) ).
cnf(s8426,plain,
~ spl165_2536,
inference(rat,[],[s6413,s5161,s5160,s6416,s4250,s6418,s106,s107,s110,s105,s104,s8000,s113,s7978,s8116,s8395,s8401]) ).
cnf(s8427,plain,
~ spl165_2640,
inference(rat,[],[s6467,s8426]) ).
cnf(s8428,plain,
spl165_2893,
inference(rat,[],[s5779,s8426]) ).
cnf(s8429,plain,
spl165_1203,
inference(rat,[],[s8425,s8426]) ).
cnf(s8432,plain,
spl165_1211,
inference(rat,[],[s1792,s8120,s8429]) ).
cnf(s8433,plain,
spl165_1445,
inference(rat,[],[s2186,s8115,s8432]) ).
cnf(s8540,plain,
spl165_1209,
inference(rat,[],[s2482,s8433]) ).
cnf(s8677,plain,
spl165_2637,
inference(rat,[],[s4613,s8428,s8540]) ).
cnf(s8681,plain,
spl165_2639,
inference(rat,[],[s4241,s8046,s8677]) ).
cnf(s8693,plain,
spl165_4218,
inference(rat,[],[s7043,s104,s105,s112,s110,s108,s106,s8681]) ).
cnf(s8738,plain,
spl165_2650,
inference(rat,[],[s6605,s8428,s8000,s104,s105,s110,s107,s106,s8681]) ).
cnf(s8770,plain,
$false,
inference(rat,[],[s7957,s8693,s8427,s8116,s7978,s104,s105,s113,s110,s107,s106,s8738,s8681]) ).
fof(f61544,plain,
$false,
inference(avatar_sat_refutation,[],[s8770]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT329+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.39 % Computer : n026.cluster.edu
% 0.13/0.39 % Model : x86_64 x86_64
% 0.13/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.39 % Memory : 8046.5625MB
% 0.13/0.39 % OS : Linux 6.8.0-71-generic
% 0.13/0.40 % CPULimit : 300
% 0.13/0.40 % WCLimit : 300
% 0.13/0.40 % DateTime : Sun Sep 27 14:44:13 UTC 2026
% 0.13/0.40 % CPUTime :
% 0.13/0.40 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.43 Running first-order theorem proving
% 0.13/0.43 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 12.23/3.19 % (2907874)Detected formulas, will run a generic FOF schedule.
% 12.23/3.19 % (2907882)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1698341834:i=109:sd=1:ins=1:gsp=on:ss=axioms_2993 on theBenchmark for (2993ds/109Mi)
% 12.23/3.19 % (2907879)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=786942880:i=141193_2993 on theBenchmark for (2993ds/141193Mi)
% 12.23/3.19 % (2907881)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=1304468548:i=141695:sd=1:nm=32:gsp=on:ss=included_2993 on theBenchmark for (2993ds/141695Mi)
% 12.23/3.19 % (2907880)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=2816071368:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2993 on theBenchmark for (2993ds/134677Mi)
% 12.23/3.19 % (2907882)Refutation not found, incomplete strategy
% 12.23/3.19 % (2907882)------------------------------
% 12.23/3.19 % (2907882)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.23/3.19 % (2907882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.23/3.19 % (2907882)CaDiCaL version: 2.1.3
% 12.23/3.19 % (2907882)Termination reason: Refutation not found, incomplete strategy
% 12.23/3.19 % (2907882)Time elapsed: 0.042 s
% 12.23/3.19 % (2907882)Peak memory usage: 107 MB
% 12.23/3.19 % (2907882)Instructions burned: 84 (million)
% 12.23/3.19 % (2907884)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=294961649:s2a=on:i=139:gtg=position_2993 on theBenchmark for (2993ds/139Mi)
% 12.23/3.19 % (2907883)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2491158091:i=119:av=off:ss=axioms_2993 on theBenchmark for (2993ds/119Mi)
% 12.23/3.19 % (2907885)dis-21_1_sil=8000:lcm=predicate:random_seed=2596828783:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2993 on theBenchmark for (2993ds/129Mi)
% 12.23/3.19 % (2907884)Instruction limit reached!
% 12.23/3.19 % (2907884)------------------------------
% 12.23/3.19 % (2907884)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.23/3.19 % (2907884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.23/3.19 % (2907884)CaDiCaL version: 2.1.3
% 12.23/3.19 % (2907884)Termination reason: Instruction limit
% 12.23/3.19 % (2907884)Termination phase: Property scanning
% 12.23/3.19 % (2907884)Time elapsed: 0.059 s
% 12.23/3.19 % (2907884)Peak memory usage: 102 MB
% 12.23/3.19 % (2907884)Instructions burned: 140 (million)
% 12.23/3.19 % (2907883)Instruction limit reached!
% 12.23/3.19 % (2907883)------------------------------
% 12.23/3.19 % (2907883)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.23/3.19 % (2907883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.23/3.19 % (2907883)CaDiCaL version: 2.1.3
% 12.23/3.19 % (2907883)Termination reason: Instruction limit
% 12.23/3.19 % (2907883)Termination phase: Function definition elimination
% 12.23/3.19 % (2907883)Time elapsed: 0.093 s
% 12.23/3.19 % (2907883)Peak memory usage: 105 MB
% 12.23/3.19 % (2907883)Instructions burned: 119 (million)
% 12.23/3.19 % (2907885)Instruction limit reached!
% 12.23/3.19 % (2907885)------------------------------
% 12.23/3.19 % (2907885)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.23/3.19 % (2907885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.23/3.19 % (2907885)CaDiCaL version: 2.1.3
% 12.23/3.19 % (2907885)Termination reason: Instruction limit
% 12.23/3.19 % (2907885)Termination phase: Preprocessing 1
% 12.23/3.19 % (2907885)Time elapsed: 0.096 s
% 12.23/3.19 % (2907885)Peak memory usage: 104 MB
% 12.23/3.19 % (2907885)Instructions burned: 129 (million)
% 12.23/3.19 % (2907882)------------------------------
% 12.23/3.19 % (2907882)------------------------------
% 12.23/3.19 % (2907893)lrs+10_1_sil=8000:sp=occurrence:random_seed=3800203133:i=285:sd=3:ss=axioms:sgt=8_2991 on theBenchmark for (2991ds/285Mi)
% 12.23/3.19 % (2907894)lrs+10_1_sil=32000:urr=on:br=off:random_seed=730106745:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2990 on theBenchmark for (2990ds/157Mi)
% 12.23/3.19 % (2907896)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=2427796026:s2a=on:i=248:s2at=1.23:gtg=position_2990 on theBenchmark for (2990ds/248Mi)
% 12.23/3.19 % (2907895)lrs+1011_1_sil=32000:sp=occurrence:random_seed=932437704:i=325:sd=1:ss=axioms:sgt=32_2990 on theBenchmark for (2990ds/325Mi)
% 19.37/4.17 % (2907894)Instruction limit reached!
% 19.37/4.17 % (2907894)------------------------------
% 19.37/4.17 % (2907894)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.37/4.17 % (2907894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.37/4.17 % (2907894)CaDiCaL version: 2.1.3
% 19.37/4.17 % (2907894)Termination reason: Instruction limit
% 19.37/4.17 % (2907894)Termination phase: Property scanning
% 19.37/4.17 % (2907894)Time elapsed: 0.066 s
% 19.37/4.17 % (2907894)Peak memory usage: 103 MB
% 19.37/4.17 % (2907894)Instructions burned: 158 (million)
% 19.37/4.17 % (2907896)Instruction limit reached!
% 19.37/4.17 % (2907896)------------------------------
% 19.37/4.17 % (2907896)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.37/4.17 % (2907896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.37/4.17 % (2907896)CaDiCaL version: 2.1.3
% 19.37/4.17 % (2907896)Termination reason: Instruction limit
% 19.37/4.17 % (2907896)Termination phase: SInE selection
% 19.37/4.17 % (2907896)Time elapsed: 0.068 s
% 19.37/4.17 % (2907896)Peak memory usage: 103 MB
% 19.37/4.17 % (2907896)Instructions burned: 251 (million)
% 19.37/4.17 % (2907893)Instruction limit reached!
% 19.37/4.17 % (2907893)------------------------------
% 19.37/4.17 % (2907893)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.37/4.17 % (2907893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.37/4.17 % (2907893)CaDiCaL version: 2.1.3
% 19.37/4.17 % (2907893)Termination reason: Instruction limit
% 19.37/4.17 % (2907893)Termination phase: Saturation
% 19.37/4.17 % (2907893)Time elapsed: 0.199 s
% 19.37/4.17 % (2907893)Peak memory usage: 110 MB
% 19.37/4.17 % (2907893)Instructions burned: 286 (million)
% 19.37/4.17 % (2907902)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3628001200:i=2350_2988 on theBenchmark for (2988ds/2350Mi)
% 19.37/4.17 % (2907895)Instruction limit reached!
% 19.37/4.17 % (2907895)------------------------------
% 19.37/4.17 % (2907895)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.37/4.17 % (2907895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.37/4.17 % (2907895)CaDiCaL version: 2.1.3
% 19.37/4.17 % (2907895)Termination reason: Instruction limit
% 19.37/4.17 % (2907895)Termination phase: Saturation
% 19.37/4.17 % (2907895)Time elapsed: 0.192 s
% 19.37/4.17 % (2907895)Peak memory usage: 108 MB
% 19.37/4.17 % (2907895)Instructions burned: 326 (million)
% 19.37/4.17 % (2907901)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=412943802:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2988 on theBenchmark for (2988ds/294Mi)
% 19.37/4.17 % (2907903)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=696369557:cts=off:i=113:fsr=off:ss=included:sgt=4_2987 on theBenchmark for (2987ds/113Mi)
% 19.37/4.17 % (2907906)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2931999541:i=127:av=off:fsr=off:sup=off_2987 on theBenchmark for (2987ds/127Mi)
% 19.37/4.17 % (2907903)Instruction limit reached!
% 19.37/4.17 % (2907903)------------------------------
% 19.37/4.17 % (2907903)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.37/4.17 % (2907903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.37/4.17 % (2907903)CaDiCaL version: 2.1.3
% 19.37/4.17 % (2907903)Termination reason: Instruction limit
% 19.37/4.17 % (2907903)Termination phase: Preprocessing 3
% 19.37/4.17 % (2907903)Time elapsed: 0.095 s
% 19.37/4.17 % (2907903)Peak memory usage: 105 MB
% 19.37/4.17 % (2907903)Instructions burned: 114 (million)
% 19.37/4.17 % (2907901)Instruction limit reached!
% 19.37/4.17 % (2907901)------------------------------
% 19.37/4.17 % (2907901)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.37/4.17 % (2907901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.37/4.17 % (2907901)CaDiCaL version: 2.1.3
% 19.37/4.17 % (2907901)Termination reason: Instruction limit
% 19.37/4.17 % (2907901)Termination phase: Saturation
% 19.37/4.17 % (2907901)Time elapsed: 0.193 s
% 19.37/4.17 % (2907901)Peak memory usage: 110 MB
% 19.37/4.17 % (2907901)Instructions burned: 295 (million)
% 19.37/4.17 % (2907906)Instruction limit reached!
% 19.37/4.17 % (2907906)------------------------------
% 19.37/4.17 % (2907906)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.37/4.17 % (2907906)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.66/7.20 % (2907906)CaDiCaL version: 2.1.3
% 40.66/7.20 % (2907906)Termination reason: Instruction limit
% 40.66/7.20 % (2907906)Termination phase: Preprocessing 2
% 40.66/7.20 % (2907906)Time elapsed: 0.104 s
% 40.66/7.20 % (2907906)Peak memory usage: 106 MB
% 40.66/7.20 % (2907906)Instructions burned: 127 (million)
% 40.66/7.20 % (2907910)lrs+10_1_sil=8000:sp=occurrence:random_seed=3850974622:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2985 on theBenchmark for (2985ds/907Mi)
% 40.66/7.20 % (2907909)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2867021118:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2985 on theBenchmark for (2985ds/114Mi)
% 40.66/7.20 % (2907909)Instruction limit reached!
% 40.66/7.20 % (2907909)------------------------------
% 40.66/7.20 % (2907909)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.66/7.20 % (2907909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.66/7.20 % (2907909)CaDiCaL version: 2.1.3
% 40.66/7.20 % (2907909)Termination reason: Instruction limit
% 40.66/7.20 % (2907909)Termination phase: Property scanning
% 40.66/7.20 % (2907909)Time elapsed: 0.050 s
% 40.66/7.20 % (2907909)Peak memory usage: 102 MB
% 40.66/7.20 % (2907909)Instructions burned: 115 (million)
% 40.66/7.20 % (2907911)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2731360088:i=437:sd=1:aac=none:ss=included_2984 on theBenchmark for (2984ds/437Mi)
% 40.66/7.20 % (2907914)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=490673786:i=5202:ss=axioms:sgt=16_2983 on theBenchmark for (2983ds/5202Mi)
% 40.66/7.20 % (2907911)Instruction limit reached!
% 40.66/7.20 % (2907911)------------------------------
% 40.66/7.20 % (2907911)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.66/7.20 % (2907911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.66/7.20 % (2907911)CaDiCaL version: 2.1.3
% 40.66/7.20 % (2907911)Termination reason: Instruction limit
% 40.66/7.20 % (2907911)Termination phase: Saturation
% 40.66/7.20 % (2907911)Time elapsed: 0.268 s
% 40.66/7.20 % (2907911)Peak memory usage: 110 MB
% 40.66/7.20 % (2907911)Instructions burned: 437 (million)
% 40.66/7.20 % (2907902)Instruction limit reached!
% 40.66/7.20 % (2907902)------------------------------
% 40.66/7.20 % (2907902)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.66/7.20 % (2907902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.66/7.20 % (2907902)CaDiCaL version: 2.1.3
% 40.66/7.20 % (2907902)Termination reason: Instruction limit
% 40.66/7.20 % (2907902)Termination phase: Saturation
% 40.66/7.20 % (2907902)Time elapsed: 0.819 s
% 40.66/7.20 % (2907902)Peak memory usage: 240 MB
% 40.66/7.20 % (2907902)Instructions burned: 2352 (million)
% 40.66/7.20 % (2907917)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3854668376:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2980 on theBenchmark for (2980ds/134Mi)
% 40.66/7.20 % (2907918)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=729123374:st=8:i=592:sd=3:ep=RST:ss=axioms_2979 on theBenchmark for (2979ds/592Mi)
% 40.66/7.20 % (2907917)Instruction limit reached!
% 40.66/7.20 % (2907917)------------------------------
% 40.66/7.20 % (2907917)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.66/7.20 % (2907917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.66/7.20 % (2907917)CaDiCaL version: 2.1.3
% 40.66/7.20 % (2907917)Termination reason: Instruction limit
% 40.66/7.20 % (2907917)Termination phase: Property scanning
% 40.66/7.20 % (2907917)Time elapsed: 0.102 s
% 40.66/7.20 % (2907917)Peak memory usage: 106 MB
% 40.66/7.20 % (2907917)Instructions burned: 136 (million)
% 40.66/7.20 % (2907910)Instruction limit reached!
% 40.66/7.20 % (2907910)------------------------------
% 40.66/7.20 % (2907910)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.66/7.20 % (2907910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.66/7.20 % (2907910)CaDiCaL version: 2.1.3
% 40.66/7.20 % (2907910)Termination reason: Instruction limit
% 40.66/7.20 % (2907910)Termination phase: Saturation
% 40.66/7.20 % (2907910)Time elapsed: 0.585 s
% 40.66/7.20 % (2907910)Peak memory usage: 121 MB
% 40.66/7.20 % (2907910)Instructions burned: 907 (million)
% 40.66/7.20 % (2907921)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1263330250:st=3:i=13193:sd=3:ss=axioms_2978 on theBenchmark for (2978ds/13193Mi)
% 40.66/7.20 % (2907922)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=1830149223:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2978 on theBenchmark for (2978ds/125Mi)
% 58.14/9.69 % (2907922)Instruction limit reached!
% 58.14/9.69 % (2907922)------------------------------
% 58.14/9.69 % (2907922)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.14/9.69 % (2907922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.14/9.69 % (2907922)CaDiCaL version: 2.1.3
% 58.14/9.69 % (2907922)Termination reason: Instruction limit
% 58.14/9.69 % (2907922)Termination phase: Property scanning
% 58.14/9.69 % (2907922)Time elapsed: 0.053 s
% 58.14/9.69 % (2907922)Peak memory usage: 102 MB
% 58.14/9.69 % (2907922)Instructions burned: 125 (million)
% 58.14/9.69 % (2907918)Instruction limit reached!
% 58.14/9.69 % (2907918)------------------------------
% 58.14/9.69 % (2907918)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.14/9.69 % (2907918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.14/9.69 % (2907918)CaDiCaL version: 2.1.3
% 58.14/9.69 % (2907918)Termination reason: Instruction limit
% 58.14/9.69 % (2907918)Termination phase: Property scanning
% 58.14/9.69 % (2907918)Time elapsed: 0.237 s
% 58.14/9.69 % (2907918)Peak memory usage: 123 MB
% 58.14/9.69 % (2907918)Instructions burned: 595 (million)
% 58.14/9.69 % (2907926)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3032293473:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2976 on theBenchmark for (2976ds/141Mi)
% 58.14/9.69 % (2907925)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2659313150:i=134:gtgl=5:slsql=off:gtg=exists_sym_2976 on theBenchmark for (2976ds/134Mi)
% 58.14/9.69 % (2907926)Refutation not found, incomplete strategy
% 58.14/9.69 % (2907926)------------------------------
% 58.14/9.69 % (2907926)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.14/9.69 % (2907926)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.14/9.69 % (2907926)CaDiCaL version: 2.1.3
% 58.14/9.69 % (2907926)Termination reason: Refutation not found, incomplete strategy
% 58.14/9.69 % (2907926)Time elapsed: 0.040 s
% 58.14/9.69 % (2907926)Peak memory usage: 107 MB
% 58.14/9.69 % (2907926)Instructions burned: 81 (million)
% 58.14/9.69 % (2907925)Instruction limit reached!
% 58.14/9.69 % (2907925)------------------------------
% 58.14/9.69 % (2907925)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.14/9.69 % (2907925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.14/9.69 % (2907925)CaDiCaL version: 2.1.3
% 58.14/9.69 % (2907925)Termination reason: Instruction limit
% 58.14/9.69 % (2907925)Termination phase: Property scanning
% 58.14/9.69 % (2907925)Time elapsed: 0.058 s
% 58.14/9.69 % (2907925)Peak memory usage: 102 MB
% 58.14/9.69 % (2907925)Instructions burned: 134 (million)
% 58.14/9.69 % (2907926)------------------------------
% 58.14/9.69 % (2907926)------------------------------
% 58.14/9.69 % (2907929)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=37261682:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2974 on theBenchmark for (2974ds/431Mi)
% 58.14/9.69 % (2907930)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=1507595123:i=6060:aac=none:ins=25_2973 on theBenchmark for (2973ds/6060Mi)
% 58.14/9.69 % (2907929)Refutation not found, incomplete strategy
% 58.14/9.69 % (2907929)------------------------------
% 58.14/9.69 % (2907929)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.14/9.69 % (2907929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.14/9.69 % (2907929)CaDiCaL version: 2.1.3
% 58.14/9.69 % (2907929)Termination reason: Refutation not found, incomplete strategy
% 58.14/9.69 % (2907929)Time elapsed: 0.075 s
% 58.14/9.69 % (2907929)Peak memory usage: 107 MB
% 58.14/9.69 % (2907929)Instructions burned: 88 (million)
% 58.14/9.69 % (2907929)------------------------------
% 58.14/9.69 % (2907929)------------------------------
% 58.14/9.69 % (2907933)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=4102543236:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2969 on theBenchmark for (2969ds/150Mi)
% 58.14/9.69 % (2907933)Instruction limit reached!
% 58.14/9.69 % (2907933)------------------------------
% 58.14/9.69 % (2907933)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.14/9.69 % (2907933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.14/9.69 % (2907933)CaDiCaL version: 2.1.3
% 58.14/9.69 % (2907933)Termination reason: Instruction limit
% 58.14/9.69 % (2907933)Termination phase: Preprocessing 1
% 58.14/9.69 % (2907933)Time elapsed: 0.117 s
% 58.14/9.69 % (2907933)Peak memory usage: 103 MB
% 58.14/9.69 % (2907933)Instructions burned: 150 (million)
% 58.14/9.69 % (2907935)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=910823966:i=14155:bd=all_2967 on theBenchmark for (2967ds/14155Mi)
% 58.14/9.69 % (2907930)Instruction limit reached!
% 58.14/9.69 % (2907930)------------------------------
% 58.14/9.69 % (2907930)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.14/9.69 % (2907930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.14/9.69 % (2907930)CaDiCaL version: 2.1.3
% 58.14/9.69 % (2907930)Termination reason: Instruction limit
% 58.14/9.69 % (2907930)Termination phase: Saturation
% 58.14/9.69 % (2907930)Time elapsed: 2.836 s
% 58.14/9.69 % (2907930)Peak memory usage: 531 MB
% 58.14/9.69 % (2907930)Instructions burned: 6061 (million)
% 58.14/9.69 % (2907914)Instruction limit reached!
% 58.14/9.69 % (2907914)------------------------------
% 58.14/9.69 % (2907914)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.14/9.69 % (2907914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.14/9.69 % (2907914)CaDiCaL version: 2.1.3
% 58.14/9.69 % (2907914)Termination reason: Instruction limit
% 58.14/9.69 % (2907914)Termination phase: Saturation
% 58.14/9.69 % (2907914)Time elapsed: 3.905 s
% 58.14/9.69 % (2907914)Peak memory usage: 436 MB
% 58.14/9.69 % (2907914)Instructions burned: 5202 (million)
% 58.14/9.69 % (2907937)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1826887216:i=667:av=off:fsr=off_2943 on theBenchmark for (2943ds/667Mi)
% 58.14/9.69 % (2907938)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=3154329420:s2a=on:i=185:s2at=1.8:fdi=4_2942 on theBenchmark for (2942ds/185Mi)
% 58.14/9.69 % (2907937)Instruction limit reached!
% 58.14/9.69 % (2907937)------------------------------
% 58.14/9.69 % (2907937)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.14/9.69 % (2907937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.14/9.69 % (2907937)CaDiCaL version: 2.1.3
% 58.14/9.69 % (2907937)Termination reason: Instruction limit
% 58.14/9.69 % (2907937)Termination phase: NewCNF
% 58.14/9.69 % (2907937)Time elapsed: 0.282 s
% 58.14/9.69 % (2907937)Peak memory usage: 135 MB
% 58.14/9.69 % (2907937)Instructions burned: 669 (million)
% 58.14/9.69 % (2907938)Instruction limit reached!
% 58.14/9.69 % (2907938)------------------------------
% 58.14/9.69 % (2907938)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.14/9.69 % (2907938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.14/9.69 % (2907938)CaDiCaL version: 2.1.3
% 58.14/9.69 % (2907938)Termination reason: Instruction limit
% 58.14/9.69 % (2907938)Termination phase: Preprocessing 1
% 58.14/9.69 % (2907938)Time elapsed: 0.147 s
% 58.14/9.69 % (2907938)Peak memory usage: 104 MB
% 58.14/9.69 % (2907938)Instructions burned: 186 (million)
% 58.14/9.69 % (2907941)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2214637223:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2939 on theBenchmark for (2939ds/193Mi)
% 58.14/9.69 % (2907942)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=705681548:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2939 on theBenchmark for (2939ds/4850Mi)
% 58.14/9.69 % (2907941)Instruction limit reached!
% 58.14/9.69 % (2907941)------------------------------
% 58.14/9.69 % (2907941)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.14/9.69 % (2907941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.14/9.69 % (2907941)CaDiCaL version: 2.1.3
% 58.14/9.69 % (2907941)Termination reason: Instruction limit
% 58.14/9.69 % (2907941)Termination phase: Equality resolution with deletion
% 58.14/9.69 % (2907941)Time elapsed: 0.086 s
% 58.14/9.69 % (2907941)Peak memory usage: 105 MB
% 58.14/9.69 % (2907941)Instructions burned: 195 (million)
% 58.14/9.69 % (2907945)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=3044608274:i=12111:sd=1:ss=included_2938 on theBenchmark for (2938ds/12111Mi)
% 58.14/9.69 % (2907945)First to succeed.
% 58.14/9.69 % (2907945)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2907874"
% 58.14/9.69 % (2907942)Instruction limit reached!
% 58.14/9.69 % (2907942)------------------------------
% 58.14/9.69 % (2907942)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.14/9.69 % (2907942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.14/9.69 % (2907942)CaDiCaL version: 2.1.3
% 58.14/9.69 % (2907942)Termination reason: Instruction limit
% 58.14/9.69 % (2907942)Termination phase: Saturation
% 58.14/9.69 % (2907942)Time elapsed: 2.593 s
% 58.14/9.69 % (2907942)Peak memory usage: 174 MB
% 58.14/9.69 % (2907942)Instructions burned: 4850 (million)
% 58.14/9.69 % (2907945)Refutation found. Thanks to Tanya!
% 58.14/9.69 % SZS status Theorem for theBenchmark
% 58.14/9.69 % SZS output start Proof for theBenchmark
% See solution above
% 58.85/9.89 % (2907945)------------------------------
% 58.85/9.89 % (2907945)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.85/9.89 % (2907945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.85/9.89 % (2907945)CaDiCaL version: 2.1.3
% 58.85/9.89 % (2907945)Termination reason: Refutation
% 58.85/9.89 % (2907945)Time elapsed: 2.254 s
% 58.85/9.89 % (2907945)Peak memory usage: 200 MB
% 58.85/9.89 % (2907945)Instructions burned: 5998 (million)
% 58.85/9.89 % (2907945)------------------------------
% 58.85/9.89 % (2907945)------------------------------
% 58.85/9.89 % (2907874)Success in time 8.812 s
% 58.85/9.89 % Vampire exiting
%------------------------------------------------------------------------------