%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT333+2 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n007.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:47:02 AM UTC 2026
% Result : Theorem 21.01s 4.04s
% Output : Refutation 22.32s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 51
% Syntax : Number of formulae : 400 ( 50 unt; 26 def)
% Number of atoms : 1668 ( 178 equ)
% Maximal formula atoms : 26 ( 4 avg)
% Number of connectives : 2059 ( 791 ~; 985 |; 201 &)
% ( 41 <=>; 41 =>; 0 <=; 0 <~>)
% Maximal formula depth : 21 ( 5 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 50 ( 48 usr; 27 prp; 0-3 aty)
% Number of functors : 17 ( 17 usr; 2 con; 0-3 aty)
% Number of variables : 290 ( 0 sgn 276 !; 14 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2512,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_filter_0(X1,X0)
=> ( v14_lattices(X0)
=> v14_lattices(k8_filter_0(X0,X1)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t66_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/sandbox/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/sandbox/benchmark/theBenchmark.p',fc6_lattice2) ).
fof(f2596,axiom,
! [X0] :
( l3_lattices(X0)
=> k1_lattice2(X0) = g3_lattices(u1_struct_0(X0),u1_lattices(X0),u2_lattices(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d2_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/sandbox/benchmark/theBenchmark.p',t18_lattice2) ).
fof(f2598,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_lattices(X0)
& l3_lattices(X0) )
=> k1_lattice2(k1_lattice2(X0)) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t19_lattice2) ).
fof(f2644,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( v13_lattices(X0)
<=> v14_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t63_lattice2) ).
fof(f2645,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( v14_lattices(X0)
<=> v13_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t64_lattice2) ).
fof(f2669,axiom,
! [X0] :
( l3_lattices(X0)
=> ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k1_lattice2) ).
fof(f2773,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_nat_lat(X1,X0)
=> ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& l3_lattices(X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m2_nat_lat) ).
fof(f2857,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_lattice4(X1,X0)
=> m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m2_lattice4) ).
fof(f2870,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_filter_2(X1,X0)
=> ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m1_filter_2) ).
fof(f2872,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_filter_2(X1,X0)
<=> m1_filter_0(X1,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_m1_filter_2) ).
fof(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/sandbox/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/sandbox/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/sandbox/benchmark/theBenchmark.p',redefinition_k15_filter_2) ).
fof(f2913,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) )
=> m2_nat_lat(k23_filter_2(X0,X1),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k23_filter_2) ).
fof(f2941,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_filter_2(X1,X0)
<=> m1_filter_2(X1,k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t21_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/sandbox/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/sandbox/benchmark/theBenchmark.p',d8_filter_2) ).
fof(f3007,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) )
=> ! [X2] :
( m2_nat_lat(X2,X0)
=> ( X2 = k23_filter_2(X0,X1)
<=> ? [X3] :
( v1_funct_1(X3)
& v1_funct_2(X3,k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(X3,k2_zfmisc_1(X1,X1),X1)
& ? [X4] :
( v1_funct_1(X4)
& v1_funct_2(X4,k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(X4,k2_zfmisc_1(X1,X1),X1)
& X3 = k1_realset1(u2_lattices(X0),X1)
& X4 = k1_realset1(u1_lattices(X0),X1)
& X2 = g3_lattices(X1,X3,X4) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d16_filter_2) ).
fof(f3008,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) )
=> ( ~ v3_struct_0(k23_filter_2(X0,X1))
& v3_lattices(k23_filter_2(X0,X1))
& v4_lattices(k23_filter_2(X0,X1))
& v5_lattices(k23_filter_2(X0,X1))
& v6_lattices(k23_filter_2(X0,X1))
& v7_lattices(k23_filter_2(X0,X1))
& v8_lattices(k23_filter_2(X0,X1))
& v9_lattices(k23_filter_2(X0,X1))
& v10_lattices(k23_filter_2(X0,X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc5_filter_2) ).
fof(f3009,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_filter_2(X1,X0)
=> k8_filter_0(X0,X1) = k23_filter_2(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t70_filter_2) ).
fof(f3012,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) )
=> ( u1_struct_0(k23_filter_2(X0,X1)) = X1
& u2_lattices(k23_filter_2(X0,X1)) = k1_realset1(u2_lattices(X0),X1)
& u1_lattices(k23_filter_2(X0,X1)) = k1_realset1(u1_lattices(X0),X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t73_filter_2) ).
fof(f3015,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_filter_2(X1,X0)
=> ( v13_lattices(X0)
=> v13_lattices(k23_filter_2(X0,X1)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t76_filter_2) ).
fof(f3016,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_filter_2(X1,X0)
=> ( v13_lattices(X0)
=> v13_lattices(k23_filter_2(X0,X1)) ) ) ),
inference(negated_conjecture,[status(cth)],[f3015]) ).
fof(f3036,plain,
! [X0] :
( ! [X1] :
( ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) )
| ~ m1_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2870]) ).
fof(f3037,plain,
! [X0] :
( ! [X1] :
( ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) )
| ~ m1_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f3036]) ).
fof(f3040,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(f3041,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,[],[f3040]) ).
fof(f3042,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(f3043,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,[],[f3042]) ).
fof(f3100,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(f3101,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,[],[f3100]) ).
fof(f3102,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(f3103,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,[],[f3102]) ).
fof(f3122,plain,
! [X0,X1] :
( m2_nat_lat(k23_filter_2(X0,X1),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0) ),
inference(ennf_transformation,[],[f2913]) ).
fof(f3123,plain,
! [X0,X1] :
( m2_nat_lat(k23_filter_2(X0,X1),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0) ),
inference(flattening,[],[f3122]) ).
fof(f3175,plain,
! [X0] :
( ! [X1] :
( m2_filter_2(X1,X0)
<=> m1_filter_2(X1,k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2941]) ).
fof(f3176,plain,
! [X0] :
( ! [X1] :
( m2_filter_2(X1,X0)
<=> m1_filter_2(X1,k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f3175]) ).
fof(f3177,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(f3178,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,[],[f3177]) ).
fof(f3199,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(f3200,plain,
! [X0] :
( k17_filter_2(X0) = u1_struct_0(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f3199]) ).
fof(f3307,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( X2 = k23_filter_2(X0,X1)
<=> ? [X3] :
( v1_funct_1(X3)
& v1_funct_2(X3,k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(X3,k2_zfmisc_1(X1,X1),X1)
& ? [X4] :
( v1_funct_1(X4)
& v1_funct_2(X4,k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(X4,k2_zfmisc_1(X1,X1),X1)
& X3 = k1_realset1(u2_lattices(X0),X1)
& X4 = k1_realset1(u1_lattices(X0),X1)
& X2 = g3_lattices(X1,X3,X4) ) ) )
| ~ m2_nat_lat(X2,X0) )
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f3007]) ).
fof(f3308,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( X2 = k23_filter_2(X0,X1)
<=> ? [X3] :
( v1_funct_1(X3)
& v1_funct_2(X3,k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(X3,k2_zfmisc_1(X1,X1),X1)
& ? [X4] :
( v1_funct_1(X4)
& v1_funct_2(X4,k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(X4,k2_zfmisc_1(X1,X1),X1)
& X3 = k1_realset1(u2_lattices(X0),X1)
& X4 = k1_realset1(u1_lattices(X0),X1)
& X2 = g3_lattices(X1,X3,X4) ) ) )
| ~ m2_nat_lat(X2,X0) )
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f3307]) ).
fof(f3309,plain,
! [X0,X1] :
( ( ~ v3_struct_0(k23_filter_2(X0,X1))
& v3_lattices(k23_filter_2(X0,X1))
& v4_lattices(k23_filter_2(X0,X1))
& v5_lattices(k23_filter_2(X0,X1))
& v6_lattices(k23_filter_2(X0,X1))
& v7_lattices(k23_filter_2(X0,X1))
& v8_lattices(k23_filter_2(X0,X1))
& v9_lattices(k23_filter_2(X0,X1))
& v10_lattices(k23_filter_2(X0,X1)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0) ),
inference(ennf_transformation,[],[f3008]) ).
fof(f3310,plain,
! [X0,X1] :
( ( ~ v3_struct_0(k23_filter_2(X0,X1))
& v3_lattices(k23_filter_2(X0,X1))
& v4_lattices(k23_filter_2(X0,X1))
& v5_lattices(k23_filter_2(X0,X1))
& v6_lattices(k23_filter_2(X0,X1))
& v7_lattices(k23_filter_2(X0,X1))
& v8_lattices(k23_filter_2(X0,X1))
& v9_lattices(k23_filter_2(X0,X1))
& v10_lattices(k23_filter_2(X0,X1)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0) ),
inference(flattening,[],[f3309]) ).
fof(f3311,plain,
! [X0] :
( ! [X1] :
( k8_filter_0(X0,X1) = k23_filter_2(X0,X1)
| ~ m1_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f3009]) ).
fof(f3312,plain,
! [X0] :
( ! [X1] :
( k8_filter_0(X0,X1) = k23_filter_2(X0,X1)
| ~ m1_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f3311]) ).
fof(f3317,plain,
! [X0] :
( ! [X1] :
( ( u1_struct_0(k23_filter_2(X0,X1)) = X1
& u2_lattices(k23_filter_2(X0,X1)) = k1_realset1(u2_lattices(X0),X1)
& u1_lattices(k23_filter_2(X0,X1)) = k1_realset1(u1_lattices(X0),X1) )
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f3012]) ).
fof(f3318,plain,
! [X0] :
( ! [X1] :
( ( u1_struct_0(k23_filter_2(X0,X1)) = X1
& u2_lattices(k23_filter_2(X0,X1)) = k1_realset1(u2_lattices(X0),X1)
& u1_lattices(k23_filter_2(X0,X1)) = k1_realset1(u1_lattices(X0),X1) )
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f3317]) ).
fof(f3323,plain,
? [X0] :
( ? [X1] :
( ~ v13_lattices(k23_filter_2(X0,X1))
& v13_lattices(X0)
& m2_filter_2(X1,X0) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(ennf_transformation,[],[f3016]) ).
fof(f3324,plain,
? [X0] :
( ? [X1] :
( ~ v13_lattices(k23_filter_2(X0,X1))
& v13_lattices(X0)
& m2_filter_2(X1,X0) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(flattening,[],[f3323]) ).
fof(f3334,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(f3335,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,[],[f3334]) ).
fof(f3439,plain,
! [X0] :
( ! [X1] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& l3_lattices(X1) )
| ~ m2_nat_lat(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2773]) ).
fof(f3440,plain,
! [X0] :
( ! [X1] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& l3_lattices(X1) )
| ~ m2_nat_lat(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f3439]) ).
fof(f3447,plain,
! [X0] :
( ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2669]) ).
fof(f3448,plain,
! [X0] :
( k1_lattice2(k1_lattice2(X0)) = X0
| v3_struct_0(X0)
| ~ v3_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2598]) ).
fof(f3449,plain,
! [X0] :
( k1_lattice2(k1_lattice2(X0)) = X0
| v3_struct_0(X0)
| ~ v3_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f3448]) ).
fof(f3450,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(f3451,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,[],[f3450]) ).
fof(f3452,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(f3453,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f3452]) ).
fof(f3616,plain,
! [X0] :
( k1_lattice2(X0) = g3_lattices(u1_struct_0(X0),u1_lattices(X0),u2_lattices(X0))
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2596]) ).
fof(f3619,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(f3620,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,[],[f3619]) ).
fof(f3683,plain,
! [X0] :
( ( v14_lattices(X0)
<=> v13_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2645]) ).
fof(f3684,plain,
! [X0] :
( ( v14_lattices(X0)
<=> v13_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f3683]) ).
fof(f3685,plain,
! [X0] :
( ( v13_lattices(X0)
<=> v14_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2644]) ).
fof(f3686,plain,
! [X0] :
( ( v13_lattices(X0)
<=> v14_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f3685]) ).
fof(f3858,plain,
! [X0] :
( ! [X1] :
( v14_lattices(k8_filter_0(X0,X1))
| ~ v14_lattices(X0)
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2512]) ).
fof(f3859,plain,
! [X0] :
( ! [X1] :
( v14_lattices(k8_filter_0(X0,X1))
| ~ v14_lattices(X0)
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f3858]) ).
fof(f4976,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,[],[f3041]) ).
fof(f4996,plain,
! [X0] :
( ! [X1] :
( ( m2_filter_2(X1,X0)
| ~ m1_filter_2(X1,k1_lattice2(X0)) )
& ( m1_filter_2(X1,k1_lattice2(X0))
| ~ m2_filter_2(X1,X0) ) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f3176]) ).
fof(f5040,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( X2 = k23_filter_2(X0,X1)
| ! [X3] :
( ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(X3,k2_zfmisc_1(X1,X1),X1)
| ! [X4] :
( ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(X4,k2_zfmisc_1(X1,X1),X1)
| k1_realset1(u2_lattices(X0),X1) != X3
| k1_realset1(u1_lattices(X0),X1) != X4
| g3_lattices(X1,X3,X4) != X2 ) ) )
& ( ? [X3] :
( v1_funct_1(X3)
& v1_funct_2(X3,k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(X3,k2_zfmisc_1(X1,X1),X1)
& ? [X4] :
( v1_funct_1(X4)
& v1_funct_2(X4,k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(X4,k2_zfmisc_1(X1,X1),X1)
& X3 = k1_realset1(u2_lattices(X0),X1)
& X4 = k1_realset1(u1_lattices(X0),X1)
& X2 = g3_lattices(X1,X3,X4) ) )
| k23_filter_2(X0,X1) != X2 ) )
| ~ m2_nat_lat(X2,X0) )
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f3308]) ).
fof(f5041,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( X2 = k23_filter_2(X0,X1)
| ! [X3] :
( ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(X3,k2_zfmisc_1(X1,X1),X1)
| ! [X4] :
( ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(X4,k2_zfmisc_1(X1,X1),X1)
| k1_realset1(u2_lattices(X0),X1) != X3
| k1_realset1(u1_lattices(X0),X1) != X4
| g3_lattices(X1,X3,X4) != X2 ) ) )
& ( ? [X5] :
( v1_funct_1(X5)
& v1_funct_2(X5,k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(X5,k2_zfmisc_1(X1,X1),X1)
& ? [X6] :
( v1_funct_1(X6)
& v1_funct_2(X6,k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(X6,k2_zfmisc_1(X1,X1),X1)
& k1_realset1(u2_lattices(X0),X1) = X5
& k1_realset1(u1_lattices(X0),X1) = X6
& g3_lattices(X1,X5,X6) = X2 ) )
| k23_filter_2(X0,X1) != X2 ) )
| ~ m2_nat_lat(X2,X0) )
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(rectify,[],[f5040]) ).
fof(f5042,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( X2 = k23_filter_2(X0,X1)
| ! [X3] :
( ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(X3,k2_zfmisc_1(X1,X1),X1)
| ! [X4] :
( ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(X4,k2_zfmisc_1(X1,X1),X1)
| k1_realset1(u2_lattices(X0),X1) != X3
| k1_realset1(u1_lattices(X0),X1) != X4
| g3_lattices(X1,X3,X4) != X2 ) ) )
& ( ( v1_funct_1(sK31(X0,X1,X2))
& v1_funct_2(sK31(X0,X1,X2),k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(sK31(X0,X1,X2),k2_zfmisc_1(X1,X1),X1)
& v1_funct_1(sK32(X0,X1,X2))
& v1_funct_2(sK32(X0,X1,X2),k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(sK32(X0,X1,X2),k2_zfmisc_1(X1,X1),X1)
& k1_realset1(u2_lattices(X0),X1) = sK31(X0,X1,X2)
& k1_realset1(u1_lattices(X0),X1) = sK32(X0,X1,X2)
& g3_lattices(X1,sK31(X0,X1,X2),sK32(X0,X1,X2)) = X2 )
| k23_filter_2(X0,X1) != X2 ) )
| ~ m2_nat_lat(X2,X0) )
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK31,sK32]),skolemize(X5,sK31(X0,X1,X2)),skolemize(X6,sK32(X0,X1,X2))],[f5041]) ).
fof(f5044,plain,
( ~ v13_lattices(k23_filter_2(sK33,sK34))
& v13_lattices(sK33)
& m2_filter_2(sK34,sK33)
& ~ v3_struct_0(sK33)
& v10_lattices(sK33)
& l3_lattices(sK33) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK33,sK34]),skolemize(X0,sK33),skolemize(X1,sK34)],[f3324]) ).
fof(f5223,plain,
! [X0] :
( ( ( v14_lattices(X0)
| ~ v13_lattices(k1_lattice2(X0)) )
& ( v13_lattices(k1_lattice2(X0))
| ~ v14_lattices(X0) ) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f3684]) ).
fof(f5224,plain,
! [X0] :
( ( ( v13_lattices(X0)
| ~ v14_lattices(k1_lattice2(X0)) )
& ( v14_lattices(k1_lattice2(X0))
| ~ v13_lattices(X0) ) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f3686]) ).
fof(f5675,plain,
! [X0,X1] :
( ~ m1_filter_2(X1,X0)
| m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f3037]) ).
fof(f5678,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,[],[f4976]) ).
fof(f5680,plain,
! [X0,X1] :
( ~ l3_lattices(X0)
| ~ m2_filter_2(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| m2_lattice4(X1,X0) ),
inference(cnf_transformation,[],[f3043]) ).
fof(f5681,plain,
! [X0,X1] :
( ~ l3_lattices(X0)
| ~ m2_filter_2(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v1_xboole_0(X1) ),
inference(cnf_transformation,[],[f3043]) ).
fof(f5713,plain,
! [X0,X1] :
( ~ m2_filter_2(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| m1_filter_2(k15_filter_2(X0,X1),k1_lattice2(X0)) ),
inference(cnf_transformation,[],[f3101]) ).
fof(f5714,plain,
! [X0,X1] :
( ~ l3_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| k7_filter_2(X0,X1) = k15_filter_2(X0,X1)
| ~ m2_filter_2(X1,X0) ),
inference(cnf_transformation,[],[f3103]) ).
fof(f5725,plain,
! [X0,X1] :
( ~ l3_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| m2_nat_lat(k23_filter_2(X0,X1),X0)
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0) ),
inference(cnf_transformation,[],[f3123]) ).
fof(f5791,plain,
! [X0,X1] :
( ~ l3_lattices(X0)
| ~ m2_filter_2(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| m1_filter_2(X1,k1_lattice2(X0)) ),
inference(cnf_transformation,[],[f4996]) ).
fof(f5792,plain,
! [X0,X1] :
( ~ l3_lattices(X0)
| ~ m1_filter_2(X1,k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| m2_filter_2(X1,X0) ),
inference(cnf_transformation,[],[f4996]) ).
fof(f5793,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| k7_filter_2(X0,X1) = X1
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f3178]) ).
fof(f5818,plain,
! [X0] :
( ~ l3_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| u1_struct_0(X0) = k17_filter_2(X0) ),
inference(cnf_transformation,[],[f3200]) ).
fof(f5983,plain,
! [X2,X0,X1] :
( g3_lattices(X1,sK31(X0,X1,X2),sK32(X0,X1,X2)) = X2
| k23_filter_2(X0,X1) != X2
| ~ m2_nat_lat(X2,X0)
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f5042]) ).
fof(f5984,plain,
! [X2,X0,X1] :
( k1_realset1(u1_lattices(X0),X1) = sK32(X0,X1,X2)
| k23_filter_2(X0,X1) != X2
| ~ m2_nat_lat(X2,X0)
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f5042]) ).
fof(f5985,plain,
! [X2,X0,X1] :
( k1_realset1(u2_lattices(X0),X1) = sK31(X0,X1,X2)
| k23_filter_2(X0,X1) != X2
| ~ m2_nat_lat(X2,X0)
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f5042]) ).
fof(f6000,plain,
! [X0,X1] :
( v3_lattices(k23_filter_2(X0,X1))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0) ),
inference(cnf_transformation,[],[f3310]) ).
fof(f6001,plain,
! [X0,X1] :
( ~ v3_struct_0(k23_filter_2(X0,X1))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0) ),
inference(cnf_transformation,[],[f3310]) ).
fof(f6002,plain,
! [X0,X1] :
( ~ m1_filter_2(X1,X0)
| k8_filter_0(X0,X1) = k23_filter_2(X0,X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f3312]) ).
fof(f6006,plain,
! [X0,X1] :
( ~ l3_lattices(X0)
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| k1_realset1(u1_lattices(X0),X1) = u1_lattices(k23_filter_2(X0,X1)) ),
inference(cnf_transformation,[],[f3318]) ).
fof(f6007,plain,
! [X0,X1] :
( ~ l3_lattices(X0)
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| k1_realset1(u2_lattices(X0),X1) = u2_lattices(k23_filter_2(X0,X1)) ),
inference(cnf_transformation,[],[f3318]) ).
fof(f6008,plain,
! [X0,X1] :
( ~ l3_lattices(X0)
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| u1_struct_0(k23_filter_2(X0,X1)) = X1 ),
inference(cnf_transformation,[],[f3318]) ).
fof(f6013,plain,
l3_lattices(sK33),
inference(cnf_transformation,[],[f5044]) ).
fof(f6014,plain,
v10_lattices(sK33),
inference(cnf_transformation,[],[f5044]) ).
fof(f6015,plain,
~ v3_struct_0(sK33),
inference(cnf_transformation,[],[f5044]) ).
fof(f6016,plain,
m2_filter_2(sK34,sK33),
inference(cnf_transformation,[],[f5044]) ).
fof(f6017,plain,
v13_lattices(sK33),
inference(cnf_transformation,[],[f5044]) ).
fof(f6018,plain,
~ v13_lattices(k23_filter_2(sK33,sK34)),
inference(cnf_transformation,[],[f5044]) ).
fof(f6039,plain,
! [X0,X1] :
( ~ l3_lattices(X0)
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ),
inference(cnf_transformation,[],[f3335]) ).
fof(f6152,plain,
! [X0,X1] :
( ~ l3_lattices(X0)
| ~ m2_nat_lat(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| l3_lattices(X1) ),
inference(cnf_transformation,[],[f3440]) ).
fof(f6153,plain,
! [X0,X1] :
( ~ l3_lattices(X0)
| ~ m2_nat_lat(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| v10_lattices(X1) ),
inference(cnf_transformation,[],[f3440]) ).
fof(f6170,plain,
! [X0] :
( ~ l3_lattices(X0)
| l3_lattices(k1_lattice2(X0)) ),
inference(cnf_transformation,[],[f3447]) ).
fof(f6172,plain,
! [X0] :
( ~ v3_lattices(X0)
| v3_struct_0(X0)
| k1_lattice2(k1_lattice2(X0)) = X0
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f3449]) ).
fof(f6173,plain,
! [X0] :
( v10_lattices(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f3451]) ).
fof(f6183,plain,
! [X0] :
( ~ v3_struct_0(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f3453]) ).
fof(f6428,plain,
! [X0] :
( ~ l3_lattices(X0)
| k1_lattice2(X0) = g3_lattices(u1_struct_0(X0),u1_lattices(X0),u2_lattices(X0)) ),
inference(cnf_transformation,[],[f3616]) ).
fof(f6432,plain,
! [X0] :
( ~ l3_lattices(X0)
| v3_struct_0(X0)
| u1_lattices(X0) = u2_lattices(k1_lattice2(X0)) ),
inference(cnf_transformation,[],[f3620]) ).
fof(f6433,plain,
! [X0] :
( ~ l3_lattices(X0)
| v3_struct_0(X0)
| u2_lattices(X0) = u1_lattices(k1_lattice2(X0)) ),
inference(cnf_transformation,[],[f3620]) ).
fof(f6515,plain,
! [X0] :
( v13_lattices(k1_lattice2(X0))
| ~ v14_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f5223]) ).
fof(f6517,plain,
! [X0] :
( v14_lattices(k1_lattice2(X0))
| ~ v13_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f5224]) ).
fof(f6804,plain,
! [X0,X1] :
( ~ v14_lattices(X0)
| v14_lattices(k8_filter_0(X0,X1))
| ~ m1_filter_0(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f3859]) ).
fof(f9032,plain,
! [X0,X1] :
( ~ l3_lattices(X0)
| ~ m2_nat_lat(k23_filter_2(X0,X1),X0)
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| k1_realset1(u2_lattices(X0),X1) = sK31(X0,X1,k23_filter_2(X0,X1)) ),
inference(equality_resolution,[],[f5985]) ).
fof(f9033,plain,
! [X0,X1] :
( ~ l3_lattices(X0)
| ~ m2_nat_lat(k23_filter_2(X0,X1),X0)
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| k1_realset1(u1_lattices(X0),X1) = sK32(X0,X1,k23_filter_2(X0,X1)) ),
inference(equality_resolution,[],[f5984]) ).
fof(f9034,plain,
! [X0,X1] :
( ~ m2_nat_lat(k23_filter_2(X0,X1),X0)
| k23_filter_2(X0,X1) = g3_lattices(X1,sK31(X0,X1,k23_filter_2(X0,X1)),sK32(X0,X1,k23_filter_2(X0,X1)))
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(equality_resolution,[],[f5983]) ).
fof(f9666,plain,
! [X0] :
( ~ m2_filter_2(X0,sK33)
| v3_struct_0(sK33)
| ~ v10_lattices(sK33)
| m2_lattice4(X0,sK33) ),
inference(resolution,[],[f5680,f6013]) ).
fof(f9667,plain,
! [X0] :
( ~ m2_filter_2(X0,sK33)
| ~ v10_lattices(sK33)
| m2_lattice4(X0,sK33) ),
inference(forward_subsumption_resolution,[],[f9666,f6015]) ).
fof(f9668,plain,
! [X0] :
( ~ m2_filter_2(X0,sK33)
| m2_lattice4(X0,sK33) ),
inference(forward_subsumption_resolution,[],[f9667,f6014]) ).
fof(f9669,plain,
m2_lattice4(sK34,sK33),
inference(resolution,[],[f9668,f6016]) ).
fof(f9670,plain,
! [X0] :
( v1_xboole_0(X0)
| ~ m2_lattice4(X0,sK33)
| v3_struct_0(sK33)
| ~ v10_lattices(sK33)
| k1_realset1(u2_lattices(sK33),X0) = u2_lattices(k23_filter_2(sK33,X0)) ),
inference(resolution,[],[f6007,f6013]) ).
fof(f9671,plain,
! [X0] :
( v1_xboole_0(X0)
| ~ m2_lattice4(X0,sK33)
| ~ v10_lattices(sK33)
| k1_realset1(u2_lattices(sK33),X0) = u2_lattices(k23_filter_2(sK33,X0)) ),
inference(forward_subsumption_resolution,[],[f9670,f6015]) ).
fof(f9672,plain,
! [X0] :
( ~ m2_lattice4(X0,sK33)
| v1_xboole_0(X0)
| k1_realset1(u2_lattices(sK33),X0) = u2_lattices(k23_filter_2(sK33,X0)) ),
inference(forward_subsumption_resolution,[],[f9671,f6014]) ).
fof(f9673,plain,
( v1_xboole_0(sK34)
| k1_realset1(u2_lattices(sK33),sK34) = u2_lattices(k23_filter_2(sK33,sK34)) ),
inference(resolution,[],[f9672,f9669]) ).
fof(f9675,definition,
( spl421_5
<=> k1_realset1(u2_lattices(sK33),sK34) = u2_lattices(k23_filter_2(sK33,sK34)) ),
introduced(definition,[new_symbols(definition,[spl421_5])],[avatar_definition]) ).
fof(f9676,plain,
( k1_realset1(u2_lattices(sK33),sK34) = u2_lattices(k23_filter_2(sK33,sK34))
| ~ spl421_5 ),
inference(avatar_component_clause,[],[f9675]) ).
fof(f9678,definition,
( spl421_6
<=> v1_xboole_0(sK34) ),
introduced(definition,[new_symbols(definition,[spl421_6])],[avatar_definition]) ).
fof(f9679,plain,
( v1_xboole_0(sK34)
| ~ spl421_6 ),
inference(avatar_component_clause,[],[f9678]) ).
fof(f9680,plain,
( spl421_5
| spl421_6 ),
inference(avatar_split_clause,[],[f9673,f9678,f9675]) ).
fof(f9681,plain,
! [X0] :
( v1_xboole_0(X0)
| ~ m2_lattice4(X0,sK33)
| v3_struct_0(sK33)
| ~ v10_lattices(sK33)
| k1_realset1(u1_lattices(sK33),X0) = u1_lattices(k23_filter_2(sK33,X0)) ),
inference(resolution,[],[f6006,f6013]) ).
fof(f9682,plain,
! [X0] :
( v1_xboole_0(X0)
| ~ m2_lattice4(X0,sK33)
| ~ v10_lattices(sK33)
| k1_realset1(u1_lattices(sK33),X0) = u1_lattices(k23_filter_2(sK33,X0)) ),
inference(forward_subsumption_resolution,[],[f9681,f6015]) ).
fof(f9683,plain,
! [X0] :
( ~ m2_lattice4(X0,sK33)
| v1_xboole_0(X0)
| k1_realset1(u1_lattices(sK33),X0) = u1_lattices(k23_filter_2(sK33,X0)) ),
inference(forward_subsumption_resolution,[],[f9682,f6014]) ).
fof(f9684,plain,
( v1_xboole_0(sK34)
| k1_realset1(u1_lattices(sK33),sK34) = u1_lattices(k23_filter_2(sK33,sK34)) ),
inference(resolution,[],[f9683,f9669]) ).
fof(f9686,definition,
( spl421_7
<=> k1_realset1(u1_lattices(sK33),sK34) = u1_lattices(k23_filter_2(sK33,sK34)) ),
introduced(definition,[new_symbols(definition,[spl421_7])],[avatar_definition]) ).
fof(f9687,plain,
( k1_realset1(u1_lattices(sK33),sK34) = u1_lattices(k23_filter_2(sK33,sK34))
| ~ spl421_7 ),
inference(avatar_component_clause,[],[f9686]) ).
fof(f9688,plain,
( spl421_7
| spl421_6 ),
inference(avatar_split_clause,[],[f9684,f9678,f9686]) ).
fof(f9689,plain,
! [X0] :
( v3_struct_0(sK33)
| ~ v10_lattices(sK33)
| k7_filter_2(sK33,X0) = k15_filter_2(sK33,X0)
| ~ m2_filter_2(X0,sK33) ),
inference(resolution,[],[f5714,f6013]) ).
fof(f9690,plain,
! [X0] :
( ~ v10_lattices(sK33)
| k7_filter_2(sK33,X0) = k15_filter_2(sK33,X0)
| ~ m2_filter_2(X0,sK33) ),
inference(forward_subsumption_resolution,[],[f9689,f6015]) ).
fof(f9691,plain,
! [X0] :
( ~ m2_filter_2(X0,sK33)
| k7_filter_2(sK33,X0) = k15_filter_2(sK33,X0) ),
inference(forward_subsumption_resolution,[],[f9690,f6014]) ).
fof(f9692,plain,
k7_filter_2(sK33,sK34) = k15_filter_2(sK33,sK34),
inference(resolution,[],[f9691,f6016]) ).
fof(f9693,plain,
! [X0] :
( ~ m2_filter_2(X0,sK33)
| v3_struct_0(sK33)
| ~ v10_lattices(sK33)
| m1_filter_2(X0,k1_lattice2(sK33)) ),
inference(resolution,[],[f5791,f6013]) ).
fof(f9694,plain,
! [X0] :
( ~ m2_filter_2(X0,sK33)
| ~ v10_lattices(sK33)
| m1_filter_2(X0,k1_lattice2(sK33)) ),
inference(forward_subsumption_resolution,[],[f9693,f6015]) ).
fof(f9695,plain,
! [X0] :
( ~ m2_filter_2(X0,sK33)
| m1_filter_2(X0,k1_lattice2(sK33)) ),
inference(forward_subsumption_resolution,[],[f9694,f6014]) ).
fof(f9696,plain,
m1_filter_2(sK34,k1_lattice2(sK33)),
inference(resolution,[],[f9695,f6016]) ).
fof(f9697,plain,
( k8_filter_0(k1_lattice2(sK33),sK34) = k23_filter_2(k1_lattice2(sK33),sK34)
| v3_struct_0(k1_lattice2(sK33))
| ~ v10_lattices(k1_lattice2(sK33))
| ~ l3_lattices(k1_lattice2(sK33)) ),
inference(resolution,[],[f9696,f6002]) ).
fof(f9698,plain,
( m1_filter_0(sK34,k1_lattice2(sK33))
| v3_struct_0(k1_lattice2(sK33))
| ~ v10_lattices(k1_lattice2(sK33))
| ~ l3_lattices(k1_lattice2(sK33)) ),
inference(resolution,[],[f9696,f5678]) ).
fof(f9700,definition,
( spl421_8
<=> l3_lattices(k1_lattice2(sK33)) ),
introduced(definition,[new_symbols(definition,[spl421_8])],[avatar_definition]) ).
fof(f9701,plain,
( ~ l3_lattices(k1_lattice2(sK33))
| spl421_8 ),
inference(avatar_component_clause,[],[f9700]) ).
fof(f9703,definition,
( spl421_9
<=> v10_lattices(k1_lattice2(sK33)) ),
introduced(definition,[new_symbols(definition,[spl421_9])],[avatar_definition]) ).
fof(f9704,plain,
( ~ v10_lattices(k1_lattice2(sK33))
| spl421_9 ),
inference(avatar_component_clause,[],[f9703]) ).
fof(f9706,definition,
( spl421_10
<=> v3_struct_0(k1_lattice2(sK33)) ),
introduced(definition,[new_symbols(definition,[spl421_10])],[avatar_definition]) ).
fof(f9707,plain,
( v3_struct_0(k1_lattice2(sK33))
| ~ spl421_10 ),
inference(avatar_component_clause,[],[f9706]) ).
fof(f9709,definition,
( spl421_11
<=> m1_filter_0(sK34,k1_lattice2(sK33)) ),
introduced(definition,[new_symbols(definition,[spl421_11])],[avatar_definition]) ).
fof(f9710,plain,
( m1_filter_0(sK34,k1_lattice2(sK33))
| ~ spl421_11 ),
inference(avatar_component_clause,[],[f9709]) ).
fof(f9711,plain,
( ~ spl421_8
| ~ spl421_9
| spl421_10
| spl421_11 ),
inference(avatar_split_clause,[],[f9698,f9709,f9706,f9703,f9700]) ).
fof(f9713,definition,
( spl421_12
<=> k8_filter_0(k1_lattice2(sK33),sK34) = k23_filter_2(k1_lattice2(sK33),sK34) ),
introduced(definition,[new_symbols(definition,[spl421_12])],[avatar_definition]) ).
fof(f9714,plain,
( k8_filter_0(k1_lattice2(sK33),sK34) = k23_filter_2(k1_lattice2(sK33),sK34)
| ~ spl421_12 ),
inference(avatar_component_clause,[],[f9713]) ).
fof(f9715,plain,
( ~ spl421_8
| ~ spl421_9
| spl421_10
| spl421_12 ),
inference(avatar_split_clause,[],[f9697,f9713,f9706,f9703,f9700]) ).
fof(f9716,plain,
! [X0] :
( v3_struct_0(sK33)
| ~ v10_lattices(sK33)
| m2_nat_lat(k23_filter_2(sK33,X0),sK33)
| v1_xboole_0(X0)
| ~ m2_lattice4(X0,sK33) ),
inference(resolution,[],[f5725,f6013]) ).
fof(f9717,plain,
! [X0] :
( ~ v10_lattices(sK33)
| m2_nat_lat(k23_filter_2(sK33,X0),sK33)
| v1_xboole_0(X0)
| ~ m2_lattice4(X0,sK33) ),
inference(forward_subsumption_resolution,[],[f9716,f6015]) ).
fof(f9718,plain,
! [X0] :
( m2_nat_lat(k23_filter_2(sK33,X0),sK33)
| v1_xboole_0(X0)
| ~ m2_lattice4(X0,sK33) ),
inference(forward_subsumption_resolution,[],[f9717,f6014]) ).
fof(f9724,plain,
! [X0] :
( v1_xboole_0(X0)
| ~ m2_lattice4(X0,sK33)
| v3_struct_0(sK33)
| ~ v10_lattices(sK33)
| u1_struct_0(k23_filter_2(sK33,X0)) = X0 ),
inference(resolution,[],[f6008,f6013]) ).
fof(f9725,plain,
! [X0] :
( v1_xboole_0(X0)
| ~ m2_lattice4(X0,sK33)
| ~ v10_lattices(sK33)
| u1_struct_0(k23_filter_2(sK33,X0)) = X0 ),
inference(forward_subsumption_resolution,[],[f9724,f6015]) ).
fof(f9726,plain,
! [X0] :
( ~ m2_lattice4(X0,sK33)
| v1_xboole_0(X0)
| u1_struct_0(k23_filter_2(sK33,X0)) = X0 ),
inference(forward_subsumption_resolution,[],[f9725,f6014]) ).
fof(f9727,plain,
( v1_xboole_0(sK34)
| sK34 = u1_struct_0(k23_filter_2(sK33,sK34)) ),
inference(resolution,[],[f9726,f9669]) ).
fof(f9728,plain,
( $false
| ~ spl421_6 ),
inference(unit_resulting_resolution,[],[f5681,f9679,f6014,f6015,f6016,f6013]) ).
fof(f9730,plain,
~ spl421_6,
inference(avatar_contradiction_clause,[],[f9728]) ).
fof(f9734,definition,
( spl421_13
<=> sK34 = u1_struct_0(k23_filter_2(sK33,sK34)) ),
introduced(definition,[new_symbols(definition,[spl421_13])],[avatar_definition]) ).
fof(f9735,plain,
( sK34 = u1_struct_0(k23_filter_2(sK33,sK34))
| ~ spl421_13 ),
inference(avatar_component_clause,[],[f9734]) ).
fof(f9736,plain,
( spl421_13
| spl421_6 ),
inference(avatar_split_clause,[],[f9727,f9678,f9734]) ).
fof(f9738,plain,
l3_lattices(k1_lattice2(sK33)),
inference(resolution,[],[f6170,f6013]) ).
fof(f9740,plain,
( $false
| spl421_8 ),
inference(forward_subsumption_resolution,[],[f9738,f9701]) ).
fof(f9741,plain,
spl421_8,
inference(avatar_contradiction_clause,[],[f9740]) ).
fof(f9745,plain,
! [X0] :
( v3_struct_0(k1_lattice2(sK33))
| ~ v10_lattices(k1_lattice2(sK33))
| m2_nat_lat(k23_filter_2(k1_lattice2(sK33),X0),k1_lattice2(sK33))
| v1_xboole_0(X0)
| ~ m2_lattice4(X0,k1_lattice2(sK33)) ),
inference(resolution,[],[f9738,f5725]) ).
fof(f9751,plain,
( m2_lattice4(sK34,k1_lattice2(sK33))
| v3_struct_0(k1_lattice2(sK33))
| ~ v10_lattices(k1_lattice2(sK33))
| ~ l3_lattices(k1_lattice2(sK33)) ),
inference(resolution,[],[f5675,f9696]) ).
fof(f9766,definition,
( spl421_16
<=> l3_lattices(k23_filter_2(sK33,sK34)) ),
introduced(definition,[new_symbols(definition,[spl421_16])],[avatar_definition]) ).
fof(f9769,definition,
( spl421_17
<=> v10_lattices(k23_filter_2(sK33,sK34)) ),
introduced(definition,[new_symbols(definition,[spl421_17])],[avatar_definition]) ).
fof(f9770,plain,
( ~ v10_lattices(k23_filter_2(sK33,sK34))
| spl421_17 ),
inference(avatar_component_clause,[],[f9769]) ).
fof(f9772,definition,
( spl421_18
<=> v3_struct_0(k23_filter_2(sK33,sK34)) ),
introduced(definition,[new_symbols(definition,[spl421_18])],[avatar_definition]) ).
fof(f9773,plain,
( v3_struct_0(k23_filter_2(sK33,sK34))
| ~ spl421_18 ),
inference(avatar_component_clause,[],[f9772]) ).
fof(f9782,plain,
( v3_struct_0(sK33)
| ~ v10_lattices(sK33)
| ~ l3_lattices(sK33)
| spl421_9 ),
inference(resolution,[],[f6173,f9704]) ).
fof(f9784,plain,
( ~ v10_lattices(sK33)
| ~ l3_lattices(sK33)
| spl421_9 ),
inference(forward_subsumption_resolution,[],[f9782,f6015]) ).
fof(f9785,plain,
( ~ l3_lattices(sK33)
| spl421_9 ),
inference(forward_subsumption_resolution,[],[f9784,f6014]) ).
fof(f9786,plain,
( $false
| spl421_9 ),
inference(forward_subsumption_resolution,[],[f9785,f6013]) ).
fof(f9787,plain,
spl421_9,
inference(avatar_contradiction_clause,[],[f9786]) ).
fof(f9789,plain,
( v3_struct_0(sK33)
| ~ l3_lattices(sK33)
| ~ spl421_10 ),
inference(resolution,[],[f6183,f9707]) ).
fof(f9791,plain,
( ~ l3_lattices(sK33)
| ~ spl421_10 ),
inference(forward_subsumption_resolution,[],[f9789,f6015]) ).
fof(f9792,plain,
( $false
| ~ spl421_10 ),
inference(forward_subsumption_resolution,[],[f9791,f6013]) ).
fof(f9793,plain,
~ spl421_10,
inference(avatar_contradiction_clause,[],[f9792]) ).
fof(f9811,definition,
( spl421_25
<=> ! [X0] :
( m2_nat_lat(k23_filter_2(k1_lattice2(sK33),X0),k1_lattice2(sK33))
| ~ m2_lattice4(X0,k1_lattice2(sK33))
| v1_xboole_0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl421_25])],[avatar_definition]) ).
fof(f9812,plain,
( ! [X0] :
( ~ m2_lattice4(X0,k1_lattice2(sK33))
| m2_nat_lat(k23_filter_2(k1_lattice2(sK33),X0),k1_lattice2(sK33))
| v1_xboole_0(X0) )
| ~ spl421_25 ),
inference(avatar_component_clause,[],[f9811]) ).
fof(f9813,plain,
( spl421_25
| ~ spl421_9
| spl421_10 ),
inference(avatar_split_clause,[],[f9745,f9706,f9703,f9811]) ).
fof(f9826,plain,
( m2_lattice4(sK34,k1_lattice2(sK33))
| v3_struct_0(k1_lattice2(sK33))
| ~ v10_lattices(k1_lattice2(sK33)) ),
inference(forward_subsumption_resolution,[],[f9751,f9738]) ).
fof(f9828,definition,
( spl421_29
<=> m2_lattice4(sK34,k1_lattice2(sK33)) ),
introduced(definition,[new_symbols(definition,[spl421_29])],[avatar_definition]) ).
fof(f9829,plain,
( m2_lattice4(sK34,k1_lattice2(sK33))
| ~ spl421_29 ),
inference(avatar_component_clause,[],[f9828]) ).
fof(f9830,plain,
( ~ spl421_9
| spl421_10
| spl421_29 ),
inference(avatar_split_clause,[],[f9826,f9828,f9706,f9703]) ).
fof(f9834,plain,
( ~ m2_nat_lat(k8_filter_0(k1_lattice2(sK33),sK34),k1_lattice2(sK33))
| k8_filter_0(k1_lattice2(sK33),sK34) = g3_lattices(sK34,sK31(k1_lattice2(sK33),sK34,k8_filter_0(k1_lattice2(sK33),sK34)),sK32(k1_lattice2(sK33),sK34,k8_filter_0(k1_lattice2(sK33),sK34)))
| v1_xboole_0(sK34)
| ~ m2_lattice4(sK34,k1_lattice2(sK33))
| v3_struct_0(k1_lattice2(sK33))
| ~ v10_lattices(k1_lattice2(sK33))
| ~ l3_lattices(k1_lattice2(sK33))
| ~ spl421_12 ),
inference(superposition,[],[f9034,f9714]) ).
fof(f9837,plain,
( ~ m2_nat_lat(k8_filter_0(k1_lattice2(sK33),sK34),k1_lattice2(sK33))
| k8_filter_0(k1_lattice2(sK33),sK34) = g3_lattices(sK34,sK31(k1_lattice2(sK33),sK34,k8_filter_0(k1_lattice2(sK33),sK34)),sK32(k1_lattice2(sK33),sK34,k8_filter_0(k1_lattice2(sK33),sK34)))
| v1_xboole_0(sK34)
| v3_struct_0(k1_lattice2(sK33))
| ~ v10_lattices(k1_lattice2(sK33))
| ~ l3_lattices(k1_lattice2(sK33))
| ~ spl421_12
| ~ spl421_29 ),
inference(forward_subsumption_resolution,[],[f9834,f9829]) ).
fof(f9840,plain,
( ~ m2_nat_lat(k8_filter_0(k1_lattice2(sK33),sK34),k1_lattice2(sK33))
| k8_filter_0(k1_lattice2(sK33),sK34) = g3_lattices(sK34,sK31(k1_lattice2(sK33),sK34,k8_filter_0(k1_lattice2(sK33),sK34)),sK32(k1_lattice2(sK33),sK34,k8_filter_0(k1_lattice2(sK33),sK34)))
| v1_xboole_0(sK34)
| v3_struct_0(k1_lattice2(sK33))
| ~ v10_lattices(k1_lattice2(sK33))
| ~ spl421_12
| ~ spl421_29 ),
inference(forward_subsumption_resolution,[],[f9837,f9738]) ).
fof(f9847,definition,
( spl421_31
<=> k8_filter_0(k1_lattice2(sK33),sK34) = g3_lattices(sK34,sK31(k1_lattice2(sK33),sK34,k8_filter_0(k1_lattice2(sK33),sK34)),sK32(k1_lattice2(sK33),sK34,k8_filter_0(k1_lattice2(sK33),sK34))) ),
introduced(definition,[new_symbols(definition,[spl421_31])],[avatar_definition]) ).
fof(f9848,plain,
( k8_filter_0(k1_lattice2(sK33),sK34) = g3_lattices(sK34,sK31(k1_lattice2(sK33),sK34,k8_filter_0(k1_lattice2(sK33),sK34)),sK32(k1_lattice2(sK33),sK34,k8_filter_0(k1_lattice2(sK33),sK34)))
| ~ spl421_31 ),
inference(avatar_component_clause,[],[f9847]) ).
fof(f9850,definition,
( spl421_32
<=> m2_nat_lat(k8_filter_0(k1_lattice2(sK33),sK34),k1_lattice2(sK33)) ),
introduced(definition,[new_symbols(definition,[spl421_32])],[avatar_definition]) ).
fof(f9852,plain,
( ~ spl421_9
| spl421_10
| spl421_6
| spl421_31
| ~ spl421_32
| ~ spl421_12
| ~ spl421_29 ),
inference(avatar_split_clause,[],[f9840,f9828,f9713,f9850,f9847,f9678,f9706,f9703]) ).
fof(f9857,plain,
( v3_struct_0(sK33)
| ~ v10_lattices(sK33)
| ~ l3_lattices(sK33)
| m1_filter_2(k15_filter_2(sK33,sK34),k1_lattice2(sK33)) ),
inference(resolution,[],[f5713,f6016]) ).
fof(f9858,plain,
( ~ v10_lattices(sK33)
| ~ l3_lattices(sK33)
| m1_filter_2(k15_filter_2(sK33,sK34),k1_lattice2(sK33)) ),
inference(forward_subsumption_resolution,[],[f9857,f6015]) ).
fof(f9859,plain,
( ~ l3_lattices(sK33)
| m1_filter_2(k15_filter_2(sK33,sK34),k1_lattice2(sK33)) ),
inference(forward_subsumption_resolution,[],[f9858,f6014]) ).
fof(f9860,plain,
m1_filter_2(k15_filter_2(sK33,sK34),k1_lattice2(sK33)),
inference(forward_subsumption_resolution,[],[f9859,f6013]) ).
fof(f9861,plain,
m1_filter_2(k7_filter_2(sK33,sK34),k1_lattice2(sK33)),
inference(forward_demodulation,[],[f9860,f9692]) ).
fof(f9862,plain,
( m2_lattice4(k7_filter_2(sK33,sK34),k1_lattice2(sK33))
| v3_struct_0(k1_lattice2(sK33))
| ~ v10_lattices(k1_lattice2(sK33))
| ~ l3_lattices(k1_lattice2(sK33)) ),
inference(resolution,[],[f9861,f5675]) ).
fof(f9863,plain,
( k8_filter_0(k1_lattice2(sK33),k7_filter_2(sK33,sK34)) = k23_filter_2(k1_lattice2(sK33),k7_filter_2(sK33,sK34))
| v3_struct_0(k1_lattice2(sK33))
| ~ v10_lattices(k1_lattice2(sK33))
| ~ l3_lattices(k1_lattice2(sK33)) ),
inference(resolution,[],[f9861,f6002]) ).
fof(f9866,plain,
( k8_filter_0(k1_lattice2(sK33),k7_filter_2(sK33,sK34)) = k23_filter_2(k1_lattice2(sK33),k7_filter_2(sK33,sK34))
| v3_struct_0(k1_lattice2(sK33))
| ~ v10_lattices(k1_lattice2(sK33)) ),
inference(forward_subsumption_resolution,[],[f9863,f9738]) ).
fof(f9867,plain,
( m2_lattice4(k7_filter_2(sK33,sK34),k1_lattice2(sK33))
| v3_struct_0(k1_lattice2(sK33))
| ~ v10_lattices(k1_lattice2(sK33)) ),
inference(forward_subsumption_resolution,[],[f9862,f9738]) ).
fof(f9873,definition,
( spl421_35
<=> k8_filter_0(k1_lattice2(sK33),k7_filter_2(sK33,sK34)) = k23_filter_2(k1_lattice2(sK33),k7_filter_2(sK33,sK34)) ),
introduced(definition,[new_symbols(definition,[spl421_35])],[avatar_definition]) ).
fof(f9874,plain,
( k8_filter_0(k1_lattice2(sK33),k7_filter_2(sK33,sK34)) = k23_filter_2(k1_lattice2(sK33),k7_filter_2(sK33,sK34))
| ~ spl421_35 ),
inference(avatar_component_clause,[],[f9873]) ).
fof(f9875,plain,
( ~ spl421_9
| spl421_10
| spl421_35 ),
inference(avatar_split_clause,[],[f9866,f9873,f9706,f9703]) ).
fof(f9877,definition,
( spl421_36
<=> m2_lattice4(k7_filter_2(sK33,sK34),k1_lattice2(sK33)) ),
introduced(definition,[new_symbols(definition,[spl421_36])],[avatar_definition]) ).
fof(f9878,plain,
( m2_lattice4(k7_filter_2(sK33,sK34),k1_lattice2(sK33))
| ~ spl421_36 ),
inference(avatar_component_clause,[],[f9877]) ).
fof(f9879,plain,
( ~ spl421_9
| spl421_10
| spl421_36 ),
inference(avatar_split_clause,[],[f9867,f9877,f9706,f9703]) ).
fof(f9949,plain,
! [X0] :
( ~ m1_filter_2(X0,k1_lattice2(sK33))
| v3_struct_0(sK33)
| ~ v10_lattices(sK33)
| m2_filter_2(X0,sK33) ),
inference(resolution,[],[f5792,f6013]) ).
fof(f9956,plain,
! [X0] :
( ~ m1_filter_2(X0,k1_lattice2(sK33))
| ~ v10_lattices(sK33)
| m2_filter_2(X0,sK33) ),
inference(forward_subsumption_resolution,[],[f9949,f6015]) ).
fof(f9957,plain,
! [X0] :
( ~ m1_filter_2(X0,k1_lattice2(sK33))
| m2_filter_2(X0,sK33) ),
inference(forward_subsumption_resolution,[],[f9956,f6014]) ).
fof(f9959,plain,
m2_filter_2(k7_filter_2(sK33,sK34),sK33),
inference(resolution,[],[f9957,f9861]) ).
fof(f9963,plain,
m2_lattice4(k7_filter_2(sK33,sK34),sK33),
inference(resolution,[],[f9959,f9668]) ).
fof(f10026,plain,
! [X0] :
( ~ m2_nat_lat(k23_filter_2(k1_lattice2(sK33),X0),k1_lattice2(sK33))
| v1_xboole_0(X0)
| ~ m2_lattice4(X0,k1_lattice2(sK33))
| v3_struct_0(k1_lattice2(sK33))
| ~ v10_lattices(k1_lattice2(sK33))
| k1_realset1(u2_lattices(k1_lattice2(sK33)),X0) = sK31(k1_lattice2(sK33),X0,k23_filter_2(k1_lattice2(sK33),X0)) ),
inference(resolution,[],[f9032,f9738]) ).
fof(f10027,plain,
( ! [X0] :
( v1_xboole_0(X0)
| ~ m2_lattice4(X0,k1_lattice2(sK33))
| v3_struct_0(k1_lattice2(sK33))
| ~ v10_lattices(k1_lattice2(sK33))
| k1_realset1(u2_lattices(k1_lattice2(sK33)),X0) = sK31(k1_lattice2(sK33),X0,k23_filter_2(k1_lattice2(sK33),X0)) )
| ~ spl421_25 ),
inference(forward_subsumption_resolution,[],[f10026,f9812]) ).
fof(f10030,definition,
( spl421_54
<=> ! [X0] :
( v1_xboole_0(X0)
| k1_realset1(u2_lattices(k1_lattice2(sK33)),X0) = sK31(k1_lattice2(sK33),X0,k23_filter_2(k1_lattice2(sK33),X0))
| ~ m2_lattice4(X0,k1_lattice2(sK33)) ) ),
introduced(definition,[new_symbols(definition,[spl421_54])],[avatar_definition]) ).
fof(f10031,plain,
( ! [X0] :
( ~ m2_lattice4(X0,k1_lattice2(sK33))
| k1_realset1(u2_lattices(k1_lattice2(sK33)),X0) = sK31(k1_lattice2(sK33),X0,k23_filter_2(k1_lattice2(sK33),X0))
| v1_xboole_0(X0) )
| ~ spl421_54 ),
inference(avatar_component_clause,[],[f10030]) ).
fof(f10032,plain,
( ~ spl421_9
| spl421_10
| spl421_54
| ~ spl421_25 ),
inference(avatar_split_clause,[],[f10027,f9811,f10030,f9706,f9703]) ).
fof(f10046,plain,
( v3_struct_0(sK33)
| ~ v10_lattices(sK33)
| u1_struct_0(sK33) = k17_filter_2(sK33) ),
inference(resolution,[],[f5818,f6013]) ).
fof(f10052,plain,
( ~ v10_lattices(sK33)
| u1_struct_0(sK33) = k17_filter_2(sK33) ),
inference(forward_subsumption_resolution,[],[f10046,f6015]) ).
fof(f10053,plain,
u1_struct_0(sK33) = k17_filter_2(sK33),
inference(forward_subsumption_resolution,[],[f10052,f6014]) ).
fof(f10056,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k17_filter_2(sK33)))
| k7_filter_2(sK33,X0) = X0
| v3_struct_0(sK33)
| ~ v10_lattices(sK33)
| ~ l3_lattices(sK33) ),
inference(superposition,[],[f5793,f10053]) ).
fof(f10059,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k17_filter_2(sK33)))
| k7_filter_2(sK33,X0) = X0
| ~ v10_lattices(sK33)
| ~ l3_lattices(sK33) ),
inference(forward_subsumption_resolution,[],[f10056,f6015]) ).
fof(f10062,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k17_filter_2(sK33)))
| k7_filter_2(sK33,X0) = X0
| ~ l3_lattices(sK33) ),
inference(forward_subsumption_resolution,[],[f10059,f6014]) ).
fof(f10065,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k17_filter_2(sK33)))
| k7_filter_2(sK33,X0) = X0 ),
inference(forward_subsumption_resolution,[],[f10062,f6013]) ).
fof(f10082,plain,
! [X0] :
( ~ m2_lattice4(X0,sK33)
| v3_struct_0(sK33)
| ~ v10_lattices(sK33)
| m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK33))) ),
inference(resolution,[],[f6039,f6013]) ).
fof(f10085,plain,
! [X0] :
( ~ m2_lattice4(X0,sK33)
| ~ v10_lattices(sK33)
| m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK33))) ),
inference(forward_subsumption_resolution,[],[f10082,f6015]) ).
fof(f10090,plain,
! [X0] :
( ~ m2_lattice4(X0,sK33)
| m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK33))) ),
inference(forward_subsumption_resolution,[],[f10085,f6014]) ).
fof(f10091,plain,
! [X0] :
( m1_subset_1(X0,k1_zfmisc_1(k17_filter_2(sK33)))
| ~ m2_lattice4(X0,sK33) ),
inference(forward_demodulation,[],[f10090,f10053]) ).
fof(f10092,plain,
! [X0] :
( ~ m2_lattice4(X0,sK33)
| k7_filter_2(sK33,X0) = X0 ),
inference(resolution,[],[f10091,f10065]) ).
fof(f10093,plain,
sK34 = k7_filter_2(sK33,sK34),
inference(resolution,[],[f10092,f9669]) ).
fof(f10105,plain,
! [X0] :
( ~ m2_nat_lat(k23_filter_2(k1_lattice2(sK33),X0),k1_lattice2(sK33))
| v1_xboole_0(X0)
| ~ m2_lattice4(X0,k1_lattice2(sK33))
| v3_struct_0(k1_lattice2(sK33))
| ~ v10_lattices(k1_lattice2(sK33))
| k1_realset1(u1_lattices(k1_lattice2(sK33)),X0) = sK32(k1_lattice2(sK33),X0,k23_filter_2(k1_lattice2(sK33),X0)) ),
inference(resolution,[],[f9033,f9738]) ).
fof(f10106,plain,
( ! [X0] :
( v1_xboole_0(X0)
| ~ m2_lattice4(X0,k1_lattice2(sK33))
| v3_struct_0(k1_lattice2(sK33))
| ~ v10_lattices(k1_lattice2(sK33))
| k1_realset1(u1_lattices(k1_lattice2(sK33)),X0) = sK32(k1_lattice2(sK33),X0,k23_filter_2(k1_lattice2(sK33),X0)) )
| ~ spl421_25 ),
inference(forward_subsumption_resolution,[],[f10105,f9812]) ).
fof(f10109,definition,
( spl421_60
<=> ! [X0] :
( v1_xboole_0(X0)
| k1_realset1(u1_lattices(k1_lattice2(sK33)),X0) = sK32(k1_lattice2(sK33),X0,k23_filter_2(k1_lattice2(sK33),X0))
| ~ m2_lattice4(X0,k1_lattice2(sK33)) ) ),
introduced(definition,[new_symbols(definition,[spl421_60])],[avatar_definition]) ).
fof(f10110,plain,
( ! [X0] :
( ~ m2_lattice4(X0,k1_lattice2(sK33))
| k1_realset1(u1_lattices(k1_lattice2(sK33)),X0) = sK32(k1_lattice2(sK33),X0,k23_filter_2(k1_lattice2(sK33),X0))
| v1_xboole_0(X0) )
| ~ spl421_60 ),
inference(avatar_component_clause,[],[f10109]) ).
fof(f10111,plain,
( ~ spl421_9
| spl421_10
| spl421_60
| ~ spl421_25 ),
inference(avatar_split_clause,[],[f10106,f9811,f10109,f9706,f9703]) ).
fof(f10278,plain,
( v3_struct_0(sK33)
| u1_lattices(sK33) = u2_lattices(k1_lattice2(sK33)) ),
inference(resolution,[],[f6432,f6013]) ).
fof(f10284,plain,
u1_lattices(sK33) = u2_lattices(k1_lattice2(sK33)),
inference(forward_subsumption_resolution,[],[f10278,f6015]) ).
fof(f10293,plain,
( v3_struct_0(sK33)
| u2_lattices(sK33) = u1_lattices(k1_lattice2(sK33)) ),
inference(resolution,[],[f6433,f6013]) ).
fof(f10296,plain,
u2_lattices(sK33) = u1_lattices(k1_lattice2(sK33)),
inference(forward_subsumption_resolution,[],[f10293,f6015]) ).
fof(f10705,plain,
! [X0] :
( ~ m2_nat_lat(X0,sK33)
| v3_struct_0(sK33)
| ~ v10_lattices(sK33)
| v10_lattices(X0) ),
inference(resolution,[],[f6153,f6013]) ).
fof(f10711,plain,
! [X0] :
( ~ m2_nat_lat(X0,sK33)
| ~ v10_lattices(sK33)
| v10_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f10705,f6015]) ).
fof(f10712,plain,
! [X0] :
( ~ m2_nat_lat(X0,sK33)
| v10_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f10711,f6014]) ).
fof(f10713,plain,
! [X0] :
( v10_lattices(k23_filter_2(sK33,X0))
| v1_xboole_0(X0)
| ~ m2_lattice4(X0,sK33) ),
inference(resolution,[],[f10712,f9718]) ).
fof(f10792,plain,
! [X0] :
( ~ m2_nat_lat(X0,sK33)
| v3_struct_0(sK33)
| ~ v10_lattices(sK33)
| l3_lattices(X0) ),
inference(resolution,[],[f6152,f6013]) ).
fof(f10798,plain,
! [X0] :
( ~ m2_nat_lat(X0,sK33)
| ~ v10_lattices(sK33)
| l3_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f10792,f6015]) ).
fof(f10799,plain,
! [X0] :
( ~ m2_nat_lat(X0,sK33)
| l3_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f10798,f6014]) ).
fof(f10800,plain,
! [X0] :
( ~ m2_lattice4(X0,sK33)
| v1_xboole_0(X0)
| l3_lattices(k23_filter_2(sK33,X0)) ),
inference(resolution,[],[f10799,f9718]) ).
fof(f10803,plain,
( v1_xboole_0(k7_filter_2(sK33,sK34))
| l3_lattices(k23_filter_2(sK33,k7_filter_2(sK33,sK34))) ),
inference(resolution,[],[f10800,f9963]) ).
fof(f10806,plain,
( v1_xboole_0(sK34)
| l3_lattices(k23_filter_2(sK33,k7_filter_2(sK33,sK34))) ),
inference(forward_demodulation,[],[f10803,f10093]) ).
fof(f10812,plain,
( l3_lattices(k23_filter_2(sK33,sK34))
| v1_xboole_0(sK34) ),
inference(forward_demodulation,[],[f10806,f10093]) ).
fof(f10814,plain,
( l3_lattices(k23_filter_2(sK33,sK34))
| ~ spl421_16 ),
inference(avatar_component_clause,[],[f9766]) ).
fof(f10816,plain,
( spl421_6
| spl421_16 ),
inference(avatar_split_clause,[],[f10812,f9766,f9678]) ).
fof(f10817,plain,
( v1_xboole_0(sK34)
| ~ m2_lattice4(sK34,sK33)
| spl421_17 ),
inference(resolution,[],[f9770,f10713]) ).
fof(f10820,plain,
( v1_xboole_0(sK34)
| spl421_17 ),
inference(forward_subsumption_resolution,[],[f10817,f9669]) ).
fof(f10822,plain,
( spl421_6
| spl421_17 ),
inference(avatar_split_clause,[],[f10820,f9769,f9678]) ).
fof(f10866,plain,
( l3_lattices(k1_lattice2(k23_filter_2(sK33,sK34)))
| ~ spl421_16 ),
inference(resolution,[],[f10814,f6170]) ).
fof(f10874,plain,
( v3_struct_0(sK33)
| ~ v10_lattices(sK33)
| ~ l3_lattices(sK33)
| v1_xboole_0(sK34)
| ~ m2_lattice4(sK34,sK33)
| ~ spl421_18 ),
inference(resolution,[],[f9773,f6001]) ).
fof(f10876,plain,
( ~ v10_lattices(sK33)
| ~ l3_lattices(sK33)
| v1_xboole_0(sK34)
| ~ m2_lattice4(sK34,sK33)
| ~ spl421_18 ),
inference(forward_subsumption_resolution,[],[f10874,f6015]) ).
fof(f10877,plain,
( ~ l3_lattices(sK33)
| v1_xboole_0(sK34)
| ~ m2_lattice4(sK34,sK33)
| ~ spl421_18 ),
inference(forward_subsumption_resolution,[],[f10876,f6014]) ).
fof(f10878,plain,
( v1_xboole_0(sK34)
| ~ m2_lattice4(sK34,sK33)
| ~ spl421_18 ),
inference(forward_subsumption_resolution,[],[f10877,f6013]) ).
fof(f10879,plain,
( v1_xboole_0(sK34)
| ~ spl421_18 ),
inference(forward_subsumption_resolution,[],[f10878,f9669]) ).
fof(f10880,plain,
( spl421_6
| ~ spl421_18 ),
inference(avatar_split_clause,[],[f10879,f9772,f9678]) ).
fof(f11167,definition,
( spl421_181
<=> v10_lattices(k1_lattice2(k23_filter_2(sK33,sK34))) ),
introduced(definition,[new_symbols(definition,[spl421_181])],[avatar_definition]) ).
fof(f11168,plain,
( ~ v10_lattices(k1_lattice2(k23_filter_2(sK33,sK34)))
| spl421_181 ),
inference(avatar_component_clause,[],[f11167]) ).
fof(f11170,definition,
( spl421_182
<=> v3_struct_0(k1_lattice2(k23_filter_2(sK33,sK34))) ),
introduced(definition,[new_symbols(definition,[spl421_182])],[avatar_definition]) ).
fof(f11171,plain,
( v3_struct_0(k1_lattice2(k23_filter_2(sK33,sK34)))
| ~ spl421_182 ),
inference(avatar_component_clause,[],[f11170]) ).
fof(f11191,plain,
( v3_struct_0(k23_filter_2(sK33,sK34))
| ~ v10_lattices(k23_filter_2(sK33,sK34))
| ~ l3_lattices(k23_filter_2(sK33,sK34))
| spl421_181 ),
inference(resolution,[],[f11168,f6173]) ).
fof(f11192,plain,
( v3_struct_0(k23_filter_2(sK33,sK34))
| ~ v10_lattices(k23_filter_2(sK33,sK34))
| ~ spl421_16
| spl421_181 ),
inference(forward_subsumption_resolution,[],[f11191,f10814]) ).
fof(f11193,plain,
( ~ spl421_17
| spl421_18
| ~ spl421_16
| spl421_181 ),
inference(avatar_split_clause,[],[f11192,f11167,f9766,f9772,f9769]) ).
fof(f11201,plain,
( v3_struct_0(k23_filter_2(sK33,sK34))
| ~ l3_lattices(k23_filter_2(sK33,sK34))
| ~ spl421_182 ),
inference(resolution,[],[f11171,f6183]) ).
fof(f11203,plain,
( v3_struct_0(k23_filter_2(sK33,sK34))
| ~ spl421_16
| ~ spl421_182 ),
inference(forward_subsumption_resolution,[],[f11201,f10814]) ).
fof(f11204,plain,
( spl421_18
| ~ spl421_16
| ~ spl421_182 ),
inference(avatar_split_clause,[],[f11203,f11170,f9766,f9772]) ).
fof(f11565,plain,
! [X0,X1] :
( v3_struct_0(k23_filter_2(X0,X1))
| k23_filter_2(X0,X1) = k1_lattice2(k1_lattice2(k23_filter_2(X0,X1)))
| ~ l3_lattices(k23_filter_2(X0,X1))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0) ),
inference(resolution,[],[f6172,f6000]) ).
fof(f11566,plain,
! [X0,X1] :
( ~ l3_lattices(X0)
| ~ l3_lattices(k23_filter_2(X0,X1))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| k23_filter_2(X0,X1) = k1_lattice2(k1_lattice2(k23_filter_2(X0,X1)))
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0) ),
inference(forward_subsumption_resolution,[],[f11565,f6001]) ).
fof(f11567,plain,
! [X0] :
( ~ l3_lattices(k23_filter_2(sK33,X0))
| v3_struct_0(sK33)
| ~ v10_lattices(sK33)
| k23_filter_2(sK33,X0) = k1_lattice2(k1_lattice2(k23_filter_2(sK33,X0)))
| v1_xboole_0(X0)
| ~ m2_lattice4(X0,sK33) ),
inference(resolution,[],[f11566,f6013]) ).
fof(f11579,plain,
! [X0] :
( v3_struct_0(sK33)
| ~ v10_lattices(sK33)
| k23_filter_2(sK33,X0) = k1_lattice2(k1_lattice2(k23_filter_2(sK33,X0)))
| v1_xboole_0(X0)
| ~ m2_lattice4(X0,sK33) ),
inference(forward_subsumption_resolution,[],[f11567,f10800]) ).
fof(f11580,plain,
! [X0] :
( ~ v10_lattices(sK33)
| k23_filter_2(sK33,X0) = k1_lattice2(k1_lattice2(k23_filter_2(sK33,X0)))
| v1_xboole_0(X0)
| ~ m2_lattice4(X0,sK33) ),
inference(forward_subsumption_resolution,[],[f11579,f6015]) ).
fof(f11581,plain,
! [X0] :
( ~ m2_lattice4(X0,sK33)
| v1_xboole_0(X0)
| k23_filter_2(sK33,X0) = k1_lattice2(k1_lattice2(k23_filter_2(sK33,X0))) ),
inference(forward_subsumption_resolution,[],[f11580,f6014]) ).
fof(f11583,plain,
( v1_xboole_0(k7_filter_2(sK33,sK34))
| k23_filter_2(sK33,k7_filter_2(sK33,sK34)) = k1_lattice2(k1_lattice2(k23_filter_2(sK33,k7_filter_2(sK33,sK34)))) ),
inference(resolution,[],[f11581,f9963]) ).
fof(f11586,definition,
( spl421_244
<=> k23_filter_2(sK33,sK34) = k1_lattice2(k1_lattice2(k23_filter_2(sK33,sK34))) ),
introduced(definition,[new_symbols(definition,[spl421_244])],[avatar_definition]) ).
fof(f11587,plain,
( k23_filter_2(sK33,sK34) = k1_lattice2(k1_lattice2(k23_filter_2(sK33,sK34)))
| ~ spl421_244 ),
inference(avatar_component_clause,[],[f11586]) ).
fof(f11589,plain,
( v1_xboole_0(sK34)
| k23_filter_2(sK33,k7_filter_2(sK33,sK34)) = k1_lattice2(k1_lattice2(k23_filter_2(sK33,k7_filter_2(sK33,sK34)))) ),
inference(forward_demodulation,[],[f11583,f10093]) ).
fof(f11594,plain,
( k23_filter_2(sK33,sK34) = k1_lattice2(k1_lattice2(k23_filter_2(sK33,sK34)))
| v1_xboole_0(sK34) ),
inference(forward_demodulation,[],[f11589,f10093]) ).
fof(f11595,plain,
( spl421_6
| spl421_244 ),
inference(avatar_split_clause,[],[f11594,f11586,f9678]) ).
fof(f11603,plain,
( v13_lattices(k23_filter_2(sK33,sK34))
| ~ v14_lattices(k1_lattice2(k23_filter_2(sK33,sK34)))
| v3_struct_0(k1_lattice2(k23_filter_2(sK33,sK34)))
| ~ v10_lattices(k1_lattice2(k23_filter_2(sK33,sK34)))
| ~ l3_lattices(k1_lattice2(k23_filter_2(sK33,sK34)))
| ~ spl421_244 ),
inference(superposition,[],[f6515,f11587]) ).
fof(f11609,plain,
( ~ v14_lattices(k1_lattice2(k23_filter_2(sK33,sK34)))
| v3_struct_0(k1_lattice2(k23_filter_2(sK33,sK34)))
| ~ v10_lattices(k1_lattice2(k23_filter_2(sK33,sK34)))
| ~ l3_lattices(k1_lattice2(k23_filter_2(sK33,sK34)))
| ~ spl421_244 ),
inference(forward_subsumption_resolution,[],[f11603,f6018]) ).
fof(f11627,plain,
( ~ v14_lattices(k1_lattice2(k23_filter_2(sK33,sK34)))
| v3_struct_0(k1_lattice2(k23_filter_2(sK33,sK34)))
| ~ v10_lattices(k1_lattice2(k23_filter_2(sK33,sK34)))
| ~ spl421_16
| ~ spl421_244 ),
inference(forward_subsumption_resolution,[],[f11609,f10866]) ).
fof(f11650,definition,
( spl421_252
<=> v14_lattices(k1_lattice2(k23_filter_2(sK33,sK34))) ),
introduced(definition,[new_symbols(definition,[spl421_252])],[avatar_definition]) ).
fof(f11651,plain,
( ~ v14_lattices(k1_lattice2(k23_filter_2(sK33,sK34)))
| spl421_252 ),
inference(avatar_component_clause,[],[f11650]) ).
fof(f11652,plain,
( ~ spl421_181
| spl421_182
| ~ spl421_252
| ~ spl421_16
| ~ spl421_244 ),
inference(avatar_split_clause,[],[f11627,f11586,f9766,f11650,f11170,f11167]) ).
fof(f14358,plain,
( k1_realset1(u1_lattices(k1_lattice2(sK33)),k7_filter_2(sK33,sK34)) = sK32(k1_lattice2(sK33),k7_filter_2(sK33,sK34),k23_filter_2(k1_lattice2(sK33),k7_filter_2(sK33,sK34)))
| v1_xboole_0(k7_filter_2(sK33,sK34))
| ~ spl421_36
| ~ spl421_60 ),
inference(resolution,[],[f10110,f9878]) ).
fof(f14368,plain,
( k1_realset1(u1_lattices(k1_lattice2(sK33)),k7_filter_2(sK33,sK34)) = sK32(k1_lattice2(sK33),k7_filter_2(sK33,sK34),k8_filter_0(k1_lattice2(sK33),k7_filter_2(sK33,sK34)))
| v1_xboole_0(k7_filter_2(sK33,sK34))
| ~ spl421_35
| ~ spl421_36
| ~ spl421_60 ),
inference(forward_demodulation,[],[f14358,f9874]) ).
fof(f14373,plain,
( k1_realset1(u1_lattices(k1_lattice2(sK33)),sK34) = sK32(k1_lattice2(sK33),sK34,k8_filter_0(k1_lattice2(sK33),sK34))
| v1_xboole_0(k7_filter_2(sK33,sK34))
| ~ spl421_35
| ~ spl421_36
| ~ spl421_60 ),
inference(forward_demodulation,[],[f14368,f10093]) ).
fof(f14376,definition,
( spl421_536
<=> k1_realset1(u2_lattices(sK33),sK34) = sK32(k1_lattice2(sK33),sK34,k8_filter_0(k1_lattice2(sK33),sK34)) ),
introduced(definition,[new_symbols(definition,[spl421_536])],[avatar_definition]) ).
fof(f14377,plain,
( k1_realset1(u2_lattices(sK33),sK34) = sK32(k1_lattice2(sK33),sK34,k8_filter_0(k1_lattice2(sK33),sK34))
| ~ spl421_536 ),
inference(avatar_component_clause,[],[f14376]) ).
fof(f14381,plain,
( k1_realset1(u2_lattices(sK33),sK34) = sK32(k1_lattice2(sK33),sK34,k8_filter_0(k1_lattice2(sK33),sK34))
| v1_xboole_0(k7_filter_2(sK33,sK34))
| ~ spl421_35
| ~ spl421_36
| ~ spl421_60 ),
inference(forward_demodulation,[],[f14373,f10296]) ).
fof(f14388,plain,
( v1_xboole_0(sK34)
| k1_realset1(u2_lattices(sK33),sK34) = sK32(k1_lattice2(sK33),sK34,k8_filter_0(k1_lattice2(sK33),sK34))
| ~ spl421_35
| ~ spl421_36
| ~ spl421_60 ),
inference(forward_demodulation,[],[f14381,f10093]) ).
fof(f14390,plain,
( spl421_536
| spl421_6
| ~ spl421_35
| ~ spl421_36
| ~ spl421_60 ),
inference(avatar_split_clause,[],[f14388,f10109,f9877,f9873,f9678,f14376]) ).
fof(f15267,plain,
( k1_realset1(u2_lattices(k1_lattice2(sK33)),k7_filter_2(sK33,sK34)) = sK31(k1_lattice2(sK33),k7_filter_2(sK33,sK34),k23_filter_2(k1_lattice2(sK33),k7_filter_2(sK33,sK34)))
| v1_xboole_0(k7_filter_2(sK33,sK34))
| ~ spl421_36
| ~ spl421_54 ),
inference(resolution,[],[f10031,f9878]) ).
fof(f15277,plain,
( k1_realset1(u2_lattices(k1_lattice2(sK33)),k7_filter_2(sK33,sK34)) = sK31(k1_lattice2(sK33),k7_filter_2(sK33,sK34),k8_filter_0(k1_lattice2(sK33),k7_filter_2(sK33,sK34)))
| v1_xboole_0(k7_filter_2(sK33,sK34))
| ~ spl421_35
| ~ spl421_36
| ~ spl421_54 ),
inference(forward_demodulation,[],[f15267,f9874]) ).
fof(f15282,plain,
( k1_realset1(u2_lattices(k1_lattice2(sK33)),sK34) = sK31(k1_lattice2(sK33),sK34,k8_filter_0(k1_lattice2(sK33),sK34))
| v1_xboole_0(k7_filter_2(sK33,sK34))
| ~ spl421_35
| ~ spl421_36
| ~ spl421_54 ),
inference(forward_demodulation,[],[f15277,f10093]) ).
fof(f15285,definition,
( spl421_564
<=> k1_realset1(u1_lattices(sK33),sK34) = sK31(k1_lattice2(sK33),sK34,k8_filter_0(k1_lattice2(sK33),sK34)) ),
introduced(definition,[new_symbols(definition,[spl421_564])],[avatar_definition]) ).
fof(f15286,plain,
( k1_realset1(u1_lattices(sK33),sK34) = sK31(k1_lattice2(sK33),sK34,k8_filter_0(k1_lattice2(sK33),sK34))
| ~ spl421_564 ),
inference(avatar_component_clause,[],[f15285]) ).
fof(f15290,plain,
( k1_realset1(u1_lattices(sK33),sK34) = sK31(k1_lattice2(sK33),sK34,k8_filter_0(k1_lattice2(sK33),sK34))
| v1_xboole_0(k7_filter_2(sK33,sK34))
| ~ spl421_35
| ~ spl421_36
| ~ spl421_54 ),
inference(forward_demodulation,[],[f15282,f10284]) ).
fof(f15297,plain,
( v1_xboole_0(sK34)
| k1_realset1(u1_lattices(sK33),sK34) = sK31(k1_lattice2(sK33),sK34,k8_filter_0(k1_lattice2(sK33),sK34))
| ~ spl421_35
| ~ spl421_36
| ~ spl421_54 ),
inference(forward_demodulation,[],[f15290,f10093]) ).
fof(f15299,plain,
( spl421_564
| spl421_6
| ~ spl421_35
| ~ spl421_36
| ~ spl421_54 ),
inference(avatar_split_clause,[],[f15297,f10030,f9877,f9873,f9678,f15285]) ).
fof(f16611,plain,
! [X0,X1] :
( v14_lattices(k8_filter_0(k1_lattice2(X0),X1))
| ~ m1_filter_0(X1,k1_lattice2(X0))
| v3_struct_0(k1_lattice2(X0))
| ~ v10_lattices(k1_lattice2(X0))
| ~ l3_lattices(k1_lattice2(X0))
| ~ v13_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(resolution,[],[f6804,f6517]) ).
fof(f16612,plain,
! [X0,X1] :
( v14_lattices(k8_filter_0(k1_lattice2(X0),X1))
| ~ m1_filter_0(X1,k1_lattice2(X0))
| ~ v10_lattices(k1_lattice2(X0))
| ~ l3_lattices(k1_lattice2(X0))
| ~ v13_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f16611,f6183]) ).
fof(f16613,plain,
! [X0,X1] :
( v14_lattices(k8_filter_0(k1_lattice2(X0),X1))
| ~ m1_filter_0(X1,k1_lattice2(X0))
| ~ l3_lattices(k1_lattice2(X0))
| ~ v13_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f16612,f6173]) ).
fof(f16614,plain,
! [X0,X1] :
( v14_lattices(k8_filter_0(k1_lattice2(X0),X1))
| ~ m1_filter_0(X1,k1_lattice2(X0))
| ~ v13_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f16613,f6170]) ).
fof(f22319,plain,
( m2_nat_lat(k23_filter_2(k1_lattice2(sK33),k7_filter_2(sK33,sK34)),k1_lattice2(sK33))
| v1_xboole_0(k7_filter_2(sK33,sK34))
| ~ spl421_25
| ~ spl421_36 ),
inference(resolution,[],[f9812,f9878]) ).
fof(f22328,plain,
( m2_nat_lat(k8_filter_0(k1_lattice2(sK33),k7_filter_2(sK33,sK34)),k1_lattice2(sK33))
| v1_xboole_0(k7_filter_2(sK33,sK34))
| ~ spl421_25
| ~ spl421_35
| ~ spl421_36 ),
inference(forward_demodulation,[],[f22319,f9874]) ).
fof(f22347,plain,
( k8_filter_0(k1_lattice2(sK33),sK34) = g3_lattices(sK34,sK31(k1_lattice2(sK33),sK34,k8_filter_0(k1_lattice2(sK33),sK34)),k1_realset1(u2_lattices(sK33),sK34))
| ~ spl421_31
| ~ spl421_536 ),
inference(forward_demodulation,[],[f9848,f14377]) ).
fof(f22354,plain,
( m2_nat_lat(k8_filter_0(k1_lattice2(sK33),sK34),k1_lattice2(sK33))
| v1_xboole_0(k7_filter_2(sK33,sK34))
| ~ spl421_25
| ~ spl421_35
| ~ spl421_36 ),
inference(forward_demodulation,[],[f22328,f10093]) ).
fof(f22357,plain,
( k8_filter_0(k1_lattice2(sK33),sK34) = g3_lattices(sK34,k1_realset1(u1_lattices(sK33),sK34),k1_realset1(u2_lattices(sK33),sK34))
| ~ spl421_31
| ~ spl421_536
| ~ spl421_564 ),
inference(forward_demodulation,[],[f22347,f15286]) ).
fof(f22362,plain,
( v1_xboole_0(sK34)
| m2_nat_lat(k8_filter_0(k1_lattice2(sK33),sK34),k1_lattice2(sK33))
| ~ spl421_25
| ~ spl421_35
| ~ spl421_36 ),
inference(forward_demodulation,[],[f22354,f10093]) ).
fof(f22367,plain,
( spl421_32
| spl421_6
| ~ spl421_25
| ~ spl421_35
| ~ spl421_36 ),
inference(avatar_split_clause,[],[f22362,f9877,f9873,f9811,f9678,f9850]) ).
fof(f23071,plain,
( k1_lattice2(k23_filter_2(sK33,sK34)) = g3_lattices(u1_struct_0(k23_filter_2(sK33,sK34)),u1_lattices(k23_filter_2(sK33,sK34)),u2_lattices(k23_filter_2(sK33,sK34)))
| ~ spl421_16 ),
inference(resolution,[],[f6428,f10814]) ).
fof(f23078,plain,
( k1_lattice2(k23_filter_2(sK33,sK34)) = g3_lattices(u1_struct_0(k23_filter_2(sK33,sK34)),u1_lattices(k23_filter_2(sK33,sK34)),k1_realset1(u2_lattices(sK33),sK34))
| ~ spl421_5
| ~ spl421_16 ),
inference(forward_demodulation,[],[f23071,f9676]) ).
fof(f23088,plain,
( k1_lattice2(k23_filter_2(sK33,sK34)) = g3_lattices(u1_struct_0(k23_filter_2(sK33,sK34)),k1_realset1(u1_lattices(sK33),sK34),k1_realset1(u2_lattices(sK33),sK34))
| ~ spl421_5
| ~ spl421_7
| ~ spl421_16 ),
inference(forward_demodulation,[],[f23078,f9687]) ).
fof(f23095,plain,
( k1_lattice2(k23_filter_2(sK33,sK34)) = g3_lattices(sK34,k1_realset1(u1_lattices(sK33),sK34),k1_realset1(u2_lattices(sK33),sK34))
| ~ spl421_5
| ~ spl421_7
| ~ spl421_13
| ~ spl421_16 ),
inference(forward_demodulation,[],[f23088,f9735]) ).
fof(f23114,plain,
( k8_filter_0(k1_lattice2(sK33),sK34) = k1_lattice2(k23_filter_2(sK33,sK34))
| ~ spl421_5
| ~ spl421_7
| ~ spl421_13
| ~ spl421_16
| ~ spl421_31
| ~ spl421_536
| ~ spl421_564 ),
inference(superposition,[],[f22357,f23095]) ).
fof(f23124,plain,
( v14_lattices(k1_lattice2(k23_filter_2(sK33,sK34)))
| ~ m1_filter_0(sK34,k1_lattice2(sK33))
| ~ v13_lattices(sK33)
| v3_struct_0(sK33)
| ~ v10_lattices(sK33)
| ~ l3_lattices(sK33)
| ~ spl421_5
| ~ spl421_7
| ~ spl421_13
| ~ spl421_16
| ~ spl421_31
| ~ spl421_536
| ~ spl421_564 ),
inference(superposition,[],[f16614,f23114]) ).
fof(f23131,plain,
( ~ m1_filter_0(sK34,k1_lattice2(sK33))
| ~ v13_lattices(sK33)
| v3_struct_0(sK33)
| ~ v10_lattices(sK33)
| ~ l3_lattices(sK33)
| ~ spl421_5
| ~ spl421_7
| ~ spl421_13
| ~ spl421_16
| ~ spl421_31
| spl421_252
| ~ spl421_536
| ~ spl421_564 ),
inference(forward_subsumption_resolution,[],[f23124,f11651]) ).
fof(f23133,plain,
( ~ v13_lattices(sK33)
| v3_struct_0(sK33)
| ~ v10_lattices(sK33)
| ~ l3_lattices(sK33)
| ~ spl421_5
| ~ spl421_7
| ~ spl421_11
| ~ spl421_13
| ~ spl421_16
| ~ spl421_31
| spl421_252
| ~ spl421_536
| ~ spl421_564 ),
inference(forward_subsumption_resolution,[],[f23131,f9710]) ).
fof(f23138,plain,
( v3_struct_0(sK33)
| ~ v10_lattices(sK33)
| ~ l3_lattices(sK33)
| ~ spl421_5
| ~ spl421_7
| ~ spl421_11
| ~ spl421_13
| ~ spl421_16
| ~ spl421_31
| spl421_252
| ~ spl421_536
| ~ spl421_564 ),
inference(forward_subsumption_resolution,[],[f23133,f6017]) ).
fof(f23139,plain,
( ~ v10_lattices(sK33)
| ~ l3_lattices(sK33)
| ~ spl421_5
| ~ spl421_7
| ~ spl421_11
| ~ spl421_13
| ~ spl421_16
| ~ spl421_31
| spl421_252
| ~ spl421_536
| ~ spl421_564 ),
inference(forward_subsumption_resolution,[],[f23138,f6015]) ).
fof(f23140,plain,
( ~ l3_lattices(sK33)
| ~ spl421_5
| ~ spl421_7
| ~ spl421_11
| ~ spl421_13
| ~ spl421_16
| ~ spl421_31
| spl421_252
| ~ spl421_536
| ~ spl421_564 ),
inference(forward_subsumption_resolution,[],[f23139,f6014]) ).
fof(f23141,plain,
( $false
| ~ spl421_5
| ~ spl421_7
| ~ spl421_11
| ~ spl421_13
| ~ spl421_16
| ~ spl421_31
| spl421_252
| ~ spl421_536
| ~ spl421_564 ),
inference(forward_subsumption_resolution,[],[f23140,f6013]) ).
fof(f23142,plain,
( ~ spl421_5
| ~ spl421_7
| ~ spl421_11
| ~ spl421_13
| ~ spl421_16
| ~ spl421_31
| spl421_252
| ~ spl421_536
| ~ spl421_564 ),
inference(avatar_contradiction_clause,[],[f23141]) ).
cnf(s3,plain,
( spl421_5
| spl421_6 ),
inference(sat_conversion,[],[f9680]) ).
cnf(s4,plain,
( spl421_6
| spl421_7 ),
inference(sat_conversion,[],[f9688]) ).
cnf(s5,plain,
( ~ spl421_8
| ~ spl421_9
| spl421_10
| spl421_11 ),
inference(sat_conversion,[],[f9711]) ).
cnf(s6,plain,
( ~ spl421_8
| ~ spl421_9
| spl421_10
| spl421_12 ),
inference(sat_conversion,[],[f9715]) ).
cnf(s7,plain,
~ spl421_6,
inference(sat_conversion,[],[f9730]) ).
cnf(s8,plain,
( spl421_6
| spl421_13 ),
inference(sat_conversion,[],[f9736]) ).
cnf(s10,plain,
spl421_8,
inference(sat_conversion,[],[f9741]) ).
cnf(s14,plain,
spl421_9,
inference(sat_conversion,[],[f9787]) ).
cnf(s16,plain,
~ spl421_10,
inference(sat_conversion,[],[f9793]) ).
cnf(s21,plain,
( ~ spl421_9
| spl421_10
| spl421_25 ),
inference(sat_conversion,[],[f9813]) ).
cnf(s25,plain,
( ~ spl421_9
| spl421_10
| spl421_29 ),
inference(sat_conversion,[],[f9830]) ).
cnf(s27,plain,
( spl421_6
| ~ spl421_9
| spl421_10
| ~ spl421_12
| ~ spl421_29
| spl421_31
| ~ spl421_32 ),
inference(sat_conversion,[],[f9852]) ).
cnf(s30,plain,
( ~ spl421_9
| spl421_10
| spl421_35 ),
inference(sat_conversion,[],[f9875]) ).
cnf(s31,plain,
( ~ spl421_9
| spl421_10
| spl421_36 ),
inference(sat_conversion,[],[f9879]) ).
cnf(s48,plain,
( ~ spl421_9
| spl421_10
| ~ spl421_25
| spl421_54 ),
inference(sat_conversion,[],[f10032]) ).
cnf(s54,plain,
( ~ spl421_9
| spl421_10
| ~ spl421_25
| spl421_60 ),
inference(sat_conversion,[],[f10111]) ).
cnf(s135,plain,
( spl421_6
| spl421_16 ),
inference(sat_conversion,[],[f10816]) ).
cnf(s136,plain,
( spl421_6
| spl421_17 ),
inference(sat_conversion,[],[f10822]) ).
cnf(s140,plain,
( spl421_6
| ~ spl421_18 ),
inference(sat_conversion,[],[f10880]) ).
cnf(s198,plain,
( ~ spl421_16
| ~ spl421_17
| spl421_18
| spl421_181 ),
inference(sat_conversion,[],[f11193]) ).
cnf(s199,plain,
( ~ spl421_16
| spl421_18
| ~ spl421_182 ),
inference(sat_conversion,[],[f11204]) ).
cnf(s257,plain,
( spl421_6
| spl421_244 ),
inference(sat_conversion,[],[f11595]) ).
cnf(s265,plain,
( ~ spl421_16
| ~ spl421_181
| spl421_182
| ~ spl421_244
| ~ spl421_252 ),
inference(sat_conversion,[],[f11652]) ).
cnf(s546,plain,
( spl421_6
| ~ spl421_35
| ~ spl421_36
| ~ spl421_60
| spl421_536 ),
inference(sat_conversion,[],[f14390]) ).
cnf(s578,plain,
( spl421_6
| ~ spl421_35
| ~ spl421_36
| ~ spl421_54
| spl421_564 ),
inference(sat_conversion,[],[f15299]) ).
cnf(s1095,plain,
( spl421_6
| ~ spl421_25
| spl421_32
| ~ spl421_35
| ~ spl421_36 ),
inference(sat_conversion,[],[f22367]) ).
cnf(s1151,plain,
( ~ spl421_5
| ~ spl421_7
| ~ spl421_11
| ~ spl421_13
| ~ spl421_16
| ~ spl421_31
| spl421_252
| ~ spl421_536
| ~ spl421_564 ),
inference(sat_conversion,[],[f23142]) ).
cnf(s1437,plain,
spl421_36,
inference(rat,[],[s31,s16,s14]) ).
cnf(s1438,plain,
spl421_35,
inference(rat,[],[s30,s16,s14]) ).
cnf(s1440,plain,
spl421_29,
inference(rat,[],[s25,s16,s14]) ).
cnf(s1444,plain,
spl421_25,
inference(rat,[],[s21,s16,s14]) ).
cnf(s1471,plain,
spl421_60,
inference(rat,[],[s54,s14,s16,s1444]) ).
cnf(s1472,plain,
spl421_54,
inference(rat,[],[s48,s14,s16,s1444]) ).
cnf(s1549,plain,
spl421_32,
inference(rat,[],[s1095,s1437,s1438,s1444,s7]) ).
cnf(s1564,plain,
spl421_564,
inference(rat,[],[s578,s1472,s1438,s1437,s7]) ).
cnf(s1565,plain,
spl421_536,
inference(rat,[],[s546,s1471,s1438,s1437,s7]) ).
cnf(s1570,plain,
spl421_244,
inference(rat,[],[s257,s7]) ).
cnf(s1571,plain,
~ spl421_18,
inference(rat,[],[s140,s7]) ).
cnf(s1572,plain,
spl421_17,
inference(rat,[],[s136,s7]) ).
cnf(s1573,plain,
spl421_16,
inference(rat,[],[s135,s7]) ).
cnf(s1586,plain,
spl421_13,
inference(rat,[],[s8,s7]) ).
cnf(s1602,plain,
~ spl421_182,
inference(rat,[],[s199,s1571,s1573]) ).
cnf(s1603,plain,
spl421_181,
inference(rat,[],[s198,s1572,s1571,s1573]) ).
cnf(s1717,plain,
~ spl421_252,
inference(rat,[],[s265,s1602,s1570,s1573,s1603]) ).
cnf(s1921,plain,
spl421_12,
inference(rat,[],[s6,s16,s14,s10]) ).
cnf(s1924,plain,
spl421_31,
inference(rat,[],[s27,s1549,s7,s1440,s14,s16,s1921]) ).
cnf(s1927,plain,
spl421_11,
inference(rat,[],[s5,s16,s14,s10]) ).
cnf(s1931,plain,
spl421_7,
inference(rat,[],[s4,s7]) ).
cnf(s1932,plain,
~ spl421_5,
inference(rat,[],[s1151,s1564,s1565,s1717,s1924,s1573,s1586,s1927,s1931]) ).
cnf(s1945,plain,
$false,
inference(rat,[],[s3,s7,s1932]) ).
fof(f23143,plain,
$false,
inference(avatar_sat_refutation,[],[s1945]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT333+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.38 % Computer : n007.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Sun Sep 27 14:40:55 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.42 Running first-order theorem proving
% 0.12/0.42 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 13.57/2.97 % (1490581)Detected formulas, will run a generic FOF schedule.
% 13.57/2.97 % (1490589)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1765890858:i=109:sd=1:ins=1:gsp=on:ss=axioms_2998 on theBenchmark for (2998ds/109Mi)
% 13.57/2.97 % (1490589)Refutation not found, incomplete strategy
% 13.57/2.97 % (1490589)------------------------------
% 13.57/2.97 % (1490589)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.57/2.97 % (1490589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.57/2.97 % (1490589)CaDiCaL version: 2.1.3
% 13.57/2.97 % (1490589)Termination reason: Refutation not found, incomplete strategy
% 13.57/2.97 % (1490589)Time elapsed: 0.008 s
% 13.57/2.97 % (1490589)Peak memory usage: 91 MB
% 13.57/2.97 % (1490589)Instructions burned: 13 (million)
% 13.57/2.97 % (1490587)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=1386600610:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2998 on theBenchmark for (2998ds/134677Mi)
% 13.57/2.97 % (1490588)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=1825296297:i=141695:sd=1:nm=32:gsp=on:ss=included_2998 on theBenchmark for (2998ds/141695Mi)
% 13.57/2.97 % (1490590)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1136558843:i=119:av=off:ss=axioms_2998 on theBenchmark for (2998ds/119Mi)
% 13.57/2.97 % (1490591)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=311801953:s2a=on:i=139:gtg=position_2998 on theBenchmark for (2998ds/139Mi)
% 13.57/2.97 % (1490586)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=2007479174:i=141193_2998 on theBenchmark for (2998ds/141193Mi)
% 13.57/2.97 % (1490592)dis-21_1_sil=8000:lcm=predicate:random_seed=410638010: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)
% 13.57/2.97 % (1490590)Instruction limit reached!
% 13.57/2.97 % (1490590)------------------------------
% 13.57/2.97 % (1490590)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.57/2.97 % (1490590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.57/2.97 % (1490590)CaDiCaL version: 2.1.3
% 13.57/2.97 % (1490590)Termination reason: Instruction limit
% 13.57/2.97 % (1490590)Termination phase: Saturation
% 13.57/2.97 % (1490590)Time elapsed: 0.078 s
% 13.57/2.97 % (1490590)Peak memory usage: 93 MB
% 13.57/2.97 % (1490590)Instructions burned: 120 (million)
% 13.57/2.97 % (1490592)Instruction limit reached!
% 13.57/2.97 % (1490592)------------------------------
% 13.57/2.97 % (1490592)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.57/2.97 % (1490592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.57/2.97 % (1490592)CaDiCaL version: 2.1.3
% 13.57/2.97 % (1490592)Termination reason: Instruction limit
% 13.57/2.97 % (1490592)Termination phase: Property scanning
% 13.57/2.97 % (1490592)Time elapsed: 0.078 s
% 13.57/2.97 % (1490592)Peak memory usage: 93 MB
% 13.57/2.97 % (1490592)Instructions burned: 131 (million)
% 13.57/2.97 % (1490591)Instruction limit reached!
% 13.57/2.97 % (1490591)------------------------------
% 13.57/2.97 % (1490591)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.57/2.97 % (1490591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.57/2.97 % (1490591)CaDiCaL version: 2.1.3
% 13.57/2.97 % (1490591)Termination reason: Instruction limit
% 13.57/2.97 % (1490591)Termination phase: Clausification
% 13.57/2.97 % (1490591)Time elapsed: 0.087 s
% 13.57/2.97 % (1490591)Peak memory usage: 94 MB
% 13.57/2.97 % (1490591)Instructions burned: 140 (million)
% 13.57/2.97 % (1490589)------------------------------
% 13.57/2.97 % (1490589)------------------------------
% 13.57/2.97 % (1490601)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2558272995:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi)
% 13.57/2.97 % (1490600)lrs+10_1_sil=8000:sp=occurrence:random_seed=716047238:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi)
% 13.57/2.97 % (1490602)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2122810734:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi)
% 13.57/2.97 % (1490601)Refutation not found, incomplete strategy
% 13.57/2.97 % (1490601)------------------------------
% 13.57/2.97 % (1490601)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.74/3.88 % (1490601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.74/3.88 % (1490601)CaDiCaL version: 2.1.3
% 19.74/3.88 % (1490601)Termination reason: Refutation not found, incomplete strategy
% 19.74/3.88 % (1490601)Time elapsed: 0.025 s
% 19.74/3.88 % (1490601)Peak memory usage: 92 MB
% 19.74/3.88 % (1490601)Instructions burned: 43 (million)
% 19.74/3.88 % (1490603)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=2133481929:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 19.74/3.88 % (1490602)Refutation not found, incomplete strategy
% 19.74/3.88 % (1490602)------------------------------
% 19.74/3.88 % (1490602)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.74/3.88 % (1490602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.74/3.88 % (1490602)CaDiCaL version: 2.1.3
% 19.74/3.88 % (1490602)Termination reason: Refutation not found, incomplete strategy
% 19.74/3.88 % (1490602)Time elapsed: 0.013 s
% 19.74/3.88 % (1490602)Peak memory usage: 92 MB
% 19.74/3.88 % (1490602)Instructions burned: 13 (million)
% 19.74/3.88 % (1490603)Instruction limit reached!
% 19.74/3.88 % (1490603)------------------------------
% 19.74/3.88 % (1490603)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.74/3.88 % (1490603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.74/3.88 % (1490603)CaDiCaL version: 2.1.3
% 19.74/3.88 % (1490603)Termination reason: Instruction limit
% 19.74/3.88 % (1490603)Termination phase: Saturation
% 19.74/3.88 % (1490603)Time elapsed: 0.078 s
% 19.74/3.88 % (1490603)Peak memory usage: 97 MB
% 19.74/3.88 % (1490603)Instructions burned: 250 (million)
% 19.74/3.88 % (1490600)Instruction limit reached!
% 19.74/3.88 % (1490600)------------------------------
% 19.74/3.88 % (1490600)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.74/3.88 % (1490600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.74/3.88 % (1490600)CaDiCaL version: 2.1.3
% 19.74/3.88 % (1490600)Termination reason: Instruction limit
% 19.74/3.88 % (1490600)Termination phase: Saturation
% 19.74/3.88 % (1490600)Time elapsed: 0.181 s
% 19.74/3.88 % (1490600)Peak memory usage: 95 MB
% 19.74/3.88 % (1490600)Instructions burned: 285 (million)
% 19.74/3.88 % (1490608)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=4122932985:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi)
% 19.74/3.88 % (1490601)------------------------------
% 19.74/3.88 % (1490601)------------------------------
% 19.74/3.88 % (1490602)------------------------------
% 19.74/3.88 % (1490602)------------------------------
% 19.74/3.88 % (1490608)Instruction limit reached!
% 19.74/3.88 % (1490608)------------------------------
% 19.74/3.88 % (1490608)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.74/3.88 % (1490608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.74/3.88 % (1490608)CaDiCaL version: 2.1.3
% 19.74/3.88 % (1490608)Termination reason: Instruction limit
% 19.74/3.88 % (1490608)Termination phase: Saturation
% 19.74/3.88 % (1490608)Time elapsed: 0.094 s
% 19.74/3.88 % (1490608)Peak memory usage: 95 MB
% 19.74/3.88 % (1490608)Instructions burned: 296 (million)
% 19.74/3.88 % (1490609)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=889199281:i=2350_2993 on theBenchmark for (2993ds/2350Mi)
% 19.74/3.88 % (1490612)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2064395091:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi)
% 19.74/3.88 % (1490611)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=913820793:cts=off:i=113:fsr=off:ss=included:sgt=4_2992 on theBenchmark for (2992ds/113Mi)
% 19.74/3.88 % (1490614)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2268980055:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 19.74/3.88 % (1490611)Instruction limit reached!
% 19.74/3.88 % (1490611)------------------------------
% 19.74/3.88 % (1490611)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.74/3.88 % (1490611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.74/3.88 % (1490611)CaDiCaL version: 2.1.3
% 19.74/3.88 % (1490611)Termination reason: Instruction limit
% 19.74/3.88 % (1490611)Termination phase: Saturation
% 19.74/3.88 % (1490611)Time elapsed: 0.066 s
% 19.74/3.88 % (1490611)Peak memory usage: 93 MB
% 21.01/4.04 % (1490611)Instructions burned: 114 (million)
% 21.01/4.04 % (1490612)Instruction limit reached!
% 21.01/4.04 % (1490612)------------------------------
% 21.01/4.04 % (1490612)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.01/4.04 % (1490612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.01/4.04 % (1490612)CaDiCaL version: 2.1.3
% 21.01/4.04 % (1490612)Termination reason: Instruction limit
% 21.01/4.04 % (1490612)Termination phase: Property scanning
% 21.01/4.04 % (1490612)Time elapsed: 0.077 s
% 21.01/4.04 % (1490612)Peak memory usage: 94 MB
% 21.01/4.04 % (1490612)Instructions burned: 128 (million)
% 21.01/4.04 % (1490614)Instruction limit reached!
% 21.01/4.04 % (1490614)------------------------------
% 21.01/4.04 % (1490614)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.01/4.04 % (1490614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.01/4.04 % (1490614)CaDiCaL version: 2.1.3
% 21.01/4.04 % (1490614)Termination reason: Instruction limit
% 21.01/4.04 % (1490614)Termination phase: Property scanning
% 21.01/4.04 % (1490614)Time elapsed: 0.032 s
% 21.01/4.04 % (1490614)Peak memory usage: 91 MB
% 21.01/4.04 % (1490614)Instructions burned: 119 (million)
% 21.01/4.04 % (1490620)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2306798394:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi)
% 21.01/4.04 % (1490618)lrs+10_1_sil=8000:sp=occurrence:random_seed=1448070946:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2989 on theBenchmark for (2989ds/907Mi)
% 21.01/4.04 % (1490619)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1602537315:i=437:sd=1:aac=none:ss=included_2989 on theBenchmark for (2989ds/437Mi)
% 21.01/4.04 % (1490619)Refutation not found, incomplete strategy
% 21.01/4.04 % (1490619)------------------------------
% 21.01/4.04 % (1490619)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.01/4.04 % (1490619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.01/4.04 % (1490619)CaDiCaL version: 2.1.3
% 21.01/4.04 % (1490619)Termination reason: Refutation not found, incomplete strategy
% 21.01/4.04 % (1490619)Time elapsed: 0.065 s
% 21.01/4.04 % (1490619)Peak memory usage: 94 MB
% 21.01/4.04 % (1490619)Instructions burned: 109 (million)
% 21.01/4.04 % (1490619)------------------------------
% 21.01/4.04 % (1490619)------------------------------
% 21.01/4.04 % (1490624)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1511394441:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2984 on theBenchmark for (2984ds/134Mi)
% 21.01/4.04 % (1490618)Instruction limit reached!
% 21.01/4.04 % (1490618)------------------------------
% 21.01/4.04 % (1490618)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.01/4.04 % (1490618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.01/4.04 % (1490618)CaDiCaL version: 2.1.3
% 21.01/4.04 % (1490618)Termination reason: Instruction limit
% 21.01/4.04 % (1490618)Termination phase: Saturation
% 21.01/4.04 % (1490618)Time elapsed: 0.581 s
% 21.01/4.04 % (1490618)Peak memory usage: 106 MB
% 21.01/4.04 % (1490618)Instructions burned: 908 (million)
% 21.01/4.04 % (1490624)Instruction limit reached!
% 21.01/4.04 % (1490624)------------------------------
% 21.01/4.04 % (1490624)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.01/4.04 % (1490624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.01/4.04 % (1490624)CaDiCaL version: 2.1.3
% 21.01/4.04 % (1490624)Termination reason: Instruction limit
% 21.01/4.04 % (1490624)Termination phase: Saturation
% 21.01/4.04 % (1490624)Time elapsed: 0.081 s
% 21.01/4.04 % (1490624)Peak memory usage: 95 MB
% 21.01/4.04 % (1490624)Instructions burned: 134 (million)
% 21.01/4.04 % (1490626)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3388152578:st=8:i=592:sd=3:ep=RST:ss=axioms_2982 on theBenchmark for (2982ds/592Mi)
% 21.01/4.04 % (1490627)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3655687184:st=3:i=13193:sd=3:ss=axioms_2982 on theBenchmark for (2982ds/13193Mi)
% 21.01/4.04 % (1490626)Refutation not found, incomplete strategy
% 21.01/4.04 % (1490626)------------------------------
% 21.01/4.04 % (1490626)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.01/4.04 % (1490626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.01/4.04 % (1490626)CaDiCaL version: 2.1.3
% 21.01/4.04 % (1490626)Termination reason: Refutation not found, incomplete strategy
% 21.01/4.04 % (1490626)Time elapsed: 0.220 s
% 21.01/4.04 % (1490626)Peak memory usage: 100 MB
% 21.01/4.04 % (1490626)Instructions burned: 460 (million)
% 21.01/4.04 % (1490609)Instruction limit reached!
% 21.01/4.04 % (1490609)------------------------------
% 21.01/4.04 % (1490609)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.01/4.04 % (1490609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.01/4.04 % (1490609)CaDiCaL version: 2.1.3
% 21.01/4.04 % (1490609)Termination reason: Instruction limit
% 21.01/4.04 % (1490609)Termination phase: Saturation
% 21.01/4.04 % (1490609)Time elapsed: 1.466 s
% 21.01/4.04 % (1490609)Peak memory usage: 226 MB
% 21.01/4.04 % (1490609)Instructions burned: 2351 (million)
% 21.01/4.04 % (1490626)------------------------------
% 21.01/4.04 % (1490626)------------------------------
% 21.01/4.04 % (1490630)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=1880569511:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2976 on theBenchmark for (2976ds/125Mi)
% 21.01/4.04 % (1490631)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1345310973:i=134:gtgl=5:slsql=off:gtg=exists_sym_2976 on theBenchmark for (2976ds/134Mi)
% 21.01/4.04 % (1490630)Instruction limit reached!
% 21.01/4.04 % (1490630)------------------------------
% 21.01/4.04 % (1490630)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.01/4.04 % (1490630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.01/4.04 % (1490630)CaDiCaL version: 2.1.3
% 21.01/4.04 % (1490630)Termination reason: Instruction limit
% 21.01/4.04 % (1490630)Termination phase: Saturation
% 21.01/4.04 % (1490630)Time elapsed: 0.069 s
% 21.01/4.04 % (1490630)Peak memory usage: 93 MB
% 21.01/4.04 % (1490630)Instructions burned: 125 (million)
% 21.01/4.04 % (1490631)Instruction limit reached!
% 21.01/4.04 % (1490631)------------------------------
% 21.01/4.04 % (1490631)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.01/4.04 % (1490631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.01/4.04 % (1490631)CaDiCaL version: 2.1.3
% 21.01/4.04 % (1490631)Termination reason: Instruction limit
% 21.01/4.04 % (1490631)Termination phase: Preprocessing 3
% 21.01/4.04 % (1490631)Time elapsed: 0.076 s
% 21.01/4.04 % (1490631)Peak memory usage: 92 MB
% 21.01/4.04 % (1490631)Instructions burned: 134 (million)
% 21.01/4.04 % (1490634)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1865865060:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2974 on theBenchmark for (2974ds/141Mi)
% 21.01/4.04 % (1490634)Refutation not found, incomplete strategy
% 21.01/4.04 % (1490634)------------------------------
% 21.01/4.04 % (1490634)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.01/4.04 % (1490634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.01/4.04 % (1490634)CaDiCaL version: 2.1.3
% 21.01/4.04 % (1490634)Termination reason: Refutation not found, incomplete strategy
% 21.01/4.04 % (1490634)Time elapsed: 0.012 s
% 21.01/4.04 % (1490634)Peak memory usage: 91 MB
% 21.01/4.04 % (1490634)Instructions burned: 12 (million)
% 21.01/4.04 % (1490635)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1340273523:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2974 on theBenchmark for (2974ds/431Mi)
% 21.01/4.04 % (1490620)Instruction limit reached!
% 21.01/4.04 % (1490620)------------------------------
% 21.01/4.04 % (1490620)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.01/4.04 % (1490620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.01/4.04 % (1490620)CaDiCaL version: 2.1.3
% 21.01/4.04 % (1490620)Termination reason: Instruction limit
% 21.01/4.04 % (1490620)Termination phase: Saturation
% 21.01/4.04 % (1490620)Time elapsed: 1.681 s
% 21.01/4.04 % (1490620)Peak memory usage: 179 MB
% 21.01/4.04 % (1490620)Instructions burned: 5205 (million)
% 21.01/4.04 % (1490587)First to succeed.
% 21.01/4.04 % (1490587)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1490581"
% 21.01/4.04 % (1490634)------------------------------
% 21.01/4.04 % (1490634)------------------------------
% 21.01/4.04 % (1490638)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=1486699961:i=6060:aac=none:ins=25_2971 on theBenchmark for (2971ds/6060Mi)
% 21.01/4.04 % (1490586)Also succeeded, but the first one will report.
% 21.01/4.04 % (1490635)Instruction limit reached!
% 21.01/4.04 % (1490635)------------------------------
% 21.01/4.04 % (1490635)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.01/4.04 % (1490635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.01/4.04 % (1490635)CaDiCaL version: 2.1.3
% 21.01/4.04 % (1490635)Termination reason: Instruction limit
% 21.01/4.04 % (1490635)Termination phase: Saturation
% 21.01/4.04 % (1490635)Time elapsed: 0.262 s
% 21.01/4.04 % (1490635)Peak memory usage: 97 MB
% 21.01/4.04 % (1490635)Instructions burned: 431 (million)
% 21.01/4.04 % (1490639)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=1104508210:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2970 on theBenchmark for (2970ds/150Mi)
% 21.01/4.04 % (1490587)Refutation found. Thanks to Tanya!
% 21.01/4.04 % SZS status Theorem for theBenchmark
% 21.01/4.04 % SZS output start Proof for theBenchmark
% See solution above
% 22.32/4.23 % (1490587)------------------------------
% 22.32/4.23 % (1490587)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.32/4.23 % (1490587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.32/4.23 % (1490587)CaDiCaL version: 2.1.3
% 22.32/4.23 % (1490587)Termination reason: Refutation
% 22.32/4.23 % (1490587)Time elapsed: 2.615 s
% 22.32/4.23 % (1490587)Peak memory usage: 166 MB
% 22.32/4.23 % (1490587)Instructions burned: 4022 (million)
% 22.32/4.23 % (1490587)------------------------------
% 22.32/4.23 % (1490587)------------------------------
% 22.32/4.23 % (1490581)Success in time 3.171 s
% 22.32/4.23 % Vampire exiting
%------------------------------------------------------------------------------