%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT369+3 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n014.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:47:25 AM UTC 2026
% Result : Theorem 14.83s 6.19s
% Output : Refutation 31.24s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 33
% Syntax : Number of formulae : 331 ( 55 unt; 15 def)
% Number of atoms : 2025 ( 35 equ)
% Maximal formula atoms : 25 ( 6 avg)
% Number of connectives : 3014 (1320 ~;1341 |; 297 &)
% ( 22 <=>; 34 =>; 0 <=; 0 <~>)
% Maximal formula depth : 28 ( 7 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 53 ( 51 usr; 16 prp; 0-3 aty)
% Number of functors : 10 ( 10 usr; 2 con; 0-3 aty)
% Number of variables : 211 ( 0 sgn 207 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1394,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
<=> m1_relset_1(X2,X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(f6788,axiom,
! [X0] :
( l1_struct_0(X0)
=> k2_pre_topc(X0) = u1_struct_0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d3_pre_topc) ).
fof(f7885,axiom,
! [X0] :
( l1_orders_2(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l1_orders_2) ).
fof(f11561,axiom,
! [X0] :
( l1_orders_2(X0)
=> ( v2_lattice3(X0)
=> ~ v3_struct_0(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc2_lattice3) ).
fof(f14866,axiom,
! [X0] :
( l1_orders_2(X0)
=> ! [X1] :
( m1_yellow_0(X1,X0)
=> l1_orders_2(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m1_yellow_0) ).
fof(f15154,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(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)) )
=> k1_yellow_2(X0,X1,X2) = u1_struct_0(k2_yellow_2(X0,X1,X2)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t11_yellow_2) ).
fof(f15204,axiom,
! [X0,X1,X2] :
( ( ~ v3_struct_0(X0)
& l1_orders_2(X0)
& ~ v3_struct_0(X1)
& l1_orders_2(X1)
& v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> ( v1_orders_2(k2_yellow_2(X0,X1,X2))
& v4_yellow_0(k2_yellow_2(X0,X1,X2),X1)
& m1_yellow_0(k2_yellow_2(X0,X1,X2),X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k2_yellow_2) ).
fof(f15225,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
=> ( ( v1_funct_1(X1)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v7_waybel_1(X1,X0) )
=> ( v1_funct_1(X1)
& ~ v1_xboole_0(X1)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v1_partfun1(X1,u1_struct_0(X0),u1_struct_0(X0))
& v6_waybel_1(X1,X0) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc3_waybel_1) ).
fof(f15232,axiom,
! [X0,X1,X2] :
( ( ~ v3_struct_0(X0)
& l1_orders_2(X0)
& ~ v3_struct_0(X1)
& l1_orders_2(X1)
& v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> ( v1_relat_1(k3_waybel_1(X0,X1,X2))
& v1_funct_1(k3_waybel_1(X0,X1,X2))
& v2_funct_1(k3_waybel_1(X0,X1,X2))
& ~ v1_xboole_0(k3_waybel_1(X0,X1,X2))
& v1_funct_2(k3_waybel_1(X0,X1,X2),u1_struct_0(k2_yellow_2(X0,X1,X2)),u1_struct_0(X1))
& v1_partfun1(k3_waybel_1(X0,X1,X2),u1_struct_0(k2_yellow_2(X0,X1,X2)),u1_struct_0(X1))
& v5_orders_3(k3_waybel_1(X0,X1,X2),k2_yellow_2(X0,X1,X2),X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc7_waybel_1) ).
fof(f15347,axiom,
! [X0,X1,X2] :
( ( ~ v3_struct_0(X0)
& l1_orders_2(X0)
& ~ v3_struct_0(X1)
& l1_orders_2(X1)
& v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> ( v1_funct_1(k3_waybel_1(X0,X1,X2))
& v1_funct_2(k3_waybel_1(X0,X1,X2),u1_struct_0(k2_yellow_2(X0,X1,X2)),u1_struct_0(X1))
& m2_relset_1(k3_waybel_1(X0,X1,X2),u1_struct_0(k2_yellow_2(X0,X1,X2)),u1_struct_0(X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k3_waybel_1) ).
fof(f16583,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& l1_orders_2(X0)
& v1_funct_1(X1)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v7_waybel_1(X1,X0)
& m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
=> ( ~ v3_struct_0(k2_yellow_2(X0,X0,X1))
& v1_orders_2(k2_yellow_2(X0,X0,X1))
& v2_orders_2(k2_yellow_2(X0,X0,X1))
& v3_orders_2(k2_yellow_2(X0,X0,X1))
& v4_orders_2(k2_yellow_2(X0,X0,X1))
& v4_yellow_0(k2_yellow_2(X0,X0,X1),X0)
& v5_yellow_0(k2_yellow_2(X0,X0,X1),X0)
& v7_yellow_0(k2_yellow_2(X0,X0,X1),X0)
& v3_waybel_0(k2_yellow_2(X0,X0,X1),X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc10_waybel10) ).
fof(f16588,axiom,
! [X0,X1] :
( ( v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& v2_lattice3(X0)
& v3_lattice3(X0)
& l1_orders_2(X0)
& v1_funct_1(X1)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v22_waybel_0(X1,X0,X0)
& v7_waybel_1(X1,X0)
& m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
=> ( ~ v3_struct_0(k2_yellow_2(X0,X0,X1))
& v1_orders_2(k2_yellow_2(X0,X0,X1))
& v2_orders_2(k2_yellow_2(X0,X0,X1))
& v3_orders_2(k2_yellow_2(X0,X0,X1))
& v4_orders_2(k2_yellow_2(X0,X0,X1))
& v2_lattice3(k2_yellow_2(X0,X0,X1))
& v4_yellow_0(k2_yellow_2(X0,X0,X1),X0)
& v5_yellow_0(k2_yellow_2(X0,X0,X1),X0)
& v7_yellow_0(k2_yellow_2(X0,X0,X1),X0)
& v3_waybel_0(k2_yellow_2(X0,X0,X1),X0)
& v4_waybel_0(k2_yellow_2(X0,X0,X1),X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc15_waybel10) ).
fof(f16621,axiom,
! [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] :
( ( v1_funct_1(X1)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v7_waybel_1(X1,X0)
& m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
=> ( v22_waybel_0(X1,X0,X0)
<=> v4_waybel_0(k2_yellow_2(X0,X0,X1),X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t26_waybel10) ).
fof(f18948,axiom,
! [X0] :
( ( v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& v2_lattice3(X0)
& v3_lattice3(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( ( v2_orders_2(X1)
& v3_orders_2(X1)
& v4_orders_2(X1)
& v1_lattice3(X1)
& v2_lattice3(X1)
& v3_lattice3(X1)
& l1_orders_2(X1) )
=> ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v17_waybel_0(X2,X0,X1)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> ( v22_waybel_0(X2,X0,X1)
=> v1_waybel34(k1_waybel34(X0,X1,X2),X1,X0) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t24_waybel34) ).
fof(f18959,axiom,
! [X0,X1] :
( ( v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& v2_lattice3(X0)
& v3_lattice3(X0)
& l1_orders_2(X0)
& v1_funct_1(X1)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v6_waybel_1(X1,X0)
& m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
=> ( ~ v3_struct_0(k2_yellow_2(X0,X0,X1))
& v1_orders_2(k2_yellow_2(X0,X0,X1))
& v2_orders_2(k2_yellow_2(X0,X0,X1))
& v3_orders_2(k2_yellow_2(X0,X0,X1))
& v4_orders_2(k2_yellow_2(X0,X0,X1))
& v1_yellow_0(k2_yellow_2(X0,X0,X1))
& v2_yellow_0(k2_yellow_2(X0,X0,X1))
& v3_yellow_0(k2_yellow_2(X0,X0,X1))
& v4_yellow_0(k2_yellow_2(X0,X0,X1),X0)
& v24_waybel_0(k2_yellow_2(X0,X0,X1))
& v25_waybel_0(k2_yellow_2(X0,X0,X1))
& v1_lattice3(k2_yellow_2(X0,X0,X1))
& v2_lattice3(k2_yellow_2(X0,X0,X1))
& v3_lattice3(k2_yellow_2(X0,X0,X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc10_waybel34) ).
fof(f18966,axiom,
! [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] :
( ( v1_funct_1(X1)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v7_waybel_1(X1,X0)
& m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
=> ( v18_waybel_0(k2_waybel_1(X0,X0,X1),X0,k2_yellow_2(X0,X0,X1))
& v17_waybel_0(k3_waybel_1(X0,X0,X1),k2_yellow_2(X0,X0,X1),X0)
& k2_waybel34(k2_yellow_2(X0,X0,X1),X0,k2_waybel_1(X0,X0,X1)) = k3_waybel_1(X0,X0,X1)
& k1_waybel34(k2_yellow_2(X0,X0,X1),X0,k3_waybel_1(X0,X0,X1)) = k2_waybel_1(X0,X0,X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t39_waybel34) ).
fof(f18967,axiom,
! [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] :
( ( v1_funct_1(X1)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v7_waybel_1(X1,X0)
& m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
=> ( v4_waybel_0(k2_yellow_2(X0,X0,X1),X0)
<=> v22_waybel_0(k3_waybel_1(X0,X0,X1),k2_yellow_2(X0,X0,X1),X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t40_waybel34) ).
fof(f18969,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] :
( ( v1_funct_1(X1)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v7_waybel_1(X1,X0)
& m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
=> ( v4_waybel_0(k2_yellow_2(X0,X0,X1),X0)
=> v1_waybel34(k2_waybel_1(X0,X0,X1),X0,k2_yellow_2(X0,X0,X1)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t42_waybel34) ).
fof(f18970,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] :
( ( v1_funct_1(X1)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v7_waybel_1(X1,X0)
& m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
=> ( v4_waybel_0(k2_yellow_2(X0,X0,X1),X0)
=> v1_waybel34(k2_waybel_1(X0,X0,X1),X0,k2_yellow_2(X0,X0,X1)) ) ) ),
inference(negated_conjecture,[status(cth)],[f18969]) ).
fof(f19204,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( v1_waybel34(k1_waybel34(X0,X1,X2),X1,X0)
| ~ v22_waybel_0(X2,X0,X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v17_waybel_0(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ v3_lattice3(X1)
| ~ l1_orders_2(X1) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f18948]) ).
fof(f19205,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( v1_waybel34(k1_waybel34(X0,X1,X2),X1,X0)
| ~ v22_waybel_0(X2,X0,X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v17_waybel_0(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ v3_lattice3(X1)
| ~ l1_orders_2(X1) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f19204]) ).
fof(f19225,plain,
! [X0,X1] :
( ( ~ v3_struct_0(k2_yellow_2(X0,X0,X1))
& v1_orders_2(k2_yellow_2(X0,X0,X1))
& v2_orders_2(k2_yellow_2(X0,X0,X1))
& v3_orders_2(k2_yellow_2(X0,X0,X1))
& v4_orders_2(k2_yellow_2(X0,X0,X1))
& v1_yellow_0(k2_yellow_2(X0,X0,X1))
& v2_yellow_0(k2_yellow_2(X0,X0,X1))
& v3_yellow_0(k2_yellow_2(X0,X0,X1))
& v4_yellow_0(k2_yellow_2(X0,X0,X1),X0)
& v24_waybel_0(k2_yellow_2(X0,X0,X1))
& v25_waybel_0(k2_yellow_2(X0,X0,X1))
& v1_lattice3(k2_yellow_2(X0,X0,X1))
& v2_lattice3(k2_yellow_2(X0,X0,X1))
& v3_lattice3(k2_yellow_2(X0,X0,X1)) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v6_waybel_1(X1,X0)
| ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f18959]) ).
fof(f19226,plain,
! [X0,X1] :
( ( ~ v3_struct_0(k2_yellow_2(X0,X0,X1))
& v1_orders_2(k2_yellow_2(X0,X0,X1))
& v2_orders_2(k2_yellow_2(X0,X0,X1))
& v3_orders_2(k2_yellow_2(X0,X0,X1))
& v4_orders_2(k2_yellow_2(X0,X0,X1))
& v1_yellow_0(k2_yellow_2(X0,X0,X1))
& v2_yellow_0(k2_yellow_2(X0,X0,X1))
& v3_yellow_0(k2_yellow_2(X0,X0,X1))
& v4_yellow_0(k2_yellow_2(X0,X0,X1),X0)
& v24_waybel_0(k2_yellow_2(X0,X0,X1))
& v25_waybel_0(k2_yellow_2(X0,X0,X1))
& v1_lattice3(k2_yellow_2(X0,X0,X1))
& v2_lattice3(k2_yellow_2(X0,X0,X1))
& v3_lattice3(k2_yellow_2(X0,X0,X1)) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v6_waybel_1(X1,X0)
| ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) ),
inference(flattening,[],[f19225]) ).
fof(f19239,plain,
! [X0] :
( ! [X1] :
( ( v18_waybel_0(k2_waybel_1(X0,X0,X1),X0,k2_yellow_2(X0,X0,X1))
& v17_waybel_0(k3_waybel_1(X0,X0,X1),k2_yellow_2(X0,X0,X1),X0)
& k2_waybel34(k2_yellow_2(X0,X0,X1),X0,k2_waybel_1(X0,X0,X1)) = k3_waybel_1(X0,X0,X1)
& k1_waybel34(k2_yellow_2(X0,X0,X1),X0,k3_waybel_1(X0,X0,X1)) = k2_waybel_1(X0,X0,X1) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v7_waybel_1(X1,X0)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f18966]) ).
fof(f19240,plain,
! [X0] :
( ! [X1] :
( ( v18_waybel_0(k2_waybel_1(X0,X0,X1),X0,k2_yellow_2(X0,X0,X1))
& v17_waybel_0(k3_waybel_1(X0,X0,X1),k2_yellow_2(X0,X0,X1),X0)
& k2_waybel34(k2_yellow_2(X0,X0,X1),X0,k2_waybel_1(X0,X0,X1)) = k3_waybel_1(X0,X0,X1)
& k1_waybel34(k2_yellow_2(X0,X0,X1),X0,k3_waybel_1(X0,X0,X1)) = k2_waybel_1(X0,X0,X1) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v7_waybel_1(X1,X0)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f19239]) ).
fof(f19241,plain,
! [X0] :
( ! [X1] :
( ( v4_waybel_0(k2_yellow_2(X0,X0,X1),X0)
<=> v22_waybel_0(k3_waybel_1(X0,X0,X1),k2_yellow_2(X0,X0,X1),X0) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v7_waybel_1(X1,X0)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f18967]) ).
fof(f19242,plain,
! [X0] :
( ! [X1] :
( ( v4_waybel_0(k2_yellow_2(X0,X0,X1),X0)
<=> v22_waybel_0(k3_waybel_1(X0,X0,X1),k2_yellow_2(X0,X0,X1),X0) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v7_waybel_1(X1,X0)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f19241]) ).
fof(f19245,plain,
? [X0] :
( ? [X1] :
( ~ v1_waybel34(k2_waybel_1(X0,X0,X1),X0,k2_yellow_2(X0,X0,X1))
& v4_waybel_0(k2_yellow_2(X0,X0,X1),X0)
& v1_funct_1(X1)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v7_waybel_1(X1,X0)
& m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
& v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& v2_lattice3(X0)
& v3_lattice3(X0)
& l1_orders_2(X0) ),
inference(ennf_transformation,[],[f18970]) ).
fof(f19246,plain,
? [X0] :
( ? [X1] :
( ~ v1_waybel34(k2_waybel_1(X0,X0,X1),X0,k2_yellow_2(X0,X0,X1))
& v4_waybel_0(k2_yellow_2(X0,X0,X1),X0)
& v1_funct_1(X1)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v7_waybel_1(X1,X0)
& m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
& v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& v2_lattice3(X0)
& v3_lattice3(X0)
& l1_orders_2(X0) ),
inference(flattening,[],[f19245]) ).
fof(f19251,plain,
! [X0] :
( ~ v3_struct_0(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f11561]) ).
fof(f19252,plain,
! [X0] :
( ~ v3_struct_0(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f19251]) ).
fof(f20080,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( k1_yellow_2(X0,X1,X2) = u1_struct_0(k2_yellow_2(X0,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_struct_0(X1)
| ~ l1_orders_2(X1) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f15154]) ).
fof(f20081,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( k1_yellow_2(X0,X1,X2) = u1_struct_0(k2_yellow_2(X0,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_struct_0(X1)
| ~ l1_orders_2(X1) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f20080]) ).
fof(f20197,plain,
! [X0,X1,X2] :
( ( v1_orders_2(k2_yellow_2(X0,X1,X2))
& v4_yellow_0(k2_yellow_2(X0,X1,X2),X1)
& m1_yellow_0(k2_yellow_2(X0,X1,X2),X1) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| v3_struct_0(X1)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(ennf_transformation,[],[f15204]) ).
fof(f20198,plain,
! [X0,X1,X2] :
( ( v1_orders_2(k2_yellow_2(X0,X1,X2))
& v4_yellow_0(k2_yellow_2(X0,X1,X2),X1)
& m1_yellow_0(k2_yellow_2(X0,X1,X2),X1) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| v3_struct_0(X1)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(flattening,[],[f20197]) ).
fof(f20299,plain,
! [X0] :
( k2_pre_topc(X0) = u1_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f6788]) ).
fof(f20348,plain,
! [X0] :
( ! [X1] :
( ( v1_funct_1(X1)
& ~ v1_xboole_0(X1)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v1_partfun1(X1,u1_struct_0(X0),u1_struct_0(X0))
& v6_waybel_1(X1,X0) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v7_waybel_1(X1,X0)
| ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f15225]) ).
fof(f20349,plain,
! [X0] :
( ! [X1] :
( ( v1_funct_1(X1)
& ~ v1_xboole_0(X1)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v1_partfun1(X1,u1_struct_0(X0),u1_struct_0(X0))
& v6_waybel_1(X1,X0) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v7_waybel_1(X1,X0)
| ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f20348]) ).
fof(f20394,plain,
! [X0,X1,X2] :
( ( v1_funct_1(k3_waybel_1(X0,X1,X2))
& v1_funct_2(k3_waybel_1(X0,X1,X2),u1_struct_0(k2_yellow_2(X0,X1,X2)),u1_struct_0(X1))
& m2_relset_1(k3_waybel_1(X0,X1,X2),u1_struct_0(k2_yellow_2(X0,X1,X2)),u1_struct_0(X1)) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| v3_struct_0(X1)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(ennf_transformation,[],[f15347]) ).
fof(f20395,plain,
! [X0,X1,X2] :
( ( v1_funct_1(k3_waybel_1(X0,X1,X2))
& v1_funct_2(k3_waybel_1(X0,X1,X2),u1_struct_0(k2_yellow_2(X0,X1,X2)),u1_struct_0(X1))
& m2_relset_1(k3_waybel_1(X0,X1,X2),u1_struct_0(k2_yellow_2(X0,X1,X2)),u1_struct_0(X1)) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| v3_struct_0(X1)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(flattening,[],[f20394]) ).
fof(f20408,plain,
! [X0,X1,X2] :
( ( v1_relat_1(k3_waybel_1(X0,X1,X2))
& v1_funct_1(k3_waybel_1(X0,X1,X2))
& v2_funct_1(k3_waybel_1(X0,X1,X2))
& ~ v1_xboole_0(k3_waybel_1(X0,X1,X2))
& v1_funct_2(k3_waybel_1(X0,X1,X2),u1_struct_0(k2_yellow_2(X0,X1,X2)),u1_struct_0(X1))
& v1_partfun1(k3_waybel_1(X0,X1,X2),u1_struct_0(k2_yellow_2(X0,X1,X2)),u1_struct_0(X1))
& v5_orders_3(k3_waybel_1(X0,X1,X2),k2_yellow_2(X0,X1,X2),X1) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| v3_struct_0(X1)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(ennf_transformation,[],[f15232]) ).
fof(f20409,plain,
! [X0,X1,X2] :
( ( v1_relat_1(k3_waybel_1(X0,X1,X2))
& v1_funct_1(k3_waybel_1(X0,X1,X2))
& v2_funct_1(k3_waybel_1(X0,X1,X2))
& ~ v1_xboole_0(k3_waybel_1(X0,X1,X2))
& v1_funct_2(k3_waybel_1(X0,X1,X2),u1_struct_0(k2_yellow_2(X0,X1,X2)),u1_struct_0(X1))
& v1_partfun1(k3_waybel_1(X0,X1,X2),u1_struct_0(k2_yellow_2(X0,X1,X2)),u1_struct_0(X1))
& v5_orders_3(k3_waybel_1(X0,X1,X2),k2_yellow_2(X0,X1,X2),X1) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| v3_struct_0(X1)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(flattening,[],[f20408]) ).
fof(f20413,plain,
! [X0] :
( ! [X1] :
( l1_orders_2(X1)
| ~ m1_yellow_0(X1,X0) )
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f14866]) ).
fof(f20442,plain,
! [X0] :
( ! [X1] :
( ( v22_waybel_0(X1,X0,X0)
<=> v4_waybel_0(k2_yellow_2(X0,X0,X1),X0) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v7_waybel_1(X1,X0)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f16621]) ).
fof(f20443,plain,
! [X0] :
( ! [X1] :
( ( v22_waybel_0(X1,X0,X0)
<=> v4_waybel_0(k2_yellow_2(X0,X0,X1),X0) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v7_waybel_1(X1,X0)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f20442]) ).
fof(f21175,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f7885]) ).
fof(f26267,plain,
! [X0,X1] :
( ( ~ v3_struct_0(k2_yellow_2(X0,X0,X1))
& v1_orders_2(k2_yellow_2(X0,X0,X1))
& v2_orders_2(k2_yellow_2(X0,X0,X1))
& v3_orders_2(k2_yellow_2(X0,X0,X1))
& v4_orders_2(k2_yellow_2(X0,X0,X1))
& v2_lattice3(k2_yellow_2(X0,X0,X1))
& v4_yellow_0(k2_yellow_2(X0,X0,X1),X0)
& v5_yellow_0(k2_yellow_2(X0,X0,X1),X0)
& v7_yellow_0(k2_yellow_2(X0,X0,X1),X0)
& v3_waybel_0(k2_yellow_2(X0,X0,X1),X0)
& v4_waybel_0(k2_yellow_2(X0,X0,X1),X0) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v22_waybel_0(X1,X0,X0)
| ~ v7_waybel_1(X1,X0)
| ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f16588]) ).
fof(f26268,plain,
! [X0,X1] :
( ( ~ v3_struct_0(k2_yellow_2(X0,X0,X1))
& v1_orders_2(k2_yellow_2(X0,X0,X1))
& v2_orders_2(k2_yellow_2(X0,X0,X1))
& v3_orders_2(k2_yellow_2(X0,X0,X1))
& v4_orders_2(k2_yellow_2(X0,X0,X1))
& v2_lattice3(k2_yellow_2(X0,X0,X1))
& v4_yellow_0(k2_yellow_2(X0,X0,X1),X0)
& v5_yellow_0(k2_yellow_2(X0,X0,X1),X0)
& v7_yellow_0(k2_yellow_2(X0,X0,X1),X0)
& v3_waybel_0(k2_yellow_2(X0,X0,X1),X0)
& v4_waybel_0(k2_yellow_2(X0,X0,X1),X0) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v22_waybel_0(X1,X0,X0)
| ~ v7_waybel_1(X1,X0)
| ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) ),
inference(flattening,[],[f26267]) ).
fof(f26269,plain,
! [X0,X1] :
( ( ~ v3_struct_0(k2_yellow_2(X0,X0,X1))
& v1_orders_2(k2_yellow_2(X0,X0,X1))
& v2_orders_2(k2_yellow_2(X0,X0,X1))
& v3_orders_2(k2_yellow_2(X0,X0,X1))
& v4_orders_2(k2_yellow_2(X0,X0,X1))
& v4_yellow_0(k2_yellow_2(X0,X0,X1),X0)
& v5_yellow_0(k2_yellow_2(X0,X0,X1),X0)
& v7_yellow_0(k2_yellow_2(X0,X0,X1),X0)
& v3_waybel_0(k2_yellow_2(X0,X0,X1),X0) )
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v7_waybel_1(X1,X0)
| ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f16583]) ).
fof(f26270,plain,
! [X0,X1] :
( ( ~ v3_struct_0(k2_yellow_2(X0,X0,X1))
& v1_orders_2(k2_yellow_2(X0,X0,X1))
& v2_orders_2(k2_yellow_2(X0,X0,X1))
& v3_orders_2(k2_yellow_2(X0,X0,X1))
& v4_orders_2(k2_yellow_2(X0,X0,X1))
& v4_yellow_0(k2_yellow_2(X0,X0,X1),X0)
& v5_yellow_0(k2_yellow_2(X0,X0,X1),X0)
& v7_yellow_0(k2_yellow_2(X0,X0,X1),X0)
& v3_waybel_0(k2_yellow_2(X0,X0,X1),X0) )
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v7_waybel_1(X1,X0)
| ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) ),
inference(flattening,[],[f26269]) ).
fof(f29865,plain,
! [X0] :
( ! [X1] :
( ( ( v4_waybel_0(k2_yellow_2(X0,X0,X1),X0)
| ~ v22_waybel_0(k3_waybel_1(X0,X0,X1),k2_yellow_2(X0,X0,X1),X0) )
& ( v22_waybel_0(k3_waybel_1(X0,X0,X1),k2_yellow_2(X0,X0,X1),X0)
| ~ v4_waybel_0(k2_yellow_2(X0,X0,X1),X0) ) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v7_waybel_1(X1,X0)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(nnf_transformation,[],[f19242]) ).
fof(f29869,plain,
( ~ v1_waybel34(k2_waybel_1(sK184,sK184,sK185),sK184,k2_yellow_2(sK184,sK184,sK185))
& v4_waybel_0(k2_yellow_2(sK184,sK184,sK185),sK184)
& v1_funct_1(sK185)
& v1_funct_2(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
& v7_waybel_1(sK185,sK184)
& m2_relset_1(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
& v2_orders_2(sK184)
& v3_orders_2(sK184)
& v4_orders_2(sK184)
& v1_lattice3(sK184)
& v2_lattice3(sK184)
& v3_lattice3(sK184)
& l1_orders_2(sK184) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK184,sK185]),skolemize(X0,sK184),skolemize(X1,sK185)],[f19246]) ).
fof(f29873,plain,
! [X0,X1,X2] :
( ( m2_relset_1(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1) )
& ( m1_relset_1(X2,X0,X1)
| ~ m2_relset_1(X2,X0,X1) ) ),
inference(nnf_transformation,[],[f1394]) ).
fof(f30324,plain,
! [X0] :
( ! [X1] :
( ( ( v22_waybel_0(X1,X0,X0)
| ~ v4_waybel_0(k2_yellow_2(X0,X0,X1),X0) )
& ( v4_waybel_0(k2_yellow_2(X0,X0,X1),X0)
| ~ v22_waybel_0(X1,X0,X0) ) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v7_waybel_1(X1,X0)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(nnf_transformation,[],[f20443]) ).
fof(f33951,plain,
! [X2,X0,X1] :
( v1_waybel34(k1_waybel34(X0,X1,X2),X1,X0)
| ~ v22_waybel_0(X2,X0,X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v17_waybel_0(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ v3_lattice3(X1)
| ~ l1_orders_2(X1)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f19205]) ).
fof(f33983,plain,
! [X0,X1] :
( ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v6_waybel_1(X1,X0)
| v3_lattice3(k2_yellow_2(X0,X0,X1)) ),
inference(cnf_transformation,[],[f19226]) ).
fof(f33985,plain,
! [X0,X1] :
( ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v6_waybel_1(X1,X0)
| v1_lattice3(k2_yellow_2(X0,X0,X1)) ),
inference(cnf_transformation,[],[f19226]) ).
fof(f34024,plain,
! [X0,X1] :
( ~ v3_lattice3(X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v7_waybel_1(X1,X0)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| k2_waybel_1(X0,X0,X1) = k1_waybel34(k2_yellow_2(X0,X0,X1),X0,k3_waybel_1(X0,X0,X1))
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f19240]) ).
fof(f34026,plain,
! [X0,X1] :
( v17_waybel_0(k3_waybel_1(X0,X0,X1),k2_yellow_2(X0,X0,X1),X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v7_waybel_1(X1,X0)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f19240]) ).
fof(f34028,plain,
! [X0,X1] :
( v22_waybel_0(k3_waybel_1(X0,X0,X1),k2_yellow_2(X0,X0,X1),X0)
| ~ v4_waybel_0(k2_yellow_2(X0,X0,X1),X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v7_waybel_1(X1,X0)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f29865]) ).
fof(f34040,plain,
l1_orders_2(sK184),
inference(cnf_transformation,[],[f29869]) ).
fof(f34041,plain,
v3_lattice3(sK184),
inference(cnf_transformation,[],[f29869]) ).
fof(f34042,plain,
v2_lattice3(sK184),
inference(cnf_transformation,[],[f29869]) ).
fof(f34043,plain,
v1_lattice3(sK184),
inference(cnf_transformation,[],[f29869]) ).
fof(f34044,plain,
v4_orders_2(sK184),
inference(cnf_transformation,[],[f29869]) ).
fof(f34045,plain,
v3_orders_2(sK184),
inference(cnf_transformation,[],[f29869]) ).
fof(f34046,plain,
v2_orders_2(sK184),
inference(cnf_transformation,[],[f29869]) ).
fof(f34047,plain,
m2_relset_1(sK185,u1_struct_0(sK184),u1_struct_0(sK184)),
inference(cnf_transformation,[],[f29869]) ).
fof(f34048,plain,
v7_waybel_1(sK185,sK184),
inference(cnf_transformation,[],[f29869]) ).
fof(f34049,plain,
v1_funct_2(sK185,u1_struct_0(sK184),u1_struct_0(sK184)),
inference(cnf_transformation,[],[f29869]) ).
fof(f34050,plain,
v1_funct_1(sK185),
inference(cnf_transformation,[],[f29869]) ).
fof(f34051,plain,
v4_waybel_0(k2_yellow_2(sK184,sK184,sK185),sK184),
inference(cnf_transformation,[],[f29869]) ).
fof(f34052,plain,
~ v1_waybel34(k2_waybel_1(sK184,sK184,sK185),sK184,k2_yellow_2(sK184,sK184,sK185)),
inference(cnf_transformation,[],[f29869]) ).
fof(f34064,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f29873]) ).
fof(f34072,plain,
! [X0] :
( ~ v2_lattice3(X0)
| ~ v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f19252]) ).
fof(f35800,plain,
! [X2,X0,X1] :
( ~ l1_orders_2(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)
| ~ l1_orders_2(X1)
| v3_struct_0(X0)
| k1_yellow_2(X0,X1,X2) = u1_struct_0(k2_yellow_2(X0,X1,X2)) ),
inference(cnf_transformation,[],[f20081]) ).
fof(f36017,plain,
! [X2,X0,X1] :
( ~ l1_orders_2(X1)
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| v3_struct_0(X1)
| m1_yellow_0(k2_yellow_2(X0,X1,X2),X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f20198]) ).
fof(f36123,plain,
! [X0] :
( ~ l1_struct_0(X0)
| u1_struct_0(X0) = k2_pre_topc(X0) ),
inference(cnf_transformation,[],[f20299]) ).
fof(f36245,plain,
! [X0,X1] :
( ~ l1_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v7_waybel_1(X1,X0)
| ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| v6_waybel_1(X1,X0) ),
inference(cnf_transformation,[],[f20349]) ).
fof(f36342,plain,
! [X2,X0,X1] :
( m2_relset_1(k3_waybel_1(X0,X1,X2),u1_struct_0(k2_yellow_2(X0,X1,X2)),u1_struct_0(X1))
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| v3_struct_0(X1)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f20395]) ).
fof(f36353,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| v3_struct_0(X1)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| v1_funct_2(k3_waybel_1(X0,X1,X2),u1_struct_0(k2_yellow_2(X0,X1,X2)),u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f20409]) ).
fof(f36356,plain,
! [X2,X0,X1] :
( ~ l1_orders_2(X1)
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| v3_struct_0(X1)
| v1_funct_1(k3_waybel_1(X0,X1,X2))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f20409]) ).
fof(f36361,plain,
! [X0,X1] :
( ~ l1_orders_2(X0)
| ~ m1_yellow_0(X1,X0)
| l1_orders_2(X1) ),
inference(cnf_transformation,[],[f20413]) ).
fof(f36397,plain,
! [X0,X1] :
( ~ v3_lattice3(X0)
| ~ v4_waybel_0(k2_yellow_2(X0,X0,X1),X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v7_waybel_1(X1,X0)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| v22_waybel_0(X1,X0,X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f30324]) ).
fof(f37630,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f21175]) ).
fof(f46193,plain,
! [X0,X1] :
( ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v22_waybel_0(X1,X0,X0)
| ~ v7_waybel_1(X1,X0)
| v2_lattice3(k2_yellow_2(X0,X0,X1)) ),
inference(cnf_transformation,[],[f26268]) ).
fof(f46203,plain,
! [X0,X1] :
( ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v7_waybel_1(X1,X0)
| v4_orders_2(k2_yellow_2(X0,X0,X1)) ),
inference(cnf_transformation,[],[f26270]) ).
fof(f46204,plain,
! [X0,X1] :
( ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v7_waybel_1(X1,X0)
| v3_orders_2(k2_yellow_2(X0,X0,X1)) ),
inference(cnf_transformation,[],[f26270]) ).
fof(f46205,plain,
! [X0,X1] :
( ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v7_waybel_1(X1,X0)
| v2_orders_2(k2_yellow_2(X0,X0,X1)) ),
inference(cnf_transformation,[],[f26270]) ).
fof(f61828,definition,
( spl2594_478
<=> v3_struct_0(sK184) ),
introduced(definition,[new_symbols(definition,[spl2594_478])],[avatar_definition]) ).
fof(f61829,plain,
( v3_struct_0(sK184)
| ~ spl2594_478 ),
inference(avatar_component_clause,[],[f61828]) ).
fof(f61831,plain,
! [X0,X1] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK184),u1_struct_0(X1))
| ~ m2_relset_1(X0,u1_struct_0(sK184),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ l1_orders_2(X1)
| v3_struct_0(sK184)
| k1_yellow_2(sK184,X1,X0) = u1_struct_0(k2_yellow_2(sK184,X1,X0)) ),
inference(resolution,[],[f35800,f34040]) ).
fof(f61833,definition,
( spl2594_479
<=> ! [X0,X1] :
( ~ v1_funct_1(X0)
| k1_yellow_2(sK184,X1,X0) = u1_struct_0(k2_yellow_2(sK184,X1,X0))
| ~ l1_orders_2(X1)
| v3_struct_0(X1)
| ~ m2_relset_1(X0,u1_struct_0(sK184),u1_struct_0(X1))
| ~ v1_funct_2(X0,u1_struct_0(sK184),u1_struct_0(X1)) ) ),
introduced(definition,[new_symbols(definition,[spl2594_479])],[avatar_definition]) ).
fof(f61834,plain,
( ! [X0,X1] :
( ~ l1_orders_2(X1)
| k1_yellow_2(sK184,X1,X0) = u1_struct_0(k2_yellow_2(sK184,X1,X0))
| ~ v1_funct_1(X0)
| v3_struct_0(X1)
| ~ m2_relset_1(X0,u1_struct_0(sK184),u1_struct_0(X1))
| ~ v1_funct_2(X0,u1_struct_0(sK184),u1_struct_0(X1)) )
| ~ spl2594_479 ),
inference(avatar_component_clause,[],[f61833]) ).
fof(f61835,plain,
( spl2594_478
| spl2594_479 ),
inference(avatar_split_clause,[],[f61831,f61833,f61828]) ).
fof(f61839,plain,
! [X0] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v7_waybel_1(X0,sK184)
| ~ m2_relset_1(X0,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v2_orders_2(sK184)
| ~ v3_orders_2(sK184)
| ~ v4_orders_2(sK184)
| ~ v1_lattice3(sK184)
| ~ v2_lattice3(sK184)
| k2_waybel_1(sK184,sK184,X0) = k1_waybel34(k2_yellow_2(sK184,sK184,X0),sK184,k3_waybel_1(sK184,sK184,X0))
| ~ l1_orders_2(sK184) ),
inference(resolution,[],[f34024,f34041]) ).
fof(f61840,plain,
! [X0] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v7_waybel_1(X0,sK184)
| ~ m2_relset_1(X0,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v3_orders_2(sK184)
| ~ v4_orders_2(sK184)
| ~ v1_lattice3(sK184)
| ~ v2_lattice3(sK184)
| k2_waybel_1(sK184,sK184,X0) = k1_waybel34(k2_yellow_2(sK184,sK184,X0),sK184,k3_waybel_1(sK184,sK184,X0))
| ~ l1_orders_2(sK184) ),
inference(forward_subsumption_resolution,[],[f61839,f34046]) ).
fof(f61841,plain,
! [X0] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v7_waybel_1(X0,sK184)
| ~ m2_relset_1(X0,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v4_orders_2(sK184)
| ~ v1_lattice3(sK184)
| ~ v2_lattice3(sK184)
| k2_waybel_1(sK184,sK184,X0) = k1_waybel34(k2_yellow_2(sK184,sK184,X0),sK184,k3_waybel_1(sK184,sK184,X0))
| ~ l1_orders_2(sK184) ),
inference(forward_subsumption_resolution,[],[f61840,f34045]) ).
fof(f61842,plain,
! [X0] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v7_waybel_1(X0,sK184)
| ~ m2_relset_1(X0,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v1_lattice3(sK184)
| ~ v2_lattice3(sK184)
| k2_waybel_1(sK184,sK184,X0) = k1_waybel34(k2_yellow_2(sK184,sK184,X0),sK184,k3_waybel_1(sK184,sK184,X0))
| ~ l1_orders_2(sK184) ),
inference(forward_subsumption_resolution,[],[f61841,f34044]) ).
fof(f61843,plain,
! [X0] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v7_waybel_1(X0,sK184)
| ~ m2_relset_1(X0,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v2_lattice3(sK184)
| k2_waybel_1(sK184,sK184,X0) = k1_waybel34(k2_yellow_2(sK184,sK184,X0),sK184,k3_waybel_1(sK184,sK184,X0))
| ~ l1_orders_2(sK184) ),
inference(forward_subsumption_resolution,[],[f61842,f34043]) ).
fof(f61844,plain,
! [X0] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v7_waybel_1(X0,sK184)
| ~ m2_relset_1(X0,u1_struct_0(sK184),u1_struct_0(sK184))
| k2_waybel_1(sK184,sK184,X0) = k1_waybel34(k2_yellow_2(sK184,sK184,X0),sK184,k3_waybel_1(sK184,sK184,X0))
| ~ l1_orders_2(sK184) ),
inference(forward_subsumption_resolution,[],[f61843,f34042]) ).
fof(f61845,plain,
! [X0] :
( ~ v7_waybel_1(X0,sK184)
| ~ v1_funct_2(X0,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v1_funct_1(X0)
| ~ m2_relset_1(X0,u1_struct_0(sK184),u1_struct_0(sK184))
| k2_waybel_1(sK184,sK184,X0) = k1_waybel34(k2_yellow_2(sK184,sK184,X0),sK184,k3_waybel_1(sK184,sK184,X0)) ),
inference(forward_subsumption_resolution,[],[f61844,f34040]) ).
fof(f61847,plain,
! [X0] :
( ~ v4_waybel_0(k2_yellow_2(sK184,sK184,X0),sK184)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v7_waybel_1(X0,sK184)
| ~ m2_relset_1(X0,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v2_orders_2(sK184)
| ~ v3_orders_2(sK184)
| ~ v4_orders_2(sK184)
| ~ v1_lattice3(sK184)
| ~ v2_lattice3(sK184)
| v22_waybel_0(X0,sK184,sK184)
| ~ l1_orders_2(sK184) ),
inference(resolution,[],[f36397,f34041]) ).
fof(f61848,plain,
! [X0] :
( ~ v4_waybel_0(k2_yellow_2(sK184,sK184,X0),sK184)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v7_waybel_1(X0,sK184)
| ~ m2_relset_1(X0,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v3_orders_2(sK184)
| ~ v4_orders_2(sK184)
| ~ v1_lattice3(sK184)
| ~ v2_lattice3(sK184)
| v22_waybel_0(X0,sK184,sK184)
| ~ l1_orders_2(sK184) ),
inference(forward_subsumption_resolution,[],[f61847,f34046]) ).
fof(f61849,plain,
! [X0] :
( ~ v4_waybel_0(k2_yellow_2(sK184,sK184,X0),sK184)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v7_waybel_1(X0,sK184)
| ~ m2_relset_1(X0,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v4_orders_2(sK184)
| ~ v1_lattice3(sK184)
| ~ v2_lattice3(sK184)
| v22_waybel_0(X0,sK184,sK184)
| ~ l1_orders_2(sK184) ),
inference(forward_subsumption_resolution,[],[f61848,f34045]) ).
fof(f61850,plain,
! [X0] :
( ~ v4_waybel_0(k2_yellow_2(sK184,sK184,X0),sK184)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v7_waybel_1(X0,sK184)
| ~ m2_relset_1(X0,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v1_lattice3(sK184)
| ~ v2_lattice3(sK184)
| v22_waybel_0(X0,sK184,sK184)
| ~ l1_orders_2(sK184) ),
inference(forward_subsumption_resolution,[],[f61849,f34044]) ).
fof(f61851,plain,
! [X0] :
( ~ v4_waybel_0(k2_yellow_2(sK184,sK184,X0),sK184)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v7_waybel_1(X0,sK184)
| ~ m2_relset_1(X0,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v2_lattice3(sK184)
| v22_waybel_0(X0,sK184,sK184)
| ~ l1_orders_2(sK184) ),
inference(forward_subsumption_resolution,[],[f61850,f34043]) ).
fof(f61852,plain,
! [X0] :
( ~ v4_waybel_0(k2_yellow_2(sK184,sK184,X0),sK184)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v7_waybel_1(X0,sK184)
| ~ m2_relset_1(X0,u1_struct_0(sK184),u1_struct_0(sK184))
| v22_waybel_0(X0,sK184,sK184)
| ~ l1_orders_2(sK184) ),
inference(forward_subsumption_resolution,[],[f61851,f34042]) ).
fof(f61853,plain,
! [X0] :
( ~ v7_waybel_1(X0,sK184)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v4_waybel_0(k2_yellow_2(sK184,sK184,X0),sK184)
| ~ m2_relset_1(X0,u1_struct_0(sK184),u1_struct_0(sK184))
| v22_waybel_0(X0,sK184,sK184) ),
inference(forward_subsumption_resolution,[],[f61852,f34040]) ).
fof(f61854,plain,
( ~ v1_funct_2(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v1_funct_1(sK185)
| ~ m2_relset_1(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| k2_waybel_1(sK184,sK184,sK185) = k1_waybel34(k2_yellow_2(sK184,sK184,sK185),sK184,k3_waybel_1(sK184,sK184,sK185)) ),
inference(resolution,[],[f61845,f34048]) ).
fof(f61855,plain,
( ~ v1_funct_1(sK185)
| ~ m2_relset_1(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| k2_waybel_1(sK184,sK184,sK185) = k1_waybel34(k2_yellow_2(sK184,sK184,sK185),sK184,k3_waybel_1(sK184,sK184,sK185)) ),
inference(forward_subsumption_resolution,[],[f61854,f34049]) ).
fof(f61856,plain,
( ~ m2_relset_1(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| k2_waybel_1(sK184,sK184,sK185) = k1_waybel34(k2_yellow_2(sK184,sK184,sK185),sK184,k3_waybel_1(sK184,sK184,sK185)) ),
inference(forward_subsumption_resolution,[],[f61855,f34050]) ).
fof(f61857,plain,
k2_waybel_1(sK184,sK184,sK185) = k1_waybel34(k2_yellow_2(sK184,sK184,sK185),sK184,k3_waybel_1(sK184,sK184,sK185)),
inference(forward_subsumption_resolution,[],[f61856,f34047]) ).
fof(f61858,plain,
( v1_waybel34(k2_waybel_1(sK184,sK184,sK185),sK184,k2_yellow_2(sK184,sK184,sK185))
| ~ v22_waybel_0(k3_waybel_1(sK184,sK184,sK185),k2_yellow_2(sK184,sK184,sK185),sK184)
| ~ v1_funct_1(k3_waybel_1(sK184,sK184,sK185))
| ~ v1_funct_2(k3_waybel_1(sK184,sK184,sK185),u1_struct_0(k2_yellow_2(sK184,sK184,sK185)),u1_struct_0(sK184))
| ~ v17_waybel_0(k3_waybel_1(sK184,sK184,sK185),k2_yellow_2(sK184,sK184,sK185),sK184)
| ~ m2_relset_1(k3_waybel_1(sK184,sK184,sK185),u1_struct_0(k2_yellow_2(sK184,sK184,sK185)),u1_struct_0(sK184))
| ~ v2_orders_2(sK184)
| ~ v3_orders_2(sK184)
| ~ v4_orders_2(sK184)
| ~ v1_lattice3(sK184)
| ~ v2_lattice3(sK184)
| ~ v3_lattice3(sK184)
| ~ l1_orders_2(sK184)
| ~ v2_orders_2(k2_yellow_2(sK184,sK184,sK185))
| ~ v3_orders_2(k2_yellow_2(sK184,sK184,sK185))
| ~ v4_orders_2(k2_yellow_2(sK184,sK184,sK185))
| ~ v1_lattice3(k2_yellow_2(sK184,sK184,sK185))
| ~ v2_lattice3(k2_yellow_2(sK184,sK184,sK185))
| ~ v3_lattice3(k2_yellow_2(sK184,sK184,sK185))
| ~ l1_orders_2(k2_yellow_2(sK184,sK184,sK185)) ),
inference(superposition,[],[f33951,f61857]) ).
fof(f61859,plain,
( ~ v22_waybel_0(k3_waybel_1(sK184,sK184,sK185),k2_yellow_2(sK184,sK184,sK185),sK184)
| ~ v1_funct_1(k3_waybel_1(sK184,sK184,sK185))
| ~ v1_funct_2(k3_waybel_1(sK184,sK184,sK185),u1_struct_0(k2_yellow_2(sK184,sK184,sK185)),u1_struct_0(sK184))
| ~ v17_waybel_0(k3_waybel_1(sK184,sK184,sK185),k2_yellow_2(sK184,sK184,sK185),sK184)
| ~ m2_relset_1(k3_waybel_1(sK184,sK184,sK185),u1_struct_0(k2_yellow_2(sK184,sK184,sK185)),u1_struct_0(sK184))
| ~ v2_orders_2(sK184)
| ~ v3_orders_2(sK184)
| ~ v4_orders_2(sK184)
| ~ v1_lattice3(sK184)
| ~ v2_lattice3(sK184)
| ~ v3_lattice3(sK184)
| ~ l1_orders_2(sK184)
| ~ v2_orders_2(k2_yellow_2(sK184,sK184,sK185))
| ~ v3_orders_2(k2_yellow_2(sK184,sK184,sK185))
| ~ v4_orders_2(k2_yellow_2(sK184,sK184,sK185))
| ~ v1_lattice3(k2_yellow_2(sK184,sK184,sK185))
| ~ v2_lattice3(k2_yellow_2(sK184,sK184,sK185))
| ~ v3_lattice3(k2_yellow_2(sK184,sK184,sK185))
| ~ l1_orders_2(k2_yellow_2(sK184,sK184,sK185)) ),
inference(forward_subsumption_resolution,[],[f61858,f34052]) ).
fof(f61860,plain,
( ~ v22_waybel_0(k3_waybel_1(sK184,sK184,sK185),k2_yellow_2(sK184,sK184,sK185),sK184)
| ~ v1_funct_1(k3_waybel_1(sK184,sK184,sK185))
| ~ v1_funct_2(k3_waybel_1(sK184,sK184,sK185),u1_struct_0(k2_yellow_2(sK184,sK184,sK185)),u1_struct_0(sK184))
| ~ v17_waybel_0(k3_waybel_1(sK184,sK184,sK185),k2_yellow_2(sK184,sK184,sK185),sK184)
| ~ m2_relset_1(k3_waybel_1(sK184,sK184,sK185),u1_struct_0(k2_yellow_2(sK184,sK184,sK185)),u1_struct_0(sK184))
| ~ v3_orders_2(sK184)
| ~ v4_orders_2(sK184)
| ~ v1_lattice3(sK184)
| ~ v2_lattice3(sK184)
| ~ v3_lattice3(sK184)
| ~ l1_orders_2(sK184)
| ~ v2_orders_2(k2_yellow_2(sK184,sK184,sK185))
| ~ v3_orders_2(k2_yellow_2(sK184,sK184,sK185))
| ~ v4_orders_2(k2_yellow_2(sK184,sK184,sK185))
| ~ v1_lattice3(k2_yellow_2(sK184,sK184,sK185))
| ~ v2_lattice3(k2_yellow_2(sK184,sK184,sK185))
| ~ v3_lattice3(k2_yellow_2(sK184,sK184,sK185))
| ~ l1_orders_2(k2_yellow_2(sK184,sK184,sK185)) ),
inference(forward_subsumption_resolution,[],[f61859,f34046]) ).
fof(f61861,plain,
( ~ v22_waybel_0(k3_waybel_1(sK184,sK184,sK185),k2_yellow_2(sK184,sK184,sK185),sK184)
| ~ v1_funct_1(k3_waybel_1(sK184,sK184,sK185))
| ~ v1_funct_2(k3_waybel_1(sK184,sK184,sK185),u1_struct_0(k2_yellow_2(sK184,sK184,sK185)),u1_struct_0(sK184))
| ~ v17_waybel_0(k3_waybel_1(sK184,sK184,sK185),k2_yellow_2(sK184,sK184,sK185),sK184)
| ~ m2_relset_1(k3_waybel_1(sK184,sK184,sK185),u1_struct_0(k2_yellow_2(sK184,sK184,sK185)),u1_struct_0(sK184))
| ~ v4_orders_2(sK184)
| ~ v1_lattice3(sK184)
| ~ v2_lattice3(sK184)
| ~ v3_lattice3(sK184)
| ~ l1_orders_2(sK184)
| ~ v2_orders_2(k2_yellow_2(sK184,sK184,sK185))
| ~ v3_orders_2(k2_yellow_2(sK184,sK184,sK185))
| ~ v4_orders_2(k2_yellow_2(sK184,sK184,sK185))
| ~ v1_lattice3(k2_yellow_2(sK184,sK184,sK185))
| ~ v2_lattice3(k2_yellow_2(sK184,sK184,sK185))
| ~ v3_lattice3(k2_yellow_2(sK184,sK184,sK185))
| ~ l1_orders_2(k2_yellow_2(sK184,sK184,sK185)) ),
inference(forward_subsumption_resolution,[],[f61860,f34045]) ).
fof(f61862,plain,
( ~ v22_waybel_0(k3_waybel_1(sK184,sK184,sK185),k2_yellow_2(sK184,sK184,sK185),sK184)
| ~ v1_funct_1(k3_waybel_1(sK184,sK184,sK185))
| ~ v1_funct_2(k3_waybel_1(sK184,sK184,sK185),u1_struct_0(k2_yellow_2(sK184,sK184,sK185)),u1_struct_0(sK184))
| ~ v17_waybel_0(k3_waybel_1(sK184,sK184,sK185),k2_yellow_2(sK184,sK184,sK185),sK184)
| ~ m2_relset_1(k3_waybel_1(sK184,sK184,sK185),u1_struct_0(k2_yellow_2(sK184,sK184,sK185)),u1_struct_0(sK184))
| ~ v1_lattice3(sK184)
| ~ v2_lattice3(sK184)
| ~ v3_lattice3(sK184)
| ~ l1_orders_2(sK184)
| ~ v2_orders_2(k2_yellow_2(sK184,sK184,sK185))
| ~ v3_orders_2(k2_yellow_2(sK184,sK184,sK185))
| ~ v4_orders_2(k2_yellow_2(sK184,sK184,sK185))
| ~ v1_lattice3(k2_yellow_2(sK184,sK184,sK185))
| ~ v2_lattice3(k2_yellow_2(sK184,sK184,sK185))
| ~ v3_lattice3(k2_yellow_2(sK184,sK184,sK185))
| ~ l1_orders_2(k2_yellow_2(sK184,sK184,sK185)) ),
inference(forward_subsumption_resolution,[],[f61861,f34044]) ).
fof(f61863,plain,
( ~ v22_waybel_0(k3_waybel_1(sK184,sK184,sK185),k2_yellow_2(sK184,sK184,sK185),sK184)
| ~ v1_funct_1(k3_waybel_1(sK184,sK184,sK185))
| ~ v1_funct_2(k3_waybel_1(sK184,sK184,sK185),u1_struct_0(k2_yellow_2(sK184,sK184,sK185)),u1_struct_0(sK184))
| ~ v17_waybel_0(k3_waybel_1(sK184,sK184,sK185),k2_yellow_2(sK184,sK184,sK185),sK184)
| ~ m2_relset_1(k3_waybel_1(sK184,sK184,sK185),u1_struct_0(k2_yellow_2(sK184,sK184,sK185)),u1_struct_0(sK184))
| ~ v2_lattice3(sK184)
| ~ v3_lattice3(sK184)
| ~ l1_orders_2(sK184)
| ~ v2_orders_2(k2_yellow_2(sK184,sK184,sK185))
| ~ v3_orders_2(k2_yellow_2(sK184,sK184,sK185))
| ~ v4_orders_2(k2_yellow_2(sK184,sK184,sK185))
| ~ v1_lattice3(k2_yellow_2(sK184,sK184,sK185))
| ~ v2_lattice3(k2_yellow_2(sK184,sK184,sK185))
| ~ v3_lattice3(k2_yellow_2(sK184,sK184,sK185))
| ~ l1_orders_2(k2_yellow_2(sK184,sK184,sK185)) ),
inference(forward_subsumption_resolution,[],[f61862,f34043]) ).
fof(f61864,plain,
( ~ v22_waybel_0(k3_waybel_1(sK184,sK184,sK185),k2_yellow_2(sK184,sK184,sK185),sK184)
| ~ v1_funct_1(k3_waybel_1(sK184,sK184,sK185))
| ~ v1_funct_2(k3_waybel_1(sK184,sK184,sK185),u1_struct_0(k2_yellow_2(sK184,sK184,sK185)),u1_struct_0(sK184))
| ~ v17_waybel_0(k3_waybel_1(sK184,sK184,sK185),k2_yellow_2(sK184,sK184,sK185),sK184)
| ~ m2_relset_1(k3_waybel_1(sK184,sK184,sK185),u1_struct_0(k2_yellow_2(sK184,sK184,sK185)),u1_struct_0(sK184))
| ~ v3_lattice3(sK184)
| ~ l1_orders_2(sK184)
| ~ v2_orders_2(k2_yellow_2(sK184,sK184,sK185))
| ~ v3_orders_2(k2_yellow_2(sK184,sK184,sK185))
| ~ v4_orders_2(k2_yellow_2(sK184,sK184,sK185))
| ~ v1_lattice3(k2_yellow_2(sK184,sK184,sK185))
| ~ v2_lattice3(k2_yellow_2(sK184,sK184,sK185))
| ~ v3_lattice3(k2_yellow_2(sK184,sK184,sK185))
| ~ l1_orders_2(k2_yellow_2(sK184,sK184,sK185)) ),
inference(forward_subsumption_resolution,[],[f61863,f34042]) ).
fof(f61865,plain,
( ~ v22_waybel_0(k3_waybel_1(sK184,sK184,sK185),k2_yellow_2(sK184,sK184,sK185),sK184)
| ~ v1_funct_1(k3_waybel_1(sK184,sK184,sK185))
| ~ v1_funct_2(k3_waybel_1(sK184,sK184,sK185),u1_struct_0(k2_yellow_2(sK184,sK184,sK185)),u1_struct_0(sK184))
| ~ v17_waybel_0(k3_waybel_1(sK184,sK184,sK185),k2_yellow_2(sK184,sK184,sK185),sK184)
| ~ m2_relset_1(k3_waybel_1(sK184,sK184,sK185),u1_struct_0(k2_yellow_2(sK184,sK184,sK185)),u1_struct_0(sK184))
| ~ l1_orders_2(sK184)
| ~ v2_orders_2(k2_yellow_2(sK184,sK184,sK185))
| ~ v3_orders_2(k2_yellow_2(sK184,sK184,sK185))
| ~ v4_orders_2(k2_yellow_2(sK184,sK184,sK185))
| ~ v1_lattice3(k2_yellow_2(sK184,sK184,sK185))
| ~ v2_lattice3(k2_yellow_2(sK184,sK184,sK185))
| ~ v3_lattice3(k2_yellow_2(sK184,sK184,sK185))
| ~ l1_orders_2(k2_yellow_2(sK184,sK184,sK185)) ),
inference(forward_subsumption_resolution,[],[f61864,f34041]) ).
fof(f61866,plain,
( ~ v22_waybel_0(k3_waybel_1(sK184,sK184,sK185),k2_yellow_2(sK184,sK184,sK185),sK184)
| ~ v1_funct_1(k3_waybel_1(sK184,sK184,sK185))
| ~ v1_funct_2(k3_waybel_1(sK184,sK184,sK185),u1_struct_0(k2_yellow_2(sK184,sK184,sK185)),u1_struct_0(sK184))
| ~ v17_waybel_0(k3_waybel_1(sK184,sK184,sK185),k2_yellow_2(sK184,sK184,sK185),sK184)
| ~ m2_relset_1(k3_waybel_1(sK184,sK184,sK185),u1_struct_0(k2_yellow_2(sK184,sK184,sK185)),u1_struct_0(sK184))
| ~ v2_orders_2(k2_yellow_2(sK184,sK184,sK185))
| ~ v3_orders_2(k2_yellow_2(sK184,sK184,sK185))
| ~ v4_orders_2(k2_yellow_2(sK184,sK184,sK185))
| ~ v1_lattice3(k2_yellow_2(sK184,sK184,sK185))
| ~ v2_lattice3(k2_yellow_2(sK184,sK184,sK185))
| ~ v3_lattice3(k2_yellow_2(sK184,sK184,sK185))
| ~ l1_orders_2(k2_yellow_2(sK184,sK184,sK185)) ),
inference(forward_subsumption_resolution,[],[f61865,f34040]) ).
fof(f61868,definition,
( spl2594_480
<=> l1_orders_2(k2_yellow_2(sK184,sK184,sK185)) ),
introduced(definition,[new_symbols(definition,[spl2594_480])],[avatar_definition]) ).
fof(f61869,plain,
( ~ l1_orders_2(k2_yellow_2(sK184,sK184,sK185))
| spl2594_480 ),
inference(avatar_component_clause,[],[f61868]) ).
fof(f61871,definition,
( spl2594_481
<=> v3_lattice3(k2_yellow_2(sK184,sK184,sK185)) ),
introduced(definition,[new_symbols(definition,[spl2594_481])],[avatar_definition]) ).
fof(f61874,definition,
( spl2594_482
<=> v2_lattice3(k2_yellow_2(sK184,sK184,sK185)) ),
introduced(definition,[new_symbols(definition,[spl2594_482])],[avatar_definition]) ).
fof(f61877,definition,
( spl2594_483
<=> v1_lattice3(k2_yellow_2(sK184,sK184,sK185)) ),
introduced(definition,[new_symbols(definition,[spl2594_483])],[avatar_definition]) ).
fof(f61880,definition,
( spl2594_484
<=> v4_orders_2(k2_yellow_2(sK184,sK184,sK185)) ),
introduced(definition,[new_symbols(definition,[spl2594_484])],[avatar_definition]) ).
fof(f61881,plain,
( ~ v4_orders_2(k2_yellow_2(sK184,sK184,sK185))
| spl2594_484 ),
inference(avatar_component_clause,[],[f61880]) ).
fof(f61883,definition,
( spl2594_485
<=> v3_orders_2(k2_yellow_2(sK184,sK184,sK185)) ),
introduced(definition,[new_symbols(definition,[spl2594_485])],[avatar_definition]) ).
fof(f61884,plain,
( ~ v3_orders_2(k2_yellow_2(sK184,sK184,sK185))
| spl2594_485 ),
inference(avatar_component_clause,[],[f61883]) ).
fof(f61886,definition,
( spl2594_486
<=> v2_orders_2(k2_yellow_2(sK184,sK184,sK185)) ),
introduced(definition,[new_symbols(definition,[spl2594_486])],[avatar_definition]) ).
fof(f61887,plain,
( ~ v2_orders_2(k2_yellow_2(sK184,sK184,sK185))
| spl2594_486 ),
inference(avatar_component_clause,[],[f61886]) ).
fof(f61889,definition,
( spl2594_487
<=> m2_relset_1(k3_waybel_1(sK184,sK184,sK185),u1_struct_0(k2_yellow_2(sK184,sK184,sK185)),u1_struct_0(sK184)) ),
introduced(definition,[new_symbols(definition,[spl2594_487])],[avatar_definition]) ).
fof(f61890,plain,
( ~ m2_relset_1(k3_waybel_1(sK184,sK184,sK185),u1_struct_0(k2_yellow_2(sK184,sK184,sK185)),u1_struct_0(sK184))
| spl2594_487 ),
inference(avatar_component_clause,[],[f61889]) ).
fof(f61892,definition,
( spl2594_488
<=> v17_waybel_0(k3_waybel_1(sK184,sK184,sK185),k2_yellow_2(sK184,sK184,sK185),sK184) ),
introduced(definition,[new_symbols(definition,[spl2594_488])],[avatar_definition]) ).
fof(f61893,plain,
( ~ v17_waybel_0(k3_waybel_1(sK184,sK184,sK185),k2_yellow_2(sK184,sK184,sK185),sK184)
| spl2594_488 ),
inference(avatar_component_clause,[],[f61892]) ).
fof(f61895,definition,
( spl2594_489
<=> v1_funct_2(k3_waybel_1(sK184,sK184,sK185),u1_struct_0(k2_yellow_2(sK184,sK184,sK185)),u1_struct_0(sK184)) ),
introduced(definition,[new_symbols(definition,[spl2594_489])],[avatar_definition]) ).
fof(f61896,plain,
( ~ v1_funct_2(k3_waybel_1(sK184,sK184,sK185),u1_struct_0(k2_yellow_2(sK184,sK184,sK185)),u1_struct_0(sK184))
| spl2594_489 ),
inference(avatar_component_clause,[],[f61895]) ).
fof(f61898,definition,
( spl2594_490
<=> v1_funct_1(k3_waybel_1(sK184,sK184,sK185)) ),
introduced(definition,[new_symbols(definition,[spl2594_490])],[avatar_definition]) ).
fof(f61899,plain,
( ~ v1_funct_1(k3_waybel_1(sK184,sK184,sK185))
| spl2594_490 ),
inference(avatar_component_clause,[],[f61898]) ).
fof(f61901,definition,
( spl2594_491
<=> v22_waybel_0(k3_waybel_1(sK184,sK184,sK185),k2_yellow_2(sK184,sK184,sK185),sK184) ),
introduced(definition,[new_symbols(definition,[spl2594_491])],[avatar_definition]) ).
fof(f61902,plain,
( ~ v22_waybel_0(k3_waybel_1(sK184,sK184,sK185),k2_yellow_2(sK184,sK184,sK185),sK184)
| spl2594_491 ),
inference(avatar_component_clause,[],[f61901]) ).
fof(f61903,plain,
( ~ spl2594_480
| ~ spl2594_481
| ~ spl2594_482
| ~ spl2594_483
| ~ spl2594_484
| ~ spl2594_485
| ~ spl2594_486
| ~ spl2594_487
| ~ spl2594_488
| ~ spl2594_489
| ~ spl2594_490
| ~ spl2594_491 ),
inference(avatar_split_clause,[],[f61866,f61901,f61898,f61895,f61892,f61889,f61886,f61883,f61880,f61877,f61874,f61871,f61868]) ).
fof(f61904,plain,
( ~ v1_funct_1(sK185)
| ~ v1_funct_2(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v4_waybel_0(k2_yellow_2(sK184,sK184,sK185),sK184)
| ~ m2_relset_1(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| v22_waybel_0(sK185,sK184,sK184) ),
inference(resolution,[],[f61853,f34048]) ).
fof(f61905,plain,
( ~ v1_funct_2(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v4_waybel_0(k2_yellow_2(sK184,sK184,sK185),sK184)
| ~ m2_relset_1(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| v22_waybel_0(sK185,sK184,sK184) ),
inference(forward_subsumption_resolution,[],[f61904,f34050]) ).
fof(f61906,plain,
( ~ v4_waybel_0(k2_yellow_2(sK184,sK184,sK185),sK184)
| ~ m2_relset_1(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| v22_waybel_0(sK185,sK184,sK184) ),
inference(forward_subsumption_resolution,[],[f61905,f34049]) ).
fof(f61907,plain,
( ~ m2_relset_1(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| v22_waybel_0(sK185,sK184,sK184) ),
inference(forward_subsumption_resolution,[],[f61906,f34051]) ).
fof(f61908,plain,
v22_waybel_0(sK185,sK184,sK184),
inference(forward_subsumption_resolution,[],[f61907,f34047]) ).
fof(f61931,plain,
( ~ v3_struct_0(sK184)
| ~ l1_orders_2(sK184) ),
inference(resolution,[],[f34072,f34042]) ).
fof(f61933,plain,
( ~ l1_orders_2(sK184)
| ~ spl2594_478 ),
inference(forward_subsumption_resolution,[],[f61931,f61829]) ).
fof(f61934,plain,
( $false
| ~ spl2594_478 ),
inference(forward_subsumption_resolution,[],[f61933,f34040]) ).
fof(f61935,plain,
~ spl2594_478,
inference(avatar_contradiction_clause,[],[f61934]) ).
fof(f61952,plain,
~ v3_struct_0(sK184),
inference(forward_subsumption_resolution,[],[f61931,f34040]) ).
fof(f61988,plain,
( ! [X0] :
( k1_yellow_2(sK184,sK184,X0) = u1_struct_0(k2_yellow_2(sK184,sK184,X0))
| ~ v1_funct_1(X0)
| v3_struct_0(sK184)
| ~ m2_relset_1(X0,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v1_funct_2(X0,u1_struct_0(sK184),u1_struct_0(sK184)) )
| ~ spl2594_479 ),
inference(resolution,[],[f61834,f34040]) ).
fof(f61989,plain,
( ! [X0] :
( ~ v1_funct_2(X0,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v1_funct_1(X0)
| ~ m2_relset_1(X0,u1_struct_0(sK184),u1_struct_0(sK184))
| k1_yellow_2(sK184,sK184,X0) = u1_struct_0(k2_yellow_2(sK184,sK184,X0)) )
| ~ spl2594_479 ),
inference(forward_subsumption_resolution,[],[f61988,f61952]) ).
fof(f61998,plain,
m1_relset_1(sK185,u1_struct_0(sK184),u1_struct_0(sK184)),
inference(resolution,[],[f34064,f34047]) ).
fof(f62023,plain,
( v3_struct_0(sK184)
| ~ l1_orders_2(sK184)
| v3_struct_0(sK184)
| ~ l1_orders_2(sK184)
| ~ v1_funct_1(sK185)
| ~ v1_funct_2(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| v1_funct_2(k3_waybel_1(sK184,sK184,sK185),u1_struct_0(k2_yellow_2(sK184,sK184,sK185)),u1_struct_0(sK184)) ),
inference(resolution,[],[f61998,f36353]) ).
fof(f62026,plain,
( ~ v2_orders_2(sK184)
| ~ v3_orders_2(sK184)
| ~ v4_orders_2(sK184)
| ~ v1_lattice3(sK184)
| ~ v2_lattice3(sK184)
| ~ v3_lattice3(sK184)
| ~ l1_orders_2(sK184)
| ~ v1_funct_1(sK185)
| ~ v1_funct_2(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v6_waybel_1(sK185,sK184)
| v3_lattice3(k2_yellow_2(sK184,sK184,sK185)) ),
inference(resolution,[],[f61998,f33983]) ).
fof(f62028,plain,
( ~ v2_orders_2(sK184)
| ~ v3_orders_2(sK184)
| ~ v4_orders_2(sK184)
| ~ v1_lattice3(sK184)
| ~ v2_lattice3(sK184)
| ~ v3_lattice3(sK184)
| ~ l1_orders_2(sK184)
| ~ v1_funct_1(sK185)
| ~ v1_funct_2(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v6_waybel_1(sK185,sK184)
| v1_lattice3(k2_yellow_2(sK184,sK184,sK185)) ),
inference(resolution,[],[f61998,f33985]) ).
fof(f62034,plain,
( ~ v2_orders_2(sK184)
| ~ v3_orders_2(sK184)
| ~ v4_orders_2(sK184)
| ~ v1_lattice3(sK184)
| ~ v2_lattice3(sK184)
| ~ v3_lattice3(sK184)
| ~ l1_orders_2(sK184)
| ~ v1_funct_1(sK185)
| ~ v1_funct_2(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v22_waybel_0(sK185,sK184,sK184)
| ~ v7_waybel_1(sK185,sK184)
| v2_lattice3(k2_yellow_2(sK184,sK184,sK185)) ),
inference(resolution,[],[f61998,f46193]) ).
fof(f62039,plain,
( v3_struct_0(sK184)
| ~ v2_orders_2(sK184)
| ~ v3_orders_2(sK184)
| ~ v4_orders_2(sK184)
| ~ l1_orders_2(sK184)
| ~ v1_funct_1(sK185)
| ~ v1_funct_2(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v7_waybel_1(sK185,sK184)
| v4_orders_2(k2_yellow_2(sK184,sK184,sK185)) ),
inference(resolution,[],[f61998,f46203]) ).
fof(f62040,plain,
( v3_struct_0(sK184)
| ~ v2_orders_2(sK184)
| ~ v3_orders_2(sK184)
| ~ v4_orders_2(sK184)
| ~ l1_orders_2(sK184)
| ~ v1_funct_1(sK185)
| ~ v1_funct_2(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v7_waybel_1(sK185,sK184)
| v3_orders_2(k2_yellow_2(sK184,sK184,sK185)) ),
inference(resolution,[],[f61998,f46204]) ).
fof(f62041,plain,
( v3_struct_0(sK184)
| ~ v2_orders_2(sK184)
| ~ v3_orders_2(sK184)
| ~ v4_orders_2(sK184)
| ~ l1_orders_2(sK184)
| ~ v1_funct_1(sK185)
| ~ v1_funct_2(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v7_waybel_1(sK185,sK184)
| v2_orders_2(k2_yellow_2(sK184,sK184,sK185)) ),
inference(resolution,[],[f61998,f46205]) ).
fof(f62046,plain,
( v3_struct_0(sK184)
| ~ l1_orders_2(sK184)
| ~ v1_funct_1(sK185)
| ~ v1_funct_2(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| v1_funct_2(k3_waybel_1(sK184,sK184,sK185),u1_struct_0(k2_yellow_2(sK184,sK184,sK185)),u1_struct_0(sK184)) ),
inference(duplicate_literal_removal,[],[f62023]) ).
fof(f62050,plain,
( ~ v2_orders_2(sK184)
| ~ v3_orders_2(sK184)
| ~ v4_orders_2(sK184)
| ~ l1_orders_2(sK184)
| ~ v1_funct_1(sK185)
| ~ v1_funct_2(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v7_waybel_1(sK185,sK184)
| v2_orders_2(k2_yellow_2(sK184,sK184,sK185)) ),
inference(forward_subsumption_resolution,[],[f62041,f61952]) ).
fof(f62051,plain,
( ~ v2_orders_2(sK184)
| ~ v3_orders_2(sK184)
| ~ v4_orders_2(sK184)
| ~ l1_orders_2(sK184)
| ~ v1_funct_1(sK185)
| ~ v1_funct_2(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v7_waybel_1(sK185,sK184)
| v3_orders_2(k2_yellow_2(sK184,sK184,sK185)) ),
inference(forward_subsumption_resolution,[],[f62040,f61952]) ).
fof(f62052,plain,
( ~ v2_orders_2(sK184)
| ~ v3_orders_2(sK184)
| ~ v4_orders_2(sK184)
| ~ l1_orders_2(sK184)
| ~ v1_funct_1(sK185)
| ~ v1_funct_2(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v7_waybel_1(sK185,sK184)
| v4_orders_2(k2_yellow_2(sK184,sK184,sK185)) ),
inference(forward_subsumption_resolution,[],[f62039,f61952]) ).
fof(f62057,plain,
( ~ v3_orders_2(sK184)
| ~ v4_orders_2(sK184)
| ~ v1_lattice3(sK184)
| ~ v2_lattice3(sK184)
| ~ v3_lattice3(sK184)
| ~ l1_orders_2(sK184)
| ~ v1_funct_1(sK185)
| ~ v1_funct_2(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v22_waybel_0(sK185,sK184,sK184)
| ~ v7_waybel_1(sK185,sK184)
| v2_lattice3(k2_yellow_2(sK184,sK184,sK185)) ),
inference(forward_subsumption_resolution,[],[f62034,f34046]) ).
fof(f62063,plain,
( ~ v3_orders_2(sK184)
| ~ v4_orders_2(sK184)
| ~ v1_lattice3(sK184)
| ~ v2_lattice3(sK184)
| ~ v3_lattice3(sK184)
| ~ l1_orders_2(sK184)
| ~ v1_funct_1(sK185)
| ~ v1_funct_2(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v6_waybel_1(sK185,sK184)
| v1_lattice3(k2_yellow_2(sK184,sK184,sK185)) ),
inference(forward_subsumption_resolution,[],[f62028,f34046]) ).
fof(f62065,plain,
( ~ v3_orders_2(sK184)
| ~ v4_orders_2(sK184)
| ~ v1_lattice3(sK184)
| ~ v2_lattice3(sK184)
| ~ v3_lattice3(sK184)
| ~ l1_orders_2(sK184)
| ~ v1_funct_1(sK185)
| ~ v1_funct_2(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v6_waybel_1(sK185,sK184)
| v3_lattice3(k2_yellow_2(sK184,sK184,sK185)) ),
inference(forward_subsumption_resolution,[],[f62026,f34046]) ).
fof(f62068,plain,
( ~ l1_orders_2(sK184)
| ~ v1_funct_1(sK185)
| ~ v1_funct_2(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| v1_funct_2(k3_waybel_1(sK184,sK184,sK185),u1_struct_0(k2_yellow_2(sK184,sK184,sK185)),u1_struct_0(sK184)) ),
inference(forward_subsumption_resolution,[],[f62046,f61952]) ).
fof(f62072,plain,
( ~ v3_orders_2(sK184)
| ~ v4_orders_2(sK184)
| ~ l1_orders_2(sK184)
| ~ v1_funct_1(sK185)
| ~ v1_funct_2(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v7_waybel_1(sK185,sK184)
| v2_orders_2(k2_yellow_2(sK184,sK184,sK185)) ),
inference(forward_subsumption_resolution,[],[f62050,f34046]) ).
fof(f62073,plain,
( ~ v3_orders_2(sK184)
| ~ v4_orders_2(sK184)
| ~ l1_orders_2(sK184)
| ~ v1_funct_1(sK185)
| ~ v1_funct_2(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v7_waybel_1(sK185,sK184)
| v3_orders_2(k2_yellow_2(sK184,sK184,sK185)) ),
inference(forward_subsumption_resolution,[],[f62051,f34046]) ).
fof(f62074,plain,
( ~ v3_orders_2(sK184)
| ~ v4_orders_2(sK184)
| ~ l1_orders_2(sK184)
| ~ v1_funct_1(sK185)
| ~ v1_funct_2(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v7_waybel_1(sK185,sK184)
| v4_orders_2(k2_yellow_2(sK184,sK184,sK185)) ),
inference(forward_subsumption_resolution,[],[f62052,f34046]) ).
fof(f62079,plain,
( ~ v4_orders_2(sK184)
| ~ v1_lattice3(sK184)
| ~ v2_lattice3(sK184)
| ~ v3_lattice3(sK184)
| ~ l1_orders_2(sK184)
| ~ v1_funct_1(sK185)
| ~ v1_funct_2(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v22_waybel_0(sK185,sK184,sK184)
| ~ v7_waybel_1(sK185,sK184)
| v2_lattice3(k2_yellow_2(sK184,sK184,sK185)) ),
inference(forward_subsumption_resolution,[],[f62057,f34045]) ).
fof(f62085,plain,
( ~ v4_orders_2(sK184)
| ~ v1_lattice3(sK184)
| ~ v2_lattice3(sK184)
| ~ v3_lattice3(sK184)
| ~ l1_orders_2(sK184)
| ~ v1_funct_1(sK185)
| ~ v1_funct_2(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v6_waybel_1(sK185,sK184)
| v1_lattice3(k2_yellow_2(sK184,sK184,sK185)) ),
inference(forward_subsumption_resolution,[],[f62063,f34045]) ).
fof(f62087,plain,
( ~ v4_orders_2(sK184)
| ~ v1_lattice3(sK184)
| ~ v2_lattice3(sK184)
| ~ v3_lattice3(sK184)
| ~ l1_orders_2(sK184)
| ~ v1_funct_1(sK185)
| ~ v1_funct_2(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v6_waybel_1(sK185,sK184)
| v3_lattice3(k2_yellow_2(sK184,sK184,sK185)) ),
inference(forward_subsumption_resolution,[],[f62065,f34045]) ).
fof(f62090,plain,
( ~ v1_funct_1(sK185)
| ~ v1_funct_2(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| v1_funct_2(k3_waybel_1(sK184,sK184,sK185),u1_struct_0(k2_yellow_2(sK184,sK184,sK185)),u1_struct_0(sK184)) ),
inference(forward_subsumption_resolution,[],[f62068,f34040]) ).
fof(f62094,plain,
( ~ v4_orders_2(sK184)
| ~ l1_orders_2(sK184)
| ~ v1_funct_1(sK185)
| ~ v1_funct_2(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v7_waybel_1(sK185,sK184)
| v2_orders_2(k2_yellow_2(sK184,sK184,sK185)) ),
inference(forward_subsumption_resolution,[],[f62072,f34045]) ).
fof(f62095,plain,
( ~ v4_orders_2(sK184)
| ~ l1_orders_2(sK184)
| ~ v1_funct_1(sK185)
| ~ v1_funct_2(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v7_waybel_1(sK185,sK184)
| v3_orders_2(k2_yellow_2(sK184,sK184,sK185)) ),
inference(forward_subsumption_resolution,[],[f62073,f34045]) ).
fof(f62096,plain,
( ~ v4_orders_2(sK184)
| ~ l1_orders_2(sK184)
| ~ v1_funct_1(sK185)
| ~ v1_funct_2(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v7_waybel_1(sK185,sK184)
| v4_orders_2(k2_yellow_2(sK184,sK184,sK185)) ),
inference(forward_subsumption_resolution,[],[f62074,f34045]) ).
fof(f62101,plain,
( ~ v1_lattice3(sK184)
| ~ v2_lattice3(sK184)
| ~ v3_lattice3(sK184)
| ~ l1_orders_2(sK184)
| ~ v1_funct_1(sK185)
| ~ v1_funct_2(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v22_waybel_0(sK185,sK184,sK184)
| ~ v7_waybel_1(sK185,sK184)
| v2_lattice3(k2_yellow_2(sK184,sK184,sK185)) ),
inference(forward_subsumption_resolution,[],[f62079,f34044]) ).
fof(f62107,plain,
( ~ v1_lattice3(sK184)
| ~ v2_lattice3(sK184)
| ~ v3_lattice3(sK184)
| ~ l1_orders_2(sK184)
| ~ v1_funct_1(sK185)
| ~ v1_funct_2(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v6_waybel_1(sK185,sK184)
| v1_lattice3(k2_yellow_2(sK184,sK184,sK185)) ),
inference(forward_subsumption_resolution,[],[f62085,f34044]) ).
fof(f62109,plain,
( ~ v1_lattice3(sK184)
| ~ v2_lattice3(sK184)
| ~ v3_lattice3(sK184)
| ~ l1_orders_2(sK184)
| ~ v1_funct_1(sK185)
| ~ v1_funct_2(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v6_waybel_1(sK185,sK184)
| v3_lattice3(k2_yellow_2(sK184,sK184,sK185)) ),
inference(forward_subsumption_resolution,[],[f62087,f34044]) ).
fof(f62112,plain,
( ~ v1_funct_2(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| v1_funct_2(k3_waybel_1(sK184,sK184,sK185),u1_struct_0(k2_yellow_2(sK184,sK184,sK185)),u1_struct_0(sK184)) ),
inference(forward_subsumption_resolution,[],[f62090,f34050]) ).
fof(f62116,plain,
( ~ l1_orders_2(sK184)
| ~ v1_funct_1(sK185)
| ~ v1_funct_2(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v7_waybel_1(sK185,sK184)
| v2_orders_2(k2_yellow_2(sK184,sK184,sK185)) ),
inference(forward_subsumption_resolution,[],[f62094,f34044]) ).
fof(f62117,plain,
( ~ l1_orders_2(sK184)
| ~ v1_funct_1(sK185)
| ~ v1_funct_2(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v7_waybel_1(sK185,sK184)
| v3_orders_2(k2_yellow_2(sK184,sK184,sK185)) ),
inference(forward_subsumption_resolution,[],[f62095,f34044]) ).
fof(f62118,plain,
( ~ l1_orders_2(sK184)
| ~ v1_funct_1(sK185)
| ~ v1_funct_2(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v7_waybel_1(sK185,sK184)
| v4_orders_2(k2_yellow_2(sK184,sK184,sK185)) ),
inference(forward_subsumption_resolution,[],[f62096,f34044]) ).
fof(f62123,plain,
( ~ v2_lattice3(sK184)
| ~ v3_lattice3(sK184)
| ~ l1_orders_2(sK184)
| ~ v1_funct_1(sK185)
| ~ v1_funct_2(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v22_waybel_0(sK185,sK184,sK184)
| ~ v7_waybel_1(sK185,sK184)
| v2_lattice3(k2_yellow_2(sK184,sK184,sK185)) ),
inference(forward_subsumption_resolution,[],[f62101,f34043]) ).
fof(f62129,plain,
( ~ v2_lattice3(sK184)
| ~ v3_lattice3(sK184)
| ~ l1_orders_2(sK184)
| ~ v1_funct_1(sK185)
| ~ v1_funct_2(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v6_waybel_1(sK185,sK184)
| v1_lattice3(k2_yellow_2(sK184,sK184,sK185)) ),
inference(forward_subsumption_resolution,[],[f62107,f34043]) ).
fof(f62131,plain,
( ~ v2_lattice3(sK184)
| ~ v3_lattice3(sK184)
| ~ l1_orders_2(sK184)
| ~ v1_funct_1(sK185)
| ~ v1_funct_2(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v6_waybel_1(sK185,sK184)
| v3_lattice3(k2_yellow_2(sK184,sK184,sK185)) ),
inference(forward_subsumption_resolution,[],[f62109,f34043]) ).
fof(f62134,plain,
v1_funct_2(k3_waybel_1(sK184,sK184,sK185),u1_struct_0(k2_yellow_2(sK184,sK184,sK185)),u1_struct_0(sK184)),
inference(forward_subsumption_resolution,[],[f62112,f34049]) ).
fof(f62138,plain,
( ~ v1_funct_1(sK185)
| ~ v1_funct_2(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v7_waybel_1(sK185,sK184)
| v2_orders_2(k2_yellow_2(sK184,sK184,sK185)) ),
inference(forward_subsumption_resolution,[],[f62116,f34040]) ).
fof(f62139,plain,
( ~ v1_funct_1(sK185)
| ~ v1_funct_2(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v7_waybel_1(sK185,sK184)
| v3_orders_2(k2_yellow_2(sK184,sK184,sK185)) ),
inference(forward_subsumption_resolution,[],[f62117,f34040]) ).
fof(f62140,plain,
( ~ v1_funct_1(sK185)
| ~ v1_funct_2(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v7_waybel_1(sK185,sK184)
| v4_orders_2(k2_yellow_2(sK184,sK184,sK185)) ),
inference(forward_subsumption_resolution,[],[f62118,f34040]) ).
fof(f62145,plain,
( ~ v3_lattice3(sK184)
| ~ l1_orders_2(sK184)
| ~ v1_funct_1(sK185)
| ~ v1_funct_2(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v22_waybel_0(sK185,sK184,sK184)
| ~ v7_waybel_1(sK185,sK184)
| v2_lattice3(k2_yellow_2(sK184,sK184,sK185)) ),
inference(forward_subsumption_resolution,[],[f62123,f34042]) ).
fof(f62151,plain,
( ~ v3_lattice3(sK184)
| ~ l1_orders_2(sK184)
| ~ v1_funct_1(sK185)
| ~ v1_funct_2(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v6_waybel_1(sK185,sK184)
| v1_lattice3(k2_yellow_2(sK184,sK184,sK185)) ),
inference(forward_subsumption_resolution,[],[f62129,f34042]) ).
fof(f62153,plain,
( ~ v3_lattice3(sK184)
| ~ l1_orders_2(sK184)
| ~ v1_funct_1(sK185)
| ~ v1_funct_2(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v6_waybel_1(sK185,sK184)
| v3_lattice3(k2_yellow_2(sK184,sK184,sK185)) ),
inference(forward_subsumption_resolution,[],[f62131,f34042]) ).
fof(f62158,plain,
( ~ v1_funct_2(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v7_waybel_1(sK185,sK184)
| v2_orders_2(k2_yellow_2(sK184,sK184,sK185)) ),
inference(forward_subsumption_resolution,[],[f62138,f34050]) ).
fof(f62159,plain,
( ~ v1_funct_2(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v7_waybel_1(sK185,sK184)
| v3_orders_2(k2_yellow_2(sK184,sK184,sK185)) ),
inference(forward_subsumption_resolution,[],[f62139,f34050]) ).
fof(f62160,plain,
( ~ v1_funct_2(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v7_waybel_1(sK185,sK184)
| v4_orders_2(k2_yellow_2(sK184,sK184,sK185)) ),
inference(forward_subsumption_resolution,[],[f62140,f34050]) ).
fof(f62164,plain,
( ~ l1_orders_2(sK184)
| ~ v1_funct_1(sK185)
| ~ v1_funct_2(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v22_waybel_0(sK185,sK184,sK184)
| ~ v7_waybel_1(sK185,sK184)
| v2_lattice3(k2_yellow_2(sK184,sK184,sK185)) ),
inference(forward_subsumption_resolution,[],[f62145,f34041]) ).
fof(f62170,plain,
( ~ l1_orders_2(sK184)
| ~ v1_funct_1(sK185)
| ~ v1_funct_2(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v6_waybel_1(sK185,sK184)
| v1_lattice3(k2_yellow_2(sK184,sK184,sK185)) ),
inference(forward_subsumption_resolution,[],[f62151,f34041]) ).
fof(f62172,plain,
( ~ l1_orders_2(sK184)
| ~ v1_funct_1(sK185)
| ~ v1_funct_2(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v6_waybel_1(sK185,sK184)
| v3_lattice3(k2_yellow_2(sK184,sK184,sK185)) ),
inference(forward_subsumption_resolution,[],[f62153,f34041]) ).
fof(f62174,plain,
( ~ v7_waybel_1(sK185,sK184)
| v2_orders_2(k2_yellow_2(sK184,sK184,sK185)) ),
inference(forward_subsumption_resolution,[],[f62158,f34049]) ).
fof(f62175,plain,
( ~ v7_waybel_1(sK185,sK184)
| v3_orders_2(k2_yellow_2(sK184,sK184,sK185)) ),
inference(forward_subsumption_resolution,[],[f62159,f34049]) ).
fof(f62176,plain,
( ~ v7_waybel_1(sK185,sK184)
| v4_orders_2(k2_yellow_2(sK184,sK184,sK185)) ),
inference(forward_subsumption_resolution,[],[f62160,f34049]) ).
fof(f62180,plain,
( ~ v1_funct_1(sK185)
| ~ v1_funct_2(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v22_waybel_0(sK185,sK184,sK184)
| ~ v7_waybel_1(sK185,sK184)
| v2_lattice3(k2_yellow_2(sK184,sK184,sK185)) ),
inference(forward_subsumption_resolution,[],[f62164,f34040]) ).
fof(f62186,plain,
( ~ v1_funct_1(sK185)
| ~ v1_funct_2(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v6_waybel_1(sK185,sK184)
| v1_lattice3(k2_yellow_2(sK184,sK184,sK185)) ),
inference(forward_subsumption_resolution,[],[f62170,f34040]) ).
fof(f62188,plain,
( ~ v1_funct_1(sK185)
| ~ v1_funct_2(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v6_waybel_1(sK185,sK184)
| v3_lattice3(k2_yellow_2(sK184,sK184,sK185)) ),
inference(forward_subsumption_resolution,[],[f62172,f34040]) ).
fof(f62190,plain,
v2_orders_2(k2_yellow_2(sK184,sK184,sK185)),
inference(forward_subsumption_resolution,[],[f62174,f34048]) ).
fof(f62191,plain,
v3_orders_2(k2_yellow_2(sK184,sK184,sK185)),
inference(forward_subsumption_resolution,[],[f62175,f34048]) ).
fof(f62192,plain,
v4_orders_2(k2_yellow_2(sK184,sK184,sK185)),
inference(forward_subsumption_resolution,[],[f62176,f34048]) ).
fof(f62196,plain,
( ~ v1_funct_2(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v22_waybel_0(sK185,sK184,sK184)
| ~ v7_waybel_1(sK185,sK184)
| v2_lattice3(k2_yellow_2(sK184,sK184,sK185)) ),
inference(forward_subsumption_resolution,[],[f62180,f34050]) ).
fof(f62202,plain,
( ~ v1_funct_2(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v6_waybel_1(sK185,sK184)
| v1_lattice3(k2_yellow_2(sK184,sK184,sK185)) ),
inference(forward_subsumption_resolution,[],[f62186,f34050]) ).
fof(f62204,plain,
( ~ v1_funct_2(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v6_waybel_1(sK185,sK184)
| v3_lattice3(k2_yellow_2(sK184,sK184,sK185)) ),
inference(forward_subsumption_resolution,[],[f62188,f34050]) ).
fof(f62206,plain,
( ~ v22_waybel_0(sK185,sK184,sK184)
| ~ v7_waybel_1(sK185,sK184)
| v2_lattice3(k2_yellow_2(sK184,sK184,sK185)) ),
inference(forward_subsumption_resolution,[],[f62196,f34049]) ).
fof(f62209,plain,
( ~ v6_waybel_1(sK185,sK184)
| v1_lattice3(k2_yellow_2(sK184,sK184,sK185)) ),
inference(forward_subsumption_resolution,[],[f62202,f34049]) ).
fof(f62211,plain,
( ~ v6_waybel_1(sK185,sK184)
| v3_lattice3(k2_yellow_2(sK184,sK184,sK185)) ),
inference(forward_subsumption_resolution,[],[f62204,f34049]) ).
fof(f62212,plain,
( ~ v7_waybel_1(sK185,sK184)
| v2_lattice3(k2_yellow_2(sK184,sK184,sK185)) ),
inference(forward_subsumption_resolution,[],[f62206,f61908]) ).
fof(f62217,definition,
( spl2594_496
<=> v6_waybel_1(sK185,sK184) ),
introduced(definition,[new_symbols(definition,[spl2594_496])],[avatar_definition]) ).
fof(f62218,plain,
( ~ v6_waybel_1(sK185,sK184)
| spl2594_496 ),
inference(avatar_component_clause,[],[f62217]) ).
fof(f62219,plain,
( spl2594_483
| ~ spl2594_496 ),
inference(avatar_split_clause,[],[f62209,f62217,f61877]) ).
fof(f62223,plain,
( spl2594_481
| ~ spl2594_496 ),
inference(avatar_split_clause,[],[f62211,f62217,f61871]) ).
fof(f62224,plain,
v2_lattice3(k2_yellow_2(sK184,sK184,sK185)),
inference(forward_subsumption_resolution,[],[f62212,f34048]) ).
fof(f62227,plain,
spl2594_482,
inference(avatar_split_clause,[],[f62224,f61874]) ).
fof(f62253,plain,
( ~ v1_funct_1(sK185)
| ~ m2_relset_1(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| u1_struct_0(k2_yellow_2(sK184,sK184,sK185)) = k1_yellow_2(sK184,sK184,sK185)
| ~ spl2594_479 ),
inference(resolution,[],[f61989,f34049]) ).
fof(f62254,plain,
( ~ m2_relset_1(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| u1_struct_0(k2_yellow_2(sK184,sK184,sK185)) = k1_yellow_2(sK184,sK184,sK185)
| ~ spl2594_479 ),
inference(forward_subsumption_resolution,[],[f62253,f34050]) ).
fof(f62255,plain,
( u1_struct_0(k2_yellow_2(sK184,sK184,sK185)) = k1_yellow_2(sK184,sK184,sK185)
| ~ spl2594_479 ),
inference(forward_subsumption_resolution,[],[f62254,f34047]) ).
fof(f62264,plain,
( m2_relset_1(k3_waybel_1(sK184,sK184,sK185),k1_yellow_2(sK184,sK184,sK185),u1_struct_0(sK184))
| v3_struct_0(sK184)
| ~ l1_orders_2(sK184)
| v3_struct_0(sK184)
| ~ l1_orders_2(sK184)
| ~ v1_funct_1(sK185)
| ~ v1_funct_2(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ m1_relset_1(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ spl2594_479 ),
inference(superposition,[],[f36342,f62255]) ).
fof(f62300,plain,
( m2_relset_1(k3_waybel_1(sK184,sK184,sK185),k1_yellow_2(sK184,sK184,sK185),u1_struct_0(sK184))
| v3_struct_0(sK184)
| ~ l1_orders_2(sK184)
| ~ v1_funct_1(sK185)
| ~ v1_funct_2(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ m1_relset_1(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ spl2594_479 ),
inference(duplicate_literal_removal,[],[f62264]) ).
fof(f62304,plain,
( m2_relset_1(k3_waybel_1(sK184,sK184,sK185),k1_yellow_2(sK184,sK184,sK185),u1_struct_0(sK184))
| ~ l1_orders_2(sK184)
| ~ v1_funct_1(sK185)
| ~ v1_funct_2(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ m1_relset_1(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ spl2594_479 ),
inference(forward_subsumption_resolution,[],[f62300,f61952]) ).
fof(f62308,plain,
( m2_relset_1(k3_waybel_1(sK184,sK184,sK185),k1_yellow_2(sK184,sK184,sK185),u1_struct_0(sK184))
| ~ v1_funct_1(sK185)
| ~ v1_funct_2(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ m1_relset_1(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ spl2594_479 ),
inference(forward_subsumption_resolution,[],[f62304,f34040]) ).
fof(f62312,plain,
( m2_relset_1(k3_waybel_1(sK184,sK184,sK185),k1_yellow_2(sK184,sK184,sK185),u1_struct_0(sK184))
| ~ v1_funct_2(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ m1_relset_1(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ spl2594_479 ),
inference(forward_subsumption_resolution,[],[f62308,f34050]) ).
fof(f62316,plain,
( m2_relset_1(k3_waybel_1(sK184,sK184,sK185),k1_yellow_2(sK184,sK184,sK185),u1_struct_0(sK184))
| ~ m1_relset_1(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ spl2594_479 ),
inference(forward_subsumption_resolution,[],[f62312,f34049]) ).
fof(f62320,plain,
( m2_relset_1(k3_waybel_1(sK184,sK184,sK185),k1_yellow_2(sK184,sK184,sK185),u1_struct_0(sK184))
| ~ spl2594_479 ),
inference(forward_subsumption_resolution,[],[f62316,f61998]) ).
fof(f62567,plain,
! [X0] :
( ~ l1_orders_2(X0)
| u1_struct_0(X0) = k2_pre_topc(X0) ),
inference(resolution,[],[f36123,f37630]) ).
fof(f62568,plain,
u1_struct_0(sK184) = k2_pre_topc(sK184),
inference(resolution,[],[f62567,f34040]) ).
fof(f62570,plain,
v1_funct_2(sK185,k2_pre_topc(sK184),k2_pre_topc(sK184)),
inference(superposition,[],[f34049,f62568]) ).
fof(f62574,plain,
m1_relset_1(sK185,k2_pre_topc(sK184),k2_pre_topc(sK184)),
inference(superposition,[],[f61998,f62568]) ).
fof(f62583,plain,
( m2_relset_1(k3_waybel_1(sK184,sK184,sK185),k1_yellow_2(sK184,sK184,sK185),k2_pre_topc(sK184))
| ~ spl2594_479 ),
inference(superposition,[],[f62320,f62568]) ).
fof(f62805,plain,
( $false
| spl2594_496 ),
inference(unit_resulting_resolution,[],[f36245,f34040,f61952,f34050,f62218,f34048,f61998,f34049]) ).
fof(f62807,plain,
spl2594_496,
inference(avatar_contradiction_clause,[],[f62805]) ).
fof(f62923,plain,
! [X0,X1] :
( v3_struct_0(X0)
| ~ l1_orders_2(X0)
| v3_struct_0(sK184)
| m1_yellow_0(k2_yellow_2(X0,sK184,X1),sK184)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(sK184))
| ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(sK184)) ),
inference(resolution,[],[f36017,f34040]) ).
fof(f62924,plain,
! [X0,X1] :
( v3_struct_0(X0)
| ~ l1_orders_2(X0)
| m1_yellow_0(k2_yellow_2(X0,sK184,X1),sK184)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(sK184))
| ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(sK184)) ),
inference(forward_subsumption_resolution,[],[f62923,f61952]) ).
fof(f62925,plain,
! [X0,X1] :
( ~ v1_funct_2(X1,u1_struct_0(X0),k2_pre_topc(sK184))
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| m1_yellow_0(k2_yellow_2(X0,sK184,X1),sK184)
| ~ v1_funct_1(X1)
| ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(sK184)) ),
inference(forward_demodulation,[],[f62924,f62568]) ).
fof(f62926,plain,
! [X0,X1] :
( ~ l1_orders_2(X0)
| ~ v1_funct_2(X1,u1_struct_0(X0),k2_pre_topc(sK184))
| v3_struct_0(X0)
| ~ m1_relset_1(X1,u1_struct_0(X0),k2_pre_topc(sK184))
| m1_yellow_0(k2_yellow_2(X0,sK184,X1),sK184)
| ~ v1_funct_1(X1) ),
inference(forward_demodulation,[],[f62925,f62568]) ).
fof(f63129,plain,
! [X0] :
( ~ v1_funct_2(X0,u1_struct_0(sK184),k2_pre_topc(sK184))
| v3_struct_0(sK184)
| ~ m1_relset_1(X0,u1_struct_0(sK184),k2_pre_topc(sK184))
| m1_yellow_0(k2_yellow_2(sK184,sK184,X0),sK184)
| ~ v1_funct_1(X0) ),
inference(resolution,[],[f62926,f34040]) ).
fof(f63130,plain,
! [X0] :
( ~ v1_funct_2(X0,u1_struct_0(sK184),k2_pre_topc(sK184))
| ~ m1_relset_1(X0,u1_struct_0(sK184),k2_pre_topc(sK184))
| m1_yellow_0(k2_yellow_2(sK184,sK184,X0),sK184)
| ~ v1_funct_1(X0) ),
inference(forward_subsumption_resolution,[],[f63129,f61952]) ).
fof(f63131,plain,
! [X0] :
( ~ v1_funct_2(X0,k2_pre_topc(sK184),k2_pre_topc(sK184))
| ~ m1_relset_1(X0,u1_struct_0(sK184),k2_pre_topc(sK184))
| m1_yellow_0(k2_yellow_2(sK184,sK184,X0),sK184)
| ~ v1_funct_1(X0) ),
inference(forward_demodulation,[],[f63130,f62568]) ).
fof(f63132,plain,
! [X0] :
( ~ m1_relset_1(X0,k2_pre_topc(sK184),k2_pre_topc(sK184))
| ~ v1_funct_2(X0,k2_pre_topc(sK184),k2_pre_topc(sK184))
| m1_yellow_0(k2_yellow_2(sK184,sK184,X0),sK184)
| ~ v1_funct_1(X0) ),
inference(forward_demodulation,[],[f63131,f62568]) ).
fof(f63133,plain,
( ~ v1_funct_2(sK185,k2_pre_topc(sK184),k2_pre_topc(sK184))
| m1_yellow_0(k2_yellow_2(sK184,sK184,sK185),sK184)
| ~ v1_funct_1(sK185) ),
inference(resolution,[],[f63132,f62574]) ).
fof(f63134,plain,
( m1_yellow_0(k2_yellow_2(sK184,sK184,sK185),sK184)
| ~ v1_funct_1(sK185) ),
inference(forward_subsumption_resolution,[],[f63133,f62570]) ).
fof(f63135,plain,
m1_yellow_0(k2_yellow_2(sK184,sK184,sK185),sK184),
inference(forward_subsumption_resolution,[],[f63134,f34050]) ).
fof(f63326,plain,
! [X0,X1] :
( v3_struct_0(X0)
| ~ l1_orders_2(X0)
| v3_struct_0(sK184)
| v1_funct_1(k3_waybel_1(X0,sK184,X1))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(sK184))
| ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(sK184)) ),
inference(resolution,[],[f36356,f34040]) ).
fof(f63327,plain,
! [X0,X1] :
( v3_struct_0(X0)
| ~ l1_orders_2(X0)
| v1_funct_1(k3_waybel_1(X0,sK184,X1))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(sK184))
| ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(sK184)) ),
inference(forward_subsumption_resolution,[],[f63326,f61952]) ).
fof(f63328,plain,
! [X0,X1] :
( ~ v1_funct_2(X1,u1_struct_0(X0),k2_pre_topc(sK184))
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| v1_funct_1(k3_waybel_1(X0,sK184,X1))
| ~ v1_funct_1(X1)
| ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(sK184)) ),
inference(forward_demodulation,[],[f63327,f62568]) ).
fof(f63329,plain,
! [X0,X1] :
( ~ l1_orders_2(X0)
| ~ v1_funct_2(X1,u1_struct_0(X0),k2_pre_topc(sK184))
| v3_struct_0(X0)
| ~ m1_relset_1(X1,u1_struct_0(X0),k2_pre_topc(sK184))
| v1_funct_1(k3_waybel_1(X0,sK184,X1))
| ~ v1_funct_1(X1) ),
inference(forward_demodulation,[],[f63328,f62568]) ).
fof(f63390,plain,
! [X0] :
( ~ v1_funct_2(X0,u1_struct_0(sK184),k2_pre_topc(sK184))
| v3_struct_0(sK184)
| ~ m1_relset_1(X0,u1_struct_0(sK184),k2_pre_topc(sK184))
| v1_funct_1(k3_waybel_1(sK184,sK184,X0))
| ~ v1_funct_1(X0) ),
inference(resolution,[],[f63329,f34040]) ).
fof(f63391,plain,
! [X0] :
( ~ v1_funct_2(X0,u1_struct_0(sK184),k2_pre_topc(sK184))
| ~ m1_relset_1(X0,u1_struct_0(sK184),k2_pre_topc(sK184))
| v1_funct_1(k3_waybel_1(sK184,sK184,X0))
| ~ v1_funct_1(X0) ),
inference(forward_subsumption_resolution,[],[f63390,f61952]) ).
fof(f63392,plain,
! [X0] :
( ~ v1_funct_2(X0,k2_pre_topc(sK184),k2_pre_topc(sK184))
| ~ m1_relset_1(X0,u1_struct_0(sK184),k2_pre_topc(sK184))
| v1_funct_1(k3_waybel_1(sK184,sK184,X0))
| ~ v1_funct_1(X0) ),
inference(forward_demodulation,[],[f63391,f62568]) ).
fof(f63393,plain,
! [X0] :
( ~ v1_funct_2(X0,k2_pre_topc(sK184),k2_pre_topc(sK184))
| ~ m1_relset_1(X0,k2_pre_topc(sK184),k2_pre_topc(sK184))
| v1_funct_1(k3_waybel_1(sK184,sK184,X0))
| ~ v1_funct_1(X0) ),
inference(forward_demodulation,[],[f63392,f62568]) ).
fof(f63819,plain,
( ~ m1_relset_1(sK185,k2_pre_topc(sK184),k2_pre_topc(sK184))
| v1_funct_1(k3_waybel_1(sK184,sK184,sK185))
| ~ v1_funct_1(sK185) ),
inference(resolution,[],[f63393,f62570]) ).
fof(f63824,plain,
( v1_funct_1(k3_waybel_1(sK184,sK184,sK185))
| ~ v1_funct_1(sK185) ),
inference(forward_subsumption_resolution,[],[f63819,f62574]) ).
fof(f63827,plain,
v1_funct_1(k3_waybel_1(sK184,sK184,sK185)),
inference(forward_subsumption_resolution,[],[f63824,f34050]) ).
fof(f66275,plain,
( $false
| spl2594_480 ),
inference(unit_resulting_resolution,[],[f36361,f61869,f63135,f34040]) ).
fof(f66278,plain,
spl2594_480,
inference(avatar_contradiction_clause,[],[f66275]) ).
fof(f66279,plain,
( $false
| spl2594_484 ),
inference(forward_subsumption_resolution,[],[f61881,f62192]) ).
fof(f66280,plain,
spl2594_484,
inference(avatar_contradiction_clause,[],[f66279]) ).
fof(f67013,plain,
( $false
| spl2594_485 ),
inference(forward_subsumption_resolution,[],[f61884,f62191]) ).
fof(f67014,plain,
spl2594_485,
inference(avatar_contradiction_clause,[],[f67013]) ).
fof(f67015,plain,
( $false
| spl2594_486 ),
inference(forward_subsumption_resolution,[],[f61887,f62190]) ).
fof(f67016,plain,
spl2594_486,
inference(avatar_contradiction_clause,[],[f67015]) ).
fof(f67017,plain,
( ~ m2_relset_1(k3_waybel_1(sK184,sK184,sK185),u1_struct_0(k2_yellow_2(sK184,sK184,sK185)),k2_pre_topc(sK184))
| spl2594_487 ),
inference(forward_demodulation,[],[f61890,f62568]) ).
fof(f67018,plain,
( ~ m2_relset_1(k3_waybel_1(sK184,sK184,sK185),k1_yellow_2(sK184,sK184,sK185),k2_pre_topc(sK184))
| ~ spl2594_479
| spl2594_487 ),
inference(forward_demodulation,[],[f67017,f62255]) ).
fof(f67019,plain,
( $false
| ~ spl2594_479
| spl2594_487 ),
inference(forward_subsumption_resolution,[],[f67018,f62583]) ).
fof(f67020,plain,
( ~ spl2594_479
| spl2594_487 ),
inference(avatar_contradiction_clause,[],[f67019]) ).
fof(f67057,plain,
( ~ v1_funct_1(sK185)
| ~ v1_funct_2(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v7_waybel_1(sK185,sK184)
| ~ m2_relset_1(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v2_orders_2(sK184)
| ~ v3_orders_2(sK184)
| ~ v4_orders_2(sK184)
| ~ v1_lattice3(sK184)
| ~ v2_lattice3(sK184)
| ~ v3_lattice3(sK184)
| ~ l1_orders_2(sK184)
| spl2594_488 ),
inference(resolution,[],[f61893,f34026]) ).
fof(f67059,plain,
( ~ v1_funct_2(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v7_waybel_1(sK185,sK184)
| ~ m2_relset_1(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v2_orders_2(sK184)
| ~ v3_orders_2(sK184)
| ~ v4_orders_2(sK184)
| ~ v1_lattice3(sK184)
| ~ v2_lattice3(sK184)
| ~ v3_lattice3(sK184)
| ~ l1_orders_2(sK184)
| spl2594_488 ),
inference(forward_subsumption_resolution,[],[f67057,f34050]) ).
fof(f67060,plain,
( ~ v7_waybel_1(sK185,sK184)
| ~ m2_relset_1(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v2_orders_2(sK184)
| ~ v3_orders_2(sK184)
| ~ v4_orders_2(sK184)
| ~ v1_lattice3(sK184)
| ~ v2_lattice3(sK184)
| ~ v3_lattice3(sK184)
| ~ l1_orders_2(sK184)
| spl2594_488 ),
inference(forward_subsumption_resolution,[],[f67059,f34049]) ).
fof(f67061,plain,
( ~ m2_relset_1(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v2_orders_2(sK184)
| ~ v3_orders_2(sK184)
| ~ v4_orders_2(sK184)
| ~ v1_lattice3(sK184)
| ~ v2_lattice3(sK184)
| ~ v3_lattice3(sK184)
| ~ l1_orders_2(sK184)
| spl2594_488 ),
inference(forward_subsumption_resolution,[],[f67060,f34048]) ).
fof(f67062,plain,
( ~ v2_orders_2(sK184)
| ~ v3_orders_2(sK184)
| ~ v4_orders_2(sK184)
| ~ v1_lattice3(sK184)
| ~ v2_lattice3(sK184)
| ~ v3_lattice3(sK184)
| ~ l1_orders_2(sK184)
| spl2594_488 ),
inference(forward_subsumption_resolution,[],[f67061,f34047]) ).
fof(f67063,plain,
( ~ v3_orders_2(sK184)
| ~ v4_orders_2(sK184)
| ~ v1_lattice3(sK184)
| ~ v2_lattice3(sK184)
| ~ v3_lattice3(sK184)
| ~ l1_orders_2(sK184)
| spl2594_488 ),
inference(forward_subsumption_resolution,[],[f67062,f34046]) ).
fof(f67064,plain,
( ~ v4_orders_2(sK184)
| ~ v1_lattice3(sK184)
| ~ v2_lattice3(sK184)
| ~ v3_lattice3(sK184)
| ~ l1_orders_2(sK184)
| spl2594_488 ),
inference(forward_subsumption_resolution,[],[f67063,f34045]) ).
fof(f67065,plain,
( ~ v1_lattice3(sK184)
| ~ v2_lattice3(sK184)
| ~ v3_lattice3(sK184)
| ~ l1_orders_2(sK184)
| spl2594_488 ),
inference(forward_subsumption_resolution,[],[f67064,f34044]) ).
fof(f67066,plain,
( ~ v2_lattice3(sK184)
| ~ v3_lattice3(sK184)
| ~ l1_orders_2(sK184)
| spl2594_488 ),
inference(forward_subsumption_resolution,[],[f67065,f34043]) ).
fof(f67067,plain,
( ~ v3_lattice3(sK184)
| ~ l1_orders_2(sK184)
| spl2594_488 ),
inference(forward_subsumption_resolution,[],[f67066,f34042]) ).
fof(f67068,plain,
( ~ l1_orders_2(sK184)
| spl2594_488 ),
inference(forward_subsumption_resolution,[],[f67067,f34041]) ).
fof(f67069,plain,
( $false
| spl2594_488 ),
inference(forward_subsumption_resolution,[],[f67068,f34040]) ).
fof(f67070,plain,
spl2594_488,
inference(avatar_contradiction_clause,[],[f67069]) ).
fof(f67071,plain,
( $false
| spl2594_489 ),
inference(forward_subsumption_resolution,[],[f61896,f62134]) ).
fof(f67072,plain,
spl2594_489,
inference(avatar_contradiction_clause,[],[f67071]) ).
fof(f67073,plain,
( $false
| spl2594_490 ),
inference(forward_subsumption_resolution,[],[f61899,f63827]) ).
fof(f67074,plain,
spl2594_490,
inference(avatar_contradiction_clause,[],[f67073]) ).
fof(f67076,plain,
( ~ v4_waybel_0(k2_yellow_2(sK184,sK184,sK185),sK184)
| ~ v1_funct_1(sK185)
| ~ v1_funct_2(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v7_waybel_1(sK185,sK184)
| ~ m2_relset_1(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v2_orders_2(sK184)
| ~ v3_orders_2(sK184)
| ~ v4_orders_2(sK184)
| ~ v1_lattice3(sK184)
| ~ v2_lattice3(sK184)
| ~ v3_lattice3(sK184)
| ~ l1_orders_2(sK184)
| spl2594_491 ),
inference(resolution,[],[f61902,f34028]) ).
fof(f67078,plain,
( ~ v1_funct_1(sK185)
| ~ v1_funct_2(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v7_waybel_1(sK185,sK184)
| ~ m2_relset_1(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v2_orders_2(sK184)
| ~ v3_orders_2(sK184)
| ~ v4_orders_2(sK184)
| ~ v1_lattice3(sK184)
| ~ v2_lattice3(sK184)
| ~ v3_lattice3(sK184)
| ~ l1_orders_2(sK184)
| spl2594_491 ),
inference(forward_subsumption_resolution,[],[f67076,f34051]) ).
fof(f67079,plain,
( ~ v1_funct_2(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v7_waybel_1(sK185,sK184)
| ~ m2_relset_1(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v2_orders_2(sK184)
| ~ v3_orders_2(sK184)
| ~ v4_orders_2(sK184)
| ~ v1_lattice3(sK184)
| ~ v2_lattice3(sK184)
| ~ v3_lattice3(sK184)
| ~ l1_orders_2(sK184)
| spl2594_491 ),
inference(forward_subsumption_resolution,[],[f67078,f34050]) ).
fof(f67080,plain,
( ~ v7_waybel_1(sK185,sK184)
| ~ m2_relset_1(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v2_orders_2(sK184)
| ~ v3_orders_2(sK184)
| ~ v4_orders_2(sK184)
| ~ v1_lattice3(sK184)
| ~ v2_lattice3(sK184)
| ~ v3_lattice3(sK184)
| ~ l1_orders_2(sK184)
| spl2594_491 ),
inference(forward_subsumption_resolution,[],[f67079,f34049]) ).
fof(f67081,plain,
( ~ m2_relset_1(sK185,u1_struct_0(sK184),u1_struct_0(sK184))
| ~ v2_orders_2(sK184)
| ~ v3_orders_2(sK184)
| ~ v4_orders_2(sK184)
| ~ v1_lattice3(sK184)
| ~ v2_lattice3(sK184)
| ~ v3_lattice3(sK184)
| ~ l1_orders_2(sK184)
| spl2594_491 ),
inference(forward_subsumption_resolution,[],[f67080,f34048]) ).
fof(f67082,plain,
( ~ v2_orders_2(sK184)
| ~ v3_orders_2(sK184)
| ~ v4_orders_2(sK184)
| ~ v1_lattice3(sK184)
| ~ v2_lattice3(sK184)
| ~ v3_lattice3(sK184)
| ~ l1_orders_2(sK184)
| spl2594_491 ),
inference(forward_subsumption_resolution,[],[f67081,f34047]) ).
fof(f67083,plain,
( ~ v3_orders_2(sK184)
| ~ v4_orders_2(sK184)
| ~ v1_lattice3(sK184)
| ~ v2_lattice3(sK184)
| ~ v3_lattice3(sK184)
| ~ l1_orders_2(sK184)
| spl2594_491 ),
inference(forward_subsumption_resolution,[],[f67082,f34046]) ).
fof(f67084,plain,
( ~ v4_orders_2(sK184)
| ~ v1_lattice3(sK184)
| ~ v2_lattice3(sK184)
| ~ v3_lattice3(sK184)
| ~ l1_orders_2(sK184)
| spl2594_491 ),
inference(forward_subsumption_resolution,[],[f67083,f34045]) ).
fof(f67085,plain,
( ~ v1_lattice3(sK184)
| ~ v2_lattice3(sK184)
| ~ v3_lattice3(sK184)
| ~ l1_orders_2(sK184)
| spl2594_491 ),
inference(forward_subsumption_resolution,[],[f67084,f34044]) ).
fof(f67086,plain,
( ~ v2_lattice3(sK184)
| ~ v3_lattice3(sK184)
| ~ l1_orders_2(sK184)
| spl2594_491 ),
inference(forward_subsumption_resolution,[],[f67085,f34043]) ).
fof(f67087,plain,
( ~ v3_lattice3(sK184)
| ~ l1_orders_2(sK184)
| spl2594_491 ),
inference(forward_subsumption_resolution,[],[f67086,f34042]) ).
fof(f67088,plain,
( ~ l1_orders_2(sK184)
| spl2594_491 ),
inference(forward_subsumption_resolution,[],[f67087,f34041]) ).
fof(f67089,plain,
( $false
| spl2594_491 ),
inference(forward_subsumption_resolution,[],[f67088,f34040]) ).
fof(f67090,plain,
spl2594_491,
inference(avatar_contradiction_clause,[],[f67089]) ).
cnf(s404,plain,
( spl2594_478
| spl2594_479 ),
inference(sat_conversion,[],[f61835]) ).
cnf(s405,plain,
( ~ spl2594_480
| ~ spl2594_481
| ~ spl2594_482
| ~ spl2594_483
| ~ spl2594_484
| ~ spl2594_485
| ~ spl2594_486
| ~ spl2594_487
| ~ spl2594_488
| ~ spl2594_489
| ~ spl2594_490
| ~ spl2594_491 ),
inference(sat_conversion,[],[f61903]) ).
cnf(s407,plain,
~ spl2594_478,
inference(sat_conversion,[],[f61935]) ).
cnf(s415,plain,
( spl2594_483
| ~ spl2594_496 ),
inference(sat_conversion,[],[f62219]) ).
cnf(s417,plain,
( spl2594_481
| ~ spl2594_496 ),
inference(sat_conversion,[],[f62223]) ).
cnf(s418,plain,
spl2594_482,
inference(sat_conversion,[],[f62227]) ).
cnf(s419,plain,
spl2594_496,
inference(sat_conversion,[],[f62807]) ).
cnf(s656,plain,
spl2594_480,
inference(sat_conversion,[],[f66278]) ).
cnf(s657,plain,
spl2594_484,
inference(sat_conversion,[],[f66280]) ).
cnf(s738,plain,
spl2594_485,
inference(sat_conversion,[],[f67014]) ).
cnf(s739,plain,
spl2594_486,
inference(sat_conversion,[],[f67016]) ).
cnf(s740,plain,
( ~ spl2594_479
| spl2594_487 ),
inference(sat_conversion,[],[f67020]) ).
cnf(s744,plain,
spl2594_488,
inference(sat_conversion,[],[f67070]) ).
cnf(s745,plain,
spl2594_489,
inference(sat_conversion,[],[f67072]) ).
cnf(s746,plain,
spl2594_490,
inference(sat_conversion,[],[f67074]) ).
cnf(s748,plain,
spl2594_491,
inference(sat_conversion,[],[f67090]) ).
cnf(s859,plain,
spl2594_481,
inference(rat,[],[s417,s419]) ).
cnf(s860,plain,
spl2594_483,
inference(rat,[],[s415,s419]) ).
cnf(s904,plain,
~ spl2594_487,
inference(rat,[],[s405,s748,s746,s745,s744,s739,s738,s657,s860,s418,s859,s656]) ).
cnf(s905,plain,
~ spl2594_479,
inference(rat,[],[s740,s904]) ).
cnf(s906,plain,
$false,
inference(rat,[],[s404,s905,s407]) ).
fof(f67091,plain,
$false,
inference(avatar_sat_refutation,[],[s906]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT369+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.38 % Computer : n014.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Sun Sep 27 15:06:04 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.42 Running first-order theorem proving
% 0.12/0.42 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 16.16/4.13 % (918477)Detected formulas, will run a generic FOF schedule.
% 16.16/4.13 % (918483)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=1928930640:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2988 on theBenchmark for (2988ds/134677Mi)
% 16.16/4.13 % (918482)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=2935571674:i=141193_2988 on theBenchmark for (2988ds/141193Mi)
% 16.16/4.13 % (918484)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=801405826:i=141695:sd=1:nm=32:gsp=on:ss=included_2988 on theBenchmark for (2988ds/141695Mi)
% 16.16/4.13 % (918486)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2512045887:i=119:av=off:ss=axioms_2988 on theBenchmark for (2988ds/119Mi)
% 16.16/4.13 % (918485)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1752791743:i=109:sd=1:ins=1:gsp=on:ss=axioms_2988 on theBenchmark for (2988ds/109Mi)
% 16.16/4.13 % (918488)dis-21_1_sil=8000:lcm=predicate:random_seed=163787525:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2988 on theBenchmark for (2988ds/129Mi)
% 16.16/4.13 % (918487)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=158601588:s2a=on:i=139:gtg=position_2988 on theBenchmark for (2988ds/139Mi)
% 16.16/4.13 % (918485)Instruction limit reached!
% 16.16/4.13 % (918485)------------------------------
% 16.16/4.13 % (918485)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.16/4.13 % (918485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.16/4.13 % (918485)CaDiCaL version: 2.1.3
% 16.16/4.13 % (918485)Termination reason: Instruction limit
% 16.16/4.13 % (918485)Termination phase: SInE selection
% 16.16/4.13 % (918485)Time elapsed: 0.086 s
% 16.16/4.13 % (918485)Peak memory usage: 112 MB
% 16.16/4.13 % (918485)Instructions burned: 110 (million)
% 16.16/4.13 % (918487)Instruction limit reached!
% 16.16/4.13 % (918487)------------------------------
% 16.16/4.13 % (918487)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.16/4.13 % (918487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.16/4.13 % (918487)CaDiCaL version: 2.1.3
% 16.16/4.13 % (918487)Termination reason: Instruction limit
% 16.16/4.13 % (918487)Termination phase: Property scanning
% 16.16/4.13 % (918487)Time elapsed: 0.060 s
% 16.16/4.13 % (918487)Peak memory usage: 112 MB
% 16.16/4.13 % (918487)Instructions burned: 140 (million)
% 16.16/4.13 % (918486)Instruction limit reached!
% 16.16/4.13 % (918486)------------------------------
% 16.16/4.13 % (918486)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.16/4.13 % (918486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.16/4.13 % (918486)CaDiCaL version: 2.1.3
% 16.16/4.13 % (918486)Termination reason: Instruction limit
% 16.16/4.13 % (918486)Termination phase: Preprocessing 1
% 16.16/4.13 % (918486)Time elapsed: 0.101 s
% 16.16/4.13 % (918486)Peak memory usage: 112 MB
% 16.16/4.13 % (918486)Instructions burned: 119 (million)
% 16.16/4.13 % (918488)Instruction limit reached!
% 16.16/4.13 % (918488)------------------------------
% 16.16/4.13 % (918488)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.16/4.13 % (918488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.16/4.13 % (918488)CaDiCaL version: 2.1.3
% 16.16/4.13 % (918488)Termination reason: Instruction limit
% 16.16/4.13 % (918488)Termination phase: SInE selection
% 16.16/4.13 % (918488)Time elapsed: 0.090 s
% 16.16/4.13 % (918488)Peak memory usage: 112 MB
% 16.16/4.13 % (918488)Instructions burned: 130 (million)
% 16.16/4.13 % (918496)lrs+10_1_sil=8000:sp=occurrence:random_seed=2658725046:i=285:sd=3:ss=axioms:sgt=8_2986 on theBenchmark for (2986ds/285Mi)
% 16.16/4.13 % (918499)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=2594660659:s2a=on:i=248:s2at=1.23:gtg=position_2986 on theBenchmark for (2986ds/248Mi)
% 16.16/4.13 % (918498)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2718262905:i=325:sd=1:ss=axioms:sgt=32_2986 on theBenchmark for (2986ds/325Mi)
% 16.16/4.13 % (918497)lrs+10_1_sil=32000:urr=on:br=off:random_seed=75084983:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2986 on theBenchmark for (2986ds/157Mi)
% 16.16/4.13 % (918497)Instruction limit reached!
% 16.16/4.13 % (918497)------------------------------
% 23.93/5.19 % (918497)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.93/5.19 % (918497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.93/5.19 % (918497)CaDiCaL version: 2.1.3
% 23.93/5.19 % (918497)Termination reason: Instruction limit
% 23.93/5.19 % (918497)Termination phase: Property scanning
% 23.93/5.19 % (918497)Time elapsed: 0.069 s
% 23.93/5.19 % (918497)Peak memory usage: 112 MB
% 23.93/5.19 % (918497)Instructions burned: 159 (million)
% 23.93/5.19 % (918499)Instruction limit reached!
% 23.93/5.19 % (918499)------------------------------
% 23.93/5.19 % (918499)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.93/5.19 % (918499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.93/5.19 % (918499)CaDiCaL version: 2.1.3
% 23.93/5.19 % (918499)Termination reason: Instruction limit
% 23.93/5.19 % (918499)Termination phase: Property scanning
% 23.93/5.19 % (918499)Time elapsed: 0.107 s
% 23.93/5.19 % (918499)Peak memory usage: 112 MB
% 23.93/5.19 % (918499)Instructions burned: 249 (million)
% 23.93/5.19 % (918498)Refutation not found, incomplete strategy
% 23.93/5.19 % (918498)------------------------------
% 23.93/5.19 % (918498)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.93/5.19 % (918498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.93/5.19 % (918498)CaDiCaL version: 2.1.3
% 23.93/5.19 % (918498)Termination reason: Refutation not found, incomplete strategy
% 23.93/5.19 % (918498)Time elapsed: 0.109 s
% 23.93/5.19 % (918498)Peak memory usage: 117 MB
% 23.93/5.19 % (918498)Instructions burned: 128 (million)
% 23.93/5.19 % (918496)Instruction limit reached!
% 23.93/5.19 % (918496)------------------------------
% 23.93/5.19 % (918496)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.93/5.19 % (918496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.93/5.19 % (918496)CaDiCaL version: 2.1.3
% 23.93/5.19 % (918496)Termination reason: Instruction limit
% 23.93/5.19 % (918496)Termination phase: Saturation
% 23.93/5.19 % (918496)Time elapsed: 0.199 s
% 23.93/5.19 % (918496)Peak memory usage: 119 MB
% 23.93/5.19 % (918496)Instructions burned: 286 (million)
% 23.93/5.19 % (918504)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2047569256:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2984 on theBenchmark for (2984ds/294Mi)
% 23.93/5.19 % (918505)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=4027290079:i=2350_2983 on theBenchmark for (2983ds/2350Mi)
% 23.93/5.19 % (918498)------------------------------
% 23.93/5.19 % (918498)------------------------------
% 23.93/5.19 % (918506)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=718429415:cts=off:i=113:fsr=off:ss=included:sgt=4_2982 on theBenchmark for (2982ds/113Mi)
% 23.93/5.19 % (918504)Instruction limit reached!
% 23.93/5.19 % (918504)------------------------------
% 23.93/5.19 % (918504)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.93/5.19 % (918504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.93/5.19 % (918504)CaDiCaL version: 2.1.3
% 23.93/5.19 % (918504)Termination reason: Instruction limit
% 23.93/5.19 % (918504)Termination phase: Property scanning
% 23.93/5.19 % (918504)Time elapsed: 0.215 s
% 23.93/5.19 % (918504)Peak memory usage: 119 MB
% 23.93/5.19 % (918504)Instructions burned: 295 (million)
% 23.93/5.19 % (918506)Instruction limit reached!
% 23.93/5.19 % (918506)------------------------------
% 23.93/5.19 % (918506)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.93/5.19 % (918506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.93/5.19 % (918506)CaDiCaL version: 2.1.3
% 23.93/5.19 % (918506)Termination reason: Instruction limit
% 23.93/5.19 % (918506)Termination phase: SInE selection
% 23.93/5.19 % (918506)Time elapsed: 0.093 s
% 23.93/5.19 % (918506)Peak memory usage: 112 MB
% 23.93/5.19 % (918506)Instructions burned: 114 (million)
% 23.93/5.19 % (918510)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2332095858:i=127:av=off:fsr=off:sup=off_2981 on theBenchmark for (2981ds/127Mi)
% 23.93/5.19 % (918511)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2249504562:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2980 on theBenchmark for (2980ds/114Mi)
% 23.93/5.19 % (918510)Instruction limit reached!
% 23.93/5.19 % (918510)------------------------------
% 23.93/5.19 % (918510)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.93/5.19 % (918510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.83/6.19 % (918510)CaDiCaL version: 2.1.3
% 14.83/6.19 % (918510)Termination reason: Instruction limit
% 14.83/6.19 % (918510)Termination phase: Preprocessing 1
% 14.83/6.19 % (918510)Time elapsed: 0.094 s
% 14.83/6.19 % (918510)Peak memory usage: 113 MB
% 14.83/6.19 % (918510)Instructions burned: 128 (million)
% 14.83/6.19 % (918512)lrs+10_1_sil=8000:sp=occurrence:random_seed=3773188118:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2980 on theBenchmark for (2980ds/907Mi)
% 14.83/6.19 % (918511)Instruction limit reached!
% 14.83/6.19 % (918511)------------------------------
% 14.83/6.19 % (918511)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.83/6.19 % (918511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.83/6.19 % (918511)CaDiCaL version: 2.1.3
% 14.83/6.19 % (918511)Termination reason: Instruction limit
% 14.83/6.19 % (918511)Termination phase: Property scanning
% 14.83/6.19 % (918511)Time elapsed: 0.050 s
% 14.83/6.19 % (918511)Peak memory usage: 112 MB
% 14.83/6.19 % (918511)Instructions burned: 116 (million)
% 14.83/6.19 % (918515)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=926306154:i=437:sd=1:aac=none:ss=included_2978 on theBenchmark for (2978ds/437Mi)
% 14.83/6.19 % (918517)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1872382026:i=5202:ss=axioms:sgt=16_2978 on theBenchmark for (2978ds/5202Mi)
% 14.83/6.19 % (918515)Instruction limit reached!
% 14.83/6.19 % (918515)------------------------------
% 14.83/6.19 % (918515)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.83/6.19 % (918515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.83/6.19 % (918515)CaDiCaL version: 2.1.3
% 14.83/6.19 % (918515)Termination reason: Instruction limit
% 14.83/6.19 % (918515)Termination phase: Saturation
% 14.83/6.19 % (918515)Time elapsed: 0.266 s
% 14.83/6.19 % (918515)Peak memory usage: 122 MB
% 14.83/6.19 % (918515)Instructions burned: 439 (million)
% 14.83/6.19 % (918512)Instruction limit reached!
% 14.83/6.19 % (918512)------------------------------
% 14.83/6.19 % (918512)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.83/6.19 % (918512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.83/6.19 % (918512)CaDiCaL version: 2.1.3
% 14.83/6.19 % (918512)Termination reason: Instruction limit
% 14.83/6.19 % (918512)Termination phase: Saturation
% 14.83/6.19 % (918512)Time elapsed: 0.551 s
% 14.83/6.19 % (918512)Peak memory usage: 132 MB
% 14.83/6.19 % (918512)Instructions burned: 908 (million)
% 14.83/6.19 % (918520)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2141983356:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2974 on theBenchmark for (2974ds/134Mi)
% 14.83/6.19 % (918521)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3106142137:st=8:i=592:sd=3:ep=RST:ss=axioms_2972 on theBenchmark for (2972ds/592Mi)
% 14.83/6.19 % (918520)Instruction limit reached!
% 14.83/6.19 % (918520)------------------------------
% 14.83/6.19 % (918520)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.83/6.19 % (918520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.83/6.19 % (918520)CaDiCaL version: 2.1.3
% 14.83/6.19 % (918520)Termination reason: Instruction limit
% 14.83/6.19 % (918520)Termination phase: Preprocessing 2
% 14.83/6.19 % (918520)Time elapsed: 0.125 s
% 14.83/6.19 % (918520)Peak memory usage: 114 MB
% 14.83/6.19 % (918520)Instructions burned: 134 (million)
% 14.83/6.19 % (918524)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2533484982:st=3:i=13193:sd=3:ss=axioms_2971 on theBenchmark for (2971ds/13193Mi)
% 14.83/6.19 % (918505)Instruction limit reached!
% 14.83/6.19 % (918505)------------------------------
% 14.83/6.19 % (918505)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.83/6.19 % (918505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.83/6.19 % (918505)CaDiCaL version: 2.1.3
% 14.83/6.19 % (918505)Termination reason: Instruction limit
% 14.83/6.19 % (918505)Termination phase: Property scanning
% 14.83/6.19 % (918505)Time elapsed: 1.287 s
% 14.83/6.19 % (918505)Peak memory usage: 171 MB
% 14.83/6.19 % (918505)Instructions burned: 2350 (million)
% 14.83/6.19 % (918526)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=1174351724:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2968 on theBenchmark for (2968ds/125Mi)
% 14.83/6.19 % (918521)Instruction limit reached!
% 14.83/6.19 % (918521)------------------------------
% 14.83/6.19 % (918521)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.83/6.19 % (918521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.83/6.19 % (918521)CaDiCaL version: 2.1.3
% 14.83/6.19 % (918521)Termination reason: Instruction limit
% 14.83/6.19 % (918521)Termination phase: Preprocessing 3
% 14.83/6.19 % (918521)Time elapsed: 0.448 s
% 14.83/6.19 % (918521)Peak memory usage: 134 MB
% 14.83/6.19 % (918521)Instructions burned: 593 (million)
% 14.83/6.19 % (918526)Instruction limit reached!
% 14.83/6.19 % (918526)------------------------------
% 14.83/6.19 % (918526)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.83/6.19 % (918526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.83/6.19 % (918526)CaDiCaL version: 2.1.3
% 14.83/6.19 % (918526)Termination reason: Instruction limit
% 14.83/6.19 % (918526)Termination phase: Property scanning
% 14.83/6.19 % (918526)Time elapsed: 0.054 s
% 14.83/6.19 % (918526)Peak memory usage: 112 MB
% 14.83/6.19 % (918526)Instructions burned: 126 (million)
% 14.83/6.19 % (918528)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2738210334:i=134:gtgl=5:slsql=off:gtg=exists_sym_2966 on theBenchmark for (2966ds/134Mi)
% 14.83/6.19 % (918529)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=508425240:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2966 on theBenchmark for (2966ds/141Mi)
% 14.83/6.19 % (918528)Instruction limit reached!
% 14.83/6.19 % (918528)------------------------------
% 14.83/6.19 % (918528)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.83/6.19 % (918528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.83/6.19 % (918528)CaDiCaL version: 2.1.3
% 14.83/6.19 % (918528)Termination reason: Instruction limit
% 14.83/6.19 % (918528)Termination phase: Property scanning
% 14.83/6.19 % (918528)Time elapsed: 0.059 s
% 14.83/6.19 % (918528)Peak memory usage: 112 MB
% 14.83/6.19 % (918528)Instructions burned: 134 (million)
% 14.83/6.19 % (918529)Refutation not found, incomplete strategy
% 14.83/6.19 % (918529)------------------------------
% 14.83/6.19 % (918529)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.83/6.19 % (918529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.83/6.19 % (918529)CaDiCaL version: 2.1.3
% 14.83/6.19 % (918529)Termination reason: Refutation not found, incomplete strategy
% 14.83/6.19 % (918529)Time elapsed: 0.110 s
% 14.83/6.19 % (918529)Peak memory usage: 117 MB
% 14.83/6.19 % (918529)Instructions burned: 124 (million)
% 14.83/6.19 % (918532)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=257233522:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2964 on theBenchmark for (2964ds/431Mi)
% 14.83/6.19 % (918529)------------------------------
% 14.83/6.19 % (918529)------------------------------
% 14.83/6.19 % (918532)Instruction limit reached!
% 14.83/6.19 % (918532)------------------------------
% 14.83/6.19 % (918532)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.83/6.19 % (918532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.83/6.19 % (918532)CaDiCaL version: 2.1.3
% 14.83/6.19 % (918532)Termination reason: Instruction limit
% 14.83/6.19 % (918532)Termination phase: Saturation
% 14.83/6.19 % (918532)Time elapsed: 0.290 s
% 14.83/6.19 % (918532)Peak memory usage: 121 MB
% 14.83/6.19 % (918532)Instructions burned: 432 (million)
% 14.83/6.19 % (918534)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=37080904:i=6060:aac=none:ins=25_2961 on theBenchmark for (2961ds/6060Mi)
% 14.83/6.19 % (918535)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=4168874107:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2959 on theBenchmark for (2959ds/150Mi)
% 14.83/6.19 % (918535)Instruction limit reached!
% 14.83/6.19 % (918535)------------------------------
% 14.83/6.19 % (918535)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.83/6.19 % (918535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.83/6.19 % (918535)CaDiCaL version: 2.1.3
% 14.83/6.19 % (918535)Termination reason: Instruction limit
% 14.83/6.19 % (918535)Termination phase: Preprocessing 1
% 14.83/6.19 % (918535)Time elapsed: 0.130 s
% 14.83/6.19 % (918535)Peak memory usage: 113 MB
% 14.83/6.19 % (918535)Instructions burned: 150 (million)
% 14.83/6.19 % (918538)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2789402356:i=14155:bd=all_2956 on theBenchmark for (2956ds/14155Mi)
% 14.83/6.19 % (918483)First to succeed.
% 14.83/6.19 % (918483)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-918477"
% 14.83/6.19 % (918483)Refutation found. Thanks to Tanya!
% 14.83/6.19 % SZS status Theorem for theBenchmark
% 14.83/6.19 % SZS output start Proof for theBenchmark
% See solution above
% 31.24/6.29 % (918483)------------------------------
% 31.24/6.29 % (918483)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.24/6.29 % (918483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.24/6.29 % (918483)CaDiCaL version: 2.1.3
% 31.24/6.29 % (918483)Termination reason: Refutation
% 31.24/6.29 % (918483)Time elapsed: 3.832 s
% 31.24/6.29 % (918483)Peak memory usage: 339 MB
% 31.24/6.29 % (918483)Instructions burned: 11472 (million)
% 31.24/6.29 % (918483)------------------------------
% 31.24/6.29 % (918483)------------------------------
% 31.24/6.29 % (918477)Success in time 5.322 s
% 31.24/6.29 % Vampire exiting
%------------------------------------------------------------------------------