%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT360+3 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n001.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:47:19 AM UTC 2026
% Result : Theorem 59.99s 18.56s
% Output : Refutation 118.73s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 78
% Syntax : Number of formulae : 502 ( 70 unt; 60 def)
% Number of atoms : 2357 ( 66 equ)
% Maximal formula atoms : 15 ( 4 avg)
% Number of connectives : 3271 (1416 ~;1585 |; 178 &)
% ( 68 <=>; 23 =>; 0 <=; 1 <~>)
% Maximal formula depth : 16 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 86 ( 84 usr; 56 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 5 con; 0-2 aty)
% Number of variables : 234 ( 0 sgn 231 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X0,X1] :
( ! [X2] :
( r2_hidden(X2,X0)
<=> r2_hidden(X2,X1) )
=> X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2_tarski) ).
fof(f480,axiom,
! [X0,X1] :
( ( ~ v1_xboole_0(X0)
=> ( m1_subset_1(X1,X0)
<=> r2_hidden(X1,X0) ) )
& ( v1_xboole_0(X0)
=> ( m1_subset_1(X1,X0)
<=> v1_xboole_0(X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d2_subset_1) ).
fof(f588,axiom,
! [X0] :
( ~ v2_setfam_1(X0)
=> ~ v1_xboole_0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc2_setfam_1) ).
fof(f675,axiom,
! [X0,X1] :
( r2_hidden(X0,X1)
=> m1_subset_1(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t1_subset) ).
fof(f6424,axiom,
! [X0] :
( l1_struct_0(X0)
=> ( v3_struct_0(X0)
<=> v1_xboole_0(u1_struct_0(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_struct_0) ).
fof(f13898,axiom,
! [X0] :
( l1_altcat_1(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l1_altcat_1) ).
fof(f13900,axiom,
! [X0] :
( l2_altcat_1(X0)
=> l1_altcat_1(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l2_altcat_1) ).
fof(f18848,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_altcat_1(X0)
& v11_altcat_1(X0)
& v12_altcat_1(X0)
& v2_yellow21(X0)
& l2_altcat_1(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> k3_yellow21(X0,X1) = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d6_yellow21) ).
fof(f18885,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v2_altcat_1(X0)
& v11_altcat_1(X0)
& v12_altcat_1(X0)
& v2_yellow21(X0)
& l2_altcat_1(X0)
& m1_subset_1(X1,u1_struct_0(X0)) )
=> ( v2_orders_2(k3_yellow21(X0,X1))
& v3_orders_2(k3_yellow21(X0,X1))
& v4_orders_2(k3_yellow21(X0,X1))
& v1_lattice3(k3_yellow21(X0,X1))
& v2_lattice3(k3_yellow21(X0,X1))
& l1_orders_2(k3_yellow21(X0,X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k3_yellow21) ).
fof(f18886,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v2_altcat_1(X0)
& v11_altcat_1(X0)
& v12_altcat_1(X0)
& v2_yellow21(X0)
& l2_altcat_1(X0)
& m1_subset_1(X1,u1_struct_0(X0)) )
=> k3_yellow21(X0,X1) = k1_yellow21(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k3_yellow21) ).
fof(f18887,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v2_altcat_1(X0)
& v11_altcat_1(X0)
& v12_altcat_1(X0)
& v3_yellow21(X0)
& l2_altcat_1(X0)
& m1_subset_1(X1,u1_struct_0(X0)) )
=> ( v2_orders_2(k4_yellow21(X0,X1))
& v3_orders_2(k4_yellow21(X0,X1))
& v4_orders_2(k4_yellow21(X0,X1))
& v1_lattice3(k4_yellow21(X0,X1))
& v2_lattice3(k4_yellow21(X0,X1))
& v3_lattice3(k4_yellow21(X0,X1))
& l1_orders_2(k4_yellow21(X0,X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k4_yellow21) ).
fof(f18888,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v2_altcat_1(X0)
& v11_altcat_1(X0)
& v12_altcat_1(X0)
& v3_yellow21(X0)
& l2_altcat_1(X0)
& m1_subset_1(X1,u1_struct_0(X0)) )
=> k4_yellow21(X0,X1) = k1_yellow21(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k4_yellow21) ).
fof(f18896,axiom,
! [X0] :
( ~ v1_xboole_0(X0)
=> ( ~ v3_struct_0(k4_waybel34(X0))
& v2_altcat_1(k4_waybel34(X0))
& v6_altcat_1(k4_waybel34(X0))
& v11_altcat_1(k4_waybel34(X0))
& v12_altcat_1(k4_waybel34(X0))
& v2_yellow21(k4_waybel34(X0))
& l2_altcat_1(k4_waybel34(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k4_waybel34) ).
fof(f18897,axiom,
! [X0] :
( ~ v1_xboole_0(X0)
=> ( ~ v3_struct_0(k5_waybel34(X0))
& v2_altcat_1(k5_waybel34(X0))
& v6_altcat_1(k5_waybel34(X0))
& v11_altcat_1(k5_waybel34(X0))
& v12_altcat_1(k5_waybel34(X0))
& v2_yellow21(k5_waybel34(X0))
& l2_altcat_1(k5_waybel34(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k5_waybel34) ).
fof(f18930,axiom,
! [X0] :
( ~ v2_setfam_1(X0)
=> ( ~ v3_struct_0(k4_waybel34(X0))
& v2_altcat_1(k4_waybel34(X0))
& v6_altcat_1(k4_waybel34(X0))
& v9_altcat_1(k4_waybel34(X0))
& v11_altcat_1(k4_waybel34(X0))
& v12_altcat_1(k4_waybel34(X0))
& v1_altcat_2(k4_waybel34(X0))
& v2_yellow18(k4_waybel34(X0))
& v3_yellow18(k4_waybel34(X0))
& v4_yellow18(k4_waybel34(X0))
& v1_yellow21(k4_waybel34(X0))
& v2_yellow21(k4_waybel34(X0))
& v3_yellow21(k4_waybel34(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc5_waybel34) ).
fof(f18932,axiom,
! [X0] :
( ~ v2_setfam_1(X0)
=> ! [X1] :
( ( v2_orders_2(X1)
& v3_orders_2(X1)
& v4_orders_2(X1)
& v1_lattice3(X1)
& v2_lattice3(X1)
& l1_orders_2(X1) )
=> ( m1_subset_1(X1,u1_struct_0(k4_waybel34(X0)))
<=> ( v1_orders_2(X1)
& v3_lattice3(X1)
& r2_hidden(u1_struct_0(X1),X0) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t13_waybel34) ).
fof(f18934,axiom,
! [X0] :
( ~ v2_setfam_1(X0)
=> ! [X1] :
( ( v2_orders_2(X1)
& v3_orders_2(X1)
& v4_orders_2(X1)
& v1_lattice3(X1)
& v2_lattice3(X1)
& l1_orders_2(X1) )
=> ( m1_subset_1(X1,u1_struct_0(k5_waybel34(X0)))
<=> ( v1_orders_2(X1)
& v3_lattice3(X1)
& r2_hidden(u1_struct_0(X1),X0) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t15_waybel34) ).
fof(f18936,conjecture,
! [X0] :
( ~ v2_setfam_1(X0)
=> u1_struct_0(k4_waybel34(X0)) = u1_struct_0(k5_waybel34(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t17_waybel34) ).
fof(f18937,negated_conjecture,
~ ! [X0] :
( ~ v2_setfam_1(X0)
=> u1_struct_0(k4_waybel34(X0)) = u1_struct_0(k5_waybel34(X0)) ),
inference(negated_conjecture,[status(cth)],[f18936]) ).
fof(f19014,plain,
? [X0] :
( u1_struct_0(k4_waybel34(X0)) != u1_struct_0(k5_waybel34(X0))
& ~ v2_setfam_1(X0) ),
inference(ennf_transformation,[],[f18937]) ).
fof(f19021,plain,
! [X0] :
( ~ v1_xboole_0(X0)
| v2_setfam_1(X0) ),
inference(ennf_transformation,[],[f588]) ).
fof(f19023,plain,
! [X0] :
( ! [X1] :
( ( m1_subset_1(X1,u1_struct_0(k4_waybel34(X0)))
<=> ( v1_orders_2(X1)
& v3_lattice3(X1)
& r2_hidden(u1_struct_0(X1),X0) ) )
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ l1_orders_2(X1) )
| v2_setfam_1(X0) ),
inference(ennf_transformation,[],[f18932]) ).
fof(f19024,plain,
! [X0] :
( ! [X1] :
( ( m1_subset_1(X1,u1_struct_0(k4_waybel34(X0)))
<=> ( v1_orders_2(X1)
& v3_lattice3(X1)
& r2_hidden(u1_struct_0(X1),X0) ) )
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ l1_orders_2(X1) )
| v2_setfam_1(X0) ),
inference(flattening,[],[f19023]) ).
fof(f19025,plain,
! [X0] :
( ( ~ v3_struct_0(k4_waybel34(X0))
& v2_altcat_1(k4_waybel34(X0))
& v6_altcat_1(k4_waybel34(X0))
& v9_altcat_1(k4_waybel34(X0))
& v11_altcat_1(k4_waybel34(X0))
& v12_altcat_1(k4_waybel34(X0))
& v1_altcat_2(k4_waybel34(X0))
& v2_yellow18(k4_waybel34(X0))
& v3_yellow18(k4_waybel34(X0))
& v4_yellow18(k4_waybel34(X0))
& v1_yellow21(k4_waybel34(X0))
& v2_yellow21(k4_waybel34(X0))
& v3_yellow21(k4_waybel34(X0)) )
| v2_setfam_1(X0) ),
inference(ennf_transformation,[],[f18930]) ).
fof(f19030,plain,
! [X0] :
( ( ~ v3_struct_0(k4_waybel34(X0))
& v2_altcat_1(k4_waybel34(X0))
& v6_altcat_1(k4_waybel34(X0))
& v11_altcat_1(k4_waybel34(X0))
& v12_altcat_1(k4_waybel34(X0))
& v2_yellow21(k4_waybel34(X0))
& l2_altcat_1(k4_waybel34(X0)) )
| v1_xboole_0(X0) ),
inference(ennf_transformation,[],[f18896]) ).
fof(f19032,plain,
! [X0] :
( ! [X1] :
( ( m1_subset_1(X1,u1_struct_0(k5_waybel34(X0)))
<=> ( v1_orders_2(X1)
& v3_lattice3(X1)
& r2_hidden(u1_struct_0(X1),X0) ) )
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ l1_orders_2(X1) )
| v2_setfam_1(X0) ),
inference(ennf_transformation,[],[f18934]) ).
fof(f19033,plain,
! [X0] :
( ! [X1] :
( ( m1_subset_1(X1,u1_struct_0(k5_waybel34(X0)))
<=> ( v1_orders_2(X1)
& v3_lattice3(X1)
& r2_hidden(u1_struct_0(X1),X0) ) )
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ l1_orders_2(X1) )
| v2_setfam_1(X0) ),
inference(flattening,[],[f19032]) ).
fof(f19039,plain,
! [X0] :
( ( ~ v3_struct_0(k5_waybel34(X0))
& v2_altcat_1(k5_waybel34(X0))
& v6_altcat_1(k5_waybel34(X0))
& v11_altcat_1(k5_waybel34(X0))
& v12_altcat_1(k5_waybel34(X0))
& v2_yellow21(k5_waybel34(X0))
& l2_altcat_1(k5_waybel34(X0)) )
| v1_xboole_0(X0) ),
inference(ennf_transformation,[],[f18897]) ).
fof(f19045,plain,
! [X0,X1] :
( ( ( m1_subset_1(X1,X0)
<=> r2_hidden(X1,X0) )
| v1_xboole_0(X0) )
& ( ( m1_subset_1(X1,X0)
<=> v1_xboole_0(X1) )
| ~ v1_xboole_0(X0) ) ),
inference(ennf_transformation,[],[f480]) ).
fof(f19166,plain,
! [X0,X1] :
( m1_subset_1(X0,X1)
| ~ r2_hidden(X0,X1) ),
inference(ennf_transformation,[],[f675]) ).
fof(f19168,plain,
! [X0,X1] :
( X0 = X1
| ? [X2] :
( r2_hidden(X2,X0)
<~> r2_hidden(X2,X1) ) ),
inference(ennf_transformation,[],[f3]) ).
fof(f19210,plain,
! [X0,X1] :
( k4_yellow21(X0,X1) = k1_yellow21(X1)
| v3_struct_0(X0)
| ~ v2_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ v3_yellow21(X0)
| ~ l2_altcat_1(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f18888]) ).
fof(f19211,plain,
! [X0,X1] :
( k4_yellow21(X0,X1) = k1_yellow21(X1)
| v3_struct_0(X0)
| ~ v2_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ v3_yellow21(X0)
| ~ l2_altcat_1(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(flattening,[],[f19210]) ).
fof(f19212,plain,
! [X0,X1] :
( ( v2_orders_2(k4_yellow21(X0,X1))
& v3_orders_2(k4_yellow21(X0,X1))
& v4_orders_2(k4_yellow21(X0,X1))
& v1_lattice3(k4_yellow21(X0,X1))
& v2_lattice3(k4_yellow21(X0,X1))
& v3_lattice3(k4_yellow21(X0,X1))
& l1_orders_2(k4_yellow21(X0,X1)) )
| v3_struct_0(X0)
| ~ v2_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ v3_yellow21(X0)
| ~ l2_altcat_1(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f18887]) ).
fof(f19213,plain,
! [X0,X1] :
( ( v2_orders_2(k4_yellow21(X0,X1))
& v3_orders_2(k4_yellow21(X0,X1))
& v4_orders_2(k4_yellow21(X0,X1))
& v1_lattice3(k4_yellow21(X0,X1))
& v2_lattice3(k4_yellow21(X0,X1))
& v3_lattice3(k4_yellow21(X0,X1))
& l1_orders_2(k4_yellow21(X0,X1)) )
| v3_struct_0(X0)
| ~ v2_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ v3_yellow21(X0)
| ~ l2_altcat_1(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(flattening,[],[f19212]) ).
fof(f19340,plain,
! [X0,X1] :
( ( v2_orders_2(k3_yellow21(X0,X1))
& v3_orders_2(k3_yellow21(X0,X1))
& v4_orders_2(k3_yellow21(X0,X1))
& v1_lattice3(k3_yellow21(X0,X1))
& v2_lattice3(k3_yellow21(X0,X1))
& l1_orders_2(k3_yellow21(X0,X1)) )
| v3_struct_0(X0)
| ~ v2_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ v2_yellow21(X0)
| ~ l2_altcat_1(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f18885]) ).
fof(f19341,plain,
! [X0,X1] :
( ( v2_orders_2(k3_yellow21(X0,X1))
& v3_orders_2(k3_yellow21(X0,X1))
& v4_orders_2(k3_yellow21(X0,X1))
& v1_lattice3(k3_yellow21(X0,X1))
& v2_lattice3(k3_yellow21(X0,X1))
& l1_orders_2(k3_yellow21(X0,X1)) )
| v3_struct_0(X0)
| ~ v2_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ v2_yellow21(X0)
| ~ l2_altcat_1(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(flattening,[],[f19340]) ).
fof(f19342,plain,
! [X0] :
( ! [X1] :
( k3_yellow21(X0,X1) = X1
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v2_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ v2_yellow21(X0)
| ~ l2_altcat_1(X0) ),
inference(ennf_transformation,[],[f18848]) ).
fof(f19343,plain,
! [X0] :
( ! [X1] :
( k3_yellow21(X0,X1) = X1
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v2_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ v2_yellow21(X0)
| ~ l2_altcat_1(X0) ),
inference(flattening,[],[f19342]) ).
fof(f19354,plain,
! [X0] :
( ( v3_struct_0(X0)
<=> v1_xboole_0(u1_struct_0(X0)) )
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f6424]) ).
fof(f20236,plain,
! [X0,X1] :
( k3_yellow21(X0,X1) = k1_yellow21(X1)
| v3_struct_0(X0)
| ~ v2_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ v2_yellow21(X0)
| ~ l2_altcat_1(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f18886]) ).
fof(f20237,plain,
! [X0,X1] :
( k3_yellow21(X0,X1) = k1_yellow21(X1)
| v3_struct_0(X0)
| ~ v2_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ v2_yellow21(X0)
| ~ l2_altcat_1(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(flattening,[],[f20236]) ).
fof(f20516,plain,
! [X0] :
( l1_altcat_1(X0)
| ~ l2_altcat_1(X0) ),
inference(ennf_transformation,[],[f13900]) ).
fof(f20517,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_altcat_1(X0) ),
inference(ennf_transformation,[],[f13898]) ).
fof(f20720,definition,
! [X0] :
( ( ~ v3_struct_0(k4_waybel34(X0))
& v2_altcat_1(k4_waybel34(X0))
& v6_altcat_1(k4_waybel34(X0))
& v9_altcat_1(k4_waybel34(X0))
& v11_altcat_1(k4_waybel34(X0))
& v12_altcat_1(k4_waybel34(X0))
& v1_altcat_2(k4_waybel34(X0))
& v2_yellow18(k4_waybel34(X0))
& v3_yellow18(k4_waybel34(X0))
& v4_yellow18(k4_waybel34(X0))
& v1_yellow21(k4_waybel34(X0))
& v2_yellow21(k4_waybel34(X0))
& v3_yellow21(k4_waybel34(X0)) )
| ~ sP0(X0) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f20721,plain,
! [X0] :
( sP0(X0)
| v2_setfam_1(X0) ),
inference(definition_folding,[],[f19025,f20720]) ).
fof(f20835,plain,
( u1_struct_0(k4_waybel34(sK71)) != u1_struct_0(k5_waybel34(sK71))
& ~ v2_setfam_1(sK71) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK71]),skolemize(X0,sK71)],[f19014]) ).
fof(f20845,plain,
! [X0] :
( ! [X1] :
( ( ( m1_subset_1(X1,u1_struct_0(k4_waybel34(X0)))
| ~ v1_orders_2(X1)
| ~ v3_lattice3(X1)
| ~ r2_hidden(u1_struct_0(X1),X0) )
& ( ( v1_orders_2(X1)
& v3_lattice3(X1)
& r2_hidden(u1_struct_0(X1),X0) )
| ~ m1_subset_1(X1,u1_struct_0(k4_waybel34(X0))) ) )
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ l1_orders_2(X1) )
| v2_setfam_1(X0) ),
inference(nnf_transformation,[],[f19024]) ).
fof(f20846,plain,
! [X0] :
( ! [X1] :
( ( ( m1_subset_1(X1,u1_struct_0(k4_waybel34(X0)))
| ~ v1_orders_2(X1)
| ~ v3_lattice3(X1)
| ~ r2_hidden(u1_struct_0(X1),X0) )
& ( ( v1_orders_2(X1)
& v3_lattice3(X1)
& r2_hidden(u1_struct_0(X1),X0) )
| ~ m1_subset_1(X1,u1_struct_0(k4_waybel34(X0))) ) )
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ l1_orders_2(X1) )
| v2_setfam_1(X0) ),
inference(flattening,[],[f20845]) ).
fof(f20847,plain,
! [X0] :
( ( ~ v3_struct_0(k4_waybel34(X0))
& v2_altcat_1(k4_waybel34(X0))
& v6_altcat_1(k4_waybel34(X0))
& v9_altcat_1(k4_waybel34(X0))
& v11_altcat_1(k4_waybel34(X0))
& v12_altcat_1(k4_waybel34(X0))
& v1_altcat_2(k4_waybel34(X0))
& v2_yellow18(k4_waybel34(X0))
& v3_yellow18(k4_waybel34(X0))
& v4_yellow18(k4_waybel34(X0))
& v1_yellow21(k4_waybel34(X0))
& v2_yellow21(k4_waybel34(X0))
& v3_yellow21(k4_waybel34(X0)) )
| ~ sP0(X0) ),
inference(nnf_transformation,[],[f20720]) ).
fof(f20866,plain,
! [X0] :
( ! [X1] :
( ( ( m1_subset_1(X1,u1_struct_0(k5_waybel34(X0)))
| ~ v1_orders_2(X1)
| ~ v3_lattice3(X1)
| ~ r2_hidden(u1_struct_0(X1),X0) )
& ( ( v1_orders_2(X1)
& v3_lattice3(X1)
& r2_hidden(u1_struct_0(X1),X0) )
| ~ m1_subset_1(X1,u1_struct_0(k5_waybel34(X0))) ) )
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ l1_orders_2(X1) )
| v2_setfam_1(X0) ),
inference(nnf_transformation,[],[f19033]) ).
fof(f20867,plain,
! [X0] :
( ! [X1] :
( ( ( m1_subset_1(X1,u1_struct_0(k5_waybel34(X0)))
| ~ v1_orders_2(X1)
| ~ v3_lattice3(X1)
| ~ r2_hidden(u1_struct_0(X1),X0) )
& ( ( v1_orders_2(X1)
& v3_lattice3(X1)
& r2_hidden(u1_struct_0(X1),X0) )
| ~ m1_subset_1(X1,u1_struct_0(k5_waybel34(X0))) ) )
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ l1_orders_2(X1) )
| v2_setfam_1(X0) ),
inference(flattening,[],[f20866]) ).
fof(f20888,plain,
! [X0,X1] :
( ( ( ( m1_subset_1(X1,X0)
| ~ r2_hidden(X1,X0) )
& ( r2_hidden(X1,X0)
| ~ m1_subset_1(X1,X0) ) )
| v1_xboole_0(X0) )
& ( ( ( m1_subset_1(X1,X0)
| ~ v1_xboole_0(X1) )
& ( v1_xboole_0(X1)
| ~ m1_subset_1(X1,X0) ) )
| ~ v1_xboole_0(X0) ) ),
inference(nnf_transformation,[],[f19045]) ).
fof(f20943,plain,
! [X0,X1] :
( X0 = X1
| ? [X2] :
( ( ~ r2_hidden(X2,X1)
| ~ r2_hidden(X2,X0) )
& ( r2_hidden(X2,X1)
| r2_hidden(X2,X0) ) ) ),
inference(nnf_transformation,[],[f19168]) ).
fof(f20944,plain,
! [X0,X1] :
( X0 = X1
| ( ( ~ r2_hidden(sK130(X0,X1),X1)
| ~ r2_hidden(sK130(X0,X1),X0) )
& ( r2_hidden(sK130(X0,X1),X1)
| r2_hidden(sK130(X0,X1),X0) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK130]),skolemize(X2,sK130(X0,X1))],[f20943]) ).
fof(f21033,plain,
! [X0] :
( ( ( v3_struct_0(X0)
| ~ v1_xboole_0(u1_struct_0(X0)) )
& ( v1_xboole_0(u1_struct_0(X0))
| ~ v3_struct_0(X0) ) )
| ~ l1_struct_0(X0) ),
inference(nnf_transformation,[],[f19354]) ).
fof(f21600,plain,
~ v2_setfam_1(sK71),
inference(cnf_transformation,[],[f20835]) ).
fof(f21601,plain,
u1_struct_0(k4_waybel34(sK71)) != u1_struct_0(k5_waybel34(sK71)),
inference(cnf_transformation,[],[f20835]) ).
fof(f21615,plain,
! [X0] :
( v2_setfam_1(X0)
| ~ v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f19021]) ).
fof(f21622,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u1_struct_0(k4_waybel34(X0)))
| r2_hidden(u1_struct_0(X1),X0)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ l1_orders_2(X1)
| v2_setfam_1(X0) ),
inference(cnf_transformation,[],[f20846]) ).
fof(f21624,plain,
! [X0,X1] :
( ~ l1_orders_2(X1)
| ~ m1_subset_1(X1,u1_struct_0(k4_waybel34(X0)))
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| v1_orders_2(X1)
| v2_setfam_1(X0) ),
inference(cnf_transformation,[],[f20846]) ).
fof(f21625,plain,
! [X0,X1] :
( m1_subset_1(X1,u1_struct_0(k4_waybel34(X0)))
| ~ v1_orders_2(X1)
| ~ v3_lattice3(X1)
| ~ r2_hidden(u1_struct_0(X1),X0)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ l1_orders_2(X1)
| v2_setfam_1(X0) ),
inference(cnf_transformation,[],[f20846]) ).
fof(f21626,plain,
! [X0] :
( v3_yellow21(k4_waybel34(X0))
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f20847]) ).
fof(f21639,plain,
! [X0] :
( sP0(X0)
| v2_setfam_1(X0) ),
inference(cnf_transformation,[],[f20721]) ).
fof(f21676,plain,
! [X0] :
( l2_altcat_1(k4_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f19030]) ).
fof(f21677,plain,
! [X0] :
( v2_yellow21(k4_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f19030]) ).
fof(f21678,plain,
! [X0] :
( v12_altcat_1(k4_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f19030]) ).
fof(f21679,plain,
! [X0] :
( v11_altcat_1(k4_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f19030]) ).
fof(f21681,plain,
! [X0] :
( v2_altcat_1(k4_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f19030]) ).
fof(f21682,plain,
! [X0] :
( ~ v3_struct_0(k4_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f19030]) ).
fof(f21688,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u1_struct_0(k5_waybel34(X0)))
| r2_hidden(u1_struct_0(X1),X0)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ l1_orders_2(X1)
| v2_setfam_1(X0) ),
inference(cnf_transformation,[],[f20867]) ).
fof(f21689,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u1_struct_0(k5_waybel34(X0)))
| v3_lattice3(X1)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ l1_orders_2(X1)
| v2_setfam_1(X0) ),
inference(cnf_transformation,[],[f20867]) ).
fof(f21690,plain,
! [X0,X1] :
( ~ l1_orders_2(X1)
| ~ m1_subset_1(X1,u1_struct_0(k5_waybel34(X0)))
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| v1_orders_2(X1)
| v2_setfam_1(X0) ),
inference(cnf_transformation,[],[f20867]) ).
fof(f21691,plain,
! [X0,X1] :
( m1_subset_1(X1,u1_struct_0(k5_waybel34(X0)))
| ~ v1_orders_2(X1)
| ~ v3_lattice3(X1)
| ~ r2_hidden(u1_struct_0(X1),X0)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ l1_orders_2(X1)
| v2_setfam_1(X0) ),
inference(cnf_transformation,[],[f20867]) ).
fof(f21742,plain,
! [X0] :
( l2_altcat_1(k5_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f19039]) ).
fof(f21743,plain,
! [X0] :
( v2_yellow21(k5_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f19039]) ).
fof(f21744,plain,
! [X0] :
( v12_altcat_1(k5_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f19039]) ).
fof(f21745,plain,
! [X0] :
( v11_altcat_1(k5_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f19039]) ).
fof(f21747,plain,
! [X0] :
( v2_altcat_1(k5_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f19039]) ).
fof(f21748,plain,
! [X0] :
( ~ v3_struct_0(k5_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f19039]) ).
fof(f21762,plain,
! [X0,X1] :
( r2_hidden(X1,X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f20888]) ).
fof(f21958,plain,
! [X0,X1] :
( m1_subset_1(X0,X1)
| ~ r2_hidden(X0,X1) ),
inference(cnf_transformation,[],[f19166]) ).
fof(f21961,plain,
! [X0,X1] :
( r2_hidden(sK130(X0,X1),X1)
| X0 = X1
| r2_hidden(sK130(X0,X1),X0) ),
inference(cnf_transformation,[],[f20944]) ).
fof(f21962,plain,
! [X0,X1] :
( ~ r2_hidden(sK130(X0,X1),X1)
| X0 = X1
| ~ r2_hidden(sK130(X0,X1),X0) ),
inference(cnf_transformation,[],[f20944]) ).
fof(f22032,plain,
! [X0,X1] :
( ~ v3_yellow21(X0)
| v3_struct_0(X0)
| ~ v2_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v12_altcat_1(X0)
| k1_yellow21(X1) = k4_yellow21(X0,X1)
| ~ l2_altcat_1(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f19211]) ).
fof(f22034,plain,
! [X0,X1] :
( ~ v3_yellow21(X0)
| v3_struct_0(X0)
| ~ v2_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v12_altcat_1(X0)
| v3_lattice3(k4_yellow21(X0,X1))
| ~ l2_altcat_1(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f19213]) ).
fof(f22035,plain,
! [X0,X1] :
( ~ v3_yellow21(X0)
| v3_struct_0(X0)
| ~ v2_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v12_altcat_1(X0)
| v2_lattice3(k4_yellow21(X0,X1))
| ~ l2_altcat_1(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f19213]) ).
fof(f22036,plain,
! [X0,X1] :
( ~ v3_yellow21(X0)
| v3_struct_0(X0)
| ~ v2_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v12_altcat_1(X0)
| v1_lattice3(k4_yellow21(X0,X1))
| ~ l2_altcat_1(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f19213]) ).
fof(f22037,plain,
! [X0,X1] :
( ~ v3_yellow21(X0)
| v3_struct_0(X0)
| ~ v2_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v12_altcat_1(X0)
| v4_orders_2(k4_yellow21(X0,X1))
| ~ l2_altcat_1(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f19213]) ).
fof(f22038,plain,
! [X0,X1] :
( ~ v3_yellow21(X0)
| v3_struct_0(X0)
| ~ v2_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v12_altcat_1(X0)
| v3_orders_2(k4_yellow21(X0,X1))
| ~ l2_altcat_1(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f19213]) ).
fof(f22039,plain,
! [X0,X1] :
( ~ v3_yellow21(X0)
| v3_struct_0(X0)
| ~ v2_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v12_altcat_1(X0)
| v2_orders_2(k4_yellow21(X0,X1))
| ~ l2_altcat_1(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f19213]) ).
fof(f22403,plain,
! [X0,X1] :
( ~ l2_altcat_1(X0)
| v3_struct_0(X0)
| ~ v2_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ v2_yellow21(X0)
| l1_orders_2(k3_yellow21(X0,X1))
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f19341]) ).
fof(f22404,plain,
! [X0,X1] :
( v2_lattice3(k3_yellow21(X0,X1))
| v3_struct_0(X0)
| ~ v2_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ v2_yellow21(X0)
| ~ l2_altcat_1(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f19341]) ).
fof(f22405,plain,
! [X0,X1] :
( v1_lattice3(k3_yellow21(X0,X1))
| v3_struct_0(X0)
| ~ v2_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ v2_yellow21(X0)
| ~ l2_altcat_1(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f19341]) ).
fof(f22406,plain,
! [X0,X1] :
( v4_orders_2(k3_yellow21(X0,X1))
| v3_struct_0(X0)
| ~ v2_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ v2_yellow21(X0)
| ~ l2_altcat_1(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f19341]) ).
fof(f22407,plain,
! [X0,X1] :
( v3_orders_2(k3_yellow21(X0,X1))
| v3_struct_0(X0)
| ~ v2_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ v2_yellow21(X0)
| ~ l2_altcat_1(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f19341]) ).
fof(f22408,plain,
! [X0,X1] :
( v2_orders_2(k3_yellow21(X0,X1))
| v3_struct_0(X0)
| ~ v2_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ v2_yellow21(X0)
| ~ l2_altcat_1(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f19341]) ).
fof(f22409,plain,
! [X0,X1] :
( k3_yellow21(X0,X1) = X1
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ v2_yellow21(X0)
| ~ l2_altcat_1(X0) ),
inference(cnf_transformation,[],[f19343]) ).
fof(f22423,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[],[f21033]) ).
fof(f23955,plain,
! [X0,X1] :
( ~ l2_altcat_1(X0)
| v3_struct_0(X0)
| ~ v2_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ v2_yellow21(X0)
| k1_yellow21(X1) = k3_yellow21(X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f20237]) ).
fof(f24420,plain,
! [X0] :
( l1_altcat_1(X0)
| ~ l2_altcat_1(X0) ),
inference(cnf_transformation,[],[f20516]) ).
fof(f24422,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_altcat_1(X0) ),
inference(cnf_transformation,[],[f20517]) ).
fof(f25032,definition,
sF539 = k4_waybel34(sK71),
introduced(definition,[new_symbols(definition,[sF539])],[function_definition]) ).
fof(f25033,plain,
k4_waybel34(sK71) = sF539,
inference(reorient_equations,[],[f25032]) ).
fof(f25034,definition,
sF540 = u1_struct_0(sF539),
introduced(definition,[new_symbols(definition,[sF540])],[function_definition]) ).
fof(f25035,plain,
u1_struct_0(sF539) = sF540,
inference(reorient_equations,[],[f25034]) ).
fof(f25036,definition,
sF541 = k5_waybel34(sK71),
introduced(definition,[new_symbols(definition,[sF541])],[function_definition]) ).
fof(f25037,plain,
k5_waybel34(sK71) = sF541,
inference(reorient_equations,[],[f25036]) ).
fof(f25038,definition,
sF542 = u1_struct_0(sF541),
introduced(definition,[new_symbols(definition,[sF542])],[function_definition]) ).
fof(f25039,plain,
u1_struct_0(sF541) = sF542,
inference(reorient_equations,[],[f25038]) ).
fof(f25040,plain,
sF540 != sF542,
inference(definition_folding,[],[f21601,f25039,f25037,f25035,f25033]) ).
fof(f25050,plain,
( ~ v3_struct_0(sF541)
| v1_xboole_0(sK71) ),
inference(superposition,[],[f21748,f25037]) ).
fof(f25052,definition,
( spl543_1
<=> v1_xboole_0(sK71) ),
introduced(definition,[new_symbols(definition,[spl543_1])],[avatar_definition]) ).
fof(f25056,definition,
( spl543_2
<=> v3_struct_0(sF541) ),
introduced(definition,[new_symbols(definition,[spl543_2])],[avatar_definition]) ).
fof(f25059,plain,
( spl543_1
| ~ spl543_2 ),
inference(avatar_split_clause,[],[f25050,f25056,f25052]) ).
fof(f25060,plain,
( ~ v3_struct_0(sF539)
| v1_xboole_0(sK71) ),
inference(superposition,[],[f21682,f25033]) ).
fof(f25062,definition,
( spl543_3
<=> v3_struct_0(sF539) ),
introduced(definition,[new_symbols(definition,[spl543_3])],[avatar_definition]) ).
fof(f25065,plain,
( spl543_1
| ~ spl543_3 ),
inference(avatar_split_clause,[],[f25060,f25062,f25052]) ).
fof(f25066,plain,
~ v1_xboole_0(sK71),
inference(resolution,[],[f21615,f21600]) ).
fof(f25067,plain,
~ spl543_1,
inference(avatar_split_clause,[],[f25066,f25052]) ).
fof(f25068,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sF539))
| r2_hidden(u1_struct_0(X0),sK71)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0)
| v2_setfam_1(sK71) ),
inference(superposition,[],[f21622,f25033]) ).
fof(f25069,plain,
! [X0] :
( ~ m1_subset_1(X0,sF540)
| r2_hidden(u1_struct_0(X0),sK71)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0)
| v2_setfam_1(sK71) ),
inference(forward_demodulation,[],[f25068,f25035]) ).
fof(f25071,definition,
( spl543_4
<=> v2_setfam_1(sK71) ),
introduced(definition,[new_symbols(definition,[spl543_4])],[avatar_definition]) ).
fof(f25072,plain,
( ~ v2_setfam_1(sK71)
| spl543_4 ),
inference(avatar_component_clause,[],[f25071]) ).
fof(f25075,definition,
( spl543_5
<=> ! [X0] :
( ~ m1_subset_1(X0,sF540)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| r2_hidden(u1_struct_0(X0),sK71) ) ),
introduced(definition,[new_symbols(definition,[spl543_5])],[avatar_definition]) ).
fof(f25076,plain,
( ! [X0] :
( r2_hidden(u1_struct_0(X0),sK71)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ m1_subset_1(X0,sF540) )
| ~ spl543_5 ),
inference(avatar_component_clause,[],[f25075]) ).
fof(f25077,plain,
( spl543_4
| spl543_5 ),
inference(avatar_split_clause,[],[f25069,f25075,f25071]) ).
fof(f25146,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sF541))
| r2_hidden(u1_struct_0(X0),sK71)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0)
| v2_setfam_1(sK71) ),
inference(superposition,[],[f21688,f25037]) ).
fof(f25147,plain,
! [X0] :
( ~ m1_subset_1(X0,sF542)
| r2_hidden(u1_struct_0(X0),sK71)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0)
| v2_setfam_1(sK71) ),
inference(forward_demodulation,[],[f25146,f25039]) ).
fof(f25149,definition,
( spl543_22
<=> ! [X0] :
( ~ m1_subset_1(X0,sF542)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| r2_hidden(u1_struct_0(X0),sK71) ) ),
introduced(definition,[new_symbols(definition,[spl543_22])],[avatar_definition]) ).
fof(f25150,plain,
( ! [X0] :
( r2_hidden(u1_struct_0(X0),sK71)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ m1_subset_1(X0,sF542) )
| ~ spl543_22 ),
inference(avatar_component_clause,[],[f25149]) ).
fof(f25151,plain,
( spl543_4
| spl543_22 ),
inference(avatar_split_clause,[],[f25147,f25149,f25071]) ).
fof(f25164,plain,
( v2_altcat_1(sF541)
| v1_xboole_0(sK71) ),
inference(superposition,[],[f21747,f25037]) ).
fof(f25166,definition,
( spl543_25
<=> v2_altcat_1(sF541) ),
introduced(definition,[new_symbols(definition,[spl543_25])],[avatar_definition]) ).
fof(f25169,plain,
( spl543_1
| spl543_25 ),
inference(avatar_split_clause,[],[f25164,f25166,f25052]) ).
fof(f25170,plain,
( v2_altcat_1(sF539)
| v1_xboole_0(sK71) ),
inference(superposition,[],[f21681,f25033]) ).
fof(f25172,definition,
( spl543_26
<=> v2_altcat_1(sF539) ),
introduced(definition,[new_symbols(definition,[spl543_26])],[avatar_definition]) ).
fof(f25175,plain,
( spl543_1
| spl543_26 ),
inference(avatar_split_clause,[],[f25170,f25172,f25052]) ).
fof(f25176,plain,
( l2_altcat_1(sF541)
| v1_xboole_0(sK71) ),
inference(superposition,[],[f21742,f25037]) ).
fof(f25178,definition,
( spl543_27
<=> l2_altcat_1(sF541) ),
introduced(definition,[new_symbols(definition,[spl543_27])],[avatar_definition]) ).
fof(f25180,plain,
( l2_altcat_1(sF541)
| ~ spl543_27 ),
inference(avatar_component_clause,[],[f25178]) ).
fof(f25181,plain,
( spl543_1
| spl543_27 ),
inference(avatar_split_clause,[],[f25176,f25178,f25052]) ).
fof(f25182,plain,
( v11_altcat_1(sF541)
| v1_xboole_0(sK71) ),
inference(superposition,[],[f21745,f25037]) ).
fof(f25184,definition,
( spl543_28
<=> v11_altcat_1(sF541) ),
introduced(definition,[new_symbols(definition,[spl543_28])],[avatar_definition]) ).
fof(f25187,plain,
( spl543_1
| spl543_28 ),
inference(avatar_split_clause,[],[f25182,f25184,f25052]) ).
fof(f25188,plain,
( v11_altcat_1(sF539)
| v1_xboole_0(sK71) ),
inference(superposition,[],[f21679,f25033]) ).
fof(f25190,definition,
( spl543_29
<=> v11_altcat_1(sF539) ),
introduced(definition,[new_symbols(definition,[spl543_29])],[avatar_definition]) ).
fof(f25193,plain,
( spl543_1
| spl543_29 ),
inference(avatar_split_clause,[],[f25188,f25190,f25052]) ).
fof(f25194,plain,
( l2_altcat_1(sF539)
| v1_xboole_0(sK71) ),
inference(superposition,[],[f21676,f25033]) ).
fof(f25196,definition,
( spl543_30
<=> l2_altcat_1(sF539) ),
introduced(definition,[new_symbols(definition,[spl543_30])],[avatar_definition]) ).
fof(f25198,plain,
( l2_altcat_1(sF539)
| ~ spl543_30 ),
inference(avatar_component_clause,[],[f25196]) ).
fof(f25199,plain,
( spl543_1
| spl543_30 ),
inference(avatar_split_clause,[],[f25194,f25196,f25052]) ).
fof(f25200,plain,
( v2_yellow21(sF541)
| v1_xboole_0(sK71) ),
inference(superposition,[],[f21743,f25037]) ).
fof(f25202,definition,
( spl543_31
<=> v2_yellow21(sF541) ),
introduced(definition,[new_symbols(definition,[spl543_31])],[avatar_definition]) ).
fof(f25205,plain,
( spl543_1
| spl543_31 ),
inference(avatar_split_clause,[],[f25200,f25202,f25052]) ).
fof(f25206,plain,
( v2_yellow21(sF539)
| v1_xboole_0(sK71) ),
inference(superposition,[],[f21677,f25033]) ).
fof(f25208,definition,
( spl543_32
<=> v2_yellow21(sF539) ),
introduced(definition,[new_symbols(definition,[spl543_32])],[avatar_definition]) ).
fof(f25211,plain,
( spl543_1
| spl543_32 ),
inference(avatar_split_clause,[],[f25206,f25208,f25052]) ).
fof(f25212,plain,
( v12_altcat_1(sF541)
| v1_xboole_0(sK71) ),
inference(superposition,[],[f21744,f25037]) ).
fof(f25214,definition,
( spl543_33
<=> v12_altcat_1(sF541) ),
introduced(definition,[new_symbols(definition,[spl543_33])],[avatar_definition]) ).
fof(f25217,plain,
( spl543_1
| spl543_33 ),
inference(avatar_split_clause,[],[f25212,f25214,f25052]) ).
fof(f25218,plain,
( v12_altcat_1(sF539)
| v1_xboole_0(sK71) ),
inference(superposition,[],[f21678,f25033]) ).
fof(f25220,definition,
( spl543_34
<=> v12_altcat_1(sF539) ),
introduced(definition,[new_symbols(definition,[spl543_34])],[avatar_definition]) ).
fof(f25223,plain,
( spl543_1
| spl543_34 ),
inference(avatar_split_clause,[],[f25218,f25220,f25052]) ).
fof(f25227,plain,
( ~ v1_xboole_0(sF540)
| v3_struct_0(sF539)
| ~ l1_struct_0(sF539) ),
inference(superposition,[],[f22423,f25035]) ).
fof(f25228,plain,
( ~ v1_xboole_0(sF542)
| v3_struct_0(sF541)
| ~ l1_struct_0(sF541) ),
inference(superposition,[],[f22423,f25039]) ).
fof(f25230,definition,
( spl543_35
<=> l1_struct_0(sF541) ),
introduced(definition,[new_symbols(definition,[spl543_35])],[avatar_definition]) ).
fof(f25232,plain,
( ~ l1_struct_0(sF541)
| spl543_35 ),
inference(avatar_component_clause,[],[f25230]) ).
fof(f25234,definition,
( spl543_36
<=> v1_xboole_0(sF542) ),
introduced(definition,[new_symbols(definition,[spl543_36])],[avatar_definition]) ).
fof(f25237,plain,
( ~ spl543_35
| spl543_2
| ~ spl543_36 ),
inference(avatar_split_clause,[],[f25228,f25234,f25056,f25230]) ).
fof(f25239,definition,
( spl543_37
<=> l1_struct_0(sF539) ),
introduced(definition,[new_symbols(definition,[spl543_37])],[avatar_definition]) ).
fof(f25241,plain,
( ~ l1_struct_0(sF539)
| spl543_37 ),
inference(avatar_component_clause,[],[f25239]) ).
fof(f25243,definition,
( spl543_38
<=> v1_xboole_0(sF540) ),
introduced(definition,[new_symbols(definition,[spl543_38])],[avatar_definition]) ).
fof(f25246,plain,
( ~ spl543_37
| spl543_3
| ~ spl543_38 ),
inference(avatar_split_clause,[],[f25227,f25243,f25062,f25239]) ).
fof(f25278,plain,
( ~ l1_altcat_1(sF539)
| spl543_37 ),
inference(resolution,[],[f25241,f24422]) ).
fof(f25285,plain,
( ~ l1_altcat_1(sF541)
| spl543_35 ),
inference(resolution,[],[f25232,f24422]) ).
fof(f25315,plain,
( ~ l2_altcat_1(sF539)
| spl543_37 ),
inference(resolution,[],[f25278,f24420]) ).
fof(f25316,plain,
( ~ spl543_30
| spl543_37 ),
inference(avatar_split_clause,[],[f25315,f25239,f25196]) ).
fof(f25317,plain,
( ~ l2_altcat_1(sF541)
| spl543_35 ),
inference(resolution,[],[f25285,f24420]) ).
fof(f25318,plain,
( ~ spl543_27
| spl543_35 ),
inference(avatar_split_clause,[],[f25317,f25230,f25178]) ).
fof(f25321,definition,
( spl543_43
<=> sP0(sK71) ),
introduced(definition,[new_symbols(definition,[spl543_43])],[avatar_definition]) ).
fof(f25323,plain,
( ~ sP0(sK71)
| spl543_43 ),
inference(avatar_component_clause,[],[f25321]) ).
fof(f25329,plain,
( v2_setfam_1(sK71)
| spl543_43 ),
inference(resolution,[],[f25323,f21639]) ).
fof(f25330,plain,
( spl543_4
| spl543_43 ),
inference(avatar_split_clause,[],[f25329,f25321,f25071]) ).
fof(f25333,plain,
~ spl543_4,
inference(avatar_split_clause,[],[f21600,f25071]) ).
fof(f25444,plain,
! [X0] :
( m1_subset_1(X0,u1_struct_0(sF539))
| ~ v1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ r2_hidden(u1_struct_0(X0),sK71)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0)
| v2_setfam_1(sK71) ),
inference(superposition,[],[f21625,f25033]) ).
fof(f25447,plain,
! [X0] :
( m1_subset_1(X0,sF540)
| ~ v1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ r2_hidden(u1_struct_0(X0),sK71)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0)
| v2_setfam_1(sK71) ),
inference(forward_demodulation,[],[f25444,f25035]) ).
fof(f25449,definition,
( spl543_56
<=> ! [X0] :
( m1_subset_1(X0,sF540)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ r2_hidden(u1_struct_0(X0),sK71)
| ~ v3_lattice3(X0)
| ~ v1_orders_2(X0) ) ),
introduced(definition,[new_symbols(definition,[spl543_56])],[avatar_definition]) ).
fof(f25450,plain,
( ! [X0] :
( ~ r2_hidden(u1_struct_0(X0),sK71)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| m1_subset_1(X0,sF540)
| ~ v3_lattice3(X0)
| ~ v1_orders_2(X0) )
| ~ spl543_56 ),
inference(avatar_component_clause,[],[f25449]) ).
fof(f25451,plain,
( spl543_4
| spl543_56 ),
inference(avatar_split_clause,[],[f25447,f25449,f25071]) ).
fof(f25480,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sF541))
| v3_lattice3(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0)
| v2_setfam_1(sK71) ),
inference(superposition,[],[f21689,f25037]) ).
fof(f25481,plain,
! [X0] :
( ~ m1_subset_1(X0,sF542)
| v3_lattice3(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0)
| v2_setfam_1(sK71) ),
inference(forward_demodulation,[],[f25480,f25039]) ).
fof(f25483,definition,
( spl543_59
<=> ! [X0] :
( ~ m1_subset_1(X0,sF542)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| v3_lattice3(X0) ) ),
introduced(definition,[new_symbols(definition,[spl543_59])],[avatar_definition]) ).
fof(f25484,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF542)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| v3_lattice3(X0) )
| ~ spl543_59 ),
inference(avatar_component_clause,[],[f25483]) ).
fof(f25485,plain,
( spl543_4
| spl543_59 ),
inference(avatar_split_clause,[],[f25481,f25483,f25071]) ).
fof(f25505,plain,
! [X0] :
( m1_subset_1(X0,u1_struct_0(sF541))
| ~ v1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ r2_hidden(u1_struct_0(X0),sK71)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0)
| v2_setfam_1(sK71) ),
inference(superposition,[],[f21691,f25037]) ).
fof(f25508,plain,
! [X0] :
( m1_subset_1(X0,sF542)
| ~ v1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ r2_hidden(u1_struct_0(X0),sK71)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0)
| v2_setfam_1(sK71) ),
inference(forward_demodulation,[],[f25505,f25039]) ).
fof(f25510,definition,
( spl543_60
<=> ! [X0] :
( m1_subset_1(X0,sF542)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ r2_hidden(u1_struct_0(X0),sK71)
| ~ v3_lattice3(X0)
| ~ v1_orders_2(X0) ) ),
introduced(definition,[new_symbols(definition,[spl543_60])],[avatar_definition]) ).
fof(f25511,plain,
( ! [X0] :
( ~ r2_hidden(u1_struct_0(X0),sK71)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| m1_subset_1(X0,sF542)
| ~ v3_lattice3(X0)
| ~ v1_orders_2(X0) )
| ~ spl543_60 ),
inference(avatar_component_clause,[],[f25510]) ).
fof(f25512,plain,
( spl543_4
| spl543_60 ),
inference(avatar_split_clause,[],[f25508,f25510,f25071]) ).
fof(f25598,plain,
( v3_yellow21(sF539)
| ~ sP0(sK71) ),
inference(superposition,[],[f21626,f25033]) ).
fof(f25600,definition,
( spl543_68
<=> v3_yellow21(sF539) ),
introduced(definition,[new_symbols(definition,[spl543_68])],[avatar_definition]) ).
fof(f25602,plain,
( v3_yellow21(sF539)
| ~ spl543_68 ),
inference(avatar_component_clause,[],[f25600]) ).
fof(f25603,plain,
( ~ spl543_43
| spl543_68 ),
inference(avatar_split_clause,[],[f25598,f25600,f25321]) ).
fof(f25675,plain,
( ! [X0] :
( v3_struct_0(sF539)
| ~ v2_altcat_1(sF539)
| ~ v11_altcat_1(sF539)
| ~ v12_altcat_1(sF539)
| ~ v2_yellow21(sF539)
| k1_yellow21(X0) = k3_yellow21(sF539,X0)
| ~ m1_subset_1(X0,u1_struct_0(sF539)) )
| ~ spl543_30 ),
inference(resolution,[],[f23955,f25198]) ).
fof(f25676,plain,
( ! [X0] :
( v3_struct_0(sF541)
| ~ v2_altcat_1(sF541)
| ~ v11_altcat_1(sF541)
| ~ v12_altcat_1(sF541)
| ~ v2_yellow21(sF541)
| k1_yellow21(X0) = k3_yellow21(sF541,X0)
| ~ m1_subset_1(X0,u1_struct_0(sF541)) )
| ~ spl543_27 ),
inference(resolution,[],[f23955,f25180]) ).
fof(f25677,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF542)
| v3_struct_0(sF541)
| ~ v2_altcat_1(sF541)
| ~ v11_altcat_1(sF541)
| ~ v12_altcat_1(sF541)
| ~ v2_yellow21(sF541)
| k1_yellow21(X0) = k3_yellow21(sF541,X0) )
| ~ spl543_27 ),
inference(forward_demodulation,[],[f25676,f25039]) ).
fof(f25678,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF540)
| v3_struct_0(sF539)
| ~ v2_altcat_1(sF539)
| ~ v11_altcat_1(sF539)
| ~ v12_altcat_1(sF539)
| ~ v2_yellow21(sF539)
| k1_yellow21(X0) = k3_yellow21(sF539,X0) )
| ~ spl543_30 ),
inference(forward_demodulation,[],[f25675,f25035]) ).
fof(f25680,definition,
( spl543_71
<=> ! [X0] :
( ~ m1_subset_1(X0,sF542)
| k1_yellow21(X0) = k3_yellow21(sF541,X0) ) ),
introduced(definition,[new_symbols(definition,[spl543_71])],[avatar_definition]) ).
fof(f25681,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF542)
| k1_yellow21(X0) = k3_yellow21(sF541,X0) )
| ~ spl543_71 ),
inference(avatar_component_clause,[],[f25680]) ).
fof(f25682,plain,
( ~ spl543_31
| ~ spl543_33
| ~ spl543_28
| ~ spl543_25
| spl543_2
| spl543_71
| ~ spl543_27 ),
inference(avatar_split_clause,[],[f25677,f25178,f25680,f25056,f25166,f25184,f25214,f25202]) ).
fof(f25684,definition,
( spl543_72
<=> ! [X0] :
( ~ m1_subset_1(X0,sF540)
| k1_yellow21(X0) = k3_yellow21(sF539,X0) ) ),
introduced(definition,[new_symbols(definition,[spl543_72])],[avatar_definition]) ).
fof(f25685,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF540)
| k1_yellow21(X0) = k3_yellow21(sF539,X0) )
| ~ spl543_72 ),
inference(avatar_component_clause,[],[f25684]) ).
fof(f25686,plain,
( ~ spl543_32
| ~ spl543_34
| ~ spl543_29
| ~ spl543_26
| spl543_3
| spl543_72
| ~ spl543_30 ),
inference(avatar_split_clause,[],[f25678,f25196,f25684,f25062,f25172,f25190,f25220,f25208]) ).
fof(f25688,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF540)
| k1_yellow21(X0) = k3_yellow21(sF539,X0) )
| ~ spl543_72 ),
inference(resolution,[],[f25685,f21958]) ).
fof(f25700,plain,
( ! [X0] :
( r2_hidden(sK130(X0,sF540),X0)
| sF540 = X0
| k1_yellow21(sK130(X0,sF540)) = k3_yellow21(sF539,sK130(X0,sF540)) )
| ~ spl543_72 ),
inference(resolution,[],[f25688,f21961]) ).
fof(f25897,definition,
( spl543_94
<=> k1_yellow21(sK130(sF542,sF540)) = k3_yellow21(sF541,sK130(sF542,sF540)) ),
introduced(definition,[new_symbols(definition,[spl543_94])],[avatar_definition]) ).
fof(f25899,plain,
( k1_yellow21(sK130(sF542,sF540)) = k3_yellow21(sF541,sK130(sF542,sF540))
| ~ spl543_94 ),
inference(avatar_component_clause,[],[f25897]) ).
fof(f25901,definition,
( spl543_95
<=> sF540 = sF542 ),
introduced(definition,[new_symbols(definition,[spl543_95])],[avatar_definition]) ).
fof(f25906,definition,
( spl543_96
<=> k1_yellow21(sK130(sF542,sF540)) = k3_yellow21(sF539,sK130(sF542,sF540)) ),
introduced(definition,[new_symbols(definition,[spl543_96])],[avatar_definition]) ).
fof(f25908,plain,
( k1_yellow21(sK130(sF542,sF540)) = k3_yellow21(sF539,sK130(sF542,sF540))
| ~ spl543_96 ),
inference(avatar_component_clause,[],[f25906]) ).
fof(f25920,plain,
( sK130(sF542,sF540) = k1_yellow21(sK130(sF542,sF540))
| ~ m1_subset_1(sK130(sF542,sF540),u1_struct_0(sF541))
| v3_struct_0(sF541)
| ~ v2_altcat_1(sF541)
| ~ v11_altcat_1(sF541)
| ~ v12_altcat_1(sF541)
| ~ v2_yellow21(sF541)
| ~ l2_altcat_1(sF541)
| ~ spl543_94 ),
inference(superposition,[],[f25899,f22409]) ).
fof(f25933,plain,
( ~ m1_subset_1(sK130(sF542,sF540),sF542)
| sK130(sF542,sF540) = k1_yellow21(sK130(sF542,sF540))
| v3_struct_0(sF541)
| ~ v2_altcat_1(sF541)
| ~ v11_altcat_1(sF541)
| ~ v12_altcat_1(sF541)
| ~ v2_yellow21(sF541)
| ~ l2_altcat_1(sF541)
| ~ spl543_94 ),
inference(forward_demodulation,[],[f25920,f25039]) ).
fof(f25935,definition,
( spl543_98
<=> sK130(sF542,sF540) = k1_yellow21(sK130(sF542,sF540)) ),
introduced(definition,[new_symbols(definition,[spl543_98])],[avatar_definition]) ).
fof(f25937,plain,
( sK130(sF542,sF540) = k1_yellow21(sK130(sF542,sF540))
| ~ spl543_98 ),
inference(avatar_component_clause,[],[f25935]) ).
fof(f25939,definition,
( spl543_99
<=> m1_subset_1(sK130(sF542,sF540),sF542) ),
introduced(definition,[new_symbols(definition,[spl543_99])],[avatar_definition]) ).
fof(f25940,plain,
( m1_subset_1(sK130(sF542,sF540),sF542)
| ~ spl543_99 ),
inference(avatar_component_clause,[],[f25939]) ).
fof(f25941,plain,
( ~ m1_subset_1(sK130(sF542,sF540),sF542)
| spl543_99 ),
inference(avatar_component_clause,[],[f25939]) ).
fof(f25968,plain,
( ~ spl543_27
| ~ spl543_31
| ~ spl543_33
| ~ spl543_28
| ~ spl543_25
| spl543_2
| spl543_98
| ~ spl543_99
| ~ spl543_94 ),
inference(avatar_split_clause,[],[f25933,f25897,f25939,f25935,f25056,f25166,f25184,f25214,f25202,f25178]) ).
fof(f25970,plain,
( ~ r2_hidden(sK130(sF542,sF540),sF542)
| spl543_99 ),
inference(resolution,[],[f25941,f21958]) ).
fof(f25986,definition,
( spl543_105
<=> r2_hidden(sK130(sF542,sF540),sF542) ),
introduced(definition,[new_symbols(definition,[spl543_105])],[avatar_definition]) ).
fof(f25987,plain,
( ~ r2_hidden(sK130(sF542,sF540),sF542)
| spl543_105 ),
inference(avatar_component_clause,[],[f25986]) ).
fof(f26012,plain,
~ spl543_95,
inference(avatar_split_clause,[],[f25040,f25901]) ).
fof(f26013,plain,
( ~ spl543_105
| spl543_99 ),
inference(avatar_split_clause,[],[f25970,f25939,f25986]) ).
fof(f26118,plain,
( ! [X0] :
( v3_struct_0(sF539)
| ~ v2_altcat_1(sF539)
| ~ v11_altcat_1(sF539)
| ~ v12_altcat_1(sF539)
| ~ v2_yellow21(sF539)
| l1_orders_2(k3_yellow21(sF539,X0))
| ~ m1_subset_1(X0,u1_struct_0(sF539)) )
| ~ spl543_30 ),
inference(resolution,[],[f22403,f25198]) ).
fof(f26119,plain,
( ! [X0] :
( v3_struct_0(sF541)
| ~ v2_altcat_1(sF541)
| ~ v11_altcat_1(sF541)
| ~ v12_altcat_1(sF541)
| ~ v2_yellow21(sF541)
| l1_orders_2(k3_yellow21(sF541,X0))
| ~ m1_subset_1(X0,u1_struct_0(sF541)) )
| ~ spl543_27 ),
inference(resolution,[],[f22403,f25180]) ).
fof(f26120,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF542)
| v3_struct_0(sF541)
| ~ v2_altcat_1(sF541)
| ~ v11_altcat_1(sF541)
| ~ v12_altcat_1(sF541)
| ~ v2_yellow21(sF541)
| l1_orders_2(k3_yellow21(sF541,X0)) )
| ~ spl543_27 ),
inference(forward_demodulation,[],[f26119,f25039]) ).
fof(f26121,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF540)
| v3_struct_0(sF539)
| ~ v2_altcat_1(sF539)
| ~ v11_altcat_1(sF539)
| ~ v12_altcat_1(sF539)
| ~ v2_yellow21(sF539)
| l1_orders_2(k3_yellow21(sF539,X0)) )
| ~ spl543_30 ),
inference(forward_demodulation,[],[f26118,f25035]) ).
fof(f26123,definition,
( spl543_116
<=> ! [X0] :
( ~ m1_subset_1(X0,sF542)
| l1_orders_2(k3_yellow21(sF541,X0)) ) ),
introduced(definition,[new_symbols(definition,[spl543_116])],[avatar_definition]) ).
fof(f26124,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF542)
| l1_orders_2(k3_yellow21(sF541,X0)) )
| ~ spl543_116 ),
inference(avatar_component_clause,[],[f26123]) ).
fof(f26125,plain,
( ~ spl543_31
| ~ spl543_33
| ~ spl543_28
| ~ spl543_25
| spl543_2
| spl543_116
| ~ spl543_27 ),
inference(avatar_split_clause,[],[f26120,f25178,f26123,f25056,f25166,f25184,f25214,f25202]) ).
fof(f26127,definition,
( spl543_117
<=> ! [X0] :
( ~ m1_subset_1(X0,sF540)
| l1_orders_2(k3_yellow21(sF539,X0)) ) ),
introduced(definition,[new_symbols(definition,[spl543_117])],[avatar_definition]) ).
fof(f26128,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF540)
| l1_orders_2(k3_yellow21(sF539,X0)) )
| ~ spl543_117 ),
inference(avatar_component_clause,[],[f26127]) ).
fof(f26129,plain,
( ~ spl543_32
| ~ spl543_34
| ~ spl543_29
| ~ spl543_26
| spl543_3
| spl543_117
| ~ spl543_30 ),
inference(avatar_split_clause,[],[f26121,f25196,f26127,f25062,f25172,f25190,f25220,f25208]) ).
fof(f26134,plain,
( sF540 = sF542
| k1_yellow21(sK130(sF542,sF540)) = k3_yellow21(sF539,sK130(sF542,sF540))
| ~ spl543_72
| spl543_105 ),
inference(resolution,[],[f25700,f25987]) ).
fof(f26141,plain,
( spl543_96
| spl543_95
| ~ spl543_72
| spl543_105 ),
inference(avatar_split_clause,[],[f26134,f25986,f25684,f25901,f25906]) ).
fof(f26142,plain,
( sK130(sF542,sF540) = k1_yellow21(sK130(sF542,sF540))
| ~ m1_subset_1(sK130(sF542,sF540),u1_struct_0(sF539))
| v3_struct_0(sF539)
| ~ v2_altcat_1(sF539)
| ~ v11_altcat_1(sF539)
| ~ v12_altcat_1(sF539)
| ~ v2_yellow21(sF539)
| ~ l2_altcat_1(sF539)
| ~ spl543_96 ),
inference(superposition,[],[f25908,f22409]) ).
fof(f26155,plain,
( ~ m1_subset_1(sK130(sF542,sF540),sF540)
| sK130(sF542,sF540) = k1_yellow21(sK130(sF542,sF540))
| v3_struct_0(sF539)
| ~ v2_altcat_1(sF539)
| ~ v11_altcat_1(sF539)
| ~ v12_altcat_1(sF539)
| ~ v2_yellow21(sF539)
| ~ l2_altcat_1(sF539)
| ~ spl543_96 ),
inference(forward_demodulation,[],[f26142,f25035]) ).
fof(f26157,definition,
( spl543_118
<=> m1_subset_1(sK130(sF542,sF540),sF540) ),
introduced(definition,[new_symbols(definition,[spl543_118])],[avatar_definition]) ).
fof(f26158,plain,
( m1_subset_1(sK130(sF542,sF540),sF540)
| ~ spl543_118 ),
inference(avatar_component_clause,[],[f26157]) ).
fof(f26159,plain,
( ~ m1_subset_1(sK130(sF542,sF540),sF540)
| spl543_118 ),
inference(avatar_component_clause,[],[f26157]) ).
fof(f26166,plain,
( ~ spl543_30
| ~ spl543_32
| ~ spl543_34
| ~ spl543_29
| ~ spl543_26
| spl543_3
| spl543_98
| ~ spl543_118
| ~ spl543_96 ),
inference(avatar_split_clause,[],[f26155,f25906,f26157,f25935,f25062,f25172,f25190,f25220,f25208,f25196]) ).
fof(f26167,plain,
( ~ r2_hidden(sK130(sF542,sF540),sF540)
| spl543_118 ),
inference(resolution,[],[f26159,f21958]) ).
fof(f26168,plain,
( sF540 = sF542
| r2_hidden(sK130(sF542,sF540),sF542)
| spl543_118 ),
inference(resolution,[],[f26167,f21961]) ).
fof(f26172,plain,
( spl543_105
| spl543_95
| spl543_118 ),
inference(avatar_split_clause,[],[f26168,f26157,f25901,f25986]) ).
fof(f26173,plain,
( l1_orders_2(k3_yellow21(sF541,sK130(sF542,sF540)))
| ~ spl543_99
| ~ spl543_116 ),
inference(resolution,[],[f25940,f26124]) ).
fof(f26174,plain,
( k1_yellow21(sK130(sF542,sF540)) = k3_yellow21(sF541,sK130(sF542,sF540))
| ~ spl543_71
| ~ spl543_99 ),
inference(resolution,[],[f25940,f25681]) ).
fof(f26175,plain,
( ~ l1_orders_2(sK130(sF542,sF540))
| ~ v2_lattice3(sK130(sF542,sF540))
| ~ v1_lattice3(sK130(sF542,sF540))
| ~ v4_orders_2(sK130(sF542,sF540))
| ~ v3_orders_2(sK130(sF542,sF540))
| ~ v2_orders_2(sK130(sF542,sF540))
| v3_lattice3(sK130(sF542,sF540))
| ~ spl543_59
| ~ spl543_99 ),
inference(resolution,[],[f25940,f25484]) ).
fof(f26177,definition,
( spl543_119
<=> v3_lattice3(sK130(sF542,sF540)) ),
introduced(definition,[new_symbols(definition,[spl543_119])],[avatar_definition]) ).
fof(f26181,definition,
( spl543_120
<=> v2_orders_2(sK130(sF542,sF540)) ),
introduced(definition,[new_symbols(definition,[spl543_120])],[avatar_definition]) ).
fof(f26185,definition,
( spl543_121
<=> v3_orders_2(sK130(sF542,sF540)) ),
introduced(definition,[new_symbols(definition,[spl543_121])],[avatar_definition]) ).
fof(f26189,definition,
( spl543_122
<=> v4_orders_2(sK130(sF542,sF540)) ),
introduced(definition,[new_symbols(definition,[spl543_122])],[avatar_definition]) ).
fof(f26193,definition,
( spl543_123
<=> v1_lattice3(sK130(sF542,sF540)) ),
introduced(definition,[new_symbols(definition,[spl543_123])],[avatar_definition]) ).
fof(f26197,definition,
( spl543_124
<=> v2_lattice3(sK130(sF542,sF540)) ),
introduced(definition,[new_symbols(definition,[spl543_124])],[avatar_definition]) ).
fof(f26201,definition,
( spl543_125
<=> l1_orders_2(sK130(sF542,sF540)) ),
introduced(definition,[new_symbols(definition,[spl543_125])],[avatar_definition]) ).
fof(f26202,plain,
( l1_orders_2(sK130(sF542,sF540))
| ~ spl543_125 ),
inference(avatar_component_clause,[],[f26201]) ).
fof(f26204,plain,
( spl543_119
| ~ spl543_120
| ~ spl543_121
| ~ spl543_122
| ~ spl543_123
| ~ spl543_124
| ~ spl543_125
| ~ spl543_59
| ~ spl543_99 ),
inference(avatar_split_clause,[],[f26175,f25939,f25483,f26201,f26197,f26193,f26189,f26185,f26181,f26177]) ).
fof(f26205,plain,
( spl543_94
| ~ spl543_71
| ~ spl543_99 ),
inference(avatar_split_clause,[],[f26174,f25939,f25680,f25897]) ).
fof(f26209,plain,
( sK130(sF542,sF540) = k3_yellow21(sF541,sK130(sF542,sF540))
| ~ spl543_94
| ~ spl543_98 ),
inference(forward_demodulation,[],[f25899,f25937]) ).
fof(f26210,plain,
( v2_orders_2(sK130(sF542,sF540))
| v3_struct_0(sF541)
| ~ v2_altcat_1(sF541)
| ~ v11_altcat_1(sF541)
| ~ v12_altcat_1(sF541)
| ~ v2_yellow21(sF541)
| ~ l2_altcat_1(sF541)
| ~ m1_subset_1(sK130(sF542,sF540),u1_struct_0(sF541))
| ~ spl543_94
| ~ spl543_98 ),
inference(superposition,[],[f22408,f26209]) ).
fof(f26211,plain,
( v4_orders_2(sK130(sF542,sF540))
| v3_struct_0(sF541)
| ~ v2_altcat_1(sF541)
| ~ v11_altcat_1(sF541)
| ~ v12_altcat_1(sF541)
| ~ v2_yellow21(sF541)
| ~ l2_altcat_1(sF541)
| ~ m1_subset_1(sK130(sF542,sF540),u1_struct_0(sF541))
| ~ spl543_94
| ~ spl543_98 ),
inference(superposition,[],[f22406,f26209]) ).
fof(f26212,plain,
( v1_lattice3(sK130(sF542,sF540))
| v3_struct_0(sF541)
| ~ v2_altcat_1(sF541)
| ~ v11_altcat_1(sF541)
| ~ v12_altcat_1(sF541)
| ~ v2_yellow21(sF541)
| ~ l2_altcat_1(sF541)
| ~ m1_subset_1(sK130(sF542,sF540),u1_struct_0(sF541))
| ~ spl543_94
| ~ spl543_98 ),
inference(superposition,[],[f22405,f26209]) ).
fof(f26213,plain,
( v2_lattice3(sK130(sF542,sF540))
| v3_struct_0(sF541)
| ~ v2_altcat_1(sF541)
| ~ v11_altcat_1(sF541)
| ~ v12_altcat_1(sF541)
| ~ v2_yellow21(sF541)
| ~ l2_altcat_1(sF541)
| ~ m1_subset_1(sK130(sF542,sF540),u1_struct_0(sF541))
| ~ spl543_94
| ~ spl543_98 ),
inference(superposition,[],[f22404,f26209]) ).
fof(f26214,plain,
( v3_orders_2(sK130(sF542,sF540))
| v3_struct_0(sF541)
| ~ v2_altcat_1(sF541)
| ~ v11_altcat_1(sF541)
| ~ v12_altcat_1(sF541)
| ~ v2_yellow21(sF541)
| ~ l2_altcat_1(sF541)
| ~ m1_subset_1(sK130(sF542,sF540),u1_struct_0(sF541))
| ~ spl543_94
| ~ spl543_98 ),
inference(superposition,[],[f22407,f26209]) ).
fof(f26215,plain,
( ~ m1_subset_1(sK130(sF542,sF540),sF542)
| v3_orders_2(sK130(sF542,sF540))
| v3_struct_0(sF541)
| ~ v2_altcat_1(sF541)
| ~ v11_altcat_1(sF541)
| ~ v12_altcat_1(sF541)
| ~ v2_yellow21(sF541)
| ~ l2_altcat_1(sF541)
| ~ spl543_94
| ~ spl543_98 ),
inference(forward_demodulation,[],[f26214,f25039]) ).
fof(f26216,plain,
( ~ m1_subset_1(sK130(sF542,sF540),sF542)
| v2_lattice3(sK130(sF542,sF540))
| v3_struct_0(sF541)
| ~ v2_altcat_1(sF541)
| ~ v11_altcat_1(sF541)
| ~ v12_altcat_1(sF541)
| ~ v2_yellow21(sF541)
| ~ l2_altcat_1(sF541)
| ~ spl543_94
| ~ spl543_98 ),
inference(forward_demodulation,[],[f26213,f25039]) ).
fof(f26217,plain,
( ~ m1_subset_1(sK130(sF542,sF540),sF542)
| v1_lattice3(sK130(sF542,sF540))
| v3_struct_0(sF541)
| ~ v2_altcat_1(sF541)
| ~ v11_altcat_1(sF541)
| ~ v12_altcat_1(sF541)
| ~ v2_yellow21(sF541)
| ~ l2_altcat_1(sF541)
| ~ spl543_94
| ~ spl543_98 ),
inference(forward_demodulation,[],[f26212,f25039]) ).
fof(f26218,plain,
( ~ m1_subset_1(sK130(sF542,sF540),sF542)
| v4_orders_2(sK130(sF542,sF540))
| v3_struct_0(sF541)
| ~ v2_altcat_1(sF541)
| ~ v11_altcat_1(sF541)
| ~ v12_altcat_1(sF541)
| ~ v2_yellow21(sF541)
| ~ l2_altcat_1(sF541)
| ~ spl543_94
| ~ spl543_98 ),
inference(forward_demodulation,[],[f26211,f25039]) ).
fof(f26219,plain,
( ~ m1_subset_1(sK130(sF542,sF540),sF542)
| v2_orders_2(sK130(sF542,sF540))
| v3_struct_0(sF541)
| ~ v2_altcat_1(sF541)
| ~ v11_altcat_1(sF541)
| ~ v12_altcat_1(sF541)
| ~ v2_yellow21(sF541)
| ~ l2_altcat_1(sF541)
| ~ spl543_94
| ~ spl543_98 ),
inference(forward_demodulation,[],[f26210,f25039]) ).
fof(f26220,plain,
( ~ spl543_27
| ~ spl543_31
| ~ spl543_33
| ~ spl543_28
| ~ spl543_25
| spl543_2
| spl543_121
| ~ spl543_99
| ~ spl543_94
| ~ spl543_98 ),
inference(avatar_split_clause,[],[f26215,f25935,f25897,f25939,f26185,f25056,f25166,f25184,f25214,f25202,f25178]) ).
fof(f26221,plain,
( ~ spl543_27
| ~ spl543_31
| ~ spl543_33
| ~ spl543_28
| ~ spl543_25
| spl543_2
| spl543_124
| ~ spl543_99
| ~ spl543_94
| ~ spl543_98 ),
inference(avatar_split_clause,[],[f26216,f25935,f25897,f25939,f26197,f25056,f25166,f25184,f25214,f25202,f25178]) ).
fof(f26222,plain,
( ~ spl543_27
| ~ spl543_31
| ~ spl543_33
| ~ spl543_28
| ~ spl543_25
| spl543_2
| spl543_123
| ~ spl543_99
| ~ spl543_94
| ~ spl543_98 ),
inference(avatar_split_clause,[],[f26217,f25935,f25897,f25939,f26193,f25056,f25166,f25184,f25214,f25202,f25178]) ).
fof(f26223,plain,
( ~ spl543_27
| ~ spl543_31
| ~ spl543_33
| ~ spl543_28
| ~ spl543_25
| spl543_2
| spl543_122
| ~ spl543_99
| ~ spl543_94
| ~ spl543_98 ),
inference(avatar_split_clause,[],[f26218,f25935,f25897,f25939,f26189,f25056,f25166,f25184,f25214,f25202,f25178]) ).
fof(f26224,plain,
( ~ spl543_27
| ~ spl543_31
| ~ spl543_33
| ~ spl543_28
| ~ spl543_25
| spl543_2
| spl543_120
| ~ spl543_99
| ~ spl543_94
| ~ spl543_98 ),
inference(avatar_split_clause,[],[f26219,f25935,f25897,f25939,f26181,f25056,f25166,f25184,f25214,f25202,f25178]) ).
fof(f26225,plain,
( l1_orders_2(k3_yellow21(sF539,sK130(sF542,sF540)))
| ~ spl543_117
| ~ spl543_118 ),
inference(resolution,[],[f26158,f26128]) ).
fof(f26228,plain,
( l1_orders_2(k1_yellow21(sK130(sF542,sF540)))
| ~ spl543_96
| ~ spl543_117
| ~ spl543_118 ),
inference(forward_demodulation,[],[f26225,f25908]) ).
fof(f26229,plain,
( l1_orders_2(sK130(sF542,sF540))
| ~ spl543_96
| ~ spl543_98
| ~ spl543_117
| ~ spl543_118 ),
inference(forward_demodulation,[],[f26228,f25937]) ).
fof(f26230,plain,
( spl543_125
| ~ spl543_96
| ~ spl543_98
| ~ spl543_117
| ~ spl543_118 ),
inference(avatar_split_clause,[],[f26229,f26157,f26127,f25935,f25906,f26201]) ).
fof(f26235,plain,
( ! [X0] :
( ~ m1_subset_1(sK130(sF542,sF540),u1_struct_0(k5_waybel34(X0)))
| ~ v2_orders_2(sK130(sF542,sF540))
| ~ v3_orders_2(sK130(sF542,sF540))
| ~ v4_orders_2(sK130(sF542,sF540))
| ~ v1_lattice3(sK130(sF542,sF540))
| ~ v2_lattice3(sK130(sF542,sF540))
| v1_orders_2(sK130(sF542,sF540))
| v2_setfam_1(X0) )
| ~ spl543_125 ),
inference(resolution,[],[f26202,f21690]) ).
fof(f26236,plain,
( ! [X0] :
( ~ m1_subset_1(sK130(sF542,sF540),u1_struct_0(k4_waybel34(X0)))
| ~ v2_orders_2(sK130(sF542,sF540))
| ~ v3_orders_2(sK130(sF542,sF540))
| ~ v4_orders_2(sK130(sF542,sF540))
| ~ v1_lattice3(sK130(sF542,sF540))
| ~ v2_lattice3(sK130(sF542,sF540))
| v1_orders_2(sK130(sF542,sF540))
| v2_setfam_1(X0) )
| ~ spl543_125 ),
inference(resolution,[],[f26202,f21624]) ).
fof(f26239,definition,
( spl543_126
<=> v1_orders_2(sK130(sF542,sF540)) ),
introduced(definition,[new_symbols(definition,[spl543_126])],[avatar_definition]) ).
fof(f26243,definition,
( spl543_127
<=> ! [X0] :
( ~ m1_subset_1(sK130(sF542,sF540),u1_struct_0(k4_waybel34(X0)))
| v2_setfam_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl543_127])],[avatar_definition]) ).
fof(f26244,plain,
( ! [X0] :
( v2_setfam_1(X0)
| ~ m1_subset_1(sK130(sF542,sF540),u1_struct_0(k4_waybel34(X0))) )
| ~ spl543_127 ),
inference(avatar_component_clause,[],[f26243]) ).
fof(f26245,plain,
( spl543_126
| ~ spl543_124
| ~ spl543_123
| ~ spl543_122
| ~ spl543_121
| ~ spl543_120
| spl543_127
| ~ spl543_125 ),
inference(avatar_split_clause,[],[f26236,f26201,f26243,f26181,f26185,f26189,f26193,f26197,f26239]) ).
fof(f26247,definition,
( spl543_128
<=> ! [X0] :
( ~ m1_subset_1(sK130(sF542,sF540),u1_struct_0(k5_waybel34(X0)))
| v2_setfam_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl543_128])],[avatar_definition]) ).
fof(f26248,plain,
( ! [X0] :
( v2_setfam_1(X0)
| ~ m1_subset_1(sK130(sF542,sF540),u1_struct_0(k5_waybel34(X0))) )
| ~ spl543_128 ),
inference(avatar_component_clause,[],[f26247]) ).
fof(f26249,plain,
( spl543_126
| ~ spl543_124
| ~ spl543_123
| ~ spl543_122
| ~ spl543_121
| ~ spl543_120
| spl543_128
| ~ spl543_125 ),
inference(avatar_split_clause,[],[f26235,f26201,f26247,f26181,f26185,f26189,f26193,f26197,f26239]) ).
fof(f26265,plain,
( ~ m1_subset_1(sK130(sF542,sF540),sF542)
| v1_xboole_0(sF542)
| spl543_105 ),
inference(resolution,[],[f25987,f21762]) ).
fof(f26967,plain,
( ! [X0] :
( v3_struct_0(sF539)
| ~ v2_altcat_1(sF539)
| ~ v11_altcat_1(sF539)
| ~ v12_altcat_1(sF539)
| k1_yellow21(X0) = k4_yellow21(sF539,X0)
| ~ l2_altcat_1(sF539)
| ~ m1_subset_1(X0,u1_struct_0(sF539)) )
| ~ spl543_68 ),
inference(resolution,[],[f22032,f25602]) ).
fof(f26970,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF540)
| v3_struct_0(sF539)
| ~ v2_altcat_1(sF539)
| ~ v11_altcat_1(sF539)
| ~ v12_altcat_1(sF539)
| k1_yellow21(X0) = k4_yellow21(sF539,X0)
| ~ l2_altcat_1(sF539) )
| ~ spl543_68 ),
inference(forward_demodulation,[],[f26967,f25035]) ).
fof(f26976,definition,
( spl543_164
<=> ! [X0] :
( ~ m1_subset_1(X0,sF540)
| k1_yellow21(X0) = k4_yellow21(sF539,X0) ) ),
introduced(definition,[new_symbols(definition,[spl543_164])],[avatar_definition]) ).
fof(f26977,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF540)
| k1_yellow21(X0) = k4_yellow21(sF539,X0) )
| ~ spl543_164 ),
inference(avatar_component_clause,[],[f26976]) ).
fof(f26978,plain,
( ~ spl543_30
| ~ spl543_34
| ~ spl543_29
| ~ spl543_26
| spl543_3
| spl543_164
| ~ spl543_68 ),
inference(avatar_split_clause,[],[f26970,f25600,f26976,f25062,f25172,f25190,f25220,f25196]) ).
fof(f26980,plain,
( k1_yellow21(sK130(sF542,sF540)) = k4_yellow21(sF539,sK130(sF542,sF540))
| ~ spl543_118
| ~ spl543_164 ),
inference(resolution,[],[f26977,f26158]) ).
fof(f26981,plain,
( sK130(sF542,sF540) = k4_yellow21(sF539,sK130(sF542,sF540))
| ~ spl543_98
| ~ spl543_118
| ~ spl543_164 ),
inference(forward_demodulation,[],[f26980,f25937]) ).
fof(f27062,plain,
( ! [X0] :
( v3_struct_0(sF539)
| ~ v2_altcat_1(sF539)
| ~ v11_altcat_1(sF539)
| ~ v12_altcat_1(sF539)
| v3_orders_2(k4_yellow21(sF539,X0))
| ~ l2_altcat_1(sF539)
| ~ m1_subset_1(X0,u1_struct_0(sF539)) )
| ~ spl543_68 ),
inference(resolution,[],[f22038,f25602]) ).
fof(f27065,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF540)
| v3_struct_0(sF539)
| ~ v2_altcat_1(sF539)
| ~ v11_altcat_1(sF539)
| ~ v12_altcat_1(sF539)
| v3_orders_2(k4_yellow21(sF539,X0))
| ~ l2_altcat_1(sF539) )
| ~ spl543_68 ),
inference(forward_demodulation,[],[f27062,f25035]) ).
fof(f27071,definition,
( spl543_170
<=> ! [X0] :
( ~ m1_subset_1(X0,sF540)
| v3_orders_2(k4_yellow21(sF539,X0)) ) ),
introduced(definition,[new_symbols(definition,[spl543_170])],[avatar_definition]) ).
fof(f27072,plain,
( ! [X0] :
( v3_orders_2(k4_yellow21(sF539,X0))
| ~ m1_subset_1(X0,sF540) )
| ~ spl543_170 ),
inference(avatar_component_clause,[],[f27071]) ).
fof(f27073,plain,
( ~ spl543_30
| ~ spl543_34
| ~ spl543_29
| ~ spl543_26
| spl543_3
| spl543_170
| ~ spl543_68 ),
inference(avatar_split_clause,[],[f27065,f25600,f27071,f25062,f25172,f25190,f25220,f25196]) ).
fof(f27074,plain,
( v3_orders_2(sK130(sF542,sF540))
| ~ m1_subset_1(sK130(sF542,sF540),sF540)
| ~ spl543_98
| ~ spl543_118
| ~ spl543_164
| ~ spl543_170 ),
inference(superposition,[],[f27072,f26981]) ).
fof(f27076,plain,
( ~ spl543_118
| spl543_121
| ~ spl543_98
| ~ spl543_118
| ~ spl543_164
| ~ spl543_170 ),
inference(avatar_split_clause,[],[f27074,f27071,f26976,f26157,f25935,f26185,f26157]) ).
fof(f27244,definition,
( spl543_177
<=> r2_hidden(sK130(sF542,sF540),sF540) ),
introduced(definition,[new_symbols(definition,[spl543_177])],[avatar_definition]) ).
fof(f27245,plain,
( r2_hidden(sK130(sF542,sF540),sF540)
| ~ spl543_177 ),
inference(avatar_component_clause,[],[f27244]) ).
fof(f27246,plain,
( ~ r2_hidden(sK130(sF542,sF540),sF540)
| spl543_177 ),
inference(avatar_component_clause,[],[f27244]) ).
fof(f27255,plain,
( ~ m1_subset_1(sK130(sF542,sF540),sF540)
| v1_xboole_0(sF540)
| spl543_177 ),
inference(resolution,[],[f27246,f21762]) ).
fof(f27257,plain,
( spl543_38
| ~ spl543_118
| spl543_177 ),
inference(avatar_split_clause,[],[f27255,f27244,f26157,f25243]) ).
fof(f27259,plain,
( sF540 = sF542
| ~ r2_hidden(sK130(sF542,sF540),sF542)
| ~ spl543_177 ),
inference(resolution,[],[f27245,f21962]) ).
fof(f27415,plain,
( ! [X0] :
( v3_struct_0(sF539)
| ~ v2_altcat_1(sF539)
| ~ v11_altcat_1(sF539)
| ~ v12_altcat_1(sF539)
| v2_lattice3(k4_yellow21(sF539,X0))
| ~ l2_altcat_1(sF539)
| ~ m1_subset_1(X0,u1_struct_0(sF539)) )
| ~ spl543_68 ),
inference(resolution,[],[f22035,f25602]) ).
fof(f27418,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF540)
| v3_struct_0(sF539)
| ~ v2_altcat_1(sF539)
| ~ v11_altcat_1(sF539)
| ~ v12_altcat_1(sF539)
| v2_lattice3(k4_yellow21(sF539,X0))
| ~ l2_altcat_1(sF539) )
| ~ spl543_68 ),
inference(forward_demodulation,[],[f27415,f25035]) ).
fof(f27424,definition,
( spl543_197
<=> ! [X0] :
( ~ m1_subset_1(X0,sF540)
| v2_lattice3(k4_yellow21(sF539,X0)) ) ),
introduced(definition,[new_symbols(definition,[spl543_197])],[avatar_definition]) ).
fof(f27425,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF540)
| v2_lattice3(k4_yellow21(sF539,X0)) )
| ~ spl543_197 ),
inference(avatar_component_clause,[],[f27424]) ).
fof(f27426,plain,
( ~ spl543_30
| ~ spl543_34
| ~ spl543_29
| ~ spl543_26
| spl543_3
| spl543_197
| ~ spl543_68 ),
inference(avatar_split_clause,[],[f27418,f25600,f27424,f25062,f25172,f25190,f25220,f25196]) ).
fof(f27428,plain,
( v2_lattice3(k4_yellow21(sF539,sK130(sF542,sF540)))
| ~ spl543_118
| ~ spl543_197 ),
inference(resolution,[],[f27425,f26158]) ).
fof(f27433,plain,
( v2_lattice3(sK130(sF542,sF540))
| ~ spl543_98
| ~ spl543_118
| ~ spl543_164
| ~ spl543_197 ),
inference(forward_demodulation,[],[f27428,f26981]) ).
fof(f27435,plain,
( spl543_124
| ~ spl543_98
| ~ spl543_118
| ~ spl543_164
| ~ spl543_197 ),
inference(avatar_split_clause,[],[f27433,f27424,f26976,f26157,f25935,f26197]) ).
fof(f27624,plain,
( ! [X0] :
( v3_struct_0(sF539)
| ~ v2_altcat_1(sF539)
| ~ v11_altcat_1(sF539)
| ~ v12_altcat_1(sF539)
| v3_lattice3(k4_yellow21(sF539,X0))
| ~ l2_altcat_1(sF539)
| ~ m1_subset_1(X0,u1_struct_0(sF539)) )
| ~ spl543_68 ),
inference(resolution,[],[f22034,f25602]) ).
fof(f27627,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF540)
| v3_struct_0(sF539)
| ~ v2_altcat_1(sF539)
| ~ v11_altcat_1(sF539)
| ~ v12_altcat_1(sF539)
| v3_lattice3(k4_yellow21(sF539,X0))
| ~ l2_altcat_1(sF539) )
| ~ spl543_68 ),
inference(forward_demodulation,[],[f27624,f25035]) ).
fof(f27633,definition,
( spl543_206
<=> ! [X0] :
( ~ m1_subset_1(X0,sF540)
| v3_lattice3(k4_yellow21(sF539,X0)) ) ),
introduced(definition,[new_symbols(definition,[spl543_206])],[avatar_definition]) ).
fof(f27634,plain,
( ! [X0] :
( v3_lattice3(k4_yellow21(sF539,X0))
| ~ m1_subset_1(X0,sF540) )
| ~ spl543_206 ),
inference(avatar_component_clause,[],[f27633]) ).
fof(f27635,plain,
( ~ spl543_30
| ~ spl543_34
| ~ spl543_29
| ~ spl543_26
| spl543_3
| spl543_206
| ~ spl543_68 ),
inference(avatar_split_clause,[],[f27627,f25600,f27633,f25062,f25172,f25190,f25220,f25196]) ).
fof(f27637,plain,
( v3_lattice3(sK130(sF542,sF540))
| ~ m1_subset_1(sK130(sF542,sF540),sF540)
| ~ spl543_98
| ~ spl543_118
| ~ spl543_164
| ~ spl543_206 ),
inference(superposition,[],[f27634,f26981]) ).
fof(f27641,plain,
( ~ spl543_118
| spl543_119
| ~ spl543_98
| ~ spl543_118
| ~ spl543_164
| ~ spl543_206 ),
inference(avatar_split_clause,[],[f27637,f27633,f26976,f26157,f25935,f26177,f26157]) ).
fof(f27825,plain,
( ! [X0] :
( v3_struct_0(sF539)
| ~ v2_altcat_1(sF539)
| ~ v11_altcat_1(sF539)
| ~ v12_altcat_1(sF539)
| v4_orders_2(k4_yellow21(sF539,X0))
| ~ l2_altcat_1(sF539)
| ~ m1_subset_1(X0,u1_struct_0(sF539)) )
| ~ spl543_68 ),
inference(resolution,[],[f22037,f25602]) ).
fof(f27828,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF540)
| v3_struct_0(sF539)
| ~ v2_altcat_1(sF539)
| ~ v11_altcat_1(sF539)
| ~ v12_altcat_1(sF539)
| v4_orders_2(k4_yellow21(sF539,X0))
| ~ l2_altcat_1(sF539) )
| ~ spl543_68 ),
inference(forward_demodulation,[],[f27825,f25035]) ).
fof(f27884,plain,
( ! [X0] :
( v3_struct_0(sF539)
| ~ v2_altcat_1(sF539)
| ~ v11_altcat_1(sF539)
| ~ v12_altcat_1(sF539)
| v1_lattice3(k4_yellow21(sF539,X0))
| ~ l2_altcat_1(sF539)
| ~ m1_subset_1(X0,u1_struct_0(sF539)) )
| ~ spl543_68 ),
inference(resolution,[],[f22036,f25602]) ).
fof(f27887,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF540)
| v3_struct_0(sF539)
| ~ v2_altcat_1(sF539)
| ~ v11_altcat_1(sF539)
| ~ v12_altcat_1(sF539)
| v1_lattice3(k4_yellow21(sF539,X0))
| ~ l2_altcat_1(sF539) )
| ~ spl543_68 ),
inference(forward_demodulation,[],[f27884,f25035]) ).
fof(f28000,plain,
( ! [X0] :
( v3_struct_0(sF539)
| ~ v2_altcat_1(sF539)
| ~ v11_altcat_1(sF539)
| ~ v12_altcat_1(sF539)
| v2_orders_2(k4_yellow21(sF539,X0))
| ~ l2_altcat_1(sF539)
| ~ m1_subset_1(X0,u1_struct_0(sF539)) )
| ~ spl543_68 ),
inference(resolution,[],[f22039,f25602]) ).
fof(f28003,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF540)
| v3_struct_0(sF539)
| ~ v2_altcat_1(sF539)
| ~ v11_altcat_1(sF539)
| ~ v12_altcat_1(sF539)
| v2_orders_2(k4_yellow21(sF539,X0))
| ~ l2_altcat_1(sF539) )
| ~ spl543_68 ),
inference(forward_demodulation,[],[f28000,f25035]) ).
fof(f28014,definition,
( spl543_218
<=> ! [X0] :
( ~ m1_subset_1(X0,sF540)
| v4_orders_2(k4_yellow21(sF539,X0)) ) ),
introduced(definition,[new_symbols(definition,[spl543_218])],[avatar_definition]) ).
fof(f28015,plain,
( ! [X0] :
( v4_orders_2(k4_yellow21(sF539,X0))
| ~ m1_subset_1(X0,sF540) )
| ~ spl543_218 ),
inference(avatar_component_clause,[],[f28014]) ).
fof(f28016,plain,
( ~ spl543_30
| ~ spl543_34
| ~ spl543_29
| ~ spl543_26
| spl543_3
| spl543_218
| ~ spl543_68 ),
inference(avatar_split_clause,[],[f27828,f25600,f28014,f25062,f25172,f25190,f25220,f25196]) ).
fof(f28018,definition,
( spl543_219
<=> ! [X0] :
( ~ m1_subset_1(X0,sF540)
| v1_lattice3(k4_yellow21(sF539,X0)) ) ),
introduced(definition,[new_symbols(definition,[spl543_219])],[avatar_definition]) ).
fof(f28019,plain,
( ! [X0] :
( v1_lattice3(k4_yellow21(sF539,X0))
| ~ m1_subset_1(X0,sF540) )
| ~ spl543_219 ),
inference(avatar_component_clause,[],[f28018]) ).
fof(f28020,plain,
( ~ spl543_30
| ~ spl543_34
| ~ spl543_29
| ~ spl543_26
| spl543_3
| spl543_219
| ~ spl543_68 ),
inference(avatar_split_clause,[],[f27887,f25600,f28018,f25062,f25172,f25190,f25220,f25196]) ).
fof(f28022,definition,
( spl543_220
<=> ! [X0] :
( ~ m1_subset_1(X0,sF540)
| v2_orders_2(k4_yellow21(sF539,X0)) ) ),
introduced(definition,[new_symbols(definition,[spl543_220])],[avatar_definition]) ).
fof(f28023,plain,
( ! [X0] :
( v2_orders_2(k4_yellow21(sF539,X0))
| ~ m1_subset_1(X0,sF540) )
| ~ spl543_220 ),
inference(avatar_component_clause,[],[f28022]) ).
fof(f28024,plain,
( ~ spl543_30
| ~ spl543_34
| ~ spl543_29
| ~ spl543_26
| spl543_3
| spl543_220
| ~ spl543_68 ),
inference(avatar_split_clause,[],[f28003,f25600,f28022,f25062,f25172,f25190,f25220,f25196]) ).
fof(f28026,plain,
( v4_orders_2(sK130(sF542,sF540))
| ~ m1_subset_1(sK130(sF542,sF540),sF540)
| ~ spl543_98
| ~ spl543_118
| ~ spl543_164
| ~ spl543_218 ),
inference(superposition,[],[f28015,f26981]) ).
fof(f28030,plain,
( ~ spl543_118
| spl543_122
| ~ spl543_98
| ~ spl543_118
| ~ spl543_164
| ~ spl543_218 ),
inference(avatar_split_clause,[],[f28026,f28014,f26976,f26157,f25935,f26189,f26157]) ).
fof(f28032,plain,
( v1_lattice3(sK130(sF542,sF540))
| ~ m1_subset_1(sK130(sF542,sF540),sF540)
| ~ spl543_98
| ~ spl543_118
| ~ spl543_164
| ~ spl543_219 ),
inference(superposition,[],[f28019,f26981]) ).
fof(f28036,plain,
( ~ spl543_118
| spl543_123
| ~ spl543_98
| ~ spl543_118
| ~ spl543_164
| ~ spl543_219 ),
inference(avatar_split_clause,[],[f28032,f28018,f26976,f26157,f25935,f26193,f26157]) ).
fof(f28038,plain,
( v2_orders_2(sK130(sF542,sF540))
| ~ m1_subset_1(sK130(sF542,sF540),sF540)
| ~ spl543_98
| ~ spl543_118
| ~ spl543_164
| ~ spl543_220 ),
inference(superposition,[],[f28023,f26981]) ).
fof(f28042,plain,
( ~ spl543_118
| spl543_120
| ~ spl543_98
| ~ spl543_118
| ~ spl543_164
| ~ spl543_220 ),
inference(avatar_split_clause,[],[f28038,f28022,f26976,f26157,f25935,f26181,f26157]) ).
fof(f28051,plain,
( ~ m1_subset_1(sK130(sF542,sF540),u1_struct_0(k4_waybel34(sK71)))
| spl543_4
| ~ spl543_127 ),
inference(resolution,[],[f26244,f25072]) ).
fof(f28052,plain,
( ~ m1_subset_1(sK130(sF542,sF540),u1_struct_0(sF539))
| spl543_4
| ~ spl543_127 ),
inference(forward_demodulation,[],[f28051,f25033]) ).
fof(f28053,plain,
( ~ m1_subset_1(sK130(sF542,sF540),sF540)
| spl543_4
| ~ spl543_127 ),
inference(forward_demodulation,[],[f28052,f25035]) ).
fof(f28054,plain,
( ~ spl543_118
| spl543_4
| ~ spl543_127 ),
inference(avatar_split_clause,[],[f28053,f26243,f25071,f26157]) ).
fof(f28055,plain,
( ~ m1_subset_1(sK130(sF542,sF540),u1_struct_0(k5_waybel34(sK71)))
| spl543_4
| ~ spl543_128 ),
inference(resolution,[],[f26248,f25072]) ).
fof(f28056,plain,
( ~ m1_subset_1(sK130(sF542,sF540),u1_struct_0(sF541))
| spl543_4
| ~ spl543_128 ),
inference(forward_demodulation,[],[f28055,f25037]) ).
fof(f28057,plain,
( ~ m1_subset_1(sK130(sF542,sF540),sF542)
| spl543_4
| ~ spl543_128 ),
inference(forward_demodulation,[],[f28056,f25039]) ).
fof(f28062,definition,
( spl543_223
<=> r2_hidden(u1_struct_0(sK130(sF542,sF540)),sK71) ),
introduced(definition,[new_symbols(definition,[spl543_223])],[avatar_definition]) ).
fof(f28063,plain,
( ~ r2_hidden(u1_struct_0(sK130(sF542,sF540)),sK71)
| spl543_223 ),
inference(avatar_component_clause,[],[f28062]) ).
fof(f28064,plain,
( r2_hidden(u1_struct_0(sK130(sF542,sF540)),sK71)
| ~ spl543_223 ),
inference(avatar_component_clause,[],[f28062]) ).
fof(f28066,plain,
( ~ l1_orders_2(sK130(sF542,sF540))
| ~ v2_lattice3(sK130(sF542,sF540))
| ~ v1_lattice3(sK130(sF542,sF540))
| ~ v4_orders_2(sK130(sF542,sF540))
| ~ v3_orders_2(sK130(sF542,sF540))
| ~ v2_orders_2(sK130(sF542,sF540))
| m1_subset_1(sK130(sF542,sF540),sF542)
| ~ v3_lattice3(sK130(sF542,sF540))
| ~ v1_orders_2(sK130(sF542,sF540))
| ~ spl543_60
| ~ spl543_223 ),
inference(resolution,[],[f28064,f25511]) ).
fof(f28067,plain,
( ~ l1_orders_2(sK130(sF542,sF540))
| ~ v2_lattice3(sK130(sF542,sF540))
| ~ v1_lattice3(sK130(sF542,sF540))
| ~ v4_orders_2(sK130(sF542,sF540))
| ~ v3_orders_2(sK130(sF542,sF540))
| ~ v2_orders_2(sK130(sF542,sF540))
| m1_subset_1(sK130(sF542,sF540),sF540)
| ~ v3_lattice3(sK130(sF542,sF540))
| ~ v1_orders_2(sK130(sF542,sF540))
| ~ spl543_56
| ~ spl543_223 ),
inference(resolution,[],[f28064,f25450]) ).
fof(f28070,plain,
( ~ spl543_126
| ~ spl543_119
| spl543_99
| ~ spl543_120
| ~ spl543_121
| ~ spl543_122
| ~ spl543_123
| ~ spl543_124
| ~ spl543_125
| ~ spl543_60
| ~ spl543_223 ),
inference(avatar_split_clause,[],[f28066,f28062,f25510,f26201,f26197,f26193,f26189,f26185,f26181,f25939,f26177,f26239]) ).
fof(f28071,plain,
( l1_orders_2(sK130(sF542,sF540))
| ~ spl543_94
| ~ spl543_98
| ~ spl543_99
| ~ spl543_116 ),
inference(forward_demodulation,[],[f26173,f26209]) ).
fof(f28072,plain,
( spl543_36
| ~ spl543_99
| spl543_105 ),
inference(avatar_split_clause,[],[f26265,f25986,f25939,f25234]) ).
fof(f28073,plain,
( ~ spl543_99
| spl543_4
| ~ spl543_128 ),
inference(avatar_split_clause,[],[f28057,f26247,f25071,f25939]) ).
fof(f28074,plain,
( ~ spl543_105
| spl543_95
| ~ spl543_177 ),
inference(avatar_split_clause,[],[f27259,f27244,f25901,f25986]) ).
fof(f28076,plain,
( ~ spl543_126
| ~ spl543_119
| spl543_118
| ~ spl543_120
| ~ spl543_121
| ~ spl543_122
| ~ spl543_123
| ~ spl543_124
| ~ spl543_125
| ~ spl543_56
| ~ spl543_223 ),
inference(avatar_split_clause,[],[f28067,f28062,f25449,f26201,f26197,f26193,f26189,f26185,f26181,f26157,f26177,f26239]) ).
fof(f28077,plain,
( ~ l1_orders_2(sK130(sF542,sF540))
| ~ v2_lattice3(sK130(sF542,sF540))
| ~ v1_lattice3(sK130(sF542,sF540))
| ~ v4_orders_2(sK130(sF542,sF540))
| ~ v3_orders_2(sK130(sF542,sF540))
| ~ v2_orders_2(sK130(sF542,sF540))
| ~ m1_subset_1(sK130(sF542,sF540),sF542)
| ~ spl543_22
| spl543_223 ),
inference(resolution,[],[f28063,f25150]) ).
fof(f28078,plain,
( ~ l1_orders_2(sK130(sF542,sF540))
| ~ v2_lattice3(sK130(sF542,sF540))
| ~ v1_lattice3(sK130(sF542,sF540))
| ~ v4_orders_2(sK130(sF542,sF540))
| ~ v3_orders_2(sK130(sF542,sF540))
| ~ v2_orders_2(sK130(sF542,sF540))
| ~ m1_subset_1(sK130(sF542,sF540),sF540)
| ~ spl543_5
| spl543_223 ),
inference(resolution,[],[f28063,f25076]) ).
fof(f28093,plain,
( ~ spl543_118
| ~ spl543_120
| ~ spl543_121
| ~ spl543_122
| ~ spl543_123
| ~ spl543_124
| ~ spl543_125
| ~ spl543_5
| spl543_223 ),
inference(avatar_split_clause,[],[f28078,f28062,f25075,f26201,f26197,f26193,f26189,f26185,f26181,f26157]) ).
fof(f28094,plain,
( ~ spl543_99
| ~ spl543_120
| ~ spl543_121
| ~ spl543_122
| ~ spl543_123
| ~ spl543_124
| ~ spl543_125
| ~ spl543_22
| spl543_223 ),
inference(avatar_split_clause,[],[f28077,f28062,f25149,f26201,f26197,f26193,f26189,f26185,f26181,f25939]) ).
fof(f28107,plain,
( spl543_125
| ~ spl543_94
| ~ spl543_98
| ~ spl543_99
| ~ spl543_116 ),
inference(avatar_split_clause,[],[f28071,f26123,f25939,f25935,f25897,f26201]) ).
cnf(s1,plain,
( spl543_1
| ~ spl543_2 ),
inference(sat_conversion,[],[f25059]) ).
cnf(s2,plain,
( spl543_1
| ~ spl543_3 ),
inference(sat_conversion,[],[f25065]) ).
cnf(s3,plain,
~ spl543_1,
inference(sat_conversion,[],[f25067]) ).
cnf(s4,plain,
( spl543_4
| spl543_5 ),
inference(sat_conversion,[],[f25077]) ).
cnf(s7,plain,
( spl543_4
| spl543_22 ),
inference(sat_conversion,[],[f25151]) ).
cnf(s10,plain,
( spl543_1
| spl543_25 ),
inference(sat_conversion,[],[f25169]) ).
cnf(s11,plain,
( spl543_1
| spl543_26 ),
inference(sat_conversion,[],[f25175]) ).
cnf(s12,plain,
( spl543_1
| spl543_27 ),
inference(sat_conversion,[],[f25181]) ).
cnf(s13,plain,
( spl543_1
| spl543_28 ),
inference(sat_conversion,[],[f25187]) ).
cnf(s14,plain,
( spl543_1
| spl543_29 ),
inference(sat_conversion,[],[f25193]) ).
cnf(s15,plain,
( spl543_1
| spl543_30 ),
inference(sat_conversion,[],[f25199]) ).
cnf(s16,plain,
( spl543_1
| spl543_31 ),
inference(sat_conversion,[],[f25205]) ).
cnf(s17,plain,
( spl543_1
| spl543_32 ),
inference(sat_conversion,[],[f25211]) ).
cnf(s18,plain,
( spl543_1
| spl543_33 ),
inference(sat_conversion,[],[f25217]) ).
cnf(s19,plain,
( spl543_1
| spl543_34 ),
inference(sat_conversion,[],[f25223]) ).
cnf(s20,plain,
( spl543_2
| ~ spl543_35
| ~ spl543_36 ),
inference(sat_conversion,[],[f25237]) ).
cnf(s21,plain,
( spl543_3
| ~ spl543_37
| ~ spl543_38 ),
inference(sat_conversion,[],[f25246]) ).
cnf(s27,plain,
( ~ spl543_30
| spl543_37 ),
inference(sat_conversion,[],[f25316]) ).
cnf(s28,plain,
( ~ spl543_27
| spl543_35 ),
inference(sat_conversion,[],[f25318]) ).
cnf(s30,plain,
( spl543_4
| spl543_43 ),
inference(sat_conversion,[],[f25330]) ).
cnf(s32,plain,
~ spl543_4,
inference(sat_conversion,[],[f25333]) ).
cnf(s43,plain,
( spl543_4
| spl543_56 ),
inference(sat_conversion,[],[f25451]) ).
cnf(s46,plain,
( spl543_4
| spl543_59 ),
inference(sat_conversion,[],[f25485]) ).
cnf(s47,plain,
( spl543_4
| spl543_60 ),
inference(sat_conversion,[],[f25512]) ).
cnf(s55,plain,
( ~ spl543_43
| spl543_68 ),
inference(sat_conversion,[],[f25603]) ).
cnf(s58,plain,
( spl543_2
| ~ spl543_25
| ~ spl543_27
| ~ spl543_28
| ~ spl543_31
| ~ spl543_33
| spl543_71 ),
inference(sat_conversion,[],[f25682]) ).
cnf(s59,plain,
( spl543_3
| ~ spl543_26
| ~ spl543_29
| ~ spl543_30
| ~ spl543_32
| ~ spl543_34
| spl543_72 ),
inference(sat_conversion,[],[f25686]) ).
cnf(s80,plain,
( spl543_2
| ~ spl543_25
| ~ spl543_27
| ~ spl543_28
| ~ spl543_31
| ~ spl543_33
| ~ spl543_94
| spl543_98
| ~ spl543_99 ),
inference(sat_conversion,[],[f25968]) ).
cnf(s83,plain,
~ spl543_95,
inference(sat_conversion,[],[f26012]) ).
cnf(s84,plain,
( spl543_99
| ~ spl543_105 ),
inference(sat_conversion,[],[f26013]) ).
cnf(s96,plain,
( spl543_2
| ~ spl543_25
| ~ spl543_27
| ~ spl543_28
| ~ spl543_31
| ~ spl543_33
| spl543_116 ),
inference(sat_conversion,[],[f26125]) ).
cnf(s97,plain,
( spl543_3
| ~ spl543_26
| ~ spl543_29
| ~ spl543_30
| ~ spl543_32
| ~ spl543_34
| spl543_117 ),
inference(sat_conversion,[],[f26129]) ).
cnf(s98,plain,
( ~ spl543_72
| spl543_95
| spl543_96
| spl543_105 ),
inference(sat_conversion,[],[f26141]) ).
cnf(s105,plain,
( spl543_3
| ~ spl543_26
| ~ spl543_29
| ~ spl543_30
| ~ spl543_32
| ~ spl543_34
| ~ spl543_96
| spl543_98
| ~ spl543_118 ),
inference(sat_conversion,[],[f26166]) ).
cnf(s106,plain,
( spl543_95
| spl543_105
| spl543_118 ),
inference(sat_conversion,[],[f26172]) ).
cnf(s107,plain,
( ~ spl543_59
| ~ spl543_99
| spl543_119
| ~ spl543_120
| ~ spl543_121
| ~ spl543_122
| ~ spl543_123
| ~ spl543_124
| ~ spl543_125 ),
inference(sat_conversion,[],[f26204]) ).
cnf(s108,plain,
( ~ spl543_71
| spl543_94
| ~ spl543_99 ),
inference(sat_conversion,[],[f26205]) ).
cnf(s109,plain,
( spl543_2
| ~ spl543_25
| ~ spl543_27
| ~ spl543_28
| ~ spl543_31
| ~ spl543_33
| ~ spl543_94
| ~ spl543_98
| ~ spl543_99
| spl543_121 ),
inference(sat_conversion,[],[f26220]) ).
cnf(s110,plain,
( spl543_2
| ~ spl543_25
| ~ spl543_27
| ~ spl543_28
| ~ spl543_31
| ~ spl543_33
| ~ spl543_94
| ~ spl543_98
| ~ spl543_99
| spl543_124 ),
inference(sat_conversion,[],[f26221]) ).
cnf(s111,plain,
( spl543_2
| ~ spl543_25
| ~ spl543_27
| ~ spl543_28
| ~ spl543_31
| ~ spl543_33
| ~ spl543_94
| ~ spl543_98
| ~ spl543_99
| spl543_123 ),
inference(sat_conversion,[],[f26222]) ).
cnf(s112,plain,
( spl543_2
| ~ spl543_25
| ~ spl543_27
| ~ spl543_28
| ~ spl543_31
| ~ spl543_33
| ~ spl543_94
| ~ spl543_98
| ~ spl543_99
| spl543_122 ),
inference(sat_conversion,[],[f26223]) ).
cnf(s113,plain,
( spl543_2
| ~ spl543_25
| ~ spl543_27
| ~ spl543_28
| ~ spl543_31
| ~ spl543_33
| ~ spl543_94
| ~ spl543_98
| ~ spl543_99
| spl543_120 ),
inference(sat_conversion,[],[f26224]) ).
cnf(s115,plain,
( ~ spl543_96
| ~ spl543_98
| ~ spl543_117
| ~ spl543_118
| spl543_125 ),
inference(sat_conversion,[],[f26230]) ).
cnf(s117,plain,
( ~ spl543_120
| ~ spl543_121
| ~ spl543_122
| ~ spl543_123
| ~ spl543_124
| ~ spl543_125
| spl543_126
| spl543_127 ),
inference(sat_conversion,[],[f26245]) ).
cnf(s118,plain,
( ~ spl543_120
| ~ spl543_121
| ~ spl543_122
| ~ spl543_123
| ~ spl543_124
| ~ spl543_125
| spl543_126
| spl543_128 ),
inference(sat_conversion,[],[f26249]) ).
cnf(s151,plain,
( spl543_3
| ~ spl543_26
| ~ spl543_29
| ~ spl543_30
| ~ spl543_34
| ~ spl543_68
| spl543_164 ),
inference(sat_conversion,[],[f26978]) ).
cnf(s161,plain,
( spl543_3
| ~ spl543_26
| ~ spl543_29
| ~ spl543_30
| ~ spl543_34
| ~ spl543_68
| spl543_170 ),
inference(sat_conversion,[],[f27073]) ).
cnf(s162,plain,
( ~ spl543_118
| ~ spl543_98
| ~ spl543_118
| spl543_121
| ~ spl543_164
| ~ spl543_170 ),
inference(sat_conversion,[],[f27076]) ).
cnf(s163,plain,
( ~ spl543_98
| ~ spl543_118
| spl543_121
| ~ spl543_164
| ~ spl543_170 ),
inference(rat,[],[s162]) ).
cnf(s197,plain,
( spl543_38
| ~ spl543_118
| spl543_177 ),
inference(sat_conversion,[],[f27257]) ).
cnf(s216,plain,
( spl543_3
| ~ spl543_26
| ~ spl543_29
| ~ spl543_30
| ~ spl543_34
| ~ spl543_68
| spl543_197 ),
inference(sat_conversion,[],[f27426]) ).
cnf(s218,plain,
( ~ spl543_98
| ~ spl543_118
| spl543_124
| ~ spl543_164
| ~ spl543_197 ),
inference(sat_conversion,[],[f27435]) ).
cnf(s225,plain,
( spl543_3
| ~ spl543_26
| ~ spl543_29
| ~ spl543_30
| ~ spl543_34
| ~ spl543_68
| spl543_206 ),
inference(sat_conversion,[],[f27635]) ).
cnf(s228,plain,
( ~ spl543_118
| ~ spl543_98
| ~ spl543_118
| spl543_119
| ~ spl543_164
| ~ spl543_206 ),
inference(sat_conversion,[],[f27641]) ).
cnf(s229,plain,
( ~ spl543_98
| ~ spl543_118
| spl543_119
| ~ spl543_164
| ~ spl543_206 ),
inference(rat,[],[s228]) ).
cnf(s241,plain,
( spl543_3
| ~ spl543_26
| ~ spl543_29
| ~ spl543_30
| ~ spl543_34
| ~ spl543_68
| spl543_218 ),
inference(sat_conversion,[],[f28016]) ).
cnf(s242,plain,
( spl543_3
| ~ spl543_26
| ~ spl543_29
| ~ spl543_30
| ~ spl543_34
| ~ spl543_68
| spl543_219 ),
inference(sat_conversion,[],[f28020]) ).
cnf(s243,plain,
( spl543_3
| ~ spl543_26
| ~ spl543_29
| ~ spl543_30
| ~ spl543_34
| ~ spl543_68
| spl543_220 ),
inference(sat_conversion,[],[f28024]) ).
cnf(s246,plain,
( ~ spl543_118
| ~ spl543_98
| ~ spl543_118
| spl543_122
| ~ spl543_164
| ~ spl543_218 ),
inference(sat_conversion,[],[f28030]) ).
cnf(s247,plain,
( ~ spl543_98
| ~ spl543_118
| spl543_122
| ~ spl543_164
| ~ spl543_218 ),
inference(rat,[],[s246]) ).
cnf(s250,plain,
( ~ spl543_118
| ~ spl543_98
| ~ spl543_118
| spl543_123
| ~ spl543_164
| ~ spl543_219 ),
inference(sat_conversion,[],[f28036]) ).
cnf(s251,plain,
( ~ spl543_98
| ~ spl543_118
| spl543_123
| ~ spl543_164
| ~ spl543_219 ),
inference(rat,[],[s250]) ).
cnf(s254,plain,
( ~ spl543_118
| ~ spl543_98
| ~ spl543_118
| spl543_120
| ~ spl543_164
| ~ spl543_220 ),
inference(sat_conversion,[],[f28042]) ).
cnf(s255,plain,
( ~ spl543_98
| ~ spl543_118
| spl543_120
| ~ spl543_164
| ~ spl543_220 ),
inference(rat,[],[s254]) ).
cnf(s258,plain,
( spl543_4
| ~ spl543_118
| ~ spl543_127 ),
inference(sat_conversion,[],[f28054]) ).
cnf(s260,plain,
( ~ spl543_60
| spl543_99
| ~ spl543_119
| ~ spl543_120
| ~ spl543_121
| ~ spl543_122
| ~ spl543_123
| ~ spl543_124
| ~ spl543_125
| ~ spl543_126
| ~ spl543_223 ),
inference(sat_conversion,[],[f28070]) ).
cnf(s261,plain,
( spl543_36
| ~ spl543_99
| spl543_105 ),
inference(sat_conversion,[],[f28072]) ).
cnf(s262,plain,
( spl543_4
| ~ spl543_99
| ~ spl543_128 ),
inference(sat_conversion,[],[f28073]) ).
cnf(s263,plain,
( spl543_95
| ~ spl543_105
| ~ spl543_177 ),
inference(sat_conversion,[],[f28074]) ).
cnf(s265,plain,
( ~ spl543_56
| spl543_118
| ~ spl543_119
| ~ spl543_120
| ~ spl543_121
| ~ spl543_122
| ~ spl543_123
| ~ spl543_124
| ~ spl543_125
| ~ spl543_126
| ~ spl543_223 ),
inference(sat_conversion,[],[f28076]) ).
cnf(s267,plain,
( ~ spl543_5
| ~ spl543_118
| ~ spl543_120
| ~ spl543_121
| ~ spl543_122
| ~ spl543_123
| ~ spl543_124
| ~ spl543_125
| spl543_223 ),
inference(sat_conversion,[],[f28093]) ).
cnf(s268,plain,
( ~ spl543_22
| ~ spl543_99
| ~ spl543_120
| ~ spl543_121
| ~ spl543_122
| ~ spl543_123
| ~ spl543_124
| ~ spl543_125
| spl543_223 ),
inference(sat_conversion,[],[f28094]) ).
cnf(s271,plain,
( ~ spl543_94
| ~ spl543_98
| ~ spl543_99
| ~ spl543_116
| spl543_125 ),
inference(sat_conversion,[],[f28107]) ).
cnf(s276,plain,
spl543_60,
inference(rat,[],[s47,s32]) ).
cnf(s277,plain,
spl543_59,
inference(rat,[],[s46,s32]) ).
cnf(s278,plain,
spl543_56,
inference(rat,[],[s43,s32]) ).
cnf(s286,plain,
spl543_43,
inference(rat,[],[s30,s32]) ).
cnf(s289,plain,
spl543_68,
inference(rat,[],[s55,s286]) ).
cnf(s294,plain,
spl543_22,
inference(rat,[],[s7,s32]) ).
cnf(s295,plain,
spl543_5,
inference(rat,[],[s4,s32]) ).
cnf(s300,plain,
spl543_34,
inference(rat,[],[s19,s3]) ).
cnf(s301,plain,
spl543_33,
inference(rat,[],[s18,s3]) ).
cnf(s302,plain,
spl543_32,
inference(rat,[],[s17,s3]) ).
cnf(s303,plain,
spl543_31,
inference(rat,[],[s16,s3]) ).
cnf(s304,plain,
spl543_30,
inference(rat,[],[s15,s3]) ).
cnf(s305,plain,
spl543_29,
inference(rat,[],[s14,s3]) ).
cnf(s306,plain,
spl543_28,
inference(rat,[],[s13,s3]) ).
cnf(s307,plain,
spl543_27,
inference(rat,[],[s12,s3]) ).
cnf(s308,plain,
spl543_26,
inference(rat,[],[s11,s3]) ).
cnf(s309,plain,
spl543_25,
inference(rat,[],[s10,s3]) ).
cnf(s311,plain,
spl543_37,
inference(rat,[],[s27,s304]) ).
cnf(s313,plain,
spl543_35,
inference(rat,[],[s28,s307]) ).
cnf(s320,plain,
~ spl543_3,
inference(rat,[],[s2,s3]) ).
cnf(s321,plain,
spl543_220,
inference(rat,[],[s243,s308,s289,s300,s304,s305,s320]) ).
cnf(s322,plain,
spl543_219,
inference(rat,[],[s242,s308,s289,s300,s304,s305,s320]) ).
cnf(s323,plain,
spl543_218,
inference(rat,[],[s241,s308,s289,s300,s304,s305,s320]) ).
cnf(s324,plain,
spl543_206,
inference(rat,[],[s225,s308,s289,s300,s304,s305,s320]) ).
cnf(s326,plain,
spl543_197,
inference(rat,[],[s216,s308,s289,s300,s304,s305,s320]) ).
cnf(s327,plain,
spl543_170,
inference(rat,[],[s161,s308,s289,s300,s304,s305,s320]) ).
cnf(s328,plain,
spl543_164,
inference(rat,[],[s151,s308,s289,s300,s304,s305,s320]) ).
cnf(s329,plain,
spl543_117,
inference(rat,[],[s97,s308,s300,s302,s304,s305,s320]) ).
cnf(s331,plain,
spl543_72,
inference(rat,[],[s59,s308,s300,s302,s304,s305,s320]) ).
cnf(s334,plain,
~ spl543_38,
inference(rat,[],[s21,s311,s320]) ).
cnf(s335,plain,
~ spl543_2,
inference(rat,[],[s1,s3]) ).
cnf(s344,plain,
spl543_116,
inference(rat,[],[s96,s309,s301,s303,s306,s307,s335]) ).
cnf(s346,plain,
spl543_71,
inference(rat,[],[s58,s309,s301,s303,s306,s307,s335]) ).
cnf(s349,plain,
~ spl543_36,
inference(rat,[],[s20,s313,s335]) ).
cnf(s350,plain,
spl543_99,
inference(rat,[],[s117,s260,s267,s115,s163,s218,s229,s247,s251,s255,s105,s258,s98,s106,s84,s276,s295,s329,s328,s327,s326,s324,s323,s322,s321,s305,s304,s302,s300,s308,s320,s32,s83,s331]) ).
cnf(s351,plain,
~ spl543_128,
inference(rat,[],[s262,s32,s350]) ).
cnf(s352,plain,
spl543_105,
inference(rat,[],[s261,s349,s350]) ).
cnf(s353,plain,
spl543_94,
inference(rat,[],[s108,s346,s350]) ).
cnf(s354,plain,
~ spl543_177,
inference(rat,[],[s263,s83,s352]) ).
cnf(s360,plain,
spl543_98,
inference(rat,[],[s80,s350,s335,s309,s301,s303,s306,s307,s353]) ).
cnf(s361,plain,
~ spl543_118,
inference(rat,[],[s197,s334,s354]) ).
cnf(s362,plain,
spl543_125,
inference(rat,[],[s271,s350,s344,s353,s360]) ).
cnf(s363,plain,
spl543_120,
inference(rat,[],[s113,s350,s353,s335,s309,s301,s303,s306,s307,s360]) ).
cnf(s364,plain,
spl543_122,
inference(rat,[],[s112,s350,s353,s335,s309,s301,s303,s306,s307,s360]) ).
cnf(s365,plain,
spl543_123,
inference(rat,[],[s111,s350,s353,s335,s309,s301,s303,s306,s307,s360]) ).
cnf(s366,plain,
spl543_124,
inference(rat,[],[s110,s350,s353,s335,s309,s301,s303,s306,s307,s360]) ).
cnf(s367,plain,
spl543_121,
inference(rat,[],[s109,s350,s353,s335,s309,s301,s303,s306,s307,s360]) ).
cnf(s369,plain,
spl543_119,
inference(rat,[],[s107,s362,s366,s365,s364,s367,s350,s277,s363]) ).
cnf(s372,plain,
spl543_223,
inference(rat,[],[s268,s363,s362,s366,s365,s364,s350,s294,s367]) ).
cnf(s373,plain,
spl543_126,
inference(rat,[],[s118,s351,s363,s362,s366,s365,s364,s367]) ).
cnf(s376,plain,
$false,
inference(rat,[],[s265,s372,s363,s362,s366,s365,s364,s367,s361,s278,s373,s369]) ).
fof(f28108,plain,
$false,
inference(avatar_sat_refutation,[],[s376]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT360+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.39 % Computer : n001.cluster.edu
% 0.13/0.39 % Model : x86_64 x86_64
% 0.13/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.39 % Memory : 8046.5625MB
% 0.13/0.39 % OS : Linux 6.8.0-71-generic
% 0.13/0.39 % CPULimit : 300
% 0.13/0.39 % WCLimit : 300
% 0.13/0.39 % DateTime : Sun Sep 27 15:06:34 UTC 2026
% 0.13/0.40 % CPUTime :
% 0.13/0.40 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.43 Running first-order theorem proving
% 0.13/0.43 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 14.08/3.80 % (3669400)Detected formulas, will run a generic FOF schedule.
% 14.08/3.80 % (3669409)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1436714430:i=119:av=off:ss=axioms_2989 on theBenchmark for (2989ds/119Mi)
% 14.08/3.80 % (3669408)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2803541172:i=109:sd=1:ins=1:gsp=on:ss=axioms_2989 on theBenchmark for (2989ds/109Mi)
% 14.08/3.80 % (3669407)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=1242558925:i=141695:sd=1:nm=32:gsp=on:ss=included_2989 on theBenchmark for (2989ds/141695Mi)
% 14.08/3.80 % (3669405)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=674879634:i=141193_2989 on theBenchmark for (2989ds/141193Mi)
% 14.08/3.80 % (3669406)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=3665447064:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2989 on theBenchmark for (2989ds/134677Mi)
% 14.08/3.80 % (3669410)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1482829953:s2a=on:i=139:gtg=position_2989 on theBenchmark for (2989ds/139Mi)
% 14.08/3.80 % (3669411)dis-21_1_sil=8000:lcm=predicate:random_seed=124080970:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2989 on theBenchmark for (2989ds/129Mi)
% 14.08/3.80 % (3669409)Instruction limit reached!
% 14.08/3.80 % (3669409)------------------------------
% 14.08/3.80 % (3669409)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.08/3.80 % (3669409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.08/3.80 % (3669409)CaDiCaL version: 2.1.3
% 14.08/3.80 % (3669409)Termination reason: Instruction limit
% 14.08/3.80 % (3669409)Termination phase: Preprocessing 1
% 14.08/3.80 % (3669409)Time elapsed: 0.061 s
% 14.08/3.80 % (3669409)Peak memory usage: 113 MB
% 14.08/3.80 % (3669409)Instructions burned: 119 (million)
% 14.08/3.80 % (3669410)Instruction limit reached!
% 14.08/3.80 % (3669410)------------------------------
% 14.08/3.80 % (3669410)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.08/3.80 % (3669410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.08/3.80 % (3669410)CaDiCaL version: 2.1.3
% 14.08/3.80 % (3669410)Termination reason: Instruction limit
% 14.08/3.80 % (3669410)Termination phase: Property scanning
% 14.08/3.80 % (3669410)Time elapsed: 0.060 s
% 14.08/3.80 % (3669410)Peak memory usage: 112 MB
% 14.08/3.80 % (3669410)Instructions burned: 140 (million)
% 14.08/3.80 % (3669408)Instruction limit reached!
% 14.08/3.80 % (3669408)------------------------------
% 14.08/3.80 % (3669408)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.08/3.80 % (3669408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.08/3.80 % (3669408)CaDiCaL version: 2.1.3
% 14.08/3.80 % (3669408)Termination reason: Instruction limit
% 14.08/3.80 % (3669408)Termination phase: SInE selection
% 14.08/3.80 % (3669408)Time elapsed: 0.084 s
% 14.08/3.80 % (3669408)Peak memory usage: 112 MB
% 14.08/3.80 % (3669408)Instructions burned: 110 (million)
% 14.08/3.80 % (3669411)Instruction limit reached!
% 14.08/3.80 % (3669411)------------------------------
% 14.08/3.80 % (3669411)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.08/3.80 % (3669411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.08/3.80 % (3669411)CaDiCaL version: 2.1.3
% 14.08/3.80 % (3669411)Termination reason: Instruction limit
% 14.08/3.80 % (3669411)Termination phase: SInE selection
% 14.08/3.80 % (3669411)Time elapsed: 0.088 s
% 14.08/3.80 % (3669411)Peak memory usage: 112 MB
% 14.08/3.80 % (3669411)Instructions burned: 130 (million)
% 14.08/3.80 % (3669419)lrs+10_1_sil=8000:sp=occurrence:random_seed=1060689720:i=285:sd=3:ss=axioms:sgt=8_2987 on theBenchmark for (2987ds/285Mi)
% 14.08/3.80 % (3669421)lrs+1011_1_sil=32000:sp=occurrence:random_seed=658440625:i=325:sd=1:ss=axioms:sgt=32_2986 on theBenchmark for (2986ds/325Mi)
% 14.08/3.80 % (3669420)lrs+10_1_sil=32000:urr=on:br=off:random_seed=4189014127:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2986 on theBenchmark for (2986ds/157Mi)
% 14.08/3.80 % (3669419)Instruction limit reached!
% 14.08/3.80 % (3669419)------------------------------
% 14.08/3.80 % (3669419)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.08/3.80 % (3669419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.20/4.73 % (3669419)CaDiCaL version: 2.1.3
% 20.20/4.73 % (3669419)Termination reason: Instruction limit
% 20.20/4.73 % (3669419)Termination phase: Saturation
% 20.20/4.73 % (3669419)Time elapsed: 0.123 s
% 20.20/4.73 % (3669419)Peak memory usage: 119 MB
% 20.20/4.73 % (3669419)Instructions burned: 286 (million)
% 20.20/4.73 % (3669422)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=2674885287:s2a=on:i=248:s2at=1.23:gtg=position_2986 on theBenchmark for (2986ds/248Mi)
% 20.20/4.73 % (3669420)Instruction limit reached!
% 20.20/4.73 % (3669420)------------------------------
% 20.20/4.73 % (3669420)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.20/4.73 % (3669420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.20/4.73 % (3669420)CaDiCaL version: 2.1.3
% 20.20/4.73 % (3669420)Termination reason: Instruction limit
% 20.20/4.73 % (3669420)Termination phase: Property scanning
% 20.20/4.73 % (3669420)Time elapsed: 0.069 s
% 20.20/4.73 % (3669420)Peak memory usage: 112 MB
% 20.20/4.73 % (3669420)Instructions burned: 159 (million)
% 20.20/4.73 % (3669422)Instruction limit reached!
% 20.20/4.73 % (3669422)------------------------------
% 20.20/4.73 % (3669422)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.20/4.73 % (3669422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.20/4.73 % (3669422)CaDiCaL version: 2.1.3
% 20.20/4.73 % (3669422)Termination reason: Instruction limit
% 20.20/4.73 % (3669422)Termination phase: Property scanning
% 20.20/4.73 % (3669422)Time elapsed: 0.110 s
% 20.20/4.73 % (3669422)Peak memory usage: 112 MB
% 20.20/4.73 % (3669422)Instructions burned: 249 (million)
% 20.20/4.73 % (3669427)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=4239732354:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2984 on theBenchmark for (2984ds/294Mi)
% 20.20/4.73 % (3669421)Instruction limit reached!
% 20.20/4.73 % (3669421)------------------------------
% 20.20/4.73 % (3669421)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.20/4.73 % (3669421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.20/4.73 % (3669421)CaDiCaL version: 2.1.3
% 20.20/4.73 % (3669421)Termination reason: Instruction limit
% 20.20/4.73 % (3669421)Termination phase: Saturation
% 20.20/4.73 % (3669421)Time elapsed: 0.219 s
% 20.20/4.73 % (3669421)Peak memory usage: 118 MB
% 20.20/4.73 % (3669421)Instructions burned: 326 (million)
% 20.20/4.73 % (3669428)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=817756023:i=2350_2984 on theBenchmark for (2984ds/2350Mi)
% 20.20/4.73 % (3669427)Instruction limit reached!
% 20.20/4.73 % (3669427)------------------------------
% 20.20/4.73 % (3669427)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.20/4.73 % (3669427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.20/4.73 % (3669427)CaDiCaL version: 2.1.3
% 20.20/4.73 % (3669427)Termination reason: Instruction limit
% 20.20/4.73 % (3669427)Termination phase: Saturation
% 20.20/4.73 % (3669427)Time elapsed: 0.115 s
% 20.20/4.73 % (3669427)Peak memory usage: 119 MB
% 20.20/4.73 % (3669427)Instructions burned: 297 (million)
% 20.20/4.73 % (3669429)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1175765453:cts=off:i=113:fsr=off:ss=included:sgt=4_2983 on theBenchmark for (2983ds/113Mi)
% 20.20/4.73 % (3669431)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=326690318:i=127:av=off:fsr=off:sup=off_2982 on theBenchmark for (2982ds/127Mi)
% 20.20/4.73 % (3669433)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=521335027:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2982 on theBenchmark for (2982ds/114Mi)
% 20.20/4.73 % (3669429)Instruction limit reached!
% 20.20/4.73 % (3669429)------------------------------
% 20.20/4.73 % (3669429)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.20/4.73 % (3669429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.20/4.73 % (3669429)CaDiCaL version: 2.1.3
% 20.20/4.73 % (3669429)Termination reason: Instruction limit
% 20.20/4.73 % (3669429)Termination phase: SInE selection
% 20.20/4.73 % (3669429)Time elapsed: 0.094 s
% 20.20/4.73 % (3669429)Peak memory usage: 112 MB
% 20.20/4.73 % (3669429)Instructions burned: 114 (million)
% 20.20/4.73 % (3669433)Instruction limit reached!
% 20.20/4.73 % (3669433)------------------------------
% 20.20/4.73 % (3669433)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.99/9.47 % (3669433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.99/9.47 % (3669433)CaDiCaL version: 2.1.3
% 53.99/9.47 % (3669433)Termination reason: Instruction limit
% 53.99/9.47 % (3669433)Termination phase: Property scanning
% 53.99/9.47 % (3669433)Time elapsed: 0.027 s
% 53.99/9.47 % (3669433)Peak memory usage: 112 MB
% 53.99/9.47 % (3669433)Instructions burned: 116 (million)
% 53.99/9.47 % (3669431)Instruction limit reached!
% 53.99/9.47 % (3669431)------------------------------
% 53.99/9.47 % (3669431)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.99/9.47 % (3669431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.99/9.47 % (3669431)CaDiCaL version: 2.1.3
% 53.99/9.47 % (3669431)Termination reason: Instruction limit
% 53.99/9.47 % (3669431)Termination phase: Preprocessing 1
% 53.99/9.47 % (3669431)Time elapsed: 0.092 s
% 53.99/9.47 % (3669431)Peak memory usage: 113 MB
% 53.99/9.47 % (3669431)Instructions burned: 128 (million)
% 53.99/9.47 % (3669438)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2602856066:i=437:sd=1:aac=none:ss=included_2980 on theBenchmark for (2980ds/437Mi)
% 53.99/9.47 % (3669437)lrs+10_1_sil=8000:sp=occurrence:random_seed=1049972067:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2980 on theBenchmark for (2980ds/907Mi)
% 53.99/9.47 % (3669439)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1757421903:i=5202:ss=axioms:sgt=16_2980 on theBenchmark for (2980ds/5202Mi)
% 53.99/9.47 % (3669438)Instruction limit reached!
% 53.99/9.47 % (3669438)------------------------------
% 53.99/9.47 % (3669438)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.99/9.47 % (3669438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.99/9.47 % (3669438)CaDiCaL version: 2.1.3
% 53.99/9.47 % (3669438)Termination reason: Instruction limit
% 53.99/9.47 % (3669438)Termination phase: Saturation
% 53.99/9.47 % (3669438)Time elapsed: 0.155 s
% 53.99/9.47 % (3669438)Peak memory usage: 119 MB
% 53.99/9.47 % (3669438)Instructions burned: 438 (million)
% 53.99/9.47 % (3669443)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=4058948816:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2978 on theBenchmark for (2978ds/134Mi)
% 53.99/9.47 % (3669443)Instruction limit reached!
% 53.99/9.47 % (3669443)------------------------------
% 53.99/9.47 % (3669443)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.99/9.47 % (3669443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.99/9.47 % (3669443)CaDiCaL version: 2.1.3
% 53.99/9.47 % (3669443)Termination reason: Instruction limit
% 53.99/9.47 % (3669443)Termination phase: NewCNF
% 53.99/9.47 % (3669443)Time elapsed: 0.068 s
% 53.99/9.47 % (3669443)Peak memory usage: 115 MB
% 53.99/9.47 % (3669443)Instructions burned: 135 (million)
% 53.99/9.47 % (3669445)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3724929753:st=8:i=592:sd=3:ep=RST:ss=axioms_2976 on theBenchmark for (2976ds/592Mi)
% 53.99/9.47 % (3669437)Instruction limit reached!
% 53.99/9.47 % (3669437)------------------------------
% 53.99/9.47 % (3669437)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.99/9.47 % (3669437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.99/9.47 % (3669437)CaDiCaL version: 2.1.3
% 53.99/9.47 % (3669437)Termination reason: Instruction limit
% 53.99/9.47 % (3669437)Termination phase: Property scanning
% 53.99/9.47 % (3669437)Time elapsed: 0.545 s
% 53.99/9.47 % (3669437)Peak memory usage: 133 MB
% 53.99/9.47 % (3669437)Instructions burned: 907 (million)
% 53.99/9.47 % (3669445)Instruction limit reached!
% 53.99/9.47 % (3669445)------------------------------
% 53.99/9.47 % (3669445)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.99/9.47 % (3669445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.99/9.47 % (3669445)CaDiCaL version: 2.1.3
% 53.99/9.47 % (3669445)Termination reason: Instruction limit
% 53.99/9.47 % (3669445)Termination phase: Property scanning
% 53.99/9.47 % (3669445)Time elapsed: 0.259 s
% 53.99/9.47 % (3669445)Peak memory usage: 135 MB
% 53.99/9.47 % (3669445)Instructions burned: 592 (million)
% 53.99/9.47 % (3669447)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=4040190564:st=3:i=13193:sd=3:ss=axioms_2973 on theBenchmark for (2973ds/13193Mi)
% 53.99/9.47 % (3669449)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=3523287909:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2972 on theBenchmark for (2972ds/125Mi)
% 93.05/14.91 % (3669449)Instruction limit reached!
% 93.05/14.91 % (3669449)------------------------------
% 93.05/14.91 % (3669449)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 93.05/14.91 % (3669449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.05/14.91 % (3669449)CaDiCaL version: 2.1.3
% 93.05/14.91 % (3669449)Termination reason: Instruction limit
% 93.05/14.91 % (3669449)Termination phase: Property scanning
% 93.05/14.91 % (3669449)Time elapsed: 0.031 s
% 93.05/14.91 % (3669449)Peak memory usage: 112 MB
% 93.05/14.91 % (3669449)Instructions burned: 128 (million)
% 93.05/14.91 % (3669428)Instruction limit reached!
% 93.05/14.91 % (3669428)------------------------------
% 93.05/14.91 % (3669428)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 93.05/14.91 % (3669428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.05/14.91 % (3669428)CaDiCaL version: 2.1.3
% 93.05/14.91 % (3669428)Termination reason: Instruction limit
% 93.05/14.91 % (3669428)Termination phase: Property scanning
% 93.05/14.91 % (3669428)Time elapsed: 1.258 s
% 93.05/14.91 % (3669428)Peak memory usage: 170 MB
% 93.05/14.91 % (3669428)Instructions burned: 2352 (million)
% 93.05/14.91 % (3669451)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2622059269:i=134:gtgl=5:slsql=off:gtg=exists_sym_2970 on theBenchmark for (2970ds/134Mi)
% 93.05/14.91 % (3669451)Instruction limit reached!
% 93.05/14.91 % (3669451)------------------------------
% 93.05/14.91 % (3669451)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 93.05/14.91 % (3669451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.05/14.91 % (3669451)CaDiCaL version: 2.1.3
% 93.05/14.91 % (3669451)Termination reason: Instruction limit
% 93.05/14.91 % (3669451)Termination phase: Property scanning
% 93.05/14.91 % (3669451)Time elapsed: 0.033 s
% 93.05/14.91 % (3669451)Peak memory usage: 112 MB
% 93.05/14.91 % (3669451)Instructions burned: 139 (million)
% 93.05/14.91 % (3669452)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=848997242:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2970 on theBenchmark for (2970ds/141Mi)
% 93.05/14.91 % (3669454)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3472863813:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2968 on theBenchmark for (2968ds/431Mi)
% 93.05/14.91 % (3669452)Refutation not found, incomplete strategy
% 93.05/14.91 % (3669452)------------------------------
% 93.05/14.91 % (3669452)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 93.05/14.91 % (3669452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.05/14.91 % (3669452)CaDiCaL version: 2.1.3
% 93.05/14.91 % (3669452)Termination reason: Refutation not found, incomplete strategy
% 93.05/14.91 % (3669452)Time elapsed: 0.118 s
% 93.05/14.91 % (3669452)Peak memory usage: 117 MB
% 93.05/14.91 % (3669452)Instructions burned: 137 (million)
% 93.05/14.91 % (3669454)Instruction limit reached!
% 93.05/14.91 % (3669454)------------------------------
% 93.05/14.91 % (3669454)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 93.05/14.91 % (3669454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.05/14.91 % (3669454)CaDiCaL version: 2.1.3
% 93.05/14.91 % (3669454)Termination reason: Instruction limit
% 93.05/14.91 % (3669454)Termination phase: Saturation
% 93.05/14.91 % (3669454)Time elapsed: 0.158 s
% 93.05/14.91 % (3669454)Peak memory usage: 119 MB
% 93.05/14.91 % (3669454)Instructions burned: 433 (million)
% 93.05/14.91 % (3669452)------------------------------
% 93.05/14.91 % (3669452)------------------------------
% 93.05/14.91 % (3669457)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=4191827370:i=6060:aac=none:ins=25_2965 on theBenchmark for (2965ds/6060Mi)
% 93.05/14.91 % (3669458)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=684452019:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2964 on theBenchmark for (2964ds/150Mi)
% 93.05/14.91 % (3669458)Instruction limit reached!
% 93.05/14.91 % (3669458)------------------------------
% 93.05/14.91 % (3669458)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 93.05/14.91 % (3669458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 104.61/16.77 % (3669458)CaDiCaL version: 2.1.3
% 104.61/16.77 % (3669458)Termination reason: Instruction limit
% 104.61/16.77 % (3669458)Termination phase: Preprocessing 1
% 104.61/16.77 % (3669458)Time elapsed: 0.128 s
% 104.61/16.77 % (3669458)Peak memory usage: 113 MB
% 104.61/16.77 % (3669458)Instructions burned: 150 (million)
% 104.61/16.77 % (3669461)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=329454730:i=14155:bd=all_2961 on theBenchmark for (2961ds/14155Mi)
% 104.61/16.77 % (3669439)Instruction limit reached!
% 104.61/16.77 % (3669439)------------------------------
% 104.61/16.77 % (3669439)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 104.61/16.77 % (3669439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 104.61/16.77 % (3669439)CaDiCaL version: 2.1.3
% 104.61/16.77 % (3669439)Termination reason: Instruction limit
% 104.61/16.77 % (3669439)Termination phase: Saturation
% 104.61/16.77 % (3669439)Time elapsed: 4.005 s
% 104.61/16.77 % (3669439)Peak memory usage: 519 MB
% 104.61/16.77 % (3669439)Instructions burned: 5203 (million)
% 104.61/16.77 % (3669457)Instruction limit reached!
% 104.61/16.77 % (3669457)------------------------------
% 104.61/16.77 % (3669457)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 104.61/16.77 % (3669457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 104.61/16.77 % (3669457)CaDiCaL version: 2.1.3
% 104.61/16.77 % (3669457)Termination reason: Instruction limit
% 104.61/16.77 % (3669457)Termination phase: Saturation
% 104.61/16.77 % (3669457)Time elapsed: 2.768 s
% 104.61/16.77 % (3669457)Peak memory usage: 613 MB
% 104.61/16.77 % (3669457)Instructions burned: 6066 (million)
% 104.61/16.77 % (3669463)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2790401862:i=667:av=off:fsr=off_2938 on theBenchmark for (2938ds/667Mi)
% 104.61/16.77 % (3669464)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=2954283945:s2a=on:i=185:s2at=1.8:fdi=4_2936 on theBenchmark for (2936ds/185Mi)
% 104.61/16.77 % (3669464)Instruction limit reached!
% 104.61/16.77 % (3669464)------------------------------
% 104.61/16.77 % (3669464)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 104.61/16.77 % (3669464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 104.61/16.77 % (3669464)CaDiCaL version: 2.1.3
% 104.61/16.77 % (3669464)Termination reason: Instruction limit
% 104.61/16.77 % (3669464)Termination phase: SInE selection
% 104.61/16.77 % (3669464)Time elapsed: 0.089 s
% 104.61/16.77 % (3669464)Peak memory usage: 112 MB
% 104.61/16.77 % (3669464)Instructions burned: 186 (million)
% 104.61/16.77 % (3669467)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=751732195:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2934 on theBenchmark for (2934ds/193Mi)
% 104.61/16.77 % (3669467)Instruction limit reached!
% 104.61/16.77 % (3669467)------------------------------
% 104.61/16.77 % (3669467)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 104.61/16.77 % (3669467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 104.61/16.77 % (3669467)CaDiCaL version: 2.1.3
% 104.61/16.77 % (3669467)Termination reason: Instruction limit
% 104.61/16.77 % (3669467)Termination phase: SInE selection
% 104.61/16.77 % (3669467)Time elapsed: 0.093 s
% 104.61/16.77 % (3669467)Peak memory usage: 112 MB
% 104.61/16.77 % (3669467)Instructions burned: 195 (million)
% 104.61/16.77 % (3669463)Instruction limit reached!
% 104.61/16.77 % (3669463)------------------------------
% 104.61/16.77 % (3669463)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 104.61/16.77 % (3669463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 104.61/16.77 % (3669463)CaDiCaL version: 2.1.3
% 104.61/16.77 % (3669463)Termination reason: Instruction limit
% 104.61/16.77 % (3669463)Termination phase: NewCNF
% 104.61/16.77 % (3669463)Time elapsed: 0.519 s
% 104.61/16.77 % (3669463)Peak memory usage: 148 MB
% 104.61/16.77 % (3669463)Instructions burned: 669 (million)
% 104.61/16.77 % (3669469)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=2269885571:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2931 on theBenchmark for (2931ds/4850Mi)
% 104.61/16.77 % (3669470)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=1035225562:i=12111:sd=1:ss=included_2931 on theBenchmark for (2931ds/12111Mi)
% 104.61/16.77 % (3669469)Instruction limit reached!
% 104.61/16.77 % (3669469)------------------------------
% 104.61/16.77 % (3669469)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.99/18.56 % (3669469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.99/18.56 % (3669469)CaDiCaL version: 2.1.3
% 59.99/18.56 % (3669469)Termination reason: Instruction limit
% 59.99/18.56 % (3669469)Termination phase: Saturation
% 59.99/18.56 % (3669469)Time elapsed: 1.582 s
% 59.99/18.56 % (3669469)Peak memory usage: 217 MB
% 59.99/18.56 % (3669469)Instructions burned: 4944 (million)
% 59.99/18.56 % (3669473)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2583443003:i=319:kws=precedence:fsr=off_2913 on theBenchmark for (2913ds/319Mi)
% 59.99/18.56 % (3669473)Instruction limit reached!
% 59.99/18.56 % (3669473)------------------------------
% 59.99/18.56 % (3669473)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.99/18.56 % (3669473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.99/18.56 % (3669473)CaDiCaL version: 2.1.3
% 59.99/18.56 % (3669473)Termination reason: Instruction limit
% 59.99/18.56 % (3669473)Termination phase: Naming
% 59.99/18.56 % (3669473)Time elapsed: 0.154 s
% 59.99/18.56 % (3669473)Peak memory usage: 135 MB
% 59.99/18.56 % (3669473)Instructions burned: 321 (million)
% 59.99/18.56 % (3669475)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=2438370724:i=2064:ep=RST_2911 on theBenchmark for (2911ds/2064Mi)
% 59.99/18.56 % (3669475)Instruction limit reached!
% 59.99/18.56 % (3669475)------------------------------
% 59.99/18.56 % (3669475)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.99/18.56 % (3669475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.99/18.56 % (3669475)CaDiCaL version: 2.1.3
% 59.99/18.56 % (3669475)Termination reason: Instruction limit
% 59.99/18.56 % (3669475)Termination phase: Property scanning
% 59.99/18.56 % (3669475)Time elapsed: 0.635 s
% 59.99/18.56 % (3669475)Peak memory usage: 170 MB
% 59.99/18.56 % (3669475)Instructions burned: 2068 (million)
% 59.99/18.56 % (3669477)dis-1011_128_sil=32000:random_seed=3871957159:i=3706:ep=RST:av=off_2903 on theBenchmark for (2903ds/3706Mi)
% 59.99/18.56 % (3669447)Instruction limit reached!
% 59.99/18.56 % (3669447)------------------------------
% 59.99/18.56 % (3669447)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.99/18.56 % (3669447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.99/18.56 % (3669447)CaDiCaL version: 2.1.3
% 59.99/18.56 % (3669447)Termination reason: Instruction limit
% 59.99/18.56 % (3669447)Termination phase: Saturation
% 59.99/18.56 % (3669447)Time elapsed: 7.346 s
% 59.99/18.56 % (3669447)Peak memory usage: 275 MB
% 59.99/18.56 % (3669447)Instructions burned: 13193 (million)
% 59.99/18.56 % (3669479)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=1051392146:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2898 on theBenchmark for (2898ds/757Mi)
% 59.99/18.56 % (3669479)Refutation not found, incomplete strategy
% 59.99/18.56 % (3669479)------------------------------
% 59.99/18.56 % (3669479)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.99/18.56 % (3669479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.99/18.56 % (3669479)CaDiCaL version: 2.1.3
% 59.99/18.56 % (3669479)Termination reason: Refutation not found, incomplete strategy
% 59.99/18.56 % (3669479)Time elapsed: 0.199 s
% 59.99/18.56 % (3669479)Peak memory usage: 120 MB
% 59.99/18.56 % (3669479)Instructions burned: 298 (million)
% 59.99/18.56 % (3669479)------------------------------
% 59.99/18.56 % (3669479)------------------------------
% 59.99/18.56 % (3669477)Instruction limit reached!
% 59.99/18.56 % (3669477)------------------------------
% 59.99/18.56 % (3669477)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.99/18.56 % (3669477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.99/18.56 % (3669477)CaDiCaL version: 2.1.3
% 59.99/18.56 % (3669477)Termination reason: Instruction limit
% 59.99/18.56 % (3669477)Termination phase: Saturation
% 59.99/18.56 % (3669477)Time elapsed: 1.071 s
% 59.99/18.56 % (3669477)Peak memory usage: 186 MB
% 59.99/18.56 % (3669477)Instructions burned: 3709 (million)
% 59.99/18.56 % (3669481)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2499877550:i=13913:ss=axioms:sgt=8_2892 on theBenchmark for (2892ds/13913Mi)
% 59.99/18.56 % (3669482)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=2782960855:i=9925:aac=none_2891 on theBenchmark for (2891ds/9925Mi)
% 59.99/18.56 % (3669461)Instruction limit reached!
% 59.99/18.56 % (3669461)------------------------------
% 59.99/18.56 % (3669461)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.99/18.56 % (3669461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.99/18.56 % (3669461)CaDiCaL version: 2.1.3
% 59.99/18.56 % (3669461)Termination reason: Instruction limit
% 59.99/18.56 % (3669461)Termination phase: Saturation
% 59.99/18.56 % (3669461)Time elapsed: 10.013 s
% 59.99/18.56 % (3669461)Peak memory usage: 784 MB
% 59.99/18.56 % (3669461)Instructions burned: 14155 (million)
% 59.99/18.56 % (3669485)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=1917406051:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2858 on theBenchmark for (2858ds/2479Mi)
% 59.99/18.56 % (3669485)Refutation not found, incomplete strategy
% 59.99/18.56 % (3669485)------------------------------
% 59.99/18.56 % (3669485)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.99/18.56 % (3669485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.99/18.56 % (3669485)CaDiCaL version: 2.1.3
% 59.99/18.56 % (3669485)Termination reason: Refutation not found, incomplete strategy
% 59.99/18.56 % (3669485)Time elapsed: 0.232 s
% 59.99/18.56 % (3669485)Peak memory usage: 118 MB
% 59.99/18.56 % (3669485)Instructions burned: 279 (million)
% 59.99/18.56 % (3669485)------------------------------
% 59.99/18.56 % (3669485)------------------------------
% 59.99/18.56 % (3669487)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=347926130:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2852 on theBenchmark for (2852ds/440Mi)
% 59.99/18.56 % (3669487)Instruction limit reached!
% 59.99/18.56 % (3669487)------------------------------
% 59.99/18.56 % (3669487)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.99/18.56 % (3669487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.99/18.56 % (3669487)CaDiCaL version: 2.1.3
% 59.99/18.56 % (3669487)Termination reason: Instruction limit
% 59.99/18.56 % (3669487)Termination phase: Property scanning
% 59.99/18.56 % (3669487)Time elapsed: 0.198 s
% 59.99/18.56 % (3669487)Peak memory usage: 112 MB
% 59.99/18.56 % (3669487)Instructions burned: 441 (million)
% 59.99/18.56 % (3669489)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=4208824236:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2848 on theBenchmark for (2848ds/11145Mi)
% 59.99/18.56 % (3669470)Instruction limit reached!
% 59.99/18.56 % (3669470)------------------------------
% 59.99/18.56 % (3669470)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.99/18.56 % (3669470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.99/18.56 % (3669470)CaDiCaL version: 2.1.3
% 59.99/18.56 % (3669470)Termination reason: Instruction limit
% 59.99/18.56 % (3669470)Termination phase: Saturation
% 59.99/18.56 % (3669470)Time elapsed: 8.394 s
% 59.99/18.56 % (3669470)Peak memory usage: 246 MB
% 59.99/18.56 % (3669470)Instructions burned: 12111 (million)
% 59.99/18.56 % (3669482)Instruction limit reached!
% 59.99/18.56 % (3669482)------------------------------
% 59.99/18.56 % (3669482)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.99/18.56 % (3669482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.99/18.56 % (3669482)CaDiCaL version: 2.1.3
% 59.99/18.56 % (3669482)Termination reason: Instruction limit
% 59.99/18.56 % (3669482)Termination phase: Saturation
% 59.99/18.56 % (3669482)Time elapsed: 4.478 s
% 59.99/18.56 % (3669482)Peak memory usage: 709 MB
% 59.99/18.56 % (3669482)Instructions burned: 9927 (million)
% 59.99/18.56 % (3669492)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=3312563583:st=2:s2a=on:i=524:s2at=2:ss=axioms_2844 on theBenchmark for (2844ds/524Mi)
% 59.99/18.56 % (3669491)lrs+1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_frequency:lcm=reverse:urr=on:bsr=on:random_seed=2106667566:cts=off:i=3034:av=off:er=known:fsd=on_2844 on theBenchmark for (2844ds/3034Mi)
% 59.99/18.56 % (3669492)Instruction limit reached!
% 59.99/18.56 % (3669492)------------------------------
% 59.99/18.56 % (3669492)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.99/18.56 % (3669492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.99/18.56 % (3669492)CaDiCaL version: 2.1.3
% 59.99/18.56 % (3669492)Termination reason: Instruction limit
% 59.99/18.56 % (3669492)Termination phase: Preprocessing 1
% 59.99/18.56 % (3669492)Time elapsed: 0.231 s
% 59.99/18.56 % (3669492)Peak memory usage: 114 MB
% 59.99/18.56 % (3669492)Instructions burned: 527 (million)
% 59.99/18.56 % (3669495)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=2319927323:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2841 on theBenchmark for (2841ds/1016Mi)
% 59.99/18.56 % (3669495)Instruction limit reached!
% 59.99/18.56 % (3669495)------------------------------
% 59.99/18.56 % (3669495)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.99/18.56 % (3669495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.99/18.56 % (3669495)CaDiCaL version: 2.1.3
% 59.99/18.56 % (3669495)Termination reason: Instruction limit
% 59.99/18.56 % (3669495)Termination phase: Saturation
% 59.99/18.56 % (3669495)Time elapsed: 0.314 s
% 59.99/18.56 % (3669495)Peak memory usage: 123 MB
% 59.99/18.56 % (3669495)Instructions burned: 1019 (million)
% 59.99/18.56 % (3669497)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=2254931252:i=14123:bd=preordered:ins=4_2836 on theBenchmark for (2836ds/14123Mi)
% 59.99/18.56 % (3669489)First to succeed.
% 59.99/18.56 % (3669491)Instruction limit reached!
% 59.99/18.56 % (3669491)------------------------------
% 59.99/18.56 % (3669491)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.99/18.56 % (3669491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.99/18.56 % (3669491)CaDiCaL version: 2.1.3
% 59.99/18.56 % (3669491)Termination reason: Instruction limit
% 59.99/18.56 % (3669491)Termination phase: Saturation
% 59.99/18.56 % (3669491)Time elapsed: 1.645 s
% 59.99/18.56 % (3669491)Peak memory usage: 190 MB
% 59.99/18.56 % (3669491)Instructions burned: 3034 (million)
% 59.99/18.56 % (3669489)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3669400"
% 59.99/18.56 % (3669499)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=1601838623:i=5781:kws=precedence:bd=all:rawr=on_2826 on theBenchmark for (2826ds/5781Mi)
% 59.99/18.56 % (3669489)Refutation found. Thanks to Tanya!
% 59.99/18.56 % SZS status Theorem for theBenchmark
% 59.99/18.56 % SZS output start Proof for theBenchmark
% See solution above
% 118.73/18.65 % (3669489)------------------------------
% 118.73/18.65 % (3669489)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 118.73/18.65 % (3669489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.73/18.65 % (3669489)CaDiCaL version: 2.1.3
% 118.73/18.65 % (3669489)Termination reason: Refutation
% 118.73/18.65 % (3669489)Time elapsed: 1.985 s
% 118.73/18.65 % (3669489)Peak memory usage: 208 MB
% 118.73/18.65 % (3669489)Instructions burned: 2988 (million)
% 118.73/18.65 % (3669489)------------------------------
% 118.73/18.65 % (3669489)------------------------------
% 118.73/18.65 % (3669400)Success in time 17.671 s
% 118.73/18.65 % Vampire exiting
%------------------------------------------------------------------------------