%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT360+2 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n015.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 44.21s 16.07s
% Output : Refutation 105.08s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 81
% Syntax : Number of formulae : 513 ( 56 unt; 62 def)
% Number of atoms : 2588 ( 55 equ)
% Maximal formula atoms : 18 ( 5 avg)
% Number of connectives : 3634 (1559 ~;1755 |; 226 &)
% ( 69 <=>; 24 =>; 0 <=; 1 <~>)
% Maximal formula depth : 20 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 88 ( 86 usr; 57 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 5 con; 0-2 aty)
% Number of variables : 224 ( 0 sgn 221 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X0,X1] :
( ! [X2] :
( r2_hidden(X2,X0)
<=> r2_hidden(X2,X1) )
=> X0 = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2_tarski) ).
fof(f343,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/sandbox/benchmark/theBenchmark.p',d2_subset_1) ).
fof(f451,axiom,
! [X0] :
( ~ v2_setfam_1(X0)
=> ~ v1_xboole_0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc2_setfam_1) ).
fof(f538,axiom,
! [X0,X1] :
( r2_hidden(X0,X1)
=> m1_subset_1(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_subset) ).
fof(f4588,axiom,
! [X0] :
( l1_struct_0(X0)
=> ( v3_struct_0(X0)
<=> v1_xboole_0(u1_struct_0(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d1_struct_0) ).
fof(f7442,axiom,
! [X0] :
( l1_altcat_1(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l1_altcat_1) ).
fof(f7444,axiom,
! [X0] :
( l2_altcat_1(X0)
=> l1_altcat_1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l2_altcat_1) ).
fof(f10269,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/sandbox/benchmark/theBenchmark.p',d6_yellow21) ).
fof(f10306,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/sandbox/benchmark/theBenchmark.p',dt_k3_yellow21) ).
fof(f10307,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/sandbox/benchmark/theBenchmark.p',redefinition_k3_yellow21) ).
fof(f10308,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/sandbox/benchmark/theBenchmark.p',dt_k4_yellow21) ).
fof(f10309,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/sandbox/benchmark/theBenchmark.p',redefinition_k4_yellow21) ).
fof(f10317,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/sandbox/benchmark/theBenchmark.p',dt_k4_waybel34) ).
fof(f10318,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/sandbox/benchmark/theBenchmark.p',dt_k5_waybel34) ).
fof(f10351,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/sandbox/benchmark/theBenchmark.p',fc5_waybel34) ).
fof(f10352,axiom,
! [X0] :
( ~ v2_setfam_1(X0)
=> ( ~ v3_struct_0(k5_waybel34(X0))
& v2_altcat_1(k5_waybel34(X0))
& v6_altcat_1(k5_waybel34(X0))
& v9_altcat_1(k5_waybel34(X0))
& v11_altcat_1(k5_waybel34(X0))
& v12_altcat_1(k5_waybel34(X0))
& v1_altcat_2(k5_waybel34(X0))
& v2_yellow18(k5_waybel34(X0))
& v3_yellow18(k5_waybel34(X0))
& v4_yellow18(k5_waybel34(X0))
& v1_yellow21(k5_waybel34(X0))
& v2_yellow21(k5_waybel34(X0))
& v3_yellow21(k5_waybel34(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc6_waybel34) ).
fof(f10353,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/sandbox/benchmark/theBenchmark.p',t13_waybel34) ).
fof(f10355,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/sandbox/benchmark/theBenchmark.p',t15_waybel34) ).
fof(f10357,conjecture,
! [X0] :
( ~ v2_setfam_1(X0)
=> u1_struct_0(k4_waybel34(X0)) = u1_struct_0(k5_waybel34(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t17_waybel34) ).
fof(f10358,negated_conjecture,
~ ! [X0] :
( ~ v2_setfam_1(X0)
=> u1_struct_0(k4_waybel34(X0)) = u1_struct_0(k5_waybel34(X0)) ),
inference(negated_conjecture,[status(cth)],[f10357]) ).
fof(f10405,plain,
? [X0] :
( u1_struct_0(k4_waybel34(X0)) != u1_struct_0(k5_waybel34(X0))
& ~ v2_setfam_1(X0) ),
inference(ennf_transformation,[],[f10358]) ).
fof(f10408,plain,
! [X0] :
( ~ v1_xboole_0(X0)
| v2_setfam_1(X0) ),
inference(ennf_transformation,[],[f451]) ).
fof(f10410,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,[],[f10353]) ).
fof(f10411,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,[],[f10410]) ).
fof(f10412,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,[],[f10351]) ).
fof(f10417,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,[],[f10317]) ).
fof(f10419,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,[],[f10355]) ).
fof(f10420,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,[],[f10419]) ).
fof(f10421,plain,
! [X0] :
( ( ~ v3_struct_0(k5_waybel34(X0))
& v2_altcat_1(k5_waybel34(X0))
& v6_altcat_1(k5_waybel34(X0))
& v9_altcat_1(k5_waybel34(X0))
& v11_altcat_1(k5_waybel34(X0))
& v12_altcat_1(k5_waybel34(X0))
& v1_altcat_2(k5_waybel34(X0))
& v2_yellow18(k5_waybel34(X0))
& v3_yellow18(k5_waybel34(X0))
& v4_yellow18(k5_waybel34(X0))
& v1_yellow21(k5_waybel34(X0))
& v2_yellow21(k5_waybel34(X0))
& v3_yellow21(k5_waybel34(X0)) )
| v2_setfam_1(X0) ),
inference(ennf_transformation,[],[f10352]) ).
fof(f10426,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,[],[f10318]) ).
fof(f10436,plain,
! [X0,X1] :
( m1_subset_1(X0,X1)
| ~ r2_hidden(X0,X1) ),
inference(ennf_transformation,[],[f538]) ).
fof(f10443,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,[],[f343]) ).
fof(f10446,plain,
! [X0,X1] :
( X0 = X1
| ? [X2] :
( r2_hidden(X2,X0)
<~> r2_hidden(X2,X1) ) ),
inference(ennf_transformation,[],[f3]) ).
fof(f10484,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,[],[f10309]) ).
fof(f10485,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,[],[f10484]) ).
fof(f10486,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,[],[f10308]) ).
fof(f10487,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,[],[f10486]) ).
fof(f10604,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,[],[f10306]) ).
fof(f10605,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,[],[f10604]) ).
fof(f10606,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,[],[f10269]) ).
fof(f10607,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,[],[f10606]) ).
fof(f10796,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,[],[f10307]) ).
fof(f10797,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,[],[f10796]) ).
fof(f11132,plain,
! [X0] :
( l1_altcat_1(X0)
| ~ l2_altcat_1(X0) ),
inference(ennf_transformation,[],[f7444]) ).
fof(f11133,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_altcat_1(X0) ),
inference(ennf_transformation,[],[f7442]) ).
fof(f11202,plain,
! [X0] :
( ( v3_struct_0(X0)
<=> v1_xboole_0(u1_struct_0(X0)) )
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f4588]) ).
fof(f11329,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(f11330,plain,
! [X0] :
( sP0(X0)
| v2_setfam_1(X0) ),
inference(definition_folding,[],[f10412,f11329]) ).
fof(f11336,definition,
! [X0] :
( ( ~ v3_struct_0(k5_waybel34(X0))
& v2_altcat_1(k5_waybel34(X0))
& v6_altcat_1(k5_waybel34(X0))
& v9_altcat_1(k5_waybel34(X0))
& v11_altcat_1(k5_waybel34(X0))
& v12_altcat_1(k5_waybel34(X0))
& v1_altcat_2(k5_waybel34(X0))
& v2_yellow18(k5_waybel34(X0))
& v3_yellow18(k5_waybel34(X0))
& v4_yellow18(k5_waybel34(X0))
& v1_yellow21(k5_waybel34(X0))
& v2_yellow21(k5_waybel34(X0))
& v3_yellow21(k5_waybel34(X0)) )
| ~ sP5(X0) ),
introduced(definition,[new_symbols(definition,[sP5])],[predicate_definition_introduction]) ).
fof(f11337,plain,
! [X0] :
( sP5(X0)
| v2_setfam_1(X0) ),
inference(definition_folding,[],[f10421,f11336]) ).
fof(f11418,plain,
( u1_struct_0(k4_waybel34(sK56)) != u1_struct_0(k5_waybel34(sK56))
& ~ v2_setfam_1(sK56) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK56]),skolemize(X0,sK56)],[f10405]) ).
fof(f11426,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,[],[f10411]) ).
fof(f11427,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,[],[f11426]) ).
fof(f11428,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,[],[f11329]) ).
fof(f11447,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,[],[f10420]) ).
fof(f11448,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,[],[f11447]) ).
fof(f11449,plain,
! [X0] :
( ( ~ v3_struct_0(k5_waybel34(X0))
& v2_altcat_1(k5_waybel34(X0))
& v6_altcat_1(k5_waybel34(X0))
& v9_altcat_1(k5_waybel34(X0))
& v11_altcat_1(k5_waybel34(X0))
& v12_altcat_1(k5_waybel34(X0))
& v1_altcat_2(k5_waybel34(X0))
& v2_yellow18(k5_waybel34(X0))
& v3_yellow18(k5_waybel34(X0))
& v4_yellow18(k5_waybel34(X0))
& v1_yellow21(k5_waybel34(X0))
& v2_yellow21(k5_waybel34(X0))
& v3_yellow21(k5_waybel34(X0)) )
| ~ sP5(X0) ),
inference(nnf_transformation,[],[f11336]) ).
fof(f11473,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,[],[f10443]) ).
fof(f11475,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,[],[f10446]) ).
fof(f11476,plain,
! [X0,X1] :
( X0 = X1
| ( ( ~ r2_hidden(sK72(X0,X1),X1)
| ~ r2_hidden(sK72(X0,X1),X0) )
& ( r2_hidden(sK72(X0,X1),X1)
| r2_hidden(sK72(X0,X1),X0) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK72]),skolemize(X2,sK72(X0,X1))],[f11475]) ).
fof(f11764,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,[],[f11202]) ).
fof(f11873,plain,
~ v2_setfam_1(sK56),
inference(cnf_transformation,[],[f11418]) ).
fof(f11874,plain,
u1_struct_0(k4_waybel34(sK56)) != u1_struct_0(k5_waybel34(sK56)),
inference(cnf_transformation,[],[f11418]) ).
fof(f11880,plain,
! [X0] :
( v2_setfam_1(X0)
| ~ v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f10408]) ).
fof(f11887,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,[],[f11427]) ).
fof(f11888,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u1_struct_0(k4_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,[],[f11427]) ).
fof(f11889,plain,
! [X0,X1] :
( ~ v2_lattice3(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)
| v1_orders_2(X1)
| ~ l1_orders_2(X1)
| v2_setfam_1(X0) ),
inference(cnf_transformation,[],[f11427]) ).
fof(f11890,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,[],[f11427]) ).
fof(f11891,plain,
! [X0] :
( v3_yellow21(k4_waybel34(X0))
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f11428]) ).
fof(f11904,plain,
! [X0] :
( sP0(X0)
| v2_setfam_1(X0) ),
inference(cnf_transformation,[],[f11330]) ).
fof(f11941,plain,
! [X0] :
( l2_altcat_1(k4_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f10417]) ).
fof(f11942,plain,
! [X0] :
( v2_yellow21(k4_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f10417]) ).
fof(f11943,plain,
! [X0] :
( v12_altcat_1(k4_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f10417]) ).
fof(f11944,plain,
! [X0] :
( v11_altcat_1(k4_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f10417]) ).
fof(f11946,plain,
! [X0] :
( v2_altcat_1(k4_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f10417]) ).
fof(f11947,plain,
! [X0] :
( ~ v3_struct_0(k4_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f10417]) ).
fof(f11953,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,[],[f11448]) ).
fof(f11954,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,[],[f11448]) ).
fof(f11955,plain,
! [X0,X1] :
( ~ v2_lattice3(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)
| v1_orders_2(X1)
| ~ l1_orders_2(X1)
| v2_setfam_1(X0) ),
inference(cnf_transformation,[],[f11448]) ).
fof(f11956,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,[],[f11448]) ).
fof(f11957,plain,
! [X0] :
( v3_yellow21(k5_waybel34(X0))
| ~ sP5(X0) ),
inference(cnf_transformation,[],[f11449]) ).
fof(f11970,plain,
! [X0] :
( sP5(X0)
| v2_setfam_1(X0) ),
inference(cnf_transformation,[],[f11337]) ).
fof(f12007,plain,
! [X0] :
( l2_altcat_1(k5_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f10426]) ).
fof(f12008,plain,
! [X0] :
( v2_yellow21(k5_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f10426]) ).
fof(f12009,plain,
! [X0] :
( v12_altcat_1(k5_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f10426]) ).
fof(f12010,plain,
! [X0] :
( v11_altcat_1(k5_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f10426]) ).
fof(f12012,plain,
! [X0] :
( v2_altcat_1(k5_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f10426]) ).
fof(f12013,plain,
! [X0] :
( ~ v3_struct_0(k5_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f10426]) ).
fof(f12021,plain,
! [X0,X1] :
( m1_subset_1(X0,X1)
| ~ r2_hidden(X0,X1) ),
inference(cnf_transformation,[],[f10436]) ).
fof(f12032,plain,
! [X0,X1] :
( r2_hidden(X1,X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f11473]) ).
fof(f12037,plain,
! [X0,X1] :
( r2_hidden(sK72(X0,X1),X1)
| X0 = X1
| r2_hidden(sK72(X0,X1),X0) ),
inference(cnf_transformation,[],[f11476]) ).
fof(f12038,plain,
! [X0,X1] :
( ~ r2_hidden(sK72(X0,X1),X1)
| X0 = X1
| ~ r2_hidden(sK72(X0,X1),X0) ),
inference(cnf_transformation,[],[f11476]) ).
fof(f12112,plain,
! [X0,X1] :
( k1_yellow21(X1) = 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(cnf_transformation,[],[f10485]) ).
fof(f12113,plain,
! [X0,X1] :
( ~ v3_yellow21(X0)
| v3_struct_0(X0)
| ~ v2_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v12_altcat_1(X0)
| l1_orders_2(k4_yellow21(X0,X1))
| ~ l2_altcat_1(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f10487]) ).
fof(f12115,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,[],[f10487]) ).
fof(f12449,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)
| v2_lattice3(k3_yellow21(X0,X1))
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f10605]) ).
fof(f12450,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,[],[f10605]) ).
fof(f12451,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,[],[f10605]) ).
fof(f12452,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,[],[f10605]) ).
fof(f12453,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,[],[f10605]) ).
fof(f12454,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,[],[f10607]) ).
fof(f12777,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,[],[f10797]) ).
fof(f13317,plain,
! [X0] :
( l1_altcat_1(X0)
| ~ l2_altcat_1(X0) ),
inference(cnf_transformation,[],[f11132]) ).
fof(f13319,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_altcat_1(X0) ),
inference(cnf_transformation,[],[f11133]) ).
fof(f13418,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[],[f11764]) ).
fof(f13719,definition,
sF365 = k4_waybel34(sK56),
introduced(definition,[new_symbols(definition,[sF365])],[function_definition]) ).
fof(f13720,plain,
k4_waybel34(sK56) = sF365,
inference(reorient_equations,[],[f13719]) ).
fof(f13721,definition,
sF366 = u1_struct_0(sF365),
introduced(definition,[new_symbols(definition,[sF366])],[function_definition]) ).
fof(f13722,plain,
u1_struct_0(sF365) = sF366,
inference(reorient_equations,[],[f13721]) ).
fof(f13723,definition,
sF367 = k5_waybel34(sK56),
introduced(definition,[new_symbols(definition,[sF367])],[function_definition]) ).
fof(f13724,plain,
k5_waybel34(sK56) = sF367,
inference(reorient_equations,[],[f13723]) ).
fof(f13725,definition,
sF368 = u1_struct_0(sF367),
introduced(definition,[new_symbols(definition,[sF368])],[function_definition]) ).
fof(f13726,plain,
u1_struct_0(sF367) = sF368,
inference(reorient_equations,[],[f13725]) ).
fof(f13727,plain,
sF366 != sF368,
inference(definition_folding,[],[f11874,f13726,f13724,f13722,f13720]) ).
fof(f13730,plain,
( ~ v3_struct_0(sF365)
| v1_xboole_0(sK56) ),
inference(superposition,[],[f11947,f13720]) ).
fof(f13732,definition,
( spl369_1
<=> v1_xboole_0(sK56) ),
introduced(definition,[new_symbols(definition,[spl369_1])],[avatar_definition]) ).
fof(f13736,definition,
( spl369_2
<=> v3_struct_0(sF365) ),
introduced(definition,[new_symbols(definition,[spl369_2])],[avatar_definition]) ).
fof(f13739,plain,
( spl369_1
| ~ spl369_2 ),
inference(avatar_split_clause,[],[f13730,f13736,f13732]) ).
fof(f13740,plain,
( ~ v3_struct_0(sF367)
| v1_xboole_0(sK56) ),
inference(superposition,[],[f12013,f13724]) ).
fof(f13742,definition,
( spl369_3
<=> v3_struct_0(sF367) ),
introduced(definition,[new_symbols(definition,[spl369_3])],[avatar_definition]) ).
fof(f13745,plain,
( spl369_1
| ~ spl369_3 ),
inference(avatar_split_clause,[],[f13740,f13742,f13732]) ).
fof(f13746,plain,
~ v1_xboole_0(sK56),
inference(resolution,[],[f11880,f11873]) ).
fof(f13747,plain,
~ spl369_1,
inference(avatar_split_clause,[],[f13746,f13732]) ).
fof(f13748,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sF365))
| r2_hidden(u1_struct_0(X0),sK56)
| ~ 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(sK56) ),
inference(superposition,[],[f11887,f13720]) ).
fof(f13749,plain,
! [X0] :
( ~ m1_subset_1(X0,sF366)
| r2_hidden(u1_struct_0(X0),sK56)
| ~ 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(sK56) ),
inference(forward_demodulation,[],[f13748,f13722]) ).
fof(f13751,definition,
( spl369_4
<=> v2_setfam_1(sK56) ),
introduced(definition,[new_symbols(definition,[spl369_4])],[avatar_definition]) ).
fof(f13752,plain,
( ~ v2_setfam_1(sK56)
| spl369_4 ),
inference(avatar_component_clause,[],[f13751]) ).
fof(f13755,definition,
( spl369_5
<=> ! [X0] :
( ~ m1_subset_1(X0,sF366)
| ~ 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),sK56) ) ),
introduced(definition,[new_symbols(definition,[spl369_5])],[avatar_definition]) ).
fof(f13756,plain,
( ! [X0] :
( r2_hidden(u1_struct_0(X0),sK56)
| ~ 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,sF366) )
| ~ spl369_5 ),
inference(avatar_component_clause,[],[f13755]) ).
fof(f13757,plain,
( spl369_4
| spl369_5 ),
inference(avatar_split_clause,[],[f13749,f13755,f13751]) ).
fof(f13826,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sF367))
| r2_hidden(u1_struct_0(X0),sK56)
| ~ 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(sK56) ),
inference(superposition,[],[f11953,f13724]) ).
fof(f13827,plain,
! [X0] :
( ~ m1_subset_1(X0,sF368)
| r2_hidden(u1_struct_0(X0),sK56)
| ~ 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(sK56) ),
inference(forward_demodulation,[],[f13826,f13726]) ).
fof(f13829,definition,
( spl369_22
<=> ! [X0] :
( ~ m1_subset_1(X0,sF368)
| ~ 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),sK56) ) ),
introduced(definition,[new_symbols(definition,[spl369_22])],[avatar_definition]) ).
fof(f13830,plain,
( ! [X0] :
( r2_hidden(u1_struct_0(X0),sK56)
| ~ 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,sF368) )
| ~ spl369_22 ),
inference(avatar_component_clause,[],[f13829]) ).
fof(f13831,plain,
( spl369_4
| spl369_22 ),
inference(avatar_split_clause,[],[f13827,f13829,f13751]) ).
fof(f13844,plain,
( v2_altcat_1(sF365)
| v1_xboole_0(sK56) ),
inference(superposition,[],[f11946,f13720]) ).
fof(f13846,definition,
( spl369_25
<=> v2_altcat_1(sF365) ),
introduced(definition,[new_symbols(definition,[spl369_25])],[avatar_definition]) ).
fof(f13849,plain,
( spl369_1
| spl369_25 ),
inference(avatar_split_clause,[],[f13844,f13846,f13732]) ).
fof(f13850,plain,
( v2_altcat_1(sF367)
| v1_xboole_0(sK56) ),
inference(superposition,[],[f12012,f13724]) ).
fof(f13852,definition,
( spl369_26
<=> v2_altcat_1(sF367) ),
introduced(definition,[new_symbols(definition,[spl369_26])],[avatar_definition]) ).
fof(f13855,plain,
( spl369_1
| spl369_26 ),
inference(avatar_split_clause,[],[f13850,f13852,f13732]) ).
fof(f13856,plain,
( v11_altcat_1(sF365)
| v1_xboole_0(sK56) ),
inference(superposition,[],[f11944,f13720]) ).
fof(f13858,definition,
( spl369_27
<=> v11_altcat_1(sF365) ),
introduced(definition,[new_symbols(definition,[spl369_27])],[avatar_definition]) ).
fof(f13861,plain,
( spl369_1
| spl369_27 ),
inference(avatar_split_clause,[],[f13856,f13858,f13732]) ).
fof(f13862,plain,
( v2_yellow21(sF365)
| v1_xboole_0(sK56) ),
inference(superposition,[],[f11942,f13720]) ).
fof(f13864,definition,
( spl369_28
<=> v2_yellow21(sF365) ),
introduced(definition,[new_symbols(definition,[spl369_28])],[avatar_definition]) ).
fof(f13867,plain,
( spl369_1
| spl369_28 ),
inference(avatar_split_clause,[],[f13862,f13864,f13732]) ).
fof(f13868,plain,
( v11_altcat_1(sF367)
| v1_xboole_0(sK56) ),
inference(superposition,[],[f12010,f13724]) ).
fof(f13870,definition,
( spl369_29
<=> v11_altcat_1(sF367) ),
introduced(definition,[new_symbols(definition,[spl369_29])],[avatar_definition]) ).
fof(f13873,plain,
( spl369_1
| spl369_29 ),
inference(avatar_split_clause,[],[f13868,f13870,f13732]) ).
fof(f13874,plain,
( l2_altcat_1(sF365)
| v1_xboole_0(sK56) ),
inference(superposition,[],[f11941,f13720]) ).
fof(f13876,definition,
( spl369_30
<=> l2_altcat_1(sF365) ),
introduced(definition,[new_symbols(definition,[spl369_30])],[avatar_definition]) ).
fof(f13878,plain,
( l2_altcat_1(sF365)
| ~ spl369_30 ),
inference(avatar_component_clause,[],[f13876]) ).
fof(f13879,plain,
( spl369_1
| spl369_30 ),
inference(avatar_split_clause,[],[f13874,f13876,f13732]) ).
fof(f13880,plain,
( v2_yellow21(sF367)
| v1_xboole_0(sK56) ),
inference(superposition,[],[f12008,f13724]) ).
fof(f13882,definition,
( spl369_31
<=> v2_yellow21(sF367) ),
introduced(definition,[new_symbols(definition,[spl369_31])],[avatar_definition]) ).
fof(f13885,plain,
( spl369_1
| spl369_31 ),
inference(avatar_split_clause,[],[f13880,f13882,f13732]) ).
fof(f13886,plain,
( l2_altcat_1(sF367)
| v1_xboole_0(sK56) ),
inference(superposition,[],[f12007,f13724]) ).
fof(f13888,definition,
( spl369_32
<=> l2_altcat_1(sF367) ),
introduced(definition,[new_symbols(definition,[spl369_32])],[avatar_definition]) ).
fof(f13890,plain,
( l2_altcat_1(sF367)
| ~ spl369_32 ),
inference(avatar_component_clause,[],[f13888]) ).
fof(f13891,plain,
( spl369_1
| spl369_32 ),
inference(avatar_split_clause,[],[f13886,f13888,f13732]) ).
fof(f13892,plain,
( v12_altcat_1(sF365)
| v1_xboole_0(sK56) ),
inference(superposition,[],[f11943,f13720]) ).
fof(f13894,definition,
( spl369_33
<=> v12_altcat_1(sF365) ),
introduced(definition,[new_symbols(definition,[spl369_33])],[avatar_definition]) ).
fof(f13897,plain,
( spl369_1
| spl369_33 ),
inference(avatar_split_clause,[],[f13892,f13894,f13732]) ).
fof(f13898,plain,
( v12_altcat_1(sF367)
| v1_xboole_0(sK56) ),
inference(superposition,[],[f12009,f13724]) ).
fof(f13900,definition,
( spl369_34
<=> v12_altcat_1(sF367) ),
introduced(definition,[new_symbols(definition,[spl369_34])],[avatar_definition]) ).
fof(f13903,plain,
( spl369_1
| spl369_34 ),
inference(avatar_split_clause,[],[f13898,f13900,f13732]) ).
fof(f13910,plain,
( ~ v1_xboole_0(sF366)
| v3_struct_0(sF365)
| ~ l1_struct_0(sF365) ),
inference(superposition,[],[f13418,f13722]) ).
fof(f13911,plain,
( ~ v1_xboole_0(sF368)
| v3_struct_0(sF367)
| ~ l1_struct_0(sF367) ),
inference(superposition,[],[f13418,f13726]) ).
fof(f13913,definition,
( spl369_35
<=> l1_struct_0(sF367) ),
introduced(definition,[new_symbols(definition,[spl369_35])],[avatar_definition]) ).
fof(f13915,plain,
( ~ l1_struct_0(sF367)
| spl369_35 ),
inference(avatar_component_clause,[],[f13913]) ).
fof(f13917,definition,
( spl369_36
<=> v1_xboole_0(sF368) ),
introduced(definition,[new_symbols(definition,[spl369_36])],[avatar_definition]) ).
fof(f13920,plain,
( ~ spl369_35
| spl369_3
| ~ spl369_36 ),
inference(avatar_split_clause,[],[f13911,f13917,f13742,f13913]) ).
fof(f13922,definition,
( spl369_37
<=> l1_struct_0(sF365) ),
introduced(definition,[new_symbols(definition,[spl369_37])],[avatar_definition]) ).
fof(f13924,plain,
( ~ l1_struct_0(sF365)
| spl369_37 ),
inference(avatar_component_clause,[],[f13922]) ).
fof(f13926,definition,
( spl369_38
<=> v1_xboole_0(sF366) ),
introduced(definition,[new_symbols(definition,[spl369_38])],[avatar_definition]) ).
fof(f13929,plain,
( ~ spl369_37
| spl369_2
| ~ spl369_38 ),
inference(avatar_split_clause,[],[f13910,f13926,f13736,f13922]) ).
fof(f13932,plain,
( ~ l1_altcat_1(sF367)
| spl369_35 ),
inference(resolution,[],[f13915,f13319]) ).
fof(f13955,plain,
( ~ l2_altcat_1(sF367)
| spl369_35 ),
inference(resolution,[],[f13932,f13317]) ).
fof(f13956,plain,
( ~ spl369_32
| spl369_35 ),
inference(avatar_split_clause,[],[f13955,f13913,f13888]) ).
fof(f13970,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sF365))
| 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(sK56) ),
inference(superposition,[],[f11888,f13720]) ).
fof(f13971,plain,
! [X0] :
( ~ m1_subset_1(X0,sF366)
| 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(sK56) ),
inference(forward_demodulation,[],[f13970,f13722]) ).
fof(f13973,definition,
( spl369_41
<=> ! [X0] :
( ~ m1_subset_1(X0,sF366)
| ~ 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,[spl369_41])],[avatar_definition]) ).
fof(f13974,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF366)
| ~ 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) )
| ~ spl369_41 ),
inference(avatar_component_clause,[],[f13973]) ).
fof(f13975,plain,
( spl369_4
| spl369_41 ),
inference(avatar_split_clause,[],[f13971,f13973,f13751]) ).
fof(f14013,plain,
! [X0] :
( m1_subset_1(X0,u1_struct_0(sF365))
| ~ v1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ r2_hidden(u1_struct_0(X0),sK56)
| ~ 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(sK56) ),
inference(superposition,[],[f11890,f13720]) ).
fof(f14016,plain,
! [X0] :
( m1_subset_1(X0,sF366)
| ~ v1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ r2_hidden(u1_struct_0(X0),sK56)
| ~ 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(sK56) ),
inference(forward_demodulation,[],[f14013,f13722]) ).
fof(f14018,definition,
( spl369_50
<=> ! [X0] :
( m1_subset_1(X0,sF366)
| ~ 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),sK56)
| ~ v3_lattice3(X0)
| ~ v1_orders_2(X0) ) ),
introduced(definition,[new_symbols(definition,[spl369_50])],[avatar_definition]) ).
fof(f14019,plain,
( ! [X0] :
( ~ r2_hidden(u1_struct_0(X0),sK56)
| ~ 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,sF366)
| ~ v3_lattice3(X0)
| ~ v1_orders_2(X0) )
| ~ spl369_50 ),
inference(avatar_component_clause,[],[f14018]) ).
fof(f14020,plain,
( spl369_4
| spl369_50 ),
inference(avatar_split_clause,[],[f14016,f14018,f13751]) ).
fof(f14023,plain,
~ spl369_4,
inference(avatar_split_clause,[],[f11873,f13751]) ).
fof(f14025,plain,
( ! [X0] :
( ~ 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,sF366)
| ~ v3_lattice3(X0)
| ~ v1_orders_2(X0)
| ~ 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,sF368) )
| ~ spl369_22
| ~ spl369_50 ),
inference(resolution,[],[f14019,f13830]) ).
fof(f14031,plain,
( ! [X0] :
( m1_subset_1(X0,sF366)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v1_orders_2(X0)
| ~ m1_subset_1(X0,sF368) )
| ~ spl369_22
| ~ spl369_50 ),
inference(duplicate_literal_removal,[],[f14025]) ).
fof(f14036,plain,
! [X0] :
( m1_subset_1(X0,u1_struct_0(sF367))
| ~ v1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ r2_hidden(u1_struct_0(X0),sK56)
| ~ 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(sK56) ),
inference(superposition,[],[f11956,f13724]) ).
fof(f14038,plain,
! [X0] :
( m1_subset_1(X0,sF368)
| ~ v1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ r2_hidden(u1_struct_0(X0),sK56)
| ~ 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(sK56) ),
inference(forward_demodulation,[],[f14036,f13726]) ).
fof(f14040,definition,
( spl369_51
<=> ! [X0] :
( m1_subset_1(X0,sF368)
| ~ 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),sK56)
| ~ v3_lattice3(X0)
| ~ v1_orders_2(X0) ) ),
introduced(definition,[new_symbols(definition,[spl369_51])],[avatar_definition]) ).
fof(f14041,plain,
( ! [X0] :
( ~ r2_hidden(u1_struct_0(X0),sK56)
| ~ 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,sF368)
| ~ v3_lattice3(X0)
| ~ v1_orders_2(X0) )
| ~ spl369_51 ),
inference(avatar_component_clause,[],[f14040]) ).
fof(f14042,plain,
( spl369_4
| spl369_51 ),
inference(avatar_split_clause,[],[f14038,f14040,f13751]) ).
fof(f14044,plain,
( ! [X0] :
( ~ 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,sF368)
| ~ v3_lattice3(X0)
| ~ v1_orders_2(X0)
| ~ 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,sF366) )
| ~ spl369_5
| ~ spl369_51 ),
inference(resolution,[],[f14041,f13756]) ).
fof(f14048,plain,
( ! [X0] :
( m1_subset_1(X0,sF368)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v1_orders_2(X0)
| ~ m1_subset_1(X0,sF366) )
| ~ spl369_5
| ~ spl369_51 ),
inference(duplicate_literal_removal,[],[f14044]) ).
fof(f14053,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sF367))
| 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(sK56) ),
inference(superposition,[],[f11954,f13724]) ).
fof(f14055,plain,
! [X0] :
( ~ m1_subset_1(X0,sF368)
| 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(sK56) ),
inference(forward_demodulation,[],[f14053,f13726]) ).
fof(f14057,definition,
( spl369_52
<=> ! [X0] :
( ~ m1_subset_1(X0,sF368)
| ~ 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,[spl369_52])],[avatar_definition]) ).
fof(f14058,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF368)
| ~ 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) )
| ~ spl369_52 ),
inference(avatar_component_clause,[],[f14057]) ).
fof(f14059,plain,
( spl369_4
| spl369_52 ),
inference(avatar_split_clause,[],[f14055,f14057,f13751]) ).
fof(f14256,definition,
( spl369_76
<=> sP0(sK56) ),
introduced(definition,[new_symbols(definition,[spl369_76])],[avatar_definition]) ).
fof(f14258,plain,
( ~ sP0(sK56)
| spl369_76 ),
inference(avatar_component_clause,[],[f14256]) ).
fof(f14264,plain,
( v2_setfam_1(sK56)
| spl369_76 ),
inference(resolution,[],[f14258,f11904]) ).
fof(f14265,plain,
( spl369_4
| spl369_76 ),
inference(avatar_split_clause,[],[f14264,f14256,f13751]) ).
fof(f14269,plain,
! [X0,X1] :
( ~ r2_hidden(sK72(X0,X1),X0)
| v1_xboole_0(X1)
| X0 = X1
| ~ m1_subset_1(sK72(X0,X1),X1) ),
inference(resolution,[],[f12032,f12038]) ).
fof(f14427,definition,
( spl369_86
<=> sF366 = sF368 ),
introduced(definition,[new_symbols(definition,[spl369_86])],[avatar_definition]) ).
fof(f14487,definition,
( spl369_96
<=> sP5(sK56) ),
introduced(definition,[new_symbols(definition,[spl369_96])],[avatar_definition]) ).
fof(f14489,plain,
( ~ sP5(sK56)
| spl369_96 ),
inference(avatar_component_clause,[],[f14487]) ).
fof(f14495,plain,
( v2_setfam_1(sK56)
| spl369_96 ),
inference(resolution,[],[f14489,f11970]) ).
fof(f14496,plain,
( spl369_4
| spl369_96 ),
inference(avatar_split_clause,[],[f14495,f14487,f13751]) ).
fof(f14537,plain,
( v3_yellow21(sF365)
| ~ sP0(sK56) ),
inference(superposition,[],[f11891,f13720]) ).
fof(f14539,definition,
( spl369_102
<=> v3_yellow21(sF365) ),
introduced(definition,[new_symbols(definition,[spl369_102])],[avatar_definition]) ).
fof(f14541,plain,
( v3_yellow21(sF365)
| ~ spl369_102 ),
inference(avatar_component_clause,[],[f14539]) ).
fof(f14542,plain,
( ~ spl369_76
| spl369_102 ),
inference(avatar_split_clause,[],[f14537,f14539,f14256]) ).
fof(f14567,plain,
( ! [X0] :
( v3_struct_0(sF367)
| ~ v2_altcat_1(sF367)
| ~ v11_altcat_1(sF367)
| ~ v12_altcat_1(sF367)
| ~ v2_yellow21(sF367)
| v2_lattice3(k3_yellow21(sF367,X0))
| ~ m1_subset_1(X0,u1_struct_0(sF367)) )
| ~ spl369_32 ),
inference(resolution,[],[f12449,f13890]) ).
fof(f14568,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF368)
| v3_struct_0(sF367)
| ~ v2_altcat_1(sF367)
| ~ v11_altcat_1(sF367)
| ~ v12_altcat_1(sF367)
| ~ v2_yellow21(sF367)
| v2_lattice3(k3_yellow21(sF367,X0)) )
| ~ spl369_32 ),
inference(forward_demodulation,[],[f14567,f13726]) ).
fof(f14571,definition,
( spl369_104
<=> ! [X0] :
( ~ m1_subset_1(X0,sF368)
| v2_lattice3(k3_yellow21(sF367,X0)) ) ),
introduced(definition,[new_symbols(definition,[spl369_104])],[avatar_definition]) ).
fof(f14572,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF368)
| v2_lattice3(k3_yellow21(sF367,X0)) )
| ~ spl369_104 ),
inference(avatar_component_clause,[],[f14571]) ).
fof(f14573,plain,
( ~ spl369_31
| ~ spl369_34
| ~ spl369_29
| ~ spl369_26
| spl369_3
| spl369_104
| ~ spl369_32 ),
inference(avatar_split_clause,[],[f14568,f13888,f14571,f13742,f13852,f13870,f13900,f13882]) ).
fof(f14591,plain,
( v3_yellow21(sF367)
| ~ sP5(sK56) ),
inference(superposition,[],[f11957,f13724]) ).
fof(f14593,definition,
( spl369_107
<=> v3_yellow21(sF367) ),
introduced(definition,[new_symbols(definition,[spl369_107])],[avatar_definition]) ).
fof(f14595,plain,
( v3_yellow21(sF367)
| ~ spl369_107 ),
inference(avatar_component_clause,[],[f14593]) ).
fof(f14596,plain,
( ~ spl369_96
| spl369_107 ),
inference(avatar_split_clause,[],[f14591,f14593,f14487]) ).
fof(f14599,plain,
( ! [X0] :
( v3_struct_0(sF365)
| ~ v2_altcat_1(sF365)
| ~ v11_altcat_1(sF365)
| ~ v12_altcat_1(sF365)
| ~ v2_yellow21(sF365)
| k1_yellow21(X0) = k3_yellow21(sF365,X0)
| ~ m1_subset_1(X0,u1_struct_0(sF365)) )
| ~ spl369_30 ),
inference(resolution,[],[f12777,f13878]) ).
fof(f14600,plain,
( ! [X0] :
( v3_struct_0(sF367)
| ~ v2_altcat_1(sF367)
| ~ v11_altcat_1(sF367)
| ~ v12_altcat_1(sF367)
| ~ v2_yellow21(sF367)
| k1_yellow21(X0) = k3_yellow21(sF367,X0)
| ~ m1_subset_1(X0,u1_struct_0(sF367)) )
| ~ spl369_32 ),
inference(resolution,[],[f12777,f13890]) ).
fof(f14601,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF368)
| v3_struct_0(sF367)
| ~ v2_altcat_1(sF367)
| ~ v11_altcat_1(sF367)
| ~ v12_altcat_1(sF367)
| ~ v2_yellow21(sF367)
| k1_yellow21(X0) = k3_yellow21(sF367,X0) )
| ~ spl369_32 ),
inference(forward_demodulation,[],[f14600,f13726]) ).
fof(f14602,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF366)
| v3_struct_0(sF365)
| ~ v2_altcat_1(sF365)
| ~ v11_altcat_1(sF365)
| ~ v12_altcat_1(sF365)
| ~ v2_yellow21(sF365)
| k1_yellow21(X0) = k3_yellow21(sF365,X0) )
| ~ spl369_30 ),
inference(forward_demodulation,[],[f14599,f13722]) ).
fof(f14604,definition,
( spl369_108
<=> ! [X0] :
( ~ m1_subset_1(X0,sF368)
| k1_yellow21(X0) = k3_yellow21(sF367,X0) ) ),
introduced(definition,[new_symbols(definition,[spl369_108])],[avatar_definition]) ).
fof(f14605,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF368)
| k1_yellow21(X0) = k3_yellow21(sF367,X0) )
| ~ spl369_108 ),
inference(avatar_component_clause,[],[f14604]) ).
fof(f14606,plain,
( ~ spl369_31
| ~ spl369_34
| ~ spl369_29
| ~ spl369_26
| spl369_3
| spl369_108
| ~ spl369_32 ),
inference(avatar_split_clause,[],[f14601,f13888,f14604,f13742,f13852,f13870,f13900,f13882]) ).
fof(f14608,definition,
( spl369_109
<=> ! [X0] :
( ~ m1_subset_1(X0,sF366)
| k1_yellow21(X0) = k3_yellow21(sF365,X0) ) ),
introduced(definition,[new_symbols(definition,[spl369_109])],[avatar_definition]) ).
fof(f14609,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF366)
| k1_yellow21(X0) = k3_yellow21(sF365,X0) )
| ~ spl369_109 ),
inference(avatar_component_clause,[],[f14608]) ).
fof(f14610,plain,
( ~ spl369_28
| ~ spl369_33
| ~ spl369_27
| ~ spl369_25
| spl369_2
| spl369_109
| ~ spl369_30 ),
inference(avatar_split_clause,[],[f14602,f13876,f14608,f13736,f13846,f13858,f13894,f13864]) ).
fof(f14748,plain,
~ spl369_86,
inference(avatar_split_clause,[],[f13727,f14427]) ).
fof(f15339,plain,
( ! [X0] :
( v3_struct_0(sF365)
| ~ v2_altcat_1(sF365)
| ~ v11_altcat_1(sF365)
| ~ v12_altcat_1(sF365)
| l1_orders_2(k4_yellow21(sF365,X0))
| ~ l2_altcat_1(sF365)
| ~ m1_subset_1(X0,u1_struct_0(sF365)) )
| ~ spl369_102 ),
inference(resolution,[],[f12113,f14541]) ).
fof(f15340,plain,
( ! [X0] :
( v3_struct_0(sF367)
| ~ v2_altcat_1(sF367)
| ~ v11_altcat_1(sF367)
| ~ v12_altcat_1(sF367)
| l1_orders_2(k4_yellow21(sF367,X0))
| ~ l2_altcat_1(sF367)
| ~ m1_subset_1(X0,u1_struct_0(sF367)) )
| ~ spl369_107 ),
inference(resolution,[],[f12113,f14595]) ).
fof(f15341,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF368)
| v3_struct_0(sF367)
| ~ v2_altcat_1(sF367)
| ~ v11_altcat_1(sF367)
| ~ v12_altcat_1(sF367)
| l1_orders_2(k4_yellow21(sF367,X0))
| ~ l2_altcat_1(sF367) )
| ~ spl369_107 ),
inference(forward_demodulation,[],[f15340,f13726]) ).
fof(f15342,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF366)
| v3_struct_0(sF365)
| ~ v2_altcat_1(sF365)
| ~ v11_altcat_1(sF365)
| ~ v12_altcat_1(sF365)
| l1_orders_2(k4_yellow21(sF365,X0))
| ~ l2_altcat_1(sF365) )
| ~ spl369_102 ),
inference(forward_demodulation,[],[f15339,f13722]) ).
fof(f15344,definition,
( spl369_169
<=> ! [X0] :
( ~ m1_subset_1(X0,sF368)
| l1_orders_2(k4_yellow21(sF367,X0)) ) ),
introduced(definition,[new_symbols(definition,[spl369_169])],[avatar_definition]) ).
fof(f15345,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF368)
| l1_orders_2(k4_yellow21(sF367,X0)) )
| ~ spl369_169 ),
inference(avatar_component_clause,[],[f15344]) ).
fof(f15346,plain,
( ~ spl369_32
| ~ spl369_34
| ~ spl369_29
| ~ spl369_26
| spl369_3
| spl369_169
| ~ spl369_107 ),
inference(avatar_split_clause,[],[f15341,f14593,f15344,f13742,f13852,f13870,f13900,f13888]) ).
fof(f15348,definition,
( spl369_170
<=> ! [X0] :
( ~ m1_subset_1(X0,sF366)
| l1_orders_2(k4_yellow21(sF365,X0)) ) ),
introduced(definition,[new_symbols(definition,[spl369_170])],[avatar_definition]) ).
fof(f15349,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF366)
| l1_orders_2(k4_yellow21(sF365,X0)) )
| ~ spl369_170 ),
inference(avatar_component_clause,[],[f15348]) ).
fof(f15350,plain,
( ~ spl369_30
| ~ spl369_33
| ~ spl369_27
| ~ spl369_25
| spl369_2
| spl369_170
| ~ spl369_102 ),
inference(avatar_split_clause,[],[f15342,f14539,f15348,f13736,f13846,f13858,f13894,f13876]) ).
fof(f15352,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF366)
| l1_orders_2(k4_yellow21(sF365,X0)) )
| ~ spl369_170 ),
inference(resolution,[],[f15349,f12021]) ).
fof(f15355,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF368)
| l1_orders_2(k4_yellow21(sF367,X0)) )
| ~ spl369_169 ),
inference(resolution,[],[f15345,f12021]) ).
fof(f15362,plain,
( ! [X0] :
( r2_hidden(sK72(X0,sF366),X0)
| sF366 = X0
| l1_orders_2(k4_yellow21(sF365,sK72(X0,sF366))) )
| ~ spl369_170 ),
inference(resolution,[],[f15352,f12037]) ).
fof(f15504,plain,
( l1_orders_2(k4_yellow21(sF367,sK72(sF368,sF366)))
| sF366 = sF368
| l1_orders_2(k4_yellow21(sF365,sK72(sF368,sF366)))
| ~ spl369_169
| ~ spl369_170 ),
inference(resolution,[],[f15355,f15362]) ).
fof(f15598,definition,
( spl369_203
<=> l1_orders_2(k4_yellow21(sF365,sK72(sF368,sF366))) ),
introduced(definition,[new_symbols(definition,[spl369_203])],[avatar_definition]) ).
fof(f15600,plain,
( l1_orders_2(k4_yellow21(sF365,sK72(sF368,sF366)))
| ~ spl369_203 ),
inference(avatar_component_clause,[],[f15598]) ).
fof(f15602,definition,
( spl369_204
<=> l1_orders_2(k4_yellow21(sF367,sK72(sF368,sF366))) ),
introduced(definition,[new_symbols(definition,[spl369_204])],[avatar_definition]) ).
fof(f15604,plain,
( l1_orders_2(k4_yellow21(sF367,sK72(sF368,sF366)))
| ~ spl369_204 ),
inference(avatar_component_clause,[],[f15602]) ).
fof(f15605,plain,
( spl369_203
| spl369_86
| spl369_204
| ~ spl369_169
| ~ spl369_170 ),
inference(avatar_split_clause,[],[f15504,f15348,f15344,f15602,f14427,f15598]) ).
fof(f15657,plain,
( ! [X0] :
( v3_struct_0(sF365)
| ~ v2_altcat_1(sF365)
| ~ v11_altcat_1(sF365)
| ~ v12_altcat_1(sF365)
| v2_lattice3(k4_yellow21(sF365,X0))
| ~ l2_altcat_1(sF365)
| ~ m1_subset_1(X0,u1_struct_0(sF365)) )
| ~ spl369_102 ),
inference(resolution,[],[f12115,f14541]) ).
fof(f15660,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF366)
| v3_struct_0(sF365)
| ~ v2_altcat_1(sF365)
| ~ v11_altcat_1(sF365)
| ~ v12_altcat_1(sF365)
| v2_lattice3(k4_yellow21(sF365,X0))
| ~ l2_altcat_1(sF365) )
| ~ spl369_102 ),
inference(forward_demodulation,[],[f15657,f13722]) ).
fof(f15663,definition,
( spl369_208
<=> ! [X0] :
( ~ m1_subset_1(X0,sF366)
| v2_lattice3(k4_yellow21(sF365,X0)) ) ),
introduced(definition,[new_symbols(definition,[spl369_208])],[avatar_definition]) ).
fof(f15664,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF366)
| v2_lattice3(k4_yellow21(sF365,X0)) )
| ~ spl369_208 ),
inference(avatar_component_clause,[],[f15663]) ).
fof(f15665,plain,
( ~ spl369_30
| ~ spl369_33
| ~ spl369_27
| ~ spl369_25
| spl369_2
| spl369_208
| ~ spl369_102 ),
inference(avatar_split_clause,[],[f15660,f14539,f15663,f13736,f13846,f13858,f13894,f13876]) ).
fof(f15745,definition,
( spl369_223
<=> m1_subset_1(sK72(sF368,sF366),sF366) ),
introduced(definition,[new_symbols(definition,[spl369_223])],[avatar_definition]) ).
fof(f15746,plain,
( m1_subset_1(sK72(sF368,sF366),sF366)
| ~ spl369_223 ),
inference(avatar_component_clause,[],[f15745]) ).
fof(f15747,plain,
( ~ m1_subset_1(sK72(sF368,sF366),sF366)
| spl369_223 ),
inference(avatar_component_clause,[],[f15745]) ).
fof(f15879,definition,
( spl369_248
<=> m1_subset_1(sK72(sF368,sF366),sF368) ),
introduced(definition,[new_symbols(definition,[spl369_248])],[avatar_definition]) ).
fof(f15880,plain,
( m1_subset_1(sK72(sF368,sF366),sF368)
| ~ spl369_248 ),
inference(avatar_component_clause,[],[f15879]) ).
fof(f15881,plain,
( ~ m1_subset_1(sK72(sF368,sF366),sF368)
| spl369_248 ),
inference(avatar_component_clause,[],[f15879]) ).
fof(f15883,plain,
( ~ v2_lattice3(sK72(sF368,sF366))
| ~ v1_lattice3(sK72(sF368,sF366))
| ~ v4_orders_2(sK72(sF368,sF366))
| ~ v3_orders_2(sK72(sF368,sF366))
| ~ v2_orders_2(sK72(sF368,sF366))
| ~ l1_orders_2(sK72(sF368,sF366))
| ~ v3_lattice3(sK72(sF368,sF366))
| ~ v1_orders_2(sK72(sF368,sF366))
| ~ m1_subset_1(sK72(sF368,sF366),sF368)
| ~ spl369_22
| ~ spl369_50
| spl369_223 ),
inference(resolution,[],[f15747,f14031]) ).
fof(f15884,plain,
( ~ r2_hidden(sK72(sF368,sF366),sF366)
| spl369_223 ),
inference(resolution,[],[f15747,f12021]) ).
fof(f15886,definition,
( spl369_249
<=> v1_orders_2(sK72(sF368,sF366)) ),
introduced(definition,[new_symbols(definition,[spl369_249])],[avatar_definition]) ).
fof(f15890,definition,
( spl369_250
<=> v3_lattice3(sK72(sF368,sF366)) ),
introduced(definition,[new_symbols(definition,[spl369_250])],[avatar_definition]) ).
fof(f15894,definition,
( spl369_251
<=> l1_orders_2(sK72(sF368,sF366)) ),
introduced(definition,[new_symbols(definition,[spl369_251])],[avatar_definition]) ).
fof(f15898,definition,
( spl369_252
<=> v2_orders_2(sK72(sF368,sF366)) ),
introduced(definition,[new_symbols(definition,[spl369_252])],[avatar_definition]) ).
fof(f15902,definition,
( spl369_253
<=> v3_orders_2(sK72(sF368,sF366)) ),
introduced(definition,[new_symbols(definition,[spl369_253])],[avatar_definition]) ).
fof(f15906,definition,
( spl369_254
<=> v4_orders_2(sK72(sF368,sF366)) ),
introduced(definition,[new_symbols(definition,[spl369_254])],[avatar_definition]) ).
fof(f15910,definition,
( spl369_255
<=> v1_lattice3(sK72(sF368,sF366)) ),
introduced(definition,[new_symbols(definition,[spl369_255])],[avatar_definition]) ).
fof(f15914,definition,
( spl369_256
<=> v2_lattice3(sK72(sF368,sF366)) ),
introduced(definition,[new_symbols(definition,[spl369_256])],[avatar_definition]) ).
fof(f15915,plain,
( v2_lattice3(sK72(sF368,sF366))
| ~ spl369_256 ),
inference(avatar_component_clause,[],[f15914]) ).
fof(f15917,plain,
( ~ spl369_248
| ~ spl369_249
| ~ spl369_250
| ~ spl369_251
| ~ spl369_252
| ~ spl369_253
| ~ spl369_254
| ~ spl369_255
| ~ spl369_256
| ~ spl369_22
| ~ spl369_50
| spl369_223 ),
inference(avatar_split_clause,[],[f15883,f15745,f14018,f13829,f15914,f15910,f15906,f15902,f15898,f15894,f15890,f15886,f15879]) ).
fof(f15918,plain,
( ~ v2_lattice3(sK72(sF368,sF366))
| ~ v1_lattice3(sK72(sF368,sF366))
| ~ v4_orders_2(sK72(sF368,sF366))
| ~ v3_orders_2(sK72(sF368,sF366))
| ~ v2_orders_2(sK72(sF368,sF366))
| ~ l1_orders_2(sK72(sF368,sF366))
| ~ v3_lattice3(sK72(sF368,sF366))
| ~ v1_orders_2(sK72(sF368,sF366))
| ~ m1_subset_1(sK72(sF368,sF366),sF366)
| ~ spl369_5
| ~ spl369_51
| spl369_248 ),
inference(resolution,[],[f15881,f14048]) ).
fof(f15919,plain,
( ~ r2_hidden(sK72(sF368,sF366),sF368)
| spl369_248 ),
inference(resolution,[],[f15881,f12021]) ).
fof(f15920,plain,
( sF366 = sF368
| l1_orders_2(k4_yellow21(sF365,sK72(sF368,sF366)))
| ~ spl369_170
| spl369_248 ),
inference(resolution,[],[f15919,f15362]) ).
fof(f15923,plain,
( spl369_203
| spl369_86
| ~ spl369_170
| spl369_248 ),
inference(avatar_split_clause,[],[f15920,f15879,f15348,f14427,f15598]) ).
fof(f15924,plain,
( sF366 = sF368
| r2_hidden(sK72(sF368,sF366),sF368)
| spl369_223 ),
inference(resolution,[],[f15884,f12037]) ).
fof(f15928,definition,
( spl369_257
<=> r2_hidden(sK72(sF368,sF366),sF368) ),
introduced(definition,[new_symbols(definition,[spl369_257])],[avatar_definition]) ).
fof(f15929,plain,
( ~ r2_hidden(sK72(sF368,sF366),sF368)
| spl369_257 ),
inference(avatar_component_clause,[],[f15928]) ).
fof(f15930,plain,
( r2_hidden(sK72(sF368,sF366),sF368)
| ~ spl369_257 ),
inference(avatar_component_clause,[],[f15928]) ).
fof(f15931,plain,
( spl369_257
| spl369_86
| spl369_223 ),
inference(avatar_split_clause,[],[f15924,f15745,f14427,f15928]) ).
fof(f15932,plain,
( ~ spl369_223
| ~ spl369_249
| ~ spl369_250
| ~ spl369_251
| ~ spl369_252
| ~ spl369_253
| ~ spl369_254
| ~ spl369_255
| ~ spl369_256
| ~ spl369_5
| ~ spl369_51
| spl369_248 ),
inference(avatar_split_clause,[],[f15918,f15879,f14040,f13755,f15914,f15910,f15906,f15902,f15898,f15894,f15890,f15886,f15745]) ).
fof(f15936,plain,
( k1_yellow21(sK72(sF368,sF366)) = k3_yellow21(sF365,sK72(sF368,sF366))
| ~ spl369_109
| ~ spl369_223 ),
inference(resolution,[],[f15746,f14609]) ).
fof(f15944,plain,
( l1_orders_2(k4_yellow21(sF365,sK72(sF368,sF366)))
| ~ spl369_170
| ~ spl369_223 ),
inference(resolution,[],[f15746,f15349]) ).
fof(f15945,plain,
( v2_lattice3(k4_yellow21(sF365,sK72(sF368,sF366)))
| ~ spl369_208
| ~ spl369_223 ),
inference(resolution,[],[f15746,f15664]) ).
fof(f15946,plain,
( spl369_203
| ~ spl369_170
| ~ spl369_223 ),
inference(avatar_split_clause,[],[f15944,f15745,f15348,f15598]) ).
fof(f15949,plain,
( sK72(sF368,sF366) = k1_yellow21(sK72(sF368,sF366))
| ~ m1_subset_1(sK72(sF368,sF366),u1_struct_0(sF365))
| v3_struct_0(sF365)
| ~ v2_altcat_1(sF365)
| ~ v11_altcat_1(sF365)
| ~ v12_altcat_1(sF365)
| ~ v2_yellow21(sF365)
| ~ l2_altcat_1(sF365)
| ~ spl369_109
| ~ spl369_223 ),
inference(superposition,[],[f15936,f12454]) ).
fof(f15950,plain,
( v2_orders_2(k1_yellow21(sK72(sF368,sF366)))
| v3_struct_0(sF365)
| ~ v2_altcat_1(sF365)
| ~ v11_altcat_1(sF365)
| ~ v12_altcat_1(sF365)
| ~ v2_yellow21(sF365)
| ~ l2_altcat_1(sF365)
| ~ m1_subset_1(sK72(sF368,sF366),u1_struct_0(sF365))
| ~ spl369_109
| ~ spl369_223 ),
inference(superposition,[],[f12453,f15936]) ).
fof(f15951,plain,
( v1_lattice3(k1_yellow21(sK72(sF368,sF366)))
| v3_struct_0(sF365)
| ~ v2_altcat_1(sF365)
| ~ v11_altcat_1(sF365)
| ~ v12_altcat_1(sF365)
| ~ v2_yellow21(sF365)
| ~ l2_altcat_1(sF365)
| ~ m1_subset_1(sK72(sF368,sF366),u1_struct_0(sF365))
| ~ spl369_109
| ~ spl369_223 ),
inference(superposition,[],[f12450,f15936]) ).
fof(f15952,plain,
( v4_orders_2(k1_yellow21(sK72(sF368,sF366)))
| v3_struct_0(sF365)
| ~ v2_altcat_1(sF365)
| ~ v11_altcat_1(sF365)
| ~ v12_altcat_1(sF365)
| ~ v2_yellow21(sF365)
| ~ l2_altcat_1(sF365)
| ~ m1_subset_1(sK72(sF368,sF366),u1_struct_0(sF365))
| ~ spl369_109
| ~ spl369_223 ),
inference(superposition,[],[f12451,f15936]) ).
fof(f15953,plain,
( v3_orders_2(k1_yellow21(sK72(sF368,sF366)))
| v3_struct_0(sF365)
| ~ v2_altcat_1(sF365)
| ~ v11_altcat_1(sF365)
| ~ v12_altcat_1(sF365)
| ~ v2_yellow21(sF365)
| ~ l2_altcat_1(sF365)
| ~ m1_subset_1(sK72(sF368,sF366),u1_struct_0(sF365))
| ~ spl369_109
| ~ spl369_223 ),
inference(superposition,[],[f12452,f15936]) ).
fof(f15956,plain,
( ~ m1_subset_1(sK72(sF368,sF366),sF366)
| v3_orders_2(k1_yellow21(sK72(sF368,sF366)))
| v3_struct_0(sF365)
| ~ v2_altcat_1(sF365)
| ~ v11_altcat_1(sF365)
| ~ v12_altcat_1(sF365)
| ~ v2_yellow21(sF365)
| ~ l2_altcat_1(sF365)
| ~ spl369_109
| ~ spl369_223 ),
inference(forward_demodulation,[],[f15953,f13722]) ).
fof(f15957,plain,
( ~ m1_subset_1(sK72(sF368,sF366),sF366)
| v4_orders_2(k1_yellow21(sK72(sF368,sF366)))
| v3_struct_0(sF365)
| ~ v2_altcat_1(sF365)
| ~ v11_altcat_1(sF365)
| ~ v12_altcat_1(sF365)
| ~ v2_yellow21(sF365)
| ~ l2_altcat_1(sF365)
| ~ spl369_109
| ~ spl369_223 ),
inference(forward_demodulation,[],[f15952,f13722]) ).
fof(f15958,plain,
( ~ m1_subset_1(sK72(sF368,sF366),sF366)
| v1_lattice3(k1_yellow21(sK72(sF368,sF366)))
| v3_struct_0(sF365)
| ~ v2_altcat_1(sF365)
| ~ v11_altcat_1(sF365)
| ~ v12_altcat_1(sF365)
| ~ v2_yellow21(sF365)
| ~ l2_altcat_1(sF365)
| ~ spl369_109
| ~ spl369_223 ),
inference(forward_demodulation,[],[f15951,f13722]) ).
fof(f15959,plain,
( ~ m1_subset_1(sK72(sF368,sF366),sF366)
| v2_orders_2(k1_yellow21(sK72(sF368,sF366)))
| v3_struct_0(sF365)
| ~ v2_altcat_1(sF365)
| ~ v11_altcat_1(sF365)
| ~ v12_altcat_1(sF365)
| ~ v2_yellow21(sF365)
| ~ l2_altcat_1(sF365)
| ~ spl369_109
| ~ spl369_223 ),
inference(forward_demodulation,[],[f15950,f13722]) ).
fof(f15960,plain,
( ~ m1_subset_1(sK72(sF368,sF366),sF366)
| sK72(sF368,sF366) = k1_yellow21(sK72(sF368,sF366))
| v3_struct_0(sF365)
| ~ v2_altcat_1(sF365)
| ~ v11_altcat_1(sF365)
| ~ v12_altcat_1(sF365)
| ~ v2_yellow21(sF365)
| ~ l2_altcat_1(sF365)
| ~ spl369_109
| ~ spl369_223 ),
inference(forward_demodulation,[],[f15949,f13722]) ).
fof(f15962,definition,
( spl369_258
<=> sK72(sF368,sF366) = k1_yellow21(sK72(sF368,sF366)) ),
introduced(definition,[new_symbols(definition,[spl369_258])],[avatar_definition]) ).
fof(f15964,plain,
( sK72(sF368,sF366) = k1_yellow21(sK72(sF368,sF366))
| ~ spl369_258 ),
inference(avatar_component_clause,[],[f15962]) ).
fof(f15967,definition,
( spl369_259
<=> v3_orders_2(k1_yellow21(sK72(sF368,sF366))) ),
introduced(definition,[new_symbols(definition,[spl369_259])],[avatar_definition]) ).
fof(f15969,plain,
( v3_orders_2(k1_yellow21(sK72(sF368,sF366)))
| ~ spl369_259 ),
inference(avatar_component_clause,[],[f15967]) ).
fof(f15970,plain,
( ~ spl369_30
| ~ spl369_28
| ~ spl369_33
| ~ spl369_27
| ~ spl369_25
| spl369_2
| spl369_259
| ~ spl369_223
| ~ spl369_109
| ~ spl369_223 ),
inference(avatar_split_clause,[],[f15956,f15745,f14608,f15745,f15967,f13736,f13846,f13858,f13894,f13864,f13876]) ).
fof(f15972,definition,
( spl369_260
<=> v4_orders_2(k1_yellow21(sK72(sF368,sF366))) ),
introduced(definition,[new_symbols(definition,[spl369_260])],[avatar_definition]) ).
fof(f15974,plain,
( v4_orders_2(k1_yellow21(sK72(sF368,sF366)))
| ~ spl369_260 ),
inference(avatar_component_clause,[],[f15972]) ).
fof(f15975,plain,
( ~ spl369_30
| ~ spl369_28
| ~ spl369_33
| ~ spl369_27
| ~ spl369_25
| spl369_2
| spl369_260
| ~ spl369_223
| ~ spl369_109
| ~ spl369_223 ),
inference(avatar_split_clause,[],[f15957,f15745,f14608,f15745,f15972,f13736,f13846,f13858,f13894,f13864,f13876]) ).
fof(f15977,definition,
( spl369_261
<=> v1_lattice3(k1_yellow21(sK72(sF368,sF366))) ),
introduced(definition,[new_symbols(definition,[spl369_261])],[avatar_definition]) ).
fof(f15979,plain,
( v1_lattice3(k1_yellow21(sK72(sF368,sF366)))
| ~ spl369_261 ),
inference(avatar_component_clause,[],[f15977]) ).
fof(f15980,plain,
( ~ spl369_30
| ~ spl369_28
| ~ spl369_33
| ~ spl369_27
| ~ spl369_25
| spl369_2
| spl369_261
| ~ spl369_223
| ~ spl369_109
| ~ spl369_223 ),
inference(avatar_split_clause,[],[f15958,f15745,f14608,f15745,f15977,f13736,f13846,f13858,f13894,f13864,f13876]) ).
fof(f15982,definition,
( spl369_262
<=> v2_orders_2(k1_yellow21(sK72(sF368,sF366))) ),
introduced(definition,[new_symbols(definition,[spl369_262])],[avatar_definition]) ).
fof(f15984,plain,
( v2_orders_2(k1_yellow21(sK72(sF368,sF366)))
| ~ spl369_262 ),
inference(avatar_component_clause,[],[f15982]) ).
fof(f15985,plain,
( ~ spl369_30
| ~ spl369_28
| ~ spl369_33
| ~ spl369_27
| ~ spl369_25
| spl369_2
| spl369_262
| ~ spl369_223
| ~ spl369_109
| ~ spl369_223 ),
inference(avatar_split_clause,[],[f15959,f15745,f14608,f15745,f15982,f13736,f13846,f13858,f13894,f13864,f13876]) ).
fof(f15986,plain,
( ~ spl369_30
| ~ spl369_28
| ~ spl369_33
| ~ spl369_27
| ~ spl369_25
| spl369_2
| spl369_258
| ~ spl369_223
| ~ spl369_109
| ~ spl369_223 ),
inference(avatar_split_clause,[],[f15960,f15745,f14608,f15745,f15962,f13736,f13846,f13858,f13894,f13864,f13876]) ).
fof(f15989,plain,
( $false
| spl369_248
| ~ spl369_257 ),
inference(backward_subsumption_resolution,[],[f15919,f15930]) ).
fof(f15990,plain,
( v1_xboole_0(sF366)
| sF366 = sF368
| ~ m1_subset_1(sK72(sF368,sF366),sF366)
| ~ spl369_257 ),
inference(resolution,[],[f15930,f14269]) ).
fof(f15991,plain,
( l1_orders_2(k4_yellow21(sF367,sK72(sF368,sF366)))
| ~ spl369_169
| ~ spl369_257 ),
inference(resolution,[],[f15930,f15355]) ).
fof(f15993,plain,
( spl369_248
| ~ spl369_257 ),
inference(avatar_contradiction_clause,[],[f15989]) ).
fof(f15994,plain,
( spl369_204
| ~ spl369_169
| ~ spl369_257 ),
inference(avatar_split_clause,[],[f15991,f15928,f15344,f15602]) ).
fof(f15995,plain,
( ~ l1_orders_2(sK72(sF368,sF366))
| ~ v2_lattice3(sK72(sF368,sF366))
| ~ v1_lattice3(sK72(sF368,sF366))
| ~ v4_orders_2(sK72(sF368,sF366))
| ~ v3_orders_2(sK72(sF368,sF366))
| ~ v2_orders_2(sK72(sF368,sF366))
| v3_lattice3(sK72(sF368,sF366))
| ~ spl369_52
| ~ spl369_248 ),
inference(resolution,[],[f15880,f14058]) ).
fof(f15996,plain,
( v2_lattice3(k3_yellow21(sF367,sK72(sF368,sF366)))
| ~ spl369_104
| ~ spl369_248 ),
inference(resolution,[],[f15880,f14572]) ).
fof(f15997,plain,
( k1_yellow21(sK72(sF368,sF366)) = k3_yellow21(sF367,sK72(sF368,sF366))
| ~ spl369_108
| ~ spl369_248 ),
inference(resolution,[],[f15880,f14605]) ).
fof(f16004,plain,
( sK72(sF368,sF366) = k1_yellow21(sK72(sF368,sF366))
| ~ m1_subset_1(sK72(sF368,sF366),u1_struct_0(sF367))
| v3_struct_0(sF367)
| ~ v2_altcat_1(sF367)
| ~ v11_altcat_1(sF367)
| ~ v12_altcat_1(sF367)
| ~ v2_yellow21(sF367)
| ~ l2_altcat_1(sF367)
| ~ spl369_108
| ~ spl369_248 ),
inference(superposition,[],[f15997,f12454]) ).
fof(f16005,plain,
( v2_orders_2(k1_yellow21(sK72(sF368,sF366)))
| v3_struct_0(sF367)
| ~ v2_altcat_1(sF367)
| ~ v11_altcat_1(sF367)
| ~ v12_altcat_1(sF367)
| ~ v2_yellow21(sF367)
| ~ l2_altcat_1(sF367)
| ~ m1_subset_1(sK72(sF368,sF366),u1_struct_0(sF367))
| ~ spl369_108
| ~ spl369_248 ),
inference(superposition,[],[f12453,f15997]) ).
fof(f16006,plain,
( v1_lattice3(k1_yellow21(sK72(sF368,sF366)))
| v3_struct_0(sF367)
| ~ v2_altcat_1(sF367)
| ~ v11_altcat_1(sF367)
| ~ v12_altcat_1(sF367)
| ~ v2_yellow21(sF367)
| ~ l2_altcat_1(sF367)
| ~ m1_subset_1(sK72(sF368,sF366),u1_struct_0(sF367))
| ~ spl369_108
| ~ spl369_248 ),
inference(superposition,[],[f12450,f15997]) ).
fof(f16007,plain,
( v4_orders_2(k1_yellow21(sK72(sF368,sF366)))
| v3_struct_0(sF367)
| ~ v2_altcat_1(sF367)
| ~ v11_altcat_1(sF367)
| ~ v12_altcat_1(sF367)
| ~ v2_yellow21(sF367)
| ~ l2_altcat_1(sF367)
| ~ m1_subset_1(sK72(sF368,sF366),u1_struct_0(sF367))
| ~ spl369_108
| ~ spl369_248 ),
inference(superposition,[],[f12451,f15997]) ).
fof(f16008,plain,
( v3_orders_2(k1_yellow21(sK72(sF368,sF366)))
| v3_struct_0(sF367)
| ~ v2_altcat_1(sF367)
| ~ v11_altcat_1(sF367)
| ~ v12_altcat_1(sF367)
| ~ v2_yellow21(sF367)
| ~ l2_altcat_1(sF367)
| ~ m1_subset_1(sK72(sF368,sF366),u1_struct_0(sF367))
| ~ spl369_108
| ~ spl369_248 ),
inference(superposition,[],[f12452,f15997]) ).
fof(f16011,plain,
( ~ m1_subset_1(sK72(sF368,sF366),sF368)
| v3_orders_2(k1_yellow21(sK72(sF368,sF366)))
| v3_struct_0(sF367)
| ~ v2_altcat_1(sF367)
| ~ v11_altcat_1(sF367)
| ~ v12_altcat_1(sF367)
| ~ v2_yellow21(sF367)
| ~ l2_altcat_1(sF367)
| ~ spl369_108
| ~ spl369_248 ),
inference(forward_demodulation,[],[f16008,f13726]) ).
fof(f16012,plain,
( ~ m1_subset_1(sK72(sF368,sF366),sF368)
| v4_orders_2(k1_yellow21(sK72(sF368,sF366)))
| v3_struct_0(sF367)
| ~ v2_altcat_1(sF367)
| ~ v11_altcat_1(sF367)
| ~ v12_altcat_1(sF367)
| ~ v2_yellow21(sF367)
| ~ l2_altcat_1(sF367)
| ~ spl369_108
| ~ spl369_248 ),
inference(forward_demodulation,[],[f16007,f13726]) ).
fof(f16013,plain,
( ~ m1_subset_1(sK72(sF368,sF366),sF368)
| v1_lattice3(k1_yellow21(sK72(sF368,sF366)))
| v3_struct_0(sF367)
| ~ v2_altcat_1(sF367)
| ~ v11_altcat_1(sF367)
| ~ v12_altcat_1(sF367)
| ~ v2_yellow21(sF367)
| ~ l2_altcat_1(sF367)
| ~ spl369_108
| ~ spl369_248 ),
inference(forward_demodulation,[],[f16006,f13726]) ).
fof(f16014,plain,
( ~ m1_subset_1(sK72(sF368,sF366),sF368)
| v2_orders_2(k1_yellow21(sK72(sF368,sF366)))
| v3_struct_0(sF367)
| ~ v2_altcat_1(sF367)
| ~ v11_altcat_1(sF367)
| ~ v12_altcat_1(sF367)
| ~ v2_yellow21(sF367)
| ~ l2_altcat_1(sF367)
| ~ spl369_108
| ~ spl369_248 ),
inference(forward_demodulation,[],[f16005,f13726]) ).
fof(f16015,plain,
( ~ m1_subset_1(sK72(sF368,sF366),sF368)
| sK72(sF368,sF366) = k1_yellow21(sK72(sF368,sF366))
| v3_struct_0(sF367)
| ~ v2_altcat_1(sF367)
| ~ v11_altcat_1(sF367)
| ~ v12_altcat_1(sF367)
| ~ v2_yellow21(sF367)
| ~ l2_altcat_1(sF367)
| ~ spl369_108
| ~ spl369_248 ),
inference(forward_demodulation,[],[f16004,f13726]) ).
fof(f16017,plain,
( ~ spl369_32
| ~ spl369_31
| ~ spl369_34
| ~ spl369_29
| ~ spl369_26
| spl369_3
| spl369_259
| ~ spl369_248
| ~ spl369_108
| ~ spl369_248 ),
inference(avatar_split_clause,[],[f16011,f15879,f14604,f15879,f15967,f13742,f13852,f13870,f13900,f13882,f13888]) ).
fof(f16018,plain,
( ~ spl369_32
| ~ spl369_31
| ~ spl369_34
| ~ spl369_29
| ~ spl369_26
| spl369_3
| spl369_260
| ~ spl369_248
| ~ spl369_108
| ~ spl369_248 ),
inference(avatar_split_clause,[],[f16012,f15879,f14604,f15879,f15972,f13742,f13852,f13870,f13900,f13882,f13888]) ).
fof(f16019,plain,
( ~ spl369_32
| ~ spl369_31
| ~ spl369_34
| ~ spl369_29
| ~ spl369_26
| spl369_3
| spl369_261
| ~ spl369_248
| ~ spl369_108
| ~ spl369_248 ),
inference(avatar_split_clause,[],[f16013,f15879,f14604,f15879,f15977,f13742,f13852,f13870,f13900,f13882,f13888]) ).
fof(f16020,plain,
( ~ spl369_32
| ~ spl369_31
| ~ spl369_34
| ~ spl369_29
| ~ spl369_26
| spl369_3
| spl369_262
| ~ spl369_248
| ~ spl369_108
| ~ spl369_248 ),
inference(avatar_split_clause,[],[f16014,f15879,f14604,f15879,f15982,f13742,f13852,f13870,f13900,f13882,f13888]) ).
fof(f16021,plain,
( ~ spl369_32
| ~ spl369_31
| ~ spl369_34
| ~ spl369_29
| ~ spl369_26
| spl369_3
| spl369_258
| ~ spl369_248
| ~ spl369_108
| ~ spl369_248 ),
inference(avatar_split_clause,[],[f16015,f15879,f14604,f15879,f15962,f13742,f13852,f13870,f13900,f13882,f13888]) ).
fof(f16040,plain,
( l1_orders_2(k1_yellow21(sK72(sF368,sF366)))
| v3_struct_0(sF365)
| ~ v2_altcat_1(sF365)
| ~ v11_altcat_1(sF365)
| ~ v12_altcat_1(sF365)
| ~ v3_yellow21(sF365)
| ~ l2_altcat_1(sF365)
| ~ m1_subset_1(sK72(sF368,sF366),u1_struct_0(sF365))
| ~ spl369_203 ),
inference(superposition,[],[f15600,f12112]) ).
fof(f16041,plain,
( l1_orders_2(sK72(sF368,sF366))
| v3_struct_0(sF365)
| ~ v2_altcat_1(sF365)
| ~ v11_altcat_1(sF365)
| ~ v12_altcat_1(sF365)
| ~ v3_yellow21(sF365)
| ~ l2_altcat_1(sF365)
| ~ m1_subset_1(sK72(sF368,sF366),u1_struct_0(sF365))
| ~ spl369_203
| ~ spl369_258 ),
inference(forward_demodulation,[],[f16040,f15964]) ).
fof(f16051,plain,
( ~ m1_subset_1(sK72(sF368,sF366),sF366)
| l1_orders_2(sK72(sF368,sF366))
| v3_struct_0(sF365)
| ~ v2_altcat_1(sF365)
| ~ v11_altcat_1(sF365)
| ~ v12_altcat_1(sF365)
| ~ v3_yellow21(sF365)
| ~ l2_altcat_1(sF365)
| ~ spl369_203
| ~ spl369_258 ),
inference(forward_demodulation,[],[f16041,f13722]) ).
fof(f16070,plain,
( l1_orders_2(k1_yellow21(sK72(sF368,sF366)))
| v3_struct_0(sF367)
| ~ v2_altcat_1(sF367)
| ~ v11_altcat_1(sF367)
| ~ v12_altcat_1(sF367)
| ~ v3_yellow21(sF367)
| ~ l2_altcat_1(sF367)
| ~ m1_subset_1(sK72(sF368,sF366),u1_struct_0(sF367))
| ~ spl369_204 ),
inference(superposition,[],[f15604,f12112]) ).
fof(f16071,plain,
( l1_orders_2(sK72(sF368,sF366))
| v3_struct_0(sF367)
| ~ v2_altcat_1(sF367)
| ~ v11_altcat_1(sF367)
| ~ v12_altcat_1(sF367)
| ~ v3_yellow21(sF367)
| ~ l2_altcat_1(sF367)
| ~ m1_subset_1(sK72(sF368,sF366),u1_struct_0(sF367))
| ~ spl369_204
| ~ spl369_258 ),
inference(forward_demodulation,[],[f16070,f15964]) ).
fof(f16081,plain,
( ~ m1_subset_1(sK72(sF368,sF366),sF368)
| l1_orders_2(sK72(sF368,sF366))
| v3_struct_0(sF367)
| ~ v2_altcat_1(sF367)
| ~ v11_altcat_1(sF367)
| ~ v12_altcat_1(sF367)
| ~ v3_yellow21(sF367)
| ~ l2_altcat_1(sF367)
| ~ spl369_204
| ~ spl369_258 ),
inference(forward_demodulation,[],[f16071,f13726]) ).
fof(f16082,plain,
( ~ spl369_32
| ~ spl369_107
| ~ spl369_34
| ~ spl369_29
| ~ spl369_26
| spl369_3
| spl369_251
| ~ spl369_248
| ~ spl369_204
| ~ spl369_258 ),
inference(avatar_split_clause,[],[f16081,f15962,f15602,f15879,f15894,f13742,f13852,f13870,f13900,f14593,f13888]) ).
fof(f16169,plain,
( v3_orders_2(sK72(sF368,sF366))
| ~ spl369_258
| ~ spl369_259 ),
inference(forward_demodulation,[],[f15969,f15964]) ).
fof(f16170,plain,
( spl369_253
| ~ spl369_258
| ~ spl369_259 ),
inference(avatar_split_clause,[],[f16169,f15967,f15962,f15902]) ).
fof(f16723,definition,
( spl369_349
<=> v2_lattice3(k4_yellow21(sF365,sK72(sF368,sF366))) ),
introduced(definition,[new_symbols(definition,[spl369_349])],[avatar_definition]) ).
fof(f16725,plain,
( v2_lattice3(k4_yellow21(sF365,sK72(sF368,sF366)))
| ~ spl369_349 ),
inference(avatar_component_clause,[],[f16723]) ).
fof(f16786,plain,
( v2_lattice3(k1_yellow21(sK72(sF368,sF366)))
| v3_struct_0(sF365)
| ~ v2_altcat_1(sF365)
| ~ v11_altcat_1(sF365)
| ~ v12_altcat_1(sF365)
| ~ v3_yellow21(sF365)
| ~ l2_altcat_1(sF365)
| ~ m1_subset_1(sK72(sF368,sF366),u1_struct_0(sF365))
| ~ spl369_349 ),
inference(superposition,[],[f16725,f12112]) ).
fof(f16787,plain,
( v2_lattice3(sK72(sF368,sF366))
| v3_struct_0(sF365)
| ~ v2_altcat_1(sF365)
| ~ v11_altcat_1(sF365)
| ~ v12_altcat_1(sF365)
| ~ v3_yellow21(sF365)
| ~ l2_altcat_1(sF365)
| ~ m1_subset_1(sK72(sF368,sF366),u1_struct_0(sF365))
| ~ spl369_258
| ~ spl369_349 ),
inference(forward_demodulation,[],[f16786,f15964]) ).
fof(f16911,plain,
( ~ m1_subset_1(sK72(sF368,sF366),sF366)
| v2_lattice3(sK72(sF368,sF366))
| v3_struct_0(sF365)
| ~ v2_altcat_1(sF365)
| ~ v11_altcat_1(sF365)
| ~ v12_altcat_1(sF365)
| ~ v3_yellow21(sF365)
| ~ l2_altcat_1(sF365)
| ~ spl369_258
| ~ spl369_349 ),
inference(forward_demodulation,[],[f16787,f13722]) ).
fof(f17033,plain,
( v2_lattice3(k1_yellow21(sK72(sF368,sF366)))
| ~ spl369_104
| ~ spl369_108
| ~ spl369_248 ),
inference(forward_demodulation,[],[f15996,f15997]) ).
fof(f17034,plain,
( v2_lattice3(sK72(sF368,sF366))
| ~ spl369_104
| ~ spl369_108
| ~ spl369_248
| ~ spl369_258 ),
inference(forward_demodulation,[],[f17033,f15964]) ).
fof(f17035,plain,
( spl369_256
| ~ spl369_104
| ~ spl369_108
| ~ spl369_248
| ~ spl369_258 ),
inference(avatar_split_clause,[],[f17034,f15962,f15879,f14604,f14571,f15914]) ).
fof(f17036,plain,
( spl369_250
| ~ spl369_252
| ~ spl369_253
| ~ spl369_254
| ~ spl369_255
| ~ spl369_256
| ~ spl369_251
| ~ spl369_52
| ~ spl369_248 ),
inference(avatar_split_clause,[],[f15995,f15879,f14057,f15894,f15914,f15910,f15906,f15902,f15898,f15890]) ).
fof(f17037,plain,
( ! [X0] :
( ~ m1_subset_1(sK72(sF368,sF366),u1_struct_0(k4_waybel34(X0)))
| ~ v2_orders_2(sK72(sF368,sF366))
| ~ v3_orders_2(sK72(sF368,sF366))
| ~ v4_orders_2(sK72(sF368,sF366))
| ~ v1_lattice3(sK72(sF368,sF366))
| v1_orders_2(sK72(sF368,sF366))
| ~ l1_orders_2(sK72(sF368,sF366))
| v2_setfam_1(X0) )
| ~ spl369_256 ),
inference(resolution,[],[f15915,f11889]) ).
fof(f17038,plain,
( ! [X0] :
( ~ m1_subset_1(sK72(sF368,sF366),u1_struct_0(k5_waybel34(X0)))
| ~ v2_orders_2(sK72(sF368,sF366))
| ~ v3_orders_2(sK72(sF368,sF366))
| ~ v4_orders_2(sK72(sF368,sF366))
| ~ v1_lattice3(sK72(sF368,sF366))
| v1_orders_2(sK72(sF368,sF366))
| ~ l1_orders_2(sK72(sF368,sF366))
| v2_setfam_1(X0) )
| ~ spl369_256 ),
inference(resolution,[],[f15915,f11955]) ).
fof(f17103,definition,
( spl369_411
<=> ! [X0] :
( ~ m1_subset_1(sK72(sF368,sF366),u1_struct_0(k5_waybel34(X0)))
| v2_setfam_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl369_411])],[avatar_definition]) ).
fof(f17104,plain,
( ! [X0] :
( v2_setfam_1(X0)
| ~ m1_subset_1(sK72(sF368,sF366),u1_struct_0(k5_waybel34(X0))) )
| ~ spl369_411 ),
inference(avatar_component_clause,[],[f17103]) ).
fof(f17105,plain,
( ~ spl369_251
| spl369_249
| ~ spl369_255
| ~ spl369_254
| ~ spl369_253
| ~ spl369_252
| spl369_411
| ~ spl369_256 ),
inference(avatar_split_clause,[],[f17038,f15914,f17103,f15898,f15902,f15906,f15910,f15886,f15894]) ).
fof(f17107,definition,
( spl369_412
<=> ! [X0] :
( ~ m1_subset_1(sK72(sF368,sF366),u1_struct_0(k4_waybel34(X0)))
| v2_setfam_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl369_412])],[avatar_definition]) ).
fof(f17108,plain,
( ! [X0] :
( v2_setfam_1(X0)
| ~ m1_subset_1(sK72(sF368,sF366),u1_struct_0(k4_waybel34(X0))) )
| ~ spl369_412 ),
inference(avatar_component_clause,[],[f17107]) ).
fof(f17109,plain,
( ~ spl369_251
| spl369_249
| ~ spl369_255
| ~ spl369_254
| ~ spl369_253
| ~ spl369_252
| spl369_412
| ~ spl369_256 ),
inference(avatar_split_clause,[],[f17037,f15914,f17107,f15898,f15902,f15906,f15910,f15886,f15894]) ).
fof(f17110,plain,
( v4_orders_2(sK72(sF368,sF366))
| ~ spl369_258
| ~ spl369_260 ),
inference(forward_demodulation,[],[f15974,f15964]) ).
fof(f17111,plain,
( spl369_254
| ~ spl369_258
| ~ spl369_260 ),
inference(avatar_split_clause,[],[f17110,f15972,f15962,f15906]) ).
fof(f17119,plain,
( v2_orders_2(sK72(sF368,sF366))
| ~ spl369_258
| ~ spl369_262 ),
inference(forward_demodulation,[],[f15984,f15964]) ).
fof(f17120,plain,
( spl369_252
| ~ spl369_258
| ~ spl369_262 ),
inference(avatar_split_clause,[],[f17119,f15982,f15962,f15898]) ).
fof(f17292,plain,
( v1_lattice3(sK72(sF368,sF366))
| ~ spl369_258
| ~ spl369_261 ),
inference(forward_demodulation,[],[f15979,f15964]) ).
fof(f17293,plain,
( spl369_255
| ~ spl369_258
| ~ spl369_261 ),
inference(avatar_split_clause,[],[f17292,f15977,f15962,f15910]) ).
fof(f17294,plain,
( ~ m1_subset_1(sK72(sF368,sF366),u1_struct_0(k4_waybel34(sK56)))
| spl369_4
| ~ spl369_412 ),
inference(resolution,[],[f17108,f13752]) ).
fof(f17295,plain,
( ~ m1_subset_1(sK72(sF368,sF366),u1_struct_0(sF365))
| spl369_4
| ~ spl369_412 ),
inference(forward_demodulation,[],[f17294,f13720]) ).
fof(f17296,plain,
( ~ m1_subset_1(sK72(sF368,sF366),sF366)
| spl369_4
| ~ spl369_412 ),
inference(forward_demodulation,[],[f17295,f13722]) ).
fof(f17297,plain,
( ~ m1_subset_1(sK72(sF368,sF366),u1_struct_0(k5_waybel34(sK56)))
| spl369_4
| ~ spl369_411 ),
inference(resolution,[],[f17104,f13752]) ).
fof(f17298,plain,
( ~ m1_subset_1(sK72(sF368,sF366),u1_struct_0(sF367))
| spl369_4
| ~ spl369_411 ),
inference(forward_demodulation,[],[f17297,f13724]) ).
fof(f17299,plain,
( ~ m1_subset_1(sK72(sF368,sF366),sF368)
| spl369_4
| ~ spl369_411 ),
inference(forward_demodulation,[],[f17298,f13726]) ).
fof(f17300,plain,
( ~ spl369_248
| spl369_4
| ~ spl369_411 ),
inference(avatar_split_clause,[],[f17299,f17103,f13751,f15879]) ).
fof(f17342,plain,
( ~ spl369_223
| spl369_86
| spl369_38
| ~ spl369_257 ),
inference(avatar_split_clause,[],[f15990,f15928,f13926,f14427,f15745]) ).
fof(f17351,plain,
( ~ spl369_223
| spl369_4
| ~ spl369_412 ),
inference(avatar_split_clause,[],[f17296,f17107,f13751,f15745]) ).
fof(f17359,plain,
( ~ l1_orders_2(sK72(sF368,sF366))
| ~ v2_lattice3(sK72(sF368,sF366))
| ~ v1_lattice3(sK72(sF368,sF366))
| ~ v4_orders_2(sK72(sF368,sF366))
| ~ v3_orders_2(sK72(sF368,sF366))
| ~ v2_orders_2(sK72(sF368,sF366))
| v3_lattice3(sK72(sF368,sF366))
| ~ spl369_41
| ~ spl369_223 ),
inference(resolution,[],[f15746,f13974]) ).
fof(f17374,plain,
( spl369_250
| ~ spl369_252
| ~ spl369_253
| ~ spl369_254
| ~ spl369_255
| ~ spl369_256
| ~ spl369_251
| ~ spl369_41
| ~ spl369_223 ),
inference(avatar_split_clause,[],[f17359,f15745,f13973,f15894,f15914,f15910,f15906,f15902,f15898,f15890]) ).
fof(f17480,plain,
( ~ l1_altcat_1(sF365)
| spl369_37 ),
inference(resolution,[],[f13924,f13319]) ).
fof(f17491,plain,
( ~ l2_altcat_1(sF365)
| spl369_37 ),
inference(resolution,[],[f17480,f13317]) ).
fof(f17492,plain,
( ~ spl369_30
| spl369_37 ),
inference(avatar_split_clause,[],[f17491,f13922,f13876]) ).
fof(f17505,plain,
( ~ m1_subset_1(sK72(sF368,sF366),sF368)
| v1_xboole_0(sF368)
| spl369_257 ),
inference(resolution,[],[f15929,f12032]) ).
fof(f17507,plain,
( spl369_36
| ~ spl369_248
| spl369_257 ),
inference(avatar_split_clause,[],[f17505,f15928,f15879,f13917]) ).
fof(f17509,plain,
( ~ spl369_30
| ~ spl369_102
| ~ spl369_33
| ~ spl369_27
| ~ spl369_25
| spl369_2
| spl369_256
| ~ spl369_223
| ~ spl369_258
| ~ spl369_349 ),
inference(avatar_split_clause,[],[f16911,f16723,f15962,f15745,f15914,f13736,f13846,f13858,f13894,f14539,f13876]) ).
fof(f17512,plain,
( spl369_349
| ~ spl369_208
| ~ spl369_223 ),
inference(avatar_split_clause,[],[f15945,f15745,f15663,f16723]) ).
fof(f17515,plain,
( ~ spl369_30
| ~ spl369_102
| ~ spl369_33
| ~ spl369_27
| ~ spl369_25
| spl369_2
| spl369_251
| ~ spl369_223
| ~ spl369_203
| ~ spl369_258 ),
inference(avatar_split_clause,[],[f16051,f15962,f15598,f15745,f15894,f13736,f13846,f13858,f13894,f14539,f13876]) ).
cnf(s1,plain,
( spl369_1
| ~ spl369_2 ),
inference(sat_conversion,[],[f13739]) ).
cnf(s2,plain,
( spl369_1
| ~ spl369_3 ),
inference(sat_conversion,[],[f13745]) ).
cnf(s3,plain,
~ spl369_1,
inference(sat_conversion,[],[f13747]) ).
cnf(s4,plain,
( spl369_4
| spl369_5 ),
inference(sat_conversion,[],[f13757]) ).
cnf(s7,plain,
( spl369_4
| spl369_22 ),
inference(sat_conversion,[],[f13831]) ).
cnf(s10,plain,
( spl369_1
| spl369_25 ),
inference(sat_conversion,[],[f13849]) ).
cnf(s11,plain,
( spl369_1
| spl369_26 ),
inference(sat_conversion,[],[f13855]) ).
cnf(s12,plain,
( spl369_1
| spl369_27 ),
inference(sat_conversion,[],[f13861]) ).
cnf(s13,plain,
( spl369_1
| spl369_28 ),
inference(sat_conversion,[],[f13867]) ).
cnf(s14,plain,
( spl369_1
| spl369_29 ),
inference(sat_conversion,[],[f13873]) ).
cnf(s15,plain,
( spl369_1
| spl369_30 ),
inference(sat_conversion,[],[f13879]) ).
cnf(s16,plain,
( spl369_1
| spl369_31 ),
inference(sat_conversion,[],[f13885]) ).
cnf(s17,plain,
( spl369_1
| spl369_32 ),
inference(sat_conversion,[],[f13891]) ).
cnf(s18,plain,
( spl369_1
| spl369_33 ),
inference(sat_conversion,[],[f13897]) ).
cnf(s19,plain,
( spl369_1
| spl369_34 ),
inference(sat_conversion,[],[f13903]) ).
cnf(s20,plain,
( spl369_3
| ~ spl369_35
| ~ spl369_36 ),
inference(sat_conversion,[],[f13920]) ).
cnf(s21,plain,
( spl369_2
| ~ spl369_37
| ~ spl369_38 ),
inference(sat_conversion,[],[f13929]) ).
cnf(s24,plain,
( ~ spl369_32
| spl369_35 ),
inference(sat_conversion,[],[f13956]) ).
cnf(s25,plain,
( spl369_4
| spl369_41 ),
inference(sat_conversion,[],[f13975]) ).
cnf(s27,plain,
( spl369_4
| spl369_50 ),
inference(sat_conversion,[],[f14020]) ).
cnf(s29,plain,
~ spl369_4,
inference(sat_conversion,[],[f14023]) ).
cnf(s30,plain,
( spl369_4
| spl369_51 ),
inference(sat_conversion,[],[f14042]) ).
cnf(s31,plain,
( spl369_4
| spl369_52 ),
inference(sat_conversion,[],[f14059]) ).
cnf(s46,plain,
( spl369_4
| spl369_76 ),
inference(sat_conversion,[],[f14265]) ).
cnf(s74,plain,
( spl369_4
| spl369_96 ),
inference(sat_conversion,[],[f14496]) ).
cnf(s79,plain,
( ~ spl369_76
| spl369_102 ),
inference(sat_conversion,[],[f14542]) ).
cnf(s81,plain,
( spl369_3
| ~ spl369_26
| ~ spl369_29
| ~ spl369_31
| ~ spl369_32
| ~ spl369_34
| spl369_104 ),
inference(sat_conversion,[],[f14573]) ).
cnf(s84,plain,
( ~ spl369_96
| spl369_107 ),
inference(sat_conversion,[],[f14596]) ).
cnf(s85,plain,
( spl369_3
| ~ spl369_26
| ~ spl369_29
| ~ spl369_31
| ~ spl369_32
| ~ spl369_34
| spl369_108 ),
inference(sat_conversion,[],[f14606]) ).
cnf(s86,plain,
( spl369_2
| ~ spl369_25
| ~ spl369_27
| ~ spl369_28
| ~ spl369_30
| ~ spl369_33
| spl369_109 ),
inference(sat_conversion,[],[f14610]) ).
cnf(s103,plain,
~ spl369_86,
inference(sat_conversion,[],[f14748]) ).
cnf(s136,plain,
( spl369_3
| ~ spl369_26
| ~ spl369_29
| ~ spl369_32
| ~ spl369_34
| ~ spl369_107
| spl369_169 ),
inference(sat_conversion,[],[f15346]) ).
cnf(s137,plain,
( spl369_2
| ~ spl369_25
| ~ spl369_27
| ~ spl369_30
| ~ spl369_33
| ~ spl369_102
| spl369_170 ),
inference(sat_conversion,[],[f15350]) ).
cnf(s168,plain,
( spl369_86
| ~ spl369_169
| ~ spl369_170
| spl369_203
| spl369_204 ),
inference(sat_conversion,[],[f15605]) ).
cnf(s174,plain,
( spl369_2
| ~ spl369_25
| ~ spl369_27
| ~ spl369_30
| ~ spl369_33
| ~ spl369_102
| spl369_208 ),
inference(sat_conversion,[],[f15665]) ).
cnf(s207,plain,
( ~ spl369_22
| ~ spl369_50
| spl369_223
| ~ spl369_248
| ~ spl369_249
| ~ spl369_250
| ~ spl369_251
| ~ spl369_252
| ~ spl369_253
| ~ spl369_254
| ~ spl369_255
| ~ spl369_256 ),
inference(sat_conversion,[],[f15917]) ).
cnf(s208,plain,
( spl369_86
| ~ spl369_170
| spl369_203
| spl369_248 ),
inference(sat_conversion,[],[f15923]) ).
cnf(s209,plain,
( spl369_86
| spl369_223
| spl369_257 ),
inference(sat_conversion,[],[f15931]) ).
cnf(s210,plain,
( ~ spl369_5
| ~ spl369_51
| ~ spl369_223
| spl369_248
| ~ spl369_249
| ~ spl369_250
| ~ spl369_251
| ~ spl369_252
| ~ spl369_253
| ~ spl369_254
| ~ spl369_255
| ~ spl369_256 ),
inference(sat_conversion,[],[f15932]) ).
cnf(s211,plain,
( ~ spl369_170
| spl369_203
| ~ spl369_223 ),
inference(sat_conversion,[],[f15946]) ).
cnf(s216,plain,
( ~ spl369_223
| ~ spl369_25
| ~ spl369_27
| ~ spl369_28
| ~ spl369_30
| ~ spl369_33
| ~ spl369_109
| spl369_2
| ~ spl369_223
| spl369_259 ),
inference(sat_conversion,[],[f15970]) ).
cnf(s217,plain,
( spl369_2
| ~ spl369_25
| ~ spl369_27
| ~ spl369_28
| ~ spl369_30
| ~ spl369_33
| ~ spl369_109
| ~ spl369_223
| spl369_259 ),
inference(rat,[],[s216]) ).
cnf(s218,plain,
( ~ spl369_223
| ~ spl369_25
| ~ spl369_27
| ~ spl369_28
| ~ spl369_30
| ~ spl369_33
| ~ spl369_109
| spl369_2
| ~ spl369_223
| spl369_260 ),
inference(sat_conversion,[],[f15975]) ).
cnf(s219,plain,
( spl369_2
| ~ spl369_25
| ~ spl369_27
| ~ spl369_28
| ~ spl369_30
| ~ spl369_33
| ~ spl369_109
| ~ spl369_223
| spl369_260 ),
inference(rat,[],[s218]) ).
cnf(s220,plain,
( ~ spl369_223
| ~ spl369_25
| ~ spl369_27
| ~ spl369_28
| ~ spl369_30
| ~ spl369_33
| ~ spl369_109
| spl369_2
| ~ spl369_223
| spl369_261 ),
inference(sat_conversion,[],[f15980]) ).
cnf(s221,plain,
( spl369_2
| ~ spl369_25
| ~ spl369_27
| ~ spl369_28
| ~ spl369_30
| ~ spl369_33
| ~ spl369_109
| ~ spl369_223
| spl369_261 ),
inference(rat,[],[s220]) ).
cnf(s222,plain,
( ~ spl369_223
| ~ spl369_25
| ~ spl369_27
| ~ spl369_28
| ~ spl369_30
| ~ spl369_33
| ~ spl369_109
| spl369_2
| ~ spl369_223
| spl369_262 ),
inference(sat_conversion,[],[f15985]) ).
cnf(s223,plain,
( spl369_2
| ~ spl369_25
| ~ spl369_27
| ~ spl369_28
| ~ spl369_30
| ~ spl369_33
| ~ spl369_109
| ~ spl369_223
| spl369_262 ),
inference(rat,[],[s222]) ).
cnf(s224,plain,
( ~ spl369_223
| ~ spl369_25
| ~ spl369_27
| ~ spl369_28
| ~ spl369_30
| ~ spl369_33
| ~ spl369_109
| spl369_2
| ~ spl369_223
| spl369_258 ),
inference(sat_conversion,[],[f15986]) ).
cnf(s225,plain,
( spl369_2
| ~ spl369_25
| ~ spl369_27
| ~ spl369_28
| ~ spl369_30
| ~ spl369_33
| ~ spl369_109
| ~ spl369_223
| spl369_258 ),
inference(rat,[],[s224]) ).
cnf(s226,plain,
( spl369_248
| ~ spl369_257 ),
inference(sat_conversion,[],[f15993]) ).
cnf(s227,plain,
( ~ spl369_169
| spl369_204
| ~ spl369_257 ),
inference(sat_conversion,[],[f15994]) ).
cnf(s231,plain,
( ~ spl369_248
| ~ spl369_26
| ~ spl369_29
| ~ spl369_31
| ~ spl369_32
| ~ spl369_34
| ~ spl369_108
| spl369_3
| ~ spl369_248
| spl369_259 ),
inference(sat_conversion,[],[f16017]) ).
cnf(s232,plain,
( spl369_3
| ~ spl369_26
| ~ spl369_29
| ~ spl369_31
| ~ spl369_32
| ~ spl369_34
| ~ spl369_108
| ~ spl369_248
| spl369_259 ),
inference(rat,[],[s231]) ).
cnf(s233,plain,
( ~ spl369_248
| ~ spl369_26
| ~ spl369_29
| ~ spl369_31
| ~ spl369_32
| ~ spl369_34
| ~ spl369_108
| spl369_3
| ~ spl369_248
| spl369_260 ),
inference(sat_conversion,[],[f16018]) ).
cnf(s234,plain,
( spl369_3
| ~ spl369_26
| ~ spl369_29
| ~ spl369_31
| ~ spl369_32
| ~ spl369_34
| ~ spl369_108
| ~ spl369_248
| spl369_260 ),
inference(rat,[],[s233]) ).
cnf(s235,plain,
( ~ spl369_248
| ~ spl369_26
| ~ spl369_29
| ~ spl369_31
| ~ spl369_32
| ~ spl369_34
| ~ spl369_108
| spl369_3
| ~ spl369_248
| spl369_261 ),
inference(sat_conversion,[],[f16019]) ).
cnf(s236,plain,
( spl369_3
| ~ spl369_26
| ~ spl369_29
| ~ spl369_31
| ~ spl369_32
| ~ spl369_34
| ~ spl369_108
| ~ spl369_248
| spl369_261 ),
inference(rat,[],[s235]) ).
cnf(s237,plain,
( ~ spl369_248
| ~ spl369_26
| ~ spl369_29
| ~ spl369_31
| ~ spl369_32
| ~ spl369_34
| ~ spl369_108
| spl369_3
| ~ spl369_248
| spl369_262 ),
inference(sat_conversion,[],[f16020]) ).
cnf(s238,plain,
( spl369_3
| ~ spl369_26
| ~ spl369_29
| ~ spl369_31
| ~ spl369_32
| ~ spl369_34
| ~ spl369_108
| ~ spl369_248
| spl369_262 ),
inference(rat,[],[s237]) ).
cnf(s239,plain,
( ~ spl369_248
| ~ spl369_26
| ~ spl369_29
| ~ spl369_31
| ~ spl369_32
| ~ spl369_34
| ~ spl369_108
| spl369_3
| ~ spl369_248
| spl369_258 ),
inference(sat_conversion,[],[f16021]) ).
cnf(s240,plain,
( spl369_3
| ~ spl369_26
| ~ spl369_29
| ~ spl369_31
| ~ spl369_32
| ~ spl369_34
| ~ spl369_108
| ~ spl369_248
| spl369_258 ),
inference(rat,[],[s239]) ).
cnf(s259,plain,
( spl369_3
| ~ spl369_26
| ~ spl369_29
| ~ spl369_32
| ~ spl369_34
| ~ spl369_107
| ~ spl369_204
| ~ spl369_248
| spl369_251
| ~ spl369_258 ),
inference(sat_conversion,[],[f16082]) ).
cnf(s271,plain,
( spl369_253
| ~ spl369_258
| ~ spl369_259 ),
inference(sat_conversion,[],[f16170]) ).
cnf(s428,plain,
( ~ spl369_104
| ~ spl369_108
| ~ spl369_248
| spl369_256
| ~ spl369_258 ),
inference(sat_conversion,[],[f17035]) ).
cnf(s429,plain,
( ~ spl369_52
| ~ spl369_248
| spl369_250
| ~ spl369_251
| ~ spl369_252
| ~ spl369_253
| ~ spl369_254
| ~ spl369_255
| ~ spl369_256 ),
inference(sat_conversion,[],[f17036]) ).
cnf(s438,plain,
( spl369_249
| ~ spl369_251
| ~ spl369_252
| ~ spl369_253
| ~ spl369_254
| ~ spl369_255
| ~ spl369_256
| spl369_411 ),
inference(sat_conversion,[],[f17105]) ).
cnf(s439,plain,
( spl369_249
| ~ spl369_251
| ~ spl369_252
| ~ spl369_253
| ~ spl369_254
| ~ spl369_255
| ~ spl369_256
| spl369_412 ),
inference(sat_conversion,[],[f17109]) ).
cnf(s440,plain,
( spl369_254
| ~ spl369_258
| ~ spl369_260 ),
inference(sat_conversion,[],[f17111]) ).
cnf(s442,plain,
( spl369_252
| ~ spl369_258
| ~ spl369_262 ),
inference(sat_conversion,[],[f17120]) ).
cnf(s472,plain,
( spl369_255
| ~ spl369_258
| ~ spl369_261 ),
inference(sat_conversion,[],[f17293]) ).
cnf(s473,plain,
( spl369_4
| ~ spl369_248
| ~ spl369_411 ),
inference(sat_conversion,[],[f17300]) ).
cnf(s484,plain,
( spl369_38
| spl369_86
| ~ spl369_223
| ~ spl369_257 ),
inference(sat_conversion,[],[f17342]) ).
cnf(s487,plain,
( spl369_4
| ~ spl369_223
| ~ spl369_412 ),
inference(sat_conversion,[],[f17351]) ).
cnf(s490,plain,
( ~ spl369_41
| ~ spl369_223
| spl369_250
| ~ spl369_251
| ~ spl369_252
| ~ spl369_253
| ~ spl369_254
| ~ spl369_255
| ~ spl369_256 ),
inference(sat_conversion,[],[f17374]) ).
cnf(s503,plain,
( ~ spl369_30
| spl369_37 ),
inference(sat_conversion,[],[f17492]) ).
cnf(s507,plain,
( spl369_36
| ~ spl369_248
| spl369_257 ),
inference(sat_conversion,[],[f17507]) ).
cnf(s508,plain,
( spl369_2
| ~ spl369_25
| ~ spl369_27
| ~ spl369_30
| ~ spl369_33
| ~ spl369_102
| ~ spl369_223
| spl369_256
| ~ spl369_258
| ~ spl369_349 ),
inference(sat_conversion,[],[f17509]) ).
cnf(s511,plain,
( ~ spl369_208
| ~ spl369_223
| spl369_349 ),
inference(sat_conversion,[],[f17512]) ).
cnf(s515,plain,
( spl369_2
| ~ spl369_25
| ~ spl369_27
| ~ spl369_30
| ~ spl369_33
| ~ spl369_102
| ~ spl369_203
| ~ spl369_223
| spl369_251
| ~ spl369_258 ),
inference(sat_conversion,[],[f17515]) ).
cnf(s519,plain,
spl369_96,
inference(rat,[],[s74,s29]) ).
cnf(s520,plain,
spl369_76,
inference(rat,[],[s46,s29]) ).
cnf(s521,plain,
spl369_52,
inference(rat,[],[s31,s29]) ).
cnf(s522,plain,
spl369_51,
inference(rat,[],[s30,s29]) ).
cnf(s524,plain,
spl369_107,
inference(rat,[],[s84,s519]) ).
cnf(s531,plain,
spl369_102,
inference(rat,[],[s79,s520]) ).
cnf(s537,plain,
spl369_50,
inference(rat,[],[s27,s29]) ).
cnf(s538,plain,
spl369_41,
inference(rat,[],[s25,s29]) ).
cnf(s539,plain,
spl369_22,
inference(rat,[],[s7,s29]) ).
cnf(s540,plain,
spl369_5,
inference(rat,[],[s4,s29]) ).
cnf(s545,plain,
spl369_34,
inference(rat,[],[s19,s3]) ).
cnf(s546,plain,
spl369_33,
inference(rat,[],[s18,s3]) ).
cnf(s547,plain,
spl369_32,
inference(rat,[],[s17,s3]) ).
cnf(s548,plain,
spl369_31,
inference(rat,[],[s16,s3]) ).
cnf(s549,plain,
spl369_30,
inference(rat,[],[s15,s3]) ).
cnf(s550,plain,
spl369_29,
inference(rat,[],[s14,s3]) ).
cnf(s551,plain,
spl369_28,
inference(rat,[],[s13,s3]) ).
cnf(s552,plain,
spl369_27,
inference(rat,[],[s12,s3]) ).
cnf(s553,plain,
spl369_26,
inference(rat,[],[s11,s3]) ).
cnf(s554,plain,
spl369_25,
inference(rat,[],[s10,s3]) ).
cnf(s557,plain,
spl369_35,
inference(rat,[],[s24,s547]) ).
cnf(s558,plain,
spl369_37,
inference(rat,[],[s503,s549]) ).
cnf(s565,plain,
~ spl369_3,
inference(rat,[],[s2,s3]) ).
cnf(s567,plain,
spl369_169,
inference(rat,[],[s136,s553,s524,s545,s547,s550,s565]) ).
cnf(s569,plain,
spl369_108,
inference(rat,[],[s85,s553,s545,s547,s548,s550,s565]) ).
cnf(s570,plain,
spl369_104,
inference(rat,[],[s81,s553,s545,s547,s548,s550,s565]) ).
cnf(s576,plain,
~ spl369_36,
inference(rat,[],[s20,s557,s565]) ).
cnf(s586,plain,
~ spl369_2,
inference(rat,[],[s1,s3]) ).
cnf(s587,plain,
spl369_208,
inference(rat,[],[s174,s554,s531,s546,s549,s552,s586]) ).
cnf(s588,plain,
spl369_170,
inference(rat,[],[s137,s554,s531,s546,s549,s552,s586]) ).
cnf(s592,plain,
spl369_109,
inference(rat,[],[s86,s554,s546,s549,s551,s552,s586]) ).
cnf(s599,plain,
~ spl369_38,
inference(rat,[],[s21,s558,s586]) ).
cnf(s610,plain,
spl369_203,
inference(rat,[],[s207,s438,s429,s259,s271,s440,s442,s472,s428,s232,s234,s236,s238,s240,s473,s168,s208,s211,s537,s539,s521,s550,s547,s545,s524,s553,s565,s569,s570,s548,s29,s103,s567,s588]) ).
cnf(s611,plain,
( spl369_223
| ~ spl369_204 ),
inference(rat,[],[s207,s438,s429,s259,s271,s440,s442,s472,s428,s232,s234,s236,s238,s240,s473,s226,s209,s537,s539,s521,s550,s547,s545,s524,s553,s565,s569,s570,s548,s29,s103]) ).
cnf(s612,plain,
~ spl369_223,
inference(rat,[],[s210,s439,s490,s515,s508,s271,s440,s442,s472,s507,s217,s219,s221,s223,s225,s484,s487,s511,s522,s540,s538,s552,s549,s546,s531,s554,s586,s610,s576,s551,s592,s103,s599,s29,s587]) ).
cnf(s613,plain,
spl369_257,
inference(rat,[],[s209,s103,s612]) ).
cnf(s614,plain,
~ spl369_204,
inference(rat,[],[s611,s612]) ).
cnf(s617,plain,
$false,
inference(rat,[],[s227,s567,s613,s614]) ).
fof(f17516,plain,
$false,
inference(avatar_sat_refutation,[],[s617]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT360+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.38 % Computer : n015.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Sun Sep 27 15:04:03 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.41 Running first-order theorem proving
% 0.10/0.41 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 10.84/2.97 % (1748360)Detected formulas, will run a generic FOF schedule.
% 10.84/2.97 % (1748371)dis-21_1_sil=8000:lcm=predicate:random_seed=2579381927:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2994 on theBenchmark for (2994ds/129Mi)
% 10.84/2.97 % (1748366)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=2137845733:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2994 on theBenchmark for (2994ds/134677Mi)
% 10.84/2.97 % (1748369)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1593956325:i=119:av=off:ss=axioms_2994 on theBenchmark for (2994ds/119Mi)
% 10.84/2.97 % (1748365)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=513665049:i=141193_2994 on theBenchmark for (2994ds/141193Mi)
% 10.84/2.97 % (1748368)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3934272705:i=109:sd=1:ins=1:gsp=on:ss=axioms_2994 on theBenchmark for (2994ds/109Mi)
% 10.84/2.97 % (1748367)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=4017918261:i=141695:sd=1:nm=32:gsp=on:ss=included_2994 on theBenchmark for (2994ds/141695Mi)
% 10.84/2.97 % (1748370)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2385715473:s2a=on:i=139:gtg=position_2994 on theBenchmark for (2994ds/139Mi)
% 10.84/2.97 % (1748371)Instruction limit reached!
% 10.84/2.97 % (1748371)------------------------------
% 10.84/2.97 % (1748371)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.84/2.97 % (1748371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.84/2.97 % (1748371)CaDiCaL version: 2.1.3
% 10.84/2.97 % (1748371)Termination reason: Instruction limit
% 10.84/2.97 % (1748371)Termination phase: Preprocessing 1
% 10.84/2.97 % (1748371)Time elapsed: 0.059 s
% 10.84/2.97 % (1748371)Peak memory usage: 100 MB
% 10.84/2.97 % (1748371)Instructions burned: 129 (million)
% 10.84/2.97 % (1748368)Refutation not found, incomplete strategy
% 10.84/2.97 % (1748368)------------------------------
% 10.84/2.97 % (1748368)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.84/2.97 % (1748368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.84/2.97 % (1748368)CaDiCaL version: 2.1.3
% 10.84/2.97 % (1748368)Termination reason: Refutation not found, incomplete strategy
% 10.84/2.97 % (1748368)Time elapsed: 0.059 s
% 10.84/2.97 % (1748368)Peak memory usage: 103 MB
% 10.84/2.97 % (1748368)Instructions burned: 76 (million)
% 10.84/2.97 % (1748370)Instruction limit reached!
% 10.84/2.97 % (1748370)------------------------------
% 10.84/2.97 % (1748370)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.84/2.97 % (1748370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.84/2.97 % (1748370)CaDiCaL version: 2.1.3
% 10.84/2.97 % (1748370)Termination reason: Instruction limit
% 10.84/2.97 % (1748370)Termination phase: Property scanning
% 10.84/2.97 % (1748370)Time elapsed: 0.060 s
% 10.84/2.97 % (1748370)Peak memory usage: 99 MB
% 10.84/2.97 % (1748370)Instructions burned: 140 (million)
% 10.84/2.97 % (1748369)Instruction limit reached!
% 10.84/2.97 % (1748369)------------------------------
% 10.84/2.97 % (1748369)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.84/2.97 % (1748369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.84/2.97 % (1748369)CaDiCaL version: 2.1.3
% 10.84/2.97 % (1748369)Termination reason: Instruction limit
% 10.84/2.97 % (1748369)Termination phase: Saturation
% 10.84/2.97 % (1748369)Time elapsed: 0.086 s
% 10.84/2.97 % (1748369)Peak memory usage: 103 MB
% 10.84/2.97 % (1748369)Instructions burned: 119 (million)
% 10.84/2.97 % (1748379)lrs+10_1_sil=8000:sp=occurrence:random_seed=1592201076:i=285:sd=3:ss=axioms:sgt=8_2992 on theBenchmark for (2992ds/285Mi)
% 10.84/2.97 % (1748380)lrs+10_1_sil=32000:urr=on:br=off:random_seed=532850437:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2992 on theBenchmark for (2992ds/157Mi)
% 10.84/2.97 % (1748381)lrs+1011_1_sil=32000:sp=occurrence:random_seed=599731056:i=325:sd=1:ss=axioms:sgt=32_2992 on theBenchmark for (2992ds/325Mi)
% 10.84/2.97 % (1748379)Instruction limit reached!
% 10.84/2.97 % (1748379)------------------------------
% 10.84/2.97 % (1748379)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.84/2.97 % (1748379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.79/4.25 % (1748379)CaDiCaL version: 2.1.3
% 20.79/4.25 % (1748379)Termination reason: Instruction limit
% 20.79/4.25 % (1748379)Termination phase: Saturation
% 20.79/4.25 % (1748379)Time elapsed: 0.110 s
% 20.79/4.25 % (1748379)Peak memory usage: 106 MB
% 20.79/4.25 % (1748379)Instructions burned: 289 (million)
% 20.79/4.25 % (1748380)Instruction limit reached!
% 20.79/4.25 % (1748380)------------------------------
% 20.79/4.25 % (1748380)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.79/4.25 % (1748380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.79/4.25 % (1748380)CaDiCaL version: 2.1.3
% 20.79/4.25 % (1748380)Termination reason: Instruction limit
% 20.79/4.25 % (1748380)Termination phase: SInE selection
% 20.79/4.25 % (1748380)Time elapsed: 0.072 s
% 20.79/4.25 % (1748380)Peak memory usage: 99 MB
% 20.79/4.25 % (1748380)Instructions burned: 158 (million)
% 20.79/4.25 % (1748368)------------------------------
% 20.79/4.25 % (1748368)------------------------------
% 20.79/4.25 % (1748385)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=3308689889:s2a=on:i=248:s2at=1.23:gtg=position_2990 on theBenchmark for (2990ds/248Mi)
% 20.79/4.25 % (1748385)Instruction limit reached!
% 20.79/4.25 % (1748385)------------------------------
% 20.79/4.25 % (1748385)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.79/4.25 % (1748385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.79/4.25 % (1748385)CaDiCaL version: 2.1.3
% 20.79/4.25 % (1748385)Termination reason: Instruction limit
% 20.79/4.25 % (1748385)Termination phase: Preprocessing 1
% 20.79/4.25 % (1748385)Time elapsed: 0.079 s
% 20.79/4.25 % (1748385)Peak memory usage: 100 MB
% 20.79/4.25 % (1748385)Instructions burned: 250 (million)
% 20.79/4.25 % (1748381)Instruction limit reached!
% 20.79/4.25 % (1748381)------------------------------
% 20.79/4.25 % (1748381)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.79/4.25 % (1748381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.79/4.25 % (1748381)CaDiCaL version: 2.1.3
% 20.79/4.25 % (1748381)Termination reason: Instruction limit
% 20.79/4.25 % (1748381)Termination phase: Saturation
% 20.79/4.25 % (1748381)Time elapsed: 0.200 s
% 20.79/4.25 % (1748381)Peak memory usage: 105 MB
% 20.79/4.25 % (1748381)Instructions burned: 326 (million)
% 20.79/4.25 % (1748386)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1097852100:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2990 on theBenchmark for (2990ds/294Mi)
% 20.79/4.25 % (1748387)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=570965599:i=2350_2989 on theBenchmark for (2989ds/2350Mi)
% 20.79/4.25 % (1748389)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=136145362:cts=off:i=113:fsr=off:ss=included:sgt=4_2989 on theBenchmark for (2989ds/113Mi)
% 20.79/4.25 % (1748389)Instruction limit reached!
% 20.79/4.25 % (1748389)------------------------------
% 20.79/4.25 % (1748389)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.79/4.25 % (1748389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.79/4.25 % (1748389)CaDiCaL version: 2.1.3
% 20.79/4.25 % (1748389)Termination reason: Instruction limit
% 20.79/4.25 % (1748389)Termination phase: Preprocessing 3
% 20.79/4.25 % (1748389)Time elapsed: 0.052 s
% 20.79/4.25 % (1748389)Peak memory usage: 102 MB
% 20.79/4.25 % (1748389)Instructions burned: 115 (million)
% 20.79/4.25 % (1748391)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=191317623:i=127:av=off:fsr=off:sup=off_2988 on theBenchmark for (2988ds/127Mi)
% 20.79/4.25 % (1748386)Instruction limit reached!
% 20.79/4.25 % (1748386)------------------------------
% 20.79/4.25 % (1748386)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.79/4.25 % (1748386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.79/4.25 % (1748386)CaDiCaL version: 2.1.3
% 20.79/4.25 % (1748386)Termination reason: Instruction limit
% 20.79/4.25 % (1748386)Termination phase: Saturation
% 20.79/4.25 % (1748386)Time elapsed: 0.187 s
% 20.79/4.25 % (1748386)Peak memory usage: 105 MB
% 20.79/4.25 % (1748386)Instructions burned: 295 (million)
% 20.79/4.25 % (1748394)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=4058329123:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2987 on theBenchmark for (2987ds/114Mi)
% 20.79/4.25 % (1748394)Instruction limit reached!
% 20.79/4.25 % (1748394)------------------------------
% 20.79/4.25 % (1748394)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.85/9.78 % (1748394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.85/9.78 % (1748394)CaDiCaL version: 2.1.3
% 59.85/9.78 % (1748394)Termination reason: Instruction limit
% 59.85/9.78 % (1748394)Termination phase: Property scanning
% 59.85/9.78 % (1748394)Time elapsed: 0.028 s
% 59.85/9.78 % (1748394)Peak memory usage: 99 MB
% 59.85/9.78 % (1748394)Instructions burned: 118 (million)
% 59.85/9.78 % (1748391)Instruction limit reached!
% 59.85/9.78 % (1748391)------------------------------
% 59.85/9.78 % (1748391)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.85/9.78 % (1748391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.85/9.78 % (1748391)CaDiCaL version: 2.1.3
% 59.85/9.78 % (1748391)Termination reason: Instruction limit
% 59.85/9.78 % (1748391)Termination phase: Preprocessing 2
% 59.85/9.78 % (1748391)Time elapsed: 0.109 s
% 59.85/9.78 % (1748391)Peak memory usage: 107 MB
% 59.85/9.78 % (1748391)Instructions burned: 127 (million)
% 59.85/9.78 % (1748398)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2796819425:i=437:sd=1:aac=none:ss=included_2986 on theBenchmark for (2986ds/437Mi)
% 59.85/9.78 % (1748396)lrs+10_1_sil=8000:sp=occurrence:random_seed=1393168454:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2986 on theBenchmark for (2986ds/907Mi)
% 59.85/9.78 % (1748399)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=455295571:i=5202:ss=axioms:sgt=16_2986 on theBenchmark for (2986ds/5202Mi)
% 59.85/9.78 % (1748398)Instruction limit reached!
% 59.85/9.78 % (1748398)------------------------------
% 59.85/9.78 % (1748398)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.85/9.78 % (1748398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.85/9.78 % (1748398)CaDiCaL version: 2.1.3
% 59.85/9.78 % (1748398)Termination reason: Instruction limit
% 59.85/9.78 % (1748398)Termination phase: Saturation
% 59.85/9.78 % (1748398)Time elapsed: 0.138 s
% 59.85/9.78 % (1748398)Peak memory usage: 106 MB
% 59.85/9.78 % (1748398)Instructions burned: 440 (million)
% 59.85/9.78 % (1748403)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1936015811:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2984 on theBenchmark for (2984ds/134Mi)
% 59.85/9.78 % (1748403)Instruction limit reached!
% 59.85/9.78 % (1748403)------------------------------
% 59.85/9.78 % (1748403)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.85/9.78 % (1748403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.85/9.78 % (1748403)CaDiCaL version: 2.1.3
% 59.85/9.78 % (1748403)Termination reason: Instruction limit
% 59.85/9.78 % (1748403)Termination phase: Property scanning
% 59.85/9.78 % (1748403)Time elapsed: 0.057 s
% 59.85/9.78 % (1748403)Peak memory usage: 103 MB
% 59.85/9.78 % (1748403)Instructions burned: 138 (million)
% 59.85/9.78 % (1748405)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=4177165158:st=8:i=592:sd=3:ep=RST:ss=axioms_2982 on theBenchmark for (2982ds/592Mi)
% 59.85/9.78 % (1748396)Instruction limit reached!
% 59.85/9.78 % (1748396)------------------------------
% 59.85/9.78 % (1748396)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.85/9.78 % (1748396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.85/9.78 % (1748396)CaDiCaL version: 2.1.3
% 59.85/9.78 % (1748396)Termination reason: Instruction limit
% 59.85/9.78 % (1748396)Termination phase: Saturation
% 59.85/9.78 % (1748396)Time elapsed: 0.529 s
% 59.85/9.78 % (1748396)Peak memory usage: 121 MB
% 59.85/9.78 % (1748396)Instructions burned: 907 (million)
% 59.85/9.78 % (1748405)Instruction limit reached!
% 59.85/9.78 % (1748405)------------------------------
% 59.85/9.78 % (1748405)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.85/9.78 % (1748405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.85/9.78 % (1748405)CaDiCaL version: 2.1.3
% 59.85/9.78 % (1748405)Termination reason: Instruction limit
% 59.85/9.78 % (1748405)Termination phase: Property scanning
% 59.85/9.78 % (1748405)Time elapsed: 0.212 s
% 59.85/9.78 % (1748405)Peak memory usage: 116 MB
% 59.85/9.78 % (1748405)Instructions burned: 592 (million)
% 59.85/9.78 % (1748407)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1051096384:st=3:i=13193:sd=3:ss=axioms_2980 on theBenchmark for (2980ds/13193Mi)
% 59.85/9.78 % (1748408)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=1124254726:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2979 on theBenchmark for (2979ds/125Mi)
% 78.97/12.46 % (1748408)Instruction limit reached!
% 78.97/12.46 % (1748408)------------------------------
% 78.97/12.46 % (1748408)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 78.97/12.46 % (1748408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.97/12.46 % (1748408)CaDiCaL version: 2.1.3
% 78.97/12.46 % (1748408)Termination reason: Instruction limit
% 78.97/12.46 % (1748408)Termination phase: Property scanning
% 78.97/12.46 % (1748408)Time elapsed: 0.028 s
% 78.97/12.46 % (1748408)Peak memory usage: 99 MB
% 78.97/12.46 % (1748408)Instructions burned: 125 (million)
% 78.97/12.46 % (1748411)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1436151856:i=134:gtgl=5:slsql=off:gtg=exists_sym_2978 on theBenchmark for (2978ds/134Mi)
% 78.97/12.46 % (1748411)Instruction limit reached!
% 78.97/12.46 % (1748411)------------------------------
% 78.97/12.46 % (1748411)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 78.97/12.46 % (1748411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.97/12.46 % (1748411)CaDiCaL version: 2.1.3
% 78.97/12.46 % (1748411)Termination reason: Instruction limit
% 78.97/12.46 % (1748411)Termination phase: Property scanning
% 78.97/12.46 % (1748411)Time elapsed: 0.060 s
% 78.97/12.46 % (1748411)Peak memory usage: 99 MB
% 78.97/12.46 % (1748411)Instructions burned: 136 (million)
% 78.97/12.46 % (1748413)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=930750311:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2976 on theBenchmark for (2976ds/141Mi)
% 78.97/12.46 % (1748413)Refutation not found, incomplete strategy
% 78.97/12.46 % (1748413)------------------------------
% 78.97/12.46 % (1748413)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 78.97/12.46 % (1748413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.97/12.46 % (1748413)CaDiCaL version: 2.1.3
% 78.97/12.46 % (1748413)Termination reason: Refutation not found, incomplete strategy
% 78.97/12.46 % (1748413)Time elapsed: 0.065 s
% 78.97/12.46 % (1748413)Peak memory usage: 103 MB
% 78.97/12.46 % (1748413)Instructions burned: 78 (million)
% 78.97/12.46 % (1748387)Instruction limit reached!
% 78.97/12.46 % (1748387)------------------------------
% 78.97/12.46 % (1748387)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 78.97/12.46 % (1748387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.97/12.46 % (1748387)CaDiCaL version: 2.1.3
% 78.97/12.46 % (1748387)Termination reason: Instruction limit
% 78.97/12.46 % (1748387)Termination phase: Saturation
% 78.97/12.46 % (1748387)Time elapsed: 1.569 s
% 78.97/12.46 % (1748387)Peak memory usage: 273 MB
% 78.97/12.46 % (1748387)Instructions burned: 2351 (million)
% 78.97/12.46 % (1748413)------------------------------
% 78.97/12.46 % (1748413)------------------------------
% 78.97/12.46 % (1748415)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1097163127:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2972 on theBenchmark for (2972ds/431Mi)
% 78.97/12.46 % (1748416)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=1194167230:i=6060:aac=none:ins=25_2971 on theBenchmark for (2971ds/6060Mi)
% 78.97/12.46 % (1748415)Instruction limit reached!
% 78.97/12.46 % (1748415)------------------------------
% 78.97/12.46 % (1748415)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 78.97/12.46 % (1748415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.97/12.46 % (1748415)CaDiCaL version: 2.1.3
% 78.97/12.46 % (1748415)Termination reason: Instruction limit
% 78.97/12.46 % (1748415)Termination phase: Saturation
% 78.97/12.46 % (1748415)Time elapsed: 0.268 s
% 78.97/12.46 % (1748415)Peak memory usage: 105 MB
% 78.97/12.46 % (1748415)Instructions burned: 432 (million)
% 78.97/12.46 % (1748419)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=3667061032:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2968 on theBenchmark for (2968ds/150Mi)
% 78.97/12.46 % (1748419)Instruction limit reached!
% 78.97/12.46 % (1748419)------------------------------
% 78.97/12.46 % (1748419)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 78.97/12.46 % (1748419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.21/16.07 % (1748419)CaDiCaL version: 2.1.3
% 44.21/16.07 % (1748419)Termination reason: Instruction limit
% 44.21/16.07 % (1748419)Termination phase: Unused predicate definition removal
% 44.21/16.07 % (1748419)Time elapsed: 0.121 s
% 44.21/16.07 % (1748419)Peak memory usage: 101 MB
% 44.21/16.07 % (1748419)Instructions burned: 150 (million)
% 44.21/16.07 % (1748421)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1799151583:i=14155:bd=all_2965 on theBenchmark for (2965ds/14155Mi)
% 44.21/16.07 % (1748399)Instruction limit reached!
% 44.21/16.07 % (1748399)------------------------------
% 44.21/16.07 % (1748399)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.21/16.07 % (1748399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.21/16.07 % (1748399)CaDiCaL version: 2.1.3
% 44.21/16.07 % (1748399)Termination reason: Instruction limit
% 44.21/16.07 % (1748399)Termination phase: Saturation
% 44.21/16.07 % (1748399)Time elapsed: 3.500 s
% 44.21/16.07 % (1748399)Peak memory usage: 390 MB
% 44.21/16.07 % (1748399)Instructions burned: 5204 (million)
% 44.21/16.07 % (1748423)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1203234235:i=667:av=off:fsr=off_2949 on theBenchmark for (2949ds/667Mi)
% 44.21/16.07 % (1748423)Instruction limit reached!
% 44.21/16.07 % (1748423)------------------------------
% 44.21/16.07 % (1748423)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.21/16.07 % (1748423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.21/16.07 % (1748423)CaDiCaL version: 2.1.3
% 44.21/16.07 % (1748423)Termination reason: Instruction limit
% 44.21/16.07 % (1748423)Termination phase: NewCNF
% 44.21/16.07 % (1748423)Time elapsed: 0.476 s
% 44.21/16.07 % (1748423)Peak memory usage: 128 MB
% 44.21/16.07 % (1748423)Instructions burned: 667 (million)
% 44.21/16.07 % (1748425)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=690629217:s2a=on:i=185:s2at=1.8:fdi=4_2943 on theBenchmark for (2943ds/185Mi)
% 44.21/16.07 % (1748425)Instruction limit reached!
% 44.21/16.07 % (1748425)------------------------------
% 44.21/16.07 % (1748425)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.21/16.07 % (1748425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.21/16.07 % (1748425)CaDiCaL version: 2.1.3
% 44.21/16.07 % (1748425)Termination reason: Instruction limit
% 44.21/16.07 % (1748425)Termination phase: Preprocessing 2
% 44.21/16.07 % (1748425)Time elapsed: 0.156 s
% 44.21/16.07 % (1748425)Peak memory usage: 102 MB
% 44.21/16.07 % (1748425)Instructions burned: 185 (million)
% 44.21/16.07 % (1748427)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=518421175:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2940 on theBenchmark for (2940ds/193Mi)
% 44.21/16.07 % (1748427)Instruction limit reached!
% 44.21/16.07 % (1748427)------------------------------
% 44.21/16.07 % (1748427)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.21/16.07 % (1748427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.21/16.07 % (1748427)CaDiCaL version: 2.1.3
% 44.21/16.07 % (1748427)Termination reason: Instruction limit
% 44.21/16.07 % (1748427)Termination phase: Saturation
% 44.21/16.07 % (1748427)Time elapsed: 0.150 s
% 44.21/16.07 % (1748427)Peak memory usage: 105 MB
% 44.21/16.07 % (1748427)Instructions burned: 194 (million)
% 44.21/16.07 % (1748429)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=4069221390:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2937 on theBenchmark for (2937ds/4850Mi)
% 44.21/16.07 % (1748416)Instruction limit reached!
% 44.21/16.07 % (1748416)------------------------------
% 44.21/16.07 % (1748416)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.21/16.07 % (1748416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.21/16.07 % (1748416)CaDiCaL version: 2.1.3
% 44.21/16.07 % (1748416)Termination reason: Instruction limit
% 44.21/16.07 % (1748416)Termination phase: Saturation
% 44.21/16.07 % (1748416)Time elapsed: 4.246 s
% 44.21/16.07 % (1748416)Peak memory usage: 363 MB
% 44.21/16.07 % (1748416)Instructions burned: 6061 (million)
% 44.21/16.07 % (1748431)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=3413791432:i=12111:sd=1:ss=included_2927 on theBenchmark for (2927ds/12111Mi)
% 44.21/16.07 % (1748407)Instruction limit reached!
% 44.21/16.07 % (1748407)------------------------------
% 44.21/16.07 % (1748407)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.21/16.07 % (1748407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.21/16.07 % (1748407)CaDiCaL version: 2.1.3
% 44.21/16.07 % (1748407)Termination reason: Instruction limit
% 44.21/16.07 % (1748407)Termination phase: Saturation
% 44.21/16.07 % (1748407)Time elapsed: 6.825 s
% 44.21/16.07 % (1748407)Peak memory usage: 230 MB
% 44.21/16.07 % (1748407)Instructions burned: 13195 (million)
% 44.21/16.07 % (1748429)Instruction limit reached!
% 44.21/16.07 % (1748429)------------------------------
% 44.21/16.07 % (1748429)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.21/16.07 % (1748429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.21/16.07 % (1748429)CaDiCaL version: 2.1.3
% 44.21/16.07 % (1748429)Termination reason: Instruction limit
% 44.21/16.07 % (1748429)Termination phase: Saturation
% 44.21/16.07 % (1748429)Time elapsed: 2.621 s
% 44.21/16.07 % (1748429)Peak memory usage: 165 MB
% 44.21/16.07 % (1748429)Instructions burned: 4850 (million)
% 44.21/16.07 % (1748433)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1023907077:i=319:kws=precedence:fsr=off_2910 on theBenchmark for (2910ds/319Mi)
% 44.21/16.07 % (1748434)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=123465582:i=2064:ep=RST_2909 on theBenchmark for (2909ds/2064Mi)
% 44.21/16.07 % (1748433)Instruction limit reached!
% 44.21/16.07 % (1748433)------------------------------
% 44.21/16.07 % (1748433)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.21/16.07 % (1748433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.21/16.07 % (1748433)CaDiCaL version: 2.1.3
% 44.21/16.07 % (1748433)Termination reason: Instruction limit
% 44.21/16.07 % (1748433)Termination phase: Preprocessing 3
% 44.21/16.07 % (1748433)Time elapsed: 0.221 s
% 44.21/16.07 % (1748433)Peak memory usage: 117 MB
% 44.21/16.07 % (1748433)Instructions burned: 319 (million)
% 44.21/16.07 % (1748437)dis-1011_128_sil=32000:random_seed=164685722:i=3706:ep=RST:av=off_2906 on theBenchmark for (2906ds/3706Mi)
% 44.21/16.07 % (1748434)Instruction limit reached!
% 44.21/16.07 % (1748434)------------------------------
% 44.21/16.07 % (1748434)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.21/16.07 % (1748434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.21/16.07 % (1748434)CaDiCaL version: 2.1.3
% 44.21/16.07 % (1748434)Termination reason: Instruction limit
% 44.21/16.07 % (1748434)Termination phase: Saturation
% 44.21/16.07 % (1748434)Time elapsed: 1.048 s
% 44.21/16.07 % (1748434)Peak memory usage: 153 MB
% 44.21/16.07 % (1748434)Instructions burned: 2064 (million)
% 44.21/16.07 % (1748439)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=3390063483:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2897 on theBenchmark for (2897ds/757Mi)
% 44.21/16.07 % (1748439)Refutation not found, incomplete strategy
% 44.21/16.07 % (1748439)------------------------------
% 44.21/16.07 % (1748439)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.21/16.07 % (1748439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.21/16.07 % (1748439)CaDiCaL version: 2.1.3
% 44.21/16.07 % (1748439)Termination reason: Refutation not found, incomplete strategy
% 44.21/16.07 % (1748439)Time elapsed: 0.150 s
% 44.21/16.07 % (1748439)Peak memory usage: 107 MB
% 44.21/16.07 % (1748439)Instructions burned: 261 (million)
% 44.21/16.07 % (1748439)------------------------------
% 44.21/16.07 % (1748439)------------------------------
% 44.21/16.07 % (1748441)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2443257476:i=13913:ss=axioms:sgt=8_2892 on theBenchmark for (2892ds/13913Mi)
% 44.21/16.07 % (1748437)Instruction limit reached!
% 44.21/16.07 % (1748437)------------------------------
% 44.21/16.07 % (1748437)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.21/16.07 % (1748437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.21/16.07 % (1748437)CaDiCaL version: 2.1.3
% 44.21/16.07 % (1748437)Termination reason: Instruction limit
% 44.21/16.07 % (1748437)Termination phase: Saturation
% 44.21/16.07 % (1748437)Time elapsed: 2.031 s
% 44.21/16.07 % (1748437)Peak memory usage: 160 MB
% 44.21/16.07 % (1748437)Instructions burned: 3706 (million)
% 44.21/16.07 % (1748443)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=1563271081:i=9925:aac=none_2885 on theBenchmark for (2885ds/9925Mi)
% 44.21/16.07 % (1748421)Instruction limit reached!
% 44.21/16.07 % (1748421)------------------------------
% 44.21/16.07 % (1748421)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.21/16.07 % (1748421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.21/16.07 % (1748421)CaDiCaL version: 2.1.3
% 44.21/16.07 % (1748421)Termination reason: Instruction limit
% 44.21/16.07 % (1748421)Termination phase: Saturation
% 44.21/16.07 % (1748421)Time elapsed: 8.751 s
% 44.21/16.07 % (1748421)Peak memory usage: 464 MB
% 44.21/16.07 % (1748421)Instructions burned: 14155 (million)
% 44.21/16.07 % (1748445)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=4130124306:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2876 on theBenchmark for (2876ds/2479Mi)
% 44.21/16.07 % (1748445)Refutation not found, incomplete strategy
% 44.21/16.07 % (1748445)------------------------------
% 44.21/16.07 % (1748445)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.21/16.07 % (1748445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.21/16.07 % (1748445)CaDiCaL version: 2.1.3
% 44.21/16.07 % (1748445)Termination reason: Refutation not found, incomplete strategy
% 44.21/16.07 % (1748445)Time elapsed: 0.121 s
% 44.21/16.07 % (1748445)Peak memory usage: 104 MB
% 44.21/16.07 % (1748445)Instructions burned: 152 (million)
% 44.21/16.07 % (1748445)------------------------------
% 44.21/16.07 % (1748445)------------------------------
% 44.21/16.07 % (1748447)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=905418416:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2871 on theBenchmark for (2871ds/440Mi)
% 44.21/16.07 % (1748447)Instruction limit reached!
% 44.21/16.07 % (1748447)------------------------------
% 44.21/16.07 % (1748447)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.21/16.07 % (1748447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.21/16.07 % (1748447)CaDiCaL version: 2.1.3
% 44.21/16.07 % (1748447)Termination reason: Instruction limit
% 44.21/16.07 % (1748447)Termination phase: Preprocessing 2
% 44.21/16.07 % (1748447)Time elapsed: 0.230 s
% 44.21/16.07 % (1748447)Peak memory usage: 103 MB
% 44.21/16.07 % (1748447)Instructions burned: 440 (million)
% 44.21/16.07 % (1748449)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=1493728819:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2867 on theBenchmark for (2867ds/11145Mi)
% 44.21/16.07 % (1748449)First to succeed.
% 44.21/16.07 % (1748449)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1748360"
% 44.21/16.07 % (1748449)Refutation found. Thanks to Tanya!
% 44.21/16.07 % SZS status Theorem for theBenchmark
% 44.21/16.07 % SZS output start Proof for theBenchmark
% See solution above
% 105.08/16.26 % (1748449)------------------------------
% 105.08/16.26 % (1748449)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 105.08/16.26 % (1748449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 105.08/16.26 % (1748449)CaDiCaL version: 2.1.3
% 105.08/16.26 % (1748449)Termination reason: Refutation
% 105.08/16.26 % (1748449)Time elapsed: 1.515 s
% 105.08/16.26 % (1748449)Peak memory usage: 170 MB
% 105.08/16.26 % (1748449)Instructions burned: 2270 (million)
% 105.08/16.26 % (1748449)------------------------------
% 105.08/16.26 % (1748449)------------------------------
% 105.08/16.26 % (1748360)Success in time 15.223 s
% 105.08/16.26 % Vampire exiting
%------------------------------------------------------------------------------