%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : LAT369+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 : 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 33.47s 5.66s
% Output : CNFRefutation 33.47s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 15
% Syntax : Number of formulae : 186 ( 33 unt; 1 def)
% Number of atoms : 1414 ( 54 equ)
% Maximal formula atoms : 26 ( 7 avg)
% Number of connectives : 2153 ( 925 ~; 910 |; 281 &)
% ( 4 <=>; 33 =>; 0 <=; 0 <~>)
% Maximal formula depth : 30 ( 8 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 : 35 ( 33 usr; 1 prp; 0-3 aty)
% Number of functors : 8 ( 8 usr; 2 con; 0-3 aty)
% Number of variables : 232 ( 0 sgn 228 !; 4 ?; 89 :)
% 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))
& 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)
=> v1_waybel34(k2_waybel_1(X0,X0,X1),X0,k2_yellow_2(X0,X0,X1)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t42_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))
& 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)
=> v1_waybel34(k2_waybel_1(X0,X0,X1),X0,k2_yellow_2(X0,X0,X1)) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f23,axiom,
! [X0] :
( l1_orders_2(X0)
=> ( v1_lattice3(X0)
=> ~ v3_struct_0(X0) ) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p',cc1_yellow_0) ).
fof(f36,axiom,
! [X0] :
( l1_orders_2(X0)
=> ( v2_lattice3(X0)
=> ~ v3_struct_0(X0) ) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p',cc3_waybel_1) ).
fof(f63,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(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) )
=> ( 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(f72,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(f82,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/sandbox/benchmark/theBenchmark.p',fc10_waybel10) ).
fof(f83,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(f134,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(f137,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(f139,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/sandbox/benchmark/theBenchmark.p',t39_waybel34) ).
fof(f141,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/sandbox/benchmark/theBenchmark.p',t40_waybel34) ).
fof(f163,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,[],[f82]) ).
fof(f184,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(f190,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)
& ~ v1_waybel34(k2_waybel_1(X0,X0,X1),X0,k2_yellow_2(X0,X0,X1)) ) ),
inference(ennf_transformation,[],[f2]) ).
fof(f191,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)
& ~ v1_waybel34(k2_waybel_1(X0,X0,X1),X0,k2_yellow_2(X0,X0,X1)) ) ),
inference(flattening,[],[f190]) ).
fof(f194,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,[],[f63]) ).
fof(f195,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,[],[f194]) ).
fof(f198,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(f199,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,[],[f198]) ).
fof(f200,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v3_struct_0(X0) ),
inference(ennf_transformation,[],[f23]) ).
fof(f201,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v3_struct_0(X0) ),
inference(flattening,[],[f200]) ).
fof(f202,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v3_struct_0(X0) ),
inference(ennf_transformation,[],[f36]) ).
fof(f203,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v3_struct_0(X0) ),
inference(flattening,[],[f202]) ).
fof(f207,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,[],[f184]) ).
fof(f208,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,[],[f207]) ).
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))
| ~ 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,[],[f141]) ).
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))
| ~ 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,[],[f209]) ).
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] :
( ~ 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,[],[f137]) ).
fof(f216,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,[],[f215]) ).
fof(f222,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,[],[f83]) ).
fof(f223,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,[],[f222]) ).
fof(f231,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ! [X1] :
( ~ m1_yellow_0(X1,X0)
| l1_orders_2(X1) ) ),
inference(ennf_transformation,[],[f72]) ).
fof(f236,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,[],[f65]) ).
fof(f237,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,[],[f236]) ).
fof(f266,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,[],[f163]) ).
fof(f267,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,[],[f266]) ).
fof(f276,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,[],[f139]) ).
fof(f277,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,[],[f276]) ).
fof(f350,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))
& v7_waybel_1(sK7,sK6)
& v1_funct_2(sK7,u1_struct_0(sK6),u1_struct_0(sK6))
& v1_funct_1(sK7)
& v4_waybel_0(k2_yellow_2(sK6,sK6,sK7),sK6)
& ~ v1_waybel34(k2_waybel_1(sK6,sK6,sK7),sK6,k2_yellow_2(sK6,sK6,sK7)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6,sK7]),skolemize(X0,sK6),skolemize(X1,sK7)],[f191]) ).
fof(f355,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,[],[f134]) ).
fof(f357,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,[],[f210]) ).
fof(f387,plain,
l1_orders_2(sK6),
inference(cnf_transformation,[],[f350]) ).
fof(f388,plain,
v3_lattice3(sK6),
inference(cnf_transformation,[],[f350]) ).
fof(f389,plain,
v2_lattice3(sK6),
inference(cnf_transformation,[],[f350]) ).
fof(f390,plain,
v1_lattice3(sK6),
inference(cnf_transformation,[],[f350]) ).
fof(f391,plain,
v4_orders_2(sK6),
inference(cnf_transformation,[],[f350]) ).
fof(f392,plain,
v3_orders_2(sK6),
inference(cnf_transformation,[],[f350]) ).
fof(f393,plain,
v2_orders_2(sK6),
inference(cnf_transformation,[],[f350]) ).
fof(f394,plain,
m2_relset_1(sK7,u1_struct_0(sK6),u1_struct_0(sK6)),
inference(cnf_transformation,[],[f350]) ).
fof(f395,plain,
v7_waybel_1(sK7,sK6),
inference(cnf_transformation,[],[f350]) ).
fof(f396,plain,
v1_funct_2(sK7,u1_struct_0(sK6),u1_struct_0(sK6)),
inference(cnf_transformation,[],[f350]) ).
fof(f397,plain,
v1_funct_1(sK7),
inference(cnf_transformation,[],[f350]) ).
fof(f398,plain,
v4_waybel_0(k2_yellow_2(sK6,sK6,sK7),sK6),
inference(cnf_transformation,[],[f350]) ).
fof(f399,plain,
~ v1_waybel34(k2_waybel_1(sK6,sK6,sK7),sK6,k2_yellow_2(sK6,sK6,sK7)),
inference(cnf_transformation,[],[f350]) ).
fof(f403,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,[],[f195]) ).
fof(f426,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| v3_struct_0(X0)
| v1_lattice3(X0) ),
inference(cnf_transformation,[],[f199]) ).
fof(f428,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v3_struct_0(X0) ),
inference(cnf_transformation,[],[f201]) ).
fof(f429,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v3_struct_0(X0) ),
inference(cnf_transformation,[],[f203]) ).
fof(f439,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,[],[f208]) ).
fof(f443,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f355]) ).
fof(f446,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)
| ~ 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(cnf_transformation,[],[f357]) ).
fof(f477,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,[],[f216]) ).
fof(f514,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,[],[f345]) ).
fof(f523,plain,
! [X0,X1] :
( ~ l1_orders_2(X0)
| ~ m1_yellow_0(X1,X0)
| l1_orders_2(X1) ),
inference(cnf_transformation,[],[f231]) ).
fof(f539,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,[],[f237]) ).
fof(f540,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,[],[f237]) ).
fof(f541,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,[],[f237]) ).
fof(f635,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,[],[f267]) ).
fof(f636,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,[],[f267]) ).
fof(f637,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,[],[f267]) ).
fof(f650,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,[],[f277]) ).
fof(f652,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,[],[f277]) ).
tcf(c_49,negated_conjecture,
~ v1_waybel34(k2_waybel_1(sK6,sK6,sK7),sK6,k2_yellow_2(sK6,sK6,sK7)),
inference(cnf_transformation,[],[f399]) ).
tcf(c_50,negated_conjecture,
v4_waybel_0(k2_yellow_2(sK6,sK6,sK7),sK6),
inference(cnf_transformation,[],[f398]) ).
tcf(c_51,negated_conjecture,
v1_funct_1(sK7),
inference(cnf_transformation,[],[f397]) ).
tcf(c_52,negated_conjecture,
v1_funct_2(sK7,u1_struct_0(sK6),u1_struct_0(sK6)),
inference(cnf_transformation,[],[f396]) ).
tcf(c_53,negated_conjecture,
v7_waybel_1(sK7,sK6),
inference(cnf_transformation,[],[f395]) ).
tcf(c_54,negated_conjecture,
m2_relset_1(sK7,u1_struct_0(sK6),u1_struct_0(sK6)),
inference(cnf_transformation,[],[f394]) ).
tcf(c_55,negated_conjecture,
v2_orders_2(sK6),
inference(cnf_transformation,[],[f393]) ).
tcf(c_56,negated_conjecture,
v3_orders_2(sK6),
inference(cnf_transformation,[],[f392]) ).
tcf(c_57,negated_conjecture,
v4_orders_2(sK6),
inference(cnf_transformation,[],[f391]) ).
tcf(c_58,negated_conjecture,
v1_lattice3(sK6),
inference(cnf_transformation,[],[f390]) ).
tcf(c_59,negated_conjecture,
v2_lattice3(sK6),
inference(cnf_transformation,[],[f389]) ).
tcf(c_60,negated_conjecture,
v3_lattice3(sK6),
inference(cnf_transformation,[],[f388]) ).
tcf(c_61,negated_conjecture,
l1_orders_2(sK6),
inference(cnf_transformation,[],[f387]) ).
tcf(c_67,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,[],[f403]) ).
tcf(c_87,plain,
! [X0: $i] :
( v3_struct_0(X0)
| v1_lattice3(X0)
| ~ l1_orders_2(X0)
| ~ v3_lattice3(X0) ),
inference(cnf_transformation,[],[f426]) ).
tcf(c_89,plain,
! [X0: $i] :
( ~ v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ v1_lattice3(X0) ),
inference(cnf_transformation,[],[f428]) ).
tcf(c_90,plain,
! [X0: $i] :
( ~ v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0) ),
inference(cnf_transformation,[],[f429]) ).
tcf(c_101,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,[],[f439]) ).
tcf(c_103,plain,
! [X0: $i,X1: $i,X2: $i] :
( m1_relset_1(X0,X1,X2)
| ~ m2_relset_1(X0,X1,X2) ),
inference(cnf_transformation,[],[f443]) ).
tcf(c_106,plain,
! [X0: $i,X1: $i] :
( v22_waybel_0(k3_waybel_1(X0,X0,X1),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))
| ~ v4_waybel_0(k2_yellow_2(X0,X0,X1),X0) ),
inference(cnf_transformation,[],[f446]) ).
tcf(c_136,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,[],[f477]) ).
tcf(c_173,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,[],[f514]) ).
tcf(c_179,plain,
! [X0: $i,X1: $i] :
( l1_orders_2(X0)
| ~ l1_orders_2(X1)
| ~ m1_yellow_0(X0,X1) ),
inference(cnf_transformation,[],[f523]) ).
tcf(c_195,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,[],[f541]) ).
tcf(c_196,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,[],[f540]) ).
tcf(c_197,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,[],[f539]) ).
tcf(c_273,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,[],[f637]) ).
tcf(c_274,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,[],[f636]) ).
tcf(c_275,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,[],[f635]) ).
tcf(c_286,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,[],[f652]) ).
tcf(c_288,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,[],[f650]) ).
tcf(c_473,plain,
( ~ v3_struct_0(sK6)
| ~ l1_orders_2(sK6)
| ~ v2_lattice3(sK6) ),
inference(instantiation,[status(thm)],[c_90]) ).
tcf(c_694,plain,
! [X0: $i,X1: $i] :
( v22_waybel_0(k3_waybel_1(X0,X0,X1),k2_yellow_2(X0,X0,X1),X0)
| ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v4_waybel_0(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_106,c_90,c_87,c_106]) ).
tcf(c_695,plain,
! [X0: $i,X1: $i] :
( v22_waybel_0(k3_waybel_1(X0,X0,X1),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))
| ~ v4_waybel_0(k2_yellow_2(X0,X0,X1),X0) ),
inference(renaming,[status(thm)],[c_694]) ).
tcf(c_6809,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ l1_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ 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)
| ~ v22_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_49,c_136]) ).
tcf(c_6810,plain,
! [X0: $i] :
( ~ 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)
| ~ 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))
| ~ v17_waybel_0(X0,k2_yellow_2(sK6,sK6,sK7),sK6)
| ~ v22_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_6809]) ).
tcf(c_6812,plain,
! [X0: $i] :
( ( k1_waybel34(k2_yellow_2(sK6,sK6,sK7),sK6,X0) != k2_waybel_1(sK6,sK6,sK7) )
| ~ v1_funct_2(X0,u1_struct_0(k2_yellow_2(sK6,sK6,sK7)),u1_struct_0(sK6))
| ~ m2_relset_1(X0,u1_struct_0(k2_yellow_2(sK6,sK6,sK7)),u1_struct_0(sK6))
| ~ v22_waybel_0(X0,k2_yellow_2(sK6,sK6,sK7),sK6)
| ~ v17_waybel_0(X0,k2_yellow_2(sK6,sK6,sK7),sK6)
| ~ 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))
| ~ v1_lattice3(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))
| ~ v1_funct_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_6810,c_61,c_60,c_59,c_58,c_57,c_56,c_55,c_6810]) ).
tcf(c_6813,plain,
! [X0: $i] :
( ~ 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))
| ~ 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))
| ~ v17_waybel_0(X0,k2_yellow_2(sK6,sK6,sK7),sK6)
| ~ v22_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(renaming,[status(thm)],[c_6812]) ).
tcf(c_8118,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ 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))
| ~ 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))
| ~ m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X1))
| ~ v22_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))
| ( 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_286,c_6813]) ).
tcf(c_8119,plain,
! [X0: $i] :
( ~ 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))
| ~ 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,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))
| ~ v22_waybel_0(k3_waybel_1(sK6,sK6,X0),k2_yellow_2(sK6,sK6,sK7),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_8118]) ).
tcf(c_8121,plain,
! [X0: $i] :
( ( 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))
| ~ v22_waybel_0(k3_waybel_1(sK6,sK6,X0),k2_yellow_2(sK6,sK6,sK7),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))
| ~ v1_lattice3(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_8119,c_61,c_60,c_59,c_58,c_57,c_56,c_55,c_8119]) ).
tcf(c_8122,plain,
! [X0: $i] :
( ~ 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))
| ~ 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,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))
| ~ v22_waybel_0(k3_waybel_1(sK6,sK6,X0),k2_yellow_2(sK6,sK6,sK7),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_8121]) ).
tcf(c_15619,plain,
! [X0: $i,X1: $i] :
( v22_waybel_0(k3_waybel_1(X0,X0,X1),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))
| ~ v4_waybel_0(k2_yellow_2(X0,X0,X1),X0)
| ( X1 != sK7 )
| ( X0 != sK6 ) ),
inference(resolution_lifted,[status(thm)],[c_53,c_695]) ).
tcf(c_15620,plain,
( v22_waybel_0(k3_waybel_1(sK6,sK6,sK7),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))
| ~ v4_waybel_0(k2_yellow_2(sK6,sK6,sK7),sK6) ),
inference(unflattening,[status(thm)],[c_15619]) ).
tcf(c_15636,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_288]) ).
tcf(c_15637,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_15636]) ).
tcf(c_15677,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_275]) ).
tcf(c_15678,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_15677]) ).
tcf(c_15679,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_15678,c_61,c_59,c_57,c_56,c_55,c_51,c_52,c_473,c_15678]) ).
tcf(c_15680,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_15679]) ).
tcf(c_15687,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_274]) ).
tcf(c_15688,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_15687]) ).
tcf(c_15689,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_15688,c_61,c_59,c_57,c_56,c_55,c_51,c_52,c_473,c_15688]) ).
tcf(c_15690,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_15689]) ).
tcf(c_15697,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_273]) ).
tcf(c_15698,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_15697]) ).
tcf(c_15699,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_15698,c_61,c_59,c_57,c_56,c_55,c_51,c_52,c_473,c_15698]) ).
tcf(c_15700,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_15699]) ).
tcf(c_15740,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_101]) ).
tcf(c_15741,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_15740]) ).
tcf(c_15742,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_15741,c_61,c_59,c_51,c_52,c_473,c_15741]) ).
tcf(c_15743,plain,
( v6_waybel_1(sK7,sK6)
| ~ m1_relset_1(sK7,u1_struct_0(sK6),u1_struct_0(sK6)) ),
inference(renaming,[status(thm)],[c_15742]) ).
tcf(c_15750,plain,
! [X0: $i] :
( ~ 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))
| ~ 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,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))
| ~ v22_waybel_0(k3_waybel_1(sK6,sK6,X0),k2_yellow_2(sK6,sK6,sK7),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_8122]) ).
tcf(c_15751,plain,
( ~ 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))
| ~ 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))
| ~ 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)
| ~ 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_15750]) ).
tcf(c_15752,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))
| ( k2_yellow_2(sK6,sK6,sK7) != k2_yellow_2(sK6,sK6,sK7) )
| ~ v1_funct_1(k3_waybel_1(sK6,sK6,sK7))
| ~ 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))
| ~ v1_lattice3(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)) ),
inference(global_subsumption_just,[status(thm)],[c_15751,c_61,c_60,c_59,c_58,c_57,c_56,c_55,c_51,c_54,c_52,c_50,c_15620,c_15637,c_15751]) ).
tcf(c_15753,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))
| ~ 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))
| ~ 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(renaming,[status(thm)],[c_15752]) ).
tcf(c_17012,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_173,c_15743]) ).
tcf(c_17013,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_17012]) ).
tcf(c_17014,plain,
( sP3(sK7,sK6)
| ~ m1_relset_1(sK7,u1_struct_0(sK6),u1_struct_0(sK6)) ),
inference(global_subsumption_just,[status(thm)],[c_17013,c_61,c_60,c_59,c_58,c_57,c_56,c_55,c_51,c_52,c_17013]) ).
tcf(c_24937,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))
| ~ 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))
| ~ 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_15753]) ).
tcf(c_25182,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_15700]) ).
tcf(c_45120,plain,
( ~ v3_struct_0(sK6)
| ~ v1_lattice3(sK6) ),
inference(superposition,[status(thm)],[c_61,c_89]) ).
tcf(c_45128,plain,
~ v3_struct_0(sK6),
inference(forward_subsumption_resolution,[status(thm)],[c_45120,c_58]) ).
tcf(c_45153,plain,
m1_relset_1(sK7,u1_struct_0(sK6),u1_struct_0(sK6)),
inference(superposition,[status(thm)],[c_54,c_103]) ).
tcf(c_45694,plain,
v2_orders_2(k2_yellow_2(sK6,sK6,sK7)),
inference(global_subsumption_just,[status(thm)],[c_25182,c_15700,c_45153]) ).
tcf(c_45696,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))
| ~ 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))
| ~ 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_24937,c_45694]) ).
tcf(c_47457,plain,
! [X0: $i] :
( l1_orders_2(k2_yellow_2(sK6,sK6,sK7))
| ~ l1_orders_2(X0)
| ~ m1_yellow_0(k2_yellow_2(sK6,sK6,sK7),X0) ),
inference(instantiation,[status(thm)],[c_179]) ).
tcf(c_47458,plain,
( l1_orders_2(k2_yellow_2(sK6,sK6,sK7))
| ~ l1_orders_2(sK6)
| ~ m1_yellow_0(k2_yellow_2(sK6,sK6,sK7),sK6) ),
inference(instantiation,[status(thm)],[c_47457]) ).
tcf(c_48617,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_195]) ).
tcf(c_48632,plain,
v1_funct_1(k3_waybel_1(sK6,sK6,sK7)),
inference(forward_subsumption_resolution,[status(thm)],[c_48617,c_45128,c_61,c_51,c_45153]) ).
tcf(c_48935,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_67]) ).
tcf(c_48950,plain,
m1_yellow_0(k2_yellow_2(sK6,sK6,sK7),sK6),
inference(forward_subsumption_resolution,[status(thm)],[c_48935,c_45128,c_61,c_51,c_45153]) ).
fof(f344,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(f345,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,[],[f223,f344]) ).
fof(f366,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,[],[f344]) ).
fof(f367,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,[],[f366]) ).
fof(f500,plain,
! [X0,X1] :
( ~ sP3(X0,X1)
| v3_lattice3(k2_yellow_2(X1,X1,X0)) ),
inference(cnf_transformation,[],[f367]) ).
fof(f501,plain,
! [X0,X1] :
( ~ sP3(X0,X1)
| v2_lattice3(k2_yellow_2(X1,X1,X0)) ),
inference(cnf_transformation,[],[f367]) ).
fof(f502,plain,
! [X0,X1] :
( ~ sP3(X0,X1)
| v1_lattice3(k2_yellow_2(X1,X1,X0)) ),
inference(cnf_transformation,[],[f367]) ).
tcf(c_170,plain,
! [X0: $i,X1: $i] :
( v1_lattice3(k2_yellow_2(X1,X1,X0))
| ~ sP3(X0,X1) ),
inference(cnf_transformation,[],[f502]) ).
tcf(c_171,plain,
! [X0: $i,X1: $i] :
( v2_lattice3(k2_yellow_2(X1,X1,X0))
| ~ sP3(X0,X1) ),
inference(cnf_transformation,[],[f501]) ).
tcf(c_172,plain,
! [X0: $i,X1: $i] :
( v3_lattice3(k2_yellow_2(X1,X1,X0))
| ~ sP3(X0,X1) ),
inference(cnf_transformation,[],[f500]) ).
tcf(c_858,plain,
! [X0: $i,X1: $i] :
( v2_lattice3(k2_yellow_2(X1,X1,X0))
| ~ sP3(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_171]) ).
tcf(c_872,plain,
! [X0: $i,X1: $i] :
( v1_lattice3(k2_yellow_2(X1,X1,X0))
| ~ sP3(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_170]) ).
tcf(c_874,plain,
! [X0: $i,X1: $i] :
( v3_lattice3(k2_yellow_2(X1,X1,X0))
| ~ sP3(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_172]) ).
tcf(c_21162,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_874,c_17014]) ).
tcf(c_21163,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_21162]) ).
tcf(c_21170,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_858,c_17014]) ).
tcf(c_21171,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_21170]) ).
tcf(c_21178,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_872,c_17014]) ).
tcf(c_21179,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_21178]) ).
tcf(c_45834,plain,
( ~ l1_orders_2(k2_yellow_2(sK6,sK6,sK7))
| ~ v1_funct_2(k3_waybel_1(sK6,sK6,sK7),u1_struct_0(k2_yellow_2(sK6,sK6,sK7)),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_1(k3_waybel_1(sK6,sK6,sK7)) ),
inference(global_subsumption_just,[status(thm)],[c_45696,c_15680,c_15690,c_21163,c_21171,c_21179,c_45153,c_45696]) ).
tcf(c_45835,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(renaming,[status(thm)],[c_45834]) ).
tcf(c_48724,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_45835,c_48632]) ).
tcf(c_51782,plain,
( ~ v1_funct_2(k3_waybel_1(sK6,sK6,sK7),u1_struct_0(k2_yellow_2(sK6,sK6,sK7)),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(global_subsumption_just,[status(thm)],[c_48724,c_61,c_45835,c_47458,c_48632,c_48950]) ).
tcf(c_51783,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(renaming,[status(thm)],[c_51782]) ).
tcf(c_51788,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_196,c_51783]) ).
tcf(c_51789,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_51788,c_45128,c_61,c_51,c_45153,c_52]) ).
tcf(c_52770,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_197,c_51789]) ).
tcf(c_52771,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_52770,c_45128,c_61,c_51,c_45153,c_52]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LAT369+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.07 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.17/0.50 % Computer : n006.cluster.edu
% 0.17/0.50 % Model : x86_64 x86_64
% 0.17/0.50 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.50 % Memory : 8046.5625MB
% 0.17/0.50 % OS : Linux 6.8.0-71-generic
% 0.17/0.50 % CPULimit : 300
% 0.17/0.50 % WCLimit : 300
% 0.17/0.50 % DateTime : Wed Sep 23 21:24:57 UTC 2026
% 0.17/0.50 % CPUTime :
% 0.17/0.50 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.17/0.57 Running first-order theorem proving
% 0.17/0.57 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.27/0.59
% 0.27/0.59 % ======== iProver multi-core TPTP/SMT =========
% 0.27/0.59
% 0.27/0.59 % Detected problem language: tptp
% 0.27/0.61 % Proving...
% 33.47/5.66 % SZS status Started for theBenchmark.p
% 33.47/5.66 % SZS status Theorem for theBenchmark.p
% 33.47/5.66
% 33.47/5.66 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 33.47/5.66
% 33.47/5.66 % ------ iProver source info
% 33.47/5.66
% 33.47/5.66 % git: date: 2026-07-19 20:42:38 +0200
% 33.47/5.66 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 33.47/5.66 % git: non_committed_changes: false
% 33.47/5.66
% 33.47/5.66 % ------ Parsing...
% 33.47/5.66 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 33.47/5.66
% 33.47/5.66 % ------ 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: 16 0s sf_e pe_s pe_e %
% 33.47/5.66
% 33.47/5.66 % ------ Preprocessing... gs_s sp: 2 0s gs_e snvd_s sp: 0 0s snvd_e %
% 33.47/5.66
% 33.47/5.66 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 33.47/5.66 % ------ Proving...
% 33.47/5.66 % ------ Problem Properties
% 33.47/5.66
% 33.47/5.66 %
% 33.47/5.66 % clauses 273
% 33.47/5.66 % conjectures 11
% 33.47/5.66 % EPR 76
% 33.47/5.66 % Horn 196
% 33.47/5.66 % unary 69
% 33.47/5.66 % binary 72
% 33.47/5.66 % lits 1128
% 33.47/5.66 % lits eq 20
% 33.47/5.66 % fd_pure 0
% 33.47/5.66 % fd_pseudo 0
% 33.47/5.66 % fd_cond 0
% 33.47/5.66 % fd_pseudo_cond 3
% 33.47/5.66 % AC symbols 0
% 33.47/5.66
% 33.47/5.66 % ------ Schedule dynamic 5 is on
% 33.47/5.66
% 33.47/5.66 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 33.47/5.66
% 33.47/5.66
% 33.47/5.66 % ------
% 33.47/5.66 % Current options:
% 33.47/5.66 % ------
% 33.47/5.66
% 33.47/5.66
% 33.47/5.66 %
% 33.47/5.66
% 33.47/5.66 % ------ Proving...
% 33.47/5.66 %
% 33.47/5.66
% 33.47/5.66 % SZS status Theorem for theBenchmark.p
% 33.47/5.66
% 33.47/5.66 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 33.47/5.67
% 33.47/5.67
%------------------------------------------------------------------------------