%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LAT286+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n001.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 0.19s 5.63s
% Output : CNFRefutation 0.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 48
% Syntax : Number of formulae : 198 ( 26 unt; 29 def)
% Number of atoms : 607 ( 31 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 672 ( 263 ~; 294 |; 66 &)
% ( 33 <=>; 16 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 49 ( 47 usr; 30 prp; 0-3 aty)
% Number of functors : 16 ( 16 usr; 2 con; 0-3 aty)
% Number of variables : 155 ( 152 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [A] :
( ( l1_pre_topc(A)
& v2_pre_topc(A)
& ~ v3_struct_0(A) )
=> m1_subset_1(k2_pre_topc(A),u1_struct_0(k6_lopclset(A))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
~ ! [A] :
( ( l1_pre_topc(A)
& v2_pre_topc(A)
& ~ v3_struct_0(A) )
=> m1_subset_1(k2_pre_topc(A),u1_struct_0(k6_lopclset(A))) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f6,axiom,
! [A,B] :
? [C] :
( v1_funct_2(C,A,B)
& v1_funct_1(C)
& v1_relat_1(C)
& m1_relset_1(C,A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
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/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [A,B,C] :
( m2_relset_1(C,A,B)
<=> m1_relset_1(C,A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f51,axiom,
! [A,B,C] :
( ( m1_subset_1(B,k1_zfmisc_1(C))
& r2_hidden(A,B) )
=> m1_subset_1(A,C) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f53,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/sandbox2/benchmark/theBenchmark.p') ).
fof(f54,axiom,
! [A,B] : r1_tarski(A,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f57,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/sandbox2/benchmark/theBenchmark.p') ).
fof(f58,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/sandbox2/benchmark/theBenchmark.p') ).
fof(f59,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/sandbox2/benchmark/theBenchmark.p') ).
fof(f73,axiom,
! [A,B] :
( m1_subset_1(A,B)
=> ( r2_hidden(A,B)
| v1_xboole_0(B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f80,axiom,
! [A] :
? [B] : m1_subset_1(B,A),
file('/export/starexec/sandbox2/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/sandbox2/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/sandbox2/benchmark/theBenchmark.p') ).
fof(f91,axiom,
! [A] :
( v4_finsub_1(k1_zfmisc_1(A))
& v3_finsub_1(k1_zfmisc_1(A))
& v1_finsub_1(k1_zfmisc_1(A))
& ~ v1_xboole_0(k1_zfmisc_1(A)) ),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p') ).
fof(f94,axiom,
! [A,B] :
( m1_subset_1(A,k1_zfmisc_1(B))
<=> r1_tarski(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f96,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/sandbox2/benchmark/theBenchmark.p') ).
fof(f97,axiom,
! [A] :
( ( l1_pre_topc(A)
& v2_pre_topc(A)
& ~ v3_struct_0(A) )
=> m2_subset_1(k2_pre_topc(A),k1_zfmisc_1(u1_struct_0(A)),k1_lopclset(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f98,plain,
? [A] :
( ~ m1_subset_1(k2_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(f99,plain,
( ~ m1_subset_1(k2_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)],[f98]) ).
fof(f100,plain,
~ v3_struct_0(sK0_skl),
inference(cnf_transformation,[status(thm)],[f99]) ).
fof(f101,plain,
v2_pre_topc(sK0_skl),
inference(cnf_transformation,[status(thm)],[f99]) ).
fof(f102,plain,
l1_pre_topc(sK0_skl),
inference(cnf_transformation,[status(thm)],[f99]) ).
fof(f103,plain,
~ m1_subset_1(k2_pre_topc(sK0_skl),u1_struct_0(k6_lopclset(sK0_skl))),
inference(cnf_transformation,[status(thm)],[f99]) ).
fof(f115,plain,
! [A,B] :
( v1_funct_2(sK1_skl(B,A),A,B)
& v1_funct_1(sK1_skl(B,A))
& v1_relat_1(sK1_skl(B,A))
& m1_relset_1(sK1_skl(B,A),A,B) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(C,sK1_skl(B,A))],[f6]) ).
fof(f116,plain,
! [X0,X1] : m1_relset_1(sK1_skl(X0,X1),X1,X0),
inference(cnf_transformation,[status(thm)],[f115]) ).
fof(f118,plain,
! [X0,X1] : v1_funct_1(sK1_skl(X0,X1)),
inference(cnf_transformation,[status(thm)],[f115]) ).
fof(f126,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(f127,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)],[f126]) ).
fof(f136,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(f137,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)],[f136]) ).
fof(f138,plain,
! [X0,X1,X2] :
( m1_relset_1(X0,X1,X2)
| ~ m2_relset_1(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f137]) ).
fof(f263,plain,
! [A,B,C] :
( m1_subset_1(A,C)
| ~ m1_subset_1(B,k1_zfmisc_1(C))
| ~ r2_hidden(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f51]) ).
fof(f264,plain,
! [A,C] :
( m1_subset_1(A,C)
| ! [B] :
( ~ m1_subset_1(B,k1_zfmisc_1(C))
| ~ r2_hidden(A,B) ) ),
inference(miniscoping,[status(thm)],[f263]) ).
fof(f265,plain,
! [X0,X1,X2] :
( m1_subset_1(X0,X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ r2_hidden(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f264]) ).
fof(f269,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)],[f53]) ).
fof(f270,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)],[f269]) ).
fof(f273,plain,
! [A] : r1_tarski(A,A),
inference(miniscoping,[status(thm)],[f54]) ).
fof(f274,plain,
! [X0] : r1_tarski(X0,X0),
inference(cnf_transformation,[status(thm)],[f273]) ).
fof(f279,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)],[f57]) ).
fof(f280,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)],[f279]) ).
fof(f281,plain,
! [X0,X1,X2] :
( l3_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)],[f279]) ).
fof(f282,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)],[f58]) ).
fof(f283,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)],[f282]) ).
fof(f284,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)],[f282]) ).
fof(f285,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)],[f282]) ).
fof(f286,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)],[f59]) ).
fof(f287,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)],[f286]) ).
fof(f288,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)],[f286]) ).
fof(f289,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)],[f286]) ).
fof(f334,plain,
! [A,B] :
( r2_hidden(A,B)
| v1_xboole_0(B)
| ~ m1_subset_1(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f73]) ).
fof(f335,plain,
! [X0,X1] :
( r2_hidden(X0,X1)
| v1_xboole_0(X1)
| ~ m1_subset_1(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f334]) ).
fof(f360,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(f361,plain,
! [X0] : m1_subset_1(sK23_skl(X0),X0),
inference(cnf_transformation,[status(thm)],[f360]) ).
fof(f365,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(f366,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)],[f365]) ).
fof(f367,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)],[f366]) ).
fof(f368,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)],[f367]) ).
fof(f370,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(f371,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)],[f370]) ).
fof(f382,plain,
( ! [A] : v4_finsub_1(k1_zfmisc_1(A))
& ! [A] : v3_finsub_1(k1_zfmisc_1(A))
& ! [A] : v1_finsub_1(k1_zfmisc_1(A))
& ! [A] : ~ v1_xboole_0(k1_zfmisc_1(A)) ),
inference(miniscoping,[status(thm)],[f91]) ).
fof(f383,plain,
! [X0] : ~ v1_xboole_0(k1_zfmisc_1(X0)),
inference(cnf_transformation,[status(thm)],[f382]) ).
fof(f387,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(f388,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)],[f387]) ).
fof(f391,plain,
! [A,B] :
( ( ~ r1_tarski(A,B)
| m1_subset_1(A,k1_zfmisc_1(B)) )
& ( r1_tarski(A,B)
| ~ m1_subset_1(A,k1_zfmisc_1(B)) ) ),
inference(NNF_transformation,[status(thm)],[f94]) ).
fof(f392,plain,
( ! [A,B] :
( ~ r1_tarski(A,B)
| m1_subset_1(A,k1_zfmisc_1(B)) )
& ! [A,B] :
( r1_tarski(A,B)
| ~ m1_subset_1(A,k1_zfmisc_1(B)) ) ),
inference(miniscoping,[status(thm)],[f391]) ).
fof(f394,plain,
! [X0,X1] :
( ~ r1_tarski(X0,X1)
| m1_subset_1(X0,k1_zfmisc_1(X1)) ),
inference(cnf_transformation,[status(thm)],[f392]) ).
fof(f397,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)],[f96]) ).
fof(f398,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)],[f397]) ).
fof(f399,plain,
! [A] :
( m2_subset_1(k2_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)],[f97]) ).
fof(f400,plain,
! [X0] :
( m2_subset_1(k2_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)],[f399]) ).
fof(f446,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k6_lopclset(sK0_skl))))
| ~ r2_hidden(k2_pre_topc(sK0_skl),X0) ),
inference(resolution,[status(thm)],[f265,f103]) ).
fof(f447,plain,
! [X0] :
( v1_xboole_0(X0)
| ~ m1_subset_1(k2_pre_topc(sK0_skl),X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k6_lopclset(sK0_skl)))) ),
inference(resolution,[status(thm)],[f446,f335]) ).
fof(f474,definition,
( sQ9_spl
<=> v1_xboole_0(k1_zfmisc_1(u1_struct_0(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f475,plain,
( ~ sQ9_spl
| v1_xboole_0(k1_zfmisc_1(u1_struct_0(sK0_skl))) ),
inference(component_clause,[status(thm)],[f474]) ).
fof(f521,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)],[f284,f101]) ).
fof(f522,definition,
( sQ11_spl
<=> v3_struct_0(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f523,plain,
( ~ sQ11_spl
| v3_struct_0(sK0_skl) ),
inference(component_clause,[status(thm)],[f522]) ).
fof(f525,definition,
( sQ12_spl
<=> l1_pre_topc(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f527,plain,
( sQ12_spl
| ~ l1_pre_topc(sK0_skl) ),
inference(component_clause,[status(thm)],[f525]) ).
fof(f528,definition,
( sQ13_spl
<=> v1_funct_2(k4_lopclset(sK0_skl),k2_zfmisc_1(k1_lopclset(sK0_skl),k1_lopclset(sK0_skl)),k1_lopclset(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f531,plain,
( sQ13_spl
| ~ sQ12_spl
| sQ11_spl ),
inference(split_clause,[status(thm)],[f521,f522,f525,f528]) ).
fof(f538,definition,
( sQ15_spl
<=> v1_funct_1(k4_lopclset(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f540,plain,
( sQ15_spl
| ~ v1_funct_1(k4_lopclset(sK0_skl)) ),
inference(component_clause,[status(thm)],[f538]) ).
fof(f541,definition,
( sQ16_spl
<=> m1_relset_1(k4_lopclset(sK0_skl),k2_zfmisc_1(k1_lopclset(sK0_skl),k1_lopclset(sK0_skl)),k1_lopclset(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f543,plain,
( sQ16_spl
| ~ m1_relset_1(k4_lopclset(sK0_skl),k2_zfmisc_1(k1_lopclset(sK0_skl),k1_lopclset(sK0_skl)),k1_lopclset(sK0_skl)) ),
inference(component_clause,[status(thm)],[f541]) ).
fof(f549,plain,
( sQ12_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f527,f102]) ).
fof(f550,plain,
sQ12_spl,
inference(contradiction_clause,[status(thm)],[f549]) ).
fof(f551,plain,
( ~ sQ11_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f523,f100]) ).
fof(f552,plain,
~ sQ11_spl,
inference(contradiction_clause,[status(thm)],[f551]) ).
fof(f560,plain,
( sQ16_spl
| ~ m2_relset_1(k4_lopclset(sK0_skl),k2_zfmisc_1(k1_lopclset(sK0_skl),k1_lopclset(sK0_skl)),k1_lopclset(sK0_skl)) ),
inference(resolution,[status(thm)],[f543,f138]) ).
fof(f602,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)],[f285,f101]) ).
fof(f603,definition,
( sQ25_spl
<=> m2_relset_1(k4_lopclset(sK0_skl),k2_zfmisc_1(k1_lopclset(sK0_skl),k1_lopclset(sK0_skl)),k1_lopclset(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f604,plain,
( ~ sQ25_spl
| m2_relset_1(k4_lopclset(sK0_skl),k2_zfmisc_1(k1_lopclset(sK0_skl),k1_lopclset(sK0_skl)),k1_lopclset(sK0_skl)) ),
inference(component_clause,[status(thm)],[f603]) ).
fof(f606,plain,
( sQ25_spl
| ~ sQ12_spl
| sQ11_spl ),
inference(split_clause,[status(thm)],[f602,f522,f525,f603]) ).
fof(f607,plain,
( ~ sQ25_spl
| sQ16_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f604,f560]) ).
fof(f608,plain,
( ~ sQ25_spl
| sQ16_spl ),
inference(contradiction_clause,[status(thm)],[f607]) ).
fof(f609,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)],[f288,f101]) ).
fof(f610,definition,
( sQ26_spl
<=> v1_funct_2(k5_lopclset(sK0_skl),k2_zfmisc_1(k1_lopclset(sK0_skl),k1_lopclset(sK0_skl)),k1_lopclset(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f613,plain,
( sQ26_spl
| ~ sQ12_spl
| sQ11_spl ),
inference(split_clause,[status(thm)],[f609,f522,f525,f610]) ).
fof(f614,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)],[f289,f101]) ).
fof(f615,definition,
( sQ27_spl
<=> m2_relset_1(k5_lopclset(sK0_skl),k2_zfmisc_1(k1_lopclset(sK0_skl),k1_lopclset(sK0_skl)),k1_lopclset(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f616,plain,
( ~ sQ27_spl
| m2_relset_1(k5_lopclset(sK0_skl),k2_zfmisc_1(k1_lopclset(sK0_skl),k1_lopclset(sK0_skl)),k1_lopclset(sK0_skl)) ),
inference(component_clause,[status(thm)],[f615]) ).
fof(f618,plain,
( sQ27_spl
| ~ sQ12_spl
| sQ11_spl ),
inference(split_clause,[status(thm)],[f614,f522,f525,f615]) ).
fof(f619,plain,
( sQ15_spl
| ~ l1_pre_topc(sK0_skl)
| ~ v2_pre_topc(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f540,f283]) ).
fof(f620,definition,
( sQ28_spl
<=> v2_pre_topc(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f622,plain,
( sQ28_spl
| ~ v2_pre_topc(sK0_skl) ),
inference(component_clause,[status(thm)],[f620]) ).
fof(f623,plain,
( sQ15_spl
| ~ sQ12_spl
| ~ sQ28_spl
| sQ11_spl ),
inference(split_clause,[status(thm)],[f619,f522,f620,f525,f538]) ).
fof(f624,plain,
( sQ28_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f622,f101]) ).
fof(f625,plain,
sQ28_spl,
inference(contradiction_clause,[status(thm)],[f624]) ).
fof(f631,definition,
( sQ30_spl
<=> v1_funct_1(k5_lopclset(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f633,plain,
( sQ30_spl
| ~ v1_funct_1(k5_lopclset(sK0_skl)) ),
inference(component_clause,[status(thm)],[f631]) ).
fof(f634,definition,
( sQ31_spl
<=> m1_relset_1(k5_lopclset(sK0_skl),k2_zfmisc_1(k1_lopclset(sK0_skl),k1_lopclset(sK0_skl)),k1_lopclset(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f636,plain,
( sQ31_spl
| ~ m1_relset_1(k5_lopclset(sK0_skl),k2_zfmisc_1(k1_lopclset(sK0_skl),k1_lopclset(sK0_skl)),k1_lopclset(sK0_skl)) ),
inference(component_clause,[status(thm)],[f634]) ).
fof(f642,plain,
( sQ30_spl
| ~ l1_pre_topc(sK0_skl)
| ~ v2_pre_topc(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f633,f287]) ).
fof(f643,plain,
( sQ30_spl
| ~ sQ12_spl
| ~ sQ28_spl
| sQ11_spl ),
inference(split_clause,[status(thm)],[f642,f522,f620,f525,f631]) ).
fof(f656,definition,
( sQ35_spl
<=> v1_funct_1(sK1_skl(k1_lopclset(sK0_skl),k2_zfmisc_1(k1_lopclset(sK0_skl),k1_lopclset(sK0_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f658,plain,
( sQ35_spl
| ~ v1_funct_1(sK1_skl(k1_lopclset(sK0_skl),k2_zfmisc_1(k1_lopclset(sK0_skl),k1_lopclset(sK0_skl)))) ),
inference(component_clause,[status(thm)],[f656]) ).
fof(f659,definition,
( sQ36_spl
<=> m1_relset_1(sK1_skl(k1_lopclset(sK0_skl),k2_zfmisc_1(k1_lopclset(sK0_skl),k1_lopclset(sK0_skl))),k2_zfmisc_1(k1_lopclset(sK0_skl),k1_lopclset(sK0_skl)),k1_lopclset(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f661,plain,
( sQ36_spl
| ~ m1_relset_1(sK1_skl(k1_lopclset(sK0_skl),k2_zfmisc_1(k1_lopclset(sK0_skl),k1_lopclset(sK0_skl))),k2_zfmisc_1(k1_lopclset(sK0_skl),k1_lopclset(sK0_skl)),k1_lopclset(sK0_skl)) ),
inference(component_clause,[status(thm)],[f659]) ).
fof(f687,definition,
! [X0] :
( sQ40_spl
<=> ~ m1_subset_1(X0,k1_xboole_0) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f688,plain,
! [X0] :
( ~ sQ40_spl
| ~ m1_subset_1(X0,k1_xboole_0) ),
inference(component_clause,[status(thm)],[f687]) ).
fof(f694,definition,
( sQ42_spl
<=> v1_xboole_0(k1_zfmisc_1(k1_xboole_0)) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f695,plain,
( ~ sQ42_spl
| v1_xboole_0(k1_zfmisc_1(k1_xboole_0)) ),
inference(component_clause,[status(thm)],[f694]) ).
fof(f698,plain,
( ~ sQ42_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f695,f383]) ).
fof(f699,plain,
~ sQ42_spl,
inference(contradiction_clause,[status(thm)],[f698]) ).
fof(f700,plain,
( ~ sQ40_spl
| $false ),
inference(resolution,[status(thm)],[f688,f361]) ).
fof(f702,plain,
~ sQ40_spl,
inference(contradiction_clause,[status(thm)],[f700]) ).
fof(f710,plain,
( sQ31_spl
| ~ m2_relset_1(k5_lopclset(sK0_skl),k2_zfmisc_1(k1_lopclset(sK0_skl),k1_lopclset(sK0_skl)),k1_lopclset(sK0_skl)) ),
inference(resolution,[status(thm)],[f636,f138]) ).
fof(f711,plain,
( sQ31_spl
| ~ sQ27_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f710,f616]) ).
fof(f712,plain,
( sQ31_spl
| ~ sQ27_spl ),
inference(contradiction_clause,[status(thm)],[f711]) ).
fof(f730,plain,
( sQ36_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f661,f116]) ).
fof(f731,plain,
sQ36_spl,
inference(contradiction_clause,[status(thm)],[f730]) ).
fof(f732,plain,
( sQ35_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f658,f118]) ).
fof(f733,plain,
sQ35_spl,
inference(contradiction_clause,[status(thm)],[f732]) ).
fof(f810,definition,
( sQ53_spl
<=> v1_xboole_0(k1_lopclset(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f811,plain,
( ~ sQ53_spl
| v1_xboole_0(k1_lopclset(sK0_skl)) ),
inference(component_clause,[status(thm)],[f810]) ).
fof(f825,plain,
( ~ sQ53_spl
| ~ l1_pre_topc(sK0_skl)
| ~ v2_pre_topc(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f811,f388]) ).
fof(f830,plain,
( ~ sQ53_spl
| ~ sQ12_spl
| ~ sQ28_spl
| sQ11_spl ),
inference(split_clause,[status(thm)],[f825,f522,f620,f525,f810]) ).
fof(f1028,definition,
( sQ72_spl
<=> m1_subset_1(sK23_skl(a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition]) ).
fof(f1030,plain,
( sQ72_spl
| ~ m1_subset_1(sK23_skl(a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl)) ),
inference(component_clause,[status(thm)],[f1028]) ).
fof(f1057,plain,
( sQ72_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1030,f361]) ).
fof(f1058,plain,
sQ72_spl,
inference(contradiction_clause,[status(thm)],[f1057]) ).
fof(f1081,definition,
( sQ75_spl
<=> m1_subset_1(sK23_skl(k1_xboole_0),k1_xboole_0) ),
introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).
fof(f1083,plain,
( sQ75_spl
| ~ m1_subset_1(sK23_skl(k1_xboole_0),k1_xboole_0) ),
inference(component_clause,[status(thm)],[f1081]) ).
fof(f1151,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| m1_subset_1(k2_pre_topc(X0),k1_lopclset(X0))
| ~ m1_subset_1(k1_lopclset(X0),k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(X0))))
| v1_xboole_0(k1_lopclset(X0))
| v1_xboole_0(k1_zfmisc_1(u1_struct_0(X0))) ),
inference(resolution,[status(thm)],[f368,f400]) ).
fof(f1153,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| m1_subset_1(k2_pre_topc(X0),k1_lopclset(X0))
| ~ m1_subset_1(k1_lopclset(X0),k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(X0))))
| v1_xboole_0(k1_lopclset(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1151,f383]) ).
fof(f1213,plain,
( sQ75_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1083,f361]) ).
fof(f1214,plain,
sQ75_spl,
inference(contradiction_clause,[status(thm)],[f1213]) ).
fof(f1219,plain,
( ~ l1_pre_topc(sK0_skl)
| v3_struct_0(sK0_skl)
| m1_subset_1(k2_pre_topc(sK0_skl),k1_lopclset(sK0_skl))
| ~ m1_subset_1(k1_lopclset(sK0_skl),k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(sK0_skl))))
| v1_xboole_0(k1_lopclset(sK0_skl)) ),
inference(resolution,[status(thm)],[f1153,f101]) ).
fof(f1220,definition,
( sQ90_spl
<=> m1_subset_1(k1_lopclset(sK0_skl),k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(sK0_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition]) ).
fof(f1222,plain,
( sQ90_spl
| ~ m1_subset_1(k1_lopclset(sK0_skl),k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(sK0_skl)))) ),
inference(component_clause,[status(thm)],[f1220]) ).
fof(f1223,definition,
( sQ91_spl
<=> m1_subset_1(k2_pre_topc(sK0_skl),k1_lopclset(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition]) ).
fof(f1224,plain,
( ~ sQ91_spl
| m1_subset_1(k2_pre_topc(sK0_skl),k1_lopclset(sK0_skl)) ),
inference(component_clause,[status(thm)],[f1223]) ).
fof(f1226,plain,
( ~ sQ12_spl
| sQ11_spl
| sQ91_spl
| ~ sQ90_spl
| sQ53_spl ),
inference(split_clause,[status(thm)],[f1219,f810,f1220,f1223,f522,f525]) ).
fof(f1246,plain,
( ~ sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f475,f383]) ).
fof(f1247,plain,
~ sQ9_spl,
inference(contradiction_clause,[status(thm)],[f1246]) ).
fof(f1375,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)],[f398,f101]) ).
fof(f1376,definition,
( sQ106_spl
<=> k6_lopclset(sK0_skl) = g3_lattices(k1_lopclset(sK0_skl),k4_lopclset(sK0_skl),k5_lopclset(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition]) ).
fof(f1377,plain,
( ~ sQ106_spl
| k6_lopclset(sK0_skl) = g3_lattices(k1_lopclset(sK0_skl),k4_lopclset(sK0_skl),k5_lopclset(sK0_skl)) ),
inference(component_clause,[status(thm)],[f1376]) ).
fof(f1379,plain,
( sQ106_spl
| ~ sQ12_spl
| sQ11_spl ),
inference(split_clause,[status(thm)],[f1375,f522,f525,f1376]) ).
fof(f1463,plain,
( ~ sQ106_spl
| l3_lattices(k6_lopclset(sK0_skl))
| ~ m1_relset_1(k5_lopclset(sK0_skl),k2_zfmisc_1(k1_lopclset(sK0_skl),k1_lopclset(sK0_skl)),k1_lopclset(sK0_skl))
| ~ v1_funct_2(k5_lopclset(sK0_skl),k2_zfmisc_1(k1_lopclset(sK0_skl),k1_lopclset(sK0_skl)),k1_lopclset(sK0_skl))
| ~ v1_funct_1(k5_lopclset(sK0_skl))
| ~ m1_relset_1(k4_lopclset(sK0_skl),k2_zfmisc_1(k1_lopclset(sK0_skl),k1_lopclset(sK0_skl)),k1_lopclset(sK0_skl))
| ~ v1_funct_2(k4_lopclset(sK0_skl),k2_zfmisc_1(k1_lopclset(sK0_skl),k1_lopclset(sK0_skl)),k1_lopclset(sK0_skl))
| ~ v1_funct_1(k4_lopclset(sK0_skl)) ),
inference(paramodulation,[status(thm)],[f1377,f281]) ).
fof(f1464,plain,
( ~ sQ106_spl
| v3_lattices(k6_lopclset(sK0_skl))
| ~ m1_relset_1(k5_lopclset(sK0_skl),k2_zfmisc_1(k1_lopclset(sK0_skl),k1_lopclset(sK0_skl)),k1_lopclset(sK0_skl))
| ~ v1_funct_2(k5_lopclset(sK0_skl),k2_zfmisc_1(k1_lopclset(sK0_skl),k1_lopclset(sK0_skl)),k1_lopclset(sK0_skl))
| ~ v1_funct_1(k5_lopclset(sK0_skl))
| ~ m1_relset_1(k4_lopclset(sK0_skl),k2_zfmisc_1(k1_lopclset(sK0_skl),k1_lopclset(sK0_skl)),k1_lopclset(sK0_skl))
| ~ v1_funct_2(k4_lopclset(sK0_skl),k2_zfmisc_1(k1_lopclset(sK0_skl),k1_lopclset(sK0_skl)),k1_lopclset(sK0_skl))
| ~ v1_funct_1(k4_lopclset(sK0_skl)) ),
inference(paramodulation,[status(thm)],[f1377,f280]) ).
fof(f1466,plain,
! [X0,X1,X2] :
( ~ sQ106_spl
| k1_lopclset(sK0_skl) = X0
| k6_lopclset(sK0_skl) != g3_lattices(X0,X1,X2)
| ~ m1_relset_1(k5_lopclset(sK0_skl),k2_zfmisc_1(k1_lopclset(sK0_skl),k1_lopclset(sK0_skl)),k1_lopclset(sK0_skl))
| ~ v1_funct_2(k5_lopclset(sK0_skl),k2_zfmisc_1(k1_lopclset(sK0_skl),k1_lopclset(sK0_skl)),k1_lopclset(sK0_skl))
| ~ v1_funct_1(k5_lopclset(sK0_skl))
| ~ m1_relset_1(k4_lopclset(sK0_skl),k2_zfmisc_1(k1_lopclset(sK0_skl),k1_lopclset(sK0_skl)),k1_lopclset(sK0_skl))
| ~ v1_funct_2(k4_lopclset(sK0_skl),k2_zfmisc_1(k1_lopclset(sK0_skl),k1_lopclset(sK0_skl)),k1_lopclset(sK0_skl))
| ~ v1_funct_1(k4_lopclset(sK0_skl)) ),
inference(paramodulation,[status(thm)],[f1377,f270]) ).
fof(f1468,definition,
( sQ127_spl
<=> l3_lattices(k6_lopclset(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ127_spl])],[split_symbol_definition]) ).
fof(f1471,plain,
( ~ sQ106_spl
| sQ127_spl
| ~ sQ31_spl
| ~ sQ26_spl
| ~ sQ30_spl
| ~ sQ16_spl
| ~ sQ13_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f1463,f538,f528,f541,f631,f610,f634,f1468,f1376]) ).
fof(f1472,definition,
( sQ128_spl
<=> v3_lattices(k6_lopclset(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ128_spl])],[split_symbol_definition]) ).
fof(f1473,plain,
( ~ sQ128_spl
| v3_lattices(k6_lopclset(sK0_skl)) ),
inference(component_clause,[status(thm)],[f1472]) ).
fof(f1475,plain,
( ~ sQ106_spl
| sQ128_spl
| ~ sQ31_spl
| ~ sQ26_spl
| ~ sQ30_spl
| ~ sQ16_spl
| ~ sQ13_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f1464,f538,f528,f541,f631,f610,f634,f1472,f1376]) ).
fof(f1476,definition,
! [X0,X1,X2] :
( sQ129_spl
<=> ( k1_lopclset(sK0_skl) = X0
| k6_lopclset(sK0_skl) != g3_lattices(X0,X1,X2) ) ),
introduced(definition,[new_symbols(definition,[sQ129_spl])],[split_symbol_definition]) ).
fof(f1477,plain,
! [X0,X1,X2] :
( ~ sQ129_spl
| k1_lopclset(sK0_skl) = X0
| k6_lopclset(sK0_skl) != g3_lattices(X0,X1,X2) ),
inference(component_clause,[status(thm)],[f1476]) ).
fof(f1479,plain,
( ~ sQ106_spl
| sQ129_spl
| ~ sQ31_spl
| ~ sQ26_spl
| ~ sQ30_spl
| ~ sQ16_spl
| ~ sQ13_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f1466,f538,f528,f541,f631,f610,f634,f1476,f1376]) ).
fof(f1484,plain,
( ~ sQ128_spl
| 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)))
| ~ l3_lattices(k6_lopclset(sK0_skl)) ),
inference(resolution,[status(thm)],[f1473,f127]) ).
fof(f1485,definition,
( sQ131_spl
<=> 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))) ),
introduced(definition,[new_symbols(definition,[sQ131_spl])],[split_symbol_definition]) ).
fof(f1486,plain,
( ~ sQ131_spl
| 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(component_clause,[status(thm)],[f1485]) ).
fof(f1488,plain,
( ~ sQ128_spl
| sQ131_spl
| ~ sQ127_spl ),
inference(split_clause,[status(thm)],[f1484,f1468,f1485,f1472]) ).
fof(f1629,plain,
( sQ90_spl
| ~ l1_pre_topc(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f1222,f371]) ).
fof(f1632,plain,
( sQ90_spl
| ~ sQ12_spl
| sQ11_spl ),
inference(split_clause,[status(thm)],[f1629,f522,f525,f1220]) ).
fof(f1643,definition,
( sQ151_spl
<=> k6_lopclset(sK0_skl) = k6_lopclset(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ151_spl])],[split_symbol_definition]) ).
fof(f1645,plain,
( sQ151_spl
| k6_lopclset(sK0_skl) != k6_lopclset(sK0_skl) ),
inference(component_clause,[status(thm)],[f1643]) ).
fof(f1664,plain,
( sQ151_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f1645]) ).
fof(f1665,plain,
sQ151_spl,
inference(contradiction_clause,[status(thm)],[f1664]) ).
fof(f1710,plain,
( ~ sQ91_spl
| v1_xboole_0(k1_lopclset(sK0_skl))
| ~ m1_subset_1(k1_lopclset(sK0_skl),k1_zfmisc_1(u1_struct_0(k6_lopclset(sK0_skl)))) ),
inference(resolution,[status(thm)],[f447,f1224]) ).
fof(f1715,definition,
( sQ157_spl
<=> m1_subset_1(k1_lopclset(sK0_skl),k1_zfmisc_1(u1_struct_0(k6_lopclset(sK0_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ157_spl])],[split_symbol_definition]) ).
fof(f1717,plain,
( sQ157_spl
| ~ m1_subset_1(k1_lopclset(sK0_skl),k1_zfmisc_1(u1_struct_0(k6_lopclset(sK0_skl)))) ),
inference(component_clause,[status(thm)],[f1715]) ).
fof(f1718,plain,
( ~ sQ91_spl
| sQ53_spl
| ~ sQ157_spl ),
inference(split_clause,[status(thm)],[f1710,f1715,f810,f1223]) ).
fof(f1729,definition,
( sQ159_spl
<=> v1_xboole_0(k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(sK0_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ159_spl])],[split_symbol_definition]) ).
fof(f1730,plain,
( ~ sQ159_spl
| v1_xboole_0(k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(sK0_skl)))) ),
inference(component_clause,[status(thm)],[f1729]) ).
fof(f1733,plain,
( ~ sQ159_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1730,f383]) ).
fof(f1734,plain,
~ sQ159_spl,
inference(contradiction_clause,[status(thm)],[f1733]) ).
fof(f1761,plain,
( sQ157_spl
| ~ r1_tarski(k1_lopclset(sK0_skl),u1_struct_0(k6_lopclset(sK0_skl))) ),
inference(resolution,[status(thm)],[f1717,f394]) ).
fof(f2679,plain,
( ~ sQ129_spl
| ~ sQ131_spl
| k1_lopclset(sK0_skl) = u1_struct_0(k6_lopclset(sK0_skl)) ),
inference(resolution,[status(thm)],[f1486,f1477]) ).
fof(f2690,plain,
( sQ157_spl
| ~ sQ129_spl
| ~ sQ131_spl
| ~ r1_tarski(k1_lopclset(sK0_skl),k1_lopclset(sK0_skl)) ),
inference(backward_demodulation,[status(thm)],[f2679,f1761]) ).
fof(f2744,plain,
( sQ157_spl
| ~ sQ129_spl
| ~ sQ131_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2690,f274]) ).
fof(f2745,plain,
( sQ157_spl
| ~ sQ129_spl
| ~ sQ131_spl ),
inference(contradiction_clause,[status(thm)],[f2744]) ).
fof(f2746,plain,
$false,
inference(sat_refutation,[status(thm)],[f531,f550,f552,f606,f608,f613,f618,f623,f625,f643,f699,f702,f712,f731,f733,f830,f1058,f1214,f1226,f1247,f1379,f1471,f1475,f1479,f1488,f1632,f1665,f1718,f1734,f2745]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : LAT286+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/5.41 % Computer : n001.cluster.edu
% 0.16/5.41 % Model : x86_64 x86_64
% 0.16/5.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/5.41 % Memory : 8046.5625MB
% 0.16/5.41 % OS : Linux 6.8.0-71-generic
% 0.16/5.42 % CPULimit : 300
% 0.16/5.42 % WCLimit : 300
% 0.16/5.42 % DateTime : Sun Sep 20 23:32:05 UTC 2026
% 0.16/5.42 % CPUTime :
% 0.16/5.43 % Drodi V4.1.1
% 0.19/5.63 % Refutation found
% 0.19/5.63 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.19/5.63 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.19/5.65 % Elapsed time: 0.210777 seconds
% 0.19/5.65 % CPU time: 1.393371 seconds
% 0.19/5.65 % Total memory used: 119.479 MB
% 0.19/5.65 % Net memory used: 117.944 MB
%------------------------------------------------------------------------------