%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : LAT370+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n006.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:41 PM UTC 2026
% Result : Theorem 15.44s 2.97s
% Output : CNFRefutation 15.44s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 15
% Syntax : Number of formulae : 181 ( 36 unt; 1 def)
% Number of atoms : 1411 ( 50 equ)
% Maximal formula atoms : 25 ( 7 avg)
% Number of connectives : 2138 ( 908 ~; 906 |; 287 &)
% ( 4 <=>; 33 =>; 0 <=; 0 <~>)
% Maximal formula depth : 29 ( 9 avg)
% Maximal term depth : 3 ( 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 : 8 ( 8 usr; 2 con; 0-3 aty)
% Number of variables : 228 ( 0 sgn 224 !; 4 ?; 87 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [X0] :
( ( l1_orders_2(X0)
& v3_waybel_3(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))
& v7_waybel_1(X1,X0)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v1_funct_1(X1) )
=> ( v1_waybel34(k2_waybel_1(X0,X0,X1),X0,k2_yellow_2(X0,X0,X1))
=> v4_waybel_0(k2_yellow_2(X0,X0,X1),X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t43_waybel34) ).
fof(f2,negated_conjecture,
~ ! [X0] :
( ( l1_orders_2(X0)
& v3_waybel_3(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))
& v7_waybel_1(X1,X0)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v1_funct_1(X1) )
=> ( v1_waybel34(k2_waybel_1(X0,X0,X1),X0,k2_yellow_2(X0,X0,X1))
=> v4_waybel_0(k2_yellow_2(X0,X0,X1),X0) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f23,axiom,
! [X0] :
( l1_orders_2(X0)
=> ( v1_lattice3(X0)
=> ~ v3_struct_0(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc1_lattice3) ).
fof(f31,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/sandbox2/benchmark/theBenchmark.p',cc1_yellow_0) ).
fof(f36,axiom,
! [X0] :
( l1_orders_2(X0)
=> ( v2_lattice3(X0)
=> ~ v3_struct_0(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc2_lattice3) ).
fof(f41,axiom,
! [X0] :
( ( l1_orders_2(X0)
& ~ v3_struct_0(X0) )
=> ! [X1] :
( m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
=> ( ( v7_waybel_1(X1,X0)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v1_funct_1(X1) )
=> ( 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/sandbox2/benchmark/theBenchmark.p',cc3_waybel_1) ).
fof(f65,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/sandbox2/benchmark/theBenchmark.p',dt_k2_yellow_2) ).
fof(f67,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/sandbox2/benchmark/theBenchmark.p',dt_k3_waybel_1) ).
fof(f74,axiom,
! [X0] :
( l1_orders_2(X0)
=> ! [X1] :
( m1_yellow_0(X1,X0)
=> l1_orders_2(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m1_yellow_0) ).
fof(f84,axiom,
! [X0,X1] :
( ( m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
& v7_waybel_1(X1,X0)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v1_funct_1(X1)
& l1_orders_2(X0)
& v4_orders_2(X0)
& v3_orders_2(X0)
& v2_orders_2(X0)
& ~ v3_struct_0(X0) )
=> ( v3_waybel_0(k2_yellow_2(X0,X0,X1),X0)
& v7_yellow_0(k2_yellow_2(X0,X0,X1),X0)
& v5_yellow_0(k2_yellow_2(X0,X0,X1),X0)
& v4_yellow_0(k2_yellow_2(X0,X0,X1),X0)
& 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/sandbox2/benchmark/theBenchmark.p',fc10_waybel10) ).
fof(f85,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/sandbox2/benchmark/theBenchmark.p',fc10_waybel34) ).
fof(f137,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
<=> m1_relset_1(X2,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(f140,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_waybel_3(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) )
=> ( v1_waybel34(k1_waybel34(X0,X1,X2),X1,X0)
=> v22_waybel_0(X2,X0,X1) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t25_waybel34) ).
fof(f142,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))
& v7_waybel_1(X1,X0)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v1_funct_1(X1) )
=> ( k1_waybel34(k2_yellow_2(X0,X0,X1),X0,k3_waybel_1(X0,X0,X1)) = k2_waybel_1(X0,X0,X1)
& k2_waybel34(k2_yellow_2(X0,X0,X1),X0,k2_waybel_1(X0,X0,X1)) = k3_waybel_1(X0,X0,X1)
& v17_waybel_0(k3_waybel_1(X0,X0,X1),k2_yellow_2(X0,X0,X1),X0)
& v18_waybel_0(k2_waybel_1(X0,X0,X1),X0,k2_yellow_2(X0,X0,X1)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t39_waybel34) ).
fof(f144,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))
& v7_waybel_1(X1,X0)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v1_funct_1(X1) )
=> ( v4_waybel_0(k2_yellow_2(X0,X0,X1),X0)
<=> v22_waybel_0(k3_waybel_1(X0,X0,X1),k2_yellow_2(X0,X0,X1),X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t40_waybel34) ).
fof(f165,plain,
! [X0,X1] :
( ( m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
& v7_waybel_1(X1,X0)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v1_funct_1(X1)
& l1_orders_2(X0)
& v4_orders_2(X0)
& v3_orders_2(X0)
& v2_orders_2(X0)
& ~ v3_struct_0(X0) )
=> ( v7_yellow_0(k2_yellow_2(X0,X0,X1),X0)
& v5_yellow_0(k2_yellow_2(X0,X0,X1),X0)
& v4_yellow_0(k2_yellow_2(X0,X0,X1),X0)
& 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(pure_predicate_removal,[],[f84]) ).
fof(f188,plain,
! [X0] :
( ( l1_orders_2(X0)
& ~ v3_struct_0(X0) )
=> ! [X1] :
( m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
=> ( ( v7_waybel_1(X1,X0)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v1_funct_1(X1) )
=> ( 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,[],[f41]) ).
fof(f193,plain,
? [X0] :
( l1_orders_2(X0)
& v3_waybel_3(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))
& v7_waybel_1(X1,X0)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v1_funct_1(X1)
& v1_waybel34(k2_waybel_1(X0,X0,X1),X0,k2_yellow_2(X0,X0,X1))
& ~ v4_waybel_0(k2_yellow_2(X0,X0,X1),X0) ) ),
inference(ennf_transformation,[],[f2]) ).
fof(f194,plain,
? [X0] :
( l1_orders_2(X0)
& v3_waybel_3(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))
& v7_waybel_1(X1,X0)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v1_funct_1(X1)
& v1_waybel34(k2_waybel_1(X0,X0,X1),X0,k2_yellow_2(X0,X0,X1))
& ~ v4_waybel_0(k2_yellow_2(X0,X0,X1),X0) ) ),
inference(flattening,[],[f193]) ).
fof(f199,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,[],[f65]) ).
fof(f200,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,[],[f199]) ).
fof(f201,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,[],[f31]) ).
fof(f202,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,[],[f201]) ).
fof(f203,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v3_struct_0(X0) ),
inference(ennf_transformation,[],[f23]) ).
fof(f204,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v3_struct_0(X0) ),
inference(flattening,[],[f203]) ).
fof(f205,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v3_struct_0(X0) ),
inference(ennf_transformation,[],[f36]) ).
fof(f206,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v3_struct_0(X0) ),
inference(flattening,[],[f205]) ).
fof(f210,plain,
! [X0] :
( ~ l1_orders_2(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v7_waybel_1(X1,X0)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| ( 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,[],[f188]) ).
fof(f211,plain,
! [X0] :
( ~ l1_orders_2(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v7_waybel_1(X1,X0)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| ( 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,[],[f210]) ).
fof(f212,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_waybel_3(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)
| ~ v1_waybel34(k1_waybel34(X0,X1,X2),X1,X0)
| v22_waybel_0(X2,X0,X1) ) ) ),
inference(ennf_transformation,[],[f140]) ).
fof(f213,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_waybel_3(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)
| ~ v1_waybel34(k1_waybel34(X0,X1,X2),X1,X0)
| v22_waybel_0(X2,X0,X1) ) ) ),
inference(flattening,[],[f212]) ).
fof(f214,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))
| ~ v7_waybel_1(X1,X0)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| ( v4_waybel_0(k2_yellow_2(X0,X0,X1),X0)
<=> v22_waybel_0(k3_waybel_1(X0,X0,X1),k2_yellow_2(X0,X0,X1),X0) ) ) ),
inference(ennf_transformation,[],[f144]) ).
fof(f215,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))
| ~ v7_waybel_1(X1,X0)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| ( v4_waybel_0(k2_yellow_2(X0,X0,X1),X0)
<=> v22_waybel_0(k3_waybel_1(X0,X0,X1),k2_yellow_2(X0,X0,X1),X0) ) ) ),
inference(flattening,[],[f214]) ).
fof(f225,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,[],[f85]) ).
fof(f226,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,[],[f225]) ).
fof(f234,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ! [X1] :
( ~ m1_yellow_0(X1,X0)
| l1_orders_2(X1) ) ),
inference(ennf_transformation,[],[f74]) ).
fof(f237,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))
| ~ v7_waybel_1(X1,X0)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| ( k1_waybel34(k2_yellow_2(X0,X0,X1),X0,k3_waybel_1(X0,X0,X1)) = k2_waybel_1(X0,X0,X1)
& k2_waybel34(k2_yellow_2(X0,X0,X1),X0,k2_waybel_1(X0,X0,X1)) = k3_waybel_1(X0,X0,X1)
& v17_waybel_0(k3_waybel_1(X0,X0,X1),k2_yellow_2(X0,X0,X1),X0)
& v18_waybel_0(k2_waybel_1(X0,X0,X1),X0,k2_yellow_2(X0,X0,X1)) ) ) ),
inference(ennf_transformation,[],[f142]) ).
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] :
( ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v7_waybel_1(X1,X0)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| ( k1_waybel34(k2_yellow_2(X0,X0,X1),X0,k3_waybel_1(X0,X0,X1)) = k2_waybel_1(X0,X0,X1)
& k2_waybel34(k2_yellow_2(X0,X0,X1),X0,k2_waybel_1(X0,X0,X1)) = k3_waybel_1(X0,X0,X1)
& v17_waybel_0(k3_waybel_1(X0,X0,X1),k2_yellow_2(X0,X0,X1),X0)
& v18_waybel_0(k2_waybel_1(X0,X0,X1),X0,k2_yellow_2(X0,X0,X1)) ) ) ),
inference(flattening,[],[f237]) ).
fof(f253,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,[],[f67]) ).
fof(f254,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,[],[f253]) ).
fof(f277,plain,
! [X0,X1] :
( ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v7_waybel_1(X1,X0)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| ~ l1_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| v3_struct_0(X0)
| ( v7_yellow_0(k2_yellow_2(X0,X0,X1),X0)
& v5_yellow_0(k2_yellow_2(X0,X0,X1),X0)
& v4_yellow_0(k2_yellow_2(X0,X0,X1),X0)
& 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,[],[f165]) ).
fof(f278,plain,
! [X0,X1] :
( ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v7_waybel_1(X1,X0)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| ~ l1_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| v3_struct_0(X0)
| ( v7_yellow_0(k2_yellow_2(X0,X0,X1),X0)
& v5_yellow_0(k2_yellow_2(X0,X0,X1),X0)
& v4_yellow_0(k2_yellow_2(X0,X0,X1),X0)
& 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,[],[f277]) ).
fof(f353,plain,
( l1_orders_2(sK6)
& v3_waybel_3(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))
& v7_waybel_1(sK7,sK6)
& v1_funct_2(sK7,u1_struct_0(sK6),u1_struct_0(sK6))
& v1_funct_1(sK7)
& v1_waybel34(k2_waybel_1(sK6,sK6,sK7),sK6,k2_yellow_2(sK6,sK6,sK7))
& ~ v4_waybel_0(k2_yellow_2(sK6,sK6,sK7),sK6) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6,sK7]),skolemize(X0,sK6),skolemize(X1,sK7)],[f194]) ).
fof(f358,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,[],[f137]) ).
fof(f360,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))
| ~ v7_waybel_1(X1,X0)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| ( ( ~ v4_waybel_0(k2_yellow_2(X0,X0,X1),X0)
| v22_waybel_0(k3_waybel_1(X0,X0,X1),k2_yellow_2(X0,X0,X1),X0) )
& ( ~ v22_waybel_0(k3_waybel_1(X0,X0,X1),k2_yellow_2(X0,X0,X1),X0)
| v4_waybel_0(k2_yellow_2(X0,X0,X1),X0) ) ) ) ),
inference(nnf_transformation,[],[f215]) ).
fof(f390,plain,
l1_orders_2(sK6),
inference(cnf_transformation,[],[f353]) ).
fof(f391,plain,
v3_waybel_3(sK6),
inference(cnf_transformation,[],[f353]) ).
fof(f392,plain,
v3_lattice3(sK6),
inference(cnf_transformation,[],[f353]) ).
fof(f393,plain,
v2_lattice3(sK6),
inference(cnf_transformation,[],[f353]) ).
fof(f394,plain,
v1_lattice3(sK6),
inference(cnf_transformation,[],[f353]) ).
fof(f395,plain,
v4_orders_2(sK6),
inference(cnf_transformation,[],[f353]) ).
fof(f396,plain,
v3_orders_2(sK6),
inference(cnf_transformation,[],[f353]) ).
fof(f397,plain,
v2_orders_2(sK6),
inference(cnf_transformation,[],[f353]) ).
fof(f398,plain,
m2_relset_1(sK7,u1_struct_0(sK6),u1_struct_0(sK6)),
inference(cnf_transformation,[],[f353]) ).
fof(f399,plain,
v7_waybel_1(sK7,sK6),
inference(cnf_transformation,[],[f353]) ).
fof(f400,plain,
v1_funct_2(sK7,u1_struct_0(sK6),u1_struct_0(sK6)),
inference(cnf_transformation,[],[f353]) ).
fof(f401,plain,
v1_funct_1(sK7),
inference(cnf_transformation,[],[f353]) ).
fof(f402,plain,
v1_waybel34(k2_waybel_1(sK6,sK6,sK7),sK6,k2_yellow_2(sK6,sK6,sK7)),
inference(cnf_transformation,[],[f353]) ).
fof(f403,plain,
~ v4_waybel_0(k2_yellow_2(sK6,sK6,sK7),sK6),
inference(cnf_transformation,[],[f353]) ).
fof(f426,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,[],[f200]) ).
fof(f430,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| v3_struct_0(X0)
| v1_lattice3(X0) ),
inference(cnf_transformation,[],[f202]) ).
fof(f432,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v3_struct_0(X0) ),
inference(cnf_transformation,[],[f204]) ).
fof(f433,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v3_struct_0(X0) ),
inference(cnf_transformation,[],[f206]) ).
fof(f443,plain,
! [X0,X1] :
( ~ l1_orders_2(X0)
| v3_struct_0(X0)
| ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v7_waybel_1(X1,X0)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| v6_waybel_1(X1,X0) ),
inference(cnf_transformation,[],[f211]) ).
fof(f447,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f358]) ).
fof(f450,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_waybel_3(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)
| ~ v1_waybel34(k1_waybel34(X0,X1,X2),X1,X0)
| v22_waybel_0(X2,X0,X1) ),
inference(cnf_transformation,[],[f213]) ).
fof(f452,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))
| ~ v7_waybel_1(X1,X0)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| ~ v22_waybel_0(k3_waybel_1(X0,X0,X1),k2_yellow_2(X0,X0,X1),X0)
| v4_waybel_0(k2_yellow_2(X0,X0,X1),X0) ),
inference(cnf_transformation,[],[f360]) ).
fof(f519,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)
| sP3(X1,X0) ),
inference(cnf_transformation,[],[f348]) ).
fof(f527,plain,
! [X0,X1] :
( ~ l1_orders_2(X0)
| ~ m1_yellow_0(X1,X0)
| l1_orders_2(X1) ),
inference(cnf_transformation,[],[f234]) ).
fof(f539,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))
| ~ v7_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) = k1_waybel34(k2_yellow_2(X0,X0,X1),X0,k3_waybel_1(X0,X0,X1)) ),
inference(cnf_transformation,[],[f238]) ).
fof(f541,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))
| ~ v7_waybel_1(X1,X0)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| v17_waybel_0(k3_waybel_1(X0,X0,X1),k2_yellow_2(X0,X0,X1),X0) ),
inference(cnf_transformation,[],[f238]) ).
fof(f573,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,[],[f254]) ).
fof(f574,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,[],[f254]) ).
fof(f575,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,[],[f254]) ).
fof(f656,plain,
! [X0,X1] :
( ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v7_waybel_1(X1,X0)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| ~ l1_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| v3_struct_0(X0)
| v4_orders_2(k2_yellow_2(X0,X0,X1)) ),
inference(cnf_transformation,[],[f278]) ).
fof(f657,plain,
! [X0,X1] :
( ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v7_waybel_1(X1,X0)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| ~ l1_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| v3_struct_0(X0)
| v3_orders_2(k2_yellow_2(X0,X0,X1)) ),
inference(cnf_transformation,[],[f278]) ).
fof(f658,plain,
! [X0,X1] :
( ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v7_waybel_1(X1,X0)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| ~ l1_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| v3_struct_0(X0)
| v2_orders_2(k2_yellow_2(X0,X0,X1)) ),
inference(cnf_transformation,[],[f278]) ).
tcf(c_49,negated_conjecture,
~ v4_waybel_0(k2_yellow_2(sK6,sK6,sK7),sK6),
inference(cnf_transformation,[],[f403]) ).
tcf(c_50,negated_conjecture,
v1_waybel34(k2_waybel_1(sK6,sK6,sK7),sK6,k2_yellow_2(sK6,sK6,sK7)),
inference(cnf_transformation,[],[f402]) ).
tcf(c_51,negated_conjecture,
v1_funct_1(sK7),
inference(cnf_transformation,[],[f401]) ).
tcf(c_52,negated_conjecture,
v1_funct_2(sK7,u1_struct_0(sK6),u1_struct_0(sK6)),
inference(cnf_transformation,[],[f400]) ).
tcf(c_53,negated_conjecture,
v7_waybel_1(sK7,sK6),
inference(cnf_transformation,[],[f399]) ).
tcf(c_54,negated_conjecture,
m2_relset_1(sK7,u1_struct_0(sK6),u1_struct_0(sK6)),
inference(cnf_transformation,[],[f398]) ).
tcf(c_55,negated_conjecture,
v2_orders_2(sK6),
inference(cnf_transformation,[],[f397]) ).
tcf(c_56,negated_conjecture,
v3_orders_2(sK6),
inference(cnf_transformation,[],[f396]) ).
tcf(c_57,negated_conjecture,
v4_orders_2(sK6),
inference(cnf_transformation,[],[f395]) ).
tcf(c_58,negated_conjecture,
v1_lattice3(sK6),
inference(cnf_transformation,[],[f394]) ).
tcf(c_59,negated_conjecture,
v2_lattice3(sK6),
inference(cnf_transformation,[],[f393]) ).
tcf(c_60,negated_conjecture,
v3_lattice3(sK6),
inference(cnf_transformation,[],[f392]) ).
tcf(c_61,negated_conjecture,
v3_waybel_3(sK6),
inference(cnf_transformation,[],[f391]) ).
tcf(c_62,negated_conjecture,
l1_orders_2(sK6),
inference(cnf_transformation,[],[f390]) ).
tcf(c_87,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,[],[f426]) ).
tcf(c_88,plain,
! [X0: $i] :
( v3_struct_0(X0)
| v1_lattice3(X0)
| ~ l1_orders_2(X0)
| ~ v3_lattice3(X0) ),
inference(cnf_transformation,[],[f430]) ).
tcf(c_90,plain,
! [X0: $i] :
( ~ v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ v1_lattice3(X0) ),
inference(cnf_transformation,[],[f432]) ).
tcf(c_91,plain,
! [X0: $i] :
( ~ v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0) ),
inference(cnf_transformation,[],[f433]) ).
tcf(c_102,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X1)
| v6_waybel_1(X0,X1)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X0)
| ~ v7_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,[],[f443]) ).
tcf(c_104,plain,
! [X0: $i,X1: $i,X2: $i] :
( m1_relset_1(X0,X1,X2)
| ~ m2_relset_1(X0,X1,X2) ),
inference(cnf_transformation,[],[f447]) ).
tcf(c_106,plain,
! [X0: $i,X1: $i,X2: $i] :
( v22_waybel_0(X2,X0,X1)
| ~ l1_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v3_waybel_3(X1)
| ~ v3_lattice3(X1)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X1)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X1)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X1)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X1)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X1)
| ~ v2_orders_2(X0)
| ~ v1_funct_1(X2)
| ~ v17_waybel_0(X2,X0,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_waybel34(k1_waybel34(X0,X1,X2),X1,X0) ),
inference(cnf_transformation,[],[f450]) ).
tcf(c_107,plain,
! [X0: $i,X1: $i] :
( v4_waybel_0(k2_yellow_2(X0,X0,X1),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)
| ~ v1_funct_1(X1)
| ~ v7_waybel_1(X1,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))
| ~ v22_waybel_0(k3_waybel_1(X0,X0,X1),k2_yellow_2(X0,X0,X1),X0) ),
inference(cnf_transformation,[],[f452]) ).
tcf(c_175,plain,
! [X0: $i,X1: $i] :
( sP3(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,[],[f519]) ).
tcf(c_180,plain,
! [X0: $i,X1: $i] :
( l1_orders_2(X0)
| ~ l1_orders_2(X1)
| ~ m1_yellow_0(X0,X1) ),
inference(cnf_transformation,[],[f527]) ).
tcf(c_193,plain,
! [X0: $i,X1: $i] :
( v17_waybel_0(k3_waybel_1(X1,X1,X0),k2_yellow_2(X1,X1,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)
| ~ v7_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,[],[f541]) ).
tcf(c_195,plain,
! [X0: $i,X1: $i] :
( ( k1_waybel34(k2_yellow_2(X1,X1,X0),X1,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)
| ~ v7_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,[],[f539]) ).
tcf(c_220,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,[],[f575]) ).
tcf(c_221,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,[],[f574]) ).
tcf(c_222,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,[],[f573]) ).
tcf(c_289,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X1)
| v2_orders_2(k2_yellow_2(X1,X1,X0))
| ~ l1_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ v1_funct_1(X0)
| ~ v7_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,[],[f658]) ).
tcf(c_290,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X1)
| v3_orders_2(k2_yellow_2(X1,X1,X0))
| ~ l1_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ v1_funct_1(X0)
| ~ v7_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,[],[f657]) ).
tcf(c_291,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X1)
| v4_orders_2(k2_yellow_2(X1,X1,X0))
| ~ l1_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ v1_funct_1(X0)
| ~ v7_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,[],[f656]) ).
tcf(c_474,plain,
( ~ v3_struct_0(sK6)
| ~ l1_orders_2(sK6)
| ~ v2_lattice3(sK6) ),
inference(instantiation,[status(thm)],[c_91]) ).
tcf(c_698,plain,
! [X0: $i,X1: $i] :
( v4_waybel_0(k2_yellow_2(X0,X0,X1),X0)
| ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v22_waybel_0(k3_waybel_1(X0,X0,X1),k2_yellow_2(X0,X0,X1),X0)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v7_waybel_1(X1,X0)
| ~ v1_funct_1(X1)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0) ),
inference(global_subsumption_just,[status(thm)],[c_107,c_91,c_88,c_107]) ).
tcf(c_699,plain,
! [X0: $i,X1: $i] :
( v4_waybel_0(k2_yellow_2(X0,X0,X1),X0)
| ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ v7_waybel_1(X1,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))
| ~ v22_waybel_0(k3_waybel_1(X0,X0,X1),k2_yellow_2(X0,X0,X1),X0) ),
inference(renaming,[status(thm)],[c_698]) ).
tcf(c_705,plain,
! [X0: $i,X1: $i,X2: $i] :
( v22_waybel_0(X2,X0,X1)
| ~ l1_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v3_waybel_3(X1)
| ~ v3_lattice3(X1)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X1)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X1)
| ~ v1_waybel34(k1_waybel34(X0,X1,X2),X1,X0)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v17_waybel_0(X2,X0,X1)
| ~ v1_funct_1(X2)
| ~ v2_orders_2(X0)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X0)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X0)
| ~ v4_orders_2(X1) ),
inference(global_subsumption_just,[status(thm)],[c_106,c_91,c_88,c_106]) ).
tcf(c_706,plain,
! [X0: $i,X1: $i,X2: $i] :
( v22_waybel_0(X2,X0,X1)
| ~ l1_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v3_waybel_3(X1)
| ~ v3_lattice3(X1)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X1)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X1)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X1)
| ~ v2_orders_2(X0)
| ~ v1_funct_1(X2)
| ~ v17_waybel_0(X2,X0,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_waybel34(k1_waybel34(X0,X1,X2),X1,X0) ),
inference(renaming,[status(thm)],[c_705]) ).
tcf(c_6822,plain,
! [X0: $i,X1: $i,X2: $i] :
( v22_waybel_0(X2,X0,X1)
| ~ l1_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v3_waybel_3(X1)
| ~ v3_lattice3(X1)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X1)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X1)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X1)
| ~ v2_orders_2(X0)
| ~ v1_funct_1(X2)
| ~ v17_waybel_0(X2,X0,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))
| ( X1 != sK6 )
| ( k2_yellow_2(sK6,sK6,sK7) != X0 )
| ( k1_waybel34(X0,X1,X2) != k2_waybel_1(sK6,sK6,sK7) ) ),
inference(resolution_lifted,[status(thm)],[c_50,c_706]) ).
tcf(c_6823,plain,
! [X0: $i] :
( v22_waybel_0(X0,k2_yellow_2(sK6,sK6,sK7),sK6)
| ~ l1_orders_2(sK6)
| ~ v3_waybel_3(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(X0)
| ~ 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))
| ~ 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))
| ~ v17_waybel_0(X0,k2_yellow_2(sK6,sK6,sK7),sK6)
| ~ m2_relset_1(X0,u1_struct_0(k2_yellow_2(sK6,sK6,sK7)),u1_struct_0(sK6))
| ~ v1_funct_2(X0,u1_struct_0(k2_yellow_2(sK6,sK6,sK7)),u1_struct_0(sK6))
| ( k1_waybel34(k2_yellow_2(sK6,sK6,sK7),sK6,X0) != k2_waybel_1(sK6,sK6,sK7) ) ),
inference(unflattening,[status(thm)],[c_6822]) ).
tcf(c_6825,plain,
! [X0: $i] :
( v22_waybel_0(X0,k2_yellow_2(sK6,sK6,sK7),sK6)
| ~ v1_funct_1(X0)
| ~ 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))
| ~ 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))
| ~ v17_waybel_0(X0,k2_yellow_2(sK6,sK6,sK7),sK6)
| ~ m2_relset_1(X0,u1_struct_0(k2_yellow_2(sK6,sK6,sK7)),u1_struct_0(sK6))
| ~ v1_funct_2(X0,u1_struct_0(k2_yellow_2(sK6,sK6,sK7)),u1_struct_0(sK6))
| ( k1_waybel34(k2_yellow_2(sK6,sK6,sK7),sK6,X0) != k2_waybel_1(sK6,sK6,sK7) ) ),
inference(global_subsumption_just,[status(thm)],[c_6823,c_62,c_61,c_60,c_59,c_58,c_57,c_56,c_55,c_6823]) ).
tcf(c_8097,plain,
! [X0: $i,X1: $i,X2: $i] :
( v22_waybel_0(X0,k2_yellow_2(sK6,sK6,sK7),sK6)
| ~ 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(X2)
| ~ v1_funct_1(X0)
| ~ v7_waybel_1(X2,X1)
| ~ 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))
| ~ 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))
| ~ m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X1))
| ~ m2_relset_1(X0,u1_struct_0(k2_yellow_2(sK6,sK6,sK7)),u1_struct_0(sK6))
| ~ v1_funct_2(X0,u1_struct_0(k2_yellow_2(sK6,sK6,sK7)),u1_struct_0(sK6))
| ( X1 != sK6 )
| ( k3_waybel_1(X1,X1,X2) != X0 )
| ( k2_yellow_2(X1,X1,X2) != k2_yellow_2(sK6,sK6,sK7) )
| ( k1_waybel34(k2_yellow_2(sK6,sK6,sK7),sK6,X0) != k2_waybel_1(sK6,sK6,sK7) ) ),
inference(resolution_lifted,[status(thm)],[c_193,c_6825]) ).
tcf(c_8098,plain,
! [X0: $i] :
( v22_waybel_0(k3_waybel_1(sK6,sK6,X0),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)
| ~ v1_funct_1(X0)
| ~ v7_waybel_1(X0,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))
| ~ 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,X0))
| ~ m2_relset_1(X0,u1_struct_0(sK6),u1_struct_0(sK6))
| ~ v1_funct_2(X0,u1_struct_0(sK6),u1_struct_0(sK6))
| ~ m2_relset_1(k3_waybel_1(sK6,sK6,X0),u1_struct_0(k2_yellow_2(sK6,sK6,sK7)),u1_struct_0(sK6))
| ~ v1_funct_2(k3_waybel_1(sK6,sK6,X0),u1_struct_0(k2_yellow_2(sK6,sK6,sK7)),u1_struct_0(sK6))
| ( k2_yellow_2(sK6,sK6,X0) != k2_yellow_2(sK6,sK6,sK7) )
| ( k1_waybel34(k2_yellow_2(sK6,sK6,sK7),sK6,k3_waybel_1(sK6,sK6,X0)) != k2_waybel_1(sK6,sK6,sK7) ) ),
inference(unflattening,[status(thm)],[c_8097]) ).
tcf(c_8100,plain,
! [X0: $i] :
( v22_waybel_0(k3_waybel_1(sK6,sK6,X0),k2_yellow_2(sK6,sK6,sK7),sK6)
| ( k1_waybel34(k2_yellow_2(sK6,sK6,sK7),sK6,k3_waybel_1(sK6,sK6,X0)) != k2_waybel_1(sK6,sK6,sK7) )
| ( k2_yellow_2(sK6,sK6,X0) != k2_yellow_2(sK6,sK6,sK7) )
| ~ v1_funct_2(k3_waybel_1(sK6,sK6,X0),u1_struct_0(k2_yellow_2(sK6,sK6,sK7)),u1_struct_0(sK6))
| ~ m2_relset_1(k3_waybel_1(sK6,sK6,X0),u1_struct_0(k2_yellow_2(sK6,sK6,sK7)),u1_struct_0(sK6))
| ~ v1_funct_2(X0,u1_struct_0(sK6),u1_struct_0(sK6))
| ~ m2_relset_1(X0,u1_struct_0(sK6),u1_struct_0(sK6))
| ~ v1_funct_1(k3_waybel_1(sK6,sK6,X0))
| ~ v2_orders_2(k2_yellow_2(sK6,sK6,sK7))
| ~ v3_orders_2(k2_yellow_2(sK6,sK6,sK7))
| ~ v4_orders_2(k2_yellow_2(sK6,sK6,sK7))
| ~ v2_lattice3(k2_yellow_2(sK6,sK6,sK7))
| ~ v3_lattice3(k2_yellow_2(sK6,sK6,sK7))
| ~ l1_orders_2(k2_yellow_2(sK6,sK6,sK7))
| ~ v7_waybel_1(X0,sK6)
| ~ v1_funct_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_8098,c_62,c_60,c_59,c_58,c_57,c_56,c_55,c_8098]) ).
tcf(c_8101,plain,
! [X0: $i] :
( v22_waybel_0(k3_waybel_1(sK6,sK6,X0),k2_yellow_2(sK6,sK6,sK7),sK6)
| ~ v1_funct_1(X0)
| ~ v7_waybel_1(X0,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))
| ~ 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,X0))
| ~ m2_relset_1(X0,u1_struct_0(sK6),u1_struct_0(sK6))
| ~ v1_funct_2(X0,u1_struct_0(sK6),u1_struct_0(sK6))
| ~ m2_relset_1(k3_waybel_1(sK6,sK6,X0),u1_struct_0(k2_yellow_2(sK6,sK6,sK7)),u1_struct_0(sK6))
| ~ v1_funct_2(k3_waybel_1(sK6,sK6,X0),u1_struct_0(k2_yellow_2(sK6,sK6,sK7)),u1_struct_0(sK6))
| ( k2_yellow_2(sK6,sK6,X0) != k2_yellow_2(sK6,sK6,sK7) )
| ( k1_waybel34(k2_yellow_2(sK6,sK6,sK7),sK6,k3_waybel_1(sK6,sK6,X0)) != k2_waybel_1(sK6,sK6,sK7) ) ),
inference(renaming,[status(thm)],[c_8100]) ).
tcf(c_15665,plain,
! [X0: $i,X1: $i] :
( v4_waybel_0(k2_yellow_2(X0,X0,X1),X0)
| ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v2_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))
| ~ v22_waybel_0(k3_waybel_1(X0,X0,X1),k2_yellow_2(X0,X0,X1),X0)
| ( X1 != sK7 )
| ( X0 != sK6 ) ),
inference(resolution_lifted,[status(thm)],[c_53,c_699]) ).
tcf(c_15666,plain,
( v4_waybel_0(k2_yellow_2(sK6,sK6,sK7),sK6)
| ~ l1_orders_2(sK6)
| ~ v3_lattice3(sK6)
| ~ v2_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))
| ~ v22_waybel_0(k3_waybel_1(sK6,sK6,sK7),k2_yellow_2(sK6,sK6,sK7),sK6) ),
inference(unflattening,[status(thm)],[c_15665]) ).
tcf(c_15704,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X0)
| v4_orders_2(k2_yellow_2(X0,X0,X1))
| ~ l1_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_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_53,c_291]) ).
tcf(c_15705,plain,
( v3_struct_0(sK6)
| v4_orders_2(k2_yellow_2(sK6,sK6,sK7))
| ~ l1_orders_2(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_15704]) ).
tcf(c_15706,plain,
( ~ m1_relset_1(sK7,u1_struct_0(sK6),u1_struct_0(sK6))
| v4_orders_2(k2_yellow_2(sK6,sK6,sK7)) ),
inference(global_subsumption_just,[status(thm)],[c_15705,c_62,c_59,c_57,c_56,c_55,c_51,c_52,c_474,c_15705]) ).
tcf(c_15707,plain,
( v4_orders_2(k2_yellow_2(sK6,sK6,sK7))
| ~ m1_relset_1(sK7,u1_struct_0(sK6),u1_struct_0(sK6)) ),
inference(renaming,[status(thm)],[c_15706]) ).
tcf(c_15714,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X0)
| v3_orders_2(k2_yellow_2(X0,X0,X1))
| ~ l1_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_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_53,c_290]) ).
tcf(c_15715,plain,
( v3_struct_0(sK6)
| v3_orders_2(k2_yellow_2(sK6,sK6,sK7))
| ~ l1_orders_2(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_15714]) ).
tcf(c_15716,plain,
( ~ m1_relset_1(sK7,u1_struct_0(sK6),u1_struct_0(sK6))
| v3_orders_2(k2_yellow_2(sK6,sK6,sK7)) ),
inference(global_subsumption_just,[status(thm)],[c_15715,c_62,c_59,c_57,c_56,c_55,c_51,c_52,c_474,c_15715]) ).
tcf(c_15717,plain,
( v3_orders_2(k2_yellow_2(sK6,sK6,sK7))
| ~ m1_relset_1(sK7,u1_struct_0(sK6),u1_struct_0(sK6)) ),
inference(renaming,[status(thm)],[c_15716]) ).
tcf(c_15724,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X0)
| v2_orders_2(k2_yellow_2(X0,X0,X1))
| ~ l1_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_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_53,c_289]) ).
tcf(c_15725,plain,
( v3_struct_0(sK6)
| v2_orders_2(k2_yellow_2(sK6,sK6,sK7))
| ~ l1_orders_2(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_15724]) ).
tcf(c_15726,plain,
( ~ m1_relset_1(sK7,u1_struct_0(sK6),u1_struct_0(sK6))
| v2_orders_2(k2_yellow_2(sK6,sK6,sK7)) ),
inference(global_subsumption_just,[status(thm)],[c_15725,c_62,c_59,c_57,c_56,c_55,c_51,c_52,c_474,c_15725]) ).
tcf(c_15727,plain,
( v2_orders_2(k2_yellow_2(sK6,sK6,sK7))
| ~ m1_relset_1(sK7,u1_struct_0(sK6),u1_struct_0(sK6)) ),
inference(renaming,[status(thm)],[c_15726]) ).
tcf(c_15754,plain,
! [X0: $i,X1: $i] :
( ( k1_waybel34(k2_yellow_2(X0,X0,X1),X0,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_53,c_195]) ).
tcf(c_15755,plain,
( ( k1_waybel34(k2_yellow_2(sK6,sK6,sK7),sK6,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_15754]) ).
tcf(c_15788,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_53,c_102]) ).
tcf(c_15789,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_15788]) ).
tcf(c_15790,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_15789,c_62,c_59,c_51,c_52,c_474,c_15789]) ).
tcf(c_15791,plain,
( v6_waybel_1(sK7,sK6)
| ~ m1_relset_1(sK7,u1_struct_0(sK6),u1_struct_0(sK6)) ),
inference(renaming,[status(thm)],[c_15790]) ).
tcf(c_15798,plain,
! [X0: $i] :
( v22_waybel_0(k3_waybel_1(sK6,sK6,X0),k2_yellow_2(sK6,sK6,sK7),sK6)
| ~ v1_funct_1(X0)
| ~ 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))
| ~ 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,X0))
| ~ m2_relset_1(X0,u1_struct_0(sK6),u1_struct_0(sK6))
| ~ v1_funct_2(X0,u1_struct_0(sK6),u1_struct_0(sK6))
| ~ m2_relset_1(k3_waybel_1(sK6,sK6,X0),u1_struct_0(k2_yellow_2(sK6,sK6,sK7)),u1_struct_0(sK6))
| ~ v1_funct_2(k3_waybel_1(sK6,sK6,X0),u1_struct_0(k2_yellow_2(sK6,sK6,sK7)),u1_struct_0(sK6))
| ( sK6 != sK6 )
| ( X0 != sK7 )
| ( k2_yellow_2(sK6,sK6,X0) != k2_yellow_2(sK6,sK6,sK7) )
| ( k1_waybel34(k2_yellow_2(sK6,sK6,sK7),sK6,k3_waybel_1(sK6,sK6,X0)) != k2_waybel_1(sK6,sK6,sK7) ) ),
inference(resolution_lifted,[status(thm)],[c_53,c_8101]) ).
tcf(c_15799,plain,
( v22_waybel_0(k3_waybel_1(sK6,sK6,sK7),k2_yellow_2(sK6,sK6,sK7),sK6)
| ~ v1_funct_1(sK7)
| ~ 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))
| ~ 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))
| ~ m2_relset_1(sK7,u1_struct_0(sK6),u1_struct_0(sK6))
| ~ v1_funct_2(sK7,u1_struct_0(sK6),u1_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))
| ~ v1_funct_2(k3_waybel_1(sK6,sK6,sK7),u1_struct_0(k2_yellow_2(sK6,sK6,sK7)),u1_struct_0(sK6))
| ( k2_yellow_2(sK6,sK6,sK7) != k2_yellow_2(sK6,sK6,sK7) )
| ( k1_waybel34(k2_yellow_2(sK6,sK6,sK7),sK6,k3_waybel_1(sK6,sK6,sK7)) != k2_waybel_1(sK6,sK6,sK7) ) ),
inference(unflattening,[status(thm)],[c_15798]) ).
tcf(c_15800,plain,
( ~ 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))
| ~ 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))
| ~ 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))
| ( k2_yellow_2(sK6,sK6,sK7) != k2_yellow_2(sK6,sK6,sK7) ) ),
inference(global_subsumption_just,[status(thm)],[c_15799,c_62,c_60,c_59,c_58,c_57,c_56,c_55,c_51,c_54,c_52,c_49,c_15666,c_15755,c_15799]) ).
tcf(c_17061,plain,
! [X0: $i,X1: $i] :
( sP3(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_175,c_15791]) ).
tcf(c_17062,plain,
( sP3(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_17061]) ).
tcf(c_17063,plain,
( sP3(sK7,sK6)
| ~ m1_relset_1(sK7,u1_struct_0(sK6),u1_struct_0(sK6)) ),
inference(global_subsumption_just,[status(thm)],[c_17062,c_62,c_60,c_59,c_58,c_57,c_56,c_55,c_51,c_52,c_17062]) ).
tcf(c_23033,plain,
( ~ 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))
| ~ 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))
| ~ 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(equality_resolution_simp,[status(thm)],[c_15800]) ).
tcf(c_23278,plain,
( v2_orders_2(k2_yellow_2(sK6,sK6,sK7))
| ~ m1_relset_1(sK7,u1_struct_0(sK6),u1_struct_0(sK6)) ),
inference(prop_impl_just,[status(thm)],[c_15727]) ).
tcf(c_41106,plain,
( ~ v3_struct_0(sK6)
| ~ v1_lattice3(sK6) ),
inference(superposition,[status(thm)],[c_62,c_90]) ).
tcf(c_41114,plain,
~ v3_struct_0(sK6),
inference(forward_subsumption_resolution,[status(thm)],[c_41106,c_58]) ).
tcf(c_41145,plain,
m1_relset_1(sK7,u1_struct_0(sK6),u1_struct_0(sK6)),
inference(superposition,[status(thm)],[c_54,c_104]) ).
tcf(c_41708,plain,
v2_orders_2(k2_yellow_2(sK6,sK6,sK7)),
inference(global_subsumption_just,[status(thm)],[c_23278,c_15727,c_41145]) ).
tcf(c_41710,plain,
( ~ 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))
| ~ v4_orders_2(k2_yellow_2(sK6,sK6,sK7))
| ~ v3_orders_2(k2_yellow_2(sK6,sK6,sK7))
| ~ v1_funct_1(k3_waybel_1(sK6,sK6,sK7))
| ~ 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(backward_subsumption_resolution,[status(thm)],[c_23033,c_41708]) ).
tcf(c_44763,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_52,c_220]) ).
tcf(c_44779,plain,
v1_funct_1(k3_waybel_1(sK6,sK6,sK7)),
inference(forward_subsumption_resolution,[status(thm)],[c_44763,c_41114,c_62,c_51,c_41145]) ).
tcf(c_45269,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_52,c_87]) ).
tcf(c_45285,plain,
m1_yellow_0(k2_yellow_2(sK6,sK6,sK7),sK6),
inference(forward_subsumption_resolution,[status(thm)],[c_45269,c_41114,c_62,c_51,c_41145]) ).
tcf(c_45883,plain,
( l1_orders_2(k2_yellow_2(sK6,sK6,sK7))
| ~ l1_orders_2(sK6) ),
inference(superposition,[status(thm)],[c_45285,c_180]) ).
tcf(c_45884,plain,
l1_orders_2(k2_yellow_2(sK6,sK6,sK7)),
inference(forward_subsumption_resolution,[status(thm)],[c_45883,c_62]) ).
fof(f347,definition,
! [X1,X0] :
( ~ sP3(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,[sP3])],[predicate_definition_introduction]) ).
fof(f348,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)
| sP3(X1,X0) ),
inference(definition_folding,[],[f226,f347]) ).
fof(f370,plain,
! [X1,X0] :
( ~ sP3(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,[],[f347]) ).
fof(f371,plain,
! [X0,X1] :
( ~ sP3(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,[],[f370]) ).
fof(f505,plain,
! [X0,X1] :
( ~ sP3(X0,X1)
| v3_lattice3(k2_yellow_2(X1,X1,X0)) ),
inference(cnf_transformation,[],[f371]) ).
fof(f506,plain,
! [X0,X1] :
( ~ sP3(X0,X1)
| v2_lattice3(k2_yellow_2(X1,X1,X0)) ),
inference(cnf_transformation,[],[f371]) ).
tcf(c_173,plain,
! [X0: $i,X1: $i] :
( v2_lattice3(k2_yellow_2(X1,X1,X0))
| ~ sP3(X0,X1) ),
inference(cnf_transformation,[],[f506]) ).
tcf(c_174,plain,
! [X0: $i,X1: $i] :
( v3_lattice3(k2_yellow_2(X1,X1,X0))
| ~ sP3(X0,X1) ),
inference(cnf_transformation,[],[f505]) ).
tcf(c_861,plain,
! [X0: $i,X1: $i] :
( v2_lattice3(k2_yellow_2(X1,X1,X0))
| ~ sP3(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_173]) ).
tcf(c_877,plain,
! [X0: $i,X1: $i] :
( v3_lattice3(k2_yellow_2(X1,X1,X0))
| ~ sP3(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_174]) ).
tcf(c_21367,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_877,c_17063]) ).
tcf(c_21368,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_21367]) ).
tcf(c_21375,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_861,c_17063]) ).
tcf(c_21376,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_21375]) ).
tcf(c_41852,plain,
( ~ l1_orders_2(k2_yellow_2(sK6,sK6,sK7))
| ~ v1_funct_1(k3_waybel_1(sK6,sK6,sK7))
| ~ 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(global_subsumption_just,[status(thm)],[c_41710,c_15707,c_15717,c_21368,c_21376,c_41145,c_41710]) ).
tcf(c_44882,plain,
( ~ l1_orders_2(k2_yellow_2(sK6,sK6,sK7))
| ~ 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(backward_subsumption_resolution,[status(thm)],[c_41852,c_44779]) ).
tcf(c_45885,plain,
( ~ 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(backward_subsumption_resolution,[status(thm)],[c_44882,c_45884]) ).
tcf(c_46142,plain,
( v3_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))
| ~ m2_relset_1(k3_waybel_1(sK6,sK6,sK7),u1_struct_0(k2_yellow_2(sK6,sK6,sK7)),u1_struct_0(sK6)) ),
inference(superposition,[status(thm)],[c_221,c_45885]) ).
tcf(c_46143,plain,
~ 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_46142,c_41114,c_62,c_51,c_41145,c_52]) ).
tcf(c_46401,plain,
( v3_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(superposition,[status(thm)],[c_222,c_46143]) ).
tcf(c_46402,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_46401,c_41114,c_62,c_51,c_41145,c_52]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT370+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.09/0.35 % Computer : n006.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Wed Sep 23 21:25:11 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.12/0.42 Running first-order theorem proving
% 0.12/0.42 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/0.43
% 0.12/0.43 % ======== iProver multi-core TPTP/SMT =========
% 0.12/0.43
% 0.12/0.43 % Detected problem language: tptp
% 0.12/0.45 % Proving...
% 15.44/2.97 % SZS status Started for theBenchmark.p
% 15.44/2.97 % SZS status Theorem for theBenchmark.p
% 15.44/2.97
% 15.44/2.97 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 15.44/2.97
% 15.44/2.97 % ------ iProver source info
% 15.44/2.97
% 15.44/2.97 % git: date: 2026-07-19 20:42:38 +0200
% 15.44/2.97 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 15.44/2.97 % git: non_committed_changes: false
% 15.44/2.97
% 15.44/2.97 % ------ Parsing...
% 15.44/2.97 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 15.44/2.97
% 15.44/2.97 % ------ Preprocessing... sup_sim: 0 sf_s rm: 30 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: 17 0s sf_e pe_s pe_e %
% 15.44/2.97
% 15.44/2.97 % ------ Preprocessing... gs_s sp: 2 0s gs_e snvd_s sp: 0 0s snvd_e %
% 15.44/2.97
% 15.44/2.97 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 15.44/2.97 % ------ Proving...
% 15.44/2.97 % ------ Problem Properties
% 15.44/2.97
% 15.44/2.97 %
% 15.44/2.97 % clauses 273
% 15.44/2.97 % conjectures 11
% 15.44/2.97 % EPR 76
% 15.44/2.97 % Horn 195
% 15.44/2.97 % unary 69
% 15.44/2.97 % binary 73
% 15.44/2.97 % lits 1124
% 15.44/2.97 % lits eq 20
% 15.44/2.97 % fd_pure 0
% 15.44/2.97 % fd_pseudo 0
% 15.44/2.97 % fd_cond 0
% 15.44/2.97 % fd_pseudo_cond 3
% 15.44/2.97 % AC symbols 0
% 15.44/2.97
% 15.44/2.97 % ------ Schedule dynamic 5 is on
% 15.44/2.97
% 15.44/2.97 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 15.44/2.97
% 15.44/2.97
% 15.44/2.97 % ------
% 15.44/2.97 % Current options:
% 15.44/2.97 % ------
% 15.44/2.97
% 15.44/2.97
% 15.44/2.97 %
% 15.44/2.97
% 15.44/2.97 % ------ Proving...
% 15.44/2.97 %
% 15.44/2.97
% 15.44/2.97 % SZS status Theorem for theBenchmark.p
% 15.44/2.97
% 15.44/2.97 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 15.44/2.98
% 15.44/2.98
%------------------------------------------------------------------------------