%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT321+2 : 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:54 AM UTC 2026
% Result : Theorem 29.22s 5.28s
% Output : Refutation 29.91s
% Verified :
% SZS Type : Refutation
% Derivation depth : 35
% Number of leaves : 35
% Syntax : Number of formulae : 317 ( 35 unt; 14 def)
% Number of atoms : 1468 ( 155 equ)
% Maximal formula atoms : 20 ( 4 avg)
% Number of connectives : 1836 ( 685 ~; 854 |; 225 &)
% ( 32 <=>; 38 =>; 0 <=; 2 <~>)
% Maximal formula depth : 22 ( 6 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 44 ( 42 usr; 15 prp; 0-3 aty)
% Number of functors : 16 ( 16 usr; 3 con; 0-2 aty)
% Number of variables : 262 ( 0 sgn 243 !; 19 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f480,axiom,
! [X0,X1] :
( ( ~ v1_xboole_0(X0)
=> ( m1_subset_1(X1,X0)
<=> r2_hidden(X1,X0) ) )
& ( v1_xboole_0(X0)
=> ( m1_subset_1(X1,X0)
<=> v1_xboole_0(X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d2_subset_1) ).
fof(f581,axiom,
! [X0,X1] :
( r2_hidden(X0,X1)
=> m1_subset_1(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t1_subset) ).
fof(f2456,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(f2502,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)
<=> ( 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_0) ).
fof(f2564,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(f2569,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(f2597,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(f2669,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(f2857,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_lattice4(X1,X0)
=> m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m2_lattice4) ).
fof(f2872,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_filter_2(X1,X0)
<=> m1_filter_0(X1,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_m1_filter_2) ).
fof(f2873,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(f2902,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(f2903,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(f2936,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(f2942,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(f2953,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> k17_filter_2(X0) = u1_struct_0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d8_filter_2) ).
fof(f2959,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_filter_2(X1,X0)
=> ( r2_filter_2(X0,X1)
<=> ( X1 != u1_struct_0(X0)
& ! [X2] :
( m2_filter_2(X2,X0)
=> ( r1_tarski(X1,X2)
=> ( X2 = u1_struct_0(X0)
| r1_filter_2(u1_struct_0(X0),X1,X2) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d10_filter_2) ).
fof(f2960,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(f2988,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(f2989,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> k7_lattices(k1_lattice2(X0),k5_filter_2(X0,X1)) = k7_lattices(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l70_filter_2) ).
fof(f2992,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)
<=> ( 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(f2993,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)
<=> ( 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) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f2992]) ).
fof(f3017,plain,
! [X0] :
( ! [X1] :
( m1_filter_2(X1,X0)
<=> m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2872]) ).
fof(f3018,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,[],[f3017]) ).
fof(f3019,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,[],[f2873]) ).
fof(f3020,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,[],[f3019]) ).
fof(f3077,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,[],[f2902]) ).
fof(f3078,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,[],[f3077]) ).
fof(f3079,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,[],[f2903]) ).
fof(f3080,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,[],[f3079]) ).
fof(f3142,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,[],[f2936]) ).
fof(f3143,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,[],[f3142]) ).
fof(f3154,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,[],[f2942]) ).
fof(f3155,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,[],[f3154]) ).
fof(f3176,plain,
! [X0] :
( k17_filter_2(X0) = u1_struct_0(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2953]) ).
fof(f3177,plain,
! [X0] :
( k17_filter_2(X0) = u1_struct_0(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f3176]) ).
fof(f3188,plain,
! [X0] :
( ! [X1] :
( ( r2_filter_2(X0,X1)
<=> ( X1 != u1_struct_0(X0)
& ! [X2] :
( X2 = u1_struct_0(X0)
| r1_filter_2(u1_struct_0(X0),X1,X2)
| ~ r1_tarski(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,[],[f2959]) ).
fof(f3189,plain,
! [X0] :
( ! [X1] :
( ( r2_filter_2(X0,X1)
<=> ( X1 != u1_struct_0(X0)
& ! [X2] :
( X2 = u1_struct_0(X0)
| r1_filter_2(u1_struct_0(X0),X1,X2)
| ~ r1_tarski(X1,X2)
| ~ m2_filter_2(X2,X0) ) ) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f3188]) ).
fof(f3190,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,[],[f2960]) ).
fof(f3191,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,[],[f3190]) ).
fof(f3246,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,[],[f2988]) ).
fof(f3247,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,[],[f3246]) ).
fof(f3248,plain,
! [X0] :
( ! [X1] :
( k7_lattices(k1_lattice2(X0),k5_filter_2(X0,X1)) = k7_lattices(X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2989]) ).
fof(f3249,plain,
! [X0] :
( ! [X1] :
( k7_lattices(k1_lattice2(X0),k5_filter_2(X0,X1)) = k7_lattices(X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f3248]) ).
fof(f3254,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,[],[f2993]) ).
fof(f3255,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,[],[f3254]) ).
fof(f3260,plain,
! [X0,X1] :
( ( ( m1_subset_1(X1,X0)
<=> r2_hidden(X1,X0) )
| v1_xboole_0(X0) )
& ( ( m1_subset_1(X1,X0)
<=> v1_xboole_0(X1) )
| ~ v1_xboole_0(X0) ) ),
inference(ennf_transformation,[],[f480]) ).
fof(f3265,plain,
! [X0] :
( ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m2_lattice4(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2857]) ).
fof(f3266,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,[],[f3265]) ).
fof(f3312,plain,
! [X0] :
( k1_filter_0(X0) = u1_struct_0(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2456]) ).
fof(f3313,plain,
! [X0] :
( k1_filter_0(X0) = u1_struct_0(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f3312]) ).
fof(f3378,plain,
! [X0] :
( ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2669]) ).
fof(f3381,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,[],[f2569]) ).
fof(f3382,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,[],[f3381]) ).
fof(f3383,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2564]) ).
fof(f3384,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f3383]) ).
fof(f3543,plain,
! [X0,X1] :
( m1_subset_1(X0,X1)
| ~ r2_hidden(X0,X1) ),
inference(ennf_transformation,[],[f581]) ).
fof(f3550,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,[],[f2597]) ).
fof(f3551,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,[],[f3550]) ).
fof(f3742,plain,
! [X0] :
( ! [X1] :
( ( v1_filter_0(X1,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)) ) ) )
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2502]) ).
fof(f3743,plain,
! [X0] :
( ! [X1] :
( ( v1_filter_0(X1,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)) ) ) )
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f3742]) ).
fof(f4907,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,[],[f3018]) ).
fof(f4937,plain,
! [X0] :
( ! [X1] :
( ( ( r2_filter_2(X0,X1)
| u1_struct_0(X0) = X1
| ? [X2] :
( u1_struct_0(X0) != X2
& ~ r1_filter_2(u1_struct_0(X0),X1,X2)
& r1_tarski(X1,X2)
& m2_filter_2(X2,X0) ) )
& ( ( X1 != u1_struct_0(X0)
& ! [X2] :
( X2 = u1_struct_0(X0)
| r1_filter_2(u1_struct_0(X0),X1,X2)
| ~ r1_tarski(X1,X2)
| ~ m2_filter_2(X2,X0) ) )
| ~ r2_filter_2(X0,X1) ) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f3189]) ).
fof(f4938,plain,
! [X0] :
( ! [X1] :
( ( ( r2_filter_2(X0,X1)
| u1_struct_0(X0) = X1
| ? [X2] :
( u1_struct_0(X0) != X2
& ~ r1_filter_2(u1_struct_0(X0),X1,X2)
& r1_tarski(X1,X2)
& m2_filter_2(X2,X0) ) )
& ( ( X1 != u1_struct_0(X0)
& ! [X2] :
( X2 = u1_struct_0(X0)
| r1_filter_2(u1_struct_0(X0),X1,X2)
| ~ r1_tarski(X1,X2)
| ~ m2_filter_2(X2,X0) ) )
| ~ r2_filter_2(X0,X1) ) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f4937]) ).
fof(f4939,plain,
! [X0] :
( ! [X1] :
( ( ( r2_filter_2(X0,X1)
| u1_struct_0(X0) = X1
| ? [X2] :
( u1_struct_0(X0) != X2
& ~ r1_filter_2(u1_struct_0(X0),X1,X2)
& r1_tarski(X1,X2)
& m2_filter_2(X2,X0) ) )
& ( ( X1 != u1_struct_0(X0)
& ! [X3] :
( u1_struct_0(X0) = X3
| r1_filter_2(u1_struct_0(X0),X1,X3)
| ~ r1_tarski(X1,X3)
| ~ m2_filter_2(X3,X0) ) )
| ~ r2_filter_2(X0,X1) ) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(rectify,[],[f4938]) ).
fof(f4940,plain,
! [X0] :
( ! [X1] :
( ( ( r2_filter_2(X0,X1)
| u1_struct_0(X0) = X1
| ( u1_struct_0(X0) != sK18(X0,X1)
& ~ r1_filter_2(u1_struct_0(X0),X1,sK18(X0,X1))
& r1_tarski(X1,sK18(X0,X1))
& m2_filter_2(sK18(X0,X1),X0) ) )
& ( ( X1 != u1_struct_0(X0)
& ! [X3] :
( u1_struct_0(X0) = X3
| r1_filter_2(u1_struct_0(X0),X1,X3)
| ~ r1_tarski(X1,X3)
| ~ m2_filter_2(X3,X0) ) )
| ~ r2_filter_2(X0,X1) ) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18]),skolemize(X2,sK18(X0,X1))],[f4939]) ).
fof(f4941,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,[],[f3191]) ).
fof(f4958,plain,
? [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)) )
| ~ 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)) ) )
| 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,[],[f3255]) ).
fof(f4959,plain,
? [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)) )
| ~ 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)) ) )
| 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,[],[f4958]) ).
fof(f4960,plain,
? [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)) )
| ~ r2_filter_2(X0,X1) )
& ( ( 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,[],[f4959]) ).
fof(f4961,plain,
( ( sK27 = u1_struct_0(sK26)
| ( ~ r2_hidden(sK28,sK27)
& ~ r2_hidden(k7_lattices(sK26,sK28),sK27)
& m1_subset_1(sK28,u1_struct_0(sK26)) )
| ~ r2_filter_2(sK26,sK27) )
& ( ( sK27 != u1_struct_0(sK26)
& ! [X3] :
( r2_hidden(X3,sK27)
| r2_hidden(k7_lattices(sK26,X3),sK27)
| ~ m1_subset_1(X3,u1_struct_0(sK26)) ) )
| r2_filter_2(sK26,sK27) )
& m2_filter_2(sK27,sK26)
& ~ v3_struct_0(sK26)
& v10_lattices(sK26)
& v17_lattices(sK26)
& l3_lattices(sK26) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK26,sK27,sK28]),skolemize(X0,sK26),skolemize(X1,sK27),skolemize(X2,sK28)],[f4960]) ).
fof(f4965,plain,
! [X0,X1] :
( ( ( ( m1_subset_1(X1,X0)
| ~ r2_hidden(X1,X0) )
& ( r2_hidden(X1,X0)
| ~ m1_subset_1(X1,X0) ) )
| v1_xboole_0(X0) )
& ( ( ( m1_subset_1(X1,X0)
| ~ v1_xboole_0(X1) )
& ( v1_xboole_0(X1)
| ~ m1_subset_1(X1,X0) ) )
| ~ v1_xboole_0(X0) ) ),
inference(nnf_transformation,[],[f3260]) ).
fof(f5179,plain,
! [X0] :
( ! [X1] :
( ( ( v1_filter_0(X1,X0)
| 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)) ) )
| ~ 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,[],[f3743]) ).
fof(f5180,plain,
! [X0] :
( ! [X1] :
( ( ( v1_filter_0(X1,X0)
| 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)) ) )
| ~ 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,[],[f5179]) ).
fof(f5181,plain,
! [X0] :
( ! [X1] :
( ( ( v1_filter_0(X1,X0)
| 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)) ) )
| ~ v1_filter_0(X1,X0) ) )
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(rectify,[],[f5180]) ).
fof(f5182,plain,
! [X0] :
( ! [X1] :
( ( ( v1_filter_0(X1,X0)
| u1_struct_0(X0) = X1
| ( ~ r2_hidden(sK161(X0,X1),X1)
& ~ r2_hidden(k7_lattices(X0,sK161(X0,X1)),X1)
& m1_subset_1(sK161(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)) ) )
| ~ v1_filter_0(X1,X0) ) )
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK161]),skolemize(X2,sK161(X0,X1))],[f5181]) ).
fof(f5595,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,[],[f4907]) ).
fof(f5597,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,[],[f3020]) ).
fof(f5598,plain,
! [X0,X1] :
( ~ v1_xboole_0(X1)
| ~ m2_filter_2(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f3020]) ).
fof(f5630,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,[],[f3078]) ).
fof(f5631,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,[],[f3080]) ).
fof(f5696,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,[],[f3143]) ).
fof(f5710,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,[],[f3155]) ).
fof(f5735,plain,
! [X0] :
( ~ v10_lattices(X0)
| v3_struct_0(X0)
| u1_struct_0(X0) = k17_filter_2(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f3177]) ).
fof(f5746,plain,
! [X0,X1] :
( u1_struct_0(X0) != X1
| ~ r2_filter_2(X0,X1)
| ~ m2_filter_2(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f4940]) ).
fof(f5751,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(cnf_transformation,[],[f4941]) ).
fof(f5752,plain,
! [X0,X1] :
( ~ 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(cnf_transformation,[],[f4941]) ).
fof(f5829,plain,
! [X0] :
( ~ v17_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| v17_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f3247]) ).
fof(f5845,plain,
! [X0,X1] :
( ~ v17_lattices(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,[],[f3249]) ).
fof(f5849,plain,
l3_lattices(sK26),
inference(cnf_transformation,[],[f4961]) ).
fof(f5850,plain,
v17_lattices(sK26),
inference(cnf_transformation,[],[f4961]) ).
fof(f5851,plain,
v10_lattices(sK26),
inference(cnf_transformation,[],[f4961]) ).
fof(f5852,plain,
~ v3_struct_0(sK26),
inference(cnf_transformation,[],[f4961]) ).
fof(f5853,plain,
m2_filter_2(sK27,sK26),
inference(cnf_transformation,[],[f4961]) ).
fof(f5854,plain,
! [X3] :
( r2_hidden(X3,sK27)
| r2_hidden(k7_lattices(sK26,X3),sK27)
| ~ m1_subset_1(X3,u1_struct_0(sK26))
| r2_filter_2(sK26,sK27) ),
inference(cnf_transformation,[],[f4961]) ).
fof(f5855,plain,
( sK27 != u1_struct_0(sK26)
| r2_filter_2(sK26,sK27) ),
inference(cnf_transformation,[],[f4961]) ).
fof(f5856,plain,
( sK27 = u1_struct_0(sK26)
| m1_subset_1(sK28,u1_struct_0(sK26))
| ~ r2_filter_2(sK26,sK27) ),
inference(cnf_transformation,[],[f4961]) ).
fof(f5857,plain,
( sK27 = u1_struct_0(sK26)
| ~ r2_hidden(k7_lattices(sK26,sK28),sK27)
| ~ r2_filter_2(sK26,sK27) ),
inference(cnf_transformation,[],[f4961]) ).
fof(f5858,plain,
( sK27 = u1_struct_0(sK26)
| ~ r2_hidden(sK28,sK27)
| ~ r2_filter_2(sK26,sK27) ),
inference(cnf_transformation,[],[f4961]) ).
fof(f5871,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,X0)
| r2_hidden(X1,X0)
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f4965]) ).
fof(f5879,plain,
! [X0,X1] :
( ~ v10_lattices(X0)
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f3266]) ).
fof(f5936,plain,
! [X0] :
( ~ v10_lattices(X0)
| v3_struct_0(X0)
| u1_struct_0(X0) = k1_filter_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f3313]) ).
fof(f6011,plain,
! [X0] :
( ~ l3_lattices(X0)
| l3_lattices(k1_lattice2(X0)) ),
inference(cnf_transformation,[],[f3378]) ).
fof(f6014,plain,
! [X0] :
( ~ v10_lattices(X0)
| v3_struct_0(X0)
| v10_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f3382]) ).
fof(f6024,plain,
! [X0] :
( ~ v3_struct_0(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f3384]) ).
fof(f6263,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| m1_subset_1(X0,X1) ),
inference(cnf_transformation,[],[f3543]) ).
fof(f6275,plain,
! [X0] :
( ~ l3_lattices(X0)
| v3_struct_0(X0)
| u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0)) ),
inference(cnf_transformation,[],[f3551]) ).
fof(f6543,plain,
! [X3,X0,X1] :
( r2_hidden(k7_lattices(X0,X3),X1)
| r2_hidden(X3,X1)
| ~ m1_subset_1(X3,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(cnf_transformation,[],[f5182]) ).
fof(f6545,plain,
! [X0,X1] :
( ~ v17_lattices(X0)
| u1_struct_0(X0) = X1
| m1_subset_1(sK161(X0,X1),u1_struct_0(X0))
| ~ m1_filter_0(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| v1_filter_0(X1,X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f5182]) ).
fof(f6546,plain,
! [X0,X1] :
( ~ v10_lattices(X0)
| u1_struct_0(X0) = X1
| ~ r2_hidden(k7_lattices(X0,sK161(X0,X1)),X1)
| ~ m1_filter_0(X1,X0)
| v3_struct_0(X0)
| v1_filter_0(X1,X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f5182]) ).
fof(f6547,plain,
! [X0,X1] :
( ~ r2_hidden(sK161(X0,X1),X1)
| u1_struct_0(X0) = X1
| v1_filter_0(X1,X0)
| ~ m1_filter_0(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f5182]) ).
fof(f8839,plain,
! [X0] :
( ~ r2_filter_2(X0,u1_struct_0(X0))
| ~ m2_filter_2(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(equality_resolution,[],[f5746]) ).
fof(f9306,definition,
( spl415_5
<=> r2_filter_2(sK26,sK27) ),
introduced(definition,[new_symbols(definition,[spl415_5])],[avatar_definition]) ).
fof(f9307,plain,
( r2_filter_2(sK26,sK27)
| ~ spl415_5 ),
inference(avatar_component_clause,[],[f9306]) ).
fof(f9309,definition,
( spl415_6
<=> ! [X3] :
( r2_hidden(X3,sK27)
| ~ m1_subset_1(X3,u1_struct_0(sK26))
| r2_hidden(k7_lattices(sK26,X3),sK27) ) ),
introduced(definition,[new_symbols(definition,[spl415_6])],[avatar_definition]) ).
fof(f9310,plain,
( ! [X3] :
( r2_hidden(k7_lattices(sK26,X3),sK27)
| ~ m1_subset_1(X3,u1_struct_0(sK26))
| r2_hidden(X3,sK27) )
| ~ spl415_6 ),
inference(avatar_component_clause,[],[f9309]) ).
fof(f9311,plain,
( spl415_5
| spl415_6 ),
inference(avatar_split_clause,[],[f5854,f9309,f9306]) ).
fof(f9313,definition,
( spl415_7
<=> sK27 = u1_struct_0(sK26) ),
introduced(definition,[new_symbols(definition,[spl415_7])],[avatar_definition]) ).
fof(f9314,plain,
( sK27 != u1_struct_0(sK26)
| spl415_7 ),
inference(avatar_component_clause,[],[f9313]) ).
fof(f9315,plain,
( spl415_5
| ~ spl415_7 ),
inference(avatar_split_clause,[],[f5855,f9313,f9306]) ).
fof(f9316,plain,
( ~ r2_filter_2(sK26,sK27)
| spl415_5 ),
inference(avatar_component_clause,[],[f9306]) ).
fof(f9318,definition,
( spl415_8
<=> m1_subset_1(sK28,u1_struct_0(sK26)) ),
introduced(definition,[new_symbols(definition,[spl415_8])],[avatar_definition]) ).
fof(f9319,plain,
( m1_subset_1(sK28,u1_struct_0(sK26))
| ~ spl415_8 ),
inference(avatar_component_clause,[],[f9318]) ).
fof(f9320,plain,
( sK27 = u1_struct_0(sK26)
| ~ spl415_7 ),
inference(avatar_component_clause,[],[f9313]) ).
fof(f9321,plain,
( ~ spl415_5
| spl415_8
| spl415_7 ),
inference(avatar_split_clause,[],[f5856,f9313,f9318,f9306]) ).
fof(f9323,definition,
( spl415_9
<=> r2_hidden(k7_lattices(sK26,sK28),sK27) ),
introduced(definition,[new_symbols(definition,[spl415_9])],[avatar_definition]) ).
fof(f9324,plain,
( ~ r2_hidden(k7_lattices(sK26,sK28),sK27)
| spl415_9 ),
inference(avatar_component_clause,[],[f9323]) ).
fof(f9325,plain,
( ~ spl415_5
| ~ spl415_9
| spl415_7 ),
inference(avatar_split_clause,[],[f5857,f9313,f9323,f9306]) ).
fof(f9327,definition,
( spl415_10
<=> r2_hidden(sK28,sK27) ),
introduced(definition,[new_symbols(definition,[spl415_10])],[avatar_definition]) ).
fof(f9328,plain,
( ~ r2_hidden(sK28,sK27)
| spl415_10 ),
inference(avatar_component_clause,[],[f9327]) ).
fof(f9329,plain,
( ~ spl415_5
| ~ spl415_10
| spl415_7 ),
inference(avatar_split_clause,[],[f5858,f9313,f9327,f9306]) ).
fof(f9447,plain,
( v3_struct_0(sK26)
| u1_struct_0(sK26) = k17_filter_2(sK26)
| ~ l3_lattices(sK26) ),
inference(resolution,[],[f5735,f5851]) ).
fof(f9448,plain,
( u1_struct_0(sK26) = k17_filter_2(sK26)
| ~ l3_lattices(sK26) ),
inference(forward_subsumption_resolution,[],[f9447,f5852]) ).
fof(f9449,plain,
u1_struct_0(sK26) = k17_filter_2(sK26),
inference(forward_subsumption_resolution,[],[f9448,f5849]) ).
fof(f9463,plain,
( v3_struct_0(sK26)
| u1_struct_0(sK26) = k1_filter_0(sK26)
| ~ l3_lattices(sK26) ),
inference(resolution,[],[f5936,f5851]) ).
fof(f9464,plain,
( u1_struct_0(sK26) = k1_filter_0(sK26)
| ~ l3_lattices(sK26) ),
inference(forward_subsumption_resolution,[],[f9463,f5852]) ).
fof(f9465,plain,
u1_struct_0(sK26) = k1_filter_0(sK26),
inference(forward_subsumption_resolution,[],[f9464,f5849]) ).
fof(f9467,plain,
k17_filter_2(sK26) = k1_filter_0(sK26),
inference(superposition,[],[f9449,f9465]) ).
fof(f9469,plain,
( sK27 != k1_filter_0(sK26)
| spl415_7 ),
inference(superposition,[],[f9314,f9465]) ).
fof(f9489,plain,
( v3_struct_0(sK26)
| u1_struct_0(sK26) = u1_struct_0(k1_lattice2(sK26)) ),
inference(resolution,[],[f6275,f5849]) ).
fof(f9490,plain,
u1_struct_0(sK26) = u1_struct_0(k1_lattice2(sK26)),
inference(forward_subsumption_resolution,[],[f9489,f5852]) ).
fof(f9491,plain,
k17_filter_2(sK26) = u1_struct_0(k1_lattice2(sK26)),
inference(forward_demodulation,[],[f9490,f9449]) ).
fof(f9492,plain,
k1_filter_0(sK26) = u1_struct_0(k1_lattice2(sK26)),
inference(forward_demodulation,[],[f9491,f9467]) ).
fof(f9493,plain,
! [X0] :
( v3_struct_0(sK26)
| k7_filter_2(sK26,X0) = k15_filter_2(sK26,X0)
| ~ l3_lattices(sK26)
| ~ m2_filter_2(X0,sK26) ),
inference(resolution,[],[f5631,f5851]) ).
fof(f9494,plain,
! [X0] :
( k7_filter_2(sK26,X0) = k15_filter_2(sK26,X0)
| ~ l3_lattices(sK26)
| ~ m2_filter_2(X0,sK26) ),
inference(forward_subsumption_resolution,[],[f9493,f5852]) ).
fof(f9495,plain,
! [X0] :
( ~ m2_filter_2(X0,sK26)
| k7_filter_2(sK26,X0) = k15_filter_2(sK26,X0) ),
inference(forward_subsumption_resolution,[],[f9494,f5849]) ).
fof(f9496,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK26))
| v3_struct_0(sK26)
| ~ v10_lattices(sK26)
| k7_lattices(sK26,X0) = k7_lattices(k1_lattice2(sK26),k5_filter_2(sK26,X0))
| ~ l3_lattices(sK26) ),
inference(resolution,[],[f5845,f5850]) ).
fof(f9497,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK26))
| ~ v10_lattices(sK26)
| k7_lattices(sK26,X0) = k7_lattices(k1_lattice2(sK26),k5_filter_2(sK26,X0))
| ~ l3_lattices(sK26) ),
inference(forward_subsumption_resolution,[],[f9496,f5852]) ).
fof(f9498,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK26))
| k7_lattices(sK26,X0) = k7_lattices(k1_lattice2(sK26),k5_filter_2(sK26,X0))
| ~ l3_lattices(sK26) ),
inference(forward_subsumption_resolution,[],[f9497,f5851]) ).
fof(f9499,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK26))
| k7_lattices(sK26,X0) = k7_lattices(k1_lattice2(sK26),k5_filter_2(sK26,X0)) ),
inference(forward_subsumption_resolution,[],[f9498,f5849]) ).
fof(f9500,plain,
! [X0] :
( ~ m1_subset_1(X0,k17_filter_2(sK26))
| k7_lattices(sK26,X0) = k7_lattices(k1_lattice2(sK26),k5_filter_2(sK26,X0)) ),
inference(forward_demodulation,[],[f9499,f9449]) ).
fof(f9501,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_filter_0(sK26))
| k7_lattices(sK26,X0) = k7_lattices(k1_lattice2(sK26),k5_filter_2(sK26,X0)) ),
inference(forward_demodulation,[],[f9500,f9467]) ).
fof(f9502,plain,
k7_filter_2(sK26,sK27) = k15_filter_2(sK26,sK27),
inference(resolution,[],[f9495,f5853]) ).
fof(f9542,definition,
( spl415_17
<=> v3_struct_0(k1_lattice2(sK26)) ),
introduced(definition,[new_symbols(definition,[spl415_17])],[avatar_definition]) ).
fof(f9543,plain,
( v3_struct_0(k1_lattice2(sK26))
| ~ spl415_17 ),
inference(avatar_component_clause,[],[f9542]) ).
fof(f9558,plain,
( ~ v1_filter_0(k7_filter_2(sK26,sK27),k1_lattice2(sK26))
| r2_filter_2(sK26,sK27)
| ~ m2_filter_2(sK27,sK26)
| v3_struct_0(sK26)
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26) ),
inference(superposition,[],[f5752,f9502]) ).
fof(f9564,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK26))
| v3_struct_0(sK26)
| k5_filter_2(sK26,X0) = X0
| ~ l3_lattices(sK26) ),
inference(resolution,[],[f5696,f5851]) ).
fof(f9565,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK26))
| k5_filter_2(sK26,X0) = X0
| ~ l3_lattices(sK26) ),
inference(forward_subsumption_resolution,[],[f9564,f5852]) ).
fof(f9566,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK26))
| k5_filter_2(sK26,X0) = X0 ),
inference(forward_subsumption_resolution,[],[f9565,f5849]) ).
fof(f9567,plain,
! [X0] :
( ~ m1_subset_1(X0,k17_filter_2(sK26))
| k5_filter_2(sK26,X0) = X0 ),
inference(forward_demodulation,[],[f9566,f9449]) ).
fof(f9568,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_filter_0(sK26))
| k5_filter_2(sK26,X0) = X0 ),
inference(forward_demodulation,[],[f9567,f9467]) ).
fof(f9570,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK26)))
| v3_struct_0(sK26)
| k7_filter_2(sK26,X0) = X0
| ~ l3_lattices(sK26) ),
inference(resolution,[],[f5710,f5851]) ).
fof(f9571,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK26)))
| k7_filter_2(sK26,X0) = X0
| ~ l3_lattices(sK26) ),
inference(forward_subsumption_resolution,[],[f9570,f5852]) ).
fof(f9572,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK26)))
| k7_filter_2(sK26,X0) = X0 ),
inference(forward_subsumption_resolution,[],[f9571,f5849]) ).
fof(f9573,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k17_filter_2(sK26)))
| k7_filter_2(sK26,X0) = X0 ),
inference(forward_demodulation,[],[f9572,f9449]) ).
fof(f9574,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k1_filter_0(sK26)))
| k7_filter_2(sK26,X0) = X0 ),
inference(forward_demodulation,[],[f9573,f9467]) ).
fof(f9579,plain,
! [X0] :
( ~ m2_filter_2(X0,sK26)
| v3_struct_0(sK26)
| m2_lattice4(X0,sK26)
| ~ l3_lattices(sK26) ),
inference(resolution,[],[f5597,f5851]) ).
fof(f9580,plain,
! [X0] :
( ~ m2_filter_2(X0,sK26)
| m2_lattice4(X0,sK26)
| ~ l3_lattices(sK26) ),
inference(forward_subsumption_resolution,[],[f9579,f5852]) ).
fof(f9581,plain,
! [X0] :
( ~ m2_filter_2(X0,sK26)
| m2_lattice4(X0,sK26) ),
inference(forward_subsumption_resolution,[],[f9580,f5849]) ).
fof(f9582,plain,
m2_lattice4(sK27,sK26),
inference(resolution,[],[f9581,f5853]) ).
fof(f9590,plain,
( v3_struct_0(sK26)
| ~ v10_lattices(sK26)
| v17_lattices(k1_lattice2(sK26))
| ~ l3_lattices(sK26) ),
inference(resolution,[],[f5829,f5850]) ).
fof(f9591,plain,
( ~ v10_lattices(sK26)
| v17_lattices(k1_lattice2(sK26))
| ~ l3_lattices(sK26) ),
inference(forward_subsumption_resolution,[],[f9590,f5852]) ).
fof(f9592,plain,
( v17_lattices(k1_lattice2(sK26))
| ~ l3_lattices(sK26) ),
inference(forward_subsumption_resolution,[],[f9591,f5851]) ).
fof(f9593,plain,
v17_lattices(k1_lattice2(sK26)),
inference(forward_subsumption_resolution,[],[f9592,f5849]) ).
fof(f9609,plain,
! [X0] :
( ~ m2_lattice4(X0,sK26)
| v3_struct_0(sK26)
| m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK26)))
| ~ l3_lattices(sK26) ),
inference(resolution,[],[f5879,f5851]) ).
fof(f9610,plain,
! [X0] :
( ~ m2_lattice4(X0,sK26)
| m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK26)))
| ~ l3_lattices(sK26) ),
inference(forward_subsumption_resolution,[],[f9609,f5852]) ).
fof(f9611,plain,
! [X0] :
( ~ m2_lattice4(X0,sK26)
| m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK26))) ),
inference(forward_subsumption_resolution,[],[f9610,f5849]) ).
fof(f9612,plain,
! [X0] :
( m1_subset_1(X0,k1_zfmisc_1(k17_filter_2(sK26)))
| ~ m2_lattice4(X0,sK26) ),
inference(forward_demodulation,[],[f9611,f9449]) ).
fof(f9613,plain,
! [X0] :
( ~ m2_lattice4(X0,sK26)
| m1_subset_1(X0,k1_zfmisc_1(k1_filter_0(sK26))) ),
inference(forward_demodulation,[],[f9612,f9467]) ).
fof(f9614,plain,
m1_subset_1(sK27,k1_zfmisc_1(k1_filter_0(sK26))),
inference(resolution,[],[f9613,f9582]) ).
fof(f9615,plain,
sK27 = k7_filter_2(sK26,sK27),
inference(resolution,[],[f9614,f9574]) ).
fof(f9656,plain,
l3_lattices(k1_lattice2(sK26)),
inference(resolution,[],[f6011,f5849]) ).
fof(f9683,plain,
( v3_struct_0(sK26)
| v10_lattices(k1_lattice2(sK26))
| ~ l3_lattices(sK26) ),
inference(resolution,[],[f6014,f5851]) ).
fof(f9685,plain,
( v10_lattices(k1_lattice2(sK26))
| ~ l3_lattices(sK26) ),
inference(forward_subsumption_resolution,[],[f9683,f5852]) ).
fof(f9689,plain,
v10_lattices(k1_lattice2(sK26)),
inference(forward_subsumption_resolution,[],[f9685,f5849]) ).
fof(f9705,plain,
! [X0] :
( u1_struct_0(k1_lattice2(sK26)) = X0
| ~ r2_hidden(k7_lattices(k1_lattice2(sK26),sK161(k1_lattice2(sK26),X0)),X0)
| ~ m1_filter_0(X0,k1_lattice2(sK26))
| v3_struct_0(k1_lattice2(sK26))
| v1_filter_0(X0,k1_lattice2(sK26))
| ~ v17_lattices(k1_lattice2(sK26))
| ~ l3_lattices(k1_lattice2(sK26)) ),
inference(resolution,[],[f9689,f6546]) ).
fof(f9728,plain,
( m1_filter_2(k7_filter_2(sK26,sK27),k1_lattice2(sK26))
| v3_struct_0(sK26)
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| ~ m2_filter_2(sK27,sK26) ),
inference(superposition,[],[f5630,f9502]) ).
fof(f9729,plain,
( m1_filter_2(k7_filter_2(sK26,sK27),k1_lattice2(sK26))
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| ~ m2_filter_2(sK27,sK26) ),
inference(forward_subsumption_resolution,[],[f9728,f5852]) ).
fof(f9731,plain,
( m1_filter_2(k7_filter_2(sK26,sK27),k1_lattice2(sK26))
| ~ l3_lattices(sK26)
| ~ m2_filter_2(sK27,sK26) ),
inference(forward_subsumption_resolution,[],[f9729,f5851]) ).
fof(f9733,plain,
( m1_filter_2(k7_filter_2(sK26,sK27),k1_lattice2(sK26))
| ~ m2_filter_2(sK27,sK26) ),
inference(forward_subsumption_resolution,[],[f9731,f5849]) ).
fof(f9735,plain,
m1_filter_2(k7_filter_2(sK26,sK27),k1_lattice2(sK26)),
inference(forward_subsumption_resolution,[],[f9733,f5853]) ).
fof(f9736,plain,
m1_filter_2(sK27,k1_lattice2(sK26)),
inference(forward_demodulation,[],[f9735,f9615]) ).
fof(f9737,plain,
( m1_filter_0(sK27,k1_lattice2(sK26))
| v3_struct_0(k1_lattice2(sK26))
| ~ v10_lattices(k1_lattice2(sK26))
| ~ l3_lattices(k1_lattice2(sK26)) ),
inference(resolution,[],[f9736,f5595]) ).
fof(f9745,plain,
( v3_struct_0(sK26)
| ~ l3_lattices(sK26)
| ~ spl415_17 ),
inference(resolution,[],[f6024,f9543]) ).
fof(f9747,plain,
( ~ l3_lattices(sK26)
| ~ spl415_17 ),
inference(forward_subsumption_resolution,[],[f9745,f5852]) ).
fof(f9748,plain,
( $false
| ~ spl415_17 ),
inference(forward_subsumption_resolution,[],[f9747,f5849]) ).
fof(f9749,plain,
~ spl415_17,
inference(avatar_contradiction_clause,[],[f9748]) ).
fof(f9756,plain,
! [X0] :
( u1_struct_0(k1_lattice2(sK26)) = X0
| ~ r2_hidden(k7_lattices(k1_lattice2(sK26),sK161(k1_lattice2(sK26),X0)),X0)
| ~ m1_filter_0(X0,k1_lattice2(sK26))
| v3_struct_0(k1_lattice2(sK26))
| v1_filter_0(X0,k1_lattice2(sK26))
| ~ l3_lattices(k1_lattice2(sK26)) ),
inference(forward_subsumption_resolution,[],[f9705,f9593]) ).
fof(f9773,plain,
( m1_filter_0(sK27,k1_lattice2(sK26))
| v3_struct_0(k1_lattice2(sK26))
| ~ l3_lattices(k1_lattice2(sK26)) ),
inference(forward_subsumption_resolution,[],[f9737,f9689]) ).
fof(f9780,plain,
! [X0] :
( u1_struct_0(k1_lattice2(sK26)) = X0
| ~ r2_hidden(k7_lattices(k1_lattice2(sK26),sK161(k1_lattice2(sK26),X0)),X0)
| ~ m1_filter_0(X0,k1_lattice2(sK26))
| v3_struct_0(k1_lattice2(sK26))
| v1_filter_0(X0,k1_lattice2(sK26)) ),
inference(forward_subsumption_resolution,[],[f9756,f9656]) ).
fof(f9815,plain,
( m1_filter_0(sK27,k1_lattice2(sK26))
| v3_struct_0(k1_lattice2(sK26)) ),
inference(forward_subsumption_resolution,[],[f9773,f9656]) ).
fof(f9827,plain,
! [X0] :
( k1_filter_0(sK26) = X0
| ~ r2_hidden(k7_lattices(k1_lattice2(sK26),sK161(k1_lattice2(sK26),X0)),X0)
| ~ m1_filter_0(X0,k1_lattice2(sK26))
| v3_struct_0(k1_lattice2(sK26))
| v1_filter_0(X0,k1_lattice2(sK26)) ),
inference(forward_demodulation,[],[f9780,f9492]) ).
fof(f9850,definition,
( spl415_35
<=> m1_filter_0(sK27,k1_lattice2(sK26)) ),
introduced(definition,[new_symbols(definition,[spl415_35])],[avatar_definition]) ).
fof(f9851,plain,
( m1_filter_0(sK27,k1_lattice2(sK26))
| ~ spl415_35 ),
inference(avatar_component_clause,[],[f9850]) ).
fof(f9852,plain,
( spl415_17
| spl415_35 ),
inference(avatar_split_clause,[],[f9815,f9850,f9542]) ).
fof(f9855,definition,
( spl415_36
<=> ! [X0] :
( k1_filter_0(sK26) = X0
| v1_filter_0(X0,k1_lattice2(sK26))
| ~ m1_filter_0(X0,k1_lattice2(sK26))
| ~ r2_hidden(k7_lattices(k1_lattice2(sK26),sK161(k1_lattice2(sK26),X0)),X0) ) ),
introduced(definition,[new_symbols(definition,[spl415_36])],[avatar_definition]) ).
fof(f9856,plain,
( ! [X0] :
( ~ r2_hidden(k7_lattices(k1_lattice2(sK26),sK161(k1_lattice2(sK26),X0)),X0)
| v1_filter_0(X0,k1_lattice2(sK26))
| ~ m1_filter_0(X0,k1_lattice2(sK26))
| k1_filter_0(sK26) = X0 )
| ~ spl415_36 ),
inference(avatar_component_clause,[],[f9855]) ).
fof(f9857,plain,
( spl415_17
| spl415_36 ),
inference(avatar_split_clause,[],[f9827,f9855,f9542]) ).
fof(f9875,plain,
! [X2,X0,X1] :
( ~ v1_filter_0(X2,X0)
| r2_hidden(X1,X2)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| m1_subset_1(k7_lattices(X0,X1),X2)
| ~ m1_filter_0(X2,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(resolution,[],[f6263,f6543]) ).
fof(f9904,definition,
( spl415_42
<=> v1_xboole_0(sK27) ),
introduced(definition,[new_symbols(definition,[spl415_42])],[avatar_definition]) ).
fof(f9905,plain,
( v1_xboole_0(sK27)
| ~ spl415_42 ),
inference(avatar_component_clause,[],[f9904]) ).
fof(f9911,plain,
( $false
| ~ spl415_42 ),
inference(unit_resulting_resolution,[],[f5598,f5849,f5851,f5852,f5853,f9905]) ).
fof(f9913,plain,
~ spl415_42,
inference(avatar_contradiction_clause,[],[f9911]) ).
fof(f10913,plain,
( ~ r2_filter_2(sK26,sK27)
| ~ m2_filter_2(sK27,sK26)
| v3_struct_0(sK26)
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| ~ spl415_7 ),
inference(superposition,[],[f8839,f9320]) ).
fof(f10914,plain,
( ~ m2_filter_2(sK27,sK26)
| v3_struct_0(sK26)
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| ~ spl415_5
| ~ spl415_7 ),
inference(forward_subsumption_resolution,[],[f10913,f9307]) ).
fof(f10916,plain,
( v3_struct_0(sK26)
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| ~ spl415_5
| ~ spl415_7 ),
inference(forward_subsumption_resolution,[],[f10914,f5853]) ).
fof(f10918,plain,
( ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| ~ spl415_5
| ~ spl415_7 ),
inference(forward_subsumption_resolution,[],[f10916,f5852]) ).
fof(f10920,plain,
( ~ l3_lattices(sK26)
| ~ spl415_5
| ~ spl415_7 ),
inference(forward_subsumption_resolution,[],[f10918,f5851]) ).
fof(f10923,plain,
( $false
| ~ spl415_5
| ~ spl415_7 ),
inference(forward_subsumption_resolution,[],[f10920,f5849]) ).
fof(f10924,plain,
( ~ spl415_5
| ~ spl415_7 ),
inference(avatar_contradiction_clause,[],[f10923]) ).
fof(f10927,plain,
( m1_subset_1(sK28,k17_filter_2(sK26))
| ~ spl415_8 ),
inference(forward_demodulation,[],[f9319,f9449]) ).
fof(f10929,plain,
( m1_subset_1(sK28,k1_filter_0(sK26))
| ~ spl415_8 ),
inference(forward_demodulation,[],[f10927,f9467]) ).
fof(f10932,plain,
( k7_lattices(sK26,sK28) = k7_lattices(k1_lattice2(sK26),k5_filter_2(sK26,sK28))
| ~ spl415_8 ),
inference(resolution,[],[f10929,f9501]) ).
fof(f10934,plain,
( sK28 = k5_filter_2(sK26,sK28)
| ~ spl415_8 ),
inference(resolution,[],[f10929,f9568]) ).
fof(f10961,plain,
( k7_lattices(sK26,sK28) = k7_lattices(k1_lattice2(sK26),sK28)
| ~ spl415_8 ),
inference(forward_demodulation,[],[f10932,f10934]) ).
fof(f10963,plain,
( v1_filter_0(k15_filter_2(sK26,sK27),k1_lattice2(sK26))
| ~ m2_filter_2(sK27,sK26)
| v3_struct_0(sK26)
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| ~ spl415_5 ),
inference(resolution,[],[f9307,f5751]) ).
fof(f10964,plain,
( v1_filter_0(k15_filter_2(sK26,sK27),k1_lattice2(sK26))
| v3_struct_0(sK26)
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| ~ spl415_5 ),
inference(forward_subsumption_resolution,[],[f10963,f5853]) ).
fof(f10966,plain,
( v1_filter_0(k15_filter_2(sK26,sK27),k1_lattice2(sK26))
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| ~ spl415_5 ),
inference(forward_subsumption_resolution,[],[f10964,f5852]) ).
fof(f10968,plain,
( v1_filter_0(k15_filter_2(sK26,sK27),k1_lattice2(sK26))
| ~ l3_lattices(sK26)
| ~ spl415_5 ),
inference(forward_subsumption_resolution,[],[f10966,f5851]) ).
fof(f10970,plain,
( v1_filter_0(k15_filter_2(sK26,sK27),k1_lattice2(sK26))
| ~ spl415_5 ),
inference(forward_subsumption_resolution,[],[f10968,f5849]) ).
fof(f10972,plain,
( v1_filter_0(k7_filter_2(sK26,sK27),k1_lattice2(sK26))
| ~ spl415_5 ),
inference(forward_demodulation,[],[f10970,f9502]) ).
fof(f10974,plain,
( v1_filter_0(sK27,k1_lattice2(sK26))
| ~ spl415_5 ),
inference(forward_demodulation,[],[f10972,f9615]) ).
fof(f10985,plain,
( ! [X0] :
( r2_hidden(X0,sK27)
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK26)))
| m1_subset_1(k7_lattices(k1_lattice2(sK26),X0),sK27)
| ~ m1_filter_0(sK27,k1_lattice2(sK26))
| v3_struct_0(k1_lattice2(sK26))
| ~ v10_lattices(k1_lattice2(sK26))
| ~ v17_lattices(k1_lattice2(sK26))
| ~ l3_lattices(k1_lattice2(sK26)) )
| ~ spl415_5 ),
inference(resolution,[],[f10974,f9875]) ).
fof(f10990,plain,
( ! [X0] :
( r2_hidden(X0,sK27)
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK26)))
| m1_subset_1(k7_lattices(k1_lattice2(sK26),X0),sK27)
| v3_struct_0(k1_lattice2(sK26))
| ~ v10_lattices(k1_lattice2(sK26))
| ~ v17_lattices(k1_lattice2(sK26))
| ~ l3_lattices(k1_lattice2(sK26)) )
| ~ spl415_5
| ~ spl415_35 ),
inference(forward_subsumption_resolution,[],[f10985,f9851]) ).
fof(f10993,plain,
( ! [X0] :
( r2_hidden(X0,sK27)
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK26)))
| m1_subset_1(k7_lattices(k1_lattice2(sK26),X0),sK27)
| v3_struct_0(k1_lattice2(sK26))
| ~ v17_lattices(k1_lattice2(sK26))
| ~ l3_lattices(k1_lattice2(sK26)) )
| ~ spl415_5
| ~ spl415_35 ),
inference(forward_subsumption_resolution,[],[f10990,f9689]) ).
fof(f10996,plain,
( ! [X0] :
( r2_hidden(X0,sK27)
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK26)))
| m1_subset_1(k7_lattices(k1_lattice2(sK26),X0),sK27)
| v3_struct_0(k1_lattice2(sK26))
| ~ l3_lattices(k1_lattice2(sK26)) )
| ~ spl415_5
| ~ spl415_35 ),
inference(forward_subsumption_resolution,[],[f10993,f9593]) ).
fof(f10999,plain,
( ! [X0] :
( r2_hidden(X0,sK27)
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK26)))
| m1_subset_1(k7_lattices(k1_lattice2(sK26),X0),sK27)
| v3_struct_0(k1_lattice2(sK26)) )
| ~ spl415_5
| ~ spl415_35 ),
inference(forward_subsumption_resolution,[],[f10996,f9656]) ).
fof(f11002,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_filter_0(sK26))
| r2_hidden(X0,sK27)
| m1_subset_1(k7_lattices(k1_lattice2(sK26),X0),sK27)
| v3_struct_0(k1_lattice2(sK26)) )
| ~ spl415_5
| ~ spl415_35 ),
inference(forward_demodulation,[],[f10999,f9492]) ).
fof(f11006,definition,
( spl415_112
<=> ! [X0] :
( ~ m1_subset_1(X0,k1_filter_0(sK26))
| m1_subset_1(k7_lattices(k1_lattice2(sK26),X0),sK27)
| r2_hidden(X0,sK27) ) ),
introduced(definition,[new_symbols(definition,[spl415_112])],[avatar_definition]) ).
fof(f11007,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_filter_0(sK26))
| m1_subset_1(k7_lattices(k1_lattice2(sK26),X0),sK27)
| r2_hidden(X0,sK27) )
| ~ spl415_112 ),
inference(avatar_component_clause,[],[f11006]) ).
fof(f11008,plain,
( spl415_17
| spl415_112
| ~ spl415_5
| ~ spl415_35 ),
inference(avatar_split_clause,[],[f11002,f9850,f9306,f11006,f9542]) ).
fof(f11172,plain,
( m1_subset_1(k7_lattices(k1_lattice2(sK26),sK28),sK27)
| r2_hidden(sK28,sK27)
| ~ spl415_8
| ~ spl415_112 ),
inference(resolution,[],[f11007,f10929]) ).
fof(f11175,plain,
( m1_subset_1(k7_lattices(k1_lattice2(sK26),sK28),sK27)
| ~ spl415_8
| spl415_10
| ~ spl415_112 ),
inference(forward_subsumption_resolution,[],[f11172,f9328]) ).
fof(f11177,plain,
( m1_subset_1(k7_lattices(sK26,sK28),sK27)
| ~ spl415_8
| spl415_10
| ~ spl415_112 ),
inference(forward_demodulation,[],[f11175,f10961]) ).
fof(f11178,plain,
( r2_hidden(k7_lattices(sK26,sK28),sK27)
| v1_xboole_0(sK27)
| ~ spl415_8
| spl415_10
| ~ spl415_112 ),
inference(resolution,[],[f11177,f5871]) ).
fof(f11179,plain,
( v1_xboole_0(sK27)
| ~ spl415_8
| spl415_9
| spl415_10
| ~ spl415_112 ),
inference(forward_subsumption_resolution,[],[f11178,f9324]) ).
fof(f11180,plain,
( spl415_42
| ~ spl415_8
| spl415_9
| spl415_10
| ~ spl415_112 ),
inference(avatar_split_clause,[],[f11179,f11006,f9327,f9323,f9318,f9904]) ).
fof(f11182,plain,
( ! [X3] :
( ~ m1_subset_1(X3,k17_filter_2(sK26))
| r2_hidden(k7_lattices(sK26,X3),sK27)
| r2_hidden(X3,sK27) )
| ~ spl415_6 ),
inference(forward_demodulation,[],[f9310,f9449]) ).
fof(f11196,plain,
( ~ v1_filter_0(k7_filter_2(sK26,sK27),k1_lattice2(sK26))
| ~ m2_filter_2(sK27,sK26)
| v3_struct_0(sK26)
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| spl415_5 ),
inference(forward_subsumption_resolution,[],[f9558,f9316]) ).
fof(f11197,plain,
( ! [X3] :
( ~ m1_subset_1(X3,k1_filter_0(sK26))
| r2_hidden(k7_lattices(sK26,X3),sK27)
| r2_hidden(X3,sK27) )
| ~ spl415_6 ),
inference(forward_demodulation,[],[f11182,f9467]) ).
fof(f11202,plain,
( ~ v1_filter_0(k7_filter_2(sK26,sK27),k1_lattice2(sK26))
| v3_struct_0(sK26)
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| spl415_5 ),
inference(forward_subsumption_resolution,[],[f11196,f5853]) ).
fof(f11205,plain,
( ~ v1_filter_0(k7_filter_2(sK26,sK27),k1_lattice2(sK26))
| ~ v10_lattices(sK26)
| ~ l3_lattices(sK26)
| spl415_5 ),
inference(forward_subsumption_resolution,[],[f11202,f5852]) ).
fof(f11208,plain,
( ~ v1_filter_0(k7_filter_2(sK26,sK27),k1_lattice2(sK26))
| ~ l3_lattices(sK26)
| spl415_5 ),
inference(forward_subsumption_resolution,[],[f11205,f5851]) ).
fof(f11210,plain,
( ~ v1_filter_0(k7_filter_2(sK26,sK27),k1_lattice2(sK26))
| spl415_5 ),
inference(forward_subsumption_resolution,[],[f11208,f5849]) ).
fof(f11212,plain,
( ~ v1_filter_0(sK27,k1_lattice2(sK26))
| spl415_5 ),
inference(forward_demodulation,[],[f11210,f9615]) ).
fof(f15716,plain,
! [X0] :
( u1_struct_0(k1_lattice2(sK26)) = X0
| m1_subset_1(sK161(k1_lattice2(sK26),X0),u1_struct_0(k1_lattice2(sK26)))
| ~ m1_filter_0(X0,k1_lattice2(sK26))
| v3_struct_0(k1_lattice2(sK26))
| ~ v10_lattices(k1_lattice2(sK26))
| v1_filter_0(X0,k1_lattice2(sK26))
| ~ l3_lattices(k1_lattice2(sK26)) ),
inference(resolution,[],[f6545,f9593]) ).
fof(f15717,plain,
! [X0] :
( u1_struct_0(k1_lattice2(sK26)) = X0
| m1_subset_1(sK161(k1_lattice2(sK26),X0),u1_struct_0(k1_lattice2(sK26)))
| ~ m1_filter_0(X0,k1_lattice2(sK26))
| v3_struct_0(k1_lattice2(sK26))
| v1_filter_0(X0,k1_lattice2(sK26))
| ~ l3_lattices(k1_lattice2(sK26)) ),
inference(forward_subsumption_resolution,[],[f15716,f9689]) ).
fof(f15719,plain,
! [X0] :
( u1_struct_0(k1_lattice2(sK26)) = X0
| m1_subset_1(sK161(k1_lattice2(sK26),X0),u1_struct_0(k1_lattice2(sK26)))
| ~ m1_filter_0(X0,k1_lattice2(sK26))
| v3_struct_0(k1_lattice2(sK26))
| v1_filter_0(X0,k1_lattice2(sK26)) ),
inference(forward_subsumption_resolution,[],[f15717,f9656]) ).
fof(f15721,plain,
! [X0] :
( k1_filter_0(sK26) = X0
| m1_subset_1(sK161(k1_lattice2(sK26),X0),u1_struct_0(k1_lattice2(sK26)))
| ~ m1_filter_0(X0,k1_lattice2(sK26))
| v3_struct_0(k1_lattice2(sK26))
| v1_filter_0(X0,k1_lattice2(sK26)) ),
inference(forward_demodulation,[],[f15719,f9492]) ).
fof(f15723,plain,
! [X0] :
( m1_subset_1(sK161(k1_lattice2(sK26),X0),k1_filter_0(sK26))
| k1_filter_0(sK26) = X0
| ~ m1_filter_0(X0,k1_lattice2(sK26))
| v3_struct_0(k1_lattice2(sK26))
| v1_filter_0(X0,k1_lattice2(sK26)) ),
inference(forward_demodulation,[],[f15721,f9492]) ).
fof(f15726,definition,
( spl415_542
<=> ! [X0] :
( m1_subset_1(sK161(k1_lattice2(sK26),X0),k1_filter_0(sK26))
| v1_filter_0(X0,k1_lattice2(sK26))
| ~ m1_filter_0(X0,k1_lattice2(sK26))
| k1_filter_0(sK26) = X0 ) ),
introduced(definition,[new_symbols(definition,[spl415_542])],[avatar_definition]) ).
fof(f15727,plain,
( ! [X0] :
( ~ m1_filter_0(X0,k1_lattice2(sK26))
| v1_filter_0(X0,k1_lattice2(sK26))
| m1_subset_1(sK161(k1_lattice2(sK26),X0),k1_filter_0(sK26))
| k1_filter_0(sK26) = X0 )
| ~ spl415_542 ),
inference(avatar_component_clause,[],[f15726]) ).
fof(f15728,plain,
( spl415_17
| spl415_542 ),
inference(avatar_split_clause,[],[f15723,f15726,f9542]) ).
fof(f15799,plain,
( v1_filter_0(sK27,k1_lattice2(sK26))
| m1_subset_1(sK161(k1_lattice2(sK26),sK27),k1_filter_0(sK26))
| sK27 = k1_filter_0(sK26)
| ~ spl415_35
| ~ spl415_542 ),
inference(resolution,[],[f15727,f9851]) ).
fof(f15804,plain,
( m1_subset_1(sK161(k1_lattice2(sK26),sK27),k1_filter_0(sK26))
| sK27 = k1_filter_0(sK26)
| spl415_5
| ~ spl415_35
| ~ spl415_542 ),
inference(forward_subsumption_resolution,[],[f15799,f11212]) ).
fof(f15807,plain,
( m1_subset_1(sK161(k1_lattice2(sK26),sK27),k1_filter_0(sK26))
| spl415_5
| spl415_7
| ~ spl415_35
| ~ spl415_542 ),
inference(forward_subsumption_resolution,[],[f15804,f9469]) ).
fof(f15818,plain,
( k7_lattices(sK26,sK161(k1_lattice2(sK26),sK27)) = k7_lattices(k1_lattice2(sK26),k5_filter_2(sK26,sK161(k1_lattice2(sK26),sK27)))
| spl415_5
| spl415_7
| ~ spl415_35
| ~ spl415_542 ),
inference(resolution,[],[f15807,f9501]) ).
fof(f15820,plain,
( sK161(k1_lattice2(sK26),sK27) = k5_filter_2(sK26,sK161(k1_lattice2(sK26),sK27))
| spl415_5
| spl415_7
| ~ spl415_35
| ~ spl415_542 ),
inference(resolution,[],[f15807,f9568]) ).
fof(f15851,plain,
( r2_hidden(k7_lattices(sK26,sK161(k1_lattice2(sK26),sK27)),sK27)
| r2_hidden(sK161(k1_lattice2(sK26),sK27),sK27)
| spl415_5
| ~ spl415_6
| spl415_7
| ~ spl415_35
| ~ spl415_542 ),
inference(resolution,[],[f15807,f11197]) ).
fof(f15939,definition,
( spl415_563
<=> r2_hidden(sK161(k1_lattice2(sK26),sK27),sK27) ),
introduced(definition,[new_symbols(definition,[spl415_563])],[avatar_definition]) ).
fof(f15940,plain,
( r2_hidden(sK161(k1_lattice2(sK26),sK27),sK27)
| ~ spl415_563 ),
inference(avatar_component_clause,[],[f15939]) ).
fof(f15942,definition,
( spl415_564
<=> r2_hidden(k7_lattices(sK26,sK161(k1_lattice2(sK26),sK27)),sK27) ),
introduced(definition,[new_symbols(definition,[spl415_564])],[avatar_definition]) ).
fof(f15943,plain,
( r2_hidden(k7_lattices(sK26,sK161(k1_lattice2(sK26),sK27)),sK27)
| ~ spl415_564 ),
inference(avatar_component_clause,[],[f15942]) ).
fof(f15944,plain,
( spl415_563
| spl415_564
| spl415_5
| ~ spl415_6
| spl415_7
| ~ spl415_35
| ~ spl415_542 ),
inference(avatar_split_clause,[],[f15851,f15726,f9850,f9313,f9309,f9306,f15942,f15939]) ).
fof(f15980,plain,
( k7_lattices(k1_lattice2(sK26),sK161(k1_lattice2(sK26),sK27)) = k7_lattices(sK26,sK161(k1_lattice2(sK26),sK27))
| spl415_5
| spl415_7
| ~ spl415_35
| ~ spl415_542 ),
inference(forward_demodulation,[],[f15818,f15820]) ).
fof(f16021,plain,
( sK27 = u1_struct_0(k1_lattice2(sK26))
| v1_filter_0(sK27,k1_lattice2(sK26))
| ~ m1_filter_0(sK27,k1_lattice2(sK26))
| v3_struct_0(k1_lattice2(sK26))
| ~ v10_lattices(k1_lattice2(sK26))
| ~ v17_lattices(k1_lattice2(sK26))
| ~ l3_lattices(k1_lattice2(sK26))
| ~ spl415_563 ),
inference(resolution,[],[f15940,f6547]) ).
fof(f16024,plain,
( sK27 = u1_struct_0(k1_lattice2(sK26))
| ~ m1_filter_0(sK27,k1_lattice2(sK26))
| v3_struct_0(k1_lattice2(sK26))
| ~ v10_lattices(k1_lattice2(sK26))
| ~ v17_lattices(k1_lattice2(sK26))
| ~ l3_lattices(k1_lattice2(sK26))
| spl415_5
| ~ spl415_563 ),
inference(forward_subsumption_resolution,[],[f16021,f11212]) ).
fof(f16025,plain,
( sK27 = u1_struct_0(k1_lattice2(sK26))
| v3_struct_0(k1_lattice2(sK26))
| ~ v10_lattices(k1_lattice2(sK26))
| ~ v17_lattices(k1_lattice2(sK26))
| ~ l3_lattices(k1_lattice2(sK26))
| spl415_5
| ~ spl415_35
| ~ spl415_563 ),
inference(forward_subsumption_resolution,[],[f16024,f9851]) ).
fof(f16026,plain,
( sK27 = u1_struct_0(k1_lattice2(sK26))
| v3_struct_0(k1_lattice2(sK26))
| ~ v17_lattices(k1_lattice2(sK26))
| ~ l3_lattices(k1_lattice2(sK26))
| spl415_5
| ~ spl415_35
| ~ spl415_563 ),
inference(forward_subsumption_resolution,[],[f16025,f9689]) ).
fof(f16027,plain,
( sK27 = u1_struct_0(k1_lattice2(sK26))
| v3_struct_0(k1_lattice2(sK26))
| ~ l3_lattices(k1_lattice2(sK26))
| spl415_5
| ~ spl415_35
| ~ spl415_563 ),
inference(forward_subsumption_resolution,[],[f16026,f9593]) ).
fof(f16028,plain,
( sK27 = u1_struct_0(k1_lattice2(sK26))
| v3_struct_0(k1_lattice2(sK26))
| spl415_5
| ~ spl415_35
| ~ spl415_563 ),
inference(forward_subsumption_resolution,[],[f16027,f9656]) ).
fof(f16029,plain,
( sK27 = k1_filter_0(sK26)
| v3_struct_0(k1_lattice2(sK26))
| spl415_5
| ~ spl415_35
| ~ spl415_563 ),
inference(forward_demodulation,[],[f16028,f9492]) ).
fof(f16030,plain,
( v3_struct_0(k1_lattice2(sK26))
| spl415_5
| spl415_7
| ~ spl415_35
| ~ spl415_563 ),
inference(forward_subsumption_resolution,[],[f16029,f9469]) ).
fof(f16031,plain,
( spl415_17
| spl415_5
| spl415_7
| ~ spl415_35
| ~ spl415_563 ),
inference(avatar_split_clause,[],[f16030,f15939,f9850,f9313,f9306,f9542]) ).
fof(f16447,plain,
( ~ r2_hidden(k7_lattices(sK26,sK161(k1_lattice2(sK26),sK27)),sK27)
| v1_filter_0(sK27,k1_lattice2(sK26))
| ~ m1_filter_0(sK27,k1_lattice2(sK26))
| sK27 = k1_filter_0(sK26)
| spl415_5
| spl415_7
| ~ spl415_35
| ~ spl415_36
| ~ spl415_542 ),
inference(superposition,[],[f9856,f15980]) ).
fof(f16459,plain,
( v1_filter_0(sK27,k1_lattice2(sK26))
| ~ m1_filter_0(sK27,k1_lattice2(sK26))
| sK27 = k1_filter_0(sK26)
| spl415_5
| spl415_7
| ~ spl415_35
| ~ spl415_36
| ~ spl415_542
| ~ spl415_564 ),
inference(forward_subsumption_resolution,[],[f16447,f15943]) ).
fof(f16463,plain,
( ~ m1_filter_0(sK27,k1_lattice2(sK26))
| sK27 = k1_filter_0(sK26)
| spl415_5
| spl415_7
| ~ spl415_35
| ~ spl415_36
| ~ spl415_542
| ~ spl415_564 ),
inference(forward_subsumption_resolution,[],[f16459,f11212]) ).
fof(f16467,plain,
( sK27 = k1_filter_0(sK26)
| spl415_5
| spl415_7
| ~ spl415_35
| ~ spl415_36
| ~ spl415_542
| ~ spl415_564 ),
inference(forward_subsumption_resolution,[],[f16463,f9851]) ).
fof(f16471,plain,
( $false
| spl415_5
| spl415_7
| ~ spl415_35
| ~ spl415_36
| ~ spl415_542
| ~ spl415_564 ),
inference(forward_subsumption_resolution,[],[f16467,f9469]) ).
fof(f16472,plain,
( spl415_5
| spl415_7
| ~ spl415_35
| ~ spl415_36
| ~ spl415_542
| ~ spl415_564 ),
inference(avatar_contradiction_clause,[],[f16471]) ).
cnf(s3,plain,
( spl415_5
| spl415_6 ),
inference(sat_conversion,[],[f9311]) ).
cnf(s4,plain,
( spl415_5
| ~ spl415_7 ),
inference(sat_conversion,[],[f9315]) ).
cnf(s5,plain,
( ~ spl415_5
| spl415_7
| spl415_8 ),
inference(sat_conversion,[],[f9321]) ).
cnf(s6,plain,
( ~ spl415_5
| spl415_7
| ~ spl415_9 ),
inference(sat_conversion,[],[f9325]) ).
cnf(s7,plain,
( ~ spl415_5
| spl415_7
| ~ spl415_10 ),
inference(sat_conversion,[],[f9329]) ).
cnf(s20,plain,
~ spl415_17,
inference(sat_conversion,[],[f9749]) ).
cnf(s34,plain,
( spl415_17
| spl415_35 ),
inference(sat_conversion,[],[f9852]) ).
cnf(s35,plain,
( spl415_17
| spl415_36 ),
inference(sat_conversion,[],[f9857]) ).
cnf(s41,plain,
~ spl415_42,
inference(sat_conversion,[],[f9913]) ).
cnf(s117,plain,
( ~ spl415_5
| ~ spl415_7 ),
inference(sat_conversion,[],[f10924]) ).
cnf(s121,plain,
( ~ spl415_5
| spl415_17
| ~ spl415_35
| spl415_112 ),
inference(sat_conversion,[],[f11008]) ).
cnf(s130,plain,
( ~ spl415_8
| spl415_9
| spl415_10
| spl415_42
| ~ spl415_112 ),
inference(sat_conversion,[],[f11180]) ).
cnf(s486,plain,
( spl415_17
| spl415_542 ),
inference(sat_conversion,[],[f15728]) ).
cnf(s501,plain,
( spl415_5
| ~ spl415_6
| spl415_7
| ~ spl415_35
| ~ spl415_542
| spl415_563
| spl415_564 ),
inference(sat_conversion,[],[f15944]) ).
cnf(s513,plain,
( spl415_5
| spl415_7
| spl415_17
| ~ spl415_35
| ~ spl415_563 ),
inference(sat_conversion,[],[f16031]) ).
cnf(s558,plain,
( spl415_5
| spl415_7
| ~ spl415_35
| ~ spl415_36
| ~ spl415_542
| ~ spl415_564 ),
inference(sat_conversion,[],[f16472]) ).
cnf(s577,plain,
spl415_542,
inference(rat,[],[s486,s20]) ).
cnf(s628,plain,
spl415_36,
inference(rat,[],[s35,s20]) ).
cnf(s629,plain,
spl415_35,
inference(rat,[],[s34,s20]) ).
cnf(s680,plain,
spl415_5,
inference(rat,[],[s501,s513,s558,s3,s4,s629,s577,s20,s628]) ).
cnf(s683,plain,
spl415_112,
inference(rat,[],[s121,s629,s20,s680]) ).
cnf(s684,plain,
~ spl415_7,
inference(rat,[],[s117,s680]) ).
cnf(s687,plain,
~ spl415_10,
inference(rat,[],[s7,s680,s684]) ).
cnf(s688,plain,
~ spl415_9,
inference(rat,[],[s6,s680,s684]) ).
cnf(s689,plain,
spl415_8,
inference(rat,[],[s5,s680,s684]) ).
cnf(s696,plain,
$false,
inference(rat,[],[s130,s683,s41,s687,s688,s689]) ).
fof(f16490,plain,
$false,
inference(avatar_sat_refutation,[],[s696]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT321+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.17/0.42 % Computer : n003.cluster.edu
% 0.17/0.42 % Model : x86_64 x86_64
% 0.17/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.42 % Memory : 8046.5625MB
% 0.17/0.42 % OS : Linux 6.8.0-71-generic
% 0.17/0.42 % CPULimit : 300
% 0.17/0.42 % WCLimit : 300
% 0.17/0.42 % DateTime : Sun Sep 27 14:37:42 UTC 2026
% 0.17/0.42 % CPUTime :
% 0.17/0.42 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.17/0.47 Running first-order theorem proving
% 0.17/0.47 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
% 21.99/4.27 % (605409)Detected formulas, will run a generic FOF schedule.
% 21.99/4.27 % (605432)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2718368879:i=119:av=off:ss=axioms_2998 on theBenchmark for (2998ds/119Mi)
% 21.99/4.27 % (605430)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=198560861:i=141695:sd=1:nm=32:gsp=on:ss=included_2998 on theBenchmark for (2998ds/141695Mi)
% 21.99/4.27 % (605434)dis-21_1_sil=8000:lcm=predicate:random_seed=2244635940:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2998 on theBenchmark for (2998ds/129Mi)
% 21.99/4.27 % (605432)Instruction limit reached!
% 21.99/4.27 % (605432)------------------------------
% 21.99/4.27 % (605432)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.99/4.27 % (605432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.99/4.27 % (605432)CaDiCaL version: 2.1.3
% 21.99/4.27 % (605432)Termination reason: Instruction limit
% 21.99/4.27 % (605432)Termination phase: Saturation
% 21.99/4.27 % (605432)Time elapsed: 0.065 s
% 21.99/4.27 % (605432)Peak memory usage: 92 MB
% 21.99/4.27 % (605432)Instructions burned: 119 (million)
% 21.99/4.27 % (605433)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=18477949:s2a=on:i=139:gtg=position_2998 on theBenchmark for (2998ds/139Mi)
% 21.99/4.27 % (605428)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=1908418725:i=141193_2998 on theBenchmark for (2998ds/141193Mi)
% 21.99/4.27 % (605431)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2602889230:i=109:sd=1:ins=1:gsp=on:ss=axioms_2998 on theBenchmark for (2998ds/109Mi)
% 21.99/4.27 % (605429)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=520091084:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2998 on theBenchmark for (2998ds/134677Mi)
% 21.99/4.27 % (605434)Instruction limit reached!
% 21.99/4.27 % (605434)------------------------------
% 21.99/4.27 % (605434)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.99/4.27 % (605434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.99/4.27 % (605434)CaDiCaL version: 2.1.3
% 21.99/4.27 % (605434)Termination reason: Instruction limit
% 21.99/4.27 % (605434)Termination phase: Property scanning
% 21.99/4.27 % (605434)Time elapsed: 0.083 s
% 21.99/4.27 % (605434)Peak memory usage: 92 MB
% 21.99/4.27 % (605434)Instructions burned: 130 (million)
% 21.99/4.27 % (605431)Instruction limit reached!
% 21.99/4.27 % (605431)------------------------------
% 21.99/4.27 % (605431)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.99/4.27 % (605431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.99/4.27 % (605431)CaDiCaL version: 2.1.3
% 21.99/4.27 % (605431)Termination reason: Instruction limit
% 21.99/4.27 % (605431)Termination phase: Saturation
% 21.99/4.27 % (605431)Time elapsed: 0.106 s
% 21.99/4.27 % (605431)Peak memory usage: 92 MB
% 21.99/4.27 % (605431)Instructions burned: 110 (million)
% 21.99/4.27 % (605433)Instruction limit reached!
% 21.99/4.27 % (605433)------------------------------
% 21.99/4.27 % (605433)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.99/4.27 % (605433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.99/4.27 % (605433)CaDiCaL version: 2.1.3
% 21.99/4.27 % (605433)Termination reason: Instruction limit
% 21.99/4.27 % (605433)Termination phase: Clausification
% 21.99/4.27 % (605433)Time elapsed: 0.140 s
% 21.99/4.27 % (605433)Peak memory usage: 94 MB
% 21.99/4.27 % (605433)Instructions burned: 139 (million)
% 21.99/4.27 % (605442)lrs+10_1_sil=8000:sp=occurrence:random_seed=227660675:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi)
% 21.99/4.27 % (605443)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1118365618:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/157Mi)
% 21.99/4.27 % (605445)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=4015673983:s2a=on:i=248:s2at=1.23:gtg=position_2994 on theBenchmark for (2994ds/248Mi)
% 21.99/4.27 % (605443)Instruction limit reached!
% 21.99/4.27 % (605443)------------------------------
% 21.99/4.27 % (605443)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.99/4.27 % (605443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.22/5.28 % (605443)CaDiCaL version: 2.1.3
% 29.22/5.28 % (605443)Termination reason: Instruction limit
% 29.22/5.28 % (605443)Termination phase: Saturation
% 29.22/5.28 % (605443)Time elapsed: 0.083 s
% 29.22/5.28 % (605443)Peak memory usage: 93 MB
% 29.22/5.28 % (605443)Instructions burned: 159 (million)
% 29.22/5.28 % (605444)lrs+1011_1_sil=32000:sp=occurrence:random_seed=930664374:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 29.22/5.28 % (605445)Instruction limit reached!
% 29.22/5.28 % (605445)------------------------------
% 29.22/5.28 % (605445)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.22/5.28 % (605445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.22/5.28 % (605445)CaDiCaL version: 2.1.3
% 29.22/5.28 % (605445)Termination reason: Instruction limit
% 29.22/5.28 % (605445)Termination phase: Saturation
% 29.22/5.28 % (605445)Time elapsed: 0.155 s
% 29.22/5.28 % (605445)Peak memory usage: 98 MB
% 29.22/5.28 % (605445)Instructions burned: 248 (million)
% 29.22/5.28 % (605442)Instruction limit reached!
% 29.22/5.28 % (605442)------------------------------
% 29.22/5.28 % (605442)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.22/5.28 % (605442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.22/5.28 % (605442)CaDiCaL version: 2.1.3
% 29.22/5.28 % (605442)Termination reason: Instruction limit
% 29.22/5.28 % (605442)Termination phase: Saturation
% 29.22/5.28 % (605442)Time elapsed: 0.286 s
% 29.22/5.28 % (605442)Peak memory usage: 95 MB
% 29.22/5.28 % (605442)Instructions burned: 285 (million)
% 29.22/5.28 % (605449)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3696451925:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi)
% 29.22/5.28 % (605451)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1909177444:i=2350_2991 on theBenchmark for (2991ds/2350Mi)
% 29.22/5.28 % (605452)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=270073256:cts=off:i=113:fsr=off:ss=included:sgt=4_2991 on theBenchmark for (2991ds/113Mi)
% 29.22/5.28 % (605444)Instruction limit reached!
% 29.22/5.28 % (605444)------------------------------
% 29.22/5.28 % (605444)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.22/5.28 % (605444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.22/5.28 % (605444)CaDiCaL version: 2.1.3
% 29.22/5.28 % (605444)Termination reason: Instruction limit
% 29.22/5.28 % (605444)Termination phase: Saturation
% 29.22/5.28 % (605444)Time elapsed: 0.347 s
% 29.22/5.28 % (605444)Peak memory usage: 96 MB
% 29.22/5.28 % (605444)Instructions burned: 325 (million)
% 29.22/5.28 % (605452)Instruction limit reached!
% 29.22/5.28 % (605452)------------------------------
% 29.22/5.28 % (605452)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.22/5.28 % (605452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.22/5.28 % (605452)CaDiCaL version: 2.1.3
% 29.22/5.28 % (605452)Termination reason: Instruction limit
% 29.22/5.28 % (605452)Termination phase: Saturation
% 29.22/5.28 % (605452)Time elapsed: 0.059 s
% 29.22/5.28 % (605452)Peak memory usage: 93 MB
% 29.22/5.28 % (605452)Instructions burned: 113 (million)
% 29.22/5.28 % (605449)Instruction limit reached!
% 29.22/5.28 % (605449)------------------------------
% 29.22/5.28 % (605449)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.22/5.28 % (605449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.22/5.28 % (605449)CaDiCaL version: 2.1.3
% 29.22/5.28 % (605449)Termination reason: Instruction limit
% 29.22/5.28 % (605449)Termination phase: Saturation
% 29.22/5.28 % (605449)Time elapsed: 0.276 s
% 29.22/5.28 % (605449)Peak memory usage: 95 MB
% 29.22/5.28 % (605449)Instructions burned: 295 (million)
% 29.22/5.28 % (605456)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3995413331:i=127:av=off:fsr=off:sup=off_2989 on theBenchmark for (2989ds/127Mi)
% 29.22/5.28 % (605457)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2723457070:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2989 on theBenchmark for (2989ds/114Mi)
% 29.22/5.28 % (605457)Instruction limit reached!
% 29.22/5.28 % (605457)------------------------------
% 29.22/5.28 % (605457)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.22/5.28 % (605457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.22/5.28 % (605457)CaDiCaL version: 2.1.3
% 29.22/5.28 % (605457)Termination reason: Instruction limit
% 29.22/5.28 % (605457)Termination phase: Property scanning
% 29.22/5.28 % (605457)Time elapsed: 0.058 s
% 29.22/5.28 % (605457)Peak memory usage: 90 MB
% 29.22/5.28 % (605457)Instructions burned: 117 (million)
% 29.22/5.28 % (605459)lrs+10_1_sil=8000:sp=occurrence:random_seed=1365032575:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2988 on theBenchmark for (2988ds/907Mi)
% 29.22/5.28 % (605456)Instruction limit reached!
% 29.22/5.28 % (605456)------------------------------
% 29.22/5.28 % (605456)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.22/5.28 % (605456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.22/5.28 % (605456)CaDiCaL version: 2.1.3
% 29.22/5.28 % (605456)Termination reason: Instruction limit
% 29.22/5.28 % (605456)Termination phase: Property scanning
% 29.22/5.28 % (605456)Time elapsed: 0.130 s
% 29.22/5.28 % (605456)Peak memory usage: 94 MB
% 29.22/5.28 % (605456)Instructions burned: 128 (million)
% 29.22/5.28 % (605463)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2949624514:i=437:sd=1:aac=none:ss=included_2986 on theBenchmark for (2986ds/437Mi)
% 29.22/5.28 % (605465)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=224977086:i=5202:ss=axioms:sgt=16_2986 on theBenchmark for (2986ds/5202Mi)
% 29.22/5.28 % (605463)Instruction limit reached!
% 29.22/5.28 % (605463)------------------------------
% 29.22/5.28 % (605463)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.22/5.28 % (605463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.22/5.28 % (605463)CaDiCaL version: 2.1.3
% 29.22/5.28 % (605463)Termination reason: Instruction limit
% 29.22/5.28 % (605463)Termination phase: Saturation
% 29.22/5.28 % (605463)Time elapsed: 0.379 s
% 29.22/5.28 % (605463)Peak memory usage: 95 MB
% 29.22/5.28 % (605463)Instructions burned: 437 (million)
% 29.22/5.28 % (605468)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2284205070:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2980 on theBenchmark for (2980ds/134Mi)
% 29.22/5.28 % (605459)Instruction limit reached!
% 29.22/5.28 % (605459)------------------------------
% 29.22/5.28 % (605459)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.22/5.28 % (605459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.22/5.28 % (605459)CaDiCaL version: 2.1.3
% 29.22/5.28 % (605459)Termination reason: Instruction limit
% 29.22/5.28 % (605459)Termination phase: Saturation
% 29.22/5.28 % (605459)Time elapsed: 0.925 s
% 29.22/5.28 % (605459)Peak memory usage: 104 MB
% 29.22/5.28 % (605459)Instructions burned: 907 (million)
% 29.22/5.28 % (605468)Instruction limit reached!
% 29.22/5.28 % (605468)------------------------------
% 29.22/5.28 % (605468)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.22/5.28 % (605468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.22/5.28 % (605468)CaDiCaL version: 2.1.3
% 29.22/5.28 % (605468)Termination reason: Instruction limit
% 29.22/5.28 % (605468)Termination phase: Saturation
% 29.22/5.28 % (605468)Time elapsed: 0.133 s
% 29.22/5.28 % (605468)Peak memory usage: 94 MB
% 29.22/5.28 % (605468)Instructions burned: 135 (million)
% 29.22/5.28 % (605471)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2426284662:st=3:i=13193:sd=3:ss=axioms_2977 on theBenchmark for (2977ds/13193Mi)
% 29.22/5.28 % (605470)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1826842987:st=8:i=592:sd=3:ep=RST:ss=axioms_2977 on theBenchmark for (2977ds/592Mi)
% 29.22/5.28 % (605470)Instruction limit reached!
% 29.22/5.28 % (605470)------------------------------
% 29.22/5.28 % (605470)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.22/5.28 % (605470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.22/5.28 % (605470)CaDiCaL version: 2.1.3
% 29.22/5.28 % (605470)Termination reason: Instruction limit
% 29.22/5.28 % (605470)Termination phase: Saturation
% 29.22/5.28 % (605470)Time elapsed: 0.502 s
% 29.22/5.28 % (605470)Peak memory usage: 102 MB
% 29.22/5.28 % (605470)Instructions burned: 592 (million)
% 29.22/5.28 % (605474)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=944731950:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2969 on theBenchmark for (2969ds/125Mi)
% 29.22/5.28 % (605451)Instruction limit reached!
% 29.22/5.28 % (605451)------------------------------
% 29.22/5.28 % (605451)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.22/5.28 % (605451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.22/5.28 % (605451)CaDiCaL version: 2.1.3
% 29.22/5.28 % (605451)Termination reason: Instruction limit
% 29.22/5.28 % (605451)Termination phase: Saturation
% 29.22/5.28 % (605451)Time elapsed: 2.263 s
% 29.22/5.28 % (605451)Peak memory usage: 214 MB
% 29.22/5.28 % (605451)Instructions burned: 2350 (million)
% 29.22/5.28 % (605474)Instruction limit reached!
% 29.22/5.28 % (605474)------------------------------
% 29.22/5.28 % (605474)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.22/5.28 % (605474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.22/5.28 % (605474)CaDiCaL version: 2.1.3
% 29.22/5.28 % (605474)Termination reason: Instruction limit
% 29.22/5.28 % (605474)Termination phase: Saturation
% 29.22/5.28 % (605474)Time elapsed: 0.114 s
% 29.22/5.28 % (605474)Peak memory usage: 93 MB
% 29.22/5.28 % (605474)Instructions burned: 125 (million)
% 29.22/5.28 % (605476)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3624831966:i=134:gtgl=5:slsql=off:gtg=exists_sym_2966 on theBenchmark for (2966ds/134Mi)
% 29.22/5.28 % (605477)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=588784407:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2966 on theBenchmark for (2966ds/141Mi)
% 29.22/5.28 % (605476)Instruction limit reached!
% 29.22/5.28 % (605476)------------------------------
% 29.22/5.28 % (605476)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.22/5.28 % (605476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.22/5.28 % (605476)CaDiCaL version: 2.1.3
% 29.22/5.28 % (605476)Termination reason: Instruction limit
% 29.22/5.28 % (605476)Termination phase: Preprocessing 3
% 29.22/5.28 % (605476)Time elapsed: 0.131 s
% 29.22/5.28 % (605476)Peak memory usage: 92 MB
% 29.22/5.28 % (605476)Instructions burned: 134 (million)
% 29.22/5.28 % (605477)Instruction limit reached!
% 29.22/5.28 % (605477)------------------------------
% 29.22/5.28 % (605477)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.22/5.28 % (605477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.22/5.28 % (605477)CaDiCaL version: 2.1.3
% 29.22/5.28 % (605477)Termination reason: Instruction limit
% 29.22/5.28 % (605477)Termination phase: Saturation
% 29.22/5.28 % (605477)Time elapsed: 0.130 s
% 29.22/5.28 % (605477)Peak memory usage: 93 MB
% 29.22/5.28 % (605477)Instructions burned: 142 (million)
% 29.22/5.28 % (605429)First to succeed.
% 29.22/5.28 % (605429)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-605409"
% 29.22/5.28 % (605482)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1874535919:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2963 on theBenchmark for (2963ds/431Mi)
% 29.22/5.28 % (605483)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=181531789:i=6060:aac=none:ins=25_2962 on theBenchmark for (2962ds/6060Mi)
% 29.22/5.28 % (605429)Refutation found. Thanks to Tanya!
% 29.22/5.28 % SZS status Theorem for theBenchmark
% 29.22/5.28 % SZS output start Proof for theBenchmark
% See solution above
% 29.91/5.54 % (605429)------------------------------
% 29.91/5.54 % (605429)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.91/5.54 % (605429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.91/5.54 % (605429)CaDiCaL version: 2.1.3
% 29.91/5.54 % (605429)Termination reason: Refutation
% 29.91/5.54 % (605429)Time elapsed: 3.446 s
% 29.91/5.54 % (605429)Peak memory usage: 165 MB
% 29.91/5.54 % (605429)Instructions burned: 3216 (million)
% 29.91/5.54 % (605429)------------------------------
% 29.91/5.54 % (605429)------------------------------
% 29.91/5.54 % (605409)Success in time 4.285 s
% 29.91/5.54 % Vampire exiting
%------------------------------------------------------------------------------