%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT369+2 : 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:25 AM UTC 2026
% Result : Theorem 17.51s 7.91s
% Output : Refutation 47.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 57
% Syntax : Number of formulae : 442 ( 80 unt; 43 def)
% Number of atoms : 3097 ( 69 equ)
% Maximal formula atoms : 25 ( 7 avg)
% Number of connectives : 4864 (2209 ~;2324 |; 257 &)
% ( 43 <=>; 31 =>; 0 <=; 0 <~>)
% Maximal formula depth : 28 ( 8 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 74 ( 72 usr; 40 prp; 0-3 aty)
% Number of functors : 12 ( 12 usr; 5 con; 0-3 aty)
% Number of variables : 264 ( 0 sgn 260 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1257,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(f6865,axiom,
! [X0] :
( l1_orders_2(X0)
=> ( v2_lattice3(X0)
=> ~ v3_struct_0(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc2_lattice3) ).
fof(f7972,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(f8310,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(f8331,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(f8338,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(f8396,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(f8398,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(f8453,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(f10369,axiom,
! [X0] :
( ( v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& v2_lattice3(X0)
& v3_lattice3(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( ( v2_orders_2(X1)
& v3_orders_2(X1)
& v4_orders_2(X1)
& v1_lattice3(X1)
& v2_lattice3(X1)
& v3_lattice3(X1)
& l1_orders_2(X1) )
=> ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v17_waybel_0(X2,X0,X1)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> ( v22_waybel_0(X2,X0,X1)
=> v1_waybel34(k1_waybel34(X0,X1,X2),X1,X0) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t24_waybel34) ).
fof(f10380,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(f10387,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(f10388,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(f10390,conjecture,
! [X0] :
( ( v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& v2_lattice3(X0)
& v3_lattice3(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( ( v1_funct_1(X1)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v7_waybel_1(X1,X0)
& m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
=> ( v4_waybel_0(k2_yellow_2(X0,X0,X1),X0)
=> v1_waybel34(k2_waybel_1(X0,X0,X1),X0,k2_yellow_2(X0,X0,X1)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t42_waybel34) ).
fof(f10391,negated_conjecture,
~ ! [X0] :
( ( v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& v2_lattice3(X0)
& v3_lattice3(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( ( v1_funct_1(X1)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v7_waybel_1(X1,X0)
& m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
=> ( v4_waybel_0(k2_yellow_2(X0,X0,X1),X0)
=> v1_waybel34(k2_waybel_1(X0,X0,X1),X0,k2_yellow_2(X0,X0,X1)) ) ) ),
inference(negated_conjecture,[status(cth)],[f10390]) ).
fof(f10508,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( v1_waybel34(k1_waybel34(X0,X1,X2),X1,X0)
| ~ v22_waybel_0(X2,X0,X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v17_waybel_0(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ v3_lattice3(X1)
| ~ l1_orders_2(X1) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f10369]) ).
fof(f10509,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( v1_waybel34(k1_waybel34(X0,X1,X2),X1,X0)
| ~ v22_waybel_0(X2,X0,X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v17_waybel_0(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ v3_lattice3(X1)
| ~ l1_orders_2(X1) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f10508]) ).
fof(f10529,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,[],[f10380]) ).
fof(f10530,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,[],[f10529]) ).
fof(f10543,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,[],[f10387]) ).
fof(f10544,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,[],[f10543]) ).
fof(f10545,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,[],[f10388]) ).
fof(f10546,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,[],[f10545]) ).
fof(f10549,plain,
? [X0] :
( ? [X1] :
( ~ v1_waybel34(k2_waybel_1(X0,X0,X1),X0,k2_yellow_2(X0,X0,X1))
& v4_waybel_0(k2_yellow_2(X0,X0,X1),X0)
& v1_funct_1(X1)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v7_waybel_1(X1,X0)
& m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
& v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& v2_lattice3(X0)
& v3_lattice3(X0)
& l1_orders_2(X0) ),
inference(ennf_transformation,[],[f10391]) ).
fof(f10550,plain,
? [X0] :
( ? [X1] :
( ~ v1_waybel34(k2_waybel_1(X0,X0,X1),X0,k2_yellow_2(X0,X0,X1))
& v4_waybel_0(k2_yellow_2(X0,X0,X1),X0)
& v1_funct_1(X1)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v7_waybel_1(X1,X0)
& m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
& v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& v2_lattice3(X0)
& v3_lattice3(X0)
& l1_orders_2(X0) ),
inference(flattening,[],[f10549]) ).
fof(f10553,plain,
! [X0] :
( ~ v3_struct_0(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f6865]) ).
fof(f10554,plain,
! [X0] :
( ~ v3_struct_0(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f10553]) ).
fof(f11313,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,[],[f8310]) ).
fof(f11314,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,[],[f11313]) ).
fof(f11411,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,[],[f8331]) ).
fof(f11412,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,[],[f11411]) ).
fof(f11441,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,[],[f8396]) ).
fof(f11442,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,[],[f11441]) ).
fof(f11451,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,[],[f8453]) ).
fof(f11452,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,[],[f11451]) ).
fof(f11463,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,[],[f8398]) ).
fof(f11464,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,[],[f11463]) ).
fof(f11465,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,[],[f8338]) ).
fof(f11466,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,[],[f11465]) ).
fof(f11469,plain,
! [X0] :
( ! [X1] :
( l1_orders_2(X1)
| ~ m1_yellow_0(X1,X0) )
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f7972]) ).
fof(f11533,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(f11534,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,[],[f10530,f11533]) ).
fof(f11700,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,[],[f11533]) ).
fof(f11701,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,[],[f11700]) ).
fof(f11712,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,[],[f10546]) ).
fof(f11717,plain,
( ~ v1_waybel34(k2_waybel_1(sK105,sK105,sK106),sK105,k2_yellow_2(sK105,sK105,sK106))
& v4_waybel_0(k2_yellow_2(sK105,sK105,sK106),sK105)
& v1_funct_1(sK106)
& v1_funct_2(sK106,u1_struct_0(sK105),u1_struct_0(sK105))
& v7_waybel_1(sK106,sK105)
& m2_relset_1(sK106,u1_struct_0(sK105),u1_struct_0(sK105))
& v2_orders_2(sK105)
& v3_orders_2(sK105)
& v4_orders_2(sK105)
& v1_lattice3(sK105)
& v2_lattice3(sK105)
& v3_lattice3(sK105)
& l1_orders_2(sK105) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK105,sK106]),skolemize(X0,sK105),skolemize(X1,sK106)],[f10550]) ).
fof(f11720,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,[],[f1257]) ).
fof(f12350,plain,
! [X2,X0,X1] :
( v1_waybel34(k1_waybel34(X0,X1,X2),X1,X0)
| ~ v22_waybel_0(X2,X0,X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v17_waybel_0(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ v3_lattice3(X1)
| ~ l1_orders_2(X1)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f10509]) ).
fof(f12383,plain,
! [X0,X1] :
( ~ sP19(X0,X1)
| v3_lattice3(k2_yellow_2(X1,X1,X0)) ),
inference(cnf_transformation,[],[f11701]) ).
fof(f12384,plain,
! [X0,X1] :
( ~ sP19(X0,X1)
| v2_lattice3(k2_yellow_2(X1,X1,X0)) ),
inference(cnf_transformation,[],[f11701]) ).
fof(f12385,plain,
! [X0,X1] :
( ~ sP19(X0,X1)
| v1_lattice3(k2_yellow_2(X1,X1,X0)) ),
inference(cnf_transformation,[],[f11701]) ).
fof(f12392,plain,
! [X0,X1] :
( ~ sP19(X0,X1)
| v4_orders_2(k2_yellow_2(X1,X1,X0)) ),
inference(cnf_transformation,[],[f11701]) ).
fof(f12393,plain,
! [X0,X1] :
( ~ sP19(X0,X1)
| v3_orders_2(k2_yellow_2(X1,X1,X0)) ),
inference(cnf_transformation,[],[f11701]) ).
fof(f12394,plain,
! [X0,X1] :
( ~ sP19(X0,X1)
| v2_orders_2(k2_yellow_2(X1,X1,X0)) ),
inference(cnf_transformation,[],[f11701]) ).
fof(f12397,plain,
! [X0,X1] :
( ~ v3_lattice3(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| sP19(X1,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,[],[f11534]) ).
fof(f12428,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,[],[f10544]) ).
fof(f12430,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,[],[f10544]) ).
fof(f12432,plain,
! [X0,X1] :
( ~ v3_lattice3(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)
| v22_waybel_0(k3_waybel_1(X0,X0,X1),k2_yellow_2(X0,X0,X1),X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f11712]) ).
fof(f12447,plain,
l1_orders_2(sK105),
inference(cnf_transformation,[],[f11717]) ).
fof(f12448,plain,
v3_lattice3(sK105),
inference(cnf_transformation,[],[f11717]) ).
fof(f12449,plain,
v2_lattice3(sK105),
inference(cnf_transformation,[],[f11717]) ).
fof(f12450,plain,
v1_lattice3(sK105),
inference(cnf_transformation,[],[f11717]) ).
fof(f12451,plain,
v4_orders_2(sK105),
inference(cnf_transformation,[],[f11717]) ).
fof(f12452,plain,
v3_orders_2(sK105),
inference(cnf_transformation,[],[f11717]) ).
fof(f12453,plain,
v2_orders_2(sK105),
inference(cnf_transformation,[],[f11717]) ).
fof(f12454,plain,
m2_relset_1(sK106,u1_struct_0(sK105),u1_struct_0(sK105)),
inference(cnf_transformation,[],[f11717]) ).
fof(f12455,plain,
v7_waybel_1(sK106,sK105),
inference(cnf_transformation,[],[f11717]) ).
fof(f12456,plain,
v1_funct_2(sK106,u1_struct_0(sK105),u1_struct_0(sK105)),
inference(cnf_transformation,[],[f11717]) ).
fof(f12457,plain,
v1_funct_1(sK106),
inference(cnf_transformation,[],[f11717]) ).
fof(f12458,plain,
v4_waybel_0(k2_yellow_2(sK105,sK105,sK106),sK105),
inference(cnf_transformation,[],[f11717]) ).
fof(f12459,plain,
~ v1_waybel34(k2_waybel_1(sK105,sK105,sK106),sK105,k2_yellow_2(sK105,sK105,sK106)),
inference(cnf_transformation,[],[f11717]) ).
fof(f12467,plain,
! [X2,X0,X1] :
( m1_relset_1(X2,X0,X1)
| ~ m2_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f11720]) ).
fof(f12475,plain,
! [X0] :
( ~ v2_lattice3(X0)
| ~ v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f10554]) ).
fof(f13807,plain,
! [X2,X0,X1] :
( ~ l1_orders_2(X0)
| v3_struct_0(X0)
| m1_yellow_0(k2_yellow_2(X0,X1,X2),X1)
| 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,[],[f11314]) ).
fof(f13955,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,[],[f11412]) ).
fof(f14021,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,[],[f11442]) ).
fof(f14030,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,[],[f11452]) ).
fof(f14038,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,[],[f11464]) ).
fof(f14041,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,[],[f11466]) ).
fof(f14044,plain,
! [X2,X0,X1] :
( v1_funct_1(k3_waybel_1(X0,X1,X2))
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| v3_struct_0(X1)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f11466]) ).
fof(f14048,plain,
! [X0,X1] :
( ~ l1_orders_2(X0)
| ~ m1_yellow_0(X1,X0)
| l1_orders_2(X1) ),
inference(cnf_transformation,[],[f11469]) ).
fof(f14177,definition,
sF287 = k2_waybel_1(sK105,sK105,sK106),
introduced(definition,[new_symbols(definition,[sF287])],[function_definition]) ).
fof(f14178,plain,
k2_waybel_1(sK105,sK105,sK106) = sF287,
inference(reorient_equations,[],[f14177]) ).
fof(f14179,definition,
sF288 = k2_yellow_2(sK105,sK105,sK106),
introduced(definition,[new_symbols(definition,[sF288])],[function_definition]) ).
fof(f14180,plain,
k2_yellow_2(sK105,sK105,sK106) = sF288,
inference(reorient_equations,[],[f14179]) ).
fof(f14181,plain,
~ v1_waybel34(sF287,sK105,sF288),
inference(definition_folding,[],[f12459,f14180,f14178]) ).
fof(f14182,plain,
v4_waybel_0(sF288,sK105),
inference(definition_folding,[],[f12458,f14180]) ).
fof(f14183,definition,
sF289 = u1_struct_0(sK105),
introduced(definition,[new_symbols(definition,[sF289])],[function_definition]) ).
fof(f14184,plain,
u1_struct_0(sK105) = sF289,
inference(reorient_equations,[],[f14183]) ).
fof(f14185,plain,
v1_funct_2(sK106,sF289,sF289),
inference(definition_folding,[],[f12456,f14184,f14184]) ).
fof(f14186,plain,
m2_relset_1(sK106,sF289,sF289),
inference(definition_folding,[],[f12454,f14184,f14184]) ).
fof(f14871,definition,
( spl290_132
<=> l1_orders_2(sK105) ),
introduced(definition,[new_symbols(definition,[spl290_132])],[avatar_definition]) ).
fof(f14873,plain,
( l1_orders_2(sK105)
| ~ spl290_132 ),
inference(avatar_component_clause,[],[f14871]) ).
fof(f14874,plain,
spl290_132,
inference(avatar_split_clause,[],[f12447,f14871]) ).
fof(f14876,definition,
( spl290_133
<=> v3_lattice3(sK105) ),
introduced(definition,[new_symbols(definition,[spl290_133])],[avatar_definition]) ).
fof(f14878,plain,
( v3_lattice3(sK105)
| ~ spl290_133 ),
inference(avatar_component_clause,[],[f14876]) ).
fof(f14879,plain,
spl290_133,
inference(avatar_split_clause,[],[f12448,f14876]) ).
fof(f14881,definition,
( spl290_134
<=> v2_lattice3(sK105) ),
introduced(definition,[new_symbols(definition,[spl290_134])],[avatar_definition]) ).
fof(f14883,plain,
( v2_lattice3(sK105)
| ~ spl290_134 ),
inference(avatar_component_clause,[],[f14881]) ).
fof(f14884,plain,
spl290_134,
inference(avatar_split_clause,[],[f12449,f14881]) ).
fof(f14886,definition,
( spl290_135
<=> v1_lattice3(sK105) ),
introduced(definition,[new_symbols(definition,[spl290_135])],[avatar_definition]) ).
fof(f14888,plain,
( v1_lattice3(sK105)
| ~ spl290_135 ),
inference(avatar_component_clause,[],[f14886]) ).
fof(f14889,plain,
spl290_135,
inference(avatar_split_clause,[],[f12450,f14886]) ).
fof(f14891,definition,
( spl290_136
<=> v4_orders_2(sK105) ),
introduced(definition,[new_symbols(definition,[spl290_136])],[avatar_definition]) ).
fof(f14893,plain,
( v4_orders_2(sK105)
| ~ spl290_136 ),
inference(avatar_component_clause,[],[f14891]) ).
fof(f14894,plain,
spl290_136,
inference(avatar_split_clause,[],[f12451,f14891]) ).
fof(f14896,definition,
( spl290_137
<=> v3_orders_2(sK105) ),
introduced(definition,[new_symbols(definition,[spl290_137])],[avatar_definition]) ).
fof(f14898,plain,
( v3_orders_2(sK105)
| ~ spl290_137 ),
inference(avatar_component_clause,[],[f14896]) ).
fof(f14899,plain,
spl290_137,
inference(avatar_split_clause,[],[f12452,f14896]) ).
fof(f14901,definition,
( spl290_138
<=> v2_orders_2(sK105) ),
introduced(definition,[new_symbols(definition,[spl290_138])],[avatar_definition]) ).
fof(f14903,plain,
( v2_orders_2(sK105)
| ~ spl290_138 ),
inference(avatar_component_clause,[],[f14901]) ).
fof(f14904,plain,
spl290_138,
inference(avatar_split_clause,[],[f12453,f14901]) ).
fof(f14906,definition,
( spl290_139
<=> m2_relset_1(sK106,sF289,sF289) ),
introduced(definition,[new_symbols(definition,[spl290_139])],[avatar_definition]) ).
fof(f14908,plain,
( m2_relset_1(sK106,sF289,sF289)
| ~ spl290_139 ),
inference(avatar_component_clause,[],[f14906]) ).
fof(f14909,plain,
spl290_139,
inference(avatar_split_clause,[],[f14186,f14906]) ).
fof(f14911,definition,
( spl290_140
<=> v7_waybel_1(sK106,sK105) ),
introduced(definition,[new_symbols(definition,[spl290_140])],[avatar_definition]) ).
fof(f14913,plain,
( v7_waybel_1(sK106,sK105)
| ~ spl290_140 ),
inference(avatar_component_clause,[],[f14911]) ).
fof(f14914,plain,
spl290_140,
inference(avatar_split_clause,[],[f12455,f14911]) ).
fof(f14916,definition,
( spl290_141
<=> v1_funct_2(sK106,sF289,sF289) ),
introduced(definition,[new_symbols(definition,[spl290_141])],[avatar_definition]) ).
fof(f14918,plain,
( v1_funct_2(sK106,sF289,sF289)
| ~ spl290_141 ),
inference(avatar_component_clause,[],[f14916]) ).
fof(f14919,plain,
spl290_141,
inference(avatar_split_clause,[],[f14185,f14916]) ).
fof(f14921,definition,
( spl290_142
<=> v1_funct_1(sK106) ),
introduced(definition,[new_symbols(definition,[spl290_142])],[avatar_definition]) ).
fof(f14923,plain,
( v1_funct_1(sK106)
| ~ spl290_142 ),
inference(avatar_component_clause,[],[f14921]) ).
fof(f14924,plain,
spl290_142,
inference(avatar_split_clause,[],[f12457,f14921]) ).
fof(f14926,definition,
( spl290_143
<=> v4_waybel_0(sF288,sK105) ),
introduced(definition,[new_symbols(definition,[spl290_143])],[avatar_definition]) ).
fof(f14928,plain,
( v4_waybel_0(sF288,sK105)
| ~ spl290_143 ),
inference(avatar_component_clause,[],[f14926]) ).
fof(f14929,plain,
spl290_143,
inference(avatar_split_clause,[],[f14182,f14926]) ).
fof(f14931,definition,
( spl290_144
<=> v1_waybel34(sF287,sK105,sF288) ),
introduced(definition,[new_symbols(definition,[spl290_144])],[avatar_definition]) ).
fof(f14933,plain,
( ~ v1_waybel34(sF287,sK105,sF288)
| spl290_144 ),
inference(avatar_component_clause,[],[f14931]) ).
fof(f14934,plain,
~ spl290_144,
inference(avatar_split_clause,[],[f14181,f14931]) ).
fof(f14945,definition,
( spl290_145
<=> k2_waybel_1(sK105,sK105,sK106) = sF287 ),
introduced(definition,[new_symbols(definition,[spl290_145])],[avatar_definition]) ).
fof(f14947,plain,
( k2_waybel_1(sK105,sK105,sK106) = sF287
| ~ spl290_145 ),
inference(avatar_component_clause,[],[f14945]) ).
fof(f14948,plain,
spl290_145,
inference(avatar_split_clause,[],[f14178,f14945]) ).
fof(f14950,definition,
( spl290_146
<=> k2_yellow_2(sK105,sK105,sK106) = sF288 ),
introduced(definition,[new_symbols(definition,[spl290_146])],[avatar_definition]) ).
fof(f14952,plain,
( k2_yellow_2(sK105,sK105,sK106) = sF288
| ~ spl290_146 ),
inference(avatar_component_clause,[],[f14950]) ).
fof(f14953,plain,
spl290_146,
inference(avatar_split_clause,[],[f14180,f14950]) ).
fof(f14955,definition,
( spl290_147
<=> u1_struct_0(sK105) = sF289 ),
introduced(definition,[new_symbols(definition,[spl290_147])],[avatar_definition]) ).
fof(f14957,plain,
( u1_struct_0(sK105) = sF289
| ~ spl290_147 ),
inference(avatar_component_clause,[],[f14955]) ).
fof(f14958,plain,
spl290_147,
inference(avatar_split_clause,[],[f14184,f14955]) ).
fof(f15003,plain,
( ! [X0] :
( ~ v4_waybel_0(k2_yellow_2(sK105,sK105,X0),sK105)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK105),u1_struct_0(sK105))
| ~ v7_waybel_1(X0,sK105)
| ~ m2_relset_1(X0,u1_struct_0(sK105),u1_struct_0(sK105))
| ~ v2_orders_2(sK105)
| ~ v3_orders_2(sK105)
| ~ v4_orders_2(sK105)
| ~ v1_lattice3(sK105)
| ~ v2_lattice3(sK105)
| v22_waybel_0(k3_waybel_1(sK105,sK105,X0),k2_yellow_2(sK105,sK105,X0),sK105)
| ~ l1_orders_2(sK105) )
| ~ spl290_133 ),
inference(resolution,[],[f12432,f14878]) ).
fof(f15004,plain,
( ! [X0] :
( ~ v4_waybel_0(k2_yellow_2(sK105,sK105,X0),sK105)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK105),u1_struct_0(sK105))
| ~ v7_waybel_1(X0,sK105)
| ~ m2_relset_1(X0,u1_struct_0(sK105),u1_struct_0(sK105))
| ~ v3_orders_2(sK105)
| ~ v4_orders_2(sK105)
| ~ v1_lattice3(sK105)
| ~ v2_lattice3(sK105)
| v22_waybel_0(k3_waybel_1(sK105,sK105,X0),k2_yellow_2(sK105,sK105,X0),sK105)
| ~ l1_orders_2(sK105) )
| ~ spl290_133
| ~ spl290_138 ),
inference(forward_subsumption_resolution,[],[f15003,f14903]) ).
fof(f15005,plain,
( ! [X0] :
( ~ v4_waybel_0(k2_yellow_2(sK105,sK105,X0),sK105)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK105),u1_struct_0(sK105))
| ~ v7_waybel_1(X0,sK105)
| ~ m2_relset_1(X0,u1_struct_0(sK105),u1_struct_0(sK105))
| ~ v4_orders_2(sK105)
| ~ v1_lattice3(sK105)
| ~ v2_lattice3(sK105)
| v22_waybel_0(k3_waybel_1(sK105,sK105,X0),k2_yellow_2(sK105,sK105,X0),sK105)
| ~ l1_orders_2(sK105) )
| ~ spl290_133
| ~ spl290_137
| ~ spl290_138 ),
inference(forward_subsumption_resolution,[],[f15004,f14898]) ).
fof(f15006,plain,
( ! [X0] :
( ~ v4_waybel_0(k2_yellow_2(sK105,sK105,X0),sK105)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK105),u1_struct_0(sK105))
| ~ v7_waybel_1(X0,sK105)
| ~ m2_relset_1(X0,u1_struct_0(sK105),u1_struct_0(sK105))
| ~ v1_lattice3(sK105)
| ~ v2_lattice3(sK105)
| v22_waybel_0(k3_waybel_1(sK105,sK105,X0),k2_yellow_2(sK105,sK105,X0),sK105)
| ~ l1_orders_2(sK105) )
| ~ spl290_133
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138 ),
inference(forward_subsumption_resolution,[],[f15005,f14893]) ).
fof(f15007,plain,
( ! [X0] :
( ~ v4_waybel_0(k2_yellow_2(sK105,sK105,X0),sK105)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK105),u1_struct_0(sK105))
| ~ v7_waybel_1(X0,sK105)
| ~ m2_relset_1(X0,u1_struct_0(sK105),u1_struct_0(sK105))
| ~ v2_lattice3(sK105)
| v22_waybel_0(k3_waybel_1(sK105,sK105,X0),k2_yellow_2(sK105,sK105,X0),sK105)
| ~ l1_orders_2(sK105) )
| ~ spl290_133
| ~ spl290_135
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138 ),
inference(forward_subsumption_resolution,[],[f15006,f14888]) ).
fof(f15008,plain,
( ! [X0] :
( ~ v4_waybel_0(k2_yellow_2(sK105,sK105,X0),sK105)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK105),u1_struct_0(sK105))
| ~ v7_waybel_1(X0,sK105)
| ~ m2_relset_1(X0,u1_struct_0(sK105),u1_struct_0(sK105))
| v22_waybel_0(k3_waybel_1(sK105,sK105,X0),k2_yellow_2(sK105,sK105,X0),sK105)
| ~ l1_orders_2(sK105) )
| ~ spl290_133
| ~ spl290_134
| ~ spl290_135
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138 ),
inference(forward_subsumption_resolution,[],[f15007,f14883]) ).
fof(f15009,plain,
( ! [X0] :
( ~ v4_waybel_0(k2_yellow_2(sK105,sK105,X0),sK105)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK105),u1_struct_0(sK105))
| ~ v7_waybel_1(X0,sK105)
| ~ m2_relset_1(X0,u1_struct_0(sK105),u1_struct_0(sK105))
| v22_waybel_0(k3_waybel_1(sK105,sK105,X0),k2_yellow_2(sK105,sK105,X0),sK105) )
| ~ spl290_132
| ~ spl290_133
| ~ spl290_134
| ~ spl290_135
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138 ),
inference(forward_subsumption_resolution,[],[f15008,f14873]) ).
fof(f15010,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF289,sF289)
| ~ v4_waybel_0(k2_yellow_2(sK105,sK105,X0),sK105)
| ~ v1_funct_1(X0)
| ~ v7_waybel_1(X0,sK105)
| ~ m2_relset_1(X0,u1_struct_0(sK105),u1_struct_0(sK105))
| v22_waybel_0(k3_waybel_1(sK105,sK105,X0),k2_yellow_2(sK105,sK105,X0),sK105) )
| ~ spl290_132
| ~ spl290_133
| ~ spl290_134
| ~ spl290_135
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138
| ~ spl290_147 ),
inference(forward_demodulation,[],[f15009,f14957]) ).
fof(f15011,plain,
( ! [X0] :
( v22_waybel_0(k3_waybel_1(sK105,sK105,X0),k2_yellow_2(sK105,sK105,X0),sK105)
| ~ v1_funct_2(X0,sF289,sF289)
| ~ v4_waybel_0(k2_yellow_2(sK105,sK105,X0),sK105)
| ~ v1_funct_1(X0)
| ~ v7_waybel_1(X0,sK105)
| ~ m2_relset_1(X0,sF289,sF289) )
| ~ spl290_132
| ~ spl290_133
| ~ spl290_134
| ~ spl290_135
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138
| ~ spl290_147 ),
inference(forward_demodulation,[],[f15010,f14957]) ).
fof(f15012,plain,
( v22_waybel_0(k3_waybel_1(sK105,sK105,sK106),sF288,sK105)
| ~ v1_funct_2(sK106,sF289,sF289)
| ~ v4_waybel_0(sF288,sK105)
| ~ v1_funct_1(sK106)
| ~ v7_waybel_1(sK106,sK105)
| ~ m2_relset_1(sK106,sF289,sF289)
| ~ spl290_132
| ~ spl290_133
| ~ spl290_134
| ~ spl290_135
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138
| ~ spl290_146
| ~ spl290_147 ),
inference(superposition,[],[f15011,f14952]) ).
fof(f15013,plain,
( v22_waybel_0(k3_waybel_1(sK105,sK105,sK106),sF288,sK105)
| ~ v4_waybel_0(sF288,sK105)
| ~ v1_funct_1(sK106)
| ~ v7_waybel_1(sK106,sK105)
| ~ m2_relset_1(sK106,sF289,sF289)
| ~ spl290_132
| ~ spl290_133
| ~ spl290_134
| ~ spl290_135
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138
| ~ spl290_141
| ~ spl290_146
| ~ spl290_147 ),
inference(forward_subsumption_resolution,[],[f15012,f14918]) ).
fof(f15014,plain,
( v22_waybel_0(k3_waybel_1(sK105,sK105,sK106),sF288,sK105)
| ~ v1_funct_1(sK106)
| ~ v7_waybel_1(sK106,sK105)
| ~ m2_relset_1(sK106,sF289,sF289)
| ~ spl290_132
| ~ spl290_133
| ~ spl290_134
| ~ spl290_135
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138
| ~ spl290_141
| ~ spl290_143
| ~ spl290_146
| ~ spl290_147 ),
inference(forward_subsumption_resolution,[],[f15013,f14928]) ).
fof(f15015,plain,
( v22_waybel_0(k3_waybel_1(sK105,sK105,sK106),sF288,sK105)
| ~ v7_waybel_1(sK106,sK105)
| ~ m2_relset_1(sK106,sF289,sF289)
| ~ spl290_132
| ~ spl290_133
| ~ spl290_134
| ~ spl290_135
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138
| ~ spl290_141
| ~ spl290_142
| ~ spl290_143
| ~ spl290_146
| ~ spl290_147 ),
inference(forward_subsumption_resolution,[],[f15014,f14923]) ).
fof(f15016,plain,
( v22_waybel_0(k3_waybel_1(sK105,sK105,sK106),sF288,sK105)
| ~ m2_relset_1(sK106,sF289,sF289)
| ~ spl290_132
| ~ spl290_133
| ~ spl290_134
| ~ spl290_135
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138
| ~ spl290_140
| ~ spl290_141
| ~ spl290_142
| ~ spl290_143
| ~ spl290_146
| ~ spl290_147 ),
inference(forward_subsumption_resolution,[],[f15015,f14913]) ).
fof(f15017,plain,
( v22_waybel_0(k3_waybel_1(sK105,sK105,sK106),sF288,sK105)
| ~ spl290_132
| ~ spl290_133
| ~ spl290_134
| ~ spl290_135
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138
| ~ spl290_139
| ~ spl290_140
| ~ spl290_141
| ~ spl290_142
| ~ spl290_143
| ~ spl290_146
| ~ spl290_147 ),
inference(forward_subsumption_resolution,[],[f15016,f14908]) ).
fof(f15019,definition,
( spl290_148
<=> v22_waybel_0(k3_waybel_1(sK105,sK105,sK106),sF288,sK105) ),
introduced(definition,[new_symbols(definition,[spl290_148])],[avatar_definition]) ).
fof(f15021,plain,
( v22_waybel_0(k3_waybel_1(sK105,sK105,sK106),sF288,sK105)
| ~ spl290_148 ),
inference(avatar_component_clause,[],[f15019]) ).
fof(f15022,plain,
( spl290_148
| ~ spl290_132
| ~ spl290_133
| ~ spl290_134
| ~ spl290_135
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138
| ~ spl290_139
| ~ spl290_140
| ~ spl290_141
| ~ spl290_142
| ~ spl290_143
| ~ spl290_146
| ~ spl290_147 ),
inference(avatar_split_clause,[],[f15017,f14955,f14950,f14926,f14921,f14916,f14911,f14906,f14901,f14896,f14891,f14886,f14881,f14876,f14871,f15019]) ).
fof(f15023,plain,
( m1_relset_1(sK106,sF289,sF289)
| ~ spl290_139 ),
inference(unit_resulting_resolution,[],[f12467,f14908]) ).
fof(f15025,definition,
( spl290_149
<=> m1_relset_1(sK106,sF289,sF289) ),
introduced(definition,[new_symbols(definition,[spl290_149])],[avatar_definition]) ).
fof(f15027,plain,
( m1_relset_1(sK106,sF289,sF289)
| ~ spl290_149 ),
inference(avatar_component_clause,[],[f15025]) ).
fof(f15028,plain,
( spl290_149
| ~ spl290_139 ),
inference(avatar_split_clause,[],[f15023,f14906,f15025]) ).
fof(f15039,plain,
( ~ v3_struct_0(sK105)
| ~ spl290_132
| ~ spl290_134 ),
inference(unit_resulting_resolution,[],[f12475,f14873,f14883]) ).
fof(f15043,definition,
( spl290_150
<=> v3_struct_0(sK105) ),
introduced(definition,[new_symbols(definition,[spl290_150])],[avatar_definition]) ).
fof(f15045,plain,
( ~ v3_struct_0(sK105)
| spl290_150 ),
inference(avatar_component_clause,[],[f15043]) ).
fof(f15046,plain,
( ~ spl290_150
| ~ spl290_132
| ~ spl290_134 ),
inference(avatar_split_clause,[],[f15039,f14881,f14871,f15043]) ).
fof(f15053,plain,
( ! [X0,X1] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(sK105))
| ~ m2_relset_1(X0,u1_struct_0(X1),u1_struct_0(sK105))
| k2_waybel_1(X1,sK105,X0) = X0
| ~ l1_orders_2(sK105)
| v3_struct_0(X1)
| ~ l1_orders_2(X1) )
| spl290_150 ),
inference(resolution,[],[f15045,f14021]) ).
fof(f15058,plain,
( ! [X0,X1] :
( m2_relset_1(k3_waybel_1(sK105,X0,X1),u1_struct_0(k2_yellow_2(sK105,X0,X1)),u1_struct_0(X0))
| ~ l1_orders_2(sK105)
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK105),u1_struct_0(X0))
| ~ m1_relset_1(X1,u1_struct_0(sK105),u1_struct_0(X0)) )
| spl290_150 ),
inference(resolution,[],[f15045,f14030]) ).
fof(f15059,plain,
( ! [X0,X1] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(sK105))
| ~ m2_relset_1(X0,u1_struct_0(X1),u1_struct_0(sK105))
| k3_waybel_1(X1,sK105,X0) = k7_grcat_1(k2_yellow_2(X1,sK105,X0))
| ~ l1_orders_2(sK105)
| v3_struct_0(X1)
| ~ l1_orders_2(X1) )
| spl290_150 ),
inference(resolution,[],[f15045,f14038]) ).
fof(f15060,plain,
( ! [X0,X1] :
( v1_funct_2(k3_waybel_1(sK105,X0,X1),u1_struct_0(k2_yellow_2(sK105,X0,X1)),u1_struct_0(X0))
| ~ l1_orders_2(sK105)
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK105),u1_struct_0(X0))
| ~ m1_relset_1(X1,u1_struct_0(sK105),u1_struct_0(X0)) )
| spl290_150 ),
inference(resolution,[],[f15045,f14041]) ).
fof(f15061,plain,
( ! [X0,X1] :
( v1_funct_2(k3_waybel_1(sK105,X0,X1),u1_struct_0(k2_yellow_2(sK105,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(sK105),u1_struct_0(X0))
| ~ m1_relset_1(X1,u1_struct_0(sK105),u1_struct_0(X0)) )
| ~ spl290_132
| spl290_150 ),
inference(forward_subsumption_resolution,[],[f15060,f14873]) ).
fof(f15062,plain,
( ! [X0,X1] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(sK105))
| ~ m2_relset_1(X0,u1_struct_0(X1),u1_struct_0(sK105))
| k3_waybel_1(X1,sK105,X0) = k7_grcat_1(k2_yellow_2(X1,sK105,X0))
| v3_struct_0(X1)
| ~ l1_orders_2(X1) )
| ~ spl290_132
| spl290_150 ),
inference(forward_subsumption_resolution,[],[f15059,f14873]) ).
fof(f15063,plain,
( ! [X0,X1] :
( m2_relset_1(k3_waybel_1(sK105,X0,X1),u1_struct_0(k2_yellow_2(sK105,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(sK105),u1_struct_0(X0))
| ~ m1_relset_1(X1,u1_struct_0(sK105),u1_struct_0(X0)) )
| ~ spl290_132
| spl290_150 ),
inference(forward_subsumption_resolution,[],[f15058,f14873]) ).
fof(f15068,plain,
( ! [X0,X1] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(sK105))
| ~ m2_relset_1(X0,u1_struct_0(X1),u1_struct_0(sK105))
| k2_waybel_1(X1,sK105,X0) = X0
| v3_struct_0(X1)
| ~ l1_orders_2(X1) )
| ~ spl290_132
| spl290_150 ),
inference(forward_subsumption_resolution,[],[f15053,f14873]) ).
fof(f15075,plain,
( ! [X0,X1] :
( ~ v1_funct_2(X1,sF289,u1_struct_0(X0))
| v1_funct_2(k3_waybel_1(sK105,X0,X1),u1_struct_0(k2_yellow_2(sK105,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(sK105),u1_struct_0(X0)) )
| ~ spl290_132
| ~ spl290_147
| spl290_150 ),
inference(forward_demodulation,[],[f15061,f14957]) ).
fof(f15076,plain,
( ! [X0,X1] :
( ~ v1_funct_2(X0,u1_struct_0(X1),sF289)
| ~ v1_funct_1(X0)
| ~ m2_relset_1(X0,u1_struct_0(X1),u1_struct_0(sK105))
| k3_waybel_1(X1,sK105,X0) = k7_grcat_1(k2_yellow_2(X1,sK105,X0))
| v3_struct_0(X1)
| ~ l1_orders_2(X1) )
| ~ spl290_132
| ~ spl290_147
| spl290_150 ),
inference(forward_demodulation,[],[f15062,f14957]) ).
fof(f15077,plain,
( ! [X0,X1] :
( ~ v1_funct_2(X1,sF289,u1_struct_0(X0))
| m2_relset_1(k3_waybel_1(sK105,X0,X1),u1_struct_0(k2_yellow_2(sK105,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(sK105),u1_struct_0(X0)) )
| ~ spl290_132
| ~ spl290_147
| spl290_150 ),
inference(forward_demodulation,[],[f15063,f14957]) ).
fof(f15082,plain,
( ! [X0,X1] :
( ~ v1_funct_2(X0,u1_struct_0(X1),sF289)
| ~ v1_funct_1(X0)
| ~ m2_relset_1(X0,u1_struct_0(X1),u1_struct_0(sK105))
| k2_waybel_1(X1,sK105,X0) = X0
| v3_struct_0(X1)
| ~ l1_orders_2(X1) )
| ~ spl290_132
| ~ spl290_147
| spl290_150 ),
inference(forward_demodulation,[],[f15068,f14957]) ).
fof(f15089,plain,
( ! [X0,X1] :
( ~ l1_orders_2(X0)
| ~ v1_funct_2(X1,sF289,u1_struct_0(X0))
| v1_funct_2(k3_waybel_1(sK105,X0,X1),u1_struct_0(k2_yellow_2(sK105,X0,X1)),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ m1_relset_1(X1,sF289,u1_struct_0(X0))
| ~ v1_funct_1(X1) )
| ~ spl290_132
| ~ spl290_147
| spl290_150 ),
inference(forward_demodulation,[],[f15075,f14957]) ).
fof(f15090,plain,
( ! [X0,X1] :
( ~ l1_orders_2(X1)
| ~ v1_funct_2(X0,u1_struct_0(X1),sF289)
| ~ v1_funct_1(X0)
| k3_waybel_1(X1,sK105,X0) = k7_grcat_1(k2_yellow_2(X1,sK105,X0))
| v3_struct_0(X1)
| ~ m2_relset_1(X0,u1_struct_0(X1),sF289) )
| ~ spl290_132
| ~ spl290_147
| spl290_150 ),
inference(forward_demodulation,[],[f15076,f14957]) ).
fof(f15091,plain,
( ! [X0,X1] :
( ~ l1_orders_2(X0)
| ~ v1_funct_2(X1,sF289,u1_struct_0(X0))
| m2_relset_1(k3_waybel_1(sK105,X0,X1),u1_struct_0(k2_yellow_2(sK105,X0,X1)),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ m1_relset_1(X1,sF289,u1_struct_0(X0))
| ~ v1_funct_1(X1) )
| ~ spl290_132
| ~ spl290_147
| spl290_150 ),
inference(forward_demodulation,[],[f15077,f14957]) ).
fof(f15096,plain,
( ! [X0,X1] :
( ~ l1_orders_2(X1)
| ~ v1_funct_2(X0,u1_struct_0(X1),sF289)
| ~ v1_funct_1(X0)
| k2_waybel_1(X1,sK105,X0) = X0
| v3_struct_0(X1)
| ~ m2_relset_1(X0,u1_struct_0(X1),sF289) )
| ~ spl290_132
| ~ spl290_147
| spl290_150 ),
inference(forward_demodulation,[],[f15082,f14957]) ).
fof(f15108,plain,
( ! [X0] :
( ~ v1_funct_2(X0,u1_struct_0(sK105),sF289)
| ~ v1_funct_1(X0)
| k2_waybel_1(sK105,sK105,X0) = X0
| v3_struct_0(sK105)
| ~ m2_relset_1(X0,u1_struct_0(sK105),sF289) )
| ~ spl290_132
| ~ spl290_147
| spl290_150 ),
inference(resolution,[],[f15096,f14873]) ).
fof(f15109,plain,
( ! [X0] :
( ~ v1_funct_2(X0,u1_struct_0(sK105),sF289)
| ~ v1_funct_1(X0)
| k2_waybel_1(sK105,sK105,X0) = X0
| ~ m2_relset_1(X0,u1_struct_0(sK105),sF289) )
| ~ spl290_132
| ~ spl290_147
| spl290_150 ),
inference(forward_subsumption_resolution,[],[f15108,f15045]) ).
fof(f15110,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF289,sF289)
| ~ v1_funct_1(X0)
| k2_waybel_1(sK105,sK105,X0) = X0
| ~ m2_relset_1(X0,u1_struct_0(sK105),sF289) )
| ~ spl290_132
| ~ spl290_147
| spl290_150 ),
inference(forward_demodulation,[],[f15109,f14957]) ).
fof(f15111,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF289,sF289)
| ~ m2_relset_1(X0,sF289,sF289)
| ~ v1_funct_1(X0)
| k2_waybel_1(sK105,sK105,X0) = X0 )
| ~ spl290_132
| ~ spl290_147
| spl290_150 ),
inference(forward_demodulation,[],[f15110,f14957]) ).
fof(f15112,plain,
( sK106 = k2_waybel_1(sK105,sK105,sK106)
| ~ spl290_132
| ~ spl290_139
| ~ spl290_141
| ~ spl290_142
| ~ spl290_147
| spl290_150 ),
inference(unit_resulting_resolution,[],[f15111,f14923,f14918,f14908]) ).
fof(f15116,definition,
( spl290_151
<=> sK106 = k2_waybel_1(sK105,sK105,sK106) ),
introduced(definition,[new_symbols(definition,[spl290_151])],[avatar_definition]) ).
fof(f15118,plain,
( sK106 = k2_waybel_1(sK105,sK105,sK106)
| ~ spl290_151 ),
inference(avatar_component_clause,[],[f15116]) ).
fof(f15119,plain,
( spl290_151
| ~ spl290_132
| ~ spl290_139
| ~ spl290_141
| ~ spl290_142
| ~ spl290_147
| spl290_150 ),
inference(avatar_split_clause,[],[f15112,f15043,f14955,f14921,f14916,f14906,f14871,f15116]) ).
fof(f15122,plain,
( sK106 = sF287
| ~ spl290_145
| ~ spl290_151 ),
inference(superposition,[],[f14947,f15118]) ).
fof(f15124,definition,
( spl290_152
<=> sK106 = sF287 ),
introduced(definition,[new_symbols(definition,[spl290_152])],[avatar_definition]) ).
fof(f15126,plain,
( sK106 = sF287
| ~ spl290_152 ),
inference(avatar_component_clause,[],[f15124]) ).
fof(f15127,plain,
( spl290_152
| ~ spl290_145
| ~ spl290_151 ),
inference(avatar_split_clause,[],[f15122,f15116,f14945,f15124]) ).
fof(f15128,plain,
( ~ v1_waybel34(sK106,sK105,sF288)
| spl290_144
| ~ spl290_152 ),
inference(superposition,[],[f14933,f15126]) ).
fof(f15130,definition,
( spl290_153
<=> v1_waybel34(sK106,sK105,sF288) ),
introduced(definition,[new_symbols(definition,[spl290_153])],[avatar_definition]) ).
fof(f15132,plain,
( ~ v1_waybel34(sK106,sK105,sF288)
| spl290_153 ),
inference(avatar_component_clause,[],[f15130]) ).
fof(f15133,plain,
( ~ spl290_153
| spl290_144
| ~ spl290_152 ),
inference(avatar_split_clause,[],[f15128,f15124,f14931,f15130]) ).
fof(f15170,definition,
( spl290_155
<=> l1_orders_2(sF288) ),
introduced(definition,[new_symbols(definition,[spl290_155])],[avatar_definition]) ).
fof(f15171,plain,
( l1_orders_2(sF288)
| ~ spl290_155 ),
inference(avatar_component_clause,[],[f15170]) ).
fof(f15172,plain,
( ~ l1_orders_2(sF288)
| spl290_155 ),
inference(avatar_component_clause,[],[f15170]) ).
fof(f15218,definition,
( spl290_167
<=> v2_orders_2(sF288) ),
introduced(definition,[new_symbols(definition,[spl290_167])],[avatar_definition]) ).
fof(f15219,plain,
( v2_orders_2(sF288)
| ~ spl290_167 ),
inference(avatar_component_clause,[],[f15218]) ).
fof(f15238,plain,
( ! [X0] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK105),u1_struct_0(sK105))
| ~ v7_waybel_1(X0,sK105)
| ~ m2_relset_1(X0,u1_struct_0(sK105),u1_struct_0(sK105))
| ~ v2_orders_2(sK105)
| ~ v3_orders_2(sK105)
| ~ v4_orders_2(sK105)
| ~ v1_lattice3(sK105)
| ~ v2_lattice3(sK105)
| v17_waybel_0(k3_waybel_1(sK105,sK105,X0),k2_yellow_2(sK105,sK105,X0),sK105)
| ~ l1_orders_2(sK105) )
| ~ spl290_133 ),
inference(resolution,[],[f12430,f14878]) ).
fof(f15239,plain,
( ! [X0] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK105),u1_struct_0(sK105))
| ~ v7_waybel_1(X0,sK105)
| ~ m2_relset_1(X0,u1_struct_0(sK105),u1_struct_0(sK105))
| ~ v3_orders_2(sK105)
| ~ v4_orders_2(sK105)
| ~ v1_lattice3(sK105)
| ~ v2_lattice3(sK105)
| v17_waybel_0(k3_waybel_1(sK105,sK105,X0),k2_yellow_2(sK105,sK105,X0),sK105)
| ~ l1_orders_2(sK105) )
| ~ spl290_133
| ~ spl290_138 ),
inference(forward_subsumption_resolution,[],[f15238,f14903]) ).
fof(f15240,plain,
( ! [X0] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK105),u1_struct_0(sK105))
| ~ v7_waybel_1(X0,sK105)
| ~ m2_relset_1(X0,u1_struct_0(sK105),u1_struct_0(sK105))
| ~ v4_orders_2(sK105)
| ~ v1_lattice3(sK105)
| ~ v2_lattice3(sK105)
| v17_waybel_0(k3_waybel_1(sK105,sK105,X0),k2_yellow_2(sK105,sK105,X0),sK105)
| ~ l1_orders_2(sK105) )
| ~ spl290_133
| ~ spl290_137
| ~ spl290_138 ),
inference(forward_subsumption_resolution,[],[f15239,f14898]) ).
fof(f15241,plain,
( ! [X0] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK105),u1_struct_0(sK105))
| ~ v7_waybel_1(X0,sK105)
| ~ m2_relset_1(X0,u1_struct_0(sK105),u1_struct_0(sK105))
| ~ v1_lattice3(sK105)
| ~ v2_lattice3(sK105)
| v17_waybel_0(k3_waybel_1(sK105,sK105,X0),k2_yellow_2(sK105,sK105,X0),sK105)
| ~ l1_orders_2(sK105) )
| ~ spl290_133
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138 ),
inference(forward_subsumption_resolution,[],[f15240,f14893]) ).
fof(f15242,plain,
( ! [X0] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK105),u1_struct_0(sK105))
| ~ v7_waybel_1(X0,sK105)
| ~ m2_relset_1(X0,u1_struct_0(sK105),u1_struct_0(sK105))
| ~ v2_lattice3(sK105)
| v17_waybel_0(k3_waybel_1(sK105,sK105,X0),k2_yellow_2(sK105,sK105,X0),sK105)
| ~ l1_orders_2(sK105) )
| ~ spl290_133
| ~ spl290_135
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138 ),
inference(forward_subsumption_resolution,[],[f15241,f14888]) ).
fof(f15243,plain,
( ! [X0] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK105),u1_struct_0(sK105))
| ~ v7_waybel_1(X0,sK105)
| ~ m2_relset_1(X0,u1_struct_0(sK105),u1_struct_0(sK105))
| v17_waybel_0(k3_waybel_1(sK105,sK105,X0),k2_yellow_2(sK105,sK105,X0),sK105)
| ~ l1_orders_2(sK105) )
| ~ spl290_133
| ~ spl290_134
| ~ spl290_135
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138 ),
inference(forward_subsumption_resolution,[],[f15242,f14883]) ).
fof(f15244,plain,
( ! [X0] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK105),u1_struct_0(sK105))
| ~ v7_waybel_1(X0,sK105)
| ~ m2_relset_1(X0,u1_struct_0(sK105),u1_struct_0(sK105))
| v17_waybel_0(k3_waybel_1(sK105,sK105,X0),k2_yellow_2(sK105,sK105,X0),sK105) )
| ~ spl290_132
| ~ spl290_133
| ~ spl290_134
| ~ spl290_135
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138 ),
inference(forward_subsumption_resolution,[],[f15243,f14873]) ).
fof(f15245,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF289,sF289)
| ~ v1_funct_1(X0)
| ~ v7_waybel_1(X0,sK105)
| ~ m2_relset_1(X0,u1_struct_0(sK105),u1_struct_0(sK105))
| v17_waybel_0(k3_waybel_1(sK105,sK105,X0),k2_yellow_2(sK105,sK105,X0),sK105) )
| ~ spl290_132
| ~ spl290_133
| ~ spl290_134
| ~ spl290_135
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138
| ~ spl290_147 ),
inference(forward_demodulation,[],[f15244,f14957]) ).
fof(f15246,plain,
( ! [X0] :
( v17_waybel_0(k3_waybel_1(sK105,sK105,X0),k2_yellow_2(sK105,sK105,X0),sK105)
| ~ v1_funct_2(X0,sF289,sF289)
| ~ v1_funct_1(X0)
| ~ v7_waybel_1(X0,sK105)
| ~ m2_relset_1(X0,sF289,sF289) )
| ~ spl290_132
| ~ spl290_133
| ~ spl290_134
| ~ spl290_135
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138
| ~ spl290_147 ),
inference(forward_demodulation,[],[f15245,f14957]) ).
fof(f15247,plain,
( v17_waybel_0(k3_waybel_1(sK105,sK105,sK106),k2_yellow_2(sK105,sK105,sK106),sK105)
| ~ spl290_132
| ~ spl290_133
| ~ spl290_134
| ~ spl290_135
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138
| ~ spl290_139
| ~ spl290_140
| ~ spl290_141
| ~ spl290_142
| ~ spl290_147 ),
inference(unit_resulting_resolution,[],[f15246,f14923,f14913,f14908,f14918]) ).
fof(f15250,plain,
( v17_waybel_0(k3_waybel_1(sK105,sK105,sK106),sF288,sK105)
| ~ spl290_132
| ~ spl290_133
| ~ spl290_134
| ~ spl290_135
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138
| ~ spl290_139
| ~ spl290_140
| ~ spl290_141
| ~ spl290_142
| ~ spl290_146
| ~ spl290_147 ),
inference(forward_demodulation,[],[f15247,f14952]) ).
fof(f15253,definition,
( spl290_171
<=> v17_waybel_0(k3_waybel_1(sK105,sK105,sK106),sF288,sK105) ),
introduced(definition,[new_symbols(definition,[spl290_171])],[avatar_definition]) ).
fof(f15255,plain,
( v17_waybel_0(k3_waybel_1(sK105,sK105,sK106),sF288,sK105)
| ~ spl290_171 ),
inference(avatar_component_clause,[],[f15253]) ).
fof(f15256,plain,
( spl290_171
| ~ spl290_132
| ~ spl290_133
| ~ spl290_134
| ~ spl290_135
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138
| ~ spl290_139
| ~ spl290_140
| ~ spl290_141
| ~ spl290_142
| ~ spl290_146
| ~ spl290_147 ),
inference(avatar_split_clause,[],[f15250,f14955,f14950,f14921,f14916,f14911,f14906,f14901,f14896,f14891,f14886,f14881,f14876,f14871,f15253]) ).
fof(f15292,plain,
( ! [X0,X1] :
( v3_struct_0(sK105)
| m1_yellow_0(k2_yellow_2(sK105,X0,X1),X0)
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK105),u1_struct_0(X0))
| ~ m1_relset_1(X1,u1_struct_0(sK105),u1_struct_0(X0)) )
| ~ spl290_132 ),
inference(resolution,[],[f13807,f14873]) ).
fof(f15293,plain,
( ! [X0,X1] :
( m1_yellow_0(k2_yellow_2(sK105,X0,X1),X0)
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK105),u1_struct_0(X0))
| ~ m1_relset_1(X1,u1_struct_0(sK105),u1_struct_0(X0)) )
| ~ spl290_132
| spl290_150 ),
inference(forward_subsumption_resolution,[],[f15292,f15045]) ).
fof(f15294,plain,
( ! [X0,X1] :
( ~ v1_funct_2(X1,sF289,u1_struct_0(X0))
| m1_yellow_0(k2_yellow_2(sK105,X0,X1),X0)
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ m1_relset_1(X1,u1_struct_0(sK105),u1_struct_0(X0)) )
| ~ spl290_132
| ~ spl290_147
| spl290_150 ),
inference(forward_demodulation,[],[f15293,f14957]) ).
fof(f15295,plain,
( ! [X0,X1] :
( ~ l1_orders_2(X0)
| ~ v1_funct_2(X1,sF289,u1_struct_0(X0))
| m1_yellow_0(k2_yellow_2(sK105,X0,X1),X0)
| v3_struct_0(X0)
| ~ m1_relset_1(X1,sF289,u1_struct_0(X0))
| ~ v1_funct_1(X1) )
| ~ spl290_132
| ~ spl290_147
| spl290_150 ),
inference(forward_demodulation,[],[f15294,f14957]) ).
fof(f15296,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF289,u1_struct_0(sK105))
| m1_yellow_0(k2_yellow_2(sK105,sK105,X0),sK105)
| v3_struct_0(sK105)
| ~ m1_relset_1(X0,sF289,u1_struct_0(sK105))
| ~ v1_funct_1(X0) )
| ~ spl290_132
| ~ spl290_147
| spl290_150 ),
inference(resolution,[],[f15295,f14873]) ).
fof(f15297,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF289,u1_struct_0(sK105))
| m1_yellow_0(k2_yellow_2(sK105,sK105,X0),sK105)
| ~ m1_relset_1(X0,sF289,u1_struct_0(sK105))
| ~ v1_funct_1(X0) )
| ~ spl290_132
| ~ spl290_147
| spl290_150 ),
inference(forward_subsumption_resolution,[],[f15296,f15045]) ).
fof(f15298,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF289,sF289)
| m1_yellow_0(k2_yellow_2(sK105,sK105,X0),sK105)
| ~ m1_relset_1(X0,sF289,u1_struct_0(sK105))
| ~ v1_funct_1(X0) )
| ~ spl290_132
| ~ spl290_147
| spl290_150 ),
inference(forward_demodulation,[],[f15297,f14957]) ).
fof(f15299,plain,
( ! [X0] :
( m1_yellow_0(k2_yellow_2(sK105,sK105,X0),sK105)
| ~ v1_funct_2(X0,sF289,sF289)
| ~ m1_relset_1(X0,sF289,sF289)
| ~ v1_funct_1(X0) )
| ~ spl290_132
| ~ spl290_147
| spl290_150 ),
inference(forward_demodulation,[],[f15298,f14957]) ).
fof(f15300,plain,
( m1_yellow_0(k2_yellow_2(sK105,sK105,sK106),sK105)
| ~ spl290_132
| ~ spl290_141
| ~ spl290_142
| ~ spl290_147
| ~ spl290_149
| spl290_150 ),
inference(unit_resulting_resolution,[],[f15299,f14923,f15027,f14918]) ).
fof(f15303,plain,
( m1_yellow_0(sF288,sK105)
| ~ spl290_132
| ~ spl290_141
| ~ spl290_142
| ~ spl290_146
| ~ spl290_147
| ~ spl290_149
| spl290_150 ),
inference(forward_demodulation,[],[f15300,f14952]) ).
fof(f15306,definition,
( spl290_173
<=> m1_yellow_0(sF288,sK105) ),
introduced(definition,[new_symbols(definition,[spl290_173])],[avatar_definition]) ).
fof(f15308,plain,
( m1_yellow_0(sF288,sK105)
| ~ spl290_173 ),
inference(avatar_component_clause,[],[f15306]) ).
fof(f15309,plain,
( spl290_173
| ~ spl290_132
| ~ spl290_141
| ~ spl290_142
| ~ spl290_146
| ~ spl290_147
| ~ spl290_149
| spl290_150 ),
inference(avatar_split_clause,[],[f15303,f15043,f15025,f14955,f14950,f14921,f14916,f14871,f15306]) ).
fof(f15361,plain,
( ! [X0] :
( ~ v1_funct_2(X0,u1_struct_0(sK105),sF289)
| ~ v1_funct_1(X0)
| k3_waybel_1(sK105,sK105,X0) = k7_grcat_1(k2_yellow_2(sK105,sK105,X0))
| v3_struct_0(sK105)
| ~ m2_relset_1(X0,u1_struct_0(sK105),sF289) )
| ~ spl290_132
| ~ spl290_147
| spl290_150 ),
inference(resolution,[],[f15090,f14873]) ).
fof(f15362,plain,
( ! [X0] :
( ~ v1_funct_2(X0,u1_struct_0(sK105),sF289)
| ~ v1_funct_1(X0)
| k3_waybel_1(sK105,sK105,X0) = k7_grcat_1(k2_yellow_2(sK105,sK105,X0))
| ~ m2_relset_1(X0,u1_struct_0(sK105),sF289) )
| ~ spl290_132
| ~ spl290_147
| spl290_150 ),
inference(forward_subsumption_resolution,[],[f15361,f15045]) ).
fof(f15363,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF289,sF289)
| ~ v1_funct_1(X0)
| k3_waybel_1(sK105,sK105,X0) = k7_grcat_1(k2_yellow_2(sK105,sK105,X0))
| ~ m2_relset_1(X0,u1_struct_0(sK105),sF289) )
| ~ spl290_132
| ~ spl290_147
| spl290_150 ),
inference(forward_demodulation,[],[f15362,f14957]) ).
fof(f15364,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF289,sF289)
| ~ m2_relset_1(X0,sF289,sF289)
| ~ v1_funct_1(X0)
| k3_waybel_1(sK105,sK105,X0) = k7_grcat_1(k2_yellow_2(sK105,sK105,X0)) )
| ~ spl290_132
| ~ spl290_147
| spl290_150 ),
inference(forward_demodulation,[],[f15363,f14957]) ).
fof(f15365,plain,
( k3_waybel_1(sK105,sK105,sK106) = k7_grcat_1(k2_yellow_2(sK105,sK105,sK106))
| ~ spl290_132
| ~ spl290_139
| ~ spl290_141
| ~ spl290_142
| ~ spl290_147
| spl290_150 ),
inference(unit_resulting_resolution,[],[f15364,f14923,f14918,f14908]) ).
fof(f15368,plain,
( k3_waybel_1(sK105,sK105,sK106) = k7_grcat_1(sF288)
| ~ spl290_132
| ~ spl290_139
| ~ spl290_141
| ~ spl290_142
| ~ spl290_146
| ~ spl290_147
| spl290_150 ),
inference(forward_demodulation,[],[f15365,f14952]) ).
fof(f15371,definition,
( spl290_176
<=> k3_waybel_1(sK105,sK105,sK106) = k7_grcat_1(sF288) ),
introduced(definition,[new_symbols(definition,[spl290_176])],[avatar_definition]) ).
fof(f15373,plain,
( k3_waybel_1(sK105,sK105,sK106) = k7_grcat_1(sF288)
| ~ spl290_176 ),
inference(avatar_component_clause,[],[f15371]) ).
fof(f15374,plain,
( spl290_176
| ~ spl290_132
| ~ spl290_139
| ~ spl290_141
| ~ spl290_142
| ~ spl290_146
| ~ spl290_147
| spl290_150 ),
inference(avatar_split_clause,[],[f15368,f15043,f14955,f14950,f14921,f14916,f14906,f14871,f15371]) ).
fof(f15376,plain,
( v17_waybel_0(k7_grcat_1(sF288),sF288,sK105)
| ~ spl290_171
| ~ spl290_176 ),
inference(superposition,[],[f15255,f15373]) ).
fof(f15377,plain,
( v22_waybel_0(k7_grcat_1(sF288),sF288,sK105)
| ~ spl290_148
| ~ spl290_176 ),
inference(superposition,[],[f15021,f15373]) ).
fof(f15383,definition,
( spl290_177
<=> v22_waybel_0(k7_grcat_1(sF288),sF288,sK105) ),
introduced(definition,[new_symbols(definition,[spl290_177])],[avatar_definition]) ).
fof(f15385,plain,
( v22_waybel_0(k7_grcat_1(sF288),sF288,sK105)
| ~ spl290_177 ),
inference(avatar_component_clause,[],[f15383]) ).
fof(f15386,plain,
( spl290_177
| ~ spl290_148
| ~ spl290_176 ),
inference(avatar_split_clause,[],[f15377,f15371,f15019,f15383]) ).
fof(f15388,definition,
( spl290_178
<=> v17_waybel_0(k7_grcat_1(sF288),sF288,sK105) ),
introduced(definition,[new_symbols(definition,[spl290_178])],[avatar_definition]) ).
fof(f15390,plain,
( v17_waybel_0(k7_grcat_1(sF288),sF288,sK105)
| ~ spl290_178 ),
inference(avatar_component_clause,[],[f15388]) ).
fof(f15391,plain,
( spl290_178
| ~ spl290_171
| ~ spl290_176 ),
inference(avatar_split_clause,[],[f15376,f15371,f15253,f15388]) ).
fof(f15549,plain,
( ! [X0] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK105),u1_struct_0(sK105))
| ~ v7_waybel_1(X0,sK105)
| ~ m2_relset_1(X0,u1_struct_0(sK105),u1_struct_0(sK105))
| ~ v2_orders_2(sK105)
| ~ v3_orders_2(sK105)
| ~ v4_orders_2(sK105)
| ~ v1_lattice3(sK105)
| ~ v2_lattice3(sK105)
| k2_waybel_1(sK105,sK105,X0) = k1_waybel34(k2_yellow_2(sK105,sK105,X0),sK105,k3_waybel_1(sK105,sK105,X0))
| ~ l1_orders_2(sK105) )
| ~ spl290_133 ),
inference(resolution,[],[f12428,f14878]) ).
fof(f15550,plain,
( ! [X0] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK105),u1_struct_0(sK105))
| ~ v7_waybel_1(X0,sK105)
| ~ m2_relset_1(X0,u1_struct_0(sK105),u1_struct_0(sK105))
| ~ v3_orders_2(sK105)
| ~ v4_orders_2(sK105)
| ~ v1_lattice3(sK105)
| ~ v2_lattice3(sK105)
| k2_waybel_1(sK105,sK105,X0) = k1_waybel34(k2_yellow_2(sK105,sK105,X0),sK105,k3_waybel_1(sK105,sK105,X0))
| ~ l1_orders_2(sK105) )
| ~ spl290_133
| ~ spl290_138 ),
inference(forward_subsumption_resolution,[],[f15549,f14903]) ).
fof(f15551,plain,
( ! [X0] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK105),u1_struct_0(sK105))
| ~ v7_waybel_1(X0,sK105)
| ~ m2_relset_1(X0,u1_struct_0(sK105),u1_struct_0(sK105))
| ~ v4_orders_2(sK105)
| ~ v1_lattice3(sK105)
| ~ v2_lattice3(sK105)
| k2_waybel_1(sK105,sK105,X0) = k1_waybel34(k2_yellow_2(sK105,sK105,X0),sK105,k3_waybel_1(sK105,sK105,X0))
| ~ l1_orders_2(sK105) )
| ~ spl290_133
| ~ spl290_137
| ~ spl290_138 ),
inference(forward_subsumption_resolution,[],[f15550,f14898]) ).
fof(f15552,plain,
( ! [X0] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK105),u1_struct_0(sK105))
| ~ v7_waybel_1(X0,sK105)
| ~ m2_relset_1(X0,u1_struct_0(sK105),u1_struct_0(sK105))
| ~ v1_lattice3(sK105)
| ~ v2_lattice3(sK105)
| k2_waybel_1(sK105,sK105,X0) = k1_waybel34(k2_yellow_2(sK105,sK105,X0),sK105,k3_waybel_1(sK105,sK105,X0))
| ~ l1_orders_2(sK105) )
| ~ spl290_133
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138 ),
inference(forward_subsumption_resolution,[],[f15551,f14893]) ).
fof(f15553,plain,
( ! [X0] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK105),u1_struct_0(sK105))
| ~ v7_waybel_1(X0,sK105)
| ~ m2_relset_1(X0,u1_struct_0(sK105),u1_struct_0(sK105))
| ~ v2_lattice3(sK105)
| k2_waybel_1(sK105,sK105,X0) = k1_waybel34(k2_yellow_2(sK105,sK105,X0),sK105,k3_waybel_1(sK105,sK105,X0))
| ~ l1_orders_2(sK105) )
| ~ spl290_133
| ~ spl290_135
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138 ),
inference(forward_subsumption_resolution,[],[f15552,f14888]) ).
fof(f15554,plain,
( ! [X0] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK105),u1_struct_0(sK105))
| ~ v7_waybel_1(X0,sK105)
| ~ m2_relset_1(X0,u1_struct_0(sK105),u1_struct_0(sK105))
| k2_waybel_1(sK105,sK105,X0) = k1_waybel34(k2_yellow_2(sK105,sK105,X0),sK105,k3_waybel_1(sK105,sK105,X0))
| ~ l1_orders_2(sK105) )
| ~ spl290_133
| ~ spl290_134
| ~ spl290_135
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138 ),
inference(forward_subsumption_resolution,[],[f15553,f14883]) ).
fof(f15555,plain,
( ! [X0] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK105),u1_struct_0(sK105))
| ~ v7_waybel_1(X0,sK105)
| ~ m2_relset_1(X0,u1_struct_0(sK105),u1_struct_0(sK105))
| k2_waybel_1(sK105,sK105,X0) = k1_waybel34(k2_yellow_2(sK105,sK105,X0),sK105,k3_waybel_1(sK105,sK105,X0)) )
| ~ spl290_132
| ~ spl290_133
| ~ spl290_134
| ~ spl290_135
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138 ),
inference(forward_subsumption_resolution,[],[f15554,f14873]) ).
fof(f15556,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF289,sF289)
| ~ v1_funct_1(X0)
| ~ v7_waybel_1(X0,sK105)
| ~ m2_relset_1(X0,u1_struct_0(sK105),u1_struct_0(sK105))
| k2_waybel_1(sK105,sK105,X0) = k1_waybel34(k2_yellow_2(sK105,sK105,X0),sK105,k3_waybel_1(sK105,sK105,X0)) )
| ~ spl290_132
| ~ spl290_133
| ~ spl290_134
| ~ spl290_135
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138
| ~ spl290_147 ),
inference(forward_demodulation,[],[f15555,f14957]) ).
fof(f15557,plain,
( ! [X0] :
( ~ v7_waybel_1(X0,sK105)
| ~ v1_funct_2(X0,sF289,sF289)
| ~ v1_funct_1(X0)
| ~ m2_relset_1(X0,sF289,sF289)
| k2_waybel_1(sK105,sK105,X0) = k1_waybel34(k2_yellow_2(sK105,sK105,X0),sK105,k3_waybel_1(sK105,sK105,X0)) )
| ~ spl290_132
| ~ spl290_133
| ~ spl290_134
| ~ spl290_135
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138
| ~ spl290_147 ),
inference(forward_demodulation,[],[f15556,f14957]) ).
fof(f15558,plain,
( k2_waybel_1(sK105,sK105,sK106) = k1_waybel34(k2_yellow_2(sK105,sK105,sK106),sK105,k3_waybel_1(sK105,sK105,sK106))
| ~ spl290_132
| ~ spl290_133
| ~ spl290_134
| ~ spl290_135
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138
| ~ spl290_139
| ~ spl290_140
| ~ spl290_141
| ~ spl290_142
| ~ spl290_147 ),
inference(unit_resulting_resolution,[],[f15557,f14923,f14913,f14908,f14918]) ).
fof(f15561,plain,
( k2_waybel_1(sK105,sK105,sK106) = k1_waybel34(k2_yellow_2(sK105,sK105,sK106),sK105,k7_grcat_1(sF288))
| ~ spl290_132
| ~ spl290_133
| ~ spl290_134
| ~ spl290_135
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138
| ~ spl290_139
| ~ spl290_140
| ~ spl290_141
| ~ spl290_142
| ~ spl290_147
| ~ spl290_176 ),
inference(forward_demodulation,[],[f15558,f15373]) ).
fof(f15563,plain,
( k2_waybel_1(sK105,sK105,sK106) = k1_waybel34(sF288,sK105,k7_grcat_1(sF288))
| ~ spl290_132
| ~ spl290_133
| ~ spl290_134
| ~ spl290_135
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138
| ~ spl290_139
| ~ spl290_140
| ~ spl290_141
| ~ spl290_142
| ~ spl290_146
| ~ spl290_147
| ~ spl290_176 ),
inference(forward_demodulation,[],[f15561,f14952]) ).
fof(f15565,plain,
( sF287 = k1_waybel34(sF288,sK105,k7_grcat_1(sF288))
| ~ spl290_132
| ~ spl290_133
| ~ spl290_134
| ~ spl290_135
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138
| ~ spl290_139
| ~ spl290_140
| ~ spl290_141
| ~ spl290_142
| ~ spl290_145
| ~ spl290_146
| ~ spl290_147
| ~ spl290_176 ),
inference(forward_demodulation,[],[f15563,f14947]) ).
fof(f15567,plain,
( sK106 = k1_waybel34(sF288,sK105,k7_grcat_1(sF288))
| ~ spl290_132
| ~ spl290_133
| ~ spl290_134
| ~ spl290_135
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138
| ~ spl290_139
| ~ spl290_140
| ~ spl290_141
| ~ spl290_142
| ~ spl290_145
| ~ spl290_146
| ~ spl290_147
| ~ spl290_152
| ~ spl290_176 ),
inference(forward_demodulation,[],[f15565,f15126]) ).
fof(f15570,definition,
( spl290_184
<=> sK106 = k1_waybel34(sF288,sK105,k7_grcat_1(sF288)) ),
introduced(definition,[new_symbols(definition,[spl290_184])],[avatar_definition]) ).
fof(f15572,plain,
( sK106 = k1_waybel34(sF288,sK105,k7_grcat_1(sF288))
| ~ spl290_184 ),
inference(avatar_component_clause,[],[f15570]) ).
fof(f15573,plain,
( spl290_184
| ~ spl290_132
| ~ spl290_133
| ~ spl290_134
| ~ spl290_135
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138
| ~ spl290_139
| ~ spl290_140
| ~ spl290_141
| ~ spl290_142
| ~ spl290_145
| ~ spl290_146
| ~ spl290_147
| ~ spl290_152
| ~ spl290_176 ),
inference(avatar_split_clause,[],[f15567,f15371,f15124,f14955,f14950,f14945,f14921,f14916,f14911,f14906,f14901,f14896,f14891,f14886,f14881,f14876,f14871,f15570]) ).
fof(f15610,plain,
( v1_waybel34(sK106,sK105,sF288)
| ~ v22_waybel_0(k7_grcat_1(sF288),sF288,sK105)
| ~ v1_funct_1(k7_grcat_1(sF288))
| ~ v1_funct_2(k7_grcat_1(sF288),u1_struct_0(sF288),u1_struct_0(sK105))
| ~ v17_waybel_0(k7_grcat_1(sF288),sF288,sK105)
| ~ m2_relset_1(k7_grcat_1(sF288),u1_struct_0(sF288),u1_struct_0(sK105))
| ~ v2_orders_2(sK105)
| ~ v3_orders_2(sK105)
| ~ v4_orders_2(sK105)
| ~ v1_lattice3(sK105)
| ~ v2_lattice3(sK105)
| ~ v3_lattice3(sK105)
| ~ l1_orders_2(sK105)
| ~ v2_orders_2(sF288)
| ~ v3_orders_2(sF288)
| ~ v4_orders_2(sF288)
| ~ v1_lattice3(sF288)
| ~ v2_lattice3(sF288)
| ~ v3_lattice3(sF288)
| ~ l1_orders_2(sF288)
| ~ spl290_184 ),
inference(superposition,[],[f12350,f15572]) ).
fof(f15662,plain,
( ! [X0] :
( ~ v2_orders_2(sK105)
| ~ v3_orders_2(sK105)
| ~ v4_orders_2(sK105)
| ~ v1_lattice3(sK105)
| ~ v2_lattice3(sK105)
| sP19(X0,sK105)
| ~ l1_orders_2(sK105)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK105),u1_struct_0(sK105))
| ~ v6_waybel_1(X0,sK105)
| ~ m1_relset_1(X0,u1_struct_0(sK105),u1_struct_0(sK105)) )
| ~ spl290_133 ),
inference(resolution,[],[f12397,f14878]) ).
fof(f15663,plain,
( ! [X0] :
( ~ v3_orders_2(sK105)
| ~ v4_orders_2(sK105)
| ~ v1_lattice3(sK105)
| ~ v2_lattice3(sK105)
| sP19(X0,sK105)
| ~ l1_orders_2(sK105)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK105),u1_struct_0(sK105))
| ~ v6_waybel_1(X0,sK105)
| ~ m1_relset_1(X0,u1_struct_0(sK105),u1_struct_0(sK105)) )
| ~ spl290_133
| ~ spl290_138 ),
inference(forward_subsumption_resolution,[],[f15662,f14903]) ).
fof(f15664,plain,
( ! [X0] :
( ~ v4_orders_2(sK105)
| ~ v1_lattice3(sK105)
| ~ v2_lattice3(sK105)
| sP19(X0,sK105)
| ~ l1_orders_2(sK105)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK105),u1_struct_0(sK105))
| ~ v6_waybel_1(X0,sK105)
| ~ m1_relset_1(X0,u1_struct_0(sK105),u1_struct_0(sK105)) )
| ~ spl290_133
| ~ spl290_137
| ~ spl290_138 ),
inference(forward_subsumption_resolution,[],[f15663,f14898]) ).
fof(f15665,plain,
( ! [X0] :
( ~ v1_lattice3(sK105)
| ~ v2_lattice3(sK105)
| sP19(X0,sK105)
| ~ l1_orders_2(sK105)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK105),u1_struct_0(sK105))
| ~ v6_waybel_1(X0,sK105)
| ~ m1_relset_1(X0,u1_struct_0(sK105),u1_struct_0(sK105)) )
| ~ spl290_133
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138 ),
inference(forward_subsumption_resolution,[],[f15664,f14893]) ).
fof(f15666,plain,
( ! [X0] :
( ~ v2_lattice3(sK105)
| sP19(X0,sK105)
| ~ l1_orders_2(sK105)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK105),u1_struct_0(sK105))
| ~ v6_waybel_1(X0,sK105)
| ~ m1_relset_1(X0,u1_struct_0(sK105),u1_struct_0(sK105)) )
| ~ spl290_133
| ~ spl290_135
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138 ),
inference(forward_subsumption_resolution,[],[f15665,f14888]) ).
fof(f15667,plain,
( ! [X0] :
( sP19(X0,sK105)
| ~ l1_orders_2(sK105)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK105),u1_struct_0(sK105))
| ~ v6_waybel_1(X0,sK105)
| ~ m1_relset_1(X0,u1_struct_0(sK105),u1_struct_0(sK105)) )
| ~ spl290_133
| ~ spl290_134
| ~ spl290_135
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138 ),
inference(forward_subsumption_resolution,[],[f15666,f14883]) ).
fof(f15668,plain,
( ! [X0] :
( sP19(X0,sK105)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK105),u1_struct_0(sK105))
| ~ v6_waybel_1(X0,sK105)
| ~ m1_relset_1(X0,u1_struct_0(sK105),u1_struct_0(sK105)) )
| ~ spl290_132
| ~ spl290_133
| ~ spl290_134
| ~ spl290_135
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138 ),
inference(forward_subsumption_resolution,[],[f15667,f14873]) ).
fof(f15669,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF289,sF289)
| sP19(X0,sK105)
| ~ v1_funct_1(X0)
| ~ v6_waybel_1(X0,sK105)
| ~ m1_relset_1(X0,u1_struct_0(sK105),u1_struct_0(sK105)) )
| ~ spl290_132
| ~ spl290_133
| ~ spl290_134
| ~ spl290_135
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138
| ~ spl290_147 ),
inference(forward_demodulation,[],[f15668,f14957]) ).
fof(f15670,plain,
( ! [X0] :
( ~ v6_waybel_1(X0,sK105)
| ~ v1_funct_2(X0,sF289,sF289)
| sP19(X0,sK105)
| ~ v1_funct_1(X0)
| ~ m1_relset_1(X0,sF289,sF289) )
| ~ spl290_132
| ~ spl290_133
| ~ spl290_134
| ~ spl290_135
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138
| ~ spl290_147 ),
inference(forward_demodulation,[],[f15669,f14957]) ).
fof(f15671,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF289,sF289)
| sP19(X0,sK105)
| ~ v1_funct_1(X0)
| ~ m1_relset_1(X0,sF289,sF289)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK105),u1_struct_0(sK105))
| ~ v7_waybel_1(X0,sK105)
| ~ m1_relset_1(X0,u1_struct_0(sK105),u1_struct_0(sK105))
| v3_struct_0(sK105)
| ~ l1_orders_2(sK105) )
| ~ spl290_132
| ~ spl290_133
| ~ spl290_134
| ~ spl290_135
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138
| ~ spl290_147 ),
inference(resolution,[],[f15670,f13955]) ).
fof(f15672,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF289,sF289)
| sP19(X0,sK105)
| ~ v1_funct_1(X0)
| ~ m1_relset_1(X0,sF289,sF289)
| ~ v1_funct_2(X0,u1_struct_0(sK105),u1_struct_0(sK105))
| ~ v7_waybel_1(X0,sK105)
| ~ m1_relset_1(X0,u1_struct_0(sK105),u1_struct_0(sK105))
| v3_struct_0(sK105)
| ~ l1_orders_2(sK105) )
| ~ spl290_132
| ~ spl290_133
| ~ spl290_134
| ~ spl290_135
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138
| ~ spl290_147 ),
inference(duplicate_literal_removal,[],[f15671]) ).
fof(f15673,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF289,sF289)
| sP19(X0,sK105)
| ~ v1_funct_1(X0)
| ~ m1_relset_1(X0,sF289,sF289)
| ~ v1_funct_2(X0,u1_struct_0(sK105),u1_struct_0(sK105))
| ~ v7_waybel_1(X0,sK105)
| ~ m1_relset_1(X0,u1_struct_0(sK105),u1_struct_0(sK105))
| ~ l1_orders_2(sK105) )
| ~ spl290_132
| ~ spl290_133
| ~ spl290_134
| ~ spl290_135
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138
| ~ spl290_147
| spl290_150 ),
inference(forward_subsumption_resolution,[],[f15672,f15045]) ).
fof(f15674,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF289,sF289)
| sP19(X0,sK105)
| ~ v1_funct_1(X0)
| ~ m1_relset_1(X0,sF289,sF289)
| ~ v1_funct_2(X0,u1_struct_0(sK105),u1_struct_0(sK105))
| ~ v7_waybel_1(X0,sK105)
| ~ m1_relset_1(X0,u1_struct_0(sK105),u1_struct_0(sK105)) )
| ~ spl290_132
| ~ spl290_133
| ~ spl290_134
| ~ spl290_135
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138
| ~ spl290_147
| spl290_150 ),
inference(forward_subsumption_resolution,[],[f15673,f14873]) ).
fof(f15675,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF289,sF289)
| ~ v1_funct_2(X0,sF289,sF289)
| sP19(X0,sK105)
| ~ v1_funct_1(X0)
| ~ m1_relset_1(X0,sF289,sF289)
| ~ v7_waybel_1(X0,sK105)
| ~ m1_relset_1(X0,u1_struct_0(sK105),u1_struct_0(sK105)) )
| ~ spl290_132
| ~ spl290_133
| ~ spl290_134
| ~ spl290_135
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138
| ~ spl290_147
| spl290_150 ),
inference(forward_demodulation,[],[f15674,f14957]) ).
fof(f15676,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF289,sF289)
| sP19(X0,sK105)
| ~ v1_funct_1(X0)
| ~ m1_relset_1(X0,sF289,sF289)
| ~ v7_waybel_1(X0,sK105)
| ~ m1_relset_1(X0,u1_struct_0(sK105),u1_struct_0(sK105)) )
| ~ spl290_132
| ~ spl290_133
| ~ spl290_134
| ~ spl290_135
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138
| ~ spl290_147
| spl290_150 ),
inference(duplicate_literal_removal,[],[f15675]) ).
fof(f15677,plain,
( ! [X0] :
( ~ m1_relset_1(X0,sF289,sF289)
| ~ v1_funct_2(X0,sF289,sF289)
| sP19(X0,sK105)
| ~ v1_funct_1(X0)
| ~ m1_relset_1(X0,sF289,sF289)
| ~ v7_waybel_1(X0,sK105) )
| ~ spl290_132
| ~ spl290_133
| ~ spl290_134
| ~ spl290_135
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138
| ~ spl290_147
| spl290_150 ),
inference(forward_demodulation,[],[f15676,f14957]) ).
fof(f15678,plain,
( ! [X0] :
( ~ v7_waybel_1(X0,sK105)
| ~ v1_funct_2(X0,sF289,sF289)
| sP19(X0,sK105)
| ~ v1_funct_1(X0)
| ~ m1_relset_1(X0,sF289,sF289) )
| ~ spl290_132
| ~ spl290_133
| ~ spl290_134
| ~ spl290_135
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138
| ~ spl290_147
| spl290_150 ),
inference(duplicate_literal_removal,[],[f15677]) ).
fof(f15763,plain,
( sP19(sK106,sK105)
| ~ spl290_132
| ~ spl290_133
| ~ spl290_134
| ~ spl290_135
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138
| ~ spl290_140
| ~ spl290_141
| ~ spl290_142
| ~ spl290_147
| ~ spl290_149
| spl290_150 ),
inference(unit_resulting_resolution,[],[f15678,f14923,f14913,f15027,f14918]) ).
fof(f15767,definition,
( spl290_195
<=> sP19(sK106,sK105) ),
introduced(definition,[new_symbols(definition,[spl290_195])],[avatar_definition]) ).
fof(f15769,plain,
( sP19(sK106,sK105)
| ~ spl290_195 ),
inference(avatar_component_clause,[],[f15767]) ).
fof(f15770,plain,
( spl290_195
| ~ spl290_132
| ~ spl290_133
| ~ spl290_134
| ~ spl290_135
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138
| ~ spl290_140
| ~ spl290_141
| ~ spl290_142
| ~ spl290_147
| ~ spl290_149
| spl290_150 ),
inference(avatar_split_clause,[],[f15763,f15043,f15025,f14955,f14921,f14916,f14911,f14901,f14896,f14891,f14886,f14881,f14876,f14871,f15767]) ).
fof(f15778,plain,
( v3_orders_2(k2_yellow_2(sK105,sK105,sK106))
| ~ spl290_195 ),
inference(resolution,[],[f15769,f12393]) ).
fof(f15779,plain,
( v1_lattice3(k2_yellow_2(sK105,sK105,sK106))
| ~ spl290_195 ),
inference(resolution,[],[f15769,f12385]) ).
fof(f15780,plain,
( v2_lattice3(k2_yellow_2(sK105,sK105,sK106))
| ~ spl290_195 ),
inference(resolution,[],[f15769,f12384]) ).
fof(f15781,plain,
( v3_lattice3(k2_yellow_2(sK105,sK105,sK106))
| ~ spl290_195 ),
inference(resolution,[],[f15769,f12383]) ).
fof(f15782,plain,
( v2_orders_2(k2_yellow_2(sK105,sK105,sK106))
| ~ spl290_195 ),
inference(resolution,[],[f15769,f12394]) ).
fof(f15783,plain,
( v2_orders_2(sF288)
| ~ spl290_146
| ~ spl290_195 ),
inference(forward_demodulation,[],[f15782,f14952]) ).
fof(f15784,plain,
( v3_lattice3(sF288)
| ~ spl290_146
| ~ spl290_195 ),
inference(forward_demodulation,[],[f15781,f14952]) ).
fof(f15785,plain,
( v2_lattice3(sF288)
| ~ spl290_146
| ~ spl290_195 ),
inference(forward_demodulation,[],[f15780,f14952]) ).
fof(f15786,plain,
( v1_lattice3(sF288)
| ~ spl290_146
| ~ spl290_195 ),
inference(forward_demodulation,[],[f15779,f14952]) ).
fof(f15787,plain,
( v3_orders_2(sF288)
| ~ spl290_146
| ~ spl290_195 ),
inference(forward_demodulation,[],[f15778,f14952]) ).
fof(f15793,plain,
( spl290_167
| ~ spl290_146
| ~ spl290_195 ),
inference(avatar_split_clause,[],[f15783,f15767,f14950,f15218]) ).
fof(f15795,definition,
( spl290_196
<=> v3_lattice3(sF288) ),
introduced(definition,[new_symbols(definition,[spl290_196])],[avatar_definition]) ).
fof(f15797,plain,
( v3_lattice3(sF288)
| ~ spl290_196 ),
inference(avatar_component_clause,[],[f15795]) ).
fof(f15798,plain,
( spl290_196
| ~ spl290_146
| ~ spl290_195 ),
inference(avatar_split_clause,[],[f15784,f15767,f14950,f15795]) ).
fof(f15800,definition,
( spl290_197
<=> v2_lattice3(sF288) ),
introduced(definition,[new_symbols(definition,[spl290_197])],[avatar_definition]) ).
fof(f15802,plain,
( v2_lattice3(sF288)
| ~ spl290_197 ),
inference(avatar_component_clause,[],[f15800]) ).
fof(f15803,plain,
( spl290_197
| ~ spl290_146
| ~ spl290_195 ),
inference(avatar_split_clause,[],[f15785,f15767,f14950,f15800]) ).
fof(f15805,definition,
( spl290_198
<=> v1_lattice3(sF288) ),
introduced(definition,[new_symbols(definition,[spl290_198])],[avatar_definition]) ).
fof(f15807,plain,
( v1_lattice3(sF288)
| ~ spl290_198 ),
inference(avatar_component_clause,[],[f15805]) ).
fof(f15808,plain,
( spl290_198
| ~ spl290_146
| ~ spl290_195 ),
inference(avatar_split_clause,[],[f15786,f15767,f14950,f15805]) ).
fof(f15810,definition,
( spl290_199
<=> v3_orders_2(sF288) ),
introduced(definition,[new_symbols(definition,[spl290_199])],[avatar_definition]) ).
fof(f15812,plain,
( v3_orders_2(sF288)
| ~ spl290_199 ),
inference(avatar_component_clause,[],[f15810]) ).
fof(f15813,plain,
( spl290_199
| ~ spl290_146
| ~ spl290_195 ),
inference(avatar_split_clause,[],[f15787,f15767,f14950,f15810]) ).
fof(f15870,plain,
( v4_orders_2(k2_yellow_2(sK105,sK105,sK106))
| ~ spl290_195 ),
inference(resolution,[],[f12392,f15769]) ).
fof(f15871,plain,
( v4_orders_2(sF288)
| ~ spl290_146
| ~ spl290_195 ),
inference(forward_demodulation,[],[f15870,f14952]) ).
fof(f15874,definition,
( spl290_201
<=> v4_orders_2(sF288) ),
introduced(definition,[new_symbols(definition,[spl290_201])],[avatar_definition]) ).
fof(f15876,plain,
( v4_orders_2(sF288)
| ~ spl290_201 ),
inference(avatar_component_clause,[],[f15874]) ).
fof(f15877,plain,
( spl290_201
| ~ spl290_146
| ~ spl290_195 ),
inference(avatar_split_clause,[],[f15871,f15767,f14950,f15874]) ).
fof(f16048,plain,
( v1_funct_1(k7_grcat_1(sF288))
| v3_struct_0(sK105)
| ~ l1_orders_2(sK105)
| v3_struct_0(sK105)
| ~ l1_orders_2(sK105)
| ~ v1_funct_1(sK106)
| ~ v1_funct_2(sK106,u1_struct_0(sK105),u1_struct_0(sK105))
| ~ m1_relset_1(sK106,u1_struct_0(sK105),u1_struct_0(sK105))
| ~ spl290_176 ),
inference(superposition,[],[f14044,f15373]) ).
fof(f16049,plain,
( v1_funct_1(k7_grcat_1(sF288))
| v3_struct_0(sK105)
| ~ l1_orders_2(sK105)
| ~ v1_funct_1(sK106)
| ~ v1_funct_2(sK106,u1_struct_0(sK105),u1_struct_0(sK105))
| ~ m1_relset_1(sK106,u1_struct_0(sK105),u1_struct_0(sK105))
| ~ spl290_176 ),
inference(duplicate_literal_removal,[],[f16048]) ).
fof(f16050,plain,
( v1_funct_1(k7_grcat_1(sF288))
| ~ l1_orders_2(sK105)
| ~ v1_funct_1(sK106)
| ~ v1_funct_2(sK106,u1_struct_0(sK105),u1_struct_0(sK105))
| ~ m1_relset_1(sK106,u1_struct_0(sK105),u1_struct_0(sK105))
| spl290_150
| ~ spl290_176 ),
inference(forward_subsumption_resolution,[],[f16049,f15045]) ).
fof(f16051,plain,
( v1_funct_1(k7_grcat_1(sF288))
| ~ v1_funct_1(sK106)
| ~ v1_funct_2(sK106,u1_struct_0(sK105),u1_struct_0(sK105))
| ~ m1_relset_1(sK106,u1_struct_0(sK105),u1_struct_0(sK105))
| ~ spl290_132
| spl290_150
| ~ spl290_176 ),
inference(forward_subsumption_resolution,[],[f16050,f14873]) ).
fof(f16052,plain,
( v1_funct_1(k7_grcat_1(sF288))
| ~ v1_funct_2(sK106,u1_struct_0(sK105),u1_struct_0(sK105))
| ~ m1_relset_1(sK106,u1_struct_0(sK105),u1_struct_0(sK105))
| ~ spl290_132
| ~ spl290_142
| spl290_150
| ~ spl290_176 ),
inference(forward_subsumption_resolution,[],[f16051,f14923]) ).
fof(f16053,plain,
( ~ v1_funct_2(sK106,sF289,sF289)
| v1_funct_1(k7_grcat_1(sF288))
| ~ m1_relset_1(sK106,u1_struct_0(sK105),u1_struct_0(sK105))
| ~ spl290_132
| ~ spl290_142
| ~ spl290_147
| spl290_150
| ~ spl290_176 ),
inference(forward_demodulation,[],[f16052,f14957]) ).
fof(f16054,plain,
( v1_funct_1(k7_grcat_1(sF288))
| ~ m1_relset_1(sK106,u1_struct_0(sK105),u1_struct_0(sK105))
| ~ spl290_132
| ~ spl290_141
| ~ spl290_142
| ~ spl290_147
| spl290_150
| ~ spl290_176 ),
inference(forward_subsumption_resolution,[],[f16053,f14918]) ).
fof(f16055,plain,
( ~ m1_relset_1(sK106,sF289,sF289)
| v1_funct_1(k7_grcat_1(sF288))
| ~ spl290_132
| ~ spl290_141
| ~ spl290_142
| ~ spl290_147
| spl290_150
| ~ spl290_176 ),
inference(forward_demodulation,[],[f16054,f14957]) ).
fof(f16056,plain,
( v1_funct_1(k7_grcat_1(sF288))
| ~ spl290_132
| ~ spl290_141
| ~ spl290_142
| ~ spl290_147
| ~ spl290_149
| spl290_150
| ~ spl290_176 ),
inference(forward_subsumption_resolution,[],[f16055,f15027]) ).
fof(f16058,definition,
( spl290_222
<=> v1_funct_1(k7_grcat_1(sF288)) ),
introduced(definition,[new_symbols(definition,[spl290_222])],[avatar_definition]) ).
fof(f16060,plain,
( v1_funct_1(k7_grcat_1(sF288))
| ~ spl290_222 ),
inference(avatar_component_clause,[],[f16058]) ).
fof(f16061,plain,
( spl290_222
| ~ spl290_132
| ~ spl290_141
| ~ spl290_142
| ~ spl290_147
| ~ spl290_149
| spl290_150
| ~ spl290_176 ),
inference(avatar_split_clause,[],[f16056,f15371,f15043,f15025,f14955,f14921,f14916,f14871,f16058]) ).
fof(f16134,plain,
( l1_orders_2(sF288)
| ~ spl290_132
| ~ spl290_173 ),
inference(unit_resulting_resolution,[],[f14048,f15308,f14873]) ).
fof(f16142,plain,
( $false
| ~ spl290_132
| spl290_155
| ~ spl290_173 ),
inference(forward_subsumption_resolution,[],[f16134,f15172]) ).
fof(f16143,plain,
( ~ spl290_132
| spl290_155
| ~ spl290_173 ),
inference(avatar_contradiction_clause,[],[f16142]) ).
fof(f16145,plain,
( ~ v22_waybel_0(k7_grcat_1(sF288),sF288,sK105)
| ~ v1_funct_1(k7_grcat_1(sF288))
| ~ v1_funct_2(k7_grcat_1(sF288),u1_struct_0(sF288),u1_struct_0(sK105))
| ~ v17_waybel_0(k7_grcat_1(sF288),sF288,sK105)
| ~ m2_relset_1(k7_grcat_1(sF288),u1_struct_0(sF288),u1_struct_0(sK105))
| ~ v2_orders_2(sK105)
| ~ v3_orders_2(sK105)
| ~ v4_orders_2(sK105)
| ~ v1_lattice3(sK105)
| ~ v2_lattice3(sK105)
| ~ v3_lattice3(sK105)
| ~ l1_orders_2(sK105)
| ~ v2_orders_2(sF288)
| ~ v3_orders_2(sF288)
| ~ v4_orders_2(sF288)
| ~ v1_lattice3(sF288)
| ~ v2_lattice3(sF288)
| ~ v3_lattice3(sF288)
| ~ l1_orders_2(sF288)
| spl290_153
| ~ spl290_184 ),
inference(forward_subsumption_resolution,[],[f15610,f15132]) ).
fof(f16162,plain,
( ~ v1_funct_1(k7_grcat_1(sF288))
| ~ v1_funct_2(k7_grcat_1(sF288),u1_struct_0(sF288),u1_struct_0(sK105))
| ~ v17_waybel_0(k7_grcat_1(sF288),sF288,sK105)
| ~ m2_relset_1(k7_grcat_1(sF288),u1_struct_0(sF288),u1_struct_0(sK105))
| ~ v2_orders_2(sK105)
| ~ v3_orders_2(sK105)
| ~ v4_orders_2(sK105)
| ~ v1_lattice3(sK105)
| ~ v2_lattice3(sK105)
| ~ v3_lattice3(sK105)
| ~ l1_orders_2(sK105)
| ~ v2_orders_2(sF288)
| ~ v3_orders_2(sF288)
| ~ v4_orders_2(sF288)
| ~ v1_lattice3(sF288)
| ~ v2_lattice3(sF288)
| ~ v3_lattice3(sF288)
| ~ l1_orders_2(sF288)
| spl290_153
| ~ spl290_177
| ~ spl290_184 ),
inference(forward_subsumption_resolution,[],[f16145,f15385]) ).
fof(f16179,plain,
( ~ v1_funct_2(k7_grcat_1(sF288),u1_struct_0(sF288),u1_struct_0(sK105))
| ~ v17_waybel_0(k7_grcat_1(sF288),sF288,sK105)
| ~ m2_relset_1(k7_grcat_1(sF288),u1_struct_0(sF288),u1_struct_0(sK105))
| ~ v2_orders_2(sK105)
| ~ v3_orders_2(sK105)
| ~ v4_orders_2(sK105)
| ~ v1_lattice3(sK105)
| ~ v2_lattice3(sK105)
| ~ v3_lattice3(sK105)
| ~ l1_orders_2(sK105)
| ~ v2_orders_2(sF288)
| ~ v3_orders_2(sF288)
| ~ v4_orders_2(sF288)
| ~ v1_lattice3(sF288)
| ~ v2_lattice3(sF288)
| ~ v3_lattice3(sF288)
| ~ l1_orders_2(sF288)
| spl290_153
| ~ spl290_177
| ~ spl290_184
| ~ spl290_222 ),
inference(forward_subsumption_resolution,[],[f16162,f16060]) ).
fof(f16194,plain,
( ~ v1_funct_2(k7_grcat_1(sF288),u1_struct_0(sF288),u1_struct_0(sK105))
| ~ m2_relset_1(k7_grcat_1(sF288),u1_struct_0(sF288),u1_struct_0(sK105))
| ~ v2_orders_2(sK105)
| ~ v3_orders_2(sK105)
| ~ v4_orders_2(sK105)
| ~ v1_lattice3(sK105)
| ~ v2_lattice3(sK105)
| ~ v3_lattice3(sK105)
| ~ l1_orders_2(sK105)
| ~ v2_orders_2(sF288)
| ~ v3_orders_2(sF288)
| ~ v4_orders_2(sF288)
| ~ v1_lattice3(sF288)
| ~ v2_lattice3(sF288)
| ~ v3_lattice3(sF288)
| ~ l1_orders_2(sF288)
| spl290_153
| ~ spl290_177
| ~ spl290_178
| ~ spl290_184
| ~ spl290_222 ),
inference(forward_subsumption_resolution,[],[f16179,f15390]) ).
fof(f16209,plain,
( ~ v1_funct_2(k7_grcat_1(sF288),u1_struct_0(sF288),u1_struct_0(sK105))
| ~ m2_relset_1(k7_grcat_1(sF288),u1_struct_0(sF288),u1_struct_0(sK105))
| ~ v3_orders_2(sK105)
| ~ v4_orders_2(sK105)
| ~ v1_lattice3(sK105)
| ~ v2_lattice3(sK105)
| ~ v3_lattice3(sK105)
| ~ l1_orders_2(sK105)
| ~ v2_orders_2(sF288)
| ~ v3_orders_2(sF288)
| ~ v4_orders_2(sF288)
| ~ v1_lattice3(sF288)
| ~ v2_lattice3(sF288)
| ~ v3_lattice3(sF288)
| ~ l1_orders_2(sF288)
| ~ spl290_138
| spl290_153
| ~ spl290_177
| ~ spl290_178
| ~ spl290_184
| ~ spl290_222 ),
inference(forward_subsumption_resolution,[],[f16194,f14903]) ).
fof(f16222,plain,
( ~ v1_funct_2(k7_grcat_1(sF288),u1_struct_0(sF288),u1_struct_0(sK105))
| ~ m2_relset_1(k7_grcat_1(sF288),u1_struct_0(sF288),u1_struct_0(sK105))
| ~ v4_orders_2(sK105)
| ~ v1_lattice3(sK105)
| ~ v2_lattice3(sK105)
| ~ v3_lattice3(sK105)
| ~ l1_orders_2(sK105)
| ~ v2_orders_2(sF288)
| ~ v3_orders_2(sF288)
| ~ v4_orders_2(sF288)
| ~ v1_lattice3(sF288)
| ~ v2_lattice3(sF288)
| ~ v3_lattice3(sF288)
| ~ l1_orders_2(sF288)
| ~ spl290_137
| ~ spl290_138
| spl290_153
| ~ spl290_177
| ~ spl290_178
| ~ spl290_184
| ~ spl290_222 ),
inference(forward_subsumption_resolution,[],[f16209,f14898]) ).
fof(f16233,plain,
( ~ v1_funct_2(k7_grcat_1(sF288),u1_struct_0(sF288),u1_struct_0(sK105))
| ~ m2_relset_1(k7_grcat_1(sF288),u1_struct_0(sF288),u1_struct_0(sK105))
| ~ v1_lattice3(sK105)
| ~ v2_lattice3(sK105)
| ~ v3_lattice3(sK105)
| ~ l1_orders_2(sK105)
| ~ v2_orders_2(sF288)
| ~ v3_orders_2(sF288)
| ~ v4_orders_2(sF288)
| ~ v1_lattice3(sF288)
| ~ v2_lattice3(sF288)
| ~ v3_lattice3(sF288)
| ~ l1_orders_2(sF288)
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138
| spl290_153
| ~ spl290_177
| ~ spl290_178
| ~ spl290_184
| ~ spl290_222 ),
inference(forward_subsumption_resolution,[],[f16222,f14893]) ).
fof(f16235,plain,
( ~ v1_funct_2(k7_grcat_1(sF288),u1_struct_0(sF288),u1_struct_0(sK105))
| ~ m2_relset_1(k7_grcat_1(sF288),u1_struct_0(sF288),u1_struct_0(sK105))
| ~ v2_lattice3(sK105)
| ~ v3_lattice3(sK105)
| ~ l1_orders_2(sK105)
| ~ v2_orders_2(sF288)
| ~ v3_orders_2(sF288)
| ~ v4_orders_2(sF288)
| ~ v1_lattice3(sF288)
| ~ v2_lattice3(sF288)
| ~ v3_lattice3(sF288)
| ~ l1_orders_2(sF288)
| ~ spl290_135
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138
| spl290_153
| ~ spl290_177
| ~ spl290_178
| ~ spl290_184
| ~ spl290_222 ),
inference(forward_subsumption_resolution,[],[f16233,f14888]) ).
fof(f16237,plain,
( ~ v1_funct_2(k7_grcat_1(sF288),u1_struct_0(sF288),u1_struct_0(sK105))
| ~ m2_relset_1(k7_grcat_1(sF288),u1_struct_0(sF288),u1_struct_0(sK105))
| ~ v3_lattice3(sK105)
| ~ l1_orders_2(sK105)
| ~ v2_orders_2(sF288)
| ~ v3_orders_2(sF288)
| ~ v4_orders_2(sF288)
| ~ v1_lattice3(sF288)
| ~ v2_lattice3(sF288)
| ~ v3_lattice3(sF288)
| ~ l1_orders_2(sF288)
| ~ spl290_134
| ~ spl290_135
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138
| spl290_153
| ~ spl290_177
| ~ spl290_178
| ~ spl290_184
| ~ spl290_222 ),
inference(forward_subsumption_resolution,[],[f16235,f14883]) ).
fof(f16239,plain,
( ~ v1_funct_2(k7_grcat_1(sF288),u1_struct_0(sF288),u1_struct_0(sK105))
| ~ m2_relset_1(k7_grcat_1(sF288),u1_struct_0(sF288),u1_struct_0(sK105))
| ~ l1_orders_2(sK105)
| ~ v2_orders_2(sF288)
| ~ v3_orders_2(sF288)
| ~ v4_orders_2(sF288)
| ~ v1_lattice3(sF288)
| ~ v2_lattice3(sF288)
| ~ v3_lattice3(sF288)
| ~ l1_orders_2(sF288)
| ~ spl290_133
| ~ spl290_134
| ~ spl290_135
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138
| spl290_153
| ~ spl290_177
| ~ spl290_178
| ~ spl290_184
| ~ spl290_222 ),
inference(forward_subsumption_resolution,[],[f16237,f14878]) ).
fof(f16241,plain,
( ~ v1_funct_2(k7_grcat_1(sF288),u1_struct_0(sF288),u1_struct_0(sK105))
| ~ m2_relset_1(k7_grcat_1(sF288),u1_struct_0(sF288),u1_struct_0(sK105))
| ~ v2_orders_2(sF288)
| ~ v3_orders_2(sF288)
| ~ v4_orders_2(sF288)
| ~ v1_lattice3(sF288)
| ~ v2_lattice3(sF288)
| ~ v3_lattice3(sF288)
| ~ l1_orders_2(sF288)
| ~ spl290_132
| ~ spl290_133
| ~ spl290_134
| ~ spl290_135
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138
| spl290_153
| ~ spl290_177
| ~ spl290_178
| ~ spl290_184
| ~ spl290_222 ),
inference(forward_subsumption_resolution,[],[f16239,f14873]) ).
fof(f16243,plain,
( ~ v1_funct_2(k7_grcat_1(sF288),u1_struct_0(sF288),u1_struct_0(sK105))
| ~ m2_relset_1(k7_grcat_1(sF288),u1_struct_0(sF288),u1_struct_0(sK105))
| ~ v3_orders_2(sF288)
| ~ v4_orders_2(sF288)
| ~ v1_lattice3(sF288)
| ~ v2_lattice3(sF288)
| ~ v3_lattice3(sF288)
| ~ l1_orders_2(sF288)
| ~ spl290_132
| ~ spl290_133
| ~ spl290_134
| ~ spl290_135
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138
| spl290_153
| ~ spl290_167
| ~ spl290_177
| ~ spl290_178
| ~ spl290_184
| ~ spl290_222 ),
inference(forward_subsumption_resolution,[],[f16241,f15219]) ).
fof(f16245,plain,
( ~ v1_funct_2(k7_grcat_1(sF288),u1_struct_0(sF288),u1_struct_0(sK105))
| ~ m2_relset_1(k7_grcat_1(sF288),u1_struct_0(sF288),u1_struct_0(sK105))
| ~ v4_orders_2(sF288)
| ~ v1_lattice3(sF288)
| ~ v2_lattice3(sF288)
| ~ v3_lattice3(sF288)
| ~ l1_orders_2(sF288)
| ~ spl290_132
| ~ spl290_133
| ~ spl290_134
| ~ spl290_135
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138
| spl290_153
| ~ spl290_167
| ~ spl290_177
| ~ spl290_178
| ~ spl290_184
| ~ spl290_199
| ~ spl290_222 ),
inference(forward_subsumption_resolution,[],[f16243,f15812]) ).
fof(f16247,plain,
( ~ v1_funct_2(k7_grcat_1(sF288),u1_struct_0(sF288),u1_struct_0(sK105))
| ~ m2_relset_1(k7_grcat_1(sF288),u1_struct_0(sF288),u1_struct_0(sK105))
| ~ v1_lattice3(sF288)
| ~ v2_lattice3(sF288)
| ~ v3_lattice3(sF288)
| ~ l1_orders_2(sF288)
| ~ spl290_132
| ~ spl290_133
| ~ spl290_134
| ~ spl290_135
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138
| spl290_153
| ~ spl290_167
| ~ spl290_177
| ~ spl290_178
| ~ spl290_184
| ~ spl290_199
| ~ spl290_201
| ~ spl290_222 ),
inference(forward_subsumption_resolution,[],[f16245,f15876]) ).
fof(f16249,plain,
( ~ v1_funct_2(k7_grcat_1(sF288),u1_struct_0(sF288),u1_struct_0(sK105))
| ~ m2_relset_1(k7_grcat_1(sF288),u1_struct_0(sF288),u1_struct_0(sK105))
| ~ v2_lattice3(sF288)
| ~ v3_lattice3(sF288)
| ~ l1_orders_2(sF288)
| ~ spl290_132
| ~ spl290_133
| ~ spl290_134
| ~ spl290_135
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138
| spl290_153
| ~ spl290_167
| ~ spl290_177
| ~ spl290_178
| ~ spl290_184
| ~ spl290_198
| ~ spl290_199
| ~ spl290_201
| ~ spl290_222 ),
inference(forward_subsumption_resolution,[],[f16247,f15807]) ).
fof(f16251,plain,
( ~ v1_funct_2(k7_grcat_1(sF288),u1_struct_0(sF288),u1_struct_0(sK105))
| ~ m2_relset_1(k7_grcat_1(sF288),u1_struct_0(sF288),u1_struct_0(sK105))
| ~ v3_lattice3(sF288)
| ~ l1_orders_2(sF288)
| ~ spl290_132
| ~ spl290_133
| ~ spl290_134
| ~ spl290_135
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138
| spl290_153
| ~ spl290_167
| ~ spl290_177
| ~ spl290_178
| ~ spl290_184
| ~ spl290_197
| ~ spl290_198
| ~ spl290_199
| ~ spl290_201
| ~ spl290_222 ),
inference(forward_subsumption_resolution,[],[f16249,f15802]) ).
fof(f16253,plain,
( ~ v1_funct_2(k7_grcat_1(sF288),u1_struct_0(sF288),u1_struct_0(sK105))
| ~ m2_relset_1(k7_grcat_1(sF288),u1_struct_0(sF288),u1_struct_0(sK105))
| ~ l1_orders_2(sF288)
| ~ spl290_132
| ~ spl290_133
| ~ spl290_134
| ~ spl290_135
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138
| spl290_153
| ~ spl290_167
| ~ spl290_177
| ~ spl290_178
| ~ spl290_184
| ~ spl290_196
| ~ spl290_197
| ~ spl290_198
| ~ spl290_199
| ~ spl290_201
| ~ spl290_222 ),
inference(forward_subsumption_resolution,[],[f16251,f15797]) ).
fof(f16255,plain,
( ~ v1_funct_2(k7_grcat_1(sF288),u1_struct_0(sF288),u1_struct_0(sK105))
| ~ m2_relset_1(k7_grcat_1(sF288),u1_struct_0(sF288),u1_struct_0(sK105))
| ~ spl290_132
| ~ spl290_133
| ~ spl290_134
| ~ spl290_135
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138
| spl290_153
| ~ spl290_155
| ~ spl290_167
| ~ spl290_177
| ~ spl290_178
| ~ spl290_184
| ~ spl290_196
| ~ spl290_197
| ~ spl290_198
| ~ spl290_199
| ~ spl290_201
| ~ spl290_222 ),
inference(forward_subsumption_resolution,[],[f16253,f15171]) ).
fof(f16257,plain,
( ~ v1_funct_2(k7_grcat_1(sF288),u1_struct_0(sF288),sF289)
| ~ m2_relset_1(k7_grcat_1(sF288),u1_struct_0(sF288),u1_struct_0(sK105))
| ~ spl290_132
| ~ spl290_133
| ~ spl290_134
| ~ spl290_135
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138
| ~ spl290_147
| spl290_153
| ~ spl290_155
| ~ spl290_167
| ~ spl290_177
| ~ spl290_178
| ~ spl290_184
| ~ spl290_196
| ~ spl290_197
| ~ spl290_198
| ~ spl290_199
| ~ spl290_201
| ~ spl290_222 ),
inference(forward_demodulation,[],[f16255,f14957]) ).
fof(f16259,plain,
( ~ m2_relset_1(k7_grcat_1(sF288),u1_struct_0(sF288),sF289)
| ~ v1_funct_2(k7_grcat_1(sF288),u1_struct_0(sF288),sF289)
| ~ spl290_132
| ~ spl290_133
| ~ spl290_134
| ~ spl290_135
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138
| ~ spl290_147
| spl290_153
| ~ spl290_155
| ~ spl290_167
| ~ spl290_177
| ~ spl290_178
| ~ spl290_184
| ~ spl290_196
| ~ spl290_197
| ~ spl290_198
| ~ spl290_199
| ~ spl290_201
| ~ spl290_222 ),
inference(forward_demodulation,[],[f16257,f14957]) ).
fof(f16262,definition,
( spl290_224
<=> v1_funct_2(k7_grcat_1(sF288),u1_struct_0(sF288),sF289) ),
introduced(definition,[new_symbols(definition,[spl290_224])],[avatar_definition]) ).
fof(f16264,plain,
( ~ v1_funct_2(k7_grcat_1(sF288),u1_struct_0(sF288),sF289)
| spl290_224 ),
inference(avatar_component_clause,[],[f16262]) ).
fof(f16266,definition,
( spl290_225
<=> m2_relset_1(k7_grcat_1(sF288),u1_struct_0(sF288),sF289) ),
introduced(definition,[new_symbols(definition,[spl290_225])],[avatar_definition]) ).
fof(f16268,plain,
( ~ m2_relset_1(k7_grcat_1(sF288),u1_struct_0(sF288),sF289)
| spl290_225 ),
inference(avatar_component_clause,[],[f16266]) ).
fof(f16269,plain,
( ~ spl290_224
| ~ spl290_225
| ~ spl290_132
| ~ spl290_133
| ~ spl290_134
| ~ spl290_135
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138
| ~ spl290_147
| spl290_153
| ~ spl290_155
| ~ spl290_167
| ~ spl290_177
| ~ spl290_178
| ~ spl290_184
| ~ spl290_196
| ~ spl290_197
| ~ spl290_198
| ~ spl290_199
| ~ spl290_201
| ~ spl290_222 ),
inference(avatar_split_clause,[],[f16259,f16058,f15874,f15810,f15805,f15800,f15795,f15570,f15388,f15383,f15218,f15170,f15130,f14955,f14901,f14896,f14891,f14886,f14881,f14876,f14871,f16266,f16262]) ).
fof(f17075,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF289,u1_struct_0(sK105))
| v1_funct_2(k3_waybel_1(sK105,sK105,X0),u1_struct_0(k2_yellow_2(sK105,sK105,X0)),u1_struct_0(sK105))
| v3_struct_0(sK105)
| ~ m1_relset_1(X0,sF289,u1_struct_0(sK105))
| ~ v1_funct_1(X0) )
| ~ spl290_132
| ~ spl290_147
| spl290_150 ),
inference(resolution,[],[f15089,f14873]) ).
fof(f17078,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF289,u1_struct_0(sK105))
| v1_funct_2(k3_waybel_1(sK105,sK105,X0),u1_struct_0(k2_yellow_2(sK105,sK105,X0)),u1_struct_0(sK105))
| ~ m1_relset_1(X0,sF289,u1_struct_0(sK105))
| ~ v1_funct_1(X0) )
| ~ spl290_132
| ~ spl290_147
| spl290_150 ),
inference(forward_subsumption_resolution,[],[f17075,f15045]) ).
fof(f17084,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF289,sF289)
| v1_funct_2(k3_waybel_1(sK105,sK105,X0),u1_struct_0(k2_yellow_2(sK105,sK105,X0)),u1_struct_0(sK105))
| ~ m1_relset_1(X0,sF289,u1_struct_0(sK105))
| ~ v1_funct_1(X0) )
| ~ spl290_132
| ~ spl290_147
| spl290_150 ),
inference(forward_demodulation,[],[f17078,f14957]) ).
fof(f17085,plain,
( ! [X0] :
( v1_funct_2(k3_waybel_1(sK105,sK105,X0),u1_struct_0(k2_yellow_2(sK105,sK105,X0)),sF289)
| ~ v1_funct_2(X0,sF289,sF289)
| ~ m1_relset_1(X0,sF289,u1_struct_0(sK105))
| ~ v1_funct_1(X0) )
| ~ spl290_132
| ~ spl290_147
| spl290_150 ),
inference(forward_demodulation,[],[f17084,f14957]) ).
fof(f17086,plain,
( ! [X0] :
( v1_funct_2(k3_waybel_1(sK105,sK105,X0),u1_struct_0(k2_yellow_2(sK105,sK105,X0)),sF289)
| ~ m1_relset_1(X0,sF289,sF289)
| ~ v1_funct_2(X0,sF289,sF289)
| ~ v1_funct_1(X0) )
| ~ spl290_132
| ~ spl290_147
| spl290_150 ),
inference(forward_demodulation,[],[f17085,f14957]) ).
fof(f17088,plain,
( v1_funct_2(k7_grcat_1(sF288),u1_struct_0(k2_yellow_2(sK105,sK105,sK106)),sF289)
| ~ m1_relset_1(sK106,sF289,sF289)
| ~ v1_funct_2(sK106,sF289,sF289)
| ~ v1_funct_1(sK106)
| ~ spl290_132
| ~ spl290_147
| spl290_150
| ~ spl290_176 ),
inference(superposition,[],[f17086,f15373]) ).
fof(f17091,plain,
( v1_funct_2(k7_grcat_1(sF288),u1_struct_0(k2_yellow_2(sK105,sK105,sK106)),sF289)
| ~ v1_funct_2(sK106,sF289,sF289)
| ~ v1_funct_1(sK106)
| ~ spl290_132
| ~ spl290_147
| ~ spl290_149
| spl290_150
| ~ spl290_176 ),
inference(forward_subsumption_resolution,[],[f17088,f15027]) ).
fof(f17094,plain,
( v1_funct_2(k7_grcat_1(sF288),u1_struct_0(k2_yellow_2(sK105,sK105,sK106)),sF289)
| ~ v1_funct_1(sK106)
| ~ spl290_132
| ~ spl290_141
| ~ spl290_147
| ~ spl290_149
| spl290_150
| ~ spl290_176 ),
inference(forward_subsumption_resolution,[],[f17091,f14918]) ).
fof(f17097,plain,
( v1_funct_2(k7_grcat_1(sF288),u1_struct_0(k2_yellow_2(sK105,sK105,sK106)),sF289)
| ~ spl290_132
| ~ spl290_141
| ~ spl290_142
| ~ spl290_147
| ~ spl290_149
| spl290_150
| ~ spl290_176 ),
inference(forward_subsumption_resolution,[],[f17094,f14923]) ).
fof(f17101,plain,
( v1_funct_2(k7_grcat_1(sF288),u1_struct_0(sF288),sF289)
| ~ spl290_132
| ~ spl290_141
| ~ spl290_142
| ~ spl290_146
| ~ spl290_147
| ~ spl290_149
| spl290_150
| ~ spl290_176 ),
inference(forward_demodulation,[],[f17097,f14952]) ).
fof(f17104,plain,
( $false
| ~ spl290_132
| ~ spl290_141
| ~ spl290_142
| ~ spl290_146
| ~ spl290_147
| ~ spl290_149
| spl290_150
| ~ spl290_176
| spl290_224 ),
inference(forward_subsumption_resolution,[],[f17101,f16264]) ).
fof(f17105,plain,
( ~ spl290_132
| ~ spl290_141
| ~ spl290_142
| ~ spl290_146
| ~ spl290_147
| ~ spl290_149
| spl290_150
| ~ spl290_176
| spl290_224 ),
inference(avatar_contradiction_clause,[],[f17104]) ).
fof(f17152,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF289,u1_struct_0(sK105))
| m2_relset_1(k3_waybel_1(sK105,sK105,X0),u1_struct_0(k2_yellow_2(sK105,sK105,X0)),u1_struct_0(sK105))
| v3_struct_0(sK105)
| ~ m1_relset_1(X0,sF289,u1_struct_0(sK105))
| ~ v1_funct_1(X0) )
| ~ spl290_132
| ~ spl290_147
| spl290_150 ),
inference(resolution,[],[f15091,f14873]) ).
fof(f17155,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF289,u1_struct_0(sK105))
| m2_relset_1(k3_waybel_1(sK105,sK105,X0),u1_struct_0(k2_yellow_2(sK105,sK105,X0)),u1_struct_0(sK105))
| ~ m1_relset_1(X0,sF289,u1_struct_0(sK105))
| ~ v1_funct_1(X0) )
| ~ spl290_132
| ~ spl290_147
| spl290_150 ),
inference(forward_subsumption_resolution,[],[f17152,f15045]) ).
fof(f17157,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF289,sF289)
| m2_relset_1(k3_waybel_1(sK105,sK105,X0),u1_struct_0(k2_yellow_2(sK105,sK105,X0)),u1_struct_0(sK105))
| ~ m1_relset_1(X0,sF289,u1_struct_0(sK105))
| ~ v1_funct_1(X0) )
| ~ spl290_132
| ~ spl290_147
| spl290_150 ),
inference(forward_demodulation,[],[f17155,f14957]) ).
fof(f17163,plain,
( ! [X0] :
( m2_relset_1(k3_waybel_1(sK105,sK105,X0),u1_struct_0(k2_yellow_2(sK105,sK105,X0)),sF289)
| ~ v1_funct_2(X0,sF289,sF289)
| ~ m1_relset_1(X0,sF289,u1_struct_0(sK105))
| ~ v1_funct_1(X0) )
| ~ spl290_132
| ~ spl290_147
| spl290_150 ),
inference(forward_demodulation,[],[f17157,f14957]) ).
fof(f17164,plain,
( ! [X0] :
( m2_relset_1(k3_waybel_1(sK105,sK105,X0),u1_struct_0(k2_yellow_2(sK105,sK105,X0)),sF289)
| ~ m1_relset_1(X0,sF289,sF289)
| ~ v1_funct_2(X0,sF289,sF289)
| ~ v1_funct_1(X0) )
| ~ spl290_132
| ~ spl290_147
| spl290_150 ),
inference(forward_demodulation,[],[f17163,f14957]) ).
fof(f17166,plain,
( m2_relset_1(k7_grcat_1(sF288),u1_struct_0(k2_yellow_2(sK105,sK105,sK106)),sF289)
| ~ m1_relset_1(sK106,sF289,sF289)
| ~ v1_funct_2(sK106,sF289,sF289)
| ~ v1_funct_1(sK106)
| ~ spl290_132
| ~ spl290_147
| spl290_150
| ~ spl290_176 ),
inference(superposition,[],[f17164,f15373]) ).
fof(f17169,plain,
( m2_relset_1(k7_grcat_1(sF288),u1_struct_0(k2_yellow_2(sK105,sK105,sK106)),sF289)
| ~ v1_funct_2(sK106,sF289,sF289)
| ~ v1_funct_1(sK106)
| ~ spl290_132
| ~ spl290_147
| ~ spl290_149
| spl290_150
| ~ spl290_176 ),
inference(forward_subsumption_resolution,[],[f17166,f15027]) ).
fof(f17172,plain,
( m2_relset_1(k7_grcat_1(sF288),u1_struct_0(k2_yellow_2(sK105,sK105,sK106)),sF289)
| ~ v1_funct_1(sK106)
| ~ spl290_132
| ~ spl290_141
| ~ spl290_147
| ~ spl290_149
| spl290_150
| ~ spl290_176 ),
inference(forward_subsumption_resolution,[],[f17169,f14918]) ).
fof(f17175,plain,
( m2_relset_1(k7_grcat_1(sF288),u1_struct_0(k2_yellow_2(sK105,sK105,sK106)),sF289)
| ~ spl290_132
| ~ spl290_141
| ~ spl290_142
| ~ spl290_147
| ~ spl290_149
| spl290_150
| ~ spl290_176 ),
inference(forward_subsumption_resolution,[],[f17172,f14923]) ).
fof(f17179,plain,
( m2_relset_1(k7_grcat_1(sF288),u1_struct_0(sF288),sF289)
| ~ spl290_132
| ~ spl290_141
| ~ spl290_142
| ~ spl290_146
| ~ spl290_147
| ~ spl290_149
| spl290_150
| ~ spl290_176 ),
inference(forward_demodulation,[],[f17175,f14952]) ).
fof(f17182,plain,
( $false
| ~ spl290_132
| ~ spl290_141
| ~ spl290_142
| ~ spl290_146
| ~ spl290_147
| ~ spl290_149
| spl290_150
| ~ spl290_176
| spl290_225 ),
inference(forward_subsumption_resolution,[],[f17179,f16268]) ).
fof(f17183,plain,
( ~ spl290_132
| ~ spl290_141
| ~ spl290_142
| ~ spl290_146
| ~ spl290_147
| ~ spl290_149
| spl290_150
| ~ spl290_176
| spl290_225 ),
inference(avatar_contradiction_clause,[],[f17182]) ).
cnf(s135,plain,
spl290_132,
inference(sat_conversion,[],[f14874]) ).
cnf(s136,plain,
spl290_133,
inference(sat_conversion,[],[f14879]) ).
cnf(s137,plain,
spl290_134,
inference(sat_conversion,[],[f14884]) ).
cnf(s138,plain,
spl290_135,
inference(sat_conversion,[],[f14889]) ).
cnf(s139,plain,
spl290_136,
inference(sat_conversion,[],[f14894]) ).
cnf(s140,plain,
spl290_137,
inference(sat_conversion,[],[f14899]) ).
cnf(s141,plain,
spl290_138,
inference(sat_conversion,[],[f14904]) ).
cnf(s142,plain,
spl290_139,
inference(sat_conversion,[],[f14909]) ).
cnf(s143,plain,
spl290_140,
inference(sat_conversion,[],[f14914]) ).
cnf(s144,plain,
spl290_141,
inference(sat_conversion,[],[f14919]) ).
cnf(s145,plain,
spl290_142,
inference(sat_conversion,[],[f14924]) ).
cnf(s146,plain,
spl290_143,
inference(sat_conversion,[],[f14929]) ).
cnf(s147,plain,
~ spl290_144,
inference(sat_conversion,[],[f14934]) ).
cnf(s148,plain,
spl290_145,
inference(sat_conversion,[],[f14948]) ).
cnf(s149,plain,
spl290_146,
inference(sat_conversion,[],[f14953]) ).
cnf(s150,plain,
spl290_147,
inference(sat_conversion,[],[f14958]) ).
cnf(s151,plain,
( ~ spl290_132
| ~ spl290_133
| ~ spl290_134
| ~ spl290_135
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138
| ~ spl290_139
| ~ spl290_140
| ~ spl290_141
| ~ spl290_142
| ~ spl290_143
| ~ spl290_146
| ~ spl290_147
| spl290_148 ),
inference(sat_conversion,[],[f15022]) ).
cnf(s152,plain,
( ~ spl290_139
| spl290_149 ),
inference(sat_conversion,[],[f15028]) ).
cnf(s153,plain,
( ~ spl290_132
| ~ spl290_134
| ~ spl290_150 ),
inference(sat_conversion,[],[f15046]) ).
cnf(s155,plain,
( ~ spl290_132
| ~ spl290_139
| ~ spl290_141
| ~ spl290_142
| ~ spl290_147
| spl290_150
| spl290_151 ),
inference(sat_conversion,[],[f15119]) ).
cnf(s157,plain,
( ~ spl290_145
| ~ spl290_151
| spl290_152 ),
inference(sat_conversion,[],[f15127]) ).
cnf(s159,plain,
( spl290_144
| ~ spl290_152
| ~ spl290_153 ),
inference(sat_conversion,[],[f15133]) ).
cnf(s176,plain,
( ~ spl290_132
| ~ spl290_133
| ~ spl290_134
| ~ spl290_135
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138
| ~ spl290_139
| ~ spl290_140
| ~ spl290_141
| ~ spl290_142
| ~ spl290_146
| ~ spl290_147
| spl290_171 ),
inference(sat_conversion,[],[f15256]) ).
cnf(s180,plain,
( ~ spl290_132
| ~ spl290_141
| ~ spl290_142
| ~ spl290_146
| ~ spl290_147
| ~ spl290_149
| spl290_150
| spl290_173 ),
inference(sat_conversion,[],[f15309]) ).
cnf(s185,plain,
( ~ spl290_132
| ~ spl290_139
| ~ spl290_141
| ~ spl290_142
| ~ spl290_146
| ~ spl290_147
| spl290_150
| spl290_176 ),
inference(sat_conversion,[],[f15374]) ).
cnf(s187,plain,
( ~ spl290_148
| ~ spl290_176
| spl290_177 ),
inference(sat_conversion,[],[f15386]) ).
cnf(s188,plain,
( ~ spl290_171
| ~ spl290_176
| spl290_178 ),
inference(sat_conversion,[],[f15391]) ).
cnf(s200,plain,
( ~ spl290_132
| ~ spl290_133
| ~ spl290_134
| ~ spl290_135
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138
| ~ spl290_139
| ~ spl290_140
| ~ spl290_141
| ~ spl290_142
| ~ spl290_145
| ~ spl290_146
| ~ spl290_147
| ~ spl290_152
| ~ spl290_176
| spl290_184 ),
inference(sat_conversion,[],[f15573]) ).
cnf(s213,plain,
( ~ spl290_132
| ~ spl290_133
| ~ spl290_134
| ~ spl290_135
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138
| ~ spl290_140
| ~ spl290_141
| ~ spl290_142
| ~ spl290_147
| ~ spl290_149
| spl290_150
| spl290_195 ),
inference(sat_conversion,[],[f15770]) ).
cnf(s215,plain,
( ~ spl290_146
| spl290_167
| ~ spl290_195 ),
inference(sat_conversion,[],[f15793]) ).
cnf(s216,plain,
( ~ spl290_146
| ~ spl290_195
| spl290_196 ),
inference(sat_conversion,[],[f15798]) ).
cnf(s217,plain,
( ~ spl290_146
| ~ spl290_195
| spl290_197 ),
inference(sat_conversion,[],[f15803]) ).
cnf(s218,plain,
( ~ spl290_146
| ~ spl290_195
| spl290_198 ),
inference(sat_conversion,[],[f15808]) ).
cnf(s219,plain,
( ~ spl290_146
| ~ spl290_195
| spl290_199 ),
inference(sat_conversion,[],[f15813]) ).
cnf(s227,plain,
( ~ spl290_146
| ~ spl290_195
| spl290_201 ),
inference(sat_conversion,[],[f15877]) ).
cnf(s250,plain,
( ~ spl290_132
| ~ spl290_141
| ~ spl290_142
| ~ spl290_147
| ~ spl290_149
| spl290_150
| ~ spl290_176
| spl290_222 ),
inference(sat_conversion,[],[f16061]) ).
cnf(s257,plain,
( ~ spl290_132
| spl290_155
| ~ spl290_173 ),
inference(sat_conversion,[],[f16143]) ).
cnf(s258,plain,
( ~ spl290_132
| ~ spl290_133
| ~ spl290_134
| ~ spl290_135
| ~ spl290_136
| ~ spl290_137
| ~ spl290_138
| ~ spl290_147
| spl290_153
| ~ spl290_155
| ~ spl290_167
| ~ spl290_177
| ~ spl290_178
| ~ spl290_184
| ~ spl290_196
| ~ spl290_197
| ~ spl290_198
| ~ spl290_199
| ~ spl290_201
| ~ spl290_222
| ~ spl290_224
| ~ spl290_225 ),
inference(sat_conversion,[],[f16269]) ).
cnf(s328,plain,
( ~ spl290_132
| ~ spl290_141
| ~ spl290_142
| ~ spl290_146
| ~ spl290_147
| ~ spl290_149
| spl290_150
| ~ spl290_176
| spl290_224 ),
inference(sat_conversion,[],[f17105]) ).
cnf(s338,plain,
( ~ spl290_132
| ~ spl290_141
| ~ spl290_142
| ~ spl290_146
| ~ spl290_147
| ~ spl290_149
| spl290_150
| ~ spl290_176
| spl290_225 ),
inference(sat_conversion,[],[f17183]) ).
cnf(s339,plain,
spl290_149,
inference(rat,[],[s152,s142]) ).
cnf(s348,plain,
spl290_171,
inference(rat,[],[s176,s136,s150,s149,s145,s144,s143,s142,s141,s140,s139,s138,s137,s135]) ).
cnf(s349,plain,
~ spl290_150,
inference(rat,[],[s153,s137,s135]) ).
cnf(s350,plain,
spl290_148,
inference(rat,[],[s151,s136,s150,s149,s146,s145,s144,s143,s142,s141,s140,s139,s138,s137,s135]) ).
cnf(s361,plain,
spl290_176,
inference(rat,[],[s185,s135,s142,s150,s149,s145,s144,s349]) ).
cnf(s362,plain,
spl290_151,
inference(rat,[],[s155,s135,s142,s150,s145,s144,s349]) ).
cnf(s365,plain,
spl290_173,
inference(rat,[],[s180,s135,s339,s144,s150,s149,s145,s349]) ).
cnf(s374,plain,
spl290_195,
inference(rat,[],[s213,s135,s136,s339,s150,s145,s144,s143,s141,s140,s139,s138,s137,s349]) ).
cnf(s376,plain,
spl290_178,
inference(rat,[],[s188,s348,s361]) ).
cnf(s377,plain,
spl290_177,
inference(rat,[],[s187,s350,s361]) ).
cnf(s378,plain,
spl290_225,
inference(rat,[],[s338,s349,s135,s339,s144,s150,s149,s145,s361]) ).
cnf(s379,plain,
spl290_224,
inference(rat,[],[s328,s349,s135,s339,s144,s150,s149,s145,s361]) ).
cnf(s381,plain,
spl290_222,
inference(rat,[],[s250,s349,s135,s339,s144,s150,s145,s361]) ).
cnf(s382,plain,
spl290_152,
inference(rat,[],[s157,s148,s362]) ).
cnf(s383,plain,
spl290_155,
inference(rat,[],[s257,s135,s365]) ).
cnf(s384,plain,
spl290_201,
inference(rat,[],[s227,s149,s374]) ).
cnf(s385,plain,
spl290_199,
inference(rat,[],[s219,s149,s374]) ).
cnf(s386,plain,
spl290_198,
inference(rat,[],[s218,s149,s374]) ).
cnf(s387,plain,
spl290_197,
inference(rat,[],[s217,s149,s374]) ).
cnf(s388,plain,
spl290_196,
inference(rat,[],[s216,s149,s374]) ).
cnf(s389,plain,
spl290_167,
inference(rat,[],[s215,s149,s374]) ).
cnf(s390,plain,
~ spl290_153,
inference(rat,[],[s159,s147,s382]) ).
cnf(s391,plain,
spl290_184,
inference(rat,[],[s200,s361,s135,s136,s150,s149,s148,s145,s144,s143,s142,s141,s140,s139,s138,s137,s382]) ).
cnf(s417,plain,
$false,
inference(rat,[],[s258,s378,s379,s381,s384,s385,s386,s387,s388,s391,s376,s377,s389,s135,s136,s150,s141,s140,s139,s138,s137,s383,s390]) ).
fof(f17184,plain,
$false,
inference(avatar_sat_refutation,[],[s417]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT369+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.37 % Computer : n014.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sun Sep 27 15:05:48 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.41 Running first-order theorem proving
% 0.10/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
% 13.10/3.17 % (916843)Detected formulas, will run a generic FOF schedule.
% 13.10/3.17 % (916851)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1604431657:i=109:sd=1:ins=1:gsp=on:ss=axioms_2994 on theBenchmark for (2994ds/109Mi)
% 13.10/3.17 % (916851)Refutation not found, incomplete strategy
% 13.10/3.17 % (916851)------------------------------
% 13.10/3.17 % (916851)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.10/3.17 % (916851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.10/3.17 % (916851)CaDiCaL version: 2.1.3
% 13.10/3.17 % (916851)Termination reason: Refutation not found, incomplete strategy
% 13.10/3.17 % (916851)Time elapsed: 0.034 s
% 13.10/3.17 % (916851)Peak memory usage: 103 MB
% 13.10/3.17 % (916851)Instructions burned: 68 (million)
% 13.10/3.17 % (916848)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=2810660881:i=141193_2994 on theBenchmark for (2994ds/141193Mi)
% 13.10/3.17 % (916850)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=2845461207:i=141695:sd=1:nm=32:gsp=on:ss=included_2994 on theBenchmark for (2994ds/141695Mi)
% 13.10/3.17 % (916849)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=515737706:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2994 on theBenchmark for (2994ds/134677Mi)
% 13.10/3.17 % (916854)dis-21_1_sil=8000:lcm=predicate:random_seed=3842880741:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2994 on theBenchmark for (2994ds/129Mi)
% 13.10/3.17 % (916852)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=588609778:i=119:av=off:ss=axioms_2994 on theBenchmark for (2994ds/119Mi)
% 13.10/3.17 % (916853)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2634279621:s2a=on:i=139:gtg=position_2994 on theBenchmark for (2994ds/139Mi)
% 13.10/3.17 % (916853)Instruction limit reached!
% 13.10/3.17 % (916853)------------------------------
% 13.10/3.17 % (916853)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.10/3.17 % (916853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.10/3.17 % (916853)CaDiCaL version: 2.1.3
% 13.10/3.17 % (916853)Termination reason: Instruction limit
% 13.10/3.17 % (916853)Termination phase: Property scanning
% 13.10/3.17 % (916853)Time elapsed: 0.060 s
% 13.10/3.17 % (916853)Peak memory usage: 99 MB
% 13.10/3.17 % (916853)Instructions burned: 140 (million)
% 13.10/3.17 % (916852)Instruction limit reached!
% 13.10/3.17 % (916852)------------------------------
% 13.10/3.17 % (916852)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.10/3.17 % (916852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.10/3.17 % (916852)CaDiCaL version: 2.1.3
% 13.10/3.17 % (916852)Termination reason: Instruction limit
% 13.10/3.17 % (916852)Termination phase: Clausification
% 13.10/3.17 % (916852)Time elapsed: 0.099 s
% 13.10/3.17 % (916852)Peak memory usage: 103 MB
% 13.10/3.17 % (916852)Instructions burned: 119 (million)
% 13.10/3.17 % (916854)Instruction limit reached!
% 13.10/3.17 % (916854)------------------------------
% 13.10/3.17 % (916854)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.10/3.17 % (916854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.10/3.17 % (916854)CaDiCaL version: 2.1.3
% 13.10/3.17 % (916854)Termination reason: Instruction limit
% 13.10/3.17 % (916854)Termination phase: Preprocessing 1
% 13.10/3.17 % (916854)Time elapsed: 0.102 s
% 13.10/3.17 % (916854)Peak memory usage: 100 MB
% 13.10/3.17 % (916854)Instructions burned: 130 (million)
% 13.10/3.17 % (916851)------------------------------
% 13.10/3.17 % (916851)------------------------------
% 13.10/3.17 % (916862)lrs+10_1_sil=8000:sp=occurrence:random_seed=1389537946:i=285:sd=3:ss=axioms:sgt=8_2992 on theBenchmark for (2992ds/285Mi)
% 13.10/3.17 % (916865)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=2407476499:s2a=on:i=248:s2at=1.23:gtg=position_2991 on theBenchmark for (2991ds/248Mi)
% 13.10/3.17 % (916864)lrs+1011_1_sil=32000:sp=occurrence:random_seed=4116132331:i=325:sd=1:ss=axioms:sgt=32_2991 on theBenchmark for (2991ds/325Mi)
% 13.10/3.17 % (916863)lrs+10_1_sil=32000:urr=on:br=off:random_seed=500211348:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2991 on theBenchmark for (2991ds/157Mi)
% 20.51/4.29 % (916863)Instruction limit reached!
% 20.51/4.29 % (916863)------------------------------
% 20.51/4.29 % (916863)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.51/4.29 % (916863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.51/4.29 % (916863)CaDiCaL version: 2.1.3
% 20.51/4.29 % (916863)Termination reason: Instruction limit
% 20.51/4.29 % (916863)Termination phase: SInE selection
% 20.51/4.29 % (916863)Time elapsed: 0.071 s
% 20.51/4.29 % (916863)Peak memory usage: 99 MB
% 20.51/4.29 % (916863)Instructions burned: 157 (million)
% 20.51/4.29 % (916865)Instruction limit reached!
% 20.51/4.29 % (916865)------------------------------
% 20.51/4.29 % (916865)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.51/4.29 % (916865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.51/4.29 % (916865)CaDiCaL version: 2.1.3
% 20.51/4.29 % (916865)Termination reason: Instruction limit
% 20.51/4.29 % (916865)Termination phase: Preprocessing 1
% 20.51/4.29 % (916865)Time elapsed: 0.077 s
% 20.51/4.29 % (916865)Peak memory usage: 100 MB
% 20.51/4.29 % (916865)Instructions burned: 248 (million)
% 20.51/4.29 % (916864)Refutation not found, incomplete strategy
% 20.51/4.29 % (916864)------------------------------
% 20.51/4.29 % (916864)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.51/4.29 % (916864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.51/4.29 % (916864)CaDiCaL version: 2.1.3
% 20.51/4.29 % (916864)Termination reason: Refutation not found, incomplete strategy
% 20.51/4.29 % (916864)Time elapsed: 0.078 s
% 20.51/4.29 % (916864)Peak memory usage: 104 MB
% 20.51/4.29 % (916864)Instructions burned: 98 (million)
% 20.51/4.29 % (916862)Instruction limit reached!
% 20.51/4.29 % (916862)------------------------------
% 20.51/4.29 % (916862)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.51/4.29 % (916862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.51/4.29 % (916862)CaDiCaL version: 2.1.3
% 20.51/4.29 % (916862)Termination reason: Instruction limit
% 20.51/4.29 % (916862)Termination phase: Saturation
% 20.51/4.29 % (916862)Time elapsed: 0.174 s
% 20.51/4.29 % (916862)Peak memory usage: 107 MB
% 20.51/4.29 % (916862)Instructions burned: 285 (million)
% 20.51/4.29 % (916871)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2646956889:i=2350_2989 on theBenchmark for (2989ds/2350Mi)
% 20.51/4.29 % (916870)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2326074696:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2989 on theBenchmark for (2989ds/294Mi)
% 20.51/4.29 % (916872)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1339153594:cts=off:i=113:fsr=off:ss=included:sgt=4_2988 on theBenchmark for (2988ds/113Mi)
% 20.51/4.29 % (916864)------------------------------
% 20.51/4.29 % (916864)------------------------------
% 20.51/4.29 % (916870)Instruction limit reached!
% 20.51/4.29 % (916870)------------------------------
% 20.51/4.29 % (916870)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.51/4.29 % (916870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.51/4.29 % (916870)CaDiCaL version: 2.1.3
% 20.51/4.29 % (916870)Termination reason: Instruction limit
% 20.51/4.29 % (916870)Termination phase: Saturation
% 20.51/4.29 % (916870)Time elapsed: 0.178 s
% 20.51/4.29 % (916870)Peak memory usage: 107 MB
% 20.51/4.29 % (916870)Instructions burned: 294 (million)
% 20.51/4.29 % (916872)Instruction limit reached!
% 20.51/4.29 % (916872)------------------------------
% 20.51/4.29 % (916872)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.51/4.29 % (916872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.51/4.29 % (916872)CaDiCaL version: 2.1.3
% 20.51/4.29 % (916872)Termination reason: Instruction limit
% 20.51/4.29 % (916872)Termination phase: Preprocessing 3
% 20.51/4.29 % (916872)Time elapsed: 0.101 s
% 20.51/4.29 % (916872)Peak memory usage: 103 MB
% 20.51/4.29 % (916872)Instructions burned: 113 (million)
% 20.51/4.29 % (916876)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2378572562:i=127:av=off:fsr=off:sup=off_2986 on theBenchmark for (2986ds/127Mi)
% 20.51/4.29 % (916877)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3228193061:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2986 on theBenchmark for (2986ds/114Mi)
% 20.51/4.29 % (916878)lrs+10_1_sil=8000:sp=occurrence:random_seed=919706451:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2985 on theBenchmark for (2985ds/907Mi)
% 17.51/7.91 % (916876)Instruction limit reached!
% 17.51/7.91 % (916876)------------------------------
% 17.51/7.91 % (916876)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.51/7.91 % (916876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.51/7.91 % (916876)CaDiCaL version: 2.1.3
% 17.51/7.91 % (916876)Termination reason: Instruction limit
% 17.51/7.91 % (916876)Termination phase: Preprocessing 2
% 17.51/7.91 % (916876)Time elapsed: 0.105 s
% 17.51/7.91 % (916876)Peak memory usage: 107 MB
% 17.51/7.91 % (916876)Instructions burned: 128 (million)
% 17.51/7.91 % (916877)Instruction limit reached!
% 17.51/7.91 % (916877)------------------------------
% 17.51/7.91 % (916877)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.51/7.91 % (916877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.51/7.91 % (916877)CaDiCaL version: 2.1.3
% 17.51/7.91 % (916877)Termination reason: Instruction limit
% 17.51/7.91 % (916877)Termination phase: Property scanning
% 17.51/7.91 % (916877)Time elapsed: 0.049 s
% 17.51/7.91 % (916877)Peak memory usage: 99 MB
% 17.51/7.91 % (916877)Instructions burned: 114 (million)
% 17.51/7.91 % (916882)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=896479266:i=437:sd=1:aac=none:ss=included_2984 on theBenchmark for (2984ds/437Mi)
% 17.51/7.91 % (916883)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=81939535:i=5202:ss=axioms:sgt=16_2984 on theBenchmark for (2984ds/5202Mi)
% 17.51/7.91 % (916882)Instruction limit reached!
% 17.51/7.91 % (916882)------------------------------
% 17.51/7.91 % (916882)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.51/7.91 % (916882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.51/7.91 % (916882)CaDiCaL version: 2.1.3
% 17.51/7.91 % (916882)Termination reason: Instruction limit
% 17.51/7.91 % (916882)Termination phase: Saturation
% 17.51/7.91 % (916882)Time elapsed: 0.243 s
% 17.51/7.91 % (916882)Peak memory usage: 109 MB
% 17.51/7.91 % (916882)Instructions burned: 439 (million)
% 17.51/7.91 % (916871)Instruction limit reached!
% 17.51/7.91 % (916871)------------------------------
% 17.51/7.91 % (916871)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.51/7.91 % (916871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.51/7.91 % (916871)CaDiCaL version: 2.1.3
% 17.51/7.91 % (916871)Termination reason: Instruction limit
% 17.51/7.91 % (916871)Termination phase: Saturation
% 17.51/7.91 % (916871)Time elapsed: 0.939 s
% 17.51/7.91 % (916871)Peak memory usage: 265 MB
% 17.51/7.91 % (916871)Instructions burned: 2351 (million)
% 17.51/7.91 % (916878)Instruction limit reached!
% 17.51/7.91 % (916878)------------------------------
% 17.51/7.91 % (916878)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.51/7.91 % (916878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.51/7.91 % (916878)CaDiCaL version: 2.1.3
% 17.51/7.91 % (916878)Termination reason: Instruction limit
% 17.51/7.91 % (916878)Termination phase: Saturation
% 17.51/7.91 % (916878)Time elapsed: 0.562 s
% 17.51/7.91 % (916878)Peak memory usage: 118 MB
% 17.51/7.91 % (916878)Instructions burned: 908 (million)
% 17.51/7.91 % (916886)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3920497561:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2980 on theBenchmark for (2980ds/134Mi)
% 17.51/7.91 % (916886)Instruction limit reached!
% 17.51/7.91 % (916886)------------------------------
% 17.51/7.91 % (916886)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.51/7.91 % (916886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.51/7.91 % (916886)CaDiCaL version: 2.1.3
% 17.51/7.91 % (916886)Termination reason: Instruction limit
% 17.51/7.91 % (916886)Termination phase: NewCNF
% 17.51/7.91 % (916886)Time elapsed: 0.064 s
% 17.51/7.91 % (916886)Peak memory usage: 104 MB
% 17.51/7.91 % (916886)Instructions burned: 137 (million)
% 17.51/7.91 % (916889)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2404629601:st=3:i=13193:sd=3:ss=axioms_2978 on theBenchmark for (2978ds/13193Mi)
% 17.51/7.91 % (916888)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=216900225:st=8:i=592:sd=3:ep=RST:ss=axioms_2978 on theBenchmark for (2978ds/592Mi)
% 17.51/7.91 % (916890)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=3219034542:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2977 on theBenchmark for (2977ds/125Mi)
% 17.51/7.91 % (916890)Instruction limit reached!
% 17.51/7.91 % (916890)------------------------------
% 17.51/7.91 % (916890)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.51/7.91 % (916890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.51/7.91 % (916890)CaDiCaL version: 2.1.3
% 17.51/7.91 % (916890)Termination reason: Instruction limit
% 17.51/7.91 % (916890)Termination phase: Property scanning
% 17.51/7.91 % (916890)Time elapsed: 0.029 s
% 17.51/7.91 % (916890)Peak memory usage: 99 MB
% 17.51/7.91 % (916890)Instructions burned: 128 (million)
% 17.51/7.91 % (916894)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1111201229:i=134:gtgl=5:slsql=off:gtg=exists_sym_2976 on theBenchmark for (2976ds/134Mi)
% 17.51/7.91 % (916894)Instruction limit reached!
% 17.51/7.91 % (916894)------------------------------
% 17.51/7.91 % (916894)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.51/7.91 % (916894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.51/7.91 % (916894)CaDiCaL version: 2.1.3
% 17.51/7.91 % (916894)Termination reason: Instruction limit
% 17.51/7.91 % (916894)Termination phase: Property scanning
% 17.51/7.91 % (916894)Time elapsed: 0.033 s
% 17.51/7.91 % (916894)Peak memory usage: 99 MB
% 17.51/7.91 % (916894)Instructions burned: 137 (million)
% 17.51/7.91 % (916896)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1561384321:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2974 on theBenchmark for (2974ds/141Mi)
% 17.51/7.91 % (916888)Instruction limit reached!
% 17.51/7.91 % (916888)------------------------------
% 17.51/7.91 % (916888)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.51/7.91 % (916888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.51/7.91 % (916888)CaDiCaL version: 2.1.3
% 17.51/7.91 % (916888)Termination reason: Instruction limit
% 17.51/7.91 % (916888)Termination phase: Property scanning
% 17.51/7.91 % (916888)Time elapsed: 0.395 s
% 17.51/7.91 % (916888)Peak memory usage: 118 MB
% 17.51/7.91 % (916888)Instructions burned: 594 (million)
% 17.51/7.91 % (916896)Refutation not found, incomplete strategy
% 17.51/7.91 % (916896)------------------------------
% 17.51/7.91 % (916896)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.51/7.91 % (916896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.51/7.91 % (916896)CaDiCaL version: 2.1.3
% 17.51/7.91 % (916896)Termination reason: Refutation not found, incomplete strategy
% 17.51/7.91 % (916896)Time elapsed: 0.033 s
% 17.51/7.91 % (916896)Peak memory usage: 103 MB
% 17.51/7.91 % (916896)Instructions burned: 65 (million)
% 17.51/7.91 % (916896)------------------------------
% 17.51/7.91 % (916896)------------------------------
% 17.51/7.91 % (916898)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2889497860:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2972 on theBenchmark for (2972ds/431Mi)
% 17.51/7.91 % (916899)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=3471851171:i=6060:aac=none:ins=25_2971 on theBenchmark for (2971ds/6060Mi)
% 17.51/7.91 % (916898)Instruction limit reached!
% 17.51/7.91 % (916898)------------------------------
% 17.51/7.91 % (916898)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.51/7.91 % (916898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.51/7.91 % (916898)CaDiCaL version: 2.1.3
% 17.51/7.91 % (916898)Termination reason: Instruction limit
% 17.51/7.91 % (916898)Termination phase: Saturation
% 17.51/7.91 % (916898)Time elapsed: 0.282 s
% 17.51/7.91 % (916898)Peak memory usage: 108 MB
% 17.51/7.91 % (916898)Instructions burned: 436 (million)
% 17.51/7.91 % (916902)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=2416775753:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2968 on theBenchmark for (2968ds/150Mi)
% 17.51/7.91 % (916902)Instruction limit reached!
% 17.51/7.91 % (916902)------------------------------
% 17.51/7.91 % (916902)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.51/7.91 % (916902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.51/7.91 % (916902)CaDiCaL version: 2.1.3
% 17.51/7.91 % (916902)Termination reason: Instruction limit
% 17.51/7.91 % (916902)Termination phase: Unused predicate definition removal
% 17.51/7.91 % (916902)Time elapsed: 0.118 s
% 17.51/7.91 % (916902)Peak memory usage: 101 MB
% 17.51/7.91 % (916902)Instructions burned: 150 (million)
% 17.51/7.91 % (916904)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3933660836:i=14155:bd=all_2965 on theBenchmark for (2965ds/14155Mi)
% 17.51/7.91 % (916883)Instruction limit reached!
% 17.51/7.91 % (916883)------------------------------
% 17.51/7.91 % (916883)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.51/7.91 % (916883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.51/7.91 % (916883)CaDiCaL version: 2.1.3
% 17.51/7.91 % (916883)Termination reason: Instruction limit
% 17.51/7.91 % (916883)Termination phase: Saturation
% 17.51/7.91 % (916883)Time elapsed: 3.043 s
% 17.51/7.91 % (916883)Peak memory usage: 199 MB
% 17.51/7.91 % (916883)Instructions burned: 5202 (million)
% 17.51/7.91 % (916906)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1871052228:i=667:av=off:fsr=off_2951 on theBenchmark for (2951ds/667Mi)
% 17.51/7.91 % (916906)Instruction limit reached!
% 17.51/7.91 % (916906)------------------------------
% 17.51/7.91 % (916906)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.51/7.91 % (916906)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.51/7.91 % (916906)CaDiCaL version: 2.1.3
% 17.51/7.91 % (916906)Termination reason: Instruction limit
% 17.51/7.91 % (916906)Termination phase: NewCNF
% 17.51/7.91 % (916906)Time elapsed: 0.482 s
% 17.51/7.91 % (916906)Peak memory usage: 128 MB
% 17.51/7.91 % (916906)Instructions burned: 667 (million)
% 17.51/7.91 % (916899)Instruction limit reached!
% 17.51/7.91 % (916899)------------------------------
% 17.51/7.91 % (916899)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.51/7.91 % (916899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.51/7.91 % (916899)CaDiCaL version: 2.1.3
% 17.51/7.91 % (916899)Termination reason: Instruction limit
% 17.51/7.91 % (916899)Termination phase: Saturation
% 17.51/7.91 % (916899)Time elapsed: 2.604 s
% 17.51/7.91 % (916899)Peak memory usage: 402 MB
% 17.51/7.91 % (916899)Instructions burned: 6063 (million)
% 17.51/7.91 % (916908)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=1405897711:s2a=on:i=185:s2at=1.8:fdi=4_2945 on theBenchmark for (2945ds/185Mi)
% 17.51/7.91 % (916909)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=3171079290:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2943 on theBenchmark for (2943ds/193Mi)
% 17.51/7.91 % (916908)Instruction limit reached!
% 17.51/7.91 % (916908)------------------------------
% 17.51/7.91 % (916908)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.51/7.91 % (916908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.51/7.91 % (916908)CaDiCaL version: 2.1.3
% 17.51/7.91 % (916908)Termination reason: Instruction limit
% 17.51/7.91 % (916908)Termination phase: Preprocessing 2
% 17.51/7.91 % (916908)Time elapsed: 0.154 s
% 17.51/7.91 % (916908)Peak memory usage: 102 MB
% 17.51/7.91 % (916908)Instructions burned: 185 (million)
% 17.51/7.91 % (916909)Instruction limit reached!
% 17.51/7.91 % (916909)------------------------------
% 17.51/7.91 % (916909)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.51/7.91 % (916909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.51/7.91 % (916909)CaDiCaL version: 2.1.3
% 17.51/7.91 % (916909)Termination reason: Instruction limit
% 17.51/7.91 % (916909)Termination phase: Property scanning
% 17.51/7.91 % (916909)Time elapsed: 0.088 s
% 17.51/7.91 % (916909)Peak memory usage: 103 MB
% 17.51/7.91 % (916909)Instructions burned: 196 (million)
% 17.51/7.91 % (916912)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=642059415:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2941 on theBenchmark for (2941ds/4850Mi)
% 17.51/7.91 % (916913)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=2186610661:i=12111:sd=1:ss=included_2941 on theBenchmark for (2941ds/12111Mi)
% 17.51/7.91 % (916913)First to succeed.
% 17.51/7.91 % (916913)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-916843"
% 17.51/7.91 % (916913)Refutation found. Thanks to Tanya!
% 17.51/7.91 % SZS status Theorem for theBenchmark
% 17.51/7.91 % SZS output start Proof for theBenchmark
% See solution above
% 47.13/8.11 % (916913)------------------------------
% 47.13/8.11 % (916913)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.13/8.11 % (916913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.13/8.11 % (916913)CaDiCaL version: 2.1.3
% 47.13/8.11 % (916913)Termination reason: Refutation
% 47.13/8.11 % (916913)Time elapsed: 0.863 s
% 47.13/8.11 % (916913)Peak memory usage: 172 MB
% 47.13/8.11 % (916913)Instructions burned: 2343 (million)
% 47.13/8.11 % (916913)------------------------------
% 47.13/8.11 % (916913)------------------------------
% 47.13/8.11 % (916843)Success in time 7.059 s
% 47.13/8.11 % Vampire exiting
%------------------------------------------------------------------------------