%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT326+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 : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:46:58 AM UTC 2026
% Result : Theorem 22.24s 3.88s
% Output : Refutation 22.94s
% Verified :
% SZS Type : Refutation
% Derivation depth : 37
% Number of leaves : 56
% Syntax : Number of formulae : 487 ( 82 unt; 31 def)
% Number of atoms : 2552 ( 74 equ)
% Maximal formula atoms : 21 ( 5 avg)
% Number of connectives : 3590 (1525 ~;1745 |; 241 &)
% ( 28 <=>; 51 =>; 0 <=; 0 <~>)
% Maximal formula depth : 26 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 53 ( 51 usr; 26 prp; 0-3 aty)
% Number of functors : 18 ( 18 usr; 9 con; 0-2 aty)
% Number of variables : 311 ( 0 sgn 303 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2341,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l3_lattices(X0) )
=> ( v10_lattices(X0)
<=> ( v4_lattices(X0)
& v5_lattices(X0)
& v8_lattices(X0)
& v6_lattices(X0)
& v7_lattices(X0)
& v9_lattices(X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d10_lattices) ).
fof(f2410,axiom,
! [X0] :
( l3_lattices(X0)
=> ( l1_lattices(X0)
& l2_lattices(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l3_lattices) ).
fof(f2428,axiom,
! [X0] :
( l1_lattices(X0)
=> ( v1_funct_1(u1_lattices(X0))
& v1_funct_2(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
& m2_relset_1(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_u1_lattices) ).
fof(f2429,axiom,
! [X0] :
( l2_lattices(X0)
=> ( v1_funct_1(u2_lattices(X0))
& v1_funct_2(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
& m2_relset_1(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_u2_lattices) ).
fof(f2455,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> m1_filter_0(u1_struct_0(X0),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t15_filter_0) ).
fof(f2540,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_filter_0(X1,X0)
=> ( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m1_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(f2567,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v6_lattices(X0)
& l1_lattices(X0) )
=> ( v1_relat_1(u1_lattices(X0))
& v1_funct_1(u1_lattices(X0))
& v1_funct_2(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
& v1_binop_1(u1_lattices(X0),u1_struct_0(X0))
& v1_partfun1(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc4_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(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(f2606,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v4_lattices(X0)
& l2_lattices(X0) )
=> v1_binop_1(u2_lattices(X0),u1_struct_0(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t27_lattice2) ).
fof(f2608,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v5_lattices(X0)
& l2_lattices(X0) )
=> v2_binop_1(u2_lattices(X0),u1_struct_0(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t29_lattice2) ).
fof(f2610,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v6_lattices(X0)
& l1_lattices(X0) )
=> v1_binop_1(u1_lattices(X0),u1_struct_0(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t31_lattice2) ).
fof(f2611,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v7_lattices(X0)
& l1_lattices(X0) )
=> v2_binop_1(u1_lattices(X0),u1_struct_0(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t32_lattice2) ).
fof(f2619,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> r1_lattice2(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t40_lattice2) ).
fof(f2620,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> r1_lattice2(u1_struct_0(X0),u1_lattices(X0),u2_lattices(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t41_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(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(f2890,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& m2_lattice4(X1,X0) )
=> m2_lattice4(k9_filter_2(X0,X1),k1_lattice2(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k9_filter_2) ).
fof(f2891,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& m2_lattice4(X1,X0) )
=> k9_filter_2(X0,X1) = k7_filter_2(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k9_filter_2) ).
fof(f2916,axiom,
! [X0] :
( ~ v1_xboole_0(X0)
=> ! [X1] :
( ( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(X0)) )
=> ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
& m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0) )
=> ! [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) )
=> ( X3 = k1_realset1(X2,X1)
=> ( ( v1_binop_1(X2,X0)
=> v1_binop_1(X3,X1) )
& ( v3_binop_1(X2,X0)
=> v3_binop_1(X3,X1) )
& ( v2_binop_1(X2,X0)
=> v2_binop_1(X3,X1) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_filter_2) ).
fof(f2920,axiom,
! [X0] :
( ~ v1_xboole_0(X0)
=> ! [X1] :
( ( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(X0)) )
=> ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
& m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0) )
=> ! [X3] :
( ( v1_funct_1(X3)
& v1_funct_2(X3,k2_zfmisc_1(X0,X0),X0)
& m2_relset_1(X3,k2_zfmisc_1(X0,X0),X0) )
=> ! [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) )
=> ! [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) )
=> ( ( X4 = k1_realset1(X2,X1)
& X5 = k1_realset1(X3,X1)
& r1_lattice2(X0,X2,X3) )
=> r1_lattice2(X1,X4,X5) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t5_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(f2996,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) )
=> ( v1_funct_1(k1_realset1(u2_lattices(X0),X1))
& v1_funct_2(k1_realset1(u2_lattices(X0),X1),k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(k1_realset1(u2_lattices(X0),X1),k2_zfmisc_1(X1,X1),X1)
& v1_funct_1(k1_realset1(u1_lattices(X0),X1))
& v1_funct_2(k1_realset1(u1_lattices(X0),X1),k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(k1_realset1(u1_lattices(X0),X1),k2_zfmisc_1(X1,X1),X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t61_filter_2) ).
fof(f2997,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) )
=> ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(X2,k2_zfmisc_1(X1,X1),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) )
=> ( ( X2 = k1_realset1(u2_lattices(X0),X1)
& X3 = k1_realset1(u1_lattices(X0),X1) )
=> ( v1_binop_1(X2,X1)
& v2_binop_1(X2,X1)
& v1_binop_1(X3,X1)
& v2_binop_1(X3,X1)
& r1_lattice2(X1,X2,X3)
& r1_lattice2(X1,X3,X2) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t62_filter_2) ).
fof(f2998,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) )
=> ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(X2,k2_zfmisc_1(X1,X1),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) )
=> ( ( X2 = k1_realset1(u2_lattices(X0),X1)
& X3 = k1_realset1(u1_lattices(X0),X1) )
=> ( v1_binop_1(X2,X1)
& v2_binop_1(X2,X1)
& v1_binop_1(X3,X1)
& v2_binop_1(X3,X1)
& r1_lattice2(X1,X2,X3)
& r1_lattice2(X1,X3,X2) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f2997]) ).
fof(f5335,plain,
! [X0] :
( ( v10_lattices(X0)
<=> ( v4_lattices(X0)
& v5_lattices(X0)
& v8_lattices(X0)
& v6_lattices(X0)
& v7_lattices(X0)
& v9_lattices(X0) ) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2341]) ).
fof(f5336,plain,
! [X0] :
( ( v10_lattices(X0)
<=> ( v4_lattices(X0)
& v5_lattices(X0)
& v8_lattices(X0)
& v6_lattices(X0)
& v7_lattices(X0)
& v9_lattices(X0) ) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f5335]) ).
fof(f5413,plain,
! [X0] :
( ( l1_lattices(X0)
& l2_lattices(X0) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2410]) ).
fof(f5446,plain,
! [X0] :
( ( v1_funct_1(u1_lattices(X0))
& v1_funct_2(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
& m2_relset_1(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0)) )
| ~ l1_lattices(X0) ),
inference(ennf_transformation,[],[f2428]) ).
fof(f5447,plain,
! [X0] :
( ( v1_funct_1(u2_lattices(X0))
& v1_funct_2(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
& m2_relset_1(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0)) )
| ~ l2_lattices(X0) ),
inference(ennf_transformation,[],[f2429]) ).
fof(f5494,plain,
! [X0] :
( m1_filter_0(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2455]) ).
fof(f5495,plain,
! [X0] :
( m1_filter_0(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f5494]) ).
fof(f5638,plain,
! [X0] :
( ! [X1] :
( ( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2540]) ).
fof(f5639,plain,
! [X0] :
( ! [X1] :
( ( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f5638]) ).
fof(f5686,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(f5687,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f5686]) ).
fof(f5692,plain,
! [X0] :
( ( v1_relat_1(u1_lattices(X0))
& v1_funct_1(u1_lattices(X0))
& v1_funct_2(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
& v1_binop_1(u1_lattices(X0),u1_struct_0(X0))
& v1_partfun1(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v6_lattices(X0)
| ~ l1_lattices(X0) ),
inference(ennf_transformation,[],[f2567]) ).
fof(f5693,plain,
! [X0] :
( ( v1_relat_1(u1_lattices(X0))
& v1_funct_1(u1_lattices(X0))
& v1_funct_2(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
& v1_binop_1(u1_lattices(X0),u1_struct_0(X0))
& v1_partfun1(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v6_lattices(X0)
| ~ l1_lattices(X0) ),
inference(flattening,[],[f5692]) ).
fof(f5696,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(f5697,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,[],[f5696]) ).
fof(f5737,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(f5738,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,[],[f5737]) ).
fof(f5751,plain,
! [X0] :
( v1_binop_1(u2_lattices(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v4_lattices(X0)
| ~ l2_lattices(X0) ),
inference(ennf_transformation,[],[f2606]) ).
fof(f5752,plain,
! [X0] :
( v1_binop_1(u2_lattices(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v4_lattices(X0)
| ~ l2_lattices(X0) ),
inference(flattening,[],[f5751]) ).
fof(f5755,plain,
! [X0] :
( v2_binop_1(u2_lattices(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v5_lattices(X0)
| ~ l2_lattices(X0) ),
inference(ennf_transformation,[],[f2608]) ).
fof(f5756,plain,
! [X0] :
( v2_binop_1(u2_lattices(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v5_lattices(X0)
| ~ l2_lattices(X0) ),
inference(flattening,[],[f5755]) ).
fof(f5759,plain,
! [X0] :
( v1_binop_1(u1_lattices(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v6_lattices(X0)
| ~ l1_lattices(X0) ),
inference(ennf_transformation,[],[f2610]) ).
fof(f5760,plain,
! [X0] :
( v1_binop_1(u1_lattices(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v6_lattices(X0)
| ~ l1_lattices(X0) ),
inference(flattening,[],[f5759]) ).
fof(f5761,plain,
! [X0] :
( v2_binop_1(u1_lattices(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v7_lattices(X0)
| ~ l1_lattices(X0) ),
inference(ennf_transformation,[],[f2611]) ).
fof(f5762,plain,
! [X0] :
( v2_binop_1(u1_lattices(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v7_lattices(X0)
| ~ l1_lattices(X0) ),
inference(flattening,[],[f5761]) ).
fof(f5777,plain,
! [X0] :
( r1_lattice2(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2619]) ).
fof(f5778,plain,
! [X0] :
( r1_lattice2(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f5777]) ).
fof(f5779,plain,
! [X0] :
( r1_lattice2(u1_struct_0(X0),u1_lattices(X0),u2_lattices(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2620]) ).
fof(f5780,plain,
! [X0] :
( r1_lattice2(u1_struct_0(X0),u1_lattices(X0),u2_lattices(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f5779]) ).
fof(f5873,plain,
! [X0] :
( ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2669]) ).
fof(f6052,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(f6053,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,[],[f6052]) ).
fof(f6118,plain,
! [X0,X1] :
( m2_lattice4(k9_filter_2(X0,X1),k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m2_lattice4(X1,X0) ),
inference(ennf_transformation,[],[f2890]) ).
fof(f6119,plain,
! [X0,X1] :
( m2_lattice4(k9_filter_2(X0,X1),k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m2_lattice4(X1,X0) ),
inference(flattening,[],[f6118]) ).
fof(f6120,plain,
! [X0,X1] :
( k9_filter_2(X0,X1) = k7_filter_2(X0,X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m2_lattice4(X1,X0) ),
inference(ennf_transformation,[],[f2891]) ).
fof(f6121,plain,
! [X0,X1] :
( k9_filter_2(X0,X1) = k7_filter_2(X0,X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m2_lattice4(X1,X0) ),
inference(flattening,[],[f6120]) ).
fof(f6170,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( ( v1_binop_1(X3,X1)
| ~ v1_binop_1(X2,X0) )
& ( v3_binop_1(X3,X1)
| ~ v3_binop_1(X2,X0) )
& ( v2_binop_1(X3,X1)
| ~ v2_binop_1(X2,X0) ) )
| k1_realset1(X2,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) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0)) )
| v1_xboole_0(X0) ),
inference(ennf_transformation,[],[f2916]) ).
fof(f6171,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( ( v1_binop_1(X3,X1)
| ~ v1_binop_1(X2,X0) )
& ( v3_binop_1(X3,X1)
| ~ v3_binop_1(X2,X0) )
& ( v2_binop_1(X3,X1)
| ~ v2_binop_1(X2,X0) ) )
| k1_realset1(X2,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) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0)) )
| v1_xboole_0(X0) ),
inference(flattening,[],[f6170]) ).
fof(f6178,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( r1_lattice2(X1,X4,X5)
| k1_realset1(X2,X1) != X4
| k1_realset1(X3,X1) != X5
| ~ r1_lattice2(X0,X2,X3)
| ~ v1_funct_1(X5)
| ~ v1_funct_2(X5,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(X5,k2_zfmisc_1(X1,X1),X1) )
| ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(X4,k2_zfmisc_1(X1,X1),X1) )
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X3,k2_zfmisc_1(X0,X0),X0) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0)) )
| v1_xboole_0(X0) ),
inference(ennf_transformation,[],[f2920]) ).
fof(f6179,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( r1_lattice2(X1,X4,X5)
| k1_realset1(X2,X1) != X4
| k1_realset1(X3,X1) != X5
| ~ r1_lattice2(X0,X2,X3)
| ~ v1_funct_1(X5)
| ~ v1_funct_2(X5,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(X5,k2_zfmisc_1(X1,X1),X1) )
| ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(X4,k2_zfmisc_1(X1,X1),X1) )
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X3,k2_zfmisc_1(X0,X0),X0) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0)) )
| v1_xboole_0(X0) ),
inference(flattening,[],[f6178]) ).
fof(f6219,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(f6220,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,[],[f6219]) ).
fof(f6327,plain,
! [X0] :
( ! [X1] :
( ( v1_funct_1(k1_realset1(u2_lattices(X0),X1))
& v1_funct_2(k1_realset1(u2_lattices(X0),X1),k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(k1_realset1(u2_lattices(X0),X1),k2_zfmisc_1(X1,X1),X1)
& v1_funct_1(k1_realset1(u1_lattices(X0),X1))
& v1_funct_2(k1_realset1(u1_lattices(X0),X1),k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(k1_realset1(u1_lattices(X0),X1),k2_zfmisc_1(X1,X1),X1) )
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2996]) ).
fof(f6328,plain,
! [X0] :
( ! [X1] :
( ( v1_funct_1(k1_realset1(u2_lattices(X0),X1))
& v1_funct_2(k1_realset1(u2_lattices(X0),X1),k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(k1_realset1(u2_lattices(X0),X1),k2_zfmisc_1(X1,X1),X1)
& v1_funct_1(k1_realset1(u1_lattices(X0),X1))
& v1_funct_2(k1_realset1(u1_lattices(X0),X1),k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(k1_realset1(u1_lattices(X0),X1),k2_zfmisc_1(X1,X1),X1) )
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f6327]) ).
fof(f6329,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( ( ~ v1_binop_1(X2,X1)
| ~ v2_binop_1(X2,X1)
| ~ v1_binop_1(X3,X1)
| ~ v2_binop_1(X3,X1)
| ~ r1_lattice2(X1,X2,X3)
| ~ r1_lattice2(X1,X3,X2) )
& X2 = k1_realset1(u2_lattices(X0),X1)
& X3 = k1_realset1(u1_lattices(X0),X1)
& v1_funct_1(X3)
& v1_funct_2(X3,k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(X3,k2_zfmisc_1(X1,X1),X1) )
& v1_funct_1(X2)
& v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(X2,k2_zfmisc_1(X1,X1),X1) )
& ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(ennf_transformation,[],[f2998]) ).
fof(f6330,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( ( ~ v1_binop_1(X2,X1)
| ~ v2_binop_1(X2,X1)
| ~ v1_binop_1(X3,X1)
| ~ v2_binop_1(X3,X1)
| ~ r1_lattice2(X1,X2,X3)
| ~ r1_lattice2(X1,X3,X2) )
& X2 = k1_realset1(u2_lattices(X0),X1)
& X3 = k1_realset1(u1_lattices(X0),X1)
& v1_funct_1(X3)
& v1_funct_2(X3,k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(X3,k2_zfmisc_1(X1,X1),X1) )
& v1_funct_1(X2)
& v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(X2,k2_zfmisc_1(X1,X1),X1) )
& ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(flattening,[],[f6329]) ).
fof(f6505,definition,
! [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)) )
| ~ sP112(X0) ),
introduced(definition,[new_symbols(definition,[sP112])],[predicate_definition_introduction]) ).
fof(f6506,plain,
! [X0] :
( sP112(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(definition_folding,[],[f5697,f6505]) ).
fof(f7802,plain,
! [X0] :
( ( ( v10_lattices(X0)
| ~ v4_lattices(X0)
| ~ v5_lattices(X0)
| ~ v8_lattices(X0)
| ~ v6_lattices(X0)
| ~ v7_lattices(X0)
| ~ v9_lattices(X0) )
& ( ( v4_lattices(X0)
& v5_lattices(X0)
& v8_lattices(X0)
& v6_lattices(X0)
& v7_lattices(X0)
& v9_lattices(X0) )
| ~ v10_lattices(X0) ) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f5336]) ).
fof(f7803,plain,
! [X0] :
( ( ( v10_lattices(X0)
| ~ v4_lattices(X0)
| ~ v5_lattices(X0)
| ~ v8_lattices(X0)
| ~ v6_lattices(X0)
| ~ v7_lattices(X0)
| ~ v9_lattices(X0) )
& ( ( v4_lattices(X0)
& v5_lattices(X0)
& v8_lattices(X0)
& v6_lattices(X0)
& v7_lattices(X0)
& v9_lattices(X0) )
| ~ v10_lattices(X0) ) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f7802]) ).
fof(f7912,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)) )
| ~ sP112(X0) ),
inference(nnf_transformation,[],[f6505]) ).
fof(f8097,plain,
( ( ~ v1_binop_1(sK1081,sK1080)
| ~ v2_binop_1(sK1081,sK1080)
| ~ v1_binop_1(sK1082,sK1080)
| ~ v2_binop_1(sK1082,sK1080)
| ~ r1_lattice2(sK1080,sK1081,sK1082)
| ~ r1_lattice2(sK1080,sK1082,sK1081) )
& sK1081 = k1_realset1(u2_lattices(sK1079),sK1080)
& sK1082 = k1_realset1(u1_lattices(sK1079),sK1080)
& v1_funct_1(sK1082)
& v1_funct_2(sK1082,k2_zfmisc_1(sK1080,sK1080),sK1080)
& m2_relset_1(sK1082,k2_zfmisc_1(sK1080,sK1080),sK1080)
& v1_funct_1(sK1081)
& v1_funct_2(sK1081,k2_zfmisc_1(sK1080,sK1080),sK1080)
& m2_relset_1(sK1081,k2_zfmisc_1(sK1080,sK1080),sK1080)
& ~ v1_xboole_0(sK1080)
& m2_lattice4(sK1080,sK1079)
& ~ v3_struct_0(sK1079)
& v10_lattices(sK1079)
& l3_lattices(sK1079) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1079,sK1080,sK1081,sK1082]),skolemize(X0,sK1079),skolemize(X1,sK1080),skolemize(X2,sK1081),skolemize(X3,sK1082)],[f6330]) ).
fof(f12370,plain,
! [X0] :
( ~ v10_lattices(X0)
| v7_lattices(X0)
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f7803]) ).
fof(f12371,plain,
! [X0] :
( ~ v10_lattices(X0)
| v6_lattices(X0)
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f7803]) ).
fof(f12373,plain,
! [X0] :
( ~ v10_lattices(X0)
| v5_lattices(X0)
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f7803]) ).
fof(f12374,plain,
! [X0] :
( ~ v10_lattices(X0)
| v4_lattices(X0)
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f7803]) ).
fof(f12465,plain,
! [X0] :
( ~ l3_lattices(X0)
| l2_lattices(X0) ),
inference(cnf_transformation,[],[f5413]) ).
fof(f12466,plain,
! [X0] :
( ~ l3_lattices(X0)
| l1_lattices(X0) ),
inference(cnf_transformation,[],[f5413]) ).
fof(f12485,plain,
! [X0] :
( m2_relset_1(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| ~ l1_lattices(X0) ),
inference(cnf_transformation,[],[f5446]) ).
fof(f12486,plain,
! [X0] :
( v1_funct_2(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| ~ l1_lattices(X0) ),
inference(cnf_transformation,[],[f5446]) ).
fof(f12487,plain,
! [X0] :
( v1_funct_1(u1_lattices(X0))
| ~ l1_lattices(X0) ),
inference(cnf_transformation,[],[f5446]) ).
fof(f12488,plain,
! [X0] :
( m2_relset_1(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| ~ l2_lattices(X0) ),
inference(cnf_transformation,[],[f5447]) ).
fof(f12489,plain,
! [X0] :
( v1_funct_2(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| ~ l2_lattices(X0) ),
inference(cnf_transformation,[],[f5447]) ).
fof(f12490,plain,
! [X0] :
( v1_funct_1(u2_lattices(X0))
| ~ l2_lattices(X0) ),
inference(cnf_transformation,[],[f5447]) ).
fof(f12579,plain,
! [X0] :
( m1_filter_0(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f5495]) ).
fof(f12745,plain,
! [X0,X1] :
( ~ m1_filter_0(X1,X0)
| ~ v1_xboole_0(X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f5639]) ).
fof(f12793,plain,
! [X0] :
( ~ v3_struct_0(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f5687]) ).
fof(f12806,plain,
! [X0] :
( v1_funct_2(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v6_lattices(X0)
| ~ l1_lattices(X0) ),
inference(cnf_transformation,[],[f5693]) ).
fof(f12807,plain,
! [X0] :
( v1_funct_1(u1_lattices(X0))
| v3_struct_0(X0)
| ~ v6_lattices(X0)
| ~ l1_lattices(X0) ),
inference(cnf_transformation,[],[f5693]) ).
fof(f12814,plain,
! [X0] :
( v10_lattices(k1_lattice2(X0))
| ~ sP112(X0) ),
inference(cnf_transformation,[],[f7912]) ).
fof(f12823,plain,
! [X0] :
( ~ v10_lattices(X0)
| v3_struct_0(X0)
| sP112(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f6506]) ).
fof(f12938,plain,
! [X0] :
( ~ l3_lattices(X0)
| v3_struct_0(X0)
| u1_lattices(X0) = u2_lattices(k1_lattice2(X0)) ),
inference(cnf_transformation,[],[f5738]) ).
fof(f12940,plain,
! [X0] :
( ~ l3_lattices(X0)
| v3_struct_0(X0)
| u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0)) ),
inference(cnf_transformation,[],[f5738]) ).
fof(f12951,plain,
! [X0] :
( v1_binop_1(u2_lattices(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v4_lattices(X0)
| ~ l2_lattices(X0) ),
inference(cnf_transformation,[],[f5752]) ).
fof(f12953,plain,
! [X0] :
( v2_binop_1(u2_lattices(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v5_lattices(X0)
| ~ l2_lattices(X0) ),
inference(cnf_transformation,[],[f5756]) ).
fof(f12955,plain,
! [X0] :
( v1_binop_1(u1_lattices(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v6_lattices(X0)
| ~ l1_lattices(X0) ),
inference(cnf_transformation,[],[f5760]) ).
fof(f12956,plain,
! [X0] :
( v2_binop_1(u1_lattices(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v7_lattices(X0)
| ~ l1_lattices(X0) ),
inference(cnf_transformation,[],[f5762]) ).
fof(f12964,plain,
! [X0] :
( r1_lattice2(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f5778]) ).
fof(f12965,plain,
! [X0] :
( r1_lattice2(u1_struct_0(X0),u1_lattices(X0),u2_lattices(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f5780]) ).
fof(f13061,plain,
! [X0] :
( l3_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f5873]) ).
fof(f13323,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(cnf_transformation,[],[f6053]) ).
fof(f13371,plain,
! [X0,X1] :
( m2_lattice4(k9_filter_2(X0,X1),k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m2_lattice4(X1,X0) ),
inference(cnf_transformation,[],[f6119]) ).
fof(f13372,plain,
! [X0,X1] :
( ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| k7_filter_2(X0,X1) = k9_filter_2(X0,X1) ),
inference(cnf_transformation,[],[f6121]) ).
fof(f13401,plain,
! [X2,X3,X0,X1] :
( v2_binop_1(X3,X1)
| ~ v2_binop_1(X2,X0)
| k1_realset1(X2,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)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f6171]) ).
fof(f13403,plain,
! [X2,X3,X0,X1] :
( v1_binop_1(X3,X1)
| ~ v1_binop_1(X2,X0)
| k1_realset1(X2,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)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f6171]) ).
fof(f13410,plain,
! [X2,X3,X0,X1,X4,X5] :
( r1_lattice2(X1,X4,X5)
| k1_realset1(X2,X1) != X4
| k1_realset1(X3,X1) != X5
| ~ r1_lattice2(X0,X2,X3)
| ~ v1_funct_1(X5)
| ~ v1_funct_2(X5,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(X5,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(X4,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X3,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f6179]) ).
fof(f13465,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,[],[f6220]) ).
fof(f13627,plain,
! [X0,X1] :
( m2_relset_1(k1_realset1(u2_lattices(X0),X1),k2_zfmisc_1(X1,X1),X1)
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f6328]) ).
fof(f13628,plain,
! [X0,X1] :
( v1_funct_2(k1_realset1(u2_lattices(X0),X1),k2_zfmisc_1(X1,X1),X1)
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f6328]) ).
fof(f13629,plain,
! [X0,X1] :
( v1_funct_1(k1_realset1(u2_lattices(X0),X1))
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f6328]) ).
fof(f13630,plain,
l3_lattices(sK1079),
inference(cnf_transformation,[],[f8097]) ).
fof(f13631,plain,
v10_lattices(sK1079),
inference(cnf_transformation,[],[f8097]) ).
fof(f13632,plain,
~ v3_struct_0(sK1079),
inference(cnf_transformation,[],[f8097]) ).
fof(f13633,plain,
m2_lattice4(sK1080,sK1079),
inference(cnf_transformation,[],[f8097]) ).
fof(f13634,plain,
~ v1_xboole_0(sK1080),
inference(cnf_transformation,[],[f8097]) ).
fof(f13635,plain,
m2_relset_1(sK1081,k2_zfmisc_1(sK1080,sK1080),sK1080),
inference(cnf_transformation,[],[f8097]) ).
fof(f13636,plain,
v1_funct_2(sK1081,k2_zfmisc_1(sK1080,sK1080),sK1080),
inference(cnf_transformation,[],[f8097]) ).
fof(f13637,plain,
v1_funct_1(sK1081),
inference(cnf_transformation,[],[f8097]) ).
fof(f13638,plain,
m2_relset_1(sK1082,k2_zfmisc_1(sK1080,sK1080),sK1080),
inference(cnf_transformation,[],[f8097]) ).
fof(f13639,plain,
v1_funct_2(sK1082,k2_zfmisc_1(sK1080,sK1080),sK1080),
inference(cnf_transformation,[],[f8097]) ).
fof(f13640,plain,
v1_funct_1(sK1082),
inference(cnf_transformation,[],[f8097]) ).
fof(f13641,plain,
sK1082 = k1_realset1(u1_lattices(sK1079),sK1080),
inference(cnf_transformation,[],[f8097]) ).
fof(f13642,plain,
sK1081 = k1_realset1(u2_lattices(sK1079),sK1080),
inference(cnf_transformation,[],[f8097]) ).
fof(f13643,plain,
( ~ v1_binop_1(sK1081,sK1080)
| ~ v2_binop_1(sK1081,sK1080)
| ~ v1_binop_1(sK1082,sK1080)
| ~ v2_binop_1(sK1082,sK1080)
| ~ r1_lattice2(sK1080,sK1081,sK1082)
| ~ r1_lattice2(sK1080,sK1082,sK1081) ),
inference(cnf_transformation,[],[f8097]) ).
fof(f15533,plain,
! [X2,X0,X1] :
( ~ v1_funct_2(k1_realset1(X2,X1),k2_zfmisc_1(X1,X1),X1)
| ~ v1_binop_1(X2,X0)
| ~ v1_funct_1(k1_realset1(X2,X1))
| v1_binop_1(k1_realset1(X2,X1),X1)
| ~ m2_relset_1(k1_realset1(X2,X1),k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| v1_xboole_0(X0) ),
inference(equality_resolution,[],[f13403]) ).
fof(f15535,plain,
! [X2,X0,X1] :
( ~ v1_funct_2(k1_realset1(X2,X1),k2_zfmisc_1(X1,X1),X1)
| ~ v2_binop_1(X2,X0)
| ~ v1_funct_1(k1_realset1(X2,X1))
| v2_binop_1(k1_realset1(X2,X1),X1)
| ~ m2_relset_1(k1_realset1(X2,X1),k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| v1_xboole_0(X0) ),
inference(equality_resolution,[],[f13401]) ).
fof(f15548,plain,
! [X2,X3,X0,X1,X5] :
( r1_lattice2(X1,k1_realset1(X2,X1),X5)
| k1_realset1(X3,X1) != X5
| ~ r1_lattice2(X0,X2,X3)
| ~ v1_funct_1(X5)
| ~ v1_funct_2(X5,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(X5,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(k1_realset1(X2,X1))
| ~ v1_funct_2(k1_realset1(X2,X1),k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(k1_realset1(X2,X1),k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X3,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| v1_xboole_0(X0) ),
inference(equality_resolution,[],[f13410]) ).
fof(f15549,plain,
! [X2,X3,X0,X1] :
( ~ v1_funct_2(k1_realset1(X3,X1),k2_zfmisc_1(X1,X1),X1)
| ~ r1_lattice2(X0,X2,X3)
| ~ v1_funct_1(k1_realset1(X3,X1))
| r1_lattice2(X1,k1_realset1(X2,X1),k1_realset1(X3,X1))
| ~ m2_relset_1(k1_realset1(X3,X1),k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(k1_realset1(X2,X1))
| ~ v1_funct_2(k1_realset1(X2,X1),k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(k1_realset1(X2,X1),k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X3,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| v1_xboole_0(X0) ),
inference(equality_resolution,[],[f15548]) ).
fof(f15570,definition,
sF1083 = u2_lattices(sK1079),
introduced(definition,[new_symbols(definition,[sF1083])],[function_definition]) ).
fof(f15571,plain,
u2_lattices(sK1079) = sF1083,
inference(reorient_equations,[],[f15570]) ).
fof(f15572,definition,
sF1084 = k1_realset1(sF1083,sK1080),
introduced(definition,[new_symbols(definition,[sF1084])],[function_definition]) ).
fof(f15573,plain,
k1_realset1(sF1083,sK1080) = sF1084,
inference(reorient_equations,[],[f15572]) ).
fof(f15574,plain,
sK1081 = sF1084,
inference(definition_folding,[],[f13642,f15573,f15571]) ).
fof(f15575,definition,
sF1085 = u1_lattices(sK1079),
introduced(definition,[new_symbols(definition,[sF1085])],[function_definition]) ).
fof(f15576,plain,
u1_lattices(sK1079) = sF1085,
inference(reorient_equations,[],[f15575]) ).
fof(f15577,definition,
sF1086 = k1_realset1(sF1085,sK1080),
introduced(definition,[new_symbols(definition,[sF1086])],[function_definition]) ).
fof(f15578,plain,
k1_realset1(sF1085,sK1080) = sF1086,
inference(reorient_equations,[],[f15577]) ).
fof(f15579,plain,
sK1082 = sF1086,
inference(definition_folding,[],[f13641,f15578,f15576]) ).
fof(f15580,definition,
sF1087 = k2_zfmisc_1(sK1080,sK1080),
introduced(definition,[new_symbols(definition,[sF1087])],[function_definition]) ).
fof(f15581,plain,
k2_zfmisc_1(sK1080,sK1080) = sF1087,
inference(reorient_equations,[],[f15580]) ).
fof(f15582,plain,
v1_funct_2(sK1082,sF1087,sK1080),
inference(definition_folding,[],[f13639,f15581]) ).
fof(f15583,plain,
m2_relset_1(sK1082,sF1087,sK1080),
inference(definition_folding,[],[f13638,f15581]) ).
fof(f15584,plain,
v1_funct_2(sK1081,sF1087,sK1080),
inference(definition_folding,[],[f13636,f15581]) ).
fof(f15585,plain,
m2_relset_1(sK1081,sF1087,sK1080),
inference(definition_folding,[],[f13635,f15581]) ).
fof(f15649,definition,
( spl1088_1
<=> r1_lattice2(sK1080,sK1082,sK1081) ),
introduced(definition,[new_symbols(definition,[spl1088_1])],[avatar_definition]) ).
fof(f15651,plain,
( ~ r1_lattice2(sK1080,sK1082,sK1081)
| spl1088_1 ),
inference(avatar_component_clause,[],[f15649]) ).
fof(f15653,definition,
( spl1088_2
<=> r1_lattice2(sK1080,sK1081,sK1082) ),
introduced(definition,[new_symbols(definition,[spl1088_2])],[avatar_definition]) ).
fof(f15655,plain,
( ~ r1_lattice2(sK1080,sK1081,sK1082)
| spl1088_2 ),
inference(avatar_component_clause,[],[f15653]) ).
fof(f15657,definition,
( spl1088_3
<=> v2_binop_1(sK1082,sK1080) ),
introduced(definition,[new_symbols(definition,[spl1088_3])],[avatar_definition]) ).
fof(f15661,definition,
( spl1088_4
<=> v1_binop_1(sK1082,sK1080) ),
introduced(definition,[new_symbols(definition,[spl1088_4])],[avatar_definition]) ).
fof(f15663,plain,
( ~ v1_binop_1(sK1082,sK1080)
| spl1088_4 ),
inference(avatar_component_clause,[],[f15661]) ).
fof(f15665,definition,
( spl1088_5
<=> v2_binop_1(sK1081,sK1080) ),
introduced(definition,[new_symbols(definition,[spl1088_5])],[avatar_definition]) ).
fof(f15669,definition,
( spl1088_6
<=> v1_binop_1(sK1081,sK1080) ),
introduced(definition,[new_symbols(definition,[spl1088_6])],[avatar_definition]) ).
fof(f15672,plain,
( ~ spl1088_1
| ~ spl1088_2
| ~ spl1088_3
| ~ spl1088_4
| ~ spl1088_5
| ~ spl1088_6 ),
inference(avatar_split_clause,[],[f13643,f15669,f15665,f15661,f15657,f15653,f15649]) ).
fof(f17549,plain,
sK1081 = k1_realset1(sF1083,sK1080),
inference(forward_demodulation,[],[f15573,f15574]) ).
fof(f17550,plain,
sK1082 = k1_realset1(sF1085,sK1080),
inference(forward_demodulation,[],[f15578,f15579]) ).
fof(f18155,plain,
! [X0,X1] :
( ~ v1_funct_2(sK1081,k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ r1_lattice2(X0,X1,sF1083)
| ~ v1_funct_1(sK1081)
| r1_lattice2(sK1080,k1_realset1(X1,sK1080),sK1081)
| ~ m2_relset_1(sK1081,k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ v1_funct_1(k1_realset1(X1,sK1080))
| ~ v1_funct_2(k1_realset1(X1,sK1080),k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ m2_relset_1(k1_realset1(X1,sK1080),k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ v1_funct_1(sF1083)
| ~ v1_funct_2(sF1083,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(sF1083,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| v1_xboole_0(sK1080)
| ~ m1_subset_1(sK1080,k1_zfmisc_1(X0))
| v1_xboole_0(X0) ),
inference(superposition,[],[f15549,f17549]) ).
fof(f18173,plain,
! [X0] :
( ~ v1_funct_2(sK1081,k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ v2_binop_1(sF1083,X0)
| ~ v1_funct_1(sK1081)
| v2_binop_1(sK1081,sK1080)
| ~ m2_relset_1(sK1081,k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ v1_funct_1(sF1083)
| ~ v1_funct_2(sF1083,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(sF1083,k2_zfmisc_1(X0,X0),X0)
| v1_xboole_0(sK1080)
| ~ m1_subset_1(sK1080,k1_zfmisc_1(X0))
| v1_xboole_0(X0) ),
inference(superposition,[],[f15535,f17549]) ).
fof(f18174,plain,
! [X0] :
( ~ v1_funct_2(sK1082,k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ v2_binop_1(sF1085,X0)
| ~ v1_funct_1(sK1082)
| v2_binop_1(sK1082,sK1080)
| ~ m2_relset_1(sK1082,k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ v1_funct_1(sF1085)
| ~ v1_funct_2(sF1085,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(sF1085,k2_zfmisc_1(X0,X0),X0)
| v1_xboole_0(sK1080)
| ~ m1_subset_1(sK1080,k1_zfmisc_1(X0))
| v1_xboole_0(X0) ),
inference(superposition,[],[f15535,f17550]) ).
fof(f18176,plain,
! [X0] :
( ~ v1_funct_2(sK1081,k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ v1_binop_1(sF1083,X0)
| ~ v1_funct_1(sK1081)
| v1_binop_1(sK1081,sK1080)
| ~ m2_relset_1(sK1081,k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ v1_funct_1(sF1083)
| ~ v1_funct_2(sF1083,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(sF1083,k2_zfmisc_1(X0,X0),X0)
| v1_xboole_0(sK1080)
| ~ m1_subset_1(sK1080,k1_zfmisc_1(X0))
| v1_xboole_0(X0) ),
inference(superposition,[],[f15533,f17549]) ).
fof(f18177,plain,
! [X0] :
( ~ v1_funct_2(sK1082,k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ v1_binop_1(sF1085,X0)
| ~ v1_funct_1(sK1082)
| v1_binop_1(sK1082,sK1080)
| ~ m2_relset_1(sK1082,k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ v1_funct_1(sF1085)
| ~ v1_funct_2(sF1085,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(sF1085,k2_zfmisc_1(X0,X0),X0)
| v1_xboole_0(sK1080)
| ~ m1_subset_1(sK1080,k1_zfmisc_1(X0))
| v1_xboole_0(X0) ),
inference(superposition,[],[f15533,f17550]) ).
fof(f18192,plain,
! [X2,X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m2_lattice4(X0,X1)
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| ~ r1_lattice2(X2,X3,u2_lattices(X1))
| ~ v1_funct_1(k1_realset1(u2_lattices(X1),X0))
| r1_lattice2(X0,k1_realset1(X3,X0),k1_realset1(u2_lattices(X1),X0))
| ~ m2_relset_1(k1_realset1(u2_lattices(X1),X0),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(k1_realset1(X3,X0))
| ~ v1_funct_2(k1_realset1(X3,X0),k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(k1_realset1(X3,X0),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(u2_lattices(X1))
| ~ v1_funct_2(u2_lattices(X1),k2_zfmisc_1(X2,X2),X2)
| ~ m2_relset_1(u2_lattices(X1),k2_zfmisc_1(X2,X2),X2)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,k2_zfmisc_1(X2,X2),X2)
| ~ m2_relset_1(X3,k2_zfmisc_1(X2,X2),X2)
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(X2))
| v1_xboole_0(X2) ),
inference(resolution,[],[f13628,f15549]) ).
fof(f18195,plain,
! [X2,X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m2_lattice4(X0,X1)
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| ~ r1_lattice2(X2,X3,u2_lattices(X1))
| ~ v1_funct_1(k1_realset1(u2_lattices(X1),X0))
| r1_lattice2(X0,k1_realset1(X3,X0),k1_realset1(u2_lattices(X1),X0))
| ~ m2_relset_1(k1_realset1(u2_lattices(X1),X0),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(k1_realset1(X3,X0))
| ~ v1_funct_2(k1_realset1(X3,X0),k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(k1_realset1(X3,X0),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(u2_lattices(X1))
| ~ v1_funct_2(u2_lattices(X1),k2_zfmisc_1(X2,X2),X2)
| ~ m2_relset_1(u2_lattices(X1),k2_zfmisc_1(X2,X2),X2)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,k2_zfmisc_1(X2,X2),X2)
| ~ m2_relset_1(X3,k2_zfmisc_1(X2,X2),X2)
| ~ m1_subset_1(X0,k1_zfmisc_1(X2))
| v1_xboole_0(X2) ),
inference(duplicate_literal_removal,[],[f18192]) ).
fof(f18210,plain,
( v2_binop_1(sF1083,u1_struct_0(sK1079))
| v3_struct_0(sK1079)
| ~ v5_lattices(sK1079)
| ~ l2_lattices(sK1079) ),
inference(superposition,[],[f12953,f15571]) ).
fof(f18211,plain,
( v2_binop_1(sF1083,u1_struct_0(sK1079))
| ~ v5_lattices(sK1079)
| ~ l2_lattices(sK1079) ),
inference(forward_subsumption_resolution,[],[f18210,f13632]) ).
fof(f18213,definition,
( spl1088_347
<=> l2_lattices(sK1079) ),
introduced(definition,[new_symbols(definition,[spl1088_347])],[avatar_definition]) ).
fof(f18214,plain,
( l2_lattices(sK1079)
| ~ spl1088_347 ),
inference(avatar_component_clause,[],[f18213]) ).
fof(f18215,plain,
( ~ l2_lattices(sK1079)
| spl1088_347 ),
inference(avatar_component_clause,[],[f18213]) ).
fof(f18217,definition,
( spl1088_348
<=> v5_lattices(sK1079) ),
introduced(definition,[new_symbols(definition,[spl1088_348])],[avatar_definition]) ).
fof(f18219,plain,
( ~ v5_lattices(sK1079)
| spl1088_348 ),
inference(avatar_component_clause,[],[f18217]) ).
fof(f18221,definition,
( spl1088_349
<=> v2_binop_1(sF1083,u1_struct_0(sK1079)) ),
introduced(definition,[new_symbols(definition,[spl1088_349])],[avatar_definition]) ).
fof(f18223,plain,
( v2_binop_1(sF1083,u1_struct_0(sK1079))
| ~ spl1088_349 ),
inference(avatar_component_clause,[],[f18221]) ).
fof(f18224,plain,
( ~ spl1088_347
| ~ spl1088_348
| spl1088_349 ),
inference(avatar_split_clause,[],[f18211,f18221,f18217,f18213]) ).
fof(f18225,plain,
( v2_binop_1(sF1085,u1_struct_0(sK1079))
| v3_struct_0(sK1079)
| ~ v7_lattices(sK1079)
| ~ l1_lattices(sK1079) ),
inference(superposition,[],[f12956,f15576]) ).
fof(f18226,plain,
( v2_binop_1(sF1085,u1_struct_0(sK1079))
| ~ v7_lattices(sK1079)
| ~ l1_lattices(sK1079) ),
inference(forward_subsumption_resolution,[],[f18225,f13632]) ).
fof(f18228,definition,
( spl1088_350
<=> l1_lattices(sK1079) ),
introduced(definition,[new_symbols(definition,[spl1088_350])],[avatar_definition]) ).
fof(f18229,plain,
( l1_lattices(sK1079)
| ~ spl1088_350 ),
inference(avatar_component_clause,[],[f18228]) ).
fof(f18230,plain,
( ~ l1_lattices(sK1079)
| spl1088_350 ),
inference(avatar_component_clause,[],[f18228]) ).
fof(f18232,definition,
( spl1088_351
<=> v7_lattices(sK1079) ),
introduced(definition,[new_symbols(definition,[spl1088_351])],[avatar_definition]) ).
fof(f18234,plain,
( ~ v7_lattices(sK1079)
| spl1088_351 ),
inference(avatar_component_clause,[],[f18232]) ).
fof(f18236,definition,
( spl1088_352
<=> v2_binop_1(sF1085,u1_struct_0(sK1079)) ),
introduced(definition,[new_symbols(definition,[spl1088_352])],[avatar_definition]) ).
fof(f18238,plain,
( v2_binop_1(sF1085,u1_struct_0(sK1079))
| ~ spl1088_352 ),
inference(avatar_component_clause,[],[f18236]) ).
fof(f18239,plain,
( ~ spl1088_350
| ~ spl1088_351
| spl1088_352 ),
inference(avatar_split_clause,[],[f18226,f18236,f18232,f18228]) ).
fof(f18247,plain,
( v1_binop_1(sF1083,u1_struct_0(sK1079))
| v3_struct_0(sK1079)
| ~ v4_lattices(sK1079)
| ~ l2_lattices(sK1079) ),
inference(superposition,[],[f12951,f15571]) ).
fof(f18248,plain,
( v1_binop_1(sF1085,u1_struct_0(sK1079))
| v3_struct_0(sK1079)
| ~ v6_lattices(sK1079)
| ~ l1_lattices(sK1079) ),
inference(superposition,[],[f12955,f15576]) ).
fof(f18322,definition,
( spl1088_355
<=> v3_struct_0(k1_lattice2(sK1079)) ),
introduced(definition,[new_symbols(definition,[spl1088_355])],[avatar_definition]) ).
fof(f18323,plain,
( ~ v3_struct_0(k1_lattice2(sK1079))
| spl1088_355 ),
inference(avatar_component_clause,[],[f18322]) ).
fof(f18324,plain,
( v3_struct_0(k1_lattice2(sK1079))
| ~ spl1088_355 ),
inference(avatar_component_clause,[],[f18322]) ).
fof(f18382,plain,
( v3_struct_0(sK1079)
| u1_lattices(sK1079) = u2_lattices(k1_lattice2(sK1079)) ),
inference(resolution,[],[f12938,f13630]) ).
fof(f18383,plain,
u1_lattices(sK1079) = u2_lattices(k1_lattice2(sK1079)),
inference(forward_subsumption_resolution,[],[f18382,f13632]) ).
fof(f18384,plain,
sF1085 = u2_lattices(k1_lattice2(sK1079)),
inference(forward_demodulation,[],[f18383,f15576]) ).
fof(f18430,plain,
( r1_lattice2(u1_struct_0(sK1079),u2_lattices(sK1079),sF1085)
| v3_struct_0(sK1079)
| ~ v10_lattices(sK1079)
| ~ l3_lattices(sK1079) ),
inference(superposition,[],[f12964,f15576]) ).
fof(f18433,plain,
( r1_lattice2(u1_struct_0(sK1079),u2_lattices(sK1079),sF1085)
| ~ v10_lattices(sK1079)
| ~ l3_lattices(sK1079) ),
inference(forward_subsumption_resolution,[],[f18430,f13632]) ).
fof(f18437,definition,
( spl1088_364
<=> l3_lattices(k1_lattice2(sK1079)) ),
introduced(definition,[new_symbols(definition,[spl1088_364])],[avatar_definition]) ).
fof(f18438,plain,
( l3_lattices(k1_lattice2(sK1079))
| ~ spl1088_364 ),
inference(avatar_component_clause,[],[f18437]) ).
fof(f18439,plain,
( ~ l3_lattices(k1_lattice2(sK1079))
| spl1088_364 ),
inference(avatar_component_clause,[],[f18437]) ).
fof(f18441,definition,
( spl1088_365
<=> v10_lattices(k1_lattice2(sK1079)) ),
introduced(definition,[new_symbols(definition,[spl1088_365])],[avatar_definition]) ).
fof(f18442,plain,
( v10_lattices(k1_lattice2(sK1079))
| ~ spl1088_365 ),
inference(avatar_component_clause,[],[f18441]) ).
fof(f18443,plain,
( ~ v10_lattices(k1_lattice2(sK1079))
| spl1088_365 ),
inference(avatar_component_clause,[],[f18441]) ).
fof(f18449,plain,
( r1_lattice2(u1_struct_0(sK1079),u2_lattices(sK1079),sF1085)
| ~ l3_lattices(sK1079) ),
inference(forward_subsumption_resolution,[],[f18433,f13631]) ).
fof(f18452,plain,
r1_lattice2(u1_struct_0(sK1079),u2_lattices(sK1079),sF1085),
inference(forward_subsumption_resolution,[],[f18449,f13630]) ).
fof(f18454,plain,
r1_lattice2(u1_struct_0(sK1079),sF1083,sF1085),
inference(forward_demodulation,[],[f18452,f15571]) ).
fof(f18458,plain,
( r1_lattice2(u1_struct_0(sK1079),u1_lattices(sK1079),sF1083)
| v3_struct_0(sK1079)
| ~ v10_lattices(sK1079)
| ~ l3_lattices(sK1079) ),
inference(superposition,[],[f12965,f15571]) ).
fof(f18460,plain,
( r1_lattice2(u1_struct_0(sK1079),u1_lattices(sK1079),sF1083)
| ~ v10_lattices(sK1079)
| ~ l3_lattices(sK1079) ),
inference(forward_subsumption_resolution,[],[f18458,f13632]) ).
fof(f18462,plain,
( r1_lattice2(u1_struct_0(sK1079),u1_lattices(sK1079),sF1083)
| ~ l3_lattices(sK1079) ),
inference(forward_subsumption_resolution,[],[f18460,f13631]) ).
fof(f18464,plain,
r1_lattice2(u1_struct_0(sK1079),u1_lattices(sK1079),sF1083),
inference(forward_subsumption_resolution,[],[f18462,f13630]) ).
fof(f18466,plain,
r1_lattice2(u1_struct_0(sK1079),sF1085,sF1083),
inference(forward_demodulation,[],[f18464,f15576]) ).
fof(f18468,plain,
l2_lattices(sK1079),
inference(resolution,[],[f12465,f13630]) ).
fof(f18469,plain,
( $false
| spl1088_347 ),
inference(forward_subsumption_resolution,[],[f18468,f18215]) ).
fof(f18470,plain,
spl1088_347,
inference(avatar_contradiction_clause,[],[f18469]) ).
fof(f18471,plain,
( v1_binop_1(sF1083,u1_struct_0(sK1079))
| ~ v4_lattices(sK1079)
| ~ l2_lattices(sK1079) ),
inference(forward_subsumption_resolution,[],[f18247,f13632]) ).
fof(f18472,plain,
( v1_binop_1(sF1083,u1_struct_0(sK1079))
| ~ v4_lattices(sK1079)
| ~ spl1088_347 ),
inference(forward_subsumption_resolution,[],[f18471,f18214]) ).
fof(f18474,definition,
( spl1088_367
<=> v4_lattices(sK1079) ),
introduced(definition,[new_symbols(definition,[spl1088_367])],[avatar_definition]) ).
fof(f18476,plain,
( ~ v4_lattices(sK1079)
| spl1088_367 ),
inference(avatar_component_clause,[],[f18474]) ).
fof(f18478,definition,
( spl1088_368
<=> v1_binop_1(sF1083,u1_struct_0(sK1079)) ),
introduced(definition,[new_symbols(definition,[spl1088_368])],[avatar_definition]) ).
fof(f18480,plain,
( v1_binop_1(sF1083,u1_struct_0(sK1079))
| ~ spl1088_368 ),
inference(avatar_component_clause,[],[f18478]) ).
fof(f18481,plain,
( ~ spl1088_367
| spl1088_368
| ~ spl1088_347 ),
inference(avatar_split_clause,[],[f18472,f18213,f18478,f18474]) ).
fof(f18489,plain,
( v1_funct_2(sF1083,k2_zfmisc_1(u1_struct_0(sK1079),u1_struct_0(sK1079)),u1_struct_0(sK1079))
| ~ l2_lattices(sK1079) ),
inference(superposition,[],[f12489,f15571]) ).
fof(f18491,plain,
( v1_funct_2(sF1083,k2_zfmisc_1(u1_struct_0(sK1079),u1_struct_0(sK1079)),u1_struct_0(sK1079))
| ~ spl1088_347 ),
inference(forward_subsumption_resolution,[],[f18489,f18214]) ).
fof(f18496,plain,
( v1_funct_1(sF1083)
| ~ l2_lattices(sK1079) ),
inference(superposition,[],[f12490,f15571]) ).
fof(f18498,plain,
( v1_funct_1(sF1083)
| ~ spl1088_347 ),
inference(forward_subsumption_resolution,[],[f18496,f18214]) ).
fof(f18508,plain,
( v1_funct_1(sF1085)
| ~ l1_lattices(sK1079) ),
inference(superposition,[],[f12487,f15576]) ).
fof(f18512,plain,
( m2_relset_1(sF1083,k2_zfmisc_1(u1_struct_0(sK1079),u1_struct_0(sK1079)),u1_struct_0(sK1079))
| ~ l2_lattices(sK1079) ),
inference(superposition,[],[f12488,f15571]) ).
fof(f18514,plain,
( m2_relset_1(sF1083,k2_zfmisc_1(u1_struct_0(sK1079),u1_struct_0(sK1079)),u1_struct_0(sK1079))
| ~ spl1088_347 ),
inference(forward_subsumption_resolution,[],[f18512,f18214]) ).
fof(f18522,plain,
( v1_funct_2(sF1085,k2_zfmisc_1(u1_struct_0(sK1079),u1_struct_0(sK1079)),u1_struct_0(sK1079))
| ~ l1_lattices(sK1079) ),
inference(superposition,[],[f12486,f15576]) ).
fof(f18528,plain,
l1_lattices(sK1079),
inference(resolution,[],[f12466,f13630]) ).
fof(f18529,plain,
( $false
| spl1088_350 ),
inference(forward_subsumption_resolution,[],[f18528,f18230]) ).
fof(f18530,plain,
spl1088_350,
inference(avatar_contradiction_clause,[],[f18529]) ).
fof(f18531,plain,
( v1_binop_1(sF1085,u1_struct_0(sK1079))
| ~ v6_lattices(sK1079)
| ~ l1_lattices(sK1079) ),
inference(forward_subsumption_resolution,[],[f18248,f13632]) ).
fof(f18532,plain,
( v1_funct_1(sF1085)
| ~ spl1088_350 ),
inference(forward_subsumption_resolution,[],[f18508,f18229]) ).
fof(f18533,plain,
( v1_funct_2(sF1085,k2_zfmisc_1(u1_struct_0(sK1079),u1_struct_0(sK1079)),u1_struct_0(sK1079))
| ~ spl1088_350 ),
inference(forward_subsumption_resolution,[],[f18522,f18229]) ).
fof(f18534,plain,
( v1_binop_1(sF1085,u1_struct_0(sK1079))
| ~ v6_lattices(sK1079)
| ~ spl1088_350 ),
inference(forward_subsumption_resolution,[],[f18531,f18229]) ).
fof(f18536,definition,
( spl1088_369
<=> v6_lattices(sK1079) ),
introduced(definition,[new_symbols(definition,[spl1088_369])],[avatar_definition]) ).
fof(f18537,plain,
( v6_lattices(sK1079)
| ~ spl1088_369 ),
inference(avatar_component_clause,[],[f18536]) ).
fof(f18538,plain,
( ~ v6_lattices(sK1079)
| spl1088_369 ),
inference(avatar_component_clause,[],[f18536]) ).
fof(f18540,definition,
( spl1088_370
<=> v1_binop_1(sF1085,u1_struct_0(sK1079)) ),
introduced(definition,[new_symbols(definition,[spl1088_370])],[avatar_definition]) ).
fof(f18542,plain,
( v1_binop_1(sF1085,u1_struct_0(sK1079))
| ~ spl1088_370 ),
inference(avatar_component_clause,[],[f18540]) ).
fof(f18543,plain,
( ~ spl1088_369
| spl1088_370
| ~ spl1088_350 ),
inference(avatar_split_clause,[],[f18534,f18228,f18540,f18536]) ).
fof(f18544,plain,
( v3_struct_0(sK1079)
| ~ v10_lattices(sK1079)
| ~ l3_lattices(sK1079)
| k7_filter_2(sK1079,sK1080) = k9_filter_2(sK1079,sK1080) ),
inference(resolution,[],[f13372,f13633]) ).
fof(f18545,plain,
( ~ v10_lattices(sK1079)
| ~ l3_lattices(sK1079)
| k7_filter_2(sK1079,sK1080) = k9_filter_2(sK1079,sK1080) ),
inference(forward_subsumption_resolution,[],[f18544,f13632]) ).
fof(f18546,plain,
( ~ l3_lattices(sK1079)
| k7_filter_2(sK1079,sK1080) = k9_filter_2(sK1079,sK1080) ),
inference(forward_subsumption_resolution,[],[f18545,f13631]) ).
fof(f18547,plain,
k7_filter_2(sK1079,sK1080) = k9_filter_2(sK1079,sK1080),
inference(forward_subsumption_resolution,[],[f18546,f13630]) ).
fof(f18550,plain,
( m2_relset_1(sF1085,k2_zfmisc_1(u1_struct_0(sK1079),u1_struct_0(sK1079)),u1_struct_0(sK1079))
| ~ l1_lattices(sK1079) ),
inference(superposition,[],[f12485,f15576]) ).
fof(f18552,plain,
( m2_relset_1(sF1085,k2_zfmisc_1(u1_struct_0(sK1079),u1_struct_0(sK1079)),u1_struct_0(sK1079))
| ~ spl1088_350 ),
inference(forward_subsumption_resolution,[],[f18550,f18229]) ).
fof(f18870,plain,
( v3_struct_0(sK1079)
| u1_struct_0(sK1079) = u1_struct_0(k1_lattice2(sK1079)) ),
inference(resolution,[],[f12940,f13630]) ).
fof(f18871,plain,
u1_struct_0(sK1079) = u1_struct_0(k1_lattice2(sK1079)),
inference(forward_subsumption_resolution,[],[f18870,f13632]) ).
fof(f18959,plain,
( ~ l3_lattices(sK1079)
| spl1088_364 ),
inference(resolution,[],[f13061,f18439]) ).
fof(f18965,plain,
( $false
| spl1088_364 ),
inference(forward_subsumption_resolution,[],[f18959,f13630]) ).
fof(f18966,plain,
spl1088_364,
inference(avatar_contradiction_clause,[],[f18965]) ).
fof(f19010,plain,
( v3_struct_0(sK1079)
| ~ l3_lattices(sK1079)
| ~ spl1088_355 ),
inference(resolution,[],[f18324,f12793]) ).
fof(f19011,plain,
( ~ l3_lattices(sK1079)
| ~ spl1088_355 ),
inference(forward_subsumption_resolution,[],[f19010,f13632]) ).
fof(f19012,plain,
( $false
| ~ spl1088_355 ),
inference(forward_subsumption_resolution,[],[f19011,f13630]) ).
fof(f19013,plain,
~ spl1088_355,
inference(avatar_contradiction_clause,[],[f19012]) ).
fof(f19014,plain,
( v3_struct_0(sK1079)
| sP112(sK1079)
| ~ l3_lattices(sK1079) ),
inference(resolution,[],[f12823,f13631]) ).
fof(f19015,plain,
( sP112(sK1079)
| ~ l3_lattices(sK1079) ),
inference(forward_subsumption_resolution,[],[f19014,f13632]) ).
fof(f19016,plain,
sP112(sK1079),
inference(forward_subsumption_resolution,[],[f19015,f13630]) ).
fof(f19583,plain,
( m2_lattice4(k7_filter_2(sK1079,sK1080),k1_lattice2(sK1079))
| v3_struct_0(sK1079)
| ~ v10_lattices(sK1079)
| ~ l3_lattices(sK1079)
| ~ m2_lattice4(sK1080,sK1079) ),
inference(superposition,[],[f13371,f18547]) ).
fof(f19584,plain,
( m2_lattice4(k7_filter_2(sK1079,sK1080),k1_lattice2(sK1079))
| ~ v10_lattices(sK1079)
| ~ l3_lattices(sK1079)
| ~ m2_lattice4(sK1080,sK1079) ),
inference(forward_subsumption_resolution,[],[f19583,f13632]) ).
fof(f19586,plain,
( m2_lattice4(k7_filter_2(sK1079,sK1080),k1_lattice2(sK1079))
| ~ l3_lattices(sK1079)
| ~ m2_lattice4(sK1080,sK1079) ),
inference(forward_subsumption_resolution,[],[f19584,f13631]) ).
fof(f19588,plain,
( m2_lattice4(k7_filter_2(sK1079,sK1080),k1_lattice2(sK1079))
| ~ m2_lattice4(sK1080,sK1079) ),
inference(forward_subsumption_resolution,[],[f19586,f13630]) ).
fof(f19589,plain,
m2_lattice4(k7_filter_2(sK1079,sK1080),k1_lattice2(sK1079)),
inference(forward_subsumption_resolution,[],[f19588,f13633]) ).
fof(f19728,plain,
( v4_lattices(sK1079)
| v3_struct_0(sK1079)
| ~ l3_lattices(sK1079) ),
inference(resolution,[],[f12374,f13631]) ).
fof(f19729,plain,
( v3_struct_0(sK1079)
| ~ l3_lattices(sK1079)
| spl1088_367 ),
inference(forward_subsumption_resolution,[],[f19728,f18476]) ).
fof(f19730,plain,
( ~ l3_lattices(sK1079)
| spl1088_367 ),
inference(forward_subsumption_resolution,[],[f19729,f13632]) ).
fof(f19731,plain,
( $false
| spl1088_367 ),
inference(forward_subsumption_resolution,[],[f19730,f13630]) ).
fof(f19732,plain,
spl1088_367,
inference(avatar_contradiction_clause,[],[f19731]) ).
fof(f19775,plain,
( v7_lattices(sK1079)
| v3_struct_0(sK1079)
| ~ l3_lattices(sK1079) ),
inference(resolution,[],[f12370,f13631]) ).
fof(f19776,plain,
( v3_struct_0(sK1079)
| ~ l3_lattices(sK1079)
| spl1088_351 ),
inference(forward_subsumption_resolution,[],[f19775,f18234]) ).
fof(f19777,plain,
( ~ l3_lattices(sK1079)
| spl1088_351 ),
inference(forward_subsumption_resolution,[],[f19776,f13632]) ).
fof(f19778,plain,
( $false
| spl1088_351 ),
inference(forward_subsumption_resolution,[],[f19777,f13630]) ).
fof(f19779,plain,
spl1088_351,
inference(avatar_contradiction_clause,[],[f19778]) ).
fof(f19789,plain,
( v5_lattices(sK1079)
| v3_struct_0(sK1079)
| ~ l3_lattices(sK1079) ),
inference(resolution,[],[f12373,f13631]) ).
fof(f19790,plain,
( v3_struct_0(sK1079)
| ~ l3_lattices(sK1079)
| spl1088_348 ),
inference(forward_subsumption_resolution,[],[f19789,f18219]) ).
fof(f19791,plain,
( ~ l3_lattices(sK1079)
| spl1088_348 ),
inference(forward_subsumption_resolution,[],[f19790,f13632]) ).
fof(f19792,plain,
( $false
| spl1088_348 ),
inference(forward_subsumption_resolution,[],[f19791,f13630]) ).
fof(f19793,plain,
spl1088_348,
inference(avatar_contradiction_clause,[],[f19792]) ).
fof(f20083,plain,
( ~ sP112(sK1079)
| spl1088_365 ),
inference(resolution,[],[f12814,f18443]) ).
fof(f20093,plain,
( $false
| spl1088_365 ),
inference(forward_subsumption_resolution,[],[f20083,f19016]) ).
fof(f20094,plain,
spl1088_365,
inference(avatar_contradiction_clause,[],[f20093]) ).
fof(f20258,plain,
( v6_lattices(sK1079)
| v3_struct_0(sK1079)
| ~ l3_lattices(sK1079) ),
inference(resolution,[],[f12371,f13631]) ).
fof(f20262,plain,
( v3_struct_0(sK1079)
| ~ l3_lattices(sK1079)
| spl1088_369 ),
inference(forward_subsumption_resolution,[],[f20258,f18538]) ).
fof(f20264,plain,
( ~ l3_lattices(sK1079)
| spl1088_369 ),
inference(forward_subsumption_resolution,[],[f20262,f13632]) ).
fof(f20267,plain,
( $false
| spl1088_369 ),
inference(forward_subsumption_resolution,[],[f20264,f13630]) ).
fof(f20268,plain,
spl1088_369,
inference(avatar_contradiction_clause,[],[f20267]) ).
fof(f20350,plain,
! [X0,X1] :
( k7_filter_2(X0,X1) = X1
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(resolution,[],[f13465,f13323]) ).
fof(f20354,plain,
! [X0,X1] :
( ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| k7_filter_2(X0,X1) = X1 ),
inference(duplicate_literal_removal,[],[f20350]) ).
fof(f20366,plain,
( v3_struct_0(sK1079)
| ~ v10_lattices(sK1079)
| ~ l3_lattices(sK1079)
| sK1080 = k7_filter_2(sK1079,sK1080) ),
inference(resolution,[],[f20354,f13633]) ).
fof(f20367,plain,
( ~ v10_lattices(sK1079)
| ~ l3_lattices(sK1079)
| sK1080 = k7_filter_2(sK1079,sK1080) ),
inference(forward_subsumption_resolution,[],[f20366,f13632]) ).
fof(f20370,plain,
( ~ l3_lattices(sK1079)
| sK1080 = k7_filter_2(sK1079,sK1080) ),
inference(forward_subsumption_resolution,[],[f20367,f13631]) ).
fof(f20373,plain,
sK1080 = k7_filter_2(sK1079,sK1080),
inference(forward_subsumption_resolution,[],[f20370,f13630]) ).
fof(f20376,plain,
m2_lattice4(sK1080,k1_lattice2(sK1079)),
inference(superposition,[],[f19589,f20373]) ).
fof(f21144,plain,
( m1_filter_0(u1_struct_0(sK1079),k1_lattice2(sK1079))
| v3_struct_0(k1_lattice2(sK1079))
| ~ v10_lattices(k1_lattice2(sK1079))
| ~ l3_lattices(k1_lattice2(sK1079)) ),
inference(superposition,[],[f12579,f18871]) ).
fof(f21156,plain,
( m1_filter_0(u1_struct_0(sK1079),k1_lattice2(sK1079))
| ~ v10_lattices(k1_lattice2(sK1079))
| ~ l3_lattices(k1_lattice2(sK1079))
| spl1088_355 ),
inference(forward_subsumption_resolution,[],[f21144,f18323]) ).
fof(f21159,plain,
( m1_filter_0(u1_struct_0(sK1079),k1_lattice2(sK1079))
| ~ l3_lattices(k1_lattice2(sK1079))
| spl1088_355
| ~ spl1088_365 ),
inference(forward_subsumption_resolution,[],[f21156,f18442]) ).
fof(f21161,plain,
( m1_filter_0(u1_struct_0(sK1079),k1_lattice2(sK1079))
| spl1088_355
| ~ spl1088_364
| ~ spl1088_365 ),
inference(forward_subsumption_resolution,[],[f21159,f18438]) ).
fof(f21243,plain,
( ~ v1_xboole_0(u1_struct_0(sK1079))
| v3_struct_0(k1_lattice2(sK1079))
| ~ v10_lattices(k1_lattice2(sK1079))
| ~ l3_lattices(k1_lattice2(sK1079))
| spl1088_355
| ~ spl1088_364
| ~ spl1088_365 ),
inference(resolution,[],[f21161,f12745]) ).
fof(f21271,plain,
! [X0,X1] :
( ~ v1_funct_2(sK1081,k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ r1_lattice2(X0,X1,sF1083)
| r1_lattice2(sK1080,k1_realset1(X1,sK1080),sK1081)
| ~ m2_relset_1(sK1081,k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ v1_funct_1(k1_realset1(X1,sK1080))
| ~ v1_funct_2(k1_realset1(X1,sK1080),k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ m2_relset_1(k1_realset1(X1,sK1080),k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ v1_funct_1(sF1083)
| ~ v1_funct_2(sF1083,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(sF1083,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| v1_xboole_0(sK1080)
| ~ m1_subset_1(sK1080,k1_zfmisc_1(X0))
| v1_xboole_0(X0) ),
inference(forward_subsumption_resolution,[],[f18155,f13637]) ).
fof(f21278,plain,
! [X0] :
( ~ v1_funct_2(sK1082,k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ v2_binop_1(sF1085,X0)
| v2_binop_1(sK1082,sK1080)
| ~ m2_relset_1(sK1082,k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ v1_funct_1(sF1085)
| ~ v1_funct_2(sF1085,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(sF1085,k2_zfmisc_1(X0,X0),X0)
| v1_xboole_0(sK1080)
| ~ m1_subset_1(sK1080,k1_zfmisc_1(X0))
| v1_xboole_0(X0) ),
inference(forward_subsumption_resolution,[],[f18174,f13640]) ).
fof(f21279,plain,
! [X0] :
( ~ v1_funct_2(sK1081,k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ v2_binop_1(sF1083,X0)
| v2_binop_1(sK1081,sK1080)
| ~ m2_relset_1(sK1081,k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ v1_funct_1(sF1083)
| ~ v1_funct_2(sF1083,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(sF1083,k2_zfmisc_1(X0,X0),X0)
| v1_xboole_0(sK1080)
| ~ m1_subset_1(sK1080,k1_zfmisc_1(X0))
| v1_xboole_0(X0) ),
inference(forward_subsumption_resolution,[],[f18173,f13637]) ).
fof(f21281,plain,
! [X0] :
( ~ v1_funct_2(sK1082,k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ v1_binop_1(sF1085,X0)
| v1_binop_1(sK1082,sK1080)
| ~ m2_relset_1(sK1082,k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ v1_funct_1(sF1085)
| ~ v1_funct_2(sF1085,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(sF1085,k2_zfmisc_1(X0,X0),X0)
| v1_xboole_0(sK1080)
| ~ m1_subset_1(sK1080,k1_zfmisc_1(X0))
| v1_xboole_0(X0) ),
inference(forward_subsumption_resolution,[],[f18177,f13640]) ).
fof(f21282,plain,
! [X0] :
( ~ v1_funct_2(sK1081,k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ v1_binop_1(sF1083,X0)
| v1_binop_1(sK1081,sK1080)
| ~ m2_relset_1(sK1081,k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ v1_funct_1(sF1083)
| ~ v1_funct_2(sF1083,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(sF1083,k2_zfmisc_1(X0,X0),X0)
| v1_xboole_0(sK1080)
| ~ m1_subset_1(sK1080,k1_zfmisc_1(X0))
| v1_xboole_0(X0) ),
inference(forward_subsumption_resolution,[],[f18176,f13637]) ).
fof(f21291,plain,
! [X2,X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m2_lattice4(X0,X1)
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| ~ r1_lattice2(X2,X3,u2_lattices(X1))
| r1_lattice2(X0,k1_realset1(X3,X0),k1_realset1(u2_lattices(X1),X0))
| ~ m2_relset_1(k1_realset1(u2_lattices(X1),X0),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(k1_realset1(X3,X0))
| ~ v1_funct_2(k1_realset1(X3,X0),k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(k1_realset1(X3,X0),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(u2_lattices(X1))
| ~ v1_funct_2(u2_lattices(X1),k2_zfmisc_1(X2,X2),X2)
| ~ m2_relset_1(u2_lattices(X1),k2_zfmisc_1(X2,X2),X2)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,k2_zfmisc_1(X2,X2),X2)
| ~ m2_relset_1(X3,k2_zfmisc_1(X2,X2),X2)
| ~ m1_subset_1(X0,k1_zfmisc_1(X2))
| v1_xboole_0(X2) ),
inference(forward_subsumption_resolution,[],[f18195,f13629]) ).
fof(f21603,definition,
( spl1088_417
<=> v1_xboole_0(u1_struct_0(sK1079)) ),
introduced(definition,[new_symbols(definition,[spl1088_417])],[avatar_definition]) ).
fof(f21604,plain,
( ~ v1_xboole_0(u1_struct_0(sK1079))
| spl1088_417 ),
inference(avatar_component_clause,[],[f21603]) ).
fof(f21618,plain,
( ~ v1_xboole_0(u1_struct_0(sK1079))
| ~ v10_lattices(k1_lattice2(sK1079))
| ~ l3_lattices(k1_lattice2(sK1079))
| spl1088_355
| ~ spl1088_364
| ~ spl1088_365 ),
inference(forward_subsumption_resolution,[],[f21243,f18323]) ).
fof(f21625,plain,
( ! [X0,X1] :
( ~ v1_funct_2(sK1081,k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ r1_lattice2(X0,X1,sF1083)
| r1_lattice2(sK1080,k1_realset1(X1,sK1080),sK1081)
| ~ m2_relset_1(sK1081,k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ v1_funct_1(k1_realset1(X1,sK1080))
| ~ v1_funct_2(k1_realset1(X1,sK1080),k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ m2_relset_1(k1_realset1(X1,sK1080),k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ v1_funct_2(sF1083,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(sF1083,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| v1_xboole_0(sK1080)
| ~ m1_subset_1(sK1080,k1_zfmisc_1(X0))
| v1_xboole_0(X0) )
| ~ spl1088_347 ),
inference(forward_subsumption_resolution,[],[f21271,f18498]) ).
fof(f21630,plain,
( ! [X0] :
( ~ v1_funct_2(sK1082,k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ v2_binop_1(sF1085,X0)
| v2_binop_1(sK1082,sK1080)
| ~ m2_relset_1(sK1082,k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ v1_funct_2(sF1085,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(sF1085,k2_zfmisc_1(X0,X0),X0)
| v1_xboole_0(sK1080)
| ~ m1_subset_1(sK1080,k1_zfmisc_1(X0))
| v1_xboole_0(X0) )
| ~ spl1088_350 ),
inference(forward_subsumption_resolution,[],[f21278,f18532]) ).
fof(f21631,plain,
( ! [X0] :
( ~ v1_funct_2(sK1081,k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ v2_binop_1(sF1083,X0)
| v2_binop_1(sK1081,sK1080)
| ~ m2_relset_1(sK1081,k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ v1_funct_2(sF1083,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(sF1083,k2_zfmisc_1(X0,X0),X0)
| v1_xboole_0(sK1080)
| ~ m1_subset_1(sK1080,k1_zfmisc_1(X0))
| v1_xboole_0(X0) )
| ~ spl1088_347 ),
inference(forward_subsumption_resolution,[],[f21279,f18498]) ).
fof(f21632,plain,
( ! [X0] :
( ~ v1_funct_2(sK1082,k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ v1_binop_1(sF1085,X0)
| ~ m2_relset_1(sK1082,k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ v1_funct_1(sF1085)
| ~ v1_funct_2(sF1085,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(sF1085,k2_zfmisc_1(X0,X0),X0)
| v1_xboole_0(sK1080)
| ~ m1_subset_1(sK1080,k1_zfmisc_1(X0))
| v1_xboole_0(X0) )
| spl1088_4 ),
inference(forward_subsumption_resolution,[],[f21281,f15663]) ).
fof(f21633,plain,
( ! [X0] :
( ~ v1_funct_2(sK1081,k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ v1_binop_1(sF1083,X0)
| v1_binop_1(sK1081,sK1080)
| ~ m2_relset_1(sK1081,k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ v1_funct_2(sF1083,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(sF1083,k2_zfmisc_1(X0,X0),X0)
| v1_xboole_0(sK1080)
| ~ m1_subset_1(sK1080,k1_zfmisc_1(X0))
| v1_xboole_0(X0) )
| ~ spl1088_347 ),
inference(forward_subsumption_resolution,[],[f21282,f18498]) ).
fof(f21640,plain,
! [X2,X3,X0,X1] :
( ~ v1_funct_2(k1_realset1(X3,X0),k2_zfmisc_1(X0,X0),X0)
| ~ m2_lattice4(X0,X1)
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| ~ r1_lattice2(X2,X3,u2_lattices(X1))
| r1_lattice2(X0,k1_realset1(X3,X0),k1_realset1(u2_lattices(X1),X0))
| ~ v1_funct_1(k1_realset1(X3,X0))
| v1_xboole_0(X0)
| ~ m2_relset_1(k1_realset1(X3,X0),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(u2_lattices(X1))
| ~ v1_funct_2(u2_lattices(X1),k2_zfmisc_1(X2,X2),X2)
| ~ m2_relset_1(u2_lattices(X1),k2_zfmisc_1(X2,X2),X2)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,k2_zfmisc_1(X2,X2),X2)
| ~ m2_relset_1(X3,k2_zfmisc_1(X2,X2),X2)
| ~ m1_subset_1(X0,k1_zfmisc_1(X2))
| v1_xboole_0(X2) ),
inference(forward_subsumption_resolution,[],[f21291,f13627]) ).
fof(f21896,plain,
( ~ v1_xboole_0(u1_struct_0(sK1079))
| ~ l3_lattices(k1_lattice2(sK1079))
| spl1088_355
| ~ spl1088_364
| ~ spl1088_365 ),
inference(forward_subsumption_resolution,[],[f21618,f18442]) ).
fof(f21902,plain,
( ! [X0,X1] :
( ~ v1_funct_2(sK1081,k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ r1_lattice2(X0,X1,sF1083)
| r1_lattice2(sK1080,k1_realset1(X1,sK1080),sK1081)
| ~ m2_relset_1(sK1081,k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ v1_funct_1(k1_realset1(X1,sK1080))
| ~ v1_funct_2(k1_realset1(X1,sK1080),k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ m2_relset_1(k1_realset1(X1,sK1080),k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ v1_funct_2(sF1083,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(sF1083,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m1_subset_1(sK1080,k1_zfmisc_1(X0))
| v1_xboole_0(X0) )
| ~ spl1088_347 ),
inference(forward_subsumption_resolution,[],[f21625,f13634]) ).
fof(f21907,plain,
( ! [X0] :
( ~ v1_funct_2(sK1082,k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ v2_binop_1(sF1085,X0)
| v2_binop_1(sK1082,sK1080)
| ~ m2_relset_1(sK1082,k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ v1_funct_2(sF1085,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(sF1085,k2_zfmisc_1(X0,X0),X0)
| ~ m1_subset_1(sK1080,k1_zfmisc_1(X0))
| v1_xboole_0(X0) )
| ~ spl1088_350 ),
inference(forward_subsumption_resolution,[],[f21630,f13634]) ).
fof(f21908,plain,
( ! [X0] :
( ~ v1_funct_2(sK1081,k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ v2_binop_1(sF1083,X0)
| v2_binop_1(sK1081,sK1080)
| ~ m2_relset_1(sK1081,k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ v1_funct_2(sF1083,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(sF1083,k2_zfmisc_1(X0,X0),X0)
| ~ m1_subset_1(sK1080,k1_zfmisc_1(X0))
| v1_xboole_0(X0) )
| ~ spl1088_347 ),
inference(forward_subsumption_resolution,[],[f21631,f13634]) ).
fof(f21909,plain,
( ! [X0] :
( ~ v1_funct_2(sK1082,k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ v1_binop_1(sF1085,X0)
| ~ m2_relset_1(sK1082,k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ v1_funct_2(sF1085,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(sF1085,k2_zfmisc_1(X0,X0),X0)
| v1_xboole_0(sK1080)
| ~ m1_subset_1(sK1080,k1_zfmisc_1(X0))
| v1_xboole_0(X0) )
| spl1088_4
| ~ spl1088_350 ),
inference(forward_subsumption_resolution,[],[f21632,f18532]) ).
fof(f21910,plain,
( ! [X0] :
( ~ v1_funct_2(sK1081,k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ v1_binop_1(sF1083,X0)
| v1_binop_1(sK1081,sK1080)
| ~ m2_relset_1(sK1081,k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ v1_funct_2(sF1083,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(sF1083,k2_zfmisc_1(X0,X0),X0)
| ~ m1_subset_1(sK1080,k1_zfmisc_1(X0))
| v1_xboole_0(X0) )
| ~ spl1088_347 ),
inference(forward_subsumption_resolution,[],[f21633,f13634]) ).
fof(f22036,plain,
( ~ v1_xboole_0(u1_struct_0(sK1079))
| spl1088_355
| ~ spl1088_364
| ~ spl1088_365 ),
inference(forward_subsumption_resolution,[],[f21896,f18438]) ).
fof(f22042,plain,
( ! [X0,X1] :
( ~ v1_funct_2(sK1081,sF1087,sK1080)
| ~ r1_lattice2(X0,X1,sF1083)
| r1_lattice2(sK1080,k1_realset1(X1,sK1080),sK1081)
| ~ m2_relset_1(sK1081,k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ v1_funct_1(k1_realset1(X1,sK1080))
| ~ v1_funct_2(k1_realset1(X1,sK1080),k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ m2_relset_1(k1_realset1(X1,sK1080),k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ v1_funct_2(sF1083,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(sF1083,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m1_subset_1(sK1080,k1_zfmisc_1(X0))
| v1_xboole_0(X0) )
| ~ spl1088_347 ),
inference(forward_demodulation,[],[f21902,f15581]) ).
fof(f22045,plain,
( ! [X0] :
( ~ v1_funct_2(sK1082,sF1087,sK1080)
| ~ v2_binop_1(sF1085,X0)
| v2_binop_1(sK1082,sK1080)
| ~ m2_relset_1(sK1082,k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ v1_funct_2(sF1085,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(sF1085,k2_zfmisc_1(X0,X0),X0)
| ~ m1_subset_1(sK1080,k1_zfmisc_1(X0))
| v1_xboole_0(X0) )
| ~ spl1088_350 ),
inference(forward_demodulation,[],[f21907,f15581]) ).
fof(f22046,plain,
( ! [X0] :
( ~ v1_funct_2(sK1081,sF1087,sK1080)
| ~ v2_binop_1(sF1083,X0)
| v2_binop_1(sK1081,sK1080)
| ~ m2_relset_1(sK1081,k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ v1_funct_2(sF1083,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(sF1083,k2_zfmisc_1(X0,X0),X0)
| ~ m1_subset_1(sK1080,k1_zfmisc_1(X0))
| v1_xboole_0(X0) )
| ~ spl1088_347 ),
inference(forward_demodulation,[],[f21908,f15581]) ).
fof(f22047,plain,
( ! [X0] :
( ~ v1_funct_2(sK1082,k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ v1_binop_1(sF1085,X0)
| ~ m2_relset_1(sK1082,k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ v1_funct_2(sF1085,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(sF1085,k2_zfmisc_1(X0,X0),X0)
| ~ m1_subset_1(sK1080,k1_zfmisc_1(X0))
| v1_xboole_0(X0) )
| spl1088_4
| ~ spl1088_350 ),
inference(forward_subsumption_resolution,[],[f21909,f13634]) ).
fof(f22048,plain,
( ! [X0] :
( ~ v1_funct_2(sK1081,sF1087,sK1080)
| ~ v1_binop_1(sF1083,X0)
| v1_binop_1(sK1081,sK1080)
| ~ m2_relset_1(sK1081,k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ v1_funct_2(sF1083,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(sF1083,k2_zfmisc_1(X0,X0),X0)
| ~ m1_subset_1(sK1080,k1_zfmisc_1(X0))
| v1_xboole_0(X0) )
| ~ spl1088_347 ),
inference(forward_demodulation,[],[f21910,f15581]) ).
fof(f22091,plain,
( ~ spl1088_417
| spl1088_355
| ~ spl1088_364
| ~ spl1088_365 ),
inference(avatar_split_clause,[],[f22036,f18441,f18437,f18322,f21603]) ).
fof(f22095,plain,
( ! [X0,X1] :
( ~ r1_lattice2(X0,X1,sF1083)
| r1_lattice2(sK1080,k1_realset1(X1,sK1080),sK1081)
| ~ m2_relset_1(sK1081,k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ v1_funct_1(k1_realset1(X1,sK1080))
| ~ v1_funct_2(k1_realset1(X1,sK1080),k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ m2_relset_1(k1_realset1(X1,sK1080),k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ v1_funct_2(sF1083,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(sF1083,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m1_subset_1(sK1080,k1_zfmisc_1(X0))
| v1_xboole_0(X0) )
| ~ spl1088_347 ),
inference(forward_subsumption_resolution,[],[f22042,f15584]) ).
fof(f22098,plain,
( ! [X0] :
( ~ v2_binop_1(sF1085,X0)
| v2_binop_1(sK1082,sK1080)
| ~ m2_relset_1(sK1082,k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ v1_funct_2(sF1085,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(sF1085,k2_zfmisc_1(X0,X0),X0)
| ~ m1_subset_1(sK1080,k1_zfmisc_1(X0))
| v1_xboole_0(X0) )
| ~ spl1088_350 ),
inference(forward_subsumption_resolution,[],[f22045,f15582]) ).
fof(f22099,plain,
( ! [X0] :
( ~ v2_binop_1(sF1083,X0)
| v2_binop_1(sK1081,sK1080)
| ~ m2_relset_1(sK1081,k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ v1_funct_2(sF1083,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(sF1083,k2_zfmisc_1(X0,X0),X0)
| ~ m1_subset_1(sK1080,k1_zfmisc_1(X0))
| v1_xboole_0(X0) )
| ~ spl1088_347 ),
inference(forward_subsumption_resolution,[],[f22046,f15584]) ).
fof(f22100,plain,
( ! [X0] :
( ~ v1_funct_2(sK1082,sF1087,sK1080)
| ~ v1_binop_1(sF1085,X0)
| ~ m2_relset_1(sK1082,k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ v1_funct_2(sF1085,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(sF1085,k2_zfmisc_1(X0,X0),X0)
| ~ m1_subset_1(sK1080,k1_zfmisc_1(X0))
| v1_xboole_0(X0) )
| spl1088_4
| ~ spl1088_350 ),
inference(forward_demodulation,[],[f22047,f15581]) ).
fof(f22101,plain,
( ! [X0] :
( ~ v1_binop_1(sF1083,X0)
| v1_binop_1(sK1081,sK1080)
| ~ m2_relset_1(sK1081,k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ v1_funct_2(sF1083,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(sF1083,k2_zfmisc_1(X0,X0),X0)
| ~ m1_subset_1(sK1080,k1_zfmisc_1(X0))
| v1_xboole_0(X0) )
| ~ spl1088_347 ),
inference(forward_subsumption_resolution,[],[f22048,f15584]) ).
fof(f22180,plain,
( ! [X0,X1] :
( ~ m2_relset_1(sK1081,sF1087,sK1080)
| ~ r1_lattice2(X0,X1,sF1083)
| r1_lattice2(sK1080,k1_realset1(X1,sK1080),sK1081)
| ~ v1_funct_1(k1_realset1(X1,sK1080))
| ~ v1_funct_2(k1_realset1(X1,sK1080),k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ m2_relset_1(k1_realset1(X1,sK1080),k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ v1_funct_2(sF1083,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(sF1083,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m1_subset_1(sK1080,k1_zfmisc_1(X0))
| v1_xboole_0(X0) )
| ~ spl1088_347 ),
inference(forward_demodulation,[],[f22095,f15581]) ).
fof(f22183,plain,
( ! [X0] :
( ~ m2_relset_1(sK1082,sF1087,sK1080)
| ~ v2_binop_1(sF1085,X0)
| v2_binop_1(sK1082,sK1080)
| ~ v1_funct_2(sF1085,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(sF1085,k2_zfmisc_1(X0,X0),X0)
| ~ m1_subset_1(sK1080,k1_zfmisc_1(X0))
| v1_xboole_0(X0) )
| ~ spl1088_350 ),
inference(forward_demodulation,[],[f22098,f15581]) ).
fof(f22184,plain,
( ! [X0] :
( ~ m2_relset_1(sK1081,sF1087,sK1080)
| ~ v2_binop_1(sF1083,X0)
| v2_binop_1(sK1081,sK1080)
| ~ v1_funct_2(sF1083,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(sF1083,k2_zfmisc_1(X0,X0),X0)
| ~ m1_subset_1(sK1080,k1_zfmisc_1(X0))
| v1_xboole_0(X0) )
| ~ spl1088_347 ),
inference(forward_demodulation,[],[f22099,f15581]) ).
fof(f22185,plain,
( ! [X0] :
( ~ v1_binop_1(sF1085,X0)
| ~ m2_relset_1(sK1082,k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ v1_funct_2(sF1085,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(sF1085,k2_zfmisc_1(X0,X0),X0)
| ~ m1_subset_1(sK1080,k1_zfmisc_1(X0))
| v1_xboole_0(X0) )
| spl1088_4
| ~ spl1088_350 ),
inference(forward_subsumption_resolution,[],[f22100,f15582]) ).
fof(f22186,plain,
( ! [X0] :
( ~ m2_relset_1(sK1081,sF1087,sK1080)
| ~ v1_binop_1(sF1083,X0)
| v1_binop_1(sK1081,sK1080)
| ~ v1_funct_2(sF1083,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(sF1083,k2_zfmisc_1(X0,X0),X0)
| ~ m1_subset_1(sK1080,k1_zfmisc_1(X0))
| v1_xboole_0(X0) )
| ~ spl1088_347 ),
inference(forward_demodulation,[],[f22101,f15581]) ).
fof(f22213,plain,
( ! [X0,X1] :
( ~ r1_lattice2(X0,X1,sF1083)
| r1_lattice2(sK1080,k1_realset1(X1,sK1080),sK1081)
| ~ v1_funct_1(k1_realset1(X1,sK1080))
| ~ v1_funct_2(k1_realset1(X1,sK1080),k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ m2_relset_1(k1_realset1(X1,sK1080),k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ v1_funct_2(sF1083,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(sF1083,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m1_subset_1(sK1080,k1_zfmisc_1(X0))
| v1_xboole_0(X0) )
| ~ spl1088_347 ),
inference(forward_subsumption_resolution,[],[f22180,f15585]) ).
fof(f22216,plain,
( ! [X0] :
( ~ v2_binop_1(sF1085,X0)
| v2_binop_1(sK1082,sK1080)
| ~ v1_funct_2(sF1085,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(sF1085,k2_zfmisc_1(X0,X0),X0)
| ~ m1_subset_1(sK1080,k1_zfmisc_1(X0))
| v1_xboole_0(X0) )
| ~ spl1088_350 ),
inference(forward_subsumption_resolution,[],[f22183,f15583]) ).
fof(f22217,plain,
( ! [X0] :
( ~ v2_binop_1(sF1083,X0)
| v2_binop_1(sK1081,sK1080)
| ~ v1_funct_2(sF1083,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(sF1083,k2_zfmisc_1(X0,X0),X0)
| ~ m1_subset_1(sK1080,k1_zfmisc_1(X0))
| v1_xboole_0(X0) )
| ~ spl1088_347 ),
inference(forward_subsumption_resolution,[],[f22184,f15585]) ).
fof(f22218,plain,
( ! [X0] :
( ~ m2_relset_1(sK1082,sF1087,sK1080)
| ~ v1_binop_1(sF1085,X0)
| ~ v1_funct_2(sF1085,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(sF1085,k2_zfmisc_1(X0,X0),X0)
| ~ m1_subset_1(sK1080,k1_zfmisc_1(X0))
| v1_xboole_0(X0) )
| spl1088_4
| ~ spl1088_350 ),
inference(forward_demodulation,[],[f22185,f15581]) ).
fof(f22219,plain,
( ! [X0] :
( ~ v1_binop_1(sF1083,X0)
| v1_binop_1(sK1081,sK1080)
| ~ v1_funct_2(sF1083,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(sF1083,k2_zfmisc_1(X0,X0),X0)
| ~ m1_subset_1(sK1080,k1_zfmisc_1(X0))
| v1_xboole_0(X0) )
| ~ spl1088_347 ),
inference(forward_subsumption_resolution,[],[f22186,f15585]) ).
fof(f22262,plain,
( ! [X0,X1] :
( ~ v1_funct_2(k1_realset1(X1,sK1080),sF1087,sK1080)
| ~ r1_lattice2(X0,X1,sF1083)
| r1_lattice2(sK1080,k1_realset1(X1,sK1080),sK1081)
| ~ v1_funct_1(k1_realset1(X1,sK1080))
| ~ m2_relset_1(k1_realset1(X1,sK1080),k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ v1_funct_2(sF1083,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(sF1083,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m1_subset_1(sK1080,k1_zfmisc_1(X0))
| v1_xboole_0(X0) )
| ~ spl1088_347 ),
inference(forward_demodulation,[],[f22213,f15581]) ).
fof(f22266,definition,
( spl1088_466
<=> ! [X0] :
( ~ v2_binop_1(sF1085,X0)
| v1_xboole_0(X0)
| ~ m1_subset_1(sK1080,k1_zfmisc_1(X0))
| ~ m2_relset_1(sF1085,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(sF1085,k2_zfmisc_1(X0,X0),X0) ) ),
introduced(definition,[new_symbols(definition,[spl1088_466])],[avatar_definition]) ).
fof(f22267,plain,
( ! [X0] :
( ~ v1_funct_2(sF1085,k2_zfmisc_1(X0,X0),X0)
| v1_xboole_0(X0)
| ~ m1_subset_1(sK1080,k1_zfmisc_1(X0))
| ~ m2_relset_1(sF1085,k2_zfmisc_1(X0,X0),X0)
| ~ v2_binop_1(sF1085,X0) )
| ~ spl1088_466 ),
inference(avatar_component_clause,[],[f22266]) ).
fof(f22268,plain,
( spl1088_3
| spl1088_466
| ~ spl1088_350 ),
inference(avatar_split_clause,[],[f22216,f18228,f22266,f15657]) ).
fof(f22270,definition,
( spl1088_467
<=> ! [X0] :
( ~ v2_binop_1(sF1083,X0)
| v1_xboole_0(X0)
| ~ m1_subset_1(sK1080,k1_zfmisc_1(X0))
| ~ m2_relset_1(sF1083,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(sF1083,k2_zfmisc_1(X0,X0),X0) ) ),
introduced(definition,[new_symbols(definition,[spl1088_467])],[avatar_definition]) ).
fof(f22271,plain,
( ! [X0] :
( ~ v1_funct_2(sF1083,k2_zfmisc_1(X0,X0),X0)
| v1_xboole_0(X0)
| ~ m1_subset_1(sK1080,k1_zfmisc_1(X0))
| ~ m2_relset_1(sF1083,k2_zfmisc_1(X0,X0),X0)
| ~ v2_binop_1(sF1083,X0) )
| ~ spl1088_467 ),
inference(avatar_component_clause,[],[f22270]) ).
fof(f22272,plain,
( spl1088_5
| spl1088_467
| ~ spl1088_347 ),
inference(avatar_split_clause,[],[f22217,f18213,f22270,f15665]) ).
fof(f22273,plain,
( ! [X0] :
( ~ v1_funct_2(sF1085,k2_zfmisc_1(X0,X0),X0)
| ~ v1_binop_1(sF1085,X0)
| ~ m2_relset_1(sF1085,k2_zfmisc_1(X0,X0),X0)
| ~ m1_subset_1(sK1080,k1_zfmisc_1(X0))
| v1_xboole_0(X0) )
| spl1088_4
| ~ spl1088_350 ),
inference(forward_subsumption_resolution,[],[f22218,f15583]) ).
fof(f22275,definition,
( spl1088_468
<=> ! [X0] :
( ~ v1_binop_1(sF1083,X0)
| v1_xboole_0(X0)
| ~ m1_subset_1(sK1080,k1_zfmisc_1(X0))
| ~ m2_relset_1(sF1083,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(sF1083,k2_zfmisc_1(X0,X0),X0) ) ),
introduced(definition,[new_symbols(definition,[spl1088_468])],[avatar_definition]) ).
fof(f22276,plain,
( ! [X0] :
( ~ v1_funct_2(sF1083,k2_zfmisc_1(X0,X0),X0)
| v1_xboole_0(X0)
| ~ m1_subset_1(sK1080,k1_zfmisc_1(X0))
| ~ m2_relset_1(sF1083,k2_zfmisc_1(X0,X0),X0)
| ~ v1_binop_1(sF1083,X0) )
| ~ spl1088_468 ),
inference(avatar_component_clause,[],[f22275]) ).
fof(f22277,plain,
( spl1088_6
| spl1088_468
| ~ spl1088_347 ),
inference(avatar_split_clause,[],[f22219,f18213,f22275,f15669]) ).
fof(f22301,plain,
( ! [X0,X1] :
( ~ v1_funct_2(sF1083,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(k1_realset1(X1,sK1080),sF1087,sK1080)
| ~ r1_lattice2(X0,X1,sF1083)
| r1_lattice2(sK1080,k1_realset1(X1,sK1080),sK1081)
| ~ v1_funct_1(k1_realset1(X1,sK1080))
| ~ m2_relset_1(k1_realset1(X1,sK1080),sF1087,sK1080)
| ~ m2_relset_1(sF1083,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m1_subset_1(sK1080,k1_zfmisc_1(X0))
| v1_xboole_0(X0) )
| ~ spl1088_347 ),
inference(forward_demodulation,[],[f22262,f15581]) ).
fof(f22308,plain,
( ! [X0] :
( ~ v1_funct_2(k1_realset1(X0,sK1080),sF1087,sK1080)
| ~ r1_lattice2(u1_struct_0(sK1079),X0,sF1083)
| r1_lattice2(sK1080,k1_realset1(X0,sK1080),sK1081)
| ~ v1_funct_1(k1_realset1(X0,sK1080))
| ~ m2_relset_1(k1_realset1(X0,sK1080),sF1087,sK1080)
| ~ m2_relset_1(sF1083,k2_zfmisc_1(u1_struct_0(sK1079),u1_struct_0(sK1079)),u1_struct_0(sK1079))
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,k2_zfmisc_1(u1_struct_0(sK1079),u1_struct_0(sK1079)),u1_struct_0(sK1079))
| ~ m2_relset_1(X0,k2_zfmisc_1(u1_struct_0(sK1079),u1_struct_0(sK1079)),u1_struct_0(sK1079))
| ~ m1_subset_1(sK1080,k1_zfmisc_1(u1_struct_0(sK1079)))
| v1_xboole_0(u1_struct_0(sK1079)) )
| ~ spl1088_347 ),
inference(resolution,[],[f22301,f18491]) ).
fof(f22311,plain,
( ! [X0] :
( ~ v1_funct_2(k1_realset1(X0,sK1080),sF1087,sK1080)
| ~ r1_lattice2(u1_struct_0(sK1079),X0,sF1083)
| r1_lattice2(sK1080,k1_realset1(X0,sK1080),sK1081)
| ~ v1_funct_1(k1_realset1(X0,sK1080))
| ~ m2_relset_1(k1_realset1(X0,sK1080),sF1087,sK1080)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,k2_zfmisc_1(u1_struct_0(sK1079),u1_struct_0(sK1079)),u1_struct_0(sK1079))
| ~ m2_relset_1(X0,k2_zfmisc_1(u1_struct_0(sK1079),u1_struct_0(sK1079)),u1_struct_0(sK1079))
| ~ m1_subset_1(sK1080,k1_zfmisc_1(u1_struct_0(sK1079)))
| v1_xboole_0(u1_struct_0(sK1079)) )
| ~ spl1088_347 ),
inference(forward_subsumption_resolution,[],[f22308,f18514]) ).
fof(f22328,plain,
( ! [X0] :
( ~ v1_funct_2(k1_realset1(X0,sK1080),sF1087,sK1080)
| ~ r1_lattice2(u1_struct_0(sK1079),X0,sF1083)
| r1_lattice2(sK1080,k1_realset1(X0,sK1080),sK1081)
| ~ v1_funct_1(k1_realset1(X0,sK1080))
| ~ m2_relset_1(k1_realset1(X0,sK1080),sF1087,sK1080)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,k2_zfmisc_1(u1_struct_0(sK1079),u1_struct_0(sK1079)),u1_struct_0(sK1079))
| ~ m2_relset_1(X0,k2_zfmisc_1(u1_struct_0(sK1079),u1_struct_0(sK1079)),u1_struct_0(sK1079))
| ~ m1_subset_1(sK1080,k1_zfmisc_1(u1_struct_0(sK1079))) )
| ~ spl1088_347
| spl1088_417 ),
inference(forward_subsumption_resolution,[],[f22311,f21604]) ).
fof(f22330,definition,
( spl1088_477
<=> m1_subset_1(sK1080,k1_zfmisc_1(u1_struct_0(sK1079))) ),
introduced(definition,[new_symbols(definition,[spl1088_477])],[avatar_definition]) ).
fof(f22331,plain,
( m1_subset_1(sK1080,k1_zfmisc_1(u1_struct_0(sK1079)))
| ~ spl1088_477 ),
inference(avatar_component_clause,[],[f22330]) ).
fof(f22332,plain,
( ~ m1_subset_1(sK1080,k1_zfmisc_1(u1_struct_0(sK1079)))
| spl1088_477 ),
inference(avatar_component_clause,[],[f22330]) ).
fof(f22334,definition,
( spl1088_478
<=> ! [X0] :
( ~ v1_funct_2(k1_realset1(X0,sK1080),sF1087,sK1080)
| ~ m2_relset_1(X0,k2_zfmisc_1(u1_struct_0(sK1079),u1_struct_0(sK1079)),u1_struct_0(sK1079))
| ~ v1_funct_2(X0,k2_zfmisc_1(u1_struct_0(sK1079),u1_struct_0(sK1079)),u1_struct_0(sK1079))
| ~ v1_funct_1(X0)
| ~ m2_relset_1(k1_realset1(X0,sK1080),sF1087,sK1080)
| ~ v1_funct_1(k1_realset1(X0,sK1080))
| r1_lattice2(sK1080,k1_realset1(X0,sK1080),sK1081)
| ~ r1_lattice2(u1_struct_0(sK1079),X0,sF1083) ) ),
introduced(definition,[new_symbols(definition,[spl1088_478])],[avatar_definition]) ).
fof(f22335,plain,
( ! [X0] :
( ~ v1_funct_2(X0,k2_zfmisc_1(u1_struct_0(sK1079),u1_struct_0(sK1079)),u1_struct_0(sK1079))
| ~ m2_relset_1(X0,k2_zfmisc_1(u1_struct_0(sK1079),u1_struct_0(sK1079)),u1_struct_0(sK1079))
| ~ v1_funct_2(k1_realset1(X0,sK1080),sF1087,sK1080)
| ~ v1_funct_1(X0)
| ~ m2_relset_1(k1_realset1(X0,sK1080),sF1087,sK1080)
| ~ v1_funct_1(k1_realset1(X0,sK1080))
| r1_lattice2(sK1080,k1_realset1(X0,sK1080),sK1081)
| ~ r1_lattice2(u1_struct_0(sK1079),X0,sF1083) )
| ~ spl1088_478 ),
inference(avatar_component_clause,[],[f22334]) ).
fof(f22336,plain,
( ~ spl1088_477
| spl1088_478
| ~ spl1088_347
| spl1088_417 ),
inference(avatar_split_clause,[],[f22328,f21603,f18213,f22334,f22330]) ).
fof(f22469,plain,
( ~ v1_binop_1(sF1085,u1_struct_0(sK1079))
| ~ m2_relset_1(sF1085,k2_zfmisc_1(u1_struct_0(sK1079),u1_struct_0(sK1079)),u1_struct_0(sK1079))
| ~ m1_subset_1(sK1080,k1_zfmisc_1(u1_struct_0(sK1079)))
| v1_xboole_0(u1_struct_0(sK1079))
| spl1088_4
| ~ spl1088_350 ),
inference(resolution,[],[f22273,f18533]) ).
fof(f22526,plain,
! [X0,X1] :
( ~ v1_funct_2(sK1081,k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ m2_lattice4(sK1080,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ r1_lattice2(X1,sF1083,u2_lattices(X0))
| r1_lattice2(sK1080,sK1081,k1_realset1(u2_lattices(X0),sK1080))
| ~ v1_funct_1(sK1081)
| v1_xboole_0(sK1080)
| ~ m2_relset_1(sK1081,k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ v1_funct_1(u2_lattices(X0))
| ~ v1_funct_2(u2_lattices(X0),k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(u2_lattices(X0),k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(sF1083)
| ~ v1_funct_2(sF1083,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(sF1083,k2_zfmisc_1(X1,X1),X1)
| ~ m1_subset_1(sK1080,k1_zfmisc_1(X1))
| v1_xboole_0(X1) ),
inference(superposition,[],[f21640,f17549]) ).
fof(f22534,plain,
! [X0,X1] :
( ~ v1_funct_2(sK1081,k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ m2_lattice4(sK1080,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ r1_lattice2(X1,sF1083,u2_lattices(X0))
| r1_lattice2(sK1080,sK1081,k1_realset1(u2_lattices(X0),sK1080))
| v1_xboole_0(sK1080)
| ~ m2_relset_1(sK1081,k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ v1_funct_1(u2_lattices(X0))
| ~ v1_funct_2(u2_lattices(X0),k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(u2_lattices(X0),k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(sF1083)
| ~ v1_funct_2(sF1083,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(sF1083,k2_zfmisc_1(X1,X1),X1)
| ~ m1_subset_1(sK1080,k1_zfmisc_1(X1))
| v1_xboole_0(X1) ),
inference(forward_subsumption_resolution,[],[f22526,f13637]) ).
fof(f22543,plain,
! [X0,X1] :
( ~ v1_funct_2(sK1081,k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ m2_lattice4(sK1080,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ r1_lattice2(X1,sF1083,u2_lattices(X0))
| r1_lattice2(sK1080,sK1081,k1_realset1(u2_lattices(X0),sK1080))
| ~ m2_relset_1(sK1081,k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ v1_funct_1(u2_lattices(X0))
| ~ v1_funct_2(u2_lattices(X0),k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(u2_lattices(X0),k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(sF1083)
| ~ v1_funct_2(sF1083,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(sF1083,k2_zfmisc_1(X1,X1),X1)
| ~ m1_subset_1(sK1080,k1_zfmisc_1(X1))
| v1_xboole_0(X1) ),
inference(forward_subsumption_resolution,[],[f22534,f13634]) ).
fof(f22552,plain,
( ! [X0,X1] :
( ~ v1_funct_2(sK1081,k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ m2_lattice4(sK1080,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ r1_lattice2(X1,sF1083,u2_lattices(X0))
| r1_lattice2(sK1080,sK1081,k1_realset1(u2_lattices(X0),sK1080))
| ~ m2_relset_1(sK1081,k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ v1_funct_1(u2_lattices(X0))
| ~ v1_funct_2(u2_lattices(X0),k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(u2_lattices(X0),k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_2(sF1083,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(sF1083,k2_zfmisc_1(X1,X1),X1)
| ~ m1_subset_1(sK1080,k1_zfmisc_1(X1))
| v1_xboole_0(X1) )
| ~ spl1088_347 ),
inference(forward_subsumption_resolution,[],[f22543,f18498]) ).
fof(f22558,plain,
( ! [X0,X1] :
( ~ v1_funct_2(sK1081,sF1087,sK1080)
| ~ m2_lattice4(sK1080,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ r1_lattice2(X1,sF1083,u2_lattices(X0))
| r1_lattice2(sK1080,sK1081,k1_realset1(u2_lattices(X0),sK1080))
| ~ m2_relset_1(sK1081,k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ v1_funct_1(u2_lattices(X0))
| ~ v1_funct_2(u2_lattices(X0),k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(u2_lattices(X0),k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_2(sF1083,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(sF1083,k2_zfmisc_1(X1,X1),X1)
| ~ m1_subset_1(sK1080,k1_zfmisc_1(X1))
| v1_xboole_0(X1) )
| ~ spl1088_347 ),
inference(forward_demodulation,[],[f22552,f15581]) ).
fof(f22562,plain,
( ! [X0,X1] :
( ~ m2_lattice4(sK1080,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ r1_lattice2(X1,sF1083,u2_lattices(X0))
| r1_lattice2(sK1080,sK1081,k1_realset1(u2_lattices(X0),sK1080))
| ~ m2_relset_1(sK1081,k2_zfmisc_1(sK1080,sK1080),sK1080)
| ~ v1_funct_1(u2_lattices(X0))
| ~ v1_funct_2(u2_lattices(X0),k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(u2_lattices(X0),k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_2(sF1083,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(sF1083,k2_zfmisc_1(X1,X1),X1)
| ~ m1_subset_1(sK1080,k1_zfmisc_1(X1))
| v1_xboole_0(X1) )
| ~ spl1088_347 ),
inference(forward_subsumption_resolution,[],[f22558,f15584]) ).
fof(f22564,plain,
( ! [X0,X1] :
( ~ m2_relset_1(sK1081,sF1087,sK1080)
| ~ m2_lattice4(sK1080,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ r1_lattice2(X1,sF1083,u2_lattices(X0))
| r1_lattice2(sK1080,sK1081,k1_realset1(u2_lattices(X0),sK1080))
| ~ v1_funct_1(u2_lattices(X0))
| ~ v1_funct_2(u2_lattices(X0),k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(u2_lattices(X0),k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_2(sF1083,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(sF1083,k2_zfmisc_1(X1,X1),X1)
| ~ m1_subset_1(sK1080,k1_zfmisc_1(X1))
| v1_xboole_0(X1) )
| ~ spl1088_347 ),
inference(forward_demodulation,[],[f22562,f15581]) ).
fof(f22566,plain,
( ! [X0,X1] :
( ~ v1_funct_2(u2_lattices(X0),k2_zfmisc_1(X1,X1),X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ r1_lattice2(X1,sF1083,u2_lattices(X0))
| r1_lattice2(sK1080,sK1081,k1_realset1(u2_lattices(X0),sK1080))
| ~ v1_funct_1(u2_lattices(X0))
| ~ m2_lattice4(sK1080,X0)
| ~ m2_relset_1(u2_lattices(X0),k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_2(sF1083,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(sF1083,k2_zfmisc_1(X1,X1),X1)
| ~ m1_subset_1(sK1080,k1_zfmisc_1(X1))
| v1_xboole_0(X1) )
| ~ spl1088_347 ),
inference(forward_subsumption_resolution,[],[f22564,f15585]) ).
fof(f22599,plain,
( ~ m2_lattice4(sK1080,sK1079)
| v3_struct_0(sK1079)
| ~ v10_lattices(sK1079)
| ~ l3_lattices(sK1079)
| spl1088_477 ),
inference(resolution,[],[f22332,f13323]) ).
fof(f22601,plain,
( v3_struct_0(sK1079)
| ~ v10_lattices(sK1079)
| ~ l3_lattices(sK1079)
| spl1088_477 ),
inference(forward_subsumption_resolution,[],[f22599,f13633]) ).
fof(f22603,plain,
( ~ v10_lattices(sK1079)
| ~ l3_lattices(sK1079)
| spl1088_477 ),
inference(forward_subsumption_resolution,[],[f22601,f13632]) ).
fof(f22605,plain,
( ~ l3_lattices(sK1079)
| spl1088_477 ),
inference(forward_subsumption_resolution,[],[f22603,f13631]) ).
fof(f22607,plain,
( $false
| spl1088_477 ),
inference(forward_subsumption_resolution,[],[f22605,f13630]) ).
fof(f22608,plain,
spl1088_477,
inference(avatar_contradiction_clause,[],[f22607]) ).
fof(f22610,plain,
( ~ m2_relset_1(sF1085,k2_zfmisc_1(u1_struct_0(sK1079),u1_struct_0(sK1079)),u1_struct_0(sK1079))
| ~ m1_subset_1(sK1080,k1_zfmisc_1(u1_struct_0(sK1079)))
| v1_xboole_0(u1_struct_0(sK1079))
| spl1088_4
| ~ spl1088_350
| ~ spl1088_370 ),
inference(forward_subsumption_resolution,[],[f22469,f18542]) ).
fof(f22612,plain,
( ~ m1_subset_1(sK1080,k1_zfmisc_1(u1_struct_0(sK1079)))
| v1_xboole_0(u1_struct_0(sK1079))
| spl1088_4
| ~ spl1088_350
| ~ spl1088_370 ),
inference(forward_subsumption_resolution,[],[f22610,f18552]) ).
fof(f22614,plain,
( v1_xboole_0(u1_struct_0(sK1079))
| spl1088_4
| ~ spl1088_350
| ~ spl1088_370
| ~ spl1088_477 ),
inference(forward_subsumption_resolution,[],[f22612,f22331]) ).
fof(f22615,plain,
( $false
| spl1088_4
| ~ spl1088_350
| ~ spl1088_370
| spl1088_417
| ~ spl1088_477 ),
inference(forward_subsumption_resolution,[],[f22614,f21604]) ).
fof(f22616,plain,
( spl1088_4
| ~ spl1088_350
| ~ spl1088_370
| spl1088_417
| ~ spl1088_477 ),
inference(avatar_contradiction_clause,[],[f22615]) ).
fof(f22645,plain,
( ~ m2_relset_1(u1_lattices(sK1079),k2_zfmisc_1(u1_struct_0(sK1079),u1_struct_0(sK1079)),u1_struct_0(sK1079))
| ~ v1_funct_2(k1_realset1(u1_lattices(sK1079),sK1080),sF1087,sK1080)
| ~ v1_funct_1(u1_lattices(sK1079))
| ~ m2_relset_1(k1_realset1(u1_lattices(sK1079),sK1080),sF1087,sK1080)
| ~ v1_funct_1(k1_realset1(u1_lattices(sK1079),sK1080))
| r1_lattice2(sK1080,k1_realset1(u1_lattices(sK1079),sK1080),sK1081)
| ~ r1_lattice2(u1_struct_0(sK1079),u1_lattices(sK1079),sF1083)
| v3_struct_0(sK1079)
| ~ v6_lattices(sK1079)
| ~ l1_lattices(sK1079)
| ~ spl1088_478 ),
inference(resolution,[],[f22335,f12806]) ).
fof(f22654,plain,
( ~ m2_relset_1(u1_lattices(sK1079),k2_zfmisc_1(u1_struct_0(sK1079),u1_struct_0(sK1079)),u1_struct_0(sK1079))
| ~ v1_funct_2(k1_realset1(u1_lattices(sK1079),sK1080),sF1087,sK1080)
| ~ m2_relset_1(k1_realset1(u1_lattices(sK1079),sK1080),sF1087,sK1080)
| ~ v1_funct_1(k1_realset1(u1_lattices(sK1079),sK1080))
| r1_lattice2(sK1080,k1_realset1(u1_lattices(sK1079),sK1080),sK1081)
| ~ r1_lattice2(u1_struct_0(sK1079),u1_lattices(sK1079),sF1083)
| v3_struct_0(sK1079)
| ~ v6_lattices(sK1079)
| ~ l1_lattices(sK1079)
| ~ spl1088_478 ),
inference(forward_subsumption_resolution,[],[f22645,f12807]) ).
fof(f22667,plain,
( ~ v1_funct_2(k1_realset1(u1_lattices(sK1079),sK1080),sF1087,sK1080)
| ~ m2_relset_1(k1_realset1(u1_lattices(sK1079),sK1080),sF1087,sK1080)
| ~ v1_funct_1(k1_realset1(u1_lattices(sK1079),sK1080))
| r1_lattice2(sK1080,k1_realset1(u1_lattices(sK1079),sK1080),sK1081)
| ~ r1_lattice2(u1_struct_0(sK1079),u1_lattices(sK1079),sF1083)
| v3_struct_0(sK1079)
| ~ v6_lattices(sK1079)
| ~ l1_lattices(sK1079)
| ~ spl1088_478 ),
inference(forward_subsumption_resolution,[],[f22654,f12485]) ).
fof(f22678,plain,
( ~ v1_funct_2(k1_realset1(u1_lattices(sK1079),sK1080),sF1087,sK1080)
| ~ m2_relset_1(k1_realset1(u1_lattices(sK1079),sK1080),sF1087,sK1080)
| ~ v1_funct_1(k1_realset1(u1_lattices(sK1079),sK1080))
| r1_lattice2(sK1080,k1_realset1(u1_lattices(sK1079),sK1080),sK1081)
| ~ r1_lattice2(u1_struct_0(sK1079),u1_lattices(sK1079),sF1083)
| ~ v6_lattices(sK1079)
| ~ l1_lattices(sK1079)
| ~ spl1088_478 ),
inference(forward_subsumption_resolution,[],[f22667,f13632]) ).
fof(f22736,plain,
( ~ v1_funct_2(k1_realset1(u1_lattices(sK1079),sK1080),sF1087,sK1080)
| ~ m2_relset_1(k1_realset1(u1_lattices(sK1079),sK1080),sF1087,sK1080)
| ~ v1_funct_1(k1_realset1(u1_lattices(sK1079),sK1080))
| r1_lattice2(sK1080,k1_realset1(u1_lattices(sK1079),sK1080),sK1081)
| ~ r1_lattice2(u1_struct_0(sK1079),u1_lattices(sK1079),sF1083)
| ~ l1_lattices(sK1079)
| ~ spl1088_369
| ~ spl1088_478 ),
inference(forward_subsumption_resolution,[],[f22678,f18537]) ).
fof(f22744,plain,
( ~ v1_funct_2(k1_realset1(u1_lattices(sK1079),sK1080),sF1087,sK1080)
| ~ m2_relset_1(k1_realset1(u1_lattices(sK1079),sK1080),sF1087,sK1080)
| ~ v1_funct_1(k1_realset1(u1_lattices(sK1079),sK1080))
| r1_lattice2(sK1080,k1_realset1(u1_lattices(sK1079),sK1080),sK1081)
| ~ r1_lattice2(u1_struct_0(sK1079),u1_lattices(sK1079),sF1083)
| ~ spl1088_350
| ~ spl1088_369
| ~ spl1088_478 ),
inference(forward_subsumption_resolution,[],[f22736,f18229]) ).
fof(f22752,plain,
( ~ v1_funct_2(k1_realset1(sF1085,sK1080),sF1087,sK1080)
| ~ m2_relset_1(k1_realset1(u1_lattices(sK1079),sK1080),sF1087,sK1080)
| ~ v1_funct_1(k1_realset1(u1_lattices(sK1079),sK1080))
| r1_lattice2(sK1080,k1_realset1(u1_lattices(sK1079),sK1080),sK1081)
| ~ r1_lattice2(u1_struct_0(sK1079),u1_lattices(sK1079),sF1083)
| ~ spl1088_350
| ~ spl1088_369
| ~ spl1088_478 ),
inference(forward_demodulation,[],[f22744,f15576]) ).
fof(f22760,plain,
( ~ v1_funct_2(sK1082,sF1087,sK1080)
| ~ m2_relset_1(k1_realset1(u1_lattices(sK1079),sK1080),sF1087,sK1080)
| ~ v1_funct_1(k1_realset1(u1_lattices(sK1079),sK1080))
| r1_lattice2(sK1080,k1_realset1(u1_lattices(sK1079),sK1080),sK1081)
| ~ r1_lattice2(u1_struct_0(sK1079),u1_lattices(sK1079),sF1083)
| ~ spl1088_350
| ~ spl1088_369
| ~ spl1088_478 ),
inference(forward_demodulation,[],[f22752,f17550]) ).
fof(f22768,plain,
( ~ m2_relset_1(k1_realset1(u1_lattices(sK1079),sK1080),sF1087,sK1080)
| ~ v1_funct_1(k1_realset1(u1_lattices(sK1079),sK1080))
| r1_lattice2(sK1080,k1_realset1(u1_lattices(sK1079),sK1080),sK1081)
| ~ r1_lattice2(u1_struct_0(sK1079),u1_lattices(sK1079),sF1083)
| ~ spl1088_350
| ~ spl1088_369
| ~ spl1088_478 ),
inference(forward_subsumption_resolution,[],[f22760,f15582]) ).
fof(f22776,plain,
( ~ m2_relset_1(k1_realset1(sF1085,sK1080),sF1087,sK1080)
| ~ v1_funct_1(k1_realset1(u1_lattices(sK1079),sK1080))
| r1_lattice2(sK1080,k1_realset1(u1_lattices(sK1079),sK1080),sK1081)
| ~ r1_lattice2(u1_struct_0(sK1079),u1_lattices(sK1079),sF1083)
| ~ spl1088_350
| ~ spl1088_369
| ~ spl1088_478 ),
inference(forward_demodulation,[],[f22768,f15576]) ).
fof(f22792,plain,
( ~ m2_relset_1(sK1082,sF1087,sK1080)
| ~ v1_funct_1(k1_realset1(u1_lattices(sK1079),sK1080))
| r1_lattice2(sK1080,k1_realset1(u1_lattices(sK1079),sK1080),sK1081)
| ~ r1_lattice2(u1_struct_0(sK1079),u1_lattices(sK1079),sF1083)
| ~ spl1088_350
| ~ spl1088_369
| ~ spl1088_478 ),
inference(forward_demodulation,[],[f22776,f17550]) ).
fof(f22800,plain,
( ~ v1_funct_1(k1_realset1(u1_lattices(sK1079),sK1080))
| r1_lattice2(sK1080,k1_realset1(u1_lattices(sK1079),sK1080),sK1081)
| ~ r1_lattice2(u1_struct_0(sK1079),u1_lattices(sK1079),sF1083)
| ~ spl1088_350
| ~ spl1088_369
| ~ spl1088_478 ),
inference(forward_subsumption_resolution,[],[f22792,f15583]) ).
fof(f22806,plain,
( ~ v1_funct_1(k1_realset1(sF1085,sK1080))
| r1_lattice2(sK1080,k1_realset1(u1_lattices(sK1079),sK1080),sK1081)
| ~ r1_lattice2(u1_struct_0(sK1079),u1_lattices(sK1079),sF1083)
| ~ spl1088_350
| ~ spl1088_369
| ~ spl1088_478 ),
inference(forward_demodulation,[],[f22800,f15576]) ).
fof(f22812,plain,
( ~ v1_funct_1(sK1082)
| r1_lattice2(sK1080,k1_realset1(u1_lattices(sK1079),sK1080),sK1081)
| ~ r1_lattice2(u1_struct_0(sK1079),u1_lattices(sK1079),sF1083)
| ~ spl1088_350
| ~ spl1088_369
| ~ spl1088_478 ),
inference(forward_demodulation,[],[f22806,f17550]) ).
fof(f22818,plain,
( r1_lattice2(sK1080,k1_realset1(u1_lattices(sK1079),sK1080),sK1081)
| ~ r1_lattice2(u1_struct_0(sK1079),u1_lattices(sK1079),sF1083)
| ~ spl1088_350
| ~ spl1088_369
| ~ spl1088_478 ),
inference(forward_subsumption_resolution,[],[f22812,f13640]) ).
fof(f22824,plain,
( r1_lattice2(sK1080,k1_realset1(sF1085,sK1080),sK1081)
| ~ r1_lattice2(u1_struct_0(sK1079),u1_lattices(sK1079),sF1083)
| ~ spl1088_350
| ~ spl1088_369
| ~ spl1088_478 ),
inference(forward_demodulation,[],[f22818,f15576]) ).
fof(f22830,plain,
( r1_lattice2(sK1080,sK1082,sK1081)
| ~ r1_lattice2(u1_struct_0(sK1079),u1_lattices(sK1079),sF1083)
| ~ spl1088_350
| ~ spl1088_369
| ~ spl1088_478 ),
inference(forward_demodulation,[],[f22824,f17550]) ).
fof(f22837,plain,
( ~ r1_lattice2(u1_struct_0(sK1079),u1_lattices(sK1079),sF1083)
| spl1088_1
| ~ spl1088_350
| ~ spl1088_369
| ~ spl1088_478 ),
inference(forward_subsumption_resolution,[],[f22830,f15651]) ).
fof(f22841,plain,
( ~ r1_lattice2(u1_struct_0(sK1079),sF1085,sF1083)
| spl1088_1
| ~ spl1088_350
| ~ spl1088_369
| ~ spl1088_478 ),
inference(forward_demodulation,[],[f22837,f15576]) ).
fof(f22846,plain,
( $false
| spl1088_1
| ~ spl1088_350
| ~ spl1088_369
| ~ spl1088_478 ),
inference(forward_subsumption_resolution,[],[f22841,f18466]) ).
fof(f22847,plain,
( spl1088_1
| ~ spl1088_350
| ~ spl1088_369
| ~ spl1088_478 ),
inference(avatar_contradiction_clause,[],[f22846]) ).
fof(f23739,plain,
( ! [X0] :
( ~ v1_funct_2(sF1085,k2_zfmisc_1(X0,X0),X0)
| v3_struct_0(k1_lattice2(sK1079))
| ~ v10_lattices(k1_lattice2(sK1079))
| ~ l3_lattices(k1_lattice2(sK1079))
| ~ r1_lattice2(X0,sF1083,sF1085)
| r1_lattice2(sK1080,sK1081,k1_realset1(sF1085,sK1080))
| ~ v1_funct_1(sF1085)
| ~ m2_lattice4(sK1080,k1_lattice2(sK1079))
| ~ m2_relset_1(sF1085,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(sF1083,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(sF1083,k2_zfmisc_1(X0,X0),X0)
| ~ m1_subset_1(sK1080,k1_zfmisc_1(X0))
| v1_xboole_0(X0) )
| ~ spl1088_347 ),
inference(superposition,[],[f22566,f18384]) ).
fof(f23746,plain,
( ! [X0] :
( ~ v1_funct_2(sF1085,k2_zfmisc_1(X0,X0),X0)
| ~ v10_lattices(k1_lattice2(sK1079))
| ~ l3_lattices(k1_lattice2(sK1079))
| ~ r1_lattice2(X0,sF1083,sF1085)
| r1_lattice2(sK1080,sK1081,k1_realset1(sF1085,sK1080))
| ~ v1_funct_1(sF1085)
| ~ m2_lattice4(sK1080,k1_lattice2(sK1079))
| ~ m2_relset_1(sF1085,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(sF1083,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(sF1083,k2_zfmisc_1(X0,X0),X0)
| ~ m1_subset_1(sK1080,k1_zfmisc_1(X0))
| v1_xboole_0(X0) )
| ~ spl1088_347
| spl1088_355 ),
inference(forward_subsumption_resolution,[],[f23739,f18323]) ).
fof(f23751,plain,
( ! [X0] :
( ~ v1_funct_2(sF1085,k2_zfmisc_1(X0,X0),X0)
| ~ l3_lattices(k1_lattice2(sK1079))
| ~ r1_lattice2(X0,sF1083,sF1085)
| r1_lattice2(sK1080,sK1081,k1_realset1(sF1085,sK1080))
| ~ v1_funct_1(sF1085)
| ~ m2_lattice4(sK1080,k1_lattice2(sK1079))
| ~ m2_relset_1(sF1085,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(sF1083,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(sF1083,k2_zfmisc_1(X0,X0),X0)
| ~ m1_subset_1(sK1080,k1_zfmisc_1(X0))
| v1_xboole_0(X0) )
| ~ spl1088_347
| spl1088_355
| ~ spl1088_365 ),
inference(forward_subsumption_resolution,[],[f23746,f18442]) ).
fof(f23756,plain,
( ! [X0] :
( ~ v1_funct_2(sF1085,k2_zfmisc_1(X0,X0),X0)
| ~ r1_lattice2(X0,sF1083,sF1085)
| r1_lattice2(sK1080,sK1081,k1_realset1(sF1085,sK1080))
| ~ v1_funct_1(sF1085)
| ~ m2_lattice4(sK1080,k1_lattice2(sK1079))
| ~ m2_relset_1(sF1085,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(sF1083,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(sF1083,k2_zfmisc_1(X0,X0),X0)
| ~ m1_subset_1(sK1080,k1_zfmisc_1(X0))
| v1_xboole_0(X0) )
| ~ spl1088_347
| spl1088_355
| ~ spl1088_364
| ~ spl1088_365 ),
inference(forward_subsumption_resolution,[],[f23751,f18438]) ).
fof(f23761,plain,
( ! [X0] :
( ~ v1_funct_2(sF1085,k2_zfmisc_1(X0,X0),X0)
| ~ r1_lattice2(X0,sF1083,sF1085)
| r1_lattice2(sK1080,sK1081,k1_realset1(sF1085,sK1080))
| ~ m2_lattice4(sK1080,k1_lattice2(sK1079))
| ~ m2_relset_1(sF1085,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(sF1083,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(sF1083,k2_zfmisc_1(X0,X0),X0)
| ~ m1_subset_1(sK1080,k1_zfmisc_1(X0))
| v1_xboole_0(X0) )
| ~ spl1088_347
| ~ spl1088_350
| spl1088_355
| ~ spl1088_364
| ~ spl1088_365 ),
inference(forward_subsumption_resolution,[],[f23756,f18532]) ).
fof(f23766,plain,
( ! [X0] :
( ~ v1_funct_2(sF1085,k2_zfmisc_1(X0,X0),X0)
| ~ r1_lattice2(X0,sF1083,sF1085)
| r1_lattice2(sK1080,sK1081,k1_realset1(sF1085,sK1080))
| ~ m2_relset_1(sF1085,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(sF1083,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(sF1083,k2_zfmisc_1(X0,X0),X0)
| ~ m1_subset_1(sK1080,k1_zfmisc_1(X0))
| v1_xboole_0(X0) )
| ~ spl1088_347
| ~ spl1088_350
| spl1088_355
| ~ spl1088_364
| ~ spl1088_365 ),
inference(forward_subsumption_resolution,[],[f23761,f20376]) ).
fof(f23771,plain,
( ! [X0] :
( r1_lattice2(sK1080,sK1081,sK1082)
| ~ v1_funct_2(sF1085,k2_zfmisc_1(X0,X0),X0)
| ~ r1_lattice2(X0,sF1083,sF1085)
| ~ m2_relset_1(sF1085,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(sF1083,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(sF1083,k2_zfmisc_1(X0,X0),X0)
| ~ m1_subset_1(sK1080,k1_zfmisc_1(X0))
| v1_xboole_0(X0) )
| ~ spl1088_347
| ~ spl1088_350
| spl1088_355
| ~ spl1088_364
| ~ spl1088_365 ),
inference(forward_demodulation,[],[f23766,f17550]) ).
fof(f23773,plain,
( ! [X0] :
( ~ v1_funct_2(sF1085,k2_zfmisc_1(X0,X0),X0)
| ~ r1_lattice2(X0,sF1083,sF1085)
| ~ m2_relset_1(sF1085,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(sF1083,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(sF1083,k2_zfmisc_1(X0,X0),X0)
| ~ m1_subset_1(sK1080,k1_zfmisc_1(X0))
| v1_xboole_0(X0) )
| spl1088_2
| ~ spl1088_347
| ~ spl1088_350
| spl1088_355
| ~ spl1088_364
| ~ spl1088_365 ),
inference(forward_subsumption_resolution,[],[f23771,f15655]) ).
fof(f23984,plain,
( ~ r1_lattice2(u1_struct_0(sK1079),sF1083,sF1085)
| ~ m2_relset_1(sF1085,k2_zfmisc_1(u1_struct_0(sK1079),u1_struct_0(sK1079)),u1_struct_0(sK1079))
| ~ v1_funct_2(sF1083,k2_zfmisc_1(u1_struct_0(sK1079),u1_struct_0(sK1079)),u1_struct_0(sK1079))
| ~ m2_relset_1(sF1083,k2_zfmisc_1(u1_struct_0(sK1079),u1_struct_0(sK1079)),u1_struct_0(sK1079))
| ~ m1_subset_1(sK1080,k1_zfmisc_1(u1_struct_0(sK1079)))
| v1_xboole_0(u1_struct_0(sK1079))
| spl1088_2
| ~ spl1088_347
| ~ spl1088_350
| spl1088_355
| ~ spl1088_364
| ~ spl1088_365 ),
inference(resolution,[],[f23773,f18533]) ).
fof(f23986,plain,
( ~ m2_relset_1(sF1085,k2_zfmisc_1(u1_struct_0(sK1079),u1_struct_0(sK1079)),u1_struct_0(sK1079))
| ~ v1_funct_2(sF1083,k2_zfmisc_1(u1_struct_0(sK1079),u1_struct_0(sK1079)),u1_struct_0(sK1079))
| ~ m2_relset_1(sF1083,k2_zfmisc_1(u1_struct_0(sK1079),u1_struct_0(sK1079)),u1_struct_0(sK1079))
| ~ m1_subset_1(sK1080,k1_zfmisc_1(u1_struct_0(sK1079)))
| v1_xboole_0(u1_struct_0(sK1079))
| spl1088_2
| ~ spl1088_347
| ~ spl1088_350
| spl1088_355
| ~ spl1088_364
| ~ spl1088_365 ),
inference(forward_subsumption_resolution,[],[f23984,f18454]) ).
fof(f23987,plain,
( ~ v1_funct_2(sF1083,k2_zfmisc_1(u1_struct_0(sK1079),u1_struct_0(sK1079)),u1_struct_0(sK1079))
| ~ m2_relset_1(sF1083,k2_zfmisc_1(u1_struct_0(sK1079),u1_struct_0(sK1079)),u1_struct_0(sK1079))
| ~ m1_subset_1(sK1080,k1_zfmisc_1(u1_struct_0(sK1079)))
| v1_xboole_0(u1_struct_0(sK1079))
| spl1088_2
| ~ spl1088_347
| ~ spl1088_350
| spl1088_355
| ~ spl1088_364
| ~ spl1088_365 ),
inference(forward_subsumption_resolution,[],[f23986,f18552]) ).
fof(f23988,plain,
( ~ m2_relset_1(sF1083,k2_zfmisc_1(u1_struct_0(sK1079),u1_struct_0(sK1079)),u1_struct_0(sK1079))
| ~ m1_subset_1(sK1080,k1_zfmisc_1(u1_struct_0(sK1079)))
| v1_xboole_0(u1_struct_0(sK1079))
| spl1088_2
| ~ spl1088_347
| ~ spl1088_350
| spl1088_355
| ~ spl1088_364
| ~ spl1088_365 ),
inference(forward_subsumption_resolution,[],[f23987,f18491]) ).
fof(f23989,plain,
( ~ m1_subset_1(sK1080,k1_zfmisc_1(u1_struct_0(sK1079)))
| v1_xboole_0(u1_struct_0(sK1079))
| spl1088_2
| ~ spl1088_347
| ~ spl1088_350
| spl1088_355
| ~ spl1088_364
| ~ spl1088_365 ),
inference(forward_subsumption_resolution,[],[f23988,f18514]) ).
fof(f23990,plain,
( v1_xboole_0(u1_struct_0(sK1079))
| spl1088_2
| ~ spl1088_347
| ~ spl1088_350
| spl1088_355
| ~ spl1088_364
| ~ spl1088_365
| ~ spl1088_477 ),
inference(forward_subsumption_resolution,[],[f23989,f22331]) ).
fof(f23991,plain,
( $false
| spl1088_2
| ~ spl1088_347
| ~ spl1088_350
| spl1088_355
| ~ spl1088_364
| ~ spl1088_365
| spl1088_417
| ~ spl1088_477 ),
inference(forward_subsumption_resolution,[],[f23990,f21604]) ).
fof(f23992,plain,
( spl1088_2
| ~ spl1088_347
| ~ spl1088_350
| spl1088_355
| ~ spl1088_364
| ~ spl1088_365
| spl1088_417
| ~ spl1088_477 ),
inference(avatar_contradiction_clause,[],[f23991]) ).
fof(f23999,plain,
( v1_xboole_0(u1_struct_0(sK1079))
| ~ m1_subset_1(sK1080,k1_zfmisc_1(u1_struct_0(sK1079)))
| ~ m2_relset_1(sF1083,k2_zfmisc_1(u1_struct_0(sK1079),u1_struct_0(sK1079)),u1_struct_0(sK1079))
| ~ v2_binop_1(sF1083,u1_struct_0(sK1079))
| ~ spl1088_347
| ~ spl1088_467 ),
inference(resolution,[],[f22271,f18491]) ).
fof(f24001,plain,
( ~ m1_subset_1(sK1080,k1_zfmisc_1(u1_struct_0(sK1079)))
| ~ m2_relset_1(sF1083,k2_zfmisc_1(u1_struct_0(sK1079),u1_struct_0(sK1079)),u1_struct_0(sK1079))
| ~ v2_binop_1(sF1083,u1_struct_0(sK1079))
| ~ spl1088_347
| spl1088_417
| ~ spl1088_467 ),
inference(forward_subsumption_resolution,[],[f23999,f21604]) ).
fof(f24002,plain,
( ~ m2_relset_1(sF1083,k2_zfmisc_1(u1_struct_0(sK1079),u1_struct_0(sK1079)),u1_struct_0(sK1079))
| ~ v2_binop_1(sF1083,u1_struct_0(sK1079))
| ~ spl1088_347
| spl1088_417
| ~ spl1088_467
| ~ spl1088_477 ),
inference(forward_subsumption_resolution,[],[f24001,f22331]) ).
fof(f24003,plain,
( ~ v2_binop_1(sF1083,u1_struct_0(sK1079))
| ~ spl1088_347
| spl1088_417
| ~ spl1088_467
| ~ spl1088_477 ),
inference(forward_subsumption_resolution,[],[f24002,f18514]) ).
fof(f24004,plain,
( $false
| ~ spl1088_347
| ~ spl1088_349
| spl1088_417
| ~ spl1088_467
| ~ spl1088_477 ),
inference(forward_subsumption_resolution,[],[f24003,f18223]) ).
fof(f24005,plain,
( ~ spl1088_347
| ~ spl1088_349
| spl1088_417
| ~ spl1088_467
| ~ spl1088_477 ),
inference(avatar_contradiction_clause,[],[f24004]) ).
fof(f24006,plain,
( v1_xboole_0(u1_struct_0(sK1079))
| ~ m1_subset_1(sK1080,k1_zfmisc_1(u1_struct_0(sK1079)))
| ~ m2_relset_1(sF1083,k2_zfmisc_1(u1_struct_0(sK1079),u1_struct_0(sK1079)),u1_struct_0(sK1079))
| ~ v1_binop_1(sF1083,u1_struct_0(sK1079))
| ~ spl1088_347
| ~ spl1088_468 ),
inference(resolution,[],[f22276,f18491]) ).
fof(f24008,plain,
( ~ m1_subset_1(sK1080,k1_zfmisc_1(u1_struct_0(sK1079)))
| ~ m2_relset_1(sF1083,k2_zfmisc_1(u1_struct_0(sK1079),u1_struct_0(sK1079)),u1_struct_0(sK1079))
| ~ v1_binop_1(sF1083,u1_struct_0(sK1079))
| ~ spl1088_347
| spl1088_417
| ~ spl1088_468 ),
inference(forward_subsumption_resolution,[],[f24006,f21604]) ).
fof(f24009,plain,
( ~ m2_relset_1(sF1083,k2_zfmisc_1(u1_struct_0(sK1079),u1_struct_0(sK1079)),u1_struct_0(sK1079))
| ~ v1_binop_1(sF1083,u1_struct_0(sK1079))
| ~ spl1088_347
| spl1088_417
| ~ spl1088_468
| ~ spl1088_477 ),
inference(forward_subsumption_resolution,[],[f24008,f22331]) ).
fof(f24010,plain,
( ~ v1_binop_1(sF1083,u1_struct_0(sK1079))
| ~ spl1088_347
| spl1088_417
| ~ spl1088_468
| ~ spl1088_477 ),
inference(forward_subsumption_resolution,[],[f24009,f18514]) ).
fof(f24011,plain,
( $false
| ~ spl1088_347
| ~ spl1088_368
| spl1088_417
| ~ spl1088_468
| ~ spl1088_477 ),
inference(forward_subsumption_resolution,[],[f24010,f18480]) ).
fof(f24012,plain,
( ~ spl1088_347
| ~ spl1088_368
| spl1088_417
| ~ spl1088_468
| ~ spl1088_477 ),
inference(avatar_contradiction_clause,[],[f24011]) ).
fof(f24013,plain,
( v1_xboole_0(u1_struct_0(sK1079))
| ~ m1_subset_1(sK1080,k1_zfmisc_1(u1_struct_0(sK1079)))
| ~ m2_relset_1(sF1085,k2_zfmisc_1(u1_struct_0(sK1079),u1_struct_0(sK1079)),u1_struct_0(sK1079))
| ~ v2_binop_1(sF1085,u1_struct_0(sK1079))
| ~ spl1088_350
| ~ spl1088_466 ),
inference(resolution,[],[f22267,f18533]) ).
fof(f24015,plain,
( ~ m1_subset_1(sK1080,k1_zfmisc_1(u1_struct_0(sK1079)))
| ~ m2_relset_1(sF1085,k2_zfmisc_1(u1_struct_0(sK1079),u1_struct_0(sK1079)),u1_struct_0(sK1079))
| ~ v2_binop_1(sF1085,u1_struct_0(sK1079))
| ~ spl1088_350
| spl1088_417
| ~ spl1088_466 ),
inference(forward_subsumption_resolution,[],[f24013,f21604]) ).
fof(f24016,plain,
( ~ m2_relset_1(sF1085,k2_zfmisc_1(u1_struct_0(sK1079),u1_struct_0(sK1079)),u1_struct_0(sK1079))
| ~ v2_binop_1(sF1085,u1_struct_0(sK1079))
| ~ spl1088_350
| spl1088_417
| ~ spl1088_466
| ~ spl1088_477 ),
inference(forward_subsumption_resolution,[],[f24015,f22331]) ).
fof(f24017,plain,
( ~ v2_binop_1(sF1085,u1_struct_0(sK1079))
| ~ spl1088_350
| spl1088_417
| ~ spl1088_466
| ~ spl1088_477 ),
inference(forward_subsumption_resolution,[],[f24016,f18552]) ).
fof(f24018,plain,
( $false
| ~ spl1088_350
| ~ spl1088_352
| spl1088_417
| ~ spl1088_466
| ~ spl1088_477 ),
inference(forward_subsumption_resolution,[],[f24017,f18238]) ).
fof(f24019,plain,
( ~ spl1088_350
| ~ spl1088_352
| spl1088_417
| ~ spl1088_466
| ~ spl1088_477 ),
inference(avatar_contradiction_clause,[],[f24018]) ).
cnf(s1,plain,
( ~ spl1088_1
| ~ spl1088_2
| ~ spl1088_3
| ~ spl1088_4
| ~ spl1088_5
| ~ spl1088_6 ),
inference(sat_conversion,[],[f15672]) ).
cnf(s296,plain,
( ~ spl1088_347
| ~ spl1088_348
| spl1088_349 ),
inference(sat_conversion,[],[f18224]) ).
cnf(s297,plain,
( ~ spl1088_350
| ~ spl1088_351
| spl1088_352 ),
inference(sat_conversion,[],[f18239]) ).
cnf(s304,plain,
spl1088_347,
inference(sat_conversion,[],[f18470]) ).
cnf(s305,plain,
( ~ spl1088_347
| ~ spl1088_367
| spl1088_368 ),
inference(sat_conversion,[],[f18481]) ).
cnf(s306,plain,
spl1088_350,
inference(sat_conversion,[],[f18530]) ).
cnf(s307,plain,
( ~ spl1088_350
| ~ spl1088_369
| spl1088_370 ),
inference(sat_conversion,[],[f18543]) ).
cnf(s318,plain,
spl1088_364,
inference(sat_conversion,[],[f18966]) ).
cnf(s324,plain,
~ spl1088_355,
inference(sat_conversion,[],[f19013]) ).
cnf(s344,plain,
spl1088_367,
inference(sat_conversion,[],[f19732]) ).
cnf(s345,plain,
spl1088_351,
inference(sat_conversion,[],[f19779]) ).
cnf(s346,plain,
spl1088_348,
inference(sat_conversion,[],[f19793]) ).
cnf(s349,plain,
spl1088_365,
inference(sat_conversion,[],[f20094]) ).
cnf(s354,plain,
spl1088_369,
inference(sat_conversion,[],[f20268]) ).
cnf(s386,plain,
( spl1088_355
| ~ spl1088_364
| ~ spl1088_365
| ~ spl1088_417 ),
inference(sat_conversion,[],[f22091]) ).
cnf(s403,plain,
( spl1088_3
| ~ spl1088_350
| spl1088_466 ),
inference(sat_conversion,[],[f22268]) ).
cnf(s404,plain,
( spl1088_5
| ~ spl1088_347
| spl1088_467 ),
inference(sat_conversion,[],[f22272]) ).
cnf(s405,plain,
( spl1088_6
| ~ spl1088_347
| spl1088_468 ),
inference(sat_conversion,[],[f22277]) ).
cnf(s409,plain,
( ~ spl1088_347
| spl1088_417
| ~ spl1088_477
| spl1088_478 ),
inference(sat_conversion,[],[f22336]) ).
cnf(s413,plain,
spl1088_477,
inference(sat_conversion,[],[f22608]) ).
cnf(s414,plain,
( spl1088_4
| ~ spl1088_350
| ~ spl1088_370
| spl1088_417
| ~ spl1088_477 ),
inference(sat_conversion,[],[f22616]) ).
cnf(s424,plain,
( spl1088_1
| ~ spl1088_350
| ~ spl1088_369
| ~ spl1088_478 ),
inference(sat_conversion,[],[f22847]) ).
cnf(s427,plain,
( spl1088_2
| ~ spl1088_347
| ~ spl1088_350
| spl1088_355
| ~ spl1088_364
| ~ spl1088_365
| spl1088_417
| ~ spl1088_477 ),
inference(sat_conversion,[],[f23992]) ).
cnf(s428,plain,
( ~ spl1088_347
| ~ spl1088_349
| spl1088_417
| ~ spl1088_467
| ~ spl1088_477 ),
inference(sat_conversion,[],[f24005]) ).
cnf(s429,plain,
( ~ spl1088_347
| ~ spl1088_368
| spl1088_417
| ~ spl1088_468
| ~ spl1088_477 ),
inference(sat_conversion,[],[f24012]) ).
cnf(s430,plain,
( ~ spl1088_350
| ~ spl1088_352
| spl1088_417
| ~ spl1088_466
| ~ spl1088_477 ),
inference(sat_conversion,[],[f24019]) ).
cnf(s431,plain,
( ~ spl1088_347
| spl1088_417
| spl1088_478 ),
inference(rat,[],[s409,s413]) ).
cnf(s448,plain,
~ spl1088_417,
inference(rat,[],[s386,s324,s349,s318]) ).
cnf(s459,plain,
( ~ spl1088_350
| spl1088_370 ),
inference(rat,[],[s307,s354]) ).
cnf(s462,plain,
spl1088_370,
inference(rat,[],[s459,s306]) ).
cnf(s464,plain,
spl1088_4,
inference(rat,[],[s414,s413,s448,s306,s462]) ).
cnf(s465,plain,
( ~ spl1088_347
| spl1088_368 ),
inference(rat,[],[s305,s344]) ).
cnf(s466,plain,
spl1088_2,
inference(rat,[],[s427,s413,s448,s349,s318,s324,s306,s304]) ).
cnf(s467,plain,
spl1088_478,
inference(rat,[],[s431,s448,s304]) ).
cnf(s471,plain,
spl1088_368,
inference(rat,[],[s465,s304]) ).
cnf(s472,plain,
spl1088_1,
inference(rat,[],[s424,s306,s354,s467]) ).
cnf(s475,plain,
~ spl1088_468,
inference(rat,[],[s429,s413,s304,s448,s471]) ).
cnf(s477,plain,
spl1088_6,
inference(rat,[],[s405,s304,s475]) ).
cnf(s483,plain,
spl1088_352,
inference(rat,[],[s297,s345,s306]) ).
cnf(s484,plain,
~ spl1088_466,
inference(rat,[],[s430,s413,s306,s448,s483]) ).
cnf(s485,plain,
spl1088_3,
inference(rat,[],[s403,s306,s484]) ).
cnf(s486,plain,
spl1088_349,
inference(rat,[],[s296,s346,s304]) ).
cnf(s487,plain,
~ spl1088_467,
inference(rat,[],[s428,s413,s304,s448,s486]) ).
cnf(s488,plain,
spl1088_5,
inference(rat,[],[s404,s304,s487]) ).
cnf(s498,plain,
$false,
inference(rat,[],[s1,s477,s488,s464,s485,s466,s472]) ).
fof(f24020,plain,
$false,
inference(avatar_sat_refutation,[],[s498]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT326+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 : n009.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:38:46 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.41 Running first-order theorem proving
% 0.12/0.41 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
% 10.38/2.17 % (2106706)Detected formulas, will run a generic FOF schedule.
% 10.38/2.17 % (2106716)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3157402211:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 10.38/2.17 % (2106715)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3749792357:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 10.38/2.17 % (2106717)dis-21_1_sil=8000:lcm=predicate:random_seed=2630835533:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 10.38/2.17 % (2106713)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=2384119412:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 10.38/2.17 % (2106714)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=4155167113:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 10.38/2.17 % (2106712)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=3867617197:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 10.38/2.17 % (2106711)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=3392341922:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 10.38/2.17 % (2106716)Instruction limit reached!
% 10.38/2.17 % (2106716)------------------------------
% 10.38/2.17 % (2106716)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.38/2.17 % (2106716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.38/2.17 % (2106716)CaDiCaL version: 2.1.3
% 10.38/2.17 % (2106716)Termination reason: Instruction limit
% 10.38/2.17 % (2106716)Termination phase: Property scanning
% 10.38/2.17 % (2106716)Time elapsed: 0.048 s
% 10.38/2.17 % (2106716)Peak memory usage: 94 MB
% 10.38/2.17 % (2106716)Instructions burned: 142 (million)
% 10.38/2.17 % (2106714)Instruction limit reached!
% 10.38/2.17 % (2106714)------------------------------
% 10.38/2.17 % (2106714)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.38/2.17 % (2106714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.38/2.17 % (2106714)CaDiCaL version: 2.1.3
% 10.38/2.17 % (2106714)Termination reason: Instruction limit
% 10.38/2.17 % (2106714)Termination phase: Saturation
% 10.38/2.17 % (2106714)Time elapsed: 0.065 s
% 10.38/2.17 % (2106714)Peak memory usage: 92 MB
% 10.38/2.17 % (2106714)Instructions burned: 110 (million)
% 10.38/2.17 % (2106715)Instruction limit reached!
% 10.38/2.17 % (2106715)------------------------------
% 10.38/2.17 % (2106715)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.38/2.17 % (2106715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.38/2.17 % (2106715)CaDiCaL version: 2.1.3
% 10.38/2.17 % (2106715)Termination reason: Instruction limit
% 10.38/2.17 % (2106715)Termination phase: Saturation
% 10.38/2.17 % (2106715)Time elapsed: 0.074 s
% 10.38/2.17 % (2106715)Peak memory usage: 93 MB
% 10.38/2.17 % (2106715)Instructions burned: 120 (million)
% 10.38/2.17 % (2106717)Instruction limit reached!
% 10.38/2.17 % (2106717)------------------------------
% 10.38/2.17 % (2106717)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.38/2.17 % (2106717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.38/2.17 % (2106717)CaDiCaL version: 2.1.3
% 10.38/2.17 % (2106717)Termination reason: Instruction limit
% 10.38/2.17 % (2106717)Termination phase: Property scanning
% 10.38/2.17 % (2106717)Time elapsed: 0.077 s
% 10.38/2.17 % (2106717)Peak memory usage: 93 MB
% 10.38/2.17 % (2106717)Instructions burned: 129 (million)
% 10.38/2.17 % (2106725)lrs+10_1_sil=8000:sp=occurrence:random_seed=3103789264:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 10.38/2.17 % (2106727)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2973556801:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 10.38/2.17 % (2106726)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2735857595:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 10.38/2.17 % (2106728)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=393293314:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 10.38/2.17 % (2106725)Instruction limit reached!
% 14.95/2.88 % (2106725)------------------------------
% 14.95/2.88 % (2106725)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.95/2.88 % (2106725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.95/2.88 % (2106725)CaDiCaL version: 2.1.3
% 14.95/2.88 % (2106725)Termination reason: Instruction limit
% 14.95/2.88 % (2106725)Termination phase: Saturation
% 14.95/2.88 % (2106725)Time elapsed: 0.103 s
% 14.95/2.88 % (2106725)Peak memory usage: 96 MB
% 14.95/2.88 % (2106725)Instructions burned: 286 (million)
% 14.95/2.88 % (2106726)Instruction limit reached!
% 14.95/2.88 % (2106726)------------------------------
% 14.95/2.88 % (2106726)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.95/2.88 % (2106726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.95/2.88 % (2106726)CaDiCaL version: 2.1.3
% 14.95/2.88 % (2106726)Termination reason: Instruction limit
% 14.95/2.88 % (2106726)Termination phase: Saturation
% 14.95/2.88 % (2106726)Time elapsed: 0.084 s
% 14.95/2.88 % (2106726)Peak memory usage: 93 MB
% 14.95/2.88 % (2106726)Instructions burned: 158 (million)
% 14.95/2.88 % (2106733)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1125320771:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 14.95/2.88 % (2106728)Instruction limit reached!
% 14.95/2.88 % (2106728)------------------------------
% 14.95/2.88 % (2106728)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.95/2.88 % (2106728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.95/2.88 % (2106728)CaDiCaL version: 2.1.3
% 14.95/2.88 % (2106728)Termination reason: Instruction limit
% 14.95/2.88 % (2106728)Termination phase: Saturation
% 14.95/2.88 % (2106728)Time elapsed: 0.138 s
% 14.95/2.88 % (2106728)Peak memory usage: 97 MB
% 14.95/2.88 % (2106728)Instructions burned: 249 (million)
% 14.95/2.88 % (2106727)Instruction limit reached!
% 14.95/2.88 % (2106727)------------------------------
% 14.95/2.88 % (2106727)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.95/2.88 % (2106727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.95/2.88 % (2106727)CaDiCaL version: 2.1.3
% 14.95/2.88 % (2106727)Termination reason: Instruction limit
% 14.95/2.88 % (2106727)Termination phase: Saturation
% 14.95/2.88 % (2106727)Time elapsed: 0.204 s
% 14.95/2.88 % (2106727)Peak memory usage: 94 MB
% 14.95/2.88 % (2106727)Instructions burned: 325 (million)
% 14.95/2.88 % (2106733)Instruction limit reached!
% 14.95/2.88 % (2106733)------------------------------
% 14.95/2.88 % (2106733)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.95/2.88 % (2106733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.95/2.88 % (2106733)CaDiCaL version: 2.1.3
% 14.95/2.88 % (2106733)Termination reason: Instruction limit
% 14.95/2.88 % (2106733)Termination phase: Saturation
% 14.95/2.88 % (2106733)Time elapsed: 0.086 s
% 14.95/2.88 % (2106733)Peak memory usage: 96 MB
% 14.95/2.88 % (2106733)Instructions burned: 294 (million)
% 14.95/2.88 % (2106734)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1349739014:i=2350_2995 on theBenchmark for (2995ds/2350Mi)
% 14.95/2.88 % (2106736)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3436030339:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 14.95/2.88 % (2106739)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=4276453093:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2994 on theBenchmark for (2994ds/114Mi)
% 14.95/2.88 % (2106738)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=358133252:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi)
% 14.95/2.88 % (2106739)Instruction limit reached!
% 14.95/2.88 % (2106739)------------------------------
% 14.95/2.88 % (2106739)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.95/2.88 % (2106739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.95/2.88 % (2106739)CaDiCaL version: 2.1.3
% 14.95/2.88 % (2106739)Termination reason: Instruction limit
% 14.95/2.88 % (2106739)Termination phase: Property scanning
% 14.95/2.88 % (2106739)Time elapsed: 0.030 s
% 14.95/2.88 % (2106739)Peak memory usage: 91 MB
% 14.95/2.88 % (2106739)Instructions burned: 116 (million)
% 14.95/2.88 % (2106736)Instruction limit reached!
% 14.95/2.88 % (2106736)------------------------------
% 14.95/2.88 % (2106736)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.24/3.88 % (2106736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.24/3.88 % (2106736)CaDiCaL version: 2.1.3
% 22.24/3.88 % (2106736)Termination reason: Instruction limit
% 22.24/3.88 % (2106736)Termination phase: Saturation
% 22.24/3.88 % (2106736)Time elapsed: 0.115 s
% 22.24/3.88 % (2106736)Peak memory usage: 93 MB
% 22.24/3.88 % (2106736)Instructions burned: 113 (million)
% 22.24/3.88 % (2106738)Instruction limit reached!
% 22.24/3.88 % (2106738)------------------------------
% 22.24/3.88 % (2106738)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.24/3.88 % (2106738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.24/3.88 % (2106738)CaDiCaL version: 2.1.3
% 22.24/3.88 % (2106738)Termination reason: Instruction limit
% 22.24/3.88 % (2106738)Termination phase: Property scanning
% 22.24/3.88 % (2106738)Time elapsed: 0.076 s
% 22.24/3.88 % (2106738)Peak memory usage: 94 MB
% 22.24/3.88 % (2106738)Instructions burned: 127 (million)
% 22.24/3.88 % (2106743)lrs+10_1_sil=8000:sp=occurrence:random_seed=3871570500:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2992 on theBenchmark for (2992ds/907Mi)
% 22.24/3.88 % (2106744)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1257765819:i=437:sd=1:aac=none:ss=included_2992 on theBenchmark for (2992ds/437Mi)
% 22.24/3.88 % (2106745)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=666700726:i=5202:ss=axioms:sgt=16_2991 on theBenchmark for (2991ds/5202Mi)
% 22.24/3.88 % (2106744)Instruction limit reached!
% 22.24/3.88 % (2106744)------------------------------
% 22.24/3.88 % (2106744)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.24/3.88 % (2106744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.24/3.88 % (2106744)CaDiCaL version: 2.1.3
% 22.24/3.88 % (2106744)Termination reason: Instruction limit
% 22.24/3.88 % (2106744)Termination phase: Saturation
% 22.24/3.88 % (2106744)Time elapsed: 0.234 s
% 22.24/3.88 % (2106744)Peak memory usage: 95 MB
% 22.24/3.88 % (2106744)Instructions burned: 437 (million)
% 22.24/3.88 % (2106743)Instruction limit reached!
% 22.24/3.88 % (2106743)------------------------------
% 22.24/3.88 % (2106743)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.24/3.88 % (2106743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.24/3.88 % (2106743)CaDiCaL version: 2.1.3
% 22.24/3.88 % (2106743)Termination reason: Instruction limit
% 22.24/3.88 % (2106743)Termination phase: Saturation
% 22.24/3.88 % (2106743)Time elapsed: 0.327 s
% 22.24/3.88 % (2106743)Peak memory usage: 104 MB
% 22.24/3.88 % (2106743)Instructions burned: 911 (million)
% 22.24/3.88 % (2106749)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2350697701:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2988 on theBenchmark for (2988ds/134Mi)
% 22.24/3.88 % (2106750)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1703647308:st=8:i=592:sd=3:ep=RST:ss=axioms_2988 on theBenchmark for (2988ds/592Mi)
% 22.24/3.88 % (2106749)Instruction limit reached!
% 22.24/3.88 % (2106749)------------------------------
% 22.24/3.88 % (2106749)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.24/3.88 % (2106749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.24/3.88 % (2106749)CaDiCaL version: 2.1.3
% 22.24/3.88 % (2106749)Termination reason: Instruction limit
% 22.24/3.88 % (2106749)Termination phase: Saturation
% 22.24/3.88 % (2106749)Time elapsed: 0.085 s
% 22.24/3.88 % (2106749)Peak memory usage: 94 MB
% 22.24/3.88 % (2106749)Instructions burned: 134 (million)
% 22.24/3.88 % (2106750)Instruction limit reached!
% 22.24/3.88 % (2106750)------------------------------
% 22.24/3.88 % (2106750)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.24/3.88 % (2106750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.24/3.88 % (2106750)CaDiCaL version: 2.1.3
% 22.24/3.88 % (2106750)Termination reason: Instruction limit
% 22.24/3.88 % (2106750)Termination phase: Saturation
% 22.24/3.88 % (2106750)Time elapsed: 0.159 s
% 22.24/3.88 % (2106750)Peak memory usage: 102 MB
% 22.24/3.88 % (2106750)Instructions burned: 593 (million)
% 22.24/3.88 % (2106753)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3032599413:st=3:i=13193:sd=3:ss=axioms_2986 on theBenchmark for (2986ds/13193Mi)
% 22.24/3.88 % (2106754)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=2407781867:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2985 on theBenchmark for (2985ds/125Mi)
% 22.24/3.88 % (2106754)Instruction limit reached!
% 22.24/3.88 % (2106754)------------------------------
% 22.24/3.88 % (2106754)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.24/3.88 % (2106754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.24/3.88 % (2106754)CaDiCaL version: 2.1.3
% 22.24/3.88 % (2106754)Termination reason: Instruction limit
% 22.24/3.88 % (2106754)Termination phase: Saturation
% 22.24/3.88 % (2106754)Time elapsed: 0.039 s
% 22.24/3.88 % (2106754)Peak memory usage: 93 MB
% 22.24/3.88 % (2106754)Instructions burned: 128 (million)
% 22.24/3.88 % (2106757)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3110901628:i=134:gtgl=5:slsql=off:gtg=exists_sym_2984 on theBenchmark for (2984ds/134Mi)
% 22.24/3.88 % (2106757)Instruction limit reached!
% 22.24/3.88 % (2106757)------------------------------
% 22.24/3.88 % (2106757)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.24/3.88 % (2106757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.24/3.88 % (2106757)CaDiCaL version: 2.1.3
% 22.24/3.88 % (2106757)Termination reason: Instruction limit
% 22.24/3.88 % (2106757)Termination phase: Preprocessing 3
% 22.24/3.88 % (2106757)Time elapsed: 0.040 s
% 22.24/3.88 % (2106757)Peak memory usage: 92 MB
% 22.24/3.88 % (2106757)Instructions burned: 137 (million)
% 22.24/3.88 % (2106759)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1789336412:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2982 on theBenchmark for (2982ds/141Mi)
% 22.24/3.88 % (2106759)Instruction limit reached!
% 22.24/3.88 % (2106759)------------------------------
% 22.24/3.88 % (2106759)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.24/3.88 % (2106759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.24/3.88 % (2106759)CaDiCaL version: 2.1.3
% 22.24/3.88 % (2106759)Termination reason: Instruction limit
% 22.24/3.88 % (2106759)Termination phase: Saturation
% 22.24/3.88 % (2106759)Time elapsed: 0.042 s
% 22.24/3.88 % (2106759)Peak memory usage: 95 MB
% 22.24/3.88 % (2106759)Instructions burned: 143 (million)
% 22.24/3.88 % (2106761)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3534803247:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2981 on theBenchmark for (2981ds/431Mi)
% 22.24/3.88 % (2106734)Instruction limit reached!
% 22.24/3.88 % (2106734)------------------------------
% 22.24/3.88 % (2106734)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.24/3.88 % (2106734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.24/3.88 % (2106734)CaDiCaL version: 2.1.3
% 22.24/3.88 % (2106734)Termination reason: Instruction limit
% 22.24/3.88 % (2106734)Termination phase: Saturation
% 22.24/3.88 % (2106734)Time elapsed: 1.460 s
% 22.24/3.88 % (2106734)Peak memory usage: 177 MB
% 22.24/3.88 % (2106734)Instructions burned: 2352 (million)
% 22.24/3.88 % (2106761)Instruction limit reached!
% 22.24/3.88 % (2106761)------------------------------
% 22.24/3.88 % (2106761)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.24/3.88 % (2106761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.24/3.88 % (2106761)CaDiCaL version: 2.1.3
% 22.24/3.88 % (2106761)Termination reason: Instruction limit
% 22.24/3.88 % (2106761)Termination phase: Saturation
% 22.24/3.88 % (2106761)Time elapsed: 0.127 s
% 22.24/3.88 % (2106761)Peak memory usage: 96 MB
% 22.24/3.88 % (2106761)Instructions burned: 435 (million)
% 22.24/3.88 % (2106763)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=783203062:i=6060:aac=none:ins=25_2979 on theBenchmark for (2979ds/6060Mi)
% 22.24/3.88 % (2106764)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=3792091181:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2978 on theBenchmark for (2978ds/150Mi)
% 22.24/3.88 % (2106764)Instruction limit reached!
% 22.24/3.88 % (2106764)------------------------------
% 22.24/3.88 % (2106764)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.24/3.88 % (2106764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.24/3.88 % (2106764)CaDiCaL version: 2.1.3
% 22.24/3.88 % (2106764)Termination reason: Instruction limit
% 22.24/3.88 % (2106764)Termination phase: Property scanning
% 22.24/3.88 % (2106764)Time elapsed: 0.050 s
% 22.24/3.88 % (2106764)Peak memory usage: 94 MB
% 22.24/3.88 % (2106764)Instructions burned: 151 (million)
% 22.24/3.88 % (2106767)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1516773524:i=14155:bd=all_2977 on theBenchmark for (2977ds/14155Mi)
% 22.24/3.88 % (2106711)First to succeed.
% 22.24/3.88 % (2106711)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2106706"
% 22.24/3.88 % (2106711)Refutation found. Thanks to Tanya!
% 22.24/3.88 % SZS status Theorem for theBenchmark
% 22.24/3.88 % SZS output start Proof for theBenchmark
% See solution above
% 22.94/4.07 % (2106711)------------------------------
% 22.94/4.07 % (2106711)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.94/4.07 % (2106711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.94/4.07 % (2106711)CaDiCaL version: 2.1.3
% 22.94/4.07 % (2106711)Termination reason: Refutation
% 22.94/4.07 % (2106711)Time elapsed: 2.797 s
% 22.94/4.07 % (2106711)Peak memory usage: 229 MB
% 22.94/4.07 % (2106711)Instructions burned: 4602 (million)
% 22.94/4.07 % (2106711)------------------------------
% 22.94/4.07 % (2106711)------------------------------
% 22.94/4.07 % (2106706)Success in time 3.263 s
% 22.94/4.07 % Vampire exiting
%------------------------------------------------------------------------------