%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : LAT366+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n012.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 : Fri Sep 25 01:59:40 PM UTC 2026
% Result : Theorem 104.30s 19.92s
% Output : CNFRefutation 104.30s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 25
% Syntax : Number of formulae : 294 ( 59 unt; 1 def)
% Number of atoms : 2183 ( 74 equ)
% Maximal formula atoms : 25 ( 7 avg)
% Number of connectives : 3210 (1321 ~;1390 |; 413 &)
% ( 9 <=>; 75 =>; 0 <=; 2 <~>)
% Maximal formula depth : 26 ( 8 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 36 ( 34 usr; 1 prp; 0-3 aty)
% Number of functors : 15 ( 15 usr; 6 con; 0-4 aty)
% Number of variables : 483 ( 0 sgn 455 !; 28 ?; 142 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [X0] :
( ( l1_orders_2(X0)
& v3_lattice3(X0)
& v2_lattice3(X0)
& v1_lattice3(X0)
& v4_orders_2(X0)
& v3_orders_2(X0)
& v2_orders_2(X0) )
=> ! [X1] :
( ( m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
& v8_waybel_1(X1,X0)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v1_funct_1(X1) )
=> ( v22_waybel_0(X1,X0,X0)
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
=> ! [X4] :
( m1_subset_1(X4,u1_struct_0(k2_yellow_2(X0,X0,X1)))
=> ! [X5] :
( m1_subset_1(X5,u1_struct_0(k2_yellow_2(X0,X0,X1)))
=> ( ( X5 = X3
& X4 = X2 )
=> ( r1_waybel_3(X0,X2,X3)
<=> r1_waybel_3(k2_yellow_2(X0,X0,X1),X4,X5) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t37_waybel34) ).
fof(f2,negated_conjecture,
~ ! [X0] :
( ( l1_orders_2(X0)
& v3_lattice3(X0)
& v2_lattice3(X0)
& v1_lattice3(X0)
& v4_orders_2(X0)
& v3_orders_2(X0)
& v2_orders_2(X0) )
=> ! [X1] :
( ( m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
& v8_waybel_1(X1,X0)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v1_funct_1(X1) )
=> ( v22_waybel_0(X1,X0,X0)
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
=> ! [X4] :
( m1_subset_1(X4,u1_struct_0(k2_yellow_2(X0,X0,X1)))
=> ! [X5] :
( m1_subset_1(X5,u1_struct_0(k2_yellow_2(X0,X0,X1)))
=> ( ( X5 = X3
& X4 = X2 )
=> ( r1_waybel_3(X0,X2,X3)
<=> r1_waybel_3(k2_yellow_2(X0,X0,X1),X4,X5) ) ) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f25,axiom,
! [X0] :
( l1_orders_2(X0)
=> ( v1_lattice3(X0)
=> ~ v3_struct_0(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc1_lattice3) ).
fof(f33,axiom,
! [X0] :
( l1_orders_2(X0)
=> ( ( v3_lattice3(X0)
& ~ v3_struct_0(X0) )
=> ( v2_lattice3(X0)
& v1_lattice3(X0)
& ~ v3_struct_0(X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc1_yellow_0) ).
fof(f38,axiom,
! [X0] :
( l1_orders_2(X0)
=> ( v2_lattice3(X0)
=> ~ v3_struct_0(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc2_lattice3) ).
fof(f48,axiom,
! [X0] :
( ( l1_orders_2(X0)
& ~ v3_struct_0(X0) )
=> ! [X1] :
( m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
=> ( ( v8_waybel_1(X1,X0)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v1_funct_1(X1) )
=> ( v6_waybel_1(X1,X0)
& v1_partfun1(X1,u1_struct_0(X0),u1_struct_0(X0))
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& ~ v1_xboole_0(X1)
& v1_funct_1(X1) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc4_waybel_1) ).
fof(f52,axiom,
! [X0] :
( ( l1_orders_2(X0)
& v2_orders_2(X0) )
=> ! [X1] :
( m1_yellow_0(X1,X0)
=> ( v4_yellow_0(X1,X0)
=> ( v4_yellow_0(X1,X0)
& v2_orders_2(X1) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc6_yellow_0) ).
fof(f54,axiom,
! [X0] :
( ( l1_orders_2(X0)
& v3_orders_2(X0) )
=> ! [X1] :
( m1_yellow_0(X1,X0)
=> ( v4_yellow_0(X1,X0)
=> ( v4_yellow_0(X1,X0)
& v3_orders_2(X1) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc7_yellow_0) ).
fof(f56,axiom,
! [X0] :
( ( l1_orders_2(X0)
& v4_orders_2(X0) )
=> ! [X1] :
( m1_yellow_0(X1,X0)
=> ( v4_yellow_0(X1,X0)
=> ( v4_yellow_0(X1,X0)
& v4_orders_2(X1) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc8_yellow_0) ).
fof(f61,axiom,
! [X0] :
( ( l1_orders_2(X0)
& v2_orders_2(X0)
& ~ v3_struct_0(X0) )
=> ! [X1] :
( ( l1_orders_2(X1)
& v2_orders_2(X1)
& ~ v3_struct_0(X1) )
=> ! [X2] :
( ( m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_1(X2) )
=> ( v1_waybel34(X2,X0,X1)
<=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
=> ! [X4] :
( m1_subset_1(X4,u1_struct_0(X0))
=> ( r1_waybel_3(X0,X3,X4)
=> r1_waybel_3(X1,k7_yellow_2(u1_struct_0(X0),X1,X2,X3),k7_yellow_2(u1_struct_0(X0),X1,X2,X4)) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d8_waybel34) ).
fof(f64,axiom,
! [X0,X1,X2] :
( ( m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_1(X2)
& l1_orders_2(X1)
& v2_lattice3(X1)
& v1_lattice3(X1)
& v4_orders_2(X1)
& v3_orders_2(X1)
& v2_orders_2(X1)
& l1_orders_2(X0)
& v2_lattice3(X0)
& v1_lattice3(X0)
& v4_orders_2(X0)
& v3_orders_2(X0)
& v2_orders_2(X0) )
=> ( m2_relset_1(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0))
& v1_funct_2(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0))
& v1_funct_1(k1_waybel34(X0,X1,X2)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k1_waybel34) ).
fof(f67,axiom,
! [X0,X1,X2] :
( ( m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))
& v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
& v1_funct_1(X2)
& l1_orders_2(X1)
& v2_lattice3(X1)
& v1_lattice3(X1)
& v4_orders_2(X1)
& v3_orders_2(X1)
& v2_orders_2(X1)
& l1_orders_2(X0)
& v2_lattice3(X0)
& v1_lattice3(X0)
& v4_orders_2(X0)
& v3_orders_2(X0)
& v2_orders_2(X0) )
=> ( m2_relset_1(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_2(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_1(k2_waybel34(X0,X1,X2)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k2_waybel34) ).
fof(f68,axiom,
! [X0,X1,X2] :
( ( m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_1(X2)
& l1_orders_2(X1)
& ~ v3_struct_0(X1)
& l1_orders_2(X0)
& ~ v3_struct_0(X0) )
=> ( m2_relset_1(k2_waybel_1(X0,X1,X2),u1_struct_0(X0),u1_struct_0(k2_yellow_2(X0,X1,X2)))
& v1_funct_2(k2_waybel_1(X0,X1,X2),u1_struct_0(X0),u1_struct_0(k2_yellow_2(X0,X1,X2)))
& v1_funct_1(k2_waybel_1(X0,X1,X2)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k2_waybel_1) ).
fof(f69,axiom,
! [X0,X1,X2] :
( ( m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_1(X2)
& l1_orders_2(X1)
& ~ v3_struct_0(X1)
& l1_orders_2(X0)
& ~ v3_struct_0(X0) )
=> ( m1_yellow_0(k2_yellow_2(X0,X1,X2),X1)
& v4_yellow_0(k2_yellow_2(X0,X1,X2),X1)
& v1_orders_2(k2_yellow_2(X0,X1,X2)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k2_yellow_2) ).
fof(f71,axiom,
! [X0,X1,X2] :
( ( m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_1(X2)
& l1_orders_2(X1)
& ~ v3_struct_0(X1)
& l1_orders_2(X0)
& ~ v3_struct_0(X0) )
=> ( m2_relset_1(k3_waybel_1(X0,X1,X2),u1_struct_0(k2_yellow_2(X0,X1,X2)),u1_struct_0(X1))
& v1_funct_2(k3_waybel_1(X0,X1,X2),u1_struct_0(k2_yellow_2(X0,X1,X2)),u1_struct_0(X1))
& v1_funct_1(k3_waybel_1(X0,X1,X2)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k3_waybel_1) ).
fof(f79,axiom,
! [X0] :
( l1_orders_2(X0)
=> ! [X1] :
( m1_yellow_0(X1,X0)
=> l1_orders_2(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m1_yellow_0) ).
fof(f90,axiom,
! [X0,X1] :
( ( m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
& v6_waybel_1(X1,X0)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v1_funct_1(X1)
& l1_orders_2(X0)
& v3_lattice3(X0)
& v2_lattice3(X0)
& v1_lattice3(X0)
& v4_orders_2(X0)
& v3_orders_2(X0)
& v2_orders_2(X0) )
=> ( v3_lattice3(k2_yellow_2(X0,X0,X1))
& v2_lattice3(k2_yellow_2(X0,X0,X1))
& v1_lattice3(k2_yellow_2(X0,X0,X1))
& v25_waybel_0(k2_yellow_2(X0,X0,X1))
& v24_waybel_0(k2_yellow_2(X0,X0,X1))
& v4_yellow_0(k2_yellow_2(X0,X0,X1),X0)
& v3_yellow_0(k2_yellow_2(X0,X0,X1))
& v2_yellow_0(k2_yellow_2(X0,X0,X1))
& v1_yellow_0(k2_yellow_2(X0,X0,X1))
& v4_orders_2(k2_yellow_2(X0,X0,X1))
& v3_orders_2(k2_yellow_2(X0,X0,X1))
& v2_orders_2(k2_yellow_2(X0,X0,X1))
& v1_orders_2(k2_yellow_2(X0,X0,X1))
& ~ v3_struct_0(k2_yellow_2(X0,X0,X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc10_waybel34) ).
fof(f99,axiom,
! [X0,X1,X2] :
( ( m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_1(X2)
& l1_orders_2(X1)
& ~ v3_struct_0(X1)
& l1_orders_2(X0)
& ~ v3_struct_0(X0) )
=> ( v4_yellow_0(k2_yellow_2(X0,X1,X2),X1)
& v1_orders_2(k2_yellow_2(X0,X1,X2))
& ~ v3_struct_0(k2_yellow_2(X0,X1,X2)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc2_yellow_2) ).
fof(f145,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
<=> m1_relset_1(X2,X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(f148,axiom,
! [X0] :
( ( l1_orders_2(X0)
& v3_lattice3(X0)
& v2_lattice3(X0)
& v1_lattice3(X0)
& v4_orders_2(X0)
& v3_orders_2(X0)
& v2_orders_2(X0) )
=> ! [X1] :
( ( l1_orders_2(X1)
& v3_lattice3(X1)
& v2_lattice3(X1)
& v1_lattice3(X1)
& v4_orders_2(X1)
& v3_orders_2(X1)
& v2_orders_2(X1) )
=> ! [X2] :
( ( m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
& v17_waybel_0(X2,X0,X1)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_1(X2) )
=> ( v22_waybel_0(X2,X0,X1)
=> v1_waybel34(k1_waybel34(X0,X1,X2),X1,X0) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t24_waybel34) ).
fof(f150,axiom,
! [X0] :
( ( l1_orders_2(X0)
& v3_lattice3(X0)
& v2_lattice3(X0)
& v1_lattice3(X0)
& v4_orders_2(X0)
& v3_orders_2(X0)
& v2_orders_2(X0) )
=> ! [X1] :
( ( m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
& v8_waybel_1(X1,X0)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v1_funct_1(X1) )
=> ( k2_waybel34(X0,k2_yellow_2(X0,X0,X1),k3_waybel_1(X0,X0,X1)) = k2_waybel_1(X0,X0,X1)
& k1_waybel34(X0,k2_yellow_2(X0,X0,X1),k2_waybel_1(X0,X0,X1)) = k3_waybel_1(X0,X0,X1)
& v18_waybel_0(k3_waybel_1(X0,X0,X1),k2_yellow_2(X0,X0,X1),X0)
& v17_waybel_0(k2_waybel_1(X0,X0,X1),X0,k2_yellow_2(X0,X0,X1)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t33_waybel34) ).
fof(f151,axiom,
! [X0] :
( ( l1_orders_2(X0)
& v3_lattice3(X0)
& v2_lattice3(X0)
& v1_lattice3(X0)
& v4_orders_2(X0)
& v3_orders_2(X0)
& v2_orders_2(X0) )
=> ! [X1] :
( ( m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
& v8_waybel_1(X1,X0)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v1_funct_1(X1) )
=> ( v22_waybel_0(X1,X0,X0)
<=> v22_waybel_0(k2_waybel_1(X0,X0,X1),X0,k2_yellow_2(X0,X0,X1)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t34_waybel34) ).
fof(f152,axiom,
! [X0] :
( ( l1_orders_2(X0)
& ~ v3_struct_0(X0) )
=> ! [X1] :
( ( l1_orders_2(X1)
& ~ v3_struct_0(X1) )
=> ! [X2] :
( ( m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_1(X2) )
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(k2_yellow_2(X0,X1,X2)))
=> k7_yellow_2(u1_struct_0(k2_yellow_2(X0,X1,X2)),X1,k3_waybel_1(X0,X1,X2),X3) = X3 ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t34_waybel_1) ).
fof(f153,axiom,
! [X0] :
( ( l1_orders_2(X0)
& v3_lattice3(X0)
& v2_lattice3(X0)
& v1_lattice3(X0)
& v4_orders_2(X0)
& v3_orders_2(X0)
& v2_orders_2(X0) )
=> ! [X1] :
( ( m1_yellow_0(X1,X0)
& v8_yellow_0(X1,X0)
& v4_yellow_0(X1,X0)
& ~ v3_struct_0(X1) )
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
=> ! [X4] :
( m1_subset_1(X4,u1_struct_0(X1))
=> ! [X5] :
( m1_subset_1(X5,u1_struct_0(X1))
=> ( ( r1_waybel_3(X0,X2,X3)
& X5 = X3
& X4 = X2 )
=> r1_waybel_3(X1,X4,X5) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t36_waybel34) ).
fof(f156,axiom,
! [X0] :
( ( l1_orders_2(X0)
& v4_orders_2(X0)
& v3_orders_2(X0)
& v2_orders_2(X0)
& ~ v3_struct_0(X0) )
=> ! [X1] :
( ( m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v1_funct_1(X1) )
=> ( ( v8_waybel_1(X1,X0)
=> v8_yellow_0(k2_yellow_2(X0,X0,X1),X0) )
& ( v7_waybel_1(X1,X0)
=> v7_yellow_0(k2_yellow_2(X0,X0,X1),X0) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t56_waybel_1) ).
fof(f195,plain,
! [X0] :
( ( l1_orders_2(X0)
& ~ v3_struct_0(X0) )
=> ! [X1] :
( m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
=> ( ( v8_waybel_1(X1,X0)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v1_funct_1(X1) )
=> ( v6_waybel_1(X1,X0)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& ~ v1_xboole_0(X1)
& v1_funct_1(X1) ) ) ) ),
inference(pure_predicate_removal,[],[f48]) ).
fof(f209,plain,
? [X0] :
( l1_orders_2(X0)
& v3_lattice3(X0)
& v2_lattice3(X0)
& v1_lattice3(X0)
& v4_orders_2(X0)
& v3_orders_2(X0)
& v2_orders_2(X0)
& ? [X1] :
( m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
& v8_waybel_1(X1,X0)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v1_funct_1(X1)
& v22_waybel_0(X1,X0,X0)
& ? [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
& ? [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
& ? [X4] :
( m1_subset_1(X4,u1_struct_0(k2_yellow_2(X0,X0,X1)))
& ? [X5] :
( m1_subset_1(X5,u1_struct_0(k2_yellow_2(X0,X0,X1)))
& X5 = X3
& X4 = X2
& ( r1_waybel_3(X0,X2,X3)
<~> r1_waybel_3(k2_yellow_2(X0,X0,X1),X4,X5) ) ) ) ) ) ) ),
inference(ennf_transformation,[],[f2]) ).
fof(f210,plain,
? [X0] :
( l1_orders_2(X0)
& v3_lattice3(X0)
& v2_lattice3(X0)
& v1_lattice3(X0)
& v4_orders_2(X0)
& v3_orders_2(X0)
& v2_orders_2(X0)
& ? [X1] :
( m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
& v8_waybel_1(X1,X0)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v1_funct_1(X1)
& v22_waybel_0(X1,X0,X0)
& ? [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
& ? [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
& ? [X4] :
( m1_subset_1(X4,u1_struct_0(k2_yellow_2(X0,X0,X1)))
& ? [X5] :
( m1_subset_1(X5,u1_struct_0(k2_yellow_2(X0,X0,X1)))
& X5 = X3
& X4 = X2
& ( r1_waybel_3(X0,X2,X3)
<~> r1_waybel_3(k2_yellow_2(X0,X0,X1),X4,X5) ) ) ) ) ) ) ),
inference(flattening,[],[f209]) ).
fof(f215,plain,
! [X0,X1,X2] :
( ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| v3_struct_0(X1)
| ~ l1_orders_2(X0)
| v3_struct_0(X0)
| ( v4_yellow_0(k2_yellow_2(X0,X1,X2),X1)
& v1_orders_2(k2_yellow_2(X0,X1,X2))
& ~ v3_struct_0(k2_yellow_2(X0,X1,X2)) ) ),
inference(ennf_transformation,[],[f99]) ).
fof(f216,plain,
! [X0,X1,X2] :
( ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| v3_struct_0(X1)
| ~ l1_orders_2(X0)
| v3_struct_0(X0)
| ( v4_yellow_0(k2_yellow_2(X0,X1,X2),X1)
& v1_orders_2(k2_yellow_2(X0,X1,X2))
& ~ v3_struct_0(k2_yellow_2(X0,X1,X2)) ) ),
inference(flattening,[],[f215]) ).
fof(f217,plain,
! [X0,X1,X2] :
( ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| v3_struct_0(X1)
| ~ l1_orders_2(X0)
| v3_struct_0(X0)
| ( m1_yellow_0(k2_yellow_2(X0,X1,X2),X1)
& v4_yellow_0(k2_yellow_2(X0,X1,X2),X1)
& v1_orders_2(k2_yellow_2(X0,X1,X2)) ) ),
inference(ennf_transformation,[],[f69]) ).
fof(f218,plain,
! [X0,X1,X2] :
( ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| v3_struct_0(X1)
| ~ l1_orders_2(X0)
| v3_struct_0(X0)
| ( m1_yellow_0(k2_yellow_2(X0,X1,X2),X1)
& v4_yellow_0(k2_yellow_2(X0,X1,X2),X1)
& v1_orders_2(k2_yellow_2(X0,X1,X2)) ) ),
inference(flattening,[],[f217]) ).
fof(f219,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| v3_struct_0(X0)
| ( v2_lattice3(X0)
& v1_lattice3(X0)
& ~ v3_struct_0(X0) ) ),
inference(ennf_transformation,[],[f33]) ).
fof(f220,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| v3_struct_0(X0)
| ( v2_lattice3(X0)
& v1_lattice3(X0)
& ~ v3_struct_0(X0) ) ),
inference(flattening,[],[f219]) ).
fof(f221,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v3_struct_0(X0) ),
inference(ennf_transformation,[],[f25]) ).
fof(f222,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v3_struct_0(X0) ),
inference(flattening,[],[f221]) ).
fof(f223,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v3_struct_0(X0) ),
inference(ennf_transformation,[],[f38]) ).
fof(f224,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v3_struct_0(X0) ),
inference(flattening,[],[f223]) ).
fof(f226,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| ( ( ~ v8_waybel_1(X1,X0)
| v8_yellow_0(k2_yellow_2(X0,X0,X1),X0) )
& ( ~ v7_waybel_1(X1,X0)
| v7_yellow_0(k2_yellow_2(X0,X0,X1),X0) ) ) ) ),
inference(ennf_transformation,[],[f156]) ).
fof(f227,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| ( ( ~ v8_waybel_1(X1,X0)
| v8_yellow_0(k2_yellow_2(X0,X0,X1),X0) )
& ( ~ v7_waybel_1(X1,X0)
| v7_yellow_0(k2_yellow_2(X0,X0,X1),X0) ) ) ) ),
inference(flattening,[],[f226]) ).
fof(f228,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ! [X1] :
( ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v8_waybel_1(X1,X0)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| ( v22_waybel_0(X1,X0,X0)
<=> v22_waybel_0(k2_waybel_1(X0,X0,X1),X0,k2_yellow_2(X0,X0,X1)) ) ) ),
inference(ennf_transformation,[],[f151]) ).
fof(f229,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ! [X1] :
( ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v8_waybel_1(X1,X0)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| ( v22_waybel_0(X1,X0,X0)
<=> v22_waybel_0(k2_waybel_1(X0,X0,X1),X0,k2_yellow_2(X0,X0,X1)) ) ) ),
inference(flattening,[],[f228]) ).
fof(f234,plain,
! [X0] :
( ~ l1_orders_2(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v8_waybel_1(X1,X0)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| ( v6_waybel_1(X1,X0)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& ~ v1_xboole_0(X1)
& v1_funct_1(X1) ) ) ),
inference(ennf_transformation,[],[f195]) ).
fof(f235,plain,
! [X0] :
( ~ l1_orders_2(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v8_waybel_1(X1,X0)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| ( v6_waybel_1(X1,X0)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& ~ v1_xboole_0(X1)
& v1_funct_1(X1) ) ) ),
inference(flattening,[],[f234]) ).
fof(f238,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ! [X1] :
( ~ m1_yellow_0(X1,X0)
| ~ v8_yellow_0(X1,X0)
| ~ v4_yellow_0(X1,X0)
| v3_struct_0(X1)
| ! [X2] :
( ~ m1_subset_1(X2,u1_struct_0(X0))
| ! [X3] :
( ~ m1_subset_1(X3,u1_struct_0(X0))
| ! [X4] :
( ~ m1_subset_1(X4,u1_struct_0(X1))
| ! [X5] :
( ~ m1_subset_1(X5,u1_struct_0(X1))
| ~ r1_waybel_3(X0,X2,X3)
| X3 != X5
| X2 != X4
| r1_waybel_3(X1,X4,X5) ) ) ) ) ) ),
inference(ennf_transformation,[],[f153]) ).
fof(f239,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ! [X1] :
( ~ m1_yellow_0(X1,X0)
| ~ v8_yellow_0(X1,X0)
| ~ v4_yellow_0(X1,X0)
| v3_struct_0(X1)
| ! [X2] :
( ~ m1_subset_1(X2,u1_struct_0(X0))
| ! [X3] :
( ~ m1_subset_1(X3,u1_struct_0(X0))
| ! [X4] :
( ~ m1_subset_1(X4,u1_struct_0(X1))
| ! [X5] :
( ~ m1_subset_1(X5,u1_struct_0(X1))
| ~ r1_waybel_3(X0,X2,X3)
| X3 != X5
| X2 != X4
| r1_waybel_3(X1,X4,X5) ) ) ) ) ) ),
inference(flattening,[],[f238]) ).
fof(f240,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v2_orders_2(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ l1_orders_2(X1)
| ~ v2_orders_2(X1)
| v3_struct_0(X1)
| ! [X2] :
( ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ( v1_waybel34(X2,X0,X1)
<=> ! [X3] :
( ~ m1_subset_1(X3,u1_struct_0(X0))
| ! [X4] :
( ~ m1_subset_1(X4,u1_struct_0(X0))
| ~ r1_waybel_3(X0,X3,X4)
| r1_waybel_3(X1,k7_yellow_2(u1_struct_0(X0),X1,X2,X3),k7_yellow_2(u1_struct_0(X0),X1,X2,X4)) ) ) ) ) ) ),
inference(ennf_transformation,[],[f61]) ).
fof(f241,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v2_orders_2(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ l1_orders_2(X1)
| ~ v2_orders_2(X1)
| v3_struct_0(X1)
| ! [X2] :
( ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ( v1_waybel34(X2,X0,X1)
<=> ! [X3] :
( ~ m1_subset_1(X3,u1_struct_0(X0))
| ! [X4] :
( ~ m1_subset_1(X4,u1_struct_0(X0))
| ~ r1_waybel_3(X0,X3,X4)
| r1_waybel_3(X1,k7_yellow_2(u1_struct_0(X0),X1,X2,X3),k7_yellow_2(u1_struct_0(X0),X1,X2,X4)) ) ) ) ) ) ),
inference(flattening,[],[f240]) ).
fof(f261,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v4_orders_2(X0)
| ! [X1] :
( ~ m1_yellow_0(X1,X0)
| ~ v4_yellow_0(X1,X0)
| ( v4_yellow_0(X1,X0)
& v4_orders_2(X1) ) ) ),
inference(ennf_transformation,[],[f56]) ).
fof(f262,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v4_orders_2(X0)
| ! [X1] :
( ~ m1_yellow_0(X1,X0)
| ~ v4_yellow_0(X1,X0)
| ( v4_yellow_0(X1,X0)
& v4_orders_2(X1) ) ) ),
inference(flattening,[],[f261]) ).
fof(f263,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v3_orders_2(X0)
| ! [X1] :
( ~ m1_yellow_0(X1,X0)
| ~ v4_yellow_0(X1,X0)
| ( v4_yellow_0(X1,X0)
& v3_orders_2(X1) ) ) ),
inference(ennf_transformation,[],[f54]) ).
fof(f264,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v3_orders_2(X0)
| ! [X1] :
( ~ m1_yellow_0(X1,X0)
| ~ v4_yellow_0(X1,X0)
| ( v4_yellow_0(X1,X0)
& v3_orders_2(X1) ) ) ),
inference(flattening,[],[f263]) ).
fof(f265,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v2_orders_2(X0)
| ! [X1] :
( ~ m1_yellow_0(X1,X0)
| ~ v4_yellow_0(X1,X0)
| ( v4_yellow_0(X1,X0)
& v2_orders_2(X1) ) ) ),
inference(ennf_transformation,[],[f52]) ).
fof(f266,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v2_orders_2(X0)
| ! [X1] :
( ~ m1_yellow_0(X1,X0)
| ~ v4_yellow_0(X1,X0)
| ( v4_yellow_0(X1,X0)
& v2_orders_2(X1) ) ) ),
inference(flattening,[],[f265]) ).
fof(f268,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ! [X1] :
( ~ m1_yellow_0(X1,X0)
| l1_orders_2(X1) ) ),
inference(ennf_transformation,[],[f79]) ).
fof(f285,plain,
! [X0,X1,X2] :
( ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| v3_struct_0(X1)
| ~ l1_orders_2(X0)
| v3_struct_0(X0)
| ( m2_relset_1(k2_waybel_1(X0,X1,X2),u1_struct_0(X0),u1_struct_0(k2_yellow_2(X0,X1,X2)))
& v1_funct_2(k2_waybel_1(X0,X1,X2),u1_struct_0(X0),u1_struct_0(k2_yellow_2(X0,X1,X2)))
& v1_funct_1(k2_waybel_1(X0,X1,X2)) ) ),
inference(ennf_transformation,[],[f68]) ).
fof(f286,plain,
! [X0,X1,X2] :
( ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| v3_struct_0(X1)
| ~ l1_orders_2(X0)
| v3_struct_0(X0)
| ( m2_relset_1(k2_waybel_1(X0,X1,X2),u1_struct_0(X0),u1_struct_0(k2_yellow_2(X0,X1,X2)))
& v1_funct_2(k2_waybel_1(X0,X1,X2),u1_struct_0(X0),u1_struct_0(k2_yellow_2(X0,X1,X2)))
& v1_funct_1(k2_waybel_1(X0,X1,X2)) ) ),
inference(flattening,[],[f285]) ).
fof(f289,plain,
! [X0,X1] :
( ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v6_waybel_1(X1,X0)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ( v3_lattice3(k2_yellow_2(X0,X0,X1))
& v2_lattice3(k2_yellow_2(X0,X0,X1))
& v1_lattice3(k2_yellow_2(X0,X0,X1))
& v25_waybel_0(k2_yellow_2(X0,X0,X1))
& v24_waybel_0(k2_yellow_2(X0,X0,X1))
& v4_yellow_0(k2_yellow_2(X0,X0,X1),X0)
& v3_yellow_0(k2_yellow_2(X0,X0,X1))
& v2_yellow_0(k2_yellow_2(X0,X0,X1))
& v1_yellow_0(k2_yellow_2(X0,X0,X1))
& v4_orders_2(k2_yellow_2(X0,X0,X1))
& v3_orders_2(k2_yellow_2(X0,X0,X1))
& v2_orders_2(k2_yellow_2(X0,X0,X1))
& v1_orders_2(k2_yellow_2(X0,X0,X1))
& ~ v3_struct_0(k2_yellow_2(X0,X0,X1)) ) ),
inference(ennf_transformation,[],[f90]) ).
fof(f290,plain,
! [X0,X1] :
( ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v6_waybel_1(X1,X0)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ( v3_lattice3(k2_yellow_2(X0,X0,X1))
& v2_lattice3(k2_yellow_2(X0,X0,X1))
& v1_lattice3(k2_yellow_2(X0,X0,X1))
& v25_waybel_0(k2_yellow_2(X0,X0,X1))
& v24_waybel_0(k2_yellow_2(X0,X0,X1))
& v4_yellow_0(k2_yellow_2(X0,X0,X1),X0)
& v3_yellow_0(k2_yellow_2(X0,X0,X1))
& v2_yellow_0(k2_yellow_2(X0,X0,X1))
& v1_yellow_0(k2_yellow_2(X0,X0,X1))
& v4_orders_2(k2_yellow_2(X0,X0,X1))
& v3_orders_2(k2_yellow_2(X0,X0,X1))
& v2_orders_2(k2_yellow_2(X0,X0,X1))
& v1_orders_2(k2_yellow_2(X0,X0,X1))
& ~ v3_struct_0(k2_yellow_2(X0,X0,X1)) ) ),
inference(flattening,[],[f289]) ).
fof(f302,plain,
! [X0] :
( ~ l1_orders_2(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ l1_orders_2(X1)
| v3_struct_0(X1)
| ! [X2] :
( ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ! [X3] :
( ~ m1_subset_1(X3,u1_struct_0(k2_yellow_2(X0,X1,X2)))
| k7_yellow_2(u1_struct_0(k2_yellow_2(X0,X1,X2)),X1,k3_waybel_1(X0,X1,X2),X3) = X3 ) ) ) ),
inference(ennf_transformation,[],[f152]) ).
fof(f303,plain,
! [X0] :
( ~ l1_orders_2(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ l1_orders_2(X1)
| v3_struct_0(X1)
| ! [X2] :
( ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ! [X3] :
( ~ m1_subset_1(X3,u1_struct_0(k2_yellow_2(X0,X1,X2)))
| k7_yellow_2(u1_struct_0(k2_yellow_2(X0,X1,X2)),X1,k3_waybel_1(X0,X1,X2),X3) = X3 ) ) ) ),
inference(flattening,[],[f302]) ).
fof(f306,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ! [X1] :
( ~ l1_orders_2(X1)
| ~ v3_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ! [X2] :
( ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v17_waybel_0(X2,X0,X1)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ v22_waybel_0(X2,X0,X1)
| v1_waybel34(k1_waybel34(X0,X1,X2),X1,X0) ) ) ),
inference(ennf_transformation,[],[f148]) ).
fof(f307,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ! [X1] :
( ~ l1_orders_2(X1)
| ~ v3_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ! [X2] :
( ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v17_waybel_0(X2,X0,X1)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ v22_waybel_0(X2,X0,X1)
| v1_waybel34(k1_waybel34(X0,X1,X2),X1,X0) ) ) ),
inference(flattening,[],[f306]) ).
fof(f345,plain,
! [X0,X1,X2] :
( ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| v3_struct_0(X1)
| ~ l1_orders_2(X0)
| v3_struct_0(X0)
| ( m2_relset_1(k3_waybel_1(X0,X1,X2),u1_struct_0(k2_yellow_2(X0,X1,X2)),u1_struct_0(X1))
& v1_funct_2(k3_waybel_1(X0,X1,X2),u1_struct_0(k2_yellow_2(X0,X1,X2)),u1_struct_0(X1))
& v1_funct_1(k3_waybel_1(X0,X1,X2)) ) ),
inference(ennf_transformation,[],[f71]) ).
fof(f346,plain,
! [X0,X1,X2] :
( ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| v3_struct_0(X1)
| ~ l1_orders_2(X0)
| v3_struct_0(X0)
| ( m2_relset_1(k3_waybel_1(X0,X1,X2),u1_struct_0(k2_yellow_2(X0,X1,X2)),u1_struct_0(X1))
& v1_funct_2(k3_waybel_1(X0,X1,X2),u1_struct_0(k2_yellow_2(X0,X1,X2)),u1_struct_0(X1))
& v1_funct_1(k3_waybel_1(X0,X1,X2)) ) ),
inference(flattening,[],[f345]) ).
fof(f349,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ! [X1] :
( ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v8_waybel_1(X1,X0)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| ( k2_waybel34(X0,k2_yellow_2(X0,X0,X1),k3_waybel_1(X0,X0,X1)) = k2_waybel_1(X0,X0,X1)
& k1_waybel34(X0,k2_yellow_2(X0,X0,X1),k2_waybel_1(X0,X0,X1)) = k3_waybel_1(X0,X0,X1)
& v18_waybel_0(k3_waybel_1(X0,X0,X1),k2_yellow_2(X0,X0,X1),X0)
& v17_waybel_0(k2_waybel_1(X0,X0,X1),X0,k2_yellow_2(X0,X0,X1)) ) ) ),
inference(ennf_transformation,[],[f150]) ).
fof(f350,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ! [X1] :
( ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v8_waybel_1(X1,X0)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| ( k2_waybel34(X0,k2_yellow_2(X0,X0,X1),k3_waybel_1(X0,X0,X1)) = k2_waybel_1(X0,X0,X1)
& k1_waybel34(X0,k2_yellow_2(X0,X0,X1),k2_waybel_1(X0,X0,X1)) = k3_waybel_1(X0,X0,X1)
& v18_waybel_0(k3_waybel_1(X0,X0,X1),k2_yellow_2(X0,X0,X1),X0)
& v17_waybel_0(k2_waybel_1(X0,X0,X1),X0,k2_yellow_2(X0,X0,X1)) ) ) ),
inference(flattening,[],[f349]) ).
fof(f351,plain,
! [X0,X1,X2] :
( ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ( m2_relset_1(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0))
& v1_funct_2(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0))
& v1_funct_1(k1_waybel34(X0,X1,X2)) ) ),
inference(ennf_transformation,[],[f64]) ).
fof(f352,plain,
! [X0,X1,X2] :
( ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ( m2_relset_1(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0))
& v1_funct_2(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0))
& v1_funct_1(k1_waybel34(X0,X1,X2)) ) ),
inference(flattening,[],[f351]) ).
fof(f371,plain,
! [X0,X1,X2] :
( ~ m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ( m2_relset_1(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_2(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_1(k2_waybel34(X0,X1,X2)) ) ),
inference(ennf_transformation,[],[f67]) ).
fof(f372,plain,
! [X0,X1,X2] :
( ~ m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ( m2_relset_1(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_2(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_1(k2_waybel34(X0,X1,X2)) ) ),
inference(flattening,[],[f371]) ).
fof(f395,plain,
? [X0] :
( l1_orders_2(X0)
& v3_lattice3(X0)
& v2_lattice3(X0)
& v1_lattice3(X0)
& v4_orders_2(X0)
& v3_orders_2(X0)
& v2_orders_2(X0)
& ? [X1] :
( m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
& v8_waybel_1(X1,X0)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v1_funct_1(X1)
& v22_waybel_0(X1,X0,X0)
& ? [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
& ? [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
& ? [X4] :
( m1_subset_1(X4,u1_struct_0(k2_yellow_2(X0,X0,X1)))
& ? [X5] :
( m1_subset_1(X5,u1_struct_0(k2_yellow_2(X0,X0,X1)))
& X5 = X3
& X4 = X2
& ( r1_waybel_3(X0,X2,X3)
| r1_waybel_3(k2_yellow_2(X0,X0,X1),X4,X5) )
& ( ~ r1_waybel_3(X0,X2,X3)
| ~ r1_waybel_3(k2_yellow_2(X0,X0,X1),X4,X5) ) ) ) ) ) ) ),
inference(nnf_transformation,[],[f210]) ).
fof(f396,plain,
? [X0] :
( l1_orders_2(X0)
& v3_lattice3(X0)
& v2_lattice3(X0)
& v1_lattice3(X0)
& v4_orders_2(X0)
& v3_orders_2(X0)
& v2_orders_2(X0)
& ? [X1] :
( m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
& v8_waybel_1(X1,X0)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v1_funct_1(X1)
& v22_waybel_0(X1,X0,X0)
& ? [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
& ? [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
& ? [X4] :
( m1_subset_1(X4,u1_struct_0(k2_yellow_2(X0,X0,X1)))
& ? [X5] :
( m1_subset_1(X5,u1_struct_0(k2_yellow_2(X0,X0,X1)))
& X5 = X3
& X4 = X2
& ( r1_waybel_3(X0,X2,X3)
| r1_waybel_3(k2_yellow_2(X0,X0,X1),X4,X5) )
& ( ~ r1_waybel_3(X0,X2,X3)
| ~ r1_waybel_3(k2_yellow_2(X0,X0,X1),X4,X5) ) ) ) ) ) ) ),
inference(flattening,[],[f395]) ).
fof(f397,plain,
( l1_orders_2(sK6)
& v3_lattice3(sK6)
& v2_lattice3(sK6)
& v1_lattice3(sK6)
& v4_orders_2(sK6)
& v3_orders_2(sK6)
& v2_orders_2(sK6)
& m2_relset_1(sK7,u1_struct_0(sK6),u1_struct_0(sK6))
& v8_waybel_1(sK7,sK6)
& v1_funct_2(sK7,u1_struct_0(sK6),u1_struct_0(sK6))
& v1_funct_1(sK7)
& v22_waybel_0(sK7,sK6,sK6)
& m1_subset_1(sK8,u1_struct_0(sK6))
& m1_subset_1(sK9,u1_struct_0(sK6))
& m1_subset_1(sK10,u1_struct_0(k2_yellow_2(sK6,sK6,sK7)))
& m1_subset_1(sK11,u1_struct_0(k2_yellow_2(sK6,sK6,sK7)))
& sK9 = sK11
& sK8 = sK10
& ( r1_waybel_3(sK6,sK8,sK9)
| r1_waybel_3(k2_yellow_2(sK6,sK6,sK7),sK10,sK11) )
& ( ~ r1_waybel_3(sK6,sK8,sK9)
| ~ r1_waybel_3(k2_yellow_2(sK6,sK6,sK7),sK10,sK11) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6,sK7,sK8,sK9,sK10,sK11]),skolemize(X0,sK6),skolemize(X1,sK7),skolemize(X2,sK8),skolemize(X3,sK9),skolemize(X4,sK10),skolemize(X5,sK11)],[f396]) ).
fof(f401,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ! [X1] :
( ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v8_waybel_1(X1,X0)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| ( ( ~ v22_waybel_0(X1,X0,X0)
| v22_waybel_0(k2_waybel_1(X0,X0,X1),X0,k2_yellow_2(X0,X0,X1)) )
& ( ~ v22_waybel_0(k2_waybel_1(X0,X0,X1),X0,k2_yellow_2(X0,X0,X1))
| v22_waybel_0(X1,X0,X0) ) ) ) ),
inference(nnf_transformation,[],[f229]) ).
fof(f403,plain,
! [X0,X1,X2] :
( ( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) )
& ( ~ m1_relset_1(X2,X0,X1)
| m2_relset_1(X2,X0,X1) ) ),
inference(nnf_transformation,[],[f145]) ).
fof(f406,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v2_orders_2(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ l1_orders_2(X1)
| ~ v2_orders_2(X1)
| v3_struct_0(X1)
| ! [X2] :
( ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ( ( ~ v1_waybel34(X2,X0,X1)
| ! [X3] :
( ~ m1_subset_1(X3,u1_struct_0(X0))
| ! [X4] :
( ~ m1_subset_1(X4,u1_struct_0(X0))
| ~ r1_waybel_3(X0,X3,X4)
| r1_waybel_3(X1,k7_yellow_2(u1_struct_0(X0),X1,X2,X3),k7_yellow_2(u1_struct_0(X0),X1,X2,X4)) ) ) )
& ( ? [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
& ? [X4] :
( m1_subset_1(X4,u1_struct_0(X0))
& r1_waybel_3(X0,X3,X4)
& ~ r1_waybel_3(X1,k7_yellow_2(u1_struct_0(X0),X1,X2,X3),k7_yellow_2(u1_struct_0(X0),X1,X2,X4)) ) )
| v1_waybel34(X2,X0,X1) ) ) ) ) ),
inference(nnf_transformation,[],[f241]) ).
fof(f407,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v2_orders_2(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ l1_orders_2(X1)
| ~ v2_orders_2(X1)
| v3_struct_0(X1)
| ! [X2] :
( ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ( ( ~ v1_waybel34(X2,X0,X1)
| ! [X5] :
( ~ m1_subset_1(X5,u1_struct_0(X0))
| ! [X6] :
( ~ m1_subset_1(X6,u1_struct_0(X0))
| ~ r1_waybel_3(X0,X5,X6)
| r1_waybel_3(X1,k7_yellow_2(u1_struct_0(X0),X1,X2,X5),k7_yellow_2(u1_struct_0(X0),X1,X2,X6)) ) ) )
& ( ? [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
& ? [X4] :
( m1_subset_1(X4,u1_struct_0(X0))
& r1_waybel_3(X0,X3,X4)
& ~ r1_waybel_3(X1,k7_yellow_2(u1_struct_0(X0),X1,X2,X3),k7_yellow_2(u1_struct_0(X0),X1,X2,X4)) ) )
| v1_waybel34(X2,X0,X1) ) ) ) ) ),
inference(rectify,[],[f406]) ).
fof(f408,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v2_orders_2(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ l1_orders_2(X1)
| ~ v2_orders_2(X1)
| v3_struct_0(X1)
| ! [X2] :
( ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ( ( ~ v1_waybel34(X2,X0,X1)
| ! [X5] :
( ~ m1_subset_1(X5,u1_struct_0(X0))
| ! [X6] :
( ~ m1_subset_1(X6,u1_struct_0(X0))
| ~ r1_waybel_3(X0,X5,X6)
| r1_waybel_3(X1,k7_yellow_2(u1_struct_0(X0),X1,X2,X5),k7_yellow_2(u1_struct_0(X0),X1,X2,X6)) ) ) )
& ( ( m1_subset_1(sK18(X0,X1,X2),u1_struct_0(X0))
& m1_subset_1(sK19(X0,X1,X2),u1_struct_0(X0))
& r1_waybel_3(X0,sK18(X0,X1,X2),sK19(X0,X1,X2))
& ~ r1_waybel_3(X1,k7_yellow_2(u1_struct_0(X0),X1,X2,sK18(X0,X1,X2)),k7_yellow_2(u1_struct_0(X0),X1,X2,sK19(X0,X1,X2))) )
| v1_waybel34(X2,X0,X1) ) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18,sK19]),skolemize(X3,sK18(X0,X1,X2)),skolemize(X4,sK19(X0,X1,X2))],[f407]) ).
fof(f440,plain,
l1_orders_2(sK6),
inference(cnf_transformation,[],[f397]) ).
fof(f441,plain,
v3_lattice3(sK6),
inference(cnf_transformation,[],[f397]) ).
fof(f442,plain,
v2_lattice3(sK6),
inference(cnf_transformation,[],[f397]) ).
fof(f443,plain,
v1_lattice3(sK6),
inference(cnf_transformation,[],[f397]) ).
fof(f444,plain,
v4_orders_2(sK6),
inference(cnf_transformation,[],[f397]) ).
fof(f445,plain,
v3_orders_2(sK6),
inference(cnf_transformation,[],[f397]) ).
fof(f446,plain,
v2_orders_2(sK6),
inference(cnf_transformation,[],[f397]) ).
fof(f447,plain,
m2_relset_1(sK7,u1_struct_0(sK6),u1_struct_0(sK6)),
inference(cnf_transformation,[],[f397]) ).
fof(f448,plain,
v8_waybel_1(sK7,sK6),
inference(cnf_transformation,[],[f397]) ).
fof(f449,plain,
v1_funct_2(sK7,u1_struct_0(sK6),u1_struct_0(sK6)),
inference(cnf_transformation,[],[f397]) ).
fof(f450,plain,
v1_funct_1(sK7),
inference(cnf_transformation,[],[f397]) ).
fof(f451,plain,
v22_waybel_0(sK7,sK6,sK6),
inference(cnf_transformation,[],[f397]) ).
fof(f452,plain,
m1_subset_1(sK8,u1_struct_0(sK6)),
inference(cnf_transformation,[],[f397]) ).
fof(f453,plain,
m1_subset_1(sK9,u1_struct_0(sK6)),
inference(cnf_transformation,[],[f397]) ).
fof(f454,plain,
m1_subset_1(sK10,u1_struct_0(k2_yellow_2(sK6,sK6,sK7))),
inference(cnf_transformation,[],[f397]) ).
fof(f455,plain,
m1_subset_1(sK11,u1_struct_0(k2_yellow_2(sK6,sK6,sK7))),
inference(cnf_transformation,[],[f397]) ).
fof(f456,plain,
sK9 = sK11,
inference(cnf_transformation,[],[f397]) ).
fof(f457,plain,
sK8 = sK10,
inference(cnf_transformation,[],[f397]) ).
fof(f458,plain,
( r1_waybel_3(sK6,sK8,sK9)
| r1_waybel_3(k2_yellow_2(sK6,sK6,sK7),sK10,sK11) ),
inference(cnf_transformation,[],[f397]) ).
fof(f459,plain,
( ~ r1_waybel_3(sK6,sK8,sK9)
| ~ r1_waybel_3(k2_yellow_2(sK6,sK6,sK7),sK10,sK11) ),
inference(cnf_transformation,[],[f397]) ).
fof(f466,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| v3_struct_0(X1)
| ~ l1_orders_2(X0)
| v3_struct_0(X0)
| ~ v3_struct_0(k2_yellow_2(X0,X1,X2)) ),
inference(cnf_transformation,[],[f216]) ).
fof(f467,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| v3_struct_0(X1)
| ~ l1_orders_2(X0)
| v3_struct_0(X0)
| m1_yellow_0(k2_yellow_2(X0,X1,X2),X1) ),
inference(cnf_transformation,[],[f218]) ).
fof(f468,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| v3_struct_0(X1)
| ~ l1_orders_2(X0)
| v3_struct_0(X0)
| v4_yellow_0(k2_yellow_2(X0,X1,X2),X1) ),
inference(cnf_transformation,[],[f218]) ).
fof(f486,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| v3_struct_0(X0)
| v2_lattice3(X0) ),
inference(cnf_transformation,[],[f220]) ).
fof(f487,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| v3_struct_0(X0)
| v1_lattice3(X0) ),
inference(cnf_transformation,[],[f220]) ).
fof(f489,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v3_struct_0(X0) ),
inference(cnf_transformation,[],[f222]) ).
fof(f490,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v3_struct_0(X0) ),
inference(cnf_transformation,[],[f224]) ).
fof(f493,plain,
! [X0,X1] :
( ~ l1_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| v3_struct_0(X0)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| ~ v8_waybel_1(X1,X0)
| v8_yellow_0(k2_yellow_2(X0,X0,X1),X0) ),
inference(cnf_transformation,[],[f227]) ).
fof(f495,plain,
! [X0,X1] :
( ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v8_waybel_1(X1,X0)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| ~ v22_waybel_0(X1,X0,X0)
| v22_waybel_0(k2_waybel_1(X0,X0,X1),X0,k2_yellow_2(X0,X0,X1)) ),
inference(cnf_transformation,[],[f401]) ).
fof(f512,plain,
! [X0,X1] :
( ~ l1_orders_2(X0)
| v3_struct_0(X0)
| ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v8_waybel_1(X1,X0)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| v6_waybel_1(X1,X0) ),
inference(cnf_transformation,[],[f235]) ).
fof(f516,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f403]) ).
fof(f523,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ m1_yellow_0(X1,X0)
| ~ v8_yellow_0(X1,X0)
| ~ v4_yellow_0(X1,X0)
| v3_struct_0(X1)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ m1_subset_1(X4,u1_struct_0(X1))
| ~ m1_subset_1(X5,u1_struct_0(X1))
| ~ r1_waybel_3(X0,X2,X3)
| X3 != X5
| X2 != X4
| r1_waybel_3(X1,X4,X5) ),
inference(cnf_transformation,[],[f239]) ).
fof(f524,plain,
! [X2,X0,X1,X6,X5] :
( ~ l1_orders_2(X0)
| ~ v2_orders_2(X0)
| v3_struct_0(X0)
| ~ l1_orders_2(X1)
| ~ v2_orders_2(X1)
| v3_struct_0(X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ v1_waybel34(X2,X0,X1)
| ~ m1_subset_1(X5,u1_struct_0(X0))
| ~ m1_subset_1(X6,u1_struct_0(X0))
| ~ r1_waybel_3(X0,X5,X6)
| r1_waybel_3(X1,k7_yellow_2(u1_struct_0(X0),X1,X2,X5),k7_yellow_2(u1_struct_0(X0),X1,X2,X6)) ),
inference(cnf_transformation,[],[f408]) ).
fof(f560,plain,
! [X0,X1] :
( ~ l1_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ m1_yellow_0(X1,X0)
| ~ v4_yellow_0(X1,X0)
| v4_orders_2(X1) ),
inference(cnf_transformation,[],[f262]) ).
fof(f562,plain,
! [X0,X1] :
( ~ l1_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ m1_yellow_0(X1,X0)
| ~ v4_yellow_0(X1,X0)
| v3_orders_2(X1) ),
inference(cnf_transformation,[],[f264]) ).
fof(f564,plain,
! [X0,X1] :
( ~ l1_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ m1_yellow_0(X1,X0)
| ~ v4_yellow_0(X1,X0)
| v2_orders_2(X1) ),
inference(cnf_transformation,[],[f266]) ).
fof(f566,plain,
! [X0,X1] :
( ~ l1_orders_2(X0)
| ~ m1_yellow_0(X1,X0)
| l1_orders_2(X1) ),
inference(cnf_transformation,[],[f268]) ).
fof(f597,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| v3_struct_0(X1)
| ~ l1_orders_2(X0)
| v3_struct_0(X0)
| m2_relset_1(k2_waybel_1(X0,X1,X2),u1_struct_0(X0),u1_struct_0(k2_yellow_2(X0,X1,X2))) ),
inference(cnf_transformation,[],[f286]) ).
fof(f598,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| v3_struct_0(X1)
| ~ l1_orders_2(X0)
| v3_struct_0(X0)
| v1_funct_2(k2_waybel_1(X0,X1,X2),u1_struct_0(X0),u1_struct_0(k2_yellow_2(X0,X1,X2))) ),
inference(cnf_transformation,[],[f286]) ).
fof(f599,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| v3_struct_0(X1)
| ~ l1_orders_2(X0)
| v3_struct_0(X0)
| v1_funct_1(k2_waybel_1(X0,X1,X2)) ),
inference(cnf_transformation,[],[f286]) ).
fof(f625,plain,
! [X0,X1] :
( ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v6_waybel_1(X1,X0)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| sP0(X1,X0) ),
inference(cnf_transformation,[],[f384]) ).
fof(f652,plain,
! [X2,X3,X0,X1] :
( ~ l1_orders_2(X0)
| v3_struct_0(X0)
| ~ l1_orders_2(X1)
| v3_struct_0(X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ m1_subset_1(X3,u1_struct_0(k2_yellow_2(X0,X1,X2)))
| k7_yellow_2(u1_struct_0(k2_yellow_2(X0,X1,X2)),X1,k3_waybel_1(X0,X1,X2),X3) = X3 ),
inference(cnf_transformation,[],[f303]) ).
fof(f654,plain,
! [X2,X0,X1] :
( ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ l1_orders_2(X1)
| ~ v3_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v17_waybel_0(X2,X0,X1)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ v22_waybel_0(X2,X0,X1)
| v1_waybel34(k1_waybel34(X0,X1,X2),X1,X0) ),
inference(cnf_transformation,[],[f307]) ).
fof(f779,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| v3_struct_0(X1)
| ~ l1_orders_2(X0)
| v3_struct_0(X0)
| m2_relset_1(k3_waybel_1(X0,X1,X2),u1_struct_0(k2_yellow_2(X0,X1,X2)),u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f346]) ).
fof(f780,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| v3_struct_0(X1)
| ~ l1_orders_2(X0)
| v3_struct_0(X0)
| v1_funct_2(k3_waybel_1(X0,X1,X2),u1_struct_0(k2_yellow_2(X0,X1,X2)),u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f346]) ).
fof(f781,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| v3_struct_0(X1)
| ~ l1_orders_2(X0)
| v3_struct_0(X0)
| v1_funct_1(k3_waybel_1(X0,X1,X2)) ),
inference(cnf_transformation,[],[f346]) ).
fof(f783,plain,
! [X0,X1] :
( ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v8_waybel_1(X1,X0)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| k2_waybel_1(X0,X0,X1) = k2_waybel34(X0,k2_yellow_2(X0,X0,X1),k3_waybel_1(X0,X0,X1)) ),
inference(cnf_transformation,[],[f350]) ).
fof(f784,plain,
! [X0,X1] :
( ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v8_waybel_1(X1,X0)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| k3_waybel_1(X0,X0,X1) = k1_waybel34(X0,k2_yellow_2(X0,X0,X1),k2_waybel_1(X0,X0,X1)) ),
inference(cnf_transformation,[],[f350]) ).
fof(f786,plain,
! [X0,X1] :
( ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v8_waybel_1(X1,X0)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| v17_waybel_0(k2_waybel_1(X0,X0,X1),X0,k2_yellow_2(X0,X0,X1)) ),
inference(cnf_transformation,[],[f350]) ).
fof(f788,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| v1_funct_2(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f352]) ).
fof(f855,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| m2_relset_1(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f372]) ).
fof(f879,plain,
( ~ r1_waybel_3(sK6,sK10,sK11)
| ~ r1_waybel_3(k2_yellow_2(sK6,sK6,sK7),sK10,sK11) ),
inference(definition_unfolding,[],[f459,f457,f456]) ).
fof(f880,plain,
( r1_waybel_3(sK6,sK10,sK11)
| r1_waybel_3(k2_yellow_2(sK6,sK6,sK7),sK10,sK11) ),
inference(definition_unfolding,[],[f458,f457,f456]) ).
fof(f881,plain,
m1_subset_1(sK11,u1_struct_0(sK6)),
inference(definition_unfolding,[],[f453,f456]) ).
fof(f882,plain,
m1_subset_1(sK10,u1_struct_0(sK6)),
inference(definition_unfolding,[],[f452,f457]) ).
fof(f883,plain,
! [X3,X0,X1,X4,X5] :
( ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ m1_yellow_0(X1,X0)
| ~ v8_yellow_0(X1,X0)
| ~ v4_yellow_0(X1,X0)
| v3_struct_0(X1)
| ~ m1_subset_1(X4,u1_struct_0(X0))
| ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ m1_subset_1(X4,u1_struct_0(X1))
| ~ m1_subset_1(X5,u1_struct_0(X1))
| ~ r1_waybel_3(X0,X4,X3)
| X3 != X5
| r1_waybel_3(X1,X4,X5) ),
inference(equality_resolution,[],[f523]) ).
fof(f884,plain,
! [X0,X1,X4,X5] :
( ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ m1_yellow_0(X1,X0)
| ~ v8_yellow_0(X1,X0)
| ~ v4_yellow_0(X1,X0)
| v3_struct_0(X1)
| ~ m1_subset_1(X4,u1_struct_0(X0))
| ~ m1_subset_1(X5,u1_struct_0(X0))
| ~ m1_subset_1(X4,u1_struct_0(X1))
| ~ m1_subset_1(X5,u1_struct_0(X1))
| ~ r1_waybel_3(X0,X4,X5)
| r1_waybel_3(X1,X4,X5) ),
inference(equality_resolution,[],[f883]) ).
tcf(c_49,negated_conjecture,
( ~ r1_waybel_3(sK6,sK10,sK11)
| ~ r1_waybel_3(k2_yellow_2(sK6,sK6,sK7),sK10,sK11) ),
inference(cnf_transformation,[],[f879]) ).
tcf(c_50,negated_conjecture,
( r1_waybel_3(sK6,sK10,sK11)
| r1_waybel_3(k2_yellow_2(sK6,sK6,sK7),sK10,sK11) ),
inference(cnf_transformation,[],[f880]) ).
tcf(c_51,negated_conjecture,
m1_subset_1(sK11,u1_struct_0(k2_yellow_2(sK6,sK6,sK7))),
inference(cnf_transformation,[],[f455]) ).
tcf(c_52,negated_conjecture,
m1_subset_1(sK10,u1_struct_0(k2_yellow_2(sK6,sK6,sK7))),
inference(cnf_transformation,[],[f454]) ).
tcf(c_53,negated_conjecture,
m1_subset_1(sK11,u1_struct_0(sK6)),
inference(cnf_transformation,[],[f881]) ).
tcf(c_54,negated_conjecture,
m1_subset_1(sK10,u1_struct_0(sK6)),
inference(cnf_transformation,[],[f882]) ).
tcf(c_55,negated_conjecture,
v22_waybel_0(sK7,sK6,sK6),
inference(cnf_transformation,[],[f451]) ).
tcf(c_56,negated_conjecture,
v1_funct_1(sK7),
inference(cnf_transformation,[],[f450]) ).
tcf(c_57,negated_conjecture,
v1_funct_2(sK7,u1_struct_0(sK6),u1_struct_0(sK6)),
inference(cnf_transformation,[],[f449]) ).
tcf(c_58,negated_conjecture,
v8_waybel_1(sK7,sK6),
inference(cnf_transformation,[],[f448]) ).
tcf(c_59,negated_conjecture,
m2_relset_1(sK7,u1_struct_0(sK6),u1_struct_0(sK6)),
inference(cnf_transformation,[],[f447]) ).
tcf(c_60,negated_conjecture,
v2_orders_2(sK6),
inference(cnf_transformation,[],[f446]) ).
tcf(c_61,negated_conjecture,
v3_orders_2(sK6),
inference(cnf_transformation,[],[f445]) ).
tcf(c_62,negated_conjecture,
v4_orders_2(sK6),
inference(cnf_transformation,[],[f444]) ).
tcf(c_63,negated_conjecture,
v1_lattice3(sK6),
inference(cnf_transformation,[],[f443]) ).
tcf(c_64,negated_conjecture,
v2_lattice3(sK6),
inference(cnf_transformation,[],[f442]) ).
tcf(c_65,negated_conjecture,
v3_lattice3(sK6),
inference(cnf_transformation,[],[f441]) ).
tcf(c_66,negated_conjecture,
l1_orders_2(sK6),
inference(cnf_transformation,[],[f440]) ).
tcf(c_71,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X2)
| v3_struct_0(X1)
| ~ l1_orders_2(X2)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X0)
| ~ v3_struct_0(k2_yellow_2(X1,X2,X0))
| ~ m1_relset_1(X0,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(X2)) ),
inference(cnf_transformation,[],[f466]) ).
tcf(c_75,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X2)
| v3_struct_0(X1)
| v4_yellow_0(k2_yellow_2(X1,X2,X0),X2)
| ~ l1_orders_2(X2)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X0)
| ~ m1_relset_1(X0,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(X2)) ),
inference(cnf_transformation,[],[f468]) ).
tcf(c_76,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X2)
| v3_struct_0(X1)
| m1_yellow_0(k2_yellow_2(X1,X2,X0),X2)
| ~ l1_orders_2(X2)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X0)
| ~ m1_relset_1(X0,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(X2)) ),
inference(cnf_transformation,[],[f467]) ).
tcf(c_93,plain,
! [X0: $i] :
( v3_struct_0(X0)
| v1_lattice3(X0)
| ~ l1_orders_2(X0)
| ~ v3_lattice3(X0) ),
inference(cnf_transformation,[],[f487]) ).
tcf(c_94,plain,
! [X0: $i] :
( v3_struct_0(X0)
| v2_lattice3(X0)
| ~ l1_orders_2(X0)
| ~ v3_lattice3(X0) ),
inference(cnf_transformation,[],[f486]) ).
tcf(c_95,plain,
! [X0: $i] :
( ~ v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ v1_lattice3(X0) ),
inference(cnf_transformation,[],[f489]) ).
tcf(c_96,plain,
! [X0: $i] :
( ~ v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0) ),
inference(cnf_transformation,[],[f490]) ).
tcf(c_100,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X1)
| v8_yellow_0(k2_yellow_2(X1,X1,X0),X1)
| ~ l1_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ v1_funct_1(X0)
| ~ v8_waybel_1(X0,X1)
| ~ m2_relset_1(X0,u1_struct_0(X1),u1_struct_0(X1))
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f493]) ).
tcf(c_102,plain,
! [X0: $i,X1: $i] :
( v22_waybel_0(k2_waybel_1(X1,X1,X0),X1,k2_yellow_2(X1,X1,X0))
| ~ l1_orders_2(X1)
| ~ v3_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ v1_funct_1(X0)
| ~ v8_waybel_1(X0,X1)
| ~ v22_waybel_0(X0,X1,X1)
| ~ m2_relset_1(X0,u1_struct_0(X1),u1_struct_0(X1))
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f495]) ).
tcf(c_119,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X1)
| v6_waybel_1(X0,X1)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X0)
| ~ v8_waybel_1(X0,X1)
| ~ m1_relset_1(X0,u1_struct_0(X1),u1_struct_0(X1))
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f512]) ).
tcf(c_121,plain,
! [X0: $i,X1: $i,X2: $i] :
( m1_relset_1(X0,X1,X2)
| ~ m2_relset_1(X0,X1,X2) ),
inference(cnf_transformation,[],[f516]) ).
tcf(c_125,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( v3_struct_0(X3)
| r1_waybel_3(X3,X1,X2)
| ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ v8_yellow_0(X3,X0)
| ~ m1_yellow_0(X3,X0)
| ~ v4_yellow_0(X3,X0)
| ~ m1_subset_1(X2,u1_struct_0(X3))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X3))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ r1_waybel_3(X0,X1,X2) ),
inference(cnf_transformation,[],[f884]) ).
tcf(c_130,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( v3_struct_0(X2)
| v3_struct_0(X1)
| r1_waybel_3(X2,k7_yellow_2(u1_struct_0(X1),X2,X0,X3),k7_yellow_2(u1_struct_0(X1),X2,X0,X4))
| ~ l1_orders_2(X2)
| ~ l1_orders_2(X1)
| ~ v2_orders_2(X2)
| ~ v2_orders_2(X1)
| ~ v1_funct_1(X0)
| ~ m1_subset_1(X4,u1_struct_0(X1))
| ~ m1_subset_1(X3,u1_struct_0(X1))
| ~ v1_waybel34(X0,X1,X2)
| ~ r1_waybel_3(X1,X3,X4)
| ~ m2_relset_1(X0,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(X2)) ),
inference(cnf_transformation,[],[f524]) ).
tcf(c_161,plain,
! [X0: $i,X1: $i] :
( v4_orders_2(X0)
| ~ l1_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ m1_yellow_0(X0,X1)
| ~ v4_yellow_0(X0,X1) ),
inference(cnf_transformation,[],[f560]) ).
tcf(c_162,plain,
! [X0: $i,X1: $i] :
( v3_orders_2(X0)
| ~ l1_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ m1_yellow_0(X0,X1)
| ~ v4_yellow_0(X0,X1) ),
inference(cnf_transformation,[],[f562]) ).
tcf(c_163,plain,
! [X0: $i,X1: $i] :
( v2_orders_2(X0)
| ~ l1_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ m1_yellow_0(X0,X1)
| ~ v4_yellow_0(X0,X1) ),
inference(cnf_transformation,[],[f564]) ).
tcf(c_165,plain,
! [X0: $i,X1: $i] :
( l1_orders_2(X0)
| ~ l1_orders_2(X1)
| ~ m1_yellow_0(X0,X1) ),
inference(cnf_transformation,[],[f566]) ).
tcf(c_194,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X2)
| v3_struct_0(X1)
| v1_funct_1(k2_waybel_1(X1,X2,X0))
| ~ l1_orders_2(X2)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X0)
| ~ m1_relset_1(X0,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(X2)) ),
inference(cnf_transformation,[],[f599]) ).
tcf(c_195,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X2)
| v3_struct_0(X1)
| v1_funct_2(k2_waybel_1(X1,X2,X0),u1_struct_0(X1),u1_struct_0(k2_yellow_2(X1,X2,X0)))
| ~ l1_orders_2(X2)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X0)
| ~ m1_relset_1(X0,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(X2)) ),
inference(cnf_transformation,[],[f598]) ).
tcf(c_196,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X2)
| v3_struct_0(X1)
| m2_relset_1(k2_waybel_1(X1,X2,X0),u1_struct_0(X1),u1_struct_0(k2_yellow_2(X1,X2,X0)))
| ~ l1_orders_2(X2)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X0)
| ~ m1_relset_1(X0,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(X2)) ),
inference(cnf_transformation,[],[f597]) ).
tcf(c_222,plain,
! [X0: $i,X1: $i] :
( sP0(X0,X1)
| ~ l1_orders_2(X1)
| ~ v3_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ v1_funct_1(X0)
| ~ v6_waybel_1(X0,X1)
| ~ m1_relset_1(X0,u1_struct_0(X1),u1_struct_0(X1))
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f625]) ).
tcf(c_245,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( v3_struct_0(X2)
| v3_struct_0(X1)
| ( k7_yellow_2(u1_struct_0(k2_yellow_2(X1,X2,X3)),X2,k3_waybel_1(X1,X2,X3),X0) = X0 )
| ~ l1_orders_2(X2)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X3)
| ~ m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X2))
| ~ m1_subset_1(X0,u1_struct_0(k2_yellow_2(X1,X2,X3))) ),
inference(cnf_transformation,[],[f652]) ).
tcf(c_247,plain,
! [X0: $i,X1: $i,X2: $i] :
( v1_waybel34(k1_waybel34(X1,X2,X0),X2,X1)
| ~ l1_orders_2(X2)
| ~ l1_orders_2(X1)
| ~ v3_lattice3(X2)
| ~ v3_lattice3(X1)
| ~ v2_lattice3(X2)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X2)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X2)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X2)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X2)
| ~ v2_orders_2(X1)
| ~ v1_funct_1(X0)
| ~ v17_waybel_0(X0,X1,X2)
| ~ v22_waybel_0(X0,X1,X2)
| ~ m2_relset_1(X0,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(X2)) ),
inference(cnf_transformation,[],[f654]) ).
tcf(c_352,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X2)
| v3_struct_0(X1)
| v1_funct_1(k3_waybel_1(X1,X2,X0))
| ~ l1_orders_2(X2)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X0)
| ~ m1_relset_1(X0,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(X2)) ),
inference(cnf_transformation,[],[f781]) ).
tcf(c_353,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X2)
| v3_struct_0(X1)
| v1_funct_2(k3_waybel_1(X1,X2,X0),u1_struct_0(k2_yellow_2(X1,X2,X0)),u1_struct_0(X2))
| ~ l1_orders_2(X2)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X0)
| ~ m1_relset_1(X0,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(X2)) ),
inference(cnf_transformation,[],[f780]) ).
tcf(c_354,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X2)
| v3_struct_0(X1)
| m2_relset_1(k3_waybel_1(X1,X2,X0),u1_struct_0(k2_yellow_2(X1,X2,X0)),u1_struct_0(X2))
| ~ l1_orders_2(X2)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X0)
| ~ m1_relset_1(X0,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(X2)) ),
inference(cnf_transformation,[],[f779]) ).
tcf(c_356,plain,
! [X0: $i,X1: $i] :
( v17_waybel_0(k2_waybel_1(X1,X1,X0),X1,k2_yellow_2(X1,X1,X0))
| ~ l1_orders_2(X1)
| ~ v3_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ v1_funct_1(X0)
| ~ v8_waybel_1(X0,X1)
| ~ m2_relset_1(X0,u1_struct_0(X1),u1_struct_0(X1))
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f786]) ).
tcf(c_358,plain,
! [X0: $i,X1: $i] :
( ( k1_waybel34(X1,k2_yellow_2(X1,X1,X0),k2_waybel_1(X1,X1,X0)) = k3_waybel_1(X1,X1,X0) )
| ~ l1_orders_2(X1)
| ~ v3_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ v1_funct_1(X0)
| ~ v8_waybel_1(X0,X1)
| ~ m2_relset_1(X0,u1_struct_0(X1),u1_struct_0(X1))
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f784]) ).
tcf(c_359,plain,
! [X0: $i,X1: $i] :
( ( k2_waybel34(X1,k2_yellow_2(X1,X1,X0),k3_waybel_1(X1,X1,X0)) = k2_waybel_1(X1,X1,X0) )
| ~ l1_orders_2(X1)
| ~ v3_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ v1_funct_1(X0)
| ~ v8_waybel_1(X0,X1)
| ~ m2_relset_1(X0,u1_struct_0(X1),u1_struct_0(X1))
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f783]) ).
tcf(c_361,plain,
! [X0: $i,X1: $i,X2: $i] :
( v1_funct_2(k1_waybel34(X1,X2,X0),u1_struct_0(X2),u1_struct_0(X1))
| ~ l1_orders_2(X2)
| ~ l1_orders_2(X1)
| ~ v2_lattice3(X2)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X2)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X2)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X2)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X2)
| ~ v2_orders_2(X1)
| ~ v1_funct_1(X0)
| ~ m1_relset_1(X0,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(X2)) ),
inference(cnf_transformation,[],[f788]) ).
tcf(c_426,plain,
! [X0: $i,X1: $i,X2: $i] :
( m2_relset_1(k2_waybel34(X2,X1,X0),u1_struct_0(X2),u1_struct_0(X1))
| ~ l1_orders_2(X2)
| ~ l1_orders_2(X1)
| ~ v2_lattice3(X2)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X2)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X2)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X2)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X2)
| ~ v2_orders_2(X1)
| ~ v1_funct_1(X0)
| ~ m1_relset_1(X0,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(X2)) ),
inference(cnf_transformation,[],[f855]) ).
tcf(c_539,plain,
( ~ v3_struct_0(sK6)
| ~ l1_orders_2(sK6)
| ~ v2_lattice3(sK6) ),
inference(instantiation,[status(thm)],[c_96]) ).
tcf(c_784,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( v3_struct_0(X3)
| r1_waybel_3(X3,X1,X2)
| ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ r1_waybel_3(X0,X1,X2)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X3))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X3))
| ~ v4_yellow_0(X3,X0)
| ~ m1_yellow_0(X3,X0)
| ~ v8_yellow_0(X3,X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0) ),
inference(global_subsumption_just,[status(thm)],[c_125,c_96,c_93,c_125]) ).
tcf(c_785,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( v3_struct_0(X3)
| r1_waybel_3(X3,X1,X2)
| ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ v8_yellow_0(X3,X0)
| ~ m1_yellow_0(X3,X0)
| ~ v4_yellow_0(X3,X0)
| ~ m1_subset_1(X2,u1_struct_0(X3))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X3))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ r1_waybel_3(X0,X1,X2) ),
inference(renaming,[status(thm)],[c_784]) ).
tcf(c_16052,plain,
! [X0: $i,X1: $i] :
( ( k2_waybel34(X0,k2_yellow_2(X0,X0,X1),k3_waybel_1(X0,X0,X1)) = k2_waybel_1(X0,X0,X1) )
| ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ( X1 != sK7 )
| ( X0 != sK6 ) ),
inference(resolution_lifted,[status(thm)],[c_58,c_359]) ).
tcf(c_16053,plain,
( ( k2_waybel34(sK6,k2_yellow_2(sK6,sK6,sK7),k3_waybel_1(sK6,sK6,sK7)) = k2_waybel_1(sK6,sK6,sK7) )
| ~ l1_orders_2(sK6)
| ~ v3_lattice3(sK6)
| ~ v2_lattice3(sK6)
| ~ v1_lattice3(sK6)
| ~ v4_orders_2(sK6)
| ~ v3_orders_2(sK6)
| ~ v2_orders_2(sK6)
| ~ v1_funct_1(sK7)
| ~ m2_relset_1(sK7,u1_struct_0(sK6),u1_struct_0(sK6))
| ~ v1_funct_2(sK7,u1_struct_0(sK6),u1_struct_0(sK6)) ),
inference(unflattening,[status(thm)],[c_16052]) ).
tcf(c_16054,plain,
k2_waybel34(sK6,k2_yellow_2(sK6,sK6,sK7),k3_waybel_1(sK6,sK6,sK7)) = k2_waybel_1(sK6,sK6,sK7),
inference(global_subsumption_just,[status(thm)],[c_16053,c_66,c_65,c_64,c_63,c_62,c_61,c_60,c_56,c_59,c_57,c_16053]) ).
tcf(c_16059,plain,
! [X0: $i,X1: $i] :
( ( k1_waybel34(X0,k2_yellow_2(X0,X0,X1),k2_waybel_1(X0,X0,X1)) = k3_waybel_1(X0,X0,X1) )
| ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ( X1 != sK7 )
| ( X0 != sK6 ) ),
inference(resolution_lifted,[status(thm)],[c_58,c_358]) ).
tcf(c_16060,plain,
( ( k1_waybel34(sK6,k2_yellow_2(sK6,sK6,sK7),k2_waybel_1(sK6,sK6,sK7)) = k3_waybel_1(sK6,sK6,sK7) )
| ~ l1_orders_2(sK6)
| ~ v3_lattice3(sK6)
| ~ v2_lattice3(sK6)
| ~ v1_lattice3(sK6)
| ~ v4_orders_2(sK6)
| ~ v3_orders_2(sK6)
| ~ v2_orders_2(sK6)
| ~ v1_funct_1(sK7)
| ~ m2_relset_1(sK7,u1_struct_0(sK6),u1_struct_0(sK6))
| ~ v1_funct_2(sK7,u1_struct_0(sK6),u1_struct_0(sK6)) ),
inference(unflattening,[status(thm)],[c_16059]) ).
tcf(c_16061,plain,
k1_waybel34(sK6,k2_yellow_2(sK6,sK6,sK7),k2_waybel_1(sK6,sK6,sK7)) = k3_waybel_1(sK6,sK6,sK7),
inference(global_subsumption_just,[status(thm)],[c_16060,c_66,c_65,c_64,c_63,c_62,c_61,c_60,c_56,c_59,c_57,c_16060]) ).
tcf(c_16073,plain,
! [X0: $i,X1: $i] :
( v17_waybel_0(k2_waybel_1(X0,X0,X1),X0,k2_yellow_2(X0,X0,X1))
| ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ( X1 != sK7 )
| ( X0 != sK6 ) ),
inference(resolution_lifted,[status(thm)],[c_58,c_356]) ).
tcf(c_16074,plain,
( v17_waybel_0(k2_waybel_1(sK6,sK6,sK7),sK6,k2_yellow_2(sK6,sK6,sK7))
| ~ l1_orders_2(sK6)
| ~ v3_lattice3(sK6)
| ~ v2_lattice3(sK6)
| ~ v1_lattice3(sK6)
| ~ v4_orders_2(sK6)
| ~ v3_orders_2(sK6)
| ~ v2_orders_2(sK6)
| ~ v1_funct_1(sK7)
| ~ m2_relset_1(sK7,u1_struct_0(sK6),u1_struct_0(sK6))
| ~ v1_funct_2(sK7,u1_struct_0(sK6),u1_struct_0(sK6)) ),
inference(unflattening,[status(thm)],[c_16073]) ).
tcf(c_16075,plain,
v17_waybel_0(k2_waybel_1(sK6,sK6,sK7),sK6,k2_yellow_2(sK6,sK6,sK7)),
inference(global_subsumption_just,[status(thm)],[c_16074,c_66,c_65,c_64,c_63,c_62,c_61,c_60,c_56,c_59,c_57,c_16074]) ).
tcf(c_16080,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X0)
| v6_waybel_1(X1,X0)
| ~ l1_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ( X1 != sK7 )
| ( X0 != sK6 ) ),
inference(resolution_lifted,[status(thm)],[c_58,c_119]) ).
tcf(c_16081,plain,
( v3_struct_0(sK6)
| v6_waybel_1(sK7,sK6)
| ~ l1_orders_2(sK6)
| ~ v1_funct_1(sK7)
| ~ m1_relset_1(sK7,u1_struct_0(sK6),u1_struct_0(sK6))
| ~ v1_funct_2(sK7,u1_struct_0(sK6),u1_struct_0(sK6)) ),
inference(unflattening,[status(thm)],[c_16080]) ).
tcf(c_16082,plain,
( ~ m1_relset_1(sK7,u1_struct_0(sK6),u1_struct_0(sK6))
| v6_waybel_1(sK7,sK6) ),
inference(global_subsumption_just,[status(thm)],[c_16081,c_66,c_64,c_56,c_57,c_539,c_16081]) ).
tcf(c_16083,plain,
( v6_waybel_1(sK7,sK6)
| ~ m1_relset_1(sK7,u1_struct_0(sK6),u1_struct_0(sK6)) ),
inference(renaming,[status(thm)],[c_16082]) ).
tcf(c_16090,plain,
! [X0: $i,X1: $i] :
( v22_waybel_0(k2_waybel_1(X0,X0,X1),X0,k2_yellow_2(X0,X0,X1))
| ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ v22_waybel_0(X1,X0,X0)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ( X1 != sK7 )
| ( X0 != sK6 ) ),
inference(resolution_lifted,[status(thm)],[c_58,c_102]) ).
tcf(c_16091,plain,
( v22_waybel_0(k2_waybel_1(sK6,sK6,sK7),sK6,k2_yellow_2(sK6,sK6,sK7))
| ~ l1_orders_2(sK6)
| ~ v3_lattice3(sK6)
| ~ v2_lattice3(sK6)
| ~ v1_lattice3(sK6)
| ~ v4_orders_2(sK6)
| ~ v3_orders_2(sK6)
| ~ v2_orders_2(sK6)
| ~ v1_funct_1(sK7)
| ~ v22_waybel_0(sK7,sK6,sK6)
| ~ m2_relset_1(sK7,u1_struct_0(sK6),u1_struct_0(sK6))
| ~ v1_funct_2(sK7,u1_struct_0(sK6),u1_struct_0(sK6)) ),
inference(unflattening,[status(thm)],[c_16090]) ).
tcf(c_16092,plain,
v22_waybel_0(k2_waybel_1(sK6,sK6,sK7),sK6,k2_yellow_2(sK6,sK6,sK7)),
inference(global_subsumption_just,[status(thm)],[c_16091,c_66,c_65,c_64,c_63,c_62,c_61,c_60,c_56,c_55,c_59,c_57,c_16091]) ).
tcf(c_16097,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X0)
| v8_yellow_0(k2_yellow_2(X0,X0,X1),X0)
| ~ l1_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ( X1 != sK7 )
| ( X0 != sK6 ) ),
inference(resolution_lifted,[status(thm)],[c_58,c_100]) ).
tcf(c_16098,plain,
( v3_struct_0(sK6)
| v8_yellow_0(k2_yellow_2(sK6,sK6,sK7),sK6)
| ~ l1_orders_2(sK6)
| ~ v4_orders_2(sK6)
| ~ v3_orders_2(sK6)
| ~ v2_orders_2(sK6)
| ~ v1_funct_1(sK7)
| ~ m2_relset_1(sK7,u1_struct_0(sK6),u1_struct_0(sK6))
| ~ v1_funct_2(sK7,u1_struct_0(sK6),u1_struct_0(sK6)) ),
inference(unflattening,[status(thm)],[c_16097]) ).
tcf(c_16739,plain,
! [X0: $i,X1: $i] :
( sP0(X0,X1)
| ~ l1_orders_2(X1)
| ~ v3_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ v1_funct_1(X0)
| ~ m1_relset_1(sK7,u1_struct_0(sK6),u1_struct_0(sK6))
| ~ m1_relset_1(X0,u1_struct_0(X1),u1_struct_0(X1))
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(X1))
| ( X1 != sK6 )
| ( X0 != sK7 ) ),
inference(resolution_lifted,[status(thm)],[c_222,c_16083]) ).
tcf(c_16740,plain,
( sP0(sK7,sK6)
| ~ l1_orders_2(sK6)
| ~ v3_lattice3(sK6)
| ~ v2_lattice3(sK6)
| ~ v1_lattice3(sK6)
| ~ v4_orders_2(sK6)
| ~ v3_orders_2(sK6)
| ~ v2_orders_2(sK6)
| ~ v1_funct_1(sK7)
| ~ m1_relset_1(sK7,u1_struct_0(sK6),u1_struct_0(sK6))
| ~ v1_funct_2(sK7,u1_struct_0(sK6),u1_struct_0(sK6)) ),
inference(unflattening,[status(thm)],[c_16739]) ).
tcf(c_16741,plain,
( sP0(sK7,sK6)
| ~ m1_relset_1(sK7,u1_struct_0(sK6),u1_struct_0(sK6)) ),
inference(global_subsumption_just,[status(thm)],[c_16740,c_66,c_65,c_64,c_63,c_62,c_61,c_60,c_56,c_57,c_16740]) ).
tcf(c_50097,plain,
( ~ v3_struct_0(sK6)
| ~ v1_lattice3(sK6) ),
inference(superposition,[status(thm)],[c_66,c_95]) ).
tcf(c_50105,plain,
~ v3_struct_0(sK6),
inference(forward_subsumption_resolution,[status(thm)],[c_50097,c_63]) ).
tcf(c_50138,plain,
m1_relset_1(sK7,u1_struct_0(sK6),u1_struct_0(sK6)),
inference(superposition,[status(thm)],[c_59,c_121]) ).
tcf(c_50914,plain,
( v3_struct_0(sK6)
| ~ l1_orders_2(sK6)
| ~ v1_funct_1(sK7)
| ~ v3_struct_0(k2_yellow_2(sK6,sK6,sK7))
| ~ m1_relset_1(sK7,u1_struct_0(sK6),u1_struct_0(sK6)) ),
inference(superposition,[status(thm)],[c_57,c_71]) ).
tcf(c_50917,plain,
~ v3_struct_0(k2_yellow_2(sK6,sK6,sK7)),
inference(forward_subsumption_resolution,[status(thm)],[c_50914,c_50105,c_66,c_56,c_50138]) ).
tcf(c_51208,plain,
( v3_struct_0(sK6)
| v4_yellow_0(k2_yellow_2(sK6,sK6,sK7),sK6)
| ~ l1_orders_2(sK6)
| ~ v1_funct_1(sK7)
| ~ m1_relset_1(sK7,u1_struct_0(sK6),u1_struct_0(sK6)) ),
inference(superposition,[status(thm)],[c_57,c_75]) ).
tcf(c_51211,plain,
v4_yellow_0(k2_yellow_2(sK6,sK6,sK7),sK6),
inference(forward_subsumption_resolution,[status(thm)],[c_51208,c_50105,c_66,c_56,c_50138]) ).
tcf(c_51510,plain,
( v3_struct_0(sK6)
| m1_yellow_0(k2_yellow_2(sK6,sK6,sK7),sK6)
| ~ l1_orders_2(sK6)
| ~ v1_funct_1(sK7)
| ~ m1_relset_1(sK7,u1_struct_0(sK6),u1_struct_0(sK6)) ),
inference(superposition,[status(thm)],[c_57,c_76]) ).
tcf(c_51514,plain,
m1_yellow_0(k2_yellow_2(sK6,sK6,sK7),sK6),
inference(forward_subsumption_resolution,[status(thm)],[c_51510,c_50105,c_66,c_56,c_50138]) ).
tcf(c_51732,plain,
( l1_orders_2(k2_yellow_2(sK6,sK6,sK7))
| ~ l1_orders_2(sK6) ),
inference(superposition,[status(thm)],[c_51514,c_165]) ).
tcf(c_51733,plain,
l1_orders_2(k2_yellow_2(sK6,sK6,sK7)),
inference(forward_subsumption_resolution,[status(thm)],[c_51732,c_66]) ).
tcf(c_51738,plain,
( v3_struct_0(k2_yellow_2(sK6,sK6,sK7))
| v2_lattice3(k2_yellow_2(sK6,sK6,sK7))
| ~ v3_lattice3(k2_yellow_2(sK6,sK6,sK7)) ),
inference(superposition,[status(thm)],[c_51733,c_94]) ).
tcf(c_51739,plain,
( v3_struct_0(k2_yellow_2(sK6,sK6,sK7))
| v1_lattice3(k2_yellow_2(sK6,sK6,sK7))
| ~ v3_lattice3(k2_yellow_2(sK6,sK6,sK7)) ),
inference(superposition,[status(thm)],[c_51733,c_93]) ).
tcf(c_51743,plain,
( v1_lattice3(k2_yellow_2(sK6,sK6,sK7))
| ~ v3_lattice3(k2_yellow_2(sK6,sK6,sK7)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_51739,c_50917]) ).
tcf(c_51746,plain,
( v2_lattice3(k2_yellow_2(sK6,sK6,sK7))
| ~ v3_lattice3(k2_yellow_2(sK6,sK6,sK7)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_51738,c_50917]) ).
tcf(c_52044,plain,
( v4_orders_2(k2_yellow_2(sK6,sK6,sK7))
| ~ l1_orders_2(sK6)
| ~ v4_orders_2(sK6)
| ~ m1_yellow_0(k2_yellow_2(sK6,sK6,sK7),sK6) ),
inference(superposition,[status(thm)],[c_51211,c_161]) ).
tcf(c_52064,plain,
v4_orders_2(k2_yellow_2(sK6,sK6,sK7)),
inference(forward_subsumption_resolution,[status(thm)],[c_52044,c_66,c_62,c_51514]) ).
tcf(c_52092,plain,
( v3_orders_2(k2_yellow_2(sK6,sK6,sK7))
| ~ l1_orders_2(sK6)
| ~ v3_orders_2(sK6)
| ~ m1_yellow_0(k2_yellow_2(sK6,sK6,sK7),sK6) ),
inference(superposition,[status(thm)],[c_51211,c_162]) ).
tcf(c_52112,plain,
v3_orders_2(k2_yellow_2(sK6,sK6,sK7)),
inference(forward_subsumption_resolution,[status(thm)],[c_52092,c_66,c_61,c_51514]) ).
tcf(c_52140,plain,
( v2_orders_2(k2_yellow_2(sK6,sK6,sK7))
| ~ l1_orders_2(sK6)
| ~ v2_orders_2(sK6)
| ~ m1_yellow_0(k2_yellow_2(sK6,sK6,sK7),sK6) ),
inference(superposition,[status(thm)],[c_51211,c_163]) ).
tcf(c_52160,plain,
v2_orders_2(k2_yellow_2(sK6,sK6,sK7)),
inference(forward_subsumption_resolution,[status(thm)],[c_52140,c_66,c_60,c_51514]) ).
tcf(c_54916,plain,
( v3_struct_0(sK6)
| v1_funct_1(k2_waybel_1(sK6,sK6,sK7))
| ~ l1_orders_2(sK6)
| ~ v1_funct_1(sK7)
| ~ m1_relset_1(sK7,u1_struct_0(sK6),u1_struct_0(sK6)) ),
inference(superposition,[status(thm)],[c_57,c_194]) ).
tcf(c_54929,plain,
v1_funct_1(k2_waybel_1(sK6,sK6,sK7)),
inference(forward_subsumption_resolution,[status(thm)],[c_54916,c_50105,c_66,c_56,c_50138]) ).
tcf(c_55038,plain,
( v3_struct_0(sK6)
| v1_funct_1(k3_waybel_1(sK6,sK6,sK7))
| ~ l1_orders_2(sK6)
| ~ v1_funct_1(sK7)
| ~ m1_relset_1(sK7,u1_struct_0(sK6),u1_struct_0(sK6)) ),
inference(superposition,[status(thm)],[c_57,c_352]) ).
tcf(c_55051,plain,
v1_funct_1(k3_waybel_1(sK6,sK6,sK7)),
inference(forward_subsumption_resolution,[status(thm)],[c_55038,c_50105,c_66,c_56,c_50138]) ).
tcf(c_56358,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X1)
| v3_struct_0(X0)
| v1_funct_2(k2_waybel_1(X0,X1,sK7),u1_struct_0(X0),u1_struct_0(k2_yellow_2(X0,X1,sK7)))
| ~ v1_funct_1(sK7)
| ~ l1_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ m1_relset_1(sK7,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(sK7,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(instantiation,[status(thm)],[c_195]) ).
tcf(c_56359,plain,
( v3_struct_0(sK6)
| v1_funct_2(k2_waybel_1(sK6,sK6,sK7),u1_struct_0(sK6),u1_struct_0(k2_yellow_2(sK6,sK6,sK7)))
| ~ l1_orders_2(sK6)
| ~ v1_funct_1(sK7)
| ~ m1_relset_1(sK7,u1_struct_0(sK6),u1_struct_0(sK6))
| ~ v1_funct_2(sK7,u1_struct_0(sK6),u1_struct_0(sK6)) ),
inference(instantiation,[status(thm)],[c_56358]) ).
tcf(c_56506,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X1)
| v3_struct_0(X0)
| m2_relset_1(k2_waybel_1(X0,X1,sK7),u1_struct_0(X0),u1_struct_0(k2_yellow_2(X0,X1,sK7)))
| ~ v1_funct_1(sK7)
| ~ l1_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ m1_relset_1(sK7,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(sK7,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(instantiation,[status(thm)],[c_196]) ).
tcf(c_56507,plain,
( v3_struct_0(sK6)
| m2_relset_1(k2_waybel_1(sK6,sK6,sK7),u1_struct_0(sK6),u1_struct_0(k2_yellow_2(sK6,sK6,sK7)))
| ~ l1_orders_2(sK6)
| ~ v1_funct_1(sK7)
| ~ m1_relset_1(sK7,u1_struct_0(sK6),u1_struct_0(sK6))
| ~ v1_funct_2(sK7,u1_struct_0(sK6),u1_struct_0(sK6)) ),
inference(instantiation,[status(thm)],[c_56506]) ).
tcf(c_56908,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X1)
| v3_struct_0(X0)
| v1_funct_2(k3_waybel_1(X0,X1,sK7),u1_struct_0(k2_yellow_2(X0,X1,sK7)),u1_struct_0(X1))
| ~ v1_funct_1(sK7)
| ~ l1_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ m1_relset_1(sK7,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(sK7,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(instantiation,[status(thm)],[c_353]) ).
tcf(c_56909,plain,
( v3_struct_0(sK6)
| v1_funct_2(k3_waybel_1(sK6,sK6,sK7),u1_struct_0(k2_yellow_2(sK6,sK6,sK7)),u1_struct_0(sK6))
| ~ l1_orders_2(sK6)
| ~ v1_funct_1(sK7)
| ~ m1_relset_1(sK7,u1_struct_0(sK6),u1_struct_0(sK6))
| ~ v1_funct_2(sK7,u1_struct_0(sK6),u1_struct_0(sK6)) ),
inference(instantiation,[status(thm)],[c_56908]) ).
tcf(c_57013,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X1)
| v3_struct_0(X0)
| m2_relset_1(k3_waybel_1(X0,X1,sK7),u1_struct_0(k2_yellow_2(X0,X1,sK7)),u1_struct_0(X1))
| ~ v1_funct_1(sK7)
| ~ l1_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ m1_relset_1(sK7,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(sK7,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(instantiation,[status(thm)],[c_354]) ).
tcf(c_57014,plain,
( v3_struct_0(sK6)
| m2_relset_1(k3_waybel_1(sK6,sK6,sK7),u1_struct_0(k2_yellow_2(sK6,sK6,sK7)),u1_struct_0(sK6))
| ~ l1_orders_2(sK6)
| ~ v1_funct_1(sK7)
| ~ m1_relset_1(sK7,u1_struct_0(sK6),u1_struct_0(sK6))
| ~ v1_funct_2(sK7,u1_struct_0(sK6),u1_struct_0(sK6)) ),
inference(instantiation,[status(thm)],[c_57013]) ).
tcf(c_57091,plain,
( v3_struct_0(sK6)
| ( k7_yellow_2(u1_struct_0(k2_yellow_2(sK6,sK6,sK7)),sK6,k3_waybel_1(sK6,sK6,sK7),sK11) = sK11 )
| ~ l1_orders_2(sK6)
| ~ v1_funct_1(sK7)
| ~ m2_relset_1(sK7,u1_struct_0(sK6),u1_struct_0(sK6))
| ~ v1_funct_2(sK7,u1_struct_0(sK6),u1_struct_0(sK6)) ),
inference(superposition,[status(thm)],[c_51,c_245]) ).
tcf(c_57092,plain,
( v3_struct_0(sK6)
| ( k7_yellow_2(u1_struct_0(k2_yellow_2(sK6,sK6,sK7)),sK6,k3_waybel_1(sK6,sK6,sK7),sK10) = sK10 )
| ~ l1_orders_2(sK6)
| ~ v1_funct_1(sK7)
| ~ m2_relset_1(sK7,u1_struct_0(sK6),u1_struct_0(sK6))
| ~ v1_funct_2(sK7,u1_struct_0(sK6),u1_struct_0(sK6)) ),
inference(superposition,[status(thm)],[c_52,c_245]) ).
tcf(c_57097,plain,
k7_yellow_2(u1_struct_0(k2_yellow_2(sK6,sK6,sK7)),sK6,k3_waybel_1(sK6,sK6,sK7),sK10) = sK10,
inference(forward_subsumption_resolution,[status(thm)],[c_57092,c_50105,c_66,c_56,c_59,c_57]) ).
tcf(c_57098,plain,
k7_yellow_2(u1_struct_0(k2_yellow_2(sK6,sK6,sK7)),sK6,k3_waybel_1(sK6,sK6,sK7),sK11) = sK11,
inference(forward_subsumption_resolution,[status(thm)],[c_57091,c_50105,c_66,c_56,c_59,c_57]) ).
tcf(c_58167,plain,
( v1_funct_2(k3_waybel_1(sK6,sK6,sK7),u1_struct_0(k2_yellow_2(sK6,sK6,sK7)),u1_struct_0(sK6))
| ~ l1_orders_2(sK6)
| ~ v2_lattice3(sK6)
| ~ v1_lattice3(sK6)
| ~ v4_orders_2(sK6)
| ~ v3_orders_2(sK6)
| ~ v2_orders_2(sK6)
| ~ l1_orders_2(k2_yellow_2(sK6,sK6,sK7))
| ~ v2_lattice3(k2_yellow_2(sK6,sK6,sK7))
| ~ v1_lattice3(k2_yellow_2(sK6,sK6,sK7))
| ~ v4_orders_2(k2_yellow_2(sK6,sK6,sK7))
| ~ v3_orders_2(k2_yellow_2(sK6,sK6,sK7))
| ~ v2_orders_2(k2_yellow_2(sK6,sK6,sK7))
| ~ v1_funct_1(k2_waybel_1(sK6,sK6,sK7))
| ~ m1_relset_1(k2_waybel_1(sK6,sK6,sK7),u1_struct_0(sK6),u1_struct_0(k2_yellow_2(sK6,sK6,sK7)))
| ~ v1_funct_2(k2_waybel_1(sK6,sK6,sK7),u1_struct_0(sK6),u1_struct_0(k2_yellow_2(sK6,sK6,sK7))) ),
inference(superposition,[status(thm)],[c_16061,c_361]) ).
tcf(c_59288,plain,
( m2_relset_1(k2_waybel_1(sK6,sK6,sK7),u1_struct_0(sK6),u1_struct_0(k2_yellow_2(sK6,sK6,sK7)))
| ~ l1_orders_2(sK6)
| ~ v2_lattice3(sK6)
| ~ v1_lattice3(sK6)
| ~ v4_orders_2(sK6)
| ~ v3_orders_2(sK6)
| ~ v2_orders_2(sK6)
| ~ l1_orders_2(k2_yellow_2(sK6,sK6,sK7))
| ~ v2_lattice3(k2_yellow_2(sK6,sK6,sK7))
| ~ v1_lattice3(k2_yellow_2(sK6,sK6,sK7))
| ~ v4_orders_2(k2_yellow_2(sK6,sK6,sK7))
| ~ v3_orders_2(k2_yellow_2(sK6,sK6,sK7))
| ~ v2_orders_2(k2_yellow_2(sK6,sK6,sK7))
| ~ v1_funct_1(k3_waybel_1(sK6,sK6,sK7))
| ~ m1_relset_1(k3_waybel_1(sK6,sK6,sK7),u1_struct_0(k2_yellow_2(sK6,sK6,sK7)),u1_struct_0(sK6))
| ~ v1_funct_2(k3_waybel_1(sK6,sK6,sK7),u1_struct_0(k2_yellow_2(sK6,sK6,sK7)),u1_struct_0(sK6)) ),
inference(superposition,[status(thm)],[c_16054,c_426]) ).
tcf(c_59401,plain,
! [X0: $i] :
( v3_struct_0(sK6)
| v3_struct_0(k2_yellow_2(sK6,sK6,sK7))
| r1_waybel_3(sK6,k7_yellow_2(u1_struct_0(k2_yellow_2(sK6,sK6,sK7)),sK6,k3_waybel_1(sK6,sK6,sK7),X0),sK11)
| ~ l1_orders_2(sK6)
| ~ v2_orders_2(sK6)
| ~ l1_orders_2(k2_yellow_2(sK6,sK6,sK7))
| ~ v2_orders_2(k2_yellow_2(sK6,sK6,sK7))
| ~ v1_funct_1(k3_waybel_1(sK6,sK6,sK7))
| ~ m1_subset_1(sK11,u1_struct_0(k2_yellow_2(sK6,sK6,sK7)))
| ~ m1_subset_1(X0,u1_struct_0(k2_yellow_2(sK6,sK6,sK7)))
| ~ r1_waybel_3(k2_yellow_2(sK6,sK6,sK7),X0,sK11)
| ~ v1_waybel34(k3_waybel_1(sK6,sK6,sK7),k2_yellow_2(sK6,sK6,sK7),sK6)
| ~ m2_relset_1(k3_waybel_1(sK6,sK6,sK7),u1_struct_0(k2_yellow_2(sK6,sK6,sK7)),u1_struct_0(sK6))
| ~ v1_funct_2(k3_waybel_1(sK6,sK6,sK7),u1_struct_0(k2_yellow_2(sK6,sK6,sK7)),u1_struct_0(sK6)) ),
inference(superposition,[status(thm)],[c_57098,c_130]) ).
tcf(c_60634,plain,
( v1_waybel34(k3_waybel_1(sK6,sK6,sK7),k2_yellow_2(sK6,sK6,sK7),sK6)
| ~ l1_orders_2(sK6)
| ~ v3_lattice3(sK6)
| ~ v2_lattice3(sK6)
| ~ v1_lattice3(sK6)
| ~ v4_orders_2(sK6)
| ~ v3_orders_2(sK6)
| ~ v2_orders_2(sK6)
| ~ l1_orders_2(k2_yellow_2(sK6,sK6,sK7))
| ~ v3_lattice3(k2_yellow_2(sK6,sK6,sK7))
| ~ v2_lattice3(k2_yellow_2(sK6,sK6,sK7))
| ~ v1_lattice3(k2_yellow_2(sK6,sK6,sK7))
| ~ v4_orders_2(k2_yellow_2(sK6,sK6,sK7))
| ~ v3_orders_2(k2_yellow_2(sK6,sK6,sK7))
| ~ v2_orders_2(k2_yellow_2(sK6,sK6,sK7))
| ~ v1_funct_1(k2_waybel_1(sK6,sK6,sK7))
| ~ v17_waybel_0(k2_waybel_1(sK6,sK6,sK7),sK6,k2_yellow_2(sK6,sK6,sK7))
| ~ v22_waybel_0(k2_waybel_1(sK6,sK6,sK7),sK6,k2_yellow_2(sK6,sK6,sK7))
| ~ m2_relset_1(k2_waybel_1(sK6,sK6,sK7),u1_struct_0(sK6),u1_struct_0(k2_yellow_2(sK6,sK6,sK7)))
| ~ v1_funct_2(k2_waybel_1(sK6,sK6,sK7),u1_struct_0(sK6),u1_struct_0(k2_yellow_2(sK6,sK6,sK7))) ),
inference(superposition,[status(thm)],[c_16061,c_247]) ).
tcf(c_166436,plain,
! [X0: $i] :
( v3_struct_0(X0)
| r1_waybel_3(X0,sK10,sK11)
| ~ l1_orders_2(sK6)
| ~ v3_lattice3(sK6)
| ~ v2_lattice3(sK6)
| ~ v4_orders_2(sK6)
| ~ v3_orders_2(sK6)
| ~ v2_orders_2(sK6)
| ~ v8_yellow_0(X0,sK6)
| ~ m1_yellow_0(X0,sK6)
| ~ v4_yellow_0(X0,sK6)
| ~ m1_subset_1(sK11,u1_struct_0(sK6))
| ~ m1_subset_1(sK10,u1_struct_0(sK6))
| ~ r1_waybel_3(sK6,sK10,sK11)
| ~ m1_subset_1(sK11,u1_struct_0(X0))
| ~ m1_subset_1(sK10,u1_struct_0(X0)) ),
inference(instantiation,[status(thm)],[c_785]) ).
tcf(c_186436,plain,
( v3_struct_0(k2_yellow_2(sK6,sK6,sK7))
| r1_waybel_3(k2_yellow_2(sK6,sK6,sK7),sK10,sK11)
| ~ l1_orders_2(sK6)
| ~ v3_lattice3(sK6)
| ~ v2_lattice3(sK6)
| ~ v4_orders_2(sK6)
| ~ v3_orders_2(sK6)
| ~ v2_orders_2(sK6)
| ~ m1_subset_1(sK11,u1_struct_0(sK6))
| ~ m1_subset_1(sK10,u1_struct_0(sK6))
| ~ r1_waybel_3(sK6,sK10,sK11)
| ~ v8_yellow_0(k2_yellow_2(sK6,sK6,sK7),sK6)
| ~ m1_yellow_0(k2_yellow_2(sK6,sK6,sK7),sK6)
| ~ v4_yellow_0(k2_yellow_2(sK6,sK6,sK7),sK6)
| ~ m1_subset_1(sK11,u1_struct_0(k2_yellow_2(sK6,sK6,sK7)))
| ~ m1_subset_1(sK10,u1_struct_0(k2_yellow_2(sK6,sK6,sK7))) ),
inference(instantiation,[status(thm)],[c_166436]) ).
fof(f383,definition,
! [X1,X0] :
( ~ sP0(X1,X0)
| ( v3_lattice3(k2_yellow_2(X0,X0,X1))
& v2_lattice3(k2_yellow_2(X0,X0,X1))
& v1_lattice3(k2_yellow_2(X0,X0,X1))
& v25_waybel_0(k2_yellow_2(X0,X0,X1))
& v24_waybel_0(k2_yellow_2(X0,X0,X1))
& v4_yellow_0(k2_yellow_2(X0,X0,X1),X0)
& v3_yellow_0(k2_yellow_2(X0,X0,X1))
& v2_yellow_0(k2_yellow_2(X0,X0,X1))
& v1_yellow_0(k2_yellow_2(X0,X0,X1))
& v4_orders_2(k2_yellow_2(X0,X0,X1))
& v3_orders_2(k2_yellow_2(X0,X0,X1))
& v2_orders_2(k2_yellow_2(X0,X0,X1))
& v1_orders_2(k2_yellow_2(X0,X0,X1))
& ~ v3_struct_0(k2_yellow_2(X0,X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f384,plain,
! [X0,X1] :
( ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v6_waybel_1(X1,X0)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| sP0(X1,X0) ),
inference(definition_folding,[],[f290,f383]) ).
fof(f418,plain,
! [X1,X0] :
( ~ sP0(X1,X0)
| ( v3_lattice3(k2_yellow_2(X0,X0,X1))
& v2_lattice3(k2_yellow_2(X0,X0,X1))
& v1_lattice3(k2_yellow_2(X0,X0,X1))
& v25_waybel_0(k2_yellow_2(X0,X0,X1))
& v24_waybel_0(k2_yellow_2(X0,X0,X1))
& v4_yellow_0(k2_yellow_2(X0,X0,X1),X0)
& v3_yellow_0(k2_yellow_2(X0,X0,X1))
& v2_yellow_0(k2_yellow_2(X0,X0,X1))
& v1_yellow_0(k2_yellow_2(X0,X0,X1))
& v4_orders_2(k2_yellow_2(X0,X0,X1))
& v3_orders_2(k2_yellow_2(X0,X0,X1))
& v2_orders_2(k2_yellow_2(X0,X0,X1))
& v1_orders_2(k2_yellow_2(X0,X0,X1))
& ~ v3_struct_0(k2_yellow_2(X0,X0,X1)) ) ),
inference(nnf_transformation,[],[f383]) ).
fof(f419,plain,
! [X0,X1] :
( ~ sP0(X0,X1)
| ( v3_lattice3(k2_yellow_2(X1,X1,X0))
& v2_lattice3(k2_yellow_2(X1,X1,X0))
& v1_lattice3(k2_yellow_2(X1,X1,X0))
& v25_waybel_0(k2_yellow_2(X1,X1,X0))
& v24_waybel_0(k2_yellow_2(X1,X1,X0))
& v4_yellow_0(k2_yellow_2(X1,X1,X0),X1)
& v3_yellow_0(k2_yellow_2(X1,X1,X0))
& v2_yellow_0(k2_yellow_2(X1,X1,X0))
& v1_yellow_0(k2_yellow_2(X1,X1,X0))
& v4_orders_2(k2_yellow_2(X1,X1,X0))
& v3_orders_2(k2_yellow_2(X1,X1,X0))
& v2_orders_2(k2_yellow_2(X1,X1,X0))
& v1_orders_2(k2_yellow_2(X1,X1,X0))
& ~ v3_struct_0(k2_yellow_2(X1,X1,X0)) ) ),
inference(rectify,[],[f418]) ).
fof(f611,plain,
! [X0,X1] :
( ~ sP0(X0,X1)
| v3_lattice3(k2_yellow_2(X1,X1,X0)) ),
inference(cnf_transformation,[],[f419]) ).
fof(f612,plain,
! [X0,X1] :
( ~ sP0(X0,X1)
| v2_lattice3(k2_yellow_2(X1,X1,X0)) ),
inference(cnf_transformation,[],[f419]) ).
fof(f613,plain,
! [X0,X1] :
( ~ sP0(X0,X1)
| v1_lattice3(k2_yellow_2(X1,X1,X0)) ),
inference(cnf_transformation,[],[f419]) ).
fof(f616,plain,
! [X0,X1] :
( ~ sP0(X0,X1)
| v4_yellow_0(k2_yellow_2(X1,X1,X0),X1) ),
inference(cnf_transformation,[],[f419]) ).
fof(f624,plain,
! [X0,X1] :
( ~ sP0(X0,X1)
| ~ v3_struct_0(k2_yellow_2(X1,X1,X0)) ),
inference(cnf_transformation,[],[f419]) ).
tcf(c_208,plain,
! [X0: $i,X1: $i] :
( ~ sP0(X1,X0)
| ~ v3_struct_0(k2_yellow_2(X0,X0,X1)) ),
inference(cnf_transformation,[],[f624]) ).
tcf(c_216,plain,
! [X0: $i,X1: $i] :
( v4_yellow_0(k2_yellow_2(X1,X1,X0),X1)
| ~ sP0(X0,X1) ),
inference(cnf_transformation,[],[f616]) ).
tcf(c_219,plain,
! [X0: $i,X1: $i] :
( v1_lattice3(k2_yellow_2(X1,X1,X0))
| ~ sP0(X0,X1) ),
inference(cnf_transformation,[],[f613]) ).
tcf(c_220,plain,
! [X0: $i,X1: $i] :
( v2_lattice3(k2_yellow_2(X1,X1,X0))
| ~ sP0(X0,X1) ),
inference(cnf_transformation,[],[f612]) ).
tcf(c_221,plain,
! [X0: $i,X1: $i] :
( v3_lattice3(k2_yellow_2(X1,X1,X0))
| ~ sP0(X0,X1) ),
inference(cnf_transformation,[],[f611]) ).
tcf(c_872,plain,
! [X0: $i,X1: $i] :
( v4_yellow_0(k2_yellow_2(X1,X1,X0),X1)
| ~ sP0(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_216]) ).
tcf(c_878,plain,
! [X0: $i,X1: $i] :
( v1_lattice3(k2_yellow_2(X1,X1,X0))
| ~ sP0(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_219]) ).
tcf(c_880,plain,
! [X0: $i,X1: $i] :
( v2_lattice3(k2_yellow_2(X1,X1,X0))
| ~ sP0(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_220]) ).
tcf(c_882,plain,
! [X0: $i,X1: $i] :
( v3_lattice3(k2_yellow_2(X1,X1,X0))
| ~ sP0(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_221]) ).
tcf(c_884,plain,
! [X0: $i,X1: $i] :
( ~ sP0(X1,X0)
| ~ v3_struct_0(k2_yellow_2(X0,X0,X1)) ),
inference(prop_impl_just,[status(thm)],[c_208]) ).
tcf(c_19515,plain,
! [X0: $i,X1: $i] :
( v3_lattice3(k2_yellow_2(X1,X1,X0))
| ~ m1_relset_1(sK7,u1_struct_0(sK6),u1_struct_0(sK6))
| ( X1 != sK6 )
| ( X0 != sK7 ) ),
inference(resolution_lifted,[status(thm)],[c_882,c_16741]) ).
tcf(c_19516,plain,
( v3_lattice3(k2_yellow_2(sK6,sK6,sK7))
| ~ m1_relset_1(sK7,u1_struct_0(sK6),u1_struct_0(sK6)) ),
inference(unflattening,[status(thm)],[c_19515]) ).
tcf(c_19523,plain,
! [X0: $i,X1: $i] :
( v2_lattice3(k2_yellow_2(X1,X1,X0))
| ~ m1_relset_1(sK7,u1_struct_0(sK6),u1_struct_0(sK6))
| ( X1 != sK6 )
| ( X0 != sK7 ) ),
inference(resolution_lifted,[status(thm)],[c_880,c_16741]) ).
tcf(c_19524,plain,
( v2_lattice3(k2_yellow_2(sK6,sK6,sK7))
| ~ m1_relset_1(sK7,u1_struct_0(sK6),u1_struct_0(sK6)) ),
inference(unflattening,[status(thm)],[c_19523]) ).
tcf(c_19531,plain,
! [X0: $i,X1: $i] :
( v1_lattice3(k2_yellow_2(X1,X1,X0))
| ~ m1_relset_1(sK7,u1_struct_0(sK6),u1_struct_0(sK6))
| ( X1 != sK6 )
| ( X0 != sK7 ) ),
inference(resolution_lifted,[status(thm)],[c_878,c_16741]) ).
tcf(c_19532,plain,
( v1_lattice3(k2_yellow_2(sK6,sK6,sK7))
| ~ m1_relset_1(sK7,u1_struct_0(sK6),u1_struct_0(sK6)) ),
inference(unflattening,[status(thm)],[c_19531]) ).
tcf(c_19547,plain,
! [X0: $i,X1: $i] :
( v4_yellow_0(k2_yellow_2(X1,X1,X0),X1)
| ~ m1_relset_1(sK7,u1_struct_0(sK6),u1_struct_0(sK6))
| ( X1 != sK6 )
| ( X0 != sK7 ) ),
inference(resolution_lifted,[status(thm)],[c_872,c_16741]) ).
tcf(c_19548,plain,
( v4_yellow_0(k2_yellow_2(sK6,sK6,sK7),sK6)
| ~ m1_relset_1(sK7,u1_struct_0(sK6),u1_struct_0(sK6)) ),
inference(unflattening,[status(thm)],[c_19547]) ).
tcf(c_19661,plain,
! [X0: $i,X1: $i] :
( ~ v3_struct_0(k2_yellow_2(X0,X0,X1))
| ~ m1_relset_1(sK7,u1_struct_0(sK6),u1_struct_0(sK6))
| ( X1 != sK7 )
| ( X0 != sK6 ) ),
inference(resolution_lifted,[status(thm)],[c_884,c_16741]) ).
tcf(c_19662,plain,
( ~ v3_struct_0(k2_yellow_2(sK6,sK6,sK7))
| ~ m1_relset_1(sK7,u1_struct_0(sK6),u1_struct_0(sK6)) ),
inference(unflattening,[status(thm)],[c_19661]) ).
tcf(c_51763,plain,
v1_lattice3(k2_yellow_2(sK6,sK6,sK7)),
inference(global_subsumption_just,[status(thm)],[c_51743,c_19532,c_50138]) ).
tcf(c_51765,plain,
v2_lattice3(k2_yellow_2(sK6,sK6,sK7)),
inference(global_subsumption_just,[status(thm)],[c_51746,c_19524,c_50138]) ).
tcf(c_58433,plain,
( v1_funct_2(k3_waybel_1(sK6,sK6,sK7),u1_struct_0(k2_yellow_2(sK6,sK6,sK7)),u1_struct_0(sK6))
| ~ m1_relset_1(k2_waybel_1(sK6,sK6,sK7),u1_struct_0(sK6),u1_struct_0(k2_yellow_2(sK6,sK6,sK7)))
| ~ v1_funct_2(k2_waybel_1(sK6,sK6,sK7),u1_struct_0(sK6),u1_struct_0(k2_yellow_2(sK6,sK6,sK7))) ),
inference(forward_subsumption_resolution,[status(thm)],[c_58167,c_66,c_64,c_63,c_62,c_61,c_60,c_51733,c_51765,c_51763,c_52064,c_52112,c_52160,c_54929]) ).
tcf(c_59091,plain,
v1_funct_2(k3_waybel_1(sK6,sK6,sK7),u1_struct_0(k2_yellow_2(sK6,sK6,sK7)),u1_struct_0(sK6)),
inference(global_subsumption_just,[status(thm)],[c_58433,c_66,c_64,c_56,c_57,c_539,c_50138,c_56909]) ).
tcf(c_59363,plain,
( m2_relset_1(k2_waybel_1(sK6,sK6,sK7),u1_struct_0(sK6),u1_struct_0(k2_yellow_2(sK6,sK6,sK7)))
| ~ m1_relset_1(k3_waybel_1(sK6,sK6,sK7),u1_struct_0(k2_yellow_2(sK6,sK6,sK7)),u1_struct_0(sK6)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_59288,c_66,c_64,c_63,c_62,c_61,c_60,c_51733,c_51765,c_51763,c_52064,c_52112,c_52160,c_55051,c_59091]) ).
tcf(c_59426,plain,
! [X0: $i] :
( r1_waybel_3(sK6,k7_yellow_2(u1_struct_0(k2_yellow_2(sK6,sK6,sK7)),sK6,k3_waybel_1(sK6,sK6,sK7),X0),sK11)
| ~ m1_subset_1(X0,u1_struct_0(k2_yellow_2(sK6,sK6,sK7)))
| ~ r1_waybel_3(k2_yellow_2(sK6,sK6,sK7),X0,sK11)
| ~ v1_waybel34(k3_waybel_1(sK6,sK6,sK7),k2_yellow_2(sK6,sK6,sK7),sK6)
| ~ m2_relset_1(k3_waybel_1(sK6,sK6,sK7),u1_struct_0(k2_yellow_2(sK6,sK6,sK7)),u1_struct_0(sK6)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_59401,c_50105,c_50917,c_66,c_60,c_51733,c_52160,c_55051,c_51,c_59091]) ).
tcf(c_60296,plain,
m2_relset_1(k2_waybel_1(sK6,sK6,sK7),u1_struct_0(sK6),u1_struct_0(k2_yellow_2(sK6,sK6,sK7))),
inference(global_subsumption_just,[status(thm)],[c_59363,c_66,c_64,c_56,c_57,c_539,c_50138,c_56507]) ).
tcf(c_60635,plain,
( v1_waybel34(k3_waybel_1(sK6,sK6,sK7),k2_yellow_2(sK6,sK6,sK7),sK6)
| ~ v3_lattice3(k2_yellow_2(sK6,sK6,sK7))
| ~ v1_funct_2(k2_waybel_1(sK6,sK6,sK7),u1_struct_0(sK6),u1_struct_0(k2_yellow_2(sK6,sK6,sK7))) ),
inference(forward_subsumption_resolution,[status(thm)],[c_60634,c_66,c_65,c_64,c_63,c_62,c_61,c_60,c_51733,c_51765,c_51763,c_52064,c_52112,c_52160,c_54929,c_16075,c_16092,c_60296]) ).
tcf(c_61828,plain,
! [X0: $i] :
( r1_waybel_3(sK6,k7_yellow_2(u1_struct_0(k2_yellow_2(sK6,sK6,sK7)),sK6,k3_waybel_1(sK6,sK6,sK7),X0),sK11)
| ~ m1_subset_1(X0,u1_struct_0(k2_yellow_2(sK6,sK6,sK7)))
| ~ r1_waybel_3(k2_yellow_2(sK6,sK6,sK7),X0,sK11) ),
inference(global_subsumption_just,[status(thm)],[c_59426,c_66,c_64,c_56,c_57,c_539,c_19516,c_50138,c_56359,c_57014,c_59426,c_60635]) ).
tcf(c_61838,plain,
( r1_waybel_3(sK6,sK10,sK11)
| ~ m1_subset_1(sK10,u1_struct_0(k2_yellow_2(sK6,sK6,sK7)))
| ~ r1_waybel_3(k2_yellow_2(sK6,sK6,sK7),sK10,sK11) ),
inference(superposition,[status(thm)],[c_57097,c_61828]) ).
tcf(c_61839,plain,
( r1_waybel_3(sK6,sK10,sK11)
| ~ r1_waybel_3(k2_yellow_2(sK6,sK6,sK7),sK10,sK11) ),
inference(forward_subsumption_resolution,[status(thm)],[c_61838,c_52]) ).
tcf(c_61845,plain,
r1_waybel_3(sK6,sK10,sK11),
inference(global_subsumption_just,[status(thm)],[c_61839,c_50,c_61839]) ).
tcf(c_186437,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_186436,c_61845,c_51514,c_50138,c_19662,c_19548,c_16098,c_49,c_539,c_51,c_52,c_57,c_59,c_53,c_54,c_56,c_60,c_61,c_62,c_64,c_65,c_66]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : LAT366+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.02 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.04/5.50 % Computer : n012.cluster.edu
% 0.04/5.50 % Model : x86_64 x86_64
% 0.04/5.50 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/5.50 % Memory : 8046.5625MB
% 0.04/5.50 % OS : Linux 6.8.0-71-generic
% 0.00/5.50 % CPULimit : 300
% 0.00/5.50 % WCLimit : 300
% 0.00/5.50 % DateTime : Wed Sep 23 21:23:57 UTC 2026
% 0.00/5.50 % CPUTime :
% 0.00/5.50 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.00/5.52 Running first-order theorem proving
% 0.00/5.52 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.00/5.53
% 0.00/5.53 % ======== iProver multi-core TPTP/SMT =========
% 0.00/5.53
% 0.00/5.53 % Detected problem language: tptp
% 0.00/5.53 % Proving...
% 104.30/19.92 % SZS status Started for theBenchmark.p
% 104.30/19.92 % SZS status Theorem for theBenchmark.p
% 104.30/19.92
% 104.30/19.92 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 104.30/19.92
% 104.30/19.92 % ------ iProver source info
% 104.30/19.92
% 104.30/19.92 % git: date: 2026-07-19 20:42:38 +0200
% 104.30/19.92 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 104.30/19.92 % git: non_committed_changes: false
% 104.30/19.92
% 104.30/19.92 % ------ Parsing...
% 104.30/19.92 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 104.30/19.92
% 104.30/19.92 % ------ Preprocessing... sup_sim: 0 sf_s rm: 36 0s sf_e pe_s pe:1:0s pe:2:0s pe:4:0s pe:8:0s pe_e sup_sim: 0 sf_s rm: 11 0s sf_e pe_s pe_e %
% 104.30/19.92
% 104.30/19.92 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 104.30/19.92
% 104.30/19.92 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 104.30/19.92 % ------ Proving...
% 104.30/19.92 % ------ Problem Properties
% 104.30/19.92
% 104.30/19.92 %
% 104.30/19.92 % clauses 297
% 104.30/19.92 % conjectures 17
% 104.30/19.92 % EPR 86
% 104.30/19.92 % Horn 191
% 104.30/19.92 % unary 70
% 104.30/19.92 % binary 66
% 104.30/19.92 % lits 1324
% 104.30/19.92 % lits eq 14
% 104.30/19.92 % fd_pure 0
% 104.30/19.92 % fd_pseudo 0
% 104.30/19.92 % fd_cond 0
% 104.30/19.92 % fd_pseudo_cond 3
% 104.30/19.92 % AC symbols 0
% 104.30/19.92
% 104.30/19.92 % ------ Schedule dynamic 5 is on
% 104.30/19.92
% 104.30/19.92 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 104.30/19.92
% 104.30/19.92
% 104.30/19.92 % ------
% 104.30/19.92 % Current options:
% 104.30/19.92 % ------
% 104.30/19.92
% 104.30/19.92
% 104.30/19.92 %
% 104.30/19.92
% 104.30/19.92 % ------ Proving...
% 104.30/19.92 % Proof_search_loop: time out after: 4168 full_loop iterations
% 104.30/19.92
% 104.30/19.92 % ------ Input Options"1. --res_lit_sel adaptive --res_lit_sel_side num_symb" Time Limit: 15.
% 104.30/19.92
% 104.30/19.92
% 104.30/19.92 % ------
% 104.30/19.92 % Current options:
% 104.30/19.92 % ------
% 104.30/19.92
% 104.30/19.92
% 104.30/19.92 %
% 104.30/19.92
% 104.30/19.92 % ------ Proving...
% 104.30/19.92 %
% 104.30/19.92
% 104.30/19.92 % SZS status Theorem for theBenchmark.p
% 104.30/19.92
% 104.30/19.92 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 104.30/19.92
% 104.30/19.92
%------------------------------------------------------------------------------