%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT370+4 : 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 : n020.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:27 AM UTC 2026
% Result : Theorem 40.36s 16.45s
% Output : Refutation 78.23s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 60
% Syntax : Number of formulae : 449 ( 83 unt; 44 def)
% Number of atoms : 3020 ( 69 equ)
% Maximal formula atoms : 25 ( 6 avg)
% Number of connectives : 4668 (2097 ~;2203 |; 291 &)
% ( 44 <=>; 33 =>; 0 <=; 0 <~>)
% Maximal formula depth : 28 ( 8 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 76 ( 74 usr; 41 prp; 0-3 aty)
% Number of functors : 12 ( 12 usr; 5 con; 0-3 aty)
% Number of variables : 309 ( 0 sgn 305 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1483,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(f28604,axiom,
! [X0] :
( l1_orders_2(X0)
=> ( v1_lattice3(X0)
=> ~ v3_struct_0(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc1_lattice3) ).
fof(f39770,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(f40126,axiom,
! [X0,X1,X2] :
( ( ~ v3_struct_0(X0)
& l1_orders_2(X0)
& ~ v3_struct_0(X1)
& l1_orders_2(X1)
& v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> ( ~ v3_struct_0(k2_yellow_2(X0,X1,X2))
& v1_orders_2(k2_yellow_2(X0,X1,X2))
& v4_yellow_0(k2_yellow_2(X0,X1,X2),X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc2_yellow_2) ).
fof(f40196,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(f40217,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(f40224,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(f40282,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(f40284,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(f40339,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(f41701,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_orders_2(X0) )
=> ( ~ v1_xboole_0(k7_grcat_1(X0))
& v1_relat_1(k7_grcat_1(X0))
& v1_funct_1(k7_grcat_1(X0))
& v1_funct_2(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))
& v5_orders_3(k7_grcat_1(X0),X0,X0)
& v1_partfun1(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_waybel_9) ).
fof(f55730,axiom,
! [X0] :
( ( v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& v2_lattice3(X0)
& v3_lattice3(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( ( v2_orders_2(X1)
& v3_orders_2(X1)
& v4_orders_2(X1)
& v1_lattice3(X1)
& v2_lattice3(X1)
& v3_lattice3(X1)
& v3_waybel_3(X1)
& l1_orders_2(X1) )
=> ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v17_waybel_0(X2,X0,X1)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> ( v1_waybel34(k1_waybel34(X0,X1,X2),X1,X0)
=> v22_waybel_0(X2,X0,X1) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t25_waybel34) ).
fof(f55740,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(f55747,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(f55748,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(f55751,conjecture,
! [X0] :
( ( v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& v2_lattice3(X0)
& v3_lattice3(X0)
& v3_waybel_3(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( ( v1_funct_1(X1)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v7_waybel_1(X1,X0)
& m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
=> ( v1_waybel34(k2_waybel_1(X0,X0,X1),X0,k2_yellow_2(X0,X0,X1))
=> v4_waybel_0(k2_yellow_2(X0,X0,X1),X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t43_waybel34) ).
fof(f55752,negated_conjecture,
~ ! [X0] :
( ( v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& v2_lattice3(X0)
& v3_lattice3(X0)
& v3_waybel_3(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( ( v1_funct_1(X1)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v7_waybel_1(X1,X0)
& m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
=> ( v1_waybel34(k2_waybel_1(X0,X0,X1),X0,k2_yellow_2(X0,X0,X1))
=> v4_waybel_0(k2_yellow_2(X0,X0,X1),X0) ) ) ),
inference(negated_conjecture,[status(cth)],[f55751]) ).
fof(f55880,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( v22_waybel_0(X2,X0,X1)
| ~ v1_waybel34(k1_waybel34(X0,X1,X2),X1,X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v17_waybel_0(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ v3_lattice3(X1)
| ~ v3_waybel_3(X1)
| ~ l1_orders_2(X1) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f55730]) ).
fof(f55881,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( v22_waybel_0(X2,X0,X1)
| ~ v1_waybel34(k1_waybel34(X0,X1,X2),X1,X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v17_waybel_0(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ v3_lattice3(X1)
| ~ v3_waybel_3(X1)
| ~ l1_orders_2(X1) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f55880]) ).
fof(f55899,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,[],[f55740]) ).
fof(f55900,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,[],[f55899]) ).
fof(f55913,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,[],[f55747]) ).
fof(f55914,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,[],[f55913]) ).
fof(f55915,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,[],[f55748]) ).
fof(f55916,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,[],[f55915]) ).
fof(f55921,plain,
? [X0] :
( ? [X1] :
( ~ v4_waybel_0(k2_yellow_2(X0,X0,X1),X0)
& v1_waybel34(k2_waybel_1(X0,X0,X1),X0,k2_yellow_2(X0,X0,X1))
& v1_funct_1(X1)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v7_waybel_1(X1,X0)
& m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
& v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& v2_lattice3(X0)
& v3_lattice3(X0)
& v3_waybel_3(X0)
& l1_orders_2(X0) ),
inference(ennf_transformation,[],[f55752]) ).
fof(f55922,plain,
? [X0] :
( ? [X1] :
( ~ v4_waybel_0(k2_yellow_2(X0,X0,X1),X0)
& v1_waybel34(k2_waybel_1(X0,X0,X1),X0,k2_yellow_2(X0,X0,X1))
& v1_funct_1(X1)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v7_waybel_1(X1,X0)
& m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
& v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& v2_lattice3(X0)
& v3_lattice3(X0)
& v3_waybel_3(X0)
& l1_orders_2(X0) ),
inference(flattening,[],[f55921]) ).
fof(f55931,plain,
! [X0] :
( ~ v3_struct_0(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f28604]) ).
fof(f55932,plain,
! [X0] :
( ~ v3_struct_0(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f55931]) ).
fof(f56421,plain,
! [X0] :
( ( ~ v1_xboole_0(k7_grcat_1(X0))
& v1_relat_1(k7_grcat_1(X0))
& v1_funct_1(k7_grcat_1(X0))
& v1_funct_2(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))
& v5_orders_3(k7_grcat_1(X0),X0,X0)
& v1_partfun1(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f41701]) ).
fof(f56422,plain,
! [X0] :
( ( ~ v1_xboole_0(k7_grcat_1(X0))
& v1_relat_1(k7_grcat_1(X0))
& v1_funct_1(k7_grcat_1(X0))
& v1_funct_2(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))
& v5_orders_3(k7_grcat_1(X0),X0,X0)
& v1_partfun1(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f56421]) ).
fof(f57026,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,[],[f40196]) ).
fof(f57027,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,[],[f57026]) ).
fof(f57028,plain,
! [X0,X1,X2] :
( ( ~ v3_struct_0(k2_yellow_2(X0,X1,X2))
& v1_orders_2(k2_yellow_2(X0,X1,X2))
& v4_yellow_0(k2_yellow_2(X0,X1,X2),X1) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| v3_struct_0(X1)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(ennf_transformation,[],[f40126]) ).
fof(f57029,plain,
! [X0,X1,X2] :
( ( ~ v3_struct_0(k2_yellow_2(X0,X1,X2))
& v1_orders_2(k2_yellow_2(X0,X1,X2))
& v4_yellow_0(k2_yellow_2(X0,X1,X2),X1) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| v3_struct_0(X1)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(flattening,[],[f57028]) ).
fof(f57223,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,[],[f40217]) ).
fof(f57224,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,[],[f57223]) ).
fof(f57259,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,[],[f40282]) ).
fof(f57260,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,[],[f57259]) ).
fof(f57269,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,[],[f40339]) ).
fof(f57270,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,[],[f57269]) ).
fof(f57281,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,[],[f40284]) ).
fof(f57282,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,[],[f57281]) ).
fof(f57283,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,[],[f40224]) ).
fof(f57284,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,[],[f57283]) ).
fof(f57288,plain,
! [X0] :
( ! [X1] :
( l1_orders_2(X1)
| ~ m1_yellow_0(X1,X0) )
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f39770]) ).
fof(f57392,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(f57393,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,[],[f55900,f57392]) ).
fof(f57586,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,[],[f57392]) ).
fof(f57587,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,[],[f57586]) ).
fof(f57598,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,[],[f55916]) ).
fof(f57603,plain,
( ~ v4_waybel_0(k2_yellow_2(sK119,sK119,sK120),sK119)
& v1_waybel34(k2_waybel_1(sK119,sK119,sK120),sK119,k2_yellow_2(sK119,sK119,sK120))
& v1_funct_1(sK120)
& v1_funct_2(sK120,u1_struct_0(sK119),u1_struct_0(sK119))
& v7_waybel_1(sK120,sK119)
& m2_relset_1(sK120,u1_struct_0(sK119),u1_struct_0(sK119))
& v2_orders_2(sK119)
& v3_orders_2(sK119)
& v4_orders_2(sK119)
& v1_lattice3(sK119)
& v2_lattice3(sK119)
& v3_lattice3(sK119)
& v3_waybel_3(sK119)
& l1_orders_2(sK119) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK119,sK120]),skolemize(X0,sK119),skolemize(X1,sK120)],[f55922]) ).
fof(f57609,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,[],[f1483]) ).
fof(f58373,plain,
! [X2,X0,X1] :
( ~ v3_waybel_3(X1)
| ~ v1_waybel34(k1_waybel34(X0,X1,X2),X1,X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v17_waybel_0(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ v3_lattice3(X1)
| v22_waybel_0(X2,X0,X1)
| ~ l1_orders_2(X1)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f55881]) ).
fof(f58405,plain,
! [X0,X1] :
( ~ sP19(X0,X1)
| v3_lattice3(k2_yellow_2(X1,X1,X0)) ),
inference(cnf_transformation,[],[f57587]) ).
fof(f58406,plain,
! [X0,X1] :
( ~ sP19(X0,X1)
| v2_lattice3(k2_yellow_2(X1,X1,X0)) ),
inference(cnf_transformation,[],[f57587]) ).
fof(f58407,plain,
! [X0,X1] :
( ~ sP19(X0,X1)
| v1_lattice3(k2_yellow_2(X1,X1,X0)) ),
inference(cnf_transformation,[],[f57587]) ).
fof(f58414,plain,
! [X0,X1] :
( ~ sP19(X0,X1)
| v4_orders_2(k2_yellow_2(X1,X1,X0)) ),
inference(cnf_transformation,[],[f57587]) ).
fof(f58415,plain,
! [X0,X1] :
( ~ sP19(X0,X1)
| v3_orders_2(k2_yellow_2(X1,X1,X0)) ),
inference(cnf_transformation,[],[f57587]) ).
fof(f58416,plain,
! [X0,X1] :
( ~ sP19(X0,X1)
| v2_orders_2(k2_yellow_2(X1,X1,X0)) ),
inference(cnf_transformation,[],[f57587]) ).
fof(f58419,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,[],[f57393]) ).
fof(f58450,plain,
! [X0,X1] :
( ~ l1_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v7_waybel_1(X1,X0)
| ~ 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)
| k2_waybel_1(X0,X0,X1) = k1_waybel34(k2_yellow_2(X0,X0,X1),X0,k3_waybel_1(X0,X0,X1)) ),
inference(cnf_transformation,[],[f55914]) ).
fof(f58452,plain,
! [X0,X1] :
( ~ l1_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v7_waybel_1(X1,X0)
| ~ 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)
| v17_waybel_0(k3_waybel_1(X0,X0,X1),k2_yellow_2(X0,X0,X1),X0) ),
inference(cnf_transformation,[],[f55914]) ).
fof(f58455,plain,
! [X0,X1] :
( ~ v3_lattice3(X0)
| ~ v22_waybel_0(k3_waybel_1(X0,X0,X1),k2_yellow_2(X0,X0,X1),X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v7_waybel_1(X1,X0)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| v4_waybel_0(k2_yellow_2(X0,X0,X1),X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f57598]) ).
fof(f58470,plain,
l1_orders_2(sK119),
inference(cnf_transformation,[],[f57603]) ).
fof(f58471,plain,
v3_waybel_3(sK119),
inference(cnf_transformation,[],[f57603]) ).
fof(f58472,plain,
v3_lattice3(sK119),
inference(cnf_transformation,[],[f57603]) ).
fof(f58473,plain,
v2_lattice3(sK119),
inference(cnf_transformation,[],[f57603]) ).
fof(f58474,plain,
v1_lattice3(sK119),
inference(cnf_transformation,[],[f57603]) ).
fof(f58475,plain,
v4_orders_2(sK119),
inference(cnf_transformation,[],[f57603]) ).
fof(f58476,plain,
v3_orders_2(sK119),
inference(cnf_transformation,[],[f57603]) ).
fof(f58477,plain,
v2_orders_2(sK119),
inference(cnf_transformation,[],[f57603]) ).
fof(f58478,plain,
m2_relset_1(sK120,u1_struct_0(sK119),u1_struct_0(sK119)),
inference(cnf_transformation,[],[f57603]) ).
fof(f58479,plain,
v7_waybel_1(sK120,sK119),
inference(cnf_transformation,[],[f57603]) ).
fof(f58480,plain,
v1_funct_2(sK120,u1_struct_0(sK119),u1_struct_0(sK119)),
inference(cnf_transformation,[],[f57603]) ).
fof(f58481,plain,
v1_funct_1(sK120),
inference(cnf_transformation,[],[f57603]) ).
fof(f58482,plain,
v1_waybel34(k2_waybel_1(sK119,sK119,sK120),sK119,k2_yellow_2(sK119,sK119,sK120)),
inference(cnf_transformation,[],[f57603]) ).
fof(f58483,plain,
~ v4_waybel_0(k2_yellow_2(sK119,sK119,sK120),sK119),
inference(cnf_transformation,[],[f57603]) ).
fof(f58505,plain,
! [X2,X0,X1] :
( m1_relset_1(X2,X0,X1)
| ~ m2_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f57609]) ).
fof(f58515,plain,
! [X0] :
( ~ v1_lattice3(X0)
| ~ v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f55932]) ).
fof(f59283,plain,
! [X0] :
( v1_funct_1(k7_grcat_1(X0))
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f56422]) ).
fof(f60354,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,[],[f57027]) ).
fof(f60359,plain,
! [X2,X0,X1] :
( ~ l1_orders_2(X0)
| v3_struct_0(X0)
| ~ v3_struct_0(k2_yellow_2(X0,X1,X2))
| 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,[],[f57029]) ).
fof(f60691,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,[],[f57224]) ).
fof(f60781,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,[],[f57260]) ).
fof(f60791,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,[],[f57270]) ).
fof(f60799,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,[],[f57282]) ).
fof(f60802,plain,
! [X2,X0,X1] :
( ~ l1_orders_2(X0)
| 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))
| 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,[],[f57284]) ).
fof(f60810,plain,
! [X0,X1] :
( ~ l1_orders_2(X0)
| ~ m1_yellow_0(X1,X0)
| l1_orders_2(X1) ),
inference(cnf_transformation,[],[f57288]) ).
fof(f61186,definition,
sF381 = k2_yellow_2(sK119,sK119,sK120),
introduced(definition,[new_symbols(definition,[sF381])],[function_definition]) ).
fof(f61187,plain,
k2_yellow_2(sK119,sK119,sK120) = sF381,
inference(reorient_equations,[],[f61186]) ).
fof(f61188,plain,
~ v4_waybel_0(sF381,sK119),
inference(definition_folding,[],[f58483,f61187]) ).
fof(f61189,definition,
sF382 = k2_waybel_1(sK119,sK119,sK120),
introduced(definition,[new_symbols(definition,[sF382])],[function_definition]) ).
fof(f61190,plain,
k2_waybel_1(sK119,sK119,sK120) = sF382,
inference(reorient_equations,[],[f61189]) ).
fof(f61191,plain,
v1_waybel34(sF382,sK119,sF381),
inference(definition_folding,[],[f58482,f61187,f61190]) ).
fof(f61192,definition,
sF383 = u1_struct_0(sK119),
introduced(definition,[new_symbols(definition,[sF383])],[function_definition]) ).
fof(f61193,plain,
u1_struct_0(sK119) = sF383,
inference(reorient_equations,[],[f61192]) ).
fof(f61194,plain,
v1_funct_2(sK120,sF383,sF383),
inference(definition_folding,[],[f58480,f61193,f61193]) ).
fof(f61195,plain,
m2_relset_1(sK120,sF383,sF383),
inference(definition_folding,[],[f58478,f61193,f61193]) ).
fof(f62172,definition,
( spl384_185
<=> l1_orders_2(sK119) ),
introduced(definition,[new_symbols(definition,[spl384_185])],[avatar_definition]) ).
fof(f62174,plain,
( l1_orders_2(sK119)
| ~ spl384_185 ),
inference(avatar_component_clause,[],[f62172]) ).
fof(f62175,plain,
spl384_185,
inference(avatar_split_clause,[],[f58470,f62172]) ).
fof(f62177,definition,
( spl384_186
<=> v3_waybel_3(sK119) ),
introduced(definition,[new_symbols(definition,[spl384_186])],[avatar_definition]) ).
fof(f62179,plain,
( v3_waybel_3(sK119)
| ~ spl384_186 ),
inference(avatar_component_clause,[],[f62177]) ).
fof(f62180,plain,
spl384_186,
inference(avatar_split_clause,[],[f58471,f62177]) ).
fof(f62182,definition,
( spl384_187
<=> v3_lattice3(sK119) ),
introduced(definition,[new_symbols(definition,[spl384_187])],[avatar_definition]) ).
fof(f62184,plain,
( v3_lattice3(sK119)
| ~ spl384_187 ),
inference(avatar_component_clause,[],[f62182]) ).
fof(f62185,plain,
spl384_187,
inference(avatar_split_clause,[],[f58472,f62182]) ).
fof(f62187,definition,
( spl384_188
<=> v2_lattice3(sK119) ),
introduced(definition,[new_symbols(definition,[spl384_188])],[avatar_definition]) ).
fof(f62189,plain,
( v2_lattice3(sK119)
| ~ spl384_188 ),
inference(avatar_component_clause,[],[f62187]) ).
fof(f62190,plain,
spl384_188,
inference(avatar_split_clause,[],[f58473,f62187]) ).
fof(f62192,definition,
( spl384_189
<=> v1_lattice3(sK119) ),
introduced(definition,[new_symbols(definition,[spl384_189])],[avatar_definition]) ).
fof(f62194,plain,
( v1_lattice3(sK119)
| ~ spl384_189 ),
inference(avatar_component_clause,[],[f62192]) ).
fof(f62195,plain,
spl384_189,
inference(avatar_split_clause,[],[f58474,f62192]) ).
fof(f62197,definition,
( spl384_190
<=> v4_orders_2(sK119) ),
introduced(definition,[new_symbols(definition,[spl384_190])],[avatar_definition]) ).
fof(f62199,plain,
( v4_orders_2(sK119)
| ~ spl384_190 ),
inference(avatar_component_clause,[],[f62197]) ).
fof(f62200,plain,
spl384_190,
inference(avatar_split_clause,[],[f58475,f62197]) ).
fof(f62202,definition,
( spl384_191
<=> v3_orders_2(sK119) ),
introduced(definition,[new_symbols(definition,[spl384_191])],[avatar_definition]) ).
fof(f62204,plain,
( v3_orders_2(sK119)
| ~ spl384_191 ),
inference(avatar_component_clause,[],[f62202]) ).
fof(f62205,plain,
spl384_191,
inference(avatar_split_clause,[],[f58476,f62202]) ).
fof(f62207,definition,
( spl384_192
<=> v2_orders_2(sK119) ),
introduced(definition,[new_symbols(definition,[spl384_192])],[avatar_definition]) ).
fof(f62209,plain,
( v2_orders_2(sK119)
| ~ spl384_192 ),
inference(avatar_component_clause,[],[f62207]) ).
fof(f62210,plain,
spl384_192,
inference(avatar_split_clause,[],[f58477,f62207]) ).
fof(f62212,definition,
( spl384_193
<=> m2_relset_1(sK120,sF383,sF383) ),
introduced(definition,[new_symbols(definition,[spl384_193])],[avatar_definition]) ).
fof(f62214,plain,
( m2_relset_1(sK120,sF383,sF383)
| ~ spl384_193 ),
inference(avatar_component_clause,[],[f62212]) ).
fof(f62215,plain,
spl384_193,
inference(avatar_split_clause,[],[f61195,f62212]) ).
fof(f62217,definition,
( spl384_194
<=> v7_waybel_1(sK120,sK119) ),
introduced(definition,[new_symbols(definition,[spl384_194])],[avatar_definition]) ).
fof(f62219,plain,
( v7_waybel_1(sK120,sK119)
| ~ spl384_194 ),
inference(avatar_component_clause,[],[f62217]) ).
fof(f62220,plain,
spl384_194,
inference(avatar_split_clause,[],[f58479,f62217]) ).
fof(f62222,definition,
( spl384_195
<=> v1_funct_2(sK120,sF383,sF383) ),
introduced(definition,[new_symbols(definition,[spl384_195])],[avatar_definition]) ).
fof(f62224,plain,
( v1_funct_2(sK120,sF383,sF383)
| ~ spl384_195 ),
inference(avatar_component_clause,[],[f62222]) ).
fof(f62225,plain,
spl384_195,
inference(avatar_split_clause,[],[f61194,f62222]) ).
fof(f62227,definition,
( spl384_196
<=> v1_funct_1(sK120) ),
introduced(definition,[new_symbols(definition,[spl384_196])],[avatar_definition]) ).
fof(f62229,plain,
( v1_funct_1(sK120)
| ~ spl384_196 ),
inference(avatar_component_clause,[],[f62227]) ).
fof(f62230,plain,
spl384_196,
inference(avatar_split_clause,[],[f58481,f62227]) ).
fof(f62232,definition,
( spl384_197
<=> v1_waybel34(sF382,sK119,sF381) ),
introduced(definition,[new_symbols(definition,[spl384_197])],[avatar_definition]) ).
fof(f62234,plain,
( v1_waybel34(sF382,sK119,sF381)
| ~ spl384_197 ),
inference(avatar_component_clause,[],[f62232]) ).
fof(f62235,plain,
spl384_197,
inference(avatar_split_clause,[],[f61191,f62232]) ).
fof(f62237,definition,
( spl384_198
<=> v4_waybel_0(sF381,sK119) ),
introduced(definition,[new_symbols(definition,[spl384_198])],[avatar_definition]) ).
fof(f62239,plain,
( ~ v4_waybel_0(sF381,sK119)
| spl384_198 ),
inference(avatar_component_clause,[],[f62237]) ).
fof(f62240,plain,
~ spl384_198,
inference(avatar_split_clause,[],[f61188,f62237]) ).
fof(f62251,definition,
( spl384_199
<=> k2_yellow_2(sK119,sK119,sK120) = sF381 ),
introduced(definition,[new_symbols(definition,[spl384_199])],[avatar_definition]) ).
fof(f62253,plain,
( k2_yellow_2(sK119,sK119,sK120) = sF381
| ~ spl384_199 ),
inference(avatar_component_clause,[],[f62251]) ).
fof(f62254,plain,
spl384_199,
inference(avatar_split_clause,[],[f61187,f62251]) ).
fof(f62256,definition,
( spl384_200
<=> k2_waybel_1(sK119,sK119,sK120) = sF382 ),
introduced(definition,[new_symbols(definition,[spl384_200])],[avatar_definition]) ).
fof(f62258,plain,
( k2_waybel_1(sK119,sK119,sK120) = sF382
| ~ spl384_200 ),
inference(avatar_component_clause,[],[f62256]) ).
fof(f62259,plain,
spl384_200,
inference(avatar_split_clause,[],[f61190,f62256]) ).
fof(f62261,definition,
( spl384_201
<=> u1_struct_0(sK119) = sF383 ),
introduced(definition,[new_symbols(definition,[spl384_201])],[avatar_definition]) ).
fof(f62263,plain,
( u1_struct_0(sK119) = sF383
| ~ spl384_201 ),
inference(avatar_component_clause,[],[f62261]) ).
fof(f62264,plain,
spl384_201,
inference(avatar_split_clause,[],[f61193,f62261]) ).
fof(f62322,plain,
( ! [X0] :
( ~ v22_waybel_0(k3_waybel_1(sK119,sK119,X0),k2_yellow_2(sK119,sK119,X0),sK119)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK119),u1_struct_0(sK119))
| ~ v7_waybel_1(X0,sK119)
| ~ m2_relset_1(X0,u1_struct_0(sK119),u1_struct_0(sK119))
| ~ v2_orders_2(sK119)
| ~ v3_orders_2(sK119)
| ~ v4_orders_2(sK119)
| ~ v1_lattice3(sK119)
| ~ v2_lattice3(sK119)
| v4_waybel_0(k2_yellow_2(sK119,sK119,X0),sK119)
| ~ l1_orders_2(sK119) )
| ~ spl384_187 ),
inference(resolution,[],[f58455,f62184]) ).
fof(f62323,plain,
( ! [X0] :
( ~ v22_waybel_0(k3_waybel_1(sK119,sK119,X0),k2_yellow_2(sK119,sK119,X0),sK119)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK119),u1_struct_0(sK119))
| ~ v7_waybel_1(X0,sK119)
| ~ m2_relset_1(X0,u1_struct_0(sK119),u1_struct_0(sK119))
| ~ v3_orders_2(sK119)
| ~ v4_orders_2(sK119)
| ~ v1_lattice3(sK119)
| ~ v2_lattice3(sK119)
| v4_waybel_0(k2_yellow_2(sK119,sK119,X0),sK119)
| ~ l1_orders_2(sK119) )
| ~ spl384_187
| ~ spl384_192 ),
inference(forward_subsumption_resolution,[],[f62322,f62209]) ).
fof(f62324,plain,
( ! [X0] :
( ~ v22_waybel_0(k3_waybel_1(sK119,sK119,X0),k2_yellow_2(sK119,sK119,X0),sK119)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK119),u1_struct_0(sK119))
| ~ v7_waybel_1(X0,sK119)
| ~ m2_relset_1(X0,u1_struct_0(sK119),u1_struct_0(sK119))
| ~ v4_orders_2(sK119)
| ~ v1_lattice3(sK119)
| ~ v2_lattice3(sK119)
| v4_waybel_0(k2_yellow_2(sK119,sK119,X0),sK119)
| ~ l1_orders_2(sK119) )
| ~ spl384_187
| ~ spl384_191
| ~ spl384_192 ),
inference(forward_subsumption_resolution,[],[f62323,f62204]) ).
fof(f62325,plain,
( ! [X0] :
( ~ v22_waybel_0(k3_waybel_1(sK119,sK119,X0),k2_yellow_2(sK119,sK119,X0),sK119)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK119),u1_struct_0(sK119))
| ~ v7_waybel_1(X0,sK119)
| ~ m2_relset_1(X0,u1_struct_0(sK119),u1_struct_0(sK119))
| ~ v1_lattice3(sK119)
| ~ v2_lattice3(sK119)
| v4_waybel_0(k2_yellow_2(sK119,sK119,X0),sK119)
| ~ l1_orders_2(sK119) )
| ~ spl384_187
| ~ spl384_190
| ~ spl384_191
| ~ spl384_192 ),
inference(forward_subsumption_resolution,[],[f62324,f62199]) ).
fof(f62326,plain,
( ! [X0] :
( ~ v22_waybel_0(k3_waybel_1(sK119,sK119,X0),k2_yellow_2(sK119,sK119,X0),sK119)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK119),u1_struct_0(sK119))
| ~ v7_waybel_1(X0,sK119)
| ~ m2_relset_1(X0,u1_struct_0(sK119),u1_struct_0(sK119))
| ~ v2_lattice3(sK119)
| v4_waybel_0(k2_yellow_2(sK119,sK119,X0),sK119)
| ~ l1_orders_2(sK119) )
| ~ spl384_187
| ~ spl384_189
| ~ spl384_190
| ~ spl384_191
| ~ spl384_192 ),
inference(forward_subsumption_resolution,[],[f62325,f62194]) ).
fof(f62327,plain,
( ! [X0] :
( ~ v22_waybel_0(k3_waybel_1(sK119,sK119,X0),k2_yellow_2(sK119,sK119,X0),sK119)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK119),u1_struct_0(sK119))
| ~ v7_waybel_1(X0,sK119)
| ~ m2_relset_1(X0,u1_struct_0(sK119),u1_struct_0(sK119))
| v4_waybel_0(k2_yellow_2(sK119,sK119,X0),sK119)
| ~ l1_orders_2(sK119) )
| ~ spl384_187
| ~ spl384_188
| ~ spl384_189
| ~ spl384_190
| ~ spl384_191
| ~ spl384_192 ),
inference(forward_subsumption_resolution,[],[f62326,f62189]) ).
fof(f62328,plain,
( ! [X0] :
( ~ v22_waybel_0(k3_waybel_1(sK119,sK119,X0),k2_yellow_2(sK119,sK119,X0),sK119)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK119),u1_struct_0(sK119))
| ~ v7_waybel_1(X0,sK119)
| ~ m2_relset_1(X0,u1_struct_0(sK119),u1_struct_0(sK119))
| v4_waybel_0(k2_yellow_2(sK119,sK119,X0),sK119) )
| ~ spl384_185
| ~ spl384_187
| ~ spl384_188
| ~ spl384_189
| ~ spl384_190
| ~ spl384_191
| ~ spl384_192 ),
inference(forward_subsumption_resolution,[],[f62327,f62174]) ).
fof(f62329,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF383,sF383)
| ~ v22_waybel_0(k3_waybel_1(sK119,sK119,X0),k2_yellow_2(sK119,sK119,X0),sK119)
| ~ v1_funct_1(X0)
| ~ v7_waybel_1(X0,sK119)
| ~ m2_relset_1(X0,u1_struct_0(sK119),u1_struct_0(sK119))
| v4_waybel_0(k2_yellow_2(sK119,sK119,X0),sK119) )
| ~ spl384_185
| ~ spl384_187
| ~ spl384_188
| ~ spl384_189
| ~ spl384_190
| ~ spl384_191
| ~ spl384_192
| ~ spl384_201 ),
inference(forward_demodulation,[],[f62328,f62263]) ).
fof(f62330,plain,
( ! [X0] :
( ~ v22_waybel_0(k3_waybel_1(sK119,sK119,X0),k2_yellow_2(sK119,sK119,X0),sK119)
| ~ v1_funct_2(X0,sF383,sF383)
| ~ m2_relset_1(X0,sF383,sF383)
| ~ v1_funct_1(X0)
| ~ v7_waybel_1(X0,sK119)
| v4_waybel_0(k2_yellow_2(sK119,sK119,X0),sK119) )
| ~ spl384_185
| ~ spl384_187
| ~ spl384_188
| ~ spl384_189
| ~ spl384_190
| ~ spl384_191
| ~ spl384_192
| ~ spl384_201 ),
inference(forward_demodulation,[],[f62329,f62263]) ).
fof(f62331,plain,
( ~ v22_waybel_0(k3_waybel_1(sK119,sK119,sK120),sF381,sK119)
| ~ v1_funct_2(sK120,sF383,sF383)
| ~ m2_relset_1(sK120,sF383,sF383)
| ~ v1_funct_1(sK120)
| ~ v7_waybel_1(sK120,sK119)
| v4_waybel_0(sF381,sK119)
| ~ spl384_185
| ~ spl384_187
| ~ spl384_188
| ~ spl384_189
| ~ spl384_190
| ~ spl384_191
| ~ spl384_192
| ~ spl384_199
| ~ spl384_201 ),
inference(superposition,[],[f62330,f62253]) ).
fof(f62332,plain,
( ~ v22_waybel_0(k3_waybel_1(sK119,sK119,sK120),sF381,sK119)
| ~ m2_relset_1(sK120,sF383,sF383)
| ~ v1_funct_1(sK120)
| ~ v7_waybel_1(sK120,sK119)
| v4_waybel_0(sF381,sK119)
| ~ spl384_185
| ~ spl384_187
| ~ spl384_188
| ~ spl384_189
| ~ spl384_190
| ~ spl384_191
| ~ spl384_192
| ~ spl384_195
| ~ spl384_199
| ~ spl384_201 ),
inference(forward_subsumption_resolution,[],[f62331,f62224]) ).
fof(f62333,plain,
( ~ v22_waybel_0(k3_waybel_1(sK119,sK119,sK120),sF381,sK119)
| ~ v1_funct_1(sK120)
| ~ v7_waybel_1(sK120,sK119)
| v4_waybel_0(sF381,sK119)
| ~ spl384_185
| ~ spl384_187
| ~ spl384_188
| ~ spl384_189
| ~ spl384_190
| ~ spl384_191
| ~ spl384_192
| ~ spl384_193
| ~ spl384_195
| ~ spl384_199
| ~ spl384_201 ),
inference(forward_subsumption_resolution,[],[f62332,f62214]) ).
fof(f62334,plain,
( ~ v22_waybel_0(k3_waybel_1(sK119,sK119,sK120),sF381,sK119)
| ~ v7_waybel_1(sK120,sK119)
| v4_waybel_0(sF381,sK119)
| ~ spl384_185
| ~ spl384_187
| ~ spl384_188
| ~ spl384_189
| ~ spl384_190
| ~ spl384_191
| ~ spl384_192
| ~ spl384_193
| ~ spl384_195
| ~ spl384_196
| ~ spl384_199
| ~ spl384_201 ),
inference(forward_subsumption_resolution,[],[f62333,f62229]) ).
fof(f62335,plain,
( ~ v22_waybel_0(k3_waybel_1(sK119,sK119,sK120),sF381,sK119)
| v4_waybel_0(sF381,sK119)
| ~ spl384_185
| ~ spl384_187
| ~ spl384_188
| ~ spl384_189
| ~ spl384_190
| ~ spl384_191
| ~ spl384_192
| ~ spl384_193
| ~ spl384_194
| ~ spl384_195
| ~ spl384_196
| ~ spl384_199
| ~ spl384_201 ),
inference(forward_subsumption_resolution,[],[f62334,f62219]) ).
fof(f62336,plain,
( ~ v22_waybel_0(k3_waybel_1(sK119,sK119,sK120),sF381,sK119)
| ~ spl384_185
| ~ spl384_187
| ~ spl384_188
| ~ spl384_189
| ~ spl384_190
| ~ spl384_191
| ~ spl384_192
| ~ spl384_193
| ~ spl384_194
| ~ spl384_195
| ~ spl384_196
| spl384_198
| ~ spl384_199
| ~ spl384_201 ),
inference(forward_subsumption_resolution,[],[f62335,f62239]) ).
fof(f62338,definition,
( spl384_204
<=> v22_waybel_0(k3_waybel_1(sK119,sK119,sK120),sF381,sK119) ),
introduced(definition,[new_symbols(definition,[spl384_204])],[avatar_definition]) ).
fof(f62340,plain,
( ~ v22_waybel_0(k3_waybel_1(sK119,sK119,sK120),sF381,sK119)
| spl384_204 ),
inference(avatar_component_clause,[],[f62338]) ).
fof(f62341,plain,
( ~ spl384_204
| ~ spl384_185
| ~ spl384_187
| ~ spl384_188
| ~ spl384_189
| ~ spl384_190
| ~ spl384_191
| ~ spl384_192
| ~ spl384_193
| ~ spl384_194
| ~ spl384_195
| ~ spl384_196
| spl384_198
| ~ spl384_199
| ~ spl384_201 ),
inference(avatar_split_clause,[],[f62336,f62261,f62251,f62237,f62227,f62222,f62217,f62212,f62207,f62202,f62197,f62192,f62187,f62182,f62172,f62338]) ).
fof(f62342,plain,
( m1_relset_1(sK120,sF383,sF383)
| ~ spl384_193 ),
inference(unit_resulting_resolution,[],[f58505,f62214]) ).
fof(f62344,definition,
( spl384_205
<=> m1_relset_1(sK120,sF383,sF383) ),
introduced(definition,[new_symbols(definition,[spl384_205])],[avatar_definition]) ).
fof(f62346,plain,
( m1_relset_1(sK120,sF383,sF383)
| ~ spl384_205 ),
inference(avatar_component_clause,[],[f62344]) ).
fof(f62347,plain,
( spl384_205
| ~ spl384_193 ),
inference(avatar_split_clause,[],[f62342,f62212,f62344]) ).
fof(f62353,plain,
( ~ v3_struct_0(sK119)
| ~ spl384_185
| ~ spl384_189 ),
inference(unit_resulting_resolution,[],[f58515,f62174,f62194]) ).
fof(f62357,definition,
( spl384_206
<=> v3_struct_0(sK119) ),
introduced(definition,[new_symbols(definition,[spl384_206])],[avatar_definition]) ).
fof(f62359,plain,
( ~ v3_struct_0(sK119)
| spl384_206 ),
inference(avatar_component_clause,[],[f62357]) ).
fof(f62360,plain,
( ~ spl384_206
| ~ spl384_185
| ~ spl384_189 ),
inference(avatar_split_clause,[],[f62353,f62192,f62172,f62357]) ).
fof(f62363,plain,
( ! [X0,X1] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(sK119))
| ~ m2_relset_1(X0,u1_struct_0(X1),u1_struct_0(sK119))
| k2_waybel_1(X1,sK119,X0) = X0
| ~ l1_orders_2(sK119)
| v3_struct_0(X1)
| ~ l1_orders_2(X1) )
| spl384_206 ),
inference(resolution,[],[f62359,f60781]) ).
fof(f62369,plain,
( ! [X0,X1] :
( m2_relset_1(k3_waybel_1(sK119,X0,X1),u1_struct_0(k2_yellow_2(sK119,X0,X1)),u1_struct_0(X0))
| ~ l1_orders_2(sK119)
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK119),u1_struct_0(X0))
| ~ m1_relset_1(X1,u1_struct_0(sK119),u1_struct_0(X0)) )
| spl384_206 ),
inference(resolution,[],[f62359,f60791]) ).
fof(f62370,plain,
( ! [X0,X1] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(sK119))
| ~ m2_relset_1(X0,u1_struct_0(X1),u1_struct_0(sK119))
| k3_waybel_1(X1,sK119,X0) = k7_grcat_1(k2_yellow_2(X1,sK119,X0))
| ~ l1_orders_2(sK119)
| v3_struct_0(X1)
| ~ l1_orders_2(X1) )
| spl384_206 ),
inference(resolution,[],[f62359,f60799]) ).
fof(f62371,plain,
( ! [X0,X1] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(sK119))
| ~ m2_relset_1(X0,u1_struct_0(X1),u1_struct_0(sK119))
| k3_waybel_1(X1,sK119,X0) = k7_grcat_1(k2_yellow_2(X1,sK119,X0))
| v3_struct_0(X1)
| ~ l1_orders_2(X1) )
| ~ spl384_185
| spl384_206 ),
inference(forward_subsumption_resolution,[],[f62370,f62174]) ).
fof(f62372,plain,
( ! [X0,X1] :
( m2_relset_1(k3_waybel_1(sK119,X0,X1),u1_struct_0(k2_yellow_2(sK119,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(sK119),u1_struct_0(X0))
| ~ m1_relset_1(X1,u1_struct_0(sK119),u1_struct_0(X0)) )
| ~ spl384_185
| spl384_206 ),
inference(forward_subsumption_resolution,[],[f62369,f62174]) ).
fof(f62378,plain,
( ! [X0,X1] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(sK119))
| ~ m2_relset_1(X0,u1_struct_0(X1),u1_struct_0(sK119))
| k2_waybel_1(X1,sK119,X0) = X0
| v3_struct_0(X1)
| ~ l1_orders_2(X1) )
| ~ spl384_185
| spl384_206 ),
inference(forward_subsumption_resolution,[],[f62363,f62174]) ).
fof(f62381,plain,
( ! [X0,X1] :
( ~ v1_funct_2(X0,u1_struct_0(X1),sF383)
| ~ v1_funct_1(X0)
| ~ m2_relset_1(X0,u1_struct_0(X1),u1_struct_0(sK119))
| k3_waybel_1(X1,sK119,X0) = k7_grcat_1(k2_yellow_2(X1,sK119,X0))
| v3_struct_0(X1)
| ~ l1_orders_2(X1) )
| ~ spl384_185
| ~ spl384_201
| spl384_206 ),
inference(forward_demodulation,[],[f62371,f62263]) ).
fof(f62382,plain,
( ! [X0,X1] :
( ~ v1_funct_2(X1,sF383,u1_struct_0(X0))
| m2_relset_1(k3_waybel_1(sK119,X0,X1),u1_struct_0(k2_yellow_2(sK119,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(sK119),u1_struct_0(X0)) )
| ~ spl384_185
| ~ spl384_201
| spl384_206 ),
inference(forward_demodulation,[],[f62372,f62263]) ).
fof(f62388,plain,
( ! [X0,X1] :
( ~ v1_funct_2(X0,u1_struct_0(X1),sF383)
| ~ v1_funct_1(X0)
| ~ m2_relset_1(X0,u1_struct_0(X1),u1_struct_0(sK119))
| k2_waybel_1(X1,sK119,X0) = X0
| v3_struct_0(X1)
| ~ l1_orders_2(X1) )
| ~ spl384_185
| ~ spl384_201
| spl384_206 ),
inference(forward_demodulation,[],[f62378,f62263]) ).
fof(f62391,plain,
( ! [X0,X1] :
( ~ l1_orders_2(X1)
| ~ v1_funct_2(X0,u1_struct_0(X1),sF383)
| ~ v1_funct_1(X0)
| k3_waybel_1(X1,sK119,X0) = k7_grcat_1(k2_yellow_2(X1,sK119,X0))
| v3_struct_0(X1)
| ~ m2_relset_1(X0,u1_struct_0(X1),sF383) )
| ~ spl384_185
| ~ spl384_201
| spl384_206 ),
inference(forward_demodulation,[],[f62381,f62263]) ).
fof(f62392,plain,
( ! [X0,X1] :
( ~ l1_orders_2(X0)
| ~ v1_funct_2(X1,sF383,u1_struct_0(X0))
| m2_relset_1(k3_waybel_1(sK119,X0,X1),u1_struct_0(k2_yellow_2(sK119,X0,X1)),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ m1_relset_1(X1,sF383,u1_struct_0(X0))
| ~ v1_funct_1(X1) )
| ~ spl384_185
| ~ spl384_201
| spl384_206 ),
inference(forward_demodulation,[],[f62382,f62263]) ).
fof(f62398,plain,
( ! [X0,X1] :
( ~ l1_orders_2(X1)
| ~ v1_funct_2(X0,u1_struct_0(X1),sF383)
| ~ v1_funct_1(X0)
| k2_waybel_1(X1,sK119,X0) = X0
| v3_struct_0(X1)
| ~ m2_relset_1(X0,u1_struct_0(X1),sF383) )
| ~ spl384_185
| ~ spl384_201
| spl384_206 ),
inference(forward_demodulation,[],[f62388,f62263]) ).
fof(f62404,plain,
( ! [X0] :
( ~ v1_funct_2(X0,u1_struct_0(sK119),sF383)
| ~ v1_funct_1(X0)
| k2_waybel_1(sK119,sK119,X0) = X0
| v3_struct_0(sK119)
| ~ m2_relset_1(X0,u1_struct_0(sK119),sF383) )
| ~ spl384_185
| ~ spl384_201
| spl384_206 ),
inference(resolution,[],[f62398,f62174]) ).
fof(f62405,plain,
( ! [X0] :
( ~ v1_funct_2(X0,u1_struct_0(sK119),sF383)
| ~ v1_funct_1(X0)
| k2_waybel_1(sK119,sK119,X0) = X0
| ~ m2_relset_1(X0,u1_struct_0(sK119),sF383) )
| ~ spl384_185
| ~ spl384_201
| spl384_206 ),
inference(forward_subsumption_resolution,[],[f62404,f62359]) ).
fof(f62406,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF383,sF383)
| ~ v1_funct_1(X0)
| k2_waybel_1(sK119,sK119,X0) = X0
| ~ m2_relset_1(X0,u1_struct_0(sK119),sF383) )
| ~ spl384_185
| ~ spl384_201
| spl384_206 ),
inference(forward_demodulation,[],[f62405,f62263]) ).
fof(f62407,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF383,sF383)
| ~ m2_relset_1(X0,sF383,sF383)
| ~ v1_funct_1(X0)
| k2_waybel_1(sK119,sK119,X0) = X0 )
| ~ spl384_185
| ~ spl384_201
| spl384_206 ),
inference(forward_demodulation,[],[f62406,f62263]) ).
fof(f62408,plain,
( sK120 = k2_waybel_1(sK119,sK119,sK120)
| ~ spl384_185
| ~ spl384_193
| ~ spl384_195
| ~ spl384_196
| ~ spl384_201
| spl384_206 ),
inference(unit_resulting_resolution,[],[f62407,f62229,f62224,f62214]) ).
fof(f62412,definition,
( spl384_207
<=> sK120 = k2_waybel_1(sK119,sK119,sK120) ),
introduced(definition,[new_symbols(definition,[spl384_207])],[avatar_definition]) ).
fof(f62414,plain,
( sK120 = k2_waybel_1(sK119,sK119,sK120)
| ~ spl384_207 ),
inference(avatar_component_clause,[],[f62412]) ).
fof(f62415,plain,
( spl384_207
| ~ spl384_185
| ~ spl384_193
| ~ spl384_195
| ~ spl384_196
| ~ spl384_201
| spl384_206 ),
inference(avatar_split_clause,[],[f62408,f62357,f62261,f62227,f62222,f62212,f62172,f62412]) ).
fof(f62429,plain,
( ! [X0,X1] :
( v3_struct_0(sK119)
| v1_funct_2(k3_waybel_1(sK119,X0,X1),u1_struct_0(k2_yellow_2(sK119,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(sK119),u1_struct_0(X0))
| ~ m1_relset_1(X1,u1_struct_0(sK119),u1_struct_0(X0)) )
| ~ spl384_185 ),
inference(resolution,[],[f60802,f62174]) ).
fof(f62430,plain,
( ! [X0,X1] :
( v1_funct_2(k3_waybel_1(sK119,X0,X1),u1_struct_0(k2_yellow_2(sK119,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(sK119),u1_struct_0(X0))
| ~ m1_relset_1(X1,u1_struct_0(sK119),u1_struct_0(X0)) )
| ~ spl384_185
| spl384_206 ),
inference(forward_subsumption_resolution,[],[f62429,f62359]) ).
fof(f62431,plain,
( ! [X0,X1] :
( ~ v1_funct_2(X1,sF383,u1_struct_0(X0))
| v1_funct_2(k3_waybel_1(sK119,X0,X1),u1_struct_0(k2_yellow_2(sK119,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(sK119),u1_struct_0(X0)) )
| ~ spl384_185
| ~ spl384_201
| spl384_206 ),
inference(forward_demodulation,[],[f62430,f62263]) ).
fof(f62432,plain,
( ! [X0,X1] :
( ~ l1_orders_2(X0)
| ~ v1_funct_2(X1,sF383,u1_struct_0(X0))
| v1_funct_2(k3_waybel_1(sK119,X0,X1),u1_struct_0(k2_yellow_2(sK119,X0,X1)),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ m1_relset_1(X1,sF383,u1_struct_0(X0))
| ~ v1_funct_1(X1) )
| ~ spl384_185
| ~ spl384_201
| spl384_206 ),
inference(forward_demodulation,[],[f62431,f62263]) ).
fof(f62433,plain,
( ! [X0,X1] :
( v3_struct_0(sK119)
| ~ v3_struct_0(k2_yellow_2(sK119,X0,X1))
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK119),u1_struct_0(X0))
| ~ m1_relset_1(X1,u1_struct_0(sK119),u1_struct_0(X0)) )
| ~ spl384_185 ),
inference(resolution,[],[f60359,f62174]) ).
fof(f62434,plain,
( ! [X0,X1] :
( ~ v3_struct_0(k2_yellow_2(sK119,X0,X1))
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK119),u1_struct_0(X0))
| ~ m1_relset_1(X1,u1_struct_0(sK119),u1_struct_0(X0)) )
| ~ spl384_185
| spl384_206 ),
inference(forward_subsumption_resolution,[],[f62433,f62359]) ).
fof(f62435,plain,
( ! [X0,X1] :
( ~ v1_funct_2(X1,sF383,u1_struct_0(X0))
| ~ v3_struct_0(k2_yellow_2(sK119,X0,X1))
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ m1_relset_1(X1,u1_struct_0(sK119),u1_struct_0(X0)) )
| ~ spl384_185
| ~ spl384_201
| spl384_206 ),
inference(forward_demodulation,[],[f62434,f62263]) ).
fof(f62436,plain,
( ! [X0,X1] :
( ~ l1_orders_2(X0)
| ~ v1_funct_2(X1,sF383,u1_struct_0(X0))
| ~ v3_struct_0(k2_yellow_2(sK119,X0,X1))
| v3_struct_0(X0)
| ~ m1_relset_1(X1,sF383,u1_struct_0(X0))
| ~ v1_funct_1(X1) )
| ~ spl384_185
| ~ spl384_201
| spl384_206 ),
inference(forward_demodulation,[],[f62435,f62263]) ).
fof(f62437,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF383,u1_struct_0(sK119))
| ~ v3_struct_0(k2_yellow_2(sK119,sK119,X0))
| v3_struct_0(sK119)
| ~ m1_relset_1(X0,sF383,u1_struct_0(sK119))
| ~ v1_funct_1(X0) )
| ~ spl384_185
| ~ spl384_201
| spl384_206 ),
inference(resolution,[],[f62436,f62174]) ).
fof(f62438,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF383,u1_struct_0(sK119))
| ~ v3_struct_0(k2_yellow_2(sK119,sK119,X0))
| ~ m1_relset_1(X0,sF383,u1_struct_0(sK119))
| ~ v1_funct_1(X0) )
| ~ spl384_185
| ~ spl384_201
| spl384_206 ),
inference(forward_subsumption_resolution,[],[f62437,f62359]) ).
fof(f62439,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF383,sF383)
| ~ v3_struct_0(k2_yellow_2(sK119,sK119,X0))
| ~ m1_relset_1(X0,sF383,u1_struct_0(sK119))
| ~ v1_funct_1(X0) )
| ~ spl384_185
| ~ spl384_201
| spl384_206 ),
inference(forward_demodulation,[],[f62438,f62263]) ).
fof(f62440,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF383,sF383)
| ~ m1_relset_1(X0,sF383,sF383)
| ~ v3_struct_0(k2_yellow_2(sK119,sK119,X0))
| ~ v1_funct_1(X0) )
| ~ spl384_185
| ~ spl384_201
| spl384_206 ),
inference(forward_demodulation,[],[f62439,f62263]) ).
fof(f62441,plain,
( ~ v3_struct_0(k2_yellow_2(sK119,sK119,sK120))
| ~ spl384_185
| ~ spl384_195
| ~ spl384_196
| ~ spl384_201
| ~ spl384_205
| spl384_206 ),
inference(unit_resulting_resolution,[],[f62440,f62229,f62224,f62346]) ).
fof(f62444,plain,
( ~ v3_struct_0(sF381)
| ~ spl384_185
| ~ spl384_195
| ~ spl384_196
| ~ spl384_199
| ~ spl384_201
| ~ spl384_205
| spl384_206 ),
inference(forward_demodulation,[],[f62441,f62253]) ).
fof(f62447,definition,
( spl384_208
<=> v3_struct_0(sF381) ),
introduced(definition,[new_symbols(definition,[spl384_208])],[avatar_definition]) ).
fof(f62449,plain,
( ~ v3_struct_0(sF381)
| spl384_208 ),
inference(avatar_component_clause,[],[f62447]) ).
fof(f62450,plain,
( ~ spl384_208
| ~ spl384_185
| ~ spl384_195
| ~ spl384_196
| ~ spl384_199
| ~ spl384_201
| ~ spl384_205
| spl384_206 ),
inference(avatar_split_clause,[],[f62444,f62357,f62344,f62261,f62251,f62227,f62222,f62172,f62447]) ).
fof(f62463,definition,
( spl384_209
<=> l1_orders_2(sF381) ),
introduced(definition,[new_symbols(definition,[spl384_209])],[avatar_definition]) ).
fof(f62464,plain,
( l1_orders_2(sF381)
| ~ spl384_209 ),
inference(avatar_component_clause,[],[f62463]) ).
fof(f62465,plain,
( ~ l1_orders_2(sF381)
| spl384_209 ),
inference(avatar_component_clause,[],[f62463]) ).
fof(f62525,plain,
( ! [X0,X1] :
( v3_struct_0(sK119)
| m1_yellow_0(k2_yellow_2(sK119,X0,X1),X0)
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK119),u1_struct_0(X0))
| ~ m1_relset_1(X1,u1_struct_0(sK119),u1_struct_0(X0)) )
| ~ spl384_185 ),
inference(resolution,[],[f60354,f62174]) ).
fof(f62526,plain,
( ! [X0,X1] :
( m1_yellow_0(k2_yellow_2(sK119,X0,X1),X0)
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK119),u1_struct_0(X0))
| ~ m1_relset_1(X1,u1_struct_0(sK119),u1_struct_0(X0)) )
| ~ spl384_185
| spl384_206 ),
inference(forward_subsumption_resolution,[],[f62525,f62359]) ).
fof(f62527,plain,
( ! [X0,X1] :
( ~ v1_funct_2(X1,sF383,u1_struct_0(X0))
| m1_yellow_0(k2_yellow_2(sK119,X0,X1),X0)
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ m1_relset_1(X1,u1_struct_0(sK119),u1_struct_0(X0)) )
| ~ spl384_185
| ~ spl384_201
| spl384_206 ),
inference(forward_demodulation,[],[f62526,f62263]) ).
fof(f62528,plain,
( ! [X0,X1] :
( ~ l1_orders_2(X0)
| ~ v1_funct_2(X1,sF383,u1_struct_0(X0))
| m1_yellow_0(k2_yellow_2(sK119,X0,X1),X0)
| v3_struct_0(X0)
| ~ m1_relset_1(X1,sF383,u1_struct_0(X0))
| ~ v1_funct_1(X1) )
| ~ spl384_185
| ~ spl384_201
| spl384_206 ),
inference(forward_demodulation,[],[f62527,f62263]) ).
fof(f62529,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF383,u1_struct_0(sK119))
| m1_yellow_0(k2_yellow_2(sK119,sK119,X0),sK119)
| v3_struct_0(sK119)
| ~ m1_relset_1(X0,sF383,u1_struct_0(sK119))
| ~ v1_funct_1(X0) )
| ~ spl384_185
| ~ spl384_201
| spl384_206 ),
inference(resolution,[],[f62528,f62174]) ).
fof(f62530,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF383,u1_struct_0(sK119))
| m1_yellow_0(k2_yellow_2(sK119,sK119,X0),sK119)
| ~ m1_relset_1(X0,sF383,u1_struct_0(sK119))
| ~ v1_funct_1(X0) )
| ~ spl384_185
| ~ spl384_201
| spl384_206 ),
inference(forward_subsumption_resolution,[],[f62529,f62359]) ).
fof(f62531,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF383,sF383)
| m1_yellow_0(k2_yellow_2(sK119,sK119,X0),sK119)
| ~ m1_relset_1(X0,sF383,u1_struct_0(sK119))
| ~ v1_funct_1(X0) )
| ~ spl384_185
| ~ spl384_201
| spl384_206 ),
inference(forward_demodulation,[],[f62530,f62263]) ).
fof(f62532,plain,
( ! [X0] :
( m1_yellow_0(k2_yellow_2(sK119,sK119,X0),sK119)
| ~ v1_funct_2(X0,sF383,sF383)
| ~ m1_relset_1(X0,sF383,sF383)
| ~ v1_funct_1(X0) )
| ~ spl384_185
| ~ spl384_201
| spl384_206 ),
inference(forward_demodulation,[],[f62531,f62263]) ).
fof(f62533,plain,
( m1_yellow_0(k2_yellow_2(sK119,sK119,sK120),sK119)
| ~ spl384_185
| ~ spl384_195
| ~ spl384_196
| ~ spl384_201
| ~ spl384_205
| spl384_206 ),
inference(unit_resulting_resolution,[],[f62532,f62229,f62346,f62224]) ).
fof(f62536,plain,
( m1_yellow_0(sF381,sK119)
| ~ spl384_185
| ~ spl384_195
| ~ spl384_196
| ~ spl384_199
| ~ spl384_201
| ~ spl384_205
| spl384_206 ),
inference(forward_demodulation,[],[f62533,f62253]) ).
fof(f62539,definition,
( spl384_221
<=> m1_yellow_0(sF381,sK119) ),
introduced(definition,[new_symbols(definition,[spl384_221])],[avatar_definition]) ).
fof(f62541,plain,
( m1_yellow_0(sF381,sK119)
| ~ spl384_221 ),
inference(avatar_component_clause,[],[f62539]) ).
fof(f62542,plain,
( spl384_221
| ~ spl384_185
| ~ spl384_195
| ~ spl384_196
| ~ spl384_199
| ~ spl384_201
| ~ spl384_205
| spl384_206 ),
inference(avatar_split_clause,[],[f62536,f62357,f62344,f62261,f62251,f62227,f62222,f62172,f62539]) ).
fof(f62549,plain,
( sK120 = sF382
| ~ spl384_200
| ~ spl384_207 ),
inference(superposition,[],[f62258,f62414]) ).
fof(f62551,definition,
( spl384_222
<=> sK120 = sF382 ),
introduced(definition,[new_symbols(definition,[spl384_222])],[avatar_definition]) ).
fof(f62553,plain,
( sK120 = sF382
| ~ spl384_222 ),
inference(avatar_component_clause,[],[f62551]) ).
fof(f62554,plain,
( spl384_222
| ~ spl384_200
| ~ spl384_207 ),
inference(avatar_split_clause,[],[f62549,f62412,f62256,f62551]) ).
fof(f62555,plain,
( v1_waybel34(sK120,sK119,sF381)
| ~ spl384_197
| ~ spl384_222 ),
inference(superposition,[],[f62234,f62553]) ).
fof(f62557,definition,
( spl384_223
<=> v1_waybel34(sK120,sK119,sF381) ),
introduced(definition,[new_symbols(definition,[spl384_223])],[avatar_definition]) ).
fof(f62559,plain,
( v1_waybel34(sK120,sK119,sF381)
| ~ spl384_223 ),
inference(avatar_component_clause,[],[f62557]) ).
fof(f62560,plain,
( spl384_223
| ~ spl384_197
| ~ spl384_222 ),
inference(avatar_split_clause,[],[f62555,f62551,f62232,f62557]) ).
fof(f62660,plain,
( ! [X0] :
( ~ v1_funct_2(X0,u1_struct_0(sK119),sF383)
| ~ v1_funct_1(X0)
| k3_waybel_1(sK119,sK119,X0) = k7_grcat_1(k2_yellow_2(sK119,sK119,X0))
| v3_struct_0(sK119)
| ~ m2_relset_1(X0,u1_struct_0(sK119),sF383) )
| ~ spl384_185
| ~ spl384_201
| spl384_206 ),
inference(resolution,[],[f62391,f62174]) ).
fof(f62661,plain,
( ! [X0] :
( ~ v1_funct_2(X0,u1_struct_0(sK119),sF383)
| ~ v1_funct_1(X0)
| k3_waybel_1(sK119,sK119,X0) = k7_grcat_1(k2_yellow_2(sK119,sK119,X0))
| ~ m2_relset_1(X0,u1_struct_0(sK119),sF383) )
| ~ spl384_185
| ~ spl384_201
| spl384_206 ),
inference(forward_subsumption_resolution,[],[f62660,f62359]) ).
fof(f62662,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF383,sF383)
| ~ v1_funct_1(X0)
| k3_waybel_1(sK119,sK119,X0) = k7_grcat_1(k2_yellow_2(sK119,sK119,X0))
| ~ m2_relset_1(X0,u1_struct_0(sK119),sF383) )
| ~ spl384_185
| ~ spl384_201
| spl384_206 ),
inference(forward_demodulation,[],[f62661,f62263]) ).
fof(f62663,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF383,sF383)
| ~ m2_relset_1(X0,sF383,sF383)
| ~ v1_funct_1(X0)
| k3_waybel_1(sK119,sK119,X0) = k7_grcat_1(k2_yellow_2(sK119,sK119,X0)) )
| ~ spl384_185
| ~ spl384_201
| spl384_206 ),
inference(forward_demodulation,[],[f62662,f62263]) ).
fof(f62664,plain,
( k3_waybel_1(sK119,sK119,sK120) = k7_grcat_1(k2_yellow_2(sK119,sK119,sK120))
| ~ spl384_185
| ~ spl384_193
| ~ spl384_195
| ~ spl384_196
| ~ spl384_201
| spl384_206 ),
inference(unit_resulting_resolution,[],[f62663,f62229,f62224,f62214]) ).
fof(f62667,plain,
( k3_waybel_1(sK119,sK119,sK120) = k7_grcat_1(sF381)
| ~ spl384_185
| ~ spl384_193
| ~ spl384_195
| ~ spl384_196
| ~ spl384_199
| ~ spl384_201
| spl384_206 ),
inference(forward_demodulation,[],[f62664,f62253]) ).
fof(f62670,definition,
( spl384_228
<=> k3_waybel_1(sK119,sK119,sK120) = k7_grcat_1(sF381) ),
introduced(definition,[new_symbols(definition,[spl384_228])],[avatar_definition]) ).
fof(f62672,plain,
( k3_waybel_1(sK119,sK119,sK120) = k7_grcat_1(sF381)
| ~ spl384_228 ),
inference(avatar_component_clause,[],[f62670]) ).
fof(f62673,plain,
( spl384_228
| ~ spl384_185
| ~ spl384_193
| ~ spl384_195
| ~ spl384_196
| ~ spl384_199
| ~ spl384_201
| spl384_206 ),
inference(avatar_split_clause,[],[f62667,f62357,f62261,f62251,f62227,f62222,f62212,f62172,f62670]) ).
fof(f62675,plain,
( ~ v22_waybel_0(k7_grcat_1(sF381),sF381,sK119)
| spl384_204
| ~ spl384_228 ),
inference(superposition,[],[f62340,f62672]) ).
fof(f62679,definition,
( spl384_229
<=> v22_waybel_0(k7_grcat_1(sF381),sF381,sK119) ),
introduced(definition,[new_symbols(definition,[spl384_229])],[avatar_definition]) ).
fof(f62681,plain,
( ~ v22_waybel_0(k7_grcat_1(sF381),sF381,sK119)
| spl384_229 ),
inference(avatar_component_clause,[],[f62679]) ).
fof(f62682,plain,
( ~ spl384_229
| spl384_204
| ~ spl384_228 ),
inference(avatar_split_clause,[],[f62675,f62670,f62338,f62679]) ).
fof(f62707,plain,
( ! [X0] :
( ~ v2_orders_2(sK119)
| ~ v3_orders_2(sK119)
| ~ v4_orders_2(sK119)
| ~ v1_lattice3(sK119)
| ~ v2_lattice3(sK119)
| sP19(X0,sK119)
| ~ l1_orders_2(sK119)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK119),u1_struct_0(sK119))
| ~ v6_waybel_1(X0,sK119)
| ~ m1_relset_1(X0,u1_struct_0(sK119),u1_struct_0(sK119)) )
| ~ spl384_187 ),
inference(resolution,[],[f58419,f62184]) ).
fof(f62708,plain,
( ! [X0] :
( ~ v3_orders_2(sK119)
| ~ v4_orders_2(sK119)
| ~ v1_lattice3(sK119)
| ~ v2_lattice3(sK119)
| sP19(X0,sK119)
| ~ l1_orders_2(sK119)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK119),u1_struct_0(sK119))
| ~ v6_waybel_1(X0,sK119)
| ~ m1_relset_1(X0,u1_struct_0(sK119),u1_struct_0(sK119)) )
| ~ spl384_187
| ~ spl384_192 ),
inference(forward_subsumption_resolution,[],[f62707,f62209]) ).
fof(f62709,plain,
( ! [X0] :
( ~ v4_orders_2(sK119)
| ~ v1_lattice3(sK119)
| ~ v2_lattice3(sK119)
| sP19(X0,sK119)
| ~ l1_orders_2(sK119)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK119),u1_struct_0(sK119))
| ~ v6_waybel_1(X0,sK119)
| ~ m1_relset_1(X0,u1_struct_0(sK119),u1_struct_0(sK119)) )
| ~ spl384_187
| ~ spl384_191
| ~ spl384_192 ),
inference(forward_subsumption_resolution,[],[f62708,f62204]) ).
fof(f62710,plain,
( ! [X0] :
( ~ v1_lattice3(sK119)
| ~ v2_lattice3(sK119)
| sP19(X0,sK119)
| ~ l1_orders_2(sK119)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK119),u1_struct_0(sK119))
| ~ v6_waybel_1(X0,sK119)
| ~ m1_relset_1(X0,u1_struct_0(sK119),u1_struct_0(sK119)) )
| ~ spl384_187
| ~ spl384_190
| ~ spl384_191
| ~ spl384_192 ),
inference(forward_subsumption_resolution,[],[f62709,f62199]) ).
fof(f62711,plain,
( ! [X0] :
( ~ v2_lattice3(sK119)
| sP19(X0,sK119)
| ~ l1_orders_2(sK119)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK119),u1_struct_0(sK119))
| ~ v6_waybel_1(X0,sK119)
| ~ m1_relset_1(X0,u1_struct_0(sK119),u1_struct_0(sK119)) )
| ~ spl384_187
| ~ spl384_189
| ~ spl384_190
| ~ spl384_191
| ~ spl384_192 ),
inference(forward_subsumption_resolution,[],[f62710,f62194]) ).
fof(f62712,plain,
( ! [X0] :
( sP19(X0,sK119)
| ~ l1_orders_2(sK119)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK119),u1_struct_0(sK119))
| ~ v6_waybel_1(X0,sK119)
| ~ m1_relset_1(X0,u1_struct_0(sK119),u1_struct_0(sK119)) )
| ~ spl384_187
| ~ spl384_188
| ~ spl384_189
| ~ spl384_190
| ~ spl384_191
| ~ spl384_192 ),
inference(forward_subsumption_resolution,[],[f62711,f62189]) ).
fof(f62713,plain,
( ! [X0] :
( sP19(X0,sK119)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK119),u1_struct_0(sK119))
| ~ v6_waybel_1(X0,sK119)
| ~ m1_relset_1(X0,u1_struct_0(sK119),u1_struct_0(sK119)) )
| ~ spl384_185
| ~ spl384_187
| ~ spl384_188
| ~ spl384_189
| ~ spl384_190
| ~ spl384_191
| ~ spl384_192 ),
inference(forward_subsumption_resolution,[],[f62712,f62174]) ).
fof(f62714,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF383,sF383)
| sP19(X0,sK119)
| ~ v1_funct_1(X0)
| ~ v6_waybel_1(X0,sK119)
| ~ m1_relset_1(X0,u1_struct_0(sK119),u1_struct_0(sK119)) )
| ~ spl384_185
| ~ spl384_187
| ~ spl384_188
| ~ spl384_189
| ~ spl384_190
| ~ spl384_191
| ~ spl384_192
| ~ spl384_201 ),
inference(forward_demodulation,[],[f62713,f62263]) ).
fof(f62715,plain,
( ! [X0] :
( ~ v6_waybel_1(X0,sK119)
| ~ v1_funct_2(X0,sF383,sF383)
| sP19(X0,sK119)
| ~ v1_funct_1(X0)
| ~ m1_relset_1(X0,sF383,sF383) )
| ~ spl384_185
| ~ spl384_187
| ~ spl384_188
| ~ spl384_189
| ~ spl384_190
| ~ spl384_191
| ~ spl384_192
| ~ spl384_201 ),
inference(forward_demodulation,[],[f62714,f62263]) ).
fof(f62716,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF383,sF383)
| sP19(X0,sK119)
| ~ v1_funct_1(X0)
| ~ m1_relset_1(X0,sF383,sF383)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK119),u1_struct_0(sK119))
| ~ v7_waybel_1(X0,sK119)
| ~ m1_relset_1(X0,u1_struct_0(sK119),u1_struct_0(sK119))
| v3_struct_0(sK119)
| ~ l1_orders_2(sK119) )
| ~ spl384_185
| ~ spl384_187
| ~ spl384_188
| ~ spl384_189
| ~ spl384_190
| ~ spl384_191
| ~ spl384_192
| ~ spl384_201 ),
inference(resolution,[],[f62715,f60691]) ).
fof(f62717,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF383,sF383)
| sP19(X0,sK119)
| ~ v1_funct_1(X0)
| ~ m1_relset_1(X0,sF383,sF383)
| ~ v1_funct_2(X0,u1_struct_0(sK119),u1_struct_0(sK119))
| ~ v7_waybel_1(X0,sK119)
| ~ m1_relset_1(X0,u1_struct_0(sK119),u1_struct_0(sK119))
| v3_struct_0(sK119)
| ~ l1_orders_2(sK119) )
| ~ spl384_185
| ~ spl384_187
| ~ spl384_188
| ~ spl384_189
| ~ spl384_190
| ~ spl384_191
| ~ spl384_192
| ~ spl384_201 ),
inference(duplicate_literal_removal,[],[f62716]) ).
fof(f62718,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF383,sF383)
| sP19(X0,sK119)
| ~ v1_funct_1(X0)
| ~ m1_relset_1(X0,sF383,sF383)
| ~ v1_funct_2(X0,u1_struct_0(sK119),u1_struct_0(sK119))
| ~ v7_waybel_1(X0,sK119)
| ~ m1_relset_1(X0,u1_struct_0(sK119),u1_struct_0(sK119))
| ~ l1_orders_2(sK119) )
| ~ spl384_185
| ~ spl384_187
| ~ spl384_188
| ~ spl384_189
| ~ spl384_190
| ~ spl384_191
| ~ spl384_192
| ~ spl384_201
| spl384_206 ),
inference(forward_subsumption_resolution,[],[f62717,f62359]) ).
fof(f62719,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF383,sF383)
| sP19(X0,sK119)
| ~ v1_funct_1(X0)
| ~ m1_relset_1(X0,sF383,sF383)
| ~ v1_funct_2(X0,u1_struct_0(sK119),u1_struct_0(sK119))
| ~ v7_waybel_1(X0,sK119)
| ~ m1_relset_1(X0,u1_struct_0(sK119),u1_struct_0(sK119)) )
| ~ spl384_185
| ~ spl384_187
| ~ spl384_188
| ~ spl384_189
| ~ spl384_190
| ~ spl384_191
| ~ spl384_192
| ~ spl384_201
| spl384_206 ),
inference(forward_subsumption_resolution,[],[f62718,f62174]) ).
fof(f62720,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF383,sF383)
| ~ v1_funct_2(X0,sF383,sF383)
| sP19(X0,sK119)
| ~ v1_funct_1(X0)
| ~ m1_relset_1(X0,sF383,sF383)
| ~ v7_waybel_1(X0,sK119)
| ~ m1_relset_1(X0,u1_struct_0(sK119),u1_struct_0(sK119)) )
| ~ spl384_185
| ~ spl384_187
| ~ spl384_188
| ~ spl384_189
| ~ spl384_190
| ~ spl384_191
| ~ spl384_192
| ~ spl384_201
| spl384_206 ),
inference(forward_demodulation,[],[f62719,f62263]) ).
fof(f62721,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF383,sF383)
| sP19(X0,sK119)
| ~ v1_funct_1(X0)
| ~ m1_relset_1(X0,sF383,sF383)
| ~ v7_waybel_1(X0,sK119)
| ~ m1_relset_1(X0,u1_struct_0(sK119),u1_struct_0(sK119)) )
| ~ spl384_185
| ~ spl384_187
| ~ spl384_188
| ~ spl384_189
| ~ spl384_190
| ~ spl384_191
| ~ spl384_192
| ~ spl384_201
| spl384_206 ),
inference(duplicate_literal_removal,[],[f62720]) ).
fof(f62722,plain,
( ! [X0] :
( ~ m1_relset_1(X0,sF383,sF383)
| ~ v1_funct_2(X0,sF383,sF383)
| sP19(X0,sK119)
| ~ v1_funct_1(X0)
| ~ m1_relset_1(X0,sF383,sF383)
| ~ v7_waybel_1(X0,sK119) )
| ~ spl384_185
| ~ spl384_187
| ~ spl384_188
| ~ spl384_189
| ~ spl384_190
| ~ spl384_191
| ~ spl384_192
| ~ spl384_201
| spl384_206 ),
inference(forward_demodulation,[],[f62721,f62263]) ).
fof(f62723,plain,
( ! [X0] :
( ~ v7_waybel_1(X0,sK119)
| ~ v1_funct_2(X0,sF383,sF383)
| sP19(X0,sK119)
| ~ v1_funct_1(X0)
| ~ m1_relset_1(X0,sF383,sF383) )
| ~ spl384_185
| ~ spl384_187
| ~ spl384_188
| ~ spl384_189
| ~ spl384_190
| ~ spl384_191
| ~ spl384_192
| ~ spl384_201
| spl384_206 ),
inference(duplicate_literal_removal,[],[f62722]) ).
fof(f62761,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF383,u1_struct_0(sK119))
| v1_funct_2(k3_waybel_1(sK119,sK119,X0),u1_struct_0(k2_yellow_2(sK119,sK119,X0)),u1_struct_0(sK119))
| v3_struct_0(sK119)
| ~ m1_relset_1(X0,sF383,u1_struct_0(sK119))
| ~ v1_funct_1(X0) )
| ~ spl384_185
| ~ spl384_201
| spl384_206 ),
inference(resolution,[],[f62432,f62174]) ).
fof(f62762,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF383,u1_struct_0(sK119))
| v1_funct_2(k3_waybel_1(sK119,sK119,X0),u1_struct_0(k2_yellow_2(sK119,sK119,X0)),u1_struct_0(sK119))
| ~ m1_relset_1(X0,sF383,u1_struct_0(sK119))
| ~ v1_funct_1(X0) )
| ~ spl384_185
| ~ spl384_201
| spl384_206 ),
inference(forward_subsumption_resolution,[],[f62761,f62359]) ).
fof(f62763,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF383,sF383)
| v1_funct_2(k3_waybel_1(sK119,sK119,X0),u1_struct_0(k2_yellow_2(sK119,sK119,X0)),u1_struct_0(sK119))
| ~ m1_relset_1(X0,sF383,u1_struct_0(sK119))
| ~ v1_funct_1(X0) )
| ~ spl384_185
| ~ spl384_201
| spl384_206 ),
inference(forward_demodulation,[],[f62762,f62263]) ).
fof(f62764,plain,
( ! [X0] :
( v1_funct_2(k3_waybel_1(sK119,sK119,X0),u1_struct_0(k2_yellow_2(sK119,sK119,X0)),sF383)
| ~ v1_funct_2(X0,sF383,sF383)
| ~ m1_relset_1(X0,sF383,u1_struct_0(sK119))
| ~ v1_funct_1(X0) )
| ~ spl384_185
| ~ spl384_201
| spl384_206 ),
inference(forward_demodulation,[],[f62763,f62263]) ).
fof(f62765,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF383,sF383)
| v1_funct_2(k3_waybel_1(sK119,sK119,X0),u1_struct_0(k2_yellow_2(sK119,sK119,X0)),sF383)
| ~ m1_relset_1(X0,sF383,sF383)
| ~ v1_funct_1(X0) )
| ~ spl384_185
| ~ spl384_201
| spl384_206 ),
inference(forward_demodulation,[],[f62764,f62263]) ).
fof(f62766,plain,
( v1_funct_2(k3_waybel_1(sK119,sK119,sK120),u1_struct_0(k2_yellow_2(sK119,sK119,sK120)),sF383)
| ~ spl384_185
| ~ spl384_195
| ~ spl384_196
| ~ spl384_201
| ~ spl384_205
| spl384_206 ),
inference(unit_resulting_resolution,[],[f62765,f62229,f62346,f62224]) ).
fof(f62769,plain,
( v1_funct_2(k3_waybel_1(sK119,sK119,sK120),u1_struct_0(sF381),sF383)
| ~ spl384_185
| ~ spl384_195
| ~ spl384_196
| ~ spl384_199
| ~ spl384_201
| ~ spl384_205
| spl384_206 ),
inference(forward_demodulation,[],[f62766,f62253]) ).
fof(f62771,plain,
( v1_funct_2(k7_grcat_1(sF381),u1_struct_0(sF381),sF383)
| ~ spl384_185
| ~ spl384_195
| ~ spl384_196
| ~ spl384_199
| ~ spl384_201
| ~ spl384_205
| spl384_206
| ~ spl384_228 ),
inference(forward_demodulation,[],[f62769,f62672]) ).
fof(f62774,definition,
( spl384_232
<=> v1_funct_2(k7_grcat_1(sF381),u1_struct_0(sF381),sF383) ),
introduced(definition,[new_symbols(definition,[spl384_232])],[avatar_definition]) ).
fof(f62776,plain,
( v1_funct_2(k7_grcat_1(sF381),u1_struct_0(sF381),sF383)
| ~ spl384_232 ),
inference(avatar_component_clause,[],[f62774]) ).
fof(f62777,plain,
( spl384_232
| ~ spl384_185
| ~ spl384_195
| ~ spl384_196
| ~ spl384_199
| ~ spl384_201
| ~ spl384_205
| spl384_206
| ~ spl384_228 ),
inference(avatar_split_clause,[],[f62771,f62670,f62357,f62344,f62261,f62251,f62227,f62222,f62172,f62774]) ).
fof(f62779,plain,
( sP19(sK120,sK119)
| ~ spl384_185
| ~ spl384_187
| ~ spl384_188
| ~ spl384_189
| ~ spl384_190
| ~ spl384_191
| ~ spl384_192
| ~ spl384_194
| ~ spl384_195
| ~ spl384_196
| ~ spl384_201
| ~ spl384_205
| spl384_206 ),
inference(unit_resulting_resolution,[],[f62723,f62229,f62219,f62346,f62224]) ).
fof(f62783,definition,
( spl384_233
<=> sP19(sK120,sK119) ),
introduced(definition,[new_symbols(definition,[spl384_233])],[avatar_definition]) ).
fof(f62785,plain,
( sP19(sK120,sK119)
| ~ spl384_233 ),
inference(avatar_component_clause,[],[f62783]) ).
fof(f62786,plain,
( spl384_233
| ~ spl384_185
| ~ spl384_187
| ~ spl384_188
| ~ spl384_189
| ~ spl384_190
| ~ spl384_191
| ~ spl384_192
| ~ spl384_194
| ~ spl384_195
| ~ spl384_196
| ~ spl384_201
| ~ spl384_205
| spl384_206 ),
inference(avatar_split_clause,[],[f62779,f62357,f62344,f62261,f62227,f62222,f62217,f62207,f62202,f62197,f62192,f62187,f62182,f62172,f62783]) ).
fof(f62795,plain,
( v2_lattice3(k2_yellow_2(sK119,sK119,sK120))
| ~ spl384_233 ),
inference(resolution,[],[f62785,f58406]) ).
fof(f62796,plain,
( v4_orders_2(k2_yellow_2(sK119,sK119,sK120))
| ~ spl384_233 ),
inference(resolution,[],[f62785,f58414]) ).
fof(f62797,plain,
( v3_orders_2(k2_yellow_2(sK119,sK119,sK120))
| ~ spl384_233 ),
inference(resolution,[],[f62785,f58415]) ).
fof(f62798,plain,
( v1_lattice3(k2_yellow_2(sK119,sK119,sK120))
| ~ spl384_233 ),
inference(resolution,[],[f62785,f58407]) ).
fof(f62799,plain,
( v2_orders_2(k2_yellow_2(sK119,sK119,sK120))
| ~ spl384_233 ),
inference(resolution,[],[f62785,f58416]) ).
fof(f62800,plain,
( v3_lattice3(k2_yellow_2(sK119,sK119,sK120))
| ~ spl384_233 ),
inference(resolution,[],[f62785,f58405]) ).
fof(f62801,plain,
( v3_lattice3(sF381)
| ~ spl384_199
| ~ spl384_233 ),
inference(forward_demodulation,[],[f62800,f62253]) ).
fof(f62802,plain,
( v2_orders_2(sF381)
| ~ spl384_199
| ~ spl384_233 ),
inference(forward_demodulation,[],[f62799,f62253]) ).
fof(f62803,plain,
( v1_lattice3(sF381)
| ~ spl384_199
| ~ spl384_233 ),
inference(forward_demodulation,[],[f62798,f62253]) ).
fof(f62804,plain,
( v3_orders_2(sF381)
| ~ spl384_199
| ~ spl384_233 ),
inference(forward_demodulation,[],[f62797,f62253]) ).
fof(f62805,plain,
( v4_orders_2(sF381)
| ~ spl384_199
| ~ spl384_233 ),
inference(forward_demodulation,[],[f62796,f62253]) ).
fof(f62806,plain,
( v2_lattice3(sF381)
| ~ spl384_199
| ~ spl384_233 ),
inference(forward_demodulation,[],[f62795,f62253]) ).
fof(f62814,definition,
( spl384_234
<=> v3_lattice3(sF381) ),
introduced(definition,[new_symbols(definition,[spl384_234])],[avatar_definition]) ).
fof(f62816,plain,
( v3_lattice3(sF381)
| ~ spl384_234 ),
inference(avatar_component_clause,[],[f62814]) ).
fof(f62817,plain,
( spl384_234
| ~ spl384_199
| ~ spl384_233 ),
inference(avatar_split_clause,[],[f62801,f62783,f62251,f62814]) ).
fof(f62819,definition,
( spl384_235
<=> v2_orders_2(sF381) ),
introduced(definition,[new_symbols(definition,[spl384_235])],[avatar_definition]) ).
fof(f62821,plain,
( v2_orders_2(sF381)
| ~ spl384_235 ),
inference(avatar_component_clause,[],[f62819]) ).
fof(f62822,plain,
( spl384_235
| ~ spl384_199
| ~ spl384_233 ),
inference(avatar_split_clause,[],[f62802,f62783,f62251,f62819]) ).
fof(f62824,definition,
( spl384_236
<=> v1_lattice3(sF381) ),
introduced(definition,[new_symbols(definition,[spl384_236])],[avatar_definition]) ).
fof(f62826,plain,
( v1_lattice3(sF381)
| ~ spl384_236 ),
inference(avatar_component_clause,[],[f62824]) ).
fof(f62827,plain,
( spl384_236
| ~ spl384_199
| ~ spl384_233 ),
inference(avatar_split_clause,[],[f62803,f62783,f62251,f62824]) ).
fof(f62829,definition,
( spl384_237
<=> v3_orders_2(sF381) ),
introduced(definition,[new_symbols(definition,[spl384_237])],[avatar_definition]) ).
fof(f62831,plain,
( v3_orders_2(sF381)
| ~ spl384_237 ),
inference(avatar_component_clause,[],[f62829]) ).
fof(f62832,plain,
( spl384_237
| ~ spl384_199
| ~ spl384_233 ),
inference(avatar_split_clause,[],[f62804,f62783,f62251,f62829]) ).
fof(f62834,definition,
( spl384_238
<=> v4_orders_2(sF381) ),
introduced(definition,[new_symbols(definition,[spl384_238])],[avatar_definition]) ).
fof(f62836,plain,
( v4_orders_2(sF381)
| ~ spl384_238 ),
inference(avatar_component_clause,[],[f62834]) ).
fof(f62837,plain,
( spl384_238
| ~ spl384_199
| ~ spl384_233 ),
inference(avatar_split_clause,[],[f62805,f62783,f62251,f62834]) ).
fof(f62839,definition,
( spl384_239
<=> v2_lattice3(sF381) ),
introduced(definition,[new_symbols(definition,[spl384_239])],[avatar_definition]) ).
fof(f62841,plain,
( v2_lattice3(sF381)
| ~ spl384_239 ),
inference(avatar_component_clause,[],[f62839]) ).
fof(f62842,plain,
( spl384_239
| ~ spl384_199
| ~ spl384_233 ),
inference(avatar_split_clause,[],[f62806,f62783,f62251,f62839]) ).
fof(f62851,plain,
( ! [X0] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK119),u1_struct_0(sK119))
| ~ v7_waybel_1(X0,sK119)
| ~ m2_relset_1(X0,u1_struct_0(sK119),u1_struct_0(sK119))
| ~ v2_orders_2(sK119)
| ~ v3_orders_2(sK119)
| ~ v4_orders_2(sK119)
| ~ v1_lattice3(sK119)
| ~ v2_lattice3(sK119)
| ~ v3_lattice3(sK119)
| v17_waybel_0(k3_waybel_1(sK119,sK119,X0),k2_yellow_2(sK119,sK119,X0),sK119) )
| ~ spl384_185 ),
inference(resolution,[],[f58452,f62174]) ).
fof(f62852,plain,
( ! [X0] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK119),u1_struct_0(sK119))
| ~ v7_waybel_1(X0,sK119)
| ~ m2_relset_1(X0,u1_struct_0(sK119),u1_struct_0(sK119))
| ~ v3_orders_2(sK119)
| ~ v4_orders_2(sK119)
| ~ v1_lattice3(sK119)
| ~ v2_lattice3(sK119)
| ~ v3_lattice3(sK119)
| v17_waybel_0(k3_waybel_1(sK119,sK119,X0),k2_yellow_2(sK119,sK119,X0),sK119) )
| ~ spl384_185
| ~ spl384_192 ),
inference(forward_subsumption_resolution,[],[f62851,f62209]) ).
fof(f62853,plain,
( ! [X0] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK119),u1_struct_0(sK119))
| ~ v7_waybel_1(X0,sK119)
| ~ m2_relset_1(X0,u1_struct_0(sK119),u1_struct_0(sK119))
| ~ v4_orders_2(sK119)
| ~ v1_lattice3(sK119)
| ~ v2_lattice3(sK119)
| ~ v3_lattice3(sK119)
| v17_waybel_0(k3_waybel_1(sK119,sK119,X0),k2_yellow_2(sK119,sK119,X0),sK119) )
| ~ spl384_185
| ~ spl384_191
| ~ spl384_192 ),
inference(forward_subsumption_resolution,[],[f62852,f62204]) ).
fof(f62854,plain,
( ! [X0] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK119),u1_struct_0(sK119))
| ~ v7_waybel_1(X0,sK119)
| ~ m2_relset_1(X0,u1_struct_0(sK119),u1_struct_0(sK119))
| ~ v1_lattice3(sK119)
| ~ v2_lattice3(sK119)
| ~ v3_lattice3(sK119)
| v17_waybel_0(k3_waybel_1(sK119,sK119,X0),k2_yellow_2(sK119,sK119,X0),sK119) )
| ~ spl384_185
| ~ spl384_190
| ~ spl384_191
| ~ spl384_192 ),
inference(forward_subsumption_resolution,[],[f62853,f62199]) ).
fof(f62855,plain,
( ! [X0] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK119),u1_struct_0(sK119))
| ~ v7_waybel_1(X0,sK119)
| ~ m2_relset_1(X0,u1_struct_0(sK119),u1_struct_0(sK119))
| ~ v2_lattice3(sK119)
| ~ v3_lattice3(sK119)
| v17_waybel_0(k3_waybel_1(sK119,sK119,X0),k2_yellow_2(sK119,sK119,X0),sK119) )
| ~ spl384_185
| ~ spl384_189
| ~ spl384_190
| ~ spl384_191
| ~ spl384_192 ),
inference(forward_subsumption_resolution,[],[f62854,f62194]) ).
fof(f62856,plain,
( ! [X0] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK119),u1_struct_0(sK119))
| ~ v7_waybel_1(X0,sK119)
| ~ m2_relset_1(X0,u1_struct_0(sK119),u1_struct_0(sK119))
| ~ v3_lattice3(sK119)
| v17_waybel_0(k3_waybel_1(sK119,sK119,X0),k2_yellow_2(sK119,sK119,X0),sK119) )
| ~ spl384_185
| ~ spl384_188
| ~ spl384_189
| ~ spl384_190
| ~ spl384_191
| ~ spl384_192 ),
inference(forward_subsumption_resolution,[],[f62855,f62189]) ).
fof(f62857,plain,
( ! [X0] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK119),u1_struct_0(sK119))
| ~ v7_waybel_1(X0,sK119)
| ~ m2_relset_1(X0,u1_struct_0(sK119),u1_struct_0(sK119))
| v17_waybel_0(k3_waybel_1(sK119,sK119,X0),k2_yellow_2(sK119,sK119,X0),sK119) )
| ~ spl384_185
| ~ spl384_187
| ~ spl384_188
| ~ spl384_189
| ~ spl384_190
| ~ spl384_191
| ~ spl384_192 ),
inference(forward_subsumption_resolution,[],[f62856,f62184]) ).
fof(f62858,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF383,sF383)
| ~ v1_funct_1(X0)
| ~ v7_waybel_1(X0,sK119)
| ~ m2_relset_1(X0,u1_struct_0(sK119),u1_struct_0(sK119))
| v17_waybel_0(k3_waybel_1(sK119,sK119,X0),k2_yellow_2(sK119,sK119,X0),sK119) )
| ~ spl384_185
| ~ spl384_187
| ~ spl384_188
| ~ spl384_189
| ~ spl384_190
| ~ spl384_191
| ~ spl384_192
| ~ spl384_201 ),
inference(forward_demodulation,[],[f62857,f62263]) ).
fof(f62859,plain,
( ! [X0] :
( ~ v7_waybel_1(X0,sK119)
| ~ v1_funct_2(X0,sF383,sF383)
| ~ v1_funct_1(X0)
| ~ m2_relset_1(X0,sF383,sF383)
| v17_waybel_0(k3_waybel_1(sK119,sK119,X0),k2_yellow_2(sK119,sK119,X0),sK119) )
| ~ spl384_185
| ~ spl384_187
| ~ spl384_188
| ~ spl384_189
| ~ spl384_190
| ~ spl384_191
| ~ spl384_192
| ~ spl384_201 ),
inference(forward_demodulation,[],[f62858,f62263]) ).
fof(f62860,plain,
( v17_waybel_0(k3_waybel_1(sK119,sK119,sK120),k2_yellow_2(sK119,sK119,sK120),sK119)
| ~ spl384_185
| ~ spl384_187
| ~ spl384_188
| ~ spl384_189
| ~ spl384_190
| ~ spl384_191
| ~ spl384_192
| ~ spl384_193
| ~ spl384_194
| ~ spl384_195
| ~ spl384_196
| ~ spl384_201 ),
inference(unit_resulting_resolution,[],[f62859,f62229,f62219,f62214,f62224]) ).
fof(f62863,plain,
( v17_waybel_0(k3_waybel_1(sK119,sK119,sK120),sF381,sK119)
| ~ spl384_185
| ~ spl384_187
| ~ spl384_188
| ~ spl384_189
| ~ spl384_190
| ~ spl384_191
| ~ spl384_192
| ~ spl384_193
| ~ spl384_194
| ~ spl384_195
| ~ spl384_196
| ~ spl384_199
| ~ spl384_201 ),
inference(forward_demodulation,[],[f62860,f62253]) ).
fof(f62865,plain,
( v17_waybel_0(k7_grcat_1(sF381),sF381,sK119)
| ~ spl384_185
| ~ spl384_187
| ~ spl384_188
| ~ spl384_189
| ~ spl384_190
| ~ spl384_191
| ~ spl384_192
| ~ spl384_193
| ~ spl384_194
| ~ spl384_195
| ~ spl384_196
| ~ spl384_199
| ~ spl384_201
| ~ spl384_228 ),
inference(forward_demodulation,[],[f62863,f62672]) ).
fof(f62868,definition,
( spl384_240
<=> v17_waybel_0(k7_grcat_1(sF381),sF381,sK119) ),
introduced(definition,[new_symbols(definition,[spl384_240])],[avatar_definition]) ).
fof(f62870,plain,
( v17_waybel_0(k7_grcat_1(sF381),sF381,sK119)
| ~ spl384_240 ),
inference(avatar_component_clause,[],[f62868]) ).
fof(f62871,plain,
( spl384_240
| ~ spl384_185
| ~ spl384_187
| ~ spl384_188
| ~ spl384_189
| ~ spl384_190
| ~ spl384_191
| ~ spl384_192
| ~ spl384_193
| ~ spl384_194
| ~ spl384_195
| ~ spl384_196
| ~ spl384_199
| ~ spl384_201
| ~ spl384_228 ),
inference(avatar_split_clause,[],[f62865,f62670,f62261,f62251,f62227,f62222,f62217,f62212,f62207,f62202,f62197,f62192,f62187,f62182,f62172,f62868]) ).
fof(f62874,plain,
( ! [X0] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK119),u1_struct_0(sK119))
| ~ v7_waybel_1(X0,sK119)
| ~ m2_relset_1(X0,u1_struct_0(sK119),u1_struct_0(sK119))
| ~ v2_orders_2(sK119)
| ~ v3_orders_2(sK119)
| ~ v4_orders_2(sK119)
| ~ v1_lattice3(sK119)
| ~ v2_lattice3(sK119)
| ~ v3_lattice3(sK119)
| k2_waybel_1(sK119,sK119,X0) = k1_waybel34(k2_yellow_2(sK119,sK119,X0),sK119,k3_waybel_1(sK119,sK119,X0)) )
| ~ spl384_185 ),
inference(resolution,[],[f58450,f62174]) ).
fof(f62875,plain,
( ! [X0] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK119),u1_struct_0(sK119))
| ~ v7_waybel_1(X0,sK119)
| ~ m2_relset_1(X0,u1_struct_0(sK119),u1_struct_0(sK119))
| ~ v3_orders_2(sK119)
| ~ v4_orders_2(sK119)
| ~ v1_lattice3(sK119)
| ~ v2_lattice3(sK119)
| ~ v3_lattice3(sK119)
| k2_waybel_1(sK119,sK119,X0) = k1_waybel34(k2_yellow_2(sK119,sK119,X0),sK119,k3_waybel_1(sK119,sK119,X0)) )
| ~ spl384_185
| ~ spl384_192 ),
inference(forward_subsumption_resolution,[],[f62874,f62209]) ).
fof(f62876,plain,
( ! [X0] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK119),u1_struct_0(sK119))
| ~ v7_waybel_1(X0,sK119)
| ~ m2_relset_1(X0,u1_struct_0(sK119),u1_struct_0(sK119))
| ~ v4_orders_2(sK119)
| ~ v1_lattice3(sK119)
| ~ v2_lattice3(sK119)
| ~ v3_lattice3(sK119)
| k2_waybel_1(sK119,sK119,X0) = k1_waybel34(k2_yellow_2(sK119,sK119,X0),sK119,k3_waybel_1(sK119,sK119,X0)) )
| ~ spl384_185
| ~ spl384_191
| ~ spl384_192 ),
inference(forward_subsumption_resolution,[],[f62875,f62204]) ).
fof(f62877,plain,
( ! [X0] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK119),u1_struct_0(sK119))
| ~ v7_waybel_1(X0,sK119)
| ~ m2_relset_1(X0,u1_struct_0(sK119),u1_struct_0(sK119))
| ~ v1_lattice3(sK119)
| ~ v2_lattice3(sK119)
| ~ v3_lattice3(sK119)
| k2_waybel_1(sK119,sK119,X0) = k1_waybel34(k2_yellow_2(sK119,sK119,X0),sK119,k3_waybel_1(sK119,sK119,X0)) )
| ~ spl384_185
| ~ spl384_190
| ~ spl384_191
| ~ spl384_192 ),
inference(forward_subsumption_resolution,[],[f62876,f62199]) ).
fof(f62878,plain,
( ! [X0] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK119),u1_struct_0(sK119))
| ~ v7_waybel_1(X0,sK119)
| ~ m2_relset_1(X0,u1_struct_0(sK119),u1_struct_0(sK119))
| ~ v2_lattice3(sK119)
| ~ v3_lattice3(sK119)
| k2_waybel_1(sK119,sK119,X0) = k1_waybel34(k2_yellow_2(sK119,sK119,X0),sK119,k3_waybel_1(sK119,sK119,X0)) )
| ~ spl384_185
| ~ spl384_189
| ~ spl384_190
| ~ spl384_191
| ~ spl384_192 ),
inference(forward_subsumption_resolution,[],[f62877,f62194]) ).
fof(f62879,plain,
( ! [X0] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK119),u1_struct_0(sK119))
| ~ v7_waybel_1(X0,sK119)
| ~ m2_relset_1(X0,u1_struct_0(sK119),u1_struct_0(sK119))
| ~ v3_lattice3(sK119)
| k2_waybel_1(sK119,sK119,X0) = k1_waybel34(k2_yellow_2(sK119,sK119,X0),sK119,k3_waybel_1(sK119,sK119,X0)) )
| ~ spl384_185
| ~ spl384_188
| ~ spl384_189
| ~ spl384_190
| ~ spl384_191
| ~ spl384_192 ),
inference(forward_subsumption_resolution,[],[f62878,f62189]) ).
fof(f62880,plain,
( ! [X0] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK119),u1_struct_0(sK119))
| ~ v7_waybel_1(X0,sK119)
| ~ m2_relset_1(X0,u1_struct_0(sK119),u1_struct_0(sK119))
| k2_waybel_1(sK119,sK119,X0) = k1_waybel34(k2_yellow_2(sK119,sK119,X0),sK119,k3_waybel_1(sK119,sK119,X0)) )
| ~ spl384_185
| ~ spl384_187
| ~ spl384_188
| ~ spl384_189
| ~ spl384_190
| ~ spl384_191
| ~ spl384_192 ),
inference(forward_subsumption_resolution,[],[f62879,f62184]) ).
fof(f62881,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF383,sF383)
| ~ v1_funct_1(X0)
| ~ v7_waybel_1(X0,sK119)
| ~ m2_relset_1(X0,u1_struct_0(sK119),u1_struct_0(sK119))
| k2_waybel_1(sK119,sK119,X0) = k1_waybel34(k2_yellow_2(sK119,sK119,X0),sK119,k3_waybel_1(sK119,sK119,X0)) )
| ~ spl384_185
| ~ spl384_187
| ~ spl384_188
| ~ spl384_189
| ~ spl384_190
| ~ spl384_191
| ~ spl384_192
| ~ spl384_201 ),
inference(forward_demodulation,[],[f62880,f62263]) ).
fof(f62882,plain,
( ! [X0] :
( ~ v7_waybel_1(X0,sK119)
| ~ v1_funct_2(X0,sF383,sF383)
| ~ v1_funct_1(X0)
| ~ m2_relset_1(X0,sF383,sF383)
| k2_waybel_1(sK119,sK119,X0) = k1_waybel34(k2_yellow_2(sK119,sK119,X0),sK119,k3_waybel_1(sK119,sK119,X0)) )
| ~ spl384_185
| ~ spl384_187
| ~ spl384_188
| ~ spl384_189
| ~ spl384_190
| ~ spl384_191
| ~ spl384_192
| ~ spl384_201 ),
inference(forward_demodulation,[],[f62881,f62263]) ).
fof(f62883,plain,
( k2_waybel_1(sK119,sK119,sK120) = k1_waybel34(k2_yellow_2(sK119,sK119,sK120),sK119,k3_waybel_1(sK119,sK119,sK120))
| ~ spl384_185
| ~ spl384_187
| ~ spl384_188
| ~ spl384_189
| ~ spl384_190
| ~ spl384_191
| ~ spl384_192
| ~ spl384_193
| ~ spl384_194
| ~ spl384_195
| ~ spl384_196
| ~ spl384_201 ),
inference(unit_resulting_resolution,[],[f62882,f62229,f62219,f62214,f62224]) ).
fof(f62886,plain,
( k2_waybel_1(sK119,sK119,sK120) = k1_waybel34(k2_yellow_2(sK119,sK119,sK120),sK119,k7_grcat_1(sF381))
| ~ spl384_185
| ~ spl384_187
| ~ spl384_188
| ~ spl384_189
| ~ spl384_190
| ~ spl384_191
| ~ spl384_192
| ~ spl384_193
| ~ spl384_194
| ~ spl384_195
| ~ spl384_196
| ~ spl384_201
| ~ spl384_228 ),
inference(forward_demodulation,[],[f62883,f62672]) ).
fof(f62888,plain,
( k2_waybel_1(sK119,sK119,sK120) = k1_waybel34(sF381,sK119,k7_grcat_1(sF381))
| ~ spl384_185
| ~ spl384_187
| ~ spl384_188
| ~ spl384_189
| ~ spl384_190
| ~ spl384_191
| ~ spl384_192
| ~ spl384_193
| ~ spl384_194
| ~ spl384_195
| ~ spl384_196
| ~ spl384_199
| ~ spl384_201
| ~ spl384_228 ),
inference(forward_demodulation,[],[f62886,f62253]) ).
fof(f62890,plain,
( sF382 = k1_waybel34(sF381,sK119,k7_grcat_1(sF381))
| ~ spl384_185
| ~ spl384_187
| ~ spl384_188
| ~ spl384_189
| ~ spl384_190
| ~ spl384_191
| ~ spl384_192
| ~ spl384_193
| ~ spl384_194
| ~ spl384_195
| ~ spl384_196
| ~ spl384_199
| ~ spl384_200
| ~ spl384_201
| ~ spl384_228 ),
inference(forward_demodulation,[],[f62888,f62258]) ).
fof(f62892,plain,
( sK120 = k1_waybel34(sF381,sK119,k7_grcat_1(sF381))
| ~ spl384_185
| ~ spl384_187
| ~ spl384_188
| ~ spl384_189
| ~ spl384_190
| ~ spl384_191
| ~ spl384_192
| ~ spl384_193
| ~ spl384_194
| ~ spl384_195
| ~ spl384_196
| ~ spl384_199
| ~ spl384_200
| ~ spl384_201
| ~ spl384_222
| ~ spl384_228 ),
inference(forward_demodulation,[],[f62890,f62553]) ).
fof(f62895,definition,
( spl384_241
<=> sK120 = k1_waybel34(sF381,sK119,k7_grcat_1(sF381)) ),
introduced(definition,[new_symbols(definition,[spl384_241])],[avatar_definition]) ).
fof(f62897,plain,
( sK120 = k1_waybel34(sF381,sK119,k7_grcat_1(sF381))
| ~ spl384_241 ),
inference(avatar_component_clause,[],[f62895]) ).
fof(f62898,plain,
( spl384_241
| ~ spl384_185
| ~ spl384_187
| ~ spl384_188
| ~ spl384_189
| ~ spl384_190
| ~ spl384_191
| ~ spl384_192
| ~ spl384_193
| ~ spl384_194
| ~ spl384_195
| ~ spl384_196
| ~ spl384_199
| ~ spl384_200
| ~ spl384_201
| ~ spl384_222
| ~ spl384_228 ),
inference(avatar_split_clause,[],[f62892,f62670,f62551,f62261,f62256,f62251,f62227,f62222,f62217,f62212,f62207,f62202,f62197,f62192,f62187,f62182,f62172,f62895]) ).
fof(f63055,plain,
( ! [X0,X1] :
( ~ v1_waybel34(k1_waybel34(X0,sK119,X1),sK119,X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(sK119))
| ~ v17_waybel_0(X1,X0,sK119)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(sK119))
| ~ v2_orders_2(sK119)
| ~ v3_orders_2(sK119)
| ~ v4_orders_2(sK119)
| ~ v1_lattice3(sK119)
| ~ v2_lattice3(sK119)
| ~ v3_lattice3(sK119)
| v22_waybel_0(X1,X0,sK119)
| ~ l1_orders_2(sK119)
| ~ 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) )
| ~ spl384_186 ),
inference(resolution,[],[f58373,f62179]) ).
fof(f63056,plain,
( ! [X0,X1] :
( ~ v1_waybel34(k1_waybel34(X0,sK119,X1),sK119,X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(sK119))
| ~ v17_waybel_0(X1,X0,sK119)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(sK119))
| ~ v3_orders_2(sK119)
| ~ v4_orders_2(sK119)
| ~ v1_lattice3(sK119)
| ~ v2_lattice3(sK119)
| ~ v3_lattice3(sK119)
| v22_waybel_0(X1,X0,sK119)
| ~ l1_orders_2(sK119)
| ~ 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) )
| ~ spl384_186
| ~ spl384_192 ),
inference(forward_subsumption_resolution,[],[f63055,f62209]) ).
fof(f63057,plain,
( ! [X0,X1] :
( ~ v1_waybel34(k1_waybel34(X0,sK119,X1),sK119,X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(sK119))
| ~ v17_waybel_0(X1,X0,sK119)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(sK119))
| ~ v4_orders_2(sK119)
| ~ v1_lattice3(sK119)
| ~ v2_lattice3(sK119)
| ~ v3_lattice3(sK119)
| v22_waybel_0(X1,X0,sK119)
| ~ l1_orders_2(sK119)
| ~ 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) )
| ~ spl384_186
| ~ spl384_191
| ~ spl384_192 ),
inference(forward_subsumption_resolution,[],[f63056,f62204]) ).
fof(f63058,plain,
( ! [X0,X1] :
( ~ v1_waybel34(k1_waybel34(X0,sK119,X1),sK119,X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(sK119))
| ~ v17_waybel_0(X1,X0,sK119)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(sK119))
| ~ v1_lattice3(sK119)
| ~ v2_lattice3(sK119)
| ~ v3_lattice3(sK119)
| v22_waybel_0(X1,X0,sK119)
| ~ l1_orders_2(sK119)
| ~ 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) )
| ~ spl384_186
| ~ spl384_190
| ~ spl384_191
| ~ spl384_192 ),
inference(forward_subsumption_resolution,[],[f63057,f62199]) ).
fof(f63059,plain,
( ! [X0,X1] :
( ~ v1_waybel34(k1_waybel34(X0,sK119,X1),sK119,X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(sK119))
| ~ v17_waybel_0(X1,X0,sK119)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(sK119))
| ~ v2_lattice3(sK119)
| ~ v3_lattice3(sK119)
| v22_waybel_0(X1,X0,sK119)
| ~ l1_orders_2(sK119)
| ~ 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) )
| ~ spl384_186
| ~ spl384_189
| ~ spl384_190
| ~ spl384_191
| ~ spl384_192 ),
inference(forward_subsumption_resolution,[],[f63058,f62194]) ).
fof(f63060,plain,
( ! [X0,X1] :
( ~ v1_waybel34(k1_waybel34(X0,sK119,X1),sK119,X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(sK119))
| ~ v17_waybel_0(X1,X0,sK119)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(sK119))
| ~ v3_lattice3(sK119)
| v22_waybel_0(X1,X0,sK119)
| ~ l1_orders_2(sK119)
| ~ 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) )
| ~ spl384_186
| ~ spl384_188
| ~ spl384_189
| ~ spl384_190
| ~ spl384_191
| ~ spl384_192 ),
inference(forward_subsumption_resolution,[],[f63059,f62189]) ).
fof(f63061,plain,
( ! [X0,X1] :
( ~ v1_waybel34(k1_waybel34(X0,sK119,X1),sK119,X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(sK119))
| ~ v17_waybel_0(X1,X0,sK119)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(sK119))
| v22_waybel_0(X1,X0,sK119)
| ~ l1_orders_2(sK119)
| ~ 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) )
| ~ spl384_186
| ~ spl384_187
| ~ spl384_188
| ~ spl384_189
| ~ spl384_190
| ~ spl384_191
| ~ spl384_192 ),
inference(forward_subsumption_resolution,[],[f63060,f62184]) ).
fof(f63062,plain,
( ! [X0,X1] :
( ~ v1_waybel34(k1_waybel34(X0,sK119,X1),sK119,X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(sK119))
| ~ v17_waybel_0(X1,X0,sK119)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(sK119))
| v22_waybel_0(X1,X0,sK119)
| ~ 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) )
| ~ spl384_185
| ~ spl384_186
| ~ spl384_187
| ~ spl384_188
| ~ spl384_189
| ~ spl384_190
| ~ spl384_191
| ~ spl384_192 ),
inference(forward_subsumption_resolution,[],[f63061,f62174]) ).
fof(f63063,plain,
( ! [X0,X1] :
( ~ v1_funct_2(X1,u1_struct_0(X0),sF383)
| ~ v1_waybel34(k1_waybel34(X0,sK119,X1),sK119,X0)
| ~ v1_funct_1(X1)
| ~ v17_waybel_0(X1,X0,sK119)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(sK119))
| v22_waybel_0(X1,X0,sK119)
| ~ 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) )
| ~ spl384_185
| ~ spl384_186
| ~ spl384_187
| ~ spl384_188
| ~ spl384_189
| ~ spl384_190
| ~ spl384_191
| ~ spl384_192
| ~ spl384_201 ),
inference(forward_demodulation,[],[f63062,f62263]) ).
fof(f63064,plain,
( ! [X0,X1] :
( ~ l1_orders_2(X0)
| ~ v1_funct_2(X1,u1_struct_0(X0),sF383)
| ~ v1_waybel34(k1_waybel34(X0,sK119,X1),sK119,X0)
| ~ v1_funct_1(X1)
| ~ v17_waybel_0(X1,X0,sK119)
| v22_waybel_0(X1,X0,sK119)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ m2_relset_1(X1,u1_struct_0(X0),sF383) )
| ~ spl384_185
| ~ spl384_186
| ~ spl384_187
| ~ spl384_188
| ~ spl384_189
| ~ spl384_190
| ~ spl384_191
| ~ spl384_192
| ~ spl384_201 ),
inference(forward_demodulation,[],[f63063,f62263]) ).
fof(f63803,plain,
( l1_orders_2(sF381)
| ~ spl384_185
| ~ spl384_221 ),
inference(unit_resulting_resolution,[],[f60810,f62541,f62174]) ).
fof(f63811,plain,
( $false
| ~ spl384_185
| spl384_209
| ~ spl384_221 ),
inference(forward_subsumption_resolution,[],[f63803,f62465]) ).
fof(f63812,plain,
( ~ spl384_185
| spl384_209
| ~ spl384_221 ),
inference(avatar_contradiction_clause,[],[f63811]) ).
fof(f63856,definition,
( spl384_311
<=> v1_funct_1(k7_grcat_1(sF381)) ),
introduced(definition,[new_symbols(definition,[spl384_311])],[avatar_definition]) ).
fof(f63857,plain,
( v1_funct_1(k7_grcat_1(sF381))
| ~ spl384_311 ),
inference(avatar_component_clause,[],[f63856]) ).
fof(f63858,plain,
( ~ v1_funct_1(k7_grcat_1(sF381))
| spl384_311 ),
inference(avatar_component_clause,[],[f63856]) ).
fof(f63869,plain,
( v3_struct_0(sF381)
| ~ l1_orders_2(sF381)
| spl384_311 ),
inference(resolution,[],[f63858,f59283]) ).
fof(f63870,plain,
( ~ l1_orders_2(sF381)
| spl384_208
| spl384_311 ),
inference(forward_subsumption_resolution,[],[f63869,f62449]) ).
fof(f63873,plain,
( $false
| spl384_208
| ~ spl384_209
| spl384_311 ),
inference(forward_subsumption_resolution,[],[f63870,f62464]) ).
fof(f63874,plain,
( spl384_208
| ~ spl384_209
| spl384_311 ),
inference(avatar_contradiction_clause,[],[f63873]) ).
fof(f64129,definition,
( spl384_329
<=> m2_relset_1(k7_grcat_1(sF381),u1_struct_0(sF381),sF383) ),
introduced(definition,[new_symbols(definition,[spl384_329])],[avatar_definition]) ).
fof(f64130,plain,
( m2_relset_1(k7_grcat_1(sF381),u1_struct_0(sF381),sF383)
| ~ spl384_329 ),
inference(avatar_component_clause,[],[f64129]) ).
fof(f64131,plain,
( ~ m2_relset_1(k7_grcat_1(sF381),u1_struct_0(sF381),sF383)
| spl384_329 ),
inference(avatar_component_clause,[],[f64129]) ).
fof(f65600,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF383,u1_struct_0(sK119))
| m2_relset_1(k3_waybel_1(sK119,sK119,X0),u1_struct_0(k2_yellow_2(sK119,sK119,X0)),u1_struct_0(sK119))
| v3_struct_0(sK119)
| ~ m1_relset_1(X0,sF383,u1_struct_0(sK119))
| ~ v1_funct_1(X0) )
| ~ spl384_185
| ~ spl384_201
| spl384_206 ),
inference(resolution,[],[f62392,f62174]) ).
fof(f65605,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF383,u1_struct_0(sK119))
| m2_relset_1(k3_waybel_1(sK119,sK119,X0),u1_struct_0(k2_yellow_2(sK119,sK119,X0)),u1_struct_0(sK119))
| ~ m1_relset_1(X0,sF383,u1_struct_0(sK119))
| ~ v1_funct_1(X0) )
| ~ spl384_185
| ~ spl384_201
| spl384_206 ),
inference(forward_subsumption_resolution,[],[f65600,f62359]) ).
fof(f65607,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF383,sF383)
| m2_relset_1(k3_waybel_1(sK119,sK119,X0),u1_struct_0(k2_yellow_2(sK119,sK119,X0)),u1_struct_0(sK119))
| ~ m1_relset_1(X0,sF383,u1_struct_0(sK119))
| ~ v1_funct_1(X0) )
| ~ spl384_185
| ~ spl384_201
| spl384_206 ),
inference(forward_demodulation,[],[f65605,f62263]) ).
fof(f65613,plain,
( ! [X0] :
( m2_relset_1(k3_waybel_1(sK119,sK119,X0),u1_struct_0(k2_yellow_2(sK119,sK119,X0)),sF383)
| ~ v1_funct_2(X0,sF383,sF383)
| ~ m1_relset_1(X0,sF383,u1_struct_0(sK119))
| ~ v1_funct_1(X0) )
| ~ spl384_185
| ~ spl384_201
| spl384_206 ),
inference(forward_demodulation,[],[f65607,f62263]) ).
fof(f65614,plain,
( ! [X0] :
( m2_relset_1(k3_waybel_1(sK119,sK119,X0),u1_struct_0(k2_yellow_2(sK119,sK119,X0)),sF383)
| ~ m1_relset_1(X0,sF383,sF383)
| ~ v1_funct_2(X0,sF383,sF383)
| ~ v1_funct_1(X0) )
| ~ spl384_185
| ~ spl384_201
| spl384_206 ),
inference(forward_demodulation,[],[f65613,f62263]) ).
fof(f65617,plain,
( m2_relset_1(k7_grcat_1(sF381),u1_struct_0(k2_yellow_2(sK119,sK119,sK120)),sF383)
| ~ m1_relset_1(sK120,sF383,sF383)
| ~ v1_funct_2(sK120,sF383,sF383)
| ~ v1_funct_1(sK120)
| ~ spl384_185
| ~ spl384_201
| spl384_206
| ~ spl384_228 ),
inference(superposition,[],[f65614,f62672]) ).
fof(f65620,plain,
( m2_relset_1(k7_grcat_1(sF381),u1_struct_0(k2_yellow_2(sK119,sK119,sK120)),sF383)
| ~ v1_funct_2(sK120,sF383,sF383)
| ~ v1_funct_1(sK120)
| ~ spl384_185
| ~ spl384_201
| ~ spl384_205
| spl384_206
| ~ spl384_228 ),
inference(forward_subsumption_resolution,[],[f65617,f62346]) ).
fof(f65624,plain,
( m2_relset_1(k7_grcat_1(sF381),u1_struct_0(k2_yellow_2(sK119,sK119,sK120)),sF383)
| ~ v1_funct_1(sK120)
| ~ spl384_185
| ~ spl384_195
| ~ spl384_201
| ~ spl384_205
| spl384_206
| ~ spl384_228 ),
inference(forward_subsumption_resolution,[],[f65620,f62224]) ).
fof(f65632,plain,
( m2_relset_1(k7_grcat_1(sF381),u1_struct_0(k2_yellow_2(sK119,sK119,sK120)),sF383)
| ~ spl384_185
| ~ spl384_195
| ~ spl384_196
| ~ spl384_201
| ~ spl384_205
| spl384_206
| ~ spl384_228 ),
inference(forward_subsumption_resolution,[],[f65624,f62229]) ).
fof(f65636,plain,
( m2_relset_1(k7_grcat_1(sF381),u1_struct_0(sF381),sF383)
| ~ spl384_185
| ~ spl384_195
| ~ spl384_196
| ~ spl384_199
| ~ spl384_201
| ~ spl384_205
| spl384_206
| ~ spl384_228 ),
inference(forward_demodulation,[],[f65632,f62253]) ).
fof(f65639,plain,
( $false
| ~ spl384_185
| ~ spl384_195
| ~ spl384_196
| ~ spl384_199
| ~ spl384_201
| ~ spl384_205
| spl384_206
| ~ spl384_228
| spl384_329 ),
inference(forward_subsumption_resolution,[],[f65636,f64131]) ).
fof(f65640,plain,
( ~ spl384_185
| ~ spl384_195
| ~ spl384_196
| ~ spl384_199
| ~ spl384_201
| ~ spl384_205
| spl384_206
| ~ spl384_228
| spl384_329 ),
inference(avatar_contradiction_clause,[],[f65639]) ).
fof(f65667,plain,
( ~ v1_waybel34(k1_waybel34(sF381,sK119,k7_grcat_1(sF381)),sK119,sF381)
| ~ spl384_185
| ~ spl384_186
| ~ spl384_187
| ~ spl384_188
| ~ spl384_189
| ~ spl384_190
| ~ spl384_191
| ~ spl384_192
| ~ spl384_201
| ~ spl384_209
| spl384_229
| ~ spl384_232
| ~ spl384_234
| ~ spl384_235
| ~ spl384_236
| ~ spl384_237
| ~ spl384_238
| ~ spl384_239
| ~ spl384_240
| ~ spl384_311
| ~ spl384_329 ),
inference(unit_resulting_resolution,[],[f63064,f62464,f62816,f62841,f62826,f62836,f62831,f62821,f63857,f62681,f62870,f62776,f64130]) ).
fof(f65688,plain,
( ~ v1_waybel34(sK120,sK119,sF381)
| ~ spl384_185
| ~ spl384_186
| ~ spl384_187
| ~ spl384_188
| ~ spl384_189
| ~ spl384_190
| ~ spl384_191
| ~ spl384_192
| ~ spl384_201
| ~ spl384_209
| spl384_229
| ~ spl384_232
| ~ spl384_234
| ~ spl384_235
| ~ spl384_236
| ~ spl384_237
| ~ spl384_238
| ~ spl384_239
| ~ spl384_240
| ~ spl384_241
| ~ spl384_311
| ~ spl384_329 ),
inference(forward_demodulation,[],[f65667,f62897]) ).
fof(f65697,plain,
( $false
| ~ spl384_185
| ~ spl384_186
| ~ spl384_187
| ~ spl384_188
| ~ spl384_189
| ~ spl384_190
| ~ spl384_191
| ~ spl384_192
| ~ spl384_201
| ~ spl384_209
| ~ spl384_223
| spl384_229
| ~ spl384_232
| ~ spl384_234
| ~ spl384_235
| ~ spl384_236
| ~ spl384_237
| ~ spl384_238
| ~ spl384_239
| ~ spl384_240
| ~ spl384_241
| ~ spl384_311
| ~ spl384_329 ),
inference(forward_subsumption_resolution,[],[f65688,f62559]) ).
fof(f65698,plain,
( ~ spl384_185
| ~ spl384_186
| ~ spl384_187
| ~ spl384_188
| ~ spl384_189
| ~ spl384_190
| ~ spl384_191
| ~ spl384_192
| ~ spl384_201
| ~ spl384_209
| ~ spl384_223
| spl384_229
| ~ spl384_232
| ~ spl384_234
| ~ spl384_235
| ~ spl384_236
| ~ spl384_237
| ~ spl384_238
| ~ spl384_239
| ~ spl384_240
| ~ spl384_241
| ~ spl384_311
| ~ spl384_329 ),
inference(avatar_contradiction_clause,[],[f65697]) ).
cnf(s188,plain,
spl384_185,
inference(sat_conversion,[],[f62175]) ).
cnf(s189,plain,
spl384_186,
inference(sat_conversion,[],[f62180]) ).
cnf(s190,plain,
spl384_187,
inference(sat_conversion,[],[f62185]) ).
cnf(s191,plain,
spl384_188,
inference(sat_conversion,[],[f62190]) ).
cnf(s192,plain,
spl384_189,
inference(sat_conversion,[],[f62195]) ).
cnf(s193,plain,
spl384_190,
inference(sat_conversion,[],[f62200]) ).
cnf(s194,plain,
spl384_191,
inference(sat_conversion,[],[f62205]) ).
cnf(s195,plain,
spl384_192,
inference(sat_conversion,[],[f62210]) ).
cnf(s196,plain,
spl384_193,
inference(sat_conversion,[],[f62215]) ).
cnf(s197,plain,
spl384_194,
inference(sat_conversion,[],[f62220]) ).
cnf(s198,plain,
spl384_195,
inference(sat_conversion,[],[f62225]) ).
cnf(s199,plain,
spl384_196,
inference(sat_conversion,[],[f62230]) ).
cnf(s200,plain,
spl384_197,
inference(sat_conversion,[],[f62235]) ).
cnf(s201,plain,
~ spl384_198,
inference(sat_conversion,[],[f62240]) ).
cnf(s202,plain,
spl384_199,
inference(sat_conversion,[],[f62254]) ).
cnf(s203,plain,
spl384_200,
inference(sat_conversion,[],[f62259]) ).
cnf(s204,plain,
spl384_201,
inference(sat_conversion,[],[f62264]) ).
cnf(s207,plain,
( ~ spl384_185
| ~ spl384_187
| ~ spl384_188
| ~ spl384_189
| ~ spl384_190
| ~ spl384_191
| ~ spl384_192
| ~ spl384_193
| ~ spl384_194
| ~ spl384_195
| ~ spl384_196
| spl384_198
| ~ spl384_199
| ~ spl384_201
| ~ spl384_204 ),
inference(sat_conversion,[],[f62341]) ).
cnf(s208,plain,
( ~ spl384_193
| spl384_205 ),
inference(sat_conversion,[],[f62347]) ).
cnf(s209,plain,
( ~ spl384_185
| ~ spl384_189
| ~ spl384_206 ),
inference(sat_conversion,[],[f62360]) ).
cnf(s211,plain,
( ~ spl384_185
| ~ spl384_193
| ~ spl384_195
| ~ spl384_196
| ~ spl384_201
| spl384_206
| spl384_207 ),
inference(sat_conversion,[],[f62415]) ).
cnf(s213,plain,
( ~ spl384_185
| ~ spl384_195
| ~ spl384_196
| ~ spl384_199
| ~ spl384_201
| ~ spl384_205
| spl384_206
| ~ spl384_208 ),
inference(sat_conversion,[],[f62450]) ).
cnf(s226,plain,
( ~ spl384_185
| ~ spl384_195
| ~ spl384_196
| ~ spl384_199
| ~ spl384_201
| ~ spl384_205
| spl384_206
| spl384_221 ),
inference(sat_conversion,[],[f62542]) ).
cnf(s228,plain,
( ~ spl384_200
| ~ spl384_207
| spl384_222 ),
inference(sat_conversion,[],[f62554]) ).
cnf(s230,plain,
( ~ spl384_197
| ~ spl384_222
| spl384_223 ),
inference(sat_conversion,[],[f62560]) ).
cnf(s239,plain,
( ~ spl384_185
| ~ spl384_193
| ~ spl384_195
| ~ spl384_196
| ~ spl384_199
| ~ spl384_201
| spl384_206
| spl384_228 ),
inference(sat_conversion,[],[f62673]) ).
cnf(s241,plain,
( spl384_204
| ~ spl384_228
| ~ spl384_229 ),
inference(sat_conversion,[],[f62682]) ).
cnf(s247,plain,
( ~ spl384_185
| ~ spl384_195
| ~ spl384_196
| ~ spl384_199
| ~ spl384_201
| ~ spl384_205
| spl384_206
| ~ spl384_228
| spl384_232 ),
inference(sat_conversion,[],[f62777]) ).
cnf(s249,plain,
( ~ spl384_185
| ~ spl384_187
| ~ spl384_188
| ~ spl384_189
| ~ spl384_190
| ~ spl384_191
| ~ spl384_192
| ~ spl384_194
| ~ spl384_195
| ~ spl384_196
| ~ spl384_201
| ~ spl384_205
| spl384_206
| spl384_233 ),
inference(sat_conversion,[],[f62786]) ).
cnf(s251,plain,
( ~ spl384_199
| ~ spl384_233
| spl384_234 ),
inference(sat_conversion,[],[f62817]) ).
cnf(s252,plain,
( ~ spl384_199
| ~ spl384_233
| spl384_235 ),
inference(sat_conversion,[],[f62822]) ).
cnf(s253,plain,
( ~ spl384_199
| ~ spl384_233
| spl384_236 ),
inference(sat_conversion,[],[f62827]) ).
cnf(s254,plain,
( ~ spl384_199
| ~ spl384_233
| spl384_237 ),
inference(sat_conversion,[],[f62832]) ).
cnf(s255,plain,
( ~ spl384_199
| ~ spl384_233
| spl384_238 ),
inference(sat_conversion,[],[f62837]) ).
cnf(s256,plain,
( ~ spl384_199
| ~ spl384_233
| spl384_239 ),
inference(sat_conversion,[],[f62842]) ).
cnf(s263,plain,
( ~ spl384_185
| ~ spl384_187
| ~ spl384_188
| ~ spl384_189
| ~ spl384_190
| ~ spl384_191
| ~ spl384_192
| ~ spl384_193
| ~ spl384_194
| ~ spl384_195
| ~ spl384_196
| ~ spl384_199
| ~ spl384_201
| ~ spl384_228
| spl384_240 ),
inference(sat_conversion,[],[f62871]) ).
cnf(s265,plain,
( ~ spl384_185
| ~ spl384_187
| ~ spl384_188
| ~ spl384_189
| ~ spl384_190
| ~ spl384_191
| ~ spl384_192
| ~ spl384_193
| ~ spl384_194
| ~ spl384_195
| ~ spl384_196
| ~ spl384_199
| ~ spl384_200
| ~ spl384_201
| ~ spl384_222
| ~ spl384_228
| spl384_241 ),
inference(sat_conversion,[],[f62898]) ).
cnf(s344,plain,
( ~ spl384_185
| spl384_209
| ~ spl384_221 ),
inference(sat_conversion,[],[f63812]) ).
cnf(s347,plain,
( spl384_208
| ~ spl384_209
| spl384_311 ),
inference(sat_conversion,[],[f63874]) ).
cnf(s504,plain,
( ~ spl384_185
| ~ spl384_195
| ~ spl384_196
| ~ spl384_199
| ~ spl384_201
| ~ spl384_205
| spl384_206
| ~ spl384_228
| spl384_329 ),
inference(sat_conversion,[],[f65640]) ).
cnf(s512,plain,
( ~ spl384_185
| ~ spl384_186
| ~ spl384_187
| ~ spl384_188
| ~ spl384_189
| ~ spl384_190
| ~ spl384_191
| ~ spl384_192
| ~ spl384_201
| ~ spl384_209
| ~ spl384_223
| spl384_229
| ~ spl384_232
| ~ spl384_234
| ~ spl384_235
| ~ spl384_236
| ~ spl384_237
| ~ spl384_238
| ~ spl384_239
| ~ spl384_240
| ~ spl384_241
| ~ spl384_311
| ~ spl384_329 ),
inference(sat_conversion,[],[f65698]) ).
cnf(s514,plain,
spl384_205,
inference(rat,[],[s208,s196]) ).
cnf(s523,plain,
~ spl384_206,
inference(rat,[],[s209,s192,s188]) ).
cnf(s524,plain,
~ spl384_204,
inference(rat,[],[s207,s190,s204,s202,s201,s199,s198,s197,s196,s195,s194,s193,s192,s191,s188]) ).
cnf(s556,plain,
spl384_228,
inference(rat,[],[s239,s188,s196,s204,s202,s199,s198,s523]) ).
cnf(s558,plain,
spl384_207,
inference(rat,[],[s211,s188,s196,s204,s199,s198,s523]) ).
cnf(s560,plain,
spl384_221,
inference(rat,[],[s226,s188,s514,s198,s204,s202,s199,s523]) ).
cnf(s562,plain,
~ spl384_208,
inference(rat,[],[s213,s188,s514,s198,s204,s202,s199,s523]) ).
cnf(s573,plain,
spl384_233,
inference(rat,[],[s249,s188,s190,s514,s204,s199,s198,s197,s195,s194,s193,s192,s191,s523]) ).
cnf(s598,plain,
~ spl384_229,
inference(rat,[],[s241,s524,s556]) ).
cnf(s599,plain,
spl384_240,
inference(rat,[],[s263,s188,s190,s204,s202,s199,s198,s197,s196,s195,s194,s193,s192,s191,s556]) ).
cnf(s600,plain,
spl384_329,
inference(rat,[],[s504,s523,s188,s514,s198,s204,s202,s199,s556]) ).
cnf(s602,plain,
spl384_232,
inference(rat,[],[s247,s523,s188,s514,s198,s204,s202,s199,s556]) ).
cnf(s604,plain,
spl384_222,
inference(rat,[],[s228,s203,s558]) ).
cnf(s605,plain,
spl384_209,
inference(rat,[],[s344,s188,s560]) ).
cnf(s606,plain,
spl384_239,
inference(rat,[],[s256,s202,s573]) ).
cnf(s607,plain,
spl384_238,
inference(rat,[],[s255,s202,s573]) ).
cnf(s608,plain,
spl384_237,
inference(rat,[],[s254,s202,s573]) ).
cnf(s609,plain,
spl384_236,
inference(rat,[],[s253,s202,s573]) ).
cnf(s610,plain,
spl384_235,
inference(rat,[],[s252,s202,s573]) ).
cnf(s611,plain,
spl384_234,
inference(rat,[],[s251,s202,s573]) ).
cnf(s630,plain,
spl384_223,
inference(rat,[],[s230,s200,s604]) ).
cnf(s632,plain,
spl384_241,
inference(rat,[],[s265,s556,s188,s190,s204,s203,s202,s199,s198,s197,s196,s195,s194,s193,s192,s191,s604]) ).
cnf(s648,plain,
spl384_311,
inference(rat,[],[s347,s562,s605]) ).
cnf(s659,plain,
$false,
inference(rat,[],[s512,s600,s648,s632,s599,s606,s607,s608,s609,s610,s611,s602,s598,s188,s189,s204,s195,s194,s193,s192,s191,s190,s630,s605]) ).
fof(f65704,plain,
$false,
inference(avatar_sat_refutation,[],[s659]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LAT370+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.09 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.20/0.46 % Computer : n020.cluster.edu
% 0.20/0.46 % Model : x86_64 x86_64
% 0.20/0.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/0.46 % Memory : 8046.5625MB
% 0.20/0.46 % OS : Linux 6.8.0-71-generic
% 0.20/0.47 % CPULimit : 300
% 0.20/0.47 % WCLimit : 300
% 0.20/0.47 % DateTime : Sun Sep 27 15:07:13 UTC 2026
% 0.20/0.47 % CPUTime :
% 0.20/0.47 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.25/0.53 Running first-order theorem proving
% 0.25/0.53 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
% 25.73/9.04 % (3508459)Detected formulas, will run a generic FOF schedule.
% 25.73/9.04 % (3508465)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=1199938595:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2949 on theBenchmark for (2949ds/134677Mi)
% 25.73/9.04 % (3508470)dis-21_1_sil=8000:lcm=predicate:random_seed=428180097:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2949 on theBenchmark for (2949ds/129Mi)
% 25.73/9.04 % (3508464)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=4049628420:i=141193_2949 on theBenchmark for (2949ds/141193Mi)
% 25.73/9.04 % (3508468)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=232380619:i=119:av=off:ss=axioms_2949 on theBenchmark for (2949ds/119Mi)
% 25.73/9.04 % (3508467)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3828826849:i=109:sd=1:ins=1:gsp=on:ss=axioms_2949 on theBenchmark for (2949ds/109Mi)
% 25.73/9.04 % (3508466)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=547163967:i=141695:sd=1:nm=32:gsp=on:ss=included_2949 on theBenchmark for (2949ds/141695Mi)
% 25.73/9.04 % (3508470)Instruction limit reached!
% 25.73/9.04 % (3508470)------------------------------
% 25.73/9.04 % (3508470)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.73/9.04 % (3508470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.73/9.04 % (3508470)CaDiCaL version: 2.1.3
% 25.73/9.04 % (3508470)Termination reason: Instruction limit
% 25.73/9.04 % (3508470)Termination phase: SInE selection
% 25.73/9.04 % (3508470)Time elapsed: 0.111 s
% 25.73/9.04 % (3508470)Peak memory usage: 173 MB
% 25.73/9.04 % (3508470)Instructions burned: 130 (million)
% 25.73/9.04 % (3508469)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1735328888:s2a=on:i=139:gtg=position_2949 on theBenchmark for (2949ds/139Mi)
% 25.73/9.04 % (3508467)Instruction limit reached!
% 25.73/9.04 % (3508467)------------------------------
% 25.73/9.04 % (3508467)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.73/9.04 % (3508467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.73/9.04 % (3508467)CaDiCaL version: 2.1.3
% 25.73/9.04 % (3508467)Termination reason: Instruction limit
% 25.73/9.04 % (3508467)Termination phase: SInE selection
% 25.73/9.04 % (3508467)Time elapsed: 0.117 s
% 25.73/9.04 % (3508467)Peak memory usage: 173 MB
% 25.73/9.04 % (3508467)Instructions burned: 109 (million)
% 25.73/9.04 % (3508468)Instruction limit reached!
% 25.73/9.04 % (3508468)------------------------------
% 25.73/9.04 % (3508468)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.73/9.04 % (3508468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.73/9.04 % (3508468)CaDiCaL version: 2.1.3
% 25.73/9.04 % (3508468)Termination reason: Instruction limit
% 25.73/9.04 % (3508468)Termination phase: SInE selection
% 25.73/9.04 % (3508468)Time elapsed: 0.128 s
% 25.73/9.04 % (3508468)Peak memory usage: 173 MB
% 25.73/9.04 % (3508468)Instructions burned: 119 (million)
% 25.73/9.04 % (3508469)Instruction limit reached!
% 25.73/9.04 % (3508469)------------------------------
% 25.73/9.04 % (3508469)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.73/9.05 % (3508469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.73/9.05 % (3508469)CaDiCaL version: 2.1.3
% 25.73/9.05 % (3508469)Termination reason: Instruction limit
% 25.73/9.05 % (3508469)Termination phase: Property scanning
% 25.73/9.05 % (3508469)Time elapsed: 0.125 s
% 25.73/9.05 % (3508469)Peak memory usage: 174 MB
% 25.73/9.05 % (3508469)Instructions burned: 140 (million)
% 25.73/9.05 % (3508478)lrs+10_1_sil=8000:sp=occurrence:random_seed=2580565672:i=285:sd=3:ss=axioms:sgt=8_2946 on theBenchmark for (2946ds/285Mi)
% 25.73/9.05 % (3508479)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3217088575:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2945 on theBenchmark for (2945ds/157Mi)
% 25.73/9.05 % (3508480)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1568692464:i=325:sd=1:ss=axioms:sgt=32_2945 on theBenchmark for (2945ds/325Mi)
% 25.73/9.05 % (3508481)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=3498320847:s2a=on:i=248:s2at=1.23:gtg=position_2944 on theBenchmark for (2944ds/248Mi)
% 25.73/9.05 % (3508479)Instruction limit reached!
% 36.65/10.74 % (3508479)------------------------------
% 36.65/10.74 % (3508479)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.65/10.74 % (3508479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.65/10.74 % (3508479)CaDiCaL version: 2.1.3
% 36.65/10.74 % (3508479)Termination reason: Instruction limit
% 36.65/10.74 % (3508479)Termination phase: Property scanning
% 36.65/10.74 % (3508479)Time elapsed: 0.139 s
% 36.65/10.74 % (3508479)Peak memory usage: 174 MB
% 36.65/10.74 % (3508479)Instructions burned: 158 (million)
% 36.65/10.74 % (3508478)Instruction limit reached!
% 36.65/10.74 % (3508478)------------------------------
% 36.65/10.74 % (3508478)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.65/10.74 % (3508478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.65/10.74 % (3508478)CaDiCaL version: 2.1.3
% 36.65/10.74 % (3508478)Termination reason: Instruction limit
% 36.65/10.74 % (3508478)Termination phase: SInE selection
% 36.65/10.74 % (3508478)Time elapsed: 0.306 s
% 36.65/10.74 % (3508478)Peak memory usage: 174 MB
% 36.65/10.74 % (3508478)Instructions burned: 285 (million)
% 36.65/10.74 % (3508481)Instruction limit reached!
% 36.65/10.74 % (3508481)------------------------------
% 36.65/10.74 % (3508481)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.65/10.74 % (3508481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.65/10.74 % (3508481)CaDiCaL version: 2.1.3
% 36.65/10.74 % (3508481)Termination reason: Instruction limit
% 36.65/10.74 % (3508481)Termination phase: Property scanning
% 36.65/10.74 % (3508481)Time elapsed: 0.214 s
% 36.65/10.74 % (3508481)Peak memory usage: 174 MB
% 36.65/10.74 % (3508481)Instructions burned: 249 (million)
% 36.65/10.74 % (3508486)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=714494468:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2940 on theBenchmark for (2940ds/294Mi)
% 36.65/10.74 % (3508480)Instruction limit reached!
% 36.65/10.74 % (3508480)------------------------------
% 36.65/10.74 % (3508480)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.65/10.74 % (3508480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.65/10.74 % (3508480)CaDiCaL version: 2.1.3
% 36.65/10.74 % (3508480)Termination reason: Instruction limit
% 36.65/10.74 % (3508480)Termination phase: SInE selection
% 36.65/10.74 % (3508480)Time elapsed: 0.349 s
% 36.65/10.74 % (3508480)Peak memory usage: 174 MB
% 36.65/10.74 % (3508480)Instructions burned: 325 (million)
% 36.65/10.74 % (3508486)Instruction limit reached!
% 36.65/10.74 % (3508486)------------------------------
% 36.65/10.74 % (3508486)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.65/10.74 % (3508486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.65/10.74 % (3508486)CaDiCaL version: 2.1.3
% 36.65/10.74 % (3508486)Termination reason: Instruction limit
% 36.65/10.74 % (3508486)Termination phase: SInE selection
% 36.65/10.74 % (3508486)Time elapsed: 0.154 s
% 36.65/10.74 % (3508486)Peak memory usage: 174 MB
% 36.65/10.74 % (3508486)Instructions burned: 294 (million)
% 36.65/10.74 % (3508488)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1103873190:cts=off:i=113:fsr=off:ss=included:sgt=4_2939 on theBenchmark for (2939ds/113Mi)
% 36.65/10.74 % (3508487)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1647404270:i=2350_2939 on theBenchmark for (2939ds/2350Mi)
% 36.65/10.74 % (3508490)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3030962275:i=127:av=off:fsr=off:sup=off_2938 on theBenchmark for (2938ds/127Mi)
% 36.65/10.74 % (3508491)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1889852301:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2937 on theBenchmark for (2937ds/114Mi)
% 36.65/10.74 % (3508488)Instruction limit reached!
% 36.65/10.74 % (3508488)------------------------------
% 36.65/10.74 % (3508488)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.65/10.74 % (3508488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.65/10.74 % (3508488)CaDiCaL version: 2.1.3
% 36.65/10.74 % (3508488)Termination reason: Instruction limit
% 36.65/10.74 % (3508488)Termination phase: SInE selection
% 36.65/10.74 % (3508488)Time elapsed: 0.127 s
% 36.65/10.74 % (3508488)Peak memory usage: 173 MB
% 36.65/10.74 % (3508488)Instructions burned: 113 (million)
% 36.65/10.74 % (3508491)Instruction limit reached!
% 36.65/10.74 % (3508491)------------------------------
% 36.65/10.74 % (3508491)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.26/15.12 % (3508491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.26/15.12 % (3508491)CaDiCaL version: 2.1.3
% 68.26/15.12 % (3508491)Termination reason: Instruction limit
% 68.26/15.12 % (3508491)Termination phase: Property scanning
% 68.26/15.12 % (3508491)Time elapsed: 0.030 s
% 68.26/15.12 % (3508491)Peak memory usage: 174 MB
% 68.26/15.12 % (3508491)Instructions burned: 116 (million)
% 68.26/15.12 % (3508490)Instruction limit reached!
% 68.26/15.12 % (3508490)------------------------------
% 68.26/15.12 % (3508490)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.26/15.12 % (3508490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.26/15.12 % (3508490)CaDiCaL version: 2.1.3
% 68.26/15.12 % (3508490)Termination reason: Instruction limit
% 68.26/15.12 % (3508490)Termination phase: Preprocessing 1
% 68.26/15.12 % (3508490)Time elapsed: 0.153 s
% 68.26/15.12 % (3508490)Peak memory usage: 175 MB
% 68.26/15.12 % (3508490)Instructions burned: 127 (million)
% 68.26/15.12 % (3508496)lrs+10_1_sil=8000:sp=occurrence:random_seed=2108576326:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2936 on theBenchmark for (2936ds/907Mi)
% 68.26/15.12 % (3508497)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1488020203:i=437:sd=1:aac=none:ss=included_2936 on theBenchmark for (2936ds/437Mi)
% 68.26/15.12 % (3508498)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=755421050:i=5202:ss=axioms:sgt=16_2934 on theBenchmark for (2934ds/5202Mi)
% 68.26/15.12 % (3508496)Instruction limit reached!
% 68.26/15.12 % (3508496)------------------------------
% 68.26/15.12 % (3508496)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.26/15.12 % (3508496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.26/15.12 % (3508496)CaDiCaL version: 2.1.3
% 68.26/15.12 % (3508496)Termination reason: Instruction limit
% 68.26/15.12 % (3508496)Termination phase: Preprocessing 3
% 68.26/15.12 % (3508496)Time elapsed: 0.410 s
% 68.26/15.12 % (3508496)Peak memory usage: 190 MB
% 68.26/15.12 % (3508496)Instructions burned: 907 (million)
% 68.26/15.12 % (3508497)Instruction limit reached!
% 68.26/15.12 % (3508497)------------------------------
% 68.26/15.12 % (3508497)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.26/15.12 % (3508497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.26/15.12 % (3508497)CaDiCaL version: 2.1.3
% 68.26/15.12 % (3508497)Termination reason: Instruction limit
% 68.26/15.12 % (3508497)Termination phase: Preprocessing 1
% 68.26/15.12 % (3508497)Time elapsed: 0.500 s
% 68.26/15.12 % (3508497)Peak memory usage: 175 MB
% 68.26/15.12 % (3508497)Instructions burned: 437 (million)
% 68.26/15.12 % (3508502)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2743171263:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2929 on theBenchmark for (2929ds/134Mi)
% 68.26/15.12 % (3508502)Instruction limit reached!
% 68.26/15.12 % (3508502)------------------------------
% 68.26/15.12 % (3508502)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.26/15.12 % (3508502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.26/15.12 % (3508502)CaDiCaL version: 2.1.3
% 68.26/15.12 % (3508502)Termination reason: Instruction limit
% 68.26/15.12 % (3508502)Termination phase: SInE selection
% 68.26/15.12 % (3508502)Time elapsed: 0.061 s
% 68.26/15.12 % (3508502)Peak memory usage: 173 MB
% 68.26/15.12 % (3508502)Instructions burned: 135 (million)
% 68.26/15.12 % (3508504)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2022992252:st=8:i=592:sd=3:ep=RST:ss=axioms_2928 on theBenchmark for (2928ds/592Mi)
% 68.26/15.12 % (3508505)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1523980814:st=3:i=13193:sd=3:ss=axioms_2927 on theBenchmark for (2927ds/13193Mi)
% 68.26/15.12 % (3508504)Instruction limit reached!
% 68.26/15.12 % (3508504)------------------------------
% 68.26/15.12 % (3508504)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.26/15.12 % (3508504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.26/15.12 % (3508504)CaDiCaL version: 2.1.3
% 68.26/15.12 % (3508504)Termination reason: Instruction limit
% 68.26/15.12 % (3508504)Termination phase: SInE selection
% 68.26/15.12 % (3508504)Time elapsed: 0.406 s
% 68.26/15.12 % (3508504)Peak memory usage: 175 MB
% 68.26/15.12 % (3508504)Instructions burned: 592 (million)
% 68.26/15.12 % (3508508)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=2674014774:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2922 on theBenchmark for (2922ds/125Mi)
% 40.36/16.45 % (3508508)Instruction limit reached!
% 40.36/16.45 % (3508508)------------------------------
% 40.36/16.45 % (3508508)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.36/16.45 % (3508508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.36/16.45 % (3508508)CaDiCaL version: 2.1.3
% 40.36/16.45 % (3508508)Termination reason: Instruction limit
% 40.36/16.45 % (3508508)Termination phase: Property scanning
% 40.36/16.45 % (3508508)Time elapsed: 0.114 s
% 40.36/16.45 % (3508508)Peak memory usage: 174 MB
% 40.36/16.45 % (3508508)Instructions burned: 125 (million)
% 40.36/16.45 % (3508510)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1674651393:i=134:gtgl=5:slsql=off:gtg=exists_sym_2919 on theBenchmark for (2919ds/134Mi)
% 40.36/16.45 % (3508510)Instruction limit reached!
% 40.36/16.45 % (3508510)------------------------------
% 40.36/16.45 % (3508510)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.36/16.45 % (3508510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.36/16.45 % (3508510)CaDiCaL version: 2.1.3
% 40.36/16.45 % (3508510)Termination reason: Instruction limit
% 40.36/16.45 % (3508510)Termination phase: Property scanning
% 40.36/16.45 % (3508510)Time elapsed: 0.120 s
% 40.36/16.45 % (3508510)Peak memory usage: 174 MB
% 40.36/16.45 % (3508510)Instructions burned: 135 (million)
% 40.36/16.45 % (3508487)Instruction limit reached!
% 40.36/16.45 % (3508487)------------------------------
% 40.36/16.45 % (3508487)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.36/16.45 % (3508487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.36/16.45 % (3508487)CaDiCaL version: 2.1.3
% 40.36/16.45 % (3508487)Termination reason: Instruction limit
% 40.36/16.45 % (3508487)Termination phase: Preprocessing 3
% 40.36/16.45 % (3508487)Time elapsed: 2.339 s
% 40.36/16.45 % (3508487)Peak memory usage: 276 MB
% 40.36/16.45 % (3508487)Instructions burned: 2352 (million)
% 40.36/16.45 % (3508512)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3034766654:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2915 on theBenchmark for (2915ds/141Mi)
% 40.36/16.45 % (3508513)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3813607278:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2913 on theBenchmark for (2913ds/431Mi)
% 40.36/16.45 % (3508512)Instruction limit reached!
% 40.36/16.45 % (3508512)------------------------------
% 40.36/16.45 % (3508512)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.36/16.45 % (3508512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.36/16.45 % (3508512)CaDiCaL version: 2.1.3
% 40.36/16.45 % (3508512)Termination reason: Instruction limit
% 40.36/16.45 % (3508512)Termination phase: SInE selection
% 40.36/16.45 % (3508512)Time elapsed: 0.159 s
% 40.36/16.45 % (3508512)Peak memory usage: 173 MB
% 40.36/16.45 % (3508512)Instructions burned: 141 (million)
% 40.36/16.45 % (3508516)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=3521779122:i=6060:aac=none:ins=25_2910 on theBenchmark for (2910ds/6060Mi)
% 40.36/16.45 % (3508513)Instruction limit reached!
% 40.36/16.45 % (3508513)------------------------------
% 40.36/16.45 % (3508513)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.36/16.45 % (3508513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.36/16.45 % (3508513)CaDiCaL version: 2.1.3
% 40.36/16.45 % (3508513)Termination reason: Instruction limit
% 40.36/16.45 % (3508513)Termination phase: Unused predicate definition removal
% 40.36/16.45 % (3508513)Time elapsed: 0.466 s
% 40.36/16.45 % (3508513)Peak memory usage: 176 MB
% 40.36/16.45 % (3508513)Instructions burned: 431 (million)
% 40.36/16.45 % (3508518)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=4134397533:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2906 on theBenchmark for (2906ds/150Mi)
% 40.36/16.45 % (3508518)Instruction limit reached!
% 40.36/16.45 % (3508518)------------------------------
% 40.36/16.45 % (3508518)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.36/16.45 % (3508518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.36/16.45 % (3508518)CaDiCaL version: 2.1.3
% 40.36/16.45 % (3508518)Termination reason: Instruction limit
% 40.36/16.45 % (3508518)Termination phase: SInE selection
% 40.36/16.45 % (3508518)Time elapsed: 0.121 s
% 40.36/16.45 % (3508518)Peak memory usage: 173 MB
% 40.36/16.45 % (3508518)Instructions burned: 150 (million)
% 40.36/16.45 % (3508520)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2122478506:i=14155:bd=all_2903 on theBenchmark for (2903ds/14155Mi)
% 40.36/16.45 % (3508498)Instruction limit reached!
% 40.36/16.45 % (3508498)------------------------------
% 40.36/16.45 % (3508498)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.36/16.45 % (3508498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.36/16.45 % (3508498)CaDiCaL version: 2.1.3
% 40.36/16.45 % (3508498)Termination reason: Instruction limit
% 40.36/16.45 % (3508498)Termination phase: Saturation
% 40.36/16.45 % (3508498)Time elapsed: 4.199 s
% 40.36/16.45 % (3508498)Peak memory usage: 291 MB
% 40.36/16.45 % (3508498)Instructions burned: 5204 (million)
% 40.36/16.45 % (3508523)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1877135120:i=667:av=off:fsr=off_2889 on theBenchmark for (2889ds/667Mi)
% 40.36/16.45 % (3508505)Instruction limit reached!
% 40.36/16.45 % (3508505)------------------------------
% 40.36/16.45 % (3508505)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.36/16.45 % (3508505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.36/16.45 % (3508505)CaDiCaL version: 2.1.3
% 40.36/16.45 % (3508505)Termination reason: Instruction limit
% 40.36/16.45 % (3508505)Termination phase: Saturation
% 40.36/16.45 % (3508505)Time elapsed: 4.453 s
% 40.36/16.45 % (3508505)Peak memory usage: 410 MB
% 40.36/16.45 % (3508505)Instructions burned: 13196 (million)
% 40.36/16.45 % (3508523)Instruction limit reached!
% 40.36/16.45 % (3508523)------------------------------
% 40.36/16.45 % (3508523)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.36/16.45 % (3508523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.36/16.45 % (3508523)CaDiCaL version: 2.1.3
% 40.36/16.45 % (3508523)Termination reason: Instruction limit
% 40.36/16.45 % (3508523)Termination phase: Preprocessing 2
% 40.36/16.45 % (3508523)Time elapsed: 0.601 s
% 40.36/16.45 % (3508523)Peak memory usage: 215 MB
% 40.36/16.45 % (3508523)Instructions burned: 667 (million)
% 40.36/16.45 % (3508525)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=1123016168:s2a=on:i=185:s2at=1.8:fdi=4_2881 on theBenchmark for (2881ds/185Mi)
% 40.36/16.45 % (3508526)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=3931165331:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2881 on theBenchmark for (2881ds/193Mi)
% 40.36/16.45 % (3508525)Instruction limit reached!
% 40.36/16.45 % (3508525)------------------------------
% 40.36/16.45 % (3508525)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.36/16.45 % (3508525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.36/16.45 % (3508525)CaDiCaL version: 2.1.3
% 40.36/16.45 % (3508525)Termination reason: Instruction limit
% 40.36/16.45 % (3508525)Termination phase: SInE selection
% 40.36/16.45 % (3508525)Time elapsed: 0.082 s
% 40.36/16.45 % (3508525)Peak memory usage: 173 MB
% 40.36/16.45 % (3508525)Instructions burned: 187 (million)
% 40.36/16.45 % (3508526)Instruction limit reached!
% 40.36/16.45 % (3508526)------------------------------
% 40.36/16.45 % (3508526)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.36/16.45 % (3508526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.36/16.45 % (3508526)CaDiCaL version: 2.1.3
% 40.36/16.45 % (3508526)Termination reason: Instruction limit
% 40.36/16.45 % (3508526)Termination phase: SInE selection
% 40.36/16.45 % (3508526)Time elapsed: 0.155 s
% 40.36/16.45 % (3508526)Peak memory usage: 173 MB
% 40.36/16.45 % (3508526)Instructions burned: 193 (million)
% 40.36/16.45 % (3508529)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=4151153394:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2879 on theBenchmark for (2879ds/4850Mi)
% 40.36/16.45 % (3508531)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=2051383184:i=12111:sd=1:ss=included_2878 on theBenchmark for (2878ds/12111Mi)
% 40.36/16.45 % (3508529)Instruction limit reached!
% 40.36/16.45 % (3508529)------------------------------
% 40.36/16.45 % (3508529)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.36/16.45 % (3508529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.36/16.45 % (3508529)CaDiCaL version: 2.1.3
% 40.36/16.45 % (3508529)Termination reason: Instruction limit
% 40.36/16.45 % (3508529)Termination phase: Function definition elimination
% 40.36/16.45 % (3508529)Time elapsed: 1.833 s
% 40.36/16.45 % (3508529)Peak memory usage: 295 MB
% 40.36/16.45 % (3508529)Instructions burned: 4852 (million)
% 40.36/16.45 % (3508533)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3977112317:i=319:kws=precedence:fsr=off_2859 on theBenchmark for (2859ds/319Mi)
% 40.36/16.45 % (3508516)Instruction limit reached!
% 40.36/16.45 % (3508516)------------------------------
% 40.36/16.45 % (3508516)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.36/16.45 % (3508516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.36/16.45 % (3508516)CaDiCaL version: 2.1.3
% 40.36/16.45 % (3508516)Termination reason: Instruction limit
% 40.36/16.45 % (3508516)Termination phase: NewCNF
% 40.36/16.45 % (3508516)Time elapsed: 5.068 s
% 40.36/16.45 % (3508516)Peak memory usage: 331 MB
% 40.36/16.45 % (3508516)Instructions burned: 6060 (million)
% 40.36/16.45 % (3508533)Instruction limit reached!
% 40.36/16.45 % (3508533)------------------------------
% 40.36/16.45 % (3508533)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.36/16.45 % (3508533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.36/16.45 % (3508533)CaDiCaL version: 2.1.3
% 40.36/16.45 % (3508533)Termination reason: Instruction limit
% 40.36/16.45 % (3508533)Termination phase: Preprocessing 1
% 40.36/16.45 % (3508533)Time elapsed: 0.137 s
% 40.36/16.45 % (3508533)Peak memory usage: 176 MB
% 40.36/16.45 % (3508533)Instructions burned: 320 (million)
% 40.36/16.45 % (3508535)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=2240887478:i=2064:ep=RST_2857 on theBenchmark for (2857ds/2064Mi)
% 40.36/16.45 % (3508536)dis-1011_128_sil=32000:random_seed=2697341965:i=3706:ep=RST:av=off_2856 on theBenchmark for (2856ds/3706Mi)
% 40.36/16.45 % (3508531)First to succeed.
% 40.36/16.45 % (3508531)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3508459"
% 40.36/16.45 % (3508531)Refutation found. Thanks to Tanya!
% 40.36/16.45 % SZS status Theorem for theBenchmark
% 40.36/16.45 % SZS output start Proof for theBenchmark
% See solution above
% 78.23/16.69 % (3508531)------------------------------
% 78.23/16.69 % (3508531)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 78.23/16.69 % (3508531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.23/16.69 % (3508531)CaDiCaL version: 2.1.3
% 78.23/16.69 % (3508531)Termination reason: Refutation
% 78.23/16.69 % (3508531)Time elapsed: 2.579 s
% 78.23/16.69 % (3508531)Peak memory usage: 273 MB
% 78.23/16.69 % (3508531)Instructions burned: 3841 (million)
% 78.23/16.69 % (3508531)------------------------------
% 78.23/16.69 % (3508531)------------------------------
% 78.23/16.69 % (3508459)Success in time 15.334 s
% 78.23/16.69 % Vampire exiting
%------------------------------------------------------------------------------