%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT374+3 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n016.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:28 AM UTC 2026
% Result : Theorem 27.94s 6.39s
% Output : Refutation 32.83s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 28
% Syntax : Number of formulae : 228 ( 32 unt; 16 def)
% Number of atoms : 1483 ( 102 equ)
% Maximal formula atoms : 36 ( 6 avg)
% Number of connectives : 1999 ( 744 ~; 878 |; 282 &)
% ( 40 <=>; 53 =>; 0 <=; 2 <~>)
% Maximal formula depth : 28 ( 7 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 47 ( 45 usr; 17 prp; 0-3 aty)
% Number of functors : 24 ( 24 usr; 3 con; 0-4 aty)
% Number of variables : 265 ( 0 sgn 221 !; 44 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f588,axiom,
! [X0] :
( ~ v2_setfam_1(X0)
=> ~ v1_xboole_0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc2_setfam_1) ).
fof(f14292,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l2_altcat_1(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& m1_altcat_2(X1,X0) )
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X1))
=> m1_subset_1(X2,u1_struct_0(X0)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t30_altcat_2) ).
fof(f18897,axiom,
! [X0] :
( ~ v1_xboole_0(X0)
=> ( ~ v3_struct_0(k5_waybel34(X0))
& v2_altcat_1(k5_waybel34(X0))
& v6_altcat_1(k5_waybel34(X0))
& v11_altcat_1(k5_waybel34(X0))
& v12_altcat_1(k5_waybel34(X0))
& v2_yellow21(k5_waybel34(X0))
& l2_altcat_1(k5_waybel34(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k5_waybel34) ).
fof(f18900,axiom,
! [X0] :
( ~ v1_xboole_0(X0)
=> ( ~ v3_struct_0(k8_waybel34(X0))
& v2_altcat_1(k8_waybel34(X0))
& v6_altcat_1(k8_waybel34(X0))
& v3_altcat_2(k8_waybel34(X0),k4_waybel34(X0))
& m1_altcat_2(k8_waybel34(X0),k4_waybel34(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k8_waybel34) ).
fof(f18901,axiom,
! [X0] :
( ~ v2_setfam_1(X0)
=> ( ~ v3_struct_0(k9_waybel34(X0))
& v2_altcat_1(k9_waybel34(X0))
& v6_altcat_1(k9_waybel34(X0))
& v3_altcat_2(k9_waybel34(X0),k5_waybel34(X0))
& m1_altcat_2(k9_waybel34(X0),k5_waybel34(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k9_waybel34) ).
fof(f18931,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/sandbox2/benchmark/theBenchmark.p',fc6_waybel34) ).
fof(f18934,axiom,
! [X0] :
( ~ v2_setfam_1(X0)
=> ! [X1] :
( ( v2_orders_2(X1)
& v3_orders_2(X1)
& v4_orders_2(X1)
& v1_lattice3(X1)
& v2_lattice3(X1)
& l1_orders_2(X1) )
=> ( m1_subset_1(X1,u1_struct_0(k5_waybel34(X0)))
<=> ( v1_orders_2(X1)
& v3_lattice3(X1)
& r2_hidden(u1_struct_0(X1),X0) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t15_waybel34) ).
fof(f18936,axiom,
! [X0] :
( ~ v2_setfam_1(X0)
=> u1_struct_0(k4_waybel34(X0)) = u1_struct_0(k5_waybel34(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t17_waybel34) ).
fof(f18971,axiom,
! [X0] :
( ~ v1_xboole_0(X0)
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v2_altcat_1(X1)
& v6_altcat_1(X1)
& v3_altcat_2(X1,k4_waybel34(X0))
& m1_altcat_2(X1,k4_waybel34(X0)) )
=> ( X1 = k8_waybel34(X0)
<=> ( ! [X2] :
( m1_subset_1(X2,u1_struct_0(k4_waybel34(X0)))
=> m1_subset_1(X2,u1_struct_0(X1)) )
& ! [X2] :
( m1_subset_1(X2,u1_struct_0(k4_waybel34(X0)))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(k4_waybel34(X0)))
=> ! [X4] :
( m1_subset_1(X4,u1_struct_0(X1))
=> ! [X5] :
( m1_subset_1(X5,u1_struct_0(X1))
=> ( ( X4 = X2
& X5 = X3 )
=> ( k1_altcat_1(k4_waybel34(X0),X2,X3) = k1_xboole_0
| ! [X6] :
( m1_subset_1(X6,k1_altcat_1(k4_waybel34(X0),X2,X3))
=> ( r2_hidden(X6,k1_altcat_1(X1,X4,X5))
<=> v22_waybel_0(k5_yellow21(k4_waybel34(X0),X2,X3,X6),k3_yellow21(k4_waybel34(X0),X2),k3_yellow21(k4_waybel34(X0),X3)) ) ) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d10_waybel34) ).
fof(f18972,axiom,
! [X0] :
( ~ v2_setfam_1(X0)
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v2_altcat_1(X1)
& v6_altcat_1(X1)
& v3_altcat_2(X1,k5_waybel34(X0))
& m1_altcat_2(X1,k5_waybel34(X0)) )
=> ( X1 = k9_waybel34(X0)
<=> ( ! [X2] :
( m1_subset_1(X2,u1_struct_0(k5_waybel34(X0)))
=> m1_subset_1(X2,u1_struct_0(X1)) )
& ! [X2] :
( m1_subset_1(X2,u1_struct_0(k5_waybel34(X0)))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(k5_waybel34(X0)))
=> ! [X4] :
( m1_subset_1(X4,u1_struct_0(X1))
=> ! [X5] :
( m1_subset_1(X5,u1_struct_0(X1))
=> ( ( X4 = X2
& X5 = X3 )
=> ( k1_altcat_1(k5_waybel34(X0),X2,X3) = k1_xboole_0
| ! [X6] :
( m1_subset_1(X6,k1_altcat_1(k5_waybel34(X0),X2,X3))
=> ( r2_hidden(X6,k1_altcat_1(X1,X4,X5))
<=> v22_waybel_0(k2_waybel34(k3_yellow21(k5_waybel34(X0),X3),k3_yellow21(k5_waybel34(X0),X2),k5_yellow21(k5_waybel34(X0),X2,X3,X6)),k3_yellow21(k5_waybel34(X0),X3),k3_yellow21(k5_waybel34(X0),X2)) ) ) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d11_waybel34) ).
fof(f18980,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(k8_waybel34(X0)))
<=> ( v1_orders_2(X1)
& v3_lattice3(X1)
& r2_hidden(u1_struct_0(X1),X0) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t47_waybel34) ).
fof(f18982,conjecture,
! [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(k9_waybel34(X0)))
<=> ( v1_orders_2(X1)
& v3_lattice3(X1)
& r2_hidden(u1_struct_0(X1),X0) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t49_waybel34) ).
fof(f18983,negated_conjecture,
~ ! [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(k9_waybel34(X0)))
<=> ( v1_orders_2(X1)
& v3_lattice3(X1)
& r2_hidden(u1_struct_0(X1),X0) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f18982]) ).
fof(f18989,plain,
! [X0] :
( ~ v1_xboole_0(X0)
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v2_altcat_1(X1)
& v6_altcat_1(X1)
& v3_altcat_2(X1,k4_waybel34(X0))
& m1_altcat_2(X1,k4_waybel34(X0)) )
=> ( X1 = k8_waybel34(X0)
<=> ( ! [X2] :
( m1_subset_1(X2,u1_struct_0(k4_waybel34(X0)))
=> m1_subset_1(X2,u1_struct_0(X1)) )
& ! [X3] :
( m1_subset_1(X3,u1_struct_0(k4_waybel34(X0)))
=> ! [X4] :
( m1_subset_1(X4,u1_struct_0(k4_waybel34(X0)))
=> ! [X5] :
( m1_subset_1(X5,u1_struct_0(X1))
=> ! [X6] :
( m1_subset_1(X6,u1_struct_0(X1))
=> ( ( X3 = X5
& X4 = X6 )
=> ( k1_xboole_0 = k1_altcat_1(k4_waybel34(X0),X3,X4)
| ! [X7] :
( m1_subset_1(X7,k1_altcat_1(k4_waybel34(X0),X3,X4))
=> ( r2_hidden(X7,k1_altcat_1(X1,X5,X6))
<=> v22_waybel_0(k5_yellow21(k4_waybel34(X0),X3,X4,X7),k3_yellow21(k4_waybel34(X0),X3),k3_yellow21(k4_waybel34(X0),X4)) ) ) ) ) ) ) ) ) ) ) ) ),
inference(rectify,[],[f18971]) ).
fof(f18990,plain,
! [X0] :
( ~ v2_setfam_1(X0)
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v2_altcat_1(X1)
& v6_altcat_1(X1)
& v3_altcat_2(X1,k5_waybel34(X0))
& m1_altcat_2(X1,k5_waybel34(X0)) )
=> ( X1 = k9_waybel34(X0)
<=> ( ! [X2] :
( m1_subset_1(X2,u1_struct_0(k5_waybel34(X0)))
=> m1_subset_1(X2,u1_struct_0(X1)) )
& ! [X3] :
( m1_subset_1(X3,u1_struct_0(k5_waybel34(X0)))
=> ! [X4] :
( m1_subset_1(X4,u1_struct_0(k5_waybel34(X0)))
=> ! [X5] :
( m1_subset_1(X5,u1_struct_0(X1))
=> ! [X6] :
( m1_subset_1(X6,u1_struct_0(X1))
=> ( ( X3 = X5
& X4 = X6 )
=> ( k1_xboole_0 = k1_altcat_1(k5_waybel34(X0),X3,X4)
| ! [X7] :
( m1_subset_1(X7,k1_altcat_1(k5_waybel34(X0),X3,X4))
=> ( r2_hidden(X7,k1_altcat_1(X1,X5,X6))
<=> v22_waybel_0(k2_waybel34(k3_yellow21(k5_waybel34(X0),X4),k3_yellow21(k5_waybel34(X0),X3),k5_yellow21(k5_waybel34(X0),X3,X4,X7)),k3_yellow21(k5_waybel34(X0),X4),k3_yellow21(k5_waybel34(X0),X3)) ) ) ) ) ) ) ) ) ) ) ) ),
inference(rectify,[],[f18972]) ).
fof(f19026,plain,
! [X0] :
( ( ~ v3_struct_0(k5_waybel34(X0))
& v2_altcat_1(k5_waybel34(X0))
& v6_altcat_1(k5_waybel34(X0))
& v11_altcat_1(k5_waybel34(X0))
& v12_altcat_1(k5_waybel34(X0))
& v2_yellow21(k5_waybel34(X0))
& l2_altcat_1(k5_waybel34(X0)) )
| v1_xboole_0(X0) ),
inference(ennf_transformation,[],[f18897]) ).
fof(f19029,plain,
! [X0] :
( ( ~ v3_struct_0(k8_waybel34(X0))
& v2_altcat_1(k8_waybel34(X0))
& v6_altcat_1(k8_waybel34(X0))
& v3_altcat_2(k8_waybel34(X0),k4_waybel34(X0))
& m1_altcat_2(k8_waybel34(X0),k4_waybel34(X0)) )
| v1_xboole_0(X0) ),
inference(ennf_transformation,[],[f18900]) ).
fof(f19030,plain,
! [X0] :
( ( ~ v3_struct_0(k9_waybel34(X0))
& v2_altcat_1(k9_waybel34(X0))
& v6_altcat_1(k9_waybel34(X0))
& v3_altcat_2(k9_waybel34(X0),k5_waybel34(X0))
& m1_altcat_2(k9_waybel34(X0),k5_waybel34(X0)) )
| v2_setfam_1(X0) ),
inference(ennf_transformation,[],[f18901]) ).
fof(f19086,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,[],[f18931]) ).
fof(f19090,plain,
! [X0] :
( ! [X1] :
( ( m1_subset_1(X1,u1_struct_0(k5_waybel34(X0)))
<=> ( v1_orders_2(X1)
& v3_lattice3(X1)
& r2_hidden(u1_struct_0(X1),X0) ) )
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ l1_orders_2(X1) )
| v2_setfam_1(X0) ),
inference(ennf_transformation,[],[f18934]) ).
fof(f19091,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,[],[f19090]) ).
fof(f19093,plain,
! [X0] :
( u1_struct_0(k4_waybel34(X0)) = u1_struct_0(k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(ennf_transformation,[],[f18936]) ).
fof(f19152,plain,
! [X0] :
( ! [X1] :
( ( X1 = k8_waybel34(X0)
<=> ( ! [X2] :
( m1_subset_1(X2,u1_struct_0(X1))
| ~ m1_subset_1(X2,u1_struct_0(k4_waybel34(X0))) )
& ! [X3] :
( ! [X4] :
( ! [X5] :
( ! [X6] :
( k1_xboole_0 = k1_altcat_1(k4_waybel34(X0),X3,X4)
| ! [X7] :
( ( r2_hidden(X7,k1_altcat_1(X1,X5,X6))
<=> v22_waybel_0(k5_yellow21(k4_waybel34(X0),X3,X4,X7),k3_yellow21(k4_waybel34(X0),X3),k3_yellow21(k4_waybel34(X0),X4)) )
| ~ m1_subset_1(X7,k1_altcat_1(k4_waybel34(X0),X3,X4)) )
| X3 != X5
| X4 != X6
| ~ m1_subset_1(X6,u1_struct_0(X1)) )
| ~ m1_subset_1(X5,u1_struct_0(X1)) )
| ~ m1_subset_1(X4,u1_struct_0(k4_waybel34(X0))) )
| ~ m1_subset_1(X3,u1_struct_0(k4_waybel34(X0))) ) ) )
| v3_struct_0(X1)
| ~ v2_altcat_1(X1)
| ~ v6_altcat_1(X1)
| ~ v3_altcat_2(X1,k4_waybel34(X0))
| ~ m1_altcat_2(X1,k4_waybel34(X0)) )
| v1_xboole_0(X0) ),
inference(ennf_transformation,[],[f18989]) ).
fof(f19153,plain,
! [X0] :
( ! [X1] :
( ( X1 = k8_waybel34(X0)
<=> ( ! [X2] :
( m1_subset_1(X2,u1_struct_0(X1))
| ~ m1_subset_1(X2,u1_struct_0(k4_waybel34(X0))) )
& ! [X3] :
( ! [X4] :
( ! [X5] :
( ! [X6] :
( k1_xboole_0 = k1_altcat_1(k4_waybel34(X0),X3,X4)
| ! [X7] :
( ( r2_hidden(X7,k1_altcat_1(X1,X5,X6))
<=> v22_waybel_0(k5_yellow21(k4_waybel34(X0),X3,X4,X7),k3_yellow21(k4_waybel34(X0),X3),k3_yellow21(k4_waybel34(X0),X4)) )
| ~ m1_subset_1(X7,k1_altcat_1(k4_waybel34(X0),X3,X4)) )
| X3 != X5
| X4 != X6
| ~ m1_subset_1(X6,u1_struct_0(X1)) )
| ~ m1_subset_1(X5,u1_struct_0(X1)) )
| ~ m1_subset_1(X4,u1_struct_0(k4_waybel34(X0))) )
| ~ m1_subset_1(X3,u1_struct_0(k4_waybel34(X0))) ) ) )
| v3_struct_0(X1)
| ~ v2_altcat_1(X1)
| ~ v6_altcat_1(X1)
| ~ v3_altcat_2(X1,k4_waybel34(X0))
| ~ m1_altcat_2(X1,k4_waybel34(X0)) )
| v1_xboole_0(X0) ),
inference(flattening,[],[f19152]) ).
fof(f19154,plain,
! [X0] :
( ! [X1] :
( ( X1 = k9_waybel34(X0)
<=> ( ! [X2] :
( m1_subset_1(X2,u1_struct_0(X1))
| ~ m1_subset_1(X2,u1_struct_0(k5_waybel34(X0))) )
& ! [X3] :
( ! [X4] :
( ! [X5] :
( ! [X6] :
( k1_xboole_0 = k1_altcat_1(k5_waybel34(X0),X3,X4)
| ! [X7] :
( ( r2_hidden(X7,k1_altcat_1(X1,X5,X6))
<=> v22_waybel_0(k2_waybel34(k3_yellow21(k5_waybel34(X0),X4),k3_yellow21(k5_waybel34(X0),X3),k5_yellow21(k5_waybel34(X0),X3,X4,X7)),k3_yellow21(k5_waybel34(X0),X4),k3_yellow21(k5_waybel34(X0),X3)) )
| ~ m1_subset_1(X7,k1_altcat_1(k5_waybel34(X0),X3,X4)) )
| X3 != X5
| X4 != X6
| ~ m1_subset_1(X6,u1_struct_0(X1)) )
| ~ m1_subset_1(X5,u1_struct_0(X1)) )
| ~ m1_subset_1(X4,u1_struct_0(k5_waybel34(X0))) )
| ~ m1_subset_1(X3,u1_struct_0(k5_waybel34(X0))) ) ) )
| v3_struct_0(X1)
| ~ v2_altcat_1(X1)
| ~ v6_altcat_1(X1)
| ~ v3_altcat_2(X1,k5_waybel34(X0))
| ~ m1_altcat_2(X1,k5_waybel34(X0)) )
| v2_setfam_1(X0) ),
inference(ennf_transformation,[],[f18990]) ).
fof(f19155,plain,
! [X0] :
( ! [X1] :
( ( X1 = k9_waybel34(X0)
<=> ( ! [X2] :
( m1_subset_1(X2,u1_struct_0(X1))
| ~ m1_subset_1(X2,u1_struct_0(k5_waybel34(X0))) )
& ! [X3] :
( ! [X4] :
( ! [X5] :
( ! [X6] :
( k1_xboole_0 = k1_altcat_1(k5_waybel34(X0),X3,X4)
| ! [X7] :
( ( r2_hidden(X7,k1_altcat_1(X1,X5,X6))
<=> v22_waybel_0(k2_waybel34(k3_yellow21(k5_waybel34(X0),X4),k3_yellow21(k5_waybel34(X0),X3),k5_yellow21(k5_waybel34(X0),X3,X4,X7)),k3_yellow21(k5_waybel34(X0),X4),k3_yellow21(k5_waybel34(X0),X3)) )
| ~ m1_subset_1(X7,k1_altcat_1(k5_waybel34(X0),X3,X4)) )
| X3 != X5
| X4 != X6
| ~ m1_subset_1(X6,u1_struct_0(X1)) )
| ~ m1_subset_1(X5,u1_struct_0(X1)) )
| ~ m1_subset_1(X4,u1_struct_0(k5_waybel34(X0))) )
| ~ m1_subset_1(X3,u1_struct_0(k5_waybel34(X0))) ) ) )
| v3_struct_0(X1)
| ~ v2_altcat_1(X1)
| ~ v6_altcat_1(X1)
| ~ v3_altcat_2(X1,k5_waybel34(X0))
| ~ m1_altcat_2(X1,k5_waybel34(X0)) )
| v2_setfam_1(X0) ),
inference(flattening,[],[f19154]) ).
fof(f19170,plain,
! [X0] :
( ! [X1] :
( ( m1_subset_1(X1,u1_struct_0(k8_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,[],[f18980]) ).
fof(f19171,plain,
! [X0] :
( ! [X1] :
( ( m1_subset_1(X1,u1_struct_0(k8_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,[],[f19170]) ).
fof(f19173,plain,
? [X0] :
( ? [X1] :
( ( m1_subset_1(X1,u1_struct_0(k9_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,[],[f18983]) ).
fof(f19174,plain,
? [X0] :
( ? [X1] :
( ( m1_subset_1(X1,u1_struct_0(k9_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,[],[f19173]) ).
fof(f19236,plain,
! [X0] :
( ~ v1_xboole_0(X0)
| v2_setfam_1(X0) ),
inference(ennf_transformation,[],[f588]) ).
fof(f19249,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ m1_altcat_2(X1,X0) )
| v3_struct_0(X0)
| ~ l2_altcat_1(X0) ),
inference(ennf_transformation,[],[f14292]) ).
fof(f19250,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ m1_altcat_2(X1,X0) )
| v3_struct_0(X0)
| ~ l2_altcat_1(X0) ),
inference(flattening,[],[f19249]) ).
fof(f20460,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,[],[f19091]) ).
fof(f20461,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,[],[f20460]) ).
fof(f20497,plain,
! [X0] :
( ! [X1] :
( ( ( X1 = k8_waybel34(X0)
| ? [X2] :
( ~ m1_subset_1(X2,u1_struct_0(X1))
& m1_subset_1(X2,u1_struct_0(k4_waybel34(X0))) )
| ? [X3] :
( ? [X4] :
( ? [X5] :
( ? [X6] :
( k1_xboole_0 != k1_altcat_1(k4_waybel34(X0),X3,X4)
& ? [X7] :
( ( ~ v22_waybel_0(k5_yellow21(k4_waybel34(X0),X3,X4,X7),k3_yellow21(k4_waybel34(X0),X3),k3_yellow21(k4_waybel34(X0),X4))
| ~ r2_hidden(X7,k1_altcat_1(X1,X5,X6)) )
& ( v22_waybel_0(k5_yellow21(k4_waybel34(X0),X3,X4,X7),k3_yellow21(k4_waybel34(X0),X3),k3_yellow21(k4_waybel34(X0),X4))
| r2_hidden(X7,k1_altcat_1(X1,X5,X6)) )
& m1_subset_1(X7,k1_altcat_1(k4_waybel34(X0),X3,X4)) )
& X3 = X5
& X4 = X6
& m1_subset_1(X6,u1_struct_0(X1)) )
& m1_subset_1(X5,u1_struct_0(X1)) )
& m1_subset_1(X4,u1_struct_0(k4_waybel34(X0))) )
& m1_subset_1(X3,u1_struct_0(k4_waybel34(X0))) ) )
& ( ( ! [X2] :
( m1_subset_1(X2,u1_struct_0(X1))
| ~ m1_subset_1(X2,u1_struct_0(k4_waybel34(X0))) )
& ! [X3] :
( ! [X4] :
( ! [X5] :
( ! [X6] :
( k1_xboole_0 = k1_altcat_1(k4_waybel34(X0),X3,X4)
| ! [X7] :
( ( ( r2_hidden(X7,k1_altcat_1(X1,X5,X6))
| ~ v22_waybel_0(k5_yellow21(k4_waybel34(X0),X3,X4,X7),k3_yellow21(k4_waybel34(X0),X3),k3_yellow21(k4_waybel34(X0),X4)) )
& ( v22_waybel_0(k5_yellow21(k4_waybel34(X0),X3,X4,X7),k3_yellow21(k4_waybel34(X0),X3),k3_yellow21(k4_waybel34(X0),X4))
| ~ r2_hidden(X7,k1_altcat_1(X1,X5,X6)) ) )
| ~ m1_subset_1(X7,k1_altcat_1(k4_waybel34(X0),X3,X4)) )
| X3 != X5
| X4 != X6
| ~ m1_subset_1(X6,u1_struct_0(X1)) )
| ~ m1_subset_1(X5,u1_struct_0(X1)) )
| ~ m1_subset_1(X4,u1_struct_0(k4_waybel34(X0))) )
| ~ m1_subset_1(X3,u1_struct_0(k4_waybel34(X0))) ) )
| k8_waybel34(X0) != X1 ) )
| v3_struct_0(X1)
| ~ v2_altcat_1(X1)
| ~ v6_altcat_1(X1)
| ~ v3_altcat_2(X1,k4_waybel34(X0))
| ~ m1_altcat_2(X1,k4_waybel34(X0)) )
| v1_xboole_0(X0) ),
inference(nnf_transformation,[],[f19153]) ).
fof(f20498,plain,
! [X0] :
( ! [X1] :
( ( ( X1 = k8_waybel34(X0)
| ? [X2] :
( ~ m1_subset_1(X2,u1_struct_0(X1))
& m1_subset_1(X2,u1_struct_0(k4_waybel34(X0))) )
| ? [X3] :
( ? [X4] :
( ? [X5] :
( ? [X6] :
( k1_xboole_0 != k1_altcat_1(k4_waybel34(X0),X3,X4)
& ? [X7] :
( ( ~ v22_waybel_0(k5_yellow21(k4_waybel34(X0),X3,X4,X7),k3_yellow21(k4_waybel34(X0),X3),k3_yellow21(k4_waybel34(X0),X4))
| ~ r2_hidden(X7,k1_altcat_1(X1,X5,X6)) )
& ( v22_waybel_0(k5_yellow21(k4_waybel34(X0),X3,X4,X7),k3_yellow21(k4_waybel34(X0),X3),k3_yellow21(k4_waybel34(X0),X4))
| r2_hidden(X7,k1_altcat_1(X1,X5,X6)) )
& m1_subset_1(X7,k1_altcat_1(k4_waybel34(X0),X3,X4)) )
& X3 = X5
& X4 = X6
& m1_subset_1(X6,u1_struct_0(X1)) )
& m1_subset_1(X5,u1_struct_0(X1)) )
& m1_subset_1(X4,u1_struct_0(k4_waybel34(X0))) )
& m1_subset_1(X3,u1_struct_0(k4_waybel34(X0))) ) )
& ( ( ! [X2] :
( m1_subset_1(X2,u1_struct_0(X1))
| ~ m1_subset_1(X2,u1_struct_0(k4_waybel34(X0))) )
& ! [X3] :
( ! [X4] :
( ! [X5] :
( ! [X6] :
( k1_xboole_0 = k1_altcat_1(k4_waybel34(X0),X3,X4)
| ! [X7] :
( ( ( r2_hidden(X7,k1_altcat_1(X1,X5,X6))
| ~ v22_waybel_0(k5_yellow21(k4_waybel34(X0),X3,X4,X7),k3_yellow21(k4_waybel34(X0),X3),k3_yellow21(k4_waybel34(X0),X4)) )
& ( v22_waybel_0(k5_yellow21(k4_waybel34(X0),X3,X4,X7),k3_yellow21(k4_waybel34(X0),X3),k3_yellow21(k4_waybel34(X0),X4))
| ~ r2_hidden(X7,k1_altcat_1(X1,X5,X6)) ) )
| ~ m1_subset_1(X7,k1_altcat_1(k4_waybel34(X0),X3,X4)) )
| X3 != X5
| X4 != X6
| ~ m1_subset_1(X6,u1_struct_0(X1)) )
| ~ m1_subset_1(X5,u1_struct_0(X1)) )
| ~ m1_subset_1(X4,u1_struct_0(k4_waybel34(X0))) )
| ~ m1_subset_1(X3,u1_struct_0(k4_waybel34(X0))) ) )
| k8_waybel34(X0) != X1 ) )
| v3_struct_0(X1)
| ~ v2_altcat_1(X1)
| ~ v6_altcat_1(X1)
| ~ v3_altcat_2(X1,k4_waybel34(X0))
| ~ m1_altcat_2(X1,k4_waybel34(X0)) )
| v1_xboole_0(X0) ),
inference(flattening,[],[f20497]) ).
fof(f20499,plain,
! [X0] :
( ! [X1] :
( ( ( X1 = k8_waybel34(X0)
| ? [X2] :
( ~ m1_subset_1(X2,u1_struct_0(X1))
& m1_subset_1(X2,u1_struct_0(k4_waybel34(X0))) )
| ? [X3] :
( ? [X4] :
( ? [X5] :
( ? [X6] :
( k1_xboole_0 != k1_altcat_1(k4_waybel34(X0),X3,X4)
& ? [X7] :
( ( ~ v22_waybel_0(k5_yellow21(k4_waybel34(X0),X3,X4,X7),k3_yellow21(k4_waybel34(X0),X3),k3_yellow21(k4_waybel34(X0),X4))
| ~ r2_hidden(X7,k1_altcat_1(X1,X5,X6)) )
& ( v22_waybel_0(k5_yellow21(k4_waybel34(X0),X3,X4,X7),k3_yellow21(k4_waybel34(X0),X3),k3_yellow21(k4_waybel34(X0),X4))
| r2_hidden(X7,k1_altcat_1(X1,X5,X6)) )
& m1_subset_1(X7,k1_altcat_1(k4_waybel34(X0),X3,X4)) )
& X3 = X5
& X4 = X6
& m1_subset_1(X6,u1_struct_0(X1)) )
& m1_subset_1(X5,u1_struct_0(X1)) )
& m1_subset_1(X4,u1_struct_0(k4_waybel34(X0))) )
& m1_subset_1(X3,u1_struct_0(k4_waybel34(X0))) ) )
& ( ( ! [X8] :
( m1_subset_1(X8,u1_struct_0(X1))
| ~ m1_subset_1(X8,u1_struct_0(k4_waybel34(X0))) )
& ! [X9] :
( ! [X10] :
( ! [X11] :
( ! [X12] :
( k1_xboole_0 = k1_altcat_1(k4_waybel34(X0),X9,X10)
| ! [X13] :
( ( ( r2_hidden(X13,k1_altcat_1(X1,X11,X12))
| ~ v22_waybel_0(k5_yellow21(k4_waybel34(X0),X9,X10,X13),k3_yellow21(k4_waybel34(X0),X9),k3_yellow21(k4_waybel34(X0),X10)) )
& ( v22_waybel_0(k5_yellow21(k4_waybel34(X0),X9,X10,X13),k3_yellow21(k4_waybel34(X0),X9),k3_yellow21(k4_waybel34(X0),X10))
| ~ r2_hidden(X13,k1_altcat_1(X1,X11,X12)) ) )
| ~ m1_subset_1(X13,k1_altcat_1(k4_waybel34(X0),X9,X10)) )
| X9 != X11
| X10 != X12
| ~ m1_subset_1(X12,u1_struct_0(X1)) )
| ~ m1_subset_1(X11,u1_struct_0(X1)) )
| ~ m1_subset_1(X10,u1_struct_0(k4_waybel34(X0))) )
| ~ m1_subset_1(X9,u1_struct_0(k4_waybel34(X0))) ) )
| k8_waybel34(X0) != X1 ) )
| v3_struct_0(X1)
| ~ v2_altcat_1(X1)
| ~ v6_altcat_1(X1)
| ~ v3_altcat_2(X1,k4_waybel34(X0))
| ~ m1_altcat_2(X1,k4_waybel34(X0)) )
| v1_xboole_0(X0) ),
inference(rectify,[],[f20498]) ).
fof(f20500,plain,
! [X0] :
( ! [X1] :
( ( ( X1 = k8_waybel34(X0)
| ( ~ m1_subset_1(sK38(X0,X1),u1_struct_0(X1))
& m1_subset_1(sK38(X0,X1),u1_struct_0(k4_waybel34(X0))) )
| ( k1_xboole_0 != k1_altcat_1(k4_waybel34(X0),sK39(X0,X1),sK40(X0,X1))
& ( ~ v22_waybel_0(k5_yellow21(k4_waybel34(X0),sK39(X0,X1),sK40(X0,X1),sK43(X0,X1)),k3_yellow21(k4_waybel34(X0),sK39(X0,X1)),k3_yellow21(k4_waybel34(X0),sK40(X0,X1)))
| ~ r2_hidden(sK43(X0,X1),k1_altcat_1(X1,sK41(X0,X1),sK42(X0,X1))) )
& ( v22_waybel_0(k5_yellow21(k4_waybel34(X0),sK39(X0,X1),sK40(X0,X1),sK43(X0,X1)),k3_yellow21(k4_waybel34(X0),sK39(X0,X1)),k3_yellow21(k4_waybel34(X0),sK40(X0,X1)))
| r2_hidden(sK43(X0,X1),k1_altcat_1(X1,sK41(X0,X1),sK42(X0,X1))) )
& m1_subset_1(sK43(X0,X1),k1_altcat_1(k4_waybel34(X0),sK39(X0,X1),sK40(X0,X1)))
& sK39(X0,X1) = sK41(X0,X1)
& sK40(X0,X1) = sK42(X0,X1)
& m1_subset_1(sK42(X0,X1),u1_struct_0(X1))
& m1_subset_1(sK41(X0,X1),u1_struct_0(X1))
& m1_subset_1(sK40(X0,X1),u1_struct_0(k4_waybel34(X0)))
& m1_subset_1(sK39(X0,X1),u1_struct_0(k4_waybel34(X0))) ) )
& ( ( ! [X8] :
( m1_subset_1(X8,u1_struct_0(X1))
| ~ m1_subset_1(X8,u1_struct_0(k4_waybel34(X0))) )
& ! [X9] :
( ! [X10] :
( ! [X11] :
( ! [X12] :
( k1_xboole_0 = k1_altcat_1(k4_waybel34(X0),X9,X10)
| ! [X13] :
( ( ( r2_hidden(X13,k1_altcat_1(X1,X11,X12))
| ~ v22_waybel_0(k5_yellow21(k4_waybel34(X0),X9,X10,X13),k3_yellow21(k4_waybel34(X0),X9),k3_yellow21(k4_waybel34(X0),X10)) )
& ( v22_waybel_0(k5_yellow21(k4_waybel34(X0),X9,X10,X13),k3_yellow21(k4_waybel34(X0),X9),k3_yellow21(k4_waybel34(X0),X10))
| ~ r2_hidden(X13,k1_altcat_1(X1,X11,X12)) ) )
| ~ m1_subset_1(X13,k1_altcat_1(k4_waybel34(X0),X9,X10)) )
| X9 != X11
| X10 != X12
| ~ m1_subset_1(X12,u1_struct_0(X1)) )
| ~ m1_subset_1(X11,u1_struct_0(X1)) )
| ~ m1_subset_1(X10,u1_struct_0(k4_waybel34(X0))) )
| ~ m1_subset_1(X9,u1_struct_0(k4_waybel34(X0))) ) )
| k8_waybel34(X0) != X1 ) )
| v3_struct_0(X1)
| ~ v2_altcat_1(X1)
| ~ v6_altcat_1(X1)
| ~ v3_altcat_2(X1,k4_waybel34(X0))
| ~ m1_altcat_2(X1,k4_waybel34(X0)) )
| v1_xboole_0(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK38,sK39,sK40,sK41,sK42,sK43]),skolemize(X2,sK38(X0,X1)),skolemize(X3,sK39(X0,X1)),skolemize(X4,sK40(X0,X1)),skolemize(X5,sK41(X0,X1)),skolemize(X6,sK42(X0,X1)),skolemize(X7,sK43(X0,X1))],[f20499]) ).
fof(f20501,plain,
! [X0] :
( ! [X1] :
( ( ( X1 = k9_waybel34(X0)
| ? [X2] :
( ~ m1_subset_1(X2,u1_struct_0(X1))
& m1_subset_1(X2,u1_struct_0(k5_waybel34(X0))) )
| ? [X3] :
( ? [X4] :
( ? [X5] :
( ? [X6] :
( k1_xboole_0 != k1_altcat_1(k5_waybel34(X0),X3,X4)
& ? [X7] :
( ( ~ v22_waybel_0(k2_waybel34(k3_yellow21(k5_waybel34(X0),X4),k3_yellow21(k5_waybel34(X0),X3),k5_yellow21(k5_waybel34(X0),X3,X4,X7)),k3_yellow21(k5_waybel34(X0),X4),k3_yellow21(k5_waybel34(X0),X3))
| ~ r2_hidden(X7,k1_altcat_1(X1,X5,X6)) )
& ( v22_waybel_0(k2_waybel34(k3_yellow21(k5_waybel34(X0),X4),k3_yellow21(k5_waybel34(X0),X3),k5_yellow21(k5_waybel34(X0),X3,X4,X7)),k3_yellow21(k5_waybel34(X0),X4),k3_yellow21(k5_waybel34(X0),X3))
| r2_hidden(X7,k1_altcat_1(X1,X5,X6)) )
& m1_subset_1(X7,k1_altcat_1(k5_waybel34(X0),X3,X4)) )
& X3 = X5
& X4 = X6
& m1_subset_1(X6,u1_struct_0(X1)) )
& m1_subset_1(X5,u1_struct_0(X1)) )
& m1_subset_1(X4,u1_struct_0(k5_waybel34(X0))) )
& m1_subset_1(X3,u1_struct_0(k5_waybel34(X0))) ) )
& ( ( ! [X2] :
( m1_subset_1(X2,u1_struct_0(X1))
| ~ m1_subset_1(X2,u1_struct_0(k5_waybel34(X0))) )
& ! [X3] :
( ! [X4] :
( ! [X5] :
( ! [X6] :
( k1_xboole_0 = k1_altcat_1(k5_waybel34(X0),X3,X4)
| ! [X7] :
( ( ( r2_hidden(X7,k1_altcat_1(X1,X5,X6))
| ~ v22_waybel_0(k2_waybel34(k3_yellow21(k5_waybel34(X0),X4),k3_yellow21(k5_waybel34(X0),X3),k5_yellow21(k5_waybel34(X0),X3,X4,X7)),k3_yellow21(k5_waybel34(X0),X4),k3_yellow21(k5_waybel34(X0),X3)) )
& ( v22_waybel_0(k2_waybel34(k3_yellow21(k5_waybel34(X0),X4),k3_yellow21(k5_waybel34(X0),X3),k5_yellow21(k5_waybel34(X0),X3,X4,X7)),k3_yellow21(k5_waybel34(X0),X4),k3_yellow21(k5_waybel34(X0),X3))
| ~ r2_hidden(X7,k1_altcat_1(X1,X5,X6)) ) )
| ~ m1_subset_1(X7,k1_altcat_1(k5_waybel34(X0),X3,X4)) )
| X3 != X5
| X4 != X6
| ~ m1_subset_1(X6,u1_struct_0(X1)) )
| ~ m1_subset_1(X5,u1_struct_0(X1)) )
| ~ m1_subset_1(X4,u1_struct_0(k5_waybel34(X0))) )
| ~ m1_subset_1(X3,u1_struct_0(k5_waybel34(X0))) ) )
| k9_waybel34(X0) != X1 ) )
| v3_struct_0(X1)
| ~ v2_altcat_1(X1)
| ~ v6_altcat_1(X1)
| ~ v3_altcat_2(X1,k5_waybel34(X0))
| ~ m1_altcat_2(X1,k5_waybel34(X0)) )
| v2_setfam_1(X0) ),
inference(nnf_transformation,[],[f19155]) ).
fof(f20502,plain,
! [X0] :
( ! [X1] :
( ( ( X1 = k9_waybel34(X0)
| ? [X2] :
( ~ m1_subset_1(X2,u1_struct_0(X1))
& m1_subset_1(X2,u1_struct_0(k5_waybel34(X0))) )
| ? [X3] :
( ? [X4] :
( ? [X5] :
( ? [X6] :
( k1_xboole_0 != k1_altcat_1(k5_waybel34(X0),X3,X4)
& ? [X7] :
( ( ~ v22_waybel_0(k2_waybel34(k3_yellow21(k5_waybel34(X0),X4),k3_yellow21(k5_waybel34(X0),X3),k5_yellow21(k5_waybel34(X0),X3,X4,X7)),k3_yellow21(k5_waybel34(X0),X4),k3_yellow21(k5_waybel34(X0),X3))
| ~ r2_hidden(X7,k1_altcat_1(X1,X5,X6)) )
& ( v22_waybel_0(k2_waybel34(k3_yellow21(k5_waybel34(X0),X4),k3_yellow21(k5_waybel34(X0),X3),k5_yellow21(k5_waybel34(X0),X3,X4,X7)),k3_yellow21(k5_waybel34(X0),X4),k3_yellow21(k5_waybel34(X0),X3))
| r2_hidden(X7,k1_altcat_1(X1,X5,X6)) )
& m1_subset_1(X7,k1_altcat_1(k5_waybel34(X0),X3,X4)) )
& X3 = X5
& X4 = X6
& m1_subset_1(X6,u1_struct_0(X1)) )
& m1_subset_1(X5,u1_struct_0(X1)) )
& m1_subset_1(X4,u1_struct_0(k5_waybel34(X0))) )
& m1_subset_1(X3,u1_struct_0(k5_waybel34(X0))) ) )
& ( ( ! [X2] :
( m1_subset_1(X2,u1_struct_0(X1))
| ~ m1_subset_1(X2,u1_struct_0(k5_waybel34(X0))) )
& ! [X3] :
( ! [X4] :
( ! [X5] :
( ! [X6] :
( k1_xboole_0 = k1_altcat_1(k5_waybel34(X0),X3,X4)
| ! [X7] :
( ( ( r2_hidden(X7,k1_altcat_1(X1,X5,X6))
| ~ v22_waybel_0(k2_waybel34(k3_yellow21(k5_waybel34(X0),X4),k3_yellow21(k5_waybel34(X0),X3),k5_yellow21(k5_waybel34(X0),X3,X4,X7)),k3_yellow21(k5_waybel34(X0),X4),k3_yellow21(k5_waybel34(X0),X3)) )
& ( v22_waybel_0(k2_waybel34(k3_yellow21(k5_waybel34(X0),X4),k3_yellow21(k5_waybel34(X0),X3),k5_yellow21(k5_waybel34(X0),X3,X4,X7)),k3_yellow21(k5_waybel34(X0),X4),k3_yellow21(k5_waybel34(X0),X3))
| ~ r2_hidden(X7,k1_altcat_1(X1,X5,X6)) ) )
| ~ m1_subset_1(X7,k1_altcat_1(k5_waybel34(X0),X3,X4)) )
| X3 != X5
| X4 != X6
| ~ m1_subset_1(X6,u1_struct_0(X1)) )
| ~ m1_subset_1(X5,u1_struct_0(X1)) )
| ~ m1_subset_1(X4,u1_struct_0(k5_waybel34(X0))) )
| ~ m1_subset_1(X3,u1_struct_0(k5_waybel34(X0))) ) )
| k9_waybel34(X0) != X1 ) )
| v3_struct_0(X1)
| ~ v2_altcat_1(X1)
| ~ v6_altcat_1(X1)
| ~ v3_altcat_2(X1,k5_waybel34(X0))
| ~ m1_altcat_2(X1,k5_waybel34(X0)) )
| v2_setfam_1(X0) ),
inference(flattening,[],[f20501]) ).
fof(f20503,plain,
! [X0] :
( ! [X1] :
( ( ( X1 = k9_waybel34(X0)
| ? [X2] :
( ~ m1_subset_1(X2,u1_struct_0(X1))
& m1_subset_1(X2,u1_struct_0(k5_waybel34(X0))) )
| ? [X3] :
( ? [X4] :
( ? [X5] :
( ? [X6] :
( k1_xboole_0 != k1_altcat_1(k5_waybel34(X0),X3,X4)
& ? [X7] :
( ( ~ v22_waybel_0(k2_waybel34(k3_yellow21(k5_waybel34(X0),X4),k3_yellow21(k5_waybel34(X0),X3),k5_yellow21(k5_waybel34(X0),X3,X4,X7)),k3_yellow21(k5_waybel34(X0),X4),k3_yellow21(k5_waybel34(X0),X3))
| ~ r2_hidden(X7,k1_altcat_1(X1,X5,X6)) )
& ( v22_waybel_0(k2_waybel34(k3_yellow21(k5_waybel34(X0),X4),k3_yellow21(k5_waybel34(X0),X3),k5_yellow21(k5_waybel34(X0),X3,X4,X7)),k3_yellow21(k5_waybel34(X0),X4),k3_yellow21(k5_waybel34(X0),X3))
| r2_hidden(X7,k1_altcat_1(X1,X5,X6)) )
& m1_subset_1(X7,k1_altcat_1(k5_waybel34(X0),X3,X4)) )
& X3 = X5
& X4 = X6
& m1_subset_1(X6,u1_struct_0(X1)) )
& m1_subset_1(X5,u1_struct_0(X1)) )
& m1_subset_1(X4,u1_struct_0(k5_waybel34(X0))) )
& m1_subset_1(X3,u1_struct_0(k5_waybel34(X0))) ) )
& ( ( ! [X8] :
( m1_subset_1(X8,u1_struct_0(X1))
| ~ m1_subset_1(X8,u1_struct_0(k5_waybel34(X0))) )
& ! [X9] :
( ! [X10] :
( ! [X11] :
( ! [X12] :
( k1_xboole_0 = k1_altcat_1(k5_waybel34(X0),X9,X10)
| ! [X13] :
( ( ( r2_hidden(X13,k1_altcat_1(X1,X11,X12))
| ~ v22_waybel_0(k2_waybel34(k3_yellow21(k5_waybel34(X0),X10),k3_yellow21(k5_waybel34(X0),X9),k5_yellow21(k5_waybel34(X0),X9,X10,X13)),k3_yellow21(k5_waybel34(X0),X10),k3_yellow21(k5_waybel34(X0),X9)) )
& ( v22_waybel_0(k2_waybel34(k3_yellow21(k5_waybel34(X0),X10),k3_yellow21(k5_waybel34(X0),X9),k5_yellow21(k5_waybel34(X0),X9,X10,X13)),k3_yellow21(k5_waybel34(X0),X10),k3_yellow21(k5_waybel34(X0),X9))
| ~ r2_hidden(X13,k1_altcat_1(X1,X11,X12)) ) )
| ~ m1_subset_1(X13,k1_altcat_1(k5_waybel34(X0),X9,X10)) )
| X9 != X11
| X10 != X12
| ~ m1_subset_1(X12,u1_struct_0(X1)) )
| ~ m1_subset_1(X11,u1_struct_0(X1)) )
| ~ m1_subset_1(X10,u1_struct_0(k5_waybel34(X0))) )
| ~ m1_subset_1(X9,u1_struct_0(k5_waybel34(X0))) ) )
| k9_waybel34(X0) != X1 ) )
| v3_struct_0(X1)
| ~ v2_altcat_1(X1)
| ~ v6_altcat_1(X1)
| ~ v3_altcat_2(X1,k5_waybel34(X0))
| ~ m1_altcat_2(X1,k5_waybel34(X0)) )
| v2_setfam_1(X0) ),
inference(rectify,[],[f20502]) ).
fof(f20504,plain,
! [X0] :
( ! [X1] :
( ( ( X1 = k9_waybel34(X0)
| ( ~ m1_subset_1(sK44(X0,X1),u1_struct_0(X1))
& m1_subset_1(sK44(X0,X1),u1_struct_0(k5_waybel34(X0))) )
| ( k1_xboole_0 != k1_altcat_1(k5_waybel34(X0),sK45(X0,X1),sK46(X0,X1))
& ( ~ v22_waybel_0(k2_waybel34(k3_yellow21(k5_waybel34(X0),sK46(X0,X1)),k3_yellow21(k5_waybel34(X0),sK45(X0,X1)),k5_yellow21(k5_waybel34(X0),sK45(X0,X1),sK46(X0,X1),sK49(X0,X1))),k3_yellow21(k5_waybel34(X0),sK46(X0,X1)),k3_yellow21(k5_waybel34(X0),sK45(X0,X1)))
| ~ r2_hidden(sK49(X0,X1),k1_altcat_1(X1,sK47(X0,X1),sK48(X0,X1))) )
& ( v22_waybel_0(k2_waybel34(k3_yellow21(k5_waybel34(X0),sK46(X0,X1)),k3_yellow21(k5_waybel34(X0),sK45(X0,X1)),k5_yellow21(k5_waybel34(X0),sK45(X0,X1),sK46(X0,X1),sK49(X0,X1))),k3_yellow21(k5_waybel34(X0),sK46(X0,X1)),k3_yellow21(k5_waybel34(X0),sK45(X0,X1)))
| r2_hidden(sK49(X0,X1),k1_altcat_1(X1,sK47(X0,X1),sK48(X0,X1))) )
& m1_subset_1(sK49(X0,X1),k1_altcat_1(k5_waybel34(X0),sK45(X0,X1),sK46(X0,X1)))
& sK45(X0,X1) = sK47(X0,X1)
& sK46(X0,X1) = sK48(X0,X1)
& m1_subset_1(sK48(X0,X1),u1_struct_0(X1))
& m1_subset_1(sK47(X0,X1),u1_struct_0(X1))
& m1_subset_1(sK46(X0,X1),u1_struct_0(k5_waybel34(X0)))
& m1_subset_1(sK45(X0,X1),u1_struct_0(k5_waybel34(X0))) ) )
& ( ( ! [X8] :
( m1_subset_1(X8,u1_struct_0(X1))
| ~ m1_subset_1(X8,u1_struct_0(k5_waybel34(X0))) )
& ! [X9] :
( ! [X10] :
( ! [X11] :
( ! [X12] :
( k1_xboole_0 = k1_altcat_1(k5_waybel34(X0),X9,X10)
| ! [X13] :
( ( ( r2_hidden(X13,k1_altcat_1(X1,X11,X12))
| ~ v22_waybel_0(k2_waybel34(k3_yellow21(k5_waybel34(X0),X10),k3_yellow21(k5_waybel34(X0),X9),k5_yellow21(k5_waybel34(X0),X9,X10,X13)),k3_yellow21(k5_waybel34(X0),X10),k3_yellow21(k5_waybel34(X0),X9)) )
& ( v22_waybel_0(k2_waybel34(k3_yellow21(k5_waybel34(X0),X10),k3_yellow21(k5_waybel34(X0),X9),k5_yellow21(k5_waybel34(X0),X9,X10,X13)),k3_yellow21(k5_waybel34(X0),X10),k3_yellow21(k5_waybel34(X0),X9))
| ~ r2_hidden(X13,k1_altcat_1(X1,X11,X12)) ) )
| ~ m1_subset_1(X13,k1_altcat_1(k5_waybel34(X0),X9,X10)) )
| X9 != X11
| X10 != X12
| ~ m1_subset_1(X12,u1_struct_0(X1)) )
| ~ m1_subset_1(X11,u1_struct_0(X1)) )
| ~ m1_subset_1(X10,u1_struct_0(k5_waybel34(X0))) )
| ~ m1_subset_1(X9,u1_struct_0(k5_waybel34(X0))) ) )
| k9_waybel34(X0) != X1 ) )
| v3_struct_0(X1)
| ~ v2_altcat_1(X1)
| ~ v6_altcat_1(X1)
| ~ v3_altcat_2(X1,k5_waybel34(X0))
| ~ m1_altcat_2(X1,k5_waybel34(X0)) )
| v2_setfam_1(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK44,sK45,sK46,sK47,sK48,sK49]),skolemize(X2,sK44(X0,X1)),skolemize(X3,sK45(X0,X1)),skolemize(X4,sK46(X0,X1)),skolemize(X5,sK47(X0,X1)),skolemize(X6,sK48(X0,X1)),skolemize(X7,sK49(X0,X1))],[f20503]) ).
fof(f20507,plain,
! [X0] :
( ! [X1] :
( ( ( m1_subset_1(X1,u1_struct_0(k8_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(k8_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,[],[f19171]) ).
fof(f20508,plain,
! [X0] :
( ! [X1] :
( ( ( m1_subset_1(X1,u1_struct_0(k8_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(k8_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,[],[f20507]) ).
fof(f20511,plain,
? [X0] :
( ? [X1] :
( ( ~ v1_orders_2(X1)
| ~ v3_lattice3(X1)
| ~ r2_hidden(u1_struct_0(X1),X0)
| ~ m1_subset_1(X1,u1_struct_0(k9_waybel34(X0))) )
& ( ( v1_orders_2(X1)
& v3_lattice3(X1)
& r2_hidden(u1_struct_0(X1),X0) )
| m1_subset_1(X1,u1_struct_0(k9_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,[],[f19174]) ).
fof(f20512,plain,
? [X0] :
( ? [X1] :
( ( ~ v1_orders_2(X1)
| ~ v3_lattice3(X1)
| ~ r2_hidden(u1_struct_0(X1),X0)
| ~ m1_subset_1(X1,u1_struct_0(k9_waybel34(X0))) )
& ( ( v1_orders_2(X1)
& v3_lattice3(X1)
& r2_hidden(u1_struct_0(X1),X0) )
| m1_subset_1(X1,u1_struct_0(k9_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,[],[f20511]) ).
fof(f20513,plain,
( ( ~ v1_orders_2(sK53)
| ~ v3_lattice3(sK53)
| ~ r2_hidden(u1_struct_0(sK53),sK52)
| ~ m1_subset_1(sK53,u1_struct_0(k9_waybel34(sK52))) )
& ( ( v1_orders_2(sK53)
& v3_lattice3(sK53)
& r2_hidden(u1_struct_0(sK53),sK52) )
| m1_subset_1(sK53,u1_struct_0(k9_waybel34(sK52))) )
& v2_orders_2(sK53)
& v3_orders_2(sK53)
& v4_orders_2(sK53)
& v1_lattice3(sK53)
& v2_lattice3(sK53)
& l1_orders_2(sK53)
& ~ v2_setfam_1(sK52) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK52,sK53]),skolemize(X0,sK52),skolemize(X1,sK53)],[f20512]) ).
fof(f20880,plain,
! [X0] :
( l2_altcat_1(k5_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f19026]) ).
fof(f20893,plain,
! [X0] :
( m1_altcat_2(k8_waybel34(X0),k4_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f19029]) ).
fof(f20894,plain,
! [X0] :
( v3_altcat_2(k8_waybel34(X0),k4_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f19029]) ).
fof(f20895,plain,
! [X0] :
( v6_altcat_1(k8_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f19029]) ).
fof(f20896,plain,
! [X0] :
( v2_altcat_1(k8_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f19029]) ).
fof(f20897,plain,
! [X0] :
( ~ v3_struct_0(k8_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f19029]) ).
fof(f20898,plain,
! [X0] :
( m1_altcat_2(k9_waybel34(X0),k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[],[f19030]) ).
fof(f20899,plain,
! [X0] :
( v3_altcat_2(k9_waybel34(X0),k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[],[f19030]) ).
fof(f20900,plain,
! [X0] :
( v6_altcat_1(k9_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[],[f19030]) ).
fof(f20901,plain,
! [X0] :
( v2_altcat_1(k9_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[],[f19030]) ).
fof(f20902,plain,
! [X0] :
( ~ v3_struct_0(k9_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[],[f19030]) ).
fof(f21073,plain,
! [X0] :
( ~ v3_struct_0(k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[],[f19086]) ).
fof(f21084,plain,
! [X0,X1] :
( v3_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)
| ~ v2_lattice3(X1)
| ~ l1_orders_2(X1)
| v2_setfam_1(X0) ),
inference(cnf_transformation,[],[f20461]) ).
fof(f21085,plain,
! [X0,X1] :
( v1_orders_2(X1)
| ~ m1_subset_1(X1,u1_struct_0(k5_waybel34(X0)))
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ l1_orders_2(X1)
| v2_setfam_1(X0) ),
inference(cnf_transformation,[],[f20461]) ).
fof(f21086,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,[],[f20461]) ).
fof(f21092,plain,
! [X0] :
( u1_struct_0(k4_waybel34(X0)) = u1_struct_0(k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[],[f19093]) ).
fof(f21245,plain,
! [X0,X1,X8] :
( m1_subset_1(X8,u1_struct_0(X1))
| ~ m1_subset_1(X8,u1_struct_0(k4_waybel34(X0)))
| k8_waybel34(X0) != X1
| v3_struct_0(X1)
| ~ v2_altcat_1(X1)
| ~ v6_altcat_1(X1)
| ~ v3_altcat_2(X1,k4_waybel34(X0))
| ~ m1_altcat_2(X1,k4_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f20500]) ).
fof(f21268,plain,
! [X0,X1,X8] :
( m1_subset_1(X8,u1_struct_0(X1))
| ~ m1_subset_1(X8,u1_struct_0(k5_waybel34(X0)))
| k9_waybel34(X0) != X1
| v3_struct_0(X1)
| ~ v2_altcat_1(X1)
| ~ v6_altcat_1(X1)
| ~ v3_altcat_2(X1,k5_waybel34(X0))
| ~ m1_altcat_2(X1,k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[],[f20504]) ).
fof(f21323,plain,
! [X0,X1] :
( r2_hidden(u1_struct_0(X1),X0)
| ~ m1_subset_1(X1,u1_struct_0(k8_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(cnf_transformation,[],[f20508]) ).
fof(f21333,plain,
~ v2_setfam_1(sK52),
inference(cnf_transformation,[],[f20513]) ).
fof(f21334,plain,
l1_orders_2(sK53),
inference(cnf_transformation,[],[f20513]) ).
fof(f21335,plain,
v2_lattice3(sK53),
inference(cnf_transformation,[],[f20513]) ).
fof(f21336,plain,
v1_lattice3(sK53),
inference(cnf_transformation,[],[f20513]) ).
fof(f21337,plain,
v4_orders_2(sK53),
inference(cnf_transformation,[],[f20513]) ).
fof(f21338,plain,
v3_orders_2(sK53),
inference(cnf_transformation,[],[f20513]) ).
fof(f21339,plain,
v2_orders_2(sK53),
inference(cnf_transformation,[],[f20513]) ).
fof(f21340,plain,
( r2_hidden(u1_struct_0(sK53),sK52)
| m1_subset_1(sK53,u1_struct_0(k9_waybel34(sK52))) ),
inference(cnf_transformation,[],[f20513]) ).
fof(f21341,plain,
( v3_lattice3(sK53)
| m1_subset_1(sK53,u1_struct_0(k9_waybel34(sK52))) ),
inference(cnf_transformation,[],[f20513]) ).
fof(f21342,plain,
( v1_orders_2(sK53)
| m1_subset_1(sK53,u1_struct_0(k9_waybel34(sK52))) ),
inference(cnf_transformation,[],[f20513]) ).
fof(f21343,plain,
( ~ v1_orders_2(sK53)
| ~ v3_lattice3(sK53)
| ~ r2_hidden(u1_struct_0(sK53),sK52)
| ~ m1_subset_1(sK53,u1_struct_0(k9_waybel34(sK52))) ),
inference(cnf_transformation,[],[f20513]) ).
fof(f21501,plain,
! [X0] :
( ~ v1_xboole_0(X0)
| v2_setfam_1(X0) ),
inference(cnf_transformation,[],[f19236]) ).
fof(f21515,plain,
! [X2,X0,X1] :
( m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X1))
| v3_struct_0(X1)
| ~ m1_altcat_2(X1,X0)
| v3_struct_0(X0)
| ~ l2_altcat_1(X0) ),
inference(cnf_transformation,[],[f19250]) ).
fof(f23393,plain,
! [X0,X8] :
( m1_subset_1(X8,u1_struct_0(k8_waybel34(X0)))
| ~ m1_subset_1(X8,u1_struct_0(k4_waybel34(X0)))
| v3_struct_0(k8_waybel34(X0))
| ~ v2_altcat_1(k8_waybel34(X0))
| ~ v6_altcat_1(k8_waybel34(X0))
| ~ v3_altcat_2(k8_waybel34(X0),k4_waybel34(X0))
| ~ m1_altcat_2(k8_waybel34(X0),k4_waybel34(X0))
| v1_xboole_0(X0) ),
inference(equality_resolution,[],[f21245]) ).
fof(f23400,plain,
! [X0,X8] :
( m1_subset_1(X8,u1_struct_0(k9_waybel34(X0)))
| ~ m1_subset_1(X8,u1_struct_0(k5_waybel34(X0)))
| v3_struct_0(k9_waybel34(X0))
| ~ v2_altcat_1(k9_waybel34(X0))
| ~ v6_altcat_1(k9_waybel34(X0))
| ~ v3_altcat_2(k9_waybel34(X0),k5_waybel34(X0))
| ~ m1_altcat_2(k9_waybel34(X0),k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(equality_resolution,[],[f21268]) ).
fof(f23671,definition,
( spl356_1
<=> m1_subset_1(sK53,u1_struct_0(k9_waybel34(sK52))) ),
introduced(definition,[new_symbols(definition,[spl356_1])],[avatar_definition]) ).
fof(f23672,plain,
( m1_subset_1(sK53,u1_struct_0(k9_waybel34(sK52)))
| ~ spl356_1 ),
inference(avatar_component_clause,[],[f23671]) ).
fof(f23673,plain,
( ~ m1_subset_1(sK53,u1_struct_0(k9_waybel34(sK52)))
| spl356_1 ),
inference(avatar_component_clause,[],[f23671]) ).
fof(f23675,definition,
( spl356_2
<=> r2_hidden(u1_struct_0(sK53),sK52) ),
introduced(definition,[new_symbols(definition,[spl356_2])],[avatar_definition]) ).
fof(f23677,plain,
( ~ r2_hidden(u1_struct_0(sK53),sK52)
| spl356_2 ),
inference(avatar_component_clause,[],[f23675]) ).
fof(f23679,definition,
( spl356_3
<=> v3_lattice3(sK53) ),
introduced(definition,[new_symbols(definition,[spl356_3])],[avatar_definition]) ).
fof(f23683,definition,
( spl356_4
<=> v1_orders_2(sK53) ),
introduced(definition,[new_symbols(definition,[spl356_4])],[avatar_definition]) ).
fof(f23685,plain,
( ~ v1_orders_2(sK53)
| spl356_4 ),
inference(avatar_component_clause,[],[f23683]) ).
fof(f23686,plain,
( ~ spl356_1
| ~ spl356_2
| ~ spl356_3
| ~ spl356_4 ),
inference(avatar_split_clause,[],[f21343,f23683,f23679,f23675,f23671]) ).
fof(f23687,plain,
( v1_orders_2(sK53)
| spl356_1 ),
inference(backward_subsumption_resolution,[],[f21342,f23673]) ).
fof(f23688,plain,
( v3_lattice3(sK53)
| spl356_1 ),
inference(backward_subsumption_resolution,[],[f21341,f23673]) ).
fof(f23689,plain,
( r2_hidden(u1_struct_0(sK53),sK52)
| spl356_1 ),
inference(backward_subsumption_resolution,[],[f21340,f23673]) ).
fof(f23690,plain,
( ~ m1_subset_1(sK53,u1_struct_0(k5_waybel34(sK52)))
| v3_struct_0(k9_waybel34(sK52))
| ~ v2_altcat_1(k9_waybel34(sK52))
| ~ v6_altcat_1(k9_waybel34(sK52))
| ~ v3_altcat_2(k9_waybel34(sK52),k5_waybel34(sK52))
| ~ m1_altcat_2(k9_waybel34(sK52),k5_waybel34(sK52))
| v2_setfam_1(sK52)
| spl356_1 ),
inference(resolution,[],[f23673,f23400]) ).
fof(f23743,plain,
( ~ m1_subset_1(sK53,u1_struct_0(k5_waybel34(sK52)))
| ~ v2_altcat_1(k9_waybel34(sK52))
| ~ v6_altcat_1(k9_waybel34(sK52))
| ~ v3_altcat_2(k9_waybel34(sK52),k5_waybel34(sK52))
| ~ m1_altcat_2(k9_waybel34(sK52),k5_waybel34(sK52))
| v2_setfam_1(sK52)
| spl356_1 ),
inference(forward_subsumption_resolution,[],[f23690,f20902]) ).
fof(f23746,plain,
( ~ m1_subset_1(sK53,u1_struct_0(k5_waybel34(sK52)))
| ~ v6_altcat_1(k9_waybel34(sK52))
| ~ v3_altcat_2(k9_waybel34(sK52),k5_waybel34(sK52))
| ~ m1_altcat_2(k9_waybel34(sK52),k5_waybel34(sK52))
| v2_setfam_1(sK52)
| spl356_1 ),
inference(forward_subsumption_resolution,[],[f23743,f20901]) ).
fof(f23749,plain,
( ~ m1_subset_1(sK53,u1_struct_0(k5_waybel34(sK52)))
| ~ v3_altcat_2(k9_waybel34(sK52),k5_waybel34(sK52))
| ~ m1_altcat_2(k9_waybel34(sK52),k5_waybel34(sK52))
| v2_setfam_1(sK52)
| spl356_1 ),
inference(forward_subsumption_resolution,[],[f23746,f20900]) ).
fof(f23752,plain,
( ~ m1_subset_1(sK53,u1_struct_0(k5_waybel34(sK52)))
| ~ m1_altcat_2(k9_waybel34(sK52),k5_waybel34(sK52))
| v2_setfam_1(sK52)
| spl356_1 ),
inference(forward_subsumption_resolution,[],[f23749,f20899]) ).
fof(f23755,plain,
( ~ m1_subset_1(sK53,u1_struct_0(k5_waybel34(sK52)))
| v2_setfam_1(sK52)
| spl356_1 ),
inference(forward_subsumption_resolution,[],[f23752,f20898]) ).
fof(f23758,plain,
( ~ m1_subset_1(sK53,u1_struct_0(k5_waybel34(sK52)))
| spl356_1 ),
inference(forward_subsumption_resolution,[],[f23755,f21333]) ).
fof(f23764,definition,
( spl356_5
<=> m1_subset_1(sK53,u1_struct_0(k5_waybel34(sK52))) ),
introduced(definition,[new_symbols(definition,[spl356_5])],[avatar_definition]) ).
fof(f23765,plain,
( m1_subset_1(sK53,u1_struct_0(k5_waybel34(sK52)))
| ~ spl356_5 ),
inference(avatar_component_clause,[],[f23764]) ).
fof(f23766,plain,
( ~ m1_subset_1(sK53,u1_struct_0(k5_waybel34(sK52)))
| spl356_5 ),
inference(avatar_component_clause,[],[f23764]) ).
fof(f23767,plain,
( ~ spl356_5
| spl356_1 ),
inference(avatar_split_clause,[],[f23758,f23671,f23764]) ).
fof(f23768,plain,
( ~ v1_orders_2(sK53)
| ~ v3_lattice3(sK53)
| ~ r2_hidden(u1_struct_0(sK53),sK52)
| ~ v2_orders_2(sK53)
| ~ v3_orders_2(sK53)
| ~ v4_orders_2(sK53)
| ~ v1_lattice3(sK53)
| ~ v2_lattice3(sK53)
| ~ l1_orders_2(sK53)
| v2_setfam_1(sK52)
| spl356_5 ),
inference(resolution,[],[f23766,f21086]) ).
fof(f23771,plain,
( ! [X0] :
( ~ m1_subset_1(sK53,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ m1_altcat_2(X0,k5_waybel34(sK52))
| v3_struct_0(k5_waybel34(sK52))
| ~ l2_altcat_1(k5_waybel34(sK52)) )
| spl356_5 ),
inference(resolution,[],[f23766,f21515]) ).
fof(f23789,plain,
( ~ v3_lattice3(sK53)
| ~ r2_hidden(u1_struct_0(sK53),sK52)
| ~ v2_orders_2(sK53)
| ~ v3_orders_2(sK53)
| ~ v4_orders_2(sK53)
| ~ v1_lattice3(sK53)
| ~ v2_lattice3(sK53)
| ~ l1_orders_2(sK53)
| v2_setfam_1(sK52)
| spl356_1
| spl356_5 ),
inference(forward_subsumption_resolution,[],[f23768,f23687]) ).
fof(f23792,plain,
( ~ r2_hidden(u1_struct_0(sK53),sK52)
| ~ v2_orders_2(sK53)
| ~ v3_orders_2(sK53)
| ~ v4_orders_2(sK53)
| ~ v1_lattice3(sK53)
| ~ v2_lattice3(sK53)
| ~ l1_orders_2(sK53)
| v2_setfam_1(sK52)
| spl356_1
| spl356_5 ),
inference(forward_subsumption_resolution,[],[f23789,f23688]) ).
fof(f23795,plain,
( ~ v2_orders_2(sK53)
| ~ v3_orders_2(sK53)
| ~ v4_orders_2(sK53)
| ~ v1_lattice3(sK53)
| ~ v2_lattice3(sK53)
| ~ l1_orders_2(sK53)
| v2_setfam_1(sK52)
| spl356_1
| spl356_5 ),
inference(forward_subsumption_resolution,[],[f23792,f23689]) ).
fof(f23798,plain,
( ~ v3_orders_2(sK53)
| ~ v4_orders_2(sK53)
| ~ v1_lattice3(sK53)
| ~ v2_lattice3(sK53)
| ~ l1_orders_2(sK53)
| v2_setfam_1(sK52)
| spl356_1
| spl356_5 ),
inference(forward_subsumption_resolution,[],[f23795,f21339]) ).
fof(f23801,plain,
( ~ v4_orders_2(sK53)
| ~ v1_lattice3(sK53)
| ~ v2_lattice3(sK53)
| ~ l1_orders_2(sK53)
| v2_setfam_1(sK52)
| spl356_1
| spl356_5 ),
inference(forward_subsumption_resolution,[],[f23798,f21338]) ).
fof(f23804,plain,
( ~ v1_lattice3(sK53)
| ~ v2_lattice3(sK53)
| ~ l1_orders_2(sK53)
| v2_setfam_1(sK52)
| spl356_1
| spl356_5 ),
inference(forward_subsumption_resolution,[],[f23801,f21337]) ).
fof(f23807,plain,
( ~ v2_lattice3(sK53)
| ~ l1_orders_2(sK53)
| v2_setfam_1(sK52)
| spl356_1
| spl356_5 ),
inference(forward_subsumption_resolution,[],[f23804,f21336]) ).
fof(f23810,plain,
( ~ l1_orders_2(sK53)
| v2_setfam_1(sK52)
| spl356_1
| spl356_5 ),
inference(forward_subsumption_resolution,[],[f23807,f21335]) ).
fof(f23811,plain,
( v2_setfam_1(sK52)
| spl356_1
| spl356_5 ),
inference(forward_subsumption_resolution,[],[f23810,f21334]) ).
fof(f23812,plain,
( $false
| spl356_1
| spl356_5 ),
inference(forward_subsumption_resolution,[],[f23811,f21333]) ).
fof(f23813,plain,
( spl356_1
| spl356_5 ),
inference(avatar_contradiction_clause,[],[f23812]) ).
fof(f23815,definition,
( spl356_6
<=> v2_setfam_1(sK52) ),
introduced(definition,[new_symbols(definition,[spl356_6])],[avatar_definition]) ).
fof(f23817,plain,
( ~ v2_setfam_1(sK52)
| spl356_6 ),
inference(avatar_component_clause,[],[f23815]) ).
fof(f23818,plain,
~ spl356_6,
inference(avatar_split_clause,[],[f21333,f23815]) ).
fof(f23820,definition,
( spl356_7
<=> l1_orders_2(sK53) ),
introduced(definition,[new_symbols(definition,[spl356_7])],[avatar_definition]) ).
fof(f23822,plain,
( l1_orders_2(sK53)
| ~ spl356_7 ),
inference(avatar_component_clause,[],[f23820]) ).
fof(f23823,plain,
spl356_7,
inference(avatar_split_clause,[],[f21334,f23820]) ).
fof(f23825,definition,
( spl356_8
<=> v2_orders_2(sK53) ),
introduced(definition,[new_symbols(definition,[spl356_8])],[avatar_definition]) ).
fof(f23827,plain,
( v2_orders_2(sK53)
| ~ spl356_8 ),
inference(avatar_component_clause,[],[f23825]) ).
fof(f23828,plain,
spl356_8,
inference(avatar_split_clause,[],[f21339,f23825]) ).
fof(f23830,definition,
( spl356_9
<=> v3_orders_2(sK53) ),
introduced(definition,[new_symbols(definition,[spl356_9])],[avatar_definition]) ).
fof(f23832,plain,
( v3_orders_2(sK53)
| ~ spl356_9 ),
inference(avatar_component_clause,[],[f23830]) ).
fof(f23833,plain,
spl356_9,
inference(avatar_split_clause,[],[f21338,f23830]) ).
fof(f23835,definition,
( spl356_10
<=> v2_lattice3(sK53) ),
introduced(definition,[new_symbols(definition,[spl356_10])],[avatar_definition]) ).
fof(f23837,plain,
( v2_lattice3(sK53)
| ~ spl356_10 ),
inference(avatar_component_clause,[],[f23835]) ).
fof(f23838,plain,
spl356_10,
inference(avatar_split_clause,[],[f21335,f23835]) ).
fof(f23840,definition,
( spl356_11
<=> v4_orders_2(sK53) ),
introduced(definition,[new_symbols(definition,[spl356_11])],[avatar_definition]) ).
fof(f23842,plain,
( v4_orders_2(sK53)
| ~ spl356_11 ),
inference(avatar_component_clause,[],[f23840]) ).
fof(f23843,plain,
spl356_11,
inference(avatar_split_clause,[],[f21337,f23840]) ).
fof(f23904,plain,
( ~ v3_struct_0(k5_waybel34(sK52))
| spl356_6 ),
inference(resolution,[],[f23817,f21073]) ).
fof(f23923,plain,
( u1_struct_0(k5_waybel34(sK52)) = u1_struct_0(k4_waybel34(sK52))
| spl356_6 ),
inference(resolution,[],[f23817,f21092]) ).
fof(f24002,plain,
( ~ v1_xboole_0(sK52)
| spl356_6 ),
inference(resolution,[],[f23817,f21501]) ).
fof(f24025,plain,
( ! [X0] :
( ~ m1_subset_1(sK53,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ m1_altcat_2(X0,k5_waybel34(sK52))
| ~ l2_altcat_1(k5_waybel34(sK52)) )
| spl356_5
| spl356_6 ),
inference(backward_subsumption_resolution,[],[f23771,f23904]) ).
fof(f24329,definition,
( spl356_13
<=> v1_lattice3(sK53) ),
introduced(definition,[new_symbols(definition,[spl356_13])],[avatar_definition]) ).
fof(f24331,plain,
( v1_lattice3(sK53)
| ~ spl356_13 ),
inference(avatar_component_clause,[],[f24329]) ).
fof(f24332,plain,
spl356_13,
inference(avatar_split_clause,[],[f21336,f24329]) ).
fof(f24542,plain,
( ! [X0] :
( v3_lattice3(sK53)
| ~ m1_subset_1(sK53,u1_struct_0(k5_waybel34(X0)))
| ~ v2_orders_2(sK53)
| ~ v3_orders_2(sK53)
| ~ v4_orders_2(sK53)
| ~ v1_lattice3(sK53)
| ~ v2_lattice3(sK53)
| v2_setfam_1(X0) )
| ~ spl356_7 ),
inference(resolution,[],[f23822,f21084]) ).
fof(f36504,plain,
( ! [X0] :
( v3_lattice3(sK53)
| ~ m1_subset_1(sK53,u1_struct_0(k5_waybel34(X0)))
| ~ v3_orders_2(sK53)
| ~ v4_orders_2(sK53)
| ~ v1_lattice3(sK53)
| ~ v2_lattice3(sK53)
| v2_setfam_1(X0) )
| ~ spl356_7
| ~ spl356_8 ),
inference(forward_subsumption_resolution,[],[f24542,f23827]) ).
fof(f36572,plain,
( ! [X0] :
( v3_lattice3(sK53)
| ~ m1_subset_1(sK53,u1_struct_0(k5_waybel34(X0)))
| ~ v4_orders_2(sK53)
| ~ v1_lattice3(sK53)
| ~ v2_lattice3(sK53)
| v2_setfam_1(X0) )
| ~ spl356_7
| ~ spl356_8
| ~ spl356_9 ),
inference(forward_subsumption_resolution,[],[f36504,f23832]) ).
fof(f36640,plain,
( ! [X0] :
( v3_lattice3(sK53)
| ~ m1_subset_1(sK53,u1_struct_0(k5_waybel34(X0)))
| ~ v1_lattice3(sK53)
| ~ v2_lattice3(sK53)
| v2_setfam_1(X0) )
| ~ spl356_7
| ~ spl356_8
| ~ spl356_9
| ~ spl356_11 ),
inference(forward_subsumption_resolution,[],[f36572,f23842]) ).
fof(f36708,plain,
( ! [X0] :
( v3_lattice3(sK53)
| ~ m1_subset_1(sK53,u1_struct_0(k5_waybel34(X0)))
| ~ v2_lattice3(sK53)
| v2_setfam_1(X0) )
| ~ spl356_7
| ~ spl356_8
| ~ spl356_9
| ~ spl356_11
| ~ spl356_13 ),
inference(forward_subsumption_resolution,[],[f36640,f24331]) ).
fof(f36776,plain,
( ! [X0] :
( v3_lattice3(sK53)
| ~ m1_subset_1(sK53,u1_struct_0(k5_waybel34(X0)))
| v2_setfam_1(X0) )
| ~ spl356_7
| ~ spl356_8
| ~ spl356_9
| ~ spl356_10
| ~ spl356_11
| ~ spl356_13 ),
inference(forward_subsumption_resolution,[],[f36708,f23837]) ).
fof(f36872,plain,
( ~ m1_subset_1(sK53,u1_struct_0(k8_waybel34(sK52)))
| ~ v2_orders_2(sK53)
| ~ v3_orders_2(sK53)
| ~ v4_orders_2(sK53)
| ~ v1_lattice3(sK53)
| ~ v2_lattice3(sK53)
| ~ l1_orders_2(sK53)
| v2_setfam_1(sK52)
| spl356_2 ),
inference(resolution,[],[f23677,f21323]) ).
fof(f36887,plain,
( ~ m1_subset_1(sK53,u1_struct_0(k8_waybel34(sK52)))
| ~ v3_orders_2(sK53)
| ~ v4_orders_2(sK53)
| ~ v1_lattice3(sK53)
| ~ v2_lattice3(sK53)
| ~ l1_orders_2(sK53)
| v2_setfam_1(sK52)
| spl356_2
| ~ spl356_8 ),
inference(forward_subsumption_resolution,[],[f36872,f23827]) ).
fof(f36891,plain,
( ~ m1_subset_1(sK53,u1_struct_0(k8_waybel34(sK52)))
| ~ v4_orders_2(sK53)
| ~ v1_lattice3(sK53)
| ~ v2_lattice3(sK53)
| ~ l1_orders_2(sK53)
| v2_setfam_1(sK52)
| spl356_2
| ~ spl356_8
| ~ spl356_9 ),
inference(forward_subsumption_resolution,[],[f36887,f23832]) ).
fof(f36895,plain,
( ~ m1_subset_1(sK53,u1_struct_0(k8_waybel34(sK52)))
| ~ v1_lattice3(sK53)
| ~ v2_lattice3(sK53)
| ~ l1_orders_2(sK53)
| v2_setfam_1(sK52)
| spl356_2
| ~ spl356_8
| ~ spl356_9
| ~ spl356_11 ),
inference(forward_subsumption_resolution,[],[f36891,f23842]) ).
fof(f36899,plain,
( ~ m1_subset_1(sK53,u1_struct_0(k8_waybel34(sK52)))
| ~ v2_lattice3(sK53)
| ~ l1_orders_2(sK53)
| v2_setfam_1(sK52)
| spl356_2
| ~ spl356_8
| ~ spl356_9
| ~ spl356_11
| ~ spl356_13 ),
inference(forward_subsumption_resolution,[],[f36895,f24331]) ).
fof(f36903,plain,
( ~ m1_subset_1(sK53,u1_struct_0(k8_waybel34(sK52)))
| ~ l1_orders_2(sK53)
| v2_setfam_1(sK52)
| spl356_2
| ~ spl356_8
| ~ spl356_9
| ~ spl356_10
| ~ spl356_11
| ~ spl356_13 ),
inference(forward_subsumption_resolution,[],[f36899,f23837]) ).
fof(f36907,plain,
( ~ m1_subset_1(sK53,u1_struct_0(k8_waybel34(sK52)))
| v2_setfam_1(sK52)
| spl356_2
| ~ spl356_7
| ~ spl356_8
| ~ spl356_9
| ~ spl356_10
| ~ spl356_11
| ~ spl356_13 ),
inference(forward_subsumption_resolution,[],[f36903,f23822]) ).
fof(f36909,plain,
( ~ m1_subset_1(sK53,u1_struct_0(k8_waybel34(sK52)))
| spl356_2
| spl356_6
| ~ spl356_7
| ~ spl356_8
| ~ spl356_9
| ~ spl356_10
| ~ spl356_11
| ~ spl356_13 ),
inference(forward_subsumption_resolution,[],[f36907,f23817]) ).
fof(f36912,definition,
( spl356_15
<=> m1_subset_1(sK53,u1_struct_0(k8_waybel34(sK52))) ),
introduced(definition,[new_symbols(definition,[spl356_15])],[avatar_definition]) ).
fof(f36914,plain,
( ~ m1_subset_1(sK53,u1_struct_0(k8_waybel34(sK52)))
| spl356_15 ),
inference(avatar_component_clause,[],[f36912]) ).
fof(f36915,plain,
( ~ spl356_15
| spl356_2
| spl356_6
| ~ spl356_7
| ~ spl356_8
| ~ spl356_9
| ~ spl356_10
| ~ spl356_11
| ~ spl356_13 ),
inference(avatar_split_clause,[],[f36909,f24329,f23840,f23835,f23830,f23825,f23820,f23815,f23675,f36912]) ).
fof(f36917,plain,
( ~ m1_subset_1(sK53,u1_struct_0(k4_waybel34(sK52)))
| v3_struct_0(k8_waybel34(sK52))
| ~ v2_altcat_1(k8_waybel34(sK52))
| ~ v6_altcat_1(k8_waybel34(sK52))
| ~ v3_altcat_2(k8_waybel34(sK52),k4_waybel34(sK52))
| ~ m1_altcat_2(k8_waybel34(sK52),k4_waybel34(sK52))
| v1_xboole_0(sK52)
| spl356_15 ),
inference(resolution,[],[f36914,f23393]) ).
fof(f36970,plain,
( ~ m1_subset_1(sK53,u1_struct_0(k4_waybel34(sK52)))
| ~ v2_altcat_1(k8_waybel34(sK52))
| ~ v6_altcat_1(k8_waybel34(sK52))
| ~ v3_altcat_2(k8_waybel34(sK52),k4_waybel34(sK52))
| ~ m1_altcat_2(k8_waybel34(sK52),k4_waybel34(sK52))
| v1_xboole_0(sK52)
| spl356_15 ),
inference(forward_subsumption_resolution,[],[f36917,f20897]) ).
fof(f36985,plain,
( ~ m1_subset_1(sK53,u1_struct_0(k4_waybel34(sK52)))
| ~ v6_altcat_1(k8_waybel34(sK52))
| ~ v3_altcat_2(k8_waybel34(sK52),k4_waybel34(sK52))
| ~ m1_altcat_2(k8_waybel34(sK52),k4_waybel34(sK52))
| v1_xboole_0(sK52)
| spl356_15 ),
inference(forward_subsumption_resolution,[],[f36970,f20896]) ).
fof(f36990,plain,
( ~ m1_subset_1(sK53,u1_struct_0(k4_waybel34(sK52)))
| ~ v3_altcat_2(k8_waybel34(sK52),k4_waybel34(sK52))
| ~ m1_altcat_2(k8_waybel34(sK52),k4_waybel34(sK52))
| v1_xboole_0(sK52)
| spl356_15 ),
inference(forward_subsumption_resolution,[],[f36985,f20895]) ).
fof(f36993,plain,
( ~ m1_subset_1(sK53,u1_struct_0(k4_waybel34(sK52)))
| ~ m1_altcat_2(k8_waybel34(sK52),k4_waybel34(sK52))
| v1_xboole_0(sK52)
| spl356_15 ),
inference(forward_subsumption_resolution,[],[f36990,f20894]) ).
fof(f36996,plain,
( ~ m1_subset_1(sK53,u1_struct_0(k4_waybel34(sK52)))
| v1_xboole_0(sK52)
| spl356_15 ),
inference(forward_subsumption_resolution,[],[f36993,f20893]) ).
fof(f36999,plain,
( ~ m1_subset_1(sK53,u1_struct_0(k4_waybel34(sK52)))
| spl356_6
| spl356_15 ),
inference(forward_subsumption_resolution,[],[f36996,f24002]) ).
fof(f37002,plain,
( ~ m1_subset_1(sK53,u1_struct_0(k5_waybel34(sK52)))
| spl356_6
| spl356_15 ),
inference(forward_demodulation,[],[f36999,f23923]) ).
fof(f59000,definition,
( spl356_32
<=> ! [X0] :
( ~ m1_subset_1(sK53,u1_struct_0(k5_waybel34(X0)))
| v2_setfam_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl356_32])],[avatar_definition]) ).
fof(f59001,plain,
( ! [X0] :
( ~ m1_subset_1(sK53,u1_struct_0(k5_waybel34(X0)))
| v2_setfam_1(X0) )
| ~ spl356_32 ),
inference(avatar_component_clause,[],[f59000]) ).
fof(f59555,definition,
( spl356_43
<=> v1_xboole_0(sK52) ),
introduced(definition,[new_symbols(definition,[spl356_43])],[avatar_definition]) ).
fof(f59557,plain,
( ~ v1_xboole_0(sK52)
| spl356_43 ),
inference(avatar_component_clause,[],[f59555]) ).
fof(f59558,plain,
( ~ spl356_43
| spl356_6 ),
inference(avatar_split_clause,[],[f24002,f23815,f59555]) ).
fof(f61760,plain,
( spl356_32
| spl356_3
| ~ spl356_7
| ~ spl356_8
| ~ spl356_9
| ~ spl356_10
| ~ spl356_11
| ~ spl356_13 ),
inference(avatar_split_clause,[],[f36776,f24329,f23840,f23835,f23830,f23825,f23820,f23679,f59000]) ).
fof(f65215,plain,
( l2_altcat_1(k5_waybel34(sK52))
| spl356_43 ),
inference(resolution,[],[f59557,f20880]) ).
fof(f66330,plain,
( ! [X0] :
( ~ m1_subset_1(sK53,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ m1_altcat_2(X0,k5_waybel34(sK52)) )
| spl356_5
| spl356_6
| spl356_43 ),
inference(backward_subsumption_resolution,[],[f24025,f65215]) ).
fof(f72684,definition,
( spl356_82
<=> ! [X0] :
( ~ m1_subset_1(sK53,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ m1_altcat_2(X0,k5_waybel34(sK52)) ) ),
introduced(definition,[new_symbols(definition,[spl356_82])],[avatar_definition]) ).
fof(f72685,plain,
( ! [X0] :
( ~ m1_altcat_2(X0,k5_waybel34(sK52))
| v3_struct_0(X0)
| ~ m1_subset_1(sK53,u1_struct_0(X0)) )
| ~ spl356_82 ),
inference(avatar_component_clause,[],[f72684]) ).
fof(f72686,plain,
( spl356_82
| spl356_5
| spl356_6
| spl356_43 ),
inference(avatar_split_clause,[],[f66330,f59555,f23815,f23764,f72684]) ).
fof(f72690,plain,
( v3_struct_0(k9_waybel34(sK52))
| ~ m1_subset_1(sK53,u1_struct_0(k9_waybel34(sK52)))
| v2_setfam_1(sK52)
| ~ spl356_82 ),
inference(resolution,[],[f72685,f20898]) ).
fof(f72720,plain,
( ~ m1_subset_1(sK53,u1_struct_0(k9_waybel34(sK52)))
| v2_setfam_1(sK52)
| ~ spl356_82 ),
inference(forward_subsumption_resolution,[],[f72690,f20902]) ).
fof(f72731,plain,
( v2_setfam_1(sK52)
| ~ spl356_1
| ~ spl356_82 ),
inference(forward_subsumption_resolution,[],[f72720,f23672]) ).
fof(f72740,plain,
( $false
| ~ spl356_1
| spl356_6
| ~ spl356_82 ),
inference(forward_subsumption_resolution,[],[f72731,f23817]) ).
fof(f72741,plain,
( ~ spl356_1
| spl356_6
| ~ spl356_82 ),
inference(avatar_contradiction_clause,[],[f72740]) ).
fof(f72754,plain,
( $false
| ~ spl356_5
| spl356_6
| spl356_15 ),
inference(forward_subsumption_resolution,[],[f37002,f23765]) ).
fof(f72755,plain,
( ~ spl356_5
| spl356_6
| spl356_15 ),
inference(avatar_contradiction_clause,[],[f72754]) ).
fof(f72761,plain,
( v2_setfam_1(sK52)
| ~ spl356_5
| ~ spl356_32 ),
inference(resolution,[],[f23765,f59001]) ).
fof(f72770,plain,
( v1_orders_2(sK53)
| ~ v2_orders_2(sK53)
| ~ v3_orders_2(sK53)
| ~ v4_orders_2(sK53)
| ~ v1_lattice3(sK53)
| ~ v2_lattice3(sK53)
| ~ l1_orders_2(sK53)
| v2_setfam_1(sK52)
| ~ spl356_5 ),
inference(resolution,[],[f23765,f21085]) ).
fof(f73482,plain,
( ~ v2_orders_2(sK53)
| ~ v3_orders_2(sK53)
| ~ v4_orders_2(sK53)
| ~ v1_lattice3(sK53)
| ~ v2_lattice3(sK53)
| ~ l1_orders_2(sK53)
| v2_setfam_1(sK52)
| spl356_4
| ~ spl356_5 ),
inference(forward_subsumption_resolution,[],[f72770,f23685]) ).
fof(f73485,plain,
( $false
| ~ spl356_5
| spl356_6
| ~ spl356_32 ),
inference(forward_subsumption_resolution,[],[f72761,f23817]) ).
fof(f73486,plain,
( ~ spl356_5
| spl356_6
| ~ spl356_32 ),
inference(avatar_contradiction_clause,[],[f73485]) ).
fof(f73607,plain,
( ~ v3_orders_2(sK53)
| ~ v4_orders_2(sK53)
| ~ v1_lattice3(sK53)
| ~ v2_lattice3(sK53)
| ~ l1_orders_2(sK53)
| v2_setfam_1(sK52)
| spl356_4
| ~ spl356_5
| ~ spl356_8 ),
inference(forward_subsumption_resolution,[],[f73482,f23827]) ).
fof(f73699,plain,
( ~ v4_orders_2(sK53)
| ~ v1_lattice3(sK53)
| ~ v2_lattice3(sK53)
| ~ l1_orders_2(sK53)
| v2_setfam_1(sK52)
| spl356_4
| ~ spl356_5
| ~ spl356_8
| ~ spl356_9 ),
inference(forward_subsumption_resolution,[],[f73607,f23832]) ).
fof(f73762,plain,
( ~ v1_lattice3(sK53)
| ~ v2_lattice3(sK53)
| ~ l1_orders_2(sK53)
| v2_setfam_1(sK52)
| spl356_4
| ~ spl356_5
| ~ spl356_8
| ~ spl356_9
| ~ spl356_11 ),
inference(forward_subsumption_resolution,[],[f73699,f23842]) ).
fof(f73821,plain,
( ~ v2_lattice3(sK53)
| ~ l1_orders_2(sK53)
| v2_setfam_1(sK52)
| spl356_4
| ~ spl356_5
| ~ spl356_8
| ~ spl356_9
| ~ spl356_11
| ~ spl356_13 ),
inference(forward_subsumption_resolution,[],[f73762,f24331]) ).
fof(f73880,plain,
( ~ l1_orders_2(sK53)
| v2_setfam_1(sK52)
| spl356_4
| ~ spl356_5
| ~ spl356_8
| ~ spl356_9
| ~ spl356_10
| ~ spl356_11
| ~ spl356_13 ),
inference(forward_subsumption_resolution,[],[f73821,f23837]) ).
fof(f73899,plain,
( v2_setfam_1(sK52)
| spl356_4
| ~ spl356_5
| ~ spl356_7
| ~ spl356_8
| ~ spl356_9
| ~ spl356_10
| ~ spl356_11
| ~ spl356_13 ),
inference(forward_subsumption_resolution,[],[f73880,f23822]) ).
fof(f73908,plain,
( $false
| spl356_4
| ~ spl356_5
| spl356_6
| ~ spl356_7
| ~ spl356_8
| ~ spl356_9
| ~ spl356_10
| ~ spl356_11
| ~ spl356_13 ),
inference(forward_subsumption_resolution,[],[f73899,f23817]) ).
fof(f73909,plain,
( spl356_4
| ~ spl356_5
| spl356_6
| ~ spl356_7
| ~ spl356_8
| ~ spl356_9
| ~ spl356_10
| ~ spl356_11
| ~ spl356_13 ),
inference(avatar_contradiction_clause,[],[f73908]) ).
cnf(s1,plain,
( ~ spl356_1
| ~ spl356_2
| ~ spl356_3
| ~ spl356_4 ),
inference(sat_conversion,[],[f23686]) ).
cnf(s2,plain,
( spl356_1
| ~ spl356_5 ),
inference(sat_conversion,[],[f23767]) ).
cnf(s3,plain,
( spl356_1
| spl356_5 ),
inference(sat_conversion,[],[f23813]) ).
cnf(s4,plain,
~ spl356_6,
inference(sat_conversion,[],[f23818]) ).
cnf(s5,plain,
spl356_7,
inference(sat_conversion,[],[f23823]) ).
cnf(s6,plain,
spl356_8,
inference(sat_conversion,[],[f23828]) ).
cnf(s7,plain,
spl356_9,
inference(sat_conversion,[],[f23833]) ).
cnf(s8,plain,
spl356_10,
inference(sat_conversion,[],[f23838]) ).
cnf(s9,plain,
spl356_11,
inference(sat_conversion,[],[f23843]) ).
cnf(s11,plain,
spl356_13,
inference(sat_conversion,[],[f24332]) ).
cnf(s13,plain,
( spl356_2
| spl356_6
| ~ spl356_7
| ~ spl356_8
| ~ spl356_9
| ~ spl356_10
| ~ spl356_11
| ~ spl356_13
| ~ spl356_15 ),
inference(sat_conversion,[],[f36915]) ).
cnf(s38,plain,
( spl356_6
| ~ spl356_43 ),
inference(sat_conversion,[],[f59558]) ).
cnf(s41,plain,
( spl356_3
| ~ spl356_7
| ~ spl356_8
| ~ spl356_9
| ~ spl356_10
| ~ spl356_11
| ~ spl356_13
| spl356_32 ),
inference(sat_conversion,[],[f61760]) ).
cnf(s88,plain,
( spl356_5
| spl356_6
| spl356_43
| spl356_82 ),
inference(sat_conversion,[],[f72686]) ).
cnf(s90,plain,
( ~ spl356_1
| spl356_6
| ~ spl356_82 ),
inference(sat_conversion,[],[f72741]) ).
cnf(s91,plain,
( ~ spl356_5
| spl356_6
| spl356_15 ),
inference(sat_conversion,[],[f72755]) ).
cnf(s92,plain,
( ~ spl356_5
| spl356_6
| ~ spl356_32 ),
inference(sat_conversion,[],[f73486]) ).
cnf(s93,plain,
( spl356_4
| ~ spl356_5
| spl356_6
| ~ spl356_7
| ~ spl356_8
| ~ spl356_9
| ~ spl356_10
| ~ spl356_11
| ~ spl356_13 ),
inference(sat_conversion,[],[f73909]) ).
cnf(s113,plain,
~ spl356_43,
inference(rat,[],[s38,s4]) ).
cnf(s128,plain,
spl356_1,
inference(rat,[],[s2,s3]) ).
cnf(s129,plain,
~ spl356_82,
inference(rat,[],[s90,s4,s128]) ).
cnf(s141,plain,
spl356_5,
inference(rat,[],[s88,s113,s4,s129]) ).
cnf(s142,plain,
spl356_4,
inference(rat,[],[s93,s11,s9,s8,s7,s6,s5,s4,s141]) ).
cnf(s143,plain,
~ spl356_32,
inference(rat,[],[s92,s4,s141]) ).
cnf(s144,plain,
spl356_15,
inference(rat,[],[s91,s4,s141]) ).
cnf(s145,plain,
spl356_3,
inference(rat,[],[s41,s5,s11,s9,s8,s7,s6,s143]) ).
cnf(s146,plain,
spl356_2,
inference(rat,[],[s13,s4,s11,s9,s8,s7,s6,s5,s144]) ).
cnf(s152,plain,
$false,
inference(rat,[],[s1,s142,s128,s145,s146]) ).
fof(f73932,plain,
$false,
inference(avatar_sat_refutation,[],[s152]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT374+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.38 % Computer : n016.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:13:21 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.42 Running first-order theorem proving
% 0.10/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 16.17/4.07 % (2763140)Detected formulas, will run a generic FOF schedule.
% 16.17/4.07 % (2763150)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=53906731:s2a=on:i=139:gtg=position_2988 on theBenchmark for (2988ds/139Mi)
% 16.17/4.07 % (2763150)Instruction limit reached!
% 16.17/4.07 % (2763150)------------------------------
% 16.17/4.07 % (2763150)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.17/4.07 % (2763150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.17/4.07 % (2763150)CaDiCaL version: 2.1.3
% 16.17/4.07 % (2763150)Termination reason: Instruction limit
% 16.17/4.07 % (2763150)Termination phase: Property scanning
% 16.17/4.07 % (2763150)Time elapsed: 0.034 s
% 16.17/4.07 % (2763150)Peak memory usage: 112 MB
% 16.17/4.07 % (2763150)Instructions burned: 143 (million)
% 16.17/4.07 % (2763148)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2882166762:i=109:sd=1:ins=1:gsp=on:ss=axioms_2988 on theBenchmark for (2988ds/109Mi)
% 16.17/4.07 % (2763151)dis-21_1_sil=8000:lcm=predicate:random_seed=2106052199:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2988 on theBenchmark for (2988ds/129Mi)
% 16.17/4.07 % (2763145)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=2925201546:i=141193_2988 on theBenchmark for (2988ds/141193Mi)
% 16.17/4.07 % (2763149)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3088333917:i=119:av=off:ss=axioms_2988 on theBenchmark for (2988ds/119Mi)
% 16.17/4.07 % (2763146)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=1320340205:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2988 on theBenchmark for (2988ds/134677Mi)
% 16.17/4.07 % (2763147)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=492982532:i=141695:sd=1:nm=32:gsp=on:ss=included_2988 on theBenchmark for (2988ds/141695Mi)
% 16.17/4.07 % (2763148)Instruction limit reached!
% 16.17/4.07 % (2763148)------------------------------
% 16.17/4.07 % (2763148)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.17/4.07 % (2763148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.17/4.07 % (2763148)CaDiCaL version: 2.1.3
% 16.17/4.07 % (2763148)Termination reason: Instruction limit
% 16.17/4.07 % (2763148)Termination phase: SInE selection
% 16.17/4.07 % (2763148)Time elapsed: 0.085 s
% 16.17/4.07 % (2763148)Peak memory usage: 112 MB
% 16.17/4.07 % (2763148)Instructions burned: 110 (million)
% 16.17/4.07 % (2763151)Instruction limit reached!
% 16.17/4.07 % (2763151)------------------------------
% 16.17/4.07 % (2763151)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.17/4.07 % (2763151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.17/4.07 % (2763151)CaDiCaL version: 2.1.3
% 16.17/4.07 % (2763151)Termination reason: Instruction limit
% 16.17/4.07 % (2763151)Termination phase: SInE selection
% 16.17/4.07 % (2763151)Time elapsed: 0.086 s
% 16.17/4.07 % (2763151)Peak memory usage: 112 MB
% 16.17/4.07 % (2763151)Instructions burned: 130 (million)
% 16.17/4.07 % (2763149)Instruction limit reached!
% 16.17/4.07 % (2763149)------------------------------
% 16.17/4.07 % (2763149)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.17/4.07 % (2763149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.17/4.07 % (2763149)CaDiCaL version: 2.1.3
% 16.17/4.07 % (2763149)Termination reason: Instruction limit
% 16.17/4.07 % (2763149)Termination phase: Preprocessing 1
% 16.17/4.07 % (2763149)Time elapsed: 0.101 s
% 16.17/4.07 % (2763149)Peak memory usage: 112 MB
% 16.17/4.07 % (2763149)Instructions burned: 119 (million)
% 16.17/4.07 % (2763153)lrs+10_1_sil=8000:sp=occurrence:random_seed=2560152195:i=285:sd=3:ss=axioms:sgt=8_2987 on theBenchmark for (2987ds/285Mi)
% 16.17/4.07 % (2763153)Instruction limit reached!
% 16.17/4.07 % (2763153)------------------------------
% 16.17/4.07 % (2763153)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.17/4.07 % (2763153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.17/4.07 % (2763153)CaDiCaL version: 2.1.3
% 16.17/4.07 % (2763153)Termination reason: Instruction limit
% 16.17/4.07 % (2763153)Termination phase: Saturation
% 16.17/4.07 % (2763153)Time elapsed: 0.120 s
% 16.17/4.07 % (2763153)Peak memory usage: 120 MB
% 16.17/4.07 % (2763153)Instructions burned: 287 (million)
% 23.29/5.11 % (2763161)lrs+1011_1_sil=32000:sp=occurrence:random_seed=542209491:i=325:sd=1:ss=axioms:sgt=32_2986 on theBenchmark for (2986ds/325Mi)
% 23.29/5.11 % (2763160)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2692593952:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2986 on theBenchmark for (2986ds/157Mi)
% 23.29/5.11 % (2763162)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=1492103568:s2a=on:i=248:s2at=1.23:gtg=position_2986 on theBenchmark for (2986ds/248Mi)
% 23.29/5.11 % (2763160)Instruction limit reached!
% 23.29/5.11 % (2763160)------------------------------
% 23.29/5.11 % (2763160)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.29/5.11 % (2763160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.29/5.11 % (2763160)CaDiCaL version: 2.1.3
% 23.29/5.11 % (2763160)Termination reason: Instruction limit
% 23.29/5.11 % (2763160)Termination phase: Property scanning
% 23.29/5.11 % (2763160)Time elapsed: 0.070 s
% 23.29/5.11 % (2763160)Peak memory usage: 112 MB
% 23.29/5.11 % (2763160)Instructions burned: 159 (million)
% 23.29/5.11 % (2763164)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3494991956:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2984 on theBenchmark for (2984ds/294Mi)
% 23.29/5.11 % (2763162)Instruction limit reached!
% 23.29/5.11 % (2763162)------------------------------
% 23.29/5.11 % (2763162)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.29/5.11 % (2763162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.29/5.11 % (2763162)CaDiCaL version: 2.1.3
% 23.29/5.11 % (2763162)Termination reason: Instruction limit
% 23.29/5.11 % (2763162)Termination phase: Property scanning
% 23.29/5.11 % (2763162)Time elapsed: 0.108 s
% 23.29/5.11 % (2763162)Peak memory usage: 112 MB
% 23.29/5.11 % (2763162)Instructions burned: 249 (million)
% 23.29/5.11 % (2763164)Instruction limit reached!
% 23.29/5.11 % (2763164)------------------------------
% 23.29/5.11 % (2763164)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.29/5.11 % (2763164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.29/5.11 % (2763164)CaDiCaL version: 2.1.3
% 23.29/5.11 % (2763164)Termination reason: Instruction limit
% 23.29/5.11 % (2763164)Termination phase: Property scanning
% 23.29/5.11 % (2763164)Time elapsed: 0.115 s
% 23.29/5.11 % (2763164)Peak memory usage: 118 MB
% 23.29/5.11 % (2763164)Instructions burned: 295 (million)
% 23.29/5.11 % (2763168)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=26501980:i=2350_2983 on theBenchmark for (2983ds/2350Mi)
% 23.29/5.11 % (2763161)Instruction limit reached!
% 23.29/5.11 % (2763161)------------------------------
% 23.29/5.11 % (2763161)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.29/5.11 % (2763161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.29/5.11 % (2763161)CaDiCaL version: 2.1.3
% 23.29/5.11 % (2763161)Termination reason: Instruction limit
% 23.29/5.11 % (2763161)Termination phase: Saturation
% 23.29/5.11 % (2763161)Time elapsed: 0.246 s
% 23.29/5.11 % (2763161)Peak memory usage: 118 MB
% 23.29/5.11 % (2763161)Instructions burned: 326 (million)
% 23.29/5.11 % (2763170)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3734514199:cts=off:i=113:fsr=off:ss=included:sgt=4_2983 on theBenchmark for (2983ds/113Mi)
% 23.29/5.11 % (2763171)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=999652402:i=127:av=off:fsr=off:sup=off_2982 on theBenchmark for (2982ds/127Mi)
% 23.29/5.11 % (2763170)Instruction limit reached!
% 23.29/5.11 % (2763170)------------------------------
% 23.29/5.11 % (2763170)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.29/5.11 % (2763170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.29/5.11 % (2763170)CaDiCaL version: 2.1.3
% 23.29/5.11 % (2763170)Termination reason: Instruction limit
% 23.29/5.11 % (2763170)Termination phase: SInE selection
% 23.29/5.11 % (2763170)Time elapsed: 0.092 s
% 23.29/5.11 % (2763170)Peak memory usage: 112 MB
% 23.29/5.11 % (2763170)Instructions burned: 113 (million)
% 23.29/5.11 % (2763171)Instruction limit reached!
% 23.29/5.11 % (2763171)------------------------------
% 23.29/5.11 % (2763171)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.29/5.11 % (2763171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.29/5.11 % (2763171)CaDiCaL version: 2.1.3
% 27.94/6.39 % (2763171)Termination reason: Instruction limit
% 27.94/6.39 % (2763171)Termination phase: Preprocessing 1
% 27.94/6.39 % (2763171)Time elapsed: 0.054 s
% 27.94/6.39 % (2763171)Peak memory usage: 113 MB
% 27.94/6.39 % (2763171)Instructions burned: 128 (million)
% 27.94/6.39 % (2763173)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3209728788:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2982 on theBenchmark for (2982ds/114Mi)
% 27.94/6.39 % (2763173)Instruction limit reached!
% 27.94/6.39 % (2763173)------------------------------
% 27.94/6.39 % (2763173)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.94/6.39 % (2763173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.94/6.39 % (2763173)CaDiCaL version: 2.1.3
% 27.94/6.39 % (2763173)Termination reason: Instruction limit
% 27.94/6.39 % (2763173)Termination phase: Property scanning
% 27.94/6.39 % (2763173)Time elapsed: 0.050 s
% 27.94/6.39 % (2763173)Peak memory usage: 112 MB
% 27.94/6.39 % (2763173)Instructions burned: 115 (million)
% 27.94/6.39 % (2763176)lrs+10_1_sil=8000:sp=occurrence:random_seed=861301518:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2980 on theBenchmark for (2980ds/907Mi)
% 27.94/6.39 % (2763177)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=888281630:i=437:sd=1:aac=none:ss=included_2980 on theBenchmark for (2980ds/437Mi)
% 27.94/6.39 % (2763179)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2255534063:i=5202:ss=axioms:sgt=16_2979 on theBenchmark for (2979ds/5202Mi)
% 27.94/6.39 % (2763177)Instruction limit reached!
% 27.94/6.39 % (2763177)------------------------------
% 27.94/6.39 % (2763177)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.94/6.39 % (2763177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.94/6.39 % (2763177)CaDiCaL version: 2.1.3
% 27.94/6.39 % (2763177)Termination reason: Instruction limit
% 27.94/6.39 % (2763177)Termination phase: Saturation
% 27.94/6.39 % (2763177)Time elapsed: 0.283 s
% 27.94/6.39 % (2763177)Peak memory usage: 123 MB
% 27.94/6.39 % (2763177)Instructions burned: 437 (million)
% 27.94/6.39 % (2763183)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1473407505:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2976 on theBenchmark for (2976ds/134Mi)
% 27.94/6.39 % (2763176)Instruction limit reached!
% 27.94/6.39 % (2763176)------------------------------
% 27.94/6.39 % (2763176)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.94/6.39 % (2763176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.94/6.39 % (2763176)CaDiCaL version: 2.1.3
% 27.94/6.39 % (2763176)Termination reason: Instruction limit
% 27.94/6.39 % (2763176)Termination phase: Property scanning
% 27.94/6.39 % (2763176)Time elapsed: 0.562 s
% 27.94/6.39 % (2763176)Peak memory usage: 133 MB
% 27.94/6.39 % (2763176)Instructions burned: 907 (million)
% 27.94/6.39 % (2763183)Instruction limit reached!
% 27.94/6.39 % (2763183)------------------------------
% 27.94/6.39 % (2763183)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.94/6.39 % (2763183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.94/6.39 % (2763183)CaDiCaL version: 2.1.3
% 27.94/6.39 % (2763183)Termination reason: Instruction limit
% 27.94/6.39 % (2763183)Termination phase: Unused predicate definition removal
% 27.94/6.39 % (2763183)Time elapsed: 0.119 s
% 27.94/6.39 % (2763183)Peak memory usage: 114 MB
% 27.94/6.39 % (2763183)Instructions burned: 134 (million)
% 27.94/6.39 % (2763185)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3163403032:st=8:i=592:sd=3:ep=RST:ss=axioms_2973 on theBenchmark for (2973ds/592Mi)
% 27.94/6.39 % (2763186)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=87673459:st=3:i=13193:sd=3:ss=axioms_2973 on theBenchmark for (2973ds/13193Mi)
% 27.94/6.39 % (2763168)Instruction limit reached!
% 27.94/6.39 % (2763168)------------------------------
% 27.94/6.39 % (2763168)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.94/6.39 % (2763168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.94/6.39 % (2763168)CaDiCaL version: 2.1.3
% 27.94/6.39 % (2763168)Termination reason: Instruction limit
% 27.94/6.39 % (2763168)Termination phase: Property scanning
% 27.94/6.39 % (2763168)Time elapsed: 1.251 s
% 27.94/6.39 % (2763168)Peak memory usage: 171 MB
% 27.94/6.39 % (2763168)Instructions burned: 2352 (million)
% 27.94/6.39 % (2763189)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=3928369382:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2969 on theBenchmark for (2969ds/125Mi)
% 27.94/6.39 % (2763185)Instruction limit reached!
% 27.94/6.39 % (2763185)------------------------------
% 27.94/6.39 % (2763185)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.94/6.39 % (2763185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.94/6.39 % (2763185)CaDiCaL version: 2.1.3
% 27.94/6.39 % (2763185)Termination reason: Instruction limit
% 27.94/6.39 % (2763185)Termination phase: Preprocessing 3
% 27.94/6.39 % (2763185)Time elapsed: 0.439 s
% 27.94/6.39 % (2763185)Peak memory usage: 134 MB
% 27.94/6.39 % (2763185)Instructions burned: 593 (million)
% 27.94/6.39 % (2763189)Instruction limit reached!
% 27.94/6.39 % (2763189)------------------------------
% 27.94/6.39 % (2763189)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.94/6.39 % (2763189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.94/6.39 % (2763189)CaDiCaL version: 2.1.3
% 27.94/6.39 % (2763189)Termination reason: Instruction limit
% 27.94/6.39 % (2763189)Termination phase: Property scanning
% 27.94/6.39 % (2763189)Time elapsed: 0.056 s
% 27.94/6.39 % (2763189)Peak memory usage: 112 MB
% 27.94/6.39 % (2763189)Instructions burned: 127 (million)
% 27.94/6.39 % (2763191)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=540080387:i=134:gtgl=5:slsql=off:gtg=exists_sym_2967 on theBenchmark for (2967ds/134Mi)
% 27.94/6.39 % (2763192)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=554562898:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2967 on theBenchmark for (2967ds/141Mi)
% 27.94/6.39 % (2763191)Instruction limit reached!
% 27.94/6.39 % (2763191)------------------------------
% 27.94/6.39 % (2763191)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.94/6.39 % (2763191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.94/6.39 % (2763191)CaDiCaL version: 2.1.3
% 27.94/6.39 % (2763191)Termination reason: Instruction limit
% 27.94/6.39 % (2763191)Termination phase: Property scanning
% 27.94/6.39 % (2763191)Time elapsed: 0.058 s
% 27.94/6.39 % (2763191)Peak memory usage: 112 MB
% 27.94/6.39 % (2763191)Instructions burned: 135 (million)
% 27.94/6.39 % (2763192)Instruction limit reached!
% 27.94/6.39 % (2763192)------------------------------
% 27.94/6.39 % (2763192)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.94/6.39 % (2763192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.94/6.39 % (2763192)CaDiCaL version: 2.1.3
% 27.94/6.39 % (2763192)Termination reason: Instruction limit
% 27.94/6.39 % (2763192)Termination phase: Saturation
% 27.94/6.39 % (2763192)Time elapsed: 0.118 s
% 27.94/6.39 % (2763192)Peak memory usage: 117 MB
% 27.94/6.39 % (2763192)Instructions burned: 142 (million)
% 27.94/6.39 % (2763195)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3268522595:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2965 on theBenchmark for (2965ds/431Mi)
% 27.94/6.39 % (2763196)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=4249858932:i=6060:aac=none:ins=25_2964 on theBenchmark for (2964ds/6060Mi)
% 27.94/6.39 % (2763195)Instruction limit reached!
% 27.94/6.39 % (2763195)------------------------------
% 27.94/6.39 % (2763195)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.94/6.39 % (2763195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.94/6.39 % (2763195)CaDiCaL version: 2.1.3
% 27.94/6.39 % (2763195)Termination reason: Instruction limit
% 27.94/6.39 % (2763195)Termination phase: Saturation
% 27.94/6.39 % (2763195)Time elapsed: 0.289 s
% 27.94/6.39 % (2763195)Peak memory usage: 120 MB
% 27.94/6.39 % (2763195)Instructions burned: 432 (million)
% 27.94/6.39 % (2763199)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=509593495:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2960 on theBenchmark for (2960ds/150Mi)
% 27.94/6.39 % (2763199)Instruction limit reached!
% 27.94/6.39 % (2763199)------------------------------
% 27.94/6.39 % (2763199)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.94/6.39 % (2763199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.94/6.39 % (2763199)CaDiCaL version: 2.1.3
% 27.94/6.39 % (2763199)Termination reason: Instruction limit
% 27.94/6.39 % (2763199)Termination phase: Preprocessing 1
% 27.94/6.39 % (2763199)Time elapsed: 0.128 s
% 27.94/6.39 % (2763199)Peak memory usage: 113 MB
% 27.94/6.39 % (2763199)Instructions burned: 151 (million)
% 27.94/6.39 % (2763201)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1490395487:i=14155:bd=all_2957 on theBenchmark for (2957ds/14155Mi)
% 27.94/6.39 % (2763147)First to succeed.
% 27.94/6.39 % (2763147)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2763140"
% 27.94/6.39 % (2763147)Refutation found. Thanks to Tanya!
% 27.94/6.39 % SZS status Theorem for theBenchmark
% 27.94/6.39 % SZS output start Proof for theBenchmark
% See solution above
% 32.83/6.60 % (2763147)------------------------------
% 32.83/6.60 % (2763147)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.83/6.60 % (2763147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.83/6.60 % (2763147)CaDiCaL version: 2.1.3
% 32.83/6.60 % (2763147)Termination reason: Refutation
% 32.83/6.60 % (2763147)Time elapsed: 4.002 s
% 32.83/6.60 % (2763147)Peak memory usage: 248 MB
% 32.83/6.60 % (2763147)Instructions burned: 11994 (million)
% 32.83/6.60 % (2763147)------------------------------
% 32.83/6.60 % (2763147)------------------------------
% 32.83/6.60 % (2763140)Success in time 5.532 s
% 32.83/6.60 % Vampire exiting
%------------------------------------------------------------------------------