%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT370+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 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:26 AM UTC 2026
% Result : Theorem 4.13s 1.58s
% Output : Refutation 0.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 40
% Number of leaves : 29
% Syntax : Number of formulae : 327 ( 33 unt; 13 def)
% Number of atoms : 2087 ( 18 equ)
% Maximal formula atoms : 25 ( 6 avg)
% Number of connectives : 3023 (1263 ~;1386 |; 320 &)
% ( 16 <=>; 38 =>; 0 <=; 0 <~>)
% Maximal formula depth : 28 ( 7 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 48 ( 46 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)
& v3_waybel_3(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( ( v1_funct_1(X1)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v7_waybel_1(X1,X0)
& m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
=> ( v1_waybel34(k2_waybel_1(X0,X0,X1),X0,k2_yellow_2(X0,X0,X1))
=> v4_waybel_0(k2_yellow_2(X0,X0,X1),X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t43_waybel34) ).
fof(f2,negated_conjecture,
~ ! [X0] :
( ( v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& v2_lattice3(X0)
& v3_lattice3(X0)
& v3_waybel_3(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( ( v1_funct_1(X1)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v7_waybel_1(X1,X0)
& m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
=> ( v1_waybel34(k2_waybel_1(X0,X0,X1),X0,k2_yellow_2(X0,X0,X1))
=> v4_waybel_0(k2_yellow_2(X0,X0,X1),X0) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(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(f56,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(f65,axiom,
! [X0,X1,X2] :
( ( ~ v3_struct_0(X0)
& l1_orders_2(X0)
& ~ v3_struct_0(X1)
& l1_orders_2(X1)
& v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> ( v1_orders_2(k2_yellow_2(X0,X1,X2))
& v4_yellow_0(k2_yellow_2(X0,X1,X2),X1)
& m1_yellow_0(k2_yellow_2(X0,X1,X2),X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k2_yellow_2) ).
fof(f67,axiom,
! [X0,X1,X2] :
( ( ~ v3_struct_0(X0)
& l1_orders_2(X0)
& ~ v3_struct_0(X1)
& l1_orders_2(X1)
& v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> ( v1_funct_1(k3_waybel_1(X0,X1,X2))
& v1_funct_2(k3_waybel_1(X0,X1,X2),u1_struct_0(k2_yellow_2(X0,X1,X2)),u1_struct_0(X1))
& m2_relset_1(k3_waybel_1(X0,X1,X2),u1_struct_0(k2_yellow_2(X0,X1,X2)),u1_struct_0(X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k3_waybel_1) ).
fof(f74,axiom,
! [X0] :
( l1_orders_2(X0)
=> ! [X1] :
( m1_yellow_0(X1,X0)
=> l1_orders_2(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m1_yellow_0) ).
fof(f84,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& l1_orders_2(X0)
& v1_funct_1(X1)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v7_waybel_1(X1,X0)
& m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
=> ( ~ v3_struct_0(k2_yellow_2(X0,X0,X1))
& v1_orders_2(k2_yellow_2(X0,X0,X1))
& v2_orders_2(k2_yellow_2(X0,X0,X1))
& v3_orders_2(k2_yellow_2(X0,X0,X1))
& v4_orders_2(k2_yellow_2(X0,X0,X1))
& v4_yellow_0(k2_yellow_2(X0,X0,X1),X0)
& v5_yellow_0(k2_yellow_2(X0,X0,X1),X0)
& v7_yellow_0(k2_yellow_2(X0,X0,X1),X0)
& v3_waybel_0(k2_yellow_2(X0,X0,X1),X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc10_waybel10) ).
fof(f85,axiom,
! [X0,X1] :
( ( v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& v2_lattice3(X0)
& v3_lattice3(X0)
& l1_orders_2(X0)
& v1_funct_1(X1)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v6_waybel_1(X1,X0)
& m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
=> ( ~ v3_struct_0(k2_yellow_2(X0,X0,X1))
& v1_orders_2(k2_yellow_2(X0,X0,X1))
& v2_orders_2(k2_yellow_2(X0,X0,X1))
& v3_orders_2(k2_yellow_2(X0,X0,X1))
& v4_orders_2(k2_yellow_2(X0,X0,X1))
& v1_yellow_0(k2_yellow_2(X0,X0,X1))
& v2_yellow_0(k2_yellow_2(X0,X0,X1))
& v3_yellow_0(k2_yellow_2(X0,X0,X1))
& v4_yellow_0(k2_yellow_2(X0,X0,X1),X0)
& v24_waybel_0(k2_yellow_2(X0,X0,X1))
& v25_waybel_0(k2_yellow_2(X0,X0,X1))
& v1_lattice3(k2_yellow_2(X0,X0,X1))
& v2_lattice3(k2_yellow_2(X0,X0,X1))
& v3_lattice3(k2_yellow_2(X0,X0,X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc10_waybel34) ).
fof(f94,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(f137,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
<=> m1_relset_1(X2,X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(f140,axiom,
! [X0] :
( ( v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& v2_lattice3(X0)
& v3_lattice3(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( ( v2_orders_2(X1)
& v3_orders_2(X1)
& v4_orders_2(X1)
& v1_lattice3(X1)
& v2_lattice3(X1)
& v3_lattice3(X1)
& v3_waybel_3(X1)
& l1_orders_2(X1) )
=> ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v17_waybel_0(X2,X0,X1)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> ( v1_waybel34(k1_waybel34(X0,X1,X2),X1,X0)
=> v22_waybel_0(X2,X0,X1) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t25_waybel34) ).
fof(f142,axiom,
! [X0] :
( ( v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& v2_lattice3(X0)
& v3_lattice3(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( ( v1_funct_1(X1)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v7_waybel_1(X1,X0)
& m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
=> ( v18_waybel_0(k2_waybel_1(X0,X0,X1),X0,k2_yellow_2(X0,X0,X1))
& v17_waybel_0(k3_waybel_1(X0,X0,X1),k2_yellow_2(X0,X0,X1),X0)
& k2_waybel34(k2_yellow_2(X0,X0,X1),X0,k2_waybel_1(X0,X0,X1)) = k3_waybel_1(X0,X0,X1)
& k1_waybel34(k2_yellow_2(X0,X0,X1),X0,k3_waybel_1(X0,X0,X1)) = k2_waybel_1(X0,X0,X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t39_waybel34) ).
fof(f144,axiom,
! [X0] :
( ( v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& v2_lattice3(X0)
& v3_lattice3(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( ( v1_funct_1(X1)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v7_waybel_1(X1,X0)
& m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
=> ( v4_waybel_0(k2_yellow_2(X0,X0,X1),X0)
<=> v22_waybel_0(k3_waybel_1(X0,X0,X1),k2_yellow_2(X0,X0,X1),X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t40_waybel34) ).
fof(f183,plain,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& l1_orders_2(X0)
& v1_funct_1(X1)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v7_waybel_1(X1,X0)
& m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
=> ( ~ v3_struct_0(k2_yellow_2(X0,X0,X1))
& v1_orders_2(k2_yellow_2(X0,X0,X1))
& v2_orders_2(k2_yellow_2(X0,X0,X1))
& v3_orders_2(k2_yellow_2(X0,X0,X1))
& v4_orders_2(k2_yellow_2(X0,X0,X1))
& v4_yellow_0(k2_yellow_2(X0,X0,X1),X0)
& v5_yellow_0(k2_yellow_2(X0,X0,X1),X0)
& v7_yellow_0(k2_yellow_2(X0,X0,X1),X0) ) ),
inference(pure_predicate_removal,[],[f84]) ).
fof(f202,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(f213,plain,
? [X0] :
( ? [X1] :
( ~ v4_waybel_0(k2_yellow_2(X0,X0,X1),X0)
& v1_waybel34(k2_waybel_1(X0,X0,X1),X0,k2_yellow_2(X0,X0,X1))
& v1_funct_1(X1)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v7_waybel_1(X1,X0)
& m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
& v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& v2_lattice3(X0)
& v3_lattice3(X0)
& v3_waybel_3(X0)
& l1_orders_2(X0) ),
inference(ennf_transformation,[],[f2]) ).
fof(f214,plain,
? [X0] :
( ? [X1] :
( ~ v4_waybel_0(k2_yellow_2(X0,X0,X1),X0)
& v1_waybel34(k2_waybel_1(X0,X0,X1),X0,k2_yellow_2(X0,X0,X1))
& v1_funct_1(X1)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v7_waybel_1(X1,X0)
& m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
& v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& v2_lattice3(X0)
& v3_lattice3(X0)
& v3_waybel_3(X0)
& l1_orders_2(X0) ),
inference(flattening,[],[f213]) ).
fof(f215,plain,
! [X0] :
( ! [X1] :
( ( v18_waybel_0(k2_waybel_1(X0,X0,X1),X0,k2_yellow_2(X0,X0,X1))
& v17_waybel_0(k3_waybel_1(X0,X0,X1),k2_yellow_2(X0,X0,X1),X0)
& k2_waybel34(k2_yellow_2(X0,X0,X1),X0,k2_waybel_1(X0,X0,X1)) = k3_waybel_1(X0,X0,X1)
& k1_waybel34(k2_yellow_2(X0,X0,X1),X0,k3_waybel_1(X0,X0,X1)) = k2_waybel_1(X0,X0,X1) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v7_waybel_1(X1,X0)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f142]) ).
fof(f216,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,[],[f215]) ).
fof(f227,plain,
! [X0] :
( ~ v3_struct_0(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f36]) ).
fof(f228,plain,
! [X0] :
( ~ v3_struct_0(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f227]) ).
fof(f229,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(f230,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,[],[f229]) ).
fof(f231,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( v22_waybel_0(X2,X0,X1)
| ~ v1_waybel34(k1_waybel34(X0,X1,X2),X1,X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v17_waybel_0(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ v3_lattice3(X1)
| ~ v3_waybel_3(X1)
| ~ l1_orders_2(X1) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f140]) ).
fof(f232,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( v22_waybel_0(X2,X0,X1)
| ~ v1_waybel34(k1_waybel34(X0,X1,X2),X1,X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v17_waybel_0(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ v3_lattice3(X1)
| ~ v3_waybel_3(X1)
| ~ l1_orders_2(X1) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f231]) ).
fof(f239,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,[],[f202]) ).
fof(f240,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,[],[f239]) ).
fof(f241,plain,
! [X0] :
( ! [X1] :
( ( v4_waybel_0(k2_yellow_2(X0,X0,X1),X0)
<=> v22_waybel_0(k3_waybel_1(X0,X0,X1),k2_yellow_2(X0,X0,X1),X0) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v7_waybel_1(X1,X0)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f144]) ).
fof(f242,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,[],[f241]) ).
fof(f256,plain,
! [X0,X1,X2] :
( ( v1_funct_1(k3_waybel_1(X0,X1,X2))
& v1_funct_2(k3_waybel_1(X0,X1,X2),u1_struct_0(k2_yellow_2(X0,X1,X2)),u1_struct_0(X1))
& m2_relset_1(k3_waybel_1(X0,X1,X2),u1_struct_0(k2_yellow_2(X0,X1,X2)),u1_struct_0(X1)) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| v3_struct_0(X1)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(ennf_transformation,[],[f67]) ).
fof(f257,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,[],[f256]) ).
fof(f278,plain,
! [X0,X1] :
( ( ~ v3_struct_0(k2_yellow_2(X0,X0,X1))
& v1_orders_2(k2_yellow_2(X0,X0,X1))
& v2_orders_2(k2_yellow_2(X0,X0,X1))
& v3_orders_2(k2_yellow_2(X0,X0,X1))
& v4_orders_2(k2_yellow_2(X0,X0,X1))
& v1_yellow_0(k2_yellow_2(X0,X0,X1))
& v2_yellow_0(k2_yellow_2(X0,X0,X1))
& v3_yellow_0(k2_yellow_2(X0,X0,X1))
& v4_yellow_0(k2_yellow_2(X0,X0,X1),X0)
& v24_waybel_0(k2_yellow_2(X0,X0,X1))
& v25_waybel_0(k2_yellow_2(X0,X0,X1))
& v1_lattice3(k2_yellow_2(X0,X0,X1))
& v2_lattice3(k2_yellow_2(X0,X0,X1))
& v3_lattice3(k2_yellow_2(X0,X0,X1)) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v6_waybel_1(X1,X0)
| ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f85]) ).
fof(f279,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,[],[f278]) ).
fof(f304,plain,
! [X0] :
( ! [X1] :
( l1_orders_2(X1)
| ~ m1_yellow_0(X1,X0) )
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f74]) ).
fof(f305,plain,
! [X0,X1,X2] :
( ( v1_orders_2(k2_yellow_2(X0,X1,X2))
& v4_yellow_0(k2_yellow_2(X0,X1,X2),X1)
& m1_yellow_0(k2_yellow_2(X0,X1,X2),X1) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| v3_struct_0(X1)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(ennf_transformation,[],[f65]) ).
fof(f306,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,[],[f305]) ).
fof(f313,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,[],[f94]) ).
fof(f314,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,[],[f313]) ).
fof(f315,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,[],[f183]) ).
fof(f316,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,[],[f315]) ).
fof(f317,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,[],[f56]) ).
fof(f318,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,[],[f317]) ).
fof(f319,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(f320,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,[],[f319]) ).
fof(f374,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(f375,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,[],[f279,f374]) ).
fof(f384,plain,
( ~ v4_waybel_0(k2_yellow_2(sK8,sK8,sK9),sK8)
& v1_waybel34(k2_waybel_1(sK8,sK8,sK9),sK8,k2_yellow_2(sK8,sK8,sK9))
& 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)
& v3_waybel_3(sK8)
& l1_orders_2(sK8) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8,sK9]),skolemize(X0,sK8),skolemize(X1,sK9)],[f214]) ).
fof(f390,plain,
! [X0,X1,X2] :
( ( m2_relset_1(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1) )
& ( m1_relset_1(X2,X0,X1)
| ~ m2_relset_1(X2,X0,X1) ) ),
inference(nnf_transformation,[],[f137]) ).
fof(f392,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,[],[f242]) ).
fof(f404,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,[],[f374]) ).
fof(f405,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,[],[f404]) ).
fof(f420,plain,
l1_orders_2(sK8),
inference(cnf_transformation,[],[f384]) ).
fof(f421,plain,
v3_waybel_3(sK8),
inference(cnf_transformation,[],[f384]) ).
fof(f422,plain,
v3_lattice3(sK8),
inference(cnf_transformation,[],[f384]) ).
fof(f423,plain,
v2_lattice3(sK8),
inference(cnf_transformation,[],[f384]) ).
fof(f424,plain,
v1_lattice3(sK8),
inference(cnf_transformation,[],[f384]) ).
fof(f425,plain,
v4_orders_2(sK8),
inference(cnf_transformation,[],[f384]) ).
fof(f426,plain,
v3_orders_2(sK8),
inference(cnf_transformation,[],[f384]) ).
fof(f427,plain,
v2_orders_2(sK8),
inference(cnf_transformation,[],[f384]) ).
fof(f428,plain,
m2_relset_1(sK9,u1_struct_0(sK8),u1_struct_0(sK8)),
inference(cnf_transformation,[],[f384]) ).
fof(f429,plain,
v7_waybel_1(sK9,sK8),
inference(cnf_transformation,[],[f384]) ).
fof(f430,plain,
v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8)),
inference(cnf_transformation,[],[f384]) ).
fof(f431,plain,
v1_funct_1(sK9),
inference(cnf_transformation,[],[f384]) ).
fof(f432,plain,
v1_waybel34(k2_waybel_1(sK8,sK8,sK9),sK8,k2_yellow_2(sK8,sK8,sK9)),
inference(cnf_transformation,[],[f384]) ).
fof(f433,plain,
~ v4_waybel_0(k2_yellow_2(sK8,sK8,sK9),sK8),
inference(cnf_transformation,[],[f384]) ).
fof(f434,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,[],[f216]) ).
fof(f436,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,[],[f216]) ).
fof(f452,plain,
! [X0] :
( ~ v3_struct_0(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f228]) ).
fof(f470,plain,
! [X0] :
( ~ l1_orders_2(X0)
| v3_struct_0(X0)
| ~ v3_lattice3(X0)
| v1_lattice3(X0) ),
inference(cnf_transformation,[],[f230]) ).
fof(f472,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)
| ~ v3_waybel_3(X1)
| ~ l1_orders_2(X1)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f232]) ).
fof(f508,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,[],[f240]) ).
fof(f512,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f390]) ).
fof(f516,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,[],[f392]) ).
fof(f557,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,[],[f257]) ).
fof(f558,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,[],[f257]) ).
fof(f559,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,[],[f257]) ).
fof(f634,plain,
! [X0,X1] :
( v3_lattice3(k2_yellow_2(X1,X1,X0))
| ~ sP3(X0,X1) ),
inference(cnf_transformation,[],[f405]) ).
fof(f648,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,[],[f375]) ).
fof(f719,plain,
! [X0,X1] :
( ~ m1_yellow_0(X1,X0)
| l1_orders_2(X1)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f304]) ).
fof(f720,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,[],[f306]) ).
fof(f729,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,[],[f314]) ).
fof(f731,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,[],[f314]) ).
fof(f732,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,[],[f316]) ).
fof(f735,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,[],[f316]) ).
fof(f736,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,[],[f316]) ).
fof(f737,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,[],[f316]) ).
fof(f740,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,[],[f318]) ).
fof(f743,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,[],[f320]) ).
fof(f920,plain,
m1_relset_1(sK9,u1_struct_0(sK8),u1_struct_0(sK8)),
inference(resolution,[],[f512,f428]) ).
fof(f955,definition,
( spl32_5
<=> v3_struct_0(sK8) ),
introduced(definition,[new_symbols(definition,[spl32_5])],[avatar_definition]) ).
fof(f956,plain,
( ~ v3_struct_0(sK8)
| spl32_5 ),
inference(avatar_component_clause,[],[f955]) ).
fof(f957,plain,
( v3_struct_0(sK8)
| ~ spl32_5 ),
inference(avatar_component_clause,[],[f955]) ).
fof(f1049,plain,
( ~ v2_lattice3(sK8)
| ~ l1_orders_2(sK8)
| ~ spl32_5 ),
inference(resolution,[],[f957,f452]) ).
fof(f1052,plain,
( ~ l1_orders_2(sK8)
| ~ spl32_5 ),
inference(forward_subsumption_resolution,[],[f1049,f423]) ).
fof(f1055,plain,
( $false
| ~ spl32_5 ),
inference(forward_subsumption_resolution,[],[f1052,f420]) ).
fof(f1056,plain,
~ spl32_5,
inference(avatar_contradiction_clause,[],[f1055]) ).
fof(f2338,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,[],[f508,f920]) ).
fof(f2362,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,[],[f2338,f431]) ).
fof(f2368,plain,
( ~ v7_waybel_1(sK9,sK8)
| v6_waybel_1(sK9,sK8)
| v3_struct_0(sK8)
| ~ l1_orders_2(sK8) ),
inference(forward_subsumption_resolution,[],[f2362,f430]) ).
fof(f2373,plain,
( v6_waybel_1(sK9,sK8)
| v3_struct_0(sK8)
| ~ l1_orders_2(sK8) ),
inference(forward_subsumption_resolution,[],[f2368,f429]) ).
fof(f2386,plain,
( v6_waybel_1(sK9,sK8)
| ~ l1_orders_2(sK8)
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f2373,f956]) ).
fof(f2398,plain,
( v6_waybel_1(sK9,sK8)
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f2386,f420]) ).
fof(f2732,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,[],[f559,f920]) ).
fof(f2755,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,[],[f2732]) ).
fof(f2768,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))
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f2755,f956]) ).
fof(f2780,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))
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f2768,f420]) ).
fof(f2784,plain,
( ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| v1_funct_1(k3_waybel_1(sK8,sK8,sK9))
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f2780,f431]) ).
fof(f2787,plain,
( v1_funct_1(k3_waybel_1(sK8,sK8,sK9))
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f2784,f430]) ).
fof(f2860,definition,
( spl32_90
<=> l1_orders_2(k2_yellow_2(sK8,sK8,sK9)) ),
introduced(definition,[new_symbols(definition,[spl32_90])],[avatar_definition]) ).
fof(f2861,plain,
( l1_orders_2(k2_yellow_2(sK8,sK8,sK9))
| ~ spl32_90 ),
inference(avatar_component_clause,[],[f2860]) ).
fof(f2862,plain,
( ~ l1_orders_2(k2_yellow_2(sK8,sK8,sK9))
| spl32_90 ),
inference(avatar_component_clause,[],[f2860]) ).
fof(f2870,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,[],[f731,f920]) ).
fof(f2893,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,[],[f2870]) ).
fof(f2906,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))
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f2893,f956]) ).
fof(f2918,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))
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f2906,f420]) ).
fof(f2922,plain,
( ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| ~ v3_struct_0(k2_yellow_2(sK8,sK8,sK9))
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f2918,f431]) ).
fof(f2925,plain,
( ~ v3_struct_0(k2_yellow_2(sK8,sK8,sK9))
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f2922,f430]) ).
fof(f2934,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,[],[f720,f920]) ).
fof(f2957,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,[],[f2934]) ).
fof(f2970,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)
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f2957,f956]) ).
fof(f2982,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)
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f2970,f420]) ).
fof(f2986,plain,
( ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| m1_yellow_0(k2_yellow_2(sK8,sK8,sK9),sK8)
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f2982,f431]) ).
fof(f2989,plain,
( m1_yellow_0(k2_yellow_2(sK8,sK8,sK9),sK8)
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f2986,f430]) ).
fof(f2998,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,[],[f729,f920]) ).
fof(f3021,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,[],[f2998]) ).
fof(f3034,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)
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f3021,f956]) ).
fof(f3046,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)
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f3034,f420]) ).
fof(f3050,plain,
( ~ v1_funct_2(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| v4_yellow_0(k2_yellow_2(sK8,sK8,sK9),sK8)
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f3046,f431]) ).
fof(f3053,plain,
( v4_yellow_0(k2_yellow_2(sK8,sK8,sK9),sK8)
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f3050,f430]) ).
fof(f3060,plain,
( l1_orders_2(k2_yellow_2(sK8,sK8,sK9))
| ~ l1_orders_2(sK8)
| spl32_5 ),
inference(resolution,[],[f2989,f719]) ).
fof(f3061,plain,
( ~ l1_orders_2(sK8)
| spl32_5
| spl32_90 ),
inference(forward_subsumption_resolution,[],[f3060,f2862]) ).
fof(f3062,plain,
( $false
| spl32_5
| spl32_90 ),
inference(forward_subsumption_resolution,[],[f3061,f420]) ).
fof(f3063,plain,
( spl32_5
| spl32_90 ),
inference(avatar_contradiction_clause,[],[f3062]) ).
fof(f3065,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))
| ~ spl32_90 ),
inference(resolution,[],[f2861,f470]) ).
fof(f3084,definition,
( spl32_93
<=> v3_lattice3(k2_yellow_2(sK8,sK8,sK9)) ),
introduced(definition,[new_symbols(definition,[spl32_93])],[avatar_definition]) ).
fof(f3085,plain,
( v3_lattice3(k2_yellow_2(sK8,sK8,sK9))
| ~ spl32_93 ),
inference(avatar_component_clause,[],[f3084]) ).
fof(f3086,plain,
( ~ v3_lattice3(k2_yellow_2(sK8,sK8,sK9))
| spl32_93 ),
inference(avatar_component_clause,[],[f3084]) ).
fof(f3088,definition,
( spl32_94
<=> v2_lattice3(k2_yellow_2(sK8,sK8,sK9)) ),
introduced(definition,[new_symbols(definition,[spl32_94])],[avatar_definition]) ).
fof(f3089,plain,
( v2_lattice3(k2_yellow_2(sK8,sK8,sK9))
| ~ spl32_94 ),
inference(avatar_component_clause,[],[f3088]) ).
fof(f3092,definition,
( spl32_95
<=> v1_lattice3(k2_yellow_2(sK8,sK8,sK9)) ),
introduced(definition,[new_symbols(definition,[spl32_95])],[avatar_definition]) ).
fof(f3093,plain,
( v1_lattice3(k2_yellow_2(sK8,sK8,sK9))
| ~ spl32_95 ),
inference(avatar_component_clause,[],[f3092]) ).
fof(f3096,definition,
( spl32_96
<=> v4_orders_2(k2_yellow_2(sK8,sK8,sK9)) ),
introduced(definition,[new_symbols(definition,[spl32_96])],[avatar_definition]) ).
fof(f3097,plain,
( v4_orders_2(k2_yellow_2(sK8,sK8,sK9))
| ~ spl32_96 ),
inference(avatar_component_clause,[],[f3096]) ).
fof(f3100,definition,
( spl32_97
<=> v3_orders_2(k2_yellow_2(sK8,sK8,sK9)) ),
introduced(definition,[new_symbols(definition,[spl32_97])],[avatar_definition]) ).
fof(f3101,plain,
( v3_orders_2(k2_yellow_2(sK8,sK8,sK9))
| ~ spl32_97 ),
inference(avatar_component_clause,[],[f3100]) ).
fof(f3104,definition,
( spl32_98
<=> v2_orders_2(k2_yellow_2(sK8,sK8,sK9)) ),
introduced(definition,[new_symbols(definition,[spl32_98])],[avatar_definition]) ).
fof(f3105,plain,
( v2_orders_2(k2_yellow_2(sK8,sK8,sK9))
| ~ spl32_98 ),
inference(avatar_component_clause,[],[f3104]) ).
fof(f3106,plain,
( ~ v2_orders_2(k2_yellow_2(sK8,sK8,sK9))
| spl32_98 ),
inference(avatar_component_clause,[],[f3104]) ).
fof(f3110,plain,
( ~ v3_lattice3(k2_yellow_2(sK8,sK8,sK9))
| v1_lattice3(k2_yellow_2(sK8,sK8,sK9))
| spl32_5
| ~ spl32_90 ),
inference(forward_subsumption_resolution,[],[f3065,f2925]) ).
fof(f3147,plain,
( spl32_95
| ~ spl32_93
| spl32_5
| ~ spl32_90 ),
inference(avatar_split_clause,[],[f3110,f2860,f955,f3084,f3092]) ).
fof(f3149,plain,
( ~ sP3(sK9,sK8)
| spl32_93 ),
inference(resolution,[],[f3086,f634]) ).
fof(f3345,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,[],[f735,f920]) ).
fof(f3369,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))
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f3345,f956]) ).
fof(f3372,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))
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f3369,f427]) ).
fof(f3374,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))
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f3372,f426]) ).
fof(f3375,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))
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f3374,f425]) ).
fof(f3376,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))
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f3375,f420]) ).
fof(f3377,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))
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f3376,f431]) ).
fof(f3378,plain,
( ~ v7_waybel_1(sK9,sK8)
| v4_orders_2(k2_yellow_2(sK8,sK8,sK9))
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f3377,f430]) ).
fof(f3379,plain,
( v4_orders_2(k2_yellow_2(sK8,sK8,sK9))
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f3378,f429]) ).
fof(f3380,plain,
( spl32_96
| spl32_5 ),
inference(avatar_split_clause,[],[f3379,f955,f3096]) ).
fof(f3383,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,[],[f736,f920]) ).
fof(f3407,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))
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f3383,f956]) ).
fof(f3410,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))
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f3407,f427]) ).
fof(f3412,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))
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f3410,f426]) ).
fof(f3413,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))
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f3412,f425]) ).
fof(f3414,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))
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f3413,f420]) ).
fof(f3415,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))
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f3414,f431]) ).
fof(f3416,plain,
( ~ v7_waybel_1(sK9,sK8)
| v3_orders_2(k2_yellow_2(sK8,sK8,sK9))
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f3415,f430]) ).
fof(f3417,plain,
( v3_orders_2(k2_yellow_2(sK8,sK8,sK9))
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f3416,f429]) ).
fof(f3418,plain,
( spl32_97
| spl32_5 ),
inference(avatar_split_clause,[],[f3417,f955,f3100]) ).
fof(f3421,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,[],[f737,f920]) ).
fof(f3445,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))
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f3421,f956]) ).
fof(f3448,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))
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f3445,f427]) ).
fof(f3450,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))
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f3448,f426]) ).
fof(f3451,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))
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f3450,f425]) ).
fof(f3452,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))
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f3451,f420]) ).
fof(f3453,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))
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f3452,f431]) ).
fof(f3454,plain,
( ~ v7_waybel_1(sK9,sK8)
| v2_orders_2(k2_yellow_2(sK8,sK8,sK9))
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f3453,f430]) ).
fof(f3455,plain,
( v2_orders_2(k2_yellow_2(sK8,sK8,sK9))
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f3454,f429]) ).
fof(f3456,plain,
( $false
| spl32_5
| spl32_98 ),
inference(forward_subsumption_resolution,[],[f3455,f3106]) ).
fof(f3457,plain,
( spl32_5
| spl32_98 ),
inference(avatar_contradiction_clause,[],[f3456]) ).
fof(f3607,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,[],[f732,f920]) ).
fof(f3634,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)
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f3607,f956]) ).
fof(f3637,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)
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f3634,f427]) ).
fof(f3639,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)
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f3637,f426]) ).
fof(f3640,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)
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f3639,f425]) ).
fof(f3641,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)
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f3640,f420]) ).
fof(f3642,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)
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f3641,f431]) ).
fof(f3643,plain,
( ~ v7_waybel_1(sK9,sK8)
| v7_yellow_0(k2_yellow_2(sK8,sK8,sK9),sK8)
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f3642,f430]) ).
fof(f3644,plain,
( v7_yellow_0(k2_yellow_2(sK8,sK8,sK9),sK8)
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f3643,f429]) ).
fof(f3646,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)
| spl32_5 ),
inference(resolution,[],[f3644,f740]) ).
fof(f3647,plain,
( v5_yellow_0(k2_yellow_2(sK8,sK8,sK9),sK8)
| v3_struct_0(sK8)
| ~ l1_orders_2(sK8)
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f3646,f2989]) ).
fof(f3648,plain,
( v5_yellow_0(k2_yellow_2(sK8,sK8,sK9),sK8)
| ~ l1_orders_2(sK8)
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f3647,f956]) ).
fof(f3649,plain,
( v5_yellow_0(k2_yellow_2(sK8,sK8,sK9),sK8)
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f3648,f420]) ).
fof(f3684,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)
| spl32_5 ),
inference(resolution,[],[f3649,f743]) ).
fof(f3685,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)
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f3684,f2925]) ).
fof(f3686,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)
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f3685,f3053]) ).
fof(f3687,plain,
( v2_lattice3(k2_yellow_2(sK8,sK8,sK9))
| ~ v3_orders_2(sK8)
| ~ v4_orders_2(sK8)
| ~ v2_lattice3(sK8)
| ~ l1_orders_2(sK8)
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f3686,f2989]) ).
fof(f3688,plain,
( v2_lattice3(k2_yellow_2(sK8,sK8,sK9))
| ~ v4_orders_2(sK8)
| ~ v2_lattice3(sK8)
| ~ l1_orders_2(sK8)
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f3687,f426]) ).
fof(f3689,plain,
( v2_lattice3(k2_yellow_2(sK8,sK8,sK9))
| ~ v2_lattice3(sK8)
| ~ l1_orders_2(sK8)
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f3688,f425]) ).
fof(f3690,plain,
( v2_lattice3(k2_yellow_2(sK8,sK8,sK9))
| ~ l1_orders_2(sK8)
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f3689,f423]) ).
fof(f3691,plain,
( v2_lattice3(k2_yellow_2(sK8,sK8,sK9))
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f3690,f420]) ).
fof(f3692,plain,
( spl32_94
| spl32_5 ),
inference(avatar_split_clause,[],[f3691,f955,f3088]) ).
fof(f3775,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,[],[f648,f920]) ).
fof(f3802,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,[],[f3775,f427]) ).
fof(f3809,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,[],[f3802,f426]) ).
fof(f3813,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,[],[f3809,f425]) ).
fof(f3816,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,[],[f3813,f424]) ).
fof(f3819,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,[],[f3816,f423]) ).
fof(f3820,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,[],[f3819,f422]) ).
fof(f3821,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,[],[f3820,f420]) ).
fof(f3822,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,[],[f3821,f431]) ).
fof(f3823,plain,
( ~ v6_waybel_1(sK9,sK8)
| sP3(sK9,sK8) ),
inference(forward_subsumption_resolution,[],[f3822,f430]) ).
fof(f3824,plain,
( sP3(sK9,sK8)
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f3823,f2398]) ).
fof(f3825,plain,
( $false
| spl32_5
| spl32_93 ),
inference(forward_subsumption_resolution,[],[f3824,f3149]) ).
fof(f3826,plain,
( spl32_5
| spl32_93 ),
inference(avatar_contradiction_clause,[],[f3825]) ).
fof(f4577,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,[],[f434,f428]) ).
fof(f4585,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,[],[f4577,f431]) ).
fof(f4587,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,[],[f4585,f430]) ).
fof(f4589,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,[],[f4587,f429]) ).
fof(f4590,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,[],[f4589,f427]) ).
fof(f4591,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,[],[f4590,f426]) ).
fof(f4592,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,[],[f4591,f425]) ).
fof(f4593,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,[],[f4592,f424]) ).
fof(f4594,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,[],[f4593,f423]) ).
fof(f4595,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,[],[f4594,f422]) ).
fof(f4596,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,[],[f4595,f420]) ).
fof(f5125,definition,
( spl32_118
<=> 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,[spl32_118])],[avatar_definition]) ).
fof(f5127,plain,
( ~ v1_funct_2(k3_waybel_1(sK8,sK8,sK9),u1_struct_0(k2_yellow_2(sK8,sK8,sK9)),u1_struct_0(sK8))
| spl32_118 ),
inference(avatar_component_clause,[],[f5125]) ).
fof(f5147,definition,
( spl32_121
<=> v17_waybel_0(k3_waybel_1(sK8,sK8,sK9),k2_yellow_2(sK8,sK8,sK9),sK8) ),
introduced(definition,[new_symbols(definition,[spl32_121])],[avatar_definition]) ).
fof(f5149,plain,
( ~ v17_waybel_0(k3_waybel_1(sK8,sK8,sK9),k2_yellow_2(sK8,sK8,sK9),sK8)
| spl32_121 ),
inference(avatar_component_clause,[],[f5147]) ).
fof(f5231,definition,
( spl32_127
<=> 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,[spl32_127])],[avatar_definition]) ).
fof(f5232,plain,
( ~ m2_relset_1(k3_waybel_1(sK8,sK8,sK9),u1_struct_0(k2_yellow_2(sK8,sK8,sK9)),u1_struct_0(sK8))
| spl32_127 ),
inference(avatar_component_clause,[],[f5231]) ).
fof(f5260,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)
| ~ v3_waybel_3(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,[],[f472,f4596]) ).
fof(f5261,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)
| ~ v3_waybel_3(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,[],[f5260,f432]) ).
fof(f5262,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)
| ~ v3_waybel_3(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))
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f5261,f2787]) ).
fof(f5263,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)
| ~ v3_waybel_3(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))
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f5262,f427]) ).
fof(f5264,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)
| ~ v3_waybel_3(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))
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f5263,f426]) ).
fof(f5265,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)
| ~ v3_waybel_3(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))
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f5264,f425]) ).
fof(f5266,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)
| ~ v3_waybel_3(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))
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f5265,f424]) ).
fof(f5267,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)
| ~ v3_waybel_3(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))
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f5266,f423]) ).
fof(f5268,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_waybel_3(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))
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f5267,f422]) ).
fof(f5269,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))
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f5268,f421]) ).
fof(f5270,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))
| spl32_5 ),
inference(forward_subsumption_resolution,[],[f5269,f420]) ).
fof(f5271,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))
| spl32_5
| ~ spl32_98 ),
inference(forward_subsumption_resolution,[],[f5270,f3105]) ).
fof(f5272,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))
| spl32_5
| ~ spl32_97
| ~ spl32_98 ),
inference(forward_subsumption_resolution,[],[f5271,f3101]) ).
fof(f5273,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))
| spl32_5
| ~ spl32_96
| ~ spl32_97
| ~ spl32_98 ),
inference(forward_subsumption_resolution,[],[f5272,f3097]) ).
fof(f5274,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))
| spl32_5
| ~ spl32_95
| ~ spl32_96
| ~ spl32_97
| ~ spl32_98 ),
inference(forward_subsumption_resolution,[],[f5273,f3093]) ).
fof(f5275,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))
| spl32_5
| ~ spl32_94
| ~ spl32_95
| ~ spl32_96
| ~ spl32_97
| ~ spl32_98 ),
inference(forward_subsumption_resolution,[],[f5274,f3089]) ).
fof(f5276,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))
| spl32_5
| ~ spl32_93
| ~ spl32_94
| ~ spl32_95
| ~ spl32_96
| ~ spl32_97
| ~ spl32_98 ),
inference(forward_subsumption_resolution,[],[f5275,f3085]) ).
fof(f5277,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))
| spl32_5
| ~ spl32_90
| ~ spl32_93
| ~ spl32_94
| ~ spl32_95
| ~ spl32_96
| ~ spl32_97
| ~ spl32_98 ),
inference(forward_subsumption_resolution,[],[f5276,f2861]) ).
fof(f5279,definition,
( spl32_130
<=> v22_waybel_0(k3_waybel_1(sK8,sK8,sK9),k2_yellow_2(sK8,sK8,sK9),sK8) ),
introduced(definition,[new_symbols(definition,[spl32_130])],[avatar_definition]) ).
fof(f5281,plain,
( v22_waybel_0(k3_waybel_1(sK8,sK8,sK9),k2_yellow_2(sK8,sK8,sK9),sK8)
| ~ spl32_130 ),
inference(avatar_component_clause,[],[f5279]) ).
fof(f5282,plain,
( ~ spl32_127
| ~ spl32_121
| ~ spl32_118
| spl32_130
| spl32_5
| ~ spl32_90
| ~ spl32_93
| ~ spl32_94
| ~ spl32_95
| ~ spl32_96
| ~ spl32_97
| ~ spl32_98 ),
inference(avatar_split_clause,[],[f5277,f3104,f3100,f3096,f3092,f3088,f3084,f2860,f955,f5279,f5125,f5147,f5231]) ).
fof(f5283,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))
| spl32_118 ),
inference(resolution,[],[f5127,f558]) ).
fof(f5284,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))
| spl32_118 ),
inference(duplicate_literal_removal,[],[f5283]) ).
fof(f5285,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))
| spl32_5
| spl32_118 ),
inference(forward_subsumption_resolution,[],[f5284,f956]) ).
fof(f5286,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))
| spl32_5
| spl32_118 ),
inference(forward_subsumption_resolution,[],[f5285,f420]) ).
fof(f5287,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))
| spl32_5
| spl32_118 ),
inference(forward_subsumption_resolution,[],[f5286,f431]) ).
fof(f5288,plain,
( ~ m1_relset_1(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| spl32_5
| spl32_118 ),
inference(forward_subsumption_resolution,[],[f5287,f430]) ).
fof(f5289,plain,
( $false
| spl32_5
| spl32_118 ),
inference(forward_subsumption_resolution,[],[f5288,f920]) ).
fof(f5290,plain,
( spl32_5
| spl32_118 ),
inference(avatar_contradiction_clause,[],[f5289]) ).
fof(f5291,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)
| spl32_121 ),
inference(resolution,[],[f5149,f436]) ).
fof(f5292,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)
| spl32_121 ),
inference(forward_subsumption_resolution,[],[f5291,f431]) ).
fof(f5293,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)
| spl32_121 ),
inference(forward_subsumption_resolution,[],[f5292,f430]) ).
fof(f5294,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)
| spl32_121 ),
inference(forward_subsumption_resolution,[],[f5293,f429]) ).
fof(f5295,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)
| spl32_121 ),
inference(forward_subsumption_resolution,[],[f5294,f428]) ).
fof(f5296,plain,
( ~ v3_orders_2(sK8)
| ~ v4_orders_2(sK8)
| ~ v1_lattice3(sK8)
| ~ v2_lattice3(sK8)
| ~ v3_lattice3(sK8)
| ~ l1_orders_2(sK8)
| spl32_121 ),
inference(forward_subsumption_resolution,[],[f5295,f427]) ).
fof(f5297,plain,
( ~ v4_orders_2(sK8)
| ~ v1_lattice3(sK8)
| ~ v2_lattice3(sK8)
| ~ v3_lattice3(sK8)
| ~ l1_orders_2(sK8)
| spl32_121 ),
inference(forward_subsumption_resolution,[],[f5296,f426]) ).
fof(f5298,plain,
( ~ v1_lattice3(sK8)
| ~ v2_lattice3(sK8)
| ~ v3_lattice3(sK8)
| ~ l1_orders_2(sK8)
| spl32_121 ),
inference(forward_subsumption_resolution,[],[f5297,f425]) ).
fof(f5299,plain,
( ~ v2_lattice3(sK8)
| ~ v3_lattice3(sK8)
| ~ l1_orders_2(sK8)
| spl32_121 ),
inference(forward_subsumption_resolution,[],[f5298,f424]) ).
fof(f5300,plain,
( ~ v3_lattice3(sK8)
| ~ l1_orders_2(sK8)
| spl32_121 ),
inference(forward_subsumption_resolution,[],[f5299,f423]) ).
fof(f5301,plain,
( ~ l1_orders_2(sK8)
| spl32_121 ),
inference(forward_subsumption_resolution,[],[f5300,f422]) ).
fof(f5302,plain,
( $false
| spl32_121 ),
inference(forward_subsumption_resolution,[],[f5301,f420]) ).
fof(f5303,plain,
spl32_121,
inference(avatar_contradiction_clause,[],[f5302]) ).
fof(f5304,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))
| spl32_127 ),
inference(resolution,[],[f5232,f557]) ).
fof(f5305,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))
| spl32_127 ),
inference(duplicate_literal_removal,[],[f5304]) ).
fof(f5306,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))
| spl32_5
| spl32_127 ),
inference(forward_subsumption_resolution,[],[f5305,f956]) ).
fof(f5307,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))
| spl32_5
| spl32_127 ),
inference(forward_subsumption_resolution,[],[f5306,f420]) ).
fof(f5308,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))
| spl32_5
| spl32_127 ),
inference(forward_subsumption_resolution,[],[f5307,f431]) ).
fof(f5309,plain,
( ~ m1_relset_1(sK9,u1_struct_0(sK8),u1_struct_0(sK8))
| spl32_5
| spl32_127 ),
inference(forward_subsumption_resolution,[],[f5308,f430]) ).
fof(f5310,plain,
( $false
| spl32_5
| spl32_127 ),
inference(forward_subsumption_resolution,[],[f5309,f920]) ).
fof(f5311,plain,
( spl32_5
| spl32_127 ),
inference(avatar_contradiction_clause,[],[f5310]) ).
fof(f5324,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)
| ~ spl32_130 ),
inference(resolution,[],[f5281,f516]) ).
fof(f5325,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)
| ~ spl32_130 ),
inference(forward_subsumption_resolution,[],[f5324,f433]) ).
fof(f5326,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)
| ~ spl32_130 ),
inference(forward_subsumption_resolution,[],[f5325,f431]) ).
fof(f5327,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)
| ~ spl32_130 ),
inference(forward_subsumption_resolution,[],[f5326,f430]) ).
fof(f5328,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)
| ~ spl32_130 ),
inference(forward_subsumption_resolution,[],[f5327,f429]) ).
fof(f5329,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)
| ~ spl32_130 ),
inference(forward_subsumption_resolution,[],[f5328,f428]) ).
fof(f5330,plain,
( ~ v3_orders_2(sK8)
| ~ v4_orders_2(sK8)
| ~ v1_lattice3(sK8)
| ~ v2_lattice3(sK8)
| ~ v3_lattice3(sK8)
| ~ l1_orders_2(sK8)
| ~ spl32_130 ),
inference(forward_subsumption_resolution,[],[f5329,f427]) ).
fof(f5331,plain,
( ~ v4_orders_2(sK8)
| ~ v1_lattice3(sK8)
| ~ v2_lattice3(sK8)
| ~ v3_lattice3(sK8)
| ~ l1_orders_2(sK8)
| ~ spl32_130 ),
inference(forward_subsumption_resolution,[],[f5330,f426]) ).
fof(f5332,plain,
( ~ v1_lattice3(sK8)
| ~ v2_lattice3(sK8)
| ~ v3_lattice3(sK8)
| ~ l1_orders_2(sK8)
| ~ spl32_130 ),
inference(forward_subsumption_resolution,[],[f5331,f425]) ).
fof(f5333,plain,
( ~ v2_lattice3(sK8)
| ~ v3_lattice3(sK8)
| ~ l1_orders_2(sK8)
| ~ spl32_130 ),
inference(forward_subsumption_resolution,[],[f5332,f424]) ).
fof(f5334,plain,
( ~ v3_lattice3(sK8)
| ~ l1_orders_2(sK8)
| ~ spl32_130 ),
inference(forward_subsumption_resolution,[],[f5333,f423]) ).
fof(f5335,plain,
( ~ l1_orders_2(sK8)
| ~ spl32_130 ),
inference(forward_subsumption_resolution,[],[f5334,f422]) ).
fof(f5336,plain,
( $false
| ~ spl32_130 ),
inference(forward_subsumption_resolution,[],[f5335,f420]) ).
fof(f5337,plain,
~ spl32_130,
inference(avatar_contradiction_clause,[],[f5336]) ).
cnf(s10,plain,
~ spl32_5,
inference(sat_conversion,[],[f1056]) ).
cnf(s64,plain,
( spl32_5
| spl32_90 ),
inference(sat_conversion,[],[f3063]) ).
cnf(s73,plain,
( spl32_5
| ~ spl32_90
| ~ spl32_93
| spl32_95 ),
inference(sat_conversion,[],[f3147]) ).
cnf(s81,plain,
( spl32_5
| spl32_96 ),
inference(sat_conversion,[],[f3380]) ).
cnf(s82,plain,
( spl32_5
| spl32_97 ),
inference(sat_conversion,[],[f3418]) ).
cnf(s83,plain,
( spl32_5
| spl32_98 ),
inference(sat_conversion,[],[f3457]) ).
cnf(s84,plain,
( spl32_5
| spl32_94 ),
inference(sat_conversion,[],[f3692]) ).
cnf(s86,plain,
( spl32_5
| spl32_93 ),
inference(sat_conversion,[],[f3826]) ).
cnf(s103,plain,
( spl32_5
| ~ spl32_90
| ~ spl32_93
| ~ spl32_94
| ~ spl32_95
| ~ spl32_96
| ~ spl32_97
| ~ spl32_98
| ~ spl32_118
| ~ spl32_121
| ~ spl32_127
| spl32_130 ),
inference(sat_conversion,[],[f5282]) ).
cnf(s104,plain,
( spl32_5
| spl32_118 ),
inference(sat_conversion,[],[f5290]) ).
cnf(s105,plain,
spl32_121,
inference(sat_conversion,[],[f5303]) ).
cnf(s106,plain,
( spl32_5
| spl32_127 ),
inference(sat_conversion,[],[f5311]) ).
cnf(s107,plain,
~ spl32_130,
inference(sat_conversion,[],[f5337]) ).
cnf(s108,plain,
( spl32_5
| ~ spl32_90
| ~ spl32_93
| ~ spl32_94
| ~ spl32_95
| ~ spl32_96
| ~ spl32_97
| ~ spl32_98
| ~ spl32_118
| ~ spl32_127 ),
inference(rat,[],[s103,s107,s105]) ).
cnf(s116,plain,
spl32_127,
inference(rat,[],[s106,s10]) ).
cnf(s117,plain,
spl32_118,
inference(rat,[],[s104,s10]) ).
cnf(s120,plain,
spl32_93,
inference(rat,[],[s86,s10]) ).
cnf(s121,plain,
spl32_94,
inference(rat,[],[s84,s10]) ).
cnf(s122,plain,
spl32_98,
inference(rat,[],[s83,s10]) ).
cnf(s123,plain,
spl32_97,
inference(rat,[],[s82,s10]) ).
cnf(s124,plain,
spl32_96,
inference(rat,[],[s81,s10]) ).
cnf(s126,plain,
spl32_90,
inference(rat,[],[s64,s10]) ).
cnf(s128,plain,
~ spl32_95,
inference(rat,[],[s108,s116,s117,s122,s123,s124,s120,s121,s10,s126]) ).
cnf(s129,plain,
$false,
inference(rat,[],[s73,s10,s120,s128,s126]) ).
fof(f5338,plain,
$false,
inference(avatar_sat_refutation,[],[s129]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT370+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.36 % Computer : n003.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sun Sep 27 15:07:56 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.39 Running first-order theorem proving
% 0.09/0.39 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
% 4.13/1.58 % (659982)Detected formulas, will run a generic FOF schedule.
% 4.13/1.58 % (659991)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3365588892:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 4.13/1.58 % (659991)Instruction limit reached!
% 4.13/1.58 % (659991)------------------------------
% 4.13/1.58 % (659991)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.13/1.58 % (659991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.13/1.58 % (659991)CaDiCaL version: 2.1.3
% 4.13/1.58 % (659991)Termination reason: Instruction limit
% 4.13/1.58 % (659991)Termination phase: Saturation
% 4.13/1.58 % (659991)Time elapsed: 0.037 s
% 4.13/1.58 % (659991)Peak memory usage: 89 MB
% 4.13/1.58 % (659991)Instructions burned: 120 (million)
% 4.13/1.58 % (659993)dis-21_1_sil=8000:lcm=predicate:random_seed=1076994524: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)
% 4.13/1.58 % (659987)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=325438078:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 4.13/1.58 % (659989)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=609434736:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 4.13/1.58 % (659988)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=2194738232:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 4.13/1.58 % (659990)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=476904629:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 4.13/1.58 % (659992)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3830861493:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 4.13/1.58 % (659990)Refutation not found, incomplete strategy
% 4.13/1.58 % (659990)------------------------------
% 4.13/1.58 % (659990)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.13/1.58 % (659990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.13/1.58 % (659990)CaDiCaL version: 2.1.3
% 4.13/1.58 % (659990)Termination reason: Refutation not found, incomplete strategy
% 4.13/1.58 % (659990)Time elapsed: 0.004 s
% 4.13/1.58 % (659990)Peak memory usage: 88 MB
% 4.13/1.58 % (659990)Instructions burned: 5 (million)
% 4.13/1.58 % (659992)Instruction limit reached!
% 4.13/1.58 % (659992)------------------------------
% 4.13/1.58 % (659992)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.13/1.58 % (659992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.13/1.58 % (659992)CaDiCaL version: 2.1.3
% 4.13/1.58 % (659992)Termination reason: Instruction limit
% 4.13/1.58 % (659992)Termination phase: Saturation
% 4.13/1.58 % (659992)Time elapsed: 0.046 s
% 4.13/1.58 % (659992)Peak memory usage: 90 MB
% 4.13/1.58 % (659992)Instructions burned: 142 (million)
% 4.13/1.58 % (659993)Instruction limit reached!
% 4.13/1.58 % (659993)------------------------------
% 4.13/1.58 % (659993)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.13/1.58 % (659993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.13/1.58 % (659993)CaDiCaL version: 2.1.3
% 4.13/1.58 % (659993)Termination reason: Instruction limit
% 4.13/1.58 % (659993)Termination phase: Saturation
% 4.13/1.58 % (659993)Time elapsed: 0.068 s
% 4.13/1.58 % (659993)Peak memory usage: 91 MB
% 4.13/1.58 % (659993)Instructions burned: 130 (million)
% 4.13/1.58 % (660000)lrs+10_1_sil=8000:sp=occurrence:random_seed=2834779397:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 4.13/1.58 % (660002)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3476031819:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 4.13/1.58 % (660002)Refutation not found, incomplete strategy
% 4.13/1.58 % (660002)------------------------------
% 4.13/1.58 % (660002)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.13/1.58 % (660002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.13/1.58 % (660002)CaDiCaL version: 2.1.3
% 4.13/1.58 % (660002)Termination reason: Refutation not found, incomplete strategy
% 4.13/1.58 % (660002)Time elapsed: 0.014 s
% 4.13/1.58 % (660002)Peak memory usage: 89 MB
% 4.13/1.58 % (660002)Instructions burned: 46 (million)
% 4.13/1.58 % (660003)lrs+1011_1_sil=32000:sp=occurrence:random_seed=454832179:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 4.13/1.58 % (659990)------------------------------
% 4.13/1.58 % (659990)------------------------------
% 4.13/1.58 % (660000)First to succeed.
% 4.13/1.58 % (660000)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-659982"
% 4.13/1.58 % (660002)------------------------------
% 4.13/1.58 % (660002)------------------------------
% 4.13/1.58 % (660003)Instruction limit reached!
% 4.13/1.58 % (660003)------------------------------
% 4.13/1.58 % (660003)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.13/1.58 % (660003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.13/1.58 % (660003)CaDiCaL version: 2.1.3
% 4.13/1.58 % (660003)Termination reason: Instruction limit
% 4.13/1.58 % (660003)Termination phase: Saturation
% 4.13/1.58 % (660003)Time elapsed: 0.171 s
% 4.13/1.58 % (660003)Peak memory usage: 95 MB
% 4.13/1.58 % (660003)Instructions burned: 327 (million)
% 4.13/1.58 % (660007)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=3139257025:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 4.13/1.58 % (660008)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=4207071226:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 4.13/1.58 % (660008)Refutation not found, incomplete strategy
% 4.13/1.58 % (660008)------------------------------
% 4.13/1.58 % (660008)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.13/1.58 % (660008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.13/1.58 % (660008)CaDiCaL version: 2.1.3
% 4.13/1.58 % (660008)Termination reason: Refutation not found, incomplete strategy
% 4.13/1.58 % (660008)Time elapsed: 0.005 s
% 4.13/1.58 % (660008)Peak memory usage: 89 MB
% 4.13/1.58 % (660008)Instructions burned: 16 (million)
% 4.13/1.58 % (660007)Instruction limit reached!
% 4.13/1.58 % (660007)------------------------------
% 4.13/1.58 % (660007)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.13/1.58 % (660007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.13/1.58 % (660009)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3994600479:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 4.13/1.58 % (660007)CaDiCaL version: 2.1.3
% 4.13/1.58 % (660007)Termination reason: Instruction limit
% 4.13/1.58 % (660007)Termination phase: Saturation
% 4.13/1.58 % (660007)Time elapsed: 0.128 s
% 4.13/1.58 % (660007)Peak memory usage: 90 MB
% 4.13/1.58 % (660007)Instructions burned: 248 (million)
% 4.13/1.58 % (660000)Refutation found. Thanks to Tanya!
% 4.13/1.58 % SZS status Theorem for theBenchmark
% 4.13/1.58 % SZS output start Proof for theBenchmark
% See solution above
% 0.14/1.80 % (660000)------------------------------
% 0.14/1.80 % (660000)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.14/1.80 % (660000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.14/1.80 % (660000)CaDiCaL version: 2.1.3
% 0.14/1.80 % (660000)Termination reason: Refutation
% 0.14/1.80 % (660000)Time elapsed: 0.142 s
% 0.14/1.80 % (660000)Peak memory usage: 92 MB
% 0.14/1.80 % (660000)Instructions burned: 272 (million)
% 0.14/1.80 % (660000)------------------------------
% 0.14/1.80 % (660000)------------------------------
% 0.14/1.80 % (659982)Success in time 0.743 s
% 0.14/1.80 % Vampire exiting
%------------------------------------------------------------------------------