%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LAT287+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n019.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 : Thu Sep 24 01:02:33 PM UTC 2026
% Result : Theorem 6.55s 1.40s
% Output : CNFRefutation 6.55s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 23
% Syntax : Number of formulae : 193 ( 36 unt; 0 def)
% Number of atoms : 634 ( 60 equ)
% Maximal formula atoms : 12 ( 3 avg)
% Number of connectives : 712 ( 271 ~; 324 |; 89 &)
% ( 5 <=>; 23 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 24 ( 22 usr; 1 prp; 0-3 aty)
% Number of functors : 16 ( 16 usr; 2 con; 0-3 aty)
% Number of variables : 196 ( 190 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [A] :
( ( l1_pre_topc(A)
& v2_pre_topc(A)
& ~ v3_struct_0(A) )
=> m1_subset_1(k1_pre_topc(A),u1_struct_0(k6_lopclset(A))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
~ ! [A] :
( ( l1_pre_topc(A)
& v2_pre_topc(A)
& ~ v3_struct_0(A) )
=> m1_subset_1(k1_pre_topc(A),u1_struct_0(k6_lopclset(A))) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f9,axiom,
! [A] :
( l3_lattices(A)
=> ( v3_lattices(A)
=> A = g3_lattices(u1_struct_0(A),u2_lattices(A),u1_lattices(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [A,B,C] :
( m2_relset_1(C,A,B)
<=> m1_relset_1(C,A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f52,axiom,
! [A,B] :
( r2_hidden(A,B)
=> m1_subset_1(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f54,axiom,
! [A,B,C] :
~ ( v1_xboole_0(C)
& m1_subset_1(B,k1_zfmisc_1(C))
& r2_hidden(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f55,axiom,
! [A,B,C] :
( ( m1_relset_1(C,k2_zfmisc_1(A,A),A)
& v1_funct_2(C,k2_zfmisc_1(A,A),A)
& v1_funct_1(C)
& m1_relset_1(B,k2_zfmisc_1(A,A),A)
& v1_funct_2(B,k2_zfmisc_1(A,A),A)
& v1_funct_1(B) )
=> ! [D,E,F] :
( g3_lattices(A,B,C) = g3_lattices(D,E,F)
=> ( C = F
& B = E
& A = D ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f59,axiom,
! [A,B,C] :
( ( m1_relset_1(C,k2_zfmisc_1(A,A),A)
& v1_funct_2(C,k2_zfmisc_1(A,A),A)
& v1_funct_1(C)
& m1_relset_1(B,k2_zfmisc_1(A,A),A)
& v1_funct_2(B,k2_zfmisc_1(A,A),A)
& v1_funct_1(B) )
=> ( l3_lattices(g3_lattices(A,B,C))
& v3_lattices(g3_lattices(A,B,C)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f60,axiom,
! [A] :
( ( l1_pre_topc(A)
& v2_pre_topc(A)
& ~ v3_struct_0(A) )
=> ( m2_relset_1(k4_lopclset(A),k2_zfmisc_1(k1_lopclset(A),k1_lopclset(A)),k1_lopclset(A))
& v1_funct_2(k4_lopclset(A),k2_zfmisc_1(k1_lopclset(A),k1_lopclset(A)),k1_lopclset(A))
& v1_funct_1(k4_lopclset(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f61,axiom,
! [A] :
( ( l1_pre_topc(A)
& v2_pre_topc(A)
& ~ v3_struct_0(A) )
=> ( m2_relset_1(k5_lopclset(A),k2_zfmisc_1(k1_lopclset(A),k1_lopclset(A)),k1_lopclset(A))
& v1_funct_2(k5_lopclset(A),k2_zfmisc_1(k1_lopclset(A),k1_lopclset(A)),k1_lopclset(A))
& v1_funct_1(k5_lopclset(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f69,axiom,
! [A] :
( l1_struct_0(A)
=> ( v5_membered(k1_pre_topc(A))
& v4_membered(k1_pre_topc(A))
& v3_membered(k1_pre_topc(A))
& v2_membered(k1_pre_topc(A))
& v1_membered(k1_pre_topc(A))
& v1_xboole_0(k1_pre_topc(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f73,axiom,
! [A,B] :
( m1_subset_1(A,B)
=> ( r2_hidden(A,B)
| v1_xboole_0(B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f74,axiom,
! [A] :
( v1_xboole_0(A)
=> A = k1_xboole_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f78,axiom,
! [A,B] :
( ( l1_pre_topc(B)
& ~ v3_struct_0(B) )
=> ( r2_hidden(A,a_1_0_lopclset(B))
<=> ? [C] :
( v4_pre_topc(C,B)
& v3_pre_topc(C,B)
& A = C
& m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B))) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f80,axiom,
! [A] :
? [B] : m1_subset_1(B,A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f82,axiom,
! [A,B] :
( ( m1_subset_1(B,k1_zfmisc_1(A))
& ~ v1_xboole_0(B)
& ~ v1_xboole_0(A) )
=> ! [C] :
( m2_subset_1(C,A,B)
<=> m1_subset_1(C,B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f83,axiom,
! [A] :
( ( l1_pre_topc(A)
& ~ v3_struct_0(A) )
=> m1_subset_1(k1_lopclset(A),k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(A)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f84,axiom,
! [A] :
( l1_struct_0(A)
=> m1_subset_1(k1_pre_topc(A),k1_zfmisc_1(u1_struct_0(A))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f86,axiom,
! [A] :
( ( l1_pre_topc(A)
& v2_pre_topc(A)
& ~ v3_struct_0(A) )
=> ( l3_lattices(k6_lopclset(A))
& v10_lattices(k6_lopclset(A))
& ~ v3_struct_0(k6_lopclset(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f87,axiom,
! [A] :
( l1_pre_topc(A)
=> l1_struct_0(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f92,axiom,
! [A] :
( ( l1_pre_topc(A)
& v2_pre_topc(A)
& ~ v3_struct_0(A) )
=> ~ v1_xboole_0(k1_lopclset(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f94,axiom,
! [A] :
( ( l1_pre_topc(A)
& ~ v3_struct_0(A) )
=> k1_lopclset(A) = a_1_0_lopclset(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f95,axiom,
! [A] :
( ( l1_pre_topc(A)
& v2_pre_topc(A)
& ~ v3_struct_0(A) )
=> k6_lopclset(A) = g3_lattices(k1_lopclset(A),k4_lopclset(A),k5_lopclset(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f96,axiom,
! [A] :
( ( l1_pre_topc(A)
& v2_pre_topc(A)
& ~ v3_struct_0(A) )
=> m2_subset_1(k1_pre_topc(A),k1_zfmisc_1(u1_struct_0(A)),k1_lopclset(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f97,plain,
? [A] :
( ~ m1_subset_1(k1_pre_topc(A),u1_struct_0(k6_lopclset(A)))
& l1_pre_topc(A)
& v2_pre_topc(A)
& ~ v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f98,plain,
( ~ m1_subset_1(k1_pre_topc(sK0_skl),u1_struct_0(k6_lopclset(sK0_skl)))
& l1_pre_topc(sK0_skl)
& v2_pre_topc(sK0_skl)
& ~ v3_struct_0(sK0_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(A,sK0_skl)],[f97]) ).
fof(f99,plain,
~ v3_struct_0(sK0_skl),
inference(cnf_transformation,[status(thm)],[f98]) ).
fof(f100,plain,
v2_pre_topc(sK0_skl),
inference(cnf_transformation,[status(thm)],[f98]) ).
fof(f101,plain,
l1_pre_topc(sK0_skl),
inference(cnf_transformation,[status(thm)],[f98]) ).
fof(f102,plain,
~ m1_subset_1(k1_pre_topc(sK0_skl),u1_struct_0(k6_lopclset(sK0_skl))),
inference(cnf_transformation,[status(thm)],[f98]) ).
fof(f125,plain,
! [A] :
( A = g3_lattices(u1_struct_0(A),u2_lattices(A),u1_lattices(A))
| ~ v3_lattices(A)
| ~ l3_lattices(A) ),
inference(pre_NNF_transformation,[status(thm)],[f9]) ).
fof(f126,plain,
! [X0] :
( X0 = g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))
| ~ v3_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f125]) ).
fof(f135,plain,
! [A,B,C] :
( ( ~ m1_relset_1(C,A,B)
| m2_relset_1(C,A,B) )
& ( m1_relset_1(C,A,B)
| ~ m2_relset_1(C,A,B) ) ),
inference(NNF_transformation,[status(thm)],[f14]) ).
fof(f136,plain,
( ! [A,B,C] :
( ~ m1_relset_1(C,A,B)
| m2_relset_1(C,A,B) )
& ! [A,B,C] :
( m1_relset_1(C,A,B)
| ~ m2_relset_1(C,A,B) ) ),
inference(miniscoping,[status(thm)],[f135]) ).
fof(f137,plain,
! [X0,X1,X2] :
( m1_relset_1(X0,X1,X2)
| ~ m2_relset_1(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f136]) ).
fof(f269,plain,
! [A,B] :
( m1_subset_1(A,B)
| ~ r2_hidden(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f52]) ).
fof(f270,plain,
! [X0,X1] :
( m1_subset_1(X0,X1)
| ~ r2_hidden(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f269]) ).
fof(f274,plain,
! [A,B,C] :
( ~ v1_xboole_0(C)
| ~ m1_subset_1(B,k1_zfmisc_1(C))
| ~ r2_hidden(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f54]) ).
fof(f275,plain,
! [C] :
( ~ v1_xboole_0(C)
| ! [B] :
( ~ m1_subset_1(B,k1_zfmisc_1(C))
| ! [A] : ~ r2_hidden(A,B) ) ),
inference(miniscoping,[status(thm)],[f274]) ).
fof(f276,plain,
! [X0,X1,X2] :
( ~ v1_xboole_0(X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ r2_hidden(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f275]) ).
fof(f277,plain,
! [A,B,C] :
( ! [D,E,F] :
( ( C = F
& B = E
& A = D )
| g3_lattices(A,B,C) != g3_lattices(D,E,F) )
| ~ m1_relset_1(C,k2_zfmisc_1(A,A),A)
| ~ v1_funct_2(C,k2_zfmisc_1(A,A),A)
| ~ v1_funct_1(C)
| ~ m1_relset_1(B,k2_zfmisc_1(A,A),A)
| ~ v1_funct_2(B,k2_zfmisc_1(A,A),A)
| ~ v1_funct_1(B) ),
inference(pre_NNF_transformation,[status(thm)],[f55]) ).
fof(f278,plain,
! [X0,X1,X2,X3,X4,X5] :
( X1 = X3
| g3_lattices(X1,X0,X2) != g3_lattices(X3,X4,X5)
| ~ m1_relset_1(X2,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(X2)
| ~ m1_relset_1(X0,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_2(X0,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(X0) ),
inference(cnf_transformation,[status(thm)],[f277]) ).
fof(f287,plain,
! [A,B,C] :
( ( l3_lattices(g3_lattices(A,B,C))
& v3_lattices(g3_lattices(A,B,C)) )
| ~ m1_relset_1(C,k2_zfmisc_1(A,A),A)
| ~ v1_funct_2(C,k2_zfmisc_1(A,A),A)
| ~ v1_funct_1(C)
| ~ m1_relset_1(B,k2_zfmisc_1(A,A),A)
| ~ v1_funct_2(B,k2_zfmisc_1(A,A),A)
| ~ v1_funct_1(B) ),
inference(pre_NNF_transformation,[status(thm)],[f59]) ).
fof(f288,plain,
! [X0,X1,X2] :
( v3_lattices(g3_lattices(X1,X0,X2))
| ~ m1_relset_1(X2,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(X2)
| ~ m1_relset_1(X0,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_2(X0,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(X0) ),
inference(cnf_transformation,[status(thm)],[f287]) ).
fof(f290,plain,
! [A] :
( ( m2_relset_1(k4_lopclset(A),k2_zfmisc_1(k1_lopclset(A),k1_lopclset(A)),k1_lopclset(A))
& v1_funct_2(k4_lopclset(A),k2_zfmisc_1(k1_lopclset(A),k1_lopclset(A)),k1_lopclset(A))
& v1_funct_1(k4_lopclset(A)) )
| ~ l1_pre_topc(A)
| ~ v2_pre_topc(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f60]) ).
fof(f291,plain,
! [X0] :
( v1_funct_1(k4_lopclset(X0))
| ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f290]) ).
fof(f292,plain,
! [X0] :
( v1_funct_2(k4_lopclset(X0),k2_zfmisc_1(k1_lopclset(X0),k1_lopclset(X0)),k1_lopclset(X0))
| ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f290]) ).
fof(f293,plain,
! [X0] :
( m2_relset_1(k4_lopclset(X0),k2_zfmisc_1(k1_lopclset(X0),k1_lopclset(X0)),k1_lopclset(X0))
| ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f290]) ).
fof(f294,plain,
! [A] :
( ( m2_relset_1(k5_lopclset(A),k2_zfmisc_1(k1_lopclset(A),k1_lopclset(A)),k1_lopclset(A))
& v1_funct_2(k5_lopclset(A),k2_zfmisc_1(k1_lopclset(A),k1_lopclset(A)),k1_lopclset(A))
& v1_funct_1(k5_lopclset(A)) )
| ~ l1_pre_topc(A)
| ~ v2_pre_topc(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f61]) ).
fof(f295,plain,
! [X0] :
( v1_funct_1(k5_lopclset(X0))
| ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f294]) ).
fof(f296,plain,
! [X0] :
( v1_funct_2(k5_lopclset(X0),k2_zfmisc_1(k1_lopclset(X0),k1_lopclset(X0)),k1_lopclset(X0))
| ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f294]) ).
fof(f297,plain,
! [X0] :
( m2_relset_1(k5_lopclset(X0),k2_zfmisc_1(k1_lopclset(X0),k1_lopclset(X0)),k1_lopclset(X0))
| ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f294]) ).
fof(f322,plain,
! [A] :
( ( v5_membered(k1_pre_topc(A))
& v4_membered(k1_pre_topc(A))
& v3_membered(k1_pre_topc(A))
& v2_membered(k1_pre_topc(A))
& v1_membered(k1_pre_topc(A))
& v1_xboole_0(k1_pre_topc(A)) )
| ~ l1_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f69]) ).
fof(f323,plain,
! [X0] :
( v1_xboole_0(k1_pre_topc(X0))
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f322]) ).
fof(f338,plain,
! [A,B] :
( r2_hidden(A,B)
| v1_xboole_0(B)
| ~ m1_subset_1(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f73]) ).
fof(f339,plain,
! [X0,X1] :
( r2_hidden(X0,X1)
| v1_xboole_0(X1)
| ~ m1_subset_1(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f338]) ).
fof(f340,plain,
! [A] :
( A = k1_xboole_0
| ~ v1_xboole_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f74]) ).
fof(f341,plain,
! [X0] :
( X0 = k1_xboole_0
| ~ v1_xboole_0(X0) ),
inference(cnf_transformation,[status(thm)],[f340]) ).
fof(f353,plain,
! [A,B] :
( ( r2_hidden(A,a_1_0_lopclset(B))
<=> ? [C] :
( v4_pre_topc(C,B)
& v3_pre_topc(C,B)
& A = C
& m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B))) ) )
| ~ l1_pre_topc(B)
| v3_struct_0(B) ),
inference(pre_NNF_transformation,[status(thm)],[f78]) ).
fof(f354,plain,
! [A,B] :
( ( ( ! [C] :
( ~ v4_pre_topc(C,B)
| ~ v3_pre_topc(C,B)
| A != C
| ~ m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B))) )
| r2_hidden(A,a_1_0_lopclset(B)) )
& ( ? [C] :
( v4_pre_topc(C,B)
& v3_pre_topc(C,B)
& A = C
& m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B))) )
| ~ r2_hidden(A,a_1_0_lopclset(B)) ) )
| ~ l1_pre_topc(B)
| v3_struct_0(B) ),
inference(NNF_transformation,[status(thm)],[f353]) ).
fof(f355,plain,
! [B] :
( ( ! [A] :
( ! [C] :
( ~ v4_pre_topc(C,B)
| ~ v3_pre_topc(C,B)
| A != C
| ~ m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B))) )
| r2_hidden(A,a_1_0_lopclset(B)) )
& ! [A] :
( ? [C] :
( v4_pre_topc(C,B)
& v3_pre_topc(C,B)
& A = C
& m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B))) )
| ~ r2_hidden(A,a_1_0_lopclset(B)) ) )
| ~ l1_pre_topc(B)
| v3_struct_0(B) ),
inference(miniscoping,[status(thm)],[f354]) ).
fof(f356,plain,
! [B] :
( ( ! [A] :
( ! [C] :
( ~ v4_pre_topc(C,B)
| ~ v3_pre_topc(C,B)
| A != C
| ~ m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B))) )
| r2_hidden(A,a_1_0_lopclset(B)) )
& ! [A] :
( ( v4_pre_topc(sK21_skl(A,B),B)
& v3_pre_topc(sK21_skl(A,B),B)
& A = sK21_skl(A,B)
& m1_subset_1(sK21_skl(A,B),k1_zfmisc_1(u1_struct_0(B))) )
| ~ r2_hidden(A,a_1_0_lopclset(B)) ) )
| ~ l1_pre_topc(B)
| v3_struct_0(B) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK21_skl]),skolemize(C,sK21_skl(A,B))],[f355]) ).
fof(f358,plain,
! [X0,X1] :
( X1 = sK21_skl(X1,X0)
| ~ r2_hidden(X1,a_1_0_lopclset(X0))
| ~ l1_pre_topc(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f356]) ).
fof(f359,plain,
! [X0,X1] :
( v3_pre_topc(sK21_skl(X1,X0),X0)
| ~ r2_hidden(X1,a_1_0_lopclset(X0))
| ~ l1_pre_topc(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f356]) ).
fof(f360,plain,
! [X0,X1] :
( v4_pre_topc(sK21_skl(X1,X0),X0)
| ~ r2_hidden(X1,a_1_0_lopclset(X0))
| ~ l1_pre_topc(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f356]) ).
fof(f361,plain,
! [X0,X1,X2] :
( ~ v4_pre_topc(X2,X0)
| ~ v3_pre_topc(X2,X0)
| X1 != X2
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
| r2_hidden(X1,a_1_0_lopclset(X0))
| ~ l1_pre_topc(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f356]) ).
fof(f364,plain,
! [A] : m1_subset_1(sK23_skl(A),A),
inference(skolemize,[status(esa),new_symbols(skolem,[sK23_skl]),skolemize(B,sK23_skl(A))],[f80]) ).
fof(f365,plain,
! [X0] : m1_subset_1(sK23_skl(X0),X0),
inference(cnf_transformation,[status(thm)],[f364]) ).
fof(f369,plain,
! [A,B] :
( ! [C] :
( m2_subset_1(C,A,B)
<=> m1_subset_1(C,B) )
| ~ m1_subset_1(B,k1_zfmisc_1(A))
| v1_xboole_0(B)
| v1_xboole_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f82]) ).
fof(f370,plain,
! [A,B] :
( ! [C] :
( ( ~ m1_subset_1(C,B)
| m2_subset_1(C,A,B) )
& ( m1_subset_1(C,B)
| ~ m2_subset_1(C,A,B) ) )
| ~ m1_subset_1(B,k1_zfmisc_1(A))
| v1_xboole_0(B)
| v1_xboole_0(A) ),
inference(NNF_transformation,[status(thm)],[f369]) ).
fof(f371,plain,
! [A,B] :
( ( ! [C] :
( ~ m1_subset_1(C,B)
| m2_subset_1(C,A,B) )
& ! [C] :
( m1_subset_1(C,B)
| ~ m2_subset_1(C,A,B) ) )
| ~ m1_subset_1(B,k1_zfmisc_1(A))
| v1_xboole_0(B)
| v1_xboole_0(A) ),
inference(miniscoping,[status(thm)],[f370]) ).
fof(f372,plain,
! [X0,X1,X2] :
( m1_subset_1(X2,X1)
| ~ m2_subset_1(X2,X0,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| v1_xboole_0(X1)
| v1_xboole_0(X0) ),
inference(cnf_transformation,[status(thm)],[f371]) ).
fof(f374,plain,
! [A] :
( m1_subset_1(k1_lopclset(A),k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(A))))
| ~ l1_pre_topc(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f83]) ).
fof(f375,plain,
! [X0] :
( m1_subset_1(k1_lopclset(X0),k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(X0))))
| ~ l1_pre_topc(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f374]) ).
fof(f376,plain,
! [A] :
( m1_subset_1(k1_pre_topc(A),k1_zfmisc_1(u1_struct_0(A)))
| ~ l1_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f84]) ).
fof(f377,plain,
! [X0] :
( m1_subset_1(k1_pre_topc(X0),k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f376]) ).
fof(f378,plain,
! [A] :
( ( l3_lattices(k6_lopclset(A))
& v10_lattices(k6_lopclset(A))
& ~ v3_struct_0(k6_lopclset(A)) )
| ~ l1_pre_topc(A)
| ~ v2_pre_topc(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f86]) ).
fof(f381,plain,
! [X0] :
( l3_lattices(k6_lopclset(X0))
| ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f378]) ).
fof(f382,plain,
! [A] :
( l1_struct_0(A)
| ~ l1_pre_topc(A) ),
inference(pre_NNF_transformation,[status(thm)],[f87]) ).
fof(f383,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[status(thm)],[f382]) ).
fof(f391,plain,
! [A] :
( ~ v1_xboole_0(k1_lopclset(A))
| ~ l1_pre_topc(A)
| ~ v2_pre_topc(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f92]) ).
fof(f392,plain,
! [X0] :
( ~ v1_xboole_0(k1_lopclset(X0))
| ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f391]) ).
fof(f397,plain,
! [A] :
( k1_lopclset(A) = a_1_0_lopclset(A)
| ~ l1_pre_topc(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f94]) ).
fof(f398,plain,
! [X0] :
( k1_lopclset(X0) = a_1_0_lopclset(X0)
| ~ l1_pre_topc(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f397]) ).
fof(f399,plain,
! [A] :
( k6_lopclset(A) = g3_lattices(k1_lopclset(A),k4_lopclset(A),k5_lopclset(A))
| ~ l1_pre_topc(A)
| ~ v2_pre_topc(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f95]) ).
fof(f400,plain,
! [X0] :
( k6_lopclset(X0) = g3_lattices(k1_lopclset(X0),k4_lopclset(X0),k5_lopclset(X0))
| ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f399]) ).
fof(f401,plain,
! [A] :
( m2_subset_1(k1_pre_topc(A),k1_zfmisc_1(u1_struct_0(A)),k1_lopclset(A))
| ~ l1_pre_topc(A)
| ~ v2_pre_topc(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f96]) ).
fof(f402,plain,
! [X0] :
( m2_subset_1(k1_pre_topc(X0),k1_zfmisc_1(u1_struct_0(X0)),k1_lopclset(X0))
| ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f401]) ).
fof(f403,plain,
! [X0,X1] :
( ~ v4_pre_topc(X1,X0)
| ~ v3_pre_topc(X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| r2_hidden(X1,a_1_0_lopclset(X0))
| ~ l1_pre_topc(X0)
| v3_struct_0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f361]) ).
fof(f407,plain,
( l3_lattices(k6_lopclset(sK0_skl))
| ~ l1_pre_topc(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f381,f100]) ).
fof(f408,plain,
( l3_lattices(k6_lopclset(sK0_skl))
| ~ l1_pre_topc(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f407,f99]) ).
fof(f409,plain,
l3_lattices(k6_lopclset(sK0_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f408,f101]) ).
fof(f558,plain,
( k6_lopclset(sK0_skl) = g3_lattices(u1_struct_0(k6_lopclset(sK0_skl)),u2_lattices(k6_lopclset(sK0_skl)),u1_lattices(k6_lopclset(sK0_skl)))
| ~ v3_lattices(k6_lopclset(sK0_skl)) ),
inference(resolution,[status(thm)],[f126,f409]) ).
fof(f617,plain,
l1_struct_0(sK0_skl),
inference(resolution,[status(thm)],[f383,f101]) ).
fof(f625,plain,
m1_subset_1(k1_pre_topc(sK0_skl),k1_zfmisc_1(u1_struct_0(sK0_skl))),
inference(resolution,[status(thm)],[f617,f377]) ).
fof(f631,plain,
v1_xboole_0(k1_pre_topc(sK0_skl)),
inference(resolution,[status(thm)],[f617,f323]) ).
fof(f640,plain,
k1_pre_topc(sK0_skl) = k1_xboole_0,
inference(resolution,[status(thm)],[f631,f341]) ).
fof(f703,plain,
m1_subset_1(k1_xboole_0,k1_zfmisc_1(u1_struct_0(sK0_skl))),
inference(backward_demodulation,[status(thm)],[f640,f625]) ).
fof(f710,plain,
~ m1_subset_1(k1_xboole_0,u1_struct_0(k6_lopclset(sK0_skl))),
inference(backward_demodulation,[status(thm)],[f640,f102]) ).
fof(f1337,plain,
! [X0] :
( r2_hidden(sK23_skl(X0),X0)
| v1_xboole_0(X0) ),
inference(resolution,[status(thm)],[f339,f365]) ).
fof(f2238,plain,
! [X0,X1] :
( v1_xboole_0(X0)
| ~ v1_xboole_0(X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(X1)) ),
inference(resolution,[status(thm)],[f276,f1337]) ).
fof(f2288,plain,
( k1_lopclset(sK0_skl) = a_1_0_lopclset(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f398,f101]) ).
fof(f2289,plain,
k1_lopclset(sK0_skl) = a_1_0_lopclset(sK0_skl),
inference(forward_subsumption_resolution,[status(thm)],[f2288,f99]) ).
fof(f2558,plain,
( v1_funct_1(k4_lopclset(sK0_skl))
| ~ l1_pre_topc(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f291,f100]) ).
fof(f2559,plain,
( v1_funct_1(k4_lopclset(sK0_skl))
| ~ l1_pre_topc(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f2558,f99]) ).
fof(f2560,plain,
( v1_funct_2(k4_lopclset(sK0_skl),k2_zfmisc_1(k1_lopclset(sK0_skl),k1_lopclset(sK0_skl)),k1_lopclset(sK0_skl))
| ~ l1_pre_topc(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f292,f100]) ).
fof(f2561,plain,
( v1_funct_2(k4_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),k1_lopclset(sK0_skl)),k1_lopclset(sK0_skl))
| ~ l1_pre_topc(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(forward_demodulation,[status(thm)],[f2289,f2560]) ).
fof(f2562,plain,
( v1_funct_2(k4_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),k1_lopclset(sK0_skl))
| ~ l1_pre_topc(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(forward_demodulation,[status(thm)],[f2289,f2561]) ).
fof(f2563,plain,
( v1_funct_2(k4_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))
| ~ l1_pre_topc(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(forward_demodulation,[status(thm)],[f2289,f2562]) ).
fof(f2564,plain,
( v1_funct_2(k4_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))
| ~ l1_pre_topc(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f2563,f99]) ).
fof(f2565,plain,
( m2_relset_1(k4_lopclset(sK0_skl),k2_zfmisc_1(k1_lopclset(sK0_skl),k1_lopclset(sK0_skl)),k1_lopclset(sK0_skl))
| ~ l1_pre_topc(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f293,f100]) ).
fof(f2566,plain,
( m2_relset_1(k4_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),k1_lopclset(sK0_skl)),k1_lopclset(sK0_skl))
| ~ l1_pre_topc(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(forward_demodulation,[status(thm)],[f2289,f2565]) ).
fof(f2567,plain,
( m2_relset_1(k4_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),k1_lopclset(sK0_skl))
| ~ l1_pre_topc(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(forward_demodulation,[status(thm)],[f2289,f2566]) ).
fof(f2568,plain,
( m2_relset_1(k4_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))
| ~ l1_pre_topc(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(forward_demodulation,[status(thm)],[f2289,f2567]) ).
fof(f2569,plain,
( m2_relset_1(k4_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))
| ~ l1_pre_topc(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f2568,f99]) ).
fof(f2570,plain,
v1_funct_1(k4_lopclset(sK0_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f2559,f101]) ).
fof(f2571,plain,
v1_funct_2(k4_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f2564,f101]) ).
fof(f2573,plain,
! [X0] :
( v3_lattices(g3_lattices(a_1_0_lopclset(sK0_skl),k4_lopclset(sK0_skl),X0))
| ~ m1_relset_1(X0,k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))
| ~ v1_funct_2(X0,k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))
| ~ v1_funct_1(X0)
| ~ m1_relset_1(k4_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))
| ~ v1_funct_1(k4_lopclset(sK0_skl)) ),
inference(resolution,[status(thm)],[f2571,f288]) ).
fof(f2576,plain,
! [X0,X1,X2,X3] :
( a_1_0_lopclset(sK0_skl) = X1
| g3_lattices(a_1_0_lopclset(sK0_skl),k4_lopclset(sK0_skl),X0) != g3_lattices(X1,X2,X3)
| ~ m1_relset_1(X0,k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))
| ~ v1_funct_2(X0,k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))
| ~ v1_funct_1(X0)
| ~ m1_relset_1(k4_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))
| ~ v1_funct_1(k4_lopclset(sK0_skl)) ),
inference(resolution,[status(thm)],[f2571,f278]) ).
fof(f2581,plain,
! [X0] :
( v3_lattices(g3_lattices(a_1_0_lopclset(sK0_skl),k4_lopclset(sK0_skl),X0))
| ~ m1_relset_1(X0,k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))
| ~ v1_funct_2(X0,k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))
| ~ v1_funct_1(X0)
| ~ m1_relset_1(k4_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f2573,f2570]) ).
fof(f2584,plain,
! [X0,X1,X2,X3] :
( a_1_0_lopclset(sK0_skl) = X1
| g3_lattices(a_1_0_lopclset(sK0_skl),k4_lopclset(sK0_skl),X0) != g3_lattices(X1,X2,X3)
| ~ m1_relset_1(X0,k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))
| ~ v1_funct_2(X0,k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))
| ~ v1_funct_1(X0)
| ~ m1_relset_1(k4_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f2576,f2570]) ).
fof(f2588,plain,
m2_relset_1(k4_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f2569,f101]) ).
fof(f2590,plain,
m1_relset_1(k4_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl)),
inference(resolution,[status(thm)],[f2588,f137]) ).
fof(f2643,plain,
( v1_funct_1(k5_lopclset(sK0_skl))
| ~ l1_pre_topc(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f295,f100]) ).
fof(f2644,plain,
( v1_funct_1(k5_lopclset(sK0_skl))
| ~ l1_pre_topc(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f2643,f99]) ).
fof(f2645,plain,
( v1_funct_2(k5_lopclset(sK0_skl),k2_zfmisc_1(k1_lopclset(sK0_skl),k1_lopclset(sK0_skl)),k1_lopclset(sK0_skl))
| ~ l1_pre_topc(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f296,f100]) ).
fof(f2646,plain,
( v1_funct_2(k5_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),k1_lopclset(sK0_skl)),k1_lopclset(sK0_skl))
| ~ l1_pre_topc(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(forward_demodulation,[status(thm)],[f2289,f2645]) ).
fof(f2647,plain,
( v1_funct_2(k5_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),k1_lopclset(sK0_skl))
| ~ l1_pre_topc(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(forward_demodulation,[status(thm)],[f2289,f2646]) ).
fof(f2648,plain,
( v1_funct_2(k5_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))
| ~ l1_pre_topc(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(forward_demodulation,[status(thm)],[f2289,f2647]) ).
fof(f2649,plain,
( v1_funct_2(k5_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))
| ~ l1_pre_topc(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f2648,f99]) ).
fof(f2650,plain,
( m2_relset_1(k5_lopclset(sK0_skl),k2_zfmisc_1(k1_lopclset(sK0_skl),k1_lopclset(sK0_skl)),k1_lopclset(sK0_skl))
| ~ l1_pre_topc(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f297,f100]) ).
fof(f2651,plain,
( m2_relset_1(k5_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),k1_lopclset(sK0_skl)),k1_lopclset(sK0_skl))
| ~ l1_pre_topc(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(forward_demodulation,[status(thm)],[f2289,f2650]) ).
fof(f2652,plain,
( m2_relset_1(k5_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),k1_lopclset(sK0_skl))
| ~ l1_pre_topc(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(forward_demodulation,[status(thm)],[f2289,f2651]) ).
fof(f2653,plain,
( m2_relset_1(k5_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))
| ~ l1_pre_topc(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(forward_demodulation,[status(thm)],[f2289,f2652]) ).
fof(f2654,plain,
( m2_relset_1(k5_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))
| ~ l1_pre_topc(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f2653,f99]) ).
fof(f2655,plain,
v1_funct_1(k5_lopclset(sK0_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f2644,f101]) ).
fof(f2660,plain,
v1_funct_2(k5_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f2649,f101]) ).
fof(f2681,plain,
m2_relset_1(k5_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f2654,f101]) ).
fof(f2683,plain,
m1_relset_1(k5_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl)),
inference(resolution,[status(thm)],[f2681,f137]) ).
fof(f2889,plain,
( ~ v4_pre_topc(k1_xboole_0,sK0_skl)
| ~ v3_pre_topc(k1_xboole_0,sK0_skl)
| r2_hidden(k1_xboole_0,a_1_0_lopclset(sK0_skl))
| ~ l1_pre_topc(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f403,f703]) ).
fof(f2900,plain,
( ~ v4_pre_topc(k1_xboole_0,sK0_skl)
| ~ v3_pre_topc(k1_xboole_0,sK0_skl)
| r2_hidden(k1_xboole_0,a_1_0_lopclset(sK0_skl))
| ~ l1_pre_topc(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f2889,f99]) ).
fof(f2983,plain,
! [X0,X1,X2,X3] :
( a_1_0_lopclset(sK0_skl) = X1
| g3_lattices(a_1_0_lopclset(sK0_skl),k4_lopclset(sK0_skl),X0) != g3_lattices(X1,X2,X3)
| ~ m1_relset_1(X0,k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))
| ~ v1_funct_2(X0,k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))
| ~ v1_funct_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f2584,f2590]) ).
fof(f2986,plain,
! [X0] :
( v3_lattices(g3_lattices(a_1_0_lopclset(sK0_skl),k4_lopclset(sK0_skl),X0))
| ~ m1_relset_1(X0,k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))
| ~ v1_funct_2(X0,k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))
| ~ v1_funct_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f2581,f2590]) ).
fof(f3087,plain,
! [X0,X1,X2] :
( m1_subset_1(X2,X0)
| ~ m2_subset_1(X2,X1,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(X1))
| v1_xboole_0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f372,f2238]) ).
fof(f3144,plain,
( m1_subset_1(k1_lopclset(sK0_skl),k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(sK0_skl))))
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f375,f101]) ).
fof(f3145,plain,
( m1_subset_1(a_1_0_lopclset(sK0_skl),k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(sK0_skl))))
| v3_struct_0(sK0_skl) ),
inference(forward_demodulation,[status(thm)],[f2289,f3144]) ).
fof(f3146,plain,
m1_subset_1(a_1_0_lopclset(sK0_skl),k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(sK0_skl)))),
inference(forward_subsumption_resolution,[status(thm)],[f3145,f99]) ).
fof(f3148,plain,
! [X0] :
( m1_subset_1(X0,a_1_0_lopclset(sK0_skl))
| ~ m2_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0_skl)),a_1_0_lopclset(sK0_skl))
| v1_xboole_0(a_1_0_lopclset(sK0_skl)) ),
inference(resolution,[status(thm)],[f3146,f3087]) ).
fof(f3241,plain,
( ~ v1_xboole_0(a_1_0_lopclset(sK0_skl))
| ~ l1_pre_topc(sK0_skl)
| ~ v2_pre_topc(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(paramodulation,[status(thm)],[f2289,f392]) ).
fof(f3242,plain,
( ~ v1_xboole_0(a_1_0_lopclset(sK0_skl))
| ~ l1_pre_topc(sK0_skl)
| ~ v2_pre_topc(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f3241,f99]) ).
fof(f3243,plain,
( k6_lopclset(sK0_skl) = g3_lattices(k1_lopclset(sK0_skl),k4_lopclset(sK0_skl),k5_lopclset(sK0_skl))
| ~ l1_pre_topc(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f400,f100]) ).
fof(f3244,plain,
( k6_lopclset(sK0_skl) = g3_lattices(a_1_0_lopclset(sK0_skl),k4_lopclset(sK0_skl),k5_lopclset(sK0_skl))
| ~ l1_pre_topc(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(forward_demodulation,[status(thm)],[f2289,f3243]) ).
fof(f3245,plain,
( k6_lopclset(sK0_skl) = g3_lattices(a_1_0_lopclset(sK0_skl),k4_lopclset(sK0_skl),k5_lopclset(sK0_skl))
| ~ l1_pre_topc(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f3244,f99]) ).
fof(f3251,plain,
( ~ v1_xboole_0(a_1_0_lopclset(sK0_skl))
| ~ l1_pre_topc(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f3242,f100]) ).
fof(f3252,plain,
k6_lopclset(sK0_skl) = g3_lattices(a_1_0_lopclset(sK0_skl),k4_lopclset(sK0_skl),k5_lopclset(sK0_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f3245,f101]) ).
fof(f3269,plain,
( m2_subset_1(k1_pre_topc(sK0_skl),k1_zfmisc_1(u1_struct_0(sK0_skl)),k1_lopclset(sK0_skl))
| ~ l1_pre_topc(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f402,f100]) ).
fof(f3270,plain,
( m2_subset_1(k1_xboole_0,k1_zfmisc_1(u1_struct_0(sK0_skl)),k1_lopclset(sK0_skl))
| ~ l1_pre_topc(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(forward_demodulation,[status(thm)],[f640,f3269]) ).
fof(f3271,plain,
( m2_subset_1(k1_xboole_0,k1_zfmisc_1(u1_struct_0(sK0_skl)),a_1_0_lopclset(sK0_skl))
| ~ l1_pre_topc(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(forward_demodulation,[status(thm)],[f2289,f3270]) ).
fof(f3272,plain,
( m2_subset_1(k1_xboole_0,k1_zfmisc_1(u1_struct_0(sK0_skl)),a_1_0_lopclset(sK0_skl))
| ~ l1_pre_topc(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f3271,f99]) ).
fof(f3318,plain,
m2_subset_1(k1_xboole_0,k1_zfmisc_1(u1_struct_0(sK0_skl)),a_1_0_lopclset(sK0_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f3272,f101]) ).
fof(f3480,plain,
( ~ v4_pre_topc(k1_xboole_0,sK0_skl)
| ~ v3_pre_topc(k1_xboole_0,sK0_skl)
| r2_hidden(k1_xboole_0,a_1_0_lopclset(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f2900,f101]) ).
fof(f3787,plain,
! [X0,X1,X2] :
( a_1_0_lopclset(sK0_skl) = X0
| g3_lattices(a_1_0_lopclset(sK0_skl),k4_lopclset(sK0_skl),k5_lopclset(sK0_skl)) != g3_lattices(X0,X1,X2)
| ~ m1_relset_1(k5_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))
| ~ v1_funct_1(k5_lopclset(sK0_skl)) ),
inference(resolution,[status(thm)],[f2983,f2660]) ).
fof(f3790,plain,
! [X0,X1,X2] :
( a_1_0_lopclset(sK0_skl) = X0
| k6_lopclset(sK0_skl) != g3_lattices(X0,X1,X2)
| ~ m1_relset_1(k5_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))
| ~ v1_funct_1(k5_lopclset(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f3252,f3787]) ).
fof(f3791,plain,
! [X0,X1,X2] :
( a_1_0_lopclset(sK0_skl) = X0
| k6_lopclset(sK0_skl) != g3_lattices(X0,X1,X2)
| ~ m1_relset_1(k5_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f3790,f2655]) ).
fof(f3923,plain,
( v3_lattices(g3_lattices(a_1_0_lopclset(sK0_skl),k4_lopclset(sK0_skl),k5_lopclset(sK0_skl)))
| ~ m1_relset_1(k5_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))
| ~ v1_funct_1(k5_lopclset(sK0_skl)) ),
inference(resolution,[status(thm)],[f2986,f2660]) ).
fof(f3926,plain,
( v3_lattices(k6_lopclset(sK0_skl))
| ~ m1_relset_1(k5_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))
| ~ v1_funct_1(k5_lopclset(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f3252,f3923]) ).
fof(f3927,plain,
( v3_lattices(k6_lopclset(sK0_skl))
| ~ m1_relset_1(k5_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f3926,f2655]) ).
fof(f4136,plain,
( m1_subset_1(k1_xboole_0,a_1_0_lopclset(sK0_skl))
| v1_xboole_0(a_1_0_lopclset(sK0_skl)) ),
inference(resolution,[status(thm)],[f3148,f3318]) ).
fof(f4276,plain,
( r2_hidden(k1_xboole_0,a_1_0_lopclset(sK0_skl))
| v1_xboole_0(a_1_0_lopclset(sK0_skl))
| v1_xboole_0(a_1_0_lopclset(sK0_skl)) ),
inference(resolution,[status(thm)],[f4136,f339]) ).
fof(f4294,plain,
( r2_hidden(k1_xboole_0,a_1_0_lopclset(sK0_skl))
| v1_xboole_0(a_1_0_lopclset(sK0_skl)) ),
inference(duplicate_literals_removal,[status(thm)],[f4276]) ).
fof(f4295,plain,
( v4_pre_topc(sK21_skl(k1_xboole_0,sK0_skl),sK0_skl)
| ~ l1_pre_topc(sK0_skl)
| v3_struct_0(sK0_skl)
| v1_xboole_0(a_1_0_lopclset(sK0_skl)) ),
inference(resolution,[status(thm)],[f4294,f360]) ).
fof(f4296,plain,
( v3_pre_topc(sK21_skl(k1_xboole_0,sK0_skl),sK0_skl)
| ~ l1_pre_topc(sK0_skl)
| v3_struct_0(sK0_skl)
| v1_xboole_0(a_1_0_lopclset(sK0_skl)) ),
inference(resolution,[status(thm)],[f4294,f359]) ).
fof(f4297,plain,
( k1_xboole_0 = sK21_skl(k1_xboole_0,sK0_skl)
| ~ l1_pre_topc(sK0_skl)
| v3_struct_0(sK0_skl)
| v1_xboole_0(a_1_0_lopclset(sK0_skl)) ),
inference(resolution,[status(thm)],[f4294,f358]) ).
fof(f4304,plain,
( v4_pre_topc(sK21_skl(k1_xboole_0,sK0_skl),sK0_skl)
| ~ l1_pre_topc(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f4295,f3251]) ).
fof(f4305,plain,
( v3_pre_topc(sK21_skl(k1_xboole_0,sK0_skl),sK0_skl)
| ~ l1_pre_topc(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f4296,f3251]) ).
fof(f4306,plain,
( k1_xboole_0 = sK21_skl(k1_xboole_0,sK0_skl)
| ~ l1_pre_topc(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f4297,f3251]) ).
fof(f4426,plain,
( k1_xboole_0 = sK21_skl(k1_xboole_0,sK0_skl)
| ~ l1_pre_topc(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f4306,f99]) ).
fof(f4427,plain,
k1_xboole_0 = sK21_skl(k1_xboole_0,sK0_skl),
inference(resolution,[status(thm)],[f4426,f101]) ).
fof(f4434,plain,
( v4_pre_topc(k1_xboole_0,sK0_skl)
| ~ l1_pre_topc(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(forward_demodulation,[status(thm)],[f4427,f4304]) ).
fof(f4435,plain,
( v4_pre_topc(k1_xboole_0,sK0_skl)
| ~ l1_pre_topc(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f4434,f99]) ).
fof(f4436,plain,
v4_pre_topc(k1_xboole_0,sK0_skl),
inference(resolution,[status(thm)],[f4435,f101]) ).
fof(f4437,plain,
( ~ v3_pre_topc(k1_xboole_0,sK0_skl)
| r2_hidden(k1_xboole_0,a_1_0_lopclset(sK0_skl)) ),
inference(backward_subsumption_resolution,[status(thm)],[f3480,f4436]) ).
fof(f4526,plain,
( v3_pre_topc(k1_xboole_0,sK0_skl)
| ~ l1_pre_topc(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(forward_demodulation,[status(thm)],[f4427,f4305]) ).
fof(f4527,plain,
( v3_pre_topc(k1_xboole_0,sK0_skl)
| ~ l1_pre_topc(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f4526,f99]) ).
fof(f4528,plain,
v3_pre_topc(k1_xboole_0,sK0_skl),
inference(resolution,[status(thm)],[f4527,f101]) ).
fof(f4529,plain,
r2_hidden(k1_xboole_0,a_1_0_lopclset(sK0_skl)),
inference(backward_subsumption_resolution,[status(thm)],[f4437,f4528]) ).
fof(f4536,plain,
m1_subset_1(k1_xboole_0,a_1_0_lopclset(sK0_skl)),
inference(resolution,[status(thm)],[f4529,f270]) ).
fof(f11821,plain,
! [X0,X1,X2] :
( a_1_0_lopclset(sK0_skl) = X0
| k6_lopclset(sK0_skl) != g3_lattices(X0,X1,X2) ),
inference(forward_subsumption_resolution,[status(thm)],[f3791,f2683]) ).
fof(f12544,plain,
k6_lopclset(sK0_skl) = g3_lattices(u1_struct_0(k6_lopclset(sK0_skl)),u2_lattices(k6_lopclset(sK0_skl)),u1_lattices(k6_lopclset(sK0_skl))),
inference(backward_subsumption_resolution,[status(thm)],[f558,f12545]) ).
fof(f12545,plain,
v3_lattices(k6_lopclset(sK0_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f3927,f2683]) ).
fof(f12548,plain,
a_1_0_lopclset(sK0_skl) = u1_struct_0(k6_lopclset(sK0_skl)),
inference(resolution,[status(thm)],[f12544,f11821]) ).
fof(f12653,plain,
~ m1_subset_1(k1_xboole_0,a_1_0_lopclset(sK0_skl)),
inference(backward_demodulation,[status(thm)],[f12548,f710]) ).
fof(f12660,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f12653,f4536]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LAT287+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.20/0.45 % Computer : n019.cluster.edu
% 0.20/0.45 % Model : x86_64 x86_64
% 0.20/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/0.45 % Memory : 8046.5625MB
% 0.20/0.45 % OS : Linux 6.8.0-71-generic
% 0.20/0.45 % CPULimit : 300
% 0.20/0.45 % WCLimit : 300
% 0.20/0.45 % DateTime : Sun Sep 20 23:26:20 UTC 2026
% 0.20/0.46 % CPUTime :
% 0.20/0.48 % Drodi V4.1.1
% 6.55/1.40 % Refutation found
% 6.55/1.40 % SZS status Theorem for theBenchmark: Theorem is valid
% 6.55/1.40 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 6.55/1.45 % Elapsed time: 0.985440 seconds
% 6.55/1.45 % CPU time: 7.361159 seconds
% 6.55/1.45 % Total memory used: 163.007 MB
% 6.55/1.45 % Net memory used: 159.510 MB
%------------------------------------------------------------------------------