%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : LAT369+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n005.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 07:50:26 AM UTC 2026
% Result : Theorem 158.20s 31.79s
% Output : CNFRefutation 158.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 43
% Number of leaves : 14
% Syntax : Number of formulae : 228 ( 35 unt; 0 def)
% Number of atoms : 1429 ( 36 equ)
% Maximal formula atoms : 25 ( 6 avg)
% Number of connectives : 2189 ( 988 ~;1020 |; 148 &)
% ( 2 <=>; 31 =>; 0 <=; 0 <~>)
% Maximal formula depth : 21 ( 7 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 34 ( 32 usr; 1 prp; 0-3 aty)
% Number of functors : 10 ( 10 usr; 2 con; 0-3 aty)
% Number of variables : 90 ( 0 sgn 35 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(cc1_lattice3,axiom,
! [A] :
( l1_orders_2(A)
=> ( v1_lattice3(A)
=> ~ v3_struct_0(A) ) ),
file('theBenchmark.p',cc1_lattice3) ).
fof(cc3_waybel_1,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('theBenchmark.p',cc3_waybel_1) ).
fof(d16_waybel_1,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('theBenchmark.p',d16_waybel_1) ).
fof(d17_waybel_1,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('theBenchmark.p',d17_waybel_1) ).
fof(dt_k2_yellow_2,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('theBenchmark.p',dt_k2_yellow_2) ).
fof(dt_k3_waybel_1,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(k3_waybel_1(A,B,C),u1_struct_0(k2_yellow_2(A,B,C)),u1_struct_0(B))
& v1_funct_2(k3_waybel_1(A,B,C),u1_struct_0(k2_yellow_2(A,B,C)),u1_struct_0(B))
& v1_funct_1(k3_waybel_1(A,B,C)) ) ),
file('theBenchmark.p',dt_k3_waybel_1) ).
fof(dt_m1_yellow_0,axiom,
! [A] :
( l1_orders_2(A)
=> ! [B] :
( m1_yellow_0(B,A)
=> l1_orders_2(B) ) ),
file('theBenchmark.p',dt_m1_yellow_0) ).
fof(fc10_waybel10,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('theBenchmark.p',fc10_waybel10) ).
fof(fc10_waybel34,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('theBenchmark.p',fc10_waybel34) ).
fof(redefinition_m2_relset_1,axiom,
! [A,B,C] :
( m2_relset_1(C,A,B)
<=> m1_relset_1(C,A,B) ),
file('theBenchmark.p',redefinition_m2_relset_1) ).
fof(t24_waybel34,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('theBenchmark.p',t24_waybel34) ).
fof(t39_waybel34,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('theBenchmark.p',t39_waybel34) ).
fof(t40_waybel34,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('theBenchmark.p',t40_waybel34) ).
fof(t42_waybel34,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('theBenchmark.p',t42_waybel34) ).
fof(t42_waybel34_neg,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(assume_negation,[status(cth)],[t42_waybel34]) ).
cnf(c_232,plain,
( ~ v3_struct_0(A)
| ~ v1_lattice3(A)
| ~ l1_orders_2(A) ),
inference(clausify,[status(thm)],[cc1_lattice3]) ).
cnf(c_269,plain,
( v6_waybel_1(B,A)
| ~ 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(clausify,[status(thm)],[cc3_waybel_1]) ).
cnf(c_289,plain,
( k8_relat_1(u1_struct_0(k2_yellow_2(A,B,C)),C) = k2_waybel_1(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(clausify,[status(thm)],[d16_waybel_1]) ).
cnf(c_290,plain,
( 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(copy,[status(thm)],[c_289]) ).
cnf(c_291,plain,
( k7_grcat_1(k2_yellow_2(A,B,C)) = k3_waybel_1(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(clausify,[status(thm)],[d17_waybel_1]) ).
cnf(c_292,plain,
( 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(copy,[status(thm)],[c_291]) ).
cnf(c_304,plain,
( m1_yellow_0(k2_yellow_2(A,B,C),B)
| ~ 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(clausify,[status(thm)],[dt_k2_yellow_2]) ).
cnf(c_305,plain,
( v1_funct_1(k3_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(clausify,[status(thm)],[dt_k3_waybel_1]) ).
cnf(c_306,plain,
( v1_funct_2(k3_waybel_1(A,B,C),u1_struct_0(k2_yellow_2(A,B,C)),u1_struct_0(B))
| ~ 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(clausify,[status(thm)],[dt_k3_waybel_1]) ).
cnf(c_307,plain,
( m2_relset_1(k3_waybel_1(A,B,C),u1_struct_0(k2_yellow_2(A,B,C)),u1_struct_0(B))
| ~ 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(clausify,[status(thm)],[dt_k3_waybel_1]) ).
cnf(c_313,plain,
( l1_orders_2(B)
| ~ m1_yellow_0(B,A)
| ~ l1_orders_2(A) ),
inference(clausify,[status(thm)],[dt_m1_yellow_0]) ).
cnf(c_323,plain,
( v2_orders_2(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(clausify,[status(thm)],[fc10_waybel10]) ).
cnf(c_324,plain,
( v3_orders_2(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(clausify,[status(thm)],[fc10_waybel10]) ).
cnf(c_325,plain,
( v4_orders_2(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(clausify,[status(thm)],[fc10_waybel10]) ).
cnf(c_341,plain,
( v1_lattice3(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(clausify,[status(thm)],[fc10_waybel34]) ).
cnf(c_342,plain,
( v2_lattice3(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(clausify,[status(thm)],[fc10_waybel34]) ).
cnf(c_343,plain,
( v3_lattice3(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(clausify,[status(thm)],[fc10_waybel34]) ).
cnf(c_587,plain,
( m1_relset_1(A,B,C)
| ~ m2_relset_1(A,B,C) ),
inference(clausify,[status(thm)],[redefinition_m2_relset_1]) ).
cnf(c_589,plain,
( 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(clausify,[status(thm)],[t24_waybel34]) ).
cnf(c_591,plain,
( v17_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(clausify,[status(thm)],[t39_waybel34]) ).
cnf(c_593,plain,
( k1_waybel34(k2_yellow_2(A,A,B),A,k3_waybel_1(A,A,B)) = k2_waybel_1(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(clausify,[status(thm)],[t39_waybel34]) ).
cnf(c_594,plain,
( 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(clausify,[status(thm)],[t40_waybel34]) ).
fof(nnf_145,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(fof_nnf,[status(thm)],[t42_waybel34_neg]) ).
fof(sk_t42_waybel34_neg,plain,
( ~ v1_waybel34(k2_waybel_1(sK0,sK0,sK1),sK0,k2_yellow_2(sK0,sK0,sK1))
& v4_waybel_0(k2_yellow_2(sK0,sK0,sK1),sK0)
& m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
& v7_waybel_1(sK1,sK0)
& v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
& v1_funct_1(sK1)
& l1_orders_2(sK0)
& v3_lattice3(sK0)
& v2_lattice3(sK0)
& v1_lattice3(sK0)
& v4_orders_2(sK0)
& v3_orders_2(sK0)
& v2_orders_2(sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(A,sK0),skolemize(B,sK1)],[nnf_145]) ).
cnf(c_597,negated_conjecture,
v2_orders_2(sK0),
inference(split_conjunct,[status(thm)],[sk_t42_waybel34_neg]) ).
cnf(c_598,negated_conjecture,
v3_orders_2(sK0),
inference(split_conjunct,[status(thm)],[sk_t42_waybel34_neg]) ).
cnf(c_599,negated_conjecture,
v4_orders_2(sK0),
inference(split_conjunct,[status(thm)],[sk_t42_waybel34_neg]) ).
cnf(c_600,negated_conjecture,
v1_lattice3(sK0),
inference(split_conjunct,[status(thm)],[sk_t42_waybel34_neg]) ).
cnf(c_601,negated_conjecture,
v2_lattice3(sK0),
inference(split_conjunct,[status(thm)],[sk_t42_waybel34_neg]) ).
cnf(c_602,negated_conjecture,
v3_lattice3(sK0),
inference(split_conjunct,[status(thm)],[sk_t42_waybel34_neg]) ).
cnf(c_603,negated_conjecture,
l1_orders_2(sK0),
inference(split_conjunct,[status(thm)],[sk_t42_waybel34_neg]) ).
cnf(c_604,negated_conjecture,
v1_funct_1(sK1),
inference(split_conjunct,[status(thm)],[sk_t42_waybel34_neg]) ).
cnf(c_605,negated_conjecture,
v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0)),
inference(split_conjunct,[status(thm)],[sk_t42_waybel34_neg]) ).
cnf(c_606,negated_conjecture,
v7_waybel_1(sK1,sK0),
inference(split_conjunct,[status(thm)],[sk_t42_waybel34_neg]) ).
cnf(c_607,negated_conjecture,
m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0)),
inference(split_conjunct,[status(thm)],[sk_t42_waybel34_neg]) ).
cnf(c_608,negated_conjecture,
v4_waybel_0(k2_yellow_2(sK0,sK0,sK1),sK0),
inference(split_conjunct,[status(thm)],[sk_t42_waybel34_neg]) ).
cnf(c_609,negated_conjecture,
~ v1_waybel34(k2_waybel_1(sK0,sK0,sK1),sK0,k2_yellow_2(sK0,sK0,sK1)),
inference(split_conjunct,[status(thm)],[sk_t42_waybel34_neg]) ).
cnf(c_27583,negated_conjecture,
( ~ v3_struct_0(sK0)
| ~ l1_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_600,c_232]) ).
cnf(c_749,negated_conjecture,
~ v3_struct_0(sK0),
inference(resolve,[status(thm)],[c_603,c_27583]) ).
cnf(c_897,plain,
m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0)),
inference(resolve,[status(thm)],[c_607,c_587]) ).
cnf(c_27584,plain,
( v6_waybel_1(sK1,sK0)
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_269,c_897]) ).
cnf(c_27585,plain,
( v6_waybel_1(sK1,sK0)
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_749,c_27584]) ).
cnf(c_27586,negated_conjecture,
( v6_waybel_1(sK1,sK0)
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1) ),
inference(resolve,[status(thm)],[c_603,c_27585]) ).
cnf(c_27587,negated_conjecture,
( v6_waybel_1(sK1,sK0)
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_604,c_27586]) ).
cnf(c_27588,negated_conjecture,
( v6_waybel_1(sK1,sK0)
| ~ v7_waybel_1(sK1,sK0) ),
inference(resolve,[status(thm)],[c_605,c_27587]) ).
cnf(c_1030,negated_conjecture,
v6_waybel_1(sK1,sK0),
inference(resolve,[status(thm)],[c_606,c_27588]) ).
cnf(c_27589,negated_conjecture,
( k2_waybel_1(sK0,sK0,sK1) = k8_relat_1(u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),sK1)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| v3_struct_0(sK0)
| ~ l1_orders_2(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_290,c_607]) ).
cnf(c_27590,negated_conjecture,
( k2_waybel_1(sK0,sK0,sK1) = k8_relat_1(u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),sK1)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ l1_orders_2(sK0)
| v3_struct_0(sK0) ),
inference(copy,[status(thm)],[c_27589]) ).
cnf(c_27591,negated_conjecture,
( k2_waybel_1(sK0,sK0,sK1) = k8_relat_1(u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),sK1)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| v3_struct_0(sK0) ),
inference(copy,[status(thm)],[c_27590]) ).
cnf(c_27592,negated_conjecture,
( k2_waybel_1(sK0,sK0,sK1) = k8_relat_1(u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),sK1)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_749,c_27591]) ).
cnf(c_27593,negated_conjecture,
( k2_waybel_1(sK0,sK0,sK1) = k8_relat_1(u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),sK1)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1) ),
inference(resolve,[status(thm)],[c_603,c_27592]) ).
cnf(c_27594,negated_conjecture,
( k2_waybel_1(sK0,sK0,sK1) = k8_relat_1(u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),sK1)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_604,c_27593]) ).
cnf(c_1114,negated_conjecture,
k2_waybel_1(sK0,sK0,sK1) = k8_relat_1(u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),sK1),
inference(resolve,[status(thm)],[c_605,c_27594]) ).
cnf(c_1127,negated_conjecture,
~ v1_waybel34(k8_relat_1(u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),sK1),sK0,k2_yellow_2(sK0,sK0,sK1)),
inference(paramod,[status(thm)],[c_1114,c_609]) ).
cnf(c_27595,negated_conjecture,
( k3_waybel_1(sK0,sK0,sK1) = k7_grcat_1(k2_yellow_2(sK0,sK0,sK1))
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| v3_struct_0(sK0)
| ~ l1_orders_2(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_292,c_607]) ).
cnf(c_27596,negated_conjecture,
( k3_waybel_1(sK0,sK0,sK1) = k7_grcat_1(k2_yellow_2(sK0,sK0,sK1))
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ l1_orders_2(sK0)
| v3_struct_0(sK0) ),
inference(copy,[status(thm)],[c_27595]) ).
cnf(c_27597,negated_conjecture,
( k3_waybel_1(sK0,sK0,sK1) = k7_grcat_1(k2_yellow_2(sK0,sK0,sK1))
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| v3_struct_0(sK0) ),
inference(copy,[status(thm)],[c_27596]) ).
cnf(c_27598,negated_conjecture,
( k3_waybel_1(sK0,sK0,sK1) = k7_grcat_1(k2_yellow_2(sK0,sK0,sK1))
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_749,c_27597]) ).
cnf(c_27599,negated_conjecture,
( k3_waybel_1(sK0,sK0,sK1) = k7_grcat_1(k2_yellow_2(sK0,sK0,sK1))
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1) ),
inference(resolve,[status(thm)],[c_603,c_27598]) ).
cnf(c_27600,negated_conjecture,
( k3_waybel_1(sK0,sK0,sK1) = k7_grcat_1(k2_yellow_2(sK0,sK0,sK1))
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_604,c_27599]) ).
cnf(c_1129,negated_conjecture,
k3_waybel_1(sK0,sK0,sK1) = k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),
inference(resolve,[status(thm)],[c_605,c_27600]) ).
cnf(c_27601,plain,
( m1_yellow_0(k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| v3_struct_0(sK0)
| ~ l1_orders_2(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_304,c_897]) ).
cnf(c_27602,plain,
( m1_yellow_0(k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ l1_orders_2(sK0)
| v3_struct_0(sK0) ),
inference(copy,[status(thm)],[c_27601]) ).
cnf(c_27603,plain,
( m1_yellow_0(k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| v3_struct_0(sK0) ),
inference(copy,[status(thm)],[c_27602]) ).
cnf(c_27604,plain,
( m1_yellow_0(k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_749,c_27603]) ).
cnf(c_27605,negated_conjecture,
( m1_yellow_0(k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1) ),
inference(resolve,[status(thm)],[c_603,c_27604]) ).
cnf(c_27606,negated_conjecture,
( m1_yellow_0(k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_604,c_27605]) ).
cnf(c_1173,negated_conjecture,
m1_yellow_0(k2_yellow_2(sK0,sK0,sK1),sK0),
inference(resolve,[status(thm)],[c_605,c_27606]) ).
cnf(c_27607,plain,
( v1_funct_1(k3_waybel_1(sK0,sK0,sK1))
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| v3_struct_0(sK0)
| ~ l1_orders_2(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_305,c_897]) ).
cnf(c_27608,plain,
( v1_funct_1(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)))
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| v3_struct_0(sK0)
| ~ l1_orders_2(sK0)
| v3_struct_0(sK0) ),
inference(paramod,[status(thm)],[c_1129,c_27607]) ).
cnf(c_27609,plain,
( v1_funct_1(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)))
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ l1_orders_2(sK0)
| v3_struct_0(sK0) ),
inference(copy,[status(thm)],[c_27608]) ).
cnf(c_27610,plain,
( v1_funct_1(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)))
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| v3_struct_0(sK0) ),
inference(copy,[status(thm)],[c_27609]) ).
cnf(c_27611,plain,
( v1_funct_1(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)))
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_749,c_27610]) ).
cnf(c_27612,negated_conjecture,
( v1_funct_1(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)))
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1) ),
inference(resolve,[status(thm)],[c_603,c_27611]) ).
cnf(c_27613,negated_conjecture,
( v1_funct_1(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)))
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_604,c_27612]) ).
cnf(c_1185,negated_conjecture,
v1_funct_1(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1))),
inference(resolve,[status(thm)],[c_605,c_27613]) ).
cnf(c_27614,plain,
( v1_funct_2(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| v3_struct_0(sK0)
| ~ l1_orders_2(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_306,c_897]) ).
cnf(c_27615,plain,
( v1_funct_2(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| v3_struct_0(sK0)
| ~ l1_orders_2(sK0)
| v3_struct_0(sK0) ),
inference(paramod,[status(thm)],[c_1129,c_27614]) ).
cnf(c_27616,plain,
( v1_funct_2(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ l1_orders_2(sK0)
| v3_struct_0(sK0) ),
inference(copy,[status(thm)],[c_27615]) ).
cnf(c_27617,plain,
( v1_funct_2(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| v3_struct_0(sK0) ),
inference(copy,[status(thm)],[c_27616]) ).
cnf(c_27618,plain,
( v1_funct_2(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_749,c_27617]) ).
cnf(c_27619,negated_conjecture,
( v1_funct_2(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1) ),
inference(resolve,[status(thm)],[c_603,c_27618]) ).
cnf(c_27620,negated_conjecture,
( v1_funct_2(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_604,c_27619]) ).
cnf(c_1188,negated_conjecture,
v1_funct_2(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0)),
inference(resolve,[status(thm)],[c_605,c_27620]) ).
cnf(c_27621,plain,
( m2_relset_1(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| v3_struct_0(sK0)
| ~ l1_orders_2(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_307,c_897]) ).
cnf(c_27622,plain,
( m2_relset_1(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| v3_struct_0(sK0)
| ~ l1_orders_2(sK0)
| v3_struct_0(sK0) ),
inference(paramod,[status(thm)],[c_1129,c_27621]) ).
cnf(c_27623,plain,
( m2_relset_1(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ l1_orders_2(sK0)
| v3_struct_0(sK0) ),
inference(copy,[status(thm)],[c_27622]) ).
cnf(c_27624,plain,
( m2_relset_1(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| v3_struct_0(sK0) ),
inference(copy,[status(thm)],[c_27623]) ).
cnf(c_27625,plain,
( m2_relset_1(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_749,c_27624]) ).
cnf(c_27626,negated_conjecture,
( m2_relset_1(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1) ),
inference(resolve,[status(thm)],[c_603,c_27625]) ).
cnf(c_27627,negated_conjecture,
( m2_relset_1(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_604,c_27626]) ).
cnf(c_1191,negated_conjecture,
m2_relset_1(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0)),
inference(resolve,[status(thm)],[c_605,c_27627]) ).
cnf(c_27628,plain,
( v2_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_323,c_897]) ).
cnf(c_27629,plain,
( v2_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_749,c_27628]) ).
cnf(c_27630,negated_conjecture,
( v2_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_597,c_27629]) ).
cnf(c_27631,negated_conjecture,
( v2_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v4_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_598,c_27630]) ).
cnf(c_27632,negated_conjecture,
( v2_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_599,c_27631]) ).
cnf(c_27633,negated_conjecture,
( v2_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1) ),
inference(resolve,[status(thm)],[c_603,c_27632]) ).
cnf(c_27634,negated_conjecture,
( v2_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_604,c_27633]) ).
cnf(c_27635,negated_conjecture,
( v2_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ v7_waybel_1(sK1,sK0) ),
inference(resolve,[status(thm)],[c_605,c_27634]) ).
cnf(c_1326,negated_conjecture,
v2_orders_2(k2_yellow_2(sK0,sK0,sK1)),
inference(resolve,[status(thm)],[c_606,c_27635]) ).
cnf(c_27636,plain,
( v3_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_324,c_897]) ).
cnf(c_27637,plain,
( v3_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_749,c_27636]) ).
cnf(c_27638,negated_conjecture,
( v3_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_597,c_27637]) ).
cnf(c_27639,negated_conjecture,
( v3_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v4_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_598,c_27638]) ).
cnf(c_27640,negated_conjecture,
( v3_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_599,c_27639]) ).
cnf(c_27641,negated_conjecture,
( v3_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1) ),
inference(resolve,[status(thm)],[c_603,c_27640]) ).
cnf(c_27642,negated_conjecture,
( v3_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_604,c_27641]) ).
cnf(c_27643,negated_conjecture,
( v3_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ v7_waybel_1(sK1,sK0) ),
inference(resolve,[status(thm)],[c_605,c_27642]) ).
cnf(c_1329,negated_conjecture,
v3_orders_2(k2_yellow_2(sK0,sK0,sK1)),
inference(resolve,[status(thm)],[c_606,c_27643]) ).
cnf(c_27644,plain,
( v4_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_325,c_897]) ).
cnf(c_27645,plain,
( v4_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_749,c_27644]) ).
cnf(c_27646,negated_conjecture,
( v4_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_597,c_27645]) ).
cnf(c_27647,negated_conjecture,
( v4_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v4_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_598,c_27646]) ).
cnf(c_27648,negated_conjecture,
( v4_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_599,c_27647]) ).
cnf(c_27649,negated_conjecture,
( v4_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1) ),
inference(resolve,[status(thm)],[c_603,c_27648]) ).
cnf(c_27650,negated_conjecture,
( v4_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_604,c_27649]) ).
cnf(c_27651,negated_conjecture,
( v4_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ v7_waybel_1(sK1,sK0) ),
inference(resolve,[status(thm)],[c_605,c_27650]) ).
cnf(c_1349,negated_conjecture,
v4_orders_2(k2_yellow_2(sK0,sK0,sK1)),
inference(resolve,[status(thm)],[c_606,c_27651]) ).
cnf(c_27652,plain,
( v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v6_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_341,c_897]) ).
cnf(c_27653,negated_conjecture,
( v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v6_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_597,c_27652]) ).
cnf(c_27654,negated_conjecture,
( v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v6_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_598,c_27653]) ).
cnf(c_27655,negated_conjecture,
( v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v6_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0) ),
inference(resolve,[status(thm)],[c_599,c_27654]) ).
cnf(c_27656,negated_conjecture,
( v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v6_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| ~ v2_lattice3(sK0) ),
inference(resolve,[status(thm)],[c_600,c_27655]) ).
cnf(c_27657,negated_conjecture,
( v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v6_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v3_lattice3(sK0) ),
inference(resolve,[status(thm)],[c_601,c_27656]) ).
cnf(c_27658,negated_conjecture,
( v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v6_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_602,c_27657]) ).
cnf(c_27659,negated_conjecture,
( v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v6_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1) ),
inference(resolve,[status(thm)],[c_603,c_27658]) ).
cnf(c_27660,negated_conjecture,
( v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v6_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_604,c_27659]) ).
cnf(c_27661,negated_conjecture,
( v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v6_waybel_1(sK1,sK0) ),
inference(resolve,[status(thm)],[c_605,c_27660]) ).
cnf(c_1439,negated_conjecture,
v1_lattice3(k2_yellow_2(sK0,sK0,sK1)),
inference(resolve,[status(thm)],[c_1030,c_27661]) ).
cnf(c_27662,plain,
( v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v6_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_342,c_897]) ).
cnf(c_27663,negated_conjecture,
( v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v6_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_597,c_27662]) ).
cnf(c_27664,negated_conjecture,
( v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v6_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_598,c_27663]) ).
cnf(c_27665,negated_conjecture,
( v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v6_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0) ),
inference(resolve,[status(thm)],[c_599,c_27664]) ).
cnf(c_27666,negated_conjecture,
( v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v6_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| ~ v2_lattice3(sK0) ),
inference(resolve,[status(thm)],[c_600,c_27665]) ).
cnf(c_27667,negated_conjecture,
( v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v6_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v3_lattice3(sK0) ),
inference(resolve,[status(thm)],[c_601,c_27666]) ).
cnf(c_27668,negated_conjecture,
( v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v6_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_602,c_27667]) ).
cnf(c_27669,negated_conjecture,
( v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v6_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1) ),
inference(resolve,[status(thm)],[c_603,c_27668]) ).
cnf(c_27670,negated_conjecture,
( v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v6_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_604,c_27669]) ).
cnf(c_27671,negated_conjecture,
( v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v6_waybel_1(sK1,sK0) ),
inference(resolve,[status(thm)],[c_605,c_27670]) ).
cnf(c_1442,negated_conjecture,
v2_lattice3(k2_yellow_2(sK0,sK0,sK1)),
inference(resolve,[status(thm)],[c_1030,c_27671]) ).
cnf(c_27672,plain,
( v3_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v6_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_343,c_897]) ).
cnf(c_27673,negated_conjecture,
( v3_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v6_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_597,c_27672]) ).
cnf(c_27674,negated_conjecture,
( v3_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v6_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_598,c_27673]) ).
cnf(c_27675,negated_conjecture,
( v3_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v6_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0) ),
inference(resolve,[status(thm)],[c_599,c_27674]) ).
cnf(c_27676,negated_conjecture,
( v3_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v6_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| ~ v2_lattice3(sK0) ),
inference(resolve,[status(thm)],[c_600,c_27675]) ).
cnf(c_27677,negated_conjecture,
( v3_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v6_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v3_lattice3(sK0) ),
inference(resolve,[status(thm)],[c_601,c_27676]) ).
cnf(c_27678,negated_conjecture,
( v3_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v6_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_602,c_27677]) ).
cnf(c_27679,negated_conjecture,
( v3_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v6_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1) ),
inference(resolve,[status(thm)],[c_603,c_27678]) ).
cnf(c_27680,negated_conjecture,
( v3_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v6_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_604,c_27679]) ).
cnf(c_27681,negated_conjecture,
( v3_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v6_waybel_1(sK1,sK0) ),
inference(resolve,[status(thm)],[c_605,c_27680]) ).
cnf(c_1445,negated_conjecture,
v3_lattice3(k2_yellow_2(sK0,sK0,sK1)),
inference(resolve,[status(thm)],[c_1030,c_27681]) ).
cnf(c_27682,plain,
( l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ l1_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_1173,c_313]) ).
cnf(c_1453,negated_conjecture,
l1_orders_2(k2_yellow_2(sK0,sK0,sK1)),
inference(resolve,[status(thm)],[c_603,c_27682]) ).
cnf(c_27683,negated_conjecture,
( v17_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_591,c_607]) ).
cnf(c_27684,negated_conjecture,
( v17_waybel_0(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0) ),
inference(paramod,[status(thm)],[c_1129,c_27683]) ).
cnf(c_27685,negated_conjecture,
( v17_waybel_0(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_597,c_27684]) ).
cnf(c_27686,negated_conjecture,
( v17_waybel_0(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_598,c_27685]) ).
cnf(c_27687,negated_conjecture,
( v17_waybel_0(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0) ),
inference(resolve,[status(thm)],[c_599,c_27686]) ).
cnf(c_27688,negated_conjecture,
( v17_waybel_0(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| ~ v2_lattice3(sK0) ),
inference(resolve,[status(thm)],[c_600,c_27687]) ).
cnf(c_27689,negated_conjecture,
( v17_waybel_0(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v3_lattice3(sK0) ),
inference(resolve,[status(thm)],[c_601,c_27688]) ).
cnf(c_27690,negated_conjecture,
( v17_waybel_0(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_602,c_27689]) ).
cnf(c_27691,negated_conjecture,
( v17_waybel_0(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1) ),
inference(resolve,[status(thm)],[c_603,c_27690]) ).
cnf(c_27692,negated_conjecture,
( v17_waybel_0(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_604,c_27691]) ).
cnf(c_27693,negated_conjecture,
( v17_waybel_0(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ v7_waybel_1(sK1,sK0) ),
inference(resolve,[status(thm)],[c_605,c_27692]) ).
cnf(c_4856,negated_conjecture,
v17_waybel_0(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),k2_yellow_2(sK0,sK0,sK1),sK0),
inference(resolve,[status(thm)],[c_606,c_27693]) ).
cnf(c_27694,negated_conjecture,
( k1_waybel34(k2_yellow_2(sK0,sK0,sK1),sK0,k3_waybel_1(sK0,sK0,sK1)) = k2_waybel_1(sK0,sK0,sK1)
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_593,c_607]) ).
cnf(c_27695,negated_conjecture,
( k1_waybel34(k2_yellow_2(sK0,sK0,sK1),sK0,k7_grcat_1(k2_yellow_2(sK0,sK0,sK1))) = k2_waybel_1(sK0,sK0,sK1)
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0) ),
inference(paramod,[status(thm)],[c_1129,c_27694]) ).
cnf(c_27696,negated_conjecture,
( k1_waybel34(k2_yellow_2(sK0,sK0,sK1),sK0,k7_grcat_1(k2_yellow_2(sK0,sK0,sK1))) = k8_relat_1(u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),sK1)
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0) ),
inference(paramod,[status(thm)],[c_1114,c_27695]) ).
cnf(c_27697,negated_conjecture,
( k1_waybel34(k2_yellow_2(sK0,sK0,sK1),sK0,k7_grcat_1(k2_yellow_2(sK0,sK0,sK1))) = k8_relat_1(u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),sK1)
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_597,c_27696]) ).
cnf(c_27698,negated_conjecture,
( k1_waybel34(k2_yellow_2(sK0,sK0,sK1),sK0,k7_grcat_1(k2_yellow_2(sK0,sK0,sK1))) = k8_relat_1(u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),sK1)
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_598,c_27697]) ).
cnf(c_27699,negated_conjecture,
( k1_waybel34(k2_yellow_2(sK0,sK0,sK1),sK0,k7_grcat_1(k2_yellow_2(sK0,sK0,sK1))) = k8_relat_1(u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),sK1)
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0) ),
inference(resolve,[status(thm)],[c_599,c_27698]) ).
cnf(c_27700,negated_conjecture,
( k1_waybel34(k2_yellow_2(sK0,sK0,sK1),sK0,k7_grcat_1(k2_yellow_2(sK0,sK0,sK1))) = k8_relat_1(u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),sK1)
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| ~ v2_lattice3(sK0) ),
inference(resolve,[status(thm)],[c_600,c_27699]) ).
cnf(c_27701,negated_conjecture,
( k1_waybel34(k2_yellow_2(sK0,sK0,sK1),sK0,k7_grcat_1(k2_yellow_2(sK0,sK0,sK1))) = k8_relat_1(u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),sK1)
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v3_lattice3(sK0) ),
inference(resolve,[status(thm)],[c_601,c_27700]) ).
cnf(c_27702,negated_conjecture,
( k1_waybel34(k2_yellow_2(sK0,sK0,sK1),sK0,k7_grcat_1(k2_yellow_2(sK0,sK0,sK1))) = k8_relat_1(u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),sK1)
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_602,c_27701]) ).
cnf(c_27703,negated_conjecture,
( k1_waybel34(k2_yellow_2(sK0,sK0,sK1),sK0,k7_grcat_1(k2_yellow_2(sK0,sK0,sK1))) = k8_relat_1(u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),sK1)
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1) ),
inference(resolve,[status(thm)],[c_603,c_27702]) ).
cnf(c_27704,negated_conjecture,
( k1_waybel34(k2_yellow_2(sK0,sK0,sK1),sK0,k7_grcat_1(k2_yellow_2(sK0,sK0,sK1))) = k8_relat_1(u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),sK1)
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_604,c_27703]) ).
cnf(c_27705,negated_conjecture,
( k1_waybel34(k2_yellow_2(sK0,sK0,sK1),sK0,k7_grcat_1(k2_yellow_2(sK0,sK0,sK1))) = k8_relat_1(u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),sK1)
| ~ v7_waybel_1(sK1,sK0) ),
inference(resolve,[status(thm)],[c_605,c_27704]) ).
cnf(c_4894,negated_conjecture,
k1_waybel34(k2_yellow_2(sK0,sK0,sK1),sK0,k7_grcat_1(k2_yellow_2(sK0,sK0,sK1))) = k8_relat_1(u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),sK1),
inference(resolve,[status(thm)],[c_606,c_27705]) ).
cnf(c_27706,negated_conjecture,
( v22_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ v4_waybel_0(k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_594,c_607]) ).
cnf(c_27707,negated_conjecture,
( v22_waybel_0(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ v4_waybel_0(k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0) ),
inference(paramod,[status(thm)],[c_1129,c_27706]) ).
cnf(c_27708,negated_conjecture,
( v22_waybel_0(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ v4_waybel_0(k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_597,c_27707]) ).
cnf(c_27709,negated_conjecture,
( v22_waybel_0(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ v4_waybel_0(k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_598,c_27708]) ).
cnf(c_27710,negated_conjecture,
( v22_waybel_0(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ v4_waybel_0(k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0) ),
inference(resolve,[status(thm)],[c_599,c_27709]) ).
cnf(c_27711,negated_conjecture,
( v22_waybel_0(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ v4_waybel_0(k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| ~ v2_lattice3(sK0) ),
inference(resolve,[status(thm)],[c_600,c_27710]) ).
cnf(c_27712,negated_conjecture,
( v22_waybel_0(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ v4_waybel_0(k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v3_lattice3(sK0) ),
inference(resolve,[status(thm)],[c_601,c_27711]) ).
cnf(c_27713,negated_conjecture,
( v22_waybel_0(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ v4_waybel_0(k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_602,c_27712]) ).
cnf(c_27714,negated_conjecture,
( v22_waybel_0(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ v4_waybel_0(k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1) ),
inference(resolve,[status(thm)],[c_603,c_27713]) ).
cnf(c_27715,negated_conjecture,
( v22_waybel_0(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ v4_waybel_0(k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_604,c_27714]) ).
cnf(c_27716,negated_conjecture,
( v22_waybel_0(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ v4_waybel_0(k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ v7_waybel_1(sK1,sK0) ),
inference(resolve,[status(thm)],[c_605,c_27715]) ).
cnf(c_27717,negated_conjecture,
( v22_waybel_0(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ v4_waybel_0(k2_yellow_2(sK0,sK0,sK1),sK0) ),
inference(resolve,[status(thm)],[c_606,c_27716]) ).
cnf(c_4903,negated_conjecture,
v22_waybel_0(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),k2_yellow_2(sK0,sK0,sK1),sK0),
inference(resolve,[status(thm)],[c_608,c_27717]) ).
cnf(c_27718,plain,
( v1_waybel34(k1_waybel34(k2_yellow_2(sK0,sK0,sK1),sK0,k7_grcat_1(k2_yellow_2(sK0,sK0,sK1))),sK0,k2_yellow_2(sK0,sK0,sK1))
| ~ v22_waybel_0(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ m2_relset_1(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_1(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)))
| ~ l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| ~ l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ v3_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v4_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ v3_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ v2_orders_2(k2_yellow_2(sK0,sK0,sK1)) ),
inference(resolve,[status(thm)],[c_4856,c_589]) ).
cnf(c_27719,plain,
( v1_waybel34(k8_relat_1(u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),sK1),sK0,k2_yellow_2(sK0,sK0,sK1))
| ~ v22_waybel_0(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ m2_relset_1(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_1(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)))
| ~ l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| ~ l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ v3_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v4_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ v3_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ v2_orders_2(k2_yellow_2(sK0,sK0,sK1)) ),
inference(paramod,[status(thm)],[c_4894,c_27718]) ).
cnf(c_27720,plain,
( v1_waybel34(k8_relat_1(u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),sK1),sK0,k2_yellow_2(sK0,sK0,sK1))
| ~ v22_waybel_0(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ m2_relset_1(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_1(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)))
| ~ l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| ~ l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ v3_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v4_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ v3_orders_2(k2_yellow_2(sK0,sK0,sK1)) ),
inference(resolve,[status(thm)],[c_1326,c_27719]) ).
cnf(c_27721,plain,
( v1_waybel34(k8_relat_1(u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),sK1),sK0,k2_yellow_2(sK0,sK0,sK1))
| ~ v22_waybel_0(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ m2_relset_1(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_1(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)))
| ~ l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| ~ l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ v3_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v4_orders_2(k2_yellow_2(sK0,sK0,sK1)) ),
inference(resolve,[status(thm)],[c_1329,c_27720]) ).
cnf(c_27722,plain,
( v1_waybel34(k8_relat_1(u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),sK1),sK0,k2_yellow_2(sK0,sK0,sK1))
| ~ v22_waybel_0(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ m2_relset_1(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_1(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)))
| ~ l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| ~ l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ v3_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v1_lattice3(k2_yellow_2(sK0,sK0,sK1)) ),
inference(resolve,[status(thm)],[c_1349,c_27721]) ).
cnf(c_27723,plain,
( v1_waybel34(k8_relat_1(u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),sK1),sK0,k2_yellow_2(sK0,sK0,sK1))
| ~ v22_waybel_0(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ m2_relset_1(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_1(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)))
| ~ l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| ~ l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ v3_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v2_lattice3(k2_yellow_2(sK0,sK0,sK1)) ),
inference(resolve,[status(thm)],[c_1439,c_27722]) ).
cnf(c_27724,plain,
( v1_waybel34(k8_relat_1(u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),sK1),sK0,k2_yellow_2(sK0,sK0,sK1))
| ~ v22_waybel_0(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ m2_relset_1(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_1(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)))
| ~ l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| ~ l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ v3_lattice3(k2_yellow_2(sK0,sK0,sK1)) ),
inference(resolve,[status(thm)],[c_1442,c_27723]) ).
cnf(c_27725,plain,
( v1_waybel34(k8_relat_1(u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),sK1),sK0,k2_yellow_2(sK0,sK0,sK1))
| ~ v22_waybel_0(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ m2_relset_1(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_1(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)))
| ~ l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| ~ l1_orders_2(k2_yellow_2(sK0,sK0,sK1)) ),
inference(resolve,[status(thm)],[c_1445,c_27724]) ).
cnf(c_27726,plain,
( v1_waybel34(k8_relat_1(u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),sK1),sK0,k2_yellow_2(sK0,sK0,sK1))
| ~ v22_waybel_0(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ m2_relset_1(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_1(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)))
| ~ l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_1453,c_27725]) ).
cnf(c_27727,negated_conjecture,
( v1_waybel34(k8_relat_1(u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),sK1),sK0,k2_yellow_2(sK0,sK0,sK1))
| ~ v22_waybel_0(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ m2_relset_1(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_1(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)))
| ~ l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_597,c_27726]) ).
cnf(c_27728,negated_conjecture,
( v1_waybel34(k8_relat_1(u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),sK1),sK0,k2_yellow_2(sK0,sK0,sK1))
| ~ v22_waybel_0(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ m2_relset_1(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_1(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)))
| ~ l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_598,c_27727]) ).
cnf(c_27729,negated_conjecture,
( v1_waybel34(k8_relat_1(u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),sK1),sK0,k2_yellow_2(sK0,sK0,sK1))
| ~ v22_waybel_0(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ m2_relset_1(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_1(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)))
| ~ l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0) ),
inference(resolve,[status(thm)],[c_599,c_27728]) ).
cnf(c_27730,negated_conjecture,
( v1_waybel34(k8_relat_1(u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),sK1),sK0,k2_yellow_2(sK0,sK0,sK1))
| ~ v22_waybel_0(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ m2_relset_1(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_1(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)))
| ~ l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| ~ v2_lattice3(sK0) ),
inference(resolve,[status(thm)],[c_600,c_27729]) ).
cnf(c_27731,negated_conjecture,
( v1_waybel34(k8_relat_1(u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),sK1),sK0,k2_yellow_2(sK0,sK0,sK1))
| ~ v22_waybel_0(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ m2_relset_1(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_1(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)))
| ~ l1_orders_2(sK0)
| ~ v3_lattice3(sK0) ),
inference(resolve,[status(thm)],[c_601,c_27730]) ).
cnf(c_27732,negated_conjecture,
( v1_waybel34(k8_relat_1(u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),sK1),sK0,k2_yellow_2(sK0,sK0,sK1))
| ~ v22_waybel_0(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ m2_relset_1(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_1(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)))
| ~ l1_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_602,c_27731]) ).
cnf(c_27733,negated_conjecture,
( v1_waybel34(k8_relat_1(u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),sK1),sK0,k2_yellow_2(sK0,sK0,sK1))
| ~ v22_waybel_0(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ m2_relset_1(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_1(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1))) ),
inference(resolve,[status(thm)],[c_603,c_27732]) ).
cnf(c_27734,negated_conjecture,
( v1_waybel34(k8_relat_1(u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),sK1),sK0,k2_yellow_2(sK0,sK0,sK1))
| ~ v22_waybel_0(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ m2_relset_1(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_1185,c_27733]) ).
cnf(c_27735,negated_conjecture,
( v1_waybel34(k8_relat_1(u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),sK1),sK0,k2_yellow_2(sK0,sK0,sK1))
| ~ v22_waybel_0(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ m2_relset_1(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_1188,c_27734]) ).
cnf(c_27736,negated_conjecture,
( v1_waybel34(k8_relat_1(u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),sK1),sK0,k2_yellow_2(sK0,sK0,sK1))
| ~ v22_waybel_0(k7_grcat_1(k2_yellow_2(sK0,sK0,sK1)),k2_yellow_2(sK0,sK0,sK1),sK0) ),
inference(resolve,[status(thm)],[c_1191,c_27735]) ).
cnf(c_27737,negated_conjecture,
v1_waybel34(k8_relat_1(u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),sK1),sK0,k2_yellow_2(sK0,sK0,sK1)),
inference(resolve,[status(thm)],[c_4903,c_27736]) ).
cnf(c_27582,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_1127,c_27737]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT369+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/10.45 % Computer : n005.cluster.edu
% 0.10/10.45 % Model : x86_64 x86_64
% 0.10/10.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/10.45 % Memory : 8046.5625MB
% 0.10/10.45 % OS : Linux 6.8.0-71-generic
% 0.10/10.45 % CPULimit : 300
% 0.10/10.45 % WCLimit : 300
% 0.10/10.45 % DateTime : Fri Sep 25 21:27:29 UTC 2026
% 0.10/10.45 % CPUTime :
% 0.10/10.45 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/10.45 % Process 272472 was started by sandbox on n005,
% 0.10/10.45 % Fri Sep 25 21:27:29 2026
% 0.10/10.45 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.10/10.49
% 0.10/10.49 % From the command line: assign(max_seconds, 300).
% 0.10/10.49
% 0.10/10.49 % SInE: 117 to sos, 27 to usable, of 144 axioms (tolerance 2.00, depth 0 fixpoint).
% 158.20/31.79
% 158.20/31.79 % given #500 (F,wt=21): 1503 -v1_xboole_0(u1_struct_0(k2_yellow_2(c13,c13,c14))). [resolve(359,b,1460,a),unit_del(a,1034)].
% 158.20/31.79
% 158.20/31.79 % given #1000 (F,wt=28): 3907 -v3_struct_0(g1_orders_2(u1_struct_0(f7(c9)),u1_orders_2(f7(c9)))). [back_unit_del(3223),unit_del(a,3857)].
% 158.20/31.79
% 158.20/31.79 % given #1500 (W,wt=14): 6884 v1_funct_1(f6(c9,c5)). [resolve(2818,a,536,a)].
% 158.20/31.79
% 158.20/31.79 % given #2000 (T,wt=17): 2696 v2_funct_1(c4) | -v4_membered(c4) | v2_membered(f17(c4)). [resolve(979,b,228,b)].
% 158.20/31.79
% 158.20/31.79 % given #2500 (W,wt=18): 2197 v3_membered(A) | -v5_membered(k1_zfmisc_1(A)) | v1_xreal_0(f17(A)). [resolve(789,b,212,b)].
% 158.20/31.79
% 158.20/31.79 % given #3000 (T,wt=18): 6158 m1_relset_1(f5(c3,c3),u1_struct_0(c3),u1_struct_0(c3)). [resolve(681,d,438,a),unit_del(a,435),unit_del(b,436),unit_del(c,437),unit_del(d,439),unit_del(e,432)].
% 158.20/31.79
% 158.20/31.79 % given #3500 (A,wt=24): 1804 v3_struct_0(f3(c9)) | v6_waybel_1(k7_grcat_1(f3(c9)),f3(c9)). [resolve(387,b,1342,a)].
% 158.20/31.79
% 158.20/31.79 % given #4000 (T,wt=19): 2535 v2_funct_1(k7_grcat_1(f3(c3))). [resolve(2534,a,382,a)].
% 158.20/31.79
% 158.20/31.79 % given #4500 (F,wt=45): 23485 -l1_orders_2(k2_yellow_2(c13,c13,k7_grcat_1(c13))) | -v3_struct_0(g1_orders_2(u1_struct_0(k2_yellow_2(c13,c13,k7_grcat_1(c13))),u1_orders_2(k2_yellow_2(c13,c13,k7_grcat_1(c13))))). [resolve(2763,a,427,a)].
% 158.20/31.79
% 158.20/31.79 % given #5000 (W,wt=17): 23883 k1_zfmisc_1(c14) = k1_xboole_0 | -v1_xboole_0(k1_zfmisc_1(c14)). [resolve(13002,a,187,a)].
% 158.20/31.79
% 158.20/31.79 % given #5500 (T,wt=19): 20536 v1_membered(f18(c12)) | -v2_membered(k1_zfmisc_1(c12)) | v1_xreal_0(f17(c12)). [resolve(20507,b,193,b)].
% 158.20/31.79
% 158.20/31.79 % given #6000 (A,wt=21): 3987 v7_waybel_1(f10(f7(c8)),f7(c8)). [back_unit_del(3732),unit_del(a,3986)].
% 158.20/31.79
% 158.20/31.79 % given #6500 (F,wt=19): 25405 -v1_xboole_0(f9(f7(c5))). [resolve(4198,a,610,h),unit_del(a,804),unit_del(b,2924),unit_del(c,3048),unit_del(d,4182),unit_del(e,4230),unit_del(f,4228),unit_del(g,4207)].
% 158.20/31.79
% 158.20/31.79 % given #7000 (W,wt=20): 4573 v3_struct_0(A) | -l1_orders_2(A) | v17_waybel_0(f13(A,c3),A,c3). [resolve(568,f,442,a),unit_del(c,433),unit_del(d,435),unit_del(e,437),unit_del(f,432)].
% 158.20/31.79
% 158.20/31.79 % given #7500 (W,wt=18): 26390 v1_funct_2(f13(c9,c13),u1_struct_0(c9),u1_struct_0(c13)). [resolve(4559,b,536,a),unit_del(a,537)].
% 158.20/31.79
% 158.20/31.79 % given #8000 (A,wt=27): 4746 v3_struct_0(A) | -l1_orders_2(A) | v22_waybel_0(f15(A,f7(c9)),A,f7(c9)). [resolve(583,f,3052,a),unit_del(c,739),unit_del(d,2922),unit_del(e,3046),unit_del(f,3857)].
% 158.20/31.79
% 158.20/31.79 % SZS status Theorem for theBenchmark
% 158.20/31.79
% 158.20/31.79 % Proof 1 at 3.78 (+ 1.32) seconds.
% 158.20/31.79 % Length of proof is 70.
% 158.20/31.79 % Level of proof is 5.
% 158.20/31.79 % Maximum clause weight is 149.000.
% 158.20/31.79 % Given clauses 8317.
% 158.20/31.79
% 158.20/31.79 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------