%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT369+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n003.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:47:25 AM UTC 2026
% Result : Theorem 2.86s 1.32s
% Output : Refutation 4.01s
% Verified :
% SZS Type : Refutation
% Derivation depth : 39
% Number of leaves : 29
% Syntax : Number of formulae : 325 ( 32 unt; 13 def)
% Number of atoms : 2055 ( 18 equ)
% Maximal formula atoms : 25 ( 6 avg)
% Number of connectives : 2974 (1244 ~;1362 |; 314 &)
% ( 16 <=>; 38 =>; 0 <=; 0 <~>)
% Maximal formula depth : 28 ( 7 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 47 ( 45 usr; 13 prp; 0-3 aty)
% Number of functors : 8 ( 8 usr; 2 con; 0-3 aty)
% Number of variables : 168 ( 0 sgn 164 !; 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)
& 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)
=> v1_waybel34(k2_waybel_1(X0,X0,X1),X0,k2_yellow_2(X0,X0,X1)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t42_waybel34) ).
fof(f2,negated_conjecture,
~ ! [X0] :
( ( 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)
=> v1_waybel34(k2_waybel_1(X0,X0,X1),X0,k2_yellow_2(X0,X0,X1)) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f9,axiom,
! [X0] :
( ( v3_orders_2(X0)
& v4_orders_2(X0)
& v2_lattice3(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( m1_yellow_0(X1,X0)
=> ( ( ~ v3_struct_0(X1)
& v4_yellow_0(X1,X0)
& v5_yellow_0(X1,X0) )
=> ( ~ v3_struct_0(X1)
& v3_orders_2(X1)
& v4_orders_2(X1)
& v2_lattice3(X1)
& v4_yellow_0(X1,X0)
& v5_yellow_0(X1,X0) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc11_yellow_0) ).
fof(f31,axiom,
! [X0] :
( l1_orders_2(X0)
=> ( ( ~ v3_struct_0(X0)
& v3_lattice3(X0) )
=> ( ~ v3_struct_0(X0)
& v1_lattice3(X0)
& v2_lattice3(X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc1_yellow_0) ).
fof(f36,axiom,
! [X0] :
( l1_orders_2(X0)
=> ( v2_lattice3(X0)
=> ~ v3_struct_0(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc2_lattice3) ).
fof(f41,axiom,
! [X0] :
( ( ~ 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(f54,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( m1_yellow_0(X1,X0)
=> ( v7_yellow_0(X1,X0)
=> v5_yellow_0(X1,X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc9_yellow_0) ).
fof(f63,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(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_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(f72,axiom,
! [X0] :
( l1_orders_2(X0)
=> ! [X1] :
( m1_yellow_0(X1,X0)
=> l1_orders_2(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m1_yellow_0) ).
fof(f82,axiom,
! [X0,X1] :
( ( ~ 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(f83,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] :
( ( ~ 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)) )
=> ( ~ v3_struct_0(k2_yellow_2(X0,X1,X2))
& v1_orders_2(k2_yellow_2(X0,X1,X2))
& v4_yellow_0(k2_yellow_2(X0,X1,X2),X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc2_yellow_2) ).
fof(f134,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
<=> m1_relset_1(X2,X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(f137,axiom,
! [X0] :
( ( 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)
& 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)) )
=> ( v22_waybel_0(X2,X0,X1)
=> v1_waybel34(k1_waybel34(X0,X1,X2),X1,X0) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t24_waybel34) ).
fof(f139,axiom,
! [X0] :
( ( 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(f141,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(f181,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,[],[f82]) ).
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(f210,plain,
? [X0] :
( ? [X1] :
( ~ v1_waybel34(k2_waybel_1(X0,X0,X1),X0,k2_yellow_2(X0,X0,X1))
& v4_waybel_0(k2_yellow_2(X0,X0,X1),X0)
& 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,[],[f2]) ).
fof(f211,plain,
? [X0] :
( ? [X1] :
( ~ v1_waybel34(k2_waybel_1(X0,X0,X1),X0,k2_yellow_2(X0,X0,X1))
& v4_waybel_0(k2_yellow_2(X0,X0,X1),X0)
& 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,[],[f210]) ).
fof(f212,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,[],[f139]) ).
fof(f213,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,[],[f212]) ).
fof(f224,plain,
! [X0] :
( ~ v3_struct_0(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f36]) ).
fof(f225,plain,
! [X0] :
( ~ v3_struct_0(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f224]) ).
fof(f226,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v1_lattice3(X0)
& v2_lattice3(X0) )
| v3_struct_0(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f31]) ).
fof(f227,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v1_lattice3(X0)
& v2_lattice3(X0) )
| v3_struct_0(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f226]) ).
fof(f230,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(f231,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,[],[f230]) ).
fof(f232,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,[],[f141]) ).
fof(f233,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,[],[f232]) ).
fof(f238,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( v1_waybel34(k1_waybel34(X0,X1,X2),X1,X0)
| ~ v22_waybel_0(X2,X0,X1)
| ~ 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)
| ~ 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,[],[f137]) ).
fof(f239,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( v1_waybel34(k1_waybel34(X0,X1,X2),X1,X0)
| ~ v22_waybel_0(X2,X0,X1)
| ~ 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)
| ~ 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,[],[f238]) ).
fof(f249,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,[],[f65]) ).
fof(f250,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,[],[f249]) ).
fof(f273,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,[],[f83]) ).
fof(f274,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,[],[f273]) ).
fof(f293,plain,
! [X0] :
( ! [X1] :
( l1_orders_2(X1)
| ~ m1_yellow_0(X1,X0) )
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f72]) ).
fof(f294,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,[],[f63]) ).
fof(f295,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,[],[f294]) ).
fof(f302,plain,
! [X0,X1,X2] :
( ( ~ v3_struct_0(k2_yellow_2(X0,X1,X2))
& v1_orders_2(k2_yellow_2(X0,X1,X2))
& v4_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,[],[f92]) ).
fof(f303,plain,
! [X0,X1,X2] :
( ( ~ v3_struct_0(k2_yellow_2(X0,X1,X2))
& v1_orders_2(k2_yellow_2(X0,X1,X2))
& v4_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,[],[f302]) ).
fof(f304,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,[],[f181]) ).
fof(f305,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,[],[f304]) ).
fof(f306,plain,
! [X0] :
( ! [X1] :
( v5_yellow_0(X1,X0)
| ~ v7_yellow_0(X1,X0)
| ~ m1_yellow_0(X1,X0) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f54]) ).
fof(f307,plain,
! [X0] :
( ! [X1] :
( v5_yellow_0(X1,X0)
| ~ v7_yellow_0(X1,X0)
| ~ m1_yellow_0(X1,X0) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f306]) ).
fof(f308,plain,
! [X0] :
( ! [X1] :
( ( ~ v3_struct_0(X1)
& v3_orders_2(X1)
& v4_orders_2(X1)
& v2_lattice3(X1)
& v4_yellow_0(X1,X0)
& v5_yellow_0(X1,X0) )
| v3_struct_0(X1)
| ~ v4_yellow_0(X1,X0)
| ~ v5_yellow_0(X1,X0)
| ~ m1_yellow_0(X1,X0) )
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f9]) ).
fof(f309,plain,
! [X0] :
( ! [X1] :
( ( ~ v3_struct_0(X1)
& v3_orders_2(X1)
& v4_orders_2(X1)
& v2_lattice3(X1)
& v4_yellow_0(X1,X0)
& v5_yellow_0(X1,X0) )
| v3_struct_0(X1)
| ~ v4_yellow_0(X1,X0)
| ~ v5_yellow_0(X1,X0)
| ~ m1_yellow_0(X1,X0) )
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f308]) ).
fof(f367,definition,
! [X1,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)) )
| ~ sP3(X1,X0) ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f368,plain,
! [X0,X1] :
( sP3(X1,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)
| ~ 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(definition_folding,[],[f274,f367]) ).
fof(f377,plain,
( ~ v1_waybel34(k2_waybel_1(sK8,sK8,sK9),sK8,k2_yellow_2(sK8,sK8,sK9))
& v4_waybel_0(k2_yellow_2(sK8,sK8,sK9),sK8)
& v1_funct_1(sK9)
& v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
& v7_waybel_1(sK9,sK8)
& m2_relset_1(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
& v2_orders_2(sK8)
& v3_orders_2(sK8)
& v4_orders_2(sK8)
& v1_lattice3(sK8)
& v2_lattice3(sK8)
& v3_lattice3(sK8)
& l1_orders_2(sK8) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8,sK9]),skolemize(X0,sK8),skolemize(X1,sK9)],[f211]) ).
fof(f382,plain,
! [X0,X1,X2] :
( ( m2_relset_1(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1) )
& ( m1_relset_1(X2,X0,X1)
| ~ m2_relset_1(X2,X0,X1) ) ),
inference(nnf_transformation,[],[f134]) ).
fof(f384,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) )
& ( 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) ) )
| ~ 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(nnf_transformation,[],[f233]) ).
fof(f397,plain,
! [X1,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)) )
| ~ sP3(X1,X0) ),
inference(nnf_transformation,[],[f367]) ).
fof(f398,plain,
! [X0,X1] :
( ( ~ v3_struct_0(k2_yellow_2(X1,X1,X0))
& v1_orders_2(k2_yellow_2(X1,X1,X0))
& v2_orders_2(k2_yellow_2(X1,X1,X0))
& v3_orders_2(k2_yellow_2(X1,X1,X0))
& v4_orders_2(k2_yellow_2(X1,X1,X0))
& v1_yellow_0(k2_yellow_2(X1,X1,X0))
& v2_yellow_0(k2_yellow_2(X1,X1,X0))
& v3_yellow_0(k2_yellow_2(X1,X1,X0))
& v4_yellow_0(k2_yellow_2(X1,X1,X0),X1)
& v24_waybel_0(k2_yellow_2(X1,X1,X0))
& v25_waybel_0(k2_yellow_2(X1,X1,X0))
& v1_lattice3(k2_yellow_2(X1,X1,X0))
& v2_lattice3(k2_yellow_2(X1,X1,X0))
& v3_lattice3(k2_yellow_2(X1,X1,X0)) )
| ~ sP3(X0,X1) ),
inference(rectify,[],[f397]) ).
fof(f412,plain,
l1_orders_2(sK8),
inference(cnf_transformation,[],[f377]) ).
fof(f413,plain,
v3_lattice3(sK8),
inference(cnf_transformation,[],[f377]) ).
fof(f414,plain,
v2_lattice3(sK8),
inference(cnf_transformation,[],[f377]) ).
fof(f415,plain,
v1_lattice3(sK8),
inference(cnf_transformation,[],[f377]) ).
fof(f416,plain,
v4_orders_2(sK8),
inference(cnf_transformation,[],[f377]) ).
fof(f417,plain,
v3_orders_2(sK8),
inference(cnf_transformation,[],[f377]) ).
fof(f418,plain,
v2_orders_2(sK8),
inference(cnf_transformation,[],[f377]) ).
fof(f419,plain,
m2_relset_1(sK9,u1_struct_0(sK8),u1_struct_0(sK8)),
inference(cnf_transformation,[],[f377]) ).
fof(f420,plain,
v7_waybel_1(sK9,sK8),
inference(cnf_transformation,[],[f377]) ).
fof(f421,plain,
v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8)),
inference(cnf_transformation,[],[f377]) ).
fof(f422,plain,
v1_funct_1(sK9),
inference(cnf_transformation,[],[f377]) ).
fof(f423,plain,
v4_waybel_0(k2_yellow_2(sK8,sK8,sK9),sK8),
inference(cnf_transformation,[],[f377]) ).
fof(f424,plain,
~ v1_waybel34(k2_waybel_1(sK8,sK8,sK9),sK8,k2_yellow_2(sK8,sK8,sK9)),
inference(cnf_transformation,[],[f377]) ).
fof(f425,plain,
! [X0,X1] :
( ~ m2_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)
| k2_waybel_1(X0,X0,X1) = k1_waybel34(k2_yellow_2(X0,X0,X1),X0,k3_waybel_1(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) ),
inference(cnf_transformation,[],[f213]) ).
fof(f427,plain,
! [X0,X1] :
( v17_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(cnf_transformation,[],[f213]) ).
fof(f443,plain,
! [X0] :
( ~ v3_struct_0(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f225]) ).
fof(f461,plain,
! [X0] :
( ~ l1_orders_2(X0)
| v3_struct_0(X0)
| ~ v3_lattice3(X0)
| v1_lattice3(X0) ),
inference(cnf_transformation,[],[f227]) ).
fof(f471,plain,
! [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)
| v6_waybel_1(X1,X0)
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f231]) ).
fof(f475,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f382]) ).
fof(f478,plain,
! [X0,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)
| ~ 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(cnf_transformation,[],[f384]) ).
fof(f509,plain,
! [X2,X0,X1] :
( v1_waybel34(k1_waybel34(X0,X1,X2),X1,X0)
| ~ v22_waybel_0(X2,X0,X1)
| ~ 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)
| ~ 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(cnf_transformation,[],[f239]) ).
fof(f521,plain,
! [X2,X0,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(cnf_transformation,[],[f250]) ).
fof(f522,plain,
! [X2,X0,X1] :
( v1_funct_2(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(cnf_transformation,[],[f250]) ).
fof(f523,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,u1_struct_0(X0),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))
| v1_funct_1(k3_waybel_1(X0,X1,X2)) ),
inference(cnf_transformation,[],[f250]) ).
fof(f604,plain,
! [X0,X1] :
( v3_lattice3(k2_yellow_2(X1,X1,X0))
| ~ sP3(X0,X1) ),
inference(cnf_transformation,[],[f398]) ).
fof(f618,plain,
! [X0,X1] :
( ~ m1_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)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v6_waybel_1(X1,X0)
| sP3(X1,X0) ),
inference(cnf_transformation,[],[f368]) ).
fof(f671,plain,
! [X0,X1] :
( ~ m1_yellow_0(X1,X0)
| l1_orders_2(X1)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f293]) ).
fof(f672,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,u1_struct_0(X0),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_yellow_0(k2_yellow_2(X0,X1,X2),X1) ),
inference(cnf_transformation,[],[f295]) ).
fof(f681,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,u1_struct_0(X0),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))
| v4_yellow_0(k2_yellow_2(X0,X1,X2),X1) ),
inference(cnf_transformation,[],[f303]) ).
fof(f683,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,u1_struct_0(X0),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))
| ~ v3_struct_0(k2_yellow_2(X0,X1,X2)) ),
inference(cnf_transformation,[],[f303]) ).
fof(f684,plain,
! [X0,X1] :
( ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(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)
| v7_yellow_0(k2_yellow_2(X0,X0,X1),X0) ),
inference(cnf_transformation,[],[f305]) ).
fof(f687,plain,
! [X0,X1] :
( ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(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)
| v4_orders_2(k2_yellow_2(X0,X0,X1)) ),
inference(cnf_transformation,[],[f305]) ).
fof(f688,plain,
! [X0,X1] :
( ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(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)
| v3_orders_2(k2_yellow_2(X0,X0,X1)) ),
inference(cnf_transformation,[],[f305]) ).
fof(f689,plain,
! [X0,X1] :
( ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(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)
| v2_orders_2(k2_yellow_2(X0,X0,X1)) ),
inference(cnf_transformation,[],[f305]) ).
fof(f692,plain,
! [X0,X1] :
( ~ v7_yellow_0(X1,X0)
| v5_yellow_0(X1,X0)
| ~ m1_yellow_0(X1,X0)
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f307]) ).
fof(f695,plain,
! [X0,X1] :
( ~ v5_yellow_0(X1,X0)
| v3_struct_0(X1)
| ~ v4_yellow_0(X1,X0)
| v2_lattice3(X1)
| ~ m1_yellow_0(X1,X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f309]) ).
fof(f882,plain,
m1_relset_1(sK9,u1_struct_0(sK8),u1_struct_0(sK8)),
inference(resolution,[],[f475,f419]) ).
fof(f921,definition,
( spl31_5
<=> v3_struct_0(sK8) ),
introduced(definition,[new_symbols(definition,[spl31_5])],[avatar_definition]) ).
fof(f922,plain,
( ~ v3_struct_0(sK8)
| spl31_5 ),
inference(avatar_component_clause,[],[f921]) ).
fof(f923,plain,
( v3_struct_0(sK8)
| ~ spl31_5 ),
inference(avatar_component_clause,[],[f921]) ).
fof(f972,plain,
( ~ v2_lattice3(sK8)
| ~ l1_orders_2(sK8)
| ~ spl31_5 ),
inference(resolution,[],[f923,f443]) ).
fof(f975,plain,
( ~ l1_orders_2(sK8)
| ~ spl31_5 ),
inference(forward_subsumption_resolution,[],[f972,f414]) ).
fof(f978,plain,
( $false
| ~ spl31_5 ),
inference(forward_subsumption_resolution,[],[f975,f412]) ).
fof(f979,plain,
~ spl31_5,
inference(avatar_contradiction_clause,[],[f978]) ).
fof(f2007,plain,
( ~ v1_funct_1(sK9)
| ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ v7_waybel_1(sK9,sK8)
| v6_waybel_1(sK9,sK8)
| v3_struct_0(sK8)
| ~ l1_orders_2(sK8) ),
inference(resolution,[],[f471,f882]) ).
fof(f2031,plain,
( ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ v7_waybel_1(sK9,sK8)
| v6_waybel_1(sK9,sK8)
| v3_struct_0(sK8)
| ~ l1_orders_2(sK8) ),
inference(forward_subsumption_resolution,[],[f2007,f422]) ).
fof(f2037,plain,
( ~ v7_waybel_1(sK9,sK8)
| v6_waybel_1(sK9,sK8)
| v3_struct_0(sK8)
| ~ l1_orders_2(sK8) ),
inference(forward_subsumption_resolution,[],[f2031,f421]) ).
fof(f2042,plain,
( v6_waybel_1(sK9,sK8)
| v3_struct_0(sK8)
| ~ l1_orders_2(sK8) ),
inference(forward_subsumption_resolution,[],[f2037,f420]) ).
fof(f2055,plain,
( v6_waybel_1(sK9,sK8)
| ~ l1_orders_2(sK8)
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f2042,f922]) ).
fof(f2067,plain,
( v6_waybel_1(sK9,sK8)
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f2055,f412]) ).
fof(f2401,plain,
( v3_struct_0(sK8)
| ~ l1_orders_2(sK8)
| v3_struct_0(sK8)
| ~ l1_orders_2(sK8)
| ~ v1_funct_1(sK9)
| ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| v1_funct_1(k3_waybel_1(sK8,sK8,sK9)) ),
inference(resolution,[],[f523,f882]) ).
fof(f2424,plain,
( v3_struct_0(sK8)
| ~ l1_orders_2(sK8)
| ~ v1_funct_1(sK9)
| ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| v1_funct_1(k3_waybel_1(sK8,sK8,sK9)) ),
inference(duplicate_literal_removal,[],[f2401]) ).
fof(f2437,plain,
( ~ l1_orders_2(sK8)
| ~ v1_funct_1(sK9)
| ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| v1_funct_1(k3_waybel_1(sK8,sK8,sK9))
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f2424,f922]) ).
fof(f2449,plain,
( ~ v1_funct_1(sK9)
| ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| v1_funct_1(k3_waybel_1(sK8,sK8,sK9))
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f2437,f412]) ).
fof(f2453,plain,
( ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| v1_funct_1(k3_waybel_1(sK8,sK8,sK9))
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f2449,f422]) ).
fof(f2456,plain,
( v1_funct_1(k3_waybel_1(sK8,sK8,sK9))
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f2453,f421]) ).
fof(f2529,definition,
( spl31_61
<=> l1_orders_2(k2_yellow_2(sK8,sK8,sK9)) ),
introduced(definition,[new_symbols(definition,[spl31_61])],[avatar_definition]) ).
fof(f2530,plain,
( l1_orders_2(k2_yellow_2(sK8,sK8,sK9))
| ~ spl31_61 ),
inference(avatar_component_clause,[],[f2529]) ).
fof(f2531,plain,
( ~ l1_orders_2(k2_yellow_2(sK8,sK8,sK9))
| spl31_61 ),
inference(avatar_component_clause,[],[f2529]) ).
fof(f2539,plain,
( v3_struct_0(sK8)
| ~ l1_orders_2(sK8)
| v3_struct_0(sK8)
| ~ l1_orders_2(sK8)
| ~ v1_funct_1(sK9)
| ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ v3_struct_0(k2_yellow_2(sK8,sK8,sK9)) ),
inference(resolution,[],[f683,f882]) ).
fof(f2562,plain,
( v3_struct_0(sK8)
| ~ l1_orders_2(sK8)
| ~ v1_funct_1(sK9)
| ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ v3_struct_0(k2_yellow_2(sK8,sK8,sK9)) ),
inference(duplicate_literal_removal,[],[f2539]) ).
fof(f2575,plain,
( ~ l1_orders_2(sK8)
| ~ v1_funct_1(sK9)
| ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ v3_struct_0(k2_yellow_2(sK8,sK8,sK9))
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f2562,f922]) ).
fof(f2587,plain,
( ~ v1_funct_1(sK9)
| ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ v3_struct_0(k2_yellow_2(sK8,sK8,sK9))
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f2575,f412]) ).
fof(f2591,plain,
( ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ v3_struct_0(k2_yellow_2(sK8,sK8,sK9))
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f2587,f422]) ).
fof(f2594,plain,
( ~ v3_struct_0(k2_yellow_2(sK8,sK8,sK9))
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f2591,f421]) ).
fof(f2603,plain,
( v3_struct_0(sK8)
| ~ l1_orders_2(sK8)
| v3_struct_0(sK8)
| ~ l1_orders_2(sK8)
| ~ v1_funct_1(sK9)
| ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| m1_yellow_0(k2_yellow_2(sK8,sK8,sK9),sK8) ),
inference(resolution,[],[f672,f882]) ).
fof(f2626,plain,
( v3_struct_0(sK8)
| ~ l1_orders_2(sK8)
| ~ v1_funct_1(sK9)
| ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| m1_yellow_0(k2_yellow_2(sK8,sK8,sK9),sK8) ),
inference(duplicate_literal_removal,[],[f2603]) ).
fof(f2639,plain,
( ~ l1_orders_2(sK8)
| ~ v1_funct_1(sK9)
| ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| m1_yellow_0(k2_yellow_2(sK8,sK8,sK9),sK8)
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f2626,f922]) ).
fof(f2651,plain,
( ~ v1_funct_1(sK9)
| ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| m1_yellow_0(k2_yellow_2(sK8,sK8,sK9),sK8)
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f2639,f412]) ).
fof(f2655,plain,
( ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| m1_yellow_0(k2_yellow_2(sK8,sK8,sK9),sK8)
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f2651,f422]) ).
fof(f2658,plain,
( m1_yellow_0(k2_yellow_2(sK8,sK8,sK9),sK8)
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f2655,f421]) ).
fof(f2667,plain,
( v3_struct_0(sK8)
| ~ l1_orders_2(sK8)
| v3_struct_0(sK8)
| ~ l1_orders_2(sK8)
| ~ v1_funct_1(sK9)
| ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| v4_yellow_0(k2_yellow_2(sK8,sK8,sK9),sK8) ),
inference(resolution,[],[f681,f882]) ).
fof(f2690,plain,
( v3_struct_0(sK8)
| ~ l1_orders_2(sK8)
| ~ v1_funct_1(sK9)
| ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| v4_yellow_0(k2_yellow_2(sK8,sK8,sK9),sK8) ),
inference(duplicate_literal_removal,[],[f2667]) ).
fof(f2703,plain,
( ~ l1_orders_2(sK8)
| ~ v1_funct_1(sK9)
| ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| v4_yellow_0(k2_yellow_2(sK8,sK8,sK9),sK8)
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f2690,f922]) ).
fof(f2715,plain,
( ~ v1_funct_1(sK9)
| ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| v4_yellow_0(k2_yellow_2(sK8,sK8,sK9),sK8)
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f2703,f412]) ).
fof(f2719,plain,
( ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| v4_yellow_0(k2_yellow_2(sK8,sK8,sK9),sK8)
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f2715,f422]) ).
fof(f2722,plain,
( v4_yellow_0(k2_yellow_2(sK8,sK8,sK9),sK8)
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f2719,f421]) ).
fof(f2729,plain,
( l1_orders_2(k2_yellow_2(sK8,sK8,sK9))
| ~ l1_orders_2(sK8)
| spl31_5 ),
inference(resolution,[],[f2658,f671]) ).
fof(f2730,plain,
( ~ l1_orders_2(sK8)
| spl31_5
| spl31_61 ),
inference(forward_subsumption_resolution,[],[f2729,f2531]) ).
fof(f2731,plain,
( $false
| spl31_5
| spl31_61 ),
inference(forward_subsumption_resolution,[],[f2730,f412]) ).
fof(f2732,plain,
( spl31_5
| spl31_61 ),
inference(avatar_contradiction_clause,[],[f2731]) ).
fof(f2734,plain,
( v3_struct_0(k2_yellow_2(sK8,sK8,sK9))
| ~ v3_lattice3(k2_yellow_2(sK8,sK8,sK9))
| v1_lattice3(k2_yellow_2(sK8,sK8,sK9))
| ~ spl31_61 ),
inference(resolution,[],[f2530,f461]) ).
fof(f2751,definition,
( spl31_64
<=> v3_lattice3(k2_yellow_2(sK8,sK8,sK9)) ),
introduced(definition,[new_symbols(definition,[spl31_64])],[avatar_definition]) ).
fof(f2752,plain,
( v3_lattice3(k2_yellow_2(sK8,sK8,sK9))
| ~ spl31_64 ),
inference(avatar_component_clause,[],[f2751]) ).
fof(f2753,plain,
( ~ v3_lattice3(k2_yellow_2(sK8,sK8,sK9))
| spl31_64 ),
inference(avatar_component_clause,[],[f2751]) ).
fof(f2755,definition,
( spl31_65
<=> v2_lattice3(k2_yellow_2(sK8,sK8,sK9)) ),
introduced(definition,[new_symbols(definition,[spl31_65])],[avatar_definition]) ).
fof(f2756,plain,
( v2_lattice3(k2_yellow_2(sK8,sK8,sK9))
| ~ spl31_65 ),
inference(avatar_component_clause,[],[f2755]) ).
fof(f2759,definition,
( spl31_66
<=> v1_lattice3(k2_yellow_2(sK8,sK8,sK9)) ),
introduced(definition,[new_symbols(definition,[spl31_66])],[avatar_definition]) ).
fof(f2760,plain,
( v1_lattice3(k2_yellow_2(sK8,sK8,sK9))
| ~ spl31_66 ),
inference(avatar_component_clause,[],[f2759]) ).
fof(f2763,definition,
( spl31_67
<=> v4_orders_2(k2_yellow_2(sK8,sK8,sK9)) ),
introduced(definition,[new_symbols(definition,[spl31_67])],[avatar_definition]) ).
fof(f2764,plain,
( v4_orders_2(k2_yellow_2(sK8,sK8,sK9))
| ~ spl31_67 ),
inference(avatar_component_clause,[],[f2763]) ).
fof(f2767,definition,
( spl31_68
<=> v3_orders_2(k2_yellow_2(sK8,sK8,sK9)) ),
introduced(definition,[new_symbols(definition,[spl31_68])],[avatar_definition]) ).
fof(f2768,plain,
( v3_orders_2(k2_yellow_2(sK8,sK8,sK9))
| ~ spl31_68 ),
inference(avatar_component_clause,[],[f2767]) ).
fof(f2771,definition,
( spl31_69
<=> v2_orders_2(k2_yellow_2(sK8,sK8,sK9)) ),
introduced(definition,[new_symbols(definition,[spl31_69])],[avatar_definition]) ).
fof(f2772,plain,
( v2_orders_2(k2_yellow_2(sK8,sK8,sK9))
| ~ spl31_69 ),
inference(avatar_component_clause,[],[f2771]) ).
fof(f2773,plain,
( ~ v2_orders_2(k2_yellow_2(sK8,sK8,sK9))
| spl31_69 ),
inference(avatar_component_clause,[],[f2771]) ).
fof(f2775,plain,
( ~ v3_lattice3(k2_yellow_2(sK8,sK8,sK9))
| v1_lattice3(k2_yellow_2(sK8,sK8,sK9))
| spl31_5
| ~ spl31_61 ),
inference(forward_subsumption_resolution,[],[f2734,f2594]) ).
fof(f2802,plain,
( spl31_66
| ~ spl31_64
| spl31_5
| ~ spl31_61 ),
inference(avatar_split_clause,[],[f2775,f2529,f921,f2751,f2759]) ).
fof(f2804,plain,
( ~ sP3(sK9,sK8)
| spl31_64 ),
inference(resolution,[],[f2753,f604]) ).
fof(f3000,plain,
( v3_struct_0(sK8)
| ~ v2_orders_2(sK8)
| ~ v3_orders_2(sK8)
| ~ v4_orders_2(sK8)
| ~ l1_orders_2(sK8)
| ~ v1_funct_1(sK9)
| ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ v7_waybel_1(sK9,sK8)
| v4_orders_2(k2_yellow_2(sK8,sK8,sK9)) ),
inference(resolution,[],[f687,f882]) ).
fof(f3024,plain,
( ~ v2_orders_2(sK8)
| ~ v3_orders_2(sK8)
| ~ v4_orders_2(sK8)
| ~ l1_orders_2(sK8)
| ~ v1_funct_1(sK9)
| ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ v7_waybel_1(sK9,sK8)
| v4_orders_2(k2_yellow_2(sK8,sK8,sK9))
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f3000,f922]) ).
fof(f3027,plain,
( ~ v3_orders_2(sK8)
| ~ v4_orders_2(sK8)
| ~ l1_orders_2(sK8)
| ~ v1_funct_1(sK9)
| ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ v7_waybel_1(sK9,sK8)
| v4_orders_2(k2_yellow_2(sK8,sK8,sK9))
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f3024,f418]) ).
fof(f3029,plain,
( ~ v4_orders_2(sK8)
| ~ l1_orders_2(sK8)
| ~ v1_funct_1(sK9)
| ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ v7_waybel_1(sK9,sK8)
| v4_orders_2(k2_yellow_2(sK8,sK8,sK9))
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f3027,f417]) ).
fof(f3030,plain,
( ~ l1_orders_2(sK8)
| ~ v1_funct_1(sK9)
| ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ v7_waybel_1(sK9,sK8)
| v4_orders_2(k2_yellow_2(sK8,sK8,sK9))
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f3029,f416]) ).
fof(f3031,plain,
( ~ v1_funct_1(sK9)
| ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ v7_waybel_1(sK9,sK8)
| v4_orders_2(k2_yellow_2(sK8,sK8,sK9))
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f3030,f412]) ).
fof(f3032,plain,
( ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ v7_waybel_1(sK9,sK8)
| v4_orders_2(k2_yellow_2(sK8,sK8,sK9))
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f3031,f422]) ).
fof(f3033,plain,
( ~ v7_waybel_1(sK9,sK8)
| v4_orders_2(k2_yellow_2(sK8,sK8,sK9))
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f3032,f421]) ).
fof(f3034,plain,
( v4_orders_2(k2_yellow_2(sK8,sK8,sK9))
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f3033,f420]) ).
fof(f3035,plain,
( spl31_67
| spl31_5 ),
inference(avatar_split_clause,[],[f3034,f921,f2763]) ).
fof(f3038,plain,
( v3_struct_0(sK8)
| ~ v2_orders_2(sK8)
| ~ v3_orders_2(sK8)
| ~ v4_orders_2(sK8)
| ~ l1_orders_2(sK8)
| ~ v1_funct_1(sK9)
| ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ v7_waybel_1(sK9,sK8)
| v3_orders_2(k2_yellow_2(sK8,sK8,sK9)) ),
inference(resolution,[],[f688,f882]) ).
fof(f3062,plain,
( ~ v2_orders_2(sK8)
| ~ v3_orders_2(sK8)
| ~ v4_orders_2(sK8)
| ~ l1_orders_2(sK8)
| ~ v1_funct_1(sK9)
| ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ v7_waybel_1(sK9,sK8)
| v3_orders_2(k2_yellow_2(sK8,sK8,sK9))
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f3038,f922]) ).
fof(f3065,plain,
( ~ v3_orders_2(sK8)
| ~ v4_orders_2(sK8)
| ~ l1_orders_2(sK8)
| ~ v1_funct_1(sK9)
| ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ v7_waybel_1(sK9,sK8)
| v3_orders_2(k2_yellow_2(sK8,sK8,sK9))
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f3062,f418]) ).
fof(f3067,plain,
( ~ v4_orders_2(sK8)
| ~ l1_orders_2(sK8)
| ~ v1_funct_1(sK9)
| ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ v7_waybel_1(sK9,sK8)
| v3_orders_2(k2_yellow_2(sK8,sK8,sK9))
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f3065,f417]) ).
fof(f3068,plain,
( ~ l1_orders_2(sK8)
| ~ v1_funct_1(sK9)
| ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ v7_waybel_1(sK9,sK8)
| v3_orders_2(k2_yellow_2(sK8,sK8,sK9))
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f3067,f416]) ).
fof(f3069,plain,
( ~ v1_funct_1(sK9)
| ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ v7_waybel_1(sK9,sK8)
| v3_orders_2(k2_yellow_2(sK8,sK8,sK9))
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f3068,f412]) ).
fof(f3070,plain,
( ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ v7_waybel_1(sK9,sK8)
| v3_orders_2(k2_yellow_2(sK8,sK8,sK9))
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f3069,f422]) ).
fof(f3071,plain,
( ~ v7_waybel_1(sK9,sK8)
| v3_orders_2(k2_yellow_2(sK8,sK8,sK9))
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f3070,f421]) ).
fof(f3072,plain,
( v3_orders_2(k2_yellow_2(sK8,sK8,sK9))
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f3071,f420]) ).
fof(f3073,plain,
( spl31_68
| spl31_5 ),
inference(avatar_split_clause,[],[f3072,f921,f2767]) ).
fof(f3076,plain,
( v3_struct_0(sK8)
| ~ v2_orders_2(sK8)
| ~ v3_orders_2(sK8)
| ~ v4_orders_2(sK8)
| ~ l1_orders_2(sK8)
| ~ v1_funct_1(sK9)
| ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ v7_waybel_1(sK9,sK8)
| v2_orders_2(k2_yellow_2(sK8,sK8,sK9)) ),
inference(resolution,[],[f689,f882]) ).
fof(f3100,plain,
( ~ v2_orders_2(sK8)
| ~ v3_orders_2(sK8)
| ~ v4_orders_2(sK8)
| ~ l1_orders_2(sK8)
| ~ v1_funct_1(sK9)
| ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ v7_waybel_1(sK9,sK8)
| v2_orders_2(k2_yellow_2(sK8,sK8,sK9))
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f3076,f922]) ).
fof(f3103,plain,
( ~ v3_orders_2(sK8)
| ~ v4_orders_2(sK8)
| ~ l1_orders_2(sK8)
| ~ v1_funct_1(sK9)
| ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ v7_waybel_1(sK9,sK8)
| v2_orders_2(k2_yellow_2(sK8,sK8,sK9))
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f3100,f418]) ).
fof(f3105,plain,
( ~ v4_orders_2(sK8)
| ~ l1_orders_2(sK8)
| ~ v1_funct_1(sK9)
| ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ v7_waybel_1(sK9,sK8)
| v2_orders_2(k2_yellow_2(sK8,sK8,sK9))
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f3103,f417]) ).
fof(f3106,plain,
( ~ l1_orders_2(sK8)
| ~ v1_funct_1(sK9)
| ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ v7_waybel_1(sK9,sK8)
| v2_orders_2(k2_yellow_2(sK8,sK8,sK9))
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f3105,f416]) ).
fof(f3107,plain,
( ~ v1_funct_1(sK9)
| ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ v7_waybel_1(sK9,sK8)
| v2_orders_2(k2_yellow_2(sK8,sK8,sK9))
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f3106,f412]) ).
fof(f3108,plain,
( ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ v7_waybel_1(sK9,sK8)
| v2_orders_2(k2_yellow_2(sK8,sK8,sK9))
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f3107,f422]) ).
fof(f3109,plain,
( ~ v7_waybel_1(sK9,sK8)
| v2_orders_2(k2_yellow_2(sK8,sK8,sK9))
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f3108,f421]) ).
fof(f3110,plain,
( v2_orders_2(k2_yellow_2(sK8,sK8,sK9))
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f3109,f420]) ).
fof(f3111,plain,
( $false
| spl31_5
| spl31_69 ),
inference(forward_subsumption_resolution,[],[f3110,f2773]) ).
fof(f3112,plain,
( spl31_5
| spl31_69 ),
inference(avatar_contradiction_clause,[],[f3111]) ).
fof(f3262,plain,
( v3_struct_0(sK8)
| ~ v2_orders_2(sK8)
| ~ v3_orders_2(sK8)
| ~ v4_orders_2(sK8)
| ~ l1_orders_2(sK8)
| ~ v1_funct_1(sK9)
| ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ v7_waybel_1(sK9,sK8)
| v7_yellow_0(k2_yellow_2(sK8,sK8,sK9),sK8) ),
inference(resolution,[],[f684,f882]) ).
fof(f3289,plain,
( ~ v2_orders_2(sK8)
| ~ v3_orders_2(sK8)
| ~ v4_orders_2(sK8)
| ~ l1_orders_2(sK8)
| ~ v1_funct_1(sK9)
| ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ v7_waybel_1(sK9,sK8)
| v7_yellow_0(k2_yellow_2(sK8,sK8,sK9),sK8)
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f3262,f922]) ).
fof(f3292,plain,
( ~ v3_orders_2(sK8)
| ~ v4_orders_2(sK8)
| ~ l1_orders_2(sK8)
| ~ v1_funct_1(sK9)
| ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ v7_waybel_1(sK9,sK8)
| v7_yellow_0(k2_yellow_2(sK8,sK8,sK9),sK8)
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f3289,f418]) ).
fof(f3294,plain,
( ~ v4_orders_2(sK8)
| ~ l1_orders_2(sK8)
| ~ v1_funct_1(sK9)
| ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ v7_waybel_1(sK9,sK8)
| v7_yellow_0(k2_yellow_2(sK8,sK8,sK9),sK8)
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f3292,f417]) ).
fof(f3295,plain,
( ~ l1_orders_2(sK8)
| ~ v1_funct_1(sK9)
| ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ v7_waybel_1(sK9,sK8)
| v7_yellow_0(k2_yellow_2(sK8,sK8,sK9),sK8)
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f3294,f416]) ).
fof(f3296,plain,
( ~ v1_funct_1(sK9)
| ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ v7_waybel_1(sK9,sK8)
| v7_yellow_0(k2_yellow_2(sK8,sK8,sK9),sK8)
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f3295,f412]) ).
fof(f3297,plain,
( ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ v7_waybel_1(sK9,sK8)
| v7_yellow_0(k2_yellow_2(sK8,sK8,sK9),sK8)
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f3296,f422]) ).
fof(f3298,plain,
( ~ v7_waybel_1(sK9,sK8)
| v7_yellow_0(k2_yellow_2(sK8,sK8,sK9),sK8)
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f3297,f421]) ).
fof(f3299,plain,
( v7_yellow_0(k2_yellow_2(sK8,sK8,sK9),sK8)
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f3298,f420]) ).
fof(f3301,plain,
( v5_yellow_0(k2_yellow_2(sK8,sK8,sK9),sK8)
| ~ m1_yellow_0(k2_yellow_2(sK8,sK8,sK9),sK8)
| v3_struct_0(sK8)
| ~ l1_orders_2(sK8)
| spl31_5 ),
inference(resolution,[],[f3299,f692]) ).
fof(f3302,plain,
( v5_yellow_0(k2_yellow_2(sK8,sK8,sK9),sK8)
| v3_struct_0(sK8)
| ~ l1_orders_2(sK8)
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f3301,f2658]) ).
fof(f3303,plain,
( v5_yellow_0(k2_yellow_2(sK8,sK8,sK9),sK8)
| ~ l1_orders_2(sK8)
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f3302,f922]) ).
fof(f3304,plain,
( v5_yellow_0(k2_yellow_2(sK8,sK8,sK9),sK8)
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f3303,f412]) ).
fof(f3339,plain,
( v3_struct_0(k2_yellow_2(sK8,sK8,sK9))
| ~ v4_yellow_0(k2_yellow_2(sK8,sK8,sK9),sK8)
| v2_lattice3(k2_yellow_2(sK8,sK8,sK9))
| ~ m1_yellow_0(k2_yellow_2(sK8,sK8,sK9),sK8)
| ~ v3_orders_2(sK8)
| ~ v4_orders_2(sK8)
| ~ v2_lattice3(sK8)
| ~ l1_orders_2(sK8)
| spl31_5 ),
inference(resolution,[],[f3304,f695]) ).
fof(f3340,plain,
( ~ v4_yellow_0(k2_yellow_2(sK8,sK8,sK9),sK8)
| v2_lattice3(k2_yellow_2(sK8,sK8,sK9))
| ~ m1_yellow_0(k2_yellow_2(sK8,sK8,sK9),sK8)
| ~ v3_orders_2(sK8)
| ~ v4_orders_2(sK8)
| ~ v2_lattice3(sK8)
| ~ l1_orders_2(sK8)
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f3339,f2594]) ).
fof(f3341,plain,
( v2_lattice3(k2_yellow_2(sK8,sK8,sK9))
| ~ m1_yellow_0(k2_yellow_2(sK8,sK8,sK9),sK8)
| ~ v3_orders_2(sK8)
| ~ v4_orders_2(sK8)
| ~ v2_lattice3(sK8)
| ~ l1_orders_2(sK8)
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f3340,f2722]) ).
fof(f3342,plain,
( v2_lattice3(k2_yellow_2(sK8,sK8,sK9))
| ~ v3_orders_2(sK8)
| ~ v4_orders_2(sK8)
| ~ v2_lattice3(sK8)
| ~ l1_orders_2(sK8)
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f3341,f2658]) ).
fof(f3343,plain,
( v2_lattice3(k2_yellow_2(sK8,sK8,sK9))
| ~ v4_orders_2(sK8)
| ~ v2_lattice3(sK8)
| ~ l1_orders_2(sK8)
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f3342,f417]) ).
fof(f3344,plain,
( v2_lattice3(k2_yellow_2(sK8,sK8,sK9))
| ~ v2_lattice3(sK8)
| ~ l1_orders_2(sK8)
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f3343,f416]) ).
fof(f3345,plain,
( v2_lattice3(k2_yellow_2(sK8,sK8,sK9))
| ~ l1_orders_2(sK8)
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f3344,f414]) ).
fof(f3346,plain,
( v2_lattice3(k2_yellow_2(sK8,sK8,sK9))
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f3345,f412]) ).
fof(f3347,plain,
( spl31_65
| spl31_5 ),
inference(avatar_split_clause,[],[f3346,f921,f2755]) ).
fof(f3430,plain,
( ~ v2_orders_2(sK8)
| ~ v3_orders_2(sK8)
| ~ v4_orders_2(sK8)
| ~ v1_lattice3(sK8)
| ~ v2_lattice3(sK8)
| ~ v3_lattice3(sK8)
| ~ l1_orders_2(sK8)
| ~ v1_funct_1(sK9)
| ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ v6_waybel_1(sK9,sK8)
| sP3(sK9,sK8) ),
inference(resolution,[],[f618,f882]) ).
fof(f3457,plain,
( ~ v3_orders_2(sK8)
| ~ v4_orders_2(sK8)
| ~ v1_lattice3(sK8)
| ~ v2_lattice3(sK8)
| ~ v3_lattice3(sK8)
| ~ l1_orders_2(sK8)
| ~ v1_funct_1(sK9)
| ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ v6_waybel_1(sK9,sK8)
| sP3(sK9,sK8) ),
inference(forward_subsumption_resolution,[],[f3430,f418]) ).
fof(f3464,plain,
( ~ v4_orders_2(sK8)
| ~ v1_lattice3(sK8)
| ~ v2_lattice3(sK8)
| ~ v3_lattice3(sK8)
| ~ l1_orders_2(sK8)
| ~ v1_funct_1(sK9)
| ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ v6_waybel_1(sK9,sK8)
| sP3(sK9,sK8) ),
inference(forward_subsumption_resolution,[],[f3457,f417]) ).
fof(f3468,plain,
( ~ v1_lattice3(sK8)
| ~ v2_lattice3(sK8)
| ~ v3_lattice3(sK8)
| ~ l1_orders_2(sK8)
| ~ v1_funct_1(sK9)
| ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ v6_waybel_1(sK9,sK8)
| sP3(sK9,sK8) ),
inference(forward_subsumption_resolution,[],[f3464,f416]) ).
fof(f3471,plain,
( ~ v2_lattice3(sK8)
| ~ v3_lattice3(sK8)
| ~ l1_orders_2(sK8)
| ~ v1_funct_1(sK9)
| ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ v6_waybel_1(sK9,sK8)
| sP3(sK9,sK8) ),
inference(forward_subsumption_resolution,[],[f3468,f415]) ).
fof(f3474,plain,
( ~ v3_lattice3(sK8)
| ~ l1_orders_2(sK8)
| ~ v1_funct_1(sK9)
| ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ v6_waybel_1(sK9,sK8)
| sP3(sK9,sK8) ),
inference(forward_subsumption_resolution,[],[f3471,f414]) ).
fof(f3475,plain,
( ~ l1_orders_2(sK8)
| ~ v1_funct_1(sK9)
| ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ v6_waybel_1(sK9,sK8)
| sP3(sK9,sK8) ),
inference(forward_subsumption_resolution,[],[f3474,f413]) ).
fof(f3476,plain,
( ~ v1_funct_1(sK9)
| ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ v6_waybel_1(sK9,sK8)
| sP3(sK9,sK8) ),
inference(forward_subsumption_resolution,[],[f3475,f412]) ).
fof(f3477,plain,
( ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ v6_waybel_1(sK9,sK8)
| sP3(sK9,sK8) ),
inference(forward_subsumption_resolution,[],[f3476,f422]) ).
fof(f3478,plain,
( ~ v6_waybel_1(sK9,sK8)
| sP3(sK9,sK8) ),
inference(forward_subsumption_resolution,[],[f3477,f421]) ).
fof(f3479,plain,
( sP3(sK9,sK8)
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f3478,f2067]) ).
fof(f3480,plain,
( $false
| spl31_5
| spl31_64 ),
inference(forward_subsumption_resolution,[],[f3479,f2804]) ).
fof(f3481,plain,
( spl31_5
| spl31_64 ),
inference(avatar_contradiction_clause,[],[f3480]) ).
fof(f4214,plain,
( ~ v1_funct_1(sK9)
| ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ v7_waybel_1(sK9,sK8)
| k2_waybel_1(sK8,sK8,sK9) = k1_waybel34(k2_yellow_2(sK8,sK8,sK9),sK8,k3_waybel_1(sK8,sK8,sK9))
| ~ v2_orders_2(sK8)
| ~ v3_orders_2(sK8)
| ~ v4_orders_2(sK8)
| ~ v1_lattice3(sK8)
| ~ v2_lattice3(sK8)
| ~ v3_lattice3(sK8)
| ~ l1_orders_2(sK8) ),
inference(resolution,[],[f425,f419]) ).
fof(f4222,plain,
( ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ v7_waybel_1(sK9,sK8)
| k2_waybel_1(sK8,sK8,sK9) = k1_waybel34(k2_yellow_2(sK8,sK8,sK9),sK8,k3_waybel_1(sK8,sK8,sK9))
| ~ v2_orders_2(sK8)
| ~ v3_orders_2(sK8)
| ~ v4_orders_2(sK8)
| ~ v1_lattice3(sK8)
| ~ v2_lattice3(sK8)
| ~ v3_lattice3(sK8)
| ~ l1_orders_2(sK8) ),
inference(forward_subsumption_resolution,[],[f4214,f422]) ).
fof(f4224,plain,
( ~ v7_waybel_1(sK9,sK8)
| k2_waybel_1(sK8,sK8,sK9) = k1_waybel34(k2_yellow_2(sK8,sK8,sK9),sK8,k3_waybel_1(sK8,sK8,sK9))
| ~ v2_orders_2(sK8)
| ~ v3_orders_2(sK8)
| ~ v4_orders_2(sK8)
| ~ v1_lattice3(sK8)
| ~ v2_lattice3(sK8)
| ~ v3_lattice3(sK8)
| ~ l1_orders_2(sK8) ),
inference(forward_subsumption_resolution,[],[f4222,f421]) ).
fof(f4226,plain,
( k2_waybel_1(sK8,sK8,sK9) = k1_waybel34(k2_yellow_2(sK8,sK8,sK9),sK8,k3_waybel_1(sK8,sK8,sK9))
| ~ v2_orders_2(sK8)
| ~ v3_orders_2(sK8)
| ~ v4_orders_2(sK8)
| ~ v1_lattice3(sK8)
| ~ v2_lattice3(sK8)
| ~ v3_lattice3(sK8)
| ~ l1_orders_2(sK8) ),
inference(forward_subsumption_resolution,[],[f4224,f420]) ).
fof(f4227,plain,
( k2_waybel_1(sK8,sK8,sK9) = k1_waybel34(k2_yellow_2(sK8,sK8,sK9),sK8,k3_waybel_1(sK8,sK8,sK9))
| ~ v3_orders_2(sK8)
| ~ v4_orders_2(sK8)
| ~ v1_lattice3(sK8)
| ~ v2_lattice3(sK8)
| ~ v3_lattice3(sK8)
| ~ l1_orders_2(sK8) ),
inference(forward_subsumption_resolution,[],[f4226,f418]) ).
fof(f4228,plain,
( k2_waybel_1(sK8,sK8,sK9) = k1_waybel34(k2_yellow_2(sK8,sK8,sK9),sK8,k3_waybel_1(sK8,sK8,sK9))
| ~ v4_orders_2(sK8)
| ~ v1_lattice3(sK8)
| ~ v2_lattice3(sK8)
| ~ v3_lattice3(sK8)
| ~ l1_orders_2(sK8) ),
inference(forward_subsumption_resolution,[],[f4227,f417]) ).
fof(f4229,plain,
( k2_waybel_1(sK8,sK8,sK9) = k1_waybel34(k2_yellow_2(sK8,sK8,sK9),sK8,k3_waybel_1(sK8,sK8,sK9))
| ~ v1_lattice3(sK8)
| ~ v2_lattice3(sK8)
| ~ v3_lattice3(sK8)
| ~ l1_orders_2(sK8) ),
inference(forward_subsumption_resolution,[],[f4228,f416]) ).
fof(f4230,plain,
( k2_waybel_1(sK8,sK8,sK9) = k1_waybel34(k2_yellow_2(sK8,sK8,sK9),sK8,k3_waybel_1(sK8,sK8,sK9))
| ~ v2_lattice3(sK8)
| ~ v3_lattice3(sK8)
| ~ l1_orders_2(sK8) ),
inference(forward_subsumption_resolution,[],[f4229,f415]) ).
fof(f4231,plain,
( k2_waybel_1(sK8,sK8,sK9) = k1_waybel34(k2_yellow_2(sK8,sK8,sK9),sK8,k3_waybel_1(sK8,sK8,sK9))
| ~ v3_lattice3(sK8)
| ~ l1_orders_2(sK8) ),
inference(forward_subsumption_resolution,[],[f4230,f414]) ).
fof(f4232,plain,
( k2_waybel_1(sK8,sK8,sK9) = k1_waybel34(k2_yellow_2(sK8,sK8,sK9),sK8,k3_waybel_1(sK8,sK8,sK9))
| ~ l1_orders_2(sK8) ),
inference(forward_subsumption_resolution,[],[f4231,f413]) ).
fof(f4233,plain,
k2_waybel_1(sK8,sK8,sK9) = k1_waybel34(k2_yellow_2(sK8,sK8,sK9),sK8,k3_waybel_1(sK8,sK8,sK9)),
inference(forward_subsumption_resolution,[],[f4232,f412]) ).
fof(f4853,definition,
( spl31_101
<=> v1_funct_2(k3_waybel_1(sK8,sK8,sK9),u1_struct_0(k2_yellow_2(sK8,sK8,sK9)),u1_struct_0(sK8)) ),
introduced(definition,[new_symbols(definition,[spl31_101])],[avatar_definition]) ).
fof(f4855,plain,
( ~ v1_funct_2(k3_waybel_1(sK8,sK8,sK9),u1_struct_0(k2_yellow_2(sK8,sK8,sK9)),u1_struct_0(sK8))
| spl31_101 ),
inference(avatar_component_clause,[],[f4853]) ).
fof(f4875,definition,
( spl31_104
<=> v17_waybel_0(k3_waybel_1(sK8,sK8,sK9),k2_yellow_2(sK8,sK8,sK9),sK8) ),
introduced(definition,[new_symbols(definition,[spl31_104])],[avatar_definition]) ).
fof(f4877,plain,
( ~ v17_waybel_0(k3_waybel_1(sK8,sK8,sK9),k2_yellow_2(sK8,sK8,sK9),sK8)
| spl31_104 ),
inference(avatar_component_clause,[],[f4875]) ).
fof(f4898,plain,
( v1_waybel34(k2_waybel_1(sK8,sK8,sK9),sK8,k2_yellow_2(sK8,sK8,sK9))
| ~ v22_waybel_0(k3_waybel_1(sK8,sK8,sK9),k2_yellow_2(sK8,sK8,sK9),sK8)
| ~ v1_funct_1(k3_waybel_1(sK8,sK8,sK9))
| ~ v1_funct_2(k3_waybel_1(sK8,sK8,sK9),u1_struct_0(k2_yellow_2(sK8,sK8,sK9)),u1_struct_0(sK8))
| ~ v17_waybel_0(k3_waybel_1(sK8,sK8,sK9),k2_yellow_2(sK8,sK8,sK9),sK8)
| ~ m2_relset_1(k3_waybel_1(sK8,sK8,sK9),u1_struct_0(k2_yellow_2(sK8,sK8,sK9)),u1_struct_0(sK8))
| ~ v2_orders_2(sK8)
| ~ v3_orders_2(sK8)
| ~ v4_orders_2(sK8)
| ~ v1_lattice3(sK8)
| ~ v2_lattice3(sK8)
| ~ v3_lattice3(sK8)
| ~ l1_orders_2(sK8)
| ~ v2_orders_2(k2_yellow_2(sK8,sK8,sK9))
| ~ v3_orders_2(k2_yellow_2(sK8,sK8,sK9))
| ~ v4_orders_2(k2_yellow_2(sK8,sK8,sK9))
| ~ v1_lattice3(k2_yellow_2(sK8,sK8,sK9))
| ~ v2_lattice3(k2_yellow_2(sK8,sK8,sK9))
| ~ v3_lattice3(k2_yellow_2(sK8,sK8,sK9))
| ~ l1_orders_2(k2_yellow_2(sK8,sK8,sK9)) ),
inference(superposition,[],[f509,f4233]) ).
fof(f4899,plain,
( ~ v22_waybel_0(k3_waybel_1(sK8,sK8,sK9),k2_yellow_2(sK8,sK8,sK9),sK8)
| ~ v1_funct_1(k3_waybel_1(sK8,sK8,sK9))
| ~ v1_funct_2(k3_waybel_1(sK8,sK8,sK9),u1_struct_0(k2_yellow_2(sK8,sK8,sK9)),u1_struct_0(sK8))
| ~ v17_waybel_0(k3_waybel_1(sK8,sK8,sK9),k2_yellow_2(sK8,sK8,sK9),sK8)
| ~ m2_relset_1(k3_waybel_1(sK8,sK8,sK9),u1_struct_0(k2_yellow_2(sK8,sK8,sK9)),u1_struct_0(sK8))
| ~ v2_orders_2(sK8)
| ~ v3_orders_2(sK8)
| ~ v4_orders_2(sK8)
| ~ v1_lattice3(sK8)
| ~ v2_lattice3(sK8)
| ~ v3_lattice3(sK8)
| ~ l1_orders_2(sK8)
| ~ v2_orders_2(k2_yellow_2(sK8,sK8,sK9))
| ~ v3_orders_2(k2_yellow_2(sK8,sK8,sK9))
| ~ v4_orders_2(k2_yellow_2(sK8,sK8,sK9))
| ~ v1_lattice3(k2_yellow_2(sK8,sK8,sK9))
| ~ v2_lattice3(k2_yellow_2(sK8,sK8,sK9))
| ~ v3_lattice3(k2_yellow_2(sK8,sK8,sK9))
| ~ l1_orders_2(k2_yellow_2(sK8,sK8,sK9)) ),
inference(forward_subsumption_resolution,[],[f4898,f424]) ).
fof(f4900,plain,
( ~ v22_waybel_0(k3_waybel_1(sK8,sK8,sK9),k2_yellow_2(sK8,sK8,sK9),sK8)
| ~ v1_funct_2(k3_waybel_1(sK8,sK8,sK9),u1_struct_0(k2_yellow_2(sK8,sK8,sK9)),u1_struct_0(sK8))
| ~ v17_waybel_0(k3_waybel_1(sK8,sK8,sK9),k2_yellow_2(sK8,sK8,sK9),sK8)
| ~ m2_relset_1(k3_waybel_1(sK8,sK8,sK9),u1_struct_0(k2_yellow_2(sK8,sK8,sK9)),u1_struct_0(sK8))
| ~ v2_orders_2(sK8)
| ~ v3_orders_2(sK8)
| ~ v4_orders_2(sK8)
| ~ v1_lattice3(sK8)
| ~ v2_lattice3(sK8)
| ~ v3_lattice3(sK8)
| ~ l1_orders_2(sK8)
| ~ v2_orders_2(k2_yellow_2(sK8,sK8,sK9))
| ~ v3_orders_2(k2_yellow_2(sK8,sK8,sK9))
| ~ v4_orders_2(k2_yellow_2(sK8,sK8,sK9))
| ~ v1_lattice3(k2_yellow_2(sK8,sK8,sK9))
| ~ v2_lattice3(k2_yellow_2(sK8,sK8,sK9))
| ~ v3_lattice3(k2_yellow_2(sK8,sK8,sK9))
| ~ l1_orders_2(k2_yellow_2(sK8,sK8,sK9))
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f4899,f2456]) ).
fof(f4901,plain,
( ~ v22_waybel_0(k3_waybel_1(sK8,sK8,sK9),k2_yellow_2(sK8,sK8,sK9),sK8)
| ~ v1_funct_2(k3_waybel_1(sK8,sK8,sK9),u1_struct_0(k2_yellow_2(sK8,sK8,sK9)),u1_struct_0(sK8))
| ~ v17_waybel_0(k3_waybel_1(sK8,sK8,sK9),k2_yellow_2(sK8,sK8,sK9),sK8)
| ~ m2_relset_1(k3_waybel_1(sK8,sK8,sK9),u1_struct_0(k2_yellow_2(sK8,sK8,sK9)),u1_struct_0(sK8))
| ~ v3_orders_2(sK8)
| ~ v4_orders_2(sK8)
| ~ v1_lattice3(sK8)
| ~ v2_lattice3(sK8)
| ~ v3_lattice3(sK8)
| ~ l1_orders_2(sK8)
| ~ v2_orders_2(k2_yellow_2(sK8,sK8,sK9))
| ~ v3_orders_2(k2_yellow_2(sK8,sK8,sK9))
| ~ v4_orders_2(k2_yellow_2(sK8,sK8,sK9))
| ~ v1_lattice3(k2_yellow_2(sK8,sK8,sK9))
| ~ v2_lattice3(k2_yellow_2(sK8,sK8,sK9))
| ~ v3_lattice3(k2_yellow_2(sK8,sK8,sK9))
| ~ l1_orders_2(k2_yellow_2(sK8,sK8,sK9))
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f4900,f418]) ).
fof(f4902,plain,
( ~ v22_waybel_0(k3_waybel_1(sK8,sK8,sK9),k2_yellow_2(sK8,sK8,sK9),sK8)
| ~ v1_funct_2(k3_waybel_1(sK8,sK8,sK9),u1_struct_0(k2_yellow_2(sK8,sK8,sK9)),u1_struct_0(sK8))
| ~ v17_waybel_0(k3_waybel_1(sK8,sK8,sK9),k2_yellow_2(sK8,sK8,sK9),sK8)
| ~ m2_relset_1(k3_waybel_1(sK8,sK8,sK9),u1_struct_0(k2_yellow_2(sK8,sK8,sK9)),u1_struct_0(sK8))
| ~ v4_orders_2(sK8)
| ~ v1_lattice3(sK8)
| ~ v2_lattice3(sK8)
| ~ v3_lattice3(sK8)
| ~ l1_orders_2(sK8)
| ~ v2_orders_2(k2_yellow_2(sK8,sK8,sK9))
| ~ v3_orders_2(k2_yellow_2(sK8,sK8,sK9))
| ~ v4_orders_2(k2_yellow_2(sK8,sK8,sK9))
| ~ v1_lattice3(k2_yellow_2(sK8,sK8,sK9))
| ~ v2_lattice3(k2_yellow_2(sK8,sK8,sK9))
| ~ v3_lattice3(k2_yellow_2(sK8,sK8,sK9))
| ~ l1_orders_2(k2_yellow_2(sK8,sK8,sK9))
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f4901,f417]) ).
fof(f4903,plain,
( ~ v22_waybel_0(k3_waybel_1(sK8,sK8,sK9),k2_yellow_2(sK8,sK8,sK9),sK8)
| ~ v1_funct_2(k3_waybel_1(sK8,sK8,sK9),u1_struct_0(k2_yellow_2(sK8,sK8,sK9)),u1_struct_0(sK8))
| ~ v17_waybel_0(k3_waybel_1(sK8,sK8,sK9),k2_yellow_2(sK8,sK8,sK9),sK8)
| ~ m2_relset_1(k3_waybel_1(sK8,sK8,sK9),u1_struct_0(k2_yellow_2(sK8,sK8,sK9)),u1_struct_0(sK8))
| ~ v1_lattice3(sK8)
| ~ v2_lattice3(sK8)
| ~ v3_lattice3(sK8)
| ~ l1_orders_2(sK8)
| ~ v2_orders_2(k2_yellow_2(sK8,sK8,sK9))
| ~ v3_orders_2(k2_yellow_2(sK8,sK8,sK9))
| ~ v4_orders_2(k2_yellow_2(sK8,sK8,sK9))
| ~ v1_lattice3(k2_yellow_2(sK8,sK8,sK9))
| ~ v2_lattice3(k2_yellow_2(sK8,sK8,sK9))
| ~ v3_lattice3(k2_yellow_2(sK8,sK8,sK9))
| ~ l1_orders_2(k2_yellow_2(sK8,sK8,sK9))
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f4902,f416]) ).
fof(f4904,plain,
( ~ v22_waybel_0(k3_waybel_1(sK8,sK8,sK9),k2_yellow_2(sK8,sK8,sK9),sK8)
| ~ v1_funct_2(k3_waybel_1(sK8,sK8,sK9),u1_struct_0(k2_yellow_2(sK8,sK8,sK9)),u1_struct_0(sK8))
| ~ v17_waybel_0(k3_waybel_1(sK8,sK8,sK9),k2_yellow_2(sK8,sK8,sK9),sK8)
| ~ m2_relset_1(k3_waybel_1(sK8,sK8,sK9),u1_struct_0(k2_yellow_2(sK8,sK8,sK9)),u1_struct_0(sK8))
| ~ v2_lattice3(sK8)
| ~ v3_lattice3(sK8)
| ~ l1_orders_2(sK8)
| ~ v2_orders_2(k2_yellow_2(sK8,sK8,sK9))
| ~ v3_orders_2(k2_yellow_2(sK8,sK8,sK9))
| ~ v4_orders_2(k2_yellow_2(sK8,sK8,sK9))
| ~ v1_lattice3(k2_yellow_2(sK8,sK8,sK9))
| ~ v2_lattice3(k2_yellow_2(sK8,sK8,sK9))
| ~ v3_lattice3(k2_yellow_2(sK8,sK8,sK9))
| ~ l1_orders_2(k2_yellow_2(sK8,sK8,sK9))
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f4903,f415]) ).
fof(f4905,plain,
( ~ v22_waybel_0(k3_waybel_1(sK8,sK8,sK9),k2_yellow_2(sK8,sK8,sK9),sK8)
| ~ v1_funct_2(k3_waybel_1(sK8,sK8,sK9),u1_struct_0(k2_yellow_2(sK8,sK8,sK9)),u1_struct_0(sK8))
| ~ v17_waybel_0(k3_waybel_1(sK8,sK8,sK9),k2_yellow_2(sK8,sK8,sK9),sK8)
| ~ m2_relset_1(k3_waybel_1(sK8,sK8,sK9),u1_struct_0(k2_yellow_2(sK8,sK8,sK9)),u1_struct_0(sK8))
| ~ v3_lattice3(sK8)
| ~ l1_orders_2(sK8)
| ~ v2_orders_2(k2_yellow_2(sK8,sK8,sK9))
| ~ v3_orders_2(k2_yellow_2(sK8,sK8,sK9))
| ~ v4_orders_2(k2_yellow_2(sK8,sK8,sK9))
| ~ v1_lattice3(k2_yellow_2(sK8,sK8,sK9))
| ~ v2_lattice3(k2_yellow_2(sK8,sK8,sK9))
| ~ v3_lattice3(k2_yellow_2(sK8,sK8,sK9))
| ~ l1_orders_2(k2_yellow_2(sK8,sK8,sK9))
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f4904,f414]) ).
fof(f4906,plain,
( ~ v22_waybel_0(k3_waybel_1(sK8,sK8,sK9),k2_yellow_2(sK8,sK8,sK9),sK8)
| ~ v1_funct_2(k3_waybel_1(sK8,sK8,sK9),u1_struct_0(k2_yellow_2(sK8,sK8,sK9)),u1_struct_0(sK8))
| ~ v17_waybel_0(k3_waybel_1(sK8,sK8,sK9),k2_yellow_2(sK8,sK8,sK9),sK8)
| ~ m2_relset_1(k3_waybel_1(sK8,sK8,sK9),u1_struct_0(k2_yellow_2(sK8,sK8,sK9)),u1_struct_0(sK8))
| ~ l1_orders_2(sK8)
| ~ v2_orders_2(k2_yellow_2(sK8,sK8,sK9))
| ~ v3_orders_2(k2_yellow_2(sK8,sK8,sK9))
| ~ v4_orders_2(k2_yellow_2(sK8,sK8,sK9))
| ~ v1_lattice3(k2_yellow_2(sK8,sK8,sK9))
| ~ v2_lattice3(k2_yellow_2(sK8,sK8,sK9))
| ~ v3_lattice3(k2_yellow_2(sK8,sK8,sK9))
| ~ l1_orders_2(k2_yellow_2(sK8,sK8,sK9))
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f4905,f413]) ).
fof(f4907,plain,
( ~ v22_waybel_0(k3_waybel_1(sK8,sK8,sK9),k2_yellow_2(sK8,sK8,sK9),sK8)
| ~ v1_funct_2(k3_waybel_1(sK8,sK8,sK9),u1_struct_0(k2_yellow_2(sK8,sK8,sK9)),u1_struct_0(sK8))
| ~ v17_waybel_0(k3_waybel_1(sK8,sK8,sK9),k2_yellow_2(sK8,sK8,sK9),sK8)
| ~ m2_relset_1(k3_waybel_1(sK8,sK8,sK9),u1_struct_0(k2_yellow_2(sK8,sK8,sK9)),u1_struct_0(sK8))
| ~ v2_orders_2(k2_yellow_2(sK8,sK8,sK9))
| ~ v3_orders_2(k2_yellow_2(sK8,sK8,sK9))
| ~ v4_orders_2(k2_yellow_2(sK8,sK8,sK9))
| ~ v1_lattice3(k2_yellow_2(sK8,sK8,sK9))
| ~ v2_lattice3(k2_yellow_2(sK8,sK8,sK9))
| ~ v3_lattice3(k2_yellow_2(sK8,sK8,sK9))
| ~ l1_orders_2(k2_yellow_2(sK8,sK8,sK9))
| spl31_5 ),
inference(forward_subsumption_resolution,[],[f4906,f412]) ).
fof(f4908,plain,
( ~ v22_waybel_0(k3_waybel_1(sK8,sK8,sK9),k2_yellow_2(sK8,sK8,sK9),sK8)
| ~ v1_funct_2(k3_waybel_1(sK8,sK8,sK9),u1_struct_0(k2_yellow_2(sK8,sK8,sK9)),u1_struct_0(sK8))
| ~ v17_waybel_0(k3_waybel_1(sK8,sK8,sK9),k2_yellow_2(sK8,sK8,sK9),sK8)
| ~ m2_relset_1(k3_waybel_1(sK8,sK8,sK9),u1_struct_0(k2_yellow_2(sK8,sK8,sK9)),u1_struct_0(sK8))
| ~ v3_orders_2(k2_yellow_2(sK8,sK8,sK9))
| ~ v4_orders_2(k2_yellow_2(sK8,sK8,sK9))
| ~ v1_lattice3(k2_yellow_2(sK8,sK8,sK9))
| ~ v2_lattice3(k2_yellow_2(sK8,sK8,sK9))
| ~ v3_lattice3(k2_yellow_2(sK8,sK8,sK9))
| ~ l1_orders_2(k2_yellow_2(sK8,sK8,sK9))
| spl31_5
| ~ spl31_69 ),
inference(forward_subsumption_resolution,[],[f4907,f2772]) ).
fof(f4909,plain,
( ~ v22_waybel_0(k3_waybel_1(sK8,sK8,sK9),k2_yellow_2(sK8,sK8,sK9),sK8)
| ~ v1_funct_2(k3_waybel_1(sK8,sK8,sK9),u1_struct_0(k2_yellow_2(sK8,sK8,sK9)),u1_struct_0(sK8))
| ~ v17_waybel_0(k3_waybel_1(sK8,sK8,sK9),k2_yellow_2(sK8,sK8,sK9),sK8)
| ~ m2_relset_1(k3_waybel_1(sK8,sK8,sK9),u1_struct_0(k2_yellow_2(sK8,sK8,sK9)),u1_struct_0(sK8))
| ~ v4_orders_2(k2_yellow_2(sK8,sK8,sK9))
| ~ v1_lattice3(k2_yellow_2(sK8,sK8,sK9))
| ~ v2_lattice3(k2_yellow_2(sK8,sK8,sK9))
| ~ v3_lattice3(k2_yellow_2(sK8,sK8,sK9))
| ~ l1_orders_2(k2_yellow_2(sK8,sK8,sK9))
| spl31_5
| ~ spl31_68
| ~ spl31_69 ),
inference(forward_subsumption_resolution,[],[f4908,f2768]) ).
fof(f4910,plain,
( ~ v22_waybel_0(k3_waybel_1(sK8,sK8,sK9),k2_yellow_2(sK8,sK8,sK9),sK8)
| ~ v1_funct_2(k3_waybel_1(sK8,sK8,sK9),u1_struct_0(k2_yellow_2(sK8,sK8,sK9)),u1_struct_0(sK8))
| ~ v17_waybel_0(k3_waybel_1(sK8,sK8,sK9),k2_yellow_2(sK8,sK8,sK9),sK8)
| ~ m2_relset_1(k3_waybel_1(sK8,sK8,sK9),u1_struct_0(k2_yellow_2(sK8,sK8,sK9)),u1_struct_0(sK8))
| ~ v1_lattice3(k2_yellow_2(sK8,sK8,sK9))
| ~ v2_lattice3(k2_yellow_2(sK8,sK8,sK9))
| ~ v3_lattice3(k2_yellow_2(sK8,sK8,sK9))
| ~ l1_orders_2(k2_yellow_2(sK8,sK8,sK9))
| spl31_5
| ~ spl31_67
| ~ spl31_68
| ~ spl31_69 ),
inference(forward_subsumption_resolution,[],[f4909,f2764]) ).
fof(f4911,plain,
( ~ v22_waybel_0(k3_waybel_1(sK8,sK8,sK9),k2_yellow_2(sK8,sK8,sK9),sK8)
| ~ v1_funct_2(k3_waybel_1(sK8,sK8,sK9),u1_struct_0(k2_yellow_2(sK8,sK8,sK9)),u1_struct_0(sK8))
| ~ v17_waybel_0(k3_waybel_1(sK8,sK8,sK9),k2_yellow_2(sK8,sK8,sK9),sK8)
| ~ m2_relset_1(k3_waybel_1(sK8,sK8,sK9),u1_struct_0(k2_yellow_2(sK8,sK8,sK9)),u1_struct_0(sK8))
| ~ v2_lattice3(k2_yellow_2(sK8,sK8,sK9))
| ~ v3_lattice3(k2_yellow_2(sK8,sK8,sK9))
| ~ l1_orders_2(k2_yellow_2(sK8,sK8,sK9))
| spl31_5
| ~ spl31_66
| ~ spl31_67
| ~ spl31_68
| ~ spl31_69 ),
inference(forward_subsumption_resolution,[],[f4910,f2760]) ).
fof(f4912,plain,
( ~ v22_waybel_0(k3_waybel_1(sK8,sK8,sK9),k2_yellow_2(sK8,sK8,sK9),sK8)
| ~ v1_funct_2(k3_waybel_1(sK8,sK8,sK9),u1_struct_0(k2_yellow_2(sK8,sK8,sK9)),u1_struct_0(sK8))
| ~ v17_waybel_0(k3_waybel_1(sK8,sK8,sK9),k2_yellow_2(sK8,sK8,sK9),sK8)
| ~ m2_relset_1(k3_waybel_1(sK8,sK8,sK9),u1_struct_0(k2_yellow_2(sK8,sK8,sK9)),u1_struct_0(sK8))
| ~ v3_lattice3(k2_yellow_2(sK8,sK8,sK9))
| ~ l1_orders_2(k2_yellow_2(sK8,sK8,sK9))
| spl31_5
| ~ spl31_65
| ~ spl31_66
| ~ spl31_67
| ~ spl31_68
| ~ spl31_69 ),
inference(forward_subsumption_resolution,[],[f4911,f2756]) ).
fof(f4913,plain,
( ~ v22_waybel_0(k3_waybel_1(sK8,sK8,sK9),k2_yellow_2(sK8,sK8,sK9),sK8)
| ~ v1_funct_2(k3_waybel_1(sK8,sK8,sK9),u1_struct_0(k2_yellow_2(sK8,sK8,sK9)),u1_struct_0(sK8))
| ~ v17_waybel_0(k3_waybel_1(sK8,sK8,sK9),k2_yellow_2(sK8,sK8,sK9),sK8)
| ~ m2_relset_1(k3_waybel_1(sK8,sK8,sK9),u1_struct_0(k2_yellow_2(sK8,sK8,sK9)),u1_struct_0(sK8))
| ~ l1_orders_2(k2_yellow_2(sK8,sK8,sK9))
| spl31_5
| ~ spl31_64
| ~ spl31_65
| ~ spl31_66
| ~ spl31_67
| ~ spl31_68
| ~ spl31_69 ),
inference(forward_subsumption_resolution,[],[f4912,f2752]) ).
fof(f4914,plain,
( ~ v22_waybel_0(k3_waybel_1(sK8,sK8,sK9),k2_yellow_2(sK8,sK8,sK9),sK8)
| ~ v1_funct_2(k3_waybel_1(sK8,sK8,sK9),u1_struct_0(k2_yellow_2(sK8,sK8,sK9)),u1_struct_0(sK8))
| ~ v17_waybel_0(k3_waybel_1(sK8,sK8,sK9),k2_yellow_2(sK8,sK8,sK9),sK8)
| ~ m2_relset_1(k3_waybel_1(sK8,sK8,sK9),u1_struct_0(k2_yellow_2(sK8,sK8,sK9)),u1_struct_0(sK8))
| spl31_5
| ~ spl31_61
| ~ spl31_64
| ~ spl31_65
| ~ spl31_66
| ~ spl31_67
| ~ spl31_68
| ~ spl31_69 ),
inference(forward_subsumption_resolution,[],[f4913,f2530]) ).
fof(f4916,definition,
( spl31_109
<=> m2_relset_1(k3_waybel_1(sK8,sK8,sK9),u1_struct_0(k2_yellow_2(sK8,sK8,sK9)),u1_struct_0(sK8)) ),
introduced(definition,[new_symbols(definition,[spl31_109])],[avatar_definition]) ).
fof(f4918,plain,
( ~ m2_relset_1(k3_waybel_1(sK8,sK8,sK9),u1_struct_0(k2_yellow_2(sK8,sK8,sK9)),u1_struct_0(sK8))
| spl31_109 ),
inference(avatar_component_clause,[],[f4916]) ).
fof(f4920,definition,
( spl31_110
<=> v22_waybel_0(k3_waybel_1(sK8,sK8,sK9),k2_yellow_2(sK8,sK8,sK9),sK8) ),
introduced(definition,[new_symbols(definition,[spl31_110])],[avatar_definition]) ).
fof(f4922,plain,
( ~ v22_waybel_0(k3_waybel_1(sK8,sK8,sK9),k2_yellow_2(sK8,sK8,sK9),sK8)
| spl31_110 ),
inference(avatar_component_clause,[],[f4920]) ).
fof(f4923,plain,
( ~ spl31_109
| ~ spl31_104
| ~ spl31_101
| ~ spl31_110
| spl31_5
| ~ spl31_61
| ~ spl31_64
| ~ spl31_65
| ~ spl31_66
| ~ spl31_67
| ~ spl31_68
| ~ spl31_69 ),
inference(avatar_split_clause,[],[f4914,f2771,f2767,f2763,f2759,f2755,f2751,f2529,f921,f4920,f4853,f4875,f4916]) ).
fof(f4924,plain,
( v3_struct_0(sK8)
| ~ l1_orders_2(sK8)
| v3_struct_0(sK8)
| ~ l1_orders_2(sK8)
| ~ v1_funct_1(sK9)
| ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ m1_relset_1(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| spl31_101 ),
inference(resolution,[],[f4855,f522]) ).
fof(f4925,plain,
( v3_struct_0(sK8)
| ~ l1_orders_2(sK8)
| ~ v1_funct_1(sK9)
| ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ m1_relset_1(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| spl31_101 ),
inference(duplicate_literal_removal,[],[f4924]) ).
fof(f4926,plain,
( ~ l1_orders_2(sK8)
| ~ v1_funct_1(sK9)
| ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ m1_relset_1(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| spl31_5
| spl31_101 ),
inference(forward_subsumption_resolution,[],[f4925,f922]) ).
fof(f4927,plain,
( ~ v1_funct_1(sK9)
| ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ m1_relset_1(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| spl31_5
| spl31_101 ),
inference(forward_subsumption_resolution,[],[f4926,f412]) ).
fof(f4928,plain,
( ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ m1_relset_1(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| spl31_5
| spl31_101 ),
inference(forward_subsumption_resolution,[],[f4927,f422]) ).
fof(f4929,plain,
( ~ m1_relset_1(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| spl31_5
| spl31_101 ),
inference(forward_subsumption_resolution,[],[f4928,f421]) ).
fof(f4930,plain,
( $false
| spl31_5
| spl31_101 ),
inference(forward_subsumption_resolution,[],[f4929,f882]) ).
fof(f4931,plain,
( spl31_5
| spl31_101 ),
inference(avatar_contradiction_clause,[],[f4930]) ).
fof(f5033,plain,
( ~ v1_funct_1(sK9)
| ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ v7_waybel_1(sK9,sK8)
| ~ m2_relset_1(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ v2_orders_2(sK8)
| ~ v3_orders_2(sK8)
| ~ v4_orders_2(sK8)
| ~ v1_lattice3(sK8)
| ~ v2_lattice3(sK8)
| ~ v3_lattice3(sK8)
| ~ l1_orders_2(sK8)
| spl31_104 ),
inference(resolution,[],[f4877,f427]) ).
fof(f5034,plain,
( ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ v7_waybel_1(sK9,sK8)
| ~ m2_relset_1(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ v2_orders_2(sK8)
| ~ v3_orders_2(sK8)
| ~ v4_orders_2(sK8)
| ~ v1_lattice3(sK8)
| ~ v2_lattice3(sK8)
| ~ v3_lattice3(sK8)
| ~ l1_orders_2(sK8)
| spl31_104 ),
inference(forward_subsumption_resolution,[],[f5033,f422]) ).
fof(f5035,plain,
( ~ v7_waybel_1(sK9,sK8)
| ~ m2_relset_1(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ v2_orders_2(sK8)
| ~ v3_orders_2(sK8)
| ~ v4_orders_2(sK8)
| ~ v1_lattice3(sK8)
| ~ v2_lattice3(sK8)
| ~ v3_lattice3(sK8)
| ~ l1_orders_2(sK8)
| spl31_104 ),
inference(forward_subsumption_resolution,[],[f5034,f421]) ).
fof(f5036,plain,
( ~ m2_relset_1(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ v2_orders_2(sK8)
| ~ v3_orders_2(sK8)
| ~ v4_orders_2(sK8)
| ~ v1_lattice3(sK8)
| ~ v2_lattice3(sK8)
| ~ v3_lattice3(sK8)
| ~ l1_orders_2(sK8)
| spl31_104 ),
inference(forward_subsumption_resolution,[],[f5035,f420]) ).
fof(f5037,plain,
( ~ v2_orders_2(sK8)
| ~ v3_orders_2(sK8)
| ~ v4_orders_2(sK8)
| ~ v1_lattice3(sK8)
| ~ v2_lattice3(sK8)
| ~ v3_lattice3(sK8)
| ~ l1_orders_2(sK8)
| spl31_104 ),
inference(forward_subsumption_resolution,[],[f5036,f419]) ).
fof(f5038,plain,
( ~ v3_orders_2(sK8)
| ~ v4_orders_2(sK8)
| ~ v1_lattice3(sK8)
| ~ v2_lattice3(sK8)
| ~ v3_lattice3(sK8)
| ~ l1_orders_2(sK8)
| spl31_104 ),
inference(forward_subsumption_resolution,[],[f5037,f418]) ).
fof(f5039,plain,
( ~ v4_orders_2(sK8)
| ~ v1_lattice3(sK8)
| ~ v2_lattice3(sK8)
| ~ v3_lattice3(sK8)
| ~ l1_orders_2(sK8)
| spl31_104 ),
inference(forward_subsumption_resolution,[],[f5038,f417]) ).
fof(f5040,plain,
( ~ v1_lattice3(sK8)
| ~ v2_lattice3(sK8)
| ~ v3_lattice3(sK8)
| ~ l1_orders_2(sK8)
| spl31_104 ),
inference(forward_subsumption_resolution,[],[f5039,f416]) ).
fof(f5041,plain,
( ~ v2_lattice3(sK8)
| ~ v3_lattice3(sK8)
| ~ l1_orders_2(sK8)
| spl31_104 ),
inference(forward_subsumption_resolution,[],[f5040,f415]) ).
fof(f5042,plain,
( ~ v3_lattice3(sK8)
| ~ l1_orders_2(sK8)
| spl31_104 ),
inference(forward_subsumption_resolution,[],[f5041,f414]) ).
fof(f5043,plain,
( ~ l1_orders_2(sK8)
| spl31_104 ),
inference(forward_subsumption_resolution,[],[f5042,f413]) ).
fof(f5044,plain,
( $false
| spl31_104 ),
inference(forward_subsumption_resolution,[],[f5043,f412]) ).
fof(f5045,plain,
spl31_104,
inference(avatar_contradiction_clause,[],[f5044]) ).
fof(f5066,plain,
( v3_struct_0(sK8)
| ~ l1_orders_2(sK8)
| v3_struct_0(sK8)
| ~ l1_orders_2(sK8)
| ~ v1_funct_1(sK9)
| ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ m1_relset_1(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| spl31_109 ),
inference(resolution,[],[f4918,f521]) ).
fof(f5067,plain,
( v3_struct_0(sK8)
| ~ l1_orders_2(sK8)
| ~ v1_funct_1(sK9)
| ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ m1_relset_1(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| spl31_109 ),
inference(duplicate_literal_removal,[],[f5066]) ).
fof(f5068,plain,
( ~ l1_orders_2(sK8)
| ~ v1_funct_1(sK9)
| ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ m1_relset_1(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| spl31_5
| spl31_109 ),
inference(forward_subsumption_resolution,[],[f5067,f922]) ).
fof(f5069,plain,
( ~ v1_funct_1(sK9)
| ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ m1_relset_1(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| spl31_5
| spl31_109 ),
inference(forward_subsumption_resolution,[],[f5068,f412]) ).
fof(f5070,plain,
( ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ m1_relset_1(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| spl31_5
| spl31_109 ),
inference(forward_subsumption_resolution,[],[f5069,f422]) ).
fof(f5071,plain,
( ~ m1_relset_1(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| spl31_5
| spl31_109 ),
inference(forward_subsumption_resolution,[],[f5070,f421]) ).
fof(f5072,plain,
( $false
| spl31_5
| spl31_109 ),
inference(forward_subsumption_resolution,[],[f5071,f882]) ).
fof(f5073,plain,
( spl31_5
| spl31_109 ),
inference(avatar_contradiction_clause,[],[f5072]) ).
fof(f5086,plain,
( ~ v4_waybel_0(k2_yellow_2(sK8,sK8,sK9),sK8)
| ~ v1_funct_1(sK9)
| ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ v7_waybel_1(sK9,sK8)
| ~ m2_relset_1(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ v2_orders_2(sK8)
| ~ v3_orders_2(sK8)
| ~ v4_orders_2(sK8)
| ~ v1_lattice3(sK8)
| ~ v2_lattice3(sK8)
| ~ v3_lattice3(sK8)
| ~ l1_orders_2(sK8)
| spl31_110 ),
inference(resolution,[],[f4922,f478]) ).
fof(f5087,plain,
( ~ v1_funct_1(sK9)
| ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ v7_waybel_1(sK9,sK8)
| ~ m2_relset_1(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ v2_orders_2(sK8)
| ~ v3_orders_2(sK8)
| ~ v4_orders_2(sK8)
| ~ v1_lattice3(sK8)
| ~ v2_lattice3(sK8)
| ~ v3_lattice3(sK8)
| ~ l1_orders_2(sK8)
| spl31_110 ),
inference(forward_subsumption_resolution,[],[f5086,f423]) ).
fof(f5088,plain,
( ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ v7_waybel_1(sK9,sK8)
| ~ m2_relset_1(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ v2_orders_2(sK8)
| ~ v3_orders_2(sK8)
| ~ v4_orders_2(sK8)
| ~ v1_lattice3(sK8)
| ~ v2_lattice3(sK8)
| ~ v3_lattice3(sK8)
| ~ l1_orders_2(sK8)
| spl31_110 ),
inference(forward_subsumption_resolution,[],[f5087,f422]) ).
fof(f5089,plain,
( ~ v7_waybel_1(sK9,sK8)
| ~ m2_relset_1(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ v2_orders_2(sK8)
| ~ v3_orders_2(sK8)
| ~ v4_orders_2(sK8)
| ~ v1_lattice3(sK8)
| ~ v2_lattice3(sK8)
| ~ v3_lattice3(sK8)
| ~ l1_orders_2(sK8)
| spl31_110 ),
inference(forward_subsumption_resolution,[],[f5088,f421]) ).
fof(f5090,plain,
( ~ m2_relset_1(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ v2_orders_2(sK8)
| ~ v3_orders_2(sK8)
| ~ v4_orders_2(sK8)
| ~ v1_lattice3(sK8)
| ~ v2_lattice3(sK8)
| ~ v3_lattice3(sK8)
| ~ l1_orders_2(sK8)
| spl31_110 ),
inference(forward_subsumption_resolution,[],[f5089,f420]) ).
fof(f5091,plain,
( ~ v2_orders_2(sK8)
| ~ v3_orders_2(sK8)
| ~ v4_orders_2(sK8)
| ~ v1_lattice3(sK8)
| ~ v2_lattice3(sK8)
| ~ v3_lattice3(sK8)
| ~ l1_orders_2(sK8)
| spl31_110 ),
inference(forward_subsumption_resolution,[],[f5090,f419]) ).
fof(f5092,plain,
( ~ v3_orders_2(sK8)
| ~ v4_orders_2(sK8)
| ~ v1_lattice3(sK8)
| ~ v2_lattice3(sK8)
| ~ v3_lattice3(sK8)
| ~ l1_orders_2(sK8)
| spl31_110 ),
inference(forward_subsumption_resolution,[],[f5091,f418]) ).
fof(f5093,plain,
( ~ v4_orders_2(sK8)
| ~ v1_lattice3(sK8)
| ~ v2_lattice3(sK8)
| ~ v3_lattice3(sK8)
| ~ l1_orders_2(sK8)
| spl31_110 ),
inference(forward_subsumption_resolution,[],[f5092,f417]) ).
fof(f5094,plain,
( ~ v1_lattice3(sK8)
| ~ v2_lattice3(sK8)
| ~ v3_lattice3(sK8)
| ~ l1_orders_2(sK8)
| spl31_110 ),
inference(forward_subsumption_resolution,[],[f5093,f416]) ).
fof(f5095,plain,
( ~ v2_lattice3(sK8)
| ~ v3_lattice3(sK8)
| ~ l1_orders_2(sK8)
| spl31_110 ),
inference(forward_subsumption_resolution,[],[f5094,f415]) ).
fof(f5096,plain,
( ~ v3_lattice3(sK8)
| ~ l1_orders_2(sK8)
| spl31_110 ),
inference(forward_subsumption_resolution,[],[f5095,f414]) ).
fof(f5097,plain,
( ~ l1_orders_2(sK8)
| spl31_110 ),
inference(forward_subsumption_resolution,[],[f5096,f413]) ).
fof(f5098,plain,
( $false
| spl31_110 ),
inference(forward_subsumption_resolution,[],[f5097,f412]) ).
fof(f5099,plain,
spl31_110,
inference(avatar_contradiction_clause,[],[f5098]) ).
cnf(s6,plain,
~ spl31_5,
inference(sat_conversion,[],[f979]) ).
cnf(s46,plain,
( spl31_5
| spl31_61 ),
inference(sat_conversion,[],[f2732]) ).
cnf(s53,plain,
( spl31_5
| ~ spl31_61
| ~ spl31_64
| spl31_66 ),
inference(sat_conversion,[],[f2802]) ).
cnf(s61,plain,
( spl31_5
| spl31_67 ),
inference(sat_conversion,[],[f3035]) ).
cnf(s62,plain,
( spl31_5
| spl31_68 ),
inference(sat_conversion,[],[f3073]) ).
cnf(s63,plain,
( spl31_5
| spl31_69 ),
inference(sat_conversion,[],[f3112]) ).
cnf(s64,plain,
( spl31_5
| spl31_65 ),
inference(sat_conversion,[],[f3347]) ).
cnf(s66,plain,
( spl31_5
| spl31_64 ),
inference(sat_conversion,[],[f3481]) ).
cnf(s86,plain,
( spl31_5
| ~ spl31_61
| ~ spl31_64
| ~ spl31_65
| ~ spl31_66
| ~ spl31_67
| ~ spl31_68
| ~ spl31_69
| ~ spl31_101
| ~ spl31_104
| ~ spl31_109
| ~ spl31_110 ),
inference(sat_conversion,[],[f4923]) ).
cnf(s87,plain,
( spl31_5
| spl31_101 ),
inference(sat_conversion,[],[f4931]) ).
cnf(s93,plain,
spl31_104,
inference(sat_conversion,[],[f5045]) ).
cnf(s95,plain,
( spl31_5
| spl31_109 ),
inference(sat_conversion,[],[f5073]) ).
cnf(s96,plain,
spl31_110,
inference(sat_conversion,[],[f5099]) ).
cnf(s97,plain,
( spl31_5
| ~ spl31_61
| ~ spl31_64
| ~ spl31_65
| ~ spl31_66
| ~ spl31_67
| ~ spl31_68
| ~ spl31_69
| ~ spl31_101
| ~ spl31_109 ),
inference(rat,[],[s86,s96,s93]) ).
cnf(s104,plain,
spl31_109,
inference(rat,[],[s95,s6]) ).
cnf(s106,plain,
spl31_101,
inference(rat,[],[s87,s6]) ).
cnf(s108,plain,
spl31_64,
inference(rat,[],[s66,s6]) ).
cnf(s109,plain,
spl31_65,
inference(rat,[],[s64,s6]) ).
cnf(s110,plain,
spl31_69,
inference(rat,[],[s63,s6]) ).
cnf(s111,plain,
spl31_68,
inference(rat,[],[s62,s6]) ).
cnf(s112,plain,
spl31_67,
inference(rat,[],[s61,s6]) ).
cnf(s113,plain,
spl31_61,
inference(rat,[],[s46,s6]) ).
cnf(s115,plain,
~ spl31_66,
inference(rat,[],[s97,s104,s106,s110,s111,s112,s108,s109,s6,s113]) ).
cnf(s116,plain,
$false,
inference(rat,[],[s53,s6,s108,s115,s113]) ).
fof(f5100,plain,
$false,
inference(avatar_sat_refutation,[],[s116]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT369+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.37 % Computer : n003.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Sun Sep 27 15:07:41 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.15/0.40 Running first-order theorem proving
% 0.15/0.40 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.86/1.32 % (659577)Detected formulas, will run a generic FOF schedule.
% 2.86/1.32 % (659586)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=579194899:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 2.86/1.32 % (659587)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1150410565:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 2.86/1.32 % (659585)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=844071387:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 2.86/1.32 % (659584)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=732650530:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 2.86/1.32 % (659582)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=3540960478:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 2.86/1.32 % (659583)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=2739665933:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 2.86/1.32 % (659585)Refutation not found, incomplete strategy
% 2.86/1.32 % (659585)------------------------------
% 2.86/1.32 % (659585)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.86/1.32 % (659585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.86/1.32 % (659585)CaDiCaL version: 2.1.3
% 2.86/1.32 % (659585)Termination reason: Refutation not found, incomplete strategy
% 2.86/1.32 % (659585)Time elapsed: 0.004 s
% 2.86/1.32 % (659585)Peak memory usage: 88 MB
% 2.86/1.32 % (659585)Instructions burned: 5 (million)
% 2.86/1.32 % (659586)Instruction limit reached!
% 2.86/1.32 % (659586)------------------------------
% 2.86/1.32 % (659586)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.86/1.32 % (659586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.86/1.32 % (659586)CaDiCaL version: 2.1.3
% 2.86/1.32 % (659586)Termination reason: Instruction limit
% 2.86/1.32 % (659586)Termination phase: Saturation
% 2.86/1.32 % (659586)Time elapsed: 0.038 s
% 2.86/1.32 % (659586)Peak memory usage: 89 MB
% 2.86/1.32 % (659586)Instructions burned: 121 (million)
% 2.86/1.32 % (659588)dis-21_1_sil=8000:lcm=predicate:random_seed=3115431664:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 2.86/1.32 % (659588)Instruction limit reached!
% 2.86/1.32 % (659588)------------------------------
% 2.86/1.32 % (659588)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.86/1.32 % (659588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.86/1.32 % (659588)CaDiCaL version: 2.1.3
% 2.86/1.32 % (659588)Termination reason: Instruction limit
% 2.86/1.32 % (659588)Termination phase: Saturation
% 2.86/1.32 % (659588)Time elapsed: 0.071 s
% 2.86/1.32 % (659588)Peak memory usage: 91 MB
% 2.86/1.32 % (659588)Instructions burned: 130 (million)
% 2.86/1.32 % (659587)Instruction limit reached!
% 2.86/1.32 % (659587)------------------------------
% 2.86/1.32 % (659587)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.86/1.32 % (659587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.86/1.32 % (659587)CaDiCaL version: 2.1.3
% 2.86/1.32 % (659587)Termination reason: Instruction limit
% 2.86/1.32 % (659587)Termination phase: Saturation
% 2.86/1.32 % (659587)Time elapsed: 0.088 s
% 2.86/1.32 % (659587)Peak memory usage: 90 MB
% 2.86/1.32 % (659587)Instructions burned: 140 (million)
% 2.86/1.32 % (659596)lrs+10_1_sil=8000:sp=occurrence:random_seed=3547208239:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 2.86/1.32 % (659596)First to succeed.
% 2.86/1.32 % (659596)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-659577"
% 2.86/1.32 % (659597)lrs+10_1_sil=32000:urr=on:br=off:random_seed=982525654:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 2.86/1.32 % (659598)lrs+1011_1_sil=32000:sp=occurrence:random_seed=786743003:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 2.86/1.32 % (659597)Refutation not found, incomplete strategy
% 2.86/1.32 % (659597)------------------------------
% 2.86/1.32 % (659597)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.86/1.32 % (659597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.86/1.32 % (659597)CaDiCaL version: 2.1.3
% 2.86/1.32 % (659597)Termination reason: Refutation not found, incomplete strategy
% 2.86/1.32 % (659597)Time elapsed: 0.018 s
% 2.86/1.32 % (659597)Peak memory usage: 89 MB
% 2.86/1.32 % (659597)Instructions burned: 31 (million)
% 2.86/1.32 % (659585)------------------------------
% 2.86/1.32 % (659585)------------------------------
% 2.86/1.32 % (659596)Refutation found. Thanks to Tanya!
% 2.86/1.32 % SZS status Theorem for theBenchmark
% 2.86/1.32 % SZS output start Proof for theBenchmark
% See solution above
% 4.01/1.51 % (659596)------------------------------
% 4.01/1.51 % (659596)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.01/1.51 % (659596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.01/1.51 % (659596)CaDiCaL version: 2.1.3
% 4.01/1.51 % (659596)Termination reason: Refutation
% 4.01/1.51 % (659596)Time elapsed: 0.075 s
% 4.01/1.51 % (659596)Peak memory usage: 92 MB
% 4.01/1.51 % (659596)Instructions burned: 269 (million)
% 4.01/1.51 % (659596)------------------------------
% 4.01/1.51 % (659596)------------------------------
% 4.01/1.51 % (659577)Success in time 0.484 s
% 4.01/1.51 % Vampire exiting
%------------------------------------------------------------------------------