%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LAT347+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 : 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:52 PM UTC 2026
% Result : Theorem 2.06s 0.74s
% Output : CNFRefutation 2.06s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 30
% Syntax : Number of formulae : 129 ( 18 unt; 19 def)
% Number of atoms : 410 ( 27 equ)
% Maximal formula atoms : 12 ( 3 avg)
% Number of connectives : 461 ( 180 ~; 182 |; 64 &)
% ( 19 <=>; 16 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 4 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 34 ( 32 usr; 20 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 2 con; 0-2 aty)
% Number of variables : 44 ( 42 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [A] :
( ( l1_orders_2(A)
& v2_lattice3(A)
& v2_yellow_0(A)
& v4_orders_2(A)
& v3_orders_2(A)
& v2_orders_2(A) )
=> ! [B] :
( ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(k2_yellow_1(k9_waybel_0(A)))))
& v1_waybel_0(B,k2_yellow_1(k9_waybel_0(A)))
& ~ v1_xboole_0(B) )
=> k1_yellow_0(k2_yellow_1(k9_waybel_0(A)),B) = k3_tarski(B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
~ ! [A] :
( ( l1_orders_2(A)
& v2_lattice3(A)
& v2_yellow_0(A)
& v4_orders_2(A)
& v3_orders_2(A)
& v2_orders_2(A) )
=> ! [B] :
( ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(k2_yellow_1(k9_waybel_0(A)))))
& v1_waybel_0(B,k2_yellow_1(k9_waybel_0(A)))
& ~ v1_xboole_0(B) )
=> k1_yellow_0(k2_yellow_1(k9_waybel_0(A)),B) = k3_tarski(B) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f15,axiom,
! [A] :
( l1_orders_2(A)
=> ( v2_lattice3(A)
=> ~ v3_struct_0(A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f21,axiom,
! [A] :
( ( l1_orders_2(A)
& v3_orders_2(A)
& v2_orders_2(A)
& ~ v3_struct_0(A) )
=> k9_waybel_0(A) = a_1_1_waybel_0(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f32,axiom,
! [A] :
( l1_orders_2(A)
=> ( l1_orders_2(k7_lattice3(A))
& v1_orders_2(k7_lattice3(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f48,axiom,
! [A] :
( ( l1_orders_2(A)
& v2_yellow_0(A) )
=> ( v1_yellow_0(k7_lattice3(A))
& v1_orders_2(k7_lattice3(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f53,axiom,
! [A] :
( ( l1_orders_2(A)
& v2_orders_2(A) )
=> ( v2_orders_2(k7_lattice3(A))
& v1_orders_2(k7_lattice3(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f55,axiom,
! [A] :
( ( l1_orders_2(A)
& v3_orders_2(A) )
=> ( v3_orders_2(k7_lattice3(A))
& v1_orders_2(k7_lattice3(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f57,axiom,
! [A] :
( ( l1_orders_2(A)
& v4_orders_2(A) )
=> ( v4_orders_2(k7_lattice3(A))
& v1_orders_2(k7_lattice3(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f62,axiom,
! [A] :
( ( l1_orders_2(A)
& v2_lattice3(A) )
=> ( v1_lattice3(k7_lattice3(A))
& v1_orders_2(k7_lattice3(A))
& ~ v3_struct_0(k7_lattice3(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f106,axiom,
! [A] :
( ( l1_orders_2(A)
& v3_orders_2(A)
& v2_orders_2(A)
& ~ v3_struct_0(A) )
=> k9_waybel_0(A) = k8_waybel_0(k7_lattice3(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f108,axiom,
! [A] :
( ( l1_orders_2(A)
& v1_yellow_0(A)
& v1_lattice3(A)
& v4_orders_2(A)
& v3_orders_2(A)
& v2_orders_2(A) )
=> ! [B] :
( ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(k2_yellow_1(k8_waybel_0(A)))))
& v1_waybel_0(B,k2_yellow_1(k8_waybel_0(A)))
& ~ v1_xboole_0(B) )
=> k1_yellow_0(k2_yellow_1(k8_waybel_0(A)),B) = k3_tarski(B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f109,plain,
? [A] :
( ? [B] :
( k1_yellow_0(k2_yellow_1(k9_waybel_0(A)),B) != k3_tarski(B)
& m1_subset_1(B,k1_zfmisc_1(u1_struct_0(k2_yellow_1(k9_waybel_0(A)))))
& v1_waybel_0(B,k2_yellow_1(k9_waybel_0(A)))
& ~ v1_xboole_0(B) )
& l1_orders_2(A)
& v2_lattice3(A)
& v2_yellow_0(A)
& v4_orders_2(A)
& v3_orders_2(A)
& v2_orders_2(A) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f110,plain,
( k1_yellow_0(k2_yellow_1(k9_waybel_0(sK0_skl)),sK1_skl) != k3_tarski(sK1_skl)
& m1_subset_1(sK1_skl,k1_zfmisc_1(u1_struct_0(k2_yellow_1(k9_waybel_0(sK0_skl)))))
& v1_waybel_0(sK1_skl,k2_yellow_1(k9_waybel_0(sK0_skl)))
& ~ v1_xboole_0(sK1_skl)
& l1_orders_2(sK0_skl)
& v2_lattice3(sK0_skl)
& v2_yellow_0(sK0_skl)
& v4_orders_2(sK0_skl)
& v3_orders_2(sK0_skl)
& v2_orders_2(sK0_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(A,sK0_skl),skolemize(B,sK1_skl)],[f109]) ).
fof(f111,plain,
v2_orders_2(sK0_skl),
inference(cnf_transformation,[status(thm)],[f110]) ).
fof(f112,plain,
v3_orders_2(sK0_skl),
inference(cnf_transformation,[status(thm)],[f110]) ).
fof(f113,plain,
v4_orders_2(sK0_skl),
inference(cnf_transformation,[status(thm)],[f110]) ).
fof(f114,plain,
v2_yellow_0(sK0_skl),
inference(cnf_transformation,[status(thm)],[f110]) ).
fof(f115,plain,
v2_lattice3(sK0_skl),
inference(cnf_transformation,[status(thm)],[f110]) ).
fof(f116,plain,
l1_orders_2(sK0_skl),
inference(cnf_transformation,[status(thm)],[f110]) ).
fof(f117,plain,
~ v1_xboole_0(sK1_skl),
inference(cnf_transformation,[status(thm)],[f110]) ).
fof(f118,plain,
v1_waybel_0(sK1_skl,k2_yellow_1(k9_waybel_0(sK0_skl))),
inference(cnf_transformation,[status(thm)],[f110]) ).
fof(f119,plain,
m1_subset_1(sK1_skl,k1_zfmisc_1(u1_struct_0(k2_yellow_1(k9_waybel_0(sK0_skl))))),
inference(cnf_transformation,[status(thm)],[f110]) ).
fof(f120,plain,
k1_yellow_0(k2_yellow_1(k9_waybel_0(sK0_skl)),sK1_skl) != k3_tarski(sK1_skl),
inference(cnf_transformation,[status(thm)],[f110]) ).
fof(f171,plain,
! [A] :
( ~ v3_struct_0(A)
| ~ v2_lattice3(A)
| ~ l1_orders_2(A) ),
inference(pre_NNF_transformation,[status(thm)],[f15]) ).
fof(f172,plain,
! [X0] :
( ~ v3_struct_0(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f171]) ).
fof(f188,plain,
! [A] :
( k9_waybel_0(A) = a_1_1_waybel_0(A)
| ~ l1_orders_2(A)
| ~ v3_orders_2(A)
| ~ v2_orders_2(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f21]) ).
fof(f189,plain,
! [X0] :
( k9_waybel_0(X0) = a_1_1_waybel_0(X0)
| ~ l1_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f188]) ).
fof(f205,plain,
! [A] :
( ( l1_orders_2(k7_lattice3(A))
& v1_orders_2(k7_lattice3(A)) )
| ~ l1_orders_2(A) ),
inference(pre_NNF_transformation,[status(thm)],[f32]) ).
fof(f207,plain,
! [X0] :
( l1_orders_2(k7_lattice3(X0))
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f205]) ).
fof(f229,plain,
! [A] :
( ( v1_yellow_0(k7_lattice3(A))
& v1_orders_2(k7_lattice3(A)) )
| ~ l1_orders_2(A)
| ~ v2_yellow_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f48]) ).
fof(f231,plain,
! [X0] :
( v1_yellow_0(k7_lattice3(X0))
| ~ l1_orders_2(X0)
| ~ v2_yellow_0(X0) ),
inference(cnf_transformation,[status(thm)],[f229]) ).
fof(f238,plain,
! [A] :
( ( v2_orders_2(k7_lattice3(A))
& v1_orders_2(k7_lattice3(A)) )
| ~ l1_orders_2(A)
| ~ v2_orders_2(A) ),
inference(pre_NNF_transformation,[status(thm)],[f53]) ).
fof(f240,plain,
! [X0] :
( v2_orders_2(k7_lattice3(X0))
| ~ l1_orders_2(X0)
| ~ v2_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f238]) ).
fof(f252,plain,
! [A] :
( ( v3_orders_2(k7_lattice3(A))
& v1_orders_2(k7_lattice3(A)) )
| ~ l1_orders_2(A)
| ~ v3_orders_2(A) ),
inference(pre_NNF_transformation,[status(thm)],[f55]) ).
fof(f254,plain,
! [X0] :
( v3_orders_2(k7_lattice3(X0))
| ~ l1_orders_2(X0)
| ~ v3_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f252]) ).
fof(f258,plain,
! [A] :
( ( v4_orders_2(k7_lattice3(A))
& v1_orders_2(k7_lattice3(A)) )
| ~ l1_orders_2(A)
| ~ v4_orders_2(A) ),
inference(pre_NNF_transformation,[status(thm)],[f57]) ).
fof(f260,plain,
! [X0] :
( v4_orders_2(k7_lattice3(X0))
| ~ l1_orders_2(X0)
| ~ v4_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f258]) ).
fof(f275,plain,
! [A] :
( ( v1_lattice3(k7_lattice3(A))
& v1_orders_2(k7_lattice3(A))
& ~ v3_struct_0(k7_lattice3(A)) )
| ~ l1_orders_2(A)
| ~ v2_lattice3(A) ),
inference(pre_NNF_transformation,[status(thm)],[f62]) ).
fof(f278,plain,
! [X0] :
( v1_lattice3(k7_lattice3(X0))
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0) ),
inference(cnf_transformation,[status(thm)],[f275]) ).
fof(f481,plain,
! [A] :
( k9_waybel_0(A) = k8_waybel_0(k7_lattice3(A))
| ~ l1_orders_2(A)
| ~ v3_orders_2(A)
| ~ v2_orders_2(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f106]) ).
fof(f482,plain,
! [X0] :
( k9_waybel_0(X0) = k8_waybel_0(k7_lattice3(X0))
| ~ l1_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f481]) ).
fof(f486,plain,
! [A] :
( ! [B] :
( k1_yellow_0(k2_yellow_1(k8_waybel_0(A)),B) = k3_tarski(B)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(k2_yellow_1(k8_waybel_0(A)))))
| ~ v1_waybel_0(B,k2_yellow_1(k8_waybel_0(A)))
| v1_xboole_0(B) )
| ~ l1_orders_2(A)
| ~ v1_yellow_0(A)
| ~ v1_lattice3(A)
| ~ v4_orders_2(A)
| ~ v3_orders_2(A)
| ~ v2_orders_2(A) ),
inference(pre_NNF_transformation,[status(thm)],[f108]) ).
fof(f487,plain,
! [X0,X1] :
( k1_yellow_0(k2_yellow_1(k8_waybel_0(X0)),X1) = k3_tarski(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(k2_yellow_1(k8_waybel_0(X0)))))
| ~ v1_waybel_0(X1,k2_yellow_1(k8_waybel_0(X0)))
| v1_xboole_0(X1)
| ~ l1_orders_2(X0)
| ~ v1_yellow_0(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f486]) ).
fof(f544,plain,
( k9_waybel_0(sK0_skl) = a_1_1_waybel_0(sK0_skl)
| ~ l1_orders_2(sK0_skl)
| ~ v3_orders_2(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f189,f111]) ).
fof(f576,definition,
( sQ15_spl
<=> v3_struct_0(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f577,plain,
( ~ sQ15_spl
| v3_struct_0(sK0_skl) ),
inference(component_clause,[status(thm)],[f576]) ).
fof(f579,definition,
( sQ16_spl
<=> v3_orders_2(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f581,plain,
( sQ16_spl
| ~ v3_orders_2(sK0_skl) ),
inference(component_clause,[status(thm)],[f579]) ).
fof(f582,definition,
( sQ17_spl
<=> l1_orders_2(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f584,plain,
( sQ17_spl
| ~ l1_orders_2(sK0_skl) ),
inference(component_clause,[status(thm)],[f582]) ).
fof(f585,definition,
( sQ18_spl
<=> k9_waybel_0(sK0_skl) = a_1_1_waybel_0(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f586,plain,
( ~ sQ18_spl
| k9_waybel_0(sK0_skl) = a_1_1_waybel_0(sK0_skl) ),
inference(component_clause,[status(thm)],[f585]) ).
fof(f588,plain,
( sQ18_spl
| ~ sQ17_spl
| ~ sQ16_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f544,f576,f579,f582,f585]) ).
fof(f589,plain,
( ~ sQ18_spl
| k1_yellow_0(k2_yellow_1(a_1_1_waybel_0(sK0_skl)),sK1_skl) != k3_tarski(sK1_skl) ),
inference(backward_demodulation,[status(thm)],[f586,f120]) ).
fof(f590,plain,
( ~ sQ18_spl
| m1_subset_1(sK1_skl,k1_zfmisc_1(u1_struct_0(k2_yellow_1(a_1_1_waybel_0(sK0_skl))))) ),
inference(backward_demodulation,[status(thm)],[f586,f119]) ).
fof(f591,plain,
( ~ sQ18_spl
| v1_waybel_0(sK1_skl,k2_yellow_1(a_1_1_waybel_0(sK0_skl))) ),
inference(backward_demodulation,[status(thm)],[f586,f118]) ).
fof(f592,plain,
( sQ17_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f584,f116]) ).
fof(f593,plain,
sQ17_spl,
inference(contradiction_clause,[status(thm)],[f592]) ).
fof(f594,plain,
( sQ16_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f581,f112]) ).
fof(f595,plain,
sQ16_spl,
inference(contradiction_clause,[status(thm)],[f594]) ).
fof(f625,plain,
( ~ sQ15_spl
| ~ v2_lattice3(sK0_skl)
| ~ l1_orders_2(sK0_skl) ),
inference(resolution,[status(thm)],[f577,f172]) ).
fof(f630,definition,
( sQ24_spl
<=> v2_lattice3(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f632,plain,
( sQ24_spl
| ~ v2_lattice3(sK0_skl) ),
inference(component_clause,[status(thm)],[f630]) ).
fof(f633,plain,
( ~ sQ15_spl
| ~ sQ24_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f625,f582,f630,f576]) ).
fof(f634,plain,
( sQ24_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f632,f115]) ).
fof(f635,plain,
sQ24_spl,
inference(contradiction_clause,[status(thm)],[f634]) ).
fof(f642,definition,
( sQ26_spl
<=> v2_orders_2(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f644,plain,
( sQ26_spl
| ~ v2_orders_2(sK0_skl) ),
inference(component_clause,[status(thm)],[f642]) ).
fof(f645,definition,
( sQ27_spl
<=> v4_orders_2(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f647,plain,
( sQ27_spl
| ~ v4_orders_2(sK0_skl) ),
inference(component_clause,[status(thm)],[f645]) ).
fof(f648,definition,
( sQ28_spl
<=> v2_yellow_0(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f650,plain,
( sQ28_spl
| ~ v2_yellow_0(sK0_skl) ),
inference(component_clause,[status(thm)],[f648]) ).
fof(f655,plain,
( sQ28_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f650,f114]) ).
fof(f656,plain,
sQ28_spl,
inference(contradiction_clause,[status(thm)],[f655]) ).
fof(f657,plain,
( sQ27_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f647,f113]) ).
fof(f658,plain,
sQ27_spl,
inference(contradiction_clause,[status(thm)],[f657]) ).
fof(f659,plain,
( sQ26_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f644,f111]) ).
fof(f660,plain,
sQ26_spl,
inference(contradiction_clause,[status(thm)],[f659]) ).
fof(f2717,plain,
( k9_waybel_0(sK0_skl) = k8_waybel_0(k7_lattice3(sK0_skl))
| ~ v3_orders_2(sK0_skl)
| ~ v2_orders_2(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f482,f116]) ).
fof(f2738,definition,
( sQ352_spl
<=> k9_waybel_0(sK0_skl) = k8_waybel_0(k7_lattice3(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ352_spl])],[split_symbol_definition]) ).
fof(f2739,plain,
( ~ sQ352_spl
| k9_waybel_0(sK0_skl) = k8_waybel_0(k7_lattice3(sK0_skl)) ),
inference(component_clause,[status(thm)],[f2738]) ).
fof(f2741,plain,
( sQ352_spl
| ~ sQ16_spl
| ~ sQ26_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f2717,f576,f642,f579,f2738]) ).
fof(f2742,plain,
( ~ sQ352_spl
| ~ sQ18_spl
| a_1_1_waybel_0(sK0_skl) = k8_waybel_0(k7_lattice3(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f586,f2739]) ).
fof(f2755,plain,
! [X0] :
( ~ sQ352_spl
| ~ sQ18_spl
| k1_yellow_0(k2_yellow_1(k8_waybel_0(k7_lattice3(sK0_skl))),X0) = k3_tarski(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k2_yellow_1(k8_waybel_0(k7_lattice3(sK0_skl))))))
| ~ v1_waybel_0(X0,k2_yellow_1(a_1_1_waybel_0(sK0_skl)))
| v1_xboole_0(X0)
| ~ l1_orders_2(k7_lattice3(sK0_skl))
| ~ v1_yellow_0(k7_lattice3(sK0_skl))
| ~ v1_lattice3(k7_lattice3(sK0_skl))
| ~ v4_orders_2(k7_lattice3(sK0_skl))
| ~ v3_orders_2(k7_lattice3(sK0_skl))
| ~ v2_orders_2(k7_lattice3(sK0_skl)) ),
inference(paramodulation,[status(thm)],[f2742,f487]) ).
fof(f2762,definition,
( sQ355_spl
<=> v2_orders_2(k7_lattice3(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ355_spl])],[split_symbol_definition]) ).
fof(f2764,plain,
( sQ355_spl
| ~ v2_orders_2(k7_lattice3(sK0_skl)) ),
inference(component_clause,[status(thm)],[f2762]) ).
fof(f2765,definition,
( sQ356_spl
<=> v3_orders_2(k7_lattice3(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ356_spl])],[split_symbol_definition]) ).
fof(f2767,plain,
( sQ356_spl
| ~ v3_orders_2(k7_lattice3(sK0_skl)) ),
inference(component_clause,[status(thm)],[f2765]) ).
fof(f2768,definition,
( sQ357_spl
<=> v4_orders_2(k7_lattice3(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ357_spl])],[split_symbol_definition]) ).
fof(f2770,plain,
( sQ357_spl
| ~ v4_orders_2(k7_lattice3(sK0_skl)) ),
inference(component_clause,[status(thm)],[f2768]) ).
fof(f2771,definition,
( sQ358_spl
<=> v1_lattice3(k7_lattice3(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ358_spl])],[split_symbol_definition]) ).
fof(f2773,plain,
( sQ358_spl
| ~ v1_lattice3(k7_lattice3(sK0_skl)) ),
inference(component_clause,[status(thm)],[f2771]) ).
fof(f2774,definition,
( sQ359_spl
<=> v1_yellow_0(k7_lattice3(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ359_spl])],[split_symbol_definition]) ).
fof(f2776,plain,
( sQ359_spl
| ~ v1_yellow_0(k7_lattice3(sK0_skl)) ),
inference(component_clause,[status(thm)],[f2774]) ).
fof(f2777,definition,
( sQ360_spl
<=> l1_orders_2(k7_lattice3(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ360_spl])],[split_symbol_definition]) ).
fof(f2779,plain,
( sQ360_spl
| ~ l1_orders_2(k7_lattice3(sK0_skl)) ),
inference(component_clause,[status(thm)],[f2777]) ).
fof(f2842,definition,
! [X0] :
( sQ379_spl
<=> ( k1_yellow_0(k2_yellow_1(k8_waybel_0(k7_lattice3(sK0_skl))),X0) = k3_tarski(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k2_yellow_1(k8_waybel_0(k7_lattice3(sK0_skl))))))
| ~ v1_waybel_0(X0,k2_yellow_1(a_1_1_waybel_0(sK0_skl)))
| v1_xboole_0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ379_spl])],[split_symbol_definition]) ).
fof(f2843,plain,
! [X0] :
( ~ sQ379_spl
| k1_yellow_0(k2_yellow_1(k8_waybel_0(k7_lattice3(sK0_skl))),X0) = k3_tarski(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k2_yellow_1(k8_waybel_0(k7_lattice3(sK0_skl))))))
| ~ v1_waybel_0(X0,k2_yellow_1(a_1_1_waybel_0(sK0_skl)))
| v1_xboole_0(X0) ),
inference(component_clause,[status(thm)],[f2842]) ).
fof(f2845,plain,
( ~ sQ352_spl
| ~ sQ18_spl
| sQ379_spl
| ~ sQ360_spl
| ~ sQ359_spl
| ~ sQ358_spl
| ~ sQ357_spl
| ~ sQ356_spl
| ~ sQ355_spl ),
inference(split_clause,[status(thm)],[f2755,f2762,f2765,f2768,f2771,f2774,f2777,f2842,f585,f2738]) ).
fof(f2860,plain,
! [X0] :
( ~ sQ379_spl
| ~ sQ352_spl
| ~ sQ18_spl
| k1_yellow_0(k2_yellow_1(k8_waybel_0(k7_lattice3(sK0_skl))),X0) = k3_tarski(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k2_yellow_1(a_1_1_waybel_0(sK0_skl)))))
| ~ v1_waybel_0(X0,k2_yellow_1(a_1_1_waybel_0(sK0_skl)))
| v1_xboole_0(X0) ),
inference(forward_demodulation,[status(thm)],[f2742,f2843]) ).
fof(f2861,plain,
! [X0] :
( ~ sQ379_spl
| ~ sQ352_spl
| ~ sQ18_spl
| k1_yellow_0(k2_yellow_1(a_1_1_waybel_0(sK0_skl)),X0) = k3_tarski(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k2_yellow_1(a_1_1_waybel_0(sK0_skl)))))
| ~ v1_waybel_0(X0,k2_yellow_1(a_1_1_waybel_0(sK0_skl)))
| v1_xboole_0(X0) ),
inference(forward_demodulation,[status(thm)],[f2742,f2860]) ).
fof(f2902,plain,
( sQ360_spl
| ~ l1_orders_2(sK0_skl) ),
inference(resolution,[status(thm)],[f2779,f207]) ).
fof(f2903,plain,
( sQ360_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f2902,f582,f2777]) ).
fof(f2904,plain,
( sQ356_spl
| ~ l1_orders_2(sK0_skl)
| ~ v3_orders_2(sK0_skl) ),
inference(resolution,[status(thm)],[f2767,f254]) ).
fof(f2905,plain,
( sQ356_spl
| ~ sQ17_spl
| ~ sQ16_spl ),
inference(split_clause,[status(thm)],[f2904,f579,f582,f2765]) ).
fof(f2906,plain,
( sQ355_spl
| ~ l1_orders_2(sK0_skl)
| ~ v2_orders_2(sK0_skl) ),
inference(resolution,[status(thm)],[f2764,f240]) ).
fof(f2907,plain,
( sQ355_spl
| ~ sQ17_spl
| ~ sQ26_spl ),
inference(split_clause,[status(thm)],[f2906,f642,f582,f2762]) ).
fof(f2909,plain,
( sQ359_spl
| ~ l1_orders_2(sK0_skl)
| ~ v2_yellow_0(sK0_skl) ),
inference(resolution,[status(thm)],[f2776,f231]) ).
fof(f2913,plain,
( sQ359_spl
| ~ sQ17_spl
| ~ sQ28_spl ),
inference(split_clause,[status(thm)],[f2909,f648,f582,f2774]) ).
fof(f2923,plain,
( sQ358_spl
| ~ l1_orders_2(sK0_skl)
| ~ v2_lattice3(sK0_skl) ),
inference(resolution,[status(thm)],[f2773,f278]) ).
fof(f2927,plain,
( sQ358_spl
| ~ sQ17_spl
| ~ sQ24_spl ),
inference(split_clause,[status(thm)],[f2923,f630,f582,f2771]) ).
fof(f2936,plain,
( sQ357_spl
| ~ l1_orders_2(sK0_skl)
| ~ v4_orders_2(sK0_skl) ),
inference(resolution,[status(thm)],[f2770,f260]) ).
fof(f2937,plain,
( sQ357_spl
| ~ sQ17_spl
| ~ sQ27_spl ),
inference(split_clause,[status(thm)],[f2936,f645,f582,f2768]) ).
fof(f3072,plain,
( ~ sQ18_spl
| ~ sQ379_spl
| ~ sQ352_spl
| ~ m1_subset_1(sK1_skl,k1_zfmisc_1(u1_struct_0(k2_yellow_1(a_1_1_waybel_0(sK0_skl)))))
| ~ v1_waybel_0(sK1_skl,k2_yellow_1(a_1_1_waybel_0(sK0_skl)))
| v1_xboole_0(sK1_skl) ),
inference(resolution,[status(thm)],[f2861,f589]) ).
fof(f3073,definition,
( sQ402_spl
<=> v1_xboole_0(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ402_spl])],[split_symbol_definition]) ).
fof(f3074,plain,
( ~ sQ402_spl
| v1_xboole_0(sK1_skl) ),
inference(component_clause,[status(thm)],[f3073]) ).
fof(f3076,definition,
( sQ403_spl
<=> v1_waybel_0(sK1_skl,k2_yellow_1(a_1_1_waybel_0(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ403_spl])],[split_symbol_definition]) ).
fof(f3078,plain,
( sQ403_spl
| ~ v1_waybel_0(sK1_skl,k2_yellow_1(a_1_1_waybel_0(sK0_skl))) ),
inference(component_clause,[status(thm)],[f3076]) ).
fof(f3079,definition,
( sQ404_spl
<=> m1_subset_1(sK1_skl,k1_zfmisc_1(u1_struct_0(k2_yellow_1(a_1_1_waybel_0(sK0_skl))))) ),
introduced(definition,[new_symbols(definition,[sQ404_spl])],[split_symbol_definition]) ).
fof(f3081,plain,
( sQ404_spl
| ~ m1_subset_1(sK1_skl,k1_zfmisc_1(u1_struct_0(k2_yellow_1(a_1_1_waybel_0(sK0_skl))))) ),
inference(component_clause,[status(thm)],[f3079]) ).
fof(f3082,plain,
( ~ sQ18_spl
| ~ sQ379_spl
| ~ sQ352_spl
| ~ sQ404_spl
| ~ sQ403_spl
| sQ402_spl ),
inference(split_clause,[status(thm)],[f3072,f3073,f3076,f3079,f2738,f2842,f585]) ).
fof(f3083,plain,
( sQ404_spl
| ~ sQ18_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3081,f590]) ).
fof(f3084,plain,
( sQ404_spl
| ~ sQ18_spl ),
inference(contradiction_clause,[status(thm)],[f3083]) ).
fof(f3085,plain,
( sQ403_spl
| ~ sQ18_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3078,f591]) ).
fof(f3086,plain,
( sQ403_spl
| ~ sQ18_spl ),
inference(contradiction_clause,[status(thm)],[f3085]) ).
fof(f3087,plain,
( ~ sQ402_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3074,f117]) ).
fof(f3088,plain,
~ sQ402_spl,
inference(contradiction_clause,[status(thm)],[f3087]) ).
fof(f3089,plain,
$false,
inference(sat_refutation,[status(thm)],[f588,f593,f595,f633,f635,f656,f658,f660,f2741,f2845,f2903,f2905,f2907,f2913,f2927,f2937,f3082,f3084,f3086,f3088]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT347+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n005.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Sun Sep 20 23:45:18 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.37 % Drodi V4.1.1
% 2.06/0.74 % Refutation found
% 2.06/0.74 % SZS status Theorem for theBenchmark: Theorem is valid
% 2.06/0.74 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 2.06/0.76 % Elapsed time: 0.397881 seconds
% 2.06/0.76 % CPU time: 2.841726 seconds
% 2.06/0.76 % Total memory used: 143.233 MB
% 2.06/0.76 % Net memory used: 140.752 MB
%------------------------------------------------------------------------------