%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT353+3 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:47:13 AM UTC 2026
% Result : Theorem 95.02s 16.86s
% Output : Refutation 112.64s
% Verified :
% SZS Type : Refutation
% Derivation depth : 69
% Number of leaves : 25
% Syntax : Number of formulae : 290 ( 59 unt; 15 def)
% Number of atoms : 2267 ( 39 equ)
% Maximal formula atoms : 27 ( 7 avg)
% Number of connectives : 3619 (1642 ~;1749 |; 184 &)
% ( 18 <=>; 26 =>; 0 <=; 0 <~>)
% Maximal formula depth : 29 ( 9 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 33 ( 31 usr; 9 prp; 0-3 aty)
% Number of functors : 20 ( 20 usr; 11 con; 0-4 aty)
% Number of variables : 230 ( 0 sgn 219 !; 11 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1394,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
<=> m1_relset_1(X2,X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(f7885,axiom,
! [X0] :
( l1_orders_2(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l1_orders_2) ).
fof(f11560,axiom,
! [X0] :
( l1_orders_2(X0)
=> ( v1_lattice3(X0)
=> ~ v3_struct_0(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc1_lattice3) ).
fof(f15209,axiom,
! [X0,X1,X2,X3] :
( ( ~ v1_xboole_0(X0)
& ~ v3_struct_0(X1)
& l1_struct_0(X1)
& v1_funct_1(X2)
& v1_funct_2(X2,X0,u1_struct_0(X1))
& m1_relset_1(X2,X0,u1_struct_0(X1))
& m1_subset_1(X3,X0) )
=> m1_subset_1(k7_yellow_2(X0,X1,X2,X3),u1_struct_0(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k7_yellow_2) ).
fof(f15255,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( r4_waybel_1(X0,X1,X2)
<=> ( r1_yellow_0(X0,X2)
& X1 = k1_yellow_0(X0,X2)
& r2_hidden(k1_yellow_0(X0,X2),X2) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d7_waybel_1) ).
fof(f15266,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v2_orders_2(X1)
& v3_orders_2(X1)
& v4_orders_2(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)) )
=> ! [X3] :
( ( v1_funct_1(X3)
& v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X0))
& m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X0)) )
=> ( v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1)
<=> ( v5_orders_3(X3,X1,X0)
& ! [X4] :
( m1_subset_1(X4,u1_struct_0(X0))
=> r4_waybel_1(X1,k7_yellow_2(u1_struct_0(X0),X1,X2,X4),k5_pre_topc(X1,X0,X3,k6_waybel_0(X0,X4))) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t12_waybel_1) ).
fof(f16826,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_orders_2(X0)
& v3_orders_2(X0)
& v1_lattice3(X0)
& l1_orders_2(X0) )
=> ( ~ v1_xboole_0(u1_struct_0(X0))
& v1_waybel_0(u1_struct_0(X0),X0)
& v12_waybel_0(u1_struct_0(X0),X0)
& m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(u1_struct_0(X0))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t4_waybel13) ).
fof(f18894,axiom,
! [X0,X1,X2] :
( ( v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& v2_lattice3(X0)
& l1_orders_2(X0)
& v2_orders_2(X1)
& v3_orders_2(X1)
& v4_orders_2(X1)
& v1_lattice3(X1)
& v2_lattice3(X1)
& l1_orders_2(X1)
& v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
& m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0)) )
=> ( v1_funct_1(k2_waybel34(X0,X1,X2))
& v1_funct_2(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
& m2_relset_1(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k2_waybel34) ).
fof(f18907,axiom,
! [X0] :
( ( v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& v2_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)
& l1_orders_2(X1) )
=> ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
& m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0)) )
=> ( ( v3_lattice3(X0)
& v3_lattice3(X1)
& v18_waybel_0(X2,X1,X0) )
=> ! [X3] :
( ( v1_funct_1(X3)
& v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
& m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1)) )
=> ( X3 = k2_waybel34(X0,X1,X2)
<=> v3_waybel_1(k1_waybel_1(X0,X1,X3,X2),X0,X1) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d2_waybel34) ).
fof(f18913,conjecture,
! [X0] :
( ( v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& v2_lattice3(X0)
& v3_lattice3(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( ( v2_orders_2(X1)
& v3_orders_2(X1)
& v4_orders_2(X1)
& v1_lattice3(X1)
& v2_lattice3(X1)
& v3_lattice3(X1)
& l1_orders_2(X1) )
=> ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
& v18_waybel_0(X2,X1,X0)
& m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0)) )
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
=> k7_yellow_2(u1_struct_0(X0),X1,k2_waybel34(X0,X1,X2),X3) = k1_yellow_0(X1,k5_pre_topc(X1,X0,X2,k6_waybel_0(X0,X3))) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t3_waybel34) ).
fof(f18914,negated_conjecture,
~ ! [X0] :
( ( v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& v2_lattice3(X0)
& v3_lattice3(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( ( v2_orders_2(X1)
& v3_orders_2(X1)
& v4_orders_2(X1)
& v1_lattice3(X1)
& v2_lattice3(X1)
& v3_lattice3(X1)
& l1_orders_2(X1) )
=> ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
& v18_waybel_0(X2,X1,X0)
& m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0)) )
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
=> k7_yellow_2(u1_struct_0(X0),X1,k2_waybel34(X0,X1,X2),X3) = k1_yellow_0(X1,k5_pre_topc(X1,X0,X2,k6_waybel_0(X0,X3))) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f18913]) ).
fof(f28555,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f7885]) ).
fof(f34372,plain,
! [X0] :
( ~ v3_struct_0(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f11560]) ).
fof(f34373,plain,
! [X0] :
( ~ v3_struct_0(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f34372]) ).
fof(f40673,plain,
! [X0,X1,X2,X3] :
( m1_subset_1(k7_yellow_2(X0,X1,X2,X3),u1_struct_0(X1))
| v1_xboole_0(X0)
| v3_struct_0(X1)
| ~ l1_struct_0(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,X0,u1_struct_0(X1))
| ~ m1_relset_1(X2,X0,u1_struct_0(X1))
| ~ m1_subset_1(X3,X0) ),
inference(ennf_transformation,[],[f15209]) ).
fof(f40674,plain,
! [X0,X1,X2,X3] :
( m1_subset_1(k7_yellow_2(X0,X1,X2,X3),u1_struct_0(X1))
| v1_xboole_0(X0)
| v3_struct_0(X1)
| ~ l1_struct_0(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,X0,u1_struct_0(X1))
| ~ m1_relset_1(X2,X0,u1_struct_0(X1))
| ~ m1_subset_1(X3,X0) ),
inference(flattening,[],[f40673]) ).
fof(f40754,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( r4_waybel_1(X0,X1,X2)
<=> ( r1_yellow_0(X0,X2)
& X1 = k1_yellow_0(X0,X2)
& r2_hidden(k1_yellow_0(X0,X2),X2) ) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f15255]) ).
fof(f40755,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( r4_waybel_1(X0,X1,X2)
<=> ( r1_yellow_0(X0,X2)
& X1 = k1_yellow_0(X0,X2)
& r2_hidden(k1_yellow_0(X0,X2),X2) ) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f40754]) ).
fof(f40774,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1)
<=> ( v5_orders_3(X3,X1,X0)
& ! [X4] :
( r4_waybel_1(X1,k7_yellow_2(u1_struct_0(X0),X1,X2,X4),k5_pre_topc(X1,X0,X3,k6_waybel_0(X0,X4)))
| ~ m1_subset_1(X4,u1_struct_0(X0)) ) ) )
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X0))
| ~ m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X0)) )
| ~ 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)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ l1_orders_2(X1) )
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f15266]) ).
fof(f40775,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1)
<=> ( v5_orders_3(X3,X1,X0)
& ! [X4] :
( r4_waybel_1(X1,k7_yellow_2(u1_struct_0(X0),X1,X2,X4),k5_pre_topc(X1,X0,X3,k6_waybel_0(X0,X4)))
| ~ m1_subset_1(X4,u1_struct_0(X0)) ) ) )
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X0))
| ~ m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X0)) )
| ~ 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)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ l1_orders_2(X1) )
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f40774]) ).
fof(f43646,plain,
! [X0] :
( ( ~ v1_xboole_0(u1_struct_0(X0))
& v1_waybel_0(u1_struct_0(X0),X0)
& v12_waybel_0(u1_struct_0(X0),X0)
& m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f16826]) ).
fof(f43647,plain,
! [X0] :
( ( ~ v1_xboole_0(u1_struct_0(X0))
& v1_waybel_0(u1_struct_0(X0),X0)
& v12_waybel_0(u1_struct_0(X0),X0)
& m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f43646]) ).
fof(f47390,plain,
! [X0,X1,X2] :
( ( v1_funct_1(k2_waybel34(X0,X1,X2))
& v1_funct_2(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
& m2_relset_1(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1)) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f18894]) ).
fof(f47391,plain,
! [X0,X1,X2] :
( ( v1_funct_1(k2_waybel34(X0,X1,X2))
& v1_funct_2(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
& m2_relset_1(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1)) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0)) ),
inference(flattening,[],[f47390]) ).
fof(f47408,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( X3 = k2_waybel34(X0,X1,X2)
<=> v3_waybel_1(k1_waybel_1(X0,X1,X3,X2),X0,X1) )
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1)) )
| ~ v3_lattice3(X0)
| ~ v3_lattice3(X1)
| ~ v18_waybel_0(X2,X1,X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0)) )
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ l1_orders_2(X1) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f18907]) ).
fof(f47409,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( X3 = k2_waybel34(X0,X1,X2)
<=> v3_waybel_1(k1_waybel_1(X0,X1,X3,X2),X0,X1) )
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1)) )
| ~ v3_lattice3(X0)
| ~ v3_lattice3(X1)
| ~ v18_waybel_0(X2,X1,X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0)) )
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ l1_orders_2(X1) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f47408]) ).
fof(f47420,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( k7_yellow_2(u1_struct_0(X0),X1,k2_waybel34(X0,X1,X2),X3) != k1_yellow_0(X1,k5_pre_topc(X1,X0,X2,k6_waybel_0(X0,X3)))
& m1_subset_1(X3,u1_struct_0(X0)) )
& v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
& v18_waybel_0(X2,X1,X0)
& m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0)) )
& v2_orders_2(X1)
& v3_orders_2(X1)
& v4_orders_2(X1)
& v1_lattice3(X1)
& v2_lattice3(X1)
& v3_lattice3(X1)
& l1_orders_2(X1) )
& v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& v2_lattice3(X0)
& v3_lattice3(X0)
& l1_orders_2(X0) ),
inference(ennf_transformation,[],[f18914]) ).
fof(f47421,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( k7_yellow_2(u1_struct_0(X0),X1,k2_waybel34(X0,X1,X2),X3) != k1_yellow_0(X1,k5_pre_topc(X1,X0,X2,k6_waybel_0(X0,X3)))
& m1_subset_1(X3,u1_struct_0(X0)) )
& v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
& v18_waybel_0(X2,X1,X0)
& m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0)) )
& v2_orders_2(X1)
& v3_orders_2(X1)
& v4_orders_2(X1)
& v1_lattice3(X1)
& v2_lattice3(X1)
& v3_lattice3(X1)
& l1_orders_2(X1) )
& v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& v2_lattice3(X0)
& v3_lattice3(X0)
& l1_orders_2(X0) ),
inference(flattening,[],[f47420]) ).
fof(f50043,plain,
! [X0,X1,X2] :
( ( m2_relset_1(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1) )
& ( m1_relset_1(X2,X0,X1)
| ~ m2_relset_1(X2,X0,X1) ) ),
inference(nnf_transformation,[],[f1394]) ).
fof(f58579,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( r4_waybel_1(X0,X1,X2)
| ~ r1_yellow_0(X0,X2)
| k1_yellow_0(X0,X2) != X1
| ~ r2_hidden(k1_yellow_0(X0,X2),X2) )
& ( ( r1_yellow_0(X0,X2)
& X1 = k1_yellow_0(X0,X2)
& r2_hidden(k1_yellow_0(X0,X2),X2) )
| ~ r4_waybel_1(X0,X1,X2) ) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(nnf_transformation,[],[f40755]) ).
fof(f58580,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( r4_waybel_1(X0,X1,X2)
| ~ r1_yellow_0(X0,X2)
| k1_yellow_0(X0,X2) != X1
| ~ r2_hidden(k1_yellow_0(X0,X2),X2) )
& ( ( r1_yellow_0(X0,X2)
& X1 = k1_yellow_0(X0,X2)
& r2_hidden(k1_yellow_0(X0,X2),X2) )
| ~ r4_waybel_1(X0,X1,X2) ) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f58579]) ).
fof(f58608,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( ( v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1)
| ~ v5_orders_3(X3,X1,X0)
| ? [X4] :
( ~ r4_waybel_1(X1,k7_yellow_2(u1_struct_0(X0),X1,X2,X4),k5_pre_topc(X1,X0,X3,k6_waybel_0(X0,X4)))
& m1_subset_1(X4,u1_struct_0(X0)) ) )
& ( ( v5_orders_3(X3,X1,X0)
& ! [X4] :
( r4_waybel_1(X1,k7_yellow_2(u1_struct_0(X0),X1,X2,X4),k5_pre_topc(X1,X0,X3,k6_waybel_0(X0,X4)))
| ~ m1_subset_1(X4,u1_struct_0(X0)) ) )
| ~ v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1) ) )
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X0))
| ~ m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X0)) )
| ~ 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)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ l1_orders_2(X1) )
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(nnf_transformation,[],[f40775]) ).
fof(f58609,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( ( v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1)
| ~ v5_orders_3(X3,X1,X0)
| ? [X4] :
( ~ r4_waybel_1(X1,k7_yellow_2(u1_struct_0(X0),X1,X2,X4),k5_pre_topc(X1,X0,X3,k6_waybel_0(X0,X4)))
& m1_subset_1(X4,u1_struct_0(X0)) ) )
& ( ( v5_orders_3(X3,X1,X0)
& ! [X4] :
( r4_waybel_1(X1,k7_yellow_2(u1_struct_0(X0),X1,X2,X4),k5_pre_topc(X1,X0,X3,k6_waybel_0(X0,X4)))
| ~ m1_subset_1(X4,u1_struct_0(X0)) ) )
| ~ v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1) ) )
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X0))
| ~ m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X0)) )
| ~ 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)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ l1_orders_2(X1) )
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f58608]) ).
fof(f58610,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( ( v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1)
| ~ v5_orders_3(X3,X1,X0)
| ? [X4] :
( ~ r4_waybel_1(X1,k7_yellow_2(u1_struct_0(X0),X1,X2,X4),k5_pre_topc(X1,X0,X3,k6_waybel_0(X0,X4)))
& m1_subset_1(X4,u1_struct_0(X0)) ) )
& ( ( v5_orders_3(X3,X1,X0)
& ! [X5] :
( r4_waybel_1(X1,k7_yellow_2(u1_struct_0(X0),X1,X2,X5),k5_pre_topc(X1,X0,X3,k6_waybel_0(X0,X5)))
| ~ m1_subset_1(X5,u1_struct_0(X0)) ) )
| ~ v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1) ) )
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X0))
| ~ m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X0)) )
| ~ 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)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ l1_orders_2(X1) )
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(rectify,[],[f58609]) ).
fof(f58611,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( ( v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1)
| ~ v5_orders_3(X3,X1,X0)
| ( ~ r4_waybel_1(X1,k7_yellow_2(u1_struct_0(X0),X1,X2,sK6406(X0,X1,X2,X3)),k5_pre_topc(X1,X0,X3,k6_waybel_0(X0,sK6406(X0,X1,X2,X3))))
& m1_subset_1(sK6406(X0,X1,X2,X3),u1_struct_0(X0)) ) )
& ( ( v5_orders_3(X3,X1,X0)
& ! [X5] :
( r4_waybel_1(X1,k7_yellow_2(u1_struct_0(X0),X1,X2,X5),k5_pre_topc(X1,X0,X3,k6_waybel_0(X0,X5)))
| ~ m1_subset_1(X5,u1_struct_0(X0)) ) )
| ~ v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1) ) )
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X0))
| ~ m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X0)) )
| ~ 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)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ l1_orders_2(X1) )
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6406]),skolemize(X4,sK6406(X0,X1,X2,X3))],[f58610]) ).
fof(f62298,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( ( X3 = k2_waybel34(X0,X1,X2)
| ~ v3_waybel_1(k1_waybel_1(X0,X1,X3,X2),X0,X1) )
& ( v3_waybel_1(k1_waybel_1(X0,X1,X3,X2),X0,X1)
| k2_waybel34(X0,X1,X2) != X3 ) )
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1)) )
| ~ v3_lattice3(X0)
| ~ v3_lattice3(X1)
| ~ v18_waybel_0(X2,X1,X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0)) )
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ l1_orders_2(X1) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(nnf_transformation,[],[f47409]) ).
fof(f62303,plain,
( k7_yellow_2(u1_struct_0(sK8407),sK8408,k2_waybel34(sK8407,sK8408,sK8409),sK8410) != k1_yellow_0(sK8408,k5_pre_topc(sK8408,sK8407,sK8409,k6_waybel_0(sK8407,sK8410)))
& m1_subset_1(sK8410,u1_struct_0(sK8407))
& v1_funct_1(sK8409)
& v1_funct_2(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
& v18_waybel_0(sK8409,sK8408,sK8407)
& m2_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
& v2_orders_2(sK8408)
& v3_orders_2(sK8408)
& v4_orders_2(sK8408)
& v1_lattice3(sK8408)
& v2_lattice3(sK8408)
& v3_lattice3(sK8408)
& l1_orders_2(sK8408)
& v2_orders_2(sK8407)
& v3_orders_2(sK8407)
& v4_orders_2(sK8407)
& v1_lattice3(sK8407)
& v2_lattice3(sK8407)
& v3_lattice3(sK8407)
& l1_orders_2(sK8407) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8407,sK8408,sK8409,sK8410]),skolemize(X0,sK8407),skolemize(X1,sK8408),skolemize(X2,sK8409),skolemize(X3,sK8410)],[f47421]) ).
fof(f64337,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f50043]) ).
fof(f77300,plain,
! [X0] :
( ~ l1_orders_2(X0)
| l1_struct_0(X0) ),
inference(cnf_transformation,[],[f28555]) ).
fof(f84947,plain,
! [X0] :
( ~ v1_lattice3(X0)
| ~ v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f34373]) ).
fof(f95493,plain,
! [X2,X3,X0,X1] :
( m1_subset_1(k7_yellow_2(X0,X1,X2,X3),u1_struct_0(X1))
| v1_xboole_0(X0)
| v3_struct_0(X1)
| ~ l1_struct_0(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,X0,u1_struct_0(X1))
| ~ m1_relset_1(X2,X0,u1_struct_0(X1))
| ~ m1_subset_1(X3,X0) ),
inference(cnf_transformation,[],[f40674]) ).
fof(f95770,plain,
! [X2,X0,X1] :
( ~ r4_waybel_1(X0,X1,X2)
| k1_yellow_0(X0,X2) = X1
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f58580]) ).
fof(f95829,plain,
! [X2,X3,X0,X1,X5] :
( r4_waybel_1(X1,k7_yellow_2(u1_struct_0(X0),X1,X2,X5),k5_pre_topc(X1,X0,X3,k6_waybel_0(X0,X5)))
| ~ m1_subset_1(X5,u1_struct_0(X0))
| ~ v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X0))
| ~ m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X0))
| ~ 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)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ l1_orders_2(X1)
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f58611]) ).
fof(f100847,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f43647]) ).
fof(f109176,plain,
! [X2,X0,X1] :
( m2_relset_1(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f47391]) ).
fof(f109177,plain,
! [X2,X0,X1] :
( v1_funct_2(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f47391]) ).
fof(f109178,plain,
! [X2,X0,X1] :
( ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X2)
| v1_funct_1(k2_waybel34(X0,X1,X2))
| ~ m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f47391]) ).
fof(f109229,plain,
! [X2,X3,X0,X1] :
( v3_waybel_1(k1_waybel_1(X0,X1,X3,X2),X0,X1)
| k2_waybel34(X0,X1,X2) != X3
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v3_lattice3(X0)
| ~ v3_lattice3(X1)
| ~ v18_waybel_0(X2,X1,X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ l1_orders_2(X1)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f62298]) ).
fof(f109260,plain,
l1_orders_2(sK8407),
inference(cnf_transformation,[],[f62303]) ).
fof(f109261,plain,
v3_lattice3(sK8407),
inference(cnf_transformation,[],[f62303]) ).
fof(f109262,plain,
v2_lattice3(sK8407),
inference(cnf_transformation,[],[f62303]) ).
fof(f109263,plain,
v1_lattice3(sK8407),
inference(cnf_transformation,[],[f62303]) ).
fof(f109264,plain,
v4_orders_2(sK8407),
inference(cnf_transformation,[],[f62303]) ).
fof(f109265,plain,
v3_orders_2(sK8407),
inference(cnf_transformation,[],[f62303]) ).
fof(f109266,plain,
v2_orders_2(sK8407),
inference(cnf_transformation,[],[f62303]) ).
fof(f109267,plain,
l1_orders_2(sK8408),
inference(cnf_transformation,[],[f62303]) ).
fof(f109268,plain,
v3_lattice3(sK8408),
inference(cnf_transformation,[],[f62303]) ).
fof(f109269,plain,
v2_lattice3(sK8408),
inference(cnf_transformation,[],[f62303]) ).
fof(f109270,plain,
v1_lattice3(sK8408),
inference(cnf_transformation,[],[f62303]) ).
fof(f109271,plain,
v4_orders_2(sK8408),
inference(cnf_transformation,[],[f62303]) ).
fof(f109272,plain,
v3_orders_2(sK8408),
inference(cnf_transformation,[],[f62303]) ).
fof(f109273,plain,
v2_orders_2(sK8408),
inference(cnf_transformation,[],[f62303]) ).
fof(f109274,plain,
m2_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407)),
inference(cnf_transformation,[],[f62303]) ).
fof(f109275,plain,
v18_waybel_0(sK8409,sK8408,sK8407),
inference(cnf_transformation,[],[f62303]) ).
fof(f109276,plain,
v1_funct_2(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407)),
inference(cnf_transformation,[],[f62303]) ).
fof(f109277,plain,
v1_funct_1(sK8409),
inference(cnf_transformation,[],[f62303]) ).
fof(f109278,plain,
m1_subset_1(sK8410,u1_struct_0(sK8407)),
inference(cnf_transformation,[],[f62303]) ).
fof(f109279,plain,
k7_yellow_2(u1_struct_0(sK8407),sK8408,k2_waybel34(sK8407,sK8408,sK8409),sK8410) != k1_yellow_0(sK8408,k5_pre_topc(sK8408,sK8407,sK8409,k6_waybel_0(sK8407,sK8410))),
inference(cnf_transformation,[],[f62303]) ).
fof(f128420,plain,
! [X2,X0,X1] :
( v3_waybel_1(k1_waybel_1(X0,X1,k2_waybel34(X0,X1,X2),X2),X0,X1)
| ~ v1_funct_1(k2_waybel34(X0,X1,X2))
| ~ v1_funct_2(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
| ~ v3_lattice3(X0)
| ~ v3_lattice3(X1)
| ~ v18_waybel_0(X2,X1,X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ l1_orders_2(X1)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(equality_resolution,[],[f109229]) ).
fof(f128421,definition,
sF8411 = u1_struct_0(sK8407),
introduced(definition,[new_symbols(definition,[sF8411])],[function_definition]) ).
fof(f128422,plain,
u1_struct_0(sK8407) = sF8411,
inference(reorient_equations,[],[f128421]) ).
fof(f128423,definition,
sF8412 = k2_waybel34(sK8407,sK8408,sK8409),
introduced(definition,[new_symbols(definition,[sF8412])],[function_definition]) ).
fof(f128424,plain,
k2_waybel34(sK8407,sK8408,sK8409) = sF8412,
inference(reorient_equations,[],[f128423]) ).
fof(f128425,definition,
sF8413 = k7_yellow_2(sF8411,sK8408,sF8412,sK8410),
introduced(definition,[new_symbols(definition,[sF8413])],[function_definition]) ).
fof(f128426,plain,
k7_yellow_2(sF8411,sK8408,sF8412,sK8410) = sF8413,
inference(reorient_equations,[],[f128425]) ).
fof(f128427,definition,
sF8414 = k6_waybel_0(sK8407,sK8410),
introduced(definition,[new_symbols(definition,[sF8414])],[function_definition]) ).
fof(f128428,plain,
k6_waybel_0(sK8407,sK8410) = sF8414,
inference(reorient_equations,[],[f128427]) ).
fof(f128429,definition,
sF8415 = k5_pre_topc(sK8408,sK8407,sK8409,sF8414),
introduced(definition,[new_symbols(definition,[sF8415])],[function_definition]) ).
fof(f128430,plain,
k5_pre_topc(sK8408,sK8407,sK8409,sF8414) = sF8415,
inference(reorient_equations,[],[f128429]) ).
fof(f128431,definition,
sF8416 = k1_yellow_0(sK8408,sF8415),
introduced(definition,[new_symbols(definition,[sF8416])],[function_definition]) ).
fof(f128432,plain,
k1_yellow_0(sK8408,sF8415) = sF8416,
inference(reorient_equations,[],[f128431]) ).
fof(f128433,plain,
sF8413 != sF8416,
inference(definition_folding,[],[f109279,f128432,f128430,f128428,f128426,f128424,f128422]) ).
fof(f128434,plain,
m1_subset_1(sK8410,sF8411),
inference(definition_folding,[],[f109278,f128422]) ).
fof(f128435,definition,
sF8417 = u1_struct_0(sK8408),
introduced(definition,[new_symbols(definition,[sF8417])],[function_definition]) ).
fof(f128436,plain,
u1_struct_0(sK8408) = sF8417,
inference(reorient_equations,[],[f128435]) ).
fof(f128437,plain,
v1_funct_2(sK8409,sF8417,sF8411),
inference(definition_folding,[],[f109276,f128422,f128436]) ).
fof(f128438,plain,
m2_relset_1(sK8409,sF8417,sF8411),
inference(definition_folding,[],[f109274,f128422,f128436]) ).
fof(f147115,plain,
( ~ v3_struct_0(sK8408)
| ~ l1_orders_2(sK8408) ),
inference(resolution,[],[f84947,f109270]) ).
fof(f147116,plain,
( ~ v3_struct_0(sK8407)
| ~ l1_orders_2(sK8407) ),
inference(resolution,[],[f84947,f109263]) ).
fof(f147119,plain,
( m2_relset_1(sF8412,u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ v2_orders_2(sK8407)
| ~ v3_orders_2(sK8407)
| ~ v4_orders_2(sK8407)
| ~ v1_lattice3(sK8407)
| ~ v2_lattice3(sK8407)
| ~ l1_orders_2(sK8407)
| ~ v2_orders_2(sK8408)
| ~ v3_orders_2(sK8408)
| ~ v4_orders_2(sK8408)
| ~ v1_lattice3(sK8408)
| ~ v2_lattice3(sK8408)
| ~ l1_orders_2(sK8408)
| ~ v1_funct_1(sK8409)
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ m1_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407)) ),
inference(superposition,[],[f109176,f128424]) ).
fof(f147125,plain,
( v1_funct_2(sF8412,u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ v2_orders_2(sK8407)
| ~ v3_orders_2(sK8407)
| ~ v4_orders_2(sK8407)
| ~ v1_lattice3(sK8407)
| ~ v2_lattice3(sK8407)
| ~ l1_orders_2(sK8407)
| ~ v2_orders_2(sK8408)
| ~ v3_orders_2(sK8408)
| ~ v4_orders_2(sK8408)
| ~ v1_lattice3(sK8408)
| ~ v2_lattice3(sK8408)
| ~ l1_orders_2(sK8408)
| ~ v1_funct_1(sK8409)
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ m1_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407)) ),
inference(superposition,[],[f109177,f128424]) ).
fof(f147130,plain,
( m1_subset_1(sF8413,u1_struct_0(sK8408))
| v1_xboole_0(sF8411)
| v3_struct_0(sK8408)
| ~ l1_struct_0(sK8408)
| ~ v1_funct_1(sF8412)
| ~ v1_funct_2(sF8412,sF8411,u1_struct_0(sK8408))
| ~ m1_relset_1(sF8412,sF8411,u1_struct_0(sK8408))
| ~ m1_subset_1(sK8410,sF8411) ),
inference(superposition,[],[f95493,f128426]) ).
fof(f147140,definition,
( spl8418_2244
<=> l1_struct_0(sK8408) ),
introduced(definition,[new_symbols(definition,[spl8418_2244])],[avatar_definition]) ).
fof(f147141,plain,
( l1_struct_0(sK8408)
| ~ spl8418_2244 ),
inference(avatar_component_clause,[],[f147140]) ).
fof(f147142,plain,
( ~ l1_struct_0(sK8408)
| spl8418_2244 ),
inference(avatar_component_clause,[],[f147140]) ).
fof(f147167,definition,
( spl8418_2249
<=> m1_relset_1(sK8409,sF8417,sF8411) ),
introduced(definition,[new_symbols(definition,[spl8418_2249])],[avatar_definition]) ).
fof(f147168,plain,
( m1_relset_1(sK8409,sF8417,sF8411)
| ~ spl8418_2249 ),
inference(avatar_component_clause,[],[f147167]) ).
fof(f147169,plain,
( ~ m1_relset_1(sK8409,sF8417,sF8411)
| spl8418_2249 ),
inference(avatar_component_clause,[],[f147167]) ).
fof(f147171,plain,
l1_struct_0(sK8408),
inference(resolution,[],[f77300,f109267]) ).
fof(f147175,plain,
( $false
| spl8418_2244 ),
inference(forward_subsumption_resolution,[],[f147171,f147142]) ).
fof(f147176,plain,
spl8418_2244,
inference(avatar_contradiction_clause,[],[f147175]) ).
fof(f147180,plain,
! [X0,X1] :
( ~ v1_funct_2(X0,sF8417,u1_struct_0(X1))
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ l1_orders_2(X1)
| ~ v2_orders_2(sK8408)
| ~ v3_orders_2(sK8408)
| ~ v4_orders_2(sK8408)
| ~ v1_lattice3(sK8408)
| ~ v2_lattice3(sK8408)
| ~ l1_orders_2(sK8408)
| ~ v1_funct_1(X0)
| v1_funct_1(k2_waybel34(X1,sK8408,X0))
| ~ m1_relset_1(X0,sF8417,u1_struct_0(X1)) ),
inference(superposition,[],[f109178,f128436]) ).
fof(f147225,plain,
m1_relset_1(sK8409,sF8417,sF8411),
inference(resolution,[],[f64337,f128438]) ).
fof(f147227,plain,
( $false
| spl8418_2249 ),
inference(forward_subsumption_resolution,[],[f147225,f147169]) ).
fof(f147228,plain,
spl8418_2249,
inference(avatar_contradiction_clause,[],[f147227]) ).
fof(f147256,plain,
! [X2,X0,X1] :
( r4_waybel_1(X0,k7_yellow_2(u1_struct_0(sK8407),X0,X1,sK8410),k5_pre_topc(X0,sK8407,X2,sF8414))
| ~ m1_subset_1(sK8410,u1_struct_0(sK8407))
| ~ v3_waybel_1(k1_waybel_1(sK8407,X0,X1,X2),sK8407,X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(sK8407))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(sK8407))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK8407),u1_struct_0(X0))
| ~ m2_relset_1(X1,u1_struct_0(sK8407),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0)
| v3_struct_0(sK8407)
| ~ v2_orders_2(sK8407)
| ~ v3_orders_2(sK8407)
| ~ v4_orders_2(sK8407)
| ~ l1_orders_2(sK8407) ),
inference(superposition,[],[f95829,f128428]) ).
fof(f147275,plain,
( ~ v1_xboole_0(sF8411)
| v3_struct_0(sK8407)
| ~ v2_orders_2(sK8407)
| ~ v3_orders_2(sK8407)
| ~ v1_lattice3(sK8407)
| ~ l1_orders_2(sK8407) ),
inference(superposition,[],[f100847,f128422]) ).
fof(f147439,definition,
( spl8418_2251
<=> v1_funct_2(sF8412,sF8411,sF8417) ),
introduced(definition,[new_symbols(definition,[spl8418_2251])],[avatar_definition]) ).
fof(f147441,plain,
( v1_funct_2(sF8412,sF8411,sF8417)
| ~ spl8418_2251 ),
inference(avatar_component_clause,[],[f147439]) ).
fof(f147992,plain,
( m2_relset_1(sF8412,u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ v3_orders_2(sK8407)
| ~ v4_orders_2(sK8407)
| ~ v1_lattice3(sK8407)
| ~ v2_lattice3(sK8407)
| ~ l1_orders_2(sK8407)
| ~ v2_orders_2(sK8408)
| ~ v3_orders_2(sK8408)
| ~ v4_orders_2(sK8408)
| ~ v1_lattice3(sK8408)
| ~ v2_lattice3(sK8408)
| ~ l1_orders_2(sK8408)
| ~ v1_funct_1(sK8409)
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ m1_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407)) ),
inference(forward_subsumption_resolution,[],[f147119,f109266]) ).
fof(f147998,plain,
( v1_funct_2(sF8412,u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ v3_orders_2(sK8407)
| ~ v4_orders_2(sK8407)
| ~ v1_lattice3(sK8407)
| ~ v2_lattice3(sK8407)
| ~ l1_orders_2(sK8407)
| ~ v2_orders_2(sK8408)
| ~ v3_orders_2(sK8408)
| ~ v4_orders_2(sK8408)
| ~ v1_lattice3(sK8408)
| ~ v2_lattice3(sK8408)
| ~ l1_orders_2(sK8408)
| ~ v1_funct_1(sK8409)
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ m1_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407)) ),
inference(forward_subsumption_resolution,[],[f147125,f109266]) ).
fof(f148002,plain,
! [X0,X1] :
( ~ v1_funct_2(X0,sF8417,u1_struct_0(X1))
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ l1_orders_2(X1)
| ~ v3_orders_2(sK8408)
| ~ v4_orders_2(sK8408)
| ~ v1_lattice3(sK8408)
| ~ v2_lattice3(sK8408)
| ~ l1_orders_2(sK8408)
| ~ v1_funct_1(X0)
| v1_funct_1(k2_waybel34(X1,sK8408,X0))
| ~ m1_relset_1(X0,sF8417,u1_struct_0(X1)) ),
inference(forward_subsumption_resolution,[],[f147180,f109273]) ).
fof(f148564,plain,
( m2_relset_1(sF8412,u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ v4_orders_2(sK8407)
| ~ v1_lattice3(sK8407)
| ~ v2_lattice3(sK8407)
| ~ l1_orders_2(sK8407)
| ~ v2_orders_2(sK8408)
| ~ v3_orders_2(sK8408)
| ~ v4_orders_2(sK8408)
| ~ v1_lattice3(sK8408)
| ~ v2_lattice3(sK8408)
| ~ l1_orders_2(sK8408)
| ~ v1_funct_1(sK8409)
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ m1_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407)) ),
inference(forward_subsumption_resolution,[],[f147992,f109265]) ).
fof(f148570,plain,
( v1_funct_2(sF8412,u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ v4_orders_2(sK8407)
| ~ v1_lattice3(sK8407)
| ~ v2_lattice3(sK8407)
| ~ l1_orders_2(sK8407)
| ~ v2_orders_2(sK8408)
| ~ v3_orders_2(sK8408)
| ~ v4_orders_2(sK8408)
| ~ v1_lattice3(sK8408)
| ~ v2_lattice3(sK8408)
| ~ l1_orders_2(sK8408)
| ~ v1_funct_1(sK8409)
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ m1_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407)) ),
inference(forward_subsumption_resolution,[],[f147998,f109265]) ).
fof(f148574,plain,
! [X0,X1] :
( ~ v1_funct_2(X0,sF8417,u1_struct_0(X1))
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ l1_orders_2(X1)
| ~ v4_orders_2(sK8408)
| ~ v1_lattice3(sK8408)
| ~ v2_lattice3(sK8408)
| ~ l1_orders_2(sK8408)
| ~ v1_funct_1(X0)
| v1_funct_1(k2_waybel34(X1,sK8408,X0))
| ~ m1_relset_1(X0,sF8417,u1_struct_0(X1)) ),
inference(forward_subsumption_resolution,[],[f148002,f109272]) ).
fof(f148650,plain,
( m2_relset_1(sF8412,u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ v1_lattice3(sK8407)
| ~ v2_lattice3(sK8407)
| ~ l1_orders_2(sK8407)
| ~ v2_orders_2(sK8408)
| ~ v3_orders_2(sK8408)
| ~ v4_orders_2(sK8408)
| ~ v1_lattice3(sK8408)
| ~ v2_lattice3(sK8408)
| ~ l1_orders_2(sK8408)
| ~ v1_funct_1(sK8409)
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ m1_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407)) ),
inference(forward_subsumption_resolution,[],[f148564,f109264]) ).
fof(f148656,plain,
( v1_funct_2(sF8412,u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ v1_lattice3(sK8407)
| ~ v2_lattice3(sK8407)
| ~ l1_orders_2(sK8407)
| ~ v2_orders_2(sK8408)
| ~ v3_orders_2(sK8408)
| ~ v4_orders_2(sK8408)
| ~ v1_lattice3(sK8408)
| ~ v2_lattice3(sK8408)
| ~ l1_orders_2(sK8408)
| ~ v1_funct_1(sK8409)
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ m1_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407)) ),
inference(forward_subsumption_resolution,[],[f148570,f109264]) ).
fof(f148660,plain,
! [X0,X1] :
( ~ v1_funct_2(X0,sF8417,u1_struct_0(X1))
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ l1_orders_2(X1)
| ~ v1_lattice3(sK8408)
| ~ v2_lattice3(sK8408)
| ~ l1_orders_2(sK8408)
| ~ v1_funct_1(X0)
| v1_funct_1(k2_waybel34(X1,sK8408,X0))
| ~ m1_relset_1(X0,sF8417,u1_struct_0(X1)) ),
inference(forward_subsumption_resolution,[],[f148574,f109271]) ).
fof(f148701,plain,
( m2_relset_1(sF8412,u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ v2_lattice3(sK8407)
| ~ l1_orders_2(sK8407)
| ~ v2_orders_2(sK8408)
| ~ v3_orders_2(sK8408)
| ~ v4_orders_2(sK8408)
| ~ v1_lattice3(sK8408)
| ~ v2_lattice3(sK8408)
| ~ l1_orders_2(sK8408)
| ~ v1_funct_1(sK8409)
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ m1_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407)) ),
inference(forward_subsumption_resolution,[],[f148650,f109263]) ).
fof(f148707,plain,
( v1_funct_2(sF8412,u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ v2_lattice3(sK8407)
| ~ l1_orders_2(sK8407)
| ~ v2_orders_2(sK8408)
| ~ v3_orders_2(sK8408)
| ~ v4_orders_2(sK8408)
| ~ v1_lattice3(sK8408)
| ~ v2_lattice3(sK8408)
| ~ l1_orders_2(sK8408)
| ~ v1_funct_1(sK8409)
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ m1_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407)) ),
inference(forward_subsumption_resolution,[],[f148656,f109263]) ).
fof(f148711,plain,
! [X0,X1] :
( ~ v1_funct_2(X0,sF8417,u1_struct_0(X1))
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ l1_orders_2(X1)
| ~ v2_lattice3(sK8408)
| ~ l1_orders_2(sK8408)
| ~ v1_funct_1(X0)
| v1_funct_1(k2_waybel34(X1,sK8408,X0))
| ~ m1_relset_1(X0,sF8417,u1_struct_0(X1)) ),
inference(forward_subsumption_resolution,[],[f148660,f109270]) ).
fof(f148747,plain,
( m2_relset_1(sF8412,u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ l1_orders_2(sK8407)
| ~ v2_orders_2(sK8408)
| ~ v3_orders_2(sK8408)
| ~ v4_orders_2(sK8408)
| ~ v1_lattice3(sK8408)
| ~ v2_lattice3(sK8408)
| ~ l1_orders_2(sK8408)
| ~ v1_funct_1(sK8409)
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ m1_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407)) ),
inference(forward_subsumption_resolution,[],[f148701,f109262]) ).
fof(f148753,plain,
( v1_funct_2(sF8412,u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ l1_orders_2(sK8407)
| ~ v2_orders_2(sK8408)
| ~ v3_orders_2(sK8408)
| ~ v4_orders_2(sK8408)
| ~ v1_lattice3(sK8408)
| ~ v2_lattice3(sK8408)
| ~ l1_orders_2(sK8408)
| ~ v1_funct_1(sK8409)
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ m1_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407)) ),
inference(forward_subsumption_resolution,[],[f148707,f109262]) ).
fof(f148757,plain,
! [X0,X1] :
( ~ v1_funct_2(X0,sF8417,u1_struct_0(X1))
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ l1_orders_2(X1)
| ~ l1_orders_2(sK8408)
| ~ v1_funct_1(X0)
| v1_funct_1(k2_waybel34(X1,sK8408,X0))
| ~ m1_relset_1(X0,sF8417,u1_struct_0(X1)) ),
inference(forward_subsumption_resolution,[],[f148711,f109269]) ).
fof(f148788,plain,
( m2_relset_1(sF8412,u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ v2_orders_2(sK8408)
| ~ v3_orders_2(sK8408)
| ~ v4_orders_2(sK8408)
| ~ v1_lattice3(sK8408)
| ~ v2_lattice3(sK8408)
| ~ l1_orders_2(sK8408)
| ~ v1_funct_1(sK8409)
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ m1_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407)) ),
inference(forward_subsumption_resolution,[],[f148747,f109260]) ).
fof(f148794,plain,
( v1_funct_2(sF8412,u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ v2_orders_2(sK8408)
| ~ v3_orders_2(sK8408)
| ~ v4_orders_2(sK8408)
| ~ v1_lattice3(sK8408)
| ~ v2_lattice3(sK8408)
| ~ l1_orders_2(sK8408)
| ~ v1_funct_1(sK8409)
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ m1_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407)) ),
inference(forward_subsumption_resolution,[],[f148753,f109260]) ).
fof(f148798,plain,
! [X0,X1] :
( ~ v1_funct_2(X0,sF8417,u1_struct_0(X1))
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X0)
| v1_funct_1(k2_waybel34(X1,sK8408,X0))
| ~ m1_relset_1(X0,sF8417,u1_struct_0(X1)) ),
inference(forward_subsumption_resolution,[],[f148757,f109267]) ).
fof(f148822,plain,
( m2_relset_1(sF8412,u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ v3_orders_2(sK8408)
| ~ v4_orders_2(sK8408)
| ~ v1_lattice3(sK8408)
| ~ v2_lattice3(sK8408)
| ~ l1_orders_2(sK8408)
| ~ v1_funct_1(sK8409)
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ m1_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407)) ),
inference(forward_subsumption_resolution,[],[f148788,f109273]) ).
fof(f148824,plain,
( v1_funct_2(sF8412,u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ v3_orders_2(sK8408)
| ~ v4_orders_2(sK8408)
| ~ v1_lattice3(sK8408)
| ~ v2_lattice3(sK8408)
| ~ l1_orders_2(sK8408)
| ~ v1_funct_1(sK8409)
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ m1_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407)) ),
inference(forward_subsumption_resolution,[],[f148794,f109273]) ).
fof(f148843,plain,
( m2_relset_1(sF8412,u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ v4_orders_2(sK8408)
| ~ v1_lattice3(sK8408)
| ~ v2_lattice3(sK8408)
| ~ l1_orders_2(sK8408)
| ~ v1_funct_1(sK8409)
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ m1_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407)) ),
inference(forward_subsumption_resolution,[],[f148822,f109272]) ).
fof(f148845,plain,
( v1_funct_2(sF8412,u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ v4_orders_2(sK8408)
| ~ v1_lattice3(sK8408)
| ~ v2_lattice3(sK8408)
| ~ l1_orders_2(sK8408)
| ~ v1_funct_1(sK8409)
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ m1_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407)) ),
inference(forward_subsumption_resolution,[],[f148824,f109272]) ).
fof(f148852,plain,
( m2_relset_1(sF8412,u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ v1_lattice3(sK8408)
| ~ v2_lattice3(sK8408)
| ~ l1_orders_2(sK8408)
| ~ v1_funct_1(sK8409)
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ m1_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407)) ),
inference(forward_subsumption_resolution,[],[f148843,f109271]) ).
fof(f148854,plain,
( v1_funct_2(sF8412,u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ v1_lattice3(sK8408)
| ~ v2_lattice3(sK8408)
| ~ l1_orders_2(sK8408)
| ~ v1_funct_1(sK8409)
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ m1_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407)) ),
inference(forward_subsumption_resolution,[],[f148845,f109271]) ).
fof(f148859,plain,
( m2_relset_1(sF8412,u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ v2_lattice3(sK8408)
| ~ l1_orders_2(sK8408)
| ~ v1_funct_1(sK8409)
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ m1_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407)) ),
inference(forward_subsumption_resolution,[],[f148852,f109270]) ).
fof(f148861,plain,
( v1_funct_2(sF8412,u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ v2_lattice3(sK8408)
| ~ l1_orders_2(sK8408)
| ~ v1_funct_1(sK8409)
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ m1_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407)) ),
inference(forward_subsumption_resolution,[],[f148854,f109270]) ).
fof(f148865,plain,
( m2_relset_1(sF8412,u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ l1_orders_2(sK8408)
| ~ v1_funct_1(sK8409)
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ m1_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407)) ),
inference(forward_subsumption_resolution,[],[f148859,f109269]) ).
fof(f148867,plain,
( v1_funct_2(sF8412,u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ l1_orders_2(sK8408)
| ~ v1_funct_1(sK8409)
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ m1_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407)) ),
inference(forward_subsumption_resolution,[],[f148861,f109269]) ).
fof(f148871,plain,
( m2_relset_1(sF8412,u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ v1_funct_1(sK8409)
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ m1_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407)) ),
inference(forward_subsumption_resolution,[],[f148865,f109267]) ).
fof(f148873,plain,
( v1_funct_2(sF8412,u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ v1_funct_1(sK8409)
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ m1_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407)) ),
inference(forward_subsumption_resolution,[],[f148867,f109267]) ).
fof(f148877,plain,
( m2_relset_1(sF8412,u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ m1_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407)) ),
inference(forward_subsumption_resolution,[],[f148871,f109277]) ).
fof(f148879,plain,
( v1_funct_2(sF8412,u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ m1_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407)) ),
inference(forward_subsumption_resolution,[],[f148873,f109277]) ).
fof(f148883,plain,
( m2_relset_1(sF8412,u1_struct_0(sK8407),sF8417)
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ m1_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407)) ),
inference(forward_demodulation,[],[f148877,f128436]) ).
fof(f148885,plain,
( v1_funct_2(sF8412,u1_struct_0(sK8407),sF8417)
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ m1_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407)) ),
inference(forward_demodulation,[],[f148879,f128436]) ).
fof(f148889,plain,
( m2_relset_1(sF8412,sF8411,sF8417)
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ m1_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407)) ),
inference(forward_demodulation,[],[f148883,f128422]) ).
fof(f148891,plain,
( v1_funct_2(sF8412,sF8411,sF8417)
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ m1_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407)) ),
inference(forward_demodulation,[],[f148885,f128422]) ).
fof(f148895,plain,
( ~ v1_funct_2(sK8409,u1_struct_0(sK8408),sF8411)
| m2_relset_1(sF8412,sF8411,sF8417)
| ~ m1_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407)) ),
inference(forward_demodulation,[],[f148889,f128422]) ).
fof(f148897,plain,
( ~ v1_funct_2(sK8409,u1_struct_0(sK8408),sF8411)
| v1_funct_2(sF8412,sF8411,sF8417)
| ~ m1_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407)) ),
inference(forward_demodulation,[],[f148891,f128422]) ).
fof(f148901,plain,
( ~ v1_funct_2(sK8409,sF8417,sF8411)
| m2_relset_1(sF8412,sF8411,sF8417)
| ~ m1_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407)) ),
inference(forward_demodulation,[],[f148895,f128436]) ).
fof(f148903,plain,
( ~ v1_funct_2(sK8409,sF8417,sF8411)
| v1_funct_2(sF8412,sF8411,sF8417)
| ~ m1_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407)) ),
inference(forward_demodulation,[],[f148897,f128436]) ).
fof(f148907,plain,
( m2_relset_1(sF8412,sF8411,sF8417)
| ~ m1_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407)) ),
inference(forward_subsumption_resolution,[],[f148901,f128437]) ).
fof(f148909,plain,
( v1_funct_2(sF8412,sF8411,sF8417)
| ~ m1_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407)) ),
inference(forward_subsumption_resolution,[],[f148903,f128437]) ).
fof(f148913,plain,
( ~ m1_relset_1(sK8409,u1_struct_0(sK8408),sF8411)
| m2_relset_1(sF8412,sF8411,sF8417) ),
inference(forward_demodulation,[],[f148907,f128422]) ).
fof(f148915,plain,
( ~ m1_relset_1(sK8409,u1_struct_0(sK8408),sF8411)
| v1_funct_2(sF8412,sF8411,sF8417) ),
inference(forward_demodulation,[],[f148909,f128422]) ).
fof(f148919,plain,
( ~ m1_relset_1(sK8409,sF8417,sF8411)
| m2_relset_1(sF8412,sF8411,sF8417) ),
inference(forward_demodulation,[],[f148913,f128436]) ).
fof(f148921,plain,
( ~ m1_relset_1(sK8409,sF8417,sF8411)
| v1_funct_2(sF8412,sF8411,sF8417) ),
inference(forward_demodulation,[],[f148915,f128436]) ).
fof(f148925,plain,
( m2_relset_1(sF8412,sF8411,sF8417)
| ~ spl8418_2249 ),
inference(forward_subsumption_resolution,[],[f148919,f147168]) ).
fof(f148927,plain,
( v1_funct_2(sF8412,sF8411,sF8417)
| ~ spl8418_2249 ),
inference(forward_subsumption_resolution,[],[f148921,f147168]) ).
fof(f148932,plain,
( spl8418_2251
| ~ spl8418_2249 ),
inference(avatar_split_clause,[],[f148927,f147167,f147439]) ).
fof(f148941,definition,
( spl8418_2398
<=> v1_funct_1(sF8412) ),
introduced(definition,[new_symbols(definition,[spl8418_2398])],[avatar_definition]) ).
fof(f148942,plain,
( v1_funct_1(sF8412)
| ~ spl8418_2398 ),
inference(avatar_component_clause,[],[f148941]) ).
fof(f148943,plain,
( ~ v1_funct_1(sF8412)
| spl8418_2398 ),
inference(avatar_component_clause,[],[f148941]) ).
fof(f148957,definition,
( spl8418_2400
<=> v3_struct_0(sK8408) ),
introduced(definition,[new_symbols(definition,[spl8418_2400])],[avatar_definition]) ).
fof(f148958,plain,
( ~ v3_struct_0(sK8408)
| spl8418_2400 ),
inference(avatar_component_clause,[],[f148957]) ).
fof(f148965,definition,
( spl8418_2402
<=> v3_struct_0(sK8407) ),
introduced(definition,[new_symbols(definition,[spl8418_2402])],[avatar_definition]) ).
fof(f148973,plain,
( ~ v1_xboole_0(sF8411)
| ~ v2_orders_2(sK8407)
| ~ v3_orders_2(sK8407)
| ~ v1_lattice3(sK8407)
| ~ l1_orders_2(sK8407) ),
inference(forward_subsumption_resolution,[],[f147275,f84947]) ).
fof(f148992,definition,
( spl8418_2404
<=> v1_xboole_0(sF8411) ),
introduced(definition,[new_symbols(definition,[spl8418_2404])],[avatar_definition]) ).
fof(f148993,plain,
( ~ v1_xboole_0(sF8411)
| spl8418_2404 ),
inference(avatar_component_clause,[],[f148992]) ).
fof(f149113,plain,
~ v3_struct_0(sK8407),
inference(forward_subsumption_resolution,[],[f147116,f109260]) ).
fof(f149114,plain,
~ v3_struct_0(sK8408),
inference(forward_subsumption_resolution,[],[f147115,f109267]) ).
fof(f149121,plain,
! [X2,X0,X1] :
( r4_waybel_1(X0,k7_yellow_2(u1_struct_0(sK8407),X0,X1,sK8410),k5_pre_topc(X0,sK8407,X2,sF8414))
| ~ m1_subset_1(sK8410,u1_struct_0(sK8407))
| ~ v3_waybel_1(k1_waybel_1(sK8407,X0,X1,X2),sK8407,X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(sK8407))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(sK8407))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK8407),u1_struct_0(X0))
| ~ m2_relset_1(X1,u1_struct_0(sK8407),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0)
| v3_struct_0(sK8407)
| ~ v3_orders_2(sK8407)
| ~ v4_orders_2(sK8407)
| ~ l1_orders_2(sK8407) ),
inference(forward_subsumption_resolution,[],[f147256,f109266]) ).
fof(f149161,plain,
( ~ v1_xboole_0(sF8411)
| ~ v3_orders_2(sK8407)
| ~ v1_lattice3(sK8407)
| ~ l1_orders_2(sK8407) ),
inference(forward_subsumption_resolution,[],[f148973,f109266]) ).
fof(f149399,plain,
~ spl8418_2402,
inference(avatar_split_clause,[],[f149113,f148965]) ).
fof(f149400,plain,
~ spl8418_2400,
inference(avatar_split_clause,[],[f149114,f148957]) ).
fof(f149404,plain,
! [X2,X0,X1] :
( r4_waybel_1(X0,k7_yellow_2(u1_struct_0(sK8407),X0,X1,sK8410),k5_pre_topc(X0,sK8407,X2,sF8414))
| ~ m1_subset_1(sK8410,u1_struct_0(sK8407))
| ~ v3_waybel_1(k1_waybel_1(sK8407,X0,X1,X2),sK8407,X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(sK8407))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(sK8407))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK8407),u1_struct_0(X0))
| ~ m2_relset_1(X1,u1_struct_0(sK8407),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0)
| v3_struct_0(sK8407)
| ~ v4_orders_2(sK8407)
| ~ l1_orders_2(sK8407) ),
inference(forward_subsumption_resolution,[],[f149121,f109265]) ).
fof(f149427,plain,
( ~ v1_xboole_0(sF8411)
| ~ v1_lattice3(sK8407)
| ~ l1_orders_2(sK8407) ),
inference(forward_subsumption_resolution,[],[f149161,f109265]) ).
fof(f149537,plain,
! [X2,X0,X1] :
( r4_waybel_1(X0,k7_yellow_2(u1_struct_0(sK8407),X0,X1,sK8410),k5_pre_topc(X0,sK8407,X2,sF8414))
| ~ m1_subset_1(sK8410,u1_struct_0(sK8407))
| ~ v3_waybel_1(k1_waybel_1(sK8407,X0,X1,X2),sK8407,X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(sK8407))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(sK8407))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK8407),u1_struct_0(X0))
| ~ m2_relset_1(X1,u1_struct_0(sK8407),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0)
| v3_struct_0(sK8407)
| ~ l1_orders_2(sK8407) ),
inference(forward_subsumption_resolution,[],[f149404,f109264]) ).
fof(f149542,plain,
( ~ v1_xboole_0(sF8411)
| ~ l1_orders_2(sK8407) ),
inference(forward_subsumption_resolution,[],[f149427,f109263]) ).
fof(f149628,plain,
! [X2,X0,X1] :
( r4_waybel_1(X0,k7_yellow_2(u1_struct_0(sK8407),X0,X1,sK8410),k5_pre_topc(X0,sK8407,X2,sF8414))
| ~ m1_subset_1(sK8410,u1_struct_0(sK8407))
| ~ v3_waybel_1(k1_waybel_1(sK8407,X0,X1,X2),sK8407,X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(sK8407))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(sK8407))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK8407),u1_struct_0(X0))
| ~ m2_relset_1(X1,u1_struct_0(sK8407),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0)
| v3_struct_0(sK8407) ),
inference(forward_subsumption_resolution,[],[f149537,f109260]) ).
fof(f149632,plain,
~ v1_xboole_0(sF8411),
inference(forward_subsumption_resolution,[],[f149542,f109260]) ).
fof(f149802,plain,
! [X2,X0,X1] :
( r4_waybel_1(X0,k7_yellow_2(sF8411,X0,X1,sK8410),k5_pre_topc(X0,sK8407,X2,sF8414))
| ~ m1_subset_1(sK8410,u1_struct_0(sK8407))
| ~ v3_waybel_1(k1_waybel_1(sK8407,X0,X1,X2),sK8407,X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(sK8407))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(sK8407))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK8407),u1_struct_0(X0))
| ~ m2_relset_1(X1,u1_struct_0(sK8407),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0)
| v3_struct_0(sK8407) ),
inference(forward_demodulation,[],[f149628,f128422]) ).
fof(f149812,plain,
~ spl8418_2404,
inference(avatar_split_clause,[],[f149632,f148992]) ).
fof(f149871,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(sK8410,sF8411)
| r4_waybel_1(X0,k7_yellow_2(sF8411,X0,X1,sK8410),k5_pre_topc(X0,sK8407,X2,sF8414))
| ~ v3_waybel_1(k1_waybel_1(sK8407,X0,X1,X2),sK8407,X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(sK8407))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(sK8407))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK8407),u1_struct_0(X0))
| ~ m2_relset_1(X1,u1_struct_0(sK8407),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0)
| v3_struct_0(sK8407) ),
inference(forward_demodulation,[],[f149802,f128422]) ).
fof(f149887,plain,
! [X2,X0,X1] :
( r4_waybel_1(X0,k7_yellow_2(sF8411,X0,X1,sK8410),k5_pre_topc(X0,sK8407,X2,sF8414))
| ~ v3_waybel_1(k1_waybel_1(sK8407,X0,X1,X2),sK8407,X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(sK8407))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(sK8407))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK8407),u1_struct_0(X0))
| ~ m2_relset_1(X1,u1_struct_0(sK8407),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0)
| v3_struct_0(sK8407) ),
inference(forward_subsumption_resolution,[],[f149871,f128434]) ).
fof(f149893,plain,
! [X2,X0,X1] :
( ~ v1_funct_2(X2,u1_struct_0(X0),sF8411)
| r4_waybel_1(X0,k7_yellow_2(sF8411,X0,X1,sK8410),k5_pre_topc(X0,sK8407,X2,sF8414))
| ~ v3_waybel_1(k1_waybel_1(sK8407,X0,X1,X2),sK8407,X0)
| ~ v1_funct_1(X2)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(sK8407))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK8407),u1_struct_0(X0))
| ~ m2_relset_1(X1,u1_struct_0(sK8407),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0)
| v3_struct_0(sK8407) ),
inference(forward_demodulation,[],[f149887,f128422]) ).
fof(f149899,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,u1_struct_0(X0),sF8411)
| ~ v1_funct_2(X2,u1_struct_0(X0),sF8411)
| r4_waybel_1(X0,k7_yellow_2(sF8411,X0,X1,sK8410),k5_pre_topc(X0,sK8407,X2,sF8414))
| ~ v3_waybel_1(k1_waybel_1(sK8407,X0,X1,X2),sK8407,X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK8407),u1_struct_0(X0))
| ~ m2_relset_1(X1,u1_struct_0(sK8407),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0)
| v3_struct_0(sK8407) ),
inference(forward_demodulation,[],[f149893,f128422]) ).
fof(f149908,plain,
! [X2,X0,X1] :
( ~ v1_funct_2(X1,sF8411,u1_struct_0(X0))
| ~ m2_relset_1(X2,u1_struct_0(X0),sF8411)
| ~ v1_funct_2(X2,u1_struct_0(X0),sF8411)
| r4_waybel_1(X0,k7_yellow_2(sF8411,X0,X1,sK8410),k5_pre_topc(X0,sK8407,X2,sF8414))
| ~ v3_waybel_1(k1_waybel_1(sK8407,X0,X1,X2),sK8407,X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_1(X1)
| ~ m2_relset_1(X1,u1_struct_0(sK8407),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0)
| v3_struct_0(sK8407) ),
inference(forward_demodulation,[],[f149899,f128422]) ).
fof(f149913,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X1,sF8411,u1_struct_0(X0))
| ~ v1_funct_2(X1,sF8411,u1_struct_0(X0))
| ~ m2_relset_1(X2,u1_struct_0(X0),sF8411)
| ~ v1_funct_2(X2,u1_struct_0(X0),sF8411)
| r4_waybel_1(X0,k7_yellow_2(sF8411,X0,X1,sK8410),k5_pre_topc(X0,sK8407,X2,sF8414))
| ~ v3_waybel_1(k1_waybel_1(sK8407,X0,X1,X2),sK8407,X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_1(X1)
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0)
| v3_struct_0(sK8407) ),
inference(forward_demodulation,[],[f149908,f128422]) ).
fof(f149919,definition,
( spl8418_2525
<=> ! [X2,X0,X1] :
( ~ m2_relset_1(X1,sF8411,u1_struct_0(X0))
| ~ l1_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| v3_struct_0(X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_1(X2)
| ~ v3_waybel_1(k1_waybel_1(sK8407,X0,X1,X2),sK8407,X0)
| r4_waybel_1(X0,k7_yellow_2(sF8411,X0,X1,sK8410),k5_pre_topc(X0,sK8407,X2,sF8414))
| ~ v1_funct_2(X2,u1_struct_0(X0),sF8411)
| ~ m2_relset_1(X2,u1_struct_0(X0),sF8411)
| ~ v1_funct_2(X1,sF8411,u1_struct_0(X0)) ) ),
introduced(definition,[new_symbols(definition,[spl8418_2525])],[avatar_definition]) ).
fof(f149920,plain,
( ! [X2,X0,X1] :
( r4_waybel_1(X0,k7_yellow_2(sF8411,X0,X1,sK8410),k5_pre_topc(X0,sK8407,X2,sF8414))
| ~ l1_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| v3_struct_0(X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_1(X2)
| ~ v3_waybel_1(k1_waybel_1(sK8407,X0,X1,X2),sK8407,X0)
| ~ m2_relset_1(X1,sF8411,u1_struct_0(X0))
| ~ v1_funct_2(X2,u1_struct_0(X0),sF8411)
| ~ m2_relset_1(X2,u1_struct_0(X0),sF8411)
| ~ v1_funct_2(X1,sF8411,u1_struct_0(X0)) )
| ~ spl8418_2525 ),
inference(avatar_component_clause,[],[f149919]) ).
fof(f149921,plain,
( spl8418_2402
| spl8418_2525 ),
inference(avatar_split_clause,[],[f149913,f149919,f148965]) ).
fof(f149988,plain,
( ! [X0] :
( r4_waybel_1(sK8408,k7_yellow_2(sF8411,sK8408,X0,sK8410),sF8415)
| ~ l1_orders_2(sK8408)
| ~ v4_orders_2(sK8408)
| ~ v3_orders_2(sK8408)
| ~ v2_orders_2(sK8408)
| v3_struct_0(sK8408)
| ~ v1_funct_1(X0)
| ~ v1_funct_1(sK8409)
| ~ v3_waybel_1(k1_waybel_1(sK8407,sK8408,X0,sK8409),sK8407,sK8408)
| ~ m2_relset_1(X0,sF8411,u1_struct_0(sK8408))
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),sF8411)
| ~ m2_relset_1(sK8409,u1_struct_0(sK8408),sF8411)
| ~ v1_funct_2(X0,sF8411,u1_struct_0(sK8408)) )
| ~ spl8418_2525 ),
inference(superposition,[],[f149920,f128430]) ).
fof(f149992,plain,
( ! [X0] :
( r4_waybel_1(sK8408,k7_yellow_2(sF8411,sK8408,X0,sK8410),sF8415)
| ~ v4_orders_2(sK8408)
| ~ v3_orders_2(sK8408)
| ~ v2_orders_2(sK8408)
| v3_struct_0(sK8408)
| ~ v1_funct_1(X0)
| ~ v1_funct_1(sK8409)
| ~ v3_waybel_1(k1_waybel_1(sK8407,sK8408,X0,sK8409),sK8407,sK8408)
| ~ m2_relset_1(X0,sF8411,u1_struct_0(sK8408))
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),sF8411)
| ~ m2_relset_1(sK8409,u1_struct_0(sK8408),sF8411)
| ~ v1_funct_2(X0,sF8411,u1_struct_0(sK8408)) )
| ~ spl8418_2525 ),
inference(forward_subsumption_resolution,[],[f149988,f109267]) ).
fof(f149994,plain,
( ! [X0] :
( r4_waybel_1(sK8408,k7_yellow_2(sF8411,sK8408,X0,sK8410),sF8415)
| ~ v3_orders_2(sK8408)
| ~ v2_orders_2(sK8408)
| v3_struct_0(sK8408)
| ~ v1_funct_1(X0)
| ~ v1_funct_1(sK8409)
| ~ v3_waybel_1(k1_waybel_1(sK8407,sK8408,X0,sK8409),sK8407,sK8408)
| ~ m2_relset_1(X0,sF8411,u1_struct_0(sK8408))
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),sF8411)
| ~ m2_relset_1(sK8409,u1_struct_0(sK8408),sF8411)
| ~ v1_funct_2(X0,sF8411,u1_struct_0(sK8408)) )
| ~ spl8418_2525 ),
inference(forward_subsumption_resolution,[],[f149992,f109271]) ).
fof(f149996,plain,
( ! [X0] :
( r4_waybel_1(sK8408,k7_yellow_2(sF8411,sK8408,X0,sK8410),sF8415)
| ~ v2_orders_2(sK8408)
| v3_struct_0(sK8408)
| ~ v1_funct_1(X0)
| ~ v1_funct_1(sK8409)
| ~ v3_waybel_1(k1_waybel_1(sK8407,sK8408,X0,sK8409),sK8407,sK8408)
| ~ m2_relset_1(X0,sF8411,u1_struct_0(sK8408))
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),sF8411)
| ~ m2_relset_1(sK8409,u1_struct_0(sK8408),sF8411)
| ~ v1_funct_2(X0,sF8411,u1_struct_0(sK8408)) )
| ~ spl8418_2525 ),
inference(forward_subsumption_resolution,[],[f149994,f109272]) ).
fof(f149998,plain,
( ! [X0] :
( r4_waybel_1(sK8408,k7_yellow_2(sF8411,sK8408,X0,sK8410),sF8415)
| v3_struct_0(sK8408)
| ~ v1_funct_1(X0)
| ~ v1_funct_1(sK8409)
| ~ v3_waybel_1(k1_waybel_1(sK8407,sK8408,X0,sK8409),sK8407,sK8408)
| ~ m2_relset_1(X0,sF8411,u1_struct_0(sK8408))
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),sF8411)
| ~ m2_relset_1(sK8409,u1_struct_0(sK8408),sF8411)
| ~ v1_funct_2(X0,sF8411,u1_struct_0(sK8408)) )
| ~ spl8418_2525 ),
inference(forward_subsumption_resolution,[],[f149996,f109273]) ).
fof(f150000,plain,
( ! [X0] :
( r4_waybel_1(sK8408,k7_yellow_2(sF8411,sK8408,X0,sK8410),sF8415)
| ~ v1_funct_1(X0)
| ~ v1_funct_1(sK8409)
| ~ v3_waybel_1(k1_waybel_1(sK8407,sK8408,X0,sK8409),sK8407,sK8408)
| ~ m2_relset_1(X0,sF8411,u1_struct_0(sK8408))
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),sF8411)
| ~ m2_relset_1(sK8409,u1_struct_0(sK8408),sF8411)
| ~ v1_funct_2(X0,sF8411,u1_struct_0(sK8408)) )
| spl8418_2400
| ~ spl8418_2525 ),
inference(forward_subsumption_resolution,[],[f149998,f148958]) ).
fof(f150002,plain,
( ! [X0] :
( r4_waybel_1(sK8408,k7_yellow_2(sF8411,sK8408,X0,sK8410),sF8415)
| ~ v1_funct_1(X0)
| ~ v3_waybel_1(k1_waybel_1(sK8407,sK8408,X0,sK8409),sK8407,sK8408)
| ~ m2_relset_1(X0,sF8411,u1_struct_0(sK8408))
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),sF8411)
| ~ m2_relset_1(sK8409,u1_struct_0(sK8408),sF8411)
| ~ v1_funct_2(X0,sF8411,u1_struct_0(sK8408)) )
| spl8418_2400
| ~ spl8418_2525 ),
inference(forward_subsumption_resolution,[],[f150000,f109277]) ).
fof(f150004,plain,
( ! [X0] :
( ~ m2_relset_1(X0,sF8411,sF8417)
| r4_waybel_1(sK8408,k7_yellow_2(sF8411,sK8408,X0,sK8410),sF8415)
| ~ v1_funct_1(X0)
| ~ v3_waybel_1(k1_waybel_1(sK8407,sK8408,X0,sK8409),sK8407,sK8408)
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),sF8411)
| ~ m2_relset_1(sK8409,u1_struct_0(sK8408),sF8411)
| ~ v1_funct_2(X0,sF8411,u1_struct_0(sK8408)) )
| spl8418_2400
| ~ spl8418_2525 ),
inference(forward_demodulation,[],[f150002,f128436]) ).
fof(f150006,plain,
( ! [X0] :
( ~ v1_funct_2(sK8409,sF8417,sF8411)
| ~ m2_relset_1(X0,sF8411,sF8417)
| r4_waybel_1(sK8408,k7_yellow_2(sF8411,sK8408,X0,sK8410),sF8415)
| ~ v1_funct_1(X0)
| ~ v3_waybel_1(k1_waybel_1(sK8407,sK8408,X0,sK8409),sK8407,sK8408)
| ~ m2_relset_1(sK8409,u1_struct_0(sK8408),sF8411)
| ~ v1_funct_2(X0,sF8411,u1_struct_0(sK8408)) )
| spl8418_2400
| ~ spl8418_2525 ),
inference(forward_demodulation,[],[f150004,f128436]) ).
fof(f150008,plain,
( ! [X0] :
( ~ m2_relset_1(X0,sF8411,sF8417)
| r4_waybel_1(sK8408,k7_yellow_2(sF8411,sK8408,X0,sK8410),sF8415)
| ~ v1_funct_1(X0)
| ~ v3_waybel_1(k1_waybel_1(sK8407,sK8408,X0,sK8409),sK8407,sK8408)
| ~ m2_relset_1(sK8409,u1_struct_0(sK8408),sF8411)
| ~ v1_funct_2(X0,sF8411,u1_struct_0(sK8408)) )
| spl8418_2400
| ~ spl8418_2525 ),
inference(forward_subsumption_resolution,[],[f150006,f128437]) ).
fof(f150010,plain,
( ! [X0] :
( ~ m2_relset_1(sK8409,sF8417,sF8411)
| ~ m2_relset_1(X0,sF8411,sF8417)
| r4_waybel_1(sK8408,k7_yellow_2(sF8411,sK8408,X0,sK8410),sF8415)
| ~ v1_funct_1(X0)
| ~ v3_waybel_1(k1_waybel_1(sK8407,sK8408,X0,sK8409),sK8407,sK8408)
| ~ v1_funct_2(X0,sF8411,u1_struct_0(sK8408)) )
| spl8418_2400
| ~ spl8418_2525 ),
inference(forward_demodulation,[],[f150008,f128436]) ).
fof(f150012,plain,
( ! [X0] :
( ~ m2_relset_1(X0,sF8411,sF8417)
| r4_waybel_1(sK8408,k7_yellow_2(sF8411,sK8408,X0,sK8410),sF8415)
| ~ v1_funct_1(X0)
| ~ v3_waybel_1(k1_waybel_1(sK8407,sK8408,X0,sK8409),sK8407,sK8408)
| ~ v1_funct_2(X0,sF8411,u1_struct_0(sK8408)) )
| spl8418_2400
| ~ spl8418_2525 ),
inference(forward_subsumption_resolution,[],[f150010,f128438]) ).
fof(f150014,plain,
( ! [X0] :
( ~ v3_waybel_1(k1_waybel_1(sK8407,sK8408,X0,sK8409),sK8407,sK8408)
| ~ m2_relset_1(X0,sF8411,sF8417)
| r4_waybel_1(sK8408,k7_yellow_2(sF8411,sK8408,X0,sK8410),sF8415)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,sF8411,sF8417) )
| spl8418_2400
| ~ spl8418_2525 ),
inference(forward_demodulation,[],[f150012,f128436]) ).
fof(f150060,plain,
( m1_relset_1(sF8412,sF8411,sF8417)
| ~ spl8418_2249 ),
inference(resolution,[],[f148925,f64337]) ).
fof(f150100,plain,
( ~ m2_relset_1(k2_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
| r4_waybel_1(sK8408,k7_yellow_2(sF8411,sK8408,k2_waybel34(sK8407,sK8408,sK8409),sK8410),sF8415)
| ~ v1_funct_1(k2_waybel34(sK8407,sK8408,sK8409))
| ~ v1_funct_2(k2_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
| ~ v1_funct_1(k2_waybel34(sK8407,sK8408,sK8409))
| ~ v1_funct_2(k2_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ m2_relset_1(k2_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ v3_lattice3(sK8407)
| ~ v3_lattice3(sK8408)
| ~ v18_waybel_0(sK8409,sK8408,sK8407)
| ~ v1_funct_1(sK8409)
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ m2_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ v2_orders_2(sK8408)
| ~ v3_orders_2(sK8408)
| ~ v4_orders_2(sK8408)
| ~ v1_lattice3(sK8408)
| ~ v2_lattice3(sK8408)
| ~ l1_orders_2(sK8408)
| ~ v2_orders_2(sK8407)
| ~ v3_orders_2(sK8407)
| ~ v4_orders_2(sK8407)
| ~ v1_lattice3(sK8407)
| ~ v2_lattice3(sK8407)
| ~ l1_orders_2(sK8407)
| spl8418_2400
| ~ spl8418_2525 ),
inference(resolution,[],[f150014,f128420]) ).
fof(f150102,plain,
( ~ m2_relset_1(k2_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
| r4_waybel_1(sK8408,k7_yellow_2(sF8411,sK8408,k2_waybel34(sK8407,sK8408,sK8409),sK8410),sF8415)
| ~ v1_funct_1(k2_waybel34(sK8407,sK8408,sK8409))
| ~ v1_funct_2(k2_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
| ~ v1_funct_2(k2_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ m2_relset_1(k2_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ v3_lattice3(sK8407)
| ~ v3_lattice3(sK8408)
| ~ v18_waybel_0(sK8409,sK8408,sK8407)
| ~ v1_funct_1(sK8409)
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ m2_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ v2_orders_2(sK8408)
| ~ v3_orders_2(sK8408)
| ~ v4_orders_2(sK8408)
| ~ v1_lattice3(sK8408)
| ~ v2_lattice3(sK8408)
| ~ l1_orders_2(sK8408)
| ~ v2_orders_2(sK8407)
| ~ v3_orders_2(sK8407)
| ~ v4_orders_2(sK8407)
| ~ v1_lattice3(sK8407)
| ~ v2_lattice3(sK8407)
| ~ l1_orders_2(sK8407)
| spl8418_2400
| ~ spl8418_2525 ),
inference(duplicate_literal_removal,[],[f150100]) ).
fof(f150103,plain,
( ~ m2_relset_1(k2_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
| r4_waybel_1(sK8408,k7_yellow_2(sF8411,sK8408,k2_waybel34(sK8407,sK8408,sK8409),sK8410),sF8415)
| ~ v1_funct_1(k2_waybel34(sK8407,sK8408,sK8409))
| ~ v1_funct_2(k2_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
| ~ v1_funct_2(k2_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ m2_relset_1(k2_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ v3_lattice3(sK8408)
| ~ v18_waybel_0(sK8409,sK8408,sK8407)
| ~ v1_funct_1(sK8409)
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ m2_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ v2_orders_2(sK8408)
| ~ v3_orders_2(sK8408)
| ~ v4_orders_2(sK8408)
| ~ v1_lattice3(sK8408)
| ~ v2_lattice3(sK8408)
| ~ l1_orders_2(sK8408)
| ~ v2_orders_2(sK8407)
| ~ v3_orders_2(sK8407)
| ~ v4_orders_2(sK8407)
| ~ v1_lattice3(sK8407)
| ~ v2_lattice3(sK8407)
| ~ l1_orders_2(sK8407)
| spl8418_2400
| ~ spl8418_2525 ),
inference(forward_subsumption_resolution,[],[f150102,f109261]) ).
fof(f150104,plain,
( ~ m2_relset_1(k2_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
| r4_waybel_1(sK8408,k7_yellow_2(sF8411,sK8408,k2_waybel34(sK8407,sK8408,sK8409),sK8410),sF8415)
| ~ v1_funct_1(k2_waybel34(sK8407,sK8408,sK8409))
| ~ v1_funct_2(k2_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
| ~ v1_funct_2(k2_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ m2_relset_1(k2_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ v18_waybel_0(sK8409,sK8408,sK8407)
| ~ v1_funct_1(sK8409)
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ m2_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ v2_orders_2(sK8408)
| ~ v3_orders_2(sK8408)
| ~ v4_orders_2(sK8408)
| ~ v1_lattice3(sK8408)
| ~ v2_lattice3(sK8408)
| ~ l1_orders_2(sK8408)
| ~ v2_orders_2(sK8407)
| ~ v3_orders_2(sK8407)
| ~ v4_orders_2(sK8407)
| ~ v1_lattice3(sK8407)
| ~ v2_lattice3(sK8407)
| ~ l1_orders_2(sK8407)
| spl8418_2400
| ~ spl8418_2525 ),
inference(forward_subsumption_resolution,[],[f150103,f109268]) ).
fof(f150105,plain,
( ~ m2_relset_1(k2_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
| r4_waybel_1(sK8408,k7_yellow_2(sF8411,sK8408,k2_waybel34(sK8407,sK8408,sK8409),sK8410),sF8415)
| ~ v1_funct_1(k2_waybel34(sK8407,sK8408,sK8409))
| ~ v1_funct_2(k2_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
| ~ v1_funct_2(k2_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ m2_relset_1(k2_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ v1_funct_1(sK8409)
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ m2_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ v2_orders_2(sK8408)
| ~ v3_orders_2(sK8408)
| ~ v4_orders_2(sK8408)
| ~ v1_lattice3(sK8408)
| ~ v2_lattice3(sK8408)
| ~ l1_orders_2(sK8408)
| ~ v2_orders_2(sK8407)
| ~ v3_orders_2(sK8407)
| ~ v4_orders_2(sK8407)
| ~ v1_lattice3(sK8407)
| ~ v2_lattice3(sK8407)
| ~ l1_orders_2(sK8407)
| spl8418_2400
| ~ spl8418_2525 ),
inference(forward_subsumption_resolution,[],[f150104,f109275]) ).
fof(f150106,plain,
( ~ m2_relset_1(k2_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
| r4_waybel_1(sK8408,k7_yellow_2(sF8411,sK8408,k2_waybel34(sK8407,sK8408,sK8409),sK8410),sF8415)
| ~ v1_funct_1(k2_waybel34(sK8407,sK8408,sK8409))
| ~ v1_funct_2(k2_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
| ~ v1_funct_2(k2_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ m2_relset_1(k2_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ m2_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ v2_orders_2(sK8408)
| ~ v3_orders_2(sK8408)
| ~ v4_orders_2(sK8408)
| ~ v1_lattice3(sK8408)
| ~ v2_lattice3(sK8408)
| ~ l1_orders_2(sK8408)
| ~ v2_orders_2(sK8407)
| ~ v3_orders_2(sK8407)
| ~ v4_orders_2(sK8407)
| ~ v1_lattice3(sK8407)
| ~ v2_lattice3(sK8407)
| ~ l1_orders_2(sK8407)
| spl8418_2400
| ~ spl8418_2525 ),
inference(forward_subsumption_resolution,[],[f150105,f109277]) ).
fof(f150107,plain,
( ~ m2_relset_1(k2_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
| r4_waybel_1(sK8408,k7_yellow_2(sF8411,sK8408,k2_waybel34(sK8407,sK8408,sK8409),sK8410),sF8415)
| ~ v1_funct_1(k2_waybel34(sK8407,sK8408,sK8409))
| ~ v1_funct_2(k2_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
| ~ v1_funct_2(k2_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ m2_relset_1(k2_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ m2_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ v3_orders_2(sK8408)
| ~ v4_orders_2(sK8408)
| ~ v1_lattice3(sK8408)
| ~ v2_lattice3(sK8408)
| ~ l1_orders_2(sK8408)
| ~ v2_orders_2(sK8407)
| ~ v3_orders_2(sK8407)
| ~ v4_orders_2(sK8407)
| ~ v1_lattice3(sK8407)
| ~ v2_lattice3(sK8407)
| ~ l1_orders_2(sK8407)
| spl8418_2400
| ~ spl8418_2525 ),
inference(forward_subsumption_resolution,[],[f150106,f109273]) ).
fof(f150108,plain,
( ~ m2_relset_1(k2_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
| r4_waybel_1(sK8408,k7_yellow_2(sF8411,sK8408,k2_waybel34(sK8407,sK8408,sK8409),sK8410),sF8415)
| ~ v1_funct_1(k2_waybel34(sK8407,sK8408,sK8409))
| ~ v1_funct_2(k2_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
| ~ v1_funct_2(k2_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ m2_relset_1(k2_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ m2_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ v4_orders_2(sK8408)
| ~ v1_lattice3(sK8408)
| ~ v2_lattice3(sK8408)
| ~ l1_orders_2(sK8408)
| ~ v2_orders_2(sK8407)
| ~ v3_orders_2(sK8407)
| ~ v4_orders_2(sK8407)
| ~ v1_lattice3(sK8407)
| ~ v2_lattice3(sK8407)
| ~ l1_orders_2(sK8407)
| spl8418_2400
| ~ spl8418_2525 ),
inference(forward_subsumption_resolution,[],[f150107,f109272]) ).
fof(f150109,plain,
( ~ m2_relset_1(k2_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
| r4_waybel_1(sK8408,k7_yellow_2(sF8411,sK8408,k2_waybel34(sK8407,sK8408,sK8409),sK8410),sF8415)
| ~ v1_funct_1(k2_waybel34(sK8407,sK8408,sK8409))
| ~ v1_funct_2(k2_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
| ~ v1_funct_2(k2_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ m2_relset_1(k2_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ m2_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ v1_lattice3(sK8408)
| ~ v2_lattice3(sK8408)
| ~ l1_orders_2(sK8408)
| ~ v2_orders_2(sK8407)
| ~ v3_orders_2(sK8407)
| ~ v4_orders_2(sK8407)
| ~ v1_lattice3(sK8407)
| ~ v2_lattice3(sK8407)
| ~ l1_orders_2(sK8407)
| spl8418_2400
| ~ spl8418_2525 ),
inference(forward_subsumption_resolution,[],[f150108,f109271]) ).
fof(f150110,plain,
( ~ m2_relset_1(k2_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
| r4_waybel_1(sK8408,k7_yellow_2(sF8411,sK8408,k2_waybel34(sK8407,sK8408,sK8409),sK8410),sF8415)
| ~ v1_funct_1(k2_waybel34(sK8407,sK8408,sK8409))
| ~ v1_funct_2(k2_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
| ~ v1_funct_2(k2_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ m2_relset_1(k2_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ m2_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ v2_lattice3(sK8408)
| ~ l1_orders_2(sK8408)
| ~ v2_orders_2(sK8407)
| ~ v3_orders_2(sK8407)
| ~ v4_orders_2(sK8407)
| ~ v1_lattice3(sK8407)
| ~ v2_lattice3(sK8407)
| ~ l1_orders_2(sK8407)
| spl8418_2400
| ~ spl8418_2525 ),
inference(forward_subsumption_resolution,[],[f150109,f109270]) ).
fof(f150111,plain,
( ~ m2_relset_1(k2_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
| r4_waybel_1(sK8408,k7_yellow_2(sF8411,sK8408,k2_waybel34(sK8407,sK8408,sK8409),sK8410),sF8415)
| ~ v1_funct_1(k2_waybel34(sK8407,sK8408,sK8409))
| ~ v1_funct_2(k2_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
| ~ v1_funct_2(k2_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ m2_relset_1(k2_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ m2_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ l1_orders_2(sK8408)
| ~ v2_orders_2(sK8407)
| ~ v3_orders_2(sK8407)
| ~ v4_orders_2(sK8407)
| ~ v1_lattice3(sK8407)
| ~ v2_lattice3(sK8407)
| ~ l1_orders_2(sK8407)
| spl8418_2400
| ~ spl8418_2525 ),
inference(forward_subsumption_resolution,[],[f150110,f109269]) ).
fof(f150112,plain,
( ~ m2_relset_1(k2_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
| r4_waybel_1(sK8408,k7_yellow_2(sF8411,sK8408,k2_waybel34(sK8407,sK8408,sK8409),sK8410),sF8415)
| ~ v1_funct_1(k2_waybel34(sK8407,sK8408,sK8409))
| ~ v1_funct_2(k2_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
| ~ v1_funct_2(k2_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ m2_relset_1(k2_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ m2_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ v2_orders_2(sK8407)
| ~ v3_orders_2(sK8407)
| ~ v4_orders_2(sK8407)
| ~ v1_lattice3(sK8407)
| ~ v2_lattice3(sK8407)
| ~ l1_orders_2(sK8407)
| spl8418_2400
| ~ spl8418_2525 ),
inference(forward_subsumption_resolution,[],[f150111,f109267]) ).
fof(f150113,plain,
( ~ m2_relset_1(k2_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
| r4_waybel_1(sK8408,k7_yellow_2(sF8411,sK8408,k2_waybel34(sK8407,sK8408,sK8409),sK8410),sF8415)
| ~ v1_funct_1(k2_waybel34(sK8407,sK8408,sK8409))
| ~ v1_funct_2(k2_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
| ~ v1_funct_2(k2_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ m2_relset_1(k2_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ m2_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ v3_orders_2(sK8407)
| ~ v4_orders_2(sK8407)
| ~ v1_lattice3(sK8407)
| ~ v2_lattice3(sK8407)
| ~ l1_orders_2(sK8407)
| spl8418_2400
| ~ spl8418_2525 ),
inference(forward_subsumption_resolution,[],[f150112,f109266]) ).
fof(f150114,plain,
( ~ m2_relset_1(k2_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
| r4_waybel_1(sK8408,k7_yellow_2(sF8411,sK8408,k2_waybel34(sK8407,sK8408,sK8409),sK8410),sF8415)
| ~ v1_funct_1(k2_waybel34(sK8407,sK8408,sK8409))
| ~ v1_funct_2(k2_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
| ~ v1_funct_2(k2_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ m2_relset_1(k2_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ m2_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ v4_orders_2(sK8407)
| ~ v1_lattice3(sK8407)
| ~ v2_lattice3(sK8407)
| ~ l1_orders_2(sK8407)
| spl8418_2400
| ~ spl8418_2525 ),
inference(forward_subsumption_resolution,[],[f150113,f109265]) ).
fof(f150115,plain,
( ~ m2_relset_1(k2_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
| r4_waybel_1(sK8408,k7_yellow_2(sF8411,sK8408,k2_waybel34(sK8407,sK8408,sK8409),sK8410),sF8415)
| ~ v1_funct_1(k2_waybel34(sK8407,sK8408,sK8409))
| ~ v1_funct_2(k2_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
| ~ v1_funct_2(k2_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ m2_relset_1(k2_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ m2_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ v1_lattice3(sK8407)
| ~ v2_lattice3(sK8407)
| ~ l1_orders_2(sK8407)
| spl8418_2400
| ~ spl8418_2525 ),
inference(forward_subsumption_resolution,[],[f150114,f109264]) ).
fof(f150116,plain,
( ~ m2_relset_1(k2_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
| r4_waybel_1(sK8408,k7_yellow_2(sF8411,sK8408,k2_waybel34(sK8407,sK8408,sK8409),sK8410),sF8415)
| ~ v1_funct_1(k2_waybel34(sK8407,sK8408,sK8409))
| ~ v1_funct_2(k2_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
| ~ v1_funct_2(k2_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ m2_relset_1(k2_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ m2_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ v2_lattice3(sK8407)
| ~ l1_orders_2(sK8407)
| spl8418_2400
| ~ spl8418_2525 ),
inference(forward_subsumption_resolution,[],[f150115,f109263]) ).
fof(f150117,plain,
( ~ m2_relset_1(k2_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
| r4_waybel_1(sK8408,k7_yellow_2(sF8411,sK8408,k2_waybel34(sK8407,sK8408,sK8409),sK8410),sF8415)
| ~ v1_funct_1(k2_waybel34(sK8407,sK8408,sK8409))
| ~ v1_funct_2(k2_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
| ~ v1_funct_2(k2_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ m2_relset_1(k2_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ m2_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ l1_orders_2(sK8407)
| spl8418_2400
| ~ spl8418_2525 ),
inference(forward_subsumption_resolution,[],[f150116,f109262]) ).
fof(f150118,plain,
( ~ m2_relset_1(k2_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
| r4_waybel_1(sK8408,k7_yellow_2(sF8411,sK8408,k2_waybel34(sK8407,sK8408,sK8409),sK8410),sF8415)
| ~ v1_funct_1(k2_waybel34(sK8407,sK8408,sK8409))
| ~ v1_funct_2(k2_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
| ~ v1_funct_2(k2_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ m2_relset_1(k2_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ m2_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| spl8418_2400
| ~ spl8418_2525 ),
inference(forward_subsumption_resolution,[],[f150117,f109260]) ).
fof(f150119,plain,
( ~ m2_relset_1(sF8412,sF8411,sF8417)
| r4_waybel_1(sK8408,k7_yellow_2(sF8411,sK8408,k2_waybel34(sK8407,sK8408,sK8409),sK8410),sF8415)
| ~ v1_funct_1(k2_waybel34(sK8407,sK8408,sK8409))
| ~ v1_funct_2(k2_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
| ~ v1_funct_2(k2_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ m2_relset_1(k2_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ m2_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| spl8418_2400
| ~ spl8418_2525 ),
inference(forward_demodulation,[],[f150118,f128424]) ).
fof(f150120,plain,
( r4_waybel_1(sK8408,k7_yellow_2(sF8411,sK8408,k2_waybel34(sK8407,sK8408,sK8409),sK8410),sF8415)
| ~ v1_funct_1(k2_waybel34(sK8407,sK8408,sK8409))
| ~ v1_funct_2(k2_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
| ~ v1_funct_2(k2_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ m2_relset_1(k2_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ m2_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ spl8418_2249
| spl8418_2400
| ~ spl8418_2525 ),
inference(forward_subsumption_resolution,[],[f150119,f148925]) ).
fof(f150121,plain,
( r4_waybel_1(sK8408,k7_yellow_2(sF8411,sK8408,sF8412,sK8410),sF8415)
| ~ v1_funct_1(k2_waybel34(sK8407,sK8408,sK8409))
| ~ v1_funct_2(k2_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
| ~ v1_funct_2(k2_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ m2_relset_1(k2_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ m2_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ spl8418_2249
| spl8418_2400
| ~ spl8418_2525 ),
inference(forward_demodulation,[],[f150120,f128424]) ).
fof(f150122,plain,
( r4_waybel_1(sK8408,sF8413,sF8415)
| ~ v1_funct_1(k2_waybel34(sK8407,sK8408,sK8409))
| ~ v1_funct_2(k2_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
| ~ v1_funct_2(k2_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ m2_relset_1(k2_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ m2_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ spl8418_2249
| spl8418_2400
| ~ spl8418_2525 ),
inference(forward_demodulation,[],[f150121,f128426]) ).
fof(f150123,plain,
( ~ v1_funct_1(sF8412)
| r4_waybel_1(sK8408,sF8413,sF8415)
| ~ v1_funct_2(k2_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
| ~ v1_funct_2(k2_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ m2_relset_1(k2_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ m2_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ spl8418_2249
| spl8418_2400
| ~ spl8418_2525 ),
inference(forward_demodulation,[],[f150122,f128424]) ).
fof(f150271,plain,
! [X0] :
( ~ v1_funct_2(X0,sF8417,sF8411)
| ~ v2_orders_2(sK8407)
| ~ v3_orders_2(sK8407)
| ~ v4_orders_2(sK8407)
| ~ v1_lattice3(sK8407)
| ~ v2_lattice3(sK8407)
| ~ l1_orders_2(sK8407)
| ~ v1_funct_1(X0)
| v1_funct_1(k2_waybel34(sK8407,sK8408,X0))
| ~ m1_relset_1(X0,sF8417,sF8411) ),
inference(superposition,[],[f148798,f128422]) ).
fof(f150276,plain,
! [X0] :
( ~ v1_funct_2(X0,sF8417,sF8411)
| ~ v3_orders_2(sK8407)
| ~ v4_orders_2(sK8407)
| ~ v1_lattice3(sK8407)
| ~ v2_lattice3(sK8407)
| ~ l1_orders_2(sK8407)
| ~ v1_funct_1(X0)
| v1_funct_1(k2_waybel34(sK8407,sK8408,X0))
| ~ m1_relset_1(X0,sF8417,sF8411) ),
inference(forward_subsumption_resolution,[],[f150271,f109266]) ).
fof(f150278,plain,
! [X0] :
( ~ v1_funct_2(X0,sF8417,sF8411)
| ~ v4_orders_2(sK8407)
| ~ v1_lattice3(sK8407)
| ~ v2_lattice3(sK8407)
| ~ l1_orders_2(sK8407)
| ~ v1_funct_1(X0)
| v1_funct_1(k2_waybel34(sK8407,sK8408,X0))
| ~ m1_relset_1(X0,sF8417,sF8411) ),
inference(forward_subsumption_resolution,[],[f150276,f109265]) ).
fof(f150280,plain,
! [X0] :
( ~ v1_funct_2(X0,sF8417,sF8411)
| ~ v1_lattice3(sK8407)
| ~ v2_lattice3(sK8407)
| ~ l1_orders_2(sK8407)
| ~ v1_funct_1(X0)
| v1_funct_1(k2_waybel34(sK8407,sK8408,X0))
| ~ m1_relset_1(X0,sF8417,sF8411) ),
inference(forward_subsumption_resolution,[],[f150278,f109264]) ).
fof(f150282,plain,
! [X0] :
( ~ v1_funct_2(X0,sF8417,sF8411)
| ~ v2_lattice3(sK8407)
| ~ l1_orders_2(sK8407)
| ~ v1_funct_1(X0)
| v1_funct_1(k2_waybel34(sK8407,sK8408,X0))
| ~ m1_relset_1(X0,sF8417,sF8411) ),
inference(forward_subsumption_resolution,[],[f150280,f109263]) ).
fof(f150284,plain,
! [X0] :
( ~ v1_funct_2(X0,sF8417,sF8411)
| ~ l1_orders_2(sK8407)
| ~ v1_funct_1(X0)
| v1_funct_1(k2_waybel34(sK8407,sK8408,X0))
| ~ m1_relset_1(X0,sF8417,sF8411) ),
inference(forward_subsumption_resolution,[],[f150282,f109262]) ).
fof(f150286,plain,
! [X0] :
( v1_funct_1(k2_waybel34(sK8407,sK8408,X0))
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,sF8417,sF8411)
| ~ m1_relset_1(X0,sF8417,sF8411) ),
inference(forward_subsumption_resolution,[],[f150284,f109260]) ).
fof(f150287,plain,
( v1_funct_1(sF8412)
| ~ v1_funct_1(sK8409)
| ~ v1_funct_2(sK8409,sF8417,sF8411)
| ~ m1_relset_1(sK8409,sF8417,sF8411) ),
inference(superposition,[],[f150286,f128424]) ).
fof(f150288,plain,
( ~ v1_funct_1(sK8409)
| ~ v1_funct_2(sK8409,sF8417,sF8411)
| ~ m1_relset_1(sK8409,sF8417,sF8411)
| spl8418_2398 ),
inference(forward_subsumption_resolution,[],[f150287,f148943]) ).
fof(f150289,plain,
( ~ v1_funct_2(sK8409,sF8417,sF8411)
| ~ m1_relset_1(sK8409,sF8417,sF8411)
| spl8418_2398 ),
inference(forward_subsumption_resolution,[],[f150288,f109277]) ).
fof(f150290,plain,
( ~ m1_relset_1(sK8409,sF8417,sF8411)
| spl8418_2398 ),
inference(forward_subsumption_resolution,[],[f150289,f128437]) ).
fof(f150291,plain,
( $false
| ~ spl8418_2249
| spl8418_2398 ),
inference(forward_subsumption_resolution,[],[f150290,f147168]) ).
fof(f150292,plain,
( ~ spl8418_2249
| spl8418_2398 ),
inference(avatar_contradiction_clause,[],[f150291]) ).
fof(f150293,plain,
( m1_subset_1(sF8413,u1_struct_0(sK8408))
| v3_struct_0(sK8408)
| ~ l1_struct_0(sK8408)
| ~ v1_funct_1(sF8412)
| ~ v1_funct_2(sF8412,sF8411,u1_struct_0(sK8408))
| ~ m1_relset_1(sF8412,sF8411,u1_struct_0(sK8408))
| ~ m1_subset_1(sK8410,sF8411)
| spl8418_2404 ),
inference(forward_subsumption_resolution,[],[f147130,f148993]) ).
fof(f150297,plain,
( r4_waybel_1(sK8408,sF8413,sF8415)
| ~ v1_funct_2(k2_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
| ~ v1_funct_2(k2_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ m2_relset_1(k2_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ m2_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ spl8418_2249
| ~ spl8418_2398
| spl8418_2400
| ~ spl8418_2525 ),
inference(forward_subsumption_resolution,[],[f150123,f148942]) ).
fof(f150299,plain,
( m1_subset_1(sF8413,u1_struct_0(sK8408))
| ~ l1_struct_0(sK8408)
| ~ v1_funct_1(sF8412)
| ~ v1_funct_2(sF8412,sF8411,u1_struct_0(sK8408))
| ~ m1_relset_1(sF8412,sF8411,u1_struct_0(sK8408))
| ~ m1_subset_1(sK8410,sF8411)
| spl8418_2400
| spl8418_2404 ),
inference(forward_subsumption_resolution,[],[f150293,f148958]) ).
fof(f150303,plain,
( ~ v1_funct_2(sF8412,sF8411,sF8417)
| r4_waybel_1(sK8408,sF8413,sF8415)
| ~ v1_funct_2(k2_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ m2_relset_1(k2_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ m2_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ spl8418_2249
| ~ spl8418_2398
| spl8418_2400
| ~ spl8418_2525 ),
inference(forward_demodulation,[],[f150297,f128424]) ).
fof(f150305,plain,
( m1_subset_1(sF8413,u1_struct_0(sK8408))
| ~ v1_funct_1(sF8412)
| ~ v1_funct_2(sF8412,sF8411,u1_struct_0(sK8408))
| ~ m1_relset_1(sF8412,sF8411,u1_struct_0(sK8408))
| ~ m1_subset_1(sK8410,sF8411)
| ~ spl8418_2244
| spl8418_2400
| spl8418_2404 ),
inference(forward_subsumption_resolution,[],[f150299,f147141]) ).
fof(f150308,plain,
( r4_waybel_1(sK8408,sF8413,sF8415)
| ~ v1_funct_2(k2_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ m2_relset_1(k2_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ m2_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ spl8418_2249
| ~ spl8418_2251
| ~ spl8418_2398
| spl8418_2400
| ~ spl8418_2525 ),
inference(forward_subsumption_resolution,[],[f150303,f147441]) ).
fof(f150310,plain,
( m1_subset_1(sF8413,u1_struct_0(sK8408))
| ~ v1_funct_2(sF8412,sF8411,u1_struct_0(sK8408))
| ~ m1_relset_1(sF8412,sF8411,u1_struct_0(sK8408))
| ~ m1_subset_1(sK8410,sF8411)
| ~ spl8418_2244
| ~ spl8418_2398
| spl8418_2400
| spl8418_2404 ),
inference(forward_subsumption_resolution,[],[f150305,f148942]) ).
fof(f150312,plain,
( ~ v1_funct_2(k2_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8407),sF8417)
| r4_waybel_1(sK8408,sF8413,sF8415)
| ~ m2_relset_1(k2_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ m2_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ spl8418_2249
| ~ spl8418_2251
| ~ spl8418_2398
| spl8418_2400
| ~ spl8418_2525 ),
inference(forward_demodulation,[],[f150308,f128436]) ).
fof(f150314,plain,
( m1_subset_1(sF8413,u1_struct_0(sK8408))
| ~ v1_funct_2(sF8412,sF8411,u1_struct_0(sK8408))
| ~ m1_relset_1(sF8412,sF8411,u1_struct_0(sK8408))
| ~ spl8418_2244
| ~ spl8418_2398
| spl8418_2400
| spl8418_2404 ),
inference(forward_subsumption_resolution,[],[f150310,f128434]) ).
fof(f150316,plain,
( ~ v1_funct_2(k2_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
| r4_waybel_1(sK8408,sF8413,sF8415)
| ~ m2_relset_1(k2_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ m2_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ spl8418_2249
| ~ spl8418_2251
| ~ spl8418_2398
| spl8418_2400
| ~ spl8418_2525 ),
inference(forward_demodulation,[],[f150312,f128422]) ).
fof(f150318,plain,
( m1_subset_1(sF8413,sF8417)
| ~ v1_funct_2(sF8412,sF8411,u1_struct_0(sK8408))
| ~ m1_relset_1(sF8412,sF8411,u1_struct_0(sK8408))
| ~ spl8418_2244
| ~ spl8418_2398
| spl8418_2400
| spl8418_2404 ),
inference(forward_demodulation,[],[f150314,f128436]) ).
fof(f150320,plain,
( ~ v1_funct_2(sF8412,sF8411,sF8417)
| r4_waybel_1(sK8408,sF8413,sF8415)
| ~ m2_relset_1(k2_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ m2_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ spl8418_2249
| ~ spl8418_2251
| ~ spl8418_2398
| spl8418_2400
| ~ spl8418_2525 ),
inference(forward_demodulation,[],[f150316,f128424]) ).
fof(f150322,plain,
( ~ v1_funct_2(sF8412,sF8411,sF8417)
| m1_subset_1(sF8413,sF8417)
| ~ m1_relset_1(sF8412,sF8411,u1_struct_0(sK8408))
| ~ spl8418_2244
| ~ spl8418_2398
| spl8418_2400
| spl8418_2404 ),
inference(forward_demodulation,[],[f150318,f128436]) ).
fof(f150324,plain,
( r4_waybel_1(sK8408,sF8413,sF8415)
| ~ m2_relset_1(k2_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8407),u1_struct_0(sK8408))
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ m2_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ spl8418_2249
| ~ spl8418_2251
| ~ spl8418_2398
| spl8418_2400
| ~ spl8418_2525 ),
inference(forward_subsumption_resolution,[],[f150320,f147441]) ).
fof(f150326,plain,
( m1_subset_1(sF8413,sF8417)
| ~ m1_relset_1(sF8412,sF8411,u1_struct_0(sK8408))
| ~ spl8418_2244
| ~ spl8418_2251
| ~ spl8418_2398
| spl8418_2400
| spl8418_2404 ),
inference(forward_subsumption_resolution,[],[f150322,f147441]) ).
fof(f150328,plain,
( ~ m2_relset_1(k2_waybel34(sK8407,sK8408,sK8409),u1_struct_0(sK8407),sF8417)
| r4_waybel_1(sK8408,sF8413,sF8415)
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ m2_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ spl8418_2249
| ~ spl8418_2251
| ~ spl8418_2398
| spl8418_2400
| ~ spl8418_2525 ),
inference(forward_demodulation,[],[f150324,f128436]) ).
fof(f150330,plain,
( ~ m1_relset_1(sF8412,sF8411,sF8417)
| m1_subset_1(sF8413,sF8417)
| ~ spl8418_2244
| ~ spl8418_2251
| ~ spl8418_2398
| spl8418_2400
| spl8418_2404 ),
inference(forward_demodulation,[],[f150326,f128436]) ).
fof(f150332,plain,
( ~ m2_relset_1(k2_waybel34(sK8407,sK8408,sK8409),sF8411,sF8417)
| r4_waybel_1(sK8408,sF8413,sF8415)
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ m2_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ spl8418_2249
| ~ spl8418_2251
| ~ spl8418_2398
| spl8418_2400
| ~ spl8418_2525 ),
inference(forward_demodulation,[],[f150328,f128422]) ).
fof(f150334,plain,
( m1_subset_1(sF8413,sF8417)
| ~ spl8418_2244
| ~ spl8418_2249
| ~ spl8418_2251
| ~ spl8418_2398
| spl8418_2400
| spl8418_2404 ),
inference(forward_subsumption_resolution,[],[f150330,f150060]) ).
fof(f150336,plain,
( ~ m2_relset_1(sF8412,sF8411,sF8417)
| r4_waybel_1(sK8408,sF8413,sF8415)
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ m2_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ spl8418_2249
| ~ spl8418_2251
| ~ spl8418_2398
| spl8418_2400
| ~ spl8418_2525 ),
inference(forward_demodulation,[],[f150332,f128424]) ).
fof(f150339,plain,
( r4_waybel_1(sK8408,sF8413,sF8415)
| ~ v1_funct_2(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ m2_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ spl8418_2249
| ~ spl8418_2251
| ~ spl8418_2398
| spl8418_2400
| ~ spl8418_2525 ),
inference(forward_subsumption_resolution,[],[f150336,f148925]) ).
fof(f150342,plain,
( ~ v1_funct_2(sK8409,u1_struct_0(sK8408),sF8411)
| r4_waybel_1(sK8408,sF8413,sF8415)
| ~ m2_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ spl8418_2249
| ~ spl8418_2251
| ~ spl8418_2398
| spl8418_2400
| ~ spl8418_2525 ),
inference(forward_demodulation,[],[f150339,f128422]) ).
fof(f150344,plain,
( ~ v1_funct_2(sK8409,sF8417,sF8411)
| r4_waybel_1(sK8408,sF8413,sF8415)
| ~ m2_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ spl8418_2249
| ~ spl8418_2251
| ~ spl8418_2398
| spl8418_2400
| ~ spl8418_2525 ),
inference(forward_demodulation,[],[f150342,f128436]) ).
fof(f150346,plain,
( r4_waybel_1(sK8408,sF8413,sF8415)
| ~ m2_relset_1(sK8409,u1_struct_0(sK8408),u1_struct_0(sK8407))
| ~ spl8418_2249
| ~ spl8418_2251
| ~ spl8418_2398
| spl8418_2400
| ~ spl8418_2525 ),
inference(forward_subsumption_resolution,[],[f150344,f128437]) ).
fof(f150348,plain,
( ~ m2_relset_1(sK8409,u1_struct_0(sK8408),sF8411)
| r4_waybel_1(sK8408,sF8413,sF8415)
| ~ spl8418_2249
| ~ spl8418_2251
| ~ spl8418_2398
| spl8418_2400
| ~ spl8418_2525 ),
inference(forward_demodulation,[],[f150346,f128422]) ).
fof(f150349,plain,
( ~ m2_relset_1(sK8409,sF8417,sF8411)
| r4_waybel_1(sK8408,sF8413,sF8415)
| ~ spl8418_2249
| ~ spl8418_2251
| ~ spl8418_2398
| spl8418_2400
| ~ spl8418_2525 ),
inference(forward_demodulation,[],[f150348,f128436]) ).
fof(f150350,plain,
( r4_waybel_1(sK8408,sF8413,sF8415)
| ~ spl8418_2249
| ~ spl8418_2251
| ~ spl8418_2398
| spl8418_2400
| ~ spl8418_2525 ),
inference(forward_subsumption_resolution,[],[f150349,f128438]) ).
fof(f150357,plain,
( sF8413 = k1_yellow_0(sK8408,sF8415)
| ~ m1_subset_1(sF8413,u1_struct_0(sK8408))
| v3_struct_0(sK8408)
| ~ l1_orders_2(sK8408)
| ~ spl8418_2249
| ~ spl8418_2251
| ~ spl8418_2398
| spl8418_2400
| ~ spl8418_2525 ),
inference(resolution,[],[f150350,f95770]) ).
fof(f150358,plain,
( sF8413 = k1_yellow_0(sK8408,sF8415)
| ~ m1_subset_1(sF8413,u1_struct_0(sK8408))
| ~ l1_orders_2(sK8408)
| ~ spl8418_2249
| ~ spl8418_2251
| ~ spl8418_2398
| spl8418_2400
| ~ spl8418_2525 ),
inference(forward_subsumption_resolution,[],[f150357,f148958]) ).
fof(f150359,plain,
( sF8413 = k1_yellow_0(sK8408,sF8415)
| ~ m1_subset_1(sF8413,u1_struct_0(sK8408))
| ~ spl8418_2249
| ~ spl8418_2251
| ~ spl8418_2398
| spl8418_2400
| ~ spl8418_2525 ),
inference(forward_subsumption_resolution,[],[f150358,f109267]) ).
fof(f150360,plain,
( sF8413 = sF8416
| ~ m1_subset_1(sF8413,u1_struct_0(sK8408))
| ~ spl8418_2249
| ~ spl8418_2251
| ~ spl8418_2398
| spl8418_2400
| ~ spl8418_2525 ),
inference(forward_demodulation,[],[f150359,f128432]) ).
fof(f150361,plain,
( ~ m1_subset_1(sF8413,u1_struct_0(sK8408))
| ~ spl8418_2249
| ~ spl8418_2251
| ~ spl8418_2398
| spl8418_2400
| ~ spl8418_2525 ),
inference(forward_subsumption_resolution,[],[f150360,f128433]) ).
fof(f150362,plain,
( ~ m1_subset_1(sF8413,sF8417)
| ~ spl8418_2249
| ~ spl8418_2251
| ~ spl8418_2398
| spl8418_2400
| ~ spl8418_2525 ),
inference(forward_demodulation,[],[f150361,f128436]) ).
fof(f150363,plain,
( $false
| ~ spl8418_2244
| ~ spl8418_2249
| ~ spl8418_2251
| ~ spl8418_2398
| spl8418_2400
| spl8418_2404
| ~ spl8418_2525 ),
inference(forward_subsumption_resolution,[],[f150362,f150334]) ).
fof(f150364,plain,
( ~ spl8418_2244
| ~ spl8418_2249
| ~ spl8418_2251
| ~ spl8418_2398
| spl8418_2400
| spl8418_2404
| ~ spl8418_2525 ),
inference(avatar_contradiction_clause,[],[f150363]) ).
cnf(s1897,plain,
spl8418_2244,
inference(sat_conversion,[],[f147176]) ).
cnf(s1898,plain,
spl8418_2249,
inference(sat_conversion,[],[f147228]) ).
cnf(s2039,plain,
( ~ spl8418_2249
| spl8418_2251 ),
inference(sat_conversion,[],[f148932]) ).
cnf(s2090,plain,
~ spl8418_2402,
inference(sat_conversion,[],[f149399]) ).
cnf(s2091,plain,
~ spl8418_2400,
inference(sat_conversion,[],[f149400]) ).
cnf(s2154,plain,
~ spl8418_2404,
inference(sat_conversion,[],[f149812]) ).
cnf(s2173,plain,
( spl8418_2402
| spl8418_2525 ),
inference(sat_conversion,[],[f149921]) ).
cnf(s2185,plain,
( ~ spl8418_2249
| spl8418_2398 ),
inference(sat_conversion,[],[f150292]) ).
cnf(s2186,plain,
( ~ spl8418_2244
| ~ spl8418_2249
| ~ spl8418_2251
| ~ spl8418_2398
| spl8418_2400
| spl8418_2404
| ~ spl8418_2525 ),
inference(sat_conversion,[],[f150364]) ).
cnf(s2211,plain,
spl8418_2525,
inference(rat,[],[s2173,s2090]) ).
cnf(s2375,plain,
spl8418_2398,
inference(rat,[],[s2185,s1898]) ).
cnf(s2376,plain,
spl8418_2251,
inference(rat,[],[s2039,s1898]) ).
cnf(s2378,plain,
~ spl8418_2244,
inference(rat,[],[s2186,s2211,s2154,s2091,s2375,s1898,s2376]) ).
cnf(s2379,plain,
$false,
inference(rat,[],[s1897,s2378]) ).
fof(f150365,plain,
$false,
inference(avatar_sat_refutation,[],[s2379]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT353+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/0.38 % Computer : n003.cluster.edu
% 0.13/0.38 % Model : x86_64 x86_64
% 0.13/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.38 % Memory : 8046.5625MB
% 0.13/0.38 % OS : Linux 6.8.0-71-generic
% 0.13/0.38 % CPULimit : 300
% 0.13/0.38 % WCLimit : 300
% 0.13/0.38 % DateTime : Sun Sep 27 14:58:44 UTC 2026
% 0.13/0.38 % CPUTime :
% 0.13/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.05/0.42 Running first-order theorem proving
% 0.05/0.42 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 12.40/2.92 % (648210)Detected formulas, will run a generic FOF schedule.
% 12.40/2.92 % (648221)dis-21_1_sil=8000:lcm=predicate:random_seed=3380534945:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2995 on theBenchmark for (2995ds/129Mi)
% 12.40/2.92 % (648220)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3104918418:s2a=on:i=139:gtg=position_2995 on theBenchmark for (2995ds/139Mi)
% 12.40/2.92 % (648218)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=785714175:i=109:sd=1:ins=1:gsp=on:ss=axioms_2995 on theBenchmark for (2995ds/109Mi)
% 12.40/2.92 % (648219)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1368883192:i=119:av=off:ss=axioms_2995 on theBenchmark for (2995ds/119Mi)
% 12.40/2.92 % (648217)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=2577516474:i=141695:sd=1:nm=32:gsp=on:ss=included_2995 on theBenchmark for (2995ds/141695Mi)
% 12.40/2.92 % (648215)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=113460119:i=141193_2995 on theBenchmark for (2995ds/141193Mi)
% 12.40/2.92 % (648216)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=3267003374:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2995 on theBenchmark for (2995ds/134677Mi)
% 12.40/2.92 % (648221)Instruction limit reached!
% 12.40/2.92 % (648221)------------------------------
% 12.40/2.92 % (648221)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.40/2.92 % (648221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.40/2.92 % (648221)CaDiCaL version: 2.1.3
% 12.40/2.92 % (648221)Termination reason: Instruction limit
% 12.40/2.92 % (648221)Termination phase: SInE selection
% 12.40/2.92 % (648221)Time elapsed: 0.049 s
% 12.40/2.92 % (648221)Peak memory usage: 112 MB
% 12.40/2.92 % (648221)Instructions burned: 129 (million)
% 12.40/2.92 % (648220)Instruction limit reached!
% 12.40/2.92 % (648220)------------------------------
% 12.40/2.92 % (648220)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.40/2.92 % (648220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.40/2.92 % (648220)CaDiCaL version: 2.1.3
% 12.40/2.92 % (648220)Termination reason: Instruction limit
% 12.40/2.92 % (648220)Termination phase: Property scanning
% 12.40/2.92 % (648220)Time elapsed: 0.059 s
% 12.40/2.92 % (648220)Peak memory usage: 112 MB
% 12.40/2.92 % (648220)Instructions burned: 141 (million)
% 12.40/2.92 % (648218)Instruction limit reached!
% 12.40/2.92 % (648218)------------------------------
% 12.40/2.92 % (648218)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.40/2.92 % (648218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.40/2.92 % (648218)CaDiCaL version: 2.1.3
% 12.40/2.92 % (648218)Termination reason: Instruction limit
% 12.40/2.92 % (648218)Termination phase: SInE selection
% 12.40/2.92 % (648218)Time elapsed: 0.081 s
% 12.40/2.92 % (648218)Peak memory usage: 112 MB
% 12.40/2.92 % (648218)Instructions burned: 109 (million)
% 12.40/2.92 % (648219)Instruction limit reached!
% 12.40/2.92 % (648219)------------------------------
% 12.40/2.92 % (648219)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.40/2.92 % (648219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.40/2.92 % (648219)CaDiCaL version: 2.1.3
% 12.40/2.92 % (648219)Termination reason: Instruction limit
% 12.40/2.92 % (648219)Termination phase: Preprocessing 1
% 12.40/2.92 % (648219)Time elapsed: 0.096 s
% 12.40/2.92 % (648219)Peak memory usage: 113 MB
% 12.40/2.92 % (648219)Instructions burned: 119 (million)
% 12.40/2.92 % (648229)lrs+10_1_sil=8000:sp=occurrence:random_seed=2995746951:i=285:sd=3:ss=axioms:sgt=8_2993 on theBenchmark for (2993ds/285Mi)
% 12.40/2.92 % (648230)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1622318925:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2993 on theBenchmark for (2993ds/157Mi)
% 12.40/2.92 % (648231)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3142042695:i=325:sd=1:ss=axioms:sgt=32_2993 on theBenchmark for (2993ds/325Mi)
% 12.40/2.92 % (648232)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=726301117:s2a=on:i=248:s2at=1.23:gtg=position_2992 on theBenchmark for (2992ds/248Mi)
% 12.40/2.92 % (648229)Instruction limit reached!
% 12.40/2.92 % (648229)------------------------------
% 19.90/3.93 % (648229)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.90/3.93 % (648229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.90/3.93 % (648229)CaDiCaL version: 2.1.3
% 19.90/3.93 % (648229)Termination reason: Instruction limit
% 19.90/3.93 % (648229)Termination phase: Saturation
% 19.90/3.93 % (648229)Time elapsed: 0.117 s
% 19.90/3.93 % (648229)Peak memory usage: 119 MB
% 19.90/3.93 % (648229)Instructions burned: 288 (million)
% 19.90/3.93 % (648230)Instruction limit reached!
% 19.90/3.93 % (648230)------------------------------
% 19.90/3.93 % (648230)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.90/3.93 % (648230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.90/3.93 % (648230)CaDiCaL version: 2.1.3
% 19.90/3.93 % (648230)Termination reason: Instruction limit
% 19.90/3.93 % (648230)Termination phase: Property scanning
% 19.90/3.93 % (648230)Time elapsed: 0.069 s
% 19.90/3.93 % (648230)Peak memory usage: 112 MB
% 19.90/3.93 % (648230)Instructions burned: 159 (million)
% 19.90/3.93 % (648231)Refutation not found, incomplete strategy
% 19.90/3.93 % (648231)------------------------------
% 19.90/3.93 % (648231)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.90/3.93 % (648231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.90/3.93 % (648231)CaDiCaL version: 2.1.3
% 19.90/3.93 % (648231)Termination reason: Refutation not found, incomplete strategy
% 19.90/3.93 % (648231)Time elapsed: 0.115 s
% 19.90/3.93 % (648231)Peak memory usage: 117 MB
% 19.90/3.93 % (648231)Instructions burned: 129 (million)
% 19.90/3.93 % (648232)Instruction limit reached!
% 19.90/3.93 % (648232)------------------------------
% 19.90/3.93 % (648232)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.90/3.93 % (648232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.90/3.93 % (648232)CaDiCaL version: 2.1.3
% 19.90/3.93 % (648232)Termination reason: Instruction limit
% 19.90/3.93 % (648232)Termination phase: Property scanning
% 19.90/3.93 % (648232)Time elapsed: 0.105 s
% 19.90/3.93 % (648232)Peak memory usage: 112 MB
% 19.90/3.93 % (648232)Instructions burned: 248 (million)
% 19.90/3.93 % (648237)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1287832906:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2991 on theBenchmark for (2991ds/294Mi)
% 19.90/3.93 % (648238)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=566505388:i=2350_2991 on theBenchmark for (2991ds/2350Mi)
% 19.90/3.93 % (648239)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1033772290:cts=off:i=113:fsr=off:ss=included:sgt=4_2990 on theBenchmark for (2990ds/113Mi)
% 19.90/3.93 % (648237)Instruction limit reached!
% 19.90/3.93 % (648237)------------------------------
% 19.90/3.93 % (648237)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.90/3.93 % (648237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.90/3.93 % (648237)CaDiCaL version: 2.1.3
% 19.90/3.93 % (648237)Termination reason: Instruction limit
% 19.90/3.93 % (648237)Termination phase: Preprocessing 3
% 19.90/3.93 % (648237)Time elapsed: 0.130 s
% 19.90/3.93 % (648237)Peak memory usage: 119 MB
% 19.90/3.93 % (648237)Instructions burned: 297 (million)
% 19.90/3.93 % (648231)------------------------------
% 19.90/3.93 % (648231)------------------------------
% 19.90/3.93 % (648239)Instruction limit reached!
% 19.90/3.93 % (648239)------------------------------
% 19.90/3.93 % (648239)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.90/3.93 % (648239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.90/3.93 % (648239)CaDiCaL version: 2.1.3
% 19.90/3.93 % (648239)Termination reason: Instruction limit
% 19.90/3.93 % (648239)Termination phase: SInE selection
% 19.90/3.93 % (648239)Time elapsed: 0.089 s
% 19.90/3.93 % (648239)Peak memory usage: 112 MB
% 19.90/3.93 % (648239)Instructions burned: 113 (million)
% 19.90/3.93 % (648243)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1169856167:i=127:av=off:fsr=off:sup=off_2988 on theBenchmark for (2988ds/127Mi)
% 19.90/3.93 % (648243)Instruction limit reached!
% 19.90/3.93 % (648243)------------------------------
% 19.90/3.93 % (648243)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.90/3.93 % (648243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.90/3.93 % (648243)CaDiCaL version: 2.1.3
% 19.90/3.93 % (648243)Termination reason: Instruction limit
% 58.35/9.23 % (648243)Termination phase: Preprocessing 1
% 58.35/9.23 % (648243)Time elapsed: 0.053 s
% 58.35/9.23 % (648243)Peak memory usage: 112 MB
% 58.35/9.23 % (648243)Instructions burned: 127 (million)
% 58.35/9.23 % (648244)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2909816062:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2987 on theBenchmark for (2987ds/114Mi)
% 58.35/9.23 % (648245)lrs+10_1_sil=8000:sp=occurrence:random_seed=2253589167:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2987 on theBenchmark for (2987ds/907Mi)
% 58.35/9.23 % (648244)Instruction limit reached!
% 58.35/9.23 % (648244)------------------------------
% 58.35/9.23 % (648244)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.35/9.23 % (648244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.35/9.23 % (648244)CaDiCaL version: 2.1.3
% 58.35/9.23 % (648244)Termination reason: Instruction limit
% 58.35/9.23 % (648244)Termination phase: Property scanning
% 58.35/9.23 % (648244)Time elapsed: 0.051 s
% 58.35/9.23 % (648244)Peak memory usage: 112 MB
% 58.35/9.23 % (648244)Instructions burned: 116 (million)
% 58.35/9.23 % (648247)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3315021046:i=437:sd=1:aac=none:ss=included_2986 on theBenchmark for (2986ds/437Mi)
% 58.35/9.23 % (648247)Instruction limit reached!
% 58.35/9.23 % (648247)------------------------------
% 58.35/9.23 % (648247)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.35/9.23 % (648247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.35/9.23 % (648247)CaDiCaL version: 2.1.3
% 58.35/9.23 % (648247)Termination reason: Instruction limit
% 58.35/9.23 % (648247)Termination phase: Saturation
% 58.35/9.23 % (648247)Time elapsed: 0.138 s
% 58.35/9.23 % (648247)Peak memory usage: 118 MB
% 58.35/9.23 % (648247)Instructions burned: 441 (million)
% 58.35/9.23 % (648251)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3410914758:i=5202:ss=axioms:sgt=16_2985 on theBenchmark for (2985ds/5202Mi)
% 58.35/9.23 % (648252)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2539901523:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2984 on theBenchmark for (2984ds/134Mi)
% 58.35/9.23 % (648252)Instruction limit reached!
% 58.35/9.23 % (648252)------------------------------
% 58.35/9.23 % (648252)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.35/9.23 % (648252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.35/9.23 % (648252)CaDiCaL version: 2.1.3
% 58.35/9.23 % (648252)Termination reason: Instruction limit
% 58.35/9.23 % (648252)Termination phase: NewCNF
% 58.35/9.23 % (648252)Time elapsed: 0.066 s
% 58.35/9.23 % (648252)Peak memory usage: 115 MB
% 58.35/9.23 % (648252)Instructions burned: 134 (million)
% 58.35/9.23 % (648255)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=791906862:st=8:i=592:sd=3:ep=RST:ss=axioms_2982 on theBenchmark for (2982ds/592Mi)
% 58.35/9.23 % (648245)Instruction limit reached!
% 58.35/9.23 % (648245)------------------------------
% 58.35/9.23 % (648245)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.35/9.23 % (648245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.35/9.23 % (648245)CaDiCaL version: 2.1.3
% 58.35/9.23 % (648245)Termination reason: Instruction limit
% 58.35/9.23 % (648245)Termination phase: Saturation
% 58.35/9.23 % (648245)Time elapsed: 0.539 s
% 58.35/9.23 % (648245)Peak memory usage: 132 MB
% 58.35/9.23 % (648245)Instructions burned: 908 (million)
% 58.35/9.23 % (648257)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=4141300254:st=3:i=13193:sd=3:ss=axioms_2980 on theBenchmark for (2980ds/13193Mi)
% 58.35/9.23 % (648255)Instruction limit reached!
% 58.35/9.23 % (648255)------------------------------
% 58.35/9.23 % (648255)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.35/9.23 % (648255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.35/9.23 % (648255)CaDiCaL version: 2.1.3
% 58.35/9.23 % (648255)Termination reason: Instruction limit
% 58.35/9.23 % (648255)Termination phase: Preprocessing 3
% 58.35/9.23 % (648255)Time elapsed: 0.267 s
% 58.35/9.23 % (648255)Peak memory usage: 134 MB
% 58.35/9.23 % (648255)Instructions burned: 595 (million)
% 58.35/9.23 % (648259)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=2519702229:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2978 on theBenchmark for (2978ds/125Mi)
% 58.35/9.23 % (648238)Instruction limit reached!
% 79.17/12.14 % (648238)------------------------------
% 79.17/12.14 % (648238)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 79.17/12.14 % (648238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.17/12.14 % (648238)CaDiCaL version: 2.1.3
% 79.17/12.14 % (648238)Termination reason: Instruction limit
% 79.17/12.14 % (648238)Termination phase: Property scanning
% 79.17/12.14 % (648238)Time elapsed: 1.244 s
% 79.17/12.14 % (648238)Peak memory usage: 170 MB
% 79.17/12.14 % (648238)Instructions burned: 2352 (million)
% 79.17/12.14 % (648259)Instruction limit reached!
% 79.17/12.14 % (648259)------------------------------
% 79.17/12.14 % (648259)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 79.17/12.14 % (648259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.17/12.14 % (648259)CaDiCaL version: 2.1.3
% 79.17/12.14 % (648259)Termination reason: Instruction limit
% 79.17/12.14 % (648259)Termination phase: Property scanning
% 79.17/12.14 % (648259)Time elapsed: 0.029 s
% 79.17/12.14 % (648259)Peak memory usage: 112 MB
% 79.17/12.14 % (648259)Instructions burned: 125 (million)
% 79.17/12.14 % (648262)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1320756912:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2976 on theBenchmark for (2976ds/141Mi)
% 79.17/12.14 % (648261)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=602052994:i=134:gtgl=5:slsql=off:gtg=exists_sym_2976 on theBenchmark for (2976ds/134Mi)
% 79.17/12.14 % (648262)Refutation not found, incomplete strategy
% 79.17/12.14 % (648262)------------------------------
% 79.17/12.14 % (648262)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 79.17/12.14 % (648262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.17/12.14 % (648262)CaDiCaL version: 2.1.3
% 79.17/12.14 % (648262)Termination reason: Refutation not found, incomplete strategy
% 79.17/12.14 % (648262)Time elapsed: 0.065 s
% 79.17/12.14 % (648262)Peak memory usage: 117 MB
% 79.17/12.14 % (648262)Instructions burned: 133 (million)
% 79.17/12.14 % (648261)Instruction limit reached!
% 79.17/12.14 % (648261)------------------------------
% 79.17/12.14 % (648261)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 79.17/12.14 % (648261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.17/12.14 % (648261)CaDiCaL version: 2.1.3
% 79.17/12.14 % (648261)Termination reason: Instruction limit
% 79.17/12.14 % (648261)Termination phase: Property scanning
% 79.17/12.14 % (648261)Time elapsed: 0.060 s
% 79.17/12.14 % (648261)Peak memory usage: 112 MB
% 79.17/12.14 % (648261)Instructions burned: 136 (million)
% 79.17/12.14 % (648262)------------------------------
% 79.17/12.14 % (648262)------------------------------
% 79.17/12.14 % (648265)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2462021746:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2974 on theBenchmark for (2974ds/431Mi)
% 79.17/12.14 % (648266)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=3913871895:i=6060:aac=none:ins=25_2973 on theBenchmark for (2973ds/6060Mi)
% 79.17/12.14 % (648265)Instruction limit reached!
% 79.17/12.14 % (648265)------------------------------
% 79.17/12.14 % (648265)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 79.17/12.14 % (648265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.17/12.14 % (648265)CaDiCaL version: 2.1.3
% 79.17/12.14 % (648265)Termination reason: Instruction limit
% 79.17/12.14 % (648265)Termination phase: Saturation
% 79.17/12.14 % (648265)Time elapsed: 0.285 s
% 79.17/12.14 % (648265)Peak memory usage: 121 MB
% 79.17/12.14 % (648265)Instructions burned: 431 (million)
% 79.17/12.14 % (648269)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=1354804731:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2969 on theBenchmark for (2969ds/150Mi)
% 79.17/12.14 % (648269)Instruction limit reached!
% 79.17/12.14 % (648269)------------------------------
% 79.17/12.14 % (648269)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 79.17/12.14 % (648269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.17/12.14 % (648269)CaDiCaL version: 2.1.3
% 79.17/12.14 % (648269)Termination reason: Instruction limit
% 79.17/12.14 % (648269)Termination phase: Preprocessing 1
% 79.17/12.14 % (648269)Time elapsed: 0.125 s
% 107.85/16.21 % (648269)Peak memory usage: 113 MB
% 107.85/16.21 % (648269)Instructions burned: 151 (million)
% 107.85/16.21 % (648271)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2559100042:i=14155:bd=all_2966 on theBenchmark for (2966ds/14155Mi)
% 107.85/16.21 % (648251)Instruction limit reached!
% 107.85/16.21 % (648251)------------------------------
% 107.85/16.21 % (648251)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 107.85/16.21 % (648251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.85/16.21 % (648251)CaDiCaL version: 2.1.3
% 107.85/16.21 % (648251)Termination reason: Instruction limit
% 107.85/16.21 % (648251)Termination phase: Saturation
% 107.85/16.21 % (648251)Time elapsed: 3.063 s
% 107.85/16.21 % (648251)Peak memory usage: 252 MB
% 107.85/16.21 % (648251)Instructions burned: 5203 (million)
% 107.85/16.21 % (648273)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3849767248:i=667:av=off:fsr=off_2953 on theBenchmark for (2953ds/667Mi)
% 107.85/16.21 % (648273)Instruction limit reached!
% 107.85/16.21 % (648273)------------------------------
% 107.85/16.21 % (648273)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 107.85/16.21 % (648273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.85/16.21 % (648273)CaDiCaL version: 2.1.3
% 107.85/16.21 % (648273)Termination reason: Instruction limit
% 107.85/16.21 % (648273)Termination phase: NewCNF
% 107.85/16.21 % (648273)Time elapsed: 0.513 s
% 107.85/16.21 % (648273)Peak memory usage: 148 MB
% 107.85/16.21 % (648273)Instructions burned: 668 (million)
% 107.85/16.21 % (648275)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=3970583586:s2a=on:i=185:s2at=1.8:fdi=4_2946 on theBenchmark for (2946ds/185Mi)
% 107.85/16.21 % (648266)Instruction limit reached!
% 107.85/16.21 % (648266)------------------------------
% 107.85/16.21 % (648266)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 107.85/16.21 % (648266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.85/16.21 % (648266)CaDiCaL version: 2.1.3
% 107.85/16.21 % (648266)Termination reason: Instruction limit
% 107.85/16.21 % (648266)Termination phase: Saturation
% 107.85/16.21 % (648266)Time elapsed: 2.761 s
% 107.85/16.21 % (648266)Peak memory usage: 633 MB
% 107.85/16.21 % (648266)Instructions burned: 6065 (million)
% 107.85/16.21 % (648275)Instruction limit reached!
% 107.85/16.21 % (648275)------------------------------
% 107.85/16.21 % (648275)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 107.85/16.21 % (648275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.85/16.21 % (648275)CaDiCaL version: 2.1.3
% 107.85/16.21 % (648275)Termination reason: Instruction limit
% 107.85/16.21 % (648275)Termination phase: SInE selection
% 107.85/16.21 % (648275)Time elapsed: 0.155 s
% 107.85/16.21 % (648275)Peak memory usage: 112 MB
% 107.85/16.21 % (648275)Instructions burned: 185 (million)
% 107.85/16.21 % (648277)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2621476454:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2944 on theBenchmark for (2944ds/193Mi)
% 107.85/16.21 % (648277)Instruction limit reached!
% 107.85/16.21 % (648277)------------------------------
% 107.85/16.21 % (648277)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 107.85/16.21 % (648277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.85/16.21 % (648277)CaDiCaL version: 2.1.3
% 107.85/16.21 % (648277)Termination reason: Instruction limit
% 107.85/16.21 % (648277)Termination phase: SInE selection
% 107.85/16.21 % (648277)Time elapsed: 0.094 s
% 107.85/16.21 % (648277)Peak memory usage: 112 MB
% 107.85/16.21 % (648277)Instructions burned: 194 (million)
% 107.85/16.21 % (648278)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=2761044682:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2942 on theBenchmark for (2942ds/4850Mi)
% 107.85/16.21 % (648280)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=1823383421:i=12111:sd=1:ss=included_2941 on theBenchmark for (2941ds/12111Mi)
% 107.85/16.21 % (648278)Instruction limit reached!
% 107.85/16.21 % (648278)------------------------------
% 107.85/16.21 % (648278)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 107.85/16.21 % (648278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.85/16.21 % (648278)CaDiCaL version: 2.1.3
% 107.85/16.21 % (648278)Termination reason: Instruction limit
% 95.02/16.86 % (648278)Termination phase: Saturation
% 95.02/16.86 % (648278)Time elapsed: 2.740 s
% 95.02/16.86 % (648278)Peak memory usage: 213 MB
% 95.02/16.86 % (648278)Instructions burned: 4851 (million)
% 95.02/16.86 % (648283)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=334460283:i=319:kws=precedence:fsr=off_2913 on theBenchmark for (2913ds/319Mi)
% 95.02/16.86 % (648283)Instruction limit reached!
% 95.02/16.86 % (648283)------------------------------
% 95.02/16.86 % (648283)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.02/16.86 % (648283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.02/16.86 % (648283)CaDiCaL version: 2.1.3
% 95.02/16.86 % (648283)Termination reason: Instruction limit
% 95.02/16.86 % (648283)Termination phase: Naming
% 95.02/16.86 % (648283)Time elapsed: 0.249 s
% 95.02/16.86 % (648283)Peak memory usage: 135 MB
% 95.02/16.86 % (648283)Instructions burned: 319 (million)
% 95.02/16.86 % (648285)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=3256141992:i=2064:ep=RST_2909 on theBenchmark for (2909ds/2064Mi)
% 95.02/16.86 % (648257)Instruction limit reached!
% 95.02/16.86 % (648257)------------------------------
% 95.02/16.86 % (648257)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.02/16.86 % (648257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.02/16.86 % (648257)CaDiCaL version: 2.1.3
% 95.02/16.86 % (648257)Termination reason: Instruction limit
% 95.02/16.86 % (648257)Termination phase: Saturation
% 95.02/16.86 % (648257)Time elapsed: 7.393 s
% 95.02/16.86 % (648257)Peak memory usage: 292 MB
% 95.02/16.86 % (648257)Instructions burned: 13195 (million)
% 95.02/16.86 % (648287)dis-1011_128_sil=32000:random_seed=2519705570:i=3706:ep=RST:av=off_2904 on theBenchmark for (2904ds/3706Mi)
% 95.02/16.86 % (648280)Instruction limit reached!
% 95.02/16.86 % (648280)------------------------------
% 95.02/16.86 % (648280)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.02/16.86 % (648280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.02/16.86 % (648280)CaDiCaL version: 2.1.3
% 95.02/16.86 % (648280)Termination reason: Instruction limit
% 95.02/16.86 % (648280)Termination phase: Saturation
% 95.02/16.86 % (648280)Time elapsed: 4.293 s
% 95.02/16.86 % (648280)Peak memory usage: 256 MB
% 95.02/16.86 % (648280)Instructions burned: 12111 (million)
% 95.02/16.86 % (648285)Instruction limit reached!
% 95.02/16.86 % (648285)------------------------------
% 95.02/16.86 % (648285)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.02/16.86 % (648285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.02/16.86 % (648285)CaDiCaL version: 2.1.3
% 95.02/16.86 % (648285)Termination reason: Instruction limit
% 95.02/16.86 % (648285)Termination phase: Property scanning
% 95.02/16.86 % (648285)Time elapsed: 1.082 s
% 95.02/16.86 % (648285)Peak memory usage: 170 MB
% 95.02/16.86 % (648285)Instructions burned: 2066 (million)
% 95.02/16.86 % (648289)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=3110239490:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2897 on theBenchmark for (2897ds/757Mi)
% 95.02/16.86 % (648290)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=450422160:i=13913:ss=axioms:sgt=8_2896 on theBenchmark for (2896ds/13913Mi)
% 95.02/16.86 % (648289)Instruction limit reached!
% 95.02/16.86 % (648289)------------------------------
% 95.02/16.86 % (648289)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.02/16.86 % (648289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.02/16.86 % (648289)CaDiCaL version: 2.1.3
% 95.02/16.86 % (648289)Termination reason: Instruction limit
% 95.02/16.86 % (648289)Termination phase: Saturation
% 95.02/16.86 % (648289)Time elapsed: 0.290 s
% 95.02/16.86 % (648289)Peak memory usage: 129 MB
% 95.02/16.86 % (648289)Instructions burned: 760 (million)
% 95.02/16.86 % (648293)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=3953500382:i=9925:aac=none_2893 on theBenchmark for (2893ds/9925Mi)
% 95.02/16.86 % (648287)Instruction limit reached!
% 95.02/16.86 % (648287)------------------------------
% 95.02/16.86 % (648287)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.02/16.86 % (648287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.02/16.86 % (648287)CaDiCaL version: 2.1.3
% 95.02/16.86 % (648287)Termination reason: Instruction limit
% 95.02/16.86 % (648287)Termination phase: Saturation
% 95.02/16.86 % (648287)Time elapsed: 1.841 s
% 95.02/16.86 % (648287)Peak memory usage: 186 MB
% 95.02/16.86 % (648287)Instructions burned: 3708 (million)
% 95.02/16.86 % (648295)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=778596834:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2884 on theBenchmark for (2884ds/2479Mi)
% 95.02/16.86 % (648271)Instruction limit reached!
% 95.02/16.86 % (648271)------------------------------
% 95.02/16.86 % (648271)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.02/16.86 % (648271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.02/16.86 % (648271)CaDiCaL version: 2.1.3
% 95.02/16.86 % (648271)Termination reason: Instruction limit
% 95.02/16.86 % (648271)Termination phase: Saturation
% 95.02/16.86 % (648271)Time elapsed: 9.587 s
% 95.02/16.86 % (648271)Peak memory usage: 489 MB
% 95.02/16.86 % (648271)Instructions burned: 14156 (million)
% 95.02/16.86 % (648295)Instruction limit reached!
% 95.02/16.86 % (648295)------------------------------
% 95.02/16.86 % (648295)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.02/16.86 % (648295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.02/16.86 % (648295)CaDiCaL version: 2.1.3
% 95.02/16.86 % (648295)Termination reason: Instruction limit
% 95.02/16.86 % (648295)Termination phase: Saturation
% 95.02/16.86 % (648295)Time elapsed: 1.580 s
% 95.02/16.86 % (648295)Peak memory usage: 134 MB
% 95.02/16.86 % (648295)Instructions burned: 2479 (million)
% 95.02/16.86 % (648297)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=2699213721:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2868 on theBenchmark for (2868ds/440Mi)
% 95.02/16.86 % (648299)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=270961430:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2866 on theBenchmark for (2866ds/11145Mi)
% 95.02/16.86 % (648297)Instruction limit reached!
% 95.02/16.86 % (648297)------------------------------
% 95.02/16.86 % (648297)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.02/16.86 % (648297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.02/16.86 % (648297)CaDiCaL version: 2.1.3
% 95.02/16.86 % (648297)Termination reason: Instruction limit
% 95.02/16.86 % (648297)Termination phase: Property scanning
% 95.02/16.86 % (648297)Time elapsed: 0.197 s
% 95.02/16.86 % (648297)Peak memory usage: 112 MB
% 95.02/16.86 % (648297)Instructions burned: 442 (million)
% 95.02/16.86 % (648301)lrs+1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_frequency:lcm=reverse:urr=on:bsr=on:random_seed=3929594335:cts=off:i=3034:av=off:er=known:fsd=on_2864 on theBenchmark for (2864ds/3034Mi)
% 95.02/16.86 % (648293)Instruction limit reached!
% 95.02/16.86 % (648293)------------------------------
% 95.02/16.86 % (648293)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.02/16.86 % (648293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.02/16.86 % (648293)CaDiCaL version: 2.1.3
% 95.02/16.86 % (648293)Termination reason: Instruction limit
% 95.02/16.86 % (648293)Termination phase: Saturation
% 95.02/16.86 % (648293)Time elapsed: 4.419 s
% 95.02/16.86 % (648293)Peak memory usage: 497 MB
% 95.02/16.86 % (648293)Instructions burned: 9928 (million)
% 95.02/16.86 % (648303)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=769646308:st=2:s2a=on:i=524:s2at=2:ss=axioms_2847 on theBenchmark for (2847ds/524Mi)
% 95.02/16.86 % (648301)Instruction limit reached!
% 95.02/16.86 % (648301)------------------------------
% 95.02/16.86 % (648301)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.02/16.86 % (648301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.02/16.86 % (648301)CaDiCaL version: 2.1.3
% 95.02/16.86 % (648301)Termination reason: Instruction limit
% 95.02/16.86 % (648301)Termination phase: Saturation
% 95.02/16.86 % (648301)Time elapsed: 1.684 s
% 95.02/16.86 % (648301)Peak memory usage: 190 MB
% 95.02/16.86 % (648301)Instructions burned: 3035 (million)
% 95.02/16.86 % (648305)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=263581757:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2846 on theBenchmark for (2846ds/1016Mi)
% 95.02/16.86 % (648303)Instruction limit reached!
% 95.02/16.86 % (648303)------------------------------
% 95.02/16.86 % (648303)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.02/16.86 % (648303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.02/16.86 % (648303)CaDiCaL version: 2.1.3
% 95.02/16.86 % (648303)Termination reason: Instruction limit
% 95.02/16.86 % (648303)Termination phase: Preprocessing 1
% 95.02/16.86 % (648303)Time elapsed: 0.226 s
% 95.02/16.86 % (648303)Peak memory usage: 114 MB
% 95.02/16.86 % (648303)Instructions burned: 525 (million)
% 95.02/16.86 % (648307)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=30322766:i=14123:bd=preordered:ins=4_2844 on theBenchmark for (2844ds/14123Mi)
% 95.02/16.86 % (648215)First to succeed.
% 95.02/16.86 % (648215)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-648210"
% 95.02/16.86 % (648305)Instruction limit reached!
% 95.02/16.86 % (648305)------------------------------
% 95.02/16.86 % (648305)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.02/16.86 % (648305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.02/16.86 % (648305)CaDiCaL version: 2.1.3
% 95.02/16.86 % (648305)Termination reason: Instruction limit
% 95.02/16.86 % (648305)Termination phase: Saturation
% 95.02/16.86 % (648305)Time elapsed: 0.611 s
% 95.02/16.86 % (648305)Peak memory usage: 133 MB
% 95.02/16.86 % (648305)Instructions burned: 1018 (million)
% 95.02/16.86 % (648215)Refutation found. Thanks to Tanya!
% 95.02/16.86 % SZS status Theorem for theBenchmark
% 95.02/16.86 % SZS output start Proof for theBenchmark
% See solution above
% 112.64/16.96 % (648215)------------------------------
% 112.64/16.96 % (648215)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.64/16.96 % (648215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.64/16.96 % (648215)CaDiCaL version: 2.1.3
% 112.64/16.96 % (648215)Termination reason: Refutation
% 112.64/16.96 % (648215)Time elapsed: 15.256 s
% 112.64/16.96 % (648215)Peak memory usage: 763 MB
% 112.64/16.96 % (648215)Instructions burned: 24848 (million)
% 112.64/16.96 % (648215)------------------------------
% 112.64/16.96 % (648215)------------------------------
% 112.64/16.96 % (648210)Success in time 16.237 s
% 112.64/16.96 % Vampire exiting
%------------------------------------------------------------------------------