%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LAT319+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 : n005.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:43 PM UTC 2026
% Result : Theorem 0.12s 0.60s
% Output : CNFRefutation 0.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 29
% Syntax : Number of formulae : 150 ( 7 unt; 20 def)
% Number of atoms : 733 ( 0 equ)
% Maximal formula atoms : 23 ( 4 avg)
% Number of connectives : 930 ( 347 ~; 386 |; 156 &)
% ( 26 <=>; 13 =>; 0 <=; 2 <~>)
% Maximal formula depth : 15 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 37 ( 36 usr; 20 prp; 0-1 aty)
% Number of functors : 2 ( 2 usr; 1 con; 0-1 aty)
% Number of variables : 52 ( 49 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( ( l3_lattices(A)
& v17_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
<=> ( l3_lattices(k1_lattice2(A))
& v17_lattices(k1_lattice2(A))
& v10_lattices(k1_lattice2(A))
& ~ v3_struct_0(k1_lattice2(A)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
~ ! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( ( l3_lattices(A)
& v17_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
<=> ( l3_lattices(k1_lattice2(A))
& v17_lattices(k1_lattice2(A))
& v10_lattices(k1_lattice2(A))
& ~ v3_struct_0(k1_lattice2(A)) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f6,axiom,
! [A] :
( l3_lattices(A)
=> ( ( v10_lattices(A)
& ~ v3_struct_0(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(f12,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(f13,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(f18,axiom,
! [A] :
( l3_lattices(A)
=> ( l3_lattices(k1_lattice2(A))
& v3_lattices(k1_lattice2(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f39,axiom,
! [A] :
( ( l3_lattices(A)
& ~ v3_struct_0(A) )
=> ( v3_lattices(k1_lattice2(A))
& ~ v3_struct_0(k1_lattice2(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f49,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( v10_lattices(k1_lattice2(A))
& v9_lattices(k1_lattice2(A))
& v8_lattices(k1_lattice2(A))
& v7_lattices(k1_lattice2(A))
& v6_lattices(k1_lattice2(A))
& v5_lattices(k1_lattice2(A))
& v4_lattices(k1_lattice2(A))
& v3_lattices(k1_lattice2(A))
& ~ v3_struct_0(k1_lattice2(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f73,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( ( l3_lattices(A)
& v16_lattices(A)
& v15_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
<=> ( l3_lattices(k1_lattice2(A))
& v16_lattices(k1_lattice2(A))
& v15_lattices(k1_lattice2(A))
& v10_lattices(k1_lattice2(A))
& ~ v3_struct_0(k1_lattice2(A)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f75,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( ( l3_lattices(A)
& v11_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
<=> ( l3_lattices(k1_lattice2(A))
& v11_lattices(k1_lattice2(A))
& v10_lattices(k1_lattice2(A))
& ~ v3_struct_0(k1_lattice2(A)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f79,plain,
? [A] :
( ( ( l3_lattices(A)
& v17_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
<~> ( l3_lattices(k1_lattice2(A))
& v17_lattices(k1_lattice2(A))
& v10_lattices(k1_lattice2(A))
& ~ v3_struct_0(k1_lattice2(A)) ) )
& l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f80,definition,
! [A] :
( sP0_prd(A)
<=> ( l3_lattices(A)
& v17_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) ) ),
introduced(definition,[new_symbols(definition,[sP0_prd])],[]) ).
fof(f81,plain,
? [A] :
( ( sP0_prd(A)
<~> ( l3_lattices(k1_lattice2(A))
& v17_lattices(k1_lattice2(A))
& v10_lattices(k1_lattice2(A))
& ~ v3_struct_0(k1_lattice2(A)) ) )
& l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) ),
inference(formula_renaming,[status(thm)],[f79,f80]) ).
fof(f82,plain,
? [A] :
( ( ~ l3_lattices(k1_lattice2(A))
| ~ v17_lattices(k1_lattice2(A))
| ~ v10_lattices(k1_lattice2(A))
| v3_struct_0(k1_lattice2(A))
| ~ sP0_prd(A) )
& ( ( l3_lattices(k1_lattice2(A))
& v17_lattices(k1_lattice2(A))
& v10_lattices(k1_lattice2(A))
& ~ v3_struct_0(k1_lattice2(A)) )
| sP0_prd(A) )
& l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) ),
inference(NNF_transformation,[status(thm)],[f81]) ).
fof(f83,plain,
( ( ~ l3_lattices(k1_lattice2(sK0_skl))
| ~ v17_lattices(k1_lattice2(sK0_skl))
| ~ v10_lattices(k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl))
| ~ sP0_prd(sK0_skl) )
& ( ( l3_lattices(k1_lattice2(sK0_skl))
& v17_lattices(k1_lattice2(sK0_skl))
& v10_lattices(k1_lattice2(sK0_skl))
& ~ v3_struct_0(k1_lattice2(sK0_skl)) )
| sP0_prd(sK0_skl) )
& l3_lattices(sK0_skl)
& v10_lattices(sK0_skl)
& ~ v3_struct_0(sK0_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(A,sK0_skl)],[f82]) ).
fof(f84,plain,
~ v3_struct_0(sK0_skl),
inference(cnf_transformation,[status(thm)],[f83]) ).
fof(f85,plain,
v10_lattices(sK0_skl),
inference(cnf_transformation,[status(thm)],[f83]) ).
fof(f86,plain,
l3_lattices(sK0_skl),
inference(cnf_transformation,[status(thm)],[f83]) ).
fof(f89,plain,
( v17_lattices(k1_lattice2(sK0_skl))
| sP0_prd(sK0_skl) ),
inference(cnf_transformation,[status(thm)],[f83]) ).
fof(f91,plain,
( ~ l3_lattices(k1_lattice2(sK0_skl))
| ~ v17_lattices(k1_lattice2(sK0_skl))
| ~ v10_lattices(k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl))
| ~ sP0_prd(sK0_skl) ),
inference(cnf_transformation,[status(thm)],[f83]) ).
fof(f98,plain,
! [A] :
( ( v9_lattices(A)
& v8_lattices(A)
& v7_lattices(A)
& v6_lattices(A)
& v5_lattices(A)
& v4_lattices(A)
& ~ v3_struct_0(A) )
| ~ v10_lattices(A)
| v3_struct_0(A)
| ~ l3_lattices(A) ),
inference(pre_NNF_transformation,[status(thm)],[f6]) ).
fof(f102,plain,
! [X0] :
( v6_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f98]) ).
fof(f103,plain,
! [X0] :
( v7_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f98]) ).
fof(f104,plain,
! [X0] :
( v8_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f98]) ).
fof(f105,plain,
! [X0] :
( v9_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f98]) ).
fof(f123,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)],[f12]) ).
fof(f125,plain,
! [X0] :
( v11_lattices(X0)
| ~ v17_lattices(X0)
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f123]) ).
fof(f128,plain,
! [X0] :
( v15_lattices(X0)
| ~ v17_lattices(X0)
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f123]) ).
fof(f129,plain,
! [X0] :
( v16_lattices(X0)
| ~ v17_lattices(X0)
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f123]) ).
fof(f130,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)],[f13]) ).
fof(f132,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)],[f130]) ).
fof(f154,plain,
! [A] :
( ( l3_lattices(k1_lattice2(A))
& v3_lattices(k1_lattice2(A)) )
| ~ l3_lattices(A) ),
inference(pre_NNF_transformation,[status(thm)],[f18]) ).
fof(f156,plain,
! [X0] :
( l3_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f154]) ).
fof(f188,plain,
! [A] :
( ( v3_lattices(k1_lattice2(A))
& ~ v3_struct_0(k1_lattice2(A)) )
| ~ l3_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f39]) ).
fof(f189,plain,
! [X0] :
( ~ v3_struct_0(k1_lattice2(X0))
| ~ l3_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f188]) ).
fof(f224,plain,
! [A] :
( ( v10_lattices(k1_lattice2(A))
& v9_lattices(k1_lattice2(A))
& v8_lattices(k1_lattice2(A))
& v7_lattices(k1_lattice2(A))
& v6_lattices(k1_lattice2(A))
& v5_lattices(k1_lattice2(A))
& v4_lattices(k1_lattice2(A))
& v3_lattices(k1_lattice2(A))
& ~ v3_struct_0(k1_lattice2(A)) )
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f49]) ).
fof(f233,plain,
! [X0] :
( v10_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f224]) ).
fof(f363,plain,
! [A] :
( ( ( l3_lattices(A)
& v16_lattices(A)
& v15_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
<=> ( l3_lattices(k1_lattice2(A))
& v16_lattices(k1_lattice2(A))
& v15_lattices(k1_lattice2(A))
& v10_lattices(k1_lattice2(A))
& ~ v3_struct_0(k1_lattice2(A)) ) )
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f73]) ).
fof(f364,plain,
! [A] :
( ( ( ~ l3_lattices(k1_lattice2(A))
| ~ v16_lattices(k1_lattice2(A))
| ~ v15_lattices(k1_lattice2(A))
| ~ v10_lattices(k1_lattice2(A))
| v3_struct_0(k1_lattice2(A))
| ( l3_lattices(A)
& v16_lattices(A)
& v15_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) ) )
& ( ( l3_lattices(k1_lattice2(A))
& v16_lattices(k1_lattice2(A))
& v15_lattices(k1_lattice2(A))
& v10_lattices(k1_lattice2(A))
& ~ v3_struct_0(k1_lattice2(A)) )
| ~ l3_lattices(A)
| ~ v16_lattices(A)
| ~ v15_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ) )
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(NNF_transformation,[status(thm)],[f363]) ).
fof(f367,plain,
! [X0] :
( v15_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0)
| ~ v16_lattices(X0)
| ~ v15_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f364]) ).
fof(f368,plain,
! [X0] :
( v16_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0)
| ~ v16_lattices(X0)
| ~ v15_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f364]) ).
fof(f372,plain,
! [X0] :
( ~ l3_lattices(k1_lattice2(X0))
| ~ v16_lattices(k1_lattice2(X0))
| ~ v15_lattices(k1_lattice2(X0))
| ~ v10_lattices(k1_lattice2(X0))
| v3_struct_0(k1_lattice2(X0))
| v15_lattices(X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f364]) ).
fof(f373,plain,
! [X0] :
( ~ l3_lattices(k1_lattice2(X0))
| ~ v16_lattices(k1_lattice2(X0))
| ~ v15_lattices(k1_lattice2(X0))
| ~ v10_lattices(k1_lattice2(X0))
| v3_struct_0(k1_lattice2(X0))
| v16_lattices(X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f364]) ).
fof(f378,plain,
! [A] :
( ( ( l3_lattices(A)
& v11_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
<=> ( l3_lattices(k1_lattice2(A))
& v11_lattices(k1_lattice2(A))
& v10_lattices(k1_lattice2(A))
& ~ v3_struct_0(k1_lattice2(A)) ) )
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f75]) ).
fof(f379,plain,
! [A] :
( ( ( ~ l3_lattices(k1_lattice2(A))
| ~ v11_lattices(k1_lattice2(A))
| ~ v10_lattices(k1_lattice2(A))
| v3_struct_0(k1_lattice2(A))
| ( l3_lattices(A)
& v11_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) ) )
& ( ( l3_lattices(k1_lattice2(A))
& v11_lattices(k1_lattice2(A))
& v10_lattices(k1_lattice2(A))
& ~ v3_struct_0(k1_lattice2(A)) )
| ~ l3_lattices(A)
| ~ v11_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ) )
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(NNF_transformation,[status(thm)],[f378]) ).
fof(f382,plain,
! [X0] :
( v11_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0)
| ~ v11_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f379]) ).
fof(f386,plain,
! [X0] :
( ~ l3_lattices(k1_lattice2(X0))
| ~ v11_lattices(k1_lattice2(X0))
| ~ v10_lattices(k1_lattice2(X0))
| v3_struct_0(k1_lattice2(X0))
| v11_lattices(X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f379]) ).
fof(f396,plain,
! [A] :
( ( ~ l3_lattices(A)
| ~ v17_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| sP0_prd(A) )
& ( ( l3_lattices(A)
& v17_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
| ~ sP0_prd(A) ) ),
inference(NNF_transformation,[status(thm)],[f80]) ).
fof(f397,plain,
( ! [A] :
( ~ l3_lattices(A)
| ~ v17_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| sP0_prd(A) )
& ! [A] :
( ( l3_lattices(A)
& v17_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
| ~ sP0_prd(A) ) ),
inference(miniscoping,[status(thm)],[f396]) ).
fof(f400,plain,
! [X0] :
( v17_lattices(X0)
| ~ sP0_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f397]) ).
fof(f402,plain,
! [X0] :
( ~ l3_lattices(X0)
| ~ v17_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| sP0_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f397]) ).
fof(f403,definition,
( sQ0_spl
<=> sP0_prd(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f405,plain,
( sQ0_spl
| ~ sP0_prd(sK0_skl) ),
inference(component_clause,[status(thm)],[f403]) ).
fof(f406,definition,
( sQ1_spl
<=> v3_struct_0(k1_lattice2(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f407,plain,
( ~ sQ1_spl
| v3_struct_0(k1_lattice2(sK0_skl)) ),
inference(component_clause,[status(thm)],[f406]) ).
fof(f410,definition,
( sQ2_spl
<=> v10_lattices(k1_lattice2(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f412,plain,
( sQ2_spl
| ~ v10_lattices(k1_lattice2(sK0_skl)) ),
inference(component_clause,[status(thm)],[f410]) ).
fof(f414,definition,
( sQ3_spl
<=> v17_lattices(k1_lattice2(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f416,plain,
( sQ3_spl
| ~ v17_lattices(k1_lattice2(sK0_skl)) ),
inference(component_clause,[status(thm)],[f414]) ).
fof(f417,plain,
( sQ3_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f89,f403,f414]) ).
fof(f418,definition,
( sQ4_spl
<=> l3_lattices(k1_lattice2(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f420,plain,
( sQ4_spl
| ~ l3_lattices(k1_lattice2(sK0_skl)) ),
inference(component_clause,[status(thm)],[f418]) ).
fof(f422,plain,
( ~ sQ4_spl
| ~ sQ3_spl
| ~ sQ2_spl
| sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f91,f403,f406,f410,f414,f418]) ).
fof(f426,plain,
! [X0] :
( v15_lattices(k1_lattice2(X0))
| ~ v16_lattices(X0)
| ~ v15_lattices(X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f367]) ).
fof(f427,plain,
! [X0] :
( v16_lattices(k1_lattice2(X0))
| ~ v16_lattices(X0)
| ~ v15_lattices(X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f368]) ).
fof(f429,plain,
! [X0] :
( ~ l3_lattices(k1_lattice2(X0))
| ~ v16_lattices(k1_lattice2(X0))
| ~ v15_lattices(k1_lattice2(X0))
| ~ v10_lattices(k1_lattice2(X0))
| v15_lattices(X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f372,f189]) ).
fof(f430,plain,
! [X0] :
( ~ l3_lattices(k1_lattice2(X0))
| ~ v16_lattices(k1_lattice2(X0))
| ~ v15_lattices(k1_lattice2(X0))
| ~ v10_lattices(k1_lattice2(X0))
| v16_lattices(X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f373,f189]) ).
fof(f433,plain,
! [X0] :
( v11_lattices(k1_lattice2(X0))
| ~ v11_lattices(X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f382]) ).
fof(f435,plain,
! [X0] :
( ~ l3_lattices(k1_lattice2(X0))
| ~ v11_lattices(k1_lattice2(X0))
| ~ v10_lattices(k1_lattice2(X0))
| v11_lattices(X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f386,f189]) ).
fof(f440,plain,
( ~ sQ1_spl
| ~ l3_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f407,f189]) ).
fof(f442,definition,
( sQ5_spl
<=> v3_struct_0(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f443,plain,
( ~ sQ5_spl
| v3_struct_0(sK0_skl) ),
inference(component_clause,[status(thm)],[f442]) ).
fof(f445,definition,
( sQ6_spl
<=> l3_lattices(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f447,plain,
( sQ6_spl
| ~ l3_lattices(sK0_skl) ),
inference(component_clause,[status(thm)],[f445]) ).
fof(f448,plain,
( ~ sQ1_spl
| ~ sQ6_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f440,f442,f445,f406]) ).
fof(f449,plain,
( sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f447,f86]) ).
fof(f450,plain,
sQ6_spl,
inference(contradiction_clause,[status(thm)],[f449]) ).
fof(f451,plain,
( ~ sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f443,f84]) ).
fof(f452,plain,
~ sQ5_spl,
inference(contradiction_clause,[status(thm)],[f451]) ).
fof(f453,plain,
( sQ2_spl
| ~ l3_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f412,f233]) ).
fof(f456,definition,
( sQ7_spl
<=> v10_lattices(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f458,plain,
( sQ7_spl
| ~ v10_lattices(sK0_skl) ),
inference(component_clause,[status(thm)],[f456]) ).
fof(f459,plain,
( sQ2_spl
| ~ sQ6_spl
| ~ sQ7_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f453,f442,f456,f445,f410]) ).
fof(f466,definition,
( sQ10_spl
<=> v6_lattices(k1_lattice2(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f468,plain,
( sQ10_spl
| ~ v6_lattices(k1_lattice2(sK0_skl)) ),
inference(component_clause,[status(thm)],[f466]) ).
fof(f469,definition,
( sQ11_spl
<=> v7_lattices(k1_lattice2(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f471,plain,
( sQ11_spl
| ~ v7_lattices(k1_lattice2(sK0_skl)) ),
inference(component_clause,[status(thm)],[f469]) ).
fof(f472,definition,
( sQ12_spl
<=> v8_lattices(k1_lattice2(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f474,plain,
( sQ12_spl
| ~ v8_lattices(k1_lattice2(sK0_skl)) ),
inference(component_clause,[status(thm)],[f472]) ).
fof(f475,definition,
( sQ13_spl
<=> v9_lattices(k1_lattice2(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f477,plain,
( sQ13_spl
| ~ v9_lattices(k1_lattice2(sK0_skl)) ),
inference(component_clause,[status(thm)],[f475]) ).
fof(f479,plain,
( sQ4_spl
| ~ l3_lattices(sK0_skl) ),
inference(resolution,[status(thm)],[f420,f156]) ).
fof(f481,plain,
( sQ4_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f479,f445,f418]) ).
fof(f482,plain,
( sQ0_spl
| ~ l3_lattices(sK0_skl)
| ~ v17_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f405,f402]) ).
fof(f483,definition,
( sQ14_spl
<=> v17_lattices(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f485,plain,
( sQ14_spl
| ~ v17_lattices(sK0_skl) ),
inference(component_clause,[status(thm)],[f483]) ).
fof(f486,plain,
( sQ0_spl
| ~ sQ6_spl
| ~ sQ14_spl
| ~ sQ7_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f482,f442,f456,f483,f445,f403]) ).
fof(f487,plain,
( sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f458,f85]) ).
fof(f488,plain,
sQ7_spl,
inference(contradiction_clause,[status(thm)],[f487]) ).
fof(f493,plain,
( sQ14_spl
| ~ sP0_prd(sK0_skl) ),
inference(resolution,[status(thm)],[f485,f400]) ).
fof(f494,plain,
( sQ14_spl
| ~ v16_lattices(sK0_skl)
| ~ v15_lattices(sK0_skl)
| ~ v11_lattices(sK0_skl)
| v3_struct_0(sK0_skl)
| ~ l3_lattices(sK0_skl) ),
inference(resolution,[status(thm)],[f485,f132]) ).
fof(f495,definition,
( sQ15_spl
<=> v11_lattices(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f497,plain,
( sQ15_spl
| ~ v11_lattices(sK0_skl) ),
inference(component_clause,[status(thm)],[f495]) ).
fof(f498,definition,
( sQ16_spl
<=> v15_lattices(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f500,plain,
( sQ16_spl
| ~ v15_lattices(sK0_skl) ),
inference(component_clause,[status(thm)],[f498]) ).
fof(f501,definition,
( sQ17_spl
<=> v16_lattices(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f503,plain,
( sQ17_spl
| ~ v16_lattices(sK0_skl) ),
inference(component_clause,[status(thm)],[f501]) ).
fof(f504,plain,
( sQ14_spl
| ~ sQ17_spl
| ~ sQ16_spl
| ~ sQ15_spl
| sQ5_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f494,f445,f442,f495,f498,f501,f483]) ).
fof(f505,plain,
( sQ17_spl
| ~ l3_lattices(k1_lattice2(sK0_skl))
| ~ v16_lattices(k1_lattice2(sK0_skl))
| ~ v15_lattices(k1_lattice2(sK0_skl))
| ~ v10_lattices(k1_lattice2(sK0_skl))
| ~ l3_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f503,f430]) ).
fof(f506,plain,
( sQ17_spl
| ~ v17_lattices(sK0_skl)
| v3_struct_0(sK0_skl)
| ~ l3_lattices(sK0_skl) ),
inference(resolution,[status(thm)],[f503,f129]) ).
fof(f507,definition,
( sQ18_spl
<=> v15_lattices(k1_lattice2(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f509,plain,
( sQ18_spl
| ~ v15_lattices(k1_lattice2(sK0_skl)) ),
inference(component_clause,[status(thm)],[f507]) ).
fof(f510,definition,
( sQ19_spl
<=> v16_lattices(k1_lattice2(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f512,plain,
( sQ19_spl
| ~ v16_lattices(k1_lattice2(sK0_skl)) ),
inference(component_clause,[status(thm)],[f510]) ).
fof(f513,plain,
( sQ17_spl
| ~ sQ4_spl
| ~ sQ19_spl
| ~ sQ18_spl
| ~ sQ2_spl
| ~ sQ6_spl
| ~ sQ7_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f505,f442,f456,f445,f410,f507,f510,f418,f501]) ).
fof(f514,plain,
( sQ17_spl
| ~ sQ14_spl
| sQ5_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f506,f445,f442,f483,f501]) ).
fof(f516,plain,
( sQ16_spl
| ~ l3_lattices(k1_lattice2(sK0_skl))
| ~ v16_lattices(k1_lattice2(sK0_skl))
| ~ v15_lattices(k1_lattice2(sK0_skl))
| ~ v10_lattices(k1_lattice2(sK0_skl))
| ~ l3_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f500,f429]) ).
fof(f517,plain,
( sQ16_spl
| ~ v17_lattices(sK0_skl)
| v3_struct_0(sK0_skl)
| ~ l3_lattices(sK0_skl) ),
inference(resolution,[status(thm)],[f500,f128]) ).
fof(f525,plain,
( sQ16_spl
| ~ sQ4_spl
| ~ sQ19_spl
| ~ sQ18_spl
| ~ sQ2_spl
| ~ sQ6_spl
| ~ sQ7_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f516,f442,f456,f445,f410,f507,f510,f418,f498]) ).
fof(f526,plain,
( sQ16_spl
| ~ sQ14_spl
| sQ5_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f517,f445,f442,f483,f498]) ).
fof(f527,plain,
( sQ15_spl
| ~ l3_lattices(k1_lattice2(sK0_skl))
| ~ v11_lattices(k1_lattice2(sK0_skl))
| ~ v10_lattices(k1_lattice2(sK0_skl))
| ~ l3_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f497,f435]) ).
fof(f528,plain,
( sQ15_spl
| ~ v17_lattices(sK0_skl)
| v3_struct_0(sK0_skl)
| ~ l3_lattices(sK0_skl) ),
inference(resolution,[status(thm)],[f497,f125]) ).
fof(f529,definition,
( sQ22_spl
<=> v11_lattices(k1_lattice2(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f531,plain,
( sQ22_spl
| ~ v11_lattices(k1_lattice2(sK0_skl)) ),
inference(component_clause,[status(thm)],[f529]) ).
fof(f532,plain,
( sQ15_spl
| ~ sQ4_spl
| ~ sQ22_spl
| ~ sQ2_spl
| ~ sQ6_spl
| ~ sQ7_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f527,f442,f456,f445,f410,f529,f418,f495]) ).
fof(f533,plain,
( sQ15_spl
| ~ sQ14_spl
| sQ5_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f528,f445,f442,f483,f495]) ).
fof(f535,plain,
( sQ13_spl
| ~ v10_lattices(k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl))
| ~ l3_lattices(k1_lattice2(sK0_skl)) ),
inference(resolution,[status(thm)],[f477,f105]) ).
fof(f537,plain,
( sQ13_spl
| ~ sQ2_spl
| sQ1_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f535,f418,f406,f410,f475]) ).
fof(f539,plain,
( sQ12_spl
| ~ v10_lattices(k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl))
| ~ l3_lattices(k1_lattice2(sK0_skl)) ),
inference(resolution,[status(thm)],[f474,f104]) ).
fof(f541,plain,
( sQ12_spl
| ~ sQ2_spl
| sQ1_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f539,f418,f406,f410,f472]) ).
fof(f543,plain,
( sQ11_spl
| ~ v10_lattices(k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl))
| ~ l3_lattices(k1_lattice2(sK0_skl)) ),
inference(resolution,[status(thm)],[f471,f103]) ).
fof(f545,plain,
( sQ11_spl
| ~ sQ2_spl
| sQ1_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f543,f418,f406,f410,f469]) ).
fof(f547,plain,
( sQ10_spl
| ~ v10_lattices(k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl))
| ~ l3_lattices(k1_lattice2(sK0_skl)) ),
inference(resolution,[status(thm)],[f468,f102]) ).
fof(f549,plain,
( sQ10_spl
| ~ sQ2_spl
| sQ1_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f547,f418,f406,f410,f466]) ).
fof(f574,plain,
( sQ18_spl
| ~ v16_lattices(sK0_skl)
| ~ v15_lattices(sK0_skl)
| ~ l3_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f509,f426]) ).
fof(f577,plain,
( sQ18_spl
| ~ v17_lattices(k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl))
| ~ l3_lattices(k1_lattice2(sK0_skl)) ),
inference(resolution,[status(thm)],[f509,f128]) ).
fof(f578,plain,
( sQ18_spl
| ~ sQ17_spl
| ~ sQ16_spl
| ~ sQ6_spl
| ~ sQ7_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f574,f442,f456,f445,f498,f501,f507]) ).
fof(f599,plain,
( sQ18_spl
| ~ sQ3_spl
| sQ1_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f577,f418,f406,f414,f507]) ).
fof(f600,plain,
( sQ22_spl
| ~ v11_lattices(sK0_skl)
| ~ l3_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f531,f433]) ).
fof(f602,plain,
( sQ22_spl
| ~ v17_lattices(k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl))
| ~ l3_lattices(k1_lattice2(sK0_skl)) ),
inference(resolution,[status(thm)],[f531,f125]) ).
fof(f603,plain,
( sQ22_spl
| ~ sQ15_spl
| ~ sQ6_spl
| ~ sQ7_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f600,f442,f456,f445,f495,f529]) ).
fof(f608,plain,
( sQ22_spl
| ~ sQ3_spl
| sQ1_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f602,f418,f406,f414,f529]) ).
fof(f610,plain,
( sQ19_spl
| ~ v16_lattices(sK0_skl)
| ~ v15_lattices(sK0_skl)
| ~ l3_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f512,f427]) ).
fof(f612,plain,
( sQ19_spl
| ~ v17_lattices(k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl))
| ~ l3_lattices(k1_lattice2(sK0_skl)) ),
inference(resolution,[status(thm)],[f512,f129]) ).
fof(f613,plain,
( sQ19_spl
| ~ sQ17_spl
| ~ sQ16_spl
| ~ sQ6_spl
| ~ sQ7_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f610,f442,f456,f445,f498,f501,f510]) ).
fof(f615,plain,
( sQ19_spl
| ~ sQ3_spl
| sQ1_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f612,f418,f406,f414,f510]) ).
fof(f616,plain,
( sQ14_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f493,f403,f483]) ).
fof(f620,plain,
( sQ3_spl
| ~ v16_lattices(k1_lattice2(sK0_skl))
| ~ v15_lattices(k1_lattice2(sK0_skl))
| ~ v11_lattices(k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl))
| ~ l3_lattices(k1_lattice2(sK0_skl)) ),
inference(resolution,[status(thm)],[f416,f132]) ).
fof(f621,plain,
( sQ3_spl
| ~ sQ19_spl
| ~ sQ18_spl
| ~ sQ22_spl
| sQ1_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f620,f418,f406,f529,f507,f510,f414]) ).
fof(f622,plain,
$false,
inference(sat_refutation,[status(thm)],[f417,f422,f448,f450,f452,f459,f481,f486,f488,f504,f513,f514,f525,f526,f532,f533,f537,f541,f545,f549,f578,f599,f603,f608,f613,f615,f616,f621]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT319+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.55 % Computer : n005.cluster.edu
% 0.09/0.55 % Model : x86_64 x86_64
% 0.09/0.55 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.55 % Memory : 8046.5625MB
% 0.09/0.55 % OS : Linux 6.8.0-71-generic
% 0.09/0.55 % CPULimit : 300
% 0.09/0.55 % WCLimit : 300
% 0.09/0.55 % DateTime : Sun Sep 20 23:35:48 UTC 2026
% 0.09/0.55 % CPUTime :
% 0.09/0.56 % Drodi V4.1.1
% 0.12/0.60 % Refutation found
% 0.12/0.60 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.12/0.60 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.12/0.62 % Elapsed time: 0.065267 seconds
% 0.12/0.62 % CPU time: 0.217285 seconds
% 0.12/0.62 % Total memory used: 92.754 MB
% 0.12/0.62 % Net memory used: 92.605 MB
%------------------------------------------------------------------------------