%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT320+4 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : 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:54 AM UTC 2026
% Result : Theorem 33.15s 9.84s
% Output : Refutation 50.46s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 21
% Syntax : Number of formulae : 166 ( 23 unt; 6 def)
% Number of atoms : 831 ( 53 equ)
% Maximal formula atoms : 19 ( 5 avg)
% Number of connectives : 1110 ( 445 ~; 483 |; 134 &)
% ( 21 <=>; 27 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 24 ( 22 usr; 7 prp; 0-3 aty)
% Number of functors : 13 ( 13 usr; 3 con; 0-3 aty)
% Number of variables : 181 ( 1 sgn 172 !; 9 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f18,axiom,
! [X0,X1] : r1_tarski(X0,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',reflexivity_r1_tarski) ).
fof(f18151,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l3_lattices(X0) )
=> ( v17_lattices(X0)
<=> ( v15_lattices(X0)
& v16_lattices(X0)
& v11_lattices(X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d20_lattices) ).
fof(f21600,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/sandbox2/benchmark/theBenchmark.p',dt_m1_filter_0) ).
fof(f22747,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l3_lattices(X0) )
=> ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_lattice2) ).
fof(f22780,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l3_lattices(X0) )
=> ( u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0))
& u2_lattices(X0) = u1_lattices(k1_lattice2(X0))
& u1_lattices(X0) = u2_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t18_lattice2) ).
fof(f22852,axiom,
! [X0] :
( l3_lattices(X0)
=> ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k1_lattice2) ).
fof(f34607,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_filter_2(X1,X0)
<=> m1_filter_0(X1,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_m1_filter_2) ).
fof(f34608,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_filter_2(X1,X0)
=> ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m2_filter_2) ).
fof(f34645,axiom,
! [X0,X1,X2] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v11_lattices(X0)
& l3_lattices(X0)
& m2_filter_2(X1,X0)
& m2_filter_2(X2,X0) )
=> m2_filter_2(k21_filter_2(X0,X1,X2),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k21_filter_2) ).
fof(f34646,axiom,
! [X0,X1,X2] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v11_lattices(X0)
& l3_lattices(X0)
& m2_filter_2(X1,X0)
& m2_filter_2(X2,X0) )
=> k21_filter_2(X0,X1,X2) = k20_filter_2(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k21_filter_2) ).
fof(f34676,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_filter_2(X1,X0)
<=> m1_filter_2(X1,k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t21_filter_2) ).
fof(f34699,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( ( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
=> ! [X2] :
( m2_filter_2(X2,X0)
=> ( X2 = k19_filter_2(X0,X1)
<=> ( r1_tarski(X1,X2)
& ! [X3] :
( m2_filter_2(X3,X0)
=> ( r1_tarski(X1,X3)
=> r1_tarski(X2,X3) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d11_filter_2) ).
fof(f34720,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_filter_2(X1,X0)
=> ! [X2] :
( m2_filter_2(X2,X0)
=> r1_filter_2(u1_struct_0(X0),k19_filter_2(X0,k4_subset_1(u1_struct_0(X0),X1,X2)),k19_filter_2(X0,k20_filter_2(X0,X1,X2))) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t52_filter_2) ).
fof(f34722,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) )
<=> ( ~ v3_struct_0(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v17_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t54_filter_2) ).
fof(f34726,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_filter_2(X1,X0)
=> ! [X2] :
( m2_filter_2(X2,X0)
=> r1_filter_2(u1_struct_0(X0),k19_filter_2(X0,k4_subset_1(u1_struct_0(X0),X1,X2)),k21_filter_2(X0,X1,X2)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t56_filter_2) ).
fof(f34727,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_filter_2(X1,X0)
=> ! [X2] :
( m2_filter_2(X2,X0)
=> r1_filter_2(u1_struct_0(X0),k19_filter_2(X0,k4_subset_1(u1_struct_0(X0),X1,X2)),k21_filter_2(X0,X1,X2)) ) ) ),
inference(negated_conjecture,[status(cth)],[f34726]) ).
fof(f34729,plain,
! [X0] : r1_tarski(X0,X0),
inference(rectify,[],[f18]) ).
fof(f35048,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ~ r1_filter_2(u1_struct_0(X0),k19_filter_2(X0,k4_subset_1(u1_struct_0(X0),X1,X2)),k21_filter_2(X0,X1,X2))
& m2_filter_2(X2,X0) )
& m2_filter_2(X1,X0) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) ),
inference(ennf_transformation,[],[f34727]) ).
fof(f35049,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ~ r1_filter_2(u1_struct_0(X0),k19_filter_2(X0,k4_subset_1(u1_struct_0(X0),X1,X2)),k21_filter_2(X0,X1,X2))
& m2_filter_2(X2,X0) )
& m2_filter_2(X1,X0) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) ),
inference(flattening,[],[f35048]) ).
fof(f35108,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( X2 = k19_filter_2(X0,X1)
<=> ( r1_tarski(X1,X2)
& ! [X3] :
( r1_tarski(X2,X3)
| ~ r1_tarski(X1,X3)
| ~ m2_filter_2(X3,X0) ) ) )
| ~ m2_filter_2(X2,X0) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f34699]) ).
fof(f35109,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( X2 = k19_filter_2(X0,X1)
<=> ( r1_tarski(X1,X2)
& ! [X3] :
( r1_tarski(X2,X3)
| ~ r1_tarski(X1,X3)
| ~ m2_filter_2(X3,X0) ) ) )
| ~ m2_filter_2(X2,X0) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35108]) ).
fof(f35134,plain,
! [X0] :
( ! [X1] :
( ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f34608]) ).
fof(f35135,plain,
! [X0] :
( ! [X1] :
( ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35134]) ).
fof(f35136,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( r1_filter_2(u1_struct_0(X0),k19_filter_2(X0,k4_subset_1(u1_struct_0(X0),X1,X2)),k19_filter_2(X0,k20_filter_2(X0,X1,X2)))
| ~ m2_filter_2(X2,X0) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f34720]) ).
fof(f35137,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( r1_filter_2(u1_struct_0(X0),k19_filter_2(X0,k4_subset_1(u1_struct_0(X0),X1,X2)),k19_filter_2(X0,k20_filter_2(X0,X1,X2)))
| ~ m2_filter_2(X2,X0) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35136]) ).
fof(f35161,plain,
! [X0,X1,X2] :
( k21_filter_2(X0,X1,X2) = k20_filter_2(X0,X1,X2)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v11_lattices(X0)
| ~ l3_lattices(X0)
| ~ m2_filter_2(X1,X0)
| ~ m2_filter_2(X2,X0) ),
inference(ennf_transformation,[],[f34646]) ).
fof(f35162,plain,
! [X0,X1,X2] :
( k21_filter_2(X0,X1,X2) = k20_filter_2(X0,X1,X2)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v11_lattices(X0)
| ~ l3_lattices(X0)
| ~ m2_filter_2(X1,X0)
| ~ m2_filter_2(X2,X0) ),
inference(flattening,[],[f35161]) ).
fof(f35163,plain,
! [X0,X1,X2] :
( m2_filter_2(k21_filter_2(X0,X1,X2),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v11_lattices(X0)
| ~ l3_lattices(X0)
| ~ m2_filter_2(X1,X0)
| ~ m2_filter_2(X2,X0) ),
inference(ennf_transformation,[],[f34645]) ).
fof(f35164,plain,
! [X0,X1,X2] :
( m2_filter_2(k21_filter_2(X0,X1,X2),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v11_lattices(X0)
| ~ l3_lattices(X0)
| ~ m2_filter_2(X1,X0)
| ~ m2_filter_2(X2,X0) ),
inference(flattening,[],[f35163]) ).
fof(f36543,plain,
! [X0] :
( ( u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0))
& u2_lattices(X0) = u1_lattices(k1_lattice2(X0))
& u1_lattices(X0) = u2_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f22780]) ).
fof(f36544,plain,
! [X0] :
( ( u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0))
& u2_lattices(X0) = u1_lattices(k1_lattice2(X0))
& u1_lattices(X0) = u2_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f36543]) ).
fof(f37578,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,[],[f21600]) ).
fof(f37579,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,[],[f37578]) ).
fof(f42464,plain,
! [X0] :
( ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) )
<=> ( ~ v3_struct_0(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v17_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f34722]) ).
fof(f42465,plain,
! [X0] :
( ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) )
<=> ( ~ v3_struct_0(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v17_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f42464]) ).
fof(f42470,plain,
! [X0] :
( ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f22852]) ).
fof(f42479,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f22747]) ).
fof(f42480,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f42479]) ).
fof(f42587,plain,
! [X0] :
( ( v17_lattices(X0)
<=> ( v15_lattices(X0)
& v16_lattices(X0)
& v11_lattices(X0) ) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f18151]) ).
fof(f42588,plain,
! [X0] :
( ( v17_lattices(X0)
<=> ( v15_lattices(X0)
& v16_lattices(X0)
& v11_lattices(X0) ) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f42587]) ).
fof(f42979,plain,
! [X0] :
( ! [X1] :
( m2_filter_2(X1,X0)
<=> m1_filter_2(X1,k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f34676]) ).
fof(f42980,plain,
! [X0] :
( ! [X1] :
( m2_filter_2(X1,X0)
<=> m1_filter_2(X1,k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f42979]) ).
fof(f42987,plain,
! [X0] :
( ! [X1] :
( m1_filter_2(X1,X0)
<=> m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f34607]) ).
fof(f42988,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,[],[f42987]) ).
fof(f43653,plain,
( ~ r1_filter_2(u1_struct_0(sK257),k19_filter_2(sK257,k4_subset_1(u1_struct_0(sK257),sK258,sK259)),k21_filter_2(sK257,sK258,sK259))
& m2_filter_2(sK259,sK257)
& m2_filter_2(sK258,sK257)
& ~ v3_struct_0(sK257)
& v10_lattices(sK257)
& v17_lattices(sK257)
& l3_lattices(sK257) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK257,sK258,sK259]),skolemize(X0,sK257),skolemize(X1,sK258),skolemize(X2,sK259)],[f35049]) ).
fof(f43660,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( X2 = k19_filter_2(X0,X1)
| ~ r1_tarski(X1,X2)
| ? [X3] :
( ~ r1_tarski(X2,X3)
& r1_tarski(X1,X3)
& m2_filter_2(X3,X0) ) )
& ( ( r1_tarski(X1,X2)
& ! [X3] :
( r1_tarski(X2,X3)
| ~ r1_tarski(X1,X3)
| ~ m2_filter_2(X3,X0) ) )
| k19_filter_2(X0,X1) != X2 ) )
| ~ m2_filter_2(X2,X0) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f35109]) ).
fof(f43661,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( X2 = k19_filter_2(X0,X1)
| ~ r1_tarski(X1,X2)
| ? [X3] :
( ~ r1_tarski(X2,X3)
& r1_tarski(X1,X3)
& m2_filter_2(X3,X0) ) )
& ( ( r1_tarski(X1,X2)
& ! [X3] :
( r1_tarski(X2,X3)
| ~ r1_tarski(X1,X3)
| ~ m2_filter_2(X3,X0) ) )
| k19_filter_2(X0,X1) != X2 ) )
| ~ m2_filter_2(X2,X0) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f43660]) ).
fof(f43662,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( X2 = k19_filter_2(X0,X1)
| ~ r1_tarski(X1,X2)
| ? [X3] :
( ~ r1_tarski(X2,X3)
& r1_tarski(X1,X3)
& m2_filter_2(X3,X0) ) )
& ( ( r1_tarski(X1,X2)
& ! [X4] :
( r1_tarski(X2,X4)
| ~ r1_tarski(X1,X4)
| ~ m2_filter_2(X4,X0) ) )
| k19_filter_2(X0,X1) != X2 ) )
| ~ m2_filter_2(X2,X0) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(rectify,[],[f43661]) ).
fof(f43663,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( X2 = k19_filter_2(X0,X1)
| ~ r1_tarski(X1,X2)
| ( ~ r1_tarski(X2,sK264(X0,X1,X2))
& r1_tarski(X1,sK264(X0,X1,X2))
& m2_filter_2(sK264(X0,X1,X2),X0) ) )
& ( ( r1_tarski(X1,X2)
& ! [X4] :
( r1_tarski(X2,X4)
| ~ r1_tarski(X1,X4)
| ~ m2_filter_2(X4,X0) ) )
| k19_filter_2(X0,X1) != X2 ) )
| ~ m2_filter_2(X2,X0) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK264]),skolemize(X3,sK264(X0,X1,X2))],[f43662]) ).
fof(f46278,plain,
! [X0] :
( ( ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) )
| v3_struct_0(k1_lattice2(X0))
| ~ v10_lattices(k1_lattice2(X0))
| ~ v17_lattices(k1_lattice2(X0))
| ~ l3_lattices(k1_lattice2(X0)) )
& ( ( ~ v3_struct_0(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v17_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f42465]) ).
fof(f46279,plain,
! [X0] :
( ( ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) )
| v3_struct_0(k1_lattice2(X0))
| ~ v10_lattices(k1_lattice2(X0))
| ~ v17_lattices(k1_lattice2(X0))
| ~ l3_lattices(k1_lattice2(X0)) )
& ( ( ~ v3_struct_0(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v17_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f46278]) ).
fof(f46341,plain,
! [X0] :
( ( ( v17_lattices(X0)
| ~ v15_lattices(X0)
| ~ v16_lattices(X0)
| ~ v11_lattices(X0) )
& ( ( v15_lattices(X0)
& v16_lattices(X0)
& v11_lattices(X0) )
| ~ v17_lattices(X0) ) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f42588]) ).
fof(f46342,plain,
! [X0] :
( ( ( v17_lattices(X0)
| ~ v15_lattices(X0)
| ~ v16_lattices(X0)
| ~ v11_lattices(X0) )
& ( ( v15_lattices(X0)
& v16_lattices(X0)
& v11_lattices(X0) )
| ~ v17_lattices(X0) ) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f46341]) ).
fof(f46465,plain,
! [X0] :
( ! [X1] :
( ( m2_filter_2(X1,X0)
| ~ m1_filter_2(X1,k1_lattice2(X0)) )
& ( m1_filter_2(X1,k1_lattice2(X0))
| ~ m2_filter_2(X1,X0) ) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f42980]) ).
fof(f46466,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,[],[f42988]) ).
fof(f46521,plain,
l3_lattices(sK257),
inference(cnf_transformation,[],[f43653]) ).
fof(f46522,plain,
v17_lattices(sK257),
inference(cnf_transformation,[],[f43653]) ).
fof(f46523,plain,
v10_lattices(sK257),
inference(cnf_transformation,[],[f43653]) ).
fof(f46524,plain,
~ v3_struct_0(sK257),
inference(cnf_transformation,[],[f43653]) ).
fof(f46525,plain,
m2_filter_2(sK258,sK257),
inference(cnf_transformation,[],[f43653]) ).
fof(f46526,plain,
m2_filter_2(sK259,sK257),
inference(cnf_transformation,[],[f43653]) ).
fof(f46527,plain,
~ r1_filter_2(u1_struct_0(sK257),k19_filter_2(sK257,k4_subset_1(u1_struct_0(sK257),sK258,sK259)),k21_filter_2(sK257,sK258,sK259)),
inference(cnf_transformation,[],[f43653]) ).
fof(f46577,plain,
! [X2,X0,X1] :
( r1_tarski(X1,sK264(X0,X1,X2))
| ~ r1_tarski(X1,X2)
| k19_filter_2(X0,X1) = X2
| ~ m2_filter_2(X2,X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f43663]) ).
fof(f46578,plain,
! [X2,X0,X1] :
( ~ r1_tarski(X2,sK264(X0,X1,X2))
| ~ r1_tarski(X1,X2)
| k19_filter_2(X0,X1) = X2
| ~ m2_filter_2(X2,X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f43663]) ).
fof(f46617,plain,
! [X0,X1] :
( ~ m2_filter_2(X1,X0)
| ~ v1_xboole_0(X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35135]) ).
fof(f46618,plain,
! [X2,X0,X1] :
( r1_filter_2(u1_struct_0(X0),k19_filter_2(X0,k4_subset_1(u1_struct_0(X0),X1,X2)),k19_filter_2(X0,k20_filter_2(X0,X1,X2)))
| ~ m2_filter_2(X2,X0)
| ~ m2_filter_2(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35137]) ).
fof(f46640,plain,
! [X2,X0,X1] :
( ~ m2_filter_2(X2,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v11_lattices(X0)
| ~ l3_lattices(X0)
| ~ m2_filter_2(X1,X0)
| k20_filter_2(X0,X1,X2) = k21_filter_2(X0,X1,X2) ),
inference(cnf_transformation,[],[f35162]) ).
fof(f46641,plain,
! [X2,X0,X1] :
( m2_filter_2(k21_filter_2(X0,X1,X2),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v11_lattices(X0)
| ~ l3_lattices(X0)
| ~ m2_filter_2(X1,X0)
| ~ m2_filter_2(X2,X0) ),
inference(cnf_transformation,[],[f35164]) ).
fof(f46765,plain,
! [X0] : r1_tarski(X0,X0),
inference(cnf_transformation,[],[f34729]) ).
fof(f48641,plain,
! [X0] :
( ~ l3_lattices(X0)
| v3_struct_0(X0)
| u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0)) ),
inference(cnf_transformation,[],[f36544]) ).
fof(f50156,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,[],[f37579]) ).
fof(f57653,plain,
! [X0] :
( v10_lattices(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f46279]) ).
fof(f57673,plain,
! [X0] :
( l3_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f42470]) ).
fof(f57691,plain,
! [X0] :
( ~ v3_struct_0(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f42480]) ).
fof(f58028,plain,
! [X0] :
( ~ v17_lattices(X0)
| v11_lattices(X0)
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f46342]) ).
fof(f58491,plain,
! [X0,X1] :
( m1_filter_2(X1,k1_lattice2(X0))
| ~ m2_filter_2(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f46465]) ).
fof(f58496,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,[],[f46466]) ).
fof(f61273,plain,
! [X0] :
( v10_lattices(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(duplicate_literal_removal,[],[f57653]) ).
fof(f62554,definition,
( spl1961_51
<=> v11_lattices(sK257) ),
introduced(definition,[new_symbols(definition,[spl1961_51])],[avatar_definition]) ).
fof(f62555,plain,
( v11_lattices(sK257)
| ~ spl1961_51 ),
inference(avatar_component_clause,[],[f62554]) ).
fof(f62556,plain,
( ~ v11_lattices(sK257)
| spl1961_51 ),
inference(avatar_component_clause,[],[f62554]) ).
fof(f62558,plain,
! [X0] :
( v3_struct_0(sK257)
| ~ v10_lattices(sK257)
| ~ v11_lattices(sK257)
| ~ l3_lattices(sK257)
| ~ m2_filter_2(X0,sK257)
| k20_filter_2(sK257,X0,sK259) = k21_filter_2(sK257,X0,sK259) ),
inference(resolution,[],[f46526,f46640]) ).
fof(f62601,plain,
! [X0,X1] :
( ~ r1_tarski(X0,X0)
| k19_filter_2(X1,X0) = X0
| ~ m2_filter_2(X0,X1)
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(X1)))
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| ~ r1_tarski(X0,X0)
| k19_filter_2(X1,X0) = X0
| ~ m2_filter_2(X0,X1)
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(X1)))
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(resolution,[],[f46578,f46577]) ).
fof(f62602,plain,
! [X0,X1] :
( ~ r1_tarski(X0,X0)
| k19_filter_2(X1,X0) = X0
| ~ m2_filter_2(X0,X1)
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(X1)))
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(duplicate_literal_removal,[],[f62601]) ).
fof(f62603,plain,
! [X0,X1] :
( k19_filter_2(X1,X0) = X0
| ~ m2_filter_2(X0,X1)
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(X1)))
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(forward_subsumption_resolution,[],[f62602,f46765]) ).
fof(f62604,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(X1)))
| ~ m2_filter_2(X0,X1)
| k19_filter_2(X1,X0) = X0
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(forward_subsumption_resolution,[],[f62603,f46617]) ).
fof(f62640,plain,
! [X0,X1] :
( m1_filter_0(X0,k1_lattice2(X1))
| v3_struct_0(k1_lattice2(X1))
| ~ v10_lattices(k1_lattice2(X1))
| ~ l3_lattices(k1_lattice2(X1))
| ~ m2_filter_2(X0,X1)
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(resolution,[],[f58496,f58491]) ).
fof(f62641,plain,
! [X0,X1] :
( m1_filter_0(X0,k1_lattice2(X1))
| ~ v10_lattices(k1_lattice2(X1))
| ~ l3_lattices(k1_lattice2(X1))
| ~ m2_filter_2(X0,X1)
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(forward_subsumption_resolution,[],[f62640,f57691]) ).
fof(f62642,plain,
! [X0,X1] :
( m1_filter_0(X0,k1_lattice2(X1))
| ~ v10_lattices(k1_lattice2(X1))
| ~ m2_filter_2(X0,X1)
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(forward_subsumption_resolution,[],[f62641,f57673]) ).
fof(f62662,plain,
( v3_struct_0(sK257)
| u1_struct_0(sK257) = u1_struct_0(k1_lattice2(sK257)) ),
inference(resolution,[],[f48641,f46521]) ).
fof(f62664,plain,
u1_struct_0(sK257) = u1_struct_0(k1_lattice2(sK257)),
inference(forward_subsumption_resolution,[],[f62662,f46524]) ).
fof(f62673,plain,
! [X0] :
( m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK257)))
| ~ m1_filter_0(X0,k1_lattice2(sK257))
| v3_struct_0(k1_lattice2(sK257))
| ~ v10_lattices(k1_lattice2(sK257))
| ~ l3_lattices(k1_lattice2(sK257)) ),
inference(superposition,[],[f50156,f62664]) ).
fof(f62680,definition,
( spl1961_56
<=> l3_lattices(k1_lattice2(sK257)) ),
introduced(definition,[new_symbols(definition,[spl1961_56])],[avatar_definition]) ).
fof(f62682,plain,
( ~ l3_lattices(k1_lattice2(sK257))
| spl1961_56 ),
inference(avatar_component_clause,[],[f62680]) ).
fof(f62684,definition,
( spl1961_57
<=> v10_lattices(k1_lattice2(sK257)) ),
introduced(definition,[new_symbols(definition,[spl1961_57])],[avatar_definition]) ).
fof(f62685,plain,
( v10_lattices(k1_lattice2(sK257))
| ~ spl1961_57 ),
inference(avatar_component_clause,[],[f62684]) ).
fof(f62686,plain,
( ~ v10_lattices(k1_lattice2(sK257))
| spl1961_57 ),
inference(avatar_component_clause,[],[f62684]) ).
fof(f62688,definition,
( spl1961_58
<=> v3_struct_0(k1_lattice2(sK257)) ),
introduced(definition,[new_symbols(definition,[spl1961_58])],[avatar_definition]) ).
fof(f62690,plain,
( v3_struct_0(k1_lattice2(sK257))
| ~ spl1961_58 ),
inference(avatar_component_clause,[],[f62688]) ).
fof(f62717,definition,
( spl1961_65
<=> ! [X0] :
( m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK257)))
| ~ m1_filter_0(X0,k1_lattice2(sK257)) ) ),
introduced(definition,[new_symbols(definition,[spl1961_65])],[avatar_definition]) ).
fof(f62718,plain,
( ! [X0] :
( m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK257)))
| ~ m1_filter_0(X0,k1_lattice2(sK257)) )
| ~ spl1961_65 ),
inference(avatar_component_clause,[],[f62717]) ).
fof(f62719,plain,
( ~ spl1961_56
| ~ spl1961_57
| spl1961_58
| spl1961_65 ),
inference(avatar_split_clause,[],[f62673,f62717,f62688,f62684,f62680]) ).
fof(f62767,plain,
( ~ l3_lattices(sK257)
| spl1961_56 ),
inference(resolution,[],[f62682,f57673]) ).
fof(f62768,plain,
( $false
| spl1961_56 ),
inference(forward_subsumption_resolution,[],[f62767,f46521]) ).
fof(f62769,plain,
spl1961_56,
inference(avatar_contradiction_clause,[],[f62768]) ).
fof(f62777,plain,
( v3_struct_0(sK257)
| ~ l3_lattices(sK257)
| ~ spl1961_58 ),
inference(resolution,[],[f62690,f57691]) ).
fof(f62778,plain,
( ~ l3_lattices(sK257)
| ~ spl1961_58 ),
inference(forward_subsumption_resolution,[],[f62777,f46524]) ).
fof(f62779,plain,
( $false
| ~ spl1961_58 ),
inference(forward_subsumption_resolution,[],[f62778,f46521]) ).
fof(f62780,plain,
~ spl1961_58,
inference(avatar_contradiction_clause,[],[f62779]) ).
fof(f62781,plain,
( v3_struct_0(sK257)
| ~ v10_lattices(sK257)
| ~ v17_lattices(sK257)
| ~ l3_lattices(sK257)
| spl1961_57 ),
inference(resolution,[],[f62686,f61273]) ).
fof(f62784,plain,
( ~ v10_lattices(sK257)
| ~ v17_lattices(sK257)
| ~ l3_lattices(sK257)
| spl1961_57 ),
inference(forward_subsumption_resolution,[],[f62781,f46524]) ).
fof(f62785,plain,
( ~ v17_lattices(sK257)
| ~ l3_lattices(sK257)
| spl1961_57 ),
inference(forward_subsumption_resolution,[],[f62784,f46523]) ).
fof(f62786,plain,
( ~ l3_lattices(sK257)
| spl1961_57 ),
inference(forward_subsumption_resolution,[],[f62785,f46522]) ).
fof(f62787,plain,
( $false
| spl1961_57 ),
inference(forward_subsumption_resolution,[],[f62786,f46521]) ).
fof(f62788,plain,
spl1961_57,
inference(avatar_contradiction_clause,[],[f62787]) ).
fof(f62887,plain,
( v11_lattices(sK257)
| v3_struct_0(sK257)
| ~ l3_lattices(sK257) ),
inference(resolution,[],[f58028,f46522]) ).
fof(f62891,plain,
( v3_struct_0(sK257)
| ~ l3_lattices(sK257)
| spl1961_51 ),
inference(forward_subsumption_resolution,[],[f62887,f62556]) ).
fof(f62893,plain,
( ~ l3_lattices(sK257)
| spl1961_51 ),
inference(forward_subsumption_resolution,[],[f62891,f46524]) ).
fof(f62894,plain,
( $false
| spl1961_51 ),
inference(forward_subsumption_resolution,[],[f62893,f46521]) ).
fof(f62895,plain,
spl1961_51,
inference(avatar_contradiction_clause,[],[f62894]) ).
fof(f62896,plain,
! [X0] :
( ~ v10_lattices(sK257)
| ~ v11_lattices(sK257)
| ~ l3_lattices(sK257)
| ~ m2_filter_2(X0,sK257)
| k20_filter_2(sK257,X0,sK259) = k21_filter_2(sK257,X0,sK259) ),
inference(forward_subsumption_resolution,[],[f62558,f46524]) ).
fof(f62897,plain,
! [X0] :
( ~ v11_lattices(sK257)
| ~ l3_lattices(sK257)
| ~ m2_filter_2(X0,sK257)
| k20_filter_2(sK257,X0,sK259) = k21_filter_2(sK257,X0,sK259) ),
inference(forward_subsumption_resolution,[],[f62896,f46523]) ).
fof(f62898,plain,
( ! [X0] :
( ~ l3_lattices(sK257)
| ~ m2_filter_2(X0,sK257)
| k20_filter_2(sK257,X0,sK259) = k21_filter_2(sK257,X0,sK259) )
| ~ spl1961_51 ),
inference(forward_subsumption_resolution,[],[f62897,f62555]) ).
fof(f62899,plain,
( ! [X0] :
( ~ m2_filter_2(X0,sK257)
| k20_filter_2(sK257,X0,sK259) = k21_filter_2(sK257,X0,sK259) )
| ~ spl1961_51 ),
inference(forward_subsumption_resolution,[],[f62898,f46521]) ).
fof(f62900,plain,
( k21_filter_2(sK257,sK258,sK259) = k20_filter_2(sK257,sK258,sK259)
| ~ spl1961_51 ),
inference(resolution,[],[f62899,f46525]) ).
fof(f62929,plain,
( ~ r1_filter_2(u1_struct_0(sK257),k19_filter_2(sK257,k4_subset_1(u1_struct_0(sK257),sK258,sK259)),k20_filter_2(sK257,sK258,sK259))
| ~ spl1961_51 ),
inference(superposition,[],[f46527,f62900]) ).
fof(f62931,plain,
( m2_filter_2(k20_filter_2(sK257,sK258,sK259),sK257)
| v3_struct_0(sK257)
| ~ v10_lattices(sK257)
| ~ v11_lattices(sK257)
| ~ l3_lattices(sK257)
| ~ m2_filter_2(sK258,sK257)
| ~ m2_filter_2(sK259,sK257)
| ~ spl1961_51 ),
inference(superposition,[],[f46641,f62900]) ).
fof(f62932,plain,
( m2_filter_2(k20_filter_2(sK257,sK258,sK259),sK257)
| ~ v10_lattices(sK257)
| ~ v11_lattices(sK257)
| ~ l3_lattices(sK257)
| ~ m2_filter_2(sK258,sK257)
| ~ m2_filter_2(sK259,sK257)
| ~ spl1961_51 ),
inference(forward_subsumption_resolution,[],[f62931,f46524]) ).
fof(f62934,plain,
( m2_filter_2(k20_filter_2(sK257,sK258,sK259),sK257)
| ~ v11_lattices(sK257)
| ~ l3_lattices(sK257)
| ~ m2_filter_2(sK258,sK257)
| ~ m2_filter_2(sK259,sK257)
| ~ spl1961_51 ),
inference(forward_subsumption_resolution,[],[f62932,f46523]) ).
fof(f62936,plain,
( m2_filter_2(k20_filter_2(sK257,sK258,sK259),sK257)
| ~ l3_lattices(sK257)
| ~ m2_filter_2(sK258,sK257)
| ~ m2_filter_2(sK259,sK257)
| ~ spl1961_51 ),
inference(forward_subsumption_resolution,[],[f62934,f62555]) ).
fof(f62938,plain,
( m2_filter_2(k20_filter_2(sK257,sK258,sK259),sK257)
| ~ m2_filter_2(sK258,sK257)
| ~ m2_filter_2(sK259,sK257)
| ~ spl1961_51 ),
inference(forward_subsumption_resolution,[],[f62936,f46521]) ).
fof(f62940,plain,
( m2_filter_2(k20_filter_2(sK257,sK258,sK259),sK257)
| ~ m2_filter_2(sK259,sK257)
| ~ spl1961_51 ),
inference(forward_subsumption_resolution,[],[f62938,f46525]) ).
fof(f62942,plain,
( m2_filter_2(k20_filter_2(sK257,sK258,sK259),sK257)
| ~ spl1961_51 ),
inference(forward_subsumption_resolution,[],[f62940,f46526]) ).
fof(f63069,definition,
( spl1961_80
<=> k20_filter_2(sK257,sK258,sK259) = k19_filter_2(sK257,k20_filter_2(sK257,sK258,sK259)) ),
introduced(definition,[new_symbols(definition,[spl1961_80])],[avatar_definition]) ).
fof(f63071,plain,
( k20_filter_2(sK257,sK258,sK259) = k19_filter_2(sK257,k20_filter_2(sK257,sK258,sK259))
| ~ spl1961_80 ),
inference(avatar_component_clause,[],[f63069]) ).
fof(f63252,plain,
( ! [X0] :
( ~ m1_filter_0(X0,k1_lattice2(sK257))
| ~ m2_filter_2(X0,sK257)
| k19_filter_2(sK257,X0) = X0
| v3_struct_0(sK257)
| ~ v10_lattices(sK257)
| ~ l3_lattices(sK257) )
| ~ spl1961_65 ),
inference(resolution,[],[f62718,f62604]) ).
fof(f63261,plain,
( ! [X0] :
( ~ m1_filter_0(X0,k1_lattice2(sK257))
| ~ m2_filter_2(X0,sK257)
| k19_filter_2(sK257,X0) = X0
| ~ v10_lattices(sK257)
| ~ l3_lattices(sK257) )
| ~ spl1961_65 ),
inference(forward_subsumption_resolution,[],[f63252,f46524]) ).
fof(f63268,plain,
( ! [X0] :
( ~ m1_filter_0(X0,k1_lattice2(sK257))
| ~ m2_filter_2(X0,sK257)
| k19_filter_2(sK257,X0) = X0
| ~ l3_lattices(sK257) )
| ~ spl1961_65 ),
inference(forward_subsumption_resolution,[],[f63261,f46523]) ).
fof(f63275,plain,
( ! [X0] :
( ~ m1_filter_0(X0,k1_lattice2(sK257))
| ~ m2_filter_2(X0,sK257)
| k19_filter_2(sK257,X0) = X0 )
| ~ spl1961_65 ),
inference(forward_subsumption_resolution,[],[f63268,f46521]) ).
fof(f63284,plain,
( ! [X0] :
( ~ m2_filter_2(X0,sK257)
| k19_filter_2(sK257,X0) = X0
| ~ v10_lattices(k1_lattice2(sK257))
| ~ m2_filter_2(X0,sK257)
| v3_struct_0(sK257)
| ~ v10_lattices(sK257)
| ~ l3_lattices(sK257) )
| ~ spl1961_65 ),
inference(resolution,[],[f63275,f62642]) ).
fof(f63287,plain,
( ! [X0] :
( ~ m2_filter_2(X0,sK257)
| k19_filter_2(sK257,X0) = X0
| ~ v10_lattices(k1_lattice2(sK257))
| v3_struct_0(sK257)
| ~ v10_lattices(sK257)
| ~ l3_lattices(sK257) )
| ~ spl1961_65 ),
inference(duplicate_literal_removal,[],[f63284]) ).
fof(f63306,plain,
( ! [X0] :
( ~ m2_filter_2(X0,sK257)
| k19_filter_2(sK257,X0) = X0
| v3_struct_0(sK257)
| ~ v10_lattices(sK257)
| ~ l3_lattices(sK257) )
| ~ spl1961_57
| ~ spl1961_65 ),
inference(forward_subsumption_resolution,[],[f63287,f62685]) ).
fof(f63317,plain,
( ! [X0] :
( ~ m2_filter_2(X0,sK257)
| k19_filter_2(sK257,X0) = X0
| ~ v10_lattices(sK257)
| ~ l3_lattices(sK257) )
| ~ spl1961_57
| ~ spl1961_65 ),
inference(forward_subsumption_resolution,[],[f63306,f46524]) ).
fof(f63319,plain,
( ! [X0] :
( ~ m2_filter_2(X0,sK257)
| k19_filter_2(sK257,X0) = X0
| ~ l3_lattices(sK257) )
| ~ spl1961_57
| ~ spl1961_65 ),
inference(forward_subsumption_resolution,[],[f63317,f46523]) ).
fof(f63321,plain,
( ! [X0] :
( ~ m2_filter_2(X0,sK257)
| k19_filter_2(sK257,X0) = X0 )
| ~ spl1961_57
| ~ spl1961_65 ),
inference(forward_subsumption_resolution,[],[f63319,f46521]) ).
fof(f63429,plain,
( k20_filter_2(sK257,sK258,sK259) = k19_filter_2(sK257,k20_filter_2(sK257,sK258,sK259))
| ~ spl1961_51
| ~ spl1961_57
| ~ spl1961_65 ),
inference(resolution,[],[f63321,f62942]) ).
fof(f63439,plain,
( spl1961_80
| ~ spl1961_51
| ~ spl1961_57
| ~ spl1961_65 ),
inference(avatar_split_clause,[],[f63429,f62717,f62684,f62554,f63069]) ).
fof(f63533,plain,
( r1_filter_2(u1_struct_0(sK257),k19_filter_2(sK257,k4_subset_1(u1_struct_0(sK257),sK258,sK259)),k20_filter_2(sK257,sK258,sK259))
| ~ m2_filter_2(sK259,sK257)
| ~ m2_filter_2(sK258,sK257)
| v3_struct_0(sK257)
| ~ v10_lattices(sK257)
| ~ l3_lattices(sK257)
| ~ spl1961_80 ),
inference(superposition,[],[f46618,f63071]) ).
fof(f63542,plain,
( ~ m2_filter_2(sK259,sK257)
| ~ m2_filter_2(sK258,sK257)
| v3_struct_0(sK257)
| ~ v10_lattices(sK257)
| ~ l3_lattices(sK257)
| ~ spl1961_51
| ~ spl1961_80 ),
inference(forward_subsumption_resolution,[],[f63533,f62929]) ).
fof(f63546,plain,
( ~ m2_filter_2(sK258,sK257)
| v3_struct_0(sK257)
| ~ v10_lattices(sK257)
| ~ l3_lattices(sK257)
| ~ spl1961_51
| ~ spl1961_80 ),
inference(forward_subsumption_resolution,[],[f63542,f46526]) ).
fof(f63550,plain,
( v3_struct_0(sK257)
| ~ v10_lattices(sK257)
| ~ l3_lattices(sK257)
| ~ spl1961_51
| ~ spl1961_80 ),
inference(forward_subsumption_resolution,[],[f63546,f46525]) ).
fof(f63554,plain,
( ~ v10_lattices(sK257)
| ~ l3_lattices(sK257)
| ~ spl1961_51
| ~ spl1961_80 ),
inference(forward_subsumption_resolution,[],[f63550,f46524]) ).
fof(f63563,plain,
( ~ l3_lattices(sK257)
| ~ spl1961_51
| ~ spl1961_80 ),
inference(forward_subsumption_resolution,[],[f63554,f46523]) ).
fof(f63564,plain,
( $false
| ~ spl1961_51
| ~ spl1961_80 ),
inference(forward_subsumption_resolution,[],[f63563,f46521]) ).
fof(f63565,plain,
( ~ spl1961_51
| ~ spl1961_80 ),
inference(avatar_contradiction_clause,[],[f63564]) ).
cnf(s54,plain,
( ~ spl1961_56
| ~ spl1961_57
| spl1961_58
| spl1961_65 ),
inference(sat_conversion,[],[f62719]) ).
cnf(s63,plain,
spl1961_56,
inference(sat_conversion,[],[f62769]) ).
cnf(s65,plain,
~ spl1961_58,
inference(sat_conversion,[],[f62780]) ).
cnf(s66,plain,
spl1961_57,
inference(sat_conversion,[],[f62788]) ).
cnf(s67,plain,
spl1961_51,
inference(sat_conversion,[],[f62895]) ).
cnf(s81,plain,
( ~ spl1961_51
| ~ spl1961_57
| ~ spl1961_65
| spl1961_80 ),
inference(sat_conversion,[],[f63439]) ).
cnf(s87,plain,
( ~ spl1961_51
| ~ spl1961_80 ),
inference(sat_conversion,[],[f63565]) ).
cnf(s90,plain,
~ spl1961_80,
inference(rat,[],[s87,s67]) ).
cnf(s92,plain,
~ spl1961_65,
inference(rat,[],[s81,s90,s67,s66]) ).
cnf(s102,plain,
$false,
inference(rat,[],[s54,s92,s65,s66,s63]) ).
fof(f63566,plain,
$false,
inference(avatar_sat_refutation,[],[s102]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT320+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.37 % Computer : n020.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:36:56 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.40 Running first-order theorem proving
% 0.11/0.40 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 18.53/5.36 % (3447284)Detected formulas, will run a generic FOF schedule.
% 18.53/5.36 % (3447291)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=1629902456:i=141695:sd=1:nm=32:gsp=on:ss=included_2977 on theBenchmark for (2977ds/141695Mi)
% 18.53/5.36 % (3447289)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=3501497553:i=141193_2977 on theBenchmark for (2977ds/141193Mi)
% 18.53/5.36 % (3447290)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=3467918951:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2977 on theBenchmark for (2977ds/134677Mi)
% 18.53/5.36 % (3447295)dis-21_1_sil=8000:lcm=predicate:random_seed=3380652423:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2977 on theBenchmark for (2977ds/129Mi)
% 18.53/5.36 % (3447292)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1641597590:i=109:sd=1:ins=1:gsp=on:ss=axioms_2977 on theBenchmark for (2977ds/109Mi)
% 18.53/5.36 % (3447294)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2536394930:s2a=on:i=139:gtg=position_2977 on theBenchmark for (2977ds/139Mi)
% 18.53/5.36 % (3447293)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3569935982:i=119:av=off:ss=axioms_2977 on theBenchmark for (2977ds/119Mi)
% 18.53/5.36 % (3447294)Instruction limit reached!
% 18.53/5.36 % (3447294)------------------------------
% 18.53/5.36 % (3447294)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.53/5.36 % (3447294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.53/5.36 % (3447294)CaDiCaL version: 2.1.3
% 18.53/5.36 % (3447294)Termination reason: Instruction limit
% 18.53/5.36 % (3447294)Termination phase: Property scanning
% 18.53/5.36 % (3447294)Time elapsed: 0.063 s
% 18.53/5.36 % (3447294)Peak memory usage: 136 MB
% 18.53/5.36 % (3447294)Instructions burned: 141 (million)
% 18.53/5.36 % (3447292)Instruction limit reached!
% 18.53/5.36 % (3447292)------------------------------
% 18.53/5.36 % (3447292)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.53/5.36 % (3447292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.53/5.36 % (3447292)CaDiCaL version: 2.1.3
% 18.53/5.36 % (3447292)Termination reason: Instruction limit
% 18.53/5.36 % (3447292)Termination phase: SInE selection
% 18.53/5.36 % (3447292)Time elapsed: 0.083 s
% 18.53/5.36 % (3447292)Peak memory usage: 136 MB
% 18.53/5.36 % (3447292)Instructions burned: 110 (million)
% 18.53/5.36 % (3447293)Instruction limit reached!
% 18.53/5.36 % (3447293)------------------------------
% 18.53/5.36 % (3447293)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.53/5.36 % (3447293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.53/5.36 % (3447293)CaDiCaL version: 2.1.3
% 18.53/5.36 % (3447293)Termination reason: Instruction limit
% 18.53/5.36 % (3447293)Termination phase: SInE selection
% 18.53/5.36 % (3447293)Time elapsed: 0.089 s
% 18.53/5.36 % (3447293)Peak memory usage: 136 MB
% 18.53/5.36 % (3447293)Instructions burned: 119 (million)
% 18.53/5.36 % (3447295)Instruction limit reached!
% 18.53/5.36 % (3447295)------------------------------
% 18.53/5.36 % (3447295)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.53/5.36 % (3447295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.53/5.36 % (3447295)CaDiCaL version: 2.1.3
% 18.53/5.36 % (3447295)Termination reason: Instruction limit
% 18.53/5.36 % (3447295)Termination phase: SInE selection
% 18.53/5.36 % (3447295)Time elapsed: 0.092 s
% 18.53/5.36 % (3447295)Peak memory usage: 136 MB
% 18.53/5.36 % (3447295)Instructions burned: 129 (million)
% 18.53/5.36 % (3447303)lrs+10_1_sil=8000:sp=occurrence:random_seed=4286666124:i=285:sd=3:ss=axioms:sgt=8_2975 on theBenchmark for (2975ds/285Mi)
% 18.53/5.36 % (3447306)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=4068179823:s2a=on:i=248:s2at=1.23:gtg=position_2975 on theBenchmark for (2975ds/248Mi)
% 18.53/5.36 % (3447305)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1064160267:i=325:sd=1:ss=axioms:sgt=32_2975 on theBenchmark for (2975ds/325Mi)
% 18.53/5.36 % (3447304)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3405608619:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2975 on theBenchmark for (2975ds/157Mi)
% 18.53/5.36 % (3447304)Instruction limit reached!
% 26.81/6.54 % (3447304)------------------------------
% 26.81/6.54 % (3447304)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.81/6.54 % (3447304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.81/6.54 % (3447304)CaDiCaL version: 2.1.3
% 26.81/6.54 % (3447304)Termination reason: Instruction limit
% 26.81/6.54 % (3447304)Termination phase: Property scanning
% 26.81/6.54 % (3447304)Time elapsed: 0.070 s
% 26.81/6.54 % (3447304)Peak memory usage: 136 MB
% 26.81/6.54 % (3447304)Instructions burned: 159 (million)
% 26.81/6.54 % (3447306)Instruction limit reached!
% 26.81/6.54 % (3447306)------------------------------
% 26.81/6.54 % (3447306)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.81/6.54 % (3447306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.81/6.54 % (3447306)CaDiCaL version: 2.1.3
% 26.81/6.54 % (3447306)Termination reason: Instruction limit
% 26.81/6.54 % (3447306)Termination phase: Property scanning
% 26.81/6.54 % (3447306)Time elapsed: 0.107 s
% 26.81/6.54 % (3447306)Peak memory usage: 136 MB
% 26.81/6.54 % (3447306)Instructions burned: 248 (million)
% 26.81/6.54 % (3447303)Instruction limit reached!
% 26.81/6.54 % (3447303)------------------------------
% 26.81/6.54 % (3447303)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.81/6.54 % (3447303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.81/6.54 % (3447303)CaDiCaL version: 2.1.3
% 26.81/6.54 % (3447303)Termination reason: Instruction limit
% 26.81/6.54 % (3447303)Termination phase: Saturation
% 26.81/6.54 % (3447303)Time elapsed: 0.220 s
% 26.81/6.54 % (3447303)Peak memory usage: 141 MB
% 26.81/6.54 % (3447303)Instructions burned: 285 (million)
% 26.81/6.54 % (3447305)Refutation not found, incomplete strategy
% 26.81/6.54 % (3447305)------------------------------
% 26.81/6.54 % (3447305)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.81/6.54 % (3447305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.81/6.54 % (3447305)CaDiCaL version: 2.1.3
% 26.81/6.54 % (3447305)Termination reason: Refutation not found, incomplete strategy
% 26.81/6.54 % (3447305)Time elapsed: 0.202 s
% 26.81/6.54 % (3447305)Peak memory usage: 142 MB
% 26.81/6.54 % (3447305)Instructions burned: 244 (million)
% 26.81/6.54 % (3447311)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2951107082:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2972 on theBenchmark for (2972ds/294Mi)
% 26.81/6.54 % (3447312)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=57845524:i=2350_2972 on theBenchmark for (2972ds/2350Mi)
% 26.81/6.54 % (3447313)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1607186599:cts=off:i=113:fsr=off:ss=included:sgt=4_2971 on theBenchmark for (2971ds/113Mi)
% 26.81/6.54 % (3447311)Instruction limit reached!
% 26.81/6.54 % (3447311)------------------------------
% 26.81/6.54 % (3447311)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.81/6.54 % (3447311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.81/6.54 % (3447311)CaDiCaL version: 2.1.3
% 26.81/6.54 % (3447311)Termination reason: Instruction limit
% 26.81/6.54 % (3447311)Termination phase: SInE selection
% 26.81/6.54 % (3447311)Time elapsed: 0.180 s
% 26.81/6.54 % (3447311)Peak memory usage: 137 MB
% 26.81/6.54 % (3447311)Instructions burned: 295 (million)
% 26.81/6.54 % (3447313)Instruction limit reached!
% 26.81/6.54 % (3447313)------------------------------
% 26.81/6.54 % (3447313)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.81/6.54 % (3447313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.81/6.54 % (3447313)CaDiCaL version: 2.1.3
% 26.81/6.54 % (3447313)Termination reason: Instruction limit
% 26.81/6.54 % (3447313)Termination phase: SInE selection
% 26.81/6.54 % (3447313)Time elapsed: 0.086 s
% 26.81/6.54 % (3447313)Peak memory usage: 136 MB
% 26.81/6.54 % (3447313)Instructions burned: 114 (million)
% 26.81/6.54 % (3447305)------------------------------
% 26.81/6.54 % (3447305)------------------------------
% 26.81/6.54 % (3447317)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3364676381:i=127:av=off:fsr=off:sup=off_2969 on theBenchmark for (2969ds/127Mi)
% 26.81/6.54 % (3447318)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=4067053912:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2969 on theBenchmark for (2969ds/114Mi)
% 26.81/6.54 % (3447318)Instruction limit reached!
% 26.81/6.54 % (3447318)------------------------------
% 33.15/9.84 % (3447318)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.15/9.84 % (3447318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.15/9.84 % (3447318)CaDiCaL version: 2.1.3
% 33.15/9.84 % (3447318)Termination reason: Instruction limit
% 33.15/9.84 % (3447318)Termination phase: Property scanning
% 33.15/9.84 % (3447318)Time elapsed: 0.051 s
% 33.15/9.84 % (3447318)Peak memory usage: 136 MB
% 33.15/9.84 % (3447318)Instructions burned: 115 (million)
% 33.15/9.84 % (3447319)lrs+10_1_sil=8000:sp=occurrence:random_seed=481116137:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2968 on theBenchmark for (2968ds/907Mi)
% 33.15/9.84 % (3447317)Instruction limit reached!
% 33.15/9.84 % (3447317)------------------------------
% 33.15/9.84 % (3447317)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.15/9.84 % (3447317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.15/9.84 % (3447317)CaDiCaL version: 2.1.3
% 33.15/9.84 % (3447317)Termination reason: Instruction limit
% 33.15/9.84 % (3447317)Termination phase: Preprocessing 1
% 33.15/9.84 % (3447317)Time elapsed: 0.095 s
% 33.15/9.84 % (3447317)Peak memory usage: 137 MB
% 33.15/9.84 % (3447317)Instructions burned: 127 (million)
% 33.15/9.84 % (3447323)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=50969909:i=437:sd=1:aac=none:ss=included_2967 on theBenchmark for (2967ds/437Mi)
% 33.15/9.84 % (3447324)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1484667751:i=5202:ss=axioms:sgt=16_2966 on theBenchmark for (2966ds/5202Mi)
% 33.15/9.84 % (3447323)Instruction limit reached!
% 33.15/9.84 % (3447323)------------------------------
% 33.15/9.84 % (3447323)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.15/9.84 % (3447323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.15/9.84 % (3447323)CaDiCaL version: 2.1.3
% 33.15/9.84 % (3447323)Termination reason: Instruction limit
% 33.15/9.84 % (3447323)Termination phase: Saturation
% 33.15/9.84 % (3447323)Time elapsed: 0.304 s
% 33.15/9.84 % (3447323)Peak memory usage: 143 MB
% 33.15/9.84 % (3447323)Instructions burned: 438 (million)
% 33.15/9.84 % (3447319)Instruction limit reached!
% 33.15/9.84 % (3447319)------------------------------
% 33.15/9.84 % (3447319)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.15/9.84 % (3447319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.15/9.84 % (3447319)CaDiCaL version: 2.1.3
% 33.15/9.84 % (3447319)Termination reason: Instruction limit
% 33.15/9.84 % (3447319)Termination phase: Property scanning
% 33.15/9.84 % (3447319)Time elapsed: 0.594 s
% 33.15/9.84 % (3447319)Peak memory usage: 156 MB
% 33.15/9.84 % (3447319)Instructions burned: 908 (million)
% 33.15/9.84 % (3447327)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2846342477:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2962 on theBenchmark for (2962ds/134Mi)
% 33.15/9.84 % (3447327)Instruction limit reached!
% 33.15/9.84 % (3447327)------------------------------
% 33.15/9.84 % (3447327)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.15/9.84 % (3447327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.15/9.84 % (3447327)CaDiCaL version: 2.1.3
% 33.15/9.84 % (3447327)Termination reason: Instruction limit
% 33.15/9.84 % (3447327)Termination phase: SInE selection
% 33.15/9.84 % (3447327)Time elapsed: 0.103 s
% 33.15/9.84 % (3447327)Peak memory usage: 136 MB
% 33.15/9.84 % (3447327)Instructions burned: 135 (million)
% 33.15/9.84 % (3447328)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3285097054:st=8:i=592:sd=3:ep=RST:ss=axioms_2961 on theBenchmark for (2961ds/592Mi)
% 33.15/9.84 % (3447330)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=4035338953:st=3:i=13193:sd=3:ss=axioms_2959 on theBenchmark for (2959ds/13193Mi)
% 33.15/9.84 % (3447328)Instruction limit reached!
% 33.15/9.84 % (3447328)------------------------------
% 33.15/9.84 % (3447328)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.15/9.84 % (3447328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.15/9.84 % (3447328)CaDiCaL version: 2.1.3
% 33.15/9.84 % (3447328)Termination reason: Instruction limit
% 33.15/9.84 % (3447328)Termination phase: Preprocessing 2
% 33.15/9.84 % (3447328)Time elapsed: 0.441 s
% 33.15/9.84 % (3447328)Peak memory usage: 146 MB
% 33.15/9.84 % (3447328)Instructions burned: 592 (million)
% 33.15/9.84 % (3447312)Instruction limit reached!
% 33.15/9.84 % (3447312)------------------------------
% 33.15/9.84 % (3447312)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.15/9.84 % (3447312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.15/9.84 % (3447312)CaDiCaL version: 2.1.3
% 33.15/9.84 % (3447312)Termination reason: Instruction limit
% 33.15/9.84 % (3447312)Termination phase: Property scanning
% 33.15/9.84 % (3447312)Time elapsed: 1.582 s
% 33.15/9.84 % (3447312)Peak memory usage: 233 MB
% 33.15/9.84 % (3447312)Instructions burned: 2351 (million)
% 33.15/9.84 % (3447334)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3765736188:i=134:gtgl=5:slsql=off:gtg=exists_sym_2954 on theBenchmark for (2954ds/134Mi)
% 33.15/9.84 % (3447333)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=712068678:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2954 on theBenchmark for (2954ds/125Mi)
% 33.15/9.84 % (3447333)Instruction limit reached!
% 33.15/9.84 % (3447333)------------------------------
% 33.15/9.84 % (3447333)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.15/9.84 % (3447333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.15/9.84 % (3447333)CaDiCaL version: 2.1.3
% 33.15/9.84 % (3447333)Termination reason: Instruction limit
% 33.15/9.84 % (3447333)Termination phase: Property scanning
% 33.15/9.84 % (3447333)Time elapsed: 0.056 s
% 33.15/9.84 % (3447333)Peak memory usage: 136 MB
% 33.15/9.84 % (3447333)Instructions burned: 127 (million)
% 33.15/9.84 % (3447334)Instruction limit reached!
% 33.15/9.84 % (3447334)------------------------------
% 33.15/9.84 % (3447334)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.15/9.84 % (3447334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.15/9.84 % (3447334)CaDiCaL version: 2.1.3
% 33.15/9.84 % (3447334)Termination reason: Instruction limit
% 33.15/9.84 % (3447334)Termination phase: Property scanning
% 33.15/9.84 % (3447334)Time elapsed: 0.059 s
% 33.15/9.84 % (3447334)Peak memory usage: 136 MB
% 33.15/9.84 % (3447334)Instructions burned: 136 (million)
% 33.15/9.84 % (3447337)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=4252103302:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2952 on theBenchmark for (2952ds/141Mi)
% 33.15/9.84 % (3447338)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2874437935:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2952 on theBenchmark for (2952ds/431Mi)
% 33.15/9.84 % (3447337)Instruction limit reached!
% 33.15/9.84 % (3447337)------------------------------
% 33.15/9.84 % (3447337)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.15/9.84 % (3447337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.15/9.84 % (3447337)CaDiCaL version: 2.1.3
% 33.15/9.84 % (3447337)Termination reason: Instruction limit
% 33.15/9.84 % (3447337)Termination phase: SInE selection
% 33.15/9.84 % (3447337)Time elapsed: 0.102 s
% 33.15/9.84 % (3447337)Peak memory usage: 136 MB
% 33.15/9.84 % (3447337)Instructions burned: 142 (million)
% 33.15/9.84 % (3447338)Refutation not found, incomplete strategy
% 33.15/9.84 % (3447338)------------------------------
% 33.15/9.84 % (3447338)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.15/9.84 % (3447338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.15/9.84 % (3447338)CaDiCaL version: 2.1.3
% 33.15/9.84 % (3447338)Termination reason: Refutation not found, incomplete strategy
% 33.15/9.84 % (3447338)Time elapsed: 0.195 s
% 33.15/9.84 % (3447338)Peak memory usage: 142 MB
% 33.15/9.84 % (3447338)Instructions burned: 250 (million)
% 33.15/9.84 % (3447341)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=3730008707:i=6060:aac=none:ins=25_2949 on theBenchmark for (2949ds/6060Mi)
% 33.15/9.84 % (3447338)------------------------------
% 33.15/9.84 % (3447338)------------------------------
% 33.15/9.84 % (3447343)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=3672877390:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2946 on theBenchmark for (2946ds/150Mi)
% 33.15/9.84 % (3447343)Instruction limit reached!
% 33.15/9.84 % (3447343)------------------------------
% 33.15/9.84 % (3447343)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.15/9.84 % (3447343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.15/9.84 % (3447343)CaDiCaL version: 2.1.3
% 33.15/9.84 % (3447343)Termination reason: Instruction limit
% 33.15/9.84 % (3447343)Termination phase: SInE selection
% 33.15/9.84 % (3447343)Time elapsed: 0.122 s
% 33.15/9.84 % (3447343)Peak memory usage: 136 MB
% 33.15/9.84 % (3447343)Instructions burned: 151 (million)
% 33.15/9.84 % (3447345)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3825824731:i=14155:bd=all_2943 on theBenchmark for (2943ds/14155Mi)
% 33.15/9.84 % (3447324)Instruction limit reached!
% 33.15/9.84 % (3447324)------------------------------
% 33.15/9.84 % (3447324)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.15/9.84 % (3447324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.15/9.84 % (3447324)CaDiCaL version: 2.1.3
% 33.15/9.84 % (3447324)Termination reason: Instruction limit
% 33.15/9.84 % (3447324)Termination phase: Saturation
% 33.15/9.84 % (3447324)Time elapsed: 3.912 s
% 33.15/9.84 % (3447324)Peak memory usage: 733 MB
% 33.15/9.84 % (3447324)Instructions burned: 5205 (million)
% 33.15/9.84 % (3447347)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3845081079:i=667:av=off:fsr=off_2925 on theBenchmark for (2925ds/667Mi)
% 33.15/9.84 % (3447347)Instruction limit reached!
% 33.15/9.84 % (3447347)------------------------------
% 33.15/9.84 % (3447347)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.15/9.84 % (3447347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.15/9.84 % (3447347)CaDiCaL version: 2.1.3
% 33.15/9.84 % (3447347)Termination reason: Instruction limit
% 33.15/9.84 % (3447347)Termination phase: NewCNF
% 33.15/9.84 % (3447347)Time elapsed: 0.552 s
% 33.15/9.84 % (3447347)Peak memory usage: 186 MB
% 33.15/9.84 % (3447347)Instructions burned: 668 (million)
% 33.15/9.84 % (3447349)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=2570057159:s2a=on:i=185:s2at=1.8:fdi=4_2917 on theBenchmark for (2917ds/185Mi)
% 33.15/9.84 % (3447349)Instruction limit reached!
% 33.15/9.84 % (3447349)------------------------------
% 33.15/9.84 % (3447349)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.15/9.84 % (3447349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.15/9.84 % (3447349)CaDiCaL version: 2.1.3
% 33.15/9.84 % (3447349)Termination reason: Instruction limit
% 33.15/9.84 % (3447349)Termination phase: SInE selection
% 33.15/9.84 % (3447349)Time elapsed: 0.131 s
% 33.15/9.84 % (3447349)Peak memory usage: 136 MB
% 33.15/9.84 % (3447349)Instructions burned: 187 (million)
% 33.15/9.84 % (3447330)First to succeed.
% 33.15/9.84 % (3447330)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3447284"
% 33.15/9.84 % (3447351)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=3835705681:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2914 on theBenchmark for (2914ds/193Mi)
% 33.15/9.84 % (3447351)Instruction limit reached!
% 33.15/9.84 % (3447351)------------------------------
% 33.15/9.84 % (3447351)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.15/9.84 % (3447351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.15/9.84 % (3447351)CaDiCaL version: 2.1.3
% 33.15/9.84 % (3447351)Termination reason: Instruction limit
% 33.15/9.84 % (3447351)Termination phase: SInE selection
% 33.15/9.84 % (3447351)Time elapsed: 0.152 s
% 33.15/9.84 % (3447351)Peak memory usage: 136 MB
% 33.15/9.84 % (3447351)Instructions burned: 193 (million)
% 33.15/9.84 % (3447330)Refutation found. Thanks to Tanya!
% 33.15/9.84 % SZS status Theorem for theBenchmark
% 33.15/9.84 % SZS output start Proof for theBenchmark
% See solution above
% 50.46/9.99 % (3447330)------------------------------
% 50.46/9.99 % (3447330)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.46/9.99 % (3447330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.46/9.99 % (3447330)CaDiCaL version: 2.1.3
% 50.46/9.99 % (3447330)Termination reason: Refutation
% 50.46/9.99 % (3447330)Time elapsed: 4.391 s
% 50.46/9.99 % (3447330)Peak memory usage: 367 MB
% 50.46/9.99 % (3447330)Instructions burned: 7282 (million)
% 50.46/9.99 % (3447330)------------------------------
% 50.46/9.99 % (3447330)------------------------------
% 50.46/9.99 % (3447284)Success in time 8.988 s
% 50.46/9.99 % Vampire exiting
%------------------------------------------------------------------------------