%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LAT352+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 : n004.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.20s 10.54s
% Output : CNFRefutation 0.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 44
% Syntax : Number of formulae : 216 ( 43 unt; 31 def)
% Number of atoms : 1270 ( 31 equ)
% Maximal formula atoms : 38 ( 5 avg)
% Number of connectives : 1847 ( 793 ~; 835 |; 152 &)
% ( 38 <=>; 29 =>; 0 <=; 0 <~>)
% Maximal formula depth : 43 ( 7 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 55 ( 53 usr; 32 prp; 0-3 aty)
% Number of functors : 14 ( 14 usr; 6 con; 0-4 aty)
% Number of variables : 190 ( 184 !; 6 ?)
% 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(A),u1_struct_0(B))
& v17_waybel_0(C,A,B)
& v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
& v1_funct_1(C) )
=> ! [D] :
( m1_subset_1(D,u1_struct_0(B))
=> k7_yellow_2(u1_struct_0(B),A,k1_waybel34(A,B,C),D) = k2_yellow_0(A,k5_pre_topc(A,B,C,k7_waybel_0(B,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(A),u1_struct_0(B))
& v17_waybel_0(C,A,B)
& v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
& v1_funct_1(C) )
=> ! [D] :
( m1_subset_1(D,u1_struct_0(B))
=> k7_yellow_2(u1_struct_0(B),A,k1_waybel34(A,B,C),D) = k2_yellow_0(A,k5_pre_topc(A,B,C,k7_waybel_0(B,D))) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f27,axiom,
! [A] :
( l1_orders_2(A)
=> ( ( v3_lattice3(A)
& ~ v3_struct_0(A) )
=> ( v2_lattice3(A)
& v1_lattice3(A)
& ~ v3_struct_0(A) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f32,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(A),u1_struct_0(B))
& v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
& v1_funct_1(C) )
=> ( ( v17_waybel_0(C,A,B)
& v3_lattice3(B)
& v3_lattice3(A) )
=> ! [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) )
=> ( D = k1_waybel34(A,B,C)
<=> v3_waybel_1(k1_waybel_1(A,B,C,D),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] :
( r3_waybel_1(A,B,C)
<=> ( r2_hidden(k2_yellow_0(A,C),C)
& B = k2_yellow_0(A,C)
& r2_yellow_0(A,C) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f52,axiom,
! [A,B,C] :
( ( m1_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)
& 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(k1_waybel34(A,B,C),u1_struct_0(B),u1_struct_0(A))
& v1_funct_2(k1_waybel34(A,B,C),u1_struct_0(B),u1_struct_0(A))
& v1_funct_1(k1_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(f90,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(f108,axiom,
? [A] :
( v1_funct_1(A)
& v1_xboole_0(A)
& v1_relat_1(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f121,axiom,
! [A,B,C] :
( m2_relset_1(C,A,B)
<=> m1_relset_1(C,A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f123,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(B))
=> r3_waybel_1(A,k7_yellow_2(u1_struct_0(B),A,D,E),k5_pre_topc(A,B,C,k7_waybel_0(B,E))) )
& v5_orders_3(C,A,B) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f129,axiom,
! [A] :
( v1_xboole_0(A)
=> A = k1_xboole_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f132,plain,
? [A] :
( ? [B] :
( ? [C] :
( ? [D] :
( k7_yellow_2(u1_struct_0(B),A,k1_waybel34(A,B,C),D) != k2_yellow_0(A,k5_pre_topc(A,B,C,k7_waybel_0(B,D)))
& m1_subset_1(D,u1_struct_0(B)) )
& m2_relset_1(C,u1_struct_0(A),u1_struct_0(B))
& v17_waybel_0(C,A,B)
& v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
& 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(f133,plain,
( k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),sK3_skl) != k2_yellow_0(sK0_skl,k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,sK3_skl)))
& m1_subset_1(sK3_skl,u1_struct_0(sK1_skl))
& m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
& v17_waybel_0(sK2_skl,sK0_skl,sK1_skl)
& v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_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)],[f132]) ).
fof(f134,plain,
v2_orders_2(sK0_skl),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f135,plain,
v3_orders_2(sK0_skl),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f136,plain,
v4_orders_2(sK0_skl),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f137,plain,
v1_lattice3(sK0_skl),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f138,plain,
v2_lattice3(sK0_skl),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f139,plain,
v3_lattice3(sK0_skl),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f140,plain,
l1_orders_2(sK0_skl),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f141,plain,
v2_orders_2(sK1_skl),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f142,plain,
v3_orders_2(sK1_skl),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f143,plain,
v4_orders_2(sK1_skl),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f144,plain,
v1_lattice3(sK1_skl),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f145,plain,
v2_lattice3(sK1_skl),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f146,plain,
v3_lattice3(sK1_skl),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f147,plain,
l1_orders_2(sK1_skl),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f148,plain,
v1_funct_1(sK2_skl),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f149,plain,
v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f150,plain,
v17_waybel_0(sK2_skl,sK0_skl,sK1_skl),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f151,plain,
m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f152,plain,
m1_subset_1(sK3_skl,u1_struct_0(sK1_skl)),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f153,plain,
k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),sK3_skl) != k2_yellow_0(sK0_skl,k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,sK3_skl))),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f250,plain,
! [A] :
( ( v2_lattice3(A)
& v1_lattice3(A)
& ~ v3_struct_0(A) )
| ~ v3_lattice3(A)
| v3_struct_0(A)
| ~ l1_orders_2(A) ),
inference(pre_NNF_transformation,[status(thm)],[f27]) ).
fof(f252,plain,
! [X0] :
( v1_lattice3(X0)
| ~ v3_lattice3(X0)
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f250]) ).
fof(f253,plain,
! [X0] :
( v2_lattice3(X0)
| ~ v3_lattice3(X0)
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f250]) ).
fof(f279,plain,
! [A] :
( ~ v3_struct_0(A)
| ~ v2_lattice3(A)
| ~ l1_orders_2(A) ),
inference(pre_NNF_transformation,[status(thm)],[f32]) ).
fof(f280,plain,
! [X0] :
( ~ v3_struct_0(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f279]) ).
fof(f321,plain,
! [A] :
( ! [B] :
( ! [C] :
( ! [D] :
( ( D = k1_waybel34(A,B,C)
<=> 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) )
| ~ v17_waybel_0(C,A,B)
| ~ v3_lattice3(B)
| ~ v3_lattice3(A)
| ~ 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)
| ~ 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(f322,plain,
! [A] :
( ! [B] :
( ! [C] :
( ! [D] :
( ( ( ~ v3_waybel_1(k1_waybel_1(A,B,C,D),A,B)
| D = k1_waybel34(A,B,C) )
& ( v3_waybel_1(k1_waybel_1(A,B,C,D),A,B)
| D != k1_waybel34(A,B,C) ) )
| ~ 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) )
| ~ v17_waybel_0(C,A,B)
| ~ v3_lattice3(B)
| ~ v3_lattice3(A)
| ~ 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)
| ~ 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)],[f321]) ).
fof(f323,plain,
! [X0,X1,X2,X3] :
( v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1)
| X3 != k1_waybel34(X0,X1,X2)
| ~ 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)
| ~ v17_waybel_0(X2,X0,X1)
| ~ v3_lattice3(X1)
| ~ v3_lattice3(X0)
| ~ 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)
| ~ 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)],[f322]) ).
fof(f326,plain,
! [A] :
( ! [B] :
( ! [C] :
( r3_waybel_1(A,B,C)
<=> ( r2_hidden(k2_yellow_0(A,C),C)
& B = k2_yellow_0(A,C)
& r2_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(f327,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( ~ r2_hidden(k2_yellow_0(A,C),C)
| B != k2_yellow_0(A,C)
| ~ r2_yellow_0(A,C)
| r3_waybel_1(A,B,C) )
& ( ( r2_hidden(k2_yellow_0(A,C),C)
& B = k2_yellow_0(A,C)
& r2_yellow_0(A,C) )
| ~ r3_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)],[f326]) ).
fof(f328,plain,
! [A] :
( ! [B] :
( ( ! [C] :
( ~ r2_hidden(k2_yellow_0(A,C),C)
| B != k2_yellow_0(A,C)
| ~ r2_yellow_0(A,C)
| r3_waybel_1(A,B,C) )
& ! [C] :
( ( r2_hidden(k2_yellow_0(A,C),C)
& B = k2_yellow_0(A,C)
& r2_yellow_0(A,C) )
| ~ r3_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)],[f327]) ).
fof(f330,plain,
! [X0,X1,X2] :
( X1 = k2_yellow_0(X0,X2)
| ~ r3_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)],[f328]) ).
fof(f335,plain,
! [A,B,C] :
( ( m2_relset_1(k1_waybel34(A,B,C),u1_struct_0(B),u1_struct_0(A))
& v1_funct_2(k1_waybel34(A,B,C),u1_struct_0(B),u1_struct_0(A))
& v1_funct_1(k1_waybel34(A,B,C)) )
| ~ m1_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)
| ~ 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)],[f52]) ).
fof(f336,plain,
! [X0,X1,X2] :
( v1_funct_1(k1_waybel34(X0,X1,X2))
| ~ m1_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)
| ~ 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)],[f335]) ).
fof(f337,plain,
! [X0,X1,X2] :
( v1_funct_2(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0))
| ~ m1_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)
| ~ 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)],[f335]) ).
fof(f338,plain,
! [X0,X1,X2] :
( m2_relset_1(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0))
| ~ m1_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)
| ~ 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)],[f335]) ).
fof(f351,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(f352,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)],[f351]) ).
fof(f353,plain,
! [A] :
( l1_struct_0(A)
| ~ l1_orders_2(A) ),
inference(pre_NNF_transformation,[status(thm)],[f64]) ).
fof(f354,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f353]) ).
fof(f416,plain,
! [A] :
( ~ v1_xboole_0(u1_struct_0(A))
| ~ l1_struct_0(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f90]) ).
fof(f417,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| ~ l1_struct_0(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f416]) ).
fof(f497,plain,
( v1_funct_1(sK18_skl)
& v1_xboole_0(sK18_skl)
& v1_relat_1(sK18_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18_skl]),skolemize(A,sK18_skl)],[f108]) ).
fof(f499,plain,
v1_xboole_0(sK18_skl),
inference(cnf_transformation,[status(thm)],[f497]) ).
fof(f565,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)],[f121]) ).
fof(f566,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)],[f565]) ).
fof(f567,plain,
! [X0,X1,X2] :
( m1_relset_1(X0,X1,X2)
| ~ m2_relset_1(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f566]) ).
fof(f568,plain,
! [X0,X1,X2] :
( ~ m1_relset_1(X0,X1,X2)
| m2_relset_1(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f566]) ).
fof(f571,plain,
! [A] :
( ! [B] :
( ! [C] :
( ! [D] :
( ( v3_waybel_1(k1_waybel_1(A,B,C,D),A,B)
<=> ( ! [E] :
( r3_waybel_1(A,k7_yellow_2(u1_struct_0(B),A,D,E),k5_pre_topc(A,B,C,k7_waybel_0(B,E)))
| ~ m1_subset_1(E,u1_struct_0(B)) )
& v5_orders_3(C,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(pre_NNF_transformation,[status(thm)],[f123]) ).
fof(f572,plain,
! [A] :
( ! [B] :
( ! [C] :
( ! [D] :
( ( ( ? [E] :
( ~ r3_waybel_1(A,k7_yellow_2(u1_struct_0(B),A,D,E),k5_pre_topc(A,B,C,k7_waybel_0(B,E)))
& m1_subset_1(E,u1_struct_0(B)) )
| ~ v5_orders_3(C,A,B)
| v3_waybel_1(k1_waybel_1(A,B,C,D),A,B) )
& ( ( ! [E] :
( r3_waybel_1(A,k7_yellow_2(u1_struct_0(B),A,D,E),k5_pre_topc(A,B,C,k7_waybel_0(B,E)))
| ~ m1_subset_1(E,u1_struct_0(B)) )
& v5_orders_3(C,A,B) )
| ~ 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)],[f571]) ).
fof(f573,plain,
! [A] :
( ! [B] :
( ! [C] :
( ! [D] :
( ( ( ( ~ r3_waybel_1(A,k7_yellow_2(u1_struct_0(B),A,D,sK27_skl(D,C,B,A)),k5_pre_topc(A,B,C,k7_waybel_0(B,sK27_skl(D,C,B,A))))
& m1_subset_1(sK27_skl(D,C,B,A),u1_struct_0(B)) )
| ~ v5_orders_3(C,A,B)
| v3_waybel_1(k1_waybel_1(A,B,C,D),A,B) )
& ( ( ! [E] :
( r3_waybel_1(A,k7_yellow_2(u1_struct_0(B),A,D,E),k5_pre_topc(A,B,C,k7_waybel_0(B,E)))
| ~ m1_subset_1(E,u1_struct_0(B)) )
& v5_orders_3(C,A,B) )
| ~ 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,[sK27_skl]),skolemize(E,sK27_skl(D,C,B,A))],[f572]) ).
fof(f575,plain,
! [X0,X1,X2,X3,X4] :
( r3_waybel_1(X0,k7_yellow_2(u1_struct_0(X1),X0,X3,X4),k5_pre_topc(X0,X1,X2,k7_waybel_0(X1,X4)))
| ~ m1_subset_1(X4,u1_struct_0(X1))
| ~ 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)],[f573]) ).
fof(f592,plain,
! [A] :
( A = k1_xboole_0
| ~ v1_xboole_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f129]) ).
fof(f593,plain,
! [X0] :
( X0 = k1_xboole_0
| ~ v1_xboole_0(X0) ),
inference(cnf_transformation,[status(thm)],[f592]) ).
fof(f600,plain,
! [X0,X1,X2] :
( v3_waybel_1(k1_waybel_1(X0,X1,X2,k1_waybel34(X0,X1,X2)),X0,X1)
| ~ m2_relset_1(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(k1_waybel34(X0,X1,X2))
| ~ v17_waybel_0(X2,X0,X1)
| ~ v3_lattice3(X1)
| ~ v3_lattice3(X0)
| ~ 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)
| ~ 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)],[f323]) ).
fof(f617,plain,
sK18_skl = k1_xboole_0,
inference(resolution,[status(thm)],[f593,f499]) ).
fof(f619,plain,
! [X0] :
( X0 = sK18_skl
| ~ v1_xboole_0(X0) ),
inference(backward_demodulation,[status(thm)],[f617,f593]) ).
fof(f645,plain,
! [X0,X1,X2] :
( ~ m1_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)
| ~ 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,X2,k1_waybel34(X0,X1,X2)),X0,X1)
| ~ m2_relset_1(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(k1_waybel34(X0,X1,X2))
| ~ v17_waybel_0(X2,X0,X1)
| ~ v3_lattice3(X1)
| ~ v3_lattice3(X0)
| ~ 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)
| ~ 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)],[f600,f337]) ).
fof(f646,plain,
! [X0,X1,X2] :
( ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| v3_waybel_1(k1_waybel_1(X0,X1,X2,k1_waybel34(X0,X1,X2)),X0,X1)
| ~ m2_relset_1(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(k1_waybel34(X0,X1,X2))
| ~ v17_waybel_0(X2,X0,X1)
| ~ v3_lattice3(X1)
| ~ v3_lattice3(X0)
| ~ 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)
| ~ 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)],[f645]) ).
fof(f647,plain,
! [X0,X1,X2] :
( ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| v3_waybel_1(k1_waybel_1(X0,X1,X2,k1_waybel34(X0,X1,X2)),X0,X1)
| ~ m2_relset_1(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(k1_waybel34(X0,X1,X2))
| ~ v17_waybel_0(X2,X0,X1)
| ~ v3_lattice3(X1)
| ~ v3_lattice3(X0)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ 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)],[f646,f568]) ).
fof(f648,plain,
! [X0,X1,X2] :
( ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| v3_waybel_1(k1_waybel_1(X0,X1,X2,k1_waybel34(X0,X1,X2)),X0,X1)
| ~ m2_relset_1(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0))
| ~ v17_waybel_0(X2,X0,X1)
| ~ v3_lattice3(X1)
| ~ v3_lattice3(X0)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ 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)],[f647,f336]) ).
fof(f649,plain,
! [X0,X1,X2,X3] :
( r3_waybel_1(X0,k7_yellow_2(u1_struct_0(X1),X0,k1_waybel34(X0,X1,X2),X3),k5_pre_topc(X0,X1,X2,k7_waybel_0(X1,X3)))
| ~ m1_subset_1(X3,u1_struct_0(X1))
| ~ m2_relset_1(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(k1_waybel34(X0,X1,X2))
| ~ 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)
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0))
| ~ v17_waybel_0(X2,X0,X1)
| ~ v3_lattice3(X1)
| ~ v3_lattice3(X0)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ 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)],[f648,f575]) ).
fof(f650,plain,
! [X0,X1,X2,X3] :
( r3_waybel_1(X0,k7_yellow_2(u1_struct_0(X1),X0,k1_waybel34(X0,X1,X2),X3),k5_pre_topc(X0,X1,X2,k7_waybel_0(X1,X3)))
| ~ m1_subset_1(X3,u1_struct_0(X1))
| ~ v1_funct_2(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(k1_waybel34(X0,X1,X2))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X1)
| v3_struct_0(X0)
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0))
| ~ v17_waybel_0(X2,X0,X1)
| ~ v3_lattice3(X1)
| ~ v3_lattice3(X0)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ 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)],[f649]) ).
fof(f651,plain,
! [X0,X1,X2,X3] :
( r3_waybel_1(X0,k7_yellow_2(u1_struct_0(X1),X0,k1_waybel34(X0,X1,X2),X3),k5_pre_topc(X0,X1,X2,k7_waybel_0(X1,X3)))
| ~ m1_subset_1(X3,u1_struct_0(X1))
| ~ v1_funct_2(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(k1_waybel34(X0,X1,X2))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X1)
| v3_struct_0(X0)
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0))
| ~ v17_waybel_0(X2,X0,X1)
| ~ v3_lattice3(X1)
| ~ v3_lattice3(X0)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ 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)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f650,f252]) ).
fof(f652,plain,
! [X0,X1,X2,X3] :
( r3_waybel_1(X0,k7_yellow_2(u1_struct_0(X1),X0,k1_waybel34(X0,X1,X2),X3),k5_pre_topc(X0,X1,X2,k7_waybel_0(X1,X3)))
| ~ m1_subset_1(X3,u1_struct_0(X1))
| ~ v1_funct_2(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(k1_waybel34(X0,X1,X2))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X1)
| v3_struct_0(X0)
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0))
| ~ v17_waybel_0(X2,X0,X1)
| ~ v3_lattice3(X1)
| ~ v3_lattice3(X0)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ 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)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f651,f253]) ).
fof(f653,plain,
! [X0,X1,X2,X3] :
( ~ m1_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)
| ~ 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)
| r3_waybel_1(X0,k7_yellow_2(u1_struct_0(X1),X0,k1_waybel34(X0,X1,X2),X3),k5_pre_topc(X0,X1,X2,k7_waybel_0(X1,X3)))
| ~ m1_subset_1(X3,u1_struct_0(X1))
| ~ v1_funct_1(k1_waybel34(X0,X1,X2))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X1)
| v3_struct_0(X0)
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0))
| ~ v17_waybel_0(X2,X0,X1)
| ~ v3_lattice3(X1)
| ~ v3_lattice3(X0)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ 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)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0) ),
inference(resolution,[status(thm)],[f652,f337]) ).
fof(f654,plain,
! [X0,X1,X2,X3] :
( ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| r3_waybel_1(X0,k7_yellow_2(u1_struct_0(X1),X0,k1_waybel34(X0,X1,X2),X3),k5_pre_topc(X0,X1,X2,k7_waybel_0(X1,X3)))
| ~ m1_subset_1(X3,u1_struct_0(X1))
| ~ v1_funct_1(k1_waybel34(X0,X1,X2))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X1)
| v3_struct_0(X0)
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0))
| ~ v17_waybel_0(X2,X0,X1)
| ~ v3_lattice3(X1)
| ~ v3_lattice3(X0)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ 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)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f653]) ).
fof(f655,plain,
! [X0,X1,X2,X3] :
( ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| r3_waybel_1(X0,k7_yellow_2(u1_struct_0(X1),X0,k1_waybel34(X0,X1,X2),X3),k5_pre_topc(X0,X1,X2,k7_waybel_0(X1,X3)))
| ~ m1_subset_1(X3,u1_struct_0(X1))
| ~ v1_funct_1(k1_waybel34(X0,X1,X2))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X1)
| v3_struct_0(X0)
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0))
| ~ v17_waybel_0(X2,X0,X1)
| ~ v3_lattice3(X1)
| ~ v3_lattice3(X0)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f654,f252]) ).
fof(f656,plain,
! [X0,X1,X2,X3] :
( ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| r3_waybel_1(X0,k7_yellow_2(u1_struct_0(X1),X0,k1_waybel34(X0,X1,X2),X3),k5_pre_topc(X0,X1,X2,k7_waybel_0(X1,X3)))
| ~ m1_subset_1(X3,u1_struct_0(X1))
| ~ v1_funct_1(k1_waybel34(X0,X1,X2))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X1)
| v3_struct_0(X0)
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0))
| ~ v17_waybel_0(X2,X0,X1)
| ~ v3_lattice3(X1)
| ~ v3_lattice3(X0)
| ~ 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)
| ~ l1_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f655,f253]) ).
fof(f657,plain,
! [X0] :
( ~ v2_lattice3(sK0_skl)
| ~ v1_lattice3(sK0_skl)
| r3_waybel_1(sK0_skl,k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0),k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))
| ~ m1_subset_1(X0,u1_struct_0(sK1_skl))
| ~ v1_funct_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl))
| ~ m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
| v3_struct_0(sK1_skl)
| v3_struct_0(sK0_skl)
| ~ m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
| ~ m2_relset_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))
| ~ v3_lattice3(sK1_skl)
| ~ v3_lattice3(sK0_skl)
| ~ v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
| ~ v1_funct_1(sK2_skl)
| ~ l1_orders_2(sK1_skl)
| ~ v4_orders_2(sK1_skl)
| ~ v3_orders_2(sK1_skl)
| ~ v2_orders_2(sK1_skl)
| ~ l1_orders_2(sK0_skl)
| ~ v4_orders_2(sK0_skl)
| ~ v3_orders_2(sK0_skl)
| ~ v2_orders_2(sK0_skl) ),
inference(resolution,[status(thm)],[f656,f150]) ).
fof(f658,definition,
( sQ2_spl
<=> v2_orders_2(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f660,plain,
( sQ2_spl
| ~ v2_orders_2(sK0_skl) ),
inference(component_clause,[status(thm)],[f658]) ).
fof(f661,definition,
( sQ3_spl
<=> v3_orders_2(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f663,plain,
( sQ3_spl
| ~ v3_orders_2(sK0_skl) ),
inference(component_clause,[status(thm)],[f661]) ).
fof(f664,definition,
( sQ4_spl
<=> v4_orders_2(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f666,plain,
( sQ4_spl
| ~ v4_orders_2(sK0_skl) ),
inference(component_clause,[status(thm)],[f664]) ).
fof(f667,definition,
( sQ5_spl
<=> l1_orders_2(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f669,plain,
( sQ5_spl
| ~ l1_orders_2(sK0_skl) ),
inference(component_clause,[status(thm)],[f667]) ).
fof(f670,definition,
( sQ6_spl
<=> v2_orders_2(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f672,plain,
( sQ6_spl
| ~ v2_orders_2(sK1_skl) ),
inference(component_clause,[status(thm)],[f670]) ).
fof(f673,definition,
( sQ7_spl
<=> v3_orders_2(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f675,plain,
( sQ7_spl
| ~ v3_orders_2(sK1_skl) ),
inference(component_clause,[status(thm)],[f673]) ).
fof(f676,definition,
( sQ8_spl
<=> v4_orders_2(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f678,plain,
( sQ8_spl
| ~ v4_orders_2(sK1_skl) ),
inference(component_clause,[status(thm)],[f676]) ).
fof(f679,definition,
( sQ9_spl
<=> l1_orders_2(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f681,plain,
( sQ9_spl
| ~ l1_orders_2(sK1_skl) ),
inference(component_clause,[status(thm)],[f679]) ).
fof(f682,definition,
( sQ10_spl
<=> v1_funct_1(sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f684,plain,
( sQ10_spl
| ~ v1_funct_1(sK2_skl) ),
inference(component_clause,[status(thm)],[f682]) ).
fof(f685,definition,
( sQ11_spl
<=> v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f687,plain,
( sQ11_spl
| ~ v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)) ),
inference(component_clause,[status(thm)],[f685]) ).
fof(f688,definition,
( sQ12_spl
<=> v3_lattice3(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f690,plain,
( sQ12_spl
| ~ v3_lattice3(sK0_skl) ),
inference(component_clause,[status(thm)],[f688]) ).
fof(f691,definition,
( sQ13_spl
<=> v3_lattice3(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f693,plain,
( sQ13_spl
| ~ v3_lattice3(sK1_skl) ),
inference(component_clause,[status(thm)],[f691]) ).
fof(f694,definition,
( sQ14_spl
<=> m2_relset_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f696,plain,
( sQ14_spl
| ~ m2_relset_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl)) ),
inference(component_clause,[status(thm)],[f694]) ).
fof(f697,definition,
( sQ15_spl
<=> m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f699,plain,
( sQ15_spl
| ~ m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)) ),
inference(component_clause,[status(thm)],[f697]) ).
fof(f700,definition,
( sQ16_spl
<=> v3_struct_0(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f701,plain,
( ~ sQ16_spl
| v3_struct_0(sK0_skl) ),
inference(component_clause,[status(thm)],[f700]) ).
fof(f703,definition,
( sQ17_spl
<=> v3_struct_0(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f704,plain,
( ~ sQ17_spl
| v3_struct_0(sK1_skl) ),
inference(component_clause,[status(thm)],[f703]) ).
fof(f706,definition,
( sQ18_spl
<=> m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f708,plain,
( sQ18_spl
| ~ m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)) ),
inference(component_clause,[status(thm)],[f706]) ).
fof(f709,definition,
( sQ19_spl
<=> v1_funct_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl)) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f711,plain,
( sQ19_spl
| ~ v1_funct_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl)) ),
inference(component_clause,[status(thm)],[f709]) ).
fof(f712,definition,
! [X0] :
( sQ20_spl
<=> ( r3_waybel_1(sK0_skl,k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0),k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))
| ~ m1_subset_1(X0,u1_struct_0(sK1_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f713,plain,
! [X0] :
( ~ sQ20_spl
| r3_waybel_1(sK0_skl,k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0),k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))
| ~ m1_subset_1(X0,u1_struct_0(sK1_skl)) ),
inference(component_clause,[status(thm)],[f712]) ).
fof(f715,definition,
( sQ21_spl
<=> v1_lattice3(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f717,plain,
( sQ21_spl
| ~ v1_lattice3(sK0_skl) ),
inference(component_clause,[status(thm)],[f715]) ).
fof(f718,definition,
( sQ22_spl
<=> v2_lattice3(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f720,plain,
( sQ22_spl
| ~ v2_lattice3(sK0_skl) ),
inference(component_clause,[status(thm)],[f718]) ).
fof(f721,plain,
( ~ sQ22_spl
| ~ sQ21_spl
| sQ20_spl
| ~ sQ19_spl
| ~ sQ18_spl
| sQ17_spl
| sQ16_spl
| ~ sQ15_spl
| ~ sQ14_spl
| ~ sQ13_spl
| ~ sQ12_spl
| ~ sQ11_spl
| ~ sQ10_spl
| ~ sQ9_spl
| ~ sQ8_spl
| ~ sQ7_spl
| ~ sQ6_spl
| ~ sQ5_spl
| ~ sQ4_spl
| ~ sQ3_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f657,f658,f661,f664,f667,f670,f673,f676,f679,f682,f685,f688,f691,f694,f697,f700,f703,f706,f709,f712,f715,f718]) ).
fof(f722,plain,
( sQ22_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f720,f138]) ).
fof(f723,plain,
sQ22_spl,
inference(contradiction_clause,[status(thm)],[f722]) ).
fof(f724,plain,
( sQ21_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f717,f137]) ).
fof(f725,plain,
sQ21_spl,
inference(contradiction_clause,[status(thm)],[f724]) ).
fof(f727,plain,
! [X0] :
( ~ sQ20_spl
| k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0) = k2_yellow_0(sK0_skl,k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))
| ~ m1_subset_1(k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0),u1_struct_0(sK0_skl))
| ~ l1_orders_2(sK0_skl)
| v3_struct_0(sK0_skl)
| ~ m1_subset_1(X0,u1_struct_0(sK1_skl)) ),
inference(resolution,[status(thm)],[f713,f330]) ).
fof(f732,definition,
! [X0] :
( sQ24_spl
<=> ( k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0) = k2_yellow_0(sK0_skl,k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))
| ~ m1_subset_1(k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0),u1_struct_0(sK0_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK1_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f733,plain,
! [X0] :
( ~ sQ24_spl
| k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0) = k2_yellow_0(sK0_skl,k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))
| ~ m1_subset_1(k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0),u1_struct_0(sK0_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK1_skl)) ),
inference(component_clause,[status(thm)],[f732]) ).
fof(f735,plain,
( ~ sQ20_spl
| ~ sQ5_spl
| sQ16_spl
| sQ24_spl ),
inference(split_clause,[status(thm)],[f727,f732,f700,f667,f712]) ).
fof(f736,plain,
( sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f669,f140]) ).
fof(f737,plain,
sQ5_spl,
inference(contradiction_clause,[status(thm)],[f736]) ).
fof(f738,plain,
( ~ sQ16_spl
| ~ v2_lattice3(sK0_skl)
| ~ l1_orders_2(sK0_skl) ),
inference(resolution,[status(thm)],[f701,f280]) ).
fof(f740,plain,
( ~ sQ16_spl
| ~ sQ22_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f738,f667,f718,f700]) ).
fof(f748,plain,
( sQ19_spl
| ~ m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
| ~ v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_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)],[f711,f336]) ).
fof(f750,definition,
( sQ25_spl
<=> v1_lattice3(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f752,plain,
( sQ25_spl
| ~ v1_lattice3(sK1_skl) ),
inference(component_clause,[status(thm)],[f750]) ).
fof(f753,definition,
( sQ26_spl
<=> v2_lattice3(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f755,plain,
( sQ26_spl
| ~ v2_lattice3(sK1_skl) ),
inference(component_clause,[status(thm)],[f753]) ).
fof(f756,plain,
( sQ19_spl
| ~ sQ15_spl
| ~ sQ11_spl
| ~ sQ10_spl
| ~ sQ9_spl
| ~ sQ26_spl
| ~ sQ25_spl
| ~ sQ8_spl
| ~ sQ7_spl
| ~ sQ6_spl
| ~ sQ5_spl
| ~ sQ22_spl
| ~ sQ21_spl
| ~ sQ4_spl
| ~ sQ3_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f748,f658,f661,f664,f715,f718,f667,f670,f673,f676,f750,f753,f679,f682,f685,f697,f709]) ).
fof(f757,plain,
( sQ15_spl
| ~ m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)) ),
inference(resolution,[status(thm)],[f699,f567]) ).
fof(f758,plain,
( sQ15_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f757,f151]) ).
fof(f759,plain,
sQ15_spl,
inference(contradiction_clause,[status(thm)],[f758]) ).
fof(f760,plain,
( sQ11_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f687,f149]) ).
fof(f761,plain,
sQ11_spl,
inference(contradiction_clause,[status(thm)],[f760]) ).
fof(f762,plain,
( sQ10_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f684,f148]) ).
fof(f763,plain,
sQ10_spl,
inference(contradiction_clause,[status(thm)],[f762]) ).
fof(f764,plain,
( sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f681,f147]) ).
fof(f765,plain,
sQ9_spl,
inference(contradiction_clause,[status(thm)],[f764]) ).
fof(f766,plain,
( sQ8_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f678,f143]) ).
fof(f767,plain,
sQ8_spl,
inference(contradiction_clause,[status(thm)],[f766]) ).
fof(f768,plain,
( sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f675,f142]) ).
fof(f769,plain,
sQ7_spl,
inference(contradiction_clause,[status(thm)],[f768]) ).
fof(f770,plain,
( sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f672,f141]) ).
fof(f771,plain,
sQ6_spl,
inference(contradiction_clause,[status(thm)],[f770]) ).
fof(f772,plain,
( sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f666,f136]) ).
fof(f773,plain,
sQ4_spl,
inference(contradiction_clause,[status(thm)],[f772]) ).
fof(f774,plain,
( sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f663,f135]) ).
fof(f775,plain,
sQ3_spl,
inference(contradiction_clause,[status(thm)],[f774]) ).
fof(f776,plain,
( sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f660,f134]) ).
fof(f777,plain,
sQ2_spl,
inference(contradiction_clause,[status(thm)],[f776]) ).
fof(f778,plain,
( sQ26_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f755,f145]) ).
fof(f779,plain,
sQ26_spl,
inference(contradiction_clause,[status(thm)],[f778]) ).
fof(f780,plain,
( sQ25_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f752,f144]) ).
fof(f781,plain,
sQ25_spl,
inference(contradiction_clause,[status(thm)],[f780]) ).
fof(f782,plain,
( sQ18_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f708,f151]) ).
fof(f783,plain,
sQ18_spl,
inference(contradiction_clause,[status(thm)],[f782]) ).
fof(f784,plain,
( ~ sQ17_spl
| ~ v2_lattice3(sK1_skl)
| ~ l1_orders_2(sK1_skl) ),
inference(resolution,[status(thm)],[f704,f280]) ).
fof(f786,plain,
( ~ sQ17_spl
| ~ sQ26_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f784,f679,f753,f703]) ).
fof(f789,plain,
( sQ14_spl
| ~ m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
| ~ v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_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)],[f696,f338]) ).
fof(f791,plain,
( sQ14_spl
| ~ sQ15_spl
| ~ sQ11_spl
| ~ sQ10_spl
| ~ sQ9_spl
| ~ sQ26_spl
| ~ sQ25_spl
| ~ sQ8_spl
| ~ sQ7_spl
| ~ sQ6_spl
| ~ sQ5_spl
| ~ sQ22_spl
| ~ sQ21_spl
| ~ sQ4_spl
| ~ sQ3_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f789,f658,f661,f664,f715,f718,f667,f670,f673,f676,f750,f753,f679,f682,f685,f697,f694]) ).
fof(f792,plain,
( sQ13_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f693,f146]) ).
fof(f793,plain,
sQ13_spl,
inference(contradiction_clause,[status(thm)],[f792]) ).
fof(f794,plain,
( sQ12_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f690,f139]) ).
fof(f795,plain,
sQ12_spl,
inference(contradiction_clause,[status(thm)],[f794]) ).
fof(f804,definition,
( sQ28_spl
<=> v1_xboole_0(u1_struct_0(sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f805,plain,
( ~ sQ28_spl
| v1_xboole_0(u1_struct_0(sK1_skl)) ),
inference(component_clause,[status(thm)],[f804]) ).
fof(f807,definition,
( sQ29_spl
<=> l1_struct_0(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f809,plain,
( sQ29_spl
| ~ l1_struct_0(sK0_skl) ),
inference(component_clause,[status(thm)],[f807]) ).
fof(f810,definition,
( sQ30_spl
<=> v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f812,plain,
( sQ30_spl
| ~ v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl)) ),
inference(component_clause,[status(thm)],[f810]) ).
fof(f813,definition,
( sQ31_spl
<=> m1_relset_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f815,plain,
( sQ31_spl
| ~ m1_relset_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl)) ),
inference(component_clause,[status(thm)],[f813]) ).
fof(f817,plain,
! [X0] :
( ~ sQ24_spl
| ~ m1_subset_1(X0,u1_struct_0(sK1_skl))
| ~ m1_relset_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))
| ~ v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))
| ~ v1_funct_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl))
| ~ l1_struct_0(sK0_skl)
| v3_struct_0(sK0_skl)
| v1_xboole_0(u1_struct_0(sK1_skl))
| k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0) = k2_yellow_0(sK0_skl,k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))
| ~ m1_subset_1(X0,u1_struct_0(sK1_skl)) ),
inference(resolution,[status(thm)],[f733,f352]) ).
fof(f818,definition,
! [X0] :
( sQ32_spl
<=> ( ~ m1_subset_1(X0,u1_struct_0(sK1_skl))
| k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0) = k2_yellow_0(sK0_skl,k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))
| ~ m1_subset_1(X0,u1_struct_0(sK1_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f819,plain,
! [X0] :
( ~ sQ32_spl
| ~ m1_subset_1(X0,u1_struct_0(sK1_skl))
| k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0) = k2_yellow_0(sK0_skl,k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))
| ~ m1_subset_1(X0,u1_struct_0(sK1_skl)) ),
inference(component_clause,[status(thm)],[f818]) ).
fof(f821,plain,
( ~ sQ24_spl
| ~ sQ31_spl
| ~ sQ30_spl
| ~ sQ19_spl
| ~ sQ29_spl
| sQ16_spl
| sQ28_spl
| sQ32_spl ),
inference(split_clause,[status(thm)],[f817,f818,f804,f700,f807,f709,f810,f813,f732]) ).
fof(f822,plain,
( sQ31_spl
| ~ m2_relset_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl)) ),
inference(resolution,[status(thm)],[f815,f567]) ).
fof(f823,plain,
( sQ31_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f822,f694,f813]) ).
fof(f824,plain,
( sQ30_spl
| ~ m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
| ~ v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_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)],[f812,f337]) ).
fof(f825,plain,
( sQ30_spl
| ~ sQ15_spl
| ~ sQ11_spl
| ~ sQ10_spl
| ~ sQ9_spl
| ~ sQ26_spl
| ~ sQ25_spl
| ~ sQ8_spl
| ~ sQ7_spl
| ~ sQ6_spl
| ~ sQ5_spl
| ~ sQ22_spl
| ~ sQ21_spl
| ~ sQ4_spl
| ~ sQ3_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f824,f658,f661,f664,f715,f718,f667,f670,f673,f676,f750,f753,f679,f682,f685,f697,f810]) ).
fof(f826,plain,
( sQ29_spl
| ~ l1_orders_2(sK0_skl) ),
inference(resolution,[status(thm)],[f809,f354]) ).
fof(f827,plain,
( sQ29_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f826,f667,f807]) ).
fof(f840,plain,
( ~ sQ28_spl
| u1_struct_0(sK1_skl) = sK18_skl ),
inference(resolution,[status(thm)],[f805,f619]) ).
fof(f879,definition,
( sQ36_spl
<=> l1_struct_0(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f881,plain,
( sQ36_spl
| ~ l1_struct_0(sK1_skl) ),
inference(component_clause,[status(thm)],[f879]) ).
fof(f986,plain,
( sQ36_spl
| ~ l1_orders_2(sK1_skl) ),
inference(resolution,[status(thm)],[f881,f354]) ).
fof(f987,plain,
( sQ36_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f986,f679,f879]) ).
fof(f989,plain,
! [X0] :
( ~ sQ32_spl
| k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),X0) = k2_yellow_0(sK0_skl,k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,X0)))
| ~ m1_subset_1(X0,u1_struct_0(sK1_skl)) ),
inference(duplicate_literals_removal,[status(thm)],[f819]) ).
fof(f1037,plain,
( ~ sQ32_spl
| k7_yellow_2(u1_struct_0(sK1_skl),sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl),sK3_skl) = k2_yellow_0(sK0_skl,k5_pre_topc(sK0_skl,sK1_skl,sK2_skl,k7_waybel_0(sK1_skl,sK3_skl))) ),
inference(resolution,[status(thm)],[f989,f152]) ).
fof(f1041,plain,
( ~ sQ32_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1037,f153]) ).
fof(f1042,plain,
~ sQ32_spl,
inference(contradiction_clause,[status(thm)],[f1041]) ).
fof(f1111,plain,
( ~ sQ28_spl
| ~ v1_xboole_0(sK18_skl)
| ~ l1_struct_0(sK1_skl)
| v3_struct_0(sK1_skl) ),
inference(paramodulation,[status(thm)],[f840,f417]) ).
fof(f1112,definition,
( sQ58_spl
<=> v1_xboole_0(sK18_skl) ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f1114,plain,
( sQ58_spl
| ~ v1_xboole_0(sK18_skl) ),
inference(component_clause,[status(thm)],[f1112]) ).
fof(f1115,plain,
( ~ sQ28_spl
| ~ sQ58_spl
| ~ sQ36_spl
| sQ17_spl ),
inference(split_clause,[status(thm)],[f1111,f703,f879,f1112,f804]) ).
fof(f1116,plain,
( sQ58_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1114,f499]) ).
fof(f1117,plain,
sQ58_spl,
inference(contradiction_clause,[status(thm)],[f1116]) ).
fof(f1118,plain,
$false,
inference(sat_refutation,[status(thm)],[f721,f723,f725,f735,f737,f740,f756,f759,f761,f763,f765,f767,f769,f771,f773,f775,f777,f779,f781,f783,f786,f791,f793,f795,f821,f823,f825,f827,f987,f1042,f1115,f1117]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT352+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/10.44 % Computer : n004.cluster.edu
% 0.15/10.44 % Model : x86_64 x86_64
% 0.15/10.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/10.44 % Memory : 8046.5625MB
% 0.15/10.44 % OS : Linux 6.8.0-71-generic
% 0.15/10.44 % CPULimit : 300
% 0.15/10.44 % WCLimit : 300
% 0.15/10.44 % DateTime : Sun Sep 20 23:46:45 UTC 2026
% 0.15/10.44 % CPUTime :
% 0.15/10.48 % Drodi V4.1.1
% 0.20/10.54 % Refutation found
% 0.20/10.54 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.20/10.54 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.20/10.59 % Elapsed time: 0.131969 seconds
% 0.20/10.59 % CPU time: 0.508755 seconds
% 0.20/10.59 % Total memory used: 117.393 MB
% 0.20/10.59 % Net memory used: 117.177 MB
%------------------------------------------------------------------------------