%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LAT369+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n008.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:59 PM UTC 2026
% Result : Theorem 132.29s 17.57s
% Output : CNFRefutation 131.07s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 60
% Syntax : Number of formulae : 246 ( 30 unt; 38 def)
% Number of atoms : 1451 ( 24 equ)
% Maximal formula atoms : 28 ( 5 avg)
% Number of connectives : 2035 ( 830 ~; 863 |; 261 &)
% ( 41 <=>; 40 =>; 0 <=; 0 <~>)
% Maximal formula depth : 31 ( 7 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 79 ( 77 usr; 39 prp; 0-3 aty)
% Number of functors : 12 ( 12 usr; 2 con; 0-3 aty)
% Number of variables : 193 ( 191 !; 2 ?)
% 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] :
( ( m2_relset_1(B,u1_struct_0(A),u1_struct_0(A))
& v7_waybel_1(B,A)
& v1_funct_2(B,u1_struct_0(A),u1_struct_0(A))
& v1_funct_1(B) )
=> ( v4_waybel_0(k2_yellow_2(A,A,B),A)
=> v1_waybel34(k2_waybel_1(A,A,B),A,k2_yellow_2(A,A,B)) ) ) ),
file('/export/starexec/sandbox2/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] :
( ( m2_relset_1(B,u1_struct_0(A),u1_struct_0(A))
& v7_waybel_1(B,A)
& v1_funct_2(B,u1_struct_0(A),u1_struct_0(A))
& v1_funct_1(B) )
=> ( v4_waybel_0(k2_yellow_2(A,A,B),A)
=> v1_waybel34(k2_waybel_1(A,A,B),A,k2_yellow_2(A,A,B)) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f25,axiom,
! [A,B,C] :
( m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B)))
=> v1_relat_1(C) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f31,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/sandbox2/benchmark/theBenchmark.p') ).
fof(f36,axiom,
! [A] :
( l1_orders_2(A)
=> ( v2_lattice3(A)
=> ~ v3_struct_0(A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f41,axiom,
! [A] :
( ( l1_orders_2(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_relset_1(B,u1_struct_0(A),u1_struct_0(A))
=> ( ( v7_waybel_1(B,A)
& v1_funct_2(B,u1_struct_0(A),u1_struct_0(A))
& v1_funct_1(B) )
=> ( v6_waybel_1(B,A)
& v1_partfun1(B,u1_struct_0(A),u1_struct_0(A))
& v1_funct_2(B,u1_struct_0(A),u1_struct_0(A))
& ~ v1_xboole_0(B)
& v1_funct_1(B) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f55,axiom,
! [A] :
( ( l1_orders_2(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( l1_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) )
=> k2_waybel_1(A,B,C) = k8_relat_1(u1_struct_0(k2_yellow_2(A,B,C)),C) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f56,axiom,
! [A] :
( ( l1_orders_2(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( l1_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) )
=> k3_waybel_1(A,B,C) = k7_grcat_1(k2_yellow_2(A,B,C)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f61,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/sandbox2/benchmark/theBenchmark.p') ).
fof(f62,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)
& ~ v3_struct_0(B)
& l1_orders_2(A)
& ~ v3_struct_0(A) )
=> ( m2_relset_1(k2_waybel_1(A,B,C),u1_struct_0(A),u1_struct_0(k2_yellow_2(A,B,C)))
& v1_funct_2(k2_waybel_1(A,B,C),u1_struct_0(A),u1_struct_0(k2_yellow_2(A,B,C)))
& v1_funct_1(k2_waybel_1(A,B,C)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f63,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)
& ~ v3_struct_0(B)
& l1_orders_2(A)
& ~ v3_struct_0(A) )
=> ( m1_yellow_0(k2_yellow_2(A,B,C),B)
& v4_yellow_0(k2_yellow_2(A,B,C),B)
& v1_orders_2(k2_yellow_2(A,B,C)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f72,axiom,
! [A] :
( l1_orders_2(A)
=> ! [B] :
( m1_yellow_0(B,A)
=> l1_orders_2(B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f73,axiom,
! [A,B,C] :
( m2_relset_1(C,A,B)
=> m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f82,axiom,
! [A,B] :
( ( m1_relset_1(B,u1_struct_0(A),u1_struct_0(A))
& v7_waybel_1(B,A)
& v1_funct_2(B,u1_struct_0(A),u1_struct_0(A))
& v1_funct_1(B)
& l1_orders_2(A)
& v4_orders_2(A)
& v3_orders_2(A)
& v2_orders_2(A)
& ~ v3_struct_0(A) )
=> ( v3_waybel_0(k2_yellow_2(A,A,B),A)
& v7_yellow_0(k2_yellow_2(A,A,B),A)
& v5_yellow_0(k2_yellow_2(A,A,B),A)
& v4_yellow_0(k2_yellow_2(A,A,B),A)
& v4_orders_2(k2_yellow_2(A,A,B))
& v3_orders_2(k2_yellow_2(A,A,B))
& v2_orders_2(k2_yellow_2(A,A,B))
& v1_orders_2(k2_yellow_2(A,A,B))
& ~ v3_struct_0(k2_yellow_2(A,A,B)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f83,axiom,
! [A,B] :
( ( m1_relset_1(B,u1_struct_0(A),u1_struct_0(A))
& v6_waybel_1(B,A)
& v1_funct_2(B,u1_struct_0(A),u1_struct_0(A))
& v1_funct_1(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) )
=> ( v3_lattice3(k2_yellow_2(A,A,B))
& v2_lattice3(k2_yellow_2(A,A,B))
& v1_lattice3(k2_yellow_2(A,A,B))
& v25_waybel_0(k2_yellow_2(A,A,B))
& v24_waybel_0(k2_yellow_2(A,A,B))
& v4_yellow_0(k2_yellow_2(A,A,B),A)
& v3_yellow_0(k2_yellow_2(A,A,B))
& v2_yellow_0(k2_yellow_2(A,A,B))
& v1_yellow_0(k2_yellow_2(A,A,B))
& v4_orders_2(k2_yellow_2(A,A,B))
& v3_orders_2(k2_yellow_2(A,A,B))
& v2_orders_2(k2_yellow_2(A,A,B))
& v1_orders_2(k2_yellow_2(A,A,B))
& ~ v3_struct_0(k2_yellow_2(A,A,B)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f90,axiom,
! [A,B,C] :
( ( m1_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) )
=> ( v5_orders_3(k2_waybel34(A,B,C),A,B)
& v4_waybel_1(k2_waybel34(A,B,C),A,B)
& v21_waybel_0(k2_waybel34(A,B,C),A,B)
& v19_waybel_0(k2_waybel34(A,B,C),A,B)
& v17_waybel_0(k2_waybel34(A,B,C),A,B)
& v1_partfun1(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_xboole_0(k2_waybel34(A,B,C))
& v1_funct_1(k2_waybel34(A,B,C))
& v1_relat_1(k2_waybel34(A,B,C)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f91,axiom,
! [A] :
( l1_orders_2(A)
=> ( v23_waybel_0(k7_grcat_1(A),A,A)
& v1_funct_2(k7_grcat_1(A),u1_struct_0(A),u1_struct_0(A))
& v1_funct_1(k7_grcat_1(A))
& v1_relat_1(k7_grcat_1(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f92,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)
& ~ v3_struct_0(B)
& l1_orders_2(A)
& ~ v3_struct_0(A) )
=> ( v4_yellow_0(k2_yellow_2(A,B,C),B)
& v1_orders_2(k2_yellow_2(A,B,C))
& ~ v3_struct_0(k2_yellow_2(A,B,C)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f98,axiom,
! [A,B] :
( ( v1_funct_1(B)
& v1_relat_1(B) )
=> ( v1_funct_1(k8_relat_1(A,B))
& v1_relat_1(k8_relat_1(A,B)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f134,axiom,
! [A,B,C] :
( m2_relset_1(C,A,B)
<=> m1_relset_1(C,A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f137,axiom,
! [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) )
=> ( v22_waybel_0(C,A,B)
=> v1_waybel34(k1_waybel34(A,B,C),B,A) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f139,axiom,
! [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] :
( ( m2_relset_1(B,u1_struct_0(A),u1_struct_0(A))
& v7_waybel_1(B,A)
& v1_funct_2(B,u1_struct_0(A),u1_struct_0(A))
& v1_funct_1(B) )
=> ( k1_waybel34(k2_yellow_2(A,A,B),A,k3_waybel_1(A,A,B)) = k2_waybel_1(A,A,B)
& k2_waybel34(k2_yellow_2(A,A,B),A,k2_waybel_1(A,A,B)) = k3_waybel_1(A,A,B)
& v17_waybel_0(k3_waybel_1(A,A,B),k2_yellow_2(A,A,B),A)
& v18_waybel_0(k2_waybel_1(A,A,B),A,k2_yellow_2(A,A,B)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f141,axiom,
! [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] :
( ( m2_relset_1(B,u1_struct_0(A),u1_struct_0(A))
& v7_waybel_1(B,A)
& v1_funct_2(B,u1_struct_0(A),u1_struct_0(A))
& v1_funct_1(B) )
=> ( v4_waybel_0(k2_yellow_2(A,A,B),A)
<=> v22_waybel_0(k3_waybel_1(A,A,B),k2_yellow_2(A,A,B),A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f147,plain,
? [A] :
( ? [B] :
( ~ v1_waybel34(k2_waybel_1(A,A,B),A,k2_yellow_2(A,A,B))
& v4_waybel_0(k2_yellow_2(A,A,B),A)
& m2_relset_1(B,u1_struct_0(A),u1_struct_0(A))
& v7_waybel_1(B,A)
& v1_funct_2(B,u1_struct_0(A),u1_struct_0(A))
& v1_funct_1(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(f148,plain,
( ~ v1_waybel34(k2_waybel_1(sK0_skl,sK0_skl,sK1_skl),sK0_skl,k2_yellow_2(sK0_skl,sK0_skl,sK1_skl))
& v4_waybel_0(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl),sK0_skl)
& m2_relset_1(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))
& v7_waybel_1(sK1_skl,sK0_skl)
& v1_funct_2(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))
& v1_funct_1(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]),skolemize(A,sK0_skl),skolemize(B,sK1_skl)],[f147]) ).
fof(f149,plain,
v2_orders_2(sK0_skl),
inference(cnf_transformation,[status(thm)],[f148]) ).
fof(f150,plain,
v3_orders_2(sK0_skl),
inference(cnf_transformation,[status(thm)],[f148]) ).
fof(f151,plain,
v4_orders_2(sK0_skl),
inference(cnf_transformation,[status(thm)],[f148]) ).
fof(f152,plain,
v1_lattice3(sK0_skl),
inference(cnf_transformation,[status(thm)],[f148]) ).
fof(f153,plain,
v2_lattice3(sK0_skl),
inference(cnf_transformation,[status(thm)],[f148]) ).
fof(f154,plain,
v3_lattice3(sK0_skl),
inference(cnf_transformation,[status(thm)],[f148]) ).
fof(f155,plain,
l1_orders_2(sK0_skl),
inference(cnf_transformation,[status(thm)],[f148]) ).
fof(f156,plain,
v1_funct_1(sK1_skl),
inference(cnf_transformation,[status(thm)],[f148]) ).
fof(f157,plain,
v1_funct_2(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),
inference(cnf_transformation,[status(thm)],[f148]) ).
fof(f158,plain,
v7_waybel_1(sK1_skl,sK0_skl),
inference(cnf_transformation,[status(thm)],[f148]) ).
fof(f159,plain,
m2_relset_1(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),
inference(cnf_transformation,[status(thm)],[f148]) ).
fof(f160,plain,
v4_waybel_0(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl),sK0_skl),
inference(cnf_transformation,[status(thm)],[f148]) ).
fof(f161,plain,
~ v1_waybel34(k2_waybel_1(sK0_skl,sK0_skl,sK1_skl),sK0_skl,k2_yellow_2(sK0_skl,sK0_skl,sK1_skl)),
inference(cnf_transformation,[status(thm)],[f148]) ).
fof(f252,plain,
! [A,B,C] :
( v1_relat_1(C)
| ~ m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) ),
inference(pre_NNF_transformation,[status(thm)],[f25]) ).
fof(f253,plain,
! [C] :
( v1_relat_1(C)
| ! [A,B] : ~ m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) ),
inference(miniscoping,[status(thm)],[f252]) ).
fof(f254,plain,
! [X0,X1,X2] :
( v1_relat_1(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_zfmisc_1(X1,X2))) ),
inference(cnf_transformation,[status(thm)],[f253]) ).
fof(f282,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)],[f31]) ).
fof(f284,plain,
! [X0] :
( v1_lattice3(X0)
| ~ v3_lattice3(X0)
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f282]) ).
fof(f285,plain,
! [X0] :
( v2_lattice3(X0)
| ~ v3_lattice3(X0)
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f282]) ).
fof(f311,plain,
! [A] :
( ~ v3_struct_0(A)
| ~ v2_lattice3(A)
| ~ l1_orders_2(A) ),
inference(pre_NNF_transformation,[status(thm)],[f36]) ).
fof(f312,plain,
! [X0] :
( ~ v3_struct_0(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f311]) ).
fof(f327,plain,
! [A] :
( ! [B] :
( ( v6_waybel_1(B,A)
& v1_partfun1(B,u1_struct_0(A),u1_struct_0(A))
& v1_funct_2(B,u1_struct_0(A),u1_struct_0(A))
& ~ v1_xboole_0(B)
& v1_funct_1(B) )
| ~ v7_waybel_1(B,A)
| ~ v1_funct_2(B,u1_struct_0(A),u1_struct_0(A))
| ~ v1_funct_1(B)
| ~ m1_relset_1(B,u1_struct_0(A),u1_struct_0(A)) )
| ~ l1_orders_2(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f41]) ).
fof(f332,plain,
! [X0,X1] :
( v6_waybel_1(X1,X0)
| ~ v7_waybel_1(X1,X0)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ l1_orders_2(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f327]) ).
fof(f380,plain,
! [A] :
( ! [B] :
( ! [C] :
( k2_waybel_1(A,B,C) = k8_relat_1(u1_struct_0(k2_yellow_2(A,B,C)),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) )
| ~ l1_orders_2(B)
| v3_struct_0(B) )
| ~ l1_orders_2(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f55]) ).
fof(f381,plain,
! [X0,X1,X2] :
( k2_waybel_1(X0,X1,X2) = k8_relat_1(u1_struct_0(k2_yellow_2(X0,X1,X2)),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)
| v3_struct_0(X1)
| ~ l1_orders_2(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f380]) ).
fof(f382,plain,
! [A] :
( ! [B] :
( ! [C] :
( k3_waybel_1(A,B,C) = k7_grcat_1(k2_yellow_2(A,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) )
| ~ l1_orders_2(B)
| v3_struct_0(B) )
| ~ l1_orders_2(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f56]) ).
fof(f383,plain,
! [X0,X1,X2] :
( k3_waybel_1(X0,X1,X2) = k7_grcat_1(k2_yellow_2(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)
| v3_struct_0(X1)
| ~ l1_orders_2(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f382]) ).
fof(f391,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)],[f61]) ).
fof(f393,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)],[f391]) ).
fof(f394,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)],[f391]) ).
fof(f395,plain,
! [A,B,C] :
( ( m2_relset_1(k2_waybel_1(A,B,C),u1_struct_0(A),u1_struct_0(k2_yellow_2(A,B,C)))
& v1_funct_2(k2_waybel_1(A,B,C),u1_struct_0(A),u1_struct_0(k2_yellow_2(A,B,C)))
& v1_funct_1(k2_waybel_1(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)
| v3_struct_0(B)
| ~ l1_orders_2(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f62]) ).
fof(f397,plain,
! [X0,X1,X2] :
( v1_funct_2(k2_waybel_1(X0,X1,X2),u1_struct_0(X0),u1_struct_0(k2_yellow_2(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)
| v3_struct_0(X1)
| ~ l1_orders_2(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f395]) ).
fof(f398,plain,
! [X0,X1,X2] :
( m2_relset_1(k2_waybel_1(X0,X1,X2),u1_struct_0(X0),u1_struct_0(k2_yellow_2(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)
| v3_struct_0(X1)
| ~ l1_orders_2(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f395]) ).
fof(f399,plain,
! [A,B,C] :
( ( m1_yellow_0(k2_yellow_2(A,B,C),B)
& v4_yellow_0(k2_yellow_2(A,B,C),B)
& v1_orders_2(k2_yellow_2(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)
| v3_struct_0(B)
| ~ l1_orders_2(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f63]) ).
fof(f402,plain,
! [X0,X1,X2] :
( m1_yellow_0(k2_yellow_2(X0,X1,X2),X1)
| ~ 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)
| v3_struct_0(X1)
| ~ l1_orders_2(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f399]) ).
fof(f416,plain,
! [A] :
( ! [B] :
( l1_orders_2(B)
| ~ m1_yellow_0(B,A) )
| ~ l1_orders_2(A) ),
inference(pre_NNF_transformation,[status(thm)],[f72]) ).
fof(f417,plain,
! [X0,X1] :
( l1_orders_2(X1)
| ~ m1_yellow_0(X1,X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f416]) ).
fof(f418,plain,
! [A,B,C] :
( m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B)))
| ~ m2_relset_1(C,A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f73]) ).
fof(f419,plain,
! [X0,X1,X2] :
( m1_subset_1(X0,k1_zfmisc_1(k2_zfmisc_1(X1,X2)))
| ~ m2_relset_1(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f418]) ).
fof(f435,plain,
! [A,B] :
( ( v3_waybel_0(k2_yellow_2(A,A,B),A)
& v7_yellow_0(k2_yellow_2(A,A,B),A)
& v5_yellow_0(k2_yellow_2(A,A,B),A)
& v4_yellow_0(k2_yellow_2(A,A,B),A)
& v4_orders_2(k2_yellow_2(A,A,B))
& v3_orders_2(k2_yellow_2(A,A,B))
& v2_orders_2(k2_yellow_2(A,A,B))
& v1_orders_2(k2_yellow_2(A,A,B))
& ~ v3_struct_0(k2_yellow_2(A,A,B)) )
| ~ m1_relset_1(B,u1_struct_0(A),u1_struct_0(A))
| ~ v7_waybel_1(B,A)
| ~ v1_funct_2(B,u1_struct_0(A),u1_struct_0(A))
| ~ v1_funct_1(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)],[f82]) ).
fof(f438,plain,
! [X0,X1] :
( v2_orders_2(k2_yellow_2(X0,X0,X1))
| ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v7_waybel_1(X1,X0)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(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)],[f435]) ).
fof(f445,plain,
! [A,B] :
( ( v3_lattice3(k2_yellow_2(A,A,B))
& v2_lattice3(k2_yellow_2(A,A,B))
& v1_lattice3(k2_yellow_2(A,A,B))
& v25_waybel_0(k2_yellow_2(A,A,B))
& v24_waybel_0(k2_yellow_2(A,A,B))
& v4_yellow_0(k2_yellow_2(A,A,B),A)
& v3_yellow_0(k2_yellow_2(A,A,B))
& v2_yellow_0(k2_yellow_2(A,A,B))
& v1_yellow_0(k2_yellow_2(A,A,B))
& v4_orders_2(k2_yellow_2(A,A,B))
& v3_orders_2(k2_yellow_2(A,A,B))
& v2_orders_2(k2_yellow_2(A,A,B))
& v1_orders_2(k2_yellow_2(A,A,B))
& ~ v3_struct_0(k2_yellow_2(A,A,B)) )
| ~ m1_relset_1(B,u1_struct_0(A),u1_struct_0(A))
| ~ v6_waybel_1(B,A)
| ~ v1_funct_2(B,u1_struct_0(A),u1_struct_0(A))
| ~ v1_funct_1(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)],[f83]) ).
fof(f449,plain,
! [X0,X1] :
( v3_orders_2(k2_yellow_2(X0,X0,X1))
| ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v6_waybel_1(X1,X0)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f445]) ).
fof(f450,plain,
! [X0,X1] :
( v4_orders_2(k2_yellow_2(X0,X0,X1))
| ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v6_waybel_1(X1,X0)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f445]) ).
fof(f459,plain,
! [X0,X1] :
( v3_lattice3(k2_yellow_2(X0,X0,X1))
| ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v6_waybel_1(X1,X0)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f445]) ).
fof(f500,plain,
! [A,B,C] :
( ( v5_orders_3(k2_waybel34(A,B,C),A,B)
& v4_waybel_1(k2_waybel34(A,B,C),A,B)
& v21_waybel_0(k2_waybel34(A,B,C),A,B)
& v19_waybel_0(k2_waybel34(A,B,C),A,B)
& v17_waybel_0(k2_waybel34(A,B,C),A,B)
& v1_partfun1(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_xboole_0(k2_waybel34(A,B,C))
& v1_funct_1(k2_waybel34(A,B,C))
& v1_relat_1(k2_waybel34(A,B,C)) )
| ~ m1_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)],[f90]) ).
fof(f506,plain,
! [X0,X1,X2] :
( v17_waybel_0(k2_waybel34(X0,X1,X2),X0,X1)
| ~ m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v18_waybel_0(X2,X1,X0)
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| ~ v3_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f500]) ).
fof(f511,plain,
! [A] :
( ( v23_waybel_0(k7_grcat_1(A),A,A)
& v1_funct_2(k7_grcat_1(A),u1_struct_0(A),u1_struct_0(A))
& v1_funct_1(k7_grcat_1(A))
& v1_relat_1(k7_grcat_1(A)) )
| ~ l1_orders_2(A) ),
inference(pre_NNF_transformation,[status(thm)],[f91]) ).
fof(f513,plain,
! [X0] :
( v1_funct_1(k7_grcat_1(X0))
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f511]) ).
fof(f516,plain,
! [A,B,C] :
( ( v4_yellow_0(k2_yellow_2(A,B,C),B)
& v1_orders_2(k2_yellow_2(A,B,C))
& ~ v3_struct_0(k2_yellow_2(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)
| v3_struct_0(B)
| ~ l1_orders_2(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f92]) ).
fof(f517,plain,
! [X0,X1,X2] :
( ~ v3_struct_0(k2_yellow_2(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)
| v3_struct_0(X1)
| ~ l1_orders_2(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f516]) ).
fof(f568,plain,
! [A,B] :
( ( v1_funct_1(k8_relat_1(A,B))
& v1_relat_1(k8_relat_1(A,B)) )
| ~ v1_funct_1(B)
| ~ v1_relat_1(B) ),
inference(pre_NNF_transformation,[status(thm)],[f98]) ).
fof(f569,plain,
! [B] :
( ( ! [A] : v1_funct_1(k8_relat_1(A,B))
& ! [A] : v1_relat_1(k8_relat_1(A,B)) )
| ~ v1_funct_1(B)
| ~ v1_relat_1(B) ),
inference(miniscoping,[status(thm)],[f568]) ).
fof(f571,plain,
! [X0,X1] :
( v1_funct_1(k8_relat_1(X1,X0))
| ~ v1_funct_1(X0)
| ~ v1_relat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f569]) ).
fof(f842,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)],[f134]) ).
fof(f843,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)],[f842]) ).
fof(f844,plain,
! [X0,X1,X2] :
( m1_relset_1(X0,X1,X2)
| ~ m2_relset_1(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f843]) ).
fof(f850,plain,
! [A] :
( ! [B] :
( ! [C] :
( v1_waybel34(k1_waybel34(A,B,C),B,A)
| ~ v22_waybel_0(C,A,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)],[f137]) ).
fof(f851,plain,
! [X0,X1,X2] :
( v1_waybel34(k1_waybel34(X0,X1,X2),X1,X0)
| ~ v22_waybel_0(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v17_waybel_0(X2,X0,X1)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| ~ v3_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f850]) ).
fof(f854,plain,
! [A] :
( ! [B] :
( ( k1_waybel34(k2_yellow_2(A,A,B),A,k3_waybel_1(A,A,B)) = k2_waybel_1(A,A,B)
& k2_waybel34(k2_yellow_2(A,A,B),A,k2_waybel_1(A,A,B)) = k3_waybel_1(A,A,B)
& v17_waybel_0(k3_waybel_1(A,A,B),k2_yellow_2(A,A,B),A)
& v18_waybel_0(k2_waybel_1(A,A,B),A,k2_yellow_2(A,A,B)) )
| ~ m2_relset_1(B,u1_struct_0(A),u1_struct_0(A))
| ~ v7_waybel_1(B,A)
| ~ v1_funct_2(B,u1_struct_0(A),u1_struct_0(A))
| ~ v1_funct_1(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)],[f139]) ).
fof(f855,plain,
! [X0,X1] :
( v18_waybel_0(k2_waybel_1(X0,X0,X1),X0,k2_yellow_2(X0,X0,X1))
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v7_waybel_1(X1,X0)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f854]) ).
fof(f857,plain,
! [X0,X1] :
( k2_waybel34(k2_yellow_2(X0,X0,X1),X0,k2_waybel_1(X0,X0,X1)) = k3_waybel_1(X0,X0,X1)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v7_waybel_1(X1,X0)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f854]) ).
fof(f858,plain,
! [X0,X1] :
( k1_waybel34(k2_yellow_2(X0,X0,X1),X0,k3_waybel_1(X0,X0,X1)) = k2_waybel_1(X0,X0,X1)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v7_waybel_1(X1,X0)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f854]) ).
fof(f863,plain,
! [A] :
( ! [B] :
( ( v4_waybel_0(k2_yellow_2(A,A,B),A)
<=> v22_waybel_0(k3_waybel_1(A,A,B),k2_yellow_2(A,A,B),A) )
| ~ m2_relset_1(B,u1_struct_0(A),u1_struct_0(A))
| ~ v7_waybel_1(B,A)
| ~ v1_funct_2(B,u1_struct_0(A),u1_struct_0(A))
| ~ v1_funct_1(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)],[f141]) ).
fof(f864,plain,
! [A] :
( ! [B] :
( ( ( ~ v22_waybel_0(k3_waybel_1(A,A,B),k2_yellow_2(A,A,B),A)
| v4_waybel_0(k2_yellow_2(A,A,B),A) )
& ( v22_waybel_0(k3_waybel_1(A,A,B),k2_yellow_2(A,A,B),A)
| ~ v4_waybel_0(k2_yellow_2(A,A,B),A) ) )
| ~ m2_relset_1(B,u1_struct_0(A),u1_struct_0(A))
| ~ v7_waybel_1(B,A)
| ~ v1_funct_2(B,u1_struct_0(A),u1_struct_0(A))
| ~ v1_funct_1(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(NNF_transformation,[status(thm)],[f863]) ).
fof(f865,plain,
! [X0,X1] :
( v22_waybel_0(k3_waybel_1(X0,X0,X1),k2_yellow_2(X0,X0,X1),X0)
| ~ v4_waybel_0(k2_yellow_2(X0,X0,X1),X0)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v7_waybel_1(X1,X0)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f864]) ).
fof(f881,plain,
m1_relset_1(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),
inference(resolution,[status(thm)],[f159,f844]) ).
fof(f904,definition,
( sQ4_spl
<=> v3_struct_0(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f905,plain,
( ~ sQ4_spl
| v3_struct_0(sK0_skl) ),
inference(component_clause,[status(thm)],[f904]) ).
fof(f907,definition,
( sQ5_spl
<=> l1_orders_2(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f909,plain,
( sQ5_spl
| ~ l1_orders_2(sK0_skl) ),
inference(component_clause,[status(thm)],[f907]) ).
fof(f910,definition,
( sQ6_spl
<=> m1_relset_1(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f912,plain,
( sQ6_spl
| ~ m1_relset_1(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)) ),
inference(component_clause,[status(thm)],[f910]) ).
fof(f913,definition,
( sQ7_spl
<=> v7_waybel_1(sK1_skl,sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f915,plain,
( sQ7_spl
| ~ v7_waybel_1(sK1_skl,sK0_skl) ),
inference(component_clause,[status(thm)],[f913]) ).
fof(f917,plain,
( sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f915,f158]) ).
fof(f918,plain,
sQ7_spl,
inference(contradiction_clause,[status(thm)],[f917]) ).
fof(f919,plain,
( sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f912,f881]) ).
fof(f920,plain,
sQ6_spl,
inference(contradiction_clause,[status(thm)],[f919]) ).
fof(f921,plain,
( sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f909,f155]) ).
fof(f922,plain,
sQ5_spl,
inference(contradiction_clause,[status(thm)],[f921]) ).
fof(f923,plain,
( ~ sQ4_spl
| ~ v2_lattice3(sK0_skl)
| ~ l1_orders_2(sK0_skl) ),
inference(resolution,[status(thm)],[f905,f312]) ).
fof(f925,definition,
( sQ8_spl
<=> v2_lattice3(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f927,plain,
( sQ8_spl
| ~ v2_lattice3(sK0_skl) ),
inference(component_clause,[status(thm)],[f925]) ).
fof(f928,plain,
( ~ sQ4_spl
| ~ sQ8_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f923,f907,f925,f904]) ).
fof(f929,definition,
( sQ9_spl
<=> v1_lattice3(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f931,plain,
( sQ9_spl
| ~ v1_lattice3(sK0_skl) ),
inference(component_clause,[status(thm)],[f929]) ).
fof(f933,plain,
( sQ8_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f927,f153]) ).
fof(f934,plain,
sQ8_spl,
inference(contradiction_clause,[status(thm)],[f933]) ).
fof(f936,plain,
! [X0,X1,X2] :
( m1_relset_1(k2_waybel_1(X0,X1,X2),u1_struct_0(X0),u1_struct_0(k2_yellow_2(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)
| v3_struct_0(X1)
| ~ l1_orders_2(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f398,f844]) ).
fof(f3534,plain,
( k2_waybel_1(sK0_skl,sK0_skl,sK1_skl) = k8_relat_1(u1_struct_0(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl)),sK1_skl)
| ~ m2_relset_1(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))
| ~ v1_funct_1(sK1_skl)
| ~ l1_orders_2(sK0_skl)
| v3_struct_0(sK0_skl)
| ~ l1_orders_2(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f381,f157]) ).
fof(f3543,definition,
( sQ309_spl
<=> v1_funct_1(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ309_spl])],[split_symbol_definition]) ).
fof(f3545,plain,
( sQ309_spl
| ~ v1_funct_1(sK1_skl) ),
inference(component_clause,[status(thm)],[f3543]) ).
fof(f3546,definition,
( sQ310_spl
<=> m2_relset_1(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ310_spl])],[split_symbol_definition]) ).
fof(f3548,plain,
( sQ310_spl
| ~ m2_relset_1(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)) ),
inference(component_clause,[status(thm)],[f3546]) ).
fof(f3549,definition,
( sQ311_spl
<=> k2_waybel_1(sK0_skl,sK0_skl,sK1_skl) = k8_relat_1(u1_struct_0(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl)),sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ311_spl])],[split_symbol_definition]) ).
fof(f3550,plain,
( ~ sQ311_spl
| k2_waybel_1(sK0_skl,sK0_skl,sK1_skl) = k8_relat_1(u1_struct_0(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl)),sK1_skl) ),
inference(component_clause,[status(thm)],[f3549]) ).
fof(f3552,plain,
( sQ311_spl
| ~ sQ310_spl
| ~ sQ309_spl
| ~ sQ5_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f3534,f904,f907,f3543,f3546,f3549]) ).
fof(f3565,plain,
( k3_waybel_1(sK0_skl,sK0_skl,sK1_skl) = k7_grcat_1(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl))
| ~ m2_relset_1(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))
| ~ v1_funct_1(sK1_skl)
| ~ l1_orders_2(sK0_skl)
| v3_struct_0(sK0_skl)
| ~ l1_orders_2(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f383,f157]) ).
fof(f3574,definition,
( sQ312_spl
<=> k3_waybel_1(sK0_skl,sK0_skl,sK1_skl) = k7_grcat_1(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ312_spl])],[split_symbol_definition]) ).
fof(f3575,plain,
( ~ sQ312_spl
| k3_waybel_1(sK0_skl,sK0_skl,sK1_skl) = k7_grcat_1(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl)) ),
inference(component_clause,[status(thm)],[f3574]) ).
fof(f3577,plain,
( sQ312_spl
| ~ sQ310_spl
| ~ sQ309_spl
| ~ sQ5_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f3565,f904,f907,f3543,f3546,f3574]) ).
fof(f3578,plain,
( sQ310_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3548,f159]) ).
fof(f3579,plain,
sQ310_spl,
inference(contradiction_clause,[status(thm)],[f3578]) ).
fof(f3580,plain,
( sQ309_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3545,f156]) ).
fof(f3581,plain,
sQ309_spl,
inference(contradiction_clause,[status(thm)],[f3580]) ).
fof(f3602,plain,
( ~ sQ312_spl
| v1_funct_1(k3_waybel_1(sK0_skl,sK0_skl,sK1_skl))
| ~ l1_orders_2(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl)) ),
inference(paramodulation,[status(thm)],[f3575,f513]) ).
fof(f3606,definition,
( sQ313_spl
<=> v3_struct_0(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ313_spl])],[split_symbol_definition]) ).
fof(f3607,plain,
( ~ sQ313_spl
| v3_struct_0(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl)) ),
inference(component_clause,[status(thm)],[f3606]) ).
fof(f3609,definition,
( sQ314_spl
<=> l1_orders_2(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ314_spl])],[split_symbol_definition]) ).
fof(f3611,plain,
( sQ314_spl
| ~ l1_orders_2(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl)) ),
inference(component_clause,[status(thm)],[f3609]) ).
fof(f3616,definition,
( sQ316_spl
<=> v2_orders_2(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ316_spl])],[split_symbol_definition]) ).
fof(f3618,plain,
( sQ316_spl
| ~ v2_orders_2(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl)) ),
inference(component_clause,[status(thm)],[f3616]) ).
fof(f3692,definition,
( sQ335_spl
<=> v1_funct_1(k3_waybel_1(sK0_skl,sK0_skl,sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ335_spl])],[split_symbol_definition]) ).
fof(f3695,plain,
( ~ sQ312_spl
| sQ335_spl
| ~ sQ314_spl ),
inference(split_clause,[status(thm)],[f3602,f3609,f3692,f3574]) ).
fof(f3702,plain,
! [X0] :
( sQ314_spl
| ~ m1_yellow_0(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl),X0)
| ~ l1_orders_2(X0) ),
inference(resolution,[status(thm)],[f3611,f417]) ).
fof(f3704,plain,
( ~ sQ311_spl
| v1_funct_1(k2_waybel_1(sK0_skl,sK0_skl,sK1_skl))
| ~ v1_funct_1(sK1_skl)
| ~ v1_relat_1(sK1_skl) ),
inference(paramodulation,[status(thm)],[f3550,f571]) ).
fof(f3706,definition,
( sQ337_spl
<=> v1_relat_1(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ337_spl])],[split_symbol_definition]) ).
fof(f3708,plain,
( sQ337_spl
| ~ v1_relat_1(sK1_skl) ),
inference(component_clause,[status(thm)],[f3706]) ).
fof(f3709,definition,
( sQ338_spl
<=> v1_funct_1(k2_waybel_1(sK0_skl,sK0_skl,sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ338_spl])],[split_symbol_definition]) ).
fof(f3712,plain,
( ~ sQ311_spl
| sQ338_spl
| ~ sQ309_spl
| ~ sQ337_spl ),
inference(split_clause,[status(thm)],[f3704,f3706,f3543,f3709,f3549]) ).
fof(f3717,plain,
! [X0,X1] :
( sQ337_spl
| ~ m1_subset_1(sK1_skl,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(resolution,[status(thm)],[f3708,f254]) ).
fof(f3718,plain,
! [X0,X1] :
( sQ337_spl
| ~ m2_relset_1(sK1_skl,X0,X1) ),
inference(resolution,[status(thm)],[f3717,f419]) ).
fof(f3721,plain,
( sQ337_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f159,f3718]) ).
fof(f3722,plain,
sQ337_spl,
inference(contradiction_clause,[status(thm)],[f3721]) ).
fof(f3960,plain,
( sQ314_spl
| ~ l1_orders_2(sK0_skl)
| ~ m1_relset_1(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))
| ~ v1_funct_2(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))
| ~ v1_funct_1(sK1_skl)
| ~ l1_orders_2(sK0_skl)
| v3_struct_0(sK0_skl)
| ~ l1_orders_2(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f402,f3702]) ).
fof(f3965,definition,
( sQ342_spl
<=> v1_funct_2(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ342_spl])],[split_symbol_definition]) ).
fof(f3967,plain,
( sQ342_spl
| ~ v1_funct_2(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)) ),
inference(component_clause,[status(thm)],[f3965]) ).
fof(f3968,plain,
( sQ314_spl
| ~ sQ6_spl
| ~ sQ342_spl
| ~ sQ309_spl
| ~ sQ5_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f3960,f904,f907,f3543,f3965,f910,f3609]) ).
fof(f3973,plain,
( sQ342_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3967,f157]) ).
fof(f3974,plain,
sQ342_spl,
inference(contradiction_clause,[status(thm)],[f3973]) ).
fof(f3977,plain,
( ~ sQ313_spl
| ~ m1_relset_1(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))
| ~ v1_funct_2(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))
| ~ v1_funct_1(sK1_skl)
| ~ l1_orders_2(sK0_skl)
| v3_struct_0(sK0_skl)
| ~ l1_orders_2(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f3607,f517]) ).
fof(f3981,definition,
( sQ343_spl
<=> v2_orders_2(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ343_spl])],[split_symbol_definition]) ).
fof(f3983,plain,
( sQ343_spl
| ~ v2_orders_2(sK0_skl) ),
inference(component_clause,[status(thm)],[f3981]) ).
fof(f3984,definition,
( sQ344_spl
<=> v3_orders_2(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ344_spl])],[split_symbol_definition]) ).
fof(f3986,plain,
( sQ344_spl
| ~ v3_orders_2(sK0_skl) ),
inference(component_clause,[status(thm)],[f3984]) ).
fof(f3987,definition,
( sQ345_spl
<=> v4_orders_2(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ345_spl])],[split_symbol_definition]) ).
fof(f3989,plain,
( sQ345_spl
| ~ v4_orders_2(sK0_skl) ),
inference(component_clause,[status(thm)],[f3987]) ).
fof(f3991,plain,
( ~ sQ313_spl
| ~ sQ6_spl
| ~ sQ342_spl
| ~ sQ309_spl
| ~ sQ5_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f3977,f904,f907,f3543,f3965,f910,f3606]) ).
fof(f3992,definition,
( sQ346_spl
<=> v2_lattice3(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ346_spl])],[split_symbol_definition]) ).
fof(f3994,plain,
( sQ346_spl
| ~ v2_lattice3(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl)) ),
inference(component_clause,[status(thm)],[f3992]) ).
fof(f3996,definition,
( sQ347_spl
<=> v1_lattice3(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ347_spl])],[split_symbol_definition]) ).
fof(f3998,plain,
( sQ347_spl
| ~ v1_lattice3(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl)) ),
inference(component_clause,[status(thm)],[f3996]) ).
fof(f4055,plain,
( sQ316_spl
| ~ m1_relset_1(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))
| ~ v7_waybel_1(sK1_skl,sK0_skl)
| ~ v1_funct_2(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))
| ~ v1_funct_1(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)],[f3618,f438]) ).
fof(f4057,plain,
( sQ316_spl
| ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ342_spl
| ~ sQ309_spl
| ~ sQ5_spl
| ~ sQ345_spl
| ~ sQ344_spl
| ~ sQ343_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f4055,f904,f3981,f3984,f3987,f907,f3543,f3965,f913,f910,f3616]) ).
fof(f4058,plain,
( sQ345_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3989,f151]) ).
fof(f4059,plain,
sQ345_spl,
inference(contradiction_clause,[status(thm)],[f4058]) ).
fof(f4060,plain,
( sQ343_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3983,f149]) ).
fof(f4061,plain,
sQ343_spl,
inference(contradiction_clause,[status(thm)],[f4060]) ).
fof(f4062,plain,
( sQ344_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3986,f150]) ).
fof(f4063,plain,
sQ344_spl,
inference(contradiction_clause,[status(thm)],[f4062]) ).
fof(f4920,plain,
( sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f931,f152]) ).
fof(f4921,plain,
sQ9_spl,
inference(contradiction_clause,[status(thm)],[f4920]) ).
fof(f14637,definition,
( sQ1717_spl
<=> v3_orders_2(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ1717_spl])],[split_symbol_definition]) ).
fof(f14639,plain,
( sQ1717_spl
| ~ v3_orders_2(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl)) ),
inference(component_clause,[status(thm)],[f14637]) ).
fof(f14640,definition,
( sQ1718_spl
<=> v4_orders_2(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ1718_spl])],[split_symbol_definition]) ).
fof(f14642,plain,
( sQ1718_spl
| ~ v4_orders_2(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl)) ),
inference(component_clause,[status(thm)],[f14640]) ).
fof(f14643,definition,
( sQ1719_spl
<=> v3_lattice3(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ1719_spl])],[split_symbol_definition]) ).
fof(f14645,plain,
( sQ1719_spl
| ~ v3_lattice3(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl)) ),
inference(component_clause,[status(thm)],[f14643]) ).
fof(f14659,definition,
( sQ1724_spl
<=> v3_lattice3(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ1724_spl])],[split_symbol_definition]) ).
fof(f14661,plain,
( sQ1724_spl
| ~ v3_lattice3(sK0_skl) ),
inference(component_clause,[status(thm)],[f14659]) ).
fof(f14703,plain,
( sQ1724_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f14661,f154]) ).
fof(f14704,plain,
sQ1724_spl,
inference(contradiction_clause,[status(thm)],[f14703]) ).
fof(f14733,plain,
( sQ1719_spl
| ~ m1_relset_1(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))
| ~ v6_waybel_1(sK1_skl,sK0_skl)
| ~ v1_funct_2(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))
| ~ v1_funct_1(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(resolution,[status(thm)],[f14645,f459]) ).
fof(f14736,definition,
( sQ1734_spl
<=> v6_waybel_1(sK1_skl,sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ1734_spl])],[split_symbol_definition]) ).
fof(f14738,plain,
( sQ1734_spl
| ~ v6_waybel_1(sK1_skl,sK0_skl) ),
inference(component_clause,[status(thm)],[f14736]) ).
fof(f14739,plain,
( sQ1719_spl
| ~ sQ6_spl
| ~ sQ1734_spl
| ~ sQ342_spl
| ~ sQ309_spl
| ~ sQ5_spl
| ~ sQ1724_spl
| ~ sQ8_spl
| ~ sQ9_spl
| ~ sQ345_spl
| ~ sQ344_spl
| ~ sQ343_spl ),
inference(split_clause,[status(thm)],[f14733,f3981,f3984,f3987,f929,f925,f14659,f907,f3543,f3965,f14736,f910,f14643]) ).
fof(f14755,plain,
( sQ1734_spl
| ~ v7_waybel_1(sK1_skl,sK0_skl)
| ~ v1_funct_2(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))
| ~ v1_funct_1(sK1_skl)
| ~ m1_relset_1(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))
| ~ l1_orders_2(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f14738,f332]) ).
fof(f14760,plain,
( sQ1734_spl
| ~ sQ7_spl
| ~ sQ342_spl
| ~ sQ309_spl
| ~ sQ6_spl
| ~ sQ5_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f14755,f904,f907,f910,f3543,f3965,f913,f14736]) ).
fof(f14764,plain,
( sQ1718_spl
| ~ m1_relset_1(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))
| ~ v6_waybel_1(sK1_skl,sK0_skl)
| ~ v1_funct_2(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))
| ~ v1_funct_1(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(resolution,[status(thm)],[f14642,f450]) ).
fof(f14771,plain,
( sQ1718_spl
| ~ sQ6_spl
| ~ sQ1734_spl
| ~ sQ342_spl
| ~ sQ309_spl
| ~ sQ5_spl
| ~ sQ1724_spl
| ~ sQ8_spl
| ~ sQ9_spl
| ~ sQ345_spl
| ~ sQ344_spl
| ~ sQ343_spl ),
inference(split_clause,[status(thm)],[f14764,f3981,f3984,f3987,f929,f925,f14659,f907,f3543,f3965,f14736,f910,f14640]) ).
fof(f14784,plain,
( sQ1717_spl
| ~ m1_relset_1(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))
| ~ v6_waybel_1(sK1_skl,sK0_skl)
| ~ v1_funct_2(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))
| ~ v1_funct_1(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(resolution,[status(thm)],[f14639,f449]) ).
fof(f14788,plain,
( sQ1717_spl
| ~ sQ6_spl
| ~ sQ1734_spl
| ~ sQ342_spl
| ~ sQ309_spl
| ~ sQ5_spl
| ~ sQ1724_spl
| ~ sQ8_spl
| ~ sQ9_spl
| ~ sQ345_spl
| ~ sQ344_spl
| ~ sQ343_spl ),
inference(split_clause,[status(thm)],[f14784,f3981,f3984,f3987,f929,f925,f14659,f907,f3543,f3965,f14736,f910,f14637]) ).
fof(f14867,plain,
( sQ347_spl
| ~ v3_lattice3(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl))
| v3_struct_0(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl))
| ~ l1_orders_2(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl)) ),
inference(resolution,[status(thm)],[f3998,f284]) ).
fof(f14870,plain,
( sQ347_spl
| ~ sQ1719_spl
| sQ313_spl
| ~ sQ314_spl ),
inference(split_clause,[status(thm)],[f14867,f3609,f3606,f14643,f3996]) ).
fof(f15322,plain,
( sQ346_spl
| ~ v3_lattice3(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl))
| v3_struct_0(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl))
| ~ l1_orders_2(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl)) ),
inference(resolution,[status(thm)],[f3994,f285]) ).
fof(f15331,plain,
( sQ346_spl
| ~ sQ1719_spl
| sQ313_spl
| ~ sQ314_spl ),
inference(split_clause,[status(thm)],[f15322,f3609,f3606,f14643,f3992]) ).
fof(f23746,plain,
( k2_waybel34(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl),sK0_skl,k2_waybel_1(sK0_skl,sK0_skl,sK1_skl)) = k3_waybel_1(sK0_skl,sK0_skl,sK1_skl)
| ~ m2_relset_1(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))
| ~ v1_funct_2(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))
| ~ v1_funct_1(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(resolution,[status(thm)],[f857,f158]) ).
fof(f23765,definition,
( sQ2532_spl
<=> k2_waybel34(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl),sK0_skl,k2_waybel_1(sK0_skl,sK0_skl,sK1_skl)) = k3_waybel_1(sK0_skl,sK0_skl,sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ2532_spl])],[split_symbol_definition]) ).
fof(f23766,plain,
( ~ sQ2532_spl
| k2_waybel34(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl),sK0_skl,k2_waybel_1(sK0_skl,sK0_skl,sK1_skl)) = k3_waybel_1(sK0_skl,sK0_skl,sK1_skl) ),
inference(component_clause,[status(thm)],[f23765]) ).
fof(f23768,plain,
( sQ2532_spl
| ~ sQ310_spl
| ~ sQ342_spl
| ~ sQ309_spl
| ~ sQ5_spl
| ~ sQ1724_spl
| ~ sQ8_spl
| ~ sQ9_spl
| ~ sQ345_spl
| ~ sQ344_spl
| ~ sQ343_spl ),
inference(split_clause,[status(thm)],[f23746,f3981,f3984,f3987,f929,f925,f14659,f907,f3543,f3965,f3546,f23765]) ).
fof(f23773,plain,
( k1_waybel34(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl),sK0_skl,k3_waybel_1(sK0_skl,sK0_skl,sK1_skl)) = k2_waybel_1(sK0_skl,sK0_skl,sK1_skl)
| ~ m2_relset_1(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))
| ~ v1_funct_2(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))
| ~ v1_funct_1(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(resolution,[status(thm)],[f858,f158]) ).
fof(f23784,definition,
( sQ2534_spl
<=> k1_waybel34(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl),sK0_skl,k3_waybel_1(sK0_skl,sK0_skl,sK1_skl)) = k2_waybel_1(sK0_skl,sK0_skl,sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ2534_spl])],[split_symbol_definition]) ).
fof(f23785,plain,
( ~ sQ2534_spl
| k1_waybel34(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl),sK0_skl,k3_waybel_1(sK0_skl,sK0_skl,sK1_skl)) = k2_waybel_1(sK0_skl,sK0_skl,sK1_skl) ),
inference(component_clause,[status(thm)],[f23784]) ).
fof(f23787,plain,
( sQ2534_spl
| ~ sQ310_spl
| ~ sQ342_spl
| ~ sQ309_spl
| ~ sQ5_spl
| ~ sQ1724_spl
| ~ sQ8_spl
| ~ sQ9_spl
| ~ sQ345_spl
| ~ sQ344_spl
| ~ sQ343_spl ),
inference(split_clause,[status(thm)],[f23773,f3981,f3984,f3987,f929,f925,f14659,f907,f3543,f3965,f3546,f23784]) ).
fof(f23797,plain,
( ~ sQ2532_spl
| v17_waybel_0(k3_waybel_1(sK0_skl,sK0_skl,sK1_skl),k2_yellow_2(sK0_skl,sK0_skl,sK1_skl),sK0_skl)
| ~ m1_relset_1(k2_waybel_1(sK0_skl,sK0_skl,sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl)))
| ~ v18_waybel_0(k2_waybel_1(sK0_skl,sK0_skl,sK1_skl),sK0_skl,k2_yellow_2(sK0_skl,sK0_skl,sK1_skl))
| ~ v1_funct_2(k2_waybel_1(sK0_skl,sK0_skl,sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl)))
| ~ v1_funct_1(k2_waybel_1(sK0_skl,sK0_skl,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)
| ~ l1_orders_2(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl))
| ~ v3_lattice3(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl))
| ~ v2_lattice3(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl))
| ~ v1_lattice3(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl))
| ~ v4_orders_2(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl))
| ~ v3_orders_2(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl))
| ~ v2_orders_2(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl)) ),
inference(paramodulation,[status(thm)],[f23766,f506]) ).
fof(f23802,plain,
( ~ sQ2532_spl
| m2_relset_1(k3_waybel_1(sK0_skl,sK0_skl,sK1_skl),u1_struct_0(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl)),u1_struct_0(sK0_skl))
| ~ m1_relset_1(k2_waybel_1(sK0_skl,sK0_skl,sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl)))
| ~ v1_funct_2(k2_waybel_1(sK0_skl,sK0_skl,sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl)))
| ~ v1_funct_1(k2_waybel_1(sK0_skl,sK0_skl,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)
| ~ l1_orders_2(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl))
| ~ v2_lattice3(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl))
| ~ v1_lattice3(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl))
| ~ v4_orders_2(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl))
| ~ v3_orders_2(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl))
| ~ v2_orders_2(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl)) ),
inference(paramodulation,[status(thm)],[f23766,f394]) ).
fof(f23803,plain,
( ~ sQ2532_spl
| v1_funct_2(k3_waybel_1(sK0_skl,sK0_skl,sK1_skl),u1_struct_0(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl)),u1_struct_0(sK0_skl))
| ~ m1_relset_1(k2_waybel_1(sK0_skl,sK0_skl,sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl)))
| ~ v1_funct_2(k2_waybel_1(sK0_skl,sK0_skl,sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl)))
| ~ v1_funct_1(k2_waybel_1(sK0_skl,sK0_skl,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)
| ~ l1_orders_2(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl))
| ~ v2_lattice3(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl))
| ~ v1_lattice3(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl))
| ~ v4_orders_2(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl))
| ~ v3_orders_2(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl))
| ~ v2_orders_2(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl)) ),
inference(paramodulation,[status(thm)],[f23766,f393]) ).
fof(f23805,definition,
( sQ2535_spl
<=> v1_funct_2(k2_waybel_1(sK0_skl,sK0_skl,sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl))) ),
introduced(definition,[new_symbols(definition,[sQ2535_spl])],[split_symbol_definition]) ).
fof(f23807,plain,
( sQ2535_spl
| ~ v1_funct_2(k2_waybel_1(sK0_skl,sK0_skl,sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl))) ),
inference(component_clause,[status(thm)],[f23805]) ).
fof(f23808,definition,
( sQ2536_spl
<=> v18_waybel_0(k2_waybel_1(sK0_skl,sK0_skl,sK1_skl),sK0_skl,k2_yellow_2(sK0_skl,sK0_skl,sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ2536_spl])],[split_symbol_definition]) ).
fof(f23810,plain,
( sQ2536_spl
| ~ v18_waybel_0(k2_waybel_1(sK0_skl,sK0_skl,sK1_skl),sK0_skl,k2_yellow_2(sK0_skl,sK0_skl,sK1_skl)) ),
inference(component_clause,[status(thm)],[f23808]) ).
fof(f23811,definition,
( sQ2537_spl
<=> m1_relset_1(k2_waybel_1(sK0_skl,sK0_skl,sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl))) ),
introduced(definition,[new_symbols(definition,[sQ2537_spl])],[split_symbol_definition]) ).
fof(f23813,plain,
( sQ2537_spl
| ~ m1_relset_1(k2_waybel_1(sK0_skl,sK0_skl,sK1_skl),u1_struct_0(sK0_skl),u1_struct_0(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl))) ),
inference(component_clause,[status(thm)],[f23811]) ).
fof(f23830,definition,
( sQ2542_spl
<=> v17_waybel_0(k3_waybel_1(sK0_skl,sK0_skl,sK1_skl),k2_yellow_2(sK0_skl,sK0_skl,sK1_skl),sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ2542_spl])],[split_symbol_definition]) ).
fof(f23833,plain,
( ~ sQ2532_spl
| sQ2542_spl
| ~ sQ2537_spl
| ~ sQ2536_spl
| ~ sQ2535_spl
| ~ sQ338_spl
| ~ sQ5_spl
| ~ sQ1724_spl
| ~ sQ8_spl
| ~ sQ9_spl
| ~ sQ345_spl
| ~ sQ344_spl
| ~ sQ343_spl
| ~ sQ314_spl
| ~ sQ1719_spl
| ~ sQ346_spl
| ~ sQ347_spl
| ~ sQ1718_spl
| ~ sQ1717_spl
| ~ sQ316_spl ),
inference(split_clause,[status(thm)],[f23797,f3616,f14637,f14640,f3996,f3992,f14643,f3609,f3981,f3984,f3987,f929,f925,f14659,f907,f3709,f23805,f23808,f23811,f23830,f23765]) ).
fof(f23844,definition,
( sQ2545_spl
<=> m2_relset_1(k3_waybel_1(sK0_skl,sK0_skl,sK1_skl),u1_struct_0(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl)),u1_struct_0(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ2545_spl])],[split_symbol_definition]) ).
fof(f23847,plain,
( ~ sQ2532_spl
| sQ2545_spl
| ~ sQ2537_spl
| ~ sQ2535_spl
| ~ sQ338_spl
| ~ sQ5_spl
| ~ sQ8_spl
| ~ sQ9_spl
| ~ sQ345_spl
| ~ sQ344_spl
| ~ sQ343_spl
| ~ sQ314_spl
| ~ sQ346_spl
| ~ sQ347_spl
| ~ sQ1718_spl
| ~ sQ1717_spl
| ~ sQ316_spl ),
inference(split_clause,[status(thm)],[f23802,f3616,f14637,f14640,f3996,f3992,f3609,f3981,f3984,f3987,f929,f925,f907,f3709,f23805,f23811,f23844,f23765]) ).
fof(f23848,definition,
( sQ2546_spl
<=> v1_funct_2(k3_waybel_1(sK0_skl,sK0_skl,sK1_skl),u1_struct_0(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl)),u1_struct_0(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ2546_spl])],[split_symbol_definition]) ).
fof(f23851,plain,
( ~ sQ2532_spl
| sQ2546_spl
| ~ sQ2537_spl
| ~ sQ2535_spl
| ~ sQ338_spl
| ~ sQ5_spl
| ~ sQ8_spl
| ~ sQ9_spl
| ~ sQ345_spl
| ~ sQ344_spl
| ~ sQ343_spl
| ~ sQ314_spl
| ~ sQ346_spl
| ~ sQ347_spl
| ~ sQ1718_spl
| ~ sQ1717_spl
| ~ sQ316_spl ),
inference(split_clause,[status(thm)],[f23803,f3616,f14637,f14640,f3996,f3992,f3609,f3981,f3984,f3987,f929,f925,f907,f3709,f23805,f23811,f23848,f23765]) ).
fof(f24043,plain,
( ~ sQ2534_spl
| v1_waybel34(k2_waybel_1(sK0_skl,sK0_skl,sK1_skl),sK0_skl,k2_yellow_2(sK0_skl,sK0_skl,sK1_skl))
| ~ v22_waybel_0(k3_waybel_1(sK0_skl,sK0_skl,sK1_skl),k2_yellow_2(sK0_skl,sK0_skl,sK1_skl),sK0_skl)
| ~ m2_relset_1(k3_waybel_1(sK0_skl,sK0_skl,sK1_skl),u1_struct_0(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl)),u1_struct_0(sK0_skl))
| ~ v17_waybel_0(k3_waybel_1(sK0_skl,sK0_skl,sK1_skl),k2_yellow_2(sK0_skl,sK0_skl,sK1_skl),sK0_skl)
| ~ v1_funct_2(k3_waybel_1(sK0_skl,sK0_skl,sK1_skl),u1_struct_0(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl)),u1_struct_0(sK0_skl))
| ~ v1_funct_1(k3_waybel_1(sK0_skl,sK0_skl,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)
| ~ l1_orders_2(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl))
| ~ v3_lattice3(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl))
| ~ v2_lattice3(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl))
| ~ v1_lattice3(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl))
| ~ v4_orders_2(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl))
| ~ v3_orders_2(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl))
| ~ v2_orders_2(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl)) ),
inference(paramodulation,[status(thm)],[f23785,f851]) ).
fof(f24066,definition,
( sQ2559_spl
<=> v22_waybel_0(k3_waybel_1(sK0_skl,sK0_skl,sK1_skl),k2_yellow_2(sK0_skl,sK0_skl,sK1_skl),sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ2559_spl])],[split_symbol_definition]) ).
fof(f24068,plain,
( sQ2559_spl
| ~ v22_waybel_0(k3_waybel_1(sK0_skl,sK0_skl,sK1_skl),k2_yellow_2(sK0_skl,sK0_skl,sK1_skl),sK0_skl) ),
inference(component_clause,[status(thm)],[f24066]) ).
fof(f24069,definition,
( sQ2560_spl
<=> v1_waybel34(k2_waybel_1(sK0_skl,sK0_skl,sK1_skl),sK0_skl,k2_yellow_2(sK0_skl,sK0_skl,sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ2560_spl])],[split_symbol_definition]) ).
fof(f24070,plain,
( ~ sQ2560_spl
| v1_waybel34(k2_waybel_1(sK0_skl,sK0_skl,sK1_skl),sK0_skl,k2_yellow_2(sK0_skl,sK0_skl,sK1_skl)) ),
inference(component_clause,[status(thm)],[f24069]) ).
fof(f24072,plain,
( ~ sQ2534_spl
| sQ2560_spl
| ~ sQ2559_spl
| ~ sQ2545_spl
| ~ sQ2542_spl
| ~ sQ2546_spl
| ~ sQ335_spl
| ~ sQ5_spl
| ~ sQ1724_spl
| ~ sQ8_spl
| ~ sQ9_spl
| ~ sQ345_spl
| ~ sQ344_spl
| ~ sQ343_spl
| ~ sQ314_spl
| ~ sQ1719_spl
| ~ sQ346_spl
| ~ sQ347_spl
| ~ sQ1718_spl
| ~ sQ1717_spl
| ~ sQ316_spl ),
inference(split_clause,[status(thm)],[f24043,f3616,f14637,f14640,f3996,f3992,f14643,f3609,f3981,f3984,f3987,f929,f925,f14659,f907,f3692,f23848,f23830,f23844,f24066,f24069,f23784]) ).
fof(f24073,plain,
( ~ sQ2560_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f24070,f161]) ).
fof(f24074,plain,
~ sQ2560_spl,
inference(contradiction_clause,[status(thm)],[f24073]) ).
fof(f25084,plain,
( sQ2537_spl
| ~ m1_relset_1(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))
| ~ v1_funct_2(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))
| ~ v1_funct_1(sK1_skl)
| ~ l1_orders_2(sK0_skl)
| v3_struct_0(sK0_skl)
| ~ l1_orders_2(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f23813,f936]) ).
fof(f25085,plain,
( sQ2537_spl
| ~ sQ6_spl
| ~ sQ342_spl
| ~ sQ309_spl
| ~ sQ5_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f25084,f904,f907,f3543,f3965,f910,f23811]) ).
fof(f25434,plain,
( sQ2535_spl
| ~ m1_relset_1(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))
| ~ v1_funct_2(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))
| ~ v1_funct_1(sK1_skl)
| ~ l1_orders_2(sK0_skl)
| v3_struct_0(sK0_skl)
| ~ l1_orders_2(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f23807,f397]) ).
fof(f25435,plain,
( sQ2535_spl
| ~ sQ6_spl
| ~ sQ342_spl
| ~ sQ309_spl
| ~ sQ5_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f25434,f904,f907,f3543,f3965,f910,f23805]) ).
fof(f25619,plain,
( sQ2536_spl
| ~ m2_relset_1(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))
| ~ v7_waybel_1(sK1_skl,sK0_skl)
| ~ v1_funct_2(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))
| ~ v1_funct_1(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(resolution,[status(thm)],[f23810,f855]) ).
fof(f25620,plain,
( sQ2536_spl
| ~ sQ310_spl
| ~ sQ7_spl
| ~ sQ342_spl
| ~ sQ309_spl
| ~ sQ5_spl
| ~ sQ1724_spl
| ~ sQ8_spl
| ~ sQ9_spl
| ~ sQ345_spl
| ~ sQ344_spl
| ~ sQ343_spl ),
inference(split_clause,[status(thm)],[f25619,f3981,f3984,f3987,f929,f925,f14659,f907,f3543,f3965,f913,f3546,f23808]) ).
fof(f27343,plain,
( sQ2559_spl
| ~ v4_waybel_0(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl),sK0_skl)
| ~ m2_relset_1(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))
| ~ v7_waybel_1(sK1_skl,sK0_skl)
| ~ v1_funct_2(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))
| ~ v1_funct_1(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(resolution,[status(thm)],[f24068,f865]) ).
fof(f27346,definition,
( sQ3101_spl
<=> v4_waybel_0(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl),sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ3101_spl])],[split_symbol_definition]) ).
fof(f27348,plain,
( sQ3101_spl
| ~ v4_waybel_0(k2_yellow_2(sK0_skl,sK0_skl,sK1_skl),sK0_skl) ),
inference(component_clause,[status(thm)],[f27346]) ).
fof(f27349,plain,
( sQ2559_spl
| ~ sQ3101_spl
| ~ sQ310_spl
| ~ sQ7_spl
| ~ sQ342_spl
| ~ sQ309_spl
| ~ sQ5_spl
| ~ sQ1724_spl
| ~ sQ8_spl
| ~ sQ9_spl
| ~ sQ345_spl
| ~ sQ344_spl
| ~ sQ343_spl ),
inference(split_clause,[status(thm)],[f27343,f3981,f3984,f3987,f929,f925,f14659,f907,f3543,f3965,f913,f3546,f27346,f24066]) ).
fof(f27358,plain,
( sQ3101_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f27348,f160]) ).
fof(f27359,plain,
sQ3101_spl,
inference(contradiction_clause,[status(thm)],[f27358]) ).
fof(f27360,plain,
$false,
inference(sat_refutation,[status(thm)],[f918,f920,f922,f928,f934,f3552,f3577,f3579,f3581,f3695,f3712,f3722,f3968,f3974,f3991,f4057,f4059,f4061,f4063,f4921,f14704,f14739,f14760,f14771,f14788,f14870,f15331,f23768,f23787,f23833,f23847,f23851,f24072,f24074,f25085,f25435,f25620,f27349,f27359]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : LAT369+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.43 % Computer : n008.cluster.edu
% 0.17/0.43 % Model : x86_64 x86_64
% 0.17/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.43 % Memory : 8046.5625MB
% 0.17/0.43 % OS : Linux 6.8.0-71-generic
% 0.17/0.43 % CPULimit : 300
% 0.17/0.43 % WCLimit : 300
% 0.17/0.43 % DateTime : Sun Sep 20 23:53:40 UTC 2026
% 0.17/0.43 % CPUTime :
% 0.17/0.47 % Drodi V4.1.1
% 132.29/17.57 % Refutation found
% 132.29/17.57 % SZS status Theorem for theBenchmark: Theorem is valid
% 132.29/17.57 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 8.47/17.99 % Elapsed time: 17.537400 seconds
% 8.47/17.99 % CPU time: 136.263844 seconds
% 8.47/17.99 % Total memory used: 526.735 MB
% 8.47/17.99 % Net memory used: 505.270 MB
%------------------------------------------------------------------------------