%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT329+2 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:47:00 AM UTC 2026
% Result : Theorem 19.44s 3.78s
% Output : Refutation 20.58s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 26
% Syntax : Number of formulae : 235 ( 33 unt; 9 def)
% Number of atoms : 953 ( 32 equ)
% Maximal formula atoms : 13 ( 4 avg)
% Number of connectives : 1276 ( 558 ~; 591 |; 77 &)
% ( 20 <=>; 30 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 22 ( 20 usr; 6 prp; 0-3 aty)
% Number of functors : 13 ( 13 usr; 6 con; 0-3 aty)
% Number of variables : 255 ( 0 sgn 249 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f8,axiom,
! [X0,X1] :
( r1_tarski(X0,X1)
<=> ! [X2] :
( r2_hidden(X2,X0)
=> r2_hidden(X2,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d3_tarski) ).
fof(f38,axiom,
! [X0,X1] :
( X0 = X1
<=> ( r1_tarski(X0,X1)
& r1_tarski(X1,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d10_xboole_0) ).
fof(f584,axiom,
! [X0,X1,X2] :
( ( r2_hidden(X0,X1)
& m1_subset_1(X1,k1_zfmisc_1(X2)) )
=> m1_subset_1(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t4_subset) ).
fof(f2396,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v14_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> r3_lattices(X0,X1,k6_lattices(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t45_lattices) ).
fof(f2410,axiom,
! [X0] :
( l3_lattices(X0)
=> ( l1_lattices(X0)
& l2_lattices(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l3_lattices) ).
fof(f2426,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l2_lattices(X0) )
=> m1_subset_1(k6_lattices(X0),u1_struct_0(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k6_lattices) ).
fof(f2455,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> m1_filter_0(u1_struct_0(X0),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t15_filter_0) ).
fof(f2459,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ( r2_hidden(X1,k2_filter_0(X0,X2))
<=> r3_lattices(X0,X2,X1) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t18_filter_0) ).
fof(f2540,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_filter_0(X1,X0)
=> ( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m1_filter_0) ).
fof(f2857,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_lattice4(X1,X0)
=> m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m2_lattice4) ).
fof(f2872,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_filter_2(X1,X0)
<=> m1_filter_0(X1,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_m1_filter_2) ).
fof(f2877,axiom,
! [X0,X1,X2] :
( ( ~ v1_xboole_0(X0)
& m1_subset_1(X1,k1_zfmisc_1(X0))
& m1_subset_1(X2,k1_zfmisc_1(X0)) )
=> ( r1_filter_2(X0,X1,X2)
<=> X1 = X2 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_r1_filter_2) ).
fof(f2880,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& m1_subset_1(X1,u1_struct_0(X0)) )
=> m1_filter_2(k2_filter_2(X0,X1),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k2_filter_2) ).
fof(f2881,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& m1_subset_1(X1,u1_struct_0(X0)) )
=> k2_filter_2(X0,X1) = k2_filter_0(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k2_filter_2) ).
fof(f2912,axiom,
! [X0,X1,X2] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& m1_subset_1(X1,u1_struct_0(X0))
& m1_subset_1(X2,u1_struct_0(X0)) )
=> ( ~ v1_xboole_0(k22_filter_2(X0,X1,X2))
& m2_lattice4(k22_filter_2(X0,X1,X2),X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k22_filter_2) ).
fof(f2999,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
=> ( r3_lattices(X0,X1,X2)
=> ( r2_hidden(X3,k22_filter_2(X0,X1,X2))
<=> ( r3_lattices(X0,X1,X3)
& r3_lattices(X0,X3,X2) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t63_filter_2) ).
fof(f3002,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ( v14_lattices(X0)
=> r1_filter_2(u1_struct_0(X0),k2_filter_2(X0,X1),k22_filter_2(X0,X1,k6_lattices(X0))) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t66_filter_2) ).
fof(f3003,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)],[f3002]) ).
fof(f3095,plain,
! [X0,X1] :
( r1_tarski(X0,X1)
<=> ! [X2] :
( r2_hidden(X2,X1)
| ~ r2_hidden(X2,X0) ) ),
inference(ennf_transformation,[],[f8]) ).
fof(f3432,plain,
! [X0,X1,X2] :
( m1_subset_1(X0,X2)
| ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2)) ),
inference(ennf_transformation,[],[f584]) ).
fof(f3433,plain,
! [X0,X1,X2] :
( m1_subset_1(X0,X2)
| ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2)) ),
inference(flattening,[],[f3432]) ).
fof(f5398,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,[],[f2396]) ).
fof(f5399,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,[],[f5398]) ).
fof(f5418,plain,
! [X0] :
( ( l1_lattices(X0)
& l2_lattices(X0) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2410]) ).
fof(f5447,plain,
! [X0] :
( m1_subset_1(k6_lattices(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l2_lattices(X0) ),
inference(ennf_transformation,[],[f2426]) ).
fof(f5448,plain,
! [X0] :
( m1_subset_1(k6_lattices(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l2_lattices(X0) ),
inference(flattening,[],[f5447]) ).
fof(f5499,plain,
! [X0] :
( m1_filter_0(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2455]) ).
fof(f5500,plain,
! [X0] :
( m1_filter_0(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f5499]) ).
fof(f5503,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,[],[f2459]) ).
fof(f5504,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,[],[f5503]) ).
fof(f5643,plain,
! [X0] :
( ! [X1] :
( ( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2540]) ).
fof(f5644,plain,
! [X0] :
( ! [X1] :
( ( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f5643]) ).
fof(f6057,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,[],[f2857]) ).
fof(f6058,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,[],[f6057]) ).
fof(f6087,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,[],[f2872]) ).
fof(f6088,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,[],[f6087]) ).
fof(f6097,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,[],[f2877]) ).
fof(f6098,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,[],[f6097]) ).
fof(f6103,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,[],[f2880]) ).
fof(f6104,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,[],[f6103]) ).
fof(f6105,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,[],[f2881]) ).
fof(f6106,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,[],[f6105]) ).
fof(f6167,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,[],[f2912]) ).
fof(f6168,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,[],[f6167]) ).
fof(f6338,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,[],[f2999]) ).
fof(f6339,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,[],[f6338]) ).
fof(f6344,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,[],[f3003]) ).
fof(f6345,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,[],[f6344]) ).
fof(f6557,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,[],[f3095]) ).
fof(f6558,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,[],[f6557]) ).
fof(f6559,plain,
! [X0,X1] :
( ( r1_tarski(X0,X1)
| ( ~ r2_hidden(sK130(X0,X1),X1)
& r2_hidden(sK130(X0,X1),X0) ) )
& ( ! [X3] :
( r2_hidden(X3,X1)
| ~ r2_hidden(X3,X0) )
| ~ r1_tarski(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK130]),skolemize(X2,sK130(X0,X1))],[f6558]) ).
fof(f6595,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(f6596,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,[],[f6595]) ).
fof(f7873,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,[],[f5504]) ).
fof(f8050,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,[],[f6088]) ).
fof(f8052,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,[],[f6098]) ).
fof(f8112,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,[],[f6339]) ).
fof(f8113,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,[],[f8112]) ).
fof(f8114,plain,
( ~ r1_filter_2(u1_struct_0(sK1079),k2_filter_2(sK1079,sK1080),k22_filter_2(sK1079,sK1080,k6_lattices(sK1079)))
& v14_lattices(sK1079)
& m1_subset_1(sK1080,u1_struct_0(sK1079))
& ~ v3_struct_0(sK1079)
& v10_lattices(sK1079)
& l3_lattices(sK1079) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1079,sK1080]),skolemize(X0,sK1079),skolemize(X1,sK1080)],[f6345]) ).
fof(f8129,plain,
! [X0,X1] :
( r2_hidden(sK130(X0,X1),X0)
| r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f6559]) ).
fof(f8130,plain,
! [X0,X1] :
( ~ r2_hidden(sK130(X0,X1),X1)
| r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f6559]) ).
fof(f8197,plain,
! [X0,X1] :
( ~ r1_tarski(X1,X0)
| ~ r1_tarski(X0,X1)
| X0 = X1 ),
inference(cnf_transformation,[],[f6596]) ).
fof(f8903,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ r2_hidden(X0,X1)
| m1_subset_1(X0,X2) ),
inference(cnf_transformation,[],[f3433]) ).
fof(f12467,plain,
! [X0,X1] :
( r3_lattices(X0,X1,k6_lattices(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v14_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f5399]) ).
fof(f12482,plain,
! [X0] :
( ~ l3_lattices(X0)
| l2_lattices(X0) ),
inference(cnf_transformation,[],[f5418]) ).
fof(f12500,plain,
! [X0] :
( m1_subset_1(k6_lattices(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l2_lattices(X0) ),
inference(cnf_transformation,[],[f5448]) ).
fof(f12596,plain,
! [X0] :
( m1_filter_0(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f5500]) ).
fof(f12598,plain,
! [X2,X0,X1] :
( ~ r2_hidden(X1,k2_filter_0(X0,X2))
| r3_lattices(X0,X2,X1)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f7873]) ).
fof(f12599,plain,
! [X2,X0,X1] :
( r2_hidden(X1,k2_filter_0(X0,X2))
| ~ r3_lattices(X0,X2,X1)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f7873]) ).
fof(f12761,plain,
! [X0,X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m1_filter_0(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f5644]) ).
fof(f12762,plain,
! [X0,X1] :
( ~ m1_filter_0(X1,X0)
| ~ v1_xboole_0(X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f5644]) ).
fof(f13340,plain,
! [X0,X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f6058]) ).
fof(f13367,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,[],[f8050]) ).
fof(f13375,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,[],[f8052]) ).
fof(f13378,plain,
! [X0,X1] :
( m1_filter_2(k2_filter_2(X0,X1),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f6104]) ).
fof(f13379,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| k2_filter_0(X0,X1) = k2_filter_2(X0,X1) ),
inference(cnf_transformation,[],[f6106]) ).
fof(f13412,plain,
! [X2,X0,X1] :
( m2_lattice4(k22_filter_2(X0,X1,X2),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f6168]) ).
fof(f13655,plain,
! [X2,X3,X0,X1] :
( ~ r2_hidden(X3,k22_filter_2(X0,X1,X2))
| r3_lattices(X0,X1,X3)
| ~ r3_lattices(X0,X1,X2)
| ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f8113]) ).
fof(f13656,plain,
! [X2,X3,X0,X1] :
( r2_hidden(X3,k22_filter_2(X0,X1,X2))
| ~ r3_lattices(X0,X1,X3)
| ~ r3_lattices(X0,X3,X2)
| ~ r3_lattices(X0,X1,X2)
| ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f8113]) ).
fof(f13660,plain,
l3_lattices(sK1079),
inference(cnf_transformation,[],[f8114]) ).
fof(f13661,plain,
v10_lattices(sK1079),
inference(cnf_transformation,[],[f8114]) ).
fof(f13662,plain,
~ v3_struct_0(sK1079),
inference(cnf_transformation,[],[f8114]) ).
fof(f13663,plain,
m1_subset_1(sK1080,u1_struct_0(sK1079)),
inference(cnf_transformation,[],[f8114]) ).
fof(f13664,plain,
v14_lattices(sK1079),
inference(cnf_transformation,[],[f8114]) ).
fof(f13665,plain,
~ r1_filter_2(u1_struct_0(sK1079),k2_filter_2(sK1079,sK1080),k22_filter_2(sK1079,sK1080,k6_lattices(sK1079))),
inference(cnf_transformation,[],[f8114]) ).
fof(f15554,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,[],[f13375]) ).
fof(f15604,definition,
sF1081 = u1_struct_0(sK1079),
introduced(definition,[new_symbols(definition,[sF1081])],[function_definition]) ).
fof(f15605,plain,
u1_struct_0(sK1079) = sF1081,
inference(reorient_equations,[],[f15604]) ).
fof(f15606,definition,
sF1082 = k2_filter_2(sK1079,sK1080),
introduced(definition,[new_symbols(definition,[sF1082])],[function_definition]) ).
fof(f15607,plain,
k2_filter_2(sK1079,sK1080) = sF1082,
inference(reorient_equations,[],[f15606]) ).
fof(f15608,definition,
sF1083 = k6_lattices(sK1079),
introduced(definition,[new_symbols(definition,[sF1083])],[function_definition]) ).
fof(f15609,plain,
k6_lattices(sK1079) = sF1083,
inference(reorient_equations,[],[f15608]) ).
fof(f15610,definition,
sF1084 = k22_filter_2(sK1079,sK1080,sF1083),
introduced(definition,[new_symbols(definition,[sF1084])],[function_definition]) ).
fof(f15611,plain,
k22_filter_2(sK1079,sK1080,sF1083) = sF1084,
inference(reorient_equations,[],[f15610]) ).
fof(f15612,plain,
~ r1_filter_2(sF1081,sF1082,sF1084),
inference(definition_folding,[],[f13665,f15611,f15609,f15607,f15605]) ).
fof(f15613,plain,
m1_subset_1(sK1080,sF1081),
inference(definition_folding,[],[f13663,f15605]) ).
fof(f15621,plain,
! [X2,X0] :
( ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| v1_xboole_0(X0)
| r1_filter_2(X0,X2,X2) ),
inference(duplicate_literal_removal,[],[f15554]) ).
fof(f18156,plain,
! [X0] :
( ~ m1_subset_1(X0,sF1081)
| v3_struct_0(sK1079)
| ~ v10_lattices(sK1079)
| ~ l3_lattices(sK1079)
| k2_filter_0(sK1079,X0) = k2_filter_2(sK1079,X0) ),
inference(superposition,[],[f13379,f15605]) ).
fof(f18157,plain,
! [X0] :
( ~ m1_subset_1(X0,sF1081)
| ~ v10_lattices(sK1079)
| ~ l3_lattices(sK1079)
| k2_filter_0(sK1079,X0) = k2_filter_2(sK1079,X0) ),
inference(forward_subsumption_resolution,[],[f18156,f13662]) ).
fof(f18158,plain,
! [X0] :
( ~ m1_subset_1(X0,sF1081)
| ~ l3_lattices(sK1079)
| k2_filter_0(sK1079,X0) = k2_filter_2(sK1079,X0) ),
inference(forward_subsumption_resolution,[],[f18157,f13661]) ).
fof(f18159,plain,
! [X0] :
( ~ m1_subset_1(X0,sF1081)
| k2_filter_0(sK1079,X0) = k2_filter_2(sK1079,X0) ),
inference(forward_subsumption_resolution,[],[f18158,f13660]) ).
fof(f18164,plain,
( m1_filter_2(sF1082,sK1079)
| v3_struct_0(sK1079)
| ~ v10_lattices(sK1079)
| ~ l3_lattices(sK1079)
| ~ m1_subset_1(sK1080,u1_struct_0(sK1079)) ),
inference(superposition,[],[f13378,f15607]) ).
fof(f18165,plain,
( m1_filter_2(sF1082,sK1079)
| ~ v10_lattices(sK1079)
| ~ l3_lattices(sK1079)
| ~ m1_subset_1(sK1080,u1_struct_0(sK1079)) ),
inference(forward_subsumption_resolution,[],[f18164,f13662]) ).
fof(f18166,plain,
( m1_filter_2(sF1082,sK1079)
| ~ l3_lattices(sK1079)
| ~ m1_subset_1(sK1080,u1_struct_0(sK1079)) ),
inference(forward_subsumption_resolution,[],[f18165,f13661]) ).
fof(f18167,plain,
( m1_filter_2(sF1082,sK1079)
| ~ m1_subset_1(sK1080,u1_struct_0(sK1079)) ),
inference(forward_subsumption_resolution,[],[f18166,f13660]) ).
fof(f18168,plain,
( ~ m1_subset_1(sK1080,sF1081)
| m1_filter_2(sF1082,sK1079) ),
inference(forward_demodulation,[],[f18167,f15605]) ).
fof(f18169,plain,
m1_filter_2(sF1082,sK1079),
inference(forward_subsumption_resolution,[],[f18168,f15613]) ).
fof(f18179,plain,
k2_filter_2(sK1079,sK1080) = k2_filter_0(sK1079,sK1080),
inference(resolution,[],[f18159,f15613]) ).
fof(f18180,plain,
sF1082 = k2_filter_0(sK1079,sK1080),
inference(forward_demodulation,[],[f18179,f15607]) ).
fof(f18221,plain,
( m1_filter_0(sF1082,sK1079)
| v3_struct_0(sK1079)
| ~ v10_lattices(sK1079)
| ~ l3_lattices(sK1079) ),
inference(resolution,[],[f13367,f18169]) ).
fof(f18223,plain,
( m1_filter_0(sF1082,sK1079)
| ~ v10_lattices(sK1079)
| ~ l3_lattices(sK1079) ),
inference(forward_subsumption_resolution,[],[f18221,f13662]) ).
fof(f18224,plain,
( m1_filter_0(sF1082,sK1079)
| ~ l3_lattices(sK1079) ),
inference(forward_subsumption_resolution,[],[f18223,f13661]) ).
fof(f18225,plain,
m1_filter_0(sF1082,sK1079),
inference(forward_subsumption_resolution,[],[f18224,f13660]) ).
fof(f18234,plain,
! [X0] :
( m1_subset_1(X0,k1_zfmisc_1(sF1081))
| ~ m2_lattice4(X0,sK1079)
| v3_struct_0(sK1079)
| ~ v10_lattices(sK1079)
| ~ l3_lattices(sK1079) ),
inference(superposition,[],[f13340,f15605]) ).
fof(f18236,plain,
! [X0] :
( m1_subset_1(X0,k1_zfmisc_1(sF1081))
| ~ m2_lattice4(X0,sK1079)
| ~ v10_lattices(sK1079)
| ~ l3_lattices(sK1079) ),
inference(forward_subsumption_resolution,[],[f18234,f13662]) ).
fof(f18237,plain,
! [X0] :
( m1_subset_1(X0,k1_zfmisc_1(sF1081))
| ~ m2_lattice4(X0,sK1079)
| ~ l3_lattices(sK1079) ),
inference(forward_subsumption_resolution,[],[f18236,f13661]) ).
fof(f18238,plain,
! [X0] :
( m1_subset_1(X0,k1_zfmisc_1(sF1081))
| ~ m2_lattice4(X0,sK1079) ),
inference(forward_subsumption_resolution,[],[f18237,f13660]) ).
fof(f18240,plain,
( m1_filter_0(sF1081,sK1079)
| v3_struct_0(sK1079)
| ~ v10_lattices(sK1079)
| ~ l3_lattices(sK1079) ),
inference(superposition,[],[f12596,f15605]) ).
fof(f18242,plain,
( m1_filter_0(sF1081,sK1079)
| ~ v10_lattices(sK1079)
| ~ l3_lattices(sK1079) ),
inference(forward_subsumption_resolution,[],[f18240,f13662]) ).
fof(f18243,plain,
( m1_filter_0(sF1081,sK1079)
| ~ l3_lattices(sK1079) ),
inference(forward_subsumption_resolution,[],[f18242,f13661]) ).
fof(f18244,plain,
m1_filter_0(sF1081,sK1079),
inference(forward_subsumption_resolution,[],[f18243,f13660]) ).
fof(f18245,plain,
! [X0] :
( r3_lattices(sK1079,X0,sF1083)
| ~ m1_subset_1(X0,u1_struct_0(sK1079))
| v3_struct_0(sK1079)
| ~ v10_lattices(sK1079)
| ~ v14_lattices(sK1079)
| ~ l3_lattices(sK1079) ),
inference(superposition,[],[f12467,f15609]) ).
fof(f18246,plain,
! [X0] :
( r3_lattices(sK1079,X0,sF1083)
| ~ m1_subset_1(X0,u1_struct_0(sK1079))
| ~ v10_lattices(sK1079)
| ~ v14_lattices(sK1079)
| ~ l3_lattices(sK1079) ),
inference(forward_subsumption_resolution,[],[f18245,f13662]) ).
fof(f18247,plain,
! [X0] :
( r3_lattices(sK1079,X0,sF1083)
| ~ m1_subset_1(X0,u1_struct_0(sK1079))
| ~ v14_lattices(sK1079)
| ~ l3_lattices(sK1079) ),
inference(forward_subsumption_resolution,[],[f18246,f13661]) ).
fof(f18248,plain,
! [X0] :
( r3_lattices(sK1079,X0,sF1083)
| ~ m1_subset_1(X0,u1_struct_0(sK1079))
| ~ l3_lattices(sK1079) ),
inference(forward_subsumption_resolution,[],[f18247,f13664]) ).
fof(f18249,plain,
! [X0] :
( r3_lattices(sK1079,X0,sF1083)
| ~ m1_subset_1(X0,u1_struct_0(sK1079)) ),
inference(forward_subsumption_resolution,[],[f18248,f13660]) ).
fof(f18250,plain,
! [X0] :
( r3_lattices(sK1079,X0,sF1083)
| ~ m1_subset_1(X0,sF1081) ),
inference(forward_demodulation,[],[f18249,f15605]) ).
fof(f18300,definition,
( spl1085_350
<=> r1_tarski(sF1082,sF1084) ),
introduced(definition,[new_symbols(definition,[spl1085_350])],[avatar_definition]) ).
fof(f18301,plain,
( r1_tarski(sF1082,sF1084)
| ~ spl1085_350 ),
inference(avatar_component_clause,[],[f18300]) ).
fof(f18308,plain,
( m2_lattice4(sF1084,sK1079)
| v3_struct_0(sK1079)
| ~ v10_lattices(sK1079)
| ~ l3_lattices(sK1079)
| ~ m1_subset_1(sK1080,u1_struct_0(sK1079))
| ~ m1_subset_1(sF1083,u1_struct_0(sK1079)) ),
inference(superposition,[],[f13412,f15611]) ).
fof(f18309,plain,
( m2_lattice4(sF1084,sK1079)
| ~ v10_lattices(sK1079)
| ~ l3_lattices(sK1079)
| ~ m1_subset_1(sK1080,u1_struct_0(sK1079))
| ~ m1_subset_1(sF1083,u1_struct_0(sK1079)) ),
inference(forward_subsumption_resolution,[],[f18308,f13662]) ).
fof(f18310,plain,
( m2_lattice4(sF1084,sK1079)
| ~ l3_lattices(sK1079)
| ~ m1_subset_1(sK1080,u1_struct_0(sK1079))
| ~ m1_subset_1(sF1083,u1_struct_0(sK1079)) ),
inference(forward_subsumption_resolution,[],[f18309,f13661]) ).
fof(f18311,plain,
( m2_lattice4(sF1084,sK1079)
| ~ m1_subset_1(sK1080,u1_struct_0(sK1079))
| ~ m1_subset_1(sF1083,u1_struct_0(sK1079)) ),
inference(forward_subsumption_resolution,[],[f18310,f13660]) ).
fof(f18312,plain,
( ~ m1_subset_1(sK1080,sF1081)
| m2_lattice4(sF1084,sK1079)
| ~ m1_subset_1(sF1083,u1_struct_0(sK1079)) ),
inference(forward_demodulation,[],[f18311,f15605]) ).
fof(f18313,plain,
( m2_lattice4(sF1084,sK1079)
| ~ m1_subset_1(sF1083,u1_struct_0(sK1079)) ),
inference(forward_subsumption_resolution,[],[f18312,f15613]) ).
fof(f18314,plain,
( ~ m1_subset_1(sF1083,sF1081)
| m2_lattice4(sF1084,sK1079) ),
inference(forward_demodulation,[],[f18313,f15605]) ).
fof(f18316,definition,
( spl1085_352
<=> m2_lattice4(sF1084,sK1079) ),
introduced(definition,[new_symbols(definition,[spl1085_352])],[avatar_definition]) ).
fof(f18318,plain,
( m2_lattice4(sF1084,sK1079)
| ~ spl1085_352 ),
inference(avatar_component_clause,[],[f18316]) ).
fof(f18320,definition,
( spl1085_353
<=> m1_subset_1(sF1083,sF1081) ),
introduced(definition,[new_symbols(definition,[spl1085_353])],[avatar_definition]) ).
fof(f18321,plain,
( m1_subset_1(sF1083,sF1081)
| ~ spl1085_353 ),
inference(avatar_component_clause,[],[f18320]) ).
fof(f18322,plain,
( ~ m1_subset_1(sF1083,sF1081)
| spl1085_353 ),
inference(avatar_component_clause,[],[f18320]) ).
fof(f18323,plain,
( spl1085_352
| ~ spl1085_353 ),
inference(avatar_split_clause,[],[f18314,f18320,f18316]) ).
fof(f18347,plain,
! [X0] :
( m1_subset_1(X0,k1_zfmisc_1(sF1081))
| ~ m1_filter_0(X0,sK1079)
| v3_struct_0(sK1079)
| ~ v10_lattices(sK1079)
| ~ l3_lattices(sK1079) ),
inference(superposition,[],[f12761,f15605]) ).
fof(f18349,plain,
! [X0] :
( m1_subset_1(X0,k1_zfmisc_1(sF1081))
| ~ m1_filter_0(X0,sK1079)
| ~ v10_lattices(sK1079)
| ~ l3_lattices(sK1079) ),
inference(forward_subsumption_resolution,[],[f18347,f13662]) ).
fof(f18350,plain,
! [X0] :
( m1_subset_1(X0,k1_zfmisc_1(sF1081))
| ~ m1_filter_0(X0,sK1079)
| ~ l3_lattices(sK1079) ),
inference(forward_subsumption_resolution,[],[f18349,f13661]) ).
fof(f18351,plain,
! [X0] :
( m1_subset_1(X0,k1_zfmisc_1(sF1081))
| ~ m1_filter_0(X0,sK1079) ),
inference(forward_subsumption_resolution,[],[f18350,f13660]) ).
fof(f18403,plain,
( m1_subset_1(k6_lattices(sK1079),sF1081)
| v3_struct_0(sK1079)
| ~ l2_lattices(sK1079) ),
inference(superposition,[],[f12500,f15605]) ).
fof(f18410,plain,
( m1_subset_1(k6_lattices(sK1079),sF1081)
| ~ l2_lattices(sK1079) ),
inference(forward_subsumption_resolution,[],[f18403,f13662]) ).
fof(f18425,plain,
( m1_subset_1(sF1083,sF1081)
| ~ l2_lattices(sK1079) ),
inference(forward_demodulation,[],[f18410,f15609]) ).
fof(f18427,plain,
( ~ l2_lattices(sK1079)
| spl1085_353 ),
inference(forward_subsumption_resolution,[],[f18425,f18322]) ).
fof(f18443,plain,
! [X0] :
( r2_hidden(X0,sF1084)
| ~ r3_lattices(sK1079,sK1080,X0)
| ~ r3_lattices(sK1079,X0,sF1083)
| ~ r3_lattices(sK1079,sK1080,sF1083)
| ~ m1_subset_1(X0,u1_struct_0(sK1079))
| ~ m1_subset_1(sF1083,u1_struct_0(sK1079))
| ~ m1_subset_1(sK1080,u1_struct_0(sK1079))
| v3_struct_0(sK1079)
| ~ v10_lattices(sK1079)
| ~ l3_lattices(sK1079) ),
inference(superposition,[],[f13656,f15611]) ).
fof(f18444,plain,
! [X0] :
( r2_hidden(X0,sF1084)
| ~ r3_lattices(sK1079,sK1080,X0)
| ~ r3_lattices(sK1079,X0,sF1083)
| ~ r3_lattices(sK1079,sK1080,sF1083)
| ~ m1_subset_1(X0,u1_struct_0(sK1079))
| ~ m1_subset_1(sF1083,u1_struct_0(sK1079))
| ~ m1_subset_1(sK1080,u1_struct_0(sK1079))
| ~ v10_lattices(sK1079)
| ~ l3_lattices(sK1079) ),
inference(forward_subsumption_resolution,[],[f18443,f13662]) ).
fof(f18445,plain,
! [X0] :
( r2_hidden(X0,sF1084)
| ~ r3_lattices(sK1079,sK1080,X0)
| ~ r3_lattices(sK1079,X0,sF1083)
| ~ r3_lattices(sK1079,sK1080,sF1083)
| ~ m1_subset_1(X0,u1_struct_0(sK1079))
| ~ m1_subset_1(sF1083,u1_struct_0(sK1079))
| ~ m1_subset_1(sK1080,u1_struct_0(sK1079))
| ~ l3_lattices(sK1079) ),
inference(forward_subsumption_resolution,[],[f18444,f13661]) ).
fof(f18446,plain,
! [X0] :
( r2_hidden(X0,sF1084)
| ~ r3_lattices(sK1079,sK1080,X0)
| ~ r3_lattices(sK1079,X0,sF1083)
| ~ r3_lattices(sK1079,sK1080,sF1083)
| ~ m1_subset_1(X0,u1_struct_0(sK1079))
| ~ m1_subset_1(sF1083,u1_struct_0(sK1079))
| ~ m1_subset_1(sK1080,u1_struct_0(sK1079)) ),
inference(forward_subsumption_resolution,[],[f18445,f13660]) ).
fof(f18447,plain,
! [X0] :
( ~ m1_subset_1(X0,sF1081)
| r2_hidden(X0,sF1084)
| ~ r3_lattices(sK1079,sK1080,X0)
| ~ r3_lattices(sK1079,X0,sF1083)
| ~ r3_lattices(sK1079,sK1080,sF1083)
| ~ m1_subset_1(sF1083,u1_struct_0(sK1079))
| ~ m1_subset_1(sK1080,u1_struct_0(sK1079)) ),
inference(forward_demodulation,[],[f18446,f15605]) ).
fof(f18448,plain,
! [X0] :
( ~ m1_subset_1(X0,sF1081)
| r2_hidden(X0,sF1084)
| ~ r3_lattices(sK1079,sK1080,X0)
| ~ r3_lattices(sK1079,sK1080,sF1083)
| ~ m1_subset_1(sF1083,u1_struct_0(sK1079))
| ~ m1_subset_1(sK1080,u1_struct_0(sK1079)) ),
inference(forward_subsumption_resolution,[],[f18447,f18250]) ).
fof(f18449,plain,
! [X0] :
( ~ m1_subset_1(sF1083,sF1081)
| ~ m1_subset_1(X0,sF1081)
| r2_hidden(X0,sF1084)
| ~ r3_lattices(sK1079,sK1080,X0)
| ~ r3_lattices(sK1079,sK1080,sF1083)
| ~ m1_subset_1(sK1080,u1_struct_0(sK1079)) ),
inference(forward_demodulation,[],[f18448,f15605]) ).
fof(f18466,plain,
! [X0] :
( ~ r2_hidden(X0,sF1084)
| r3_lattices(sK1079,sK1080,X0)
| ~ r3_lattices(sK1079,sK1080,sF1083)
| ~ m1_subset_1(X0,u1_struct_0(sK1079))
| ~ m1_subset_1(sF1083,u1_struct_0(sK1079))
| ~ m1_subset_1(sK1080,u1_struct_0(sK1079))
| v3_struct_0(sK1079)
| ~ v10_lattices(sK1079)
| ~ l3_lattices(sK1079) ),
inference(superposition,[],[f13655,f15611]) ).
fof(f18470,plain,
! [X0] :
( ~ r2_hidden(X0,sF1084)
| r3_lattices(sK1079,sK1080,X0)
| ~ r3_lattices(sK1079,sK1080,sF1083)
| ~ m1_subset_1(X0,u1_struct_0(sK1079))
| ~ m1_subset_1(sF1083,u1_struct_0(sK1079))
| ~ m1_subset_1(sK1080,u1_struct_0(sK1079))
| ~ v10_lattices(sK1079)
| ~ l3_lattices(sK1079) ),
inference(forward_subsumption_resolution,[],[f18466,f13662]) ).
fof(f18471,plain,
! [X0] :
( ~ r2_hidden(X0,sF1084)
| r3_lattices(sK1079,sK1080,X0)
| ~ r3_lattices(sK1079,sK1080,sF1083)
| ~ m1_subset_1(X0,u1_struct_0(sK1079))
| ~ m1_subset_1(sF1083,u1_struct_0(sK1079))
| ~ m1_subset_1(sK1080,u1_struct_0(sK1079))
| ~ l3_lattices(sK1079) ),
inference(forward_subsumption_resolution,[],[f18470,f13661]) ).
fof(f18472,plain,
! [X0] :
( ~ r2_hidden(X0,sF1084)
| r3_lattices(sK1079,sK1080,X0)
| ~ r3_lattices(sK1079,sK1080,sF1083)
| ~ m1_subset_1(X0,u1_struct_0(sK1079))
| ~ m1_subset_1(sF1083,u1_struct_0(sK1079))
| ~ m1_subset_1(sK1080,u1_struct_0(sK1079)) ),
inference(forward_subsumption_resolution,[],[f18471,f13660]) ).
fof(f18473,plain,
! [X0] :
( ~ m1_subset_1(X0,sF1081)
| ~ r2_hidden(X0,sF1084)
| r3_lattices(sK1079,sK1080,X0)
| ~ r3_lattices(sK1079,sK1080,sF1083)
| ~ m1_subset_1(sF1083,u1_struct_0(sK1079))
| ~ m1_subset_1(sK1080,u1_struct_0(sK1079)) ),
inference(forward_demodulation,[],[f18472,f15605]) ).
fof(f18474,plain,
! [X0] :
( ~ m1_subset_1(sF1083,sF1081)
| ~ m1_subset_1(X0,sF1081)
| ~ r2_hidden(X0,sF1084)
| r3_lattices(sK1079,sK1080,X0)
| ~ r3_lattices(sK1079,sK1080,sF1083)
| ~ m1_subset_1(sK1080,u1_struct_0(sK1079)) ),
inference(forward_demodulation,[],[f18473,f15605]) ).
fof(f18495,plain,
! [X0] :
( ~ r2_hidden(X0,sF1082)
| r3_lattices(sK1079,sK1080,X0)
| ~ m1_subset_1(sK1080,u1_struct_0(sK1079))
| ~ m1_subset_1(X0,u1_struct_0(sK1079))
| v3_struct_0(sK1079)
| ~ v10_lattices(sK1079)
| ~ l3_lattices(sK1079) ),
inference(superposition,[],[f12598,f18180]) ).
fof(f18496,plain,
! [X0] :
( ~ r2_hidden(X0,sF1082)
| r3_lattices(sK1079,sK1080,X0)
| ~ m1_subset_1(sK1080,u1_struct_0(sK1079))
| ~ m1_subset_1(X0,u1_struct_0(sK1079))
| ~ v10_lattices(sK1079)
| ~ l3_lattices(sK1079) ),
inference(forward_subsumption_resolution,[],[f18495,f13662]) ).
fof(f18497,plain,
! [X0] :
( ~ r2_hidden(X0,sF1082)
| r3_lattices(sK1079,sK1080,X0)
| ~ m1_subset_1(sK1080,u1_struct_0(sK1079))
| ~ m1_subset_1(X0,u1_struct_0(sK1079))
| ~ l3_lattices(sK1079) ),
inference(forward_subsumption_resolution,[],[f18496,f13661]) ).
fof(f18498,plain,
! [X0] :
( ~ r2_hidden(X0,sF1082)
| r3_lattices(sK1079,sK1080,X0)
| ~ m1_subset_1(sK1080,u1_struct_0(sK1079))
| ~ m1_subset_1(X0,u1_struct_0(sK1079)) ),
inference(forward_subsumption_resolution,[],[f18497,f13660]) ).
fof(f18499,plain,
! [X0] :
( ~ m1_subset_1(sK1080,sF1081)
| ~ r2_hidden(X0,sF1082)
| r3_lattices(sK1079,sK1080,X0)
| ~ m1_subset_1(X0,u1_struct_0(sK1079)) ),
inference(forward_demodulation,[],[f18498,f15605]) ).
fof(f18500,plain,
! [X0] :
( ~ r2_hidden(X0,sF1082)
| r3_lattices(sK1079,sK1080,X0)
| ~ m1_subset_1(X0,u1_struct_0(sK1079)) ),
inference(forward_subsumption_resolution,[],[f18499,f15613]) ).
fof(f18501,plain,
! [X0] :
( r3_lattices(sK1079,sK1080,X0)
| ~ r2_hidden(X0,sF1082)
| ~ m1_subset_1(X0,sF1081) ),
inference(forward_demodulation,[],[f18500,f15605]) ).
fof(f18504,plain,
( ~ v1_xboole_0(sF1081)
| v3_struct_0(sK1079)
| ~ v10_lattices(sK1079)
| ~ l3_lattices(sK1079) ),
inference(resolution,[],[f12762,f18244]) ).
fof(f18521,definition,
( spl1085_357
<=> v1_xboole_0(sF1081) ),
introduced(definition,[new_symbols(definition,[spl1085_357])],[avatar_definition]) ).
fof(f18522,plain,
( ~ v1_xboole_0(sF1081)
| spl1085_357 ),
inference(avatar_component_clause,[],[f18521]) ).
fof(f18554,plain,
( ~ v1_xboole_0(sF1081)
| ~ v10_lattices(sK1079)
| ~ l3_lattices(sK1079) ),
inference(forward_subsumption_resolution,[],[f18504,f13662]) ).
fof(f18575,plain,
( ~ v1_xboole_0(sF1081)
| ~ l3_lattices(sK1079) ),
inference(forward_subsumption_resolution,[],[f18554,f13661]) ).
fof(f18577,plain,
~ v1_xboole_0(sF1081),
inference(forward_subsumption_resolution,[],[f18575,f13660]) ).
fof(f18578,plain,
~ spl1085_357,
inference(avatar_split_clause,[],[f18577,f18521]) ).
fof(f18708,plain,
l2_lattices(sK1079),
inference(resolution,[],[f12482,f13660]) ).
fof(f18713,plain,
( $false
| spl1085_353 ),
inference(forward_subsumption_resolution,[],[f18708,f18427]) ).
fof(f18714,plain,
spl1085_353,
inference(avatar_contradiction_clause,[],[f18713]) ).
fof(f18717,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF1081)
| r2_hidden(X0,sF1084)
| ~ r3_lattices(sK1079,sK1080,X0)
| ~ r3_lattices(sK1079,sK1080,sF1083)
| ~ m1_subset_1(sK1080,u1_struct_0(sK1079)) )
| ~ spl1085_353 ),
inference(forward_subsumption_resolution,[],[f18449,f18321]) ).
fof(f18718,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF1081)
| ~ r2_hidden(X0,sF1084)
| r3_lattices(sK1079,sK1080,X0)
| ~ r3_lattices(sK1079,sK1080,sF1083)
| ~ m1_subset_1(sK1080,u1_struct_0(sK1079)) )
| ~ spl1085_353 ),
inference(forward_subsumption_resolution,[],[f18474,f18321]) ).
fof(f18722,plain,
( ! [X0] :
( ~ m1_subset_1(sK1080,sF1081)
| ~ m1_subset_1(X0,sF1081)
| r2_hidden(X0,sF1084)
| ~ r3_lattices(sK1079,sK1080,X0)
| ~ r3_lattices(sK1079,sK1080,sF1083) )
| ~ spl1085_353 ),
inference(forward_demodulation,[],[f18717,f15605]) ).
fof(f18723,plain,
( ! [X0] :
( ~ m1_subset_1(sK1080,sF1081)
| ~ m1_subset_1(X0,sF1081)
| ~ r2_hidden(X0,sF1084)
| r3_lattices(sK1079,sK1080,X0)
| ~ r3_lattices(sK1079,sK1080,sF1083) )
| ~ spl1085_353 ),
inference(forward_demodulation,[],[f18718,f15605]) ).
fof(f18726,plain,
( ! [X0] :
( ~ m1_subset_1(sK1080,sF1081)
| ~ m1_subset_1(X0,sF1081)
| r2_hidden(X0,sF1084)
| ~ r3_lattices(sK1079,sK1080,X0) )
| ~ spl1085_353 ),
inference(forward_subsumption_resolution,[],[f18722,f18250]) ).
fof(f18727,plain,
( ! [X0] :
( ~ m1_subset_1(sK1080,sF1081)
| ~ m1_subset_1(X0,sF1081)
| ~ r2_hidden(X0,sF1084)
| r3_lattices(sK1079,sK1080,X0) )
| ~ spl1085_353 ),
inference(forward_subsumption_resolution,[],[f18723,f18250]) ).
fof(f18730,plain,
( ! [X0] :
( ~ r3_lattices(sK1079,sK1080,X0)
| r2_hidden(X0,sF1084)
| ~ m1_subset_1(X0,sF1081) )
| ~ spl1085_353 ),
inference(forward_subsumption_resolution,[],[f18726,f15613]) ).
fof(f18731,plain,
( ! [X0] :
( r3_lattices(sK1079,sK1080,X0)
| ~ r2_hidden(X0,sF1084)
| ~ m1_subset_1(X0,sF1081) )
| ~ spl1085_353 ),
inference(forward_subsumption_resolution,[],[f18727,f15613]) ).
fof(f18732,plain,
( ! [X0] :
( r2_hidden(X0,sF1084)
| ~ m1_subset_1(X0,sF1081)
| ~ r2_hidden(X0,sF1082)
| ~ m1_subset_1(X0,sF1081) )
| ~ spl1085_353 ),
inference(resolution,[],[f18730,f18501]) ).
fof(f18737,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF1081)
| r2_hidden(X0,sF1084)
| ~ r2_hidden(X0,sF1082) )
| ~ spl1085_353 ),
inference(duplicate_literal_removal,[],[f18732]) ).
fof(f18940,definition,
( spl1085_378
<=> m1_subset_1(sF1082,k1_zfmisc_1(sF1081)) ),
introduced(definition,[new_symbols(definition,[spl1085_378])],[avatar_definition]) ).
fof(f18941,plain,
( m1_subset_1(sF1082,k1_zfmisc_1(sF1081))
| ~ spl1085_378 ),
inference(avatar_component_clause,[],[f18940]) ).
fof(f18942,plain,
( ~ m1_subset_1(sF1082,k1_zfmisc_1(sF1081))
| spl1085_378 ),
inference(avatar_component_clause,[],[f18940]) ).
fof(f18954,plain,
( ~ m1_filter_0(sF1082,sK1079)
| spl1085_378 ),
inference(resolution,[],[f18942,f18351]) ).
fof(f18958,plain,
( $false
| spl1085_378 ),
inference(forward_subsumption_resolution,[],[f18954,f18225]) ).
fof(f18959,plain,
spl1085_378,
inference(avatar_contradiction_clause,[],[f18958]) ).
fof(f18961,plain,
( v1_xboole_0(sF1081)
| r1_filter_2(sF1081,sF1082,sF1082)
| ~ spl1085_378 ),
inference(resolution,[],[f18941,f15621]) ).
fof(f18964,plain,
( r1_filter_2(sF1081,sF1082,sF1082)
| spl1085_357
| ~ spl1085_378 ),
inference(forward_subsumption_resolution,[],[f18961,f18522]) ).
fof(f19485,plain,
! [X0,X1] :
( ~ m2_lattice4(X1,sK1079)
| m1_subset_1(X0,sF1081)
| ~ r2_hidden(X0,X1) ),
inference(resolution,[],[f8903,f18238]) ).
fof(f19486,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF1082)
| m1_subset_1(X0,sF1081) )
| ~ spl1085_378 ),
inference(resolution,[],[f8903,f18941]) ).
fof(f19495,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF1084)
| m1_subset_1(X0,sF1081) )
| ~ spl1085_352 ),
inference(resolution,[],[f19485,f18318]) ).
fof(f19596,plain,
! [X0] :
( r2_hidden(X0,sF1082)
| ~ r3_lattices(sK1079,sK1080,X0)
| ~ m1_subset_1(sK1080,u1_struct_0(sK1079))
| ~ m1_subset_1(X0,u1_struct_0(sK1079))
| v3_struct_0(sK1079)
| ~ v10_lattices(sK1079)
| ~ l3_lattices(sK1079) ),
inference(superposition,[],[f12599,f18180]) ).
fof(f19598,plain,
! [X0] :
( r2_hidden(X0,sF1082)
| ~ r3_lattices(sK1079,sK1080,X0)
| ~ m1_subset_1(sK1080,u1_struct_0(sK1079))
| ~ m1_subset_1(X0,u1_struct_0(sK1079))
| ~ v10_lattices(sK1079)
| ~ l3_lattices(sK1079) ),
inference(forward_subsumption_resolution,[],[f19596,f13662]) ).
fof(f19599,plain,
! [X0] :
( r2_hidden(X0,sF1082)
| ~ r3_lattices(sK1079,sK1080,X0)
| ~ m1_subset_1(sK1080,u1_struct_0(sK1079))
| ~ m1_subset_1(X0,u1_struct_0(sK1079))
| ~ l3_lattices(sK1079) ),
inference(forward_subsumption_resolution,[],[f19598,f13661]) ).
fof(f19600,plain,
! [X0] :
( r2_hidden(X0,sF1082)
| ~ r3_lattices(sK1079,sK1080,X0)
| ~ m1_subset_1(sK1080,u1_struct_0(sK1079))
| ~ m1_subset_1(X0,u1_struct_0(sK1079)) ),
inference(forward_subsumption_resolution,[],[f19599,f13660]) ).
fof(f19601,plain,
! [X0] :
( ~ m1_subset_1(sK1080,sF1081)
| r2_hidden(X0,sF1082)
| ~ r3_lattices(sK1079,sK1080,X0)
| ~ m1_subset_1(X0,u1_struct_0(sK1079)) ),
inference(forward_demodulation,[],[f19600,f15605]) ).
fof(f19602,plain,
! [X0] :
( r2_hidden(X0,sF1082)
| ~ r3_lattices(sK1079,sK1080,X0)
| ~ m1_subset_1(X0,u1_struct_0(sK1079)) ),
inference(forward_subsumption_resolution,[],[f19601,f15613]) ).
fof(f19603,plain,
! [X0] :
( ~ r3_lattices(sK1079,sK1080,X0)
| r2_hidden(X0,sF1082)
| ~ m1_subset_1(X0,sF1081) ),
inference(forward_demodulation,[],[f19602,f15605]) ).
fof(f19604,plain,
( ! [X0] :
( r2_hidden(X0,sF1082)
| ~ m1_subset_1(X0,sF1081)
| ~ r2_hidden(X0,sF1084)
| ~ m1_subset_1(X0,sF1081) )
| ~ spl1085_353 ),
inference(resolution,[],[f19603,f18731]) ).
fof(f19611,plain,
( ! [X0] :
( r2_hidden(X0,sF1082)
| ~ m1_subset_1(X0,sF1081)
| ~ r2_hidden(X0,sF1084) )
| ~ spl1085_353 ),
inference(duplicate_literal_removal,[],[f19604]) ).
fof(f19613,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF1084)
| r2_hidden(X0,sF1082) )
| ~ spl1085_352
| ~ spl1085_353 ),
inference(forward_subsumption_resolution,[],[f19611,f19495]) ).
fof(f19957,plain,
( ! [X0] :
( m1_subset_1(sK130(sF1082,X0),sF1081)
| r1_tarski(sF1082,X0) )
| ~ spl1085_378 ),
inference(resolution,[],[f8129,f19486]) ).
fof(f19958,plain,
( ! [X0] :
( r2_hidden(sK130(sF1084,X0),sF1082)
| r1_tarski(sF1084,X0) )
| ~ spl1085_352
| ~ spl1085_353 ),
inference(resolution,[],[f8129,f19613]) ).
fof(f19967,plain,
( ! [X0] :
( r1_tarski(sF1082,X0)
| r2_hidden(sK130(sF1082,X0),sF1084)
| ~ r2_hidden(sK130(sF1082,X0),sF1082) )
| ~ spl1085_353
| ~ spl1085_378 ),
inference(resolution,[],[f19957,f18737]) ).
fof(f19972,plain,
( ! [X0] :
( r2_hidden(sK130(sF1082,X0),sF1084)
| r1_tarski(sF1082,X0) )
| ~ spl1085_353
| ~ spl1085_378 ),
inference(forward_subsumption_resolution,[],[f19967,f8129]) ).
fof(f20727,plain,
( r1_tarski(sF1084,sF1082)
| r1_tarski(sF1084,sF1082)
| ~ spl1085_352
| ~ spl1085_353 ),
inference(resolution,[],[f8130,f19958]) ).
fof(f20728,plain,
( r1_tarski(sF1082,sF1084)
| r1_tarski(sF1082,sF1084)
| ~ spl1085_353
| ~ spl1085_378 ),
inference(resolution,[],[f8130,f19972]) ).
fof(f20732,plain,
( r1_tarski(sF1082,sF1084)
| ~ spl1085_353
| ~ spl1085_378 ),
inference(duplicate_literal_removal,[],[f20728]) ).
fof(f20733,plain,
( r1_tarski(sF1084,sF1082)
| ~ spl1085_352
| ~ spl1085_353 ),
inference(duplicate_literal_removal,[],[f20727]) ).
fof(f20737,plain,
( spl1085_350
| ~ spl1085_353
| ~ spl1085_378 ),
inference(avatar_split_clause,[],[f20732,f18940,f18320,f18300]) ).
fof(f20740,plain,
( ~ r1_tarski(sF1082,sF1084)
| sF1082 = sF1084
| ~ spl1085_352
| ~ spl1085_353 ),
inference(resolution,[],[f20733,f8197]) ).
fof(f20741,plain,
( sF1082 = sF1084
| ~ spl1085_350
| ~ spl1085_352
| ~ spl1085_353 ),
inference(forward_subsumption_resolution,[],[f20740,f18301]) ).
fof(f20742,plain,
( ~ r1_filter_2(sF1081,sF1082,sF1082)
| ~ spl1085_350
| ~ spl1085_352
| ~ spl1085_353 ),
inference(superposition,[],[f15612,f20741]) ).
fof(f20765,plain,
( $false
| ~ spl1085_350
| ~ spl1085_352
| ~ spl1085_353
| spl1085_357
| ~ spl1085_378 ),
inference(forward_subsumption_resolution,[],[f20742,f18964]) ).
fof(f20766,plain,
( ~ spl1085_350
| ~ spl1085_352
| ~ spl1085_353
| spl1085_357
| ~ spl1085_378 ),
inference(avatar_contradiction_clause,[],[f20765]) ).
cnf(s299,plain,
( spl1085_352
| ~ spl1085_353 ),
inference(sat_conversion,[],[f18323]) ).
cnf(s316,plain,
~ spl1085_357,
inference(sat_conversion,[],[f18578]) ).
cnf(s321,plain,
spl1085_353,
inference(sat_conversion,[],[f18714]) ).
cnf(s331,plain,
spl1085_378,
inference(sat_conversion,[],[f18959]) ).
cnf(s392,plain,
( spl1085_350
| ~ spl1085_353
| ~ spl1085_378 ),
inference(sat_conversion,[],[f20737]) ).
cnf(s393,plain,
( ~ spl1085_350
| ~ spl1085_352
| ~ spl1085_353
| spl1085_357
| ~ spl1085_378 ),
inference(sat_conversion,[],[f20766]) ).
cnf(s401,plain,
spl1085_350,
inference(rat,[],[s392,s331,s321]) ).
cnf(s405,plain,
~ spl1085_352,
inference(rat,[],[s393,s331,s401,s321,s316]) ).
cnf(s422,plain,
$false,
inference(rat,[],[s299,s321,s405]) ).
fof(f20767,plain,
$false,
inference(avatar_sat_refutation,[],[s422]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT329+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.37 % Computer : n004.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sun Sep 27 14:40:52 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.41 Running first-order theorem proving
% 0.11/0.41 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 11.99/2.68 % (3590085)Detected formulas, will run a generic FOF schedule.
% 11.99/2.68 % (3590095)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=696233936:s2a=on:i=139:gtg=position_2998 on theBenchmark for (2998ds/139Mi)
% 11.99/2.68 % (3590094)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=4075055200:i=119:av=off:ss=axioms_2998 on theBenchmark for (2998ds/119Mi)
% 11.99/2.68 % (3590090)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=944834398:i=141193_2998 on theBenchmark for (2998ds/141193Mi)
% 11.99/2.68 % (3590092)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=3631062426:i=141695:sd=1:nm=32:gsp=on:ss=included_2998 on theBenchmark for (2998ds/141695Mi)
% 11.99/2.68 % (3590096)dis-21_1_sil=8000:lcm=predicate:random_seed=1730422401:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2998 on theBenchmark for (2998ds/129Mi)
% 11.99/2.68 % (3590093)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3795513870:i=109:sd=1:ins=1:gsp=on:ss=axioms_2998 on theBenchmark for (2998ds/109Mi)
% 11.99/2.68 % (3590091)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=1831085160:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2998 on theBenchmark for (2998ds/134677Mi)
% 11.99/2.68 % (3590095)Instruction limit reached!
% 11.99/2.68 % (3590095)------------------------------
% 11.99/2.68 % (3590095)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.99/2.68 % (3590095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.99/2.68 % (3590095)CaDiCaL version: 2.1.3
% 11.99/2.68 % (3590095)Termination reason: Instruction limit
% 11.99/2.68 % (3590095)Termination phase: Clausification
% 11.99/2.68 % (3590095)Time elapsed: 0.049 s
% 11.99/2.68 % (3590095)Peak memory usage: 94 MB
% 11.99/2.68 % (3590095)Instructions burned: 139 (million)
% 11.99/2.68 % (3590093)Refutation not found, incomplete strategy
% 11.99/2.68 % (3590093)------------------------------
% 11.99/2.68 % (3590093)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.99/2.68 % (3590093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.99/2.68 % (3590093)CaDiCaL version: 2.1.3
% 11.99/2.68 % (3590093)Termination reason: Refutation not found, incomplete strategy
% 11.99/2.68 % (3590093)Time elapsed: 0.014 s
% 11.99/2.68 % (3590093)Peak memory usage: 91 MB
% 11.99/2.68 % (3590093)Instructions burned: 17 (million)
% 11.99/2.68 % (3590094)Instruction limit reached!
% 11.99/2.68 % (3590094)------------------------------
% 11.99/2.68 % (3590094)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.99/2.68 % (3590094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.99/2.68 % (3590094)CaDiCaL version: 2.1.3
% 11.99/2.68 % (3590094)Termination reason: Instruction limit
% 11.99/2.68 % (3590094)Termination phase: Saturation
% 11.99/2.68 % (3590094)Time elapsed: 0.075 s
% 11.99/2.68 % (3590094)Peak memory usage: 93 MB
% 11.99/2.68 % (3590094)Instructions burned: 119 (million)
% 11.99/2.68 % (3590096)Instruction limit reached!
% 11.99/2.68 % (3590096)------------------------------
% 11.99/2.68 % (3590096)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.99/2.68 % (3590096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.99/2.68 % (3590096)CaDiCaL version: 2.1.3
% 11.99/2.68 % (3590096)Termination reason: Instruction limit
% 11.99/2.68 % (3590096)Termination phase: Property scanning
% 11.99/2.68 % (3590096)Time elapsed: 0.078 s
% 11.99/2.68 % (3590096)Peak memory usage: 93 MB
% 11.99/2.68 % (3590096)Instructions burned: 129 (million)
% 11.99/2.68 % (3590104)lrs+10_1_sil=8000:sp=occurrence:random_seed=35423729:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 11.99/2.68 % (3590105)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2312303534:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi)
% 11.99/2.68 % (3590106)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1634092530:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi)
% 11.99/2.68 % (3590104)Instruction limit reached!
% 11.99/2.68 % (3590104)------------------------------
% 11.99/2.68 % (3590104)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.99/2.68 % (3590104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.44/3.71 % (3590104)CaDiCaL version: 2.1.3
% 19.44/3.71 % (3590104)Termination reason: Instruction limit
% 19.44/3.71 % (3590104)Termination phase: Saturation
% 19.44/3.71 % (3590104)Time elapsed: 0.098 s
% 19.44/3.71 % (3590104)Peak memory usage: 95 MB
% 19.44/3.71 % (3590104)Instructions burned: 288 (million)
% 19.44/3.71 % (3590093)------------------------------
% 19.44/3.71 % (3590093)------------------------------
% 19.44/3.71 % (3590105)Refutation not found, incomplete strategy
% 19.44/3.71 % (3590105)------------------------------
% 19.44/3.71 % (3590105)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.44/3.71 % (3590105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.44/3.71 % (3590105)CaDiCaL version: 2.1.3
% 19.44/3.71 % (3590105)Termination reason: Refutation not found, incomplete strategy
% 19.44/3.71 % (3590105)Time elapsed: 0.029 s
% 19.44/3.71 % (3590105)Peak memory usage: 92 MB
% 19.44/3.71 % (3590105)Instructions burned: 48 (million)
% 19.44/3.71 % (3590106)Refutation not found, incomplete strategy
% 19.44/3.71 % (3590106)------------------------------
% 19.44/3.71 % (3590106)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.44/3.71 % (3590106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.44/3.71 % (3590106)CaDiCaL version: 2.1.3
% 19.44/3.71 % (3590106)Termination reason: Refutation not found, incomplete strategy
% 19.44/3.71 % (3590106)Time elapsed: 0.043 s
% 19.44/3.71 % (3590106)Peak memory usage: 92 MB
% 19.44/3.71 % (3590106)Instructions burned: 43 (million)
% 19.44/3.71 % (3590110)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=2256788110:s2a=on:i=248:s2at=1.23:gtg=position_2994 on theBenchmark for (2994ds/248Mi)
% 19.44/3.71 % (3590111)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2020822043:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 19.44/3.71 % (3590110)Instruction limit reached!
% 19.44/3.71 % (3590110)------------------------------
% 19.44/3.71 % (3590110)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.44/3.71 % (3590110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.44/3.71 % (3590110)CaDiCaL version: 2.1.3
% 19.44/3.71 % (3590110)Termination reason: Instruction limit
% 19.44/3.71 % (3590110)Termination phase: Saturation
% 19.44/3.71 % (3590110)Time elapsed: 0.076 s
% 19.44/3.71 % (3590110)Peak memory usage: 97 MB
% 19.44/3.71 % (3590110)Instructions burned: 249 (million)
% 19.44/3.71 % (3590105)------------------------------
% 19.44/3.71 % (3590105)------------------------------
% 19.44/3.71 % (3590106)------------------------------
% 19.44/3.71 % (3590106)------------------------------
% 19.44/3.71 % (3590114)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2437586054:i=2350_2992 on theBenchmark for (2992ds/2350Mi)
% 19.44/3.71 % (3590111)Instruction limit reached!
% 19.44/3.71 % (3590111)------------------------------
% 19.44/3.71 % (3590111)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.44/3.71 % (3590111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.44/3.71 % (3590111)CaDiCaL version: 2.1.3
% 19.44/3.71 % (3590111)Termination reason: Instruction limit
% 19.44/3.71 % (3590111)Termination phase: Saturation
% 19.44/3.71 % (3590111)Time elapsed: 0.173 s
% 19.44/3.71 % (3590111)Peak memory usage: 95 MB
% 19.44/3.71 % (3590111)Instructions burned: 294 (million)
% 19.44/3.71 % (3590115)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2976462133:cts=off:i=113:fsr=off:ss=included:sgt=4_2992 on theBenchmark for (2992ds/113Mi)
% 19.44/3.71 % (3590116)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1575526472:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi)
% 19.44/3.71 % (3590115)Instruction limit reached!
% 19.44/3.71 % (3590115)------------------------------
% 19.44/3.71 % (3590115)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.44/3.71 % (3590115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.44/3.71 % (3590115)CaDiCaL version: 2.1.3
% 19.44/3.71 % (3590115)Termination reason: Instruction limit
% 19.44/3.71 % (3590115)Termination phase: Saturation
% 19.44/3.71 % (3590115)Time elapsed: 0.065 s
% 19.44/3.71 % (3590115)Peak memory usage: 93 MB
% 19.44/3.71 % (3590115)Instructions burned: 114 (million)
% 19.44/3.71 % (3590116)Instruction limit reached!
% 19.44/3.71 % (3590116)------------------------------
% 19.44/3.71 % (3590116)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.44/3.78 % (3590116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.44/3.78 % (3590116)CaDiCaL version: 2.1.3
% 19.44/3.78 % (3590116)Termination reason: Instruction limit
% 19.44/3.78 % (3590116)Termination phase: Property scanning
% 19.44/3.78 % (3590116)Time elapsed: 0.076 s
% 19.44/3.78 % (3590116)Peak memory usage: 94 MB
% 19.44/3.78 % (3590116)Instructions burned: 128 (million)
% 19.44/3.78 % (3590118)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2216073862:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 19.44/3.78 % (3590118)Instruction limit reached!
% 19.44/3.78 % (3590118)------------------------------
% 19.44/3.78 % (3590118)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.44/3.78 % (3590118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.44/3.78 % (3590118)CaDiCaL version: 2.1.3
% 19.44/3.78 % (3590118)Termination reason: Instruction limit
% 19.44/3.78 % (3590118)Termination phase: Property scanning
% 19.44/3.78 % (3590118)Time elapsed: 0.060 s
% 19.44/3.78 % (3590118)Peak memory usage: 91 MB
% 19.44/3.78 % (3590118)Instructions burned: 116 (million)
% 19.44/3.78 % (3590121)lrs+10_1_sil=8000:sp=occurrence:random_seed=4024065596:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2989 on theBenchmark for (2989ds/907Mi)
% 19.44/3.78 % (3590123)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3117138928:i=437:sd=1:aac=none:ss=included_2989 on theBenchmark for (2989ds/437Mi)
% 19.44/3.78 % (3590124)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1737542339:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi)
% 19.44/3.78 % (3590123)Instruction limit reached!
% 19.44/3.78 % (3590123)------------------------------
% 19.44/3.78 % (3590123)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.44/3.78 % (3590123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.44/3.78 % (3590123)CaDiCaL version: 2.1.3
% 19.44/3.78 % (3590123)Termination reason: Instruction limit
% 19.44/3.78 % (3590123)Termination phase: Saturation
% 19.44/3.78 % (3590123)Time elapsed: 0.243 s
% 19.44/3.78 % (3590123)Peak memory usage: 95 MB
% 19.44/3.78 % (3590123)Instructions burned: 438 (million)
% 19.44/3.78 % (3590128)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3643069341:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2985 on theBenchmark for (2985ds/134Mi)
% 19.44/3.78 % (3590128)Instruction limit reached!
% 19.44/3.78 % (3590128)------------------------------
% 19.44/3.78 % (3590128)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.44/3.78 % (3590128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.44/3.78 % (3590128)CaDiCaL version: 2.1.3
% 19.44/3.78 % (3590128)Termination reason: Instruction limit
% 19.44/3.78 % (3590128)Termination phase: Saturation
% 19.44/3.78 % (3590128)Time elapsed: 0.080 s
% 19.44/3.78 % (3590128)Peak memory usage: 95 MB
% 19.44/3.78 % (3590128)Instructions burned: 134 (million)
% 19.44/3.78 % (3590114)Instruction limit reached!
% 19.44/3.78 % (3590114)------------------------------
% 19.44/3.78 % (3590114)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.44/3.78 % (3590114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.44/3.78 % (3590114)CaDiCaL version: 2.1.3
% 19.44/3.78 % (3590114)Termination reason: Instruction limit
% 19.44/3.78 % (3590114)Termination phase: Saturation
% 19.44/3.78 % (3590114)Time elapsed: 0.850 s
% 19.44/3.78 % (3590114)Peak memory usage: 219 MB
% 19.44/3.78 % (3590114)Instructions burned: 2353 (million)
% 19.44/3.78 % (3590121)Instruction limit reached!
% 19.44/3.78 % (3590121)------------------------------
% 19.44/3.78 % (3590121)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.44/3.78 % (3590121)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.44/3.78 % (3590121)CaDiCaL version: 2.1.3
% 19.44/3.78 % (3590121)Termination reason: Instruction limit
% 19.44/3.78 % (3590121)Termination phase: Saturation
% 19.44/3.78 % (3590121)Time elapsed: 0.591 s
% 19.44/3.78 % (3590121)Peak memory usage: 104 MB
% 19.44/3.78 % (3590121)Instructions burned: 908 (million)
% 19.44/3.78 % (3590131)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3469109123:st=3:i=13193:sd=3:ss=axioms_2983 on theBenchmark for (2983ds/13193Mi)
% 19.44/3.78 % (3590130)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2876770433:st=8:i=592:sd=3:ep=RST:ss=axioms_2983 on theBenchmark for (2983ds/592Mi)
% 19.44/3.78 % (3590132)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=3252088767:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2982 on theBenchmark for (2982ds/125Mi)
% 19.44/3.78 % (3590132)Instruction limit reached!
% 19.44/3.78 % (3590132)------------------------------
% 19.44/3.78 % (3590132)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.44/3.78 % (3590132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.44/3.78 % (3590132)CaDiCaL version: 2.1.3
% 19.44/3.78 % (3590132)Termination reason: Instruction limit
% 19.44/3.78 % (3590132)Termination phase: Saturation
% 19.44/3.78 % (3590132)Time elapsed: 0.069 s
% 19.44/3.78 % (3590132)Peak memory usage: 93 MB
% 19.44/3.78 % (3590132)Instructions burned: 126 (million)
% 19.44/3.78 % (3590130)Instruction limit reached!
% 19.44/3.78 % (3590130)------------------------------
% 19.44/3.78 % (3590130)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.44/3.78 % (3590130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.44/3.78 % (3590130)CaDiCaL version: 2.1.3
% 19.44/3.78 % (3590130)Termination reason: Instruction limit
% 19.44/3.78 % (3590130)Termination phase: Saturation
% 19.44/3.78 % (3590130)Time elapsed: 0.295 s
% 19.44/3.78 % (3590130)Peak memory usage: 102 MB
% 19.44/3.78 % (3590130)Instructions burned: 593 (million)
% 19.44/3.78 % (3590136)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1134545122:i=134:gtgl=5:slsql=off:gtg=exists_sym_2980 on theBenchmark for (2980ds/134Mi)
% 19.44/3.78 % (3590136)Instruction limit reached!
% 19.44/3.78 % (3590136)------------------------------
% 19.44/3.78 % (3590136)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.44/3.78 % (3590136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.44/3.78 % (3590136)CaDiCaL version: 2.1.3
% 19.44/3.78 % (3590136)Termination reason: Instruction limit
% 19.44/3.78 % (3590136)Termination phase: Preprocessing 3
% 19.44/3.78 % (3590136)Time elapsed: 0.077 s
% 19.44/3.78 % (3590136)Peak memory usage: 92 MB
% 19.44/3.78 % (3590136)Instructions burned: 134 (million)
% 19.44/3.78 % (3590137)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=569045985:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2978 on theBenchmark for (2978ds/141Mi)
% 19.44/3.78 % (3590137)Refutation not found, incomplete strategy
% 19.44/3.78 % (3590137)------------------------------
% 19.44/3.78 % (3590137)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.44/3.78 % (3590137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.44/3.78 % (3590137)CaDiCaL version: 2.1.3
% 19.44/3.78 % (3590137)Termination reason: Refutation not found, incomplete strategy
% 19.44/3.78 % (3590137)Time elapsed: 0.014 s
% 19.44/3.78 % (3590137)Peak memory usage: 92 MB
% 19.44/3.78 % (3590137)Instructions burned: 15 (million)
% 19.44/3.78 % (3590139)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3396763071:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2977 on theBenchmark for (2977ds/431Mi)
% 19.44/3.78 % (3590139)Refutation not found, incomplete strategy
% 19.44/3.78 % (3590139)------------------------------
% 19.44/3.78 % (3590139)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.44/3.78 % (3590139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.44/3.78 % (3590139)CaDiCaL version: 2.1.3
% 19.44/3.78 % (3590139)Termination reason: Refutation not found, incomplete strategy
% 19.44/3.78 % (3590139)Time elapsed: 0.019 s
% 19.44/3.78 % (3590139)Peak memory usage: 92 MB
% 19.44/3.78 % (3590139)Instructions burned: 23 (million)
% 19.44/3.78 % (3590137)------------------------------
% 19.44/3.78 % (3590137)------------------------------
% 19.44/3.78 % (3590090)First to succeed.
% 19.44/3.78 % (3590090)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3590085"
% 19.44/3.78 % (3590139)------------------------------
% 19.44/3.78 % (3590139)------------------------------
% 19.44/3.78 % (3590142)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=2676205856:i=6060:aac=none:ins=25_2974 on theBenchmark for (2974ds/6060Mi)
% 19.44/3.78 % (3590143)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=1432384557:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2973 on theBenchmark for (2973ds/150Mi)
% 19.44/3.78 % (3590090)Refutation found. Thanks to Tanya!
% 19.44/3.78 % SZS status Theorem for theBenchmark
% 19.44/3.78 % SZS output start Proof for theBenchmark
% See solution above
% 20.58/3.98 % (3590090)------------------------------
% 20.58/3.98 % (3590090)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.58/3.98 % (3590090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.58/3.98 % (3590090)CaDiCaL version: 2.1.3
% 20.58/3.98 % (3590090)Termination reason: Refutation
% 20.58/3.98 % (3590090)Time elapsed: 2.381 s
% 20.58/3.98 % (3590090)Peak memory usage: 221 MB
% 20.58/3.98 % (3590090)Instructions burned: 3934 (million)
% 20.58/3.98 % (3590090)------------------------------
% 20.58/3.98 % (3590090)------------------------------
% 20.58/3.98 % (3590085)Success in time 2.925 s
% 20.58/3.98 % Vampire exiting
%------------------------------------------------------------------------------