%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LAT353+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 : n009.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:53 PM UTC 2026
% Result : Theorem 0.10s 0.44s
% Output : CNFRefutation 0.10s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 42
% Syntax : Number of formulae : 199 ( 42 unt; 32 def)
% Number of atoms : 1032 ( 20 equ)
% Maximal formula atoms : 36 ( 5 avg)
% Number of connectives : 1431 ( 598 ~; 625 |; 143 &)
% ( 39 <=>; 26 =>; 0 <=; 0 <~>)
% Maximal formula depth : 40 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 55 ( 53 usr; 33 prp; 0-3 aty)
% Number of functors : 12 ( 12 usr; 4 con; 0-4 aty)
% Number of variables : 142 ( 137 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [A] :
( ( l1_orders_2(A)
& v3_lattice3(A)
& v2_lattice3(A)
& v1_lattice3(A)
& v4_orders_2(A)
& v3_orders_2(A)
& v2_orders_2(A) )
=> ! [B] :
( ( l1_orders_2(B)
& v3_lattice3(B)
& v2_lattice3(B)
& v1_lattice3(B)
& v4_orders_2(B)
& v3_orders_2(B)
& v2_orders_2(B) )
=> ! [C] :
( ( m2_relset_1(C,u1_struct_0(B),u1_struct_0(A))
& v18_waybel_0(C,B,A)
& v1_funct_2(C,u1_struct_0(B),u1_struct_0(A))
& v1_funct_1(C) )
=> ! [D] :
( m1_subset_1(D,u1_struct_0(A))
=> k7_yellow_2(u1_struct_0(A),B,k2_waybel34(A,B,C),D) = k1_yellow_0(B,k5_pre_topc(B,A,C,k6_waybel_0(A,D))) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
~ ! [A] :
( ( l1_orders_2(A)
& v3_lattice3(A)
& v2_lattice3(A)
& v1_lattice3(A)
& v4_orders_2(A)
& v3_orders_2(A)
& v2_orders_2(A) )
=> ! [B] :
( ( l1_orders_2(B)
& v3_lattice3(B)
& v2_lattice3(B)
& v1_lattice3(B)
& v4_orders_2(B)
& v3_orders_2(B)
& v2_orders_2(B) )
=> ! [C] :
( ( m2_relset_1(C,u1_struct_0(B),u1_struct_0(A))
& v18_waybel_0(C,B,A)
& v1_funct_2(C,u1_struct_0(B),u1_struct_0(A))
& v1_funct_1(C) )
=> ! [D] :
( m1_subset_1(D,u1_struct_0(A))
=> k7_yellow_2(u1_struct_0(A),B,k2_waybel34(A,B,C),D) = k1_yellow_0(B,k5_pre_topc(B,A,C,k6_waybel_0(A,D))) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f33,axiom,
! [A] :
( l1_orders_2(A)
=> ( v2_lattice3(A)
=> ~ v3_struct_0(A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f45,axiom,
! [A] :
( ( l1_orders_2(A)
& v2_lattice3(A)
& v1_lattice3(A)
& v4_orders_2(A)
& v3_orders_2(A)
& v2_orders_2(A) )
=> ! [B] :
( ( l1_orders_2(B)
& v2_lattice3(B)
& v1_lattice3(B)
& v4_orders_2(B)
& v3_orders_2(B)
& v2_orders_2(B) )
=> ! [C] :
( ( m2_relset_1(C,u1_struct_0(B),u1_struct_0(A))
& v1_funct_2(C,u1_struct_0(B),u1_struct_0(A))
& v1_funct_1(C) )
=> ( ( v18_waybel_0(C,B,A)
& v3_lattice3(B)
& v3_lattice3(A) )
=> ! [D] :
( ( m2_relset_1(D,u1_struct_0(A),u1_struct_0(B))
& v1_funct_2(D,u1_struct_0(A),u1_struct_0(B))
& v1_funct_1(D) )
=> ( D = k2_waybel34(A,B,C)
<=> v3_waybel_1(k1_waybel_1(A,B,D,C),A,B) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f47,axiom,
! [A] :
( ( l1_orders_2(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,u1_struct_0(A))
=> ! [C] :
( r4_waybel_1(A,B,C)
<=> ( r2_hidden(k1_yellow_0(A,C),C)
& B = k1_yellow_0(A,C)
& r1_yellow_0(A,C) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f57,axiom,
! [A,B,C] :
( ( m1_relset_1(C,u1_struct_0(B),u1_struct_0(A))
& v1_funct_2(C,u1_struct_0(B),u1_struct_0(A))
& v1_funct_1(C)
& l1_orders_2(B)
& v2_lattice3(B)
& v1_lattice3(B)
& v4_orders_2(B)
& v3_orders_2(B)
& v2_orders_2(B)
& l1_orders_2(A)
& v2_lattice3(A)
& v1_lattice3(A)
& v4_orders_2(A)
& v3_orders_2(A)
& v2_orders_2(A) )
=> ( m2_relset_1(k2_waybel34(A,B,C),u1_struct_0(A),u1_struct_0(B))
& v1_funct_2(k2_waybel34(A,B,C),u1_struct_0(A),u1_struct_0(B))
& v1_funct_1(k2_waybel34(A,B,C)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f63,axiom,
! [A,B,C,D] :
( ( m1_subset_1(D,A)
& m1_relset_1(C,A,u1_struct_0(B))
& v1_funct_2(C,A,u1_struct_0(B))
& v1_funct_1(C)
& l1_struct_0(B)
& ~ v3_struct_0(B)
& ~ v1_xboole_0(A) )
=> m1_subset_1(k7_yellow_2(A,B,C,D),u1_struct_0(B)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f64,axiom,
! [A] :
( l1_orders_2(A)
=> l1_struct_0(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f89,axiom,
! [A] :
( ( l1_struct_0(A)
& ~ v3_struct_0(A) )
=> ~ v1_xboole_0(u1_struct_0(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f122,axiom,
! [A,B,C] :
( m2_relset_1(C,A,B)
<=> m1_relset_1(C,A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f124,axiom,
! [A] :
( ( l1_orders_2(A)
& v4_orders_2(A)
& v3_orders_2(A)
& v2_orders_2(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( l1_orders_2(B)
& v4_orders_2(B)
& v3_orders_2(B)
& v2_orders_2(B)
& ~ v3_struct_0(B) )
=> ! [C] :
( ( m2_relset_1(C,u1_struct_0(A),u1_struct_0(B))
& v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
& v1_funct_1(C) )
=> ! [D] :
( ( m2_relset_1(D,u1_struct_0(B),u1_struct_0(A))
& v1_funct_2(D,u1_struct_0(B),u1_struct_0(A))
& v1_funct_1(D) )
=> ( v3_waybel_1(k1_waybel_1(A,B,C,D),A,B)
<=> ( ! [E] :
( m1_subset_1(E,u1_struct_0(A))
=> r4_waybel_1(B,k7_yellow_2(u1_struct_0(A),B,C,E),k5_pre_topc(B,A,D,k6_waybel_0(A,E))) )
& v5_orders_3(D,B,A) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f133,plain,
? [A] :
( ? [B] :
( ? [C] :
( ? [D] :
( k7_yellow_2(u1_struct_0(A),B,k2_waybel34(A,B,C),D) != k1_yellow_0(B,k5_pre_topc(B,A,C,k6_waybel_0(A,D)))
& m1_subset_1(D,u1_struct_0(A)) )
& m2_relset_1(C,u1_struct_0(B),u1_struct_0(A))
& v18_waybel_0(C,B,A)
& v1_funct_2(C,u1_struct_0(B),u1_struct_0(A))
& v1_funct_1(C) )
& l1_orders_2(B)
& v3_lattice3(B)
& v2_lattice3(B)
& v1_lattice3(B)
& v4_orders_2(B)
& v3_orders_2(B)
& v2_orders_2(B) )
& l1_orders_2(A)
& v3_lattice3(A)
& v2_lattice3(A)
& v1_lattice3(A)
& v4_orders_2(A)
& v3_orders_2(A)
& v2_orders_2(A) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f134,plain,
( k7_yellow_2(u1_struct_0(sK0_skl),sK1_skl,k2_waybel34(sK0_skl,sK1_skl,sK2_skl),sK3_skl) != k1_yellow_0(sK1_skl,k5_pre_topc(sK1_skl,sK0_skl,sK2_skl,k6_waybel_0(sK0_skl,sK3_skl)))
& m1_subset_1(sK3_skl,u1_struct_0(sK0_skl))
& m2_relset_1(sK2_skl,u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))
& v18_waybel_0(sK2_skl,sK1_skl,sK0_skl)
& v1_funct_2(sK2_skl,u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))
& v1_funct_1(sK2_skl)
& l1_orders_2(sK1_skl)
& v3_lattice3(sK1_skl)
& v2_lattice3(sK1_skl)
& v1_lattice3(sK1_skl)
& v4_orders_2(sK1_skl)
& v3_orders_2(sK1_skl)
& v2_orders_2(sK1_skl)
& l1_orders_2(sK0_skl)
& v3_lattice3(sK0_skl)
& v2_lattice3(sK0_skl)
& v1_lattice3(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,sK2_skl,sK3_skl]),skolemize(A,sK0_skl),skolemize(B,sK1_skl),skolemize(C,sK2_skl),skolemize(D,sK3_skl)],[f133]) ).
fof(f135,plain,
v2_orders_2(sK0_skl),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f136,plain,
v3_orders_2(sK0_skl),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f137,plain,
v4_orders_2(sK0_skl),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f138,plain,
v1_lattice3(sK0_skl),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f139,plain,
v2_lattice3(sK0_skl),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f140,plain,
v3_lattice3(sK0_skl),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f141,plain,
l1_orders_2(sK0_skl),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f142,plain,
v2_orders_2(sK1_skl),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f143,plain,
v3_orders_2(sK1_skl),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f144,plain,
v4_orders_2(sK1_skl),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f145,plain,
v1_lattice3(sK1_skl),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f146,plain,
v2_lattice3(sK1_skl),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f147,plain,
v3_lattice3(sK1_skl),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f148,plain,
l1_orders_2(sK1_skl),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f149,plain,
v1_funct_1(sK2_skl),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f150,plain,
v1_funct_2(sK2_skl,u1_struct_0(sK1_skl),u1_struct_0(sK0_skl)),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f151,plain,
v18_waybel_0(sK2_skl,sK1_skl,sK0_skl),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f152,plain,
m2_relset_1(sK2_skl,u1_struct_0(sK1_skl),u1_struct_0(sK0_skl)),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f153,plain,
m1_subset_1(sK3_skl,u1_struct_0(sK0_skl)),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f154,plain,
k7_yellow_2(u1_struct_0(sK0_skl),sK1_skl,k2_waybel34(sK0_skl,sK1_skl,sK2_skl),sK3_skl) != k1_yellow_0(sK1_skl,k5_pre_topc(sK1_skl,sK0_skl,sK2_skl,k6_waybel_0(sK0_skl,sK3_skl))),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f288,plain,
! [A] :
( ~ v3_struct_0(A)
| ~ v2_lattice3(A)
| ~ l1_orders_2(A) ),
inference(pre_NNF_transformation,[status(thm)],[f33]) ).
fof(f289,plain,
! [X0] :
( ~ v3_struct_0(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f288]) ).
fof(f322,plain,
! [A] :
( ! [B] :
( ! [C] :
( ! [D] :
( ( D = k2_waybel34(A,B,C)
<=> v3_waybel_1(k1_waybel_1(A,B,D,C),A,B) )
| ~ m2_relset_1(D,u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_2(D,u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_1(D) )
| ~ v18_waybel_0(C,B,A)
| ~ v3_lattice3(B)
| ~ v3_lattice3(A)
| ~ m2_relset_1(C,u1_struct_0(B),u1_struct_0(A))
| ~ v1_funct_2(C,u1_struct_0(B),u1_struct_0(A))
| ~ v1_funct_1(C) )
| ~ l1_orders_2(B)
| ~ v2_lattice3(B)
| ~ v1_lattice3(B)
| ~ v4_orders_2(B)
| ~ v3_orders_2(B)
| ~ v2_orders_2(B) )
| ~ l1_orders_2(A)
| ~ v2_lattice3(A)
| ~ v1_lattice3(A)
| ~ v4_orders_2(A)
| ~ v3_orders_2(A)
| ~ v2_orders_2(A) ),
inference(pre_NNF_transformation,[status(thm)],[f45]) ).
fof(f323,plain,
! [A] :
( ! [B] :
( ! [C] :
( ! [D] :
( ( ( ~ v3_waybel_1(k1_waybel_1(A,B,D,C),A,B)
| D = k2_waybel34(A,B,C) )
& ( v3_waybel_1(k1_waybel_1(A,B,D,C),A,B)
| D != k2_waybel34(A,B,C) ) )
| ~ m2_relset_1(D,u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_2(D,u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_1(D) )
| ~ v18_waybel_0(C,B,A)
| ~ v3_lattice3(B)
| ~ v3_lattice3(A)
| ~ m2_relset_1(C,u1_struct_0(B),u1_struct_0(A))
| ~ v1_funct_2(C,u1_struct_0(B),u1_struct_0(A))
| ~ v1_funct_1(C) )
| ~ l1_orders_2(B)
| ~ v2_lattice3(B)
| ~ v1_lattice3(B)
| ~ v4_orders_2(B)
| ~ v3_orders_2(B)
| ~ v2_orders_2(B) )
| ~ l1_orders_2(A)
| ~ v2_lattice3(A)
| ~ v1_lattice3(A)
| ~ v4_orders_2(A)
| ~ v3_orders_2(A)
| ~ v2_orders_2(A) ),
inference(NNF_transformation,[status(thm)],[f322]) ).
fof(f324,plain,
! [X0,X1,X2,X3] :
( v3_waybel_1(k1_waybel_1(X0,X1,X3,X2),X0,X1)
| X3 != k2_waybel34(X0,X1,X2)
| ~ m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X3)
| ~ v18_waybel_0(X2,X1,X0)
| ~ v3_lattice3(X1)
| ~ v3_lattice3(X0)
| ~ m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f323]) ).
fof(f327,plain,
! [A] :
( ! [B] :
( ! [C] :
( r4_waybel_1(A,B,C)
<=> ( r2_hidden(k1_yellow_0(A,C),C)
& B = k1_yellow_0(A,C)
& r1_yellow_0(A,C) ) )
| ~ m1_subset_1(B,u1_struct_0(A)) )
| ~ l1_orders_2(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f47]) ).
fof(f328,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( ~ r2_hidden(k1_yellow_0(A,C),C)
| B != k1_yellow_0(A,C)
| ~ r1_yellow_0(A,C)
| r4_waybel_1(A,B,C) )
& ( ( r2_hidden(k1_yellow_0(A,C),C)
& B = k1_yellow_0(A,C)
& r1_yellow_0(A,C) )
| ~ r4_waybel_1(A,B,C) ) )
| ~ m1_subset_1(B,u1_struct_0(A)) )
| ~ l1_orders_2(A)
| v3_struct_0(A) ),
inference(NNF_transformation,[status(thm)],[f327]) ).
fof(f329,plain,
! [A] :
( ! [B] :
( ( ! [C] :
( ~ r2_hidden(k1_yellow_0(A,C),C)
| B != k1_yellow_0(A,C)
| ~ r1_yellow_0(A,C)
| r4_waybel_1(A,B,C) )
& ! [C] :
( ( r2_hidden(k1_yellow_0(A,C),C)
& B = k1_yellow_0(A,C)
& r1_yellow_0(A,C) )
| ~ r4_waybel_1(A,B,C) ) )
| ~ m1_subset_1(B,u1_struct_0(A)) )
| ~ l1_orders_2(A)
| v3_struct_0(A) ),
inference(miniscoping,[status(thm)],[f328]) ).
fof(f331,plain,
! [X0,X1,X2] :
( X1 = k1_yellow_0(X0,X2)
| ~ r4_waybel_1(X0,X1,X2)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l1_orders_2(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f329]) ).
fof(f341,plain,
! [A,B,C] :
( ( m2_relset_1(k2_waybel34(A,B,C),u1_struct_0(A),u1_struct_0(B))
& v1_funct_2(k2_waybel34(A,B,C),u1_struct_0(A),u1_struct_0(B))
& v1_funct_1(k2_waybel34(A,B,C)) )
| ~ m1_relset_1(C,u1_struct_0(B),u1_struct_0(A))
| ~ v1_funct_2(C,u1_struct_0(B),u1_struct_0(A))
| ~ v1_funct_1(C)
| ~ l1_orders_2(B)
| ~ v2_lattice3(B)
| ~ v1_lattice3(B)
| ~ v4_orders_2(B)
| ~ v3_orders_2(B)
| ~ v2_orders_2(B)
| ~ l1_orders_2(A)
| ~ v2_lattice3(A)
| ~ v1_lattice3(A)
| ~ v4_orders_2(A)
| ~ v3_orders_2(A)
| ~ v2_orders_2(A) ),
inference(pre_NNF_transformation,[status(thm)],[f57]) ).
fof(f342,plain,
! [X0,X1,X2] :
( v1_funct_1(k2_waybel34(X0,X1,X2))
| ~ m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f341]) ).
fof(f343,plain,
! [X0,X1,X2] :
( v1_funct_2(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f341]) ).
fof(f344,plain,
! [X0,X1,X2] :
( m2_relset_1(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f341]) ).
fof(f352,plain,
! [A,B,C,D] :
( m1_subset_1(k7_yellow_2(A,B,C,D),u1_struct_0(B))
| ~ m1_subset_1(D,A)
| ~ m1_relset_1(C,A,u1_struct_0(B))
| ~ v1_funct_2(C,A,u1_struct_0(B))
| ~ v1_funct_1(C)
| ~ l1_struct_0(B)
| v3_struct_0(B)
| v1_xboole_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f63]) ).
fof(f353,plain,
! [X0,X1,X2,X3] :
( m1_subset_1(k7_yellow_2(X0,X1,X2,X3),u1_struct_0(X1))
| ~ m1_subset_1(X3,X0)
| ~ m1_relset_1(X2,X0,u1_struct_0(X1))
| ~ v1_funct_2(X2,X0,u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ l1_struct_0(X1)
| v3_struct_0(X1)
| v1_xboole_0(X0) ),
inference(cnf_transformation,[status(thm)],[f352]) ).
fof(f354,plain,
! [A] :
( l1_struct_0(A)
| ~ l1_orders_2(A) ),
inference(pre_NNF_transformation,[status(thm)],[f64]) ).
fof(f355,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f354]) ).
fof(f414,plain,
! [A] :
( ~ v1_xboole_0(u1_struct_0(A))
| ~ l1_struct_0(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f89]) ).
fof(f415,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| ~ l1_struct_0(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f414]) ).
fof(f572,plain,
! [A,B,C] :
( ( ~ m1_relset_1(C,A,B)
| m2_relset_1(C,A,B) )
& ( m1_relset_1(C,A,B)
| ~ m2_relset_1(C,A,B) ) ),
inference(NNF_transformation,[status(thm)],[f122]) ).
fof(f573,plain,
( ! [A,B,C] :
( ~ m1_relset_1(C,A,B)
| m2_relset_1(C,A,B) )
& ! [A,B,C] :
( m1_relset_1(C,A,B)
| ~ m2_relset_1(C,A,B) ) ),
inference(miniscoping,[status(thm)],[f572]) ).
fof(f574,plain,
! [X0,X1,X2] :
( m1_relset_1(X0,X1,X2)
| ~ m2_relset_1(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f573]) ).
fof(f575,plain,
! [X0,X1,X2] :
( ~ m1_relset_1(X0,X1,X2)
| m2_relset_1(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f573]) ).
fof(f578,plain,
! [A] :
( ! [B] :
( ! [C] :
( ! [D] :
( ( v3_waybel_1(k1_waybel_1(A,B,C,D),A,B)
<=> ( ! [E] :
( r4_waybel_1(B,k7_yellow_2(u1_struct_0(A),B,C,E),k5_pre_topc(B,A,D,k6_waybel_0(A,E)))
| ~ m1_subset_1(E,u1_struct_0(A)) )
& v5_orders_3(D,B,A) ) )
| ~ m2_relset_1(D,u1_struct_0(B),u1_struct_0(A))
| ~ v1_funct_2(D,u1_struct_0(B),u1_struct_0(A))
| ~ v1_funct_1(D) )
| ~ m2_relset_1(C,u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_1(C) )
| ~ l1_orders_2(B)
| ~ v4_orders_2(B)
| ~ v3_orders_2(B)
| ~ v2_orders_2(B)
| v3_struct_0(B) )
| ~ l1_orders_2(A)
| ~ v4_orders_2(A)
| ~ v3_orders_2(A)
| ~ v2_orders_2(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f124]) ).
fof(f579,plain,
! [A] :
( ! [B] :
( ! [C] :
( ! [D] :
( ( ( ? [E] :
( ~ r4_waybel_1(B,k7_yellow_2(u1_struct_0(A),B,C,E),k5_pre_topc(B,A,D,k6_waybel_0(A,E)))
& m1_subset_1(E,u1_struct_0(A)) )
| ~ v5_orders_3(D,B,A)
| v3_waybel_1(k1_waybel_1(A,B,C,D),A,B) )
& ( ( ! [E] :
( r4_waybel_1(B,k7_yellow_2(u1_struct_0(A),B,C,E),k5_pre_topc(B,A,D,k6_waybel_0(A,E)))
| ~ m1_subset_1(E,u1_struct_0(A)) )
& v5_orders_3(D,B,A) )
| ~ v3_waybel_1(k1_waybel_1(A,B,C,D),A,B) ) )
| ~ m2_relset_1(D,u1_struct_0(B),u1_struct_0(A))
| ~ v1_funct_2(D,u1_struct_0(B),u1_struct_0(A))
| ~ v1_funct_1(D) )
| ~ m2_relset_1(C,u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_1(C) )
| ~ l1_orders_2(B)
| ~ v4_orders_2(B)
| ~ v3_orders_2(B)
| ~ v2_orders_2(B)
| v3_struct_0(B) )
| ~ l1_orders_2(A)
| ~ v4_orders_2(A)
| ~ v3_orders_2(A)
| ~ v2_orders_2(A)
| v3_struct_0(A) ),
inference(NNF_transformation,[status(thm)],[f578]) ).
fof(f580,plain,
! [A] :
( ! [B] :
( ! [C] :
( ! [D] :
( ( ( ( ~ r4_waybel_1(B,k7_yellow_2(u1_struct_0(A),B,C,sK28_skl(D,C,B,A)),k5_pre_topc(B,A,D,k6_waybel_0(A,sK28_skl(D,C,B,A))))
& m1_subset_1(sK28_skl(D,C,B,A),u1_struct_0(A)) )
| ~ v5_orders_3(D,B,A)
| v3_waybel_1(k1_waybel_1(A,B,C,D),A,B) )
& ( ( ! [E] :
( r4_waybel_1(B,k7_yellow_2(u1_struct_0(A),B,C,E),k5_pre_topc(B,A,D,k6_waybel_0(A,E)))
| ~ m1_subset_1(E,u1_struct_0(A)) )
& v5_orders_3(D,B,A) )
| ~ v3_waybel_1(k1_waybel_1(A,B,C,D),A,B) ) )
| ~ m2_relset_1(D,u1_struct_0(B),u1_struct_0(A))
| ~ v1_funct_2(D,u1_struct_0(B),u1_struct_0(A))
| ~ v1_funct_1(D) )
| ~ m2_relset_1(C,u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_1(C) )
| ~ l1_orders_2(B)
| ~ v4_orders_2(B)
| ~ v3_orders_2(B)
| ~ v2_orders_2(B)
| v3_struct_0(B) )
| ~ l1_orders_2(A)
| ~ v4_orders_2(A)
| ~ v3_orders_2(A)
| ~ v2_orders_2(A)
| v3_struct_0(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK28_skl]),skolemize(E,sK28_skl(D,C,B,A))],[f579]) ).
fof(f582,plain,
! [X0,X1,X2,X3,X4] :
( r4_waybel_1(X1,k7_yellow_2(u1_struct_0(X0),X1,X2,X4),k5_pre_topc(X1,X0,X3,k6_waybel_0(X0,X4)))
| ~ m1_subset_1(X4,u1_struct_0(X0))
| ~ v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1)
| ~ m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X3)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| v3_struct_0(X1)
| ~ l1_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f580]) ).
fof(f607,plain,
! [X0,X1,X2] :
( v3_waybel_1(k1_waybel_1(X0,X1,k2_waybel34(X0,X1,X2),X2),X0,X1)
| ~ m2_relset_1(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(k2_waybel34(X0,X1,X2))
| ~ v18_waybel_0(X2,X1,X0)
| ~ v3_lattice3(X1)
| ~ v3_lattice3(X0)
| ~ m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f324]) ).
fof(f765,definition,
( sQ6_spl
<=> v1_xboole_0(u1_struct_0(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f766,plain,
( ~ sQ6_spl
| v1_xboole_0(u1_struct_0(sK0_skl)) ),
inference(component_clause,[status(thm)],[f765]) ).
fof(f769,plain,
( ~ sQ6_spl
| ~ l1_struct_0(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f766,f415]) ).
fof(f775,definition,
( sQ7_spl
<=> v3_struct_0(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f776,plain,
( ~ sQ7_spl
| v3_struct_0(sK0_skl) ),
inference(component_clause,[status(thm)],[f775]) ).
fof(f778,definition,
( sQ8_spl
<=> l1_struct_0(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f780,plain,
( sQ8_spl
| ~ l1_struct_0(sK0_skl) ),
inference(component_clause,[status(thm)],[f778]) ).
fof(f781,plain,
( ~ sQ6_spl
| ~ sQ8_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f769,f775,f778,f765]) ).
fof(f782,plain,
( sQ8_spl
| ~ l1_orders_2(sK0_skl) ),
inference(resolution,[status(thm)],[f780,f355]) ).
fof(f783,plain,
( sQ8_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f782,f141]) ).
fof(f784,plain,
sQ8_spl,
inference(contradiction_clause,[status(thm)],[f783]) ).
fof(f785,plain,
( ~ sQ7_spl
| ~ v2_lattice3(sK0_skl)
| ~ l1_orders_2(sK0_skl) ),
inference(resolution,[status(thm)],[f776,f289]) ).
fof(f787,definition,
( sQ9_spl
<=> l1_orders_2(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f789,plain,
( sQ9_spl
| ~ l1_orders_2(sK0_skl) ),
inference(component_clause,[status(thm)],[f787]) ).
fof(f790,definition,
( sQ10_spl
<=> v2_lattice3(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f792,plain,
( sQ10_spl
| ~ v2_lattice3(sK0_skl) ),
inference(component_clause,[status(thm)],[f790]) ).
fof(f793,plain,
( ~ sQ7_spl
| ~ sQ10_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f785,f787,f790,f775]) ).
fof(f794,definition,
( sQ11_spl
<=> v1_lattice3(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f796,plain,
( sQ11_spl
| ~ v1_lattice3(sK0_skl) ),
inference(component_clause,[status(thm)],[f794]) ).
fof(f798,plain,
( sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f789,f141]) ).
fof(f799,plain,
sQ9_spl,
inference(contradiction_clause,[status(thm)],[f798]) ).
fof(f800,plain,
( sQ11_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f796,f138]) ).
fof(f801,plain,
sQ11_spl,
inference(contradiction_clause,[status(thm)],[f800]) ).
fof(f945,definition,
( sQ27_spl
<=> v3_struct_0(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f946,plain,
( ~ sQ27_spl
| v3_struct_0(sK1_skl) ),
inference(component_clause,[status(thm)],[f945]) ).
fof(f958,plain,
! [X0,X1,X2] :
( ~ m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| v3_waybel_1(k1_waybel_1(X0,X1,k2_waybel34(X0,X1,X2),X2),X0,X1)
| ~ m2_relset_1(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(k2_waybel34(X0,X1,X2))
| ~ v18_waybel_0(X2,X1,X0)
| ~ v3_lattice3(X1)
| ~ v3_lattice3(X0)
| ~ m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0) ),
inference(resolution,[status(thm)],[f607,f343]) ).
fof(f959,plain,
! [X0,X1,X2] :
( ~ m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))
| v3_waybel_1(k1_waybel_1(X0,X1,k2_waybel34(X0,X1,X2),X2),X0,X1)
| ~ m2_relset_1(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(k2_waybel34(X0,X1,X2))
| ~ v18_waybel_0(X2,X1,X0)
| ~ v3_lattice3(X1)
| ~ v3_lattice3(X0)
| ~ m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f958]) ).
fof(f960,plain,
! [X0,X1,X2] :
( ~ m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))
| v3_waybel_1(k1_waybel_1(X0,X1,k2_waybel34(X0,X1,X2),X2),X0,X1)
| ~ m2_relset_1(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(k2_waybel34(X0,X1,X2))
| ~ v18_waybel_0(X2,X1,X0)
| ~ v3_lattice3(X1)
| ~ v3_lattice3(X0)
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f959,f575]) ).
fof(f961,plain,
( ~ sQ27_spl
| ~ v2_lattice3(sK1_skl)
| ~ l1_orders_2(sK1_skl) ),
inference(resolution,[status(thm)],[f946,f289]) ).
fof(f963,definition,
( sQ30_spl
<=> l1_orders_2(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f965,plain,
( sQ30_spl
| ~ l1_orders_2(sK1_skl) ),
inference(component_clause,[status(thm)],[f963]) ).
fof(f966,definition,
( sQ31_spl
<=> v2_lattice3(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f968,plain,
( sQ31_spl
| ~ v2_lattice3(sK1_skl) ),
inference(component_clause,[status(thm)],[f966]) ).
fof(f969,plain,
( ~ sQ27_spl
| ~ sQ31_spl
| ~ sQ30_spl ),
inference(split_clause,[status(thm)],[f961,f963,f966,f945]) ).
fof(f970,definition,
( sQ32_spl
<=> v1_lattice3(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f972,plain,
( sQ32_spl
| ~ v1_lattice3(sK1_skl) ),
inference(component_clause,[status(thm)],[f970]) ).
fof(f974,plain,
( sQ30_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f965,f148]) ).
fof(f975,plain,
sQ30_spl,
inference(contradiction_clause,[status(thm)],[f974]) ).
fof(f976,plain,
( sQ31_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f968,f146]) ).
fof(f977,plain,
sQ31_spl,
inference(contradiction_clause,[status(thm)],[f976]) ).
fof(f978,plain,
! [X0,X1,X2] :
( ~ m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))
| v3_waybel_1(k1_waybel_1(X0,X1,k2_waybel34(X0,X1,X2),X2),X0,X1)
| ~ m2_relset_1(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
| ~ v18_waybel_0(X2,X1,X0)
| ~ v3_lattice3(X1)
| ~ v3_lattice3(X0)
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f960,f342]) ).
fof(f979,plain,
( ~ m1_relset_1(sK2_skl,u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))
| v3_waybel_1(k1_waybel_1(sK0_skl,sK1_skl,k2_waybel34(sK0_skl,sK1_skl,sK2_skl),sK2_skl),sK0_skl,sK1_skl)
| ~ m2_relset_1(k2_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
| ~ v3_lattice3(sK1_skl)
| ~ v3_lattice3(sK0_skl)
| ~ v1_funct_2(sK2_skl,u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))
| ~ v1_funct_1(sK2_skl)
| ~ l1_orders_2(sK1_skl)
| ~ v2_lattice3(sK1_skl)
| ~ v1_lattice3(sK1_skl)
| ~ v4_orders_2(sK1_skl)
| ~ v3_orders_2(sK1_skl)
| ~ v2_orders_2(sK1_skl)
| ~ l1_orders_2(sK0_skl)
| ~ v2_lattice3(sK0_skl)
| ~ v1_lattice3(sK0_skl)
| ~ v4_orders_2(sK0_skl)
| ~ v3_orders_2(sK0_skl)
| ~ v2_orders_2(sK0_skl) ),
inference(resolution,[status(thm)],[f978,f151]) ).
fof(f980,definition,
( sQ33_spl
<=> v2_orders_2(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f982,plain,
( sQ33_spl
| ~ v2_orders_2(sK0_skl) ),
inference(component_clause,[status(thm)],[f980]) ).
fof(f983,definition,
( sQ34_spl
<=> v3_orders_2(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f985,plain,
( sQ34_spl
| ~ v3_orders_2(sK0_skl) ),
inference(component_clause,[status(thm)],[f983]) ).
fof(f986,definition,
( sQ35_spl
<=> v4_orders_2(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f988,plain,
( sQ35_spl
| ~ v4_orders_2(sK0_skl) ),
inference(component_clause,[status(thm)],[f986]) ).
fof(f989,definition,
( sQ36_spl
<=> v2_orders_2(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f991,plain,
( sQ36_spl
| ~ v2_orders_2(sK1_skl) ),
inference(component_clause,[status(thm)],[f989]) ).
fof(f992,definition,
( sQ37_spl
<=> v3_orders_2(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f994,plain,
( sQ37_spl
| ~ v3_orders_2(sK1_skl) ),
inference(component_clause,[status(thm)],[f992]) ).
fof(f995,definition,
( sQ38_spl
<=> v4_orders_2(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f997,plain,
( sQ38_spl
| ~ v4_orders_2(sK1_skl) ),
inference(component_clause,[status(thm)],[f995]) ).
fof(f998,definition,
( sQ39_spl
<=> v1_funct_1(sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f1000,plain,
( sQ39_spl
| ~ v1_funct_1(sK2_skl) ),
inference(component_clause,[status(thm)],[f998]) ).
fof(f1001,definition,
( sQ40_spl
<=> v1_funct_2(sK2_skl,u1_struct_0(sK1_skl),u1_struct_0(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f1003,plain,
( sQ40_spl
| ~ v1_funct_2(sK2_skl,u1_struct_0(sK1_skl),u1_struct_0(sK0_skl)) ),
inference(component_clause,[status(thm)],[f1001]) ).
fof(f1004,definition,
( sQ41_spl
<=> v3_lattice3(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f1006,plain,
( sQ41_spl
| ~ v3_lattice3(sK0_skl) ),
inference(component_clause,[status(thm)],[f1004]) ).
fof(f1007,definition,
( sQ42_spl
<=> v3_lattice3(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f1009,plain,
( sQ42_spl
| ~ v3_lattice3(sK1_skl) ),
inference(component_clause,[status(thm)],[f1007]) ).
fof(f1010,definition,
( sQ43_spl
<=> m2_relset_1(k2_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f1012,plain,
( sQ43_spl
| ~ m2_relset_1(k2_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)) ),
inference(component_clause,[status(thm)],[f1010]) ).
fof(f1013,definition,
( sQ44_spl
<=> v3_waybel_1(k1_waybel_1(sK0_skl,sK1_skl,k2_waybel34(sK0_skl,sK1_skl,sK2_skl),sK2_skl),sK0_skl,sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f1014,plain,
( ~ sQ44_spl
| v3_waybel_1(k1_waybel_1(sK0_skl,sK1_skl,k2_waybel34(sK0_skl,sK1_skl,sK2_skl),sK2_skl),sK0_skl,sK1_skl) ),
inference(component_clause,[status(thm)],[f1013]) ).
fof(f1016,definition,
( sQ45_spl
<=> m1_relset_1(sK2_skl,u1_struct_0(sK1_skl),u1_struct_0(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f1018,plain,
( sQ45_spl
| ~ m1_relset_1(sK2_skl,u1_struct_0(sK1_skl),u1_struct_0(sK0_skl)) ),
inference(component_clause,[status(thm)],[f1016]) ).
fof(f1019,plain,
( ~ sQ45_spl
| sQ44_spl
| ~ sQ43_spl
| ~ sQ42_spl
| ~ sQ41_spl
| ~ sQ40_spl
| ~ sQ39_spl
| ~ sQ30_spl
| ~ sQ31_spl
| ~ sQ32_spl
| ~ sQ38_spl
| ~ sQ37_spl
| ~ sQ36_spl
| ~ sQ9_spl
| ~ sQ10_spl
| ~ sQ11_spl
| ~ sQ35_spl
| ~ sQ34_spl
| ~ sQ33_spl ),
inference(split_clause,[status(thm)],[f979,f980,f983,f986,f794,f790,f787,f989,f992,f995,f970,f966,f963,f998,f1001,f1004,f1007,f1010,f1013,f1016]) ).
fof(f1020,plain,
( sQ32_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f972,f145]) ).
fof(f1021,plain,
sQ32_spl,
inference(contradiction_clause,[status(thm)],[f1020]) ).
fof(f1022,plain,
( sQ10_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f792,f139]) ).
fof(f1023,plain,
sQ10_spl,
inference(contradiction_clause,[status(thm)],[f1022]) ).
fof(f1024,plain,
( sQ45_spl
| ~ m2_relset_1(sK2_skl,u1_struct_0(sK1_skl),u1_struct_0(sK0_skl)) ),
inference(resolution,[status(thm)],[f1018,f574]) ).
fof(f1025,plain,
( sQ45_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1024,f152]) ).
fof(f1026,plain,
sQ45_spl,
inference(contradiction_clause,[status(thm)],[f1025]) ).
fof(f1028,plain,
! [X0] :
( ~ sQ44_spl
| r4_waybel_1(sK1_skl,k7_yellow_2(u1_struct_0(sK0_skl),sK1_skl,k2_waybel34(sK0_skl,sK1_skl,sK2_skl),X0),k5_pre_topc(sK1_skl,sK0_skl,sK2_skl,k6_waybel_0(sK0_skl,X0)))
| ~ m1_subset_1(X0,u1_struct_0(sK0_skl))
| ~ m2_relset_1(sK2_skl,u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))
| ~ v1_funct_2(sK2_skl,u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))
| ~ v1_funct_1(sK2_skl)
| ~ m2_relset_1(k2_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
| ~ v1_funct_2(k2_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
| ~ v1_funct_1(k2_waybel34(sK0_skl,sK1_skl,sK2_skl))
| ~ l1_orders_2(sK1_skl)
| ~ v4_orders_2(sK1_skl)
| ~ v3_orders_2(sK1_skl)
| ~ v2_orders_2(sK1_skl)
| v3_struct_0(sK1_skl)
| ~ l1_orders_2(sK0_skl)
| ~ v4_orders_2(sK0_skl)
| ~ v3_orders_2(sK0_skl)
| ~ v2_orders_2(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f1014,f582]) ).
fof(f1029,definition,
( sQ46_spl
<=> m2_relset_1(sK2_skl,u1_struct_0(sK1_skl),u1_struct_0(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f1031,plain,
( sQ46_spl
| ~ m2_relset_1(sK2_skl,u1_struct_0(sK1_skl),u1_struct_0(sK0_skl)) ),
inference(component_clause,[status(thm)],[f1029]) ).
fof(f1035,definition,
( sQ48_spl
<=> v1_funct_1(k2_waybel34(sK0_skl,sK1_skl,sK2_skl)) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f1037,plain,
( sQ48_spl
| ~ v1_funct_1(k2_waybel34(sK0_skl,sK1_skl,sK2_skl)) ),
inference(component_clause,[status(thm)],[f1035]) ).
fof(f1038,definition,
( sQ49_spl
<=> v1_funct_2(k2_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f1040,plain,
( sQ49_spl
| ~ v1_funct_2(k2_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)) ),
inference(component_clause,[status(thm)],[f1038]) ).
fof(f1045,definition,
! [X0] :
( sQ51_spl
<=> ( r4_waybel_1(sK1_skl,k7_yellow_2(u1_struct_0(sK0_skl),sK1_skl,k2_waybel34(sK0_skl,sK1_skl,sK2_skl),X0),k5_pre_topc(sK1_skl,sK0_skl,sK2_skl,k6_waybel_0(sK0_skl,X0)))
| ~ m1_subset_1(X0,u1_struct_0(sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f1046,plain,
! [X0] :
( ~ sQ51_spl
| r4_waybel_1(sK1_skl,k7_yellow_2(u1_struct_0(sK0_skl),sK1_skl,k2_waybel34(sK0_skl,sK1_skl,sK2_skl),X0),k5_pre_topc(sK1_skl,sK0_skl,sK2_skl,k6_waybel_0(sK0_skl,X0)))
| ~ m1_subset_1(X0,u1_struct_0(sK0_skl)) ),
inference(component_clause,[status(thm)],[f1045]) ).
fof(f1048,plain,
( ~ sQ44_spl
| sQ51_spl
| ~ sQ46_spl
| ~ sQ40_spl
| ~ sQ39_spl
| ~ sQ43_spl
| ~ sQ49_spl
| ~ sQ48_spl
| ~ sQ30_spl
| ~ sQ38_spl
| ~ sQ37_spl
| ~ sQ36_spl
| sQ27_spl
| ~ sQ9_spl
| ~ sQ35_spl
| ~ sQ34_spl
| ~ sQ33_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f1028,f775,f980,f983,f986,f787,f945,f989,f992,f995,f963,f1035,f1038,f1010,f998,f1001,f1029,f1045,f1013]) ).
fof(f1049,plain,
( sQ40_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1003,f150]) ).
fof(f1050,plain,
sQ40_spl,
inference(contradiction_clause,[status(thm)],[f1049]) ).
fof(f1051,plain,
( sQ39_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1000,f149]) ).
fof(f1052,plain,
sQ39_spl,
inference(contradiction_clause,[status(thm)],[f1051]) ).
fof(f1113,plain,
( sQ43_spl
| ~ m1_relset_1(sK2_skl,u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))
| ~ v1_funct_2(sK2_skl,u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))
| ~ v1_funct_1(sK2_skl)
| ~ l1_orders_2(sK1_skl)
| ~ v2_lattice3(sK1_skl)
| ~ v1_lattice3(sK1_skl)
| ~ v4_orders_2(sK1_skl)
| ~ v3_orders_2(sK1_skl)
| ~ v2_orders_2(sK1_skl)
| ~ l1_orders_2(sK0_skl)
| ~ v2_lattice3(sK0_skl)
| ~ v1_lattice3(sK0_skl)
| ~ v4_orders_2(sK0_skl)
| ~ v3_orders_2(sK0_skl)
| ~ v2_orders_2(sK0_skl) ),
inference(resolution,[status(thm)],[f1012,f344]) ).
fof(f1115,plain,
( sQ43_spl
| ~ sQ45_spl
| ~ sQ40_spl
| ~ sQ39_spl
| ~ sQ30_spl
| ~ sQ31_spl
| ~ sQ32_spl
| ~ sQ38_spl
| ~ sQ37_spl
| ~ sQ36_spl
| ~ sQ9_spl
| ~ sQ10_spl
| ~ sQ11_spl
| ~ sQ35_spl
| ~ sQ34_spl
| ~ sQ33_spl ),
inference(split_clause,[status(thm)],[f1113,f980,f983,f986,f794,f790,f787,f989,f992,f995,f970,f966,f963,f998,f1001,f1016,f1010]) ).
fof(f1116,plain,
( sQ38_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f997,f144]) ).
fof(f1117,plain,
sQ38_spl,
inference(contradiction_clause,[status(thm)],[f1116]) ).
fof(f1118,plain,
( sQ37_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f994,f143]) ).
fof(f1119,plain,
sQ37_spl,
inference(contradiction_clause,[status(thm)],[f1118]) ).
fof(f1120,plain,
( sQ36_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f991,f142]) ).
fof(f1121,plain,
sQ36_spl,
inference(contradiction_clause,[status(thm)],[f1120]) ).
fof(f1122,plain,
( sQ35_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f988,f137]) ).
fof(f1123,plain,
sQ35_spl,
inference(contradiction_clause,[status(thm)],[f1122]) ).
fof(f1124,plain,
( sQ34_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f985,f136]) ).
fof(f1125,plain,
sQ34_spl,
inference(contradiction_clause,[status(thm)],[f1124]) ).
fof(f1126,plain,
( sQ33_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f982,f135]) ).
fof(f1127,plain,
sQ33_spl,
inference(contradiction_clause,[status(thm)],[f1126]) ).
fof(f1128,plain,
( sQ46_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1031,f152]) ).
fof(f1129,plain,
sQ46_spl,
inference(contradiction_clause,[status(thm)],[f1128]) ).
fof(f1130,plain,
( sQ42_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1009,f147]) ).
fof(f1131,plain,
sQ42_spl,
inference(contradiction_clause,[status(thm)],[f1130]) ).
fof(f1132,plain,
( sQ41_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1006,f140]) ).
fof(f1133,plain,
sQ41_spl,
inference(contradiction_clause,[status(thm)],[f1132]) ).
fof(f1134,plain,
( sQ49_spl
| ~ m1_relset_1(sK2_skl,u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))
| ~ v1_funct_2(sK2_skl,u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))
| ~ v1_funct_1(sK2_skl)
| ~ l1_orders_2(sK1_skl)
| ~ v2_lattice3(sK1_skl)
| ~ v1_lattice3(sK1_skl)
| ~ v4_orders_2(sK1_skl)
| ~ v3_orders_2(sK1_skl)
| ~ v2_orders_2(sK1_skl)
| ~ l1_orders_2(sK0_skl)
| ~ v2_lattice3(sK0_skl)
| ~ v1_lattice3(sK0_skl)
| ~ v4_orders_2(sK0_skl)
| ~ v3_orders_2(sK0_skl)
| ~ v2_orders_2(sK0_skl) ),
inference(resolution,[status(thm)],[f1040,f343]) ).
fof(f1135,plain,
( sQ49_spl
| ~ sQ45_spl
| ~ sQ40_spl
| ~ sQ39_spl
| ~ sQ30_spl
| ~ sQ31_spl
| ~ sQ32_spl
| ~ sQ38_spl
| ~ sQ37_spl
| ~ sQ36_spl
| ~ sQ9_spl
| ~ sQ10_spl
| ~ sQ11_spl
| ~ sQ35_spl
| ~ sQ34_spl
| ~ sQ33_spl ),
inference(split_clause,[status(thm)],[f1134,f980,f983,f986,f794,f790,f787,f989,f992,f995,f970,f966,f963,f998,f1001,f1016,f1038]) ).
fof(f1136,plain,
( sQ48_spl
| ~ m1_relset_1(sK2_skl,u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))
| ~ v1_funct_2(sK2_skl,u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))
| ~ v1_funct_1(sK2_skl)
| ~ l1_orders_2(sK1_skl)
| ~ v2_lattice3(sK1_skl)
| ~ v1_lattice3(sK1_skl)
| ~ v4_orders_2(sK1_skl)
| ~ v3_orders_2(sK1_skl)
| ~ v2_orders_2(sK1_skl)
| ~ l1_orders_2(sK0_skl)
| ~ v2_lattice3(sK0_skl)
| ~ v1_lattice3(sK0_skl)
| ~ v4_orders_2(sK0_skl)
| ~ v3_orders_2(sK0_skl)
| ~ v2_orders_2(sK0_skl) ),
inference(resolution,[status(thm)],[f1037,f342]) ).
fof(f1138,plain,
( sQ48_spl
| ~ sQ45_spl
| ~ sQ40_spl
| ~ sQ39_spl
| ~ sQ30_spl
| ~ sQ31_spl
| ~ sQ32_spl
| ~ sQ38_spl
| ~ sQ37_spl
| ~ sQ36_spl
| ~ sQ9_spl
| ~ sQ10_spl
| ~ sQ11_spl
| ~ sQ35_spl
| ~ sQ34_spl
| ~ sQ33_spl ),
inference(split_clause,[status(thm)],[f1136,f980,f983,f986,f794,f790,f787,f989,f992,f995,f970,f966,f963,f998,f1001,f1016,f1035]) ).
fof(f1155,plain,
( ~ sQ51_spl
| r4_waybel_1(sK1_skl,k7_yellow_2(u1_struct_0(sK0_skl),sK1_skl,k2_waybel34(sK0_skl,sK1_skl,sK2_skl),sK3_skl),k5_pre_topc(sK1_skl,sK0_skl,sK2_skl,k6_waybel_0(sK0_skl,sK3_skl))) ),
inference(resolution,[status(thm)],[f1046,f153]) ).
fof(f1258,definition,
( sQ78_spl
<=> l1_struct_0(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition]) ).
fof(f1260,plain,
( sQ78_spl
| ~ l1_struct_0(sK1_skl) ),
inference(component_clause,[status(thm)],[f1258]) ).
fof(f1261,definition,
( sQ79_spl
<=> m1_relset_1(k2_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition]) ).
fof(f1263,plain,
( sQ79_spl
| ~ m1_relset_1(k2_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)) ),
inference(component_clause,[status(thm)],[f1261]) ).
fof(f1270,plain,
( sQ78_spl
| ~ l1_orders_2(sK1_skl) ),
inference(resolution,[status(thm)],[f1260,f355]) ).
fof(f1271,plain,
( sQ78_spl
| ~ sQ30_spl ),
inference(split_clause,[status(thm)],[f1270,f963,f1258]) ).
fof(f1373,plain,
( ~ sQ51_spl
| k7_yellow_2(u1_struct_0(sK0_skl),sK1_skl,k2_waybel34(sK0_skl,sK1_skl,sK2_skl),sK3_skl) = k1_yellow_0(sK1_skl,k5_pre_topc(sK1_skl,sK0_skl,sK2_skl,k6_waybel_0(sK0_skl,sK3_skl)))
| ~ m1_subset_1(k7_yellow_2(u1_struct_0(sK0_skl),sK1_skl,k2_waybel34(sK0_skl,sK1_skl,sK2_skl),sK3_skl),u1_struct_0(sK1_skl))
| ~ l1_orders_2(sK1_skl)
| v3_struct_0(sK1_skl) ),
inference(resolution,[status(thm)],[f1155,f331]) ).
fof(f1383,definition,
( sQ95_spl
<=> m1_subset_1(k7_yellow_2(u1_struct_0(sK0_skl),sK1_skl,k2_waybel34(sK0_skl,sK1_skl,sK2_skl),sK3_skl),u1_struct_0(sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition]) ).
fof(f1385,plain,
( sQ95_spl
| ~ m1_subset_1(k7_yellow_2(u1_struct_0(sK0_skl),sK1_skl,k2_waybel34(sK0_skl,sK1_skl,sK2_skl),sK3_skl),u1_struct_0(sK1_skl)) ),
inference(component_clause,[status(thm)],[f1383]) ).
fof(f1417,definition,
( sQ104_spl
<=> k7_yellow_2(u1_struct_0(sK0_skl),sK1_skl,k2_waybel34(sK0_skl,sK1_skl,sK2_skl),sK3_skl) = k1_yellow_0(sK1_skl,k5_pre_topc(sK1_skl,sK0_skl,sK2_skl,k6_waybel_0(sK0_skl,sK3_skl))) ),
introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition]) ).
fof(f1418,plain,
( ~ sQ104_spl
| k7_yellow_2(u1_struct_0(sK0_skl),sK1_skl,k2_waybel34(sK0_skl,sK1_skl,sK2_skl),sK3_skl) = k1_yellow_0(sK1_skl,k5_pre_topc(sK1_skl,sK0_skl,sK2_skl,k6_waybel_0(sK0_skl,sK3_skl))) ),
inference(component_clause,[status(thm)],[f1417]) ).
fof(f1420,plain,
( ~ sQ51_spl
| sQ104_spl
| ~ sQ95_spl
| ~ sQ30_spl
| sQ27_spl ),
inference(split_clause,[status(thm)],[f1373,f945,f963,f1383,f1417,f1045]) ).
fof(f1421,plain,
( sQ95_spl
| ~ m1_subset_1(sK3_skl,u1_struct_0(sK0_skl))
| ~ m1_relset_1(k2_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
| ~ v1_funct_2(k2_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
| ~ v1_funct_1(k2_waybel34(sK0_skl,sK1_skl,sK2_skl))
| ~ l1_struct_0(sK1_skl)
| v3_struct_0(sK1_skl)
| v1_xboole_0(u1_struct_0(sK0_skl)) ),
inference(resolution,[status(thm)],[f1385,f353]) ).
fof(f1423,definition,
( sQ105_spl
<=> m1_subset_1(sK3_skl,u1_struct_0(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition]) ).
fof(f1425,plain,
( sQ105_spl
| ~ m1_subset_1(sK3_skl,u1_struct_0(sK0_skl)) ),
inference(component_clause,[status(thm)],[f1423]) ).
fof(f1426,plain,
( sQ95_spl
| ~ sQ105_spl
| ~ sQ79_spl
| ~ sQ49_spl
| ~ sQ48_spl
| ~ sQ78_spl
| sQ27_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f1421,f765,f945,f1258,f1035,f1038,f1261,f1423,f1383]) ).
fof(f1427,plain,
( sQ79_spl
| ~ m2_relset_1(k2_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)) ),
inference(resolution,[status(thm)],[f1263,f574]) ).
fof(f1428,plain,
( sQ79_spl
| ~ sQ43_spl ),
inference(split_clause,[status(thm)],[f1427,f1010,f1261]) ).
fof(f1429,plain,
( ~ sQ104_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1418,f154]) ).
fof(f1430,plain,
~ sQ104_spl,
inference(contradiction_clause,[status(thm)],[f1429]) ).
fof(f1431,plain,
( sQ105_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1425,f153]) ).
fof(f1432,plain,
sQ105_spl,
inference(contradiction_clause,[status(thm)],[f1431]) ).
fof(f1433,plain,
$false,
inference(sat_refutation,[status(thm)],[f781,f784,f793,f799,f801,f969,f975,f977,f1019,f1021,f1023,f1026,f1048,f1050,f1052,f1115,f1117,f1119,f1121,f1123,f1125,f1127,f1129,f1131,f1133,f1135,f1138,f1271,f1420,f1426,f1428,f1430,f1432]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT353+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n009.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sun Sep 20 23:46:58 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.38 % Drodi V4.1.1
% 0.10/0.44 % Refutation found
% 0.10/0.44 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.10/0.44 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.10/0.46 % Elapsed time: 0.087856 seconds
% 0.10/0.46 % CPU time: 0.414027 seconds
% 0.10/0.46 % Total memory used: 93.636 MB
% 0.10/0.46 % Net memory used: 93.337 MB
%------------------------------------------------------------------------------