%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT370+3 : 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 : n014.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 17.39s 8.47s
% Output : Refutation 47.69s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 62
% Syntax : Number of formulae : 477 ( 84 unt; 45 def)
% Number of atoms : 3318 ( 69 equ)
% Maximal formula atoms : 25 ( 6 avg)
% Number of connectives : 5172 (2331 ~;2462 |; 298 &)
% ( 45 <=>; 36 =>; 0 <=; 0 <~>)
% Maximal formula depth : 28 ( 8 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 77 ( 75 usr; 42 prp; 0-3 aty)
% Number of functors : 12 ( 12 usr; 5 con; 0-3 aty)
% Number of variables : 317 ( 0 sgn 313 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1394,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(f11560,axiom,
! [X0] :
( l1_orders_2(X0)
=> ( v1_lattice3(X0)
=> ~ v3_struct_0(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc1_lattice3) ).
fof(f14866,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(f15134,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(f15204,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(f15225,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(f15232,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_relat_1(k3_waybel_1(X0,X1,X2))
& v1_funct_1(k3_waybel_1(X0,X1,X2))
& v2_funct_1(k3_waybel_1(X0,X1,X2))
& ~ v1_xboole_0(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))
& v1_partfun1(k3_waybel_1(X0,X1,X2),u1_struct_0(k2_yellow_2(X0,X1,X2)),u1_struct_0(X1))
& v5_orders_3(k3_waybel_1(X0,X1,X2),k2_yellow_2(X0,X1,X2),X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc7_waybel_1) ).
fof(f15290,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& l1_orders_2(X1) )
=> ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> k2_waybel_1(X0,X1,X2) = X2 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t32_waybel_1) ).
fof(f15292,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& l1_orders_2(X1) )
=> ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> k3_waybel_1(X0,X1,X2) = k7_grcat_1(k2_yellow_2(X0,X1,X2)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d17_waybel_1) ).
fof(f15305,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(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))
& m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
=> ( v6_waybel_1(X1,X0)
=> v3_lattice3(k2_yellow_2(X0,X0,X1)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t57_waybel_1) ).
fof(f15347,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(f16465,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_orders_2(X0) )
=> ( ~ v1_xboole_0(k7_grcat_1(X0))
& v1_relat_1(k7_grcat_1(X0))
& v1_funct_1(k7_grcat_1(X0))
& v1_funct_2(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))
& v5_orders_3(k7_grcat_1(X0),X0,X0)
& v1_partfun1(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_waybel_9) ).
fof(f18949,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(f18959,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(f18966,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(f18967,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(f18970,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(f18971,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)],[f18970]) ).
fof(f19090,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,[],[f18949]) ).
fof(f19091,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,[],[f19090]) ).
fof(f19109,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,[],[f18959]) ).
fof(f19110,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,[],[f19109]) ).
fof(f19123,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,[],[f18966]) ).
fof(f19124,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,[],[f19123]) ).
fof(f19125,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,[],[f18967]) ).
fof(f19126,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,[],[f19125]) ).
fof(f19131,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,[],[f18971]) ).
fof(f19132,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,[],[f19131]) ).
fof(f19135,plain,
! [X0] :
( ~ v3_struct_0(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f11560]) ).
fof(f19136,plain,
! [X0] :
( ~ v3_struct_0(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f19135]) ).
fof(f19557,plain,
! [X0] :
( ( ~ v1_xboole_0(k7_grcat_1(X0))
& v1_relat_1(k7_grcat_1(X0))
& v1_funct_1(k7_grcat_1(X0))
& v1_funct_2(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))
& v5_orders_3(k7_grcat_1(X0),X0,X0)
& v1_partfun1(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f16465]) ).
fof(f19558,plain,
! [X0] :
( ( ~ v1_xboole_0(k7_grcat_1(X0))
& v1_relat_1(k7_grcat_1(X0))
& v1_funct_1(k7_grcat_1(X0))
& v1_funct_2(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))
& v5_orders_3(k7_grcat_1(X0),X0,X0)
& v1_partfun1(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f19557]) ).
fof(f20027,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,[],[f15204]) ).
fof(f20028,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,[],[f20027]) ).
fof(f20029,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,[],[f15134]) ).
fof(f20030,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,[],[f20029]) ).
fof(f20168,plain,
! [X0] :
( ! [X1] :
( v3_lattice3(k2_yellow_2(X0,X0,X1))
| ~ v6_waybel_1(X1,X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ m2_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)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f15305]) ).
fof(f20169,plain,
! [X0] :
( ! [X1] :
( v3_lattice3(k2_yellow_2(X0,X0,X1))
| ~ v6_waybel_1(X1,X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ m2_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)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f20168]) ).
fof(f20178,plain,
! [X0] :
( ! [X1] :
( ( 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) )
| ~ 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,[],[f15225]) ).
fof(f20179,plain,
! [X0] :
( ! [X1] :
( ( 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) )
| ~ 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,[],[f20178]) ).
fof(f20214,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( k2_waybel_1(X0,X1,X2) = X2
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ l1_orders_2(X1) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f15290]) ).
fof(f20215,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( k2_waybel_1(X0,X1,X2) = X2
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ l1_orders_2(X1) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f20214]) ).
fof(f20222,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,[],[f15347]) ).
fof(f20223,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,[],[f20222]) ).
fof(f20232,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( k3_waybel_1(X0,X1,X2) = k7_grcat_1(k2_yellow_2(X0,X1,X2))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ l1_orders_2(X1) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f15292]) ).
fof(f20233,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( k3_waybel_1(X0,X1,X2) = k7_grcat_1(k2_yellow_2(X0,X1,X2))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ l1_orders_2(X1) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f20232]) ).
fof(f20234,plain,
! [X0,X1,X2] :
( ( v1_relat_1(k3_waybel_1(X0,X1,X2))
& v1_funct_1(k3_waybel_1(X0,X1,X2))
& v2_funct_1(k3_waybel_1(X0,X1,X2))
& ~ v1_xboole_0(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))
& v1_partfun1(k3_waybel_1(X0,X1,X2),u1_struct_0(k2_yellow_2(X0,X1,X2)),u1_struct_0(X1))
& v5_orders_3(k3_waybel_1(X0,X1,X2),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,[],[f15232]) ).
fof(f20235,plain,
! [X0,X1,X2] :
( ( v1_relat_1(k3_waybel_1(X0,X1,X2))
& v1_funct_1(k3_waybel_1(X0,X1,X2))
& v2_funct_1(k3_waybel_1(X0,X1,X2))
& ~ v1_xboole_0(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))
& v1_partfun1(k3_waybel_1(X0,X1,X2),u1_struct_0(k2_yellow_2(X0,X1,X2)),u1_struct_0(X1))
& v5_orders_3(k3_waybel_1(X0,X1,X2),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,[],[f20234]) ).
fof(f20239,plain,
! [X0] :
( ! [X1] :
( l1_orders_2(X1)
| ~ m1_yellow_0(X1,X0) )
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f14866]) ).
fof(f20323,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)) )
| ~ sP19(X1,X0) ),
introduced(definition,[new_symbols(definition,[sP19])],[predicate_definition_introduction]) ).
fof(f20324,plain,
! [X0,X1] :
( sP19(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,[],[f19110,f20323]) ).
fof(f20501,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)) )
| ~ sP19(X1,X0) ),
inference(nnf_transformation,[],[f20323]) ).
fof(f20502,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)) )
| ~ sP19(X0,X1) ),
inference(rectify,[],[f20501]) ).
fof(f20513,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,[],[f19126]) ).
fof(f20518,plain,
( ~ v4_waybel_0(k2_yellow_2(sK111,sK111,sK112),sK111)
& v1_waybel34(k2_waybel_1(sK111,sK111,sK112),sK111,k2_yellow_2(sK111,sK111,sK112))
& v1_funct_1(sK112)
& v1_funct_2(sK112,u1_struct_0(sK111),u1_struct_0(sK111))
& v7_waybel_1(sK112,sK111)
& m2_relset_1(sK112,u1_struct_0(sK111),u1_struct_0(sK111))
& v2_orders_2(sK111)
& v3_orders_2(sK111)
& v4_orders_2(sK111)
& v1_lattice3(sK111)
& v2_lattice3(sK111)
& v3_lattice3(sK111)
& v3_waybel_3(sK111)
& l1_orders_2(sK111) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK111,sK112]),skolemize(X0,sK111),skolemize(X1,sK112)],[f19132]) ).
fof(f20522,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,[],[f1394]) ).
fof(f21211,plain,
! [X2,X0,X1] :
( ~ v3_waybel_3(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)
| v22_waybel_0(X2,X0,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,[],[f19091]) ).
fof(f21244,plain,
! [X0,X1] :
( ~ sP19(X0,X1)
| v2_lattice3(k2_yellow_2(X1,X1,X0)) ),
inference(cnf_transformation,[],[f20502]) ).
fof(f21245,plain,
! [X0,X1] :
( v1_lattice3(k2_yellow_2(X1,X1,X0))
| ~ sP19(X0,X1) ),
inference(cnf_transformation,[],[f20502]) ).
fof(f21252,plain,
! [X0,X1] :
( ~ sP19(X0,X1)
| v4_orders_2(k2_yellow_2(X1,X1,X0)) ),
inference(cnf_transformation,[],[f20502]) ).
fof(f21253,plain,
! [X0,X1] :
( v3_orders_2(k2_yellow_2(X1,X1,X0))
| ~ sP19(X0,X1) ),
inference(cnf_transformation,[],[f20502]) ).
fof(f21254,plain,
! [X0,X1] :
( v2_orders_2(k2_yellow_2(X1,X1,X0))
| ~ sP19(X0,X1) ),
inference(cnf_transformation,[],[f20502]) ).
fof(f21257,plain,
! [X0,X1] :
( sP19(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(cnf_transformation,[],[f20324]) ).
fof(f21288,plain,
! [X0,X1] :
( ~ v3_lattice3(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)
| k2_waybel_1(X0,X0,X1) = k1_waybel34(k2_yellow_2(X0,X0,X1),X0,k3_waybel_1(X0,X0,X1))
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f19124]) ).
fof(f21290,plain,
! [X0,X1] :
( ~ v3_lattice3(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)
| v17_waybel_0(k3_waybel_1(X0,X0,X1),k2_yellow_2(X0,X0,X1),X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f19124]) ).
fof(f21293,plain,
! [X0,X1] :
( ~ v3_lattice3(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)
| v4_waybel_0(k2_yellow_2(X0,X0,X1),X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f20513]) ).
fof(f21308,plain,
l1_orders_2(sK111),
inference(cnf_transformation,[],[f20518]) ).
fof(f21309,plain,
v3_waybel_3(sK111),
inference(cnf_transformation,[],[f20518]) ).
fof(f21310,plain,
v3_lattice3(sK111),
inference(cnf_transformation,[],[f20518]) ).
fof(f21311,plain,
v2_lattice3(sK111),
inference(cnf_transformation,[],[f20518]) ).
fof(f21312,plain,
v1_lattice3(sK111),
inference(cnf_transformation,[],[f20518]) ).
fof(f21313,plain,
v4_orders_2(sK111),
inference(cnf_transformation,[],[f20518]) ).
fof(f21314,plain,
v3_orders_2(sK111),
inference(cnf_transformation,[],[f20518]) ).
fof(f21315,plain,
v2_orders_2(sK111),
inference(cnf_transformation,[],[f20518]) ).
fof(f21316,plain,
m2_relset_1(sK112,u1_struct_0(sK111),u1_struct_0(sK111)),
inference(cnf_transformation,[],[f20518]) ).
fof(f21317,plain,
v7_waybel_1(sK112,sK111),
inference(cnf_transformation,[],[f20518]) ).
fof(f21318,plain,
v1_funct_2(sK112,u1_struct_0(sK111),u1_struct_0(sK111)),
inference(cnf_transformation,[],[f20518]) ).
fof(f21319,plain,
v1_funct_1(sK112),
inference(cnf_transformation,[],[f20518]) ).
fof(f21320,plain,
v1_waybel34(k2_waybel_1(sK111,sK111,sK112),sK111,k2_yellow_2(sK111,sK111,sK112)),
inference(cnf_transformation,[],[f20518]) ).
fof(f21321,plain,
~ v4_waybel_0(k2_yellow_2(sK111,sK111,sK112),sK111),
inference(cnf_transformation,[],[f20518]) ).
fof(f21333,plain,
! [X2,X0,X1] :
( m1_relset_1(X2,X0,X1)
| ~ m2_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f20522]) ).
fof(f21334,plain,
! [X2,X0,X1] :
( m2_relset_1(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f20522]) ).
fof(f21340,plain,
! [X0] :
( ~ v1_lattice3(X0)
| ~ v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f19136]) ).
fof(f22000,plain,
! [X0] :
( v1_funct_1(k7_grcat_1(X0))
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f19558]) ).
fof(f22836,plain,
! [X2,X0,X1] :
( v3_struct_0(X0)
| m1_yellow_0(k2_yellow_2(X0,X1,X2),X1)
| ~ 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,[],[f20028]) ).
fof(f22841,plain,
! [X2,X0,X1] :
( v3_struct_0(X0)
| ~ v3_struct_0(k2_yellow_2(X0,X1,X2))
| ~ 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,[],[f20030]) ).
fof(f23028,plain,
! [X0,X1] :
( ~ v3_lattice3(X0)
| ~ v6_waybel_1(X1,X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ m2_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)
| v3_lattice3(k2_yellow_2(X0,X0,X1))
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f20169]) ).
fof(f23068,plain,
! [X0,X1] :
( 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(cnf_transformation,[],[f20179]) ).
fof(f23158,plain,
! [X2,X0,X1] :
( v3_struct_0(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| k2_waybel_1(X0,X1,X2) = X2
| ~ l1_orders_2(X1)
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f20215]) ).
fof(f23167,plain,
! [X2,X0,X1] :
( v3_struct_0(X0)
| m2_relset_1(k3_waybel_1(X0,X1,X2),u1_struct_0(k2_yellow_2(X0,X1,X2)),u1_struct_0(X1))
| ~ 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,[],[f20223]) ).
fof(f23174,plain,
! [X2,X0,X1] :
( v3_struct_0(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| k3_waybel_1(X0,X1,X2) = k7_grcat_1(k2_yellow_2(X0,X1,X2))
| ~ l1_orders_2(X1)
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f20233]) ).
fof(f23177,plain,
! [X2,X0,X1] :
( v3_struct_0(X0)
| v1_funct_2(k3_waybel_1(X0,X1,X2),u1_struct_0(k2_yellow_2(X0,X1,X2)),u1_struct_0(X1))
| ~ 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,[],[f20235]) ).
fof(f23185,plain,
! [X0,X1] :
( ~ m1_yellow_0(X1,X0)
| l1_orders_2(X1)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f20239]) ).
fof(f23373,definition,
sF325 = k2_yellow_2(sK111,sK111,sK112),
introduced(definition,[new_symbols(definition,[sF325])],[function_definition]) ).
fof(f23374,plain,
k2_yellow_2(sK111,sK111,sK112) = sF325,
inference(reorient_equations,[],[f23373]) ).
fof(f23375,plain,
~ v4_waybel_0(sF325,sK111),
inference(definition_folding,[],[f21321,f23374]) ).
fof(f23376,definition,
sF326 = k2_waybel_1(sK111,sK111,sK112),
introduced(definition,[new_symbols(definition,[sF326])],[function_definition]) ).
fof(f23377,plain,
k2_waybel_1(sK111,sK111,sK112) = sF326,
inference(reorient_equations,[],[f23376]) ).
fof(f23378,plain,
v1_waybel34(sF326,sK111,sF325),
inference(definition_folding,[],[f21320,f23374,f23377]) ).
fof(f23379,definition,
sF327 = u1_struct_0(sK111),
introduced(definition,[new_symbols(definition,[sF327])],[function_definition]) ).
fof(f23380,plain,
u1_struct_0(sK111) = sF327,
inference(reorient_equations,[],[f23379]) ).
fof(f23381,plain,
v1_funct_2(sK112,sF327,sF327),
inference(definition_folding,[],[f21318,f23380,f23380]) ).
fof(f23382,plain,
m2_relset_1(sK112,sF327,sF327),
inference(definition_folding,[],[f21316,f23380,f23380]) ).
fof(f24100,definition,
( spl328_137
<=> l1_orders_2(sK111) ),
introduced(definition,[new_symbols(definition,[spl328_137])],[avatar_definition]) ).
fof(f24102,plain,
( l1_orders_2(sK111)
| ~ spl328_137 ),
inference(avatar_component_clause,[],[f24100]) ).
fof(f24103,plain,
spl328_137,
inference(avatar_split_clause,[],[f21308,f24100]) ).
fof(f24105,definition,
( spl328_138
<=> v3_waybel_3(sK111) ),
introduced(definition,[new_symbols(definition,[spl328_138])],[avatar_definition]) ).
fof(f24107,plain,
( v3_waybel_3(sK111)
| ~ spl328_138 ),
inference(avatar_component_clause,[],[f24105]) ).
fof(f24108,plain,
spl328_138,
inference(avatar_split_clause,[],[f21309,f24105]) ).
fof(f24110,definition,
( spl328_139
<=> v3_lattice3(sK111) ),
introduced(definition,[new_symbols(definition,[spl328_139])],[avatar_definition]) ).
fof(f24112,plain,
( v3_lattice3(sK111)
| ~ spl328_139 ),
inference(avatar_component_clause,[],[f24110]) ).
fof(f24113,plain,
spl328_139,
inference(avatar_split_clause,[],[f21310,f24110]) ).
fof(f24115,definition,
( spl328_140
<=> v2_lattice3(sK111) ),
introduced(definition,[new_symbols(definition,[spl328_140])],[avatar_definition]) ).
fof(f24117,plain,
( v2_lattice3(sK111)
| ~ spl328_140 ),
inference(avatar_component_clause,[],[f24115]) ).
fof(f24118,plain,
spl328_140,
inference(avatar_split_clause,[],[f21311,f24115]) ).
fof(f24120,definition,
( spl328_141
<=> v1_lattice3(sK111) ),
introduced(definition,[new_symbols(definition,[spl328_141])],[avatar_definition]) ).
fof(f24122,plain,
( v1_lattice3(sK111)
| ~ spl328_141 ),
inference(avatar_component_clause,[],[f24120]) ).
fof(f24123,plain,
spl328_141,
inference(avatar_split_clause,[],[f21312,f24120]) ).
fof(f24125,definition,
( spl328_142
<=> v4_orders_2(sK111) ),
introduced(definition,[new_symbols(definition,[spl328_142])],[avatar_definition]) ).
fof(f24127,plain,
( v4_orders_2(sK111)
| ~ spl328_142 ),
inference(avatar_component_clause,[],[f24125]) ).
fof(f24128,plain,
spl328_142,
inference(avatar_split_clause,[],[f21313,f24125]) ).
fof(f24130,definition,
( spl328_143
<=> v3_orders_2(sK111) ),
introduced(definition,[new_symbols(definition,[spl328_143])],[avatar_definition]) ).
fof(f24132,plain,
( v3_orders_2(sK111)
| ~ spl328_143 ),
inference(avatar_component_clause,[],[f24130]) ).
fof(f24133,plain,
spl328_143,
inference(avatar_split_clause,[],[f21314,f24130]) ).
fof(f24135,definition,
( spl328_144
<=> v2_orders_2(sK111) ),
introduced(definition,[new_symbols(definition,[spl328_144])],[avatar_definition]) ).
fof(f24137,plain,
( v2_orders_2(sK111)
| ~ spl328_144 ),
inference(avatar_component_clause,[],[f24135]) ).
fof(f24138,plain,
spl328_144,
inference(avatar_split_clause,[],[f21315,f24135]) ).
fof(f24140,definition,
( spl328_145
<=> m2_relset_1(sK112,sF327,sF327) ),
introduced(definition,[new_symbols(definition,[spl328_145])],[avatar_definition]) ).
fof(f24142,plain,
( m2_relset_1(sK112,sF327,sF327)
| ~ spl328_145 ),
inference(avatar_component_clause,[],[f24140]) ).
fof(f24143,plain,
spl328_145,
inference(avatar_split_clause,[],[f23382,f24140]) ).
fof(f24145,definition,
( spl328_146
<=> v7_waybel_1(sK112,sK111) ),
introduced(definition,[new_symbols(definition,[spl328_146])],[avatar_definition]) ).
fof(f24147,plain,
( v7_waybel_1(sK112,sK111)
| ~ spl328_146 ),
inference(avatar_component_clause,[],[f24145]) ).
fof(f24148,plain,
spl328_146,
inference(avatar_split_clause,[],[f21317,f24145]) ).
fof(f24150,definition,
( spl328_147
<=> v1_funct_2(sK112,sF327,sF327) ),
introduced(definition,[new_symbols(definition,[spl328_147])],[avatar_definition]) ).
fof(f24152,plain,
( v1_funct_2(sK112,sF327,sF327)
| ~ spl328_147 ),
inference(avatar_component_clause,[],[f24150]) ).
fof(f24153,plain,
spl328_147,
inference(avatar_split_clause,[],[f23381,f24150]) ).
fof(f24155,definition,
( spl328_148
<=> v1_funct_1(sK112) ),
introduced(definition,[new_symbols(definition,[spl328_148])],[avatar_definition]) ).
fof(f24157,plain,
( v1_funct_1(sK112)
| ~ spl328_148 ),
inference(avatar_component_clause,[],[f24155]) ).
fof(f24158,plain,
spl328_148,
inference(avatar_split_clause,[],[f21319,f24155]) ).
fof(f24160,definition,
( spl328_149
<=> v1_waybel34(sF326,sK111,sF325) ),
introduced(definition,[new_symbols(definition,[spl328_149])],[avatar_definition]) ).
fof(f24162,plain,
( v1_waybel34(sF326,sK111,sF325)
| ~ spl328_149 ),
inference(avatar_component_clause,[],[f24160]) ).
fof(f24163,plain,
spl328_149,
inference(avatar_split_clause,[],[f23378,f24160]) ).
fof(f24165,definition,
( spl328_150
<=> v4_waybel_0(sF325,sK111) ),
introduced(definition,[new_symbols(definition,[spl328_150])],[avatar_definition]) ).
fof(f24167,plain,
( ~ v4_waybel_0(sF325,sK111)
| spl328_150 ),
inference(avatar_component_clause,[],[f24165]) ).
fof(f24168,plain,
~ spl328_150,
inference(avatar_split_clause,[],[f23375,f24165]) ).
fof(f24179,definition,
( spl328_151
<=> k2_yellow_2(sK111,sK111,sK112) = sF325 ),
introduced(definition,[new_symbols(definition,[spl328_151])],[avatar_definition]) ).
fof(f24181,plain,
( k2_yellow_2(sK111,sK111,sK112) = sF325
| ~ spl328_151 ),
inference(avatar_component_clause,[],[f24179]) ).
fof(f24182,plain,
spl328_151,
inference(avatar_split_clause,[],[f23374,f24179]) ).
fof(f24184,definition,
( spl328_152
<=> k2_waybel_1(sK111,sK111,sK112) = sF326 ),
introduced(definition,[new_symbols(definition,[spl328_152])],[avatar_definition]) ).
fof(f24186,plain,
( k2_waybel_1(sK111,sK111,sK112) = sF326
| ~ spl328_152 ),
inference(avatar_component_clause,[],[f24184]) ).
fof(f24187,plain,
spl328_152,
inference(avatar_split_clause,[],[f23377,f24184]) ).
fof(f24189,definition,
( spl328_153
<=> u1_struct_0(sK111) = sF327 ),
introduced(definition,[new_symbols(definition,[spl328_153])],[avatar_definition]) ).
fof(f24191,plain,
( u1_struct_0(sK111) = sF327
| ~ spl328_153 ),
inference(avatar_component_clause,[],[f24189]) ).
fof(f24192,plain,
spl328_153,
inference(avatar_split_clause,[],[f23380,f24189]) ).
fof(f24225,plain,
( ! [X0] :
( ~ v22_waybel_0(k3_waybel_1(sK111,sK111,X0),k2_yellow_2(sK111,sK111,X0),sK111)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ v7_waybel_1(X0,sK111)
| ~ m2_relset_1(X0,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ v2_orders_2(sK111)
| ~ v3_orders_2(sK111)
| ~ v4_orders_2(sK111)
| ~ v1_lattice3(sK111)
| ~ v2_lattice3(sK111)
| v4_waybel_0(k2_yellow_2(sK111,sK111,X0),sK111)
| ~ l1_orders_2(sK111) )
| ~ spl328_139 ),
inference(resolution,[],[f21293,f24112]) ).
fof(f24226,plain,
( ! [X0] :
( ~ v22_waybel_0(k3_waybel_1(sK111,sK111,X0),k2_yellow_2(sK111,sK111,X0),sK111)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ v7_waybel_1(X0,sK111)
| ~ m2_relset_1(X0,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ v3_orders_2(sK111)
| ~ v4_orders_2(sK111)
| ~ v1_lattice3(sK111)
| ~ v2_lattice3(sK111)
| v4_waybel_0(k2_yellow_2(sK111,sK111,X0),sK111)
| ~ l1_orders_2(sK111) )
| ~ spl328_139
| ~ spl328_144 ),
inference(forward_subsumption_resolution,[],[f24225,f24137]) ).
fof(f24227,plain,
( ! [X0] :
( ~ v22_waybel_0(k3_waybel_1(sK111,sK111,X0),k2_yellow_2(sK111,sK111,X0),sK111)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ v7_waybel_1(X0,sK111)
| ~ m2_relset_1(X0,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ v4_orders_2(sK111)
| ~ v1_lattice3(sK111)
| ~ v2_lattice3(sK111)
| v4_waybel_0(k2_yellow_2(sK111,sK111,X0),sK111)
| ~ l1_orders_2(sK111) )
| ~ spl328_139
| ~ spl328_143
| ~ spl328_144 ),
inference(forward_subsumption_resolution,[],[f24226,f24132]) ).
fof(f24228,plain,
( ! [X0] :
( ~ v22_waybel_0(k3_waybel_1(sK111,sK111,X0),k2_yellow_2(sK111,sK111,X0),sK111)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ v7_waybel_1(X0,sK111)
| ~ m2_relset_1(X0,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ v1_lattice3(sK111)
| ~ v2_lattice3(sK111)
| v4_waybel_0(k2_yellow_2(sK111,sK111,X0),sK111)
| ~ l1_orders_2(sK111) )
| ~ spl328_139
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144 ),
inference(forward_subsumption_resolution,[],[f24227,f24127]) ).
fof(f24229,plain,
( ! [X0] :
( ~ v22_waybel_0(k3_waybel_1(sK111,sK111,X0),k2_yellow_2(sK111,sK111,X0),sK111)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ v7_waybel_1(X0,sK111)
| ~ m2_relset_1(X0,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ v2_lattice3(sK111)
| v4_waybel_0(k2_yellow_2(sK111,sK111,X0),sK111)
| ~ l1_orders_2(sK111) )
| ~ spl328_139
| ~ spl328_141
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144 ),
inference(forward_subsumption_resolution,[],[f24228,f24122]) ).
fof(f24230,plain,
( ! [X0] :
( ~ v22_waybel_0(k3_waybel_1(sK111,sK111,X0),k2_yellow_2(sK111,sK111,X0),sK111)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ v7_waybel_1(X0,sK111)
| ~ m2_relset_1(X0,u1_struct_0(sK111),u1_struct_0(sK111))
| v4_waybel_0(k2_yellow_2(sK111,sK111,X0),sK111)
| ~ l1_orders_2(sK111) )
| ~ spl328_139
| ~ spl328_140
| ~ spl328_141
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144 ),
inference(forward_subsumption_resolution,[],[f24229,f24117]) ).
fof(f24231,plain,
( ! [X0] :
( ~ v22_waybel_0(k3_waybel_1(sK111,sK111,X0),k2_yellow_2(sK111,sK111,X0),sK111)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ v7_waybel_1(X0,sK111)
| ~ m2_relset_1(X0,u1_struct_0(sK111),u1_struct_0(sK111))
| v4_waybel_0(k2_yellow_2(sK111,sK111,X0),sK111) )
| ~ spl328_137
| ~ spl328_139
| ~ spl328_140
| ~ spl328_141
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144 ),
inference(forward_subsumption_resolution,[],[f24230,f24102]) ).
fof(f24232,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF327,sF327)
| ~ v22_waybel_0(k3_waybel_1(sK111,sK111,X0),k2_yellow_2(sK111,sK111,X0),sK111)
| ~ v1_funct_1(X0)
| ~ v7_waybel_1(X0,sK111)
| ~ m2_relset_1(X0,u1_struct_0(sK111),u1_struct_0(sK111))
| v4_waybel_0(k2_yellow_2(sK111,sK111,X0),sK111) )
| ~ spl328_137
| ~ spl328_139
| ~ spl328_140
| ~ spl328_141
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144
| ~ spl328_153 ),
inference(forward_demodulation,[],[f24231,f24191]) ).
fof(f24233,plain,
( ! [X0] :
( ~ v22_waybel_0(k3_waybel_1(sK111,sK111,X0),k2_yellow_2(sK111,sK111,X0),sK111)
| ~ v1_funct_2(X0,sF327,sF327)
| ~ m2_relset_1(X0,sF327,sF327)
| ~ v1_funct_1(X0)
| ~ v7_waybel_1(X0,sK111)
| v4_waybel_0(k2_yellow_2(sK111,sK111,X0),sK111) )
| ~ spl328_137
| ~ spl328_139
| ~ spl328_140
| ~ spl328_141
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144
| ~ spl328_153 ),
inference(forward_demodulation,[],[f24232,f24191]) ).
fof(f24234,plain,
( ~ v22_waybel_0(k3_waybel_1(sK111,sK111,sK112),sF325,sK111)
| ~ v1_funct_2(sK112,sF327,sF327)
| ~ m2_relset_1(sK112,sF327,sF327)
| ~ v1_funct_1(sK112)
| ~ v7_waybel_1(sK112,sK111)
| v4_waybel_0(sF325,sK111)
| ~ spl328_137
| ~ spl328_139
| ~ spl328_140
| ~ spl328_141
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144
| ~ spl328_151
| ~ spl328_153 ),
inference(superposition,[],[f24233,f24181]) ).
fof(f24235,plain,
( ~ v22_waybel_0(k3_waybel_1(sK111,sK111,sK112),sF325,sK111)
| ~ m2_relset_1(sK112,sF327,sF327)
| ~ v1_funct_1(sK112)
| ~ v7_waybel_1(sK112,sK111)
| v4_waybel_0(sF325,sK111)
| ~ spl328_137
| ~ spl328_139
| ~ spl328_140
| ~ spl328_141
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144
| ~ spl328_147
| ~ spl328_151
| ~ spl328_153 ),
inference(forward_subsumption_resolution,[],[f24234,f24152]) ).
fof(f24236,plain,
( ~ v22_waybel_0(k3_waybel_1(sK111,sK111,sK112),sF325,sK111)
| ~ v1_funct_1(sK112)
| ~ v7_waybel_1(sK112,sK111)
| v4_waybel_0(sF325,sK111)
| ~ spl328_137
| ~ spl328_139
| ~ spl328_140
| ~ spl328_141
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144
| ~ spl328_145
| ~ spl328_147
| ~ spl328_151
| ~ spl328_153 ),
inference(forward_subsumption_resolution,[],[f24235,f24142]) ).
fof(f24237,plain,
( ~ v22_waybel_0(k3_waybel_1(sK111,sK111,sK112),sF325,sK111)
| ~ v7_waybel_1(sK112,sK111)
| v4_waybel_0(sF325,sK111)
| ~ spl328_137
| ~ spl328_139
| ~ spl328_140
| ~ spl328_141
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144
| ~ spl328_145
| ~ spl328_147
| ~ spl328_148
| ~ spl328_151
| ~ spl328_153 ),
inference(forward_subsumption_resolution,[],[f24236,f24157]) ).
fof(f24238,plain,
( ~ v22_waybel_0(k3_waybel_1(sK111,sK111,sK112),sF325,sK111)
| v4_waybel_0(sF325,sK111)
| ~ spl328_137
| ~ spl328_139
| ~ spl328_140
| ~ spl328_141
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144
| ~ spl328_145
| ~ spl328_146
| ~ spl328_147
| ~ spl328_148
| ~ spl328_151
| ~ spl328_153 ),
inference(forward_subsumption_resolution,[],[f24237,f24147]) ).
fof(f24239,plain,
( ~ v22_waybel_0(k3_waybel_1(sK111,sK111,sK112),sF325,sK111)
| ~ spl328_137
| ~ spl328_139
| ~ spl328_140
| ~ spl328_141
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144
| ~ spl328_145
| ~ spl328_146
| ~ spl328_147
| ~ spl328_148
| spl328_150
| ~ spl328_151
| ~ spl328_153 ),
inference(forward_subsumption_resolution,[],[f24238,f24167]) ).
fof(f24241,definition,
( spl328_154
<=> v22_waybel_0(k3_waybel_1(sK111,sK111,sK112),sF325,sK111) ),
introduced(definition,[new_symbols(definition,[spl328_154])],[avatar_definition]) ).
fof(f24243,plain,
( ~ v22_waybel_0(k3_waybel_1(sK111,sK111,sK112),sF325,sK111)
| spl328_154 ),
inference(avatar_component_clause,[],[f24241]) ).
fof(f24244,plain,
( ~ spl328_154
| ~ spl328_137
| ~ spl328_139
| ~ spl328_140
| ~ spl328_141
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144
| ~ spl328_145
| ~ spl328_146
| ~ spl328_147
| ~ spl328_148
| spl328_150
| ~ spl328_151
| ~ spl328_153 ),
inference(avatar_split_clause,[],[f24239,f24189,f24179,f24165,f24155,f24150,f24145,f24140,f24135,f24130,f24125,f24120,f24115,f24110,f24100,f24241]) ).
fof(f24263,plain,
( m1_relset_1(sK112,sF327,sF327)
| ~ spl328_145 ),
inference(unit_resulting_resolution,[],[f21333,f24142]) ).
fof(f24265,definition,
( spl328_155
<=> m1_relset_1(sK112,sF327,sF327) ),
introduced(definition,[new_symbols(definition,[spl328_155])],[avatar_definition]) ).
fof(f24267,plain,
( m1_relset_1(sK112,sF327,sF327)
| ~ spl328_155 ),
inference(avatar_component_clause,[],[f24265]) ).
fof(f24268,plain,
( spl328_155
| ~ spl328_145 ),
inference(avatar_split_clause,[],[f24263,f24140,f24265]) ).
fof(f24270,plain,
( ~ v3_struct_0(sK111)
| ~ spl328_137
| ~ spl328_141 ),
inference(unit_resulting_resolution,[],[f21340,f24102,f24122]) ).
fof(f24274,definition,
( spl328_156
<=> v3_struct_0(sK111) ),
introduced(definition,[new_symbols(definition,[spl328_156])],[avatar_definition]) ).
fof(f24276,plain,
( ~ v3_struct_0(sK111)
| spl328_156 ),
inference(avatar_component_clause,[],[f24274]) ).
fof(f24277,plain,
( ~ spl328_156
| ~ spl328_137
| ~ spl328_141 ),
inference(avatar_split_clause,[],[f24270,f24120,f24100,f24274]) ).
fof(f24279,plain,
( ! [X0,X1] :
( m1_yellow_0(k2_yellow_2(sK111,X0,X1),X0)
| ~ l1_orders_2(sK111)
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK111),u1_struct_0(X0))
| ~ m1_relset_1(X1,u1_struct_0(sK111),u1_struct_0(X0)) )
| spl328_156 ),
inference(resolution,[],[f24276,f22836]) ).
fof(f24280,plain,
( ! [X0,X1] :
( ~ v3_struct_0(k2_yellow_2(sK111,X0,X1))
| ~ l1_orders_2(sK111)
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK111),u1_struct_0(X0))
| ~ m1_relset_1(X1,u1_struct_0(sK111),u1_struct_0(X0)) )
| spl328_156 ),
inference(resolution,[],[f24276,f22841]) ).
fof(f24282,plain,
( ! [X0,X1] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(sK111))
| ~ m2_relset_1(X0,u1_struct_0(X1),u1_struct_0(sK111))
| k2_waybel_1(X1,sK111,X0) = X0
| ~ l1_orders_2(sK111)
| v3_struct_0(X1)
| ~ l1_orders_2(X1) )
| spl328_156 ),
inference(resolution,[],[f24276,f23158]) ).
fof(f24287,plain,
( ! [X0,X1] :
( m2_relset_1(k3_waybel_1(sK111,X0,X1),u1_struct_0(k2_yellow_2(sK111,X0,X1)),u1_struct_0(X0))
| ~ l1_orders_2(sK111)
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK111),u1_struct_0(X0))
| ~ m1_relset_1(X1,u1_struct_0(sK111),u1_struct_0(X0)) )
| spl328_156 ),
inference(resolution,[],[f24276,f23167]) ).
fof(f24288,plain,
( ! [X0,X1] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(sK111))
| ~ m2_relset_1(X0,u1_struct_0(X1),u1_struct_0(sK111))
| k3_waybel_1(X1,sK111,X0) = k7_grcat_1(k2_yellow_2(X1,sK111,X0))
| ~ l1_orders_2(sK111)
| v3_struct_0(X1)
| ~ l1_orders_2(X1) )
| spl328_156 ),
inference(resolution,[],[f24276,f23174]) ).
fof(f24289,plain,
( ! [X0,X1] :
( v1_funct_2(k3_waybel_1(sK111,X0,X1),u1_struct_0(k2_yellow_2(sK111,X0,X1)),u1_struct_0(X0))
| ~ l1_orders_2(sK111)
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK111),u1_struct_0(X0))
| ~ m1_relset_1(X1,u1_struct_0(sK111),u1_struct_0(X0)) )
| spl328_156 ),
inference(resolution,[],[f24276,f23177]) ).
fof(f24290,plain,
( ! [X0,X1] :
( v1_funct_2(k3_waybel_1(sK111,X0,X1),u1_struct_0(k2_yellow_2(sK111,X0,X1)),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK111),u1_struct_0(X0))
| ~ m1_relset_1(X1,u1_struct_0(sK111),u1_struct_0(X0)) )
| ~ spl328_137
| spl328_156 ),
inference(forward_subsumption_resolution,[],[f24289,f24102]) ).
fof(f24291,plain,
( ! [X0,X1] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(sK111))
| ~ m2_relset_1(X0,u1_struct_0(X1),u1_struct_0(sK111))
| k3_waybel_1(X1,sK111,X0) = k7_grcat_1(k2_yellow_2(X1,sK111,X0))
| v3_struct_0(X1)
| ~ l1_orders_2(X1) )
| ~ spl328_137
| spl328_156 ),
inference(forward_subsumption_resolution,[],[f24288,f24102]) ).
fof(f24292,plain,
( ! [X0,X1] :
( m2_relset_1(k3_waybel_1(sK111,X0,X1),u1_struct_0(k2_yellow_2(sK111,X0,X1)),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK111),u1_struct_0(X0))
| ~ m1_relset_1(X1,u1_struct_0(sK111),u1_struct_0(X0)) )
| ~ spl328_137
| spl328_156 ),
inference(forward_subsumption_resolution,[],[f24287,f24102]) ).
fof(f24297,plain,
( ! [X0,X1] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(sK111))
| ~ m2_relset_1(X0,u1_struct_0(X1),u1_struct_0(sK111))
| k2_waybel_1(X1,sK111,X0) = X0
| v3_struct_0(X1)
| ~ l1_orders_2(X1) )
| ~ spl328_137
| spl328_156 ),
inference(forward_subsumption_resolution,[],[f24282,f24102]) ).
fof(f24299,plain,
( ! [X0,X1] :
( ~ v3_struct_0(k2_yellow_2(sK111,X0,X1))
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK111),u1_struct_0(X0))
| ~ m1_relset_1(X1,u1_struct_0(sK111),u1_struct_0(X0)) )
| ~ spl328_137
| spl328_156 ),
inference(forward_subsumption_resolution,[],[f24280,f24102]) ).
fof(f24300,plain,
( ! [X0,X1] :
( m1_yellow_0(k2_yellow_2(sK111,X0,X1),X0)
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK111),u1_struct_0(X0))
| ~ m1_relset_1(X1,u1_struct_0(sK111),u1_struct_0(X0)) )
| ~ spl328_137
| spl328_156 ),
inference(forward_subsumption_resolution,[],[f24279,f24102]) ).
fof(f24302,plain,
( ! [X0,X1] :
( ~ v1_funct_2(X1,sF327,u1_struct_0(X0))
| v1_funct_2(k3_waybel_1(sK111,X0,X1),u1_struct_0(k2_yellow_2(sK111,X0,X1)),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ m1_relset_1(X1,u1_struct_0(sK111),u1_struct_0(X0)) )
| ~ spl328_137
| ~ spl328_153
| spl328_156 ),
inference(forward_demodulation,[],[f24290,f24191]) ).
fof(f24303,plain,
( ! [X0,X1] :
( ~ v1_funct_2(X0,u1_struct_0(X1),sF327)
| ~ v1_funct_1(X0)
| ~ m2_relset_1(X0,u1_struct_0(X1),u1_struct_0(sK111))
| k3_waybel_1(X1,sK111,X0) = k7_grcat_1(k2_yellow_2(X1,sK111,X0))
| v3_struct_0(X1)
| ~ l1_orders_2(X1) )
| ~ spl328_137
| ~ spl328_153
| spl328_156 ),
inference(forward_demodulation,[],[f24291,f24191]) ).
fof(f24304,plain,
( ! [X0,X1] :
( ~ v1_funct_2(X1,sF327,u1_struct_0(X0))
| m2_relset_1(k3_waybel_1(sK111,X0,X1),u1_struct_0(k2_yellow_2(sK111,X0,X1)),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ m1_relset_1(X1,u1_struct_0(sK111),u1_struct_0(X0)) )
| ~ spl328_137
| ~ spl328_153
| spl328_156 ),
inference(forward_demodulation,[],[f24292,f24191]) ).
fof(f24309,plain,
( ! [X0,X1] :
( ~ v1_funct_2(X0,u1_struct_0(X1),sF327)
| ~ v1_funct_1(X0)
| ~ m2_relset_1(X0,u1_struct_0(X1),u1_struct_0(sK111))
| k2_waybel_1(X1,sK111,X0) = X0
| v3_struct_0(X1)
| ~ l1_orders_2(X1) )
| ~ spl328_137
| ~ spl328_153
| spl328_156 ),
inference(forward_demodulation,[],[f24297,f24191]) ).
fof(f24311,plain,
( ! [X0,X1] :
( ~ v1_funct_2(X1,sF327,u1_struct_0(X0))
| ~ v3_struct_0(k2_yellow_2(sK111,X0,X1))
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ m1_relset_1(X1,u1_struct_0(sK111),u1_struct_0(X0)) )
| ~ spl328_137
| ~ spl328_153
| spl328_156 ),
inference(forward_demodulation,[],[f24299,f24191]) ).
fof(f24312,plain,
( ! [X0,X1] :
( ~ v1_funct_2(X1,sF327,u1_struct_0(X0))
| m1_yellow_0(k2_yellow_2(sK111,X0,X1),X0)
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ m1_relset_1(X1,u1_struct_0(sK111),u1_struct_0(X0)) )
| ~ spl328_137
| ~ spl328_153
| spl328_156 ),
inference(forward_demodulation,[],[f24300,f24191]) ).
fof(f24314,plain,
( ! [X0,X1] :
( ~ l1_orders_2(X0)
| ~ v1_funct_2(X1,sF327,u1_struct_0(X0))
| v1_funct_2(k3_waybel_1(sK111,X0,X1),u1_struct_0(k2_yellow_2(sK111,X0,X1)),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ m1_relset_1(X1,sF327,u1_struct_0(X0))
| ~ v1_funct_1(X1) )
| ~ spl328_137
| ~ spl328_153
| spl328_156 ),
inference(forward_demodulation,[],[f24302,f24191]) ).
fof(f24315,plain,
( ! [X0,X1] :
( ~ l1_orders_2(X1)
| ~ v1_funct_2(X0,u1_struct_0(X1),sF327)
| ~ v1_funct_1(X0)
| k3_waybel_1(X1,sK111,X0) = k7_grcat_1(k2_yellow_2(X1,sK111,X0))
| v3_struct_0(X1)
| ~ m2_relset_1(X0,u1_struct_0(X1),sF327) )
| ~ spl328_137
| ~ spl328_153
| spl328_156 ),
inference(forward_demodulation,[],[f24303,f24191]) ).
fof(f24316,plain,
( ! [X0,X1] :
( ~ l1_orders_2(X0)
| ~ v1_funct_2(X1,sF327,u1_struct_0(X0))
| m2_relset_1(k3_waybel_1(sK111,X0,X1),u1_struct_0(k2_yellow_2(sK111,X0,X1)),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ m1_relset_1(X1,sF327,u1_struct_0(X0))
| ~ v1_funct_1(X1) )
| ~ spl328_137
| ~ spl328_153
| spl328_156 ),
inference(forward_demodulation,[],[f24304,f24191]) ).
fof(f24321,plain,
( ! [X0,X1] :
( ~ l1_orders_2(X1)
| ~ v1_funct_2(X0,u1_struct_0(X1),sF327)
| ~ v1_funct_1(X0)
| k2_waybel_1(X1,sK111,X0) = X0
| v3_struct_0(X1)
| ~ m2_relset_1(X0,u1_struct_0(X1),sF327) )
| ~ spl328_137
| ~ spl328_153
| spl328_156 ),
inference(forward_demodulation,[],[f24309,f24191]) ).
fof(f24323,plain,
( ! [X0,X1] :
( ~ l1_orders_2(X0)
| ~ v1_funct_2(X1,sF327,u1_struct_0(X0))
| ~ v3_struct_0(k2_yellow_2(sK111,X0,X1))
| v3_struct_0(X0)
| ~ m1_relset_1(X1,sF327,u1_struct_0(X0))
| ~ v1_funct_1(X1) )
| ~ spl328_137
| ~ spl328_153
| spl328_156 ),
inference(forward_demodulation,[],[f24311,f24191]) ).
fof(f24324,plain,
( ! [X0,X1] :
( ~ l1_orders_2(X0)
| ~ v1_funct_2(X1,sF327,u1_struct_0(X0))
| m1_yellow_0(k2_yellow_2(sK111,X0,X1),X0)
| v3_struct_0(X0)
| ~ m1_relset_1(X1,sF327,u1_struct_0(X0))
| ~ v1_funct_1(X1) )
| ~ spl328_137
| ~ spl328_153
| spl328_156 ),
inference(forward_demodulation,[],[f24312,f24191]) ).
fof(f24329,plain,
( ! [X0] :
( ~ v1_funct_2(X0,u1_struct_0(sK111),sF327)
| ~ v1_funct_1(X0)
| k2_waybel_1(sK111,sK111,X0) = X0
| v3_struct_0(sK111)
| ~ m2_relset_1(X0,u1_struct_0(sK111),sF327) )
| ~ spl328_137
| ~ spl328_153
| spl328_156 ),
inference(resolution,[],[f24321,f24102]) ).
fof(f24330,plain,
( ! [X0] :
( ~ v1_funct_2(X0,u1_struct_0(sK111),sF327)
| ~ v1_funct_1(X0)
| k2_waybel_1(sK111,sK111,X0) = X0
| ~ m2_relset_1(X0,u1_struct_0(sK111),sF327) )
| ~ spl328_137
| ~ spl328_153
| spl328_156 ),
inference(forward_subsumption_resolution,[],[f24329,f24276]) ).
fof(f24331,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF327,sF327)
| ~ v1_funct_1(X0)
| k2_waybel_1(sK111,sK111,X0) = X0
| ~ m2_relset_1(X0,u1_struct_0(sK111),sF327) )
| ~ spl328_137
| ~ spl328_153
| spl328_156 ),
inference(forward_demodulation,[],[f24330,f24191]) ).
fof(f24332,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF327,sF327)
| ~ m2_relset_1(X0,sF327,sF327)
| ~ v1_funct_1(X0)
| k2_waybel_1(sK111,sK111,X0) = X0 )
| ~ spl328_137
| ~ spl328_153
| spl328_156 ),
inference(forward_demodulation,[],[f24331,f24191]) ).
fof(f24333,plain,
( sK112 = k2_waybel_1(sK111,sK111,sK112)
| ~ spl328_137
| ~ spl328_145
| ~ spl328_147
| ~ spl328_148
| ~ spl328_153
| spl328_156 ),
inference(unit_resulting_resolution,[],[f24332,f24157,f24152,f24142]) ).
fof(f24337,definition,
( spl328_157
<=> sK112 = k2_waybel_1(sK111,sK111,sK112) ),
introduced(definition,[new_symbols(definition,[spl328_157])],[avatar_definition]) ).
fof(f24339,plain,
( sK112 = k2_waybel_1(sK111,sK111,sK112)
| ~ spl328_157 ),
inference(avatar_component_clause,[],[f24337]) ).
fof(f24340,plain,
( spl328_157
| ~ spl328_137
| ~ spl328_145
| ~ spl328_147
| ~ spl328_148
| ~ spl328_153
| spl328_156 ),
inference(avatar_split_clause,[],[f24333,f24274,f24189,f24155,f24150,f24140,f24100,f24337]) ).
fof(f24441,plain,
( ! [X0] :
( ~ v1_funct_2(X0,u1_struct_0(sK111),sF327)
| ~ v1_funct_1(X0)
| k3_waybel_1(sK111,sK111,X0) = k7_grcat_1(k2_yellow_2(sK111,sK111,X0))
| v3_struct_0(sK111)
| ~ m2_relset_1(X0,u1_struct_0(sK111),sF327) )
| ~ spl328_137
| ~ spl328_153
| spl328_156 ),
inference(resolution,[],[f24315,f24102]) ).
fof(f24442,plain,
( ! [X0] :
( ~ v1_funct_2(X0,u1_struct_0(sK111),sF327)
| ~ v1_funct_1(X0)
| k3_waybel_1(sK111,sK111,X0) = k7_grcat_1(k2_yellow_2(sK111,sK111,X0))
| ~ m2_relset_1(X0,u1_struct_0(sK111),sF327) )
| ~ spl328_137
| ~ spl328_153
| spl328_156 ),
inference(forward_subsumption_resolution,[],[f24441,f24276]) ).
fof(f24443,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF327,sF327)
| ~ v1_funct_1(X0)
| k3_waybel_1(sK111,sK111,X0) = k7_grcat_1(k2_yellow_2(sK111,sK111,X0))
| ~ m2_relset_1(X0,u1_struct_0(sK111),sF327) )
| ~ spl328_137
| ~ spl328_153
| spl328_156 ),
inference(forward_demodulation,[],[f24442,f24191]) ).
fof(f24444,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF327,sF327)
| ~ m2_relset_1(X0,sF327,sF327)
| ~ v1_funct_1(X0)
| k3_waybel_1(sK111,sK111,X0) = k7_grcat_1(k2_yellow_2(sK111,sK111,X0)) )
| ~ spl328_137
| ~ spl328_153
| spl328_156 ),
inference(forward_demodulation,[],[f24443,f24191]) ).
fof(f24445,plain,
( k3_waybel_1(sK111,sK111,sK112) = k7_grcat_1(k2_yellow_2(sK111,sK111,sK112))
| ~ spl328_137
| ~ spl328_145
| ~ spl328_147
| ~ spl328_148
| ~ spl328_153
| spl328_156 ),
inference(unit_resulting_resolution,[],[f24444,f24157,f24152,f24142]) ).
fof(f24448,plain,
( k3_waybel_1(sK111,sK111,sK112) = k7_grcat_1(sF325)
| ~ spl328_137
| ~ spl328_145
| ~ spl328_147
| ~ spl328_148
| ~ spl328_151
| ~ spl328_153
| spl328_156 ),
inference(forward_demodulation,[],[f24445,f24181]) ).
fof(f24451,definition,
( spl328_162
<=> k3_waybel_1(sK111,sK111,sK112) = k7_grcat_1(sF325) ),
introduced(definition,[new_symbols(definition,[spl328_162])],[avatar_definition]) ).
fof(f24453,plain,
( k3_waybel_1(sK111,sK111,sK112) = k7_grcat_1(sF325)
| ~ spl328_162 ),
inference(avatar_component_clause,[],[f24451]) ).
fof(f24454,plain,
( spl328_162
| ~ spl328_137
| ~ spl328_145
| ~ spl328_147
| ~ spl328_148
| ~ spl328_151
| ~ spl328_153
| spl328_156 ),
inference(avatar_split_clause,[],[f24448,f24274,f24189,f24179,f24155,f24150,f24140,f24100,f24451]) ).
fof(f24456,plain,
( ~ v22_waybel_0(k7_grcat_1(sF325),sF325,sK111)
| spl328_154
| ~ spl328_162 ),
inference(superposition,[],[f24243,f24453]) ).
fof(f24460,definition,
( spl328_163
<=> v22_waybel_0(k7_grcat_1(sF325),sF325,sK111) ),
introduced(definition,[new_symbols(definition,[spl328_163])],[avatar_definition]) ).
fof(f24462,plain,
( ~ v22_waybel_0(k7_grcat_1(sF325),sF325,sK111)
| spl328_163 ),
inference(avatar_component_clause,[],[f24460]) ).
fof(f24463,plain,
( ~ spl328_163
| spl328_154
| ~ spl328_162 ),
inference(avatar_split_clause,[],[f24456,f24451,f24241,f24460]) ).
fof(f24476,plain,
( sK112 = sF326
| ~ spl328_152
| ~ spl328_157 ),
inference(superposition,[],[f24186,f24339]) ).
fof(f24478,definition,
( spl328_164
<=> sK112 = sF326 ),
introduced(definition,[new_symbols(definition,[spl328_164])],[avatar_definition]) ).
fof(f24480,plain,
( sK112 = sF326
| ~ spl328_164 ),
inference(avatar_component_clause,[],[f24478]) ).
fof(f24481,plain,
( spl328_164
| ~ spl328_152
| ~ spl328_157 ),
inference(avatar_split_clause,[],[f24476,f24337,f24184,f24478]) ).
fof(f24483,plain,
( v1_waybel34(sK112,sK111,sF325)
| ~ spl328_149
| ~ spl328_164 ),
inference(superposition,[],[f24162,f24480]) ).
fof(f24485,definition,
( spl328_165
<=> v1_waybel34(sK112,sK111,sF325) ),
introduced(definition,[new_symbols(definition,[spl328_165])],[avatar_definition]) ).
fof(f24487,plain,
( v1_waybel34(sK112,sK111,sF325)
| ~ spl328_165 ),
inference(avatar_component_clause,[],[f24485]) ).
fof(f24488,plain,
( spl328_165
| ~ spl328_149
| ~ spl328_164 ),
inference(avatar_split_clause,[],[f24483,f24478,f24160,f24485]) ).
fof(f24520,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF327,u1_struct_0(sK111))
| ~ v3_struct_0(k2_yellow_2(sK111,sK111,X0))
| v3_struct_0(sK111)
| ~ m1_relset_1(X0,sF327,u1_struct_0(sK111))
| ~ v1_funct_1(X0) )
| ~ spl328_137
| ~ spl328_153
| spl328_156 ),
inference(resolution,[],[f24323,f24102]) ).
fof(f24521,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF327,u1_struct_0(sK111))
| ~ v3_struct_0(k2_yellow_2(sK111,sK111,X0))
| ~ m1_relset_1(X0,sF327,u1_struct_0(sK111))
| ~ v1_funct_1(X0) )
| ~ spl328_137
| ~ spl328_153
| spl328_156 ),
inference(forward_subsumption_resolution,[],[f24520,f24276]) ).
fof(f24522,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF327,sF327)
| ~ v3_struct_0(k2_yellow_2(sK111,sK111,X0))
| ~ m1_relset_1(X0,sF327,u1_struct_0(sK111))
| ~ v1_funct_1(X0) )
| ~ spl328_137
| ~ spl328_153
| spl328_156 ),
inference(forward_demodulation,[],[f24521,f24191]) ).
fof(f24523,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF327,sF327)
| ~ m1_relset_1(X0,sF327,sF327)
| ~ v3_struct_0(k2_yellow_2(sK111,sK111,X0))
| ~ v1_funct_1(X0) )
| ~ spl328_137
| ~ spl328_153
| spl328_156 ),
inference(forward_demodulation,[],[f24522,f24191]) ).
fof(f24524,plain,
( ~ v3_struct_0(k2_yellow_2(sK111,sK111,sK112))
| ~ spl328_137
| ~ spl328_147
| ~ spl328_148
| ~ spl328_153
| ~ spl328_155
| spl328_156 ),
inference(unit_resulting_resolution,[],[f24523,f24157,f24152,f24267]) ).
fof(f24527,plain,
( ~ v3_struct_0(sF325)
| ~ spl328_137
| ~ spl328_147
| ~ spl328_148
| ~ spl328_151
| ~ spl328_153
| ~ spl328_155
| spl328_156 ),
inference(forward_demodulation,[],[f24524,f24181]) ).
fof(f24530,definition,
( spl328_167
<=> v3_struct_0(sF325) ),
introduced(definition,[new_symbols(definition,[spl328_167])],[avatar_definition]) ).
fof(f24532,plain,
( ~ v3_struct_0(sF325)
| spl328_167 ),
inference(avatar_component_clause,[],[f24530]) ).
fof(f24533,plain,
( ~ spl328_167
| ~ spl328_137
| ~ spl328_147
| ~ spl328_148
| ~ spl328_151
| ~ spl328_153
| ~ spl328_155
| spl328_156 ),
inference(avatar_split_clause,[],[f24527,f24274,f24265,f24189,f24179,f24155,f24150,f24100,f24530]) ).
fof(f24548,definition,
( spl328_168
<=> l1_orders_2(sF325) ),
introduced(definition,[new_symbols(definition,[spl328_168])],[avatar_definition]) ).
fof(f24549,plain,
( l1_orders_2(sF325)
| ~ spl328_168 ),
inference(avatar_component_clause,[],[f24548]) ).
fof(f24550,plain,
( ~ l1_orders_2(sF325)
| spl328_168 ),
inference(avatar_component_clause,[],[f24548]) ).
fof(f24631,plain,
( ! [X0] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ v7_waybel_1(X0,sK111)
| ~ m2_relset_1(X0,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ v2_orders_2(sK111)
| ~ v3_orders_2(sK111)
| ~ v4_orders_2(sK111)
| ~ v1_lattice3(sK111)
| ~ v2_lattice3(sK111)
| v17_waybel_0(k3_waybel_1(sK111,sK111,X0),k2_yellow_2(sK111,sK111,X0),sK111)
| ~ l1_orders_2(sK111) )
| ~ spl328_139 ),
inference(resolution,[],[f21290,f24112]) ).
fof(f24632,plain,
( ! [X0] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ v7_waybel_1(X0,sK111)
| ~ m2_relset_1(X0,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ v3_orders_2(sK111)
| ~ v4_orders_2(sK111)
| ~ v1_lattice3(sK111)
| ~ v2_lattice3(sK111)
| v17_waybel_0(k3_waybel_1(sK111,sK111,X0),k2_yellow_2(sK111,sK111,X0),sK111)
| ~ l1_orders_2(sK111) )
| ~ spl328_139
| ~ spl328_144 ),
inference(forward_subsumption_resolution,[],[f24631,f24137]) ).
fof(f24633,plain,
( ! [X0] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ v7_waybel_1(X0,sK111)
| ~ m2_relset_1(X0,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ v4_orders_2(sK111)
| ~ v1_lattice3(sK111)
| ~ v2_lattice3(sK111)
| v17_waybel_0(k3_waybel_1(sK111,sK111,X0),k2_yellow_2(sK111,sK111,X0),sK111)
| ~ l1_orders_2(sK111) )
| ~ spl328_139
| ~ spl328_143
| ~ spl328_144 ),
inference(forward_subsumption_resolution,[],[f24632,f24132]) ).
fof(f24634,plain,
( ! [X0] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ v7_waybel_1(X0,sK111)
| ~ m2_relset_1(X0,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ v1_lattice3(sK111)
| ~ v2_lattice3(sK111)
| v17_waybel_0(k3_waybel_1(sK111,sK111,X0),k2_yellow_2(sK111,sK111,X0),sK111)
| ~ l1_orders_2(sK111) )
| ~ spl328_139
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144 ),
inference(forward_subsumption_resolution,[],[f24633,f24127]) ).
fof(f24635,plain,
( ! [X0] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ v7_waybel_1(X0,sK111)
| ~ m2_relset_1(X0,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ v2_lattice3(sK111)
| v17_waybel_0(k3_waybel_1(sK111,sK111,X0),k2_yellow_2(sK111,sK111,X0),sK111)
| ~ l1_orders_2(sK111) )
| ~ spl328_139
| ~ spl328_141
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144 ),
inference(forward_subsumption_resolution,[],[f24634,f24122]) ).
fof(f24636,plain,
( ! [X0] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ v7_waybel_1(X0,sK111)
| ~ m2_relset_1(X0,u1_struct_0(sK111),u1_struct_0(sK111))
| v17_waybel_0(k3_waybel_1(sK111,sK111,X0),k2_yellow_2(sK111,sK111,X0),sK111)
| ~ l1_orders_2(sK111) )
| ~ spl328_139
| ~ spl328_140
| ~ spl328_141
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144 ),
inference(forward_subsumption_resolution,[],[f24635,f24117]) ).
fof(f24637,plain,
( ! [X0] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ v7_waybel_1(X0,sK111)
| ~ m2_relset_1(X0,u1_struct_0(sK111),u1_struct_0(sK111))
| v17_waybel_0(k3_waybel_1(sK111,sK111,X0),k2_yellow_2(sK111,sK111,X0),sK111) )
| ~ spl328_137
| ~ spl328_139
| ~ spl328_140
| ~ spl328_141
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144 ),
inference(forward_subsumption_resolution,[],[f24636,f24102]) ).
fof(f24638,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF327,sF327)
| ~ v1_funct_1(X0)
| ~ v7_waybel_1(X0,sK111)
| ~ m2_relset_1(X0,u1_struct_0(sK111),u1_struct_0(sK111))
| v17_waybel_0(k3_waybel_1(sK111,sK111,X0),k2_yellow_2(sK111,sK111,X0),sK111) )
| ~ spl328_137
| ~ spl328_139
| ~ spl328_140
| ~ spl328_141
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144
| ~ spl328_153 ),
inference(forward_demodulation,[],[f24637,f24191]) ).
fof(f24639,plain,
( ! [X0] :
( ~ v7_waybel_1(X0,sK111)
| ~ v1_funct_2(X0,sF327,sF327)
| ~ v1_funct_1(X0)
| ~ m2_relset_1(X0,sF327,sF327)
| v17_waybel_0(k3_waybel_1(sK111,sK111,X0),k2_yellow_2(sK111,sK111,X0),sK111) )
| ~ spl328_137
| ~ spl328_139
| ~ spl328_140
| ~ spl328_141
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144
| ~ spl328_153 ),
inference(forward_demodulation,[],[f24638,f24191]) ).
fof(f24640,plain,
( v17_waybel_0(k3_waybel_1(sK111,sK111,sK112),k2_yellow_2(sK111,sK111,sK112),sK111)
| ~ spl328_137
| ~ spl328_139
| ~ spl328_140
| ~ spl328_141
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144
| ~ spl328_145
| ~ spl328_146
| ~ spl328_147
| ~ spl328_148
| ~ spl328_153 ),
inference(unit_resulting_resolution,[],[f24639,f24157,f24147,f24142,f24152]) ).
fof(f24643,plain,
( v17_waybel_0(k3_waybel_1(sK111,sK111,sK112),sF325,sK111)
| ~ spl328_137
| ~ spl328_139
| ~ spl328_140
| ~ spl328_141
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144
| ~ spl328_145
| ~ spl328_146
| ~ spl328_147
| ~ spl328_148
| ~ spl328_151
| ~ spl328_153 ),
inference(forward_demodulation,[],[f24640,f24181]) ).
fof(f24645,plain,
( v17_waybel_0(k7_grcat_1(sF325),sF325,sK111)
| ~ spl328_137
| ~ spl328_139
| ~ spl328_140
| ~ spl328_141
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144
| ~ spl328_145
| ~ spl328_146
| ~ spl328_147
| ~ spl328_148
| ~ spl328_151
| ~ spl328_153
| ~ spl328_162 ),
inference(forward_demodulation,[],[f24643,f24453]) ).
fof(f24648,definition,
( spl328_183
<=> v17_waybel_0(k7_grcat_1(sF325),sF325,sK111) ),
introduced(definition,[new_symbols(definition,[spl328_183])],[avatar_definition]) ).
fof(f24650,plain,
( v17_waybel_0(k7_grcat_1(sF325),sF325,sK111)
| ~ spl328_183 ),
inference(avatar_component_clause,[],[f24648]) ).
fof(f24651,plain,
( spl328_183
| ~ spl328_137
| ~ spl328_139
| ~ spl328_140
| ~ spl328_141
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144
| ~ spl328_145
| ~ spl328_146
| ~ spl328_147
| ~ spl328_148
| ~ spl328_151
| ~ spl328_153
| ~ spl328_162 ),
inference(avatar_split_clause,[],[f24645,f24451,f24189,f24179,f24155,f24150,f24145,f24140,f24135,f24130,f24125,f24120,f24115,f24110,f24100,f24648]) ).
fof(f24654,plain,
( ! [X0] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ v7_waybel_1(X0,sK111)
| ~ m2_relset_1(X0,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ v2_orders_2(sK111)
| ~ v3_orders_2(sK111)
| ~ v4_orders_2(sK111)
| ~ v1_lattice3(sK111)
| ~ v2_lattice3(sK111)
| k2_waybel_1(sK111,sK111,X0) = k1_waybel34(k2_yellow_2(sK111,sK111,X0),sK111,k3_waybel_1(sK111,sK111,X0))
| ~ l1_orders_2(sK111) )
| ~ spl328_139 ),
inference(resolution,[],[f21288,f24112]) ).
fof(f24655,plain,
( ! [X0] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ v7_waybel_1(X0,sK111)
| ~ m2_relset_1(X0,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ v3_orders_2(sK111)
| ~ v4_orders_2(sK111)
| ~ v1_lattice3(sK111)
| ~ v2_lattice3(sK111)
| k2_waybel_1(sK111,sK111,X0) = k1_waybel34(k2_yellow_2(sK111,sK111,X0),sK111,k3_waybel_1(sK111,sK111,X0))
| ~ l1_orders_2(sK111) )
| ~ spl328_139
| ~ spl328_144 ),
inference(forward_subsumption_resolution,[],[f24654,f24137]) ).
fof(f24656,plain,
( ! [X0] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ v7_waybel_1(X0,sK111)
| ~ m2_relset_1(X0,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ v4_orders_2(sK111)
| ~ v1_lattice3(sK111)
| ~ v2_lattice3(sK111)
| k2_waybel_1(sK111,sK111,X0) = k1_waybel34(k2_yellow_2(sK111,sK111,X0),sK111,k3_waybel_1(sK111,sK111,X0))
| ~ l1_orders_2(sK111) )
| ~ spl328_139
| ~ spl328_143
| ~ spl328_144 ),
inference(forward_subsumption_resolution,[],[f24655,f24132]) ).
fof(f24657,plain,
( ! [X0] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ v7_waybel_1(X0,sK111)
| ~ m2_relset_1(X0,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ v1_lattice3(sK111)
| ~ v2_lattice3(sK111)
| k2_waybel_1(sK111,sK111,X0) = k1_waybel34(k2_yellow_2(sK111,sK111,X0),sK111,k3_waybel_1(sK111,sK111,X0))
| ~ l1_orders_2(sK111) )
| ~ spl328_139
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144 ),
inference(forward_subsumption_resolution,[],[f24656,f24127]) ).
fof(f24658,plain,
( ! [X0] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ v7_waybel_1(X0,sK111)
| ~ m2_relset_1(X0,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ v2_lattice3(sK111)
| k2_waybel_1(sK111,sK111,X0) = k1_waybel34(k2_yellow_2(sK111,sK111,X0),sK111,k3_waybel_1(sK111,sK111,X0))
| ~ l1_orders_2(sK111) )
| ~ spl328_139
| ~ spl328_141
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144 ),
inference(forward_subsumption_resolution,[],[f24657,f24122]) ).
fof(f24659,plain,
( ! [X0] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ v7_waybel_1(X0,sK111)
| ~ m2_relset_1(X0,u1_struct_0(sK111),u1_struct_0(sK111))
| k2_waybel_1(sK111,sK111,X0) = k1_waybel34(k2_yellow_2(sK111,sK111,X0),sK111,k3_waybel_1(sK111,sK111,X0))
| ~ l1_orders_2(sK111) )
| ~ spl328_139
| ~ spl328_140
| ~ spl328_141
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144 ),
inference(forward_subsumption_resolution,[],[f24658,f24117]) ).
fof(f24660,plain,
( ! [X0] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ v7_waybel_1(X0,sK111)
| ~ m2_relset_1(X0,u1_struct_0(sK111),u1_struct_0(sK111))
| k2_waybel_1(sK111,sK111,X0) = k1_waybel34(k2_yellow_2(sK111,sK111,X0),sK111,k3_waybel_1(sK111,sK111,X0)) )
| ~ spl328_137
| ~ spl328_139
| ~ spl328_140
| ~ spl328_141
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144 ),
inference(forward_subsumption_resolution,[],[f24659,f24102]) ).
fof(f24661,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF327,sF327)
| ~ v1_funct_1(X0)
| ~ v7_waybel_1(X0,sK111)
| ~ m2_relset_1(X0,u1_struct_0(sK111),u1_struct_0(sK111))
| k2_waybel_1(sK111,sK111,X0) = k1_waybel34(k2_yellow_2(sK111,sK111,X0),sK111,k3_waybel_1(sK111,sK111,X0)) )
| ~ spl328_137
| ~ spl328_139
| ~ spl328_140
| ~ spl328_141
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144
| ~ spl328_153 ),
inference(forward_demodulation,[],[f24660,f24191]) ).
fof(f24662,plain,
( ! [X0] :
( ~ v7_waybel_1(X0,sK111)
| ~ v1_funct_2(X0,sF327,sF327)
| ~ v1_funct_1(X0)
| ~ m2_relset_1(X0,sF327,sF327)
| k2_waybel_1(sK111,sK111,X0) = k1_waybel34(k2_yellow_2(sK111,sK111,X0),sK111,k3_waybel_1(sK111,sK111,X0)) )
| ~ spl328_137
| ~ spl328_139
| ~ spl328_140
| ~ spl328_141
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144
| ~ spl328_153 ),
inference(forward_demodulation,[],[f24661,f24191]) ).
fof(f24663,plain,
( k2_waybel_1(sK111,sK111,sK112) = k1_waybel34(k2_yellow_2(sK111,sK111,sK112),sK111,k3_waybel_1(sK111,sK111,sK112))
| ~ spl328_137
| ~ spl328_139
| ~ spl328_140
| ~ spl328_141
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144
| ~ spl328_145
| ~ spl328_146
| ~ spl328_147
| ~ spl328_148
| ~ spl328_153 ),
inference(unit_resulting_resolution,[],[f24662,f24157,f24147,f24142,f24152]) ).
fof(f24666,plain,
( k2_waybel_1(sK111,sK111,sK112) = k1_waybel34(k2_yellow_2(sK111,sK111,sK112),sK111,k7_grcat_1(sF325))
| ~ spl328_137
| ~ spl328_139
| ~ spl328_140
| ~ spl328_141
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144
| ~ spl328_145
| ~ spl328_146
| ~ spl328_147
| ~ spl328_148
| ~ spl328_153
| ~ spl328_162 ),
inference(forward_demodulation,[],[f24663,f24453]) ).
fof(f24668,plain,
( k2_waybel_1(sK111,sK111,sK112) = k1_waybel34(sF325,sK111,k7_grcat_1(sF325))
| ~ spl328_137
| ~ spl328_139
| ~ spl328_140
| ~ spl328_141
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144
| ~ spl328_145
| ~ spl328_146
| ~ spl328_147
| ~ spl328_148
| ~ spl328_151
| ~ spl328_153
| ~ spl328_162 ),
inference(forward_demodulation,[],[f24666,f24181]) ).
fof(f24670,plain,
( sF326 = k1_waybel34(sF325,sK111,k7_grcat_1(sF325))
| ~ spl328_137
| ~ spl328_139
| ~ spl328_140
| ~ spl328_141
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144
| ~ spl328_145
| ~ spl328_146
| ~ spl328_147
| ~ spl328_148
| ~ spl328_151
| ~ spl328_152
| ~ spl328_153
| ~ spl328_162 ),
inference(forward_demodulation,[],[f24668,f24186]) ).
fof(f24672,plain,
( sK112 = k1_waybel34(sF325,sK111,k7_grcat_1(sF325))
| ~ spl328_137
| ~ spl328_139
| ~ spl328_140
| ~ spl328_141
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144
| ~ spl328_145
| ~ spl328_146
| ~ spl328_147
| ~ spl328_148
| ~ spl328_151
| ~ spl328_152
| ~ spl328_153
| ~ spl328_162
| ~ spl328_164 ),
inference(forward_demodulation,[],[f24670,f24480]) ).
fof(f24675,definition,
( spl328_184
<=> sK112 = k1_waybel34(sF325,sK111,k7_grcat_1(sF325)) ),
introduced(definition,[new_symbols(definition,[spl328_184])],[avatar_definition]) ).
fof(f24677,plain,
( sK112 = k1_waybel34(sF325,sK111,k7_grcat_1(sF325))
| ~ spl328_184 ),
inference(avatar_component_clause,[],[f24675]) ).
fof(f24678,plain,
( spl328_184
| ~ spl328_137
| ~ spl328_139
| ~ spl328_140
| ~ spl328_141
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144
| ~ spl328_145
| ~ spl328_146
| ~ spl328_147
| ~ spl328_148
| ~ spl328_151
| ~ spl328_152
| ~ spl328_153
| ~ spl328_162
| ~ spl328_164 ),
inference(avatar_split_clause,[],[f24672,f24478,f24451,f24189,f24184,f24179,f24155,f24150,f24145,f24140,f24135,f24130,f24125,f24120,f24115,f24110,f24100,f24675]) ).
fof(f24815,plain,
( ! [X0] :
( ~ v6_waybel_1(X0,sK111)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ m2_relset_1(X0,u1_struct_0(sK111),u1_struct_0(sK111))
| v3_struct_0(sK111)
| ~ v2_orders_2(sK111)
| ~ v3_orders_2(sK111)
| ~ v4_orders_2(sK111)
| v3_lattice3(k2_yellow_2(sK111,sK111,X0))
| ~ l1_orders_2(sK111) )
| ~ spl328_139 ),
inference(resolution,[],[f23028,f24112]) ).
fof(f24816,plain,
( ! [X0] :
( ~ v6_waybel_1(X0,sK111)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ m2_relset_1(X0,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ v2_orders_2(sK111)
| ~ v3_orders_2(sK111)
| ~ v4_orders_2(sK111)
| v3_lattice3(k2_yellow_2(sK111,sK111,X0))
| ~ l1_orders_2(sK111) )
| ~ spl328_139
| spl328_156 ),
inference(forward_subsumption_resolution,[],[f24815,f24276]) ).
fof(f24817,plain,
( ! [X0] :
( ~ v6_waybel_1(X0,sK111)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ m2_relset_1(X0,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ v3_orders_2(sK111)
| ~ v4_orders_2(sK111)
| v3_lattice3(k2_yellow_2(sK111,sK111,X0))
| ~ l1_orders_2(sK111) )
| ~ spl328_139
| ~ spl328_144
| spl328_156 ),
inference(forward_subsumption_resolution,[],[f24816,f24137]) ).
fof(f24818,plain,
( ! [X0] :
( ~ v6_waybel_1(X0,sK111)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ m2_relset_1(X0,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ v4_orders_2(sK111)
| v3_lattice3(k2_yellow_2(sK111,sK111,X0))
| ~ l1_orders_2(sK111) )
| ~ spl328_139
| ~ spl328_143
| ~ spl328_144
| spl328_156 ),
inference(forward_subsumption_resolution,[],[f24817,f24132]) ).
fof(f24819,plain,
( ! [X0] :
( ~ v6_waybel_1(X0,sK111)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ m2_relset_1(X0,u1_struct_0(sK111),u1_struct_0(sK111))
| v3_lattice3(k2_yellow_2(sK111,sK111,X0))
| ~ l1_orders_2(sK111) )
| ~ spl328_139
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144
| spl328_156 ),
inference(forward_subsumption_resolution,[],[f24818,f24127]) ).
fof(f24820,plain,
( ! [X0] :
( ~ v6_waybel_1(X0,sK111)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ m2_relset_1(X0,u1_struct_0(sK111),u1_struct_0(sK111))
| v3_lattice3(k2_yellow_2(sK111,sK111,X0)) )
| ~ spl328_137
| ~ spl328_139
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144
| spl328_156 ),
inference(forward_subsumption_resolution,[],[f24819,f24102]) ).
fof(f24821,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF327,sF327)
| ~ v6_waybel_1(X0,sK111)
| ~ v1_funct_1(X0)
| ~ m2_relset_1(X0,u1_struct_0(sK111),u1_struct_0(sK111))
| v3_lattice3(k2_yellow_2(sK111,sK111,X0)) )
| ~ spl328_137
| ~ spl328_139
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144
| ~ spl328_153
| spl328_156 ),
inference(forward_demodulation,[],[f24820,f24191]) ).
fof(f24822,plain,
( ! [X0] :
( ~ v6_waybel_1(X0,sK111)
| ~ v1_funct_2(X0,sF327,sF327)
| ~ m2_relset_1(X0,sF327,sF327)
| ~ v1_funct_1(X0)
| v3_lattice3(k2_yellow_2(sK111,sK111,X0)) )
| ~ spl328_137
| ~ spl328_139
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144
| ~ spl328_153
| spl328_156 ),
inference(forward_demodulation,[],[f24821,f24191]) ).
fof(f24823,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF327,sF327)
| ~ m2_relset_1(X0,sF327,sF327)
| ~ v1_funct_1(X0)
| v3_lattice3(k2_yellow_2(sK111,sK111,X0))
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ v7_waybel_1(X0,sK111)
| ~ m1_relset_1(X0,u1_struct_0(sK111),u1_struct_0(sK111))
| v3_struct_0(sK111)
| ~ l1_orders_2(sK111) )
| ~ spl328_137
| ~ spl328_139
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144
| ~ spl328_153
| spl328_156 ),
inference(resolution,[],[f24822,f23068]) ).
fof(f24824,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF327,sF327)
| ~ m2_relset_1(X0,sF327,sF327)
| ~ v1_funct_1(X0)
| v3_lattice3(k2_yellow_2(sK111,sK111,X0))
| ~ v1_funct_2(X0,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ v7_waybel_1(X0,sK111)
| ~ m1_relset_1(X0,u1_struct_0(sK111),u1_struct_0(sK111))
| v3_struct_0(sK111)
| ~ l1_orders_2(sK111) )
| ~ spl328_137
| ~ spl328_139
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144
| ~ spl328_153
| spl328_156 ),
inference(duplicate_literal_removal,[],[f24823]) ).
fof(f24825,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF327,sF327)
| ~ m2_relset_1(X0,sF327,sF327)
| ~ v1_funct_1(X0)
| v3_lattice3(k2_yellow_2(sK111,sK111,X0))
| ~ v1_funct_2(X0,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ v7_waybel_1(X0,sK111)
| ~ m1_relset_1(X0,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ l1_orders_2(sK111) )
| ~ spl328_137
| ~ spl328_139
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144
| ~ spl328_153
| spl328_156 ),
inference(forward_subsumption_resolution,[],[f24824,f24276]) ).
fof(f24826,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF327,sF327)
| ~ m2_relset_1(X0,sF327,sF327)
| ~ v1_funct_1(X0)
| v3_lattice3(k2_yellow_2(sK111,sK111,X0))
| ~ v1_funct_2(X0,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ v7_waybel_1(X0,sK111)
| ~ m1_relset_1(X0,u1_struct_0(sK111),u1_struct_0(sK111)) )
| ~ spl328_137
| ~ spl328_139
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144
| ~ spl328_153
| spl328_156 ),
inference(forward_subsumption_resolution,[],[f24825,f24102]) ).
fof(f24827,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF327,sF327)
| ~ v1_funct_2(X0,sF327,sF327)
| ~ m2_relset_1(X0,sF327,sF327)
| ~ v1_funct_1(X0)
| v3_lattice3(k2_yellow_2(sK111,sK111,X0))
| ~ v7_waybel_1(X0,sK111)
| ~ m1_relset_1(X0,u1_struct_0(sK111),u1_struct_0(sK111)) )
| ~ spl328_137
| ~ spl328_139
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144
| ~ spl328_153
| spl328_156 ),
inference(forward_demodulation,[],[f24826,f24191]) ).
fof(f24828,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF327,sF327)
| ~ m2_relset_1(X0,sF327,sF327)
| ~ v1_funct_1(X0)
| v3_lattice3(k2_yellow_2(sK111,sK111,X0))
| ~ v7_waybel_1(X0,sK111)
| ~ m1_relset_1(X0,u1_struct_0(sK111),u1_struct_0(sK111)) )
| ~ spl328_137
| ~ spl328_139
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144
| ~ spl328_153
| spl328_156 ),
inference(duplicate_literal_removal,[],[f24827]) ).
fof(f24829,plain,
( ! [X0] :
( ~ m1_relset_1(X0,sF327,sF327)
| ~ v1_funct_2(X0,sF327,sF327)
| ~ m2_relset_1(X0,sF327,sF327)
| ~ v1_funct_1(X0)
| v3_lattice3(k2_yellow_2(sK111,sK111,X0))
| ~ v7_waybel_1(X0,sK111) )
| ~ spl328_137
| ~ spl328_139
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144
| ~ spl328_153
| spl328_156 ),
inference(forward_demodulation,[],[f24828,f24191]) ).
fof(f24830,plain,
( ! [X0] :
( ~ v7_waybel_1(X0,sK111)
| ~ v1_funct_2(X0,sF327,sF327)
| ~ v1_funct_1(X0)
| v3_lattice3(k2_yellow_2(sK111,sK111,X0))
| ~ m1_relset_1(X0,sF327,sF327) )
| ~ spl328_137
| ~ spl328_139
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144
| ~ spl328_153
| spl328_156 ),
inference(forward_subsumption_resolution,[],[f24829,f21334]) ).
fof(f24960,plain,
( ! [X0,X1] :
( ~ v1_waybel34(k1_waybel34(X0,sK111,X1),sK111,X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(sK111))
| ~ v17_waybel_0(X1,X0,sK111)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(sK111))
| ~ v2_orders_2(sK111)
| ~ v3_orders_2(sK111)
| ~ v4_orders_2(sK111)
| ~ v1_lattice3(sK111)
| ~ v2_lattice3(sK111)
| ~ v3_lattice3(sK111)
| v22_waybel_0(X1,X0,sK111)
| ~ l1_orders_2(sK111)
| ~ 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) )
| ~ spl328_138 ),
inference(resolution,[],[f21211,f24107]) ).
fof(f24961,plain,
( ! [X0,X1] :
( ~ v1_waybel34(k1_waybel34(X0,sK111,X1),sK111,X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(sK111))
| ~ v17_waybel_0(X1,X0,sK111)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(sK111))
| ~ v3_orders_2(sK111)
| ~ v4_orders_2(sK111)
| ~ v1_lattice3(sK111)
| ~ v2_lattice3(sK111)
| ~ v3_lattice3(sK111)
| v22_waybel_0(X1,X0,sK111)
| ~ l1_orders_2(sK111)
| ~ 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) )
| ~ spl328_138
| ~ spl328_144 ),
inference(forward_subsumption_resolution,[],[f24960,f24137]) ).
fof(f24962,plain,
( ! [X0,X1] :
( ~ v1_waybel34(k1_waybel34(X0,sK111,X1),sK111,X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(sK111))
| ~ v17_waybel_0(X1,X0,sK111)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(sK111))
| ~ v4_orders_2(sK111)
| ~ v1_lattice3(sK111)
| ~ v2_lattice3(sK111)
| ~ v3_lattice3(sK111)
| v22_waybel_0(X1,X0,sK111)
| ~ l1_orders_2(sK111)
| ~ 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) )
| ~ spl328_138
| ~ spl328_143
| ~ spl328_144 ),
inference(forward_subsumption_resolution,[],[f24961,f24132]) ).
fof(f24963,plain,
( ! [X0,X1] :
( ~ v1_waybel34(k1_waybel34(X0,sK111,X1),sK111,X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(sK111))
| ~ v17_waybel_0(X1,X0,sK111)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(sK111))
| ~ v1_lattice3(sK111)
| ~ v2_lattice3(sK111)
| ~ v3_lattice3(sK111)
| v22_waybel_0(X1,X0,sK111)
| ~ l1_orders_2(sK111)
| ~ 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) )
| ~ spl328_138
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144 ),
inference(forward_subsumption_resolution,[],[f24962,f24127]) ).
fof(f24964,plain,
( ! [X0,X1] :
( ~ v1_waybel34(k1_waybel34(X0,sK111,X1),sK111,X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(sK111))
| ~ v17_waybel_0(X1,X0,sK111)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(sK111))
| ~ v2_lattice3(sK111)
| ~ v3_lattice3(sK111)
| v22_waybel_0(X1,X0,sK111)
| ~ l1_orders_2(sK111)
| ~ 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) )
| ~ spl328_138
| ~ spl328_141
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144 ),
inference(forward_subsumption_resolution,[],[f24963,f24122]) ).
fof(f24965,plain,
( ! [X0,X1] :
( ~ v1_waybel34(k1_waybel34(X0,sK111,X1),sK111,X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(sK111))
| ~ v17_waybel_0(X1,X0,sK111)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(sK111))
| ~ v3_lattice3(sK111)
| v22_waybel_0(X1,X0,sK111)
| ~ l1_orders_2(sK111)
| ~ 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) )
| ~ spl328_138
| ~ spl328_140
| ~ spl328_141
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144 ),
inference(forward_subsumption_resolution,[],[f24964,f24117]) ).
fof(f24966,plain,
( ! [X0,X1] :
( ~ v1_waybel34(k1_waybel34(X0,sK111,X1),sK111,X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(sK111))
| ~ v17_waybel_0(X1,X0,sK111)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(sK111))
| v22_waybel_0(X1,X0,sK111)
| ~ l1_orders_2(sK111)
| ~ 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) )
| ~ spl328_138
| ~ spl328_139
| ~ spl328_140
| ~ spl328_141
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144 ),
inference(forward_subsumption_resolution,[],[f24965,f24112]) ).
fof(f24967,plain,
( ! [X0,X1] :
( ~ v1_waybel34(k1_waybel34(X0,sK111,X1),sK111,X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(sK111))
| ~ v17_waybel_0(X1,X0,sK111)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(sK111))
| v22_waybel_0(X1,X0,sK111)
| ~ 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) )
| ~ spl328_137
| ~ spl328_138
| ~ spl328_139
| ~ spl328_140
| ~ spl328_141
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144 ),
inference(forward_subsumption_resolution,[],[f24966,f24102]) ).
fof(f24968,plain,
( ! [X0,X1] :
( ~ v1_funct_2(X1,u1_struct_0(X0),sF327)
| ~ v1_waybel34(k1_waybel34(X0,sK111,X1),sK111,X0)
| ~ v1_funct_1(X1)
| ~ v17_waybel_0(X1,X0,sK111)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(sK111))
| v22_waybel_0(X1,X0,sK111)
| ~ 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) )
| ~ spl328_137
| ~ spl328_138
| ~ spl328_139
| ~ spl328_140
| ~ spl328_141
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144
| ~ spl328_153 ),
inference(forward_demodulation,[],[f24967,f24191]) ).
fof(f24969,plain,
( ! [X0,X1] :
( ~ v3_lattice3(X0)
| ~ v1_funct_2(X1,u1_struct_0(X0),sF327)
| ~ v1_waybel34(k1_waybel34(X0,sK111,X1),sK111,X0)
| ~ v1_funct_1(X1)
| ~ v17_waybel_0(X1,X0,sK111)
| v22_waybel_0(X1,X0,sK111)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ m2_relset_1(X1,u1_struct_0(X0),sF327)
| ~ l1_orders_2(X0) )
| ~ spl328_137
| ~ spl328_138
| ~ spl328_139
| ~ spl328_140
| ~ spl328_141
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144
| ~ spl328_153 ),
inference(forward_demodulation,[],[f24968,f24191]) ).
fof(f25027,plain,
( v3_lattice3(k2_yellow_2(sK111,sK111,sK112))
| ~ spl328_137
| ~ spl328_139
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144
| ~ spl328_146
| ~ spl328_147
| ~ spl328_148
| ~ spl328_153
| ~ spl328_155
| spl328_156 ),
inference(unit_resulting_resolution,[],[f24830,f24157,f24147,f24267,f24152]) ).
fof(f25030,plain,
( v3_lattice3(sF325)
| ~ spl328_137
| ~ spl328_139
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144
| ~ spl328_146
| ~ spl328_147
| ~ spl328_148
| ~ spl328_151
| ~ spl328_153
| ~ spl328_155
| spl328_156 ),
inference(forward_demodulation,[],[f25027,f24181]) ).
fof(f25033,definition,
( spl328_200
<=> v3_lattice3(sF325) ),
introduced(definition,[new_symbols(definition,[spl328_200])],[avatar_definition]) ).
fof(f25035,plain,
( v3_lattice3(sF325)
| ~ spl328_200 ),
inference(avatar_component_clause,[],[f25033]) ).
fof(f25036,plain,
( spl328_200
| ~ spl328_137
| ~ spl328_139
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144
| ~ spl328_146
| ~ spl328_147
| ~ spl328_148
| ~ spl328_151
| ~ spl328_153
| ~ spl328_155
| spl328_156 ),
inference(avatar_split_clause,[],[f25030,f24274,f24265,f24189,f24179,f24155,f24150,f24145,f24135,f24130,f24125,f24110,f24100,f25033]) ).
fof(f25064,plain,
( ~ m1_yellow_0(sF325,sK111)
| ~ spl328_137
| spl328_168 ),
inference(unit_resulting_resolution,[],[f23185,f24102,f24550]) ).
fof(f25066,definition,
( spl328_201
<=> m1_yellow_0(sF325,sK111) ),
introduced(definition,[new_symbols(definition,[spl328_201])],[avatar_definition]) ).
fof(f25068,plain,
( ~ m1_yellow_0(sF325,sK111)
| spl328_201 ),
inference(avatar_component_clause,[],[f25066]) ).
fof(f25069,plain,
( ~ spl328_201
| ~ spl328_137
| spl328_168 ),
inference(avatar_split_clause,[],[f25064,f24548,f24100,f25066]) ).
fof(f25094,plain,
( v2_orders_2(sF325)
| ~ sP19(sK112,sK111)
| ~ spl328_151 ),
inference(superposition,[],[f21254,f24181]) ).
fof(f25096,definition,
( spl328_203
<=> sP19(sK112,sK111) ),
introduced(definition,[new_symbols(definition,[spl328_203])],[avatar_definition]) ).
fof(f25097,plain,
( sP19(sK112,sK111)
| ~ spl328_203 ),
inference(avatar_component_clause,[],[f25096]) ).
fof(f25098,plain,
( ~ sP19(sK112,sK111)
| spl328_203 ),
inference(avatar_component_clause,[],[f25096]) ).
fof(f25100,definition,
( spl328_204
<=> v2_orders_2(sF325) ),
introduced(definition,[new_symbols(definition,[spl328_204])],[avatar_definition]) ).
fof(f25102,plain,
( v2_orders_2(sF325)
| ~ spl328_204 ),
inference(avatar_component_clause,[],[f25100]) ).
fof(f25103,plain,
( ~ spl328_203
| spl328_204
| ~ spl328_151 ),
inference(avatar_split_clause,[],[f25094,f24179,f25100,f25096]) ).
fof(f25104,plain,
( ~ v2_orders_2(sK111)
| ~ v3_orders_2(sK111)
| ~ v4_orders_2(sK111)
| ~ v1_lattice3(sK111)
| ~ v2_lattice3(sK111)
| ~ v3_lattice3(sK111)
| ~ l1_orders_2(sK111)
| ~ v1_funct_1(sK112)
| ~ v1_funct_2(sK112,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ v6_waybel_1(sK112,sK111)
| ~ m1_relset_1(sK112,u1_struct_0(sK111),u1_struct_0(sK111))
| spl328_203 ),
inference(resolution,[],[f25098,f21257]) ).
fof(f25105,plain,
( ~ v3_orders_2(sK111)
| ~ v4_orders_2(sK111)
| ~ v1_lattice3(sK111)
| ~ v2_lattice3(sK111)
| ~ v3_lattice3(sK111)
| ~ l1_orders_2(sK111)
| ~ v1_funct_1(sK112)
| ~ v1_funct_2(sK112,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ v6_waybel_1(sK112,sK111)
| ~ m1_relset_1(sK112,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ spl328_144
| spl328_203 ),
inference(forward_subsumption_resolution,[],[f25104,f24137]) ).
fof(f25106,plain,
( ~ v4_orders_2(sK111)
| ~ v1_lattice3(sK111)
| ~ v2_lattice3(sK111)
| ~ v3_lattice3(sK111)
| ~ l1_orders_2(sK111)
| ~ v1_funct_1(sK112)
| ~ v1_funct_2(sK112,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ v6_waybel_1(sK112,sK111)
| ~ m1_relset_1(sK112,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ spl328_143
| ~ spl328_144
| spl328_203 ),
inference(forward_subsumption_resolution,[],[f25105,f24132]) ).
fof(f25107,plain,
( ~ v1_lattice3(sK111)
| ~ v2_lattice3(sK111)
| ~ v3_lattice3(sK111)
| ~ l1_orders_2(sK111)
| ~ v1_funct_1(sK112)
| ~ v1_funct_2(sK112,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ v6_waybel_1(sK112,sK111)
| ~ m1_relset_1(sK112,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144
| spl328_203 ),
inference(forward_subsumption_resolution,[],[f25106,f24127]) ).
fof(f25108,plain,
( ~ v2_lattice3(sK111)
| ~ v3_lattice3(sK111)
| ~ l1_orders_2(sK111)
| ~ v1_funct_1(sK112)
| ~ v1_funct_2(sK112,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ v6_waybel_1(sK112,sK111)
| ~ m1_relset_1(sK112,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ spl328_141
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144
| spl328_203 ),
inference(forward_subsumption_resolution,[],[f25107,f24122]) ).
fof(f25109,plain,
( ~ v3_lattice3(sK111)
| ~ l1_orders_2(sK111)
| ~ v1_funct_1(sK112)
| ~ v1_funct_2(sK112,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ v6_waybel_1(sK112,sK111)
| ~ m1_relset_1(sK112,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ spl328_140
| ~ spl328_141
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144
| spl328_203 ),
inference(forward_subsumption_resolution,[],[f25108,f24117]) ).
fof(f25110,plain,
( ~ l1_orders_2(sK111)
| ~ v1_funct_1(sK112)
| ~ v1_funct_2(sK112,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ v6_waybel_1(sK112,sK111)
| ~ m1_relset_1(sK112,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ spl328_139
| ~ spl328_140
| ~ spl328_141
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144
| spl328_203 ),
inference(forward_subsumption_resolution,[],[f25109,f24112]) ).
fof(f25111,plain,
( ~ v1_funct_1(sK112)
| ~ v1_funct_2(sK112,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ v6_waybel_1(sK112,sK111)
| ~ m1_relset_1(sK112,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ spl328_137
| ~ spl328_139
| ~ spl328_140
| ~ spl328_141
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144
| spl328_203 ),
inference(forward_subsumption_resolution,[],[f25110,f24102]) ).
fof(f25112,plain,
( ~ v1_funct_2(sK112,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ v6_waybel_1(sK112,sK111)
| ~ m1_relset_1(sK112,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ spl328_137
| ~ spl328_139
| ~ spl328_140
| ~ spl328_141
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144
| ~ spl328_148
| spl328_203 ),
inference(forward_subsumption_resolution,[],[f25111,f24157]) ).
fof(f25113,plain,
( ~ v1_funct_2(sK112,sF327,sF327)
| ~ v6_waybel_1(sK112,sK111)
| ~ m1_relset_1(sK112,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ spl328_137
| ~ spl328_139
| ~ spl328_140
| ~ spl328_141
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144
| ~ spl328_148
| ~ spl328_153
| spl328_203 ),
inference(forward_demodulation,[],[f25112,f24191]) ).
fof(f25114,plain,
( ~ v6_waybel_1(sK112,sK111)
| ~ m1_relset_1(sK112,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ spl328_137
| ~ spl328_139
| ~ spl328_140
| ~ spl328_141
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144
| ~ spl328_147
| ~ spl328_148
| ~ spl328_153
| spl328_203 ),
inference(forward_subsumption_resolution,[],[f25113,f24152]) ).
fof(f25115,plain,
( ~ m1_relset_1(sK112,sF327,sF327)
| ~ v6_waybel_1(sK112,sK111)
| ~ spl328_137
| ~ spl328_139
| ~ spl328_140
| ~ spl328_141
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144
| ~ spl328_147
| ~ spl328_148
| ~ spl328_153
| spl328_203 ),
inference(forward_demodulation,[],[f25114,f24191]) ).
fof(f25116,plain,
( ~ v6_waybel_1(sK112,sK111)
| ~ spl328_137
| ~ spl328_139
| ~ spl328_140
| ~ spl328_141
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144
| ~ spl328_147
| ~ spl328_148
| ~ spl328_153
| ~ spl328_155
| spl328_203 ),
inference(forward_subsumption_resolution,[],[f25115,f24267]) ).
fof(f25118,definition,
( spl328_205
<=> v6_waybel_1(sK112,sK111) ),
introduced(definition,[new_symbols(definition,[spl328_205])],[avatar_definition]) ).
fof(f25120,plain,
( ~ v6_waybel_1(sK112,sK111)
| spl328_205 ),
inference(avatar_component_clause,[],[f25118]) ).
fof(f25121,plain,
( ~ spl328_205
| ~ spl328_137
| ~ spl328_139
| ~ spl328_140
| ~ spl328_141
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144
| ~ spl328_147
| ~ spl328_148
| ~ spl328_153
| ~ spl328_155
| spl328_203 ),
inference(avatar_split_clause,[],[f25116,f25096,f24265,f24189,f24155,f24150,f24135,f24130,f24125,f24120,f24115,f24110,f24100,f25118]) ).
fof(f25122,plain,
( ~ v1_funct_1(sK112)
| ~ v1_funct_2(sK112,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ v7_waybel_1(sK112,sK111)
| ~ m1_relset_1(sK112,u1_struct_0(sK111),u1_struct_0(sK111))
| v3_struct_0(sK111)
| ~ l1_orders_2(sK111)
| spl328_205 ),
inference(resolution,[],[f25120,f23068]) ).
fof(f25123,plain,
( ~ v1_funct_2(sK112,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ v7_waybel_1(sK112,sK111)
| ~ m1_relset_1(sK112,u1_struct_0(sK111),u1_struct_0(sK111))
| v3_struct_0(sK111)
| ~ l1_orders_2(sK111)
| ~ spl328_148
| spl328_205 ),
inference(forward_subsumption_resolution,[],[f25122,f24157]) ).
fof(f25124,plain,
( ~ v1_funct_2(sK112,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ m1_relset_1(sK112,u1_struct_0(sK111),u1_struct_0(sK111))
| v3_struct_0(sK111)
| ~ l1_orders_2(sK111)
| ~ spl328_146
| ~ spl328_148
| spl328_205 ),
inference(forward_subsumption_resolution,[],[f25123,f24147]) ).
fof(f25125,plain,
( ~ v1_funct_2(sK112,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ m1_relset_1(sK112,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ l1_orders_2(sK111)
| ~ spl328_146
| ~ spl328_148
| spl328_156
| spl328_205 ),
inference(forward_subsumption_resolution,[],[f25124,f24276]) ).
fof(f25126,plain,
( ~ v1_funct_2(sK112,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ m1_relset_1(sK112,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ spl328_137
| ~ spl328_146
| ~ spl328_148
| spl328_156
| spl328_205 ),
inference(forward_subsumption_resolution,[],[f25125,f24102]) ).
fof(f25127,plain,
( ~ v1_funct_2(sK112,sF327,sF327)
| ~ m1_relset_1(sK112,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ spl328_137
| ~ spl328_146
| ~ spl328_148
| ~ spl328_153
| spl328_156
| spl328_205 ),
inference(forward_demodulation,[],[f25126,f24191]) ).
fof(f25128,plain,
( ~ m1_relset_1(sK112,u1_struct_0(sK111),u1_struct_0(sK111))
| ~ spl328_137
| ~ spl328_146
| ~ spl328_147
| ~ spl328_148
| ~ spl328_153
| spl328_156
| spl328_205 ),
inference(forward_subsumption_resolution,[],[f25127,f24152]) ).
fof(f25129,plain,
( ~ m1_relset_1(sK112,sF327,sF327)
| ~ spl328_137
| ~ spl328_146
| ~ spl328_147
| ~ spl328_148
| ~ spl328_153
| spl328_156
| spl328_205 ),
inference(forward_demodulation,[],[f25128,f24191]) ).
fof(f25130,plain,
( $false
| ~ spl328_137
| ~ spl328_146
| ~ spl328_147
| ~ spl328_148
| ~ spl328_153
| ~ spl328_155
| spl328_156
| spl328_205 ),
inference(forward_subsumption_resolution,[],[f25129,f24267]) ).
fof(f25131,plain,
( ~ spl328_137
| ~ spl328_146
| ~ spl328_147
| ~ spl328_148
| ~ spl328_153
| ~ spl328_155
| spl328_156
| spl328_205 ),
inference(avatar_contradiction_clause,[],[f25130]) ).
fof(f25149,plain,
( v4_orders_2(k2_yellow_2(sK111,sK111,sK112))
| ~ spl328_203 ),
inference(resolution,[],[f25097,f21252]) ).
fof(f25152,plain,
( v4_orders_2(sF325)
| ~ spl328_151
| ~ spl328_203 ),
inference(forward_demodulation,[],[f25149,f24181]) ).
fof(f25157,definition,
( spl328_206
<=> v4_orders_2(sF325) ),
introduced(definition,[new_symbols(definition,[spl328_206])],[avatar_definition]) ).
fof(f25159,plain,
( v4_orders_2(sF325)
| ~ spl328_206 ),
inference(avatar_component_clause,[],[f25157]) ).
fof(f25160,plain,
( spl328_206
| ~ spl328_151
| ~ spl328_203 ),
inference(avatar_split_clause,[],[f25152,f25096,f24179,f25157]) ).
fof(f25211,plain,
( v3_orders_2(sF325)
| ~ sP19(sK112,sK111)
| ~ spl328_151 ),
inference(superposition,[],[f21253,f24181]) ).
fof(f25212,plain,
( v3_orders_2(sF325)
| ~ spl328_151
| ~ spl328_203 ),
inference(forward_subsumption_resolution,[],[f25211,f25097]) ).
fof(f25216,definition,
( spl328_208
<=> v3_orders_2(sF325) ),
introduced(definition,[new_symbols(definition,[spl328_208])],[avatar_definition]) ).
fof(f25218,plain,
( v3_orders_2(sF325)
| ~ spl328_208 ),
inference(avatar_component_clause,[],[f25216]) ).
fof(f25219,plain,
( spl328_208
| ~ spl328_151
| ~ spl328_203 ),
inference(avatar_split_clause,[],[f25212,f25096,f24179,f25216]) ).
fof(f25242,plain,
( v1_lattice3(sF325)
| ~ sP19(sK112,sK111)
| ~ spl328_151 ),
inference(superposition,[],[f21245,f24181]) ).
fof(f25243,plain,
( v1_lattice3(sF325)
| ~ spl328_151
| ~ spl328_203 ),
inference(forward_subsumption_resolution,[],[f25242,f25097]) ).
fof(f25246,definition,
( spl328_210
<=> v1_lattice3(sF325) ),
introduced(definition,[new_symbols(definition,[spl328_210])],[avatar_definition]) ).
fof(f25248,plain,
( v1_lattice3(sF325)
| ~ spl328_210 ),
inference(avatar_component_clause,[],[f25246]) ).
fof(f25249,plain,
( spl328_210
| ~ spl328_151
| ~ spl328_203 ),
inference(avatar_split_clause,[],[f25243,f25096,f24179,f25246]) ).
fof(f25276,plain,
( v2_lattice3(k2_yellow_2(sK111,sK111,sK112))
| ~ spl328_203 ),
inference(resolution,[],[f21244,f25097]) ).
fof(f25277,plain,
( v2_lattice3(sF325)
| ~ spl328_151
| ~ spl328_203 ),
inference(forward_demodulation,[],[f25276,f24181]) ).
fof(f25280,definition,
( spl328_212
<=> v2_lattice3(sF325) ),
introduced(definition,[new_symbols(definition,[spl328_212])],[avatar_definition]) ).
fof(f25282,plain,
( v2_lattice3(sF325)
| ~ spl328_212 ),
inference(avatar_component_clause,[],[f25280]) ).
fof(f25283,plain,
( spl328_212
| ~ spl328_151
| ~ spl328_203 ),
inference(avatar_split_clause,[],[f25277,f25096,f24179,f25280]) ).
fof(f25478,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF327,u1_struct_0(sK111))
| m1_yellow_0(k2_yellow_2(sK111,sK111,X0),sK111)
| v3_struct_0(sK111)
| ~ m1_relset_1(X0,sF327,u1_struct_0(sK111))
| ~ v1_funct_1(X0) )
| ~ spl328_137
| ~ spl328_153
| spl328_156 ),
inference(resolution,[],[f24324,f24102]) ).
fof(f25479,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF327,u1_struct_0(sK111))
| m1_yellow_0(k2_yellow_2(sK111,sK111,X0),sK111)
| ~ m1_relset_1(X0,sF327,u1_struct_0(sK111))
| ~ v1_funct_1(X0) )
| ~ spl328_137
| ~ spl328_153
| spl328_156 ),
inference(forward_subsumption_resolution,[],[f25478,f24276]) ).
fof(f25480,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF327,sF327)
| m1_yellow_0(k2_yellow_2(sK111,sK111,X0),sK111)
| ~ m1_relset_1(X0,sF327,u1_struct_0(sK111))
| ~ v1_funct_1(X0) )
| ~ spl328_137
| ~ spl328_153
| spl328_156 ),
inference(forward_demodulation,[],[f25479,f24191]) ).
fof(f25481,plain,
( ! [X0] :
( m1_yellow_0(k2_yellow_2(sK111,sK111,X0),sK111)
| ~ v1_funct_2(X0,sF327,sF327)
| ~ m1_relset_1(X0,sF327,sF327)
| ~ v1_funct_1(X0) )
| ~ spl328_137
| ~ spl328_153
| spl328_156 ),
inference(forward_demodulation,[],[f25480,f24191]) ).
fof(f25484,plain,
( m1_yellow_0(sF325,sK111)
| ~ v1_funct_2(sK112,sF327,sF327)
| ~ m1_relset_1(sK112,sF327,sF327)
| ~ v1_funct_1(sK112)
| ~ spl328_137
| ~ spl328_151
| ~ spl328_153
| spl328_156 ),
inference(superposition,[],[f25481,f24181]) ).
fof(f25485,plain,
( ~ v1_funct_2(sK112,sF327,sF327)
| ~ m1_relset_1(sK112,sF327,sF327)
| ~ v1_funct_1(sK112)
| ~ spl328_137
| ~ spl328_151
| ~ spl328_153
| spl328_156
| spl328_201 ),
inference(forward_subsumption_resolution,[],[f25484,f25068]) ).
fof(f25488,plain,
( ~ m1_relset_1(sK112,sF327,sF327)
| ~ v1_funct_1(sK112)
| ~ spl328_137
| ~ spl328_147
| ~ spl328_151
| ~ spl328_153
| spl328_156
| spl328_201 ),
inference(forward_subsumption_resolution,[],[f25485,f24152]) ).
fof(f25491,plain,
( ~ v1_funct_1(sK112)
| ~ spl328_137
| ~ spl328_147
| ~ spl328_151
| ~ spl328_153
| ~ spl328_155
| spl328_156
| spl328_201 ),
inference(forward_subsumption_resolution,[],[f25488,f24267]) ).
fof(f25492,plain,
( $false
| ~ spl328_137
| ~ spl328_147
| ~ spl328_148
| ~ spl328_151
| ~ spl328_153
| ~ spl328_155
| spl328_156
| spl328_201 ),
inference(forward_subsumption_resolution,[],[f25491,f24157]) ).
fof(f25493,plain,
( ~ spl328_137
| ~ spl328_147
| ~ spl328_148
| ~ spl328_151
| ~ spl328_153
| ~ spl328_155
| spl328_156
| spl328_201 ),
inference(avatar_contradiction_clause,[],[f25492]) ).
fof(f25620,definition,
( spl328_238
<=> v1_funct_2(k7_grcat_1(sF325),u1_struct_0(sF325),sF327) ),
introduced(definition,[new_symbols(definition,[spl328_238])],[avatar_definition]) ).
fof(f25621,plain,
( v1_funct_2(k7_grcat_1(sF325),u1_struct_0(sF325),sF327)
| ~ spl328_238 ),
inference(avatar_component_clause,[],[f25620]) ).
fof(f25622,plain,
( ~ v1_funct_2(k7_grcat_1(sF325),u1_struct_0(sF325),sF327)
| spl328_238 ),
inference(avatar_component_clause,[],[f25620]) ).
fof(f25624,definition,
( spl328_239
<=> m2_relset_1(k7_grcat_1(sF325),u1_struct_0(sF325),sF327) ),
introduced(definition,[new_symbols(definition,[spl328_239])],[avatar_definition]) ).
fof(f25625,plain,
( m2_relset_1(k7_grcat_1(sF325),u1_struct_0(sF325),sF327)
| ~ spl328_239 ),
inference(avatar_component_clause,[],[f25624]) ).
fof(f25633,plain,
( v1_funct_1(k7_grcat_1(sF325))
| spl328_167
| ~ spl328_168 ),
inference(unit_resulting_resolution,[],[f22000,f24532,f24549]) ).
fof(f25711,definition,
( spl328_241
<=> v1_funct_1(k7_grcat_1(sF325)) ),
introduced(definition,[new_symbols(definition,[spl328_241])],[avatar_definition]) ).
fof(f25713,plain,
( v1_funct_1(k7_grcat_1(sF325))
| ~ spl328_241 ),
inference(avatar_component_clause,[],[f25711]) ).
fof(f25714,plain,
( spl328_241
| spl328_167
| ~ spl328_168 ),
inference(avatar_split_clause,[],[f25633,f24548,f24530,f25711]) ).
fof(f26395,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF327,u1_struct_0(sK111))
| m2_relset_1(k3_waybel_1(sK111,sK111,X0),u1_struct_0(k2_yellow_2(sK111,sK111,X0)),u1_struct_0(sK111))
| v3_struct_0(sK111)
| ~ m1_relset_1(X0,sF327,u1_struct_0(sK111))
| ~ v1_funct_1(X0) )
| ~ spl328_137
| ~ spl328_153
| spl328_156 ),
inference(resolution,[],[f24316,f24102]) ).
fof(f26398,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF327,u1_struct_0(sK111))
| m2_relset_1(k3_waybel_1(sK111,sK111,X0),u1_struct_0(k2_yellow_2(sK111,sK111,X0)),u1_struct_0(sK111))
| ~ m1_relset_1(X0,sF327,u1_struct_0(sK111))
| ~ v1_funct_1(X0) )
| ~ spl328_137
| ~ spl328_153
| spl328_156 ),
inference(forward_subsumption_resolution,[],[f26395,f24276]) ).
fof(f26404,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF327,sF327)
| m2_relset_1(k3_waybel_1(sK111,sK111,X0),u1_struct_0(k2_yellow_2(sK111,sK111,X0)),u1_struct_0(sK111))
| ~ m1_relset_1(X0,sF327,u1_struct_0(sK111))
| ~ v1_funct_1(X0) )
| ~ spl328_137
| ~ spl328_153
| spl328_156 ),
inference(forward_demodulation,[],[f26398,f24191]) ).
fof(f26405,plain,
( ! [X0] :
( m2_relset_1(k3_waybel_1(sK111,sK111,X0),u1_struct_0(k2_yellow_2(sK111,sK111,X0)),sF327)
| ~ v1_funct_2(X0,sF327,sF327)
| ~ m1_relset_1(X0,sF327,u1_struct_0(sK111))
| ~ v1_funct_1(X0) )
| ~ spl328_137
| ~ spl328_153
| spl328_156 ),
inference(forward_demodulation,[],[f26404,f24191]) ).
fof(f26406,plain,
( ! [X0] :
( m2_relset_1(k3_waybel_1(sK111,sK111,X0),u1_struct_0(k2_yellow_2(sK111,sK111,X0)),sF327)
| ~ m1_relset_1(X0,sF327,sF327)
| ~ v1_funct_2(X0,sF327,sF327)
| ~ v1_funct_1(X0) )
| ~ spl328_137
| ~ spl328_153
| spl328_156 ),
inference(forward_demodulation,[],[f26405,f24191]) ).
fof(f26407,plain,
( m2_relset_1(k3_waybel_1(sK111,sK111,sK112),u1_struct_0(k2_yellow_2(sK111,sK111,sK112)),sF327)
| ~ spl328_137
| ~ spl328_147
| ~ spl328_148
| ~ spl328_153
| ~ spl328_155
| spl328_156 ),
inference(unit_resulting_resolution,[],[f26406,f24157,f24152,f24267]) ).
fof(f26412,plain,
( m2_relset_1(k3_waybel_1(sK111,sK111,sK112),u1_struct_0(sF325),sF327)
| ~ spl328_137
| ~ spl328_147
| ~ spl328_148
| ~ spl328_151
| ~ spl328_153
| ~ spl328_155
| spl328_156 ),
inference(forward_demodulation,[],[f26407,f24181]) ).
fof(f26415,plain,
( m2_relset_1(k7_grcat_1(sF325),u1_struct_0(sF325),sF327)
| ~ spl328_137
| ~ spl328_147
| ~ spl328_148
| ~ spl328_151
| ~ spl328_153
| ~ spl328_155
| spl328_156
| ~ spl328_162 ),
inference(forward_demodulation,[],[f26412,f24453]) ).
fof(f26418,plain,
( spl328_239
| ~ spl328_137
| ~ spl328_147
| ~ spl328_148
| ~ spl328_151
| ~ spl328_153
| ~ spl328_155
| spl328_156
| ~ spl328_162 ),
inference(avatar_split_clause,[],[f26415,f24451,f24274,f24265,f24189,f24179,f24155,f24150,f24100,f25624]) ).
fof(f26450,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF327,u1_struct_0(sK111))
| v1_funct_2(k3_waybel_1(sK111,sK111,X0),u1_struct_0(k2_yellow_2(sK111,sK111,X0)),u1_struct_0(sK111))
| v3_struct_0(sK111)
| ~ m1_relset_1(X0,sF327,u1_struct_0(sK111))
| ~ v1_funct_1(X0) )
| ~ spl328_137
| ~ spl328_153
| spl328_156 ),
inference(resolution,[],[f24314,f24102]) ).
fof(f26453,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF327,u1_struct_0(sK111))
| v1_funct_2(k3_waybel_1(sK111,sK111,X0),u1_struct_0(k2_yellow_2(sK111,sK111,X0)),u1_struct_0(sK111))
| ~ m1_relset_1(X0,sF327,u1_struct_0(sK111))
| ~ v1_funct_1(X0) )
| ~ spl328_137
| ~ spl328_153
| spl328_156 ),
inference(forward_subsumption_resolution,[],[f26450,f24276]) ).
fof(f26459,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF327,sF327)
| v1_funct_2(k3_waybel_1(sK111,sK111,X0),u1_struct_0(k2_yellow_2(sK111,sK111,X0)),u1_struct_0(sK111))
| ~ m1_relset_1(X0,sF327,u1_struct_0(sK111))
| ~ v1_funct_1(X0) )
| ~ spl328_137
| ~ spl328_153
| spl328_156 ),
inference(forward_demodulation,[],[f26453,f24191]) ).
fof(f26460,plain,
( ! [X0] :
( v1_funct_2(k3_waybel_1(sK111,sK111,X0),u1_struct_0(k2_yellow_2(sK111,sK111,X0)),sF327)
| ~ v1_funct_2(X0,sF327,sF327)
| ~ m1_relset_1(X0,sF327,u1_struct_0(sK111))
| ~ v1_funct_1(X0) )
| ~ spl328_137
| ~ spl328_153
| spl328_156 ),
inference(forward_demodulation,[],[f26459,f24191]) ).
fof(f26461,plain,
( ! [X0] :
( v1_funct_2(k3_waybel_1(sK111,sK111,X0),u1_struct_0(k2_yellow_2(sK111,sK111,X0)),sF327)
| ~ m1_relset_1(X0,sF327,sF327)
| ~ v1_funct_2(X0,sF327,sF327)
| ~ v1_funct_1(X0) )
| ~ spl328_137
| ~ spl328_153
| spl328_156 ),
inference(forward_demodulation,[],[f26460,f24191]) ).
fof(f26463,plain,
( v1_funct_2(k7_grcat_1(sF325),u1_struct_0(k2_yellow_2(sK111,sK111,sK112)),sF327)
| ~ m1_relset_1(sK112,sF327,sF327)
| ~ v1_funct_2(sK112,sF327,sF327)
| ~ v1_funct_1(sK112)
| ~ spl328_137
| ~ spl328_153
| spl328_156
| ~ spl328_162 ),
inference(superposition,[],[f26461,f24453]) ).
fof(f26466,plain,
( v1_funct_2(k7_grcat_1(sF325),u1_struct_0(k2_yellow_2(sK111,sK111,sK112)),sF327)
| ~ v1_funct_2(sK112,sF327,sF327)
| ~ v1_funct_1(sK112)
| ~ spl328_137
| ~ spl328_153
| ~ spl328_155
| spl328_156
| ~ spl328_162 ),
inference(forward_subsumption_resolution,[],[f26463,f24267]) ).
fof(f26469,plain,
( v1_funct_2(k7_grcat_1(sF325),u1_struct_0(k2_yellow_2(sK111,sK111,sK112)),sF327)
| ~ v1_funct_1(sK112)
| ~ spl328_137
| ~ spl328_147
| ~ spl328_153
| ~ spl328_155
| spl328_156
| ~ spl328_162 ),
inference(forward_subsumption_resolution,[],[f26466,f24152]) ).
fof(f26472,plain,
( v1_funct_2(k7_grcat_1(sF325),u1_struct_0(k2_yellow_2(sK111,sK111,sK112)),sF327)
| ~ spl328_137
| ~ spl328_147
| ~ spl328_148
| ~ spl328_153
| ~ spl328_155
| spl328_156
| ~ spl328_162 ),
inference(forward_subsumption_resolution,[],[f26469,f24157]) ).
fof(f26476,plain,
( v1_funct_2(k7_grcat_1(sF325),u1_struct_0(sF325),sF327)
| ~ spl328_137
| ~ spl328_147
| ~ spl328_148
| ~ spl328_151
| ~ spl328_153
| ~ spl328_155
| spl328_156
| ~ spl328_162 ),
inference(forward_demodulation,[],[f26472,f24181]) ).
fof(f26479,plain,
( $false
| ~ spl328_137
| ~ spl328_147
| ~ spl328_148
| ~ spl328_151
| ~ spl328_153
| ~ spl328_155
| spl328_156
| ~ spl328_162
| spl328_238 ),
inference(forward_subsumption_resolution,[],[f26476,f25622]) ).
fof(f26480,plain,
( ~ spl328_137
| ~ spl328_147
| ~ spl328_148
| ~ spl328_151
| ~ spl328_153
| ~ spl328_155
| spl328_156
| ~ spl328_162
| spl328_238 ),
inference(avatar_contradiction_clause,[],[f26479]) ).
fof(f26487,plain,
( ~ v1_waybel34(k1_waybel34(sF325,sK111,k7_grcat_1(sF325)),sK111,sF325)
| ~ spl328_137
| ~ spl328_138
| ~ spl328_139
| ~ spl328_140
| ~ spl328_141
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144
| ~ spl328_153
| spl328_163
| ~ spl328_168
| ~ spl328_183
| ~ spl328_200
| ~ spl328_204
| ~ spl328_206
| ~ spl328_208
| ~ spl328_210
| ~ spl328_212
| ~ spl328_238
| ~ spl328_239
| ~ spl328_241 ),
inference(unit_resulting_resolution,[],[f24969,f24549,f25035,f25282,f25248,f25159,f25218,f25102,f25713,f24462,f24650,f25625,f25621]) ).
fof(f26522,plain,
( ~ v1_waybel34(sK112,sK111,sF325)
| ~ spl328_137
| ~ spl328_138
| ~ spl328_139
| ~ spl328_140
| ~ spl328_141
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144
| ~ spl328_153
| spl328_163
| ~ spl328_168
| ~ spl328_183
| ~ spl328_184
| ~ spl328_200
| ~ spl328_204
| ~ spl328_206
| ~ spl328_208
| ~ spl328_210
| ~ spl328_212
| ~ spl328_238
| ~ spl328_239
| ~ spl328_241 ),
inference(forward_demodulation,[],[f26487,f24677]) ).
fof(f26535,plain,
( $false
| ~ spl328_137
| ~ spl328_138
| ~ spl328_139
| ~ spl328_140
| ~ spl328_141
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144
| ~ spl328_153
| spl328_163
| ~ spl328_165
| ~ spl328_168
| ~ spl328_183
| ~ spl328_184
| ~ spl328_200
| ~ spl328_204
| ~ spl328_206
| ~ spl328_208
| ~ spl328_210
| ~ spl328_212
| ~ spl328_238
| ~ spl328_239
| ~ spl328_241 ),
inference(forward_subsumption_resolution,[],[f26522,f24487]) ).
fof(f26536,plain,
( ~ spl328_137
| ~ spl328_138
| ~ spl328_139
| ~ spl328_140
| ~ spl328_141
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144
| ~ spl328_153
| spl328_163
| ~ spl328_165
| ~ spl328_168
| ~ spl328_183
| ~ spl328_184
| ~ spl328_200
| ~ spl328_204
| ~ spl328_206
| ~ spl328_208
| ~ spl328_210
| ~ spl328_212
| ~ spl328_238
| ~ spl328_239
| ~ spl328_241 ),
inference(avatar_contradiction_clause,[],[f26535]) ).
cnf(s140,plain,
spl328_137,
inference(sat_conversion,[],[f24103]) ).
cnf(s141,plain,
spl328_138,
inference(sat_conversion,[],[f24108]) ).
cnf(s142,plain,
spl328_139,
inference(sat_conversion,[],[f24113]) ).
cnf(s143,plain,
spl328_140,
inference(sat_conversion,[],[f24118]) ).
cnf(s144,plain,
spl328_141,
inference(sat_conversion,[],[f24123]) ).
cnf(s145,plain,
spl328_142,
inference(sat_conversion,[],[f24128]) ).
cnf(s146,plain,
spl328_143,
inference(sat_conversion,[],[f24133]) ).
cnf(s147,plain,
spl328_144,
inference(sat_conversion,[],[f24138]) ).
cnf(s148,plain,
spl328_145,
inference(sat_conversion,[],[f24143]) ).
cnf(s149,plain,
spl328_146,
inference(sat_conversion,[],[f24148]) ).
cnf(s150,plain,
spl328_147,
inference(sat_conversion,[],[f24153]) ).
cnf(s151,plain,
spl328_148,
inference(sat_conversion,[],[f24158]) ).
cnf(s152,plain,
spl328_149,
inference(sat_conversion,[],[f24163]) ).
cnf(s153,plain,
~ spl328_150,
inference(sat_conversion,[],[f24168]) ).
cnf(s154,plain,
spl328_151,
inference(sat_conversion,[],[f24182]) ).
cnf(s155,plain,
spl328_152,
inference(sat_conversion,[],[f24187]) ).
cnf(s156,plain,
spl328_153,
inference(sat_conversion,[],[f24192]) ).
cnf(s157,plain,
( ~ spl328_137
| ~ spl328_139
| ~ spl328_140
| ~ spl328_141
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144
| ~ spl328_145
| ~ spl328_146
| ~ spl328_147
| ~ spl328_148
| spl328_150
| ~ spl328_151
| ~ spl328_153
| ~ spl328_154 ),
inference(sat_conversion,[],[f24244]) ).
cnf(s158,plain,
( ~ spl328_145
| spl328_155 ),
inference(sat_conversion,[],[f24268]) ).
cnf(s159,plain,
( ~ spl328_137
| ~ spl328_141
| ~ spl328_156 ),
inference(sat_conversion,[],[f24277]) ).
cnf(s161,plain,
( ~ spl328_137
| ~ spl328_145
| ~ spl328_147
| ~ spl328_148
| ~ spl328_153
| spl328_156
| spl328_157 ),
inference(sat_conversion,[],[f24340]) ).
cnf(s170,plain,
( ~ spl328_137
| ~ spl328_145
| ~ spl328_147
| ~ spl328_148
| ~ spl328_151
| ~ spl328_153
| spl328_156
| spl328_162 ),
inference(sat_conversion,[],[f24454]) ).
cnf(s172,plain,
( spl328_154
| ~ spl328_162
| ~ spl328_163 ),
inference(sat_conversion,[],[f24463]) ).
cnf(s174,plain,
( ~ spl328_152
| ~ spl328_157
| spl328_164 ),
inference(sat_conversion,[],[f24481]) ).
cnf(s176,plain,
( ~ spl328_149
| ~ spl328_164
| spl328_165 ),
inference(sat_conversion,[],[f24488]) ).
cnf(s178,plain,
( ~ spl328_137
| ~ spl328_147
| ~ spl328_148
| ~ spl328_151
| ~ spl328_153
| ~ spl328_155
| spl328_156
| ~ spl328_167 ),
inference(sat_conversion,[],[f24533]) ).
cnf(s195,plain,
( ~ spl328_137
| ~ spl328_139
| ~ spl328_140
| ~ spl328_141
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144
| ~ spl328_145
| ~ spl328_146
| ~ spl328_147
| ~ spl328_148
| ~ spl328_151
| ~ spl328_153
| ~ spl328_162
| spl328_183 ),
inference(sat_conversion,[],[f24651]) ).
cnf(s197,plain,
( ~ spl328_137
| ~ spl328_139
| ~ spl328_140
| ~ spl328_141
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144
| ~ spl328_145
| ~ spl328_146
| ~ spl328_147
| ~ spl328_148
| ~ spl328_151
| ~ spl328_152
| ~ spl328_153
| ~ spl328_162
| ~ spl328_164
| spl328_184 ),
inference(sat_conversion,[],[f24678]) ).
cnf(s218,plain,
( ~ spl328_137
| ~ spl328_139
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144
| ~ spl328_146
| ~ spl328_147
| ~ spl328_148
| ~ spl328_151
| ~ spl328_153
| ~ spl328_155
| spl328_156
| spl328_200 ),
inference(sat_conversion,[],[f25036]) ).
cnf(s220,plain,
( ~ spl328_137
| spl328_168
| ~ spl328_201 ),
inference(sat_conversion,[],[f25069]) ).
cnf(s222,plain,
( ~ spl328_151
| ~ spl328_203
| spl328_204 ),
inference(sat_conversion,[],[f25103]) ).
cnf(s223,plain,
( ~ spl328_137
| ~ spl328_139
| ~ spl328_140
| ~ spl328_141
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144
| ~ spl328_147
| ~ spl328_148
| ~ spl328_153
| ~ spl328_155
| spl328_203
| ~ spl328_205 ),
inference(sat_conversion,[],[f25121]) ).
cnf(s224,plain,
( ~ spl328_137
| ~ spl328_146
| ~ spl328_147
| ~ spl328_148
| ~ spl328_153
| ~ spl328_155
| spl328_156
| spl328_205 ),
inference(sat_conversion,[],[f25131]) ).
cnf(s225,plain,
( ~ spl328_151
| ~ spl328_203
| spl328_206 ),
inference(sat_conversion,[],[f25160]) ).
cnf(s229,plain,
( ~ spl328_151
| ~ spl328_203
| spl328_208 ),
inference(sat_conversion,[],[f25219]) ).
cnf(s233,plain,
( ~ spl328_151
| ~ spl328_203
| spl328_210 ),
inference(sat_conversion,[],[f25249]) ).
cnf(s236,plain,
( ~ spl328_151
| ~ spl328_203
| spl328_212 ),
inference(sat_conversion,[],[f25283]) ).
cnf(s262,plain,
( ~ spl328_137
| ~ spl328_147
| ~ spl328_148
| ~ spl328_151
| ~ spl328_153
| ~ spl328_155
| spl328_156
| spl328_201 ),
inference(sat_conversion,[],[f25493]) ).
cnf(s265,plain,
( spl328_167
| ~ spl328_168
| spl328_241 ),
inference(sat_conversion,[],[f25714]) ).
cnf(s339,plain,
( ~ spl328_137
| ~ spl328_147
| ~ spl328_148
| ~ spl328_151
| ~ spl328_153
| ~ spl328_155
| spl328_156
| ~ spl328_162
| spl328_239 ),
inference(sat_conversion,[],[f26418]) ).
cnf(s347,plain,
( ~ spl328_137
| ~ spl328_147
| ~ spl328_148
| ~ spl328_151
| ~ spl328_153
| ~ spl328_155
| spl328_156
| ~ spl328_162
| spl328_238 ),
inference(sat_conversion,[],[f26480]) ).
cnf(s356,plain,
( ~ spl328_137
| ~ spl328_138
| ~ spl328_139
| ~ spl328_140
| ~ spl328_141
| ~ spl328_142
| ~ spl328_143
| ~ spl328_144
| ~ spl328_153
| spl328_163
| ~ spl328_165
| ~ spl328_168
| ~ spl328_183
| ~ spl328_184
| ~ spl328_200
| ~ spl328_204
| ~ spl328_206
| ~ spl328_208
| ~ spl328_210
| ~ spl328_212
| ~ spl328_238
| ~ spl328_239
| ~ spl328_241 ),
inference(sat_conversion,[],[f26536]) ).
cnf(s357,plain,
spl328_155,
inference(rat,[],[s158,s148]) ).
cnf(s365,plain,
~ spl328_156,
inference(rat,[],[s159,s144,s140]) ).
cnf(s366,plain,
~ spl328_154,
inference(rat,[],[s157,s142,s156,s154,s153,s151,s150,s149,s148,s147,s146,s145,s144,s143,s140]) ).
cnf(s377,plain,
spl328_162,
inference(rat,[],[s170,s140,s148,s156,s154,s151,s150,s365]) ).
cnf(s379,plain,
spl328_157,
inference(rat,[],[s161,s140,s148,s156,s151,s150,s365]) ).
cnf(s380,plain,
spl328_201,
inference(rat,[],[s262,s140,s357,s150,s156,s154,s151,s365]) ).
cnf(s381,plain,
~ spl328_167,
inference(rat,[],[s178,s140,s357,s150,s156,s154,s151,s365]) ).
cnf(s385,plain,
spl328_205,
inference(rat,[],[s224,s140,s357,s149,s156,s151,s150,s365]) ).
cnf(s392,plain,
spl328_200,
inference(rat,[],[s218,s140,s142,s357,s156,s154,s151,s150,s149,s147,s146,s145,s365]) ).
cnf(s406,plain,
~ spl328_163,
inference(rat,[],[s172,s366,s377]) ).
cnf(s407,plain,
spl328_183,
inference(rat,[],[s195,s140,s142,s156,s154,s151,s150,s149,s148,s147,s146,s145,s144,s143,s377]) ).
cnf(s408,plain,
spl328_238,
inference(rat,[],[s347,s365,s140,s357,s150,s156,s154,s151,s377]) ).
cnf(s409,plain,
spl328_239,
inference(rat,[],[s339,s365,s140,s357,s150,s156,s154,s151,s377]) ).
cnf(s411,plain,
spl328_164,
inference(rat,[],[s174,s155,s379]) ).
cnf(s412,plain,
spl328_168,
inference(rat,[],[s220,s140,s380]) ).
cnf(s413,plain,
spl328_203,
inference(rat,[],[s223,s140,s142,s357,s156,s151,s150,s147,s146,s145,s144,s143,s385]) ).
cnf(s416,plain,
spl328_165,
inference(rat,[],[s176,s152,s411]) ).
cnf(s423,plain,
spl328_184,
inference(rat,[],[s197,s377,s140,s142,s156,s155,s154,s151,s150,s149,s148,s147,s146,s145,s144,s143,s411]) ).
cnf(s427,plain,
spl328_241,
inference(rat,[],[s265,s381,s412]) ).
cnf(s441,plain,
spl328_212,
inference(rat,[],[s236,s154,s413]) ).
cnf(s442,plain,
spl328_210,
inference(rat,[],[s233,s154,s413]) ).
cnf(s443,plain,
spl328_208,
inference(rat,[],[s229,s154,s413]) ).
cnf(s444,plain,
spl328_206,
inference(rat,[],[s225,s154,s413]) ).
cnf(s445,plain,
spl328_204,
inference(rat,[],[s222,s154,s413]) ).
cnf(s446,plain,
$false,
inference(rat,[],[s356,s427,s409,s408,s441,s442,s443,s444,s445,s392,s406,s407,s412,s140,s141,s156,s147,s146,s145,s144,s143,s142,s423,s416]) ).
fof(f26537,plain,
$false,
inference(avatar_sat_refutation,[],[s446]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT370+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.37 % Computer : n014.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sun Sep 27 15:06:20 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.41 Running first-order theorem proving
% 0.11/0.41 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
% 12.51/3.55 % (920101)Detected formulas, will run a generic FOF schedule.
% 12.51/3.55 % (920110)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1709404447:i=119:av=off:ss=axioms_2989 on theBenchmark for (2989ds/119Mi)
% 12.51/3.55 % (920108)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=3106195720:i=141695:sd=1:nm=32:gsp=on:ss=included_2989 on theBenchmark for (2989ds/141695Mi)
% 12.51/3.55 % (920107)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=547526124:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2989 on theBenchmark for (2989ds/134677Mi)
% 12.51/3.55 % (920109)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=4185497843:i=109:sd=1:ins=1:gsp=on:ss=axioms_2989 on theBenchmark for (2989ds/109Mi)
% 12.51/3.55 % (920106)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=2003268525:i=141193_2989 on theBenchmark for (2989ds/141193Mi)
% 12.51/3.55 % (920112)dis-21_1_sil=8000:lcm=predicate:random_seed=2778572139:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2989 on theBenchmark for (2989ds/129Mi)
% 12.51/3.55 % (920111)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=996370740:s2a=on:i=139:gtg=position_2989 on theBenchmark for (2989ds/139Mi)
% 12.51/3.55 % (920110)Instruction limit reached!
% 12.51/3.55 % (920110)------------------------------
% 12.51/3.55 % (920110)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.51/3.55 % (920110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.51/3.55 % (920110)CaDiCaL version: 2.1.3
% 12.51/3.55 % (920110)Termination reason: Instruction limit
% 12.51/3.55 % (920110)Termination phase: Preprocessing 1
% 12.51/3.55 % (920110)Time elapsed: 0.060 s
% 12.51/3.55 % (920110)Peak memory usage: 113 MB
% 12.51/3.55 % (920110)Instructions burned: 119 (million)
% 12.51/3.55 % (920111)Instruction limit reached!
% 12.51/3.55 % (920111)------------------------------
% 12.51/3.55 % (920111)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.51/3.55 % (920111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.51/3.55 % (920111)CaDiCaL version: 2.1.3
% 12.51/3.55 % (920111)Termination reason: Instruction limit
% 12.51/3.55 % (920111)Termination phase: Property scanning
% 12.51/3.55 % (920111)Time elapsed: 0.061 s
% 12.51/3.55 % (920111)Peak memory usage: 112 MB
% 12.51/3.55 % (920111)Instructions burned: 140 (million)
% 12.51/3.55 % (920109)Instruction limit reached!
% 12.51/3.55 % (920109)------------------------------
% 12.51/3.55 % (920109)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.51/3.55 % (920109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.51/3.55 % (920109)CaDiCaL version: 2.1.3
% 12.51/3.55 % (920109)Termination reason: Instruction limit
% 12.51/3.55 % (920109)Termination phase: SInE selection
% 12.51/3.55 % (920109)Time elapsed: 0.087 s
% 12.51/3.55 % (920109)Peak memory usage: 112 MB
% 12.51/3.55 % (920109)Instructions burned: 109 (million)
% 12.51/3.55 % (920112)Instruction limit reached!
% 12.51/3.55 % (920112)------------------------------
% 12.51/3.55 % (920112)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.51/3.55 % (920112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.51/3.55 % (920112)CaDiCaL version: 2.1.3
% 12.51/3.55 % (920112)Termination reason: Instruction limit
% 12.51/3.55 % (920112)Termination phase: SInE selection
% 12.51/3.55 % (920112)Time elapsed: 0.092 s
% 12.51/3.55 % (920112)Peak memory usage: 112 MB
% 12.51/3.55 % (920112)Instructions burned: 130 (million)
% 12.51/3.55 % (920120)lrs+10_1_sil=8000:sp=occurrence:random_seed=4251147473:i=285:sd=3:ss=axioms:sgt=8_2987 on theBenchmark for (2987ds/285Mi)
% 12.51/3.55 % (920121)lrs+10_1_sil=32000:urr=on:br=off:random_seed=638968640:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2986 on theBenchmark for (2986ds/157Mi)
% 12.51/3.55 % (920120)Instruction limit reached!
% 12.51/3.55 % (920120)------------------------------
% 12.51/3.55 % (920120)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.51/3.55 % (920120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.51/3.55 % (920120)CaDiCaL version: 2.1.3
% 12.51/3.55 % (920120)Termination reason: Instruction limit
% 12.51/3.55 % (920120)Termination phase: Saturation
% 18.48/4.47 % (920120)Time elapsed: 0.116 s
% 18.48/4.47 % (920120)Peak memory usage: 119 MB
% 18.48/4.47 % (920120)Instructions burned: 286 (million)
% 18.48/4.47 % (920122)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3114740089:i=325:sd=1:ss=axioms:sgt=32_2986 on theBenchmark for (2986ds/325Mi)
% 18.48/4.47 % (920124)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=1607361615:s2a=on:i=248:s2at=1.23:gtg=position_2986 on theBenchmark for (2986ds/248Mi)
% 18.48/4.47 % (920121)Instruction limit reached!
% 18.48/4.47 % (920121)------------------------------
% 18.48/4.47 % (920121)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.48/4.47 % (920121)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.48/4.47 % (920121)CaDiCaL version: 2.1.3
% 18.48/4.47 % (920121)Termination reason: Instruction limit
% 18.48/4.47 % (920121)Termination phase: Property scanning
% 18.48/4.47 % (920121)Time elapsed: 0.069 s
% 18.48/4.47 % (920121)Peak memory usage: 112 MB
% 18.48/4.47 % (920121)Instructions burned: 159 (million)
% 18.48/4.47 % (920126)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3669149766:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2985 on theBenchmark for (2985ds/294Mi)
% 18.48/4.47 % (920122)Refutation not found, incomplete strategy
% 18.48/4.47 % (920122)------------------------------
% 18.48/4.47 % (920122)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.48/4.47 % (920122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.48/4.47 % (920122)CaDiCaL version: 2.1.3
% 18.48/4.47 % (920122)Termination reason: Refutation not found, incomplete strategy
% 18.48/4.47 % (920122)Time elapsed: 0.116 s
% 18.48/4.47 % (920122)Peak memory usage: 117 MB
% 18.48/4.47 % (920122)Instructions burned: 129 (million)
% 18.48/4.47 % (920124)Instruction limit reached!
% 18.48/4.47 % (920124)------------------------------
% 18.48/4.47 % (920124)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.48/4.47 % (920124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.48/4.47 % (920124)CaDiCaL version: 2.1.3
% 18.48/4.47 % (920124)Termination reason: Instruction limit
% 18.48/4.47 % (920124)Termination phase: Property scanning
% 18.48/4.47 % (920124)Time elapsed: 0.107 s
% 18.48/4.47 % (920124)Peak memory usage: 112 MB
% 18.48/4.47 % (920124)Instructions burned: 248 (million)
% 18.48/4.47 % (920129)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1585935825:i=2350_2984 on theBenchmark for (2984ds/2350Mi)
% 18.48/4.47 % (920126)Instruction limit reached!
% 18.48/4.47 % (920126)------------------------------
% 18.48/4.47 % (920126)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.48/4.47 % (920126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.48/4.47 % (920126)CaDiCaL version: 2.1.3
% 18.48/4.47 % (920126)Termination reason: Instruction limit
% 18.48/4.47 % (920126)Termination phase: Property scanning
% 18.48/4.47 % (920126)Time elapsed: 0.130 s
% 18.48/4.47 % (920126)Peak memory usage: 119 MB
% 18.48/4.47 % (920126)Instructions burned: 295 (million)
% 18.48/4.47 % (920131)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2771226498:cts=off:i=113:fsr=off:ss=included:sgt=4_2984 on theBenchmark for (2984ds/113Mi)
% 18.48/4.47 % (920133)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1782210286:i=127:av=off:fsr=off:sup=off_2983 on theBenchmark for (2983ds/127Mi)
% 18.48/4.47 % (920131)Instruction limit reached!
% 18.48/4.47 % (920131)------------------------------
% 18.48/4.47 % (920131)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.48/4.47 % (920131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.48/4.47 % (920131)CaDiCaL version: 2.1.3
% 18.48/4.47 % (920131)Termination reason: Instruction limit
% 18.48/4.47 % (920131)Termination phase: SInE selection
% 18.48/4.47 % (920131)Time elapsed: 0.089 s
% 18.48/4.47 % (920131)Peak memory usage: 112 MB
% 18.48/4.47 % (920131)Instructions burned: 113 (million)
% 18.48/4.47 % (920122)------------------------------
% 18.48/4.47 % (920122)------------------------------
% 18.48/4.47 % (920133)Instruction limit reached!
% 18.48/4.47 % (920133)------------------------------
% 18.48/4.47 % (920133)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.48/4.47 % (920133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.48/4.47 % (920133)CaDiCaL version: 2.1.3
% 18.48/4.47 % (920133)Termination reason: Instruction limit
% 17.39/8.47 % (920133)Termination phase: Preprocessing 1
% 17.39/8.47 % (920133)Time elapsed: 0.056 s
% 17.39/8.47 % (920133)Peak memory usage: 113 MB
% 17.39/8.47 % (920133)Instructions burned: 129 (million)
% 17.39/8.47 % (920138)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=859662443:i=437:sd=1:aac=none:ss=included_2981 on theBenchmark for (2981ds/437Mi)
% 17.39/8.47 % (920136)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3216981002:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2981 on theBenchmark for (2981ds/114Mi)
% 17.39/8.47 % (920137)lrs+10_1_sil=8000:sp=occurrence:random_seed=618513285:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2981 on theBenchmark for (2981ds/907Mi)
% 17.39/8.47 % (920136)Instruction limit reached!
% 17.39/8.47 % (920136)------------------------------
% 17.39/8.47 % (920136)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.39/8.47 % (920136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.39/8.47 % (920136)CaDiCaL version: 2.1.3
% 17.39/8.47 % (920136)Termination reason: Instruction limit
% 17.39/8.47 % (920136)Termination phase: Property scanning
% 17.39/8.47 % (920136)Time elapsed: 0.050 s
% 17.39/8.47 % (920136)Peak memory usage: 112 MB
% 17.39/8.47 % (920136)Instructions burned: 116 (million)
% 17.39/8.47 % (920138)Instruction limit reached!
% 17.39/8.47 % (920138)------------------------------
% 17.39/8.47 % (920138)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.39/8.47 % (920138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.39/8.47 % (920138)CaDiCaL version: 2.1.3
% 17.39/8.47 % (920138)Termination reason: Instruction limit
% 17.39/8.47 % (920138)Termination phase: Saturation
% 17.39/8.47 % (920138)Time elapsed: 0.150 s
% 17.39/8.47 % (920138)Peak memory usage: 122 MB
% 17.39/8.47 % (920138)Instructions burned: 442 (million)
% 17.39/8.47 % (920142)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=503628383:i=5202:ss=axioms:sgt=16_2980 on theBenchmark for (2980ds/5202Mi)
% 17.39/8.47 % (920143)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3537093621:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2979 on theBenchmark for (2979ds/134Mi)
% 17.39/8.47 % (920143)Instruction limit reached!
% 17.39/8.47 % (920143)------------------------------
% 17.39/8.47 % (920143)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.39/8.47 % (920143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.39/8.47 % (920143)CaDiCaL version: 2.1.3
% 17.39/8.47 % (920143)Termination reason: Instruction limit
% 17.39/8.47 % (920143)Termination phase: Preprocessing 2
% 17.39/8.47 % (920143)Time elapsed: 0.076 s
% 17.39/8.47 % (920143)Peak memory usage: 114 MB
% 17.39/8.47 % (920143)Instructions burned: 135 (million)
% 17.39/8.47 % (920146)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=273025102:st=8:i=592:sd=3:ep=RST:ss=axioms_2977 on theBenchmark for (2977ds/592Mi)
% 17.39/8.47 % (920137)Instruction limit reached!
% 17.39/8.47 % (920137)------------------------------
% 17.39/8.47 % (920137)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.39/8.47 % (920137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.39/8.47 % (920137)CaDiCaL version: 2.1.3
% 17.39/8.47 % (920137)Termination reason: Instruction limit
% 17.39/8.47 % (920137)Termination phase: Saturation
% 17.39/8.47 % (920137)Time elapsed: 0.551 s
% 17.39/8.47 % (920137)Peak memory usage: 132 MB
% 17.39/8.47 % (920137)Instructions burned: 908 (million)
% 17.39/8.47 % (920146)Instruction limit reached!
% 17.39/8.47 % (920146)------------------------------
% 17.39/8.47 % (920146)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.39/8.47 % (920146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.39/8.47 % (920146)CaDiCaL version: 2.1.3
% 17.39/8.47 % (920146)Termination reason: Instruction limit
% 17.39/8.47 % (920146)Termination phase: Preprocessing 3
% 17.39/8.47 % (920146)Time elapsed: 0.260 s
% 17.39/8.47 % (920146)Peak memory usage: 134 MB
% 17.39/8.47 % (920146)Instructions burned: 595 (million)
% 17.39/8.47 % (920148)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1511020657:st=3:i=13193:sd=3:ss=axioms_2974 on theBenchmark for (2974ds/13193Mi)
% 17.39/8.47 % (920149)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=3450480419:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2973 on theBenchmark for (2973ds/125Mi)
% 17.39/8.47 % (920149)Instruction limit reached!
% 17.39/8.47 % (920149)------------------------------
% 17.39/8.47 % (920149)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.39/8.47 % (920149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.39/8.47 % (920149)CaDiCaL version: 2.1.3
% 17.39/8.47 % (920149)Termination reason: Instruction limit
% 17.39/8.47 % (920149)Termination phase: Property scanning
% 17.39/8.47 % (920149)Time elapsed: 0.030 s
% 17.39/8.47 % (920149)Peak memory usage: 112 MB
% 17.39/8.47 % (920149)Instructions burned: 130 (million)
% 17.39/8.47 % (920152)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=664048652:i=134:gtgl=5:slsql=off:gtg=exists_sym_2972 on theBenchmark for (2972ds/134Mi)
% 17.39/8.47 % (920152)Instruction limit reached!
% 17.39/8.47 % (920152)------------------------------
% 17.39/8.47 % (920152)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.39/8.47 % (920152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.39/8.47 % (920152)CaDiCaL version: 2.1.3
% 17.39/8.47 % (920152)Termination reason: Instruction limit
% 17.39/8.47 % (920152)Termination phase: Property scanning
% 17.39/8.47 % (920152)Time elapsed: 0.032 s
% 17.39/8.47 % (920152)Peak memory usage: 112 MB
% 17.39/8.47 % (920152)Instructions burned: 137 (million)
% 17.39/8.47 % (920129)Instruction limit reached!
% 17.39/8.47 % (920129)------------------------------
% 17.39/8.47 % (920129)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.39/8.47 % (920129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.39/8.47 % (920129)CaDiCaL version: 2.1.3
% 17.39/8.47 % (920129)Termination reason: Instruction limit
% 17.39/8.47 % (920129)Termination phase: Property scanning
% 17.39/8.47 % (920129)Time elapsed: 1.256 s
% 17.39/8.47 % (920129)Peak memory usage: 171 MB
% 17.39/8.47 % (920129)Instructions burned: 2350 (million)
% 17.39/8.47 % (920154)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2721767210:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2971 on theBenchmark for (2971ds/141Mi)
% 17.39/8.47 % (920154)Refutation not found, incomplete strategy
% 17.39/8.47 % (920154)------------------------------
% 17.39/8.47 % (920154)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.39/8.47 % (920154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.39/8.47 % (920154)CaDiCaL version: 2.1.3
% 17.39/8.47 % (920154)Termination reason: Refutation not found, incomplete strategy
% 17.39/8.47 % (920154)Time elapsed: 0.065 s
% 17.39/8.47 % (920154)Peak memory usage: 117 MB
% 17.39/8.47 % (920154)Instructions burned: 124 (million)
% 17.39/8.47 % (920155)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=626826268:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2970 on theBenchmark for (2970ds/431Mi)
% 17.39/8.47 % (920154)------------------------------
% 17.39/8.47 % (920154)------------------------------
% 17.39/8.47 % (920158)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=215145447:i=6060:aac=none:ins=25_2968 on theBenchmark for (2968ds/6060Mi)
% 17.39/8.47 % (920155)Instruction limit reached!
% 17.39/8.47 % (920155)------------------------------
% 17.39/8.47 % (920155)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.39/8.47 % (920155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.39/8.47 % (920155)CaDiCaL version: 2.1.3
% 17.39/8.47 % (920155)Termination reason: Instruction limit
% 17.39/8.47 % (920155)Termination phase: Saturation
% 17.39/8.47 % (920155)Time elapsed: 0.309 s
% 17.39/8.47 % (920155)Peak memory usage: 121 MB
% 17.39/8.47 % (920155)Instructions burned: 431 (million)
% 17.39/8.47 % (920160)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=3905992234:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2966 on theBenchmark for (2966ds/150Mi)
% 17.39/8.47 % (920160)Instruction limit reached!
% 17.39/8.47 % (920160)------------------------------
% 17.39/8.47 % (920160)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.39/8.47 % (920160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.39/8.47 % (920160)CaDiCaL version: 2.1.3
% 17.39/8.47 % (920160)Termination reason: Instruction limit
% 17.39/8.47 % (920160)Termination phase: Preprocessing 1
% 17.39/8.47 % (920160)Time elapsed: 0.125 s
% 17.39/8.47 % (920160)Peak memory usage: 113 MB
% 17.39/8.47 % (920160)Instructions burned: 151 (million)
% 17.39/8.47 % (920162)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3871538370:i=14155:bd=all_2963 on theBenchmark for (2963ds/14155Mi)
% 17.39/8.47 % (920142)Instruction limit reached!
% 17.39/8.47 % (920142)------------------------------
% 17.39/8.47 % (920142)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.39/8.47 % (920142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.39/8.47 % (920142)CaDiCaL version: 2.1.3
% 17.39/8.47 % (920142)Termination reason: Instruction limit
% 17.39/8.47 % (920142)Termination phase: Saturation
% 17.39/8.47 % (920142)Time elapsed: 3.043 s
% 17.39/8.47 % (920142)Peak memory usage: 238 MB
% 17.39/8.47 % (920142)Instructions burned: 5206 (million)
% 17.39/8.47 % (920164)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3615224239:i=667:av=off:fsr=off_2948 on theBenchmark for (2948ds/667Mi)
% 17.39/8.47 % (920164)Instruction limit reached!
% 17.39/8.47 % (920164)------------------------------
% 17.39/8.47 % (920164)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.39/8.47 % (920164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.39/8.47 % (920164)CaDiCaL version: 2.1.3
% 17.39/8.47 % (920164)Termination reason: Instruction limit
% 17.39/8.47 % (920164)Termination phase: NewCNF
% 17.39/8.47 % (920164)Time elapsed: 0.532 s
% 17.39/8.47 % (920164)Peak memory usage: 149 MB
% 17.39/8.47 % (920164)Instructions burned: 669 (million)
% 17.39/8.47 % (920158)Instruction limit reached!
% 17.39/8.47 % (920158)------------------------------
% 17.39/8.47 % (920158)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.39/8.47 % (920158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.39/8.47 % (920158)CaDiCaL version: 2.1.3
% 17.39/8.47 % (920158)Termination reason: Instruction limit
% 17.39/8.47 % (920158)Termination phase: Saturation
% 17.39/8.47 % (920158)Time elapsed: 2.733 s
% 17.39/8.47 % (920158)Peak memory usage: 574 MB
% 17.39/8.47 % (920158)Instructions burned: 6064 (million)
% 17.39/8.47 % (920166)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=3096830991:s2a=on:i=185:s2at=1.8:fdi=4_2941 on theBenchmark for (2941ds/185Mi)
% 17.39/8.47 % (920168)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2428751020:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2939 on theBenchmark for (2939ds/193Mi)
% 17.39/8.47 % (920166)Instruction limit reached!
% 17.39/8.47 % (920166)------------------------------
% 17.39/8.47 % (920166)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.39/8.47 % (920166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.39/8.47 % (920166)CaDiCaL version: 2.1.3
% 17.39/8.47 % (920166)Termination reason: Instruction limit
% 17.39/8.47 % (920166)Termination phase: SInE selection
% 17.39/8.47 % (920166)Time elapsed: 0.154 s
% 17.39/8.47 % (920166)Peak memory usage: 113 MB
% 17.39/8.47 % (920166)Instructions burned: 185 (million)
% 17.39/8.47 % (920168)Instruction limit reached!
% 17.39/8.47 % (920168)------------------------------
% 17.39/8.47 % (920168)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.39/8.47 % (920168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.39/8.47 % (920168)CaDiCaL version: 2.1.3
% 17.39/8.47 % (920168)Termination reason: Instruction limit
% 17.39/8.47 % (920168)Termination phase: SInE selection
% 17.39/8.47 % (920168)Time elapsed: 0.129 s
% 17.39/8.47 % (920168)Peak memory usage: 112 MB
% 17.39/8.47 % (920168)Instructions burned: 193 (million)
% 17.39/8.47 % (920170)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=3737553931:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2938 on theBenchmark for (2938ds/4850Mi)
% 17.39/8.47 % (920171)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=3544588488:i=12111:sd=1:ss=included_2937 on theBenchmark for (2937ds/12111Mi)
% 17.39/8.47 % (920171)First to succeed.
% 17.39/8.47 % (920171)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-920101"
% 17.39/8.47 % (920171)Refutation found. Thanks to Tanya!
% 17.39/8.47 % SZS status Theorem for theBenchmark
% 17.39/8.47 % SZS output start Proof for theBenchmark
% See solution above
% 47.69/8.68 % (920171)------------------------------
% 47.69/8.68 % (920171)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.69/8.68 % (920171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.69/8.68 % (920171)CaDiCaL version: 2.1.3
% 47.69/8.68 % (920171)Termination reason: Refutation
% 47.69/8.68 % (920171)Time elapsed: 0.979 s
% 47.69/8.68 % (920171)Peak memory usage: 197 MB
% 47.69/8.68 % (920171)Instructions burned: 2622 (million)
% 47.69/8.68 % (920171)------------------------------
% 47.69/8.68 % (920171)------------------------------
% 47.69/8.68 % (920101)Success in time 7.62 s
% 47.69/8.68 % Vampire exiting
%------------------------------------------------------------------------------