%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LAT370+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n001.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 : Tue Sep 29 11:48:40 AM UTC 2026
% Result : Theorem 2.60s 0.91s
% Output : Refutation 2.60s
% Verified :
% SZS Type : Refutation
% Derivation depth : 34
% Number of leaves : 28
% Syntax : Number of formulae : 374 ( 52 unt; 13 def)
% Number of atoms : 2846 ( 32 equ)
% Maximal formula atoms : 28 ( 7 avg)
% Number of connectives : 3721 (1249 ~;2074 |; 347 &)
% ( 17 <=>; 34 =>; 0 <=; 0 <~>)
% Maximal formula depth : 29 ( 9 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 53 ( 51 usr; 14 prp; 0-3 aty)
% Number of functors : 8 ( 8 usr; 2 con; 0-3 aty)
% Number of variables : 223 ( 0 sgn 219 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [X0] :
( ( v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& v2_lattice3(X0)
& v3_lattice3(X0)
& v3_waybel_3(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( ( v1_funct_1(X1)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v7_waybel_1(X1,X0)
& m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
=> ( 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/sandbox/benchmark/theBenchmark.p',t43_waybel34) ).
fof(f2,negated_conjecture,
~ ! [X0] :
( ( v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& v2_lattice3(X0)
& v3_lattice3(X0)
& v3_waybel_3(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( ( v1_funct_1(X1)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v7_waybel_1(X1,X0)
& m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
=> ( 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/sandbox/benchmark/theBenchmark.p',cc1_lattice3) ).
fof(f41,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
=> ( ( v1_funct_1(X1)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v7_waybel_1(X1,X0) )
=> ( v1_funct_1(X1)
& ~ v1_xboole_0(X1)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v1_partfun1(X1,u1_struct_0(X0),u1_struct_0(X0))
& v6_waybel_1(X1,X0) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc3_waybel_1) ).
fof(f63,axiom,
! [X0,X1,X2] :
( ( v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& v2_lattice3(X0)
& l1_orders_2(X0)
& v2_orders_2(X1)
& v3_orders_2(X1)
& v4_orders_2(X1)
& v1_lattice3(X1)
& v2_lattice3(X1)
& l1_orders_2(X1)
& v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
& m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0)) )
=> ( v1_funct_1(k2_waybel34(X0,X1,X2))
& v1_funct_2(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
& m2_relset_1(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k2_waybel34) ).
fof(f64,axiom,
! [X0,X1,X2] :
( ( ~ v3_struct_0(X0)
& l1_orders_2(X0)
& ~ v3_struct_0(X1)
& l1_orders_2(X1)
& v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> ( v1_funct_1(k2_waybel_1(X0,X1,X2))
& v1_funct_2(k2_waybel_1(X0,X1,X2),u1_struct_0(X0),u1_struct_0(k2_yellow_2(X0,X1,X2)))
& m2_relset_1(k2_waybel_1(X0,X1,X2),u1_struct_0(X0),u1_struct_0(k2_yellow_2(X0,X1,X2))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k2_waybel_1) ).
fof(f65,axiom,
! [X0,X1,X2] :
( ( ~ v3_struct_0(X0)
& l1_orders_2(X0)
& ~ v3_struct_0(X1)
& l1_orders_2(X1)
& v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> ( v1_orders_2(k2_yellow_2(X0,X1,X2))
& v4_yellow_0(k2_yellow_2(X0,X1,X2),X1)
& m1_yellow_0(k2_yellow_2(X0,X1,X2),X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k2_yellow_2) ).
fof(f67,axiom,
! [X0,X1,X2] :
( ( ~ v3_struct_0(X0)
& l1_orders_2(X0)
& ~ v3_struct_0(X1)
& l1_orders_2(X1)
& v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> ( v1_funct_1(k3_waybel_1(X0,X1,X2))
& v1_funct_2(k3_waybel_1(X0,X1,X2),u1_struct_0(k2_yellow_2(X0,X1,X2)),u1_struct_0(X1))
& m2_relset_1(k3_waybel_1(X0,X1,X2),u1_struct_0(k2_yellow_2(X0,X1,X2)),u1_struct_0(X1)) ) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p',dt_m1_yellow_0) ).
fof(f84,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& l1_orders_2(X0)
& v1_funct_1(X1)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v7_waybel_1(X1,X0)
& m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
=> ( ~ v3_struct_0(k2_yellow_2(X0,X0,X1))
& v1_orders_2(k2_yellow_2(X0,X0,X1))
& v2_orders_2(k2_yellow_2(X0,X0,X1))
& v3_orders_2(k2_yellow_2(X0,X0,X1))
& v4_orders_2(k2_yellow_2(X0,X0,X1))
& v4_yellow_0(k2_yellow_2(X0,X0,X1),X0)
& v5_yellow_0(k2_yellow_2(X0,X0,X1),X0)
& v7_yellow_0(k2_yellow_2(X0,X0,X1),X0)
& v3_waybel_0(k2_yellow_2(X0,X0,X1),X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc10_waybel10) ).
fof(f85,axiom,
! [X0,X1] :
( ( v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& v2_lattice3(X0)
& v3_lattice3(X0)
& l1_orders_2(X0)
& v1_funct_1(X1)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v6_waybel_1(X1,X0)
& m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
=> ( ~ v3_struct_0(k2_yellow_2(X0,X0,X1))
& v1_orders_2(k2_yellow_2(X0,X0,X1))
& v2_orders_2(k2_yellow_2(X0,X0,X1))
& v3_orders_2(k2_yellow_2(X0,X0,X1))
& v4_orders_2(k2_yellow_2(X0,X0,X1))
& v1_yellow_0(k2_yellow_2(X0,X0,X1))
& v2_yellow_0(k2_yellow_2(X0,X0,X1))
& v3_yellow_0(k2_yellow_2(X0,X0,X1))
& v4_yellow_0(k2_yellow_2(X0,X0,X1),X0)
& v24_waybel_0(k2_yellow_2(X0,X0,X1))
& v25_waybel_0(k2_yellow_2(X0,X0,X1))
& v1_lattice3(k2_yellow_2(X0,X0,X1))
& v2_lattice3(k2_yellow_2(X0,X0,X1))
& v3_lattice3(k2_yellow_2(X0,X0,X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc10_waybel34) ).
fof(f92,axiom,
! [X0,X1,X2] :
( ( v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& v2_lattice3(X0)
& v3_lattice3(X0)
& l1_orders_2(X0)
& v2_orders_2(X1)
& v3_orders_2(X1)
& v4_orders_2(X1)
& v1_lattice3(X1)
& v2_lattice3(X1)
& v3_lattice3(X1)
& l1_orders_2(X1)
& v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
& v18_waybel_0(X2,X1,X0)
& m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0)) )
=> ( v1_relat_1(k2_waybel34(X0,X1,X2))
& v1_funct_1(k2_waybel34(X0,X1,X2))
& ~ v1_xboole_0(k2_waybel34(X0,X1,X2))
& v1_funct_2(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
& v1_partfun1(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
& v17_waybel_0(k2_waybel34(X0,X1,X2),X0,X1)
& v19_waybel_0(k2_waybel34(X0,X1,X2),X0,X1)
& v21_waybel_0(k2_waybel34(X0,X1,X2),X0,X1)
& v4_waybel_1(k2_waybel34(X0,X1,X2),X0,X1)
& v5_orders_3(k2_waybel34(X0,X1,X2),X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc2_waybel34) ).
fof(f137,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(f140,axiom,
! [X0] :
( ( v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& v2_lattice3(X0)
& v3_lattice3(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( ( v2_orders_2(X1)
& v3_orders_2(X1)
& v4_orders_2(X1)
& v1_lattice3(X1)
& v2_lattice3(X1)
& v3_lattice3(X1)
& v3_waybel_3(X1)
& l1_orders_2(X1) )
=> ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v17_waybel_0(X2,X0,X1)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> ( v1_waybel34(k1_waybel34(X0,X1,X2),X1,X0)
=> v22_waybel_0(X2,X0,X1) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t25_waybel34) ).
fof(f142,axiom,
! [X0] :
( ( v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& v2_lattice3(X0)
& v3_lattice3(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( ( v1_funct_1(X1)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v7_waybel_1(X1,X0)
& m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
=> ( v18_waybel_0(k2_waybel_1(X0,X0,X1),X0,k2_yellow_2(X0,X0,X1))
& v17_waybel_0(k3_waybel_1(X0,X0,X1),k2_yellow_2(X0,X0,X1),X0)
& k2_waybel34(k2_yellow_2(X0,X0,X1),X0,k2_waybel_1(X0,X0,X1)) = k3_waybel_1(X0,X0,X1)
& k1_waybel34(k2_yellow_2(X0,X0,X1),X0,k3_waybel_1(X0,X0,X1)) = k2_waybel_1(X0,X0,X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t39_waybel34) ).
fof(f144,axiom,
! [X0] :
( ( v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& v2_lattice3(X0)
& v3_lattice3(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( ( v1_funct_1(X1)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v7_waybel_1(X1,X0)
& m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
=> ( 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(f172,plain,
! [X0,X1,X2] :
( ( v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& v2_lattice3(X0)
& v3_lattice3(X0)
& l1_orders_2(X0)
& v2_orders_2(X1)
& v3_orders_2(X1)
& v4_orders_2(X1)
& v1_lattice3(X1)
& v2_lattice3(X1)
& v3_lattice3(X1)
& l1_orders_2(X1)
& v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
& v18_waybel_0(X2,X1,X0)
& m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0)) )
=> ( v1_relat_1(k2_waybel34(X0,X1,X2))
& v1_funct_1(k2_waybel34(X0,X1,X2))
& ~ v1_xboole_0(k2_waybel34(X0,X1,X2))
& v1_funct_2(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
& v1_partfun1(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
& v17_waybel_0(k2_waybel34(X0,X1,X2),X0,X1)
& v19_waybel_0(k2_waybel34(X0,X1,X2),X0,X1)
& v4_waybel_1(k2_waybel34(X0,X1,X2),X0,X1)
& v5_orders_3(k2_waybel34(X0,X1,X2),X0,X1) ) ),
inference(pure_predicate_removal,[],[f92]) ).
fof(f177,plain,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& l1_orders_2(X0)
& v1_funct_1(X1)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v7_waybel_1(X1,X0)
& m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
=> ( ~ v3_struct_0(k2_yellow_2(X0,X0,X1))
& v1_orders_2(k2_yellow_2(X0,X0,X1))
& v2_orders_2(k2_yellow_2(X0,X0,X1))
& v3_orders_2(k2_yellow_2(X0,X0,X1))
& v4_orders_2(k2_yellow_2(X0,X0,X1))
& v4_yellow_0(k2_yellow_2(X0,X0,X1),X0)
& v5_yellow_0(k2_yellow_2(X0,X0,X1),X0)
& v7_yellow_0(k2_yellow_2(X0,X0,X1),X0) ) ),
inference(pure_predicate_removal,[],[f84]) ).
fof(f197,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
=> ( ( v1_funct_1(X1)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v7_waybel_1(X1,X0) )
=> ( v1_funct_1(X1)
& ~ v1_xboole_0(X1)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v6_waybel_1(X1,X0) ) ) ) ),
inference(pure_predicate_removal,[],[f41]) ).
fof(f203,plain,
! [X0,X1,X2] :
( ( v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& v2_lattice3(X0)
& v3_lattice3(X0)
& l1_orders_2(X0)
& v2_orders_2(X1)
& v3_orders_2(X1)
& v4_orders_2(X1)
& v1_lattice3(X1)
& v2_lattice3(X1)
& v3_lattice3(X1)
& l1_orders_2(X1)
& v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
& v18_waybel_0(X2,X1,X0)
& m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0)) )
=> ( v1_relat_1(k2_waybel34(X0,X1,X2))
& v1_funct_1(k2_waybel34(X0,X1,X2))
& ~ v1_xboole_0(k2_waybel34(X0,X1,X2))
& v1_funct_2(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
& v17_waybel_0(k2_waybel34(X0,X1,X2),X0,X1)
& v19_waybel_0(k2_waybel34(X0,X1,X2),X0,X1)
& v4_waybel_1(k2_waybel34(X0,X1,X2),X0,X1)
& v5_orders_3(k2_waybel34(X0,X1,X2),X0,X1) ) ),
inference(pure_predicate_removal,[],[f172]) ).
fof(f221,plain,
? [X0] :
( ? [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))
& v1_funct_1(X1)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v7_waybel_1(X1,X0)
& m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
& v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& v2_lattice3(X0)
& v3_lattice3(X0)
& v3_waybel_3(X0)
& l1_orders_2(X0) ),
inference(ennf_transformation,[],[f2]) ).
fof(f222,plain,
? [X0] :
( ? [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))
& v1_funct_1(X1)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v7_waybel_1(X1,X0)
& m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
& v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& v2_lattice3(X0)
& v3_lattice3(X0)
& v3_waybel_3(X0)
& l1_orders_2(X0) ),
inference(flattening,[],[f221]) ).
fof(f245,plain,
! [X0] :
( ~ v3_struct_0(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f23]) ).
fof(f246,plain,
! [X0] :
( ~ v3_struct_0(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f245]) ).
fof(f273,plain,
! [X0] :
( ! [X1] :
( ( v1_funct_1(X1)
& ~ v1_xboole_0(X1)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v6_waybel_1(X1,X0) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v7_waybel_1(X1,X0)
| ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f197]) ).
fof(f274,plain,
! [X0] :
( ! [X1] :
( ( v1_funct_1(X1)
& ~ v1_xboole_0(X1)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v6_waybel_1(X1,X0) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v7_waybel_1(X1,X0)
| ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f273]) ).
fof(f311,plain,
! [X0,X1,X2] :
( ( v1_funct_1(k2_waybel34(X0,X1,X2))
& v1_funct_2(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
& m2_relset_1(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1)) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f63]) ).
fof(f312,plain,
! [X0,X1,X2] :
( ( v1_funct_1(k2_waybel34(X0,X1,X2))
& v1_funct_2(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
& m2_relset_1(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1)) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0)) ),
inference(flattening,[],[f311]) ).
fof(f313,plain,
! [X0,X1,X2] :
( ( v1_funct_1(k2_waybel_1(X0,X1,X2))
& v1_funct_2(k2_waybel_1(X0,X1,X2),u1_struct_0(X0),u1_struct_0(k2_yellow_2(X0,X1,X2)))
& m2_relset_1(k2_waybel_1(X0,X1,X2),u1_struct_0(X0),u1_struct_0(k2_yellow_2(X0,X1,X2))) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| v3_struct_0(X1)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(ennf_transformation,[],[f64]) ).
fof(f314,plain,
! [X0,X1,X2] :
( ( v1_funct_1(k2_waybel_1(X0,X1,X2))
& v1_funct_2(k2_waybel_1(X0,X1,X2),u1_struct_0(X0),u1_struct_0(k2_yellow_2(X0,X1,X2)))
& m2_relset_1(k2_waybel_1(X0,X1,X2),u1_struct_0(X0),u1_struct_0(k2_yellow_2(X0,X1,X2))) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| v3_struct_0(X1)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(flattening,[],[f313]) ).
fof(f315,plain,
! [X0,X1,X2] :
( ( v1_orders_2(k2_yellow_2(X0,X1,X2))
& v4_yellow_0(k2_yellow_2(X0,X1,X2),X1)
& m1_yellow_0(k2_yellow_2(X0,X1,X2),X1) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| v3_struct_0(X1)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(ennf_transformation,[],[f65]) ).
fof(f316,plain,
! [X0,X1,X2] :
( ( v1_orders_2(k2_yellow_2(X0,X1,X2))
& v4_yellow_0(k2_yellow_2(X0,X1,X2),X1)
& m1_yellow_0(k2_yellow_2(X0,X1,X2),X1) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| v3_struct_0(X1)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(flattening,[],[f315]) ).
fof(f317,plain,
! [X0,X1,X2] :
( ( v1_funct_1(k3_waybel_1(X0,X1,X2))
& v1_funct_2(k3_waybel_1(X0,X1,X2),u1_struct_0(k2_yellow_2(X0,X1,X2)),u1_struct_0(X1))
& m2_relset_1(k3_waybel_1(X0,X1,X2),u1_struct_0(k2_yellow_2(X0,X1,X2)),u1_struct_0(X1)) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| v3_struct_0(X1)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(ennf_transformation,[],[f67]) ).
fof(f318,plain,
! [X0,X1,X2] :
( ( v1_funct_1(k3_waybel_1(X0,X1,X2))
& v1_funct_2(k3_waybel_1(X0,X1,X2),u1_struct_0(k2_yellow_2(X0,X1,X2)),u1_struct_0(X1))
& m2_relset_1(k3_waybel_1(X0,X1,X2),u1_struct_0(k2_yellow_2(X0,X1,X2)),u1_struct_0(X1)) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| v3_struct_0(X1)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(flattening,[],[f317]) ).
fof(f322,plain,
! [X0] :
( ! [X1] :
( l1_orders_2(X1)
| ~ m1_yellow_0(X1,X0) )
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f74]) ).
fof(f326,plain,
! [X0,X1] :
( ( ~ v3_struct_0(k2_yellow_2(X0,X0,X1))
& v1_orders_2(k2_yellow_2(X0,X0,X1))
& v2_orders_2(k2_yellow_2(X0,X0,X1))
& v3_orders_2(k2_yellow_2(X0,X0,X1))
& v4_orders_2(k2_yellow_2(X0,X0,X1))
& v4_yellow_0(k2_yellow_2(X0,X0,X1),X0)
& v5_yellow_0(k2_yellow_2(X0,X0,X1),X0)
& v7_yellow_0(k2_yellow_2(X0,X0,X1),X0) )
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v7_waybel_1(X1,X0)
| ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f177]) ).
fof(f327,plain,
! [X0,X1] :
( ( ~ v3_struct_0(k2_yellow_2(X0,X0,X1))
& v1_orders_2(k2_yellow_2(X0,X0,X1))
& v2_orders_2(k2_yellow_2(X0,X0,X1))
& v3_orders_2(k2_yellow_2(X0,X0,X1))
& v4_orders_2(k2_yellow_2(X0,X0,X1))
& v4_yellow_0(k2_yellow_2(X0,X0,X1),X0)
& v5_yellow_0(k2_yellow_2(X0,X0,X1),X0)
& v7_yellow_0(k2_yellow_2(X0,X0,X1),X0) )
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v7_waybel_1(X1,X0)
| ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) ),
inference(flattening,[],[f326]) ).
fof(f328,plain,
! [X0,X1] :
( ( ~ v3_struct_0(k2_yellow_2(X0,X0,X1))
& v1_orders_2(k2_yellow_2(X0,X0,X1))
& v2_orders_2(k2_yellow_2(X0,X0,X1))
& v3_orders_2(k2_yellow_2(X0,X0,X1))
& v4_orders_2(k2_yellow_2(X0,X0,X1))
& v1_yellow_0(k2_yellow_2(X0,X0,X1))
& v2_yellow_0(k2_yellow_2(X0,X0,X1))
& v3_yellow_0(k2_yellow_2(X0,X0,X1))
& v4_yellow_0(k2_yellow_2(X0,X0,X1),X0)
& v24_waybel_0(k2_yellow_2(X0,X0,X1))
& v25_waybel_0(k2_yellow_2(X0,X0,X1))
& v1_lattice3(k2_yellow_2(X0,X0,X1))
& v2_lattice3(k2_yellow_2(X0,X0,X1))
& v3_lattice3(k2_yellow_2(X0,X0,X1)) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v6_waybel_1(X1,X0)
| ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f85]) ).
fof(f329,plain,
! [X0,X1] :
( ( ~ v3_struct_0(k2_yellow_2(X0,X0,X1))
& v1_orders_2(k2_yellow_2(X0,X0,X1))
& v2_orders_2(k2_yellow_2(X0,X0,X1))
& v3_orders_2(k2_yellow_2(X0,X0,X1))
& v4_orders_2(k2_yellow_2(X0,X0,X1))
& v1_yellow_0(k2_yellow_2(X0,X0,X1))
& v2_yellow_0(k2_yellow_2(X0,X0,X1))
& v3_yellow_0(k2_yellow_2(X0,X0,X1))
& v4_yellow_0(k2_yellow_2(X0,X0,X1),X0)
& v24_waybel_0(k2_yellow_2(X0,X0,X1))
& v25_waybel_0(k2_yellow_2(X0,X0,X1))
& v1_lattice3(k2_yellow_2(X0,X0,X1))
& v2_lattice3(k2_yellow_2(X0,X0,X1))
& v3_lattice3(k2_yellow_2(X0,X0,X1)) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v6_waybel_1(X1,X0)
| ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) ),
inference(flattening,[],[f328]) ).
fof(f342,plain,
! [X0,X1,X2] :
( ( v1_relat_1(k2_waybel34(X0,X1,X2))
& v1_funct_1(k2_waybel34(X0,X1,X2))
& ~ v1_xboole_0(k2_waybel34(X0,X1,X2))
& v1_funct_2(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
& v17_waybel_0(k2_waybel34(X0,X1,X2),X0,X1)
& v19_waybel_0(k2_waybel34(X0,X1,X2),X0,X1)
& v4_waybel_1(k2_waybel34(X0,X1,X2),X0,X1)
& v5_orders_3(k2_waybel34(X0,X1,X2),X0,X1) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ v3_lattice3(X1)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v18_waybel_0(X2,X1,X0)
| ~ m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f203]) ).
fof(f343,plain,
! [X0,X1,X2] :
( ( v1_relat_1(k2_waybel34(X0,X1,X2))
& v1_funct_1(k2_waybel34(X0,X1,X2))
& ~ v1_xboole_0(k2_waybel34(X0,X1,X2))
& v1_funct_2(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
& v17_waybel_0(k2_waybel34(X0,X1,X2),X0,X1)
& v19_waybel_0(k2_waybel34(X0,X1,X2),X0,X1)
& v4_waybel_1(k2_waybel34(X0,X1,X2),X0,X1)
& v5_orders_3(k2_waybel34(X0,X1,X2),X0,X1) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ v3_lattice3(X1)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v18_waybel_0(X2,X1,X0)
| ~ m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0)) ),
inference(flattening,[],[f342]) ).
fof(f403,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( v22_waybel_0(X2,X0,X1)
| ~ v1_waybel34(k1_waybel34(X0,X1,X2),X1,X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v17_waybel_0(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ v3_lattice3(X1)
| ~ v3_waybel_3(X1)
| ~ l1_orders_2(X1) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f140]) ).
fof(f404,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( v22_waybel_0(X2,X0,X1)
| ~ v1_waybel34(k1_waybel34(X0,X1,X2),X1,X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v17_waybel_0(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ v3_lattice3(X1)
| ~ v3_waybel_3(X1)
| ~ l1_orders_2(X1) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f403]) ).
fof(f407,plain,
! [X0] :
( ! [X1] :
( ( v18_waybel_0(k2_waybel_1(X0,X0,X1),X0,k2_yellow_2(X0,X0,X1))
& v17_waybel_0(k3_waybel_1(X0,X0,X1),k2_yellow_2(X0,X0,X1),X0)
& k2_waybel34(k2_yellow_2(X0,X0,X1),X0,k2_waybel_1(X0,X0,X1)) = k3_waybel_1(X0,X0,X1)
& k1_waybel34(k2_yellow_2(X0,X0,X1),X0,k3_waybel_1(X0,X0,X1)) = k2_waybel_1(X0,X0,X1) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v7_waybel_1(X1,X0)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f142]) ).
fof(f408,plain,
! [X0] :
( ! [X1] :
( ( v18_waybel_0(k2_waybel_1(X0,X0,X1),X0,k2_yellow_2(X0,X0,X1))
& v17_waybel_0(k3_waybel_1(X0,X0,X1),k2_yellow_2(X0,X0,X1),X0)
& k2_waybel34(k2_yellow_2(X0,X0,X1),X0,k2_waybel_1(X0,X0,X1)) = k3_waybel_1(X0,X0,X1)
& k1_waybel34(k2_yellow_2(X0,X0,X1),X0,k3_waybel_1(X0,X0,X1)) = k2_waybel_1(X0,X0,X1) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v7_waybel_1(X1,X0)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f407]) ).
fof(f410,plain,
! [X0] :
( ! [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) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v7_waybel_1(X1,X0)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f144]) ).
fof(f411,plain,
! [X0] :
( ! [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) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v7_waybel_1(X1,X0)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f410]) ).
fof(f418,plain,
m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0)),
inference(cnf_transformation,[],[f222]) ).
fof(f419,plain,
v7_waybel_1(sK1,sK0),
inference(cnf_transformation,[],[f222]) ).
fof(f420,plain,
v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0)),
inference(cnf_transformation,[],[f222]) ).
fof(f421,plain,
v1_funct_1(sK1),
inference(cnf_transformation,[],[f222]) ).
fof(f422,plain,
v1_waybel34(k2_waybel_1(sK0,sK0,sK1),sK0,k2_yellow_2(sK0,sK0,sK1)),
inference(cnf_transformation,[],[f222]) ).
fof(f423,plain,
~ v4_waybel_0(k2_yellow_2(sK0,sK0,sK1),sK0),
inference(cnf_transformation,[],[f222]) ).
fof(f424,plain,
l1_orders_2(sK0),
inference(cnf_transformation,[],[f222]) ).
fof(f425,plain,
v3_waybel_3(sK0),
inference(cnf_transformation,[],[f222]) ).
fof(f426,plain,
v3_lattice3(sK0),
inference(cnf_transformation,[],[f222]) ).
fof(f427,plain,
v2_lattice3(sK0),
inference(cnf_transformation,[],[f222]) ).
fof(f428,plain,
v1_lattice3(sK0),
inference(cnf_transformation,[],[f222]) ).
fof(f429,plain,
v4_orders_2(sK0),
inference(cnf_transformation,[],[f222]) ).
fof(f430,plain,
v3_orders_2(sK0),
inference(cnf_transformation,[],[f222]) ).
fof(f431,plain,
v2_orders_2(sK0),
inference(cnf_transformation,[],[f222]) ).
fof(f463,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v3_struct_0(X0) ),
inference(cnf_transformation,[],[f246]) ).
fof(f494,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,[],[f274]) ).
fof(f523,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| m2_relset_1(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f312]) ).
fof(f524,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| v1_funct_2(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f312]) ).
fof(f526,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| v3_struct_0(X1)
| ~ l1_orders_2(X0)
| v3_struct_0(X0)
| m2_relset_1(k2_waybel_1(X0,X1,X2),u1_struct_0(X0),u1_struct_0(k2_yellow_2(X0,X1,X2))) ),
inference(cnf_transformation,[],[f314]) ).
fof(f527,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| v3_struct_0(X1)
| ~ l1_orders_2(X0)
| v3_struct_0(X0)
| v1_funct_2(k2_waybel_1(X0,X1,X2),u1_struct_0(X0),u1_struct_0(k2_yellow_2(X0,X1,X2))) ),
inference(cnf_transformation,[],[f314]) ).
fof(f528,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| v3_struct_0(X1)
| ~ l1_orders_2(X0)
| v3_struct_0(X0)
| v1_funct_1(k2_waybel_1(X0,X1,X2)) ),
inference(cnf_transformation,[],[f314]) ).
fof(f529,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,[],[f316]) ).
fof(f534,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,[],[f318]) ).
fof(f540,plain,
! [X0,X1] :
( ~ l1_orders_2(X0)
| ~ m1_yellow_0(X1,X0)
| l1_orders_2(X1) ),
inference(cnf_transformation,[],[f322]) ).
fof(f552,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,[],[f327]) ).
fof(f553,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,[],[f327]) ).
fof(f554,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,[],[f327]) ).
fof(f557,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)) ),
inference(cnf_transformation,[],[f329]) ).
fof(f558,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)
| v2_lattice3(k2_yellow_2(X0,X0,X1)) ),
inference(cnf_transformation,[],[f329]) ).
fof(f559,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)
| v1_lattice3(k2_yellow_2(X0,X0,X1)) ),
inference(cnf_transformation,[],[f329]) ).
fof(f603,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v18_waybel_0(X2,X1,X0)
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X2)
| ~ 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)
| ~ 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)
| v17_waybel_0(k2_waybel34(X0,X1,X2),X0,X1) ),
inference(cnf_transformation,[],[f343]) ).
fof(f867,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f137]) ).
fof(f870,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,[],[f404]) ).
fof(f872,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,[],[f408]) ).
fof(f873,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)
| k3_waybel_1(X0,X0,X1) = k2_waybel34(k2_yellow_2(X0,X0,X1),X0,k2_waybel_1(X0,X0,X1)) ),
inference(cnf_transformation,[],[f408]) ).
fof(f875,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)
| v18_waybel_0(k2_waybel_1(X0,X0,X1),X0,k2_yellow_2(X0,X0,X1)) ),
inference(cnf_transformation,[],[f408]) ).
fof(f877,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,[],[f411]) ).
fof(f884,plain,
~ v2_orders_2(sK0),
inference(consistent_polarity_flipping,[],[f431]) ).
fof(f885,plain,
~ v3_orders_2(sK0),
inference(consistent_polarity_flipping,[],[f430]) ).
fof(f886,plain,
~ v1_lattice3(sK0),
inference(consistent_polarity_flipping,[],[f428]) ).
fof(f887,plain,
~ v2_lattice3(sK0),
inference(consistent_polarity_flipping,[],[f427]) ).
fof(f888,plain,
~ v3_waybel_3(sK0),
inference(consistent_polarity_flipping,[],[f425]) ).
fof(f889,plain,
~ l1_orders_2(sK0),
inference(consistent_polarity_flipping,[],[f424]) ).
fof(f890,plain,
~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0)),
inference(consistent_polarity_flipping,[],[f420]) ).
fof(f922,plain,
! [X0] :
( v1_lattice3(X0)
| l1_orders_2(X0)
| v3_struct_0(X0) ),
inference(consistent_polarity_flipping,[],[f463]) ).
fof(f954,plain,
! [X0,X1] :
( ~ v7_waybel_1(X1,X0)
| ~ v3_struct_0(X0)
| ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| l1_orders_2(X0)
| v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| v6_waybel_1(X1,X0) ),
inference(consistent_polarity_flipping,[],[f494]) ).
fof(f981,plain,
! [X2,X0,X1] :
( ~ v1_funct_2(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
| v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X2)
| l1_orders_2(X1)
| v2_lattice3(X1)
| v1_lattice3(X1)
| ~ v4_orders_2(X1)
| v3_orders_2(X1)
| v2_orders_2(X1)
| l1_orders_2(X0)
| v2_lattice3(X0)
| v1_lattice3(X0)
| ~ v4_orders_2(X0)
| v3_orders_2(X0)
| v2_orders_2(X0)
| ~ m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0)) ),
inference(consistent_polarity_flipping,[],[f524]) ).
fof(f982,plain,
! [X2,X0,X1] :
( m2_relset_1(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
| v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X2)
| l1_orders_2(X1)
| v2_lattice3(X1)
| v1_lattice3(X1)
| ~ v4_orders_2(X1)
| v3_orders_2(X1)
| v2_orders_2(X1)
| l1_orders_2(X0)
| v2_lattice3(X0)
| v1_lattice3(X0)
| ~ v4_orders_2(X0)
| v3_orders_2(X0)
| v2_orders_2(X0)
| ~ m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0)) ),
inference(consistent_polarity_flipping,[],[f523]) ).
fof(f983,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| l1_orders_2(X1)
| ~ v3_struct_0(X1)
| l1_orders_2(X0)
| ~ v3_struct_0(X0)
| v1_funct_1(k2_waybel_1(X0,X1,X2)) ),
inference(consistent_polarity_flipping,[],[f528]) ).
fof(f984,plain,
! [X2,X0,X1] :
( ~ v1_funct_2(k2_waybel_1(X0,X1,X2),u1_struct_0(X0),u1_struct_0(k2_yellow_2(X0,X1,X2)))
| 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_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(consistent_polarity_flipping,[],[f527]) ).
fof(f985,plain,
! [X2,X0,X1] :
( m2_relset_1(k2_waybel_1(X0,X1,X2),u1_struct_0(X0),u1_struct_0(k2_yellow_2(X0,X1,X2)))
| v1_funct_2(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_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(consistent_polarity_flipping,[],[f526]) ).
fof(f988,plain,
! [X2,X0,X1] :
( m1_yellow_0(k2_yellow_2(X0,X1,X2),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_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(consistent_polarity_flipping,[],[f529]) ).
fof(f989,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(consistent_polarity_flipping,[],[f534]) ).
fof(f995,plain,
! [X0,X1] :
( ~ l1_orders_2(X1)
| ~ m1_yellow_0(X1,X0)
| l1_orders_2(X0) ),
inference(consistent_polarity_flipping,[],[f540]) ).
fof(f1003,plain,
! [X0,X1] :
( ~ v2_orders_2(k2_yellow_2(X0,X0,X1))
| ~ 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)
| ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) ),
inference(consistent_polarity_flipping,[],[f554]) ).
fof(f1004,plain,
! [X0,X1] :
( ~ v3_orders_2(k2_yellow_2(X0,X0,X1))
| ~ 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)
| ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) ),
inference(consistent_polarity_flipping,[],[f553]) ).
fof(f1005,plain,
! [X0,X1] :
( ~ v7_waybel_1(X1,X0)
| ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| 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(consistent_polarity_flipping,[],[f552]) ).
fof(f1020,plain,
! [X0,X1] :
( ~ v1_lattice3(k2_yellow_2(X0,X0,X1))
| ~ 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)
| ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) ),
inference(consistent_polarity_flipping,[],[f559]) ).
fof(f1021,plain,
! [X0,X1] :
( ~ v2_lattice3(k2_yellow_2(X0,X0,X1))
| ~ 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)
| ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) ),
inference(consistent_polarity_flipping,[],[f558]) ).
fof(f1022,plain,
! [X0,X1] :
( ~ v6_waybel_1(X1,X0)
| ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| 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)) ),
inference(consistent_polarity_flipping,[],[f557]) ).
fof(f1055,plain,
! [X2,X0,X1] :
( ~ v17_waybel_0(k2_waybel34(X0,X1,X2),X0,X1)
| v18_waybel_0(X2,X1,X0)
| v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X2)
| 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)
| l1_orders_2(X0)
| ~ v3_lattice3(X0)
| v2_lattice3(X0)
| v1_lattice3(X0)
| ~ v4_orders_2(X0)
| v3_orders_2(X0)
| v2_orders_2(X0)
| ~ m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0)) ),
inference(consistent_polarity_flipping,[],[f603]) ).
fof(f1280,plain,
! [X2,X0,X1] :
( ~ v1_waybel34(k1_waybel34(X0,X1,X2),X1,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)
| l1_orders_2(X0)
| v22_waybel_0(X2,X0,X1) ),
inference(consistent_polarity_flipping,[],[f870]) ).
fof(f1282,plain,
! [X0,X1] :
( ~ v18_waybel_0(k2_waybel_1(X0,X0,X1),X0,k2_yellow_2(X0,X0,X1))
| ~ 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)
| l1_orders_2(X0) ),
inference(consistent_polarity_flipping,[],[f875]) ).
fof(f1284,plain,
! [X0,X1] :
( ~ v7_waybel_1(X1,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))
| l1_orders_2(X0)
| v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| k3_waybel_1(X0,X0,X1) = k2_waybel34(k2_yellow_2(X0,X0,X1),X0,k2_waybel_1(X0,X0,X1)) ),
inference(consistent_polarity_flipping,[],[f873]) ).
fof(f1285,plain,
! [X0,X1] :
( ~ v7_waybel_1(X1,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))
| l1_orders_2(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(consistent_polarity_flipping,[],[f872]) ).
fof(f1288,plain,
! [X0,X1] :
( ~ v22_waybel_0(k3_waybel_1(X0,X0,X1),k2_yellow_2(X0,X0,X1),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)
| l1_orders_2(X0)
| v4_waybel_0(k2_yellow_2(X0,X0,X1),X0) ),
inference(consistent_polarity_flipping,[],[f877]) ).
fof(f1315,plain,
( l1_orders_2(sK0)
| v3_struct_0(sK0) ),
inference(resolution,[],[f922,f886]) ).
fof(f1320,plain,
v3_struct_0(sK0),
inference(forward_subsumption_resolution,[],[f1315,f889]) ).
fof(f1341,plain,
m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0)),
inference(resolution,[],[f867,f418]) ).
fof(f1916,plain,
( ~ v3_struct_0(sK0)
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| l1_orders_2(sK0)
| v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| v6_waybel_1(sK1,sK0) ),
inference(resolution,[],[f954,f419]) ).
fof(f1922,plain,
( ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| l1_orders_2(sK0)
| v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| v6_waybel_1(sK1,sK0) ),
inference(forward_subsumption_resolution,[],[f1916,f1320]) ).
fof(f1923,plain,
( l1_orders_2(sK0)
| v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| v6_waybel_1(sK1,sK0) ),
inference(forward_subsumption_resolution,[],[f1922,f1341]) ).
fof(f1924,plain,
( v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| v6_waybel_1(sK1,sK0) ),
inference(forward_subsumption_resolution,[],[f1923,f889]) ).
fof(f1925,plain,
( ~ v1_funct_1(sK1)
| v6_waybel_1(sK1,sK0) ),
inference(forward_subsumption_resolution,[],[f1924,f890]) ).
fof(f1926,plain,
v6_waybel_1(sK1,sK0),
inference(forward_subsumption_resolution,[],[f1925,f421]) ).
fof(f1949,definition,
( spl33_26
<=> v6_waybel_1(sK1,sK0) ),
introduced(definition,[new_symbols(definition,[spl33_26])],[avatar_definition]) ).
fof(f1951,plain,
( v6_waybel_1(sK1,sK0)
| ~ spl33_26 ),
inference(avatar_component_clause,[],[f1949]) ).
fof(f1957,plain,
spl33_26,
inference(avatar_split_clause,[],[f1926,f1949]) ).
fof(f1958,plain,
( v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| l1_orders_2(sK0)
| ~ v3_struct_0(sK0)
| l1_orders_2(sK0)
| ~ v3_struct_0(sK0)
| v1_funct_1(k2_waybel_1(sK0,sK0,sK1)) ),
inference(resolution,[],[f983,f1341]) ).
fof(f1975,plain,
( v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| l1_orders_2(sK0)
| ~ v3_struct_0(sK0)
| v1_funct_1(k2_waybel_1(sK0,sK0,sK1)) ),
inference(duplicate_literal_removal,[],[f1958]) ).
fof(f1983,plain,
( ~ v1_funct_1(sK1)
| l1_orders_2(sK0)
| ~ v3_struct_0(sK0)
| v1_funct_1(k2_waybel_1(sK0,sK0,sK1)) ),
inference(forward_subsumption_resolution,[],[f1975,f890]) ).
fof(f1991,plain,
( l1_orders_2(sK0)
| ~ v3_struct_0(sK0)
| v1_funct_1(k2_waybel_1(sK0,sK0,sK1)) ),
inference(forward_subsumption_resolution,[],[f1983,f421]) ).
fof(f1992,plain,
( ~ v3_struct_0(sK0)
| v1_funct_1(k2_waybel_1(sK0,sK0,sK1)) ),
inference(forward_subsumption_resolution,[],[f1991,f889]) ).
fof(f1993,plain,
v1_funct_1(k2_waybel_1(sK0,sK0,sK1)),
inference(forward_subsumption_resolution,[],[f1992,f1320]) ).
fof(f2032,plain,
( v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| l1_orders_2(sK0)
| ~ v3_struct_0(sK0)
| l1_orders_2(sK0)
| ~ v3_struct_0(sK0)
| v1_funct_1(k3_waybel_1(sK0,sK0,sK1)) ),
inference(resolution,[],[f989,f1341]) ).
fof(f2049,plain,
( v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| l1_orders_2(sK0)
| ~ v3_struct_0(sK0)
| v1_funct_1(k3_waybel_1(sK0,sK0,sK1)) ),
inference(duplicate_literal_removal,[],[f2032]) ).
fof(f2057,plain,
( ~ v1_funct_1(sK1)
| l1_orders_2(sK0)
| ~ v3_struct_0(sK0)
| v1_funct_1(k3_waybel_1(sK0,sK0,sK1)) ),
inference(forward_subsumption_resolution,[],[f2049,f890]) ).
fof(f2065,plain,
( l1_orders_2(sK0)
| ~ v3_struct_0(sK0)
| v1_funct_1(k3_waybel_1(sK0,sK0,sK1)) ),
inference(forward_subsumption_resolution,[],[f2057,f421]) ).
fof(f2066,plain,
( ~ v3_struct_0(sK0)
| v1_funct_1(k3_waybel_1(sK0,sK0,sK1)) ),
inference(forward_subsumption_resolution,[],[f2065,f889]) ).
fof(f2067,plain,
v1_funct_1(k3_waybel_1(sK0,sK0,sK1)),
inference(forward_subsumption_resolution,[],[f2066,f1320]) ).
fof(f2183,definition,
( spl33_29
<=> l1_orders_2(k2_yellow_2(sK0,sK0,sK1)) ),
introduced(definition,[new_symbols(definition,[spl33_29])],[avatar_definition]) ).
fof(f2185,plain,
( l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ spl33_29 ),
inference(avatar_component_clause,[],[f2183]) ).
fof(f2289,plain,
( ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| l1_orders_2(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ v3_struct_0(sK0)
| v4_orders_2(k2_yellow_2(sK0,sK0,sK1)) ),
inference(resolution,[],[f1005,f419]) ).
fof(f2297,plain,
( v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| l1_orders_2(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ v3_struct_0(sK0)
| v4_orders_2(k2_yellow_2(sK0,sK0,sK1)) ),
inference(forward_subsumption_resolution,[],[f2289,f1341]) ).
fof(f2301,plain,
( ~ v1_funct_1(sK1)
| l1_orders_2(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ v3_struct_0(sK0)
| v4_orders_2(k2_yellow_2(sK0,sK0,sK1)) ),
inference(forward_subsumption_resolution,[],[f2297,f890]) ).
fof(f2305,plain,
( l1_orders_2(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ v3_struct_0(sK0)
| v4_orders_2(k2_yellow_2(sK0,sK0,sK1)) ),
inference(forward_subsumption_resolution,[],[f2301,f421]) ).
fof(f2306,plain,
( ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ v3_struct_0(sK0)
| v4_orders_2(k2_yellow_2(sK0,sK0,sK1)) ),
inference(forward_subsumption_resolution,[],[f2305,f889]) ).
fof(f2307,plain,
( v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ v3_struct_0(sK0)
| v4_orders_2(k2_yellow_2(sK0,sK0,sK1)) ),
inference(forward_subsumption_resolution,[],[f2306,f429]) ).
fof(f2308,plain,
( v2_orders_2(sK0)
| ~ v3_struct_0(sK0)
| v4_orders_2(k2_yellow_2(sK0,sK0,sK1)) ),
inference(forward_subsumption_resolution,[],[f2307,f885]) ).
fof(f2309,plain,
( ~ v3_struct_0(sK0)
| v4_orders_2(k2_yellow_2(sK0,sK0,sK1)) ),
inference(forward_subsumption_resolution,[],[f2308,f884]) ).
fof(f2310,plain,
v4_orders_2(k2_yellow_2(sK0,sK0,sK1)),
inference(forward_subsumption_resolution,[],[f2309,f1320]) ).
fof(f2375,definition,
( spl33_35
<=> v2_orders_2(k2_yellow_2(sK0,sK0,sK1)) ),
introduced(definition,[new_symbols(definition,[spl33_35])],[avatar_definition]) ).
fof(f2376,plain,
( ~ v2_orders_2(k2_yellow_2(sK0,sK0,sK1))
| spl33_35 ),
inference(avatar_component_clause,[],[f2375]) ).
fof(f2377,plain,
( v2_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ spl33_35 ),
inference(avatar_component_clause,[],[f2375]) ).
fof(f2379,definition,
( spl33_36
<=> v3_orders_2(k2_yellow_2(sK0,sK0,sK1)) ),
introduced(definition,[new_symbols(definition,[spl33_36])],[avatar_definition]) ).
fof(f2381,plain,
( v3_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ spl33_36 ),
inference(avatar_component_clause,[],[f2379]) ).
fof(f2383,definition,
( spl33_37
<=> v1_lattice3(k2_yellow_2(sK0,sK0,sK1)) ),
introduced(definition,[new_symbols(definition,[spl33_37])],[avatar_definition]) ).
fof(f2385,plain,
( v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ spl33_37 ),
inference(avatar_component_clause,[],[f2383]) ).
fof(f2387,definition,
( spl33_38
<=> v2_lattice3(k2_yellow_2(sK0,sK0,sK1)) ),
introduced(definition,[new_symbols(definition,[spl33_38])],[avatar_definition]) ).
fof(f2389,plain,
( v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ spl33_38 ),
inference(avatar_component_clause,[],[f2387]) ).
fof(f2409,plain,
( ! [X0] :
( ~ m1_yellow_0(k2_yellow_2(sK0,sK0,sK1),X0)
| l1_orders_2(X0) )
| ~ spl33_29 ),
inference(resolution,[],[f2185,f995]) ).
fof(f2413,plain,
! [X2,X0,X1] :
( m1_relset_1(k2_waybel_1(X1,X2,X0),u1_struct_0(X1),u1_struct_0(k2_yellow_2(X1,X2,X0)))
| ~ v1_funct_1(X0)
| l1_orders_2(X2)
| ~ v3_struct_0(X2)
| l1_orders_2(X1)
| ~ v3_struct_0(X1)
| ~ 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(resolution,[],[f985,f867]) ).
fof(f2757,plain,
( ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| v2_lattice3(sK0)
| v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| v3_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ spl33_26 ),
inference(resolution,[],[f1022,f1951]) ).
fof(f2763,plain,
( v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| v2_lattice3(sK0)
| v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| v3_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ spl33_26 ),
inference(forward_subsumption_resolution,[],[f2757,f1341]) ).
fof(f2769,plain,
( ~ v1_funct_1(sK1)
| l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| v2_lattice3(sK0)
| v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| v3_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ spl33_26 ),
inference(forward_subsumption_resolution,[],[f2763,f890]) ).
fof(f2775,plain,
( l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| v2_lattice3(sK0)
| v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| v3_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ spl33_26 ),
inference(forward_subsumption_resolution,[],[f2769,f421]) ).
fof(f2781,plain,
( ~ v3_lattice3(sK0)
| v2_lattice3(sK0)
| v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| v3_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ spl33_26 ),
inference(forward_subsumption_resolution,[],[f2775,f889]) ).
fof(f2787,plain,
( v2_lattice3(sK0)
| v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| v3_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ spl33_26 ),
inference(forward_subsumption_resolution,[],[f2781,f426]) ).
fof(f2792,plain,
( v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| v3_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ spl33_26 ),
inference(forward_subsumption_resolution,[],[f2787,f887]) ).
fof(f2793,plain,
( ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| v3_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ spl33_26 ),
inference(forward_subsumption_resolution,[],[f2792,f886]) ).
fof(f2794,plain,
( v3_orders_2(sK0)
| v2_orders_2(sK0)
| v3_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ spl33_26 ),
inference(forward_subsumption_resolution,[],[f2793,f429]) ).
fof(f2795,plain,
( v2_orders_2(sK0)
| v3_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ spl33_26 ),
inference(forward_subsumption_resolution,[],[f2794,f885]) ).
fof(f2796,plain,
( v3_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ spl33_26 ),
inference(forward_subsumption_resolution,[],[f2795,f884]) ).
fof(f3048,plain,
( ~ v3_lattice3(sK0)
| v2_lattice3(sK0)
| v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| l1_orders_2(sK0)
| v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| k3_waybel_1(sK0,sK0,sK1) = k2_waybel34(k2_yellow_2(sK0,sK0,sK1),sK0,k2_waybel_1(sK0,sK0,sK1)) ),
inference(resolution,[],[f1284,f419]) ).
fof(f3056,plain,
( v2_lattice3(sK0)
| v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| l1_orders_2(sK0)
| v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| k3_waybel_1(sK0,sK0,sK1) = k2_waybel34(k2_yellow_2(sK0,sK0,sK1),sK0,k2_waybel_1(sK0,sK0,sK1)) ),
inference(forward_subsumption_resolution,[],[f3048,f426]) ).
fof(f3060,plain,
( v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| l1_orders_2(sK0)
| v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| k3_waybel_1(sK0,sK0,sK1) = k2_waybel34(k2_yellow_2(sK0,sK0,sK1),sK0,k2_waybel_1(sK0,sK0,sK1)) ),
inference(forward_subsumption_resolution,[],[f3056,f887]) ).
fof(f3064,plain,
( ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| l1_orders_2(sK0)
| v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| k3_waybel_1(sK0,sK0,sK1) = k2_waybel34(k2_yellow_2(sK0,sK0,sK1),sK0,k2_waybel_1(sK0,sK0,sK1)) ),
inference(forward_subsumption_resolution,[],[f3060,f886]) ).
fof(f3068,plain,
( v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| l1_orders_2(sK0)
| v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| k3_waybel_1(sK0,sK0,sK1) = k2_waybel34(k2_yellow_2(sK0,sK0,sK1),sK0,k2_waybel_1(sK0,sK0,sK1)) ),
inference(forward_subsumption_resolution,[],[f3064,f429]) ).
fof(f3070,plain,
( v2_orders_2(sK0)
| ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| l1_orders_2(sK0)
| v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| k3_waybel_1(sK0,sK0,sK1) = k2_waybel34(k2_yellow_2(sK0,sK0,sK1),sK0,k2_waybel_1(sK0,sK0,sK1)) ),
inference(forward_subsumption_resolution,[],[f3068,f885]) ).
fof(f3071,plain,
( ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| l1_orders_2(sK0)
| v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| k3_waybel_1(sK0,sK0,sK1) = k2_waybel34(k2_yellow_2(sK0,sK0,sK1),sK0,k2_waybel_1(sK0,sK0,sK1)) ),
inference(forward_subsumption_resolution,[],[f3070,f884]) ).
fof(f3072,plain,
( l1_orders_2(sK0)
| v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| k3_waybel_1(sK0,sK0,sK1) = k2_waybel34(k2_yellow_2(sK0,sK0,sK1),sK0,k2_waybel_1(sK0,sK0,sK1)) ),
inference(forward_subsumption_resolution,[],[f3071,f418]) ).
fof(f3073,plain,
( v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| k3_waybel_1(sK0,sK0,sK1) = k2_waybel34(k2_yellow_2(sK0,sK0,sK1),sK0,k2_waybel_1(sK0,sK0,sK1)) ),
inference(forward_subsumption_resolution,[],[f3072,f889]) ).
fof(f3074,plain,
( ~ v1_funct_1(sK1)
| k3_waybel_1(sK0,sK0,sK1) = k2_waybel34(k2_yellow_2(sK0,sK0,sK1),sK0,k2_waybel_1(sK0,sK0,sK1)) ),
inference(forward_subsumption_resolution,[],[f3073,f890]) ).
fof(f3075,plain,
k3_waybel_1(sK0,sK0,sK1) = k2_waybel34(k2_yellow_2(sK0,sK0,sK1),sK0,k2_waybel_1(sK0,sK0,sK1)),
inference(forward_subsumption_resolution,[],[f3074,f421]) ).
fof(f3077,plain,
( ~ v3_lattice3(sK0)
| v2_lattice3(sK0)
| v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| l1_orders_2(sK0)
| v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| k2_waybel_1(sK0,sK0,sK1) = k1_waybel34(k2_yellow_2(sK0,sK0,sK1),sK0,k3_waybel_1(sK0,sK0,sK1)) ),
inference(resolution,[],[f1285,f419]) ).
fof(f3085,plain,
( v2_lattice3(sK0)
| v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| l1_orders_2(sK0)
| v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| k2_waybel_1(sK0,sK0,sK1) = k1_waybel34(k2_yellow_2(sK0,sK0,sK1),sK0,k3_waybel_1(sK0,sK0,sK1)) ),
inference(forward_subsumption_resolution,[],[f3077,f426]) ).
fof(f3089,plain,
( v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| l1_orders_2(sK0)
| v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| k2_waybel_1(sK0,sK0,sK1) = k1_waybel34(k2_yellow_2(sK0,sK0,sK1),sK0,k3_waybel_1(sK0,sK0,sK1)) ),
inference(forward_subsumption_resolution,[],[f3085,f887]) ).
fof(f3093,plain,
( ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| l1_orders_2(sK0)
| v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| k2_waybel_1(sK0,sK0,sK1) = k1_waybel34(k2_yellow_2(sK0,sK0,sK1),sK0,k3_waybel_1(sK0,sK0,sK1)) ),
inference(forward_subsumption_resolution,[],[f3089,f886]) ).
fof(f3097,plain,
( v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| l1_orders_2(sK0)
| v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| k2_waybel_1(sK0,sK0,sK1) = k1_waybel34(k2_yellow_2(sK0,sK0,sK1),sK0,k3_waybel_1(sK0,sK0,sK1)) ),
inference(forward_subsumption_resolution,[],[f3093,f429]) ).
fof(f3099,plain,
( v2_orders_2(sK0)
| ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| l1_orders_2(sK0)
| v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| k2_waybel_1(sK0,sK0,sK1) = k1_waybel34(k2_yellow_2(sK0,sK0,sK1),sK0,k3_waybel_1(sK0,sK0,sK1)) ),
inference(forward_subsumption_resolution,[],[f3097,f885]) ).
fof(f3100,plain,
( ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| l1_orders_2(sK0)
| v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| k2_waybel_1(sK0,sK0,sK1) = k1_waybel34(k2_yellow_2(sK0,sK0,sK1),sK0,k3_waybel_1(sK0,sK0,sK1)) ),
inference(forward_subsumption_resolution,[],[f3099,f884]) ).
fof(f3101,plain,
( l1_orders_2(sK0)
| v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| k2_waybel_1(sK0,sK0,sK1) = k1_waybel34(k2_yellow_2(sK0,sK0,sK1),sK0,k3_waybel_1(sK0,sK0,sK1)) ),
inference(forward_subsumption_resolution,[],[f3100,f418]) ).
fof(f3102,plain,
( v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| k2_waybel_1(sK0,sK0,sK1) = k1_waybel34(k2_yellow_2(sK0,sK0,sK1),sK0,k3_waybel_1(sK0,sK0,sK1)) ),
inference(forward_subsumption_resolution,[],[f3101,f889]) ).
fof(f3103,plain,
( ~ v1_funct_1(sK1)
| k2_waybel_1(sK0,sK0,sK1) = k1_waybel34(k2_yellow_2(sK0,sK0,sK1),sK0,k3_waybel_1(sK0,sK0,sK1)) ),
inference(forward_subsumption_resolution,[],[f3102,f890]) ).
fof(f3104,plain,
k2_waybel_1(sK0,sK0,sK1) = k1_waybel34(k2_yellow_2(sK0,sK0,sK1),sK0,k3_waybel_1(sK0,sK0,sK1)),
inference(forward_subsumption_resolution,[],[f3103,f421]) ).
fof(f3702,plain,
( l1_orders_2(sK0)
| v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| l1_orders_2(sK0)
| ~ v3_struct_0(sK0)
| l1_orders_2(sK0)
| ~ v3_struct_0(sK0)
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl33_29 ),
inference(resolution,[],[f2409,f988]) ).
fof(f3703,plain,
( l1_orders_2(sK0)
| v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ v3_struct_0(sK0)
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl33_29 ),
inference(duplicate_literal_removal,[],[f3702]) ).
fof(f3704,plain,
( v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ v3_struct_0(sK0)
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl33_29 ),
inference(forward_subsumption_resolution,[],[f3703,f889]) ).
fof(f3705,plain,
( ~ v1_funct_1(sK1)
| ~ v3_struct_0(sK0)
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl33_29 ),
inference(forward_subsumption_resolution,[],[f3704,f890]) ).
fof(f3706,plain,
( ~ v3_struct_0(sK0)
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl33_29 ),
inference(forward_subsumption_resolution,[],[f3705,f421]) ).
fof(f3707,plain,
( ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl33_29 ),
inference(forward_subsumption_resolution,[],[f3706,f1320]) ).
fof(f3708,plain,
( $false
| ~ spl33_29 ),
inference(forward_subsumption_resolution,[],[f3707,f1341]) ).
fof(f3709,plain,
~ spl33_29,
inference(avatar_contradiction_clause,[],[f3708]) ).
fof(f3866,plain,
( ~ v7_waybel_1(sK1,sK0)
| v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| l1_orders_2(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ v3_struct_0(sK0)
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl33_35 ),
inference(resolution,[],[f2377,f1003]) ).
fof(f3870,plain,
( v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| l1_orders_2(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ v3_struct_0(sK0)
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl33_35 ),
inference(forward_subsumption_resolution,[],[f3866,f419]) ).
fof(f3872,plain,
( ~ v1_funct_1(sK1)
| l1_orders_2(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ v3_struct_0(sK0)
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl33_35 ),
inference(forward_subsumption_resolution,[],[f3870,f890]) ).
fof(f3874,plain,
( l1_orders_2(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ v3_struct_0(sK0)
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl33_35 ),
inference(forward_subsumption_resolution,[],[f3872,f421]) ).
fof(f3876,plain,
( ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ v3_struct_0(sK0)
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl33_35 ),
inference(forward_subsumption_resolution,[],[f3874,f889]) ).
fof(f3878,plain,
( v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ v3_struct_0(sK0)
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl33_35 ),
inference(forward_subsumption_resolution,[],[f3876,f429]) ).
fof(f3880,plain,
( v2_orders_2(sK0)
| ~ v3_struct_0(sK0)
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl33_35 ),
inference(forward_subsumption_resolution,[],[f3878,f885]) ).
fof(f3882,plain,
( ~ v3_struct_0(sK0)
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl33_35 ),
inference(forward_subsumption_resolution,[],[f3880,f884]) ).
fof(f3884,plain,
( ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl33_35 ),
inference(forward_subsumption_resolution,[],[f3882,f1320]) ).
fof(f3886,plain,
( $false
| ~ spl33_35 ),
inference(forward_subsumption_resolution,[],[f3884,f1341]) ).
fof(f3887,plain,
~ spl33_35,
inference(avatar_contradiction_clause,[],[f3886]) ).
fof(f3903,plain,
( ~ v1_funct_2(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| v1_funct_2(k2_waybel_1(sK0,sK0,sK1),u1_struct_0(sK0),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)))
| ~ v1_funct_1(k2_waybel_1(sK0,sK0,sK1))
| l1_orders_2(sK0)
| v2_lattice3(sK0)
| v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v4_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v3_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v2_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ m1_relset_1(k2_waybel_1(sK0,sK0,sK1),u1_struct_0(sK0),u1_struct_0(k2_yellow_2(sK0,sK0,sK1))) ),
inference(superposition,[],[f981,f3075]) ).
fof(f3904,plain,
( m2_relset_1(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| v1_funct_2(k2_waybel_1(sK0,sK0,sK1),u1_struct_0(sK0),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)))
| ~ v1_funct_1(k2_waybel_1(sK0,sK0,sK1))
| l1_orders_2(sK0)
| v2_lattice3(sK0)
| v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v4_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v3_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v2_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ m1_relset_1(k2_waybel_1(sK0,sK0,sK1),u1_struct_0(sK0),u1_struct_0(k2_yellow_2(sK0,sK0,sK1))) ),
inference(superposition,[],[f982,f3075]) ).
fof(f3906,plain,
( ~ v17_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| v18_waybel_0(k2_waybel_1(sK0,sK0,sK1),sK0,k2_yellow_2(sK0,sK0,sK1))
| v1_funct_2(k2_waybel_1(sK0,sK0,sK1),u1_struct_0(sK0),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)))
| ~ v1_funct_1(k2_waybel_1(sK0,sK0,sK1))
| l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| v2_lattice3(sK0)
| v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ v3_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v4_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v3_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v2_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ m1_relset_1(k2_waybel_1(sK0,sK0,sK1),u1_struct_0(sK0),u1_struct_0(k2_yellow_2(sK0,sK0,sK1))) ),
inference(superposition,[],[f1055,f3075]) ).
fof(f3913,plain,
( ~ v17_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| v18_waybel_0(k2_waybel_1(sK0,sK0,sK1),sK0,k2_yellow_2(sK0,sK0,sK1))
| v1_funct_2(k2_waybel_1(sK0,sK0,sK1),u1_struct_0(sK0),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)))
| l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| v2_lattice3(sK0)
| v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ v3_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v4_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v3_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v2_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ m1_relset_1(k2_waybel_1(sK0,sK0,sK1),u1_struct_0(sK0),u1_struct_0(k2_yellow_2(sK0,sK0,sK1))) ),
inference(forward_subsumption_resolution,[],[f3906,f1993]) ).
fof(f3915,plain,
( m2_relset_1(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| v1_funct_2(k2_waybel_1(sK0,sK0,sK1),u1_struct_0(sK0),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)))
| l1_orders_2(sK0)
| v2_lattice3(sK0)
| v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v4_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v3_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v2_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ m1_relset_1(k2_waybel_1(sK0,sK0,sK1),u1_struct_0(sK0),u1_struct_0(k2_yellow_2(sK0,sK0,sK1))) ),
inference(forward_subsumption_resolution,[],[f3904,f1993]) ).
fof(f3916,plain,
( ~ v1_funct_2(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| v1_funct_2(k2_waybel_1(sK0,sK0,sK1),u1_struct_0(sK0),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)))
| l1_orders_2(sK0)
| v2_lattice3(sK0)
| v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v4_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v3_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v2_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ m1_relset_1(k2_waybel_1(sK0,sK0,sK1),u1_struct_0(sK0),u1_struct_0(k2_yellow_2(sK0,sK0,sK1))) ),
inference(forward_subsumption_resolution,[],[f3903,f1993]) ).
fof(f3920,plain,
( ~ v17_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| v18_waybel_0(k2_waybel_1(sK0,sK0,sK1),sK0,k2_yellow_2(sK0,sK0,sK1))
| v1_funct_2(k2_waybel_1(sK0,sK0,sK1),u1_struct_0(sK0),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)))
| ~ v3_lattice3(sK0)
| v2_lattice3(sK0)
| v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ v3_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v4_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v3_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v2_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ m1_relset_1(k2_waybel_1(sK0,sK0,sK1),u1_struct_0(sK0),u1_struct_0(k2_yellow_2(sK0,sK0,sK1))) ),
inference(forward_subsumption_resolution,[],[f3913,f889]) ).
fof(f3922,plain,
( m2_relset_1(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| v1_funct_2(k2_waybel_1(sK0,sK0,sK1),u1_struct_0(sK0),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)))
| v2_lattice3(sK0)
| v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v4_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v3_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v2_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ m1_relset_1(k2_waybel_1(sK0,sK0,sK1),u1_struct_0(sK0),u1_struct_0(k2_yellow_2(sK0,sK0,sK1))) ),
inference(forward_subsumption_resolution,[],[f3915,f889]) ).
fof(f3923,plain,
( ~ v1_funct_2(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| v1_funct_2(k2_waybel_1(sK0,sK0,sK1),u1_struct_0(sK0),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)))
| v2_lattice3(sK0)
| v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v4_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v3_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v2_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ m1_relset_1(k2_waybel_1(sK0,sK0,sK1),u1_struct_0(sK0),u1_struct_0(k2_yellow_2(sK0,sK0,sK1))) ),
inference(forward_subsumption_resolution,[],[f3916,f889]) ).
fof(f3927,plain,
( ~ v17_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| v18_waybel_0(k2_waybel_1(sK0,sK0,sK1),sK0,k2_yellow_2(sK0,sK0,sK1))
| v1_funct_2(k2_waybel_1(sK0,sK0,sK1),u1_struct_0(sK0),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)))
| v2_lattice3(sK0)
| v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ v3_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v4_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v3_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v2_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ m1_relset_1(k2_waybel_1(sK0,sK0,sK1),u1_struct_0(sK0),u1_struct_0(k2_yellow_2(sK0,sK0,sK1))) ),
inference(forward_subsumption_resolution,[],[f3920,f426]) ).
fof(f3929,plain,
( m2_relset_1(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| v1_funct_2(k2_waybel_1(sK0,sK0,sK1),u1_struct_0(sK0),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)))
| v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v4_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v3_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v2_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ m1_relset_1(k2_waybel_1(sK0,sK0,sK1),u1_struct_0(sK0),u1_struct_0(k2_yellow_2(sK0,sK0,sK1))) ),
inference(forward_subsumption_resolution,[],[f3922,f887]) ).
fof(f3930,plain,
( ~ v1_funct_2(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| v1_funct_2(k2_waybel_1(sK0,sK0,sK1),u1_struct_0(sK0),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)))
| v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v4_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v3_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v2_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ m1_relset_1(k2_waybel_1(sK0,sK0,sK1),u1_struct_0(sK0),u1_struct_0(k2_yellow_2(sK0,sK0,sK1))) ),
inference(forward_subsumption_resolution,[],[f3923,f887]) ).
fof(f3934,plain,
( ~ v17_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| v18_waybel_0(k2_waybel_1(sK0,sK0,sK1),sK0,k2_yellow_2(sK0,sK0,sK1))
| v1_funct_2(k2_waybel_1(sK0,sK0,sK1),u1_struct_0(sK0),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)))
| v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ v3_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v4_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v3_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v2_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ m1_relset_1(k2_waybel_1(sK0,sK0,sK1),u1_struct_0(sK0),u1_struct_0(k2_yellow_2(sK0,sK0,sK1))) ),
inference(forward_subsumption_resolution,[],[f3927,f887]) ).
fof(f3936,plain,
( m2_relset_1(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| v1_funct_2(k2_waybel_1(sK0,sK0,sK1),u1_struct_0(sK0),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)))
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v4_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v3_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v2_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ m1_relset_1(k2_waybel_1(sK0,sK0,sK1),u1_struct_0(sK0),u1_struct_0(k2_yellow_2(sK0,sK0,sK1))) ),
inference(forward_subsumption_resolution,[],[f3929,f886]) ).
fof(f3937,plain,
( ~ v1_funct_2(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| v1_funct_2(k2_waybel_1(sK0,sK0,sK1),u1_struct_0(sK0),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)))
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v4_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v3_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v2_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ m1_relset_1(k2_waybel_1(sK0,sK0,sK1),u1_struct_0(sK0),u1_struct_0(k2_yellow_2(sK0,sK0,sK1))) ),
inference(forward_subsumption_resolution,[],[f3930,f886]) ).
fof(f3941,plain,
( ~ v17_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| v18_waybel_0(k2_waybel_1(sK0,sK0,sK1),sK0,k2_yellow_2(sK0,sK0,sK1))
| v1_funct_2(k2_waybel_1(sK0,sK0,sK1),u1_struct_0(sK0),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)))
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ v3_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v4_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v3_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v2_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ m1_relset_1(k2_waybel_1(sK0,sK0,sK1),u1_struct_0(sK0),u1_struct_0(k2_yellow_2(sK0,sK0,sK1))) ),
inference(forward_subsumption_resolution,[],[f3934,f886]) ).
fof(f3943,plain,
( m2_relset_1(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| v1_funct_2(k2_waybel_1(sK0,sK0,sK1),u1_struct_0(sK0),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)))
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v4_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v3_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v2_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ m1_relset_1(k2_waybel_1(sK0,sK0,sK1),u1_struct_0(sK0),u1_struct_0(k2_yellow_2(sK0,sK0,sK1))) ),
inference(forward_subsumption_resolution,[],[f3936,f429]) ).
fof(f3944,plain,
( ~ v1_funct_2(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| v1_funct_2(k2_waybel_1(sK0,sK0,sK1),u1_struct_0(sK0),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)))
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v4_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v3_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v2_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ m1_relset_1(k2_waybel_1(sK0,sK0,sK1),u1_struct_0(sK0),u1_struct_0(k2_yellow_2(sK0,sK0,sK1))) ),
inference(forward_subsumption_resolution,[],[f3937,f429]) ).
fof(f3948,plain,
( ~ v17_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| v18_waybel_0(k2_waybel_1(sK0,sK0,sK1),sK0,k2_yellow_2(sK0,sK0,sK1))
| v1_funct_2(k2_waybel_1(sK0,sK0,sK1),u1_struct_0(sK0),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)))
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ v3_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v4_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v3_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v2_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ m1_relset_1(k2_waybel_1(sK0,sK0,sK1),u1_struct_0(sK0),u1_struct_0(k2_yellow_2(sK0,sK0,sK1))) ),
inference(forward_subsumption_resolution,[],[f3941,f429]) ).
fof(f3950,plain,
( m2_relset_1(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| v1_funct_2(k2_waybel_1(sK0,sK0,sK1),u1_struct_0(sK0),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)))
| v2_orders_2(sK0)
| l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v4_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v3_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v2_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ m1_relset_1(k2_waybel_1(sK0,sK0,sK1),u1_struct_0(sK0),u1_struct_0(k2_yellow_2(sK0,sK0,sK1))) ),
inference(forward_subsumption_resolution,[],[f3943,f885]) ).
fof(f3951,plain,
( ~ v1_funct_2(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| v1_funct_2(k2_waybel_1(sK0,sK0,sK1),u1_struct_0(sK0),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)))
| v2_orders_2(sK0)
| l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v4_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v3_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v2_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ m1_relset_1(k2_waybel_1(sK0,sK0,sK1),u1_struct_0(sK0),u1_struct_0(k2_yellow_2(sK0,sK0,sK1))) ),
inference(forward_subsumption_resolution,[],[f3944,f885]) ).
fof(f3955,plain,
( ~ v17_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| v18_waybel_0(k2_waybel_1(sK0,sK0,sK1),sK0,k2_yellow_2(sK0,sK0,sK1))
| v1_funct_2(k2_waybel_1(sK0,sK0,sK1),u1_struct_0(sK0),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)))
| v2_orders_2(sK0)
| l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ v3_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v4_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v3_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v2_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ m1_relset_1(k2_waybel_1(sK0,sK0,sK1),u1_struct_0(sK0),u1_struct_0(k2_yellow_2(sK0,sK0,sK1))) ),
inference(forward_subsumption_resolution,[],[f3948,f885]) ).
fof(f3957,plain,
( m2_relset_1(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| v1_funct_2(k2_waybel_1(sK0,sK0,sK1),u1_struct_0(sK0),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)))
| l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v4_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v3_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v2_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ m1_relset_1(k2_waybel_1(sK0,sK0,sK1),u1_struct_0(sK0),u1_struct_0(k2_yellow_2(sK0,sK0,sK1))) ),
inference(forward_subsumption_resolution,[],[f3950,f884]) ).
fof(f3958,plain,
( ~ v1_funct_2(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| v1_funct_2(k2_waybel_1(sK0,sK0,sK1),u1_struct_0(sK0),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)))
| l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v4_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v3_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v2_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ m1_relset_1(k2_waybel_1(sK0,sK0,sK1),u1_struct_0(sK0),u1_struct_0(k2_yellow_2(sK0,sK0,sK1))) ),
inference(forward_subsumption_resolution,[],[f3951,f884]) ).
fof(f3962,plain,
( ~ v17_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| v18_waybel_0(k2_waybel_1(sK0,sK0,sK1),sK0,k2_yellow_2(sK0,sK0,sK1))
| v1_funct_2(k2_waybel_1(sK0,sK0,sK1),u1_struct_0(sK0),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)))
| l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ v3_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v4_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v3_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v2_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ m1_relset_1(k2_waybel_1(sK0,sK0,sK1),u1_struct_0(sK0),u1_struct_0(k2_yellow_2(sK0,sK0,sK1))) ),
inference(forward_subsumption_resolution,[],[f3955,f884]) ).
fof(f3964,plain,
( m2_relset_1(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| v1_funct_2(k2_waybel_1(sK0,sK0,sK1),u1_struct_0(sK0),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)))
| l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v3_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v2_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ m1_relset_1(k2_waybel_1(sK0,sK0,sK1),u1_struct_0(sK0),u1_struct_0(k2_yellow_2(sK0,sK0,sK1))) ),
inference(forward_subsumption_resolution,[],[f3957,f2310]) ).
fof(f3965,plain,
( ~ v1_funct_2(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| v1_funct_2(k2_waybel_1(sK0,sK0,sK1),u1_struct_0(sK0),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)))
| l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v3_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v2_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ m1_relset_1(k2_waybel_1(sK0,sK0,sK1),u1_struct_0(sK0),u1_struct_0(k2_yellow_2(sK0,sK0,sK1))) ),
inference(forward_subsumption_resolution,[],[f3958,f2310]) ).
fof(f3969,plain,
( ~ v17_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| v18_waybel_0(k2_waybel_1(sK0,sK0,sK1),sK0,k2_yellow_2(sK0,sK0,sK1))
| v1_funct_2(k2_waybel_1(sK0,sK0,sK1),u1_struct_0(sK0),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)))
| l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v4_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v3_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v2_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ m1_relset_1(k2_waybel_1(sK0,sK0,sK1),u1_struct_0(sK0),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)))
| ~ spl33_26 ),
inference(forward_subsumption_resolution,[],[f3962,f2796]) ).
fof(f3972,definition,
( spl33_86
<=> m1_relset_1(k2_waybel_1(sK0,sK0,sK1),u1_struct_0(sK0),u1_struct_0(k2_yellow_2(sK0,sK0,sK1))) ),
introduced(definition,[new_symbols(definition,[spl33_86])],[avatar_definition]) ).
fof(f3974,plain,
( ~ m1_relset_1(k2_waybel_1(sK0,sK0,sK1),u1_struct_0(sK0),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)))
| spl33_86 ),
inference(avatar_component_clause,[],[f3972]) ).
fof(f3976,definition,
( spl33_87
<=> v1_funct_2(k2_waybel_1(sK0,sK0,sK1),u1_struct_0(sK0),u1_struct_0(k2_yellow_2(sK0,sK0,sK1))) ),
introduced(definition,[new_symbols(definition,[spl33_87])],[avatar_definition]) ).
fof(f3978,plain,
( v1_funct_2(k2_waybel_1(sK0,sK0,sK1),u1_struct_0(sK0),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)))
| ~ spl33_87 ),
inference(avatar_component_clause,[],[f3976]) ).
fof(f3980,definition,
( spl33_88
<=> m2_relset_1(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0)) ),
introduced(definition,[new_symbols(definition,[spl33_88])],[avatar_definition]) ).
fof(f3983,plain,
( ~ spl33_86
| spl33_35
| spl33_36
| spl33_37
| spl33_38
| spl33_29
| spl33_87
| spl33_88 ),
inference(avatar_split_clause,[],[f3964,f3980,f3976,f2183,f2387,f2383,f2379,f2375,f3972]) ).
fof(f3985,definition,
( spl33_89
<=> v1_funct_2(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0)) ),
introduced(definition,[new_symbols(definition,[spl33_89])],[avatar_definition]) ).
fof(f3988,plain,
( ~ spl33_86
| spl33_35
| spl33_36
| spl33_37
| spl33_38
| spl33_29
| spl33_87
| ~ spl33_89 ),
inference(avatar_split_clause,[],[f3965,f3985,f3976,f2183,f2387,f2383,f2379,f2375,f3972]) ).
fof(f3992,plain,
( ~ v17_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| v18_waybel_0(k2_waybel_1(sK0,sK0,sK1),sK0,k2_yellow_2(sK0,sK0,sK1))
| v1_funct_2(k2_waybel_1(sK0,sK0,sK1),u1_struct_0(sK0),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)))
| l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v3_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v2_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ m1_relset_1(k2_waybel_1(sK0,sK0,sK1),u1_struct_0(sK0),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)))
| ~ spl33_26 ),
inference(forward_subsumption_resolution,[],[f3969,f2310]) ).
fof(f3995,definition,
( spl33_90
<=> v18_waybel_0(k2_waybel_1(sK0,sK0,sK1),sK0,k2_yellow_2(sK0,sK0,sK1)) ),
introduced(definition,[new_symbols(definition,[spl33_90])],[avatar_definition]) ).
fof(f3997,plain,
( v18_waybel_0(k2_waybel_1(sK0,sK0,sK1),sK0,k2_yellow_2(sK0,sK0,sK1))
| ~ spl33_90 ),
inference(avatar_component_clause,[],[f3995]) ).
fof(f4014,definition,
( spl33_94
<=> v17_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0) ),
introduced(definition,[new_symbols(definition,[spl33_94])],[avatar_definition]) ).
fof(f4017,plain,
( ~ spl33_86
| spl33_35
| spl33_36
| spl33_37
| spl33_38
| spl33_29
| spl33_87
| spl33_90
| ~ spl33_94
| ~ spl33_26 ),
inference(avatar_split_clause,[],[f3992,f1949,f4014,f3995,f3976,f2183,f2387,f2383,f2379,f2375,f3972]) ).
fof(f4021,plain,
( ~ v7_waybel_1(sK1,sK0)
| v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| l1_orders_2(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ v3_struct_0(sK0)
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl33_36 ),
inference(resolution,[],[f2381,f1004]) ).
fof(f4025,plain,
( v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| l1_orders_2(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ v3_struct_0(sK0)
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl33_36 ),
inference(forward_subsumption_resolution,[],[f4021,f419]) ).
fof(f4027,plain,
( ~ v1_funct_1(sK1)
| l1_orders_2(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ v3_struct_0(sK0)
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl33_36 ),
inference(forward_subsumption_resolution,[],[f4025,f890]) ).
fof(f4029,plain,
( l1_orders_2(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ v3_struct_0(sK0)
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl33_36 ),
inference(forward_subsumption_resolution,[],[f4027,f421]) ).
fof(f4031,plain,
( ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ v3_struct_0(sK0)
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl33_36 ),
inference(forward_subsumption_resolution,[],[f4029,f889]) ).
fof(f4033,plain,
( v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ v3_struct_0(sK0)
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl33_36 ),
inference(forward_subsumption_resolution,[],[f4031,f429]) ).
fof(f4035,plain,
( v2_orders_2(sK0)
| ~ v3_struct_0(sK0)
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl33_36 ),
inference(forward_subsumption_resolution,[],[f4033,f885]) ).
fof(f4037,plain,
( ~ v3_struct_0(sK0)
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl33_36 ),
inference(forward_subsumption_resolution,[],[f4035,f884]) ).
fof(f4039,plain,
( ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl33_36 ),
inference(forward_subsumption_resolution,[],[f4037,f1320]) ).
fof(f4041,plain,
( $false
| ~ spl33_36 ),
inference(forward_subsumption_resolution,[],[f4039,f1341]) ).
fof(f4042,plain,
~ spl33_36,
inference(avatar_contradiction_clause,[],[f4041]) ).
fof(f4054,plain,
( ~ v1_waybel34(k2_waybel_1(sK0,sK0,sK1),sK0,k2_yellow_2(sK0,sK0,sK1))
| ~ v3_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v4_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v3_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v2_orders_2(k2_yellow_2(sK0,sK0,sK1))
| l1_orders_2(sK0)
| v3_waybel_3(sK0)
| ~ v3_lattice3(sK0)
| v2_lattice3(sK0)
| v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m2_relset_1(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| v17_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| v1_funct_2(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_1(k3_waybel_1(sK0,sK0,sK1))
| l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v22_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0) ),
inference(superposition,[],[f1280,f3104]) ).
fof(f4055,plain,
( ~ v3_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v4_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v3_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v2_orders_2(k2_yellow_2(sK0,sK0,sK1))
| l1_orders_2(sK0)
| v3_waybel_3(sK0)
| ~ v3_lattice3(sK0)
| v2_lattice3(sK0)
| v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m2_relset_1(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| v17_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| v1_funct_2(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_1(k3_waybel_1(sK0,sK0,sK1))
| l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v22_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0) ),
inference(forward_subsumption_resolution,[],[f4054,f422]) ).
fof(f4063,plain,
( v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v4_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v3_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v2_orders_2(k2_yellow_2(sK0,sK0,sK1))
| l1_orders_2(sK0)
| v3_waybel_3(sK0)
| ~ v3_lattice3(sK0)
| v2_lattice3(sK0)
| v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m2_relset_1(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| v17_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| v1_funct_2(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_1(k3_waybel_1(sK0,sK0,sK1))
| l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v22_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ spl33_26 ),
inference(forward_subsumption_resolution,[],[f4055,f2796]) ).
fof(f4071,plain,
( v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v3_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v2_orders_2(k2_yellow_2(sK0,sK0,sK1))
| l1_orders_2(sK0)
| v3_waybel_3(sK0)
| ~ v3_lattice3(sK0)
| v2_lattice3(sK0)
| v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m2_relset_1(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| v17_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| v1_funct_2(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_1(k3_waybel_1(sK0,sK0,sK1))
| l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v22_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ spl33_26 ),
inference(forward_subsumption_resolution,[],[f4063,f2310]) ).
fof(f4079,plain,
( v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v3_orders_2(k2_yellow_2(sK0,sK0,sK1))
| l1_orders_2(sK0)
| v3_waybel_3(sK0)
| ~ v3_lattice3(sK0)
| v2_lattice3(sK0)
| v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m2_relset_1(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| v17_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| v1_funct_2(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_1(k3_waybel_1(sK0,sK0,sK1))
| l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v22_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ spl33_26
| spl33_35 ),
inference(forward_subsumption_resolution,[],[f4071,f2376]) ).
fof(f4087,plain,
( v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v3_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v3_waybel_3(sK0)
| ~ v3_lattice3(sK0)
| v2_lattice3(sK0)
| v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m2_relset_1(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| v17_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| v1_funct_2(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_1(k3_waybel_1(sK0,sK0,sK1))
| l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v22_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ spl33_26
| spl33_35 ),
inference(forward_subsumption_resolution,[],[f4079,f889]) ).
fof(f4095,plain,
( v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v3_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ v3_lattice3(sK0)
| v2_lattice3(sK0)
| v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m2_relset_1(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| v17_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| v1_funct_2(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_1(k3_waybel_1(sK0,sK0,sK1))
| l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v22_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ spl33_26
| spl33_35 ),
inference(forward_subsumption_resolution,[],[f4087,f888]) ).
fof(f4103,plain,
( v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v3_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v2_lattice3(sK0)
| v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m2_relset_1(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| v17_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| v1_funct_2(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_1(k3_waybel_1(sK0,sK0,sK1))
| l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v22_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ spl33_26
| spl33_35 ),
inference(forward_subsumption_resolution,[],[f4095,f426]) ).
fof(f4111,plain,
( v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v3_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m2_relset_1(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| v17_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| v1_funct_2(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_1(k3_waybel_1(sK0,sK0,sK1))
| l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v22_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ spl33_26
| spl33_35 ),
inference(forward_subsumption_resolution,[],[f4103,f887]) ).
fof(f4119,plain,
( v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v3_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m2_relset_1(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| v17_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| v1_funct_2(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_1(k3_waybel_1(sK0,sK0,sK1))
| l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v22_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ spl33_26
| spl33_35 ),
inference(forward_subsumption_resolution,[],[f4111,f886]) ).
fof(f4127,plain,
( v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v3_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m2_relset_1(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| v17_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| v1_funct_2(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_1(k3_waybel_1(sK0,sK0,sK1))
| l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v22_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ spl33_26
| spl33_35 ),
inference(forward_subsumption_resolution,[],[f4119,f429]) ).
fof(f4143,plain,
( v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v3_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v2_orders_2(sK0)
| ~ m2_relset_1(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| v17_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| v1_funct_2(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_1(k3_waybel_1(sK0,sK0,sK1))
| l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v22_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ spl33_26
| spl33_35 ),
inference(forward_subsumption_resolution,[],[f4127,f885]) ).
fof(f4149,plain,
( v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v3_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ m2_relset_1(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| v17_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| v1_funct_2(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_1(k3_waybel_1(sK0,sK0,sK1))
| l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v22_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ spl33_26
| spl33_35 ),
inference(forward_subsumption_resolution,[],[f4143,f884]) ).
fof(f4167,plain,
( v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v3_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ m2_relset_1(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| v17_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| v1_funct_2(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| v22_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ spl33_26
| spl33_35 ),
inference(forward_subsumption_resolution,[],[f4149,f2067]) ).
fof(f4169,definition,
( spl33_100
<=> v22_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0) ),
introduced(definition,[new_symbols(definition,[spl33_100])],[avatar_definition]) ).
fof(f4171,plain,
( v22_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ spl33_100 ),
inference(avatar_component_clause,[],[f4169]) ).
fof(f4172,plain,
( spl33_100
| spl33_29
| spl33_89
| spl33_94
| ~ spl33_88
| spl33_36
| spl33_37
| spl33_38
| ~ spl33_26
| spl33_35 ),
inference(avatar_split_clause,[],[f4167,f2375,f1949,f2387,f2383,f2379,f3980,f4014,f3985,f2183,f4169]) ).
fof(f4244,plain,
( ~ v6_waybel_1(sK1,sK0)
| v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| v2_lattice3(sK0)
| v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl33_37 ),
inference(resolution,[],[f2385,f1020]) ).
fof(f4251,plain,
( v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| v2_lattice3(sK0)
| v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl33_26
| ~ spl33_37 ),
inference(forward_subsumption_resolution,[],[f4244,f1951]) ).
fof(f4254,plain,
( ~ v1_funct_1(sK1)
| l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| v2_lattice3(sK0)
| v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl33_26
| ~ spl33_37 ),
inference(forward_subsumption_resolution,[],[f4251,f890]) ).
fof(f4257,plain,
( l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| v2_lattice3(sK0)
| v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl33_26
| ~ spl33_37 ),
inference(forward_subsumption_resolution,[],[f4254,f421]) ).
fof(f4259,plain,
( ~ v3_lattice3(sK0)
| v2_lattice3(sK0)
| v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl33_26
| ~ spl33_37 ),
inference(forward_subsumption_resolution,[],[f4257,f889]) ).
fof(f4261,plain,
( v2_lattice3(sK0)
| v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl33_26
| ~ spl33_37 ),
inference(forward_subsumption_resolution,[],[f4259,f426]) ).
fof(f4263,plain,
( v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl33_26
| ~ spl33_37 ),
inference(forward_subsumption_resolution,[],[f4261,f887]) ).
fof(f4264,plain,
( ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl33_26
| ~ spl33_37 ),
inference(forward_subsumption_resolution,[],[f4263,f886]) ).
fof(f4265,plain,
( v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl33_26
| ~ spl33_37 ),
inference(forward_subsumption_resolution,[],[f4264,f429]) ).
fof(f4266,plain,
( v2_orders_2(sK0)
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl33_26
| ~ spl33_37 ),
inference(forward_subsumption_resolution,[],[f4265,f885]) ).
fof(f4267,plain,
( ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl33_26
| ~ spl33_37 ),
inference(forward_subsumption_resolution,[],[f4266,f884]) ).
fof(f4268,plain,
( $false
| ~ spl33_26
| ~ spl33_37 ),
inference(forward_subsumption_resolution,[],[f4267,f1341]) ).
fof(f4269,plain,
( ~ spl33_26
| ~ spl33_37 ),
inference(avatar_contradiction_clause,[],[f4268]) ).
fof(f4302,plain,
( ~ v6_waybel_1(sK1,sK0)
| v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| v2_lattice3(sK0)
| v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl33_38 ),
inference(resolution,[],[f2389,f1021]) ).
fof(f4313,plain,
( v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| v2_lattice3(sK0)
| v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl33_26
| ~ spl33_38 ),
inference(forward_subsumption_resolution,[],[f4302,f1951]) ).
fof(f4317,plain,
( ~ v1_funct_1(sK1)
| l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| v2_lattice3(sK0)
| v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl33_26
| ~ spl33_38 ),
inference(forward_subsumption_resolution,[],[f4313,f890]) ).
fof(f4321,plain,
( l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| v2_lattice3(sK0)
| v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl33_26
| ~ spl33_38 ),
inference(forward_subsumption_resolution,[],[f4317,f421]) ).
fof(f4324,plain,
( ~ v3_lattice3(sK0)
| v2_lattice3(sK0)
| v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl33_26
| ~ spl33_38 ),
inference(forward_subsumption_resolution,[],[f4321,f889]) ).
fof(f4327,plain,
( v2_lattice3(sK0)
| v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl33_26
| ~ spl33_38 ),
inference(forward_subsumption_resolution,[],[f4324,f426]) ).
fof(f4329,plain,
( v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl33_26
| ~ spl33_38 ),
inference(forward_subsumption_resolution,[],[f4327,f887]) ).
fof(f4331,plain,
( ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl33_26
| ~ spl33_38 ),
inference(forward_subsumption_resolution,[],[f4329,f886]) ).
fof(f4332,plain,
( v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl33_26
| ~ spl33_38 ),
inference(forward_subsumption_resolution,[],[f4331,f429]) ).
fof(f4333,plain,
( v2_orders_2(sK0)
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl33_26
| ~ spl33_38 ),
inference(forward_subsumption_resolution,[],[f4332,f885]) ).
fof(f4334,plain,
( ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl33_26
| ~ spl33_38 ),
inference(forward_subsumption_resolution,[],[f4333,f884]) ).
fof(f4335,plain,
( $false
| ~ spl33_26
| ~ spl33_38 ),
inference(forward_subsumption_resolution,[],[f4334,f1341]) ).
fof(f4336,plain,
( ~ spl33_26
| ~ spl33_38 ),
inference(avatar_contradiction_clause,[],[f4335]) ).
fof(f16818,plain,
( ~ v1_funct_1(sK1)
| l1_orders_2(sK0)
| ~ v3_struct_0(sK0)
| l1_orders_2(sK0)
| ~ v3_struct_0(sK0)
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| spl33_86 ),
inference(resolution,[],[f3974,f2413]) ).
fof(f16819,plain,
( ~ v1_funct_1(sK1)
| l1_orders_2(sK0)
| ~ v3_struct_0(sK0)
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| spl33_86 ),
inference(duplicate_literal_removal,[],[f16818]) ).
fof(f16820,plain,
( l1_orders_2(sK0)
| ~ v3_struct_0(sK0)
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| spl33_86 ),
inference(forward_subsumption_resolution,[],[f16819,f421]) ).
fof(f16821,plain,
( ~ v3_struct_0(sK0)
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| spl33_86 ),
inference(forward_subsumption_resolution,[],[f16820,f889]) ).
fof(f16822,plain,
( ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| spl33_86 ),
inference(forward_subsumption_resolution,[],[f16821,f1320]) ).
fof(f16823,plain,
( v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| spl33_86 ),
inference(forward_subsumption_resolution,[],[f16822,f1341]) ).
fof(f16824,plain,
( $false
| spl33_86 ),
inference(forward_subsumption_resolution,[],[f16823,f890]) ).
fof(f16825,plain,
spl33_86,
inference(avatar_contradiction_clause,[],[f16824]) ).
fof(f16921,plain,
( v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| l1_orders_2(sK0)
| ~ v3_struct_0(sK0)
| l1_orders_2(sK0)
| ~ v3_struct_0(sK0)
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl33_87 ),
inference(resolution,[],[f3978,f984]) ).
fof(f16922,plain,
( v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| l1_orders_2(sK0)
| ~ v3_struct_0(sK0)
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl33_87 ),
inference(duplicate_literal_removal,[],[f16921]) ).
fof(f16923,plain,
( ~ v1_funct_1(sK1)
| l1_orders_2(sK0)
| ~ v3_struct_0(sK0)
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl33_87 ),
inference(forward_subsumption_resolution,[],[f16922,f890]) ).
fof(f16924,plain,
( l1_orders_2(sK0)
| ~ v3_struct_0(sK0)
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl33_87 ),
inference(forward_subsumption_resolution,[],[f16923,f421]) ).
fof(f16925,plain,
( ~ v3_struct_0(sK0)
| ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl33_87 ),
inference(forward_subsumption_resolution,[],[f16924,f889]) ).
fof(f16926,plain,
( ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl33_87 ),
inference(forward_subsumption_resolution,[],[f16925,f1320]) ).
fof(f16927,plain,
( $false
| ~ spl33_87 ),
inference(forward_subsumption_resolution,[],[f16926,f1341]) ).
fof(f16928,plain,
~ spl33_87,
inference(avatar_contradiction_clause,[],[f16927]) ).
fof(f16929,plain,
( ~ v3_lattice3(sK0)
| v2_lattice3(sK0)
| v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v7_waybel_1(sK1,sK0)
| v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| l1_orders_2(sK0)
| ~ spl33_90 ),
inference(resolution,[],[f3997,f1282]) ).
fof(f16930,plain,
( v2_lattice3(sK0)
| v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v7_waybel_1(sK1,sK0)
| v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| l1_orders_2(sK0)
| ~ spl33_90 ),
inference(forward_subsumption_resolution,[],[f16929,f426]) ).
fof(f16931,plain,
( v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v7_waybel_1(sK1,sK0)
| v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| l1_orders_2(sK0)
| ~ spl33_90 ),
inference(forward_subsumption_resolution,[],[f16930,f887]) ).
fof(f16932,plain,
( ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v7_waybel_1(sK1,sK0)
| v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| l1_orders_2(sK0)
| ~ spl33_90 ),
inference(forward_subsumption_resolution,[],[f16931,f886]) ).
fof(f16933,plain,
( v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v7_waybel_1(sK1,sK0)
| v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| l1_orders_2(sK0)
| ~ spl33_90 ),
inference(forward_subsumption_resolution,[],[f16932,f429]) ).
fof(f16934,plain,
( v2_orders_2(sK0)
| ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v7_waybel_1(sK1,sK0)
| v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| l1_orders_2(sK0)
| ~ spl33_90 ),
inference(forward_subsumption_resolution,[],[f16933,f885]) ).
fof(f16935,plain,
( ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v7_waybel_1(sK1,sK0)
| v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| l1_orders_2(sK0)
| ~ spl33_90 ),
inference(forward_subsumption_resolution,[],[f16934,f884]) ).
fof(f16936,plain,
( ~ v7_waybel_1(sK1,sK0)
| v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| l1_orders_2(sK0)
| ~ spl33_90 ),
inference(forward_subsumption_resolution,[],[f16935,f418]) ).
fof(f16937,plain,
( v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| l1_orders_2(sK0)
| ~ spl33_90 ),
inference(forward_subsumption_resolution,[],[f16936,f419]) ).
fof(f16938,plain,
( ~ v1_funct_1(sK1)
| l1_orders_2(sK0)
| ~ spl33_90 ),
inference(forward_subsumption_resolution,[],[f16937,f890]) ).
fof(f16939,plain,
( l1_orders_2(sK0)
| ~ spl33_90 ),
inference(forward_subsumption_resolution,[],[f16938,f421]) ).
fof(f16940,plain,
( $false
| ~ spl33_90 ),
inference(forward_subsumption_resolution,[],[f16939,f889]) ).
fof(f16941,plain,
~ spl33_90,
inference(avatar_contradiction_clause,[],[f16940]) ).
fof(f16990,plain,
( ~ v3_lattice3(sK0)
| v2_lattice3(sK0)
| v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v7_waybel_1(sK1,sK0)
| v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| l1_orders_2(sK0)
| v4_waybel_0(k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ spl33_100 ),
inference(resolution,[],[f4171,f1288]) ).
fof(f16992,plain,
( v2_lattice3(sK0)
| v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v7_waybel_1(sK1,sK0)
| v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| l1_orders_2(sK0)
| v4_waybel_0(k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ spl33_100 ),
inference(forward_subsumption_resolution,[],[f16990,f426]) ).
fof(f16993,plain,
( v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v7_waybel_1(sK1,sK0)
| v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| l1_orders_2(sK0)
| v4_waybel_0(k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ spl33_100 ),
inference(forward_subsumption_resolution,[],[f16992,f887]) ).
fof(f16994,plain,
( ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v7_waybel_1(sK1,sK0)
| v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| l1_orders_2(sK0)
| v4_waybel_0(k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ spl33_100 ),
inference(forward_subsumption_resolution,[],[f16993,f886]) ).
fof(f16995,plain,
( v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v7_waybel_1(sK1,sK0)
| v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| l1_orders_2(sK0)
| v4_waybel_0(k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ spl33_100 ),
inference(forward_subsumption_resolution,[],[f16994,f429]) ).
fof(f16996,plain,
( v2_orders_2(sK0)
| ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v7_waybel_1(sK1,sK0)
| v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| l1_orders_2(sK0)
| v4_waybel_0(k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ spl33_100 ),
inference(forward_subsumption_resolution,[],[f16995,f885]) ).
fof(f16997,plain,
( ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v7_waybel_1(sK1,sK0)
| v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| l1_orders_2(sK0)
| v4_waybel_0(k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ spl33_100 ),
inference(forward_subsumption_resolution,[],[f16996,f884]) ).
fof(f16998,plain,
( ~ v7_waybel_1(sK1,sK0)
| v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| l1_orders_2(sK0)
| v4_waybel_0(k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ spl33_100 ),
inference(forward_subsumption_resolution,[],[f16997,f418]) ).
fof(f16999,plain,
( v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| l1_orders_2(sK0)
| v4_waybel_0(k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ spl33_100 ),
inference(forward_subsumption_resolution,[],[f16998,f419]) ).
fof(f17000,plain,
( ~ v1_funct_1(sK1)
| l1_orders_2(sK0)
| v4_waybel_0(k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ spl33_100 ),
inference(forward_subsumption_resolution,[],[f16999,f890]) ).
fof(f17001,plain,
( l1_orders_2(sK0)
| v4_waybel_0(k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ spl33_100 ),
inference(forward_subsumption_resolution,[],[f17000,f421]) ).
fof(f17002,plain,
( v4_waybel_0(k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ spl33_100 ),
inference(forward_subsumption_resolution,[],[f17001,f889]) ).
fof(f17003,plain,
( $false
| ~ spl33_100 ),
inference(forward_subsumption_resolution,[],[f17002,f423]) ).
fof(f17004,plain,
~ spl33_100,
inference(avatar_contradiction_clause,[],[f17003]) ).
cnf(s23,plain,
spl33_26,
inference(sat_conversion,[],[f1957]) ).
cnf(s48,plain,
~ spl33_29,
inference(sat_conversion,[],[f3709]) ).
cnf(s76,plain,
~ spl33_35,
inference(sat_conversion,[],[f3887]) ).
cnf(s79,plain,
( spl33_29
| spl33_35
| spl33_36
| spl33_37
| spl33_38
| ~ spl33_86
| spl33_87
| spl33_88 ),
inference(sat_conversion,[],[f3983]) ).
cnf(s80,plain,
( spl33_29
| spl33_35
| spl33_36
| spl33_37
| spl33_38
| ~ spl33_86
| spl33_87
| ~ spl33_89 ),
inference(sat_conversion,[],[f3988]) ).
cnf(s84,plain,
( ~ spl33_26
| spl33_29
| spl33_35
| spl33_36
| spl33_37
| spl33_38
| ~ spl33_86
| spl33_87
| spl33_90
| ~ spl33_94 ),
inference(sat_conversion,[],[f4017]) ).
cnf(s86,plain,
~ spl33_36,
inference(sat_conversion,[],[f4042]) ).
cnf(s95,plain,
( ~ spl33_26
| spl33_29
| spl33_35
| spl33_36
| spl33_37
| spl33_38
| ~ spl33_88
| spl33_89
| spl33_94
| spl33_100 ),
inference(sat_conversion,[],[f4172]) ).
cnf(s102,plain,
( ~ spl33_26
| ~ spl33_37 ),
inference(sat_conversion,[],[f4269]) ).
cnf(s109,plain,
( ~ spl33_26
| ~ spl33_38 ),
inference(sat_conversion,[],[f4336]) ).
cnf(s693,plain,
spl33_86,
inference(sat_conversion,[],[f16825]) ).
cnf(s703,plain,
~ spl33_87,
inference(sat_conversion,[],[f16928]) ).
cnf(s704,plain,
~ spl33_90,
inference(sat_conversion,[],[f16941]) ).
cnf(s708,plain,
~ spl33_100,
inference(sat_conversion,[],[f17004]) ).
cnf(s976,plain,
( ~ spl33_26
| spl33_29
| spl33_35
| spl33_36
| spl33_37
| spl33_38
| ~ spl33_88
| spl33_89
| spl33_94 ),
inference(rat,[],[s95,s708]) ).
cnf(s978,plain,
( ~ spl33_26
| spl33_29
| spl33_35
| spl33_37
| spl33_38
| ~ spl33_94 ),
inference(rat,[],[s84,s704,s703,s693,s86]) ).
cnf(s982,plain,
( spl33_29
| spl33_35
| spl33_37
| spl33_38
| ~ spl33_89 ),
inference(rat,[],[s80,s703,s693,s86]) ).
cnf(s983,plain,
( spl33_29
| spl33_35
| spl33_37
| spl33_38
| spl33_88 ),
inference(rat,[],[s79,s703,s693,s86]) ).
cnf(s1045,plain,
~ spl33_38,
inference(rat,[],[s109,s23]) ).
cnf(s1046,plain,
~ spl33_37,
inference(rat,[],[s102,s23]) ).
cnf(s1051,plain,
~ spl33_89,
inference(rat,[],[s982,s1045,s48,s76,s1046]) ).
cnf(s1052,plain,
spl33_88,
inference(rat,[],[s983,s1045,s48,s76,s1046]) ).
cnf(s1061,plain,
~ spl33_94,
inference(rat,[],[s978,s23,s1045,s48,s76,s1046]) ).
cnf(s1076,plain,
$false,
inference(rat,[],[s976,s1046,s1051,s23,s1045,s48,s86,s76,s1061,s1052]) ).
fof(f17005,plain,
$false,
inference(avatar_sat_refutation,[],[s1076]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT370+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.12/0.38 % Computer : n001.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Sun Sep 27 15:12:01 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.12/0.42 Running first-order model finding
% 0.12/0.42 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.60/0.91 % (3682262)Will run a generic schedule for satisfiability detection.
% 2.60/0.91 % (3682273)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3027135101:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 2.60/0.91 % (3682268)% WARNING: option uhcvi not known.
% 2.60/0.91 % (3682267)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3329181937_2999 on theBenchmark for (2999ds/0Mi)
% 2.60/0.91 % (3682268)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=309734775:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 2.60/0.91 % (3682269)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=705204849:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 2.60/0.91 % (3682270)dis+10_1_sil=32000:sp=arity:random_seed=1447352682:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 2.60/0.91 % (3682271)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1075168718:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 2.60/0.91 % (3682272)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=726399057:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 2.60/0.91 % TRYING [1]
% 2.60/0.91 % (3682273)Instruction limit reached!
% 2.60/0.91 % (3682273)------------------------------
% 2.60/0.91 % (3682273)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.60/0.91 % (3682273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.60/0.91 % (3682273)CaDiCaL version: 2.1.3
% 2.60/0.91 % (3682273)Termination reason: Instruction limit
% 2.60/0.91 % (3682273)Termination phase: Saturation
% 2.60/0.91 % (3682273)Time elapsed: 0.052 s
% 2.60/0.91 % (3682273)Peak memory usage: 15 MB
% 2.60/0.91 % (3682273)Instructions burned: 163 (million)
% 2.60/0.91 % TRYING [2]
% 2.60/0.91 % (3682281)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2221845812:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 2.60/0.91 % TRYING [3]
% 2.60/0.91 % (3682270)Instruction limit reached!
% 2.60/0.91 % (3682270)------------------------------
% 2.60/0.91 % (3682270)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.60/0.91 % (3682270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.60/0.91 % (3682270)CaDiCaL version: 2.1.3
% 2.60/0.91 % (3682270)Termination reason: Instruction limit
% 2.60/0.91 % (3682270)Termination phase: Saturation
% 2.60/0.91 % (3682270)Time elapsed: 0.063 s
% 2.60/0.91 % (3682270)Peak memory usage: 13 MB
% 2.60/0.91 % (3682270)Instructions burned: 104 (million)
% 2.60/0.91 % (3682271)Instruction limit reached!
% 2.60/0.91 % (3682271)------------------------------
% 2.60/0.91 % (3682271)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.60/0.91 % (3682271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.60/0.91 % (3682271)CaDiCaL version: 2.1.3
% 2.60/0.91 % (3682271)Termination reason: Instruction limit
% 2.60/0.91 % (3682271)Termination phase: Saturation
% 2.60/0.91 % (3682271)Time elapsed: 0.064 s
% 2.60/0.91 % (3682271)Peak memory usage: 14 MB
% 2.60/0.91 % (3682271)Instructions burned: 116 (million)
% 2.60/0.91 % TRYING [1]
% 2.60/0.91 % TRYING [2]
% 2.60/0.91 % (3682272)Instruction limit reached!
% 2.60/0.91 % (3682272)------------------------------
% 2.60/0.91 % (3682272)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.60/0.91 % (3682272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.60/0.91 % (3682272)CaDiCaL version: 2.1.3
% 2.60/0.91 % (3682272)Termination reason: Instruction limit
% 2.60/0.91 % (3682272)Termination phase: Saturation
% 2.60/0.91 % (3682272)Time elapsed: 0.071 s
% 2.60/0.91 % (3682272)Peak memory usage: 14 MB
% 2.60/0.91 % (3682272)Instructions burned: 132 (million)
% 2.60/0.91 % TRYING [3]
% 2.60/0.91 % (3682283)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1102286653:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 2.60/0.91 % (3682284)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=1079277657:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 2.60/0.91 % (3682285)ott-21_1_sil=16000:fs=off:random_seed=2017076432:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 2.60/0.91 % TRYING [4]
% 2.60/0.91 % TRYING [4]
% 2.60/0.91 % (3682283)Instruction limit reached!
% 2.60/0.91 % (3682283)------------------------------
% 2.60/0.91 % (3682283)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.60/0.91 % (3682283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.60/0.91 % (3682283)CaDiCaL version: 2.1.3
% 2.60/0.91 % (3682283)Termination reason: Instruction limit
% 2.60/0.91 % (3682283)Termination phase: Saturation
% 2.60/0.91 % (3682283)Time elapsed: 0.074 s
% 2.60/0.91 % (3682283)Peak memory usage: 14 MB
% 2.60/0.91 % (3682283)Instructions burned: 133 (million)
% 2.60/0.91 % (3682289)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3773356978:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 2.60/0.91 % (3682285)Instruction limit reached!
% 2.60/0.91 % (3682285)------------------------------
% 2.60/0.91 % (3682285)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.60/0.91 % (3682285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.60/0.91 % (3682285)CaDiCaL version: 2.1.3
% 2.60/0.91 % (3682285)Termination reason: Instruction limit
% 2.60/0.91 % (3682285)Termination phase: Saturation
% 2.60/0.91 % (3682285)Time elapsed: 0.099 s
% 2.60/0.91 % (3682285)Peak memory usage: 13 MB
% 2.60/0.91 % (3682285)Instructions burned: 181 (million)
% 2.60/0.91 % (3682291)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3366972045:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 2.60/0.91 % (3682281)Instruction limit reached!
% 2.60/0.91 % (3682281)------------------------------
% 2.60/0.91 % (3682281)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.60/0.91 % (3682281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.60/0.91 % (3682281)CaDiCaL version: 2.1.3
% 2.60/0.91 % (3682281)Termination reason: Instruction limit
% 2.60/0.91 % (3682281)Termination phase: Finite model building SAT solving
% 2.60/0.91 % (3682281)Time elapsed: 0.162 s
% 2.60/0.91 % (3682281)Peak memory usage: 36 MB
% 2.60/0.91 % (3682281)Instructions burned: 717 (million)
% 2.60/0.91 % (3682293)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1356967787:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 2.60/0.91 % TRYING [1]
% 2.60/0.91 % TRYING [2]
% 2.60/0.91 % TRYING [3]
% 2.60/0.91 % (3682268) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3682262-3682268"...
% 2.60/0.91 % (3682268)...printing done.
% 2.60/0.91 % (3682268)Refutation found. Thanks to Tanya!
% 2.60/0.91 % SZS status Theorem for theBenchmark
% 2.60/0.91 % SZS output start Proof for theBenchmark
% See solution above
% 2.60/0.91 % (3682268)------------------------------
% 2.60/0.91 % (3682268)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.60/0.91 % (3682268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.60/0.91 % (3682268)CaDiCaL version: 2.1.3
% 2.60/0.91 % (3682268)Termination reason: Refutation
% 2.60/0.91 % (3682268)Time elapsed: 0.441 s
% 2.60/0.91 % (3682268)Peak memory usage: 20 MB
% 2.60/0.91 % (3682268)Instructions burned: 772 (million)
% 2.60/0.91 % (3682262)Success in time 0.485 s
% 2.60/0.91 % Vampire exiting
%------------------------------------------------------------------------------