%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT353+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:47:13 AM UTC 2026
% Result : Theorem 4.36s 1.57s
% Output : Refutation 5.59s
% Verified :
% SZS Type : Refutation
% Derivation depth : 60
% Number of leaves : 26
% Syntax : Number of formulae : 293 ( 61 unt; 16 def)
% Number of atoms : 2217 ( 39 equ)
% Maximal formula atoms : 27 ( 7 avg)
% Number of connectives : 3519 (1595 ~;1707 |; 172 &)
% ( 19 <=>; 26 =>; 0 <=; 0 <~>)
% Maximal formula depth : 29 ( 9 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 32 ( 30 usr; 10 prp; 0-3 aty)
% Number of functors : 19 ( 19 usr; 11 con; 0-4 aty)
% Number of variables : 230 ( 0 sgn 219 !; 11 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [X0] :
( ( v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& v2_lattice3(X0)
& v3_lattice3(X0)
& 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(f2,negated_conjecture,
~ ! [X0] :
( ( v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& v2_lattice3(X0)
& v3_lattice3(X0)
& 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)],[f1]) ).
fof(f33,axiom,
! [X0] :
( l1_orders_2(X0)
=> ( v2_lattice3(X0)
=> ~ v3_struct_0(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc2_lattice3) ).
fof(f45,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(f47,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(f57,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(f63,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(f64,axiom,
! [X0] :
( l1_orders_2(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l1_orders_2) ).
fof(f89,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_struct_0(X0) )
=> ~ v1_xboole_0(u1_struct_0(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_struct_0) ).
fof(f122,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(f124,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(f157,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,[],[f2]) ).
fof(f158,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,[],[f157]) ).
fof(f202,plain,
! [X0] :
( ~ v3_struct_0(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f33]) ).
fof(f203,plain,
! [X0] :
( ~ v3_struct_0(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f202]) ).
fof(f221,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,[],[f45]) ).
fof(f222,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,[],[f221]) ).
fof(f223,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,[],[f47]) ).
fof(f224,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,[],[f223]) ).
fof(f228,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,[],[f57]) ).
fof(f229,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,[],[f228]) ).
fof(f236,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,[],[f63]) ).
fof(f237,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,[],[f236]) ).
fof(f238,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f64]) ).
fof(f256,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f89]) ).
fof(f257,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(flattening,[],[f256]) ).
fof(f296,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,[],[f124]) ).
fof(f297,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,[],[f296]) ).
fof(f312,plain,
( k7_yellow_2(u1_struct_0(sK2),sK3,k2_waybel34(sK2,sK3,sK4),sK5) != k1_yellow_0(sK3,k5_pre_topc(sK3,sK2,sK4,k6_waybel_0(sK2,sK5)))
& m1_subset_1(sK5,u1_struct_0(sK2))
& v1_funct_1(sK4)
& v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
& v18_waybel_0(sK4,sK3,sK2)
& m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
& v2_orders_2(sK3)
& v3_orders_2(sK3)
& v4_orders_2(sK3)
& v1_lattice3(sK3)
& v2_lattice3(sK3)
& v3_lattice3(sK3)
& l1_orders_2(sK3)
& v2_orders_2(sK2)
& v3_orders_2(sK2)
& v4_orders_2(sK2)
& v1_lattice3(sK2)
& v2_lattice3(sK2)
& v3_lattice3(sK2)
& l1_orders_2(sK2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3,sK4,sK5]),skolemize(X0,sK2),skolemize(X1,sK3),skolemize(X2,sK4),skolemize(X3,sK5)],[f158]) ).
fof(f315,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,[],[f222]) ).
fof(f316,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,[],[f224]) ).
fof(f317,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,[],[f316]) ).
fof(f341,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,[],[f122]) ).
fof(f342,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,[],[f297]) ).
fof(f343,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,[],[f342]) ).
fof(f344,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,[],[f343]) ).
fof(f345,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,sK29(X0,X1,X2,X3)),k5_pre_topc(X1,X0,X3,k6_waybel_0(X0,sK29(X0,X1,X2,X3))))
& m1_subset_1(sK29(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,[sK29]),skolemize(X4,sK29(X0,X1,X2,X3))],[f344]) ).
fof(f346,plain,
l1_orders_2(sK2),
inference(cnf_transformation,[],[f312]) ).
fof(f347,plain,
v3_lattice3(sK2),
inference(cnf_transformation,[],[f312]) ).
fof(f348,plain,
v2_lattice3(sK2),
inference(cnf_transformation,[],[f312]) ).
fof(f349,plain,
v1_lattice3(sK2),
inference(cnf_transformation,[],[f312]) ).
fof(f350,plain,
v4_orders_2(sK2),
inference(cnf_transformation,[],[f312]) ).
fof(f351,plain,
v3_orders_2(sK2),
inference(cnf_transformation,[],[f312]) ).
fof(f352,plain,
v2_orders_2(sK2),
inference(cnf_transformation,[],[f312]) ).
fof(f353,plain,
l1_orders_2(sK3),
inference(cnf_transformation,[],[f312]) ).
fof(f354,plain,
v3_lattice3(sK3),
inference(cnf_transformation,[],[f312]) ).
fof(f355,plain,
v2_lattice3(sK3),
inference(cnf_transformation,[],[f312]) ).
fof(f356,plain,
v1_lattice3(sK3),
inference(cnf_transformation,[],[f312]) ).
fof(f357,plain,
v4_orders_2(sK3),
inference(cnf_transformation,[],[f312]) ).
fof(f358,plain,
v3_orders_2(sK3),
inference(cnf_transformation,[],[f312]) ).
fof(f359,plain,
v2_orders_2(sK3),
inference(cnf_transformation,[],[f312]) ).
fof(f360,plain,
m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)),
inference(cnf_transformation,[],[f312]) ).
fof(f361,plain,
v18_waybel_0(sK4,sK3,sK2),
inference(cnf_transformation,[],[f312]) ).
fof(f362,plain,
v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2)),
inference(cnf_transformation,[],[f312]) ).
fof(f363,plain,
v1_funct_1(sK4),
inference(cnf_transformation,[],[f312]) ).
fof(f364,plain,
m1_subset_1(sK5,u1_struct_0(sK2)),
inference(cnf_transformation,[],[f312]) ).
fof(f365,plain,
k7_yellow_2(u1_struct_0(sK2),sK3,k2_waybel34(sK2,sK3,sK4),sK5) != k1_yellow_0(sK3,k5_pre_topc(sK3,sK2,sK4,k6_waybel_0(sK2,sK5))),
inference(cnf_transformation,[],[f312]) ).
fof(f466,plain,
! [X0] :
( ~ v3_struct_0(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f203]) ).
fof(f487,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,[],[f315]) ).
fof(f491,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,[],[f317]) ).
fof(f496,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,[],[f229]) ).
fof(f497,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,[],[f229]) ).
fof(f498,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(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_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| v1_funct_1(k2_waybel34(X0,X1,X2)) ),
inference(cnf_transformation,[],[f229]) ).
fof(f502,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,[],[f237]) ).
fof(f503,plain,
! [X0] :
( ~ l1_orders_2(X0)
| l1_struct_0(X0) ),
inference(cnf_transformation,[],[f238]) ).
fof(f538,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[],[f257]) ).
fof(f642,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f341]) ).
fof(f645,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,[],[f345]) ).
fof(f658,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,[],[f487]) ).
fof(f660,definition,
sF30 = u1_struct_0(sK2),
introduced(definition,[new_symbols(definition,[sF30])],[function_definition]) ).
fof(f661,plain,
u1_struct_0(sK2) = sF30,
inference(reorient_equations,[],[f660]) ).
fof(f662,definition,
sF31 = k2_waybel34(sK2,sK3,sK4),
introduced(definition,[new_symbols(definition,[sF31])],[function_definition]) ).
fof(f663,plain,
k2_waybel34(sK2,sK3,sK4) = sF31,
inference(reorient_equations,[],[f662]) ).
fof(f664,definition,
sF32 = k7_yellow_2(sF30,sK3,sF31,sK5),
introduced(definition,[new_symbols(definition,[sF32])],[function_definition]) ).
fof(f665,plain,
k7_yellow_2(sF30,sK3,sF31,sK5) = sF32,
inference(reorient_equations,[],[f664]) ).
fof(f666,definition,
sF33 = k6_waybel_0(sK2,sK5),
introduced(definition,[new_symbols(definition,[sF33])],[function_definition]) ).
fof(f667,plain,
k6_waybel_0(sK2,sK5) = sF33,
inference(reorient_equations,[],[f666]) ).
fof(f668,definition,
sF34 = k5_pre_topc(sK3,sK2,sK4,sF33),
introduced(definition,[new_symbols(definition,[sF34])],[function_definition]) ).
fof(f669,plain,
k5_pre_topc(sK3,sK2,sK4,sF33) = sF34,
inference(reorient_equations,[],[f668]) ).
fof(f670,definition,
sF35 = k1_yellow_0(sK3,sF34),
introduced(definition,[new_symbols(definition,[sF35])],[function_definition]) ).
fof(f671,plain,
k1_yellow_0(sK3,sF34) = sF35,
inference(reorient_equations,[],[f670]) ).
fof(f672,plain,
sF32 != sF35,
inference(definition_folding,[],[f365,f671,f669,f667,f665,f663,f661]) ).
fof(f673,plain,
m1_subset_1(sK5,sF30),
inference(definition_folding,[],[f364,f661]) ).
fof(f674,definition,
sF36 = u1_struct_0(sK3),
introduced(definition,[new_symbols(definition,[sF36])],[function_definition]) ).
fof(f675,plain,
u1_struct_0(sK3) = sF36,
inference(reorient_equations,[],[f674]) ).
fof(f676,plain,
v1_funct_2(sK4,sF36,sF30),
inference(definition_folding,[],[f362,f661,f675]) ).
fof(f677,plain,
m2_relset_1(sK4,sF36,sF30),
inference(definition_folding,[],[f360,f661,f675]) ).
fof(f680,plain,
m1_relset_1(sK4,sF36,sF30),
inference(resolution,[],[f642,f677]) ).
fof(f693,definition,
( spl37_1
<=> l1_struct_0(sK3) ),
introduced(definition,[new_symbols(definition,[spl37_1])],[avatar_definition]) ).
fof(f694,plain,
( l1_struct_0(sK3)
| ~ spl37_1 ),
inference(avatar_component_clause,[],[f693]) ).
fof(f695,plain,
( ~ l1_struct_0(sK3)
| spl37_1 ),
inference(avatar_component_clause,[],[f693]) ).
fof(f701,definition,
( spl37_3
<=> l1_struct_0(sK2) ),
introduced(definition,[new_symbols(definition,[spl37_3])],[avatar_definition]) ).
fof(f702,plain,
( l1_struct_0(sK2)
| ~ spl37_3 ),
inference(avatar_component_clause,[],[f701]) ).
fof(f703,plain,
( ~ l1_struct_0(sK2)
| spl37_3 ),
inference(avatar_component_clause,[],[f701]) ).
fof(f718,plain,
! [X2,X0,X1] :
( r4_waybel_1(X0,k7_yellow_2(u1_struct_0(sK2),X0,X1,sK5),k5_pre_topc(X0,sK2,X2,sF33))
| ~ m1_subset_1(sK5,u1_struct_0(sK2))
| ~ v3_waybel_1(k1_waybel_1(sK2,X0,X1,X2),sK2,X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(sK2))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(sK2))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK2),u1_struct_0(X0))
| ~ m2_relset_1(X1,u1_struct_0(sK2),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(sK2)
| ~ v2_orders_2(sK2)
| ~ v3_orders_2(sK2)
| ~ v4_orders_2(sK2)
| ~ l1_orders_2(sK2) ),
inference(superposition,[],[f645,f667]) ).
fof(f719,plain,
! [X2,X0,X1] :
( r4_waybel_1(X0,k7_yellow_2(u1_struct_0(sK2),X0,X1,sK5),k5_pre_topc(X0,sK2,X2,sF33))
| ~ m1_subset_1(sK5,u1_struct_0(sK2))
| ~ v3_waybel_1(k1_waybel_1(sK2,X0,X1,X2),sK2,X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(sK2))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(sK2))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK2),u1_struct_0(X0))
| ~ m2_relset_1(X1,u1_struct_0(sK2),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(sK2)
| ~ v3_orders_2(sK2)
| ~ v4_orders_2(sK2)
| ~ l1_orders_2(sK2) ),
inference(forward_subsumption_resolution,[],[f718,f352]) ).
fof(f722,plain,
! [X2,X0,X1] :
( r4_waybel_1(X0,k7_yellow_2(u1_struct_0(sK2),X0,X1,sK5),k5_pre_topc(X0,sK2,X2,sF33))
| ~ m1_subset_1(sK5,u1_struct_0(sK2))
| ~ v3_waybel_1(k1_waybel_1(sK2,X0,X1,X2),sK2,X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(sK2))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(sK2))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK2),u1_struct_0(X0))
| ~ m2_relset_1(X1,u1_struct_0(sK2),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(sK2)
| ~ v4_orders_2(sK2)
| ~ l1_orders_2(sK2) ),
inference(forward_subsumption_resolution,[],[f719,f351]) ).
fof(f725,plain,
! [X2,X0,X1] :
( r4_waybel_1(X0,k7_yellow_2(u1_struct_0(sK2),X0,X1,sK5),k5_pre_topc(X0,sK2,X2,sF33))
| ~ m1_subset_1(sK5,u1_struct_0(sK2))
| ~ v3_waybel_1(k1_waybel_1(sK2,X0,X1,X2),sK2,X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(sK2))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(sK2))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK2),u1_struct_0(X0))
| ~ m2_relset_1(X1,u1_struct_0(sK2),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(sK2)
| ~ l1_orders_2(sK2) ),
inference(forward_subsumption_resolution,[],[f722,f350]) ).
fof(f728,plain,
! [X2,X0,X1] :
( r4_waybel_1(X0,k7_yellow_2(u1_struct_0(sK2),X0,X1,sK5),k5_pre_topc(X0,sK2,X2,sF33))
| ~ m1_subset_1(sK5,u1_struct_0(sK2))
| ~ v3_waybel_1(k1_waybel_1(sK2,X0,X1,X2),sK2,X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(sK2))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(sK2))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK2),u1_struct_0(X0))
| ~ m2_relset_1(X1,u1_struct_0(sK2),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(sK2) ),
inference(forward_subsumption_resolution,[],[f725,f346]) ).
fof(f731,plain,
! [X2,X0,X1] :
( r4_waybel_1(X0,k7_yellow_2(sF30,X0,X1,sK5),k5_pre_topc(X0,sK2,X2,sF33))
| ~ m1_subset_1(sK5,u1_struct_0(sK2))
| ~ v3_waybel_1(k1_waybel_1(sK2,X0,X1,X2),sK2,X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(sK2))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(sK2))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK2),u1_struct_0(X0))
| ~ m2_relset_1(X1,u1_struct_0(sK2),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(sK2) ),
inference(forward_demodulation,[],[f728,f661]) ).
fof(f733,definition,
( spl37_7
<=> v3_struct_0(sK3) ),
introduced(definition,[new_symbols(definition,[spl37_7])],[avatar_definition]) ).
fof(f734,plain,
( ~ v3_struct_0(sK3)
| spl37_7 ),
inference(avatar_component_clause,[],[f733]) ).
fof(f735,plain,
( v3_struct_0(sK3)
| ~ spl37_7 ),
inference(avatar_component_clause,[],[f733]) ).
fof(f741,definition,
( spl37_9
<=> v3_struct_0(sK2) ),
introduced(definition,[new_symbols(definition,[spl37_9])],[avatar_definition]) ).
fof(f742,plain,
( ~ v3_struct_0(sK2)
| spl37_9 ),
inference(avatar_component_clause,[],[f741]) ).
fof(f743,plain,
( v3_struct_0(sK2)
| ~ spl37_9 ),
inference(avatar_component_clause,[],[f741]) ).
fof(f748,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(sK5,sF30)
| r4_waybel_1(X0,k7_yellow_2(sF30,X0,X1,sK5),k5_pre_topc(X0,sK2,X2,sF33))
| ~ v3_waybel_1(k1_waybel_1(sK2,X0,X1,X2),sK2,X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(sK2))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(sK2))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK2),u1_struct_0(X0))
| ~ m2_relset_1(X1,u1_struct_0(sK2),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(sK2) ),
inference(forward_demodulation,[],[f731,f661]) ).
fof(f749,plain,
! [X2,X0,X1] :
( r4_waybel_1(X0,k7_yellow_2(sF30,X0,X1,sK5),k5_pre_topc(X0,sK2,X2,sF33))
| ~ v3_waybel_1(k1_waybel_1(sK2,X0,X1,X2),sK2,X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(sK2))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(sK2))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK2),u1_struct_0(X0))
| ~ m2_relset_1(X1,u1_struct_0(sK2),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(sK2) ),
inference(forward_subsumption_resolution,[],[f748,f673]) ).
fof(f750,plain,
! [X2,X0,X1] :
( ~ v1_funct_2(X2,u1_struct_0(X0),sF30)
| r4_waybel_1(X0,k7_yellow_2(sF30,X0,X1,sK5),k5_pre_topc(X0,sK2,X2,sF33))
| ~ v3_waybel_1(k1_waybel_1(sK2,X0,X1,X2),sK2,X0)
| ~ v1_funct_1(X2)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(sK2))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK2),u1_struct_0(X0))
| ~ m2_relset_1(X1,u1_struct_0(sK2),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(sK2) ),
inference(forward_demodulation,[],[f749,f661]) ).
fof(f751,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,u1_struct_0(X0),sF30)
| ~ v1_funct_2(X2,u1_struct_0(X0),sF30)
| r4_waybel_1(X0,k7_yellow_2(sF30,X0,X1,sK5),k5_pre_topc(X0,sK2,X2,sF33))
| ~ v3_waybel_1(k1_waybel_1(sK2,X0,X1,X2),sK2,X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK2),u1_struct_0(X0))
| ~ m2_relset_1(X1,u1_struct_0(sK2),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(sK2) ),
inference(forward_demodulation,[],[f750,f661]) ).
fof(f752,plain,
! [X2,X0,X1] :
( ~ v1_funct_2(X1,sF30,u1_struct_0(X0))
| ~ m2_relset_1(X2,u1_struct_0(X0),sF30)
| ~ v1_funct_2(X2,u1_struct_0(X0),sF30)
| r4_waybel_1(X0,k7_yellow_2(sF30,X0,X1,sK5),k5_pre_topc(X0,sK2,X2,sF33))
| ~ v3_waybel_1(k1_waybel_1(sK2,X0,X1,X2),sK2,X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_1(X1)
| ~ m2_relset_1(X1,u1_struct_0(sK2),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(sK2) ),
inference(forward_demodulation,[],[f751,f661]) ).
fof(f753,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X1,sF30,u1_struct_0(X0))
| ~ v1_funct_2(X1,sF30,u1_struct_0(X0))
| ~ m2_relset_1(X2,u1_struct_0(X0),sF30)
| ~ v1_funct_2(X2,u1_struct_0(X0),sF30)
| r4_waybel_1(X0,k7_yellow_2(sF30,X0,X1,sK5),k5_pre_topc(X0,sK2,X2,sF33))
| ~ v3_waybel_1(k1_waybel_1(sK2,X0,X1,X2),sK2,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(sK2) ),
inference(forward_demodulation,[],[f752,f661]) ).
fof(f755,definition,
( spl37_11
<=> ! [X2,X0,X1] :
( ~ m2_relset_1(X1,sF30,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(sK2,X0,X1,X2),sK2,X0)
| r4_waybel_1(X0,k7_yellow_2(sF30,X0,X1,sK5),k5_pre_topc(X0,sK2,X2,sF33))
| ~ v1_funct_2(X2,u1_struct_0(X0),sF30)
| ~ m2_relset_1(X2,u1_struct_0(X0),sF30)
| ~ v1_funct_2(X1,sF30,u1_struct_0(X0)) ) ),
introduced(definition,[new_symbols(definition,[spl37_11])],[avatar_definition]) ).
fof(f756,plain,
( ! [X2,X0,X1] :
( r4_waybel_1(X0,k7_yellow_2(sF30,X0,X1,sK5),k5_pre_topc(X0,sK2,X2,sF33))
| ~ 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(sK2,X0,X1,X2),sK2,X0)
| ~ m2_relset_1(X1,sF30,u1_struct_0(X0))
| ~ v1_funct_2(X2,u1_struct_0(X0),sF30)
| ~ m2_relset_1(X2,u1_struct_0(X0),sF30)
| ~ v1_funct_2(X1,sF30,u1_struct_0(X0)) )
| ~ spl37_11 ),
inference(avatar_component_clause,[],[f755]) ).
fof(f757,plain,
( spl37_9
| spl37_11 ),
inference(avatar_split_clause,[],[f753,f755,f741]) ).
fof(f761,plain,
( m1_subset_1(sF32,u1_struct_0(sK3))
| v1_xboole_0(sF30)
| v3_struct_0(sK3)
| ~ l1_struct_0(sK3)
| ~ v1_funct_1(sF31)
| ~ v1_funct_2(sF31,sF30,u1_struct_0(sK3))
| ~ m1_relset_1(sF31,sF30,u1_struct_0(sK3))
| ~ m1_subset_1(sK5,sF30) ),
inference(superposition,[],[f502,f665]) ).
fof(f767,plain,
( ~ v2_lattice3(sK3)
| ~ l1_orders_2(sK3)
| ~ spl37_7 ),
inference(resolution,[],[f466,f735]) ).
fof(f768,plain,
( ~ v2_lattice3(sK2)
| ~ l1_orders_2(sK2)
| ~ spl37_9 ),
inference(resolution,[],[f466,f743]) ).
fof(f769,plain,
( ~ l1_orders_2(sK2)
| ~ spl37_9 ),
inference(forward_subsumption_resolution,[],[f768,f348]) ).
fof(f770,plain,
( ~ l1_orders_2(sK3)
| ~ spl37_7 ),
inference(forward_subsumption_resolution,[],[f767,f355]) ).
fof(f771,plain,
( $false
| ~ spl37_9 ),
inference(forward_subsumption_resolution,[],[f769,f346]) ).
fof(f772,plain,
~ spl37_9,
inference(avatar_contradiction_clause,[],[f771]) ).
fof(f773,plain,
( $false
| ~ spl37_7 ),
inference(forward_subsumption_resolution,[],[f770,f353]) ).
fof(f774,plain,
~ spl37_7,
inference(avatar_contradiction_clause,[],[f773]) ).
fof(f777,plain,
( ! [X0] :
( r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,X0,sK5),sF34)
| ~ l1_orders_2(sK3)
| ~ v4_orders_2(sK3)
| ~ v3_orders_2(sK3)
| ~ v2_orders_2(sK3)
| v3_struct_0(sK3)
| ~ v1_funct_1(X0)
| ~ v1_funct_1(sK4)
| ~ v3_waybel_1(k1_waybel_1(sK2,sK3,X0,sK4),sK2,sK3)
| ~ m2_relset_1(X0,sF30,u1_struct_0(sK3))
| ~ v1_funct_2(sK4,u1_struct_0(sK3),sF30)
| ~ m2_relset_1(sK4,u1_struct_0(sK3),sF30)
| ~ v1_funct_2(X0,sF30,u1_struct_0(sK3)) )
| ~ spl37_11 ),
inference(superposition,[],[f756,f669]) ).
fof(f779,plain,
( ! [X0] :
( r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,X0,sK5),sF34)
| ~ v4_orders_2(sK3)
| ~ v3_orders_2(sK3)
| ~ v2_orders_2(sK3)
| v3_struct_0(sK3)
| ~ v1_funct_1(X0)
| ~ v1_funct_1(sK4)
| ~ v3_waybel_1(k1_waybel_1(sK2,sK3,X0,sK4),sK2,sK3)
| ~ m2_relset_1(X0,sF30,u1_struct_0(sK3))
| ~ v1_funct_2(sK4,u1_struct_0(sK3),sF30)
| ~ m2_relset_1(sK4,u1_struct_0(sK3),sF30)
| ~ v1_funct_2(X0,sF30,u1_struct_0(sK3)) )
| ~ spl37_11 ),
inference(forward_subsumption_resolution,[],[f777,f353]) ).
fof(f781,plain,
( ! [X0] :
( r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,X0,sK5),sF34)
| ~ v3_orders_2(sK3)
| ~ v2_orders_2(sK3)
| v3_struct_0(sK3)
| ~ v1_funct_1(X0)
| ~ v1_funct_1(sK4)
| ~ v3_waybel_1(k1_waybel_1(sK2,sK3,X0,sK4),sK2,sK3)
| ~ m2_relset_1(X0,sF30,u1_struct_0(sK3))
| ~ v1_funct_2(sK4,u1_struct_0(sK3),sF30)
| ~ m2_relset_1(sK4,u1_struct_0(sK3),sF30)
| ~ v1_funct_2(X0,sF30,u1_struct_0(sK3)) )
| ~ spl37_11 ),
inference(forward_subsumption_resolution,[],[f779,f357]) ).
fof(f783,plain,
( ! [X0] :
( r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,X0,sK5),sF34)
| ~ v2_orders_2(sK3)
| v3_struct_0(sK3)
| ~ v1_funct_1(X0)
| ~ v1_funct_1(sK4)
| ~ v3_waybel_1(k1_waybel_1(sK2,sK3,X0,sK4),sK2,sK3)
| ~ m2_relset_1(X0,sF30,u1_struct_0(sK3))
| ~ v1_funct_2(sK4,u1_struct_0(sK3),sF30)
| ~ m2_relset_1(sK4,u1_struct_0(sK3),sF30)
| ~ v1_funct_2(X0,sF30,u1_struct_0(sK3)) )
| ~ spl37_11 ),
inference(forward_subsumption_resolution,[],[f781,f358]) ).
fof(f785,plain,
( ! [X0] :
( r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,X0,sK5),sF34)
| v3_struct_0(sK3)
| ~ v1_funct_1(X0)
| ~ v1_funct_1(sK4)
| ~ v3_waybel_1(k1_waybel_1(sK2,sK3,X0,sK4),sK2,sK3)
| ~ m2_relset_1(X0,sF30,u1_struct_0(sK3))
| ~ v1_funct_2(sK4,u1_struct_0(sK3),sF30)
| ~ m2_relset_1(sK4,u1_struct_0(sK3),sF30)
| ~ v1_funct_2(X0,sF30,u1_struct_0(sK3)) )
| ~ spl37_11 ),
inference(forward_subsumption_resolution,[],[f783,f359]) ).
fof(f787,plain,
( ! [X0] :
( r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,X0,sK5),sF34)
| ~ v1_funct_1(X0)
| ~ v1_funct_1(sK4)
| ~ v3_waybel_1(k1_waybel_1(sK2,sK3,X0,sK4),sK2,sK3)
| ~ m2_relset_1(X0,sF30,u1_struct_0(sK3))
| ~ v1_funct_2(sK4,u1_struct_0(sK3),sF30)
| ~ m2_relset_1(sK4,u1_struct_0(sK3),sF30)
| ~ v1_funct_2(X0,sF30,u1_struct_0(sK3)) )
| spl37_7
| ~ spl37_11 ),
inference(forward_subsumption_resolution,[],[f785,f734]) ).
fof(f789,plain,
( ! [X0] :
( r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,X0,sK5),sF34)
| ~ v1_funct_1(X0)
| ~ v3_waybel_1(k1_waybel_1(sK2,sK3,X0,sK4),sK2,sK3)
| ~ m2_relset_1(X0,sF30,u1_struct_0(sK3))
| ~ v1_funct_2(sK4,u1_struct_0(sK3),sF30)
| ~ m2_relset_1(sK4,u1_struct_0(sK3),sF30)
| ~ v1_funct_2(X0,sF30,u1_struct_0(sK3)) )
| spl37_7
| ~ spl37_11 ),
inference(forward_subsumption_resolution,[],[f787,f363]) ).
fof(f791,plain,
( ! [X0] :
( ~ m2_relset_1(X0,sF30,sF36)
| r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,X0,sK5),sF34)
| ~ v1_funct_1(X0)
| ~ v3_waybel_1(k1_waybel_1(sK2,sK3,X0,sK4),sK2,sK3)
| ~ v1_funct_2(sK4,u1_struct_0(sK3),sF30)
| ~ m2_relset_1(sK4,u1_struct_0(sK3),sF30)
| ~ v1_funct_2(X0,sF30,u1_struct_0(sK3)) )
| spl37_7
| ~ spl37_11 ),
inference(forward_demodulation,[],[f789,f675]) ).
fof(f793,plain,
( ! [X0] :
( ~ v1_funct_2(sK4,sF36,sF30)
| ~ m2_relset_1(X0,sF30,sF36)
| r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,X0,sK5),sF34)
| ~ v1_funct_1(X0)
| ~ v3_waybel_1(k1_waybel_1(sK2,sK3,X0,sK4),sK2,sK3)
| ~ m2_relset_1(sK4,u1_struct_0(sK3),sF30)
| ~ v1_funct_2(X0,sF30,u1_struct_0(sK3)) )
| spl37_7
| ~ spl37_11 ),
inference(forward_demodulation,[],[f791,f675]) ).
fof(f795,plain,
( ! [X0] :
( ~ m2_relset_1(X0,sF30,sF36)
| r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,X0,sK5),sF34)
| ~ v1_funct_1(X0)
| ~ v3_waybel_1(k1_waybel_1(sK2,sK3,X0,sK4),sK2,sK3)
| ~ m2_relset_1(sK4,u1_struct_0(sK3),sF30)
| ~ v1_funct_2(X0,sF30,u1_struct_0(sK3)) )
| spl37_7
| ~ spl37_11 ),
inference(forward_subsumption_resolution,[],[f793,f676]) ).
fof(f797,plain,
( ! [X0] :
( ~ m2_relset_1(sK4,sF36,sF30)
| ~ m2_relset_1(X0,sF30,sF36)
| r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,X0,sK5),sF34)
| ~ v1_funct_1(X0)
| ~ v3_waybel_1(k1_waybel_1(sK2,sK3,X0,sK4),sK2,sK3)
| ~ v1_funct_2(X0,sF30,u1_struct_0(sK3)) )
| spl37_7
| ~ spl37_11 ),
inference(forward_demodulation,[],[f795,f675]) ).
fof(f799,definition,
( spl37_12
<=> v1_funct_1(sF31) ),
introduced(definition,[new_symbols(definition,[spl37_12])],[avatar_definition]) ).
fof(f800,plain,
( v1_funct_1(sF31)
| ~ spl37_12 ),
inference(avatar_component_clause,[],[f799]) ).
fof(f801,plain,
( ~ v1_funct_1(sF31)
| spl37_12 ),
inference(avatar_component_clause,[],[f799]) ).
fof(f803,definition,
( spl37_13
<=> m2_relset_1(sF31,sF30,sF36) ),
introduced(definition,[new_symbols(definition,[spl37_13])],[avatar_definition]) ).
fof(f804,plain,
( m2_relset_1(sF31,sF30,sF36)
| ~ spl37_13 ),
inference(avatar_component_clause,[],[f803]) ).
fof(f810,definition,
( spl37_15
<=> v1_funct_2(sF31,sF30,sF36) ),
introduced(definition,[new_symbols(definition,[spl37_15])],[avatar_definition]) ).
fof(f811,plain,
( v1_funct_2(sF31,sF30,sF36)
| ~ spl37_15 ),
inference(avatar_component_clause,[],[f810]) ).
fof(f814,plain,
( ! [X0] :
( ~ m2_relset_1(X0,sF30,sF36)
| r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,X0,sK5),sF34)
| ~ v1_funct_1(X0)
| ~ v3_waybel_1(k1_waybel_1(sK2,sK3,X0,sK4),sK2,sK3)
| ~ v1_funct_2(X0,sF30,u1_struct_0(sK3)) )
| spl37_7
| ~ spl37_11 ),
inference(forward_subsumption_resolution,[],[f797,f677]) ).
fof(f815,plain,
( ! [X0] :
( ~ v3_waybel_1(k1_waybel_1(sK2,sK3,X0,sK4),sK2,sK3)
| ~ m2_relset_1(X0,sF30,sF36)
| r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,X0,sK5),sF34)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,sF30,sF36) )
| spl37_7
| ~ spl37_11 ),
inference(forward_demodulation,[],[f814,f675]) ).
fof(f826,plain,
l1_struct_0(sK3),
inference(resolution,[],[f503,f353]) ).
fof(f827,plain,
l1_struct_0(sK2),
inference(resolution,[],[f503,f346]) ).
fof(f828,plain,
( $false
| spl37_3 ),
inference(forward_subsumption_resolution,[],[f827,f703]) ).
fof(f829,plain,
spl37_3,
inference(avatar_contradiction_clause,[],[f828]) ).
fof(f830,plain,
( $false
| spl37_1 ),
inference(forward_subsumption_resolution,[],[f826,f695]) ).
fof(f831,plain,
spl37_1,
inference(avatar_contradiction_clause,[],[f830]) ).
fof(f928,plain,
( ~ v1_funct_1(k2_waybel34(sK2,sK3,sK4))
| ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v3_lattice3(sK2)
| ~ v3_lattice3(sK3)
| ~ v18_waybel_0(sK4,sK3,sK2)
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ v2_orders_2(sK3)
| ~ v3_orders_2(sK3)
| ~ v4_orders_2(sK3)
| ~ v1_lattice3(sK3)
| ~ v2_lattice3(sK3)
| ~ l1_orders_2(sK3)
| ~ v2_orders_2(sK2)
| ~ v3_orders_2(sK2)
| ~ v4_orders_2(sK2)
| ~ v1_lattice3(sK2)
| ~ v2_lattice3(sK2)
| ~ l1_orders_2(sK2)
| ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
| r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,k2_waybel34(sK2,sK3,sK4),sK5),sF34)
| ~ v1_funct_1(k2_waybel34(sK2,sK3,sK4))
| ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
| spl37_7
| ~ spl37_11 ),
inference(resolution,[],[f658,f815]) ).
fof(f930,plain,
( ~ v1_funct_1(k2_waybel34(sK2,sK3,sK4))
| ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v3_lattice3(sK2)
| ~ v3_lattice3(sK3)
| ~ v18_waybel_0(sK4,sK3,sK2)
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ v2_orders_2(sK3)
| ~ v3_orders_2(sK3)
| ~ v4_orders_2(sK3)
| ~ v1_lattice3(sK3)
| ~ v2_lattice3(sK3)
| ~ l1_orders_2(sK3)
| ~ v2_orders_2(sK2)
| ~ v3_orders_2(sK2)
| ~ v4_orders_2(sK2)
| ~ v1_lattice3(sK2)
| ~ v2_lattice3(sK2)
| ~ l1_orders_2(sK2)
| ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
| r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,k2_waybel34(sK2,sK3,sK4),sK5),sF34)
| ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
| spl37_7
| ~ spl37_11 ),
inference(duplicate_literal_removal,[],[f928]) ).
fof(f932,plain,
( ~ v1_funct_1(k2_waybel34(sK2,sK3,sK4))
| ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v3_lattice3(sK3)
| ~ v18_waybel_0(sK4,sK3,sK2)
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ v2_orders_2(sK3)
| ~ v3_orders_2(sK3)
| ~ v4_orders_2(sK3)
| ~ v1_lattice3(sK3)
| ~ v2_lattice3(sK3)
| ~ l1_orders_2(sK3)
| ~ v2_orders_2(sK2)
| ~ v3_orders_2(sK2)
| ~ v4_orders_2(sK2)
| ~ v1_lattice3(sK2)
| ~ v2_lattice3(sK2)
| ~ l1_orders_2(sK2)
| ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
| r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,k2_waybel34(sK2,sK3,sK4),sK5),sF34)
| ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
| spl37_7
| ~ spl37_11 ),
inference(forward_subsumption_resolution,[],[f930,f347]) ).
fof(f933,plain,
( ~ v1_funct_1(k2_waybel34(sK2,sK3,sK4))
| ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v18_waybel_0(sK4,sK3,sK2)
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ v2_orders_2(sK3)
| ~ v3_orders_2(sK3)
| ~ v4_orders_2(sK3)
| ~ v1_lattice3(sK3)
| ~ v2_lattice3(sK3)
| ~ l1_orders_2(sK3)
| ~ v2_orders_2(sK2)
| ~ v3_orders_2(sK2)
| ~ v4_orders_2(sK2)
| ~ v1_lattice3(sK2)
| ~ v2_lattice3(sK2)
| ~ l1_orders_2(sK2)
| ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
| r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,k2_waybel34(sK2,sK3,sK4),sK5),sF34)
| ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
| spl37_7
| ~ spl37_11 ),
inference(forward_subsumption_resolution,[],[f932,f354]) ).
fof(f934,plain,
( ~ v1_funct_1(k2_waybel34(sK2,sK3,sK4))
| ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ v2_orders_2(sK3)
| ~ v3_orders_2(sK3)
| ~ v4_orders_2(sK3)
| ~ v1_lattice3(sK3)
| ~ v2_lattice3(sK3)
| ~ l1_orders_2(sK3)
| ~ v2_orders_2(sK2)
| ~ v3_orders_2(sK2)
| ~ v4_orders_2(sK2)
| ~ v1_lattice3(sK2)
| ~ v2_lattice3(sK2)
| ~ l1_orders_2(sK2)
| ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
| r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,k2_waybel34(sK2,sK3,sK4),sK5),sF34)
| ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
| spl37_7
| ~ spl37_11 ),
inference(forward_subsumption_resolution,[],[f933,f361]) ).
fof(f935,plain,
( ~ v1_funct_1(k2_waybel34(sK2,sK3,sK4))
| ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ v2_orders_2(sK3)
| ~ v3_orders_2(sK3)
| ~ v4_orders_2(sK3)
| ~ v1_lattice3(sK3)
| ~ v2_lattice3(sK3)
| ~ l1_orders_2(sK3)
| ~ v2_orders_2(sK2)
| ~ v3_orders_2(sK2)
| ~ v4_orders_2(sK2)
| ~ v1_lattice3(sK2)
| ~ v2_lattice3(sK2)
| ~ l1_orders_2(sK2)
| ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
| r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,k2_waybel34(sK2,sK3,sK4),sK5),sF34)
| ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
| spl37_7
| ~ spl37_11 ),
inference(forward_subsumption_resolution,[],[f934,f363]) ).
fof(f936,plain,
( ~ v1_funct_1(k2_waybel34(sK2,sK3,sK4))
| ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ v3_orders_2(sK3)
| ~ v4_orders_2(sK3)
| ~ v1_lattice3(sK3)
| ~ v2_lattice3(sK3)
| ~ l1_orders_2(sK3)
| ~ v2_orders_2(sK2)
| ~ v3_orders_2(sK2)
| ~ v4_orders_2(sK2)
| ~ v1_lattice3(sK2)
| ~ v2_lattice3(sK2)
| ~ l1_orders_2(sK2)
| ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
| r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,k2_waybel34(sK2,sK3,sK4),sK5),sF34)
| ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
| spl37_7
| ~ spl37_11 ),
inference(forward_subsumption_resolution,[],[f935,f359]) ).
fof(f937,plain,
( ~ v1_funct_1(k2_waybel34(sK2,sK3,sK4))
| ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ v4_orders_2(sK3)
| ~ v1_lattice3(sK3)
| ~ v2_lattice3(sK3)
| ~ l1_orders_2(sK3)
| ~ v2_orders_2(sK2)
| ~ v3_orders_2(sK2)
| ~ v4_orders_2(sK2)
| ~ v1_lattice3(sK2)
| ~ v2_lattice3(sK2)
| ~ l1_orders_2(sK2)
| ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
| r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,k2_waybel34(sK2,sK3,sK4),sK5),sF34)
| ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
| spl37_7
| ~ spl37_11 ),
inference(forward_subsumption_resolution,[],[f936,f358]) ).
fof(f938,plain,
( ~ v1_funct_1(k2_waybel34(sK2,sK3,sK4))
| ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ v1_lattice3(sK3)
| ~ v2_lattice3(sK3)
| ~ l1_orders_2(sK3)
| ~ v2_orders_2(sK2)
| ~ v3_orders_2(sK2)
| ~ v4_orders_2(sK2)
| ~ v1_lattice3(sK2)
| ~ v2_lattice3(sK2)
| ~ l1_orders_2(sK2)
| ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
| r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,k2_waybel34(sK2,sK3,sK4),sK5),sF34)
| ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
| spl37_7
| ~ spl37_11 ),
inference(forward_subsumption_resolution,[],[f937,f357]) ).
fof(f939,plain,
( ~ v1_funct_1(k2_waybel34(sK2,sK3,sK4))
| ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ v2_lattice3(sK3)
| ~ l1_orders_2(sK3)
| ~ v2_orders_2(sK2)
| ~ v3_orders_2(sK2)
| ~ v4_orders_2(sK2)
| ~ v1_lattice3(sK2)
| ~ v2_lattice3(sK2)
| ~ l1_orders_2(sK2)
| ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
| r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,k2_waybel34(sK2,sK3,sK4),sK5),sF34)
| ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
| spl37_7
| ~ spl37_11 ),
inference(forward_subsumption_resolution,[],[f938,f356]) ).
fof(f940,plain,
( ~ v1_funct_1(k2_waybel34(sK2,sK3,sK4))
| ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ l1_orders_2(sK3)
| ~ v2_orders_2(sK2)
| ~ v3_orders_2(sK2)
| ~ v4_orders_2(sK2)
| ~ v1_lattice3(sK2)
| ~ v2_lattice3(sK2)
| ~ l1_orders_2(sK2)
| ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
| r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,k2_waybel34(sK2,sK3,sK4),sK5),sF34)
| ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
| spl37_7
| ~ spl37_11 ),
inference(forward_subsumption_resolution,[],[f939,f355]) ).
fof(f941,plain,
( ~ v1_funct_1(k2_waybel34(sK2,sK3,sK4))
| ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ v2_orders_2(sK2)
| ~ v3_orders_2(sK2)
| ~ v4_orders_2(sK2)
| ~ v1_lattice3(sK2)
| ~ v2_lattice3(sK2)
| ~ l1_orders_2(sK2)
| ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
| r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,k2_waybel34(sK2,sK3,sK4),sK5),sF34)
| ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
| spl37_7
| ~ spl37_11 ),
inference(forward_subsumption_resolution,[],[f940,f353]) ).
fof(f942,plain,
( ~ v1_funct_1(k2_waybel34(sK2,sK3,sK4))
| ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ v3_orders_2(sK2)
| ~ v4_orders_2(sK2)
| ~ v1_lattice3(sK2)
| ~ v2_lattice3(sK2)
| ~ l1_orders_2(sK2)
| ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
| r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,k2_waybel34(sK2,sK3,sK4),sK5),sF34)
| ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
| spl37_7
| ~ spl37_11 ),
inference(forward_subsumption_resolution,[],[f941,f352]) ).
fof(f943,plain,
( ~ v1_funct_1(k2_waybel34(sK2,sK3,sK4))
| ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ v4_orders_2(sK2)
| ~ v1_lattice3(sK2)
| ~ v2_lattice3(sK2)
| ~ l1_orders_2(sK2)
| ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
| r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,k2_waybel34(sK2,sK3,sK4),sK5),sF34)
| ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
| spl37_7
| ~ spl37_11 ),
inference(forward_subsumption_resolution,[],[f942,f351]) ).
fof(f944,plain,
( ~ v1_funct_1(k2_waybel34(sK2,sK3,sK4))
| ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ v1_lattice3(sK2)
| ~ v2_lattice3(sK2)
| ~ l1_orders_2(sK2)
| ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
| r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,k2_waybel34(sK2,sK3,sK4),sK5),sF34)
| ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
| spl37_7
| ~ spl37_11 ),
inference(forward_subsumption_resolution,[],[f943,f350]) ).
fof(f945,plain,
( ~ v1_funct_1(k2_waybel34(sK2,sK3,sK4))
| ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ v2_lattice3(sK2)
| ~ l1_orders_2(sK2)
| ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
| r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,k2_waybel34(sK2,sK3,sK4),sK5),sF34)
| ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
| spl37_7
| ~ spl37_11 ),
inference(forward_subsumption_resolution,[],[f944,f349]) ).
fof(f946,plain,
( ~ v1_funct_1(k2_waybel34(sK2,sK3,sK4))
| ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ l1_orders_2(sK2)
| ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
| r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,k2_waybel34(sK2,sK3,sK4),sK5),sF34)
| ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
| spl37_7
| ~ spl37_11 ),
inference(forward_subsumption_resolution,[],[f945,f348]) ).
fof(f947,plain,
( ~ v1_funct_1(k2_waybel34(sK2,sK3,sK4))
| ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
| r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,k2_waybel34(sK2,sK3,sK4),sK5),sF34)
| ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
| spl37_7
| ~ spl37_11 ),
inference(forward_subsumption_resolution,[],[f946,f346]) ).
fof(f948,plain,
( ~ v1_funct_1(sF31)
| ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
| r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,k2_waybel34(sK2,sK3,sK4),sK5),sF34)
| ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
| spl37_7
| ~ spl37_11 ),
inference(forward_demodulation,[],[f947,f663]) ).
fof(f952,plain,
( m2_relset_1(sF31,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v2_orders_2(sK2)
| ~ v3_orders_2(sK2)
| ~ v4_orders_2(sK2)
| ~ v1_lattice3(sK2)
| ~ v2_lattice3(sK2)
| ~ l1_orders_2(sK2)
| ~ v2_orders_2(sK3)
| ~ v3_orders_2(sK3)
| ~ v4_orders_2(sK3)
| ~ v1_lattice3(sK3)
| ~ v2_lattice3(sK3)
| ~ l1_orders_2(sK3)
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
inference(superposition,[],[f496,f663]) ).
fof(f961,plain,
( m2_relset_1(sF31,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v3_orders_2(sK2)
| ~ v4_orders_2(sK2)
| ~ v1_lattice3(sK2)
| ~ v2_lattice3(sK2)
| ~ l1_orders_2(sK2)
| ~ v2_orders_2(sK3)
| ~ v3_orders_2(sK3)
| ~ v4_orders_2(sK3)
| ~ v1_lattice3(sK3)
| ~ v2_lattice3(sK3)
| ~ l1_orders_2(sK3)
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
inference(forward_subsumption_resolution,[],[f952,f352]) ).
fof(f966,plain,
( m2_relset_1(sF31,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v4_orders_2(sK2)
| ~ v1_lattice3(sK2)
| ~ v2_lattice3(sK2)
| ~ l1_orders_2(sK2)
| ~ v2_orders_2(sK3)
| ~ v3_orders_2(sK3)
| ~ v4_orders_2(sK3)
| ~ v1_lattice3(sK3)
| ~ v2_lattice3(sK3)
| ~ l1_orders_2(sK3)
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
inference(forward_subsumption_resolution,[],[f961,f351]) ).
fof(f971,plain,
( m2_relset_1(sF31,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v1_lattice3(sK2)
| ~ v2_lattice3(sK2)
| ~ l1_orders_2(sK2)
| ~ v2_orders_2(sK3)
| ~ v3_orders_2(sK3)
| ~ v4_orders_2(sK3)
| ~ v1_lattice3(sK3)
| ~ v2_lattice3(sK3)
| ~ l1_orders_2(sK3)
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
inference(forward_subsumption_resolution,[],[f966,f350]) ).
fof(f976,plain,
( m2_relset_1(sF31,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v2_lattice3(sK2)
| ~ l1_orders_2(sK2)
| ~ v2_orders_2(sK3)
| ~ v3_orders_2(sK3)
| ~ v4_orders_2(sK3)
| ~ v1_lattice3(sK3)
| ~ v2_lattice3(sK3)
| ~ l1_orders_2(sK3)
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
inference(forward_subsumption_resolution,[],[f971,f349]) ).
fof(f981,plain,
( m2_relset_1(sF31,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ l1_orders_2(sK2)
| ~ v2_orders_2(sK3)
| ~ v3_orders_2(sK3)
| ~ v4_orders_2(sK3)
| ~ v1_lattice3(sK3)
| ~ v2_lattice3(sK3)
| ~ l1_orders_2(sK3)
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
inference(forward_subsumption_resolution,[],[f976,f348]) ).
fof(f986,plain,
( m2_relset_1(sF31,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v2_orders_2(sK3)
| ~ v3_orders_2(sK3)
| ~ v4_orders_2(sK3)
| ~ v1_lattice3(sK3)
| ~ v2_lattice3(sK3)
| ~ l1_orders_2(sK3)
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
inference(forward_subsumption_resolution,[],[f981,f346]) ).
fof(f987,plain,
( m2_relset_1(sF31,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v3_orders_2(sK3)
| ~ v4_orders_2(sK3)
| ~ v1_lattice3(sK3)
| ~ v2_lattice3(sK3)
| ~ l1_orders_2(sK3)
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
inference(forward_subsumption_resolution,[],[f986,f359]) ).
fof(f988,plain,
( m2_relset_1(sF31,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v4_orders_2(sK3)
| ~ v1_lattice3(sK3)
| ~ v2_lattice3(sK3)
| ~ l1_orders_2(sK3)
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
inference(forward_subsumption_resolution,[],[f987,f358]) ).
fof(f989,plain,
( m2_relset_1(sF31,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v1_lattice3(sK3)
| ~ v2_lattice3(sK3)
| ~ l1_orders_2(sK3)
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
inference(forward_subsumption_resolution,[],[f988,f357]) ).
fof(f990,plain,
( m2_relset_1(sF31,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v2_lattice3(sK3)
| ~ l1_orders_2(sK3)
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
inference(forward_subsumption_resolution,[],[f989,f356]) ).
fof(f991,plain,
( m2_relset_1(sF31,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ l1_orders_2(sK3)
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
inference(forward_subsumption_resolution,[],[f990,f355]) ).
fof(f992,plain,
( m2_relset_1(sF31,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
inference(forward_subsumption_resolution,[],[f991,f353]) ).
fof(f993,plain,
( m2_relset_1(sF31,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
inference(forward_subsumption_resolution,[],[f992,f363]) ).
fof(f994,plain,
( m2_relset_1(sF31,u1_struct_0(sK2),sF36)
| ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
inference(forward_demodulation,[],[f993,f675]) ).
fof(f995,plain,
( m2_relset_1(sF31,sF30,sF36)
| ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
inference(forward_demodulation,[],[f994,f661]) ).
fof(f996,plain,
( ~ v1_funct_2(sK4,u1_struct_0(sK3),sF30)
| m2_relset_1(sF31,sF30,sF36)
| ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
inference(forward_demodulation,[],[f995,f661]) ).
fof(f997,plain,
( ~ v1_funct_2(sK4,sF36,sF30)
| m2_relset_1(sF31,sF30,sF36)
| ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
inference(forward_demodulation,[],[f996,f675]) ).
fof(f998,plain,
( m2_relset_1(sF31,sF30,sF36)
| ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
inference(forward_subsumption_resolution,[],[f997,f676]) ).
fof(f999,plain,
( ~ m1_relset_1(sK4,u1_struct_0(sK3),sF30)
| m2_relset_1(sF31,sF30,sF36) ),
inference(forward_demodulation,[],[f998,f661]) ).
fof(f1000,plain,
( ~ m1_relset_1(sK4,sF36,sF30)
| m2_relset_1(sF31,sF30,sF36) ),
inference(forward_demodulation,[],[f999,f675]) ).
fof(f1001,plain,
m2_relset_1(sF31,sF30,sF36),
inference(forward_subsumption_resolution,[],[f1000,f680]) ).
fof(f1002,plain,
spl37_13,
inference(avatar_split_clause,[],[f1001,f803]) ).
fof(f1003,plain,
( m1_relset_1(sF31,sF30,sF36)
| ~ spl37_13 ),
inference(resolution,[],[f804,f642]) ).
fof(f1042,plain,
( ~ v1_xboole_0(sF30)
| v3_struct_0(sK2)
| ~ l1_struct_0(sK2) ),
inference(superposition,[],[f538,f661]) ).
fof(f1045,plain,
( ~ v1_xboole_0(sF30)
| ~ l1_struct_0(sK2)
| spl37_9 ),
inference(forward_subsumption_resolution,[],[f1042,f742]) ).
fof(f1047,plain,
( ~ v1_xboole_0(sF30)
| ~ spl37_3
| spl37_9 ),
inference(forward_subsumption_resolution,[],[f1045,f702]) ).
fof(f1081,plain,
! [X0,X1] :
( ~ m1_relset_1(X0,sF36,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(sK3)
| ~ v3_orders_2(sK3)
| ~ v4_orders_2(sK3)
| ~ v1_lattice3(sK3)
| ~ v2_lattice3(sK3)
| ~ l1_orders_2(sK3)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,sF36,u1_struct_0(X1))
| v1_funct_1(k2_waybel34(X1,sK3,X0)) ),
inference(superposition,[],[f498,f675]) ).
fof(f1086,plain,
! [X0,X1] :
( ~ m1_relset_1(X0,sF36,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(sK3)
| ~ v4_orders_2(sK3)
| ~ v1_lattice3(sK3)
| ~ v2_lattice3(sK3)
| ~ l1_orders_2(sK3)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,sF36,u1_struct_0(X1))
| v1_funct_1(k2_waybel34(X1,sK3,X0)) ),
inference(forward_subsumption_resolution,[],[f1081,f359]) ).
fof(f1090,plain,
! [X0,X1] :
( ~ m1_relset_1(X0,sF36,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(sK3)
| ~ v1_lattice3(sK3)
| ~ v2_lattice3(sK3)
| ~ l1_orders_2(sK3)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,sF36,u1_struct_0(X1))
| v1_funct_1(k2_waybel34(X1,sK3,X0)) ),
inference(forward_subsumption_resolution,[],[f1086,f358]) ).
fof(f1094,plain,
! [X0,X1] :
( ~ m1_relset_1(X0,sF36,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(sK3)
| ~ v2_lattice3(sK3)
| ~ l1_orders_2(sK3)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,sF36,u1_struct_0(X1))
| v1_funct_1(k2_waybel34(X1,sK3,X0)) ),
inference(forward_subsumption_resolution,[],[f1090,f357]) ).
fof(f1098,plain,
! [X0,X1] :
( ~ m1_relset_1(X0,sF36,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(sK3)
| ~ l1_orders_2(sK3)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,sF36,u1_struct_0(X1))
| v1_funct_1(k2_waybel34(X1,sK3,X0)) ),
inference(forward_subsumption_resolution,[],[f1094,f356]) ).
fof(f1102,plain,
! [X0,X1] :
( ~ m1_relset_1(X0,sF36,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(sK3)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,sF36,u1_struct_0(X1))
| v1_funct_1(k2_waybel34(X1,sK3,X0)) ),
inference(forward_subsumption_resolution,[],[f1098,f355]) ).
fof(f1106,plain,
! [X0,X1] :
( ~ m1_relset_1(X0,sF36,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_2(X0,sF36,u1_struct_0(X1))
| v1_funct_1(k2_waybel34(X1,sK3,X0)) ),
inference(forward_subsumption_resolution,[],[f1102,f353]) ).
fof(f1108,plain,
( v1_funct_2(sF31,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v2_orders_2(sK2)
| ~ v3_orders_2(sK2)
| ~ v4_orders_2(sK2)
| ~ v1_lattice3(sK2)
| ~ v2_lattice3(sK2)
| ~ l1_orders_2(sK2)
| ~ v2_orders_2(sK3)
| ~ v3_orders_2(sK3)
| ~ v4_orders_2(sK3)
| ~ v1_lattice3(sK3)
| ~ v2_lattice3(sK3)
| ~ l1_orders_2(sK3)
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
inference(superposition,[],[f497,f663]) ).
fof(f1117,plain,
( v1_funct_2(sF31,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v3_orders_2(sK2)
| ~ v4_orders_2(sK2)
| ~ v1_lattice3(sK2)
| ~ v2_lattice3(sK2)
| ~ l1_orders_2(sK2)
| ~ v2_orders_2(sK3)
| ~ v3_orders_2(sK3)
| ~ v4_orders_2(sK3)
| ~ v1_lattice3(sK3)
| ~ v2_lattice3(sK3)
| ~ l1_orders_2(sK3)
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
inference(forward_subsumption_resolution,[],[f1108,f352]) ).
fof(f1122,plain,
( v1_funct_2(sF31,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v4_orders_2(sK2)
| ~ v1_lattice3(sK2)
| ~ v2_lattice3(sK2)
| ~ l1_orders_2(sK2)
| ~ v2_orders_2(sK3)
| ~ v3_orders_2(sK3)
| ~ v4_orders_2(sK3)
| ~ v1_lattice3(sK3)
| ~ v2_lattice3(sK3)
| ~ l1_orders_2(sK3)
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
inference(forward_subsumption_resolution,[],[f1117,f351]) ).
fof(f1127,plain,
( v1_funct_2(sF31,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v1_lattice3(sK2)
| ~ v2_lattice3(sK2)
| ~ l1_orders_2(sK2)
| ~ v2_orders_2(sK3)
| ~ v3_orders_2(sK3)
| ~ v4_orders_2(sK3)
| ~ v1_lattice3(sK3)
| ~ v2_lattice3(sK3)
| ~ l1_orders_2(sK3)
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
inference(forward_subsumption_resolution,[],[f1122,f350]) ).
fof(f1132,plain,
( v1_funct_2(sF31,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v2_lattice3(sK2)
| ~ l1_orders_2(sK2)
| ~ v2_orders_2(sK3)
| ~ v3_orders_2(sK3)
| ~ v4_orders_2(sK3)
| ~ v1_lattice3(sK3)
| ~ v2_lattice3(sK3)
| ~ l1_orders_2(sK3)
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
inference(forward_subsumption_resolution,[],[f1127,f349]) ).
fof(f1137,plain,
( v1_funct_2(sF31,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ l1_orders_2(sK2)
| ~ v2_orders_2(sK3)
| ~ v3_orders_2(sK3)
| ~ v4_orders_2(sK3)
| ~ v1_lattice3(sK3)
| ~ v2_lattice3(sK3)
| ~ l1_orders_2(sK3)
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
inference(forward_subsumption_resolution,[],[f1132,f348]) ).
fof(f1142,plain,
( v1_funct_2(sF31,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v2_orders_2(sK3)
| ~ v3_orders_2(sK3)
| ~ v4_orders_2(sK3)
| ~ v1_lattice3(sK3)
| ~ v2_lattice3(sK3)
| ~ l1_orders_2(sK3)
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
inference(forward_subsumption_resolution,[],[f1137,f346]) ).
fof(f1143,plain,
( v1_funct_2(sF31,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v3_orders_2(sK3)
| ~ v4_orders_2(sK3)
| ~ v1_lattice3(sK3)
| ~ v2_lattice3(sK3)
| ~ l1_orders_2(sK3)
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
inference(forward_subsumption_resolution,[],[f1142,f359]) ).
fof(f1144,plain,
( v1_funct_2(sF31,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v4_orders_2(sK3)
| ~ v1_lattice3(sK3)
| ~ v2_lattice3(sK3)
| ~ l1_orders_2(sK3)
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
inference(forward_subsumption_resolution,[],[f1143,f358]) ).
fof(f1145,plain,
( v1_funct_2(sF31,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v1_lattice3(sK3)
| ~ v2_lattice3(sK3)
| ~ l1_orders_2(sK3)
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
inference(forward_subsumption_resolution,[],[f1144,f357]) ).
fof(f1146,plain,
( v1_funct_2(sF31,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v2_lattice3(sK3)
| ~ l1_orders_2(sK3)
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
inference(forward_subsumption_resolution,[],[f1145,f356]) ).
fof(f1147,plain,
( v1_funct_2(sF31,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ l1_orders_2(sK3)
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
inference(forward_subsumption_resolution,[],[f1146,f355]) ).
fof(f1148,plain,
( v1_funct_2(sF31,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
inference(forward_subsumption_resolution,[],[f1147,f353]) ).
fof(f1149,plain,
( v1_funct_2(sF31,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
inference(forward_subsumption_resolution,[],[f1148,f363]) ).
fof(f1150,plain,
( v1_funct_2(sF31,u1_struct_0(sK2),sF36)
| ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
inference(forward_demodulation,[],[f1149,f675]) ).
fof(f1151,plain,
( v1_funct_2(sF31,sF30,sF36)
| ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
inference(forward_demodulation,[],[f1150,f661]) ).
fof(f1152,plain,
( ~ v1_funct_2(sK4,u1_struct_0(sK3),sF30)
| v1_funct_2(sF31,sF30,sF36)
| ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
inference(forward_demodulation,[],[f1151,f661]) ).
fof(f1153,plain,
( ~ v1_funct_2(sK4,sF36,sF30)
| v1_funct_2(sF31,sF30,sF36)
| ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
inference(forward_demodulation,[],[f1152,f675]) ).
fof(f1154,plain,
( v1_funct_2(sF31,sF30,sF36)
| ~ m1_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2)) ),
inference(forward_subsumption_resolution,[],[f1153,f676]) ).
fof(f1155,plain,
( ~ m1_relset_1(sK4,u1_struct_0(sK3),sF30)
| v1_funct_2(sF31,sF30,sF36) ),
inference(forward_demodulation,[],[f1154,f661]) ).
fof(f1156,plain,
( ~ m1_relset_1(sK4,sF36,sF30)
| v1_funct_2(sF31,sF30,sF36) ),
inference(forward_demodulation,[],[f1155,f675]) ).
fof(f1157,plain,
v1_funct_2(sF31,sF30,sF36),
inference(forward_subsumption_resolution,[],[f1156,f680]) ).
fof(f1158,plain,
spl37_15,
inference(avatar_split_clause,[],[f1157,f810]) ).
fof(f1181,plain,
! [X0] :
( ~ m1_relset_1(X0,sF36,sF30)
| ~ v2_orders_2(sK2)
| ~ v3_orders_2(sK2)
| ~ v4_orders_2(sK2)
| ~ v1_lattice3(sK2)
| ~ v2_lattice3(sK2)
| ~ l1_orders_2(sK2)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,sF36,sF30)
| v1_funct_1(k2_waybel34(sK2,sK3,X0)) ),
inference(superposition,[],[f1106,f661]) ).
fof(f1184,plain,
! [X0] :
( ~ m1_relset_1(X0,sF36,sF30)
| ~ v3_orders_2(sK2)
| ~ v4_orders_2(sK2)
| ~ v1_lattice3(sK2)
| ~ v2_lattice3(sK2)
| ~ l1_orders_2(sK2)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,sF36,sF30)
| v1_funct_1(k2_waybel34(sK2,sK3,X0)) ),
inference(forward_subsumption_resolution,[],[f1181,f352]) ).
fof(f1186,plain,
! [X0] :
( ~ m1_relset_1(X0,sF36,sF30)
| ~ v4_orders_2(sK2)
| ~ v1_lattice3(sK2)
| ~ v2_lattice3(sK2)
| ~ l1_orders_2(sK2)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,sF36,sF30)
| v1_funct_1(k2_waybel34(sK2,sK3,X0)) ),
inference(forward_subsumption_resolution,[],[f1184,f351]) ).
fof(f1188,plain,
! [X0] :
( ~ m1_relset_1(X0,sF36,sF30)
| ~ v1_lattice3(sK2)
| ~ v2_lattice3(sK2)
| ~ l1_orders_2(sK2)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,sF36,sF30)
| v1_funct_1(k2_waybel34(sK2,sK3,X0)) ),
inference(forward_subsumption_resolution,[],[f1186,f350]) ).
fof(f1190,plain,
! [X0] :
( ~ m1_relset_1(X0,sF36,sF30)
| ~ v2_lattice3(sK2)
| ~ l1_orders_2(sK2)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,sF36,sF30)
| v1_funct_1(k2_waybel34(sK2,sK3,X0)) ),
inference(forward_subsumption_resolution,[],[f1188,f349]) ).
fof(f1192,plain,
! [X0] :
( ~ m1_relset_1(X0,sF36,sF30)
| ~ l1_orders_2(sK2)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,sF36,sF30)
| v1_funct_1(k2_waybel34(sK2,sK3,X0)) ),
inference(forward_subsumption_resolution,[],[f1190,f348]) ).
fof(f1194,plain,
! [X0] :
( v1_funct_1(k2_waybel34(sK2,sK3,X0))
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,sF36,sF30)
| ~ m1_relset_1(X0,sF36,sF30) ),
inference(forward_subsumption_resolution,[],[f1192,f346]) ).
fof(f1195,plain,
( v1_funct_1(sF31)
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,sF36,sF30)
| ~ m1_relset_1(sK4,sF36,sF30) ),
inference(superposition,[],[f1194,f663]) ).
fof(f1196,plain,
( ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,sF36,sF30)
| ~ m1_relset_1(sK4,sF36,sF30)
| spl37_12 ),
inference(forward_subsumption_resolution,[],[f1195,f801]) ).
fof(f1197,plain,
( ~ v1_funct_2(sK4,sF36,sF30)
| ~ m1_relset_1(sK4,sF36,sF30)
| spl37_12 ),
inference(forward_subsumption_resolution,[],[f1196,f363]) ).
fof(f1198,plain,
( ~ m1_relset_1(sK4,sF36,sF30)
| spl37_12 ),
inference(forward_subsumption_resolution,[],[f1197,f676]) ).
fof(f1199,plain,
( $false
| spl37_12 ),
inference(forward_subsumption_resolution,[],[f1198,f680]) ).
fof(f1200,plain,
spl37_12,
inference(avatar_contradiction_clause,[],[f1199]) ).
fof(f1201,plain,
( m1_subset_1(sF32,u1_struct_0(sK3))
| v3_struct_0(sK3)
| ~ l1_struct_0(sK3)
| ~ v1_funct_1(sF31)
| ~ v1_funct_2(sF31,sF30,u1_struct_0(sK3))
| ~ m1_relset_1(sF31,sF30,u1_struct_0(sK3))
| ~ m1_subset_1(sK5,sF30)
| ~ spl37_3
| spl37_9 ),
inference(forward_subsumption_resolution,[],[f761,f1047]) ).
fof(f1203,plain,
( ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
| r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,k2_waybel34(sK2,sK3,sK4),sK5),sF34)
| ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
| spl37_7
| ~ spl37_11
| ~ spl37_12 ),
inference(forward_subsumption_resolution,[],[f948,f800]) ).
fof(f1208,plain,
( m1_subset_1(sF32,u1_struct_0(sK3))
| ~ l1_struct_0(sK3)
| ~ v1_funct_1(sF31)
| ~ v1_funct_2(sF31,sF30,u1_struct_0(sK3))
| ~ m1_relset_1(sF31,sF30,u1_struct_0(sK3))
| ~ m1_subset_1(sK5,sF30)
| ~ spl37_3
| spl37_7
| spl37_9 ),
inference(forward_subsumption_resolution,[],[f1201,f734]) ).
fof(f1210,plain,
( ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),sF36)
| ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
| r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,k2_waybel34(sK2,sK3,sK4),sK5),sF34)
| ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
| spl37_7
| ~ spl37_11
| ~ spl37_12 ),
inference(forward_demodulation,[],[f1203,f675]) ).
fof(f1215,plain,
( m1_subset_1(sF32,u1_struct_0(sK3))
| ~ v1_funct_1(sF31)
| ~ v1_funct_2(sF31,sF30,u1_struct_0(sK3))
| ~ m1_relset_1(sF31,sF30,u1_struct_0(sK3))
| ~ m1_subset_1(sK5,sF30)
| ~ spl37_1
| ~ spl37_3
| spl37_7
| spl37_9 ),
inference(forward_subsumption_resolution,[],[f1208,f694]) ).
fof(f1217,plain,
( ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
| ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
| r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,k2_waybel34(sK2,sK3,sK4),sK5),sF34)
| ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
| spl37_7
| ~ spl37_11
| ~ spl37_12 ),
inference(forward_demodulation,[],[f1210,f661]) ).
fof(f1218,plain,
( ~ v1_funct_2(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
| ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
| r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,k2_waybel34(sK2,sK3,sK4),sK5),sF34)
| spl37_7
| ~ spl37_11
| ~ spl37_12 ),
inference(duplicate_literal_removal,[],[f1217]) ).
fof(f1222,plain,
( m1_subset_1(sF32,u1_struct_0(sK3))
| ~ v1_funct_2(sF31,sF30,u1_struct_0(sK3))
| ~ m1_relset_1(sF31,sF30,u1_struct_0(sK3))
| ~ m1_subset_1(sK5,sF30)
| ~ spl37_1
| ~ spl37_3
| spl37_7
| spl37_9
| ~ spl37_12 ),
inference(forward_subsumption_resolution,[],[f1215,f800]) ).
fof(f1224,plain,
( ~ v1_funct_2(sF31,sF30,sF36)
| ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
| r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,k2_waybel34(sK2,sK3,sK4),sK5),sF34)
| spl37_7
| ~ spl37_11
| ~ spl37_12 ),
inference(forward_demodulation,[],[f1218,f663]) ).
fof(f1227,plain,
( m1_subset_1(sF32,u1_struct_0(sK3))
| ~ v1_funct_2(sF31,sF30,u1_struct_0(sK3))
| ~ m1_relset_1(sF31,sF30,u1_struct_0(sK3))
| ~ spl37_1
| ~ spl37_3
| spl37_7
| spl37_9
| ~ spl37_12 ),
inference(forward_subsumption_resolution,[],[f1222,f673]) ).
fof(f1229,plain,
( ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
| r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,k2_waybel34(sK2,sK3,sK4),sK5),sF34)
| spl37_7
| ~ spl37_11
| ~ spl37_12
| ~ spl37_15 ),
inference(forward_subsumption_resolution,[],[f1224,f811]) ).
fof(f1232,plain,
( m1_subset_1(sF32,sF36)
| ~ v1_funct_2(sF31,sF30,u1_struct_0(sK3))
| ~ m1_relset_1(sF31,sF30,u1_struct_0(sK3))
| ~ spl37_1
| ~ spl37_3
| spl37_7
| spl37_9
| ~ spl37_12 ),
inference(forward_demodulation,[],[f1227,f675]) ).
fof(f1234,plain,
( ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),u1_struct_0(sK2),sF36)
| ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
| r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,k2_waybel34(sK2,sK3,sK4),sK5),sF34)
| spl37_7
| ~ spl37_11
| ~ spl37_12
| ~ spl37_15 ),
inference(forward_demodulation,[],[f1229,f675]) ).
fof(f1237,plain,
( ~ v1_funct_2(sF31,sF30,sF36)
| m1_subset_1(sF32,sF36)
| ~ m1_relset_1(sF31,sF30,u1_struct_0(sK3))
| ~ spl37_1
| ~ spl37_3
| spl37_7
| spl37_9
| ~ spl37_12 ),
inference(forward_demodulation,[],[f1232,f675]) ).
fof(f1239,plain,
( ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
| ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
| r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,k2_waybel34(sK2,sK3,sK4),sK5),sF34)
| spl37_7
| ~ spl37_11
| ~ spl37_12
| ~ spl37_15 ),
inference(forward_demodulation,[],[f1234,f661]) ).
fof(f1240,plain,
( ~ m2_relset_1(k2_waybel34(sK2,sK3,sK4),sF30,sF36)
| ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,k2_waybel34(sK2,sK3,sK4),sK5),sF34)
| spl37_7
| ~ spl37_11
| ~ spl37_12
| ~ spl37_15 ),
inference(duplicate_literal_removal,[],[f1239]) ).
fof(f1247,definition,
( spl37_22
<=> r4_waybel_1(sK3,sF32,sF34) ),
introduced(definition,[new_symbols(definition,[spl37_22])],[avatar_definition]) ).
fof(f1249,plain,
( r4_waybel_1(sK3,sF32,sF34)
| ~ spl37_22 ),
inference(avatar_component_clause,[],[f1247]) ).
fof(f1251,plain,
( m1_subset_1(sF32,sF36)
| ~ m1_relset_1(sF31,sF30,u1_struct_0(sK3))
| ~ spl37_1
| ~ spl37_3
| spl37_7
| spl37_9
| ~ spl37_12
| ~ spl37_15 ),
inference(forward_subsumption_resolution,[],[f1237,f811]) ).
fof(f1253,plain,
( ~ m2_relset_1(sF31,sF30,sF36)
| ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,k2_waybel34(sK2,sK3,sK4),sK5),sF34)
| spl37_7
| ~ spl37_11
| ~ spl37_12
| ~ spl37_15 ),
inference(forward_demodulation,[],[f1240,f663]) ).
fof(f1255,plain,
( ~ m1_relset_1(sF31,sF30,sF36)
| m1_subset_1(sF32,sF36)
| ~ spl37_1
| ~ spl37_3
| spl37_7
| spl37_9
| ~ spl37_12
| ~ spl37_15 ),
inference(forward_demodulation,[],[f1251,f675]) ).
fof(f1257,plain,
( ~ v1_funct_2(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,k2_waybel34(sK2,sK3,sK4),sK5),sF34)
| spl37_7
| ~ spl37_11
| ~ spl37_12
| ~ spl37_13
| ~ spl37_15 ),
inference(forward_subsumption_resolution,[],[f1253,f804]) ).
fof(f1259,plain,
( m1_subset_1(sF32,sF36)
| ~ spl37_1
| ~ spl37_3
| spl37_7
| spl37_9
| ~ spl37_12
| ~ spl37_13
| ~ spl37_15 ),
inference(forward_subsumption_resolution,[],[f1255,f1003]) ).
fof(f1261,plain,
( ~ v1_funct_2(sK4,u1_struct_0(sK3),sF30)
| ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,k2_waybel34(sK2,sK3,sK4),sK5),sF34)
| spl37_7
| ~ spl37_11
| ~ spl37_12
| ~ spl37_13
| ~ spl37_15 ),
inference(forward_demodulation,[],[f1257,f661]) ).
fof(f1264,plain,
( ~ v1_funct_2(sK4,sF36,sF30)
| ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,k2_waybel34(sK2,sK3,sK4),sK5),sF34)
| spl37_7
| ~ spl37_11
| ~ spl37_12
| ~ spl37_13
| ~ spl37_15 ),
inference(forward_demodulation,[],[f1261,f675]) ).
fof(f1267,plain,
( ~ m2_relset_1(sK4,u1_struct_0(sK3),u1_struct_0(sK2))
| r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,k2_waybel34(sK2,sK3,sK4),sK5),sF34)
| spl37_7
| ~ spl37_11
| ~ spl37_12
| ~ spl37_13
| ~ spl37_15 ),
inference(forward_subsumption_resolution,[],[f1264,f676]) ).
fof(f1270,plain,
( ~ m2_relset_1(sK4,u1_struct_0(sK3),sF30)
| r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,k2_waybel34(sK2,sK3,sK4),sK5),sF34)
| spl37_7
| ~ spl37_11
| ~ spl37_12
| ~ spl37_13
| ~ spl37_15 ),
inference(forward_demodulation,[],[f1267,f661]) ).
fof(f1273,plain,
( ~ m2_relset_1(sK4,sF36,sF30)
| r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,k2_waybel34(sK2,sK3,sK4),sK5),sF34)
| spl37_7
| ~ spl37_11
| ~ spl37_12
| ~ spl37_13
| ~ spl37_15 ),
inference(forward_demodulation,[],[f1270,f675]) ).
fof(f1276,plain,
( r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,k2_waybel34(sK2,sK3,sK4),sK5),sF34)
| spl37_7
| ~ spl37_11
| ~ spl37_12
| ~ spl37_13
| ~ spl37_15 ),
inference(forward_subsumption_resolution,[],[f1273,f677]) ).
fof(f1278,plain,
( r4_waybel_1(sK3,k7_yellow_2(sF30,sK3,sF31,sK5),sF34)
| spl37_7
| ~ spl37_11
| ~ spl37_12
| ~ spl37_13
| ~ spl37_15 ),
inference(forward_demodulation,[],[f1276,f663]) ).
fof(f1280,plain,
( r4_waybel_1(sK3,sF32,sF34)
| spl37_7
| ~ spl37_11
| ~ spl37_12
| ~ spl37_13
| ~ spl37_15 ),
inference(forward_demodulation,[],[f1278,f665]) ).
fof(f1282,plain,
( spl37_22
| spl37_7
| ~ spl37_11
| ~ spl37_12
| ~ spl37_13
| ~ spl37_15 ),
inference(avatar_split_clause,[],[f1280,f810,f803,f799,f755,f733,f1247]) ).
fof(f1295,plain,
( sF32 = k1_yellow_0(sK3,sF34)
| ~ m1_subset_1(sF32,u1_struct_0(sK3))
| v3_struct_0(sK3)
| ~ l1_orders_2(sK3)
| ~ spl37_22 ),
inference(resolution,[],[f1249,f491]) ).
fof(f1296,plain,
( sF32 = k1_yellow_0(sK3,sF34)
| ~ m1_subset_1(sF32,u1_struct_0(sK3))
| ~ l1_orders_2(sK3)
| spl37_7
| ~ spl37_22 ),
inference(forward_subsumption_resolution,[],[f1295,f734]) ).
fof(f1297,plain,
( sF32 = k1_yellow_0(sK3,sF34)
| ~ m1_subset_1(sF32,u1_struct_0(sK3))
| spl37_7
| ~ spl37_22 ),
inference(forward_subsumption_resolution,[],[f1296,f353]) ).
fof(f1298,plain,
( sF32 = sF35
| ~ m1_subset_1(sF32,u1_struct_0(sK3))
| spl37_7
| ~ spl37_22 ),
inference(forward_demodulation,[],[f1297,f671]) ).
fof(f1299,plain,
( ~ m1_subset_1(sF32,u1_struct_0(sK3))
| spl37_7
| ~ spl37_22 ),
inference(forward_subsumption_resolution,[],[f1298,f672]) ).
fof(f1300,plain,
( ~ m1_subset_1(sF32,sF36)
| spl37_7
| ~ spl37_22 ),
inference(forward_demodulation,[],[f1299,f675]) ).
fof(f1301,plain,
( $false
| ~ spl37_1
| ~ spl37_3
| spl37_7
| spl37_9
| ~ spl37_12
| ~ spl37_13
| ~ spl37_15
| ~ spl37_22 ),
inference(forward_subsumption_resolution,[],[f1300,f1259]) ).
fof(f1302,plain,
( ~ spl37_1
| ~ spl37_3
| spl37_7
| spl37_9
| ~ spl37_12
| ~ spl37_13
| ~ spl37_15
| ~ spl37_22 ),
inference(avatar_contradiction_clause,[],[f1301]) ).
cnf(s7,plain,
( spl37_9
| spl37_11 ),
inference(sat_conversion,[],[f757]) ).
cnf(s8,plain,
~ spl37_9,
inference(sat_conversion,[],[f772]) ).
cnf(s9,plain,
~ spl37_7,
inference(sat_conversion,[],[f774]) ).
cnf(s11,plain,
spl37_3,
inference(sat_conversion,[],[f829]) ).
cnf(s12,plain,
spl37_1,
inference(sat_conversion,[],[f831]) ).
cnf(s14,plain,
spl37_13,
inference(sat_conversion,[],[f1002]) ).
cnf(s17,plain,
spl37_15,
inference(sat_conversion,[],[f1158]) ).
cnf(s18,plain,
spl37_12,
inference(sat_conversion,[],[f1200]) ).
cnf(s20,plain,
( spl37_7
| ~ spl37_11
| ~ spl37_12
| ~ spl37_13
| ~ spl37_15
| spl37_22 ),
inference(sat_conversion,[],[f1282]) ).
cnf(s22,plain,
( ~ spl37_1
| ~ spl37_3
| spl37_7
| spl37_9
| ~ spl37_12
| ~ spl37_13
| ~ spl37_15
| ~ spl37_22 ),
inference(sat_conversion,[],[f1302]) ).
cnf(s27,plain,
~ spl37_22,
inference(rat,[],[s22,s9,s17,s14,s18,s11,s12,s8]) ).
cnf(s29,plain,
~ spl37_11,
inference(rat,[],[s20,s9,s17,s14,s18,s27]) ).
cnf(s30,plain,
$false,
inference(rat,[],[s7,s29,s8]) ).
fof(f1303,plain,
$false,
inference(avatar_sat_refutation,[],[s30]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT353+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.37 % Computer : n020.cluster.edu
% 0.08/0.37 % Model : x86_64 x86_64
% 0.08/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.37 % Memory : 8046.5625MB
% 0.08/0.37 % OS : Linux 6.8.0-71-generic
% 0.08/0.37 % CPULimit : 300
% 0.08/0.37 % WCLimit : 300
% 0.08/0.37 % DateTime : Sun Sep 27 14:57:19 UTC 2026
% 0.08/0.37 % CPUTime :
% 0.08/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.40 Running first-order theorem proving
% 0.08/0.40 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.36/1.57 % (3466850)Detected formulas, will run a generic FOF schedule.
% 4.36/1.57 % (3466855)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=2950211008:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 4.36/1.57 % (3466860)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=14399906:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 4.36/1.57 % (3466858)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=4238003522:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 4.36/1.57 % (3466857)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=3467670301:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 4.36/1.57 % (3466856)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=3209232613:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 4.36/1.57 % (3466859)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1225087402:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 4.36/1.57 % (3466858)Refutation not found, incomplete strategy
% 4.36/1.57 % (3466858)------------------------------
% 4.36/1.57 % (3466858)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.36/1.57 % (3466858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.36/1.57 % (3466858)CaDiCaL version: 2.1.3
% 4.36/1.57 % (3466858)Termination reason: Refutation not found, incomplete strategy
% 4.36/1.57 % (3466858)Time elapsed: 0.004 s
% 4.36/1.57 % (3466858)Peak memory usage: 88 MB
% 4.36/1.57 % (3466858)Instructions burned: 4 (million)
% 4.36/1.57 % (3466859)Refutation not found, incomplete strategy
% 4.36/1.57 % (3466859)------------------------------
% 4.36/1.57 % (3466859)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.36/1.57 % (3466859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.36/1.57 % (3466859)CaDiCaL version: 2.1.3
% 4.36/1.57 % (3466859)Termination reason: Refutation not found, incomplete strategy
% 4.36/1.57 % (3466859)Time elapsed: 0.004 s
% 4.36/1.57 % (3466859)Peak memory usage: 88 MB
% 4.36/1.57 % (3466859)Instructions burned: 5 (million)
% 4.36/1.57 % (3466861)dis-21_1_sil=8000:lcm=predicate:random_seed=262104357:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 4.36/1.57 % (3466861)Instruction limit reached!
% 4.36/1.57 % (3466861)------------------------------
% 4.36/1.57 % (3466861)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.36/1.57 % (3466861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.36/1.57 % (3466861)CaDiCaL version: 2.1.3
% 4.36/1.57 % (3466861)Termination reason: Instruction limit
% 4.36/1.57 % (3466861)Termination phase: Saturation
% 4.36/1.57 % (3466861)Time elapsed: 0.070 s
% 4.36/1.57 % (3466861)Peak memory usage: 91 MB
% 4.36/1.57 % (3466861)Instructions burned: 129 (million)
% 4.36/1.57 % (3466860)Instruction limit reached!
% 4.36/1.57 % (3466860)------------------------------
% 4.36/1.57 % (3466860)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.36/1.57 % (3466860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.36/1.57 % (3466860)CaDiCaL version: 2.1.3
% 4.36/1.57 % (3466860)Termination reason: Instruction limit
% 4.36/1.57 % (3466860)Termination phase: Saturation
% 4.36/1.57 % (3466860)Time elapsed: 0.091 s
% 4.36/1.57 % (3466860)Peak memory usage: 90 MB
% 4.36/1.57 % (3466860)Instructions burned: 141 (million)
% 4.36/1.57 % (3466869)lrs+10_1_sil=8000:sp=occurrence:random_seed=4096087727:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 4.36/1.57 % (3466870)lrs+10_1_sil=32000:urr=on:br=off:random_seed=915626559:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 4.36/1.57 % (3466858)------------------------------
% 4.36/1.57 % (3466858)------------------------------
% 4.36/1.57 % (3466859)------------------------------
% 4.36/1.57 % (3466859)------------------------------
% 4.36/1.57 % (3466870)Instruction limit reached!
% 4.36/1.57 % (3466870)------------------------------
% 4.36/1.57 % (3466870)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.36/1.57 % (3466870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.36/1.57 % (3466870)CaDiCaL version: 2.1.3
% 4.36/1.57 % (3466870)Termination reason: Instruction limit
% 4.36/1.57 % (3466870)Termination phase: Saturation
% 4.36/1.57 % (3466870)Time elapsed: 0.082 s
% 4.36/1.57 % (3466870)Peak memory usage: 89 MB
% 4.36/1.57 % (3466870)Instructions burned: 157 (million)
% 4.36/1.57 % (3466855)First to succeed.
% 4.36/1.57 % (3466855)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3466850"
% 4.36/1.57 % (3466869)Instruction limit reached!
% 4.36/1.57 % (3466869)------------------------------
% 4.36/1.57 % (3466869)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.36/1.57 % (3466869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.36/1.57 % (3466869)CaDiCaL version: 2.1.3
% 4.36/1.57 % (3466869)Termination reason: Instruction limit
% 4.36/1.57 % (3466869)Termination phase: Saturation
% 4.36/1.57 % (3466869)Time elapsed: 0.159 s
% 4.36/1.57 % (3466869)Peak memory usage: 91 MB
% 4.36/1.57 % (3466869)Instructions burned: 287 (million)
% 4.36/1.57 % (3466874)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=1285680190:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 4.36/1.57 % (3466873)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3656984840:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 4.36/1.57 % (3466875)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2817551942:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 4.36/1.57 % (3466875)Refutation not found, incomplete strategy
% 4.36/1.57 % (3466875)------------------------------
% 4.36/1.57 % (3466875)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.36/1.57 % (3466875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.36/1.57 % (3466875)CaDiCaL version: 2.1.3
% 4.36/1.57 % (3466875)Termination reason: Refutation not found, incomplete strategy
% 4.36/1.57 % (3466875)Time elapsed: 0.011 s
% 4.36/1.57 % (3466875)Peak memory usage: 89 MB
% 4.36/1.57 % (3466875)Instructions burned: 18 (million)
% 4.36/1.57 % (3466855)Refutation found. Thanks to Tanya!
% 4.36/1.57 % SZS status Theorem for theBenchmark
% 4.36/1.57 % SZS output start Proof for theBenchmark
% See solution above
% 5.59/1.77 % (3466855)------------------------------
% 5.59/1.77 % (3466855)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.59/1.77 % (3466855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.59/1.77 % (3466855)CaDiCaL version: 2.1.3
% 5.59/1.77 % (3466855)Termination reason: Refutation
% 5.59/1.77 % (3466855)Time elapsed: 0.405 s
% 5.59/1.77 % (3466855)Peak memory usage: 133 MB
% 5.59/1.77 % (3466855)Instructions burned: 1112 (million)
% 5.59/1.77 % (3466855)------------------------------
% 5.59/1.77 % (3466855)------------------------------
% 5.59/1.77 % (3466850)Success in time 0.727 s
% 5.59/1.77 % Vampire exiting
%------------------------------------------------------------------------------