%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LAT369+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:48:40 AM UTC 2026
% Result : Theorem 2.00s 0.70s
% Output : Refutation 2.00s
% Verified :
% SZS Type : Refutation
% Derivation depth : 35
% Number of leaves : 21
% Syntax : Number of formulae : 282 ( 31 unt; 9 def)
% Number of atoms : 1985 ( 19 equ)
% Maximal formula atoms : 25 ( 7 avg)
% Number of connectives : 2902 (1199 ~;1440 |; 221 &)
% ( 13 <=>; 29 =>; 0 <=; 0 <~>)
% Maximal formula depth : 28 ( 8 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 43 ( 41 usr; 10 prp; 0-3 aty)
% Number of functors : 8 ( 8 usr; 2 con; 0-3 aty)
% Number of variables : 166 ( 0 sgn 162 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [X0] :
( ( v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& v2_lattice3(X0)
& v3_lattice3(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( ( 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(f2,negated_conjecture,
~ ! [X0] :
( ( v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v1_lattice3(X0)
& v2_lattice3(X0)
& v3_lattice3(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( ( 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)],[f1]) ).
fof(f36,axiom,
! [X0] :
( l1_orders_2(X0)
=> ( v2_lattice3(X0)
=> ~ v3_struct_0(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc2_lattice3) ).
fof(f41,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(f63,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(f65,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(f72,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(f82,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(f83,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(f134,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(f137,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(f139,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(f141,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(f175,plain,
! [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) ) ),
inference(pure_predicate_removal,[],[f82]) ).
fof(f196,plain,
! [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))
& v6_waybel_1(X1,X0) ) ) ) ),
inference(pure_predicate_removal,[],[f41]) ).
fof(f218,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,[],[f2]) ).
fof(f219,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,[],[f218]) ).
fof(f262,plain,
! [X0] :
( ~ v3_struct_0(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f36]) ).
fof(f263,plain,
! [X0] :
( ~ v3_struct_0(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f262]) ).
fof(f270,plain,
! [X0] :
( ! [X1] :
( ( v1_funct_1(X1)
& ~ v1_xboole_0(X1)
& v1_funct_2(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,[],[f196]) ).
fof(f271,plain,
! [X0] :
( ! [X1] :
( ( v1_funct_1(X1)
& ~ v1_xboole_0(X1)
& v1_funct_2(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,[],[f270]) ).
fof(f308,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,[],[f63]) ).
fof(f309,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,[],[f308]) ).
fof(f310,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,[],[f65]) ).
fof(f311,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,[],[f310]) ).
fof(f315,plain,
! [X0] :
( ! [X1] :
( l1_orders_2(X1)
| ~ m1_yellow_0(X1,X0) )
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f72]) ).
fof(f319,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_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,[],[f175]) ).
fof(f320,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_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,[],[f319]) ).
fof(f321,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,[],[f83]) ).
fof(f322,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,[],[f321]) ).
fof(f396,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,[],[f137]) ).
fof(f397,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,[],[f396]) ).
fof(f400,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,[],[f139]) ).
fof(f401,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,[],[f400]) ).
fof(f403,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,[],[f141]) ).
fof(f404,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,[],[f403]) ).
fof(f411,plain,
m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0)),
inference(cnf_transformation,[],[f219]) ).
fof(f412,plain,
v7_waybel_1(sK1,sK0),
inference(cnf_transformation,[],[f219]) ).
fof(f413,plain,
v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0)),
inference(cnf_transformation,[],[f219]) ).
fof(f414,plain,
v1_funct_1(sK1),
inference(cnf_transformation,[],[f219]) ).
fof(f415,plain,
v4_waybel_0(k2_yellow_2(sK0,sK0,sK1),sK0),
inference(cnf_transformation,[],[f219]) ).
fof(f416,plain,
~ v1_waybel34(k2_waybel_1(sK0,sK0,sK1),sK0,k2_yellow_2(sK0,sK0,sK1)),
inference(cnf_transformation,[],[f219]) ).
fof(f417,plain,
l1_orders_2(sK0),
inference(cnf_transformation,[],[f219]) ).
fof(f418,plain,
v3_lattice3(sK0),
inference(cnf_transformation,[],[f219]) ).
fof(f419,plain,
v2_lattice3(sK0),
inference(cnf_transformation,[],[f219]) ).
fof(f420,plain,
v1_lattice3(sK0),
inference(cnf_transformation,[],[f219]) ).
fof(f421,plain,
v4_orders_2(sK0),
inference(cnf_transformation,[],[f219]) ).
fof(f422,plain,
v3_orders_2(sK0),
inference(cnf_transformation,[],[f219]) ).
fof(f423,plain,
v2_orders_2(sK0),
inference(cnf_transformation,[],[f219]) ).
fof(f479,plain,
! [X0] :
( ~ v3_struct_0(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f263]) ).
fof(f486,plain,
! [X0,X1] :
( ~ l1_orders_2(X0)
| v3_struct_0(X0)
| ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v7_waybel_1(X1,X0)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| v6_waybel_1(X1,X0) ),
inference(cnf_transformation,[],[f271]) ).
fof(f517,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| v3_struct_0(X1)
| ~ l1_orders_2(X0)
| v3_struct_0(X0)
| m1_yellow_0(k2_yellow_2(X0,X1,X2),X1) ),
inference(cnf_transformation,[],[f309]) ).
fof(f520,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| v3_struct_0(X1)
| ~ l1_orders_2(X0)
| v3_struct_0(X0)
| m2_relset_1(k3_waybel_1(X0,X1,X2),u1_struct_0(k2_yellow_2(X0,X1,X2)),u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f311]) ).
fof(f521,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| v3_struct_0(X1)
| ~ l1_orders_2(X0)
| v3_struct_0(X0)
| 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,[],[f311]) ).
fof(f522,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| v3_struct_0(X1)
| ~ l1_orders_2(X0)
| v3_struct_0(X0)
| v1_funct_1(k3_waybel_1(X0,X1,X2)) ),
inference(cnf_transformation,[],[f311]) ).
fof(f528,plain,
! [X0,X1] :
( ~ l1_orders_2(X0)
| ~ m1_yellow_0(X1,X0)
| l1_orders_2(X1) ),
inference(cnf_transformation,[],[f315]) ).
fof(f540,plain,
! [X0,X1] :
( ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v7_waybel_1(X1,X0)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| ~ l1_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| v3_struct_0(X0)
| v4_orders_2(k2_yellow_2(X0,X0,X1)) ),
inference(cnf_transformation,[],[f320]) ).
fof(f541,plain,
! [X0,X1] :
( ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v7_waybel_1(X1,X0)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| ~ l1_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| v3_struct_0(X0)
| v3_orders_2(k2_yellow_2(X0,X0,X1)) ),
inference(cnf_transformation,[],[f320]) ).
fof(f542,plain,
! [X0,X1] :
( ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v7_waybel_1(X1,X0)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| ~ l1_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| v3_struct_0(X0)
| v2_orders_2(k2_yellow_2(X0,X0,X1)) ),
inference(cnf_transformation,[],[f320]) ).
fof(f545,plain,
! [X0,X1] :
( ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v6_waybel_1(X1,X0)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| v3_lattice3(k2_yellow_2(X0,X0,X1)) ),
inference(cnf_transformation,[],[f322]) ).
fof(f546,plain,
! [X0,X1] :
( ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v6_waybel_1(X1,X0)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| v2_lattice3(k2_yellow_2(X0,X0,X1)) ),
inference(cnf_transformation,[],[f322]) ).
fof(f547,plain,
! [X0,X1] :
( ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v6_waybel_1(X1,X0)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| v1_lattice3(k2_yellow_2(X0,X0,X1)) ),
inference(cnf_transformation,[],[f322]) ).
fof(f839,plain,
! [X2,X0,X1] :
( m1_relset_1(X2,X0,X1)
| ~ m2_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f134]) ).
fof(f842,plain,
! [X2,X0,X1] :
( ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ l1_orders_2(X1)
| ~ v3_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v17_waybel_0(X2,X0,X1)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ v22_waybel_0(X2,X0,X1)
| v1_waybel34(k1_waybel34(X0,X1,X2),X1,X0) ),
inference(cnf_transformation,[],[f397]) ).
fof(f844,plain,
! [X0,X1] :
( ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v7_waybel_1(X1,X0)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| k2_waybel_1(X0,X0,X1) = k1_waybel34(k2_yellow_2(X0,X0,X1),X0,k3_waybel_1(X0,X0,X1)) ),
inference(cnf_transformation,[],[f401]) ).
fof(f846,plain,
! [X0,X1] :
( ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v7_waybel_1(X1,X0)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| v17_waybel_0(k3_waybel_1(X0,X0,X1),k2_yellow_2(X0,X0,X1),X0) ),
inference(cnf_transformation,[],[f401]) ).
fof(f850,plain,
! [X0,X1] :
( ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v7_waybel_1(X1,X0)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(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) ),
inference(cnf_transformation,[],[f404]) ).
fof(f856,plain,
~ v3_lattice3(sK0),
inference(consistent_polarity_flipping,[],[f418]) ).
fof(f857,plain,
v1_waybel34(k2_waybel_1(sK0,sK0,sK1),sK0,k2_yellow_2(sK0,sK0,sK1)),
inference(consistent_polarity_flipping,[],[f416]) ).
fof(f906,plain,
! [X0,X1] :
( ~ v7_waybel_1(X1,X0)
| v3_struct_0(X0)
| m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ l1_orders_2(X0)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| v6_waybel_1(X1,X0) ),
inference(consistent_polarity_flipping,[],[f486]) ).
fof(f931,plain,
! [X2,X0,X1] :
( ~ m1_yellow_0(k2_yellow_2(X0,X1,X2),X1)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| v3_struct_0(X1)
| ~ l1_orders_2(X0)
| v3_struct_0(X0)
| m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(consistent_polarity_flipping,[],[f517]) ).
fof(f932,plain,
! [X2,X0,X1] :
( m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| v3_struct_0(X1)
| ~ l1_orders_2(X0)
| v3_struct_0(X0)
| v1_funct_1(k3_waybel_1(X0,X1,X2)) ),
inference(consistent_polarity_flipping,[],[f522]) ).
fof(f933,plain,
! [X2,X0,X1] :
( v1_funct_2(k3_waybel_1(X0,X1,X2),u1_struct_0(k2_yellow_2(X0,X1,X2)),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| v3_struct_0(X1)
| ~ l1_orders_2(X0)
| v3_struct_0(X0)
| m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(consistent_polarity_flipping,[],[f521]) ).
fof(f934,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))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| v3_struct_0(X1)
| ~ l1_orders_2(X0)
| v3_struct_0(X0)
| m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(consistent_polarity_flipping,[],[f520]) ).
fof(f940,plain,
! [X0,X1] :
( m1_yellow_0(X1,X0)
| ~ l1_orders_2(X0)
| l1_orders_2(X1) ),
inference(consistent_polarity_flipping,[],[f528]) ).
fof(f948,plain,
! [X0,X1] :
( ~ v7_waybel_1(X1,X0)
| m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| ~ l1_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| v3_struct_0(X0)
| v2_orders_2(k2_yellow_2(X0,X0,X1)) ),
inference(consistent_polarity_flipping,[],[f542]) ).
fof(f949,plain,
! [X0,X1] :
( ~ v7_waybel_1(X1,X0)
| m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| ~ l1_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| v3_struct_0(X0)
| v3_orders_2(k2_yellow_2(X0,X0,X1)) ),
inference(consistent_polarity_flipping,[],[f541]) ).
fof(f950,plain,
! [X0,X1] :
( ~ v7_waybel_1(X1,X0)
| m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| ~ l1_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| v3_struct_0(X0)
| v4_orders_2(k2_yellow_2(X0,X0,X1)) ),
inference(consistent_polarity_flipping,[],[f540]) ).
fof(f965,plain,
! [X0,X1] :
( ~ v6_waybel_1(X1,X0)
| m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| ~ l1_orders_2(X0)
| v3_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| v1_lattice3(k2_yellow_2(X0,X0,X1)) ),
inference(consistent_polarity_flipping,[],[f547]) ).
fof(f966,plain,
! [X0,X1] :
( ~ v6_waybel_1(X1,X0)
| m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| ~ l1_orders_2(X0)
| v3_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| v2_lattice3(k2_yellow_2(X0,X0,X1)) ),
inference(consistent_polarity_flipping,[],[f546]) ).
fof(f967,plain,
! [X0,X1] :
( ~ v3_lattice3(k2_yellow_2(X0,X0,X1))
| ~ v6_waybel_1(X1,X0)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| ~ l1_orders_2(X0)
| v3_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) ),
inference(consistent_polarity_flipping,[],[f545]) ).
fof(f1118,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,X0,X1)
| ~ m2_relset_1(X2,X0,X1) ),
inference(consistent_polarity_flipping,[],[f839]) ).
fof(f1121,plain,
! [X2,X0,X1] :
( ~ v1_waybel34(k1_waybel34(X0,X1,X2),X1,X0)
| v3_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ l1_orders_2(X1)
| v3_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v17_waybel_0(X2,X0,X1)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| v22_waybel_0(X2,X0,X1)
| ~ l1_orders_2(X0) ),
inference(consistent_polarity_flipping,[],[f842]) ).
fof(f1124,plain,
! [X0,X1] :
( v17_waybel_0(k3_waybel_1(X0,X0,X1),k2_yellow_2(X0,X0,X1),X0)
| v3_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v7_waybel_1(X1,X0)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| ~ l1_orders_2(X0) ),
inference(consistent_polarity_flipping,[],[f846]) ).
fof(f1126,plain,
! [X0,X1] :
( ~ v7_waybel_1(X1,X0)
| v3_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ l1_orders_2(X0)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| k2_waybel_1(X0,X0,X1) = k1_waybel34(k2_yellow_2(X0,X0,X1),X0,k3_waybel_1(X0,X0,X1)) ),
inference(consistent_polarity_flipping,[],[f844]) ).
fof(f1128,plain,
! [X0,X1] :
( ~ v22_waybel_0(k3_waybel_1(X0,X0,X1),k2_yellow_2(X0,X0,X1),X0)
| v3_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v7_waybel_1(X1,X0)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| ~ l1_orders_2(X0)
| ~ v4_waybel_0(k2_yellow_2(X0,X0,X1),X0) ),
inference(consistent_polarity_flipping,[],[f850]) ).
fof(f1400,definition,
( spl32_14
<=> v3_struct_0(sK0) ),
introduced(definition,[new_symbols(definition,[spl32_14])],[avatar_definition]) ).
fof(f1401,plain,
( ~ v3_struct_0(sK0)
| spl32_14 ),
inference(avatar_component_clause,[],[f1400]) ).
fof(f1402,plain,
( v3_struct_0(sK0)
| ~ spl32_14 ),
inference(avatar_component_clause,[],[f1400]) ).
fof(f1836,plain,
( v3_struct_0(sK0)
| m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ l1_orders_2(sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| v6_waybel_1(sK1,sK0) ),
inference(resolution,[],[f906,f412]) ).
fof(f1842,plain,
( v3_struct_0(sK0)
| m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| v6_waybel_1(sK1,sK0) ),
inference(forward_subsumption_resolution,[],[f1836,f417]) ).
fof(f1843,plain,
( v3_struct_0(sK0)
| m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| v6_waybel_1(sK1,sK0) ),
inference(forward_subsumption_resolution,[],[f1842,f413]) ).
fof(f1844,plain,
( v3_struct_0(sK0)
| m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| v6_waybel_1(sK1,sK0) ),
inference(forward_subsumption_resolution,[],[f1843,f414]) ).
fof(f1846,definition,
( spl32_36
<=> v6_waybel_1(sK1,sK0) ),
introduced(definition,[new_symbols(definition,[spl32_36])],[avatar_definition]) ).
fof(f1848,plain,
( v6_waybel_1(sK1,sK0)
| ~ spl32_36 ),
inference(avatar_component_clause,[],[f1846]) ).
fof(f1850,definition,
( spl32_37
<=> m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0)) ),
introduced(definition,[new_symbols(definition,[spl32_37])],[avatar_definition]) ).
fof(f1851,plain,
( ~ m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| spl32_37 ),
inference(avatar_component_clause,[],[f1850]) ).
fof(f1852,plain,
( m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl32_37 ),
inference(avatar_component_clause,[],[f1850]) ).
fof(f1853,plain,
( spl32_36
| spl32_37
| spl32_14 ),
inference(avatar_split_clause,[],[f1844,f1400,f1850,f1846]) ).
fof(f1890,plain,
( ~ v2_lattice3(sK0)
| ~ l1_orders_2(sK0)
| ~ spl32_14 ),
inference(resolution,[],[f1402,f479]) ).
fof(f1893,plain,
( ~ l1_orders_2(sK0)
| ~ spl32_14 ),
inference(forward_subsumption_resolution,[],[f1890,f419]) ).
fof(f1896,plain,
( $false
| ~ spl32_14 ),
inference(forward_subsumption_resolution,[],[f1893,f417]) ).
fof(f1897,plain,
~ spl32_14,
inference(avatar_contradiction_clause,[],[f1896]) ).
fof(f1968,plain,
( ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl32_37 ),
inference(resolution,[],[f1852,f1118]) ).
fof(f1969,plain,
( $false
| ~ spl32_37 ),
inference(forward_subsumption_resolution,[],[f1968,f411]) ).
fof(f1970,plain,
~ spl32_37,
inference(avatar_contradiction_clause,[],[f1969]) ).
fof(f1972,plain,
( ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| v3_struct_0(sK0)
| ~ l1_orders_2(sK0)
| v3_struct_0(sK0)
| v1_funct_1(k3_waybel_1(sK0,sK0,sK1))
| spl32_37 ),
inference(resolution,[],[f1851,f932]) ).
fof(f1978,plain,
( ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| v3_struct_0(sK0)
| v1_funct_1(k3_waybel_1(sK0,sK0,sK1))
| spl32_37 ),
inference(duplicate_literal_removal,[],[f1972]) ).
fof(f1980,plain,
( ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| v3_struct_0(sK0)
| v1_funct_1(k3_waybel_1(sK0,sK0,sK1))
| spl32_37 ),
inference(forward_subsumption_resolution,[],[f1978,f413]) ).
fof(f1982,plain,
( ~ l1_orders_2(sK0)
| v3_struct_0(sK0)
| v1_funct_1(k3_waybel_1(sK0,sK0,sK1))
| spl32_37 ),
inference(forward_subsumption_resolution,[],[f1980,f414]) ).
fof(f1984,plain,
( v3_struct_0(sK0)
| v1_funct_1(k3_waybel_1(sK0,sK0,sK1))
| spl32_37 ),
inference(forward_subsumption_resolution,[],[f1982,f417]) ).
fof(f1986,plain,
( v1_funct_1(k3_waybel_1(sK0,sK0,sK1))
| spl32_14
| spl32_37 ),
inference(forward_subsumption_resolution,[],[f1984,f1401]) ).
fof(f1990,plain,
! [X2,X0,X1] :
( ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_1(X0)
| ~ l1_orders_2(X2)
| v3_struct_0(X2)
| ~ l1_orders_2(X1)
| v3_struct_0(X1)
| m1_relset_1(X0,u1_struct_0(X1),u1_struct_0(X2))
| ~ l1_orders_2(X2)
| l1_orders_2(k2_yellow_2(X1,X2,X0)) ),
inference(resolution,[],[f931,f940]) ).
fof(f1991,plain,
! [X2,X0,X1] :
( m1_relset_1(X0,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_1(X0)
| ~ l1_orders_2(X2)
| v3_struct_0(X2)
| ~ l1_orders_2(X1)
| v3_struct_0(X1)
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(X2))
| l1_orders_2(k2_yellow_2(X1,X2,X0)) ),
inference(duplicate_literal_removal,[],[f1990]) ).
fof(f2085,plain,
( m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| v3_struct_0(sK0)
| v2_orders_2(k2_yellow_2(sK0,sK0,sK1)) ),
inference(resolution,[],[f948,f412]) ).
fof(f2093,plain,
( ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| v3_struct_0(sK0)
| v2_orders_2(k2_yellow_2(sK0,sK0,sK1))
| spl32_37 ),
inference(forward_subsumption_resolution,[],[f2085,f1851]) ).
fof(f2097,plain,
( ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| v3_struct_0(sK0)
| v2_orders_2(k2_yellow_2(sK0,sK0,sK1))
| spl32_37 ),
inference(forward_subsumption_resolution,[],[f2093,f413]) ).
fof(f2101,plain,
( ~ l1_orders_2(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| v3_struct_0(sK0)
| v2_orders_2(k2_yellow_2(sK0,sK0,sK1))
| spl32_37 ),
inference(forward_subsumption_resolution,[],[f2097,f414]) ).
fof(f2102,plain,
( ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| v3_struct_0(sK0)
| v2_orders_2(k2_yellow_2(sK0,sK0,sK1))
| spl32_37 ),
inference(forward_subsumption_resolution,[],[f2101,f417]) ).
fof(f2103,plain,
( ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| v3_struct_0(sK0)
| v2_orders_2(k2_yellow_2(sK0,sK0,sK1))
| spl32_37 ),
inference(forward_subsumption_resolution,[],[f2102,f421]) ).
fof(f2104,plain,
( ~ v2_orders_2(sK0)
| v3_struct_0(sK0)
| v2_orders_2(k2_yellow_2(sK0,sK0,sK1))
| spl32_37 ),
inference(forward_subsumption_resolution,[],[f2103,f422]) ).
fof(f2105,plain,
( v3_struct_0(sK0)
| v2_orders_2(k2_yellow_2(sK0,sK0,sK1))
| spl32_37 ),
inference(forward_subsumption_resolution,[],[f2104,f423]) ).
fof(f2106,plain,
( v2_orders_2(k2_yellow_2(sK0,sK0,sK1))
| spl32_14
| spl32_37 ),
inference(forward_subsumption_resolution,[],[f2105,f1401]) ).
fof(f2108,plain,
( m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| v3_struct_0(sK0)
| v3_orders_2(k2_yellow_2(sK0,sK0,sK1)) ),
inference(resolution,[],[f949,f412]) ).
fof(f2116,plain,
( ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| v3_struct_0(sK0)
| v3_orders_2(k2_yellow_2(sK0,sK0,sK1))
| spl32_37 ),
inference(forward_subsumption_resolution,[],[f2108,f1851]) ).
fof(f2120,plain,
( ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| v3_struct_0(sK0)
| v3_orders_2(k2_yellow_2(sK0,sK0,sK1))
| spl32_37 ),
inference(forward_subsumption_resolution,[],[f2116,f413]) ).
fof(f2124,plain,
( ~ l1_orders_2(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| v3_struct_0(sK0)
| v3_orders_2(k2_yellow_2(sK0,sK0,sK1))
| spl32_37 ),
inference(forward_subsumption_resolution,[],[f2120,f414]) ).
fof(f2125,plain,
( ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| v3_struct_0(sK0)
| v3_orders_2(k2_yellow_2(sK0,sK0,sK1))
| spl32_37 ),
inference(forward_subsumption_resolution,[],[f2124,f417]) ).
fof(f2126,plain,
( ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| v3_struct_0(sK0)
| v3_orders_2(k2_yellow_2(sK0,sK0,sK1))
| spl32_37 ),
inference(forward_subsumption_resolution,[],[f2125,f421]) ).
fof(f2127,plain,
( ~ v2_orders_2(sK0)
| v3_struct_0(sK0)
| v3_orders_2(k2_yellow_2(sK0,sK0,sK1))
| spl32_37 ),
inference(forward_subsumption_resolution,[],[f2126,f422]) ).
fof(f2128,plain,
( v3_struct_0(sK0)
| v3_orders_2(k2_yellow_2(sK0,sK0,sK1))
| spl32_37 ),
inference(forward_subsumption_resolution,[],[f2127,f423]) ).
fof(f2129,plain,
( v3_orders_2(k2_yellow_2(sK0,sK0,sK1))
| spl32_14
| spl32_37 ),
inference(forward_subsumption_resolution,[],[f2128,f1401]) ).
fof(f2131,plain,
( m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| v3_struct_0(sK0)
| v4_orders_2(k2_yellow_2(sK0,sK0,sK1)) ),
inference(resolution,[],[f950,f412]) ).
fof(f2139,plain,
( ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| v3_struct_0(sK0)
| v4_orders_2(k2_yellow_2(sK0,sK0,sK1))
| spl32_37 ),
inference(forward_subsumption_resolution,[],[f2131,f1851]) ).
fof(f2143,plain,
( ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| v3_struct_0(sK0)
| v4_orders_2(k2_yellow_2(sK0,sK0,sK1))
| spl32_37 ),
inference(forward_subsumption_resolution,[],[f2139,f413]) ).
fof(f2147,plain,
( ~ l1_orders_2(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| v3_struct_0(sK0)
| v4_orders_2(k2_yellow_2(sK0,sK0,sK1))
| spl32_37 ),
inference(forward_subsumption_resolution,[],[f2143,f414]) ).
fof(f2148,plain,
( ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| v3_struct_0(sK0)
| v4_orders_2(k2_yellow_2(sK0,sK0,sK1))
| spl32_37 ),
inference(forward_subsumption_resolution,[],[f2147,f417]) ).
fof(f2149,plain,
( ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| v3_struct_0(sK0)
| v4_orders_2(k2_yellow_2(sK0,sK0,sK1))
| spl32_37 ),
inference(forward_subsumption_resolution,[],[f2148,f421]) ).
fof(f2150,plain,
( ~ v2_orders_2(sK0)
| v3_struct_0(sK0)
| v4_orders_2(k2_yellow_2(sK0,sK0,sK1))
| spl32_37 ),
inference(forward_subsumption_resolution,[],[f2149,f422]) ).
fof(f2151,plain,
( v3_struct_0(sK0)
| v4_orders_2(k2_yellow_2(sK0,sK0,sK1))
| spl32_37 ),
inference(forward_subsumption_resolution,[],[f2150,f423]) ).
fof(f2152,plain,
( v4_orders_2(k2_yellow_2(sK0,sK0,sK1))
| spl32_14
| spl32_37 ),
inference(forward_subsumption_resolution,[],[f2151,f1401]) ).
fof(f2479,definition,
( spl32_63
<=> l1_orders_2(k2_yellow_2(sK0,sK0,sK1)) ),
introduced(definition,[new_symbols(definition,[spl32_63])],[avatar_definition]) ).
fof(f2795,plain,
( m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ spl32_36 ),
inference(resolution,[],[f965,f1848]) ).
fof(f2801,plain,
( ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ spl32_36
| spl32_37 ),
inference(forward_subsumption_resolution,[],[f2795,f1851]) ).
fof(f2807,plain,
( ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ spl32_36
| spl32_37 ),
inference(forward_subsumption_resolution,[],[f2801,f413]) ).
fof(f2813,plain,
( ~ l1_orders_2(sK0)
| v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ spl32_36
| spl32_37 ),
inference(forward_subsumption_resolution,[],[f2807,f414]) ).
fof(f2819,plain,
( v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ spl32_36
| spl32_37 ),
inference(forward_subsumption_resolution,[],[f2813,f417]) ).
fof(f2825,plain,
( ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ spl32_36
| spl32_37 ),
inference(forward_subsumption_resolution,[],[f2819,f856]) ).
fof(f2830,plain,
( ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ spl32_36
| spl32_37 ),
inference(forward_subsumption_resolution,[],[f2825,f419]) ).
fof(f2831,plain,
( ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ spl32_36
| spl32_37 ),
inference(forward_subsumption_resolution,[],[f2830,f420]) ).
fof(f2832,plain,
( ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ spl32_36
| spl32_37 ),
inference(forward_subsumption_resolution,[],[f2831,f421]) ).
fof(f2833,plain,
( ~ v2_orders_2(sK0)
| v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ spl32_36
| spl32_37 ),
inference(forward_subsumption_resolution,[],[f2832,f422]) ).
fof(f2834,plain,
( v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ spl32_36
| spl32_37 ),
inference(forward_subsumption_resolution,[],[f2833,f423]) ).
fof(f2840,plain,
( m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ spl32_36 ),
inference(resolution,[],[f966,f1848]) ).
fof(f2846,plain,
( ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ spl32_36
| spl32_37 ),
inference(forward_subsumption_resolution,[],[f2840,f1851]) ).
fof(f2852,plain,
( ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ spl32_36
| spl32_37 ),
inference(forward_subsumption_resolution,[],[f2846,f413]) ).
fof(f2858,plain,
( ~ l1_orders_2(sK0)
| v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ spl32_36
| spl32_37 ),
inference(forward_subsumption_resolution,[],[f2852,f414]) ).
fof(f2864,plain,
( v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ spl32_36
| spl32_37 ),
inference(forward_subsumption_resolution,[],[f2858,f417]) ).
fof(f2870,plain,
( ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ spl32_36
| spl32_37 ),
inference(forward_subsumption_resolution,[],[f2864,f856]) ).
fof(f2875,plain,
( ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ spl32_36
| spl32_37 ),
inference(forward_subsumption_resolution,[],[f2870,f419]) ).
fof(f2876,plain,
( ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ spl32_36
| spl32_37 ),
inference(forward_subsumption_resolution,[],[f2875,f420]) ).
fof(f2877,plain,
( ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ spl32_36
| spl32_37 ),
inference(forward_subsumption_resolution,[],[f2876,f421]) ).
fof(f2878,plain,
( ~ v2_orders_2(sK0)
| v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ spl32_36
| spl32_37 ),
inference(forward_subsumption_resolution,[],[f2877,f422]) ).
fof(f2879,plain,
( v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ spl32_36
| spl32_37 ),
inference(forward_subsumption_resolution,[],[f2878,f423]) ).
fof(f3384,plain,
( v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ l1_orders_2(sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| k2_waybel_1(sK0,sK0,sK1) = k1_waybel34(k2_yellow_2(sK0,sK0,sK1),sK0,k3_waybel_1(sK0,sK0,sK1)) ),
inference(resolution,[],[f1126,f412]) ).
fof(f3392,plain,
( ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ l1_orders_2(sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| k2_waybel_1(sK0,sK0,sK1) = k1_waybel34(k2_yellow_2(sK0,sK0,sK1),sK0,k3_waybel_1(sK0,sK0,sK1)) ),
inference(forward_subsumption_resolution,[],[f3384,f856]) ).
fof(f3396,plain,
( ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ l1_orders_2(sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| k2_waybel_1(sK0,sK0,sK1) = k1_waybel34(k2_yellow_2(sK0,sK0,sK1),sK0,k3_waybel_1(sK0,sK0,sK1)) ),
inference(forward_subsumption_resolution,[],[f3392,f419]) ).
fof(f3400,plain,
( ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ l1_orders_2(sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| k2_waybel_1(sK0,sK0,sK1) = k1_waybel34(k2_yellow_2(sK0,sK0,sK1),sK0,k3_waybel_1(sK0,sK0,sK1)) ),
inference(forward_subsumption_resolution,[],[f3396,f420]) ).
fof(f3404,plain,
( ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ l1_orders_2(sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| k2_waybel_1(sK0,sK0,sK1) = k1_waybel34(k2_yellow_2(sK0,sK0,sK1),sK0,k3_waybel_1(sK0,sK0,sK1)) ),
inference(forward_subsumption_resolution,[],[f3400,f421]) ).
fof(f3406,plain,
( ~ v2_orders_2(sK0)
| ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ l1_orders_2(sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| k2_waybel_1(sK0,sK0,sK1) = k1_waybel34(k2_yellow_2(sK0,sK0,sK1),sK0,k3_waybel_1(sK0,sK0,sK1)) ),
inference(forward_subsumption_resolution,[],[f3404,f422]) ).
fof(f3407,plain,
( ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ l1_orders_2(sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| k2_waybel_1(sK0,sK0,sK1) = k1_waybel34(k2_yellow_2(sK0,sK0,sK1),sK0,k3_waybel_1(sK0,sK0,sK1)) ),
inference(forward_subsumption_resolution,[],[f3406,f423]) ).
fof(f3408,plain,
( ~ l1_orders_2(sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| k2_waybel_1(sK0,sK0,sK1) = k1_waybel34(k2_yellow_2(sK0,sK0,sK1),sK0,k3_waybel_1(sK0,sK0,sK1)) ),
inference(forward_subsumption_resolution,[],[f3407,f411]) ).
fof(f3409,plain,
( ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| k2_waybel_1(sK0,sK0,sK1) = k1_waybel34(k2_yellow_2(sK0,sK0,sK1),sK0,k3_waybel_1(sK0,sK0,sK1)) ),
inference(forward_subsumption_resolution,[],[f3408,f417]) ).
fof(f3410,plain,
( ~ v1_funct_1(sK1)
| k2_waybel_1(sK0,sK0,sK1) = k1_waybel34(k2_yellow_2(sK0,sK0,sK1),sK0,k3_waybel_1(sK0,sK0,sK1)) ),
inference(forward_subsumption_resolution,[],[f3409,f413]) ).
fof(f3411,plain,
k2_waybel_1(sK0,sK0,sK1) = k1_waybel34(k2_yellow_2(sK0,sK0,sK1),sK0,k3_waybel_1(sK0,sK0,sK1)),
inference(forward_subsumption_resolution,[],[f3410,f414]) ).
fof(f3978,plain,
( ~ v1_waybel34(k2_waybel_1(sK0,sK0,sK1),sK0,k2_yellow_2(sK0,sK0,sK1))
| v3_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v4_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ v3_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ v2_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ l1_orders_2(sK0)
| v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| ~ m2_relset_1(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v17_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ v1_funct_2(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_1(k3_waybel_1(sK0,sK0,sK1))
| v22_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ l1_orders_2(k2_yellow_2(sK0,sK0,sK1)) ),
inference(superposition,[],[f1121,f3411]) ).
fof(f5581,plain,
( ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| v3_struct_0(sK0)
| ~ l1_orders_2(sK0)
| v3_struct_0(sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| spl32_37 ),
inference(resolution,[],[f1991,f1851]) ).
fof(f5603,plain,
( ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| v3_struct_0(sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| spl32_37 ),
inference(duplicate_literal_removal,[],[f5581]) ).
fof(f5613,plain,
( ~ l1_orders_2(sK0)
| v3_struct_0(sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| spl32_37 ),
inference(forward_subsumption_resolution,[],[f5603,f414]) ).
fof(f5623,plain,
( v3_struct_0(sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| spl32_37 ),
inference(forward_subsumption_resolution,[],[f5613,f417]) ).
fof(f5626,plain,
( ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| spl32_14
| spl32_37 ),
inference(forward_subsumption_resolution,[],[f5623,f1401]) ).
fof(f5628,plain,
( l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| spl32_14
| spl32_37 ),
inference(forward_subsumption_resolution,[],[f5626,f413]) ).
fof(f5652,plain,
( v3_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v2_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v4_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ v3_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ v2_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ l1_orders_2(sK0)
| v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| ~ m2_relset_1(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v17_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ v1_funct_2(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_1(k3_waybel_1(sK0,sK0,sK1))
| v22_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ l1_orders_2(k2_yellow_2(sK0,sK0,sK1)) ),
inference(forward_subsumption_resolution,[],[f3978,f857]) ).
fof(f5659,definition,
( spl32_182
<=> v3_lattice3(k2_yellow_2(sK0,sK0,sK1)) ),
introduced(definition,[new_symbols(definition,[spl32_182])],[avatar_definition]) ).
fof(f5661,plain,
( v3_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ spl32_182 ),
inference(avatar_component_clause,[],[f5659]) ).
fof(f5677,plain,
( spl32_63
| spl32_14
| spl32_37 ),
inference(avatar_split_clause,[],[f5628,f1850,f1400,f2479]) ).
fof(f5701,plain,
( v3_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v1_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v4_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ v3_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ v2_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ l1_orders_2(sK0)
| v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| ~ m2_relset_1(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v17_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ v1_funct_2(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_1(k3_waybel_1(sK0,sK0,sK1))
| v22_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ spl32_36
| spl32_37 ),
inference(forward_subsumption_resolution,[],[f5652,f2879]) ).
fof(f5744,plain,
( v3_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v4_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ v3_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ v2_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ l1_orders_2(sK0)
| v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| ~ m2_relset_1(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v17_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ v1_funct_2(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_1(k3_waybel_1(sK0,sK0,sK1))
| v22_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ spl32_36
| spl32_37 ),
inference(forward_subsumption_resolution,[],[f5701,f2834]) ).
fof(f5781,plain,
( v3_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v3_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ v2_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ l1_orders_2(sK0)
| v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| ~ m2_relset_1(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v17_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ v1_funct_2(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_1(k3_waybel_1(sK0,sK0,sK1))
| v22_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| spl32_14
| ~ spl32_36
| spl32_37 ),
inference(forward_subsumption_resolution,[],[f5744,f2152]) ).
fof(f5860,plain,
( v3_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v2_orders_2(k2_yellow_2(sK0,sK0,sK1))
| ~ l1_orders_2(sK0)
| v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| ~ m2_relset_1(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v17_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ v1_funct_2(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_1(k3_waybel_1(sK0,sK0,sK1))
| v22_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| spl32_14
| ~ spl32_36
| spl32_37 ),
inference(forward_subsumption_resolution,[],[f5781,f2129]) ).
fof(f5883,plain,
( v3_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ l1_orders_2(sK0)
| v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| ~ m2_relset_1(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v17_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ v1_funct_2(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_1(k3_waybel_1(sK0,sK0,sK1))
| v22_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| spl32_14
| ~ spl32_36
| spl32_37 ),
inference(forward_subsumption_resolution,[],[f5860,f2106]) ).
fof(f5898,plain,
( v3_lattice3(k2_yellow_2(sK0,sK0,sK1))
| v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| ~ m2_relset_1(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v17_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ v1_funct_2(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_1(k3_waybel_1(sK0,sK0,sK1))
| v22_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| spl32_14
| ~ spl32_36
| spl32_37 ),
inference(forward_subsumption_resolution,[],[f5883,f417]) ).
fof(f5913,plain,
( v3_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| ~ m2_relset_1(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v17_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ v1_funct_2(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_1(k3_waybel_1(sK0,sK0,sK1))
| v22_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| spl32_14
| ~ spl32_36
| spl32_37 ),
inference(forward_subsumption_resolution,[],[f5898,f856]) ).
fof(f5928,plain,
( v3_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| ~ m2_relset_1(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v17_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ v1_funct_2(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_1(k3_waybel_1(sK0,sK0,sK1))
| v22_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| spl32_14
| ~ spl32_36
| spl32_37 ),
inference(forward_subsumption_resolution,[],[f5913,f419]) ).
fof(f5943,plain,
( v3_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| ~ m2_relset_1(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v17_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ v1_funct_2(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_1(k3_waybel_1(sK0,sK0,sK1))
| v22_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| spl32_14
| ~ spl32_36
| spl32_37 ),
inference(forward_subsumption_resolution,[],[f5928,f420]) ).
fof(f5958,plain,
( v3_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| ~ m2_relset_1(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v17_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ v1_funct_2(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_1(k3_waybel_1(sK0,sK0,sK1))
| v22_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| spl32_14
| ~ spl32_36
| spl32_37 ),
inference(forward_subsumption_resolution,[],[f5943,f421]) ).
fof(f5973,plain,
( v3_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ v2_orders_2(sK0)
| ~ m2_relset_1(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v17_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ v1_funct_2(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_1(k3_waybel_1(sK0,sK0,sK1))
| v22_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| spl32_14
| ~ spl32_36
| spl32_37 ),
inference(forward_subsumption_resolution,[],[f5958,f422]) ).
fof(f5983,definition,
( spl32_207
<=> v1_funct_2(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0)) ),
introduced(definition,[new_symbols(definition,[spl32_207])],[avatar_definition]) ).
fof(f5984,plain,
( ~ v1_funct_2(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| spl32_207 ),
inference(avatar_component_clause,[],[f5983]) ).
fof(f5988,definition,
( spl32_208
<=> m2_relset_1(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0)) ),
introduced(definition,[new_symbols(definition,[spl32_208])],[avatar_definition]) ).
fof(f5989,plain,
( ~ m2_relset_1(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| spl32_208 ),
inference(avatar_component_clause,[],[f5988]) ).
fof(f6012,plain,
( v3_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ m2_relset_1(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v17_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ v1_funct_2(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v1_funct_1(k3_waybel_1(sK0,sK0,sK1))
| v22_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| spl32_14
| ~ spl32_36
| spl32_37 ),
inference(forward_subsumption_resolution,[],[f5973,f423]) ).
fof(f6020,definition,
( spl32_212
<=> v17_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0) ),
introduced(definition,[new_symbols(definition,[spl32_212])],[avatar_definition]) ).
fof(f6022,plain,
( ~ v17_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| spl32_212 ),
inference(avatar_component_clause,[],[f6020]) ).
fof(f6059,plain,
( v3_lattice3(k2_yellow_2(sK0,sK0,sK1))
| ~ m2_relset_1(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| ~ v17_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ v1_funct_2(k3_waybel_1(sK0,sK0,sK1),u1_struct_0(k2_yellow_2(sK0,sK0,sK1)),u1_struct_0(sK0))
| v22_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ l1_orders_2(k2_yellow_2(sK0,sK0,sK1))
| spl32_14
| ~ spl32_36
| spl32_37 ),
inference(forward_subsumption_resolution,[],[f6012,f1986]) ).
fof(f6061,definition,
( spl32_220
<=> v22_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0) ),
introduced(definition,[new_symbols(definition,[spl32_220])],[avatar_definition]) ).
fof(f6063,plain,
( v22_waybel_0(k3_waybel_1(sK0,sK0,sK1),k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ spl32_220 ),
inference(avatar_component_clause,[],[f6061]) ).
fof(f6064,plain,
( ~ spl32_63
| spl32_220
| ~ spl32_207
| ~ spl32_212
| ~ spl32_208
| spl32_182
| spl32_14
| ~ spl32_36
| spl32_37 ),
inference(avatar_split_clause,[],[f6059,f1850,f1846,f1400,f5659,f5988,f6020,f5983,f6061,f2479]) ).
fof(f7116,plain,
( ~ v6_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl32_182 ),
inference(resolution,[],[f5661,f967]) ).
fof(f7124,plain,
( ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl32_36
| ~ spl32_182 ),
inference(forward_subsumption_resolution,[],[f7116,f1848]) ).
fof(f7128,plain,
( ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl32_36
| ~ spl32_182 ),
inference(forward_subsumption_resolution,[],[f7124,f413]) ).
fof(f7132,plain,
( ~ l1_orders_2(sK0)
| v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl32_36
| ~ spl32_182 ),
inference(forward_subsumption_resolution,[],[f7128,f414]) ).
fof(f7136,plain,
( v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl32_36
| ~ spl32_182 ),
inference(forward_subsumption_resolution,[],[f7132,f417]) ).
fof(f7140,plain,
( ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl32_36
| ~ spl32_182 ),
inference(forward_subsumption_resolution,[],[f7136,f856]) ).
fof(f7144,plain,
( ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl32_36
| ~ spl32_182 ),
inference(forward_subsumption_resolution,[],[f7140,f419]) ).
fof(f7149,plain,
( ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl32_36
| ~ spl32_182 ),
inference(forward_subsumption_resolution,[],[f7144,f420]) ).
fof(f7153,plain,
( ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl32_36
| ~ spl32_182 ),
inference(forward_subsumption_resolution,[],[f7149,f421]) ).
fof(f7155,plain,
( ~ v2_orders_2(sK0)
| m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl32_36
| ~ spl32_182 ),
inference(forward_subsumption_resolution,[],[f7153,f422]) ).
fof(f7157,plain,
( m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ spl32_36
| ~ spl32_182 ),
inference(forward_subsumption_resolution,[],[f7155,f423]) ).
fof(f7158,plain,
( $false
| ~ spl32_36
| spl32_37
| ~ spl32_182 ),
inference(forward_subsumption_resolution,[],[f7157,f1851]) ).
fof(f7159,plain,
( ~ spl32_36
| spl32_37
| ~ spl32_182 ),
inference(avatar_contradiction_clause,[],[f7158]) ).
fof(f7331,plain,
( ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| v3_struct_0(sK0)
| ~ l1_orders_2(sK0)
| v3_struct_0(sK0)
| m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| spl32_207 ),
inference(resolution,[],[f5984,f933]) ).
fof(f7332,plain,
( ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| v3_struct_0(sK0)
| m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| spl32_207 ),
inference(duplicate_literal_removal,[],[f7331]) ).
fof(f7333,plain,
( ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| v3_struct_0(sK0)
| m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| spl32_207 ),
inference(forward_subsumption_resolution,[],[f7332,f413]) ).
fof(f7334,plain,
( ~ l1_orders_2(sK0)
| v3_struct_0(sK0)
| m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| spl32_207 ),
inference(forward_subsumption_resolution,[],[f7333,f414]) ).
fof(f7335,plain,
( v3_struct_0(sK0)
| m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| spl32_207 ),
inference(forward_subsumption_resolution,[],[f7334,f417]) ).
fof(f7336,plain,
( m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| spl32_14
| spl32_207 ),
inference(forward_subsumption_resolution,[],[f7335,f1401]) ).
fof(f7337,plain,
( $false
| spl32_14
| spl32_37
| spl32_207 ),
inference(forward_subsumption_resolution,[],[f7336,f1851]) ).
fof(f7338,plain,
( spl32_14
| spl32_37
| spl32_207 ),
inference(avatar_contradiction_clause,[],[f7337]) ).
fof(f7422,plain,
( v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| spl32_212 ),
inference(resolution,[],[f6022,f1124]) ).
fof(f7423,plain,
( ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| spl32_212 ),
inference(forward_subsumption_resolution,[],[f7422,f856]) ).
fof(f7424,plain,
( ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| spl32_212 ),
inference(forward_subsumption_resolution,[],[f7423,f419]) ).
fof(f7425,plain,
( ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| spl32_212 ),
inference(forward_subsumption_resolution,[],[f7424,f420]) ).
fof(f7426,plain,
( ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| spl32_212 ),
inference(forward_subsumption_resolution,[],[f7425,f421]) ).
fof(f7427,plain,
( ~ v2_orders_2(sK0)
| ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| spl32_212 ),
inference(forward_subsumption_resolution,[],[f7426,f422]) ).
fof(f7428,plain,
( ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| spl32_212 ),
inference(forward_subsumption_resolution,[],[f7427,f423]) ).
fof(f7429,plain,
( ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| spl32_212 ),
inference(forward_subsumption_resolution,[],[f7428,f411]) ).
fof(f7430,plain,
( ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| spl32_212 ),
inference(forward_subsumption_resolution,[],[f7429,f412]) ).
fof(f7431,plain,
( ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| spl32_212 ),
inference(forward_subsumption_resolution,[],[f7430,f413]) ).
fof(f7432,plain,
( ~ l1_orders_2(sK0)
| spl32_212 ),
inference(forward_subsumption_resolution,[],[f7431,f414]) ).
fof(f7433,plain,
( $false
| spl32_212 ),
inference(forward_subsumption_resolution,[],[f7432,f417]) ).
fof(f7434,plain,
spl32_212,
inference(avatar_contradiction_clause,[],[f7433]) ).
fof(f8024,plain,
( ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| v3_struct_0(sK0)
| ~ l1_orders_2(sK0)
| v3_struct_0(sK0)
| m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| spl32_208 ),
inference(resolution,[],[f5989,f934]) ).
fof(f8026,plain,
( ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| v3_struct_0(sK0)
| m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| spl32_208 ),
inference(duplicate_literal_removal,[],[f8024]) ).
fof(f8028,plain,
( ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| v3_struct_0(sK0)
| m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| spl32_208 ),
inference(forward_subsumption_resolution,[],[f8026,f413]) ).
fof(f8029,plain,
( ~ l1_orders_2(sK0)
| v3_struct_0(sK0)
| m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| spl32_208 ),
inference(forward_subsumption_resolution,[],[f8028,f414]) ).
fof(f8030,plain,
( v3_struct_0(sK0)
| m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| spl32_208 ),
inference(forward_subsumption_resolution,[],[f8029,f417]) ).
fof(f8031,plain,
( m1_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| spl32_14
| spl32_208 ),
inference(forward_subsumption_resolution,[],[f8030,f1401]) ).
fof(f8032,plain,
( $false
| spl32_14
| spl32_37
| spl32_208 ),
inference(forward_subsumption_resolution,[],[f8031,f1851]) ).
fof(f8033,plain,
( spl32_14
| spl32_37
| spl32_208 ),
inference(avatar_contradiction_clause,[],[f8032]) ).
fof(f8037,plain,
( v3_lattice3(sK0)
| ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v4_waybel_0(k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ spl32_220 ),
inference(resolution,[],[f6063,f1128]) ).
fof(f8040,plain,
( ~ v2_lattice3(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v4_waybel_0(k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ spl32_220 ),
inference(forward_subsumption_resolution,[],[f8037,f856]) ).
fof(f8042,plain,
( ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v4_waybel_0(k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ spl32_220 ),
inference(forward_subsumption_resolution,[],[f8040,f419]) ).
fof(f8044,plain,
( ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v4_waybel_0(k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ spl32_220 ),
inference(forward_subsumption_resolution,[],[f8042,f420]) ).
fof(f8046,plain,
( ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v4_waybel_0(k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ spl32_220 ),
inference(forward_subsumption_resolution,[],[f8044,f421]) ).
fof(f8048,plain,
( ~ v2_orders_2(sK0)
| ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v4_waybel_0(k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ spl32_220 ),
inference(forward_subsumption_resolution,[],[f8046,f422]) ).
fof(f8050,plain,
( ~ m2_relset_1(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v4_waybel_0(k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ spl32_220 ),
inference(forward_subsumption_resolution,[],[f8048,f423]) ).
fof(f8056,plain,
( ~ v7_waybel_1(sK1,sK0)
| ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v4_waybel_0(k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ spl32_220 ),
inference(forward_subsumption_resolution,[],[f8050,f411]) ).
fof(f8057,plain,
( ~ v1_funct_2(sK1,u1_struct_0(sK0),u1_struct_0(sK0))
| ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v4_waybel_0(k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ spl32_220 ),
inference(forward_subsumption_resolution,[],[f8056,f412]) ).
fof(f8058,plain,
( ~ v1_funct_1(sK1)
| ~ l1_orders_2(sK0)
| ~ v4_waybel_0(k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ spl32_220 ),
inference(forward_subsumption_resolution,[],[f8057,f413]) ).
fof(f8059,plain,
( ~ l1_orders_2(sK0)
| ~ v4_waybel_0(k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ spl32_220 ),
inference(forward_subsumption_resolution,[],[f8058,f414]) ).
fof(f8060,plain,
( ~ v4_waybel_0(k2_yellow_2(sK0,sK0,sK1),sK0)
| ~ spl32_220 ),
inference(forward_subsumption_resolution,[],[f8059,f417]) ).
fof(f8061,plain,
( $false
| ~ spl32_220 ),
inference(forward_subsumption_resolution,[],[f8060,f415]) ).
fof(f8062,plain,
~ spl32_220,
inference(avatar_contradiction_clause,[],[f8061]) ).
cnf(s38,plain,
( spl32_14
| spl32_36
| spl32_37 ),
inference(sat_conversion,[],[f1853]) ).
cnf(s40,plain,
~ spl32_14,
inference(sat_conversion,[],[f1897]) ).
cnf(s42,plain,
~ spl32_37,
inference(sat_conversion,[],[f1970]) ).
cnf(s191,plain,
( spl32_14
| spl32_37
| spl32_63 ),
inference(sat_conversion,[],[f5677]) ).
cnf(s227,plain,
( spl32_14
| ~ spl32_36
| spl32_37
| ~ spl32_63
| spl32_182
| ~ spl32_207
| ~ spl32_208
| ~ spl32_212
| spl32_220 ),
inference(sat_conversion,[],[f6064]) ).
cnf(s272,plain,
( ~ spl32_36
| spl32_37
| ~ spl32_182 ),
inference(sat_conversion,[],[f7159]) ).
cnf(s279,plain,
( spl32_14
| spl32_37
| spl32_207 ),
inference(sat_conversion,[],[f7338]) ).
cnf(s283,plain,
spl32_212,
inference(sat_conversion,[],[f7434]) ).
cnf(s308,plain,
( spl32_14
| spl32_37
| spl32_208 ),
inference(sat_conversion,[],[f8033]) ).
cnf(s310,plain,
~ spl32_220,
inference(sat_conversion,[],[f8062]) ).
cnf(s311,plain,
( spl32_14
| ~ spl32_36
| spl32_37
| ~ spl32_63
| spl32_182
| ~ spl32_207
| ~ spl32_208 ),
inference(rat,[],[s227,s310,s283]) ).
cnf(s327,plain,
spl32_208,
inference(rat,[],[s308,s42,s40]) ).
cnf(s328,plain,
spl32_207,
inference(rat,[],[s279,s42,s40]) ).
cnf(s331,plain,
spl32_63,
inference(rat,[],[s191,s42,s40]) ).
cnf(s359,plain,
spl32_36,
inference(rat,[],[s38,s42,s40]) ).
cnf(s360,plain,
~ spl32_182,
inference(rat,[],[s272,s42,s359]) ).
cnf(s361,plain,
$false,
inference(rat,[],[s311,s327,s328,s331,s40,s42,s360,s359]) ).
fof(f8063,plain,
$false,
inference(avatar_sat_refutation,[],[s361]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT369+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.37 % Computer : n011.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sun Sep 27 15:06:00 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.41 Running first-order model finding
% 0.11/0.41 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.32/0.70 % (2523436)Will run a generic schedule for satisfiability detection.
% 1.32/0.70 % (2523445)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4220220584:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 1.32/0.70 % (2523442)% WARNING: option uhcvi not known.
% 1.32/0.70 % (2523441)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1874643830_2999 on theBenchmark for (2999ds/0Mi)
% 1.32/0.70 % (2523442)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2958144786:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 1.32/0.70 % (2523443)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1487081725:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 1.32/0.70 % (2523444)dis+10_1_sil=32000:sp=arity:random_seed=2417987332:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 1.32/0.70 % (2523447)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2106862315:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 1.32/0.70 % (2523446)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2248802487:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 1.32/0.70 % (2523445)Instruction limit reached!
% 1.32/0.70 % (2523445)------------------------------
% 1.32/0.70 % (2523445)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.32/0.70 % (2523445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.32/0.70 % (2523445)CaDiCaL version: 2.1.3
% 1.32/0.70 % (2523445)Termination reason: Instruction limit
% 1.32/0.70 % (2523445)Termination phase: Saturation
% 1.32/0.70 % (2523445)Time elapsed: 0.037 s
% 1.32/0.70 % (2523445)Peak memory usage: 13 MB
% 1.32/0.70 % (2523445)Instructions burned: 118 (million)
% 1.32/0.70 % (2523455)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3563855924:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 1.32/0.70 % TRYING [1]
% 1.32/0.70 % TRYING [2]
% 1.32/0.70 % TRYING [1]
% 1.32/0.70 % TRYING [2]
% 1.32/0.70 % TRYING [3]
% 1.32/0.70 % TRYING [3]
% 1.32/0.70 % (2523444)Instruction limit reached!
% 1.32/0.70 % (2523444)------------------------------
% 1.32/0.70 % (2523444)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.32/0.70 % (2523444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.32/0.70 % (2523444)CaDiCaL version: 2.1.3
% 1.32/0.70 % (2523444)Termination reason: Instruction limit
% 1.32/0.70 % (2523444)Termination phase: Saturation
% 1.32/0.70 % (2523444)Time elapsed: 0.063 s
% 1.32/0.70 % (2523444)Peak memory usage: 13 MB
% 1.32/0.70 % (2523444)Instructions burned: 103 (million)
% 1.32/0.70 % (2523446)Instruction limit reached!
% 1.32/0.70 % (2523446)------------------------------
% 1.32/0.70 % (2523446)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.32/0.70 % (2523446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.32/0.70 % (2523446)CaDiCaL version: 2.1.3
% 1.32/0.70 % (2523446)Termination reason: Instruction limit
% 1.32/0.70 % (2523446)Termination phase: Saturation
% 1.32/0.70 % (2523446)Time elapsed: 0.073 s
% 1.32/0.70 % (2523446)Peak memory usage: 14 MB
% 1.32/0.70 % (2523446)Instructions burned: 131 (million)
% 1.32/0.70 % (2523457)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2534275484:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 1.32/0.70 % (2523458)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=3196425518:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 2.00/0.70 % TRYING [4]
% 2.00/0.70 % (2523447)Instruction limit reached!
% 2.00/0.70 % (2523447)------------------------------
% 2.00/0.70 % (2523447)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.00/0.70 % (2523447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.00/0.70 % (2523447)CaDiCaL version: 2.1.3
% 2.00/0.70 % (2523447)Termination reason: Instruction limit
% 2.00/0.70 % (2523447)Termination phase: Saturation
% 2.00/0.70 % (2523447)Time elapsed: 0.101 s
% 2.00/0.70 % (2523447)Peak memory usage: 15 MB
% 2.00/0.70 % (2523447)Instructions burned: 159 (million)
% 2.00/0.70 % (2523461)ott-21_1_sil=16000:fs=off:random_seed=580306247:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 2.00/0.70 % TRYING [4]
% 2.00/0.70 % (2523457)Instruction limit reached!
% 2.00/0.70 % (2523457)------------------------------
% 2.00/0.70 % (2523457)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.00/0.70 % (2523457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.00/0.70 % (2523457)CaDiCaL version: 2.1.3
% 2.00/0.70 % (2523457)Termination reason: Instruction limit
% 2.00/0.70 % (2523457)Termination phase: Saturation
% 2.00/0.70 % (2523457)Time elapsed: 0.075 s
% 2.00/0.70 % (2523457)Peak memory usage: 14 MB
% 2.00/0.70 % (2523457)Instructions burned: 133 (million)
% 2.00/0.70 % (2523463)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=591274883:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 2.00/0.70 % (2523455)Instruction limit reached!
% 2.00/0.70 % (2523455)------------------------------
% 2.00/0.70 % (2523455)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.00/0.70 % (2523455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.00/0.70 % (2523455)CaDiCaL version: 2.1.3
% 2.00/0.70 % (2523455)Termination reason: Instruction limit
% 2.00/0.70 % (2523455)Termination phase: Finite model building SAT solving
% 2.00/0.70 % (2523455)Time elapsed: 0.167 s
% 2.00/0.70 % (2523455)Peak memory usage: 36 MB
% 2.00/0.70 % (2523455)Instructions burned: 715 (million)
% 2.00/0.70 % (2523461)Instruction limit reached!
% 2.00/0.70 % (2523461)------------------------------
% 2.00/0.70 % (2523461)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.00/0.70 % (2523461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.00/0.70 % (2523461)CaDiCaL version: 2.1.3
% 2.00/0.70 % (2523461)Termination reason: Instruction limit
% 2.00/0.70 % (2523461)Termination phase: Saturation
% 2.00/0.70 % (2523461)Time elapsed: 0.098 s
% 2.00/0.70 % (2523461)Peak memory usage: 13 MB
% 2.00/0.70 % (2523461)Instructions burned: 180 (million)
% 2.00/0.70 % (2523465)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2139634749:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 2.00/0.70 % (2523442) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2523436-2523442"...
% 2.00/0.70 % (2523442)...printing done.
% 2.00/0.70 % (2523442)Refutation found. Thanks to Tanya!
% 2.00/0.70 % SZS status Theorem for theBenchmark
% 2.00/0.70 % SZS output start Proof for theBenchmark
% See solution above
% 2.00/0.70 % (2523442)------------------------------
% 2.00/0.70 % (2523442)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.00/0.70 % (2523442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.00/0.70 % (2523442)CaDiCaL version: 2.1.3
% 2.00/0.70 % (2523442)Termination reason: Refutation
% 2.00/0.70 % (2523442)Time elapsed: 0.235 s
% 2.00/0.70 % (2523442)Peak memory usage: 17 MB
% 2.00/0.70 % (2523442)Instructions burned: 379 (million)
% 2.00/0.70 % (2523436)Success in time 0.281 s
% 2.00/0.70 % Vampire exiting
%------------------------------------------------------------------------------