%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT284+1 : 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 : n012.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:31 AM UTC 2026
% Result : Theorem 5.06s 1.38s
% Output : Refutation 6.01s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 41
% Syntax : Number of formulae : 290 ( 38 unt; 25 def)
% Number of atoms : 1198 ( 123 equ)
% Maximal formula atoms : 10 ( 4 avg)
% Number of connectives : 1554 ( 646 ~; 749 |; 105 &)
% ( 26 <=>; 28 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 47 ( 45 usr; 25 prp; 0-3 aty)
% Number of functors : 17 ( 17 usr; 3 con; 0-3 aty)
% Number of variables : 247 ( 0 sgn 241 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(k6_lopclset(X0)))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(k6_lopclset(X0)))
=> k4_lattices(k6_lopclset(X0),X1,X2) = k3_xboole_0(X1,X2) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t12_lopclset) ).
fof(f2,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(k6_lopclset(X0)))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(k6_lopclset(X0)))
=> k4_lattices(k6_lopclset(X0),X1,X2) = k3_xboole_0(X1,X2) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f73,axiom,
! [X0] :
( l3_lattices(X0)
=> ( v3_lattices(X0)
=> X0 = g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',abstractness_v3_lattices) ).
fof(f80,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
<=> m1_relset_1(X2,X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(f85,axiom,
! [X0] :
( l3_lattices(X0)
=> ( l1_lattices(X0)
& l2_lattices(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l3_lattices) ).
fof(f92,axiom,
! [X0] :
( l3_lattices(X0)
=> ( ( ~ v3_struct_0(X0)
& v10_lattices(X0) )
=> ( ~ v3_struct_0(X0)
& v4_lattices(X0)
& v5_lattices(X0)
& v6_lattices(X0)
& v7_lattices(X0)
& v8_lattices(X0)
& v9_lattices(X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc1_lattices) ).
fof(f109,axiom,
! [X0,X1,X2] :
( ( v1_funct_1(X1)
& v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
& m1_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
& v1_funct_1(X2)
& v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
& m1_relset_1(X2,k2_zfmisc_1(X0,X0),X0) )
=> ! [X3,X4,X5] :
( g3_lattices(X0,X1,X2) = g3_lattices(X3,X4,X5)
=> ( X0 = X3
& X1 = X4
& X2 = X5 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',free_g3_lattices) ).
fof(f111,axiom,
! [X0,X1,X2] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0)
& m1_subset_1(X1,k1_lopclset(X0))
& m1_subset_1(X2,k1_lopclset(X0)) )
=> k3_lopclset(X0,X1,X1) = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',idempotence_k3_lopclset) ).
fof(f118,axiom,
! [X0,X1,X2] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0)
& m1_subset_1(X1,k1_lopclset(X0))
& m1_subset_1(X2,k1_lopclset(X0)) )
=> k3_lopclset(X0,X1,X2) = k3_xboole_0(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k3_lopclset) ).
fof(f119,axiom,
! [X0,X1,X2] :
( ( ~ v3_struct_0(X0)
& v6_lattices(X0)
& l1_lattices(X0)
& m1_subset_1(X1,u1_struct_0(X0))
& m1_subset_1(X2,u1_struct_0(X0)) )
=> k4_lattices(X0,X1,X2) = k2_lattices(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k4_lattices) ).
fof(f121,axiom,
! [X0,X1,X2] :
( ( v1_funct_1(X1)
& v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
& m1_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
& v1_funct_1(X2)
& v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
& m1_relset_1(X2,k2_zfmisc_1(X0,X0),X0) )
=> ( v3_lattices(g3_lattices(X0,X1,X2))
& l3_lattices(g3_lattices(X0,X1,X2)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_g3_lattices) ).
fof(f125,axiom,
! [X0,X1,X2] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0)
& m1_subset_1(X1,k1_lopclset(X0))
& m1_subset_1(X2,k1_lopclset(X0)) )
=> m2_subset_1(k3_lopclset(X0,X1,X2),k1_zfmisc_1(u1_struct_0(X0)),k1_lopclset(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k3_lopclset) ).
fof(f128,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> ( v1_funct_1(k4_lopclset(X0))
& v1_funct_2(k4_lopclset(X0),k2_zfmisc_1(k1_lopclset(X0),k1_lopclset(X0)),k1_lopclset(X0))
& m2_relset_1(k4_lopclset(X0),k2_zfmisc_1(k1_lopclset(X0),k1_lopclset(X0)),k1_lopclset(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k4_lopclset) ).
fof(f129,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> ( v1_funct_1(k5_lopclset(X0))
& v1_funct_2(k5_lopclset(X0),k2_zfmisc_1(k1_lopclset(X0),k1_lopclset(X0)),k1_lopclset(X0))
& m2_relset_1(k5_lopclset(X0),k2_zfmisc_1(k1_lopclset(X0),k1_lopclset(X0)),k1_lopclset(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k5_lopclset) ).
fof(f130,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> ( ~ v3_struct_0(k6_lopclset(X0))
& v10_lattices(k6_lopclset(X0))
& l3_lattices(k6_lopclset(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k6_lopclset) ).
fof(f140,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> k6_lopclset(X0) = g3_lattices(k1_lopclset(X0),k4_lopclset(X0),k5_lopclset(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d4_lopclset) ).
fof(f141,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(g3_lattices(k1_lopclset(X0),k4_lopclset(X0),k5_lopclset(X0))))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(g3_lattices(k1_lopclset(X0),k4_lopclset(X0),k5_lopclset(X0))))
=> ! [X3] :
( m2_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)),k1_lopclset(X0))
=> ! [X4] :
( m2_subset_1(X4,k1_zfmisc_1(u1_struct_0(X0)),k1_lopclset(X0))
=> ( ( X1 = X3
& X2 = X4 )
=> k2_lattices(g3_lattices(k1_lopclset(X0),k4_lopclset(X0),k5_lopclset(X0)),X1,X2) = k3_lopclset(X0,X3,X4) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t6_lopclset) ).
fof(f145,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( k4_lattices(k6_lopclset(X0),X1,X2) != k3_xboole_0(X1,X2)
& m1_subset_1(X2,u1_struct_0(k6_lopclset(X0))) )
& m1_subset_1(X1,u1_struct_0(k6_lopclset(X0))) )
& ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f2]) ).
fof(f146,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( k4_lattices(k6_lopclset(X0),X1,X2) != k3_xboole_0(X1,X2)
& m1_subset_1(X2,u1_struct_0(k6_lopclset(X0))) )
& m1_subset_1(X1,u1_struct_0(k6_lopclset(X0))) )
& ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) ),
inference(flattening,[],[f145]) ).
fof(f210,plain,
! [X0] :
( X0 = g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))
| ~ v3_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f73]) ).
fof(f211,plain,
! [X0] :
( X0 = g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))
| ~ v3_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f210]) ).
fof(f217,plain,
! [X0] :
( ( l1_lattices(X0)
& l2_lattices(X0) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f85]) ).
fof(f223,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v4_lattices(X0)
& v5_lattices(X0)
& v6_lattices(X0)
& v7_lattices(X0)
& v8_lattices(X0)
& v9_lattices(X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f92]) ).
fof(f224,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v4_lattices(X0)
& v5_lattices(X0)
& v6_lattices(X0)
& v7_lattices(X0)
& v8_lattices(X0)
& v9_lattices(X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f223]) ).
fof(f246,plain,
! [X0,X1,X2] :
( ! [X3,X4,X5] :
( ( X0 = X3
& X1 = X4
& X2 = X5 )
| g3_lattices(X0,X1,X2) != g3_lattices(X3,X4,X5) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m1_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m1_relset_1(X2,k2_zfmisc_1(X0,X0),X0) ),
inference(ennf_transformation,[],[f109]) ).
fof(f247,plain,
! [X0,X1,X2] :
( ! [X3,X4,X5] :
( ( X0 = X3
& X1 = X4
& X2 = X5 )
| g3_lattices(X0,X1,X2) != g3_lattices(X3,X4,X5) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m1_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m1_relset_1(X2,k2_zfmisc_1(X0,X0),X0) ),
inference(flattening,[],[f246]) ).
fof(f250,plain,
! [X0,X1,X2] :
( k3_lopclset(X0,X1,X1) = X1
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| ~ m1_subset_1(X1,k1_lopclset(X0))
| ~ m1_subset_1(X2,k1_lopclset(X0)) ),
inference(ennf_transformation,[],[f111]) ).
fof(f251,plain,
! [X0,X1,X2] :
( k3_lopclset(X0,X1,X1) = X1
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| ~ m1_subset_1(X1,k1_lopclset(X0))
| ~ m1_subset_1(X2,k1_lopclset(X0)) ),
inference(flattening,[],[f250]) ).
fof(f256,plain,
! [X0,X1,X2] :
( k3_lopclset(X0,X1,X2) = k3_xboole_0(X1,X2)
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| ~ m1_subset_1(X1,k1_lopclset(X0))
| ~ m1_subset_1(X2,k1_lopclset(X0)) ),
inference(ennf_transformation,[],[f118]) ).
fof(f257,plain,
! [X0,X1,X2] :
( k3_lopclset(X0,X1,X2) = k3_xboole_0(X1,X2)
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| ~ m1_subset_1(X1,k1_lopclset(X0))
| ~ m1_subset_1(X2,k1_lopclset(X0)) ),
inference(flattening,[],[f256]) ).
fof(f258,plain,
! [X0,X1,X2] :
( k4_lattices(X0,X1,X2) = k2_lattices(X0,X1,X2)
| v3_struct_0(X0)
| ~ v6_lattices(X0)
| ~ l1_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f119]) ).
fof(f259,plain,
! [X0,X1,X2] :
( k4_lattices(X0,X1,X2) = k2_lattices(X0,X1,X2)
| v3_struct_0(X0)
| ~ v6_lattices(X0)
| ~ l1_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(flattening,[],[f258]) ).
fof(f262,plain,
! [X0,X1,X2] :
( ( v3_lattices(g3_lattices(X0,X1,X2))
& l3_lattices(g3_lattices(X0,X1,X2)) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m1_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m1_relset_1(X2,k2_zfmisc_1(X0,X0),X0) ),
inference(ennf_transformation,[],[f121]) ).
fof(f263,plain,
! [X0,X1,X2] :
( ( v3_lattices(g3_lattices(X0,X1,X2))
& l3_lattices(g3_lattices(X0,X1,X2)) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m1_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m1_relset_1(X2,k2_zfmisc_1(X0,X0),X0) ),
inference(flattening,[],[f262]) ).
fof(f268,plain,
! [X0,X1,X2] :
( m2_subset_1(k3_lopclset(X0,X1,X2),k1_zfmisc_1(u1_struct_0(X0)),k1_lopclset(X0))
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| ~ m1_subset_1(X1,k1_lopclset(X0))
| ~ m1_subset_1(X2,k1_lopclset(X0)) ),
inference(ennf_transformation,[],[f125]) ).
fof(f269,plain,
! [X0,X1,X2] :
( m2_subset_1(k3_lopclset(X0,X1,X2),k1_zfmisc_1(u1_struct_0(X0)),k1_lopclset(X0))
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| ~ m1_subset_1(X1,k1_lopclset(X0))
| ~ m1_subset_1(X2,k1_lopclset(X0)) ),
inference(flattening,[],[f268]) ).
fof(f272,plain,
! [X0] :
( ( v1_funct_1(k4_lopclset(X0))
& v1_funct_2(k4_lopclset(X0),k2_zfmisc_1(k1_lopclset(X0),k1_lopclset(X0)),k1_lopclset(X0))
& m2_relset_1(k4_lopclset(X0),k2_zfmisc_1(k1_lopclset(X0),k1_lopclset(X0)),k1_lopclset(X0)) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f128]) ).
fof(f273,plain,
! [X0] :
( ( v1_funct_1(k4_lopclset(X0))
& v1_funct_2(k4_lopclset(X0),k2_zfmisc_1(k1_lopclset(X0),k1_lopclset(X0)),k1_lopclset(X0))
& m2_relset_1(k4_lopclset(X0),k2_zfmisc_1(k1_lopclset(X0),k1_lopclset(X0)),k1_lopclset(X0)) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f272]) ).
fof(f274,plain,
! [X0] :
( ( v1_funct_1(k5_lopclset(X0))
& v1_funct_2(k5_lopclset(X0),k2_zfmisc_1(k1_lopclset(X0),k1_lopclset(X0)),k1_lopclset(X0))
& m2_relset_1(k5_lopclset(X0),k2_zfmisc_1(k1_lopclset(X0),k1_lopclset(X0)),k1_lopclset(X0)) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f129]) ).
fof(f275,plain,
! [X0] :
( ( v1_funct_1(k5_lopclset(X0))
& v1_funct_2(k5_lopclset(X0),k2_zfmisc_1(k1_lopclset(X0),k1_lopclset(X0)),k1_lopclset(X0))
& m2_relset_1(k5_lopclset(X0),k2_zfmisc_1(k1_lopclset(X0),k1_lopclset(X0)),k1_lopclset(X0)) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f274]) ).
fof(f276,plain,
! [X0] :
( ( ~ v3_struct_0(k6_lopclset(X0))
& v10_lattices(k6_lopclset(X0))
& l3_lattices(k6_lopclset(X0)) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f130]) ).
fof(f277,plain,
! [X0] :
( ( ~ v3_struct_0(k6_lopclset(X0))
& v10_lattices(k6_lopclset(X0))
& l3_lattices(k6_lopclset(X0)) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f276]) ).
fof(f288,plain,
! [X0] :
( k6_lopclset(X0) = g3_lattices(k1_lopclset(X0),k4_lopclset(X0),k5_lopclset(X0))
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f140]) ).
fof(f289,plain,
! [X0] :
( k6_lopclset(X0) = g3_lattices(k1_lopclset(X0),k4_lopclset(X0),k5_lopclset(X0))
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f288]) ).
fof(f290,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( k2_lattices(g3_lattices(k1_lopclset(X0),k4_lopclset(X0),k5_lopclset(X0)),X1,X2) = k3_lopclset(X0,X3,X4)
| X1 != X3
| X2 != X4
| ~ m2_subset_1(X4,k1_zfmisc_1(u1_struct_0(X0)),k1_lopclset(X0)) )
| ~ m2_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)),k1_lopclset(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(g3_lattices(k1_lopclset(X0),k4_lopclset(X0),k5_lopclset(X0)))) )
| ~ m1_subset_1(X1,u1_struct_0(g3_lattices(k1_lopclset(X0),k4_lopclset(X0),k5_lopclset(X0)))) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f141]) ).
fof(f291,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( k2_lattices(g3_lattices(k1_lopclset(X0),k4_lopclset(X0),k5_lopclset(X0)),X1,X2) = k3_lopclset(X0,X3,X4)
| X1 != X3
| X2 != X4
| ~ m2_subset_1(X4,k1_zfmisc_1(u1_struct_0(X0)),k1_lopclset(X0)) )
| ~ m2_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)),k1_lopclset(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(g3_lattices(k1_lopclset(X0),k4_lopclset(X0),k5_lopclset(X0)))) )
| ~ m1_subset_1(X1,u1_struct_0(g3_lattices(k1_lopclset(X0),k4_lopclset(X0),k5_lopclset(X0)))) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f290]) ).
fof(f292,plain,
( k4_lattices(k6_lopclset(sK0),sK1,sK2) != k3_xboole_0(sK1,sK2)
& m1_subset_1(sK2,u1_struct_0(k6_lopclset(sK0)))
& m1_subset_1(sK1,u1_struct_0(k6_lopclset(sK0)))
& ~ v3_struct_0(sK0)
& v2_pre_topc(sK0)
& l1_pre_topc(sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2)],[f146]) ).
fof(f308,plain,
! [X0,X1,X2] :
( ( m2_relset_1(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1) )
& ( m1_relset_1(X2,X0,X1)
| ~ m2_relset_1(X2,X0,X1) ) ),
inference(nnf_transformation,[],[f80]) ).
fof(f322,plain,
l1_pre_topc(sK0),
inference(cnf_transformation,[],[f292]) ).
fof(f323,plain,
v2_pre_topc(sK0),
inference(cnf_transformation,[],[f292]) ).
fof(f324,plain,
~ v3_struct_0(sK0),
inference(cnf_transformation,[],[f292]) ).
fof(f325,plain,
m1_subset_1(sK1,u1_struct_0(k6_lopclset(sK0))),
inference(cnf_transformation,[],[f292]) ).
fof(f326,plain,
m1_subset_1(sK2,u1_struct_0(k6_lopclset(sK0))),
inference(cnf_transformation,[],[f292]) ).
fof(f327,plain,
k4_lattices(k6_lopclset(sK0),sK1,sK2) != k3_xboole_0(sK1,sK2),
inference(cnf_transformation,[],[f292]) ).
fof(f490,plain,
! [X0] :
( g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) = X0
| ~ v3_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f211]) ).
fof(f497,plain,
! [X2,X0,X1] :
( m1_relset_1(X2,X0,X1)
| ~ m2_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f308]) ).
fof(f502,plain,
! [X0] :
( l1_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f217]) ).
fof(f518,plain,
! [X0] :
( v6_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f224]) ).
fof(f556,plain,
! [X2,X3,X0,X1,X4,X5] :
( X0 = X3
| g3_lattices(X0,X1,X2) != g3_lattices(X3,X4,X5)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m1_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m1_relset_1(X2,k2_zfmisc_1(X0,X0),X0) ),
inference(cnf_transformation,[],[f247]) ).
fof(f558,plain,
! [X2,X0,X1] :
( k3_lopclset(X0,X1,X1) = X1
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| ~ m1_subset_1(X1,k1_lopclset(X0))
| ~ m1_subset_1(X2,k1_lopclset(X0)) ),
inference(cnf_transformation,[],[f251]) ).
fof(f565,plain,
! [X2,X0,X1] :
( k3_xboole_0(X1,X2) = k3_lopclset(X0,X1,X2)
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| ~ m1_subset_1(X1,k1_lopclset(X0))
| ~ m1_subset_1(X2,k1_lopclset(X0)) ),
inference(cnf_transformation,[],[f257]) ).
fof(f566,plain,
! [X2,X0,X1] :
( k4_lattices(X0,X1,X2) = k2_lattices(X0,X1,X2)
| v3_struct_0(X0)
| ~ v6_lattices(X0)
| ~ l1_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f259]) ).
fof(f570,plain,
! [X2,X0,X1] :
( v3_lattices(g3_lattices(X0,X1,X2))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m1_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m1_relset_1(X2,k2_zfmisc_1(X0,X0),X0) ),
inference(cnf_transformation,[],[f263]) ).
fof(f573,plain,
! [X2,X0,X1] :
( m2_subset_1(k3_lopclset(X0,X1,X2),k1_zfmisc_1(u1_struct_0(X0)),k1_lopclset(X0))
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| ~ m1_subset_1(X1,k1_lopclset(X0))
| ~ m1_subset_1(X2,k1_lopclset(X0)) ),
inference(cnf_transformation,[],[f269]) ).
fof(f575,plain,
! [X0] :
( m2_relset_1(k4_lopclset(X0),k2_zfmisc_1(k1_lopclset(X0),k1_lopclset(X0)),k1_lopclset(X0))
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f273]) ).
fof(f576,plain,
! [X0] :
( v1_funct_2(k4_lopclset(X0),k2_zfmisc_1(k1_lopclset(X0),k1_lopclset(X0)),k1_lopclset(X0))
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f273]) ).
fof(f577,plain,
! [X0] :
( v1_funct_1(k4_lopclset(X0))
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f273]) ).
fof(f578,plain,
! [X0] :
( m2_relset_1(k5_lopclset(X0),k2_zfmisc_1(k1_lopclset(X0),k1_lopclset(X0)),k1_lopclset(X0))
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f275]) ).
fof(f579,plain,
! [X0] :
( v1_funct_2(k5_lopclset(X0),k2_zfmisc_1(k1_lopclset(X0),k1_lopclset(X0)),k1_lopclset(X0))
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f275]) ).
fof(f580,plain,
! [X0] :
( v1_funct_1(k5_lopclset(X0))
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f275]) ).
fof(f581,plain,
! [X0] :
( l3_lattices(k6_lopclset(X0))
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f277]) ).
fof(f582,plain,
! [X0] :
( v10_lattices(k6_lopclset(X0))
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f277]) ).
fof(f583,plain,
! [X0] :
( ~ v3_struct_0(k6_lopclset(X0))
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f277]) ).
fof(f594,plain,
! [X0] :
( k6_lopclset(X0) = g3_lattices(k1_lopclset(X0),k4_lopclset(X0),k5_lopclset(X0))
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f289]) ).
fof(f595,plain,
! [X2,X3,X0,X1,X4] :
( k2_lattices(g3_lattices(k1_lopclset(X0),k4_lopclset(X0),k5_lopclset(X0)),X1,X2) = k3_lopclset(X0,X3,X4)
| X1 != X3
| X2 != X4
| ~ m2_subset_1(X4,k1_zfmisc_1(u1_struct_0(X0)),k1_lopclset(X0))
| ~ m2_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)),k1_lopclset(X0))
| ~ m1_subset_1(X2,u1_struct_0(g3_lattices(k1_lopclset(X0),k4_lopclset(X0),k5_lopclset(X0))))
| ~ m1_subset_1(X1,u1_struct_0(g3_lattices(k1_lopclset(X0),k4_lopclset(X0),k5_lopclset(X0))))
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f291]) ).
fof(f598,plain,
! [X2,X3,X0,X4] :
( k3_lopclset(X0,X3,X4) = k2_lattices(g3_lattices(k1_lopclset(X0),k4_lopclset(X0),k5_lopclset(X0)),X3,X2)
| X2 != X4
| ~ m2_subset_1(X4,k1_zfmisc_1(u1_struct_0(X0)),k1_lopclset(X0))
| ~ m2_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)),k1_lopclset(X0))
| ~ m1_subset_1(X2,u1_struct_0(g3_lattices(k1_lopclset(X0),k4_lopclset(X0),k5_lopclset(X0))))
| ~ m1_subset_1(X3,u1_struct_0(g3_lattices(k1_lopclset(X0),k4_lopclset(X0),k5_lopclset(X0))))
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(equality_resolution,[],[f595]) ).
fof(f599,plain,
! [X3,X0,X4] :
( k3_lopclset(X0,X3,X4) = k2_lattices(g3_lattices(k1_lopclset(X0),k4_lopclset(X0),k5_lopclset(X0)),X3,X4)
| ~ m2_subset_1(X4,k1_zfmisc_1(u1_struct_0(X0)),k1_lopclset(X0))
| ~ m2_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)),k1_lopclset(X0))
| ~ m1_subset_1(X4,u1_struct_0(g3_lattices(k1_lopclset(X0),k4_lopclset(X0),k5_lopclset(X0))))
| ~ m1_subset_1(X3,u1_struct_0(g3_lattices(k1_lopclset(X0),k4_lopclset(X0),k5_lopclset(X0))))
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(equality_resolution,[],[f598]) ).
fof(f602,plain,
! [X2,X0] :
( ~ m1_subset_1(X2,k1_lopclset(X0))
| sP28(X0) ),
inference(cnf_transformation,[],[f602_D]) ).
fof(f602_D,definition,
! [X0] :
( ! [X2] : ~ m1_subset_1(X2,k1_lopclset(X0))
<=> ~ sP28(X0) ),
introduced(definition,[new_symbols(definition,[sP28])],[general_splitting_component_introduction]) ).
fof(f603,plain,
! [X0,X1] :
( k3_lopclset(X0,X1,X1) = X1
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| ~ m1_subset_1(X1,k1_lopclset(X0))
| ~ sP28(X0) ),
inference(general_splitting,[],[f558,f602_D]) ).
fof(f605,definition,
( spl29_1
<=> v3_struct_0(sK0) ),
introduced(definition,[new_symbols(definition,[spl29_1])],[avatar_definition]) ).
fof(f607,plain,
( ~ v3_struct_0(sK0)
| spl29_1 ),
inference(avatar_component_clause,[],[f605]) ).
fof(f608,plain,
~ spl29_1,
inference(avatar_split_clause,[],[f324,f605]) ).
fof(f610,definition,
( spl29_2
<=> l1_pre_topc(sK0) ),
introduced(definition,[new_symbols(definition,[spl29_2])],[avatar_definition]) ).
fof(f612,plain,
( l1_pre_topc(sK0)
| ~ spl29_2 ),
inference(avatar_component_clause,[],[f610]) ).
fof(f613,plain,
spl29_2,
inference(avatar_split_clause,[],[f322,f610]) ).
fof(f639,plain,
( m2_relset_1(k4_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0))
| ~ v2_pre_topc(sK0)
| ~ l1_pre_topc(sK0)
| spl29_1 ),
inference(resolution,[],[f607,f575]) ).
fof(f640,plain,
( v1_funct_2(k4_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0))
| ~ v2_pre_topc(sK0)
| ~ l1_pre_topc(sK0)
| spl29_1 ),
inference(resolution,[],[f607,f576]) ).
fof(f641,plain,
( v1_funct_1(k4_lopclset(sK0))
| ~ v2_pre_topc(sK0)
| ~ l1_pre_topc(sK0)
| spl29_1 ),
inference(resolution,[],[f607,f577]) ).
fof(f642,plain,
( m2_relset_1(k5_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0))
| ~ v2_pre_topc(sK0)
| ~ l1_pre_topc(sK0)
| spl29_1 ),
inference(resolution,[],[f607,f578]) ).
fof(f643,plain,
( v1_funct_2(k5_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0))
| ~ v2_pre_topc(sK0)
| ~ l1_pre_topc(sK0)
| spl29_1 ),
inference(resolution,[],[f607,f579]) ).
fof(f644,plain,
( v1_funct_1(k5_lopclset(sK0))
| ~ v2_pre_topc(sK0)
| ~ l1_pre_topc(sK0)
| spl29_1 ),
inference(resolution,[],[f607,f580]) ).
fof(f645,plain,
( l3_lattices(k6_lopclset(sK0))
| ~ v2_pre_topc(sK0)
| ~ l1_pre_topc(sK0)
| spl29_1 ),
inference(resolution,[],[f607,f581]) ).
fof(f646,plain,
( v10_lattices(k6_lopclset(sK0))
| ~ v2_pre_topc(sK0)
| ~ l1_pre_topc(sK0)
| spl29_1 ),
inference(resolution,[],[f607,f582]) ).
fof(f647,plain,
( ~ v3_struct_0(k6_lopclset(sK0))
| ~ v2_pre_topc(sK0)
| ~ l1_pre_topc(sK0)
| spl29_1 ),
inference(resolution,[],[f607,f583]) ).
fof(f651,plain,
( k6_lopclset(sK0) = g3_lattices(k1_lopclset(sK0),k4_lopclset(sK0),k5_lopclset(sK0))
| ~ v2_pre_topc(sK0)
| ~ l1_pre_topc(sK0)
| spl29_1 ),
inference(resolution,[],[f607,f594]) ).
fof(f654,plain,
( ! [X0] :
( k3_lopclset(sK0,X0,X0) = X0
| ~ v2_pre_topc(sK0)
| ~ l1_pre_topc(sK0)
| ~ m1_subset_1(X0,k1_lopclset(sK0))
| ~ sP28(sK0) )
| spl29_1 ),
inference(resolution,[],[f607,f603]) ).
fof(f655,plain,
( ! [X0] :
( k3_lopclset(sK0,X0,X0) = X0
| ~ v2_pre_topc(sK0)
| ~ l1_pre_topc(sK0)
| ~ m1_subset_1(X0,k1_lopclset(sK0)) )
| spl29_1 ),
inference(forward_subsumption_resolution,[],[f654,f602]) ).
fof(f658,plain,
( k6_lopclset(sK0) = g3_lattices(k1_lopclset(sK0),k4_lopclset(sK0),k5_lopclset(sK0))
| ~ l1_pre_topc(sK0)
| spl29_1 ),
inference(forward_subsumption_resolution,[],[f651,f323]) ).
fof(f661,plain,
( ~ v3_struct_0(k6_lopclset(sK0))
| ~ l1_pre_topc(sK0)
| spl29_1 ),
inference(forward_subsumption_resolution,[],[f647,f323]) ).
fof(f662,plain,
( v10_lattices(k6_lopclset(sK0))
| ~ l1_pre_topc(sK0)
| spl29_1 ),
inference(forward_subsumption_resolution,[],[f646,f323]) ).
fof(f663,plain,
( l3_lattices(k6_lopclset(sK0))
| ~ l1_pre_topc(sK0)
| spl29_1 ),
inference(forward_subsumption_resolution,[],[f645,f323]) ).
fof(f664,plain,
( v1_funct_1(k5_lopclset(sK0))
| ~ l1_pre_topc(sK0)
| spl29_1 ),
inference(forward_subsumption_resolution,[],[f644,f323]) ).
fof(f665,plain,
( v1_funct_2(k5_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0))
| ~ l1_pre_topc(sK0)
| spl29_1 ),
inference(forward_subsumption_resolution,[],[f643,f323]) ).
fof(f666,plain,
( m2_relset_1(k5_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0))
| ~ l1_pre_topc(sK0)
| spl29_1 ),
inference(forward_subsumption_resolution,[],[f642,f323]) ).
fof(f667,plain,
( v1_funct_1(k4_lopclset(sK0))
| ~ l1_pre_topc(sK0)
| spl29_1 ),
inference(forward_subsumption_resolution,[],[f641,f323]) ).
fof(f668,plain,
( v1_funct_2(k4_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0))
| ~ l1_pre_topc(sK0)
| spl29_1 ),
inference(forward_subsumption_resolution,[],[f640,f323]) ).
fof(f669,plain,
( m2_relset_1(k4_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0))
| ~ l1_pre_topc(sK0)
| spl29_1 ),
inference(forward_subsumption_resolution,[],[f639,f323]) ).
fof(f681,plain,
( ! [X0] :
( k3_lopclset(sK0,X0,X0) = X0
| ~ l1_pre_topc(sK0)
| ~ m1_subset_1(X0,k1_lopclset(sK0)) )
| spl29_1 ),
inference(forward_subsumption_resolution,[],[f655,f323]) ).
fof(f683,plain,
( k6_lopclset(sK0) = g3_lattices(k1_lopclset(sK0),k4_lopclset(sK0),k5_lopclset(sK0))
| spl29_1
| ~ spl29_2 ),
inference(forward_subsumption_resolution,[],[f658,f612]) ).
fof(f685,plain,
( ~ v3_struct_0(k6_lopclset(sK0))
| spl29_1
| ~ spl29_2 ),
inference(forward_subsumption_resolution,[],[f661,f612]) ).
fof(f686,plain,
( v10_lattices(k6_lopclset(sK0))
| spl29_1
| ~ spl29_2 ),
inference(forward_subsumption_resolution,[],[f662,f612]) ).
fof(f687,plain,
( l3_lattices(k6_lopclset(sK0))
| spl29_1
| ~ spl29_2 ),
inference(forward_subsumption_resolution,[],[f663,f612]) ).
fof(f688,plain,
( v1_funct_1(k5_lopclset(sK0))
| spl29_1
| ~ spl29_2 ),
inference(forward_subsumption_resolution,[],[f664,f612]) ).
fof(f689,plain,
( v1_funct_2(k5_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0))
| spl29_1
| ~ spl29_2 ),
inference(forward_subsumption_resolution,[],[f665,f612]) ).
fof(f690,plain,
( m2_relset_1(k5_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0))
| spl29_1
| ~ spl29_2 ),
inference(forward_subsumption_resolution,[],[f666,f612]) ).
fof(f691,plain,
( v1_funct_1(k4_lopclset(sK0))
| spl29_1
| ~ spl29_2 ),
inference(forward_subsumption_resolution,[],[f667,f612]) ).
fof(f692,plain,
( v1_funct_2(k4_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0))
| spl29_1
| ~ spl29_2 ),
inference(forward_subsumption_resolution,[],[f668,f612]) ).
fof(f693,plain,
( m2_relset_1(k4_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0))
| spl29_1
| ~ spl29_2 ),
inference(forward_subsumption_resolution,[],[f669,f612]) ).
fof(f704,plain,
( ! [X0] :
( k3_lopclset(sK0,X0,X0) = X0
| ~ m1_subset_1(X0,k1_lopclset(sK0)) )
| spl29_1
| ~ spl29_2 ),
inference(forward_subsumption_resolution,[],[f681,f612]) ).
fof(f706,definition,
( spl29_3
<=> m1_subset_1(sK1,u1_struct_0(k6_lopclset(sK0))) ),
introduced(definition,[new_symbols(definition,[spl29_3])],[avatar_definition]) ).
fof(f708,plain,
( m1_subset_1(sK1,u1_struct_0(k6_lopclset(sK0)))
| ~ spl29_3 ),
inference(avatar_component_clause,[],[f706]) ).
fof(f709,plain,
spl29_3,
inference(avatar_split_clause,[],[f325,f706]) ).
fof(f713,plain,
( ! [X0] :
( k4_lattices(k6_lopclset(sK0),sK1,X0) = k2_lattices(k6_lopclset(sK0),sK1,X0)
| v3_struct_0(k6_lopclset(sK0))
| ~ v6_lattices(k6_lopclset(sK0))
| ~ l1_lattices(k6_lopclset(sK0))
| ~ m1_subset_1(X0,u1_struct_0(k6_lopclset(sK0))) )
| ~ spl29_3 ),
inference(resolution,[],[f708,f566]) ).
fof(f747,plain,
( ! [X0] :
( k4_lattices(k6_lopclset(sK0),sK1,X0) = k2_lattices(k6_lopclset(sK0),sK1,X0)
| ~ v6_lattices(k6_lopclset(sK0))
| ~ l1_lattices(k6_lopclset(sK0))
| ~ m1_subset_1(X0,u1_struct_0(k6_lopclset(sK0))) )
| spl29_1
| ~ spl29_2
| ~ spl29_3 ),
inference(forward_subsumption_resolution,[],[f713,f685]) ).
fof(f752,definition,
( spl29_4
<=> m1_subset_1(sK2,u1_struct_0(k6_lopclset(sK0))) ),
introduced(definition,[new_symbols(definition,[spl29_4])],[avatar_definition]) ).
fof(f754,plain,
( m1_subset_1(sK2,u1_struct_0(k6_lopclset(sK0)))
| ~ spl29_4 ),
inference(avatar_component_clause,[],[f752]) ).
fof(f755,plain,
spl29_4,
inference(avatar_split_clause,[],[f326,f752]) ).
fof(f841,definition,
( spl29_5
<=> k4_lattices(k6_lopclset(sK0),sK1,sK2) = k3_xboole_0(sK1,sK2) ),
introduced(definition,[new_symbols(definition,[spl29_5])],[avatar_definition]) ).
fof(f843,plain,
( k4_lattices(k6_lopclset(sK0),sK1,sK2) != k3_xboole_0(sK1,sK2)
| spl29_5 ),
inference(avatar_component_clause,[],[f841]) ).
fof(f844,plain,
~ spl29_5,
inference(avatar_split_clause,[],[f327,f841]) ).
fof(f846,definition,
( spl29_6
<=> v2_pre_topc(sK0) ),
introduced(definition,[new_symbols(definition,[spl29_6])],[avatar_definition]) ).
fof(f848,plain,
( v2_pre_topc(sK0)
| ~ spl29_6 ),
inference(avatar_component_clause,[],[f846]) ).
fof(f849,plain,
spl29_6,
inference(avatar_split_clause,[],[f323,f846]) ).
fof(f873,definition,
( spl29_7
<=> ! [X0] :
( k3_lopclset(sK0,X0,X0) = X0
| ~ m1_subset_1(X0,k1_lopclset(sK0)) ) ),
introduced(definition,[new_symbols(definition,[spl29_7])],[avatar_definition]) ).
fof(f874,plain,
( ! [X0] :
( k3_lopclset(sK0,X0,X0) = X0
| ~ m1_subset_1(X0,k1_lopclset(sK0)) )
| ~ spl29_7 ),
inference(avatar_component_clause,[],[f873]) ).
fof(f875,plain,
( spl29_7
| spl29_1
| ~ spl29_2 ),
inference(avatar_split_clause,[],[f704,f610,f605,f873]) ).
fof(f877,plain,
( ! [X0] :
( m2_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0)),k1_lopclset(sK0))
| v3_struct_0(sK0)
| ~ v2_pre_topc(sK0)
| ~ l1_pre_topc(sK0)
| ~ m1_subset_1(X0,k1_lopclset(sK0))
| ~ m1_subset_1(X0,k1_lopclset(sK0))
| ~ m1_subset_1(X0,k1_lopclset(sK0)) )
| ~ spl29_7 ),
inference(superposition,[],[f573,f874]) ).
fof(f880,plain,
( ! [X0] :
( m2_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0)),k1_lopclset(sK0))
| v3_struct_0(sK0)
| ~ v2_pre_topc(sK0)
| ~ l1_pre_topc(sK0)
| ~ m1_subset_1(X0,k1_lopclset(sK0)) )
| ~ spl29_7 ),
inference(duplicate_literal_removal,[],[f877]) ).
fof(f882,plain,
( ! [X0] :
( m2_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0)),k1_lopclset(sK0))
| ~ v2_pre_topc(sK0)
| ~ l1_pre_topc(sK0)
| ~ m1_subset_1(X0,k1_lopclset(sK0)) )
| spl29_1
| ~ spl29_7 ),
inference(forward_subsumption_resolution,[],[f880,f607]) ).
fof(f883,plain,
( ! [X0] :
( m2_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0)),k1_lopclset(sK0))
| ~ l1_pre_topc(sK0)
| ~ m1_subset_1(X0,k1_lopclset(sK0)) )
| spl29_1
| ~ spl29_6
| ~ spl29_7 ),
inference(forward_subsumption_resolution,[],[f882,f848]) ).
fof(f884,plain,
( ! [X0] :
( m2_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0)),k1_lopclset(sK0))
| ~ m1_subset_1(X0,k1_lopclset(sK0)) )
| spl29_1
| ~ spl29_2
| ~ spl29_6
| ~ spl29_7 ),
inference(forward_subsumption_resolution,[],[f883,f612]) ).
fof(f886,definition,
( spl29_8
<=> v3_struct_0(k6_lopclset(sK0)) ),
introduced(definition,[new_symbols(definition,[spl29_8])],[avatar_definition]) ).
fof(f888,plain,
( ~ v3_struct_0(k6_lopclset(sK0))
| spl29_8 ),
inference(avatar_component_clause,[],[f886]) ).
fof(f889,plain,
( ~ spl29_8
| spl29_1
| ~ spl29_2 ),
inference(avatar_split_clause,[],[f685,f610,f605,f886]) ).
fof(f897,plain,
( v6_lattices(k6_lopclset(sK0))
| ~ v10_lattices(k6_lopclset(sK0))
| ~ l3_lattices(k6_lopclset(sK0))
| spl29_8 ),
inference(resolution,[],[f888,f518]) ).
fof(f934,plain,
( v6_lattices(k6_lopclset(sK0))
| ~ l3_lattices(k6_lopclset(sK0))
| spl29_1
| ~ spl29_2
| spl29_8 ),
inference(forward_subsumption_resolution,[],[f897,f686]) ).
fof(f940,plain,
( v6_lattices(k6_lopclset(sK0))
| spl29_1
| ~ spl29_2
| spl29_8 ),
inference(forward_subsumption_resolution,[],[f934,f687]) ).
fof(f946,plain,
( ! [X0] :
( k4_lattices(k6_lopclset(sK0),sK1,X0) = k2_lattices(k6_lopclset(sK0),sK1,X0)
| ~ l1_lattices(k6_lopclset(sK0))
| ~ m1_subset_1(X0,u1_struct_0(k6_lopclset(sK0))) )
| spl29_1
| ~ spl29_2
| ~ spl29_3
| spl29_8 ),
inference(backward_subsumption_resolution,[],[f747,f940]) ).
fof(f958,definition,
( spl29_9
<=> l1_lattices(k6_lopclset(sK0)) ),
introduced(definition,[new_symbols(definition,[spl29_9])],[avatar_definition]) ).
fof(f959,plain,
( l1_lattices(k6_lopclset(sK0))
| ~ spl29_9 ),
inference(avatar_component_clause,[],[f958]) ).
fof(f960,plain,
( ~ l1_lattices(k6_lopclset(sK0))
| spl29_9 ),
inference(avatar_component_clause,[],[f958]) ).
fof(f965,plain,
( ~ l3_lattices(k6_lopclset(sK0))
| spl29_9 ),
inference(resolution,[],[f960,f502]) ).
fof(f966,plain,
( $false
| spl29_1
| ~ spl29_2
| spl29_9 ),
inference(forward_subsumption_resolution,[],[f965,f687]) ).
fof(f967,plain,
( spl29_1
| ~ spl29_2
| spl29_9 ),
inference(avatar_contradiction_clause,[],[f966]) ).
fof(f980,plain,
( ! [X0] :
( k4_lattices(k6_lopclset(sK0),sK1,X0) = k2_lattices(k6_lopclset(sK0),sK1,X0)
| ~ m1_subset_1(X0,u1_struct_0(k6_lopclset(sK0))) )
| spl29_1
| ~ spl29_2
| ~ spl29_3
| spl29_8
| ~ spl29_9 ),
inference(backward_subsumption_resolution,[],[f946,f959]) ).
fof(f1003,definition,
( spl29_12
<=> ! [X0] :
( k4_lattices(k6_lopclset(sK0),sK1,X0) = k2_lattices(k6_lopclset(sK0),sK1,X0)
| ~ m1_subset_1(X0,u1_struct_0(k6_lopclset(sK0))) ) ),
introduced(definition,[new_symbols(definition,[spl29_12])],[avatar_definition]) ).
fof(f1004,plain,
( ! [X0] :
( k4_lattices(k6_lopclset(sK0),sK1,X0) = k2_lattices(k6_lopclset(sK0),sK1,X0)
| ~ m1_subset_1(X0,u1_struct_0(k6_lopclset(sK0))) )
| ~ spl29_12 ),
inference(avatar_component_clause,[],[f1003]) ).
fof(f1005,plain,
( spl29_12
| spl29_1
| ~ spl29_2
| ~ spl29_3
| spl29_8
| ~ spl29_9 ),
inference(avatar_split_clause,[],[f980,f958,f886,f706,f610,f605,f1003]) ).
fof(f1382,definition,
( spl29_21
<=> k6_lopclset(sK0) = g3_lattices(k1_lopclset(sK0),k4_lopclset(sK0),k5_lopclset(sK0)) ),
introduced(definition,[new_symbols(definition,[spl29_21])],[avatar_definition]) ).
fof(f1384,plain,
( k6_lopclset(sK0) = g3_lattices(k1_lopclset(sK0),k4_lopclset(sK0),k5_lopclset(sK0))
| ~ spl29_21 ),
inference(avatar_component_clause,[],[f1382]) ).
fof(f1385,plain,
( spl29_21
| spl29_1
| ~ spl29_2 ),
inference(avatar_split_clause,[],[f683,f610,f605,f1382]) ).
fof(f1388,plain,
( ! [X0,X1] :
( k3_lopclset(sK0,X0,X1) = k2_lattices(k6_lopclset(sK0),X0,X1)
| ~ m2_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK0)),k1_lopclset(sK0))
| ~ m2_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0)),k1_lopclset(sK0))
| ~ m1_subset_1(X1,u1_struct_0(k6_lopclset(sK0)))
| ~ m1_subset_1(X0,u1_struct_0(k6_lopclset(sK0)))
| v3_struct_0(sK0)
| ~ v2_pre_topc(sK0)
| ~ l1_pre_topc(sK0) )
| ~ spl29_21 ),
inference(superposition,[],[f599,f1384]) ).
fof(f1395,plain,
( ! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != k6_lopclset(sK0)
| k1_lopclset(sK0) = X0
| ~ v1_funct_1(k4_lopclset(sK0))
| ~ v1_funct_2(k4_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0))
| ~ m1_relset_1(k4_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0))
| ~ v1_funct_1(k5_lopclset(sK0))
| ~ v1_funct_2(k5_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0))
| ~ m1_relset_1(k5_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0)) )
| ~ spl29_21 ),
inference(superposition,[],[f556,f1384]) ).
fof(f1398,plain,
( v3_lattices(k6_lopclset(sK0))
| ~ v1_funct_1(k4_lopclset(sK0))
| ~ v1_funct_2(k4_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0))
| ~ m1_relset_1(k4_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0))
| ~ v1_funct_1(k5_lopclset(sK0))
| ~ v1_funct_2(k5_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0))
| ~ m1_relset_1(k5_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0))
| ~ spl29_21 ),
inference(superposition,[],[f570,f1384]) ).
fof(f1399,plain,
( v3_lattices(k6_lopclset(sK0))
| ~ v1_funct_2(k4_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0))
| ~ m1_relset_1(k4_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0))
| ~ v1_funct_1(k5_lopclset(sK0))
| ~ v1_funct_2(k5_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0))
| ~ m1_relset_1(k5_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0))
| spl29_1
| ~ spl29_2
| ~ spl29_21 ),
inference(forward_subsumption_resolution,[],[f1398,f691]) ).
fof(f1400,plain,
( ! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != k6_lopclset(sK0)
| k1_lopclset(sK0) = X0
| ~ v1_funct_2(k4_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0))
| ~ m1_relset_1(k4_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0))
| ~ v1_funct_1(k5_lopclset(sK0))
| ~ v1_funct_2(k5_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0))
| ~ m1_relset_1(k5_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0)) )
| spl29_1
| ~ spl29_2
| ~ spl29_21 ),
inference(forward_subsumption_resolution,[],[f1395,f691]) ).
fof(f1404,plain,
( ! [X0,X1] :
( k3_lopclset(sK0,X0,X1) = k2_lattices(k6_lopclset(sK0),X0,X1)
| ~ m2_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK0)),k1_lopclset(sK0))
| ~ m2_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0)),k1_lopclset(sK0))
| ~ m1_subset_1(X1,u1_struct_0(k6_lopclset(sK0)))
| ~ m1_subset_1(X0,u1_struct_0(k6_lopclset(sK0)))
| ~ v2_pre_topc(sK0)
| ~ l1_pre_topc(sK0) )
| spl29_1
| ~ spl29_21 ),
inference(forward_subsumption_resolution,[],[f1388,f607]) ).
fof(f1407,plain,
( v3_lattices(k6_lopclset(sK0))
| ~ m1_relset_1(k4_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0))
| ~ v1_funct_1(k5_lopclset(sK0))
| ~ v1_funct_2(k5_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0))
| ~ m1_relset_1(k5_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0))
| spl29_1
| ~ spl29_2
| ~ spl29_21 ),
inference(forward_subsumption_resolution,[],[f1399,f692]) ).
fof(f1408,plain,
( ! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != k6_lopclset(sK0)
| k1_lopclset(sK0) = X0
| ~ m1_relset_1(k4_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0))
| ~ v1_funct_1(k5_lopclset(sK0))
| ~ v1_funct_2(k5_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0))
| ~ m1_relset_1(k5_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0)) )
| spl29_1
| ~ spl29_2
| ~ spl29_21 ),
inference(forward_subsumption_resolution,[],[f1400,f692]) ).
fof(f1412,plain,
( ! [X0,X1] :
( k3_lopclset(sK0,X0,X1) = k2_lattices(k6_lopclset(sK0),X0,X1)
| ~ m2_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK0)),k1_lopclset(sK0))
| ~ m2_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0)),k1_lopclset(sK0))
| ~ m1_subset_1(X1,u1_struct_0(k6_lopclset(sK0)))
| ~ m1_subset_1(X0,u1_struct_0(k6_lopclset(sK0)))
| ~ l1_pre_topc(sK0) )
| spl29_1
| ~ spl29_6
| ~ spl29_21 ),
inference(forward_subsumption_resolution,[],[f1404,f848]) ).
fof(f1415,plain,
( v3_lattices(k6_lopclset(sK0))
| ~ m1_relset_1(k4_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0))
| ~ v1_funct_2(k5_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0))
| ~ m1_relset_1(k5_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0))
| spl29_1
| ~ spl29_2
| ~ spl29_21 ),
inference(forward_subsumption_resolution,[],[f1407,f688]) ).
fof(f1416,plain,
( ! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != k6_lopclset(sK0)
| k1_lopclset(sK0) = X0
| ~ m1_relset_1(k4_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0))
| ~ v1_funct_2(k5_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0))
| ~ m1_relset_1(k5_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0)) )
| spl29_1
| ~ spl29_2
| ~ spl29_21 ),
inference(forward_subsumption_resolution,[],[f1408,f688]) ).
fof(f1420,plain,
( ! [X0,X1] :
( k3_lopclset(sK0,X0,X1) = k2_lattices(k6_lopclset(sK0),X0,X1)
| ~ m2_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK0)),k1_lopclset(sK0))
| ~ m2_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0)),k1_lopclset(sK0))
| ~ m1_subset_1(X1,u1_struct_0(k6_lopclset(sK0)))
| ~ m1_subset_1(X0,u1_struct_0(k6_lopclset(sK0))) )
| spl29_1
| ~ spl29_2
| ~ spl29_6
| ~ spl29_21 ),
inference(forward_subsumption_resolution,[],[f1412,f612]) ).
fof(f1423,plain,
( v3_lattices(k6_lopclset(sK0))
| ~ m1_relset_1(k4_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0))
| ~ m1_relset_1(k5_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0))
| spl29_1
| ~ spl29_2
| ~ spl29_21 ),
inference(forward_subsumption_resolution,[],[f1415,f689]) ).
fof(f1424,plain,
( ! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != k6_lopclset(sK0)
| k1_lopclset(sK0) = X0
| ~ m1_relset_1(k4_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0))
| ~ m1_relset_1(k5_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0)) )
| spl29_1
| ~ spl29_2
| ~ spl29_21 ),
inference(forward_subsumption_resolution,[],[f1416,f689]) ).
fof(f1553,definition,
( spl29_29
<=> l3_lattices(k6_lopclset(sK0)) ),
introduced(definition,[new_symbols(definition,[spl29_29])],[avatar_definition]) ).
fof(f1555,plain,
( l3_lattices(k6_lopclset(sK0))
| ~ spl29_29 ),
inference(avatar_component_clause,[],[f1553]) ).
fof(f1556,plain,
( spl29_29
| spl29_1
| ~ spl29_2 ),
inference(avatar_split_clause,[],[f687,f610,f605,f1553]) ).
fof(f1558,plain,
( k6_lopclset(sK0) = g3_lattices(u1_struct_0(k6_lopclset(sK0)),u2_lattices(k6_lopclset(sK0)),u1_lattices(k6_lopclset(sK0)))
| ~ v3_lattices(k6_lopclset(sK0))
| ~ spl29_29 ),
inference(resolution,[],[f1555,f490]) ).
fof(f1612,definition,
( spl29_32
<=> ! [X0] :
( m2_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0)),k1_lopclset(sK0))
| ~ m1_subset_1(X0,k1_lopclset(sK0)) ) ),
introduced(definition,[new_symbols(definition,[spl29_32])],[avatar_definition]) ).
fof(f1613,plain,
( ! [X0] :
( m2_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0)),k1_lopclset(sK0))
| ~ m1_subset_1(X0,k1_lopclset(sK0)) )
| ~ spl29_32 ),
inference(avatar_component_clause,[],[f1612]) ).
fof(f1614,plain,
( spl29_32
| spl29_1
| ~ spl29_2
| ~ spl29_6
| ~ spl29_7 ),
inference(avatar_split_clause,[],[f884,f873,f846,f610,f605,f1612]) ).
fof(f1995,definition,
( spl29_41
<=> m1_relset_1(k5_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0)) ),
introduced(definition,[new_symbols(definition,[spl29_41])],[avatar_definition]) ).
fof(f1996,plain,
( m1_relset_1(k5_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0))
| ~ spl29_41 ),
inference(avatar_component_clause,[],[f1995]) ).
fof(f1997,plain,
( ~ m1_relset_1(k5_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0))
| spl29_41 ),
inference(avatar_component_clause,[],[f1995]) ).
fof(f1999,definition,
( spl29_42
<=> m1_relset_1(k4_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0)) ),
introduced(definition,[new_symbols(definition,[spl29_42])],[avatar_definition]) ).
fof(f2000,plain,
( m1_relset_1(k4_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0))
| ~ spl29_42 ),
inference(avatar_component_clause,[],[f1999]) ).
fof(f2001,plain,
( ~ m1_relset_1(k4_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0))
| spl29_42 ),
inference(avatar_component_clause,[],[f1999]) ).
fof(f2003,definition,
( spl29_43
<=> ! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != k6_lopclset(sK0)
| k1_lopclset(sK0) = X0 ) ),
introduced(definition,[new_symbols(definition,[spl29_43])],[avatar_definition]) ).
fof(f2004,plain,
( ! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != k6_lopclset(sK0)
| k1_lopclset(sK0) = X0 )
| ~ spl29_43 ),
inference(avatar_component_clause,[],[f2003]) ).
fof(f2005,plain,
( ~ spl29_41
| ~ spl29_42
| spl29_43
| spl29_1
| ~ spl29_2
| ~ spl29_21 ),
inference(avatar_split_clause,[],[f1424,f1382,f610,f605,f2003,f1999,f1995]) ).
fof(f2006,plain,
( ~ m2_relset_1(k5_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0))
| spl29_41 ),
inference(resolution,[],[f1997,f497]) ).
fof(f2007,plain,
( $false
| spl29_1
| ~ spl29_2
| spl29_41 ),
inference(forward_subsumption_resolution,[],[f2006,f690]) ).
fof(f2008,plain,
( spl29_1
| ~ spl29_2
| spl29_41 ),
inference(avatar_contradiction_clause,[],[f2007]) ).
fof(f2011,plain,
( v3_lattices(k6_lopclset(sK0))
| ~ m1_relset_1(k4_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0))
| spl29_1
| ~ spl29_2
| ~ spl29_21
| ~ spl29_41 ),
inference(backward_subsumption_resolution,[],[f1423,f1996]) ).
fof(f2012,plain,
( ~ m2_relset_1(k4_lopclset(sK0),k2_zfmisc_1(k1_lopclset(sK0),k1_lopclset(sK0)),k1_lopclset(sK0))
| spl29_42 ),
inference(resolution,[],[f2001,f497]) ).
fof(f2013,plain,
( $false
| spl29_1
| ~ spl29_2
| spl29_42 ),
inference(forward_subsumption_resolution,[],[f2012,f693]) ).
fof(f2014,plain,
( spl29_1
| ~ spl29_2
| spl29_42 ),
inference(avatar_contradiction_clause,[],[f2013]) ).
fof(f2017,plain,
( v3_lattices(k6_lopclset(sK0))
| spl29_1
| ~ spl29_2
| ~ spl29_21
| ~ spl29_41
| ~ spl29_42 ),
inference(forward_subsumption_resolution,[],[f2011,f2000]) ).
fof(f2018,plain,
( k6_lopclset(sK0) = g3_lattices(u1_struct_0(k6_lopclset(sK0)),u2_lattices(k6_lopclset(sK0)),u1_lattices(k6_lopclset(sK0)))
| spl29_1
| ~ spl29_2
| ~ spl29_21
| ~ spl29_29
| ~ spl29_41
| ~ spl29_42 ),
inference(backward_subsumption_resolution,[],[f1558,f2017]) ).
fof(f2684,definition,
( spl29_66
<=> k6_lopclset(sK0) = g3_lattices(u1_struct_0(k6_lopclset(sK0)),u2_lattices(k6_lopclset(sK0)),u1_lattices(k6_lopclset(sK0))) ),
introduced(definition,[new_symbols(definition,[spl29_66])],[avatar_definition]) ).
fof(f2686,plain,
( k6_lopclset(sK0) = g3_lattices(u1_struct_0(k6_lopclset(sK0)),u2_lattices(k6_lopclset(sK0)),u1_lattices(k6_lopclset(sK0)))
| ~ spl29_66 ),
inference(avatar_component_clause,[],[f2684]) ).
fof(f2687,plain,
( spl29_66
| spl29_1
| ~ spl29_2
| ~ spl29_21
| ~ spl29_29
| ~ spl29_41
| ~ spl29_42 ),
inference(avatar_split_clause,[],[f2018,f1999,f1995,f1553,f1382,f610,f605,f2684]) ).
fof(f2698,plain,
( k6_lopclset(sK0) != k6_lopclset(sK0)
| u1_struct_0(k6_lopclset(sK0)) = k1_lopclset(sK0)
| ~ spl29_43
| ~ spl29_66 ),
inference(superposition,[],[f2004,f2686]) ).
fof(f2703,plain,
( u1_struct_0(k6_lopclset(sK0)) = k1_lopclset(sK0)
| ~ spl29_43
| ~ spl29_66 ),
inference(trivial_inequality_removal,[],[f2698]) ).
fof(f2725,definition,
( spl29_68
<=> u1_struct_0(k6_lopclset(sK0)) = k1_lopclset(sK0) ),
introduced(definition,[new_symbols(definition,[spl29_68])],[avatar_definition]) ).
fof(f2727,plain,
( u1_struct_0(k6_lopclset(sK0)) = k1_lopclset(sK0)
| ~ spl29_68 ),
inference(avatar_component_clause,[],[f2725]) ).
fof(f2728,plain,
( spl29_68
| ~ spl29_43
| ~ spl29_66 ),
inference(avatar_split_clause,[],[f2703,f2684,f2003,f2725]) ).
fof(f2734,plain,
( m1_subset_1(sK1,k1_lopclset(sK0))
| ~ spl29_3
| ~ spl29_68 ),
inference(superposition,[],[f708,f2727]) ).
fof(f2735,plain,
( m1_subset_1(sK2,k1_lopclset(sK0))
| ~ spl29_4
| ~ spl29_68 ),
inference(superposition,[],[f754,f2727]) ).
fof(f2847,definition,
( spl29_70
<=> m1_subset_1(sK1,k1_lopclset(sK0)) ),
introduced(definition,[new_symbols(definition,[spl29_70])],[avatar_definition]) ).
fof(f2849,plain,
( m1_subset_1(sK1,k1_lopclset(sK0))
| ~ spl29_70 ),
inference(avatar_component_clause,[],[f2847]) ).
fof(f2850,plain,
( spl29_70
| ~ spl29_3
| ~ spl29_68 ),
inference(avatar_split_clause,[],[f2734,f2725,f706,f2847]) ).
fof(f2854,plain,
( ! [X0] :
( k3_lopclset(sK0,sK1,X0) = k3_xboole_0(sK1,X0)
| v3_struct_0(sK0)
| ~ v2_pre_topc(sK0)
| ~ l1_pre_topc(sK0)
| ~ m1_subset_1(X0,k1_lopclset(sK0)) )
| ~ spl29_70 ),
inference(resolution,[],[f2849,f565]) ).
fof(f2887,plain,
( ! [X0] :
( k3_lopclset(sK0,sK1,X0) = k3_xboole_0(sK1,X0)
| ~ v2_pre_topc(sK0)
| ~ l1_pre_topc(sK0)
| ~ m1_subset_1(X0,k1_lopclset(sK0)) )
| spl29_1
| ~ spl29_70 ),
inference(forward_subsumption_resolution,[],[f2854,f607]) ).
fof(f2894,plain,
( ! [X0] :
( k3_lopclset(sK0,sK1,X0) = k3_xboole_0(sK1,X0)
| ~ l1_pre_topc(sK0)
| ~ m1_subset_1(X0,k1_lopclset(sK0)) )
| spl29_1
| ~ spl29_6
| ~ spl29_70 ),
inference(forward_subsumption_resolution,[],[f2887,f848]) ).
fof(f2901,plain,
( ! [X0] :
( k3_lopclset(sK0,sK1,X0) = k3_xboole_0(sK1,X0)
| ~ m1_subset_1(X0,k1_lopclset(sK0)) )
| spl29_1
| ~ spl29_2
| ~ spl29_6
| ~ spl29_70 ),
inference(forward_subsumption_resolution,[],[f2894,f612]) ).
fof(f2907,definition,
( spl29_71
<=> m1_subset_1(sK2,k1_lopclset(sK0)) ),
introduced(definition,[new_symbols(definition,[spl29_71])],[avatar_definition]) ).
fof(f2909,plain,
( m1_subset_1(sK2,k1_lopclset(sK0))
| ~ spl29_71 ),
inference(avatar_component_clause,[],[f2907]) ).
fof(f2910,plain,
( spl29_71
| ~ spl29_4
| ~ spl29_68 ),
inference(avatar_split_clause,[],[f2735,f2725,f752,f2907]) ).
fof(f3025,definition,
( spl29_72
<=> ! [X0] :
( k3_lopclset(sK0,sK1,X0) = k3_xboole_0(sK1,X0)
| ~ m1_subset_1(X0,k1_lopclset(sK0)) ) ),
introduced(definition,[new_symbols(definition,[spl29_72])],[avatar_definition]) ).
fof(f3026,plain,
( ! [X0] :
( k3_lopclset(sK0,sK1,X0) = k3_xboole_0(sK1,X0)
| ~ m1_subset_1(X0,k1_lopclset(sK0)) )
| ~ spl29_72 ),
inference(avatar_component_clause,[],[f3025]) ).
fof(f3027,plain,
( spl29_72
| spl29_1
| ~ spl29_2
| ~ spl29_6
| ~ spl29_70 ),
inference(avatar_split_clause,[],[f2901,f2847,f846,f610,f605,f3025]) ).
fof(f3647,definition,
( spl29_91
<=> ! [X0,X1] :
( k3_lopclset(sK0,X0,X1) = k2_lattices(k6_lopclset(sK0),X0,X1)
| ~ m2_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK0)),k1_lopclset(sK0))
| ~ m2_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0)),k1_lopclset(sK0))
| ~ m1_subset_1(X1,u1_struct_0(k6_lopclset(sK0)))
| ~ m1_subset_1(X0,u1_struct_0(k6_lopclset(sK0))) ) ),
introduced(definition,[new_symbols(definition,[spl29_91])],[avatar_definition]) ).
fof(f3648,plain,
( ! [X0,X1] :
( k3_lopclset(sK0,X0,X1) = k2_lattices(k6_lopclset(sK0),X0,X1)
| ~ m2_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK0)),k1_lopclset(sK0))
| ~ m2_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0)),k1_lopclset(sK0))
| ~ m1_subset_1(X1,u1_struct_0(k6_lopclset(sK0)))
| ~ m1_subset_1(X0,u1_struct_0(k6_lopclset(sK0))) )
| ~ spl29_91 ),
inference(avatar_component_clause,[],[f3647]) ).
fof(f3649,plain,
( spl29_91
| spl29_1
| ~ spl29_2
| ~ spl29_6
| ~ spl29_21 ),
inference(avatar_split_clause,[],[f1420,f1382,f846,f610,f605,f3647]) ).
fof(f3650,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X1,k1_lopclset(sK0))
| k3_lopclset(sK0,X0,X1) = k2_lattices(k6_lopclset(sK0),X0,X1)
| ~ m2_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK0)),k1_lopclset(sK0))
| ~ m2_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0)),k1_lopclset(sK0))
| ~ m1_subset_1(X0,u1_struct_0(k6_lopclset(sK0))) )
| ~ spl29_68
| ~ spl29_91 ),
inference(forward_demodulation,[],[f3648,f2727]) ).
fof(f3651,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X1,k1_lopclset(sK0))
| k3_lopclset(sK0,X0,X1) = k2_lattices(k6_lopclset(sK0),X0,X1)
| ~ m2_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0)),k1_lopclset(sK0))
| ~ m1_subset_1(X0,u1_struct_0(k6_lopclset(sK0))) )
| ~ spl29_32
| ~ spl29_68
| ~ spl29_91 ),
inference(forward_subsumption_resolution,[],[f3650,f1613]) ).
fof(f3652,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,k1_lopclset(sK0))
| ~ m1_subset_1(X1,k1_lopclset(sK0))
| k3_lopclset(sK0,X0,X1) = k2_lattices(k6_lopclset(sK0),X0,X1)
| ~ m2_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0)),k1_lopclset(sK0)) )
| ~ spl29_32
| ~ spl29_68
| ~ spl29_91 ),
inference(forward_demodulation,[],[f3651,f2727]) ).
fof(f3653,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,k1_lopclset(sK0))
| ~ m1_subset_1(X1,k1_lopclset(sK0))
| k3_lopclset(sK0,X0,X1) = k2_lattices(k6_lopclset(sK0),X0,X1) )
| ~ spl29_32
| ~ spl29_68
| ~ spl29_91 ),
inference(forward_subsumption_resolution,[],[f3652,f1613]) ).
fof(f3711,definition,
( spl29_93
<=> ! [X0,X1] :
( ~ m1_subset_1(X0,k1_lopclset(sK0))
| ~ m1_subset_1(X1,k1_lopclset(sK0))
| k3_lopclset(sK0,X0,X1) = k2_lattices(k6_lopclset(sK0),X0,X1) ) ),
introduced(definition,[new_symbols(definition,[spl29_93])],[avatar_definition]) ).
fof(f3712,plain,
( ! [X0,X1] :
( k3_lopclset(sK0,X0,X1) = k2_lattices(k6_lopclset(sK0),X0,X1)
| ~ m1_subset_1(X1,k1_lopclset(sK0))
| ~ m1_subset_1(X0,k1_lopclset(sK0)) )
| ~ spl29_93 ),
inference(avatar_component_clause,[],[f3711]) ).
fof(f3713,plain,
( spl29_93
| ~ spl29_32
| ~ spl29_68
| ~ spl29_91 ),
inference(avatar_split_clause,[],[f3653,f3647,f2725,f1612,f3711]) ).
fof(f3730,plain,
( ! [X0] :
( k4_lattices(k6_lopclset(sK0),sK1,X0) = k3_lopclset(sK0,sK1,X0)
| ~ m1_subset_1(X0,u1_struct_0(k6_lopclset(sK0)))
| ~ m1_subset_1(X0,k1_lopclset(sK0))
| ~ m1_subset_1(sK1,k1_lopclset(sK0)) )
| ~ spl29_12
| ~ spl29_93 ),
inference(superposition,[],[f1004,f3712]) ).
fof(f3737,plain,
( ! [X0] :
( k4_lattices(k6_lopclset(sK0),sK1,X0) = k3_lopclset(sK0,sK1,X0)
| ~ m1_subset_1(X0,u1_struct_0(k6_lopclset(sK0)))
| ~ m1_subset_1(X0,k1_lopclset(sK0)) )
| ~ spl29_12
| ~ spl29_70
| ~ spl29_93 ),
inference(forward_subsumption_resolution,[],[f3730,f2849]) ).
fof(f3748,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_lopclset(sK0))
| k4_lattices(k6_lopclset(sK0),sK1,X0) = k3_lopclset(sK0,sK1,X0)
| ~ m1_subset_1(X0,k1_lopclset(sK0)) )
| ~ spl29_12
| ~ spl29_68
| ~ spl29_70
| ~ spl29_93 ),
inference(forward_demodulation,[],[f3737,f2727]) ).
fof(f3749,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_lopclset(sK0))
| k4_lattices(k6_lopclset(sK0),sK1,X0) = k3_lopclset(sK0,sK1,X0) )
| ~ spl29_12
| ~ spl29_68
| ~ spl29_70
| ~ spl29_93 ),
inference(duplicate_literal_removal,[],[f3748]) ).
fof(f3764,definition,
( spl29_94
<=> ! [X0] :
( ~ m1_subset_1(X0,k1_lopclset(sK0))
| k4_lattices(k6_lopclset(sK0),sK1,X0) = k3_lopclset(sK0,sK1,X0) ) ),
introduced(definition,[new_symbols(definition,[spl29_94])],[avatar_definition]) ).
fof(f3765,plain,
( ! [X0] :
( k4_lattices(k6_lopclset(sK0),sK1,X0) = k3_lopclset(sK0,sK1,X0)
| ~ m1_subset_1(X0,k1_lopclset(sK0)) )
| ~ spl29_94 ),
inference(avatar_component_clause,[],[f3764]) ).
fof(f3766,plain,
( spl29_94
| ~ spl29_12
| ~ spl29_68
| ~ spl29_70
| ~ spl29_93 ),
inference(avatar_split_clause,[],[f3749,f3711,f2847,f2725,f1003,f3764]) ).
fof(f3783,plain,
( k3_xboole_0(sK1,sK2) != k3_lopclset(sK0,sK1,sK2)
| ~ m1_subset_1(sK2,k1_lopclset(sK0))
| spl29_5
| ~ spl29_94 ),
inference(superposition,[],[f843,f3765]) ).
fof(f3799,plain,
( ~ m1_subset_1(sK2,k1_lopclset(sK0))
| spl29_5
| ~ spl29_72
| ~ spl29_94 ),
inference(forward_subsumption_resolution,[],[f3783,f3026]) ).
fof(f3820,plain,
( $false
| spl29_5
| ~ spl29_71
| ~ spl29_72
| ~ spl29_94 ),
inference(forward_subsumption_resolution,[],[f3799,f2909]) ).
fof(f3821,plain,
( spl29_5
| ~ spl29_71
| ~ spl29_72
| ~ spl29_94 ),
inference(avatar_contradiction_clause,[],[f3820]) ).
cnf(s1,plain,
~ spl29_1,
inference(sat_conversion,[],[f608]) ).
cnf(s2,plain,
spl29_2,
inference(sat_conversion,[],[f613]) ).
cnf(s3,plain,
spl29_3,
inference(sat_conversion,[],[f709]) ).
cnf(s4,plain,
spl29_4,
inference(sat_conversion,[],[f755]) ).
cnf(s5,plain,
~ spl29_5,
inference(sat_conversion,[],[f844]) ).
cnf(s6,plain,
spl29_6,
inference(sat_conversion,[],[f849]) ).
cnf(s7,plain,
( spl29_1
| ~ spl29_2
| spl29_7 ),
inference(sat_conversion,[],[f875]) ).
cnf(s8,plain,
( spl29_1
| ~ spl29_2
| ~ spl29_8 ),
inference(sat_conversion,[],[f889]) ).
cnf(s10,plain,
( spl29_1
| ~ spl29_2
| spl29_9 ),
inference(sat_conversion,[],[f967]) ).
cnf(s12,plain,
( spl29_1
| ~ spl29_2
| ~ spl29_3
| spl29_8
| ~ spl29_9
| spl29_12 ),
inference(sat_conversion,[],[f1005]) ).
cnf(s21,plain,
( spl29_1
| ~ spl29_2
| spl29_21 ),
inference(sat_conversion,[],[f1385]) ).
cnf(s29,plain,
( spl29_1
| ~ spl29_2
| spl29_29 ),
inference(sat_conversion,[],[f1556]) ).
cnf(s32,plain,
( spl29_1
| ~ spl29_2
| ~ spl29_6
| ~ spl29_7
| spl29_32 ),
inference(sat_conversion,[],[f1614]) ).
cnf(s41,plain,
( spl29_1
| ~ spl29_2
| ~ spl29_21
| ~ spl29_41
| ~ spl29_42
| spl29_43 ),
inference(sat_conversion,[],[f2005]) ).
cnf(s42,plain,
( spl29_1
| ~ spl29_2
| spl29_41 ),
inference(sat_conversion,[],[f2008]) ).
cnf(s43,plain,
( spl29_1
| ~ spl29_2
| spl29_42 ),
inference(sat_conversion,[],[f2014]) ).
cnf(s66,plain,
( spl29_1
| ~ spl29_2
| ~ spl29_21
| ~ spl29_29
| ~ spl29_41
| ~ spl29_42
| spl29_66 ),
inference(sat_conversion,[],[f2687]) ).
cnf(s68,plain,
( ~ spl29_43
| ~ spl29_66
| spl29_68 ),
inference(sat_conversion,[],[f2728]) ).
cnf(s70,plain,
( ~ spl29_3
| ~ spl29_68
| spl29_70 ),
inference(sat_conversion,[],[f2850]) ).
cnf(s71,plain,
( ~ spl29_4
| ~ spl29_68
| spl29_71 ),
inference(sat_conversion,[],[f2910]) ).
cnf(s72,plain,
( spl29_1
| ~ spl29_2
| ~ spl29_6
| ~ spl29_70
| spl29_72 ),
inference(sat_conversion,[],[f3027]) ).
cnf(s91,plain,
( spl29_1
| ~ spl29_2
| ~ spl29_6
| ~ spl29_21
| spl29_91 ),
inference(sat_conversion,[],[f3649]) ).
cnf(s93,plain,
( ~ spl29_32
| ~ spl29_68
| ~ spl29_91
| spl29_93 ),
inference(sat_conversion,[],[f3713]) ).
cnf(s94,plain,
( ~ spl29_12
| ~ spl29_68
| ~ spl29_70
| ~ spl29_93
| spl29_94 ),
inference(sat_conversion,[],[f3766]) ).
cnf(s95,plain,
( spl29_5
| ~ spl29_71
| ~ spl29_72
| ~ spl29_94 ),
inference(sat_conversion,[],[f3821]) ).
cnf(s108,plain,
spl29_42,
inference(rat,[],[s43,s2,s1]) ).
cnf(s109,plain,
spl29_41,
inference(rat,[],[s42,s2,s1]) ).
cnf(s114,plain,
spl29_29,
inference(rat,[],[s29,s2,s1]) ).
cnf(s115,plain,
spl29_21,
inference(rat,[],[s21,s2,s1]) ).
cnf(s117,plain,
spl29_9,
inference(rat,[],[s10,s2,s1]) ).
cnf(s118,plain,
~ spl29_8,
inference(rat,[],[s8,s2,s1]) ).
cnf(s119,plain,
spl29_7,
inference(rat,[],[s7,s2,s1]) ).
cnf(s122,plain,
spl29_91,
inference(rat,[],[s91,s1,s2,s6,s115]) ).
cnf(s123,plain,
spl29_66,
inference(rat,[],[s66,s114,s108,s109,s1,s2,s115]) ).
cnf(s127,plain,
spl29_43,
inference(rat,[],[s41,s1,s108,s109,s2,s115]) ).
cnf(s155,plain,
spl29_12,
inference(rat,[],[s12,s117,s1,s2,s3,s118]) ).
cnf(s158,plain,
spl29_32,
inference(rat,[],[s32,s1,s2,s6,s119]) ).
cnf(s161,plain,
spl29_68,
inference(rat,[],[s68,s123,s127]) ).
cnf(s166,plain,
spl29_93,
inference(rat,[],[s93,s158,s122,s161]) ).
cnf(s171,plain,
spl29_71,
inference(rat,[],[s71,s4,s161]) ).
cnf(s172,plain,
spl29_70,
inference(rat,[],[s70,s3,s161]) ).
cnf(s182,plain,
spl29_72,
inference(rat,[],[s72,s1,s2,s6,s172]) ).
cnf(s183,plain,
spl29_94,
inference(rat,[],[s94,s166,s161,s155,s172]) ).
cnf(s184,plain,
$false,
inference(rat,[],[s95,s171,s5,s183,s182]) ).
fof(f3833,plain,
$false,
inference(avatar_sat_refutation,[],[s184]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : LAT284+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.04/0.32 % Computer : n012.cluster.edu
% 0.04/0.32 % Model : x86_64 x86_64
% 0.04/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/0.32 % Memory : 8046.5625MB
% 0.04/0.32 % OS : Linux 6.8.0-71-generic
% 0.04/0.32 % CPULimit : 300
% 0.04/0.32 % WCLimit : 300
% 0.04/0.32 % DateTime : Sun Sep 27 14:13:35 UTC 2026
% 0.04/0.32 % CPUTime :
% 0.04/0.33 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.04/0.34 Running first-order theorem proving
% 0.04/0.34 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
% 5.06/1.38 % (2416787)Detected formulas, will run a generic FOF schedule.
% 5.06/1.38 % (2416796)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3666356635:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 5.06/1.38 % (2416794)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=473832042:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 5.06/1.38 % (2416792)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=3166283806:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 5.06/1.38 % (2416797)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=358684103:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 5.06/1.38 % (2416793)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=2084893093:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 5.06/1.38 % (2416798)dis-21_1_sil=8000:lcm=predicate:random_seed=3402621073: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)
% 5.06/1.38 % (2416795)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2429131651:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 5.06/1.38 % (2416795)Refutation not found, incomplete strategy
% 5.06/1.38 % (2416795)------------------------------
% 5.06/1.38 % (2416795)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.06/1.38 % (2416795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.06/1.38 % (2416795)CaDiCaL version: 2.1.3
% 5.06/1.38 % (2416795)Termination reason: Refutation not found, incomplete strategy
% 5.06/1.38 % (2416795)Time elapsed: 0.001 s
% 5.06/1.38 % (2416795)Peak memory usage: 88 MB
% 5.06/1.38 % (2416795)Instructions burned: 1 (million)
% 5.06/1.38 % (2416796)Instruction limit reached!
% 5.06/1.38 % (2416796)------------------------------
% 5.06/1.38 % (2416796)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.06/1.38 % (2416796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.06/1.38 % (2416796)CaDiCaL version: 2.1.3
% 5.06/1.38 % (2416796)Termination reason: Instruction limit
% 5.06/1.38 % (2416796)Termination phase: Saturation
% 5.06/1.38 % (2416796)Time elapsed: 0.037 s
% 5.06/1.38 % (2416796)Peak memory usage: 89 MB
% 5.06/1.38 % (2416796)Instructions burned: 120 (million)
% 5.06/1.38 % (2416798)Instruction limit reached!
% 5.06/1.38 % (2416798)------------------------------
% 5.06/1.38 % (2416798)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.06/1.38 % (2416798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.06/1.38 % (2416798)CaDiCaL version: 2.1.3
% 5.06/1.38 % (2416798)Termination reason: Instruction limit
% 5.06/1.38 % (2416798)Termination phase: Saturation
% 5.06/1.38 % (2416798)Time elapsed: 0.039 s
% 5.06/1.38 % (2416798)Peak memory usage: 90 MB
% 5.06/1.38 % (2416798)Instructions burned: 130 (million)
% 5.06/1.38 % (2416797)Instruction limit reached!
% 5.06/1.38 % (2416797)------------------------------
% 5.06/1.38 % (2416797)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.06/1.38 % (2416797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.06/1.38 % (2416797)CaDiCaL version: 2.1.3
% 5.06/1.38 % (2416797)Termination reason: Instruction limit
% 5.06/1.38 % (2416797)Termination phase: Saturation
% 5.06/1.38 % (2416797)Time elapsed: 0.053 s
% 5.06/1.38 % (2416797)Peak memory usage: 90 MB
% 5.06/1.38 % (2416797)Instructions burned: 140 (million)
% 5.06/1.38 % (2416806)lrs+10_1_sil=8000:sp=occurrence:random_seed=3260990183:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 5.06/1.38 % (2416807)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3619042521:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/157Mi)
% 5.06/1.38 % (2416807)Refutation not found, incomplete strategy
% 5.06/1.38 % (2416807)------------------------------
% 5.06/1.38 % (2416807)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.06/1.38 % (2416807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.06/1.38 % (2416807)CaDiCaL version: 2.1.3
% 5.06/1.38 % (2416807)Termination reason: Refutation not found, incomplete strategy
% 5.06/1.38 % (2416807)Time elapsed: 0.002 s
% 5.06/1.38 % (2416807)Peak memory usage: 89 MB
% 5.06/1.38 % (2416807)Instructions burned: 3 (million)
% 5.06/1.38 % (2416795)------------------------------
% 5.06/1.38 % (2416795)------------------------------
% 5.06/1.38 % (2416808)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1926517989:i=325:sd=1:ss=axioms:sgt=32_2998 on theBenchmark for (2998ds/325Mi)
% 5.06/1.38 % (2416806)Instruction limit reached!
% 5.06/1.38 % (2416806)------------------------------
% 5.06/1.38 % (2416806)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.06/1.38 % (2416806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.06/1.38 % (2416806)CaDiCaL version: 2.1.3
% 5.06/1.38 % (2416806)Termination reason: Instruction limit
% 5.06/1.38 % (2416806)Termination phase: Saturation
% 5.06/1.38 % (2416806)Time elapsed: 0.095 s
% 5.06/1.38 % (2416806)Peak memory usage: 92 MB
% 5.06/1.38 % (2416806)Instructions burned: 288 (million)
% 5.06/1.38 % (2416808)Instruction limit reached!
% 5.06/1.38 % (2416808)------------------------------
% 5.06/1.38 % (2416808)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.06/1.38 % (2416808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.06/1.38 % (2416808)CaDiCaL version: 2.1.3
% 5.06/1.38 % (2416808)Termination reason: Instruction limit
% 5.06/1.38 % (2416808)Termination phase: Saturation
% 5.06/1.38 % (2416808)Time elapsed: 0.087 s
% 5.06/1.38 % (2416808)Peak memory usage: 89 MB
% 5.06/1.38 % (2416808)Instructions burned: 326 (million)
% 5.06/1.38 % (2416811)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=2592640002:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 5.06/1.38 % (2416807)------------------------------
% 5.06/1.38 % (2416807)------------------------------
% 5.06/1.38 % (2416813)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2008470720:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2996 on theBenchmark for (2996ds/294Mi)
% 5.06/1.38 % (2416811)Instruction limit reached!
% 5.06/1.38 % (2416811)------------------------------
% 5.06/1.38 % (2416811)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.06/1.38 % (2416811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.06/1.38 % (2416811)CaDiCaL version: 2.1.3
% 5.06/1.38 % (2416811)Termination reason: Instruction limit
% 5.06/1.38 % (2416811)Termination phase: Saturation
% 5.06/1.38 % (2416811)Time elapsed: 0.073 s
% 5.06/1.38 % (2416811)Peak memory usage: 92 MB
% 5.06/1.38 % (2416811)Instructions burned: 252 (million)
% 5.06/1.38 % (2416813)Refutation not found, incomplete strategy
% 5.06/1.38 % (2416813)------------------------------
% 5.06/1.38 % (2416813)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.06/1.38 % (2416813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.06/1.38 % (2416813)CaDiCaL version: 2.1.3
% 5.06/1.38 % (2416813)Termination reason: Refutation not found, incomplete strategy
% 5.06/1.38 % (2416813)Time elapsed: 0.003 s
% 5.06/1.38 % (2416813)Peak memory usage: 89 MB
% 5.06/1.38 % (2416813)Instructions burned: 9 (million)
% 5.06/1.38 % (2416814)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=725157618:i=2350_2996 on theBenchmark for (2996ds/2350Mi)
% 5.06/1.38 % (2416816)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3151757755:cts=off:i=113:fsr=off:ss=included:sgt=4_2995 on theBenchmark for (2995ds/113Mi)
% 5.06/1.38 % (2416816)Instruction limit reached!
% 5.06/1.38 % (2416816)------------------------------
% 5.06/1.38 % (2416816)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.06/1.38 % (2416816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.06/1.38 % (2416816)CaDiCaL version: 2.1.3
% 5.06/1.38 % (2416816)Termination reason: Instruction limit
% 5.06/1.38 % (2416816)Termination phase: Saturation
% 5.06/1.38 % (2416816)Time elapsed: 0.041 s
% 5.06/1.38 % (2416816)Peak memory usage: 91 MB
% 5.06/1.38 % (2416816)Instructions burned: 116 (million)
% 5.06/1.38 % (2416818)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=748448406:i=127:av=off:fsr=off:sup=off_2995 on theBenchmark for (2995ds/127Mi)
% 5.06/1.38 % (2416813)------------------------------
% 5.06/1.38 % (2416813)------------------------------
% 5.06/1.38 % (2416818)Instruction limit reached!
% 5.06/1.38 % (2416818)------------------------------
% 5.06/1.38 % (2416818)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.06/1.38 % (2416818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.06/1.38 % (2416818)CaDiCaL version: 2.1.3
% 5.06/1.38 % (2416818)Termination reason: Instruction limit
% 5.06/1.38 % (2416818)Termination phase: Saturation
% 5.06/1.38 % (2416818)Time elapsed: 0.034 s
% 5.06/1.38 % (2416818)Peak memory usage: 89 MB
% 5.06/1.38 % (2416818)Instructions burned: 129 (million)
% 5.06/1.38 % (2416794)First to succeed.
% 5.06/1.38 % (2416794)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2416787"
% 5.06/1.38 % (2416792)Also succeeded, but the first one will report.
% 5.06/1.38 % (2416821)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=324749568:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2993 on theBenchmark for (2993ds/114Mi)
% 5.06/1.38 % (2416821)Instruction limit reached!
% 5.06/1.38 % (2416821)------------------------------
% 5.06/1.38 % (2416821)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.06/1.38 % (2416821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.06/1.38 % (2416821)CaDiCaL version: 2.1.3
% 5.06/1.38 % (2416821)Termination reason: Instruction limit
% 5.06/1.38 % (2416821)Termination phase: Saturation
% 5.06/1.38 % (2416821)Time elapsed: 0.032 s
% 5.06/1.38 % (2416821)Peak memory usage: 89 MB
% 5.06/1.38 % (2416821)Instructions burned: 115 (million)
% 5.06/1.38 % (2416824)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3903592368:i=437:sd=1:aac=none:ss=included_2993 on theBenchmark for (2993ds/437Mi)
% 5.06/1.38 % (2416823)lrs+10_1_sil=8000:sp=occurrence:random_seed=2814165105:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2993 on theBenchmark for (2993ds/907Mi)
% 5.06/1.38 % (2416824)Refutation not found, incomplete strategy
% 5.06/1.38 % (2416824)------------------------------
% 5.06/1.38 % (2416824)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.06/1.38 % (2416824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.06/1.38 % (2416824)CaDiCaL version: 2.1.3
% 5.06/1.38 % (2416824)Termination reason: Refutation not found, incomplete strategy
% 5.06/1.38 % (2416824)Time elapsed: 0.005 s
% 5.06/1.38 % (2416824)Peak memory usage: 89 MB
% 5.06/1.38 % (2416824)Instructions burned: 12 (million)
% 5.06/1.38 % (2416794)Refutation found. Thanks to Tanya!
% 5.06/1.38 % SZS status Theorem for theBenchmark
% 5.06/1.38 % SZS output start Proof for theBenchmark
% See solution above
% 6.01/1.47 % (2416794)------------------------------
% 6.01/1.47 % (2416794)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.01/1.47 % (2416794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.01/1.47 % (2416794)CaDiCaL version: 2.1.3
% 6.01/1.47 % (2416794)Termination reason: Refutation
% 6.01/1.47 % (2416794)Time elapsed: 0.525 s
% 6.01/1.47 % (2416794)Peak memory usage: 133 MB
% 6.01/1.47 % (2416794)Instructions burned: 1433 (million)
% 6.01/1.47 % (2416794)------------------------------
% 6.01/1.47 % (2416794)------------------------------
% 6.01/1.47 % (2416787)Success in time 0.833 s
% 6.01/1.47 % Vampire exiting
%------------------------------------------------------------------------------