%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT354+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n001.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:14 AM UTC 2026
% Result : Theorem 10.55s 2.76s
% Output : Refutation 12.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 47
% Number of leaves : 44
% Syntax : Number of formulae : 449 ( 74 unt; 25 def)
% Number of atoms : 3394 ( 73 equ)
% Maximal formula atoms : 28 ( 7 avg)
% Number of connectives : 5437 (2492 ~;2518 |; 352 &)
% ( 35 <=>; 40 =>; 0 <=; 0 <~>)
% Maximal formula depth : 34 ( 9 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 56 ( 54 usr; 26 prp; 0-3 aty)
% Number of functors : 9 ( 9 usr; 3 con; 0-4 aty)
% Number of variables : 257 ( 0 sgn 251 !; 6 ?)
% 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)) )
=> k1_waybel34(X0,X1,X2) = k2_waybel34(k7_lattice3(X1),k7_lattice3(X0),k3_waybel34(X0,X1,X2)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t4_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)) )
=> k1_waybel34(X0,X1,X2) = k2_waybel34(k7_lattice3(X1),k7_lattice3(X0),k3_waybel34(X0,X1,X2)) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f23,axiom,
! [X0] :
( l1_orders_2(X0)
=> ( v1_lattice3(X0)
=> ~ v3_struct_0(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc1_lattice3) ).
fof(f72,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/sandbox2/benchmark/theBenchmark.p',d1_waybel34) ).
fof(f73,axiom,
! [X0] :
( ( v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& v2_lattice3(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( ( v2_orders_2(X1)
& v3_orders_2(X1)
& v4_orders_2(X1)
& v1_lattice3(X1)
& v2_lattice3(X1)
& l1_orders_2(X1) )
=> ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
& m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0)) )
=> ( ( v3_lattice3(X0)
& v3_lattice3(X1)
& v18_waybel_0(X2,X1,X0) )
=> ! [X3] :
( ( v1_funct_1(X3)
& v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
& m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1)) )
=> ( X3 = k2_waybel34(X0,X1,X2)
<=> v3_waybel_1(k1_waybel_1(X0,X1,X3,X2),X0,X1) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d2_waybel34) ).
fof(f74,axiom,
! [X0] :
( l1_orders_2(X0)
=> ! [X1] :
( l1_orders_2(X1)
=> ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> k3_waybel34(X0,X1,X2) = X2 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d3_waybel34) ).
fof(f79,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/sandbox2/benchmark/theBenchmark.p',dt_k1_waybel34) ).
fof(f86,axiom,
! [X0,X1,X2] :
( ( l1_orders_2(X0)
& l1_orders_2(X1)
& v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> ( v1_funct_1(k3_waybel34(X0,X1,X2))
& v1_funct_2(k3_waybel34(X0,X1,X2),u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
& m2_relset_1(k3_waybel34(X0,X1,X2),u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k3_waybel34) ).
fof(f90,axiom,
! [X0] :
( l1_orders_2(X0)
=> ( v1_orders_2(k7_lattice3(X0))
& l1_orders_2(k7_lattice3(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k7_lattice3) ).
fof(f120,axiom,
! [X0,X1,X2] :
( ( 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)
& 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)
& v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v17_waybel_0(X2,X0,X1)
& m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> ( v1_relat_1(k1_waybel34(X0,X1,X2))
& v1_funct_1(k1_waybel34(X0,X1,X2))
& ~ v1_xboole_0(k1_waybel34(X0,X1,X2))
& v1_funct_2(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0))
& v1_partfun1(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0))
& v18_waybel_0(k1_waybel34(X0,X1,X2),X1,X0)
& v20_waybel_0(k1_waybel34(X0,X1,X2),X1,X0)
& v22_waybel_0(k1_waybel34(X0,X1,X2),X1,X0)
& v5_waybel_1(k1_waybel34(X0,X1,X2),X0,X1)
& v5_orders_3(k1_waybel34(X0,X1,X2),X1,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_waybel34) ).
fof(f122,axiom,
! [X0] :
( ( v2_orders_2(X0)
& l1_orders_2(X0) )
=> ( v1_orders_2(k7_lattice3(X0))
& v2_orders_2(k7_lattice3(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_yellow_7) ).
fof(f127,axiom,
! [X0] :
( ( v3_orders_2(X0)
& l1_orders_2(X0) )
=> ( v1_orders_2(k7_lattice3(X0))
& v3_orders_2(k7_lattice3(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc2_yellow_7) ).
fof(f130,axiom,
! [X0,X1,X2] :
( ( 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)
& 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)
& v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v17_waybel_0(X2,X0,X1)
& m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> ( v1_relat_1(k3_waybel34(X0,X1,X2))
& v1_funct_1(k3_waybel34(X0,X1,X2))
& ~ v1_xboole_0(k3_waybel34(X0,X1,X2))
& v1_funct_2(k3_waybel34(X0,X1,X2),u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
& v1_partfun1(k3_waybel34(X0,X1,X2),u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
& v18_waybel_0(k3_waybel34(X0,X1,X2),k7_lattice3(X0),k7_lattice3(X1))
& v20_waybel_0(k3_waybel34(X0,X1,X2),k7_lattice3(X0),k7_lattice3(X1))
& v22_waybel_0(k3_waybel34(X0,X1,X2),k7_lattice3(X0),k7_lattice3(X1))
& v5_waybel_1(k3_waybel34(X0,X1,X2),k7_lattice3(X1),k7_lattice3(X0))
& v5_orders_3(k3_waybel34(X0,X1,X2),k7_lattice3(X0),k7_lattice3(X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc3_waybel34) ).
fof(f131,axiom,
! [X0] :
( ( v4_orders_2(X0)
& l1_orders_2(X0) )
=> ( v1_orders_2(k7_lattice3(X0))
& v4_orders_2(k7_lattice3(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc3_yellow_7) ).
fof(f132,axiom,
! [X0,X1,X2] :
( ( 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)
& 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)
& v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v18_waybel_0(X2,X0,X1)
& m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> ( v1_relat_1(k3_waybel34(X0,X1,X2))
& v1_funct_1(k3_waybel34(X0,X1,X2))
& ~ v1_xboole_0(k3_waybel34(X0,X1,X2))
& v1_funct_2(k3_waybel34(X0,X1,X2),u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
& v1_partfun1(k3_waybel34(X0,X1,X2),u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
& v17_waybel_0(k3_waybel34(X0,X1,X2),k7_lattice3(X0),k7_lattice3(X1))
& v19_waybel_0(k3_waybel34(X0,X1,X2),k7_lattice3(X0),k7_lattice3(X1))
& v21_waybel_0(k3_waybel34(X0,X1,X2),k7_lattice3(X0),k7_lattice3(X1))
& v4_waybel_1(k3_waybel34(X0,X1,X2),k7_lattice3(X0),k7_lattice3(X1))
& v5_orders_3(k3_waybel34(X0,X1,X2),k7_lattice3(X0),k7_lattice3(X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc4_waybel34) ).
fof(f137,axiom,
! [X0] :
( ( v2_lattice3(X0)
& l1_orders_2(X0) )
=> ( ~ v3_struct_0(k7_lattice3(X0))
& v1_orders_2(k7_lattice3(X0))
& v1_lattice3(k7_lattice3(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc5_yellow_7) ).
fof(f141,axiom,
! [X0] :
( ( v1_lattice3(X0)
& l1_orders_2(X0) )
=> ( ~ v3_struct_0(k7_lattice3(X0))
& v1_orders_2(k7_lattice3(X0))
& v2_lattice3(k7_lattice3(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc6_yellow_7) ).
fof(f144,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_lattice3(X0)
& l1_orders_2(X0) )
=> ( ~ v3_struct_0(k7_lattice3(X0))
& v1_orders_2(k7_lattice3(X0))
& v1_lattice3(k7_lattice3(X0))
& v2_lattice3(k7_lattice3(X0))
& v3_lattice3(k7_lattice3(X0))
& v1_yellow_0(k7_lattice3(X0))
& v2_yellow_0(k7_lattice3(X0))
& v3_yellow_0(k7_lattice3(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc7_yellow_7) ).
fof(f188,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
<=> m1_relset_1(X2,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(f193,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)) )
=> ! [X4] :
( ( v1_funct_1(X4)
& v1_funct_2(X4,u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
& m2_relset_1(X4,u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1))) )
=> ! [X5] :
( ( v1_funct_1(X5)
& v1_funct_2(X5,u1_struct_0(k7_lattice3(X1)),u1_struct_0(k7_lattice3(X0)))
& m2_relset_1(X5,u1_struct_0(k7_lattice3(X1)),u1_struct_0(k7_lattice3(X0))) )
=> ( ( X2 = X4
& X3 = X5 )
=> ( v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1)
<=> v3_waybel_1(k1_waybel_1(k7_lattice3(X1),k7_lattice3(X0),X5,X4),k7_lattice3(X1),k7_lattice3(X0)) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t44_yellow_7) ).
fof(f200,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( k1_waybel34(X0,X1,X2) != k2_waybel34(k7_lattice3(X1),k7_lattice3(X0),k3_waybel34(X0,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)) )
& 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(f201,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( k1_waybel34(X0,X1,X2) != k2_waybel34(k7_lattice3(X1),k7_lattice3(X0),k3_waybel34(X0,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)) )
& 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,[],[f200]) ).
fof(f229,plain,
! [X0] :
( ~ v3_struct_0(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f23]) ).
fof(f230,plain,
! [X0] :
( ~ v3_struct_0(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f229]) ).
fof(f318,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,[],[f72]) ).
fof(f319,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,[],[f318]) ).
fof(f320,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( X3 = k2_waybel34(X0,X1,X2)
<=> v3_waybel_1(k1_waybel_1(X0,X1,X3,X2),X0,X1) )
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1)) )
| ~ v3_lattice3(X0)
| ~ v3_lattice3(X1)
| ~ v18_waybel_0(X2,X1,X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0)) )
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ l1_orders_2(X1) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f73]) ).
fof(f321,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( X3 = k2_waybel34(X0,X1,X2)
<=> v3_waybel_1(k1_waybel_1(X0,X1,X3,X2),X0,X1) )
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1)) )
| ~ v3_lattice3(X0)
| ~ v3_lattice3(X1)
| ~ v18_waybel_0(X2,X1,X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0)) )
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ l1_orders_2(X1) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f320]) ).
fof(f322,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( k3_waybel34(X0,X1,X2) = X2
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| ~ l1_orders_2(X1) )
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f74]) ).
fof(f323,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( k3_waybel34(X0,X1,X2) = X2
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| ~ l1_orders_2(X1) )
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f322]) ).
fof(f326,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,[],[f79]) ).
fof(f327,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,[],[f326]) ).
fof(f332,plain,
! [X0,X1,X2] :
( ( v1_funct_1(k3_waybel34(X0,X1,X2))
& v1_funct_2(k3_waybel34(X0,X1,X2),u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
& m2_relset_1(k3_waybel34(X0,X1,X2),u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1))) )
| ~ l1_orders_2(X0)
| ~ 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,[],[f86]) ).
fof(f333,plain,
! [X0,X1,X2] :
( ( v1_funct_1(k3_waybel34(X0,X1,X2))
& v1_funct_2(k3_waybel34(X0,X1,X2),u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
& m2_relset_1(k3_waybel34(X0,X1,X2),u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1))) )
| ~ l1_orders_2(X0)
| ~ 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,[],[f332]) ).
fof(f336,plain,
! [X0] :
( ( v1_orders_2(k7_lattice3(X0))
& l1_orders_2(k7_lattice3(X0)) )
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f90]) ).
fof(f368,plain,
! [X0,X1,X2] :
( ( v1_relat_1(k1_waybel34(X0,X1,X2))
& v1_funct_1(k1_waybel34(X0,X1,X2))
& ~ v1_xboole_0(k1_waybel34(X0,X1,X2))
& v1_funct_2(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0))
& v1_partfun1(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0))
& v18_waybel_0(k1_waybel34(X0,X1,X2),X1,X0)
& v20_waybel_0(k1_waybel34(X0,X1,X2),X1,X0)
& v22_waybel_0(k1_waybel34(X0,X1,X2),X1,X0)
& v5_waybel_1(k1_waybel34(X0,X1,X2),X0,X1)
& v5_orders_3(k1_waybel34(X0,X1,X2),X1,X0) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0)
| ~ 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)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v17_waybel_0(X2,X0,X1)
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(ennf_transformation,[],[f120]) ).
fof(f369,plain,
! [X0,X1,X2] :
( ( v1_relat_1(k1_waybel34(X0,X1,X2))
& v1_funct_1(k1_waybel34(X0,X1,X2))
& ~ v1_xboole_0(k1_waybel34(X0,X1,X2))
& v1_funct_2(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0))
& v1_partfun1(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0))
& v18_waybel_0(k1_waybel34(X0,X1,X2),X1,X0)
& v20_waybel_0(k1_waybel34(X0,X1,X2),X1,X0)
& v22_waybel_0(k1_waybel34(X0,X1,X2),X1,X0)
& v5_waybel_1(k1_waybel34(X0,X1,X2),X0,X1)
& v5_orders_3(k1_waybel34(X0,X1,X2),X1,X0) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0)
| ~ 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)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v17_waybel_0(X2,X0,X1)
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(flattening,[],[f368]) ).
fof(f371,plain,
! [X0] :
( ( v1_orders_2(k7_lattice3(X0))
& v2_orders_2(k7_lattice3(X0)) )
| ~ v2_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f122]) ).
fof(f372,plain,
! [X0] :
( ( v1_orders_2(k7_lattice3(X0))
& v2_orders_2(k7_lattice3(X0)) )
| ~ v2_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f371]) ).
fof(f378,plain,
! [X0] :
( ( v1_orders_2(k7_lattice3(X0))
& v3_orders_2(k7_lattice3(X0)) )
| ~ v3_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f127]) ).
fof(f379,plain,
! [X0] :
( ( v1_orders_2(k7_lattice3(X0))
& v3_orders_2(k7_lattice3(X0)) )
| ~ v3_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f378]) ).
fof(f384,plain,
! [X0,X1,X2] :
( ( v1_relat_1(k3_waybel34(X0,X1,X2))
& v1_funct_1(k3_waybel34(X0,X1,X2))
& ~ v1_xboole_0(k3_waybel34(X0,X1,X2))
& v1_funct_2(k3_waybel34(X0,X1,X2),u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
& v1_partfun1(k3_waybel34(X0,X1,X2),u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
& v18_waybel_0(k3_waybel34(X0,X1,X2),k7_lattice3(X0),k7_lattice3(X1))
& v20_waybel_0(k3_waybel34(X0,X1,X2),k7_lattice3(X0),k7_lattice3(X1))
& v22_waybel_0(k3_waybel34(X0,X1,X2),k7_lattice3(X0),k7_lattice3(X1))
& v5_waybel_1(k3_waybel34(X0,X1,X2),k7_lattice3(X1),k7_lattice3(X0))
& v5_orders_3(k3_waybel34(X0,X1,X2),k7_lattice3(X0),k7_lattice3(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)
| ~ 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)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v17_waybel_0(X2,X0,X1)
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(ennf_transformation,[],[f130]) ).
fof(f385,plain,
! [X0,X1,X2] :
( ( v1_relat_1(k3_waybel34(X0,X1,X2))
& v1_funct_1(k3_waybel34(X0,X1,X2))
& ~ v1_xboole_0(k3_waybel34(X0,X1,X2))
& v1_funct_2(k3_waybel34(X0,X1,X2),u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
& v1_partfun1(k3_waybel34(X0,X1,X2),u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
& v18_waybel_0(k3_waybel34(X0,X1,X2),k7_lattice3(X0),k7_lattice3(X1))
& v20_waybel_0(k3_waybel34(X0,X1,X2),k7_lattice3(X0),k7_lattice3(X1))
& v22_waybel_0(k3_waybel34(X0,X1,X2),k7_lattice3(X0),k7_lattice3(X1))
& v5_waybel_1(k3_waybel34(X0,X1,X2),k7_lattice3(X1),k7_lattice3(X0))
& v5_orders_3(k3_waybel34(X0,X1,X2),k7_lattice3(X0),k7_lattice3(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)
| ~ 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)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v17_waybel_0(X2,X0,X1)
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(flattening,[],[f384]) ).
fof(f386,plain,
! [X0] :
( ( v1_orders_2(k7_lattice3(X0))
& v4_orders_2(k7_lattice3(X0)) )
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f131]) ).
fof(f387,plain,
! [X0] :
( ( v1_orders_2(k7_lattice3(X0))
& v4_orders_2(k7_lattice3(X0)) )
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f386]) ).
fof(f388,plain,
! [X0,X1,X2] :
( ( v1_relat_1(k3_waybel34(X0,X1,X2))
& v1_funct_1(k3_waybel34(X0,X1,X2))
& ~ v1_xboole_0(k3_waybel34(X0,X1,X2))
& v1_funct_2(k3_waybel34(X0,X1,X2),u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
& v1_partfun1(k3_waybel34(X0,X1,X2),u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
& v17_waybel_0(k3_waybel34(X0,X1,X2),k7_lattice3(X0),k7_lattice3(X1))
& v19_waybel_0(k3_waybel34(X0,X1,X2),k7_lattice3(X0),k7_lattice3(X1))
& v21_waybel_0(k3_waybel34(X0,X1,X2),k7_lattice3(X0),k7_lattice3(X1))
& v4_waybel_1(k3_waybel34(X0,X1,X2),k7_lattice3(X0),k7_lattice3(X1))
& v5_orders_3(k3_waybel34(X0,X1,X2),k7_lattice3(X0),k7_lattice3(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)
| ~ 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)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v18_waybel_0(X2,X0,X1)
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(ennf_transformation,[],[f132]) ).
fof(f389,plain,
! [X0,X1,X2] :
( ( v1_relat_1(k3_waybel34(X0,X1,X2))
& v1_funct_1(k3_waybel34(X0,X1,X2))
& ~ v1_xboole_0(k3_waybel34(X0,X1,X2))
& v1_funct_2(k3_waybel34(X0,X1,X2),u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
& v1_partfun1(k3_waybel34(X0,X1,X2),u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
& v17_waybel_0(k3_waybel34(X0,X1,X2),k7_lattice3(X0),k7_lattice3(X1))
& v19_waybel_0(k3_waybel34(X0,X1,X2),k7_lattice3(X0),k7_lattice3(X1))
& v21_waybel_0(k3_waybel34(X0,X1,X2),k7_lattice3(X0),k7_lattice3(X1))
& v4_waybel_1(k3_waybel34(X0,X1,X2),k7_lattice3(X0),k7_lattice3(X1))
& v5_orders_3(k3_waybel34(X0,X1,X2),k7_lattice3(X0),k7_lattice3(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)
| ~ 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)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v18_waybel_0(X2,X0,X1)
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(flattening,[],[f388]) ).
fof(f398,plain,
! [X0] :
( ( ~ v3_struct_0(k7_lattice3(X0))
& v1_orders_2(k7_lattice3(X0))
& v1_lattice3(k7_lattice3(X0)) )
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f137]) ).
fof(f399,plain,
! [X0] :
( ( ~ v3_struct_0(k7_lattice3(X0))
& v1_orders_2(k7_lattice3(X0))
& v1_lattice3(k7_lattice3(X0)) )
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f398]) ).
fof(f404,plain,
! [X0] :
( ( ~ v3_struct_0(k7_lattice3(X0))
& v1_orders_2(k7_lattice3(X0))
& v2_lattice3(k7_lattice3(X0)) )
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f141]) ).
fof(f405,plain,
! [X0] :
( ( ~ v3_struct_0(k7_lattice3(X0))
& v1_orders_2(k7_lattice3(X0))
& v2_lattice3(k7_lattice3(X0)) )
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f404]) ).
fof(f409,plain,
! [X0] :
( ( ~ v3_struct_0(k7_lattice3(X0))
& v1_orders_2(k7_lattice3(X0))
& v1_lattice3(k7_lattice3(X0))
& v2_lattice3(k7_lattice3(X0))
& v3_lattice3(k7_lattice3(X0))
& v1_yellow_0(k7_lattice3(X0))
& v2_yellow_0(k7_lattice3(X0))
& v3_yellow_0(k7_lattice3(X0)) )
| v3_struct_0(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f144]) ).
fof(f410,plain,
! [X0] :
( ( ~ v3_struct_0(k7_lattice3(X0))
& v1_orders_2(k7_lattice3(X0))
& v1_lattice3(k7_lattice3(X0))
& v2_lattice3(k7_lattice3(X0))
& v3_lattice3(k7_lattice3(X0))
& v1_yellow_0(k7_lattice3(X0))
& v2_yellow_0(k7_lattice3(X0))
& v3_yellow_0(k7_lattice3(X0)) )
| v3_struct_0(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f409]) ).
fof(f451,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( ( v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1)
<=> v3_waybel_1(k1_waybel_1(k7_lattice3(X1),k7_lattice3(X0),X5,X4),k7_lattice3(X1),k7_lattice3(X0)) )
| X2 != X4
| X3 != X5
| ~ v1_funct_1(X5)
| ~ v1_funct_2(X5,u1_struct_0(k7_lattice3(X1)),u1_struct_0(k7_lattice3(X0)))
| ~ m2_relset_1(X5,u1_struct_0(k7_lattice3(X1)),u1_struct_0(k7_lattice3(X0))) )
| ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
| ~ m2_relset_1(X4,u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(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,[],[f193]) ).
fof(f452,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( ( v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1)
<=> v3_waybel_1(k1_waybel_1(k7_lattice3(X1),k7_lattice3(X0),X5,X4),k7_lattice3(X1),k7_lattice3(X0)) )
| X2 != X4
| X3 != X5
| ~ v1_funct_1(X5)
| ~ v1_funct_2(X5,u1_struct_0(k7_lattice3(X1)),u1_struct_0(k7_lattice3(X0)))
| ~ m2_relset_1(X5,u1_struct_0(k7_lattice3(X1)),u1_struct_0(k7_lattice3(X0))) )
| ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
| ~ m2_relset_1(X4,u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(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,[],[f451]) ).
fof(f459,plain,
( k1_waybel34(sK0,sK1,sK2) != k2_waybel34(k7_lattice3(sK1),k7_lattice3(sK0),k3_waybel34(sK0,sK1,sK2))
& v1_funct_1(sK2)
& v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
& v17_waybel_0(sK2,sK0,sK1)
& m2_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
& v2_orders_2(sK1)
& v3_orders_2(sK1)
& v4_orders_2(sK1)
& v1_lattice3(sK1)
& v2_lattice3(sK1)
& v3_lattice3(sK1)
& l1_orders_2(sK1)
& v2_orders_2(sK0)
& v3_orders_2(sK0)
& v4_orders_2(sK0)
& v1_lattice3(sK0)
& v2_lattice3(sK0)
& v3_lattice3(sK0)
& l1_orders_2(sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2)],[f201]) ).
fof(f460,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,[],[f319]) ).
fof(f461,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( ( X3 = k2_waybel34(X0,X1,X2)
| ~ v3_waybel_1(k1_waybel_1(X0,X1,X3,X2),X0,X1) )
& ( v3_waybel_1(k1_waybel_1(X0,X1,X3,X2),X0,X1)
| k2_waybel34(X0,X1,X2) != X3 ) )
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1)) )
| ~ v3_lattice3(X0)
| ~ v3_lattice3(X1)
| ~ v18_waybel_0(X2,X1,X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0)) )
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ l1_orders_2(X1) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(nnf_transformation,[],[f321]) ).
fof(f500,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,[],[f188]) ).
fof(f502,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( ( ( v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1)
| ~ v3_waybel_1(k1_waybel_1(k7_lattice3(X1),k7_lattice3(X0),X5,X4),k7_lattice3(X1),k7_lattice3(X0)) )
& ( v3_waybel_1(k1_waybel_1(k7_lattice3(X1),k7_lattice3(X0),X5,X4),k7_lattice3(X1),k7_lattice3(X0))
| ~ v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1) ) )
| X2 != X4
| X3 != X5
| ~ v1_funct_1(X5)
| ~ v1_funct_2(X5,u1_struct_0(k7_lattice3(X1)),u1_struct_0(k7_lattice3(X0)))
| ~ m2_relset_1(X5,u1_struct_0(k7_lattice3(X1)),u1_struct_0(k7_lattice3(X0))) )
| ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
| ~ m2_relset_1(X4,u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(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,[],[f452]) ).
fof(f503,plain,
l1_orders_2(sK0),
inference(cnf_transformation,[],[f459]) ).
fof(f504,plain,
v3_lattice3(sK0),
inference(cnf_transformation,[],[f459]) ).
fof(f505,plain,
v2_lattice3(sK0),
inference(cnf_transformation,[],[f459]) ).
fof(f506,plain,
v1_lattice3(sK0),
inference(cnf_transformation,[],[f459]) ).
fof(f507,plain,
v4_orders_2(sK0),
inference(cnf_transformation,[],[f459]) ).
fof(f508,plain,
v3_orders_2(sK0),
inference(cnf_transformation,[],[f459]) ).
fof(f509,plain,
v2_orders_2(sK0),
inference(cnf_transformation,[],[f459]) ).
fof(f510,plain,
l1_orders_2(sK1),
inference(cnf_transformation,[],[f459]) ).
fof(f511,plain,
v3_lattice3(sK1),
inference(cnf_transformation,[],[f459]) ).
fof(f512,plain,
v2_lattice3(sK1),
inference(cnf_transformation,[],[f459]) ).
fof(f513,plain,
v1_lattice3(sK1),
inference(cnf_transformation,[],[f459]) ).
fof(f514,plain,
v4_orders_2(sK1),
inference(cnf_transformation,[],[f459]) ).
fof(f515,plain,
v3_orders_2(sK1),
inference(cnf_transformation,[],[f459]) ).
fof(f516,plain,
v2_orders_2(sK1),
inference(cnf_transformation,[],[f459]) ).
fof(f517,plain,
m2_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1)),
inference(cnf_transformation,[],[f459]) ).
fof(f518,plain,
v17_waybel_0(sK2,sK0,sK1),
inference(cnf_transformation,[],[f459]) ).
fof(f519,plain,
v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1)),
inference(cnf_transformation,[],[f459]) ).
fof(f520,plain,
v1_funct_1(sK2),
inference(cnf_transformation,[],[f459]) ).
fof(f521,plain,
k1_waybel34(sK0,sK1,sK2) != k2_waybel34(k7_lattice3(sK1),k7_lattice3(sK0),k3_waybel34(sK0,sK1,sK2)),
inference(cnf_transformation,[],[f459]) ).
fof(f591,plain,
! [X0] :
( ~ v3_struct_0(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f230]) ).
fof(f819,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,[],[f460]) ).
fof(f822,plain,
! [X2,X3,X0,X1] :
( ~ m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v3_waybel_1(k1_waybel_1(X0,X1,X3,X2),X0,X1)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
| k2_waybel34(X0,X1,X2) = X3
| ~ v3_lattice3(X0)
| ~ v3_lattice3(X1)
| ~ v18_waybel_0(X2,X1,X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ l1_orders_2(X1)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f461]) ).
fof(f823,plain,
! [X2,X0,X1] :
( ~ v1_funct_1(X2)
| k3_waybel34(X0,X1,X2) = 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))
| ~ l1_orders_2(X1)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f323]) ).
fof(f828,plain,
! [X2,X0,X1] :
( ~ v1_funct_1(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)
| m2_relset_1(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0))
| ~ 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,[],[f327]) ).
fof(f830,plain,
! [X2,X0,X1] :
( ~ v1_funct_1(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(k1_waybel34(X0,X1,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,[],[f327]) ).
fof(f835,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ l1_orders_2(X0)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| m2_relset_1(k3_waybel34(X0,X1,X2),u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1))) ),
inference(cnf_transformation,[],[f333]) ).
fof(f836,plain,
! [X2,X0,X1] :
( v1_funct_2(k3_waybel34(X0,X1,X2),u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
| ~ l1_orders_2(X0)
| ~ 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,[],[f333]) ).
fof(f837,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ l1_orders_2(X0)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| v1_funct_1(k3_waybel34(X0,X1,X2)) ),
inference(cnf_transformation,[],[f333]) ).
fof(f840,plain,
! [X0] :
( l1_orders_2(k7_lattice3(X0))
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f336]) ).
fof(f921,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)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ v3_lattice3(X1)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v17_waybel_0(X2,X0,X1)
| v18_waybel_0(k1_waybel34(X0,X1,X2),X1,X0) ),
inference(cnf_transformation,[],[f369]) ).
fof(f923,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)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ v3_lattice3(X1)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v17_waybel_0(X2,X0,X1)
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f369]) ).
fof(f925,plain,
! [X2,X0,X1] :
( ~ v17_waybel_0(X2,X0,X1)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0)
| ~ 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)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| v1_funct_1(k1_waybel34(X0,X1,X2))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f369]) ).
fof(f930,plain,
! [X0] :
( v2_orders_2(k7_lattice3(X0))
| ~ v2_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f372]) ).
fof(f952,plain,
! [X0] :
( v3_orders_2(k7_lattice3(X0))
| ~ v3_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f379]) ).
fof(f962,plain,
! [X2,X0,X1] :
( v18_waybel_0(k3_waybel34(X0,X1,X2),k7_lattice3(X0),k7_lattice3(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)
| ~ 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)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v17_waybel_0(X2,X0,X1)
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f385]) ).
fof(f968,plain,
! [X0] :
( v4_orders_2(k7_lattice3(X0))
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f387]) ).
fof(f976,plain,
! [X2,X0,X1] :
( v1_funct_2(k3_waybel34(X0,X1,X2),u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(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)
| ~ 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)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v18_waybel_0(X2,X0,X1)
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f389]) ).
fof(f992,plain,
! [X0] :
( v1_lattice3(k7_lattice3(X0))
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f399]) ).
fof(f1005,plain,
! [X0] :
( v2_lattice3(k7_lattice3(X0))
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f405]) ).
fof(f1014,plain,
! [X0] :
( v3_lattice3(k7_lattice3(X0))
| v3_struct_0(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f410]) ).
fof(f1305,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f500]) ).
fof(f1312,plain,
! [X2,X3,X0,X1,X4,X5] :
( v3_waybel_1(k1_waybel_1(k7_lattice3(X1),k7_lattice3(X0),X5,X4),k7_lattice3(X1),k7_lattice3(X0))
| ~ v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1)
| X2 != X4
| X3 != X5
| ~ v1_funct_1(X5)
| ~ v1_funct_2(X5,u1_struct_0(k7_lattice3(X1)),u1_struct_0(k7_lattice3(X0)))
| ~ m2_relset_1(X5,u1_struct_0(k7_lattice3(X1)),u1_struct_0(k7_lattice3(X0)))
| ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
| ~ m2_relset_1(X4,u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(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,[],[f502]) ).
fof(f1320,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(k1_waybel34(X0,X1,X2))
| ~ v1_funct_2(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0))
| v3_waybel_1(k1_waybel_1(X0,X1,X2,k1_waybel34(X0,X1,X2)),X0,X1)
| ~ 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,[],[f819]) ).
fof(f1324,plain,
! [X3,X0,X1,X4,X5] :
( v3_waybel_1(k1_waybel_1(k7_lattice3(X1),k7_lattice3(X0),X5,X4),k7_lattice3(X1),k7_lattice3(X0))
| ~ v3_waybel_1(k1_waybel_1(X0,X1,X4,X3),X0,X1)
| X3 != X5
| ~ v1_funct_1(X5)
| ~ v1_funct_2(X5,u1_struct_0(k7_lattice3(X1)),u1_struct_0(k7_lattice3(X0)))
| ~ m2_relset_1(X5,u1_struct_0(k7_lattice3(X1)),u1_struct_0(k7_lattice3(X0)))
| ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
| ~ m2_relset_1(X4,u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(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(X4)
| ~ v1_funct_2(X4,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X4,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(equality_resolution,[],[f1312]) ).
fof(f1325,plain,
! [X0,X1,X4,X5] :
( v3_waybel_1(k1_waybel_1(k7_lattice3(X1),k7_lattice3(X0),X5,X4),k7_lattice3(X1),k7_lattice3(X0))
| ~ v3_waybel_1(k1_waybel_1(X0,X1,X4,X5),X0,X1)
| ~ v1_funct_1(X5)
| ~ v1_funct_2(X5,u1_struct_0(k7_lattice3(X1)),u1_struct_0(k7_lattice3(X0)))
| ~ m2_relset_1(X5,u1_struct_0(k7_lattice3(X1)),u1_struct_0(k7_lattice3(X0)))
| ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
| ~ m2_relset_1(X4,u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
| ~ v1_funct_1(X5)
| ~ v1_funct_2(X5,u1_struct_0(X1),u1_struct_0(X0))
| ~ m2_relset_1(X5,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X4,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(equality_resolution,[],[f1324]) ).
fof(f1326,plain,
! [X0,X1,X4,X5] :
( v3_waybel_1(k1_waybel_1(k7_lattice3(X1),k7_lattice3(X0),X5,X4),k7_lattice3(X1),k7_lattice3(X0))
| ~ v3_waybel_1(k1_waybel_1(X0,X1,X4,X5),X0,X1)
| ~ v1_funct_1(X5)
| ~ v1_funct_2(X5,u1_struct_0(k7_lattice3(X1)),u1_struct_0(k7_lattice3(X0)))
| ~ m2_relset_1(X5,u1_struct_0(k7_lattice3(X1)),u1_struct_0(k7_lattice3(X0)))
| ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
| ~ m2_relset_1(X4,u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
| ~ v1_funct_2(X5,u1_struct_0(X1),u1_struct_0(X0))
| ~ m2_relset_1(X5,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X4,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X4,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(duplicate_literal_removal,[],[f1325]) ).
fof(f1365,plain,
! [X0,X1] :
( ~ m2_relset_1(sK2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(sK2,u1_struct_0(X0),u1_struct_0(X1))
| sK2 = k3_waybel34(X0,X1,sK2)
| ~ l1_orders_2(X1)
| ~ l1_orders_2(X0) ),
inference(resolution,[],[f823,f520]) ).
fof(f1369,plain,
m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1)),
inference(resolution,[],[f1305,f517]) ).
fof(f1370,plain,
( ~ v2_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v4_orders_2(sK0)
| ~ v1_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v3_lattice3(sK0)
| ~ l1_orders_2(sK0)
| ~ v2_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ v3_lattice3(sK1)
| ~ l1_orders_2(sK1)
| ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v17_waybel_0(sK2,sK0,sK1)
| v18_waybel_0(k1_waybel34(sK0,sK1,sK2),sK1,sK0) ),
inference(resolution,[],[f1369,f921]) ).
fof(f1371,plain,
( ~ l1_orders_2(sK0)
| ~ l1_orders_2(sK1)
| ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| m2_relset_1(k3_waybel34(sK0,sK1,sK2),u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1))) ),
inference(resolution,[],[f1369,f835]) ).
fof(f1376,plain,
( ~ l1_orders_2(sK1)
| ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| m2_relset_1(k3_waybel34(sK0,sK1,sK2),u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1))) ),
inference(forward_subsumption_resolution,[],[f1371,f503]) ).
fof(f1377,plain,
( ~ v3_orders_2(sK0)
| ~ v4_orders_2(sK0)
| ~ v1_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v3_lattice3(sK0)
| ~ l1_orders_2(sK0)
| ~ v2_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ v3_lattice3(sK1)
| ~ l1_orders_2(sK1)
| ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v17_waybel_0(sK2,sK0,sK1)
| v18_waybel_0(k1_waybel34(sK0,sK1,sK2),sK1,sK0) ),
inference(forward_subsumption_resolution,[],[f1370,f509]) ).
fof(f1380,plain,
( ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| m2_relset_1(k3_waybel34(sK0,sK1,sK2),u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1))) ),
inference(forward_subsumption_resolution,[],[f1376,f510]) ).
fof(f1381,plain,
( ~ v4_orders_2(sK0)
| ~ v1_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v3_lattice3(sK0)
| ~ l1_orders_2(sK0)
| ~ v2_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ v3_lattice3(sK1)
| ~ l1_orders_2(sK1)
| ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v17_waybel_0(sK2,sK0,sK1)
| v18_waybel_0(k1_waybel34(sK0,sK1,sK2),sK1,sK0) ),
inference(forward_subsumption_resolution,[],[f1377,f508]) ).
fof(f1384,plain,
( ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| m2_relset_1(k3_waybel34(sK0,sK1,sK2),u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1))) ),
inference(forward_subsumption_resolution,[],[f1380,f520]) ).
fof(f1385,plain,
( ~ v1_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v3_lattice3(sK0)
| ~ l1_orders_2(sK0)
| ~ v2_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ v3_lattice3(sK1)
| ~ l1_orders_2(sK1)
| ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v17_waybel_0(sK2,sK0,sK1)
| v18_waybel_0(k1_waybel34(sK0,sK1,sK2),sK1,sK0) ),
inference(forward_subsumption_resolution,[],[f1381,f507]) ).
fof(f1388,plain,
m2_relset_1(k3_waybel34(sK0,sK1,sK2),u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1))),
inference(forward_subsumption_resolution,[],[f1384,f519]) ).
fof(f1389,plain,
( ~ v2_lattice3(sK0)
| ~ v3_lattice3(sK0)
| ~ l1_orders_2(sK0)
| ~ v2_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ v3_lattice3(sK1)
| ~ l1_orders_2(sK1)
| ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v17_waybel_0(sK2,sK0,sK1)
| v18_waybel_0(k1_waybel34(sK0,sK1,sK2),sK1,sK0) ),
inference(forward_subsumption_resolution,[],[f1385,f506]) ).
fof(f1391,plain,
( ~ v3_lattice3(sK0)
| ~ l1_orders_2(sK0)
| ~ v2_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ v3_lattice3(sK1)
| ~ l1_orders_2(sK1)
| ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v17_waybel_0(sK2,sK0,sK1)
| v18_waybel_0(k1_waybel34(sK0,sK1,sK2),sK1,sK0) ),
inference(forward_subsumption_resolution,[],[f1389,f505]) ).
fof(f1393,plain,
( ~ l1_orders_2(sK0)
| ~ v2_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ v3_lattice3(sK1)
| ~ l1_orders_2(sK1)
| ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v17_waybel_0(sK2,sK0,sK1)
| v18_waybel_0(k1_waybel34(sK0,sK1,sK2),sK1,sK0) ),
inference(forward_subsumption_resolution,[],[f1391,f504]) ).
fof(f1395,plain,
( ~ v2_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ v3_lattice3(sK1)
| ~ l1_orders_2(sK1)
| ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v17_waybel_0(sK2,sK0,sK1)
| v18_waybel_0(k1_waybel34(sK0,sK1,sK2),sK1,sK0) ),
inference(forward_subsumption_resolution,[],[f1393,f503]) ).
fof(f1397,plain,
( ~ v3_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ v3_lattice3(sK1)
| ~ l1_orders_2(sK1)
| ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v17_waybel_0(sK2,sK0,sK1)
| v18_waybel_0(k1_waybel34(sK0,sK1,sK2),sK1,sK0) ),
inference(forward_subsumption_resolution,[],[f1395,f516]) ).
fof(f1399,plain,
( ~ v4_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ v3_lattice3(sK1)
| ~ l1_orders_2(sK1)
| ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v17_waybel_0(sK2,sK0,sK1)
| v18_waybel_0(k1_waybel34(sK0,sK1,sK2),sK1,sK0) ),
inference(forward_subsumption_resolution,[],[f1397,f515]) ).
fof(f1401,plain,
( ~ v1_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ v3_lattice3(sK1)
| ~ l1_orders_2(sK1)
| ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v17_waybel_0(sK2,sK0,sK1)
| v18_waybel_0(k1_waybel34(sK0,sK1,sK2),sK1,sK0) ),
inference(forward_subsumption_resolution,[],[f1399,f514]) ).
fof(f1403,plain,
( ~ v2_lattice3(sK1)
| ~ v3_lattice3(sK1)
| ~ l1_orders_2(sK1)
| ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v17_waybel_0(sK2,sK0,sK1)
| v18_waybel_0(k1_waybel34(sK0,sK1,sK2),sK1,sK0) ),
inference(forward_subsumption_resolution,[],[f1401,f513]) ).
fof(f1405,plain,
( ~ v3_lattice3(sK1)
| ~ l1_orders_2(sK1)
| ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v17_waybel_0(sK2,sK0,sK1)
| v18_waybel_0(k1_waybel34(sK0,sK1,sK2),sK1,sK0) ),
inference(forward_subsumption_resolution,[],[f1403,f512]) ).
fof(f1407,plain,
( ~ l1_orders_2(sK1)
| ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v17_waybel_0(sK2,sK0,sK1)
| v18_waybel_0(k1_waybel34(sK0,sK1,sK2),sK1,sK0) ),
inference(forward_subsumption_resolution,[],[f1405,f511]) ).
fof(f1409,plain,
( ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v17_waybel_0(sK2,sK0,sK1)
| v18_waybel_0(k1_waybel34(sK0,sK1,sK2),sK1,sK0) ),
inference(forward_subsumption_resolution,[],[f1407,f510]) ).
fof(f1411,plain,
( ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v17_waybel_0(sK2,sK0,sK1)
| v18_waybel_0(k1_waybel34(sK0,sK1,sK2),sK1,sK0) ),
inference(forward_subsumption_resolution,[],[f1409,f520]) ).
fof(f1413,plain,
( ~ v17_waybel_0(sK2,sK0,sK1)
| v18_waybel_0(k1_waybel34(sK0,sK1,sK2),sK1,sK0) ),
inference(forward_subsumption_resolution,[],[f1411,f519]) ).
fof(f1415,plain,
v18_waybel_0(k1_waybel34(sK0,sK1,sK2),sK1,sK0),
inference(forward_subsumption_resolution,[],[f1413,f518]) ).
fof(f1424,definition,
( spl41_1
<=> l1_orders_2(k7_lattice3(sK0)) ),
introduced(definition,[new_symbols(definition,[spl41_1])],[avatar_definition]) ).
fof(f1425,plain,
( ~ l1_orders_2(k7_lattice3(sK0))
| spl41_1 ),
inference(avatar_component_clause,[],[f1424]) ).
fof(f1427,definition,
( spl41_2
<=> v2_lattice3(k7_lattice3(sK0)) ),
introduced(definition,[new_symbols(definition,[spl41_2])],[avatar_definition]) ).
fof(f1428,plain,
( ~ v2_lattice3(k7_lattice3(sK0))
| spl41_2 ),
inference(avatar_component_clause,[],[f1427]) ).
fof(f1430,definition,
( spl41_3
<=> v1_lattice3(k7_lattice3(sK0)) ),
introduced(definition,[new_symbols(definition,[spl41_3])],[avatar_definition]) ).
fof(f1431,plain,
( ~ v1_lattice3(k7_lattice3(sK0))
| spl41_3 ),
inference(avatar_component_clause,[],[f1430]) ).
fof(f1433,definition,
( spl41_4
<=> v4_orders_2(k7_lattice3(sK0)) ),
introduced(definition,[new_symbols(definition,[spl41_4])],[avatar_definition]) ).
fof(f1434,plain,
( ~ v4_orders_2(k7_lattice3(sK0))
| spl41_4 ),
inference(avatar_component_clause,[],[f1433]) ).
fof(f1436,definition,
( spl41_5
<=> v3_orders_2(k7_lattice3(sK0)) ),
introduced(definition,[new_symbols(definition,[spl41_5])],[avatar_definition]) ).
fof(f1437,plain,
( ~ v3_orders_2(k7_lattice3(sK0))
| spl41_5 ),
inference(avatar_component_clause,[],[f1436]) ).
fof(f1439,definition,
( spl41_6
<=> v2_orders_2(k7_lattice3(sK0)) ),
introduced(definition,[new_symbols(definition,[spl41_6])],[avatar_definition]) ).
fof(f1440,plain,
( ~ v2_orders_2(k7_lattice3(sK0))
| spl41_6 ),
inference(avatar_component_clause,[],[f1439]) ).
fof(f1442,definition,
( spl41_7
<=> l1_orders_2(k7_lattice3(sK1)) ),
introduced(definition,[new_symbols(definition,[spl41_7])],[avatar_definition]) ).
fof(f1443,plain,
( ~ l1_orders_2(k7_lattice3(sK1))
| spl41_7 ),
inference(avatar_component_clause,[],[f1442]) ).
fof(f1445,definition,
( spl41_8
<=> v2_lattice3(k7_lattice3(sK1)) ),
introduced(definition,[new_symbols(definition,[spl41_8])],[avatar_definition]) ).
fof(f1446,plain,
( ~ v2_lattice3(k7_lattice3(sK1))
| spl41_8 ),
inference(avatar_component_clause,[],[f1445]) ).
fof(f1448,definition,
( spl41_9
<=> v1_lattice3(k7_lattice3(sK1)) ),
introduced(definition,[new_symbols(definition,[spl41_9])],[avatar_definition]) ).
fof(f1449,plain,
( ~ v1_lattice3(k7_lattice3(sK1))
| spl41_9 ),
inference(avatar_component_clause,[],[f1448]) ).
fof(f1451,definition,
( spl41_10
<=> v4_orders_2(k7_lattice3(sK1)) ),
introduced(definition,[new_symbols(definition,[spl41_10])],[avatar_definition]) ).
fof(f1452,plain,
( ~ v4_orders_2(k7_lattice3(sK1))
| spl41_10 ),
inference(avatar_component_clause,[],[f1451]) ).
fof(f1454,definition,
( spl41_11
<=> v3_orders_2(k7_lattice3(sK1)) ),
introduced(definition,[new_symbols(definition,[spl41_11])],[avatar_definition]) ).
fof(f1455,plain,
( ~ v3_orders_2(k7_lattice3(sK1))
| spl41_11 ),
inference(avatar_component_clause,[],[f1454]) ).
fof(f1457,definition,
( spl41_12
<=> v2_orders_2(k7_lattice3(sK1)) ),
introduced(definition,[new_symbols(definition,[spl41_12])],[avatar_definition]) ).
fof(f1458,plain,
( ~ v2_orders_2(k7_lattice3(sK1))
| spl41_12 ),
inference(avatar_component_clause,[],[f1457]) ).
fof(f1460,definition,
( spl41_13
<=> v3_lattice3(k7_lattice3(sK1)) ),
introduced(definition,[new_symbols(definition,[spl41_13])],[avatar_definition]) ).
fof(f1461,plain,
( ~ v3_lattice3(k7_lattice3(sK1))
| spl41_13 ),
inference(avatar_component_clause,[],[f1460]) ).
fof(f1463,definition,
( spl41_14
<=> v3_lattice3(k7_lattice3(sK0)) ),
introduced(definition,[new_symbols(definition,[spl41_14])],[avatar_definition]) ).
fof(f1464,plain,
( ~ v3_lattice3(k7_lattice3(sK0))
| spl41_14 ),
inference(avatar_component_clause,[],[f1463]) ).
fof(f1481,definition,
( spl41_17
<=> v3_struct_0(sK1) ),
introduced(definition,[new_symbols(definition,[spl41_17])],[avatar_definition]) ).
fof(f1482,plain,
( v3_struct_0(sK1)
| ~ spl41_17 ),
inference(avatar_component_clause,[],[f1481]) ).
fof(f1484,definition,
( spl41_18
<=> v3_struct_0(sK0) ),
introduced(definition,[new_symbols(definition,[spl41_18])],[avatar_definition]) ).
fof(f1485,plain,
( v3_struct_0(sK0)
| ~ spl41_18 ),
inference(avatar_component_clause,[],[f1484]) ).
fof(f1506,plain,
( ~ l1_orders_2(sK0)
| spl41_1 ),
inference(resolution,[],[f1425,f840]) ).
fof(f1508,plain,
( $false
| spl41_1 ),
inference(forward_subsumption_resolution,[],[f1506,f503]) ).
fof(f1509,plain,
spl41_1,
inference(avatar_contradiction_clause,[],[f1508]) ).
fof(f1511,plain,
( ~ v1_lattice3(sK0)
| ~ l1_orders_2(sK0)
| spl41_2 ),
inference(resolution,[],[f1428,f1005]) ).
fof(f1513,plain,
( ~ l1_orders_2(sK0)
| spl41_2 ),
inference(forward_subsumption_resolution,[],[f1511,f506]) ).
fof(f1514,plain,
( $false
| spl41_2 ),
inference(forward_subsumption_resolution,[],[f1513,f503]) ).
fof(f1515,plain,
spl41_2,
inference(avatar_contradiction_clause,[],[f1514]) ).
fof(f1517,plain,
( ~ v2_lattice3(sK0)
| ~ l1_orders_2(sK0)
| spl41_3 ),
inference(resolution,[],[f1431,f992]) ).
fof(f1519,plain,
( ~ l1_orders_2(sK0)
| spl41_3 ),
inference(forward_subsumption_resolution,[],[f1517,f505]) ).
fof(f1520,plain,
( $false
| spl41_3 ),
inference(forward_subsumption_resolution,[],[f1519,f503]) ).
fof(f1521,plain,
spl41_3,
inference(avatar_contradiction_clause,[],[f1520]) ).
fof(f1523,plain,
( ~ v4_orders_2(sK0)
| ~ l1_orders_2(sK0)
| spl41_4 ),
inference(resolution,[],[f1434,f968]) ).
fof(f1525,plain,
( ~ l1_orders_2(sK0)
| spl41_4 ),
inference(forward_subsumption_resolution,[],[f1523,f507]) ).
fof(f1526,plain,
( $false
| spl41_4 ),
inference(forward_subsumption_resolution,[],[f1525,f503]) ).
fof(f1527,plain,
spl41_4,
inference(avatar_contradiction_clause,[],[f1526]) ).
fof(f1529,plain,
( ~ v3_orders_2(sK0)
| ~ l1_orders_2(sK0)
| spl41_5 ),
inference(resolution,[],[f1437,f952]) ).
fof(f1531,plain,
( ~ l1_orders_2(sK0)
| spl41_5 ),
inference(forward_subsumption_resolution,[],[f1529,f508]) ).
fof(f1532,plain,
( $false
| spl41_5 ),
inference(forward_subsumption_resolution,[],[f1531,f503]) ).
fof(f1533,plain,
spl41_5,
inference(avatar_contradiction_clause,[],[f1532]) ).
fof(f1535,plain,
( ~ v2_orders_2(sK0)
| ~ l1_orders_2(sK0)
| spl41_6 ),
inference(resolution,[],[f1440,f930]) ).
fof(f1537,plain,
( ~ l1_orders_2(sK0)
| spl41_6 ),
inference(forward_subsumption_resolution,[],[f1535,f509]) ).
fof(f1538,plain,
( $false
| spl41_6 ),
inference(forward_subsumption_resolution,[],[f1537,f503]) ).
fof(f1539,plain,
spl41_6,
inference(avatar_contradiction_clause,[],[f1538]) ).
fof(f1541,plain,
( ~ l1_orders_2(sK1)
| spl41_7 ),
inference(resolution,[],[f1443,f840]) ).
fof(f1543,plain,
( $false
| spl41_7 ),
inference(forward_subsumption_resolution,[],[f1541,f510]) ).
fof(f1544,plain,
spl41_7,
inference(avatar_contradiction_clause,[],[f1543]) ).
fof(f1546,plain,
( ~ v1_lattice3(sK1)
| ~ l1_orders_2(sK1)
| spl41_8 ),
inference(resolution,[],[f1446,f1005]) ).
fof(f1548,plain,
( ~ l1_orders_2(sK1)
| spl41_8 ),
inference(forward_subsumption_resolution,[],[f1546,f513]) ).
fof(f1549,plain,
( $false
| spl41_8 ),
inference(forward_subsumption_resolution,[],[f1548,f510]) ).
fof(f1550,plain,
spl41_8,
inference(avatar_contradiction_clause,[],[f1549]) ).
fof(f1552,plain,
( ~ v2_lattice3(sK1)
| ~ l1_orders_2(sK1)
| spl41_9 ),
inference(resolution,[],[f1449,f992]) ).
fof(f1554,plain,
( ~ l1_orders_2(sK1)
| spl41_9 ),
inference(forward_subsumption_resolution,[],[f1552,f512]) ).
fof(f1555,plain,
( $false
| spl41_9 ),
inference(forward_subsumption_resolution,[],[f1554,f510]) ).
fof(f1556,plain,
spl41_9,
inference(avatar_contradiction_clause,[],[f1555]) ).
fof(f1558,plain,
( ~ v4_orders_2(sK1)
| ~ l1_orders_2(sK1)
| spl41_10 ),
inference(resolution,[],[f1452,f968]) ).
fof(f1560,plain,
( ~ l1_orders_2(sK1)
| spl41_10 ),
inference(forward_subsumption_resolution,[],[f1558,f514]) ).
fof(f1561,plain,
( $false
| spl41_10 ),
inference(forward_subsumption_resolution,[],[f1560,f510]) ).
fof(f1562,plain,
spl41_10,
inference(avatar_contradiction_clause,[],[f1561]) ).
fof(f1564,plain,
( ~ v3_orders_2(sK1)
| ~ l1_orders_2(sK1)
| spl41_11 ),
inference(resolution,[],[f1455,f952]) ).
fof(f1566,plain,
( ~ l1_orders_2(sK1)
| spl41_11 ),
inference(forward_subsumption_resolution,[],[f1564,f515]) ).
fof(f1567,plain,
( $false
| spl41_11 ),
inference(forward_subsumption_resolution,[],[f1566,f510]) ).
fof(f1568,plain,
spl41_11,
inference(avatar_contradiction_clause,[],[f1567]) ).
fof(f1570,plain,
( ~ v2_orders_2(sK1)
| ~ l1_orders_2(sK1)
| spl41_12 ),
inference(resolution,[],[f1458,f930]) ).
fof(f1572,plain,
( ~ l1_orders_2(sK1)
| spl41_12 ),
inference(forward_subsumption_resolution,[],[f1570,f516]) ).
fof(f1573,plain,
( $false
| spl41_12 ),
inference(forward_subsumption_resolution,[],[f1572,f510]) ).
fof(f1574,plain,
spl41_12,
inference(avatar_contradiction_clause,[],[f1573]) ).
fof(f1614,plain,
! [X0,X1] :
( ~ m1_relset_1(sK2,u1_struct_0(X0),u1_struct_0(X1))
| ~ 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)
| m2_relset_1(k1_waybel34(X0,X1,sK2),u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(sK2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v2_orders_2(X0) ),
inference(resolution,[],[f828,f520]) ).
fof(f1616,plain,
( ~ v3_orders_2(sK0)
| ~ v4_orders_2(sK0)
| ~ v1_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ l1_orders_2(sK0)
| ~ v2_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ l1_orders_2(sK1)
| m2_relset_1(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v2_orders_2(sK0) ),
inference(resolution,[],[f1614,f1369]) ).
fof(f1617,plain,
( ~ v4_orders_2(sK0)
| ~ v1_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ l1_orders_2(sK0)
| ~ v2_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ l1_orders_2(sK1)
| m2_relset_1(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v2_orders_2(sK0) ),
inference(forward_subsumption_resolution,[],[f1616,f508]) ).
fof(f1618,plain,
( ~ v1_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ l1_orders_2(sK0)
| ~ v2_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ l1_orders_2(sK1)
| m2_relset_1(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v2_orders_2(sK0) ),
inference(forward_subsumption_resolution,[],[f1617,f507]) ).
fof(f1619,plain,
( ~ v2_lattice3(sK0)
| ~ l1_orders_2(sK0)
| ~ v2_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ l1_orders_2(sK1)
| m2_relset_1(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v2_orders_2(sK0) ),
inference(forward_subsumption_resolution,[],[f1618,f506]) ).
fof(f1620,plain,
( ~ l1_orders_2(sK0)
| ~ v2_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ l1_orders_2(sK1)
| m2_relset_1(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v2_orders_2(sK0) ),
inference(forward_subsumption_resolution,[],[f1619,f505]) ).
fof(f1621,plain,
( ~ v2_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ l1_orders_2(sK1)
| m2_relset_1(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v2_orders_2(sK0) ),
inference(forward_subsumption_resolution,[],[f1620,f503]) ).
fof(f1622,plain,
( ~ v3_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ l1_orders_2(sK1)
| m2_relset_1(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v2_orders_2(sK0) ),
inference(forward_subsumption_resolution,[],[f1621,f516]) ).
fof(f1623,plain,
( ~ v4_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ l1_orders_2(sK1)
| m2_relset_1(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v2_orders_2(sK0) ),
inference(forward_subsumption_resolution,[],[f1622,f515]) ).
fof(f1624,plain,
( ~ v1_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ l1_orders_2(sK1)
| m2_relset_1(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v2_orders_2(sK0) ),
inference(forward_subsumption_resolution,[],[f1623,f514]) ).
fof(f1625,plain,
( ~ v2_lattice3(sK1)
| ~ l1_orders_2(sK1)
| m2_relset_1(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v2_orders_2(sK0) ),
inference(forward_subsumption_resolution,[],[f1624,f513]) ).
fof(f1626,plain,
( ~ l1_orders_2(sK1)
| m2_relset_1(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v2_orders_2(sK0) ),
inference(forward_subsumption_resolution,[],[f1625,f512]) ).
fof(f1627,plain,
( m2_relset_1(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v2_orders_2(sK0) ),
inference(forward_subsumption_resolution,[],[f1626,f510]) ).
fof(f1628,plain,
( m2_relset_1(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v2_orders_2(sK0) ),
inference(forward_subsumption_resolution,[],[f1627,f519]) ).
fof(f1629,plain,
m2_relset_1(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0)),
inference(forward_subsumption_resolution,[],[f1628,f509]) ).
fof(f1630,plain,
( ~ v1_funct_1(k1_waybel34(sK0,sK1,sK2))
| ~ v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| v3_waybel_1(k1_waybel_1(sK0,sK1,sK2,k1_waybel34(sK0,sK1,sK2)),sK0,sK1)
| ~ v3_lattice3(sK0)
| ~ v3_lattice3(sK1)
| ~ v17_waybel_0(sK2,sK0,sK1)
| ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ m2_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v2_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ l1_orders_2(sK1)
| ~ v2_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v4_orders_2(sK0)
| ~ v1_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ l1_orders_2(sK0) ),
inference(resolution,[],[f1629,f1320]) ).
fof(f1632,plain,
m1_relset_1(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0)),
inference(resolution,[],[f1629,f1305]) ).
fof(f1634,plain,
( ~ v1_funct_1(k1_waybel34(sK0,sK1,sK2))
| ~ v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| v3_waybel_1(k1_waybel_1(sK0,sK1,sK2,k1_waybel34(sK0,sK1,sK2)),sK0,sK1)
| ~ v3_lattice3(sK1)
| ~ v17_waybel_0(sK2,sK0,sK1)
| ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ m2_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v2_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ l1_orders_2(sK1)
| ~ v2_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v4_orders_2(sK0)
| ~ v1_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ l1_orders_2(sK0) ),
inference(forward_subsumption_resolution,[],[f1630,f504]) ).
fof(f1636,plain,
( ~ v1_funct_1(k1_waybel34(sK0,sK1,sK2))
| ~ v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| v3_waybel_1(k1_waybel_1(sK0,sK1,sK2,k1_waybel34(sK0,sK1,sK2)),sK0,sK1)
| ~ v17_waybel_0(sK2,sK0,sK1)
| ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ m2_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v2_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ l1_orders_2(sK1)
| ~ v2_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v4_orders_2(sK0)
| ~ v1_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ l1_orders_2(sK0) ),
inference(forward_subsumption_resolution,[],[f1634,f511]) ).
fof(f1638,plain,
( ~ v1_funct_1(k1_waybel34(sK0,sK1,sK2))
| ~ v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| v3_waybel_1(k1_waybel_1(sK0,sK1,sK2,k1_waybel34(sK0,sK1,sK2)),sK0,sK1)
| ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ m2_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v2_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ l1_orders_2(sK1)
| ~ v2_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v4_orders_2(sK0)
| ~ v1_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ l1_orders_2(sK0) ),
inference(forward_subsumption_resolution,[],[f1636,f518]) ).
fof(f1640,plain,
( ~ v1_funct_1(k1_waybel34(sK0,sK1,sK2))
| ~ v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| v3_waybel_1(k1_waybel_1(sK0,sK1,sK2,k1_waybel34(sK0,sK1,sK2)),sK0,sK1)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ m2_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v2_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ l1_orders_2(sK1)
| ~ v2_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v4_orders_2(sK0)
| ~ v1_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ l1_orders_2(sK0) ),
inference(forward_subsumption_resolution,[],[f1638,f520]) ).
fof(f1642,plain,
( ~ v1_funct_1(k1_waybel34(sK0,sK1,sK2))
| ~ v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| v3_waybel_1(k1_waybel_1(sK0,sK1,sK2,k1_waybel34(sK0,sK1,sK2)),sK0,sK1)
| ~ m2_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v2_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ l1_orders_2(sK1)
| ~ v2_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v4_orders_2(sK0)
| ~ v1_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ l1_orders_2(sK0) ),
inference(forward_subsumption_resolution,[],[f1640,f519]) ).
fof(f1644,plain,
( ~ v1_funct_1(k1_waybel34(sK0,sK1,sK2))
| ~ v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| v3_waybel_1(k1_waybel_1(sK0,sK1,sK2,k1_waybel34(sK0,sK1,sK2)),sK0,sK1)
| ~ v2_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ l1_orders_2(sK1)
| ~ v2_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v4_orders_2(sK0)
| ~ v1_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ l1_orders_2(sK0) ),
inference(forward_subsumption_resolution,[],[f1642,f517]) ).
fof(f1646,plain,
( ~ v1_funct_1(k1_waybel34(sK0,sK1,sK2))
| ~ v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| v3_waybel_1(k1_waybel_1(sK0,sK1,sK2,k1_waybel34(sK0,sK1,sK2)),sK0,sK1)
| ~ v3_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ l1_orders_2(sK1)
| ~ v2_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v4_orders_2(sK0)
| ~ v1_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ l1_orders_2(sK0) ),
inference(forward_subsumption_resolution,[],[f1644,f516]) ).
fof(f1648,plain,
( ~ v1_funct_1(k1_waybel34(sK0,sK1,sK2))
| ~ v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| v3_waybel_1(k1_waybel_1(sK0,sK1,sK2,k1_waybel34(sK0,sK1,sK2)),sK0,sK1)
| ~ v4_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ l1_orders_2(sK1)
| ~ v2_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v4_orders_2(sK0)
| ~ v1_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ l1_orders_2(sK0) ),
inference(forward_subsumption_resolution,[],[f1646,f515]) ).
fof(f1650,plain,
( ~ v1_funct_1(k1_waybel34(sK0,sK1,sK2))
| ~ v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| v3_waybel_1(k1_waybel_1(sK0,sK1,sK2,k1_waybel34(sK0,sK1,sK2)),sK0,sK1)
| ~ v1_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ l1_orders_2(sK1)
| ~ v2_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v4_orders_2(sK0)
| ~ v1_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ l1_orders_2(sK0) ),
inference(forward_subsumption_resolution,[],[f1648,f514]) ).
fof(f1652,plain,
( ~ v1_funct_1(k1_waybel34(sK0,sK1,sK2))
| ~ v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| v3_waybel_1(k1_waybel_1(sK0,sK1,sK2,k1_waybel34(sK0,sK1,sK2)),sK0,sK1)
| ~ v2_lattice3(sK1)
| ~ l1_orders_2(sK1)
| ~ v2_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v4_orders_2(sK0)
| ~ v1_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ l1_orders_2(sK0) ),
inference(forward_subsumption_resolution,[],[f1650,f513]) ).
fof(f1654,plain,
( ~ v1_funct_1(k1_waybel34(sK0,sK1,sK2))
| ~ v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| v3_waybel_1(k1_waybel_1(sK0,sK1,sK2,k1_waybel34(sK0,sK1,sK2)),sK0,sK1)
| ~ l1_orders_2(sK1)
| ~ v2_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v4_orders_2(sK0)
| ~ v1_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ l1_orders_2(sK0) ),
inference(forward_subsumption_resolution,[],[f1652,f512]) ).
fof(f1656,plain,
( ~ v1_funct_1(k1_waybel34(sK0,sK1,sK2))
| ~ v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| v3_waybel_1(k1_waybel_1(sK0,sK1,sK2,k1_waybel34(sK0,sK1,sK2)),sK0,sK1)
| ~ v2_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v4_orders_2(sK0)
| ~ v1_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ l1_orders_2(sK0) ),
inference(forward_subsumption_resolution,[],[f1654,f510]) ).
fof(f1658,plain,
( ~ v1_funct_1(k1_waybel34(sK0,sK1,sK2))
| ~ v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| v3_waybel_1(k1_waybel_1(sK0,sK1,sK2,k1_waybel34(sK0,sK1,sK2)),sK0,sK1)
| ~ v3_orders_2(sK0)
| ~ v4_orders_2(sK0)
| ~ v1_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ l1_orders_2(sK0) ),
inference(forward_subsumption_resolution,[],[f1656,f509]) ).
fof(f1660,plain,
( ~ v1_funct_1(k1_waybel34(sK0,sK1,sK2))
| ~ v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| v3_waybel_1(k1_waybel_1(sK0,sK1,sK2,k1_waybel34(sK0,sK1,sK2)),sK0,sK1)
| ~ v4_orders_2(sK0)
| ~ v1_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ l1_orders_2(sK0) ),
inference(forward_subsumption_resolution,[],[f1658,f508]) ).
fof(f1662,definition,
( spl41_24
<=> v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0)) ),
introduced(definition,[new_symbols(definition,[spl41_24])],[avatar_definition]) ).
fof(f1663,plain,
( ~ v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| spl41_24 ),
inference(avatar_component_clause,[],[f1662]) ).
fof(f1665,definition,
( spl41_25
<=> v1_funct_1(k1_waybel34(sK0,sK1,sK2)) ),
introduced(definition,[new_symbols(definition,[spl41_25])],[avatar_definition]) ).
fof(f1666,plain,
( ~ v1_funct_1(k1_waybel34(sK0,sK1,sK2))
| spl41_25 ),
inference(avatar_component_clause,[],[f1665]) ).
fof(f1671,plain,
( ~ v1_funct_1(k1_waybel34(sK0,sK1,sK2))
| ~ v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| v3_waybel_1(k1_waybel_1(sK0,sK1,sK2,k1_waybel34(sK0,sK1,sK2)),sK0,sK1)
| ~ v1_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ l1_orders_2(sK0) ),
inference(forward_subsumption_resolution,[],[f1660,f507]) ).
fof(f1672,plain,
( ~ v1_funct_1(k1_waybel34(sK0,sK1,sK2))
| ~ v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| v3_waybel_1(k1_waybel_1(sK0,sK1,sK2,k1_waybel34(sK0,sK1,sK2)),sK0,sK1)
| ~ v2_lattice3(sK0)
| ~ l1_orders_2(sK0) ),
inference(forward_subsumption_resolution,[],[f1671,f506]) ).
fof(f1673,plain,
( ~ v1_funct_1(k1_waybel34(sK0,sK1,sK2))
| ~ v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| v3_waybel_1(k1_waybel_1(sK0,sK1,sK2,k1_waybel34(sK0,sK1,sK2)),sK0,sK1)
| ~ l1_orders_2(sK0) ),
inference(forward_subsumption_resolution,[],[f1672,f505]) ).
fof(f1674,plain,
( ~ v1_funct_1(k1_waybel34(sK0,sK1,sK2))
| ~ v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| v3_waybel_1(k1_waybel_1(sK0,sK1,sK2,k1_waybel34(sK0,sK1,sK2)),sK0,sK1) ),
inference(forward_subsumption_resolution,[],[f1673,f503]) ).
fof(f1676,definition,
( spl41_27
<=> v3_waybel_1(k1_waybel_1(sK0,sK1,sK2,k1_waybel34(sK0,sK1,sK2)),sK0,sK1) ),
introduced(definition,[new_symbols(definition,[spl41_27])],[avatar_definition]) ).
fof(f1677,plain,
( v3_waybel_1(k1_waybel_1(sK0,sK1,sK2,k1_waybel34(sK0,sK1,sK2)),sK0,sK1)
| ~ spl41_27 ),
inference(avatar_component_clause,[],[f1676]) ).
fof(f1678,plain,
( spl41_27
| ~ spl41_24
| ~ spl41_25 ),
inference(avatar_split_clause,[],[f1674,f1665,f1662,f1676]) ).
fof(f1680,plain,
( ~ v2_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v4_orders_2(sK0)
| ~ v1_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v3_lattice3(sK0)
| ~ l1_orders_2(sK0)
| ~ v2_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ v3_lattice3(sK1)
| ~ l1_orders_2(sK1)
| ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v17_waybel_0(sK2,sK0,sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| spl41_24 ),
inference(resolution,[],[f1663,f923]) ).
fof(f1682,plain,
( ~ v3_orders_2(sK0)
| ~ v4_orders_2(sK0)
| ~ v1_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v3_lattice3(sK0)
| ~ l1_orders_2(sK0)
| ~ v2_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ v3_lattice3(sK1)
| ~ l1_orders_2(sK1)
| ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v17_waybel_0(sK2,sK0,sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| spl41_24 ),
inference(forward_subsumption_resolution,[],[f1680,f509]) ).
fof(f1683,plain,
( ~ v4_orders_2(sK0)
| ~ v1_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v3_lattice3(sK0)
| ~ l1_orders_2(sK0)
| ~ v2_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ v3_lattice3(sK1)
| ~ l1_orders_2(sK1)
| ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v17_waybel_0(sK2,sK0,sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| spl41_24 ),
inference(forward_subsumption_resolution,[],[f1682,f508]) ).
fof(f1684,plain,
( ~ v1_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v3_lattice3(sK0)
| ~ l1_orders_2(sK0)
| ~ v2_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ v3_lattice3(sK1)
| ~ l1_orders_2(sK1)
| ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v17_waybel_0(sK2,sK0,sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| spl41_24 ),
inference(forward_subsumption_resolution,[],[f1683,f507]) ).
fof(f1685,plain,
( ~ v2_lattice3(sK0)
| ~ v3_lattice3(sK0)
| ~ l1_orders_2(sK0)
| ~ v2_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ v3_lattice3(sK1)
| ~ l1_orders_2(sK1)
| ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v17_waybel_0(sK2,sK0,sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| spl41_24 ),
inference(forward_subsumption_resolution,[],[f1684,f506]) ).
fof(f1686,plain,
( ~ v3_lattice3(sK0)
| ~ l1_orders_2(sK0)
| ~ v2_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ v3_lattice3(sK1)
| ~ l1_orders_2(sK1)
| ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v17_waybel_0(sK2,sK0,sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| spl41_24 ),
inference(forward_subsumption_resolution,[],[f1685,f505]) ).
fof(f1687,plain,
( ~ l1_orders_2(sK0)
| ~ v2_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ v3_lattice3(sK1)
| ~ l1_orders_2(sK1)
| ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v17_waybel_0(sK2,sK0,sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| spl41_24 ),
inference(forward_subsumption_resolution,[],[f1686,f504]) ).
fof(f1688,plain,
( ~ v2_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ v3_lattice3(sK1)
| ~ l1_orders_2(sK1)
| ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v17_waybel_0(sK2,sK0,sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| spl41_24 ),
inference(forward_subsumption_resolution,[],[f1687,f503]) ).
fof(f1689,plain,
( ~ v3_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ v3_lattice3(sK1)
| ~ l1_orders_2(sK1)
| ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v17_waybel_0(sK2,sK0,sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| spl41_24 ),
inference(forward_subsumption_resolution,[],[f1688,f516]) ).
fof(f1690,plain,
( ~ v4_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ v3_lattice3(sK1)
| ~ l1_orders_2(sK1)
| ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v17_waybel_0(sK2,sK0,sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| spl41_24 ),
inference(forward_subsumption_resolution,[],[f1689,f515]) ).
fof(f1691,plain,
( ~ v1_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ v3_lattice3(sK1)
| ~ l1_orders_2(sK1)
| ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v17_waybel_0(sK2,sK0,sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| spl41_24 ),
inference(forward_subsumption_resolution,[],[f1690,f514]) ).
fof(f1692,plain,
( ~ v2_lattice3(sK1)
| ~ v3_lattice3(sK1)
| ~ l1_orders_2(sK1)
| ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v17_waybel_0(sK2,sK0,sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| spl41_24 ),
inference(forward_subsumption_resolution,[],[f1691,f513]) ).
fof(f1693,plain,
( ~ v3_lattice3(sK1)
| ~ l1_orders_2(sK1)
| ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v17_waybel_0(sK2,sK0,sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| spl41_24 ),
inference(forward_subsumption_resolution,[],[f1692,f512]) ).
fof(f1694,plain,
( ~ l1_orders_2(sK1)
| ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v17_waybel_0(sK2,sK0,sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| spl41_24 ),
inference(forward_subsumption_resolution,[],[f1693,f511]) ).
fof(f1695,plain,
( ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v17_waybel_0(sK2,sK0,sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| spl41_24 ),
inference(forward_subsumption_resolution,[],[f1694,f510]) ).
fof(f1696,plain,
( ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v17_waybel_0(sK2,sK0,sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| spl41_24 ),
inference(forward_subsumption_resolution,[],[f1695,f520]) ).
fof(f1697,plain,
( ~ v17_waybel_0(sK2,sK0,sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| spl41_24 ),
inference(forward_subsumption_resolution,[],[f1696,f519]) ).
fof(f1698,plain,
( ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| spl41_24 ),
inference(forward_subsumption_resolution,[],[f1697,f518]) ).
fof(f1699,plain,
( $false
| spl41_24 ),
inference(forward_subsumption_resolution,[],[f1698,f1369]) ).
fof(f1700,plain,
spl41_24,
inference(avatar_contradiction_clause,[],[f1699]) ).
fof(f1701,plain,
( $false
| spl41_25 ),
inference(unit_resulting_resolution,[],[f925,f508,f507,f509,f520,f510,f511,f512,f513,f514,f515,f516,f503,f504,f505,f506,f518,f1369,f519,f1666]) ).
fof(f1702,plain,
spl41_25,
inference(avatar_contradiction_clause,[],[f1701]) ).
fof(f1712,plain,
( ~ l1_orders_2(sK1)
| ~ l1_orders_2(sK0)
| ~ v1_funct_1(k1_waybel34(sK0,sK1,sK2))
| ~ v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| m2_relset_1(k3_waybel34(sK1,sK0,k1_waybel34(sK0,sK1,sK2)),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0))) ),
inference(resolution,[],[f1632,f835]) ).
fof(f1713,plain,
( ~ l1_orders_2(sK1)
| ~ l1_orders_2(sK0)
| ~ v1_funct_1(k1_waybel34(sK0,sK1,sK2))
| ~ v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| v1_funct_1(k3_waybel34(sK1,sK0,k1_waybel34(sK0,sK1,sK2))) ),
inference(resolution,[],[f1632,f837]) ).
fof(f1718,plain,
( ~ l1_orders_2(sK0)
| ~ v1_funct_1(k1_waybel34(sK0,sK1,sK2))
| ~ v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| v1_funct_1(k3_waybel34(sK1,sK0,k1_waybel34(sK0,sK1,sK2))) ),
inference(forward_subsumption_resolution,[],[f1713,f510]) ).
fof(f1719,plain,
( ~ l1_orders_2(sK0)
| ~ v1_funct_1(k1_waybel34(sK0,sK1,sK2))
| ~ v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| m2_relset_1(k3_waybel34(sK1,sK0,k1_waybel34(sK0,sK1,sK2)),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0))) ),
inference(forward_subsumption_resolution,[],[f1712,f510]) ).
fof(f1722,plain,
( ~ v1_funct_1(k1_waybel34(sK0,sK1,sK2))
| ~ v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| v1_funct_1(k3_waybel34(sK1,sK0,k1_waybel34(sK0,sK1,sK2))) ),
inference(forward_subsumption_resolution,[],[f1718,f503]) ).
fof(f1723,plain,
( ~ v1_funct_1(k1_waybel34(sK0,sK1,sK2))
| ~ v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| m2_relset_1(k3_waybel34(sK1,sK0,k1_waybel34(sK0,sK1,sK2)),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0))) ),
inference(forward_subsumption_resolution,[],[f1719,f503]) ).
fof(f1727,definition,
( spl41_29
<=> v1_funct_1(k3_waybel34(sK1,sK0,k1_waybel34(sK0,sK1,sK2))) ),
introduced(definition,[new_symbols(definition,[spl41_29])],[avatar_definition]) ).
fof(f1728,plain,
( v1_funct_1(k3_waybel34(sK1,sK0,k1_waybel34(sK0,sK1,sK2)))
| ~ spl41_29 ),
inference(avatar_component_clause,[],[f1727]) ).
fof(f1729,plain,
( spl41_29
| ~ spl41_24
| ~ spl41_25 ),
inference(avatar_split_clause,[],[f1722,f1665,f1662,f1727]) ).
fof(f1731,definition,
( spl41_30
<=> m2_relset_1(k3_waybel34(sK1,sK0,k1_waybel34(sK0,sK1,sK2)),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0))) ),
introduced(definition,[new_symbols(definition,[spl41_30])],[avatar_definition]) ).
fof(f1732,plain,
( m2_relset_1(k3_waybel34(sK1,sK0,k1_waybel34(sK0,sK1,sK2)),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ spl41_30 ),
inference(avatar_component_clause,[],[f1731]) ).
fof(f1733,plain,
( spl41_30
| ~ spl41_24
| ~ spl41_25 ),
inference(avatar_split_clause,[],[f1723,f1665,f1662,f1731]) ).
fof(f1777,plain,
! [X0,X1] :
( ~ m1_relset_1(sK2,u1_struct_0(X0),u1_struct_0(X1))
| ~ 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(k1_waybel34(X0,X1,sK2))
| ~ v1_funct_2(sK2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v2_orders_2(X0) ),
inference(resolution,[],[f830,f520]) ).
fof(f1780,plain,
( ~ v3_orders_2(sK0)
| ~ v4_orders_2(sK0)
| ~ v1_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ l1_orders_2(sK0)
| ~ v2_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ l1_orders_2(sK1)
| v1_funct_1(k1_waybel34(sK0,sK1,sK2))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v2_orders_2(sK0) ),
inference(resolution,[],[f1777,f1369]) ).
fof(f1781,plain,
( ~ v4_orders_2(sK0)
| ~ v1_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ l1_orders_2(sK0)
| ~ v2_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ l1_orders_2(sK1)
| v1_funct_1(k1_waybel34(sK0,sK1,sK2))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v2_orders_2(sK0) ),
inference(forward_subsumption_resolution,[],[f1780,f508]) ).
fof(f1782,plain,
( ~ v1_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ l1_orders_2(sK0)
| ~ v2_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ l1_orders_2(sK1)
| v1_funct_1(k1_waybel34(sK0,sK1,sK2))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v2_orders_2(sK0) ),
inference(forward_subsumption_resolution,[],[f1781,f507]) ).
fof(f1783,plain,
( ~ v2_lattice3(sK0)
| ~ l1_orders_2(sK0)
| ~ v2_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ l1_orders_2(sK1)
| v1_funct_1(k1_waybel34(sK0,sK1,sK2))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v2_orders_2(sK0) ),
inference(forward_subsumption_resolution,[],[f1782,f506]) ).
fof(f1784,plain,
( ~ l1_orders_2(sK0)
| ~ v2_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ l1_orders_2(sK1)
| v1_funct_1(k1_waybel34(sK0,sK1,sK2))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v2_orders_2(sK0) ),
inference(forward_subsumption_resolution,[],[f1783,f505]) ).
fof(f1785,plain,
( ~ v2_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ l1_orders_2(sK1)
| v1_funct_1(k1_waybel34(sK0,sK1,sK2))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v2_orders_2(sK0) ),
inference(forward_subsumption_resolution,[],[f1784,f503]) ).
fof(f1786,plain,
( ~ v3_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ l1_orders_2(sK1)
| v1_funct_1(k1_waybel34(sK0,sK1,sK2))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v2_orders_2(sK0) ),
inference(forward_subsumption_resolution,[],[f1785,f516]) ).
fof(f1787,plain,
( ~ v4_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ l1_orders_2(sK1)
| v1_funct_1(k1_waybel34(sK0,sK1,sK2))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v2_orders_2(sK0) ),
inference(forward_subsumption_resolution,[],[f1786,f515]) ).
fof(f1788,plain,
( ~ v1_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ l1_orders_2(sK1)
| v1_funct_1(k1_waybel34(sK0,sK1,sK2))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v2_orders_2(sK0) ),
inference(forward_subsumption_resolution,[],[f1787,f514]) ).
fof(f1789,plain,
( ~ v2_lattice3(sK1)
| ~ l1_orders_2(sK1)
| v1_funct_1(k1_waybel34(sK0,sK1,sK2))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v2_orders_2(sK0) ),
inference(forward_subsumption_resolution,[],[f1788,f513]) ).
fof(f1790,plain,
( ~ l1_orders_2(sK1)
| v1_funct_1(k1_waybel34(sK0,sK1,sK2))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v2_orders_2(sK0) ),
inference(forward_subsumption_resolution,[],[f1789,f512]) ).
fof(f1791,plain,
( v1_funct_1(k1_waybel34(sK0,sK1,sK2))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v2_orders_2(sK0) ),
inference(forward_subsumption_resolution,[],[f1790,f510]) ).
fof(f1792,plain,
( v1_funct_1(k1_waybel34(sK0,sK1,sK2))
| ~ v2_orders_2(sK0) ),
inference(forward_subsumption_resolution,[],[f1791,f519]) ).
fof(f1793,plain,
v1_funct_1(k1_waybel34(sK0,sK1,sK2)),
inference(forward_subsumption_resolution,[],[f1792,f509]) ).
fof(f1796,plain,
! [X0,X1] :
( ~ m2_relset_1(k1_waybel34(sK0,sK1,sK2),u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(X0),u1_struct_0(X1))
| k1_waybel34(sK0,sK1,sK2) = k3_waybel34(X0,X1,k1_waybel34(sK0,sK1,sK2))
| ~ l1_orders_2(X1)
| ~ l1_orders_2(X0) ),
inference(resolution,[],[f1793,f823]) ).
fof(f2206,plain,
( ! [X0] :
( ~ v3_waybel_1(k1_waybel_1(k7_lattice3(sK1),k7_lattice3(sK0),k3_waybel34(sK1,sK0,k1_waybel34(sK0,sK1,sK2)),X0),k7_lattice3(sK1),k7_lattice3(sK0))
| ~ v1_funct_1(k3_waybel34(sK1,sK0,k1_waybel34(sK0,sK1,sK2)))
| ~ v1_funct_2(k3_waybel34(sK1,sK0,k1_waybel34(sK0,sK1,sK2)),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| k3_waybel34(sK1,sK0,k1_waybel34(sK0,sK1,sK2)) = k2_waybel34(k7_lattice3(sK1),k7_lattice3(sK0),X0)
| ~ v3_lattice3(k7_lattice3(sK1))
| ~ v3_lattice3(k7_lattice3(sK0))
| ~ v18_waybel_0(X0,k7_lattice3(sK0),k7_lattice3(sK1))
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ m2_relset_1(X0,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ v2_orders_2(k7_lattice3(sK0))
| ~ v3_orders_2(k7_lattice3(sK0))
| ~ v4_orders_2(k7_lattice3(sK0))
| ~ v1_lattice3(k7_lattice3(sK0))
| ~ v2_lattice3(k7_lattice3(sK0))
| ~ l1_orders_2(k7_lattice3(sK0))
| ~ v2_orders_2(k7_lattice3(sK1))
| ~ v3_orders_2(k7_lattice3(sK1))
| ~ v4_orders_2(k7_lattice3(sK1))
| ~ v1_lattice3(k7_lattice3(sK1))
| ~ v2_lattice3(k7_lattice3(sK1))
| ~ l1_orders_2(k7_lattice3(sK1)) )
| ~ spl41_30 ),
inference(resolution,[],[f1732,f822]) ).
fof(f2236,plain,
( ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| sK2 = k3_waybel34(sK0,sK1,sK2)
| ~ l1_orders_2(sK1)
| ~ l1_orders_2(sK0) ),
inference(resolution,[],[f1365,f517]) ).
fof(f2237,plain,
( sK2 = k3_waybel34(sK0,sK1,sK2)
| ~ l1_orders_2(sK1)
| ~ l1_orders_2(sK0) ),
inference(forward_subsumption_resolution,[],[f2236,f519]) ).
fof(f2238,plain,
( sK2 = k3_waybel34(sK0,sK1,sK2)
| ~ l1_orders_2(sK0) ),
inference(forward_subsumption_resolution,[],[f2237,f510]) ).
fof(f2239,plain,
sK2 = k3_waybel34(sK0,sK1,sK2),
inference(forward_subsumption_resolution,[],[f2238,f503]) ).
fof(f2240,plain,
k1_waybel34(sK0,sK1,sK2) != k2_waybel34(k7_lattice3(sK1),k7_lattice3(sK0),sK2),
inference(superposition,[],[f521,f2239]) ).
fof(f2242,plain,
m2_relset_1(sK2,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1))),
inference(superposition,[],[f1388,f2239]) ).
fof(f2246,plain,
( v1_funct_2(sK2,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ l1_orders_2(sK0)
| ~ l1_orders_2(sK1)
| ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(superposition,[],[f836,f2239]) ).
fof(f2249,plain,
( v18_waybel_0(sK2,k7_lattice3(sK0),k7_lattice3(sK1))
| ~ v2_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v4_orders_2(sK0)
| ~ v1_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v3_lattice3(sK0)
| ~ l1_orders_2(sK0)
| ~ v2_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ v3_lattice3(sK1)
| ~ l1_orders_2(sK1)
| ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v17_waybel_0(sK2,sK0,sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(superposition,[],[f962,f2239]) ).
fof(f2255,plain,
( v18_waybel_0(sK2,k7_lattice3(sK0),k7_lattice3(sK1))
| ~ v3_orders_2(sK0)
| ~ v4_orders_2(sK0)
| ~ v1_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v3_lattice3(sK0)
| ~ l1_orders_2(sK0)
| ~ v2_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ v3_lattice3(sK1)
| ~ l1_orders_2(sK1)
| ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v17_waybel_0(sK2,sK0,sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(forward_subsumption_resolution,[],[f2249,f509]) ).
fof(f2258,plain,
( v1_funct_2(sK2,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ l1_orders_2(sK1)
| ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(forward_subsumption_resolution,[],[f2246,f503]) ).
fof(f2263,plain,
( v18_waybel_0(sK2,k7_lattice3(sK0),k7_lattice3(sK1))
| ~ v4_orders_2(sK0)
| ~ v1_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v3_lattice3(sK0)
| ~ l1_orders_2(sK0)
| ~ v2_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ v3_lattice3(sK1)
| ~ l1_orders_2(sK1)
| ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v17_waybel_0(sK2,sK0,sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(forward_subsumption_resolution,[],[f2255,f508]) ).
fof(f2266,plain,
( v1_funct_2(sK2,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(forward_subsumption_resolution,[],[f2258,f510]) ).
fof(f2269,plain,
( v18_waybel_0(sK2,k7_lattice3(sK0),k7_lattice3(sK1))
| ~ v1_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v3_lattice3(sK0)
| ~ l1_orders_2(sK0)
| ~ v2_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ v3_lattice3(sK1)
| ~ l1_orders_2(sK1)
| ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v17_waybel_0(sK2,sK0,sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(forward_subsumption_resolution,[],[f2263,f507]) ).
fof(f2272,plain,
( v1_funct_2(sK2,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(forward_subsumption_resolution,[],[f2266,f520]) ).
fof(f2275,plain,
( v18_waybel_0(sK2,k7_lattice3(sK0),k7_lattice3(sK1))
| ~ v2_lattice3(sK0)
| ~ v3_lattice3(sK0)
| ~ l1_orders_2(sK0)
| ~ v2_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ v3_lattice3(sK1)
| ~ l1_orders_2(sK1)
| ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v17_waybel_0(sK2,sK0,sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(forward_subsumption_resolution,[],[f2269,f506]) ).
fof(f2278,plain,
( v1_funct_2(sK2,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(forward_subsumption_resolution,[],[f2272,f519]) ).
fof(f2281,plain,
( v18_waybel_0(sK2,k7_lattice3(sK0),k7_lattice3(sK1))
| ~ v3_lattice3(sK0)
| ~ l1_orders_2(sK0)
| ~ v2_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ v3_lattice3(sK1)
| ~ l1_orders_2(sK1)
| ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v17_waybel_0(sK2,sK0,sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(forward_subsumption_resolution,[],[f2275,f505]) ).
fof(f2284,plain,
v1_funct_2(sK2,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1))),
inference(forward_subsumption_resolution,[],[f2278,f1369]) ).
fof(f2287,plain,
( v18_waybel_0(sK2,k7_lattice3(sK0),k7_lattice3(sK1))
| ~ l1_orders_2(sK0)
| ~ v2_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ v3_lattice3(sK1)
| ~ l1_orders_2(sK1)
| ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v17_waybel_0(sK2,sK0,sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(forward_subsumption_resolution,[],[f2281,f504]) ).
fof(f2291,plain,
( v18_waybel_0(sK2,k7_lattice3(sK0),k7_lattice3(sK1))
| ~ v2_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ v3_lattice3(sK1)
| ~ l1_orders_2(sK1)
| ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v17_waybel_0(sK2,sK0,sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(forward_subsumption_resolution,[],[f2287,f503]) ).
fof(f2295,plain,
( v18_waybel_0(sK2,k7_lattice3(sK0),k7_lattice3(sK1))
| ~ v3_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ v3_lattice3(sK1)
| ~ l1_orders_2(sK1)
| ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v17_waybel_0(sK2,sK0,sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(forward_subsumption_resolution,[],[f2291,f516]) ).
fof(f2299,plain,
( v18_waybel_0(sK2,k7_lattice3(sK0),k7_lattice3(sK1))
| ~ v4_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ v3_lattice3(sK1)
| ~ l1_orders_2(sK1)
| ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v17_waybel_0(sK2,sK0,sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(forward_subsumption_resolution,[],[f2295,f515]) ).
fof(f2303,plain,
( v18_waybel_0(sK2,k7_lattice3(sK0),k7_lattice3(sK1))
| ~ v1_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ v3_lattice3(sK1)
| ~ l1_orders_2(sK1)
| ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v17_waybel_0(sK2,sK0,sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(forward_subsumption_resolution,[],[f2299,f514]) ).
fof(f2307,plain,
( v18_waybel_0(sK2,k7_lattice3(sK0),k7_lattice3(sK1))
| ~ v2_lattice3(sK1)
| ~ v3_lattice3(sK1)
| ~ l1_orders_2(sK1)
| ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v17_waybel_0(sK2,sK0,sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(forward_subsumption_resolution,[],[f2303,f513]) ).
fof(f2311,plain,
( v18_waybel_0(sK2,k7_lattice3(sK0),k7_lattice3(sK1))
| ~ v3_lattice3(sK1)
| ~ l1_orders_2(sK1)
| ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v17_waybel_0(sK2,sK0,sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(forward_subsumption_resolution,[],[f2307,f512]) ).
fof(f2315,plain,
( v18_waybel_0(sK2,k7_lattice3(sK0),k7_lattice3(sK1))
| ~ l1_orders_2(sK1)
| ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v17_waybel_0(sK2,sK0,sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(forward_subsumption_resolution,[],[f2311,f511]) ).
fof(f2319,plain,
( v18_waybel_0(sK2,k7_lattice3(sK0),k7_lattice3(sK1))
| ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v17_waybel_0(sK2,sK0,sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(forward_subsumption_resolution,[],[f2315,f510]) ).
fof(f2323,plain,
( v18_waybel_0(sK2,k7_lattice3(sK0),k7_lattice3(sK1))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v17_waybel_0(sK2,sK0,sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(forward_subsumption_resolution,[],[f2319,f520]) ).
fof(f2327,plain,
( v18_waybel_0(sK2,k7_lattice3(sK0),k7_lattice3(sK1))
| ~ v17_waybel_0(sK2,sK0,sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(forward_subsumption_resolution,[],[f2323,f519]) ).
fof(f2331,plain,
( v18_waybel_0(sK2,k7_lattice3(sK0),k7_lattice3(sK1))
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(forward_subsumption_resolution,[],[f2327,f518]) ).
fof(f2335,plain,
v18_waybel_0(sK2,k7_lattice3(sK0),k7_lattice3(sK1)),
inference(forward_subsumption_resolution,[],[f2331,f1369]) ).
fof(f2366,plain,
( v3_struct_0(sK1)
| ~ v3_lattice3(sK1)
| ~ l1_orders_2(sK1)
| spl41_13 ),
inference(resolution,[],[f1014,f1461]) ).
fof(f2508,plain,
( ~ v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| k1_waybel34(sK0,sK1,sK2) = k3_waybel34(sK1,sK0,k1_waybel34(sK0,sK1,sK2))
| ~ l1_orders_2(sK0)
| ~ l1_orders_2(sK1) ),
inference(resolution,[],[f1796,f1629]) ).
fof(f2509,plain,
( ~ v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| k1_waybel34(sK0,sK1,sK2) = k3_waybel34(sK1,sK0,k1_waybel34(sK0,sK1,sK2))
| ~ l1_orders_2(sK1) ),
inference(forward_subsumption_resolution,[],[f2508,f503]) ).
fof(f2510,plain,
( ~ v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| k1_waybel34(sK0,sK1,sK2) = k3_waybel34(sK1,sK0,k1_waybel34(sK0,sK1,sK2)) ),
inference(forward_subsumption_resolution,[],[f2509,f510]) ).
fof(f2512,definition,
( spl41_70
<=> k1_waybel34(sK0,sK1,sK2) = k3_waybel34(sK1,sK0,k1_waybel34(sK0,sK1,sK2)) ),
introduced(definition,[new_symbols(definition,[spl41_70])],[avatar_definition]) ).
fof(f2513,plain,
( k1_waybel34(sK0,sK1,sK2) = k3_waybel34(sK1,sK0,k1_waybel34(sK0,sK1,sK2))
| ~ spl41_70 ),
inference(avatar_component_clause,[],[f2512]) ).
fof(f2514,plain,
( spl41_70
| ~ spl41_24 ),
inference(avatar_split_clause,[],[f2510,f1662,f2512]) ).
fof(f2516,plain,
( m2_relset_1(k1_waybel34(sK0,sK1,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ spl41_30
| ~ spl41_70 ),
inference(superposition,[],[f1732,f2513]) ).
fof(f2525,plain,
( v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ v2_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ v3_lattice3(sK1)
| ~ l1_orders_2(sK1)
| ~ v2_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v4_orders_2(sK0)
| ~ v1_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v3_lattice3(sK0)
| ~ l1_orders_2(sK0)
| ~ v1_funct_1(k1_waybel34(sK0,sK1,sK2))
| ~ v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v18_waybel_0(k1_waybel34(sK0,sK1,sK2),sK1,sK0)
| ~ m1_relset_1(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ spl41_70 ),
inference(superposition,[],[f976,f2513]) ).
fof(f2526,plain,
( v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ v3_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ v3_lattice3(sK1)
| ~ l1_orders_2(sK1)
| ~ v2_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v4_orders_2(sK0)
| ~ v1_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v3_lattice3(sK0)
| ~ l1_orders_2(sK0)
| ~ v1_funct_1(k1_waybel34(sK0,sK1,sK2))
| ~ v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v18_waybel_0(k1_waybel34(sK0,sK1,sK2),sK1,sK0)
| ~ m1_relset_1(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ spl41_70 ),
inference(forward_subsumption_resolution,[],[f2525,f516]) ).
fof(f2532,plain,
( v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ v4_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ v3_lattice3(sK1)
| ~ l1_orders_2(sK1)
| ~ v2_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v4_orders_2(sK0)
| ~ v1_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v3_lattice3(sK0)
| ~ l1_orders_2(sK0)
| ~ v1_funct_1(k1_waybel34(sK0,sK1,sK2))
| ~ v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v18_waybel_0(k1_waybel34(sK0,sK1,sK2),sK1,sK0)
| ~ m1_relset_1(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ spl41_70 ),
inference(forward_subsumption_resolution,[],[f2526,f515]) ).
fof(f2535,plain,
( v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ v1_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ v3_lattice3(sK1)
| ~ l1_orders_2(sK1)
| ~ v2_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v4_orders_2(sK0)
| ~ v1_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v3_lattice3(sK0)
| ~ l1_orders_2(sK0)
| ~ v1_funct_1(k1_waybel34(sK0,sK1,sK2))
| ~ v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v18_waybel_0(k1_waybel34(sK0,sK1,sK2),sK1,sK0)
| ~ m1_relset_1(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ spl41_70 ),
inference(forward_subsumption_resolution,[],[f2532,f514]) ).
fof(f2538,plain,
( v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ v2_lattice3(sK1)
| ~ v3_lattice3(sK1)
| ~ l1_orders_2(sK1)
| ~ v2_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v4_orders_2(sK0)
| ~ v1_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v3_lattice3(sK0)
| ~ l1_orders_2(sK0)
| ~ v1_funct_1(k1_waybel34(sK0,sK1,sK2))
| ~ v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v18_waybel_0(k1_waybel34(sK0,sK1,sK2),sK1,sK0)
| ~ m1_relset_1(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ spl41_70 ),
inference(forward_subsumption_resolution,[],[f2535,f513]) ).
fof(f2541,plain,
( v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ v3_lattice3(sK1)
| ~ l1_orders_2(sK1)
| ~ v2_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v4_orders_2(sK0)
| ~ v1_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v3_lattice3(sK0)
| ~ l1_orders_2(sK0)
| ~ v1_funct_1(k1_waybel34(sK0,sK1,sK2))
| ~ v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v18_waybel_0(k1_waybel34(sK0,sK1,sK2),sK1,sK0)
| ~ m1_relset_1(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ spl41_70 ),
inference(forward_subsumption_resolution,[],[f2538,f512]) ).
fof(f2544,definition,
( spl41_71
<=> v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0))) ),
introduced(definition,[new_symbols(definition,[spl41_71])],[avatar_definition]) ).
fof(f2545,plain,
( v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ spl41_71 ),
inference(avatar_component_clause,[],[f2544]) ).
fof(f2547,plain,
( v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ l1_orders_2(sK1)
| ~ v2_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v4_orders_2(sK0)
| ~ v1_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v3_lattice3(sK0)
| ~ l1_orders_2(sK0)
| ~ v1_funct_1(k1_waybel34(sK0,sK1,sK2))
| ~ v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v18_waybel_0(k1_waybel34(sK0,sK1,sK2),sK1,sK0)
| ~ m1_relset_1(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ spl41_70 ),
inference(forward_subsumption_resolution,[],[f2541,f511]) ).
fof(f2549,plain,
( v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ v2_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v4_orders_2(sK0)
| ~ v1_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v3_lattice3(sK0)
| ~ l1_orders_2(sK0)
| ~ v1_funct_1(k1_waybel34(sK0,sK1,sK2))
| ~ v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v18_waybel_0(k1_waybel34(sK0,sK1,sK2),sK1,sK0)
| ~ m1_relset_1(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ spl41_70 ),
inference(forward_subsumption_resolution,[],[f2547,f510]) ).
fof(f2551,plain,
( v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ v3_orders_2(sK0)
| ~ v4_orders_2(sK0)
| ~ v1_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v3_lattice3(sK0)
| ~ l1_orders_2(sK0)
| ~ v1_funct_1(k1_waybel34(sK0,sK1,sK2))
| ~ v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v18_waybel_0(k1_waybel34(sK0,sK1,sK2),sK1,sK0)
| ~ m1_relset_1(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ spl41_70 ),
inference(forward_subsumption_resolution,[],[f2549,f509]) ).
fof(f2553,plain,
( v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ v4_orders_2(sK0)
| ~ v1_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v3_lattice3(sK0)
| ~ l1_orders_2(sK0)
| ~ v1_funct_1(k1_waybel34(sK0,sK1,sK2))
| ~ v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v18_waybel_0(k1_waybel34(sK0,sK1,sK2),sK1,sK0)
| ~ m1_relset_1(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ spl41_70 ),
inference(forward_subsumption_resolution,[],[f2551,f508]) ).
fof(f2555,plain,
( v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ v1_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v3_lattice3(sK0)
| ~ l1_orders_2(sK0)
| ~ v1_funct_1(k1_waybel34(sK0,sK1,sK2))
| ~ v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v18_waybel_0(k1_waybel34(sK0,sK1,sK2),sK1,sK0)
| ~ m1_relset_1(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ spl41_70 ),
inference(forward_subsumption_resolution,[],[f2553,f507]) ).
fof(f2557,plain,
( v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ v2_lattice3(sK0)
| ~ v3_lattice3(sK0)
| ~ l1_orders_2(sK0)
| ~ v1_funct_1(k1_waybel34(sK0,sK1,sK2))
| ~ v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v18_waybel_0(k1_waybel34(sK0,sK1,sK2),sK1,sK0)
| ~ m1_relset_1(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ spl41_70 ),
inference(forward_subsumption_resolution,[],[f2555,f506]) ).
fof(f2559,plain,
( v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ v3_lattice3(sK0)
| ~ l1_orders_2(sK0)
| ~ v1_funct_1(k1_waybel34(sK0,sK1,sK2))
| ~ v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v18_waybel_0(k1_waybel34(sK0,sK1,sK2),sK1,sK0)
| ~ m1_relset_1(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ spl41_70 ),
inference(forward_subsumption_resolution,[],[f2557,f505]) ).
fof(f2561,plain,
( v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ l1_orders_2(sK0)
| ~ v1_funct_1(k1_waybel34(sK0,sK1,sK2))
| ~ v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v18_waybel_0(k1_waybel34(sK0,sK1,sK2),sK1,sK0)
| ~ m1_relset_1(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ spl41_70 ),
inference(forward_subsumption_resolution,[],[f2559,f504]) ).
fof(f2563,plain,
( v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ v1_funct_1(k1_waybel34(sK0,sK1,sK2))
| ~ v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v18_waybel_0(k1_waybel34(sK0,sK1,sK2),sK1,sK0)
| ~ m1_relset_1(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ spl41_70 ),
inference(forward_subsumption_resolution,[],[f2561,f503]) ).
fof(f2565,plain,
( v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v18_waybel_0(k1_waybel34(sK0,sK1,sK2),sK1,sK0)
| ~ m1_relset_1(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ spl41_70 ),
inference(forward_subsumption_resolution,[],[f2563,f1793]) ).
fof(f2567,plain,
( v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ m1_relset_1(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ spl41_70 ),
inference(forward_subsumption_resolution,[],[f2565,f1415]) ).
fof(f2569,plain,
( v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ spl41_70 ),
inference(forward_subsumption_resolution,[],[f2567,f1632]) ).
fof(f2571,plain,
( ~ spl41_24
| spl41_71
| ~ spl41_70 ),
inference(avatar_split_clause,[],[f2569,f2512,f2544,f1662]) ).
fof(f2577,plain,
( ~ v1_lattice3(sK1)
| ~ l1_orders_2(sK1)
| ~ spl41_17 ),
inference(resolution,[],[f591,f1482]) ).
fof(f2579,plain,
( ~ l1_orders_2(sK1)
| ~ spl41_17 ),
inference(forward_subsumption_resolution,[],[f2577,f513]) ).
fof(f2580,plain,
( $false
| ~ spl41_17 ),
inference(forward_subsumption_resolution,[],[f2579,f510]) ).
fof(f2581,plain,
~ spl41_17,
inference(avatar_contradiction_clause,[],[f2580]) ).
fof(f2582,plain,
( v3_struct_0(sK1)
| ~ l1_orders_2(sK1)
| spl41_13 ),
inference(forward_subsumption_resolution,[],[f2366,f511]) ).
fof(f2583,plain,
( v3_struct_0(sK1)
| spl41_13 ),
inference(forward_subsumption_resolution,[],[f2582,f510]) ).
fof(f2584,plain,
( spl41_17
| spl41_13 ),
inference(avatar_split_clause,[],[f2583,f1460,f1481]) ).
fof(f2585,plain,
( v3_struct_0(sK0)
| ~ v3_lattice3(sK0)
| ~ l1_orders_2(sK0)
| spl41_14 ),
inference(resolution,[],[f1464,f1014]) ).
fof(f2587,plain,
( ~ v1_lattice3(sK0)
| ~ l1_orders_2(sK0)
| ~ spl41_18 ),
inference(resolution,[],[f1485,f591]) ).
fof(f2589,plain,
( ~ l1_orders_2(sK0)
| ~ spl41_18 ),
inference(forward_subsumption_resolution,[],[f2587,f506]) ).
fof(f2590,plain,
( $false
| ~ spl41_18 ),
inference(forward_subsumption_resolution,[],[f2589,f503]) ).
fof(f2591,plain,
~ spl41_18,
inference(avatar_contradiction_clause,[],[f2590]) ).
fof(f2595,plain,
( v3_struct_0(sK0)
| ~ l1_orders_2(sK0)
| spl41_14 ),
inference(forward_subsumption_resolution,[],[f2585,f504]) ).
fof(f2599,plain,
( v3_struct_0(sK0)
| spl41_14 ),
inference(forward_subsumption_resolution,[],[f2595,f503]) ).
fof(f2600,plain,
( spl41_18
| spl41_14 ),
inference(avatar_split_clause,[],[f2599,f1463,f1484]) ).
fof(f2611,plain,
( ! [X0] :
( ~ v3_waybel_1(k1_waybel_1(k7_lattice3(sK1),k7_lattice3(sK0),k3_waybel34(sK1,sK0,k1_waybel34(sK0,sK1,sK2)),X0),k7_lattice3(sK1),k7_lattice3(sK0))
| ~ v1_funct_2(k3_waybel34(sK1,sK0,k1_waybel34(sK0,sK1,sK2)),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| k3_waybel34(sK1,sK0,k1_waybel34(sK0,sK1,sK2)) = k2_waybel34(k7_lattice3(sK1),k7_lattice3(sK0),X0)
| ~ v3_lattice3(k7_lattice3(sK1))
| ~ v3_lattice3(k7_lattice3(sK0))
| ~ v18_waybel_0(X0,k7_lattice3(sK0),k7_lattice3(sK1))
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ m2_relset_1(X0,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ v2_orders_2(k7_lattice3(sK0))
| ~ v3_orders_2(k7_lattice3(sK0))
| ~ v4_orders_2(k7_lattice3(sK0))
| ~ v1_lattice3(k7_lattice3(sK0))
| ~ v2_lattice3(k7_lattice3(sK0))
| ~ l1_orders_2(k7_lattice3(sK0))
| ~ v2_orders_2(k7_lattice3(sK1))
| ~ v3_orders_2(k7_lattice3(sK1))
| ~ v4_orders_2(k7_lattice3(sK1))
| ~ v1_lattice3(k7_lattice3(sK1))
| ~ v2_lattice3(k7_lattice3(sK1))
| ~ l1_orders_2(k7_lattice3(sK1)) )
| ~ spl41_29
| ~ spl41_30 ),
inference(forward_subsumption_resolution,[],[f2206,f1728]) ).
fof(f2628,plain,
( ! [X0] :
( ~ v3_waybel_1(k1_waybel_1(k7_lattice3(sK1),k7_lattice3(sK0),k1_waybel34(sK0,sK1,sK2),X0),k7_lattice3(sK1),k7_lattice3(sK0))
| ~ v1_funct_2(k3_waybel34(sK1,sK0,k1_waybel34(sK0,sK1,sK2)),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| k3_waybel34(sK1,sK0,k1_waybel34(sK0,sK1,sK2)) = k2_waybel34(k7_lattice3(sK1),k7_lattice3(sK0),X0)
| ~ v3_lattice3(k7_lattice3(sK1))
| ~ v3_lattice3(k7_lattice3(sK0))
| ~ v18_waybel_0(X0,k7_lattice3(sK0),k7_lattice3(sK1))
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ m2_relset_1(X0,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ v2_orders_2(k7_lattice3(sK0))
| ~ v3_orders_2(k7_lattice3(sK0))
| ~ v4_orders_2(k7_lattice3(sK0))
| ~ v1_lattice3(k7_lattice3(sK0))
| ~ v2_lattice3(k7_lattice3(sK0))
| ~ l1_orders_2(k7_lattice3(sK0))
| ~ v2_orders_2(k7_lattice3(sK1))
| ~ v3_orders_2(k7_lattice3(sK1))
| ~ v4_orders_2(k7_lattice3(sK1))
| ~ v1_lattice3(k7_lattice3(sK1))
| ~ v2_lattice3(k7_lattice3(sK1))
| ~ l1_orders_2(k7_lattice3(sK1)) )
| ~ spl41_29
| ~ spl41_30
| ~ spl41_70 ),
inference(forward_demodulation,[],[f2611,f2513]) ).
fof(f2641,plain,
( ! [X0] :
( ~ v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ v3_waybel_1(k1_waybel_1(k7_lattice3(sK1),k7_lattice3(sK0),k1_waybel34(sK0,sK1,sK2),X0),k7_lattice3(sK1),k7_lattice3(sK0))
| k3_waybel34(sK1,sK0,k1_waybel34(sK0,sK1,sK2)) = k2_waybel34(k7_lattice3(sK1),k7_lattice3(sK0),X0)
| ~ v3_lattice3(k7_lattice3(sK1))
| ~ v3_lattice3(k7_lattice3(sK0))
| ~ v18_waybel_0(X0,k7_lattice3(sK0),k7_lattice3(sK1))
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ m2_relset_1(X0,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ v2_orders_2(k7_lattice3(sK0))
| ~ v3_orders_2(k7_lattice3(sK0))
| ~ v4_orders_2(k7_lattice3(sK0))
| ~ v1_lattice3(k7_lattice3(sK0))
| ~ v2_lattice3(k7_lattice3(sK0))
| ~ l1_orders_2(k7_lattice3(sK0))
| ~ v2_orders_2(k7_lattice3(sK1))
| ~ v3_orders_2(k7_lattice3(sK1))
| ~ v4_orders_2(k7_lattice3(sK1))
| ~ v1_lattice3(k7_lattice3(sK1))
| ~ v2_lattice3(k7_lattice3(sK1))
| ~ l1_orders_2(k7_lattice3(sK1)) )
| ~ spl41_29
| ~ spl41_30
| ~ spl41_70 ),
inference(forward_demodulation,[],[f2628,f2513]) ).
fof(f2649,plain,
( ! [X0] :
( ~ v3_waybel_1(k1_waybel_1(k7_lattice3(sK1),k7_lattice3(sK0),k1_waybel34(sK0,sK1,sK2),X0),k7_lattice3(sK1),k7_lattice3(sK0))
| k3_waybel34(sK1,sK0,k1_waybel34(sK0,sK1,sK2)) = k2_waybel34(k7_lattice3(sK1),k7_lattice3(sK0),X0)
| ~ v3_lattice3(k7_lattice3(sK1))
| ~ v3_lattice3(k7_lattice3(sK0))
| ~ v18_waybel_0(X0,k7_lattice3(sK0),k7_lattice3(sK1))
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ m2_relset_1(X0,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ v2_orders_2(k7_lattice3(sK0))
| ~ v3_orders_2(k7_lattice3(sK0))
| ~ v4_orders_2(k7_lattice3(sK0))
| ~ v1_lattice3(k7_lattice3(sK0))
| ~ v2_lattice3(k7_lattice3(sK0))
| ~ l1_orders_2(k7_lattice3(sK0))
| ~ v2_orders_2(k7_lattice3(sK1))
| ~ v3_orders_2(k7_lattice3(sK1))
| ~ v4_orders_2(k7_lattice3(sK1))
| ~ v1_lattice3(k7_lattice3(sK1))
| ~ v2_lattice3(k7_lattice3(sK1))
| ~ l1_orders_2(k7_lattice3(sK1)) )
| ~ spl41_29
| ~ spl41_30
| ~ spl41_70
| ~ spl41_71 ),
inference(forward_subsumption_resolution,[],[f2641,f2545]) ).
fof(f2669,plain,
( ! [X0] :
( k1_waybel34(sK0,sK1,sK2) = k2_waybel34(k7_lattice3(sK1),k7_lattice3(sK0),X0)
| ~ v3_waybel_1(k1_waybel_1(k7_lattice3(sK1),k7_lattice3(sK0),k1_waybel34(sK0,sK1,sK2),X0),k7_lattice3(sK1),k7_lattice3(sK0))
| ~ v3_lattice3(k7_lattice3(sK1))
| ~ v3_lattice3(k7_lattice3(sK0))
| ~ v18_waybel_0(X0,k7_lattice3(sK0),k7_lattice3(sK1))
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ m2_relset_1(X0,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ v2_orders_2(k7_lattice3(sK0))
| ~ v3_orders_2(k7_lattice3(sK0))
| ~ v4_orders_2(k7_lattice3(sK0))
| ~ v1_lattice3(k7_lattice3(sK0))
| ~ v2_lattice3(k7_lattice3(sK0))
| ~ l1_orders_2(k7_lattice3(sK0))
| ~ v2_orders_2(k7_lattice3(sK1))
| ~ v3_orders_2(k7_lattice3(sK1))
| ~ v4_orders_2(k7_lattice3(sK1))
| ~ v1_lattice3(k7_lattice3(sK1))
| ~ v2_lattice3(k7_lattice3(sK1))
| ~ l1_orders_2(k7_lattice3(sK1)) )
| ~ spl41_29
| ~ spl41_30
| ~ spl41_70
| ~ spl41_71 ),
inference(forward_demodulation,[],[f2649,f2513]) ).
fof(f2683,definition,
( spl41_83
<=> ! [X0] :
( k1_waybel34(sK0,sK1,sK2) = k2_waybel34(k7_lattice3(sK1),k7_lattice3(sK0),X0)
| ~ m2_relset_1(X0,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ v1_funct_2(X0,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ v1_funct_1(X0)
| ~ v18_waybel_0(X0,k7_lattice3(sK0),k7_lattice3(sK1))
| ~ v3_waybel_1(k1_waybel_1(k7_lattice3(sK1),k7_lattice3(sK0),k1_waybel34(sK0,sK1,sK2),X0),k7_lattice3(sK1),k7_lattice3(sK0)) ) ),
introduced(definition,[new_symbols(definition,[spl41_83])],[avatar_definition]) ).
fof(f2684,plain,
( ! [X0] :
( ~ v3_waybel_1(k1_waybel_1(k7_lattice3(sK1),k7_lattice3(sK0),k1_waybel34(sK0,sK1,sK2),X0),k7_lattice3(sK1),k7_lattice3(sK0))
| ~ m2_relset_1(X0,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ v1_funct_2(X0,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ v1_funct_1(X0)
| ~ v18_waybel_0(X0,k7_lattice3(sK0),k7_lattice3(sK1))
| k1_waybel34(sK0,sK1,sK2) = k2_waybel34(k7_lattice3(sK1),k7_lattice3(sK0),X0) )
| ~ spl41_83 ),
inference(avatar_component_clause,[],[f2683]) ).
fof(f2685,plain,
( ~ spl41_7
| ~ spl41_8
| ~ spl41_9
| ~ spl41_10
| ~ spl41_11
| ~ spl41_12
| ~ spl41_1
| ~ spl41_2
| ~ spl41_3
| ~ spl41_4
| ~ spl41_5
| ~ spl41_6
| ~ spl41_14
| ~ spl41_13
| spl41_83
| ~ spl41_29
| ~ spl41_30
| ~ spl41_70
| ~ spl41_71 ),
inference(avatar_split_clause,[],[f2669,f2544,f2512,f1731,f1727,f2683,f1460,f1463,f1439,f1436,f1433,f1430,f1427,f1424,f1457,f1454,f1451,f1448,f1445,f1442]) ).
fof(f2707,plain,
( ! [X0] :
( ~ m2_relset_1(X0,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ v1_funct_2(X0,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ v1_funct_1(X0)
| ~ v18_waybel_0(X0,k7_lattice3(sK0),k7_lattice3(sK1))
| k1_waybel34(sK0,sK1,sK2) = k2_waybel34(k7_lattice3(sK1),k7_lattice3(sK0),X0)
| ~ v3_waybel_1(k1_waybel_1(sK0,sK1,X0,k1_waybel34(sK0,sK1,sK2)),sK0,sK1)
| ~ v1_funct_1(k1_waybel34(sK0,sK1,sK2))
| ~ v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ m2_relset_1(k1_waybel34(sK0,sK1,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ m2_relset_1(X0,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ m2_relset_1(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v1_funct_2(X0,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ m2_relset_1(X0,u1_struct_0(sK0),u1_struct_0(sK1))
| v3_struct_0(sK1)
| ~ v2_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ l1_orders_2(sK1)
| v3_struct_0(sK0)
| ~ v2_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v4_orders_2(sK0)
| ~ l1_orders_2(sK0) )
| ~ spl41_83 ),
inference(resolution,[],[f2684,f1326]) ).
fof(f2708,plain,
( ! [X0] :
( ~ m2_relset_1(X0,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ v1_funct_2(X0,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ v1_funct_1(X0)
| ~ v18_waybel_0(X0,k7_lattice3(sK0),k7_lattice3(sK1))
| k1_waybel34(sK0,sK1,sK2) = k2_waybel34(k7_lattice3(sK1),k7_lattice3(sK0),X0)
| ~ v3_waybel_1(k1_waybel_1(sK0,sK1,X0,k1_waybel34(sK0,sK1,sK2)),sK0,sK1)
| ~ v1_funct_1(k1_waybel34(sK0,sK1,sK2))
| ~ v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ m2_relset_1(k1_waybel34(sK0,sK1,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ m2_relset_1(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v1_funct_2(X0,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ m2_relset_1(X0,u1_struct_0(sK0),u1_struct_0(sK1))
| v3_struct_0(sK1)
| ~ v2_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ l1_orders_2(sK1)
| v3_struct_0(sK0)
| ~ v2_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v4_orders_2(sK0)
| ~ l1_orders_2(sK0) )
| ~ spl41_83 ),
inference(duplicate_literal_removal,[],[f2707]) ).
fof(f2709,plain,
( ! [X0] :
( ~ m2_relset_1(X0,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ v1_funct_2(X0,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ v1_funct_1(X0)
| ~ v18_waybel_0(X0,k7_lattice3(sK0),k7_lattice3(sK1))
| k1_waybel34(sK0,sK1,sK2) = k2_waybel34(k7_lattice3(sK1),k7_lattice3(sK0),X0)
| ~ v3_waybel_1(k1_waybel_1(sK0,sK1,X0,k1_waybel34(sK0,sK1,sK2)),sK0,sK1)
| ~ v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ m2_relset_1(k1_waybel34(sK0,sK1,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ m2_relset_1(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v1_funct_2(X0,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ m2_relset_1(X0,u1_struct_0(sK0),u1_struct_0(sK1))
| v3_struct_0(sK1)
| ~ v2_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ l1_orders_2(sK1)
| v3_struct_0(sK0)
| ~ v2_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v4_orders_2(sK0)
| ~ l1_orders_2(sK0) )
| ~ spl41_83 ),
inference(forward_subsumption_resolution,[],[f2708,f1793]) ).
fof(f2710,plain,
( ! [X0] :
( ~ m2_relset_1(X0,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ v1_funct_2(X0,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ v1_funct_1(X0)
| ~ v18_waybel_0(X0,k7_lattice3(sK0),k7_lattice3(sK1))
| k1_waybel34(sK0,sK1,sK2) = k2_waybel34(k7_lattice3(sK1),k7_lattice3(sK0),X0)
| ~ v3_waybel_1(k1_waybel_1(sK0,sK1,X0,k1_waybel34(sK0,sK1,sK2)),sK0,sK1)
| ~ m2_relset_1(k1_waybel34(sK0,sK1,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ m2_relset_1(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v1_funct_2(X0,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ m2_relset_1(X0,u1_struct_0(sK0),u1_struct_0(sK1))
| v3_struct_0(sK1)
| ~ v2_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ l1_orders_2(sK1)
| v3_struct_0(sK0)
| ~ v2_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v4_orders_2(sK0)
| ~ l1_orders_2(sK0) )
| ~ spl41_71
| ~ spl41_83 ),
inference(forward_subsumption_resolution,[],[f2709,f2545]) ).
fof(f2711,plain,
( ! [X0] :
( ~ m2_relset_1(X0,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ v1_funct_2(X0,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ v1_funct_1(X0)
| ~ v18_waybel_0(X0,k7_lattice3(sK0),k7_lattice3(sK1))
| k1_waybel34(sK0,sK1,sK2) = k2_waybel34(k7_lattice3(sK1),k7_lattice3(sK0),X0)
| ~ v3_waybel_1(k1_waybel_1(sK0,sK1,X0,k1_waybel34(sK0,sK1,sK2)),sK0,sK1)
| ~ v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ m2_relset_1(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v1_funct_2(X0,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ m2_relset_1(X0,u1_struct_0(sK0),u1_struct_0(sK1))
| v3_struct_0(sK1)
| ~ v2_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ l1_orders_2(sK1)
| v3_struct_0(sK0)
| ~ v2_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v4_orders_2(sK0)
| ~ l1_orders_2(sK0) )
| ~ spl41_30
| ~ spl41_70
| ~ spl41_71
| ~ spl41_83 ),
inference(forward_subsumption_resolution,[],[f2710,f2516]) ).
fof(f2712,plain,
( ! [X0] :
( ~ m2_relset_1(X0,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ v1_funct_2(X0,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ v1_funct_1(X0)
| ~ v18_waybel_0(X0,k7_lattice3(sK0),k7_lattice3(sK1))
| k1_waybel34(sK0,sK1,sK2) = k2_waybel34(k7_lattice3(sK1),k7_lattice3(sK0),X0)
| ~ v3_waybel_1(k1_waybel_1(sK0,sK1,X0,k1_waybel34(sK0,sK1,sK2)),sK0,sK1)
| ~ v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v1_funct_2(X0,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ m2_relset_1(X0,u1_struct_0(sK0),u1_struct_0(sK1))
| v3_struct_0(sK1)
| ~ v2_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ l1_orders_2(sK1)
| v3_struct_0(sK0)
| ~ v2_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v4_orders_2(sK0)
| ~ l1_orders_2(sK0) )
| ~ spl41_30
| ~ spl41_70
| ~ spl41_71
| ~ spl41_83 ),
inference(forward_subsumption_resolution,[],[f2711,f1629]) ).
fof(f2713,plain,
( ! [X0] :
( ~ m2_relset_1(X0,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ v1_funct_2(X0,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ v1_funct_1(X0)
| ~ v18_waybel_0(X0,k7_lattice3(sK0),k7_lattice3(sK1))
| k1_waybel34(sK0,sK1,sK2) = k2_waybel34(k7_lattice3(sK1),k7_lattice3(sK0),X0)
| ~ v3_waybel_1(k1_waybel_1(sK0,sK1,X0,k1_waybel34(sK0,sK1,sK2)),sK0,sK1)
| ~ v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v1_funct_2(X0,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ m2_relset_1(X0,u1_struct_0(sK0),u1_struct_0(sK1))
| v3_struct_0(sK1)
| ~ v3_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ l1_orders_2(sK1)
| v3_struct_0(sK0)
| ~ v2_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v4_orders_2(sK0)
| ~ l1_orders_2(sK0) )
| ~ spl41_30
| ~ spl41_70
| ~ spl41_71
| ~ spl41_83 ),
inference(forward_subsumption_resolution,[],[f2712,f516]) ).
fof(f2714,plain,
( ! [X0] :
( ~ m2_relset_1(X0,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ v1_funct_2(X0,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ v1_funct_1(X0)
| ~ v18_waybel_0(X0,k7_lattice3(sK0),k7_lattice3(sK1))
| k1_waybel34(sK0,sK1,sK2) = k2_waybel34(k7_lattice3(sK1),k7_lattice3(sK0),X0)
| ~ v3_waybel_1(k1_waybel_1(sK0,sK1,X0,k1_waybel34(sK0,sK1,sK2)),sK0,sK1)
| ~ v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v1_funct_2(X0,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ m2_relset_1(X0,u1_struct_0(sK0),u1_struct_0(sK1))
| v3_struct_0(sK1)
| ~ v4_orders_2(sK1)
| ~ l1_orders_2(sK1)
| v3_struct_0(sK0)
| ~ v2_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v4_orders_2(sK0)
| ~ l1_orders_2(sK0) )
| ~ spl41_30
| ~ spl41_70
| ~ spl41_71
| ~ spl41_83 ),
inference(forward_subsumption_resolution,[],[f2713,f515]) ).
fof(f2715,plain,
( ! [X0] :
( ~ m2_relset_1(X0,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ v1_funct_2(X0,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ v1_funct_1(X0)
| ~ v18_waybel_0(X0,k7_lattice3(sK0),k7_lattice3(sK1))
| k1_waybel34(sK0,sK1,sK2) = k2_waybel34(k7_lattice3(sK1),k7_lattice3(sK0),X0)
| ~ v3_waybel_1(k1_waybel_1(sK0,sK1,X0,k1_waybel34(sK0,sK1,sK2)),sK0,sK1)
| ~ v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v1_funct_2(X0,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ m2_relset_1(X0,u1_struct_0(sK0),u1_struct_0(sK1))
| v3_struct_0(sK1)
| ~ l1_orders_2(sK1)
| v3_struct_0(sK0)
| ~ v2_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v4_orders_2(sK0)
| ~ l1_orders_2(sK0) )
| ~ spl41_30
| ~ spl41_70
| ~ spl41_71
| ~ spl41_83 ),
inference(forward_subsumption_resolution,[],[f2714,f514]) ).
fof(f2716,plain,
( ! [X0] :
( ~ m2_relset_1(X0,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ v1_funct_2(X0,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ v1_funct_1(X0)
| ~ v18_waybel_0(X0,k7_lattice3(sK0),k7_lattice3(sK1))
| k1_waybel34(sK0,sK1,sK2) = k2_waybel34(k7_lattice3(sK1),k7_lattice3(sK0),X0)
| ~ v3_waybel_1(k1_waybel_1(sK0,sK1,X0,k1_waybel34(sK0,sK1,sK2)),sK0,sK1)
| ~ v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v1_funct_2(X0,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ m2_relset_1(X0,u1_struct_0(sK0),u1_struct_0(sK1))
| v3_struct_0(sK1)
| v3_struct_0(sK0)
| ~ v2_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v4_orders_2(sK0)
| ~ l1_orders_2(sK0) )
| ~ spl41_30
| ~ spl41_70
| ~ spl41_71
| ~ spl41_83 ),
inference(forward_subsumption_resolution,[],[f2715,f510]) ).
fof(f2717,plain,
( ! [X0] :
( ~ m2_relset_1(X0,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ v1_funct_2(X0,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ v1_funct_1(X0)
| ~ v18_waybel_0(X0,k7_lattice3(sK0),k7_lattice3(sK1))
| k1_waybel34(sK0,sK1,sK2) = k2_waybel34(k7_lattice3(sK1),k7_lattice3(sK0),X0)
| ~ v3_waybel_1(k1_waybel_1(sK0,sK1,X0,k1_waybel34(sK0,sK1,sK2)),sK0,sK1)
| ~ v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v1_funct_2(X0,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ m2_relset_1(X0,u1_struct_0(sK0),u1_struct_0(sK1))
| v3_struct_0(sK1)
| v3_struct_0(sK0)
| ~ v3_orders_2(sK0)
| ~ v4_orders_2(sK0)
| ~ l1_orders_2(sK0) )
| ~ spl41_30
| ~ spl41_70
| ~ spl41_71
| ~ spl41_83 ),
inference(forward_subsumption_resolution,[],[f2716,f509]) ).
fof(f2718,plain,
( ! [X0] :
( ~ m2_relset_1(X0,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ v1_funct_2(X0,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ v1_funct_1(X0)
| ~ v18_waybel_0(X0,k7_lattice3(sK0),k7_lattice3(sK1))
| k1_waybel34(sK0,sK1,sK2) = k2_waybel34(k7_lattice3(sK1),k7_lattice3(sK0),X0)
| ~ v3_waybel_1(k1_waybel_1(sK0,sK1,X0,k1_waybel34(sK0,sK1,sK2)),sK0,sK1)
| ~ v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v1_funct_2(X0,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ m2_relset_1(X0,u1_struct_0(sK0),u1_struct_0(sK1))
| v3_struct_0(sK1)
| v3_struct_0(sK0)
| ~ v4_orders_2(sK0)
| ~ l1_orders_2(sK0) )
| ~ spl41_30
| ~ spl41_70
| ~ spl41_71
| ~ spl41_83 ),
inference(forward_subsumption_resolution,[],[f2717,f508]) ).
fof(f2719,plain,
( ! [X0] :
( ~ m2_relset_1(X0,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ v1_funct_2(X0,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ v1_funct_1(X0)
| ~ v18_waybel_0(X0,k7_lattice3(sK0),k7_lattice3(sK1))
| k1_waybel34(sK0,sK1,sK2) = k2_waybel34(k7_lattice3(sK1),k7_lattice3(sK0),X0)
| ~ v3_waybel_1(k1_waybel_1(sK0,sK1,X0,k1_waybel34(sK0,sK1,sK2)),sK0,sK1)
| ~ v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v1_funct_2(X0,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ m2_relset_1(X0,u1_struct_0(sK0),u1_struct_0(sK1))
| v3_struct_0(sK1)
| v3_struct_0(sK0)
| ~ l1_orders_2(sK0) )
| ~ spl41_30
| ~ spl41_70
| ~ spl41_71
| ~ spl41_83 ),
inference(forward_subsumption_resolution,[],[f2718,f507]) ).
fof(f2720,plain,
( ! [X0] :
( ~ m2_relset_1(X0,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ v1_funct_2(X0,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ v1_funct_1(X0)
| ~ v18_waybel_0(X0,k7_lattice3(sK0),k7_lattice3(sK1))
| k1_waybel34(sK0,sK1,sK2) = k2_waybel34(k7_lattice3(sK1),k7_lattice3(sK0),X0)
| ~ v3_waybel_1(k1_waybel_1(sK0,sK1,X0,k1_waybel34(sK0,sK1,sK2)),sK0,sK1)
| ~ v1_funct_2(k1_waybel34(sK0,sK1,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v1_funct_2(X0,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ m2_relset_1(X0,u1_struct_0(sK0),u1_struct_0(sK1))
| v3_struct_0(sK1)
| v3_struct_0(sK0) )
| ~ spl41_30
| ~ spl41_70
| ~ spl41_71
| ~ spl41_83 ),
inference(forward_subsumption_resolution,[],[f2719,f503]) ).
fof(f2722,definition,
( spl41_85
<=> ! [X0] :
( ~ m2_relset_1(X0,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ m2_relset_1(X0,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_2(X0,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v3_waybel_1(k1_waybel_1(sK0,sK1,X0,k1_waybel34(sK0,sK1,sK2)),sK0,sK1)
| k1_waybel34(sK0,sK1,sK2) = k2_waybel34(k7_lattice3(sK1),k7_lattice3(sK0),X0)
| ~ v18_waybel_0(X0,k7_lattice3(sK0),k7_lattice3(sK1))
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1))) ) ),
introduced(definition,[new_symbols(definition,[spl41_85])],[avatar_definition]) ).
fof(f2723,plain,
( ! [X0] :
( ~ v3_waybel_1(k1_waybel_1(sK0,sK1,X0,k1_waybel34(sK0,sK1,sK2)),sK0,sK1)
| ~ m2_relset_1(X0,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_2(X0,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ m2_relset_1(X0,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| k1_waybel34(sK0,sK1,sK2) = k2_waybel34(k7_lattice3(sK1),k7_lattice3(sK0),X0)
| ~ v18_waybel_0(X0,k7_lattice3(sK0),k7_lattice3(sK1))
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1))) )
| ~ spl41_85 ),
inference(avatar_component_clause,[],[f2722]) ).
fof(f2724,plain,
( spl41_18
| spl41_17
| ~ spl41_24
| spl41_85
| ~ spl41_30
| ~ spl41_70
| ~ spl41_71
| ~ spl41_83 ),
inference(avatar_split_clause,[],[f2720,f2683,f2544,f2512,f1731,f2722,f1662,f1481,f1484]) ).
fof(f2739,plain,
( ~ m2_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ m2_relset_1(sK2,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| k1_waybel34(sK0,sK1,sK2) = k2_waybel34(k7_lattice3(sK1),k7_lattice3(sK0),sK2)
| ~ v18_waybel_0(sK2,k7_lattice3(sK0),k7_lattice3(sK1))
| ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ spl41_27
| ~ spl41_85 ),
inference(resolution,[],[f2723,f1677]) ).
fof(f2741,plain,
( ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ m2_relset_1(sK2,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| k1_waybel34(sK0,sK1,sK2) = k2_waybel34(k7_lattice3(sK1),k7_lattice3(sK0),sK2)
| ~ v18_waybel_0(sK2,k7_lattice3(sK0),k7_lattice3(sK1))
| ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ spl41_27
| ~ spl41_85 ),
inference(forward_subsumption_resolution,[],[f2739,f517]) ).
fof(f2742,plain,
( ~ m2_relset_1(sK2,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| k1_waybel34(sK0,sK1,sK2) = k2_waybel34(k7_lattice3(sK1),k7_lattice3(sK0),sK2)
| ~ v18_waybel_0(sK2,k7_lattice3(sK0),k7_lattice3(sK1))
| ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ spl41_27
| ~ spl41_85 ),
inference(forward_subsumption_resolution,[],[f2741,f519]) ).
fof(f2743,plain,
( k1_waybel34(sK0,sK1,sK2) = k2_waybel34(k7_lattice3(sK1),k7_lattice3(sK0),sK2)
| ~ v18_waybel_0(sK2,k7_lattice3(sK0),k7_lattice3(sK1))
| ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ spl41_27
| ~ spl41_85 ),
inference(forward_subsumption_resolution,[],[f2742,f2242]) ).
fof(f2744,plain,
( ~ v18_waybel_0(sK2,k7_lattice3(sK0),k7_lattice3(sK1))
| ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ spl41_27
| ~ spl41_85 ),
inference(forward_subsumption_resolution,[],[f2743,f2240]) ).
fof(f2745,plain,
( ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ spl41_27
| ~ spl41_85 ),
inference(forward_subsumption_resolution,[],[f2744,f2335]) ).
fof(f2746,plain,
( ~ v1_funct_2(sK2,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ spl41_27
| ~ spl41_85 ),
inference(forward_subsumption_resolution,[],[f2745,f520]) ).
fof(f2747,plain,
( $false
| ~ spl41_27
| ~ spl41_85 ),
inference(forward_subsumption_resolution,[],[f2746,f2284]) ).
fof(f2748,plain,
( ~ spl41_27
| ~ spl41_85 ),
inference(avatar_contradiction_clause,[],[f2747]) ).
cnf(s6,plain,
spl41_1,
inference(sat_conversion,[],[f1509]) ).
cnf(s8,plain,
spl41_2,
inference(sat_conversion,[],[f1515]) ).
cnf(s10,plain,
spl41_3,
inference(sat_conversion,[],[f1521]) ).
cnf(s12,plain,
spl41_4,
inference(sat_conversion,[],[f1527]) ).
cnf(s14,plain,
spl41_5,
inference(sat_conversion,[],[f1533]) ).
cnf(s16,plain,
spl41_6,
inference(sat_conversion,[],[f1539]) ).
cnf(s18,plain,
spl41_7,
inference(sat_conversion,[],[f1544]) ).
cnf(s20,plain,
spl41_8,
inference(sat_conversion,[],[f1550]) ).
cnf(s22,plain,
spl41_9,
inference(sat_conversion,[],[f1556]) ).
cnf(s24,plain,
spl41_10,
inference(sat_conversion,[],[f1562]) ).
cnf(s26,plain,
spl41_11,
inference(sat_conversion,[],[f1568]) ).
cnf(s28,plain,
spl41_12,
inference(sat_conversion,[],[f1574]) ).
cnf(s32,plain,
( ~ spl41_24
| ~ spl41_25
| spl41_27 ),
inference(sat_conversion,[],[f1678]) ).
cnf(s34,plain,
spl41_24,
inference(sat_conversion,[],[f1700]) ).
cnf(s35,plain,
spl41_25,
inference(sat_conversion,[],[f1702]) ).
cnf(s37,plain,
( ~ spl41_24
| ~ spl41_25
| spl41_29 ),
inference(sat_conversion,[],[f1729]) ).
cnf(s38,plain,
( ~ spl41_24
| ~ spl41_25
| spl41_30 ),
inference(sat_conversion,[],[f1733]) ).
cnf(s69,plain,
( ~ spl41_24
| spl41_70 ),
inference(sat_conversion,[],[f2514]) ).
cnf(s72,plain,
( ~ spl41_24
| ~ spl41_70
| spl41_71 ),
inference(sat_conversion,[],[f2571]) ).
cnf(s75,plain,
~ spl41_17,
inference(sat_conversion,[],[f2581]) ).
cnf(s76,plain,
( spl41_13
| spl41_17 ),
inference(sat_conversion,[],[f2584]) ).
cnf(s78,plain,
~ spl41_18,
inference(sat_conversion,[],[f2591]) ).
cnf(s80,plain,
( spl41_14
| spl41_18 ),
inference(sat_conversion,[],[f2600]) ).
cnf(s92,plain,
( ~ spl41_1
| ~ spl41_2
| ~ spl41_3
| ~ spl41_4
| ~ spl41_5
| ~ spl41_6
| ~ spl41_7
| ~ spl41_8
| ~ spl41_9
| ~ spl41_10
| ~ spl41_11
| ~ spl41_12
| ~ spl41_13
| ~ spl41_14
| ~ spl41_29
| ~ spl41_30
| ~ spl41_70
| ~ spl41_71
| spl41_83 ),
inference(sat_conversion,[],[f2685]) ).
cnf(s94,plain,
( spl41_17
| spl41_18
| ~ spl41_24
| ~ spl41_30
| ~ spl41_70
| ~ spl41_71
| ~ spl41_83
| spl41_85 ),
inference(sat_conversion,[],[f2724]) ).
cnf(s98,plain,
( ~ spl41_27
| ~ spl41_85 ),
inference(sat_conversion,[],[f2748]) ).
cnf(s101,plain,
spl41_14,
inference(rat,[],[s80,s78]) ).
cnf(s102,plain,
spl41_13,
inference(rat,[],[s76,s75]) ).
cnf(s120,plain,
spl41_70,
inference(rat,[],[s69,s34]) ).
cnf(s122,plain,
spl41_30,
inference(rat,[],[s38,s35,s34]) ).
cnf(s123,plain,
spl41_29,
inference(rat,[],[s37,s35,s34]) ).
cnf(s125,plain,
spl41_71,
inference(rat,[],[s72,s34,s120]) ).
cnf(s130,plain,
spl41_27,
inference(rat,[],[s32,s35,s34]) ).
cnf(s131,plain,
~ spl41_85,
inference(rat,[],[s98,s130]) ).
cnf(s133,plain,
~ spl41_83,
inference(rat,[],[s94,s122,s120,s125,s34,s75,s78,s131]) ).
cnf(s136,plain,
~ spl41_1,
inference(rat,[],[s92,s133,s125,s120,s122,s123,s101,s102,s28,s26,s24,s22,s20,s18,s16,s14,s12,s10,s8]) ).
cnf(s137,plain,
$false,
inference(rat,[],[s6,s136]) ).
fof(f2749,plain,
$false,
inference(avatar_sat_refutation,[],[s137]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT354+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.14/0.61 % Computer : n001.cluster.edu
% 0.14/0.61 % Model : x86_64 x86_64
% 0.14/0.61 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.61 % Memory : 8046.5625MB
% 0.14/0.61 % OS : Linux 6.8.0-71-generic
% 0.14/0.61 % CPULimit : 300
% 0.14/0.61 % WCLimit : 300
% 0.14/0.61 % DateTime : Sun Sep 27 15:03:16 UTC 2026
% 0.14/0.61 % CPUTime :
% 0.14/0.61 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.18/0.65 Running first-order theorem proving
% 0.18/0.65 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 10.55/2.76 % (3657544)Detected formulas, will run a generic FOF schedule.
% 10.55/2.76 % (3657556)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2831512499:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 10.55/2.76 % (3657556)Instruction limit reached!
% 10.55/2.76 % (3657556)------------------------------
% 10.55/2.76 % (3657556)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.55/2.76 % (3657556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.55/2.76 % (3657556)CaDiCaL version: 2.1.3
% 10.55/2.76 % (3657556)Termination reason: Instruction limit
% 10.55/2.76 % (3657556)Termination phase: Saturation
% 10.55/2.76 % (3657556)Time elapsed: 0.034 s
% 10.55/2.76 % (3657556)Peak memory usage: 89 MB
% 10.55/2.76 % (3657556)Instructions burned: 119 (million)
% 10.55/2.76 % (3657555)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=962077700:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 10.55/2.76 % (3657553)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=447614277:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 10.55/2.76 % (3657554)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=945757319:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 10.55/2.76 % (3657552)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=549046951:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 10.55/2.76 % (3657558)dis-21_1_sil=8000:lcm=predicate:random_seed=187111461: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)
% 10.55/2.76 % (3657557)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1481486158:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 10.55/2.76 % (3657555)Instruction limit reached!
% 10.55/2.76 % (3657555)------------------------------
% 10.55/2.76 % (3657555)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.55/2.76 % (3657555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.55/2.76 % (3657555)CaDiCaL version: 2.1.3
% 10.55/2.76 % (3657555)Termination reason: Instruction limit
% 10.55/2.76 % (3657555)Termination phase: Saturation
% 10.55/2.76 % (3657555)Time elapsed: 0.100 s
% 10.55/2.76 % (3657555)Peak memory usage: 90 MB
% 10.55/2.76 % (3657555)Instructions burned: 110 (million)
% 10.55/2.76 % (3657560)lrs+10_1_sil=8000:sp=occurrence:random_seed=161999634:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 10.55/2.76 % (3657558)Instruction limit reached!
% 10.55/2.76 % (3657558)------------------------------
% 10.55/2.76 % (3657558)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.55/2.76 % (3657558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.55/2.76 % (3657558)CaDiCaL version: 2.1.3
% 10.55/2.76 % (3657558)Termination reason: Instruction limit
% 10.55/2.76 % (3657558)Termination phase: Saturation
% 10.55/2.76 % (3657558)Time elapsed: 0.126 s
% 10.55/2.76 % (3657558)Peak memory usage: 93 MB
% 10.55/2.76 % (3657558)Instructions burned: 130 (million)
% 10.55/2.76 % (3657557)Instruction limit reached!
% 10.55/2.76 % (3657557)------------------------------
% 10.55/2.76 % (3657557)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.55/2.76 % (3657557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.55/2.76 % (3657557)CaDiCaL version: 2.1.3
% 10.55/2.76 % (3657557)Termination reason: Instruction limit
% 10.55/2.76 % (3657557)Termination phase: Saturation
% 10.55/2.76 % (3657557)Time elapsed: 0.128 s
% 10.55/2.76 % (3657557)Peak memory usage: 90 MB
% 10.55/2.76 % (3657557)Instructions burned: 140 (million)
% 10.55/2.76 % (3657560)Instruction limit reached!
% 10.55/2.76 % (3657560)------------------------------
% 10.55/2.76 % (3657560)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.55/2.76 % (3657560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.55/2.76 % (3657560)CaDiCaL version: 2.1.3
% 10.55/2.76 % (3657560)Termination reason: Instruction limit
% 10.55/2.76 % (3657560)Termination phase: Saturation
% 10.55/2.76 % (3657560)Time elapsed: 0.131 s
% 10.55/2.76 % (3657560)Peak memory usage: 92 MB
% 10.55/2.76 % (3657560)Instructions burned: 286 (million)
% 10.55/2.76 % (3657567)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2754814937:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi)
% 10.55/2.76 % (3657570)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=1549668214:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi)
% 10.55/2.76 % (3657569)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2376756087:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi)
% 10.55/2.76 % (3657571)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=22894968:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 10.55/2.76 % (3657567)Instruction limit reached!
% 10.55/2.76 % (3657567)------------------------------
% 10.55/2.76 % (3657567)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.55/2.76 % (3657567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.55/2.76 % (3657567)CaDiCaL version: 2.1.3
% 10.55/2.76 % (3657567)Termination reason: Instruction limit
% 10.55/2.76 % (3657567)Termination phase: Saturation
% 10.55/2.76 % (3657567)Time elapsed: 0.134 s
% 10.55/2.76 % (3657567)Peak memory usage: 89 MB
% 10.55/2.76 % (3657567)Instructions burned: 157 (million)
% 10.55/2.76 % (3657570)Instruction limit reached!
% 10.55/2.76 % (3657570)------------------------------
% 10.55/2.76 % (3657570)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.55/2.76 % (3657570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.55/2.76 % (3657570)CaDiCaL version: 2.1.3
% 10.55/2.76 % (3657570)Termination reason: Instruction limit
% 10.55/2.76 % (3657570)Termination phase: Saturation
% 10.55/2.76 % (3657570)Time elapsed: 0.213 s
% 10.55/2.76 % (3657570)Peak memory usage: 91 MB
% 10.55/2.76 % (3657570)Instructions burned: 249 (million)
% 10.55/2.76 % (3657571)Instruction limit reached!
% 10.55/2.76 % (3657571)------------------------------
% 10.55/2.76 % (3657571)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.55/2.76 % (3657571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.55/2.76 % (3657571)CaDiCaL version: 2.1.3
% 10.55/2.76 % (3657571)Termination reason: Instruction limit
% 10.55/2.76 % (3657571)Termination phase: Saturation
% 10.55/2.76 % (3657571)Time elapsed: 0.132 s
% 10.55/2.76 % (3657571)Peak memory usage: 91 MB
% 10.55/2.76 % (3657571)Instructions burned: 294 (million)
% 10.55/2.76 % (3657569)Instruction limit reached!
% 10.55/2.76 % (3657569)------------------------------
% 10.55/2.76 % (3657569)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.55/2.76 % (3657569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.55/2.76 % (3657569)CaDiCaL version: 2.1.3
% 10.55/2.76 % (3657569)Termination reason: Instruction limit
% 10.55/2.76 % (3657569)Termination phase: Saturation
% 10.55/2.76 % (3657569)Time elapsed: 0.273 s
% 10.55/2.76 % (3657569)Peak memory usage: 91 MB
% 10.55/2.76 % (3657569)Instructions burned: 325 (million)
% 10.55/2.76 % (3657578)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1310104326:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi)
% 10.55/2.76 % (3657576)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1232751609:i=2350_2993 on theBenchmark for (2993ds/2350Mi)
% 10.55/2.76 % (3657577)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1730469795:cts=off:i=113:fsr=off:ss=included:sgt=4_2992 on theBenchmark for (2992ds/113Mi)
% 10.55/2.76 % (3657578)Instruction limit reached!
% 10.55/2.76 % (3657578)------------------------------
% 10.55/2.76 % (3657578)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.55/2.76 % (3657578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.55/2.76 % (3657578)CaDiCaL version: 2.1.3
% 10.55/2.76 % (3657578)Termination reason: Instruction limit
% 10.55/2.76 % (3657578)Termination phase: Saturation
% 10.55/2.76 % (3657578)Time elapsed: 0.036 s
% 10.55/2.76 % (3657578)Peak memory usage: 89 MB
% 10.55/2.76 % (3657578)Instructions burned: 128 (million)
% 10.55/2.76 % (3657577)Instruction limit reached!
% 10.55/2.76 % (3657577)------------------------------
% 10.55/2.76 % (3657577)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.55/2.76 % (3657577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.55/2.76 % (3657577)CaDiCaL version: 2.1.3
% 10.55/2.76 % (3657577)Termination reason: Instruction limit
% 10.55/2.76 % (3657577)Termination phase: Saturation
% 10.55/2.76 % (3657577)Time elapsed: 0.058 s
% 10.55/2.76 % (3657577)Peak memory usage: 90 MB
% 10.55/2.76 % (3657577)Instructions burned: 114 (million)
% 10.55/2.76 % (3657579)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1412801862:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 10.55/2.76 % (3657584)lrs+10_1_sil=8000:sp=occurrence:random_seed=1441548148:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi)
% 10.55/2.76 % (3657579)Instruction limit reached!
% 10.55/2.76 % (3657579)------------------------------
% 10.55/2.76 % (3657579)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.55/2.76 % (3657579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.55/2.76 % (3657579)CaDiCaL version: 2.1.3
% 10.55/2.76 % (3657579)Termination reason: Instruction limit
% 10.55/2.76 % (3657579)Termination phase: Saturation
% 10.55/2.76 % (3657579)Time elapsed: 0.063 s
% 10.55/2.76 % (3657579)Peak memory usage: 89 MB
% 10.55/2.76 % (3657579)Instructions burned: 115 (million)
% 10.55/2.76 % (3657585)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2423156460:i=437:sd=1:aac=none:ss=included_2990 on theBenchmark for (2990ds/437Mi)
% 10.55/2.76 % (3657588)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=4026845382:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi)
% 10.55/2.76 % (3657584)Instruction limit reached!
% 10.55/2.76 % (3657584)------------------------------
% 10.55/2.76 % (3657584)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.55/2.76 % (3657584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.55/2.76 % (3657584)CaDiCaL version: 2.1.3
% 10.55/2.76 % (3657584)Termination reason: Instruction limit
% 10.55/2.76 % (3657584)Termination phase: Saturation
% 10.55/2.76 % (3657584)Time elapsed: 0.235 s
% 10.55/2.76 % (3657584)Peak memory usage: 97 MB
% 10.55/2.76 % (3657584)Instructions burned: 911 (million)
% 10.55/2.76 % (3657585)Instruction limit reached!
% 10.55/2.76 % (3657585)------------------------------
% 10.55/2.76 % (3657585)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.55/2.76 % (3657585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.55/2.76 % (3657585)CaDiCaL version: 2.1.3
% 10.55/2.76 % (3657585)Termination reason: Instruction limit
% 10.55/2.76 % (3657585)Termination phase: Saturation
% 10.55/2.76 % (3657585)Time elapsed: 0.196 s
% 10.55/2.76 % (3657585)Peak memory usage: 92 MB
% 10.55/2.76 % (3657585)Instructions burned: 439 (million)
% 10.55/2.76 % (3657628)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3423234720:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2987 on theBenchmark for (2987ds/134Mi)
% 10.55/2.76 % (3657553)First to succeed.
% 10.55/2.76 % (3657628)Instruction limit reached!
% 10.55/2.76 % (3657628)------------------------------
% 10.55/2.76 % (3657628)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.55/2.76 % (3657628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.55/2.76 % (3657628)CaDiCaL version: 2.1.3
% 10.55/2.76 % (3657628)Termination reason: Instruction limit
% 10.55/2.76 % (3657628)Termination phase: Saturation
% 10.55/2.76 % (3657628)Time elapsed: 0.039 s
% 10.55/2.76 % (3657628)Peak memory usage: 91 MB
% 10.55/2.76 % (3657628)Instructions burned: 136 (million)
% 10.55/2.76 % (3657553)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3657544"
% 10.55/2.76 % (3657629)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1683417568:st=8:i=592:sd=3:ep=RST:ss=axioms_2987 on theBenchmark for (2987ds/592Mi)
% 10.55/2.76 % (3657640)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=4088589392:st=3:i=13193:sd=3:ss=axioms_2986 on theBenchmark for (2986ds/13193Mi)
% 10.55/2.76 % (3657552)Also succeeded, but the first one will report.
% 10.55/2.76 % (3657553)Refutation found. Thanks to Tanya!
% 10.55/2.76 % SZS status Theorem for theBenchmark
% 10.55/2.76 % SZS output start Proof for theBenchmark
% See solution above
% 12.14/2.96 % (3657553)------------------------------
% 12.14/2.96 % (3657553)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.14/2.96 % (3657553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.14/2.96 % (3657553)CaDiCaL version: 2.1.3
% 12.14/2.96 % (3657553)Termination reason: Refutation
% 12.14/2.96 % (3657553)Time elapsed: 1.148 s
% 12.14/2.96 % (3657553)Peak memory usage: 136 MB
% 12.14/2.96 % (3657553)Instructions burned: 1384 (million)
% 12.14/2.96 % (3657553)------------------------------
% 12.14/2.96 % (3657553)------------------------------
% 12.14/2.96 % (3657544)Success in time 1.627 s
% 12.14/2.96 % Vampire exiting
%------------------------------------------------------------------------------