%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT289+3 : 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 : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:46:34 AM UTC 2026
% Result : Theorem 7.61s 2.60s
% Output : Refutation 9.08s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 22
% Syntax : Number of formulae : 206 ( 32 unt; 10 def)
% Number of atoms : 936 ( 85 equ)
% Maximal formula atoms : 16 ( 4 avg)
% Number of connectives : 1218 ( 488 ~; 567 |; 121 &)
% ( 24 <=>; 18 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 27 ( 25 usr; 11 prp; 0-3 aty)
% Number of functors : 18 ( 18 usr; 5 con; 0-4 aty)
% Number of variables : 153 ( 0 sgn 137 !; 16 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f29,axiom,
! [X0] :
( X0 = k1_xboole_0
<=> ! [X1] : ~ r2_hidden(X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d1_xboole_0) ).
fof(f68,axiom,
! [X0,X1] :
~ ( r2_hidden(X0,X1)
& v1_xboole_0(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t7_boole) ).
fof(f932,axiom,
! [X0] :
( ( v1_relat_1(X0)
& v1_funct_1(X0) )
=> ! [X1,X2] :
( ( r2_hidden(X1,k1_relat_1(X0))
=> ( X2 = k1_funct_1(X0,X1)
<=> r2_hidden(k4_tarski(X1,X2),X0) ) )
& ( ~ r2_hidden(X1,k1_relat_1(X0))
=> ( X2 = k1_funct_1(X0,X1)
<=> X2 = k1_xboole_0 ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d4_funct_1) ).
fof(f1394,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
<=> m1_relset_1(X2,X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(f2017,axiom,
! [X0,X1,X2,X3] :
( ( ~ v1_xboole_0(X0)
& v1_funct_1(X2)
& v1_funct_2(X2,X0,X1)
& m1_relset_1(X2,X0,X1)
& m1_subset_1(X3,X0) )
=> k8_funct_2(X0,X1,X2,X3) = k1_funct_1(X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k8_funct_2) ).
fof(f3551,axiom,
np__0 = k1_xboole_0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t51_card_1) ).
fof(f12344,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& ~ v3_realset2(X0)
& l3_lattices(X0) )
=> ( v1_relat_1(k8_lopclset(X0))
& v1_funct_1(k8_lopclset(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k8_lopclset) ).
fof(f12345,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& ~ v3_realset2(X0)
& l3_lattices(X0) )
=> ( v1_funct_1(k9_lopclset(X0))
& v1_funct_2(k9_lopclset(X0),u1_struct_0(X0),k1_zfmisc_1(k7_lopclset(X0)))
& m2_relset_1(k9_lopclset(X0),u1_struct_0(X0),k1_zfmisc_1(k7_lopclset(X0))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k9_lopclset) ).
fof(f12346,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& ~ v3_realset2(X0)
& l3_lattices(X0) )
=> k9_lopclset(X0) = k8_lopclset(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k9_lopclset) ).
fof(f12379,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& ~ v3_realset2(X0)
& l3_lattices(X0) )
=> ! [X1] :
( ( v1_relat_1(X1)
& v1_funct_1(X1) )
=> ( X1 = k8_lopclset(X0)
<=> ( k1_relat_1(X1) = u1_struct_0(X0)
& ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> k1_funct_1(X1,X2) = a_2_0_lopclset(X0,X2) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d6_lopclset) ).
fof(f12380,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& v17_lattices(X1)
& ~ v3_realset2(X1)
& l3_lattices(X1) )
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X1))
=> ( r2_hidden(X0,k1_funct_1(k8_lopclset(X1),X2))
<=> ? [X3] :
( m1_filter_0(X3,X1)
& X3 = X0
& v1_filter_0(X3,X1)
& r2_hidden(X2,X3) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t20_lopclset) ).
fof(f12391,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& ~ v3_realset2(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_filter_0(X2,X0)
=> ~ ( v1_filter_0(X2,X0)
& ~ r2_hidden(X2,k8_funct_2(u1_struct_0(X0),k1_zfmisc_1(k7_lopclset(X0)),k9_lopclset(X0),X1))
& r2_hidden(X1,X2) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t27_lopclset) ).
fof(f12392,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& ~ v3_realset2(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_filter_0(X2,X0)
=> ~ ( v1_filter_0(X2,X0)
& ~ r2_hidden(X2,k8_funct_2(u1_struct_0(X0),k1_zfmisc_1(k7_lopclset(X0)),k9_lopclset(X0),X1))
& r2_hidden(X1,X2) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f12391]) ).
fof(f12564,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( v1_filter_0(X2,X0)
& ~ r2_hidden(X2,k8_funct_2(u1_struct_0(X0),k1_zfmisc_1(k7_lopclset(X0)),k9_lopclset(X0),X1))
& r2_hidden(X1,X2)
& m1_filter_0(X2,X0) )
& m1_subset_1(X1,u1_struct_0(X0)) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& ~ v3_realset2(X0)
& l3_lattices(X0) ),
inference(ennf_transformation,[],[f12392]) ).
fof(f12565,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( v1_filter_0(X2,X0)
& ~ r2_hidden(X2,k8_funct_2(u1_struct_0(X0),k1_zfmisc_1(k7_lopclset(X0)),k9_lopclset(X0),X1))
& r2_hidden(X1,X2)
& m1_filter_0(X2,X0) )
& m1_subset_1(X1,u1_struct_0(X0)) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& ~ v3_realset2(X0)
& l3_lattices(X0) ),
inference(flattening,[],[f12564]) ).
fof(f12605,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| ~ v1_xboole_0(X1) ),
inference(ennf_transformation,[],[f68]) ).
fof(f12629,plain,
! [X0,X1,X2,X3] :
( k8_funct_2(X0,X1,X2,X3) = k1_funct_1(X2,X3)
| v1_xboole_0(X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1)
| ~ m1_subset_1(X3,X0) ),
inference(ennf_transformation,[],[f2017]) ).
fof(f12630,plain,
! [X0,X1,X2,X3] :
( k8_funct_2(X0,X1,X2,X3) = k1_funct_1(X2,X3)
| v1_xboole_0(X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1)
| ~ m1_subset_1(X3,X0) ),
inference(flattening,[],[f12629]) ).
fof(f12699,plain,
! [X0,X1] :
( ! [X2] :
( ( r2_hidden(X0,k1_funct_1(k8_lopclset(X1),X2))
<=> ? [X3] :
( m1_filter_0(X3,X1)
& X3 = X0
& v1_filter_0(X3,X1)
& r2_hidden(X2,X3) ) )
| ~ m1_subset_1(X2,u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ v17_lattices(X1)
| v3_realset2(X1)
| ~ l3_lattices(X1) ),
inference(ennf_transformation,[],[f12380]) ).
fof(f12700,plain,
! [X0,X1] :
( ! [X2] :
( ( r2_hidden(X0,k1_funct_1(k8_lopclset(X1),X2))
<=> ? [X3] :
( m1_filter_0(X3,X1)
& X3 = X0
& v1_filter_0(X3,X1)
& r2_hidden(X2,X3) ) )
| ~ m1_subset_1(X2,u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ v17_lattices(X1)
| v3_realset2(X1)
| ~ l3_lattices(X1) ),
inference(flattening,[],[f12699]) ).
fof(f12721,plain,
! [X0] :
( ( v1_funct_1(k9_lopclset(X0))
& v1_funct_2(k9_lopclset(X0),u1_struct_0(X0),k1_zfmisc_1(k7_lopclset(X0)))
& m2_relset_1(k9_lopclset(X0),u1_struct_0(X0),k1_zfmisc_1(k7_lopclset(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f12345]) ).
fof(f12722,plain,
! [X0] :
( ( v1_funct_1(k9_lopclset(X0))
& v1_funct_2(k9_lopclset(X0),u1_struct_0(X0),k1_zfmisc_1(k7_lopclset(X0)))
& m2_relset_1(k9_lopclset(X0),u1_struct_0(X0),k1_zfmisc_1(k7_lopclset(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f12721]) ).
fof(f12727,plain,
! [X0] :
( k9_lopclset(X0) = k8_lopclset(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f12346]) ).
fof(f12728,plain,
! [X0] :
( k9_lopclset(X0) = k8_lopclset(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f12727]) ).
fof(f12888,plain,
! [X0] :
( ! [X1,X2] :
( ( ( X2 = k1_funct_1(X0,X1)
<=> r2_hidden(k4_tarski(X1,X2),X0) )
| ~ r2_hidden(X1,k1_relat_1(X0)) )
& ( ( X2 = k1_funct_1(X0,X1)
<=> X2 = k1_xboole_0 )
| r2_hidden(X1,k1_relat_1(X0)) ) )
| ~ v1_relat_1(X0)
| ~ v1_funct_1(X0) ),
inference(ennf_transformation,[],[f932]) ).
fof(f12889,plain,
! [X0] :
( ! [X1,X2] :
( ( ( X2 = k1_funct_1(X0,X1)
<=> r2_hidden(k4_tarski(X1,X2),X0) )
| ~ r2_hidden(X1,k1_relat_1(X0)) )
& ( ( X2 = k1_funct_1(X0,X1)
<=> X2 = k1_xboole_0 )
| r2_hidden(X1,k1_relat_1(X0)) ) )
| ~ v1_relat_1(X0)
| ~ v1_funct_1(X0) ),
inference(flattening,[],[f12888]) ).
fof(f14083,plain,
! [X0] :
( ! [X1] :
( ( X1 = k8_lopclset(X0)
<=> ( k1_relat_1(X1) = u1_struct_0(X0)
& ! [X2] :
( k1_funct_1(X1,X2) = a_2_0_lopclset(X0,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0)) ) ) )
| ~ v1_relat_1(X1)
| ~ v1_funct_1(X1) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f12379]) ).
fof(f14084,plain,
! [X0] :
( ! [X1] :
( ( X1 = k8_lopclset(X0)
<=> ( k1_relat_1(X1) = u1_struct_0(X0)
& ! [X2] :
( k1_funct_1(X1,X2) = a_2_0_lopclset(X0,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0)) ) ) )
| ~ v1_relat_1(X1)
| ~ v1_funct_1(X1) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f14083]) ).
fof(f14087,plain,
! [X0] :
( ( v1_relat_1(k8_lopclset(X0))
& v1_funct_1(k8_lopclset(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f12344]) ).
fof(f14088,plain,
! [X0] :
( ( v1_relat_1(k8_lopclset(X0))
& v1_funct_1(k8_lopclset(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f14087]) ).
fof(f14139,plain,
( v1_filter_0(sK30,sK28)
& ~ r2_hidden(sK30,k8_funct_2(u1_struct_0(sK28),k1_zfmisc_1(k7_lopclset(sK28)),k9_lopclset(sK28),sK29))
& r2_hidden(sK29,sK30)
& m1_filter_0(sK30,sK28)
& m1_subset_1(sK29,u1_struct_0(sK28))
& ~ v3_struct_0(sK28)
& v10_lattices(sK28)
& v17_lattices(sK28)
& ~ v3_realset2(sK28)
& l3_lattices(sK28) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK28,sK29,sK30]),skolemize(X0,sK28),skolemize(X1,sK29),skolemize(X2,sK30)],[f12565]) ).
fof(f14160,plain,
! [X0] :
( ( X0 = k1_xboole_0
| ? [X1] : r2_hidden(X1,X0) )
& ( ! [X1] : ~ r2_hidden(X1,X0)
| k1_xboole_0 != X0 ) ),
inference(nnf_transformation,[],[f29]) ).
fof(f14161,plain,
! [X0] :
( ( X0 = k1_xboole_0
| ? [X1] : r2_hidden(X1,X0) )
& ( ! [X2] : ~ r2_hidden(X2,X0)
| k1_xboole_0 != X0 ) ),
inference(rectify,[],[f14160]) ).
fof(f14162,plain,
! [X0] :
( ( X0 = k1_xboole_0
| r2_hidden(sK45(X0),X0) )
& ( ! [X2] : ~ r2_hidden(X2,X0)
| k1_xboole_0 != X0 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK45]),skolemize(X1,sK45(X0))],[f14161]) ).
fof(f14211,plain,
! [X0,X1] :
( ! [X2] :
( ( ( r2_hidden(X0,k1_funct_1(k8_lopclset(X1),X2))
| ! [X3] :
( ~ m1_filter_0(X3,X1)
| X0 != X3
| ~ v1_filter_0(X3,X1)
| ~ r2_hidden(X2,X3) ) )
& ( ? [X3] :
( m1_filter_0(X3,X1)
& X3 = X0
& v1_filter_0(X3,X1)
& r2_hidden(X2,X3) )
| ~ r2_hidden(X0,k1_funct_1(k8_lopclset(X1),X2)) ) )
| ~ m1_subset_1(X2,u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ v17_lattices(X1)
| v3_realset2(X1)
| ~ l3_lattices(X1) ),
inference(nnf_transformation,[],[f12700]) ).
fof(f14212,plain,
! [X0,X1] :
( ! [X2] :
( ( ( r2_hidden(X0,k1_funct_1(k8_lopclset(X1),X2))
| ! [X3] :
( ~ m1_filter_0(X3,X1)
| X0 != X3
| ~ v1_filter_0(X3,X1)
| ~ r2_hidden(X2,X3) ) )
& ( ? [X4] :
( m1_filter_0(X4,X1)
& X0 = X4
& v1_filter_0(X4,X1)
& r2_hidden(X2,X4) )
| ~ r2_hidden(X0,k1_funct_1(k8_lopclset(X1),X2)) ) )
| ~ m1_subset_1(X2,u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ v17_lattices(X1)
| v3_realset2(X1)
| ~ l3_lattices(X1) ),
inference(rectify,[],[f14211]) ).
fof(f14213,plain,
! [X0,X1] :
( ! [X2] :
( ( ( r2_hidden(X0,k1_funct_1(k8_lopclset(X1),X2))
| ! [X3] :
( ~ m1_filter_0(X3,X1)
| X0 != X3
| ~ v1_filter_0(X3,X1)
| ~ r2_hidden(X2,X3) ) )
& ( ( m1_filter_0(sK71(X0,X1,X2),X1)
& sK71(X0,X1,X2) = X0
& v1_filter_0(sK71(X0,X1,X2),X1)
& r2_hidden(X2,sK71(X0,X1,X2)) )
| ~ r2_hidden(X0,k1_funct_1(k8_lopclset(X1),X2)) ) )
| ~ m1_subset_1(X2,u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ v17_lattices(X1)
| v3_realset2(X1)
| ~ l3_lattices(X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK71]),skolemize(X4,sK71(X0,X1,X2))],[f14212]) ).
fof(f14295,plain,
! [X0] :
( ! [X1,X2] :
( ( ( ( X2 = k1_funct_1(X0,X1)
| ~ r2_hidden(k4_tarski(X1,X2),X0) )
& ( r2_hidden(k4_tarski(X1,X2),X0)
| k1_funct_1(X0,X1) != X2 ) )
| ~ r2_hidden(X1,k1_relat_1(X0)) )
& ( ( ( X2 = k1_funct_1(X0,X1)
| k1_xboole_0 != X2 )
& ( X2 = k1_xboole_0
| k1_funct_1(X0,X1) != X2 ) )
| r2_hidden(X1,k1_relat_1(X0)) ) )
| ~ v1_relat_1(X0)
| ~ v1_funct_1(X0) ),
inference(nnf_transformation,[],[f12889]) ).
fof(f14443,plain,
! [X0,X1,X2] :
( ( m2_relset_1(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1) )
& ( m1_relset_1(X2,X0,X1)
| ~ m2_relset_1(X2,X0,X1) ) ),
inference(nnf_transformation,[],[f1394]) ).
fof(f14693,plain,
! [X0] :
( ! [X1] :
( ( ( X1 = k8_lopclset(X0)
| k1_relat_1(X1) != u1_struct_0(X0)
| ? [X2] :
( k1_funct_1(X1,X2) != a_2_0_lopclset(X0,X2)
& m1_subset_1(X2,u1_struct_0(X0)) ) )
& ( ( k1_relat_1(X1) = u1_struct_0(X0)
& ! [X2] :
( k1_funct_1(X1,X2) = a_2_0_lopclset(X0,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0)) ) )
| k8_lopclset(X0) != X1 ) )
| ~ v1_relat_1(X1)
| ~ v1_funct_1(X1) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f14084]) ).
fof(f14694,plain,
! [X0] :
( ! [X1] :
( ( ( X1 = k8_lopclset(X0)
| k1_relat_1(X1) != u1_struct_0(X0)
| ? [X2] :
( k1_funct_1(X1,X2) != a_2_0_lopclset(X0,X2)
& m1_subset_1(X2,u1_struct_0(X0)) ) )
& ( ( k1_relat_1(X1) = u1_struct_0(X0)
& ! [X2] :
( k1_funct_1(X1,X2) = a_2_0_lopclset(X0,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0)) ) )
| k8_lopclset(X0) != X1 ) )
| ~ v1_relat_1(X1)
| ~ v1_funct_1(X1) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f14693]) ).
fof(f14695,plain,
! [X0] :
( ! [X1] :
( ( ( X1 = k8_lopclset(X0)
| k1_relat_1(X1) != u1_struct_0(X0)
| ? [X2] :
( k1_funct_1(X1,X2) != a_2_0_lopclset(X0,X2)
& m1_subset_1(X2,u1_struct_0(X0)) ) )
& ( ( k1_relat_1(X1) = u1_struct_0(X0)
& ! [X3] :
( k1_funct_1(X1,X3) = a_2_0_lopclset(X0,X3)
| ~ m1_subset_1(X3,u1_struct_0(X0)) ) )
| k8_lopclset(X0) != X1 ) )
| ~ v1_relat_1(X1)
| ~ v1_funct_1(X1) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(rectify,[],[f14694]) ).
fof(f14696,plain,
! [X0] :
( ! [X1] :
( ( ( X1 = k8_lopclset(X0)
| k1_relat_1(X1) != u1_struct_0(X0)
| ( k1_funct_1(X1,sK356(X0,X1)) != a_2_0_lopclset(X0,sK356(X0,X1))
& m1_subset_1(sK356(X0,X1),u1_struct_0(X0)) ) )
& ( ( k1_relat_1(X1) = u1_struct_0(X0)
& ! [X3] :
( k1_funct_1(X1,X3) = a_2_0_lopclset(X0,X3)
| ~ m1_subset_1(X3,u1_struct_0(X0)) ) )
| k8_lopclset(X0) != X1 ) )
| ~ v1_relat_1(X1)
| ~ v1_funct_1(X1) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK356]),skolemize(X2,sK356(X0,X1))],[f14695]) ).
fof(f14697,plain,
l3_lattices(sK28),
inference(cnf_transformation,[],[f14139]) ).
fof(f14698,plain,
~ v3_realset2(sK28),
inference(cnf_transformation,[],[f14139]) ).
fof(f14699,plain,
v17_lattices(sK28),
inference(cnf_transformation,[],[f14139]) ).
fof(f14700,plain,
v10_lattices(sK28),
inference(cnf_transformation,[],[f14139]) ).
fof(f14701,plain,
~ v3_struct_0(sK28),
inference(cnf_transformation,[],[f14139]) ).
fof(f14702,plain,
m1_subset_1(sK29,u1_struct_0(sK28)),
inference(cnf_transformation,[],[f14139]) ).
fof(f14703,plain,
m1_filter_0(sK30,sK28),
inference(cnf_transformation,[],[f14139]) ).
fof(f14704,plain,
r2_hidden(sK29,sK30),
inference(cnf_transformation,[],[f14139]) ).
fof(f14705,plain,
~ r2_hidden(sK30,k8_funct_2(u1_struct_0(sK28),k1_zfmisc_1(k7_lopclset(sK28)),k9_lopclset(sK28),sK29)),
inference(cnf_transformation,[],[f14139]) ).
fof(f14706,plain,
v1_filter_0(sK30,sK28),
inference(cnf_transformation,[],[f14139]) ).
fof(f14765,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| ~ v1_xboole_0(X1) ),
inference(cnf_transformation,[],[f12605]) ).
fof(f14766,plain,
! [X2,X0] :
( ~ r2_hidden(X2,X0)
| k1_xboole_0 != X0 ),
inference(cnf_transformation,[],[f14162]) ).
fof(f14804,plain,
! [X2,X3,X0,X1] :
( k1_funct_1(X2,X3) = k8_funct_2(X0,X1,X2,X3)
| v1_xboole_0(X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1)
| ~ m1_subset_1(X3,X0) ),
inference(cnf_transformation,[],[f12630]) ).
fof(f14909,plain,
! [X2,X3,X0,X1] :
( r2_hidden(X0,k1_funct_1(k8_lopclset(X1),X2))
| ~ m1_filter_0(X3,X1)
| X0 != X3
| ~ v1_filter_0(X3,X1)
| ~ r2_hidden(X2,X3)
| ~ m1_subset_1(X2,u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ v17_lattices(X1)
| v3_realset2(X1)
| ~ l3_lattices(X1) ),
inference(cnf_transformation,[],[f14213]) ).
fof(f14944,plain,
! [X0] :
( m2_relset_1(k9_lopclset(X0),u1_struct_0(X0),k1_zfmisc_1(k7_lopclset(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f12722]) ).
fof(f14945,plain,
! [X0] :
( v1_funct_2(k9_lopclset(X0),u1_struct_0(X0),k1_zfmisc_1(k7_lopclset(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f12722]) ).
fof(f14946,plain,
! [X0] :
( v1_funct_1(k9_lopclset(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f12722]) ).
fof(f14949,plain,
! [X0] :
( k8_lopclset(X0) = k9_lopclset(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f12728]) ).
fof(f15182,plain,
! [X2,X0,X1] :
( k1_xboole_0 = X2
| k1_funct_1(X0,X1) != X2
| r2_hidden(X1,k1_relat_1(X0))
| ~ v1_relat_1(X0)
| ~ v1_funct_1(X0) ),
inference(cnf_transformation,[],[f14295]) ).
fof(f15229,plain,
k1_xboole_0 = np__0,
inference(cnf_transformation,[],[f3551]) ).
fof(f15856,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f14443]) ).
fof(f17063,plain,
! [X0,X1] :
( k1_relat_1(X1) = u1_struct_0(X0)
| k8_lopclset(X0) != X1
| ~ v1_relat_1(X1)
| ~ v1_funct_1(X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f14696]) ).
fof(f17067,plain,
! [X0] :
( v1_funct_1(k8_lopclset(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f14088]) ).
fof(f17068,plain,
! [X0] :
( v1_relat_1(k8_lopclset(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f14088]) ).
fof(f17081,plain,
! [X2,X0] :
( ~ r2_hidden(X2,X0)
| np__0 != X0 ),
inference(definition_unfolding,[],[f14766,f15229]) ).
fof(f17190,plain,
! [X2,X0,X1] :
( np__0 = X2
| k1_funct_1(X0,X1) != X2
| r2_hidden(X1,k1_relat_1(X0))
| ~ v1_relat_1(X0)
| ~ v1_funct_1(X0) ),
inference(definition_unfolding,[],[f15182,f15229]) ).
fof(f17510,plain,
! [X2] : ~ r2_hidden(X2,np__0),
inference(equality_resolution,[],[f17081]) ).
fof(f17511,plain,
! [X2,X3,X1] :
( r2_hidden(X3,k1_funct_1(k8_lopclset(X1),X2))
| ~ m1_filter_0(X3,X1)
| ~ v1_filter_0(X3,X1)
| ~ r2_hidden(X2,X3)
| ~ m1_subset_1(X2,u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ v17_lattices(X1)
| v3_realset2(X1)
| ~ l3_lattices(X1) ),
inference(equality_resolution,[],[f14909]) ).
fof(f17545,plain,
! [X0,X1] :
( k1_funct_1(X0,X1) = np__0
| r2_hidden(X1,k1_relat_1(X0))
| ~ v1_relat_1(X0)
| ~ v1_funct_1(X0) ),
inference(equality_resolution,[],[f17190]) ).
fof(f17718,plain,
! [X0] :
( u1_struct_0(X0) = k1_relat_1(k8_lopclset(X0))
| ~ v1_relat_1(k8_lopclset(X0))
| ~ v1_funct_1(k8_lopclset(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(equality_resolution,[],[f17063]) ).
fof(f17818,definition,
( spl357_3
<=> v1_xboole_0(u1_struct_0(sK28)) ),
introduced(definition,[new_symbols(definition,[spl357_3])],[avatar_definition]) ).
fof(f17819,plain,
( ~ v1_xboole_0(u1_struct_0(sK28))
| spl357_3 ),
inference(avatar_component_clause,[],[f17818]) ).
fof(f17820,plain,
( v1_xboole_0(u1_struct_0(sK28))
| ~ spl357_3 ),
inference(avatar_component_clause,[],[f17818]) ).
fof(f17856,plain,
( ~ r2_hidden(sK30,k1_funct_1(k9_lopclset(sK28),sK29))
| v1_xboole_0(u1_struct_0(sK28))
| ~ v1_funct_1(k9_lopclset(sK28))
| ~ v1_funct_2(k9_lopclset(sK28),u1_struct_0(sK28),k1_zfmisc_1(k7_lopclset(sK28)))
| ~ m1_relset_1(k9_lopclset(sK28),u1_struct_0(sK28),k1_zfmisc_1(k7_lopclset(sK28)))
| ~ m1_subset_1(sK29,u1_struct_0(sK28)) ),
inference(superposition,[],[f14705,f14804]) ).
fof(f17861,plain,
( ~ r2_hidden(sK30,k1_funct_1(k9_lopclset(sK28),sK29))
| ~ v1_funct_1(k9_lopclset(sK28))
| ~ v1_funct_2(k9_lopclset(sK28),u1_struct_0(sK28),k1_zfmisc_1(k7_lopclset(sK28)))
| ~ m1_relset_1(k9_lopclset(sK28),u1_struct_0(sK28),k1_zfmisc_1(k7_lopclset(sK28)))
| ~ m1_subset_1(sK29,u1_struct_0(sK28))
| spl357_3 ),
inference(forward_subsumption_resolution,[],[f17856,f17819]) ).
fof(f17866,plain,
( ~ r2_hidden(sK30,k1_funct_1(k9_lopclset(sK28),sK29))
| ~ v1_funct_1(k9_lopclset(sK28))
| ~ v1_funct_2(k9_lopclset(sK28),u1_struct_0(sK28),k1_zfmisc_1(k7_lopclset(sK28)))
| ~ m1_relset_1(k9_lopclset(sK28),u1_struct_0(sK28),k1_zfmisc_1(k7_lopclset(sK28)))
| spl357_3 ),
inference(forward_subsumption_resolution,[],[f17861,f14702]) ).
fof(f17872,definition,
( spl357_9
<=> m1_relset_1(k9_lopclset(sK28),u1_struct_0(sK28),k1_zfmisc_1(k7_lopclset(sK28))) ),
introduced(definition,[new_symbols(definition,[spl357_9])],[avatar_definition]) ).
fof(f17874,plain,
( ~ m1_relset_1(k9_lopclset(sK28),u1_struct_0(sK28),k1_zfmisc_1(k7_lopclset(sK28)))
| spl357_9 ),
inference(avatar_component_clause,[],[f17872]) ).
fof(f17876,definition,
( spl357_10
<=> v1_funct_2(k9_lopclset(sK28),u1_struct_0(sK28),k1_zfmisc_1(k7_lopclset(sK28))) ),
introduced(definition,[new_symbols(definition,[spl357_10])],[avatar_definition]) ).
fof(f17878,plain,
( ~ v1_funct_2(k9_lopclset(sK28),u1_struct_0(sK28),k1_zfmisc_1(k7_lopclset(sK28)))
| spl357_10 ),
inference(avatar_component_clause,[],[f17876]) ).
fof(f17880,definition,
( spl357_11
<=> v1_funct_1(k9_lopclset(sK28)) ),
introduced(definition,[new_symbols(definition,[spl357_11])],[avatar_definition]) ).
fof(f17881,plain,
( v1_funct_1(k9_lopclset(sK28))
| ~ spl357_11 ),
inference(avatar_component_clause,[],[f17880]) ).
fof(f17882,plain,
( ~ v1_funct_1(k9_lopclset(sK28))
| spl357_11 ),
inference(avatar_component_clause,[],[f17880]) ).
fof(f17884,definition,
( spl357_12
<=> r2_hidden(sK30,k1_funct_1(k9_lopclset(sK28),sK29)) ),
introduced(definition,[new_symbols(definition,[spl357_12])],[avatar_definition]) ).
fof(f17885,plain,
( r2_hidden(sK30,k1_funct_1(k9_lopclset(sK28),sK29))
| ~ spl357_12 ),
inference(avatar_component_clause,[],[f17884]) ).
fof(f17886,plain,
( ~ r2_hidden(sK30,k1_funct_1(k9_lopclset(sK28),sK29))
| spl357_12 ),
inference(avatar_component_clause,[],[f17884]) ).
fof(f17887,plain,
( ~ spl357_9
| ~ spl357_10
| ~ spl357_11
| ~ spl357_12
| spl357_3 ),
inference(avatar_split_clause,[],[f17866,f17818,f17884,f17880,f17876,f17872]) ).
fof(f17891,definition,
( spl357_13
<=> m2_relset_1(k9_lopclset(sK28),u1_struct_0(sK28),k1_zfmisc_1(k7_lopclset(sK28))) ),
introduced(definition,[new_symbols(definition,[spl357_13])],[avatar_definition]) ).
fof(f17892,plain,
( m2_relset_1(k9_lopclset(sK28),u1_struct_0(sK28),k1_zfmisc_1(k7_lopclset(sK28)))
| ~ spl357_13 ),
inference(avatar_component_clause,[],[f17891]) ).
fof(f17893,plain,
( ~ m2_relset_1(k9_lopclset(sK28),u1_struct_0(sK28),k1_zfmisc_1(k7_lopclset(sK28)))
| spl357_13 ),
inference(avatar_component_clause,[],[f17891]) ).
fof(f17905,plain,
( v3_struct_0(sK28)
| ~ v10_lattices(sK28)
| ~ v17_lattices(sK28)
| v3_realset2(sK28)
| ~ l3_lattices(sK28)
| spl357_11 ),
inference(resolution,[],[f17882,f14946]) ).
fof(f17909,plain,
( ~ v10_lattices(sK28)
| ~ v17_lattices(sK28)
| v3_realset2(sK28)
| ~ l3_lattices(sK28)
| spl357_11 ),
inference(forward_subsumption_resolution,[],[f17905,f14701]) ).
fof(f17911,plain,
( ~ v17_lattices(sK28)
| v3_realset2(sK28)
| ~ l3_lattices(sK28)
| spl357_11 ),
inference(forward_subsumption_resolution,[],[f17909,f14700]) ).
fof(f17913,plain,
( v3_realset2(sK28)
| ~ l3_lattices(sK28)
| spl357_11 ),
inference(forward_subsumption_resolution,[],[f17911,f14699]) ).
fof(f17915,plain,
( ~ l3_lattices(sK28)
| spl357_11 ),
inference(forward_subsumption_resolution,[],[f17913,f14698]) ).
fof(f17917,plain,
( $false
| spl357_11 ),
inference(forward_subsumption_resolution,[],[f17915,f14697]) ).
fof(f17918,plain,
spl357_11,
inference(avatar_contradiction_clause,[],[f17917]) ).
fof(f17977,plain,
( ~ r2_hidden(sK30,k1_funct_1(k8_lopclset(sK28),sK29))
| v3_struct_0(sK28)
| ~ v10_lattices(sK28)
| ~ v17_lattices(sK28)
| v3_realset2(sK28)
| ~ l3_lattices(sK28)
| spl357_12 ),
inference(superposition,[],[f17886,f14949]) ).
fof(f17980,plain,
( ~ r2_hidden(sK30,k1_funct_1(k8_lopclset(sK28),sK29))
| ~ v10_lattices(sK28)
| ~ v17_lattices(sK28)
| v3_realset2(sK28)
| ~ l3_lattices(sK28)
| spl357_12 ),
inference(forward_subsumption_resolution,[],[f17977,f14701]) ).
fof(f17981,plain,
( ~ r2_hidden(sK30,k1_funct_1(k8_lopclset(sK28),sK29))
| ~ v17_lattices(sK28)
| v3_realset2(sK28)
| ~ l3_lattices(sK28)
| spl357_12 ),
inference(forward_subsumption_resolution,[],[f17980,f14700]) ).
fof(f17982,plain,
( ~ r2_hidden(sK30,k1_funct_1(k8_lopclset(sK28),sK29))
| v3_realset2(sK28)
| ~ l3_lattices(sK28)
| spl357_12 ),
inference(forward_subsumption_resolution,[],[f17981,f14699]) ).
fof(f17983,plain,
( ~ r2_hidden(sK30,k1_funct_1(k8_lopclset(sK28),sK29))
| ~ l3_lattices(sK28)
| spl357_12 ),
inference(forward_subsumption_resolution,[],[f17982,f14698]) ).
fof(f17984,plain,
( ~ r2_hidden(sK30,k1_funct_1(k8_lopclset(sK28),sK29))
| spl357_12 ),
inference(forward_subsumption_resolution,[],[f17983,f14697]) ).
fof(f17999,plain,
( v3_struct_0(sK28)
| ~ v10_lattices(sK28)
| ~ v17_lattices(sK28)
| v3_realset2(sK28)
| ~ l3_lattices(sK28)
| spl357_10 ),
inference(resolution,[],[f17878,f14945]) ).
fof(f18009,plain,
( ~ v10_lattices(sK28)
| ~ v17_lattices(sK28)
| v3_realset2(sK28)
| ~ l3_lattices(sK28)
| spl357_10 ),
inference(forward_subsumption_resolution,[],[f17999,f14701]) ).
fof(f18020,plain,
( ~ v17_lattices(sK28)
| v3_realset2(sK28)
| ~ l3_lattices(sK28)
| spl357_10 ),
inference(forward_subsumption_resolution,[],[f18009,f14700]) ).
fof(f18023,plain,
( v3_realset2(sK28)
| ~ l3_lattices(sK28)
| spl357_10 ),
inference(forward_subsumption_resolution,[],[f18020,f14699]) ).
fof(f18025,plain,
( ~ l3_lattices(sK28)
| spl357_10 ),
inference(forward_subsumption_resolution,[],[f18023,f14698]) ).
fof(f18027,plain,
( $false
| spl357_10 ),
inference(forward_subsumption_resolution,[],[f18025,f14697]) ).
fof(f18028,plain,
spl357_10,
inference(avatar_contradiction_clause,[],[f18027]) ).
fof(f18046,plain,
( ~ m1_filter_0(sK30,sK28)
| ~ v1_filter_0(sK30,sK28)
| ~ r2_hidden(sK29,sK30)
| ~ m1_subset_1(sK29,u1_struct_0(sK28))
| v3_struct_0(sK28)
| ~ v10_lattices(sK28)
| ~ v17_lattices(sK28)
| v3_realset2(sK28)
| ~ l3_lattices(sK28)
| spl357_12 ),
inference(resolution,[],[f17984,f17511]) ).
fof(f18051,plain,
( ~ v1_filter_0(sK30,sK28)
| ~ r2_hidden(sK29,sK30)
| ~ m1_subset_1(sK29,u1_struct_0(sK28))
| v3_struct_0(sK28)
| ~ v10_lattices(sK28)
| ~ v17_lattices(sK28)
| v3_realset2(sK28)
| ~ l3_lattices(sK28)
| spl357_12 ),
inference(forward_subsumption_resolution,[],[f18046,f14703]) ).
fof(f18053,plain,
( ~ r2_hidden(sK29,sK30)
| ~ m1_subset_1(sK29,u1_struct_0(sK28))
| v3_struct_0(sK28)
| ~ v10_lattices(sK28)
| ~ v17_lattices(sK28)
| v3_realset2(sK28)
| ~ l3_lattices(sK28)
| spl357_12 ),
inference(forward_subsumption_resolution,[],[f18051,f14706]) ).
fof(f18055,plain,
( ~ m1_subset_1(sK29,u1_struct_0(sK28))
| v3_struct_0(sK28)
| ~ v10_lattices(sK28)
| ~ v17_lattices(sK28)
| v3_realset2(sK28)
| ~ l3_lattices(sK28)
| spl357_12 ),
inference(forward_subsumption_resolution,[],[f18053,f14704]) ).
fof(f18057,plain,
( v3_struct_0(sK28)
| ~ v10_lattices(sK28)
| ~ v17_lattices(sK28)
| v3_realset2(sK28)
| ~ l3_lattices(sK28)
| spl357_12 ),
inference(forward_subsumption_resolution,[],[f18055,f14702]) ).
fof(f18059,plain,
( ~ v10_lattices(sK28)
| ~ v17_lattices(sK28)
| v3_realset2(sK28)
| ~ l3_lattices(sK28)
| spl357_12 ),
inference(forward_subsumption_resolution,[],[f18057,f14701]) ).
fof(f18061,plain,
( ~ v17_lattices(sK28)
| v3_realset2(sK28)
| ~ l3_lattices(sK28)
| spl357_12 ),
inference(forward_subsumption_resolution,[],[f18059,f14700]) ).
fof(f18063,plain,
( v3_realset2(sK28)
| ~ l3_lattices(sK28)
| spl357_12 ),
inference(forward_subsumption_resolution,[],[f18061,f14699]) ).
fof(f18065,plain,
( ~ l3_lattices(sK28)
| spl357_12 ),
inference(forward_subsumption_resolution,[],[f18063,f14698]) ).
fof(f18068,plain,
( $false
| spl357_12 ),
inference(forward_subsumption_resolution,[],[f18065,f14697]) ).
fof(f18069,plain,
spl357_12,
inference(avatar_contradiction_clause,[],[f18068]) ).
fof(f18079,plain,
( r2_hidden(sK30,np__0)
| r2_hidden(sK29,k1_relat_1(k9_lopclset(sK28)))
| ~ v1_relat_1(k9_lopclset(sK28))
| ~ v1_funct_1(k9_lopclset(sK28))
| ~ spl357_12 ),
inference(superposition,[],[f17885,f17545]) ).
fof(f18082,plain,
( r2_hidden(sK29,k1_relat_1(k9_lopclset(sK28)))
| ~ v1_relat_1(k9_lopclset(sK28))
| ~ v1_funct_1(k9_lopclset(sK28))
| ~ spl357_12 ),
inference(forward_subsumption_resolution,[],[f18079,f17510]) ).
fof(f18093,plain,
( r2_hidden(sK29,k1_relat_1(k9_lopclset(sK28)))
| ~ v1_relat_1(k9_lopclset(sK28))
| ~ spl357_11
| ~ spl357_12 ),
inference(forward_subsumption_resolution,[],[f18082,f17881]) ).
fof(f18096,definition,
( spl357_23
<=> v1_relat_1(k9_lopclset(sK28)) ),
introduced(definition,[new_symbols(definition,[spl357_23])],[avatar_definition]) ).
fof(f18098,plain,
( ~ v1_relat_1(k9_lopclset(sK28))
| spl357_23 ),
inference(avatar_component_clause,[],[f18096]) ).
fof(f18100,definition,
( spl357_24
<=> r2_hidden(sK29,k1_relat_1(k9_lopclset(sK28))) ),
introduced(definition,[new_symbols(definition,[spl357_24])],[avatar_definition]) ).
fof(f18102,plain,
( r2_hidden(sK29,k1_relat_1(k9_lopclset(sK28)))
| ~ spl357_24 ),
inference(avatar_component_clause,[],[f18100]) ).
fof(f18104,plain,
( ~ spl357_23
| spl357_24
| ~ spl357_11
| ~ spl357_12 ),
inference(avatar_split_clause,[],[f18093,f17884,f17880,f18100,f18096]) ).
fof(f18109,plain,
( ~ v1_relat_1(k8_lopclset(sK28))
| v3_struct_0(sK28)
| ~ v10_lattices(sK28)
| ~ v17_lattices(sK28)
| v3_realset2(sK28)
| ~ l3_lattices(sK28)
| spl357_23 ),
inference(superposition,[],[f18098,f14949]) ).
fof(f18110,plain,
( ~ v1_relat_1(k8_lopclset(sK28))
| ~ v10_lattices(sK28)
| ~ v17_lattices(sK28)
| v3_realset2(sK28)
| ~ l3_lattices(sK28)
| spl357_23 ),
inference(forward_subsumption_resolution,[],[f18109,f14701]) ).
fof(f18111,plain,
( ~ v1_relat_1(k8_lopclset(sK28))
| ~ v17_lattices(sK28)
| v3_realset2(sK28)
| ~ l3_lattices(sK28)
| spl357_23 ),
inference(forward_subsumption_resolution,[],[f18110,f14700]) ).
fof(f18112,plain,
( ~ v1_relat_1(k8_lopclset(sK28))
| v3_realset2(sK28)
| ~ l3_lattices(sK28)
| spl357_23 ),
inference(forward_subsumption_resolution,[],[f18111,f14699]) ).
fof(f18113,plain,
( ~ v1_relat_1(k8_lopclset(sK28))
| ~ l3_lattices(sK28)
| spl357_23 ),
inference(forward_subsumption_resolution,[],[f18112,f14698]) ).
fof(f18114,plain,
( ~ v1_relat_1(k8_lopclset(sK28))
| spl357_23 ),
inference(forward_subsumption_resolution,[],[f18113,f14697]) ).
fof(f18115,plain,
( v3_struct_0(sK28)
| ~ v10_lattices(sK28)
| ~ v17_lattices(sK28)
| v3_realset2(sK28)
| ~ l3_lattices(sK28)
| spl357_13 ),
inference(resolution,[],[f17893,f14944]) ).
fof(f18143,plain,
( ~ v10_lattices(sK28)
| ~ v17_lattices(sK28)
| v3_realset2(sK28)
| ~ l3_lattices(sK28)
| spl357_13 ),
inference(forward_subsumption_resolution,[],[f18115,f14701]) ).
fof(f18146,plain,
( ~ v17_lattices(sK28)
| v3_realset2(sK28)
| ~ l3_lattices(sK28)
| spl357_13 ),
inference(forward_subsumption_resolution,[],[f18143,f14700]) ).
fof(f18149,plain,
( v3_realset2(sK28)
| ~ l3_lattices(sK28)
| spl357_13 ),
inference(forward_subsumption_resolution,[],[f18146,f14699]) ).
fof(f18151,plain,
( ~ l3_lattices(sK28)
| spl357_13 ),
inference(forward_subsumption_resolution,[],[f18149,f14698]) ).
fof(f18153,plain,
( $false
| spl357_13 ),
inference(forward_subsumption_resolution,[],[f18151,f14697]) ).
fof(f18154,plain,
spl357_13,
inference(avatar_contradiction_clause,[],[f18153]) ).
fof(f18180,plain,
( m1_relset_1(k9_lopclset(sK28),u1_struct_0(sK28),k1_zfmisc_1(k7_lopclset(sK28)))
| ~ spl357_13 ),
inference(resolution,[],[f17892,f15856]) ).
fof(f18193,plain,
( $false
| spl357_9
| ~ spl357_13 ),
inference(forward_subsumption_resolution,[],[f18180,f17874]) ).
fof(f18194,plain,
( spl357_9
| ~ spl357_13 ),
inference(avatar_contradiction_clause,[],[f18193]) ).
fof(f18258,plain,
( v3_struct_0(sK28)
| ~ v10_lattices(sK28)
| ~ v17_lattices(sK28)
| v3_realset2(sK28)
| ~ l3_lattices(sK28)
| spl357_23 ),
inference(resolution,[],[f18114,f17068]) ).
fof(f18260,plain,
( ~ v10_lattices(sK28)
| ~ v17_lattices(sK28)
| v3_realset2(sK28)
| ~ l3_lattices(sK28)
| spl357_23 ),
inference(forward_subsumption_resolution,[],[f18258,f14701]) ).
fof(f18261,plain,
( ~ v17_lattices(sK28)
| v3_realset2(sK28)
| ~ l3_lattices(sK28)
| spl357_23 ),
inference(forward_subsumption_resolution,[],[f18260,f14700]) ).
fof(f18262,plain,
( v3_realset2(sK28)
| ~ l3_lattices(sK28)
| spl357_23 ),
inference(forward_subsumption_resolution,[],[f18261,f14699]) ).
fof(f18263,plain,
( ~ l3_lattices(sK28)
| spl357_23 ),
inference(forward_subsumption_resolution,[],[f18262,f14698]) ).
fof(f18264,plain,
( $false
| spl357_23 ),
inference(forward_subsumption_resolution,[],[f18263,f14697]) ).
fof(f18265,plain,
spl357_23,
inference(avatar_contradiction_clause,[],[f18264]) ).
fof(f18393,plain,
( ~ v1_xboole_0(k1_relat_1(k9_lopclset(sK28)))
| ~ spl357_24 ),
inference(resolution,[],[f18102,f14765]) ).
fof(f18417,plain,
( ~ v1_xboole_0(k1_relat_1(k8_lopclset(sK28)))
| v3_struct_0(sK28)
| ~ v10_lattices(sK28)
| ~ v17_lattices(sK28)
| v3_realset2(sK28)
| ~ l3_lattices(sK28)
| ~ spl357_24 ),
inference(superposition,[],[f18393,f14949]) ).
fof(f18421,plain,
( ~ v1_xboole_0(k1_relat_1(k8_lopclset(sK28)))
| ~ v10_lattices(sK28)
| ~ v17_lattices(sK28)
| v3_realset2(sK28)
| ~ l3_lattices(sK28)
| ~ spl357_24 ),
inference(forward_subsumption_resolution,[],[f18417,f14701]) ).
fof(f18423,plain,
( ~ v1_xboole_0(k1_relat_1(k8_lopclset(sK28)))
| ~ v17_lattices(sK28)
| v3_realset2(sK28)
| ~ l3_lattices(sK28)
| ~ spl357_24 ),
inference(forward_subsumption_resolution,[],[f18421,f14700]) ).
fof(f18424,plain,
( ~ v1_xboole_0(k1_relat_1(k8_lopclset(sK28)))
| v3_realset2(sK28)
| ~ l3_lattices(sK28)
| ~ spl357_24 ),
inference(forward_subsumption_resolution,[],[f18423,f14699]) ).
fof(f18425,plain,
( ~ v1_xboole_0(k1_relat_1(k8_lopclset(sK28)))
| ~ l3_lattices(sK28)
| ~ spl357_24 ),
inference(forward_subsumption_resolution,[],[f18424,f14698]) ).
fof(f18426,plain,
( ~ v1_xboole_0(k1_relat_1(k8_lopclset(sK28)))
| ~ spl357_24 ),
inference(forward_subsumption_resolution,[],[f18425,f14697]) ).
fof(f18447,plain,
( ~ v1_xboole_0(u1_struct_0(sK28))
| ~ v1_relat_1(k8_lopclset(sK28))
| ~ v1_funct_1(k8_lopclset(sK28))
| v3_struct_0(sK28)
| ~ v10_lattices(sK28)
| ~ v17_lattices(sK28)
| v3_realset2(sK28)
| ~ l3_lattices(sK28)
| ~ spl357_24 ),
inference(superposition,[],[f18426,f17718]) ).
fof(f18452,definition,
( spl357_33
<=> v1_funct_1(k8_lopclset(sK28)) ),
introduced(definition,[new_symbols(definition,[spl357_33])],[avatar_definition]) ).
fof(f18454,plain,
( ~ v1_funct_1(k8_lopclset(sK28))
| spl357_33 ),
inference(avatar_component_clause,[],[f18452]) ).
fof(f18456,definition,
( spl357_34
<=> v1_relat_1(k8_lopclset(sK28)) ),
introduced(definition,[new_symbols(definition,[spl357_34])],[avatar_definition]) ).
fof(f18458,plain,
( ~ v1_relat_1(k8_lopclset(sK28))
| spl357_34 ),
inference(avatar_component_clause,[],[f18456]) ).
fof(f18463,plain,
( ~ v1_relat_1(k8_lopclset(sK28))
| ~ v1_funct_1(k8_lopclset(sK28))
| v3_struct_0(sK28)
| ~ v10_lattices(sK28)
| ~ v17_lattices(sK28)
| v3_realset2(sK28)
| ~ l3_lattices(sK28)
| ~ spl357_3
| ~ spl357_24 ),
inference(forward_subsumption_resolution,[],[f18447,f17820]) ).
fof(f18469,plain,
( ~ v1_relat_1(k8_lopclset(sK28))
| ~ v1_funct_1(k8_lopclset(sK28))
| ~ v10_lattices(sK28)
| ~ v17_lattices(sK28)
| v3_realset2(sK28)
| ~ l3_lattices(sK28)
| ~ spl357_3
| ~ spl357_24 ),
inference(forward_subsumption_resolution,[],[f18463,f14701]) ).
fof(f18470,plain,
( ~ v1_relat_1(k8_lopclset(sK28))
| ~ v1_funct_1(k8_lopclset(sK28))
| ~ v17_lattices(sK28)
| v3_realset2(sK28)
| ~ l3_lattices(sK28)
| ~ spl357_3
| ~ spl357_24 ),
inference(forward_subsumption_resolution,[],[f18469,f14700]) ).
fof(f18471,plain,
( ~ v1_relat_1(k8_lopclset(sK28))
| ~ v1_funct_1(k8_lopclset(sK28))
| v3_realset2(sK28)
| ~ l3_lattices(sK28)
| ~ spl357_3
| ~ spl357_24 ),
inference(forward_subsumption_resolution,[],[f18470,f14699]) ).
fof(f18472,plain,
( ~ v1_relat_1(k8_lopclset(sK28))
| ~ v1_funct_1(k8_lopclset(sK28))
| ~ l3_lattices(sK28)
| ~ spl357_3
| ~ spl357_24 ),
inference(forward_subsumption_resolution,[],[f18471,f14698]) ).
fof(f18473,plain,
( ~ v1_relat_1(k8_lopclset(sK28))
| ~ v1_funct_1(k8_lopclset(sK28))
| ~ spl357_3
| ~ spl357_24 ),
inference(forward_subsumption_resolution,[],[f18472,f14697]) ).
fof(f18474,plain,
( ~ spl357_33
| ~ spl357_34
| ~ spl357_3
| ~ spl357_24 ),
inference(avatar_split_clause,[],[f18473,f18100,f17818,f18456,f18452]) ).
fof(f18533,plain,
( v3_struct_0(sK28)
| ~ v10_lattices(sK28)
| ~ v17_lattices(sK28)
| v3_realset2(sK28)
| ~ l3_lattices(sK28)
| spl357_33 ),
inference(resolution,[],[f18454,f17067]) ).
fof(f18535,plain,
( ~ v10_lattices(sK28)
| ~ v17_lattices(sK28)
| v3_realset2(sK28)
| ~ l3_lattices(sK28)
| spl357_33 ),
inference(forward_subsumption_resolution,[],[f18533,f14701]) ).
fof(f18536,plain,
( ~ v17_lattices(sK28)
| v3_realset2(sK28)
| ~ l3_lattices(sK28)
| spl357_33 ),
inference(forward_subsumption_resolution,[],[f18535,f14700]) ).
fof(f18537,plain,
( v3_realset2(sK28)
| ~ l3_lattices(sK28)
| spl357_33 ),
inference(forward_subsumption_resolution,[],[f18536,f14699]) ).
fof(f18538,plain,
( ~ l3_lattices(sK28)
| spl357_33 ),
inference(forward_subsumption_resolution,[],[f18537,f14698]) ).
fof(f18539,plain,
( $false
| spl357_33 ),
inference(forward_subsumption_resolution,[],[f18538,f14697]) ).
fof(f18540,plain,
spl357_33,
inference(avatar_contradiction_clause,[],[f18539]) ).
fof(f18664,plain,
( v3_struct_0(sK28)
| ~ v10_lattices(sK28)
| ~ v17_lattices(sK28)
| v3_realset2(sK28)
| ~ l3_lattices(sK28)
| spl357_34 ),
inference(resolution,[],[f18458,f17068]) ).
fof(f18666,plain,
( ~ v10_lattices(sK28)
| ~ v17_lattices(sK28)
| v3_realset2(sK28)
| ~ l3_lattices(sK28)
| spl357_34 ),
inference(forward_subsumption_resolution,[],[f18664,f14701]) ).
fof(f18667,plain,
( ~ v17_lattices(sK28)
| v3_realset2(sK28)
| ~ l3_lattices(sK28)
| spl357_34 ),
inference(forward_subsumption_resolution,[],[f18666,f14700]) ).
fof(f18668,plain,
( v3_realset2(sK28)
| ~ l3_lattices(sK28)
| spl357_34 ),
inference(forward_subsumption_resolution,[],[f18667,f14699]) ).
fof(f18669,plain,
( ~ l3_lattices(sK28)
| spl357_34 ),
inference(forward_subsumption_resolution,[],[f18668,f14698]) ).
fof(f18670,plain,
( $false
| spl357_34 ),
inference(forward_subsumption_resolution,[],[f18669,f14697]) ).
fof(f18671,plain,
spl357_34,
inference(avatar_contradiction_clause,[],[f18670]) ).
cnf(s7,plain,
( spl357_3
| ~ spl357_9
| ~ spl357_10
| ~ spl357_11
| ~ spl357_12 ),
inference(sat_conversion,[],[f17887]) ).
cnf(s10,plain,
spl357_11,
inference(sat_conversion,[],[f17918]) ).
cnf(s14,plain,
spl357_10,
inference(sat_conversion,[],[f18028]) ).
cnf(s16,plain,
spl357_12,
inference(sat_conversion,[],[f18069]) ).
cnf(s19,plain,
( ~ spl357_11
| ~ spl357_12
| ~ spl357_23
| spl357_24 ),
inference(sat_conversion,[],[f18104]) ).
cnf(s21,plain,
spl357_13,
inference(sat_conversion,[],[f18154]) ).
cnf(s28,plain,
( spl357_9
| ~ spl357_13 ),
inference(sat_conversion,[],[f18194]) ).
cnf(s30,plain,
spl357_23,
inference(sat_conversion,[],[f18265]) ).
cnf(s34,plain,
( ~ spl357_3
| ~ spl357_24
| ~ spl357_33
| ~ spl357_34 ),
inference(sat_conversion,[],[f18474]) ).
cnf(s37,plain,
spl357_33,
inference(sat_conversion,[],[f18540]) ).
cnf(s46,plain,
spl357_34,
inference(sat_conversion,[],[f18671]) ).
cnf(s47,plain,
( ~ spl357_3
| ~ spl357_24 ),
inference(rat,[],[s34,s46,s37]) ).
cnf(s50,plain,
spl357_9,
inference(rat,[],[s28,s21]) ).
cnf(s53,plain,
( ~ spl357_11
| ~ spl357_12
| spl357_24 ),
inference(rat,[],[s19,s30]) ).
cnf(s55,plain,
spl357_24,
inference(rat,[],[s53,s16,s10]) ).
cnf(s56,plain,
~ spl357_3,
inference(rat,[],[s47,s55]) ).
cnf(s60,plain,
$false,
inference(rat,[],[s7,s16,s10,s14,s50,s56]) ).
fof(f18672,plain,
$false,
inference(avatar_sat_refutation,[],[s60]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT289+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.39 % Computer : n020.cluster.edu
% 0.10/0.39 % Model : x86_64 x86_64
% 0.10/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.39 % Memory : 8046.5625MB
% 0.10/0.39 % OS : Linux 6.8.0-71-generic
% 0.10/0.39 % CPULimit : 300
% 0.10/0.39 % WCLimit : 300
% 0.10/0.39 % DateTime : Sun Sep 27 14:15:37 UTC 2026
% 0.10/0.39 % CPUTime :
% 0.10/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.42 Running first-order theorem proving
% 0.10/0.42 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
% 7.61/2.60 % (3416540)Detected formulas, will run a generic FOF schedule.
% 7.61/2.60 % (3416545)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=2723492359:i=141193_2993 on theBenchmark for (2993ds/141193Mi)
% 7.61/2.60 % (3416550)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1731213516:s2a=on:i=139:gtg=position_2993 on theBenchmark for (2993ds/139Mi)
% 7.61/2.60 % (3416549)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=785742975:i=119:av=off:ss=axioms_2993 on theBenchmark for (2993ds/119Mi)
% 7.61/2.60 % (3416546)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=767837706:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2993 on theBenchmark for (2993ds/134677Mi)
% 7.61/2.60 % (3416547)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=2455376493:i=141695:sd=1:nm=32:gsp=on:ss=included_2993 on theBenchmark for (2993ds/141695Mi)
% 7.61/2.60 % (3416548)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2738090204:i=109:sd=1:ins=1:gsp=on:ss=axioms_2993 on theBenchmark for (2993ds/109Mi)
% 7.61/2.60 % (3416551)dis-21_1_sil=8000:lcm=predicate:random_seed=1701394280: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)
% 7.61/2.60 % (3416550)Instruction limit reached!
% 7.61/2.60 % (3416550)------------------------------
% 7.61/2.60 % (3416550)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.61/2.60 % (3416550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.61/2.60 % (3416550)CaDiCaL version: 2.1.3
% 7.61/2.60 % (3416550)Termination reason: Instruction limit
% 7.61/2.60 % (3416550)Termination phase: Property scanning
% 7.61/2.60 % (3416550)Time elapsed: 0.058 s
% 7.61/2.60 % (3416550)Peak memory usage: 100 MB
% 7.61/2.60 % (3416550)Instructions burned: 140 (million)
% 7.61/2.60 % (3416548)Instruction limit reached!
% 7.61/2.60 % (3416548)------------------------------
% 7.61/2.60 % (3416548)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.61/2.60 % (3416548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.61/2.60 % (3416548)CaDiCaL version: 2.1.3
% 7.61/2.60 % (3416548)Termination reason: Instruction limit
% 7.61/2.60 % (3416548)Termination phase: Saturation
% 7.61/2.60 % (3416548)Time elapsed: 0.081 s
% 7.61/2.60 % (3416548)Peak memory usage: 105 MB
% 7.61/2.60 % (3416548)Instructions burned: 110 (million)
% 7.61/2.60 % (3416549)Instruction limit reached!
% 7.61/2.60 % (3416549)------------------------------
% 7.61/2.60 % (3416549)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.61/2.60 % (3416549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.61/2.60 % (3416549)CaDiCaL version: 2.1.3
% 7.61/2.60 % (3416549)Termination reason: Instruction limit
% 7.61/2.60 % (3416549)Termination phase: Saturation
% 7.61/2.60 % (3416549)Time elapsed: 0.083 s
% 7.61/2.60 % (3416549)Peak memory usage: 105 MB
% 7.61/2.60 % (3416549)Instructions burned: 119 (million)
% 7.61/2.60 % (3416551)Instruction limit reached!
% 7.61/2.60 % (3416551)------------------------------
% 7.61/2.60 % (3416551)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.61/2.60 % (3416551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.61/2.60 % (3416551)CaDiCaL version: 2.1.3
% 7.61/2.60 % (3416551)Termination reason: Instruction limit
% 7.61/2.60 % (3416551)Termination phase: Preprocessing 1
% 7.61/2.60 % (3416551)Time elapsed: 0.098 s
% 7.61/2.60 % (3416551)Peak memory usage: 102 MB
% 7.61/2.60 % (3416551)Instructions burned: 129 (million)
% 7.61/2.60 % (3416559)lrs+10_1_sil=8000:sp=occurrence:random_seed=4099215759:i=285:sd=3:ss=axioms:sgt=8_2991 on theBenchmark for (2991ds/285Mi)
% 7.61/2.60 % (3416561)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2739961622:i=325:sd=1:ss=axioms:sgt=32_2991 on theBenchmark for (2991ds/325Mi)
% 7.61/2.60 % (3416560)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1667116631:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2991 on theBenchmark for (2991ds/157Mi)
% 7.61/2.60 % (3416562)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=658438963:s2a=on:i=248:s2at=1.23:gtg=position_2991 on theBenchmark for (2991ds/248Mi)
% 7.61/2.60 % (3416560)Instruction limit reached!
% 7.61/2.60 % (3416560)------------------------------
% 7.61/2.60 % (3416560)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.61/2.60 % (3416560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.61/2.60 % (3416560)CaDiCaL version: 2.1.3
% 7.61/2.60 % (3416560)Termination reason: Instruction limit
% 7.61/2.60 % (3416560)Termination phase: SInE selection
% 7.61/2.60 % (3416560)Time elapsed: 0.069 s
% 7.61/2.60 % (3416560)Peak memory usage: 100 MB
% 7.61/2.60 % (3416560)Instructions burned: 157 (million)
% 7.61/2.60 % (3416562)Instruction limit reached!
% 7.61/2.60 % (3416562)------------------------------
% 7.61/2.60 % (3416562)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.61/2.60 % (3416562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.61/2.60 % (3416562)CaDiCaL version: 2.1.3
% 7.61/2.60 % (3416562)Termination reason: Instruction limit
% 7.61/2.60 % (3416562)Termination phase: SInE selection
% 7.61/2.60 % (3416562)Time elapsed: 0.138 s
% 7.61/2.60 % (3416562)Peak memory usage: 101 MB
% 7.61/2.60 % (3416562)Instructions burned: 248 (million)
% 7.61/2.60 % (3416559)Instruction limit reached!
% 7.61/2.60 % (3416559)------------------------------
% 7.61/2.60 % (3416559)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.61/2.60 % (3416559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.61/2.60 % (3416559)CaDiCaL version: 2.1.3
% 7.61/2.60 % (3416559)Termination reason: Instruction limit
% 7.61/2.60 % (3416559)Termination phase: Saturation
% 7.61/2.60 % (3416559)Time elapsed: 0.212 s
% 7.61/2.60 % (3416559)Peak memory usage: 108 MB
% 7.61/2.60 % (3416559)Instructions burned: 285 (million)
% 7.61/2.60 % (3416561)Instruction limit reached!
% 7.61/2.60 % (3416561)------------------------------
% 7.61/2.60 % (3416561)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.61/2.60 % (3416561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.61/2.60 % (3416561)CaDiCaL version: 2.1.3
% 7.61/2.60 % (3416561)Termination reason: Instruction limit
% 7.61/2.60 % (3416561)Termination phase: Saturation
% 7.61/2.60 % (3416561)Time elapsed: 0.232 s
% 7.61/2.60 % (3416561)Peak memory usage: 107 MB
% 7.61/2.60 % (3416561)Instructions burned: 326 (million)
% 7.61/2.60 % (3416567)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1163822944:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2989 on theBenchmark for (2989ds/294Mi)
% 7.61/2.60 % (3416568)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3855164664:i=2350_2988 on theBenchmark for (2988ds/2350Mi)
% 7.61/2.60 % (3416569)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1994637558:cts=off:i=113:fsr=off:ss=included:sgt=4_2987 on theBenchmark for (2987ds/113Mi)
% 7.61/2.60 % (3416570)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=525270759:i=127:av=off:fsr=off:sup=off_2987 on theBenchmark for (2987ds/127Mi)
% 7.61/2.60 % (3416567)First to succeed.
% 7.61/2.60 % (3416569)Instruction limit reached!
% 7.61/2.60 % (3416569)------------------------------
% 7.61/2.60 % (3416569)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.61/2.60 % (3416569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.61/2.60 % (3416569)CaDiCaL version: 2.1.3
% 7.61/2.60 % (3416569)Termination reason: Instruction limit
% 7.61/2.60 % (3416569)Termination phase: Preprocessing 3
% 7.61/2.60 % (3416569)Time elapsed: 0.091 s
% 7.61/2.60 % (3416569)Peak memory usage: 104 MB
% 7.61/2.60 % (3416569)Instructions burned: 113 (million)
% 7.61/2.60 % (3416567)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3416540"
% 7.61/2.60 % (3416570)Instruction limit reached!
% 7.61/2.60 % (3416570)------------------------------
% 7.61/2.60 % (3416570)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.61/2.60 % (3416570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.61/2.60 % (3416570)CaDiCaL version: 2.1.3
% 7.61/2.60 % (3416570)Termination reason: Instruction limit
% 7.61/2.60 % (3416570)Termination phase: Preprocessing 2
% 7.61/2.60 % (3416570)Time elapsed: 0.105 s
% 7.61/2.60 % (3416570)Peak memory usage: 107 MB
% 7.61/2.60 % (3416570)Instructions burned: 127 (million)
% 7.61/2.60 % (3416575)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1439271237:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2985 on theBenchmark for (2985ds/114Mi)
% 7.61/2.60 % (3416575)Instruction limit reached!
% 7.61/2.60 % (3416575)------------------------------
% 7.61/2.60 % (3416575)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.61/2.60 % (3416575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.61/2.60 % (3416575)CaDiCaL version: 2.1.3
% 7.61/2.60 % (3416575)Termination reason: Instruction limit
% 7.61/2.60 % (3416575)Termination phase: Property scanning
% 7.61/2.60 % (3416575)Time elapsed: 0.049 s
% 7.61/2.60 % (3416575)Peak memory usage: 101 MB
% 7.61/2.60 % (3416575)Instructions burned: 116 (million)
% 7.61/2.60 % (3416576)lrs+10_1_sil=8000:sp=occurrence:random_seed=3980941957:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2984 on theBenchmark for (2984ds/907Mi)
% 7.61/2.60 % (3416567)Refutation found. Thanks to Tanya!
% 7.61/2.60 % SZS status Theorem for theBenchmark
% 7.61/2.60 % SZS output start Proof for theBenchmark
% See solution above
% 9.08/2.75 % (3416567)------------------------------
% 9.08/2.75 % (3416567)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.08/2.75 % (3416567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.08/2.75 % (3416567)CaDiCaL version: 2.1.3
% 9.08/2.75 % (3416567)Termination reason: Refutation
% 9.08/2.75 % (3416567)Time elapsed: 0.190 s
% 9.08/2.75 % (3416567)Peak memory usage: 110 MB
% 9.08/2.75 % (3416567)Instructions burned: 285 (million)
% 9.08/2.75 % (3416567)------------------------------
% 9.08/2.75 % (3416567)------------------------------
% 9.08/2.75 % (3416540)Success in time 1.729 s
% 9.08/2.75 % Vampire exiting
%------------------------------------------------------------------------------