%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LAT337+2 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n026.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:49 PM UTC 2026
% Result : Theorem 198.70s 25.99s
% Output : CNFRefutation 173.78s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 28
% Syntax : Number of formulae : 113 ( 14 unt; 19 def)
% Number of atoms : 606 ( 4 equ)
% Maximal formula atoms : 17 ( 5 avg)
% Number of connectives : 793 ( 300 ~; 325 |; 120 &)
% ( 19 <=>; 29 =>; 0 <=; 0 <~>)
% Maximal formula depth : 20 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 40 ( 38 usr; 20 prp; 0-3 aty)
% Number of functors : 8 ( 8 usr; 3 con; 0-3 aty)
% Number of variables : 74 ( 71 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2328,axiom,
! [A] :
( l3_lattices(A)
=> ( ( v17_lattices(A)
& ~ v3_struct_0(A) )
=> ( v16_lattices(A)
& v15_lattices(A)
& v14_lattices(A)
& v13_lattices(A)
& v11_lattices(A)
& ~ v3_struct_0(A) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2329,axiom,
! [A] :
( l3_lattices(A)
=> ( ( v16_lattices(A)
& v15_lattices(A)
& v11_lattices(A)
& ~ v3_struct_0(A) )
=> ( v17_lattices(A)
& ~ v3_struct_0(A) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2331,axiom,
! [A] :
( l3_lattices(A)
=> ( ( v11_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( v12_lattices(A)
& v10_lattices(A)
& v9_lattices(A)
& v8_lattices(A)
& v7_lattices(A)
& v6_lattices(A)
& v5_lattices(A)
& v4_lattices(A)
& ~ v3_struct_0(A) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2437,axiom,
! [A] :
( l3_lattices(A)
=> ( ( v3_filter_0(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( v12_lattices(A)
& v11_lattices(A)
& v10_lattices(A)
& v9_lattices(A)
& v8_lattices(A)
& v7_lattices(A)
& v6_lattices(A)
& v5_lattices(A)
& v4_lattices(A)
& ~ v3_struct_0(A) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2486,axiom,
! [A] :
( ( l3_lattices(A)
& v17_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> v3_filter_0(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3018,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,u1_struct_0(A))
=> ! [C] :
( m1_subset_1(C,u1_struct_0(A))
=> ( ( r3_lattices(A,B,C)
& v3_filter_0(A) )
=> v3_filter_0(k23_filter_2(A,k22_filter_2(A,B,C))) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3023,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,u1_struct_0(A))
=> ! [C] :
( m1_subset_1(C,u1_struct_0(A))
=> ( r3_lattices(A,B,C)
=> ( k5_lattices(k23_filter_2(A,k22_filter_2(A,B,C))) = B
& k6_lattices(k23_filter_2(A,k22_filter_2(A,B,C))) = C
& v15_lattices(k23_filter_2(A,k22_filter_2(A,B,C))) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3025,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,u1_struct_0(A))
=> ! [C] :
( m1_subset_1(C,u1_struct_0(A))
=> ( ( r3_lattices(A,B,C)
& v12_lattices(A)
& l3_lattices(A)
& v16_lattices(A)
& v15_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( l3_lattices(k23_filter_2(A,k22_filter_2(A,B,C)))
& v16_lattices(k23_filter_2(A,k22_filter_2(A,B,C)))
& v15_lattices(k23_filter_2(A,k22_filter_2(A,B,C)))
& v10_lattices(k23_filter_2(A,k22_filter_2(A,B,C)))
& ~ v3_struct_0(k23_filter_2(A,k22_filter_2(A,B,C))) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3026,conjecture,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,u1_struct_0(A))
=> ! [C] :
( m1_subset_1(C,u1_struct_0(A))
=> ( ( r3_lattices(A,B,C)
& l3_lattices(A)
& v17_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( l3_lattices(k23_filter_2(A,k22_filter_2(A,B,C)))
& v17_lattices(k23_filter_2(A,k22_filter_2(A,B,C)))
& v10_lattices(k23_filter_2(A,k22_filter_2(A,B,C)))
& ~ v3_struct_0(k23_filter_2(A,k22_filter_2(A,B,C))) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3027,negated_conjecture,
~ ! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,u1_struct_0(A))
=> ! [C] :
( m1_subset_1(C,u1_struct_0(A))
=> ( ( r3_lattices(A,B,C)
& l3_lattices(A)
& v17_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( l3_lattices(k23_filter_2(A,k22_filter_2(A,B,C)))
& v17_lattices(k23_filter_2(A,k22_filter_2(A,B,C)))
& v10_lattices(k23_filter_2(A,k22_filter_2(A,B,C)))
& ~ v3_struct_0(k23_filter_2(A,k22_filter_2(A,B,C))) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f3026]) ).
fof(f9723,plain,
! [A] :
( ( v16_lattices(A)
& v15_lattices(A)
& v14_lattices(A)
& v13_lattices(A)
& v11_lattices(A)
& ~ v3_struct_0(A) )
| ~ v17_lattices(A)
| v3_struct_0(A)
| ~ l3_lattices(A) ),
inference(pre_NNF_transformation,[status(thm)],[f2328]) ).
fof(f9725,plain,
! [X0] :
( v11_lattices(X0)
| ~ v17_lattices(X0)
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f9723]) ).
fof(f9728,plain,
! [X0] :
( v15_lattices(X0)
| ~ v17_lattices(X0)
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f9723]) ).
fof(f9729,plain,
! [X0] :
( v16_lattices(X0)
| ~ v17_lattices(X0)
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f9723]) ).
fof(f9730,plain,
! [A] :
( ( v17_lattices(A)
& ~ v3_struct_0(A) )
| ~ v16_lattices(A)
| ~ v15_lattices(A)
| ~ v11_lattices(A)
| v3_struct_0(A)
| ~ l3_lattices(A) ),
inference(pre_NNF_transformation,[status(thm)],[f2329]) ).
fof(f9732,plain,
! [X0] :
( v17_lattices(X0)
| ~ v16_lattices(X0)
| ~ v15_lattices(X0)
| ~ v11_lattices(X0)
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f9730]) ).
fof(f9750,plain,
! [A] :
( ( v12_lattices(A)
& v10_lattices(A)
& v9_lattices(A)
& v8_lattices(A)
& v7_lattices(A)
& v6_lattices(A)
& v5_lattices(A)
& v4_lattices(A)
& ~ v3_struct_0(A) )
| ~ v11_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| ~ l3_lattices(A) ),
inference(pre_NNF_transformation,[status(thm)],[f2331]) ).
fof(f9759,plain,
! [X0] :
( v12_lattices(X0)
| ~ v11_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f9750]) ).
fof(f10053,plain,
! [A] :
( ( v12_lattices(A)
& v11_lattices(A)
& v10_lattices(A)
& v9_lattices(A)
& v8_lattices(A)
& v7_lattices(A)
& v6_lattices(A)
& v5_lattices(A)
& v4_lattices(A)
& ~ v3_struct_0(A) )
| ~ v3_filter_0(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| ~ l3_lattices(A) ),
inference(pre_NNF_transformation,[status(thm)],[f2437]) ).
fof(f10062,plain,
! [X0] :
( v11_lattices(X0)
| ~ v3_filter_0(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f10053]) ).
fof(f10234,plain,
! [A] :
( v3_filter_0(A)
| ~ l3_lattices(A)
| ~ v17_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f2486]) ).
fof(f10235,plain,
! [X0] :
( v3_filter_0(X0)
| ~ l3_lattices(X0)
| ~ v17_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f10234]) ).
fof(f11876,plain,
! [A] :
( ! [B] :
( ! [C] :
( v3_filter_0(k23_filter_2(A,k22_filter_2(A,B,C)))
| ~ r3_lattices(A,B,C)
| ~ v3_filter_0(A)
| ~ m1_subset_1(C,u1_struct_0(A)) )
| ~ m1_subset_1(B,u1_struct_0(A)) )
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f3018]) ).
fof(f11877,plain,
! [X0,X1,X2] :
( v3_filter_0(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
| ~ r3_lattices(X0,X1,X2)
| ~ v3_filter_0(X0)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f11876]) ).
fof(f11887,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( k5_lattices(k23_filter_2(A,k22_filter_2(A,B,C))) = B
& k6_lattices(k23_filter_2(A,k22_filter_2(A,B,C))) = C
& v15_lattices(k23_filter_2(A,k22_filter_2(A,B,C))) )
| ~ r3_lattices(A,B,C)
| ~ m1_subset_1(C,u1_struct_0(A)) )
| ~ m1_subset_1(B,u1_struct_0(A)) )
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f3023]) ).
fof(f11888,plain,
! [X0,X1,X2] :
( v15_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
| ~ r3_lattices(X0,X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f11887]) ).
fof(f11897,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( l3_lattices(k23_filter_2(A,k22_filter_2(A,B,C)))
& v16_lattices(k23_filter_2(A,k22_filter_2(A,B,C)))
& v15_lattices(k23_filter_2(A,k22_filter_2(A,B,C)))
& v10_lattices(k23_filter_2(A,k22_filter_2(A,B,C)))
& ~ v3_struct_0(k23_filter_2(A,k22_filter_2(A,B,C))) )
| ~ r3_lattices(A,B,C)
| ~ v12_lattices(A)
| ~ l3_lattices(A)
| ~ v16_lattices(A)
| ~ v15_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| ~ m1_subset_1(C,u1_struct_0(A)) )
| ~ m1_subset_1(B,u1_struct_0(A)) )
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f3025]) ).
fof(f11898,plain,
! [X0,X1,X2] :
( ~ v3_struct_0(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
| ~ r3_lattices(X0,X1,X2)
| ~ v12_lattices(X0)
| ~ l3_lattices(X0)
| ~ v16_lattices(X0)
| ~ v15_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f11897]) ).
fof(f11899,plain,
! [X0,X1,X2] :
( v10_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
| ~ r3_lattices(X0,X1,X2)
| ~ v12_lattices(X0)
| ~ l3_lattices(X0)
| ~ v16_lattices(X0)
| ~ v15_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f11897]) ).
fof(f11901,plain,
! [X0,X1,X2] :
( v16_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
| ~ r3_lattices(X0,X1,X2)
| ~ v12_lattices(X0)
| ~ l3_lattices(X0)
| ~ v16_lattices(X0)
| ~ v15_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f11897]) ).
fof(f11902,plain,
! [X0,X1,X2] :
( l3_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
| ~ r3_lattices(X0,X1,X2)
| ~ v12_lattices(X0)
| ~ l3_lattices(X0)
| ~ v16_lattices(X0)
| ~ v15_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f11897]) ).
fof(f11903,plain,
? [A] :
( ? [B] :
( ? [C] :
( ( ~ l3_lattices(k23_filter_2(A,k22_filter_2(A,B,C)))
| ~ v17_lattices(k23_filter_2(A,k22_filter_2(A,B,C)))
| ~ v10_lattices(k23_filter_2(A,k22_filter_2(A,B,C)))
| v3_struct_0(k23_filter_2(A,k22_filter_2(A,B,C))) )
& r3_lattices(A,B,C)
& l3_lattices(A)
& v17_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A)
& m1_subset_1(C,u1_struct_0(A)) )
& m1_subset_1(B,u1_struct_0(A)) )
& l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f3027]) ).
fof(f11904,plain,
( ( ~ l3_lattices(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,sK916_skl)))
| ~ v17_lattices(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,sK916_skl)))
| ~ v10_lattices(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,sK916_skl)))
| v3_struct_0(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,sK916_skl))) )
& r3_lattices(sK914_skl,sK915_skl,sK916_skl)
& l3_lattices(sK914_skl)
& v17_lattices(sK914_skl)
& v10_lattices(sK914_skl)
& ~ v3_struct_0(sK914_skl)
& m1_subset_1(sK916_skl,u1_struct_0(sK914_skl))
& m1_subset_1(sK915_skl,u1_struct_0(sK914_skl))
& l3_lattices(sK914_skl)
& v10_lattices(sK914_skl)
& ~ v3_struct_0(sK914_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK914_skl,sK915_skl,sK916_skl]),skolemize(A,sK914_skl),skolemize(B,sK915_skl),skolemize(C,sK916_skl)],[f11903]) ).
fof(f11905,plain,
~ v3_struct_0(sK914_skl),
inference(cnf_transformation,[status(thm)],[f11904]) ).
fof(f11906,plain,
v10_lattices(sK914_skl),
inference(cnf_transformation,[status(thm)],[f11904]) ).
fof(f11907,plain,
l3_lattices(sK914_skl),
inference(cnf_transformation,[status(thm)],[f11904]) ).
fof(f11908,plain,
m1_subset_1(sK915_skl,u1_struct_0(sK914_skl)),
inference(cnf_transformation,[status(thm)],[f11904]) ).
fof(f11909,plain,
m1_subset_1(sK916_skl,u1_struct_0(sK914_skl)),
inference(cnf_transformation,[status(thm)],[f11904]) ).
fof(f11912,plain,
v17_lattices(sK914_skl),
inference(cnf_transformation,[status(thm)],[f11904]) ).
fof(f11914,plain,
r3_lattices(sK914_skl,sK915_skl,sK916_skl),
inference(cnf_transformation,[status(thm)],[f11904]) ).
fof(f11915,plain,
( ~ l3_lattices(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,sK916_skl)))
| ~ v17_lattices(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,sK916_skl)))
| ~ v10_lattices(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,sK916_skl)))
| v3_struct_0(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,sK916_skl))) ),
inference(cnf_transformation,[status(thm)],[f11904]) ).
fof(f13882,definition,
( sQ313_spl
<=> v3_struct_0(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,sK916_skl))) ),
introduced(definition,[new_symbols(definition,[sQ313_spl])],[split_symbol_definition]) ).
fof(f13883,plain,
( ~ sQ313_spl
| v3_struct_0(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,sK916_skl))) ),
inference(component_clause,[status(thm)],[f13882]) ).
fof(f13885,definition,
( sQ314_spl
<=> v10_lattices(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,sK916_skl))) ),
introduced(definition,[new_symbols(definition,[sQ314_spl])],[split_symbol_definition]) ).
fof(f13886,plain,
( ~ sQ314_spl
| v10_lattices(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,sK916_skl))) ),
inference(component_clause,[status(thm)],[f13885]) ).
fof(f13888,definition,
( sQ315_spl
<=> v17_lattices(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,sK916_skl))) ),
introduced(definition,[new_symbols(definition,[sQ315_spl])],[split_symbol_definition]) ).
fof(f13891,definition,
( sQ316_spl
<=> l3_lattices(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,sK916_skl))) ),
introduced(definition,[new_symbols(definition,[sQ316_spl])],[split_symbol_definition]) ).
fof(f13894,plain,
( ~ sQ316_spl
| ~ sQ315_spl
| ~ sQ314_spl
| sQ313_spl ),
inference(split_clause,[status(thm)],[f11915,f13882,f13885,f13888,f13891]) ).
fof(f14804,plain,
! [X0,X1,X2] :
( ~ v3_struct_0(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
| ~ r3_lattices(X0,X1,X2)
| ~ v12_lattices(X0)
| ~ v16_lattices(X0)
| ~ v15_lattices(X0)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f11898]) ).
fof(f14805,plain,
! [X0,X1,X2] :
( v10_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
| ~ r3_lattices(X0,X1,X2)
| ~ v12_lattices(X0)
| ~ v16_lattices(X0)
| ~ v15_lattices(X0)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f11899]) ).
fof(f14807,plain,
! [X0,X1,X2] :
( v16_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
| ~ r3_lattices(X0,X1,X2)
| ~ v12_lattices(X0)
| ~ v16_lattices(X0)
| ~ v15_lattices(X0)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f11901]) ).
fof(f14808,plain,
! [X0,X1,X2] :
( l3_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
| ~ r3_lattices(X0,X1,X2)
| ~ v12_lattices(X0)
| ~ v16_lattices(X0)
| ~ v15_lattices(X0)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f11902]) ).
fof(f14965,definition,
( sQ390_spl
<=> v3_struct_0(sK914_skl) ),
introduced(definition,[new_symbols(definition,[sQ390_spl])],[split_symbol_definition]) ).
fof(f14966,plain,
( ~ sQ390_spl
| v3_struct_0(sK914_skl) ),
inference(component_clause,[status(thm)],[f14965]) ).
fof(f14968,definition,
( sQ391_spl
<=> v10_lattices(sK914_skl) ),
introduced(definition,[new_symbols(definition,[sQ391_spl])],[split_symbol_definition]) ).
fof(f14970,plain,
( sQ391_spl
| ~ v10_lattices(sK914_skl) ),
inference(component_clause,[status(thm)],[f14968]) ).
fof(f14971,definition,
( sQ392_spl
<=> l3_lattices(sK914_skl) ),
introduced(definition,[new_symbols(definition,[sQ392_spl])],[split_symbol_definition]) ).
fof(f14973,plain,
( sQ392_spl
| ~ l3_lattices(sK914_skl) ),
inference(component_clause,[status(thm)],[f14971]) ).
fof(f14985,plain,
( sQ392_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f14973,f11907]) ).
fof(f14986,plain,
sQ392_spl,
inference(contradiction_clause,[status(thm)],[f14985]) ).
fof(f14987,plain,
( sQ391_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f14970,f11906]) ).
fof(f14988,plain,
sQ391_spl,
inference(contradiction_clause,[status(thm)],[f14987]) ).
fof(f14989,plain,
( ~ sQ390_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f14966,f11905]) ).
fof(f14990,plain,
~ sQ390_spl,
inference(contradiction_clause,[status(thm)],[f14989]) ).
fof(f15017,definition,
( sQ401_spl
<=> m1_subset_1(sK915_skl,u1_struct_0(sK914_skl)) ),
introduced(definition,[new_symbols(definition,[sQ401_spl])],[split_symbol_definition]) ).
fof(f15019,plain,
( sQ401_spl
| ~ m1_subset_1(sK915_skl,u1_struct_0(sK914_skl)) ),
inference(component_clause,[status(thm)],[f15017]) ).
fof(f15020,definition,
( sQ402_spl
<=> m1_subset_1(sK916_skl,u1_struct_0(sK914_skl)) ),
introduced(definition,[new_symbols(definition,[sQ402_spl])],[split_symbol_definition]) ).
fof(f15022,plain,
( sQ402_spl
| ~ m1_subset_1(sK916_skl,u1_struct_0(sK914_skl)) ),
inference(component_clause,[status(thm)],[f15020]) ).
fof(f15027,plain,
( sQ402_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f15022,f11909]) ).
fof(f15028,plain,
sQ402_spl,
inference(contradiction_clause,[status(thm)],[f15027]) ).
fof(f15029,plain,
( sQ401_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f15019,f11908]) ).
fof(f15030,plain,
sQ401_spl,
inference(contradiction_clause,[status(thm)],[f15029]) ).
fof(f15041,plain,
( v15_lattices(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,sK916_skl)))
| ~ m1_subset_1(sK916_skl,u1_struct_0(sK914_skl))
| ~ m1_subset_1(sK915_skl,u1_struct_0(sK914_skl))
| ~ l3_lattices(sK914_skl)
| ~ v10_lattices(sK914_skl)
| v3_struct_0(sK914_skl) ),
inference(resolution,[status(thm)],[f11888,f11914]) ).
fof(f15042,definition,
( sQ406_spl
<=> v15_lattices(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,sK916_skl))) ),
introduced(definition,[new_symbols(definition,[sQ406_spl])],[split_symbol_definition]) ).
fof(f15043,plain,
( ~ sQ406_spl
| v15_lattices(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,sK916_skl))) ),
inference(component_clause,[status(thm)],[f15042]) ).
fof(f15045,plain,
( sQ406_spl
| ~ sQ402_spl
| ~ sQ401_spl
| ~ sQ392_spl
| ~ sQ391_spl
| sQ390_spl ),
inference(split_clause,[status(thm)],[f15041,f14965,f14968,f14971,f15017,f15020,f15042]) ).
fof(f15056,plain,
( v3_filter_0(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,sK916_skl)))
| ~ v3_filter_0(sK914_skl)
| ~ m1_subset_1(sK916_skl,u1_struct_0(sK914_skl))
| ~ m1_subset_1(sK915_skl,u1_struct_0(sK914_skl))
| ~ l3_lattices(sK914_skl)
| ~ v10_lattices(sK914_skl)
| v3_struct_0(sK914_skl) ),
inference(resolution,[status(thm)],[f11877,f11914]) ).
fof(f15057,definition,
( sQ409_spl
<=> v3_filter_0(sK914_skl) ),
introduced(definition,[new_symbols(definition,[sQ409_spl])],[split_symbol_definition]) ).
fof(f15060,definition,
( sQ410_spl
<=> v3_filter_0(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,sK916_skl))) ),
introduced(definition,[new_symbols(definition,[sQ410_spl])],[split_symbol_definition]) ).
fof(f15063,plain,
( sQ410_spl
| ~ sQ409_spl
| ~ sQ402_spl
| ~ sQ401_spl
| ~ sQ392_spl
| ~ sQ391_spl
| sQ390_spl ),
inference(split_clause,[status(thm)],[f15056,f14965,f14968,f14971,f15017,f15020,f15057,f15060]) ).
fof(f15064,plain,
( v10_lattices(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,sK916_skl)))
| ~ v12_lattices(sK914_skl)
| ~ v16_lattices(sK914_skl)
| ~ v15_lattices(sK914_skl)
| ~ m1_subset_1(sK916_skl,u1_struct_0(sK914_skl))
| ~ m1_subset_1(sK915_skl,u1_struct_0(sK914_skl))
| ~ l3_lattices(sK914_skl)
| ~ v10_lattices(sK914_skl)
| v3_struct_0(sK914_skl) ),
inference(resolution,[status(thm)],[f14805,f11914]) ).
fof(f15065,definition,
( sQ411_spl
<=> v15_lattices(sK914_skl) ),
introduced(definition,[new_symbols(definition,[sQ411_spl])],[split_symbol_definition]) ).
fof(f15068,definition,
( sQ412_spl
<=> v16_lattices(sK914_skl) ),
introduced(definition,[new_symbols(definition,[sQ412_spl])],[split_symbol_definition]) ).
fof(f15071,definition,
( sQ413_spl
<=> v12_lattices(sK914_skl) ),
introduced(definition,[new_symbols(definition,[sQ413_spl])],[split_symbol_definition]) ).
fof(f15074,plain,
( sQ314_spl
| ~ sQ413_spl
| ~ sQ412_spl
| ~ sQ411_spl
| ~ sQ402_spl
| ~ sQ401_spl
| ~ sQ392_spl
| ~ sQ391_spl
| sQ390_spl ),
inference(split_clause,[status(thm)],[f15064,f14965,f14968,f14971,f15017,f15020,f15065,f15068,f15071,f13885]) ).
fof(f15075,plain,
( v16_lattices(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,sK916_skl)))
| ~ v12_lattices(sK914_skl)
| ~ v16_lattices(sK914_skl)
| ~ v15_lattices(sK914_skl)
| ~ m1_subset_1(sK916_skl,u1_struct_0(sK914_skl))
| ~ m1_subset_1(sK915_skl,u1_struct_0(sK914_skl))
| ~ l3_lattices(sK914_skl)
| ~ v10_lattices(sK914_skl)
| v3_struct_0(sK914_skl) ),
inference(resolution,[status(thm)],[f14807,f11914]) ).
fof(f15076,definition,
( sQ414_spl
<=> v16_lattices(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,sK916_skl))) ),
introduced(definition,[new_symbols(definition,[sQ414_spl])],[split_symbol_definition]) ).
fof(f15079,plain,
( sQ414_spl
| ~ sQ413_spl
| ~ sQ412_spl
| ~ sQ411_spl
| ~ sQ402_spl
| ~ sQ401_spl
| ~ sQ392_spl
| ~ sQ391_spl
| sQ390_spl ),
inference(split_clause,[status(thm)],[f15075,f14965,f14968,f14971,f15017,f15020,f15065,f15068,f15071,f15076]) ).
fof(f15080,plain,
( l3_lattices(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,sK916_skl)))
| ~ v12_lattices(sK914_skl)
| ~ v16_lattices(sK914_skl)
| ~ v15_lattices(sK914_skl)
| ~ m1_subset_1(sK916_skl,u1_struct_0(sK914_skl))
| ~ m1_subset_1(sK915_skl,u1_struct_0(sK914_skl))
| ~ l3_lattices(sK914_skl)
| ~ v10_lattices(sK914_skl)
| v3_struct_0(sK914_skl) ),
inference(resolution,[status(thm)],[f14808,f11914]) ).
fof(f15081,plain,
( sQ316_spl
| ~ sQ413_spl
| ~ sQ412_spl
| ~ sQ411_spl
| ~ sQ402_spl
| ~ sQ401_spl
| ~ sQ392_spl
| ~ sQ391_spl
| sQ390_spl ),
inference(split_clause,[status(thm)],[f15080,f14965,f14968,f14971,f15017,f15020,f15065,f15068,f15071,f13891]) ).
fof(f15179,plain,
( v11_lattices(sK914_skl)
| v3_struct_0(sK914_skl)
| ~ l3_lattices(sK914_skl) ),
inference(resolution,[status(thm)],[f9725,f11912]) ).
fof(f15180,definition,
( sQ421_spl
<=> v11_lattices(sK914_skl) ),
introduced(definition,[new_symbols(definition,[sQ421_spl])],[split_symbol_definition]) ).
fof(f15183,plain,
( sQ421_spl
| sQ390_spl
| ~ sQ392_spl ),
inference(split_clause,[status(thm)],[f15179,f14971,f14965,f15180]) ).
fof(f15191,plain,
( v15_lattices(sK914_skl)
| v3_struct_0(sK914_skl)
| ~ l3_lattices(sK914_skl) ),
inference(resolution,[status(thm)],[f9728,f11912]) ).
fof(f15192,plain,
( sQ411_spl
| sQ390_spl
| ~ sQ392_spl ),
inference(split_clause,[status(thm)],[f15191,f14971,f14965,f15065]) ).
fof(f15193,plain,
( v16_lattices(sK914_skl)
| v3_struct_0(sK914_skl)
| ~ l3_lattices(sK914_skl) ),
inference(resolution,[status(thm)],[f9729,f11912]) ).
fof(f15194,plain,
( sQ412_spl
| sQ390_spl
| ~ sQ392_spl ),
inference(split_clause,[status(thm)],[f15193,f14971,f14965,f15068]) ).
fof(f15473,plain,
( v12_lattices(sK914_skl)
| ~ v11_lattices(sK914_skl)
| v3_struct_0(sK914_skl)
| ~ l3_lattices(sK914_skl) ),
inference(resolution,[status(thm)],[f9759,f11906]) ).
fof(f15475,plain,
( sQ413_spl
| ~ sQ421_spl
| sQ390_spl
| ~ sQ392_spl ),
inference(split_clause,[status(thm)],[f15473,f14971,f14965,f15180,f15071]) ).
fof(f15702,plain,
( ~ sQ313_spl
| ~ r3_lattices(sK914_skl,sK915_skl,sK916_skl)
| ~ v12_lattices(sK914_skl)
| ~ v16_lattices(sK914_skl)
| ~ v15_lattices(sK914_skl)
| ~ m1_subset_1(sK916_skl,u1_struct_0(sK914_skl))
| ~ m1_subset_1(sK915_skl,u1_struct_0(sK914_skl))
| ~ l3_lattices(sK914_skl)
| ~ v10_lattices(sK914_skl)
| v3_struct_0(sK914_skl) ),
inference(resolution,[status(thm)],[f13883,f14804]) ).
fof(f15704,definition,
( sQ445_spl
<=> r3_lattices(sK914_skl,sK915_skl,sK916_skl) ),
introduced(definition,[new_symbols(definition,[sQ445_spl])],[split_symbol_definition]) ).
fof(f15706,plain,
( sQ445_spl
| ~ r3_lattices(sK914_skl,sK915_skl,sK916_skl) ),
inference(component_clause,[status(thm)],[f15704]) ).
fof(f15707,plain,
( ~ sQ313_spl
| ~ sQ445_spl
| ~ sQ413_spl
| ~ sQ412_spl
| ~ sQ411_spl
| ~ sQ402_spl
| ~ sQ401_spl
| ~ sQ392_spl
| ~ sQ391_spl
| sQ390_spl ),
inference(split_clause,[status(thm)],[f15702,f14965,f14968,f14971,f15017,f15020,f15065,f15068,f15071,f15704,f13882]) ).
fof(f15715,plain,
( sQ445_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f15706,f11914]) ).
fof(f15716,plain,
sQ445_spl,
inference(contradiction_clause,[status(thm)],[f15715]) ).
fof(f15775,plain,
( ~ sQ314_spl
| v11_lattices(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,sK916_skl)))
| ~ v3_filter_0(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,sK916_skl)))
| v3_struct_0(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,sK916_skl)))
| ~ l3_lattices(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,sK916_skl))) ),
inference(resolution,[status(thm)],[f13886,f10062]) ).
fof(f15785,definition,
( sQ460_spl
<=> v11_lattices(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,sK916_skl))) ),
introduced(definition,[new_symbols(definition,[sQ460_spl])],[split_symbol_definition]) ).
fof(f15788,plain,
( ~ sQ314_spl
| sQ460_spl
| ~ sQ410_spl
| sQ313_spl
| ~ sQ316_spl ),
inference(split_clause,[status(thm)],[f15775,f13891,f13882,f15060,f15785,f13885]) ).
fof(f16395,plain,
( v3_filter_0(sK914_skl)
| ~ l3_lattices(sK914_skl)
| ~ v10_lattices(sK914_skl)
| v3_struct_0(sK914_skl) ),
inference(resolution,[status(thm)],[f10235,f11912]) ).
fof(f16396,plain,
( sQ409_spl
| ~ sQ392_spl
| ~ sQ391_spl
| sQ390_spl ),
inference(split_clause,[status(thm)],[f16395,f14965,f14968,f14971,f15057]) ).
fof(f20241,plain,
( ~ sQ406_spl
| v17_lattices(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,sK916_skl)))
| ~ v16_lattices(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,sK916_skl)))
| ~ v11_lattices(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,sK916_skl)))
| v3_struct_0(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,sK916_skl)))
| ~ l3_lattices(k23_filter_2(sK914_skl,k22_filter_2(sK914_skl,sK915_skl,sK916_skl))) ),
inference(resolution,[status(thm)],[f15043,f9732]) ).
fof(f20244,plain,
( ~ sQ406_spl
| sQ315_spl
| ~ sQ414_spl
| ~ sQ460_spl
| sQ313_spl
| ~ sQ316_spl ),
inference(split_clause,[status(thm)],[f20241,f13891,f13882,f15785,f15076,f13888,f15042]) ).
fof(f20253,plain,
$false,
inference(sat_refutation,[status(thm)],[f13894,f14986,f14988,f14990,f15028,f15030,f15045,f15063,f15074,f15079,f15081,f15183,f15192,f15194,f15475,f15707,f15716,f15788,f16396,f20244]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : LAT337+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.43 % Computer : n026.cluster.edu
% 0.16/0.43 % Model : x86_64 x86_64
% 0.16/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.43 % Memory : 8046.5625MB
% 0.16/0.43 % OS : Linux 6.8.0-71-generic
% 0.16/0.43 % CPULimit : 300
% 0.16/0.43 % WCLimit : 300
% 0.16/0.43 % DateTime : Sun Sep 20 23:44:06 UTC 2026
% 0.16/0.43 % CPUTime :
% 0.55/0.87 % Drodi V4.1.1
% 198.70/25.99 % Refutation found
% 198.70/25.99 % SZS status Theorem for theBenchmark: Theorem is valid
% 198.70/25.99 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 173.78/26.20 % Elapsed time: 25.742545 seconds
% 173.78/26.20 % CPU time: 199.809312 seconds
% 173.78/26.20 % Total memory used: 919.823 MB
% 173.78/26.20 % Net memory used: 840.105 MB
%------------------------------------------------------------------------------