%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : LAT356+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 : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 07:50:23 AM UTC 2026
% Result : Theorem 7.92s 1.47s
% Output : CNFRefutation 7.92s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 9
% Syntax : Number of formulae : 91 ( 19 unt; 0 def)
% Number of atoms : 729 ( 60 equ)
% Maximal formula atoms : 23 ( 8 avg)
% Number of connectives : 1178 ( 540 ~; 532 |; 85 &)
% ( 2 <=>; 19 =>; 0 <=; 0 <~>)
% Maximal formula depth : 24 ( 9 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 31 ( 29 usr; 1 prp; 0-3 aty)
% Number of functors : 6 ( 6 usr; 1 con; 0-4 aty)
% Number of variables : 33 ( 0 sgn 16 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(cc1_lattice3,axiom,
! [A] :
( l1_orders_2(A)
=> ( v1_lattice3(A)
=> ~ v3_struct_0(A) ) ),
file('theBenchmark.p',cc1_lattice3) ).
fof(d1_waybel34,axiom,
! [A] :
( ( l1_orders_2(A)
& v2_lattice3(A)
& v1_lattice3(A)
& v4_orders_2(A)
& v3_orders_2(A)
& v2_orders_2(A) )
=> ! [B] :
( ( l1_orders_2(B)
& v2_lattice3(B)
& v1_lattice3(B)
& v4_orders_2(B)
& v3_orders_2(B)
& v2_orders_2(B) )
=> ! [C] :
( ( m2_relset_1(C,u1_struct_0(A),u1_struct_0(B))
& v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
& v1_funct_1(C) )
=> ( ( v17_waybel_0(C,A,B)
& v3_lattice3(B)
& v3_lattice3(A) )
=> ! [D] :
( ( m2_relset_1(D,u1_struct_0(B),u1_struct_0(A))
& v1_funct_2(D,u1_struct_0(B),u1_struct_0(A))
& v1_funct_1(D) )
=> ( D = k1_waybel34(A,B,C)
<=> v3_waybel_1(k1_waybel_1(A,B,C,D),A,B) ) ) ) ) ) ),
file('theBenchmark.p',d1_waybel34) ).
fof(d2_waybel34,axiom,
! [A] :
( ( l1_orders_2(A)
& v2_lattice3(A)
& v1_lattice3(A)
& v4_orders_2(A)
& v3_orders_2(A)
& v2_orders_2(A) )
=> ! [B] :
( ( l1_orders_2(B)
& v2_lattice3(B)
& v1_lattice3(B)
& v4_orders_2(B)
& v3_orders_2(B)
& v2_orders_2(B) )
=> ! [C] :
( ( m2_relset_1(C,u1_struct_0(B),u1_struct_0(A))
& v1_funct_2(C,u1_struct_0(B),u1_struct_0(A))
& v1_funct_1(C) )
=> ( ( v18_waybel_0(C,B,A)
& v3_lattice3(B)
& v3_lattice3(A) )
=> ! [D] :
( ( m2_relset_1(D,u1_struct_0(A),u1_struct_0(B))
& v1_funct_2(D,u1_struct_0(A),u1_struct_0(B))
& v1_funct_1(D) )
=> ( D = k2_waybel34(A,B,C)
<=> v3_waybel_1(k1_waybel_1(A,B,D,C),A,B) ) ) ) ) ) ),
file('theBenchmark.p',d2_waybel34) ).
fof(dt_k7_grcat_1,axiom,
! [A] :
( l1_struct_0(A)
=> ( m2_relset_1(k7_grcat_1(A),u1_struct_0(A),u1_struct_0(A))
& v1_funct_2(k7_grcat_1(A),u1_struct_0(A),u1_struct_0(A))
& v1_funct_1(k7_grcat_1(A)) ) ),
file('theBenchmark.p',dt_k7_grcat_1) ).
fof(dt_l1_orders_2,axiom,
! [A] :
( l1_orders_2(A)
=> l1_struct_0(A) ),
file('theBenchmark.p',dt_l1_orders_2) ).
fof(fc2_waybel_1,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('theBenchmark.p',fc2_waybel_1) ).
fof(fc4_waybel10,axiom,
! [A] :
( ( l1_orders_2(A)
& v2_orders_2(A)
& ~ v3_struct_0(A) )
=> ( v8_waybel_1(k7_grcat_1(A),A)
& v7_waybel_1(k7_grcat_1(A),A)
& v6_waybel_1(k7_grcat_1(A),A)
& v23_waybel_0(k7_grcat_1(A),A,A)
& v22_waybel_0(k7_grcat_1(A),A,A)
& v21_waybel_0(k7_grcat_1(A),A,A)
& v20_waybel_0(k7_grcat_1(A),A,A)
& v19_waybel_0(k7_grcat_1(A),A,A)
& v18_waybel_0(k7_grcat_1(A),A,A)
& v17_waybel_0(k7_grcat_1(A),A,A)
& v5_orders_3(k7_grcat_1(A),A,A)
& v11_quantal1(k7_grcat_1(A))
& v1_partfun1(k7_grcat_1(A),u1_struct_0(A),u1_struct_0(A))
& v1_funct_2(k7_grcat_1(A),u1_struct_0(A),u1_struct_0(A))
& ~ v1_xboole_0(k7_grcat_1(A))
& v2_funct_1(k7_grcat_1(A))
& v1_funct_1(k7_grcat_1(A))
& v1_relat_1(k7_grcat_1(A)) ) ),
file('theBenchmark.p',fc4_waybel10) ).
fof(t6_waybel34,axiom,
! [A] :
( ( l1_orders_2(A)
& ~ v3_struct_0(A) )
=> v3_waybel_1(k1_waybel_1(A,A,k7_grcat_1(A),k7_grcat_1(A)),A,A) ),
file('theBenchmark.p',t6_waybel34) ).
fof(t7_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) )
=> ( k2_waybel34(A,A,k7_grcat_1(A)) = k7_grcat_1(A)
& k1_waybel34(A,A,k7_grcat_1(A)) = k7_grcat_1(A) ) ),
file('theBenchmark.p',t7_waybel34) ).
fof(t7_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) )
=> ( k2_waybel34(A,A,k7_grcat_1(A)) = k7_grcat_1(A)
& k1_waybel34(A,A,k7_grcat_1(A)) = k7_grcat_1(A) ) ),
inference(assume_negation,[status(cth)],[t7_waybel34]) ).
cnf(c_195,plain,
( ~ v3_struct_0(A)
| ~ v1_lattice3(A)
| ~ l1_orders_2(A) ),
inference(clausify,[status(thm)],[cc1_lattice3]) ).
cnf(c_250,plain,
( ~ v3_waybel_1(k1_waybel_1(A,B,C,D),A,B)
| k1_waybel34(A,B,C) = D
| ~ m2_relset_1(D,u1_struct_0(B),u1_struct_0(A))
| ~ v1_funct_2(D,u1_struct_0(B),u1_struct_0(A))
| ~ v1_funct_1(D)
| ~ v17_waybel_0(C,A,B)
| ~ v3_lattice3(B)
| ~ v3_lattice3(A)
| ~ m2_relset_1(C,u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_1(C)
| ~ l1_orders_2(B)
| ~ v2_lattice3(B)
| ~ v1_lattice3(B)
| ~ v4_orders_2(B)
| ~ v3_orders_2(B)
| ~ v2_orders_2(B)
| ~ l1_orders_2(A)
| ~ v2_lattice3(A)
| ~ v1_lattice3(A)
| ~ v4_orders_2(A)
| ~ v3_orders_2(A)
| ~ v2_orders_2(A) ),
inference(clausify,[status(thm)],[d1_waybel34]) ).
cnf(c_252,plain,
( ~ v3_waybel_1(k1_waybel_1(A,B,D,C),A,B)
| k2_waybel34(A,B,C) = D
| ~ m2_relset_1(D,u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_2(D,u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_1(D)
| ~ v18_waybel_0(C,B,A)
| ~ v3_lattice3(B)
| ~ v3_lattice3(A)
| ~ m2_relset_1(C,u1_struct_0(B),u1_struct_0(A))
| ~ v1_funct_2(C,u1_struct_0(B),u1_struct_0(A))
| ~ v1_funct_1(C)
| ~ l1_orders_2(B)
| ~ v2_lattice3(B)
| ~ v1_lattice3(B)
| ~ v4_orders_2(B)
| ~ v3_orders_2(B)
| ~ v2_orders_2(B)
| ~ l1_orders_2(A)
| ~ v2_lattice3(A)
| ~ v1_lattice3(A)
| ~ v4_orders_2(A)
| ~ v3_orders_2(A)
| ~ v2_orders_2(A) ),
inference(clausify,[status(thm)],[d2_waybel34]) ).
cnf(c_262,plain,
( m2_relset_1(k7_grcat_1(A),u1_struct_0(A),u1_struct_0(A))
| ~ l1_struct_0(A) ),
inference(clausify,[status(thm)],[dt_k7_grcat_1]) ).
cnf(c_263,plain,
( l1_struct_0(A)
| ~ l1_orders_2(A) ),
inference(clausify,[status(thm)],[dt_l1_orders_2]) ).
cnf(c_317,plain,
( v1_funct_1(k7_grcat_1(A))
| ~ l1_orders_2(A) ),
inference(clausify,[status(thm)],[fc2_waybel_1]) ).
cnf(c_318,plain,
( v1_funct_2(k7_grcat_1(A),u1_struct_0(A),u1_struct_0(A))
| ~ l1_orders_2(A) ),
inference(clausify,[status(thm)],[fc2_waybel_1]) ).
cnf(c_329,plain,
( v17_waybel_0(k7_grcat_1(A),A,A)
| ~ l1_orders_2(A)
| ~ v2_orders_2(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[fc4_waybel10]) ).
cnf(c_330,plain,
( v18_waybel_0(k7_grcat_1(A),A,A)
| ~ l1_orders_2(A)
| ~ v2_orders_2(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[fc4_waybel10]) ).
cnf(c_457,plain,
( v3_waybel_1(k1_waybel_1(A,A,k7_grcat_1(A),k7_grcat_1(A)),A,A)
| ~ l1_orders_2(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t6_waybel34]) ).
fof(nnf_130,plain,
? [A] :
( ( k2_waybel34(A,A,k7_grcat_1(A)) != k7_grcat_1(A)
| k1_waybel34(A,A,k7_grcat_1(A)) != k7_grcat_1(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) ),
inference(fof_nnf,[status(thm)],[t7_waybel34_neg]) ).
fof(sk_t7_waybel34_neg,plain,
( ( k2_waybel34(sK0,sK0,k7_grcat_1(sK0)) != k7_grcat_1(sK0)
| k1_waybel34(sK0,sK0,k7_grcat_1(sK0)) != k7_grcat_1(sK0) )
& 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]),skolemize(A,sK0)],[nnf_130]) ).
cnf(c_459,negated_conjecture,
v2_orders_2(sK0),
inference(split_conjunct,[status(thm)],[sk_t7_waybel34_neg]) ).
cnf(c_460,negated_conjecture,
v3_orders_2(sK0),
inference(split_conjunct,[status(thm)],[sk_t7_waybel34_neg]) ).
cnf(c_461,negated_conjecture,
v4_orders_2(sK0),
inference(split_conjunct,[status(thm)],[sk_t7_waybel34_neg]) ).
cnf(c_462,negated_conjecture,
v1_lattice3(sK0),
inference(split_conjunct,[status(thm)],[sk_t7_waybel34_neg]) ).
cnf(c_463,negated_conjecture,
v2_lattice3(sK0),
inference(split_conjunct,[status(thm)],[sk_t7_waybel34_neg]) ).
cnf(c_464,negated_conjecture,
v3_lattice3(sK0),
inference(split_conjunct,[status(thm)],[sk_t7_waybel34_neg]) ).
cnf(c_465,negated_conjecture,
l1_orders_2(sK0),
inference(split_conjunct,[status(thm)],[sk_t7_waybel34_neg]) ).
cnf(c_466,negated_conjecture,
( k2_waybel34(sK0,sK0,k7_grcat_1(sK0)) != k7_grcat_1(sK0)
| k1_waybel34(sK0,sK0,k7_grcat_1(sK0)) != k7_grcat_1(sK0) ),
inference(split_conjunct,[status(thm)],[sk_t7_waybel34_neg]) ).
cnf(c_5999,negated_conjecture,
( ~ v3_struct_0(sK0)
| ~ l1_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_462,c_195]) ).
cnf(c_576,negated_conjecture,
~ v3_struct_0(sK0),
inference(resolve,[status(thm)],[c_465,c_5999]) ).
cnf(c_584,plain,
v1_funct_1(k7_grcat_1(sK0)),
inference(resolve,[status(thm)],[c_317,c_465]) ).
cnf(c_599,plain,
v1_funct_2(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0)),
inference(resolve,[status(thm)],[c_318,c_465]) ).
cnf(c_6000,negated_conjecture,
( v3_waybel_1(k1_waybel_1(sK0,sK0,k7_grcat_1(sK0),k7_grcat_1(sK0)),sK0,sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_457,c_465]) ).
cnf(c_677,negated_conjecture,
v3_waybel_1(k1_waybel_1(sK0,sK0,k7_grcat_1(sK0),k7_grcat_1(sK0)),sK0,sK0),
inference(resolve,[status(thm)],[c_576,c_6000]) ).
cnf(c_6001,plain,
( k1_waybel34(sK0,sK0,k7_grcat_1(sK0)) = k7_grcat_1(sK0)
| ~ m2_relset_1(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(k7_grcat_1(sK0))
| ~ v17_waybel_0(k7_grcat_1(sK0),sK0,sK0)
| ~ v3_lattice3(sK0)
| ~ v3_lattice3(sK0)
| ~ m2_relset_1(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(k7_grcat_1(sK0))
| ~ l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| ~ l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_250,c_677]) ).
cnf(c_6002,plain,
( k1_waybel34(sK0,sK0,k7_grcat_1(sK0)) = k7_grcat_1(sK0)
| ~ m2_relset_1(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(k7_grcat_1(sK0))
| ~ v17_waybel_0(k7_grcat_1(sK0),sK0,sK0)
| ~ v3_lattice3(sK0)
| ~ v3_lattice3(sK0)
| ~ m2_relset_1(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(k7_grcat_1(sK0))
| ~ l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0) ),
inference(copy,[status(thm)],[c_6001]) ).
cnf(c_6003,plain,
( k1_waybel34(sK0,sK0,k7_grcat_1(sK0)) = k7_grcat_1(sK0)
| ~ m2_relset_1(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(k7_grcat_1(sK0))
| ~ v17_waybel_0(k7_grcat_1(sK0),sK0,sK0)
| ~ v3_lattice3(sK0)
| ~ v3_lattice3(sK0)
| ~ m2_relset_1(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(k7_grcat_1(sK0))
| ~ l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0) ),
inference(copy,[status(thm)],[c_6002]) ).
cnf(c_6004,plain,
( k1_waybel34(sK0,sK0,k7_grcat_1(sK0)) = k7_grcat_1(sK0)
| ~ m2_relset_1(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(k7_grcat_1(sK0))
| ~ v17_waybel_0(k7_grcat_1(sK0),sK0,sK0)
| ~ v3_lattice3(sK0)
| ~ v3_lattice3(sK0)
| ~ m2_relset_1(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(k7_grcat_1(sK0))
| ~ l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0) ),
inference(copy,[status(thm)],[c_6003]) ).
cnf(c_6005,plain,
( k1_waybel34(sK0,sK0,k7_grcat_1(sK0)) = k7_grcat_1(sK0)
| ~ m2_relset_1(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(k7_grcat_1(sK0))
| ~ v17_waybel_0(k7_grcat_1(sK0),sK0,sK0)
| ~ v3_lattice3(sK0)
| ~ v3_lattice3(sK0)
| ~ m2_relset_1(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(k7_grcat_1(sK0))
| ~ l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0) ),
inference(copy,[status(thm)],[c_6004]) ).
cnf(c_6006,plain,
( k1_waybel34(sK0,sK0,k7_grcat_1(sK0)) = k7_grcat_1(sK0)
| ~ m2_relset_1(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(k7_grcat_1(sK0))
| ~ v17_waybel_0(k7_grcat_1(sK0),sK0,sK0)
| ~ v3_lattice3(sK0)
| ~ v3_lattice3(sK0)
| ~ m2_relset_1(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(k7_grcat_1(sK0))
| ~ l1_orders_2(sK0)
| ~ l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0) ),
inference(copy,[status(thm)],[c_6005]) ).
cnf(c_6007,plain,
( k1_waybel34(sK0,sK0,k7_grcat_1(sK0)) = k7_grcat_1(sK0)
| ~ m2_relset_1(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(k7_grcat_1(sK0))
| ~ v17_waybel_0(k7_grcat_1(sK0),sK0,sK0)
| ~ v3_lattice3(sK0)
| ~ v3_lattice3(sK0)
| ~ m2_relset_1(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(k7_grcat_1(sK0))
| ~ l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0) ),
inference(copy,[status(thm)],[c_6006]) ).
cnf(c_6008,plain,
( k1_waybel34(sK0,sK0,k7_grcat_1(sK0)) = k7_grcat_1(sK0)
| ~ m2_relset_1(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(k7_grcat_1(sK0))
| ~ v17_waybel_0(k7_grcat_1(sK0),sK0,sK0)
| ~ v3_lattice3(sK0)
| ~ m2_relset_1(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(k7_grcat_1(sK0))
| ~ l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0) ),
inference(copy,[status(thm)],[c_6007]) ).
cnf(c_6009,plain,
( k1_waybel34(sK0,sK0,k7_grcat_1(sK0)) = k7_grcat_1(sK0)
| ~ m2_relset_1(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v17_waybel_0(k7_grcat_1(sK0),sK0,sK0)
| ~ v3_lattice3(sK0)
| ~ m2_relset_1(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(k7_grcat_1(sK0))
| ~ l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0) ),
inference(copy,[status(thm)],[c_6008]) ).
cnf(c_6010,plain,
( k1_waybel34(sK0,sK0,k7_grcat_1(sK0)) = k7_grcat_1(sK0)
| ~ m2_relset_1(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v17_waybel_0(k7_grcat_1(sK0),sK0,sK0)
| ~ v3_lattice3(sK0)
| ~ m2_relset_1(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(k7_grcat_1(sK0))
| ~ l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0) ),
inference(copy,[status(thm)],[c_6009]) ).
cnf(c_6011,plain,
( k1_waybel34(sK0,sK0,k7_grcat_1(sK0)) = k7_grcat_1(sK0)
| ~ v17_waybel_0(k7_grcat_1(sK0),sK0,sK0)
| ~ v3_lattice3(sK0)
| ~ m2_relset_1(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(k7_grcat_1(sK0))
| ~ l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0) ),
inference(copy,[status(thm)],[c_6010]) ).
cnf(c_6012,negated_conjecture,
( k1_waybel34(sK0,sK0,k7_grcat_1(sK0)) = k7_grcat_1(sK0)
| ~ v17_waybel_0(k7_grcat_1(sK0),sK0,sK0)
| ~ v3_lattice3(sK0)
| ~ m2_relset_1(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(k7_grcat_1(sK0))
| ~ l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_459,c_6011]) ).
cnf(c_6013,negated_conjecture,
( k1_waybel34(sK0,sK0,k7_grcat_1(sK0)) = k7_grcat_1(sK0)
| ~ v17_waybel_0(k7_grcat_1(sK0),sK0,sK0)
| ~ v3_lattice3(sK0)
| ~ m2_relset_1(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(k7_grcat_1(sK0))
| ~ l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_460,c_6012]) ).
cnf(c_6014,negated_conjecture,
( k1_waybel34(sK0,sK0,k7_grcat_1(sK0)) = k7_grcat_1(sK0)
| ~ v17_waybel_0(k7_grcat_1(sK0),sK0,sK0)
| ~ v3_lattice3(sK0)
| ~ m2_relset_1(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(k7_grcat_1(sK0))
| ~ l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0) ),
inference(resolve,[status(thm)],[c_461,c_6013]) ).
cnf(c_6015,negated_conjecture,
( k1_waybel34(sK0,sK0,k7_grcat_1(sK0)) = k7_grcat_1(sK0)
| ~ v17_waybel_0(k7_grcat_1(sK0),sK0,sK0)
| ~ v3_lattice3(sK0)
| ~ m2_relset_1(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(k7_grcat_1(sK0))
| ~ l1_orders_2(sK0)
| ~ v2_lattice3(sK0) ),
inference(resolve,[status(thm)],[c_462,c_6014]) ).
cnf(c_6016,negated_conjecture,
( k1_waybel34(sK0,sK0,k7_grcat_1(sK0)) = k7_grcat_1(sK0)
| ~ v17_waybel_0(k7_grcat_1(sK0),sK0,sK0)
| ~ v3_lattice3(sK0)
| ~ m2_relset_1(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(k7_grcat_1(sK0))
| ~ l1_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_463,c_6015]) ).
cnf(c_6017,negated_conjecture,
( k1_waybel34(sK0,sK0,k7_grcat_1(sK0)) = k7_grcat_1(sK0)
| ~ v17_waybel_0(k7_grcat_1(sK0),sK0,sK0)
| ~ v3_lattice3(sK0)
| ~ m2_relset_1(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(k7_grcat_1(sK0)) ),
inference(resolve,[status(thm)],[c_465,c_6016]) ).
cnf(c_6018,negated_conjecture,
( k1_waybel34(sK0,sK0,k7_grcat_1(sK0)) = k7_grcat_1(sK0)
| ~ v17_waybel_0(k7_grcat_1(sK0),sK0,sK0)
| ~ v3_lattice3(sK0)
| ~ m2_relset_1(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_584,c_6017]) ).
cnf(c_6019,negated_conjecture,
( k1_waybel34(sK0,sK0,k7_grcat_1(sK0)) = k7_grcat_1(sK0)
| ~ v17_waybel_0(k7_grcat_1(sK0),sK0,sK0)
| ~ v3_lattice3(sK0)
| ~ m2_relset_1(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_599,c_6018]) ).
cnf(c_1245,negated_conjecture,
( k1_waybel34(sK0,sK0,k7_grcat_1(sK0)) = k7_grcat_1(sK0)
| ~ v17_waybel_0(k7_grcat_1(sK0),sK0,sK0)
| ~ m2_relset_1(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_464,c_6019]) ).
cnf(c_6020,plain,
( k2_waybel34(sK0,sK0,k7_grcat_1(sK0)) = k7_grcat_1(sK0)
| ~ m2_relset_1(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(k7_grcat_1(sK0))
| ~ v18_waybel_0(k7_grcat_1(sK0),sK0,sK0)
| ~ v3_lattice3(sK0)
| ~ v3_lattice3(sK0)
| ~ m2_relset_1(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(k7_grcat_1(sK0))
| ~ l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| ~ l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_252,c_677]) ).
cnf(c_6021,plain,
( k2_waybel34(sK0,sK0,k7_grcat_1(sK0)) = k7_grcat_1(sK0)
| ~ m2_relset_1(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(k7_grcat_1(sK0))
| ~ v18_waybel_0(k7_grcat_1(sK0),sK0,sK0)
| ~ v3_lattice3(sK0)
| ~ v3_lattice3(sK0)
| ~ m2_relset_1(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(k7_grcat_1(sK0))
| ~ l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0) ),
inference(copy,[status(thm)],[c_6020]) ).
cnf(c_6022,plain,
( k2_waybel34(sK0,sK0,k7_grcat_1(sK0)) = k7_grcat_1(sK0)
| ~ m2_relset_1(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(k7_grcat_1(sK0))
| ~ v18_waybel_0(k7_grcat_1(sK0),sK0,sK0)
| ~ v3_lattice3(sK0)
| ~ v3_lattice3(sK0)
| ~ m2_relset_1(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(k7_grcat_1(sK0))
| ~ l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0) ),
inference(copy,[status(thm)],[c_6021]) ).
cnf(c_6023,plain,
( k2_waybel34(sK0,sK0,k7_grcat_1(sK0)) = k7_grcat_1(sK0)
| ~ m2_relset_1(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(k7_grcat_1(sK0))
| ~ v18_waybel_0(k7_grcat_1(sK0),sK0,sK0)
| ~ v3_lattice3(sK0)
| ~ v3_lattice3(sK0)
| ~ m2_relset_1(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(k7_grcat_1(sK0))
| ~ l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0) ),
inference(copy,[status(thm)],[c_6022]) ).
cnf(c_6024,plain,
( k2_waybel34(sK0,sK0,k7_grcat_1(sK0)) = k7_grcat_1(sK0)
| ~ m2_relset_1(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(k7_grcat_1(sK0))
| ~ v18_waybel_0(k7_grcat_1(sK0),sK0,sK0)
| ~ v3_lattice3(sK0)
| ~ v3_lattice3(sK0)
| ~ m2_relset_1(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(k7_grcat_1(sK0))
| ~ l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0) ),
inference(copy,[status(thm)],[c_6023]) ).
cnf(c_6025,plain,
( k2_waybel34(sK0,sK0,k7_grcat_1(sK0)) = k7_grcat_1(sK0)
| ~ m2_relset_1(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(k7_grcat_1(sK0))
| ~ v18_waybel_0(k7_grcat_1(sK0),sK0,sK0)
| ~ v3_lattice3(sK0)
| ~ v3_lattice3(sK0)
| ~ m2_relset_1(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(k7_grcat_1(sK0))
| ~ l1_orders_2(sK0)
| ~ l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0) ),
inference(copy,[status(thm)],[c_6024]) ).
cnf(c_6026,plain,
( k2_waybel34(sK0,sK0,k7_grcat_1(sK0)) = k7_grcat_1(sK0)
| ~ m2_relset_1(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(k7_grcat_1(sK0))
| ~ v18_waybel_0(k7_grcat_1(sK0),sK0,sK0)
| ~ v3_lattice3(sK0)
| ~ v3_lattice3(sK0)
| ~ m2_relset_1(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(k7_grcat_1(sK0))
| ~ l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0) ),
inference(copy,[status(thm)],[c_6025]) ).
cnf(c_6027,plain,
( k2_waybel34(sK0,sK0,k7_grcat_1(sK0)) = k7_grcat_1(sK0)
| ~ m2_relset_1(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(k7_grcat_1(sK0))
| ~ v18_waybel_0(k7_grcat_1(sK0),sK0,sK0)
| ~ v3_lattice3(sK0)
| ~ m2_relset_1(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(k7_grcat_1(sK0))
| ~ l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0) ),
inference(copy,[status(thm)],[c_6026]) ).
cnf(c_6028,plain,
( k2_waybel34(sK0,sK0,k7_grcat_1(sK0)) = k7_grcat_1(sK0)
| ~ m2_relset_1(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v18_waybel_0(k7_grcat_1(sK0),sK0,sK0)
| ~ v3_lattice3(sK0)
| ~ m2_relset_1(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(k7_grcat_1(sK0))
| ~ l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0) ),
inference(copy,[status(thm)],[c_6027]) ).
cnf(c_6029,plain,
( k2_waybel34(sK0,sK0,k7_grcat_1(sK0)) = k7_grcat_1(sK0)
| ~ m2_relset_1(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v18_waybel_0(k7_grcat_1(sK0),sK0,sK0)
| ~ v3_lattice3(sK0)
| ~ m2_relset_1(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(k7_grcat_1(sK0))
| ~ l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0) ),
inference(copy,[status(thm)],[c_6028]) ).
cnf(c_6030,plain,
( k2_waybel34(sK0,sK0,k7_grcat_1(sK0)) = k7_grcat_1(sK0)
| ~ v18_waybel_0(k7_grcat_1(sK0),sK0,sK0)
| ~ v3_lattice3(sK0)
| ~ m2_relset_1(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(k7_grcat_1(sK0))
| ~ l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0) ),
inference(copy,[status(thm)],[c_6029]) ).
cnf(c_6031,negated_conjecture,
( k2_waybel34(sK0,sK0,k7_grcat_1(sK0)) = k7_grcat_1(sK0)
| ~ v18_waybel_0(k7_grcat_1(sK0),sK0,sK0)
| ~ v3_lattice3(sK0)
| ~ m2_relset_1(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(k7_grcat_1(sK0))
| ~ l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_459,c_6030]) ).
cnf(c_6032,negated_conjecture,
( k2_waybel34(sK0,sK0,k7_grcat_1(sK0)) = k7_grcat_1(sK0)
| ~ v18_waybel_0(k7_grcat_1(sK0),sK0,sK0)
| ~ v3_lattice3(sK0)
| ~ m2_relset_1(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(k7_grcat_1(sK0))
| ~ l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_460,c_6031]) ).
cnf(c_6033,negated_conjecture,
( k2_waybel34(sK0,sK0,k7_grcat_1(sK0)) = k7_grcat_1(sK0)
| ~ v18_waybel_0(k7_grcat_1(sK0),sK0,sK0)
| ~ v3_lattice3(sK0)
| ~ m2_relset_1(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(k7_grcat_1(sK0))
| ~ l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0) ),
inference(resolve,[status(thm)],[c_461,c_6032]) ).
cnf(c_6034,negated_conjecture,
( k2_waybel34(sK0,sK0,k7_grcat_1(sK0)) = k7_grcat_1(sK0)
| ~ v18_waybel_0(k7_grcat_1(sK0),sK0,sK0)
| ~ v3_lattice3(sK0)
| ~ m2_relset_1(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(k7_grcat_1(sK0))
| ~ l1_orders_2(sK0)
| ~ v2_lattice3(sK0) ),
inference(resolve,[status(thm)],[c_462,c_6033]) ).
cnf(c_6035,negated_conjecture,
( k2_waybel34(sK0,sK0,k7_grcat_1(sK0)) = k7_grcat_1(sK0)
| ~ v18_waybel_0(k7_grcat_1(sK0),sK0,sK0)
| ~ v3_lattice3(sK0)
| ~ m2_relset_1(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(k7_grcat_1(sK0))
| ~ l1_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_463,c_6034]) ).
cnf(c_6036,negated_conjecture,
( k2_waybel34(sK0,sK0,k7_grcat_1(sK0)) = k7_grcat_1(sK0)
| ~ v18_waybel_0(k7_grcat_1(sK0),sK0,sK0)
| ~ v3_lattice3(sK0)
| ~ m2_relset_1(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(k7_grcat_1(sK0)) ),
inference(resolve,[status(thm)],[c_465,c_6035]) ).
cnf(c_6037,negated_conjecture,
( k2_waybel34(sK0,sK0,k7_grcat_1(sK0)) = k7_grcat_1(sK0)
| ~ v18_waybel_0(k7_grcat_1(sK0),sK0,sK0)
| ~ v3_lattice3(sK0)
| ~ m2_relset_1(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_584,c_6036]) ).
cnf(c_6038,negated_conjecture,
( k2_waybel34(sK0,sK0,k7_grcat_1(sK0)) = k7_grcat_1(sK0)
| ~ v18_waybel_0(k7_grcat_1(sK0),sK0,sK0)
| ~ v3_lattice3(sK0)
| ~ m2_relset_1(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_599,c_6037]) ).
cnf(c_1332,negated_conjecture,
( k2_waybel34(sK0,sK0,k7_grcat_1(sK0)) = k7_grcat_1(sK0)
| ~ v18_waybel_0(k7_grcat_1(sK0),sK0,sK0)
| ~ m2_relset_1(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_464,c_6038]) ).
cnf(c_1487,plain,
l1_struct_0(sK0),
inference(resolve,[status(thm)],[c_263,c_465]) ).
cnf(c_1490,plain,
m2_relset_1(k7_grcat_1(sK0),u1_struct_0(sK0),u1_struct_0(sK0)),
inference(resolve,[status(thm)],[c_1487,c_262]) ).
cnf(c_1491,negated_conjecture,
( k2_waybel34(sK0,sK0,k7_grcat_1(sK0)) = k7_grcat_1(sK0)
| ~ v18_waybel_0(k7_grcat_1(sK0),sK0,sK0) ),
inference(resolve,[status(thm)],[c_1490,c_1332]) ).
cnf(c_1492,negated_conjecture,
( k1_waybel34(sK0,sK0,k7_grcat_1(sK0)) = k7_grcat_1(sK0)
| ~ v17_waybel_0(k7_grcat_1(sK0),sK0,sK0) ),
inference(resolve,[status(thm)],[c_1490,c_1245]) ).
cnf(c_6039,negated_conjecture,
( v17_waybel_0(k7_grcat_1(sK0),sK0,sK0)
| ~ l1_orders_2(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_329,c_459]) ).
cnf(c_6040,negated_conjecture,
( v17_waybel_0(k7_grcat_1(sK0),sK0,sK0)
| ~ l1_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_576,c_6039]) ).
cnf(c_5974,negated_conjecture,
v17_waybel_0(k7_grcat_1(sK0),sK0,sK0),
inference(resolve,[status(thm)],[c_465,c_6040]) ).
cnf(c_5977,negated_conjecture,
k1_waybel34(sK0,sK0,k7_grcat_1(sK0)) = k7_grcat_1(sK0),
inference(resolve,[status(thm)],[c_5974,c_1492]) ).
cnf(c_6041,negated_conjecture,
( k2_waybel34(sK0,sK0,k7_grcat_1(sK0)) != k7_grcat_1(sK0)
| k7_grcat_1(sK0) != k7_grcat_1(sK0) ),
inference(paramod,[status(thm)],[c_5977,c_466]) ).
cnf(c_5981,negated_conjecture,
k2_waybel34(sK0,sK0,k7_grcat_1(sK0)) != k7_grcat_1(sK0),
inference(copy,[status(thm)],[c_6041]) ).
cnf(c_5983,negated_conjecture,
~ v18_waybel_0(k7_grcat_1(sK0),sK0,sK0),
inference(resolve,[status(thm)],[c_5981,c_1491]) ).
cnf(c_6042,negated_conjecture,
( v18_waybel_0(k7_grcat_1(sK0),sK0,sK0)
| ~ l1_orders_2(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_330,c_459]) ).
cnf(c_6043,negated_conjecture,
( v18_waybel_0(k7_grcat_1(sK0),sK0,sK0)
| ~ l1_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_576,c_6042]) ).
cnf(c_6044,negated_conjecture,
v18_waybel_0(k7_grcat_1(sK0),sK0,sK0),
inference(resolve,[status(thm)],[c_465,c_6043]) ).
cnf(c_5998,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_5983,c_6044]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT356+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n004.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Fri Sep 25 21:16:06 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.35 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.35 % Process 4167800 was started by sandbox on n004,
% 0.09/0.35 % Fri Sep 25 21:16:06 2026
% 0.09/0.35 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.12/0.41
% 0.12/0.41 % From the command line: assign(max_seconds, 300).
% 0.12/0.41
% 0.12/0.41 % SInE: 103 to sos, 26 to usable, of 129 axioms (tolerance 2.00, depth 0 fixpoint).
% 7.92/1.47
% 7.92/1.47 % given #500 (W,wt=28): 997 -v4_membered(k2_zfmisc_1(u1_struct_0(c8),u1_struct_0(c8))) | v3_membered(k1_waybel34(c8,c8,f15(c8,c8))). [resolve(905,a,191,b)].
% 7.92/1.47
% 7.92/1.47 % given #1000 (A,wt=63): 303 -v2_orders_2(A) | -v3_orders_2(A) | -v4_orders_2(A) | -v1_lattice3(A) | -v2_lattice3(A) | -v3_lattice3(A) | -l1_orders_2(A) | -v2_orders_2(B) | -v3_orders_2(B) | -v4_orders_2(B) | -v1_lattice3(B) | -v2_lattice3(B) | -v3_lattice3(B) | -l1_orders_2(B) | -v1_funct_1(C) | -v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)) | -v17_waybel_0(C,A,B) | -m1_relset_1(C,u1_struct_0(A),u1_struct_0(B)) | v5_waybel_1(k1_waybel34(A,B,C),A,B) # tptp_name(fc1_waybel34) # sine_depth(1). [clausify(67)].
% 7.92/1.47
% 7.92/1.47 % SZS status Theorem for theBenchmark
% 7.92/1.47
% 7.92/1.47 % Proof 1 at 0.84 (+ 0.20) seconds.
% 7.92/1.47 % Length of proof is 42.
% 7.92/1.47 % Level of proof is 9.
% 7.92/1.47 % Maximum clause weight is 121.000.
% 7.92/1.47 % Given clauses 1102.
% 7.92/1.47
% 7.92/1.47 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------