%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT352+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 : n007.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:12 AM UTC 2026
% Result : Theorem 8.11s 2.10s
% Output : Refutation 8.77s
% Verified :
% SZS Type : Refutation
% Derivation depth : 56
% Number of leaves : 26
% Syntax : Number of formulae : 293 ( 61 unt; 16 def)
% Number of atoms : 2191 ( 39 equ)
% Maximal formula atoms : 26 ( 7 avg)
% Number of connectives : 3506 (1608 ~;1681 |; 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 : 231 ( 0 sgn 220 !; 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(X0),u1_struct_0(X1))
& v17_waybel_0(X2,X0,X1)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X1))
=> k7_yellow_2(u1_struct_0(X1),X0,k1_waybel34(X0,X1,X2),X3) = k2_yellow_0(X0,k5_pre_topc(X0,X1,X2,k7_waybel_0(X1,X3))) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2_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(X0),u1_struct_0(X1))
& v17_waybel_0(X2,X0,X1)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X1))
=> k7_yellow_2(u1_struct_0(X1),X0,k1_waybel34(X0,X1,X2),X3) = k2_yellow_0(X0,k5_pre_topc(X0,X1,X2,k7_waybel_0(X1,X3))) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f32,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(X0),u1_struct_0(X1))
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> ( ( v3_lattice3(X0)
& v3_lattice3(X1)
& v17_waybel_0(X2,X0,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)) )
=> ( X3 = k1_waybel34(X0,X1,X2)
<=> v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d1_waybel34) ).
fof(f47,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( r3_waybel_1(X0,X1,X2)
<=> ( r2_yellow_0(X0,X2)
& X1 = k2_yellow_0(X0,X2)
& r2_hidden(k2_yellow_0(X0,X2),X2) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d6_waybel_1) ).
fof(f52,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(X0),u1_struct_0(X1))
& m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> ( v1_funct_1(k1_waybel34(X0,X1,X2))
& v1_funct_2(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0))
& m2_relset_1(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k1_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(f90,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(f121,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(f123,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(X2,X0,X1)
& ! [X4] :
( m1_subset_1(X4,u1_struct_0(X1))
=> r3_waybel_1(X0,k7_yellow_2(u1_struct_0(X1),X0,X3,X4),k5_pre_topc(X0,X1,X2,k7_waybel_0(X1,X4))) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t11_waybel_1) ).
fof(f156,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( k7_yellow_2(u1_struct_0(X1),X0,k1_waybel34(X0,X1,X2),X3) != k2_yellow_0(X0,k5_pre_topc(X0,X1,X2,k7_waybel_0(X1,X3)))
& m1_subset_1(X3,u1_struct_0(X1)) )
& v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v17_waybel_0(X2,X0,X1)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
& v2_orders_2(X1)
& v3_orders_2(X1)
& v4_orders_2(X1)
& v1_lattice3(X1)
& v2_lattice3(X1)
& v3_lattice3(X1)
& l1_orders_2(X1) )
& v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& v2_lattice3(X0)
& v3_lattice3(X0)
& l1_orders_2(X0) ),
inference(ennf_transformation,[],[f2]) ).
fof(f157,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( k7_yellow_2(u1_struct_0(X1),X0,k1_waybel34(X0,X1,X2),X3) != k2_yellow_0(X0,k5_pre_topc(X0,X1,X2,k7_waybel_0(X1,X3)))
& m1_subset_1(X3,u1_struct_0(X1)) )
& v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v17_waybel_0(X2,X0,X1)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
& v2_orders_2(X1)
& v3_orders_2(X1)
& v4_orders_2(X1)
& v1_lattice3(X1)
& v2_lattice3(X1)
& v3_lattice3(X1)
& l1_orders_2(X1) )
& v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& v2_lattice3(X0)
& v3_lattice3(X0)
& l1_orders_2(X0) ),
inference(flattening,[],[f156]) ).
fof(f199,plain,
! [X0] :
( ~ v3_struct_0(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f32]) ).
fof(f200,plain,
! [X0] :
( ~ v3_struct_0(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f199]) ).
fof(f220,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( X3 = k1_waybel34(X0,X1,X2)
<=> 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)) )
| ~ v3_lattice3(X0)
| ~ v3_lattice3(X1)
| ~ v17_waybel_0(X2,X0,X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| ~ 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(f221,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( X3 = k1_waybel34(X0,X1,X2)
<=> 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)) )
| ~ v3_lattice3(X0)
| ~ v3_lattice3(X1)
| ~ v17_waybel_0(X2,X0,X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| ~ 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,[],[f220]) ).
fof(f222,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( r3_waybel_1(X0,X1,X2)
<=> ( r2_yellow_0(X0,X2)
& X1 = k2_yellow_0(X0,X2)
& r2_hidden(k2_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(f223,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( r3_waybel_1(X0,X1,X2)
<=> ( r2_yellow_0(X0,X2)
& X1 = k2_yellow_0(X0,X2)
& r2_hidden(k2_yellow_0(X0,X2),X2) ) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f222]) ).
fof(f226,plain,
! [X0,X1,X2] :
( ( v1_funct_1(k1_waybel34(X0,X1,X2))
& v1_funct_2(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0))
& m2_relset_1(k1_waybel34(X0,X1,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(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(ennf_transformation,[],[f52]) ).
fof(f227,plain,
! [X0,X1,X2] :
( ( v1_funct_1(k1_waybel34(X0,X1,X2))
& v1_funct_2(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0))
& m2_relset_1(k1_waybel34(X0,X1,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(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(flattening,[],[f226]) ).
fof(f235,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(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(flattening,[],[f235]) ).
fof(f237,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f64]) ).
fof(f257,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f90]) ).
fof(f258,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(flattening,[],[f257]) ).
fof(f293,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1)
<=> ( v5_orders_3(X2,X0,X1)
& ! [X4] :
( r3_waybel_1(X0,k7_yellow_2(u1_struct_0(X1),X0,X3,X4),k5_pre_topc(X0,X1,X2,k7_waybel_0(X1,X4)))
| ~ m1_subset_1(X4,u1_struct_0(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(ennf_transformation,[],[f123]) ).
fof(f294,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1)
<=> ( v5_orders_3(X2,X0,X1)
& ! [X4] :
( r3_waybel_1(X0,k7_yellow_2(u1_struct_0(X1),X0,X3,X4),k5_pre_topc(X0,X1,X2,k7_waybel_0(X1,X4)))
| ~ m1_subset_1(X4,u1_struct_0(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,[],[f293]) ).
fof(f309,plain,
( k7_yellow_2(u1_struct_0(sK3),sK2,k1_waybel34(sK2,sK3,sK4),sK5) != k2_yellow_0(sK2,k5_pre_topc(sK2,sK3,sK4,k7_waybel_0(sK3,sK5)))
& m1_subset_1(sK5,u1_struct_0(sK3))
& v1_funct_1(sK4)
& v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
& v17_waybel_0(sK4,sK2,sK3)
& m2_relset_1(sK4,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)
& 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)],[f157]) ).
fof(f312,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( ( X3 = k1_waybel34(X0,X1,X2)
| ~ v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1) )
& ( v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1)
| k1_waybel34(X0,X1,X2) != 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_lattice3(X0)
| ~ v3_lattice3(X1)
| ~ v17_waybel_0(X2,X0,X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| ~ 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,[],[f221]) ).
fof(f313,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( r3_waybel_1(X0,X1,X2)
| ~ r2_yellow_0(X0,X2)
| k2_yellow_0(X0,X2) != X1
| ~ r2_hidden(k2_yellow_0(X0,X2),X2) )
& ( ( r2_yellow_0(X0,X2)
& X1 = k2_yellow_0(X0,X2)
& r2_hidden(k2_yellow_0(X0,X2),X2) )
| ~ r3_waybel_1(X0,X1,X2) ) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(nnf_transformation,[],[f223]) ).
fof(f314,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( r3_waybel_1(X0,X1,X2)
| ~ r2_yellow_0(X0,X2)
| k2_yellow_0(X0,X2) != X1
| ~ r2_hidden(k2_yellow_0(X0,X2),X2) )
& ( ( r2_yellow_0(X0,X2)
& X1 = k2_yellow_0(X0,X2)
& r2_hidden(k2_yellow_0(X0,X2),X2) )
| ~ r3_waybel_1(X0,X1,X2) ) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f313]) ).
fof(f337,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,[],[f121]) ).
fof(f338,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( ( v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1)
| ~ v5_orders_3(X2,X0,X1)
| ? [X4] :
( ~ r3_waybel_1(X0,k7_yellow_2(u1_struct_0(X1),X0,X3,X4),k5_pre_topc(X0,X1,X2,k7_waybel_0(X1,X4)))
& m1_subset_1(X4,u1_struct_0(X1)) ) )
& ( ( v5_orders_3(X2,X0,X1)
& ! [X4] :
( r3_waybel_1(X0,k7_yellow_2(u1_struct_0(X1),X0,X3,X4),k5_pre_topc(X0,X1,X2,k7_waybel_0(X1,X4)))
| ~ m1_subset_1(X4,u1_struct_0(X1)) ) )
| ~ 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,[],[f294]) ).
fof(f339,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( ( v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1)
| ~ v5_orders_3(X2,X0,X1)
| ? [X4] :
( ~ r3_waybel_1(X0,k7_yellow_2(u1_struct_0(X1),X0,X3,X4),k5_pre_topc(X0,X1,X2,k7_waybel_0(X1,X4)))
& m1_subset_1(X4,u1_struct_0(X1)) ) )
& ( ( v5_orders_3(X2,X0,X1)
& ! [X4] :
( r3_waybel_1(X0,k7_yellow_2(u1_struct_0(X1),X0,X3,X4),k5_pre_topc(X0,X1,X2,k7_waybel_0(X1,X4)))
| ~ m1_subset_1(X4,u1_struct_0(X1)) ) )
| ~ 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,[],[f338]) ).
fof(f340,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( ( v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1)
| ~ v5_orders_3(X2,X0,X1)
| ? [X4] :
( ~ r3_waybel_1(X0,k7_yellow_2(u1_struct_0(X1),X0,X3,X4),k5_pre_topc(X0,X1,X2,k7_waybel_0(X1,X4)))
& m1_subset_1(X4,u1_struct_0(X1)) ) )
& ( ( v5_orders_3(X2,X0,X1)
& ! [X5] :
( r3_waybel_1(X0,k7_yellow_2(u1_struct_0(X1),X0,X3,X5),k5_pre_topc(X0,X1,X2,k7_waybel_0(X1,X5)))
| ~ m1_subset_1(X5,u1_struct_0(X1)) ) )
| ~ 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,[],[f339]) ).
fof(f341,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( ( v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1)
| ~ v5_orders_3(X2,X0,X1)
| ( ~ r3_waybel_1(X0,k7_yellow_2(u1_struct_0(X1),X0,X3,sK28(X0,X1,X2,X3)),k5_pre_topc(X0,X1,X2,k7_waybel_0(X1,sK28(X0,X1,X2,X3))))
& m1_subset_1(sK28(X0,X1,X2,X3),u1_struct_0(X1)) ) )
& ( ( v5_orders_3(X2,X0,X1)
& ! [X5] :
( r3_waybel_1(X0,k7_yellow_2(u1_struct_0(X1),X0,X3,X5),k5_pre_topc(X0,X1,X2,k7_waybel_0(X1,X5)))
| ~ m1_subset_1(X5,u1_struct_0(X1)) ) )
| ~ 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,[sK28]),skolemize(X4,sK28(X0,X1,X2,X3))],[f340]) ).
fof(f342,plain,
l1_orders_2(sK2),
inference(cnf_transformation,[],[f309]) ).
fof(f343,plain,
v3_lattice3(sK2),
inference(cnf_transformation,[],[f309]) ).
fof(f344,plain,
v2_lattice3(sK2),
inference(cnf_transformation,[],[f309]) ).
fof(f345,plain,
v1_lattice3(sK2),
inference(cnf_transformation,[],[f309]) ).
fof(f346,plain,
v4_orders_2(sK2),
inference(cnf_transformation,[],[f309]) ).
fof(f347,plain,
v3_orders_2(sK2),
inference(cnf_transformation,[],[f309]) ).
fof(f348,plain,
v2_orders_2(sK2),
inference(cnf_transformation,[],[f309]) ).
fof(f349,plain,
l1_orders_2(sK3),
inference(cnf_transformation,[],[f309]) ).
fof(f350,plain,
v3_lattice3(sK3),
inference(cnf_transformation,[],[f309]) ).
fof(f351,plain,
v2_lattice3(sK3),
inference(cnf_transformation,[],[f309]) ).
fof(f352,plain,
v1_lattice3(sK3),
inference(cnf_transformation,[],[f309]) ).
fof(f353,plain,
v4_orders_2(sK3),
inference(cnf_transformation,[],[f309]) ).
fof(f354,plain,
v3_orders_2(sK3),
inference(cnf_transformation,[],[f309]) ).
fof(f355,plain,
v2_orders_2(sK3),
inference(cnf_transformation,[],[f309]) ).
fof(f356,plain,
m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)),
inference(cnf_transformation,[],[f309]) ).
fof(f357,plain,
v17_waybel_0(sK4,sK2,sK3),
inference(cnf_transformation,[],[f309]) ).
fof(f358,plain,
v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3)),
inference(cnf_transformation,[],[f309]) ).
fof(f359,plain,
v1_funct_1(sK4),
inference(cnf_transformation,[],[f309]) ).
fof(f360,plain,
m1_subset_1(sK5,u1_struct_0(sK3)),
inference(cnf_transformation,[],[f309]) ).
fof(f361,plain,
k7_yellow_2(u1_struct_0(sK3),sK2,k1_waybel34(sK2,sK3,sK4),sK5) != k2_yellow_0(sK2,k5_pre_topc(sK2,sK3,sK4,k7_waybel_0(sK3,sK5))),
inference(cnf_transformation,[],[f309]) ).
fof(f457,plain,
! [X0] :
( ~ v3_struct_0(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f200]) ).
fof(f483,plain,
! [X2,X3,X0,X1] :
( v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1)
| k1_waybel34(X0,X1,X2) != 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_lattice3(X0)
| ~ v3_lattice3(X1)
| ~ v17_waybel_0(X2,X0,X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ 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,[],[f312]) ).
fof(f487,plain,
! [X2,X0,X1] :
( ~ r3_waybel_1(X0,X1,X2)
| k2_yellow_0(X0,X2) = X1
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f314]) ).
fof(f491,plain,
! [X2,X0,X1] :
( m2_relset_1(k1_waybel34(X0,X1,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(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f227]) ).
fof(f492,plain,
! [X2,X0,X1] :
( v1_funct_2(k1_waybel34(X0,X1,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(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f227]) ).
fof(f493,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(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(X0),u1_struct_0(X1))
| v1_funct_1(k1_waybel34(X0,X1,X2)) ),
inference(cnf_transformation,[],[f227]) ).
fof(f498,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,[],[f236]) ).
fof(f499,plain,
! [X0] :
( ~ l1_orders_2(X0)
| l1_struct_0(X0) ),
inference(cnf_transformation,[],[f237]) ).
fof(f536,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[],[f258]) ).
fof(f634,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f337]) ).
fof(f637,plain,
! [X2,X3,X0,X1,X5] :
( r3_waybel_1(X0,k7_yellow_2(u1_struct_0(X1),X0,X3,X5),k5_pre_topc(X0,X1,X2,k7_waybel_0(X1,X5)))
| ~ m1_subset_1(X5,u1_struct_0(X1))
| ~ 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,[],[f341]) ).
fof(f650,plain,
! [X2,X0,X1] :
( v3_waybel_1(k1_waybel_1(X0,X1,X2,k1_waybel34(X0,X1,X2)),X0,X1)
| ~ v1_funct_1(k1_waybel34(X0,X1,X2))
| ~ v1_funct_2(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0))
| ~ m2_relset_1(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0))
| ~ v3_lattice3(X0)
| ~ v3_lattice3(X1)
| ~ v17_waybel_0(X2,X0,X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ 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,[],[f483]) ).
fof(f652,definition,
sF29 = u1_struct_0(sK3),
introduced(definition,[new_symbols(definition,[sF29])],[function_definition]) ).
fof(f653,plain,
u1_struct_0(sK3) = sF29,
inference(reorient_equations,[],[f652]) ).
fof(f654,definition,
sF30 = k1_waybel34(sK2,sK3,sK4),
introduced(definition,[new_symbols(definition,[sF30])],[function_definition]) ).
fof(f655,plain,
k1_waybel34(sK2,sK3,sK4) = sF30,
inference(reorient_equations,[],[f654]) ).
fof(f656,definition,
sF31 = k7_yellow_2(sF29,sK2,sF30,sK5),
introduced(definition,[new_symbols(definition,[sF31])],[function_definition]) ).
fof(f657,plain,
k7_yellow_2(sF29,sK2,sF30,sK5) = sF31,
inference(reorient_equations,[],[f656]) ).
fof(f658,definition,
sF32 = k7_waybel_0(sK3,sK5),
introduced(definition,[new_symbols(definition,[sF32])],[function_definition]) ).
fof(f659,plain,
k7_waybel_0(sK3,sK5) = sF32,
inference(reorient_equations,[],[f658]) ).
fof(f660,definition,
sF33 = k5_pre_topc(sK2,sK3,sK4,sF32),
introduced(definition,[new_symbols(definition,[sF33])],[function_definition]) ).
fof(f661,plain,
k5_pre_topc(sK2,sK3,sK4,sF32) = sF33,
inference(reorient_equations,[],[f660]) ).
fof(f662,definition,
sF34 = k2_yellow_0(sK2,sF33),
introduced(definition,[new_symbols(definition,[sF34])],[function_definition]) ).
fof(f663,plain,
k2_yellow_0(sK2,sF33) = sF34,
inference(reorient_equations,[],[f662]) ).
fof(f664,plain,
sF31 != sF34,
inference(definition_folding,[],[f361,f663,f661,f659,f657,f655,f653]) ).
fof(f665,plain,
m1_subset_1(sK5,sF29),
inference(definition_folding,[],[f360,f653]) ).
fof(f666,definition,
sF35 = u1_struct_0(sK2),
introduced(definition,[new_symbols(definition,[sF35])],[function_definition]) ).
fof(f667,plain,
u1_struct_0(sK2) = sF35,
inference(reorient_equations,[],[f666]) ).
fof(f668,plain,
v1_funct_2(sK4,sF35,sF29),
inference(definition_folding,[],[f358,f653,f667]) ).
fof(f669,plain,
m2_relset_1(sK4,sF35,sF29),
inference(definition_folding,[],[f356,f653,f667]) ).
fof(f672,plain,
m1_relset_1(sK4,sF35,sF29),
inference(resolution,[],[f634,f669]) ).
fof(f675,plain,
! [X2,X0,X1] :
( r3_waybel_1(X0,k7_yellow_2(u1_struct_0(sK3),X0,X1,sK5),k5_pre_topc(X0,sK3,X2,sF32))
| ~ m1_subset_1(sK5,u1_struct_0(sK3))
| ~ v3_waybel_1(k1_waybel_1(X0,sK3,X2,X1),X0,sK3)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK3),u1_struct_0(X0))
| ~ m2_relset_1(X1,u1_struct_0(sK3),u1_struct_0(X0))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(sK3))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(sK3))
| v3_struct_0(sK3)
| ~ v2_orders_2(sK3)
| ~ v3_orders_2(sK3)
| ~ v4_orders_2(sK3)
| ~ l1_orders_2(sK3)
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(superposition,[],[f637,f659]) ).
fof(f676,plain,
! [X2,X0,X1] :
( r3_waybel_1(X0,k7_yellow_2(u1_struct_0(sK3),X0,X1,sK5),k5_pre_topc(X0,sK3,X2,sF32))
| ~ m1_subset_1(sK5,u1_struct_0(sK3))
| ~ v3_waybel_1(k1_waybel_1(X0,sK3,X2,X1),X0,sK3)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK3),u1_struct_0(X0))
| ~ m2_relset_1(X1,u1_struct_0(sK3),u1_struct_0(X0))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(sK3))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(sK3))
| v3_struct_0(sK3)
| ~ v3_orders_2(sK3)
| ~ v4_orders_2(sK3)
| ~ l1_orders_2(sK3)
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(forward_subsumption_resolution,[],[f675,f355]) ).
fof(f679,plain,
! [X2,X0,X1] :
( r3_waybel_1(X0,k7_yellow_2(u1_struct_0(sK3),X0,X1,sK5),k5_pre_topc(X0,sK3,X2,sF32))
| ~ m1_subset_1(sK5,u1_struct_0(sK3))
| ~ v3_waybel_1(k1_waybel_1(X0,sK3,X2,X1),X0,sK3)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK3),u1_struct_0(X0))
| ~ m2_relset_1(X1,u1_struct_0(sK3),u1_struct_0(X0))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(sK3))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(sK3))
| v3_struct_0(sK3)
| ~ v4_orders_2(sK3)
| ~ l1_orders_2(sK3)
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(forward_subsumption_resolution,[],[f676,f354]) ).
fof(f682,plain,
! [X2,X0,X1] :
( r3_waybel_1(X0,k7_yellow_2(u1_struct_0(sK3),X0,X1,sK5),k5_pre_topc(X0,sK3,X2,sF32))
| ~ m1_subset_1(sK5,u1_struct_0(sK3))
| ~ v3_waybel_1(k1_waybel_1(X0,sK3,X2,X1),X0,sK3)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK3),u1_struct_0(X0))
| ~ m2_relset_1(X1,u1_struct_0(sK3),u1_struct_0(X0))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(sK3))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(sK3))
| v3_struct_0(sK3)
| ~ l1_orders_2(sK3)
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(forward_subsumption_resolution,[],[f679,f353]) ).
fof(f685,plain,
! [X2,X0,X1] :
( r3_waybel_1(X0,k7_yellow_2(u1_struct_0(sK3),X0,X1,sK5),k5_pre_topc(X0,sK3,X2,sF32))
| ~ m1_subset_1(sK5,u1_struct_0(sK3))
| ~ v3_waybel_1(k1_waybel_1(X0,sK3,X2,X1),X0,sK3)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK3),u1_struct_0(X0))
| ~ m2_relset_1(X1,u1_struct_0(sK3),u1_struct_0(X0))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(sK3))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(sK3))
| v3_struct_0(sK3)
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(forward_subsumption_resolution,[],[f682,f349]) ).
fof(f688,plain,
! [X2,X0,X1] :
( r3_waybel_1(X0,k7_yellow_2(sF29,X0,X1,sK5),k5_pre_topc(X0,sK3,X2,sF32))
| ~ m1_subset_1(sK5,u1_struct_0(sK3))
| ~ v3_waybel_1(k1_waybel_1(X0,sK3,X2,X1),X0,sK3)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK3),u1_struct_0(X0))
| ~ m2_relset_1(X1,u1_struct_0(sK3),u1_struct_0(X0))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(sK3))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(sK3))
| v3_struct_0(sK3)
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(forward_demodulation,[],[f685,f653]) ).
fof(f690,definition,
( spl36_1
<=> v3_struct_0(sK2) ),
introduced(definition,[new_symbols(definition,[spl36_1])],[avatar_definition]) ).
fof(f691,plain,
( ~ v3_struct_0(sK2)
| spl36_1 ),
inference(avatar_component_clause,[],[f690]) ).
fof(f692,plain,
( v3_struct_0(sK2)
| ~ spl36_1 ),
inference(avatar_component_clause,[],[f690]) ).
fof(f698,definition,
( spl36_3
<=> v3_struct_0(sK3) ),
introduced(definition,[new_symbols(definition,[spl36_3])],[avatar_definition]) ).
fof(f699,plain,
( ~ v3_struct_0(sK3)
| spl36_3 ),
inference(avatar_component_clause,[],[f698]) ).
fof(f700,plain,
( v3_struct_0(sK3)
| ~ spl36_3 ),
inference(avatar_component_clause,[],[f698]) ).
fof(f705,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(sK5,sF29)
| r3_waybel_1(X0,k7_yellow_2(sF29,X0,X1,sK5),k5_pre_topc(X0,sK3,X2,sF32))
| ~ v3_waybel_1(k1_waybel_1(X0,sK3,X2,X1),X0,sK3)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK3),u1_struct_0(X0))
| ~ m2_relset_1(X1,u1_struct_0(sK3),u1_struct_0(X0))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(sK3))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(sK3))
| v3_struct_0(sK3)
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(forward_demodulation,[],[f688,f653]) ).
fof(f706,plain,
! [X2,X0,X1] :
( r3_waybel_1(X0,k7_yellow_2(sF29,X0,X1,sK5),k5_pre_topc(X0,sK3,X2,sF32))
| ~ v3_waybel_1(k1_waybel_1(X0,sK3,X2,X1),X0,sK3)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK3),u1_struct_0(X0))
| ~ m2_relset_1(X1,u1_struct_0(sK3),u1_struct_0(X0))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(sK3))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(sK3))
| v3_struct_0(sK3)
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(forward_subsumption_resolution,[],[f705,f665]) ).
fof(f707,plain,
! [X2,X0,X1] :
( ~ v1_funct_2(X1,sF29,u1_struct_0(X0))
| r3_waybel_1(X0,k7_yellow_2(sF29,X0,X1,sK5),k5_pre_topc(X0,sK3,X2,sF32))
| ~ v3_waybel_1(k1_waybel_1(X0,sK3,X2,X1),X0,sK3)
| ~ v1_funct_1(X1)
| ~ m2_relset_1(X1,u1_struct_0(sK3),u1_struct_0(X0))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(sK3))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(sK3))
| v3_struct_0(sK3)
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(forward_demodulation,[],[f706,f653]) ).
fof(f708,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X1,sF29,u1_struct_0(X0))
| ~ v1_funct_2(X1,sF29,u1_struct_0(X0))
| r3_waybel_1(X0,k7_yellow_2(sF29,X0,X1,sK5),k5_pre_topc(X0,sK3,X2,sF32))
| ~ v3_waybel_1(k1_waybel_1(X0,sK3,X2,X1),X0,sK3)
| ~ v1_funct_1(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(sK3))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(sK3))
| v3_struct_0(sK3)
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(forward_demodulation,[],[f707,f653]) ).
fof(f709,plain,
! [X2,X0,X1] :
( ~ v1_funct_2(X2,u1_struct_0(X0),sF29)
| ~ m2_relset_1(X1,sF29,u1_struct_0(X0))
| ~ v1_funct_2(X1,sF29,u1_struct_0(X0))
| r3_waybel_1(X0,k7_yellow_2(sF29,X0,X1,sK5),k5_pre_topc(X0,sK3,X2,sF32))
| ~ v3_waybel_1(k1_waybel_1(X0,sK3,X2,X1),X0,sK3)
| ~ v1_funct_1(X1)
| ~ v1_funct_1(X2)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(sK3))
| v3_struct_0(sK3)
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(forward_demodulation,[],[f708,f653]) ).
fof(f710,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,u1_struct_0(X0),sF29)
| ~ v1_funct_2(X2,u1_struct_0(X0),sF29)
| ~ m2_relset_1(X1,sF29,u1_struct_0(X0))
| ~ v1_funct_2(X1,sF29,u1_struct_0(X0))
| r3_waybel_1(X0,k7_yellow_2(sF29,X0,X1,sK5),k5_pre_topc(X0,sK3,X2,sF32))
| ~ v3_waybel_1(k1_waybel_1(X0,sK3,X2,X1),X0,sK3)
| ~ v1_funct_1(X1)
| ~ v1_funct_1(X2)
| v3_struct_0(sK3)
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(forward_demodulation,[],[f709,f653]) ).
fof(f712,definition,
( spl36_5
<=> ! [X2,X0,X1] :
( ~ m2_relset_1(X2,u1_struct_0(X0),sF29)
| ~ l1_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| v3_struct_0(X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_1(X1)
| ~ v3_waybel_1(k1_waybel_1(X0,sK3,X2,X1),X0,sK3)
| r3_waybel_1(X0,k7_yellow_2(sF29,X0,X1,sK5),k5_pre_topc(X0,sK3,X2,sF32))
| ~ v1_funct_2(X1,sF29,u1_struct_0(X0))
| ~ m2_relset_1(X1,sF29,u1_struct_0(X0))
| ~ v1_funct_2(X2,u1_struct_0(X0),sF29) ) ),
introduced(definition,[new_symbols(definition,[spl36_5])],[avatar_definition]) ).
fof(f713,plain,
( ! [X2,X0,X1] :
( r3_waybel_1(X0,k7_yellow_2(sF29,X0,X1,sK5),k5_pre_topc(X0,sK3,X2,sF32))
| ~ l1_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| v3_struct_0(X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_1(X1)
| ~ v3_waybel_1(k1_waybel_1(X0,sK3,X2,X1),X0,sK3)
| ~ m2_relset_1(X2,u1_struct_0(X0),sF29)
| ~ v1_funct_2(X1,sF29,u1_struct_0(X0))
| ~ m2_relset_1(X1,sF29,u1_struct_0(X0))
| ~ v1_funct_2(X2,u1_struct_0(X0),sF29) )
| ~ spl36_5 ),
inference(avatar_component_clause,[],[f712]) ).
fof(f714,plain,
( spl36_3
| spl36_5 ),
inference(avatar_split_clause,[],[f710,f712,f698]) ).
fof(f727,definition,
( spl36_6
<=> l1_struct_0(sK2) ),
introduced(definition,[new_symbols(definition,[spl36_6])],[avatar_definition]) ).
fof(f728,plain,
( l1_struct_0(sK2)
| ~ spl36_6 ),
inference(avatar_component_clause,[],[f727]) ).
fof(f729,plain,
( ~ l1_struct_0(sK2)
| spl36_6 ),
inference(avatar_component_clause,[],[f727]) ).
fof(f735,definition,
( spl36_8
<=> l1_struct_0(sK3) ),
introduced(definition,[new_symbols(definition,[spl36_8])],[avatar_definition]) ).
fof(f736,plain,
( l1_struct_0(sK3)
| ~ spl36_8 ),
inference(avatar_component_clause,[],[f735]) ).
fof(f737,plain,
( ~ l1_struct_0(sK3)
| spl36_8 ),
inference(avatar_component_clause,[],[f735]) ).
fof(f754,plain,
( m1_subset_1(sF31,u1_struct_0(sK2))
| v1_xboole_0(sF29)
| v3_struct_0(sK2)
| ~ l1_struct_0(sK2)
| ~ v1_funct_1(sF30)
| ~ v1_funct_2(sF30,sF29,u1_struct_0(sK2))
| ~ m1_relset_1(sF30,sF29,u1_struct_0(sK2))
| ~ m1_subset_1(sK5,sF29) ),
inference(superposition,[],[f498,f657]) ).
fof(f767,plain,
( ~ v2_lattice3(sK3)
| ~ l1_orders_2(sK3)
| ~ spl36_3 ),
inference(resolution,[],[f457,f700]) ).
fof(f768,plain,
( ~ l1_orders_2(sK3)
| ~ spl36_3 ),
inference(forward_subsumption_resolution,[],[f767,f351]) ).
fof(f769,plain,
( $false
| ~ spl36_3 ),
inference(forward_subsumption_resolution,[],[f768,f349]) ).
fof(f770,plain,
~ spl36_3,
inference(avatar_contradiction_clause,[],[f769]) ).
fof(f773,plain,
( ! [X0] :
( r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,X0,sK5),sF33)
| ~ l1_orders_2(sK2)
| ~ v4_orders_2(sK2)
| ~ v3_orders_2(sK2)
| ~ v2_orders_2(sK2)
| v3_struct_0(sK2)
| ~ v1_funct_1(sK4)
| ~ v1_funct_1(X0)
| ~ v3_waybel_1(k1_waybel_1(sK2,sK3,sK4,X0),sK2,sK3)
| ~ m2_relset_1(sK4,u1_struct_0(sK2),sF29)
| ~ v1_funct_2(X0,sF29,u1_struct_0(sK2))
| ~ m2_relset_1(X0,sF29,u1_struct_0(sK2))
| ~ v1_funct_2(sK4,u1_struct_0(sK2),sF29) )
| ~ spl36_5 ),
inference(superposition,[],[f713,f661]) ).
fof(f775,plain,
( ! [X0] :
( r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,X0,sK5),sF33)
| ~ v4_orders_2(sK2)
| ~ v3_orders_2(sK2)
| ~ v2_orders_2(sK2)
| v3_struct_0(sK2)
| ~ v1_funct_1(sK4)
| ~ v1_funct_1(X0)
| ~ v3_waybel_1(k1_waybel_1(sK2,sK3,sK4,X0),sK2,sK3)
| ~ m2_relset_1(sK4,u1_struct_0(sK2),sF29)
| ~ v1_funct_2(X0,sF29,u1_struct_0(sK2))
| ~ m2_relset_1(X0,sF29,u1_struct_0(sK2))
| ~ v1_funct_2(sK4,u1_struct_0(sK2),sF29) )
| ~ spl36_5 ),
inference(forward_subsumption_resolution,[],[f773,f342]) ).
fof(f777,plain,
( ! [X0] :
( r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,X0,sK5),sF33)
| ~ v3_orders_2(sK2)
| ~ v2_orders_2(sK2)
| v3_struct_0(sK2)
| ~ v1_funct_1(sK4)
| ~ v1_funct_1(X0)
| ~ v3_waybel_1(k1_waybel_1(sK2,sK3,sK4,X0),sK2,sK3)
| ~ m2_relset_1(sK4,u1_struct_0(sK2),sF29)
| ~ v1_funct_2(X0,sF29,u1_struct_0(sK2))
| ~ m2_relset_1(X0,sF29,u1_struct_0(sK2))
| ~ v1_funct_2(sK4,u1_struct_0(sK2),sF29) )
| ~ spl36_5 ),
inference(forward_subsumption_resolution,[],[f775,f346]) ).
fof(f779,plain,
( ! [X0] :
( r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,X0,sK5),sF33)
| ~ v2_orders_2(sK2)
| v3_struct_0(sK2)
| ~ v1_funct_1(sK4)
| ~ v1_funct_1(X0)
| ~ v3_waybel_1(k1_waybel_1(sK2,sK3,sK4,X0),sK2,sK3)
| ~ m2_relset_1(sK4,u1_struct_0(sK2),sF29)
| ~ v1_funct_2(X0,sF29,u1_struct_0(sK2))
| ~ m2_relset_1(X0,sF29,u1_struct_0(sK2))
| ~ v1_funct_2(sK4,u1_struct_0(sK2),sF29) )
| ~ spl36_5 ),
inference(forward_subsumption_resolution,[],[f777,f347]) ).
fof(f781,plain,
( ! [X0] :
( r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,X0,sK5),sF33)
| v3_struct_0(sK2)
| ~ v1_funct_1(sK4)
| ~ v1_funct_1(X0)
| ~ v3_waybel_1(k1_waybel_1(sK2,sK3,sK4,X0),sK2,sK3)
| ~ m2_relset_1(sK4,u1_struct_0(sK2),sF29)
| ~ v1_funct_2(X0,sF29,u1_struct_0(sK2))
| ~ m2_relset_1(X0,sF29,u1_struct_0(sK2))
| ~ v1_funct_2(sK4,u1_struct_0(sK2),sF29) )
| ~ spl36_5 ),
inference(forward_subsumption_resolution,[],[f779,f348]) ).
fof(f783,plain,
( ! [X0] :
( r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,X0,sK5),sF33)
| v3_struct_0(sK2)
| ~ v1_funct_1(X0)
| ~ v3_waybel_1(k1_waybel_1(sK2,sK3,sK4,X0),sK2,sK3)
| ~ m2_relset_1(sK4,u1_struct_0(sK2),sF29)
| ~ v1_funct_2(X0,sF29,u1_struct_0(sK2))
| ~ m2_relset_1(X0,sF29,u1_struct_0(sK2))
| ~ v1_funct_2(sK4,u1_struct_0(sK2),sF29) )
| ~ spl36_5 ),
inference(forward_subsumption_resolution,[],[f781,f359]) ).
fof(f785,plain,
( ! [X0] :
( ~ m2_relset_1(sK4,sF35,sF29)
| r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,X0,sK5),sF33)
| v3_struct_0(sK2)
| ~ v1_funct_1(X0)
| ~ v3_waybel_1(k1_waybel_1(sK2,sK3,sK4,X0),sK2,sK3)
| ~ v1_funct_2(X0,sF29,u1_struct_0(sK2))
| ~ m2_relset_1(X0,sF29,u1_struct_0(sK2))
| ~ v1_funct_2(sK4,u1_struct_0(sK2),sF29) )
| ~ spl36_5 ),
inference(forward_demodulation,[],[f783,f667]) ).
fof(f787,plain,
( ! [X0] :
( r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,X0,sK5),sF33)
| v3_struct_0(sK2)
| ~ v1_funct_1(X0)
| ~ v3_waybel_1(k1_waybel_1(sK2,sK3,sK4,X0),sK2,sK3)
| ~ v1_funct_2(X0,sF29,u1_struct_0(sK2))
| ~ m2_relset_1(X0,sF29,u1_struct_0(sK2))
| ~ v1_funct_2(sK4,u1_struct_0(sK2),sF29) )
| ~ spl36_5 ),
inference(forward_subsumption_resolution,[],[f785,f669]) ).
fof(f789,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF29,sF35)
| r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,X0,sK5),sF33)
| v3_struct_0(sK2)
| ~ v1_funct_1(X0)
| ~ v3_waybel_1(k1_waybel_1(sK2,sK3,sK4,X0),sK2,sK3)
| ~ m2_relset_1(X0,sF29,u1_struct_0(sK2))
| ~ v1_funct_2(sK4,u1_struct_0(sK2),sF29) )
| ~ spl36_5 ),
inference(forward_demodulation,[],[f787,f667]) ).
fof(f791,plain,
( ! [X0] :
( ~ m2_relset_1(X0,sF29,sF35)
| ~ v1_funct_2(X0,sF29,sF35)
| r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,X0,sK5),sF33)
| v3_struct_0(sK2)
| ~ v1_funct_1(X0)
| ~ v3_waybel_1(k1_waybel_1(sK2,sK3,sK4,X0),sK2,sK3)
| ~ v1_funct_2(sK4,u1_struct_0(sK2),sF29) )
| ~ spl36_5 ),
inference(forward_demodulation,[],[f789,f667]) ).
fof(f793,definition,
( spl36_12
<=> v1_funct_1(sF30) ),
introduced(definition,[new_symbols(definition,[spl36_12])],[avatar_definition]) ).
fof(f794,plain,
( v1_funct_1(sF30)
| ~ spl36_12 ),
inference(avatar_component_clause,[],[f793]) ).
fof(f795,plain,
( ~ v1_funct_1(sF30)
| spl36_12 ),
inference(avatar_component_clause,[],[f793]) ).
fof(f797,definition,
( spl36_13
<=> v1_funct_2(sF30,sF29,sF35) ),
introduced(definition,[new_symbols(definition,[spl36_13])],[avatar_definition]) ).
fof(f798,plain,
( v1_funct_2(sF30,sF29,sF35)
| ~ spl36_13 ),
inference(avatar_component_clause,[],[f797]) ).
fof(f801,definition,
( spl36_14
<=> m2_relset_1(sF30,sF29,sF35) ),
introduced(definition,[new_symbols(definition,[spl36_14])],[avatar_definition]) ).
fof(f802,plain,
( m2_relset_1(sF30,sF29,sF35)
| ~ spl36_14 ),
inference(avatar_component_clause,[],[f801]) ).
fof(f808,plain,
( ! [X0] :
( ~ v1_funct_2(sK4,sF35,sF29)
| ~ m2_relset_1(X0,sF29,sF35)
| ~ v1_funct_2(X0,sF29,sF35)
| r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,X0,sK5),sF33)
| v3_struct_0(sK2)
| ~ v1_funct_1(X0)
| ~ v3_waybel_1(k1_waybel_1(sK2,sK3,sK4,X0),sK2,sK3) )
| ~ spl36_5 ),
inference(forward_demodulation,[],[f791,f667]) ).
fof(f809,plain,
( ! [X0] :
( ~ m2_relset_1(X0,sF29,sF35)
| ~ v1_funct_2(X0,sF29,sF35)
| r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,X0,sK5),sF33)
| v3_struct_0(sK2)
| ~ v1_funct_1(X0)
| ~ v3_waybel_1(k1_waybel_1(sK2,sK3,sK4,X0),sK2,sK3) )
| ~ spl36_5 ),
inference(forward_subsumption_resolution,[],[f808,f668]) ).
fof(f811,definition,
( spl36_16
<=> ! [X0] :
( ~ m2_relset_1(X0,sF29,sF35)
| ~ v3_waybel_1(k1_waybel_1(sK2,sK3,sK4,X0),sK2,sK3)
| ~ v1_funct_1(X0)
| r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,X0,sK5),sF33)
| ~ v1_funct_2(X0,sF29,sF35) ) ),
introduced(definition,[new_symbols(definition,[spl36_16])],[avatar_definition]) ).
fof(f812,plain,
( ! [X0] :
( ~ v3_waybel_1(k1_waybel_1(sK2,sK3,sK4,X0),sK2,sK3)
| ~ m2_relset_1(X0,sF29,sF35)
| ~ v1_funct_1(X0)
| r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,X0,sK5),sF33)
| ~ v1_funct_2(X0,sF29,sF35) )
| ~ spl36_16 ),
inference(avatar_component_clause,[],[f811]) ).
fof(f813,plain,
( spl36_1
| spl36_16
| ~ spl36_5 ),
inference(avatar_split_clause,[],[f809,f712,f811,f690]) ).
fof(f814,plain,
( ~ v2_lattice3(sK2)
| ~ l1_orders_2(sK2)
| ~ spl36_1 ),
inference(resolution,[],[f692,f457]) ).
fof(f815,plain,
( ~ l1_orders_2(sK2)
| ~ spl36_1 ),
inference(forward_subsumption_resolution,[],[f814,f344]) ).
fof(f816,plain,
( $false
| ~ spl36_1 ),
inference(forward_subsumption_resolution,[],[f815,f342]) ).
fof(f817,plain,
~ spl36_1,
inference(avatar_contradiction_clause,[],[f816]) ).
fof(f820,plain,
l1_struct_0(sK2),
inference(resolution,[],[f499,f342]) ).
fof(f821,plain,
l1_struct_0(sK3),
inference(resolution,[],[f499,f349]) ).
fof(f822,plain,
( $false
| spl36_8 ),
inference(forward_subsumption_resolution,[],[f821,f737]) ).
fof(f823,plain,
spl36_8,
inference(avatar_contradiction_clause,[],[f822]) ).
fof(f824,plain,
( $false
| spl36_6 ),
inference(forward_subsumption_resolution,[],[f820,f729]) ).
fof(f825,plain,
spl36_6,
inference(avatar_contradiction_clause,[],[f824]) ).
fof(f942,plain,
( m2_relset_1(sF30,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)
| ~ 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(sK2),u1_struct_0(sK3))
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
inference(superposition,[],[f491,f655]) ).
fof(f951,plain,
( m2_relset_1(sF30,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)
| ~ 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(sK2),u1_struct_0(sK3))
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
inference(forward_subsumption_resolution,[],[f942,f348]) ).
fof(f956,plain,
( m2_relset_1(sF30,u1_struct_0(sK3),u1_struct_0(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(sK2),u1_struct_0(sK3))
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
inference(forward_subsumption_resolution,[],[f951,f347]) ).
fof(f961,plain,
( m2_relset_1(sF30,u1_struct_0(sK3),u1_struct_0(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(sK2),u1_struct_0(sK3))
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
inference(forward_subsumption_resolution,[],[f956,f346]) ).
fof(f966,plain,
( m2_relset_1(sF30,u1_struct_0(sK3),u1_struct_0(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(sK2),u1_struct_0(sK3))
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
inference(forward_subsumption_resolution,[],[f961,f345]) ).
fof(f971,plain,
( m2_relset_1(sF30,u1_struct_0(sK3),u1_struct_0(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(sK2),u1_struct_0(sK3))
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
inference(forward_subsumption_resolution,[],[f966,f344]) ).
fof(f976,plain,
( m2_relset_1(sF30,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)
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
inference(forward_subsumption_resolution,[],[f971,f342]) ).
fof(f977,plain,
( m2_relset_1(sF30,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)
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
inference(forward_subsumption_resolution,[],[f976,f355]) ).
fof(f978,plain,
( m2_relset_1(sF30,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ 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(sK2),u1_struct_0(sK3))
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
inference(forward_subsumption_resolution,[],[f977,f354]) ).
fof(f979,plain,
( m2_relset_1(sF30,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ v1_lattice3(sK3)
| ~ v2_lattice3(sK3)
| ~ l1_orders_2(sK3)
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
inference(forward_subsumption_resolution,[],[f978,f353]) ).
fof(f980,plain,
( m2_relset_1(sF30,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ v2_lattice3(sK3)
| ~ l1_orders_2(sK3)
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
inference(forward_subsumption_resolution,[],[f979,f352]) ).
fof(f981,plain,
( m2_relset_1(sF30,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ l1_orders_2(sK3)
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
inference(forward_subsumption_resolution,[],[f980,f351]) ).
fof(f982,plain,
( m2_relset_1(sF30,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
inference(forward_subsumption_resolution,[],[f981,f349]) ).
fof(f983,plain,
( m2_relset_1(sF30,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
inference(forward_subsumption_resolution,[],[f982,f359]) ).
fof(f984,plain,
( m2_relset_1(sF30,u1_struct_0(sK3),sF35)
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
inference(forward_demodulation,[],[f983,f667]) ).
fof(f985,plain,
( m2_relset_1(sF30,sF29,sF35)
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
inference(forward_demodulation,[],[f984,f653]) ).
fof(f986,plain,
( ~ v1_funct_2(sK4,u1_struct_0(sK2),sF29)
| m2_relset_1(sF30,sF29,sF35)
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
inference(forward_demodulation,[],[f985,f653]) ).
fof(f987,plain,
( ~ v1_funct_2(sK4,sF35,sF29)
| m2_relset_1(sF30,sF29,sF35)
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
inference(forward_demodulation,[],[f986,f667]) ).
fof(f988,plain,
( m2_relset_1(sF30,sF29,sF35)
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
inference(forward_subsumption_resolution,[],[f987,f668]) ).
fof(f989,plain,
( ~ m1_relset_1(sK4,u1_struct_0(sK2),sF29)
| m2_relset_1(sF30,sF29,sF35) ),
inference(forward_demodulation,[],[f988,f653]) ).
fof(f990,plain,
( ~ m1_relset_1(sK4,sF35,sF29)
| m2_relset_1(sF30,sF29,sF35) ),
inference(forward_demodulation,[],[f989,f667]) ).
fof(f991,plain,
m2_relset_1(sF30,sF29,sF35),
inference(forward_subsumption_resolution,[],[f990,f672]) ).
fof(f992,plain,
spl36_14,
inference(avatar_split_clause,[],[f991,f801]) ).
fof(f993,plain,
( m1_relset_1(sF30,sF29,sF35)
| ~ spl36_14 ),
inference(resolution,[],[f802,f634]) ).
fof(f999,plain,
! [X0,X1] :
( ~ m1_relset_1(X0,u1_struct_0(X1),sF29)
| ~ 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,u1_struct_0(X1),sF29)
| v1_funct_1(k1_waybel34(X1,sK3,X0)) ),
inference(superposition,[],[f493,f653]) ).
fof(f1002,plain,
! [X0,X1] :
( ~ m1_relset_1(X0,u1_struct_0(X1),sF29)
| ~ 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,u1_struct_0(X1),sF29)
| v1_funct_1(k1_waybel34(X1,sK3,X0)) ),
inference(forward_subsumption_resolution,[],[f999,f355]) ).
fof(f1006,plain,
! [X0,X1] :
( ~ m1_relset_1(X0,u1_struct_0(X1),sF29)
| ~ 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,u1_struct_0(X1),sF29)
| v1_funct_1(k1_waybel34(X1,sK3,X0)) ),
inference(forward_subsumption_resolution,[],[f1002,f354]) ).
fof(f1010,plain,
! [X0,X1] :
( ~ m1_relset_1(X0,u1_struct_0(X1),sF29)
| ~ 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,u1_struct_0(X1),sF29)
| v1_funct_1(k1_waybel34(X1,sK3,X0)) ),
inference(forward_subsumption_resolution,[],[f1006,f353]) ).
fof(f1014,plain,
! [X0,X1] :
( ~ m1_relset_1(X0,u1_struct_0(X1),sF29)
| ~ 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,u1_struct_0(X1),sF29)
| v1_funct_1(k1_waybel34(X1,sK3,X0)) ),
inference(forward_subsumption_resolution,[],[f1010,f352]) ).
fof(f1018,plain,
! [X0,X1] :
( ~ m1_relset_1(X0,u1_struct_0(X1),sF29)
| ~ 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,u1_struct_0(X1),sF29)
| v1_funct_1(k1_waybel34(X1,sK3,X0)) ),
inference(forward_subsumption_resolution,[],[f1014,f351]) ).
fof(f1022,plain,
! [X0,X1] :
( ~ m1_relset_1(X0,u1_struct_0(X1),sF29)
| ~ 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,u1_struct_0(X1),sF29)
| v1_funct_1(k1_waybel34(X1,sK3,X0)) ),
inference(forward_subsumption_resolution,[],[f1018,f349]) ).
fof(f1025,plain,
( ~ v1_xboole_0(sF29)
| v3_struct_0(sK3)
| ~ l1_struct_0(sK3) ),
inference(superposition,[],[f536,f653]) ).
fof(f1028,plain,
( ~ v1_xboole_0(sF29)
| ~ l1_struct_0(sK3)
| spl36_3 ),
inference(forward_subsumption_resolution,[],[f1025,f699]) ).
fof(f1030,plain,
( ~ v1_xboole_0(sF29)
| spl36_3
| ~ spl36_8 ),
inference(forward_subsumption_resolution,[],[f1028,f736]) ).
fof(f1064,plain,
( ~ v1_funct_1(k1_waybel34(sK2,sK3,sK4))
| ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
| ~ v3_lattice3(sK2)
| ~ v3_lattice3(sK3)
| ~ v17_waybel_0(sK4,sK2,sK3)
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_relset_1(sK4,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)
| ~ 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(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
| ~ v1_funct_1(k1_waybel34(sK2,sK3,sK4))
| r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,k1_waybel34(sK2,sK3,sK4),sK5),sF33)
| ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
| ~ spl36_16 ),
inference(resolution,[],[f650,f812]) ).
fof(f1066,plain,
( ~ v1_funct_1(k1_waybel34(sK2,sK3,sK4))
| ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
| ~ v3_lattice3(sK2)
| ~ v3_lattice3(sK3)
| ~ v17_waybel_0(sK4,sK2,sK3)
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_relset_1(sK4,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)
| ~ 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(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
| r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,k1_waybel34(sK2,sK3,sK4),sK5),sF33)
| ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
| ~ spl36_16 ),
inference(duplicate_literal_removal,[],[f1064]) ).
fof(f1068,plain,
( ~ v1_funct_1(k1_waybel34(sK2,sK3,sK4))
| ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
| ~ v3_lattice3(sK3)
| ~ v17_waybel_0(sK4,sK2,sK3)
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_relset_1(sK4,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)
| ~ 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(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
| r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,k1_waybel34(sK2,sK3,sK4),sK5),sF33)
| ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
| ~ spl36_16 ),
inference(forward_subsumption_resolution,[],[f1066,f343]) ).
fof(f1069,plain,
( ~ v1_funct_1(k1_waybel34(sK2,sK3,sK4))
| ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
| ~ v17_waybel_0(sK4,sK2,sK3)
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_relset_1(sK4,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)
| ~ 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(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
| r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,k1_waybel34(sK2,sK3,sK4),sK5),sF33)
| ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
| ~ spl36_16 ),
inference(forward_subsumption_resolution,[],[f1068,f350]) ).
fof(f1070,plain,
( ~ v1_funct_1(k1_waybel34(sK2,sK3,sK4))
| ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_relset_1(sK4,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)
| ~ 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(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
| r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,k1_waybel34(sK2,sK3,sK4),sK5),sF33)
| ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
| ~ spl36_16 ),
inference(forward_subsumption_resolution,[],[f1069,f357]) ).
fof(f1071,plain,
( ~ v1_funct_1(k1_waybel34(sK2,sK3,sK4))
| ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_relset_1(sK4,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)
| ~ 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(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
| r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,k1_waybel34(sK2,sK3,sK4),sK5),sF33)
| ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
| ~ spl36_16 ),
inference(forward_subsumption_resolution,[],[f1070,f359]) ).
fof(f1072,plain,
( ~ v1_funct_1(k1_waybel34(sK2,sK3,sK4))
| ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_relset_1(sK4,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)
| ~ 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(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
| r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,k1_waybel34(sK2,sK3,sK4),sK5),sF33)
| ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
| ~ spl36_16 ),
inference(forward_subsumption_resolution,[],[f1071,f355]) ).
fof(f1073,plain,
( ~ v1_funct_1(k1_waybel34(sK2,sK3,sK4))
| ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(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(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
| r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,k1_waybel34(sK2,sK3,sK4),sK5),sF33)
| ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
| ~ spl36_16 ),
inference(forward_subsumption_resolution,[],[f1072,f354]) ).
fof(f1074,plain,
( ~ v1_funct_1(k1_waybel34(sK2,sK3,sK4))
| ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(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(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
| r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,k1_waybel34(sK2,sK3,sK4),sK5),sF33)
| ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
| ~ spl36_16 ),
inference(forward_subsumption_resolution,[],[f1073,f353]) ).
fof(f1075,plain,
( ~ v1_funct_1(k1_waybel34(sK2,sK3,sK4))
| ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(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(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
| r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,k1_waybel34(sK2,sK3,sK4),sK5),sF33)
| ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
| ~ spl36_16 ),
inference(forward_subsumption_resolution,[],[f1074,f352]) ).
fof(f1076,plain,
( ~ v1_funct_1(k1_waybel34(sK2,sK3,sK4))
| ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(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(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
| r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,k1_waybel34(sK2,sK3,sK4),sK5),sF33)
| ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
| ~ spl36_16 ),
inference(forward_subsumption_resolution,[],[f1075,f351]) ).
fof(f1077,plain,
( ~ v1_funct_1(k1_waybel34(sK2,sK3,sK4))
| ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_relset_1(sK4,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)
| ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
| r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,k1_waybel34(sK2,sK3,sK4),sK5),sF33)
| ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
| ~ spl36_16 ),
inference(forward_subsumption_resolution,[],[f1076,f349]) ).
fof(f1078,plain,
( ~ v1_funct_1(k1_waybel34(sK2,sK3,sK4))
| ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_relset_1(sK4,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)
| ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
| r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,k1_waybel34(sK2,sK3,sK4),sK5),sF33)
| ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
| ~ spl36_16 ),
inference(forward_subsumption_resolution,[],[f1077,f348]) ).
fof(f1079,plain,
( ~ v1_funct_1(k1_waybel34(sK2,sK3,sK4))
| ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v4_orders_2(sK2)
| ~ v1_lattice3(sK2)
| ~ v2_lattice3(sK2)
| ~ l1_orders_2(sK2)
| ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
| r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,k1_waybel34(sK2,sK3,sK4),sK5),sF33)
| ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
| ~ spl36_16 ),
inference(forward_subsumption_resolution,[],[f1078,f347]) ).
fof(f1080,plain,
( ~ v1_funct_1(k1_waybel34(sK2,sK3,sK4))
| ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v1_lattice3(sK2)
| ~ v2_lattice3(sK2)
| ~ l1_orders_2(sK2)
| ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
| r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,k1_waybel34(sK2,sK3,sK4),sK5),sF33)
| ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
| ~ spl36_16 ),
inference(forward_subsumption_resolution,[],[f1079,f346]) ).
fof(f1081,plain,
( ~ v1_funct_1(k1_waybel34(sK2,sK3,sK4))
| ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ v2_lattice3(sK2)
| ~ l1_orders_2(sK2)
| ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
| r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,k1_waybel34(sK2,sK3,sK4),sK5),sF33)
| ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
| ~ spl36_16 ),
inference(forward_subsumption_resolution,[],[f1080,f345]) ).
fof(f1082,plain,
( ~ v1_funct_1(k1_waybel34(sK2,sK3,sK4))
| ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ l1_orders_2(sK2)
| ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
| r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,k1_waybel34(sK2,sK3,sK4),sK5),sF33)
| ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
| ~ spl36_16 ),
inference(forward_subsumption_resolution,[],[f1081,f344]) ).
fof(f1083,plain,
( ~ v1_funct_1(k1_waybel34(sK2,sK3,sK4))
| ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
| r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,k1_waybel34(sK2,sK3,sK4),sK5),sF33)
| ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
| ~ spl36_16 ),
inference(forward_subsumption_resolution,[],[f1082,f342]) ).
fof(f1084,plain,
( ~ v1_funct_1(sF30)
| ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
| r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,k1_waybel34(sK2,sK3,sK4),sK5),sF33)
| ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
| ~ spl36_16 ),
inference(forward_demodulation,[],[f1083,f655]) ).
fof(f1085,plain,
( v1_funct_2(sF30,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)
| ~ 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(sK2),u1_struct_0(sK3))
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
inference(superposition,[],[f492,f655]) ).
fof(f1094,plain,
( v1_funct_2(sF30,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)
| ~ 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(sK2),u1_struct_0(sK3))
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
inference(forward_subsumption_resolution,[],[f1085,f348]) ).
fof(f1099,plain,
( v1_funct_2(sF30,u1_struct_0(sK3),u1_struct_0(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(sK2),u1_struct_0(sK3))
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
inference(forward_subsumption_resolution,[],[f1094,f347]) ).
fof(f1104,plain,
( v1_funct_2(sF30,u1_struct_0(sK3),u1_struct_0(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(sK2),u1_struct_0(sK3))
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
inference(forward_subsumption_resolution,[],[f1099,f346]) ).
fof(f1109,plain,
( v1_funct_2(sF30,u1_struct_0(sK3),u1_struct_0(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(sK2),u1_struct_0(sK3))
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
inference(forward_subsumption_resolution,[],[f1104,f345]) ).
fof(f1114,plain,
( v1_funct_2(sF30,u1_struct_0(sK3),u1_struct_0(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(sK2),u1_struct_0(sK3))
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
inference(forward_subsumption_resolution,[],[f1109,f344]) ).
fof(f1119,plain,
( v1_funct_2(sF30,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)
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
inference(forward_subsumption_resolution,[],[f1114,f342]) ).
fof(f1120,plain,
( v1_funct_2(sF30,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)
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
inference(forward_subsumption_resolution,[],[f1119,f355]) ).
fof(f1121,plain,
( v1_funct_2(sF30,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ 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(sK2),u1_struct_0(sK3))
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
inference(forward_subsumption_resolution,[],[f1120,f354]) ).
fof(f1122,plain,
( v1_funct_2(sF30,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ v1_lattice3(sK3)
| ~ v2_lattice3(sK3)
| ~ l1_orders_2(sK3)
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
inference(forward_subsumption_resolution,[],[f1121,f353]) ).
fof(f1123,plain,
( v1_funct_2(sF30,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ v2_lattice3(sK3)
| ~ l1_orders_2(sK3)
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
inference(forward_subsumption_resolution,[],[f1122,f352]) ).
fof(f1124,plain,
( v1_funct_2(sF30,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ l1_orders_2(sK3)
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
inference(forward_subsumption_resolution,[],[f1123,f351]) ).
fof(f1125,plain,
( v1_funct_2(sF30,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
inference(forward_subsumption_resolution,[],[f1124,f349]) ).
fof(f1126,plain,
( v1_funct_2(sF30,u1_struct_0(sK3),u1_struct_0(sK2))
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
inference(forward_subsumption_resolution,[],[f1125,f359]) ).
fof(f1127,plain,
( v1_funct_2(sF30,u1_struct_0(sK3),sF35)
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
inference(forward_demodulation,[],[f1126,f667]) ).
fof(f1128,plain,
( v1_funct_2(sF30,sF29,sF35)
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
inference(forward_demodulation,[],[f1127,f653]) ).
fof(f1129,plain,
( ~ v1_funct_2(sK4,u1_struct_0(sK2),sF29)
| v1_funct_2(sF30,sF29,sF35)
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
inference(forward_demodulation,[],[f1128,f653]) ).
fof(f1130,plain,
( ~ v1_funct_2(sK4,sF35,sF29)
| v1_funct_2(sF30,sF29,sF35)
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
inference(forward_demodulation,[],[f1129,f667]) ).
fof(f1131,plain,
( v1_funct_2(sF30,sF29,sF35)
| ~ m1_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)) ),
inference(forward_subsumption_resolution,[],[f1130,f668]) ).
fof(f1132,plain,
( ~ m1_relset_1(sK4,u1_struct_0(sK2),sF29)
| v1_funct_2(sF30,sF29,sF35) ),
inference(forward_demodulation,[],[f1131,f653]) ).
fof(f1133,plain,
( ~ m1_relset_1(sK4,sF35,sF29)
| v1_funct_2(sF30,sF29,sF35) ),
inference(forward_demodulation,[],[f1132,f667]) ).
fof(f1134,plain,
v1_funct_2(sF30,sF29,sF35),
inference(forward_subsumption_resolution,[],[f1133,f672]) ).
fof(f1135,plain,
spl36_13,
inference(avatar_split_clause,[],[f1134,f797]) ).
fof(f1137,plain,
! [X0] :
( ~ m1_relset_1(X0,sF35,sF29)
| ~ 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,sF35,sF29)
| v1_funct_1(k1_waybel34(sK2,sK3,X0)) ),
inference(superposition,[],[f1022,f667]) ).
fof(f1138,plain,
! [X0] :
( ~ m1_relset_1(X0,sF35,sF29)
| ~ 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,sF35,sF29)
| v1_funct_1(k1_waybel34(sK2,sK3,X0)) ),
inference(forward_subsumption_resolution,[],[f1137,f348]) ).
fof(f1140,plain,
! [X0] :
( ~ m1_relset_1(X0,sF35,sF29)
| ~ v4_orders_2(sK2)
| ~ v1_lattice3(sK2)
| ~ v2_lattice3(sK2)
| ~ l1_orders_2(sK2)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,sF35,sF29)
| v1_funct_1(k1_waybel34(sK2,sK3,X0)) ),
inference(forward_subsumption_resolution,[],[f1138,f347]) ).
fof(f1142,plain,
! [X0] :
( ~ m1_relset_1(X0,sF35,sF29)
| ~ v1_lattice3(sK2)
| ~ v2_lattice3(sK2)
| ~ l1_orders_2(sK2)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,sF35,sF29)
| v1_funct_1(k1_waybel34(sK2,sK3,X0)) ),
inference(forward_subsumption_resolution,[],[f1140,f346]) ).
fof(f1144,plain,
! [X0] :
( ~ m1_relset_1(X0,sF35,sF29)
| ~ v2_lattice3(sK2)
| ~ l1_orders_2(sK2)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,sF35,sF29)
| v1_funct_1(k1_waybel34(sK2,sK3,X0)) ),
inference(forward_subsumption_resolution,[],[f1142,f345]) ).
fof(f1146,plain,
! [X0] :
( ~ m1_relset_1(X0,sF35,sF29)
| ~ l1_orders_2(sK2)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,sF35,sF29)
| v1_funct_1(k1_waybel34(sK2,sK3,X0)) ),
inference(forward_subsumption_resolution,[],[f1144,f344]) ).
fof(f1148,plain,
! [X0] :
( v1_funct_1(k1_waybel34(sK2,sK3,X0))
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,sF35,sF29)
| ~ m1_relset_1(X0,sF35,sF29) ),
inference(forward_subsumption_resolution,[],[f1146,f342]) ).
fof(f1150,plain,
( v1_funct_1(sF30)
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,sF35,sF29)
| ~ m1_relset_1(sK4,sF35,sF29) ),
inference(superposition,[],[f1148,f655]) ).
fof(f1151,plain,
( ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,sF35,sF29)
| ~ m1_relset_1(sK4,sF35,sF29)
| spl36_12 ),
inference(forward_subsumption_resolution,[],[f1150,f795]) ).
fof(f1152,plain,
( ~ v1_funct_2(sK4,sF35,sF29)
| ~ m1_relset_1(sK4,sF35,sF29)
| spl36_12 ),
inference(forward_subsumption_resolution,[],[f1151,f359]) ).
fof(f1153,plain,
( ~ m1_relset_1(sK4,sF35,sF29)
| spl36_12 ),
inference(forward_subsumption_resolution,[],[f1152,f668]) ).
fof(f1154,plain,
( $false
| spl36_12 ),
inference(forward_subsumption_resolution,[],[f1153,f672]) ).
fof(f1155,plain,
spl36_12,
inference(avatar_contradiction_clause,[],[f1154]) ).
fof(f1156,plain,
( m1_subset_1(sF31,u1_struct_0(sK2))
| v3_struct_0(sK2)
| ~ l1_struct_0(sK2)
| ~ v1_funct_1(sF30)
| ~ v1_funct_2(sF30,sF29,u1_struct_0(sK2))
| ~ m1_relset_1(sF30,sF29,u1_struct_0(sK2))
| ~ m1_subset_1(sK5,sF29)
| spl36_3
| ~ spl36_8 ),
inference(forward_subsumption_resolution,[],[f754,f1030]) ).
fof(f1161,plain,
( ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
| ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
| r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,k1_waybel34(sK2,sK3,sK4),sK5),sF33)
| ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
| ~ spl36_12
| ~ spl36_16 ),
inference(forward_subsumption_resolution,[],[f1084,f794]) ).
fof(f1162,plain,
( m1_subset_1(sF31,u1_struct_0(sK2))
| ~ l1_struct_0(sK2)
| ~ v1_funct_1(sF30)
| ~ v1_funct_2(sF30,sF29,u1_struct_0(sK2))
| ~ m1_relset_1(sF30,sF29,u1_struct_0(sK2))
| ~ m1_subset_1(sK5,sF29)
| spl36_1
| spl36_3
| ~ spl36_8 ),
inference(forward_subsumption_resolution,[],[f1156,f691]) ).
fof(f1167,plain,
( ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),sF35)
| ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
| r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,k1_waybel34(sK2,sK3,sK4),sK5),sF33)
| ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
| ~ spl36_12
| ~ spl36_16 ),
inference(forward_demodulation,[],[f1161,f667]) ).
fof(f1168,plain,
( m1_subset_1(sF31,u1_struct_0(sK2))
| ~ v1_funct_1(sF30)
| ~ v1_funct_2(sF30,sF29,u1_struct_0(sK2))
| ~ m1_relset_1(sF30,sF29,u1_struct_0(sK2))
| ~ m1_subset_1(sK5,sF29)
| spl36_1
| spl36_3
| ~ spl36_6
| ~ spl36_8 ),
inference(forward_subsumption_resolution,[],[f1162,f728]) ).
fof(f1172,plain,
( ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
| ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
| r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,k1_waybel34(sK2,sK3,sK4),sK5),sF33)
| ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
| ~ spl36_12
| ~ spl36_16 ),
inference(forward_demodulation,[],[f1167,f653]) ).
fof(f1173,plain,
( ~ v1_funct_2(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
| ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
| r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,k1_waybel34(sK2,sK3,sK4),sK5),sF33)
| ~ spl36_12
| ~ spl36_16 ),
inference(duplicate_literal_removal,[],[f1172]) ).
fof(f1174,plain,
( m1_subset_1(sF31,u1_struct_0(sK2))
| ~ v1_funct_2(sF30,sF29,u1_struct_0(sK2))
| ~ m1_relset_1(sF30,sF29,u1_struct_0(sK2))
| ~ m1_subset_1(sK5,sF29)
| spl36_1
| spl36_3
| ~ spl36_6
| ~ spl36_8
| ~ spl36_12 ),
inference(forward_subsumption_resolution,[],[f1168,f794]) ).
fof(f1177,plain,
( ~ v1_funct_2(sF30,sF29,sF35)
| ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
| r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,k1_waybel34(sK2,sK3,sK4),sK5),sF33)
| ~ spl36_12
| ~ spl36_16 ),
inference(forward_demodulation,[],[f1173,f655]) ).
fof(f1178,plain,
( m1_subset_1(sF31,u1_struct_0(sK2))
| ~ v1_funct_2(sF30,sF29,u1_struct_0(sK2))
| ~ m1_relset_1(sF30,sF29,u1_struct_0(sK2))
| spl36_1
| spl36_3
| ~ spl36_6
| ~ spl36_8
| ~ spl36_12 ),
inference(forward_subsumption_resolution,[],[f1174,f665]) ).
fof(f1181,plain,
( ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),u1_struct_0(sK2))
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
| r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,k1_waybel34(sK2,sK3,sK4),sK5),sF33)
| ~ spl36_12
| ~ spl36_13
| ~ spl36_16 ),
inference(forward_subsumption_resolution,[],[f1177,f798]) ).
fof(f1182,plain,
( m1_subset_1(sF31,sF35)
| ~ v1_funct_2(sF30,sF29,u1_struct_0(sK2))
| ~ m1_relset_1(sF30,sF29,u1_struct_0(sK2))
| spl36_1
| spl36_3
| ~ spl36_6
| ~ spl36_8
| ~ spl36_12 ),
inference(forward_demodulation,[],[f1178,f667]) ).
fof(f1185,plain,
( ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),u1_struct_0(sK3),sF35)
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
| r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,k1_waybel34(sK2,sK3,sK4),sK5),sF33)
| ~ spl36_12
| ~ spl36_13
| ~ spl36_16 ),
inference(forward_demodulation,[],[f1181,f667]) ).
fof(f1186,plain,
( ~ v1_funct_2(sF30,sF29,sF35)
| m1_subset_1(sF31,sF35)
| ~ m1_relset_1(sF30,sF29,u1_struct_0(sK2))
| spl36_1
| spl36_3
| ~ spl36_6
| ~ spl36_8
| ~ spl36_12 ),
inference(forward_demodulation,[],[f1182,f667]) ).
fof(f1189,plain,
( ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
| r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,k1_waybel34(sK2,sK3,sK4),sK5),sF33)
| ~ spl36_12
| ~ spl36_13
| ~ spl36_16 ),
inference(forward_demodulation,[],[f1185,f653]) ).
fof(f1190,plain,
( ~ m2_relset_1(k1_waybel34(sK2,sK3,sK4),sF29,sF35)
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,k1_waybel34(sK2,sK3,sK4),sK5),sF33)
| ~ spl36_12
| ~ spl36_13
| ~ spl36_16 ),
inference(duplicate_literal_removal,[],[f1189]) ).
fof(f1191,plain,
( m1_subset_1(sF31,sF35)
| ~ m1_relset_1(sF30,sF29,u1_struct_0(sK2))
| spl36_1
| spl36_3
| ~ spl36_6
| ~ spl36_8
| ~ spl36_12
| ~ spl36_13 ),
inference(forward_subsumption_resolution,[],[f1186,f798]) ).
fof(f1194,plain,
( ~ m2_relset_1(sF30,sF29,sF35)
| ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,k1_waybel34(sK2,sK3,sK4),sK5),sF33)
| ~ spl36_12
| ~ spl36_13
| ~ spl36_16 ),
inference(forward_demodulation,[],[f1190,f655]) ).
fof(f1195,plain,
( ~ m1_relset_1(sF30,sF29,sF35)
| m1_subset_1(sF31,sF35)
| spl36_1
| spl36_3
| ~ spl36_6
| ~ spl36_8
| ~ spl36_12
| ~ spl36_13 ),
inference(forward_demodulation,[],[f1191,f667]) ).
fof(f1198,plain,
( ~ v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,k1_waybel34(sK2,sK3,sK4),sK5),sF33)
| ~ spl36_12
| ~ spl36_13
| ~ spl36_14
| ~ spl36_16 ),
inference(forward_subsumption_resolution,[],[f1194,f802]) ).
fof(f1199,plain,
( m1_subset_1(sF31,sF35)
| spl36_1
| spl36_3
| ~ spl36_6
| ~ spl36_8
| ~ spl36_12
| ~ spl36_13
| ~ spl36_14 ),
inference(forward_subsumption_resolution,[],[f1195,f993]) ).
fof(f1202,plain,
( ~ v1_funct_2(sK4,u1_struct_0(sK2),sF29)
| ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,k1_waybel34(sK2,sK3,sK4),sK5),sF33)
| ~ spl36_12
| ~ spl36_13
| ~ spl36_14
| ~ spl36_16 ),
inference(forward_demodulation,[],[f1198,f653]) ).
fof(f1204,plain,
( ~ v1_funct_2(sK4,sF35,sF29)
| ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,k1_waybel34(sK2,sK3,sK4),sK5),sF33)
| ~ spl36_12
| ~ spl36_13
| ~ spl36_14
| ~ spl36_16 ),
inference(forward_demodulation,[],[f1202,f667]) ).
fof(f1206,plain,
( ~ m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
| r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,k1_waybel34(sK2,sK3,sK4),sK5),sF33)
| ~ spl36_12
| ~ spl36_13
| ~ spl36_14
| ~ spl36_16 ),
inference(forward_subsumption_resolution,[],[f1204,f668]) ).
fof(f1208,plain,
( ~ m2_relset_1(sK4,u1_struct_0(sK2),sF29)
| r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,k1_waybel34(sK2,sK3,sK4),sK5),sF33)
| ~ spl36_12
| ~ spl36_13
| ~ spl36_14
| ~ spl36_16 ),
inference(forward_demodulation,[],[f1206,f653]) ).
fof(f1210,plain,
( ~ m2_relset_1(sK4,sF35,sF29)
| r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,k1_waybel34(sK2,sK3,sK4),sK5),sF33)
| ~ spl36_12
| ~ spl36_13
| ~ spl36_14
| ~ spl36_16 ),
inference(forward_demodulation,[],[f1208,f667]) ).
fof(f1212,plain,
( r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,k1_waybel34(sK2,sK3,sK4),sK5),sF33)
| ~ spl36_12
| ~ spl36_13
| ~ spl36_14
| ~ spl36_16 ),
inference(forward_subsumption_resolution,[],[f1210,f669]) ).
fof(f1214,plain,
( r3_waybel_1(sK2,k7_yellow_2(sF29,sK2,sF30,sK5),sF33)
| ~ spl36_12
| ~ spl36_13
| ~ spl36_14
| ~ spl36_16 ),
inference(forward_demodulation,[],[f1212,f655]) ).
fof(f1216,plain,
( r3_waybel_1(sK2,sF31,sF33)
| ~ spl36_12
| ~ spl36_13
| ~ spl36_14
| ~ spl36_16 ),
inference(forward_demodulation,[],[f1214,f657]) ).
fof(f1229,plain,
( sF31 = k2_yellow_0(sK2,sF33)
| ~ m1_subset_1(sF31,u1_struct_0(sK2))
| v3_struct_0(sK2)
| ~ l1_orders_2(sK2)
| ~ spl36_12
| ~ spl36_13
| ~ spl36_14
| ~ spl36_16 ),
inference(resolution,[],[f1216,f487]) ).
fof(f1230,plain,
( sF31 = k2_yellow_0(sK2,sF33)
| ~ m1_subset_1(sF31,u1_struct_0(sK2))
| ~ l1_orders_2(sK2)
| spl36_1
| ~ spl36_12
| ~ spl36_13
| ~ spl36_14
| ~ spl36_16 ),
inference(forward_subsumption_resolution,[],[f1229,f691]) ).
fof(f1231,plain,
( sF31 = k2_yellow_0(sK2,sF33)
| ~ m1_subset_1(sF31,u1_struct_0(sK2))
| spl36_1
| ~ spl36_12
| ~ spl36_13
| ~ spl36_14
| ~ spl36_16 ),
inference(forward_subsumption_resolution,[],[f1230,f342]) ).
fof(f1232,plain,
( sF31 = sF34
| ~ m1_subset_1(sF31,u1_struct_0(sK2))
| spl36_1
| ~ spl36_12
| ~ spl36_13
| ~ spl36_14
| ~ spl36_16 ),
inference(forward_demodulation,[],[f1231,f663]) ).
fof(f1233,plain,
( ~ m1_subset_1(sF31,u1_struct_0(sK2))
| spl36_1
| ~ spl36_12
| ~ spl36_13
| ~ spl36_14
| ~ spl36_16 ),
inference(forward_subsumption_resolution,[],[f1232,f664]) ).
fof(f1234,plain,
( ~ m1_subset_1(sF31,sF35)
| spl36_1
| ~ spl36_12
| ~ spl36_13
| ~ spl36_14
| ~ spl36_16 ),
inference(forward_demodulation,[],[f1233,f667]) ).
fof(f1235,plain,
( $false
| spl36_1
| spl36_3
| ~ spl36_6
| ~ spl36_8
| ~ spl36_12
| ~ spl36_13
| ~ spl36_14
| ~ spl36_16 ),
inference(forward_subsumption_resolution,[],[f1234,f1199]) ).
fof(f1236,plain,
( spl36_1
| spl36_3
| ~ spl36_6
| ~ spl36_8
| ~ spl36_12
| ~ spl36_13
| ~ spl36_14
| ~ spl36_16 ),
inference(avatar_contradiction_clause,[],[f1235]) ).
cnf(s3,plain,
( spl36_3
| spl36_5 ),
inference(sat_conversion,[],[f714]) ).
cnf(s8,plain,
~ spl36_3,
inference(sat_conversion,[],[f770]) ).
cnf(s10,plain,
( spl36_1
| ~ spl36_5
| spl36_16 ),
inference(sat_conversion,[],[f813]) ).
cnf(s11,plain,
~ spl36_1,
inference(sat_conversion,[],[f817]) ).
cnf(s12,plain,
spl36_8,
inference(sat_conversion,[],[f823]) ).
cnf(s13,plain,
spl36_6,
inference(sat_conversion,[],[f825]) ).
cnf(s16,plain,
spl36_14,
inference(sat_conversion,[],[f992]) ).
cnf(s18,plain,
spl36_13,
inference(sat_conversion,[],[f1135]) ).
cnf(s19,plain,
spl36_12,
inference(sat_conversion,[],[f1155]) ).
cnf(s20,plain,
( spl36_1
| spl36_3
| ~ spl36_6
| ~ spl36_8
| ~ spl36_12
| ~ spl36_13
| ~ spl36_14
| ~ spl36_16 ),
inference(sat_conversion,[],[f1236]) ).
cnf(s22,plain,
( ~ spl36_5
| spl36_16 ),
inference(rat,[],[s10,s11]) ).
cnf(s24,plain,
~ spl36_16,
inference(rat,[],[s20,s11,s16,s18,s19,s12,s13,s8]) ).
cnf(s26,plain,
~ spl36_5,
inference(rat,[],[s22,s24]) ).
cnf(s31,plain,
$false,
inference(rat,[],[s3,s26,s8]) ).
fof(f1237,plain,
$false,
inference(avatar_sat_refutation,[],[s31]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT352+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.10/0.44 % Computer : n007.cluster.edu
% 0.10/0.44 % Model : x86_64 x86_64
% 0.10/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.44 % Memory : 8046.5625MB
% 0.10/0.44 % OS : Linux 6.8.0-71-generic
% 0.10/0.44 % CPULimit : 300
% 0.10/0.44 % WCLimit : 300
% 0.10/0.44 % DateTime : Sun Sep 27 14:53:40 UTC 2026
% 0.10/0.44 % CPUTime :
% 0.10/0.44 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.14/0.48 Running first-order theorem proving
% 0.14/0.48 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
% 8.11/2.10 % (1518967)Detected formulas, will run a generic FOF schedule.
% 8.11/2.10 % (1519023)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2275196259:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 8.11/2.10 % (1519023)Refutation not found, incomplete strategy
% 8.11/2.10 % (1519023)------------------------------
% 8.11/2.10 % (1519023)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.11/2.10 % (1519023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.11/2.10 % (1519023)CaDiCaL version: 2.1.3
% 8.11/2.10 % (1519023)Termination reason: Refutation not found, incomplete strategy
% 8.11/2.10 % (1519023)Time elapsed: 0.002 s
% 8.11/2.10 % (1519023)Peak memory usage: 88 MB
% 8.11/2.10 % (1519023)Instructions burned: 4 (million)
% 8.11/2.10 % (1519026)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=159328579:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 8.11/2.10 % (1519027)dis-21_1_sil=8000:lcm=predicate:random_seed=2303968212: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)
% 8.11/2.10 % (1519022)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=3084939332:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 8.11/2.10 % (1519020)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=2511490275:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 8.11/2.10 % (1519021)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=3288282051:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 8.11/2.10 % (1519024)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=380141969:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 8.11/2.10 % (1519024)Refutation not found, incomplete strategy
% 8.11/2.10 % (1519024)------------------------------
% 8.11/2.10 % (1519024)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.11/2.10 % (1519024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.11/2.10 % (1519024)CaDiCaL version: 2.1.3
% 8.11/2.10 % (1519024)Termination reason: Refutation not found, incomplete strategy
% 8.11/2.10 % (1519024)Time elapsed: 0.004 s
% 8.11/2.10 % (1519024)Peak memory usage: 88 MB
% 8.11/2.10 % (1519024)Instructions burned: 5 (million)
% 8.11/2.10 % (1519027)Instruction limit reached!
% 8.11/2.10 % (1519027)------------------------------
% 8.11/2.10 % (1519027)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.11/2.10 % (1519027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.11/2.10 % (1519027)CaDiCaL version: 2.1.3
% 8.11/2.10 % (1519027)Termination reason: Instruction limit
% 8.11/2.10 % (1519027)Termination phase: Saturation
% 8.11/2.10 % (1519027)Time elapsed: 0.071 s
% 8.11/2.10 % (1519027)Peak memory usage: 90 MB
% 8.11/2.10 % (1519027)Instructions burned: 129 (million)
% 8.11/2.10 % (1519026)Instruction limit reached!
% 8.11/2.10 % (1519026)------------------------------
% 8.11/2.10 % (1519026)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.11/2.10 % (1519026)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.11/2.10 % (1519026)CaDiCaL version: 2.1.3
% 8.11/2.10 % (1519026)Termination reason: Instruction limit
% 8.11/2.10 % (1519026)Termination phase: Saturation
% 8.11/2.10 % (1519026)Time elapsed: 0.090 s
% 8.11/2.10 % (1519026)Peak memory usage: 90 MB
% 8.11/2.10 % (1519026)Instructions burned: 140 (million)
% 8.11/2.10 % (1519023)------------------------------
% 8.11/2.10 % (1519023)------------------------------
% 8.11/2.10 % (1519057)lrs+10_1_sil=8000:sp=occurrence:random_seed=2820413375:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 8.11/2.10 % (1519060)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2057122042:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 8.11/2.10 % (1519063)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3987081557:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 8.11/2.10 % (1519024)------------------------------
% 8.11/2.10 % (1519024)------------------------------
% 8.11/2.10 % (1519060)Instruction limit reached!
% 8.11/2.10 % (1519060)------------------------------
% 8.11/2.10 % (1519060)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.11/2.10 % (1519060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.11/2.10 % (1519060)CaDiCaL version: 2.1.3
% 8.11/2.10 % (1519060)Termination reason: Instruction limit
% 8.11/2.10 % (1519060)Termination phase: Saturation
% 8.11/2.10 % (1519060)Time elapsed: 0.085 s
% 8.11/2.10 % (1519060)Peak memory usage: 89 MB
% 8.11/2.10 % (1519060)Instructions burned: 159 (million)
% 8.11/2.10 % (1519063)Instruction limit reached!
% 8.11/2.10 % (1519063)------------------------------
% 8.11/2.10 % (1519063)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.11/2.10 % (1519063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.11/2.10 % (1519063)CaDiCaL version: 2.1.3
% 8.11/2.10 % (1519063)Termination reason: Instruction limit
% 8.11/2.10 % (1519063)Termination phase: Saturation
% 8.11/2.10 % (1519063)Time elapsed: 0.093 s
% 8.11/2.10 % (1519063)Peak memory usage: 91 MB
% 8.11/2.10 % (1519063)Instructions burned: 328 (million)
% 8.11/2.10 % (1519057)Instruction limit reached!
% 8.11/2.10 % (1519057)------------------------------
% 8.11/2.10 % (1519057)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.11/2.10 % (1519057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.11/2.10 % (1519057)CaDiCaL version: 2.1.3
% 8.11/2.10 % (1519057)Termination reason: Instruction limit
% 8.11/2.10 % (1519057)Termination phase: Saturation
% 8.11/2.10 % (1519057)Time elapsed: 0.162 s
% 8.11/2.10 % (1519057)Peak memory usage: 92 MB
% 8.11/2.10 % (1519057)Instructions burned: 285 (million)
% 8.11/2.10 % (1519091)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=48708131:i=2350_2995 on theBenchmark for (2995ds/2350Mi)
% 8.11/2.10 % (1519084)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=269445062:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 8.11/2.10 % (1519089)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1324920565:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 8.11/2.10 % (1519089)Refutation not found, incomplete strategy
% 8.11/2.10 % (1519089)------------------------------
% 8.11/2.10 % (1519089)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.11/2.10 % (1519089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.11/2.10 % (1519089)CaDiCaL version: 2.1.3
% 8.11/2.10 % (1519089)Termination reason: Refutation not found, incomplete strategy
% 8.11/2.10 % (1519089)Time elapsed: 0.011 s
% 8.11/2.10 % (1519089)Peak memory usage: 89 MB
% 8.11/2.10 % (1519089)Instructions burned: 17 (million)
% 8.11/2.10 % (1519097)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3392949126:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 8.11/2.10 % (1519084)Instruction limit reached!
% 8.11/2.10 % (1519084)------------------------------
% 8.11/2.10 % (1519084)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.11/2.10 % (1519084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.11/2.10 % (1519084)CaDiCaL version: 2.1.3
% 8.11/2.10 % (1519084)Termination reason: Instruction limit
% 8.11/2.10 % (1519084)Termination phase: Saturation
% 8.11/2.10 % (1519084)Time elapsed: 0.139 s
% 8.11/2.10 % (1519084)Peak memory usage: 91 MB
% 8.11/2.10 % (1519084)Instructions burned: 249 (million)
% 8.11/2.10 % (1519097)Instruction limit reached!
% 8.11/2.10 % (1519097)------------------------------
% 8.11/2.10 % (1519097)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.11/2.10 % (1519097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.11/2.10 % (1519097)CaDiCaL version: 2.1.3
% 8.11/2.10 % (1519097)Termination reason: Instruction limit
% 8.11/2.10 % (1519097)Termination phase: Saturation
% 8.11/2.10 % (1519097)Time elapsed: 0.059 s
% 8.11/2.10 % (1519097)Peak memory usage: 90 MB
% 8.11/2.10 % (1519097)Instructions burned: 115 (million)
% 8.11/2.10 % (1519089)------------------------------
% 8.11/2.10 % (1519089)------------------------------
% 8.11/2.10 % (1519122)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=225447108:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi)
% 8.11/2.10 % (1519020)First to succeed.
% 8.11/2.10 % (1519020)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1518967"
% 8.11/2.10 % (1519125)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1141461228:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2992 on theBenchmark for (2992ds/114Mi)
% 8.11/2.10 % (1519122)Instruction limit reached!
% 8.11/2.10 % (1519122)------------------------------
% 8.11/2.10 % (1519122)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.11/2.10 % (1519122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.11/2.10 % (1519122)CaDiCaL version: 2.1.3
% 8.11/2.10 % (1519122)Termination reason: Instruction limit
% 8.11/2.10 % (1519122)Termination phase: Saturation
% 8.11/2.10 % (1519122)Time elapsed: 0.064 s
% 8.11/2.10 % (1519122)Peak memory usage: 89 MB
% 8.11/2.10 % (1519122)Instructions burned: 127 (million)
% 8.11/2.10 % (1519125)Instruction limit reached!
% 8.11/2.10 % (1519125)------------------------------
% 8.11/2.10 % (1519125)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.11/2.10 % (1519125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.11/2.10 % (1519125)CaDiCaL version: 2.1.3
% 8.11/2.10 % (1519125)Termination reason: Instruction limit
% 8.11/2.10 % (1519125)Termination phase: Saturation
% 8.11/2.10 % (1519125)Time elapsed: 0.068 s
% 8.11/2.10 % (1519125)Peak memory usage: 89 MB
% 8.11/2.10 % (1519125)Instructions burned: 115 (million)
% 8.11/2.10 % (1519140)lrs+10_1_sil=8000:sp=occurrence:random_seed=853443197:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2991 on theBenchmark for (2991ds/907Mi)
% 8.11/2.10 % (1519021)Also succeeded, but the first one will report.
% 8.11/2.10 % (1519091)Also succeeded, but the first one will report.
% 8.11/2.10 % (1519149)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=164346749:i=437:sd=1:aac=none:ss=included_2990 on theBenchmark for (2990ds/437Mi)
% 8.11/2.10 % (1519149)Refutation not found, incomplete strategy
% 8.11/2.10 % (1519149)------------------------------
% 8.11/2.10 % (1519149)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.11/2.10 % (1519149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.11/2.10 % (1519149)CaDiCaL version: 2.1.3
% 8.11/2.10 % (1519149)Termination reason: Refutation not found, incomplete strategy
% 8.11/2.10 % (1519149)Time elapsed: 0.013 s
% 8.11/2.10 % (1519149)Peak memory usage: 89 MB
% 8.11/2.10 % (1519149)Instructions burned: 21 (million)
% 8.11/2.10 % (1519152)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3938218731:i=5202:ss=axioms:sgt=16_2990 on theBenchmark for (2990ds/5202Mi)
% 8.11/2.10 % (1519020)Refutation found. Thanks to Tanya!
% 8.11/2.10 % SZS status Theorem for theBenchmark
% 8.11/2.10 % SZS output start Proof for theBenchmark
% See solution above
% 8.77/2.29 % (1519020)------------------------------
% 8.77/2.29 % (1519020)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.77/2.29 % (1519020)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.77/2.29 % (1519020)CaDiCaL version: 2.1.3
% 8.77/2.29 % (1519020)Termination reason: Refutation
% 8.77/2.29 % (1519020)Time elapsed: 0.738 s
% 8.77/2.29 % (1519020)Peak memory usage: 130 MB
% 8.77/2.29 % (1519020)Instructions burned: 1107 (million)
% 8.77/2.29 % (1519020)------------------------------
% 8.77/2.29 % (1519020)------------------------------
% 8.77/2.29 % (1518967)Success in time 1.178 s
% 8.77/2.29 % Vampire exiting
%------------------------------------------------------------------------------