%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT323+3 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n003.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:56 AM UTC 2026
% Result : Theorem 20.70s 4.68s
% Output : Refutation 24.56s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 25
% Syntax : Number of formulae : 206 ( 34 unt; 7 def)
% Number of atoms : 906 ( 73 equ)
% Maximal formula atoms : 20 ( 4 avg)
% Number of connectives : 1135 ( 435 ~; 452 |; 188 &)
% ( 21 <=>; 37 =>; 0 <=; 2 <~>)
% Maximal formula depth : 22 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 35 ( 33 usr; 8 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 3 con; 0-2 aty)
% Number of variables : 204 ( 0 sgn 189 !; 15 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f8589,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> k1_filter_0(X0) = u1_struct_0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d2_filter_0) ).
fof(f8637,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_filter_0(X1,X0)
=> ( v1_filter_0(X1,X0)
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ( r2_hidden(X2,X1)
<=> ~ r2_hidden(k7_lattices(X0,X2),X1) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t59_filter_0) ).
fof(f9358,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(f9363,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v4_lattices(k1_lattice2(X0))
& v5_lattices(k1_lattice2(X0))
& v6_lattices(k1_lattice2(X0))
& v7_lattices(k1_lattice2(X0))
& v8_lattices(k1_lattice2(X0))
& v9_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc6_lattice2) ).
fof(f9391,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(f9463,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(f12317,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_lattice4(X1,X0)
=> m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m2_lattice4) ).
fof(f13531,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_filter_2(X1,X0)
<=> m1_filter_0(X1,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_m1_filter_2) ).
fof(f13532,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(f13561,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& m2_filter_2(X1,X0) )
=> m1_filter_2(k15_filter_2(X0,X1),k1_lattice2(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k15_filter_2) ).
fof(f13562,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& m2_filter_2(X1,X0) )
=> k15_filter_2(X0,X1) = k7_filter_2(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k15_filter_2) ).
fof(f13595,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> k5_filter_2(X0,X1) = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d4_filter_2) ).
fof(f13601,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
=> k7_filter_2(X0,X1) = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d6_filter_2) ).
fof(f13619,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_filter_2(X1,X0)
=> ( r2_filter_2(X0,X1)
<=> v1_filter_0(k15_filter_2(X0,X1),k1_lattice2(X0)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t33_filter_2) ).
fof(f13647,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) )
=> ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v4_lattices(k1_lattice2(X0))
& v5_lattices(k1_lattice2(X0))
& v6_lattices(k1_lattice2(X0))
& v7_lattices(k1_lattice2(X0))
& v8_lattices(k1_lattice2(X0))
& v9_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v11_lattices(k1_lattice2(X0))
& v12_lattices(k1_lattice2(X0))
& v13_lattices(k1_lattice2(X0))
& v14_lattices(k1_lattice2(X0))
& v15_lattices(k1_lattice2(X0))
& v16_lattices(k1_lattice2(X0))
& v17_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc4_filter_2) ).
fof(f13649,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(k1_lattice2(X0)))
=> ( k7_lattices(k1_lattice2(X0),k5_filter_2(X0,X1)) = k7_lattices(X0,X1)
& k7_lattices(X0,k6_filter_2(X0,X2)) = k7_lattices(k1_lattice2(X0),X2) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t55_filter_2) ).
fof(f13651,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_filter_2(X1,X0)
=> ( r2_filter_2(X0,X1)
<=> ( X1 != u1_struct_0(X0)
& ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ( r2_hidden(X2,X1)
| r2_hidden(k7_lattices(X0,X2),X1) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t57_filter_2) ).
fof(f13653,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_filter_2(X1,X0)
=> ( r2_filter_2(X0,X1)
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ( r2_hidden(X2,X1)
<=> ~ r2_hidden(k7_lattices(X0,X2),X1) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t59_filter_2) ).
fof(f13654,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_filter_2(X1,X0)
=> ( r2_filter_2(X0,X1)
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ( r2_hidden(X2,X1)
<=> ~ r2_hidden(k7_lattices(X0,X2),X1) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f13653]) ).
fof(f13701,plain,
! [X0] :
( ! [X1] :
( m1_filter_2(X1,X0)
<=> m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f13531]) ).
fof(f13702,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,[],[f13701]) ).
fof(f13703,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,[],[f13532]) ).
fof(f13704,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,[],[f13703]) ).
fof(f13761,plain,
! [X0,X1] :
( m1_filter_2(k15_filter_2(X0,X1),k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m2_filter_2(X1,X0) ),
inference(ennf_transformation,[],[f13561]) ).
fof(f13762,plain,
! [X0,X1] :
( m1_filter_2(k15_filter_2(X0,X1),k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m2_filter_2(X1,X0) ),
inference(flattening,[],[f13761]) ).
fof(f13763,plain,
! [X0,X1] :
( k15_filter_2(X0,X1) = k7_filter_2(X0,X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m2_filter_2(X1,X0) ),
inference(ennf_transformation,[],[f13562]) ).
fof(f13764,plain,
! [X0,X1] :
( k15_filter_2(X0,X1) = k7_filter_2(X0,X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m2_filter_2(X1,X0) ),
inference(flattening,[],[f13763]) ).
fof(f13826,plain,
! [X0] :
( ! [X1] :
( k5_filter_2(X0,X1) = X1
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f13595]) ).
fof(f13827,plain,
! [X0] :
( ! [X1] :
( k5_filter_2(X0,X1) = X1
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13826]) ).
fof(f13838,plain,
! [X0] :
( ! [X1] :
( k7_filter_2(X0,X1) = 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,[],[f13601]) ).
fof(f13839,plain,
! [X0] :
( ! [X1] :
( k7_filter_2(X0,X1) = X1
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13838]) ).
fof(f13874,plain,
! [X0] :
( ! [X1] :
( ( r2_filter_2(X0,X1)
<=> v1_filter_0(k15_filter_2(X0,X1),k1_lattice2(X0)) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f13619]) ).
fof(f13875,plain,
! [X0] :
( ! [X1] :
( ( r2_filter_2(X0,X1)
<=> v1_filter_0(k15_filter_2(X0,X1),k1_lattice2(X0)) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13874]) ).
fof(f13930,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v4_lattices(k1_lattice2(X0))
& v5_lattices(k1_lattice2(X0))
& v6_lattices(k1_lattice2(X0))
& v7_lattices(k1_lattice2(X0))
& v8_lattices(k1_lattice2(X0))
& v9_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v11_lattices(k1_lattice2(X0))
& v12_lattices(k1_lattice2(X0))
& v13_lattices(k1_lattice2(X0))
& v14_lattices(k1_lattice2(X0))
& v15_lattices(k1_lattice2(X0))
& v16_lattices(k1_lattice2(X0))
& v17_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f13647]) ).
fof(f13931,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v4_lattices(k1_lattice2(X0))
& v5_lattices(k1_lattice2(X0))
& v6_lattices(k1_lattice2(X0))
& v7_lattices(k1_lattice2(X0))
& v8_lattices(k1_lattice2(X0))
& v9_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v11_lattices(k1_lattice2(X0))
& v12_lattices(k1_lattice2(X0))
& v13_lattices(k1_lattice2(X0))
& v14_lattices(k1_lattice2(X0))
& v15_lattices(k1_lattice2(X0))
& v16_lattices(k1_lattice2(X0))
& v17_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13930]) ).
fof(f13934,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( k7_lattices(k1_lattice2(X0),k5_filter_2(X0,X1)) = k7_lattices(X0,X1)
& k7_lattices(X0,k6_filter_2(X0,X2)) = k7_lattices(k1_lattice2(X0),X2) )
| ~ m1_subset_1(X2,u1_struct_0(k1_lattice2(X0))) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f13649]) ).
fof(f13935,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( k7_lattices(k1_lattice2(X0),k5_filter_2(X0,X1)) = k7_lattices(X0,X1)
& k7_lattices(X0,k6_filter_2(X0,X2)) = k7_lattices(k1_lattice2(X0),X2) )
| ~ m1_subset_1(X2,u1_struct_0(k1_lattice2(X0))) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13934]) ).
fof(f13938,plain,
! [X0] :
( ! [X1] :
( ( r2_filter_2(X0,X1)
<=> ( X1 != u1_struct_0(X0)
& ! [X2] :
( r2_hidden(X2,X1)
| r2_hidden(k7_lattices(X0,X2),X1)
| ~ m1_subset_1(X2,u1_struct_0(X0)) ) ) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f13651]) ).
fof(f13939,plain,
! [X0] :
( ! [X1] :
( ( r2_filter_2(X0,X1)
<=> ( X1 != u1_struct_0(X0)
& ! [X2] :
( r2_hidden(X2,X1)
| r2_hidden(k7_lattices(X0,X2),X1)
| ~ m1_subset_1(X2,u1_struct_0(X0)) ) ) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13938]) ).
fof(f13942,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ( r2_hidden(X2,X1)
<~> ~ r2_hidden(k7_lattices(X0,X2),X1) )
& m1_subset_1(X2,u1_struct_0(X0)) )
& r2_filter_2(X0,X1)
& m2_filter_2(X1,X0) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) ),
inference(ennf_transformation,[],[f13654]) ).
fof(f13943,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ( r2_hidden(X2,X1)
<~> ~ r2_hidden(k7_lattices(X0,X2),X1) )
& m1_subset_1(X2,u1_struct_0(X0)) )
& r2_filter_2(X0,X1)
& m2_filter_2(X1,X0) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) ),
inference(flattening,[],[f13942]) ).
fof(f13954,plain,
! [X0] :
( ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m2_lattice4(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f12317]) ).
fof(f13955,plain,
! [X0] :
( ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m2_lattice4(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13954]) ).
fof(f13996,plain,
! [X0] :
( k1_filter_0(X0) = u1_struct_0(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f8589]) ).
fof(f13997,plain,
! [X0] :
( k1_filter_0(X0) = u1_struct_0(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13996]) ).
fof(f14062,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,[],[f9391]) ).
fof(f14063,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,[],[f14062]) ).
fof(f14075,plain,
! [X0] :
( ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f9463]) ).
fof(f14078,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v4_lattices(k1_lattice2(X0))
& v5_lattices(k1_lattice2(X0))
& v6_lattices(k1_lattice2(X0))
& v7_lattices(k1_lattice2(X0))
& v8_lattices(k1_lattice2(X0))
& v9_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f9363]) ).
fof(f14079,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v4_lattices(k1_lattice2(X0))
& v5_lattices(k1_lattice2(X0))
& v6_lattices(k1_lattice2(X0))
& v7_lattices(k1_lattice2(X0))
& v8_lattices(k1_lattice2(X0))
& v9_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f14078]) ).
fof(f14080,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f9358]) ).
fof(f14081,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f14080]) ).
fof(f14443,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( r2_hidden(X2,X1)
<=> ~ r2_hidden(k7_lattices(X0,X2),X1) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ v1_filter_0(X1,X0)
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f8637]) ).
fof(f14444,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( r2_hidden(X2,X1)
<=> ~ r2_hidden(k7_lattices(X0,X2),X1) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ v1_filter_0(X1,X0)
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f14443]) ).
fof(f18291,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,[],[f13702]) ).
fof(f18325,plain,
! [X0] :
( ! [X1] :
( ( ( r2_filter_2(X0,X1)
| ~ v1_filter_0(k15_filter_2(X0,X1),k1_lattice2(X0)) )
& ( v1_filter_0(k15_filter_2(X0,X1),k1_lattice2(X0))
| ~ r2_filter_2(X0,X1) ) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f13875]) ).
fof(f18342,plain,
! [X0] :
( ! [X1] :
( ( ( r2_filter_2(X0,X1)
| u1_struct_0(X0) = X1
| ? [X2] :
( ~ r2_hidden(X2,X1)
& ~ r2_hidden(k7_lattices(X0,X2),X1)
& m1_subset_1(X2,u1_struct_0(X0)) ) )
& ( ( X1 != u1_struct_0(X0)
& ! [X2] :
( r2_hidden(X2,X1)
| r2_hidden(k7_lattices(X0,X2),X1)
| ~ m1_subset_1(X2,u1_struct_0(X0)) ) )
| ~ r2_filter_2(X0,X1) ) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f13939]) ).
fof(f18343,plain,
! [X0] :
( ! [X1] :
( ( ( r2_filter_2(X0,X1)
| u1_struct_0(X0) = X1
| ? [X2] :
( ~ r2_hidden(X2,X1)
& ~ r2_hidden(k7_lattices(X0,X2),X1)
& m1_subset_1(X2,u1_struct_0(X0)) ) )
& ( ( X1 != u1_struct_0(X0)
& ! [X2] :
( r2_hidden(X2,X1)
| r2_hidden(k7_lattices(X0,X2),X1)
| ~ m1_subset_1(X2,u1_struct_0(X0)) ) )
| ~ r2_filter_2(X0,X1) ) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f18342]) ).
fof(f18344,plain,
! [X0] :
( ! [X1] :
( ( ( r2_filter_2(X0,X1)
| u1_struct_0(X0) = X1
| ? [X2] :
( ~ r2_hidden(X2,X1)
& ~ r2_hidden(k7_lattices(X0,X2),X1)
& m1_subset_1(X2,u1_struct_0(X0)) ) )
& ( ( X1 != u1_struct_0(X0)
& ! [X3] :
( r2_hidden(X3,X1)
| r2_hidden(k7_lattices(X0,X3),X1)
| ~ m1_subset_1(X3,u1_struct_0(X0)) ) )
| ~ r2_filter_2(X0,X1) ) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(rectify,[],[f18343]) ).
fof(f18345,plain,
! [X0] :
( ! [X1] :
( ( ( r2_filter_2(X0,X1)
| u1_struct_0(X0) = X1
| ( ~ r2_hidden(sK42(X0,X1),X1)
& ~ r2_hidden(k7_lattices(X0,sK42(X0,X1)),X1)
& m1_subset_1(sK42(X0,X1),u1_struct_0(X0)) ) )
& ( ( X1 != u1_struct_0(X0)
& ! [X3] :
( r2_hidden(X3,X1)
| r2_hidden(k7_lattices(X0,X3),X1)
| ~ m1_subset_1(X3,u1_struct_0(X0)) ) )
| ~ r2_filter_2(X0,X1) ) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK42]),skolemize(X2,sK42(X0,X1))],[f18344]) ).
fof(f18348,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ( r2_hidden(k7_lattices(X0,X2),X1)
| ~ r2_hidden(X2,X1) )
& ( ~ r2_hidden(k7_lattices(X0,X2),X1)
| r2_hidden(X2,X1) )
& m1_subset_1(X2,u1_struct_0(X0)) )
& r2_filter_2(X0,X1)
& m2_filter_2(X1,X0) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) ),
inference(nnf_transformation,[],[f13943]) ).
fof(f18349,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ( r2_hidden(k7_lattices(X0,X2),X1)
| ~ r2_hidden(X2,X1) )
& ( ~ r2_hidden(k7_lattices(X0,X2),X1)
| r2_hidden(X2,X1) )
& m1_subset_1(X2,u1_struct_0(X0)) )
& r2_filter_2(X0,X1)
& m2_filter_2(X1,X0) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) ),
inference(flattening,[],[f18348]) ).
fof(f18350,plain,
( ( r2_hidden(k7_lattices(sK43,sK45),sK44)
| ~ r2_hidden(sK45,sK44) )
& ( ~ r2_hidden(k7_lattices(sK43,sK45),sK44)
| r2_hidden(sK45,sK44) )
& m1_subset_1(sK45,u1_struct_0(sK43))
& r2_filter_2(sK43,sK44)
& m2_filter_2(sK44,sK43)
& ~ v3_struct_0(sK43)
& v10_lattices(sK43)
& v17_lattices(sK43)
& l3_lattices(sK43) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK43,sK44,sK45]),skolemize(X0,sK43),skolemize(X1,sK44),skolemize(X2,sK45)],[f18349]) ).
fof(f18572,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( r2_hidden(X2,X1)
| r2_hidden(k7_lattices(X0,X2),X1) )
& ( ~ r2_hidden(k7_lattices(X0,X2),X1)
| ~ r2_hidden(X2,X1) ) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ v1_filter_0(X1,X0)
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f14444]) ).
fof(f19802,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,[],[f18291]) ).
fof(f19804,plain,
! [X0,X1] :
( ~ v10_lattices(X0)
| ~ m2_filter_2(X1,X0)
| v3_struct_0(X0)
| m2_lattice4(X1,X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13704]) ).
fof(f19837,plain,
! [X0,X1] :
( m1_filter_2(k15_filter_2(X0,X1),k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m2_filter_2(X1,X0) ),
inference(cnf_transformation,[],[f13762]) ).
fof(f19838,plain,
! [X0,X1] :
( ~ v10_lattices(X0)
| v3_struct_0(X0)
| k7_filter_2(X0,X1) = k15_filter_2(X0,X1)
| ~ l3_lattices(X0)
| ~ m2_filter_2(X1,X0) ),
inference(cnf_transformation,[],[f13764]) ).
fof(f19903,plain,
! [X0,X1] :
( ~ v10_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| k5_filter_2(X0,X1) = X1
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13827]) ).
fof(f19917,plain,
! [X0,X1] :
( ~ v10_lattices(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| k7_filter_2(X0,X1) = X1
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13839]) ).
fof(f19958,plain,
! [X0,X1] :
( ~ v10_lattices(X0)
| ~ r2_filter_2(X0,X1)
| ~ m2_filter_2(X1,X0)
| v3_struct_0(X0)
| v1_filter_0(k15_filter_2(X0,X1),k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f18325]) ).
fof(f20036,plain,
! [X0] :
( ~ v17_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| v17_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13931]) ).
fof(f20054,plain,
! [X2,X0,X1] :
( ~ v17_lattices(X0)
| ~ m1_subset_1(X2,u1_struct_0(k1_lattice2(X0)))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| k7_lattices(X0,X1) = k7_lattices(k1_lattice2(X0),k5_filter_2(X0,X1))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13935]) ).
fof(f20056,plain,
! [X3,X0,X1] :
( ~ v17_lattices(X0)
| r2_hidden(k7_lattices(X0,X3),X1)
| ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ r2_filter_2(X0,X1)
| ~ m2_filter_2(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| r2_hidden(X3,X1)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f18345]) ).
fof(f20064,plain,
l3_lattices(sK43),
inference(cnf_transformation,[],[f18350]) ).
fof(f20065,plain,
v17_lattices(sK43),
inference(cnf_transformation,[],[f18350]) ).
fof(f20066,plain,
v10_lattices(sK43),
inference(cnf_transformation,[],[f18350]) ).
fof(f20067,plain,
~ v3_struct_0(sK43),
inference(cnf_transformation,[],[f18350]) ).
fof(f20068,plain,
m2_filter_2(sK44,sK43),
inference(cnf_transformation,[],[f18350]) ).
fof(f20069,plain,
r2_filter_2(sK43,sK44),
inference(cnf_transformation,[],[f18350]) ).
fof(f20070,plain,
m1_subset_1(sK45,u1_struct_0(sK43)),
inference(cnf_transformation,[],[f18350]) ).
fof(f20071,plain,
( ~ r2_hidden(k7_lattices(sK43,sK45),sK44)
| r2_hidden(sK45,sK44) ),
inference(cnf_transformation,[],[f18350]) ).
fof(f20072,plain,
( r2_hidden(k7_lattices(sK43,sK45),sK44)
| ~ r2_hidden(sK45,sK44) ),
inference(cnf_transformation,[],[f18350]) ).
fof(f20091,plain,
! [X0,X1] :
( ~ m2_lattice4(X1,X0)
| m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13955]) ).
fof(f20131,plain,
! [X0] :
( ~ v10_lattices(X0)
| v3_struct_0(X0)
| u1_struct_0(X0) = k1_filter_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13997]) ).
fof(f20194,plain,
! [X0] :
( ~ l3_lattices(X0)
| v3_struct_0(X0)
| u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0)) ),
inference(cnf_transformation,[],[f14063]) ).
fof(f20216,plain,
! [X0] :
( ~ l3_lattices(X0)
| l3_lattices(k1_lattice2(X0)) ),
inference(cnf_transformation,[],[f14075]) ).
fof(f20219,plain,
! [X0] :
( ~ v10_lattices(X0)
| v3_struct_0(X0)
| v10_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f14079]) ).
fof(f20229,plain,
! [X0] :
( ~ v3_struct_0(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f14081]) ).
fof(f20764,plain,
! [X2,X0,X1] :
( ~ v1_filter_0(X1,X0)
| ~ r2_hidden(X2,X1)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ r2_hidden(k7_lattices(X0,X2),X1)
| ~ m1_filter_0(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f18572]) ).
fof(f28608,definition,
( spl882_36
<=> r2_hidden(sK45,sK44) ),
introduced(definition,[new_symbols(definition,[spl882_36])],[avatar_definition]) ).
fof(f28609,plain,
( r2_hidden(sK45,sK44)
| ~ spl882_36 ),
inference(avatar_component_clause,[],[f28608]) ).
fof(f28611,definition,
( spl882_37
<=> r2_hidden(k7_lattices(sK43,sK45),sK44) ),
introduced(definition,[new_symbols(definition,[spl882_37])],[avatar_definition]) ).
fof(f28612,plain,
( ~ r2_hidden(k7_lattices(sK43,sK45),sK44)
| spl882_37 ),
inference(avatar_component_clause,[],[f28611]) ).
fof(f28613,plain,
( spl882_36
| ~ spl882_37 ),
inference(avatar_split_clause,[],[f20071,f28611,f28608]) ).
fof(f28614,plain,
( ~ r2_hidden(sK45,sK44)
| spl882_36 ),
inference(avatar_component_clause,[],[f28608]) ).
fof(f28615,plain,
( r2_hidden(k7_lattices(sK43,sK45),sK44)
| ~ spl882_37 ),
inference(avatar_component_clause,[],[f28611]) ).
fof(f28616,plain,
( ~ spl882_36
| spl882_37 ),
inference(avatar_split_clause,[],[f20072,f28611,f28608]) ).
fof(f28973,plain,
( $false
| spl882_36
| spl882_37 ),
inference(unit_resulting_resolution,[],[f20056,f20064,f20065,f20066,f20067,f28614,f20068,f20069,f20070,f28612]) ).
fof(f28975,plain,
( spl882_36
| spl882_37 ),
inference(avatar_contradiction_clause,[],[f28973]) ).
fof(f29006,plain,
( v3_struct_0(sK43)
| u1_struct_0(sK43) = k1_filter_0(sK43)
| ~ l3_lattices(sK43) ),
inference(resolution,[],[f20131,f20066]) ).
fof(f29007,plain,
( u1_struct_0(sK43) = k1_filter_0(sK43)
| ~ l3_lattices(sK43) ),
inference(forward_subsumption_resolution,[],[f29006,f20067]) ).
fof(f29008,plain,
u1_struct_0(sK43) = k1_filter_0(sK43),
inference(forward_subsumption_resolution,[],[f29007,f20064]) ).
fof(f29010,plain,
m1_subset_1(sK45,k1_filter_0(sK43)),
inference(superposition,[],[f20070,f29008]) ).
fof(f29040,plain,
! [X0] :
( v3_struct_0(sK43)
| k7_filter_2(sK43,X0) = k15_filter_2(sK43,X0)
| ~ l3_lattices(sK43)
| ~ m2_filter_2(X0,sK43) ),
inference(resolution,[],[f19838,f20066]) ).
fof(f29041,plain,
! [X0] :
( k7_filter_2(sK43,X0) = k15_filter_2(sK43,X0)
| ~ l3_lattices(sK43)
| ~ m2_filter_2(X0,sK43) ),
inference(forward_subsumption_resolution,[],[f29040,f20067]) ).
fof(f29042,plain,
! [X0] :
( ~ m2_filter_2(X0,sK43)
| k7_filter_2(sK43,X0) = k15_filter_2(sK43,X0) ),
inference(forward_subsumption_resolution,[],[f29041,f20064]) ).
fof(f29043,plain,
k7_filter_2(sK43,sK44) = k15_filter_2(sK43,sK44),
inference(resolution,[],[f29042,f20068]) ).
fof(f29061,definition,
( spl882_48
<=> v3_struct_0(k1_lattice2(sK43)) ),
introduced(definition,[new_symbols(definition,[spl882_48])],[avatar_definition]) ).
fof(f29062,plain,
( v3_struct_0(k1_lattice2(sK43))
| ~ spl882_48 ),
inference(avatar_component_clause,[],[f29061]) ).
fof(f29067,plain,
! [X0] :
( ~ r2_filter_2(sK43,X0)
| ~ m2_filter_2(X0,sK43)
| v3_struct_0(sK43)
| v1_filter_0(k15_filter_2(sK43,X0),k1_lattice2(sK43))
| ~ l3_lattices(sK43) ),
inference(resolution,[],[f19958,f20066]) ).
fof(f29068,plain,
! [X0] :
( ~ r2_filter_2(sK43,X0)
| ~ m2_filter_2(X0,sK43)
| v1_filter_0(k15_filter_2(sK43,X0),k1_lattice2(sK43))
| ~ l3_lattices(sK43) ),
inference(forward_subsumption_resolution,[],[f29067,f20067]) ).
fof(f29069,plain,
! [X0] :
( ~ r2_filter_2(sK43,X0)
| ~ m2_filter_2(X0,sK43)
| v1_filter_0(k15_filter_2(sK43,X0),k1_lattice2(sK43)) ),
inference(forward_subsumption_resolution,[],[f29068,f20064]) ).
fof(f29070,plain,
( ~ m2_filter_2(sK44,sK43)
| v1_filter_0(k15_filter_2(sK43,sK44),k1_lattice2(sK43)) ),
inference(resolution,[],[f29069,f20069]) ).
fof(f29071,plain,
v1_filter_0(k15_filter_2(sK43,sK44),k1_lattice2(sK43)),
inference(forward_subsumption_resolution,[],[f29070,f20068]) ).
fof(f29072,plain,
v1_filter_0(k7_filter_2(sK43,sK44),k1_lattice2(sK43)),
inference(forward_demodulation,[],[f29071,f29043]) ).
fof(f29075,plain,
( v3_struct_0(sK43)
| u1_struct_0(sK43) = u1_struct_0(k1_lattice2(sK43)) ),
inference(resolution,[],[f20194,f20064]) ).
fof(f29076,plain,
u1_struct_0(sK43) = u1_struct_0(k1_lattice2(sK43)),
inference(forward_subsumption_resolution,[],[f29075,f20067]) ).
fof(f29077,plain,
k1_filter_0(sK43) = u1_struct_0(k1_lattice2(sK43)),
inference(forward_demodulation,[],[f29076,f29008]) ).
fof(f29084,plain,
l3_lattices(k1_lattice2(sK43)),
inference(resolution,[],[f20216,f20064]) ).
fof(f29100,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK43)))
| ~ m1_subset_1(X1,u1_struct_0(sK43))
| v3_struct_0(sK43)
| ~ v10_lattices(sK43)
| k7_lattices(sK43,X1) = k7_lattices(k1_lattice2(sK43),k5_filter_2(sK43,X1))
| ~ l3_lattices(sK43) ),
inference(resolution,[],[f20054,f20065]) ).
fof(f29101,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK43)))
| ~ m1_subset_1(X1,u1_struct_0(sK43))
| ~ v10_lattices(sK43)
| k7_lattices(sK43,X1) = k7_lattices(k1_lattice2(sK43),k5_filter_2(sK43,X1))
| ~ l3_lattices(sK43) ),
inference(forward_subsumption_resolution,[],[f29100,f20067]) ).
fof(f29102,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK43)))
| ~ m1_subset_1(X1,u1_struct_0(sK43))
| k7_lattices(sK43,X1) = k7_lattices(k1_lattice2(sK43),k5_filter_2(sK43,X1))
| ~ l3_lattices(sK43) ),
inference(forward_subsumption_resolution,[],[f29101,f20066]) ).
fof(f29103,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK43)))
| ~ m1_subset_1(X1,u1_struct_0(sK43))
| k7_lattices(sK43,X1) = k7_lattices(k1_lattice2(sK43),k5_filter_2(sK43,X1)) ),
inference(forward_subsumption_resolution,[],[f29102,f20064]) ).
fof(f29104,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_filter_0(sK43))
| ~ m1_subset_1(X1,u1_struct_0(sK43))
| k7_lattices(sK43,X1) = k7_lattices(k1_lattice2(sK43),k5_filter_2(sK43,X1)) ),
inference(forward_demodulation,[],[f29103,f29077]) ).
fof(f29105,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,k1_filter_0(sK43))
| ~ m1_subset_1(X0,k1_filter_0(sK43))
| k7_lattices(sK43,X1) = k7_lattices(k1_lattice2(sK43),k5_filter_2(sK43,X1)) ),
inference(forward_demodulation,[],[f29104,f29008]) ).
fof(f29107,definition,
( spl882_51
<=> ! [X0] : ~ m1_subset_1(X0,k1_filter_0(sK43)) ),
introduced(definition,[new_symbols(definition,[spl882_51])],[avatar_definition]) ).
fof(f29108,plain,
( ! [X0] : ~ m1_subset_1(X0,k1_filter_0(sK43))
| ~ spl882_51 ),
inference(avatar_component_clause,[],[f29107]) ).
fof(f29110,definition,
( spl882_52
<=> ! [X1] :
( ~ m1_subset_1(X1,k1_filter_0(sK43))
| k7_lattices(sK43,X1) = k7_lattices(k1_lattice2(sK43),k5_filter_2(sK43,X1)) ) ),
introduced(definition,[new_symbols(definition,[spl882_52])],[avatar_definition]) ).
fof(f29111,plain,
( ! [X1] :
( ~ m1_subset_1(X1,k1_filter_0(sK43))
| k7_lattices(sK43,X1) = k7_lattices(k1_lattice2(sK43),k5_filter_2(sK43,X1)) )
| ~ spl882_52 ),
inference(avatar_component_clause,[],[f29110]) ).
fof(f29112,plain,
( spl882_51
| spl882_52 ),
inference(avatar_split_clause,[],[f29105,f29110,f29107]) ).
fof(f29113,plain,
( $false
| ~ spl882_51 ),
inference(unit_resulting_resolution,[],[f29108,f29010]) ).
fof(f29116,plain,
~ spl882_51,
inference(avatar_contradiction_clause,[],[f29113]) ).
fof(f29118,plain,
( v3_struct_0(sK43)
| v10_lattices(k1_lattice2(sK43))
| ~ l3_lattices(sK43) ),
inference(resolution,[],[f20219,f20066]) ).
fof(f29120,plain,
( v10_lattices(k1_lattice2(sK43))
| ~ l3_lattices(sK43) ),
inference(forward_subsumption_resolution,[],[f29118,f20067]) ).
fof(f29124,plain,
v10_lattices(k1_lattice2(sK43)),
inference(forward_subsumption_resolution,[],[f29120,f20064]) ).
fof(f29134,plain,
( v3_struct_0(sK43)
| ~ l3_lattices(sK43)
| ~ spl882_48 ),
inference(resolution,[],[f20229,f29062]) ).
fof(f29136,plain,
( ~ l3_lattices(sK43)
| ~ spl882_48 ),
inference(forward_subsumption_resolution,[],[f29134,f20067]) ).
fof(f29137,plain,
( $false
| ~ spl882_48 ),
inference(forward_subsumption_resolution,[],[f29136,f20064]) ).
fof(f29138,plain,
~ spl882_48,
inference(avatar_contradiction_clause,[],[f29137]) ).
fof(f29211,definition,
( spl882_64
<=> m1_filter_0(k7_filter_2(sK43,sK44),k1_lattice2(sK43)) ),
introduced(definition,[new_symbols(definition,[spl882_64])],[avatar_definition]) ).
fof(f29226,plain,
( v3_struct_0(sK43)
| ~ v10_lattices(sK43)
| v17_lattices(k1_lattice2(sK43))
| ~ l3_lattices(sK43) ),
inference(resolution,[],[f20036,f20065]) ).
fof(f29228,plain,
( ~ v10_lattices(sK43)
| v17_lattices(k1_lattice2(sK43))
| ~ l3_lattices(sK43) ),
inference(forward_subsumption_resolution,[],[f29226,f20067]) ).
fof(f29229,plain,
( v17_lattices(k1_lattice2(sK43))
| ~ l3_lattices(sK43) ),
inference(forward_subsumption_resolution,[],[f29228,f20066]) ).
fof(f29233,plain,
v17_lattices(k1_lattice2(sK43)),
inference(forward_subsumption_resolution,[],[f29229,f20064]) ).
fof(f29275,plain,
! [X0] :
( ~ m2_filter_2(X0,sK43)
| v3_struct_0(sK43)
| m2_lattice4(X0,sK43)
| ~ l3_lattices(sK43) ),
inference(resolution,[],[f19804,f20066]) ).
fof(f29278,plain,
! [X0] :
( ~ m2_filter_2(X0,sK43)
| m2_lattice4(X0,sK43)
| ~ l3_lattices(sK43) ),
inference(forward_subsumption_resolution,[],[f29275,f20067]) ).
fof(f29283,plain,
! [X0] :
( ~ m2_filter_2(X0,sK43)
| m2_lattice4(X0,sK43) ),
inference(forward_subsumption_resolution,[],[f29278,f20064]) ).
fof(f29284,plain,
m2_lattice4(sK44,sK43),
inference(resolution,[],[f29283,f20068]) ).
fof(f29345,plain,
( k7_lattices(sK43,sK45) = k7_lattices(k1_lattice2(sK43),k5_filter_2(sK43,sK45))
| ~ spl882_52 ),
inference(resolution,[],[f29111,f29010]) ).
fof(f29371,plain,
! [X0] :
( ~ r2_hidden(X0,k7_filter_2(sK43,sK44))
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK43)))
| ~ r2_hidden(k7_lattices(k1_lattice2(sK43),X0),k7_filter_2(sK43,sK44))
| ~ m1_filter_0(k7_filter_2(sK43,sK44),k1_lattice2(sK43))
| v3_struct_0(k1_lattice2(sK43))
| ~ v10_lattices(k1_lattice2(sK43))
| ~ v17_lattices(k1_lattice2(sK43))
| ~ l3_lattices(k1_lattice2(sK43)) ),
inference(resolution,[],[f20764,f29072]) ).
fof(f29451,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK43)))
| v3_struct_0(sK43)
| k7_filter_2(sK43,X0) = X0
| ~ l3_lattices(sK43) ),
inference(resolution,[],[f19917,f20066]) ).
fof(f29454,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK43)))
| k7_filter_2(sK43,X0) = X0
| ~ l3_lattices(sK43) ),
inference(forward_subsumption_resolution,[],[f29451,f20067]) ).
fof(f29456,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK43)))
| k7_filter_2(sK43,X0) = X0 ),
inference(forward_subsumption_resolution,[],[f29454,f20064]) ).
fof(f29461,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k1_filter_0(sK43)))
| k7_filter_2(sK43,X0) = X0 ),
inference(forward_demodulation,[],[f29456,f29008]) ).
fof(f29494,plain,
( m1_filter_2(k7_filter_2(sK43,sK44),k1_lattice2(sK43))
| v3_struct_0(sK43)
| ~ v10_lattices(sK43)
| ~ l3_lattices(sK43)
| ~ m2_filter_2(sK44,sK43) ),
inference(superposition,[],[f19837,f29043]) ).
fof(f29495,plain,
( m1_filter_2(k7_filter_2(sK43,sK44),k1_lattice2(sK43))
| ~ v10_lattices(sK43)
| ~ l3_lattices(sK43)
| ~ m2_filter_2(sK44,sK43) ),
inference(forward_subsumption_resolution,[],[f29494,f20067]) ).
fof(f29497,plain,
( m1_filter_2(k7_filter_2(sK43,sK44),k1_lattice2(sK43))
| ~ l3_lattices(sK43)
| ~ m2_filter_2(sK44,sK43) ),
inference(forward_subsumption_resolution,[],[f29495,f20066]) ).
fof(f29499,plain,
( m1_filter_2(k7_filter_2(sK43,sK44),k1_lattice2(sK43))
| ~ m2_filter_2(sK44,sK43) ),
inference(forward_subsumption_resolution,[],[f29497,f20064]) ).
fof(f29501,plain,
m1_filter_2(k7_filter_2(sK43,sK44),k1_lattice2(sK43)),
inference(forward_subsumption_resolution,[],[f29499,f20068]) ).
fof(f29502,plain,
( m1_filter_0(k7_filter_2(sK43,sK44),k1_lattice2(sK43))
| v3_struct_0(k1_lattice2(sK43))
| ~ v10_lattices(k1_lattice2(sK43))
| ~ l3_lattices(k1_lattice2(sK43)) ),
inference(resolution,[],[f29501,f19802]) ).
fof(f29507,plain,
! [X0] :
( ~ r2_hidden(X0,k7_filter_2(sK43,sK44))
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK43)))
| ~ r2_hidden(k7_lattices(k1_lattice2(sK43),X0),k7_filter_2(sK43,sK44))
| ~ m1_filter_0(k7_filter_2(sK43,sK44),k1_lattice2(sK43))
| v3_struct_0(k1_lattice2(sK43))
| ~ v17_lattices(k1_lattice2(sK43))
| ~ l3_lattices(k1_lattice2(sK43)) ),
inference(forward_subsumption_resolution,[],[f29371,f29124]) ).
fof(f29508,plain,
( m1_filter_0(k7_filter_2(sK43,sK44),k1_lattice2(sK43))
| v3_struct_0(k1_lattice2(sK43))
| ~ l3_lattices(k1_lattice2(sK43)) ),
inference(forward_subsumption_resolution,[],[f29502,f29124]) ).
fof(f29509,plain,
! [X0] :
( ~ r2_hidden(X0,k7_filter_2(sK43,sK44))
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK43)))
| ~ r2_hidden(k7_lattices(k1_lattice2(sK43),X0),k7_filter_2(sK43,sK44))
| ~ m1_filter_0(k7_filter_2(sK43,sK44),k1_lattice2(sK43))
| v3_struct_0(k1_lattice2(sK43))
| ~ l3_lattices(k1_lattice2(sK43)) ),
inference(forward_subsumption_resolution,[],[f29507,f29233]) ).
fof(f29510,plain,
( m1_filter_0(k7_filter_2(sK43,sK44),k1_lattice2(sK43))
| v3_struct_0(k1_lattice2(sK43)) ),
inference(forward_subsumption_resolution,[],[f29508,f29084]) ).
fof(f29511,plain,
! [X0] :
( ~ r2_hidden(X0,k7_filter_2(sK43,sK44))
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK43)))
| ~ r2_hidden(k7_lattices(k1_lattice2(sK43),X0),k7_filter_2(sK43,sK44))
| ~ m1_filter_0(k7_filter_2(sK43,sK44),k1_lattice2(sK43))
| v3_struct_0(k1_lattice2(sK43)) ),
inference(forward_subsumption_resolution,[],[f29509,f29084]) ).
fof(f29513,plain,
( spl882_48
| spl882_64 ),
inference(avatar_split_clause,[],[f29510,f29211,f29061]) ).
fof(f29514,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_filter_0(sK43))
| ~ r2_hidden(X0,k7_filter_2(sK43,sK44))
| ~ r2_hidden(k7_lattices(k1_lattice2(sK43),X0),k7_filter_2(sK43,sK44))
| ~ m1_filter_0(k7_filter_2(sK43,sK44),k1_lattice2(sK43))
| v3_struct_0(k1_lattice2(sK43)) ),
inference(forward_demodulation,[],[f29511,f29077]) ).
fof(f29516,definition,
( spl882_89
<=> ! [X0] :
( ~ m1_subset_1(X0,k1_filter_0(sK43))
| ~ r2_hidden(k7_lattices(k1_lattice2(sK43),X0),k7_filter_2(sK43,sK44))
| ~ r2_hidden(X0,k7_filter_2(sK43,sK44)) ) ),
introduced(definition,[new_symbols(definition,[spl882_89])],[avatar_definition]) ).
fof(f29517,plain,
( ! [X0] :
( ~ r2_hidden(k7_lattices(k1_lattice2(sK43),X0),k7_filter_2(sK43,sK44))
| ~ m1_subset_1(X0,k1_filter_0(sK43))
| ~ r2_hidden(X0,k7_filter_2(sK43,sK44)) )
| ~ spl882_89 ),
inference(avatar_component_clause,[],[f29516]) ).
fof(f29518,plain,
( spl882_48
| ~ spl882_64
| spl882_89 ),
inference(avatar_split_clause,[],[f29514,f29516,f29211,f29061]) ).
fof(f29734,plain,
( m1_subset_1(sK44,k1_zfmisc_1(u1_struct_0(sK43)))
| v3_struct_0(sK43)
| ~ v10_lattices(sK43)
| ~ l3_lattices(sK43) ),
inference(resolution,[],[f20091,f29284]) ).
fof(f29735,plain,
( m1_subset_1(sK44,k1_zfmisc_1(u1_struct_0(sK43)))
| ~ v10_lattices(sK43)
| ~ l3_lattices(sK43) ),
inference(forward_subsumption_resolution,[],[f29734,f20067]) ).
fof(f29736,plain,
( m1_subset_1(sK44,k1_zfmisc_1(u1_struct_0(sK43)))
| ~ l3_lattices(sK43) ),
inference(forward_subsumption_resolution,[],[f29735,f20066]) ).
fof(f29737,plain,
m1_subset_1(sK44,k1_zfmisc_1(u1_struct_0(sK43))),
inference(forward_subsumption_resolution,[],[f29736,f20064]) ).
fof(f29738,plain,
m1_subset_1(sK44,k1_zfmisc_1(k1_filter_0(sK43))),
inference(forward_demodulation,[],[f29737,f29008]) ).
fof(f29739,plain,
sK44 = k7_filter_2(sK43,sK44),
inference(resolution,[],[f29738,f29461]) ).
fof(f29743,plain,
( ! [X0] :
( ~ r2_hidden(k7_lattices(k1_lattice2(sK43),X0),sK44)
| ~ m1_subset_1(X0,k1_filter_0(sK43))
| ~ r2_hidden(X0,sK44) )
| ~ spl882_89 ),
inference(superposition,[],[f29517,f29739]) ).
fof(f29764,plain,
( ~ r2_hidden(k7_lattices(sK43,sK45),sK44)
| ~ m1_subset_1(k5_filter_2(sK43,sK45),k1_filter_0(sK43))
| ~ r2_hidden(k5_filter_2(sK43,sK45),sK44)
| ~ spl882_52
| ~ spl882_89 ),
inference(superposition,[],[f29743,f29345]) ).
fof(f29885,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK43))
| v3_struct_0(sK43)
| k5_filter_2(sK43,X0) = X0
| ~ l3_lattices(sK43) ),
inference(resolution,[],[f19903,f20066]) ).
fof(f29888,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK43))
| k5_filter_2(sK43,X0) = X0
| ~ l3_lattices(sK43) ),
inference(forward_subsumption_resolution,[],[f29885,f20067]) ).
fof(f29890,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK43))
| k5_filter_2(sK43,X0) = X0 ),
inference(forward_subsumption_resolution,[],[f29888,f20064]) ).
fof(f29895,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_filter_0(sK43))
| k5_filter_2(sK43,X0) = X0 ),
inference(forward_demodulation,[],[f29890,f29008]) ).
fof(f29896,plain,
sK45 = k5_filter_2(sK43,sK45),
inference(resolution,[],[f29895,f29010]) ).
fof(f29907,plain,
( ~ m1_subset_1(k5_filter_2(sK43,sK45),k1_filter_0(sK43))
| ~ r2_hidden(k5_filter_2(sK43,sK45),sK44)
| ~ spl882_37
| ~ spl882_52
| ~ spl882_89 ),
inference(forward_subsumption_resolution,[],[f29764,f28615]) ).
fof(f29910,plain,
( ~ m1_subset_1(sK45,k1_filter_0(sK43))
| ~ r2_hidden(k5_filter_2(sK43,sK45),sK44)
| ~ spl882_37
| ~ spl882_52
| ~ spl882_89 ),
inference(forward_demodulation,[],[f29907,f29896]) ).
fof(f29911,plain,
( ~ r2_hidden(k5_filter_2(sK43,sK45),sK44)
| ~ spl882_37
| ~ spl882_52
| ~ spl882_89 ),
inference(forward_subsumption_resolution,[],[f29910,f29010]) ).
fof(f29912,plain,
( ~ r2_hidden(sK45,sK44)
| ~ spl882_37
| ~ spl882_52
| ~ spl882_89 ),
inference(forward_demodulation,[],[f29911,f29896]) ).
fof(f29913,plain,
( $false
| ~ spl882_36
| ~ spl882_37
| ~ spl882_52
| ~ spl882_89 ),
inference(forward_subsumption_resolution,[],[f29912,f28609]) ).
fof(f29914,plain,
( ~ spl882_36
| ~ spl882_37
| ~ spl882_52
| ~ spl882_89 ),
inference(avatar_contradiction_clause,[],[f29913]) ).
cnf(s14,plain,
( spl882_36
| ~ spl882_37 ),
inference(sat_conversion,[],[f28613]) ).
cnf(s15,plain,
( ~ spl882_36
| spl882_37 ),
inference(sat_conversion,[],[f28616]) ).
cnf(s36,plain,
( spl882_36
| spl882_37 ),
inference(sat_conversion,[],[f28975]) ).
cnf(s48,plain,
( spl882_51
| spl882_52 ),
inference(sat_conversion,[],[f29112]) ).
cnf(s50,plain,
~ spl882_51,
inference(sat_conversion,[],[f29116]) ).
cnf(s54,plain,
~ spl882_48,
inference(sat_conversion,[],[f29138]) ).
cnf(s93,plain,
( spl882_48
| spl882_64 ),
inference(sat_conversion,[],[f29513]) ).
cnf(s94,plain,
( spl882_48
| ~ spl882_64
| spl882_89 ),
inference(sat_conversion,[],[f29518]) ).
cnf(s127,plain,
( ~ spl882_36
| ~ spl882_37
| ~ spl882_52
| ~ spl882_89 ),
inference(sat_conversion,[],[f29914]) ).
cnf(s142,plain,
spl882_64,
inference(rat,[],[s93,s54]) ).
cnf(s170,plain,
spl882_89,
inference(rat,[],[s94,s54,s142]) ).
cnf(s181,plain,
spl882_52,
inference(rat,[],[s48,s50]) ).
cnf(s195,plain,
spl882_36,
inference(rat,[],[s14,s36]) ).
cnf(s196,plain,
~ spl882_37,
inference(rat,[],[s127,s170,s181,s195]) ).
cnf(s198,plain,
$false,
inference(rat,[],[s15,s196,s195]) ).
fof(f29915,plain,
$false,
inference(avatar_sat_refutation,[],[s198]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : LAT323+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.17/0.44 % Computer : n003.cluster.edu
% 0.17/0.44 % Model : x86_64 x86_64
% 0.17/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.44 % Memory : 8046.5625MB
% 0.17/0.44 % OS : Linux 6.8.0-71-generic
% 0.17/0.44 % CPULimit : 300
% 0.17/0.44 % WCLimit : 300
% 0.17/0.44 % DateTime : Sun Sep 27 14:39:12 UTC 2026
% 0.17/0.45 % CPUTime :
% 0.17/0.45 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.21/0.50 Running first-order theorem proving
% 0.21/0.50 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
% 22.46/4.43 % (610681)Detected formulas, will run a generic FOF schedule.
% 22.46/4.43 % (610694)dis-21_1_sil=8000:lcm=predicate:random_seed=4185228958:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2995 on theBenchmark for (2995ds/129Mi)
% 22.46/4.43 % (610694)Instruction limit reached!
% 22.46/4.43 % (610694)------------------------------
% 22.46/4.43 % (610694)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.46/4.43 % (610694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.46/4.43 % (610694)CaDiCaL version: 2.1.3
% 22.46/4.43 % (610694)Termination reason: Instruction limit
% 22.46/4.43 % (610694)Termination phase: Preprocessing 1
% 22.46/4.43 % (610694)Time elapsed: 0.080 s
% 22.46/4.43 % (610694)Peak memory usage: 104 MB
% 22.46/4.43 % (610694)Instructions burned: 129 (million)
% 22.46/4.43 % (610689)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=2430203400:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2995 on theBenchmark for (2995ds/134677Mi)
% 22.46/4.43 % (610692)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2882418437:i=119:av=off:ss=axioms_2995 on theBenchmark for (2995ds/119Mi)
% 22.46/4.43 % (610691)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2169317006:i=109:sd=1:ins=1:gsp=on:ss=axioms_2995 on theBenchmark for (2995ds/109Mi)
% 22.46/4.43 % (610688)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=923376099:i=141193_2995 on theBenchmark for (2995ds/141193Mi)
% 22.46/4.43 % (610693)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2920471148:s2a=on:i=139:gtg=position_2995 on theBenchmark for (2995ds/139Mi)
% 22.46/4.43 % (610690)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=3001337841:i=141695:sd=1:nm=32:gsp=on:ss=included_2995 on theBenchmark for (2995ds/141695Mi)
% 22.46/4.43 % (610693)Instruction limit reached!
% 22.46/4.43 % (610693)------------------------------
% 22.46/4.43 % (610693)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.46/4.43 % (610693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.46/4.43 % (610693)CaDiCaL version: 2.1.3
% 22.46/4.43 % (610693)Termination reason: Instruction limit
% 22.46/4.43 % (610693)Termination phase: Property scanning
% 22.46/4.43 % (610693)Time elapsed: 0.117 s
% 22.46/4.43 % (610693)Peak memory usage: 103 MB
% 22.46/4.43 % (610693)Instructions burned: 139 (million)
% 22.46/4.43 % (610691)Instruction limit reached!
% 22.46/4.43 % (610691)------------------------------
% 22.46/4.43 % (610691)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.46/4.43 % (610691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.46/4.43 % (610691)CaDiCaL version: 2.1.3
% 22.46/4.43 % (610691)Termination reason: Instruction limit
% 22.46/4.43 % (610691)Termination phase: Saturation
% 22.46/4.43 % (610691)Time elapsed: 0.123 s
% 22.46/4.43 % (610691)Peak memory usage: 107 MB
% 22.46/4.43 % (610691)Instructions burned: 110 (million)
% 22.46/4.43 % (610692)Instruction limit reached!
% 22.46/4.43 % (610692)------------------------------
% 22.46/4.43 % (610692)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.46/4.43 % (610692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.46/4.43 % (610692)CaDiCaL version: 2.1.3
% 22.46/4.43 % (610692)Termination reason: Instruction limit
% 22.46/4.43 % (610692)Termination phase: Function definition elimination
% 22.46/4.43 % (610692)Time elapsed: 0.135 s
% 22.46/4.43 % (610692)Peak memory usage: 106 MB
% 22.46/4.43 % (610692)Instructions burned: 119 (million)
% 22.46/4.43 % (610696)lrs+10_1_sil=8000:sp=occurrence:random_seed=375971198:i=285:sd=3:ss=axioms:sgt=8_2993 on theBenchmark for (2993ds/285Mi)
% 22.46/4.43 % (610704)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3718549794:i=325:sd=1:ss=axioms:sgt=32_2991 on theBenchmark for (2991ds/325Mi)
% 22.46/4.43 % (610696)Instruction limit reached!
% 22.46/4.43 % (610696)------------------------------
% 22.46/4.43 % (610696)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.46/4.43 % (610696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.46/4.43 % (610696)CaDiCaL version: 2.1.3
% 22.46/4.43 % (610696)Termination reason: Instruction limit
% 22.46/4.43 % (610696)Termination phase: Saturation
% 20.70/4.68 % (610696)Time elapsed: 0.164 s
% 20.70/4.68 % (610696)Peak memory usage: 110 MB
% 20.70/4.68 % (610696)Instructions burned: 286 (million)
% 20.70/4.68 % (610703)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1931329805:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2991 on theBenchmark for (2991ds/157Mi)
% 20.70/4.68 % (610705)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=3165195173:s2a=on:i=248:s2at=1.23:gtg=position_2991 on theBenchmark for (2991ds/248Mi)
% 20.70/4.68 % (610703)Instruction limit reached!
% 20.70/4.68 % (610703)------------------------------
% 20.70/4.68 % (610703)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.70/4.68 % (610703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.70/4.68 % (610703)CaDiCaL version: 2.1.3
% 20.70/4.68 % (610703)Termination reason: Instruction limit
% 20.70/4.68 % (610703)Termination phase: Property scanning
% 20.70/4.68 % (610703)Time elapsed: 0.130 s
% 20.70/4.68 % (610703)Peak memory usage: 103 MB
% 20.70/4.68 % (610703)Instructions burned: 157 (million)
% 20.70/4.68 % (610708)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=179637206:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2989 on theBenchmark for (2989ds/294Mi)
% 20.70/4.68 % (610705)Instruction limit reached!
% 20.70/4.68 % (610705)------------------------------
% 20.70/4.68 % (610705)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.70/4.68 % (610705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.70/4.68 % (610705)CaDiCaL version: 2.1.3
% 20.70/4.68 % (610705)Termination reason: Instruction limit
% 20.70/4.68 % (610705)Termination phase: SInE selection
% 20.70/4.68 % (610705)Time elapsed: 0.225 s
% 20.70/4.68 % (610705)Peak memory usage: 103 MB
% 20.70/4.68 % (610705)Instructions burned: 248 (million)
% 20.70/4.68 % (610704)Instruction limit reached!
% 20.70/4.68 % (610704)------------------------------
% 20.70/4.68 % (610704)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.70/4.68 % (610704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.70/4.68 % (610704)CaDiCaL version: 2.1.3
% 20.70/4.68 % (610704)Termination reason: Instruction limit
% 20.70/4.68 % (610704)Termination phase: Saturation
% 20.70/4.68 % (610704)Time elapsed: 0.344 s
% 20.70/4.68 % (610704)Peak memory usage: 110 MB
% 20.70/4.68 % (610704)Instructions burned: 325 (million)
% 20.70/4.68 % (610708)Instruction limit reached!
% 20.70/4.68 % (610708)------------------------------
% 20.70/4.68 % (610708)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.70/4.68 % (610708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.70/4.68 % (610708)CaDiCaL version: 2.1.3
% 20.70/4.68 % (610708)Termination reason: Instruction limit
% 20.70/4.68 % (610708)Termination phase: Saturation
% 20.70/4.68 % (610708)Time elapsed: 0.159 s
% 20.70/4.68 % (610708)Peak memory usage: 110 MB
% 20.70/4.68 % (610708)Instructions burned: 297 (million)
% 20.70/4.68 % (610711)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3459345415:i=2350_2987 on theBenchmark for (2987ds/2350Mi)
% 20.70/4.68 % (610713)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2322160908:cts=off:i=113:fsr=off:ss=included:sgt=4_2986 on theBenchmark for (2986ds/113Mi)
% 20.70/4.68 % (610714)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2362207768:i=127:av=off:fsr=off:sup=off_2986 on theBenchmark for (2986ds/127Mi)
% 20.70/4.68 % (610713)Instruction limit reached!
% 20.70/4.68 % (610713)------------------------------
% 20.70/4.68 % (610713)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.70/4.68 % (610713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.70/4.68 % (610713)CaDiCaL version: 2.1.3
% 20.70/4.68 % (610713)Termination reason: Instruction limit
% 20.70/4.68 % (610713)Termination phase: Preprocessing 3
% 20.70/4.68 % (610713)Time elapsed: 0.087 s
% 20.70/4.68 % (610713)Peak memory usage: 105 MB
% 20.70/4.68 % (610713)Instructions burned: 113 (million)
% 20.70/4.68 % (610715)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3509637764:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2985 on theBenchmark for (2985ds/114Mi)
% 20.70/4.68 % (610715)Instruction limit reached!
% 20.70/4.68 % (610715)------------------------------
% 20.70/4.68 % (610715)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.70/4.68 % (610715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.70/4.68 % (610715)CaDiCaL version: 2.1.3
% 20.70/4.68 % (610715)Termination reason: Instruction limit
% 20.70/4.68 % (610715)Termination phase: Property scanning
% 20.70/4.68 % (610715)Time elapsed: 0.054 s
% 20.70/4.68 % (610715)Peak memory usage: 103 MB
% 20.70/4.68 % (610715)Instructions burned: 114 (million)
% 20.70/4.68 % (610714)Instruction limit reached!
% 20.70/4.68 % (610714)------------------------------
% 20.70/4.68 % (610714)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.70/4.68 % (610714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.70/4.68 % (610714)CaDiCaL version: 2.1.3
% 20.70/4.68 % (610714)Termination reason: Instruction limit
% 20.70/4.68 % (610714)Termination phase: Preprocessing 2
% 20.70/4.68 % (610714)Time elapsed: 0.155 s
% 20.70/4.68 % (610714)Peak memory usage: 106 MB
% 20.70/4.68 % (610714)Instructions burned: 127 (million)
% 20.70/4.68 % (610720)lrs+10_1_sil=8000:sp=occurrence:random_seed=2833520595:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2983 on theBenchmark for (2983ds/907Mi)
% 20.70/4.68 % (610721)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3841506735:i=437:sd=1:aac=none:ss=included_2982 on theBenchmark for (2982ds/437Mi)
% 20.70/4.68 % (610722)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3460308601:i=5202:ss=axioms:sgt=16_2981 on theBenchmark for (2981ds/5202Mi)
% 20.70/4.68 % (610721)Instruction limit reached!
% 20.70/4.68 % (610721)------------------------------
% 20.70/4.68 % (610721)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.70/4.68 % (610721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.70/4.68 % (610721)CaDiCaL version: 2.1.3
% 20.70/4.68 % (610721)Termination reason: Instruction limit
% 20.70/4.68 % (610721)Termination phase: Saturation
% 20.70/4.68 % (610721)Time elapsed: 0.213 s
% 20.70/4.68 % (610721)Peak memory usage: 109 MB
% 20.70/4.68 % (610721)Instructions burned: 440 (million)
% 20.70/4.68 % (610726)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2298338545:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2978 on theBenchmark for (2978ds/134Mi)
% 20.70/4.68 % (610726)Instruction limit reached!
% 20.70/4.68 % (610726)------------------------------
% 20.70/4.68 % (610726)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.70/4.68 % (610726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.70/4.68 % (610726)CaDiCaL version: 2.1.3
% 20.70/4.68 % (610726)Termination reason: Instruction limit
% 20.70/4.68 % (610726)Termination phase: Property scanning
% 20.70/4.68 % (610726)Time elapsed: 0.141 s
% 20.70/4.68 % (610726)Peak memory usage: 106 MB
% 20.70/4.68 % (610726)Instructions burned: 135 (million)
% 20.70/4.68 % (610728)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3837496588:st=8:i=592:sd=3:ep=RST:ss=axioms_2974 on theBenchmark for (2974ds/592Mi)
% 20.70/4.68 % (610720)Instruction limit reached!
% 20.70/4.68 % (610720)------------------------------
% 20.70/4.68 % (610720)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.70/4.68 % (610720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.70/4.68 % (610720)CaDiCaL version: 2.1.3
% 20.70/4.68 % (610720)Termination reason: Instruction limit
% 20.70/4.68 % (610720)Termination phase: Saturation
% 20.70/4.68 % (610720)Time elapsed: 0.957 s
% 20.70/4.68 % (610720)Peak memory usage: 121 MB
% 20.70/4.68 % (610720)Instructions burned: 907 (million)
% 20.70/4.68 % (610730)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=120489187:st=3:i=13193:sd=3:ss=axioms_2971 on theBenchmark for (2971ds/13193Mi)
% 20.70/4.68 % (610728)Instruction limit reached!
% 20.70/4.68 % (610728)------------------------------
% 20.70/4.68 % (610728)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.70/4.68 % (610728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.70/4.68 % (610728)CaDiCaL version: 2.1.3
% 20.70/4.68 % (610728)Termination reason: Instruction limit
% 20.70/4.68 % (610728)Termination phase: Property scanning
% 20.70/4.68 % (610728)Time elapsed: 0.524 s
% 20.70/4.68 % (610728)Peak memory usage: 122 MB
% 20.70/4.68 % (610728)Instructions burned: 592 (million)
% 20.70/4.68 % (610689)First to succeed.
% 20.70/4.68 % (610689)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-610681"
% 20.70/4.68 % (610734)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=739948762:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2966 on theBenchmark for (2966ds/125Mi)
% 20.70/4.68 % (610734)Instruction limit reached!
% 20.70/4.68 % (610734)------------------------------
% 20.70/4.68 % (610734)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.70/4.68 % (610734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.70/4.68 % (610734)CaDiCaL version: 2.1.3
% 20.70/4.68 % (610734)Termination reason: Instruction limit
% 20.70/4.68 % (610734)Termination phase: Property scanning
% 20.70/4.68 % (610734)Time elapsed: 0.085 s
% 20.70/4.68 % (610734)Peak memory usage: 102 MB
% 20.70/4.68 % (610734)Instructions burned: 126 (million)
% 20.70/4.68 % (610689)Refutation found. Thanks to Tanya!
% 20.70/4.68 % SZS status Theorem for theBenchmark
% 20.70/4.68 % SZS output start Proof for theBenchmark
% See solution above
% 24.56/4.81 % (610689)------------------------------
% 24.56/4.81 % (610689)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.56/4.81 % (610689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.56/4.81 % (610689)CaDiCaL version: 2.1.3
% 24.56/4.81 % (610689)Termination reason: Refutation
% 24.56/4.81 % (610689)Time elapsed: 2.811 s
% 24.56/4.81 % (610689)Peak memory usage: 242 MB
% 24.56/4.81 % (610689)Instructions burned: 4207 (million)
% 24.56/4.81 % (610689)------------------------------
% 24.56/4.81 % (610689)------------------------------
% 24.56/4.81 % (610681)Success in time 3.816 s
% 24.56/4.81 % Vampire exiting
%------------------------------------------------------------------------------