%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LAT292+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 : n018.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:35 PM UTC 2026
% Result : Theorem 0.20s 0.51s
% Output : CNFRefutation 0.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 25
% Syntax : Number of formulae : 101 ( 21 unt; 15 def)
% Number of atoms : 443 ( 6 equ)
% Maximal formula atoms : 17 ( 4 avg)
% Number of connectives : 476 ( 134 ~; 135 |; 186 &)
% ( 15 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 39 ( 37 usr; 16 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 6 con; 0-1 aty)
% Number of variables : 26 ( 18 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [A] :
( ( l3_lattices(A)
& ~ v3_realset2(A)
& v17_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ? [B] :
( r1_filter_1(A,k6_lopclset(B))
& l1_pre_topc(B)
& v2_pre_topc(B)
& ~ v3_struct_0(B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
~ ! [A] :
( ( l3_lattices(A)
& ~ v3_realset2(A)
& v17_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ? [B] :
( r1_filter_1(A,k6_lopclset(B))
& l1_pre_topc(B)
& v2_pre_topc(B)
& ~ v3_struct_0(B) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f38,axiom,
! [A] :
( ( l3_lattices(A)
& ~ v3_realset2(A)
& v17_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> k12_lopclset(A) = k6_lopclset(k11_lopclset(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f41,axiom,
! [A] :
( ( l3_lattices(A)
& ~ v3_realset2(A)
& v17_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( l1_pre_topc(k11_lopclset(A))
& v2_pre_topc(k11_lopclset(A))
& v1_pre_topc(k11_lopclset(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f75,axiom,
! [A] :
( ( l3_lattices(A)
& ~ v3_realset2(A)
& v17_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( v2_pre_topc(k11_lopclset(A))
& v1_pre_topc(k11_lopclset(A))
& ~ v3_struct_0(k11_lopclset(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f80,axiom,
? [A] :
( v14_lattices(A)
& v13_lattices(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_lattices(A)
& ~ v3_struct_0(A)
& l3_lattices(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f81,axiom,
? [A] :
( v15_lattices(A)
& v14_lattices(A)
& v13_lattices(A)
& v10_lattices(A)
& v9_lattices(A)
& v8_lattices(A)
& v7_lattices(A)
& v6_lattices(A)
& v5_lattices(A)
& v4_lattices(A)
& v3_lattices(A)
& ~ v3_struct_0(A)
& l3_lattices(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f82,axiom,
? [A] :
( v16_lattices(A)
& v15_lattices(A)
& v14_lattices(A)
& v13_lattices(A)
& v10_lattices(A)
& v9_lattices(A)
& v8_lattices(A)
& v7_lattices(A)
& v6_lattices(A)
& v5_lattices(A)
& v4_lattices(A)
& v3_lattices(A)
& ~ v3_struct_0(A)
& l3_lattices(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f83,axiom,
? [A] :
( v17_lattices(A)
& v16_lattices(A)
& v15_lattices(A)
& v14_lattices(A)
& v13_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_lattices(A)
& ~ v3_struct_0(A)
& l3_lattices(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f86,axiom,
? [A] :
( ~ v3_realset2(A)
& v17_lattices(A)
& v16_lattices(A)
& v15_lattices(A)
& v14_lattices(A)
& v13_lattices(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)
& l3_lattices(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f108,axiom,
! [A] :
( ( l3_lattices(A)
& ~ v3_realset2(A)
& v17_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> r1_filter_1(A,k12_lopclset(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f114,plain,
? [A] :
( ! [B] :
( ~ r1_filter_1(A,k6_lopclset(B))
| ~ l1_pre_topc(B)
| ~ v2_pre_topc(B)
| v3_struct_0(B) )
& l3_lattices(A)
& ~ v3_realset2(A)
& v17_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f115,plain,
( ! [B] :
( ~ r1_filter_1(sK0_skl,k6_lopclset(B))
| ~ l1_pre_topc(B)
| ~ v2_pre_topc(B)
| v3_struct_0(B) )
& l3_lattices(sK0_skl)
& ~ v3_realset2(sK0_skl)
& v17_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)],[f114]) ).
fof(f116,plain,
~ v3_struct_0(sK0_skl),
inference(cnf_transformation,[status(thm)],[f115]) ).
fof(f117,plain,
v10_lattices(sK0_skl),
inference(cnf_transformation,[status(thm)],[f115]) ).
fof(f118,plain,
v17_lattices(sK0_skl),
inference(cnf_transformation,[status(thm)],[f115]) ).
fof(f119,plain,
~ v3_realset2(sK0_skl),
inference(cnf_transformation,[status(thm)],[f115]) ).
fof(f120,plain,
l3_lattices(sK0_skl),
inference(cnf_transformation,[status(thm)],[f115]) ).
fof(f121,plain,
! [X0] :
( ~ r1_filter_1(sK0_skl,k6_lopclset(X0))
| ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f115]) ).
fof(f249,plain,
! [A] :
( k12_lopclset(A) = k6_lopclset(k11_lopclset(A))
| ~ l3_lattices(A)
| v3_realset2(A)
| ~ v17_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f38]) ).
fof(f250,plain,
! [X0] :
( k12_lopclset(X0) = k6_lopclset(k11_lopclset(X0))
| ~ l3_lattices(X0)
| v3_realset2(X0)
| ~ v17_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f249]) ).
fof(f257,plain,
! [A] :
( ( l1_pre_topc(k11_lopclset(A))
& v2_pre_topc(k11_lopclset(A))
& v1_pre_topc(k11_lopclset(A)) )
| ~ l3_lattices(A)
| v3_realset2(A)
| ~ v17_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f41]) ).
fof(f259,plain,
! [X0] :
( v2_pre_topc(k11_lopclset(X0))
| ~ l3_lattices(X0)
| v3_realset2(X0)
| ~ v17_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f257]) ).
fof(f260,plain,
! [X0] :
( l1_pre_topc(k11_lopclset(X0))
| ~ l3_lattices(X0)
| v3_realset2(X0)
| ~ v17_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f257]) ).
fof(f330,plain,
! [A] :
( ( v2_pre_topc(k11_lopclset(A))
& v1_pre_topc(k11_lopclset(A))
& ~ v3_struct_0(k11_lopclset(A)) )
| ~ l3_lattices(A)
| v3_realset2(A)
| ~ v17_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f75]) ).
fof(f331,plain,
! [X0] :
( ~ v3_struct_0(k11_lopclset(X0))
| ~ l3_lattices(X0)
| v3_realset2(X0)
| ~ v17_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f330]) ).
fof(f356,plain,
( v14_lattices(sK10_skl)
& v13_lattices(sK10_skl)
& v12_lattices(sK10_skl)
& v11_lattices(sK10_skl)
& v10_lattices(sK10_skl)
& v9_lattices(sK10_skl)
& v8_lattices(sK10_skl)
& v7_lattices(sK10_skl)
& v6_lattices(sK10_skl)
& v5_lattices(sK10_skl)
& v4_lattices(sK10_skl)
& v3_lattices(sK10_skl)
& ~ v3_struct_0(sK10_skl)
& l3_lattices(sK10_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(A,sK10_skl)],[f80]) ).
fof(f366,plain,
v10_lattices(sK10_skl),
inference(cnf_transformation,[status(thm)],[f356]) ).
fof(f371,plain,
( v15_lattices(sK11_skl)
& v14_lattices(sK11_skl)
& v13_lattices(sK11_skl)
& v10_lattices(sK11_skl)
& v9_lattices(sK11_skl)
& v8_lattices(sK11_skl)
& v7_lattices(sK11_skl)
& v6_lattices(sK11_skl)
& v5_lattices(sK11_skl)
& v4_lattices(sK11_skl)
& v3_lattices(sK11_skl)
& ~ v3_struct_0(sK11_skl)
& l3_lattices(sK11_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(A,sK11_skl)],[f81]) ).
fof(f381,plain,
v10_lattices(sK11_skl),
inference(cnf_transformation,[status(thm)],[f371]) ).
fof(f385,plain,
( v16_lattices(sK12_skl)
& v15_lattices(sK12_skl)
& v14_lattices(sK12_skl)
& v13_lattices(sK12_skl)
& v10_lattices(sK12_skl)
& v9_lattices(sK12_skl)
& v8_lattices(sK12_skl)
& v7_lattices(sK12_skl)
& v6_lattices(sK12_skl)
& v5_lattices(sK12_skl)
& v4_lattices(sK12_skl)
& v3_lattices(sK12_skl)
& ~ v3_struct_0(sK12_skl)
& l3_lattices(sK12_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl]),skolemize(A,sK12_skl)],[f82]) ).
fof(f395,plain,
v10_lattices(sK12_skl),
inference(cnf_transformation,[status(thm)],[f385]) ).
fof(f400,plain,
( v17_lattices(sK13_skl)
& v16_lattices(sK13_skl)
& v15_lattices(sK13_skl)
& v14_lattices(sK13_skl)
& v13_lattices(sK13_skl)
& v11_lattices(sK13_skl)
& v10_lattices(sK13_skl)
& v9_lattices(sK13_skl)
& v8_lattices(sK13_skl)
& v7_lattices(sK13_skl)
& v6_lattices(sK13_skl)
& v5_lattices(sK13_skl)
& v4_lattices(sK13_skl)
& v3_lattices(sK13_skl)
& ~ v3_struct_0(sK13_skl)
& l3_lattices(sK13_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl]),skolemize(A,sK13_skl)],[f83]) ).
fof(f401,plain,
l3_lattices(sK13_skl),
inference(cnf_transformation,[status(thm)],[f400]) ).
fof(f425,plain,
( ~ v3_realset2(sK16_skl)
& v17_lattices(sK16_skl)
& v16_lattices(sK16_skl)
& v15_lattices(sK16_skl)
& v14_lattices(sK16_skl)
& v13_lattices(sK16_skl)
& v12_lattices(sK16_skl)
& v11_lattices(sK16_skl)
& v10_lattices(sK16_skl)
& v9_lattices(sK16_skl)
& v8_lattices(sK16_skl)
& v7_lattices(sK16_skl)
& v6_lattices(sK16_skl)
& v5_lattices(sK16_skl)
& v4_lattices(sK16_skl)
& ~ v3_struct_0(sK16_skl)
& l3_lattices(sK16_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16_skl]),skolemize(A,sK16_skl)],[f86]) ).
fof(f442,plain,
~ v3_realset2(sK16_skl),
inference(cnf_transformation,[status(thm)],[f425]) ).
fof(f530,plain,
! [A] :
( r1_filter_1(A,k12_lopclset(A))
| ~ l3_lattices(A)
| v3_realset2(A)
| ~ v17_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f108]) ).
fof(f531,plain,
! [X0] :
( r1_filter_1(X0,k12_lopclset(X0))
| ~ l3_lattices(X0)
| v3_realset2(X0)
| ~ v17_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f530]) ).
fof(f581,plain,
( k12_lopclset(sK0_skl) = k6_lopclset(k11_lopclset(sK0_skl))
| ~ l3_lattices(sK0_skl)
| ~ v17_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f250,f119]) ).
fof(f598,definition,
( sQ11_spl
<=> v3_struct_0(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f599,plain,
( ~ sQ11_spl
| v3_struct_0(sK0_skl) ),
inference(component_clause,[status(thm)],[f598]) ).
fof(f601,definition,
( sQ12_spl
<=> v10_lattices(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f603,plain,
( sQ12_spl
| ~ v10_lattices(sK0_skl) ),
inference(component_clause,[status(thm)],[f601]) ).
fof(f604,definition,
( sQ13_spl
<=> v17_lattices(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f606,plain,
( sQ13_spl
| ~ v17_lattices(sK0_skl) ),
inference(component_clause,[status(thm)],[f604]) ).
fof(f607,definition,
( sQ14_spl
<=> l3_lattices(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f609,plain,
( sQ14_spl
| ~ l3_lattices(sK0_skl) ),
inference(component_clause,[status(thm)],[f607]) ).
fof(f610,definition,
( sQ15_spl
<=> k12_lopclset(sK0_skl) = k6_lopclset(k11_lopclset(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f611,plain,
( ~ sQ15_spl
| k12_lopclset(sK0_skl) = k6_lopclset(k11_lopclset(sK0_skl)) ),
inference(component_clause,[status(thm)],[f610]) ).
fof(f613,plain,
( sQ15_spl
| ~ sQ14_spl
| ~ sQ13_spl
| ~ sQ12_spl
| sQ11_spl ),
inference(split_clause,[status(thm)],[f581,f598,f601,f604,f607,f610]) ).
fof(f614,plain,
( sQ14_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f609,f120]) ).
fof(f615,plain,
sQ14_spl,
inference(contradiction_clause,[status(thm)],[f614]) ).
fof(f616,plain,
( sQ13_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f606,f118]) ).
fof(f617,plain,
sQ13_spl,
inference(contradiction_clause,[status(thm)],[f616]) ).
fof(f618,plain,
( sQ12_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f603,f117]) ).
fof(f619,plain,
sQ12_spl,
inference(contradiction_clause,[status(thm)],[f618]) ).
fof(f620,plain,
( ~ sQ11_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f599,f116]) ).
fof(f621,plain,
~ sQ11_spl,
inference(contradiction_clause,[status(thm)],[f620]) ).
fof(f625,plain,
( ~ sQ15_spl
| ~ r1_filter_1(sK0_skl,k12_lopclset(sK0_skl))
| ~ l1_pre_topc(k11_lopclset(sK0_skl))
| ~ v2_pre_topc(k11_lopclset(sK0_skl))
| v3_struct_0(k11_lopclset(sK0_skl)) ),
inference(paramodulation,[status(thm)],[f611,f121]) ).
fof(f626,definition,
( sQ16_spl
<=> v3_struct_0(k11_lopclset(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f627,plain,
( ~ sQ16_spl
| v3_struct_0(k11_lopclset(sK0_skl)) ),
inference(component_clause,[status(thm)],[f626]) ).
fof(f629,definition,
( sQ17_spl
<=> v2_pre_topc(k11_lopclset(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f631,plain,
( sQ17_spl
| ~ v2_pre_topc(k11_lopclset(sK0_skl)) ),
inference(component_clause,[status(thm)],[f629]) ).
fof(f632,definition,
( sQ18_spl
<=> l1_pre_topc(k11_lopclset(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f634,plain,
( sQ18_spl
| ~ l1_pre_topc(k11_lopclset(sK0_skl)) ),
inference(component_clause,[status(thm)],[f632]) ).
fof(f647,definition,
( sQ22_spl
<=> r1_filter_1(sK0_skl,k12_lopclset(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f649,plain,
( sQ22_spl
| ~ r1_filter_1(sK0_skl,k12_lopclset(sK0_skl)) ),
inference(component_clause,[status(thm)],[f647]) ).
fof(f650,plain,
( ~ sQ15_spl
| ~ sQ22_spl
| ~ sQ18_spl
| ~ sQ17_spl
| sQ16_spl ),
inference(split_clause,[status(thm)],[f625,f626,f629,f632,f647,f610]) ).
fof(f692,plain,
( sQ17_spl
| ~ l3_lattices(sK0_skl)
| v3_realset2(sK0_skl)
| ~ v17_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f631,f259]) ).
fof(f693,definition,
( sQ32_spl
<=> v3_realset2(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f694,plain,
( ~ sQ32_spl
| v3_realset2(sK0_skl) ),
inference(component_clause,[status(thm)],[f693]) ).
fof(f696,plain,
( sQ17_spl
| ~ sQ14_spl
| sQ32_spl
| ~ sQ13_spl
| ~ sQ12_spl
| sQ11_spl ),
inference(split_clause,[status(thm)],[f692,f598,f601,f604,f693,f607,f629]) ).
fof(f697,plain,
( ~ sQ32_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f694,f119]) ).
fof(f698,plain,
~ sQ32_spl,
inference(contradiction_clause,[status(thm)],[f697]) ).
fof(f704,plain,
( sQ22_spl
| ~ l3_lattices(sK0_skl)
| v3_realset2(sK0_skl)
| ~ v17_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f649,f531]) ).
fof(f705,plain,
( sQ22_spl
| ~ sQ14_spl
| sQ32_spl
| ~ sQ13_spl
| ~ sQ12_spl
| sQ11_spl ),
inference(split_clause,[status(thm)],[f704,f598,f601,f604,f693,f607,f647]) ).
fof(f707,definition,
( sQ34_spl
<=> v3_realset2(sK16_skl) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f708,plain,
( ~ sQ34_spl
| v3_realset2(sK16_skl) ),
inference(component_clause,[status(thm)],[f707]) ).
fof(f711,plain,
( ~ sQ34_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f708,f442]) ).
fof(f712,plain,
~ sQ34_spl,
inference(contradiction_clause,[status(thm)],[f711]) ).
fof(f725,plain,
( sQ18_spl
| ~ l3_lattices(sK0_skl)
| v3_realset2(sK0_skl)
| ~ v17_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f260,f634]) ).
fof(f727,plain,
( sQ18_spl
| ~ sQ14_spl
| sQ32_spl
| ~ sQ13_spl
| ~ sQ12_spl
| sQ11_spl ),
inference(split_clause,[status(thm)],[f725,f598,f601,f604,f693,f607,f632]) ).
fof(f792,definition,
( sQ47_spl
<=> v10_lattices(sK12_skl) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f794,plain,
( sQ47_spl
| ~ v10_lattices(sK12_skl) ),
inference(component_clause,[status(thm)],[f792]) ).
fof(f796,definition,
( sQ48_spl
<=> v10_lattices(sK11_skl) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f798,plain,
( sQ48_spl
| ~ v10_lattices(sK11_skl) ),
inference(component_clause,[status(thm)],[f796]) ).
fof(f800,definition,
( sQ49_spl
<=> v10_lattices(sK10_skl) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f802,plain,
( sQ49_spl
| ~ v10_lattices(sK10_skl) ),
inference(component_clause,[status(thm)],[f800]) ).
fof(f806,plain,
( sQ49_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f802,f366]) ).
fof(f807,plain,
sQ49_spl,
inference(contradiction_clause,[status(thm)],[f806]) ).
fof(f808,plain,
( sQ48_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f798,f381]) ).
fof(f809,plain,
sQ48_spl,
inference(contradiction_clause,[status(thm)],[f808]) ).
fof(f810,plain,
( sQ47_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f794,f395]) ).
fof(f811,plain,
sQ47_spl,
inference(contradiction_clause,[status(thm)],[f810]) ).
fof(f884,definition,
( sQ62_spl
<=> l3_lattices(sK13_skl) ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f886,plain,
( sQ62_spl
| ~ l3_lattices(sK13_skl) ),
inference(component_clause,[status(thm)],[f884]) ).
fof(f891,plain,
( sQ62_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f886,f401]) ).
fof(f892,plain,
sQ62_spl,
inference(contradiction_clause,[status(thm)],[f891]) ).
fof(f924,plain,
( ~ sQ16_spl
| ~ l3_lattices(sK0_skl)
| v3_realset2(sK0_skl)
| ~ v17_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f331,f627]) ).
fof(f926,plain,
( ~ sQ16_spl
| ~ sQ14_spl
| sQ32_spl
| ~ sQ13_spl
| ~ sQ12_spl
| sQ11_spl ),
inference(split_clause,[status(thm)],[f924,f598,f601,f604,f693,f607,f626]) ).
fof(f927,plain,
$false,
inference(sat_refutation,[status(thm)],[f613,f615,f617,f619,f621,f650,f696,f698,f705,f712,f727,f807,f809,f811,f892,f926]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LAT292+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.07 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.20/0.46 % Computer : n018.cluster.edu
% 0.20/0.46 % Model : x86_64 x86_64
% 0.20/0.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/0.46 % Memory : 8046.5625MB
% 0.20/0.46 % OS : Linux 6.8.0-71-generic
% 0.20/0.46 % CPULimit : 300
% 0.20/0.46 % WCLimit : 300
% 0.20/0.46 % DateTime : Sun Sep 20 23:29:13 UTC 2026
% 0.20/0.46 % CPUTime :
% 0.20/0.49 % Drodi V4.1.1
% 0.20/0.51 % Refutation found
% 0.20/0.51 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.20/0.51 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.24/0.58 % Elapsed time: 0.110271 seconds
% 0.24/0.58 % CPU time: 0.179063 seconds
% 0.24/0.58 % Total memory used: 26.815 MB
% 0.24/0.58 % Net memory used: 26.774 MB
%------------------------------------------------------------------------------