%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LAT355+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n007.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:48:35 AM UTC 2026
% Result : Theorem 1.38s 0.79s
% Output : Refutation 1.38s
% Verified :
% SZS Type : Refutation
% Derivation depth : 49
% Number of leaves : 29
% Syntax : Number of formulae : 386 ( 63 unt; 14 def)
% Number of atoms : 3241 ( 76 equ)
% Maximal formula atoms : 43 ( 8 avg)
% Number of connectives : 4742 (1887 ~;2498 |; 294 &)
% ( 24 <=>; 39 =>; 0 <=; 0 <~>)
% Maximal formula depth : 48 ( 9 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 42 ( 40 usr; 15 prp; 0-3 aty)
% Number of functors : 9 ( 9 usr; 3 con; 0-4 aty)
% Number of variables : 264 ( 0 sgn 258 !; 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))
& v18_waybel_0(X2,X0,X1)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> k1_waybel34(k7_lattice3(X0),k7_lattice3(X1),k3_waybel34(X0,X1,X2)) = k2_waybel34(X1,X0,X2) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t5_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))
& v18_waybel_0(X2,X0,X1)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> k1_waybel34(k7_lattice3(X0),k7_lattice3(X1),k3_waybel34(X0,X1,X2)) = k2_waybel34(X1,X0,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/sandbox/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/sandbox/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/sandbox/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/sandbox/benchmark/theBenchmark.p',d3_waybel34) ).
fof(f84,axiom,
! [X0,X1,X2] :
( ( v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& v2_lattice3(X0)
& l1_orders_2(X0)
& v2_orders_2(X1)
& v3_orders_2(X1)
& v4_orders_2(X1)
& v1_lattice3(X1)
& v2_lattice3(X1)
& l1_orders_2(X1)
& v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
& m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0)) )
=> ( v1_funct_1(k2_waybel34(X0,X1,X2))
& v1_funct_2(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
& m2_relset_1(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k2_waybel34) ).
fof(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/sandbox/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/sandbox/benchmark/theBenchmark.p',dt_k7_lattice3) ).
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/sandbox/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/sandbox/benchmark/theBenchmark.p',fc2_yellow_7) ).
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/sandbox/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/sandbox/benchmark/theBenchmark.p',fc4_waybel34) ).
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/sandbox/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/sandbox/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/sandbox/benchmark/theBenchmark.p',t44_yellow_7) ).
fof(f237,plain,
! [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))
& 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)) ) ),
inference(pure_predicate_removal,[],[f132]) ).
fof(f241,plain,
! [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)))
& 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))
& 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)) ) ),
inference(pure_predicate_removal,[],[f237]) ).
fof(f255,plain,
! [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)))
& 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))
& v4_waybel_1(k3_waybel34(X0,X1,X2),k7_lattice3(X0),k7_lattice3(X1)) ) ),
inference(pure_predicate_removal,[],[f241]) ).
fof(f257,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( k1_waybel34(k7_lattice3(X0),k7_lattice3(X1),k3_waybel34(X0,X1,X2)) != k2_waybel34(X1,X0,X2)
& v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v18_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(f258,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( k1_waybel34(k7_lattice3(X0),k7_lattice3(X1),k3_waybel34(X0,X1,X2)) != k2_waybel34(X1,X0,X2)
& v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v18_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,[],[f257]) ).
fof(f286,plain,
! [X0] :
( ~ v3_struct_0(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f23]) ).
fof(f287,plain,
! [X0] :
( ~ v3_struct_0(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f286]) ).
fof(f371,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(f372,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,[],[f371]) ).
fof(f373,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(f374,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,[],[f373]) ).
fof(f375,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(f376,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,[],[f375]) ).
fof(f381,plain,
! [X0,X1,X2] :
( ( v1_funct_1(k2_waybel34(X0,X1,X2))
& v1_funct_2(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
& m2_relset_1(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1)) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f84]) ).
fof(f382,plain,
! [X0,X1,X2] :
( ( v1_funct_1(k2_waybel34(X0,X1,X2))
& v1_funct_2(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
& m2_relset_1(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1)) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0)) ),
inference(flattening,[],[f381]) ).
fof(f383,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(f384,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,[],[f383]) ).
fof(f387,plain,
! [X0] :
( ( v1_orders_2(k7_lattice3(X0))
& l1_orders_2(k7_lattice3(X0)) )
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f90]) ).
fof(f420,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(f421,plain,
! [X0] :
( ( v1_orders_2(k7_lattice3(X0))
& v2_orders_2(k7_lattice3(X0)) )
| ~ v2_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f420]) ).
fof(f427,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(f428,plain,
! [X0] :
( ( v1_orders_2(k7_lattice3(X0))
& v3_orders_2(k7_lattice3(X0)) )
| ~ v3_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f427]) ).
fof(f435,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(f436,plain,
! [X0] :
( ( v1_orders_2(k7_lattice3(X0))
& v4_orders_2(k7_lattice3(X0)) )
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f435]) ).
fof(f437,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)))
& 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))
& v4_waybel_1(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,[],[f255]) ).
fof(f438,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)))
& 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))
& v4_waybel_1(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,[],[f437]) ).
fof(f458,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(f459,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,[],[f458]) ).
fof(f501,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(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)) )
| 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,[],[f501]) ).
fof(f509,plain,
m2_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1)),
inference(cnf_transformation,[],[f258]) ).
fof(f510,plain,
v18_waybel_0(sK2,sK0,sK1),
inference(cnf_transformation,[],[f258]) ).
fof(f511,plain,
v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1)),
inference(cnf_transformation,[],[f258]) ).
fof(f512,plain,
v1_funct_1(sK2),
inference(cnf_transformation,[],[f258]) ).
fof(f513,plain,
k1_waybel34(k7_lattice3(sK0),k7_lattice3(sK1),k3_waybel34(sK0,sK1,sK2)) != k2_waybel34(sK1,sK0,sK2),
inference(cnf_transformation,[],[f258]) ).
fof(f514,plain,
l1_orders_2(sK1),
inference(cnf_transformation,[],[f258]) ).
fof(f515,plain,
v3_lattice3(sK1),
inference(cnf_transformation,[],[f258]) ).
fof(f516,plain,
v2_lattice3(sK1),
inference(cnf_transformation,[],[f258]) ).
fof(f517,plain,
v1_lattice3(sK1),
inference(cnf_transformation,[],[f258]) ).
fof(f518,plain,
v4_orders_2(sK1),
inference(cnf_transformation,[],[f258]) ).
fof(f519,plain,
v3_orders_2(sK1),
inference(cnf_transformation,[],[f258]) ).
fof(f520,plain,
v2_orders_2(sK1),
inference(cnf_transformation,[],[f258]) ).
fof(f521,plain,
l1_orders_2(sK0),
inference(cnf_transformation,[],[f258]) ).
fof(f522,plain,
v3_lattice3(sK0),
inference(cnf_transformation,[],[f258]) ).
fof(f523,plain,
v2_lattice3(sK0),
inference(cnf_transformation,[],[f258]) ).
fof(f524,plain,
v1_lattice3(sK0),
inference(cnf_transformation,[],[f258]) ).
fof(f525,plain,
v4_orders_2(sK0),
inference(cnf_transformation,[],[f258]) ).
fof(f526,plain,
v3_orders_2(sK0),
inference(cnf_transformation,[],[f258]) ).
fof(f527,plain,
v2_orders_2(sK0),
inference(cnf_transformation,[],[f258]) ).
fof(f579,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v3_struct_0(X0) ),
inference(cnf_transformation,[],[f287]) ).
fof(f688,plain,
! [X2,X3,X0,X1] :
( ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ v17_waybel_0(X2,X0,X1)
| ~ v3_lattice3(X1)
| ~ v3_lattice3(X0)
| ~ m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X3)
| ~ v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1)
| k1_waybel34(X0,X1,X2) = X3 ),
inference(cnf_transformation,[],[f372]) ).
fof(f691,plain,
! [X2,X3,X0,X1] :
( ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X2)
| ~ v18_waybel_0(X2,X1,X0)
| ~ v3_lattice3(X1)
| ~ v3_lattice3(X0)
| ~ m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X3)
| v3_waybel_1(k1_waybel_1(X0,X1,X3,X2),X0,X1)
| k2_waybel34(X0,X1,X2) != X3 ),
inference(cnf_transformation,[],[f374]) ).
fof(f692,plain,
! [X2,X0,X1] :
( ~ l1_orders_2(X0)
| ~ l1_orders_2(X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| k3_waybel34(X0,X1,X2) = X2 ),
inference(cnf_transformation,[],[f376]) ).
fof(f700,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| m2_relset_1(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f382]) ).
fof(f701,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| v1_funct_2(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f382]) ).
fof(f702,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| v1_funct_1(k2_waybel34(X0,X1,X2)) ),
inference(cnf_transformation,[],[f382]) ).
fof(f703,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| ~ l1_orders_2(X0)
| m2_relset_1(k3_waybel34(X0,X1,X2),u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1))) ),
inference(cnf_transformation,[],[f384]) ).
fof(f704,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| ~ l1_orders_2(X0)
| v1_funct_2(k3_waybel34(X0,X1,X2),u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1))) ),
inference(cnf_transformation,[],[f384]) ).
fof(f708,plain,
! [X0] :
( ~ l1_orders_2(X0)
| l1_orders_2(k7_lattice3(X0)) ),
inference(cnf_transformation,[],[f387]) ).
fof(f792,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v2_orders_2(X0)
| v2_orders_2(k7_lattice3(X0)) ),
inference(cnf_transformation,[],[f421]) ).
fof(f811,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v3_orders_2(X0)
| v3_orders_2(k7_lattice3(X0)) ),
inference(cnf_transformation,[],[f428]) ).
fof(f824,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v4_orders_2(X0)
| v4_orders_2(k7_lattice3(X0)) ),
inference(cnf_transformation,[],[f436]) ).
fof(f828,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v18_waybel_0(X2,X0,X1)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| ~ v3_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| v17_waybel_0(k3_waybel34(X0,X1,X2),k7_lattice3(X0),k7_lattice3(X1)) ),
inference(cnf_transformation,[],[f438]) ).
fof(f867,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| v3_struct_0(X0)
| v3_lattice3(k7_lattice3(X0)) ),
inference(cnf_transformation,[],[f459]) ).
fof(f868,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| v3_struct_0(X0)
| v2_lattice3(k7_lattice3(X0)) ),
inference(cnf_transformation,[],[f459]) ).
fof(f869,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| v3_struct_0(X0)
| v1_lattice3(k7_lattice3(X0)) ),
inference(cnf_transformation,[],[f459]) ).
fof(f1140,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f188]) ).
fof(f1146,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ l1_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| v3_struct_0(X0)
| ~ l1_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| v3_struct_0(X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X3)
| ~ m2_relset_1(X4,u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
| ~ v1_funct_2(X4,u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
| ~ v1_funct_1(X4)
| ~ m2_relset_1(X5,u1_struct_0(k7_lattice3(X1)),u1_struct_0(k7_lattice3(X0)))
| ~ v1_funct_2(X5,u1_struct_0(k7_lattice3(X1)),u1_struct_0(k7_lattice3(X0)))
| ~ v1_funct_1(X5)
| X3 != X5
| X2 != X4
| 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) ),
inference(cnf_transformation,[],[f502]) ).
fof(f1154,plain,
! [X2,X0,X1] :
( ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X2)
| ~ v18_waybel_0(X2,X1,X0)
| ~ v3_lattice3(X1)
| ~ v3_lattice3(X0)
| ~ m2_relset_1(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(k2_waybel34(X0,X1,X2))
| v3_waybel_1(k1_waybel_1(X0,X1,k2_waybel34(X0,X1,X2),X2),X0,X1) ),
inference(equality_resolution,[],[f691]) ).
fof(f1155,plain,
! [X2,X0,X1,X4,X5] :
( ~ l1_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| v3_struct_0(X0)
| ~ l1_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| v3_struct_0(X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ m2_relset_1(X5,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X5,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X5)
| ~ m2_relset_1(X4,u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
| ~ v1_funct_2(X4,u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
| ~ v1_funct_1(X4)
| ~ m2_relset_1(X5,u1_struct_0(k7_lattice3(X1)),u1_struct_0(k7_lattice3(X0)))
| ~ v1_funct_2(X5,u1_struct_0(k7_lattice3(X1)),u1_struct_0(k7_lattice3(X0)))
| ~ v1_funct_1(X5)
| X2 != X4
| 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,X5),X0,X1) ),
inference(equality_resolution,[],[f1146]) ).
fof(f1156,plain,
! [X0,X1,X4,X5] :
( ~ l1_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| v3_struct_0(X0)
| ~ l1_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| v3_struct_0(X1)
| ~ m2_relset_1(X4,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X4,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X4)
| ~ m2_relset_1(X5,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X5,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X5)
| ~ m2_relset_1(X4,u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
| ~ v1_funct_2(X4,u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
| ~ v1_funct_1(X4)
| ~ m2_relset_1(X5,u1_struct_0(k7_lattice3(X1)),u1_struct_0(k7_lattice3(X0)))
| ~ v1_funct_2(X5,u1_struct_0(k7_lattice3(X1)),u1_struct_0(k7_lattice3(X0)))
| ~ v1_funct_1(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) ),
inference(equality_resolution,[],[f1155]) ).
fof(f1159,plain,
~ v2_orders_2(sK0),
inference(consistent_polarity_flipping,[],[f527]) ).
fof(f1160,plain,
~ v3_orders_2(sK0),
inference(consistent_polarity_flipping,[],[f526]) ).
fof(f1161,plain,
~ l1_orders_2(sK0),
inference(consistent_polarity_flipping,[],[f521]) ).
fof(f1162,plain,
~ v2_orders_2(sK1),
inference(consistent_polarity_flipping,[],[f520]) ).
fof(f1163,plain,
~ v3_orders_2(sK1),
inference(consistent_polarity_flipping,[],[f519]) ).
fof(f1164,plain,
~ l1_orders_2(sK1),
inference(consistent_polarity_flipping,[],[f514]) ).
fof(f1165,plain,
~ v18_waybel_0(sK2,sK0,sK1),
inference(consistent_polarity_flipping,[],[f510]) ).
fof(f1217,plain,
! [X0] :
( ~ v1_lattice3(X0)
| l1_orders_2(X0)
| v3_struct_0(X0) ),
inference(consistent_polarity_flipping,[],[f579]) ).
fof(f1324,plain,
! [X2,X3,X0,X1] :
( v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| v3_orders_2(X0)
| v2_orders_2(X0)
| l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| v3_orders_2(X1)
| v2_orders_2(X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ v17_waybel_0(X2,X0,X1)
| ~ v3_lattice3(X1)
| ~ v3_lattice3(X0)
| ~ m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X3)
| l1_orders_2(X0)
| k1_waybel34(X0,X1,X2) = X3 ),
inference(consistent_polarity_flipping,[],[f688]) ).
fof(f1325,plain,
! [X2,X0,X1] :
( ~ v1_funct_2(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| v3_orders_2(X0)
| v2_orders_2(X0)
| l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| v3_orders_2(X1)
| v2_orders_2(X1)
| ~ m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X2)
| v18_waybel_0(X2,X1,X0)
| ~ v3_lattice3(X1)
| ~ v3_lattice3(X0)
| ~ m2_relset_1(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
| l1_orders_2(X0)
| ~ v1_funct_1(k2_waybel34(X0,X1,X2))
| ~ v3_waybel_1(k1_waybel_1(X0,X1,k2_waybel34(X0,X1,X2),X2),X0,X1) ),
inference(consistent_polarity_flipping,[],[f1154]) ).
fof(f1327,plain,
! [X2,X0,X1] :
( ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| l1_orders_2(X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| l1_orders_2(X0)
| ~ v1_funct_1(X2)
| k3_waybel34(X0,X1,X2) = X2 ),
inference(consistent_polarity_flipping,[],[f692]) ).
fof(f1334,plain,
! [X2,X0,X1] :
( ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X2)
| l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| v3_orders_2(X1)
| v2_orders_2(X1)
| l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| v3_orders_2(X0)
| v2_orders_2(X0)
| v1_funct_1(k2_waybel34(X0,X1,X2)) ),
inference(consistent_polarity_flipping,[],[f702]) ).
fof(f1335,plain,
! [X2,X0,X1] :
( ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X2)
| l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| v3_orders_2(X1)
| v2_orders_2(X1)
| l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| v3_orders_2(X0)
| v2_orders_2(X0)
| v1_funct_2(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1)) ),
inference(consistent_polarity_flipping,[],[f701]) ).
fof(f1336,plain,
! [X2,X0,X1] :
( m2_relset_1(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X2)
| l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| v3_orders_2(X1)
| v2_orders_2(X1)
| l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| v3_orders_2(X0)
| v2_orders_2(X0)
| ~ m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0)) ),
inference(consistent_polarity_flipping,[],[f700]) ).
fof(f1338,plain,
! [X2,X0,X1] :
( v1_funct_2(k3_waybel34(X0,X1,X2),u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| l1_orders_2(X1)
| l1_orders_2(X0)
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(consistent_polarity_flipping,[],[f704]) ).
fof(f1339,plain,
! [X2,X0,X1] :
( m2_relset_1(k3_waybel34(X0,X1,X2),u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| l1_orders_2(X1)
| l1_orders_2(X0)
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(consistent_polarity_flipping,[],[f703]) ).
fof(f1342,plain,
! [X0] :
( ~ l1_orders_2(k7_lattice3(X0))
| l1_orders_2(X0) ),
inference(consistent_polarity_flipping,[],[f708]) ).
fof(f1423,plain,
! [X0] :
( ~ v2_orders_2(k7_lattice3(X0))
| v2_orders_2(X0)
| l1_orders_2(X0) ),
inference(consistent_polarity_flipping,[],[f792]) ).
fof(f1442,plain,
! [X0] :
( ~ v3_orders_2(k7_lattice3(X0))
| v3_orders_2(X0)
| l1_orders_2(X0) ),
inference(consistent_polarity_flipping,[],[f811]) ).
fof(f1455,plain,
! [X0] :
( v4_orders_2(k7_lattice3(X0))
| ~ v4_orders_2(X0)
| l1_orders_2(X0) ),
inference(consistent_polarity_flipping,[],[f824]) ).
fof(f1460,plain,
! [X2,X0,X1] :
( v17_waybel_0(k3_waybel34(X0,X1,X2),k7_lattice3(X0),k7_lattice3(X1))
| v18_waybel_0(X2,X0,X1)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| l1_orders_2(X1)
| ~ v3_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| v3_orders_2(X1)
| v2_orders_2(X1)
| l1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| v3_orders_2(X0)
| v2_orders_2(X0)
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(consistent_polarity_flipping,[],[f828]) ).
fof(f1493,plain,
! [X0] :
( v1_lattice3(k7_lattice3(X0))
| ~ v3_lattice3(X0)
| ~ v3_struct_0(X0)
| l1_orders_2(X0) ),
inference(consistent_polarity_flipping,[],[f869]) ).
fof(f1494,plain,
! [X0] :
( v2_lattice3(k7_lattice3(X0))
| ~ v3_lattice3(X0)
| ~ v3_struct_0(X0)
| l1_orders_2(X0) ),
inference(consistent_polarity_flipping,[],[f868]) ).
fof(f1495,plain,
! [X0] :
( v3_lattice3(k7_lattice3(X0))
| ~ v3_lattice3(X0)
| ~ v3_struct_0(X0)
| l1_orders_2(X0) ),
inference(consistent_polarity_flipping,[],[f867]) ).
fof(f1678,plain,
! [X0,X1,X4,X5] :
( l1_orders_2(X0)
| ~ v4_orders_2(X0)
| v3_orders_2(X0)
| v2_orders_2(X0)
| ~ v3_struct_0(X0)
| l1_orders_2(X1)
| ~ v4_orders_2(X1)
| v3_orders_2(X1)
| v2_orders_2(X1)
| ~ v3_struct_0(X1)
| ~ m2_relset_1(X4,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X4,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X4)
| ~ m2_relset_1(X5,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X5,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X5)
| ~ m2_relset_1(X4,u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
| ~ v1_funct_2(X4,u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
| ~ v1_funct_1(X4)
| ~ m2_relset_1(X5,u1_struct_0(k7_lattice3(X1)),u1_struct_0(k7_lattice3(X0)))
| ~ v1_funct_2(X5,u1_struct_0(k7_lattice3(X1)),u1_struct_0(k7_lattice3(X0)))
| ~ v1_funct_1(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) ),
inference(consistent_polarity_flipping,[],[f1156]) ).
fof(f1686,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))
| ~ v4_orders_2(X0)
| v3_orders_2(X0)
| v2_orders_2(X0)
| ~ v3_struct_0(X0)
| l1_orders_2(X1)
| ~ v4_orders_2(X1)
| v3_orders_2(X1)
| v2_orders_2(X1)
| ~ v3_struct_0(X1)
| ~ m2_relset_1(X4,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X4,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X4)
| ~ m2_relset_1(X5,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X5,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X5)
| ~ m2_relset_1(X4,u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
| ~ v1_funct_2(X4,u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
| ~ m2_relset_1(X5,u1_struct_0(k7_lattice3(X1)),u1_struct_0(k7_lattice3(X0)))
| ~ v1_funct_2(X5,u1_struct_0(k7_lattice3(X1)),u1_struct_0(k7_lattice3(X0)))
| l1_orders_2(X0)
| v3_waybel_1(k1_waybel_1(X0,X1,X4,X5),X0,X1) ),
inference(duplicate_literal_removal,[],[f1678]) ).
fof(f1704,plain,
( l1_orders_2(sK0)
| v3_struct_0(sK0) ),
inference(resolution,[],[f1217,f524]) ).
fof(f1705,plain,
( l1_orders_2(sK1)
| v3_struct_0(sK1) ),
inference(resolution,[],[f1217,f517]) ).
fof(f1717,plain,
v3_struct_0(sK1),
inference(forward_subsumption_resolution,[],[f1705,f1164]) ).
fof(f1718,plain,
v3_struct_0(sK0),
inference(forward_subsumption_resolution,[],[f1704,f1161]) ).
fof(f1784,plain,
m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1)),
inference(resolution,[],[f1140,f509]) ).
fof(f2827,plain,
( l1_orders_2(sK1)
| ~ m2_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| l1_orders_2(sK0)
| ~ v1_funct_1(sK2)
| sK2 = k3_waybel34(sK0,sK1,sK2) ),
inference(resolution,[],[f1327,f511]) ).
fof(f2837,plain,
( ~ m2_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| l1_orders_2(sK0)
| ~ v1_funct_1(sK2)
| sK2 = k3_waybel34(sK0,sK1,sK2) ),
inference(forward_subsumption_resolution,[],[f2827,f1164]) ).
fof(f2838,plain,
( l1_orders_2(sK0)
| ~ v1_funct_1(sK2)
| sK2 = k3_waybel34(sK0,sK1,sK2) ),
inference(forward_subsumption_resolution,[],[f2837,f509]) ).
fof(f2839,plain,
( ~ v1_funct_1(sK2)
| sK2 = k3_waybel34(sK0,sK1,sK2) ),
inference(forward_subsumption_resolution,[],[f2838,f1161]) ).
fof(f2840,plain,
sK2 = k3_waybel34(sK0,sK1,sK2),
inference(forward_subsumption_resolution,[],[f2839,f512]) ).
fof(f2843,plain,
k2_waybel34(sK1,sK0,sK2) != k1_waybel34(k7_lattice3(sK0),k7_lattice3(sK1),sK2),
inference(superposition,[],[f513,f2840]) ).
fof(f2846,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))
| ~ v1_funct_1(sK2)
| l1_orders_2(sK1)
| l1_orders_2(sK0)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(superposition,[],[f1338,f2840]) ).
fof(f2847,plain,
( v1_funct_2(sK2,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ v1_funct_1(sK2)
| l1_orders_2(sK1)
| l1_orders_2(sK0)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(forward_subsumption_resolution,[],[f2846,f511]) ).
fof(f2850,plain,
( v1_funct_2(sK2,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| l1_orders_2(sK1)
| l1_orders_2(sK0)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(forward_subsumption_resolution,[],[f2847,f512]) ).
fof(f2853,plain,
( v1_funct_2(sK2,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| l1_orders_2(sK0)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(forward_subsumption_resolution,[],[f2850,f1164]) ).
fof(f2856,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,[],[f2853,f1161]) ).
fof(f2857,plain,
v1_funct_2(sK2,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1))),
inference(forward_subsumption_resolution,[],[f2856,f1784]) ).
fof(f2860,plain,
( m2_relset_1(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))
| ~ v1_funct_1(sK2)
| l1_orders_2(sK1)
| l1_orders_2(sK0)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(superposition,[],[f1339,f2840]) ).
fof(f2861,plain,
( m2_relset_1(sK2,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ v1_funct_1(sK2)
| l1_orders_2(sK1)
| l1_orders_2(sK0)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(forward_subsumption_resolution,[],[f2860,f511]) ).
fof(f2862,plain,
( m2_relset_1(sK2,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| l1_orders_2(sK1)
| l1_orders_2(sK0)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(forward_subsumption_resolution,[],[f2861,f512]) ).
fof(f2863,plain,
( m2_relset_1(sK2,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| l1_orders_2(sK0)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(forward_subsumption_resolution,[],[f2862,f1164]) ).
fof(f2864,plain,
( m2_relset_1(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,[],[f2863,f1161]) ).
fof(f2865,plain,
m2_relset_1(sK2,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1))),
inference(forward_subsumption_resolution,[],[f2864,f1784]) ).
fof(f2886,definition,
( spl40_41
<=> m2_relset_1(sK2,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1))) ),
introduced(definition,[new_symbols(definition,[spl40_41])],[avatar_definition]) ).
fof(f2887,plain,
( m2_relset_1(sK2,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ spl40_41 ),
inference(avatar_component_clause,[],[f2886]) ).
fof(f2890,plain,
spl40_41,
inference(avatar_split_clause,[],[f2865,f2886]) ).
fof(f3108,definition,
( spl40_57
<=> v1_lattice3(k7_lattice3(sK0)) ),
introduced(definition,[new_symbols(definition,[spl40_57])],[avatar_definition]) ).
fof(f3109,plain,
( v1_lattice3(k7_lattice3(sK0))
| ~ spl40_57 ),
inference(avatar_component_clause,[],[f3108]) ).
fof(f3110,plain,
( ~ v1_lattice3(k7_lattice3(sK0))
| spl40_57 ),
inference(avatar_component_clause,[],[f3108]) ).
fof(f3112,definition,
( spl40_58
<=> v2_lattice3(k7_lattice3(sK0)) ),
introduced(definition,[new_symbols(definition,[spl40_58])],[avatar_definition]) ).
fof(f3113,plain,
( v2_lattice3(k7_lattice3(sK0))
| ~ spl40_58 ),
inference(avatar_component_clause,[],[f3112]) ).
fof(f3114,plain,
( ~ v2_lattice3(k7_lattice3(sK0))
| spl40_58 ),
inference(avatar_component_clause,[],[f3112]) ).
fof(f3116,definition,
( spl40_59
<=> v1_lattice3(k7_lattice3(sK1)) ),
introduced(definition,[new_symbols(definition,[spl40_59])],[avatar_definition]) ).
fof(f3117,plain,
( v1_lattice3(k7_lattice3(sK1))
| ~ spl40_59 ),
inference(avatar_component_clause,[],[f3116]) ).
fof(f3118,plain,
( ~ v1_lattice3(k7_lattice3(sK1))
| spl40_59 ),
inference(avatar_component_clause,[],[f3116]) ).
fof(f3120,definition,
( spl40_60
<=> v2_lattice3(k7_lattice3(sK1)) ),
introduced(definition,[new_symbols(definition,[spl40_60])],[avatar_definition]) ).
fof(f3121,plain,
( v2_lattice3(k7_lattice3(sK1))
| ~ spl40_60 ),
inference(avatar_component_clause,[],[f3120]) ).
fof(f3122,plain,
( ~ v2_lattice3(k7_lattice3(sK1))
| spl40_60 ),
inference(avatar_component_clause,[],[f3120]) ).
fof(f3136,plain,
( ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_1(sK2)
| l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| l1_orders_2(sK1)
| ~ v2_lattice3(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| v3_orders_2(sK1)
| v2_orders_2(sK1)
| v1_funct_1(k2_waybel34(sK1,sK0,sK2)) ),
inference(resolution,[],[f1334,f511]) ).
fof(f3151,plain,
( ~ v1_funct_1(sK2)
| l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| l1_orders_2(sK1)
| ~ v2_lattice3(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| v3_orders_2(sK1)
| v2_orders_2(sK1)
| v1_funct_1(k2_waybel34(sK1,sK0,sK2)) ),
inference(forward_subsumption_resolution,[],[f3136,f1784]) ).
fof(f3158,plain,
( l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| l1_orders_2(sK1)
| ~ v2_lattice3(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| v3_orders_2(sK1)
| v2_orders_2(sK1)
| v1_funct_1(k2_waybel34(sK1,sK0,sK2)) ),
inference(forward_subsumption_resolution,[],[f3151,f512]) ).
fof(f3164,plain,
( ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| l1_orders_2(sK1)
| ~ v2_lattice3(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| v3_orders_2(sK1)
| v2_orders_2(sK1)
| v1_funct_1(k2_waybel34(sK1,sK0,sK2)) ),
inference(forward_subsumption_resolution,[],[f3158,f1161]) ).
fof(f3173,plain,
( ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| l1_orders_2(sK1)
| ~ v2_lattice3(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| v3_orders_2(sK1)
| v2_orders_2(sK1)
| v1_funct_1(k2_waybel34(sK1,sK0,sK2)) ),
inference(forward_subsumption_resolution,[],[f3164,f523]) ).
fof(f3174,plain,
( ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| l1_orders_2(sK1)
| ~ v2_lattice3(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| v3_orders_2(sK1)
| v2_orders_2(sK1)
| v1_funct_1(k2_waybel34(sK1,sK0,sK2)) ),
inference(forward_subsumption_resolution,[],[f3173,f524]) ).
fof(f3175,plain,
( v3_orders_2(sK0)
| v2_orders_2(sK0)
| l1_orders_2(sK1)
| ~ v2_lattice3(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| v3_orders_2(sK1)
| v2_orders_2(sK1)
| v1_funct_1(k2_waybel34(sK1,sK0,sK2)) ),
inference(forward_subsumption_resolution,[],[f3174,f525]) ).
fof(f3176,plain,
( v2_orders_2(sK0)
| l1_orders_2(sK1)
| ~ v2_lattice3(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| v3_orders_2(sK1)
| v2_orders_2(sK1)
| v1_funct_1(k2_waybel34(sK1,sK0,sK2)) ),
inference(forward_subsumption_resolution,[],[f3175,f1160]) ).
fof(f3177,plain,
( l1_orders_2(sK1)
| ~ v2_lattice3(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| v3_orders_2(sK1)
| v2_orders_2(sK1)
| v1_funct_1(k2_waybel34(sK1,sK0,sK2)) ),
inference(forward_subsumption_resolution,[],[f3176,f1159]) ).
fof(f3178,plain,
( ~ v2_lattice3(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| v3_orders_2(sK1)
| v2_orders_2(sK1)
| v1_funct_1(k2_waybel34(sK1,sK0,sK2)) ),
inference(forward_subsumption_resolution,[],[f3177,f1164]) ).
fof(f3179,plain,
( ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| v3_orders_2(sK1)
| v2_orders_2(sK1)
| v1_funct_1(k2_waybel34(sK1,sK0,sK2)) ),
inference(forward_subsumption_resolution,[],[f3178,f516]) ).
fof(f3180,plain,
( ~ v4_orders_2(sK1)
| v3_orders_2(sK1)
| v2_orders_2(sK1)
| v1_funct_1(k2_waybel34(sK1,sK0,sK2)) ),
inference(forward_subsumption_resolution,[],[f3179,f517]) ).
fof(f3181,plain,
( v3_orders_2(sK1)
| v2_orders_2(sK1)
| v1_funct_1(k2_waybel34(sK1,sK0,sK2)) ),
inference(forward_subsumption_resolution,[],[f3180,f518]) ).
fof(f3182,plain,
( v2_orders_2(sK1)
| v1_funct_1(k2_waybel34(sK1,sK0,sK2)) ),
inference(forward_subsumption_resolution,[],[f3181,f1163]) ).
fof(f3183,plain,
v1_funct_1(k2_waybel34(sK1,sK0,sK2)),
inference(forward_subsumption_resolution,[],[f3182,f1162]) ).
fof(f3271,plain,
( ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_1(sK2)
| l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| l1_orders_2(sK1)
| ~ v2_lattice3(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| v3_orders_2(sK1)
| v2_orders_2(sK1)
| v1_funct_2(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0)) ),
inference(resolution,[],[f1335,f511]) ).
fof(f3286,plain,
( ~ v1_funct_1(sK2)
| l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| l1_orders_2(sK1)
| ~ v2_lattice3(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| v3_orders_2(sK1)
| v2_orders_2(sK1)
| v1_funct_2(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0)) ),
inference(forward_subsumption_resolution,[],[f3271,f1784]) ).
fof(f3293,plain,
( l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| l1_orders_2(sK1)
| ~ v2_lattice3(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| v3_orders_2(sK1)
| v2_orders_2(sK1)
| v1_funct_2(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0)) ),
inference(forward_subsumption_resolution,[],[f3286,f512]) ).
fof(f3299,plain,
( ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| l1_orders_2(sK1)
| ~ v2_lattice3(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| v3_orders_2(sK1)
| v2_orders_2(sK1)
| v1_funct_2(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0)) ),
inference(forward_subsumption_resolution,[],[f3293,f1161]) ).
fof(f3308,plain,
( ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| l1_orders_2(sK1)
| ~ v2_lattice3(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| v3_orders_2(sK1)
| v2_orders_2(sK1)
| v1_funct_2(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0)) ),
inference(forward_subsumption_resolution,[],[f3299,f523]) ).
fof(f3309,plain,
( ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| l1_orders_2(sK1)
| ~ v2_lattice3(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| v3_orders_2(sK1)
| v2_orders_2(sK1)
| v1_funct_2(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0)) ),
inference(forward_subsumption_resolution,[],[f3308,f524]) ).
fof(f3310,plain,
( v3_orders_2(sK0)
| v2_orders_2(sK0)
| l1_orders_2(sK1)
| ~ v2_lattice3(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| v3_orders_2(sK1)
| v2_orders_2(sK1)
| v1_funct_2(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0)) ),
inference(forward_subsumption_resolution,[],[f3309,f525]) ).
fof(f3311,plain,
( v2_orders_2(sK0)
| l1_orders_2(sK1)
| ~ v2_lattice3(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| v3_orders_2(sK1)
| v2_orders_2(sK1)
| v1_funct_2(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0)) ),
inference(forward_subsumption_resolution,[],[f3310,f1160]) ).
fof(f3312,plain,
( l1_orders_2(sK1)
| ~ v2_lattice3(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| v3_orders_2(sK1)
| v2_orders_2(sK1)
| v1_funct_2(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0)) ),
inference(forward_subsumption_resolution,[],[f3311,f1159]) ).
fof(f3313,plain,
( ~ v2_lattice3(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| v3_orders_2(sK1)
| v2_orders_2(sK1)
| v1_funct_2(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0)) ),
inference(forward_subsumption_resolution,[],[f3312,f1164]) ).
fof(f3314,plain,
( ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| v3_orders_2(sK1)
| v2_orders_2(sK1)
| v1_funct_2(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0)) ),
inference(forward_subsumption_resolution,[],[f3313,f516]) ).
fof(f3315,plain,
( ~ v4_orders_2(sK1)
| v3_orders_2(sK1)
| v2_orders_2(sK1)
| v1_funct_2(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0)) ),
inference(forward_subsumption_resolution,[],[f3314,f517]) ).
fof(f3316,plain,
( v3_orders_2(sK1)
| v2_orders_2(sK1)
| v1_funct_2(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0)) ),
inference(forward_subsumption_resolution,[],[f3315,f518]) ).
fof(f3317,plain,
( v2_orders_2(sK1)
| v1_funct_2(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0)) ),
inference(forward_subsumption_resolution,[],[f3316,f1163]) ).
fof(f3318,plain,
v1_funct_2(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0)),
inference(forward_subsumption_resolution,[],[f3317,f1162]) ).
fof(f3320,plain,
! [X2,X0,X1] :
( m1_relset_1(k2_waybel34(X2,X1,X0),u1_struct_0(X2),u1_struct_0(X1))
| ~ v1_funct_1(X0)
| l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| v3_orders_2(X1)
| v2_orders_2(X1)
| l1_orders_2(X2)
| ~ v2_lattice3(X2)
| ~ v1_lattice3(X2)
| ~ v4_orders_2(X2)
| v3_orders_2(X2)
| v2_orders_2(X2)
| ~ m1_relset_1(X0,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(X2)) ),
inference(resolution,[],[f1336,f1140]) ).
fof(f3414,definition,
( spl40_66
<=> v3_lattice3(k7_lattice3(sK1)) ),
introduced(definition,[new_symbols(definition,[spl40_66])],[avatar_definition]) ).
fof(f3415,plain,
( v3_lattice3(k7_lattice3(sK1))
| ~ spl40_66 ),
inference(avatar_component_clause,[],[f3414]) ).
fof(f3416,plain,
( ~ v3_lattice3(k7_lattice3(sK1))
| spl40_66 ),
inference(avatar_component_clause,[],[f3414]) ).
fof(f3418,definition,
( spl40_67
<=> v3_lattice3(k7_lattice3(sK0)) ),
introduced(definition,[new_symbols(definition,[spl40_67])],[avatar_definition]) ).
fof(f3419,plain,
( v3_lattice3(k7_lattice3(sK0))
| ~ spl40_67 ),
inference(avatar_component_clause,[],[f3418]) ).
fof(f3420,plain,
( ~ v3_lattice3(k7_lattice3(sK0))
| spl40_67 ),
inference(avatar_component_clause,[],[f3418]) ).
fof(f3581,definition,
( spl40_71
<=> v17_waybel_0(sK2,k7_lattice3(sK0),k7_lattice3(sK1)) ),
introduced(definition,[new_symbols(definition,[spl40_71])],[avatar_definition]) ).
fof(f3582,plain,
( v17_waybel_0(sK2,k7_lattice3(sK0),k7_lattice3(sK1))
| ~ spl40_71 ),
inference(avatar_component_clause,[],[f3581]) ).
fof(f3654,plain,
( v17_waybel_0(sK2,k7_lattice3(sK0),k7_lattice3(sK1))
| v18_waybel_0(sK2,sK0,sK1)
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_1(sK2)
| l1_orders_2(sK1)
| ~ v3_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| v3_orders_2(sK1)
| v2_orders_2(sK1)
| l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(superposition,[],[f1460,f2840]) ).
fof(f3657,plain,
( v17_waybel_0(sK2,k7_lattice3(sK0),k7_lattice3(sK1))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_1(sK2)
| l1_orders_2(sK1)
| ~ v3_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| v3_orders_2(sK1)
| v2_orders_2(sK1)
| l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(forward_subsumption_resolution,[],[f3654,f1165]) ).
fof(f3664,plain,
( v17_waybel_0(sK2,k7_lattice3(sK0),k7_lattice3(sK1))
| ~ v1_funct_1(sK2)
| l1_orders_2(sK1)
| ~ v3_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| v3_orders_2(sK1)
| v2_orders_2(sK1)
| l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(forward_subsumption_resolution,[],[f3657,f511]) ).
fof(f3671,plain,
( v17_waybel_0(sK2,k7_lattice3(sK0),k7_lattice3(sK1))
| l1_orders_2(sK1)
| ~ v3_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| v3_orders_2(sK1)
| v2_orders_2(sK1)
| l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(forward_subsumption_resolution,[],[f3664,f512]) ).
fof(f3678,plain,
( v17_waybel_0(sK2,k7_lattice3(sK0),k7_lattice3(sK1))
| ~ v3_lattice3(sK1)
| ~ v2_lattice3(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| v3_orders_2(sK1)
| v2_orders_2(sK1)
| l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(forward_subsumption_resolution,[],[f3671,f1164]) ).
fof(f3689,plain,
( v17_waybel_0(sK2,k7_lattice3(sK0),k7_lattice3(sK1))
| ~ v2_lattice3(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| v3_orders_2(sK1)
| v2_orders_2(sK1)
| l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(forward_subsumption_resolution,[],[f3678,f515]) ).
fof(f3695,plain,
( v17_waybel_0(sK2,k7_lattice3(sK0),k7_lattice3(sK1))
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| v3_orders_2(sK1)
| v2_orders_2(sK1)
| l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(forward_subsumption_resolution,[],[f3689,f516]) ).
fof(f3701,plain,
( v17_waybel_0(sK2,k7_lattice3(sK0),k7_lattice3(sK1))
| ~ v4_orders_2(sK1)
| v3_orders_2(sK1)
| v2_orders_2(sK1)
| l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(forward_subsumption_resolution,[],[f3695,f517]) ).
fof(f3706,plain,
( v17_waybel_0(sK2,k7_lattice3(sK0),k7_lattice3(sK1))
| v3_orders_2(sK1)
| v2_orders_2(sK1)
| l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(forward_subsumption_resolution,[],[f3701,f518]) ).
fof(f3711,plain,
( v17_waybel_0(sK2,k7_lattice3(sK0),k7_lattice3(sK1))
| v2_orders_2(sK1)
| l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(forward_subsumption_resolution,[],[f3706,f1163]) ).
fof(f3716,plain,
( v17_waybel_0(sK2,k7_lattice3(sK0),k7_lattice3(sK1))
| l1_orders_2(sK0)
| ~ v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(forward_subsumption_resolution,[],[f3711,f1162]) ).
fof(f3721,plain,
( v17_waybel_0(sK2,k7_lattice3(sK0),k7_lattice3(sK1))
| ~ v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(forward_subsumption_resolution,[],[f3716,f1161]) ).
fof(f3726,plain,
( v17_waybel_0(sK2,k7_lattice3(sK0),k7_lattice3(sK1))
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(forward_subsumption_resolution,[],[f3721,f522]) ).
fof(f3731,plain,
( v17_waybel_0(sK2,k7_lattice3(sK0),k7_lattice3(sK1))
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(forward_subsumption_resolution,[],[f3726,f523]) ).
fof(f3736,plain,
( v17_waybel_0(sK2,k7_lattice3(sK0),k7_lattice3(sK1))
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(forward_subsumption_resolution,[],[f3731,f524]) ).
fof(f3741,plain,
( v17_waybel_0(sK2,k7_lattice3(sK0),k7_lattice3(sK1))
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(forward_subsumption_resolution,[],[f3736,f525]) ).
fof(f3742,plain,
( v17_waybel_0(sK2,k7_lattice3(sK0),k7_lattice3(sK1))
| v2_orders_2(sK0)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(forward_subsumption_resolution,[],[f3741,f1160]) ).
fof(f3743,plain,
( v17_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,[],[f3742,f1159]) ).
fof(f3744,plain,
v17_waybel_0(sK2,k7_lattice3(sK0),k7_lattice3(sK1)),
inference(forward_subsumption_resolution,[],[f3743,f1784]) ).
fof(f3745,plain,
spl40_71,
inference(avatar_split_clause,[],[f3744,f3581]) ).
fof(f3829,plain,
! [X2,X3,X0,X1] :
( ~ v4_orders_2(X0)
| v3_orders_2(X0)
| v2_orders_2(X0)
| ~ v3_struct_0(X0)
| l1_orders_2(X1)
| ~ v4_orders_2(X1)
| v3_orders_2(X1)
| v2_orders_2(X1)
| ~ v3_struct_0(X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X3)
| ~ m2_relset_1(X2,u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
| ~ v1_funct_2(X2,u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
| ~ m2_relset_1(X3,u1_struct_0(k7_lattice3(X1)),u1_struct_0(k7_lattice3(X0)))
| ~ v1_funct_2(X3,u1_struct_0(k7_lattice3(X1)),u1_struct_0(k7_lattice3(X0)))
| l1_orders_2(X0)
| v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1)
| ~ v2_lattice3(k7_lattice3(X1))
| ~ v1_lattice3(k7_lattice3(X1))
| ~ v4_orders_2(k7_lattice3(X1))
| v3_orders_2(k7_lattice3(X1))
| v2_orders_2(k7_lattice3(X1))
| l1_orders_2(k7_lattice3(X0))
| ~ v2_lattice3(k7_lattice3(X0))
| ~ v1_lattice3(k7_lattice3(X0))
| ~ v4_orders_2(k7_lattice3(X0))
| v3_orders_2(k7_lattice3(X0))
| v2_orders_2(k7_lattice3(X0))
| ~ m2_relset_1(X3,u1_struct_0(k7_lattice3(X1)),u1_struct_0(k7_lattice3(X0)))
| ~ v1_funct_2(X3,u1_struct_0(k7_lattice3(X1)),u1_struct_0(k7_lattice3(X0)))
| ~ v1_funct_1(X3)
| ~ v17_waybel_0(X3,k7_lattice3(X1),k7_lattice3(X0))
| ~ v3_lattice3(k7_lattice3(X0))
| ~ v3_lattice3(k7_lattice3(X1))
| ~ m2_relset_1(X2,u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
| ~ v1_funct_2(X2,u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
| ~ v1_funct_1(X2)
| l1_orders_2(k7_lattice3(X1))
| k1_waybel34(k7_lattice3(X1),k7_lattice3(X0),X3) = X2 ),
inference(resolution,[],[f1686,f1324]) ).
fof(f3830,plain,
! [X2,X3,X0,X1] :
( ~ v4_orders_2(X0)
| v3_orders_2(X0)
| v2_orders_2(X0)
| ~ v3_struct_0(X0)
| l1_orders_2(X1)
| ~ v4_orders_2(X1)
| v3_orders_2(X1)
| v2_orders_2(X1)
| ~ v3_struct_0(X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X3)
| ~ m2_relset_1(X2,u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
| ~ v1_funct_2(X2,u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
| ~ m2_relset_1(X3,u1_struct_0(k7_lattice3(X1)),u1_struct_0(k7_lattice3(X0)))
| ~ v1_funct_2(X3,u1_struct_0(k7_lattice3(X1)),u1_struct_0(k7_lattice3(X0)))
| l1_orders_2(X0)
| v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1)
| ~ v2_lattice3(k7_lattice3(X1))
| ~ v1_lattice3(k7_lattice3(X1))
| ~ v4_orders_2(k7_lattice3(X1))
| v3_orders_2(k7_lattice3(X1))
| v2_orders_2(k7_lattice3(X1))
| l1_orders_2(k7_lattice3(X0))
| ~ v2_lattice3(k7_lattice3(X0))
| ~ v1_lattice3(k7_lattice3(X0))
| ~ v4_orders_2(k7_lattice3(X0))
| v3_orders_2(k7_lattice3(X0))
| v2_orders_2(k7_lattice3(X0))
| ~ v17_waybel_0(X3,k7_lattice3(X1),k7_lattice3(X0))
| ~ v3_lattice3(k7_lattice3(X0))
| ~ v3_lattice3(k7_lattice3(X1))
| l1_orders_2(k7_lattice3(X1))
| k1_waybel34(k7_lattice3(X1),k7_lattice3(X0),X3) = X2 ),
inference(duplicate_literal_removal,[],[f3829]) ).
fof(f3833,plain,
! [X2,X3,X0,X1] :
( ~ v4_orders_2(X0)
| v3_orders_2(X0)
| v2_orders_2(X0)
| ~ v3_struct_0(X0)
| l1_orders_2(X1)
| ~ v4_orders_2(X1)
| v3_orders_2(X1)
| v2_orders_2(X1)
| ~ v3_struct_0(X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X3)
| ~ m2_relset_1(X2,u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
| ~ v1_funct_2(X2,u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
| ~ m2_relset_1(X3,u1_struct_0(k7_lattice3(X1)),u1_struct_0(k7_lattice3(X0)))
| ~ v1_funct_2(X3,u1_struct_0(k7_lattice3(X1)),u1_struct_0(k7_lattice3(X0)))
| l1_orders_2(X0)
| v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1)
| ~ v2_lattice3(k7_lattice3(X1))
| ~ v1_lattice3(k7_lattice3(X1))
| v3_orders_2(k7_lattice3(X1))
| v2_orders_2(k7_lattice3(X1))
| l1_orders_2(k7_lattice3(X0))
| ~ v2_lattice3(k7_lattice3(X0))
| ~ v1_lattice3(k7_lattice3(X0))
| ~ v4_orders_2(k7_lattice3(X0))
| v3_orders_2(k7_lattice3(X0))
| v2_orders_2(k7_lattice3(X0))
| ~ v17_waybel_0(X3,k7_lattice3(X1),k7_lattice3(X0))
| ~ v3_lattice3(k7_lattice3(X0))
| ~ v3_lattice3(k7_lattice3(X1))
| l1_orders_2(k7_lattice3(X1))
| k1_waybel34(k7_lattice3(X1),k7_lattice3(X0),X3) = X2 ),
inference(forward_subsumption_resolution,[],[f3830,f1455]) ).
fof(f3835,plain,
! [X2,X3,X0,X1] :
( ~ v4_orders_2(X0)
| v3_orders_2(X0)
| v2_orders_2(X0)
| ~ v3_struct_0(X0)
| l1_orders_2(X1)
| ~ v4_orders_2(X1)
| v3_orders_2(X1)
| v2_orders_2(X1)
| ~ v3_struct_0(X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X3)
| ~ m2_relset_1(X2,u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
| ~ v1_funct_2(X2,u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
| ~ m2_relset_1(X3,u1_struct_0(k7_lattice3(X1)),u1_struct_0(k7_lattice3(X0)))
| ~ v1_funct_2(X3,u1_struct_0(k7_lattice3(X1)),u1_struct_0(k7_lattice3(X0)))
| l1_orders_2(X0)
| v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1)
| ~ v2_lattice3(k7_lattice3(X1))
| ~ v1_lattice3(k7_lattice3(X1))
| v2_orders_2(k7_lattice3(X1))
| l1_orders_2(k7_lattice3(X0))
| ~ v2_lattice3(k7_lattice3(X0))
| ~ v1_lattice3(k7_lattice3(X0))
| ~ v4_orders_2(k7_lattice3(X0))
| v3_orders_2(k7_lattice3(X0))
| v2_orders_2(k7_lattice3(X0))
| ~ v17_waybel_0(X3,k7_lattice3(X1),k7_lattice3(X0))
| ~ v3_lattice3(k7_lattice3(X0))
| ~ v3_lattice3(k7_lattice3(X1))
| l1_orders_2(k7_lattice3(X1))
| k1_waybel34(k7_lattice3(X1),k7_lattice3(X0),X3) = X2 ),
inference(forward_subsumption_resolution,[],[f3833,f1442]) ).
fof(f3837,plain,
! [X2,X3,X0,X1] :
( ~ v4_orders_2(X0)
| v3_orders_2(X0)
| v2_orders_2(X0)
| ~ v3_struct_0(X0)
| l1_orders_2(X1)
| ~ v4_orders_2(X1)
| v3_orders_2(X1)
| v2_orders_2(X1)
| ~ v3_struct_0(X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X3)
| ~ m2_relset_1(X2,u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
| ~ v1_funct_2(X2,u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
| ~ m2_relset_1(X3,u1_struct_0(k7_lattice3(X1)),u1_struct_0(k7_lattice3(X0)))
| ~ v1_funct_2(X3,u1_struct_0(k7_lattice3(X1)),u1_struct_0(k7_lattice3(X0)))
| l1_orders_2(X0)
| v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1)
| ~ v2_lattice3(k7_lattice3(X1))
| ~ v1_lattice3(k7_lattice3(X1))
| l1_orders_2(k7_lattice3(X0))
| ~ v2_lattice3(k7_lattice3(X0))
| ~ v1_lattice3(k7_lattice3(X0))
| ~ v4_orders_2(k7_lattice3(X0))
| v3_orders_2(k7_lattice3(X0))
| v2_orders_2(k7_lattice3(X0))
| ~ v17_waybel_0(X3,k7_lattice3(X1),k7_lattice3(X0))
| ~ v3_lattice3(k7_lattice3(X0))
| ~ v3_lattice3(k7_lattice3(X1))
| l1_orders_2(k7_lattice3(X1))
| k1_waybel34(k7_lattice3(X1),k7_lattice3(X0),X3) = X2 ),
inference(forward_subsumption_resolution,[],[f3835,f1423]) ).
fof(f3839,plain,
! [X2,X3,X0,X1] :
( ~ v4_orders_2(X0)
| v3_orders_2(X0)
| v2_orders_2(X0)
| ~ v3_struct_0(X0)
| l1_orders_2(X1)
| ~ v4_orders_2(X1)
| v3_orders_2(X1)
| v2_orders_2(X1)
| ~ v3_struct_0(X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X3)
| ~ m2_relset_1(X2,u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
| ~ v1_funct_2(X2,u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
| ~ m2_relset_1(X3,u1_struct_0(k7_lattice3(X1)),u1_struct_0(k7_lattice3(X0)))
| ~ v1_funct_2(X3,u1_struct_0(k7_lattice3(X1)),u1_struct_0(k7_lattice3(X0)))
| l1_orders_2(X0)
| v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1)
| ~ v2_lattice3(k7_lattice3(X1))
| ~ v1_lattice3(k7_lattice3(X1))
| ~ v2_lattice3(k7_lattice3(X0))
| ~ v1_lattice3(k7_lattice3(X0))
| ~ v4_orders_2(k7_lattice3(X0))
| v3_orders_2(k7_lattice3(X0))
| v2_orders_2(k7_lattice3(X0))
| ~ v17_waybel_0(X3,k7_lattice3(X1),k7_lattice3(X0))
| ~ v3_lattice3(k7_lattice3(X0))
| ~ v3_lattice3(k7_lattice3(X1))
| l1_orders_2(k7_lattice3(X1))
| k1_waybel34(k7_lattice3(X1),k7_lattice3(X0),X3) = X2 ),
inference(forward_subsumption_resolution,[],[f3837,f1342]) ).
fof(f3841,plain,
! [X2,X3,X0,X1] :
( ~ v4_orders_2(X0)
| v3_orders_2(X0)
| v2_orders_2(X0)
| ~ v3_struct_0(X0)
| l1_orders_2(X1)
| ~ v4_orders_2(X1)
| v3_orders_2(X1)
| v2_orders_2(X1)
| ~ v3_struct_0(X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X3)
| ~ m2_relset_1(X2,u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
| ~ v1_funct_2(X2,u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
| ~ m2_relset_1(X3,u1_struct_0(k7_lattice3(X1)),u1_struct_0(k7_lattice3(X0)))
| ~ v1_funct_2(X3,u1_struct_0(k7_lattice3(X1)),u1_struct_0(k7_lattice3(X0)))
| l1_orders_2(X0)
| v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1)
| ~ v2_lattice3(k7_lattice3(X1))
| ~ v1_lattice3(k7_lattice3(X1))
| ~ v2_lattice3(k7_lattice3(X0))
| ~ v1_lattice3(k7_lattice3(X0))
| v3_orders_2(k7_lattice3(X0))
| v2_orders_2(k7_lattice3(X0))
| ~ v17_waybel_0(X3,k7_lattice3(X1),k7_lattice3(X0))
| ~ v3_lattice3(k7_lattice3(X0))
| ~ v3_lattice3(k7_lattice3(X1))
| l1_orders_2(k7_lattice3(X1))
| k1_waybel34(k7_lattice3(X1),k7_lattice3(X0),X3) = X2 ),
inference(forward_subsumption_resolution,[],[f3839,f1455]) ).
fof(f3843,plain,
! [X2,X3,X0,X1] :
( ~ v4_orders_2(X0)
| v3_orders_2(X0)
| v2_orders_2(X0)
| ~ v3_struct_0(X0)
| l1_orders_2(X1)
| ~ v4_orders_2(X1)
| v3_orders_2(X1)
| v2_orders_2(X1)
| ~ v3_struct_0(X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X3)
| ~ m2_relset_1(X2,u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
| ~ v1_funct_2(X2,u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
| ~ m2_relset_1(X3,u1_struct_0(k7_lattice3(X1)),u1_struct_0(k7_lattice3(X0)))
| ~ v1_funct_2(X3,u1_struct_0(k7_lattice3(X1)),u1_struct_0(k7_lattice3(X0)))
| l1_orders_2(X0)
| v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1)
| ~ v2_lattice3(k7_lattice3(X1))
| ~ v1_lattice3(k7_lattice3(X1))
| ~ v2_lattice3(k7_lattice3(X0))
| ~ v1_lattice3(k7_lattice3(X0))
| v2_orders_2(k7_lattice3(X0))
| ~ v17_waybel_0(X3,k7_lattice3(X1),k7_lattice3(X0))
| ~ v3_lattice3(k7_lattice3(X0))
| ~ v3_lattice3(k7_lattice3(X1))
| l1_orders_2(k7_lattice3(X1))
| k1_waybel34(k7_lattice3(X1),k7_lattice3(X0),X3) = X2 ),
inference(forward_subsumption_resolution,[],[f3841,f1442]) ).
fof(f3845,plain,
! [X2,X3,X0,X1] :
( ~ v4_orders_2(X0)
| v3_orders_2(X0)
| v2_orders_2(X0)
| ~ v3_struct_0(X0)
| l1_orders_2(X1)
| ~ v4_orders_2(X1)
| v3_orders_2(X1)
| v2_orders_2(X1)
| ~ v3_struct_0(X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X3)
| ~ m2_relset_1(X2,u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
| ~ v1_funct_2(X2,u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
| ~ m2_relset_1(X3,u1_struct_0(k7_lattice3(X1)),u1_struct_0(k7_lattice3(X0)))
| ~ v1_funct_2(X3,u1_struct_0(k7_lattice3(X1)),u1_struct_0(k7_lattice3(X0)))
| l1_orders_2(X0)
| v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1)
| ~ v2_lattice3(k7_lattice3(X1))
| ~ v1_lattice3(k7_lattice3(X1))
| ~ v2_lattice3(k7_lattice3(X0))
| ~ v1_lattice3(k7_lattice3(X0))
| ~ v17_waybel_0(X3,k7_lattice3(X1),k7_lattice3(X0))
| ~ v3_lattice3(k7_lattice3(X0))
| ~ v3_lattice3(k7_lattice3(X1))
| l1_orders_2(k7_lattice3(X1))
| k1_waybel34(k7_lattice3(X1),k7_lattice3(X0),X3) = X2 ),
inference(forward_subsumption_resolution,[],[f3843,f1423]) ).
fof(f3847,plain,
! [X2,X3,X0,X1] :
( v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1)
| v3_orders_2(X0)
| v2_orders_2(X0)
| ~ v3_struct_0(X0)
| l1_orders_2(X1)
| ~ v4_orders_2(X1)
| v3_orders_2(X1)
| v2_orders_2(X1)
| ~ v3_struct_0(X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X3)
| ~ m2_relset_1(X2,u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
| ~ v1_funct_2(X2,u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
| ~ m2_relset_1(X3,u1_struct_0(k7_lattice3(X1)),u1_struct_0(k7_lattice3(X0)))
| ~ v1_funct_2(X3,u1_struct_0(k7_lattice3(X1)),u1_struct_0(k7_lattice3(X0)))
| l1_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v2_lattice3(k7_lattice3(X1))
| ~ v1_lattice3(k7_lattice3(X1))
| ~ v2_lattice3(k7_lattice3(X0))
| ~ v1_lattice3(k7_lattice3(X0))
| ~ v17_waybel_0(X3,k7_lattice3(X1),k7_lattice3(X0))
| ~ v3_lattice3(k7_lattice3(X0))
| ~ v3_lattice3(k7_lattice3(X1))
| k1_waybel34(k7_lattice3(X1),k7_lattice3(X0),X3) = X2 ),
inference(forward_subsumption_resolution,[],[f3845,f1342]) ).
fof(f4075,plain,
( l1_orders_2(sK0)
| ~ m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| l1_orders_2(sK1)
| ~ v1_funct_1(k2_waybel34(sK1,sK0,sK2))
| k2_waybel34(sK1,sK0,sK2) = k3_waybel34(sK1,sK0,k2_waybel34(sK1,sK0,sK2)) ),
inference(resolution,[],[f3318,f1327]) ).
fof(f4085,plain,
( ~ v2_lattice3(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| v3_orders_2(sK1)
| v2_orders_2(sK1)
| l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m2_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_1(sK2)
| v18_waybel_0(sK2,sK0,sK1)
| ~ v3_lattice3(sK0)
| ~ v3_lattice3(sK1)
| ~ m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| l1_orders_2(sK1)
| ~ v1_funct_1(k2_waybel34(sK1,sK0,sK2))
| ~ v3_waybel_1(k1_waybel_1(sK1,sK0,k2_waybel34(sK1,sK0,sK2),sK2),sK1,sK0) ),
inference(resolution,[],[f3318,f1325]) ).
fof(f4086,plain,
( ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| v3_orders_2(sK1)
| v2_orders_2(sK1)
| l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m2_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_1(sK2)
| v18_waybel_0(sK2,sK0,sK1)
| ~ v3_lattice3(sK0)
| ~ v3_lattice3(sK1)
| ~ m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| l1_orders_2(sK1)
| ~ v1_funct_1(k2_waybel34(sK1,sK0,sK2))
| ~ v3_waybel_1(k1_waybel_1(sK1,sK0,k2_waybel34(sK1,sK0,sK2),sK2),sK1,sK0) ),
inference(forward_subsumption_resolution,[],[f4085,f516]) ).
fof(f4095,plain,
( ~ m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| l1_orders_2(sK1)
| ~ v1_funct_1(k2_waybel34(sK1,sK0,sK2))
| k2_waybel34(sK1,sK0,sK2) = k3_waybel34(sK1,sK0,k2_waybel34(sK1,sK0,sK2)) ),
inference(forward_subsumption_resolution,[],[f4075,f1161]) ).
fof(f4098,plain,
( ~ v4_orders_2(sK1)
| v3_orders_2(sK1)
| v2_orders_2(sK1)
| l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m2_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_1(sK2)
| v18_waybel_0(sK2,sK0,sK1)
| ~ v3_lattice3(sK0)
| ~ v3_lattice3(sK1)
| ~ m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| l1_orders_2(sK1)
| ~ v1_funct_1(k2_waybel34(sK1,sK0,sK2))
| ~ v3_waybel_1(k1_waybel_1(sK1,sK0,k2_waybel34(sK1,sK0,sK2),sK2),sK1,sK0) ),
inference(forward_subsumption_resolution,[],[f4086,f517]) ).
fof(f4107,plain,
( ~ m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v1_funct_1(k2_waybel34(sK1,sK0,sK2))
| k2_waybel34(sK1,sK0,sK2) = k3_waybel34(sK1,sK0,k2_waybel34(sK1,sK0,sK2)) ),
inference(forward_subsumption_resolution,[],[f4095,f1164]) ).
fof(f4110,plain,
( v3_orders_2(sK1)
| v2_orders_2(sK1)
| l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m2_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_1(sK2)
| v18_waybel_0(sK2,sK0,sK1)
| ~ v3_lattice3(sK0)
| ~ v3_lattice3(sK1)
| ~ m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| l1_orders_2(sK1)
| ~ v1_funct_1(k2_waybel34(sK1,sK0,sK2))
| ~ v3_waybel_1(k1_waybel_1(sK1,sK0,k2_waybel34(sK1,sK0,sK2),sK2),sK1,sK0) ),
inference(forward_subsumption_resolution,[],[f4098,f518]) ).
fof(f4119,plain,
( ~ m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| k2_waybel34(sK1,sK0,sK2) = k3_waybel34(sK1,sK0,k2_waybel34(sK1,sK0,sK2)) ),
inference(forward_subsumption_resolution,[],[f4107,f3183]) ).
fof(f4122,plain,
( v2_orders_2(sK1)
| l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m2_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_1(sK2)
| v18_waybel_0(sK2,sK0,sK1)
| ~ v3_lattice3(sK0)
| ~ v3_lattice3(sK1)
| ~ m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| l1_orders_2(sK1)
| ~ v1_funct_1(k2_waybel34(sK1,sK0,sK2))
| ~ v3_waybel_1(k1_waybel_1(sK1,sK0,k2_waybel34(sK1,sK0,sK2),sK2),sK1,sK0) ),
inference(forward_subsumption_resolution,[],[f4110,f1163]) ).
fof(f4124,definition,
( spl40_94
<=> m1_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0)) ),
introduced(definition,[new_symbols(definition,[spl40_94])],[avatar_definition]) ).
fof(f4125,plain,
( m1_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ spl40_94 ),
inference(avatar_component_clause,[],[f4124]) ).
fof(f4126,plain,
( ~ m1_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| spl40_94 ),
inference(avatar_component_clause,[],[f4124]) ).
fof(f4143,definition,
( spl40_97
<=> k2_waybel34(sK1,sK0,sK2) = k3_waybel34(sK1,sK0,k2_waybel34(sK1,sK0,sK2)) ),
introduced(definition,[new_symbols(definition,[spl40_97])],[avatar_definition]) ).
fof(f4145,plain,
( k2_waybel34(sK1,sK0,sK2) = k3_waybel34(sK1,sK0,k2_waybel34(sK1,sK0,sK2))
| ~ spl40_97 ),
inference(avatar_component_clause,[],[f4143]) ).
fof(f4147,definition,
( spl40_98
<=> m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0)) ),
introduced(definition,[new_symbols(definition,[spl40_98])],[avatar_definition]) ).
fof(f4148,plain,
( m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ spl40_98 ),
inference(avatar_component_clause,[],[f4147]) ).
fof(f4149,plain,
( ~ m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| spl40_98 ),
inference(avatar_component_clause,[],[f4147]) ).
fof(f4150,plain,
( spl40_97
| ~ spl40_98 ),
inference(avatar_split_clause,[],[f4119,f4147,f4143]) ).
fof(f4153,plain,
( l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m2_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_1(sK2)
| v18_waybel_0(sK2,sK0,sK1)
| ~ v3_lattice3(sK0)
| ~ v3_lattice3(sK1)
| ~ m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| l1_orders_2(sK1)
| ~ v1_funct_1(k2_waybel34(sK1,sK0,sK2))
| ~ v3_waybel_1(k1_waybel_1(sK1,sK0,k2_waybel34(sK1,sK0,sK2),sK2),sK1,sK0) ),
inference(forward_subsumption_resolution,[],[f4122,f1162]) ).
fof(f4162,plain,
( ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m2_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_1(sK2)
| v18_waybel_0(sK2,sK0,sK1)
| ~ v3_lattice3(sK0)
| ~ v3_lattice3(sK1)
| ~ m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| l1_orders_2(sK1)
| ~ v1_funct_1(k2_waybel34(sK1,sK0,sK2))
| ~ v3_waybel_1(k1_waybel_1(sK1,sK0,k2_waybel34(sK1,sK0,sK2),sK2),sK1,sK0) ),
inference(forward_subsumption_resolution,[],[f4153,f1161]) ).
fof(f4179,plain,
( ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m2_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_1(sK2)
| v18_waybel_0(sK2,sK0,sK1)
| ~ v3_lattice3(sK0)
| ~ v3_lattice3(sK1)
| ~ m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| l1_orders_2(sK1)
| ~ v1_funct_1(k2_waybel34(sK1,sK0,sK2))
| ~ v3_waybel_1(k1_waybel_1(sK1,sK0,k2_waybel34(sK1,sK0,sK2),sK2),sK1,sK0) ),
inference(forward_subsumption_resolution,[],[f4162,f523]) ).
fof(f4187,plain,
( ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m2_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_1(sK2)
| v18_waybel_0(sK2,sK0,sK1)
| ~ v3_lattice3(sK0)
| ~ v3_lattice3(sK1)
| ~ m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| l1_orders_2(sK1)
| ~ v1_funct_1(k2_waybel34(sK1,sK0,sK2))
| ~ v3_waybel_1(k1_waybel_1(sK1,sK0,k2_waybel34(sK1,sK0,sK2),sK2),sK1,sK0) ),
inference(forward_subsumption_resolution,[],[f4179,f524]) ).
fof(f4195,plain,
( v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ m2_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_1(sK2)
| v18_waybel_0(sK2,sK0,sK1)
| ~ v3_lattice3(sK0)
| ~ v3_lattice3(sK1)
| ~ m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| l1_orders_2(sK1)
| ~ v1_funct_1(k2_waybel34(sK1,sK0,sK2))
| ~ v3_waybel_1(k1_waybel_1(sK1,sK0,k2_waybel34(sK1,sK0,sK2),sK2),sK1,sK0) ),
inference(forward_subsumption_resolution,[],[f4187,f525]) ).
fof(f4203,plain,
( v2_orders_2(sK0)
| ~ m2_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_1(sK2)
| v18_waybel_0(sK2,sK0,sK1)
| ~ v3_lattice3(sK0)
| ~ v3_lattice3(sK1)
| ~ m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| l1_orders_2(sK1)
| ~ v1_funct_1(k2_waybel34(sK1,sK0,sK2))
| ~ v3_waybel_1(k1_waybel_1(sK1,sK0,k2_waybel34(sK1,sK0,sK2),sK2),sK1,sK0) ),
inference(forward_subsumption_resolution,[],[f4195,f1160]) ).
fof(f4211,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))
| ~ v1_funct_1(sK2)
| v18_waybel_0(sK2,sK0,sK1)
| ~ v3_lattice3(sK0)
| ~ v3_lattice3(sK1)
| ~ m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| l1_orders_2(sK1)
| ~ v1_funct_1(k2_waybel34(sK1,sK0,sK2))
| ~ v3_waybel_1(k1_waybel_1(sK1,sK0,k2_waybel34(sK1,sK0,sK2),sK2),sK1,sK0) ),
inference(forward_subsumption_resolution,[],[f4203,f1159]) ).
fof(f4219,plain,
( ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_1(sK2)
| v18_waybel_0(sK2,sK0,sK1)
| ~ v3_lattice3(sK0)
| ~ v3_lattice3(sK1)
| ~ m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| l1_orders_2(sK1)
| ~ v1_funct_1(k2_waybel34(sK1,sK0,sK2))
| ~ v3_waybel_1(k1_waybel_1(sK1,sK0,k2_waybel34(sK1,sK0,sK2),sK2),sK1,sK0) ),
inference(forward_subsumption_resolution,[],[f4211,f509]) ).
fof(f4231,plain,
( ~ v1_funct_1(sK2)
| v18_waybel_0(sK2,sK0,sK1)
| ~ v3_lattice3(sK0)
| ~ v3_lattice3(sK1)
| ~ m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| l1_orders_2(sK1)
| ~ v1_funct_1(k2_waybel34(sK1,sK0,sK2))
| ~ v3_waybel_1(k1_waybel_1(sK1,sK0,k2_waybel34(sK1,sK0,sK2),sK2),sK1,sK0) ),
inference(forward_subsumption_resolution,[],[f4219,f511]) ).
fof(f4238,plain,
( v18_waybel_0(sK2,sK0,sK1)
| ~ v3_lattice3(sK0)
| ~ v3_lattice3(sK1)
| ~ m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| l1_orders_2(sK1)
| ~ v1_funct_1(k2_waybel34(sK1,sK0,sK2))
| ~ v3_waybel_1(k1_waybel_1(sK1,sK0,k2_waybel34(sK1,sK0,sK2),sK2),sK1,sK0) ),
inference(forward_subsumption_resolution,[],[f4231,f512]) ).
fof(f4261,plain,
( ~ v3_lattice3(sK0)
| ~ v3_lattice3(sK1)
| ~ m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| l1_orders_2(sK1)
| ~ v1_funct_1(k2_waybel34(sK1,sK0,sK2))
| ~ v3_waybel_1(k1_waybel_1(sK1,sK0,k2_waybel34(sK1,sK0,sK2),sK2),sK1,sK0) ),
inference(forward_subsumption_resolution,[],[f4238,f1165]) ).
fof(f4264,plain,
( ~ v3_lattice3(sK1)
| ~ m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| l1_orders_2(sK1)
| ~ v1_funct_1(k2_waybel34(sK1,sK0,sK2))
| ~ v3_waybel_1(k1_waybel_1(sK1,sK0,k2_waybel34(sK1,sK0,sK2),sK2),sK1,sK0) ),
inference(forward_subsumption_resolution,[],[f4261,f522]) ).
fof(f4275,plain,
( ~ m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| l1_orders_2(sK1)
| ~ v1_funct_1(k2_waybel34(sK1,sK0,sK2))
| ~ v3_waybel_1(k1_waybel_1(sK1,sK0,k2_waybel34(sK1,sK0,sK2),sK2),sK1,sK0) ),
inference(forward_subsumption_resolution,[],[f4264,f515]) ).
fof(f4276,plain,
( ~ m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v1_funct_1(k2_waybel34(sK1,sK0,sK2))
| ~ v3_waybel_1(k1_waybel_1(sK1,sK0,k2_waybel34(sK1,sK0,sK2),sK2),sK1,sK0) ),
inference(forward_subsumption_resolution,[],[f4275,f1164]) ).
fof(f4277,plain,
( ~ m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v3_waybel_1(k1_waybel_1(sK1,sK0,k2_waybel34(sK1,sK0,sK2),sK2),sK1,sK0) ),
inference(forward_subsumption_resolution,[],[f4276,f3183]) ).
fof(f4279,definition,
( spl40_108
<=> v3_waybel_1(k1_waybel_1(sK1,sK0,k2_waybel34(sK1,sK0,sK2),sK2),sK1,sK0) ),
introduced(definition,[new_symbols(definition,[spl40_108])],[avatar_definition]) ).
fof(f4281,plain,
( ~ v3_waybel_1(k1_waybel_1(sK1,sK0,k2_waybel34(sK1,sK0,sK2),sK2),sK1,sK0)
| spl40_108 ),
inference(avatar_component_clause,[],[f4279]) ).
fof(f4282,plain,
( ~ spl40_108
| ~ spl40_98 ),
inference(avatar_split_clause,[],[f4277,f4147,f4279]) ).
fof(f4307,plain,
( ~ v3_lattice3(sK0)
| ~ v3_struct_0(sK0)
| l1_orders_2(sK0)
| spl40_57 ),
inference(resolution,[],[f3110,f1493]) ).
fof(f4310,plain,
( ~ v3_struct_0(sK0)
| l1_orders_2(sK0)
| spl40_57 ),
inference(forward_subsumption_resolution,[],[f4307,f522]) ).
fof(f4313,plain,
( l1_orders_2(sK0)
| spl40_57 ),
inference(forward_subsumption_resolution,[],[f4310,f1718]) ).
fof(f4314,plain,
( $false
| spl40_57 ),
inference(forward_subsumption_resolution,[],[f4313,f1161]) ).
fof(f4315,plain,
spl40_57,
inference(avatar_contradiction_clause,[],[f4314]) ).
fof(f4332,plain,
( ~ v3_lattice3(sK0)
| ~ v3_struct_0(sK0)
| l1_orders_2(sK0)
| spl40_58 ),
inference(resolution,[],[f3114,f1494]) ).
fof(f4335,plain,
( ~ v3_struct_0(sK0)
| l1_orders_2(sK0)
| spl40_58 ),
inference(forward_subsumption_resolution,[],[f4332,f522]) ).
fof(f4338,plain,
( l1_orders_2(sK0)
| spl40_58 ),
inference(forward_subsumption_resolution,[],[f4335,f1718]) ).
fof(f4339,plain,
( $false
| spl40_58 ),
inference(forward_subsumption_resolution,[],[f4338,f1161]) ).
fof(f4340,plain,
spl40_58,
inference(avatar_contradiction_clause,[],[f4339]) ).
fof(f4392,plain,
( ~ v3_lattice3(sK1)
| ~ v3_struct_0(sK1)
| l1_orders_2(sK1)
| spl40_59 ),
inference(resolution,[],[f3118,f1493]) ).
fof(f4395,plain,
( ~ v3_struct_0(sK1)
| l1_orders_2(sK1)
| spl40_59 ),
inference(forward_subsumption_resolution,[],[f4392,f515]) ).
fof(f4398,plain,
( l1_orders_2(sK1)
| spl40_59 ),
inference(forward_subsumption_resolution,[],[f4395,f1717]) ).
fof(f4399,plain,
( $false
| spl40_59 ),
inference(forward_subsumption_resolution,[],[f4398,f1164]) ).
fof(f4400,plain,
spl40_59,
inference(avatar_contradiction_clause,[],[f4399]) ).
fof(f5164,plain,
( ~ v3_lattice3(sK1)
| ~ v3_struct_0(sK1)
| l1_orders_2(sK1)
| spl40_60 ),
inference(resolution,[],[f3122,f1494]) ).
fof(f5167,plain,
( ~ v3_struct_0(sK1)
| l1_orders_2(sK1)
| spl40_60 ),
inference(forward_subsumption_resolution,[],[f5164,f515]) ).
fof(f5170,plain,
( l1_orders_2(sK1)
| spl40_60 ),
inference(forward_subsumption_resolution,[],[f5167,f1717]) ).
fof(f5171,plain,
( $false
| spl40_60 ),
inference(forward_subsumption_resolution,[],[f5170,f1164]) ).
fof(f5172,plain,
spl40_60,
inference(avatar_contradiction_clause,[],[f5171]) ).
fof(f5253,plain,
( ~ v3_lattice3(sK1)
| ~ v3_struct_0(sK1)
| l1_orders_2(sK1)
| spl40_66 ),
inference(resolution,[],[f3416,f1495]) ).
fof(f5254,plain,
( ~ v3_struct_0(sK1)
| l1_orders_2(sK1)
| spl40_66 ),
inference(forward_subsumption_resolution,[],[f5253,f515]) ).
fof(f5255,plain,
( l1_orders_2(sK1)
| spl40_66 ),
inference(forward_subsumption_resolution,[],[f5254,f1717]) ).
fof(f5256,plain,
( $false
| spl40_66 ),
inference(forward_subsumption_resolution,[],[f5255,f1164]) ).
fof(f5257,plain,
spl40_66,
inference(avatar_contradiction_clause,[],[f5256]) ).
fof(f5260,plain,
( ~ v3_lattice3(sK0)
| ~ v3_struct_0(sK0)
| l1_orders_2(sK0)
| spl40_67 ),
inference(resolution,[],[f3420,f1495]) ).
fof(f5261,plain,
( ~ v3_struct_0(sK0)
| l1_orders_2(sK0)
| spl40_67 ),
inference(forward_subsumption_resolution,[],[f5260,f522]) ).
fof(f5262,plain,
( l1_orders_2(sK0)
| spl40_67 ),
inference(forward_subsumption_resolution,[],[f5261,f1718]) ).
fof(f5263,plain,
( $false
| spl40_67 ),
inference(forward_subsumption_resolution,[],[f5262,f1161]) ).
fof(f5264,plain,
spl40_67,
inference(avatar_contradiction_clause,[],[f5263]) ).
fof(f10805,plain,
( ~ v1_funct_1(sK2)
| l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| l1_orders_2(sK1)
| ~ v2_lattice3(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| v3_orders_2(sK1)
| v2_orders_2(sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| spl40_94 ),
inference(resolution,[],[f4126,f3320]) ).
fof(f10806,plain,
( l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| l1_orders_2(sK1)
| ~ v2_lattice3(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| v3_orders_2(sK1)
| v2_orders_2(sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| spl40_94 ),
inference(forward_subsumption_resolution,[],[f10805,f512]) ).
fof(f10807,plain,
( ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| l1_orders_2(sK1)
| ~ v2_lattice3(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| v3_orders_2(sK1)
| v2_orders_2(sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| spl40_94 ),
inference(forward_subsumption_resolution,[],[f10806,f1161]) ).
fof(f10808,plain,
( ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| l1_orders_2(sK1)
| ~ v2_lattice3(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| v3_orders_2(sK1)
| v2_orders_2(sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| spl40_94 ),
inference(forward_subsumption_resolution,[],[f10807,f523]) ).
fof(f10809,plain,
( ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| l1_orders_2(sK1)
| ~ v2_lattice3(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| v3_orders_2(sK1)
| v2_orders_2(sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| spl40_94 ),
inference(forward_subsumption_resolution,[],[f10808,f524]) ).
fof(f10810,plain,
( v3_orders_2(sK0)
| v2_orders_2(sK0)
| l1_orders_2(sK1)
| ~ v2_lattice3(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| v3_orders_2(sK1)
| v2_orders_2(sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| spl40_94 ),
inference(forward_subsumption_resolution,[],[f10809,f525]) ).
fof(f10811,plain,
( v2_orders_2(sK0)
| l1_orders_2(sK1)
| ~ v2_lattice3(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| v3_orders_2(sK1)
| v2_orders_2(sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| spl40_94 ),
inference(forward_subsumption_resolution,[],[f10810,f1160]) ).
fof(f10812,plain,
( l1_orders_2(sK1)
| ~ v2_lattice3(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| v3_orders_2(sK1)
| v2_orders_2(sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| spl40_94 ),
inference(forward_subsumption_resolution,[],[f10811,f1159]) ).
fof(f10813,plain,
( ~ v2_lattice3(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| v3_orders_2(sK1)
| v2_orders_2(sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| spl40_94 ),
inference(forward_subsumption_resolution,[],[f10812,f1164]) ).
fof(f10814,plain,
( ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| v3_orders_2(sK1)
| v2_orders_2(sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| spl40_94 ),
inference(forward_subsumption_resolution,[],[f10813,f516]) ).
fof(f10815,plain,
( ~ v4_orders_2(sK1)
| v3_orders_2(sK1)
| v2_orders_2(sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| spl40_94 ),
inference(forward_subsumption_resolution,[],[f10814,f517]) ).
fof(f10816,plain,
( v3_orders_2(sK1)
| v2_orders_2(sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| spl40_94 ),
inference(forward_subsumption_resolution,[],[f10815,f518]) ).
fof(f10817,plain,
( v2_orders_2(sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| spl40_94 ),
inference(forward_subsumption_resolution,[],[f10816,f1163]) ).
fof(f10818,plain,
( ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| spl40_94 ),
inference(forward_subsumption_resolution,[],[f10817,f1162]) ).
fof(f10819,plain,
( ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| spl40_94 ),
inference(forward_subsumption_resolution,[],[f10818,f1784]) ).
fof(f10820,plain,
( $false
| spl40_94 ),
inference(forward_subsumption_resolution,[],[f10819,f511]) ).
fof(f10821,plain,
spl40_94,
inference(avatar_contradiction_clause,[],[f10820]) ).
fof(f10952,plain,
( ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_1(sK2)
| l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| l1_orders_2(sK1)
| ~ v2_lattice3(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| v3_orders_2(sK1)
| v2_orders_2(sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| spl40_98 ),
inference(resolution,[],[f4149,f1336]) ).
fof(f10956,plain,
( ~ v1_funct_1(sK2)
| l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| l1_orders_2(sK1)
| ~ v2_lattice3(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| v3_orders_2(sK1)
| v2_orders_2(sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| spl40_98 ),
inference(forward_subsumption_resolution,[],[f10952,f511]) ).
fof(f10957,plain,
( l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| l1_orders_2(sK1)
| ~ v2_lattice3(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| v3_orders_2(sK1)
| v2_orders_2(sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| spl40_98 ),
inference(forward_subsumption_resolution,[],[f10956,f512]) ).
fof(f10958,plain,
( ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| l1_orders_2(sK1)
| ~ v2_lattice3(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| v3_orders_2(sK1)
| v2_orders_2(sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| spl40_98 ),
inference(forward_subsumption_resolution,[],[f10957,f1161]) ).
fof(f10959,plain,
( ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| l1_orders_2(sK1)
| ~ v2_lattice3(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| v3_orders_2(sK1)
| v2_orders_2(sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| spl40_98 ),
inference(forward_subsumption_resolution,[],[f10958,f523]) ).
fof(f10960,plain,
( ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| l1_orders_2(sK1)
| ~ v2_lattice3(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| v3_orders_2(sK1)
| v2_orders_2(sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| spl40_98 ),
inference(forward_subsumption_resolution,[],[f10959,f524]) ).
fof(f10961,plain,
( v3_orders_2(sK0)
| v2_orders_2(sK0)
| l1_orders_2(sK1)
| ~ v2_lattice3(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| v3_orders_2(sK1)
| v2_orders_2(sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| spl40_98 ),
inference(forward_subsumption_resolution,[],[f10960,f525]) ).
fof(f10962,plain,
( v2_orders_2(sK0)
| l1_orders_2(sK1)
| ~ v2_lattice3(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| v3_orders_2(sK1)
| v2_orders_2(sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| spl40_98 ),
inference(forward_subsumption_resolution,[],[f10961,f1160]) ).
fof(f10963,plain,
( l1_orders_2(sK1)
| ~ v2_lattice3(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| v3_orders_2(sK1)
| v2_orders_2(sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| spl40_98 ),
inference(forward_subsumption_resolution,[],[f10962,f1159]) ).
fof(f10964,plain,
( ~ v2_lattice3(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| v3_orders_2(sK1)
| v2_orders_2(sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| spl40_98 ),
inference(forward_subsumption_resolution,[],[f10963,f1164]) ).
fof(f10965,plain,
( ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| v3_orders_2(sK1)
| v2_orders_2(sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| spl40_98 ),
inference(forward_subsumption_resolution,[],[f10964,f516]) ).
fof(f10966,plain,
( ~ v4_orders_2(sK1)
| v3_orders_2(sK1)
| v2_orders_2(sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| spl40_98 ),
inference(forward_subsumption_resolution,[],[f10965,f517]) ).
fof(f10967,plain,
( v3_orders_2(sK1)
| v2_orders_2(sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| spl40_98 ),
inference(forward_subsumption_resolution,[],[f10966,f518]) ).
fof(f10968,plain,
( v2_orders_2(sK1)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| spl40_98 ),
inference(forward_subsumption_resolution,[],[f10967,f1163]) ).
fof(f10969,plain,
( ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| spl40_98 ),
inference(forward_subsumption_resolution,[],[f10968,f1162]) ).
fof(f10970,plain,
( $false
| spl40_98 ),
inference(forward_subsumption_resolution,[],[f10969,f1784]) ).
fof(f10971,plain,
spl40_98,
inference(avatar_contradiction_clause,[],[f10970]) ).
fof(f11212,plain,
( v3_orders_2(sK1)
| v2_orders_2(sK1)
| ~ v3_struct_0(sK1)
| l1_orders_2(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ v3_struct_0(sK0)
| ~ m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v1_funct_2(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v1_funct_1(k2_waybel34(sK1,sK0,sK2))
| ~ m2_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_1(sK2)
| ~ m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ v1_funct_2(k2_waybel34(sK1,sK0,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ m2_relset_1(sK2,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ v1_funct_2(sK2,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| l1_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ v2_lattice3(k7_lattice3(sK0))
| ~ v1_lattice3(k7_lattice3(sK0))
| ~ v2_lattice3(k7_lattice3(sK1))
| ~ v1_lattice3(k7_lattice3(sK1))
| ~ v17_waybel_0(sK2,k7_lattice3(sK0),k7_lattice3(sK1))
| ~ v3_lattice3(k7_lattice3(sK1))
| ~ v3_lattice3(k7_lattice3(sK0))
| k2_waybel34(sK1,sK0,sK2) = k1_waybel34(k7_lattice3(sK0),k7_lattice3(sK1),sK2)
| spl40_108 ),
inference(resolution,[],[f4281,f3847]) ).
fof(f11216,plain,
( v2_orders_2(sK1)
| ~ v3_struct_0(sK1)
| l1_orders_2(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ v3_struct_0(sK0)
| ~ m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v1_funct_2(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v1_funct_1(k2_waybel34(sK1,sK0,sK2))
| ~ m2_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_1(sK2)
| ~ m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ v1_funct_2(k2_waybel34(sK1,sK0,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ m2_relset_1(sK2,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ v1_funct_2(sK2,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| l1_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ v2_lattice3(k7_lattice3(sK0))
| ~ v1_lattice3(k7_lattice3(sK0))
| ~ v2_lattice3(k7_lattice3(sK1))
| ~ v1_lattice3(k7_lattice3(sK1))
| ~ v17_waybel_0(sK2,k7_lattice3(sK0),k7_lattice3(sK1))
| ~ v3_lattice3(k7_lattice3(sK1))
| ~ v3_lattice3(k7_lattice3(sK0))
| k2_waybel34(sK1,sK0,sK2) = k1_waybel34(k7_lattice3(sK0),k7_lattice3(sK1),sK2)
| spl40_108 ),
inference(forward_subsumption_resolution,[],[f11212,f1163]) ).
fof(f11219,plain,
( ~ v3_struct_0(sK1)
| l1_orders_2(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ v3_struct_0(sK0)
| ~ m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v1_funct_2(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v1_funct_1(k2_waybel34(sK1,sK0,sK2))
| ~ m2_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_1(sK2)
| ~ m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ v1_funct_2(k2_waybel34(sK1,sK0,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ m2_relset_1(sK2,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ v1_funct_2(sK2,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| l1_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ v2_lattice3(k7_lattice3(sK0))
| ~ v1_lattice3(k7_lattice3(sK0))
| ~ v2_lattice3(k7_lattice3(sK1))
| ~ v1_lattice3(k7_lattice3(sK1))
| ~ v17_waybel_0(sK2,k7_lattice3(sK0),k7_lattice3(sK1))
| ~ v3_lattice3(k7_lattice3(sK1))
| ~ v3_lattice3(k7_lattice3(sK0))
| k2_waybel34(sK1,sK0,sK2) = k1_waybel34(k7_lattice3(sK0),k7_lattice3(sK1),sK2)
| spl40_108 ),
inference(forward_subsumption_resolution,[],[f11216,f1162]) ).
fof(f11222,plain,
( l1_orders_2(sK0)
| ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ v3_struct_0(sK0)
| ~ m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v1_funct_2(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v1_funct_1(k2_waybel34(sK1,sK0,sK2))
| ~ m2_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_1(sK2)
| ~ m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ v1_funct_2(k2_waybel34(sK1,sK0,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ m2_relset_1(sK2,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ v1_funct_2(sK2,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| l1_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ v2_lattice3(k7_lattice3(sK0))
| ~ v1_lattice3(k7_lattice3(sK0))
| ~ v2_lattice3(k7_lattice3(sK1))
| ~ v1_lattice3(k7_lattice3(sK1))
| ~ v17_waybel_0(sK2,k7_lattice3(sK0),k7_lattice3(sK1))
| ~ v3_lattice3(k7_lattice3(sK1))
| ~ v3_lattice3(k7_lattice3(sK0))
| k2_waybel34(sK1,sK0,sK2) = k1_waybel34(k7_lattice3(sK0),k7_lattice3(sK1),sK2)
| spl40_108 ),
inference(forward_subsumption_resolution,[],[f11219,f1717]) ).
fof(f11225,plain,
( ~ v4_orders_2(sK0)
| v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ v3_struct_0(sK0)
| ~ m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v1_funct_2(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v1_funct_1(k2_waybel34(sK1,sK0,sK2))
| ~ m2_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_1(sK2)
| ~ m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ v1_funct_2(k2_waybel34(sK1,sK0,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ m2_relset_1(sK2,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ v1_funct_2(sK2,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| l1_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ v2_lattice3(k7_lattice3(sK0))
| ~ v1_lattice3(k7_lattice3(sK0))
| ~ v2_lattice3(k7_lattice3(sK1))
| ~ v1_lattice3(k7_lattice3(sK1))
| ~ v17_waybel_0(sK2,k7_lattice3(sK0),k7_lattice3(sK1))
| ~ v3_lattice3(k7_lattice3(sK1))
| ~ v3_lattice3(k7_lattice3(sK0))
| k2_waybel34(sK1,sK0,sK2) = k1_waybel34(k7_lattice3(sK0),k7_lattice3(sK1),sK2)
| spl40_108 ),
inference(forward_subsumption_resolution,[],[f11222,f1161]) ).
fof(f11228,plain,
( v3_orders_2(sK0)
| v2_orders_2(sK0)
| ~ v3_struct_0(sK0)
| ~ m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v1_funct_2(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v1_funct_1(k2_waybel34(sK1,sK0,sK2))
| ~ m2_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_1(sK2)
| ~ m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ v1_funct_2(k2_waybel34(sK1,sK0,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ m2_relset_1(sK2,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ v1_funct_2(sK2,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| l1_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ v2_lattice3(k7_lattice3(sK0))
| ~ v1_lattice3(k7_lattice3(sK0))
| ~ v2_lattice3(k7_lattice3(sK1))
| ~ v1_lattice3(k7_lattice3(sK1))
| ~ v17_waybel_0(sK2,k7_lattice3(sK0),k7_lattice3(sK1))
| ~ v3_lattice3(k7_lattice3(sK1))
| ~ v3_lattice3(k7_lattice3(sK0))
| k2_waybel34(sK1,sK0,sK2) = k1_waybel34(k7_lattice3(sK0),k7_lattice3(sK1),sK2)
| spl40_108 ),
inference(forward_subsumption_resolution,[],[f11225,f525]) ).
fof(f11231,plain,
( v2_orders_2(sK0)
| ~ v3_struct_0(sK0)
| ~ m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v1_funct_2(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v1_funct_1(k2_waybel34(sK1,sK0,sK2))
| ~ m2_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_1(sK2)
| ~ m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ v1_funct_2(k2_waybel34(sK1,sK0,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ m2_relset_1(sK2,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ v1_funct_2(sK2,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| l1_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ v2_lattice3(k7_lattice3(sK0))
| ~ v1_lattice3(k7_lattice3(sK0))
| ~ v2_lattice3(k7_lattice3(sK1))
| ~ v1_lattice3(k7_lattice3(sK1))
| ~ v17_waybel_0(sK2,k7_lattice3(sK0),k7_lattice3(sK1))
| ~ v3_lattice3(k7_lattice3(sK1))
| ~ v3_lattice3(k7_lattice3(sK0))
| k2_waybel34(sK1,sK0,sK2) = k1_waybel34(k7_lattice3(sK0),k7_lattice3(sK1),sK2)
| spl40_108 ),
inference(forward_subsumption_resolution,[],[f11228,f1160]) ).
fof(f11234,plain,
( ~ v3_struct_0(sK0)
| ~ m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v1_funct_2(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v1_funct_1(k2_waybel34(sK1,sK0,sK2))
| ~ m2_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_1(sK2)
| ~ m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ v1_funct_2(k2_waybel34(sK1,sK0,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ m2_relset_1(sK2,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ v1_funct_2(sK2,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| l1_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ v2_lattice3(k7_lattice3(sK0))
| ~ v1_lattice3(k7_lattice3(sK0))
| ~ v2_lattice3(k7_lattice3(sK1))
| ~ v1_lattice3(k7_lattice3(sK1))
| ~ v17_waybel_0(sK2,k7_lattice3(sK0),k7_lattice3(sK1))
| ~ v3_lattice3(k7_lattice3(sK1))
| ~ v3_lattice3(k7_lattice3(sK0))
| k2_waybel34(sK1,sK0,sK2) = k1_waybel34(k7_lattice3(sK0),k7_lattice3(sK1),sK2)
| spl40_108 ),
inference(forward_subsumption_resolution,[],[f11231,f1159]) ).
fof(f11237,plain,
( ~ m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v1_funct_2(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v1_funct_1(k2_waybel34(sK1,sK0,sK2))
| ~ m2_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_1(sK2)
| ~ m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ v1_funct_2(k2_waybel34(sK1,sK0,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ m2_relset_1(sK2,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ v1_funct_2(sK2,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| l1_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ v2_lattice3(k7_lattice3(sK0))
| ~ v1_lattice3(k7_lattice3(sK0))
| ~ v2_lattice3(k7_lattice3(sK1))
| ~ v1_lattice3(k7_lattice3(sK1))
| ~ v17_waybel_0(sK2,k7_lattice3(sK0),k7_lattice3(sK1))
| ~ v3_lattice3(k7_lattice3(sK1))
| ~ v3_lattice3(k7_lattice3(sK0))
| k2_waybel34(sK1,sK0,sK2) = k1_waybel34(k7_lattice3(sK0),k7_lattice3(sK1),sK2)
| spl40_108 ),
inference(forward_subsumption_resolution,[],[f11234,f1718]) ).
fof(f11240,plain,
( ~ v1_funct_2(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v1_funct_1(k2_waybel34(sK1,sK0,sK2))
| ~ m2_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_1(sK2)
| ~ m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ v1_funct_2(k2_waybel34(sK1,sK0,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ m2_relset_1(sK2,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ v1_funct_2(sK2,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| l1_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ v2_lattice3(k7_lattice3(sK0))
| ~ v1_lattice3(k7_lattice3(sK0))
| ~ v2_lattice3(k7_lattice3(sK1))
| ~ v1_lattice3(k7_lattice3(sK1))
| ~ v17_waybel_0(sK2,k7_lattice3(sK0),k7_lattice3(sK1))
| ~ v3_lattice3(k7_lattice3(sK1))
| ~ v3_lattice3(k7_lattice3(sK0))
| k2_waybel34(sK1,sK0,sK2) = k1_waybel34(k7_lattice3(sK0),k7_lattice3(sK1),sK2)
| ~ spl40_98
| spl40_108 ),
inference(forward_subsumption_resolution,[],[f11237,f4148]) ).
fof(f11243,plain,
( ~ v1_funct_1(k2_waybel34(sK1,sK0,sK2))
| ~ m2_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_1(sK2)
| ~ m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ v1_funct_2(k2_waybel34(sK1,sK0,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ m2_relset_1(sK2,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ v1_funct_2(sK2,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| l1_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ v2_lattice3(k7_lattice3(sK0))
| ~ v1_lattice3(k7_lattice3(sK0))
| ~ v2_lattice3(k7_lattice3(sK1))
| ~ v1_lattice3(k7_lattice3(sK1))
| ~ v17_waybel_0(sK2,k7_lattice3(sK0),k7_lattice3(sK1))
| ~ v3_lattice3(k7_lattice3(sK1))
| ~ v3_lattice3(k7_lattice3(sK0))
| k2_waybel34(sK1,sK0,sK2) = k1_waybel34(k7_lattice3(sK0),k7_lattice3(sK1),sK2)
| ~ spl40_98
| spl40_108 ),
inference(forward_subsumption_resolution,[],[f11240,f3318]) ).
fof(f11246,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))
| ~ v1_funct_1(sK2)
| ~ m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ v1_funct_2(k2_waybel34(sK1,sK0,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ m2_relset_1(sK2,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ v1_funct_2(sK2,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| l1_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ v2_lattice3(k7_lattice3(sK0))
| ~ v1_lattice3(k7_lattice3(sK0))
| ~ v2_lattice3(k7_lattice3(sK1))
| ~ v1_lattice3(k7_lattice3(sK1))
| ~ v17_waybel_0(sK2,k7_lattice3(sK0),k7_lattice3(sK1))
| ~ v3_lattice3(k7_lattice3(sK1))
| ~ v3_lattice3(k7_lattice3(sK0))
| k2_waybel34(sK1,sK0,sK2) = k1_waybel34(k7_lattice3(sK0),k7_lattice3(sK1),sK2)
| ~ spl40_98
| spl40_108 ),
inference(forward_subsumption_resolution,[],[f11243,f3183]) ).
fof(f11249,plain,
( ~ v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_1(sK2)
| ~ m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ v1_funct_2(k2_waybel34(sK1,sK0,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ m2_relset_1(sK2,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ v1_funct_2(sK2,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| l1_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ v2_lattice3(k7_lattice3(sK0))
| ~ v1_lattice3(k7_lattice3(sK0))
| ~ v2_lattice3(k7_lattice3(sK1))
| ~ v1_lattice3(k7_lattice3(sK1))
| ~ v17_waybel_0(sK2,k7_lattice3(sK0),k7_lattice3(sK1))
| ~ v3_lattice3(k7_lattice3(sK1))
| ~ v3_lattice3(k7_lattice3(sK0))
| k2_waybel34(sK1,sK0,sK2) = k1_waybel34(k7_lattice3(sK0),k7_lattice3(sK1),sK2)
| ~ spl40_98
| spl40_108 ),
inference(forward_subsumption_resolution,[],[f11246,f509]) ).
fof(f11252,plain,
( ~ v1_funct_1(sK2)
| ~ m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ v1_funct_2(k2_waybel34(sK1,sK0,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ m2_relset_1(sK2,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ v1_funct_2(sK2,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| l1_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ v2_lattice3(k7_lattice3(sK0))
| ~ v1_lattice3(k7_lattice3(sK0))
| ~ v2_lattice3(k7_lattice3(sK1))
| ~ v1_lattice3(k7_lattice3(sK1))
| ~ v17_waybel_0(sK2,k7_lattice3(sK0),k7_lattice3(sK1))
| ~ v3_lattice3(k7_lattice3(sK1))
| ~ v3_lattice3(k7_lattice3(sK0))
| k2_waybel34(sK1,sK0,sK2) = k1_waybel34(k7_lattice3(sK0),k7_lattice3(sK1),sK2)
| ~ spl40_98
| spl40_108 ),
inference(forward_subsumption_resolution,[],[f11249,f511]) ).
fof(f11255,plain,
( ~ m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ v1_funct_2(k2_waybel34(sK1,sK0,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ m2_relset_1(sK2,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| ~ v1_funct_2(sK2,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| l1_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ v2_lattice3(k7_lattice3(sK0))
| ~ v1_lattice3(k7_lattice3(sK0))
| ~ v2_lattice3(k7_lattice3(sK1))
| ~ v1_lattice3(k7_lattice3(sK1))
| ~ v17_waybel_0(sK2,k7_lattice3(sK0),k7_lattice3(sK1))
| ~ v3_lattice3(k7_lattice3(sK1))
| ~ v3_lattice3(k7_lattice3(sK0))
| k2_waybel34(sK1,sK0,sK2) = k1_waybel34(k7_lattice3(sK0),k7_lattice3(sK1),sK2)
| ~ spl40_98
| spl40_108 ),
inference(forward_subsumption_resolution,[],[f11252,f512]) ).
fof(f11258,plain,
( ~ m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ v1_funct_2(k2_waybel34(sK1,sK0,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ v1_funct_2(sK2,u1_struct_0(k7_lattice3(sK0)),u1_struct_0(k7_lattice3(sK1)))
| l1_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ v2_lattice3(k7_lattice3(sK0))
| ~ v1_lattice3(k7_lattice3(sK0))
| ~ v2_lattice3(k7_lattice3(sK1))
| ~ v1_lattice3(k7_lattice3(sK1))
| ~ v17_waybel_0(sK2,k7_lattice3(sK0),k7_lattice3(sK1))
| ~ v3_lattice3(k7_lattice3(sK1))
| ~ v3_lattice3(k7_lattice3(sK0))
| k2_waybel34(sK1,sK0,sK2) = k1_waybel34(k7_lattice3(sK0),k7_lattice3(sK1),sK2)
| ~ spl40_41
| ~ spl40_98
| spl40_108 ),
inference(forward_subsumption_resolution,[],[f11255,f2887]) ).
fof(f11261,plain,
( ~ m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ v1_funct_2(k2_waybel34(sK1,sK0,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| l1_orders_2(sK1)
| ~ v4_orders_2(sK1)
| ~ v2_lattice3(k7_lattice3(sK0))
| ~ v1_lattice3(k7_lattice3(sK0))
| ~ v2_lattice3(k7_lattice3(sK1))
| ~ v1_lattice3(k7_lattice3(sK1))
| ~ v17_waybel_0(sK2,k7_lattice3(sK0),k7_lattice3(sK1))
| ~ v3_lattice3(k7_lattice3(sK1))
| ~ v3_lattice3(k7_lattice3(sK0))
| k2_waybel34(sK1,sK0,sK2) = k1_waybel34(k7_lattice3(sK0),k7_lattice3(sK1),sK2)
| ~ spl40_41
| ~ spl40_98
| spl40_108 ),
inference(forward_subsumption_resolution,[],[f11258,f2857]) ).
fof(f11264,plain,
( ~ m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ v1_funct_2(k2_waybel34(sK1,sK0,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ v4_orders_2(sK1)
| ~ v2_lattice3(k7_lattice3(sK0))
| ~ v1_lattice3(k7_lattice3(sK0))
| ~ v2_lattice3(k7_lattice3(sK1))
| ~ v1_lattice3(k7_lattice3(sK1))
| ~ v17_waybel_0(sK2,k7_lattice3(sK0),k7_lattice3(sK1))
| ~ v3_lattice3(k7_lattice3(sK1))
| ~ v3_lattice3(k7_lattice3(sK0))
| k2_waybel34(sK1,sK0,sK2) = k1_waybel34(k7_lattice3(sK0),k7_lattice3(sK1),sK2)
| ~ spl40_41
| ~ spl40_98
| spl40_108 ),
inference(forward_subsumption_resolution,[],[f11261,f1164]) ).
fof(f11267,plain,
( ~ m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ v1_funct_2(k2_waybel34(sK1,sK0,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ v2_lattice3(k7_lattice3(sK0))
| ~ v1_lattice3(k7_lattice3(sK0))
| ~ v2_lattice3(k7_lattice3(sK1))
| ~ v1_lattice3(k7_lattice3(sK1))
| ~ v17_waybel_0(sK2,k7_lattice3(sK0),k7_lattice3(sK1))
| ~ v3_lattice3(k7_lattice3(sK1))
| ~ v3_lattice3(k7_lattice3(sK0))
| k2_waybel34(sK1,sK0,sK2) = k1_waybel34(k7_lattice3(sK0),k7_lattice3(sK1),sK2)
| ~ spl40_41
| ~ spl40_98
| spl40_108 ),
inference(forward_subsumption_resolution,[],[f11264,f518]) ).
fof(f11270,plain,
( ~ m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ v1_funct_2(k2_waybel34(sK1,sK0,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ v1_lattice3(k7_lattice3(sK0))
| ~ v2_lattice3(k7_lattice3(sK1))
| ~ v1_lattice3(k7_lattice3(sK1))
| ~ v17_waybel_0(sK2,k7_lattice3(sK0),k7_lattice3(sK1))
| ~ v3_lattice3(k7_lattice3(sK1))
| ~ v3_lattice3(k7_lattice3(sK0))
| k2_waybel34(sK1,sK0,sK2) = k1_waybel34(k7_lattice3(sK0),k7_lattice3(sK1),sK2)
| ~ spl40_41
| ~ spl40_58
| ~ spl40_98
| spl40_108 ),
inference(forward_subsumption_resolution,[],[f11267,f3113]) ).
fof(f11273,plain,
( ~ m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ v1_funct_2(k2_waybel34(sK1,sK0,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ v2_lattice3(k7_lattice3(sK1))
| ~ v1_lattice3(k7_lattice3(sK1))
| ~ v17_waybel_0(sK2,k7_lattice3(sK0),k7_lattice3(sK1))
| ~ v3_lattice3(k7_lattice3(sK1))
| ~ v3_lattice3(k7_lattice3(sK0))
| k2_waybel34(sK1,sK0,sK2) = k1_waybel34(k7_lattice3(sK0),k7_lattice3(sK1),sK2)
| ~ spl40_41
| ~ spl40_57
| ~ spl40_58
| ~ spl40_98
| spl40_108 ),
inference(forward_subsumption_resolution,[],[f11270,f3109]) ).
fof(f11284,plain,
( ~ m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ v1_funct_2(k2_waybel34(sK1,sK0,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ v1_lattice3(k7_lattice3(sK1))
| ~ v17_waybel_0(sK2,k7_lattice3(sK0),k7_lattice3(sK1))
| ~ v3_lattice3(k7_lattice3(sK1))
| ~ v3_lattice3(k7_lattice3(sK0))
| k2_waybel34(sK1,sK0,sK2) = k1_waybel34(k7_lattice3(sK0),k7_lattice3(sK1),sK2)
| ~ spl40_41
| ~ spl40_57
| ~ spl40_58
| ~ spl40_60
| ~ spl40_98
| spl40_108 ),
inference(forward_subsumption_resolution,[],[f11273,f3121]) ).
fof(f11286,plain,
( ~ m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ v1_funct_2(k2_waybel34(sK1,sK0,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ v17_waybel_0(sK2,k7_lattice3(sK0),k7_lattice3(sK1))
| ~ v3_lattice3(k7_lattice3(sK1))
| ~ v3_lattice3(k7_lattice3(sK0))
| k2_waybel34(sK1,sK0,sK2) = k1_waybel34(k7_lattice3(sK0),k7_lattice3(sK1),sK2)
| ~ spl40_41
| ~ spl40_57
| ~ spl40_58
| ~ spl40_59
| ~ spl40_60
| ~ spl40_98
| spl40_108 ),
inference(forward_subsumption_resolution,[],[f11284,f3117]) ).
fof(f11288,plain,
( ~ m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ v1_funct_2(k2_waybel34(sK1,sK0,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ v3_lattice3(k7_lattice3(sK1))
| ~ v3_lattice3(k7_lattice3(sK0))
| k2_waybel34(sK1,sK0,sK2) = k1_waybel34(k7_lattice3(sK0),k7_lattice3(sK1),sK2)
| ~ spl40_41
| ~ spl40_57
| ~ spl40_58
| ~ spl40_59
| ~ spl40_60
| ~ spl40_71
| ~ spl40_98
| spl40_108 ),
inference(forward_subsumption_resolution,[],[f11286,f3582]) ).
fof(f11290,plain,
( ~ m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ v1_funct_2(k2_waybel34(sK1,sK0,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ v3_lattice3(k7_lattice3(sK0))
| k2_waybel34(sK1,sK0,sK2) = k1_waybel34(k7_lattice3(sK0),k7_lattice3(sK1),sK2)
| ~ spl40_41
| ~ spl40_57
| ~ spl40_58
| ~ spl40_59
| ~ spl40_60
| ~ spl40_66
| ~ spl40_71
| ~ spl40_98
| spl40_108 ),
inference(forward_subsumption_resolution,[],[f11288,f3415]) ).
fof(f11292,plain,
( ~ m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ v1_funct_2(k2_waybel34(sK1,sK0,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| k2_waybel34(sK1,sK0,sK2) = k1_waybel34(k7_lattice3(sK0),k7_lattice3(sK1),sK2)
| ~ spl40_41
| ~ spl40_57
| ~ spl40_58
| ~ spl40_59
| ~ spl40_60
| ~ spl40_66
| ~ spl40_67
| ~ spl40_71
| ~ spl40_98
| spl40_108 ),
inference(forward_subsumption_resolution,[],[f11290,f3419]) ).
fof(f11302,definition,
( spl40_495
<=> v1_funct_2(k2_waybel34(sK1,sK0,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0))) ),
introduced(definition,[new_symbols(definition,[spl40_495])],[avatar_definition]) ).
fof(f11306,definition,
( spl40_496
<=> m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0))) ),
introduced(definition,[new_symbols(definition,[spl40_496])],[avatar_definition]) ).
fof(f11310,plain,
( ~ m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ v1_funct_2(k2_waybel34(sK1,sK0,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ spl40_41
| ~ spl40_57
| ~ spl40_58
| ~ spl40_59
| ~ spl40_60
| ~ spl40_66
| ~ spl40_67
| ~ spl40_71
| ~ spl40_98
| spl40_108 ),
inference(forward_subsumption_resolution,[],[f11292,f2843]) ).
fof(f11311,plain,
( ~ spl40_495
| ~ spl40_496
| ~ spl40_41
| ~ spl40_57
| ~ spl40_58
| ~ spl40_59
| ~ spl40_60
| ~ spl40_66
| ~ spl40_67
| ~ spl40_71
| ~ spl40_98
| spl40_108 ),
inference(avatar_split_clause,[],[f11310,f4279,f4147,f3581,f3418,f3414,f3120,f3116,f3112,f3108,f2886,f11306,f11302]) ).
fof(f12199,plain,
( v1_funct_2(k2_waybel34(sK1,sK0,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ v1_funct_2(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v1_funct_1(k2_waybel34(sK1,sK0,sK2))
| l1_orders_2(sK0)
| l1_orders_2(sK1)
| ~ m1_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ spl40_97 ),
inference(superposition,[],[f1338,f4145]) ).
fof(f12200,plain,
( m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ v1_funct_2(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ v1_funct_1(k2_waybel34(sK1,sK0,sK2))
| l1_orders_2(sK0)
| l1_orders_2(sK1)
| ~ m1_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ spl40_97 ),
inference(superposition,[],[f1339,f4145]) ).
fof(f12219,plain,
( m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ v1_funct_1(k2_waybel34(sK1,sK0,sK2))
| l1_orders_2(sK0)
| l1_orders_2(sK1)
| ~ m1_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ spl40_97 ),
inference(forward_subsumption_resolution,[],[f12200,f3318]) ).
fof(f12220,plain,
( v1_funct_2(k2_waybel34(sK1,sK0,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ v1_funct_1(k2_waybel34(sK1,sK0,sK2))
| l1_orders_2(sK0)
| l1_orders_2(sK1)
| ~ m1_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ spl40_97 ),
inference(forward_subsumption_resolution,[],[f12199,f3318]) ).
fof(f12229,plain,
( m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| l1_orders_2(sK0)
| l1_orders_2(sK1)
| ~ m1_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ spl40_97 ),
inference(forward_subsumption_resolution,[],[f12219,f3183]) ).
fof(f12230,plain,
( v1_funct_2(k2_waybel34(sK1,sK0,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| l1_orders_2(sK0)
| l1_orders_2(sK1)
| ~ m1_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ spl40_97 ),
inference(forward_subsumption_resolution,[],[f12220,f3183]) ).
fof(f12239,plain,
( m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| l1_orders_2(sK1)
| ~ m1_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ spl40_97 ),
inference(forward_subsumption_resolution,[],[f12229,f1161]) ).
fof(f12240,plain,
( v1_funct_2(k2_waybel34(sK1,sK0,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| l1_orders_2(sK1)
| ~ m1_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ spl40_97 ),
inference(forward_subsumption_resolution,[],[f12230,f1161]) ).
fof(f12249,plain,
( m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ m1_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ spl40_97 ),
inference(forward_subsumption_resolution,[],[f12239,f1164]) ).
fof(f12250,plain,
( v1_funct_2(k2_waybel34(sK1,sK0,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ m1_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(sK1),u1_struct_0(sK0))
| ~ spl40_97 ),
inference(forward_subsumption_resolution,[],[f12240,f1164]) ).
fof(f12259,plain,
( m2_relset_1(k2_waybel34(sK1,sK0,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ spl40_94
| ~ spl40_97 ),
inference(forward_subsumption_resolution,[],[f12249,f4125]) ).
fof(f12260,plain,
( v1_funct_2(k2_waybel34(sK1,sK0,sK2),u1_struct_0(k7_lattice3(sK1)),u1_struct_0(k7_lattice3(sK0)))
| ~ spl40_94
| ~ spl40_97 ),
inference(forward_subsumption_resolution,[],[f12250,f4125]) ).
fof(f12267,plain,
( spl40_496
| ~ spl40_94
| ~ spl40_97 ),
inference(avatar_split_clause,[],[f12259,f4143,f4124,f11306]) ).
fof(f12268,plain,
( spl40_495
| ~ spl40_94
| ~ spl40_97 ),
inference(avatar_split_clause,[],[f12260,f4143,f4124,f11302]) ).
cnf(s35,plain,
spl40_41,
inference(sat_conversion,[],[f2890]) ).
cnf(s64,plain,
spl40_71,
inference(sat_conversion,[],[f3745]) ).
cnf(s87,plain,
( spl40_97
| ~ spl40_98 ),
inference(sat_conversion,[],[f4150]) ).
cnf(s96,plain,
( ~ spl40_98
| ~ spl40_108 ),
inference(sat_conversion,[],[f4282]) ).
cnf(s101,plain,
spl40_57,
inference(sat_conversion,[],[f4315]) ).
cnf(s103,plain,
spl40_58,
inference(sat_conversion,[],[f4340]) ).
cnf(s109,plain,
spl40_59,
inference(sat_conversion,[],[f4400]) ).
cnf(s162,plain,
spl40_60,
inference(sat_conversion,[],[f5172]) ).
cnf(s167,plain,
spl40_66,
inference(sat_conversion,[],[f5257]) ).
cnf(s168,plain,
spl40_67,
inference(sat_conversion,[],[f5264]) ).
cnf(s412,plain,
spl40_94,
inference(sat_conversion,[],[f10821]) ).
cnf(s423,plain,
spl40_98,
inference(sat_conversion,[],[f10971]) ).
cnf(s457,plain,
( ~ spl40_41
| ~ spl40_57
| ~ spl40_58
| ~ spl40_59
| ~ spl40_60
| ~ spl40_66
| ~ spl40_67
| ~ spl40_71
| ~ spl40_98
| spl40_108
| ~ spl40_495
| ~ spl40_496 ),
inference(sat_conversion,[],[f11311]) ).
cnf(s515,plain,
( ~ spl40_94
| ~ spl40_97
| spl40_496 ),
inference(sat_conversion,[],[f12267]) ).
cnf(s516,plain,
( ~ spl40_94
| ~ spl40_97
| spl40_495 ),
inference(sat_conversion,[],[f12268]) ).
cnf(s590,plain,
~ spl40_108,
inference(rat,[],[s96,s423]) ).
cnf(s599,plain,
spl40_97,
inference(rat,[],[s87,s423]) ).
cnf(s601,plain,
spl40_495,
inference(rat,[],[s516,s412,s599]) ).
cnf(s602,plain,
spl40_496,
inference(rat,[],[s515,s412,s599]) ).
cnf(s620,plain,
~ spl40_41,
inference(rat,[],[s457,s602,s601,s590,s423,s101,s168,s167,s162,s109,s103,s64]) ).
cnf(s683,plain,
$false,
inference(rat,[],[s35,s620]) ).
fof(f12335,plain,
$false,
inference(avatar_sat_refutation,[],[s683]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : LAT355+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.18/0.43 % Computer : n007.cluster.edu
% 0.18/0.43 % Model : x86_64 x86_64
% 0.18/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.43 % Memory : 8046.5625MB
% 0.18/0.43 % OS : Linux 6.8.0-71-generic
% 0.18/0.43 % CPULimit : 300
% 0.18/0.43 % WCLimit : 300
% 0.18/0.43 % DateTime : Sun Sep 27 14:55:41 UTC 2026
% 0.18/0.43 % CPUTime :
% 0.18/0.43 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.18/0.47 Running first-order model finding
% 0.18/0.47 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.38/0.79 % (1529145)Will run a generic schedule for satisfiability detection.
% 1.38/0.79 % (1529161)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1478623562:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 1.38/0.79 % (1529156)% WARNING: option uhcvi not known.
% 1.38/0.79 % (1529157)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3696107930:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 1.38/0.79 % (1529159)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1815312221:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 1.38/0.79 % (1529155)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3150056777_2999 on theBenchmark for (2999ds/0Mi)
% 1.38/0.79 % (1529156)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2870634677:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 1.38/0.79 % (1529158)dis+10_1_sil=32000:sp=arity:random_seed=46408841:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 1.38/0.79 % (1529160)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=959934002:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 1.38/0.79 % (1529161)Instruction limit reached!
% 1.38/0.79 % (1529161)------------------------------
% 1.38/0.79 % (1529161)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.38/0.79 % (1529161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.38/0.79 % (1529161)CaDiCaL version: 2.1.3
% 1.38/0.79 % (1529161)Termination reason: Instruction limit
% 1.38/0.79 % (1529161)Termination phase: Saturation
% 1.38/0.79 % (1529161)Time elapsed: 0.052 s
% 1.38/0.79 % (1529161)Peak memory usage: 15 MB
% 1.38/0.79 % (1529161)Instructions burned: 161 (million)
% 1.38/0.79 % TRYING [1]
% 1.38/0.79 % TRYING [2]
% 1.38/0.79 % (1529198)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3491568759:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 1.38/0.79 % (1529158)Instruction limit reached!
% 1.38/0.79 % (1529158)------------------------------
% 1.38/0.79 % (1529158)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.38/0.79 % (1529158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.38/0.79 % (1529158)CaDiCaL version: 2.1.3
% 1.38/0.79 % (1529158)Termination reason: Instruction limit
% 1.38/0.79 % (1529158)Termination phase: Saturation
% 1.38/0.79 % (1529158)Time elapsed: 0.058 s
% 1.38/0.79 % (1529158)Peak memory usage: 13 MB
% 1.38/0.79 % (1529158)Instructions burned: 103 (million)
% 1.38/0.79 % (1529159)Instruction limit reached!
% 1.38/0.79 % (1529159)------------------------------
% 1.38/0.79 % (1529159)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.38/0.79 % (1529159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.38/0.79 % (1529159)CaDiCaL version: 2.1.3
% 1.38/0.79 % (1529159)Termination reason: Instruction limit
% 1.38/0.79 % (1529159)Termination phase: Saturation
% 1.38/0.79 % (1529159)Time elapsed: 0.062 s
% 1.38/0.79 % (1529159)Peak memory usage: 14 MB
% 1.38/0.79 % (1529159)Instructions burned: 116 (million)
% 1.38/0.79 % TRYING [3]
% 1.38/0.79 % (1529160)Instruction limit reached!
% 1.38/0.79 % (1529160)------------------------------
% 1.38/0.79 % (1529160)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.38/0.79 % (1529160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.38/0.79 % (1529160)CaDiCaL version: 2.1.3
% 1.38/0.79 % (1529160)Termination reason: Instruction limit
% 1.38/0.79 % (1529160)Termination phase: Saturation
% 1.38/0.79 % (1529160)Time elapsed: 0.069 s
% 1.38/0.79 % (1529160)Peak memory usage: 14 MB
% 1.38/0.79 % (1529160)Instructions burned: 131 (million)
% 1.38/0.79 % TRYING [1]
% 1.38/0.79 % TRYING [2]
% 1.38/0.79 % (1529205)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3447575994:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 1.38/0.79 % (1529206)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=142237671:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 1.38/0.79 % TRYING [3]
% 1.38/0.79 % (1529207)ott-21_1_sil=16000:fs=off:random_seed=2456765913:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 1.38/0.79 % TRYING [4]
% 1.38/0.79 % (1529205)Instruction limit reached!
% 1.38/0.79 % (1529205)------------------------------
% 1.38/0.79 % (1529205)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.38/0.79 % (1529205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.38/0.79 % (1529205)CaDiCaL version: 2.1.3
% 1.38/0.79 % (1529205)Termination reason: Instruction limit
% 1.38/0.79 % (1529205)Termination phase: Saturation
% 1.38/0.79 % (1529205)Time elapsed: 0.069 s
% 1.38/0.79 % (1529205)Peak memory usage: 14 MB
% 1.38/0.79 % (1529205)Instructions burned: 131 (million)
% 1.38/0.79 % TRYING [4]
% 1.38/0.79 % (1529211)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1518691549:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 1.38/0.79 % (1529207)Instruction limit reached!
% 1.38/0.79 % (1529207)------------------------------
% 1.38/0.79 % (1529207)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.38/0.79 % (1529207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.38/0.79 % (1529207)CaDiCaL version: 2.1.3
% 1.38/0.79 % (1529207)Termination reason: Instruction limit
% 1.38/0.79 % (1529207)Termination phase: Saturation
% 1.38/0.79 % (1529207)Time elapsed: 0.089 s
% 1.38/0.79 % (1529207)Peak memory usage: 13 MB
% 1.38/0.79 % (1529207)Instructions burned: 181 (million)
% 1.38/0.79 % (1529213)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=495727041:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 1.38/0.79 % (1529198)Instruction limit reached!
% 1.38/0.79 % (1529198)------------------------------
% 1.38/0.79 % (1529198)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.38/0.79 % (1529198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.38/0.79 % (1529198)CaDiCaL version: 2.1.3
% 1.38/0.79 % (1529198)Termination reason: Instruction limit
% 1.38/0.79 % (1529198)Termination phase: Finite model building constraint generation
% 1.38/0.79 % (1529198)Time elapsed: 0.144 s
% 1.38/0.79 % (1529198)Peak memory usage: 34 MB
% 1.38/0.79 % (1529198)Instructions burned: 718 (million)
% 1.38/0.79 % (1529215)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=397951925:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 1.38/0.79 % TRYING [1]
% 1.38/0.79 % TRYING [2]
% 1.38/0.79 % (1529156) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1529145-1529156"...
% 1.38/0.79 % (1529156)...printing done.
% 1.38/0.79 % (1529156)Refutation found. Thanks to Tanya!
% 1.38/0.79 % SZS status Theorem for theBenchmark
% 1.38/0.79 % SZS output start Proof for theBenchmark
% See solution above
% 1.38/0.80 % (1529156)------------------------------
% 1.38/0.80 % (1529156)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.38/0.80 % (1529156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.38/0.80 % (1529156)CaDiCaL version: 2.1.3
% 1.38/0.80 % (1529156)Termination reason: Refutation
% 1.38/0.80 % (1529156)Time elapsed: 0.282 s
% 1.38/0.80 % (1529156)Peak memory usage: 18 MB
% 1.38/0.80 % (1529156)Instructions burned: 497 (million)
% 1.38/0.80 % (1529145)Success in time 0.318 s
% 1.38/0.80 % Vampire exiting
%------------------------------------------------------------------------------